~/bend-docscommunity

proofs/containers/bitset/arr.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/arr.bend as Arr

11 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL
import ../../lib/u32.bend as U
import ../../lib/array.bend as A
import ../../../spec/lib/common.bend as SC
import ../../../src/containers/bitset.bend as B
import ./model.bend as MD
import ./walk.bend as WK
import ./listx.bend as LX

Definitions

def wmap source · line 20 · raw

@xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> List<&2, U32>

def ws source · line 27 · raw

@t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> List<&2, U32>

def nths source · line 32 · raw

@xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @q:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd

Slot q of a word list (the callers always stay in range; the default keeps the function total and agrees with WK.nthw's default).

def wmap_length source · line 43 · raw

@xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, wmap(xs)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, xs) : Nat}

def wmap_update source · line 50 · raw

@xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @q:Nat -> @+v:U32 -> {wmap(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, xs, q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.W{v})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, wmap(xs), q, v) : List<&2, U32>}

def wval_nths source · line 60 · raw

@xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @q:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.wval(nths(xs, q)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/walk.nthw(wmap(xs), q) : U32}

def nths_nth source · line 69 · raw

@xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @q:Nat -> @+h:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, xs, q) == Some{nths(xs, q)} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd>}

def ws_length source · line 80 · raw

@+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ws(t)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d) : Nat}

def slots_lt source · line 84 · raw

@+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+q:Nat -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, t) == True{} : Bool} -> @+hq:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, t))) == True{} : Bool}

def idx_ok source · line 88 · raw

@+d:Nat -> @+q:Nat -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hq:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {U32.to_nat(U32.from_nat(q)) == q : Nat}

def read_ok source · line 93 · raw

@+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+q:Nat -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hq:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.read(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, t), d, q) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/walk.nthw(ws(t), q)) : Pair(Array<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd>, U32)}

def write_ok source · line 105 · raw

@+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+q:Nat -> @+v:U32 -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hq:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.write(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, t), d, q, v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, t, q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.W{v})) : Array<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd>}

def ws_upd source · line 112 · raw

@+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+q:Nat -> @+v:U32 -> @+hq:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, t) == True{} : Bool} -> {ws(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, t, q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.W{v})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, ws(t), q, v) : List<&2, U32>}

def upd_perfect source · line 117 · raw

@+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+q:Nat -> @+v:U32 -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, t, q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.W{v})) == True{} : Bool}

def wmap_replicate source · line 120 · raw

@+m:Nat -> @+v:U32 -> {wmap(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.replicate(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, m, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.W{v})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.replicate(U32, m, v) : List<&2, U32>}

def ws_trep source · line 128 · raw

@+d:Nat -> @+v:U32 -> {ws(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.W{v})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.replicate(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), v) : List<&2, U32>}