1	import Base
2	import ./execution_context.bend as Ctx
3	import ./world.bend as W
4	import ./system.bend as Sys
5	import ./event_runtime.bend as Ev
6	import ./trace_facts.bend as Facts
7	import ./ordinary_event_declaration.bend as Event
8	import ./event_stream.bend as Leaf
9	
10	# F is any finite generated product of typed stream leaves and affine owners.
11	# Actual sole World with heterogeneous family state F and routing tick. Canonical
12	# family builders couple selectors/streams; raw take/put/synchronize are trusted.
13	type Runtime<S:Data,C:Type,R:Type,P:Data,F:Type> is Type:
14	  Runtime{world:W.World<S,C,R,P>,family:F,tick:Nat}
15	# Affine reader token binding World namespace, stream-reader id and registry id
16	# to its typed stream selection. Raw field fabrication does not establish authority.
17	type Reader<S:Data,E:Data,F:Type,-take:F -> F & Leaf.Stream<S,E>,-put:F -> Leaf.Stream<S,E> -> F> is Type:
18	  Reader{namespace:U32,id:U32,registryId:U32}
19	# Successful registration retains runtime, actual reader and actual registry;
20	# failure returns runtime without dropping heterogeneous family owners.
21	type Registration<S:Data,C:Type,R:Type,P:Data,E:Data,F:Type,A:Type,Error:Data,O:Type,-take:F -> F & Leaf.Stream<S,E>,-put:F -> Leaf.Stream<S,E> -> F,-runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>> is Type:
22	  Registered{runtime:Runtime<S,C,R,P,F>,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>}
23	  RegistrationFailed{runtime:Runtime<S,C,R,P,F>}
24	def registration_identity(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,world:W.World<S,C,R,P>,family:F,+tick:Nat,+namespace:U32,returned:Leaf.Stream<S,E> & U32,identified:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner> & U32) -> Registration<S,C,R,P,E,F,A,Error,O,take,put,runner>:
25	  (stream,id)=returned
26	  (registry,registryId)=identified
27	  Registered{Runtime{world,put(family,stream),tick},Reader{namespace,id,registryId},registry}
28	def registration_result(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,family:F,+stream:Leaf.Stream<S,E>,+tick:Nat,+namespace:U32,result:Sys.RegistrationResult<S,C,R,P,Ev.Input<E,A>,Error,O,runner>) -> Registration<S,C,R,P,E,F,A,Error,O,take,put,runner>:
29	  match result:
30	    case Sys.RegistrationFailed{world}:RegistrationFailed{Runtime{world,put(family,stream),tick}}
31	    case Sys.Registered{world,registry}:registration_identity(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,world,family,tick,namespace,Leaf.registered(~S,~E,stream,tick),Sys.identity(~S,~C,~R,~P,~Ev.Input<E,A>,~Error,~O,~runner,registry))
32	def registration_read_checked(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,available:Bool,family:F,stream:Leaf.Stream<S,E>,tick:Nat,domain:Event.Domain<S,E>,+name:String,world:W.World<S,C,R,P>,namespace:U32) -> Registration<S,C,R,P,E,F,A,Error,O,take,put,runner>:
33	  match available:
34	    case False{}:RegistrationFailed{Runtime{world,put(family,stream),tick}}
35	    case True{}:registration_result(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,family,stream,tick,namespace,Sys.register(~S,~C,~R,~P,~Ev.Input<E,A>,~Error,~O,~runner,world,name,[Event.access(~S,~E,Event.Declaration{domain,Event.Read{}})]))
36	def registration_namespace(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,family:F,+stream:Leaf.Stream<S,E>,tick:Nat,declaration:Event.Declaration<S,E>,+name:String,world:W.World<S,C,R,P>,namespace:U32) -> Registration<S,C,R,P,E,F,A,Error,O,take,put,runner>:
37	  match declaration:
38	    case Event.Declaration{_,Event.Write{}}:RegistrationFailed{Runtime{world,put(family,stream),tick}}
39	    case Event.Declaration{+domain,Event.Read{}}:registration_read_checked(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,Leaf.can_register(~S,~E,stream),family,stream,tick,domain,name,world,namespace)
40	def registration_named(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,family:F,stream:Leaf.Stream<S,E>,tick:Nat,declaration:Event.Declaration<S,E>,name:String,named:W.World<S,C,R,P> & U32) -> Registration<S,C,R,P,E,F,A,Error,O,take,put,runner>:
41	  match named:
42	    case (world,namespace):registration_namespace(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,family,stream,tick,declaration,name,world,namespace)
43	def registration_leaf(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,world:W.World<S,C,R,P>,tick:Nat,name:String,returned:F & Leaf.Stream<S,E>) -> Registration<S,C,R,P,E,F,A,Error,O,take,put,runner>:
44	  match returned:
45	    case (family,+stream):registration_named(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,family,stream,tick,Leaf.read_declaration(~S,~E,stream),name,W.namespace(~S,~C,~R,~P,world))
46	# Register against the selected stream's read declaration and actual World.
47	# Check stream/system id admission before returning reader/registry; does not run
48	# a callback or activate unread position merely by registering.
49	def register(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,runtime:Runtime<S,C,R,P,F>,name:String) -> Registration<S,C,R,P,E,F,A,Error,O,take,put,runner>:
50	  match runtime:
51	    case Runtime{world,family,tick}:registration_leaf(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,world,tick,name,take(family))
52	
53	# Every route result retains runtime, reader and registry. Inspect completion:
54	# Succeeded carries O, Failed carries callback error, Rejected returns actual Args.
55	# Semantic failure may be encoded inside O by higher adapters; inspect that too.
56	type RunResult<S:Data,C:Type,R:Type,P:Data,E:Data,F:Type,A:Type,Error:Data,O:Type,-take:F -> F & Leaf.Stream<S,E>,-put:F -> Leaf.Stream<S,E> -> F,-runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>> is Type:
57	  Ran{runtime:Runtime<S,C,R,P,F>,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,completion:Ev.Completion<Error,O,A>}
58	def run_synchronized_traced(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~observed:Facts.State -> W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O> & Facts.State,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,tick:Nat,output:O,returned:W.World<S,C,R,P> & F,trace:Facts.State) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner> & Facts.State:
59	  match returned:
60	    case (world,family):(Ran{Runtime{world,family,tick},reader,registry,Ev.Succeeded{output}},trace)
61	def prior_positions(~S:Data,~E:Data,stream:Leaf.Stream<S,E>) -> Leaf.Stream<S,E> & List<&2,Ev.Position>:
62	  match stream:
63	    case Leaf.Stream{domain,batches,+positions,nextReader,frameStart,boundary,capacity,dropped}:(Leaf.Stream{domain,batches,positions,nextReader,frameStart,boundary,capacity,dropped},positions)
64	def restored_positions(~S:Data,~E:Data,old:List<&2,Ev.Position>,id:U32,tick:Nat,stream:Leaf.Stream<S,E>) -> Leaf.Stream<S,E>:
65	  match stream:
66	    case Leaf.Stream{domain,batches,_,nextReader,frameStart,boundary,capacity,dropped}:Leaf.Stream{domain,batches,Ev.activate(old,id,Nat.sub(tick,1n)),nextReader,frameStart,boundary,capacity,dropped}
67	def run_completion_taken(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~observed:Facts.State -> W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O> & Facts.State,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,+tick:Nat,output:O,world:W.World<S,C,R,P>,old:List<&2,Ev.Position>,id:U32,returned:F & Leaf.Stream<S,E>,trace:Facts.State) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner> & Facts.State:
68	  match returned:
69	    case (family,stream):(Ran{Runtime{world,put(family,restored_positions(~S,~E,old,id,tick,stream)),tick},reader,registry,Ev.Succeeded{output}},trace)
70	def run_completion_synced(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~observed:Facts.State -> W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O> & Facts.State,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,tick:Nat,output:O,old:List<&2,Ev.Position>,id:U32,returned:W.World<S,C,R,P> & F,trace:Facts.State) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner> & Facts.State:
71	  match returned:
72	    case (world,family):run_completion_taken(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~observed,reader,registry,tick,output,world,old,id,take(family),trace)
73	def run_accepted_positions(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~observed:Facts.State -> W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O> & Facts.State,~accepted:O -> O & Bool,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,family:F,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,+id:U32,+tick:Nat,world:W.World<S,C,R,P>,output:O,success:Bool,prior:Leaf.Stream<S,E> & List<&2,Ev.Position>,trace:Facts.State) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner> & Facts.State:
74	  match success prior:
75	    case True{}, (stream,_):run_synchronized_traced(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~observed,reader,registry,1n+tick,output,synchronize(world,put(family,Leaf.completed(~S,~E,stream,id,1n+tick,True{})),1n+tick),trace)
76	    case False{}, (stream,old):run_completion_synced(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~observed,reader,registry,1n+tick,output,old,id,synchronize(world,put(family,Leaf.completed(~S,~E,stream,id,1n+tick,True{})),1n+tick),trace)
77	def run_accepted_traced(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~observed:Facts.State -> W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O> & Facts.State,~accepted:O -> O & Bool,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,family:F,+stream:Leaf.Stream<S,E>,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,+id:U32,+tick:Nat,world:W.World<S,C,R,P>,completion:O & Bool,trace:Facts.State) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner> & Facts.State:
78	  match completion:
79	    case (output,success):run_accepted_positions(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~observed,~accepted,~synchronize,family,reader,registry,id,tick,world,output,success,prior_positions(~S,~E,stream),trace)
80	def run_outcome_traced(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~observed:Facts.State -> W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O> & Facts.State,~accepted:O -> O & Bool,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,family:F,+stream:Leaf.Stream<S,E>,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,+id:U32,+tick:Nat,outcome:Sys.Outcome<W.World<S,C,R,P>,Error,O>,trace:Facts.State) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner> & Facts.State:
81	  match outcome:
82	    case Sys.Failed{world,error}:(Ran{Runtime{world,put(family,Leaf.completed(~S,~E,stream,id,1n+tick,False{})),1n+tick},reader,registry,Ev.Failed{error}},trace)
83	    case Sys.Succeeded{world,output}:run_accepted_traced(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~observed,~accepted,~synchronize,family,stream,reader,registry,id,tick,world,accepted(output),trace)
84	def run_result_traced(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~observed:Facts.State -> W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O> & Facts.State,~accepted:O -> O & Bool,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,family:F,stream:Leaf.Stream<S,E>,reader:Reader<S,E,F,take,put>,id:U32,tick:Nat,result:Sys.RunResult<S,C,R,P,Ev.Input<E,A>,Error,O,runner> & Facts.State) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner> & Facts.State:
85	  match result:
86	    case (Sys.RegistrationRejected{registry,world,Ev.Input{_,_,args}},trace):(Ran{Runtime{world,put(family,stream),1n+tick},reader,registry,Ev.Rejected{args}},trace)
87	    case (Sys.Completed{registry,outcome},trace):run_outcome_traced(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~observed,~accepted,~synchronize,family,stream,reader,registry,id,tick,outcome,trace)
88	def read_fact_declared(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~observed:Facts.State -> W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O> & Facts.State,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,readerId:U32,lagged:Bool,facts:List<&2,Facts.Fact>,declaration:Event.Declaration<S,E>) -> Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner> & Facts.State:
89	  match registry declaration:
90	    case Sys.Registry{+namespace,+id,+name,access,cursor} Event.Declaration{Event.Domain{domain},_}:(Sys.Registry{namespace,id,name,access,cursor},Facts.On{Facts.ReaderFact{namespace,id,name,readerId,domain,lagged} <> facts})
91	def read_fact(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~observed:Facts.State -> W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O> & Facts.State,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,readerId:U32,lagged:Bool,stream:Leaf.Stream<S,E>,trace:Facts.State) -> Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner> & Facts.State:
92	  match trace:
93	    case Facts.Off{}:(registry,Facts.Off{})
94	    case Facts.On{facts}:read_fact_declared(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~observed,registry,readerId,lagged,facts,Leaf.read_declaration(~S,~E,stream))
95	def run_recorded(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~observed:Facts.State -> W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O> & Facts.State,~accepted:O -> O & Bool,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,world:W.World<S,C,R,P>,family:F,stream:Leaf.Stream<S,E>,reader:Reader<S,E,F,take,put>,id:U32,tick:Nat,args:A,values:List<&2,E>,lagged:Bool,recorded:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner> & Facts.State) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner> & Facts.State:
96	  match recorded:
97	    case (registry,trace):run_result_traced(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~observed,~accepted,~synchronize,family,stream,reader,id,tick,Sys.run_observed(~S,~C,~R,~P,~Ev.Input<E,A>,~Error,~O,~runner,~observed,registry,trace,world,Ev.Input{values,lagged,args}))
98	def run_reading_traced(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~observed:Facts.State -> W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O> & Facts.State,~accepted:O -> O & Bool,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,world:W.World<S,C,R,P>,family:F,+stream:Leaf.Stream<S,E>,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,+id:U32,tick:Nat,args:A,reading:Ev.Reading<E>,trace:Facts.State) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner> & Facts.State:
99	  match reading:
100	    case Ev.Reading{values,+lagged}:run_recorded(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~observed,~accepted,~synchronize,world,family,stream,reader,id,tick,args,values,lagged,read_fact(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~observed,registry,id,lagged,stream,trace))
101	def run_leaf_reading_traced(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~observed:Facts.State -> W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O> & Facts.State,~accepted:O -> O & Bool,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,world:W.World<S,C,R,P>,family:F,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,id:U32,tick:Nat,args:A,returned:Leaf.Stream<S,E> & Ev.Reading<E>,trace:Facts.State) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner> & Facts.State:
102	  match returned:
103	    case (stream,reading):run_reading_traced(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~observed,~accepted,~synchronize,world,family,stream,reader,registry,id,tick,args,reading,trace)
104	def run_leaf_traced(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~observed:Facts.State -> W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O> & Facts.State,~accepted:O -> O & Bool,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,world:W.World<S,C,R,P>,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,+id:U32,+tick:Nat,args:A,returned:F & Leaf.Stream<S,E>,trace:Facts.State) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner> & Facts.State:
105	  match returned:
106	    case (family,stream):run_leaf_reading_traced(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~observed,~accepted,~synchronize,world,family,reader,registry,id,tick,args,Leaf.reading(~S,~E,stream,id,tick),trace)
107	def run_live_checked(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~observed:Facts.State -> W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O> & Facts.State,~accepted:O -> O & Bool,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,family:F,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,id:U32,tick:Nat,args:A,trace:Facts.State,checked:W.World<S,C,R,P> & Bool) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner> & Facts.State:
108	  match checked:
109	    case (world,False{}):(Ran{Runtime{world,family,1n+tick},reader,registry,Ev.Rejected{args}},trace)
110	    case (world,True{}):run_leaf_traced(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~observed,~accepted,~synchronize,world,reader,registry,id,tick,args,take(family),trace)
111	def run_metadata_checked(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~observed:Facts.State -> W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O> & Facts.State,~accepted:O -> O & Bool,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,family:F,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,id:U32,tick:Nat,args:A,trace:Facts.State,namespaceAllowed:Bool,checked:W.World<S,C,R,P> & Bool) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner> & Facts.State:
112	  match checked:
113	    case (world,allowed):run_live_checked(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~observed,~accepted,~synchronize,family,reader,registry,id,tick,args,trace, (world,Bool.and(namespaceAllowed,allowed)))
114	def run_registry_named(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~observed:Facts.State -> W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O> & Facts.State,~accepted:O -> O & Bool,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,family:F,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,id:U32,tick:Nat,args:A,trace:Facts.State,named:W.World<S,C,R,P> & U32) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner> & Facts.State:
115	  match registry named:
116	    case Sys.Registry{+namespace,+registryId,+name,+access,cursor}, (world,actual):run_metadata_checked(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~observed,~accepted,~synchronize,family,reader,Sys.Registry{namespace,registryId,name,access,cursor},id,tick,args,trace,U32.is_eq(namespace,actual),W.registration_matches(~S,~C,~R,~P,world,registryId,name,access))
117	def run_registered(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~observed:Facts.State -> W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O> & Facts.State,~accepted:O -> O & Bool,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,world:W.World<S,C,R,P>,family:F,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,id:U32,tick:Nat,args:A,trace:Facts.State) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner> & Facts.State:
118	  run_registry_named(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~observed,~accepted,~synchronize,family,reader,registry,id,tick,args,trace,W.namespace(~S,~C,~R,~P,world))
119	def run_checked_traced(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~observed:Facts.State -> W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O> & Facts.State,~accepted:O -> O & Bool,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,allowed:Bool,world:W.World<S,C,R,P>,family:F,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,id:U32,tick:Nat,args:A,trace:Facts.State) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner> & Facts.State:
120	  match allowed:
121	    case False{}:(Ran{Runtime{world,family,tick},reader,registry,Ev.Rejected{args}},trace)
122	    case True{}:run_registered(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~observed,~accepted,~synchronize,world,family,reader,registry,id,tick,args,trace)
123	def run_identity_traced(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~observed:Facts.State -> W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O> & Facts.State,~accepted:O -> O & Bool,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,family:F,tick:Nat,args:A,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,actual:U32,named:W.World<S,C,R,P> & U32,trace:Facts.State) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner> & Facts.State:
124	  match reader:
125	    case Reader{+namespace,+id,+registryId}:
126	      (world,actualNamespace)=named
127	      run_checked_traced(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~observed,~accepted,~synchronize,Bool.and(U32.is_eq(namespace,actualNamespace),U32.is_eq(registryId,actual)),world,family,Reader{namespace,id,registryId},registry,id,tick,args,trace)
128	def run_identified_traced(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~observed:Facts.State -> W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O> & Facts.State,~accepted:O -> O & Bool,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,runtime:Runtime<S,C,R,P,F>,reader:Reader<S,E,F,take,put>,args:A,identified:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner> & U32,trace:Facts.State) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner> & Facts.State:
129	  match runtime:
130	    case Runtime{world,family,tick}:
131	      (registry,actual)=identified
132	      run_identity_traced(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~observed,~accepted,~synchronize,family,tick,args,reader,registry,actual,W.namespace(~S,~C,~R,~P,world),trace)
133	# Validated reader/registry routing with trace-aware runner and semantic accepted
134	# callback. Namespace/id mismatch rejects before invocation and returns Args;
135	# actual registry metadata is also checked. Read unread values in stream order
136	# with lag status. Success advances cursor and synchronizes returned publications;
137	# Sys failure retains unread position. accepted(False) restores prior selected
138	# positions despite transport success, preserving higher-level semantic retry.
139	# Return actual owners and fact state; no payload copying, implicit barrier or
140	# automatic rollback of arbitrary callback effects is supplied.
141	def run_traced(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~observed:Facts.State -> W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O> & Facts.State,~accepted:O -> O & Bool,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,runtime:Runtime<S,C,R,P,F>,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,args:A,trace:Facts.State) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner> & Facts.State:
142	  run_identified_traced(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~observed,~accepted,~synchronize,runtime,reader,args,Sys.identity(~S,~C,~R,~P,~Ev.Input<E,A>,~Error,~O,~runner,registry),trace)
143	def accept_all(~O:Type,value:O) -> O & Bool:(value,True{})
144	
145	def unobserved(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,trace:Facts.State,world:W.World<S,C,R,P>,args:Ev.Input<E,A>) -> Sys.Outcome<W.World<S,C,R,P>,Error,O> & Facts.State:
146	  (runner(world,args),trace)
147	def without_trace(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,result:RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner> & Facts.State) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner>:
148	  match result:
149	    case (result,_):result
150	def run_synchronized(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,tick:Nat,output:O,returned:W.World<S,C,R,P> & F) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner>:
151	  without_trace(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,run_synchronized_traced(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~unobserved(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner),reader,registry,tick,output,returned,Facts.Off{}))
152	def run_outcome(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,family:F,+stream:Leaf.Stream<S,E>,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,+id:U32,+tick:Nat,outcome:Sys.Outcome<W.World<S,C,R,P>,Error,O>) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner>:
153	  without_trace(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,run_outcome_traced(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~unobserved(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner),~accept_all(~O),~synchronize,family,stream,reader,registry,id,tick,outcome,Facts.Off{}))
154	def run_result(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,family:F,stream:Leaf.Stream<S,E>,reader:Reader<S,E,F,take,put>,id:U32,tick:Nat,result:Sys.RunResult<S,C,R,P,Ev.Input<E,A>,Error,O,runner>) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner>:
155	  without_trace(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,run_result_traced(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~unobserved(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner),~accept_all(~O),~synchronize,family,stream,reader,id,tick,(result,Facts.Off{})))
156	def run_reading(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,world:W.World<S,C,R,P>,family:F,stream:Leaf.Stream<S,E>,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,id:U32,tick:Nat,args:A,reading:Ev.Reading<E>) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner>:
157	  without_trace(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,run_reading_traced(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~unobserved(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner),~accept_all(~O),~synchronize,world,family,stream,reader,registry,id,tick,args,reading,Facts.Off{}))
158	def run_leaf_reading(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,world:W.World<S,C,R,P>,family:F,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,id:U32,tick:Nat,args:A,returned:Leaf.Stream<S,E> & Ev.Reading<E>) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner>:
159	  without_trace(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,run_leaf_reading_traced(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~unobserved(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner),~accept_all(~O),~synchronize,world,family,reader,registry,id,tick,args,returned,Facts.Off{}))
160	def run_leaf(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,world:W.World<S,C,R,P>,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,+id:U32,+tick:Nat,args:A,returned:F & Leaf.Stream<S,E>) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner>:
161	  without_trace(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,run_leaf_traced(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~unobserved(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner),~accept_all(~O),~synchronize,world,reader,registry,id,tick,args,returned,Facts.Off{}))
162	def run_checked(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,allowed:Bool,world:W.World<S,C,R,P>,family:F,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,id:U32,tick:Nat,args:A) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner>:
163	  without_trace(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,run_checked_traced(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~unobserved(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner),~accept_all(~O),~synchronize,allowed,world,family,reader,registry,id,tick,args,Facts.Off{}))
164	def run_identity(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,family:F,tick:Nat,args:A,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,actual:U32,named:W.World<S,C,R,P> & U32) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner>:
165	  without_trace(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,run_identity_traced(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~unobserved(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner),~accept_all(~O),~synchronize,family,tick,args,reader,registry,actual,named,Facts.Off{}))
166	def run_identified(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,runtime:Runtime<S,C,R,P,F>,reader:Reader<S,E,F,take,put>,args:A,identified:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner> & U32) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner>:
167	  without_trace(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,run_identified_traced(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~unobserved(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner),~accept_all(~O),~synchronize,runtime,reader,args,identified,Facts.Off{}))
168	# Untraced routing using the same identity/registry admission and ownership path.
169	# Every Sys.Succeeded output is accepted here; adapters encoding semantic failure
170	# in O must reconcile it or use run_traced with an acceptance callback.
171	# Rejected returns Args, Failed does not promise consumed Args recovery. Tick
172	# changes follow the routing branch, not an ordinary lifecycle-reader cursor.
173	def run(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,~synchronize:W.World<S,C,R,P> -> F -> Nat -> W.World<S,C,R,P> & F,runtime:Runtime<S,C,R,P,F>,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,args:A) -> RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner>:
174	  without_trace(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,run_traced(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner,~unobserved(~S,~C,~R,~P,~E,~F,~A,~Error,~O,~take,~put,~runner),~accept_all(~O),~synchronize,runtime,reader,registry,args,Facts.Off{}))
175	
176	# Execution-context result retaining actual World/trace, family, routing tick,
177	# reader, registry and completion separately. Not a copied runtime checkpoint.
178	type ContextRunResult<S:Data,C:Type,R:Type,P:Data,E:Data,F:Type,A:Type,Error:Data,O:Type,-take:F -> F & Leaf.Stream<S,E>,-put:F -> Leaf.Stream<S,E> -> F,-runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>> is Type:
179	  ContextRan{context:Ctx.Context<W.World<S,C,R,P>>,family:F,tick:Nat,reader:Reader<S,E,F,take,put>,registry:Sys.Registry<S,C,R,P,Ev.Input<E,A>,Error,O,runner>,completion:Ev.Completion<Error,O,A>}
180	# Advanced transport from traced route result to context form, preserving all
181	# actual owners and completion; does not execute or acknowledge another reader.
182	def context_returned(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~A:Type,~Error:Data,~O:Type,~take:F -> F & Leaf.Stream<S,E>,~put:F -> Leaf.Stream<S,E> -> F,~runner:W.World<S,C,R,P> -> Ev.Input<E,A> -> Sys.Outcome<W.World<S,C,R,P>,Error,O>,result:RunResult<S,C,R,P,E,F,A,Error,O,take,put,runner> & Facts.State) -> ContextRunResult<S,C,R,P,E,F,A,Error,O,take,put,runner>:
183	  match result:
184	    case (Ran{Runtime{world,family,tick},reader,registry,completion},trace):ContextRan{Ctx.Context{world,trace},family,tick,reader,registry,completion}