Extended Euclidean algorithm — Bezout coefficients and modular inverse
Beyond the gcd, the extended algorithm finds integers x, y with a·x + b·y = gcd(a, b) (Bezout's identity). When gcd(a, m) = 1, x mod m is the modular inverse of a. Returns a record { g, x, y }.
A Soma program from the math part of the verified corpus: 70 lines, cells ExtEuclid, ExtEuclidTests. It passes soma check with soma 3.2.4.
How it is built
The cell ExtEuclid declares 3 signals in its face: egcd(a: Int, b: Int) -> Map, inverse(a: Int, m: Int) -> Int and run() -> Map. Handlers: egcd (line 19), inverse (line 41) and run (line 47).
The file also holds 1 test cell (ExtEuclidTests) with 5 assertions, run by soma test.
The source
ext_euclid.cell
// ============================================================================
// Extended Euclidean algorithm — Bezout coefficients and modular inverse
// ============================================================================
//
// Beyond the gcd, the extended algorithm finds integers x, y with
// a·x + b·y = gcd(a, b) (Bezout's identity). When gcd(a, m) = 1, x mod m is
// the modular inverse of a. Returns a record { g, x, y }.
//
// soma run ext_euclid.cell run
// ============================================================================
cell ExtEuclid {
face {
signal egcd(a: Int, b: Int) -> Map
signal inverse(a: Int, m: Int) -> Int
signal run() -> Map
}
on egcd(a: Int, b: Int) {
let old_r = a
let r = b
let old_s = 1
let s = 0
let old_t = 0
let t = 1
while r != 0 {
let q = idiv(old_r, r)
let nr = old_r - q * r
old_r = r
r = nr
let ns = old_s - q * s
old_s = s
s = ns
let nt = old_t - q * t
old_t = t
t = nt
}
return Bezout { g: old_r, x: old_s, y: old_t }
}
on inverse(a: Int, m: Int) {
let e = egcd(a, m)
if e.g != 1 { return 0 - 1 } // no inverse exists
return ((e.x % m) + m) % m
}
on run() {
let e = egcd(240, 46)
return map(
"gcd", e.g,
"x", e.x,
"y", e.y,
"inv_3_mod_11", inverse(3, 11)
)
}
}
cell test ExtEuclidTests {
rules {
// gcd(240, 46) = 2, with Bezout coefficients verifying the identity
assert egcd(240, 46).g == 2
assert 240 * egcd(240, 46).x + 46 * egcd(240, 46).y == 2
// inverse of 3 mod 11 is 4
assert inverse(3, 11) == 4
assert (3 * inverse(3, 11)) % 11 == 1
// no inverse when not coprime
assert inverse(4, 8) == 0 - 1
}
}What the toolchain says
$ soma check ext_euclid.cell
✓ All checks passed.$ soma test ext_euclid.cell
test ExtEuclidTests ...
✓ assert egcd(240, 46).g == 2
✓ assert 240 * egcd(240, 46).x + 46 * egcd(240, 46).y == 2
✓ assert inverse(3, 11) == 4
✓ assert (3 * inverse(3, 11)) % 11 == 1
✓ assert inverse(4, 8) == 0 - 1
5 tests: 5 passed, 0 failed$ soma verify ext_euclid.cell
Verifying ext_euclid.cell...
ExtEuclid/termination:
⚠ handler `egcd`: while-loop without provable termination bound (write `while [loop_bound(N)] cond { … }`, or a for-loop over a bounded range)
⚠ `inverse` calls `ExtEuclid.egcd`, which may not terminate
⚠ `run` calls `ExtEuclid.egcd`, which may not terminate
0 passed, 3 warnings, 0 failures
Temporal: 0 passed, 0 failed
VERIFY OK$ soma run ext_euclid.cell run
{"gcd": 2, "x": -9, "y": 47, "inv_3_mod_11": 4}