def cvb

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:203

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/f64.bend as SF
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
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U

203# the value of clear0(r, b): r, or r with bit 0 cleared
204def cvb(+l: U32, +h: U32, +b: Bool) -> {SW.value(X.clear0(WU.U64{l, h}, b)) == SF.pick(Nat, b, Nat.sub(SW.value(WU.U64{l, h}), Nat.mod(SW.value(WU.U64{l, h}), 2n)), SW.value(WU.U64{l, h})) : Nat}:
205  match b:
206    case True{}:
207      +vl = v(l)
208      +S32 = C.shift(32n, v(h))
209      +m = Nat.mod(vl, 2n)
210      +em = LW.odd_val(l)
211      +hle = L.subst(Nat, z => {Nat.is_le(z, vl) == True{} : Bool}, C.bit(vl), m, WW.bit_mod(vl), bit_le_self(vl))
212      +hle2 = L.subst(Nat, z => {Nat.is_le(z, vl) == True{} : Bool}, m, v(U32.and(l, 1)), Equal.sym(Nat, v(U32.and(l, 1)), m, em), hle)
213      +es2 = Equal.trans(Nat, v(U32.sub(l, U32.and(l, 1))), Nat.sub(vl, v(U32.and(l, 1))), Nat.sub(vl, m), U.sub_nat(l, U32.and(l, 1), hle2), Equal.cong(Nat, Nat, z => Nat.sub(vl, z), v(U32.and(l, 1)), m, em))
214      +e1 = Equal.cong(Nat, Nat, z => Nat.add(z, S32), v(U32.sub(l, U32.and(l, 1))), Nat.sub(vl, m), es2)
215      +eo = WW.odd_limb(31n, vl, v(h))
216      +e2 = Equal.trans(Nat, Nat.sub(Nat.add(vl, S32), Nat.mod(Nat.add(vl, S32), 2n)), Nat.sub(Nat.add(vl, S32), m), Nat.add(Nat.sub(vl, m), S32), Equal.cong(Nat, Nat, z => Nat.sub(Nat.add(vl, S32), z), Nat.mod(Nat.add(vl, S32), 2n), m, eo), sub_add_r(vl, S32, m, hle))
217      Equal.trans(Nat, SW.value(X.clear0(WU.U64{l, h}, True{})), Nat.sub(SW.value(WU.U64{l, h}), Nat.mod(SW.value(WU.U64{l, h}), 2n)), SF.pick(Nat, True{}, Nat.sub(SW.value(WU.U64{l, h}), Nat.mod(SW.value(WU.U64{l, h}), 2n)), SW.value(WU.U64{l, h})), Equal.trans(Nat, Nat.add(v(U32.sub(l, U32.and(l, 1))), S32), Nat.add(Nat.sub(vl, m), S32), Nat.sub(Nat.add(vl, S32), Nat.mod(Nat.add(vl, S32), 2n)), e1, Equal.sym(Nat, Nat.sub(Nat.add(vl, S32), Nat.mod(Nat.add(vl, S32), 2n)), Nat.add(Nat.sub(vl, m), S32), e2)), Equal.sym(Nat, SF.pick(Nat, True{}, Nat.sub(SW.value(WU.U64{l, h}), Nat.mod(SW.value(WU.U64{l, h}), 2n)), SW.value(WU.U64{l, h})), Nat.sub(SW.value(WU.U64{l, h}), Nat.mod(SW.value(WU.U64{l, h}), 2n)), pk_t(Nat, Nat.sub(SW.value(WU.U64{l, h}), Nat.mod(SW.value(WU.U64{l, h}), 2n)), SW.value(WU.U64{l, h}))))
218    case False{}:
219      +vl = v(l)
220      +e0 = FB.andm(l, 0n, 0, {==})
221      +hle = L.subst(Nat, z => {Nat.is_le(z, vl) == True{} : Bool}, 0n, v(U32.and(l, 0)), Equal.sym(Nat, v(U32.and(l, 0)), 0n, e0), N.zero_le(vl))
222      +es2 = Equal.trans(Nat, v(U32.sub(l, U32.and(l, 0))), Nat.sub(vl, v(U32.and(l, 0))), vl, U.sub_nat(l, U32.and(l, 0), hle), Equal.trans(Nat, Nat.sub(vl, v(U32.and(l, 0))), Nat.sub(vl, 0n), vl, Equal.cong(Nat, Nat, z => Nat.sub(vl, z), v(U32.and(l, 0)), 0n, e0), N.sub_zero(vl)))
223      Equal.trans(Nat, SW.value(X.clear0(WU.U64{l, h}, False{})), SW.value(WU.U64{l, h}), SF.pick(Nat, False{}, Nat.sub(SW.value(WU.U64{l, h}), Nat.mod(SW.value(WU.U64{l, h}), 2n)), SW.value(WU.U64{l, h})), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, v(h))), v(U32.sub(l, U32.and(l, 0))), vl, es2), Equal.sym(Nat, SF.pick(Nat, False{}, Nat.sub(SW.value(WU.U64{l, h}), Nat.mod(SW.value(WU.U64{l, h}), 2n)), SW.value(WU.U64{l, h})), SW.value(WU.U64{l, h}), pk_f(Nat, Nat.sub(SW.value(WU.U64{l, h}), Nat.mod(SW.value(WU.U64{l, h}), 2n)), SW.value(WU.U64{l, h}))))