1	# Discharge the reader premises for the actual tensor traversal kernels.
2	# Public operations use only the flat certificates returned at their boundary.
3	import Base
4	import ../tensor_access.bend as Access
5	import ../tensor_view.bend as Views
6	import ../traversal_array.bend as Traversal
7	import ../traversal_loop.bend as Loop
8	import ../tensor_cursor.bend as Cursor
9	import ./tensor_cursor_witness.bend as CursorWitness
10	import ./traversal_visit_witness.bend as VisitWitness
11	import ./storage_certificate.bend as Certificate
12	import ./storage_tree_model.bend as Tree
13	import ./storage_witness.bend as Witness
14	import ./traversal_witness.bend as TraversalWitness
15	import ./traversal_certificate.bend as TraversalCertificate
16	
17	def 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	
21	type CopyCall is Data:
22	  CopyCall{fast: Bool,count: Nat,source: Views.View,destination: U32}
23	
24	def 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	
28	def 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.
36	def 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.
47	def 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	
51	def 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	
61	def 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	
80	def 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	
93	def 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	
105	def 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	
112	def 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	
124	def 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	
139	def 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	
153	def 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	
163	def 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	
173	def 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	
183	type ScatterCall is Data:
184	  ScatterCall{count: Nat,target: Views.View,source: U32}
185	
186	def 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	
190	def 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	
199	def 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	
211	def 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	
224	def 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	
231	def 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	
238	def 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.
247	def 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	
259	def 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	
277	def 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	
288	def 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	
298	def 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	
308	type LinesCall<-Accumulator: Data> is Data:
309	  LinesCall{count: Nat,view: Views.View,runs: Nat,extent: U32,stride: U32,initial: Accumulator}
310	
311	def 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	
316	def 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	
328	def 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	
338	def 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.
347	def 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	
354	def 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	
364	def 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	
378	type SweepCall<-Element: Data> is Data:
379	  SweepCall{count: Nat,context: Access.SweepContext<Element>}
380	
381	def 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	
386	def 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	
398	def 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)