proofs/traversal_batch_refinement.bend
stelliferous@0.0.3.0 · 242 lines · 0 definitions
1# A batch writes the mapped values of consecutive positions after reading all
2# of them from the original tree. Inside the tree it is the ordered in-place
3# map of the same positions: no step of that map reads a position an earlier
4# step wrote. For every element type and every batch length.
5import Base
6import stelliferous@0.0.3.0/traversal_array.bend as Traversal
7import stelliferous@0.0.3.0/traversal_loop.bend as Loop
8import stelliferous@0.0.3.0/proofs/traversal_array_refinement.bend as ArrayLaws
9import stelliferous@0.0.3.0/proofs/traversal_map_readback.bend as MapReadback
10import stelliferous@0.0.3.0/proofs/storage_tree_model.bend as Tree
11import stelliferous@0.0.3.0/proofs/storage_shape.bend as Shape
12import stelliferous@0.0.3.0/proofs/nat_to_u32_bounds.bend as Bounds
13import stelliferous@0.0.3.0/proofs/nat_order.bend as Order
14import stelliferous@0.0.3.0/proofs/natural_addition.bend as Addition
15import stelliferous@0.0.3.0/proofs/nat_interval.bend as Interval
16import stelliferous@0.0.3.0/proofs/loop_projection.bend as Projection
17import stelliferous@0.0.3.0/proofs/row_major_index.bend as RowMajor
18
19def batch(~Element: Data,~Context: Data,~map: Context -> U32 -> Element -> Element,count: Nat,+position: U32,+context: Context,+source: Tree.Tree<Element>,
20 target: Tree.Tree<Element>) -> Tree.Tree<Element>:
21 match count:
22 case 0n: target
23 case 1n+rest:
24 batch(~Element,~Context,~map,rest,(position + 1 : U32),context,source,Tree.write(Element,target,position,map(context,position,Tree.read(Element,source,position))))
25
26def ModelState(~Element: Data,~Context: Data) -> Data:
27 Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>
28
29# A loop's last step, for every state and count.
30def last_step(~State: Data,~step: State -> State,+count: Nat,+state: State) ->
31 {Loop.run(~State,~step,1n+count,state) == step(Loop.run(~State,~step,count,state)) : State}:
32 match count:
33 case 0n: {==}
34 case 1n+ +rest: last_step(~State,~step,rest,step(state))
35
36# The whole state after count steps of the model map.
37def state_after(~Element: Data,~Context: Data,~map: Context -> U32 -> Element -> Element,+count: Nat,+start: Nat,+context: Context,+input: Tree.Tree<Element>) ->
38 {Loop.run(~ModelState(~Element,~Context),~ArrayLaws.model_map_step(~Element,~Context,~map),count,Traversal.State{Unit{},input,U32.from_nat(start),context}) ==
39 Traversal.State{Unit{},MapReadback.run_indexed(~Element,~Context,~map,count,U32.from_nat(start),context,input),U32.from_nat(Nat.add(start,count)),context} :
40 ModelState(~Element,~Context)}:
41 match count:
42 case 0n:
43 %Equal.sym(Nat,Nat.add(start,0n),start,Addition.zero_right(start)) :
44 {Traversal.State{Unit{},input,U32.from_nat(start),context} == Traversal.State{Unit{},input,U32.from_nat(_),context} : ModelState(~Element,~Context)}
45 {==}
46 case 1n+ +rest:
47 +written = Tree.write(Element,input,U32.from_nat(start),map(context,U32.from_nat(start),Tree.read(Element,input,U32.from_nat(start))))
48 %Equal.sym(Nat,Nat.add(start,1n+rest),1n+Nat.add(start,rest),Addition.successor_right(start,rest)) :
49 {Loop.run(~ModelState(~Element,~Context),~ArrayLaws.model_map_step(~Element,~Context,~map),rest,Traversal.State{Unit{},written,(U32.from_nat(start) + 1 : U32),context}) ==
50 Traversal.State{Unit{},MapReadback.run_indexed(~Element,~Context,~map,rest,(U32.from_nat(start) + 1 : U32),context,written),U32.from_nat(_),context} : ModelState(~Element,~Context)}
51 %Equal.sym(U32,(U32.from_nat(start) + 1 : U32),U32.from_nat(1n+start),Bounds.add_one(U32.from_nat(start))) :
52 {Loop.run(~ModelState(~Element,~Context),~ArrayLaws.model_map_step(~Element,~Context,~map),rest,Traversal.State{Unit{},written,_,context}) ==
53 Traversal.State{Unit{},MapReadback.run_indexed(~Element,~Context,~map,rest,_,context,written),U32.from_nat(1n+Nat.add(start,rest)),context} : ModelState(~Element,~Context)}
54 state_after(~Element,~Context,~map,rest,1n+start,context,written)
55
56# One more step of the model map writes the position after the ones it mapped.
57def map_split(~Element: Data,~Context: Data,~map: Context -> U32 -> Element -> Element,+first: Nat,+second: Nat,+start: Nat,+context: Context,+input: Tree.Tree<Element>) ->
58 {MapReadback.run_indexed(~Element,~Context,~map,Nat.add(first,second),U32.from_nat(start),context,input) ==
59 MapReadback.run_indexed(~Element,~Context,~map,second,U32.from_nat(Nat.add(start,first)),context,MapReadback.run_indexed(~Element,~Context,~map,first,U32.from_nat(start),context,input)) : Tree.Tree<Element>}:
60 +initial = {Traversal.State{Unit{},input,U32.from_nat(start),context} : ModelState(~Element,~Context)}
61 %Equal.sym(ModelState(~Element,~Context),Loop.run(~ModelState(~Element,~Context),~ArrayLaws.model_map_step(~Element,~Context,~map),Nat.add(first,second),initial),
62 Loop.run(~ModelState(~Element,~Context),~ArrayLaws.model_map_step(~Element,~Context,~map),second,Loop.run(~ModelState(~Element,~Context),~ArrayLaws.model_map_step(~Element,~Context,~map),first,initial)),
63 Projection.iteration_split(~ModelState(~Element,~Context),~ArrayLaws.model_map_step(~Element,~Context,~map),first,second,initial)) :
64 {MapReadback.output(~Element,~Context,_) == MapReadback.run_indexed(~Element,~Context,~map,second,U32.from_nat(Nat.add(start,first)),context,MapReadback.run_indexed(~Element,~Context,~map,first,U32.from_nat(start),context,input)) : Tree.Tree<Element>}
65 %Equal.sym(ModelState(~Element,~Context),Loop.run(~ModelState(~Element,~Context),~ArrayLaws.model_map_step(~Element,~Context,~map),first,initial),
66 Traversal.State{Unit{},MapReadback.run_indexed(~Element,~Context,~map,first,U32.from_nat(start),context,input),U32.from_nat(Nat.add(start,first)),context},state_after(~Element,~Context,~map,first,start,context,input)) :
67 {MapReadback.output(~Element,~Context,Loop.run(~ModelState(~Element,~Context),~ArrayLaws.model_map_step(~Element,~Context,~map),second,_)) == MapReadback.run_indexed(~Element,~Context,~map,second,U32.from_nat(Nat.add(start,first)),context,MapReadback.run_indexed(~Element,~Context,~map,first,U32.from_nat(start),context,input)) : Tree.Tree<Element>}
68 {==}
69
70def extended(~Element: Data,~Context: Data,~map: Context -> U32 -> Element -> Element,+done: Nat,+start: Nat,+context: Context,+input: Tree.Tree<Element>) ->
71 {MapReadback.run_indexed(~Element,~Context,~map,1n+done,U32.from_nat(start),context,input) ==
72 Tree.write(Element,MapReadback.run_indexed(~Element,~Context,~map,done,U32.from_nat(start),context,input),U32.from_nat(Nat.add(start,done)),
73 map(context,U32.from_nat(Nat.add(start,done)),Tree.read(Element,MapReadback.run_indexed(~Element,~Context,~map,done,U32.from_nat(start),context,input),U32.from_nat(Nat.add(start,done))))) : Tree.Tree<Element>}:
74 +initial = {Traversal.State{Unit{},input,U32.from_nat(start),context} : ModelState(~Element,~Context)}
75 %Equal.sym(ModelState(~Element,~Context),Loop.run(~ModelState(~Element,~Context),~ArrayLaws.model_map_step(~Element,~Context,~map),1n+done,initial),
76 ArrayLaws.model_map_step(~Element,~Context,~map,Loop.run(~ModelState(~Element,~Context),~ArrayLaws.model_map_step(~Element,~Context,~map),done,initial)),
77 last_step(~ModelState(~Element,~Context),~ArrayLaws.model_map_step(~Element,~Context,~map),done,initial)) :
78 {MapReadback.output(~Element,~Context,_) ==
79 Tree.write(Element,MapReadback.run_indexed(~Element,~Context,~map,done,U32.from_nat(start),context,input),U32.from_nat(Nat.add(start,done)),
80 map(context,U32.from_nat(Nat.add(start,done)),Tree.read(Element,MapReadback.run_indexed(~Element,~Context,~map,done,U32.from_nat(start),context,input),U32.from_nat(Nat.add(start,done))))) : Tree.Tree<Element>}
81 %Equal.sym(ModelState(~Element,~Context),Loop.run(~ModelState(~Element,~Context),~ArrayLaws.model_map_step(~Element,~Context,~map),done,initial),
82 Traversal.State{Unit{},MapReadback.run_indexed(~Element,~Context,~map,done,U32.from_nat(start),context,input),U32.from_nat(Nat.add(start,done)),context},
83 state_after(~Element,~Context,~map,done,start,context,input)) :
84 {MapReadback.output(~Element,~Context,ArrayLaws.model_map_step(~Element,~Context,~map,_)) ==
85 Tree.write(Element,MapReadback.run_indexed(~Element,~Context,~map,done,U32.from_nat(start),context,input),U32.from_nat(Nat.add(start,done)),
86 map(context,U32.from_nat(Nat.add(start,done)),Tree.read(Element,MapReadback.run_indexed(~Element,~Context,~map,done,U32.from_nat(start),context,input),U32.from_nat(Nat.add(start,done))))) : Tree.Tree<Element>}
87 {==}
88
89# A batch that continues done steps of the map completes the map.
90def continued(~Element: Data,~Context: Data,~map: Context -> U32 -> Element -> Element,+remaining: Nat,+done: Nat,+start: Nat,+context: Context,+input: Tree.Tree<Element>,
91 +depth: Nat,+capacity: U32,+capacity_equal: {Tree.capacity(Element,input) == capacity : U32},+balanced: Shape.Balanced(Element,depth,input),
92 +limit: {Nat.is_le(depth,31n) == True{} : Bool},+capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool},
93 +room: {Nat.is_le(Nat.add(Nat.add(start,done),remaining),U32.to_nat(capacity)) == True{} : Bool}) ->
94 {batch(~Element,~Context,~map,remaining,U32.from_nat(Nat.add(start,done)),context,input,MapReadback.run_indexed(~Element,~Context,~map,done,U32.from_nat(start),context,input)) ==
95 MapReadback.run_indexed(~Element,~Context,~map,Nat.add(done,remaining),U32.from_nat(start),context,input) : Tree.Tree<Element>}:
96 match remaining:
97 case 0n:
98 %Equal.sym(Nat,Nat.add(done,0n),done,Addition.zero_right(done)) :
99 {MapReadback.run_indexed(~Element,~Context,~map,done,U32.from_nat(start),context,input) == MapReadback.run_indexed(~Element,~Context,~map,_,U32.from_nat(start),context,input) : Tree.Tree<Element>}
100 {==}
101 case 1n+ +rest:
102 +reached = Nat.add(start,done)
103 +query = U32.from_nat(reached)
104 +mapped = MapReadback.run_indexed(~Element,~Context,~map,done,U32.from_nat(start),context,input)
105 +inside = Order.room_index(reached,rest,U32.to_nat(capacity),room)
106 +within = Bounds.strict_le(reached,U32.to_nat(capacity),inside)
107 +unread = MapReadback.outside_indexed(~Element,~Context,~map,done,start,query,context,input,depth,capacity,capacity_equal,balanced,limit,capacity_ok,within,
108 MapReadback.address_inside(reached,capacity,capacity_ok,inside),
109 Interval.After{
110 %Equal.sym(Nat,U32.to_nat(query),reached,Bounds.roundtrip(reached,capacity,capacity_ok,within)) : {Nat.is_le(reached,_) == True{} : Bool}
111 Order.reflexive(reached)})
112 %Equal.sym(Nat,Nat.add(done,1n+rest),1n+Nat.add(done,rest),Addition.successor_right(done,rest)) :
113 {batch(~Element,~Context,~map,rest,(query + 1 : U32),context,input,Tree.write(Element,mapped,query,map(context,query,Tree.read(Element,input,query)))) ==
114 MapReadback.run_indexed(~Element,~Context,~map,_,U32.from_nat(start),context,input) : Tree.Tree<Element>}
115 %unread :
116 {batch(~Element,~Context,~map,rest,(query + 1 : U32),context,input,Tree.write(Element,mapped,query,map(context,query,_))) ==
117 MapReadback.run_indexed(~Element,~Context,~map,1n+Nat.add(done,rest),U32.from_nat(start),context,input) : Tree.Tree<Element>}
118 %extended(~Element,~Context,~map,done,start,context,input) :
119 {batch(~Element,~Context,~map,rest,(query + 1 : U32),context,input,_) ==
120 MapReadback.run_indexed(~Element,~Context,~map,1n+Nat.add(done,rest),U32.from_nat(start),context,input) : Tree.Tree<Element>}
121 %Equal.sym(U32,(query + 1 : U32),U32.from_nat(1n+reached),Bounds.add_one(query)) :
122 {batch(~Element,~Context,~map,rest,_,context,input,MapReadback.run_indexed(~Element,~Context,~map,1n+done,U32.from_nat(start),context,input)) ==
123 MapReadback.run_indexed(~Element,~Context,~map,1n+Nat.add(done,rest),U32.from_nat(start),context,input) : Tree.Tree<Element>}
124 %Addition.successor_right(start,done) :
125 {batch(~Element,~Context,~map,rest,U32.from_nat(_),context,input,MapReadback.run_indexed(~Element,~Context,~map,1n+done,U32.from_nat(start),context,input)) ==
126 MapReadback.run_indexed(~Element,~Context,~map,1n+Nat.add(done,rest),U32.from_nat(start),context,input) : Tree.Tree<Element>}
127 continued(~Element,~Context,~map,rest,1n+done,start,context,input,depth,capacity,capacity_equal,balanced,limit,capacity_ok,
128 %Equal.sym(Nat,Nat.add(start,1n+done),1n+reached,Addition.successor_right(start,done)) : {Nat.is_le(Nat.add(_,rest),U32.to_nat(capacity)) == True{} : Bool}
129 Order.advance_room(reached,rest,U32.to_nat(capacity),room))
130
131# A batch from the original tree is the map of its positions.
132def mapped(~Element: Data,~Context: Data,~map: Context -> U32 -> Element -> Element,+count: Nat,+start: Nat,+context: Context,+input: Tree.Tree<Element>,
133 +depth: Nat,+capacity: U32,+capacity_equal: {Tree.capacity(Element,input) == capacity : U32},+balanced: Shape.Balanced(Element,depth,input),
134 +limit: {Nat.is_le(depth,31n) == True{} : Bool},+capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool},
135 +room: {Nat.is_le(Nat.add(start,count),U32.to_nat(capacity)) == True{} : Bool}) ->
136 {batch(~Element,~Context,~map,count,U32.from_nat(start),context,input,input) == MapReadback.run_indexed(~Element,~Context,~map,count,U32.from_nat(start),context,input) : Tree.Tree<Element>}:
137 %Addition.zero_right(start) :
138 {batch(~Element,~Context,~map,count,U32.from_nat(_),context,input,input) == MapReadback.run_indexed(~Element,~Context,~map,count,U32.from_nat(start),context,input) : Tree.Tree<Element>}
139 continued(~Element,~Context,~map,count,0n,start,context,input,depth,capacity,capacity_equal,balanced,limit,capacity_ok,
140 %Equal.sym(Nat,Nat.add(start,0n),start,Addition.zero_right(start)) : {Nat.is_le(Nat.add(_,count),U32.to_nat(capacity)) == True{} : Bool}
141 room)
142
143# Consecutive fixed-width jobs use the indexed traversal invariant. A caller
144# supplies the equation for one batch and its preserved reader frame.
145type RoundPlan<-Element: Data,-Context: Data,-width: Nat> is Data:
146 RoundPlan{count: Nat,context: Context,original: Tree.Tree<Element>,depth: Nat,capacity: U32,
147 capacity_equal: {Tree.capacity(Element,original) == capacity : U32},
148 balanced: Shape.Balanced(Element,depth,original),depth_ok: {Nat.is_le(depth,31n) == True{} : Bool},
149 capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool},
150 room: {Nat.is_le(Nat.mul(count,width),U32.to_nat(capacity)) == True{} : Bool}}
151
152def round_count(~Element: Data,~Context: Data,~width: Nat,plan: RoundPlan<Element,Context,width>) -> Nat:
153 RoundPlan{count,context,original,depth,capacity,capacity_equal,balanced,depth_ok,capacity_ok,room} = plan
154 count
155
156def round_context(~Element: Data,~Context: Data,~width: Nat,plan: RoundPlan<Element,Context,width>) -> Context:
157 RoundPlan{count,context,original,depth,capacity,capacity_equal,balanced,depth_ok,capacity_ok,room} = plan
158 context
159
160def round_original(~Element: Data,~Context: Data,~width: Nat,plan: RoundPlan<Element,Context,width>) -> Tree.Tree<Element>:
161 RoundPlan{count,context,original,depth,capacity,capacity_equal,balanced,depth_ok,capacity_ok,room} = plan
162 original
163
164def round_update(~Element: Data,~Context: Data,~State: Data,~width: Nat,~step: U32 -> Context -> State -> State,index: U32,plan: RoundPlan<Element,Context,width>,state: State) -> State:
165 step(index,round_context(~Element,~Context,~width,plan),state)
166
167def round_frame(~Element: Data,~Context: Data,~State: Data,~MapContext: Data,~width: Nat,
168 ~output: State -> Tree.Tree<Element>,~map_context: Context -> MapContext,~map: MapContext -> U32 -> Element -> Element,~Frame: Context -> State -> Data,
169 plan: RoundPlan<Element,Context,width>,index: Nat,state: State) -> Data:
170 Shape.Both<Frame(round_context(~Element,~Context,~width,plan),state),
171 {output(state) == MapReadback.run_indexed(~Element,~MapContext,~map,Nat.mul(index,width),0,map_context(round_context(~Element,~Context,~width,plan)),round_original(~Element,~Context,~width,plan)) : Tree.Tree<Element>}>
172
173def round_frame_step(~Element: Data,~Context: Data,~State: Data,~MapContext: Data,~width: Nat,
174 ~output: State -> Tree.Tree<Element>,~map_context: Context -> MapContext,~map: MapContext -> U32 -> Element -> Element,~Frame: Context -> State -> Data,
175 ~step: U32 -> Context -> State -> State,
176 ~frame_step: @+context: Context -> @+index: U32 -> @+state: State -> Frame(context,state) -> Frame(context,step(index,context,state)),
177 ~batch_matches: @+context: Context -> @+index: Nat -> @+state: State -> @+depth: Nat -> @+capacity: U32 -> Frame(context,state) ->
178 {Tree.capacity(Element,output(state)) == capacity : U32} -> Shape.Balanced(Element,depth,output(state)) ->
179 {Nat.is_le(depth,31n) == True{} : Bool} -> {U32.is_le(capacity,2147483648) == True{} : Bool} ->
180 {Nat.is_le(Nat.add(Nat.mul(index,width),width),U32.to_nat(capacity)) == True{} : Bool} ->
181 {output(step(U32.from_nat(index),context,state)) == MapReadback.run_indexed(~Element,~MapContext,~map,width,U32.from_nat(Nat.mul(index,width)),map_context(context),output(state)) : Tree.Tree<Element>},
182 +plan: RoundPlan<Element,Context,width>,+index: Nat,+state: State,
183 inside: {Nat.is_lt(index,round_count(~Element,~Context,~width,plan)) == True{} : Bool},
184 progress: round_frame(~Element,~Context,~State,~MapContext,~width,~output,~map_context,~map,~Frame,plan,index,state)) ->
185 round_frame(~Element,~Context,~State,~MapContext,~width,~output,~map_context,~map,~Frame,plan,1n+index,round_update(~Element,~Context,~State,~width,~step,U32.from_nat(index),plan,state)):
186 RoundPlan{+count,+context,+original,+depth,+capacity,+capacity_equal,+balanced,+depth_ok,+capacity_ok,+room} = plan
187 Shape.Both{+frame,+mapped} = progress
188 +done = Nat.mul(index,width)
189 +values = MapReadback.run_indexed(~Element,~MapContext,~map,done,0,map_context(context),original)
190 +batch_room = {
191 %Order.commutative(width,done) : {Nat.is_le(_,U32.to_nat(capacity)) == True{} : Bool}
192 Order.transitive(Nat.mul(1n+index,width),Nat.mul(count,width),U32.to_nat(capacity),
193 RowMajor.mul_le(1n+index,count,width,Order.strict_follow(index,count,inside)),room)
194 : {Nat.is_le(Nat.add(done,width),U32.to_nat(capacity)) == True{} : Bool}}
195 +equal_capacity = Equal.trans(U32,Tree.capacity(Element,output(state)),Tree.capacity(Element,values),capacity,
196 Equal.cong(Tree.Tree<Element>,U32,tree => Tree.capacity(Element,tree),output(state),values,mapped),
197 Equal.trans(U32,Tree.capacity(Element,values),Tree.capacity(Element,original),capacity,MapReadback.capacity_indexed(~Element,~MapContext,~map,done,0,map_context(context),original),capacity_equal))
198 +balance = {
199 %Equal.sym(Tree.Tree<Element>,output(state),values,mapped) : Shape.Balanced(Element,depth,_)
200 MapReadback.balanced_indexed(~Element,~MapContext,~map,done,0,map_context(context),original,depth,balanced)
201 : Shape.Balanced(Element,depth,output(state))}
202 +one = batch_matches(context,index,state,depth,capacity,frame,equal_capacity,balance,depth_ok,capacity_ok,batch_room)
203 Shape.Both{frame_step(context,U32.from_nat(index),state,frame),
204 %Order.commutative(done,width) : {output(step(U32.from_nat(index),context,state)) == MapReadback.run_indexed(~Element,~MapContext,~map,_,0,map_context(context),original) : Tree.Tree<Element>}
205 Equal.trans(Tree.Tree<Element>,output(step(U32.from_nat(index),context,state)),
206 MapReadback.run_indexed(~Element,~MapContext,~map,width,U32.from_nat(done),map_context(context),output(state)),
207 MapReadback.run_indexed(~Element,~MapContext,~map,Nat.add(done,width),0,map_context(context),original),one,
208 Equal.trans(Tree.Tree<Element>,MapReadback.run_indexed(~Element,~MapContext,~map,width,U32.from_nat(done),map_context(context),output(state)),
209 MapReadback.run_indexed(~Element,~MapContext,~map,width,U32.from_nat(done),map_context(context),values),
210 MapReadback.run_indexed(~Element,~MapContext,~map,Nat.add(done,width),0,map_context(context),original),
211 Equal.cong(Tree.Tree<Element>,Tree.Tree<Element>,tree => MapReadback.run_indexed(~Element,~MapContext,~map,width,U32.from_nat(done),map_context(context),tree),output(state),values,mapped),
212 Equal.sym(Tree.Tree<Element>,MapReadback.run_indexed(~Element,~MapContext,~map,Nat.add(done,width),0,map_context(context),original),
213 MapReadback.run_indexed(~Element,~MapContext,~map,width,U32.from_nat(done),map_context(context),values),map_split(~Element,~MapContext,~map,done,width,0n,map_context(context),original))))}
214
215def round_same_step(~Element: Data,~Context: Data,~State: Data,~width: Nat,~step: U32 -> Context -> State -> State,
216 +index: U32,+plan: RoundPlan<Element,Context,width>,+state: State) ->
217 {round_update(~Element,~Context,~State,~width,~step,index,plan,state) == step(index,round_context(~Element,~Context,~width,plan),state) : State}:
218 {==}
219
220def fold_mapped(~Element: Data,~Context: Data,~State: Data,~MapContext: Data,~width: Nat,
221 ~output: State -> Tree.Tree<Element>,~map_context: Context -> MapContext,~map: MapContext -> U32 -> Element -> Element,~Frame: Context -> State -> Data,
222 ~step: U32 -> Context -> State -> State,
223 ~frame_step: @+context: Context -> @+index: U32 -> @+state: State -> Frame(context,state) -> Frame(context,step(index,context,state)),
224 ~batch_matches: @+context: Context -> @+index: Nat -> @+state: State -> @+depth: Nat -> @+capacity: U32 -> Frame(context,state) ->
225 {Tree.capacity(Element,output(state)) == capacity : U32} -> Shape.Balanced(Element,depth,output(state)) ->
226 {Nat.is_le(depth,31n) == True{} : Bool} -> {U32.is_le(capacity,2147483648) == True{} : Bool} ->
227 {Nat.is_le(Nat.add(Nat.mul(index,width),width),U32.to_nat(capacity)) == True{} : Bool} ->
228 {output(step(U32.from_nat(index),context,state)) == MapReadback.run_indexed(~Element,~MapContext,~map,width,U32.from_nat(Nat.mul(index,width)),map_context(context),output(state)) : Tree.Tree<Element>},
229 +count: Nat,+context: Context,+state: State,+depth: Nat,+capacity: U32,+frame: Frame(context,state),
230 +capacity_equal: {Tree.capacity(Element,output(state)) == capacity : U32},+balanced: Shape.Balanced(Element,depth,output(state)),
231 +depth_ok: {Nat.is_le(depth,31n) == True{} : Bool},+capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool},
232 +room: {Nat.is_le(Nat.mul(count,width),U32.to_nat(capacity)) == True{} : Bool}) ->
233 Shape.Both<Frame(context,Traversal.indexed_fold(~State,~Context,~step,count,0,context,state)),
234 {output(Traversal.indexed_fold(~State,~Context,~step,count,0,context,state)) == MapReadback.run_indexed(~Element,~MapContext,~map,Nat.mul(count,width),0,map_context(context),output(state)) : Tree.Tree<Element>}>:
235 +plan = {RoundPlan{count,context,output(state),depth,capacity,capacity_equal,balanced,depth_ok,capacity_ok,room} : RoundPlan<Element,Context,width>}
236 %ArrayLaws.indexed_fold_change_context(~State,~RoundPlan<Element,Context,width>,~Context,~round_context(~Element,~Context,~width),
237 ~round_update(~Element,~Context,~State,~width,~step),~step,~round_same_step(~Element,~Context,~State,~width,~step),count,0,plan,state) :
238 Shape.Both<Frame(context,_),{output(_) == MapReadback.run_indexed(~Element,~MapContext,~map,Nat.mul(count,width),0,map_context(context),output(state)) : Tree.Tree<Element>}>
239 ArrayLaws.indexed_fold_preserves_invariant(~State,~RoundPlan<Element,Context,width>,~round_count(~Element,~Context,~width),
240 ~round_frame(~Element,~Context,~State,~MapContext,~width,~output,~map_context,~map,~Frame),~round_update(~Element,~Context,~State,~width,~step),
241 ~round_frame_step(~Element,~Context,~State,~MapContext,~width,~output,~map_context,~map,~Frame,~step,~frame_step,~batch_matches),
242 count,0n,plan,state,Order.reflexive(count),Shape.Both{frame,{==}})