~/bend-docscommunity

proofs/containers/deque/steps.bend checks

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

11 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL
import ../../../spec/lib/common.bend as SC
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 ./rebalance.bend as RB

Definitions

def pred1 source · line 20 · raw

@-T:Data -> @+x:T -> @+t:List<&2, T> -> @+b:List<&2, T> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.DE{t, b, Nat.sub(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, x <> t), 1n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, b)} == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Sh{t, b}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.Deque<T>}

def pred1b source · line 23 · raw

@-T:Data -> @+f:List<&2, T> -> @+x:T -> @+t:List<&2, T> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.DE{f, t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, f), Nat.sub(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, x <> t), 1n)} == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Sh{f, t}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.Deque<T>}

def model_back source · line 27 · raw

@-T:Data -> @+f:List<&2, T> -> @+x:T -> @+t:List<&2, T> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Sh{f, x <> t}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Sh{f, t}), x) : List<&2, T>}

the model with a nonempty back ends in the back's head

def pop_back_snoc source · line 30 · raw

@-T:Data -> @+ys:List<&2, T> -> @+x:T -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.pop_back(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(T, ys, x)) == (ys, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.OItem{Done{x}}) : Pair(List<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Obs<T>)}

Templates

template Read source · line 17 · raw

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

the result of reading one end of a readied shadow

template pop_front_ready source · line 39 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @+hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/rebalance.rdy_f(T, sh) == True{} : Bool} -> Read(T, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.obs_item(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.pop_front_ready(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, sh))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.pop_front(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh)))

template peek_front_ready source · line 48 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @+hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/rebalance.rdy_f(T, sh) == True{} : Bool} -> Read(T, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.obs_item(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.peek_front_ready(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, sh))), (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.OItem{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.item(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.head(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh)))}))

template pop_back_ready source · line 57 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @+hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/rebalance.rdy_b(T, sh) == True{} : Bool} -> Read(T, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.obs_item(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.pop_back_ready(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, sh))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.pop_back(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh)))

template peek_back_ready source · line 69 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @+hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/rebalance.rdy_b(T, sh) == True{} : Bool} -> Read(T, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.obs_item(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.peek_back_ready(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, sh))), (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.OItem{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.item(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.last(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh)))}))

template op_length source · line 83 · raw

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

template op_push_front source · line 90 · raw

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

template op_push_back source · line 95 · raw

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

template op_to_list source · line 100 · raw

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

template pf_fin source · line 106 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @+sh1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.ready_front(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, sh1) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.Deque<T>} -> @+em:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh1) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh) : List<&2, T>} -> @rd:Read(T, sh1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.obs_item(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.pop_front_ready(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, sh1))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.pop_front(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh1))) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/stepok.StepOK(T, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.PopFront{})

template pf_rf source · line 113 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @rf:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/rebalance.RF(T, sh) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/stepok.StepOK(T, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.PopFront{})

template kf_fin source · line 118 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @+sh1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.ready_front(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, sh1) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.Deque<T>} -> @+em:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh1) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh) : List<&2, T>} -> @rd:Read(T, sh1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.obs_item(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.peek_front_ready(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, sh1))), (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh1), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.OItem{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.item(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.head(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh1)))})) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/stepok.StepOK(T, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.PeekFront{})

template kf_rf source · line 125 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @rf:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/rebalance.RF(T, sh) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/stepok.StepOK(T, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.PeekFront{})

template pb_fin source · line 130 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @+sh1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.ready_back(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, sh1) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.Deque<T>} -> @+em:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh1) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh) : List<&2, T>} -> @rd:Read(T, sh1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.obs_item(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.pop_back_ready(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, sh1))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.pop_back(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh1))) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/stepok.StepOK(T, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.PopBack{})

template pb_rb source · line 137 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @rb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/rebalance.RB(T, sh) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/stepok.StepOK(T, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.PopBack{})

template kb_fin source · line 142 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @+sh1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.ready_back(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, sh1) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.Deque<T>} -> @+em:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh1) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh) : List<&2, T>} -> @rd:Read(T, sh1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.obs_item(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.peek_back_ready(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, sh1))), (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh1), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.OItem{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.item(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.last(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh1)))})) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/stepok.StepOK(T, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.PeekBack{})

template kb_rb source · line 149 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @rb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/rebalance.RB(T, sh) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/stepok.StepOK(T, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.PeekBack{})

template step_ok source · line 155 · 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)

every public operation refines the spec step