~/bend-docscommunity

proofs/containers/deque/proof.bend checks

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

12 imports
import Base
import ../../../spec/containers/deque.bend as S
import ../../../src/containers/deque.bend as DQ
import ../../../src/containers/types/deque.bend as E
import ./state.bend as ST
import ./stepok.bend as K
import ./steps.bend as PS
import ./trace.bend as FT
import ../../lib/logic.bend as L
import ../../../spec/lib/common.bend as SC
import ../../../spec/lib/sequence.bend as V
import ../../lib/sequence.bend as VL

Definitions

def length_result source · line 64 · raw

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

---- Length, iteration ----

def length_frame source · line 67 · raw

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

def to_list_model source · line 70 · raw

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

def to_list_frame source · line 73 · raw

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

def push_front_length source · line 85 · raw

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

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

def push_front_first source · line 88 · raw

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

def push_front_shifted source · line 91 · raw

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

def push_back_length source · line 95 · raw

@-T:Data -> @+xs:List<&2, T> -> @+v:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.Append.push_back_length(T, xs, v)

---- Append: Length + 1, Equal_Prefix (Model'Old, Model), Element (Last'Old + 1) = New_Item ----

def push_back_prefix source · line 98 · raw

@-T:Data -> @+xs:List<&2, T> -> @+v:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.Append.push_back_prefix(T, xs, v)

def push_back_element source · line 101 · raw

@-T:Data -> @+xs:List<&2, T> -> @+v:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.Append.push_back_element(T, xs, v)

def pop_front_length source · line 105 · raw

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

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

def pop_front_shifted source · line 108 · raw

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

def pop_front_result source · line 111 · raw

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

def pop_front_empty source · line 114 · raw

@-T:Data -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.Delete_First.pop_front_empty(T)

def pop_back_length source · line 118 · raw

@-T:Data -> @+h:T -> @+t:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.Delete_Last.pop_back_length(T, h, t)

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

def pop_back_prefix source · line 121 · raw

@-T:Data -> @+h:T -> @+t:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.Delete_Last.pop_back_prefix(T, h, t)

def pop_back_result source · line 124 · raw

@-T:Data -> @+h:T -> @+t:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.Delete_Last.pop_back_result(T, h, t)

def pop_back_empty source · line 128 · raw

@-T:Data -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.Delete_Last.pop_back_empty(T)

def peek_front_first source · line 132 · raw

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

---- First_Element / Last_Element: the end elements; nothing changes ----

def peek_front_frame source · line 135 · raw

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

def peek_front_empty source · line 138 · raw

@-T:Data -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.First_Element.peek_front_empty(T)

def peek_back_last source · line 141 · raw

@-T:Data -> @+h:T -> @+t:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.Last_Element.peek_back_last(T, h, t)

def peek_back_frame source · line 145 · raw

@-T:Data -> @+xs:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.Last_Element.peek_back_frame(T, xs)

def peek_back_empty source · line 148 · raw

@-T:Data -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.Last_Element.peek_back_empty(T)

Templates

template new_abs source · line 29 · raw

@-T:Data -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.initial(T)) == [] : List<&2, T>}

template new_real source · line 32 · raw

@-T:Data -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.new(T) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.initial(T)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.Deque<T>}

template step_ok source · line 35 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Op<T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/stepok.StepOK(T, sh, op)

template shadow_unique source · line 39 · raw

@-T:Data -> @+a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, a) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, b) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.Deque<T>} -> {a == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T>}

a deque determines its shadow

template trace_from source · line 42 · raw

@-T:Data -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Op<T>> -> @+sh0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/trace.TraceOK(T, ops, sh0)

template trace_new source · line 46 · raw

@-T:Data -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Op<T>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/trace.TraceOK(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.initial(T))

arbitrary finite operation traces from the real constructor

template Impl source · line 52 · raw

@-T:Data -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Op<T> -> @Post:(@_:Pair(List<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Obs<T>) -> Type) -> Type

---- the implementation ----

template impl_of source · line 55 · raw

@-T:Data -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Op<T> -> @-Post:(@_:Pair(List<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Obs<T>) -> Type) -> @k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/stepok.StepOK(T, sh, op) -> @pf:Post(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh), op)) -> Impl(T, sh, op, Post)

template impl source · line 60 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Op<T> -> @-Post:(@_:Pair(List<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Obs<T>) -> Type) -> @pf:Post(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh), op)) -> Impl(T, sh, op, Post)

template new_empty source · line 77 · raw

@-T:Data -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.initial(T))) == 0n : Nat}

---- Empty_Vector ----

template new_impl source · line 81 · raw

@-T:Data -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.new(T) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.initial(T)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.Deque<T>}