proofs/containers/bitset/state.bend checks

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

13 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 ../../lib/array.bend as A
import ./model.bend as MD
import ./arr.bend as AR
import ./depth.bend as DP
import ./lists.bend as BL
import ./word.bend as W

Types

type Sh source · line 238 · raw

Data

Sh

@len:Nat -> @depth:Nat -> @tree:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> Sh

Definitions

def flat source · line 21 · raw

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

def invf source · line 28 · raw

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

def inv_le source · line 31 · raw

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

def inv_tail source · line 34 · raw

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

def inv_mk source · line 37 · raw

@+n:Nat -> @+xs:List<&2, Bool> -> @+a:{Nat.is_le(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> @+c:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.allf(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(Bool, xs, n)) == True{} : Bool} -> {invf(n, xs) == True{} : Bool}

def length_abs source · line 41 · raw

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

The logical length is len.

def split source · line 45 · raw

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

The stored bits are the logical bits followed by the zero tail.

def take32 source · line 48 · raw

@+w:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/word.ubits(w), 32n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/word.ubits(w) : List<&2, Bool>}

def length_flat_cons source · line 51 · raw

@+w:U32 -> @+t:List<&2, U32> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, flat(w <> t)) == Nat.add(32n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, flat(t))) : Nat}

def get_case source · line 58 · raw

@+w:U32 -> @+t:List<&2, U32> -> @+i:Nat -> @b:Bool -> @+eb:{Nat.is_lt(i, 32n) == b : Bool} -> @+h:{Nat.is_lt(i, Nat.add(32n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, flat(t)))) == True{} : Bool} -> @ih:(@+h2:{Nat.is_lt(Nat.sub(i, 32n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, flat(t))) == True{} : Bool} -> {Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.get_walk(t, Nat.sub(i, 32n))} == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Bool, flat(t), Nat.sub(i, 32n)) : Maybe<&2, Bool>}) -> {Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.get_pick(b, w, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.get_walk(t, Nat.sub(i, 32n)))} == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/word.ubits(w), flat(t)), i) : Maybe<&2, Bool>}

def get_walk source · line 72 · raw

@+ws:List<&2, U32> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, flat(ws))) == True{} : Bool} -> {Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.get_walk(ws, i)} == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Bool, flat(ws), i) : Maybe<&2, Bool>}

def put_case source · line 79 · raw

@+v:Bool -> @+w:U32 -> @+i:Nat -> @+t:List<&2, U32> -> @b:Bool -> @+eb:{Nat.is_lt(i, 32n) == b : Bool} -> @+ih:{flat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.put_walk(t, Nat.sub(i, 32n), v)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, flat(t), Nat.sub(i, 32n), v) : List<&2, Bool>} -> {flat(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(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/word.ubits(w), flat(t)), i, v) : List<&2, Bool>}

def put_walk source · line 94 · raw

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

def zip_words source · line 101 · raw

@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+ws:List<&2, U32> -> @+vs:List<&2, U32> -> {flat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.zip_words(k, ws, vs)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.zipk(k, flat(ws), flat(vs)) : List<&2, Bool>}

def count_words source · line 113 · raw

@+ws:List<&2, U32> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.count_words(ws) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.count(flat(ws)) : Nat}

def members_words source · line 123 · raw

@+ws:List<&2, U32> -> @+off:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.members_words(ws, off) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.members(flat(ws), off) : List<&2, Nat>}

def invf_update source · line 137 · raw

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

def invf_zipk source · line 143 · raw

@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+n:Nat -> @+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+gx:{invf(n, xs) == True{} : Bool} -> @+gy:{invf(n, ys) == True{} : Bool} -> {invf(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.zipk(k, xs, ys)) == True{} : Bool}

def put_abs source · line 150 · raw

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

put_walk as seen through the abstraction.

def put_inv source · line 154 · raw

@+n:Nat -> @+ws:List<&2, U32> -> @+i:Nat -> @+v:Bool -> @+h:{Nat.is_lt(i, n) == True{} : Bool} -> @+g:{invf(n, flat(ws)) == True{} : Bool} -> {invf(n, flat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.put_walk(ws, i, v))) == True{} : Bool}

def rep source · line 162 · raw

@+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> Bool

def abs source · line 165 · raw

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

def rep_depth source · line 168 · raw

@+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+g:{rep(n, d, t) == True{} : Bool} -> {Nat.is_eq(d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.depth_for(n)) == True{} : Bool}

def rep_perfect source · line 171 · raw

@+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+g:{rep(n, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, t) == True{} : Bool}

def rep_invf source · line 175 · raw

@+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+g:{rep(n, d, t) == True{} : Bool} -> {invf(n, flat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(t))) == True{} : Bool}

def rep_mk source · line 179 · raw

@+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+a:{Nat.is_eq(d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.depth_for(n)) == True{} : Bool} -> @+b:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, t) == True{} : Bool} -> @+c:{invf(n, flat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(t))) == True{} : Bool} -> {rep(n, d, t) == True{} : Bool}

def rep_lt source · line 183 · raw

@+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+g:{rep(n, d, t) == True{} : Bool} -> {Nat.is_lt(d, 32n) == True{} : Bool}

def length_flat source · line 190 · raw

@ws:List<&2, U32> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, flat(ws)) == Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ws), 32n) : Nat}

def flat_zeros source · line 198 · raw

@+m:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.allf(flat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.replicate(U32, m, 0))) == True{} : Bool}

def zero_length source · line 205 · raw

@+d:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, flat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.W{0})))) == Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 32n) : Nat}

def zero_allf source · line 210 · raw

@+d:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.allf(flat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.W{0})))) == True{} : Bool}

def new_le source · line 216 · raw

@+n:Nat -> @+h:{Nat.is_le(n, Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.depth_for(n)), 32n)) == True{} : Bool} -> {Nat.is_le(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, flat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.depth_for(n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.W{0}))))) == True{} : Bool}

fits is the documented capacity condition: the depth the representation is allowed to reach (2^31 words = 2^36 bits) must cover n.

def new_rep source · line 220 · raw

@+n:Nat -> @+h:{Nat.is_le(n, Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.depth_for(n)), 32n)) == True{} : Bool} -> {rep(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.depth_for(n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.depth_for(n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.W{0})) == True{} : Bool}

def new_abs source · line 227 · raw

@+n:Nat -> @+h:{Nat.is_le(n, Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.depth_for(n)), 32n)) == True{} : Bool} -> {abs(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.depth_for(n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.W{0})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.new(n) : List<&2, Bool>}

def new_form source · line 231 · raw

@+n:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.new(n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.BS{n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.depth_for(n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.depth_for(n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.W{0}))} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset}

new(n) is that array, thawed.

def real source · line 241 · raw

@sh:Sh -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset

def good source · line 246 · raw

@sh:Sh -> Bool

def model source · line 251 · raw

@sh:Sh -> List<&2, Bool>

def flat_len source · line 257 · 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(Bool, flat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(t))) == Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 32n) : Nat}

The stored bit count is 32 per word.

def rep_fits source · line 262 · raw

@+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+g:{rep(n, d, t) == True{} : Bool} -> {Nat.is_le(n, Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.depth_for(n)), 32n)) == True{} : Bool}

Any bitset satisfying the invariant is within the capacity.

def wordix_go source · line 269 · raw

@m:Nat -> @+i:Nat -> @b:Bool -> @+eb:{Nat.is_lt(i, 32n) == b : Bool} -> @+h:{Nat.is_lt(i, Nat.mul(m, 32n)) == True{} : Bool} -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.wordix(i), m) == True{} : Bool}

A bit index below the logical size addresses a word inside the array.

def wordix_lt source · line 281 · raw

@+i:Nat -> @+m:Nat -> @+h:{Nat.is_lt(i, Nat.mul(m, 32n)) == True{} : Bool} -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.wordix(i), m) == True{} : Bool}

def burn_any source · line 285 · raw

@xs:List<&1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.burn_list(xs) == Unit{} : Unit}

Releasing a bitset is the unit: burn_list consumes any finite list.

def dispose_ok source · line 292 · raw

@+n:Nat -> @+d:Nat -> @t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.dispose(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.BS{n, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, t)}) == Unit{} : Unit}

def blen_go source · line 303 · raw

@+n:Nat -> @u:Unit -> Nat

def blen source · line 308 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset -> Nat

def bdepth source · line 313 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset -> Nat

def btree source · line 318 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd>

def sh_len source · line 323 · raw

@sh:Sh -> Nat

def sh_depth source · line 328 · raw

@sh:Sh -> Nat

def sh_tree source · line 333 · raw

@sh:Sh -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd>

def real_len source · line 338 · raw

@+sh:Sh -> {blen(real(sh)) == sh_len(sh) : Nat}

def real_depth source · line 343 · raw

@+sh:Sh -> {bdepth(real(sh)) == sh_depth(sh) : Nat}

def real_tree source · line 348 · raw

@+sh:Sh -> {btree(real(sh)) == sh_tree(sh) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd>}

def sh_eta source · line 353 · raw

@+sh:Sh -> {sh == Sh{sh_len(sh), sh_depth(sh), sh_tree(sh)} : Sh}

def real_inj_parts source · line 358 · raw

@+a:Sh -> @+b:Sh -> @+e:{real(a) == real(b) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset} -> {Sh{sh_len(a), sh_depth(a), sh_tree(a)} == Sh{sh_len(b), sh_depth(b), sh_tree(b)} : Sh}

def real_inj source · line 367 · raw

@+a:Sh -> @+b:Sh -> @+e:{real(a) == real(b) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset} -> {a == b : Sh}