def wd.st

bend-osdev-word64@0.1.1.0 · PROOF_div.bend:298
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-u32@0.1.0.0/LAWS.bend as UL
import bend-osdev-word64@0.1.1.0/word64.bend as W
import bend-osdev-word64@0.1.1.0/LAWS.bend as WB
import bend-osdev-word64@0.1.1.0/LAWS_bits.bend as LB
import bend-osdev-word64@0.1.1.0/PROOF_bits.bend as LBP

298def wd.st(+x: Bool, +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(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), U.U32Nat.bit(x)), U.U32Nat.dbl(64n, 1n)) == True{} : Bool}) -> {Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.step(x, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.step(x, b, (q, r))))) == Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), U.U32Nat.bit(x)) : Nat} & {Nat.is_lt(W.W64.to_nat(W.W64.snd(W.W64.div.step(x, b, (q, r)))), W.W64.to_nat(b)) == True{} : Bool}:
299  (Equal.trans(Nat, Nat.add(Nat.mul(W.W64.to_nat(W.W64.or(W.W64.shl(q, 1n), W.W64.from_u32(W.W64.bit(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)))))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.sel(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)), W.W64.sub(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b), W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x)))))), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), U32.to_nat(W.W64.bit(x))), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), U.U32Nat.bit(x)), wd.p1(Nat.add(Nat.mul(W.W64.to_nat(W.W64.or(W.W64.shl(q, 1n), W.W64.from_u32(W.W64.bit(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)))))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.sel(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)), W.W64.sub(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b), W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x)))))), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), U32.to_nat(W.W64.bit(x))), W.W64.to_nat(W.W64.sel(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)), W.W64.sub(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b), W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))))), W.W64.to_nat(b), wd.k(64n, W.W64.to_nat(q), W.W64.to_nat(b), W.W64.to_nat(r), U32.to_nat(W.W64.bit(x)), W.W64.to_nat(W.W64.shl(r, 1n)), U32.to_nat(U32.shrn(W.W64.hi(r), 31n)), W.W64.to_nat(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x)))), W.W64.to_nat(W.W64.shl(q, 1n)), U32.to_nat(U32.shrn(W.W64.hi(q), 31n)), W.W64.to_nat(W.W64.or(W.W64.shl(q, 1n), W.W64.from_u32(W.W64.bit(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)))))), W.W64.to_nat(W.W64.sel(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)), W.W64.sub(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b), W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))))), U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_lt(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b), Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)), hR, hb, Equal.trans(Bool, Nat.is_lt(Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), U32.to_nat(W.W64.bit(x))), U.U32Nat.dbl(64n, 1n)), Nat.is_lt(Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), U.U32Nat.bit(x)), 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(q), W.W64.to_nat(b)), W.W64.to_nat(r))), U32.to_nat(W.W64.bit(x))), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), U.U32Nat.bit(x)), Equal.sym(Nat, Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), U.U32Nat.bit(x)), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), U32.to_nat(W.W64.bit(x))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), zz), U.U32Nat.bit(x), U32.to_nat(W.W64.bit(x)), Equal.sym(Nat, U32.to_nat(W.W64.bit(x)), U.U32Nat.bit(x), wd.bv(x))))), hX), LB.shl_one_wrap(r), LB.shl_one_wrap(q), LBP.wb.or_bit(r, W.W64.bit(x), wd.bl(x)), Equal.trans(Nat, W.W64.to_nat(W.W64.or(W.W64.shl(q, 1n), W.W64.from_u32(W.W64.bit(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)))))), Nat.add(W.W64.to_nat(W.W64.shl(q, 1n)), U32.to_nat(W.W64.bit(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b))))), Nat.add(W.W64.to_nat(W.W64.shl(q, 1n)), U.U32Nat.bit(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)))), LBP.wb.or_bit(q, W.W64.bit(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b))), wd.bl(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)))), Equal.cong(Nat, Nat, zz => Nat.add(W.W64.to_nat(W.W64.shl(q, 1n)), zz), U32.to_nat(W.W64.bit(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)))), U.U32Nat.bit(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b))), wd.bv(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b))))), wd.bl(x), wd.top(r), Equal.trans(Bool, U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), Nat.is_eq(U32.to_nat(U32.shrn(W.W64.hi(r), 31n)), U32.to_nat(1)), Nat.is_eq(U32.to_nat(U32.shrn(W.W64.hi(r), 31n)), 1n), UL.u32_eq_value(U32.shrn(W.W64.hi(r), 31n), 1), {==}), Equal.sym(Bool, W.W64.is_lt(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b), Nat.is_lt(W.W64.to_nat(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x)))), W.W64.to_nat(b)), WB.lt_value(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)), Equal.cong(Bool, Bool, zz => Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), zz), Bool.not(W.W64.is_lt(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b), Equal.sym(Bool, W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b), Bool.not(W.W64.is_lt(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)), wn.ge_lt(W.W64.cmp(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)))), wd.sel(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)), W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), zz), U32.to_nat(W.W64.bit(x)), U.U32Nat.bit(x), wd.bv(x))), wd.p2(Nat.add(Nat.mul(W.W64.to_nat(W.W64.or(W.W64.shl(q, 1n), W.W64.from_u32(W.W64.bit(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)))))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.sel(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)), W.W64.sub(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b), W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x)))))), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), U32.to_nat(W.W64.bit(x))), W.W64.to_nat(W.W64.sel(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)), W.W64.sub(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b), W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))))), W.W64.to_nat(b), wd.k(64n, W.W64.to_nat(q), W.W64.to_nat(b), W.W64.to_nat(r), U32.to_nat(W.W64.bit(x)), W.W64.to_nat(W.W64.shl(r, 1n)), U32.to_nat(U32.shrn(W.W64.hi(r), 31n)), W.W64.to_nat(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x)))), W.W64.to_nat(W.W64.shl(q, 1n)), U32.to_nat(U32.shrn(W.W64.hi(q), 31n)), W.W64.to_nat(W.W64.or(W.W64.shl(q, 1n), W.W64.from_u32(W.W64.bit(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)))))), W.W64.to_nat(W.W64.sel(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)), W.W64.sub(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b), W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))))), U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_lt(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b), Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)), hR, hb, Equal.trans(Bool, Nat.is_lt(Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), U32.to_nat(W.W64.bit(x))), U.U32Nat.dbl(64n, 1n)), Nat.is_lt(Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), U.U32Nat.bit(x)), 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(q), W.W64.to_nat(b)), W.W64.to_nat(r))), U32.to_nat(W.W64.bit(x))), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), U.U32Nat.bit(x)), Equal.sym(Nat, Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), U.U32Nat.bit(x)), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), U32.to_nat(W.W64.bit(x))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), zz), U.U32Nat.bit(x), U32.to_nat(W.W64.bit(x)), Equal.sym(Nat, U32.to_nat(W.W64.bit(x)), U.U32Nat.bit(x), wd.bv(x))))), hX), LB.shl_one_wrap(r), LB.shl_one_wrap(q), LBP.wb.or_bit(r, W.W64.bit(x), wd.bl(x)), Equal.trans(Nat, W.W64.to_nat(W.W64.or(W.W64.shl(q, 1n), W.W64.from_u32(W.W64.bit(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)))))), Nat.add(W.W64.to_nat(W.W64.shl(q, 1n)), U32.to_nat(W.W64.bit(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b))))), Nat.add(W.W64.to_nat(W.W64.shl(q, 1n)), U.U32Nat.bit(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)))), LBP.wb.or_bit(q, W.W64.bit(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b))), wd.bl(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)))), Equal.cong(Nat, Nat, zz => Nat.add(W.W64.to_nat(W.W64.shl(q, 1n)), zz), U32.to_nat(W.W64.bit(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)))), U.U32Nat.bit(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b))), wd.bv(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b))))), wd.bl(x), wd.top(r), Equal.trans(Bool, U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), Nat.is_eq(U32.to_nat(U32.shrn(W.W64.hi(r), 31n)), U32.to_nat(1)), Nat.is_eq(U32.to_nat(U32.shrn(W.W64.hi(r), 31n)), 1n), UL.u32_eq_value(U32.shrn(W.W64.hi(r), 31n), 1), {==}), Equal.sym(Bool, W.W64.is_lt(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b), Nat.is_lt(W.W64.to_nat(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x)))), W.W64.to_nat(b)), WB.lt_value(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)), Equal.cong(Bool, Bool, zz => Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), zz), Bool.not(W.W64.is_lt(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b), Equal.sym(Bool, W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b), Bool.not(W.W64.is_lt(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)), wn.ge_lt(W.W64.cmp(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)))), wd.sel(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)), W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b))))
Uses (46)

Used by (1)

bend-osdev-word64@0.1.1.0/PROOF_div:wd.bs