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 ../kernel_block.bend as Block 5 import ../traversal_array.bend as Traversal 6 import ../traversal_loop.bend as Loop 7 import ./storage_tree_model.bend as Tree 8 import ./storage_refinement.bend as StorageLaws 9 import ./loop_projection.bend as Projection 10 import ./natural_addition.bend as Addition 11 import ./nat_to_u32_bounds.bend as Bounds 12 import ./nat_order.bend as Order 13 14 def represent(~Reader: Type,~Model: Data,~Element: Data,~Context: Data,~pack_reader: Model -> Reader, 15 state: Traversal.State<&2,&2,Model,Tree.Tree,Context>) -> Traversal.State<&1,&1,Reader,Array,Context>: 16 Traversal.State{reader,output,position,context} = state 17 Traversal.State{pack_reader(reader),Tree.pack(Element,output),position,context} 18 19 def 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,Context>) -> Traversal.State<&2,&2,Model,Tree.Tree,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 25 def 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,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,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,Context>} 39 %Equal.sym(Array,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,Context>} 45 {==} 46 47 def 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,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,Context>,~model_step(~Model,~Element,~Context,~sample,~destination),count,state)) : 56 Traversal.State<&1,&1,Reader,Array,Context>}: 57 Projection.iteration_refines_model(~Traversal.State<&1,&1,Reader,Array,Context>,~Traversal.State<&2,&2,Model,Tree.Tree,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 62 def pack_tree(~Element: Data,tree: Tree.Tree) -> Array: 63 Tree.pack(Element,tree) 64 65 def sample_offset(~Element: Data,tree: Tree.Tree,context: Traversal.Offsets,position: U32) -> Element: 66 Traversal.Offsets{source,destination} = context 67 Tree.read(Element,tree,(source + position : U32)) 68 69 def offset_read_refines_storage(~Element: Data,+tree: Tree.Tree,+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}: 72 Traversal.Offsets{source,destination} = context 73 StorageLaws.read(Element,tree,(source + position : U32)) 74 75 def copy_traversal_refines_storage(~Element: Data,+count: Nat, 76 +state: Traversal.State<&2,&2,Tree.Tree,Tree.Tree,Traversal.Offsets>) -> 77 {Traversal.run(~Array,~Element,~Traversal.Offsets,~Traversal.source_offset(~Element),~Traversal.destination_offset,count, 78 represent(~Array,~Tree.Tree,~Element,~Traversal.Offsets,~pack_tree(~Element),state)) == 79 represent(~Array,~Tree.Tree,~Element,~Traversal.Offsets,~pack_tree(~Element), 80 Loop.run(~Traversal.State<&2,&2,Tree.Tree,Tree.Tree,Traversal.Offsets>, 81 ~model_step(~Tree.Tree,~Element,~Traversal.Offsets,~sample_offset(~Element),~Traversal.destination_offset),count,state)) : 82 Traversal.State<&1,&1,Array,Array,Traversal.Offsets>}: 83 traversal_refines_model(~Array,~Tree.Tree,~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. 88 def 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 93 def 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 99 def 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 118 def 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. 135 def represent_map(~Element: Data,~Context: Data, 136 state: Traversal.State<&2,&2,Unit,Tree.Tree,Context>) -> Traversal.State<&2,&1,Unit,Array,Context>: 137 Traversal.State{Unit{},output,position,context} = state 138 Traversal.State{Unit{},Tree.pack(Element,output),position,context} 139 140 def unindexed(~Element: Data,~Context: Data,~map: Context -> Element -> Element,context: Context,position: U32,value: Element) -> Element: 141 map(context,value) 142 143 def model_map_step(~Element: Data,~Context: Data,~map: Context -> U32 -> Element -> Element, 144 state: Traversal.State<&2,&2,Unit,Tree.Tree,Context>) -> Traversal.State<&2,&2,Unit,Tree.Tree,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 149 def map_step_refines_model(~Element: Data,~Context: Data,~map: Context -> Element -> Element, 150 +state: Traversal.State<&2,&2,Unit,Tree.Tree,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,Context>}: 153 Traversal.State{Unit{},+output,+position,+context} = state 154 %Equal.sym(Array & 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,Context>} 158 %Equal.sym(Array,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,Context>} 163 {==} 164 165 def map_loop_refines_model(~Element: Data,~Context: Data,~map: Context -> Element -> Element, 166 +count: Nat,+state: Traversal.State<&2,&2,Unit,Tree.Tree,Context>) -> 167 {Loop.run(~Traversal.State<&2,&1,Unit,Array,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,Context>, 170 ~model_map_step(~Element,~Context,~unindexed(~Element,~Context,~map)),count,state)) : Traversal.State<&2,&1,Unit,Array,Context>}: 171 Projection.iteration_refines_model(~Traversal.State<&2,&1,Unit,Array,Context>,~Traversal.State<&2,&2,Unit,Tree.Tree,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. 181 def 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,Context>) -> Traversal.State<&2,&2,Model,Tree.Tree,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 188 def 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,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,Context>}: 198 Traversal.State{+reader,+output,+position,+context} = state 199 %Equal.sym(Array & 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,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,Context>} 209 %Equal.sym(Array,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,Context>} 217 {==} 218 219 def 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,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,Context>, 229 ~model_update_step(~Model,~Element,~Sample,~Context,~sample,~combine,~destination),count,state)) : 230 Traversal.State<&1,&1,Reader,Array,Context>}: 231 Projection.iteration_refines_model(~Traversal.State<&1,&1,Reader,Array,Context>,~Traversal.State<&2,&2,Model,Tree.Tree,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 237 def 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. 257 def 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 273 def 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. 297 def 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))