def shl_small

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

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/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

210def shl_small(+l: U32, +h: U32, +j: Nat, +hk: {Nat.is_lt(1n+j, 32n) == True{} : Bool}) -> {SW.value(X.shl_lt(WU.U64{l, h}, 1n+j)) == C.low(64n, C.shift(1n+j, val(l, h))) : Nat}:
211  +t = {1n+j : Nat}
212  +s = Nat.sub(32n, t)
213  +hts = N.sub_add(32n, t, N.lt_le(t, 32n, hk))
214  +hst = Equal.trans(Nat, Nat.add(s, t), Nat.add(t, s), 32n, N.add_comm(s, t), hts)
215  +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))))
216  +a1 = Equal.trans(Nat, v(U32.mul(l, X.pow2(t))), C.low(32n, C.shift(t, v(l))), C.shift(t, C.low(s, v(l))), mul_p2(l, t, hk), Equal.trans(Nat, C.low(32n, C.shift(t, v(l))), C.low(Nat.add(t, s), C.shift(t, v(l))), C.shift(t, C.low(s, v(l))), Equal.cong(Nat, Nat, z => C.low(z, C.shift(t, v(l))), 32n, Nat.add(t, s), Equal.sym(Nat, Nat.add(t, s), 32n, hts)), WW.low_shift(t, s, v(l))))
217  +a2 = Equal.trans(Nat, v(U32.mul(h, X.pow2(t))), C.low(32n, C.shift(t, v(h))), C.shift(t, C.low(s, v(h))), mul_p2(h, t, hk), Equal.trans(Nat, C.low(32n, C.shift(t, v(h))), C.low(Nat.add(t, s), C.shift(t, v(h))), C.shift(t, C.low(s, v(h))), Equal.cong(Nat, Nat, z => C.low(z, C.shift(t, v(h))), 32n, Nat.add(t, s), Equal.sym(Nat, Nat.add(t, s), 32n, hts)), WW.low_shift(t, s, v(h))))
218  +a3 = SR.shrn_high(l, s)
219  +hr = WW.lt_of_fits(t, C.high(s, v(l)), fits_high(s, t, v(l), fits32(s, t, hst, l)))
220  +hsum = WW.two_limb_lt(t, s, C.high(s, v(l)), C.low(s, v(h)), hr, WW.low_lt(s, v(h)))
221  +x1 = U32.mul(h, X.pow2(t))
222  +x2 = U32.shrn(l, s)
223  +es = Equal.trans(Nat, Nat.add(v(x1), v(x2)), Nat.add(C.shift(t, C.low(s, v(h))), C.high(s, v(l))), Nat.add(C.high(s, v(l)), C.shift(t, C.low(s, v(h)))), Equal.trans(Nat, Nat.add(v(x1), v(x2)), Nat.add(C.shift(t, C.low(s, v(h))), v(x2)), Nat.add(C.shift(t, C.low(s, v(h))), C.high(s, v(l))), Equal.cong(Nat, Nat, z => Nat.add(z, v(x2)), v(x1), C.shift(t, C.low(s, v(h))), a2), Equal.cong(Nat, Nat, z => Nat.add(C.shift(t, C.low(s, v(h))), z), v(x2), C.high(s, v(l)), a3)), N.add_comm(C.shift(t, C.low(s, v(h))), C.high(s, v(l))))
224  +hf = L.subst(Nat, z => {C.fits(z, Nat.add(v(x1), v(x2))) == True{} : Bool}, Nat.add(t, s), 32n, hts, WW.fits_of_lt(Nat.add(t, s), Nat.add(v(x1), v(x2)), L.subst(Nat, z => {Nat.is_lt(z, C.pow2(Nat.add(t, s))) == True{} : Bool}, Nat.add(C.high(s, v(l)), C.shift(t, C.low(s, v(h)))), Nat.add(v(x1), v(x2)), Equal.sym(Nat, Nat.add(v(x1), v(x2)), Nat.add(C.high(s, v(l)), C.shift(t, C.low(s, v(h)))), es), hsum)))
225  +ehi = Equal.trans(Nat, v(U32.add(x1, x2)), Nat.add(v(x1), v(x2)), Nat.add(C.high(s, v(l)), C.shift(t, C.low(s, v(h)))), WA.add_exact(1n, {==}, x1, x2, hf), es)
226  +ev = Equal.trans(Nat, Nat.add(v(U32.mul(l, X.pow2(t))), C.shift(32n, v(U32.add(x1, x2)))), Nat.add(C.shift(t, C.low(s, v(l))), C.shift(32n, v(U32.add(x1, x2)))), Nat.add(C.shift(t, C.low(s, v(l))), C.shift(32n, Nat.add(C.high(s, v(l)), C.shift(t, C.low(s, v(h)))))), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, v(U32.add(x1, x2)))), v(U32.mul(l, X.pow2(t))), C.shift(t, C.low(s, v(l))), a1), Equal.cong(Nat, Nat, z => Nat.add(C.shift(t, C.low(s, v(l))), C.shift(32n, z)), v(U32.add(x1, x2)), Nat.add(C.high(s, v(l)), C.shift(t, C.low(s, v(h)))), ehi))
227  +hR = WW.limbs_fit(32n, 32n, C.shift(t, C.low(s, v(l))), Nat.add(C.high(s, v(l)), C.shift(t, C.low(s, v(h)))), L.subst(Nat, z => {C.fits(z, C.shift(t, C.low(s, v(l)))) == True{} : Bool}, Nat.add(t, s), 32n, hts, WW.fits_of_lt(Nat.add(t, s), C.shift(t, C.low(s, v(l))), L.subst(Nat, z => {Nat.is_lt(C.shift(t, C.low(s, v(l))), z) == True{} : Bool}, C.shift(t, C.pow2(s)), C.pow2(Nat.add(t, s)), WW.shift_pow2(t, s), WW.shift_lt(t, C.low(s, v(l)), C.pow2(s), WW.low_lt(s, v(l)))))), L.subst(Nat, z => {C.fits(z, Nat.add(C.high(s, v(l)), C.shift(t, C.low(s, v(h))))) == True{} : Bool}, Nat.add(t, s), 32n, hts, WW.fits_of_lt(Nat.add(t, s), Nat.add(C.high(s, v(l)), C.shift(t, C.low(s, v(h)))), hsum)))
228  +et = Equal.trans(Nat, C.low(64n, C.shift(t, Nat.add(v(l), C.shift(32n, v(h))))), C.low(64n, Nat.add(Nat.add(C.shift(t, C.low(s, v(l))), C.shift(32n, Nat.add(C.high(s, v(l)), C.shift(t, C.low(s, v(h)))))), C.shift(64n, C.high(s, v(h))))), Nat.add(C.shift(t, C.low(s, v(l))), C.shift(32n, Nat.add(C.high(s, v(l)), C.shift(t, C.low(s, v(h)))))), Equal.cong(Nat, Nat, z => C.low(64n, z), C.shift(t, Nat.add(v(l), C.shift(32n, v(h)))), Nat.add(Nat.add(C.shift(t, C.low(s, v(l))), C.shift(32n, Nat.add(C.high(s, v(l)), C.shift(t, C.low(s, v(h)))))), C.shift(64n, C.high(s, v(h)))), shl_eq(t, s, hts, l, h)), Equal.trans(Nat, C.low(64n, Nat.add(Nat.add(C.shift(t, C.low(s, v(l))), C.shift(32n, Nat.add(C.high(s, v(l)), C.shift(t, C.low(s, v(h)))))), C.shift(64n, C.high(s, v(h))))), C.low(64n, Nat.add(C.shift(t, C.low(s, v(l))), C.shift(32n, Nat.add(C.high(s, v(l)), C.shift(t, C.low(s, v(h))))))), Nat.add(C.shift(t, C.low(s, v(l))), C.shift(32n, Nat.add(C.high(s, v(l)), C.shift(t, C.low(s, v(h)))))), WW.low_add_shift(64n, Nat.add(C.shift(t, C.low(s, v(l))), C.shift(32n, Nat.add(C.high(s, v(l)), C.shift(t, C.low(s, v(h)))))), C.high(s, v(h))), WW.low_fit(64n, Nat.add(C.shift(t, C.low(s, v(l))), C.shift(32n, Nat.add(C.high(s, v(l)), C.shift(t, C.low(s, v(h)))))), hR)))
229  Equal.trans(Nat, Nat.add(v(U32.mul(l, X.pow2(t))), C.shift(32n, v(U32.add(x1, x2)))), Nat.add(C.shift(t, C.low(s, v(l))), C.shift(32n, Nat.add(C.high(s, v(l)), C.shift(t, C.low(s, v(h)))))), C.low(64n, C.shift(t, Nat.add(v(l), C.shift(32n, v(h))))), ev, Equal.sym(Nat, C.low(64n, C.shift(t, Nat.add(v(l), C.shift(32n, v(h))))), Nat.add(C.shift(t, C.low(s, v(l))), C.shift(32n, Nat.add(C.high(s, v(l)), C.shift(t, C.low(s, v(h)))))), et))