cakeml
cakeml copied to clipboard
CakeML
CakeML: A Verified Implementation of ML
Currently stackLang programs write a number onto the stack at each function call. The number is an index into the bitmaps (used by the GC if it is called). An...
MLIR has a very interesting [variant of SSA](https://mlir.llvm.org/docs/Rationale/Rationale/#block-arguments-vs-phi-nodes) which seems naturally suited to functional big-step semantics. There are several high reward optimizations that are much easier to do on a...
Most of our targets have instructions that do things more complicated than a single mips or riscv op. If we're accessing a heap object (with the base pointer), say, on...
Several targets have a jump encoding breakpoint that can plausibly reach a large number of functions, but not the entire binary. (mips conditionals 32K, riscv unconditional & arm8 conditional 1M,...
We spend a lot of instructions and bytes saving registers to the stack before calls and reloading them after. We could do less of this (exact amount is difficult to...
It would be nice to make the compiler API as consistent as possible between targets and to eliminate a failure case in the space safety theorem. I expect that this...
x64, riscv, and arm7 have a set of 8 registers which can be used by shorter forms of instructions, and should be preferred for variables that are frequently accessed. To...
CakeML currently uses a link register calling convention on all targets, but even on targets where that is native it does not use the "jump and link" instruction. This could...
CakeML's intermediate representation semantics are parameterized by the size of pointers. This is a good thing, as it avoids an irrelevant multiplication of states, and the proof system can handle...
On riscv, this might be as simple as changing Encode to EncodeRVC in compiler/encoders/riscv/riscv_targetScript.sml and fixing the type error. This should be optional since riscv implementations are allowed to omit...