W64add.halfval: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend as W64add Lines 241-265 of bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend&start_line=241&end_line=265 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 def 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}: +b = U32.and(h, 1) +s31 = C.shift(31n, one) +bt = C.bit(v(h)) +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)))) +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))) +hb1 = WW.bit_le1(v(h)) +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)) +hs1 = L.subst(Nat, z => {Nat.is_le(z, s31) == True{} : Bool}, one, 1n, h1, WW.shift_ge(31n, one)) +hsd = N.succ_le_lt(s31, Nat.double(s31), N.double_succ_le(s31, hs1)) +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)) +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)) +m = U32.mul(b, c) +evm = Equal.trans(Nat, v(m), Nat.mul(v(b), v(c)), Nat.mul(bt, s31), PD.mul32(one, h1, b, c, hplt), epr) +hl = C.half(v(l)) +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)))) +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))) +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)))) +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)) +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)) +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) +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)))) +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)) +eh = WW.half_limbs(31n, one, h1, v(l), v(h)) 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))) Uses (50): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.and https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mul https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shr https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=double_self https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=subst https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=double_succ_le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_add_left https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_lt_trans https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_add_r2 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_le_trans https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=succ_le_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=pw https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=sc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/u32laws.bend&name=odd_val https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/u32laws.bend&name=ops_half https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend&name=add_exact https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend&name=half_div https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend&name=half_g https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend&name=mul_le1 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend&name=v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend&name=val https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend&name=vb https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend&name=shift_sc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend&name=bit_le1 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend&name=bit_mod https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend&name=fits_one https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend&name=half_limbs https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend&name=lt_half https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend&name=lt_one https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend&name=shift_ge https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend&name=mul32 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend&name=pow32 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=bit https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=half https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend&name=value