Overcoming Restraint: Composing Verification of Foreign Functions with Cogent

TL;DR

This paper presents a method for verifying foreign functions in Cogent, a restricted functional language, ensuring correctness when integrating with C code, and demonstrates its application to file systems and algorithms.

Contribution

It introduces a verification approach for Cogent's foreign function interface with C, enabling compositional correctness proofs for mixed-language systems.

Findings

Verified correctness of foreign functions in Cogent

Applied verification to binary search and file system examples

Demonstrated compositional proofs for Cogent-C systems

Abstract

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.