F64round.cvb: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as F64round Lines 203-223 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&start_line=203&end_line=223 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 # the value of clear0(r, b): r, or r with bit 0 cleared def 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}: match b: case True{}: +vl = v(l) +S32 = C.shift(32n, v(h)) +m = Nat.mod(vl, 2n) +em = LW.odd_val(l) +hle = L.subst(Nat, z => {Nat.is_le(z, vl) == True{} : Bool}, C.bit(vl), m, WW.bit_mod(vl), bit_le_self(vl)) +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) +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)) +e1 = Equal.cong(Nat, Nat, z => Nat.add(z, S32), v(U32.sub(l, U32.and(l, 1))), Nat.sub(vl, m), es2) +eo = WW.odd_limb(31n, vl, v(h)) +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)) 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})))) case False{}: +vl = v(l) +e0 = FB.andm(l, 0n, 0, {==}) +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)) +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))) 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})))) Uses (31): 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.is_le 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.sub https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 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.sub https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=subst https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=sub_zero https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=zero_le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend&name=sub_nat https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend&name=andm https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=bit_le_self https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=pk_f https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=pk_t https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=sub_add_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend&name=odd_val https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=bit_mod https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=odd_limb https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=bit https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=pick https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=clear0