def shr_small

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64sh.bend:144

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/math/w64.bend as SW
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU
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/logic.bend as L
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/typed/w64add.bend as WA
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/math/typed/shrn.bend as SR

144# 1 <= t < 32, s == 32 - t
145def shr_small(+l: U32, +h: U32, +j: Nat, +hk: {Nat.is_lt(1n+j, 32n) == True{} : Bool}) -> {SW.value(X.shr_lt(WU.U64{l, h}, 1n+j)) == C.high(1n+j, val(l, h)) : Nat}:
146  +t = {1n+j : Nat}
147  +s = Nat.sub(32n, t)
148  +hts = N.sub_add(32n, t, N.lt_le(t, 32n, hk))
149  +hst = Equal.trans(Nat, Nat.add(s, t), Nat.add(t, s), 32n, N.add_comm(s, t), hts)
150  +hs = L.subst(Nat, z => {Nat.is_lt(s, z) == True{} : Bool}, Nat.add(t, s), 32n, hts, N.le_lt_trans(s, Nat.add(j, s), 1n+Nat.add(j, s), L.subst(Nat, z => {Nat.is_le(s, z) == True{} : Bool}, Nat.add(s, j), Nat.add(j, s), N.add_comm(s, j), N.le_add_right(s, j)), N.lt_succ(Nat.add(j, s))))
151  +hl = C.high(t, v(l))
152  +lh = C.low(t, v(h))
153  +hh = C.high(t, v(h))
154  +a1 = SR.shrn_high(l, t)
155  +a2 = Equal.trans(Nat, v(U32.mul(h, X.pow2(s))), C.low(32n, C.shift(s, v(h))), C.shift(s, lh), mul_p2(h, s, hs), Equal.trans(Nat, C.low(32n, C.shift(s, v(h))), C.low(Nat.add(s, t), C.shift(s, v(h))), C.shift(s, lh), Equal.cong(Nat, Nat, z => C.low(z, C.shift(s, v(h))), 32n, Nat.add(s, t), Equal.sym(Nat, Nat.add(s, t), 32n, hst)), WW.low_shift(s, t, v(h))))
156  +a3 = SR.shrn_high(h, t)
157  +hr = WW.lt_of_fits(s, hl, fits_high(t, s, v(l), fits32(t, s, hts, l)))
158  +hsum = WW.two_limb_lt(s, t, hl, lh, hr, WW.low_lt(t, v(h)))
159  +es = Equal.trans(Nat, Nat.add(v(U32.shrn(l, t)), v(U32.mul(h, X.pow2(s)))), Nat.add(hl, v(U32.mul(h, X.pow2(s)))), Nat.add(hl, C.shift(s, lh)), Equal.cong(Nat, Nat, z => Nat.add(z, v(U32.mul(h, X.pow2(s)))), v(U32.shrn(l, t)), hl, a1), Equal.cong(Nat, Nat, z => Nat.add(hl, z), v(U32.mul(h, X.pow2(s))), C.shift(s, lh), a2))
160  +hf = L.subst(Nat, z => {C.fits(z, Nat.add(v(U32.shrn(l, t)), v(U32.mul(h, X.pow2(s))))) == True{} : Bool}, Nat.add(s, t), 32n, hst, WW.fits_of_lt(Nat.add(s, t), Nat.add(v(U32.shrn(l, t)), v(U32.mul(h, X.pow2(s)))), L.subst(Nat, z => {Nat.is_lt(z, C.pow2(Nat.add(s, t))) == True{} : Bool}, Nat.add(hl, C.shift(s, lh)), Nat.add(v(U32.shrn(l, t)), v(U32.mul(h, X.pow2(s)))), Equal.sym(Nat, Nat.add(v(U32.shrn(l, t)), v(U32.mul(h, X.pow2(s)))), Nat.add(hl, C.shift(s, lh)), es), hsum)))
161  +elo = Equal.trans(Nat, v(U32.add(U32.shrn(l, t), U32.mul(h, X.pow2(s)))), Nat.add(v(U32.shrn(l, t)), v(U32.mul(h, X.pow2(s)))), Nat.add(hl, C.shift(s, lh)), WA.add_exact(1n, {==}, U32.shrn(l, t), U32.mul(h, X.pow2(s)), hf), es)
162  +ev = Equal.trans(Nat, Nat.add(v(U32.add(U32.shrn(l, t), U32.mul(h, X.pow2(s)))), C.shift(32n, v(U32.shrn(h, t)))), Nat.add(Nat.add(hl, C.shift(s, lh)), C.shift(32n, v(U32.shrn(h, t)))), Nat.add(Nat.add(hl, C.shift(s, lh)), C.shift(32n, hh)), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, v(U32.shrn(h, t)))), v(U32.add(U32.shrn(l, t), U32.mul(h, X.pow2(s)))), Nat.add(hl, C.shift(s, lh)), elo), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(hl, C.shift(s, lh)), C.shift(32n, z)), v(U32.shrn(h, t)), hh, a3))
163  +e32 = Equal.trans(Nat, C.shift(32n, v(h)), C.shift(Nat.add(t, s), v(h)), C.shift(t, C.shift(s, v(h))), Equal.cong(Nat, Nat, z => C.shift(z, v(h)), 32n, Nat.add(t, s), Equal.sym(Nat, Nat.add(t, s), 32n, hts)), WW.shift_comp(t, s, v(h)))
164  +eh1 = Equal.trans(Nat, C.high(t, val(l, h)), C.high(t, Nat.add(v(l), C.shift(t, C.shift(s, v(h))))), Nat.add(hl, C.shift(s, v(h))), Equal.cong(Nat, Nat, z => C.high(t, Nat.add(v(l), z)), C.shift(32n, v(h)), C.shift(t, C.shift(s, v(h))), e32), WW.high_add_shift(t, v(l), C.shift(s, v(h))))
165  +esh = Equal.trans(Nat, C.shift(s, v(h)), C.shift(s, Nat.add(lh, C.shift(t, hh))), Nat.add(C.shift(s, lh), C.shift(32n, hh)), Equal.cong(Nat, Nat, z => C.shift(s, z), v(h), Nat.add(lh, C.shift(t, hh)), WW.low_high(t, v(h))), Equal.trans(Nat, C.shift(s, Nat.add(lh, C.shift(t, hh))), Nat.add(C.shift(s, lh), C.shift(s, C.shift(t, hh))), Nat.add(C.shift(s, lh), C.shift(32n, hh)), WW.shift_add(s, lh, C.shift(t, hh)), Equal.cong(Nat, Nat, z => Nat.add(C.shift(s, lh), z), C.shift(s, C.shift(t, hh)), C.shift(32n, hh), Equal.trans(Nat, C.shift(s, C.shift(t, hh)), C.shift(Nat.add(s, t), hh), C.shift(32n, hh), Equal.sym(Nat, C.shift(Nat.add(s, t), hh), C.shift(s, C.shift(t, hh)), WW.shift_comp(s, t, hh)), Equal.cong(Nat, Nat, z => C.shift(z, hh), Nat.add(s, t), 32n, hst)))))
166  +et = Equal.trans(Nat, C.high(t, val(l, h)), Nat.add(hl, Nat.add(C.shift(s, lh), C.shift(32n, hh))), Nat.add(Nat.add(hl, C.shift(s, lh)), C.shift(32n, hh)), Equal.trans(Nat, C.high(t, val(l, h)), Nat.add(hl, C.shift(s, v(h))), Nat.add(hl, Nat.add(C.shift(s, lh), C.shift(32n, hh))), eh1, Equal.cong(Nat, Nat, z => Nat.add(hl, z), C.shift(s, v(h)), Nat.add(C.shift(s, lh), C.shift(32n, hh)), esh)), Equal.sym(Nat, Nat.add(Nat.add(hl, C.shift(s, lh)), C.shift(32n, hh)), Nat.add(hl, Nat.add(C.shift(s, lh), C.shift(32n, hh))), NA.add_assoc(hl, C.shift(s, lh), C.shift(32n, hh))))
167  Equal.trans(Nat, Nat.add(v(U32.add(U32.shrn(l, t), U32.mul(h, X.pow2(s)))), C.shift(32n, v(U32.shrn(h, t)))), Nat.add(Nat.add(hl, C.shift(s, lh)), C.shift(32n, hh)), C.high(t, val(l, h)), ev, Equal.sym(Nat, C.high(t, val(l, h)), Nat.add(Nat.add(hl, C.shift(s, lh)), C.shift(32n, hh)), et))