1 import Base 2 import ./lifecycle.bend as L 3 import ./change_tick.bend as Tick 4 5 # Trusted storage. Public declarations confine these owners before gameplay runs. 6 type Column<-S:Data,-C:Type> is Type: 7 Leaf{values:Array>,stamps:Array} 8 Branch{half:U32,left:Column,right:Column} 9 type SwapOutcome<-S:Data,-C:Type> is Type: 10 Accepted{column:Column,previous:Maybe<&1,C>} 11 Rejected{column:Column,incoming:Maybe<&1,C>} 12 13 def absent_generic(-C:Type,depth:Nat) -> Array>: 14 match depth: 15 case 0n:ALeaf{None{}} 16 case 1n++rest:ANode{absent_generic(C,rest),absent_generic(C,rest)} 17 def empty_generic(-S:Data,-C:Type) -> Column: 18 Leaf{absent_generic(C,3n),[L.Stamp{None{},None{}} : L.Stamp^3n]} 19 def capacity_generic(-S:Data,-C:Type,column:Column) -> Column & U32: 20 match column: 21 case Leaf{values,stamps}:(Leaf{values,stamps},8) 22 case Branch{+half,left,right}:(Branch{half,left,right},U32.add(half,half)) 23 def vacant_generic(-S:Data,-C:Type,depth:Nat) -> Column: 24 match depth: 25 case 0n:empty_generic(S,C) 26 case 1n++rest: 27 +half = U32.shln(8,rest) 28 Branch{half,vacant_generic(S,C,rest),vacant_generic(S,C,rest)} 29 def grown_generic(-S:Data,-C:Type,fuel:Nat,column:Column,+size:U32,+depth:Nat,+target:U32,enough:Bool) -> Column: 30 match fuel enough: 31 case _ True{}:column 32 case 0n False{}:column 33 case 1n+rest False{}:grown_generic(S,C,rest,Branch{size,column,vacant_generic(S,C,depth)},U32.add(size,size),1n+depth,target,U32.is_le(target,U32.add(size,size))) 34 def ensure_sized_generic(-S:Data,-C:Type,+target:U32,result:Column & U32) -> Column: 35 match result: 36 case (column,+size):grown_generic(S,C,14n,column,size,Nat.sub(U32.log2(size),3n),target,U32.is_le(target,size)) 37 def maximum_capacity() -> U32:131072 38 def ensure_generic(-S:Data,-C:Type,column:Column,target:U32) -> Column: 39 ensure_sized_generic(S,C,U32.min(target,maximum_capacity()),capacity_generic(S,C,column)) 40 def absent(~C:Type,depth:Nat) -> Array>:absent_generic(C,depth) 41 def empty(~S:Data,~C:Type) -> Column:empty_generic(S,C) 42 def capacity(~S:Data,~C:Type,column:Column) -> Column & U32:capacity_generic(S,C,column) 43 def vacant(~S:Data,~C:Type,depth:Nat) -> Column:vacant_generic(S,C,depth) 44 def grown(~S:Data,~C:Type,fuel:Nat,column:Column,size:U32,depth:Nat,target:U32,enough:Bool) -> Column:grown_generic(S,C,fuel,column,size,depth,target,enough) 45 def ensure_sized(~S:Data,~C:Type,target:U32,result:Column & U32) -> Column:ensure_sized_generic(S,C,target,result) 46 def ensure(~S:Data,~C:Type,column:Column,target:U32) -> Column:ensure_generic(S,C,column,target) 47 48 # Actual presence only; None distinguishes unavailable/malformed leaf storage. 49 # Bounds use actual array lengths before any affine cell is temporarily moved. 50 def vacancy_restored(-S:Data,-C:Type,stamps:Array,index:U32,result:Array> & Maybe<&1,C>) -> Column & Maybe<&2,Bool>: 51 match result: 52 case (values,None{}):(Leaf{values,stamps},Some{True{}}) 53 case (values,Some{owner}):(Leaf{Array.set(Maybe<&1,C>,values,index,Some{owner}),stamps},Some{False{}}) 54 def vacancy_bounded(-S:Data,-C:Type,values:Array>,stamps:Array,+index:U32,valid:Bool) -> Column & Maybe<&2,Bool>: 55 match valid: 56 case False{}:(Leaf{values,stamps},None{}) 57 case True{}:vacancy_restored(S,C,stamps,index,Array.swap(Maybe<&1,C>,values,index,None{})) 58 def vacancy_stamps(-S:Data,-C:Type,values:Array>,valueSize:U32,+index:U32,result:Array & U32) -> Column & Maybe<&2,Bool>: 59 match result: 60 case (stamps,stampSize):vacancy_bounded(S,C,values,stamps,index,Bool.and(U32.is_eq(valueSize,8),Bool.and(U32.is_eq(stampSize,8),U32.is_lt(index,8)))) 61 def vacancy_values(-S:Data,-C:Type,stamps:Array,index:U32,result:Array> & U32) -> Column & Maybe<&2,Bool>: 62 match result: 63 case (values,size):vacancy_stamps(S,C,values,size,index,Array.size(L.Stamp,stamps)) 64 def vacancy_join(-S:Data,-C:Type,half:U32,leftResult:Column & Maybe<&2,Bool>,rightResult:Column & Maybe<&2,Bool>) -> Column & Maybe<&2,Bool>: 65 match leftResult rightResult: 66 case (left,Some{result}), (right,_):(Branch{half,left,right},Some{result}) 67 case (left,None{}), (right,result):(Branch{half,left,right},result) 68 def vacancy_selected(-S:Data,-C:Type,column:Column,+index:U32,selected:Bool) -> Column & Maybe<&2,Bool>: 69 match column selected: 70 case column False{}:(column,None{}) 71 case Leaf{values,stamps} True{}:vacancy_values(S,C,stamps,index,Array.size(Maybe<&1,C>,values)) 72 case Branch{+half,left,right} True{}:vacancy_join(S,C,half,vacancy_selected(S,C,left,index,U32.is_lt(index,half)),vacancy_selected(S,C,right,U32.sub(index,half),Bool.not(U32.is_lt(index,half)))) 73 def vacancy_generic(-S:Data,-C:Type,column:Column,index:U32) -> Column & Maybe<&2,Bool>: 74 vacancy_selected(S,C,column,index,True{}) 75 76 def present_generic(-C:Type,value:Maybe<&1,C>) -> Maybe<&1,C> & Bool: 77 match value: 78 case None{}: (None{},False{}) 79 case Some{owner}: (Some{owner},True{}) 80 def present(~C:Type,value:Maybe<&1,C>) -> Maybe<&1,C> & Bool: 81 present_generic(C,value) 82 83 def swap_finish_generic(-S:Data,-C:Type,values:Array>,+index:U32,incoming:Bool,previous:Maybe<&1,C>,wasPresent:Bool,tick:Tick.Tick,result:Array & L.Stamp) -> SwapOutcome: 84 match result: 85 case (stamps,stamp): Accepted{Leaf{values,Array.set(L.Stamp,stamps,index,L.after_write(incoming,wasPresent,stamp,tick))},previous} 86 def swap_finish(~S:Data,~C:Type,values:Array>,+index:U32,incoming:Bool,previous:Maybe<&1,C>,wasPresent:Bool,tick:Tick.Tick,result:Array & L.Stamp) -> SwapOutcome: 87 swap_finish_generic(S,C,values,index,incoming,previous,wasPresent,tick,result) 88 89 def swap_presence_generic(-S:Data,-C:Type,values:Array>,stamps:Array,+index:U32,incoming:Bool,tick:Tick.Tick,result:Maybe<&1,C> & Bool) -> SwapOutcome: 90 match result: 91 case (previous,wasPresent): swap_finish_generic(S,C,values,index,incoming,previous,wasPresent,tick,Array.get(L.Stamp,stamps,index)) 92 def swap_presence(~S:Data,~C:Type,values:Array>,stamps:Array,+index:U32,incoming:Bool,tick:Tick.Tick,result:Maybe<&1,C> & Bool) -> SwapOutcome: 93 swap_presence_generic(S,C,values,stamps,index,incoming,tick,result) 94 95 def swap_previous_generic(-S:Data,-C:Type,stamps:Array,index:U32,incoming:Bool,tick:Tick.Tick,result:Array> & Maybe<&1,C>) -> SwapOutcome: 96 match result: 97 case (values,previous): swap_presence_generic(S,C,values,stamps,index,incoming,tick,present_generic(C,previous)) 98 def swap_previous(~S:Data,~C:Type,stamps:Array,index:U32,incoming:Bool,tick:Tick.Tick,result:Array> & Maybe<&1,C>) -> SwapOutcome: 99 swap_previous_generic(S,C,stamps,index,incoming,tick,result) 100 101 def swap_incoming_generic(-S:Data,-C:Type,values:Array>,stamps:Array,+index:U32,tick:Tick.Tick,result:Maybe<&1,C> & Bool) -> SwapOutcome: 102 match result: 103 case (incoming,isPresent): swap_previous_generic(S,C,stamps,index,isPresent,tick,Array.swap(Maybe<&1,C>,values,index,incoming)) 104 def swap_incoming(~S:Data,~C:Type,values:Array>,stamps:Array,+index:U32,tick:Tick.Tick,result:Maybe<&1,C> & Bool) -> SwapOutcome: 105 swap_incoming_generic(S,C,values,stamps,index,tick,result) 106 107 def swap_leaf_generic(-S:Data,-C:Type,values:Array>,stamps:Array,+index:U32,incoming:Maybe<&1,C>,tick:Tick.Tick,valid:Bool) -> SwapOutcome: 108 match valid: 109 case False{}: Rejected{Leaf{values,stamps},incoming} 110 case True{}: swap_incoming_generic(S,C,values,stamps,index,tick,present_generic(C,incoming)) 111 def swap_leaf(~S:Data,~C:Type,values:Array>,stamps:Array,+index:U32,incoming:Maybe<&1,C>,tick:Tick.Tick,valid:Bool) -> SwapOutcome: 112 swap_leaf_generic(S,C,values,stamps,index,incoming,tick,valid) 113 114 def swap_left(~S:Data,~C:Type,half:U32,right:Column,result:SwapOutcome) -> SwapOutcome: 115 match result: 116 case Accepted{left,previous}: Accepted{Branch{half,left,right},previous} 117 case Rejected{left,incoming}: Rejected{Branch{half,left,right},incoming} 118 def swap_right(~S:Data,~C:Type,half:U32,left:Column,result:SwapOutcome) -> SwapOutcome: 119 match result: 120 case Accepted{right,previous}: Accepted{Branch{half,left,right},previous} 121 case Rejected{right,incoming}: Rejected{Branch{half,left,right},incoming} 122 type Path<-S:Data,-C:Type> is Type: 123 Root{} 124 FromLeft{half:U32,right:Column,parent:Path} 125 FromRight{half:U32,left:Column,parent:Path} 126 def rebuild(~S:Data,~C:Type,path:Path,column:Column) -> Column: 127 match path: 128 case Root{}: column 129 case FromLeft{half,right,parent}: rebuild(~S,~C,parent,Branch{half,column,right}) 130 case FromRight{half,left,parent}: rebuild(~S,~C,parent,Branch{half,left,column}) 131 def returned(~S:Data,~C:Type,path:Path,result:SwapOutcome) -> SwapOutcome: 132 match result: 133 case Accepted{column,previous}: Accepted{rebuild(~S,~C,path,column),previous} 134 case Rejected{column,incoming}: Rejected{rebuild(~S,~C,path,column),incoming} 135 type Search<-S:Data,-C:Type> is Type: 136 Search{column:Column,index:U32,incoming:Maybe<&1,C>,path:Path} 137 def route(~S:Data,~C:Type,left:Column,right:Column,+half:U32,+index:U32,incoming:Maybe<&1,C>,path:Path,first:Bool) -> Search: 138 match first: 139 case True{}: Search{left,index,incoming,FromLeft{half,right,path}} 140 case False{}: Search{right,U32.sub(index,half),incoming,FromRight{half,left,path}} 141 def search(~S:Data,~C:Type,fuel:Nat,state:Search,+tick:Tick.Tick) -> SwapOutcome: 142 match fuel state: 143 case 0n Search{column,_,incoming,path}: Rejected{rebuild(~S,~C,path,column),incoming} 144 case 1n+_ Search{Leaf{values,stamps},+index,incoming,path}: returned(~S,~C,path,swap_leaf(~S,~C,values,stamps,index,incoming,tick,U32.is_lt(index,8))) 145 case 1n+rest Search{Branch{+half,left,right},+index,incoming,path}: search(~S,~C,rest,route(~S,~C,left,right,half,index,incoming,path,U32.is_lt(index,half)),tick) 146 def swap_at(~S:Data,~C:Type,column:Column,index:U32,incoming:Maybe<&1,C>,tick:Tick.Tick) -> SwapOutcome: 147 search(~S,~C,15n,Search{column,index,incoming,Root{}},tick) 148 def swap(~S:Data,~C:Type,column:Column,index:U32,incoming:Maybe<&1,C>) -> SwapOutcome: 149 swap_at(~S,~C,column,index,incoming,Tick.zero()) 150 151 def edit_mark(index:U32,tick:Tick.Tick,result:Array & L.Stamp) -> Array: 152 match result: 153 case (stamps,stamp): Array.set(L.Stamp,stamps,index,L.written(True{},stamp,tick)) 154 def edit_stamps(stamps:Array,+index:U32,tick:Tick.Tick,write:Bool) -> Array: 155 match write: 156 case False{}: stamps 157 case True{}: edit_mark(index,tick,Array.get(L.Stamp,stamps,index)) 158 def edit_projected(-S:Data,-C:Type,-V:Data,values:Array>,stamps:Array,+index:U32,tick:Tick.Tick,write:Bool,result:C & V) -> Column & Maybe<&2,V>: 159 match result: 160 case (owner,value): (Leaf{Array.set(Maybe<&1,C>,values,index,Some{owner}),edit_stamps(stamps,index,tick,write)},Some{value}) 161 def edit_taken(-S:Data,-C:Type,-V:Data,transform:C -> C & V,stamps:Array,index:U32,tick:Tick.Tick,write:Bool,result:Array> & Maybe<&1,C>) -> Column & Maybe<&2,V>: 162 match result: 163 case (values,None{}): (Leaf{values,stamps},None{}) 164 case (values,Some{owner}): edit_projected(S,C,V,values,stamps,index,tick,write,transform(owner)) 165 def edit_leaf(-S:Data,-C:Type,-V:Data,transform:C -> C & V,values:Array>,stamps:Array,+index:U32,tick:Tick.Tick,write:Bool,valid:Bool) -> Column & Maybe<&2,V>: 166 match valid: 167 case False{}: (Leaf{values,stamps},None{}) 168 case True{}: edit_taken(S,C,V,transform,stamps,index,tick,write,Array.swap(Maybe<&1,C>,values,index,None{})) 169 def edit_return(~S:Data,~C:Type,~V:Data,path:Path,result:Column & Maybe<&2,V>) -> Column & Maybe<&2,V>: 170 match result: 171 case (column,value): (rebuild(~S,~C,path,column),value) 172 type Visit<-S:Data,-C:Type> is Type: 173 Visit{column:Column,index:U32,path:Path} 174 def edit_route(~S:Data,~C:Type,left:Column,right:Column,+half:U32,+index:U32,path:Path,first:Bool) -> Visit: 175 match first: 176 case True{}: Visit{left,index,FromLeft{half,right,path}} 177 case False{}: Visit{right,U32.sub(index,half),FromRight{half,left,path}} 178 def edit_search(~S:Data,~C:Type,~V:Data,transform:C -> C & V,fuel:Nat,state:Visit,+tick:Tick.Tick,+write:Bool) -> Column & Maybe<&2,V>: 179 match fuel state: 180 case 0n Visit{column,_,path}: (rebuild(~S,~C,path,column),None{}) 181 case 1n+_ Visit{Leaf{values,stamps},+index,path}: edit_return(~S,~C,~V,path,edit_leaf(S,C,V,transform,values,stamps,index,tick,write,U32.is_lt(index,8))) 182 case 1n+rest Visit{Branch{+half,left,right},+index,path}: edit_search(~S,~C,~V,transform,rest,edit_route(~S,~C,left,right,half,index,path,U32.is_lt(index,half)),tick,write) 183 def view(~S:Data,~C:Type,~V:Data,~project:C -> C & V,column:Column,index:U32) -> Column & Maybe<&2,V>: 184 edit_search(~S,~C,~V,project,15n,Visit{column,index,Root{}},Tick.zero(),False{}) 185 def modify_at(~S:Data,~C:Type,~V:Data,~transform:C -> C & V,column:Column,index:U32,tick:Tick.Tick) -> Column & Maybe<&2,V>: 186 edit_search(~S,~C,~V,transform,15n,Visit{column,index,Root{}},tick,True{}) 187 def modify(~S:Data,~C:Type,~V:Data,~transform:C -> C & V,column:Column,index:U32) -> Column & Maybe<&2,V>: 188 modify_at(~S,~C,~V,~transform,column,index,Tick.zero()) 189 def stamp_got(~S:Data,~C:Type,values:Array>,result:Array & L.Stamp) -> Column & Maybe<&2,L.Stamp>: 190 match result: 191 case (stamps,stamp): (Leaf{values,stamps},Some{stamp}) 192 def stamp_leaf(~S:Data,~C:Type,values:Array>,stamps:Array,+index:U32,valid:Bool) -> Column & Maybe<&2,L.Stamp>: 193 match valid: 194 case False{}: (Leaf{values,stamps},None{}) 195 case True{}: stamp_got(~S,~C,values,Array.get(L.Stamp,stamps,index)) 196 def stamp_search(~S:Data,~C:Type,fuel:Nat,state:Visit) -> Column & Maybe<&2,L.Stamp>: 197 match fuel state: 198 case 0n Visit{column,_,path}: (rebuild(~S,~C,path,column),None{}) 199 case 1n+_ Visit{Leaf{values,stamps},+index,path}: edit_return(~S,~C,~L.Stamp,path,stamp_leaf(~S,~C,values,stamps,index,U32.is_lt(index,8))) 200 case 1n+rest Visit{Branch{+half,left,right},+index,path}: stamp_search(~S,~C,rest,edit_route(~S,~C,left,right,half,index,path,U32.is_lt(index,half))) 201 def lifecycle(~S:Data,~C:Type,column:Column,index:U32) -> Column & Maybe<&2,L.Stamp>: 202 stamp_search(~S,~C,15n,Visit{column,index,Root{} }) 203 204 # Trusted recovery restores the recorded stamp without changing payload owners. 205 def restore_leaf(~S:Data,~C:Type,values:Array>,stamps:Array,index:U32,stamp:L.Stamp,valid:Bool) -> Column: 206 match valid: 207 case False{}:Leaf{values,stamps} 208 case True{}:Leaf{values,Array.set(L.Stamp,stamps,index,stamp)} 209 def restore_search(~S:Data,~C:Type,fuel:Nat,state:Visit,+stamp:L.Stamp) -> Column: 210 match fuel state: 211 case 0n Visit{column,_,path}:rebuild(~S,~C,path,column) 212 case 1n+_ Visit{Leaf{values,stamps},+index,path}:rebuild(~S,~C,path,restore_leaf(~S,~C,values,stamps,index,stamp,U32.is_lt(index,8))) 213 case 1n+rest Visit{Branch{+half,left,right},+index,path}:restore_search(~S,~C,rest,edit_route(~S,~C,left,right,half,index,path,U32.is_lt(index,half)),stamp) 214 def restore_stamp(~S:Data,~C:Type,column:Column,index:U32,stamp:L.Stamp) -> Column: 215 restore_search(~S,~C,15n,Visit{column,index,Root{}},stamp) 216 217 def modify_runtime(~S:Data,~C:Type,~V:Data,transform:C -> C & V,column:Column,index:U32,tick:Tick.Tick) -> Column & Maybe<&2,V>: 218 edit_search(~S,~C,~V,transform,15n,Visit{column,index,Root{}},tick,True{}) 219 220 # Unlike the template-specialized write operations, this removal accepts an 221 # ordinary irrelevant payload Type so a canonical heterogeneous schema fold can 222 # return every actual owner. It never grows storage and clears the same stamps 223 # as swap_at(..., None, ...), including an already absent in-range component. 224 def take_leaf_done(-S:Data,-C:Type,stamps:Array,index:U32,result:Array> & Maybe<&1,C>) -> Column & Maybe<&1,C>: 225 match result: 226 case (values,previous):(Leaf{values,Array.set(L.Stamp,stamps,index,L.Stamp{None{},None{}})},previous) 227 def take_leaf(-S:Data,-C:Type,values:Array>,stamps:Array,+index:U32,allowed:Bool) -> Column & Maybe<&1,C>: 228 match allowed: 229 case False{}:(Leaf{values,stamps},None{}) 230 case True{}:take_leaf_done(S,C,stamps,index,Array.swap(Maybe<&1,C>,values,index,None{})) 231 def take_left_done(-S:Data,-C:Type,half:U32,right:Column,result:Column & Maybe<&1,C>) -> Column & Maybe<&1,C>: 232 match result: 233 case (left,previous):(Branch{half,left,right},previous) 234 def take_right_done(-S:Data,-C:Type,half:U32,left:Column,result:Column & Maybe<&1,C>) -> Column & Maybe<&1,C>: 235 match result: 236 case (right,previous):(Branch{half,left,right},previous) 237 def take_branch(-S:Data,-C:Type,descend:Column -> U32 -> Column & Maybe<&1,C>,+half:U32,index:U32,left:Column,right:Column,first:Bool) -> Column & Maybe<&1,C>: 238 match first: 239 case True{}:take_left_done(S,C,half,right,descend(left,index)) 240 case False{}:take_right_done(S,C,half,left,descend(right,U32.sub(index,half))) 241 def take_search(-S:Data,-C:Type,fuel:Nat,column:Column,+index:U32) -> Column & Maybe<&1,C>: 242 match fuel column: 243 case 0n column:(column,None{}) 244 case 1n+_ Leaf{values,stamps}:take_leaf(S,C,values,stamps,index,U32.is_lt(index,8)) 245 case 1n+rest Branch{+half,left,right}:take_branch(S,C,(column => index => take_search(S,C,rest,column,index)),half,index,left,right,U32.is_lt(index,half)) 246 def take(-S:Data,-C:Type,column:Column,index:U32) -> Column & Maybe<&1,C>: 247 take_search(S,C,15n,column,index)