The program declares Words, a list of words with the constructors nil and
cons, and three functions on it. Words.first returns the first word or 0, Words.sumAcc adds
the words to an accumulator by tail recursion, and Words.range n builds the words below n with a
loop. The module definition compiles the three into the 1,648-byte words.wasm.
A user recursive type with one constructor without fields and one with fields gets the record layout
of List UInt64: nil is the null pointer, and cons x w is a record of two slots. The program
states that layout through the Encode and EncodeSlotted instances in
Encode.lean, which the theorems use. sumAcc is tail recursion over records: the
compiler turns it into a loop that reads the record's slots and follows the pointer, and
sumAcc_step proves one iteration. The derivation runs verified_recursive_type
for Words in a module apart from the encoding, so that the verified compiler's programs over the
type share one set of conversions and lemmas.
| Theorem | Statement |
|---|---|
first_implements |
Function 2 of words.module implements Words.first. |
sumAcc_step |
One iteration of the compiled loop of sumAcc: on nil it stores the accumulator, and on cons x r it moves to (acc + x, r), which has the same sum and a smaller list. |
sumAcc_implements |
Function 3 implements Words.sumAcc. |
range_implements |
Function 4 implements Words.range: a call returns a chain of records, owned by the caller, or stops at unreachable. |
words_bytes |
encode succeeds on the module, and the module that decode reads from the bytes implements all three functions. |
The proofs are in Verify.lean, and they use only the axioms propext,
Classical.choice, and Quot.sound. The LeanExe compiler
manual gives the rules for recursive types.
Its section on representations describes Encode
and EncodeSlotted.
tools/leanrun --timeout 60m lake build Examples.Words.Verify
mkdir -p build/words
tools/leanrun --timeout 10m lake env lean --run tools/Emit.lean \
Examples.Words.Module Examples.Words.words.module build/words/words.wasm
build/tools/leanexe-wasmtime-host call build/words/words.wasm range chain-u64 i64:4
build/tools/leanexe-wasmtime-host call build/words/words.wasm sumAcc i64 i64:10 chain-u64:1,2,3The commands build the proofs, write the module, and call it in the Wasmtime host, with the setup of
the repository README. The first call prints [0, 1, 2, 3], and the
second prints 16, the accumulator 10 plus 1, 2, and 3.
tests/modules/run.sh compares 26 cases of Cases.lean
with native Lean.
Lists has the same layout for Lean's List UInt64, with a fold instead of
tail recursion. Trees has a recursive type with two children and non-tail
recursion. Gcd has tail recursion on words. The LTG entries
tail-recursion-records,
node-match, and
list-cell describe the rules.