def wd.dz2
bend-osdev-word64@0.1.1.0 · PROOF_div.bend:415
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
import bend-osdev-word64@0.1.1.0/LAWS.bend as WB
415def wd.dz2(+hw: Word(32n), +lw: Word(32n), +b: W.W64, +h: {W.W64.is_zero(b) == False{} : Bool}, i1: {Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))) == Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.zero()), W.W64.to_nat(b)), W.W64.to_nat(W.W64.zero()))), Word.to_nat(32n, hw)) : Nat} & {Nat.is_lt(W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)) == True{} : Bool}) -> {Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.divmod.pick(False{}, W.W64{U32{hw}, U32{lw}}, b))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.divmod.pick(False{}, W.W64{U32{hw}, U32{lw}}, b)))) == W.W64.to_nat(W.W64{U32{hw}, U32{lw}}) : Nat} & {Nat.is_lt(W.W64.to_nat(W.W64.snd(W.W64.divmod.pick(False{}, W.W64{U32{hw}, U32{lw}}, b))), W.W64.to_nat(b)) == True{} : Bool}:
416 (+e1, +l1) = i1
417 %Equal.sym(W.W64 & W.W64, W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())), (W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))), W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), wd.eta(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))) : {Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, lw, b, _))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, lw, b, _)))) == W.W64.to_nat(W.W64{U32{hw}, U32{lw}}) : Nat} & {Nat.is_lt(W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, lw, b, _))), W.W64.to_nat(b)) == True{} : Bool}
418 (Equal.trans(Nat, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, lw, b, (W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))), W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, lw, b, (W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))), W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))))))), Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))))), Word.to_nat(32n, lw)), W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), wd.p1(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, lw, b, (W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))), W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, lw, b, (W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))), W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))))))), Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))))), Word.to_nat(32n, lw)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, lw, b, (W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))), W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))))), W.W64.to_nat(b), wd.bits(32n, lw, b, W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))), W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))), l1, wv.lt64(b), Equal.trans(Bool, Nat.is_lt(Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))))), Word.to_nat(32n, lw)), U.U32Nat.dbl(64n, 1n)), Nat.is_lt(W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), U.U32Nat.dbl(64n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(64n, 1n)), Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))))), Word.to_nat(32n, lw)), W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), Equal.sym(Nat, W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))))), Word.to_nat(32n, lw)), Equal.trans(Nat, W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), Nat.add(Word.to_nat(32n, lw), U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))))), Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))))), Word.to_nat(32n, lw)), Equal.trans(Nat, W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), Nat.add(Word.to_nat(32n, lw), U.U32Nat.dbl(32n, Word.to_nat(32n, hw))), Nat.add(Word.to_nat(32n, lw), U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))))), Equal.trans(Nat, W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), Nat.add(U32.to_nat(U32{lw}), U.U32Nat.dbl(32n, U32.to_nat(U32{hw}))), Nat.add(Word.to_nat(32n, lw), U.U32Nat.dbl(32n, Word.to_nat(32n, hw))), WB.to_nat_parts(U32{hw}, U32{lw}), {==}), Equal.cong(Nat, Nat, zz => Nat.add(Word.to_nat(32n, lw), U.U32Nat.dbl(32n, zz)), Word.to_nat(32n, hw), Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))), Equal.sym(Nat, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))), Word.to_nat(32n, hw), Equal.trans(Nat, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))), Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.zero()), W.W64.to_nat(b)), W.W64.to_nat(W.W64.zero()))), Word.to_nat(32n, hw)), Word.to_nat(32n, hw), e1, {==})))), wr.d10(Word.to_nat(32n, lw), W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))))))), wv.lt64(W.W64{U32{hw}, U32{lw}})))), Equal.sym(Nat, W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))))), Word.to_nat(32n, lw)), Equal.trans(Nat, W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), Nat.add(Word.to_nat(32n, lw), U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))))), Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))))), Word.to_nat(32n, lw)), Equal.trans(Nat, W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), Nat.add(Word.to_nat(32n, lw), U.U32Nat.dbl(32n, Word.to_nat(32n, hw))), Nat.add(Word.to_nat(32n, lw), U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))))), Equal.trans(Nat, W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), Nat.add(U32.to_nat(U32{lw}), U.U32Nat.dbl(32n, U32.to_nat(U32{hw}))), Nat.add(Word.to_nat(32n, lw), U.U32Nat.dbl(32n, Word.to_nat(32n, hw))), WB.to_nat_parts(U32{hw}, U32{lw}), {==}), Equal.cong(Nat, Nat, zz => Nat.add(Word.to_nat(32n, lw), U.U32Nat.dbl(32n, zz)), Word.to_nat(32n, hw), Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))), Equal.sym(Nat, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))), Word.to_nat(32n, hw), Equal.trans(Nat, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))), Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.zero()), W.W64.to_nat(b)), W.W64.to_nat(W.W64.zero()))), Word.to_nat(32n, hw)), Word.to_nat(32n, hw), e1, {==})))), wr.d10(Word.to_nat(32n, lw), W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))))))), wd.p2(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, lw, b, (W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))), W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, lw, b, (W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))), W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))))))), Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))))), Word.to_nat(32n, lw)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, lw, b, (W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))), W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))))), W.W64.to_nat(b), wd.bits(32n, lw, b, W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))), W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))), l1, wv.lt64(b), Equal.trans(Bool, Nat.is_lt(Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))))), Word.to_nat(32n, lw)), U.U32Nat.dbl(64n, 1n)), Nat.is_lt(W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), U.U32Nat.dbl(64n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(64n, 1n)), Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))))), Word.to_nat(32n, lw)), W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), Equal.sym(Nat, W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))))), Word.to_nat(32n, lw)), Equal.trans(Nat, W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), Nat.add(Word.to_nat(32n, lw), U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))))), Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))))), Word.to_nat(32n, lw)), Equal.trans(Nat, W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), Nat.add(Word.to_nat(32n, lw), U.U32Nat.dbl(32n, Word.to_nat(32n, hw))), Nat.add(Word.to_nat(32n, lw), U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))))), Equal.trans(Nat, W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), Nat.add(U32.to_nat(U32{lw}), U.U32Nat.dbl(32n, U32.to_nat(U32{hw}))), Nat.add(Word.to_nat(32n, lw), U.U32Nat.dbl(32n, Word.to_nat(32n, hw))), WB.to_nat_parts(U32{hw}, U32{lw}), {==}), Equal.cong(Nat, Nat, zz => Nat.add(Word.to_nat(32n, lw), U.U32Nat.dbl(32n, zz)), Word.to_nat(32n, hw), Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))), Equal.sym(Nat, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))), Word.to_nat(32n, hw), Equal.trans(Nat, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))), Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.zero()), W.W64.to_nat(b)), W.W64.to_nat(W.W64.zero()))), Word.to_nat(32n, hw)), Word.to_nat(32n, hw), e1, {==})))), wr.d10(Word.to_nat(32n, lw), W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))))))), wv.lt64(W.W64{U32{hw}, U32{lw}})))))