1	# Proof-only preservation of affine traversal owners. Reader values are handed
2	# back unchanged; output witnesses keep their original depth. Numerical loops
3	# call none of these functions: certificate equations use them under rewrites.
4	import Base
5	import ../traversal_loop.bend as Loop
6	import ../traversal_array.bend as Traversal
7	import ./storage_witness.bend as Witness
8	
9	type Sample<-Reader: Type,-Element: Data,-reader: Reader,-result: Reader & Element> is Data:
10	  Sample{-value: Element,equation: {result == (reader,value) : Reader & Element}}
11	
12	type StateEvidence<-Reader: Type,-Element: Data,-Context: Data,-reader: Reader,-depth: Nat,
13	  -state: Traversal.State<&1,&1,Reader,Array<Element>,Context>> is Data:
14	  StateEvidence{-output: Array<Element>,position: U32,context: Context,
15	    equation: {state == Traversal.State{reader,output,position,context} : Traversal.State<&1,&1,Reader,Array<Element>,Context>},
16	    output_evidence: Witness.Witness(Element,depth,output)}
17	
18	def store(~Reader: Type,~Element: Data,~Context: Data,~destination: Context -> U32 -> U32,
19	  +depth: Nat,-reader: Reader,+position: U32,+context: Context,-output: Array<Element>,-result: Reader & Element,
20	  output_evidence: Witness.Witness(Element,depth,output),sample: Sample<Reader,Element,reader,result>) ->
21	  StateEvidence<Reader,Element,Context,reader,depth,Traversal.store(~Reader,~Element,~Context,~destination,position,context,output,result)>:
22	  match sample:
23	    case Sample{value,equation}:
24	      %Equal.sym(Reader & Element,result,(reader,value),equation) :
25	        StateEvidence<Reader,Element,Context,reader,depth,Traversal.store(~Reader,~Element,~Context,~destination,position,context,output,_)>
26	      StateEvidence{Array.set(Element,output,destination(context,position),value),(position + 1 : U32),context,{==},
27	        Witness.write(Element,depth,output,destination(context,position),value,output_evidence)}
28	
29	def step(~Reader: Type,~Element: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
30	  ~read: Reader -> Context -> U32 -> Reader & Element,~destination: Context -> U32 -> U32,
31	  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) ->
32	    Sample<Reader,Element,reader,read(reader,context,index)>,
33	  +depth: Nat,-reader: Reader,-state: Traversal.State<&1,&1,Reader,Array<Element>,Context>,
34	  reader_evidence: ReaderEvidence(reader),evidence: StateEvidence<Reader,Element,Context,reader,depth,state>) ->
35	  StateEvidence<Reader,Element,Context,reader,depth,Traversal.step(~Reader,~Element,~Context,~read,~destination,state)>:
36	  match evidence:
37	    case StateEvidence{output,+position,+context,equation,output_evidence}:
38	      %Equal.sym(Traversal.State<&1,&1,Reader,Array<Element>,Context>,state,Traversal.State{reader,output,position,context},equation) :
39	        StateEvidence<Reader,Element,Context,reader,depth,Traversal.step(~Reader,~Element,~Context,~read,~destination,_)>
40	      store(~Reader,~Element,~Context,~destination,depth,reader,position,context,output,read(reader,context,position),output_evidence,
41	        read_preserves(reader,context,position,reader_evidence))
42	
43	def run(~Reader: Type,~Element: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
44	  ~read: Reader -> Context -> U32 -> Reader & Element,~destination: Context -> U32 -> U32,
45	  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) ->
46	    Sample<Reader,Element,reader,read(reader,context,index)>,
47	  +depth: Nat,count: Nat,-reader: Reader,-state: Traversal.State<&1,&1,Reader,Array<Element>,Context>,
48	  +reader_evidence: ReaderEvidence(reader),evidence: StateEvidence<Reader,Element,Context,reader,depth,state>) ->
49	  StateEvidence<Reader,Element,Context,reader,depth,Traversal.run(~Reader,~Element,~Context,~read,~destination,count,state)>:
50	  match count:
51	    case 0n: evidence
52	    case 1n+rest:
53	      run(~Reader,~Element,~Context,~ReaderEvidence,~read,~destination,~read_preserves,depth,rest,reader,
54	        Traversal.step(~Reader,~Element,~Context,~read,~destination,state),reader_evidence,
55	        step(~Reader,~Element,~Context,~ReaderEvidence,~read,~destination,~read_preserves,depth,reader,state,reader_evidence,evidence))
56	
57	type ResultEvidence<-Reader: Type,-Element: Data,-reader: Reader,-depth: Nat,-result: Reader & Array<Element>> is Data:
58	  ResultEvidence{-output: Array<Element>,equation: {result == (reader,output) : Reader & Array<Element>},
59	    output_evidence: Witness.Witness(Element,depth,output)}
60	
61	def finish(~Reader: Type,~Element: Data,~Context: Data,-reader: Reader,-depth: Nat,
62	  -state: Traversal.State<&1,&1,Reader,Array<Element>,Context>,evidence: StateEvidence<Reader,Element,Context,reader,depth,state>) ->
63	  ResultEvidence<Reader,Element,reader,depth,Traversal.finish(~Reader,~Element,~Context,state)>:
64	  match evidence:
65	    case StateEvidence{output,position,context,equation,output_evidence}:
66	      %Equal.sym(Traversal.State<&1,&1,Reader,Array<Element>,Context>,state,Traversal.State{reader,output,position,context},equation) :
67	        ResultEvidence<Reader,Element,reader,depth,Traversal.finish(~Reader,~Element,~Context,_)>
68	      ResultEvidence{output,{==},output_evidence}
69	
70	def array_evidence(~Element: Data,-storage: Array<Element>) -> Data:
71	  Witness.ArrayWitness<Element,storage>
72	
73	def array_sample(~Element: Data,-storage: Array<Element>,-result: Array<Element> & Element,
74	  read: Witness.Read<Element,storage,result>) -> Sample<Array<Element>,Element,storage,result>:
75	  match read:
76	    case Witness.Read{value,equation}: Sample{value,equation}
77	
78	def offset_read(~Element: Data,-storage: Array<Element>,context: Traversal.Offsets,index: U32,
79	  evidence: Witness.ArrayWitness<Element,storage>) ->
80	  Sample<Array<Element>,Element,storage,Traversal.source_offset(~Element,storage,context,index)>:
81	  Traversal.Offsets{source,destination} = context
82	  array_sample(~Element,storage,Array.get(Element,storage,(source + index : U32)),Witness.observed(Element,storage,(source + index : U32),evidence))
83	
84	def first(~Left: Type,~Right: Type,pair: Left & Right) -> Left:
85	  (left,right) = pair
86	  left
87	
88	def second(~Left: Type,~Right: Type,pair: Left & Right) -> Right:
89	  (left,right) = pair
90	  right
91	
92	def source_unchanged(~Reader: Type,~Element: Data,-reader: Reader,-depth: Nat,-result: Reader & Array<Element>,
93	  evidence: ResultEvidence<Reader,Element,reader,depth,result>) -> {first(~Reader,~Array<Element>,result) == reader : Reader}:
94	  match evidence:
95	    case ResultEvidence{output,equation,output_evidence}:
96	      Equal.cong(Reader & Array<Element>,Reader,pair => first(~Reader,~Array<Element>,pair),result,(reader,output),equation)
97	
98	def output_witness(~Reader: Type,~Element: Data,-reader: Reader,-depth: Nat,-result: Reader & Array<Element>,
99	  evidence: ResultEvidence<Reader,Element,reader,depth,result>) -> Witness.Witness(Element,depth,second(~Reader,~Array<Element>,result)):
100	  match evidence:
101	    case ResultEvidence{output,equation,output_evidence}:
102	      %Equal.sym(Reader & Array<Element>,result,(reader,output),equation) : Witness.Witness(Element,depth,second(~Reader,~Array<Element>,_))
103	      output_evidence
104	
105	def update_sample(~Reader: Type,~Element: Data,~Value: Data,~Context: Data,
106	  ~combine: Element -> Value -> Element,~destination: Context -> U32 -> U32,
107	  +depth: Nat,-reader: Reader,+position: U32,+context: Context,-output: Array<Element>,-current: Element,
108	  -result: Reader & Value,output_evidence: Witness.Witness(Element,depth,output),
109	  sample: Sample<Reader,Value,reader,result>) ->
110	  StateEvidence<Reader,Element,Context,reader,depth,
111	    Traversal.update_sample(~Reader,~Element,~Value,~Context,~combine,~destination,position,context,output,current,result)>:
112	  match sample:
113	    case Sample{value,equation}:
114	      %Equal.sym(Reader & Value,result,(reader,value),equation) :
115	        StateEvidence<Reader,Element,Context,reader,depth,
116	          Traversal.update_sample(~Reader,~Element,~Value,~Context,~combine,~destination,position,context,output,current,_)>
117	      StateEvidence{Array.set(Element,output,destination(context,position),combine(current,value)),(position + 1 : U32),context,{==},
118	        Witness.write(Element,depth,output,destination(context,position),combine(current,value),output_evidence)}
119	
120	def update_current(~Reader: Type,~Element: Data,~Value: Data,~Context: Data,
121	  ~read: Reader -> Context -> U32 -> Reader & Value,~combine: Element -> Value -> Element,
122	  ~destination: Context -> U32 -> U32,+depth: Nat,-reader: Reader,+position: U32,+context: Context,
123	  -output: Array<Element>,-result: Array<Element> & Element,
124	  output_evidence: Witness.Witness(Element,depth,output),observed: Witness.Read<Element,output,result>,
125	  sample: Sample<Reader,Value,reader,read(reader,context,position)>) ->
126	  StateEvidence<Reader,Element,Context,reader,depth,
127	    Traversal.update_current(~Reader,~Element,~Value,~Context,~read,~combine,~destination,reader,position,context,result)>:
128	  match observed:
129	    case Witness.Read{value,equation}:
130	      %Equal.sym(Array<Element> & Element,result,(output,value),equation) :
131	        StateEvidence<Reader,Element,Context,reader,depth,
132	          Traversal.update_current(~Reader,~Element,~Value,~Context,~read,~combine,~destination,reader,position,context,_)>
133	      update_sample(~Reader,~Element,~Value,~Context,~combine,~destination,depth,reader,position,context,output,value,
134	        read(reader,context,position),output_evidence,sample)
135	
136	def update_step(~Reader: Type,~Element: Data,~Value: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
137	  ~read: Reader -> Context -> U32 -> Reader & Value,~combine: Element -> Value -> Element,~destination: Context -> U32 -> U32,
138	  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) ->
139	    Sample<Reader,Value,reader,read(reader,context,index)>,
140	  +depth: Nat,-reader: Reader,-state: Traversal.State<&1,&1,Reader,Array<Element>,Context>,
141	  reader_evidence: ReaderEvidence(reader),evidence: StateEvidence<Reader,Element,Context,reader,depth,state>) ->
142	  StateEvidence<Reader,Element,Context,reader,depth,
143	    Traversal.update_step(~Reader,~Element,~Value,~Context,~read,~combine,~destination,state)>:
144	  match evidence:
145	    case StateEvidence{output,+position,+context,equation,+output_evidence}:
146	      %Equal.sym(Traversal.State<&1,&1,Reader,Array<Element>,Context>,state,Traversal.State{reader,output,position,context},equation) :
147	        StateEvidence<Reader,Element,Context,reader,depth,
148	          Traversal.update_step(~Reader,~Element,~Value,~Context,~read,~combine,~destination,_)>
149	      update_current(~Reader,~Element,~Value,~Context,~read,~combine,~destination,depth,reader,position,context,output,
150	        Array.get(Element,output,destination(context,position)),output_evidence,
151	        Witness.read(Element,depth,output,destination(context,position),output_evidence),
152	        read_preserves(reader,context,position,reader_evidence))
153	
154	def update(~Reader: Type,~Element: Data,~Value: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
155	  ~read: Reader -> Context -> U32 -> Reader & Value,~combine: Element -> Value -> Element,~destination: Context -> U32 -> U32,
156	  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) ->
157	    Sample<Reader,Value,reader,read(reader,context,index)>,
158	  +depth: Nat,count: Nat,-reader: Reader,-state: Traversal.State<&1,&1,Reader,Array<Element>,Context>,
159	  +reader_evidence: ReaderEvidence(reader),evidence: StateEvidence<Reader,Element,Context,reader,depth,state>) ->
160	  StateEvidence<Reader,Element,Context,reader,depth,
161	    Traversal.update(~Reader,~Element,~Value,~Context,~read,~combine,~destination,count,state)>:
162	  match count:
163	    case 0n: evidence
164	    case 1n+rest:
165	      update(~Reader,~Element,~Value,~Context,~ReaderEvidence,~read,~combine,~destination,~read_preserves,depth,rest,reader,
166	        Traversal.update_step(~Reader,~Element,~Value,~Context,~read,~combine,~destination,state),reader_evidence,
167	        update_step(~Reader,~Element,~Value,~Context,~ReaderEvidence,~read,~combine,~destination,~read_preserves,
168	          depth,reader,state,reader_evidence,evidence))
169	
170	type MapEvidence<-Element: Data,-Context: Data,-depth: Nat,
171	  -state: Traversal.State<&2,&1,Unit,Array<Element>,Context>> is Data:
172	  MapEvidence{-output: Array<Element>,position: U32,context: Context,
173	    equation: {state == Traversal.State{Unit{},output,position,context} : Traversal.State<&2,&1,Unit,Array<Element>,Context>},
174	    output_evidence: Witness.Witness(Element,depth,output)}
175	
176	def mapped_value(~Element: Data,~Context: Data,~map: Context -> Element -> Element,
177	  +depth: Nat,+position: U32,+context: Context,-output: Array<Element>,-result: Array<Element> & Element,
178	  output_evidence: Witness.Witness(Element,depth,output),observed: Witness.Read<Element,output,result>) ->
179	  MapEvidence<Element,Context,depth,Traversal.mapped_value(~Element,~Context,~map,position,context,result)>:
180	  match observed:
181	    case Witness.Read{value,equation}:
182	      %Equal.sym(Array<Element> & Element,result,(output,value),equation) :
183	        MapEvidence<Element,Context,depth,Traversal.mapped_value(~Element,~Context,~map,position,context,_)>
184	      MapEvidence{Array.set(Element,output,position,map(context,value)),(position + 1 : U32),context,{==},
185	        Witness.write(Element,depth,output,position,map(context,value),output_evidence)}
186	
187	def map_step(~Element: Data,~Context: Data,~map: Context -> Element -> Element,+depth: Nat,
188	  -state: Traversal.State<&2,&1,Unit,Array<Element>,Context>,evidence: MapEvidence<Element,Context,depth,state>) ->
189	  MapEvidence<Element,Context,depth,Traversal.map_step(~Element,~Context,~map,state)>:
190	  match evidence:
191	    case MapEvidence{output,+position,+context,equation,+output_evidence}:
192	      %Equal.sym(Traversal.State<&2,&1,Unit,Array<Element>,Context>,state,Traversal.State{Unit{},output,position,context},equation) :
193	        MapEvidence<Element,Context,depth,Traversal.map_step(~Element,~Context,~map,_)>
194	      mapped_value(~Element,~Context,~map,depth,position,context,output,Array.get(Element,output,position),output_evidence,
195	        Witness.read(Element,depth,output,position,output_evidence))
196	
197	def map_run(~Element: Data,~Context: Data,~map: Context -> Element -> Element,+depth: Nat,count: Nat,
198	  -state: Traversal.State<&2,&1,Unit,Array<Element>,Context>,evidence: MapEvidence<Element,Context,depth,state>) ->
199	  MapEvidence<Element,Context,depth,Loop.run(~Traversal.State<&2,&1,Unit,Array<Element>,Context>,~Traversal.map_step(~Element,~Context,~map),count,state)>:
200	  match count:
201	    case 0n: evidence
202	    case 1n+rest:
203	      map_run(~Element,~Context,~map,depth,rest,Traversal.map_step(~Element,~Context,~map,state),
204	        map_step(~Element,~Context,~map,depth,state,evidence))
205	
206	def mapped_output(~Element: Data,~Context: Data,-depth: Nat,-state: Traversal.State<&2,&1,Unit,Array<Element>,Context>,
207	  evidence: MapEvidence<Element,Context,depth,state>) -> Witness.Witness(Element,depth,Traversal.mapped_output(~Element,~Context,state)):
208	  match evidence:
209	    case MapEvidence{output,position,context,equation,output_evidence}:
210	      %Equal.sym(Traversal.State<&2,&1,Unit,Array<Element>,Context>,state,Traversal.State{Unit{},output,position,context},equation) :
211	        Witness.Witness(Element,depth,Traversal.mapped_output(~Element,~Context,_))
212	      output_evidence
213	
214	def map_in_place(~Element: Data,~Context: Data,~map: Context -> Element -> Element,+depth: Nat,count: Nat,
215	  position: U32,context: Context,-output: Array<Element>,evidence: Witness.Witness(Element,depth,output)) ->
216	  Witness.Witness(Element,depth,Traversal.map_in_place(~Element,~Context,~map,count,position,context,output)):
217	  mapped_output(~Element,~Context,depth,
218	    Loop.run(~Traversal.State<&2,&1,Unit,Array<Element>,Context>,~Traversal.map_step(~Element,~Context,~map),count,
219	      Traversal.State{Unit{},output,position,context}),
220	    map_run(~Element,~Context,~map,depth,count,Traversal.State{Unit{},output,position,context},MapEvidence{output,position,context,{==},evidence}))
221	
222	type FoldEvidence<-Reader: Type,-Accumulator: Data,-Context: Data,-reader: Reader,
223	  -state: Traversal.State<&1,&2,Reader,Accumulator,Context>> is Data:
224	  FoldEvidence{-accumulator: Accumulator,position: U32,context: Context,
225	    equation: {state == Traversal.State{reader,accumulator,position,context} : Traversal.State<&1,&2,Reader,Accumulator,Context>}}
226	
227	def fold_value(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data,
228	  ~combine: Accumulator -> Element -> Accumulator,-reader: Reader,-accumulator: Accumulator,+position: U32,context: Context,
229	  -result: Reader & Element,sample: Sample<Reader,Element,reader,result>) ->
230	  FoldEvidence<Reader,Accumulator,Context,reader,
231	    Traversal.fold_value(~Reader,~Element,~Accumulator,~Context,~combine,accumulator,position,context,result)>:
232	  match sample:
233	    case Sample{value,equation}:
234	      %Equal.sym(Reader & Element,result,(reader,value),equation) :
235	        FoldEvidence<Reader,Accumulator,Context,reader,
236	          Traversal.fold_value(~Reader,~Element,~Accumulator,~Context,~combine,accumulator,position,context,_)>
237	      FoldEvidence{combine(accumulator,value),(position + 1 : U32),context,{==}}
238	
239	def fold_step(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
240	  ~read: Reader -> Context -> U32 -> Reader & Element,~combine: Accumulator -> Element -> Accumulator,
241	  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) ->
242	    Sample<Reader,Element,reader,read(reader,context,index)>,
243	  -reader: Reader,-state: Traversal.State<&1,&2,Reader,Accumulator,Context>,reader_evidence: ReaderEvidence(reader),
244	  evidence: FoldEvidence<Reader,Accumulator,Context,reader,state>) ->
245	  FoldEvidence<Reader,Accumulator,Context,reader,Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine,state)>:
246	  match evidence:
247	    case FoldEvidence{accumulator,+position,+context,equation}:
248	      %Equal.sym(Traversal.State<&1,&2,Reader,Accumulator,Context>,state,Traversal.State{reader,accumulator,position,context},equation) :
249	        FoldEvidence<Reader,Accumulator,Context,reader,Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine,_)>
250	      fold_value(~Reader,~Element,~Accumulator,~Context,~combine,reader,accumulator,position,context,read(reader,context,position),
251	        read_preserves(reader,context,position,reader_evidence))
252	
253	def fold_run(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
254	  ~read: Reader -> Context -> U32 -> Reader & Element,~combine: Accumulator -> Element -> Accumulator,
255	  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) ->
256	    Sample<Reader,Element,reader,read(reader,context,index)>,
257	  count: Nat,-reader: Reader,-state: Traversal.State<&1,&2,Reader,Accumulator,Context>,+reader_evidence: ReaderEvidence(reader),
258	  evidence: FoldEvidence<Reader,Accumulator,Context,reader,state>) ->
259	  FoldEvidence<Reader,Accumulator,Context,reader,
260	    Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine),count,state)>:
261	  match count:
262	    case 0n: evidence
263	    case 1n+rest:
264	      fold_run(~Reader,~Element,~Accumulator,~Context,~ReaderEvidence,~read,~combine,~read_preserves,rest,reader,
265	        Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine,state),reader_evidence,
266	        fold_step(~Reader,~Element,~Accumulator,~Context,~ReaderEvidence,~read,~combine,~read_preserves,reader,state,reader_evidence,evidence))
267	
268	def fold_finished(~Reader: Type,~Accumulator: Data,~Context: Data,-reader: Reader,
269	  -state: Traversal.State<&1,&2,Reader,Accumulator,Context>,evidence: FoldEvidence<Reader,Accumulator,Context,reader,state>) ->
270	  {first(~Reader,~Accumulator,Traversal.finish_fold(~Reader,~Accumulator,~Context,state)) == reader : Reader}:
271	  match evidence:
272	    case FoldEvidence{accumulator,position,context,equation}:
273	      %Equal.sym(Traversal.State<&1,&2,Reader,Accumulator,Context>,state,Traversal.State{reader,accumulator,position,context},equation) :
274	        {first(~Reader,~Accumulator,Traversal.finish_fold(~Reader,~Accumulator,~Context,_)) == reader : Reader}
275	      {==}
276	
277	def fold(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
278	  ~read: Reader -> Context -> U32 -> Reader & Element,~combine: Accumulator -> Element -> Accumulator,
279	  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) ->
280	    Sample<Reader,Element,reader,read(reader,context,index)>,
281	  count: Nat,-reader: Reader,position: U32,context: Context,-initial: Accumulator,reader_evidence: ReaderEvidence(reader)) ->
282	  {first(~Reader,~Accumulator,Traversal.fold(~Reader,~Element,~Accumulator,~Context,~read,~combine,count,position,reader,initial,context)) == reader : Reader}:
283	  fold_finished(~Reader,~Accumulator,~Context,reader,
284	    Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine),count,
285	      Traversal.State{reader,initial,position,context}),
286	    fold_run(~Reader,~Element,~Accumulator,~Context,~ReaderEvidence,~read,~combine,~read_preserves,count,reader,
287	      Traversal.State{reader,initial,position,context},reader_evidence,FoldEvidence{initial,position,context,{==}}))