def wd.k

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

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-u32@0.1.0.0/LAWS_order.bend as UO

267def wd.k(+N: Nat, +Q: Nat, +B: Nat, +R: Nat, +tx: Nat, +Sr: Nat, +tr: Nat, +R2: Nat, +Sq: Nat, +tq: Nat, +Q1: Nat, +R1: Nat, +T: Bool, +L: Bool, +g: Bool, +hR: {Nat.is_lt(R, B) == True{} : Bool}, +hB: {Nat.is_lt(B, U.U32Nat.dbl(N, 1n)) == True{} : Bool}, +hX: {Nat.is_lt(Nat.add(Nat.double(Nat.add(Nat.mul(Q, B), R)), tx), U.U32Nat.dbl(N, 1n)) == True{} : Bool}, +fr: {Nat.add(Sr, U.U32Nat.dbl(N, tr)) == Nat.double(R) : Nat}, +fq: {Nat.add(Sq, U.U32Nat.dbl(N, tq)) == Nat.double(Q) : Nat}, +er2: {R2 == Nat.add(Sr, tx) : Nat}, +eq1: {Q1 == Nat.add(Sq, U.U32Nat.bit(g)) : Nat}, +htx: {Nat.is_lt(tx, U.U32Nat.dbl(1n, 1n)) == True{} : Bool}, +htr: {Nat.is_lt(tr, U.U32Nat.dbl(1n, 1n)) == True{} : Bool}, +eT: {T == Nat.is_eq(tr, 1n) : Bool}, +eL: {Nat.is_lt(R2, B) == L : Bool}, +eg: {Bool.or(T, Bool.not(L)) == g : Bool}, +er1: {Nat.add(R1, Nat.mul(U.U32Nat.bit(g), B)) == Nat.add(R2, U.U32Nat.dbl(N, Nat.mul(U.U32Nat.bit(g), U.U32Nat.bit(L)))) : Nat}) -> {Nat.add(Nat.mul(Q1, B), R1) == Nat.add(Nat.double(Nat.add(Nat.mul(Q, B), R)), tx) : Nat} & {Nat.is_lt(R1, B) == True{} : Bool}:
268  +bT = Equal.trans(Nat, U.U32Nat.bit(T), U.U32Nat.bit(Nat.is_eq(tr, 1n)), tr, Equal.cong(Bool, Nat, zz => U.U32Nat.bit(zz), T, Nat.is_eq(tr, 1n), eT), wd.bt(tr, htr))
269  +eput = Equal.trans(Nat, Nat.add(R2, U.U32Nat.dbl(N, U.U32Nat.bit(T))), Nat.add(tx, Nat.add(Sr, U.U32Nat.dbl(N, tr))), Nat.add(tx, Nat.double(R)), Equal.trans(Nat, Nat.add(R2, U.U32Nat.dbl(N, U.U32Nat.bit(T))), Nat.add(Nat.add(Sr, tx), U.U32Nat.dbl(N, tr)), Nat.add(tx, Nat.add(Sr, U.U32Nat.dbl(N, tr))), Equal.trans(Nat, Nat.add(R2, U.U32Nat.dbl(N, U.U32Nat.bit(T))), Nat.add(Nat.add(Sr, tx), U.U32Nat.dbl(N, U.U32Nat.bit(T))), Nat.add(Nat.add(Sr, tx), U.U32Nat.dbl(N, tr)), Equal.cong(Nat, Nat, zz => Nat.add(zz, U.U32Nat.dbl(N, U.U32Nat.bit(T))), R2, Nat.add(Sr, tx), er2), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(Sr, tx), U.U32Nat.dbl(N, zz)), U.U32Nat.bit(T), tr, bT)), wr.d0(Sr, tx, N, tr)), Equal.cong(Nat, Nat, zz => Nat.add(tx, zz), Nat.add(Sr, U.U32Nat.dbl(N, tr)), Nat.double(R), fr))
270  +c1 = UL.divstep_value(N, R2, B, R, tx, R1, T, L, g, eput, eL, eg, er1, wd.lt2(tx, htx), hR, hB)
271  +c2 = UL.divstep_lt(N, R2, B, R, tx, R1, T, L, g, eput, eL, eg, er1, wd.lt2(tx, htx), hR, hB)
272  +qle = Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(Q, Nat.sub(B, 1n+R)), Nat.add(Nat.mul(Q, R), R)), Q), Nat.add(Nat.mul(Q, Nat.add(Nat.sub(B, 1n+R), 1n+R)), R), Nat.add(Nat.mul(Q, B), R), wr.d1(Q, Nat.sub(B, 1n+R), R), Equal.cong(Nat, Nat, zz => Nat.add(Nat.mul(Q, zz), R), Nat.add(Nat.sub(B, 1n+R), 1n+R), B, UL.nat_lt_witness(R, B, hR)))
273  +hQ = UO.nat_le_lt_trans(Nat.double(Q), Nat.add(Nat.double(Nat.add(Nat.mul(Q, B), R)), tx), U.U32Nat.dbl(N, 1n), Equal.trans(Bool, Nat.is_le(Nat.double(Q), Nat.add(Nat.double(Nat.add(Nat.mul(Q, B), R)), tx)), Nat.is_le(Nat.double(Q), Nat.add(Nat.add(Nat.double(Nat.add(Nat.mul(Q, Nat.sub(B, 1n+R)), Nat.add(Nat.mul(Q, R), R))), tx), Nat.double(Q))), True{}, Equal.sym(Bool, Nat.is_le(Nat.double(Q), Nat.add(Nat.add(Nat.double(Nat.add(Nat.mul(Q, Nat.sub(B, 1n+R)), Nat.add(Nat.mul(Q, R), R))), tx), Nat.double(Q))), Nat.is_le(Nat.double(Q), Nat.add(Nat.double(Nat.add(Nat.mul(Q, B), R)), tx)), Equal.cong(Nat, Bool, zz => Nat.is_le(Nat.double(Q), zz), Nat.add(Nat.add(Nat.double(Nat.add(Nat.mul(Q, Nat.sub(B, 1n+R)), Nat.add(Nat.mul(Q, R), R))), tx), Nat.double(Q)), Nat.add(Nat.double(Nat.add(Nat.mul(Q, B), R)), tx), Equal.trans(Nat, Nat.add(Nat.add(Nat.double(Nat.add(Nat.mul(Q, Nat.sub(B, 1n+R)), Nat.add(Nat.mul(Q, R), R))), tx), Nat.double(Q)), Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(Q, Nat.sub(B, 1n+R)), Nat.add(Nat.mul(Q, R), R)), Q)), tx), Nat.add(Nat.double(Nat.add(Nat.mul(Q, B), R)), tx), wr.d2(Q, Nat.sub(B, 1n+R), R, tx), Equal.cong(Nat, Nat, zz => Nat.add(Nat.double(zz), tx), Nat.add(Nat.add(Nat.mul(Q, Nat.sub(B, 1n+R)), Nat.add(Nat.mul(Q, R), R)), Q), Nat.add(Nat.mul(Q, B), R), qle)))), UL.nat_le_add(Nat.double(Q), Nat.add(Nat.double(Nat.add(Nat.mul(Q, Nat.sub(B, 1n+R)), Nat.add(Nat.mul(Q, R), R))), tx))), hX)
274  +esq = UL.dbl_nowrap(N, tq, Sq, Nat.double(Q), Nat.double(Q), fq, UL.nat_le_refl(Nat.double(Q)), hQ)
275  (Equal.trans(Nat, Nat.add(Nat.mul(Q1, B), R1), Nat.add(Nat.double(Nat.mul(Q, B)), Nat.add(tx, Nat.double(R))), Nat.add(Nat.double(Nat.add(Nat.mul(Q, B), R)), tx), Equal.trans(Nat, Nat.add(Nat.mul(Q1, B), R1), Nat.add(Nat.double(Nat.mul(Q, B)), Nat.add(R1, Nat.mul(U.U32Nat.bit(g), B))), Nat.add(Nat.double(Nat.mul(Q, B)), Nat.add(tx, Nat.double(R))), Equal.trans(Nat, Nat.add(Nat.mul(Q1, B), R1), Nat.add(Nat.mul(Nat.add(Nat.double(Q), U.U32Nat.bit(g)), B), R1), Nat.add(Nat.double(Nat.mul(Q, B)), Nat.add(R1, Nat.mul(U.U32Nat.bit(g), B))), Equal.trans(Nat, Nat.add(Nat.mul(Q1, B), R1), Nat.add(Nat.mul(Nat.add(Sq, U.U32Nat.bit(g)), B), R1), Nat.add(Nat.mul(Nat.add(Nat.double(Q), U.U32Nat.bit(g)), B), R1), Equal.cong(Nat, Nat, zz => Nat.add(Nat.mul(zz, B), R1), Q1, Nat.add(Sq, U.U32Nat.bit(g)), eq1), Equal.cong(Nat, Nat, zz => Nat.add(Nat.mul(Nat.add(zz, U.U32Nat.bit(g)), B), R1), Sq, Nat.double(Q), esq)), wr.d3(Q, U.U32Nat.bit(g), B, R1)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.double(Nat.mul(Q, B)), zz), Nat.add(R1, Nat.mul(U.U32Nat.bit(g), B)), Nat.add(tx, Nat.double(R)), c1)), wr.d4(Q, B, tx, R)), c2)