def canon_u

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

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend as L
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/crypto/secp256k1/semiring.bend as SR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as I
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend as B

236def canon_u(+one: Nat, +h1: {one == 1n : Nat}, +mp: Nat, +c: List<&2, Nat>, +t: List<&2, Nat>, +ht16: {FS.limbs16(one, 16n, t) == True{} : Bool}, +hv: {Nat.is_lt(LV.ev(t), C.shift(256n, one)) == True{} : Bool}, +htc: {Nat.add(1n+mp, LV.ev(c)) == C.shift(256n, one) : Nat}, +hcc: {Nat.is_lt(Nat.add(LV.ev(c), LV.ev(c)), C.shift(256n, one)) == True{} : Bool}, b: Nat, +eb: {LV.ev(L.drop(16n, L.carry(32n, L.add(t, c), 0n))) == b : Nat}, +hb: {Nat.is_lt(b, 2n) == True{} : Bool}) -> {LV.ev(L.select(b, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t)) == Nat.mod(LV.ev(t), 1n+mp) : Nat}:
237  match b:
238    case 0n:
239      +u = L.carry(32n, L.add(t, c), 0n)
240      +hu16 = B.carry_limbs(one, h1, 32n, 16n, L.add(t, c), 0n, {==})
241      +ll = I.lt_subst_r(LV.ev(L.take(16n, u)), LV.pos(16n, one), C.shift(256n, one), B.pos16(one), B.limbs_lt(one, h1, 16n, L.take(16n, u), hu16))
242      +es = Equal.trans(Nat, Nat.add(LV.ev(t), LV.ev(c)), LV.ev(u), LV.ev(L.take(16n, u)), Equal.sym(Nat, LV.ev(u), Nat.add(LV.ev(t), LV.ev(c)), u_val(c, t)),
243        Equal.trans(Nat, LV.ev(u), Nat.add(LV.ev(L.take(16n, u)), Nat.mul(LV.ev(L.drop(16n, u)), C.shift(256n, one))), LV.ev(L.take(16n, u)), split256(one, h1, u),
244          Equal.trans(Nat, Nat.add(LV.ev(L.take(16n, u)), Nat.mul(LV.ev(L.drop(16n, u)), C.shift(256n, one))), Nat.add(LV.ev(L.take(16n, u)), Nat.mul(0n, C.shift(256n, one))), LV.ev(L.take(16n, u)), Equal.cong(Nat, Nat, z => Nat.add(LV.ev(L.take(16n, u)), Nat.mul(z, C.shift(256n, one))), LV.ev(L.drop(16n, u)), 0n, eb), NA.add_zero(LV.ev(L.take(16n, u))))))
245      %Equal.sym(List<&2, Nat>, L.select(0n, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t), t, sel_zero(one, 16n, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t, hu16, ht16)) : {LV.ev(_) == Nat.mod(LV.ev(t), 1n+mp) : Nat}
246      canon0_val(mp, LV.ev(t), LV.ev(c), LV.ev(L.take(16n, u)), C.shift(256n, one), htc, ll, es)
247    case 1n:
248      +u = L.carry(32n, L.add(t, c), 0n)
249      +hu16 = B.carry_limbs(one, h1, 32n, 16n, L.add(t, c), 0n, {==})
250      +es = Equal.trans(Nat, Nat.add(LV.ev(t), LV.ev(c)), LV.ev(u), Nat.add(LV.ev(L.take(16n, u)), C.shift(256n, one)), Equal.sym(Nat, LV.ev(u), Nat.add(LV.ev(t), LV.ev(c)), u_val(c, t)),
251        Equal.trans(Nat, LV.ev(u), Nat.add(LV.ev(L.take(16n, u)), Nat.mul(LV.ev(L.drop(16n, u)), C.shift(256n, one))), Nat.add(LV.ev(L.take(16n, u)), C.shift(256n, one)), split256(one, h1, u),
252          Equal.trans(Nat, Nat.add(LV.ev(L.take(16n, u)), Nat.mul(LV.ev(L.drop(16n, u)), C.shift(256n, one))), Nat.add(LV.ev(L.take(16n, u)), Nat.mul(1n, C.shift(256n, one))), Nat.add(LV.ev(L.take(16n, u)), C.shift(256n, one)), Equal.cong(Nat, Nat, z => Nat.add(LV.ev(L.take(16n, u)), Nat.mul(z, C.shift(256n, one))), LV.ev(L.drop(16n, u)), 1n, eb), Equal.cong(Nat, Nat, z => Nat.add(LV.ev(L.take(16n, u)), z), Nat.mul(1n, C.shift(256n, one)), C.shift(256n, one), SR.one_mul(C.shift(256n, one))))))
253      %Equal.sym(List<&2, Nat>, L.select(1n, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t), L.take(16n, L.carry(32n, L.add(t, c), 0n)), sel_one(one, 16n, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t, hu16, ht16)) : {LV.ev(_) == Nat.mod(LV.ev(t), 1n+mp) : Nat}
254      canon1_val(mp, LV.ev(t), LV.ev(c), LV.ev(L.take(16n, u)), C.shift(256n, one), htc, hv, hcc, es)
255    case 2n+ +k:
256      Empty.absurd({LV.ev(L.select(2n+k, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t)) == Nat.mod(LV.ev(t), 1n+mp) : Nat}, N.lt_zero_absurd(k, hb))