1	import Base
2	import column.bend as Col
3	import owner_handoff.bend as H
4	import lifecycle.bend as L
5	import indexed_lifecycle.bend as M
6	
7	# Provisioning captures a restoration closure only after accepted extraction.
8	# Gameplay never receives its captured column/index or a replacement restore target.
9	type Slot<-C:Type> is Type:
10	  Slot{owner:Maybe<&1,C>,stamp:L.Stamp,dirty:Bool}
11	type Capture<-S:Data,-C:Type> is Type:
12	  Captured{id:U32,owner:Maybe<&1,C>,stamp:L.Stamp,restore:Slot<C> -> Col.Column<S,C>}
13	  Unavailable{column:Col.Column<S,C>}
14	
15	def stamped(~S:Data,~C:Type,+id:U32,column:Col.Column<S,C>,stamp:L.Stamp,dirty:Bool) -> Col.Column<S,C>:
16	  match dirty:
17	    case False{}: column
18	    case True{}: Col.restore_stamp(~S,~C,column,id,stamp)
19	def restore_plain(~S:Data,~C:Type,+id:U32,values:Array<Maybe<&1,C>>,stamps:List<&2,L.Entry>,slot:Slot<C>) -> Col.Column<S,C>:
20	  match slot:
21	    case Slot{owner,stamp,dirty}: stamped(~S,~C,id,Col.Column{Array.set(Maybe<&1,C>,values,U32.sub(id,1),owner),stamps},stamp,dirty)
22	def indexed_restore_plain(~S:Data,~C:Type,+id:U32,values:Array<Maybe<&1,C>>,metadata:M.Metadata,slot:Slot<C>) -> Col.Column<S,C>:
23	  match slot:
24	    case Slot{owner,stamp,dirty}: stamped(~S,~C,id,Col.indexed_wrap(~S,~C,Array.set(Maybe<&1,C>,values,U32.sub(id,1),owner),metadata),stamp,dirty)
25	def indexed_plain_got(~S:Data,~C:Type,+id:U32,values:Array<Maybe<&1,C>>,owner:Maybe<&1,C>,result:M.Metadata & L.Stamp) -> Capture<S,C>:
26	  match result:
27	    case (metadata,stamp): Captured{id,owner,stamp,slot => indexed_restore_plain(~S,~C,id,values,metadata,slot)}
28	def indexed_plain_taken(~S:Data,~C:Type,+id:U32,metadata:M.Metadata,result:Array<Maybe<&1,C>> & Maybe<&1,C>) -> Capture<S,C>:
29	  match result:
30	    case (values,owner): indexed_plain_got(~S,~C,id,values,owner,M.get(metadata,id))
31	def indexed_plain_checked(~S:Data,~C:Type,+id:U32,metadata:M.Metadata,values:Array<Maybe<&1,C>>,valid:Bool) -> Capture<S,C>:
32	  match valid:
33	    case False{}: Unavailable{Col.indexed_wrap(~S,~C,values,metadata)}
34	    case True{}: indexed_plain_taken(~S,~C,id,metadata,Array.swap(Maybe<&1,C>,values,U32.sub(id,1),None{}))
35	def indexed_plain_sized(~S:Data,~C:Type,+id:U32,metadata:M.Metadata,sized:Array<Maybe<&1,C>> & U32) -> Capture<S,C>:
36	  match sized:
37	    case (values,size): indexed_plain_checked(~S,~C,id,metadata,values,U32.is_gt(id,0) && U32.is_le(id,size) && U32.is_le(id,131072))
38	def indexed_plain_state(~S:Data,~C:Type,+id:U32,state:Col.IndexedOrdinaryState<S,C>) -> Capture<S,C>:
39	  match state:
40	    case Col.IndexedOrdinaryState{values,metadata}: indexed_plain_sized(~S,~C,id,metadata,Array.size(Maybe<&1,C>,values))
41	def restore_prepared(~S:Data,~C:Type,+id:U32,values:Array<Maybe<&1,C>>,stamps:List<&2,L.Entry>,capacity:U32,remaining:H.PrototypeHandoffRows<S,C>,past:Col.History<S,C>,slot:Slot<C>) -> Col.Column<S,C>:
42	  match slot:
43	    case Slot{owner,stamp,dirty}: stamped(~S,~C,id,Col.Prepared{Col.Owned{Col.State{values,stamps,capacity,id,owner,remaining,past}}},stamp,dirty)
44	def indexed_restore_prepared(~S:Data,~C:Type,+id:U32,values:Array<Maybe<&1,C>>,metadata:M.Metadata,capacity:U32,remaining:H.PrototypeHandoffRows<S,C>,past:Col.History<S,C>,slot:Slot<C>) -> Col.Column<S,C>:
45	  match slot:
46	    case Slot{owner,stamp,dirty}: stamped(~S,~C,id,Col.PreparedIndexed{Col.IndexedPreparedOwned{Col.IndexedPreparedState{values,metadata,capacity,id,owner,remaining,past}}},stamp,dirty)
47	def captured_prepared(~S:Data,~C:Type,+id:U32,values:Array<Maybe<&1,C>>,+stamps:List<&2,L.Entry>,capacity:U32,owner:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:Col.History<S,C>) -> Capture<S,C>:
48	  Captured{id,owner,L.get(stamps,id),slot => restore_prepared(~S,~C,id,values,stamps,capacity,remaining,past,slot)}
49	# Exact constant-None specialization of Col.seek: phase and fuel remain observable.
50	def indexed_captured_got(~S:Data,~C:Type,+id:U32,values:Array<Maybe<&1,C>>,capacity:U32,owner:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:Col.History<S,C>,result:M.Metadata & L.Stamp) -> Capture<S,C>:
51	  match result:
52	    case (metadata,stamp): Captured{id,owner,stamp,slot => indexed_restore_prepared(~S,~C,id,values,metadata,capacity,remaining,past,slot)}
53	def indexed_captured_prepared(~S:Data,~C:Type,+id:U32,values:Array<Maybe<&1,C>>,metadata:M.Metadata,capacity:U32,owner:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:Col.History<S,C>) -> Capture<S,C>:
54	  indexed_captured_got(~S,~C,id,values,capacity,owner,remaining,past,M.get(metadata,id))
55	def capture_seek(~S:Data,~C:Type,fuel:Nat,values:Array<Maybe<&1,C>>,stamps:List<&2,L.Entry>,capacity:U32,+target:U32,remaining:H.PrototypeHandoffRows<S,C>,past:Col.History<S,C>,phase:Col.SeekPhase) -> Capture<S,C>:
56	  match fuel remaining phase:
57	    case _ H.HandoffNil{} _: captured_prepared(~S,~C,target,values,stamps,capacity,None{},H.HandoffNil{},past)
58	    case 0n H.HandoffCon{id,owner,rest} _: Unavailable{Col.Prepared{Col.Owned{Col.State{values,stamps,capacity,0,None{},H.HandoffCon{id,owner,rest},past}}}}
59	    case 1n+more H.HandoffCon{+id,owner,rest} Col.Inspect{}: capture_seek(~S,~C,more,values,stamps,capacity,target,H.HandoffCon{id,owner,rest},past,Col.Choice{U32.is_eq(target,id),U32.is_lt(target,id)})
60	    case 1n+more H.HandoffCon{id,owner,rest} Col.Choice{True{},_}: captured_prepared(~S,~C,target,values,stamps,capacity,Some{owner},rest,past)
61	    case 1n+more H.HandoffCon{id,owner,rest} Col.Choice{False{},True{}}: captured_prepared(~S,~C,target,values,stamps,capacity,None{},H.HandoffCon{id,owner,rest},past)
62	    case 1n+more H.HandoffCon{id,owner,rest} Col.Choice{False{},False{}}: capture_seek(~S,~C,more,values,stamps,capacity,target,rest,Col.HistoryCon{id,Some{owner},past},Col.Inspect{})
63	def indexed_capture_seek(~S:Data,~C:Type,fuel:Nat,values:Array<Maybe<&1,C>>,metadata:M.Metadata,capacity:U32,+target:U32,remaining:H.PrototypeHandoffRows<S,C>,past:Col.History<S,C>,phase:Col.SeekPhase) -> Capture<S,C>:
64	  match fuel remaining phase:
65	    case _ H.HandoffNil{} _: indexed_captured_prepared(~S,~C,target,values,metadata,capacity,None{},H.HandoffNil{},past)
66	    case 0n H.HandoffCon{id,owner,rest} _: Unavailable{Col.PreparedIndexed{Col.IndexedPreparedOwned{Col.IndexedPreparedState{values,metadata,capacity,0,None{},H.HandoffCon{id,owner,rest},past}}}}
67	    case 1n+more H.HandoffCon{+id,owner,rest} Col.Inspect{}: indexed_capture_seek(~S,~C,more,values,metadata,capacity,target,H.HandoffCon{id,owner,rest},past,Col.Choice{U32.is_eq(target,id),U32.is_lt(target,id)})
68	    case 1n+more H.HandoffCon{id,owner,rest} Col.Choice{True{},_}: indexed_captured_prepared(~S,~C,target,values,metadata,capacity,Some{owner},rest,past)
69	    case 1n+more H.HandoffCon{id,owner,rest} Col.Choice{False{},True{}}: indexed_captured_prepared(~S,~C,target,values,metadata,capacity,None{},H.HandoffCon{id,owner,rest},past)
70	    case 1n+more H.HandoffCon{id,owner,rest} Col.Choice{False{},False{}}: indexed_capture_seek(~S,~C,more,values,metadata,capacity,target,rest,Col.HistoryCon{id,Some{owner},past},Col.Inspect{})
71	def plain_taken(~S:Data,~C:Type,+id:U32,+stamps:List<&2,L.Entry>,result:Array<Maybe<&1,C>> & Maybe<&1,C>) -> Capture<S,C>:
72	  match result:
73	    case (values,owner): Captured{id,owner,L.get(stamps,id),slot => restore_plain(~S,~C,id,values,stamps,slot)}
74	def plain_checked(~S:Data,~C:Type,+id:U32,stamps:List<&2,L.Entry>,values:Array<Maybe<&1,C>>,valid:Bool) -> Capture<S,C>:
75	  match valid:
76	    case False{}: Unavailable{Col.Column{values,stamps}}
77	    case True{}: plain_taken(~S,~C,id,stamps,Array.swap(Maybe<&1,C>,values,U32.sub(id,1),None{}))
78	def plain_sized(~S:Data,~C:Type,+id:U32,stamps:List<&2,L.Entry>,sized:Array<Maybe<&1,C>> & U32) -> Capture<S,C>:
79	  match sized:
80	    case (values,size): plain_checked(~S,~C,id,stamps,values,U32.is_gt(id,0) && U32.is_le(id,size) && U32.is_le(id,131072))
81	def recovered_capture(~S:Data,~C:Type,+id:U32,column:Col.Column<S,C>) -> Capture<S,C>:
82	  match column:
83	    case Col.Column{values,stamps}: plain_sized(~S,~C,id,stamps,Array.size(Maybe<&1,C>,values))
84	    case Col.Indexed{carrier}: indexed_plain_state(~S,~C,id,Col.indexed_unseal(~S,~C,carrier))
85	    case other: Unavailable{other}
86	def prepared_checked(~S:Data,~C:Type,+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:Col.History<S,C>,valid:Bool,same:Bool,backwards:Bool) -> Capture<S,C>:
87	  match valid same backwards:
88	    case False{} _ _: Unavailable{Col.Prepared{Col.Owned{Col.State{values,stamps,capacity,current,owner,remaining,past}}}}
89	    case True{} True{} _: captured_prepared(~S,~C,id,values,stamps,capacity,owner,remaining,past)
90	    case True{} False{} True{}: recovered_capture(~S,~C,id,Col.recover(~S,~C,Col.Prepared{Col.Owned{Col.State{values,stamps,capacity,current,owner,remaining,past}}}))
91	    case True{} False{} False{}: capture_seek(~S,~C,U32.to_nat(U32.add(U32.add(capacity,capacity),1)),values,stamps,capacity,id,remaining,Col.past_current(~S,~C,current,owner,past,U32.is_gt(current,0)),Col.Inspect{})
92	def indexed_prepared_checked(~S:Data,~C:Type,+id:U32,values:Array<Maybe<&1,C>>,metadata:M.Metadata,+capacity:U32,+current:U32,owner:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:Col.History<S,C>,valid:Bool,same:Bool,backwards:Bool) -> Capture<S,C>:
93	  match valid same backwards:
94	    case False{} _ _: Unavailable{Col.PreparedIndexed{Col.IndexedPreparedOwned{Col.IndexedPreparedState{values,metadata,capacity,current,owner,remaining,past}}}}
95	    case True{} True{} _: indexed_captured_prepared(~S,~C,id,values,metadata,capacity,owner,remaining,past)
96	    case True{} False{} True{}: recovered_capture(~S,~C,id,Col.recover(~S,~C,Col.PreparedIndexed{Col.IndexedPreparedOwned{Col.IndexedPreparedState{values,metadata,capacity,current,owner,remaining,past}}}))
97	    case True{} False{} False{}: indexed_capture_seek(~S,~C,U32.to_nat(U32.add(U32.add(capacity,capacity),1)),values,metadata,capacity,id,remaining,Col.past_current(~S,~C,current,owner,past,U32.is_gt(current,0)),Col.Inspect{})
98	def prepared_state(~S:Data,~C:Type,+id:U32,state:Col.State<S,C>) -> Capture<S,C>:
99	  match state:
100	    case Col.State{values,stamps,+capacity,+current,owner,remaining,past}: prepared_checked(~S,~C,id,values,stamps,capacity,current,owner,remaining,past,U32.is_gt(id,0) && U32.is_le(id,capacity),U32.is_eq(id,current),U32.is_lt(id,current))
101	def indexed_prepared_state(~S:Data,~C:Type,+id:U32,state:Col.IndexedPreparedState<S,C>) -> Capture<S,C>:
102	  match state:
103	    case Col.IndexedPreparedState{values,metadata,+capacity,+current,owner,remaining,past}: indexed_prepared_checked(~S,~C,id,values,metadata,capacity,current,owner,remaining,past,U32.is_gt(id,0) && U32.is_le(id,capacity),U32.is_eq(id,current),U32.is_lt(id,current))
104	def capture(~S:Data,~C:Type,column:Col.Column<S,C>,+id:U32) -> Capture<S,C>:
105	  match column:
106	    case Col.Column{values,stamps}: plain_sized(~S,~C,id,stamps,Array.size(Maybe<&1,C>,values))
107	    case Col.Prepared{carrier}: prepared_state(~S,~C,id,Col.unseal(~S,~C,carrier))
108	    case Col.Indexed{carrier}: indexed_plain_state(~S,~C,id,Col.indexed_unseal(~S,~C,carrier))
109	    case Col.PreparedIndexed{carrier}: indexed_prepared_state(~S,~C,id,Col.indexed_prepared_unseal(~S,~C,carrier))