Overcoming Restraint: Composing Verification of Foreign Functions with Cogent
summary
Cogent’s FFI is proven to preserve uniqueness typing and memory safety while composing Cogent proofs down to C: the compiler’s multi‑phase refinement pipeline (shallow→polymorphic→monomorphic→update→C) composes with manually proved refinements for template C. Verified artifacts include array operations (length get put fold map), a reusable repeat iterator and a binary‑search implementation, all proved refinement and memory‑safe in isabelle hull and used to discharge obligations for BilbyFs, demonstrating mixed Cogent‑C verification works.
AI-written summary · about
chapters (9)
- 0:00Start
- 0:13Motivation
- 3:54Proof Requirements
- 6:31Typing Constraints
- 7:18Frame Constraints
- 8:52Binary Search
- 9:38Functional Correctness Specification of Binary Search
- 9:58Binary Search Encoding
- 11:23The Correctness Theorem
related talks
20mA Verified Foreign Function Interface Between Coq and C
01h 05mAll the Languages Together
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
21mSecurely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typ...
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
24mFormally Verified Native Code Generation in an Effectful JIT: Turning the CompCe...
01h 02mMelocoton: A Program Logic for Verified Interoperability Between OCaml and C (I...