proofs/containers/bitset/proof.bend checks

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

17 imports

import Base
import ../../lib/array.bend as A
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/bitset.bend as S
import ../../../src/containers/bitset.bend as B
import ../../../src/containers/types/bitset.bend as E
import ./lists.bend as BL
import ./word.bend as W
import ./index.bend as IX
import ./depth.bend as DP
import ./arr.bend as AR
import ./state.bend as ST
import ./steps.bend as BS
import ./trace.bend as BT
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL

Definitions

def capacity source · line 40 · raw

@+n:Nat -> Type

def new_abs source · line 43 · 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} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.model(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/trace.initial(n)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.new(n) : List<&2, Bool>}

def new_inv source · line 46 · 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} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.good(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/trace.initial(n)) == True{} : Bool}

def new_real source · line 49 · raw

@+n:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.new(n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/trace.initial(n)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset}

def from_bools source · line 52 · raw

@+ys:List<&2, Bool> -> @+hf:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bool_count(ys), Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.depth_for(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bool_count(ys))), 32n)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/steps.FromOK(ys)

def step_ok source · line 55 · raw

@sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.good(sh) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/steps.StepOK(sh, op)

def shadow_unique source · line 61 · raw

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

A runtime bitset determines its shadow, so "the operation lands on the array of THIS shadow, whose model is the spec's" pins the abstract state: the laws above cannot be satisfied by naming a different shadow.

def trace_new source · line 65 · raw

@+n:Nat -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op> -> @+h:{Nat.is_le(n, Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.depth_for(n)), 32n)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/trace.TraceOK(ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/trace.initial(n))

Arbitrary finite operation traces from the real constructor.

def Impl source · line 71 · raw

@sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op -> @Post:(@_:Pair(List<&2, Bool>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs) -> Type) -> Type

---- the implementation ----

def impl_of source · line 74 · raw

@-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op -> @-Post:(@_:Pair(List<&2, Bool>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs) -> Type) -> @k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/steps.StepOK(sh, op) -> @pf:Post(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.step(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.model(sh), op)) -> Impl(sh, op, Post)

def impl source · line 79 · raw

@sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.good(sh) == True{} : Bool} -> @-Post:(@_:Pair(List<&2, Bool>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs) -> Type) -> @pf:Post(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.step(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.model(sh), op)) -> Impl(sh, op, Post)

def succ_ne_zero source · line 83 · raw

@+a:Nat -> @+e:{1n+a == 0n : Nat} -> Empty

---- arithmetic and Boolean facts ----

def zero_ne_succ source · line 86 · raw

@+a:Nat -> @+e:{0n == 1n+a : Nat} -> Empty

def succ_pick source · line 89 · raw

@+b:Bool -> @+x:Nat -> @+y:Nat -> {1n+Bool.pick(Nat, b, x, y) == Bool.pick(Nat, b, 1n+x, 1n+y) : Nat}

def zero_add source · line 96 · raw

@+n:Nat -> {Nat.add(0n, n) == n : Nat}

def succ_add source · line 99 · raw

@+a:Nat -> @+b:Nat -> {Nat.add(1n+a, b) == Nat.add(a, 1n+b) : Nat}

def inset_nth source · line 105 · raw

@+xs:List<&2, Bool> -> @+k:Nat -> @+b:Bool -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Bool, xs, k) == Some{b} : Maybe<&2, Bool>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.inset(xs, k) == b : Bool}

---- Contains ----

def gr_y source · line 109 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> @+y:Maybe<&2, Bool> -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Bool, xs, i) == y : Maybe<&2, Bool>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.ob(xs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Get{i}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.OBit{Done{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.inset(xs, i)}} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs}

def get_result source · line 117 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Contains.get_result(xs, i, h)

def get_frame source · line 120 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Contains.get_frame(xs, i)

def get_outside source · line 123 · raw

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

def count_result source · line 128 · raw

@+xs:List<&2, Bool> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Length.count_result(xs)

---- Length (the member count), Capacity (the universe) ----

def count_frame source · line 131 · raw

@+xs:List<&2, Bool> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Length.count_frame(xs)

def length_result source · line 134 · raw

@+xs:List<&2, Bool> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Capacity.length_result(xs)

def length_frame source · line 137 · raw

@+xs:List<&2, Bool> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Capacity.length_frame(xs)

def new_contains source · line 141 · raw

@+n:Nat -> @+k:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Empty_Set.new_contains(n, k)

---- Empty_Set: no member, Length 0, over the universe [0, n) ----

def new_count source · line 150 · raw

@+n:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Empty_Set.new_count(n)

def new_length source · line 157 · raw

@+n:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Empty_Set.new_length(n)

def assign_is source · line 161 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+v:Bool -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> @+y:Maybe<&2, Bool> -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Bool, xs, i) == y : Maybe<&2, Bool>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.assign(xs, i, v) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, xs, i, v), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.OUnit{Done{Unit{}}}) : Pair(List<&2, Bool>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs)}

---- the update of one bit ----

def inset_update_same source · line 169 · raw

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

def inset_update_other source · line 172 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+j:Nat -> @+v:Bool -> @+ne:{Nat.is_eq(i, j) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.inset(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, xs, i, v), j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.inset(xs, j) : Bool}

def cu_set source · line 176 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.count(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, xs, i, True{})) == Bool.pick(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.inset(xs, i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.count(xs), 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.count(xs)) : Nat}

count after setting a bit: one more unless it was set

def cu_clear source · line 191 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.count(xs) == Bool.pick(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.inset(xs, i), 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.count(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, xs, i, False{})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.count(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, xs, i, False{}))) : Nat}

count after clearing a bit: one less if it was set

def set_model source · line 206 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.nx(xs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Set{i}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, xs, i, True{}) : List<&2, Bool>}

---- Include / Insert (set) ----

def set_contains source · line 210 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Include.set_contains(xs, i, h)

def set_others source · line 214 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> @+j:Nat -> @+ne:{Nat.is_eq(i, j) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Include.set_others(xs, i, h, j, ne)

def set_universe source · line 218 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Include.set_universe(xs, i, h)

def set_outside source · line 222 · raw

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

def clear_model source · line 227 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.nx(xs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Clear{i}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, xs, i, False{}) : List<&2, Bool>}

---- Exclude / Delete (clear) ----

def clear_contains source · line 231 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Exclude.clear_contains(xs, i, h)

def clear_others source · line 235 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> @+j:Nat -> @+ne:{Nat.is_eq(i, j) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Exclude.clear_others(xs, i, h, j, ne)

def clear_universe source · line 239 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Exclude.clear_universe(xs, i, h)

def clear_outside source · line 243 · raw

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

def set_count source · line 248 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Include.set_count(xs, i, h)

Include: one more member unless it was one (Insert's Pre: it was not)

def clear_count source · line 253 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Exclude.clear_count(xs, i, h)

Exclude: one member less if it was one (Delete's Pre: it was)

def union_pt source · line 258 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+k:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, ys) : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.inset(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.zip_or(xs, ys), k) == Bool.or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.inset(xs, k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.inset(ys, k)) : Bool}

---- Union (1180) ----

def union_contains source · line 271 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+k:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, ys) : Nat} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Union.union_contains(xs, ys, k, h)

def union_mismatch source · line 276 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+h:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, ys)) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Union.union_mismatch(xs, ys, h)

def intersection_pt source · line 281 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+k:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, ys) : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.inset(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.zip_and(xs, ys), k) == Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.inset(xs, k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.inset(ys, k)) : Bool}

---- Intersection (1279) ----

def intersection_contains source · line 294 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+k:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, ys) : Nat} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Intersection.intersection_contains(xs, ys, k, h)

def intersection_mismatch source · line 299 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+h:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, ys)) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Intersection.intersection_mismatch(xs, ys, h)

def difference_pt source · line 304 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+k:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, ys) : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.inset(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.zip_diff(xs, ys), k) == Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.inset(xs, k), Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.inset(ys, k))) : Bool}

---- Difference (1340) ----

def difference_contains source · line 317 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+k:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, ys) : Nat} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Difference.difference_contains(xs, ys, k, h)

def difference_mismatch source · line 322 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+h:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, ys)) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Difference.difference_mismatch(xs, ys, h)

def symmetric_difference_pt source · line 327 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+k:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, ys) : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.inset(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.zip_xor(xs, ys), k) == Bool.xor(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.inset(xs, k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.inset(ys, k)) : Bool}

---- Symmetric_Difference (1404) ----

def symmetric_difference_contains source · line 340 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+k:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, ys) : Nat} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Symmetric_Difference.symmetric_difference_contains(xs, ys, k, h)

def xor_mismatch source · line 345 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+h:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, ys)) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Symmetric_Difference.xor_mismatch(xs, ys, h)

def to_list_result source · line 349 · raw

@+xs:List<&2, Bool> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Elements.to_list_result(xs)

def to_list_frame source · line 352 · raw

@+xs:List<&2, Bool> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Elements.to_list_frame(xs)

def members_above source · line 356 · raw

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

no member below the offset

def rel_add source · line 366 · raw

@+off:Nat -> @+p:Nat -> {Nat.add(1n+off, p) == Nat.add(1n+p, off) : Nat}

def ne_add_succ source · line 369 · raw

@+off:Nat -> @+p:Nat -> {Nat.is_eq(off, Nat.add(1n+p, off)) == False{} : Bool}

def members_pt source · line 373 · raw

@+xs:List<&2, Bool> -> @+k:Nat -> @+off:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.nmem(Nat.add(k, off), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.members(xs, off)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.inset(xs, k) : Bool}

the member at relative index k is there exactly when bit k is set

def elements_contains source · line 392 · raw

@+xs:List<&2, Bool> -> @+k:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Elements.elements_contains(xs, k)

def elements_length source · line 397 · raw

@+xs:List<&2, Bool> -> @+off:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.Elements.elements_length(xs, off)

as many elements as members (SPARK: Length (Elements) = Length (Container))