def shl_big

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

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

231def shl_big(+l: U32, +h: U32, +k: Nat, +hge: {Nat.is_le(32n, k) == True{} : Bool}, +hlt: {Nat.is_lt(k, 64n) == True{} : Bool}) -> {SW.value(WU.U64{0, U32.mul(l, X.pow2(Nat.sub(k, 32n)))}) == C.low(64n, C.shift(k, val(l, h))) : Nat}:
232  +d = Nat.sub(k, 32n)
233  +ek = N.sub_add(k, 32n, hge)
234  +hd = L.subst(Nat, z => {Nat.is_lt(d, z) == True{} : Bool}, Nat.sub(64n, 32n), 32n, {==}, WW.sub_lt_sub(k, 64n, 32n, hlt, hge))
235  +y = C.shift(d, v(l))
236  +w = C.shift(d, v(h))
237  +e1 = Equal.trans(Nat, C.shift(k, val(l, h)), C.shift(Nat.add(32n, d), val(l, h)), C.shift(32n, C.shift(d, val(l, h))), Equal.cong(Nat, Nat, z => C.shift(z, val(l, h)), k, Nat.add(32n, d), Equal.sym(Nat, Nat.add(32n, d), k, ek)), WW.shift_comp(32n, d, val(l, h)))
238  +e2 = Equal.trans(Nat, C.shift(d, val(l, h)), Nat.add(y, C.shift(d, C.shift(32n, v(h)))), Nat.add(y, C.shift(32n, w)), WW.shift_add(d, v(l), C.shift(32n, v(h))), Equal.cong(Nat, Nat, z => Nat.add(y, z), C.shift(d, C.shift(32n, v(h))), C.shift(32n, w), shift_swap(d, 32n, v(h))))
239  +e3 = Equal.trans(Nat, C.shift(32n, Nat.add(y, C.shift(32n, w))), Nat.add(C.shift(32n, y), C.shift(32n, C.shift(32n, w))), Nat.add(C.shift(32n, y), C.shift(64n, w)), WW.shift_add(32n, y, C.shift(32n, w)), Equal.cong(Nat, Nat, z => Nat.add(C.shift(32n, y), z), C.shift(32n, C.shift(32n, w)), C.shift(64n, w), Equal.sym(Nat, C.shift(64n, w), C.shift(32n, C.shift(32n, w)), WW.shift_comp(32n, 32n, w))))
240  +e4 = Equal.trans(Nat, C.shift(k, val(l, h)), C.shift(32n, C.shift(d, val(l, h))), Nat.add(C.shift(32n, y), C.shift(64n, w)), e1, Equal.trans(Nat, C.shift(32n, C.shift(d, val(l, h))), C.shift(32n, Nat.add(y, C.shift(32n, w))), Nat.add(C.shift(32n, y), C.shift(64n, w)), Equal.cong(Nat, Nat, z => C.shift(32n, z), C.shift(d, val(l, h)), Nat.add(y, C.shift(32n, w)), e2), e3))
241  +e5 = Equal.trans(Nat, C.low(64n, C.shift(k, val(l, h))), C.low(64n, Nat.add(C.shift(32n, y), C.shift(64n, w))), C.shift(32n, C.low(32n, y)), Equal.cong(Nat, Nat, z => C.low(64n, z), C.shift(k, val(l, h)), Nat.add(C.shift(32n, y), C.shift(64n, w)), e4), Equal.trans(Nat, C.low(64n, Nat.add(C.shift(32n, y), C.shift(64n, w))), C.low(64n, C.shift(32n, y)), C.shift(32n, C.low(32n, y)), WW.low_add_shift(64n, C.shift(32n, y), w), WW.low_shift(32n, 32n, y)))
242  Equal.trans(Nat, C.shift(32n, v(U32.mul(l, X.pow2(d)))), C.shift(32n, C.low(32n, y)), C.low(64n, C.shift(k, val(l, h))), Equal.cong(Nat, Nat, z => C.shift(32n, z), v(U32.mul(l, X.pow2(d))), C.low(32n, y), mul_p2(l, d, hd)), Equal.sym(Nat, C.low(64n, C.shift(k, val(l, h))), C.shift(32n, C.low(32n, y)), e5))