proofs/math/typed/w64isq.bend checks

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

15 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/word.bend as WD
import ../../lib/u32.bend as U
import ./w64mul.bend as W64M
import ./w64sqrt.bend as W64S
import ./w64add.bend as WA
import ./width.bend as WW
import ./u32laws.bend as LW

Definitions

def v source · line 22 · raw

@+x:U32 -> Nat

def sq source · line 25 · raw

@+n:Nat -> Nat

def true_ne_false source · line 28 · raw

@+h:{True{} == False{} : Bool} -> Empty

def ovs source · line 32 · raw

@+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+r:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sq_over(n, r) == Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n), sq(v(r))) : Bool}

r^2 > n

def dn64 source · line 35 · raw

@+fu:Nat -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+r:U32 -> @+cb:Bool -> @+nr:Nat -> @+hf:{Nat.is_lt(v(r), fu) == True{} : Bool} -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sq_over(n, r) == cb : Bool} -> @+hnr:{v(r) == nr : Nat} -> {Nat.is_le(sq(v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.down64(fu, n, r, cb))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n)) == True{} : Bool}

def up64_okg source · line 51 · raw

@+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+r:U32 -> @+m:U32 -> Bool

def up64g source · line 54 · raw

@fuel:Nat -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+r:U32 -> @up:Bool -> @+m:U32 -> U32

def impl_up64 source · line 63 · raw

@+fuel:Nat -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+r:U32 -> @+up:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.up64(fuel, n, r, up) == up64g(fuel, n, r, up, 4294967295) : U32}

def not_t source · line 72 · raw

@+x:Bool -> @+h:{Bool.not(x) == True{} : Bool} -> {x == False{} : Bool}

def not_not source · line 79 · raw

@+c:Bool -> {Bool.not(Bool.not(c)) == c : Bool}

def m32 source · line 86 · 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}

def succ_m source · line 89 · raw

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

def ustop source · line 94 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+q:U32 -> @+m:U32 -> @+pm:{m == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 32n)} : U32} -> @+hle:{Nat.is_le(v(q), v(m)) == True{} : Bool} -> @+hX:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n), sq(1n+v(m))) == True{} : Bool} -> @+a:Bool -> @+ha:{U32.is_lt(q, m) == a : Bool} -> @+c:Bool -> @+hcb:{Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sq_over(n, U32.add(q, 1))) == c : Bool} -> @+hstop:{Bool.and(a, c) == False{} : Bool} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n), sq(1n+v(q))) == True{} : Bool}

def up64p source · line 108 · raw

@+fu:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+q:U32 -> @+m:U32 -> @+pm:{m == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 32n)} : U32} -> @+ub:Bool -> @+hf:{Nat.is_lt(Nat.sub(v(m), v(q)), fu) == True{} : Bool} -> @+hle:{Nat.is_le(v(q), v(m)) == True{} : Bool} -> @+hs:{Nat.is_le(sq(v(q)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n)) == True{} : Bool} -> @+hX:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n), sq(1n+v(m))) == True{} : Bool} -> @+hub:{up64_okg(n, q, m) == ub : Bool} -> Pair({Nat.is_le(sq(v(up64g(fu, n, q, ub, m))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n)) == True{} : Bool}, {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n), sq(1n+v(up64g(fu, n, q, ub, m)))) == True{} : Bool})

def val0 source · line 127 · raw

@+x:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{x, 0}) == v(x) : Nat}

def isq_fin source · line 130 · raw

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

def fit64 source · line 134 · raw

@+l:U32 -> @+h:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h})) == True{} : Bool}

def big_g source · line 137 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+l:U32 -> @+h:U32 -> @+r0:U32 -> @+m:U32 -> @+pm:{m == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 32n)} : U32} -> {v(up64g(1n+v(U32.sub(m, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.down64(1n+v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q_clamp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.half(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.fst_q(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.div32(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, r0)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{r0, 0})))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q_clamp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.half(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.fst_q(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.div32(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, r0)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{r0, 0}))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sq_over(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q_clamp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.half(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.fst_q(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.div32(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, r0)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{r0, 0}))))))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.down64(1n+v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q_clamp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.half(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.fst_q(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.div32(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, r0)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{r0, 0})))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q_clamp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.half(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.fst_q(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.div32(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, r0)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{r0, 0}))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sq_over(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q_clamp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.half(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.fst_q(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.div32(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, r0)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{r0, 0}))))), up64_okg(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.down64(1n+v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q_clamp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.half(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.fst_q(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.div32(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, r0)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{r0, 0})))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q_clamp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.half(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.fst_q(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.div32(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, r0)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{r0, 0}))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sq_over(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q_clamp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.half(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.fst_q(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.div32(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, r0)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{r0, 0}))))), m), m)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h})) : Nat}

def big_v source · line 148 · raw

@+l:U32 -> @+h:U32 -> @+r0:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt_big(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, r0)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h})) : Nat}

def isqrt_c source · line 152 · raw

@+l:U32 -> @+h:U32 -> @+z:Bool -> @+hz:{U32.is_zero(h) == z : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt_pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, z)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h})) : Nat}

def isqrt_value source · line 161 · raw

@+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.Isqrt.value(n)