Steel: Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic
Aymeric Fromherz (Computer Science Department, Carnegie Mellon University,
Pittsburgh, PA, USA; Electrical and Computer Engineering Department,
Carnegie Mellon University)
Aseem
Rastogi (Microsoft Research, Bengaluru, Karnataka, India)
Nikhil
Swamy (RiSE: Research
in Software Engineering, Microsoft Research, Redmond, WA, USA)
Sydney Gibson (CMU ECE)
Guido
Martínez
(CIFASIS-CONICET, Rosario,
Argentina)
Denis Merigoux (Prosecco, INRIA,
Paris, France)
Tahina Ramananandro (RiSE)
ICFP 2021 (accepted for publication, to appear)
Steel is a language for developing and proving concurrent programs embedded
in F*, a dependently typed programming language and proof assistant. Based
on SteelCore, a concurrent separation logic (CSL) formalized in F*, our
work focuses on exposing the proof rules of the logic in a form that
enables programs and proofs to be effectively co-developed.
Our main contributions include a new formulation of a Hoare logic of
quintuples involving both separation logic and first-order logic, enabling
efficient verification condition (VC) generation and proof discharge using
a combination of tactics and SMT solving. We relate the VCs produced by our
quintuple system to solving a system of associativity-commutativity (AC)
unification constraints and develop tactics to (partially) solve these
constraints using AC-matching modulo SMT-dischargeable equations.
Our system is fully mechanized and implemented in F*. We evaluate it by
developing several verified programs and libraries, including various
sequential and concurrent linked data structures, proof libraries, and a
library for 2-party session types. Our experience leads us to conclude that
our system enables a mixture of automated and interactive proof, making it
productive to build programs foundationally verified against a highly
expressive, state-of-the-art CSL.