def halfval

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64add.bend:241

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/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/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend as W64M
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/u32laws.bend as LW
import bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend as PD

241def halfval(+one: Nat, +h1: {one == 1n : Nat}, +l: U32, +h: U32, +c: U32, +pc: {c == U32{WD.pw(32n, 31n)} : U32}) -> {SW.value(half_g(l, h, c)) == Nat.div(val(l, h), 2n) : Nat}:
242  +b = U32.and(h, 1)
243  +s31 = C.shift(31n, one)
244  +bt = C.bit(v(h))
245  +evb = Equal.trans(Nat, v(b), Nat.mod(v(h), 2n), bt, LW.odd_val(h), Equal.sym(Nat, bt, Nat.mod(v(h), 2n), WW.bit_mod(v(h))))
246  +evc = Equal.trans(Nat, v(c), WD.sc(31n, one), s31, PD.pow32(31n, {==}, one, h1, c, pc), Equal.sym(Nat, s31, WD.sc(31n, one), W64M.shift_sc(31n, one)))
247  +hb1 = WW.bit_le1(v(h))
248  +epr = Equal.trans(Nat, Nat.mul(v(b), v(c)), Nat.mul(bt, v(c)), Nat.mul(bt, s31), Equal.cong(Nat, Nat, t => Nat.mul(t, v(c)), v(b), bt, evb), Equal.cong(Nat, Nat, t => Nat.mul(bt, t), v(c), s31, evc))
249  +hs1 = L.subst(Nat, z => {Nat.is_le(z, s31) == True{} : Bool}, one, 1n, h1, WW.shift_ge(31n, one))
250  +hsd = N.succ_le_lt(s31, Nat.double(s31), N.double_succ_le(s31, hs1))
251  +hple = L.subst(Nat, z => {Nat.is_le(z, s31) == True{} : Bool}, Nat.mul(bt, s31), Nat.mul(v(b), v(c)), Equal.sym(Nat, Nat.mul(v(b), v(c)), Nat.mul(bt, s31), epr), mul_le1(bt, s31, hb1))
252  +hplt = L.subst(Nat, z => {Nat.is_lt(Nat.mul(v(b), v(c)), z) == True{} : Bool}, C.shift(32n, one), WD.sc(32n, one), W64M.shift_sc(32n, one), N.le_lt_trans(Nat.mul(v(b), v(c)), s31, Nat.double(s31), hple, hsd))
253  +m = U32.mul(b, c)
254  +evm = Equal.trans(Nat, v(m), Nat.mul(v(b), v(c)), Nat.mul(bt, s31), PD.mul32(one, h1, b, c, hplt), epr)
255  +hl = C.half(v(l))
256  +evs = Equal.trans(Nat, v(U32.shr(l)), Nat.div(v(l), 2n), hl, LW.ops_half(l), Equal.sym(Nat, hl, Nat.div(v(l), 2n), half_div(v(l))))
257  +hlt = Equal.trans(Bool, Nat.is_lt(hl, s31), Nat.is_lt(v(l), Nat.double(s31)), True{}, WW.lt_half(v(l), s31), WW.lt_one(32n, one, h1, v(l), vb(l)))
258  +hsum = N.lt_le_trans(Nat.add(hl, Nat.mul(bt, s31)), Nat.add(s31, Nat.mul(bt, s31)), Nat.double(s31), N.lt_add_r2(hl, s31, Nat.mul(bt, s31), hlt), L.subst(Nat, z => {Nat.is_le(Nat.add(s31, Nat.mul(bt, s31)), z) == True{} : Bool}, Nat.add(s31, s31), Nat.double(s31), Equal.sym(Nat, Nat.double(s31), Nat.add(s31, s31), NA.double_self(s31)), N.le_add_left(Nat.mul(bt, s31), s31, s31, mul_le1(bt, s31, hb1))))
259  +es = Equal.trans(Nat, Nat.add(v(U32.shr(l)), v(m)), Nat.add(hl, v(m)), Nat.add(hl, Nat.mul(bt, s31)), Equal.cong(Nat, Nat, t => Nat.add(t, v(m)), v(U32.shr(l)), hl, evs), Equal.cong(Nat, Nat, t => Nat.add(hl, t), v(m), Nat.mul(bt, s31), evm))
260  +hfit = WW.fits_one(32n, one, h1, Nat.add(v(U32.shr(l)), v(m)), L.subst(Nat, z => {Nat.is_lt(z, C.shift(32n, one)) == True{} : Bool}, Nat.add(hl, Nat.mul(bt, s31)), Nat.add(v(U32.shr(l)), v(m)), Equal.sym(Nat, Nat.add(v(U32.shr(l)), v(m)), Nat.add(hl, Nat.mul(bt, s31)), es), hsum))
261  +elo = Equal.trans(Nat, v(U32.add(U32.shr(l), m)), Nat.add(v(U32.shr(l)), v(m)), Nat.add(hl, Nat.mul(bt, s31)), add_exact(one, h1, U32.shr(l), m, hfit), es)
262  +ehi = Equal.trans(Nat, v(U32.shr(h)), Nat.div(v(h), 2n), C.half(v(h)), LW.ops_half(h), Equal.sym(Nat, C.half(v(h)), Nat.div(v(h), 2n), half_div(v(h))))
263  +ev = Equal.trans(Nat, Nat.add(v(U32.add(U32.shr(l), m)), C.shift(32n, v(U32.shr(h)))), Nat.add(Nat.add(hl, Nat.mul(bt, s31)), C.shift(32n, v(U32.shr(h)))), Nat.add(Nat.add(hl, Nat.mul(bt, s31)), C.shift(32n, C.half(v(h)))), Equal.cong(Nat, Nat, t => Nat.add(t, C.shift(32n, v(U32.shr(h)))), v(U32.add(U32.shr(l), m)), Nat.add(hl, Nat.mul(bt, s31)), elo), Equal.cong(Nat, Nat, t => Nat.add(Nat.add(hl, Nat.mul(bt, s31)), C.shift(32n, t)), v(U32.shr(h)), C.half(v(h)), ehi))
264  +eh = WW.half_limbs(31n, one, h1, v(l), v(h))
265  Equal.trans(Nat, Nat.add(v(U32.add(U32.shr(l), m)), C.shift(32n, v(U32.shr(h)))), C.half(val(l, h)), Nat.div(val(l, h), 2n), Equal.trans(Nat, Nat.add(v(U32.add(U32.shr(l), m)), C.shift(32n, v(U32.shr(h)))), Nat.add(Nat.add(hl, Nat.mul(bt, s31)), C.shift(32n, C.half(v(h)))), C.half(val(l, h)), ev, Equal.sym(Nat, C.half(val(l, h)), Nat.add(Nat.add(hl, Nat.mul(bt, s31)), C.shift(32n, C.half(v(h)))), eh)), half_div(val(l, h)))