def lo_eq

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

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

142def 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}:
143  +ln = UD.v(lo)
144  +l1 = UD.v(U32.div(lo, c20))
145  +r1 = UD.v(U32.mod(lo, c20))
146  +w8 = UD.v(U32.div(lo, c8))
147  +r8 = UD.v(U32.mod(lo, c8))
148  +l2 = UD.v(U32.and(U32.div(lo, c8), m12))
149  +l3 = UD.v(U32.and(lo, m8))
150  +y2 = hp32(12n, U32.div(lo, c8))
151  +y3 = hp32(8n, lo)
152  +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))
153  +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))
154  +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))
155  +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))
156  +s3 = and32(8n, lo, m8, hm8)
157  +b3 = and32_lt(8n, one, h1, lo, m8, hm8)
158  +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)
159  +s2 = and32(12n, U32.div(lo, c8), m12, hm12)
160  +b2 = and32_lt(12n, one, h1, U32.div(lo, c8), m12, hm12)
161  # ln == (2^8 l2 + 2^20 y2) + l3
162  +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),
163    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)),
164    Equal.cong(Nat, Nat, z => Nat.add(z, l3), WD.sc(8n, w8), Nat.add(WD.sc(8n, l2), WD.sc(20n, y2)),
165      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))))))
166  +hb2 = AR.digit_lt(8n, one, h1, l3, l2, WD.sc(12n, one), b3, b2)
167  +er1 = WD.uniq(20n, one, h1, r1, Nat.add(WD.sc(8n, l2), l3), l1, y2,
168    Equal.trans(Nat, Nat.add(r1, WD.sc(20n, l1)), ln, Nat.add(Nat.add(WD.sc(8n, l2), l3), WD.sc(20n, y2)),
169      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),
170      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))),
171    l20, hb2)
172  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),
173    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)),
174    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)))