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 strided_read(~Element: Data,-storage: Array<Element>,context: Traversal.Strided,index: U32,
85	  evidence: Witness.ArrayWitness<Element,storage>) ->
86	  Sample<Array<Element>,Element,storage,Traversal.strided(~Element,storage,context,index)>:
87	  Traversal.Strided{base,stride} = context
88	  array_sample(~Element,storage,Array.get(Element,storage,(base + index * stride : U32)),Witness.observed(Element,storage,(base + index * stride : U32),evidence))
89	
90	def first(~Left: Type,~Right: Type,pair: Left & Right) -> Left:
91	  (left,right) = pair
92	  left
93	
94	def second(~Left: Type,~Right: Type,pair: Left & Right) -> Right:
95	  (left,right) = pair
96	  right
97	
98	def source_unchanged(~Reader: Type,~Element: Data,-reader: Reader,-depth: Nat,-result: Reader & Array<Element>,
99	  evidence: ResultEvidence<Reader,Element,reader,depth,result>) -> {first(~Reader,~Array<Element>,result) == reader : Reader}:
100	  match evidence:
101	    case ResultEvidence{output,equation,output_evidence}:
102	      Equal.cong(Reader & Array<Element>,Reader,pair => first(~Reader,~Array<Element>,pair),result,(reader,output),equation)
103	
104	def output_witness(~Reader: Type,~Element: Data,-reader: Reader,-depth: Nat,-result: Reader & Array<Element>,
105	  evidence: ResultEvidence<Reader,Element,reader,depth,result>) -> Witness.Witness(Element,depth,second(~Reader,~Array<Element>,result)):
106	  match evidence:
107	    case ResultEvidence{output,equation,output_evidence}:
108	      %Equal.sym(Reader & Array<Element>,result,(reader,output),equation) : Witness.Witness(Element,depth,second(~Reader,~Array<Element>,_))
109	      output_evidence
110	
111	def update_sample(~Reader: Type,~Element: Data,~Value: Data,~Context: Data,
112	  ~combine: Element -> Value -> Element,~destination: Context -> U32 -> U32,
113	  +depth: Nat,-reader: Reader,+position: U32,+context: Context,-output: Array<Element>,-current: Element,
114	  -result: Reader & Value,output_evidence: Witness.Witness(Element,depth,output),
115	  sample: Sample<Reader,Value,reader,result>) ->
116	  StateEvidence<Reader,Element,Context,reader,depth,
117	    Traversal.update_sample(~Reader,~Element,~Value,~Context,~combine,~destination,position,context,output,current,result)>:
118	  match sample:
119	    case Sample{value,equation}:
120	      %Equal.sym(Reader & Value,result,(reader,value),equation) :
121	        StateEvidence<Reader,Element,Context,reader,depth,
122	          Traversal.update_sample(~Reader,~Element,~Value,~Context,~combine,~destination,position,context,output,current,_)>
123	      StateEvidence{Array.set(Element,output,destination(context,position),combine(current,value)),(position + 1 : U32),context,{==},
124	        Witness.write(Element,depth,output,destination(context,position),combine(current,value),output_evidence)}
125	
126	def update_current(~Reader: Type,~Element: Data,~Value: Data,~Context: Data,
127	  ~read: Reader -> Context -> U32 -> Reader & Value,~combine: Element -> Value -> Element,
128	  ~destination: Context -> U32 -> U32,+depth: Nat,-reader: Reader,+position: U32,+context: Context,
129	  -output: Array<Element>,-result: Array<Element> & Element,
130	  output_evidence: Witness.Witness(Element,depth,output),observed: Witness.Read<Element,output,result>,
131	  sample: Sample<Reader,Value,reader,read(reader,context,position)>) ->
132	  StateEvidence<Reader,Element,Context,reader,depth,
133	    Traversal.update_current(~Reader,~Element,~Value,~Context,~read,~combine,~destination,reader,position,context,result)>:
134	  match observed:
135	    case Witness.Read{value,equation}:
136	      %Equal.sym(Array<Element> & Element,result,(output,value),equation) :
137	        StateEvidence<Reader,Element,Context,reader,depth,
138	          Traversal.update_current(~Reader,~Element,~Value,~Context,~read,~combine,~destination,reader,position,context,_)>
139	      update_sample(~Reader,~Element,~Value,~Context,~combine,~destination,depth,reader,position,context,output,value,
140	        read(reader,context,position),output_evidence,sample)
141	
142	def update_step(~Reader: Type,~Element: Data,~Value: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
143	  ~read: Reader -> Context -> U32 -> Reader & Value,~combine: Element -> Value -> Element,~destination: Context -> U32 -> U32,
144	  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) ->
145	    Sample<Reader,Value,reader,read(reader,context,index)>,
146	  +depth: Nat,-reader: Reader,-state: Traversal.State<&1,&1,Reader,Array<Element>,Context>,
147	  reader_evidence: ReaderEvidence(reader),evidence: StateEvidence<Reader,Element,Context,reader,depth,state>) ->
148	  StateEvidence<Reader,Element,Context,reader,depth,
149	    Traversal.update_step(~Reader,~Element,~Value,~Context,~read,~combine,~destination,state)>:
150	  match evidence:
151	    case StateEvidence{output,+position,+context,equation,+output_evidence}:
152	      %Equal.sym(Traversal.State<&1,&1,Reader,Array<Element>,Context>,state,Traversal.State{reader,output,position,context},equation) :
153	        StateEvidence<Reader,Element,Context,reader,depth,
154	          Traversal.update_step(~Reader,~Element,~Value,~Context,~read,~combine,~destination,_)>
155	      update_current(~Reader,~Element,~Value,~Context,~read,~combine,~destination,depth,reader,position,context,output,
156	        Array.get(Element,output,destination(context,position)),output_evidence,
157	        Witness.read(Element,depth,output,destination(context,position),output_evidence),
158	        read_preserves(reader,context,position,reader_evidence))
159	
160	def update(~Reader: Type,~Element: Data,~Value: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
161	  ~read: Reader -> Context -> U32 -> Reader & Value,~combine: Element -> Value -> Element,~destination: Context -> U32 -> U32,
162	  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) ->
163	    Sample<Reader,Value,reader,read(reader,context,index)>,
164	  +depth: Nat,count: Nat,-reader: Reader,-state: Traversal.State<&1,&1,Reader,Array<Element>,Context>,
165	  +reader_evidence: ReaderEvidence(reader),evidence: StateEvidence<Reader,Element,Context,reader,depth,state>) ->
166	  StateEvidence<Reader,Element,Context,reader,depth,
167	    Traversal.update(~Reader,~Element,~Value,~Context,~read,~combine,~destination,count,state)>:
168	  match count:
169	    case 0n: evidence
170	    case 1n+rest:
171	      update(~Reader,~Element,~Value,~Context,~ReaderEvidence,~read,~combine,~destination,~read_preserves,depth,rest,reader,
172	        Traversal.update_step(~Reader,~Element,~Value,~Context,~read,~combine,~destination,state),reader_evidence,
173	        update_step(~Reader,~Element,~Value,~Context,~ReaderEvidence,~read,~combine,~destination,~read_preserves,
174	          depth,reader,state,reader_evidence,evidence))
175	
176	type MapEvidence<-Element: Data,-Context: Data,-depth: Nat,
177	  -state: Traversal.State<&2,&1,Unit,Array<Element>,Context>> is Data:
178	  MapEvidence{-output: Array<Element>,position: U32,context: Context,
179	    equation: {state == Traversal.State{Unit{},output,position,context} : Traversal.State<&2,&1,Unit,Array<Element>,Context>},
180	    output_evidence: Witness.Witness(Element,depth,output)}
181	
182	def mapped_value(~Element: Data,~Context: Data,~map: Context -> Element -> Element,
183	  +depth: Nat,+position: U32,+context: Context,-output: Array<Element>,-result: Array<Element> & Element,
184	  output_evidence: Witness.Witness(Element,depth,output),observed: Witness.Read<Element,output,result>) ->
185	  MapEvidence<Element,Context,depth,Traversal.mapped_value(~Element,~Context,~map,position,context,result)>:
186	  match observed:
187	    case Witness.Read{value,equation}:
188	      %Equal.sym(Array<Element> & Element,result,(output,value),equation) :
189	        MapEvidence<Element,Context,depth,Traversal.mapped_value(~Element,~Context,~map,position,context,_)>
190	      MapEvidence{Array.set(Element,output,position,map(context,value)),(position + 1 : U32),context,{==},
191	        Witness.write(Element,depth,output,position,map(context,value),output_evidence)}
192	
193	def map_step(~Element: Data,~Context: Data,~map: Context -> Element -> Element,+depth: Nat,
194	  -state: Traversal.State<&2,&1,Unit,Array<Element>,Context>,evidence: MapEvidence<Element,Context,depth,state>) ->
195	  MapEvidence<Element,Context,depth,Traversal.map_step(~Element,~Context,~map,state)>:
196	  match evidence:
197	    case MapEvidence{output,+position,+context,equation,+output_evidence}:
198	      %Equal.sym(Traversal.State<&2,&1,Unit,Array<Element>,Context>,state,Traversal.State{Unit{},output,position,context},equation) :
199	        MapEvidence<Element,Context,depth,Traversal.map_step(~Element,~Context,~map,_)>
200	      mapped_value(~Element,~Context,~map,depth,position,context,output,Array.get(Element,output,position),output_evidence,
201	        Witness.read(Element,depth,output,position,output_evidence))
202	
203	def map_run(~Element: Data,~Context: Data,~map: Context -> Element -> Element,+depth: Nat,count: Nat,
204	  -state: Traversal.State<&2,&1,Unit,Array<Element>,Context>,evidence: MapEvidence<Element,Context,depth,state>) ->
205	  MapEvidence<Element,Context,depth,Loop.run(~Traversal.State<&2,&1,Unit,Array<Element>,Context>,~Traversal.map_step(~Element,~Context,~map),count,state)>:
206	  match count:
207	    case 0n: evidence
208	    case 1n+rest:
209	      map_run(~Element,~Context,~map,depth,rest,Traversal.map_step(~Element,~Context,~map,state),
210	        map_step(~Element,~Context,~map,depth,state,evidence))
211	
212	def mapped_output(~Element: Data,~Context: Data,-depth: Nat,-state: Traversal.State<&2,&1,Unit,Array<Element>,Context>,
213	  evidence: MapEvidence<Element,Context,depth,state>) -> Witness.Witness(Element,depth,Traversal.mapped_output(~Element,~Context,state)):
214	  match evidence:
215	    case MapEvidence{output,position,context,equation,output_evidence}:
216	      %Equal.sym(Traversal.State<&2,&1,Unit,Array<Element>,Context>,state,Traversal.State{Unit{},output,position,context},equation) :
217	        Witness.Witness(Element,depth,Traversal.mapped_output(~Element,~Context,_))
218	      output_evidence
219	
220	def map_in_place(~Element: Data,~Context: Data,~map: Context -> Element -> Element,+depth: Nat,count: Nat,
221	  position: U32,context: Context,-output: Array<Element>,evidence: Witness.Witness(Element,depth,output)) ->
222	  Witness.Witness(Element,depth,Traversal.map_in_place(~Element,~Context,~map,count,position,context,output)):
223	  mapped_output(~Element,~Context,depth,
224	    Loop.run(~Traversal.State<&2,&1,Unit,Array<Element>,Context>,~Traversal.map_step(~Element,~Context,~map),count,
225	      Traversal.State{Unit{},output,position,context}),
226	    map_run(~Element,~Context,~map,depth,count,Traversal.State{Unit{},output,position,context},MapEvidence{output,position,context,{==},evidence}))
227	
228	type FoldEvidence<-Reader: Type,-Accumulator: Data,-Context: Data,-reader: Reader,
229	  -state: Traversal.State<&1,&2,Reader,Accumulator,Context>> is Data:
230	  FoldEvidence{-accumulator: Accumulator,position: U32,context: Context,
231	    equation: {state == Traversal.State{reader,accumulator,position,context} : Traversal.State<&1,&2,Reader,Accumulator,Context>}}
232	
233	def fold_value(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data,
234	  ~combine: Accumulator -> Element -> Accumulator,-reader: Reader,-accumulator: Accumulator,+position: U32,context: Context,
235	  -result: Reader & Element,sample: Sample<Reader,Element,reader,result>) ->
236	  FoldEvidence<Reader,Accumulator,Context,reader,
237	    Traversal.fold_value(~Reader,~Element,~Accumulator,~Context,~combine,accumulator,position,context,result)>:
238	  match sample:
239	    case Sample{value,equation}:
240	      %Equal.sym(Reader & Element,result,(reader,value),equation) :
241	        FoldEvidence<Reader,Accumulator,Context,reader,
242	          Traversal.fold_value(~Reader,~Element,~Accumulator,~Context,~combine,accumulator,position,context,_)>
243	      FoldEvidence{combine(accumulator,value),(position + 1 : U32),context,{==}}
244	
245	def fold_step(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
246	  ~read: Reader -> Context -> U32 -> Reader & Element,~combine: Accumulator -> Element -> Accumulator,
247	  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) ->
248	    Sample<Reader,Element,reader,read(reader,context,index)>,
249	  -reader: Reader,-state: Traversal.State<&1,&2,Reader,Accumulator,Context>,reader_evidence: ReaderEvidence(reader),
250	  evidence: FoldEvidence<Reader,Accumulator,Context,reader,state>) ->
251	  FoldEvidence<Reader,Accumulator,Context,reader,Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine,state)>:
252	  match evidence:
253	    case FoldEvidence{accumulator,+position,+context,equation}:
254	      %Equal.sym(Traversal.State<&1,&2,Reader,Accumulator,Context>,state,Traversal.State{reader,accumulator,position,context},equation) :
255	        FoldEvidence<Reader,Accumulator,Context,reader,Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine,_)>
256	      fold_value(~Reader,~Element,~Accumulator,~Context,~combine,reader,accumulator,position,context,read(reader,context,position),
257	        read_preserves(reader,context,position,reader_evidence))
258	
259	def fold_run(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
260	  ~read: Reader -> Context -> U32 -> Reader & Element,~combine: Accumulator -> Element -> Accumulator,
261	  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) ->
262	    Sample<Reader,Element,reader,read(reader,context,index)>,
263	  count: Nat,-reader: Reader,-state: Traversal.State<&1,&2,Reader,Accumulator,Context>,+reader_evidence: ReaderEvidence(reader),
264	  evidence: FoldEvidence<Reader,Accumulator,Context,reader,state>) ->
265	  FoldEvidence<Reader,Accumulator,Context,reader,
266	    Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine),count,state)>:
267	  match count:
268	    case 0n: evidence
269	    case 1n+rest:
270	      fold_run(~Reader,~Element,~Accumulator,~Context,~ReaderEvidence,~read,~combine,~read_preserves,rest,reader,
271	        Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine,state),reader_evidence,
272	        fold_step(~Reader,~Element,~Accumulator,~Context,~ReaderEvidence,~read,~combine,~read_preserves,reader,state,reader_evidence,evidence))
273	
274	def fold_finished(~Reader: Type,~Accumulator: Data,~Context: Data,-reader: Reader,
275	  -state: Traversal.State<&1,&2,Reader,Accumulator,Context>,evidence: FoldEvidence<Reader,Accumulator,Context,reader,state>) ->
276	  {first(~Reader,~Accumulator,Traversal.finish_fold(~Reader,~Accumulator,~Context,state)) == reader : Reader}:
277	  match evidence:
278	    case FoldEvidence{accumulator,position,context,equation}:
279	      %Equal.sym(Traversal.State<&1,&2,Reader,Accumulator,Context>,state,Traversal.State{reader,accumulator,position,context},equation) :
280	        {first(~Reader,~Accumulator,Traversal.finish_fold(~Reader,~Accumulator,~Context,_)) == reader : Reader}
281	      {==}
282	
283	def fold(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
284	  ~read: Reader -> Context -> U32 -> Reader & Element,~combine: Accumulator -> Element -> Accumulator,
285	  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) ->
286	    Sample<Reader,Element,reader,read(reader,context,index)>,
287	  count: Nat,-reader: Reader,position: U32,context: Context,-initial: Accumulator,reader_evidence: ReaderEvidence(reader)) ->
288	  {first(~Reader,~Accumulator,Traversal.fold(~Reader,~Element,~Accumulator,~Context,~read,~combine,count,position,reader,initial,context)) == reader : Reader}:
289	  fold_finished(~Reader,~Accumulator,~Context,reader,
290	    Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine),count,
291	      Traversal.State{reader,initial,position,context}),
292	    fold_run(~Reader,~Element,~Accumulator,~Context,~ReaderEvidence,~read,~combine,~read_preserves,count,reader,
293	      Traversal.State{reader,initial,position,context},reader_evidence,FoldEvidence{initial,position,context,{==}}))
294	
295	# The eight reads of a round hand the reader back.
296	def read_last(~Reader: Type,~Element: Data,-reader: Reader,-a: Element,-b: Element,-c: Element,-d: Element,-e: Element,-f: Element,-g: Element,
297	  -result: Reader & Element,sample: Sample<Reader,Element,reader,result>) ->
298	  Sample<Reader,Traversal.Eight<Element>,reader,Traversal.read_last(~Reader,~Element,a,b,c,d,e,f,g,result)>:
299	  match sample:
300	    case Sample{value,equation}:
301	      %Equal.sym(Reader & Element,result,(reader,value),equation) :
302	        Sample<Reader,Traversal.Eight<Element>,reader,Traversal.read_last(~Reader,~Element,a,b,c,d,e,f,g,_)>
303	      Sample{Traversal.Eight{a,b,c,d,e,f,g,value},{==}}
304	
305	def read_seventh(~Reader: Type,~Element: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,~read: Reader -> Context -> U32 -> Reader & Element,
306	  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) -> Sample<Reader,Element,reader,read(reader,context,index)>,
307	  -reader: Reader,+position: U32,+context: Context,-a: Element,-b: Element,-c: Element,-d: Element,-e: Element,-f: Element,
308	  -result: Reader & Element,+reader_evidence: ReaderEvidence(reader),sample: Sample<Reader,Element,reader,result>) ->
309	  Sample<Reader,Traversal.Eight<Element>,reader,Traversal.read_seventh(~Reader,~Element,~Context,~read,position,context,a,b,c,d,e,f,result)>:
310	  match sample:
311	    case Sample{value,equation}:
312	      %Equal.sym(Reader & Element,result,(reader,value),equation) :
313	        Sample<Reader,Traversal.Eight<Element>,reader,Traversal.read_seventh(~Reader,~Element,~Context,~read,position,context,a,b,c,d,e,f,_)>
314	      read_last(~Reader,~Element,reader,a,b,c,d,e,f,value,read(reader,context,(position + 1 : U32)),read_preserves(reader,context,(position + 1 : U32),reader_evidence))
315	
316	def read_sixth(~Reader: Type,~Element: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,~read: Reader -> Context -> U32 -> Reader & Element,
317	  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) -> Sample<Reader,Element,reader,read(reader,context,index)>,
318	  -reader: Reader,+position: U32,+context: Context,-a: Element,-b: Element,-c: Element,-d: Element,-e: Element,
319	  -result: Reader & Element,+reader_evidence: ReaderEvidence(reader),sample: Sample<Reader,Element,reader,result>) ->
320	  Sample<Reader,Traversal.Eight<Element>,reader,Traversal.read_sixth(~Reader,~Element,~Context,~read,position,context,a,b,c,d,e,result)>:
321	  match sample:
322	    case Sample{value,equation}:
323	      %Equal.sym(Reader & Element,result,(reader,value),equation) :
324	        Sample<Reader,Traversal.Eight<Element>,reader,Traversal.read_sixth(~Reader,~Element,~Context,~read,position,context,a,b,c,d,e,_)>
325	      read_seventh(~Reader,~Element,~Context,~ReaderEvidence,~read,~read_preserves,reader,(position + 1 : U32),context,a,b,c,d,e,value,
326	        read(reader,context,(position + 1 : U32)),reader_evidence,read_preserves(reader,context,(position + 1 : U32),reader_evidence))
327	
328	def read_fifth(~Reader: Type,~Element: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,~read: Reader -> Context -> U32 -> Reader & Element,
329	  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) -> Sample<Reader,Element,reader,read(reader,context,index)>,
330	  -reader: Reader,+position: U32,+context: Context,-a: Element,-b: Element,-c: Element,-d: Element,
331	  -result: Reader & Element,+reader_evidence: ReaderEvidence(reader),sample: Sample<Reader,Element,reader,result>) ->
332	  Sample<Reader,Traversal.Eight<Element>,reader,Traversal.read_fifth(~Reader,~Element,~Context,~read,position,context,a,b,c,d,result)>:
333	  match sample:
334	    case Sample{value,equation}:
335	      %Equal.sym(Reader & Element,result,(reader,value),equation) :
336	        Sample<Reader,Traversal.Eight<Element>,reader,Traversal.read_fifth(~Reader,~Element,~Context,~read,position,context,a,b,c,d,_)>
337	      read_sixth(~Reader,~Element,~Context,~ReaderEvidence,~read,~read_preserves,reader,(position + 1 : U32),context,a,b,c,d,value,
338	        read(reader,context,(position + 1 : U32)),reader_evidence,read_preserves(reader,context,(position + 1 : U32),reader_evidence))
339	
340	def read_fourth(~Reader: Type,~Element: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,~read: Reader -> Context -> U32 -> Reader & Element,
341	  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) -> Sample<Reader,Element,reader,read(reader,context,index)>,
342	  -reader: Reader,+position: U32,+context: Context,-a: Element,-b: Element,-c: Element,
343	  -result: Reader & Element,+reader_evidence: ReaderEvidence(reader),sample: Sample<Reader,Element,reader,result>) ->
344	  Sample<Reader,Traversal.Eight<Element>,reader,Traversal.read_fourth(~Reader,~Element,~Context,~read,position,context,a,b,c,result)>:
345	  match sample:
346	    case Sample{value,equation}:
347	      %Equal.sym(Reader & Element,result,(reader,value),equation) :
348	        Sample<Reader,Traversal.Eight<Element>,reader,Traversal.read_fourth(~Reader,~Element,~Context,~read,position,context,a,b,c,_)>
349	      read_fifth(~Reader,~Element,~Context,~ReaderEvidence,~read,~read_preserves,reader,(position + 1 : U32),context,a,b,c,value,
350	        read(reader,context,(position + 1 : U32)),reader_evidence,read_preserves(reader,context,(position + 1 : U32),reader_evidence))
351	
352	def read_third(~Reader: Type,~Element: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,~read: Reader -> Context -> U32 -> Reader & Element,
353	  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) -> Sample<Reader,Element,reader,read(reader,context,index)>,
354	  -reader: Reader,+position: U32,+context: Context,-a: Element,-b: Element,
355	  -result: Reader & Element,+reader_evidence: ReaderEvidence(reader),sample: Sample<Reader,Element,reader,result>) ->
356	  Sample<Reader,Traversal.Eight<Element>,reader,Traversal.read_third(~Reader,~Element,~Context,~read,position,context,a,b,result)>:
357	  match sample:
358	    case Sample{value,equation}:
359	      %Equal.sym(Reader & Element,result,(reader,value),equation) :
360	        Sample<Reader,Traversal.Eight<Element>,reader,Traversal.read_third(~Reader,~Element,~Context,~read,position,context,a,b,_)>
361	      read_fourth(~Reader,~Element,~Context,~ReaderEvidence,~read,~read_preserves,reader,(position + 1 : U32),context,a,b,value,
362	        read(reader,context,(position + 1 : U32)),reader_evidence,read_preserves(reader,context,(position + 1 : U32),reader_evidence))
363	
364	def read_second(~Reader: Type,~Element: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,~read: Reader -> Context -> U32 -> Reader & Element,
365	  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) -> Sample<Reader,Element,reader,read(reader,context,index)>,
366	  -reader: Reader,+position: U32,+context: Context,-a: Element,
367	  -result: Reader & Element,+reader_evidence: ReaderEvidence(reader),sample: Sample<Reader,Element,reader,result>) ->
368	  Sample<Reader,Traversal.Eight<Element>,reader,Traversal.read_second(~Reader,~Element,~Context,~read,position,context,a,result)>:
369	  match sample:
370	    case Sample{value,equation}:
371	      %Equal.sym(Reader & Element,result,(reader,value),equation) :
372	        Sample<Reader,Traversal.Eight<Element>,reader,Traversal.read_second(~Reader,~Element,~Context,~read,position,context,a,_)>
373	      read_third(~Reader,~Element,~Context,~ReaderEvidence,~read,~read_preserves,reader,(position + 1 : U32),context,a,value,
374	        read(reader,context,(position + 1 : U32)),reader_evidence,read_preserves(reader,context,(position + 1 : U32),reader_evidence))
375	
376	def read_eight(~Reader: Type,~Element: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,~read: Reader -> Context -> U32 -> Reader & Element,
377	  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) -> Sample<Reader,Element,reader,read(reader,context,index)>,
378	  -reader: Reader,+position: U32,+context: Context,
379	  -result: Reader & Element,+reader_evidence: ReaderEvidence(reader),sample: Sample<Reader,Element,reader,result>) ->
380	  Sample<Reader,Traversal.Eight<Element>,reader,Traversal.read_eight(~Reader,~Element,~Context,~read,position,context,result)>:
381	  match sample:
382	    case Sample{value,equation}:
383	      %Equal.sym(Reader & Element,result,(reader,value),equation) :
384	        Sample<Reader,Traversal.Eight<Element>,reader,Traversal.read_eight(~Reader,~Element,~Context,~read,position,context,_)>
385	      read_second(~Reader,~Element,~Context,~ReaderEvidence,~read,~read_preserves,reader,(position + 1 : U32),context,value,
386	        read(reader,context,(position + 1 : U32)),reader_evidence,read_preserves(reader,context,(position + 1 : U32),reader_evidence))
387	
388	def round_value(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data,~combine: Accumulator -> Element -> Accumulator,
389	  -reader: Reader,-accumulator: Accumulator,+position: U32,context: Context,
390	  -result: Reader & Traversal.Eight<Element>,sample: Sample<Reader,Traversal.Eight<Element>,reader,result>) ->
391	  FoldEvidence<Reader,Accumulator,Context,reader,Traversal.round_value(~Reader,~Element,~Accumulator,~Context,~combine,accumulator,position,context,result)>:
392	  match sample:
393	    case Sample{values,equation}:
394	      %Equal.sym(Reader & Traversal.Eight<Element>,result,(reader,values),equation) :
395	        FoldEvidence<Reader,Accumulator,Context,reader,Traversal.round_value(~Reader,~Element,~Accumulator,~Context,~combine,accumulator,position,context,_)>
396	      FoldEvidence{Traversal.combine_eight(~Element,~Accumulator,~combine,accumulator,values),Traversal.after_eight(position),context,{==}}
397	
398	def fold_round(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
399	  ~read: Reader -> Context -> U32 -> Reader & Element,~combine: Accumulator -> Element -> Accumulator,
400	  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) ->
401	    Sample<Reader,Element,reader,read(reader,context,index)>,
402	  -reader: Reader,-state: Traversal.State<&1,&2,Reader,Accumulator,Context>,+reader_evidence: ReaderEvidence(reader),
403	  evidence: FoldEvidence<Reader,Accumulator,Context,reader,state>) ->
404	  FoldEvidence<Reader,Accumulator,Context,reader,Traversal.fold_round(~Reader,~Element,~Accumulator,~Context,~read,~combine,state)>:
405	  match evidence:
406	    case FoldEvidence{accumulator,+position,+context,equation}:
407	      %Equal.sym(Traversal.State<&1,&2,Reader,Accumulator,Context>,state,Traversal.State{reader,accumulator,position,context},equation) :
408	        FoldEvidence<Reader,Accumulator,Context,reader,Traversal.fold_round(~Reader,~Element,~Accumulator,~Context,~read,~combine,_)>
409	      round_value(~Reader,~Element,~Accumulator,~Context,~combine,reader,accumulator,position,context,
410	        Traversal.read_eight(~Reader,~Element,~Context,~read,position,context,read(reader,context,position)),
411	        read_eight(~Reader,~Element,~Context,~ReaderEvidence,~read,~read_preserves,reader,position,context,read(reader,context,position),reader_evidence,
412	          read_preserves(reader,context,position,reader_evidence)))
413	
414	def rounds_run(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
415	  ~read: Reader -> Context -> U32 -> Reader & Element,~combine: Accumulator -> Element -> Accumulator,
416	  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) ->
417	    Sample<Reader,Element,reader,read(reader,context,index)>,
418	  count: Nat,-reader: Reader,-state: Traversal.State<&1,&2,Reader,Accumulator,Context>,+reader_evidence: ReaderEvidence(reader),
419	  evidence: FoldEvidence<Reader,Accumulator,Context,reader,state>) ->
420	  FoldEvidence<Reader,Accumulator,Context,reader,
421	    Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_round(~Reader,~Element,~Accumulator,~Context,~read,~combine),count,state)>:
422	  match count:
423	    case 0n: evidence
424	    case 1n+rest:
425	      rounds_run(~Reader,~Element,~Accumulator,~Context,~ReaderEvidence,~read,~combine,~read_preserves,rest,reader,
426	        Traversal.fold_round(~Reader,~Element,~Accumulator,~Context,~read,~combine,state),reader_evidence,
427	        fold_round(~Reader,~Element,~Accumulator,~Context,~ReaderEvidence,~read,~combine,~read_preserves,reader,state,reader_evidence,evidence))
428	
429	def rounds(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
430	  ~read: Reader -> Context -> U32 -> Reader & Element,~combine: Accumulator -> Element -> Accumulator,
431	  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) ->
432	    Sample<Reader,Element,reader,read(reader,context,index)>,
433	  +count: Nat,-reader: Reader,position: U32,context: Context,-initial: Accumulator,+reader_evidence: ReaderEvidence(reader)) ->
434	  FoldEvidence<Reader,Accumulator,Context,reader,
435	    Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_round(~Reader,~Element,~Accumulator,~Context,~read,~combine),Nat.div(count,8n),
436	      Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine),Nat.mod(count,8n),
437	        Traversal.State{reader,initial,position,context}))>:
438	  rounds_run(~Reader,~Element,~Accumulator,~Context,~ReaderEvidence,~read,~combine,~read_preserves,Nat.div(count,8n),reader,
439	    Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine),Nat.mod(count,8n),
440	      Traversal.State{reader,initial,position,context}),reader_evidence,
441	    fold_run(~Reader,~Element,~Accumulator,~Context,~ReaderEvidence,~read,~combine,~read_preserves,Nat.mod(count,8n),reader,
442	      Traversal.State{reader,initial,position,context},reader_evidence,FoldEvidence{initial,position,context,{==}}))
443	
444	def fold_rounds(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
445	  ~read: Reader -> Context -> U32 -> Reader & Element,~combine: Accumulator -> Element -> Accumulator,
446	  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) ->
447	    Sample<Reader,Element,reader,read(reader,context,index)>,
448	  +count: Nat,-reader: Reader,position: U32,context: Context,-initial: Accumulator,+reader_evidence: ReaderEvidence(reader)) ->
449	  {first(~Reader,~Accumulator,Traversal.fold_rounds(~Reader,~Element,~Accumulator,~Context,~read,~combine,count,position,reader,initial,context)) == reader : Reader}:
450	  fold_finished(~Reader,~Accumulator,~Context,reader,
451	    Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_round(~Reader,~Element,~Accumulator,~Context,~read,~combine),Nat.div(count,8n),
452	      Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine),Nat.mod(count,8n),
453	        Traversal.State{reader,initial,position,context})),
454	    rounds(~Reader,~Element,~Accumulator,~Context,~ReaderEvidence,~read,~combine,~read_preserves,count,reader,position,context,initial,reader_evidence))