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.
翻译: Cogent 是一种有限的功能语言, 旨在降低开发经核实的系统代码的成本。 由于它有时会受到一些非常严格的限制, 例如缺乏对循环支持及其严格的独有类型系统的支持, Cogent 提供了外功能界面( FFI) 向 C 代码 提供的逃生舱。 当核查 Cogent 程序时, 这造成了一个问题, 因为进口的 C 组件并不享有与 Cogent 相同的静态保障水平。 在 Cogent 中执行的文件系统的先前核查仅仅假设它们的 C 组件是正确的, 它们保存着 Cogent 类型系统的变异性。 在本文中, 我们证明这些义务。 我们展示它们如何顺利地与现有的 Cogent 理论兼容, 并导致整个 Cogent- C 代码系统的正确性理论。 Cogent FFI 制约确保即使在调用 C 代码时, Cogent 类型系统的关键变量也得到维持。 我们核查高排序和多变式功能, 包括通用循环调试调器和编程器, 并演示其应用几个例子, 包括二进式搜索和BilbyF 文件系统。 我们展示了多种核查系统的可行性。