1	import Base
2	import ../storage/main.bend as Storage
3	import ../storage/model.bend as Model
4	import ../storage/refinement.bend as Refinement
5	import ../storage/route.bend as Route
6	
7	def logical_length(storage: Storage.Storage) -> Nat:
8	  match storage:
9	    case Storage.Empty{}:
10	      0n
11	    case Storage.Owned{d, n, array, balanced, valid}:
12	      n
13	
14	def retained_read(result: Storage.Storage & Result<&2, &2, Storage.Error, F32>) -> Nat:
15	  (storage, value) = result
16	  logical_length(storage)
17	
18	def retained_write(result: Storage.Storage & Result<&2, &2, Storage.Error, Unit>) -> Nat:
19	  (storage, value) = result
20	  logical_length(storage)
21	
22	def finish_read_length(+d: Nat, +n: Nat, -original: Array<F32>, +i: U32,
23	  result: Array<F32> & F32, -exact: {result == Array.get(F32, original, i) : Array<F32> & F32},
24	  -balanced: Model.Balanced(F32, d, original), -valid: {Storage.bounds(d, n) == True{} : Bool}) ->
25	  {retained_read(Storage.finish_read(d, n, original, i, result, exact, balanced, valid)) == n : Nat}:
26	  (array, value) = result
27	  {==}
28	
29	def get_checked_length(+d: Nat, +n: Nat, array: Array<F32>, +i: U32, allowed: Bool,
30	  -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool},
31	  -balanced: Model.Balanced(F32, d, array), -valid: {Storage.bounds(d, n) == True{} : Bool}) ->
32	  {retained_read(Storage.get_checked(d, n, array, i, allowed, decision, balanced, valid)) == n : Nat}:
33	  match allowed:
34	    case False{}:
35	      {==}
36	    case True{}:
37	      finish_read_length(d, n, array, i, Array.get(F32, array, i), {==}, balanced, valid)
38	
39	def get_length(storage: Storage.Storage, +i: U32) ->
40	  {retained_read(Storage.get(storage, i)) == logical_length(storage) : Nat}:
41	  match storage:
42	    case Storage.Empty{}:
43	      {==}
44	    case Storage.Owned{+d, +n, array, balanced, valid}:
45	      get_checked_length(d, n, array, i, Nat.is_lt(U32.to_nat(i), n), {==}, balanced, valid)
46	
47	def set_checked_length(+d: Nat, +n: Nat, array: Array<F32>, +i: U32, +value: F32, allowed: Bool,
48	  -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool},
49	  -balanced: Model.Balanced(F32, d, array), -valid: {Storage.bounds(d, n) == True{} : Bool}) ->
50	  {retained_write(Storage.set_checked(d, n, array, i, value, allowed, decision, balanced, valid)) == n : Nat}:
51	  match allowed:
52	    case False{}:
53	      {==}
54	    case True{}:
55	      {==}
56	
57	def set_length(storage: Storage.Storage, +i: U32, +value: F32) ->
58	  {retained_write(Storage.set(storage, i, value)) == logical_length(storage) : Nat}:
59	  match storage:
60	    case Storage.Empty{}:
61	      {==}
62	    case Storage.Owned{+d, +n, array, balanced, valid}:
63	      set_checked_length(d, n, array, i, value, Nat.is_lt(U32.to_nat(i), n), {==}, balanced, valid)
64	
65	def first_length(pair: Storage.Storage & Storage.Storage) -> Nat:
66	  (first, second) = pair
67	  logical_length(first)
68	
69	def second_length(pair: Storage.Storage & Storage.Storage) -> Nat:
70	  (first, second) = pair
71	  logical_length(second)
72	
73	def finish_clone_first(+d: Nat, +n: Nat, -original: Array<F32>, pair: Array<F32> & Array<F32>,
74	  -exact: {pair == Array.clone(F32, original) : Array<F32> & Array<F32>},
75	  -balanced: Model.Balanced(F32, d, original), -valid: {Storage.bounds(d, n) == True{} : Bool}) ->
76	  {first_length(Storage.finish_clone(d, n, original, pair, exact, balanced, valid)) == n : Nat}:
77	  (first, second) = pair
78	  {==}
79	
80	def finish_clone_second(+d: Nat, +n: Nat, -original: Array<F32>, pair: Array<F32> & Array<F32>,
81	  -exact: {pair == Array.clone(F32, original) : Array<F32> & Array<F32>},
82	  -balanced: Model.Balanced(F32, d, original), -valid: {Storage.bounds(d, n) == True{} : Bool}) ->
83	  {second_length(Storage.finish_clone(d, n, original, pair, exact, balanced, valid)) == n : Nat}:
84	  (first, second) = pair
85	  {==}
86	
87	def clone_first_length(storage: Storage.Storage) ->
88	  {first_length(Storage.clone(storage)) == logical_length(storage) : Nat}:
89	  match storage:
90	    case Storage.Empty{}:
91	      {==}
92	    case Storage.Owned{+d, +n, array, balanced, valid}:
93	      finish_clone_first(d, n, array, Array.clone(F32, array), {==}, balanced, valid)
94	
95	def clone_second_length(storage: Storage.Storage) ->
96	  {second_length(Storage.clone(storage)) == logical_length(storage) : Nat}:
97	  match storage:
98	    case Storage.Empty{}:
99	      {==}
100	    case Storage.Owned{+d, +n, array, balanced, valid}:
101	      finish_clone_second(d, n, array, Array.clone(F32, array), {==}, balanced, valid)
102	
103	def length_owner(pair: Storage.Storage & Nat) -> Nat:
104	  (storage, n) = pair
105	  logical_length(storage)
106	
107	def length_value(pair: Storage.Storage & Nat) -> Nat:
108	  (storage, n) = pair
109	  n
110	
111	def length_exact(storage: Storage.Storage) ->
112	  {length_owner(Storage.length(storage)) == length_value(Storage.length(storage)) : Nat}:
113	  match storage:
114	    case Storage.Empty{}:
115	      {==}
116	    case Storage.Owned{d, n, array, balanced, valid}:
117	      {==}
118	
119	def length_preserved(storage: Storage.Storage) ->
120	  {length_owner(Storage.length(storage)) == logical_length(storage) : Nat}:
121	  match storage:
122	    case Storage.Empty{}:
123	      {==}
124	    case Storage.Owned{d, n, array, balanced, valid}:
125	      {==}
126	
127	def IsTrue(value: Bool) -> Data:
128	  match value:
129	    case True{}:
130	      Unit
131	    case False{}:
132	      Empty
133	
134	def false_true(equal: {True{} == False{} : Bool}) -> Empty:
135	  %equal : IsTrue(_)
136	  Unit{}
137	
138	def natural_equal(+a: Nat, +b: Nat, equal: {True{} == Nat.is_eq(a, b) : Bool}) -> {a == b : Nat}:
139	  match a b:
140	    case 0n 0n:
141	      {==}
142	    case 0n 1n+q:
143	      Empty.absurd({0n == 1n+q : Nat}, false_true(equal))
144	    case 1n+p 0n:
145	      Empty.absurd({1n+p == 0n : Nat}, false_true(equal))
146	    case 1n+p 1n+q:
147	      Equal.cong(Nat, Nat, x => 1n+x, p, q, natural_equal(p, q, equal))
148	
149	def observe(storage: Storage.Storage, +index: U32) -> Maybe<&2, F32>:
150	  match storage:
151	    case Storage.Empty{}:
152	      None{}
153	    case Storage.Owned{+d, n, array, balanced, valid}:
154	      Model.observe(F32, d, array, Refinement.route(d, index))
155	
156	def read_value(pair: Storage.Storage & Result<&2, &2, Storage.Error, F32>) -> Maybe<&2, F32>:
157	  (storage, result) = pair
158	  match result:
159	    case Fail{error}:
160	      None{}
161	    case Done{value}:
162	      Some{value}
163	
164	def observe_index(+depth: Nat, -length: Nat, array: Array<F32>, +index: U32, matched: Bool) -> Maybe<&2, F32>:
165	  match matched:
166	    case False{}:
167	      None{}
168	    case True{}:
169	      Model.observe(F32, depth, array, Refinement.route(depth, index))
170	
171	def observe_allowed(+depth: Nat, +length: Nat, array: Array<F32>, +index: U32, allowed: Bool) -> Maybe<&2, F32>:
172	  match allowed:
173	    case False{}:
174	      None{}
175	    case True{}:
176	      observe_index(depth, length, array, index, Storage.index_matches(depth, length, index))
177	
178	def checked_observe(storage: Storage.Storage, +index: U32) -> Maybe<&2, F32>:
179	  match storage:
180	    case Storage.Empty{}:
181	      None{}
182	    case Storage.Owned{+depth, +length, array, balanced, valid}:
183	      observe_allowed(depth, length, array, index, Nat.is_lt(U32.to_nat(index), length))
184	
185	def finish_read_value(-depth: Nat, -length: Nat, -original: Array<F32>, -index: U32,
186	  pair: Array<F32> & F32, -exact: {pair == Array.get(F32, original, index) : Array<F32> & F32},
187	  -balanced: Model.Balanced(F32, depth, original), -valid: {Storage.bounds(depth, length) == True{} : Bool}) ->
188	  {read_value(Storage.finish_read(depth, length, original, index, pair, exact, balanced, valid)) ==
189	    Some{Refinement.second(F32, pair)} : Maybe<&2, F32>}:
190	  (array, value) = pair
191	  {==}
192	
193	type ReadCheckedModel<-depth: Nat, -length: Nat, -array: Array<F32>, -index: U32, -allowed: Bool,
194	  -decision: {allowed == Nat.is_lt(U32.to_nat(index), length) : Bool},
195	  -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool}> is Data:
196	  ReadCheckedModel{-meaning: {read_value(Storage.get_checked(depth, length, array, index, allowed, decision, balanced, valid)) ==
197	    observe_allowed(depth, length, array, index, allowed) : Maybe<&2, F32>}}
198	
199	def read_checked_model(+depth: Nat, +length: Nat, -array: Array<F32>, +index: U32, allowed: Bool,
200	  -decision: {allowed == Nat.is_lt(U32.to_nat(index), length) : Bool},
201	  -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool}) ->
202	  ReadCheckedModel<depth, length, array, index, allowed, decision, balanced, valid>:
203	  match allowed:
204	    case False{}:
205	      ReadCheckedModel{{==}}
206	    case True{}:
207	      ReadCheckedModel{
208	        %Route.index_complete(depth, length, index, valid,
209	          Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(index), length), decision)) :
210	          {read_value(Storage.finish_read(depth, length, array, index, Array.get(F32, array, index), {==}, balanced, valid)) ==
211	            observe_index(depth, length, array, index, _) : Maybe<&2, F32>}
212	        Equal.trans(Maybe<&2, F32>,
213	          read_value(Storage.finish_read(depth, length, array, index, Array.get(F32, array, index), {==}, balanced, valid)),
214	          Some{Refinement.second(F32, Array.get(F32, array, index))}, Model.observe(F32, depth, array, Refinement.route(depth, index)),
215	          finish_read_value(depth, length, array, index, Array.get(F32, array, index), {==}, balanced, valid),
216	          Refinement.law_get_refines(F32, depth, array, index, balanced))}
217	
218	type StorageReadModel<-original: Storage.Storage, -index: U32> is Data:
219	  StorageReadModel{-meaning: {read_value(Storage.get(original, index)) == checked_observe(original, index) : Maybe<&2, F32>}}
220	
221	def read_checked_storage(+depth: Nat, +length: Nat, -array: Array<F32>, +index: U32,
222	  -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
223	  certificate: ReadCheckedModel<depth, length, array, index, Nat.is_lt(U32.to_nat(index), length), {==}, balanced, valid>) ->
224	  StorageReadModel<Storage.Owned{depth, length, array, balanced, valid}, index>:
225	  ReadCheckedModel{meaning} = certificate
226	  StorageReadModel{meaning}
227	
228	def storage_read_model(original: Storage.Storage, +index: U32) -> StorageReadModel<original, index>:
229	  match original:
230	    case Storage.Empty{}:
231	      StorageReadModel{{==}}
232	    case Storage.Owned{+depth, +length, array, balanced, valid}:
233	      read_checked_storage(depth, length, array, index, balanced, valid,
234	        read_checked_model(depth, length, array, index, Nat.is_lt(U32.to_nat(index), length), {==}, balanced, valid))
235	
236	def checked_observe_array(+depth: Nat, +length: Nat, array: Array<F32>, +index: U32) -> Maybe<&2, F32>:
237	  observe_allowed(depth, length, array, index, Nat.is_lt(U32.to_nat(index), length))
238	
239	def retained_observe(pair: Storage.Storage & Result<&2, &2, Storage.Error, F32>, index: U32) -> Maybe<&2, F32>:
240	  (storage, result) = pair
241	  checked_observe(storage, index)
242	
243	def finish_read_observe(+depth: Nat, +length: Nat, -original: Array<F32>, -index: U32, +other: U32,
244	  pair: Array<F32> & F32, -exact: {pair == Array.get(F32, original, index) : Array<F32> & F32},
245	  -balanced: Model.Balanced(F32, depth, original), -valid: {Storage.bounds(depth, length) == True{} : Bool}) ->
246	  {retained_observe(Storage.finish_read(depth, length, original, index, pair, exact, balanced, valid), other) ==
247	    checked_observe_array(depth, length, Refinement.first(F32, pair), other) : Maybe<&2, F32>}:
248	  (array, value) = pair
249	  {==}
250	
251	type ReadCheckedKeeps<-depth: Nat, -length: Nat, -array: Array<F32>, -index: U32, -allowed: Bool,
252	  -decision: {allowed == Nat.is_lt(U32.to_nat(index), length) : Bool},
253	  -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool}> is Data:
254	  ReadCheckedKeeps{-kept: @+other: U32 ->
255	    {retained_observe(Storage.get_checked(depth, length, array, index, allowed, decision, balanced, valid), other) ==
256	      checked_observe_array(depth, length, array, other) : Maybe<&2, F32>}}
257	
258	def read_checked_keeps(+depth: Nat, +length: Nat, -array: Array<F32>, +index: U32, allowed: Bool,
259	  -decision: {allowed == Nat.is_lt(U32.to_nat(index), length) : Bool},
260	  -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool}) ->
261	  ReadCheckedKeeps<depth, length, array, index, allowed, decision, balanced, valid>:
262	  match allowed:
263	    case False{}:
264	      ReadCheckedKeeps{other => {==}}
265	    case True{}:
266	      ReadCheckedKeeps{other => Equal.trans(Maybe<&2, F32>,
267	        retained_observe(Storage.finish_read(depth, length, array, index, Array.get(F32, array, index), {==}, balanced, valid), other),
268	        checked_observe_array(depth, length, Refinement.first(F32, Array.get(F32, array, index)), other),
269	        checked_observe_array(depth, length, array, other),
270	        finish_read_observe(depth, length, array, index, other, Array.get(F32, array, index), {==}, balanced, valid),
271	        Equal.cong(Array<F32>, Maybe<&2, F32>, a => checked_observe_array(depth, length, a, other),
272	          Refinement.first(F32, Array.get(F32, array, index)), array, Refinement.law_get_retains(F32, depth, array, index, balanced)))}
273	
274	type StorageReadKeeps<-original: Storage.Storage, -index: U32> is Data:
275	  StorageReadKeeps{-kept: @+other: U32 ->
276	    {retained_observe(Storage.get(original, index), other) == checked_observe(original, other) : Maybe<&2, F32>}}
277	
278	def read_checked_storage_keeps(+depth: Nat, +length: Nat, -array: Array<F32>, +index: U32,
279	  -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
280	  certificate: ReadCheckedKeeps<depth, length, array, index, Nat.is_lt(U32.to_nat(index), length), {==}, balanced, valid>) ->
281	  StorageReadKeeps<Storage.Owned{depth, length, array, balanced, valid}, index>:
282	  ReadCheckedKeeps{kept} = certificate
283	  StorageReadKeeps{kept}
284	
285	def storage_read_keeps(original: Storage.Storage, +index: U32) -> StorageReadKeeps<original, index>:
286	  match original:
287	    case Storage.Empty{}:
288	      StorageReadKeeps{other => {==}}
289	    case Storage.Owned{+depth, +length, array, balanced, valid}:
290	      read_checked_storage_keeps(depth, length, array, index, balanced, valid,
291	        read_checked_keeps(depth, length, array, index, Nat.is_lt(U32.to_nat(index), length), {==}, balanced, valid))
292	
293	def and_left_true(+left: Bool, +right: Bool, equal: {Bool.and(left, right) == True{} : Bool}) -> {left == True{} : Bool}:
294	  match left:
295	    case False{}:
296	      Empty.absurd({False{} == True{} : Bool}, false_true(Equal.sym(Bool, False{}, True{}, equal)))
297	    case True{}:
298	      {==}
299	
300	def and_right_true(+left: Bool, +right: Bool, equal: {Bool.and(left, right) == True{} : Bool}) -> {right == True{} : Bool}:
301	  match left:
302	    case False{}:
303	      Empty.absurd({right == True{} : Bool}, false_true(Equal.sym(Bool, False{}, True{}, equal)))
304	    case True{}:
305	      equal
306	
307	def checked_index_allowed(+depth: Nat, +length: Nat, +index: U32,
308	  +checked: {Storage.index_matches(depth, length, index) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(index), length) == True{} : Bool}:
309	  %natural_equal(Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index),
310	    Equal.sym(Bool, Nat.is_eq(Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index)), True{},
311	      and_left_true(Nat.is_eq(Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index)),
312	        Nat.is_lt(Model.offset(depth, Refinement.route(depth, index)), length), checked))) :
313	    {Nat.is_lt(_, length) == True{} : Bool}
314	  and_right_true(Nat.is_eq(Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index)),
315	    Nat.is_lt(Model.offset(depth, Refinement.route(depth, index)), length), checked)
316	
317	type ArrayObservationModel<-depth: Nat, -length: Nat, -array: Array<F32>, -index: U32,
318	  -checked: {Storage.index_matches(depth, length, index) == True{} : Bool}> is Data:
319	  ArrayObservationModel{-equal: {checked_observe_array(depth, length, array, index) ==
320	    Model.observe(F32, depth, array, Refinement.route(depth, index)) : Maybe<&2, F32>}}
321	
322	def array_observation_model(+depth: Nat, +length: Nat, -array: Array<F32>, +index: U32,
323	  +checked: {Storage.index_matches(depth, length, index) == True{} : Bool}) -> ArrayObservationModel<depth, length, array, index, checked>:
324	  ArrayObservationModel{
325	    %Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), length), True{}, checked_index_allowed(depth, length, index, checked)) :
326	      {observe_allowed(depth, length, array, index, _) == Model.observe(F32, depth, array, Refinement.route(depth, index)) : Maybe<&2, F32>}
327	    %Equal.sym(Bool, Storage.index_matches(depth, length, index), True{}, checked) :
328	      {observe_index(depth, length, array, index, _) == Model.observe(F32, depth, array, Refinement.route(depth, index)) : Maybe<&2, F32>}
329	    {==}}