Overcoming Restraint: Modular Refinement using Cogent's Principled Foreign Function Interface
share
Cogent is a restricted functional language designed to reduce the cost of developing verified systems code. However, Cogent does not support recursion nor iteration, and its type system imposes restrictions that are sometimes too strong for low-level system programming. To overcome these restrictions, Cogent provides a foreign function interface (FFI) between Cogent and C which allows for implementing those parts of the system which cannot be expressed in Cogent, such as data structures and iterators over these data structures, to be implemented in C and called from Cogent. The Cogent framework automatically guarantees correctness of the overall Cogent-C system when provided proofs that the C components are functionally correct and satisfy Cogent's FFI constraints. We previously implemented file systems in Cogent and verified key file system operations. However, the C components and the FFI constraints that define the Cogent-C interoperability were axiomatized. In this paper, we verify the correctness and FFI constraints of the C implementation of word arrays used in the file systems. We demonstrate how these proofs modularly compose with existing Cogent theorems and result in a functional correctness theorem of the overall Cogent-C system. This demonstrates that Cogent 's FFI constraints ensure correct and safe inter-language interoperability.
READ FULL TEXT