def isnan_g

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

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-crypto@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD

240def isnan_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), Bool.not(X.is_zero(WU.U64{l, U32.and(h, m20)}))) == SF.is_nan(F.Bits{l, h}) : Bool}:
241  +ei = v(U32.and(U32.div(h, c20), m11))
242  +es = SF.efield(F.Bits{l, h})
243  +zi = X.is_zero(WU.U64{l, U32.and(h, m20)})
244  +zs = Nat.is_eq(SF.frac(F.Bits{l, h}), 0n)
245  Equal.trans(Bool, Bool.and(Nat.is_eq(ei, 2047n), Bool.not(zi)), Bool.and(Nat.is_eq(es, 2047n), Bool.not(zi)), Bool.and(Nat.is_eq(es, 2047n), Bool.not(zs)), Equal.cong(Nat, Bool, z => Bool.and(Nat.is_eq(z, 2047n), Bool.not(zi)), ei, es, ef_g(one, h1, h, c20, hc20, m11, hm11)), Equal.cong(Bool, Bool, z => Bool.and(Nat.is_eq(es, 2047n), Bool.not(z)), zi, zs, fz_g(l, h, m20, hm20)))