def canon1_val

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/reduce.bend:200

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend as SR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as I

200# v + cv = lo + t with t = m + cv, v < t, cv + cv < t: v mod m = lo
201def canon1_val(+mp: Nat, +v: Nat, +cv: Nat, +lo: Nat, +t: Nat, +ht: {Nat.add(1n+mp, cv) == t : Nat}, +hv: {Nat.is_lt(v, t) == True{} : Bool}, +hcc: {Nat.is_lt(Nat.add(cv, cv), t) == True{} : Bool}, +eu: {Nat.add(v, cv) == Nat.add(lo, t) : Nat}) -> {lo == Nat.mod(v, 1n+mp) : Nat}:
202  +m = {1n+mp : Nat}
203  # v = lo + m
204  +e1 = Equal.trans(Nat, Nat.add(v, cv), Nat.add(lo, t), Nat.add(Nat.add(lo, m), cv), eu, Equal.trans(Nat, Nat.add(lo, t), Nat.add(lo, Nat.add(m, cv)), Nat.add(Nat.add(lo, m), cv), Equal.cong(Nat, Nat, z => Nat.add(lo, z), t, Nat.add(m, cv), Equal.sym(Nat, Nat.add(m, cv), t, ht)), Equal.sym(Nat, Nat.add(Nat.add(lo, m), cv), Nat.add(lo, Nat.add(m, cv)), NA.add_assoc(lo, m, cv))))
205  +e2 = NR.add_cancel(cv, v, Nat.add(lo, m), Equal.trans(Nat, Nat.add(cv, v), Nat.add(v, cv), Nat.add(cv, Nat.add(lo, m)), NA.add_comm(cv, v), Equal.trans(Nat, Nat.add(v, cv), Nat.add(Nat.add(lo, m), cv), Nat.add(cv, Nat.add(lo, m)), e1, NA.add_comm(Nat.add(lo, m), cv))))
206  # lo < cv < m
207  +s1 = I.lt_subst_l(v, Nat.add(lo, m), t, e2, hv)
208  +s2 = I.lt_subst_r(Nat.add(lo, m), t, Nat.add(cv, m), Equal.trans(Nat, t, Nat.add(m, cv), Nat.add(cv, m), Equal.sym(Nat, Nat.add(m, cv), t, ht), NA.add_comm(m, cv)), s1)
209  +s3 = Equal.trans(Bool, Nat.is_lt(lo, cv), Nat.is_lt(Nat.add(lo, m), Nat.add(cv, m)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(lo, m), Nat.add(cv, m)), Nat.is_lt(lo, cv), WW.lt_cancel_r(lo, cv, m)), s2)
210  +s4 = I.lt_subst_r(Nat.add(cv, cv), t, Nat.add(m, cv), Equal.sym(Nat, Nat.add(m, cv), t, ht), hcc)
211  +s5 = Equal.trans(Bool, Nat.is_lt(cv, m), Nat.is_lt(Nat.add(cv, cv), Nat.add(m, cv)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(cv, cv), Nat.add(m, cv)), Nat.is_lt(cv, m), WW.lt_cancel_r(cv, m, cv)), s4)
212  +s6 = N.lt_trans(lo, cv, m, s3, s5)
213  # v mod m = (lo + 1 m) mod m = lo
214  %Equal.sym(Nat, v, Nat.add(lo, 1n+mp), e2) : {lo == Nat.mod(_, 1n+mp) : Nat}
215  %Equal.sym(Nat, Nat.add(lo, 1n+mp), Nat.add(1n+mp, lo), NA.add_comm(lo, 1n+mp)) : {lo == Nat.mod(_, 1n+mp) : Nat}
216  %Equal.sym(Nat, 1n+mp, Nat.mul(1n, 1n+mp), Equal.sym(Nat, Nat.mul(1n, 1n+mp), 1n+mp, SR.one_mul(1n+mp))) : {lo == Nat.mod(Nat.add(_, lo), 1n+mp) : Nat}
217  %Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(1n, 1n+mp), lo), 1n+mp), Nat.mod(lo, 1n+mp), NR.absorb(mp, 1n, lo)) : {lo == _ : Nat}
218  %Equal.sym(Nat, Nat.mod(lo, 1n+mp), lo, NR.mod_of(0n, mp, lo, s6)) : {lo == _ : Nat}
219  {==}