~/bend-docscommunity

proofs/math/typed/w64est.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64est.bend as W64est

24 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/w64.bend as SW
import ../../../src/math/w64.bend as X
import ../../../src/math/u64.bend as WU
import ../../../src/math/natural.bend as M
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../lib/word.bend as WD
import ../natural/arith.bend as NR
import ../natural/bits.bend as BT
import ./w64dm.bend as DM
import ./w64div.bend as W64D
import ./w64mul.bend as W64M
import ./w64sqrt.bend as W64S
import ./w64add.bend as WA
import ./w64sh.bend as SH
import ./w64clz.bend as CLZ
import ./f64bl.bend as BL
import ./width.bend as WW
import ./u32laws.bend as LW
import ../../lib/u32.bend as U3
import ../../lib/u32div.bend as UD

Definitions

def v source · line 33 · raw

@+x:U32 -> Nat

def up_x source · line 39 · raw

@+t:Nat -> @+x:Nat -> {Nat.is_lt(x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(t, 1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(t, x))) == True{} : Bool}

x < (high(t, x) + 1) 2^t

def shb_le source · line 50 · raw

@+t:Nat -> @+bv:Nat -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(t, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(t, bv)), bv) == True{} : Bool}

high(t, b) 2^t <= b

def succ_le source · line 57 · raw

@+bp:Nat -> @+y:Nat -> {Nat.is_le(1n+y, Nat.mul(1n+Nat.div(y, 1n+bp), 1n+bp)) == True{} : Bool}

y + 1 <= (y / B + 1) B

def core source · line 67 · raw

@+t:Nat -> @+x:Nat -> @+bv:Nat -> @+bp:Nat -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(t, bv) == 1n+bp : Nat} -> {Nat.is_lt(x, Nat.mul(1n+Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(t, x), 1n+bp), bv)) == True{} : Bool}

x < (high(t, x) / high(t, b) + 1) b for high(t, b) >= 1

def hpos source · line 77 · raw

@+t:Nat -> @+bv:Nat -> @+c:Bool -> @+hc:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(t, bv), 0n) == c : Bool} -> @+hle:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(t), bv) == True{} : Bool} -> {c == False{} : Bool}

high(t, b) != 0 when 2^t <= b

def lo_fit source · line 88 · raw

@+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w)) == True{} : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(w)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w) : Nat}

def lo_hi0 source · line 93 · raw

@+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hz:{U32.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(w)) == True{} : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(w)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w) : Nat}

def m32 source · line 101 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+m:U32 -> @+pm:{m == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 32n)} : U32} -> {1n+v(m) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one) : Nat}

1 + v(m) == 2^32 for the all-ones word

def cl_w source · line 107 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+m:U32 -> @+pm:{m == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 32n)} : U32} -> @+hm:{4294967295 == m : U32} -> @+x:Nat -> @+bv:Nat -> @+q:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+c:Bool -> @+hc:{U32.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(q)) == c : Bool} -> @+w:U32 -> @+hw:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q_clamp_z(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(q), c) == w : U32} -> @+hq:{Nat.is_lt(x, Nat.mul(1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(q), bv)) == True{} : Bool} -> @+hX:{Nat.is_lt(x, Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one), bv)) == True{} : Bool} -> {Nat.is_lt(x, Nat.mul(1n+v(w), bv)) == True{} : Bool}

the clamp to 2^32 - 1 keeps x < (q + 1) b, as x < 2^32 b. The clamped word is the variable w: with the literal 2^32 - 1 in the goal the checker would expand (2^32 - 1) * b.

def cl source · line 116 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+m:U32 -> @+pm:{m == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 32n)} : U32} -> @+hm:{4294967295 == m : U32} -> @+x:Nat -> @+bv:Nat -> @+q:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+c:Bool -> @+hc:{U32.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(q)) == c : Bool} -> @+hq:{Nat.is_lt(x, Nat.mul(1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(q), bv)) == True{} : Bool} -> @+hX:{Nat.is_lt(x, Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one), bv)) == True{} : Bool} -> {Nat.is_lt(x, Nat.mul(1n+v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q_clamp_z(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(q), c)), bv)) == True{} : Bool}

def low_shift source · line 121 · raw

@+n:Nat -> @+k:Nat -> @+t:Nat -> @+y:Nat -> @+e:{Nat.add(k, t) == n : Nat} -> @+hs0:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(t))) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y) : Nat}

C.low(n, y << k) == y << k when y < 2^t and k + t == n; n stays a variable, as a closed 2^64 in a goal is expanded by the checker.

def yv source · line 126 · raw

@+xl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+xh:U32 -> @+t:Nat -> @+t1:{Nat.is_le(1n, t) == True{} : Bool} -> @+t32:{Nat.is_le(t, 32n) == True{} : Bool} -> @+hx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.add(64n, t), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.X96(xl, xh)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr(xl, t), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{xh, 0}, Nat.sub(64n, t)))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(t, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.X96(xl, xh)) : Nat}

x >> t as the sum of xl >> t and xh << (64 - t), below 2^64

def hpos_le_w source · line 152 · raw

@+w:Nat -> @+lo:Nat -> @+h:Nat -> @+t:Nat -> @+tw:{Nat.is_le(t, w) == True{} : Bool} -> @+hh:{Nat.is_eq(h, 0n) == False{} : Bool} -> {Nat.is_le(1n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(t, Nat.add(lo, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(w, h)))) == True{} : Bool}

1 <= high(t, b) for t <= 32 and b >= 2^32 the bound 2^w stays open (w is 32 at the use): a closed 2^32 is expanded

def hpos_le source · line 160 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bl:U32 -> @+bh:U32 -> @+t:Nat -> @+t32:{Nat.is_le(t, 32n) == True{} : Bool} -> @+hz:{U32.is_zero(bh) == False{} : Bool} -> {Nat.is_le(1n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(t, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}))) == True{} : Bool}

def dsmall source · line 166 · raw

@+hi:U32 -> @+d:U32 -> @+hd:{U32.is_zero(d) == False{} : Bool} -> @+bp:Nat -> @+hb:{v(d) == 1n+bp : Nat} -> @+hl:{Nat.is_lt(v(hi), 1n+bp) == True{} : Bool} -> {U32.div(hi, d) == 0 : U32}

a high word below the divisor: quotient 0, remainder itself

def msmall source · line 170 · raw

@+hi:U32 -> @+d:U32 -> @+hd:{U32.is_zero(d) == False{} : Bool} -> @+bp:Nat -> @+hb:{v(d) == 1n+bp : Nat} -> @+hl:{Nat.is_lt(v(hi), 1n+bp) == True{} : Bool} -> {U32.mod(hi, d) == hi : U32}

def ne0 source · line 174 · raw

@+n:Nat -> @+h:{Nat.is_le(1n, n) == True{} : Bool} -> {Nat.is_eq(n, 0n) == False{} : Bool}

def dpos source · line 182 · raw

@+hi:U32 -> @+d:U32 -> @+hd:{U32.is_zero(d) == False{} : Bool} -> @+bp:Nat -> @+hb:{v(d) == 1n+bp : Nat} -> @+hle:{Nat.is_le(1n+bp, v(hi)) == True{} : Bool} -> {U32.is_zero(U32.div(hi, d)) == False{} : Bool}

a divisor at most the high word: the high quotient word is nonzero

def est_eq_c source · line 189 · raw

@+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+d:U32 -> @+hd:{U32.is_zero(d) == False{} : Bool} -> @+bp:Nat -> @+hn:{v(d) == 1n+bp : Nat} -> @+c:Bool -> @+hc:{U32.is_le(d, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(y)) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.est_pick(y, d, c) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q_clamp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.fst_q(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.div32(y, d))) : U32}

def est_eq_n source · line 203 · raw

@+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+d:U32 -> @+hd:{U32.is_zero(d) == False{} : Bool} -> @+n:Nat -> @+hn:{v(d) == n : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.est32(y, d) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q_clamp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.fst_q(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.div32(y, d))) : U32}

def est_eq source · line 212 · raw

@+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+d:U32 -> @+hd:{U32.is_zero(d) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.est32(y, d) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q_clamp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.fst_q(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.div32(y, d))) : U32}

the estimate est32 of q_est is min(floor(y / d), 2^32 - 1), the clamped div32 quotient

def est_m source · line 216 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+xh:U32 -> @+bl:U32 -> @+bh:U32 -> @+hz:{U32.is_zero(bh) == False{} : Bool} -> @+t:Nat -> @+t1:{Nat.is_le(1n, t) == True{} : Bool} -> @+t32:{Nat.is_le(t, 32n) == True{} : Bool} -> @+hx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.add(64n, t), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.X96(xl, xh)) == True{} : Bool} -> @+fb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(t, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}))) == True{} : Bool} -> @+hX:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.X96(xl, xh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}))) == True{} : Bool} -> @+nb:Nat -> @+hnb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(t, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh})) == nb : Nat} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.X96(xl, xh), Nat.mul(1n+v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q_est(xl, xh, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}, t)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}))) == True{} : Bool}

the estimate for B = high(t, b) = 1 + bp

def two_limb_fits source · line 237 · raw

@+k:Nat -> @+j:Nat -> @+r:Nat -> @+x:Nat -> @+hr:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, r) == True{} : Bool} -> @+hx:{Nat.is_lt(x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(j)) == True{} : Bool} -> {Nat.is_lt(Nat.add(r, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, x)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(Nat.add(k, j))) == True{} : Bool}

WW.two_limb_lt from C.fits(k, r): the bound 2^k stays open (k is 32 at the use)

def est_t source · line 240 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+xh:U32 -> @+bl:U32 -> @+bh:U32 -> @+hz:{U32.is_zero(bh) == False{} : Bool} -> @+hX:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.X96(xl, xh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}))) == True{} : Bool} -> @+t:Nat -> @+ht:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.bitlen(bh) == t : Nat} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.X96(xl, xh), Nat.mul(1n+v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q_est(xl, xh, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}, t)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}))) == True{} : Bool}

def est_up source · line 259 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+xh:U32 -> @+bl:U32 -> @+bh:U32 -> @+hz:{U32.is_zero(bh) == False{} : Bool} -> @+hX:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.X96(xl, xh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}))) == True{} : Bool} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.X96(xl, xh), Nat.mul(1n+v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q_est(xl, xh, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.bitlen(bh))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}))) == True{} : Bool}

the estimate is never below the quotient: x < (q_est + 1) b