def ovq

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

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

94# q b > x
95def ovq(+one: Nat, +h1: {one == 1n : Nat}, +xl: WU.U64, +xh: U32, +b: WU.U64, +q: U32) -> {X.over96(xl, xh, X.mul_32_64(q, b)) == Nat.is_lt(X96(xl, xh), Nat.mul(v(q), SW.value(b))) : Bool}:
96  match b:
97    case WU.U64{+bl, +bh}:
98      Equal.trans(Bool, X.over96(xl, xh, (X.fst_q(X.mul_32_64(q, WU.U64{bl, bh})), X.snd_r(X.mul_32_64(q, WU.U64{bl, bh})))), Nat.is_lt(X96(xl, xh), Nat.add(SW.value(X.fst_q(X.mul_32_64(q, WU.U64{bl, bh}))), C.shift(64n, v(X.snd_r(X.mul_32_64(q, WU.U64{bl, bh})))))), Nat.is_lt(X96(xl, xh), Nat.mul(v(q), SW.value(WU.U64{bl, bh}))), ov96(xl, xh, X.fst_q(X.mul_32_64(q, WU.U64{bl, bh})), X.snd_r(X.mul_32_64(q, WU.U64{bl, bh}))), Equal.cong(Nat, Bool, z => Nat.is_lt(X96(xl, xh), z), Nat.add(SW.value(X.fst_q(X.mul_32_64(q, WU.U64{bl, bh}))), C.shift(64n, v(X.snd_r(X.mul_32_64(q, WU.U64{bl, bh}))))), Nat.mul(v(q), SW.value(WU.U64{bl, bh})), mul3264(one, h1, q, bl, bh)))