~/bend-docscommunity

proofs/lib/u32.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as MU32

12 imports
import Base
import ./logic.bend as L
import ./nat.bend as N
import ../../spec/lib/common.bend as SC
import ./lemmas/spec/numeric.bend as S
import ./lemmas/proofs/numeric.bend as RN
import ./lemmas/proofs/nat_algebra.bend as NA
import ./lemmas/proofs/modular_addition.bend as MA
import ./lemmas/proofs/word_value.bend as WV
import ./lemmas/proofs/word_shift.bend as WS
import ./lemmas/proofs/word_comparison.bend as WC
import ./lemmas/proofs/subtraction_bounds.bend as SB

Definitions

def to_nat_word source · line 18 · raw

@+w:Word(32n) -> {U32.to_nat(U32{w}) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(32n, w) : Nat}

def pow2_scale source · line 21 · raw

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

def double_pow source · line 28 · raw

@+x:Nat -> {Nat.double(x) == Nat.add(x, Nat.add(x, 0n)) : Nat}

def pow2_pow source · line 32 · raw

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

def word_from_unsigned source · line 41 · raw

@+w:Word(32n) -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.from_nat(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(32n, w)) == w : Word(32n)}

Every word is recovered from its unsigned interpretation (reconstruct at 0).

def injective source · line 45 · raw

@+a:U32 -> @+b:U32 -> @+e:{U32.to_nat(a) == U32.to_nat(b) : Nat} -> {a == b : U32}

def pow2_le_pow source · line 58 · raw

@+n:Nat -> @+k:Nat -> @+hk:{Nat.is_le(k, n) == True{} : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k), Nat.pow(2n, n)) == True{} : Bool}

def pow2_le_scale source · line 62 · raw

@+n:Nat -> @+k:Nat -> @+hk:{Nat.is_le(k, n) == True{} : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.scale_binary(n, 1n)) == True{} : Bool}

def from_nat_value_k source · line 67 · raw

@+n:Nat -> @+k:Nat -> @+v:Nat -> @+hk:{Nat.is_le(k, n) == True{} : Bool} -> @+hv:{Nat.is_lt(v, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.from_nat(n, v)) == v : Nat}

Width-generic wrappers: bounds are 2^k with k <= n, never a closed 2^32.

def shl_exact_k source · line 70 · raw

@+n:Nat -> @+k:Nat -> @+w:Word(n) -> @+hk:{Nat.is_le(k, n) == True{} : Bool} -> @+h:{Nat.is_lt(Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, w)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, Word.shl(n, w)) == Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, w)) : Nat}

def inc_from source · line 75 · raw

@+n:Nat -> @+p:Nat -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.from_nat(n, p)) == p : Nat} -> {Word.inc(n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.from_nat(n, p)) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.from_nat(n, 1n+p) : Word(n)}

one increment over an abstract width (the checker never expands a literal-width word here)

def from_nat_step source · line 81 · raw

@+p:Nat -> @+a:Word(32n) -> @+b:Word(32n) -> @+rec:{U32.from_nat(p) == U32{a} : U32} -> @+hinc:{Word.inc(32n, a) == b : Word(32n)} -> {U32.from_nat(1n+p) == U32{b} : U32}

the U32 step over abstract words a (for p) and b (for p + 1)

def from_nat_word source · line 85 · raw

@+i:Nat -> @+k:Nat -> @+hk:{Nat.is_le(k, 32n) == True{} : Bool} -> @+h:{Nat.is_lt(i, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k)) == True{} : Bool} -> {U32.from_nat(i) == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.from_nat(32n, i)} : U32}

def to_nat_from_nat source · line 93 · raw

@+i:Nat -> @+k:Nat -> @+hk:{Nat.is_le(k, 32n) == True{} : Bool} -> @+h:{Nat.is_lt(i, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k)) == True{} : Bool} -> {U32.to_nat(U32.from_nat(i)) == i : Nat}

def is_lt_nat source · line 97 · raw

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

def sub_nat source · line 100 · raw

@+a:U32 -> @+b:U32 -> @+e:{Nat.is_le(U32.to_nat(b), U32.to_nat(a)) == True{} : Bool} -> {U32.to_nat(U32.sub(a, b)) == Nat.sub(U32.to_nat(a), U32.to_nat(b)) : Nat}

def WB_unsigned source · line 103 · raw

@+n:Nat -> @+w:Word(n) -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, w), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.scale_binary(n, 1n)) == True{} : Bool}

def shl_bound source · line 114 · raw

@+w:Word(32n) -> @+k:Nat -> @+h:{Nat.is_lt(Nat.double(U32.to_nat(U32{w})), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k)) == True{} : Bool} -> {Nat.is_lt(Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(32n, w)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k)) == True{} : Bool}

def shl_value source · line 118 · raw

@+x:U32 -> @+k:Nat -> @+hk:{Nat.is_le(k, 32n) == True{} : Bool} -> @+h:{Nat.is_lt(Nat.double(U32.to_nat(x)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k)) == True{} : Bool} -> {U32.to_nat(U32.shl(x)) == Nat.double(U32.to_nat(x)) : Nat}

def pad_value source · line 125 · raw

@+n:Nat -> @+w:Word(n) -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(1n+n, Word.shr.pad(n, w)) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, w) : Nat}

def low_bit source · line 136 · raw

@x:U32 -> Bool

def shr_split source · line 143 · raw

@+x:U32 -> {U32.to_nat(x) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(low_bit(x)), Nat.double(U32.to_nat(U32.shr(x)))) : Nat}

def pow2u source · line 154 · raw

@d:Nat -> U32

2^d as the U32 built by Base Array.size (1, then shl per level).

def pow2u_shl_bound source · line 161 · raw

@+p:Nat -> @+ih:{U32.to_nat(pow2u(p)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(p) : Nat} -> {Nat.is_lt(Nat.double(U32.to_nat(pow2u(p))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(2n+p)) == True{} : Bool}

def pow2u_value source · line 165 · raw

@+d:Nat -> @+h:{Nat.is_lt(d, 32n) == True{} : Bool} -> {U32.to_nat(pow2u(d)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(d) : Nat}

def shr_pow2u source · line 175 · raw

@+p:Nat -> @+h:{Nat.is_lt(1n+p, 32n) == True{} : Bool} -> {U32.shr(pow2u(1n+p)) == pow2u(p) : U32}

def and_true source · line 186 · raw

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

def lt_one_zero source · line 193 · raw

@+v:Nat -> @+e:{Nat.is_lt(v, 1n) == True{} : Bool} -> {v == 0n : Nat}

def and_low_prev source · line 200 · raw

@d:Nat -> Nat

def and_low_hy source · line 207 · raw

@+m:Nat -> @+d:Nat -> @+yb:Bool -> @+yt:Word(m) -> @+hy:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(yb), Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(m, yt))) == Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(d), 1n) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(m, yt) == Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(and_low_prev(d)), 1n) : Nat}

def and_low_hyb source · line 214 · raw

@+m:Nat -> @+d:Nat -> @+yb:Bool -> @+yt:Word(m) -> @+hy:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(yb), Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(m, yt))) == Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(d), 1n) : Nat} -> {yb == Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/nat.is_zero(d)) : Bool}

def and_low_hx source · line 221 · raw

@+m:Nat -> @+d:Nat -> @+xb:Bool -> @+xt:Word(m) -> @+hx:{Nat.is_lt(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(xb), Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(m, xt))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(d)) == True{} : Bool} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(m, xt), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(and_low_prev(d))) == True{} : Bool}

def and_low_hxb source · line 229 · raw

@+m:Nat -> @+xb:Bool -> @+xt:Word(m) -> @+hx:{Nat.is_lt(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(xb), Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(m, xt))), 1n) == True{} : Bool} -> {xb == False{} : Bool}

def and_low_step source · line 232 · raw

@+m:Nat -> @+d:Nat -> @+xb:Bool -> @+xt:Word(m) -> @+yb:Bool -> @+yt:Word(m) -> @+hy:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(yb), Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(m, yt))) == Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(d), 1n) : Nat} -> @+hx:{Nat.is_lt(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(xb), Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(m, xt))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(d)) == True{} : Bool} -> @+ih:{Word.and(m, xt, yt) == xt : Word(m)} -> {WCon{Bool.and(xb, yb), Word.and(m, xt, yt)} == WCon{xb, xt} : Word(1n+m)}

def and_low source · line 245 · raw

@+n:Nat -> @+d:Nat -> @+x:Word(n) -> @+y:Word(n) -> @+hy:{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, y) == Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(d), 1n) : Nat} -> @+hx:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(d)) == True{} : Bool} -> {Word.and(n, x, y) == x : Word(n)}

def mask_hx source · line 256 · raw

@+wx:Word(32n) -> @+d:Nat -> @+hx:{Nat.is_lt(U32.to_nat(U32{wx}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(d)) == True{} : Bool} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(32n, wx), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(d)) == True{} : Bool}

def mask_word source · line 260 · raw

@+x:U32 -> @+y:U32 -> @+d:Nat -> @+hy:{U32.to_nat(y) == Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(d), 1n) : Nat} -> @+hx:{Nat.is_lt(U32.to_nat(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(d)) == True{} : Bool} -> {U32.and(x, y) == x : U32}

def one_le_pow2u source · line 269 · raw

@+d:Nat -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> {Nat.is_le(U32.to_nat(1), U32.to_nat(pow2u(d))) == True{} : Bool}

Base Array masks every index with size - 1; below the size this is the identity.

def mask_pow2u source · line 273 · raw

@+x:U32 -> @+d:Nat -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hx:{Nat.is_lt(U32.to_nat(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(d)) == True{} : Bool} -> {U32.and(x, U32.sub(pow2u(d), 1)) == x : U32}

def u32_cmp source · line 280 · raw

@+a:U32 -> @+b:U32 -> {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}

def fin_refl source · line 283 · raw

@+c:Cmp -> @+b:Bool -> @+h:{Cmp.is_eq(c) == True{} : Bool} -> {Cmp.is_eq(Word.cmp.fin(b, b, c)) == True{} : Bool}

def cmp_refl_eq source · line 294 · raw

@+n:Nat -> @+w:Word(n) -> {Cmp.is_eq(Word.cmp(n, w, w)) == True{} : Bool}

def u32_eq_refl source · line 301 · raw

@+x:U32 -> {U32.is_eq(x, x) == True{} : Bool}