~/bend-docscommunity

proofs/containers/stack/proof.bend checks

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

9 imports
import Base
import ../../../src/containers/stack.bend as D
import ../../../spec/containers/stack.bend as S
import ../../../spec/lib/common.bend as C
import ../../../src/containers/types/stack.bend as E
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../../spec/lib/sequence.bend as V
import ../../lib/sequence.bend as VL

Definitions

def length_result source · line 53 · raw

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

---- Length, iteration ----

def length_frame source · line 60 · raw

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

def to_list_model source · line 67 · raw

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

def to_list_frame source · line 74 · raw

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

def new_empty source · line 82 · raw

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

---- Empty_Vector ----

def push_length source · line 89 · raw

@-T:Data -> @+xs:List<&2, T> -> @+v:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/stack.Prepend.push_length(T, xs, v)

---- Prepend: Length + 1, Element (First) = New_Item, Range_Shifted (Old, New, First, Last'Old, 1) ----

def push_first source · line 96 · raw

@-T:Data -> @+xs:List<&2, T> -> @+v:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/stack.Prepend.push_first(T, xs, v)

def push_is source · line 103 · raw

@-T:Data -> @+xs:List<&2, T> -> @+v:T -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/stack.nx(T, xs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/stack.Push{v}) == v <> xs : List<&2, T>}

def push_shifted source · line 110 · raw

@-T:Data -> @+xs:List<&2, T> -> @+v:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/stack.Prepend.push_shifted(T, xs, v)

def pop_length source · line 114 · raw

@-T:Data -> @+h:T -> @+t:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/stack.Delete_First.pop_length(T, h, t)

---- Delete_First: Length - 1, Range_Shifted (New, Old, First, Last, 1); pop returns First_Element'Old ----

def pop_shifted source · line 117 · raw

@-T:Data -> @+h:T -> @+t:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/stack.Delete_First.pop_shifted(T, h, t)

def pop_result source · line 120 · raw

@-T:Data -> @+h:T -> @+t:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/stack.Delete_First.pop_result(T, h, t)

def pop_empty source · line 123 · raw

@-T:Data -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/stack.Delete_First.pop_empty(T)

def peek_first source · line 127 · raw

@-T:Data -> @+h:T -> @+t:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/stack.First_Element.peek_first(T, h, t)

---- First_Element: Element (Model, First); nothing changes ----

def peek_frame source · line 130 · raw

@-T:Data -> @+xs:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/stack.First_Element.peek_frame(T, xs)

def peek_empty source · line 137 · raw

@-T:Data -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/stack.First_Element.peek_empty(T)

Templates

template real source · line 13 · raw

@-T:Data -> @+xs:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/stack.Stack<T>

Universal one-step refinement, including cached count preservation and empty errors. Concrete instances in STACK_COMPONENT_PROOF.bend.

template lift source · line 16 · raw

@-T:Data -> @r:Pair(List<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/stack.Obs<T>) -> Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/stack.Stack<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/stack.Obs<T>)

template step_correct source · line 20 · raw

@-T:Data -> @+xs:List<&2, T> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/stack.Op<T> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/stack.step(T, real(T, xs), op) == lift(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/stack.step(T, xs, op)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/stack.Stack<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/stack.Obs<T>)}

template constructor source · line 43 · raw

@-T:Data -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/stack.new(T) == real(T, []) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/stack.Stack<T>}

template impl source · line 49 · raw

@-T:Data -> @+xs:List<&2, T> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/stack.Op<T> -> @-Post:(@_:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/stack.Stack<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/stack.Obs<T>) -> Type) -> @pf:Post(lift(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/stack.step(T, xs, op))) -> Post(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/stack.step(T, real(T, xs), op))

---- the implementation ----

template new_impl source · line 85 · raw

@-T:Data -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/stack.new(T) == real(T, []) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/stack.Stack<T>}