~/bend-docscommunity

proofs/containers/bitset/lists.bend checks

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

7 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

Definitions

def bop source · line 13 · raw

@k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @a:Bool -> @b:Bool -> Bool

def zipk source · line 24 · raw

@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @xs:List<&2, Bool> -> @ys:List<&2, Bool> -> List<&2, Bool>

def allf source · line 33 · raw

@xs:List<&2, Bool> -> Bool

def rep source · line 42 · raw

@n:Nat -> List<&2, Bool>

def spec_or source · line 47 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.zip_or(xs, ys) == zipk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.KOr{}, xs, ys) : List<&2, Bool>}

def spec_and source · line 58 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.zip_and(xs, ys) == zipk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.KAnd{}, xs, ys) : List<&2, Bool>}

def spec_diff source · line 69 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.zip_diff(xs, ys) == zipk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.KDiff{}, xs, ys) : List<&2, Bool>}

def spec_xor source · line 80 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.zip_xor(xs, ys) == zipk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.KXor{}, xs, ys) : List<&2, Bool>}

def zipk_nil_r source · line 93 · raw

@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+xs:List<&2, Bool> -> {zipk(k, xs, []) == [] : List<&2, Bool>}

def zipk_append source · line 100 · raw

@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+xs2:List<&2, Bool> -> @+ys2:List<&2, Bool> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, ys) : Nat} -> {zipk(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Bool, xs, xs2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Bool, ys, ys2)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Bool, zipk(k, xs, ys), zipk(k, xs2, ys2)) : List<&2, Bool>}

def take_zipk source · line 111 · raw

@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+n:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, zipk(k, xs, ys), n) == zipk(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, xs, n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, ys, n)) : List<&2, Bool>}

def drop_zipk source · line 122 · raw

@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+n:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(Bool, zipk(k, xs, ys), n) == zipk(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(Bool, xs, n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(Bool, ys, n)) : List<&2, Bool>}

def bop_ff source · line 133 · raw

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

def allf_zipk source · line 144 · raw

@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+hx:{allf(xs) == True{} : Bool} -> @+hy:{allf(ys) == True{} : Bool} -> {allf(zipk(k, xs, ys)) == True{} : Bool}

def length_zipk_le source · line 158 · raw

@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> {Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, zipk(k, xs, ys)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool}

def le_length_zipk source · line 167 · raw

@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+n:Nat -> @+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+hx:{Nat.is_le(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> @+hy:{Nat.is_le(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, ys)) == True{} : Bool} -> {Nat.is_le(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, zipk(k, xs, ys))) == True{} : Bool}

def allf_append source · line 180 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+hx:{allf(xs) == True{} : Bool} -> @+hy:{allf(ys) == True{} : Bool} -> {allf(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Bool, xs, ys)) == True{} : Bool}

def allf_rep source · line 189 · raw

@+n:Nat -> {allf(rep(n)) == True{} : Bool}

def drop_allf source · line 196 · raw

@+xs:List<&2, Bool> -> @+n:Nat -> @+h:{allf(xs) == True{} : Bool} -> {allf(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(Bool, xs, n)) == True{} : Bool}

def take_allf source · line 207 · raw

@+xs:List<&2, Bool> -> @+n:Nat -> @+h:{allf(xs) == True{} : Bool} -> @+hn:{Nat.is_le(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, xs, n) == rep(n) : List<&2, Bool>}

def count_allf source · line 220 · raw

@+xs:List<&2, Bool> -> @+h:{allf(xs) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.count(xs) == 0n : Nat}

def members_allf source · line 229 · raw

@+xs:List<&2, Bool> -> @+off:Nat -> @+h:{allf(xs) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.members(xs, off) == [] : List<&2, Nat>}

def count_append source · line 240 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.count(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Bool, xs, ys)) == Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.count(xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.count(ys)) : Nat}

def members_append source · line 249 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+off:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.members(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Bool, xs, ys), off) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.members(xs, off), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.members(ys, Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs), off))) : List<&2, Nat>}

def count_take_snoc source · line 260 · raw

@+xs:List<&2, Bool> -> @+m:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.count(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(Bool, xs, False{}), m)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.count(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, xs, m)) : Nat}

def members_take_snoc source · line 273 · raw

@+xs:List<&2, Bool> -> @+m:Nat -> @+off:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.members(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(Bool, xs, False{}), m), off) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.members(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, xs, m), off) : List<&2, Nat>}

def take_all source · line 288 · raw

@+xs:List<&2, Bool> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, xs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == xs : List<&2, Bool>}

def take_drop source · line 295 · raw

@+xs:List<&2, Bool> -> @+n:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, xs, n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(Bool, xs, n)) == xs : List<&2, Bool>}

def length_take source · line 304 · raw

@+xs:List<&2, Bool> -> @+n:Nat -> @+h:{Nat.is_le(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, xs, n)) == n : Nat}

def nth_take source · line 315 · raw

@+xs:List<&2, Bool> -> @+n:Nat -> @+i:Nat -> @+h:{Nat.is_lt(i, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, xs, n), i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Bool, xs, i) : Maybe<&2, Bool>}

def take_update source · line 326 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+v:Bool -> @+n:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, xs, i, v), n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, xs, n), i, v) : List<&2, Bool>}

def drop_update source · line 339 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+v:Bool -> @+n:Nat -> @+h:{Nat.is_lt(i, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, xs, i, v), n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(Bool, xs, n) : List<&2, Bool>}

def take_rep_succ source · line 352 · raw

@+m:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, rep(1n+m), m) == rep(m) : List<&2, Bool>}

def take_onehot source · line 360 · raw

@+m:Nat -> @+p:Nat -> @+h:{Nat.is_lt(p, m) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, rep(1n+m), p, True{}), m) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, rep(m), p, True{}) : List<&2, Bool>}

Shifting a one-hot mask up by one position.

def or_rep source · line 369 · raw

@+xs:List<&2, Bool> -> {zipk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.KOr{}, xs, rep(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs))) == xs : List<&2, Bool>}

def diff_rep source · line 378 · raw

@+xs:List<&2, Bool> -> {zipk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.KDiff{}, xs, rep(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs))) == xs : List<&2, Bool>}

def or_onehot source · line 388 · raw

@+xs:List<&2, Bool> -> @+k:Nat -> {zipk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.KOr{}, xs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, rep(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)), k, True{})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, xs, k, True{}) : List<&2, Bool>}

OR with the one-hot mask for k sets bit k.

def diff_onehot source · line 402 · raw

@+xs:List<&2, Bool> -> @+k:Nat -> {zipk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.KDiff{}, xs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, rep(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)), k, True{})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, xs, k, False{}) : List<&2, Bool>}

AND NOT with the one-hot mask for k clears bit k.