7.7. Worked example🔗

The block below runs the pure (non-@[extern]) operations: the Nat extended GCD, the trial-division test, and the Nat-level Barrett reducer. The wide-word operations are @[extern]: the interpreter runs their native C symbol rather than the Lean definition, and that symbol is not linked into the manual's evaluator, so #eval and #guard cannot run them. They are documented by signature and law above.

open HexArith Hex.Nat

namespace HexArithChapter

-- gcd(12, 18) = 6, with Bezout (-1)·12 + 1·18 = 6.
#guard extGcd 12 18 = (6, -1, 1)
-- gcd(240, 46) = 2, with (-9)·240 + 47·46 = 2.
#guard extGcd 240 46 = (2, -9, 47)

-- Soundness: 97 is prime, 91 = 7·13 is not, and the
-- test rejects 1 (it demands 2 ≤ n).
#guard isPrimeTrial 97 = true
#guard isPrimeTrial 91 = false
#guard isPrimeTrial 1 = false

-- Barrett reduction modulo 97 with pinv = ⌊2^64 / 97⌋
-- reproduces ordinary remainder: 1000 mod 97 = 30.
#guard barrettReduceNat 97 (barrettRadix / 97) 1000 = 30

end HexArithChapter