proofs/containers/bitset/word.bend checks

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

8 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/bitset.bend as S
import ../../../src/containers/bitset.bend as B
import ./lists.bend as BL

Definitions

def wbits source · line 13 · raw

@n:Nat -> @w:Word(n) -> List<&2, Bool>

def ubits source · line 22 · raw

@x:U32 -> List<&2, Bool>

def len_wbits source · line 27 · raw

@+n:Nat -> @+w:Word(n) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, wbits(n, w)) == n : Nat}

def ulen source · line 36 · raw

@+x:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, ubits(x)) == 32n : Nat}

def w_or source · line 43 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> {wbits(n, Word.or(n, a, b)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.zipk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.KOr{}, wbits(n, a), wbits(n, b)) : List<&2, Bool>}

def w_and source · line 52 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> {wbits(n, Word.and(n, a, b)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.zipk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.KAnd{}, wbits(n, a), wbits(n, b)) : List<&2, Bool>}

def w_diff source · line 61 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> {wbits(n, Word.and(n, a, Word.not(n, b))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.zipk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.KDiff{}, wbits(n, a), wbits(n, b)) : List<&2, Bool>}

def w_xor source · line 70 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> {wbits(n, Word.xor(n, a, b)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.zipk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.KXor{}, wbits(n, a), wbits(n, b)) : List<&2, Bool>}

def u_op source · line 79 · raw

@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+a:U32 -> @+b:U32 -> {ubits(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_op(k, a, b)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.zipk(k, ubits(a), ubits(b)) : List<&2, Bool>}

def and_zero source · line 92 · raw

@+n:Nat -> @+t:Word(n) -> {Word.and(n, t, Word.zero(n)) == Word.zero(n) : Word(n)}

def low_word source · line 107 · raw

@+b:Bool -> @+t:Word(31n) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.low(U32{WCon{b, t}}) == b : Bool}

def low_nth source · line 116 · raw

@+x:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Bool, ubits(x), 0n) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.low(x)} : Maybe<&2, Bool>}

def pad source · line 126 · raw

@+n:Nat -> @+w:Word(n) -> {wbits(1n+n, Word.shr.pad(n, w)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(Bool, wbits(n, w), False{}) : List<&2, Bool>}

def u_shr source · line 137 · raw

@+b:Bool -> @+t:Word(31n) -> {ubits(U32.shr(U32{WCon{b, t}})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(Bool, wbits(31n, t), False{}) : List<&2, Bool>}

def shr_nth source · line 140 · raw

@+x:U32 -> @+j:Nat -> @+h:{Nat.is_lt(j, 31n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Bool, ubits(U32.shr(x)), j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Bool, ubits(x), 1n+j) : Maybe<&2, Bool>}

def shrn_nth source · line 149 · raw

@+k:Nat -> @+x:U32 -> @+j:Nat -> @+h:{Nat.is_lt(Nat.add(j, k), 32n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Bool, ubits(U32.shrn(x, k)), j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Bool, ubits(x), Nat.add(j, k)) : Maybe<&2, Bool>}

def word_get source · line 161 · raw

@+w:U32 -> @+k:Nat -> @+h:{Nat.is_lt(k, 32n) == True{} : Bool} -> {Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_get(w, k)} == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Bool, ubits(w), k) : Maybe<&2, Bool>}

def shl_put source · line 166 · raw

@+n:Nat -> @+c:Bool -> @+w:Word(n) -> {wbits(n, Word.shl.put(n, c, w)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, c <> wbits(n, w), n) : List<&2, Bool>}

def u_shl source · line 175 · raw

@+x:U32 -> {ubits(U32.shl(x)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, False{} <> ubits(x), 32n) : List<&2, Bool>}

def onehot source · line 183 · raw

@+k:Nat -> @+h:{Nat.is_lt(k, 32n) == True{} : Bool} -> {ubits(U32.shln(1, k)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.rep(32n), k, True{}) : List<&2, Bool>}

1 << k is the one-hot mask for bit k.

def word_put source · line 193 · raw

@+v:Bool -> @+w:U32 -> @+k:Nat -> @+h:{Nat.is_lt(k, 32n) == True{} : Bool} -> {ubits(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_put(v, w, k)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, ubits(w), k, v) : List<&2, Bool>}

def word_count source · line 208 · raw

@+m:Nat -> @+x:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_count(m, x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.count(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, ubits(x), m)) : Nat}

def word_members source · line 227 · raw

@+m:Nat -> @+x:U32 -> @+off:Nat -> @+rest:List<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_members(m, x, off, rest) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.members(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, ubits(x), m), off), rest) : List<&2, Nat>}