Steel: proof-oriented programming in a dependently typed concurrent separation logic
Steel: proof-oriented programming in a dependently typed concurrent separation logic
复制标题
Steel：依赖类型并发分离逻辑中的面向证明编程
DOI：
--
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
T. Ramananandro
中科院分区：
文献类型：
--
作者：
Aymeric Fromherz;Aseem Rastogi;N. Swamy;Sydney Gibson;Guido Martínez;Denis Merigoux;T. Ramananandro
Steel是一种用于开发和证明嵌入在F语言中的并发程序的语言，F语言是一种依赖类型的编程语言和证明助手。基于SteelCore（一种用F形式化的并发分离逻辑（CSL）），我们的工作重点是以一种使程序和证明能够有效协同开发的形式公开逻辑的证明规则。我们的主要贡献包括一个新的配方霍尔逻辑的五元组，涉及分离逻辑和一阶逻辑，使有效的验证条件（VC）的生成和证明放电使用的策略和SMT解决的组合。我们与我们的五元组系统产生的VC解决系统的关联性-交换性（AC）统一的约束和开发策略（部分）解决这些约束使用AC匹配模SMT放电方程。我们的系统是完全机械化的，并在F。我们通过开发几个经过验证的程序和库来评估它，包括各种顺序和并发链接的数据结构，证明库和一个用于2方会话类型的库。我们的经验使我们得出结论，我们的系统能够混合自动化和交互式的证明，使其富有成效地建立程序的基础上验证了一个高度表达，国家的最先进的CSL。
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.