~/bend-docscommunity

proofs/containers/dynamic_array/proof.bend checks

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

17 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/list.bend as LL
import ../../lib/nat.bend as N
import ../../lib/array.bend as AR
import ../../../spec/containers/dynamic_array.bend as S
import ../../../src/containers/dynamic_array.bend as DA
import ../../../src/containers/types/dynamic_array.bend as E
import ./state.bend as ST
import ./steps.bend as SP
import ./trace.bend as TR
import ./closed.bend as CL
import ./owned_instances.bend as OWN
import ./owned_swap.bend as OS
import ../../../spec/lib/common.bend as SC
import ../../../spec/lib/sequence.bend as V
import ../../lib/sequence.bend as VL

Definitions

def view source · line 26 · raw

@-T:Data -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>) -> Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>)

def view1 source · line 31 · raw

@-T:Data -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>) -> Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>)

def new_inv source · line 38 · raw

@-T:Data -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new(T))

def new_abs source · line 41 · raw

@-T:Data -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.abs(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new(T)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.new(T) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>}

def limit_good source · line 44 · raw

@-T:Data -> @+k:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/trace.limited(T, k)) == True{} : Bool}

def with_limit_inv source · line 47 · raw

@-T:Data -> @+k:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.with_limit(T, k))

def with_limit_abs source · line 50 · raw

@-T:Data -> @+k:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.abs(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.with_limit(T, k)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.with_limit(T, k) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>}

def step_refines source · line 56 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, sh) == True{} : Bool} -> {view1(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, sh), op)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.abs(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, sh)), op) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>)}

def step_preserves source · line 64 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, sh) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(T, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, sh), op)))

def run_from source · line 70 · raw

@-T:Data -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T>> -> @+sh0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T> -> @+g0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, sh0) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, sh0)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/trace.ro_sh(T, ops, sh0, [], 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/trace.run_ok(T, ops, sh0, [], g0))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/trace.srun_obs(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.model(T, sh0))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>)}

def trace_from source · line 77 · raw

@-T:Data -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T>> -> @+sh0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T> -> @+g0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, sh0) == True{} : Bool} -> {view(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, sh0))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.run(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.model(T, sh0)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>)}

def inv_from source · line 85 · raw

@-T:Data -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T>> -> @+sh0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T> -> @+g0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, sh0) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(T, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, sh0))))

def trace_new source · line 92 · raw

@-T:Data -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T>> -> {view(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new(T))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.run(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.new(T)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>)}

Public trace laws: every finite op list run from DA.new / DA.with_limit through the actual DA.run equals the specification run, and the final array satisfies the invariant.

def trace_new_inv source · line 95 · raw

@-T:Data -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(T, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new(T))))

def trace_with_limit source · line 98 · raw

@-T:Data -> @+k:Nat -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T>> -> {view(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.with_limit(T, k))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.run(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.with_limit(T, k)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>)}

def trace_with_limit_inv source · line 102 · raw

@-T:Data -> @+k:Nat -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(T, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.with_limit(T, k))))

def impl source · line 157 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, sh) == True{} : Bool} -> @-Post:(@_:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>) -> Type) -> @pf:Post(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.abs(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, sh)), op)) -> Post(view1(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, sh), op)))

---- the implementation ---- every Post below is a property of S.step; it holds of DA.step read back through the abstraction (view1), on every good array

def length_result source · line 161 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Length.length_result(T, l, d, xs)

---- Length, Capacity, iteration: the value, and nothing changes ----

def length_frame source · line 164 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Length.length_frame(T, l, d, xs)

def capacity_result source · line 167 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Capacity.capacity_result(T, l, d, xs)

def capacity_frame source · line 170 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Capacity.capacity_frame(T, l, d, xs)

def to_list_model source · line 173 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Iteration.to_list_model(T, l, d, xs)

def to_list_frame source · line 176 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Iteration.to_list_frame(T, l, d, xs)

def new_empty source · line 180 · raw

@-T:Data -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Empty_Vector.new_empty(T)

---- Empty_Vector: Length 0 (the default capacity is 2^0) ----

def new_capacity source · line 183 · raw

@-T:Data -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Empty_Vector.new_capacity(T)

def new_impl source · line 186 · raw

@-T:Data -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.abs(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new(T)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.new(T) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>}

def with_limit_empty source · line 189 · raw

@-T:Data -> @+k:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Empty_Vector.with_limit_empty(T, k)

def with_limit_impl source · line 192 · raw

@-T:Data -> @+k:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.abs(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.with_limit(T, k)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.with_limit(T, k) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>}

def re_c source · line 196 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+n:Nat -> @+c1:Bool -> @+h1:{Nat.is_le(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == c1 : Bool} -> @+c2:Bool -> @+h2:{Nat.is_le(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(l)) == c2 : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.items(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.nx(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.M{l, d, xs}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Reserve{n})) == xs : List<&2, T>}

---- Reserve_Capacity: M.Equal (Model, Model'Old) ----

def reserve_equal source · line 210 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+n:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Reserve_Capacity.reserve_equal(T, l, d, xs, n)

def clear_length source · line 214 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Clear.clear_length(T, l, d, xs)

---- Clear: Length 0 (the capacity is kept) ----

def clear_capacity source · line 217 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Clear.clear_capacity(T, l, d, xs)

def get_element source · line 221 · raw

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

---- Element / First_Element / Last_Element ----

def get_frame source · line 225 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+i:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Element.get_frame(T, l, d, xs, i)

def get_outside source · line 228 · raw

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

def first_element source · line 232 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+h:T -> @+t:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.First_Element.first_element(T, l, d, h, t)

def last_element source · line 235 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Last_Element.last_element(T, l, d, xs)

def set_step source · line 239 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+i:Nat -> @+v:T -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.M{l, d, xs}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Set{i, v}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.M{l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(T, xs, i, v)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.OUnit{Done{Unit{}}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>)}

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

def set_items source · line 243 · raw

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

def set_length source · line 247 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+i:Nat -> @+v:T -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Replace_Element.set_length(T, l, d, xs, i, v, h)

def set_element source · line 251 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+i:Nat -> @+v:T -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Replace_Element.set_element(T, l, d, xs, i, v, h)

def set_except source · line 255 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+i:Nat -> @+v:T -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Replace_Element.set_except(T, l, d, xs, i, v, h)

def set_outside source · line 258 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+i:Nat -> @+v:T -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs)) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Replace_Element.set_outside(T, l, d, xs, i, v, h)

def pi_c source · line 262 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+v:T -> @+c1:Bool -> @+h1:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == c1 : Bool} -> @+c2:Bool -> @+h2:{Nat.is_lt(d, l) == c2 : Bool} -> @+hr:{Bool.or(c1, c2) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.items(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.nx(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.M{l, d, xs}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Push{v})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(T, xs, v) : List<&2, T>}

def push_items source · line 274 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+v:T -> @+hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.room(T, l, d, xs) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.items(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.nx(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.M{l, d, xs}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Push{v})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(T, xs, v) : List<&2, T>}

def push_length source · line 277 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+v:T -> @+hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.room(T, l, d, xs) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Append.push_length(T, l, d, xs, v, hr)

def push_prefix source · line 281 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+v:T -> @+hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.room(T, l, d, xs) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Append.push_prefix(T, l, d, xs, v, hr)

def push_element source · line 284 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+v:T -> @+hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.room(T, l, d, xs) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Append.push_element(T, l, d, xs, v, hr)

def push_full source · line 288 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+v:T -> @+h1:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == False{} : Bool} -> @+h2:{Nat.is_lt(d, l) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Append.push_full(T, l, d, xs, v, h1, h2)

def pop_length source · line 294 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+h:T -> @+t:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Delete_Last.pop_length(T, l, d, h, t)

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

def pop_prefix source · line 297 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+h:T -> @+t:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Delete_Last.pop_prefix(T, l, d, h, t)

def pop_result source · line 300 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+h:T -> @+t:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Delete_Last.pop_result(T, l, d, h, t)

def pop_empty source · line 304 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Delete_Last.pop_empty(T, l, d)

Templates

template new_at_abs source · line 112 · raw

@-T:Data -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.abs(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_at(T)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.new(T) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>}

template new_at_inv source · line 116 · raw

@-T:Data -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_at(T))

template with_limit_at_abs source · line 120 · raw

@-T:Data -> @+k:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.abs(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.with_limit_at(T, k)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.with_limit(T, k) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>}

template step_at_refines source · line 124 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, sh) == True{} : Bool} -> {view1(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step_at(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, sh), op)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.abs(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, sh)), op) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>)}

template step_at_preserves source · line 128 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, sh) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(T, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step_at(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, sh), op)))

template trace_new_at source · line 132 · raw

@-T:Data -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T>> -> {view(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run_at(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_at(T))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.run(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.new(T)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>)}

template trace_new_at_inv source · line 137 · raw

@-T:Data -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(T, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run_at(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_at(T))))

template trace_with_limit_at source · line 142 · raw

@-T:Data -> @+k:Nat -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T>> -> {view(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run_at(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.with_limit_at(T, k))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.run(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.with_limit(T, k)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>)}

template trace_with_limit_at_inv source · line 147 · raw

@-T:Data -> @+k:Nat -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(T, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run_at(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.with_limit_at(T, k))))