def ov96

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64dm.bend:84

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/w64.bend as SW
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/u32.bend as U
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/u32laws.bend as LW

84# the 96-bit comparison of over96
85def ov96(+xl: WU.U64, +xh: U32, +pl: WU.U64, +ph: U32) -> {X.over96(xl, xh, (pl, ph)) == Nat.is_lt(Nat.add(SW.value(xl), C.shift(64n, v(xh))), Nat.add(SW.value(pl), C.shift(64n, v(ph)))) : Bool}:
86  +e1 = Equal.cong(Bool, Bool, z => Bool.or(z, Bool.and(U32.is_eq(xh, ph), X.lt(xl, pl))), U32.is_lt(xh, ph), Nat.is_lt(v(xh), v(ph)), U.is_lt_nat(xh, ph))
87  +e2 = Equal.cong(Bool, Bool, z => Bool.or(Nat.is_lt(v(xh), v(ph)), Bool.and(z, X.lt(xl, pl))), U32.is_eq(xh, ph), Nat.is_eq(v(xh), v(ph)), LW.eq_nat(xh, ph))
88  +e3 = Equal.cong(Bool, Bool, z => Bool.or(Nat.is_lt(v(xh), v(ph)), Bool.and(Nat.is_eq(v(xh), v(ph)), z)), X.lt(xl, pl), Nat.is_lt(SW.value(xl), SW.value(pl)), WA.lt_value(xl, pl))
89  Equal.trans(Bool, X.over96(xl, xh, (pl, ph)), Bool.or(Nat.is_lt(v(xh), v(ph)), Bool.and(U32.is_eq(xh, ph), X.lt(xl, pl))), Nat.is_lt(Nat.add(SW.value(xl), C.shift(64n, v(xh))), Nat.add(SW.value(pl), C.shift(64n, v(ph)))), e1, Equal.trans(Bool, Bool.or(Nat.is_lt(v(xh), v(ph)), Bool.and(U32.is_eq(xh, ph), X.lt(xl, pl))), Bool.or(Nat.is_lt(v(xh), v(ph)), Bool.and(Nat.is_eq(v(xh), v(ph)), X.lt(xl, pl))), Nat.is_lt(Nat.add(SW.value(xl), C.shift(64n, v(xh))), Nat.add(SW.value(pl), C.shift(64n, v(ph)))), e2, Equal.trans(Bool, Bool.or(Nat.is_lt(v(xh), v(ph)), Bool.and(Nat.is_eq(v(xh), v(ph)), X.lt(xl, pl))), Bool.or(Nat.is_lt(v(xh), v(ph)), Bool.and(Nat.is_eq(v(xh), v(ph)), Nat.is_lt(SW.value(xl), SW.value(pl)))), Nat.is_lt(Nat.add(SW.value(xl), C.shift(64n, v(xh))), Nat.add(SW.value(pl), C.shift(64n, v(ph)))), e3, WW.lt_limbs(64n, SW.value(xl), v(xh), SW.value(pl), v(ph), fit64(xl), fit64(pl)))))