1	import Base
2	import ./deferred_command.bend as Deferred
3	import ./trace_facts.bend as TraceFacts
4	import entity_key.bend as K
5	import bundle_delivery.bend as B
6	import world.bend as W
7	import transaction.bend as T
8	import commands.bend as Cmd
9	
10	# Prepared payload owners remain typed until successful body completion.
11	# This insert-only journal introduces no reservation/cancellation policy.
12	type Prepared<S:Data,P:Type> is Type:
13	  Prepared{target:W.Handle<S>,payload:P,position:Nat}
14	  ReservationReceipt{target:W.Handle<S>}
15	type Batch<S:Data,Store:Type,R:Type,E:Data,P:Type> is Type:
16	  Batch{tx:T.Tx<W.World<S,Store,R,E>,E>,prepared:List<Prepared<S,P>>}
17	type Inserted<S:Data,Store:Type,R:Type,E:Data,P:Type> is Type:
18	  Inserted{batch:Batch<S,Store,R,E,P>}
19	  Refused{batch:Batch<S,Store,R,E,P>,payload:P,error:W.WorldError}
20	type Spawned<S:Data,Store:Type,R:Type,E:Data,P:Type> is Type:
21	  Spawned{batch:Batch<S,Store,R,E,P>,target:W.Handle<S>}
22	  SpawnRefused{batch:Batch<S,Store,R,E,P>,payload:P,error:W.WorldError}
23	type Finished<S:Data,Store:Type,R:Type,E:Data,P:Type,Error:Data> is Type:
24	  Committed{world:W.World<S,Store,R,E>}
25	  Failed{world:W.World<S,Store,R,E>,payloads:List<P>,error:Error}
26	def begin(~S:Data,~Store:Type,~R:Type,~E:Data,~P:Type,tx:T.Tx<W.World<S,Store,R,E>,E>) -> Batch<S,Store,R,E,P>:
27	  Batch{tx,[]}
28	# Count returns the very same affine closures in the same reverse queue order.
29	def counted(~World:Type,command:Deferred.Command<World>,result:List<Deferred.Command<World>> & Nat) -> List<Deferred.Command<World>> & Nat:
30	  match result:
31	    case (commands,count): (command <> commands,1n+count)
32	def count_commands(~World:Type,commands:List<Deferred.Command<World>>) -> List<Deferred.Command<World>> & Nat:
33	  match commands:
34	    case []: ([],0n)
35	    case command <> tail: counted(~World,command,count_commands(~World,tail))
36	def positioned(~S:Data,~Store:Type,~R:Type,~E:Data,~P:Type,prepared:List<Prepared<S,P>>,world:W.World<S,Store,R,E>,undo:List<(W.World<S,Store,R,E> -> W.World<S,Store,R,E>)>,events:List<&2,E>,trace:TraceFacts.State,target:W.Handle<S>,payload:P,result:List<Deferred.Command<W.World<S,Store,R,E>>> & Nat) -> Inserted<S,Store,R,E,P>:
37	  match result:
38	    case (commands,position): Inserted{Batch{T.Tx{world,undo,commands,events,trace},Prepared{target,payload,position} <> prepared}}
39	# Receipt rows are created only from this Batch's actual Cmd.tx_spawn result.
40	# Public gameplay cannot construct the opaque Batch; raw engine constructors
41	# and provider callbacks remain explicitly trusted setup boundaries.
42	def receipt_join(~S:Data,~P:Type,entry:Prepared<S,P>,seen:Bool,result:List<Prepared<S,P>> & Bool) -> List<Prepared<S,P>> & Bool:
43	  match result:
44	    case (tail,found): (entry <> tail,Bool.or(seen,found))
45	def receipt_find(~S:Data,~P:Type,prepared:List<Prepared<S,P>>,+target:W.Handle<S>) -> List<Prepared<S,P>> & Bool:
46	  match prepared:
47	    case []: ([],False{})
48	    case Prepared{handle,payload,position} <> tail: receipt_join(~S,~P,Prepared{handle,payload,position},False{},receipt_find(~S,~P,tail,target))
49	    case ReservationReceipt{W.Handle{+ns,+id}} <> tail:
50	      match target:
51	        case W.Handle{+otherNs,+otherId}: receipt_join(~S,~P,ReservationReceipt{W.Handle{ns,id}},Bool.and(U32.is_eq(ns,otherNs),K.equal(id,otherId)),receipt_find(~S,~P,tail,W.Handle{otherNs,otherId}))
52	def receipt_checked(~S:Data,~Store:Type,~R:Type,~E:Data,~P:Type,world:W.World<S,Store,R,E>,undo:List<(W.World<S,Store,R,E> -> W.World<S,Store,R,E>)>,commands:List<Deferred.Command<W.World<S,Store,R,E>>>,events:List<&2,E>,trace:TraceFacts.State,target:W.Handle<S>,payload:P,result:List<Prepared<S,P>> & Bool) -> Inserted<S,Store,R,E,P>:
53	  match result:
54	    case (prepared,False{}): Refused{Batch{T.Tx{world,undo,commands,events,trace},prepared},payload,W.MissingEntity{}}
55	    case (prepared,True{}): positioned(~S,~Store,~R,~E,~P,prepared,world,undo,events,trace,target,payload,count_commands(~W.World<S,Store,R,E>,commands))
56	def checked(~S:Data,~Store:Type,~R:Type,~E:Data,~P:Type,prepared:List<Prepared<S,P>>,undo:List<(W.World<S,Store,R,E> -> W.World<S,Store,R,E>)>,commands:List<Deferred.Command<W.World<S,Store,R,E>>>,events:List<&2,E>,trace:TraceFacts.State,+target:W.Handle<S>,payload:P,observed:W.World<S,Store,R,E> & Bool) -> Inserted<S,Store,R,E,P>:
57	  match observed:
58	    case (world,False{}): receipt_checked(~S,~Store,~R,~E,~P,world,undo,commands,events,trace,target,payload,receipt_find(~S,~P,prepared,target))
59	    case (world,True{}): positioned(~S,~Store,~R,~E,~P,prepared,world,undo,events,trace,target,payload,count_commands(~W.World<S,Store,R,E>,commands))
60	def insert(~S:Data,~Store:Type,~R:Type,~E:Data,~P:Type,batch:Batch<S,Store,R,E,P>,+target:W.Handle<S>,payload:P) -> Inserted<S,Store,R,E,P>:
61	  match batch:
62	    case Batch{T.Tx{world,undo,commands,events,trace},prepared}: checked(~S,~Store,~R,~E,~P,prepared,undo,commands,events,trace,target,payload,W.valid(~S,~Store,~R,~E,world,target))
63	# Replay only closures preceding this authored insertion. Position is generated
64	# by count_commands, not supplied by gameplay; raw constructors remain trusted.
65	def preceding(~World:Type,~E:Data,count:Nat,commands:List<Deferred.Command<World>>,tx:T.Tx<World,E>) -> List<Deferred.Command<World>> & T.Tx<World,E>:
66	  match count commands:
67	    case 0n _: (commands,tx)
68	    case 1n+rest Nil{}: ([],tx)
69	    case 1n+rest Con{command,tail}: preceding(~World,~E,rest,tail,T.stage_command(~World,~E,tx,command))
70	def remaining(~World:Type,~E:Data,commands:List<Deferred.Command<World>>,tx:T.Tx<World,E>) -> T.Tx<World,E>:
71	  match commands:
72	    case []: tx
73	    case command <> tail: remaining(~World,~E,tail,T.stage_command(~World,~E,tx,command))
74	def staged_after(~S:Data,~Store:Type,~R:Type,~E:Data,~P:Type,~attempt:W.World<S,Store,R,E> -> W.Handle<S> -> P -> B.Delivery<W.World<S,Store,R,E>,P>,~recover:W.World<S,Store,R,E> -> P -> W.WorldError -> W.World<S,Store,R,E>,target:W.Handle<S>,payload:P,next:List<Deferred.Command<W.World<S,Store,R,E>>> -> T.Tx<W.World<S,Store,R,E>,E> -> T.Tx<W.World<S,Store,R,E>,E>,result:List<Deferred.Command<W.World<S,Store,R,E>>> & T.Tx<W.World<S,Store,R,E>,E>) -> T.Tx<W.World<S,Store,R,E>,E>:
75	  match result:
76	    case (after,before): next(after,B.enqueue(~S,~Store,~R,~E,~P,~attempt,~recover,before,target,payload))
77	def staged(~S:Data,~Store:Type,~R:Type,~E:Data,~P:Type,~attempt:W.World<S,Store,R,E> -> W.Handle<S> -> P -> B.Delivery<W.World<S,Store,R,E>,P>,~recover:W.World<S,Store,R,E> -> P -> W.WorldError -> W.World<S,Store,R,E>,prepared:List<Prepared<S,P>>,commands:List<Deferred.Command<W.World<S,Store,R,E>>>,+current:Nat,tx:T.Tx<W.World<S,Store,R,E>,E>) -> T.Tx<W.World<S,Store,R,E>,E>:
78	  match prepared:
79	    case []: remaining(~W.World<S,Store,R,E>,~E,commands,tx)
80	    case ReservationReceipt{target} <> tail: staged(~S,~Store,~R,~E,~P,~attempt,~recover,tail,commands,current,tx)
81	    case Prepared{+target,payload,+position} <> tail:
82	      staged_after(~S,~Store,~R,~E,~P,~attempt,~recover,target,payload,after => before => staged(~S,~Store,~R,~E,~P,~attempt,~recover,tail,after,position,before),preceding(~W.World<S,Store,R,E>,~E,Nat.sub(position,current),commands,tx))
83	def stage(~S:Data,~Store:Type,~R:Type,~E:Data,~P:Type,~attempt:W.World<S,Store,R,E> -> W.Handle<S> -> P -> B.Delivery<W.World<S,Store,R,E>,P>,~recover:W.World<S,Store,R,E> -> P -> W.WorldError -> W.World<S,Store,R,E>,prepared:List<Prepared<S,P>>,tx:T.Tx<W.World<S,Store,R,E>,E>) -> T.Tx<W.World<S,Store,R,E>,E>:
84	  match tx:
85	    case T.Tx{world,undo,commands,events,trace}: staged(~S,~Store,~R,~E,~P,~attempt,~recover,prepared,List.reverse(&1,Deferred.Command<W.World<S,Store,R,E>>,commands),0n,T.Tx{world,undo,[],events,trace})
86	def originals(~S:Data,~P:Type,prepared:List<Prepared<S,P>>) -> List<P>:
87	  match prepared:
88	    case []: []
89	    case ReservationReceipt{target} <> tail: originals(~S,~P,tail)
90	    case Prepared{target,payload,position} <> tail: payload <> originals(~S,~P,tail)
91	def committed(~S:Data,~Store:Type,~R:Type,~E:Data,~P:Type,~Error:Data,observed:T.Returned<W.World<S,Store,R,E>,Error>) -> Finished<S,Store,R,E,P,Error>:
92	  match observed:
93	    case T.Returned{world,outcome}: Committed{world}
94	def failed(~S:Data,~Store:Type,~R:Type,~E:Data,~P:Type,~Error:Data,payloads:List<P>,error:Error,observed:T.Returned<W.World<S,Store,R,E>,Error>) -> Finished<S,Store,R,E,P,Error>:
95	  match observed:
96	    case T.Returned{world,outcome}: Failed{world,payloads,error}
97	def finish(~S:Data,~Store:Type,~R:Type,~E:Data,~P:Type,~Error:Data,~attempt:W.World<S,Store,R,E> -> W.Handle<S> -> P -> B.Delivery<W.World<S,Store,R,E>,P>,~recover:W.World<S,Store,R,E> -> P -> W.WorldError -> W.World<S,Store,R,E>,batch:Batch<S,Store,R,E,P>,outcome:T.Outcome<Error>) -> Finished<S,Store,R,E,P,Error>:
98	  match batch outcome:
99	    case Batch{tx,prepared} T.Success{}: committed(~S,~Store,~R,~E,~P,~Error,Cmd.tx_finish(~S,~Store,~R,~E,~Error,stage(~S,~Store,~R,~E,~P,~attempt,~recover,List.reverse(&1,Prepared<S,P>,prepared),tx),T.Success{}))
100	    case Batch{tx,prepared} T.Failure{+error}: failed(~S,~Store,~R,~E,~P,~Error,originals(~S,~P,List.reverse(&1,Prepared<S,P>,prepared)),error,Cmd.tx_finish(~S,~Store,~R,~E,~Error,tx,T.Failure{error}))
101	
102	def empty_population(~S:Data,~Store:Type,~R:Type,~E:Data,world:W.World<S,Store,R,E>,handle:W.Handle<S>,unit:Unit) -> W.World<S,Store,R,E>:
103	  world
104	def spawn_positioned(~S:Data,~Store:Type,~R:Type,~E:Data,~P:Type,target:W.Handle<S>,result:Inserted<S,Store,R,E,P>) -> Spawned<S,Store,R,E,P>:
105	  match result:
106	    case Inserted{batch}: Spawned{batch,target}
107	    case Refused{batch,payload,error}: SpawnRefused{batch,payload,error}
108	def spawn_reserved(~S:Data,~Store:Type,~R:Type,~E:Data,~P:Type,prepared:List<Prepared<S,P>>,payload:P,result:T.Tx<W.World<S,Store,R,E>,E> & W.Reservation<S>) -> Spawned<S,Store,R,E,P>:
109	  match result:
110	    case (T.Tx{world,undo,commands,events,trace},W.Reserved{+target}): spawn_positioned(~S,~Store,~R,~E,~P,target,positioned(~S,~Store,~R,~E,~P,ReservationReceipt{target} <> prepared,world,undo,events,trace,target,payload,count_commands(~W.World<S,Store,R,E>,commands)))
111	    case (tx,W.ReservationRejected{error}): SpawnRefused{Batch{tx,prepared},payload,error}
112	def spawn(~S:Data,~Store:Type,~R:Type,~E:Data,~P:Type,batch:Batch<S,Store,R,E,P>,payload:P) -> Spawned<S,Store,R,E,P>:
113	  match batch:
114	    case Batch{tx,prepared}: spawn_reserved(~S,~Store,~R,~E,~P,prepared,payload,Cmd.tx_spawn(~S,~Store,~R,~E,~Unit,~(world => handle => unit => world),tx,Unit{}))