def inv_step_ok

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/inverse.bend:69

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as R
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend as LC

69# one extended-Euclid step keeps the invariant
70def inv_step_ok(+mp: Nat, +a: Nat, +r0: Nat, +s0: Nat, +rp: Nat, +s1: Nat, +h0: {Nat.mod(Nat.mul(a, s0), 1n+mp) == Nat.mod(r0, 1n+mp) : Nat}, +h1: {Nat.mod(Nat.mul(a, s1), 1n+mp) == Nat.mod(1n+rp, 1n+mp) : Nat}) -> {Nat.mod(Nat.mul(a, M.inv_step(1n+mp, Nat.div(r0, 1n+rp), s0, s1)), 1n+mp) == Nat.mod(Nat.mod(r0, 1n+rp), 1n+mp) : Nat}:
71  +m = {1n+mp : Nat}
72  +r1 = {1n+rp : Nat}
73  +q = Nat.div(r0, r1)
74  +r = Nat.mod(r0, r1)
75  +t = Nat.mod(Nat.mul(q, s1), m)
76  +u = Nat.sub(m, t)
77  +x = Nat.mul(a, Nat.add(s0, u))
78  +c = Nat.mul(q, r1)
79  +e1 = R.mod_mul_r(mp, a, Nat.add(s0, u))
80  # c == a t (mod m)
81  +ec = Equal.trans(Nat, Nat.mod(c, m), Nat.mod(Nat.mul(q, Nat.mul(a, s1)), m), Nat.mod(Nat.mul(a, t), m), cong_mul_r(mp, q, r1, Nat.mul(a, s1), Equal.sym(Nat, Nat.mod(Nat.mul(a, s1), m), Nat.mod(r1, m), h1)),
82    Equal.trans(Nat, Nat.mod(Nat.mul(q, Nat.mul(a, s1)), m), Nat.mod(Nat.mul(a, Nat.mul(q, s1)), m), Nat.mod(Nat.mul(a, t), m), Equal.cong(Nat, Nat, z => Nat.mod(z, m), Nat.mul(q, Nat.mul(a, s1)), Nat.mul(a, Nat.mul(q, s1)), LC.swap_cw(q, a, s1)), Equal.sym(Nat, Nat.mod(Nat.mul(a, t), m), Nat.mod(Nat.mul(a, Nat.mul(q, s1)), m), R.mod_mul_r(mp, a, Nat.mul(q, s1)))))
83  # x + a t == a s0 + a m
84  +ex = Equal.trans(Nat, Nat.add(x, Nat.mul(a, t)), Nat.add(Nat.add(Nat.mul(a, s0), Nat.mul(a, u)), Nat.mul(a, t)), Nat.add(Nat.mul(a, m), Nat.mul(a, s0)),
85    Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(a, t)), x, Nat.add(Nat.mul(a, s0), Nat.mul(a, u)), A.mul_add_left(a, s0, u)),
86    Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(a, s0), Nat.mul(a, u)), Nat.mul(a, t)), Nat.add(Nat.mul(a, s0), Nat.add(Nat.mul(a, u), Nat.mul(a, t))), Nat.add(Nat.mul(a, m), Nat.mul(a, s0)), A.add_assoc(Nat.mul(a, s0), Nat.mul(a, u), Nat.mul(a, t)),
87      Equal.trans(Nat, Nat.add(Nat.mul(a, s0), Nat.add(Nat.mul(a, u), Nat.mul(a, t))), Nat.add(Nat.mul(a, s0), Nat.mul(a, m)), Nat.add(Nat.mul(a, m), Nat.mul(a, s0)),
88        Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(a, s0), z), Nat.add(Nat.mul(a, u), Nat.mul(a, t)), Nat.mul(a, m), Equal.trans(Nat, Nat.add(Nat.mul(a, u), Nat.mul(a, t)), Nat.mul(a, Nat.add(u, t)), Nat.mul(a, m), Equal.sym(Nat, Nat.mul(a, Nat.add(u, t)), Nat.add(Nat.mul(a, u), Nat.mul(a, t)), A.mul_add_left(a, u, t)), Equal.cong(Nat, Nat, z => Nat.mul(a, z), Nat.add(u, t), m, sub_plus(m, t, R.dm_lt(mp, Nat.mul(q, s1)))))),
89        A.add_comm(Nat.mul(a, s0), Nat.mul(a, m)))))
90  # x + c == r + c (mod m), both == r0
91  +exc = Equal.trans(Nat, Nat.mod(Nat.add(x, c), m), Nat.mod(Nat.add(x, Nat.mul(a, t)), m), Nat.mod(r0, m), cong_add_r(mp, x, c, Nat.mul(a, t), ec),
92    Equal.trans(Nat, Nat.mod(Nat.add(x, Nat.mul(a, t)), m), Nat.mod(Nat.add(Nat.mul(a, m), Nat.mul(a, s0)), m), Nat.mod(r0, m), Equal.cong(Nat, Nat, z => Nat.mod(z, m), Nat.add(x, Nat.mul(a, t)), Nat.add(Nat.mul(a, m), Nat.mul(a, s0)), ex),
93      Equal.trans(Nat, Nat.mod(Nat.add(Nat.mul(a, m), Nat.mul(a, s0)), m), Nat.mod(Nat.mul(a, s0), m), Nat.mod(r0, m), R.absorb(mp, a, Nat.mul(a, s0)), h0)))
94  +erc = Equal.cong(Nat, Nat, z => Nat.mod(z, m), Nat.add(r, c), r0, Equal.trans(Nat, Nat.add(r, c), Nat.add(c, r), r0, A.add_comm(r, c), Equal.sym(Nat, r0, Nat.add(c, r), R.dm_eq(rp, r0))))
95  Equal.trans(Nat, Nat.mod(Nat.mul(a, M.inv_step(m, q, s0, s1)), m), Nat.mod(x, m), Nat.mod(r, m), e1, add_cancel_mod(mp, x, r, c, Equal.trans(Nat, Nat.mod(Nat.add(x, c), m), Nat.mod(r0, m), Nat.mod(Nat.add(r, c), m), exc, Equal.sym(Nat, Nat.mod(Nat.add(r, c), m), Nat.mod(r0, m), erc))))