def top_eq

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64tools.bend:136

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/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/lemmas/proofs/nat_algebra.bend as NA
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/w64add.bend as WA
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/word.bend as WD

136# the top value 2^63 of the test in rw_z (the word c = 2^31 kept abstract, so
137# the checker never expands 2^31 in unary)
138def top_eq(+one: Nat, +h1: {one == 1n : Nat}, +w: WU.U64, +c: U32, +hc: {c == U32{WD.pw(32n, 31n)} : U32}) -> {X.le(WU.U64{0, c}, w) == Bool.not(C.fits(63n, SW.value(w))) : Bool}:
139  e1 = WA.le_value(WU.U64{0, c}, w)
140  +ec = FB.pwv(31n, {==}, one, h1, c, hc)
141  +e2 = Equal.cong(Nat, Nat, t => Nat.add(0n, C.shift(32n, t)), v(c), C.shift(31n, one), ec)
142  +S = C.shift(32n, C.shift(31n, one))
143  +e30 = Equal.trans(Nat, Nat.add(0n, S), Nat.add(S, 0n), S, NA.add_comm(0n, S), N.add_zero(S))
144  +e3 = Equal.trans(Nat, Nat.add(0n, S), S, C.shift(63n, one), e30, Equal.sym(Nat, C.shift(63n, one), S, WW.shift_comp(32n, 31n, one)))
145  +e4 = Equal.cong(Nat, Bool, t => Nat.is_le(t, SW.value(w)), SW.value(WU.U64{0, c}), C.shift(63n, one), Equal.trans(Nat, SW.value(WU.U64{0, c}), Nat.add(0n, C.shift(32n, C.shift(31n, one))), C.shift(63n, one), e2, e3))
146  Equal.trans(Bool, X.le(WU.U64{0, c}, w), Nat.is_le(SW.value(WU.U64{0, c}), SW.value(w)), Bool.not(C.fits(63n, SW.value(w))), e1, Equal.trans(Bool, Nat.is_le(SW.value(WU.U64{0, c}), SW.value(w)), Nat.is_le(C.shift(63n, one), SW.value(w)), Bool.not(C.fits(63n, SW.value(w))), e4, FB.le_fit(63n, one, h1, SW.value(w))))