§ Notes on Liam O Connor's thesis: Cogent

• AutoCoress: cool tool
• sel4: translate C to HOL using AutoCoress
• cake: verify subset of ML
• Cogent has no recursion, provide higher order iterators/recursion schemes to do stuff.
• We do this by using the ! operator. Converts linear, writeable type into read-only type. Function that takes value of type Buffer! is free to read, but not write to Buffer.
• Constraint based type inference: (1) generate constraints, (2) solve.
• refinement relation R between values in the value semantics and states in the update semantics, and show that any update semantics evaluation has a corresponding value semantics evaluation that preserves this relation. When each semantics is viewed as a binary relation from initial states to final states (outputs), this requirement can be succinctly expressed as a commutative diagram...
• "Translation is the art of failure. Umberto Eco" --- nice.
• For the most part, this is because these refinement stages involve shallow embeddings, which do not allow the kind of term inspection needed to directly model a compiler phase and prove it.
• Strange, refinement relation goes upwards ? Not downwards?
• State = (Set (a, state), bool) seems weird to me. I would have expected State = Set (a, state, bool). But I guess if some contol flow path leads to UB, you can blow everything out.
• Translation validation: for each output, produce proof of correctness. Different from proving a compiler correct. More like a proof certificate.
• The reasoning behind the decision to relate representations instead of Cogent types to C types is quite subtle: Unlike in C, for a Cogent value to be well-typed, all accessible pointers in the value must be valid (i.e. defined in the store μ) and the values those pointers reference must also, in turn, be well-typed. For taken fields of a record, however, no typing obligations are required for those values, as they may include invalid pointers (see the update semantics erasure of the rules in Figure 4.5). In C, however, taken fields [what is a taken field? ] must still be well-typed, and values can be well-typed even if they contain invalid pointers. Therefore, it is impossible to determine from a Cogent value alone what C type it corresponds to, making the overloading used for these relations ambiguous
• Cogent is a total language and does not permit recursion, so we have, in principle, a well-ordering on function calls in any program. Therefore, our tactic proceeds by starting at the leaves of the call graph, proving corres theorems bottom-up until refinement is proven for the entire program. [amazing ]
• With this state definition, it is not well-defined to take a pointer to a stack-allocated variable, nor to reinterpret stack memory as a different type. C code that performs such operations is rejected by the parser.
• At the moment, such processes are implemented in Cogent with a C shell, which awaits events in a loop and executes a Cogent function whenever an event occurs. These are clearly better speci ed as productive corecursive programs. Extending Cogent to support corecursion will likely be ultimately needed in order to support moving these particular C loops into Cogent. Fortunately, Isabelle also supports corecursive shallow embeddings, providing us with a direct translation target.
• Future work: Property based testing, Concurrency, Recursion+Non-termination+Coinduction, Richer type system (refinement types), Data layout /Data description