1	import Base
2	import ./change_tick.bend as Tick
3	import ./world.bend as W
4	import ./event_runtime.bend as Ev
5	import ./relation_commands.bend as A
6	import ./inspector.bend as I
7	import ./inspector_stream_frame.bend as F
8	import ./capabilities.bend as Cap
9	
10	# A run plan grants capabilities over one stream-backed frame. The frame owns
11	# the actual event runtime; callers do not receive a detached or reconstructed
12	# event log.
13	type Plan<-S:Data,-C:Type,-R:Type,-E:Data,-Ops:Type -> Type> is Type:
14	  Plan{caps:Ops(F.Frame<S,C,R,E>)}
15	
16	# The result returns the exact runtime owner produced by the callback, with the
17	# inspector's single successful clock advance applied to its World.
18	type RunResult<S:Data,C:Type,R:Type,E:Data,U:Data,Out:Data> is Type:
19	  RunResult{runtime:Ev.Runtime<S,C,R,A.Notice<S,E>>,instance:I.Instance<S>,result:Result<&2,&2,U,Out>}
20	
21	def plan_caps(~S:Data,~C:Type,~R:Type,~E:Data,~Ops:Type -> Type,plan:Plan<S,C,R,E,Ops>) -> Ops(F.Frame<S,C,R,E>):
22	  match plan:
23	    case Plan{caps}:caps
24	
25	def fresh_join(~S:Data,~C:Type,~R:Type,~E:Data,clocked:W.World<S,C,R,A.Notice<S,E>> & Tick.Tick,namespace:U32,batches:List<&2,Ev.Batch<A.Notice<S,E>>>,positions:List<&2,Ev.Position>,nextReader:U32,tick:Nat,frameStart:Nat,boundary:Nat,capacity:Nat,dropped:Nat) -> Ev.Runtime<S,C,R,A.Notice<S,E>> & Tick.Tick:
26	  (world,registeredAt)=clocked
27	  (Ev.Runtime{world,namespace,batches,positions,nextReader,tick,frameStart,boundary,capacity,dropped},registeredAt)
28	
29	def fresh_runtime(~S:Data,~C:Type,~R:Type,~E:Data,runtime:Ev.Runtime<S,C,R,A.Notice<S,E>>) -> Ev.Runtime<S,C,R,A.Notice<S,E>> & Tick.Tick:
30	  match runtime:
31	    case Ev.Runtime{world,+namespace,+batches,+positions,+nextReader,+tick,+frameStart,+boundary,+capacity,+dropped}:
32	      fresh_join(~S,~C,~R,~E,W.clock(~S,~C,~R,~A.Notice<S,E>,world),namespace,batches,positions,nextReader,tick,frameStart,boundary,capacity,dropped)
33	
34	def bumped_runtime(~S:Data,~C:Type,~R:Type,~E:Data,advanced:W.World<S,C,R,A.Notice<S,E>> & Tick.Tick,namespace:U32,batches:List<&2,Ev.Batch<A.Notice<S,E>>>,positions:List<&2,Ev.Position>,nextReader:U32,tick:Nat,frameStart:Nat,boundary:Nat,capacity:Nat,dropped:Nat) -> Ev.Runtime<S,C,R,A.Notice<S,E>> & Tick.Tick:
35	  (world,cursor)=advanced
36	  (Ev.Runtime{world,namespace,batches,positions,nextReader,tick,frameStart,boundary,capacity,dropped},cursor)
37	
38	def advance_runtime(~S:Data,~C:Type,~R:Type,~E:Data,runtime:Ev.Runtime<S,C,R,A.Notice<S,E>>) -> Ev.Runtime<S,C,R,A.Notice<S,E>> & Tick.Tick:
39	  match runtime:
40	    case Ev.Runtime{world,+namespace,+batches,+positions,+nextReader,+tick,+frameStart,+boundary,+capacity,+dropped}:
41	      bumped_runtime(~S,~C,~R,~E,W.advance_clock(~S,~C,~R,~A.Notice<S,E>,world),namespace,batches,positions,nextReader,tick,frameStart,boundary,capacity,dropped)
42	
43	def succeeded(~S:Data,~C:Type,~R:Type,~E:Data,~U:Data,~Out:Data,registeredAt:Tick.Tick,value:Out,observed:Ev.Runtime<S,C,R,A.Notice<S,E>> & Tick.Tick) -> RunResult<S,C,R,E,U,Out>:
44	  (runtime,cursor)=observed
45	  RunResult{runtime,I.Active{Some{cursor},registeredAt},Done{value}}
46	
47	def finished(~S:Data,~C:Type,~R:Type,~E:Data,~U:Data,~Out:Data,cursor:Maybe<&2,Tick.Tick>,registeredAt:Tick.Tick,observed:F.Frame<S,C,R,E> & Result<&2,&2,U,Out>) -> RunResult<S,C,R,E,U,Out>:
48	  match observed:
49	    case (F.Frame{runtime,_},Fail{error}):RunResult{runtime,I.Active{cursor,registeredAt},Fail{error}}
50	    case (F.Frame{runtime,_},Done{value}):succeeded(~S,~C,~R,~E,~U,~Out,registeredAt,value,advance_runtime(~S,~C,~R,~E,runtime))
51	
52	def invoked(~S:Data,~C:Type,~R:Type,~E:Data,~Ops:Type -> Type,~A0:Data,~U:Data,~Out:Data,~plan:Plan<S,C,R,E,Ops>,~body:@-H:Type -> @-caps:Ops(H) -> A0 -> H -> H & Result<&2,&2,U,Out>,args:A0,+cursor:Maybe<&2,Tick.Tick>,+registeredAt:Tick.Tick,runtime:Ev.Runtime<S,C,R,A.Notice<S,E>>) -> RunResult<S,C,R,E,U,Out>:
53	  finished(~S,~C,~R,~E,~U,~Out,cursor,registeredAt,Cap.invoke(~Ops,~A0,~Result<&2,&2,U,Out>,~body,~F.Frame<S,C,R,E>,~plan_caps(~S,~C,~R,~E,~Ops,plan),args,F.Frame{runtime,cursor}))
54	
55	def begin_fresh(~S:Data,~C:Type,~R:Type,~E:Data,~Ops:Type -> Type,~A0:Data,~U:Data,~Out:Data,~plan:Plan<S,C,R,E,Ops>,~body:@-H:Type -> @-caps:Ops(H) -> A0 -> H -> H & Result<&2,&2,U,Out>,args:A0,runtime:Ev.Runtime<S,C,R,A.Notice<S,E>> & Tick.Tick) -> RunResult<S,C,R,E,U,Out>:
56	  (runtime,registeredAt)=runtime
57	  invoked(~S,~C,~R,~E,~Ops,~A0,~U,~Out,~plan,~body,args,None{},registeredAt,runtime)
58	
59	def run(~S:Data,~C:Type,~R:Type,~E:Data,~Ops:Type -> Type,~A0:Data,~U:Data,~Out:Data,~plan:Plan<S,C,R,E,Ops>,~body:@-H:Type -> @-caps:Ops(H) -> A0 -> H -> H & Result<&2,&2,U,Out>,instance:I.Instance<S>,args:A0,runtime:Ev.Runtime<S,C,R,A.Notice<S,E>>) -> RunResult<S,C,R,E,U,Out>:
60	  match instance:
61	    case I.Fresh{}:begin_fresh(~S,~C,~R,~E,~Ops,~A0,~U,~Out,~plan,~body,args,fresh_runtime(~S,~C,~R,~E,runtime))
62	    case I.Active{cursor,registeredAt}:invoked(~S,~C,~R,~E,~Ops,~A0,~U,~Out,~plan,~body,args,cursor,registeredAt,runtime)
63	
64	# Lift a trusted World-backed capability without detaching or duplicating the
65	# event runtime. This preserves the supplied grant exactly; it is not a sandbox
66	# or a type-enforced read-only boundary for caller-constructed capabilities.
67	# As with I.Plan, grant construction is part of the trusted setup boundary.
68	# Every Event Runtime field except its World is preserved.
69	def restored_read(~S:Data,~C:Type,~R:Type,~E:Data,~V:Data,observed:I.Frame<S,C,R,A.Notice<S,E>> & V,namespace:U32,batches:List<&2,Ev.Batch<A.Notice<S,E>>>,positions:List<&2,Ev.Position>,nextReader:U32,tick:Nat,frameStart:Nat,boundary:Nat,capacity:Nat,dropped:Nat) -> F.Frame<S,C,R,E> & V:
70	  match observed:
71	    case (I.Frame{world,cursor},value): (F.Frame{Ev.Runtime{world,namespace,batches,positions,nextReader,tick,frameStart,boundary,capacity,dropped},cursor},value)
72	
73	def read_runtime(~S:Data,~C:Type,~R:Type,~E:Data,~V:Data,~cap:Cap.ValueRead<I.Frame<S,C,R,A.Notice<S,E>>,V>,cursor:Maybe<&2,Tick.Tick>,runtime:Ev.Runtime<S,C,R,A.Notice<S,E>>) -> F.Frame<S,C,R,E> & V:
74	  match runtime:
75	    case Ev.Runtime{world,+namespace,+batches,+positions,+nextReader,+tick,+frameStart,+boundary,+capacity,+dropped}:
76	      restored_read(~S,~C,~R,~E,~V,Cap.value_read(~I.Frame<S,C,R,A.Notice<S,E>>,~V,~cap,I.Frame{world,cursor}),namespace,batches,positions,nextReader,tick,frameStart,boundary,capacity,dropped)
77	
78	def read_frame(~S:Data,~C:Type,~R:Type,~E:Data,~V:Data,~cap:Cap.ValueRead<I.Frame<S,C,R,A.Notice<S,E>>,V>,frame:F.Frame<S,C,R,E>) -> F.Frame<S,C,R,E> & V:
79	  match frame:
80	    case F.Frame{runtime,cursor}:read_runtime(~S,~C,~R,~E,~V,~cap,cursor,runtime)
81	
82	def lift_world_read(~S:Data,~C:Type,~R:Type,~E:Data,~V:Data,~cap:Cap.ValueRead<I.Frame<S,C,R,A.Notice<S,E>>,V>) -> Cap.ValueRead<F.Frame<S,C,R,E>,V>:
83	  Cap.ValueRead{read_frame(~S,~C,~R,~E,~V,~cap)}
84	
85	# A handle lookup remains an ordinary runtime argument. This lift restores the
86	# event owner around the existing Inspector lookup without capturing a handle
87	# or detaching any of the runtime's reader/event metadata. It preserves the
88	# supplied trusted grant and does not make an arbitrary Lookup closure safe.
89	def restored_lookup(~S:Data,~C:Type,~R:Type,~E:Data,~V:Data,observed:I.Frame<S,C,R,A.Notice<S,E>> & I.Value<V>,namespace:U32,batches:List<&2,Ev.Batch<A.Notice<S,E>>>,positions:List<&2,Ev.Position>,nextReader:U32,tick:Nat,frameStart:Nat,boundary:Nat,capacity:Nat,dropped:Nat) -> F.Frame<S,C,R,E> & I.Value<V>:
90	  match observed:
91	    case (I.Frame{world,cursor},value):(F.Frame{Ev.Runtime{world,namespace,batches,positions,nextReader,tick,frameStart,boundary,capacity,dropped},cursor},value)
92	
93	def lookup_runtime(~S:Data,~C:Type,~R:Type,~E:Data,~V:Data,~cap:I.Lookup<I.Frame<S,C,R,A.Notice<S,E>>,S,V>,cursor:Maybe<&2,Tick.Tick>,runtime:Ev.Runtime<S,C,R,A.Notice<S,E>>,target:W.Handle<S>) -> F.Frame<S,C,R,E> & I.Value<V>:
94	  match runtime:
95	    case Ev.Runtime{world,+namespace,+batches,+positions,+nextReader,+tick,+frameStart,+boundary,+capacity,+dropped}:
96	      restored_lookup(~S,~C,~R,~E,~V,I.lookup(~I.Frame<S,C,R,A.Notice<S,E>>,~S,~V,~cap,I.Frame{world,cursor},target),namespace,batches,positions,nextReader,tick,frameStart,boundary,capacity,dropped)
97	
98	def lookup_frame(~S:Data,~C:Type,~R:Type,~E:Data,~V:Data,~cap:I.Lookup<I.Frame<S,C,R,A.Notice<S,E>>,S,V>,frame:F.Frame<S,C,R,E>,target:W.Handle<S>) -> F.Frame<S,C,R,E> & I.Value<V>:
99	  match frame:
100	    case F.Frame{runtime,cursor}:lookup_runtime(~S,~C,~R,~E,~V,~cap,cursor,runtime,target)
101	
102	def lift_world_lookup(~S:Data,~C:Type,~R:Type,~E:Data,~V:Data,~cap:I.Lookup<I.Frame<S,C,R,A.Notice<S,E>>,S,V>) -> I.Lookup<F.Frame<S,C,R,E>,S,V>:
103	  I.Lookup{frame => target => lookup_frame(~S,~C,~R,~E,~V,~cap,frame,target)}