A version of the compiler that starts from wordLang (without GC)

[myreen]

We want to compile HOL functions that essentially only operate over a memory modelling function and word types to wordLang (phase 1) and from there compile it to concrete machine code (phase 2).

Phase 1 would be proof-producing, while phase 2 would be a verified compiler. Importantly, one gets a certificate theorem at the end relating the HOL functions with the execution of the generated machine code.

In the long-term, there could be a systems programming dialect of CakeML.

[myreen]

It might be better to target stackLang after a few shallow-to-shallow transformations within phase 1. The advantage is that then one can influence the stack size immediately (e.g. use one stack frame for the entire program) and one can use While loops. This means that one can extract the last bits of performance from code. In contrast, a path through wordLang would force the code to use one stack frame per function and all loops would have to conform to the calling convention.

Example: User writes HOL function:

|- foo (x1:word32,x2,mem) =
     let x1 = x2 + mem x1 in
     let mem = (x2 =+ x1) mem in
       mem

Instruction selection (easy to prove, just expand let expressions):

|- foo (x1,x2,mem) =
     let t1 = mem x1 in
     let x1 = x2 + t1 in
     let mem = (x2 =+ x1) mem in
       mem

Register allocation (easy to prove, just expand let expressions):

|- foo (r0,r1,mem) =
     let r2 = mem r0 in
     let r0 = r1 + r2 in
     let mem = (r1 =+ r0) mem in
       mem

Produce stackLang program (more interesting but purely mechanical):

prog :=
  Seq (Inst MemOp Load ...)
      (Seq (Inst ...)
           (Inst ...))

where the transformation automatically proves:

|- ?k s'.
     evaluate (prog,s with clock := k) = (NONE,s') /\
     s'.mem = foo (s.regs 0, s.regs 2, s.mem)

[sorear]

Is this issue still relevant now that pancake exists?