Overcoming Restraint: Composing Verification of Foreign Functions with Cogent

Cogent is a restricted functional language designed to reduce
the cost of developing verified systems code. Because of its
sometimes-onerous restrictions, such as the lack of support
for recursion and its strict uniqueness type system, Cogent
provides an escape hatch in the form of a foreign function
interface (FFI) to C code. This poses a problem when verifying
Cogent programs, as imported C components do not
enjoy the same level of static guarantees that Cogent does.
Previous verification of file systems implemented in Cogent
merely assumed that their C components were correct and
that they preserved the invariants of Cogent’s type system.
In this paper, we instead prove such obligations. We demonstrate
how they smoothly compose with existing Cogent
theorems, and result in a correctness theorem of the overall
Cogent-C system. The Cogent FFI constraints ensure that
key invariants of Cogent’s type system are maintained even
when calling C code. We verify reusable higher-order and
polymorphic functions including a generic loop combinator
and array iterators and demonstrate their application to
several examples including binary search and the BilbyFs
file system. We demonstrate the feasibility of verification of
mixed Cogent-C systems, and provide some insight into verification
of software comprised of code in multiple languages
with differing levels of static guarantees.