~/bend-docscommunity

proofs/math/typed/fixgen.bend checks

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

10 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../src/math/fixed.bend as F
import ../../../spec/math/fixed.bend as SF
import ../../../spec/math/generic.bend as SG
import ../../../src/math/num.bend as NM
import ../../lib/nat.bend as N
import ../../lib/arith.bend as AR
import ../natural/arith.bend as R
import ./width.bend as WW

Definitions

def bnot_eq source · line 19 · raw

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

def top_ok source · line 44 · raw

@+w:Nat -> @+t:Nat -> @+h1:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(w, t) == True{} : Bool} -> @+h2:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(w, 1n+t) == False{} : Bool} -> {Bool.and(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(w, t), Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(w, 1n+t))) == True{} : Bool}

the largest w-bit value: it fits, its successor does not

def add_cancel_r source · line 63 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+e:{Nat.add(a, c) == Nat.add(b, c) : Nat} -> {a == b : Nat}

def fits_sub source · line 69 · raw

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

def rot3 source · line 73 · raw

@+z:Nat -> @+s:Nat -> @+y:Nat -> {Nat.add(Nat.add(z, s), y) == Nat.add(Nat.add(y, z), s) : Nat}

(z + s) + y == (y + z) + s

def wsub source · line 77 · raw

@+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> @+y:Nat -> @+d:Nat -> @+e:{Nat.add(d, y) == Nat.add(x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, one)) : Nat} -> @+hx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, x) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_lt(x, y) == c : Bool} -> {Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, d), y) == Nat.add(x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.bn(c))) : Nat}

d == x - y + 2^k modulo 2^k: its low part plus y is x, plus 2^k when x < y

def low_mod source · line 102 · raw

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

low(k, n) is n mod 2^k

def mod_small source · line 112 · raw

@+k:Nat -> @+n:Nat -> @+pp:Nat -> @+hp:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k) == 1n+pp : Nat} -> @+h:{Nat.is_lt(n, 1n+pp) == True{} : Bool} -> {Nat.mod(n, 1n+pp) == n : Nat}

a value below 2^k is its own low part mod 2^k

def low_add_low source · line 116 · raw

@+k:Nat -> @+x:Nat -> @+y:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, x), y)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, Nat.add(x, y)) : Nat}

the low part absorbs an inner low part: (x mod 2^k + y) mod 2^k

def plus_one source · line 125 · raw

@+x:Nat -> @+t:Nat -> @+y:Nat -> @+M:Nat -> @+S:Nat -> @+h:{Nat.add(y, t) == M : Nat} -> @+hS:{1n+M == S : Nat} -> {Nat.add(Nat.add(Nat.add(x, t), 1n), y) == Nat.add(x, S) : Nat}

((x + t) + 1) + y == x + S when y + t == M and 1 + M == S

def lt1 source · line 134 · raw

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

Templates

template some_of source · line 24 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @+bad:Bool -> @+hb:{bad == False{} : Bool} -> @+r:T -> @+n:Nat -> @+hv:{val(r) == n : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(T, val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.opt(T, bad, r)) == Some{n} : Maybe<&2, Nat>}

template none_of source · line 28 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @+bad:Bool -> @+hb:{bad == True{} : Bool} -> @+r:T -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(T, val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.opt(T, bad, r)) == None{} : Maybe<&2, Nat>}

template chk_fit source · line 34 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @+w:Nat -> @+n:Nat -> @+r:T -> @+bad:Bool -> @+hb:{bad == Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(w, n)) : Bool} -> @+hv:{val(r) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(w, n) : Nat} -> @+ok:Bool -> @+hok:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(w, n) == ok : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(T, val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.opt(T, bad, r)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.keep(ok, n) : Maybe<&2, Nat>}

the result r is low(w, n) and bad says n does not fit: Some n exactly when n fits

template sat_fit source · line 49 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @+w:Nat -> @+n:Nat -> @+r:T -> @+top:T -> @+bad:Bool -> @+hb:{bad == Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(w, n)) : Bool} -> @+hv:{val(r) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(w, n) : Nat} -> @+ht:{Bool.and(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(w, val(top)), Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(w, 1n+val(top)))) == True{} : Bool} -> @+ok:Bool -> @+hok:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(w, n) == ok : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.saturated(w, n, val(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.pick(T, bad, top, r)), ok) == True{} : Bool}

template bad_res source · line 142 · raw

@-T:Data -> @-of:(@_:Nat -> T) -> @+w:Nat -> @+n:Nat -> @+r:Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, T> -> @+hr:{r == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.checked(T, of, w, n) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, T>} -> @+ok:Bool -> @+hok:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(w, n) == ok : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.res_bad(T, r) == Bool.not(ok) : Bool}

and it failed exactly when n does not fit