proofs/math/typed/w64sh.bend checks

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

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 ../../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 ../../lib/u32.bend as U
import ../../lib/u32div.bend as UD
import ../../lib/lemmas/spec/numeric.bend as S
import ../natural/arith.bend as NR
import ../u64/u64div.bend as PD
import ./w64mul.bend as W64M
import ./w64add.bend as WA
import ./width.bend as WW
import ./u32laws.bend as LW
import ./shrn.bend as SR

Definitions

def v source · line 27 · raw

@+x:U32 -> Nat

def vb source · line 30 · raw

@+x:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, v(x)) == True{} : Bool}

def p2w source · line 34 · raw

@+k:Nat -> @+hk:{Nat.is_lt(k, 32n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pow2(k) == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, k)} : U32}

the 2^k table is the word with bit k set

def p2v source · line 103 · raw

@+k:Nat -> @+hk:{Nat.is_lt(k, 32n) == True{} : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pow2(k)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k) : Nat}

def pow2_eq source · line 106 · raw

@+k:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k) == 1n+Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k), 1n) : Nat}

def div_p2 source · line 110 · raw

@+x:U32 -> @+k:Nat -> @+hk:{Nat.is_lt(k, 32n) == True{} : Bool} -> {v(U32.div(x, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pow2(k))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(k, v(x)) : Nat}

x / 2^k on a word is high(k, x)

def mul_low source · line 117 · raw

@+x:U32 -> @+y:U32 -> {v(U32.mul(x, y)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(32n, Nat.mul(v(x), v(y))) : Nat}

a word product wraps mod 2^32

def mul_p2 source · line 122 · raw

@+x:U32 -> @+k:Nat -> @+hk:{Nat.is_lt(k, 32n) == True{} : Bool} -> {v(U32.mul(x, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pow2(k))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, v(x))) : Nat}

x 2^k on a word: low(32, shift(k, x))

def fits_high source · line 126 · raw

@+t:Nat -> @+s:Nat -> @+x:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.add(t, s), x) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(t, x)) == True{} : Bool}

def fits_mono source · line 129 · raw

@+a:Nat -> @+b:Nat -> @+x:Nat -> @+hab:{Nat.is_le(a, b) == True{} : Bool} -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(a, x) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(b, x) == True{} : Bool}

def val source · line 132 · raw

@+l:U32 -> @+h:U32 -> Nat

def fit64 source · line 135 · raw

@+l:U32 -> @+h:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, val(l, h)) == True{} : Bool}

def val0 source · line 138 · raw

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

def fits32 source · line 141 · raw

@+t:Nat -> @+s:Nat -> @+hts:{Nat.add(t, s) == 32n : Nat} -> @+x:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.add(t, s), v(x)) == True{} : Bool}

def shr_small source · line 145 · raw

@+l:U32 -> @+h:U32 -> @+j:Nat -> @+hk:{Nat.is_lt(1n+j, 32n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr_lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, 1n+j)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(1n+j, val(l, h)) : Nat}

1 <= t < 32, s == 32 - t

def zero64 source · line 169 · raw

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

def shr_big source · line 174 · raw

@+l:U32 -> @+h:U32 -> @+k:Nat -> @+hge:{Nat.is_le(32n, k) == True{} : Bool} -> @+hlt:{Nat.is_lt(k, 64n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{U32.shrn(h, Nat.sub(k, 32n)), 0}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(k, val(l, h)) : Nat}

32 <= k < 64: the high word shifted by k - 32

def shr_ge_c source · line 182 · raw

@+l:U32 -> @+h:U32 -> @+k:Nat -> @+hge:{Nat.is_le(32n, k) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_le(64n, k) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr_ge(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, k, c)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(k, val(l, h)) : Nat}

def shr_c source · line 189 · raw

@+l:U32 -> @+h:U32 -> @+k:Nat -> @+c:Bool -> @+hc:{Nat.is_lt(k, 32n) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr_pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, k, c)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(k, val(l, h)) : Nat}

def shr_value source · line 198 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.Shr.value(a, k)

def shift_swap source · line 203 · raw

@+a:Nat -> @+b:Nat -> @+x:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(a, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(b, x)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(b, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(a, x)) : Nat}

def shl_eq source · line 207 · raw

@+t:Nat -> @+s:Nat -> @+hts:{Nat.add(t, s) == 32n : Nat} -> @+l:U32 -> @+h:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(t, Nat.add(v(l), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, v(h)))) == Nat.add(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(t, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(s, v(l))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(s, v(l)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(t, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(s, v(h)))))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(s, v(h)))) : Nat}

shift(t, a) in 32-bit pieces, t + s == 32

def shl_small source · line 210 · raw

@+l:U32 -> @+h:U32 -> @+j:Nat -> @+hk:{Nat.is_lt(1n+j, 32n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl_lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, 1n+j)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(1n+j, val(l, h))) : Nat}

def shl_big source · line 231 · raw

@+l:U32 -> @+h:U32 -> @+k:Nat -> @+hge:{Nat.is_le(32n, k) == True{} : Bool} -> @+hlt:{Nat.is_lt(k, 64n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, U32.mul(l, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pow2(Nat.sub(k, 32n)))}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, val(l, h))) : Nat}

def shl_c source · line 244 · raw

@+l:U32 -> @+h:U32 -> @+k:Nat -> @+c:Bool -> @+hc:{Nat.is_lt(k, 32n) == c : Bool} -> @+hk:{Nat.is_lt(k, 64n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl_pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, k, c)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, val(l, h))) : Nat}

def shl_value source · line 253 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:Nat -> @+hk:{Nat.is_lt(k, 64n) == True{} : Bool} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.Shl.value(a, k, hk)

def or_zero source · line 260 · raw

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

def or_t source · line 271 · raw

@+b:Bool -> {Bool.or(b, True{}) == True{} : Bool}

def half_bv source · line 278 · raw

@+b:Bool -> @+u:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(b), Nat.double(u))) == u : Nat}

def or1 source · line 286 · raw

@+x:U32 -> {v(U32.or(x, 1)) == 1n+Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(v(x))) : Nat}

setting bit 0: 1 + 2 half(x)

def or0 source · line 297 · raw

@+x:U32 -> {U32.or(x, 0) == x : U32}

def mod2_lt source · line 302 · raw

@+q:Nat -> {Nat.is_lt(Nat.mod(q, 2n), 2n) == True{} : Bool}

def jam0_eq source · line 305 · raw

@+q:Nat -> {Nat.add(Nat.mul(2n, Nat.div(q, 2n)), Nat.mod(q, 2n)) == q : Nat}

def jam1_eq source · line 308 · raw

@+q:Nat -> {Nat.add(Nat.mul(2n, Nat.div(q, 2n)), 1n) == 1n+Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(q)) : Nat}

def jam0_m source · line 312 · raw

@+q:Nat -> @+m:Nat -> @+hm:{Nat.mod(q, 2n) == m : Nat} -> @+h2:{Nat.is_lt(m, 2n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(q, 0n) == q : Nat}

def jam1_k source · line 321 · raw

@+q:Nat -> @+m:Nat -> @+hm:{Nat.mod(q, 2n) == m : Nat} -> @+h2:{Nat.is_lt(m, 2n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(q, 1n) == 1n+Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(q)) : Nat}

def min1 source · line 330 · raw

@+rp:Nat -> {Nat.min(1n+rp, 1n) == 1n : Nat}

def jam_r1 source · line 337 · raw

@+q:Nat -> @+rp:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(q, 1n+rp) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(q, 1n) : Nat}

def jam1_m source · line 340 · raw

@+q:Nat -> @+rp:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(q, 1n+rp) == 1n+Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(q)) : Nat}

def huge_n source · line 343 · raw

@+x:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(Bool.not(Nat.is_eq(x, 0n))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0n, x) : Nat}

def is_eq_add source · line 350 · raw

@+l:Nat -> @+s:Nat -> {Nat.is_eq(s, Nat.add(l, s)) == Nat.is_eq(l, 0n) : Bool}

def fits_lek source · line 358 · raw

@+k:Nat -> @+x:Nat -> @+y:Nat -> @+h:{Nat.is_le(x, y) == True{} : Bool} -> @+hy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, y) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, x) == True{} : Bool}

def sj_big source · line 361 · raw

@+l:U32 -> @+h:U32 -> @+k:Nat -> @+hk:{Nat.is_le(64n, k) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.b32(Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}))), 0}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(k, val(l, h)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, val(l, h))) : Nat}

def sj_bit source · line 371 · raw

@+l:U32 -> @+h:U32 -> @+k:Nat -> @+hk:{Nat.is_lt(k, 64n) == True{} : Bool} -> {Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.eq(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, k), k), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h})) == Bool.not(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, val(l, h)), 0n)) : Bool}

def sj_c source · line 384 · raw

@+l:U32 -> @+h:U32 -> @+k:Nat -> @+ln:Nat -> @+hL:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, val(l, h)) == ln : Nat} -> @+hk:{Nat.is_lt(k, 64n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.or_bit(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, k), Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.eq(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, k), k), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h})))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(k, val(l, h)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, val(l, h))) : Nat}

def sj_top source · line 407 · raw

@+l:U32 -> @+h:U32 -> @+k:Nat -> @+c:Bool -> @+hc:{Nat.is_le(64n, k) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.jam_pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, k, c)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(k, val(l, h)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, val(l, h))) : Nat}

def shr_jam_value source · line 414 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.ShrJam.value(a, k)