def wd.bits

bend-osdev-word64@0.1.1.0 · PROOF_div.bend:400

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
import bend-osdev-word64@0.1.1.0/word64.bend as W
import bend-osdev-u32@0.1.0.0/LAWS_order.bend as UO

400def wd.bits(m: Nat, w: Word(m), +b: W.W64, +q: W.W64, +r: W.W64, +hR: {Nat.is_lt(W.W64.to_nat(r), W.W64.to_nat(b)) == True{} : Bool}, +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(m, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(m, w)), U.U32Nat.dbl(64n, 1n)) == True{} : Bool}) -> {Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(m, w, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(m, w, b, (q, r))))) == Nat.add(U.U32Nat.dbl(m, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(m, w)) : Nat} & {Nat.is_lt(W.W64.to_nat(W.W64.snd(W.W64.div.bits(m, w, b, (q, r)))), W.W64.to_nat(b)) == True{} : Bool}:
401  match m w:
402    case 0n WNil{}:
403      (Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)), 0n), Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)), UL.nat_add_zero(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), hR)
404    case 1n+ +p WCon{+x, +hi}:
405      wd.bs(p, x, hi, b, q, r, hb, hX, wd.bits(p, hi, b, q, r, hR, hb, UO.nat_le_lt_trans(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.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), Equal.trans(Bool, Nat.is_le(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.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.is_le(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.add(Nat.add(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(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)))), True{}, Equal.sym(Bool, Nat.is_le(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.add(Nat.add(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(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.is_le(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.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, Bool, zz => Nat.is_le(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)), zz), Nat.add(Nat.add(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(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.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.add(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(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.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})), wr.d9(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.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)))), {==})))), UL.nat_le_add(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.add(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)))), hX)))