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. 5 import Base 6 import ../traversal_array.bend as Traversal 7 import ../traversal_loop.bend as Loop 8 import ./traversal_array_refinement.bend as ArrayLaws 9 import ./traversal_map_readback.bend as MapReadback 10 import ./storage_tree_model.bend as Tree 11 import ./storage_shape.bend as Shape 12 import ./nat_to_u32_bounds.bend as Bounds 13 import ./nat_order.bend as Order 14 import ./natural_addition.bend as Addition 15 import ./nat_interval.bend as Interval 16 import ./loop_projection.bend as Projection 17 import ./row_major_index.bend as RowMajor 18 19 def batch(~Element: Data,~Context: Data,~map: Context -> U32 -> Element -> Element,count: Nat,+position: U32,+context: Context,+source: Tree.Tree, 20 target: Tree.Tree) -> Tree.Tree: 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 26 def ModelState(~Element: Data,~Context: Data) -> Data: 27 Traversal.State<&2,&2,Unit,Tree.Tree,Context> 28 29 # A loop's last step, for every state and count. 30 def 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. 37 def state_after(~Element: Data,~Context: Data,~map: Context -> U32 -> Element -> Element,+count: Nat,+start: Nat,+context: Context,+input: Tree.Tree) -> 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. 57 def map_split(~Element: Data,~Context: Data,~map: Context -> U32 -> Element -> Element,+first: Nat,+second: Nat,+start: Nat,+context: Context,+input: Tree.Tree) -> 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}: 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} 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} 68 {==} 69 70 def extended(~Element: Data,~Context: Data,~map: Context -> U32 -> Element -> Element,+done: Nat,+start: Nat,+context: Context,+input: Tree.Tree) -> 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}: 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} 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} 87 {==} 88 89 # A batch that continues done steps of the map completes the map. 90 def continued(~Element: Data,~Context: Data,~map: Context -> U32 -> Element -> Element,+remaining: Nat,+done: Nat,+start: Nat,+context: Context,+input: Tree.Tree, 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}: 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} 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} 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} 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} 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} 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} 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. 132 def mapped(~Element: Data,~Context: Data,~map: Context -> U32 -> Element -> Element,+count: Nat,+start: Nat,+context: Context,+input: Tree.Tree, 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}: 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} 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. 145 type RoundPlan<-Element: Data,-Context: Data,-width: Nat> is Data: 146 RoundPlan{count: Nat,context: Context,original: Tree.Tree,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 152 def round_count(~Element: Data,~Context: Data,~width: Nat,plan: RoundPlan) -> Nat: 153 RoundPlan{count,context,original,depth,capacity,capacity_equal,balanced,depth_ok,capacity_ok,room} = plan 154 count 155 156 def round_context(~Element: Data,~Context: Data,~width: Nat,plan: RoundPlan) -> Context: 157 RoundPlan{count,context,original,depth,capacity,capacity_equal,balanced,depth_ok,capacity_ok,room} = plan 158 context 159 160 def round_original(~Element: Data,~Context: Data,~width: Nat,plan: RoundPlan) -> Tree.Tree: 161 RoundPlan{count,context,original,depth,capacity,capacity_equal,balanced,depth_ok,capacity_ok,room} = plan 162 original 163 164 def round_update(~Element: Data,~Context: Data,~State: Data,~width: Nat,~step: U32 -> Context -> State -> State,index: U32,plan: RoundPlan,state: State) -> State: 165 step(index,round_context(~Element,~Context,~width,plan),state) 166 167 def round_frame(~Element: Data,~Context: Data,~State: Data,~MapContext: Data,~width: Nat, 168 ~output: State -> Tree.Tree,~map_context: Context -> MapContext,~map: MapContext -> U32 -> Element -> Element,~Frame: Context -> State -> Data, 169 plan: RoundPlan,index: Nat,state: State) -> Data: 170 Shape.Both}> 172 173 def round_frame_step(~Element: Data,~Context: Data,~State: Data,~MapContext: Data,~width: Nat, 174 ~output: State -> Tree.Tree,~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}, 182 +plan: RoundPlan,+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,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,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} 205 Equal.trans(Tree.Tree,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,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,Tree.Tree,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,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 215 def round_same_step(~Element: Data,~Context: Data,~State: Data,~width: Nat,~step: U32 -> Context -> State -> State, 216 +index: U32,+plan: RoundPlan,+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 220 def fold_mapped(~Element: Data,~Context: Data,~State: Data,~MapContext: Data,~width: Nat, 221 ~output: State -> Tree.Tree,~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}, 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}>: 235 +plan = {RoundPlan{count,context,output(state),depth,capacity,capacity_equal,balanced,depth_ok,capacity_ok,room} : RoundPlan} 236 %ArrayLaws.indexed_fold_change_context(~State,~RoundPlan,~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}> 239 ArrayLaws.indexed_fold_preserves_invariant(~State,~RoundPlan,~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,{==}})