~/bend-docscommunity

proofs/containers/dynamic_array/steps.bend checks

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

14 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL
import ../../lib/u32.bend as U
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 ./growth.bend as GR
import ./walk.bend as W

Definitions

def StepOK source · line 18 · raw

@-T:Data -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T> -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T> -> Type

One actual public operation on a good shadow's array yields the array of a new good shadow, and (abstract state, observation) equals the spec step.

def length_ok source · line 21 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> StepOK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Length{})

def capacity_ok source · line 27 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> StepOK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Capacity{})

def n_le_cap source · line 34 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> {Nat.is_le(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool}

def idx_lt source · line 37 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+i:Nat -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {Nat.is_lt(U32.to_nat(U32.from_nat(i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool}

def idx_slot source · line 40 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+i:Nat -> @+x:Maybe<&2, T> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, t), i) == Some{x} : Maybe<&2, Maybe<&2, T>>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, t), U32.to_nat(U32.from_nat(i))) == Some{x} : Maybe<&2, Maybe<&2, T>>}

def get_case source · line 45 · raw

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

def get_ok source · line 66 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+i:Nat -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> StepOK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Get{i})

def set_arr source · line 71 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+i:Nat -> @+w:Maybe<&2, T> -> @+x:Maybe<&2, T> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, t), i) == Some{x} : Maybe<&2, Maybe<&2, T>>} -> {Array.set(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, t), U32.from_nat(i), w) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(Maybe<&2, T>, d, t, i, w)) : Array<Maybe<&2, T>>}

def swap_arr source · line 75 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+i:Nat -> @+w:Maybe<&2, T> -> @+x:Maybe<&2, T> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, t), i) == Some{x} : Maybe<&2, Maybe<&2, T>>} -> {Array.swap(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, t), U32.from_nat(i), w) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(Maybe<&2, T>, d, t, i, w)), x) : Pair(Array<Maybe<&2, T>>, Maybe<&2, T>)}

def upd_slots source · line 80 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+i:Nat -> @+w:Maybe<&2, T> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(Maybe<&2, T>, d, t, i, w)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, t), i, w) : List<&2, Maybe<&2, T>>}

slots of an updated tree (index below the capacity).

def set_case source · line 85 · raw

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

def set_ok source · line 118 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+i:Nat -> @+v:T -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> StepOK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Set{i, v})

def len_slots source · line 123 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> @+hn:{Nat.is_lt(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {Nat.is_lt(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, t))) == True{} : Bool}

def pi_arr source · line 126 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+v:T -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> @+hn:{Nat.is_lt(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {Array.set(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, t), U32.from_nat(n), Some{v}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(Maybe<&2, T>, d, t, n, Some{v})) : Array<Maybe<&2, T>>}

def pi_good source · line 129 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+v:T -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> @+hn:{Nat.is_lt(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, 1n+n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(Maybe<&2, T>, d, t, n, Some{v})}) == True{} : Bool}

def pi_model source · line 135 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+v:T -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> @+hn:{Nat.is_lt(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/layout.somes(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(Maybe<&2, T>, d, t, n, Some{v}))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/layout.somes(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, t)), v) : List<&2, T>}

def room_nat source · line 141 · raw

@+n:Nat -> @+d:Nat -> @+b:Bool -> @+e:{Nat.is_lt(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == b : Bool} -> {Nat.is_lt(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == b : Bool}

def push_case source · line 144 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+v:T -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> @+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} -> StepOK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Push{v})

def push_ok source · line 192 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+v:T -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> StepOK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Push{v})

def pop_spec source · line 197 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+m:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs) == 1n+m : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.pop(T, l, d, xs) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.M{l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(T, xs)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.OItem{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.item_result(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(T, xs, m))}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>)}

def pop_ok source · line 205 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> StepOK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Pop{})

def clear_ok source · line 233 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> StepOK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Clear{})

def to_list_ok source · line 246 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> StepOK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.ToList{})

def feasible_fuel source · line 270 · raw

@+l:Nat -> @+d:Nat -> @+k:Nat -> @+hdl:{Nat.is_le(d, l) == True{} : Bool} -> @+hp:{Nat.is_le(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(l)) == True{} : Bool} -> {Nat.is_le(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(Nat.add(d, Nat.sub(l, d)))) == True{} : Bool}

def spec_fuel source · line 273 · raw

@+d:Nat -> @+k:Nat -> {Nat.is_le(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(Nat.add(d, k))) == True{} : Bool}

def reserve_case source · line 276 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+k:Nat -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> @+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} -> StepOK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Reserve{k})

def reserve_ok source · line 317 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+k:Nat -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> StepOK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Reserve{k})

def step_ok source · line 322 · 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} -> StepOK(T, sh, op)