def u_hi

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

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/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/limbs.bend as LV
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as I

226# the carried sum t + c is below 2 2^256, so its part above 2^256 is 0 or 1
227def u_hi(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +t: List<&2, Nat>, +hv: {Nat.is_lt(LV.ev(t), C.shift(256n, one)) == True{} : Bool}, +hcc: {Nat.is_lt(Nat.add(LV.ev(c), LV.ev(c)), C.shift(256n, one)) == True{} : Bool}) -> {Nat.is_lt(LV.ev(L.drop(16n, L.carry(32n, L.add(t, c), 0n))), 2n) == True{} : Bool}:
228  +tt = C.shift(256n, one)
229  +u = L.carry(32n, L.add(t, c), 0n)
230  +hc = N.le_lt_trans(LV.ev(c), Nat.add(LV.ev(c), LV.ev(c)), tt, N.le_add_right(LV.ev(c), LV.ev(c)), hcc)
231  +s1 = I.lt_le_add(LV.ev(t), LV.ev(c), tt, tt, hv, N.lt_le(LV.ev(c), tt, hc))
232  +s2 = I.lt_subst_l(Nat.add(LV.ev(t), LV.ev(c)), LV.ev(u), Nat.add(tt, tt), Equal.sym(Nat, LV.ev(u), Nat.add(LV.ev(t), LV.ev(c)), u_val(c, t)), s1)
233  +s3 = I.lt_subst_r(LV.ev(u), Nat.add(tt, tt), Nat.mul(2n, tt), Equal.trans(Nat, Nat.add(tt, tt), Nat.add(tt, Nat.add(tt, 0n)), Nat.mul(2n, tt), Equal.cong(Nat, Nat, z => Nat.add(tt, z), tt, Nat.add(tt, 0n), Equal.sym(Nat, Nat.add(tt, 0n), tt, NA.add_zero(tt))), {==}), s2)
234  hi_lt(one, h1, u, 2n, s3)