~/bend-docscommunity

proofs/math/typed/w64clz.bend checks

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

19 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/u32.bend as U
import ../natural/arith.bend as NR
import ../natural/bits.bend as BT
import ./natfuel.bend as NF
import ./w64sqrt.bend as W64S
import ./w64add.bend as WA
import ./w64sh.bend as SH
import ./shrn.bend as SR
import ./width.bend as WW
import ./u32laws.bend as LW

Definitions

def v source · line 26 · raw

@+x:U32 -> Nat

def true_ne_false source · line 29 · raw

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

def bl_succ source · line 33 · raw

@+np:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(1n+np) == 1n+0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(1n+np)) : Nat}

bit_length(1 + np) == 1 + bit_length(half(1 + np))

def high0 source · line 39 · raw

@+p:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(p, 0n) == 0n : Nat}

def bl_high source · line 47 · raw

@+k:Nat -> @+n:Nat -> @+h:{Nat.is_le(1n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(k, n)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n) == Nat.add(k, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(k, n))) : Nat}

high(k, n) >= 1: bit_length(n) == k + bit_length(high(k, n))

def hp_c source · line 56 · raw

@+k:Nat -> @+y:Nat -> @+h:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k), y) == True{} : Bool} -> @+q:Nat -> @+hq:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(k, y) == q : Nat} -> {Nat.is_le(1n, q) == True{} : Bool}

def high_pos source · line 66 · raw

@+k:Nat -> @+y:Nat -> @+h:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k), y) == True{} : Bool} -> {Nat.is_le(1n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(k, y)) == True{} : Bool}

2^k <= y: high(k, y) >= 1

def P1 source · line 71 · raw

@st:Pair(Nat, U32) -> Nat

def P2 source · line 75 · raw

@st:Pair(Nat, U32) -> U32

def INV source · line 79 · raw

@+k:Nat -> @+n:Nat -> @st:Pair(Nat, U32) -> Type

def eta_step source · line 82 · raw

@+k:Nat -> @st:Pair(Nat, U32) -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.bl_step(k, st) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.bl_step(k, (P1(st), P2(st))) : Pair(Nat, U32)}

def eta_fin source · line 87 · raw

@st:Pair(Nat, U32) -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.bl_fin(st) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.bl_fin((P1(st), P2(st))) : Nat}

def blstep_c source · line 92 · raw

@+k:Nat -> @+hk:{Nat.is_lt(k, 32n) == True{} : Bool} -> @+n:Nat -> @+base:Nat -> @+y:U32 -> @+hy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.add(k, k), v(y)) == True{} : Bool} -> @+inv:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n) == Nat.add(base, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(v(y))) : Nat} -> @+c:Bool -> @+hc:{U32.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pow2(k), y) == c : Bool} -> INV(k, n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.bl_pick(y, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pow2(k), k, base, c))

def blstep source · line 106 · raw

@+k:Nat -> @+hk:{Nat.is_lt(k, 32n) == True{} : Bool} -> @+n:Nat -> @+b:Nat -> @+y:U32 -> @+hi:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n) == Nat.add(b, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(v(y))) : Nat} -> @+hy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.add(k, k), v(y)) == True{} : Bool} -> INV(k, n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.bl_step(k, (b, y)))

def small_c source · line 109 · raw

@+y:U32 -> @+c:Bool -> @+hc:{U32.is_lt(y, 1) == c : Bool} -> @+nv:Nat -> @+hnv:{v(y) == nv : Nat} -> @+hy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(1n, v(y)) == True{} : Bool} -> {v(Bool.pick(U32, c, y, 1)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(v(y)) : Nat}

def S0 source · line 127 · raw

@+x:U32 -> Pair(Nat, U32)

def S1 source · line 129 · raw

@+x:U32 -> Pair(Nat, U32)

def S2 source · line 131 · raw

@+x:U32 -> Pair(Nat, U32)

def S3 source · line 133 · raw

@+x:U32 -> Pair(Nat, U32)

def S4 source · line 135 · raw

@+x:U32 -> Pair(Nat, U32)

def S5 source · line 137 · raw

@+x:U32 -> Pair(Nat, U32)

def bl_fin_v source · line 140 · raw

@+x:U32 -> @p:INV(1n, v(x), S5(x)) -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.bl_fin(S5(x)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(v(x)) : Nat}

def bstep2 source · line 146 · raw

@+k:Nat -> @+hk:{Nat.is_lt(k, 32n) == True{} : Bool} -> @+n:Nat -> @+b:Nat -> @+y:U32 -> @p:Pair({0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n) == Nat.add(b, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(v(y))) : Nat}, {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.add(k, k), v(y)) == True{} : Bool}) -> INV(k, n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.bl_step(k, (b, y)))

def Q1 source · line 150 · raw

@+x:U32 -> INV(16n, v(x), S1(x))

def Q2 source · line 153 · raw

@+x:U32 -> INV(8n, v(x), S2(x))

def Q3 source · line 156 · raw

@+x:U32 -> INV(4n, v(x), S3(x))

def Q4 source · line 159 · raw

@+x:U32 -> INV(2n, v(x), S4(x))

def Q5 source · line 162 · raw

@+x:U32 -> INV(1n, v(x), S5(x))

def eta_chain source · line 165 · raw

@+x:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.bitlen(x) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.bl_fin(S5(x)) : Nat}

def bitlen_v source · line 173 · raw

@+x:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.bitlen(x) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(v(x)) : Nat}

def not_t source · line 178 · raw

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

def not_f source · line 185 · raw

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

def clz_c source · line 192 · raw

@+l:U32 -> @+h:U32 -> @+c:Bool -> @+hc:{Bool.not(U32.is_zero(h)) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz_pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, c) == Nat.sub(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}))) : Nat}

def clz_value source · line 205 · raw

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