Increment

Increment: each element plus one

Request, specification, and program

The request asks for each element of an array of at most eight words plus one, with wrapping arithmetic, and for the empty array when the input is longer. The specification states that behavior in ordinary Lean, with Array.map. The program sets the count to the input's size when it is at most eight and to 0 otherwise, and builds that many words, each the input's word plus one. One build serves both cases, because the dialect places builds at the top of a function rather than in a branch. The module definition compiles it into a 1,524-byte increment.wasm that exports compute.

The bytes compute the increment, with total execution

Theorem	Statement
compute_eq	The program equals the specification on every array of fewer than 2^64 words.
increment_bytes	The module's bytes decode to a module whose compute export implements expected: from any store that satisfies the runtime invariant, a call with an array in memory returns the words of expected or stops at unreachable.
increment_total	From an allocator whose top leaves 120 bytes within the first 16 pages, with 16 pages and a cap that allows them, the call returns the words of expected without stopping at unreachable and leaves memory at 16 pages.

The theorems are in the proofs, and they use only propext, Classical.choice, and Quot.sound. The proof of Implements applies the rule of the build template. With compute_eq, Implements.congr states it for the specification.

Building, running, and testing

tools/leanrun --timeout 60m lake build Examples.Increment.Verify
mkdir -p build/increment
tools/leanrun --timeout 10m lake env lean --run tools/Emit.lean \
  Examples.Increment.Module Examples.Increment.increment.module build/increment/increment.wasm
build/tools/leanexe-wasmtime-host call build/increment/increment.wasm compute array-u64 \
  array-u64:0,41,18446744073709551615

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 [1, 42, 0]: the last word wraps. The module tests of Cases.lean run the request's samples and edge cases in Wasmtime against expected.

Related examples

RemoveZero also builds its result with LeanExe.build. Euler and Drone have complete-execution theorems with memory bounds of the same form as increment_total. The LTG entry array-build describes the build template.

References

• The LeanExe compiler manual's section on total execution and memory bounds, which describes ImplementsA and the budget.
• The Lean 4 reference on arrays, for Array.map.