~/bend-docscommunity

proofs/containers/dynamic_array/closed.bend checks

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

17 imports
import Base
import ../../../src/math/pow2.bend as P2
import ../../math/pow2/pow2.bend as PT
import ./clear.bend as CLR
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/lib/common.bend as SC
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 ./layout.bend as LY
import ./state.bend as ST
import ./steps.bend as SP
import ./growth.bend as GR
import ./trace.bend as TR

Templates

template gstep_at_case source · line 26 · raw

@-T:Data -> @+k:Nat -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+b:Bool -> @+eb:{Nat.is_le(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.grow_step_at(T, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/growth.sgstep(T, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t})) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>}

template grow_until_at_real source · line 38 · raw

@-T:Data -> @+f:Nat -> @+k:Nat -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.grow_until_at(T, f, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/growth.sgrow(T, f, k, sh)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>}

template grow_until_eq source · line 46 · raw

@-T:Data -> @+f:Nat -> @+k:Nat -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.grow_until_at(T, f, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.grow_until(T, f, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, sh)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>}

template found_eq source · line 52 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+c:Nat -> @+n:Nat -> @r:Pair(Array<Maybe<&2, T>>, Maybe<&2, T>) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.get_found_at(T, l, d, c, n, r) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.get_found(T, l, d, c, n, r) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>)}

template get_eq_case source · line 59 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+i:Nat -> @+b:Bool -> @+eb:{Nat.is_lt(i, n) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step_at(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Get{i}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Get{i}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>)}

template set_eq_case source · line 68 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+i:Nat -> @+v:T -> @+b:Bool -> @+eb:{Nat.is_lt(i, n) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step_at(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Set{i, v}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Set{i, v}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>)}

template push_eq_case source · line 77 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+v:T -> @+room:Bool -> @+er:{Nat.is_lt(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == room : Bool} -> @+grow:Bool -> @+eg:{Nat.is_lt(d, l) == grow : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step_at(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Push{v}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Push{v}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>)}

template pop_eq_case source · line 93 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step_at(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Pop{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Pop{}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>)}

template tl_go_eq source · line 100 · raw

@-T:Data -> @k:Nat -> @acc:List<&2, T> -> @r:Pair(Array<Maybe<&2, T>>, Maybe<&2, T>) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.tl_go_at(T, k, acc, r) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.tl_go(k, T, acc, r) : Pair(Array<Maybe<&2, T>>, List<&2, T>)}

template to_list_eq source · line 107 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step_at(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.ToList{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.ToList{}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>)}

template reserve_eq_case source · line 117 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+k:Nat -> @+fits:Bool -> @+ef:{Nat.is_le(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == fits : Bool} -> @+feas:Bool -> @+ep:{Nat.is_le(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.pow2(l)) == feas : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step_at(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Reserve{k}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Reserve{k}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>)}

template step_eq source · line 134 · 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/src/containers/dynamic_array.step_at(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, sh), op) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, sh), op) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>)}

template run_acc_eq source · line 157 · raw

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

template run_eq source · line 169 · raw

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

template new_eq source · line 174 · raw

@-T:Data -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_at(T) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new(T) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>}

template with_limit_eq source · line 177 · raw

@-T:Data -> @+k:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.with_limit_at(T, k) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.with_limit(T, k) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>}