~/bend-docscommunity

proofs/containers/bitset/walk.bend checks

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

7 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../../spec/lib/common.bend as SC
import ../../../src/containers/bitset.bend as B
import ./model.bend as MD
import ./index.bend as IX

Definitions

def nthw source · line 18 · raw

@ws:List<&2, U32> -> @q:Nat -> U32

Word q of the list (0 beyond the end; the callers always stay in range).

def shrn_zero source · line 27 · raw

@+k:Nat -> {U32.shrn(0, k) == 0 : U32}

def word_get_zero source · line 35 · raw

@+k:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_get(0, k) == False{} : Bool}

def get_case source · line 41 · raw

@+w:U32 -> @+t:List<&2, U32> -> @+i:Nat -> @b:Bool -> @+eb:{Nat.is_lt(i, 32n) == b : Bool} -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.get_walk(t, Nat.sub(i, 32n)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_get(nthw(t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.wordix(Nat.sub(i, 32n))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bitix(Nat.sub(i, 32n))) : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.get_pick(b, w, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.get_walk(t, Nat.sub(i, 32n))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_get(nthw(w <> t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.wordix(i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bitix(i)) : Bool}

def get_index source · line 52 · raw

@ws:List<&2, U32> -> @+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.get_walk(ws, i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_get(nthw(ws, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.wordix(i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bitix(i)) : Bool}

def put_case source · line 61 · raw

@+v:Bool -> @+w:U32 -> @+t:List<&2, U32> -> @+i:Nat -> @b:Bool -> @+eb:{Nat.is_lt(i, 32n) == b : Bool} -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.put_walk(t, Nat.sub(i, 32n), v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.wordix(Nat.sub(i, 32n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_put(v, nthw(t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.wordix(Nat.sub(i, 32n))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bitix(Nat.sub(i, 32n)))) : List<&2, U32>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.put_pick(b, v, w, i, t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.put_walk(t, Nat.sub(i, 32n), v)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, w <> t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.wordix(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_put(v, nthw(w <> t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.wordix(i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bitix(i))) : List<&2, U32>}

def put_index source · line 75 · raw

@ws:List<&2, U32> -> @+i:Nat -> @+v:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.put_walk(ws, i, v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, ws, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.wordix(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_put(v, nthw(ws, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.wordix(i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bitix(i))) : List<&2, U32>}

def nthw_nth source · line 84 · raw

@ws:List<&2, U32> -> @q:Nat -> @+h:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ws)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(U32, ws, q) == Some{nthw(ws, q)} : Maybe<&2, U32>}