def tie_v

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

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/w64.bend as SW
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/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

230# the tie test reads the low 10 bits
231def tie_v(+l: U32, +h: U32) -> {U32.is_eq(U32.and(l, 1023), 512) == Nat.is_eq(C.low(10n, SW.value(WU.U64{l, h})), 512n) : Bool}:
232  +e1 = LW.eq_nat(U32.and(l, 1023), 512)
233  +e2 = Equal.cong(Nat, Bool, z => Nat.is_eq(z, 512n), v(U32.and(l, 1023)), C.low(10n, v(l)), FB.andm(l, 10n, 1023, {==}))
234  +e3 = Equal.trans(Nat, C.low(10n, Nat.add(v(l), C.shift(32n, v(h)))), C.low(10n, Nat.add(v(l), C.shift(10n, C.shift(22n, v(h))))), C.low(10n, v(l)), Equal.cong(Nat, Nat, z => C.low(10n, Nat.add(v(l), z)), C.shift(32n, v(h)), C.shift(10n, C.shift(22n, v(h))), WW.shift_comp(10n, 22n, v(h))), WW.low_add_shift(10n, v(l), C.shift(22n, v(h))))
235  Equal.trans(Bool, U32.is_eq(U32.and(l, 1023), 512), Nat.is_eq(C.low(10n, v(l)), 512n), Nat.is_eq(C.low(10n, SW.value(WU.U64{l, h})), 512n), Equal.trans(Bool, U32.is_eq(U32.and(l, 1023), 512), Nat.is_eq(v(U32.and(l, 1023)), 512n), Nat.is_eq(C.low(10n, v(l)), 512n), e1, e2), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 512n), C.low(10n, v(l)), C.low(10n, SW.value(WU.U64{l, h})), Equal.sym(Nat, C.low(10n, SW.value(WU.U64{l, h})), C.low(10n, v(l)), e3)))