proofs/containers/deque/proof.bend
bend-collections-laws-containers@1.0.0.0 · 149 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/containers/deque.bend as S
3import bend-collections-laws-containers@1.0.0.0/src/containers/deque.bend as DQ
4import bend-collections-laws-containers@1.0.0.0/src/containers/types/deque.bend as E
5import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/state.bend as ST
6import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/stepok.bend as K
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/steps.bend as PS
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/trace.bend as FT
9import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
10import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
11import bend-collections-laws-containers@1.0.0.0/spec/lib/sequence.bend as V
12import bend-collections-laws-containers@1.0.0.0/proofs/lib/sequence.bend as VL
13
14# Deque (two lists, src/containers/deque.bend): public proof entry point.
15# shadow ST.Sh{front, back}: the deque DE{front, back, |front|,
16# |back|} (the counts are the list lengths by construction)
17# abstraction ST.model(sh) = front ++ reverse(back), front first
18# rebalance proofs/deque/rebalance.bend: ready_front / ready_back move
19# half of the other list over, keep the model, and leave the
20# requested end nonempty unless the deque is empty
21# operations PS.step_ok: every public operation, errors included (pop or
22# peek on an empty deque is Fail{EmptyDeque}, deque unchanged)
23# traces trace_from / trace_new: any finite operation list, no
24# premise on its length or on the deque's size
25#
26# Every law is a template in the element type; END_TO_END.bend instantiates
27# them at U32 and String.
28
29def new_abs(~T: Data) -> {ST.model(T, ST.initial(T)) == Nil{} : List<&2, T>}:
30 {==}
31
32def new_real(~T: Data) -> {DQ.new(~T) == ST.real(T, ST.initial(T)) : DQ.Deque<T>}:
33 {==}
34
35def step_ok(~T: Data, +sh: ST.Shadow<T>, +op: E.Op<T>) -> K.StepOK(~T, sh, op):
36 PS.step_ok(~T, sh, op)
37
38# a deque determines its shadow
39def shadow_unique(~T: Data, +a: ST.Shadow<T>, +b: ST.Shadow<T>, +e: {ST.real(T, a) == ST.real(T, b) : DQ.Deque<T>}) -> {a == b : ST.Shadow<T>}:
40 ST.real_inj(T, a, b, e)
41
42def trace_from(~T: Data, +ops: List<&2, E.Op<T>>, +sh0: ST.Shadow<T>) -> FT.TraceOK(~T, ops, sh0):
43 FT.trace_from(~T, ops, sh0)
44
45# arbitrary finite operation traces from the real constructor
46def trace_new(~T: Data, +ops: List<&2, E.Op<T>>) -> FT.TraceOK(~T, ops, ST.initial(T)):
47 FT.trace_from(~T, ops, ST.initial(T))
48
49# ==== the contract of deque (stated in spec/containers/deque.bend) ====================
50
51# ---- the implementation ----
52def Impl(~T: Data, sh: ST.Shadow<T>, op: E.Op<T>, Post: (List<&2, T> & E.Obs<T>) -> Type) -> Type:
53 Sigma<&1, &1, ST.Shadow<T>, sh2 => Sigma<&1, &1, E.Obs<T>, o => {DQ.step(~T, ST.real(T, sh), op) == (ST.real(T, sh2), o) : DQ.Deque<T> & E.Obs<T>} & Post((ST.model(T, sh2), o))>>
54
55def impl_of(~T: Data, -sh: ST.Shadow<T>, -op: E.Op<T>, -Post: (List<&2, T> & E.Obs<T>) -> Type, k: K.StepOK(~T, sh, op), pf: Post(S.step(T, ST.model(T, sh), op))) -> Impl(~T, sh, op, Post):
56 match k:
57 case Tuple{sh2, Tuple{o, Tuple{e1, e2}}}:
58 (sh2, (o, (e1, L.subst(List<&2, T> & E.Obs<T>, Post, S.step(T, ST.model(T, sh), op), (ST.model(T, sh2), o), Equal.sym(List<&2, T> & E.Obs<T>, (ST.model(T, sh2), o), S.step(T, ST.model(T, sh), op), e2), pf))))
59
60def impl(~T: Data, +sh: ST.Shadow<T>, +op: E.Op<T>, -Post: (List<&2, T> & E.Obs<T>) -> Type, pf: Post(S.step(T, ST.model(T, sh), op))) -> Impl(~T, sh, op, Post):
61 impl_of(~T, sh, op, Post, step_ok(~T, sh, op), pf)
62
63# ---- Length, iteration ----
64def length_result(-T: Data, +xs: List<&2, T>) -> S.Length.length_result(T, xs):
65 {==}
66
67def length_frame(-T: Data, +xs: List<&2, T>) -> S.Length.length_frame(T, xs):
68 {==}
69
70def to_list_model(-T: Data, +xs: List<&2, T>) -> S.Iteration.to_list_model(T, xs):
71 {==}
72
73def to_list_frame(-T: Data, +xs: List<&2, T>) -> S.Iteration.to_list_frame(T, xs):
74 {==}
75
76# ---- Empty_Vector ----
77def new_empty(~T: Data) -> {SC.length(T, ST.model(T, ST.initial(T))) == 0n : Nat}:
78 %Equal.sym(List<&2, T>, ST.model(T, ST.initial(T)), Nil{}, new_abs(~T)) : {SC.length(T, _) == 0n : Nat}
79 {==}
80
81def new_impl(~T: Data) -> {DQ.new(~T) == ST.real(T, ST.initial(T)) : DQ.Deque<T>}:
82 new_real(~T)
83
84# ---- Prepend: Length + 1, Element (First) = New_Item, Range_Shifted (Old, New, First, Last'Old, 1) ----
85def push_front_length(-T: Data, +xs: List<&2, T>, +v: T) -> S.Prepend.push_front_length(T, xs, v):
86 {==}
87
88def push_front_first(-T: Data, +xs: List<&2, T>, +v: T) -> S.Prepend.push_front_first(T, xs, v):
89 {==}
90
91def push_front_shifted(-T: Data, +xs: List<&2, T>, +v: T) -> S.Prepend.push_front_shifted(T, xs, v):
92 VL.cons_shifted(T, xs, v)
93
94# ---- Append: Length + 1, Equal_Prefix (Model'Old, Model), Element (Last'Old + 1) = New_Item ----
95def push_back_length(-T: Data, +xs: List<&2, T>, +v: T) -> S.Append.push_back_length(T, xs, v):
96 VL.snoc_length(T, xs, v)
97
98def push_back_prefix(-T: Data, +xs: List<&2, T>, +v: T) -> S.Append.push_back_prefix(T, xs, v):
99 VL.snoc_prefix(T, xs, v)
100
101def push_back_element(-T: Data, +xs: List<&2, T>, +v: T) -> S.Append.push_back_element(T, xs, v):
102 VL.snoc_last(T, xs, v)
103
104# ---- Delete_First: Length - 1, Range_Shifted (New, Old, First, Last, 1); pop_front returns First_Element'Old ----
105def pop_front_length(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_First.pop_front_length(T, h, t):
106 {==}
107
108def pop_front_shifted(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_First.pop_front_shifted(T, h, t):
109 VL.tail_shifted(T, h, t)
110
111def pop_front_result(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_First.pop_front_result(T, h, t):
112 {==}
113
114def pop_front_empty(-T: Data) -> S.Delete_First.pop_front_empty(T):
115 {==}
116
117# ---- Delete_Last: Length - 1, Equal_Prefix (Model, Model'Old); pop_back returns Last_Element'Old ----
118def pop_back_length(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_Last.pop_back_length(T, h, t):
119 VL.init_length(T, t, h)
120
121def pop_back_prefix(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_Last.pop_back_prefix(T, h, t):
122 VL.init_prefix(T, t, h)
123
124def pop_back_result(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_Last.pop_back_result(T, h, t):
125 %Equal.sym(Maybe<&2, T>, SC.last(T, Con{h, t}), V.last_elem(T, Con{h, t}), VL.last_is_elem(T, t, h)) : {E.OItem{S.item(T, _)} == E.OItem{S.item(T, V.last_elem(T, Con{h, t}))} : E.Obs<T>}
126 {==}
127
128def pop_back_empty(-T: Data) -> S.Delete_Last.pop_back_empty(T):
129 {==}
130
131# ---- First_Element / Last_Element: the end elements; nothing changes ----
132def peek_front_first(-T: Data, +h: T, +t: List<&2, T>) -> S.First_Element.peek_front_first(T, h, t):
133 ({==}, {==})
134
135def peek_front_frame(-T: Data, +xs: List<&2, T>) -> S.First_Element.peek_front_frame(T, xs):
136 {==}
137
138def peek_front_empty(-T: Data) -> S.First_Element.peek_front_empty(T):
139 {==}
140
141def peek_back_last(-T: Data, +h: T, +t: List<&2, T>) -> S.Last_Element.peek_back_last(T, h, t):
142 %Equal.sym(Maybe<&2, T>, SC.last(T, Con{h, t}), V.last_elem(T, Con{h, t}), VL.last_is_elem(T, t, h)) : {E.OItem{S.item(T, _)} == E.OItem{S.item(T, V.last_elem(T, Con{h, t}))} : E.Obs<T>}
143 {==}
144
145def peek_back_frame(-T: Data, +xs: List<&2, T>) -> S.Last_Element.peek_back_frame(T, xs):
146 {==}
147
148def peek_back_empty(-T: Data) -> S.Last_Element.peek_back_empty(T):
149 {==}