~/bend-docscommunity

proofs/math/typed/u32.bend checks

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

13 imports
import Base
import ../../../spec/math/generic.bend as SG
import ../../../spec/lib/common.bend as SC
import ../../../src/math/generic.bend as G
import ../../../src/math/instances.bend as I
import ../../../src/math/num.bend as NM
import ../../../src/math/natural.bend as M
import ../../lib/nat.bend as N
import ../../lib/u32.bend as U
import ../../lib/u32div.bend as UD
import ../../lib/lemmas/spec/numeric.bend as S
import ../../lib/words32.bend as W32
import ../../lib/word.bend as WD

Definitions

def min_of_ge source · line 23 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(b, a) == False{} : Bool} -> {Nat.min(a, b) == a : Nat}

def min_of_lt source · line 32 · raw

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

def max_of_lt source · line 41 · raw

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

def max_of_ge source · line 50 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(a, b) == False{} : Bool} -> {Nat.max(a, b) == a : Nat}

def val_lt source · line 64 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk:{k == 32n : Nat} -> @+a:U32 -> {Nat.is_lt(U32.to_nat(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k)) == True{} : Bool}

(one and k stay symbolic, so 2^32 is never expanded)

def le_k source · line 69 · raw

@+k:Nat -> @+hk:{k == 32n : Nat} -> {Nat.is_le(k, 32n) == True{} : Bool}

def round_trip_k source · line 74 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk:{k == 32n : Nat} -> @+a:U32 -> {U32.from_nat(U32.to_nat(a)) == a : U32}

a U32 is the U32 of its value

def round_trip source · line 77 · raw

@+a:U32 -> {U32.from_nat(U32.to_nat(a)) == a : U32}

def abs_identity source · line 82 · raw

@+x:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Abs.identity(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, x)

def min_c source · line 85 · raw

@+a:U32 -> @+b:U32 -> @+c:Bool -> @+hc:{Nat.is_lt(U32.to_nat(b), U32.to_nat(a)) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.pick(U32, c, b, a) == U32.from_nat(Nat.min(U32.to_nat(a), U32.to_nat(b))) : U32}

def min_agrees source · line 94 · raw

@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Min.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, a, b)

def max_c source · line 98 · raw

@+a:U32 -> @+b:U32 -> @+c:Bool -> @+hc:{Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.pick(U32, c, b, a) == U32.from_nat(Nat.max(U32.to_nat(a), U32.to_nat(b))) : U32}

def max_agrees source · line 107 · raw

@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Max.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, a, b)

def true_ne_false source · line 113 · raw

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

def lt_zero_false source · line 116 · raw

@+n:Nat -> {Nat.is_lt(n, 0n) == False{} : Bool}

def pos_ge_one source · line 124 · raw

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

0 < n gives not n < 1

def zero_lt_one source · line 132 · raw

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

not 0 < n gives n < 1

def sign_c source · line 139 · raw

@+x:U32 -> @+c:Bool -> @+hc:{Nat.is_lt(0n, U32.to_nat(x)) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.sign_above(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, x, c) == U32.from_nat(Nat.min(U32.to_nat(x), 1n)) : U32}

def sign_agrees source · line 150 · raw

@+x:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Sign.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, x)

def max_val_c source · line 156 · raw

@+x:U32 -> @+lo:U32 -> @+c:Bool -> @+hc:{Nat.is_lt(U32.to_nat(x), U32.to_nat(lo)) == c : Bool} -> {U32.to_nat(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.pick(U32, c, lo, x)) == Nat.max(U32.to_nat(x), U32.to_nat(lo)) : Nat}

def max_val source · line 164 · raw

@+x:U32 -> @+lo:U32 -> {U32.to_nat(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.max(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, x, lo)) == Nat.max(U32.to_nat(x), U32.to_nat(lo)) : Nat}

the value of max(x, lo) is the larger value

def clamp_c source · line 168 · raw

@+x:U32 -> @+lo:U32 -> @+hi:U32 -> @+c:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.clamp_ok(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, x, lo, hi, c) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.lift(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.clamp_ok(U32.to_nat(x), U32.to_nat(lo), U32.to_nat(hi), c)) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, U32>}

def clamp_agrees source · line 177 · raw

@+x:U32 -> @+lo:U32 -> @+hi:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Clamp.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, x, lo, hi)