The Pancake Project
Pancake is a new 'thin' language constructed with the aims of (1) ease of source-level verification, (2) user-controlled small memory footprint, and (3) simple transportation of correctness results from source to executable binary code. The Pancake compiler builds on the lower parts of the CakeML compiler.
Motivation
Several people have expressed interest in an imperative space-constrained language (no GC, no dynamic memory allocation) built on the CakeML compiler. We have claimed that infrastructure in the CakeML compiler can be used to implement other compilers. Pancake is our answer.
The Pancake Language
Name. Originally, the name Pancake stood for "Pascal-like language based on the lower half of CakeML compiler". However, the Pascal part should not be taken too seriously. Instead, the language can be seen as mix between a portable assembly language with structured control-flow and an untyped C-like language, but, unlike either of those, Pancake has a straightforward and verification friendly (low-level) semantics.
Why is Pancake untyped? Type systems for languages like C are a way to establish some basic safety properties. Pancake is untyped because programmers might not like to be tied down to a type system. The basic safety properties provided by a type system seem pointless in the context of Pancake programs that are intended for proofs of functional correctness. The functional correctness properties that one proves for Pancake programs imply the basic safety properties that type systems can provide.
Values. Pancake programs consist of a collection of (possibly mutually recursive) functions. These functions take multiple arguments and return multiple values. Local variables hold source values that consist of machine words or tuples/structs of source values, i.e. nested tuples/structs are supported. Structs/tuples held in local variables are stored in registers and/or the stack.
Memory. The language is built to be very explicit about memory usage. Heap memory usage is completely controlled by the programmer. Stack usage is something the compiler determines and is explicit about. If the user refrains from non-tail-recursive recursion, then the compiler will output the number of machine words of stack space that the program can at most use. This number is a proved-correct upper bound on stack usage.
Tools for Pancake
Two tools are currently under development for Pancake:
- The verified Pancake compiler: This compiler converts Pancake source programs into executable machine code that can be linked and run either bare-metal or together with external trusted C programs. The Pancake compiler will have a correctness theorem that allows easy transfer of proved properties of the source code to transfer to proved properties of the generated machine code.
- A proof-producing shallow-embedding extractor: A shallow-embedding extractor or decompiler will be the main tool support for proofs of functional correctness properties of source Pancake programs. Users will write Pancake programs in a C inspired syntax and then run this extractor/decompiler on the Pancake code in order to get similar looking HOL functions that are guaranteed to have the same behaviour as the original Pancake code. Any properties proved of the convenient shallow HOL functions are also true for the original Pancake source program. This tool is very similar to this proof-producing decompiler that has been used to decompile the machine code of the seL4 microkernel.
State of development: the compiler is almost complete; the extractor is still work-in-progress.
Contact
Get in touch with Magnus Myreen with questions. Alternatively, join our Discord (with this link) and ask questions about Pancake.