~/bend-docscommunity

proofs/math/typed/w64sqrt.bend checks

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

15 imports
import Base
import ../../../spec/math/w64.bend as SW
import ../../../src/math/w64.bend as X
import ../../../src/math/natural.bend as M
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/u32.bend as U
import ../../lib/u32div.bend as UD
import ../../lib/word.bend as WD
import ../../lib/arith.bend as AR
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../u64/u64div.bend as PD
import ../natural/proof.bend as NP
import ./w64mul.bend as WM
import ./u32.bend as U32P

Definitions

def v source · line 26 · raw

@+x:U32 -> Nat

def sq source · line 29 · raw

@+n:Nat -> Nat

def mz source · line 34 · raw

@+p:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.uw(p, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(p, 0n)) == 0n : Nat}

def mval source · line 41 · raw

@+n:Nat -> @+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+hk:{Nat.is_le(k, n) == True{} : Bool} -> {1n+0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.uw(n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(n, k)) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.sc(k, one) : Nat}

def mask_v source · line 53 · raw

@+k:Nat -> @+hk:{Nat.is_le(k, 32n) == True{} : Bool} -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+m:U32 -> @+pm:{m == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, k)} : U32} -> {1n+v(m) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.sc(k, one) : Nat}

def m16 source · line 58 · raw

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

1 + v(m) == 2^16 for m the 16-bit mask

def sq_exact source · line 63 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:U32 -> @+hb:{Nat.is_lt(v(r), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.sc(16n, one)) == True{} : Bool} -> {v(U32.mul(r, r)) == sq(v(r)) : Nat}

def is_le_nat source · line 66 · raw

@+a:U32 -> @+b:U32 -> {U32.is_le(a, b) == Nat.is_le(v(a), v(b)) : Bool}

def DN source · line 72 · raw

@+one:Nat -> @+x:U32 -> @+r:U32 -> Type

def lt_sq source · line 75 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+r:U32 -> @+hb:{Nat.is_lt(v(r), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.sc(16n, one)) == True{} : Bool} -> {U32.is_lt(x, U32.mul(r, r)) == Nat.is_lt(v(x), sq(v(r))) : Bool}

def dn source · line 78 · raw

@+fu:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+r:U32 -> @+hf:{Nat.is_lt(v(r), fu) == True{} : Bool} -> @+hb:{Nat.is_lt(v(r), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.sc(16n, one)) == True{} : Bool} -> @+cb:Bool -> @+hc:{U32.is_lt(x, U32.mul(r, r)) == cb : Bool} -> @+nval:Nat -> @+hnr:{v(r) == nval : Nat} -> Pair({Nat.is_le(sq(v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.down32(fu, x, r, cb))), v(x)) == True{} : Bool}, {Nat.is_lt(v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.down32(fu, x, r, cb)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.sc(16n, one)) == True{} : Bool})

def up_okg source · line 102 · raw

@+x:U32 -> @+r:U32 -> @+m:U32 -> Bool

def up32g source · line 105 · raw

@fuel:Nat -> @+x:U32 -> @+r:U32 -> @up:Bool -> @+m:U32 -> U32

def impl_up source · line 114 · raw

@+fuel:Nat -> @+x:U32 -> @+r:U32 -> @+up:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.up32(fuel, x, r, up) == up32g(fuel, x, r, up, 65535) : U32}

def lt_to_le source · line 123 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(a, b) == True{} : Bool} -> {Nat.is_le(1n+a, b) == True{} : Bool}

def up_stop source · line 127 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+r:U32 -> @+m:U32 -> @+pm:{m == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 16n)} : U32} -> @+hle:{Nat.is_le(v(r), v(m)) == True{} : Bool} -> @+b:Bool -> @+hb2:{U32.is_le(U32.mul(U32.add(r, 1), U32.add(r, 1)), x) == b : Bool} -> @+a:Bool -> @+ha:{U32.is_lt(r, m) == a : Bool} -> @+hstop:{Bool.and(a, b) == False{} : Bool} -> {Nat.is_lt(v(x), sq(1n+v(r))) == True{} : Bool}

where the up loop stops, x < (r + 1)^2

def and_l source · line 150 · raw

@+a:Bool -> @+b:Bool -> @+h:{Bool.and(a, b) == True{} : Bool} -> {a == True{} : Bool}

def and_r source · line 157 · raw

@+a:Bool -> @+b:Bool -> @+h:{Bool.and(a, b) == True{} : Bool} -> {b == True{} : Bool}

def sub_succ_r source · line 165 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(a, b) == True{} : Bool} -> {Nat.sub(b, a) == 1n+Nat.sub(b, 1n+a) : Nat}

b - a == 1 + (b - (a + 1)) for a < b

def succ_v source · line 173 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:U32 -> @+m:U32 -> @+pm:{m == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 16n)} : U32} -> @+lt:{Nat.is_lt(v(r), v(m)) == True{} : Bool} -> {v(U32.add(r, 1)) == 1n+v(r) : Nat}

r + 1 below 2^16 when r < m == 2^16 - 1: its value and its exact square

def up source · line 180 · raw

@+fu:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+r:U32 -> @+m:U32 -> @+pm:{m == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 16n)} : U32} -> @+hf:{Nat.is_lt(Nat.sub(v(m), v(r)), fu) == True{} : Bool} -> @+hle:{Nat.is_le(v(r), v(m)) == True{} : Bool} -> @+hs:{Nat.is_le(sq(v(r)), v(x)) == True{} : Bool} -> @+ub:Bool -> @+hub:{up_okg(x, r, m) == ub : Bool} -> Pair({Nat.is_le(sq(v(up32g(fu, x, r, ub, m))), v(x)) == True{} : Bool}, {Nat.is_lt(v(x), sq(1n+v(up32g(fu, x, r, ub, m)))) == True{} : Bool})

def pow_sq source · line 205 · raw

@+a:Nat -> {Nat.pow(a, 2n) == sq(a) : Nat}

def sq_mono source · line 208 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_le(a, b) == True{} : Bool} -> {Nat.is_le(sq(a), sq(b)) == True{} : Bool}

def root_le source · line 212 · raw

@+r:Nat -> @+s:Nat -> @+n:Nat -> @+hr:{Nat.is_le(sq(r), n) == True{} : Bool} -> @+hs:{Nat.is_lt(n, sq(1n+s)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_lt(s, r) == c : Bool} -> {Nat.is_le(r, s) == True{} : Bool}

r^2 <= n < (s + 1)^2 gives r <= s

def root_uniq source · line 221 · raw

@+r:Nat -> @+s:Nat -> @+n:Nat -> @+h1:{Nat.is_le(sq(r), n) == True{} : Bool} -> @+h2:{Nat.is_lt(n, sq(1n+r)) == True{} : Bool} -> @+h3:{Nat.is_le(sq(s), n) == True{} : Bool} -> @+h4:{Nat.is_lt(n, sq(1n+s)) == True{} : Bool} -> {r == s : Nat}

def is_isqrt source · line 225 · raw

@+r:Nat -> @+n:Nat -> @+h1:{Nat.is_le(sq(r), n) == True{} : Bool} -> @+h2:{Nat.is_lt(n, sq(1n+r)) == True{} : Bool} -> {r == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n) : Nat}

a root r with r^2 <= n < (r + 1)^2 is M.isqrt(n)

def min_le source · line 233 · raw

@+e:U32 -> @+m:U32 -> @+c:Bool -> @+hc:{U32.is_lt(e, m) == c : Bool} -> {Nat.is_le(v(Bool.pick(U32, c, e, m)), v(m)) == True{} : Bool}

def min_pick source · line 241 · raw

@+e:U32 -> @+m:U32 -> {U32.min(e, m) == Bool.pick(U32, U32.is_lt(e, m), e, m) : U32}

Base 2.0.32 opens both words before it compares them.

def lt16 source · line 248 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:U32 -> @+m:U32 -> @+pm:{m == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 16n)} : U32} -> @+h:{Nat.is_le(v(r), v(m)) == True{} : Bool} -> {Nat.is_lt(v(r), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.sc(16n, one)) == True{} : Bool}

def le16 source · line 251 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:U32 -> @+m:U32 -> @+pm:{m == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 16n)} : U32} -> @+h:{Nat.is_lt(v(r), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.sc(16n, one)) == True{} : Bool} -> {Nat.is_le(v(r), v(m)) == True{} : Bool}

def RES source · line 254 · raw

@+fu:Nat -> @+x:U32 -> @+r:U32 -> @+m:U32 -> Nat

def main_fin source · line 257 · raw

@+x:U32 -> @+rd:U32 -> @+m:U32 -> @+fu:Nat -> @q:Pair({Nat.is_le(sq(v(up32g(fu, x, rd, up_okg(x, rd, m), m))), v(x)) == True{} : Bool}, {Nat.is_lt(v(x), sq(1n+v(up32g(fu, x, rd, up_okg(x, rd, m), m)))) == True{} : Bool}) -> {v(up32g(fu, x, rd, up_okg(x, rd, m), m)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(v(x)) : Nat}

def main_up source · line 261 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+rd:U32 -> @+m:U32 -> @+pm:{m == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 16n)} : U32} -> @p:Pair({Nat.is_le(sq(v(rd)), v(x)) == True{} : Bool}, {Nat.is_lt(v(rd), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.sc(16n, one)) == True{} : Bool}) -> {v(up32g(1n+U32.to_nat(U32.sub(m, rd)), x, rd, up_okg(x, rd, m), m)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(v(x)) : Nat}

def main_sqrt source · line 268 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+r0:U32 -> @+m:U32 -> @+pm:{m == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 16n)} : U32} -> @+hr0:{Nat.is_le(v(r0), v(m)) == True{} : Bool} -> {v(up32g(1n+U32.to_nat(U32.sub(m, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.down32(1n+U32.to_nat(r0), x, r0, U32.is_lt(x, U32.mul(r0, r0))))), x, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.down32(1n+U32.to_nat(r0), x, r0, U32.is_lt(x, U32.mul(r0, r0))), up_okg(x, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.down32(1n+U32.to_nat(r0), x, r0, U32.is_lt(x, U32.mul(r0, r0))), m), m)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(v(x)) : Nat}

def main_est source · line 272 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+e:U32 -> @+m:U32 -> @+pm:{m == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 16n)} : U32} -> {v(up32g(1n+U32.to_nat(U32.sub(m, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.down32(1n+U32.to_nat(U32.min(e, m)), x, U32.min(e, m), U32.is_lt(x, U32.mul(U32.min(e, m), U32.min(e, m)))))), x, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.down32(1n+U32.to_nat(U32.min(e, m)), x, U32.min(e, m), U32.is_lt(x, U32.mul(U32.min(e, m), U32.min(e, m)))), up_okg(x, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.down32(1n+U32.to_nat(U32.min(e, m)), x, U32.min(e, m), U32.is_lt(x, U32.mul(U32.min(e, m), U32.min(e, m)))), m), m)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(v(x)) : Nat}

from any estimate e, clamped to m == 2^16 - 1

def isqrt32_value source · line 276 · raw

@+x:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.Isqrt32.value(x)

Isqrt32.value: floor(sqrt(x)) for every U32, whatever the F32 estimate is