~/bend-docscommunity

proofs/containers/bitlist/proof.bend checks

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

14 imports
import Base
import ../../../spec/lib/common.bend as SC
import ../../../src/containers/bitlist.bend as BLI
import ../../../src/containers/types/bitlist.bend as E
import ../../../spec/containers/bitlist.bend as S
import ./state.bend as SS
import ./steps.bend as BS
import ./trace.bend as TR
import ../../lib/list.bend as LL
import ../bitset/lists.bend as BL
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../../spec/lib/sequence.bend as V
import ../../lib/sequence.bend as VL

Definitions

def assign_in source · line 19 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+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/bitlist.assign_at(y, l, c, xs, i, v) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.M{l, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, xs, i, v)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.OUnit{Done{Unit{}}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs)}

---- assign: the written bit reads back, every other bit is unchanged ----

def assign_step source · line 26 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+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/bitlist.step(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.M{l, c, xs}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Assign{i, v}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.M{l, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, xs, i, v)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.OUnit{Done{Unit{}}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs)}

def get_assign_same source · line 29 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+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/bitlist.Replace_Element.get_assign_same(l, c, xs, i, v, h)

def get_assign_other source · line 34 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+i:Nat -> @+j:Nat -> @+v:Bool -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> @+ne:{Nat.is_eq(i, j) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Replace_Element.get_assign_other(l, c, xs, i, j, v, h, ne)

def length_assign source · line 39 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+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/bitlist.Replace_Element.length_assign(l, c, xs, i, v, h)

def nth_snoc_end source · line 43 · raw

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

def pop_snoc source · line 50 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+ys:List<&2, Bool> -> @+b:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.pop(l, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(Bool, ys, b)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.M{l, c, ys}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.OBit{Done{b}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs)}

def push_step source · line 60 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+v:Bool -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.room(l, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.step(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.M{l, c, xs}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Push{v}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.M{l, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(Bool, xs, v)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.OUnit{Done{Unit{}}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs)}

---- push / pop: append one bit, pop returns it and restores the list ----

def length_push source · line 64 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+v:Bool -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.room(l, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Append.length_push(l, c, xs, v, h)

def get_push_last source · line 68 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+v:Bool -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.room(l, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Append.get_push_last(l, c, xs, v, h)

def pop_push source · line 73 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+v:Bool -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.room(l, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Delete_Last.pop_push(l, c, xs, v, h)

def count_push source · line 77 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+v:Bool -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.room(l, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Append.count_push(l, c, xs, v, h)

def room_of source · line 83 · raw

@+c:Nat -> @+xs:List<&2, Bool> -> @+b:Bool -> @+t:List<&2, Bool> -> @+h:{Nat.is_le(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, b <> t)), Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(c), 32n)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.room(None{}, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool}

---- from_bools spells its input ----

def fits_tail source · line 87 · raw

@+c:Nat -> @+xs:List<&2, Bool> -> @+b:Bool -> @+t:List<&2, Bool> -> @+h:{Nat.is_le(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, b <> t)), Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(c), 32n)) == True{} : Bool} -> {Nat.is_le(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(Bool, xs, b)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, t)), Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(c), 32n)) == True{} : Bool}

def push_all_spells source · line 91 · raw

@+bs:List<&2, Bool> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+h:{Nat.is_le(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, bs)), Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(c), 32n)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.push_all(bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.M{None{}, c, xs}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.M{None{}, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Bool, xs, bs)} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model}

def new_real source · line 124 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.new == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/trace.initial(None{})) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.Bitlist}

def new_model source · line 127 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.model(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/trace.initial(None{})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.new : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model}

def with_limit_real source · line 130 · raw

@+n:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.with_limit(n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/trace.initial(Some{n})) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.Bitlist}

def with_limit_model source · line 133 · raw

@+n:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.model(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/trace.initial(Some{n})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.with_limit(n) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model}

def initial_good source · line 136 · raw

@+l:Maybe<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.good(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/trace.initial(l)) == True{} : Bool}

def step_ok source · line 139 · raw

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

def trace_new source · line 142 · raw

@+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/trace.TraceOK(ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/trace.initial(None{}))

def trace_with_limit source · line 145 · raw

@+n:Nat -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/trace.TraceOK(ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/trace.initial(Some{n}))

def from_bools source · line 148 · raw

@+bs:List<&2, Bool> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/trace.FromOK(bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/trace.initial(None{}))

def from_bools_spells source · line 152 · raw

@+bs:List<&2, Bool> -> @+c:Nat -> @+hc:{c == 31n : Nat} -> @+h:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, bs), Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(c), 32n)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.push_all(bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.M{None{}, c, []}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.M{None{}, c, bs} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model}

with room for every bit, the spec's from_bools is exactly the input

def Impl source · line 158 · raw

@sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.Sh -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op -> @Post:(@_:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs) -> Type) -> Type

---- the implementation ----

def impl_of source · line 161 · raw

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

def impl source · line 166 · raw

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

def length_result source · line 170 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Length.length_result(l, c, xs)

---- Length, Capacity (the S.limit), Count, iteration: the value, and nothing changes ----

def length_frame source · line 173 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Length.length_frame(l, c, xs)

def limit_result source · line 176 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Capacity.limit_result(l, c, xs)

def limit_frame source · line 179 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Capacity.limit_frame(l, c, xs)

def count_result source · line 182 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Implementation.count_result(l, c, xs)

def to_list_model source · line 185 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Iteration.to_list_model(l, c, xs)

def to_list_frame source · line 188 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Iteration.to_list_frame(l, c, xs)

def new_empty source · line 192 · raw

0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Empty_Vector.new_empty

---- Empty_Vector, To_Vector ----

def with_limit_empty source · line 195 · raw

@+n:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Empty_Vector.with_limit_empty(n)

def new_impl source · line 198 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.new == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/trace.initial(None{})) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.Bitlist}

def from_bools_model source · line 201 · raw

@+bs:List<&2, Bool> -> @+c:Nat -> @+hc:{c == 31n : Nat} -> @+h:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, bs), Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(c), 32n)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.To_Vector.from_bools_model(bs, c, hc, h)

def clear_length source · line 205 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Clear.clear_length(l, c, xs)

---- Clear: Length 0 (the S.limit is kept) ----

def clear_limit source · line 208 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Clear.clear_limit(l, c, xs)

def get_element source · line 212 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+i:Nat -> @+v:Bool -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Bool, xs, i) == Some{v} : Maybe<&2, Bool>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Element.get_element(l, c, xs, i, v, h)

---- Element ----

def get_frame source · line 216 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+i:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Element.get_frame(l, c, xs, i)

def get_outside source · line 219 · raw

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

def assign_bits source · line 224 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+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/bitlist.bits(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.nx(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.M{l, c, xs}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Assign{i, v})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, xs, i, v) : List<&2, Bool>}

---- Replace_Element: Length kept, Element (Index) = New_Item, Equal_Except elsewhere ----

def assign_length source · line 228 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+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/bitlist.Replace_Element.assign_length(l, c, xs, i, v, h)

def assign_element source · line 231 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+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/bitlist.Replace_Element.assign_element(l, c, xs, i, v, h)

def assign_except source · line 235 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+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/bitlist.Replace_Element.assign_except(l, c, xs, i, v, h)

def assign_outside source · line 238 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+i:Nat -> @+v:Bool -> @+h:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs), i) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Replace_Element.assign_outside(l, c, xs, i, v, h)

def push_bits source · line 243 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+v:Bool -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.room(l, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.bits(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.nx(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.M{l, c, xs}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Push{v})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(Bool, xs, v) : List<&2, Bool>}

---- Append: Length + 1, Equal_Prefix (Model'Old, Model), Element (Last'Old + 1) = New_Item ----

def push_length source · line 247 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+v:Bool -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.room(l, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Append.push_length(l, c, xs, v, h)

def push_prefix source · line 250 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+v:Bool -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.room(l, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Append.push_prefix(l, c, xs, v, h)

def push_element source · line 253 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+v:Bool -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.room(l, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Append.push_element(l, c, xs, v, h)

def push_full source · line 257 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+v:Bool -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.room(l, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Append.push_full(l, c, xs, v, h)

def pop_length source · line 262 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+h:Bool -> @+t:List<&2, Bool> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Delete_Last.pop_length(l, c, h, t)

---- Delete_Last: Length - 1, Equal_Prefix (Model, Model'Old); pop returns Last_Element'Old ----

def pop_prefix source · line 265 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+h:Bool -> @+t:List<&2, Bool> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Delete_Last.pop_prefix(l, c, h, t)

def pop_result source · line 268 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+h:Bool -> @+t:List<&2, Bool> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Delete_Last.pop_result(l, c, h, t)

def pop_empty source · line 272 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Delete_Last.pop_empty(l, c)