def wd.bs
bend-osdev-word64@0.1.1.0 · PROOF_div.bend:395
import bend-osdev-word64@0.1.1.0/PROOF_div.bend as PROOFDiv
import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-word64@0.1.1.0/word64.bend as W
395def wd.bs(+p: Nat, +x: Bool, +hi: Word(p), +b: W.W64, +q: W.W64, +r: W.W64, +hb: {Nat.is_lt(W.W64.to_nat(b), U.U32Nat.dbl(64n, 1n)) == True{} : Bool}, +hX: {Nat.is_lt(Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), U.U32Nat.dbl(64n, 1n)) == True{} : Bool}, ih: {Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))))) == Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi)) : Nat} & {Nat.is_lt(W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)) == True{} : Bool}) -> {Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(1n+p, WCon{x, hi}, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(1n+p, WCon{x, hi}, b, (q, r))))) == Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})) : Nat} & {Nat.is_lt(W.W64.to_nat(W.W64.snd(W.W64.div.bits(1n+p, WCon{x, hi}, b, (q, r)))), W.W64.to_nat(b)) == True{} : Bool}:
396 (+e, +l) = ih
397 %Equal.sym(W.W64 & W.W64, W.W64.div.bits(p, hi, b, (q, r)), (W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))), wd.eta(W.W64.div.bits(p, hi, b, (q, r)))) : {Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.step(x, b, _))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.step(x, b, _)))) == Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})) : Nat} & {Nat.is_lt(W.W64.to_nat(W.W64.snd(W.W64.div.step(x, b, _))), W.W64.to_nat(b)) == True{} : Bool}
398 (Equal.trans(Nat, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.step(x, b, (W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))))))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.step(x, b, (W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))))), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), wd.p1(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.step(x, b, (W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))))))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.step(x, b, (W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))))), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), W.W64.to_nat(W.W64.snd(W.W64.div.step(x, b, (W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))))))), W.W64.to_nat(b), wd.st(x, b, W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))), l, hb, Equal.trans(Bool, Nat.is_lt(Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), U.U32Nat.dbl(64n, 1n)), Nat.is_lt(Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), U.U32Nat.dbl(64n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(64n, 1n)), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), Equal.sym(Nat, Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), Equal.trans(Nat, Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi))), U.U32Nat.bit(x)), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), Equal.cong(Nat, Nat, zz => Nat.add(Nat.double(zz), U.U32Nat.bit(x)), Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))))), Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi)), e), Equal.trans(Nat, Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi))), U.U32Nat.bit(x)), Nat.add(Nat.double(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), Word.to_nat(1n+p, WCon{x, hi})), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), Equal.trans(Nat, Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi))), U.U32Nat.bit(x)), Nat.add(Nat.double(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), Nat.add(U.U32Nat.bit(x), Nat.double(Word.to_nat(p, hi)))), Nat.add(Nat.double(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), Word.to_nat(1n+p, WCon{x, hi})), wr.d8(p, W.W64.to_nat(q), W.W64.to_nat(b), W.W64.to_nat(r), Word.to_nat(p, hi), U.U32Nat.bit(x)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.double(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), zz), Nat.add(U.U32Nat.bit(x), Nat.double(Word.to_nat(p, hi))), Word.to_nat(1n+p, WCon{x, hi}), Equal.sym(Nat, Word.to_nat(1n+p, WCon{x, hi}), Nat.add(U.U32Nat.bit(x), Nat.double(Word.to_nat(p, hi))), wd.wv(p, x, hi)))), {==}))))), hX))), Equal.trans(Nat, Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi))), U.U32Nat.bit(x)), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), Equal.cong(Nat, Nat, zz => Nat.add(Nat.double(zz), U.U32Nat.bit(x)), Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))))), Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi)), e), Equal.trans(Nat, Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi))), U.U32Nat.bit(x)), Nat.add(Nat.double(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), Word.to_nat(1n+p, WCon{x, hi})), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), Equal.trans(Nat, Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi))), U.U32Nat.bit(x)), Nat.add(Nat.double(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), Nat.add(U.U32Nat.bit(x), Nat.double(Word.to_nat(p, hi)))), Nat.add(Nat.double(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), Word.to_nat(1n+p, WCon{x, hi})), wr.d8(p, W.W64.to_nat(q), W.W64.to_nat(b), W.W64.to_nat(r), Word.to_nat(p, hi), U.U32Nat.bit(x)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.double(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), zz), Nat.add(U.U32Nat.bit(x), Nat.double(Word.to_nat(p, hi))), Word.to_nat(1n+p, WCon{x, hi}), Equal.sym(Nat, Word.to_nat(1n+p, WCon{x, hi}), Nat.add(U.U32Nat.bit(x), Nat.double(Word.to_nat(p, hi))), wd.wv(p, x, hi)))), {==}))), wd.p2(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.step(x, b, (W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))))))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.step(x, b, (W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))))), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), W.W64.to_nat(W.W64.snd(W.W64.div.step(x, b, (W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))))))), W.W64.to_nat(b), wd.st(x, b, W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))), l, hb, Equal.trans(Bool, Nat.is_lt(Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), U.U32Nat.dbl(64n, 1n)), Nat.is_lt(Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), U.U32Nat.dbl(64n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(64n, 1n)), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), Equal.sym(Nat, Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), Equal.trans(Nat, Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi))), U.U32Nat.bit(x)), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), Equal.cong(Nat, Nat, zz => Nat.add(Nat.double(zz), U.U32Nat.bit(x)), Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))))), Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi)), e), Equal.trans(Nat, Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi))), U.U32Nat.bit(x)), Nat.add(Nat.double(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), Word.to_nat(1n+p, WCon{x, hi})), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), Equal.trans(Nat, Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi))), U.U32Nat.bit(x)), Nat.add(Nat.double(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), Nat.add(U.U32Nat.bit(x), Nat.double(Word.to_nat(p, hi)))), Nat.add(Nat.double(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), Word.to_nat(1n+p, WCon{x, hi})), wr.d8(p, W.W64.to_nat(q), W.W64.to_nat(b), W.W64.to_nat(r), Word.to_nat(p, hi), U.U32Nat.bit(x)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.double(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), zz), Nat.add(U.U32Nat.bit(x), Nat.double(Word.to_nat(p, hi))), Word.to_nat(1n+p, WCon{x, hi}), Equal.sym(Nat, Word.to_nat(1n+p, WCon{x, hi}), Nat.add(U.U32Nat.bit(x), Nat.double(Word.to_nat(p, hi))), wd.wv(p, x, hi)))), {==}))))), hX))))