proofs/traversal_array_refinement.bend

stelliferous@0.0.2.0 · 317 lines · 24 definitions

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.
3import Base
4import stelliferous@0.0.2.0/kernel_block.bend as Block
5import stelliferous@0.0.2.0/traversal_array.bend as Traversal
6import stelliferous@0.0.2.0/traversal_loop.bend as Loop
7import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
8import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageLaws
9import stelliferous@0.0.2.0/proofs/loop_projection.bend as Projection
10import stelliferous@0.0.2.0/proofs/natural_addition.bend as Addition
11import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as Bounds
12import stelliferous@0.0.2.0/proofs/nat_order.bend as Order
13
14def represent(~Reader: Type,~Model: Data,~Element: Data,~Context: Data,~pack_reader: Model -> Reader,
15  state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) -> Traversal.State<&1,&1,Reader,Array<Element>,Context>:
16  Traversal.State{reader,output,position,context} = state
17  Traversal.State{pack_reader(reader),Tree.pack(Element,output),position,context}
18
19def model_step(~Model: Data,~Element: Data,~Context: Data,
20  ~sample: Model -> Context -> U32 -> Element,~destination: Context -> U32 -> U32,
21  state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) -> Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>:
22  Traversal.State{+reader,output,+position,+context} = state
23  Traversal.State{reader,Tree.write(Element,output,destination(context,position),sample(reader,context,position)),(position + 1 : U32),context}
24
25def step_refines_model(~Reader: Type,~Model: Data,~Element: Data,~Context: Data,
26  ~pack_reader: Model -> Reader,~read: Reader -> Context -> U32 -> Reader & Element,
27  ~sample: Model -> Context -> U32 -> Element,~destination: Context -> U32 -> U32,
28  ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
29    {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
30  +state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) ->
31  {Traversal.step(~Reader,~Element,~Context,~read,~destination,represent(~Reader,~Model,~Element,~Context,~pack_reader,state)) ==
32    represent(~Reader,~Model,~Element,~Context,~pack_reader,model_step(~Model,~Element,~Context,~sample,~destination,state)) :
33    Traversal.State<&1,&1,Reader,Array<Element>,Context>}:
34  Traversal.State{+reader,+output,+position,+context} = state
35  %Equal.sym(Reader & Element,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),read_matches(reader,context,position)) :
36    {Traversal.store(~Reader,~Element,~Context,~destination,position,context,Tree.pack(Element,output),_) ==
37      represent(~Reader,~Model,~Element,~Context,~pack_reader,model_step(~Model,~Element,~Context,~sample,~destination,
38        Traversal.State{reader,output,position,context})) : Traversal.State<&1,&1,Reader,Array<Element>,Context>}
39  %Equal.sym(Array<Element>,Array.set(Element,Tree.pack(Element,output),destination(context,position),sample(reader,context,position)),
40    Tree.pack(Element,Tree.write(Element,output,destination(context,position),sample(reader,context,position))),
41    StorageLaws.write(Element,output,destination(context,position),sample(reader,context,position))) :
42    {Traversal.State{pack_reader(reader),_,(position + 1 : U32),context} ==
43      represent(~Reader,~Model,~Element,~Context,~pack_reader,model_step(~Model,~Element,~Context,~sample,~destination,
44        Traversal.State{reader,output,position,context})) : Traversal.State<&1,&1,Reader,Array<Element>,Context>}
45  {==}
46
47def traversal_refines_model(~Reader: Type,~Model: Data,~Element: Data,~Context: Data,
48  ~pack_reader: Model -> Reader,~read: Reader -> Context -> U32 -> Reader & Element,
49  ~sample: Model -> Context -> U32 -> Element,~destination: Context -> U32 -> U32,
50  ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
51    {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
52  +count: Nat,+state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) ->
53  {Traversal.run(~Reader,~Element,~Context,~read,~destination,count,represent(~Reader,~Model,~Element,~Context,~pack_reader,state)) ==
54    represent(~Reader,~Model,~Element,~Context,~pack_reader,
55      Loop.run(~Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>,~model_step(~Model,~Element,~Context,~sample,~destination),count,state)) :
56    Traversal.State<&1,&1,Reader,Array<Element>,Context>}:
57  Projection.iteration_refines_model(~Traversal.State<&1,&1,Reader,Array<Element>,Context>,~Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>,
58    ~Traversal.step(~Reader,~Element,~Context,~read,~destination),~model_step(~Model,~Element,~Context,~sample,~destination),
59    ~represent(~Reader,~Model,~Element,~Context,~pack_reader),~step_refines_model(~Reader,~Model,~Element,~Context,~pack_reader,~read,~sample,~destination,~read_matches),count,state)
60# Concrete copy/zip readers discharge the generic traversal's only read premise.
61
62def pack_tree(~Element: Data,tree: Tree.Tree<Element>) -> Array<Element>:
63  Tree.pack(Element,tree)
64
65def sample_offset(~Element: Data,tree: Tree.Tree<Element>,context: Traversal.Offsets,position: U32) -> Element:
66  Traversal.Offsets{source,destination} = context
67  Tree.read(Element,tree,(source + position : U32))
68
69def offset_read_refines_storage(~Element: Data,+tree: Tree.Tree<Element>,+context: Traversal.Offsets,+position: U32) ->
70  {Traversal.source_offset(~Element,pack_tree(~Element,tree),context,position) ==
71    (pack_tree(~Element,tree),sample_offset(~Element,tree,context,position)) : Array<Element> & Element}:
72  Traversal.Offsets{source,destination} = context
73  StorageLaws.read(Element,tree,(source + position : U32))
74
75def copy_traversal_refines_storage(~Element: Data,+count: Nat,
76  +state: Traversal.State<&2,&2,Tree.Tree<Element>,Tree.Tree<Element>,Traversal.Offsets>) ->
77  {Traversal.run(~Array<Element>,~Element,~Traversal.Offsets,~Traversal.source_offset(~Element),~Traversal.destination_offset,count,
78      represent(~Array<Element>,~Tree.Tree<Element>,~Element,~Traversal.Offsets,~pack_tree(~Element),state)) ==
79    represent(~Array<Element>,~Tree.Tree<Element>,~Element,~Traversal.Offsets,~pack_tree(~Element),
80      Loop.run(~Traversal.State<&2,&2,Tree.Tree<Element>,Tree.Tree<Element>,Traversal.Offsets>,
81        ~model_step(~Tree.Tree<Element>,~Element,~Traversal.Offsets,~sample_offset(~Element),~Traversal.destination_offset),count,state)) :
82    Traversal.State<&1,&1,Array<Element>,Array<Element>,Traversal.Offsets>}:
83  traversal_refines_model(~Array<Element>,~Tree.Tree<Element>,~Element,~Traversal.Offsets,~pack_tree(~Element),
84    ~Traversal.source_offset(~Element),~sample_offset(~Element),~Traversal.destination_offset,~offset_read_refines_storage(~Element),count,state)
85
86# The accumulator is an observation, independent of its numeric interpretation.
87# In particular this theorem never rewrites or reassociates a floating sum.
88def represent_fold(~Reader: Type,~Model: Data,~Accumulator: Data,~Context: Data,~pack_reader: Model -> Reader,
89  state: Traversal.State<&2,&2,Model,Accumulator,Context>) -> Traversal.State<&1,&2,Reader,Accumulator,Context>:
90  Traversal.State{reader,accumulator,position,context} = state
91  Traversal.State{pack_reader(reader),accumulator,position,context}
92
93def model_fold_step(~Model: Data,~Element: Data,~Accumulator: Data,~Context: Data,
94  ~sample: Model -> Context -> U32 -> Element,~combine: Accumulator -> Element -> Accumulator,
95  state: Traversal.State<&2,&2,Model,Accumulator,Context>) -> Traversal.State<&2,&2,Model,Accumulator,Context>:
96  Traversal.State{+reader,accumulator,+position,+context} = state
97  Traversal.State{reader,combine(accumulator,sample(reader,context,position)),(position + 1 : U32),context}
98
99def fold_step_refines_model(~Reader: Type,~Model: Data,~Element: Data,~Accumulator: Data,~Context: Data,
100  ~pack_reader: Model -> Reader,~read: Reader -> Context -> U32 -> Reader & Element,
101  ~sample: Model -> Context -> U32 -> Element,~combine: Accumulator -> Element -> Accumulator,
102  ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
103    {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
104  +state: Traversal.State<&2,&2,Model,Accumulator,Context>) ->
105  {Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine,
106      represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,state)) ==
107    represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,
108      model_fold_step(~Model,~Element,~Accumulator,~Context,~sample,~combine,state)) : Traversal.State<&1,&2,Reader,Accumulator,Context>}:
109  Traversal.State{+reader,+accumulator,+position,+context} = state
110  %Equal.sym(Reader & Element,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),
111    read_matches(reader,context,position)) :
112    {Traversal.fold_value(~Reader,~Element,~Accumulator,~Context,~combine,accumulator,position,context,_) ==
113      represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,
114        model_fold_step(~Model,~Element,~Accumulator,~Context,~sample,~combine,Traversal.State{reader,accumulator,position,context})) :
115      Traversal.State<&1,&2,Reader,Accumulator,Context>}
116  {==}
117
118def fold_refines_ordered_model(~Reader: Type,~Model: Data,~Element: Data,~Accumulator: Data,~Context: Data,
119  ~pack_reader: Model -> Reader,~read: Reader -> Context -> U32 -> Reader & Element,
120  ~sample: Model -> Context -> U32 -> Element,~combine: Accumulator -> Element -> Accumulator,
121  ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
122    {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
123  +count: Nat,+state: Traversal.State<&2,&2,Model,Accumulator,Context>) ->
124  {Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine),
125      count,represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,state)) ==
126    represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,
127      Loop.run(~Traversal.State<&2,&2,Model,Accumulator,Context>,~model_fold_step(~Model,~Element,~Accumulator,~Context,~sample,~combine),count,state)) :
128    Traversal.State<&1,&2,Reader,Accumulator,Context>}:
129  Projection.iteration_refines_model(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.State<&2,&2,Model,Accumulator,Context>,
130    ~Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine),~model_fold_step(~Model,~Element,~Accumulator,~Context,~sample,~combine),
131    ~represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader),
132    ~fold_step_refines_model(~Reader,~Model,~Element,~Accumulator,~Context,~pack_reader,~read,~sample,~combine,~read_matches),count,state)
133
134# In-place transforms retain one owner and use the same generic loop lifting.
135def represent_map(~Element: Data,~Context: Data,
136  state: Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>) -> Traversal.State<&2,&1,Unit,Array<Element>,Context>:
137  Traversal.State{Unit{},output,position,context} = state
138  Traversal.State{Unit{},Tree.pack(Element,output),position,context}
139
140def unindexed(~Element: Data,~Context: Data,~map: Context -> Element -> Element,context: Context,position: U32,value: Element) -> Element:
141  map(context,value)
142
143def model_map_step(~Element: Data,~Context: Data,~map: Context -> U32 -> Element -> Element,
144  state: Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>) -> Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>:
145  Traversal.State{Unit{},+output,+position,+context} = state
146  Traversal.State{Unit{},Tree.write(Element,output,position,map(context,position,Tree.read(Element,output,position))),
147    (position + 1 : U32),context}
148
149def map_step_refines_model(~Element: Data,~Context: Data,~map: Context -> Element -> Element,
150  +state: Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>) ->
151  {Traversal.map_step(~Element,~Context,~map,represent_map(~Element,~Context,state)) ==
152    represent_map(~Element,~Context,model_map_step(~Element,~Context,~unindexed(~Element,~Context,~map),state)) : Traversal.State<&2,&1,Unit,Array<Element>,Context>}:
153  Traversal.State{Unit{},+output,+position,+context} = state
154  %Equal.sym(Array<Element> & Element,Array.get(Element,Tree.pack(Element,output),position),
155    (Tree.pack(Element,output),Tree.read(Element,output,position)),StorageLaws.read(Element,output,position)) :
156    {Traversal.mapped_value(~Element,~Context,~map,position,context,_) ==
157      represent_map(~Element,~Context,model_map_step(~Element,~Context,~unindexed(~Element,~Context,~map),state)) : Traversal.State<&2,&1,Unit,Array<Element>,Context>}
158  %Equal.sym(Array<Element>,Array.set(Element,Tree.pack(Element,output),position,map(context,Tree.read(Element,output,position))),
159    Tree.pack(Element,Tree.write(Element,output,position,map(context,Tree.read(Element,output,position)))),
160    StorageLaws.write(Element,output,position,map(context,Tree.read(Element,output,position)))) :
161    {Traversal.State{Unit{},_,(position + 1 : U32),context} ==
162      represent_map(~Element,~Context,model_map_step(~Element,~Context,~unindexed(~Element,~Context,~map),state)) : Traversal.State<&2,&1,Unit,Array<Element>,Context>}
163  {==}
164
165def map_loop_refines_model(~Element: Data,~Context: Data,~map: Context -> Element -> Element,
166  +count: Nat,+state: Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>) ->
167  {Loop.run(~Traversal.State<&2,&1,Unit,Array<Element>,Context>,~Traversal.map_step(~Element,~Context,~map),
168      count,represent_map(~Element,~Context,state)) ==
169    represent_map(~Element,~Context,Loop.run(~Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>,
170      ~model_map_step(~Element,~Context,~unindexed(~Element,~Context,~map)),count,state)) : Traversal.State<&2,&1,Unit,Array<Element>,Context>}:
171  Projection.iteration_refines_model(~Traversal.State<&2,&1,Unit,Array<Element>,Context>,~Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>,
172    ~Traversal.map_step(~Element,~Context,~map),~model_map_step(~Element,~Context,~unindexed(~Element,~Context,~map)),~represent_map(~Element,~Context),
173    ~map_step_refines_model(~Element,~Context,~map),count,state)
174
175# One representation proof covers the entire indexed output traversal. The
176# strategy supplies a single-step result, not another outer-loop induction.
177
178# In-place binary updates use the current destination value in left position.
179# This theorem models sequential writes, including modular/overlapping raw
180# addresses. Valid view guards and non-overlap are separate obligations.
181def model_update_step(~Model: Data,~Element: Data,~Sample: Data,~Context: Data,
182  ~sample: Model -> Context -> U32 -> Sample,~combine: Element -> Sample -> Element,~destination: Context -> U32 -> U32,
183  state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) -> Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>:
184  Traversal.State{+reader,+output,+position,+context} = state
185  Traversal.State{reader,Tree.write(Element,output,destination(context,position),
186    combine(Tree.read(Element,output,destination(context,position)),sample(reader,context,position))),(position + 1 : U32),context}
187
188def update_step_refines_model(~Reader: Type,~Model: Data,~Element: Data,~Sample: Data,~Context: Data,
189  ~pack_reader: Model -> Reader,~read: Reader -> Context -> U32 -> Reader & Sample,
190  ~sample: Model -> Context -> U32 -> Sample,~combine: Element -> Sample -> Element,~destination: Context -> U32 -> U32,
191  ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
192    {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Sample},
193  +state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) ->
194  {Traversal.update_step(~Reader,~Element,~Sample,~Context,~read,~combine,~destination,
195      represent(~Reader,~Model,~Element,~Context,~pack_reader,state)) ==
196    represent(~Reader,~Model,~Element,~Context,~pack_reader,model_update_step(~Model,~Element,~Sample,~Context,~sample,~combine,~destination,state)) :
197    Traversal.State<&1,&1,Reader,Array<Element>,Context>}:
198  Traversal.State{+reader,+output,+position,+context} = state
199  %Equal.sym(Array<Element> & Element,Array.get(Element,Tree.pack(Element,output),destination(context,position)),
200    (Tree.pack(Element,output),Tree.read(Element,output,destination(context,position))),StorageLaws.read(Element,output,destination(context,position))) :
201    {Traversal.update_current(~Reader,~Element,~Sample,~Context,~read,~combine,~destination,pack_reader(reader),position,context,_) ==
202      represent(~Reader,~Model,~Element,~Context,~pack_reader,model_update_step(~Model,~Element,~Sample,~Context,~sample,~combine,~destination,
203        Traversal.State{reader,output,position,context})) : Traversal.State<&1,&1,Reader,Array<Element>,Context>}
204  %Equal.sym(Reader & Sample,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),read_matches(reader,context,position)) :
205    {Traversal.update_sample(~Reader,~Element,~Sample,~Context,~combine,~destination,position,context,Tree.pack(Element,output),
206      Tree.read(Element,output,destination(context,position)),_) ==
207      represent(~Reader,~Model,~Element,~Context,~pack_reader,model_update_step(~Model,~Element,~Sample,~Context,~sample,~combine,~destination,
208        Traversal.State{reader,output,position,context})) : Traversal.State<&1,&1,Reader,Array<Element>,Context>}
209  %Equal.sym(Array<Element>,Array.set(Element,Tree.pack(Element,output),destination(context,position),
210      combine(Tree.read(Element,output,destination(context,position)),sample(reader,context,position))),
211    Tree.pack(Element,Tree.write(Element,output,destination(context,position),
212      combine(Tree.read(Element,output,destination(context,position)),sample(reader,context,position)))),
213    StorageLaws.write(Element,output,destination(context,position),combine(Tree.read(Element,output,destination(context,position)),sample(reader,context,position)))) :
214    {Traversal.State{pack_reader(reader),_,(position + 1 : U32),context} ==
215      represent(~Reader,~Model,~Element,~Context,~pack_reader,model_update_step(~Model,~Element,~Sample,~Context,~sample,~combine,~destination,
216        Traversal.State{reader,output,position,context})) : Traversal.State<&1,&1,Reader,Array<Element>,Context>}
217  {==}
218
219def update_refines_model(~Reader: Type,~Model: Data,~Element: Data,~Sample: Data,~Context: Data,
220  ~pack_reader: Model -> Reader,~read: Reader -> Context -> U32 -> Reader & Sample,
221  ~sample: Model -> Context -> U32 -> Sample,~combine: Element -> Sample -> Element,~destination: Context -> U32 -> U32,
222  ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
223    {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Sample},
224  +count: Nat,+state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) ->
225  {Traversal.update(~Reader,~Element,~Sample,~Context,~read,~combine,~destination,count,
226      represent(~Reader,~Model,~Element,~Context,~pack_reader,state)) ==
227    represent(~Reader,~Model,~Element,~Context,~pack_reader,
228      Loop.run(~Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>,
229        ~model_update_step(~Model,~Element,~Sample,~Context,~sample,~combine,~destination),count,state)) :
230    Traversal.State<&1,&1,Reader,Array<Element>,Context>}:
231  Projection.iteration_refines_model(~Traversal.State<&1,&1,Reader,Array<Element>,Context>,~Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>,
232    ~Traversal.update_step(~Reader,~Element,~Sample,~Context,~read,~combine,~destination),
233    ~model_update_step(~Model,~Element,~Sample,~Context,~sample,~combine,~destination),
234    ~represent(~Reader,~Model,~Element,~Context,~pack_reader),
235    ~update_step_refines_model(~Reader,~Model,~Element,~Sample,~Context,~pack_reader,~read,~sample,~combine,~destination,~read_matches),count,state)
236
237def indexed_fold_refines_model(~Runtime: Type,~Model: Data,~Context: Data,
238  ~update: U32 -> Context -> Runtime -> Runtime,~model_update: U32 -> Context -> Model -> Model,
239  ~represent: Model -> Runtime,
240  ~step_matches: @+index: U32 -> @+context: Context -> @+state: Model ->
241    {update(index,context,represent(state)) == represent(model_update(index,context,state)) : Runtime},
242  +count: Nat,+index: U32,+context: Context,+state: Model) ->
243  {Traversal.indexed_fold(~Runtime,~Context,~update,count,index,context,represent(state)) ==
244    represent(Traversal.indexed_fold(~Model,~Context,~model_update,count,index,context,state)) : Runtime}:
245  match count:
246    case 0n: {==}
247    case 1n+ +rest:
248      %Equal.sym(Runtime,update(index,context,represent(state)),represent(model_update(index,context,state)),step_matches(index,context,state)) :
249        {Traversal.indexed_fold(~Runtime,~Context,~update,rest,(index + 1 : U32),context,_) ==
250          represent(Traversal.indexed_fold(~Model,~Context,~model_update,rest,(index + 1 : U32),context,model_update(index,context,state))) : Runtime}
251      indexed_fold_refines_model(~Runtime,~Model,~Context,~update,~model_update,~represent,~step_matches,
252        rest,(index + 1 : U32),context,model_update(index,context,state))
253
254# One bounded induction carries capacity, preserved sources and completed
255# output values together. A strategy proves its local update obligation;
256# it does not reimplement the whole output traversal proof.
257def indexed_fold_change_context(~State: Data,~Outer: Data,~Inner: Data,
258  ~project: Outer -> Inner,~outer_step: U32 -> Outer -> State -> State,~inner_step: U32 -> Inner -> State -> State,
259  ~same_step: @+index: U32 -> @+context: Outer -> @+state: State ->
260    {outer_step(index,context,state) == inner_step(index,project(context),state) : State},
261  +count: Nat,+first: U32,+context: Outer,+state: State) ->
262  {Traversal.indexed_fold(~State,~Outer,~outer_step,count,first,context,state) ==
263    Traversal.indexed_fold(~State,~Inner,~inner_step,count,first,project(context),state) : State}:
264  match count:
265    case 0n: {==}
266    case 1n+ +rest:
267      %Equal.sym(State,outer_step(first,context,state),inner_step(first,project(context),state),same_step(first,context,state)) :
268        {Traversal.indexed_fold(~State,~Outer,~outer_step,rest,(first + 1 : U32),context,_) ==
269          Traversal.indexed_fold(~State,~Inner,~inner_step,rest,(first + 1 : U32),project(context),inner_step(first,project(context),state)) : State}
270      indexed_fold_change_context(~State,~Outer,~Inner,~project,~outer_step,~inner_step,~same_step,
271        rest,(first + 1 : U32),context,inner_step(first,project(context),state))
272
273def indexed_fold_preserves_invariant(~State: Data,~Context: Data,
274  ~limit: Context -> Nat,~Invariant: Context -> Nat -> State -> Data,
275  ~update: U32 -> Context -> State -> State,
276  ~preserve: @+context: Context -> @+index: Nat -> @+state: State ->
277    {Nat.is_lt(index,limit(context)) == True{} : Bool} -> Invariant(context,index,state) ->
278    Invariant(context,1n+index,update(U32.from_nat(index),context,state)),
279  +count: Nat,+first: Nat,+context: Context,+state: State,
280  +room: {Nat.is_le(Nat.add(first,count),limit(context)) == True{} : Bool},
281  evidence: Invariant(context,first,state)) ->
282  Invariant(context,Nat.add(first,count),Traversal.indexed_fold(~State,~Context,~update,count,U32.from_nat(first),context,state)):
283  match count:
284    case 0n:
285      %Equal.sym(Nat,Nat.add(first,0n),first,Addition.zero_right(first)) : Invariant(context,_,state)
286      evidence
287    case 1n+ +rest:
288      %Equal.sym(U32,(U32.from_nat(first) + 1 : U32),U32.from_nat(1n+first),Bounds.add_one(U32.from_nat(first))) :
289        Invariant(context,Nat.add(first,1n+rest),Traversal.indexed_fold(~State,~Context,~update,rest,_,context,update(U32.from_nat(first),context,state)))
290      %Equal.sym(Nat,Nat.add(first,1n+rest),1n+Nat.add(first,rest),Addition.successor_right(first,rest)) :
291        Invariant(context,_,Traversal.indexed_fold(~State,~Context,~update,rest,U32.from_nat(1n+first),context,update(U32.from_nat(first),context,state)))
292      indexed_fold_preserves_invariant(~State,~Context,~limit,~Invariant,~update,~preserve,rest,1n+first,context,update(U32.from_nat(first),context,state),
293        Order.advance_room(first,rest,limit(context),room),preserve(context,first,state,Order.room_index(first,rest,limit(context),room),evidence))
294
295# Splitting a traversal preserves every state update in the same order. The
296# boundary uses modular U32 conversion; no scalar/FP32-specific induction.
297def indexed_fold_split(~Value: Type,~Context: Data,~update: U32 -> Context -> Value -> Value,
298  +first: Nat,+second: Nat,+start: Nat,+context: Context,-initial: Value) ->
299  {Traversal.indexed_fold(~Value,~Context,~update,Nat.add(first,second),U32.from_nat(start),context,initial) ==
300    Traversal.indexed_fold(~Value,~Context,~update,second,U32.from_nat(Nat.add(start,first)),context,
301      Traversal.indexed_fold(~Value,~Context,~update,first,U32.from_nat(start),context,initial)) : Value}:
302  match first:
303    case 0n:
304      %Equal.sym(Nat,Nat.add(start,0n),start,Addition.zero_right(start)) :
305        {Traversal.indexed_fold(~Value,~Context,~update,second,U32.from_nat(start),context,initial) ==
306          Traversal.indexed_fold(~Value,~Context,~update,second,U32.from_nat(_),context,initial) : Value}
307      {==}
308    case 1n+ +rest:
309      %Equal.sym(U32,(U32.from_nat(start) + 1 : U32),U32.from_nat(1n+start),Bounds.add_one(U32.from_nat(start))) :
310        {Traversal.indexed_fold(~Value,~Context,~update,Nat.add(rest,second),_,context,update(U32.from_nat(start),context,initial)) ==
311          Traversal.indexed_fold(~Value,~Context,~update,second,U32.from_nat(Nat.add(start,1n+rest)),context,
312            Traversal.indexed_fold(~Value,~Context,~update,rest,_,context,update(U32.from_nat(start),context,initial))) : Value}
313      %Equal.sym(Nat,Nat.add(start,1n+rest),1n+Nat.add(start,rest),Addition.successor_right(start,rest)) :
314        {Traversal.indexed_fold(~Value,~Context,~update,Nat.add(rest,second),U32.from_nat(1n+start),context,update(U32.from_nat(start),context,initial)) ==
315          Traversal.indexed_fold(~Value,~Context,~update,second,U32.from_nat(_),context,
316            Traversal.indexed_fold(~Value,~Context,~update,rest,U32.from_nat(1n+start),context,update(U32.from_nat(start),context,initial))) : Value}
317      indexed_fold_split(~Value,~Context,~update,rest,second,1n+start,context,update(U32.from_nat(start),context,initial))