Skip to content

README.md

Latest commit

 

History

History
91 lines (72 loc) · 5.58 KB

README.md

File metadata and controls

91 lines (72 loc) · 5.58 KB
Raw

Folds: sum, product, and exclusive or

Request and programs

This example computes three folds of an array of words: the wrapping sum, the wrapping product, and the bitwise exclusive or. The request asks for the three folds over an array of any length, with scalar results. The request defines each result as a left fold, so each program is its own specification and the example has no Spec.lean.

The implementations live in the word-reduction library. This example retains the fold-template proofs, compilation modules, and cases.

The programs are xs.foldl (· + ·) 0, xs.foldl (· * ·) 1, and xs.foldl (· ^^^ ·) 0. The compiler translates each to the fold template: an assignment of the initial value to an accumulator, then a loop that loads each element and applies the operation. The module definitions compile sumArray alone into sumArray.wasm, and productArray and xorArray into a 1,534-byte folds.wasm that exports both.

One fold rule for three programs

Theorem Statement
Func.foldl_implements A function whose body is the fold template with any operation other than division and remainder computes xs.foldl op.apply init.
sumArray_bytes The bytes of sumArray.module decode to a module whose export implements sumArray.
folds_bytes The bytes of folds.module decode to a module whose functions 2 and 3 implement productArray and xorArray.

Func.foldl_implements is in the fold rule, and each program's theorem applies it with its operation and initial value. The theorems are in the proofs. They use only propext, Classical.choice, and Quot.sound.

Building, running, and testing

tools/leanrun --timeout 60m lake build Examples.SumArray.Verify
mkdir -p build/folds
tools/leanrun --timeout 10m lake env lean --run tools/Emit.lean \
  Examples.SumArray.Module Examples.SumArray.folds.module build/folds/folds.wasm
build/tools/leanexe-wasmtime-host call build/folds/folds.wasm productArray i64 array-u64:2,3,7

The commands build the proofs, write the module, and call it in the Wasmtime host, with the setup of the repository README. The call prints 42, the product of 2, 3, and 7. The module tests of Cases.lean run 35 arrays in Wasmtime against native Lean for each export, including the empty array and words near 2^64.

The verified compiler's modules

The verified compilation divides the folds as the LeanExe modules do: verified_compile compiledSum := [sumArray] writes the 1,503-byte sumArray.wasm, and verified_compile compiledFolds := [productArray, xorArray] the 1,666-byte folds.wasm, both of the module registry. The folds read their borrowed array and allocate nothing, so each generated implements theorem states that its function returns the fold without a trap, and the generated native theorem states the same of its C function. The library's module compiles the same definitions in one module, libwordreductions.

Theorem Statement
compiledSum.sumArray.implements Function 2 of compiledSum.module, called with a borrowed array from any store with the allocator invariant and a memory cap of at most 65,535 pages, returns sumArray xs without a trap.
compiledFolds.productArray.implements, compiledFolds.xorArray.implements Functions 2 and 3 of compiledFolds.module return productArray xs and xorArray xs in the same way.
compiledSum.bytes, compiledFolds.bytes encode succeeds on each module, its bytes decode to the module, and the module implements its functions.
sumArray_file, sumArray_file_decode, folds_file, folds_file_decode build/verified/sumArray.wasm and build/verified/folds.wasm hold the modules' encodings and decode to the modules, as the file module of sumArray and that of folds state. 
tools/leanrun --timeout 60m lake build Examples.SumArray.Compiled
mkdir -p build/verified
tools/leanrun --timeout 10m lake env lean --run tools/Emit.lean \
  Examples.SumArray.Compiled Examples.SumArray.compiledFolds.module build/verified/folds.wasm
build/tools/leanexe-wasmtime-host call build/verified/folds.wasm productArray i64 array-u64:2,3,7
tests/verified/run.sh --cases sumArray
tests/verified/run.sh --cases folds
tests/native/verified.sh --module folds

The call prints 42, as the LeanExe module's call does. The verified driver runs the arrays of Cases.lean in Wasmtime against native Lean for each export, and the native driver runs them on the modules' translations to C, compiled with CompCert. The cases state one block that stays allocated, the input array.

Related examples

SumSquares and Mean fold over arrays of floats. PairSum folds over a temporary array, and Lists folds over a list. The LTG entry array-fold-loop describes the rule.

References