proofs/containers/deque/steps.bend
bend-collections-laws-containers@1.0.0.0 · 172 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/spec/containers/deque.bend as S
7import bend-collections-laws-containers@1.0.0.0/src/containers/deque.bend as DQ
8import bend-collections-laws-containers@1.0.0.0/src/containers/types/deque.bend as E
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/state.bend as ST
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/stepok.bend as K
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/rebalance.bend as RB
12
13# Every public deque operation, including the errors (pop/peek on an empty
14# deque: Fail{EmptyDeque}, deque unchanged), refines the spec step.
15
16# the result of reading one end of a readied shadow
17def Read(~T: Data, sh: ST.Shadow<T>, r: DQ.Deque<T> & E.Obs<T>, spec: List<&2, T> & E.Obs<T>) -> Type:
18 Sigma<&1, &1, ST.Shadow<T>, sh2 => Sigma<&1, &1, E.Obs<T>, o => {r == (ST.real(T, sh2), o) : DQ.Deque<T> & E.Obs<T>} & {(ST.model(T, sh2), o) == spec : List<&2, T> & E.Obs<T>}>>
19
20def pred1(-T: Data, +x: T, +t: List<&2, T>, +b: List<&2, T>) -> {DQ.DE{t, b, Nat.sub(SC.length(T, Con{x, t}), 1n), SC.length(T, b)} == ST.real(T, ST.Sh{t, b}) : DQ.Deque<T>}:
21 Equal.cong(Nat, DQ.Deque<T>, z => DQ.DE{t, b, z, SC.length(T, b)}, Nat.sub(1n+SC.length(T, t), 1n), SC.length(T, t), N.sub_zero(SC.length(T, t)))
22
23def pred1b(-T: Data, +f: List<&2, T>, +x: T, +t: List<&2, T>) -> {DQ.DE{f, t, SC.length(T, f), Nat.sub(SC.length(T, Con{x, t}), 1n)} == ST.real(T, ST.Sh{f, t}) : DQ.Deque<T>}:
24 Equal.cong(Nat, DQ.Deque<T>, z => DQ.DE{f, t, SC.length(T, f), z}, Nat.sub(1n+SC.length(T, t), 1n), SC.length(T, t), N.sub_zero(SC.length(T, t)))
25
26# the model with a nonempty back ends in the back's head
27def model_back(-T: Data, +f: List<&2, T>, +x: T, +t: List<&2, T>) -> {ST.model(T, ST.Sh{f, Con{x, t}}) == SC.snoc(T, ST.model(T, ST.Sh{f, t}), x) : List<&2, T>}:
28 LL.append_snoc(T, f, SC.reverse(T, t), x)
29
30def pop_back_snoc(-T: Data, +ys: List<&2, T>, +x: T) -> {S.pop_back(T, SC.snoc(T, ys, x)) == (ys, E.OItem{Done{x}}) : List<&2, T> & E.Obs<T>}:
31 match ys:
32 case Nil{}:
33 {==}
34 case Con{h, t}:
35 %LL.init_snoc(T, Con{h, t}, x) : {S.pop_back(T, SC.snoc(T, Con{h, t}, x)) == (_, E.OItem{Done{x}}) : List<&2, T> & E.Obs<T>}
36 %LL.last_snoc(T, Con{h, t}, x) : {S.pop_back(T, SC.snoc(T, Con{h, t}, x)) == (SC.init(T, SC.snoc(T, Con{h, t}, x)), E.OItem{S.item(T, _)}) : List<&2, T> & E.Obs<T>}
37 {==}
38
39def pop_front_ready(~T: Data, +sh: ST.Shadow<T>, +hr: {RB.rdy_f(T, sh) == True{} : Bool}) -> Read(~T, sh, DQ.obs_item(~T, DQ.pop_front_ready(~T, ST.real(T, sh))), S.pop_front(T, ST.model(T, sh))):
40 match sh:
41 case ST.Sh{Con{x, t}, b}:
42 (ST.Sh{t, b}, (E.OItem{Done{x}}, (Equal.cong(DQ.Deque<T>, DQ.Deque<T> & E.Obs<T>, d => (d, E.OItem{Done{x}}), DQ.DE{t, b, Nat.sub(SC.length(T, Con{x, t}), 1n), SC.length(T, b)}, ST.real(T, ST.Sh{t, b}), pred1(T, x, t, b)), {==})))
43 case ST.Sh{Nil{}, Nil{}}:
44 (ST.Sh{Nil{}, Nil{}}, (E.OItem{Fail{E.EmptyDeque{}}}, ({==}, {==})))
45 case ST.Sh{Nil{}, Con{y, t}}:
46 Empty.absurd(Read(~T, ST.Sh{Nil{}, Con{y, t}}, DQ.obs_item(~T, DQ.pop_front_ready(~T, ST.real(T, ST.Sh{Nil{}, Con{y, t}}))), S.pop_front(T, ST.model(T, ST.Sh{Nil{}, Con{y, t}}))), L.false_true(hr))
47
48def peek_front_ready(~T: Data, +sh: ST.Shadow<T>, +hr: {RB.rdy_f(T, sh) == True{} : Bool}) -> Read(~T, sh, DQ.obs_item(~T, DQ.peek_front_ready(~T, ST.real(T, sh))), (ST.model(T, sh), E.OItem{S.item(T, SC.head(T, ST.model(T, sh)))})):
49 match sh:
50 case ST.Sh{Con{x, t}, b}:
51 (ST.Sh{Con{x, t}, b}, (E.OItem{Done{x}}, ({==}, {==})))
52 case ST.Sh{Nil{}, Nil{}}:
53 (ST.Sh{Nil{}, Nil{}}, (E.OItem{Fail{E.EmptyDeque{}}}, ({==}, {==})))
54 case ST.Sh{Nil{}, Con{y, t}}:
55 Empty.absurd(Read(~T, ST.Sh{Nil{}, Con{y, t}}, DQ.obs_item(~T, DQ.peek_front_ready(~T, ST.real(T, ST.Sh{Nil{}, Con{y, t}}))), (ST.model(T, ST.Sh{Nil{}, Con{y, t}}), E.OItem{S.item(T, SC.head(T, ST.model(T, ST.Sh{Nil{}, Con{y, t}})))})), L.false_true(hr))
56
57def pop_back_ready(~T: Data, +sh: ST.Shadow<T>, +hr: {RB.rdy_b(T, sh) == True{} : Bool}) -> Read(~T, sh, DQ.obs_item(~T, DQ.pop_back_ready(~T, ST.real(T, sh))), S.pop_back(T, ST.model(T, sh))):
58 match sh:
59 case ST.Sh{f, Con{x, t}}:
60 +sp = Equal.trans(List<&2, T> & E.Obs<T>, (ST.model(T, ST.Sh{f, t}), E.OItem{Done{x}}), S.pop_back(T, SC.snoc(T, ST.model(T, ST.Sh{f, t}), x)), S.pop_back(T, ST.model(T, ST.Sh{f, Con{x, t}})),
61 Equal.sym(List<&2, T> & E.Obs<T>, S.pop_back(T, SC.snoc(T, ST.model(T, ST.Sh{f, t}), x)), (ST.model(T, ST.Sh{f, t}), E.OItem{Done{x}}), pop_back_snoc(T, ST.model(T, ST.Sh{f, t}), x)),
62 Equal.cong(List<&2, T>, List<&2, T> & E.Obs<T>, z => S.pop_back(T, z), SC.snoc(T, ST.model(T, ST.Sh{f, t}), x), ST.model(T, ST.Sh{f, Con{x, t}}), Equal.sym(List<&2, T>, ST.model(T, ST.Sh{f, Con{x, t}}), SC.snoc(T, ST.model(T, ST.Sh{f, t}), x), model_back(T, f, x, t))))
63 (ST.Sh{f, t}, (E.OItem{Done{x}}, (Equal.cong(DQ.Deque<T>, DQ.Deque<T> & E.Obs<T>, d => (d, E.OItem{Done{x}}), DQ.DE{f, t, SC.length(T, f), Nat.sub(SC.length(T, Con{x, t}), 1n)}, ST.real(T, ST.Sh{f, t}), pred1b(T, f, x, t)), sp)))
64 case ST.Sh{Nil{}, Nil{}}:
65 (ST.Sh{Nil{}, Nil{}}, (E.OItem{Fail{E.EmptyDeque{}}}, ({==}, {==})))
66 case ST.Sh{Con{y, t}, Nil{}}:
67 Empty.absurd(Read(~T, ST.Sh{Con{y, t}, Nil{}}, DQ.obs_item(~T, DQ.pop_back_ready(~T, ST.real(T, ST.Sh{Con{y, t}, Nil{}}))), S.pop_back(T, ST.model(T, ST.Sh{Con{y, t}, Nil{}}))), L.false_true(hr))
68
69def peek_back_ready(~T: Data, +sh: ST.Shadow<T>, +hr: {RB.rdy_b(T, sh) == True{} : Bool}) -> Read(~T, sh, DQ.obs_item(~T, DQ.peek_back_ready(~T, ST.real(T, sh))), (ST.model(T, sh), E.OItem{S.item(T, SC.last(T, ST.model(T, sh)))})):
70 match sh:
71 case ST.Sh{f, Con{x, t}}:
72 +sp = Equal.cong(List<&2, T>, List<&2, T> & E.Obs<T>, z => (z, E.OItem{S.item(T, SC.last(T, z))}), SC.snoc(T, ST.model(T, ST.Sh{f, t}), x), ST.model(T, ST.Sh{f, Con{x, t}}), Equal.sym(List<&2, T>, ST.model(T, ST.Sh{f, Con{x, t}}), SC.snoc(T, ST.model(T, ST.Sh{f, t}), x), model_back(T, f, x, t)))
73 +lx = Equal.cong(Maybe<&2, T>, List<&2, T> & E.Obs<T>, m => (ST.model(T, ST.Sh{f, Con{x, t}}), E.OItem{S.item(T, m)}), Some{x}, SC.last(T, SC.snoc(T, ST.model(T, ST.Sh{f, t}), x)), Equal.sym(Maybe<&2, T>, SC.last(T, SC.snoc(T, ST.model(T, ST.Sh{f, t}), x)), Some{x}, LL.last_snoc(T, ST.model(T, ST.Sh{f, t}), x)))
74 (ST.Sh{f, Con{x, t}}, (E.OItem{Done{x}}, ({==}, Equal.trans(List<&2, T> & E.Obs<T>, (ST.model(T, ST.Sh{f, Con{x, t}}), E.OItem{Done{x}}), (ST.model(T, ST.Sh{f, Con{x, t}}), E.OItem{S.item(T, SC.last(T, SC.snoc(T, ST.model(T, ST.Sh{f, t}), x)))}), (ST.model(T, ST.Sh{f, Con{x, t}}), E.OItem{S.item(T, SC.last(T, ST.model(T, ST.Sh{f, Con{x, t}})))}), lx,
75 Equal.cong(List<&2, T>, List<&2, T> & E.Obs<T>, z => (ST.model(T, ST.Sh{f, Con{x, t}}), E.OItem{S.item(T, SC.last(T, z))}), SC.snoc(T, ST.model(T, ST.Sh{f, t}), x), ST.model(T, ST.Sh{f, Con{x, t}}), Equal.sym(List<&2, T>, ST.model(T, ST.Sh{f, Con{x, t}}), SC.snoc(T, ST.model(T, ST.Sh{f, t}), x), model_back(T, f, x, t)))))))
76 case ST.Sh{Nil{}, Nil{}}:
77 (ST.Sh{Nil{}, Nil{}}, (E.OItem{Fail{E.EmptyDeque{}}}, ({==}, {==})))
78 case ST.Sh{Con{y, t}, Nil{}}:
79 Empty.absurd(Read(~T, ST.Sh{Con{y, t}, Nil{}}, DQ.obs_item(~T, DQ.peek_back_ready(~T, ST.real(T, ST.Sh{Con{y, t}, Nil{}}))), (ST.model(T, ST.Sh{Con{y, t}, Nil{}}), E.OItem{S.item(T, SC.last(T, ST.model(T, ST.Sh{Con{y, t}, Nil{}})))})), L.false_true(hr))
80
81# ---- each operation ----
82
83def op_length(~T: Data, +sh: ST.Shadow<T>) -> K.StepOK(~T, sh, E.Length{}):
84 match sh:
85 case ST.Sh{+f, +b}:
86 +n = Nat.add(SC.length(T, f), SC.length(T, b))
87 +el = Equal.trans(Nat, n, Nat.add(SC.length(T, f), SC.length(T, SC.reverse(T, b))), SC.length(T, SC.append(T, f, SC.reverse(T, b))), Equal.cong(Nat, Nat, z => Nat.add(SC.length(T, f), z), SC.length(T, b), SC.length(T, SC.reverse(T, b)), Equal.sym(Nat, SC.length(T, SC.reverse(T, b)), SC.length(T, b), LL.length_rev(T, b))), Equal.sym(Nat, SC.length(T, SC.append(T, f, SC.reverse(T, b))), Nat.add(SC.length(T, f), SC.length(T, SC.reverse(T, b))), LL.length_append(T, f, SC.reverse(T, b))))
88 K.mk(~T, ST.Sh{f, b}, E.Length{}, ST.Sh{f, b}, E.ONat{n}, {==}, Equal.cong(Nat, List<&2, T> & E.Obs<T>, z => (ST.model(T, ST.Sh{f, b}), E.ONat{z}), n, SC.length(T, ST.model(T, ST.Sh{f, b})), el))
89
90def op_push_front(~T: Data, +sh: ST.Shadow<T>, +x: T) -> K.StepOK(~T, sh, E.PushFront{x}):
91 match sh:
92 case ST.Sh{+f, +b}:
93 K.mk(~T, ST.Sh{f, b}, E.PushFront{x}, ST.Sh{Con{x, f}, b}, E.OUnit{}, {==}, {==})
94
95def op_push_back(~T: Data, +sh: ST.Shadow<T>, +x: T) -> K.StepOK(~T, sh, E.PushBack{x}):
96 match sh:
97 case ST.Sh{+f, +b}:
98 K.mk(~T, ST.Sh{f, b}, E.PushBack{x}, ST.Sh{f, Con{x, b}}, E.OUnit{}, {==}, Equal.cong(List<&2, T>, List<&2, T> & E.Obs<T>, z => (z, E.OUnit{}), ST.model(T, ST.Sh{f, Con{x, b}}), SC.snoc(T, ST.model(T, ST.Sh{f, b}), x), model_back(T, f, x, b)))
99
100def op_to_list(~T: Data, +sh: ST.Shadow<T>) -> K.StepOK(~T, sh, E.ToList{}):
101 match sh:
102 case ST.Sh{+f, +b}:
103 +el = Equal.trans(List<&2, T>, List.append(&2, T, f, List.reverse(&2, T, b)), List.append(&2, T, f, SC.reverse(T, b)), SC.append(T, f, SC.reverse(T, b)), Equal.cong(List<&2, T>, List<&2, T>, z => List.append(&2, T, f, z), List.reverse(&2, T, b), SC.reverse(T, b), LL.base_rev(T, b)), LL.base_append(T, f, SC.reverse(T, b)))
104 K.mk(~T, ST.Sh{f, b}, E.ToList{}, ST.Sh{f, b}, E.OList{List.append(&2, T, f, List.reverse(&2, T, b))}, {==}, Equal.cong(List<&2, T>, List<&2, T> & E.Obs<T>, z => (ST.model(T, ST.Sh{f, b}), E.OList{z}), List.append(&2, T, f, List.reverse(&2, T, b)), ST.model(T, ST.Sh{f, b}), el))
105
106def pf_fin(~T: Data, +sh: ST.Shadow<T>, +sh1: ST.Shadow<T>, +e: {DQ.ready_front(~T, ST.real(T, sh)) == ST.real(T, sh1) : DQ.Deque<T>}, +em: {ST.model(T, sh1) == ST.model(T, sh) : List<&2, T>}, rd: Read(~T, sh1, DQ.obs_item(~T, DQ.pop_front_ready(~T, ST.real(T, sh1))), S.pop_front(T, ST.model(T, sh1)))) -> K.StepOK(~T, sh, E.PopFront{}):
107 match rd:
108 case Tuple{+sh2, Tuple{+o, Tuple{e1, e2}}}:
109 K.mk(~T, sh, E.PopFront{}, sh2, o,
110 Equal.trans(DQ.Deque<T> & E.Obs<T>, DQ.obs_item(~T, DQ.pop_front_ready(~T, DQ.ready_front(~T, ST.real(T, sh)))), DQ.obs_item(~T, DQ.pop_front_ready(~T, ST.real(T, sh1))), (ST.real(T, sh2), o), Equal.cong(DQ.Deque<T>, DQ.Deque<T> & E.Obs<T>, d => DQ.obs_item(~T, DQ.pop_front_ready(~T, d)), DQ.ready_front(~T, ST.real(T, sh)), ST.real(T, sh1), e), e1),
111 Equal.trans(List<&2, T> & E.Obs<T>, (ST.model(T, sh2), o), S.pop_front(T, ST.model(T, sh1)), S.pop_front(T, ST.model(T, sh)), e2, Equal.cong(List<&2, T>, List<&2, T> & E.Obs<T>, z => S.pop_front(T, z), ST.model(T, sh1), ST.model(T, sh), em)))
112
113def pf_rf(~T: Data, +sh: ST.Shadow<T>, rf: RB.RF(~T, sh)) -> K.StepOK(~T, sh, E.PopFront{}):
114 match rf:
115 case Tuple{+sh1, Tuple{e, Tuple{em, hr}}}:
116 pf_fin(~T, sh, sh1, e, em, pop_front_ready(~T, sh1, hr))
117
118def kf_fin(~T: Data, +sh: ST.Shadow<T>, +sh1: ST.Shadow<T>, +e: {DQ.ready_front(~T, ST.real(T, sh)) == ST.real(T, sh1) : DQ.Deque<T>}, +em: {ST.model(T, sh1) == ST.model(T, sh) : List<&2, T>}, rd: Read(~T, sh1, DQ.obs_item(~T, DQ.peek_front_ready(~T, ST.real(T, sh1))), (ST.model(T, sh1), E.OItem{S.item(T, SC.head(T, ST.model(T, sh1)))}))) -> K.StepOK(~T, sh, E.PeekFront{}):
119 match rd:
120 case Tuple{+sh2, Tuple{+o, Tuple{e1, e2}}}:
121 K.mk(~T, sh, E.PeekFront{}, sh2, o,
122 Equal.trans(DQ.Deque<T> & E.Obs<T>, DQ.obs_item(~T, DQ.peek_front_ready(~T, DQ.ready_front(~T, ST.real(T, sh)))), DQ.obs_item(~T, DQ.peek_front_ready(~T, ST.real(T, sh1))), (ST.real(T, sh2), o), Equal.cong(DQ.Deque<T>, DQ.Deque<T> & E.Obs<T>, d => DQ.obs_item(~T, DQ.peek_front_ready(~T, d)), DQ.ready_front(~T, ST.real(T, sh)), ST.real(T, sh1), e), e1),
123 Equal.trans(List<&2, T> & E.Obs<T>, (ST.model(T, sh2), o), (ST.model(T, sh1), E.OItem{S.item(T, SC.head(T, ST.model(T, sh1)))}), (ST.model(T, sh), E.OItem{S.item(T, SC.head(T, ST.model(T, sh)))}), e2, Equal.cong(List<&2, T>, List<&2, T> & E.Obs<T>, z => (z, E.OItem{S.item(T, SC.head(T, z))}), ST.model(T, sh1), ST.model(T, sh), em)))
124
125def kf_rf(~T: Data, +sh: ST.Shadow<T>, rf: RB.RF(~T, sh)) -> K.StepOK(~T, sh, E.PeekFront{}):
126 match rf:
127 case Tuple{+sh1, Tuple{e, Tuple{em, hr}}}:
128 kf_fin(~T, sh, sh1, e, em, peek_front_ready(~T, sh1, hr))
129
130def pb_fin(~T: Data, +sh: ST.Shadow<T>, +sh1: ST.Shadow<T>, +e: {DQ.ready_back(~T, ST.real(T, sh)) == ST.real(T, sh1) : DQ.Deque<T>}, +em: {ST.model(T, sh1) == ST.model(T, sh) : List<&2, T>}, rd: Read(~T, sh1, DQ.obs_item(~T, DQ.pop_back_ready(~T, ST.real(T, sh1))), S.pop_back(T, ST.model(T, sh1)))) -> K.StepOK(~T, sh, E.PopBack{}):
131 match rd:
132 case Tuple{+sh2, Tuple{+o, Tuple{e1, e2}}}:
133 K.mk(~T, sh, E.PopBack{}, sh2, o,
134 Equal.trans(DQ.Deque<T> & E.Obs<T>, DQ.obs_item(~T, DQ.pop_back_ready(~T, DQ.ready_back(~T, ST.real(T, sh)))), DQ.obs_item(~T, DQ.pop_back_ready(~T, ST.real(T, sh1))), (ST.real(T, sh2), o), Equal.cong(DQ.Deque<T>, DQ.Deque<T> & E.Obs<T>, d => DQ.obs_item(~T, DQ.pop_back_ready(~T, d)), DQ.ready_back(~T, ST.real(T, sh)), ST.real(T, sh1), e), e1),
135 Equal.trans(List<&2, T> & E.Obs<T>, (ST.model(T, sh2), o), S.pop_back(T, ST.model(T, sh1)), S.pop_back(T, ST.model(T, sh)), e2, Equal.cong(List<&2, T>, List<&2, T> & E.Obs<T>, z => S.pop_back(T, z), ST.model(T, sh1), ST.model(T, sh), em)))
136
137def pb_rb(~T: Data, +sh: ST.Shadow<T>, rb: RB.RB(~T, sh)) -> K.StepOK(~T, sh, E.PopBack{}):
138 match rb:
139 case Tuple{+sh1, Tuple{e, Tuple{em, hr}}}:
140 pb_fin(~T, sh, sh1, e, em, pop_back_ready(~T, sh1, hr))
141
142def kb_fin(~T: Data, +sh: ST.Shadow<T>, +sh1: ST.Shadow<T>, +e: {DQ.ready_back(~T, ST.real(T, sh)) == ST.real(T, sh1) : DQ.Deque<T>}, +em: {ST.model(T, sh1) == ST.model(T, sh) : List<&2, T>}, rd: Read(~T, sh1, DQ.obs_item(~T, DQ.peek_back_ready(~T, ST.real(T, sh1))), (ST.model(T, sh1), E.OItem{S.item(T, SC.last(T, ST.model(T, sh1)))}))) -> K.StepOK(~T, sh, E.PeekBack{}):
143 match rd:
144 case Tuple{+sh2, Tuple{+o, Tuple{e1, e2}}}:
145 K.mk(~T, sh, E.PeekBack{}, sh2, o,
146 Equal.trans(DQ.Deque<T> & E.Obs<T>, DQ.obs_item(~T, DQ.peek_back_ready(~T, DQ.ready_back(~T, ST.real(T, sh)))), DQ.obs_item(~T, DQ.peek_back_ready(~T, ST.real(T, sh1))), (ST.real(T, sh2), o), Equal.cong(DQ.Deque<T>, DQ.Deque<T> & E.Obs<T>, d => DQ.obs_item(~T, DQ.peek_back_ready(~T, d)), DQ.ready_back(~T, ST.real(T, sh)), ST.real(T, sh1), e), e1),
147 Equal.trans(List<&2, T> & E.Obs<T>, (ST.model(T, sh2), o), (ST.model(T, sh1), E.OItem{S.item(T, SC.last(T, ST.model(T, sh1)))}), (ST.model(T, sh), E.OItem{S.item(T, SC.last(T, ST.model(T, sh)))}), e2, Equal.cong(List<&2, T>, List<&2, T> & E.Obs<T>, z => (z, E.OItem{S.item(T, SC.last(T, z))}), ST.model(T, sh1), ST.model(T, sh), em)))
148
149def kb_rb(~T: Data, +sh: ST.Shadow<T>, rb: RB.RB(~T, sh)) -> K.StepOK(~T, sh, E.PeekBack{}):
150 match rb:
151 case Tuple{+sh1, Tuple{e, Tuple{em, hr}}}:
152 kb_fin(~T, sh, sh1, e, em, peek_back_ready(~T, sh1, hr))
153
154# every public operation refines the spec step
155def step_ok(~T: Data, +sh: ST.Shadow<T>, +op: E.Op<T>) -> K.StepOK(~T, sh, op):
156 match op:
157 case E.Length{}:
158 op_length(~T, sh)
159 case E.PushFront{+x}:
160 op_push_front(~T, sh, x)
161 case E.PushBack{+x}:
162 op_push_back(~T, sh, x)
163 case E.PopFront{}:
164 pf_rf(~T, sh, RB.ready_front(~T, sh))
165 case E.PopBack{}:
166 pb_rb(~T, sh, RB.ready_back(~T, sh))
167 case E.PeekFront{}:
168 kf_rf(~T, sh, RB.ready_front(~T, sh))
169 case E.PeekBack{}:
170 kb_rb(~T, sh, RB.ready_back(~T, sh))
171 case E.ToList{}:
172 op_to_list(~T, sh)