README.md

Gcd: Euclid's algorithm

Request, specification, and program

The request asks for the greatest common divisor of any two words, by Euclid's remainder loop, with gcd a 0 = a. The specification states it with Lean's Nat.gcd. The program is tail recursive: gcd a b is a when b = 0 and gcd b (a % b) otherwise, and it terminates because a % b < b. The compiler translates the tail recursion into a loop, so a call makes no further calls. The module definition compiles it into a 1,445-byte gcd.wasm that exports gcd.

The bytes compute Nat.gcd

Theorem	Statement
gcd_eq	The program equals the specification on every pair of words.
gcd_implements	Function 2 computes gcd on its two arguments.
gcd_bytes	The module's bytes decode to a module whose gcd export implements expected: from any store that satisfies the runtime invariant, a call returns expected (a, b) or stops at unreachable.

The theorems are in the proofs, and they use only propext, Classical.choice, and Quot.sound. gcd_implements follows from gcd_step, one theorem about a run of the loop body, by the rule of the tail-recursion template. gcd_eq follows from Nat.gcd_rec by induction on the second argument.

Building, running, and testing

tools/leanrun --timeout 60m lake build Library.Numerics.Arithmetic.Gcd.Verify
mkdir -p build/gcd
tools/leanrun --timeout 10m lake env lean --run tools/Emit.lean \
  Library.Numerics.Arithmetic.Gcd.Module Library.Numerics.Arithmetic.Gcd.gcd.module build/gcd/gcd.wasm
build/tools/leanexe-wasmtime-host call build/gcd/gcd.wasm gcd i64 i64:60 i64:42

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 6. The module tests of Cases.lean compare 49 pairs in Wasmtime against expected, including (0, 0), (1, 2^64 − 1), and consecutive Fibonacci numbers.

Related examples

PrimeFactors is tail recursion with a measure of two values instead of one. Words has tail recursion over records, and Scale shows how the IR tests a divisor. The LTG entry tail-recursion-loop describes the rule.

References

• D. E. Knuth, The Art of Computer Programming, Vol. 2, Seminumerical Algorithms, 3rd ed., Addison-Wesley, 1997, section 4.5.2, on Euclid's algorithm.
• Lean core's Nat.gcd, which the specification uses, and Mathlib's lemmas about it, which the proof of gcd_eq uses.