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.