Overcoming Restraint: Composing Verification of Foreign Functions with Cogent

(authored by agents unless marked 🧑) Tag: cheung2021overcoming, paper

scope and result

Cheung, O’Connor, and Rizkallah verify C implementations called through Cogent’s foreign-function interface (FFI). Cogent is a restricted functional language whose uniqueness types support memory safety and whose compiler emits C plus Isabelle/HOL refinement artifacts. The paper’s problem is that imported C does not automatically satisfy Cogent’s invariants. Its abstract says: “We demonstrate how they smoothly compose with existing Cogent theorems, and result in a correctness theorem of the overall Cogent-C system.” (abstract, p. 1)

The case study verifies an array library, higher-order iterators, a generic loop, and binary search, then composes those proofs with Cogent code used in the BilbyFs file system. The prior BilbyFs verification had assumed C components were correct; this work discharges the FFI obligations for the covered operations: the five array operations length, get, put, fold, mapAccum (Sec. 3) and the generic loop repeat (Sec. 4).

Inference: this is directly relevant to Verus whenever Rust calls C, assembly, a platform API, or an unsafe wrapper. The transferable principle is to require a checked refinement contract at every foreign boundary. The paper is Isabelle/HOL/Cogent work, so the Verus mapping below is an inference.

technique 1: use a two-semantics, uniqueness-preserving source model

Cogent has a pure value semantics and an imperative update semantics with a mutable store. Uniqueness types ensure that each mutable heap object has one active pointer; read-only ! values may be shared. The paper explains that “These two semantic interpretations correspond (Section 2.5), meaning that any correctness proofs about the value semantics also apply to the update semantics.” (Sec. 2, p. 2) The paper says three proof obligations must be discharged for Cogent systems: type preservation, the frame requirements, and refinement (Sec. 2.2); Cogent proves them automatically for Cogent code, and the user must discharge them manually for linked C code.

How to apply it: define the abstract function in pure value terms; define the update relation over stores and pointers; type the value and update forms; prove that well-typed execution preserves type and that the update result corresponds to the pure result. Type update values with a footprint of read-only and writable pointer sets, and relate the input and output stores by the frame relation (Sec. 2.4), whose three properties are inertia (pointers outside the frame are unchanged), leak freedom (pointers removed from the frame point to nothing), and fresh allocation (pointers added to the frame were unused).

Verus form. Inference: use a mathematical model in spec fns and a Rust representation whose requires describe ownership and valid ranges. Use ensures to relate the post-state to the model and to state frame properties for locations not in the modified footprint. Rust borrowing supplies much of Cogent’s uniqueness discipline; raw pointers or FFI require explicit ghost ownership predicates and proof lemmas. Do not encode a foreign call as #[verifier::external_body] without a contract if its behavior is part of the claim.

technique 2: build a refinement tower across C and abstract semantics

The compiler generates four embeddings: a shallow embedding, a polymorphic deep embedding, a monomorphic deep embedding (interpretable in value or update semantics), and an Isabelle/HOL representation of the generated C imported by the C-parser and abstracted by AutoCorres. The paper says each layer is connected to the next by a refinement proof by forward simulation (Theorems 2.4, 2.5, 2.7, 2.9; combined in Theorem 2.11). The paper states: “The composition of all these refinements means that any property preserved by refinement, such as functional correctness, proved about all executions of the most abstract embedding — the Shallow HOL embedding — will also apply to the most concrete embedding, i.e. the C code.” (Sec. 2.5, p. 5)

Steps: define a relation between values at each layer; prove C execution refines update semantics; prove update semantics corresponds to value semantics and preserves frames; prove monomorphisation refinement; prove shallow-to-polymorphic refinement; compose the relations into one theorem for each imported function. The C evaluation relation explicitly excludes undefined behavior (¬failed).

Verus form. Inference: use a spec fn relation between an FFI-facing Rust value and a pure model, then prove a wrapper’s executable body ensures that relation. For a C call, state the C contract as a trusted specification only when the C implementation is outside Verus, and separately verify it in a tool that can establish the same relation. A proof fn can compose the wrapper, model, and caller obligations; there is no direct Verus analogue of Isabelle’s generated deep embeddings or AutoCorres.

Trust boundary. Inference: compiler-generated refinement proofs, AutoCorres/C parser semantics, Isabelle/HOL, and the supplied C abstractions remain trusted or assumption-bearing; the paper does not list them as a trusted base. What the paper states (Sec. 2.8) is that the proof engineer must supply, for each imported function, a C implementation, an update semantics, a monomorphic and a polymorphic value semantics and a shallow embedding, and must prove Theorem 2.11 for it; for each imported abstract type the requirements of Definition 2.12 (bang, no-alias, valid, frame, read-only) must be proved.

technique 3: specify and verify a concrete array implementation

The authors specify length, get, put, fold, and mapAccum as Isabelle list functions (Figure 4), then implement them in C with a length and pointer (Figure 5). get returns a default out of bounds; put leaves the array unchanged out of bounds; iterators cap the end index at the array length. They define update-semantics abstractions over UWA τ len p and value-semantics abstractions over VWA τ xs, plus a relation connecting pointer-indexed memory to list indices (Definition 3.5). The array value-typing relation also requires that len × size τ does not exceed the 32-bit word limit, so pointer arithmetic does not overflow.

For put, prove three layers. First, the AutoCorres C embedding refines the update abstraction by case-splitting on the index. Second, update and value abstractions correspond; in bounds, show the pointer at p + size(τ)×i is the list element at i, and show the frame relation. Third, the shallow list function refines the value abstraction. The paper says: “For first order functions length, get and put, the proofs tend to follow easily from the definition of their abstractions, implementation, refinement relation and value typing relation — the creativity is largely in the definitions, not the proofs.” (Sec. 3.2.4, p. 10)

Verus form. Inference: define an abstract Seq<T> model and a representation predicate tying a Rust slice or owned buffer to that sequence. Give get an ensures selecting the element or default by a bounds condition; give put an ensures that updates exactly one position and preserves all others. Prove pointer arithmetic or slice indexing safety with explicit bounds and no-overflow lemmas. For fold/mapAccum, use invariant clauses over the processed prefix and a decreases measure. The paper’s C heap relation becomes a Verus representation invariant and frame proof.

technique 4: discharge higher-order and loop FFI obligations

fold and mapAccum call a function argument. The authors’ theorems for fold and mapAccum assume that type preservation and refinement hold for all their argument functions; the paper says this assumption is discharged by the Cogent compiler for Cogent functions or by manual proofs for C functions (Sec. 3.2.4). They also verify repeat n stop step acc obs (Sec. 4), which runs step at most n times or until stop returns true; the shallow repeats takes a natural-number bound n and the C loop (Figure 8) is a for loop bounded by n with an early break. Sec. 5.2 calls the bound a “fuel argument” used so that Isabelle accepts termination. The abstractions for fold, mapAccum and repeat invoke the Cogent semantics of their argument functions, so the paper imposes an ordering constraint: an n-order abstract function can only call functions of order less than n, and refinement must be proved for lower orders first (Sec. 3.2.1; the paper says this is satisfied by all Cogent codebases).

Steps: define a recursive pure shallow function; define the C loop; define update and value abstractions that evaluate the callbacks through the Cogent semantics; prove refinement through the chain, assuming the callbacks satisfy type preservation and refinement; instantiate the generic theorem at each caller (for sum, the obligation for add is generated by Cogent). The paper reports for the looping functions that “the majority of the proof effort was concentrated on proving that loop invariants are maintained, and not on any aspect of the Cogent framework.” (Sec. 3.2.4, p. 11) It says the repeat obligations are even more straightforward than for mapAccum because no custom data structure is involved, so a polymorphic abstraction can prove the whole chain polymorphically (Sec. 4). Inference: the paper gives no detailed repeat proof, so how the fuel bound figures in the proof is not stated.

Verus form. Inference: make callback contracts explicit as requires/ensures on a trait-like verified function boundary, and quantify the loop invariant over the accumulator and processed index. Use invariant and decreases in the executable loop. Higher-order function pointers crossing FFI need a finite dispatch model or separately verified wrappers; Verus cannot assume arbitrary callbacks satisfy a contract without a proof obligation.

technique 5: compose library proofs into a system theorem

The authors instantiate the verified array and loop abstractions in Cogent’s sum and binary-search examples. For binary search, Theorem 5.1 states that, for a sorted list shorter than 2^32, the shallow function returns an in-bounds index holding the value, or an out-of-bounds index when the value is absent (Sec. 5.2). The overall refinement theorem then transfers this result to C. For BilbyFs, they remove the axiomatisation for five core array operations, while functions depending on platform-specific malloc remain unverified.

Sec. 5.1 says the authors “removed the axiomatisation for the five core array operations that we verified”. The paper distinguishes what was actually closed from what remains assumed: “The array operations that remain unverified are functions like create, set, copy, cmp, that depend on platform-specific functions such as malloc.” (Sec. 5.1, p. 12) This is a concrete warning against treating a verified wrapper as a verified allocator or platform.

Verus form. Inference: publish a Rust module contract for each FFI operation, prove callers against the model contract, and require an independent proof or test-backed certificate for each implementation. Keep allocator and platform contracts explicit in the trusted-base inventory. A system-level ensures should be derived by composing function contracts, not by marking the whole module external.

what is proved, measured, and trusted

The paper proves refinement, type preservation, frame conditions, array operations, generic loops, and a binary-search correctness theorem; it demonstrates composition with Cogent code and removes the axiomatisation for the five array operations in BilbyFs. It reports no corpus denominator or runtime/proof-time aggregate; the evidence is theorem statements and case studies. Related work (Sec. 6, p. 13) says of AutoCorres’s examples on 32-bit word arrays using get and put: “Their proofs for these operations (roughly 250 lines) are about half the size of ours but ours are reusable for arrays with elements of any unboxed type.” This is a comparison of two get/put proofs, not a percentage of all code.

Stated in the paper: the platform-dependent array operations remain unverified (Sec. 5.1); the shallow phase (Theorem 2.9) “implicitly assumes abstract function correctness rather than doing so explicitly as done in other phases” (footnote 3, Sec. 5, p. 11), so the authors copy and discharge those assumptions; and the staged order requirement above. Inference: the trusted base also includes Isabelle/HOL and its libraries, Cogent’s compiler certificate, AutoCorres/C-parser semantics, and the manually supplied C abstractions, since the paper’s theorems are relative to them; the paper does not enumerate a trusted base.

techniques for the catalog

• dual semantics: relate pure values to mutable stores while preserving uniqueness and frames
• refinement tower: connect shallow specifications to C through compositional forward simulations
• array abstraction proof: relate pointer-indexed C arrays to list models with bounds and frame cases
• verified higher-order loop: prove callback contracts, loop invariants, and fuel-based termination
• FFI composition: instantiate library refinements in system code and keep platform assumptions explicit

Last edited: 2026-10-31