1	# The same ownership-parameterized state is used by implementation and model.
2	# One read contract and one generic Array.set refinement cover every traversal.
3	import Base
4	import ../traversal_array.bend as Traversal
5	import ../traversal_loop.bend as Loop
6	import ./storage_tree_model.bend as Tree
7	import ./storage_refinement.bend as StorageLaws
8	import ./loop_projection.bend as Projection
9	import ./natural_addition.bend as Addition
10	import ./nat_to_u32_bounds.bend as Bounds
11	import ./nat_order.bend as Order
12	import ./sequence_membership.bend as Members
13	import ./storage_shape.bend as Shape
14	import ./ordered_ranges.bend as Ranges
15	import ./list_storage_readback.bend as ListRead
16	import ./bounded_u32_arithmetic.bend as Arithmetic
17	
18	def collect_values_context(~ownership: Quant,~Runtime: Kind(ownership),~Model: Data,~Context: Data,~pack: Context -> Model -> Runtime,values: List<&2,Model>,+context: Context) -> List<ownership,Runtime>:
19	  match values:
20	    case Nil{}: []
21	    case head <> tail: pack(context,head) <> collect_values_context(~ownership,~Runtime,~Model,~Context,~pack,tail,context)
22	
23	def collect_values(~ownership: Quant,~Runtime: Kind(ownership),~Model: Data,~pack: Model -> Runtime,values: List<&2,Model>) -> List<ownership,Runtime>:
24	  collect_values_context(~ownership,~Runtime,~Model,~Unit,~{context => pack : Unit -> Model -> Runtime},values,Unit{})
25	
26	def collect_result(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,
27	  ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,result: Source & List<&2,Model>) -> Reader & List<ownership,Runtime>:
28	  (+source,+values) = result
29	  (pack_reader(source),collect_values(~ownership,~Runtime,~Model,~pack_value,values))
30	
31	def collected_result(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,~Context: Data,
32	  ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,result: Source & Traversal.Collected<&2,Context,Model>) -> Reader & Traversal.Collected<ownership,Context,Runtime>:
33	  (source,Traversal.Collected{context,value}) = result
34	  (pack_reader(source),Traversal.Collected{context,pack_value(value)})
35	
36	def collect_prepend_matches(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,
37	  ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,+value: Model,result: Source & List<&2,Model>) ->
38	  {Traversal.collect_prepend(~ownership,~Reader,~Runtime,pack_value(value),collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,result)) ==
39	    collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,Traversal.collect_prepend(~&2,~Source,~Model,value,result)) : Reader & List<ownership,Runtime>}:
40	  (+source,+values) = result
41	  {==}
42	
43	def collect_next_matches(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,~Context: Data,
44	  ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,head: Source & Traversal.Collected<&2,Context,Model>,
45	  -runtime_tail: Reader -> Context -> Reader & List<ownership,Runtime>,model_tail: Source -> Context -> Source & List<&2,Model>,
46	  tail_matches: @+source: Source -> @+context: Context ->
47	    {runtime_tail(pack_reader(source),context) == collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,model_tail(source,context)) : Reader & List<ownership,Runtime>}) ->
48	  {Traversal.collect_next(~ownership,~Reader,~Runtime,~Context,collected_result(~ownership,~Reader,~Source,~Runtime,~Model,~Context,~pack_reader,~pack_value,head),runtime_tail) ==
49	    collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,Traversal.collect_next(~&2,~Source,~Model,~Context,head,model_tail)) : Reader & List<ownership,Runtime>}:
50	  (+source,Traversal.Collected{+context,+value}) = head
51	  %Equal.sym(Reader & List<ownership,Runtime>,runtime_tail(pack_reader(source),context),collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,model_tail(source,context)),tail_matches(source,context)) :
52	    {Traversal.collect_prepend(~ownership,~Reader,~Runtime,pack_value(value),_) == collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,Traversal.collect_prepend(~&2,~Source,~Model,value,model_tail(source,context))) : Reader & List<ownership,Runtime>}
53	  collect_prepend_matches(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,value,model_tail(source,context))
54	
55	def collect_refines_model(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,~Context: Data,
56	  ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,
57	  ~read: Reader -> Context -> Reader & Traversal.Collected<ownership,Context,Runtime>,~model_read: Source -> Context -> Source & Traversal.Collected<&2,Context,Model>,
58	  ~read_matches: @+source: Source -> @+context: Context ->
59	    {read(pack_reader(source),context) == collected_result(~ownership,~Reader,~Source,~Runtime,~Model,~Context,~pack_reader,~pack_value,model_read(source,context)) : Reader & Traversal.Collected<ownership,Context,Runtime>},
60	  count: Nat,+source: Source,+context: Context) ->
61	  {Traversal.collect(~ownership,~Reader,~Runtime,~Context,~read,count,pack_reader(source),context) ==
62	    collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,Traversal.collect(~&2,~Source,~Model,~Context,~model_read,count,source,context)) : Reader & List<ownership,Runtime>}:
63	  match count:
64	    case 0n: {==}
65	    case 1n+ +rest:
66	      %Equal.sym(Reader & Traversal.Collected<ownership,Context,Runtime>,read(pack_reader(source),context),collected_result(~ownership,~Reader,~Source,~Runtime,~Model,~Context,~pack_reader,~pack_value,model_read(source,context)),read_matches(source,context)) :
67	        {Traversal.collect_next(~ownership,~Reader,~Runtime,~Context,_,reader => context => Traversal.collect(~ownership,~Reader,~Runtime,~Context,~read,rest,reader,context)) == collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,Traversal.collect(~&2,~Source,~Model,~Context,~model_read,1n+rest,source,context)) : Reader & List<ownership,Runtime>}
68	      collect_next_matches(~ownership,~Reader,~Source,~Runtime,~Model,~Context,~pack_reader,~pack_value,model_read(source,context),
69	        reader => context => Traversal.collect(~ownership,~Reader,~Runtime,~Context,~read,rest,reader,context),source => context => Traversal.collect(~&2,~Source,~Model,~Context,~model_read,rest,source,context),
70	        source => context => collect_refines_model(~ownership,~Reader,~Source,~Runtime,~Model,~Context,~pack_reader,~pack_value,~read,~model_read,~read_matches,rest,source,context))
71	
72	def collect_identity(~Element: Data,~Context: Data,context: Context,value: Element) -> Element:
73	  value
74	
75	def collect_values_context_identity(~Element: Data,~Context: Data,values: List<&2,Element>,+context: Context) ->
76	  {collect_values_context(~&2,~Element,~Element,~Context,~collect_identity(~Element,~Context),values,context) == values : List<&2,Element>}:
77	  match values:
78	    case Nil{}: {==}
79	    case +head <> +rest:
80	      Equal.cong(List<&2,Element>,List<&2,Element>,values => head <> values,
81	        collect_values_context(~&2,~Element,~Element,~Context,~collect_identity(~Element,~Context),rest,context),rest,collect_values_context_identity(~Element,~Context,rest,context))
82	
83	def collect_values_identity(~Element: Data,values: List<&2,Element>) ->
84	  {collect_values(~&2,~Element,~Element,~(value => value),values) == values : List<&2,Element>}:
85	  collect_values_context_identity(~Element,~Unit,values,Unit{})
86	
87	def collect_result_identity(~Reader: Type,~Source: Data,~Element: Data,~pack_reader: Source -> Reader,result: Source & List<&2,Element>) ->
88	  {collect_result(~&2,~Reader,~Source,~Element,~Element,~pack_reader,~(value => value),result) ==
89	    (pack_reader(Pair.fst(Source,List<&2,Element>,result)),Pair.snd(Source,List<&2,Element>,result)) : Reader & List<&2,Element>}:
90	  (source,+values) = result
91	  Equal.cong(List<&2,Element>,Reader & List<&2,Element>,values => (pack_reader(source),values),collect_values(~&2,~Element,~Element,~(value => value),values),values,collect_values_identity(~Element,values))
92	
93	def collect_prepend_source(~Source: Data,~Element: Data,+value: Element,result: Source & List<&2,Element>) ->
94	  {Pair.fst(Source,List<&2,Element>,Traversal.collect_prepend(~&2,~Source,~Element,value,result)) == Pair.fst(Source,List<&2,Element>,result) : Source}:
95	  (source,values) = result
96	  {==}
97	
98	def collect_next_source(~Source: Data,~Element: Data,~Context: Data,head: Source & Traversal.Collected<&2,Context,Element>,
99	  tail: Source -> Context -> Source & List<&2,Element>,
100	  kept: @+source: Source -> @+context: Context -> {Pair.fst(Source,List<&2,Element>,tail(source,context)) == source : Source}) ->
101	  {Pair.fst(Source,List<&2,Element>,Traversal.collect_next(~&2,~Source,~Element,~Context,head,tail)) == Pair.fst(Source,Traversal.Collected<&2,Context,Element>,head) : Source}:
102	  (+source,+collected) = head
103	  Traversal.Collected{+context,+value} = collected
104	  Equal.trans(Source,Pair.fst(Source,List<&2,Element>,Traversal.collect_prepend(~&2,~Source,~Element,value,tail(source,context))),Pair.fst(Source,List<&2,Element>,tail(source,context)),source,collect_prepend_source(~Source,~Element,value,tail(source,context)),kept(source,context))
105	
106	def collect_preserves_source(~Source: Data,~Element: Data,~Context: Data,
107	  ~read: Source -> Context -> Source & Traversal.Collected<&2,Context,Element>,
108	  ~kept: @+source: Source -> @+context: Context -> {Pair.fst(Source,Traversal.Collected<&2,Context,Element>,read(source,context)) == source : Source},
109	  count: Nat,+source: Source,+context: Context) ->
110	  {Pair.fst(Source,List<&2,Element>,Traversal.collect(~&2,~Source,~Element,~Context,~read,count,source,context)) == source : Source}:
111	  match count:
112	    case 0n: {==}
113	    case 1n+ +rest:
114	      Equal.trans(Source,Pair.fst(Source,List<&2,Element>,Traversal.collect(~&2,~Source,~Element,~Context,~read,1n+rest,source,context)),Pair.fst(Source,Traversal.Collected<&2,Context,Element>,read(source,context)),source,
115	        collect_next_source(~Source,~Element,~Context,read(source,context),source => context => Traversal.collect(~&2,~Source,~Element,~Context,~read,rest,source,context),
116	          source => context => collect_preserves_source(~Source,~Element,~Context,~read,~kept,rest,source,context)),kept(source,context))
117	
118	def collect_list_next_source(~Source: Data,~Element: Data,head: Source & Element,tail: Source -> Source & List<&2,Element>,
119	  kept: @+source: Source -> {Pair.fst(Source,List<&2,Element>,tail(source)) == source : Source}) ->
120	  {Pair.fst(Source,List<&2,Element>,Traversal.collect_list_next(~&2,~Source,~Element,head,tail)) == Pair.fst(Source,Element,head) : Source}:
121	  (+source,+value) = head
122	  Equal.trans(Source,Pair.fst(Source,List<&2,Element>,Traversal.collect_prepend(~&2,~Source,~Element,value,tail(source))),Pair.fst(Source,List<&2,Element>,tail(source)),source,
123	    collect_prepend_source(~Source,~Element,value,tail(source)),kept(source))
124	
125	# A keyed collection whose reads keep the source keeps it.
126	def collect_list_preserves_source(~Source: Data,~Element: Data,~Key: Data,~Context: Data,
127	  ~read: Source -> Context -> Key -> Source & Element,
128	  ~kept: @+source: Source -> @+context: Context -> @+key: Key -> {Pair.fst(Source,Element,read(source,context,key)) == source : Source},
129	  keys: List<&2,Key>,+source: Source,+context: Context) ->
130	  {Pair.fst(Source,List<&2,Element>,Traversal.collect_list(~&2,~Source,~Element,~Key,~Context,~read,keys,source,context)) == source : Source}:
131	  match keys:
132	    case Nil{}: {==}
133	    case Con{+key,+rest}:
134	      Equal.trans(Source,Pair.fst(Source,List<&2,Element>,Traversal.collect_list(~&2,~Source,~Element,~Key,~Context,~read,Con{key,rest},source,context)),
135	        Pair.fst(Source,Element,read(source,context,key)),source,
136	        collect_list_next_source(~Source,~Element,read(source,context,key),source => Traversal.collect_list(~&2,~Source,~Element,~Key,~Context,~read,rest,source,context),
137	          source => collect_list_preserves_source(~Source,~Element,~Key,~Context,~read,~kept,rest,source,context)),kept(source,context,key))
138	
139	def collect_list_read(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,
140	  ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,result: Source & Model) -> Reader & Runtime:
141	  (source,value) = result
142	  (pack_reader(source),pack_value(value))
143	
144	def collect_list_next_matches(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,
145	  ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,head: Source & Model,
146	  -runtime_tail: Reader -> Reader & List<ownership,Runtime>,model_tail: Source -> Source & List<&2,Model>,
147	  tail_matches: @+source: Source ->
148	    {runtime_tail(pack_reader(source)) == collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,model_tail(source)) : Reader & List<ownership,Runtime>}) ->
149	  {Traversal.collect_list_next(~ownership,~Reader,~Runtime,collect_list_read(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,head),runtime_tail) ==
150	    collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,Traversal.collect_list_next(~&2,~Source,~Model,head,model_tail)) : Reader & List<ownership,Runtime>}:
151	  (+source,+value) = head
152	  %Equal.sym(Reader & List<ownership,Runtime>,runtime_tail(pack_reader(source)),collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,model_tail(source)),tail_matches(source)) :
153	    {Traversal.collect_prepend(~ownership,~Reader,~Runtime,pack_value(value),_) == collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,Traversal.collect_prepend(~&2,~Source,~Model,value,model_tail(source))) : Reader & List<ownership,Runtime>}
154	  collect_prepend_matches(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,value,model_tail(source))
155	
156	def collect_list_refines_model(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,~Key: Data,~Context: Data,
157	  ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,
158	  ~read: Reader -> Context -> Key -> Reader & Runtime,~model_read: Source -> Context -> Key -> Source & Model,
159	  ~read_matches: @+source: Source -> @+context: Context -> @+key: Key ->
160	    {read(pack_reader(source),context,key) == collect_list_read(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,model_read(source,context,key)) : Reader & Runtime},
161	  keys: List<&2,Key>,+source: Source,+context: Context) ->
162	  {Traversal.collect_list(~ownership,~Reader,~Runtime,~Key,~Context,~read,keys,pack_reader(source),context) ==
163	    collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,Traversal.collect_list(~&2,~Source,~Model,~Key,~Context,~model_read,keys,source,context)) : Reader & List<ownership,Runtime>}:
164	  match keys:
165	    case Nil{}: {==}
166	    case +key <> +rest:
167	      %Equal.sym(Reader & Runtime,read(pack_reader(source),context,key),collect_list_read(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,model_read(source,context,key)),read_matches(source,context,key)) :
168	        {Traversal.collect_list_next(~ownership,~Reader,~Runtime,_,reader => Traversal.collect_list(~ownership,~Reader,~Runtime,~Key,~Context,~read,rest,reader,context)) == collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,Traversal.collect_list(~&2,~Source,~Model,~Key,~Context,~model_read,keys,source,context)) : Reader & List<ownership,Runtime>}
169	      collect_list_next_matches(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,model_read(source,context,key),
170	        reader => Traversal.collect_list(~ownership,~Reader,~Runtime,~Key,~Context,~read,rest,reader,context),source => Traversal.collect_list(~&2,~Source,~Model,~Key,~Context,~model_read,rest,source,context),
171	        source => collect_list_refines_model(~ownership,~Reader,~Source,~Runtime,~Model,~Key,~Context,~pack_reader,~pack_value,~read,~model_read,~read_matches,rest,source,context))
172	
173	# The loops gather newest first and reverse once; a gathered prefix stands
174	# in front of the recursive collection of the rest.
175	def onto(~Source: Data,~Model: Data,gathered: List<&2,Model>,result: Source & List<&2,Model>) -> Source & List<&2,Model>:
176	  (+source,+values) = result
177	  (source,Traversal.reversed_onto(~&2,~Model,gathered,values))
178	
179	def onto_empty(~Source: Data,~Model: Data,result: Source & List<&2,Model>) -> {onto(~Source,~Model,[],result) == result : Source & List<&2,Model>}:
180	  (+source,+values) = result
181	  {==}
182	
183	def onto_prepend(~Source: Data,~Model: Data,+value: Model,+gathered: List<&2,Model>,result: Source & List<&2,Model>) ->
184	  {onto(~Source,~Model,value <> gathered,result) == onto(~Source,~Model,gathered,Traversal.collect_prepend(~&2,~Source,~Model,value,result)) : Source & List<&2,Model>}:
185	  (+source,+values) = result
186	  {==}
187	
188	def collect_values_reversed(~ownership: Quant,~Runtime: Kind(ownership),~Model: Data,~pack_value: Model -> Runtime,values: List<&2,Model>,+tail: List<&2,Model>) ->
189	  {collect_values(~ownership,~Runtime,~Model,~pack_value,Traversal.reversed_onto(~&2,~Model,values,tail)) ==
190	    Traversal.reversed_onto(~ownership,~Runtime,collect_values(~ownership,~Runtime,~Model,~pack_value,values),collect_values(~ownership,~Runtime,~Model,~pack_value,tail)) : List<ownership,Runtime>}:
191	  match values:
192	    case Nil{}: {==}
193	    case +head <> +rest: collect_values_reversed(~ownership,~Runtime,~Model,~pack_value,rest,head <> tail)
194	
195	def gathering_finished(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,
196	  ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,+source: Source,+gathered: List<&2,Model>) ->
197	  {(pack_reader(source),Traversal.reversed_onto(~ownership,~Runtime,collect_values(~ownership,~Runtime,~Model,~pack_value,gathered),[])) ==
198	    collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,gathered,(source,[]))) : Reader & List<ownership,Runtime>}:
199	  Equal.cong(List<ownership,Runtime>,Reader & List<ownership,Runtime>,values => (pack_reader(source),values),
200	    Traversal.reversed_onto(~ownership,~Runtime,collect_values(~ownership,~Runtime,~Model,~pack_value,gathered),[]),
201	    collect_values(~ownership,~Runtime,~Model,~pack_value,Traversal.reversed_onto(~&2,~Model,gathered,[])),
202	    Equal.sym(List<ownership,Runtime>,collect_values(~ownership,~Runtime,~Model,~pack_value,Traversal.reversed_onto(~&2,~Model,gathered,[])),
203	      Traversal.reversed_onto(~ownership,~Runtime,collect_values(~ownership,~Runtime,~Model,~pack_value,gathered),[]),
204	      collect_values_reversed(~ownership,~Runtime,~Model,~pack_value,gathered,[])))
205	
206	def gathered_matches(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,~Context: Data,
207	  ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,head: Source & Traversal.Collected<&2,Context,Model>,+gathered: List<&2,Model>,
208	  -runtime_rest: Traversal.Gathering<&1,ownership,Reader,Runtime,Context> -> Reader & List<ownership,Runtime>,model_rest: Source -> Context -> Source & List<&2,Model>,
209	  rest_matches: @+source: Source -> @+context: Context -> @+gathered: List<&2,Model> ->
210	    {runtime_rest(Traversal.Gathering{pack_reader(source),context,collect_values(~ownership,~Runtime,~Model,~pack_value,gathered)}) ==
211	      collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,gathered,model_rest(source,context))) : Reader & List<ownership,Runtime>}) ->
212	  {runtime_rest(Traversal.gathered(~ownership,~Reader,~Runtime,~Context,collected_result(~ownership,~Reader,~Source,~Runtime,~Model,~Context,~pack_reader,~pack_value,head),
213	      collect_values(~ownership,~Runtime,~Model,~pack_value,gathered))) ==
214	    collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,gathered,Traversal.collect_next(~&2,~Source,~Model,~Context,head,model_rest))) : Reader & List<ownership,Runtime>}:
215	  (+source,Traversal.Collected{+context,+value}) = head
216	  Equal.trans(Reader & List<ownership,Runtime>,
217	    runtime_rest(Traversal.Gathering{pack_reader(source),context,collect_values(~ownership,~Runtime,~Model,~pack_value,value <> gathered)}),
218	    collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,value <> gathered,model_rest(source,context))),
219	    collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,gathered,Traversal.collect_prepend(~&2,~Source,~Model,value,model_rest(source,context)))),
220	    rest_matches(source,context,value <> gathered),
221	    Equal.cong(Source & List<&2,Model>,Reader & List<ownership,Runtime>,result => collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,result),
222	      onto(~Source,~Model,value <> gathered,model_rest(source,context)),onto(~Source,~Model,gathered,Traversal.collect_prepend(~&2,~Source,~Model,value,model_rest(source,context))),
223	      onto_prepend(~Source,~Model,value,gathered,model_rest(source,context))))
224	
225	def collect_loop_gathers(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,~Context: Data,
226	  ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,
227	  ~read: Reader -> Context -> Reader & Traversal.Collected<ownership,Context,Runtime>,~model_read: Source -> Context -> Source & Traversal.Collected<&2,Context,Model>,
228	  ~read_matches: @+source: Source -> @+context: Context ->
229	    {read(pack_reader(source),context) == collected_result(~ownership,~Reader,~Source,~Runtime,~Model,~Context,~pack_reader,~pack_value,model_read(source,context)) : Reader & Traversal.Collected<ownership,Context,Runtime>},
230	  count: Nat,+source: Source,+context: Context,+gathered: List<&2,Model>) ->
231	  {Traversal.gathering_result(~ownership,~Reader,~Runtime,~Context,
232	      Loop.run(~Traversal.Gathering<&1,ownership,Reader,Runtime,Context>,~Traversal.gather_step(~ownership,~Reader,~Runtime,~Context,~read),count,
233	        Traversal.Gathering{pack_reader(source),context,collect_values(~ownership,~Runtime,~Model,~pack_value,gathered)})) ==
234	    collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,gathered,Traversal.collect(~&2,~Source,~Model,~Context,~model_read,count,source,context))) : Reader & List<ownership,Runtime>}:
235	  match count:
236	    case 0n: gathering_finished(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,source,gathered)
237	    case 1n+ +rest:
238	      %Equal.sym(Reader & Traversal.Collected<ownership,Context,Runtime>,read(pack_reader(source),context),collected_result(~ownership,~Reader,~Source,~Runtime,~Model,~Context,~pack_reader,~pack_value,model_read(source,context)),read_matches(source,context)) :
239	        {Traversal.gathering_result(~ownership,~Reader,~Runtime,~Context,
240	            Loop.run(~Traversal.Gathering<&1,ownership,Reader,Runtime,Context>,~Traversal.gather_step(~ownership,~Reader,~Runtime,~Context,~read),rest,
241	              Traversal.gathered(~ownership,~Reader,~Runtime,~Context,_,collect_values(~ownership,~Runtime,~Model,~pack_value,gathered)))) ==
242	          collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,gathered,Traversal.collect(~&2,~Source,~Model,~Context,~model_read,1n+rest,source,context))) : Reader & List<ownership,Runtime>}
243	      gathered_matches(~ownership,~Reader,~Source,~Runtime,~Model,~Context,~pack_reader,~pack_value,model_read(source,context),gathered,
244	        state => Traversal.gathering_result(~ownership,~Reader,~Runtime,~Context,
245	          Loop.run(~Traversal.Gathering<&1,ownership,Reader,Runtime,Context>,~Traversal.gather_step(~ownership,~Reader,~Runtime,~Context,~read),rest,state)),
246	        source => context => Traversal.collect(~&2,~Source,~Model,~Context,~model_read,rest,source,context),
247	        source => context => gathered => collect_loop_gathers(~ownership,~Reader,~Source,~Runtime,~Model,~Context,~pack_reader,~pack_value,~read,~model_read,~read_matches,rest,source,context,gathered))
248	
249	# The collection loop refines the recursive model collection.
250	def collect_loop_refines_model(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,~Context: Data,
251	  ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,
252	  ~read: Reader -> Context -> Reader & Traversal.Collected<ownership,Context,Runtime>,~model_read: Source -> Context -> Source & Traversal.Collected<&2,Context,Model>,
253	  ~read_matches: @+source: Source -> @+context: Context ->
254	    {read(pack_reader(source),context) == collected_result(~ownership,~Reader,~Source,~Runtime,~Model,~Context,~pack_reader,~pack_value,model_read(source,context)) : Reader & Traversal.Collected<ownership,Context,Runtime>},
255	  +count: Nat,+source: Source,+context: Context) ->
256	  {Traversal.collect_loop(~ownership,~Reader,~Runtime,~Context,~read,count,pack_reader(source),context) ==
257	    collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,Traversal.collect(~&2,~Source,~Model,~Context,~model_read,count,source,context)) : Reader & List<ownership,Runtime>}:
258	  %onto_empty(~Source,~Model,Traversal.collect(~&2,~Source,~Model,~Context,~model_read,count,source,context)) :
259	    {Traversal.collect_loop(~ownership,~Reader,~Runtime,~Context,~read,count,pack_reader(source),context) ==
260	      collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,_) : Reader & List<ownership,Runtime>}
261	  collect_loop_gathers(~ownership,~Reader,~Source,~Runtime,~Model,~Context,~pack_reader,~pack_value,~read,~model_read,~read_matches,count,source,context,[])
262	
263	def gathered_key_matches(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,~Key: Data,~Context: Data,
264	  ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,head: Source & Model,+rest: List<&2,Key>,+context: Context,+gathered: List<&2,Model>,
265	  -runtime_rest: Traversal.Gathering<&1,ownership,Reader,Runtime,Traversal.Keyed<Key,Context>> -> Reader & List<ownership,Runtime>,model_rest: Source -> Source & List<&2,Model>,
266	  rest_matches: @+source: Source -> @+gathered: List<&2,Model> ->
267	    {runtime_rest(Traversal.Gathering{pack_reader(source),Traversal.Keyed{rest,context},collect_values(~ownership,~Runtime,~Model,~pack_value,gathered)}) ==
268	      collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,gathered,model_rest(source))) : Reader & List<ownership,Runtime>}) ->
269	  {runtime_rest(Traversal.gathered_key(~ownership,~Reader,~Runtime,~Key,~Context,collect_list_read(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,head),rest,context,
270	      collect_values(~ownership,~Runtime,~Model,~pack_value,gathered))) ==
271	    collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,gathered,Traversal.collect_list_next(~&2,~Source,~Model,head,model_rest))) : Reader & List<ownership,Runtime>}:
272	  (+source,+value) = head
273	  Equal.trans(Reader & List<ownership,Runtime>,
274	    runtime_rest(Traversal.Gathering{pack_reader(source),Traversal.Keyed{rest,context},collect_values(~ownership,~Runtime,~Model,~pack_value,value <> gathered)}),
275	    collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,value <> gathered,model_rest(source))),
276	    collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,gathered,Traversal.collect_prepend(~&2,~Source,~Model,value,model_rest(source)))),
277	    rest_matches(source,value <> gathered),
278	    Equal.cong(Source & List<&2,Model>,Reader & List<ownership,Runtime>,result => collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,result),
279	      onto(~Source,~Model,value <> gathered,model_rest(source)),onto(~Source,~Model,gathered,Traversal.collect_prepend(~&2,~Source,~Model,value,model_rest(source))),
280	      onto_prepend(~Source,~Model,value,gathered,model_rest(source))))
281	
282	def collect_list_loop_gathers(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,~Key: Data,~Context: Data,
283	  ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,
284	  ~read: Reader -> Context -> Key -> Reader & Runtime,~model_read: Source -> Context -> Key -> Source & Model,
285	  ~read_matches: @+source: Source -> @+context: Context -> @+key: Key ->
286	    {read(pack_reader(source),context,key) == collect_list_read(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,model_read(source,context,key)) : Reader & Runtime},
287	  keys: List<&2,Key>,+source: Source,+context: Context,+gathered: List<&2,Model>) ->
288	  {Traversal.gathering_result(~ownership,~Reader,~Runtime,~Traversal.Keyed<Key,Context>,
289	      Loop.run(~Traversal.Gathering<&1,ownership,Reader,Runtime,Traversal.Keyed<Key,Context>>,~Traversal.gather_key_step(~ownership,~Reader,~Runtime,~Key,~Context,~read),List.length(&2,Key,keys),
290	        Traversal.Gathering{pack_reader(source),Traversal.Keyed{keys,context},collect_values(~ownership,~Runtime,~Model,~pack_value,gathered)})) ==
291	    collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,gathered,Traversal.collect_list(~&2,~Source,~Model,~Key,~Context,~model_read,keys,source,context))) : Reader & List<ownership,Runtime>}:
292	  match keys:
293	    case Nil{}: gathering_finished(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,source,gathered)
294	    case +key <> +rest:
295	      %Equal.sym(Reader & Runtime,read(pack_reader(source),context,key),collect_list_read(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,model_read(source,context,key)),read_matches(source,context,key)) :
296	        {Traversal.gathering_result(~ownership,~Reader,~Runtime,~Traversal.Keyed<Key,Context>,
297	            Loop.run(~Traversal.Gathering<&1,ownership,Reader,Runtime,Traversal.Keyed<Key,Context>>,~Traversal.gather_key_step(~ownership,~Reader,~Runtime,~Key,~Context,~read),List.length(&2,Key,rest),
298	              Traversal.gathered_key(~ownership,~Reader,~Runtime,~Key,~Context,_,rest,context,collect_values(~ownership,~Runtime,~Model,~pack_value,gathered)))) ==
299	          collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,gathered,Traversal.collect_list(~&2,~Source,~Model,~Key,~Context,~model_read,key <> rest,source,context))) : Reader & List<ownership,Runtime>}
300	      gathered_key_matches(~ownership,~Reader,~Source,~Runtime,~Model,~Key,~Context,~pack_reader,~pack_value,model_read(source,context,key),rest,context,gathered,
301	        state => Traversal.gathering_result(~ownership,~Reader,~Runtime,~Traversal.Keyed<Key,Context>,
302	          Loop.run(~Traversal.Gathering<&1,ownership,Reader,Runtime,Traversal.Keyed<Key,Context>>,~Traversal.gather_key_step(~ownership,~Reader,~Runtime,~Key,~Context,~read),List.length(&2,Key,rest),state)),
303	        source => Traversal.collect_list(~&2,~Source,~Model,~Key,~Context,~model_read,rest,source,context),
304	        source => gathered => collect_list_loop_gathers(~ownership,~Reader,~Source,~Runtime,~Model,~Key,~Context,~pack_reader,~pack_value,~read,~model_read,~read_matches,rest,source,context,gathered))
305	
306	# The keyed collection loop refines the recursive model collection.
307	def collect_list_loop_refines_model(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,~Key: Data,~Context: Data,
308	  ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,
309	  ~read: Reader -> Context -> Key -> Reader & Runtime,~model_read: Source -> Context -> Key -> Source & Model,
310	  ~read_matches: @+source: Source -> @+context: Context -> @+key: Key ->
311	    {read(pack_reader(source),context,key) == collect_list_read(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,model_read(source,context,key)) : Reader & Runtime},
312	  +keys: List<&2,Key>,+source: Source,+context: Context) ->
313	  {Traversal.collect_list_loop(~ownership,~Reader,~Runtime,~Key,~Context,~read,keys,pack_reader(source),context) ==
314	    collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,Traversal.collect_list(~&2,~Source,~Model,~Key,~Context,~model_read,keys,source,context)) : Reader & List<ownership,Runtime>}:
315	  %onto_empty(~Source,~Model,Traversal.collect_list(~&2,~Source,~Model,~Key,~Context,~model_read,keys,source,context)) :
316	    {Traversal.collect_list_loop(~ownership,~Reader,~Runtime,~Key,~Context,~read,keys,pack_reader(source),context) ==
317	      collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,_) : Reader & List<ownership,Runtime>}
318	  collect_list_loop_gathers(~ownership,~Reader,~Source,~Runtime,~Model,~Key,~Context,~pack_reader,~pack_value,~read,~model_read,~read_matches,keys,source,context,[])
319	
320	def represent(~Reader: Type,~Model: Data,~Element: Data,~Context: Data,~pack_reader: Model -> Reader,
321	  state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) -> Traversal.State<&1,&1,Reader,Array<Element>,Context>:
322	  Traversal.State{reader,output,position,context} = state
323	  Traversal.State{pack_reader(reader),Tree.pack(Element,output),position,context}
324	
325	def model_step(~Model: Data,~Element: Data,~Context: Data,
326	  ~sample: Model -> Context -> U32 -> Element,~destination: Context -> U32 -> U32,
327	  state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) -> Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>:
328	  Traversal.State{+reader,output,+position,+context} = state
329	  Traversal.State{reader,Tree.write(Element,output,destination(context,position),sample(reader,context,position)),(position + 1 : U32),context}
330	
331	def model_reader(~Model: Data,~Element: Data,~Context: Data,state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) -> Model:
332	  Traversal.State{reader,output,position,context} = state
333	  reader
334	
335	def model_reader_step(~Model: Data,~Element: Data,~Context: Data,~sample: Model -> Context -> U32 -> Element,~destination: Context -> U32 -> U32,
336	  +state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) ->
337	  {model_reader(~Model,~Element,~Context,model_step(~Model,~Element,~Context,~sample,~destination,state)) == model_reader(~Model,~Element,~Context,state) : Model}:
338	  Traversal.State{reader,output,position,context} = state
339	  {==}
340	
341	def model_reader_kept(~Model: Data,~Element: Data,~Context: Data,~sample: Model -> Context -> U32 -> Element,~destination: Context -> U32 -> U32,
342	  +count: Nat,+state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) ->
343	  {model_reader(~Model,~Element,~Context,Loop.run(~Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>,~model_step(~Model,~Element,~Context,~sample,~destination),count,state)) == model_reader(~Model,~Element,~Context,state) : Model}:
344	  Projection.preserves_observation(~Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>,~Model,~model_step(~Model,~Element,~Context,~sample,~destination),~model_reader(~Model,~Element,~Context),~model_reader_step(~Model,~Element,~Context,~sample,~destination),count,state)
345	
346	def step_refines_model(~Reader: Type,~Model: Data,~Element: Data,~Context: Data,
347	  ~pack_reader: Model -> Reader,~read: Reader -> Context -> U32 -> Reader & Element,
348	  ~sample: Model -> Context -> U32 -> Element,~destination: Context -> U32 -> U32,
349	  ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
350	    {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
351	  +state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) ->
352	  {Traversal.step(~Reader,~Element,~Context,~read,~destination,represent(~Reader,~Model,~Element,~Context,~pack_reader,state)) ==
353	    represent(~Reader,~Model,~Element,~Context,~pack_reader,model_step(~Model,~Element,~Context,~sample,~destination,state)) :
354	    Traversal.State<&1,&1,Reader,Array<Element>,Context>}:
355	  Traversal.State{+reader,+output,+position,+context} = state
356	  %Equal.sym(Reader & Element,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),read_matches(reader,context,position)) :
357	    {Traversal.store(~Reader,~Element,~Context,~destination,position,context,Tree.pack(Element,output),_) ==
358	      represent(~Reader,~Model,~Element,~Context,~pack_reader,model_step(~Model,~Element,~Context,~sample,~destination,
359	        Traversal.State{reader,output,position,context})) : Traversal.State<&1,&1,Reader,Array<Element>,Context>}
360	  %Equal.sym(Array<Element>,Array.set(Element,Tree.pack(Element,output),destination(context,position),sample(reader,context,position)),
361	    Tree.pack(Element,Tree.write(Element,output,destination(context,position),sample(reader,context,position))),
362	    StorageLaws.write(Element,output,destination(context,position),sample(reader,context,position))) :
363	    {Traversal.State{pack_reader(reader),_,(position + 1 : U32),context} ==
364	      represent(~Reader,~Model,~Element,~Context,~pack_reader,model_step(~Model,~Element,~Context,~sample,~destination,
365	        Traversal.State{reader,output,position,context})) : Traversal.State<&1,&1,Reader,Array<Element>,Context>}
366	  {==}
367	
368	def traversal_refines_model(~Reader: Type,~Model: Data,~Element: Data,~Context: Data,
369	  ~pack_reader: Model -> Reader,~read: Reader -> Context -> U32 -> Reader & Element,
370	  ~sample: Model -> Context -> U32 -> Element,~destination: Context -> U32 -> U32,
371	  ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
372	    {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
373	  +count: Nat,+state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) ->
374	  {Traversal.run(~Reader,~Element,~Context,~read,~destination,count,represent(~Reader,~Model,~Element,~Context,~pack_reader,state)) ==
375	    represent(~Reader,~Model,~Element,~Context,~pack_reader,
376	      Loop.run(~Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>,~model_step(~Model,~Element,~Context,~sample,~destination),count,state)) :
377	    Traversal.State<&1,&1,Reader,Array<Element>,Context>}:
378	  Projection.iteration_refines_model(~Traversal.State<&1,&1,Reader,Array<Element>,Context>,~Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>,
379	    ~Traversal.step(~Reader,~Element,~Context,~read,~destination),~model_step(~Model,~Element,~Context,~sample,~destination),
380	    ~represent(~Reader,~Model,~Element,~Context,~pack_reader),~step_refines_model(~Reader,~Model,~Element,~Context,~pack_reader,~read,~sample,~destination,~read_matches),count,state)
381	# Concrete copy/zip readers discharge the generic traversal's only read premise.
382	
383	def pack_tree(~Element: Data,tree: Tree.Tree<Element>) -> Array<Element>:
384	  Tree.pack(Element,tree)
385	
386	def sample_offset(~Element: Data,tree: Tree.Tree<Element>,context: Traversal.Offsets,position: U32) -> Element:
387	  Traversal.Offsets{source,destination} = context
388	  Tree.read(Element,tree,(source + position : U32))
389	
390	def offset_read_refines_storage(~Element: Data,+tree: Tree.Tree<Element>,+context: Traversal.Offsets,+position: U32) ->
391	  {Traversal.source_offset(~Element,pack_tree(~Element,tree),context,position) ==
392	    (pack_tree(~Element,tree),sample_offset(~Element,tree,context,position)) : Array<Element> & Element}:
393	  Traversal.Offsets{source,destination} = context
394	  StorageLaws.read(Element,tree,(source + position : U32))
395	
396	def sample_strided(~Element: Data,tree: Tree.Tree<Element>,context: Traversal.Strided,position: U32) -> Element:
397	  Traversal.Strided{base,stride} = context
398	  Tree.read(Element,tree,(base + position * stride : U32))
399	
400	def strided_read_refines_storage(~Element: Data,+tree: Tree.Tree<Element>,+context: Traversal.Strided,+position: U32) ->
401	  {Traversal.strided(~Element,pack_tree(~Element,tree),context,position) ==
402	    (pack_tree(~Element,tree),sample_strided(~Element,tree,context,position)) : Array<Element> & Element}:
403	  Traversal.Strided{base,stride} = context
404	  StorageLaws.read(Element,tree,(base + position * stride : U32))
405	
406	def copy_traversal_refines_storage(~Element: Data,+count: Nat,
407	  +state: Traversal.State<&2,&2,Tree.Tree<Element>,Tree.Tree<Element>,Traversal.Offsets>) ->
408	  {Traversal.run(~Array<Element>,~Element,~Traversal.Offsets,~Traversal.source_offset(~Element),~Traversal.destination_offset,count,
409	      represent(~Array<Element>,~Tree.Tree<Element>,~Element,~Traversal.Offsets,~pack_tree(~Element),state)) ==
410	    represent(~Array<Element>,~Tree.Tree<Element>,~Element,~Traversal.Offsets,~pack_tree(~Element),
411	      Loop.run(~Traversal.State<&2,&2,Tree.Tree<Element>,Tree.Tree<Element>,Traversal.Offsets>,
412	        ~model_step(~Tree.Tree<Element>,~Element,~Traversal.Offsets,~sample_offset(~Element),~Traversal.destination_offset),count,state)) :
413	    Traversal.State<&1,&1,Array<Element>,Array<Element>,Traversal.Offsets>}:
414	  traversal_refines_model(~Array<Element>,~Tree.Tree<Element>,~Element,~Traversal.Offsets,~pack_tree(~Element),
415	    ~Traversal.source_offset(~Element),~sample_offset(~Element),~Traversal.destination_offset,~offset_read_refines_storage(~Element),count,state)
416	
417	# The accumulator is an observation, independent of its numeric interpretation.
418	# In particular this theorem never rewrites or reassociates a floating sum.
419	def represent_fold(~Reader: Type,~Model: Data,~Accumulator: Data,~Context: Data,~pack_reader: Model -> Reader,
420	  state: Traversal.State<&2,&2,Model,Accumulator,Context>) -> Traversal.State<&1,&2,Reader,Accumulator,Context>:
421	  Traversal.State{reader,accumulator,position,context} = state
422	  Traversal.State{pack_reader(reader),accumulator,position,context}
423	
424	def model_fold_step(~Model: Data,~Element: Data,~Accumulator: Data,~Context: Data,
425	  ~sample: Model -> Context -> U32 -> Element,~combine: Accumulator -> Element -> Accumulator,
426	  state: Traversal.State<&2,&2,Model,Accumulator,Context>) -> Traversal.State<&2,&2,Model,Accumulator,Context>:
427	  Traversal.State{+reader,accumulator,+position,+context} = state
428	  Traversal.State{reader,combine(accumulator,sample(reader,context,position)),(position + 1 : U32),context}
429	
430	def fold_step_refines_model(~Reader: Type,~Model: Data,~Element: Data,~Accumulator: Data,~Context: Data,
431	  ~pack_reader: Model -> Reader,~read: Reader -> Context -> U32 -> Reader & Element,
432	  ~sample: Model -> Context -> U32 -> Element,~combine: Accumulator -> Element -> Accumulator,
433	  ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
434	    {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
435	  +state: Traversal.State<&2,&2,Model,Accumulator,Context>) ->
436	  {Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine,
437	      represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,state)) ==
438	    represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,
439	      model_fold_step(~Model,~Element,~Accumulator,~Context,~sample,~combine,state)) : Traversal.State<&1,&2,Reader,Accumulator,Context>}:
440	  Traversal.State{+reader,+accumulator,+position,+context} = state
441	  %Equal.sym(Reader & Element,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),
442	    read_matches(reader,context,position)) :
443	    {Traversal.fold_value(~Reader,~Element,~Accumulator,~Context,~combine,accumulator,position,context,_) ==
444	      represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,
445	        model_fold_step(~Model,~Element,~Accumulator,~Context,~sample,~combine,Traversal.State{reader,accumulator,position,context})) :
446	      Traversal.State<&1,&2,Reader,Accumulator,Context>}
447	  {==}
448	
449	def fold_refines_ordered_model(~Reader: Type,~Model: Data,~Element: Data,~Accumulator: Data,~Context: Data,
450	  ~pack_reader: Model -> Reader,~read: Reader -> Context -> U32 -> Reader & Element,
451	  ~sample: Model -> Context -> U32 -> Element,~combine: Accumulator -> Element -> Accumulator,
452	  ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
453	    {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
454	  +count: Nat,+state: Traversal.State<&2,&2,Model,Accumulator,Context>) ->
455	  {Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine),
456	      count,represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,state)) ==
457	    represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,
458	      Loop.run(~Traversal.State<&2,&2,Model,Accumulator,Context>,~model_fold_step(~Model,~Element,~Accumulator,~Context,~sample,~combine),count,state)) :
459	    Traversal.State<&1,&2,Reader,Accumulator,Context>}:
460	  Projection.iteration_refines_model(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.State<&2,&2,Model,Accumulator,Context>,
461	    ~Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine),~model_fold_step(~Model,~Element,~Accumulator,~Context,~sample,~combine),
462	    ~represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader),
463	    ~fold_step_refines_model(~Reader,~Model,~Element,~Accumulator,~Context,~pack_reader,~read,~sample,~combine,~read_matches),count,state)
464	
465	# The eight reads of a round are the samples at position, position + 1, ...
466	def read_last_matches(~Reader: Type,~Model: Data,~Element: Data,~Context: Data,~pack_reader: Model -> Reader,
467	  ~read: Reader -> Context -> U32 -> Reader & Element,~sample: Model -> Context -> U32 -> Element,
468	  ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
469	    {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
470	  +reader: Model,+context: Context,+position: U32,+a: Element,+b: Element,+c: Element,+d: Element,+e: Element,+f: Element,+g: Element) ->
471	  {Traversal.read_last(~Reader,~Element,a,b,c,d,e,f,g,read(pack_reader(reader),context,position)) ==
472	    (pack_reader(reader),Traversal.Eight{a,b,c,d,e,f,g,sample(reader,context,position)}) : Reader & Traversal.Eight<Element>}:
473	  %Equal.sym(Reader & Element,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),read_matches(reader,context,position)) :
474	    {Traversal.read_last(~Reader,~Element,a,b,c,d,e,f,g,_) == (pack_reader(reader),Traversal.Eight{a,b,c,d,e,f,g,sample(reader,context,position)}) : Reader & Traversal.Eight<Element>}
475	  {==}
476	
477	def read_seventh_matches(~Reader: Type,~Model: Data,~Element: Data,~Context: Data,~pack_reader: Model -> Reader,
478	  ~read: Reader -> Context -> U32 -> Reader & Element,~sample: Model -> Context -> U32 -> Element,
479	  ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
480	    {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
481	  +reader: Model,+context: Context,+position: U32,+a: Element,+b: Element,+c: Element,+d: Element,+e: Element,+f: Element) ->
482	  {Traversal.read_seventh(~Reader,~Element,~Context,~read,position,context,a,b,c,d,e,f,read(pack_reader(reader),context,position)) ==
483	    (pack_reader(reader),Traversal.Eight{a,b,c,d,e,f,sample(reader,context,position),sample(reader,context,(position + 1 : U32))}) : Reader & Traversal.Eight<Element>}:
484	  %Equal.sym(Reader & Element,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),read_matches(reader,context,position)) :
485	    {Traversal.read_seventh(~Reader,~Element,~Context,~read,position,context,a,b,c,d,e,f,_) ==
486	      (pack_reader(reader),Traversal.Eight{a,b,c,d,e,f,sample(reader,context,position),sample(reader,context,(position + 1 : U32))}) : Reader & Traversal.Eight<Element>}
487	  read_last_matches(~Reader,~Model,~Element,~Context,~pack_reader,~read,~sample,~read_matches,reader,context,(position + 1 : U32),a,b,c,d,e,f,sample(reader,context,position))
488	
489	def read_sixth_matches(~Reader: Type,~Model: Data,~Element: Data,~Context: Data,~pack_reader: Model -> Reader,
490	  ~read: Reader -> Context -> U32 -> Reader & Element,~sample: Model -> Context -> U32 -> Element,
491	  ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
492	    {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
493	  +reader: Model,+context: Context,+position: U32,+a: Element,+b: Element,+c: Element,+d: Element,+e: Element) ->
494	  {Traversal.read_sixth(~Reader,~Element,~Context,~read,position,context,a,b,c,d,e,read(pack_reader(reader),context,position)) ==
495	    (pack_reader(reader),Traversal.Eight{a,b,c,d,e,sample(reader,context,position),sample(reader,context,(position + 1 : U32)),
496	      sample(reader,context,((position + 1 : U32) + 1 : U32))}) : Reader & Traversal.Eight<Element>}:
497	  %Equal.sym(Reader & Element,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),read_matches(reader,context,position)) :
498	    {Traversal.read_sixth(~Reader,~Element,~Context,~read,position,context,a,b,c,d,e,_) ==
499	      (pack_reader(reader),Traversal.Eight{a,b,c,d,e,sample(reader,context,position),sample(reader,context,(position + 1 : U32)),
500	        sample(reader,context,((position + 1 : U32) + 1 : U32))}) : Reader & Traversal.Eight<Element>}
501	  read_seventh_matches(~Reader,~Model,~Element,~Context,~pack_reader,~read,~sample,~read_matches,reader,context,(position + 1 : U32),a,b,c,d,e,sample(reader,context,position))
502	
503	def read_fifth_matches(~Reader: Type,~Model: Data,~Element: Data,~Context: Data,~pack_reader: Model -> Reader,
504	  ~read: Reader -> Context -> U32 -> Reader & Element,~sample: Model -> Context -> U32 -> Element,
505	  ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
506	    {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
507	  +reader: Model,+context: Context,+position: U32,+a: Element,+b: Element,+c: Element,+d: Element) ->
508	  {Traversal.read_fifth(~Reader,~Element,~Context,~read,position,context,a,b,c,d,read(pack_reader(reader),context,position)) ==
509	    (pack_reader(reader),Traversal.Eight{a,b,c,d,sample(reader,context,position),sample(reader,context,(position + 1 : U32)),
510	      sample(reader,context,((position + 1 : U32) + 1 : U32)),sample(reader,context,(((position + 1 : U32) + 1 : U32) + 1 : U32))}) : Reader & Traversal.Eight<Element>}:
511	  %Equal.sym(Reader & Element,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),read_matches(reader,context,position)) :
512	    {Traversal.read_fifth(~Reader,~Element,~Context,~read,position,context,a,b,c,d,_) ==
513	      (pack_reader(reader),Traversal.Eight{a,b,c,d,sample(reader,context,position),sample(reader,context,(position + 1 : U32)),
514	        sample(reader,context,((position + 1 : U32) + 1 : U32)),sample(reader,context,(((position + 1 : U32) + 1 : U32) + 1 : U32))}) : Reader & Traversal.Eight<Element>}
515	  read_sixth_matches(~Reader,~Model,~Element,~Context,~pack_reader,~read,~sample,~read_matches,reader,context,(position + 1 : U32),a,b,c,d,sample(reader,context,position))
516	
517	def read_fourth_matches(~Reader: Type,~Model: Data,~Element: Data,~Context: Data,~pack_reader: Model -> Reader,
518	  ~read: Reader -> Context -> U32 -> Reader & Element,~sample: Model -> Context -> U32 -> Element,
519	  ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
520	    {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
521	  +reader: Model,+context: Context,+position: U32,+a: Element,+b: Element,+c: Element) ->
522	  {Traversal.read_fourth(~Reader,~Element,~Context,~read,position,context,a,b,c,read(pack_reader(reader),context,position)) ==
523	    (pack_reader(reader),Traversal.Eight{a,b,c,sample(reader,context,position),sample(reader,context,(position + 1 : U32)),
524	      sample(reader,context,((position + 1 : U32) + 1 : U32)),sample(reader,context,(((position + 1 : U32) + 1 : U32) + 1 : U32)),
525	      sample(reader,context,((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32))}) : Reader & Traversal.Eight<Element>}:
526	  %Equal.sym(Reader & Element,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),read_matches(reader,context,position)) :
527	    {Traversal.read_fourth(~Reader,~Element,~Context,~read,position,context,a,b,c,_) ==
528	      (pack_reader(reader),Traversal.Eight{a,b,c,sample(reader,context,position),sample(reader,context,(position + 1 : U32)),
529	        sample(reader,context,((position + 1 : U32) + 1 : U32)),sample(reader,context,(((position + 1 : U32) + 1 : U32) + 1 : U32)),
530	        sample(reader,context,((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32))}) : Reader & Traversal.Eight<Element>}
531	  read_fifth_matches(~Reader,~Model,~Element,~Context,~pack_reader,~read,~sample,~read_matches,reader,context,(position + 1 : U32),a,b,c,sample(reader,context,position))
532	
533	def read_third_matches(~Reader: Type,~Model: Data,~Element: Data,~Context: Data,~pack_reader: Model -> Reader,
534	  ~read: Reader -> Context -> U32 -> Reader & Element,~sample: Model -> Context -> U32 -> Element,
535	  ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
536	    {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
537	  +reader: Model,+context: Context,+position: U32,+a: Element,+b: Element) ->
538	  {Traversal.read_third(~Reader,~Element,~Context,~read,position,context,a,b,read(pack_reader(reader),context,position)) ==
539	    (pack_reader(reader),Traversal.Eight{a,b,sample(reader,context,position),sample(reader,context,(position + 1 : U32)),
540	      sample(reader,context,((position + 1 : U32) + 1 : U32)),sample(reader,context,(((position + 1 : U32) + 1 : U32) + 1 : U32)),
541	      sample(reader,context,((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32)),
542	      sample(reader,context,(((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32))}) : Reader & Traversal.Eight<Element>}:
543	  %Equal.sym(Reader & Element,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),read_matches(reader,context,position)) :
544	    {Traversal.read_third(~Reader,~Element,~Context,~read,position,context,a,b,_) ==
545	      (pack_reader(reader),Traversal.Eight{a,b,sample(reader,context,position),sample(reader,context,(position + 1 : U32)),
546	        sample(reader,context,((position + 1 : U32) + 1 : U32)),sample(reader,context,(((position + 1 : U32) + 1 : U32) + 1 : U32)),
547	        sample(reader,context,((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32)),
548	        sample(reader,context,(((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32))}) : Reader & Traversal.Eight<Element>}
549	  read_fourth_matches(~Reader,~Model,~Element,~Context,~pack_reader,~read,~sample,~read_matches,reader,context,(position + 1 : U32),a,b,sample(reader,context,position))
550	
551	def read_second_matches(~Reader: Type,~Model: Data,~Element: Data,~Context: Data,~pack_reader: Model -> Reader,
552	  ~read: Reader -> Context -> U32 -> Reader & Element,~sample: Model -> Context -> U32 -> Element,
553	  ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
554	    {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
555	  +reader: Model,+context: Context,+position: U32,+a: Element) ->
556	  {Traversal.read_second(~Reader,~Element,~Context,~read,position,context,a,read(pack_reader(reader),context,position)) ==
557	    (pack_reader(reader),Traversal.Eight{a,sample(reader,context,position),sample(reader,context,(position + 1 : U32)),
558	      sample(reader,context,((position + 1 : U32) + 1 : U32)),sample(reader,context,(((position + 1 : U32) + 1 : U32) + 1 : U32)),
559	      sample(reader,context,((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32)),
560	      sample(reader,context,(((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32)),
561	      sample(reader,context,((((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32))}) : Reader & Traversal.Eight<Element>}:
562	  %Equal.sym(Reader & Element,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),read_matches(reader,context,position)) :
563	    {Traversal.read_second(~Reader,~Element,~Context,~read,position,context,a,_) ==
564	      (pack_reader(reader),Traversal.Eight{a,sample(reader,context,position),sample(reader,context,(position + 1 : U32)),
565	        sample(reader,context,((position + 1 : U32) + 1 : U32)),sample(reader,context,(((position + 1 : U32) + 1 : U32) + 1 : U32)),
566	        sample(reader,context,((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32)),
567	        sample(reader,context,(((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32)),
568	        sample(reader,context,((((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32))}) : Reader & Traversal.Eight<Element>}
569	  read_third_matches(~Reader,~Model,~Element,~Context,~pack_reader,~read,~sample,~read_matches,reader,context,(position + 1 : U32),a,sample(reader,context,position))
570	
571	# The model of eight fold steps.
572	def model_round(~Model: Data,~Element: Data,~Accumulator: Data,~Context: Data,
573	  ~sample: Model -> Context -> U32 -> Element,~combine: Accumulator -> Element -> Accumulator,
574	  state: Traversal.State<&2,&2,Model,Accumulator,Context>) -> Traversal.State<&2,&2,Model,Accumulator,Context>:
575	  Loop.run(~Traversal.State<&2,&2,Model,Accumulator,Context>,~model_fold_step(~Model,~Element,~Accumulator,~Context,~sample,~combine),8n,state)
576	
577	def round_refines_model(~Reader: Type,~Model: Data,~Element: Data,~Accumulator: Data,~Context: Data,
578	  ~pack_reader: Model -> Reader,~read: Reader -> Context -> U32 -> Reader & Element,
579	  ~sample: Model -> Context -> U32 -> Element,~combine: Accumulator -> Element -> Accumulator,
580	  ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
581	    {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
582	  +state: Traversal.State<&2,&2,Model,Accumulator,Context>) ->
583	  {Traversal.fold_round(~Reader,~Element,~Accumulator,~Context,~read,~combine,
584	      represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,state)) ==
585	    represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,
586	      model_round(~Model,~Element,~Accumulator,~Context,~sample,~combine,state)) : Traversal.State<&1,&2,Reader,Accumulator,Context>}:
587	  Traversal.State{+reader,+accumulator,+position,+context} = state
588	  %Equal.sym(Reader & Element,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),read_matches(reader,context,position)) :
589	    {Traversal.round_value(~Reader,~Element,~Accumulator,~Context,~combine,accumulator,position,context,
590	      Traversal.read_eight(~Reader,~Element,~Context,~read,position,context,_)) ==
591	      represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,
592	        model_round(~Model,~Element,~Accumulator,~Context,~sample,~combine,Traversal.State{reader,accumulator,position,context})) : Traversal.State<&1,&2,Reader,Accumulator,Context>}
593	  %Equal.sym(Reader & Traversal.Eight<Element>,
594	    Traversal.read_second(~Reader,~Element,~Context,~read,(position + 1 : U32),context,sample(reader,context,position),read(pack_reader(reader),context,(position + 1 : U32))),
595	    (pack_reader(reader),Traversal.Eight{sample(reader,context,position),sample(reader,context,(position + 1 : U32)),
596	      sample(reader,context,((position + 1 : U32) + 1 : U32)),sample(reader,context,(((position + 1 : U32) + 1 : U32) + 1 : U32)),
597	      sample(reader,context,((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32)),
598	      sample(reader,context,(((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32)),
599	      sample(reader,context,((((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32)),
600	      sample(reader,context,(((((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32))}),
601	    read_second_matches(~Reader,~Model,~Element,~Context,~pack_reader,~read,~sample,~read_matches,reader,context,(position + 1 : U32),sample(reader,context,position))) :
602	    {Traversal.round_value(~Reader,~Element,~Accumulator,~Context,~combine,accumulator,position,context,_) ==
603	      represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,
604	        model_round(~Model,~Element,~Accumulator,~Context,~sample,~combine,Traversal.State{reader,accumulator,position,context})) : Traversal.State<&1,&2,Reader,Accumulator,Context>}
605	  {==}
606	
607	def round_steps(~Model: Data,~Element: Data,~Accumulator: Data,~Context: Data,
608	  ~sample: Model -> Context -> U32 -> Element,~combine: Accumulator -> Element -> Accumulator,-state: Traversal.State<&2,&2,Model,Accumulator,Context>) ->
609	  {model_round(~Model,~Element,~Accumulator,~Context,~sample,~combine,state) ==
610	    Loop.run(~Traversal.State<&2,&2,Model,Accumulator,Context>,~model_fold_step(~Model,~Element,~Accumulator,~Context,~sample,~combine),8n,state) : Traversal.State<&2,&2,Model,Accumulator,Context>}:
611	  {==}
612	
613	# fold_rounds runs the ordered model fold: count % 8 steps, then rounds of eight.
614	def rounds_refine_ordered_model(~Reader: Type,~Model: Data,~Element: Data,~Accumulator: Data,~Context: Data,
615	  ~pack_reader: Model -> Reader,~read: Reader -> Context -> U32 -> Reader & Element,
616	  ~sample: Model -> Context -> U32 -> Element,~combine: Accumulator -> Element -> Accumulator,
617	  ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
618	    {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
619	  +count: Nat,+state: Traversal.State<&2,&2,Model,Accumulator,Context>) ->
620	  {Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_round(~Reader,~Element,~Accumulator,~Context,~read,~combine),Nat.div(count,8n),
621	      Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine),Nat.mod(count,8n),
622	        represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,state))) ==
623	    represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,
624	      Loop.run(~Traversal.State<&2,&2,Model,Accumulator,Context>,~model_fold_step(~Model,~Element,~Accumulator,~Context,~sample,~combine),count,state)) :
625	    Traversal.State<&1,&2,Reader,Accumulator,Context>}:
626	  +head = Loop.run(~Traversal.State<&2,&2,Model,Accumulator,Context>,~model_fold_step(~Model,~Element,~Accumulator,~Context,~sample,~combine),Nat.mod(count,8n),state)
627	  %Projection.head_then_eights(~Traversal.State<&2,&2,Model,Accumulator,Context>,~model_fold_step(~Model,~Element,~Accumulator,~Context,~sample,~combine),
628	    ~model_round(~Model,~Element,~Accumulator,~Context,~sample,~combine),~round_steps(~Model,~Element,~Accumulator,~Context,~sample,~combine),count,state) :
629	    {Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_round(~Reader,~Element,~Accumulator,~Context,~read,~combine),Nat.div(count,8n),
630	        Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine),Nat.mod(count,8n),
631	          represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,state))) ==
632	      represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,_) : Traversal.State<&1,&2,Reader,Accumulator,Context>}
633	  %Equal.sym(Traversal.State<&1,&2,Reader,Accumulator,Context>,
634	    Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine),Nat.mod(count,8n),
635	      represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,state)),
636	    represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,head),
637	    fold_refines_ordered_model(~Reader,~Model,~Element,~Accumulator,~Context,~pack_reader,~read,~sample,~combine,~read_matches,Nat.mod(count,8n),state)) :
638	    {Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_round(~Reader,~Element,~Accumulator,~Context,~read,~combine),Nat.div(count,8n),_) ==
639	      represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,
640	        Loop.run(~Traversal.State<&2,&2,Model,Accumulator,Context>,~model_round(~Model,~Element,~Accumulator,~Context,~sample,~combine),Nat.div(count,8n),head)) :
641	      Traversal.State<&1,&2,Reader,Accumulator,Context>}
642	  Projection.iteration_refines_model(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.State<&2,&2,Model,Accumulator,Context>,
643	    ~Traversal.fold_round(~Reader,~Element,~Accumulator,~Context,~read,~combine),~model_round(~Model,~Element,~Accumulator,~Context,~sample,~combine),
644	    ~represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader),
645	    ~round_refines_model(~Reader,~Model,~Element,~Accumulator,~Context,~pack_reader,~read,~sample,~combine,~read_matches),Nat.div(count,8n),head)
646	
647	# In-place transforms retain one owner and use the same generic loop lifting.
648	def represent_map(~Element: Data,~Context: Data,
649	  state: Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>) -> Traversal.State<&2,&1,Unit,Array<Element>,Context>:
650	  Traversal.State{Unit{},output,position,context} = state
651	  Traversal.State{Unit{},Tree.pack(Element,output),position,context}
652	
653	def unindexed(~Element: Data,~Context: Data,~map: Context -> Element -> Element,context: Context,position: U32,value: Element) -> Element:
654	  map(context,value)
655	
656	def model_map_step(~Element: Data,~Context: Data,~map: Context -> U32 -> Element -> Element,
657	  state: Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>) -> Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>:
658	  Traversal.State{Unit{},+output,+position,+context} = state
659	  Traversal.State{Unit{},Tree.write(Element,output,position,map(context,position,Tree.read(Element,output,position))),
660	    (position + 1 : U32),context}
661	
662	def map_step_refines_model(~Element: Data,~Context: Data,~map: Context -> Element -> Element,
663	  +state: Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>) ->
664	  {Traversal.map_step(~Element,~Context,~map,represent_map(~Element,~Context,state)) ==
665	    represent_map(~Element,~Context,model_map_step(~Element,~Context,~unindexed(~Element,~Context,~map),state)) : Traversal.State<&2,&1,Unit,Array<Element>,Context>}:
666	  Traversal.State{Unit{},+output,+position,+context} = state
667	  %Equal.sym(Array<Element> & Element,Array.get(Element,Tree.pack(Element,output),position),
668	    (Tree.pack(Element,output),Tree.read(Element,output,position)),StorageLaws.read(Element,output,position)) :
669	    {Traversal.mapped_value(~Element,~Context,~map,position,context,_) ==
670	      represent_map(~Element,~Context,model_map_step(~Element,~Context,~unindexed(~Element,~Context,~map),state)) : Traversal.State<&2,&1,Unit,Array<Element>,Context>}
671	  %Equal.sym(Array<Element>,Array.set(Element,Tree.pack(Element,output),position,map(context,Tree.read(Element,output,position))),
672	    Tree.pack(Element,Tree.write(Element,output,position,map(context,Tree.read(Element,output,position)))),
673	    StorageLaws.write(Element,output,position,map(context,Tree.read(Element,output,position)))) :
674	    {Traversal.State{Unit{},_,(position + 1 : U32),context} ==
675	      represent_map(~Element,~Context,model_map_step(~Element,~Context,~unindexed(~Element,~Context,~map),state)) : Traversal.State<&2,&1,Unit,Array<Element>,Context>}
676	  {==}
677	
678	def map_loop_refines_model(~Element: Data,~Context: Data,~map: Context -> Element -> Element,
679	  +count: Nat,+state: Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>) ->
680	  {Loop.run(~Traversal.State<&2,&1,Unit,Array<Element>,Context>,~Traversal.map_step(~Element,~Context,~map),
681	      count,represent_map(~Element,~Context,state)) ==
682	    represent_map(~Element,~Context,Loop.run(~Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>,
683	      ~model_map_step(~Element,~Context,~unindexed(~Element,~Context,~map)),count,state)) : Traversal.State<&2,&1,Unit,Array<Element>,Context>}:
684	  Projection.iteration_refines_model(~Traversal.State<&2,&1,Unit,Array<Element>,Context>,~Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>,
685	    ~Traversal.map_step(~Element,~Context,~map),~model_map_step(~Element,~Context,~unindexed(~Element,~Context,~map)),~represent_map(~Element,~Context),
686	    ~map_step_refines_model(~Element,~Context,~map),count,state)
687	
688	# One representation proof covers the entire indexed output traversal. The
689	# strategy supplies a single-step result, not another outer-loop induction.
690	
691	# In-place binary updates use the current destination value in left position.
692	# This theorem models sequential writes, including modular/overlapping raw
693	# addresses. Valid view guards and non-overlap are separate obligations.
694	def model_update_step(~Model: Data,~Element: Data,~Sample: Data,~Context: Data,
695	  ~sample: Model -> Context -> U32 -> Sample,~combine: Element -> Sample -> Element,~destination: Context -> U32 -> U32,
696	  state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) -> Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>:
697	  Traversal.State{+reader,+output,+position,+context} = state
698	  Traversal.State{reader,Tree.write(Element,output,destination(context,position),
699	    combine(Tree.read(Element,output,destination(context,position)),sample(reader,context,position))),(position + 1 : U32),context}
700	
701	def update_step_refines_model(~Reader: Type,~Model: Data,~Element: Data,~Sample: Data,~Context: Data,
702	  ~pack_reader: Model -> Reader,~read: Reader -> Context -> U32 -> Reader & Sample,
703	  ~sample: Model -> Context -> U32 -> Sample,~combine: Element -> Sample -> Element,~destination: Context -> U32 -> U32,
704	  ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
705	    {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Sample},
706	  +state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) ->
707	  {Traversal.update_step(~Reader,~Element,~Sample,~Context,~read,~combine,~destination,
708	      represent(~Reader,~Model,~Element,~Context,~pack_reader,state)) ==
709	    represent(~Reader,~Model,~Element,~Context,~pack_reader,model_update_step(~Model,~Element,~Sample,~Context,~sample,~combine,~destination,state)) :
710	    Traversal.State<&1,&1,Reader,Array<Element>,Context>}:
711	  Traversal.State{+reader,+output,+position,+context} = state
712	  %Equal.sym(Array<Element> & Element,Array.get(Element,Tree.pack(Element,output),destination(context,position)),
713	    (Tree.pack(Element,output),Tree.read(Element,output,destination(context,position))),StorageLaws.read(Element,output,destination(context,position))) :
714	    {Traversal.update_current(~Reader,~Element,~Sample,~Context,~read,~combine,~destination,pack_reader(reader),position,context,_) ==
715	      represent(~Reader,~Model,~Element,~Context,~pack_reader,model_update_step(~Model,~Element,~Sample,~Context,~sample,~combine,~destination,
716	        Traversal.State{reader,output,position,context})) : Traversal.State<&1,&1,Reader,Array<Element>,Context>}
717	  %Equal.sym(Reader & Sample,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),read_matches(reader,context,position)) :
718	    {Traversal.update_sample(~Reader,~Element,~Sample,~Context,~combine,~destination,position,context,Tree.pack(Element,output),
719	      Tree.read(Element,output,destination(context,position)),_) ==
720	      represent(~Reader,~Model,~Element,~Context,~pack_reader,model_update_step(~Model,~Element,~Sample,~Context,~sample,~combine,~destination,
721	        Traversal.State{reader,output,position,context})) : Traversal.State<&1,&1,Reader,Array<Element>,Context>}
722	  %Equal.sym(Array<Element>,Array.set(Element,Tree.pack(Element,output),destination(context,position),
723	      combine(Tree.read(Element,output,destination(context,position)),sample(reader,context,position))),
724	    Tree.pack(Element,Tree.write(Element,output,destination(context,position),
725	      combine(Tree.read(Element,output,destination(context,position)),sample(reader,context,position)))),
726	    StorageLaws.write(Element,output,destination(context,position),combine(Tree.read(Element,output,destination(context,position)),sample(reader,context,position)))) :
727	    {Traversal.State{pack_reader(reader),_,(position + 1 : U32),context} ==
728	      represent(~Reader,~Model,~Element,~Context,~pack_reader,model_update_step(~Model,~Element,~Sample,~Context,~sample,~combine,~destination,
729	        Traversal.State{reader,output,position,context})) : Traversal.State<&1,&1,Reader,Array<Element>,Context>}
730	  {==}
731	
732	def update_refines_model(~Reader: Type,~Model: Data,~Element: Data,~Sample: Data,~Context: Data,
733	  ~pack_reader: Model -> Reader,~read: Reader -> Context -> U32 -> Reader & Sample,
734	  ~sample: Model -> Context -> U32 -> Sample,~combine: Element -> Sample -> Element,~destination: Context -> U32 -> U32,
735	  ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
736	    {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Sample},
737	  +count: Nat,+state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) ->
738	  {Traversal.update(~Reader,~Element,~Sample,~Context,~read,~combine,~destination,count,
739	      represent(~Reader,~Model,~Element,~Context,~pack_reader,state)) ==
740	    represent(~Reader,~Model,~Element,~Context,~pack_reader,
741	      Loop.run(~Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>,
742	        ~model_update_step(~Model,~Element,~Sample,~Context,~sample,~combine,~destination),count,state)) :
743	    Traversal.State<&1,&1,Reader,Array<Element>,Context>}:
744	  Projection.iteration_refines_model(~Traversal.State<&1,&1,Reader,Array<Element>,Context>,~Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>,
745	    ~Traversal.update_step(~Reader,~Element,~Sample,~Context,~read,~combine,~destination),
746	    ~model_update_step(~Model,~Element,~Sample,~Context,~sample,~combine,~destination),
747	    ~represent(~Reader,~Model,~Element,~Context,~pack_reader),
748	    ~update_step_refines_model(~Reader,~Model,~Element,~Sample,~Context,~pack_reader,~read,~sample,~combine,~destination,~read_matches),count,state)
749	
750	# A state with a moving counter is the same indexed fold as its stores.
751	def indexed_loop(~Runtime: Type,~Model: Data,~Context: Data,
752	  ~step: Runtime -> Runtime,~update: U32 -> Context -> Model -> Model,
753	  ~represent: Context -> U32 -> Model -> Runtime,
754	  ~step_matches: @+context: Context -> @+index: U32 -> @+state: Model ->
755	    {step(represent(context,index,state)) == represent(context,(index + 1 : U32),update(index,context,state)) : Runtime},
756	  count: Nat,+index: U32,+context: Context,+state: Model) ->
757	  {Loop.run(~Runtime,~step,count,represent(context,index,state)) ==
758	    represent(context,(index + U32.from_nat(count) : U32),Traversal.indexed_fold(~Model,~Context,~update,count,index,context,state)) : Runtime}:
759	  match count:
760	    case 0n:
761	      %Equal.sym(U32,(index + 0 : U32),index,Arithmetic.add_zero(index)) :
762	        {represent(context,index,state) == represent(context,_,state) : Runtime}
763	      {==}
764	    case 1n+ +rest:
765	      %Equal.sym(Runtime,step(represent(context,index,state)),represent(context,(index + 1 : U32),update(index,context,state)),step_matches(context,index,state)) :
766	        {Loop.run(~Runtime,~step,rest,_) == represent(context,(index + U32.from_nat(1n+rest) : U32),
767	          Traversal.indexed_fold(~Model,~Context,~update,rest,(index + 1 : U32),context,update(index,context,state))) : Runtime}
768	      %Equal.sym(U32,(index + U32.from_nat(1n+rest) : U32),((index + 1 : U32) + U32.from_nat(rest) : U32),Projection.indexed_successor(index,rest)) :
769	        {Loop.run(~Runtime,~step,rest,represent(context,(index + 1 : U32),update(index,context,state))) ==
770	          represent(context,_,Traversal.indexed_fold(~Model,~Context,~update,rest,(index + 1 : U32),context,update(index,context,state))) : Runtime}
771	      indexed_loop(~Runtime,~Model,~Context,~step,~update,~represent,~step_matches,rest,(index + 1 : U32),context,update(index,context,state))
772	
773	def indexed_fold_refines_model(~Runtime: Type,~Model: Data,~Context: Data,
774	  ~update: U32 -> Context -> Runtime -> Runtime,~model_update: U32 -> Context -> Model -> Model,
775	  ~represent: Model -> Runtime,
776	  ~step_matches: @+index: U32 -> @+context: Context -> @+state: Model ->
777	    {update(index,context,represent(state)) == represent(model_update(index,context,state)) : Runtime},
778	  +count: Nat,+index: U32,+context: Context,+state: Model) ->
779	  {Traversal.indexed_fold(~Runtime,~Context,~update,count,index,context,represent(state)) ==
780	    represent(Traversal.indexed_fold(~Model,~Context,~model_update,count,index,context,state)) : Runtime}:
781	  match count:
782	    case 0n: {==}
783	    case 1n+ +rest:
784	      %Equal.sym(Runtime,update(index,context,represent(state)),represent(model_update(index,context,state)),step_matches(index,context,state)) :
785	        {Traversal.indexed_fold(~Runtime,~Context,~update,rest,(index + 1 : U32),context,_) ==
786	          represent(Traversal.indexed_fold(~Model,~Context,~model_update,rest,(index + 1 : U32),context,model_update(index,context,state))) : Runtime}
787	      indexed_fold_refines_model(~Runtime,~Model,~Context,~update,~model_update,~represent,~step_matches,
788	        rest,(index + 1 : U32),context,model_update(index,context,state))
789	
790	# An indexed traversal transports a fixed observation through its own update.
791	def indexed_fold_observes(~State: Data,~Observation: Data,~Context: Data,
792	  ~update: U32 -> Context -> State -> State,~observe: State -> Observation,
793	  ~observed_update: U32 -> Context -> Observation -> Observation,
794	  ~step_observed: @+index: U32 -> @+context: Context -> @+state: State ->
795	    {observe(update(index,context,state)) == observed_update(index,context,observe(state)) : Observation},
796	  count: Nat,+first: U32,+context: Context,+state: State) ->
797	  {observe(Traversal.indexed_fold(~State,~Context,~update,count,first,context,state)) ==
798	    Traversal.indexed_fold(~Observation,~Context,~observed_update,count,first,context,observe(state)) : Observation}:
799	  match count:
800	    case 0n: {==}
801	    case 1n+rest:
802	      %step_observed(first,context,state) :
803	        {observe(Traversal.indexed_fold(~State,~Context,~update,rest,(first + 1 : U32),context,update(first,context,state))) ==
804	          Traversal.indexed_fold(~Observation,~Context,~observed_update,rest,(first + 1 : U32),context,_) : Observation}
805	      indexed_fold_observes(~State,~Observation,~Context,~update,~observe,~observed_update,~step_observed,
806	        rest,(first + 1 : U32),context,update(first,context,state))
807	
808	def indexed_fold_fixed(~State: Data,~Context: Data,~update: U32 -> Context -> State -> State,
809	  ~fixed: @+index: U32 -> @+context: Context -> @+state: State -> {update(index,context,state) == state : State},
810	  count: Nat,+first: U32,+context: Context,+state: State) ->
811	  {Traversal.indexed_fold(~State,~Context,~update,count,first,context,state) == state : State}:
812	  match count:
813	    case 0n: {==}
814	    case 1n+rest:
815	      %Equal.sym(State,update(first,context,state),state,fixed(first,context,state)) :
816	        {Traversal.indexed_fold(~State,~Context,~update,rest,(first + 1 : U32),context,_) == state : State}
817	      indexed_fold_fixed(~State,~Context,~update,~fixed,rest,(first + 1 : U32),context,state)
818	
819	# One bounded induction carries capacity, preserved sources and completed
820	# output values together. A strategy proves its local update obligation;
821	# it does not reimplement the whole output traversal proof.
822	def indexed_fold_change_context(~State: Data,~Outer: Data,~Inner: Data,
823	  ~project: Outer -> Inner,~outer_step: U32 -> Outer -> State -> State,~inner_step: U32 -> Inner -> State -> State,
824	  ~same_step: @+index: U32 -> @+context: Outer -> @+state: State ->
825	    {outer_step(index,context,state) == inner_step(index,project(context),state) : State},
826	  +count: Nat,+first: U32,+context: Outer,+state: State) ->
827	  {Traversal.indexed_fold(~State,~Outer,~outer_step,count,first,context,state) ==
828	    Traversal.indexed_fold(~State,~Inner,~inner_step,count,first,project(context),state) : State}:
829	  match count:
830	    case 0n: {==}
831	    case 1n+ +rest:
832	      %Equal.sym(State,outer_step(first,context,state),inner_step(first,project(context),state),same_step(first,context,state)) :
833	        {Traversal.indexed_fold(~State,~Outer,~outer_step,rest,(first + 1 : U32),context,_) ==
834	          Traversal.indexed_fold(~State,~Inner,~inner_step,rest,(first + 1 : U32),project(context),inner_step(first,project(context),state)) : State}
835	      indexed_fold_change_context(~State,~Outer,~Inner,~project,~outer_step,~inner_step,~same_step,
836	        rest,(first + 1 : U32),context,inner_step(first,project(context),state))
837	
838	def indexed_fold_preserves_invariant(~State: Data,~Context: Data,
839	  ~limit: Context -> Nat,~Invariant: Context -> Nat -> State -> Data,
840	  ~update: U32 -> Context -> State -> State,
841	  ~preserve: @+context: Context -> @+index: Nat -> @+state: State ->
842	    {Nat.is_lt(index,limit(context)) == True{} : Bool} -> Invariant(context,index,state) ->
843	    Invariant(context,1n+index,update(U32.from_nat(index),context,state)),
844	  +count: Nat,+first: Nat,+context: Context,+state: State,
845	  +room: {Nat.is_le(Nat.add(first,count),limit(context)) == True{} : Bool},
846	  evidence: Invariant(context,first,state)) ->
847	  Invariant(context,Nat.add(first,count),Traversal.indexed_fold(~State,~Context,~update,count,U32.from_nat(first),context,state)):
848	  match count:
849	    case 0n:
850	      %Equal.sym(Nat,Nat.add(first,0n),first,Addition.zero_right(first)) : Invariant(context,_,state)
851	      evidence
852	    case 1n+ +rest:
853	      %Equal.sym(U32,(U32.from_nat(first) + 1 : U32),U32.from_nat(1n+first),Bounds.add_one(U32.from_nat(first))) :
854	        Invariant(context,Nat.add(first,1n+rest),Traversal.indexed_fold(~State,~Context,~update,rest,_,context,update(U32.from_nat(first),context,state)))
855	      %Equal.sym(Nat,Nat.add(first,1n+rest),1n+Nat.add(first,rest),Addition.successor_right(first,rest)) :
856	        Invariant(context,_,Traversal.indexed_fold(~State,~Context,~update,rest,U32.from_nat(1n+first),context,update(U32.from_nat(first),context,state)))
857	      indexed_fold_preserves_invariant(~State,~Context,~limit,~Invariant,~update,~preserve,rest,1n+first,context,update(U32.from_nat(first),context,state),
858	        Order.advance_room(first,rest,limit(context),room),preserve(context,first,state,Order.room_index(first,rest,limit(context),room),evidence))
859	
860	# Splitting a traversal preserves every state update in the same order. The
861	# boundary uses modular U32 conversion; no scalar/FP32-specific induction.
862	def indexed_fold_split(~Value: Type,~Context: Data,~update: U32 -> Context -> Value -> Value,
863	  +first: Nat,+second: Nat,+start: Nat,+context: Context,-initial: Value) ->
864	  {Traversal.indexed_fold(~Value,~Context,~update,Nat.add(first,second),U32.from_nat(start),context,initial) ==
865	    Traversal.indexed_fold(~Value,~Context,~update,second,U32.from_nat(Nat.add(start,first)),context,
866	      Traversal.indexed_fold(~Value,~Context,~update,first,U32.from_nat(start),context,initial)) : Value}:
867	  match first:
868	    case 0n:
869	      %Equal.sym(Nat,Nat.add(start,0n),start,Addition.zero_right(start)) :
870	        {Traversal.indexed_fold(~Value,~Context,~update,second,U32.from_nat(start),context,initial) ==
871	          Traversal.indexed_fold(~Value,~Context,~update,second,U32.from_nat(_),context,initial) : Value}
872	      {==}
873	    case 1n+ +rest:
874	      %Equal.sym(U32,(U32.from_nat(start) + 1 : U32),U32.from_nat(1n+start),Bounds.add_one(U32.from_nat(start))) :
875	        {Traversal.indexed_fold(~Value,~Context,~update,Nat.add(rest,second),_,context,update(U32.from_nat(start),context,initial)) ==
876	          Traversal.indexed_fold(~Value,~Context,~update,second,U32.from_nat(Nat.add(start,1n+rest)),context,
877	            Traversal.indexed_fold(~Value,~Context,~update,rest,_,context,update(U32.from_nat(start),context,initial))) : Value}
878	      %Equal.sym(Nat,Nat.add(start,1n+rest),1n+Nat.add(start,rest),Addition.successor_right(start,rest)) :
879	        {Traversal.indexed_fold(~Value,~Context,~update,Nat.add(rest,second),U32.from_nat(1n+start),context,update(U32.from_nat(start),context,initial)) ==
880	          Traversal.indexed_fold(~Value,~Context,~update,second,U32.from_nat(_),context,
881	            Traversal.indexed_fold(~Value,~Context,~update,rest,U32.from_nat(1n+start),context,update(U32.from_nat(start),context,initial))) : Value}
882	      indexed_fold_split(~Value,~Context,~update,rest,second,1n+start,context,update(U32.from_nat(start),context,initial))
883	
884	# Reading the values projection does not need the reader's representation.
885	def collect_prepend_values(~Reader: Type,~Element: Data,+value: Element,result: Reader & List<&2,Element>) ->
886	  {Pair.snd(Reader,List<&2,Element>,Traversal.collect_prepend(~&2,~Reader,~Element,value,result)) == value <> Pair.snd(Reader,List<&2,Element>,result) : List<&2,Element>}:
887	  (reader,values) = result
888	  {==}
889	
890	# One leaf supplies source, value and observation facts. The shared collection
891	# lifts all three together, including leaf premises for each input key.
892	def collected_leaf_frame(~Source: Data,~Element: Data,~Key: Data,~Context: Data,~Model: Data,
893	  ~Frame: Context -> Source -> Data,~ValueFrame: Context -> Element -> Data,
894	  ~observe: Context -> Element -> Model,~sample: Context -> Key -> Model,context: Context,key: Key,result: Source & Element) -> Data:
895	  (+source,+value) = result
896	  Shape.Both<Frame(context,source),Shape.Both<ValueFrame(context,value),{observe(context,value) == sample(context,key) : Model}>>
897	
898	def collected_list_frame(~Source: Data,~Element: Data,~Key: Data,~Context: Data,~Model: Data,
899	  ~Frame: Context -> Source -> Data,~ValueFrame: Context -> Element -> Data,
900	  ~observe: Context -> Element -> Model,~sample: Context -> Key -> Model,+context: Context,+keys: List<&2,Key>,result: Source & List<&2,Element>) -> Data:
901	  (+source,+values) = result
902	  Shape.Both<Frame(context,source),Shape.Both<Members.All(Element,{value => ValueFrame(context,value) : Element -> Data},values),
903	    {collect_values_context(~&2,~Model,~Element,~Context,~observe,values,context) ==
904	      collect_values_context(~&2,~Model,~Key,~Context,~sample,keys,context) : List<&2,Model>}>>
905	
906	def collect_list_certified_join(~Source: Data,~Element: Data,~Key: Data,~Context: Data,~Model: Data,
907	  ~Frame: Context -> Source -> Data,~ValueFrame: Context -> Element -> Data,
908	  ~observe: Context -> Element -> Model,~sample: Context -> Key -> Model,+context: Context,+key: Key,+rest: List<&2,Key>,+value: Element,
909	  tail: Source & List<&2,Element>,value_frame: ValueFrame(context,value),+value_equal: {observe(context,value) == sample(context,key) : Model},
910	  tail_frame: collected_list_frame(~Source,~Element,~Key,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,rest,tail)) ->
911	  collected_list_frame(~Source,~Element,~Key,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,key <> rest,Traversal.collect_prepend(~&2,~Source,~Element,value,tail)):
912	  (source,+values) = tail
913	  Shape.Both{source_frame,Shape.Both{values_frame,+values_equal}} = tail_frame
914	  Shape.Both{source_frame,Shape.Both{Shape.Both{value_frame,values_frame},
915	    %value_equal : {observe(context,value) <> collect_values_context(~&2,~Model,~Element,~Context,~observe,values,context) == _ <> collect_values_context(~&2,~Model,~Key,~Context,~sample,rest,context) : List<&2,Model>}
916	    Equal.cong(List<&2,Model>,List<&2,Model>,values => observe(context,value) <> values,
917	      collect_values_context(~&2,~Model,~Element,~Context,~observe,values,context),
918	      collect_values_context(~&2,~Model,~Key,~Context,~sample,rest,context),values_equal)}}
919	
920	def collect_list_certified_next(~Source: Data,~Element: Data,~Key: Data,~Context: Data,~Model: Data,
921	  ~Frame: Context -> Source -> Data,~ValueFrame: Context -> Element -> Data,
922	  ~observe: Context -> Element -> Model,~sample: Context -> Key -> Model,+context: Context,+key: Key,+rest: List<&2,Key>,
923	  head: Source & Element,tail: Source -> Source & List<&2,Element>,
924	  head_frame: collected_leaf_frame(~Source,~Element,~Key,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,key,head),
925	  tail_frame: @+source: Source -> Frame(context,source) -> collected_list_frame(~Source,~Element,~Key,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,rest,tail(source))) ->
926	  collected_list_frame(~Source,~Element,~Key,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,key <> rest,
927	    Traversal.collect_list_next(~&2,~Source,~Element,head,tail)):
928	  (+source,+value) = head
929	  Shape.Both{source_frame,Shape.Both{value_frame,+value_equal}} = head_frame
930	  collect_list_certified_join(~Source,~Element,~Key,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,key,rest,value,tail(source),value_frame,value_equal,tail_frame(source,source_frame))
931	
932	def collect_list_certified(~Source: Data,~Element: Data,~Key: Data,~Context: Data,~Model: Data,~ReadContext: Data,~project: Context -> ReadContext,
933	  ~Frame: Context -> Source -> Data,~ValueFrame: Context -> Element -> Data,~KeyFrame: Context -> Key -> Data,
934	  ~observe: Context -> Element -> Model,~sample: Context -> Key -> Model,
935	  ~read: Source -> ReadContext -> Key -> Source & Element,
936	  ~leaf: @+source: Source -> @+context: Context -> @+key: Key -> Frame(context,source) -> KeyFrame(context,key) ->
937	    collected_leaf_frame(~Source,~Element,~Key,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,key,read(source,project(context),key)),
938	  +keys: List<&2,Key>,+source: Source,+context: Context,source_frame: Frame(context,source),
939	  keys_frame: Members.All(Key,{key => KeyFrame(context,key) : Key -> Data},keys)) ->
940	  collected_list_frame(~Source,~Element,~Key,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,keys,
941	    Traversal.collect_list(~&2,~Source,~Element,~Key,~ReadContext,~read,keys,source,project(context))):
942	  match keys:
943	    case Nil{}: Shape.Both{source_frame,Shape.Both{Unit{},{==}}}
944	    case +key <> +rest:
945	      Shape.Both{head_frame,+tail_frame} = keys_frame
946	      collect_list_certified_next(~Source,~Element,~Key,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,key,rest,read(source,project(context),key),
947	        source => Traversal.collect_list(~&2,~Source,~Element,~Key,~ReadContext,~read,rest,source,project(context)),leaf(source,context,key,source_frame,head_frame),
948	        source => source_frame => collect_list_certified(~Source,~Element,~Key,~Context,~Model,~ReadContext,~project,~Frame,~ValueFrame,~KeyFrame,~observe,~sample,~read,~leaf,rest,source,context,source_frame,tail_frame))
949	
950	def collect_values_context_length(~ownership: Quant,~Runtime: Kind(ownership),~Model: Data,~Context: Data,~pack: Context -> Model -> Runtime,
951	  values: List<&2,Model>,+context: Context) ->
952	  {List.length(ownership,Runtime,collect_values_context(~ownership,~Runtime,~Model,~Context,~pack,values,context)) == List.length(&2,Model,values) : Nat}:
953	  match values:
954	    case Nil{}: {==}
955	    case head <> +rest:
956	      Equal.cong(Nat,Nat,value => 1n+value,List.length(ownership,Runtime,collect_values_context(~ownership,~Runtime,~Model,~Context,~pack,rest,context)),
957	        List.length(&2,Model,rest),collect_values_context_length(~ownership,~Runtime,~Model,~Context,~pack,rest,context))
958	
959	# A projected context exposes the logical index while the reader carries its
960	# own counters. The leaf proves the transition used by the common collector.
961	def collected_indexed_leaf_frame(~Source: Data,~Element: Data,~Context: Data,~Model: Data,~ReadContext: Data,~project: Context -> Nat -> ReadContext,
962	  ~Frame: Context -> Source -> Data,~ValueFrame: Context -> Element -> Data,
963	  ~observe: Context -> Element -> Model,~sample: Context -> Nat -> Model,+context: Context,+index: Nat,
964	  result: Source & Traversal.Collected<&2,ReadContext,Element>) -> Data:
965	  (+source,Traversal.Collected{next,+value}) = result
966	  Shape.Both<{next == project(context,1n+index) : ReadContext},
967	    collected_leaf_frame(~Source,~Element,~Nat,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,index,(source,value))>
968	
969	def collect_certified_next(~Source: Data,~Element: Data,~Context: Data,~Model: Data,~ReadContext: Data,~project: Context -> Nat -> ReadContext,
970	  ~Frame: Context -> Source -> Data,~ValueFrame: Context -> Element -> Data,
971	  ~observe: Context -> Element -> Model,~sample: Context -> Nat -> Model,+context: Context,+count: Nat,+index: Nat,
972	  head: Source & Traversal.Collected<&2,ReadContext,Element>,tail: Source -> ReadContext -> Source & List<&2,Element>,
973	  head_frame: collected_indexed_leaf_frame(~Source,~Element,~Context,~Model,~ReadContext,~project,~Frame,~ValueFrame,~observe,~sample,context,index,head),
974	  tail_frame: @+source: Source -> Frame(context,source) ->
975	    collected_list_frame(~Source,~Element,~Nat,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,Ranges.range(count,1n+index),tail(source,project(context,1n+index)))) ->
976	  collected_list_frame(~Source,~Element,~Nat,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,Ranges.range(1n+count,index),
977	    Traversal.collect_next(~&2,~Source,~Element,~ReadContext,head,tail)):
978	  (+source,Traversal.Collected{+next,+value}) = head
979	  Shape.Both{+next_equal,Shape.Both{source_frame,Shape.Both{value_frame,+value_equal}}} = head_frame
980	  %Equal.sym(ReadContext,next,project(context,1n+index),next_equal) :
981	    collected_list_frame(~Source,~Element,~Nat,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,Ranges.range(1n+count,index),
982	      Traversal.collect_prepend(~&2,~Source,~Element,value,tail(source,_)))
983	  collect_list_certified_join(~Source,~Element,~Nat,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,index,Ranges.range(count,1n+index),value,
984	    tail(source,project(context,1n+index)),value_frame,value_equal,tail_frame(source,source_frame))
985	
986	def collect_certified(~Source: Data,~Element: Data,~Context: Data,~Model: Data,~ReadContext: Data,~project: Context -> Nat -> ReadContext,
987	  ~Frame: Context -> Source -> Data,~ValueFrame: Context -> Element -> Data,~KeyFrame: Context -> Nat -> Data,
988	  ~observe: Context -> Element -> Model,~sample: Context -> Nat -> Model,
989	  ~read: Source -> ReadContext -> Source & Traversal.Collected<&2,ReadContext,Element>,
990	  ~leaf: @+source: Source -> @+context: Context -> @+index: Nat -> Frame(context,source) -> KeyFrame(context,index) ->
991	    collected_indexed_leaf_frame(~Source,~Element,~Context,~Model,~ReadContext,~project,~Frame,~ValueFrame,~observe,~sample,context,index,read(source,project(context,index))),
992	  +count: Nat,+index: Nat,+source: Source,+context: Context,source_frame: Frame(context,source),
993	  keys_frame: Members.All(Nat,{key => KeyFrame(context,key) : Nat -> Data},Ranges.range(count,index))) ->
994	  collected_list_frame(~Source,~Element,~Nat,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,Ranges.range(count,index),
995	    Traversal.collect(~&2,~Source,~Element,~ReadContext,~read,count,source,project(context,index))):
996	  match count:
997	    case 0n: Shape.Both{source_frame,Shape.Both{Unit{},{==}}}
998	    case 1n+ +rest:
999	      Shape.Both{head_frame,+tail_frame} = keys_frame
1000	      collect_certified_next(~Source,~Element,~Context,~Model,~ReadContext,~project,~Frame,~ValueFrame,~observe,~sample,context,rest,index,read(source,project(context,index)),
1001	        source => context => Traversal.collect(~&2,~Source,~Element,~ReadContext,~read,rest,source,context),leaf(source,context,index,source_frame,head_frame),
1002	        source => source_frame => collect_certified(~Source,~Element,~Context,~Model,~ReadContext,~project,~Frame,~ValueFrame,~KeyFrame,~observe,~sample,~read,~leaf,rest,1n+index,source,context,source_frame,tail_frame))
1003	
1004	def collect_values_context_range(~Element: Data,~Context: Data,~sample: Context -> Nat -> Element,
1005	  count: Nat,+first: Nat,+context: Context) ->
1006	  {collect_values_context(~&2,~Element,~Nat,~Context,~sample,Ranges.range(count,first),context) ==
1007	    ListRead.enumerate(~Element,~Context,~sample,count,first,context) : List<&2,Element>}:
1008	  match count:
1009	    case 0n: {==}
1010	    case 1n+ +rest:
1011	      Equal.cong(List<&2,Element>,List<&2,Element>,values => sample(context,first) <> values,
1012	        collect_values_context(~&2,~Element,~Nat,~Context,~sample,Ranges.range(rest,1n+first),context),
1013	        ListRead.enumerate(~Element,~Context,~sample,rest,1n+first,context),collect_values_context_range(~Element,~Context,~sample,rest,1n+first,context))
1014	
1015	def collect_next_length(~Source: Data,~Element: Data,~Context: Data,+count: Nat,
1016	  head: Source & Traversal.Collected<&2,Context,Element>,tail: Source -> Context -> Source & List<&2,Element>,
1017	  tail_length: @+source: Source -> @+context: Context -> {List.length(&2,Element,Pair.snd(Source,List<&2,Element>,tail(source,context))) == count : Nat}) ->
1018	  {List.length(&2,Element,Pair.snd(Source,List<&2,Element>,Traversal.collect_next(~&2,~Source,~Element,~Context,head,tail))) == 1n+count : Nat}:
1019	  (+source,Traversal.Collected{+context,+value}) = head
1020	  %Equal.sym(List<&2,Element>,Pair.snd(Source,List<&2,Element>,Traversal.collect_prepend(~&2,~Source,~Element,value,tail(source,context))),
1021	    value <> Pair.snd(Source,List<&2,Element>,tail(source,context)),collect_prepend_values(~Source,~Element,value,tail(source,context))) :
1022	    {List.length(&2,Element,_) == 1n+count : Nat}
1023	  Equal.cong(Nat,Nat,length => 1n+length,List.length(&2,Element,Pair.snd(Source,List<&2,Element>,tail(source,context))),count,tail_length(source,context))
1024	
1025	def collect_length(~Source: Data,~Element: Data,~Context: Data,
1026	  ~read: Source -> Context -> Source & Traversal.Collected<&2,Context,Element>,count: Nat,+source: Source,+context: Context) ->
1027	  {List.length(&2,Element,Pair.snd(Source,List<&2,Element>,Traversal.collect(~&2,~Source,~Element,~Context,~read,count,source,context))) == count : Nat}:
1028	  match count:
1029	    case 0n: {==}
1030	    case 1n+ +rest:
1031	      collect_next_length(~Source,~Element,~Context,rest,read(source,context),
1032	        source => context => Traversal.collect(~&2,~Source,~Element,~Context,~read,rest,source,context),
1033	        source => context => collect_length(~Source,~Element,~Context,~read,rest,source,context))
1034	
1035	# Pointwise equality on the visited keys preserves any collected value list.
1036	def collect_values_context_agrees(~Element: Data,~Key: Data,~LeftContext: Data,~RightContext: Data,
1037	  ~left: LeftContext -> Key -> Element,~right: RightContext -> Key -> Element,
1038	  +keys: List<&2,Key>,+left_context: LeftContext,+right_context: RightContext,
1039	  agreements: Members.All(Key,{key => {left(left_context,key) == right(right_context,key) : Element} : Key -> Data},keys)) ->
1040	  {collect_values_context(~&2,~Element,~Key,~LeftContext,~left,keys,left_context) ==
1041	    collect_values_context(~&2,~Element,~Key,~RightContext,~right,keys,right_context) : List<&2,Element>}:
1042	  match keys:
1043	    case Nil{}: {==}
1044	    case +key <> +rest:
1045	      Shape.Both{head,tail} = agreements
1046	      %Equal.sym(Element,left(left_context,key),right(right_context,key),head) :
1047	        {_ <> collect_values_context(~&2,~Element,~Key,~LeftContext,~left,rest,left_context) ==
1048	          right(right_context,key) <> collect_values_context(~&2,~Element,~Key,~RightContext,~right,rest,right_context) : List<&2,Element>}
1049	      Equal.cong(List<&2,Element>,List<&2,Element>,values => right(right_context,key) <> values,
1050	        collect_values_context(~&2,~Element,~Key,~LeftContext,~left,rest,left_context),
1051	        collect_values_context(~&2,~Element,~Key,~RightContext,~right,rest,right_context),
1052	        collect_values_context_agrees(~Element,~Key,~LeftContext,~RightContext,~left,~right,rest,left_context,right_context,tail))
1053	
1054	# A fixed context condition is carried unchanged while its fold is projected.
1055	def indexed_fold_change_context_under(~State: Data,~Outer: Data,~Inner: Data,
1056	  ~project: Outer -> Inner,~Condition: Outer -> Data,
1057	  ~outer_step: U32 -> Outer -> State -> State,~inner_step: U32 -> Inner -> State -> State,
1058	  ~same_step: @+index: U32 -> @+context: Outer -> @+state: State -> Condition(context) ->
1059	    {outer_step(index,context,state) == inner_step(index,project(context),state) : State},
1060	  count: Nat,+first: U32,+context: Outer,+state: State,+condition: Condition(context)) ->
1061	  {Traversal.indexed_fold(~State,~Outer,~outer_step,count,first,context,state) ==
1062	    Traversal.indexed_fold(~State,~Inner,~inner_step,count,first,project(context),state) : State}:
1063	  match count:
1064	    case 0n: {==}
1065	    case 1n+rest:
1066	      %Equal.sym(State,outer_step(first,context,state),inner_step(first,project(context),state),same_step(first,context,state,condition)) :
1067	        {Traversal.indexed_fold(~State,~Outer,~outer_step,rest,(first + 1 : U32),context,_) ==
1068	          Traversal.indexed_fold(~State,~Inner,~inner_step,rest,(first + 1 : U32),project(context),inner_step(first,project(context),state)) : State}
1069	      indexed_fold_change_context_under(~State,~Outer,~Inner,~project,~Condition,~outer_step,~inner_step,~same_step,rest,(first + 1 : U32),context,inner_step(first,project(context),state),condition)