spec/containers/dynamic_array.bend
bend-collections-laws-containers@1.0.0.0 · 272 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-containers@1.0.0.0/src/containers/types/dynamic_array.bend as E
4import bend-collections-laws-containers@1.0.0.0/spec/lib/sequence.bend as V
5
6# Independent model of a bounded growable array: a sequence of items, a
7# capacity exponent `depth` (capacity 2^depth) and a fixed exponent bound
8# `limit`. Capacity policy: a push into a full array doubles the capacity
9# once; reserve(n) takes the least exponent k >= depth with n <= 2^k; clear
10# keeps the capacity. Nothing here refers to trees, slots or Base.Array.
11
12type Model<-T: Data> is Data:
13 M{limit: Nat, depth: Nat, items: List<&2, T>}
14
15def new(-T: Data) -> Model<T>:
16 M{31n, 0n, Nil{}}
17
18def with_limit(-T: Data, +k: Nat) -> Model<T>:
19 M{Nat.min(k, 31n), 0n, Nil{}}
20
21def item_result(-T: Data, x: Maybe<&2, T>) -> Result<&2, &2, E.Error, T>:
22 match x:
23 case None{}:
24 Fail{E.IndexOutOfRange{}}
25 case Some{v}:
26 Done{v}
27
28# Least k >= d with n <= 2^k, searching at most `fuel` doublings.
29def fit(fuel: Nat, +d: Nat, +n: Nat) -> Nat:
30 match fuel:
31 case 0n:
32 d
33 case 1n+f:
34 Bool.pick(Nat, Nat.is_le(n, C.pow2(d)), d, fit(f, 1n+d, n))
35
36def ok_unit() -> Result<&2, &2, E.Error, Unit>:
37 Done{Unit{}}
38
39def pop(-T: Data, +l: Nat, +d: Nat, xs: List<&2, T>) -> Model<T> & E.Obs<T>:
40 match xs:
41 case Nil{}:
42 (M{l, d, Nil{}}, E.OItem{Fail{E.EmptyArray{}}})
43 case Con{+h, +t}:
44 (M{l, d, C.init(T, Con{h, t})}, E.OItem{item_result(T, C.last(T, Con{h, t}))})
45
46def step_parts(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +op: E.Op<T>) -> Model<T> & E.Obs<T>:
47 match op:
48 case E.Length{}:
49 (M{l, d, xs}, E.ONat{C.length(T, xs)})
50 case E.Capacity{}:
51 (M{l, d, xs}, E.ONat{C.pow2(d)})
52 case E.Get{i}:
53 (M{l, d, xs}, E.OItem{item_result(T, C.nth(T, xs, i))})
54 case E.Set{i, v}:
55 Bool.pick(Model<T> & E.Obs<T>, Nat.is_lt(i, C.length(T, xs)),
56 (M{l, d, C.update(T, xs, i, v)}, E.OUnit{ok_unit()}),
57 (M{l, d, xs}, E.OUnit{Fail{E.IndexOutOfRange{}}}))
58 case E.Push{v}:
59 Bool.pick(Model<T> & E.Obs<T>, Nat.is_lt(C.length(T, xs), C.pow2(d)),
60 (M{l, d, C.snoc(T, xs, v)}, E.OUnit{ok_unit()}),
61 Bool.pick(Model<T> & E.Obs<T>, Nat.is_lt(d, l),
62 (M{l, 1n+d, C.snoc(T, xs, v)}, E.OUnit{ok_unit()}),
63 (M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}})))
64 case E.Pop{}:
65 pop(T, l, d, xs)
66 case E.Reserve{n}:
67 Bool.pick(Model<T> & E.Obs<T>, Nat.is_le(n, C.pow2(d)),
68 (M{l, d, xs}, E.OUnit{ok_unit()}),
69 Bool.pick(Model<T> & E.Obs<T>, Nat.is_le(n, C.pow2(l)),
70 (M{l, fit(n, d, n), xs}, E.OUnit{ok_unit()}),
71 (M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}})))
72 case E.Clear{}:
73 (M{l, d, Nil{}}, E.OUnit{ok_unit()})
74 case E.ToList{}:
75 (M{l, d, xs}, E.OList{xs})
76
77# Every operation: the next model and the observation.
78def step(-T: Data, m: Model<T>, op: E.Op<T>) -> Model<T> & E.Obs<T>:
79 M{l, d, xs} = m
80 step_parts(T, l, d, xs, op)
81
82def cons_obs(-T: Data, o: E.Obs<T>, r: Model<T> & List<&2, E.Obs<T>>) -> Model<T> & List<&2, E.Obs<T>>:
83 (m, os) = r
84 (m, Con{o, os})
85
86# Arbitrary finite traces: final model and every observation, in order.
87def run(-T: Data, ops: List<&2, E.Op<T>>, +m: Model<T>) -> Model<T> & List<&2, E.Obs<T>>:
88 match ops:
89 case Nil{}:
90 (m, Nil{})
91 case Con{+op, rest}:
92 cons_obs(T, Pair.snd(Model<T>, E.Obs<T>, step(T, m, op)), run(T, rest, Pair.fst(Model<T>, E.Obs<T>, step(T, m, op))))
93
94# ---- contract (SPARK formal containers) ----
95# Each `<Subprogram>.<clause>` definition below states one Post clause of
96# that SPARK subprogram, as a proposition on this model; the table names the
97# clauses. proofs/containers/dynamic_array/ proves every clause under its clause name,
98# and its `impl` lemma carries them to the implementation.
99#
100# Contracts of the dynamic array in the style of SPARK's formal vectors
101# (SPARKlib src/spark-containers-formal-vectors.ads, AdaCore/SPARKlib
102# 46ec319; the model predicates are in spec/lib/sequence.bend). Each
103# lemma is one Post clause, stated over the model step step; `impl`
104# (P.step_refines) makes the implementation's step, read back through its
105# abstraction, equal to step on every good array, so every clause holds
106# for DA.step as well.
107#
108# SPARK subprogram (.ads line) ours clauses
109# Length (284) length length_result, length_frame
110# Capacity (322) capacity capacity_result, capacity_frame
111# Empty_Vector (292) new new_empty, new_capacity, new_impl
112# with_limit with_limit_empty, with_limit_impl
113# Reserve_Capacity (328) reserve reserve_equal
114# Clear (341) clear clear_length, clear_capacity
115# Element (373) get get_element, get_frame, get_outside
116# First_Element (913) get 0 first_element
117# Last_Element (923) get (len-1) last_element
118# Replace_Element (384) set set_length, set_element,
119# set_except, set_outside
120# Append (706) push push_length, push_prefix,
121# push_element, push_full
122# Delete_Last (866) pop pop_length, pop_prefix,
123# pop_result, pop_empty
124# iteration (Iter_Model, 1193) to_list to_list_model, to_list_frame
125# implementation DA.step impl
126# Not in this API (no such operation): Is_Empty ("=" Length 0), "=",
127# To_Vector, Assign/Copy/Move (values are persistent: a copy is the value
128# itself), Constant_Reference/Reference, Insert/Insert_Vector, Prepend*,
129# Append_Vector, Append with Count, Delete (at an index), Delete_First,
130# Delete_Last with Count, Reverse_Elements, Swap, Find_Index,
131# Reverse_Find_Index, Contains, Has_Element (indices are plain Nat).
132# SPARK's Pre (Index in range, Length < Capacity) is a defensive check;
133# here the operation returns an error value and changes nothing, which the
134# *_outside, *_full and *_empty lemmas state.
135
136def items(-T: Data, m: Model<T>) -> List<&2, T>:
137 match m:
138 case M{l, d, xs}:
139 xs
140
141def depth(-T: Data, m: Model<T>) -> Nat:
142 match m:
143 case M{l, d, xs}:
144 d
145
146def nx(-T: Data, +m: Model<T>, +op: E.Op<T>) -> Model<T>:
147 Pair.fst(Model<T>, E.Obs<T>, step(T, m, op))
148
149def ob(-T: Data, +m: Model<T>, +op: E.Op<T>) -> E.Obs<T>:
150 Pair.snd(Model<T>, E.Obs<T>, step(T, m, op))
151
152# ---- Append: Length + 1, Equal_Prefix (Model'Old, Model), Element (Last_Index'Old + 1) = New_Item ----
153# room: SPARK's Pre Length < Capacity; here the array doubles once when
154# full and below its limit, so room is Length < 2^depth or depth < limit
155def room(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> Bool:
156 Bool.or(Nat.is_lt(C.length(T, xs), C.pow2(d)), Nat.is_lt(d, l))
157
158# Length (284)
159def Length.length_result(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> Type:
160 {ob(T, M{l, d, xs}, E.Length{}) == E.ONat{C.length(T, xs)} : E.Obs<T>}
161
162# Length (284)
163def Length.length_frame(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> Type:
164 {nx(T, M{l, d, xs}, E.Length{}) == M{l, d, xs} : Model<T>}
165
166# Capacity (322)
167def Capacity.capacity_result(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> Type:
168 {ob(T, M{l, d, xs}, E.Capacity{}) == E.ONat{C.pow2(d)} : E.Obs<T>}
169
170# Capacity (322)
171def Capacity.capacity_frame(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> Type:
172 {nx(T, M{l, d, xs}, E.Capacity{}) == M{l, d, xs} : Model<T>}
173
174# iteration (Iter_Model, 1193)
175def Iteration.to_list_model(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> Type:
176 {ob(T, M{l, d, xs}, E.ToList{}) == E.OList{xs} : E.Obs<T>}
177
178# iteration (Iter_Model, 1193)
179def Iteration.to_list_frame(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> Type:
180 {nx(T, M{l, d, xs}, E.ToList{}) == M{l, d, xs} : Model<T>}
181
182# Empty_Vector (292)
183def Empty_Vector.new_empty(-T: Data) -> Type:
184 {C.length(T, items(T, new(T))) == 0n : Nat}
185
186# Empty_Vector (292)
187def Empty_Vector.new_capacity(-T: Data) -> Type:
188 {C.pow2(depth(T, new(T))) == 1n : Nat}
189
190# Empty_Vector (292)
191def Empty_Vector.with_limit_empty(-T: Data, +k: Nat) -> Type:
192 {C.length(T, items(T, with_limit(T, k))) == 0n : Nat}
193
194# Reserve_Capacity (328)
195def Reserve_Capacity.reserve_equal(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +n: Nat) -> Type:
196 {items(T, nx(T, M{l, d, xs}, E.Reserve{n})) == xs : List<&2, T>}
197
198# Clear (341)
199def Clear.clear_length(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> Type:
200 {C.length(T, items(T, nx(T, M{l, d, xs}, E.Clear{}))) == 0n : Nat}
201
202# Clear (341)
203def Clear.clear_capacity(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> Type:
204 {depth(T, nx(T, M{l, d, xs}, E.Clear{})) == d : Nat}
205
206# Element (373)
207def Element.get_element(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat, +v: T, +h: {C.nth(T, xs, i) == Some{v} : Maybe<&2, T>}) -> Type:
208 {ob(T, M{l, d, xs}, E.Get{i}) == E.OItem{Done{v}} : E.Obs<T>}
209
210# Element (373)
211def Element.get_frame(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat) -> Type:
212 {nx(T, M{l, d, xs}, E.Get{i}) == M{l, d, xs} : Model<T>}
213
214# Element (373)
215def Element.get_outside(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat, +h: {Nat.is_le(C.length(T, xs), i) == True{} : Bool}) -> Type:
216 {ob(T, M{l, d, xs}, E.Get{i}) == E.OItem{Fail{E.IndexOutOfRange{}}} : E.Obs<T>}
217
218# First_Element (913)
219def First_Element.first_element(-T: Data, +l: Nat, +d: Nat, +h: T, +t: List<&2, T>) -> Type:
220 {ob(T, M{l, d, Con{h, t}}, E.Get{0n}) == E.OItem{Done{h}} : E.Obs<T>}
221
222# Last_Element (923)
223def Last_Element.last_element(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> Type:
224 {ob(T, M{l, d, xs}, E.Get{Nat.sub(C.length(T, xs), 1n)}) == E.OItem{item_result(T, V.last_elem(T, xs))} : E.Obs<T>}
225
226# Replace_Element (384)
227def Replace_Element.set_length(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat, +v: T, +h: {Nat.is_lt(i, C.length(T, xs)) == True{} : Bool}) -> Type:
228 {C.length(T, items(T, nx(T, M{l, d, xs}, E.Set{i, v}))) == C.length(T, xs) : Nat}
229
230# Replace_Element (384)
231def Replace_Element.set_element(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat, +v: T, +h: {Nat.is_lt(i, C.length(T, xs)) == True{} : Bool}) -> Type:
232 {C.nth(T, items(T, nx(T, M{l, d, xs}, E.Set{i, v})), i) == Some{v} : Maybe<&2, T>}
233
234# Replace_Element (384)
235def Replace_Element.set_except(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat, +v: T, +h: {Nat.is_lt(i, C.length(T, xs)) == True{} : Bool}) -> Type:
236 V.EqualExcept(T, xs, items(T, nx(T, M{l, d, xs}, E.Set{i, v})), i)
237
238# Replace_Element (384)
239def Replace_Element.set_outside(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat, +v: T, +h: {Nat.is_lt(i, C.length(T, xs)) == False{} : Bool}) -> Type:
240 {step(T, M{l, d, xs}, E.Set{i, v}) == (M{l, d, xs}, E.OUnit{Fail{E.IndexOutOfRange{}}}) : Model<T> & E.Obs<T>}
241
242# Append (706)
243def Append.push_length(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +v: T, +hr: {room(T, l, d, xs) == True{} : Bool}) -> Type:
244 {C.length(T, items(T, nx(T, M{l, d, xs}, E.Push{v}))) == 1n+C.length(T, xs) : Nat}
245
246# Append (706)
247def Append.push_prefix(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +v: T, +hr: {room(T, l, d, xs) == True{} : Bool}) -> Type:
248 V.EqualPrefix(T, xs, items(T, nx(T, M{l, d, xs}, E.Push{v})))
249
250# Append (706)
251def Append.push_element(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +v: T, +hr: {room(T, l, d, xs) == True{} : Bool}) -> Type:
252 {C.nth(T, items(T, nx(T, M{l, d, xs}, E.Push{v})), C.length(T, xs)) == Some{v} : Maybe<&2, T>}
253
254# Append (706)
255def Append.push_full(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +v: T, +h1: {Nat.is_lt(C.length(T, xs), C.pow2(d)) == False{} : Bool}, +h2: {Nat.is_lt(d, l) == False{} : Bool}) -> Type:
256 {step(T, M{l, d, xs}, E.Push{v}) == (M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}) : Model<T> & E.Obs<T>}
257
258# Delete_Last (866)
259def Delete_Last.pop_length(-T: Data, +l: Nat, +d: Nat, +h: T, +t: List<&2, T>) -> Type:
260 {C.length(T, items(T, nx(T, M{l, d, Con{h, t}}, E.Pop{}))) == C.length(T, t) : Nat}
261
262# Delete_Last (866)
263def Delete_Last.pop_prefix(-T: Data, +l: Nat, +d: Nat, +h: T, +t: List<&2, T>) -> Type:
264 V.EqualPrefix(T, items(T, nx(T, M{l, d, Con{h, t}}, E.Pop{})), Con{h, t})
265
266# Delete_Last (866)
267def Delete_Last.pop_result(-T: Data, +l: Nat, +d: Nat, +h: T, +t: List<&2, T>) -> Type:
268 {ob(T, M{l, d, Con{h, t}}, E.Pop{}) == E.OItem{item_result(T, V.last_elem(T, Con{h, t}))} : E.Obs<T>}
269
270# Delete_Last (866)
271def Delete_Last.pop_empty(-T: Data, +l: Nat, +d: Nat) -> Type:
272 {step(T, M{l, d, Nil{}}, E.Pop{}) == (M{l, d, Nil{}}, E.OItem{Fail{E.EmptyArray{}}}) : Model<T> & E.Obs<T>}