event_family_routing.bend
bendvy-ecs-core@0.1.0.0 · 184 lines · 0 definitions
1import Base
2import bendvy-ecs-core@0.1.0.0/execution_context.bend as Ctx
3import bendvy-ecs-core@0.1.0.0/world.bend as W
4import bendvy-ecs-core@0.1.0.0/system.bend as Sys
5import bendvy-ecs-core@0.1.0.0/event_runtime.bend as Ev
6import bendvy-ecs-core@0.1.0.0/trace_facts.bend as Facts
7import bendvy-ecs-core@0.1.0.0/ordinary_event_declaration.bend as Event
8import bendvy-ecs-core@0.1.0.0/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.
13type 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.
17type 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.
21type 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>}
24def 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}
28def 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))
32def 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{}})]))
36def 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)
40def 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)
43def 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.
49def 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.
56type 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>}
58def 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)
61def 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)
64def 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}
67def 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)
70def 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)
73def 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)
77def 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)
80def 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)
84def 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)
88def 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})
91def 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))
95def 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}))
98def 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))
101def 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)
104def 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)
107def 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)
111def 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)))
114def 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))
117def 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))
119def 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)
123def 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)
128def 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.
141def 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)
143def accept_all(~O:Type,value:O) -> O & Bool:(value,True{})
144
145def 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)
147def 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
150def 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{}))
152def 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{}))
154def 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{})))
156def 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{}))
158def 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{}))
160def 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{}))
162def 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{}))
164def 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{}))
166def 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.
173def 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.
178type 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.
182def 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}