def iszero_g

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

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
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
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/u32laws.bend as LW

274def iszero_g(+l: U32, +h: U32, +m31: U32, +hm31: {m31 == U32{WD.mask(32n, 31n)} : U32}) -> {X.is_zero(WU.U64{l, U32.and(h, m31)}) == SF.is_zero(F.Bits{l, h}) : Bool}:
275  +H = v(h)
276  +f = C.low(20n, H)
277  +E = C.low(11n, C.high(20n, H))
278  +e1 = Equal.cong(Bool, Bool, z => Bool.and(z, U32.is_zero(U32.and(h, m31))), U32.is_zero(l), Nat.is_eq(v(l), 0n), LW.zero_nat(l))
279  +e2 = Equal.trans(Bool, U32.is_zero(U32.and(h, m31)), Nat.is_eq(v(U32.and(h, m31)), 0n), Nat.is_eq(C.low(31n, H), 0n), LW.zero_nat(U32.and(h, m31)), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), v(U32.and(h, m31)), C.low(31n, H), andm(h, 31n, m31, hm31)))
280  +e3 = Equal.trans(Bool, Nat.is_eq(C.low(31n, H), 0n), Nat.is_eq(Nat.add(f, C.shift(20n, E)), 0n), Bool.and(Nat.is_eq(f, 0n), Nat.is_eq(E, 0n)), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), C.low(31n, H), Nat.add(f, C.shift(20n, E)), low_split(20n, 11n, H)), z2(f, 20n, E))
281  +e4 = Equal.cong(Bool, Bool, z => Bool.and(Nat.is_eq(v(l), 0n), z), U32.is_zero(U32.and(h, m31)), Bool.and(Nat.is_eq(f, 0n), Nat.is_eq(E, 0n)), Equal.trans(Bool, U32.is_zero(U32.and(h, m31)), Nat.is_eq(C.low(31n, H), 0n), Bool.and(Nat.is_eq(f, 0n), Nat.is_eq(E, 0n)), e2, e3))
282  +e5 = rot3(Nat.is_eq(v(l), 0n), Nat.is_eq(f, 0n), Nat.is_eq(E, 0n))
283  +e6 = Equal.cong(Bool, Bool, z => Bool.and(Nat.is_eq(E, 0n), z), Bool.and(Nat.is_eq(v(l), 0n), Nat.is_eq(f, 0n)), Nat.is_eq(Nat.add(v(l), C.shift(32n, f)), 0n), Equal.sym(Bool, Nat.is_eq(Nat.add(v(l), C.shift(32n, f)), 0n), Bool.and(Nat.is_eq(v(l), 0n), Nat.is_eq(f, 0n)), z2(v(l), 32n, f)))
284  Equal.trans(Bool, Bool.and(U32.is_zero(l), U32.is_zero(U32.and(h, m31))), Bool.and(Nat.is_eq(v(l), 0n), U32.is_zero(U32.and(h, m31))), Bool.and(Nat.is_eq(E, 0n), Nat.is_eq(Nat.add(v(l), C.shift(32n, f)), 0n)), e1, Equal.trans(Bool, Bool.and(Nat.is_eq(v(l), 0n), U32.is_zero(U32.and(h, m31))), Bool.and(Nat.is_eq(v(l), 0n), Bool.and(Nat.is_eq(f, 0n), Nat.is_eq(E, 0n))), Bool.and(Nat.is_eq(E, 0n), Nat.is_eq(Nat.add(v(l), C.shift(32n, f)), 0n)), e4, Equal.trans(Bool, Bool.and(Nat.is_eq(v(l), 0n), Bool.and(Nat.is_eq(f, 0n), Nat.is_eq(E, 0n))), Bool.and(Nat.is_eq(E, 0n), Bool.and(Nat.is_eq(v(l), 0n), Nat.is_eq(f, 0n))), Bool.and(Nat.is_eq(E, 0n), Nat.is_eq(Nat.add(v(l), C.shift(32n, f)), 0n)), e5, e6)))