proofs/traversal_witness.bend
stelliferous@0.0.3.0 · 454 lines · 0 definitions
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.
4import Base
5import stelliferous@0.0.3.0/traversal_loop.bend as Loop
6import stelliferous@0.0.3.0/traversal_array.bend as Traversal
7import stelliferous@0.0.3.0/proofs/storage_witness.bend as Witness
8
9type Sample<-Reader: Type,-Element: Data,-reader: Reader,-result: Reader & Element> is Data:
10 Sample{-value: Element,equation: {result == (reader,value) : Reader & Element}}
11
12type 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
18def 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
29def 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
43def 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
57type 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
61def 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
70def array_evidence(~Element: Data,-storage: Array<Element>) -> Data:
71 Witness.ArrayWitness<Element,storage>
72
73def 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
78def 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
84def 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
90def first(~Left: Type,~Right: Type,pair: Left & Right) -> Left:
91 (left,right) = pair
92 left
93
94def second(~Left: Type,~Right: Type,pair: Left & Right) -> Right:
95 (left,right) = pair
96 right
97
98def 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
104def 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
111def 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
126def 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
142def 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
160def 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
176type 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
182def 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
193def 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
203def 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
212def 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
220def 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
228type 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
233def 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
245def 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
259def 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
274def 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
283def 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.
296def 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
305def 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
316def 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
328def 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
340def 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
352def 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
364def 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
376def 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
388def 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
398def 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
414def 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
429def 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
444def 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))