def mo_top

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64add.bend:445

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/src/math/w64.bend as X
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/u32laws.bend as LW

445def mo_top(+al: U32, +ah: U32, +bl: U32, +bh: U32, +z1: Bool, +z2: Bool, +hz1: {U32.is_zero(ah) == z1 : Bool}, +hz2: {U32.is_zero(bh) == z2 : Bool}) -> {Bool.or(Bool.and(Bool.not(z1), Bool.not(z2)), X.mul_over_one(X.mul32(al, bl), X.add(X.mul32(ah, bl), X.mul32(al, bh)))) == Bool.not(C.fits(64n, Nat.mul(val(al, ah), val(bl, bh)))) : Bool}:
446  match z1 z2:
447    case False{} False{}:
448      +h1 = pos_ne(v(ah), Equal.trans(Bool, Nat.is_eq(v(ah), 0n), U32.is_zero(ah), False{}, Equal.sym(Bool, U32.is_zero(ah), Nat.is_eq(v(ah), 0n), LW.zero_nat(ah)), hz1))
449      +h2 = pos_ne(v(bh), Equal.trans(Bool, Nat.is_eq(v(bh), 0n), U32.is_zero(bh), False{}, Equal.sym(Bool, U32.is_zero(bh), Nat.is_eq(v(bh), 0n), LW.zero_nat(bh)), hz2))
450      +hb = both_hi(32n, v(al), v(ah), v(bl), v(bh), h1, h2)
451      Equal.sym(Bool, Bool.not(C.fits(64n, Nat.mul(val(al, ah), val(bl, bh)))), True{}, Equal.cong(Bool, Bool, t => Bool.not(t), C.fits(64n, Nat.mul(val(al, ah), val(bl, bh))), False{}, hb))
452    case True{} _:
453      +eah = N.eq_from_is_eq(v(ah), 0n, Equal.trans(Bool, Nat.is_eq(v(ah), 0n), U32.is_zero(ah), True{}, Equal.sym(Bool, U32.is_zero(ah), Nat.is_eq(v(ah), 0n), LW.zero_nat(ah)), hz1))
454      +eh = L.subst(Nat, z => {Nat.mul(z, v(bh)) == 0n : Nat}, 0n, v(ah), Equal.sym(Nat, v(ah), 0n, eah), {==})
455      +hT = L.subst(Nat, z => {C.fits(64n, Nat.add(Nat.mul(z, v(bl)), Nat.mul(v(al), v(bh)))) == True{} : Bool}, 0n, v(ah), Equal.sym(Nat, v(ah), 0n, eah), prod_fits(32n, v(al), v(bh), vb(al), vb(bh)))
456      mo_core(al, ah, bl, bh, eh, hT)
457    case False{} True{}:
458      +ebh = N.eq_from_is_eq(v(bh), 0n, Equal.trans(Bool, Nat.is_eq(v(bh), 0n), U32.is_zero(bh), True{}, Equal.sym(Bool, U32.is_zero(bh), Nat.is_eq(v(bh), 0n), LW.zero_nat(bh)), hz2))
459      +eh = L.subst(Nat, z => {Nat.mul(v(ah), z) == 0n : Nat}, 0n, v(bh), Equal.sym(Nat, v(bh), 0n, ebh), NA.mul_zero(v(ah)))
460      +e0 = Equal.trans(Nat, Nat.add(Nat.mul(v(ah), v(bl)), Nat.mul(v(al), 0n)), Nat.add(Nat.mul(v(ah), v(bl)), 0n), Nat.mul(v(ah), v(bl)), Equal.cong(Nat, Nat, t => Nat.add(Nat.mul(v(ah), v(bl)), t), Nat.mul(v(al), 0n), 0n, NA.mul_zero(v(al))), N.add_zero(Nat.mul(v(ah), v(bl))))
461      +hT0 = L.subst(Nat, z => {C.fits(64n, z) == True{} : Bool}, Nat.mul(v(ah), v(bl)), Nat.add(Nat.mul(v(ah), v(bl)), Nat.mul(v(al), 0n)), Equal.sym(Nat, Nat.add(Nat.mul(v(ah), v(bl)), Nat.mul(v(al), 0n)), Nat.mul(v(ah), v(bl)), e0), prod_fits(32n, v(ah), v(bl), vb(ah), vb(bl)))
462      +hT = L.subst(Nat, z => {C.fits(64n, Nat.add(Nat.mul(v(ah), v(bl)), Nat.mul(v(al), z))) == True{} : Bool}, 0n, v(bh), Equal.sym(Nat, v(bh), 0n, ebh), hT0)
463      mo_core(al, ah, bl, bh, eh, hT)