def isinf_g

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64bits.bend:252

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
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/word.bend as WD

252def isinf_g(+one: Nat, +h1: {one == 1n : Nat}, +l: U32, +h: U32, +c20: U32, +hc20: {c20 == U32{WD.pw(32n, 20n)} : U32}, +m11: U32, +hm11: {m11 == U32{WD.mask(32n, 11n)} : U32}, +m20: U32, +hm20: {m20 == U32{WD.mask(32n, 20n)} : U32}) -> {Bool.and(Nat.is_eq(v(U32.and(U32.div(h, c20), m11)), 2047n), X.is_zero(WU.U64{l, U32.and(h, m20)})) == SF.is_inf(F.Bits{l, h}) : Bool}:
253  +ei = v(U32.and(U32.div(h, c20), m11))
254  +es = SF.efield(F.Bits{l, h})
255  +zi = X.is_zero(WU.U64{l, U32.and(h, m20)})
256  +zs = Nat.is_eq(SF.frac(F.Bits{l, h}), 0n)
257  Equal.trans(Bool, Bool.and(Nat.is_eq(ei, 2047n), zi), Bool.and(Nat.is_eq(es, 2047n), zi), Bool.and(Nat.is_eq(es, 2047n), zs), Equal.cong(Nat, Bool, z => Bool.and(Nat.is_eq(z, 2047n), zi), ei, es, ef_g(one, h1, h, c20, hc20, m11, hm11)), Equal.cong(Bool, Bool, z => Bool.and(Nat.is_eq(es, 2047n), z), zi, zs, fz_g(l, h, m20, hm20)))