def lo_dig

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64div.bend:32

import Base
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/logic.bend as L
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/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend as PD

32def lo_dig(+one: Nat, +h1: {one == 1n : Nat}, +lo: U32, +c16: U32, +m16: U32, +h16: {UD.v(c16) == WD.sc(16n, one) : Nat}, +hm16: {m16 == U32{WD.mask(32n, 16n)} : U32}, +nz16: {U32.is_zero(c16) == False{} : Bool}) -> {UD.v(lo) == Nat.add(WD.sc(16n, UD.v(U32.div(lo, c16))), UD.v(U32.and(lo, m16))) : Nat}:
33  +ln = UD.v(lo)
34  +l1 = UD.v(U32.div(lo, c16))
35  +r1 = UD.v(U32.mod(lo, c16))
36  +l2 = UD.v(U32.and(lo, m16))
37  +y = PD.hp32(16n, lo)
38  +e16 = Equal.trans(Nat, Nat.add(WD.sc(16n, l1), r1), Nat.add(Nat.mul(l1, UD.v(c16)), r1), ln, Equal.cong(Nat, Nat, z => Nat.add(z, r1), WD.sc(16n, l1), Nat.mul(l1, UD.v(c16)), Equal.sym(Nat, Nat.mul(l1, UD.v(c16)), WD.sc(16n, l1), PD.mul_pow(one, h1, 16n, l1, UD.v(c16), h16))), PD.dm_e(lo, c16, nz16))
39  +l16 = L.subst(Nat, z => {Nat.is_lt(r1, z) == True{} : Bool}, UD.v(c16), WD.sc(16n, one), h16, PD.dm_l(lo, c16, nz16))
40  +s2 = PD.and32(16n, lo, m16, hm16)
41  +b2 = PD.and32_lt(16n, one, h1, lo, m16, hm16)
42  +er = WD.uniq(16n, one, h1, r1, l2, l1, y, Equal.trans(Nat, Nat.add(r1, WD.sc(16n, l1)), Nat.add(WD.sc(16n, l1), r1), Nat.add(l2, WD.sc(16n, y)), N.add_comm(r1, WD.sc(16n, l1)), Equal.trans(Nat, Nat.add(WD.sc(16n, l1), r1), ln, Nat.add(l2, WD.sc(16n, y)), e16, s2)), l16, b2)
43  Equal.trans(Nat, ln, Nat.add(WD.sc(16n, l1), r1), Nat.add(WD.sc(16n, l1), l2), Equal.sym(Nat, Nat.add(WD.sc(16n, l1), r1), ln, e16), Equal.cong(Nat, Nat, z => Nat.add(WD.sc(16n, l1), z), r1, l2, er))