~/bend-docscommunity

proofs/containers/dynamic_array/state.bend checks

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

11 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 ./layout.bend as LY
import ../../../src/containers/types/dynamic_array.bend as E

Types

type Shadow source · line 16 · raw

@-T:Data -> Data

Definitions

def real source · line 19 · raw

@-T:Data -> @sh:Shadow<T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>

def good source · line 25 · raw

@-T:Data -> @sh:Shadow<T> -> Bool

Representation invariant.

def model source · line 30 · raw

@-T:Data -> @sh:Shadow<T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>

def abs source · line 37 · raw

@-T:Data -> @da:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>

Abstraction of an actual dynamic array (proof-level; reads the Base.Array tree through AR.freeze).

def abs_real source · line 42 · raw

@-T:Data -> @+sh:Shadow<T> -> {abs(T, real(T, sh)) == model(T, sh) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>}

def Inv source · line 49 · raw

@-T:Data -> @da:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T> -> Type

Invariant of an actual array: it is the realization of a good shadow.

def g_limit source · line 54 · raw

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

def g_rest1 source · line 57 · raw

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

def g_depth source · line 60 · raw

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

def g_rest2 source · line 63 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+g:{good(T, Sh{l, d, n, t}) == True{} : Bool} -> {Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, T>, d, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/layout.lay(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, t), n)) == True{} : Bool}

def g_perfect source · line 66 · raw

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

def g_lay source · line 69 · raw

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

def good_intro source · line 72 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+a:{Nat.is_le(l, 31n) == True{} : Bool} -> @+b:{Nat.is_le(d, l) == True{} : Bool} -> @+c:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, T>, d, t) == True{} : Bool} -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/layout.lay(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, t), n) == True{} : Bool} -> {good(T, Sh{l, d, n, t}) == True{} : Bool}

def lt32 source · line 79 · raw

@+d:Nat -> @+l:Nat -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> {Nat.is_lt(d, 32n) == True{} : Bool}

def le32 source · line 82 · raw

@+d:Nat -> @+l:Nat -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> {Nat.is_le(d, 32n) == True{} : Bool}

def pow2_src source · line 85 · raw

@+d:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.pow2(d) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d) : Nat}

def slot_item source · line 92 · raw

@-T:Data -> @+m:Maybe<&2, T> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.slot_result(T, m) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.item_result(T, m) : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>}

def empty_eq source · line 99 · raw

@-T:Data -> @+d:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.empty_slots(T, d) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(Maybe<&2, T>, d, None{})) : Array<Maybe<&2, T>>}

def grown_eq source · line 102 · raw

@-T:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.grown(T, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, t)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TNode{t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(Maybe<&2, T>, d, None{})}) : Array<Maybe<&2, T>>}

def slots_grown source · line 106 · raw

@-T:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TNode{t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(Maybe<&2, T>, d, None{})}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.replicate(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), None{})) : List<&2, Maybe<&2, T>>}