1	import Base
2	import ../lib/common.bend as C
3	import ../../src/containers/types/dynamic_array.bend as E
4	import ../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	
12	type Model<-T: Data> is Data:
13	  M{limit: Nat, depth: Nat, items: List<&2, T>}
14	
15	def new(-T: Data) -> Model<T>:
16	  M{31n, 0n, Nil{}}
17	
18	def with_limit(-T: Data, +k: Nat) -> Model<T>:
19	  M{Nat.min(k, 31n), 0n, Nil{}}
20	
21	def 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.
29	def 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	
36	def ok_unit() -> Result<&2, &2, E.Error, Unit>:
37	  Done{Unit{}}
38	
39	def 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	
46	def 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.
78	def 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	
82	def 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.
87	def 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	
136	def items(-T: Data, m: Model<T>) -> List<&2, T>:
137	  match m:
138	    case M{l, d, xs}:
139	      xs
140	
141	def depth(-T: Data, m: Model<T>) -> Nat:
142	  match m:
143	    case M{l, d, xs}:
144	      d
145	
146	def 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	
149	def 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
155	def 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)
159	def 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)
163	def 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)
167	def 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)
171	def 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)
175	def 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)
179	def 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)
183	def Empty_Vector.new_empty(-T: Data) -> Type:
184	  {C.length(T, items(T, new(T))) == 0n : Nat}
185	
186	# Empty_Vector (292)
187	def Empty_Vector.new_capacity(-T: Data) -> Type:
188	  {C.pow2(depth(T, new(T))) == 1n : Nat}
189	
190	# Empty_Vector (292)
191	def 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)
195	def 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)
199	def 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)
203	def 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)
207	def 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)
211	def 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)
215	def 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)
219	def 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)
223	def 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)
227	def 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)
231	def 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)
235	def 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)
239	def 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)
243	def 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)
247	def 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)
251	def 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)
255	def 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)
259	def 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)
263	def 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)
267	def 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)
271	def 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>}