def gval

bend-collections-laws-crypto@1.0.0.0 · proofs/math/u64/u64div.bend:192

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as U
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/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend as DQ
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/lib/arith.bend as AR
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32div.bend as UD
import bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64.bend as P

192def gval(+one: Nat, +h1: {one == 1n : Nat}, +lo: U32, +hi: U32, +d: U32, +c20: U32, +c12: U32, +c8: U32, +m12: U32, +m8: U32, +hd0: {U32.is_zero(d) == False{} : Bool}, +hle: {U32.is_le(d, c20) == True{} : Bool}, +p20: {c20 == U32{WD.pw(32n, 20n)} : U32}, +p12: {c12 == U32{WD.pw(32n, 12n)} : U32}, +p8: {c8 == U32{WD.pw(32n, 8n)} : U32}, +hm12: {m12 == U32{WD.mask(32n, 12n)} : U32}, +hm8: {m8 == U32{WD.mask(32n, 8n)} : U32}, +nz20: {U32.is_zero(c20) == False{} : Bool}, +nz8: {U32.is_zero(c8) == False{} : Bool}) -> {P.val(gdiv(U.U64{lo, hi}, d, c20, c12, c8, m12, m8)) == Nat.div(P.val(U.U64{lo, hi}), UD.v(d)) : Nat}:
193  +kk = WD.sc(32n, one)
194  +mm = WD.sc(20n, one)
195  +pp = WD.sc(12n, one)
196  +h20 = pow32(20n, {==}, one, h1, c20, p20)
197  +h12 = pow32(12n, {==}, one, h1, c12, p12)
198  +h8 = pow32(8n, {==}, one, h1, c8, p8)
199  +dn = UD.v(d)
200  +hdm = L.subst(Nat, z => {Nat.is_le(dn, z) == True{} : Bool}, UD.v(c20), mm, h20, le32(d, c20, hle))
201  +hk12 = AR.sc_le(12n, dn, mm, hdm)
202  +hk8 = N.le_trans(WD.sc(8n, dn), WD.sc(8n, mm), WD.sc(8n, WD.sc(4n, mm)), AR.sc_le(8n, dn, mm, hdm), AR.sc_le(8n, mm, WD.sc(4n, mm), AR.le_sc(4n, mm)))
203  # the high limb
204  +qh = UD.v(U32.div(hi, d))
205  +rh = UD.v(U32.mod(hi, d))
206  +eh = dm_e(hi, d, hd0)
207  +lh = dm_l(hi, d, hd0)
208  # the low limb's digits
209  +l1u = U32.div(lo, c20)
210  +l2u = U32.and(U32.div(lo, c8), m12)
211  +l3u = U32.and(lo, m8)
212  +l1 = UD.v(l1u)
213  +l2 = UD.v(l2u)
214  +l3 = UD.v(l3u)
215  +hl1 = lo_l1(one, h1, lo, c20, h20, nz20)
216  +hl2 = and32_lt(12n, one, h1, U32.div(lo, c8), m12, hm12)
217  +hl3 = and32_lt(8n, one, h1, lo, m8, hm8)
218  +hlw = lo_eq(one, h1, lo, c20, c8, m12, m8, h20, h8, hm12, hm8, nz20, nz8)
219  # t1
220  +t1 = U32.add(U32.mul(U32.mod(hi, d), c12), l1u)
221  +vt1 = tval(one, h1, 12n, U32.mod(hi, d), c12, l1u, dn, h12, hl1, lh, hk12)
222  +q1 = UD.v(U32.div(t1, d))
223  +r1 = UD.v(U32.mod(t1, d))
224  +lr1 = dm_l(t1, d, hd0)
225  +f1 = Equal.trans(Nat, Nat.add(WD.sc(12n, rh), l1), UD.v(t1), Nat.add(Nat.mul(q1, dn), r1), Equal.sym(Nat, UD.v(t1), Nat.add(WD.sc(12n, rh), l1), vt1), Equal.sym(Nat, Nat.add(Nat.mul(q1, dn), r1), UD.v(t1), dm_e(t1, d, hd0)))
226  +hq1 = AR.quot_lt(12n, one, h1, q1, dn, r1, lt_eq(Nat.add(WD.sc(12n, rh), l1), Nat.add(Nat.mul(q1, dn), r1), WD.sc(12n, dn), f1, AR.digit_lt(12n, one, h1, l1, rh, dn, hl1, lh)))
227  # t2
228  +t2 = U32.add(U32.mul(U32.mod(t1, d), c12), l2u)
229  +vt2 = tval(one, h1, 12n, U32.mod(t1, d), c12, l2u, dn, h12, hl2, lr1, hk12)
230  +q2 = UD.v(U32.div(t2, d))
231  +r2 = UD.v(U32.mod(t2, d))
232  +lr2 = dm_l(t2, d, hd0)
233  +f2 = Equal.trans(Nat, Nat.add(WD.sc(12n, r1), l2), UD.v(t2), Nat.add(Nat.mul(q2, dn), r2), Equal.sym(Nat, UD.v(t2), Nat.add(WD.sc(12n, r1), l2), vt2), Equal.sym(Nat, Nat.add(Nat.mul(q2, dn), r2), UD.v(t2), dm_e(t2, d, hd0)))
234  +hq2 = AR.quot_lt(12n, one, h1, q2, dn, r2, lt_eq(Nat.add(WD.sc(12n, r1), l2), Nat.add(Nat.mul(q2, dn), r2), WD.sc(12n, dn), f2, AR.digit_lt(12n, one, h1, l2, r1, dn, hl2, lr1)))
235  # t3
236  +t3 = U32.add(U32.mul(U32.mod(t2, d), c8), l3u)
237  +vt3 = tval(one, h1, 8n, U32.mod(t2, d), c8, l3u, dn, h8, hl3, lr2, hk8)
238  +q3 = UD.v(U32.div(t3, d))
239  +r3 = UD.v(U32.mod(t3, d))
240  +lr3 = dm_l(t3, d, hd0)
241  +f3 = Equal.trans(Nat, Nat.add(WD.sc(8n, r2), l3), UD.v(t3), Nat.add(Nat.mul(q3, dn), r3), Equal.sym(Nat, UD.v(t3), Nat.add(WD.sc(8n, r2), l3), vt3), Equal.sym(Nat, Nat.add(Nat.mul(q3, dn), r3), UD.v(t3), dm_e(t3, d, hd0)))
242  +hq3 = AR.quot_lt(8n, one, h1, q3, dn, r3, lt_eq(Nat.add(WD.sc(8n, r2), l3), Nat.add(Nat.mul(q3, dn), r3), WD.sc(8n, dn), f3, AR.digit_lt(8n, one, h1, l3, r2, dn, hl3, lr2)))
243  # the quotient's low limb
244  +a1 = U32.mul(U32.div(t1, d), c20)
245  +a2 = U32.mul(U32.div(t2, d), c8)
246  +a12 = U32.add(a1, a2)
247  +lo2 = U32.add(a12, U32.div(t3, d))
248  +hi2 = U32.div(hi, d)
249  +va1 = mulp32(one, h1, 20n, U32.div(t1, d), c20, h20, AR.sc_lt(20n, q1, pp, hq1))
250  +hq2m = AR.sc_lt(8n, q2, pp, hq2)
251  +va2 = mulp32(one, h1, 8n, U32.div(t2, d), c8, h8, N.lt_le_trans(WD.sc(8n, q2), mm, kk, hq2m, AR.le_sc(12n, mm)))
252  +va12 = addv32(one, h1, a1, a2, WD.sc(20n, q1), WD.sc(8n, q2), va1, va2, AR.digit_lt(20n, one, h1, WD.sc(8n, q2), q1, pp, hq2m, hq1))
253  +hx = AR.digit_lt(8n, one, h1, q3, q2, pp, hq3, hq2)
254  +hb = AR.digit_lt(20n, one, h1, Nat.add(WD.sc(8n, q2), q3), q1, pp, hx, hq1)
255  +hb2 = lt_eq(Nat.add(WD.sc(20n, q1), Nat.add(WD.sc(8n, q2), q3)), Nat.add(Nat.add(WD.sc(20n, q1), WD.sc(8n, q2)), q3), kk, Equal.sym(Nat, Nat.add(Nat.add(WD.sc(20n, q1), WD.sc(8n, q2)), q3), Nat.add(WD.sc(20n, q1), Nat.add(WD.sc(8n, q2), q3)), N.add_assoc(WD.sc(20n, q1), WD.sc(8n, q2), q3)), hb)
256  +vlo2 = addv32(one, h1, a12, U32.div(t3, d), Nat.add(WD.sc(20n, q1), WD.sc(8n, q2)), q3, va12, {==}, hb2)
257  # the division identity, three digits at a time
258  +x1 = AR.step(12n, qh, rh, dn, l1, q1, r1, UD.v(hi), Equal.sym(Nat, Nat.add(Nat.mul(qh, dn), rh), UD.v(hi), eh), f1)
259  +x2 = AR.step(12n, Nat.add(WD.sc(12n, qh), q1), r1, dn, l2, q2, r2, Nat.add(WD.sc(12n, UD.v(hi)), l1), x1, f2)
260  +x3 = AR.step(8n, Nat.add(WD.sc(12n, Nat.add(WD.sc(12n, qh), q1)), q2), r2, dn, l3, q3, r3, Nat.add(WD.sc(12n, Nat.add(WD.sc(12n, UD.v(hi)), l1)), l2), x2, f3)
261  +ea = expand(UD.v(hi), l1, l2, l3)
262  +eq = expand(qh, q1, q2, q3)
263  +qx = Nat.add(WD.sc(8n, Nat.add(WD.sc(12n, Nat.add(WD.sc(12n, qh), q1)), q2)), q3)
264  +qv = Nat.add(UD.v(lo2), WD.sc(32n, qh))
265  +eqv = Equal.trans(Nat, qx, Nat.add(Nat.add(Nat.add(WD.sc(20n, q1), WD.sc(8n, q2)), q3), WD.sc(32n, qh)), qv, eq, Equal.cong(Nat, Nat, z => Nat.add(z, WD.sc(32n, qh)), Nat.add(Nat.add(WD.sc(20n, q1), WD.sc(8n, q2)), q3), UD.v(lo2), Equal.sym(Nat, UD.v(lo2), Nat.add(Nat.add(WD.sc(20n, q1), WD.sc(8n, q2)), q3), vlo2)))
266  +lhs3 = Nat.add(WD.sc(8n, Nat.add(WD.sc(12n, Nat.add(WD.sc(12n, UD.v(hi)), l1)), l2)), l3)
267  +ca = Equal.trans(Nat, P.val(U.U64{lo, hi}), Nat.add(UD.v(lo), WD.sc(32n, UD.v(hi))), lhs3, P.val_pack(lo, hi),
268    Equal.trans(Nat, Nat.add(UD.v(lo), WD.sc(32n, UD.v(hi))), Nat.add(Nat.add(Nat.add(WD.sc(20n, l1), WD.sc(8n, l2)), l3), WD.sc(32n, UD.v(hi))), lhs3, Equal.cong(Nat, Nat, z => Nat.add(z, WD.sc(32n, UD.v(hi))), UD.v(lo), Nat.add(Nat.add(WD.sc(20n, l1), WD.sc(8n, l2)), l3), hlw), Equal.sym(Nat, lhs3, Nat.add(Nat.add(Nat.add(WD.sc(20n, l1), WD.sc(8n, l2)), l3), WD.sc(32n, UD.v(hi))), ea)))
269  +c = Equal.trans(Nat, P.val(U.U64{lo, hi}), lhs3, Nat.add(Nat.mul(qv, dn), r3), ca, Equal.trans(Nat, lhs3, Nat.add(Nat.mul(qx, dn), r3), Nat.add(Nat.mul(qv, dn), r3), x3, Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(z, dn), r3), qx, qv, eqv)))
270  Equal.trans(Nat, P.val(gdiv(U.U64{lo, hi}, d, c20, c12, c8, m12, m8)), qv, Nat.div(P.val(U.U64{lo, hi}), dn), P.val_pack(lo2, hi2),
271    Equal.sym(Nat, Nat.div(P.val(U.U64{lo, hi}), dn), qv, Equal.trans(Nat, Nat.div(P.val(U.U64{lo, hi}), dn), Nat.div(Nat.add(Nat.mul(qv, dn), r3), dn), qv, Equal.cong(Nat, Nat, z => Nat.div(z, dn), P.val(U.U64{lo, hi}), Nat.add(Nat.mul(qv, dn), r3), c), DQ.identify(qv, dn, r3, lr3))))