U64div.gval: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend as U64div Lines 192-271 of bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend&start_line=192&end_line=271 import Base import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as U import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend as DQ import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as AR import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend as P def 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}: +kk = WD.sc(32n, one) +mm = WD.sc(20n, one) +pp = WD.sc(12n, one) +h20 = pow32(20n, {==}, one, h1, c20, p20) +h12 = pow32(12n, {==}, one, h1, c12, p12) +h8 = pow32(8n, {==}, one, h1, c8, p8) +dn = UD.v(d) +hdm = L.subst(Nat, z => {Nat.is_le(dn, z) == True{} : Bool}, UD.v(c20), mm, h20, le32(d, c20, hle)) +hk12 = AR.sc_le(12n, dn, mm, hdm) +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))) # the high limb +qh = UD.v(U32.div(hi, d)) +rh = UD.v(U32.mod(hi, d)) +eh = dm_e(hi, d, hd0) +lh = dm_l(hi, d, hd0) # the low limb's digits +l1u = U32.div(lo, c20) +l2u = U32.and(U32.div(lo, c8), m12) +l3u = U32.and(lo, m8) +l1 = UD.v(l1u) +l2 = UD.v(l2u) +l3 = UD.v(l3u) +hl1 = lo_l1(one, h1, lo, c20, h20, nz20) +hl2 = and32_lt(12n, one, h1, U32.div(lo, c8), m12, hm12) +hl3 = and32_lt(8n, one, h1, lo, m8, hm8) +hlw = lo_eq(one, h1, lo, c20, c8, m12, m8, h20, h8, hm12, hm8, nz20, nz8) # t1 +t1 = U32.add(U32.mul(U32.mod(hi, d), c12), l1u) +vt1 = tval(one, h1, 12n, U32.mod(hi, d), c12, l1u, dn, h12, hl1, lh, hk12) +q1 = UD.v(U32.div(t1, d)) +r1 = UD.v(U32.mod(t1, d)) +lr1 = dm_l(t1, d, hd0) +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))) +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))) # t2 +t2 = U32.add(U32.mul(U32.mod(t1, d), c12), l2u) +vt2 = tval(one, h1, 12n, U32.mod(t1, d), c12, l2u, dn, h12, hl2, lr1, hk12) +q2 = UD.v(U32.div(t2, d)) +r2 = UD.v(U32.mod(t2, d)) +lr2 = dm_l(t2, d, hd0) +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))) +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))) # t3 +t3 = U32.add(U32.mul(U32.mod(t2, d), c8), l3u) +vt3 = tval(one, h1, 8n, U32.mod(t2, d), c8, l3u, dn, h8, hl3, lr2, hk8) +q3 = UD.v(U32.div(t3, d)) +r3 = UD.v(U32.mod(t3, d)) +lr3 = dm_l(t3, d, hd0) +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))) +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))) # the quotient's low limb +a1 = U32.mul(U32.div(t1, d), c20) +a2 = U32.mul(U32.div(t2, d), c8) +a12 = U32.add(a1, a2) +lo2 = U32.add(a12, U32.div(t3, d)) +hi2 = U32.div(hi, d) +va1 = mulp32(one, h1, 20n, U32.div(t1, d), c20, h20, AR.sc_lt(20n, q1, pp, hq1)) +hq2m = AR.sc_lt(8n, q2, pp, hq2) +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))) +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)) +hx = AR.digit_lt(8n, one, h1, q3, q2, pp, hq3, hq2) +hb = AR.digit_lt(20n, one, h1, Nat.add(WD.sc(8n, q2), q3), q1, pp, hx, hq1) +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) +vlo2 = addv32(one, h1, a12, U32.div(t3, d), Nat.add(WD.sc(20n, q1), WD.sc(8n, q2)), q3, va12, {==}, hb2) # the division identity, three digits at a time +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) +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) +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) +ea = expand(UD.v(hi), l1, l2, l3) +eq = expand(qh, q1, q2, q3) +qx = Nat.add(WD.sc(8n, Nat.add(WD.sc(12n, Nat.add(WD.sc(12n, qh), q1)), q2)), q3) +qv = Nat.add(UD.v(lo2), WD.sc(32n, qh)) +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))) +lhs3 = Nat.add(WD.sc(8n, Nat.add(WD.sc(12n, Nat.add(WD.sc(12n, UD.v(hi)), l1)), l2)), l3) +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), 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))) +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))) 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), 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)))) Uses (48): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.and https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.div https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_zero https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mod https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mul https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=digit_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=le_sc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=quot_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=sc_le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=sc_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=step https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend&name=identify https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=subst https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_assoc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_trans https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_le_trans https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend&name=v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=mask https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=pw https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=sc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend&name=val https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend&name=val_pack https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend&name=addv32 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend&name=and32_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend&name=dm_e https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend&name=dm_l https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend&name=expand https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend&name=gdiv https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend&name=le32 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend&name=lo_eq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend&name=lo_l1 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend&name=lt_eq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend&name=mulp32 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend&name=pow32 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend&name=tval https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64