A Case for Lightweight Interfaces in Coq
summary
Bedrock uses Coq and the Iris program logic to verify a large concurrent C++ hypervisor stack and finds Coq’s lack of lightweight interface files hurts scale: predicate configuration and opaque sealing are necessary for automation, with ad hoc hints producing up to 25× speedups and type-class search succeeding under 1% of attempts. The proposal adds .vi interface files that hide implementations, enable parallel compilation and contain proof-side effects; module-wrapping is a conservative fallback but multiple implementations remain tricky.
AI-written summary · about
chapters (6)
- 0:00Intro
- 0:16Motivation Bed Rock Systems
- 4:50Anatomy of a Verification (Hierarchy Builder)
- 9:16Proposal: Separate Compilation
- 10:39Different Approaches
- 12:12Feedback?
related talks
01h 04mCoq's vibrant ecosystem for verification engineering
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
01h 02mMelocoton: A Program Logic for Verified Interoperability Between OCaml and C (I...
23mSpecifying and Verifying Future Conditions
36mSpecification-Guided Component-Based Synthesis from Effectful Libraries
18mMelocoton: A Program Logic for Verified Interoperability Between OCaml and C
21mMechanised Hypersafety Proofs about Structured Data
19mProof Automation for Linearizability in Separation Logic