Reduce.canon_u: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reduce.bend as Reduce Lines 236-256 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reduce.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reduce.bend&start_line=236&end_line=256 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 def 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}: match b: case 0n: +u = L.carry(32n, L.add(t, c), 0n) +hu16 = B.carry_limbs(one, h1, 32n, 16n, L.add(t, c), 0n, {==}) +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)) +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)), 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), 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)))))) %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} canon0_val(mp, LV.ev(t), LV.ev(c), LV.ev(L.take(16n, u)), C.shift(256n, one), htc, ll, es) case 1n: +u = L.carry(32n, L.add(t, c), 0n) +hu16 = B.carry_limbs(one, h1, 32n, 16n, L.add(t, c), 0n, {==}) +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)), 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), 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)))))) %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} canon1_val(mp, LV.ev(t), LV.ev(c), LV.ev(L.take(16n, u)), C.shift(256n, one), htc, hv, hcc, es) case 2n+ +k: 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)) Uses (33): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend&name=carry_limbs https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend&name=limbs_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend&name=pos16 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend&name=lt_subst_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend&name=ev https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend&name=pos https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reduce.bend&name=canon0_val https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reduce.bend&name=canon1_val https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reduce.bend&name=sel_one https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reduce.bend&name=sel_zero https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reduce.bend&name=split256 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reduce.bend&name=u_val https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend&name=one_mul https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_zero https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_zero_absurd https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=limbs16 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=carry https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=drop https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=select https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=take