column.bend
bendvy-ecs-core@0.1.0.0 · 556 lines · 0 definitions
1import Base
2import bendvy-ecs-core@0.1.0.0/change_tick.bend as Tick
3import lifecycle.bend as L
4import owner_handoff.bend as H
5import indexed_lifecycle.bend as M
6
7# Schema provisioning owns columns. Gameplay receives abstract providers instead.
8# IDs are one-based; this bounded slice supports at most 131072 slots.
9type History<-S:Data,-C:Type> is Type:
10 HistoryNil{}
11 HistoryCon{id:U32,value:Maybe<&1,C>,rest:History<S,C>}
12type Auxiliary is Type:
13 Auxiliary{}
14type Marker is Data:
15 Marker{}
16type State<-S:Data,-C:Type> is Type:
17 State{values:Array<Maybe<&1,C>>,stamps:List<&2,L.Entry>,capacity:U32,current:U32,owner:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:History<S,C>}
18# Recursive ownership carrier prevents native union-wide field transport.
19# Every constructor owns a State, directly or through its inner carrier.
20type Carrier<-S:Data,-C:Type> is Type:
21 Owned{state:State<S,C>}
22 Wrapped{inner:Carrier<S,C>}
23type IndexedOrdinaryState<-S:Data,-C:Type> is Type:
24 IndexedOrdinaryState{values:Array<Maybe<&1,C>>,metadata:M.Metadata}
25type IndexedOrdinaryCarrier<-S:Data,-C:Type> is Type:
26 IndexedOrdinaryOwned{state:IndexedOrdinaryState<S,C>}
27 IndexedOrdinaryWrapped{inner:IndexedOrdinaryCarrier<S,C>}
28type IndexedPreparedState<-S:Data,-C:Type> is Type:
29 IndexedPreparedState{values:Array<Maybe<&1,C>>,metadata:M.Metadata,capacity:U32,current:U32,owner:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:History<S,C>}
30type IndexedPreparedCarrier<-S:Data,-C:Type> is Type:
31 IndexedPreparedOwned{state:IndexedPreparedState<S,C>}
32 IndexedPreparedWrapped{inner:IndexedPreparedCarrier<S,C>}
33# Trusted schema storage owning optional affine payloads and lifecycle data.
34# Representation variants are engine details, not additional gameplay APIs.
35# Raw column operations use slot indices and do not validate World handles;
36# applications normally use typed component/query capabilities.
37type Column<-S: Data, -C: Type> is Type:
38 Column{values: Array<Maybe<&1,C>>,stamps: List<&2,L.Entry>}
39 Prepared{state:Carrier<S,C>}
40 Indexed{state:IndexedOrdinaryCarrier<S,C>}
41 PreparedIndexed{state:IndexedPreparedCarrier<S,C>}
42def indexed_prepared_unseal(~S:Data,~C:Type,carrier:IndexedPreparedCarrier<S,C>) -> IndexedPreparedState<S,C>:
43 match carrier:
44 case IndexedPreparedOwned{state}: state
45 case IndexedPreparedWrapped{inner}: indexed_prepared_unseal(~S,~C,inner)
46def indexed_unseal(~S:Data,~C:Type,carrier:IndexedOrdinaryCarrier<S,C>) -> IndexedOrdinaryState<S,C>:
47 match carrier:
48 case IndexedOrdinaryOwned{state}: state
49 case IndexedOrdinaryWrapped{inner}: indexed_unseal(~S,~C,inner)
50def indexed_wrap(~S:Data,~C:Type,values:Array<Maybe<&1,C>>,metadata:M.Metadata) -> Column<S,C>:
51 Indexed{IndexedOrdinaryOwned{IndexedOrdinaryState{values,metadata}}}
52# Create an empty indexed column for trusted schema setup. Its layout is
53# not a component-kind restriction: C may be affine Type. No entity is spawned.
54# Example: examples/health-decay/schema.bend, empty().
55def empty_indexed(~S:Data,~C:Type) -> Column<S,C>:
56 indexed_wrap(~S,~C,ALeaf{None{}},M.empty())
57def absent(~C: Type, +depth: Nat) -> Array<Maybe<&1,C>>:
58 match depth:
59 case 0n:
60 ALeaf{None{}}
61 case 1n+rest:
62 ANode{absent(~C, rest), absent(~C, rest)}
63
64
65def indexed_grow(~S:Data,~C:Type,fuel:Nat,values:Array<Maybe<&1,C>>,metadata:M.Metadata,+size:U32,+depth:Nat,+target:U32,enough:Bool) -> Column<S,C>:
66 match fuel enough:
67 case _ True{}: indexed_wrap(~S,~C,values,metadata)
68 case 0n False{}: indexed_wrap(~S,~C,values,metadata)
69 case 1n+rest False{}:
70 +next = U32.shl(size)
71 indexed_grow(~S,~C,rest,ANode{values,absent(~C,depth)},metadata,next,1n+depth,target,U32.is_le(target,next))
72def indexed_ensure_sized(~S:Data,~C:Type,+target:U32,metadata:M.Metadata,result:Array<Maybe<&1,C>> & U32) -> Column<S,C>:
73 match result:
74 case (values,+size): indexed_grow(~S,~C,17n,values,metadata,size,U32.log2(size),target,U32.is_le(target,size))
75def indexed_ensure_state(~S:Data,~C:Type,target:U32,state:IndexedOrdinaryState<S,C>) -> Column<S,C>:
76 match state:
77 case IndexedOrdinaryState{values,metadata}: indexed_ensure_sized(~S,~C,target,metadata,Array.size(Maybe<&1,C>,values))
78def unseal(~S:Data,~C:Type,carrier:Carrier<S,C>) -> State<S,C>:
79 match carrier:
80 case Owned{state}: state
81 case Wrapped{inner}: unseal(~S,~C,inner)
82
83# Raw column replacement result. Accepted returns column and displaced
84# optional payload; Rejected returns column and incoming optional payload.
85# Neither branch provides runtime entity/world validation by itself.
86type SwapOutcome<-S: Data, -C: Type> is Type:
87 Accepted{column: Column<S,C>, previous: Maybe<&1,C>}
88 Rejected{column: Column<S,C>, incoming: Maybe<&1,C>}
89
90def indexed_swapped(~S:Data,~C:Type,metadata:M.Metadata,result:Array<Maybe<&1,C>> & Maybe<&1,C>) -> SwapOutcome<S,C>:
91 match result:
92 case (values,previous): Accepted{indexed_wrap(~S,~C,values,metadata),previous}
93def indexed_swap_checked(~S:Data,~C:Type,+id:U32,incoming:Maybe<&1,C>,metadata:M.Metadata,values:Array<Maybe<&1,C>>,valid:Bool) -> SwapOutcome<S,C>:
94 match valid:
95 case False{}: Rejected{indexed_wrap(~S,~C,values,metadata),incoming}
96 case True{}: indexed_swapped(~S,~C,metadata,Array.swap(Maybe<&1,C>,values,U32.sub(id,1),incoming))
97def indexed_swap_sized(~S:Data,~C:Type,+id:U32,incoming:Maybe<&1,C>,metadata:M.Metadata,result:Array<Maybe<&1,C>> & U32) -> SwapOutcome<S,C>:
98 match result:
99 case (values,size): indexed_swap_checked(~S,~C,id,incoming,metadata,values,U32.is_gt(id,0) && U32.is_le(id,size) && U32.is_le(id,131072))
100def indexed_swap_state(~S:Data,~C:Type,+id:U32,incoming:Maybe<&1,C>,state:IndexedOrdinaryState<S,C>) -> SwapOutcome<S,C>:
101 match state:
102 case IndexedOrdinaryState{values,metadata}: indexed_swap_sized(~S,~C,id,incoming,metadata,Array.size(Maybe<&1,C>,values))
103def indexed_view_restored(~S:Data,~C:Type,~V:Data,metadata:M.Metadata,projection:V,result:Array<Maybe<&1,C>> & Maybe<&1,C>) -> Column<S,C> & Maybe<&2,V>:
104 match result:
105 case (values,_): (indexed_wrap(~S,~C,values,metadata),Some{projection})
106def indexed_view_projected(~S:Data,~C:Type,~V:Data,+id:U32,values:Array<Maybe<&1,C>>,metadata:M.Metadata,result:C & V) -> Column<S,C> & Maybe<&2,V>:
107 match result:
108 case (owner,projection): indexed_view_restored(~S,~C,~V,metadata,projection,Array.swap(Maybe<&1,C>,values,U32.sub(id,1),Some{owner}))
109def indexed_view_taken(~S:Data,~C:Type,~V:Data,~project:C -> C & V,+id:U32,metadata:M.Metadata,result:Array<Maybe<&1,C>> & Maybe<&1,C>) -> Column<S,C> & Maybe<&2,V>:
110 match result:
111 case (values,None{}): (indexed_wrap(~S,~C,values,metadata),None{})
112 case (values,Some{owner}): indexed_view_projected(~S,~C,~V,id,values,metadata,project(owner))
113def indexed_view_checked(~S:Data,~C:Type,~V:Data,~project:C -> C & V,+id:U32,values:Array<Maybe<&1,C>>,metadata:M.Metadata,valid:Bool) -> Column<S,C> & Maybe<&2,V>:
114 match valid:
115 case False{}: (indexed_wrap(~S,~C,values,metadata),None{})
116 case True{}: indexed_view_taken(~S,~C,~V,~project,id,metadata,Array.swap(Maybe<&1,C>,values,U32.sub(id,1),None{}))
117def indexed_view_sized(~S:Data,~C:Type,~V:Data,~project:C -> C & V,+id:U32,metadata:M.Metadata,result:Array<Maybe<&1,C>> & U32) -> Column<S,C> & Maybe<&2,V>:
118 match result:
119 case (values,size): indexed_view_checked(~S,~C,~V,~project,id,values,metadata,U32.is_gt(id,0) && U32.is_le(id,size) && U32.is_le(id,131072))
120def indexed_view_state(~S:Data,~C:Type,~V:Data,~project:C -> C & V,+id:U32,state:IndexedOrdinaryState<S,C>) -> Column<S,C> & Maybe<&2,V>:
121 match state:
122 case IndexedOrdinaryState{values,metadata}: indexed_view_sized(~S,~C,~V,~project,id,metadata,Array.size(Maybe<&1,C>,values))
123def indexed_projected_state(~S:Data,~C:Type,~V:Data,+id:U32,result:C & V,state:IndexedOrdinaryState<S,C>) -> Column<S,C> & Maybe<&2,V>:
124 match state:
125 case IndexedOrdinaryState{values,metadata}: indexed_view_projected(~S,~C,~V,id,values,metadata,result)
126def indexed_lifecycle_got(~S:Data,~C:Type,values:Array<Maybe<&1,C>>,result:M.Metadata & L.Stamp) -> Column<S,C> & L.Stamp:
127 match result:
128 case (metadata,stamp): (indexed_wrap(~S,~C,values,metadata),stamp)
129def indexed_lifecycle_state(~S:Data,~C:Type,+id:U32,state:IndexedOrdinaryState<S,C>) -> Column<S,C> & L.Stamp:
130 match state:
131 case IndexedOrdinaryState{values,metadata}: indexed_lifecycle_got(~S,~C,values,M.get(metadata,id))
132def indexed_restore_state(~S:Data,~C:Type,+id:U32,stamp:L.Stamp,state:IndexedOrdinaryState<S,C>) -> Column<S,C>:
133 match state:
134 case IndexedOrdinaryState{values,metadata}: indexed_wrap(~S,~C,values,M.set(metadata,id,stamp))
135def indexed_mark_got(~S:Data,~C:Type,+id:U32,incoming:Bool,wasPresent:Bool,tick:Tick.Tick,values:Array<Maybe<&1,C>>,result:M.Metadata & L.Stamp) -> Column<S,C>:
136 match result:
137 case (metadata,stamp): indexed_wrap(~S,~C,values,M.set(metadata,id,L.after_write(incoming,wasPresent,stamp,tick)))
138def indexed_mark_state(~S:Data,~C:Type,+id:U32,incoming:Bool,wasPresent:Bool,tick:Tick.Tick,state:IndexedOrdinaryState<S,C>) -> Column<S,C>:
139 match state:
140 case IndexedOrdinaryState{values,metadata}: indexed_mark_got(~S,~C,id,incoming,wasPresent,tick,values,M.get(metadata,id))
141def indexed_clear_state(~S:Data,~C:Type,+id:U32,state:IndexedOrdinaryState<S,C>) -> Column<S,C>:
142 match state:
143 case IndexedOrdinaryState{values,metadata}: indexed_wrap(~S,~C,values,M.clear(metadata,id))
144
145# Create an empty trusted schema column without component payloads.
146def empty(~S: Data, ~C: Type) -> Column<S,C>:
147 Column{ALeaf{None{}},[]}
148
149def grow(~S: Data, ~C: Type, fuel: Nat, values: Array<Maybe<&1,C>>, +stamps: List<&2,L.Entry>, +size: U32, +depth: Nat, +target: U32, enough: Bool) -> Column<S,C>:
150 match fuel enough:
151 case _ True{}:
152 Column{values,stamps}
153 case 0n False{}:
154 Column{values,stamps}
155 case 1n+rest False{}:
156 +next = U32.shl(size)
157 grow(~S, ~C, rest, ANode{values, absent(~C, depth)}, stamps, next, 1n+depth, target, U32.is_le(target, next))
158
159def ensure_sized(~S: Data, ~C: Type, +target: U32, +stamps: List<&2,L.Entry>, sized: Array<Maybe<&1,C>> & U32) -> Column<S,C>:
160 (values, +size) = sized
161 grow(~S, ~C, 17n, values, stamps, size, U32.log2(size), target, U32.is_le(target, size))
162
163# Recovery completes every evacuated owner before ordinary-array fallback.
164def recover_past(~S:Data,~C:Type,past:History<S,C>,values:Array<Maybe<&1,C>>) -> Array<Maybe<&1,C>>:
165 match past:
166 case HistoryNil{}: values
167 case HistoryCon{+id,owner,rest}: recover_past(~S,~C,rest,Array.set(Maybe<&1,C>,values,U32.sub(id,1),owner))
168def recover_remaining(~S:Data,~C:Type,stamps:List<&2,L.Entry>,result:Array<Maybe<&1,C>> & List<&2,U32>) -> Column<S,C>:
169 match result:
170 case (values,_): Column{values,stamps}
171# Partial evaluation of selected recovery's unused ID-list projection.
172# Actual affine owners and ascending Array.set writes are unchanged.
173def recover_selected_rows(-S:Data,-C:Type,rows:H.PrototypeHandoffRows<S,C>,values:Array<Maybe<&1,C>>) -> Array<Maybe<&1,C>>:
174 match rows:
175 case H.HandoffNil{}: values
176 case H.HandoffCon{+id,owner,rest}: recover_selected_rows(S,C,rest,Array.set(Maybe<&1,C>,values,U32.sub(id,1),Some{owner}))
177def recover_current(~S:Data,~C:Type,values:Array<Maybe<&1,C>>,+stamps:List<&2,L.Entry>,+current:U32,owner:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:History<S,C>,active:Bool) -> Column<S,C>:
178 match active:
179 case False{}: Column{recover_selected_rows(S,C,remaining,recover_past(~S,~C,past,values)),stamps}
180 case True{}: Column{recover_selected_rows(S,C,remaining,recover_past(~S,~C,past,Array.set(Maybe<&1,C>,values,U32.sub(current,1),owner))),stamps}
181def indexed_recover_current(~S:Data,~C:Type,values:Array<Maybe<&1,C>>,metadata:M.Metadata,+current:U32,owner:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:History<S,C>,active:Bool) -> Column<S,C>:
182 match active:
183 case False{}: indexed_wrap(~S,~C,recover_selected_rows(S,C,remaining,recover_past(~S,~C,past,values)),metadata)
184 case True{}: indexed_wrap(~S,~C,recover_selected_rows(S,C,remaining,recover_past(~S,~C,past,Array.set(Maybe<&1,C>,values,U32.sub(current,1),owner))),metadata)
185def recover_state(~S:Data,~C:Type,state:State<S,C>) -> Column<S,C>:
186 match state:
187 case State{values,stamps,_,+current,owner,remaining,past}: recover_current(~S,~C,values,stamps,current,owner,remaining,past,U32.is_gt(current,0))
188def indexed_recover_state(~S:Data,~C:Type,state:IndexedPreparedState<S,C>) -> Column<S,C>:
189 match state:
190 case IndexedPreparedState{values,metadata,_,+current,owner,remaining,past}: indexed_recover_current(~S,~C,values,metadata,current,owner,remaining,past,U32.is_gt(current,0))
191def recover(~S:Data,~C:Type,column:Column<S,C>) -> Column<S,C>:
192 match column:
193 case Column{values,stamps}: Column{values,stamps}
194 case Prepared{carrier}: recover_state(~S,~C,unseal(~S,~C,carrier))
195 case Indexed{carrier}: Indexed{carrier}
196 case PreparedIndexed{carrier}: indexed_recover_state(~S,~C,indexed_prepared_unseal(~S,~C,carrier))
197def prepared_return(~S:Data,~C:Type,stamps:List<&2,L.Entry>,capacity:U32,result:H.Rows<C,Auxiliary,Marker> & H.PrototypeHandoffRows<S,C>) -> Column<S,C>:
198 match result:
199 case (H.Rows{values,_,_,_,_,_},rows): Prepared{Owned{State{values,stamps,capacity,0,None{},rows,HistoryNil{}}}}
200# Source partial evaluation of exact selected Required/all-live handoff producer.
201# Every physical index is in bounds; synthetic Aux/flags/stamps were unused.
202type EvacuationPhase<-S:Data,-C:Type> is Type:
203 Fetch{fuel:Nat,id:U32,values:Array<Maybe<&1,C>>,rows:H.PrototypeHandoffRows<S,C>}
204 Taken{fuel:Nat,id:U32,rows:H.PrototypeHandoffRows<S,C>,result:Array<Maybe<&1,C>> & Maybe<&1,C>}
205def evacuate_phase(~S:Data,~C:Type,gas:Nat,phase:EvacuationPhase<S,C>) -> Array<Maybe<&1,C>> & H.PrototypeHandoffRows<S,C>:
206 match gas phase:
207 case _ Fetch{0n,_,values,rows}: (values,rows)
208 case 0n Fetch{_,_,values,rows}: (values,rows)
209 case 0n Taken{_,_,rows,(values,None{})}: (values,rows)
210 case 0n Taken{_,id,rows,(values,Some{owner})}: (values,H.HandoffCon{id,owner,rows})
211 case 1n+more Fetch{1n+rest,+id,values,rows}: evacuate_phase(~S,~C,more,Taken{rest,id,rows,Array.swap(Maybe<&1,C>,values,U32.sub(id,1),None{})})
212 case 1n+more Taken{fuel,+id,rows,(values,None{})}: evacuate_phase(~S,~C,more,Fetch{fuel,U32.sub(id,1),values,rows})
213 case 1n+more Taken{fuel,+id,rows,(values,Some{owner})}: evacuate_phase(~S,~C,more,Fetch{fuel,U32.sub(id,1),values,H.HandoffCon{id,owner,rows}})
214# The pending swap tuple is already fetched; zero fuel still moves that owner.
215def evacuate_pending(~S:Data,~C:Type,fuel:Nat,+id:U32,rows:H.PrototypeHandoffRows<S,C>,observed:Array<Maybe<&1,C>> & Maybe<&1,C>) -> Array<Maybe<&1,C>> & H.PrototypeHandoffRows<S,C>:
216 match fuel observed:
217 case 0n, (values,None{}): (values,rows)
218 case 0n, (values,Some{owner}): (values,H.HandoffCon{id,owner,rows})
219 case 1n+rest, (values,None{}):
220 +nextId = U32.sub(id,1)
221 evacuate_pending(~S,~C,rest,nextId,rows,Array.swap(Maybe<&1,C>,values,U32.sub(nextId,1),None{}))
222 case 1n+rest, (values,Some{owner}):
223 +nextId = U32.sub(id,1)
224 evacuate_pending(~S,~C,rest,nextId,H.HandoffCon{id,owner,rows},Array.swap(Maybe<&1,C>,values,U32.sub(nextId,1),None{}))
225def evacuate_start(~S:Data,~C:Type,fuel:Nat,+id:U32,values:Array<Maybe<&1,C>>,rows:H.PrototypeHandoffRows<S,C>) -> Array<Maybe<&1,C>> & H.PrototypeHandoffRows<S,C>:
226 evacuate_pending(~S,~C,fuel,id,rows,Array.swap(Maybe<&1,C>,values,U32.sub(id,1),None{}))
227# Keep the exact original exported reusable-fuel/affine-ID function type.
228def evacuate(~S:Data,~C:Type,+fuel:Nat,id:U32,values:Array<Maybe<&1,C>>,rows:H.PrototypeHandoffRows<S,C>) -> Array<Maybe<&1,C>> & H.PrototypeHandoffRows<S,C>:
229 match fuel:
230 case 0n: (values,rows)
231 case 1n+rest: evacuate_start(~S,~C,rest,id,values,rows)
232def prepared_evacuated(~S:Data,~C:Type,stamps:List<&2,L.Entry>,capacity:U32,result:Array<Maybe<&1,C>> & H.PrototypeHandoffRows<S,C>) -> Column<S,C>:
233 match result:
234 case (values,rows): Prepared{Owned{State{values,stamps,capacity,0,None{},rows,HistoryNil{}}}}
235def indexed_prepared_evacuated(~S:Data,~C:Type,metadata:M.Metadata,capacity:U32,result:Array<Maybe<&1,C>> & H.PrototypeHandoffRows<S,C>) -> Column<S,C>:
236 match result:
237 case (values,rows): PreparedIndexed{IndexedPreparedOwned{IndexedPreparedState{values,metadata,capacity,0,None{},rows,HistoryNil{}}}}
238def prepare_sized(~S:Data,~C:Type,+stamps:List<&2,L.Entry>,result:Array<Maybe<&1,C>> & U32) -> Column<S,C>:
239 match result:
240 case (values,+size): prepared_evacuated(~S,~C,stamps,size,evacuate(~S,~C,U32.to_nat(size),size,values,H.HandoffNil{}))
241def indexed_prepare_sized(~S:Data,~C:Type,metadata:M.Metadata,result:Array<Maybe<&1,C>> & U32) -> Column<S,C>:
242 match result:
243 case (values,+size): indexed_prepared_evacuated(~S,~C,metadata,size,evacuate(~S,~C,U32.to_nat(size),size,values,H.HandoffNil{}))
244def indexed_prepare_state(~S:Data,~C:Type,state:IndexedOrdinaryState<S,C>) -> Column<S,C>:
245 match state:
246 case IndexedOrdinaryState{values,metadata}: indexed_prepare_sized(~S,~C,metadata,Array.size(Maybe<&1,C>,values))
247def prepare(~S:Data,~C:Type,column:Column<S,C>) -> Column<S,C>:
248 match column:
249 case Column{values,stamps}: prepare_sized(~S,~C,stamps,Array.size(Maybe<&1,C>,values))
250 case Prepared{carrier}: Prepared{carrier}
251 case Indexed{carrier}: indexed_prepare_state(~S,~C,indexed_unseal(~S,~C,carrier))
252 case PreparedIndexed{carrier}: PreparedIndexed{carrier}
253
254def ensure_recovered(~S:Data,~C:Type,target:U32,column:Column<S,C>) -> Column<S,C>:
255 match column:
256 case Column{values,stamps}: ensure_sized(~S,~C,target,stamps,Array.size(Maybe<&1,C>,values))
257 case Indexed{carrier}: indexed_ensure_state(~S,~C,target,indexed_unseal(~S,~C,carrier))
258 case other: other
259def ensure_prepared(~S:Data,~C:Type,+target:U32,column:Column<S,C>,fits:Bool) -> Column<S,C>:
260 match fits:
261 case True{}: column
262 case False{}: ensure_recovered(~S,~C,target,recover(~S,~C,column))
263
264def ensure_state(~S:Data,~C:Type,+target:U32,state:State<S,C>) -> Column<S,C>:
265 match state:
266 case State{values,stamps,+capacity,current,owner,remaining,past}: ensure_prepared(~S,~C,target,Prepared{Owned{State{values,stamps,capacity,current,owner,remaining,past}}},U32.is_le(target,capacity))
267def indexed_prepared_ensure_state(~S:Data,~C:Type,+target:U32,state:IndexedPreparedState<S,C>) -> Column<S,C>:
268 match state:
269 case IndexedPreparedState{values,metadata,+capacity,current,owner,remaining,past}: ensure_prepared(~S,~C,target,PreparedIndexed{IndexedPreparedOwned{IndexedPreparedState{values,metadata,capacity,current,owner,remaining,past}}},U32.is_le(target,capacity))
270def ensure_checked(~S: Data, ~C: Type, column: Column<S,C>, +target: U32, valid: Bool) -> Column<S,C>:
271 match column valid:
272 case _ False{}:
273 column
274 case Column{values,stamps} True{}:
275 ensure_sized(~S, ~C, target, stamps, Array.size(Maybe<&1,C>, values))
276 case Prepared{carrier} True{}: ensure_state(~S,~C,target,unseal(~S,~C,carrier))
277 case Indexed{carrier} True{}: indexed_ensure_state(~S,~C,target,indexed_unseal(~S,~C,carrier))
278 case PreparedIndexed{carrier} True{}: indexed_prepared_ensure_state(~S,~C,target,indexed_prepared_unseal(~S,~C,carrier))
279
280def ensure(~S: Data, ~C: Type, column: Column<S,C>, +target: U32) -> Column<S,C>:
281 ensure_checked(~S, ~C, column, target, U32.is_gt(target, 0) && U32.is_le(target, 131072))
282
283def swapped(~S: Data, ~C: Type, result: Array<Maybe<&1,C>> & Maybe<&1,C>,stamps: List<&2,L.Entry>) -> SwapOutcome<S,C>:
284 (values, previous) = result
285 Accepted{Column{values,stamps}, previous}
286
287def swap_checked(~S: Data, ~C: Type, values: Array<Maybe<&1,C>>,stamps: List<&2,L.Entry>, id: U32, incoming: Maybe<&1,C>, valid: Bool) -> SwapOutcome<S,C>:
288 match valid:
289 case False{}:
290 Rejected{Column{values,stamps}, incoming}
291 case True{}:
292 swapped(~S, ~C, Array.swap(Maybe<&1,C>, values, U32.sub(id, 1), incoming),stamps)
293
294def swap_sized(~S: Data, ~C: Type, +id: U32, incoming: Maybe<&1,C>, stamps: List<&2,L.Entry>, sized: Array<Maybe<&1,C>> & U32) -> SwapOutcome<S,C>:
295 (values, size) = sized
296 swap_checked(~S, ~C, values, stamps, id, incoming, U32.is_gt(id, 0) && U32.is_le(id, size) && U32.is_le(id, 131072))
297
298def past_current(~S:Data,~C:Type,current:U32,owner:Maybe<&1,C>,past:History<S,C>,active:Bool) -> History<S,C>:
299 match active:
300 case False{}: past
301 case True{}: HistoryCon{current,owner,past}
302type SeekPhase is Data:
303 Inspect{}
304 Choice{equal:Bool,before:Bool}
305def seek(~S:Data,~C:Type,fuel:Nat,values:Array<Maybe<&1,C>>,stamps:List<&2,L.Entry>,capacity:U32,+target:U32,incoming:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:History<S,C>,phase:SeekPhase) -> SwapOutcome<S,C>:
306 match fuel remaining phase:
307 case _ H.HandoffNil{} _: Accepted{Prepared{Owned{State{values,stamps,capacity,target,incoming,H.HandoffNil{},past}}},None{}}
308 case 0n H.HandoffCon{id,owner,rest} _: Rejected{Prepared{Owned{State{values,stamps,capacity,0,None{},H.HandoffCon{id,owner,rest},past}}},incoming}
309 case 1n+more H.HandoffCon{+id,owner,rest} Inspect{}: seek(~S,~C,more,values,stamps,capacity,target,incoming,H.HandoffCon{id,owner,rest},past,Choice{U32.is_eq(target,id),U32.is_lt(target,id)})
310 case 1n+more H.HandoffCon{id,owner,rest} Choice{True{},_}: Accepted{Prepared{Owned{State{values,stamps,capacity,target,incoming,rest,past}}},Some{owner}}
311 case 1n+more H.HandoffCon{id,owner,rest} Choice{False{},True{}}: Accepted{Prepared{Owned{State{values,stamps,capacity,target,incoming,H.HandoffCon{id,owner,rest},past}}},None{}}
312 case 1n+more H.HandoffCon{id,owner,rest} Choice{False{},False{}}: seek(~S,~C,more,values,stamps,capacity,target,incoming,rest,HistoryCon{id,Some{owner},past},Inspect{})
313def indexed_seek(~S:Data,~C:Type,fuel:Nat,values:Array<Maybe<&1,C>>,metadata:M.Metadata,capacity:U32,+target:U32,incoming:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:History<S,C>,phase:SeekPhase) -> SwapOutcome<S,C>:
314 match fuel remaining phase:
315 case _ H.HandoffNil{} _: Accepted{PreparedIndexed{IndexedPreparedOwned{IndexedPreparedState{values,metadata,capacity,target,incoming,H.HandoffNil{},past}}},None{}}
316 case 0n H.HandoffCon{id,owner,rest} _: Rejected{PreparedIndexed{IndexedPreparedOwned{IndexedPreparedState{values,metadata,capacity,0,None{},H.HandoffCon{id,owner,rest},past}}},incoming}
317 case 1n+more H.HandoffCon{+id,owner,rest} Inspect{}: indexed_seek(~S,~C,more,values,metadata,capacity,target,incoming,H.HandoffCon{id,owner,rest},past,Choice{U32.is_eq(target,id),U32.is_lt(target,id)})
318 case 1n+more H.HandoffCon{id,owner,rest} Choice{True{},_}: Accepted{PreparedIndexed{IndexedPreparedOwned{IndexedPreparedState{values,metadata,capacity,target,incoming,rest,past}}},Some{owner}}
319 case 1n+more H.HandoffCon{id,owner,rest} Choice{False{},True{}}: Accepted{PreparedIndexed{IndexedPreparedOwned{IndexedPreparedState{values,metadata,capacity,target,incoming,H.HandoffCon{id,owner,rest},past}}},None{}}
320 case 1n+more H.HandoffCon{id,owner,rest} Choice{False{},False{}}: indexed_seek(~S,~C,more,values,metadata,capacity,target,incoming,rest,HistoryCon{id,Some{owner},past},Inspect{})
321def swap_recovered(~S:Data,~C:Type,+id:U32,incoming:Maybe<&1,C>,column:Column<S,C>) -> SwapOutcome<S,C>:
322 match column:
323 case Column{values,stamps}: swap_sized(~S,~C,id,incoming,stamps,Array.size(Maybe<&1,C>,values))
324 case Indexed{carrier}: indexed_swap_state(~S,~C,id,incoming,indexed_unseal(~S,~C,carrier))
325 case other: Rejected{other,incoming}
326def prepared_swap(~S:Data,~C:Type,values:Array<Maybe<&1,C>>,stamps:List<&2,L.Entry>,+capacity:U32,+current:U32,owner:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:History<S,C>,+id:U32,incoming:Maybe<&1,C>,valid:Bool,same:Bool,backwards:Bool) -> SwapOutcome<S,C>:
327 match valid same backwards:
328 case False{} _ _: Rejected{Prepared{Owned{State{values,stamps,capacity,current,owner,remaining,past}}},incoming}
329 case True{} True{} _: Accepted{Prepared{Owned{State{values,stamps,capacity,current,incoming,remaining,past}}},owner}
330 case True{} False{} True{}: swap_recovered(~S,~C,id,incoming,recover(~S,~C,Prepared{Owned{State{values,stamps,capacity,current,owner,remaining,past}}}))
331 case True{} False{} False{}: seek(~S,~C,U32.to_nat(U32.add(U32.add(capacity,capacity),1)),values,stamps,capacity,id,incoming,remaining,past_current(~S,~C,current,owner,past,U32.is_gt(current,0)),Inspect{})
332def indexed_prepared_swap(~S:Data,~C:Type,values:Array<Maybe<&1,C>>,metadata:M.Metadata,+capacity:U32,+current:U32,owner:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:History<S,C>,+id:U32,incoming:Maybe<&1,C>,valid:Bool,same:Bool,backwards:Bool) -> SwapOutcome<S,C>:
333 match valid same backwards:
334 case False{} _ _: Rejected{PreparedIndexed{IndexedPreparedOwned{IndexedPreparedState{values,metadata,capacity,current,owner,remaining,past}}},incoming}
335 case True{} True{} _: Accepted{PreparedIndexed{IndexedPreparedOwned{IndexedPreparedState{values,metadata,capacity,current,incoming,remaining,past}}},owner}
336 case True{} False{} True{}: swap_recovered(~S,~C,id,incoming,recover(~S,~C,PreparedIndexed{IndexedPreparedOwned{IndexedPreparedState{values,metadata,capacity,current,owner,remaining,past}}}))
337 case True{} False{} False{}: indexed_seek(~S,~C,U32.to_nat(U32.add(U32.add(capacity,capacity),1)),values,metadata,capacity,id,incoming,remaining,past_current(~S,~C,current,owner,past,U32.is_gt(current,0)),Inspect{})
338def swap_state(~S:Data,~C:Type,+id:U32,incoming:Maybe<&1,C>,state:State<S,C>) -> SwapOutcome<S,C>:
339 match state:
340 case State{values,stamps,+capacity,+current,owner,remaining,past}: prepared_swap(~S,~C,values,stamps,capacity,current,owner,remaining,past,id,incoming,U32.is_gt(id,0) && U32.is_le(id,capacity),U32.is_eq(id,current),U32.is_lt(id,current))
341def indexed_prepared_swap_state(~S:Data,~C:Type,+id:U32,incoming:Maybe<&1,C>,state:IndexedPreparedState<S,C>) -> SwapOutcome<S,C>:
342 match state:
343 case IndexedPreparedState{values,metadata,+capacity,+current,owner,remaining,past}: indexed_prepared_swap(~S,~C,values,metadata,capacity,current,owner,remaining,past,id,incoming,U32.is_gt(id,0) && U32.is_le(id,capacity),U32.is_eq(id,current),U32.is_lt(id,current))
344def swap(~S: Data, ~C: Type, column: Column<S,C>, +id: U32, incoming: Maybe<&1,C>) -> SwapOutcome<S,C>:
345 match column:
346 case Column{values,stamps}: swap_sized(~S,~C,id,incoming,stamps,Array.size(Maybe<&1,C>,values))
347 case Prepared{carrier}: swap_state(~S,~C,id,incoming,unseal(~S,~C,carrier))
348 case Indexed{carrier}: indexed_swap_state(~S,~C,id,incoming,indexed_unseal(~S,~C,carrier))
349 case PreparedIndexed{carrier}: indexed_prepared_swap_state(~S,~C,id,incoming,indexed_prepared_unseal(~S,~C,carrier))
350
351def remove(~S: Data, ~C: Type, column: Column<S,C>, id: U32) -> SwapOutcome<S,C>:
352 swap(~S, ~C, column, id, None{})
353
354def restored(~S: Data, ~C: Type, ~V: Data, result: Array<Maybe<&1,C>> & Maybe<&1,C>, projection: V,stamps: List<&2,L.Entry>) -> Column<S,C> & Maybe<&2,V>:
355 (values, none) = result
356 (Column{values,stamps}, Some{projection})
357
358def viewed_return(~S:Data,~C:Type,~V:Data,view:V,result:SwapOutcome<S,C>) -> Column<S,C> & Maybe<&2,V>:
359 match result:
360 case Accepted{column,_}: (column,Some{view})
361 case Rejected{column,_}: (column,None{})
362def viewed(~S: Data, ~C: Type, ~V: Data, projected: C & V, column: Column<S,C>, id: U32) -> Column<S,C> & Maybe<&2,V>:
363 match projected column:
364 case (owner,result) Column{values,stamps}: restored(~S,~C,~V,Array.swap(Maybe<&1,C>,values,U32.sub(id,1),Some{owner}),result,stamps)
365 case (owner,result) Prepared{carrier}: viewed_return(~S,~C,~V,result,swap(~S,~C,Prepared{carrier},id,Some{owner}))
366 case (owner,result) Indexed{carrier}: indexed_projected_state(~S,~C,~V,id,(owner,result),indexed_unseal(~S,~C,carrier))
367 case (owner,result) PreparedIndexed{carrier}: viewed_return(~S,~C,~V,result,swap(~S,~C,PreparedIndexed{carrier},id,Some{owner}))
368
369def view_taken(~S: Data, ~C: Type, ~V: Data, ~project: C -> C & V, id: U32, outcome: SwapOutcome<S,C>) -> Column<S,C> & Maybe<&2,V>:
370 match outcome:
371 case Rejected{column, incoming}:
372 (column, None{})
373 case Accepted{column, None{}}:
374 (column, None{})
375 case Accepted{column, Some{owner}}:
376 viewed(~S, ~C, ~V, project(owner), column, id)
377
378# Ordinary columns retain direct affine Array projection/restoration. Preparing
379# is opt-in; unused prepared storage must not add temporary swap-owner transport.
380def plain_view_projected(~S:Data,~C:Type,~V:Data,values:Array<Maybe<&1,C>>,stamps:List<&2,L.Entry>,id:U32,result:C & V) -> Column<S,C> & Maybe<&2,V>:
381 match result:
382 case (owner,projection): (Column{Array.set(Maybe<&1,C>,values,U32.sub(id,1),Some{owner}),stamps},Some{projection})
383def plain_view_taken(~S:Data,~C:Type,~V:Data,~project:C -> C & V,stamps:List<&2,L.Entry>,id:U32,result:Array<Maybe<&1,C>> & Maybe<&1,C>) -> Column<S,C> & Maybe<&2,V>:
384 match result:
385 case (values,None{}): (Column{values,stamps},None{})
386 case (values,Some{owner}): plain_view_projected(~S,~C,~V,values,stamps,id,project(owner))
387def plain_view_checked(~S:Data,~C:Type,~V:Data,~project:C -> C & V,values:Array<Maybe<&1,C>>,stamps:List<&2,L.Entry>,+id:U32,valid:Bool) -> Column<S,C> & Maybe<&2,V>:
388 match valid:
389 case False{}: (Column{values,stamps},None{})
390 case True{}: plain_view_taken(~S,~C,~V,~project,stamps,id,Array.swap(Maybe<&1,C>,values,U32.sub(id,1),None{}))
391def plain_view_sized(~S:Data,~C:Type,~V:Data,~project:C -> C & V,+id:U32,stamps:List<&2,L.Entry>,result:Array<Maybe<&1,C>> & U32) -> Column<S,C> & Maybe<&2,V>:
392 match result:
393 case (values,size): plain_view_checked(~S,~C,~V,~project,values,stamps,id,U32.is_gt(id,0) && U32.is_le(id,size) && U32.is_le(id,131072))
394def prepared_view_projected(~S:Data,~C:Type,~V:Data,values:Array<Maybe<&1,C>>,stamps:List<&2,L.Entry>,capacity:U32,current:U32,remaining:H.PrototypeHandoffRows<S,C>,past:History<S,C>,result:C & V) -> Column<S,C> & Maybe<&2,V>:
395 match result:
396 case (owner,projection): (Prepared{Owned{State{values,stamps,capacity,current,Some{owner},remaining,past}}},Some{projection})
397def indexed_prepared_view_projected(~S:Data,~C:Type,~V:Data,values:Array<Maybe<&1,C>>,metadata:M.Metadata,capacity:U32,current:U32,remaining:H.PrototypeHandoffRows<S,C>,past:History<S,C>,result:C & V) -> Column<S,C> & Maybe<&2,V>:
398 match result:
399 case (owner,projection): (PreparedIndexed{IndexedPreparedOwned{IndexedPreparedState{values,metadata,capacity,current,Some{owner},remaining,past}}},Some{projection})
400def prepared_view_current(~S:Data,~C:Type,~V:Data,~project:C -> C & V,values:Array<Maybe<&1,C>>,stamps:List<&2,L.Entry>,capacity:U32,current:U32,owner:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:History<S,C>) -> Column<S,C> & Maybe<&2,V>:
401 match owner:
402 case None{}: (Prepared{Owned{State{values,stamps,capacity,current,None{},remaining,past}}},None{})
403 case Some{owned}: prepared_view_projected(~S,~C,~V,values,stamps,capacity,current,remaining,past,project(owned))
404def indexed_prepared_view_current(~S:Data,~C:Type,~V:Data,~project:C -> C & V,values:Array<Maybe<&1,C>>,metadata:M.Metadata,capacity:U32,current:U32,owner:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:History<S,C>) -> Column<S,C> & Maybe<&2,V>:
405 match owner:
406 case None{}: (PreparedIndexed{IndexedPreparedOwned{IndexedPreparedState{values,metadata,capacity,current,None{},remaining,past}}},None{})
407 case Some{owned}: indexed_prepared_view_projected(~S,~C,~V,values,metadata,capacity,current,remaining,past,project(owned))
408def prepared_view_taken_state(~S:Data,~C:Type,~V:Data,~project:C -> C & V,owner:C,state:State<S,C>) -> Column<S,C> & Maybe<&2,V>:
409 match state:
410 case State{values,stamps,capacity,current,_,remaining,past}: prepared_view_projected(~S,~C,~V,values,stamps,capacity,current,remaining,past,project(owner))
411def indexed_prepared_view_taken_state(~S:Data,~C:Type,~V:Data,~project:C -> C & V,owner:C,state:IndexedPreparedState<S,C>) -> Column<S,C> & Maybe<&2,V>:
412 match state:
413 case IndexedPreparedState{values,metadata,capacity,current,_,remaining,past}: indexed_prepared_view_projected(~S,~C,~V,values,metadata,capacity,current,remaining,past,project(owner))
414def prepared_view_taken(~S:Data,~C:Type,~V:Data,~project:C -> C & V,id:U32,result:SwapOutcome<S,C>) -> Column<S,C> & Maybe<&2,V>:
415 match result:
416 case Rejected{column,_}: (column,None{})
417 case Accepted{column,None{}}: (column,None{})
418 case Accepted{Column{values,stamps},Some{owner}}: viewed(~S,~C,~V,project(owner),Column{values,stamps},id)
419 case Accepted{Prepared{carrier},Some{owner}}: prepared_view_taken_state(~S,~C,~V,~project,owner,unseal(~S,~C,carrier))
420 case Accepted{Indexed{carrier},Some{owner}}: indexed_projected_state(~S,~C,~V,id,project(owner),indexed_unseal(~S,~C,carrier))
421 case Accepted{PreparedIndexed{carrier},Some{owner}}: indexed_prepared_view_taken_state(~S,~C,~V,~project,owner,indexed_prepared_unseal(~S,~C,carrier))
422# Read terminals project the actual row owner before constructing its carrier.
423# Writer seek and the public low-fuel API remain unchanged.
424def seek_view(~S:Data,~C:Type,~V:Data,~project:C -> C & V,fuel:Nat,values:Array<Maybe<&1,C>>,stamps:List<&2,L.Entry>,capacity:U32,+target:U32,remaining:H.PrototypeHandoffRows<S,C>,past:History<S,C>,phase:SeekPhase) -> Column<S,C> & Maybe<&2,V>:
425 match fuel remaining phase:
426 case _ H.HandoffNil{} _: (Prepared{Owned{State{values,stamps,capacity,target,None{},H.HandoffNil{},past}}},None{})
427 case 0n H.HandoffCon{id,owner,rest} _: (Prepared{Owned{State{values,stamps,capacity,0,None{},H.HandoffCon{id,owner,rest},past}}},None{})
428 case 1n+more H.HandoffCon{+id,owner,rest} Inspect{}: seek_view(~S,~C,~V,~project,more,values,stamps,capacity,target,H.HandoffCon{id,owner,rest},past,Choice{U32.is_eq(target,id),U32.is_lt(target,id)})
429 case 1n+more H.HandoffCon{id,owner,rest} Choice{True{},_}: prepared_view_projected(~S,~C,~V,values,stamps,capacity,target,rest,past,project(owner))
430 case 1n+more H.HandoffCon{id,owner,rest} Choice{False{},True{}}: (Prepared{Owned{State{values,stamps,capacity,target,None{},H.HandoffCon{id,owner,rest},past}}},None{})
431 case 1n+more H.HandoffCon{id,owner,rest} Choice{False{},False{}}: seek_view(~S,~C,~V,~project,more,values,stamps,capacity,target,rest,HistoryCon{id,Some{owner},past},Inspect{})
432def indexed_seek_view(~S:Data,~C:Type,~V:Data,~project:C -> C & V,fuel:Nat,values:Array<Maybe<&1,C>>,metadata:M.Metadata,capacity:U32,+target:U32,remaining:H.PrototypeHandoffRows<S,C>,past:History<S,C>,phase:SeekPhase) -> Column<S,C> & Maybe<&2,V>:
433 match fuel remaining phase:
434 case _ H.HandoffNil{} _: (PreparedIndexed{IndexedPreparedOwned{IndexedPreparedState{values,metadata,capacity,target,None{},H.HandoffNil{},past}}},None{})
435 case 0n H.HandoffCon{id,owner,rest} _: (PreparedIndexed{IndexedPreparedOwned{IndexedPreparedState{values,metadata,capacity,0,None{},H.HandoffCon{id,owner,rest},past}}},None{})
436 case 1n+more H.HandoffCon{+id,owner,rest} Inspect{}: indexed_seek_view(~S,~C,~V,~project,more,values,metadata,capacity,target,H.HandoffCon{id,owner,rest},past,Choice{U32.is_eq(target,id),U32.is_lt(target,id)})
437 case 1n+more H.HandoffCon{id,owner,rest} Choice{True{},_}: indexed_prepared_view_projected(~S,~C,~V,values,metadata,capacity,target,rest,past,project(owner))
438 case 1n+more H.HandoffCon{id,owner,rest} Choice{False{},True{}}: (PreparedIndexed{IndexedPreparedOwned{IndexedPreparedState{values,metadata,capacity,target,None{},H.HandoffCon{id,owner,rest},past}}},None{})
439 case 1n+more H.HandoffCon{id,owner,rest} Choice{False{},False{}}: indexed_seek_view(~S,~C,~V,~project,more,values,metadata,capacity,target,rest,HistoryCon{id,Some{owner},past},Inspect{})
440def prepared_view_different(~S:Data,~C:Type,~V:Data,~project:C -> C & V,+id:U32,values:Array<Maybe<&1,C>>,stamps:List<&2,L.Entry>,+capacity:U32,+current:U32,owner:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:History<S,C>,backwards:Bool) -> Column<S,C> & Maybe<&2,V>:
441 match backwards:
442 case True{}: view_taken(~S,~C,~V,~project,id,swap_recovered(~S,~C,id,None{},recover_current(~S,~C,values,stamps,current,owner,remaining,past,U32.is_gt(current,0))))
443 case False{}: seek_view(~S,~C,~V,~project,U32.to_nat(U32.add(U32.add(capacity,capacity),1)),values,stamps,capacity,id,remaining,past_current(~S,~C,current,owner,past,U32.is_gt(current,0)),Inspect{})
444def indexed_prepared_view_different(~S:Data,~C:Type,~V:Data,~project:C -> C & V,+id:U32,values:Array<Maybe<&1,C>>,metadata:M.Metadata,+capacity:U32,+current:U32,owner:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:History<S,C>,backwards:Bool) -> Column<S,C> & Maybe<&2,V>:
445 match backwards:
446 case True{}: view_taken(~S,~C,~V,~project,id,swap_recovered(~S,~C,id,None{},indexed_recover_current(~S,~C,values,metadata,current,owner,remaining,past,U32.is_gt(current,0))))
447 case False{}: indexed_seek_view(~S,~C,~V,~project,U32.to_nat(U32.add(U32.add(capacity,capacity),1)),values,metadata,capacity,id,remaining,past_current(~S,~C,current,owner,past,U32.is_gt(current,0)),Inspect{})
448def prepared_view_checked(~S:Data,~C:Type,~V:Data,~project:C -> C & V,+id:U32,values:Array<Maybe<&1,C>>,stamps:List<&2,L.Entry>,+capacity:U32,+current:U32,owner:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:History<S,C>,valid:Bool,same:Bool) -> Column<S,C> & Maybe<&2,V>:
449 match valid same:
450 case False{} _: (Prepared{Owned{State{values,stamps,capacity,current,owner,remaining,past}}},None{})
451 case True{} True{}: prepared_view_current(~S,~C,~V,~project,values,stamps,capacity,current,owner,remaining,past)
452 case True{} False{}: prepared_view_different(~S,~C,~V,~project,id,values,stamps,capacity,current,owner,remaining,past,U32.is_lt(id,current))
453def indexed_prepared_view_checked(~S:Data,~C:Type,~V:Data,~project:C -> C & V,+id:U32,values:Array<Maybe<&1,C>>,metadata:M.Metadata,+capacity:U32,+current:U32,owner:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:History<S,C>,valid:Bool,same:Bool) -> Column<S,C> & Maybe<&2,V>:
454 match valid same:
455 case False{} _: (PreparedIndexed{IndexedPreparedOwned{IndexedPreparedState{values,metadata,capacity,current,owner,remaining,past}}},None{})
456 case True{} True{}: indexed_prepared_view_current(~S,~C,~V,~project,values,metadata,capacity,current,owner,remaining,past)
457 case True{} False{}: indexed_prepared_view_different(~S,~C,~V,~project,id,values,metadata,capacity,current,owner,remaining,past,U32.is_lt(id,current))
458def prepared_view_state(~S:Data,~C:Type,~V:Data,~project:C -> C & V,+id:U32,state:State<S,C>) -> Column<S,C> & Maybe<&2,V>:
459 match state:
460 case State{values,stamps,+capacity,+current,owner,remaining,past}: prepared_view_checked(~S,~C,~V,~project,id,values,stamps,capacity,current,owner,remaining,past,U32.is_gt(id,0) && U32.is_le(id,capacity),U32.is_eq(id,current))
461def indexed_prepared_view_state(~S:Data,~C:Type,~V:Data,~project:C -> C & V,+id:U32,state:IndexedPreparedState<S,C>) -> Column<S,C> & Maybe<&2,V>:
462 match state:
463 case IndexedPreparedState{values,metadata,+capacity,+current,owner,remaining,past}: indexed_prepared_view_checked(~S,~C,~V,~project,id,values,metadata,capacity,current,owner,remaining,past,U32.is_gt(id,0) && U32.is_le(id,capacity),U32.is_eq(id,current))
464def view(~S: Data, ~C: Type, ~V: Data, ~project: C -> C & V, column: Column<S,C>, +id: U32) -> Column<S,C> & Maybe<&2,V>:
465 match column:
466 case Column{values,stamps}: plain_view_sized(~S,~C,~V,~project,id,stamps,Array.size(Maybe<&1,C>,values))
467 case Prepared{carrier}: prepared_view_state(~S,~C,~V,~project,id,unseal(~S,~C,carrier))
468 case Indexed{carrier}: indexed_view_state(~S,~C,~V,~project,id,indexed_unseal(~S,~C,carrier))
469 case PreparedIndexed{carrier}: indexed_prepared_view_state(~S,~C,~V,~project,id,indexed_prepared_unseal(~S,~C,carrier))
470
471def present(~C: Type, owner: C) -> C & Bool:
472 (owner, True{})
473
474def presence(~S: Data, ~C: Type, result: Column<S,C> & Maybe<&2,Bool>) -> Column<S,C> & Bool:
475 match result:
476 case (column, None{}):
477 (column, False{})
478 case (column, Some{found}):
479 (column, found)
480
481def has(~S: Data, ~C: Type, column: Column<S,C>, id: U32) -> Column<S,C> & Bool:
482 presence(~S, ~C, view(~S, ~C, ~Bool, ~present(~C), column, id))
483
484# Raw owner swaps/projection are metadata-neutral. Only the component world
485# write seam advances stamps, and rollback restores a saved stamp explicitly.
486def lifecycle_state(~S:Data,~C:Type,+id:U32,state:State<S,C>) -> Column<S,C> & L.Stamp:
487 match state:
488 case State{values,+stamps,capacity,current,owner,remaining,past}: (Prepared{Owned{State{values,stamps,capacity,current,owner,remaining,past}}},L.get(stamps,id))
489def indexed_prepared_lifecycle_got(~S:Data,~C:Type,values:Array<Maybe<&1,C>>,capacity:U32,current:U32,owner:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:History<S,C>,result:M.Metadata & L.Stamp) -> Column<S,C> & L.Stamp:
490 match result:
491 case (metadata,stamp): (PreparedIndexed{IndexedPreparedOwned{IndexedPreparedState{values,metadata,capacity,current,owner,remaining,past}}},stamp)
492def indexed_prepared_lifecycle_state(~S:Data,~C:Type,+id:U32,state:IndexedPreparedState<S,C>) -> Column<S,C> & L.Stamp:
493 match state:
494 case IndexedPreparedState{values,metadata,capacity,current,owner,remaining,past}: indexed_prepared_lifecycle_got(~S,~C,values,capacity,current,owner,remaining,past,M.get(metadata,id))
495def lifecycle(~S: Data,~C: Type,column: Column<S,C>,+id: U32) -> Column<S,C> & L.Stamp:
496 match column:
497 case Column{values,+stamps}: (Column{values,stamps},L.get(stamps,id))
498 case Prepared{carrier}: lifecycle_state(~S,~C,id,unseal(~S,~C,carrier))
499 case Indexed{carrier}: indexed_lifecycle_state(~S,~C,id,indexed_unseal(~S,~C,carrier))
500 case PreparedIndexed{carrier}: indexed_prepared_lifecycle_state(~S,~C,id,indexed_prepared_unseal(~S,~C,carrier))
501
502def restore_state(~S:Data,~C:Type,+id:U32,stamp:L.Stamp,state:State<S,C>) -> Column<S,C>:
503 match state:
504 case State{values,stamps,capacity,current,owner,remaining,past}: Prepared{Owned{State{values,L.set(stamps,id,stamp),capacity,current,owner,remaining,past}}}
505def indexed_prepared_restore_state(~S:Data,~C:Type,+id:U32,stamp:L.Stamp,state:IndexedPreparedState<S,C>) -> Column<S,C>:
506 match state:
507 case IndexedPreparedState{values,metadata,capacity,current,owner,remaining,past}: PreparedIndexed{IndexedPreparedOwned{IndexedPreparedState{values,M.set(metadata,id,stamp),capacity,current,owner,remaining,past}}}
508def restore_stamp(~S: Data,~C: Type,column: Column<S,C>,+id: U32,stamp: L.Stamp) -> Column<S,C>:
509 match column:
510 case Column{values,stamps}: Column{values,L.set(stamps,id,stamp)}
511 case Prepared{carrier}: restore_state(~S,~C,id,stamp,unseal(~S,~C,carrier))
512 case Indexed{carrier}: indexed_restore_state(~S,~C,id,stamp,indexed_unseal(~S,~C,carrier))
513 case PreparedIndexed{carrier}: indexed_prepared_restore_state(~S,~C,id,stamp,indexed_prepared_unseal(~S,~C,carrier))
514
515def mark_state(~S:Data,~C:Type,+id:U32,incoming:Bool,wasPresent:Bool,tick:Tick.Tick,state:State<S,C>) -> Column<S,C>:
516 match state:
517 case State{values,+stamps,capacity,current,owner,remaining,past}: Prepared{Owned{State{values,L.set(stamps,id,L.after_write(incoming,wasPresent,L.get(stamps,id),tick)),capacity,current,owner,remaining,past}}}
518def indexed_prepared_mark_got(~S:Data,~C:Type,+id:U32,incoming:Bool,wasPresent:Bool,tick:Tick.Tick,values:Array<Maybe<&1,C>>,capacity:U32,current:U32,owner:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:History<S,C>,result:M.Metadata & L.Stamp) -> Column<S,C>:
519 match result:
520 case (metadata,stamp): PreparedIndexed{IndexedPreparedOwned{IndexedPreparedState{values,M.set(metadata,id,L.after_write(incoming,wasPresent,stamp,tick)),capacity,current,owner,remaining,past}}}
521def indexed_prepared_mark_state(~S:Data,~C:Type,+id:U32,incoming:Bool,wasPresent:Bool,tick:Tick.Tick,state:IndexedPreparedState<S,C>) -> Column<S,C>:
522 match state:
523 case IndexedPreparedState{values,metadata,capacity,current,owner,remaining,past}: indexed_prepared_mark_got(~S,~C,id,incoming,wasPresent,tick,values,capacity,current,owner,remaining,past,M.get(metadata,id))
524def mark(~S: Data,~C: Type,column: Column<S,C>,+id: U32,incoming: Bool,wasPresent: Bool,tick: Tick.Tick) -> Column<S,C>:
525 match column:
526 case Column{values,+stamps}: Column{values,L.set(stamps,id,L.after_write(incoming,wasPresent,L.get(stamps,id),tick))}
527 case Prepared{carrier}: mark_state(~S,~C,id,incoming,wasPresent,tick,unseal(~S,~C,carrier))
528 case Indexed{carrier}: indexed_mark_state(~S,~C,id,incoming,wasPresent,tick,indexed_unseal(~S,~C,carrier))
529 case PreparedIndexed{carrier}: indexed_prepared_mark_state(~S,~C,id,incoming,wasPresent,tick,indexed_prepared_unseal(~S,~C,carrier))
530
531# Structural cleanup releases payload and associated lifecycle entry. Projection
532# and journal swaps remain metadata-neutral; despawn must use this explicit seam.
533def clear_state(~S:Data,~C:Type,+id:U32,state:State<S,C>) -> Column<S,C>:
534 match state:
535 case State{values,stamps,capacity,current,owner,remaining,past}: Prepared{Owned{State{values,L.clear(stamps,id),capacity,current,owner,remaining,past}}}
536def indexed_prepared_clear_state(~S:Data,~C:Type,+id:U32,state:IndexedPreparedState<S,C>) -> Column<S,C>:
537 match state:
538 case IndexedPreparedState{values,metadata,capacity,current,owner,remaining,past}: PreparedIndexed{IndexedPreparedOwned{IndexedPreparedState{values,M.clear(metadata,id),capacity,current,owner,remaining,past}}}
539def clear_stamp(~S: Data,~C: Type,column: Column<S,C>,+id: U32) -> Column<S,C>:
540 match column:
541 case Column{values,stamps}: Column{values,L.clear(stamps,id)}
542 case Prepared{carrier}: clear_state(~S,~C,id,unseal(~S,~C,carrier))
543 case Indexed{carrier}: indexed_clear_state(~S,~C,id,indexed_unseal(~S,~C,carrier))
544 case PreparedIndexed{carrier}: indexed_prepared_clear_state(~S,~C,id,indexed_prepared_unseal(~S,~C,carrier))
545
546def cleared(~S: Data,~C: Type,+id: U32,outcome: SwapOutcome<S,C>) -> SwapOutcome<S,C>:
547 match outcome:
548 case Accepted{column,previous}: Accepted{clear_stamp(~S,~C,column,id),previous}
549 case Rejected{column,incoming}: Rejected{column,incoming}
550
551# Trusted slot-level removal returning column and its displaced optional
552# payload; successful removal also clears that slot's lifecycle stamp. Does
553# not validate namespace/generation or finalize the returned payload. Use the
554# matching schema cleanup adapter after runtime handle validation.
555def clear(~S: Data,~C: Type,column: Column<S,C>,+id: U32) -> SwapOutcome<S,C>:
556 cleared(~S,~C,id,swap(~S,~C,column,id,None{}))