proofs/tensor_access_certificate.bend
stelliferous@0.0.3.0 · 403 lines · 0 definitions
1# Discharge the reader premises for the actual tensor traversal kernels.
2# Public operations use only the flat certificates returned at their boundary.
3import Base
4import stelliferous@0.0.3.0/tensor_access.bend as Access
5import stelliferous@0.0.3.0/tensor_view.bend as Views
6import stelliferous@0.0.3.0/traversal_array.bend as Traversal
7import stelliferous@0.0.3.0/traversal_loop.bend as Loop
8import stelliferous@0.0.3.0/tensor_cursor.bend as Cursor
9import stelliferous@0.0.3.0/proofs/tensor_cursor_witness.bend as CursorWitness
10import stelliferous@0.0.3.0/proofs/traversal_visit_witness.bend as VisitWitness
11import stelliferous@0.0.3.0/proofs/storage_certificate.bend as Certificate
12import stelliferous@0.0.3.0/proofs/storage_tree_model.bend as Tree
13import stelliferous@0.0.3.0/proofs/storage_witness.bend as Witness
14import stelliferous@0.0.3.0/proofs/traversal_witness.bend as TraversalWitness
15import stelliferous@0.0.3.0/proofs/traversal_certificate.bend as TraversalCertificate
16
17def read_index(~Element: Data,-input: Array<Element>,context: Unit,index: U32,evidence: Witness.ArrayWitness<Element,input>) ->
18 TraversalWitness.Sample<Array<Element>,Element,input,Traversal.read_index(~Element,input,context,index)>:
19 TraversalWitness.array_sample(~Element,input,Array.get(Element,input,index),Witness.observed(Element,input,index,evidence))
20
21type CopyCall is Data:
22 CopyCall{fast: Bool,count: Nat,source: Views.View,destination: U32}
23
24def copy_operation(~Element: Data,call: CopyCall,input: Array<Element>,output: Array<Element>) -> Array<Element> & Array<Element>:
25 CopyCall{fast,count,source,destination} = call
26 Access.copy_run(~Element,fast,count,source,destination,input,output)
27
28def combine_operation(~Element: Data,~operation: Element -> Element -> Element,call: CopyCall,input: Array<Element>,output: Array<Element>) -> Array<Element> & Array<Element>:
29 CopyCall{fast,count,source,destination} = call
30 Access.combine_run(~Element,~operation,fast,count,source,destination,input,output)
31
32# A strided operation keeps its owners through each part of a run: the stride
33# steps, the state handed to the cursor, and the cursor step that ends the run.
34# The lemmas are generic in the two element steps and in the evidence that
35# each of them keeps.
36def last_of_run(~Element: Data,+depth: Nat,extent: Nat,stride: U32,rewind: U32,rest: Cursor.Depth1(),-input: Array<Element>,
37 -state: Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Stride>,
38 evidence: TraversalWitness.StateEvidence<Array<Element>,Element,Cursor.Stride,input,depth,state>) ->
39 TraversalWitness.StateEvidence<Array<Element>,Element,Cursor.Cursor,input,depth,Access.last_of_run(~Element,extent,stride,rewind,rest,state)>:
40 match evidence:
41 case TraversalWitness.StateEvidence{output,position,Cursor.Stride{address,step},equation,output_evidence}:
42 %Equal.sym(Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Stride>,state,Traversal.State{input,output,position,Cursor.Stride{address,step}},equation) :
43 TraversalWitness.StateEvidence<Array<Element>,Element,Cursor.Cursor,input,depth,Access.last_of_run(~Element,extent,stride,rewind,rest,_)>
44 TraversalWitness.StateEvidence{output,position,Cursor.Cursor{Cursor.Level{Cursor.Axis{extent,1n,stride,rewind},rest},address},{==},output_evidence}
45
46# A step keeps the evidence of its state.
47def Keeps(~Element: Data,~Context: Data,~step: Traversal.State<&1,&1,Array<Element>,Array<Element>,Context> -> Traversal.State<&1,&1,Array<Element>,Array<Element>,Context>) -> Type:
48 @+depth: Nat -> @-input: Array<Element> -> @-state: Traversal.State<&1,&1,Array<Element>,Array<Element>,Context> -> Witness.ArrayWitness<Element,input> ->
49 TraversalWitness.StateEvidence<Array<Element>,Element,Context,input,depth,state> -> TraversalWitness.StateEvidence<Array<Element>,Element,Context,input,depth,step(state)>
50
51def loop(~Element: Data,~Context: Data,~step: Traversal.State<&1,&1,Array<Element>,Array<Element>,Context> -> Traversal.State<&1,&1,Array<Element>,Array<Element>,Context>,
52 ~keeps: Keeps(~Element,~Context,~step),
53 +depth: Nat,count: Nat,-input: Array<Element>,-state: Traversal.State<&1,&1,Array<Element>,Array<Element>,Context>,+input_evidence: Witness.ArrayWitness<Element,input>,
54 evidence: TraversalWitness.StateEvidence<Array<Element>,Element,Context,input,depth,state>) ->
55 TraversalWitness.StateEvidence<Array<Element>,Element,Context,input,depth,Loop.run(~Traversal.State<&1,&1,Array<Element>,Array<Element>,Context>,~step,count,state)>:
56 match count:
57 case 0n: evidence
58 case 1n+rest:
59 loop(~Element,~Context,~step,~keeps,depth,rest,input,step(state),input_evidence,keeps(depth,input,state,input_evidence,evidence))
60
61def run_axis(~Element: Data,~inside: Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Stride> -> Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Stride>,~last: Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor> -> Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor>,
62 ~inside_keeps: Keeps(~Element,~Cursor.Stride,~inside),
63 ~last_keeps: Keeps(~Element,~Cursor.Cursor,~last),
64 +depth: Nat,remaining: Nat,extent: Nat,+stride: U32,rewind: U32,rest: Cursor.Depth1(),+address: U32,
65 -input: Array<Element>,-output: Array<Element>,position: U32,+input_evidence: Witness.ArrayWitness<Element,input>,
66 output_evidence: Witness.Witness(Element,depth,output)) ->
67 TraversalWitness.StateEvidence<Array<Element>,Element,Cursor.Cursor,input,depth,Access.run_axis(~Element,~inside,~last,remaining,extent,stride,rewind,rest,address,input,output,position)>:
68 match remaining:
69 case 0n:
70 last_keeps(depth,input,Traversal.State{input,output,position,Cursor.Cursor{Cursor.Level{Cursor.Axis{extent,0n,stride,rewind},rest},address}},input_evidence,
71 TraversalWitness.StateEvidence{output,position,Cursor.Cursor{Cursor.Level{Cursor.Axis{extent,0n,stride,rewind},rest},address},{==},output_evidence})
72 case 1n+count:
73 last_keeps(depth,input,
74 Access.last_of_run(~Element,extent,stride,rewind,rest,Loop.run(~Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Stride>,~inside,count,Traversal.State{input,output,position,Cursor.Stride{address,stride}})),
75 input_evidence,
76 last_of_run(~Element,depth,extent,stride,rewind,rest,input,Loop.run(~Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Stride>,~inside,count,Traversal.State{input,output,position,Cursor.Stride{address,stride}}),
77 loop(~Element,~Cursor.Stride,~inside,~inside_keeps,depth,count,input,Traversal.State{input,output,position,Cursor.Stride{address,stride}},input_evidence,
78 TraversalWitness.StateEvidence{output,position,Cursor.Stride{address,stride},{==},output_evidence})))
79
80def run_step(~Element: Data,~inside: Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Stride> -> Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Stride>,~last: Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor> -> Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor>,
81 ~inside_keeps: Keeps(~Element,~Cursor.Stride,~inside),
82 ~last_keeps: Keeps(~Element,~Cursor.Cursor,~last),
83 +depth: Nat,-input: Array<Element>,-state: Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor>,
84 +input_evidence: Witness.ArrayWitness<Element,input>,evidence: TraversalWitness.StateEvidence<Array<Element>,Element,Cursor.Cursor,input,depth,state>) ->
85 TraversalWitness.StateEvidence<Array<Element>,Element,Cursor.Cursor,input,depth,Access.run_step(~Element,~inside,~last,state)>:
86 match evidence:
87 case TraversalWitness.StateEvidence{output,position,Cursor.Cursor{Cursor.Level{Cursor.Axis{extent,remaining,stride,rewind},rest},address},equation,output_evidence}:
88 %Equal.sym(Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor>,state,
89 Traversal.State{input,output,position,Cursor.Cursor{Cursor.Level{Cursor.Axis{extent,remaining,stride,rewind},rest},address}},equation) :
90 TraversalWitness.StateEvidence<Array<Element>,Element,Cursor.Cursor,input,depth,Access.run_step(~Element,~inside,~last,_)>
91 run_axis(~Element,~inside,~last,~inside_keeps,~last_keeps,depth,remaining,extent,stride,rewind,rest,address,input,output,position,input_evidence,output_evidence)
92
93def run_loop(~Element: Data,~inside: Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Stride> -> Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Stride>,~last: Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor> -> Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor>,
94 ~inside_keeps: Keeps(~Element,~Cursor.Stride,~inside),
95 ~last_keeps: Keeps(~Element,~Cursor.Cursor,~last),
96 +depth: Nat,count: Nat,-input: Array<Element>,-state: Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor>,
97 +input_evidence: Witness.ArrayWitness<Element,input>,evidence: TraversalWitness.StateEvidence<Array<Element>,Element,Cursor.Cursor,input,depth,state>) ->
98 TraversalWitness.StateEvidence<Array<Element>,Element,Cursor.Cursor,input,depth,Loop.run(~Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor>,~Access.run_step(~Element,~inside,~last),count,state)>:
99 match count:
100 case 0n: evidence
101 case 1n+rest:
102 run_loop(~Element,~inside,~last,~inside_keeps,~last_keeps,depth,rest,input,Access.run_step(~Element,~inside,~last,state),input_evidence,
103 run_step(~Element,~inside,~last,~inside_keeps,~last_keeps,depth,input,state,input_evidence,evidence))
104
105def last_loop(~Element: Data,~last: Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor> -> Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor>,
106 ~last_keeps: Keeps(~Element,~Cursor.Cursor,~last),
107 +depth: Nat,count: Nat,-input: Array<Element>,-state: Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor>,
108 +input_evidence: Witness.ArrayWitness<Element,input>,evidence: TraversalWitness.StateEvidence<Array<Element>,Element,Cursor.Cursor,input,depth,state>) ->
109 TraversalWitness.StateEvidence<Array<Element>,Element,Cursor.Cursor,input,depth,Loop.run(~Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor>,~last,count,state)>:
110 loop(~Element,~Cursor.Cursor,~last,~last_keeps,depth,count,input,state,input_evidence,evidence)
111
112def stepped(~Element: Data,~last: Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor> -> Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor>,
113 ~last_keeps: Keeps(~Element,~Cursor.Cursor,~last),
114 +depth: Nat,count: Nat,cursor: Cursor.Cursor,destination: U32,-input: Array<Element>,-output: Array<Element>,
115 input_evidence: Witness.ArrayWitness<Element,input>,
116 equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
117 TraversalWitness.ResultEvidence<Array<Element>,Element,input,depth,
118 Traversal.finish(~Array<Element>,~Element,~Cursor.Cursor,Loop.run(~Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor>,~last,count,
119 Traversal.State{input,output,destination,cursor}))>:
120 TraversalCertificate.completed(~Array<Element>,~Element,~Cursor.Cursor,~TraversalWitness.array_evidence(~Element),
121 ~Loop.run(~Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor>,~last),~last_loop(~Element,~last,~last_keeps),
122 count,destination,cursor,input,output,input_evidence,depth,equation)
123
124def guarded(~Element: Data,~inside: Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Stride> -> Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Stride>,~last: Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor> -> Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor>,
125 ~inside_keeps: Keeps(~Element,~Cursor.Stride,~inside),
126 ~last_keeps: Keeps(~Element,~Cursor.Cursor,~last),
127 +depth: Nat,full_run: Bool,whole_runs: Bool,runs: Nat,count: Nat,cursor: Cursor.Cursor,destination: U32,
128 -input: Array<Element>,-output: Array<Element>,input_evidence: Witness.ArrayWitness<Element,input>,
129 equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
130 TraversalWitness.ResultEvidence<Array<Element>,Element,input,depth,Access.run_guarded(~Element,~inside,~last,full_run,whole_runs,runs,count,cursor,destination,input,output)>:
131 match full_run whole_runs:
132 case True{} True{}:
133 TraversalCertificate.completed(~Array<Element>,~Element,~Cursor.Cursor,~TraversalWitness.array_evidence(~Element),
134 ~Loop.run(~Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor>,~Access.run_step(~Element,~inside,~last)),~run_loop(~Element,~inside,~last,~inside_keeps,~last_keeps),
135 runs,destination,cursor,input,output,input_evidence,depth,equation)
136 case True{} False{}: stepped(~Element,~last,~last_keeps,depth,count,cursor,destination,input,output,input_evidence,equation)
137 case False{} whole_runs: stepped(~Element,~last,~last_keeps,depth,count,cursor,destination,input,output,input_evidence,equation)
138
139def remaining_run(~Element: Data,~inside: Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Stride> -> Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Stride>,~last: Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor> -> Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor>,
140 ~inside_keeps: Keeps(~Element,~Cursor.Stride,~inside),
141 ~last_keeps: Keeps(~Element,~Cursor.Cursor,~last),
142 +depth: Nat,remaining: Nat,+extent: Nat,stride: U32,rewind: U32,rest: Cursor.Depth1(),address: U32,+count: Nat,destination: U32,
143 -input: Array<Element>,-output: Array<Element>,input_evidence: Witness.ArrayWitness<Element,input>,
144 equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
145 TraversalWitness.ResultEvidence<Array<Element>,Element,input,depth,Access.run_remaining(~Element,~inside,~last,remaining,extent,stride,rewind,rest,address,count,destination,input,output)>:
146 match remaining:
147 case 0n:
148 stepped(~Element,~last,~last_keeps,depth,count,Cursor.Cursor{Cursor.Level{Cursor.Axis{extent,0n,stride,rewind},rest},address},destination,input,output,input_evidence,equation)
149 case 1n+ +inner_count:
150 guarded(~Element,~inside,~last,~inside_keeps,~last_keeps,depth,Nat.is_eq(extent,1n+inner_count),Nat.is_eq(Nat.mul(Nat.div(count,1n+inner_count),1n+inner_count),count),Nat.div(count,1n+inner_count),count,
151 Cursor.Cursor{Cursor.Level{Cursor.Axis{extent,1n+inner_count,stride,rewind},rest},address},destination,input,output,input_evidence,equation)
152
153def strided(~Element: Data,~inside: Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Stride> -> Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Stride>,~last: Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor> -> Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor>,
154 ~inside_keeps: Keeps(~Element,~Cursor.Stride,~inside),
155 ~last_keeps: Keeps(~Element,~Cursor.Cursor,~last),
156 +depth: Nat,count: Nat,cursor: Cursor.Cursor,destination: U32,-input: Array<Element>,-output: Array<Element>,
157 input_evidence: Witness.ArrayWitness<Element,input>,
158 equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
159 TraversalWitness.ResultEvidence<Array<Element>,Element,input,depth,Access.run_strided(~Element,~inside,~last,count,cursor,destination,input,output)>:
160 Cursor.Cursor{Cursor.Level{Cursor.Axis{extent,remaining,stride,rewind},rest},address} = cursor
161 remaining_run(~Element,~inside,~last,~inside_keeps,~last_keeps,depth,remaining,extent,stride,rewind,rest,address,count,destination,input,output,input_evidence,equation)
162
163def copied_strided(~Element: Data,+depth: Nat,count: Nat,cursor: Cursor.Cursor,destination: U32,-input: Array<Element>,-output: Array<Element>,
164 input_evidence: Witness.ArrayWitness<Element,input>,
165 equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
166 TraversalWitness.ResultEvidence<Array<Element>,Element,input,depth,Access.copy_strided(~Element,count,cursor,destination,input,output)>:
167 strided(~Element,~Traversal.visit_step(~Array<Element>,~Element,~Cursor.Stride,~Cursor.read_stride(~Element)),
168 ~Traversal.visit_step(~Array<Element>,~Element,~Cursor.Cursor,~Cursor.read(~Element)),
169 ~VisitWitness.step(~Array<Element>,~Element,~Cursor.Stride,~TraversalWitness.array_evidence(~Element),~Cursor.read_stride(~Element),~CursorWitness.read_stride(~Element)),
170 ~VisitWitness.step(~Array<Element>,~Element,~Cursor.Cursor,~TraversalWitness.array_evidence(~Element),~Cursor.read(~Element),~CursorWitness.read(~Element)),
171 depth,count,cursor,destination,input,output,input_evidence,equation)
172
173def updated_strided(~Element: Data,~operation: Element -> Element -> Element,+depth: Nat,count: Nat,cursor: Cursor.Cursor,destination: U32,
174 -input: Array<Element>,-output: Array<Element>,input_evidence: Witness.ArrayWitness<Element,input>,
175 equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
176 TraversalWitness.ResultEvidence<Array<Element>,Element,input,depth,Access.update_strided(~Element,~operation,count,cursor,destination,input,output)>:
177 strided(~Element,~Traversal.visit_update_step(~Array<Element>,~Element,~Cursor.Stride,~Cursor.read_stride(~Element),~operation),
178 ~Traversal.visit_update_step(~Array<Element>,~Element,~Cursor.Cursor,~Cursor.read(~Element),~operation),
179 ~VisitWitness.update_step(~Array<Element>,~Element,~Cursor.Stride,~TraversalWitness.array_evidence(~Element),~Cursor.read_stride(~Element),~operation,~CursorWitness.read_stride(~Element)),
180 ~VisitWitness.update_step(~Array<Element>,~Element,~Cursor.Cursor,~TraversalWitness.array_evidence(~Element),~Cursor.read(~Element),~operation,~CursorWitness.read(~Element)),
181 depth,count,cursor,destination,input,output,input_evidence,equation)
182
183type ScatterCall is Data:
184 ScatterCall{count: Nat,target: Views.View,source: U32}
185
186def scatter_operation(~Element: Data,call: ScatterCall,input: Array<Element>,output: Array<Element>) -> Array<Element> & Array<Element>:
187 ScatterCall{count,target,source} = call
188 Access.scatter_run(~Element,count,target,source,input,output)
189
190def scattered(~Element: Data,+depth: Nat,call: ScatterCall,-input: Array<Element>,-output: Array<Element>,input_certificate: Certificate.Certificate<Element,input>,
191 equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
192 TraversalWitness.ResultEvidence<Array<Element>,Element,input,depth,scatter_operation(~Element,call,input,output)>:
193 match call:
194 case ScatterCall{count,target,source}:
195 strided(~Element,~Traversal.spread_step(~Element,~Cursor.Stride,~Cursor.target_stride),~Traversal.spread_step(~Element,~Cursor.Cursor,~Cursor.target),
196 ~VisitWitness.spread_step(~Element,~Cursor.Stride,~Cursor.target_stride),~VisitWitness.spread_step(~Element,~Cursor.Cursor,~Cursor.target),
197 depth,count,Cursor.prepare(target),source,input,output,Certificate.witness(Element,input,input_certificate),equation)
198
199def copied(~Element: Data,+depth: Nat,call: CopyCall,-input: Array<Element>,-output: Array<Element>,input_certificate: Certificate.Certificate<Element,input>,
200 equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
201 TraversalWitness.ResultEvidence<Array<Element>,Element,input,depth,copy_operation(~Element,call,input,output)>:
202 match call:
203 case CopyCall{True{},count,Views.View{axes,offset},destination}:
204 TraversalCertificate.completed(~Array<Element>,~Element,~Traversal.Offsets,~TraversalWitness.array_evidence(~Element),
205 ~Traversal.run(~Array<Element>,~Element,~Traversal.Offsets,~Traversal.source_offset(~Element),~Traversal.destination_offset),
206 ~TraversalWitness.run(~Array<Element>,~Element,~Traversal.Offsets,~TraversalWitness.array_evidence(~Element),~Traversal.source_offset(~Element),~Traversal.destination_offset,~TraversalWitness.offset_read(~Element)),
207 count,0,Traversal.Offsets{offset,destination},input,output,Certificate.witness(Element,input,input_certificate),depth,equation)
208 case CopyCall{False{},count,source,destination}:
209 copied_strided(~Element,depth,count,Cursor.prepare(source),destination,input,output,Certificate.witness(Element,input,input_certificate),equation)
210
211def combined(~Element: Data,~operation: Element -> Element -> Element,+depth: Nat,call: CopyCall,-input: Array<Element>,-output: Array<Element>,
212 input_certificate: Certificate.Certificate<Element,input>,
213 equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
214 TraversalWitness.ResultEvidence<Array<Element>,Element,input,depth,combine_operation(~Element,~operation,call,input,output)>:
215 match call:
216 case CopyCall{True{},count,source,destination}:
217 TraversalCertificate.completed(~Array<Element>,~Element,~Unit,~TraversalWitness.array_evidence(~Element),
218 ~Traversal.update(~Array<Element>,~Element,~Element,~Unit,~Traversal.read_index(~Element),~operation,~Traversal.index),
219 ~TraversalWitness.update(~Array<Element>,~Element,~Element,~Unit,~TraversalWitness.array_evidence(~Element),~Traversal.read_index(~Element),~operation,~Traversal.index,~read_index(~Element)),
220 count,0,Unit{},input,output,Certificate.witness(Element,input,input_certificate),depth,equation)
221 case CopyCall{False{},count,source,destination}:
222 updated_strided(~Element,~operation,depth,count,Cursor.prepare(source),destination,input,output,Certificate.witness(Element,input,input_certificate),equation)
223
224def copy(~Element: Data,fast: Bool,count: Nat,source: Views.View,destination: U32,-input: Array<Element>,-output: Array<Element>,
225 input_certificate: Certificate.Certificate<Element,input>,output_certificate: Certificate.Certificate<Element,output>) ->
226 TraversalCertificate.Certificates<Array<Element>,Element,Certificate.family(~Element),Access.copy_run(~Element,fast,count,source,destination,input,output)>:
227 Certificate.Certificate{+depth,+equation} = input_certificate
228 TraversalCertificate.operation(~Array<Element>,~Element,~CopyCall,~Certificate.family(~Element),~copy_operation(~Element),~copied(~Element),
229 CopyCall{fast,count,source,destination},input,output,Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation},output_certificate)
230
231def scatter(~Element: Data,count: Nat,target: Views.View,source: U32,-input: Array<Element>,-output: Array<Element>,
232 input_certificate: Certificate.Certificate<Element,input>,output_certificate: Certificate.Certificate<Element,output>) ->
233 TraversalCertificate.Certificates<Array<Element>,Element,Certificate.family(~Element),Access.scatter_run(~Element,count,target,source,input,output)>:
234 Certificate.Certificate{+depth,+equation} = input_certificate
235 TraversalCertificate.operation(~Array<Element>,~Element,~ScatterCall,~Certificate.family(~Element),~scatter_operation(~Element),~scattered(~Element),
236 ScatterCall{count,target,source},input,output,Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation},output_certificate)
237
238def combine(~Element: Data,~operation: Element -> Element -> Element,fast: Bool,count: Nat,source: Views.View,destination: U32,
239 -input: Array<Element>,-output: Array<Element>,input_certificate: Certificate.Certificate<Element,input>,output_certificate: Certificate.Certificate<Element,output>) ->
240 TraversalCertificate.Certificates<Array<Element>,Element,Certificate.family(~Element),Access.combine_run(~Element,~operation,fast,count,source,destination,input,output)>:
241 Certificate.Certificate{+depth,+equation} = input_certificate
242 TraversalCertificate.operation(~Array<Element>,~Element,~CopyCall,~Certificate.family(~Element),~combine_operation(~Element,~operation),~combined(~Element,~operation),
243 CopyCall{fast,count,source,destination},input,output,Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation},output_certificate)
244
245# The reduction of the lines of a view: every run reads the input and
246# returns it, so the visit returns its input and writes only its output.
247def ran(~Element: Data,~Accumulator: Data,+axes: Cursor.Levels(),+address: U32,+extent: U32,+stride: U32,+position: U32,
248 -input: Array<Element>,-state: Traversal.State<&1,&2,Array<Element>,Accumulator,Traversal.Strided>,
249 evidence: TraversalWitness.FoldEvidence<Array<Element>,Accumulator,Traversal.Strided,input,state>) ->
250 TraversalWitness.FoldEvidence<Array<Element>,Accumulator,Access.Runs,input,
251 Access.ran(~Element,~Accumulator,axes,address,extent,stride,position,Traversal.finish_fold(~Array<Element>,~Accumulator,~Traversal.Strided,state))>:
252 match evidence:
253 case TraversalWitness.FoldEvidence{accumulator,inner,context,equation}:
254 %Equal.sym(Traversal.State<&1,&2,Array<Element>,Accumulator,Traversal.Strided>,state,Traversal.State{input,accumulator,inner,context},equation) :
255 TraversalWitness.FoldEvidence<Array<Element>,Accumulator,Access.Runs,input,
256 Access.ran(~Element,~Accumulator,axes,address,extent,stride,position,Traversal.finish_fold(~Array<Element>,~Accumulator,~Traversal.Strided,_))>
257 TraversalWitness.FoldEvidence{accumulator,(position + 1 : U32),Access.Runs{Cursor.advance(axes,address),extent,stride},{==}}
258
259def fold_run(~Element: Data,~Accumulator: Data,~operation: Accumulator -> Element -> Accumulator,
260 -input: Array<Element>,-state: Traversal.State<&1,&2,Array<Element>,Accumulator,Access.Runs>,+witness: Witness.ArrayWitness<Element,input>,
261 evidence: TraversalWitness.FoldEvidence<Array<Element>,Accumulator,Access.Runs,input,state>) ->
262 TraversalWitness.FoldEvidence<Array<Element>,Accumulator,Access.Runs,input,Access.fold_run(~Element,~Accumulator,~operation,state)>:
263 match evidence:
264 case TraversalWitness.FoldEvidence{+accumulator,+position,Access.Runs{Cursor.Cursor{+axes,+address},+extent,+stride},equation}:
265 %Equal.sym(Traversal.State<&1,&2,Array<Element>,Accumulator,Access.Runs>,state,
266 Traversal.State{input,accumulator,position,Access.Runs{Cursor.Cursor{axes,address},extent,stride}},equation) :
267 TraversalWitness.FoldEvidence<Array<Element>,Accumulator,Access.Runs,input,Access.fold_run(~Element,~Accumulator,~operation,_)>
268 ran(~Element,~Accumulator,axes,address,extent,stride,position,input,
269 Loop.run(~Traversal.State<&1,&2,Array<Element>,Accumulator,Traversal.Strided>,
270 ~Traversal.fold_round(~Array<Element>,~Element,~Accumulator,~Traversal.Strided,~Traversal.strided(~Element),~operation),Nat.div(U32.to_nat(extent),8n),
271 Loop.run(~Traversal.State<&1,&2,Array<Element>,Accumulator,Traversal.Strided>,
272 ~Traversal.fold_step(~Array<Element>,~Element,~Accumulator,~Traversal.Strided,~Traversal.strided(~Element),~operation),Nat.mod(U32.to_nat(extent),8n),
273 Traversal.State{input,accumulator,0,Traversal.Strided{address,stride}})),
274 TraversalWitness.rounds(~Array<Element>,~Element,~Accumulator,~Traversal.Strided,~TraversalWitness.array_evidence(~Element),~Traversal.strided(~Element),~operation,
275 ~TraversalWitness.strided_read(~Element),U32.to_nat(extent),input,0,Traversal.Strided{address,stride},accumulator,witness))
276
277def runs_done(~Element: Data,~Accumulator: Data,~operation: Accumulator -> Element -> Accumulator,count: Nat,
278 -input: Array<Element>,-state: Traversal.State<&1,&2,Array<Element>,Accumulator,Access.Runs>,+witness: Witness.ArrayWitness<Element,input>,
279 evidence: TraversalWitness.FoldEvidence<Array<Element>,Accumulator,Access.Runs,input,state>) ->
280 TraversalWitness.FoldEvidence<Array<Element>,Accumulator,Access.Runs,input,
281 Loop.run(~Traversal.State<&1,&2,Array<Element>,Accumulator,Access.Runs>,~Access.fold_run(~Element,~Accumulator,~operation),count,state)>:
282 match count:
283 case 0n: evidence
284 case 1n+rest:
285 runs_done(~Element,~Accumulator,~operation,rest,input,Access.fold_run(~Element,~Accumulator,~operation,state),witness,
286 fold_run(~Element,~Accumulator,~operation,input,state,witness,evidence))
287
288def folded_line(~Element: Data,~Accumulator: Data,~finish: Accumulator -> Element,+runs: Nat,+initial: Accumulator,
289 -input: Array<Element>,-state: Traversal.State<&1,&2,Array<Element>,Accumulator,Access.Runs>,
290 evidence: TraversalWitness.FoldEvidence<Array<Element>,Accumulator,Access.Runs,input,state>) ->
291 VisitWitness.Sample<Array<Element>,Element,Access.Lines<Accumulator>,input,Access.folded_line(~Element,~Accumulator,~finish,runs,initial,state)>:
292 match evidence:
293 case TraversalWitness.FoldEvidence{accumulator,position,Access.Runs{cursor,extent,stride},equation}:
294 %Equal.sym(Traversal.State<&1,&2,Array<Element>,Accumulator,Access.Runs>,state,Traversal.State{input,accumulator,position,Access.Runs{cursor,extent,stride}},equation) :
295 VisitWitness.Sample<Array<Element>,Element,Access.Lines<Accumulator>,input,Access.folded_line(~Element,~Accumulator,~finish,runs,initial,_)>
296 VisitWitness.Sample{Access.Lines{cursor,runs,extent,stride,initial},finish(accumulator),{==}}
297
298def fold_line(~Element: Data,~Accumulator: Data,~operation: Accumulator -> Element -> Accumulator,~finish: Accumulator -> Element,
299 -input: Array<Element>,context: Access.Lines<Accumulator>,evidence: Witness.ArrayWitness<Element,input>) ->
300 VisitWitness.Sample<Array<Element>,Element,Access.Lines<Accumulator>,input,Access.fold_line(~Element,~Accumulator,~operation,~finish,input,context)>:
301 Access.Lines{+cursor,+runs,+extent,+stride,+initial} = context
302 folded_line(~Element,~Accumulator,~finish,runs,initial,input,
303 Loop.run(~Traversal.State<&1,&2,Array<Element>,Accumulator,Access.Runs>,~Access.fold_run(~Element,~Accumulator,~operation),runs,
304 Traversal.State{input,initial,0,Access.Runs{cursor,extent,stride}}),
305 runs_done(~Element,~Accumulator,~operation,runs,input,Traversal.State{input,initial,0,Access.Runs{cursor,extent,stride}},evidence,
306 TraversalWitness.FoldEvidence{initial,0,Access.Runs{cursor,extent,stride},{==}}))
307
308type LinesCall<-Accumulator: Data> is Data:
309 LinesCall{count: Nat,view: Views.View,runs: Nat,extent: U32,stride: U32,initial: Accumulator}
310
311def lines_operation(~Element: Data,~Accumulator: Data,~operation: Accumulator -> Element -> Accumulator,~finish: Accumulator -> Element,
312 call: LinesCall<Accumulator>,input: Array<Element>,output: Array<Element>) -> Array<Element> & Array<Element>:
313 LinesCall{count,view,runs,extent,stride,initial} = call
314 Access.reduce_lines(~Element,~Accumulator,~operation,~finish,count,view,runs,extent,stride,initial,input,output)
315
316def lined(~Element: Data,~Accumulator: Data,~operation: Accumulator -> Element -> Accumulator,~finish: Accumulator -> Element,
317 +depth: Nat,call: LinesCall<Accumulator>,-input: Array<Element>,-output: Array<Element>,input_certificate: Certificate.Certificate<Element,input>,
318 equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
319 TraversalWitness.ResultEvidence<Array<Element>,Element,input,depth,lines_operation(~Element,~Accumulator,~operation,~finish,call,input,output)>:
320 match call:
321 case LinesCall{count,view,runs,extent,stride,initial}:
322 TraversalCertificate.completed(~Array<Element>,~Element,~Access.Lines<Accumulator>,~TraversalWitness.array_evidence(~Element),
323 ~Traversal.visit(~Array<Element>,~Element,~Access.Lines<Accumulator>,~Access.fold_line(~Element,~Accumulator,~operation,~finish)),
324 ~VisitWitness.visit(~Array<Element>,~Element,~Access.Lines<Accumulator>,~TraversalWitness.array_evidence(~Element),
325 ~Access.fold_line(~Element,~Accumulator,~operation,~finish),~fold_line(~Element,~Accumulator,~operation,~finish)),
326 count,0,Access.Lines{Cursor.prepare(view),runs,extent,stride,initial},input,output,Certificate.witness(Element,input,input_certificate),depth,equation)
327
328def lines(~Element: Data,~Accumulator: Data,~operation: Accumulator -> Element -> Accumulator,~finish: Accumulator -> Element,
329 count: Nat,view: Views.View,runs: Nat,extent: U32,stride: U32,initial: Accumulator,-input: Array<Element>,-output: Array<Element>,
330 input_certificate: Certificate.Certificate<Element,input>,output_certificate: Certificate.Certificate<Element,output>) ->
331 TraversalCertificate.Certificates<Array<Element>,Element,Certificate.family(~Element),
332 Access.reduce_lines(~Element,~Accumulator,~operation,~finish,count,view,runs,extent,stride,initial,input,output)>:
333 Certificate.Certificate{+depth,+equation} = input_certificate
334 TraversalCertificate.operation(~Array<Element>,~Element,~LinesCall<Accumulator>,~Certificate.family(~Element),
335 ~lines_operation(~Element,~Accumulator,~operation,~finish),~lined(~Element,~Accumulator,~operation,~finish),
336 LinesCall{count,view,runs,extent,stride,initial},input,output,Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation},output_certificate)
337
338def window_read_sample(~Element: Data,+pad: Element,valid: Bool,-input: Array<Element>,+index: U32,
339 evidence: Witness.ArrayWitness<Element,input>) ->
340 TraversalWitness.Sample<Array<Element>,Element,input,Access.window_read(~Element,pad,valid,input,index)>:
341 match valid:
342 case False{}: TraversalWitness.Sample{pad,{==}}
343 case True{}: TraversalWitness.array_sample(~Element,input,Array.get(Element,input,index),Witness.observed(Element,input,index,evidence))
344
345# The one-axis window reduction: every sample is an element of the input or
346# the pad, so the sweep returns its input and writes only its output.
347def read_line_sample(~Element: Data,-input: Array<Element>,line: Access.Line<Element>,position: U32,
348 evidence: Witness.ArrayWitness<Element,input>) ->
349 TraversalWitness.Sample<Array<Element>,Element,input,Access.read_line(~Element,input,line,position)>:
350 Access.Line{+base,+first,+extent,+step,+padding,+pad} = line
351 +coordinate = (first + position - padding : U32)
352 window_read_sample(~Element,pad,U32.is_lt(coordinate,extent),input,(base + coordinate * step : U32),evidence)
353
354def line_sample(~Element: Data,-input: Array<Element>,
355 -state: Traversal.State<&1,&2,Array<Element>,Element,Access.Line<Element>>,
356 evidence: TraversalWitness.FoldEvidence<Array<Element>,Element,Access.Line<Element>,input,state>) ->
357 TraversalWitness.Sample<Array<Element>,Element,input,Traversal.finish_fold(~Array<Element>,~Element,~Access.Line<Element>,state)>:
358 match evidence:
359 case TraversalWitness.FoldEvidence{accumulator,position,context,equation}:
360 %Equal.sym(Traversal.State<&1,&2,Array<Element>,Element,Access.Line<Element>>,state,Traversal.State{input,accumulator,position,context},equation) :
361 TraversalWitness.Sample<Array<Element>,Element,input,Traversal.finish_fold(~Array<Element>,~Element,~Access.Line<Element>,_)>
362 TraversalWitness.Sample{accumulator,{==}}
363
364def swept_sample(~Element: Data,~operation: Element -> Element -> Element,-input: Array<Element>,context: Access.SweepContext<Element>,position: U32,
365 evidence: Witness.ArrayWitness<Element,input>) ->
366 TraversalWitness.Sample<Array<Element>,Element,input,Access.read_swept(~Element,~operation,input,context,position)>:
367 Access.SweepContext{+sweep,+pad} = context
368 Access.Sweep{extent,step,+kernel,stride,padding,out_extent,origin} = sweep
369 +position = position
370 line_sample(~Element,input,
371 Loop.run(~Traversal.State<&1,&2,Array<Element>,Element,Access.Line<Element>>,
372 ~Traversal.fold_step(~Array<Element>,~Element,~Element,~Access.Line<Element>,~Access.read_line(~Element),~operation),
373 U32.to_nat(kernel),Traversal.State{input,pad,0,Access.line_at(~Element,sweep,pad,position)}),
374 TraversalWitness.fold_run(~Array<Element>,~Element,~Element,~Access.Line<Element>,~TraversalWitness.array_evidence(~Element),~Access.read_line(~Element),~operation,
375 ~read_line_sample(~Element),U32.to_nat(kernel),input,Traversal.State{input,pad,0,Access.line_at(~Element,sweep,pad,position)},evidence,
376 TraversalWitness.FoldEvidence{pad,0,Access.line_at(~Element,sweep,pad,position),{==}}))
377
378type SweepCall<-Element: Data> is Data:
379 SweepCall{count: Nat,context: Access.SweepContext<Element>}
380
381def sweep_operation(~Element: Data,~operation: Element -> Element -> Element,call: SweepCall<Element>,input: Array<Element>,output: Array<Element>) ->
382 Array<Element> & Array<Element>:
383 SweepCall{count,context} = call
384 Access.sweep_run(~Element,~operation,count,context,input,output)
385
386def swept(~Element: Data,~operation: Element -> Element -> Element,+depth: Nat,call: SweepCall<Element>,-input: Array<Element>,-output: Array<Element>,
387 input_certificate: Certificate.Certificate<Element,input>,
388 equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
389 TraversalWitness.ResultEvidence<Array<Element>,Element,input,depth,sweep_operation(~Element,~operation,call,input,output)>:
390 match call:
391 case SweepCall{count,context}:
392 TraversalCertificate.completed(~Array<Element>,~Element,~Access.SweepContext<Element>,~TraversalWitness.array_evidence(~Element),
393 ~Traversal.run(~Array<Element>,~Element,~Access.SweepContext<Element>,~Access.read_swept(~Element,~operation),~Access.swept_index(~Element)),
394 ~TraversalWitness.run(~Array<Element>,~Element,~Access.SweepContext<Element>,~TraversalWitness.array_evidence(~Element),~Access.read_swept(~Element,~operation),
395 ~Access.swept_index(~Element),~swept_sample(~Element,~operation)),
396 count,0,context,input,output,Certificate.witness(Element,input,input_certificate),depth,equation)
397
398def sweep(~Element: Data,~operation: Element -> Element -> Element,count: Nat,context: Access.SweepContext<Element>,-input: Array<Element>,-output: Array<Element>,
399 input_certificate: Certificate.Certificate<Element,input>,output_certificate: Certificate.Certificate<Element,output>) ->
400 TraversalCertificate.Certificates<Array<Element>,Element,Certificate.family(~Element),Access.sweep_run(~Element,~operation,count,context,input,output)>:
401 Certificate.Certificate{+depth,+equation} = input_certificate
402 TraversalCertificate.operation(~Array<Element>,~Element,~SweepCall<Element>,~Certificate.family(~Element),~sweep_operation(~Element,~operation),~swept(~Element,~operation),
403 SweepCall{count,context},input,output,Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation},output_certificate)