def wsd.step
bend-osdev-word64@0.1.1.0 · PROOF_text.bend:205
import bend-osdev-word64@0.1.1.0/PROOF_text.bend as PROOFText
import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
205def wsd.step(+rp: U32, +qp: U32, +c: U32, +hR: {Nat.is_lt(U32.to_nat(rp), 10n) == True{} : Bool}, +hC: {Nat.is_lt(U32.to_nat(c), U.U32Nat.dbl(16n, 1n)) == True{} : Bool}, +hQ: {Nat.is_lt(U32.to_nat(qp), U.U32Nat.dbl(16n, 1n)) == True{} : Bool}) -> {U32.to_nat(wsd.q(qp, rp, c)) == Nat.add(U.U32Nat.dbl(16n, U32.to_nat(qp)), U32.to_nat(wsd.d(rp, c))) : Nat} & {Nat.add(Nat.mul(U32.to_nat(wsd.d(rp, c)), 10n), U32.to_nat(wsd.m(rp, c))) == Nat.add(U.U32Nat.dbl(16n, U32.to_nat(rp)), U32.to_nat(c)) : Nat} & {Nat.is_lt(U32.to_nat(wsd.m(rp, c)), 10n) == True{} : Bool} & {Nat.is_lt(U32.to_nat(wsd.d(rp, c)), U.U32Nat.dbl(16n, 1n)) == True{} : Bool}:
206 +ev = wsd.fst(U32.to_nat(wsd.v(rp, c)), Nat.add(U.U32Nat.dbl(16n, U32.to_nat(rp)), U32.to_nat(c)), U32.to_nat(wsd.v(rp, c)), U.U32Nat.dbl(16n, 10n), wsd.k1(32n, 16n, U32.to_nat(rp), U32.to_nat(c), U32.to_nat(U32.mul(rp, 65536)), U32.to_nat(wsd.v(rp, c)), U.U32Nat.bit(U32.is_lt(wsd.v(rp, c), U32.mul(rp, 65536))), {==}, {==}, hR, hC, wsd.mul16(rp), UL.u32_add_wrap(U32.mul(rp, 65536), c)))
207 +vl = wsd.snd(U32.to_nat(wsd.v(rp, c)), Nat.add(U.U32Nat.dbl(16n, U32.to_nat(rp)), U32.to_nat(c)), U32.to_nat(wsd.v(rp, c)), U.U32Nat.dbl(16n, 10n), wsd.k1(32n, 16n, U32.to_nat(rp), U32.to_nat(c), U32.to_nat(U32.mul(rp, 65536)), U32.to_nat(wsd.v(rp, c)), U.U32Nat.bit(U32.is_lt(wsd.v(rp, c), U32.mul(rp, 65536))), {==}, {==}, hR, hC, wsd.mul16(rp), UL.u32_add_wrap(U32.mul(rp, 65536), c)))
208 +edm = Equal.trans(Nat, Nat.add(Nat.mul(U32.to_nat(wsd.d(rp, c)), 10n), U32.to_nat(wsd.m(rp, c))), Nat.add(Nat.mul(U32.to_nat(wsd.d(rp, c)), U32.to_nat(10)), U32.to_nat(wsd.m(rp, c))), U32.to_nat(wsd.v(rp, c)), {==}, UL.u32_divmod(wsd.v(rp, c), 10, {==}))
209 +mlt = Equal.trans(Bool, Nat.is_lt(U32.to_nat(wsd.m(rp, c)), 10n), Nat.is_lt(U32.to_nat(wsd.m(rp, c)), U32.to_nat(10)), True{}, {==}, UL.u32_mod_lt(wsd.v(rp, c), 10, {==}))
210 +dlt = wsd.k2(16n, U32.to_nat(wsd.v(rp, c)), U32.to_nat(wsd.d(rp, c)), U32.to_nat(wsd.m(rp, c)), edm, vl)
211 +eq = Equal.trans(Nat, U32.to_nat(wsd.q(qp, rp, c)), Nat.add(U32.to_nat(U32.shln(qp, 16n)), U32.to_nat(wsd.d(rp, c))), Nat.add(U.U32Nat.dbl(16n, U32.to_nat(qp)), U32.to_nat(wsd.d(rp, c))), UL.u32_or_split(U32.shln(qp, 16n), wsd.d(rp, c), 16n, U32.to_nat(qp), wsd.k3(32n, 16n, U32.to_nat(qp), U32.to_nat(U32.shln(qp, 16n)), {==}, hQ, UL.u32_shln_low(qp, 16n)), dlt), Equal.cong(Nat, Nat, zz => Nat.add(zz, U32.to_nat(wsd.d(rp, c))), U32.to_nat(U32.shln(qp, 16n)), U.U32Nat.dbl(16n, U32.to_nat(qp)), wsd.k3(32n, 16n, U32.to_nat(qp), U32.to_nat(U32.shln(qp, 16n)), {==}, hQ, UL.u32_shln_low(qp, 16n))))
212 (eq, Equal.trans(Nat, Nat.add(Nat.mul(U32.to_nat(wsd.d(rp, c)), 10n), U32.to_nat(wsd.m(rp, c))), U32.to_nat(wsd.v(rp, c)), Nat.add(U.U32Nat.dbl(16n, U32.to_nat(rp)), U32.to_nat(c)), edm, ev), mlt, dlt)