def yv

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64est.bend:125

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/w64dm.bend as DM
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/w64sh.bend as SH
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW

125# x >> t as the sum of xl >> t and xh << (64 - t), below 2^64
126def yv(+xl: WU.U64, +xh: U32, +t: Nat, +t1: {Nat.is_le(1n, t) == True{} : Bool}, +t32: {Nat.is_le(t, 32n) == True{} : Bool}, +hx: {C.fits(Nat.add(64n, t), DM.X96(xl, xh)) == True{} : Bool}) -> {SW.value(X.add(X.shr(xl, t), X.shl(WU.U64{xh, 0}, Nat.sub(64n, t)))) == C.high(t, DM.X96(xl, xh)) : Nat}:
127  +k = Nat.sub(64n, t)
128  +x9 = DM.X96(xl, xh)
129  +t64 = N.le_trans(t, 32n, 64n, t32, {==})
130  +ek = N.sub_add(64n, t, t64)
131  +h64 = Equal.trans(Bool, Nat.is_lt(Nat.add(64n, 0n), Nat.add(64n, t)), Nat.is_lt(0n, t), True{}, WW.lt_cancel_l(64n, 0n, t), N.succ_le_lt(0n, t, t1))
132  +hk = N.sub_lt(64n, t, 64n, t64, L.subst(Nat, z => {Nat.is_lt(64n, z) == True{} : Bool}, Nat.add(64n, t), Nat.add(t, 64n), N.add_comm(64n, t), h64))
133  +exh = WW.high_u(64n, SW.value(xl), v(xh), DM.fit64(xl))
134  +fxh = L.subst(Nat, z => {C.fits(t, z) == True{} : Bool}, C.high(64n, x9), v(xh), exh, SH.fits_high(64n, t, x9, hx))
135  +s = C.shift(k, v(xh))
136  +eka = Equal.trans(Nat, Nat.add(k, t), Nat.add(t, k), 64n, N.add_comm(k, t), ek)
137  +hs0 = WW.shift_lt(k, v(xh), C.pow2(t), WW.lt_of_fits(t, v(xh), fxh))
138  +els = low_shift(64n, k, t, v(xh), eka, hs0)
139  +esh = Equal.trans(Nat, C.shift(64n, v(xh)), C.shift(Nat.add(t, k), v(xh)), C.shift(t, s), Equal.cong(Nat, Nat, z => C.shift(z, v(xh)), 64n, Nat.add(t, k), Equal.sym(Nat, Nat.add(t, k), 64n, ek)), WW.shift_comp(t, k, v(xh)))
140  +ex = Equal.cong(Nat, Nat, z => Nat.add(SW.value(xl), z), C.shift(64n, v(xh)), C.shift(t, s), esh)
141  +ehx = Equal.trans(Nat, C.high(t, x9), C.high(t, Nat.add(SW.value(xl), C.shift(t, s))), Nat.add(C.high(t, SW.value(xl)), s), Equal.cong(Nat, Nat, z => C.high(t, z), x9, Nat.add(SW.value(xl), C.shift(t, s)), ex), WW.high_add_shift(t, SW.value(xl), s))
142  +hx2 = L.subst(Nat, z => {C.fits(z, x9) == True{} : Bool}, Nat.add(64n, t), Nat.add(t, 64n), N.add_comm(64n, t), hx)
143  +fy = SH.fits_high(t, 64n, x9, hx2)
144  +a = X.shr(xl, t)
145  +bw = X.shl(WU.U64{xh, 0}, k)
146  +eb = Equal.trans(Nat, SW.value(bw), C.low(64n, C.shift(k, SW.value(WU.U64{xh, 0}))), s, SH.shl_value(WU.U64{xh, 0}, k, hk), Equal.trans(Nat, C.low(64n, C.shift(k, SW.value(WU.U64{xh, 0}))), C.low(64n, s), s, Equal.cong(Nat, Nat, z => C.low(64n, C.shift(k, z)), SW.value(WU.U64{xh, 0}), v(xh), DM.u32_0(xh)), els))
147  +esum = Equal.trans(Nat, Nat.add(SW.value(a), SW.value(bw)), Nat.add(C.high(t, SW.value(xl)), s), C.high(t, x9), Equal.trans(Nat, Nat.add(SW.value(a), SW.value(bw)), Nat.add(C.high(t, SW.value(xl)), SW.value(bw)), Nat.add(C.high(t, SW.value(xl)), s), Equal.cong(Nat, Nat, z => Nat.add(z, SW.value(bw)), SW.value(a), C.high(t, SW.value(xl)), SH.shr_value(xl, t)), Equal.cong(Nat, Nat, z => Nat.add(C.high(t, SW.value(xl)), z), SW.value(bw), s, eb)), Equal.sym(Nat, C.high(t, x9), Nat.add(C.high(t, SW.value(xl)), s), ehx))
148  Equal.trans(Nat, SW.value(X.add(a, bw)), C.low(64n, Nat.add(SW.value(a), SW.value(bw))), C.high(t, x9), WA.add_value(a, bw), Equal.trans(Nat, C.low(64n, Nat.add(SW.value(a), SW.value(bw))), C.low(64n, C.high(t, x9)), C.high(t, x9), Equal.cong(Nat, Nat, z => C.low(64n, z), Nat.add(SW.value(a), SW.value(bw)), C.high(t, x9), esum), WW.low_fit(64n, C.high(t, x9), fy)))