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	type ReduceCall is Data:
246	  ReduceCall{fast: Bool,count: Nat,view: Views.View}
247	
248	def reduce_operation(~Element: Data,~Accumulator: Data,~operation: Accumulator -> Element -> Accumulator,
249	  call: ReduceCall,storage: Array<Element>,initial: Accumulator) -> Array<Element> & Accumulator:
250	  ReduceCall{fast,count,view} = call
251	  Access.reduce_run(~Element,~Accumulator,~operation,fast,count,view,storage,initial)
252	
253	def reduced(~Element: Data,~Accumulator: Data,~operation: Accumulator -> Element -> Accumulator,
254	  call: ReduceCall,-storage: Array<Element>,-initial: Accumulator,certificate: Certificate.Certificate<Element,storage>) ->
255	  {TraversalWitness.first(~Array<Element>,~Accumulator,reduce_operation(~Element,~Accumulator,~operation,call,storage,initial)) == storage : Array<Element>}:
256	  match call:
257	    case ReduceCall{True{},count,Views.View{axes,offset}}:
258	      TraversalWitness.fold(~Array<Element>,~Element,~Accumulator,~Traversal.Offsets,~TraversalWitness.array_evidence(~Element),~Traversal.source_offset(~Element),~operation,~TraversalWitness.offset_read(~Element),
259	        count,storage,0,Traversal.Offsets{offset,0},initial,Certificate.witness(Element,storage,certificate))
260	    case ReduceCall{False{},count,view}:
261	      TraversalWitness.fold_finished(~Array<Element>,~Accumulator,~Cursor.Cursor,storage,
262	        Traversal.visit_fold(~Array<Element>,~Element,~Accumulator,~Cursor.Cursor,~Cursor.read(~Element),~operation,count,Traversal.State{storage,initial,0,Cursor.prepare(view)}),
263	        VisitWitness.fold_run(~Array<Element>,~Element,~Accumulator,~Cursor.Cursor,~TraversalWitness.array_evidence(~Element),~Cursor.read(~Element),~operation,~CursorWitness.read(~Element),
264	          count,storage,Traversal.State{storage,initial,0,Cursor.prepare(view)},Certificate.witness(Element,storage,certificate),
265	          TraversalWitness.FoldEvidence{initial,0,Cursor.prepare(view),{==}}))
266	
267	def reduce(~Element: Data,~Accumulator: Data,~operation: Accumulator -> Element -> Accumulator,fast: Bool,count: Nat,view: Views.View,
268	  -storage: Array<Element>,-initial: Accumulator,certificate: Certificate.Certificate<Element,storage>) ->
269	  Certificate.Certificate<Element,TraversalWitness.first(~Array<Element>,~Accumulator,Access.reduce_run(~Element,~Accumulator,~operation,fast,count,view,storage,initial))>:
270	  Certificate.Certificate{+depth,+equation} = certificate
271	  TraversalCertificate.fold_operation(~Array<Element>,~Accumulator,~ReduceCall,~Certificate.family(~Element),~reduce_operation(~Element,~Accumulator,~operation),~reduced(~Element,~Accumulator,~operation),
272	    ReduceCall{fast,count,view},storage,initial,Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation})
273	
274	type IndexedCall is Data:
275	  IndexedCall{count: Nat,view: Views.View}
276	
277	def indexed_operation(~Element: Data,~operation: U32 -> Element -> Element,call: IndexedCall,input: Array<Element>,output: Array<Element>) ->
278	  Array<Element> & Array<Element>:
279	  IndexedCall{count,view} = call
280	  Access.apply_indexed_run(~Element,~operation,count,view,input,output)
281	
282	def indexed_sample(~Element: Data,~operation: U32 -> Element -> Element,-storage: Array<Element>,+position: U32,-result: Array<Element> & Element,
283	  sample: TraversalWitness.Sample<Array<Element>,Element,storage,result>) ->
284	  TraversalWitness.Sample<Array<Element>,Element,storage,Access.indexed_value(~Element,~operation,position,result)>:
285	  match sample:
286	    case TraversalWitness.Sample{value,equation}:
287	      %Equal.sym(Array<Element> & Element,result,(storage,value),equation) :
288	        TraversalWitness.Sample<Array<Element>,Element,storage,Access.indexed_value(~Element,~operation,position,_)>
289	      TraversalWitness.Sample{operation(position,value),{==}}
290	
291	def indexed_read(~Element: Data,~operation: U32 -> Element -> Element,-storage: Array<Element>,context: Traversal.Offsets,index: U32,
292	  evidence: Witness.ArrayWitness<Element,storage>) ->
293	  TraversalWitness.Sample<Array<Element>,Element,storage,Access.read_indexed(~Element,~operation,storage,context,index)>:
294	  +index = index
295	  indexed_sample(~Element,~operation,storage,index,Traversal.source_offset(~Element,storage,context,index),
296	    TraversalWitness.offset_read(~Element,storage,context,index,evidence))
297	
298	def indexed(~Element: Data,~operation: U32 -> Element -> Element,+depth: Nat,call: IndexedCall,-input: Array<Element>,-output: Array<Element>,
299	  input_certificate: Certificate.Certificate<Element,input>,
300	  equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
301	  TraversalWitness.ResultEvidence<Array<Element>,Element,input,depth,indexed_operation(~Element,~operation,call,input,output)>:
302	  match call:
303	    case IndexedCall{count,Views.View{axes,offset}}:
304	      TraversalCertificate.completed(~Array<Element>,~Element,~Traversal.Offsets,~TraversalWitness.array_evidence(~Element),
305	        ~Traversal.run(~Array<Element>,~Element,~Traversal.Offsets,~Access.read_indexed(~Element,~operation),~Traversal.destination_offset),
306	        ~TraversalWitness.run(~Array<Element>,~Element,~Traversal.Offsets,~TraversalWitness.array_evidence(~Element),~Access.read_indexed(~Element,~operation),~Traversal.destination_offset,~indexed_read(~Element,~operation)),
307	        count,0,Traversal.Offsets{offset,0},input,output,Certificate.witness(Element,input,input_certificate),depth,equation)
308	
309	def apply_indexed(~Element: Data,~operation: U32 -> Element -> Element,count: Nat,view: Views.View,-input: Array<Element>,-output: Array<Element>,
310	  input_certificate: Certificate.Certificate<Element,input>,output_certificate: Certificate.Certificate<Element,output>) ->
311	  TraversalCertificate.Certificates<Array<Element>,Element,Certificate.family(~Element),Access.apply_indexed_run(~Element,~operation,count,view,input,output)>:
312	  Certificate.Certificate{+depth,+equation} = input_certificate
313	  TraversalCertificate.operation(~Array<Element>,~Element,~IndexedCall,~Certificate.family(~Element),~indexed_operation(~Element,~operation),~indexed(~Element,~operation),
314	    IndexedCall{count,view},input,output,Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation},output_certificate)
315	
316	def window_read_sample(~Element: Data,+pad: Element,valid: Bool,-input: Array<Element>,+index: U32,
317	  evidence: Witness.ArrayWitness<Element,input>) ->
318	  TraversalWitness.Sample<Array<Element>,Element,input,Access.window_read(~Element,pad,valid,input,index)>:
319	  match valid:
320	    case False{}: TraversalWitness.Sample{pad,{==}}
321	    case True{}: TraversalWitness.array_sample(~Element,input,Array.get(Element,input,index),Witness.observed(Element,input,index,evidence))
322	
323	# The one-axis window reduction: every sample is an element of the input or
324	# the pad, so the sweep returns its input and writes only its output.
325	def read_line_sample(~Element: Data,-input: Array<Element>,line: Access.Line<Element>,position: U32,
326	  evidence: Witness.ArrayWitness<Element,input>) ->
327	  TraversalWitness.Sample<Array<Element>,Element,input,Access.read_line(~Element,input,line,position)>:
328	  Access.Line{+base,+first,+extent,+step,+padding,+pad} = line
329	  +coordinate = (first + position - padding : U32)
330	  window_read_sample(~Element,pad,U32.is_lt(coordinate,extent),input,(base + coordinate * step : U32),evidence)
331	
332	def line_sample(~Element: Data,-input: Array<Element>,
333	  -state: Traversal.State<&1,&2,Array<Element>,Element,Access.Line<Element>>,
334	  evidence: TraversalWitness.FoldEvidence<Array<Element>,Element,Access.Line<Element>,input,state>) ->
335	  TraversalWitness.Sample<Array<Element>,Element,input,Traversal.finish_fold(~Array<Element>,~Element,~Access.Line<Element>,state)>:
336	  match evidence:
337	    case TraversalWitness.FoldEvidence{accumulator,position,context,equation}:
338	      %Equal.sym(Traversal.State<&1,&2,Array<Element>,Element,Access.Line<Element>>,state,Traversal.State{input,accumulator,position,context},equation) :
339	        TraversalWitness.Sample<Array<Element>,Element,input,Traversal.finish_fold(~Array<Element>,~Element,~Access.Line<Element>,_)>
340	      TraversalWitness.Sample{accumulator,{==}}
341	
342	def swept_sample(~Element: Data,~operation: Element -> Element -> Element,-input: Array<Element>,context: Access.SweepContext<Element>,position: U32,
343	  evidence: Witness.ArrayWitness<Element,input>) ->
344	  TraversalWitness.Sample<Array<Element>,Element,input,Access.read_swept(~Element,~operation,input,context,position)>:
345	  Access.SweepContext{+sweep,+pad} = context
346	  Access.Sweep{extent,step,+kernel,stride,padding,out_extent,origin} = sweep
347	  +position = position
348	  line_sample(~Element,input,
349	    Loop.run(~Traversal.State<&1,&2,Array<Element>,Element,Access.Line<Element>>,
350	      ~Traversal.fold_step(~Array<Element>,~Element,~Element,~Access.Line<Element>,~Access.read_line(~Element),~operation),
351	      U32.to_nat(kernel),Traversal.State{input,pad,0,Access.line_at(~Element,sweep,pad,position)}),
352	    TraversalWitness.fold_run(~Array<Element>,~Element,~Element,~Access.Line<Element>,~TraversalWitness.array_evidence(~Element),~Access.read_line(~Element),~operation,
353	      ~read_line_sample(~Element),U32.to_nat(kernel),input,Traversal.State{input,pad,0,Access.line_at(~Element,sweep,pad,position)},evidence,
354	      TraversalWitness.FoldEvidence{pad,0,Access.line_at(~Element,sweep,pad,position),{==}}))
355	
356	type SweepCall<-Element: Data> is Data:
357	  SweepCall{count: Nat,context: Access.SweepContext<Element>}
358	
359	def sweep_operation(~Element: Data,~operation: Element -> Element -> Element,call: SweepCall<Element>,input: Array<Element>,output: Array<Element>) ->
360	  Array<Element> & Array<Element>:
361	  SweepCall{count,context} = call
362	  Access.sweep_run(~Element,~operation,count,context,input,output)
363	
364	def swept(~Element: Data,~operation: Element -> Element -> Element,+depth: Nat,call: SweepCall<Element>,-input: Array<Element>,-output: Array<Element>,
365	  input_certificate: Certificate.Certificate<Element,input>,
366	  equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
367	  TraversalWitness.ResultEvidence<Array<Element>,Element,input,depth,sweep_operation(~Element,~operation,call,input,output)>:
368	  match call:
369	    case SweepCall{count,context}:
370	      TraversalCertificate.completed(~Array<Element>,~Element,~Access.SweepContext<Element>,~TraversalWitness.array_evidence(~Element),
371	        ~Traversal.run(~Array<Element>,~Element,~Access.SweepContext<Element>,~Access.read_swept(~Element,~operation),~Access.swept_index(~Element)),
372	        ~TraversalWitness.run(~Array<Element>,~Element,~Access.SweepContext<Element>,~TraversalWitness.array_evidence(~Element),~Access.read_swept(~Element,~operation),
373	          ~Access.swept_index(~Element),~swept_sample(~Element,~operation)),
374	        count,0,context,input,output,Certificate.witness(Element,input,input_certificate),depth,equation)
375	
376	def sweep(~Element: Data,~operation: Element -> Element -> Element,count: Nat,context: Access.SweepContext<Element>,-input: Array<Element>,-output: Array<Element>,
377	  input_certificate: Certificate.Certificate<Element,input>,output_certificate: Certificate.Certificate<Element,output>) ->
378	  TraversalCertificate.Certificates<Array<Element>,Element,Certificate.family(~Element),Access.sweep_run(~Element,~operation,count,context,input,output)>:
379	  Certificate.Certificate{+depth,+equation} = input_certificate
380	  TraversalCertificate.operation(~Array<Element>,~Element,~SweepCall<Element>,~Certificate.family(~Element),~sweep_operation(~Element,~operation),~swept(~Element,~operation),
381	    SweepCall{count,context},input,output,Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation},output_certificate)