U64div.lo_eq: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend as U64div Lines 142-174 of bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend&start_line=142&end_line=174 import Base 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/u32alg.bend as A 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 def lo_eq(+one: Nat, +h1: {one == 1n : Nat}, +lo: U32, +c20: U32, +c8: U32, +m12: U32, +m8: U32, +h20: {UD.v(c20) == WD.sc(20n, one) : Nat}, +h8: {UD.v(c8) == WD.sc(8n, one) : Nat}, +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}) -> {UD.v(lo) == Nat.add(Nat.add(WD.sc(20n, UD.v(U32.div(lo, c20))), WD.sc(8n, UD.v(U32.and(U32.div(lo, c8), m12)))), UD.v(U32.and(lo, m8))) : Nat}: +ln = UD.v(lo) +l1 = UD.v(U32.div(lo, c20)) +r1 = UD.v(U32.mod(lo, c20)) +w8 = UD.v(U32.div(lo, c8)) +r8 = UD.v(U32.mod(lo, c8)) +l2 = UD.v(U32.and(U32.div(lo, c8), m12)) +l3 = UD.v(U32.and(lo, m8)) +y2 = hp32(12n, U32.div(lo, c8)) +y3 = hp32(8n, lo) +e20 = Equal.trans(Nat, Nat.add(WD.sc(20n, l1), r1), Nat.add(Nat.mul(l1, UD.v(c20)), r1), ln, Equal.cong(Nat, Nat, z => Nat.add(z, r1), WD.sc(20n, l1), Nat.mul(l1, UD.v(c20)), Equal.sym(Nat, Nat.mul(l1, UD.v(c20)), WD.sc(20n, l1), mul_pow(one, h1, 20n, l1, UD.v(c20), h20))), dm_e(lo, c20, nz20)) +l20 = L.subst(Nat, z => {Nat.is_lt(r1, z) == True{} : Bool}, UD.v(c20), WD.sc(20n, one), h20, dm_l(lo, c20, nz20)) +e8 = Equal.trans(Nat, Nat.add(WD.sc(8n, w8), r8), Nat.add(Nat.mul(w8, UD.v(c8)), r8), ln, Equal.cong(Nat, Nat, z => Nat.add(z, r8), WD.sc(8n, w8), Nat.mul(w8, UD.v(c8)), Equal.sym(Nat, Nat.mul(w8, UD.v(c8)), WD.sc(8n, w8), mul_pow(one, h1, 8n, w8, UD.v(c8), h8))), dm_e(lo, c8, nz8)) +l8 = L.subst(Nat, z => {Nat.is_lt(r8, z) == True{} : Bool}, UD.v(c8), WD.sc(8n, one), h8, dm_l(lo, c8, nz8)) +s3 = and32(8n, lo, m8, hm8) +b3 = and32_lt(8n, one, h1, lo, m8, hm8) +er8 = WD.uniq(8n, one, h1, r8, l3, w8, y3, Equal.trans(Nat, Nat.add(r8, WD.sc(8n, w8)), Nat.add(WD.sc(8n, w8), r8), Nat.add(l3, WD.sc(8n, y3)), N.add_comm(r8, WD.sc(8n, w8)), Equal.trans(Nat, Nat.add(WD.sc(8n, w8), r8), ln, Nat.add(l3, WD.sc(8n, y3)), e8, s3)), l8, b3) +s2 = and32(12n, U32.div(lo, c8), m12, hm12) +b2 = and32_lt(12n, one, h1, U32.div(lo, c8), m12, hm12) # ln == (2^8 l2 + 2^20 y2) + l3 +elw = Equal.trans(Nat, ln, Nat.add(WD.sc(8n, w8), l3), Nat.add(Nat.add(WD.sc(8n, l2), WD.sc(20n, y2)), l3), Equal.trans(Nat, ln, Nat.add(WD.sc(8n, w8), r8), Nat.add(WD.sc(8n, w8), l3), Equal.sym(Nat, Nat.add(WD.sc(8n, w8), r8), ln, e8), Equal.cong(Nat, Nat, z => Nat.add(WD.sc(8n, w8), z), r8, l3, er8)), Equal.cong(Nat, Nat, z => Nat.add(z, l3), WD.sc(8n, w8), Nat.add(WD.sc(8n, l2), WD.sc(20n, y2)), Equal.trans(Nat, WD.sc(8n, w8), WD.sc(8n, Nat.add(l2, WD.sc(12n, y2))), Nat.add(WD.sc(8n, l2), WD.sc(20n, y2)), Equal.cong(Nat, Nat, z => WD.sc(8n, z), w8, Nat.add(l2, WD.sc(12n, y2)), s2), Equal.sym(Nat, Nat.add(WD.sc(8n, l2), WD.sc(8n, WD.sc(12n, y2))), WD.sc(8n, Nat.add(l2, WD.sc(12n, y2))), A.sc_add(8n, l2, WD.sc(12n, y2)))))) +hb2 = AR.digit_lt(8n, one, h1, l3, l2, WD.sc(12n, one), b3, b2) +er1 = WD.uniq(20n, one, h1, r1, Nat.add(WD.sc(8n, l2), l3), l1, y2, Equal.trans(Nat, Nat.add(r1, WD.sc(20n, l1)), ln, Nat.add(Nat.add(WD.sc(8n, l2), l3), WD.sc(20n, y2)), Equal.trans(Nat, Nat.add(r1, WD.sc(20n, l1)), Nat.add(WD.sc(20n, l1), r1), ln, N.add_comm(r1, WD.sc(20n, l1)), e20), Equal.trans(Nat, ln, Nat.add(Nat.add(WD.sc(8n, l2), WD.sc(20n, y2)), l3), Nat.add(Nat.add(WD.sc(8n, l2), l3), WD.sc(20n, y2)), elw, A.add_rot(WD.sc(8n, l2), WD.sc(20n, y2), l3))), l20, hb2) Equal.trans(Nat, ln, Nat.add(WD.sc(20n, l1), Nat.add(WD.sc(8n, l2), l3)), Nat.add(Nat.add(WD.sc(20n, l1), WD.sc(8n, l2)), l3), Equal.trans(Nat, ln, Nat.add(WD.sc(20n, l1), r1), Nat.add(WD.sc(20n, l1), Nat.add(WD.sc(8n, l2), l3)), Equal.sym(Nat, Nat.add(WD.sc(20n, l1), r1), ln, e20), Equal.cong(Nat, Nat, z => Nat.add(WD.sc(20n, l1), z), r1, Nat.add(WD.sc(8n, l2), l3), er1)), Equal.sym(Nat, Nat.add(Nat.add(WD.sc(20n, l1), WD.sc(8n, l2)), l3), Nat.add(WD.sc(20n, l1), Nat.add(WD.sc(8n, l2), l3)), N.add_assoc(WD.sc(20n, l1), WD.sc(8n, l2), l3))) Uses (29): 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.is_lt 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.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_zero https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mod https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend&name=digit_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=subst https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=add_assoc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=add_comm https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend&name=add_rot https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend&name=sc_add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32div.bend&name=v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=mask https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=sc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=uniq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend&name=and32 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend&name=and32_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend&name=dm_e https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend&name=dm_l https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend&name=hp32 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend&name=mul_pow