def qup2

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

import Base
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/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/u32.bend as U

122# down keeps x < (q + 1) b: a step is taken only when x < q b
123def qup2(+fu: Nat, +one: Nat, +h1: {one == 1n : Nat}, +xl: WU.U64, +xh: U32, +b: WU.U64, +q: U32, +cb: Bool, +nq: Nat, +hf: {Nat.is_lt(v(q), fu) == True{} : Bool}, +hc: {X.over96(xl, xh, X.mul_32_64(q, b)) == cb : Bool}, +hnq: {v(q) == nq : Nat}, +hu: {Nat.is_lt(X96(xl, xh), Nat.mul(1n+v(q), SW.value(b))) == True{} : Bool}) -> {Nat.is_lt(X96(xl, xh), Nat.mul(1n+v(X.q_fix(fu, xl, xh, b, q, cb)), SW.value(b))) == True{} : Bool}:
124  match fu cb nq:
125    case 0n _ _:
126      Empty.absurd({Nat.is_lt(X96(xl, xh), Nat.mul(1n+v(X.q_fix(0n, xl, xh, b, q, cb)), SW.value(b))) == True{} : Bool}, N.lt_zero_absurd(v(q), hf))
127    case 1n+g False{} _:
128      hu
129    case 1n+g True{} 0n:
130      +h0 = Equal.trans(Bool, Nat.is_lt(X96(xl, xh), QB(b, q)), X.over96(xl, xh, X.mul_32_64(q, b)), True{}, Equal.sym(Bool, X.over96(xl, xh, X.mul_32_64(q, b)), Nat.is_lt(X96(xl, xh), QB(b, q)), ovq(one, h1, xl, xh, b, q)), hc)
131      +h1b = L.subst(Nat, z => {Nat.is_lt(X96(xl, xh), Nat.mul(z, SW.value(b))) == True{} : Bool}, v(q), 0n, hnq, h0)
132      Empty.absurd({Nat.is_lt(X96(xl, xh), Nat.mul(1n+v(X.q_fix(1n+g, xl, xh, b, q, True{})), SW.value(b))) == True{} : Bool}, N.lt_zero_absurd(X96(xl, xh), h1b))
133    case 1n+ +g True{} 1n+ +qp:
134      +q1 = U32.sub(q, 1)
135      +e1 = Equal.trans(Nat, v(q1), Nat.sub(v(q), 1n), qp, U.sub_nat(q, 1, L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, 1n+qp, v(q), Equal.sym(Nat, v(q), 1n+qp, hnq), N.zero_le(qp))), Equal.trans(Nat, Nat.sub(v(q), 1n), Nat.sub(1n+qp, 1n), qp, Equal.cong(Nat, Nat, t => Nat.sub(t, 1n), v(q), 1n+qp, hnq), N.sub_zero(qp)))
136      +hf1 = L.subst(Nat, z => {Nat.is_lt(z, g) == True{} : Bool}, qp, v(q1), Equal.sym(Nat, v(q1), qp, e1), L.subst(Nat, z => {Nat.is_lt(z, 1n+g) == True{} : Bool}, v(q), 1n+qp, hnq, hf))
137      +h0 = Equal.trans(Bool, Nat.is_lt(X96(xl, xh), QB(b, q)), X.over96(xl, xh, X.mul_32_64(q, b)), True{}, Equal.sym(Bool, X.over96(xl, xh, X.mul_32_64(q, b)), Nat.is_lt(X96(xl, xh), QB(b, q)), ovq(one, h1, xl, xh, b, q)), hc)
138      +h2 = L.subst(Nat, z => {Nat.is_lt(X96(xl, xh), Nat.mul(z, SW.value(b))) == True{} : Bool}, v(q), 1n+qp, hnq, h0)
139      +hu1 = L.subst(Nat, z => {Nat.is_lt(X96(xl, xh), Nat.mul(1n+z, SW.value(b))) == True{} : Bool}, qp, v(q1), Equal.sym(Nat, v(q1), qp, e1), h2)
140      qup2(g, one, h1, xl, xh, b, q1, X.over96(xl, xh, X.mul_32_64(q1, b)), qp, hf1, {==}, e1, hu1)