1	import Base
2	import ./change_tick.bend as Tick
3	import ./ordinary_machine_initialization.bend as Init
4	import ./ordinary_machine_declaration.bend as OD
5	import ./ordinary_machine_handler_bundle.bend as Classic
6	import ./ordinary_machine_handler_bundle_context.bend as Operation
7	import ./trace_facts.bend as Facts
8	import ./ordinary_machine_schedule.bend as Ordinary
9	import ./machine_handler_bundle.bend as B
10	import ./machine_handler_phases.bend as Phase
11	import ./machine_handlers.bend as H
12	import ./machine_stream.bend as St
13	import ./machine.bend as M
14	import ./world.bend as W
15	import ./system.bend as Sys
16	import ./schedule.bend as Sch
17	import ./event_runtime.bend as Ev
18	
19	def take_world(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,world:W.World<S,C,R,E>) -> W.World<S,C,R,E> & M.Slot<S,K,V>:
20	  W.observe_resource(~S,~C,~R,~E,~M.Slot<S,K,V>,~Init.take_slot(~S,~K,~V,~R,~take,~put),world)
21	def put_resource(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~same:V -> V -> Bool,resource:R,value:M.Slot<S,K,V>) -> R & Unit:
22	  (Init.put_slot(~S,~K,~V,~R,~take,~put,~same,resource,value),Unit{})
23	def returned_world(~S:Data,~C:Type,~R:Type,~E:Data,pair:W.World<S,C,R,E> & Unit) -> W.World<S,C,R,E>:
24	  match pair:
25	    case (world,_):world
26	def put_world(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~same:V -> V -> Bool,world:W.World<S,C,R,E>,value:M.Slot<S,K,V>) -> W.World<S,C,R,E>:
27	  returned_world(~S,~C,~R,~E,Init.with_resource(~S,~C,~R,~E,~Unit,(resource => put_resource(~S,~K,~V,~R,~take,~put,~C,~E,~same,resource,value)),world))
28	def stream_taken(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,pair:R & Init.State<S,K,V>) -> R & St.Stream<V>:
29	  match pair:
30	    case (resource,Init.State{slot,+stream,revision}):(put(resource,Init.State{slot,stream,revision}),stream)
31	def stream_put_taken(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,stream:St.Stream<V>,pair:R & Init.State<S,K,V>) -> R & Unit:
32	  match pair:
33	    case (resource,Init.State{slot,_,revision}):(put(resource,Init.State{slot,stream,revision}),Unit{})
34	def stream_put(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,world:W.World<S,C,R,E>,stream:St.Stream<V>) -> W.World<S,C,R,E>:
35	  returned_world(~S,~C,~R,~E,Init.with_resource(~S,~C,~R,~E,~Unit,(resource => stream_put_taken(~S,~K,~V,~R,~take,~put,~C,~E,stream,take(resource))),world))
36	def published(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,tick:Nat,event:M.Transition<V>,pair:W.World<S,C,R,E> & St.Stream<V>) -> W.World<S,C,R,E>:
37	  match pair:
38	    case (world,stream):stream_put(~S,~K,~V,~R,~take,~put,~C,~E,world,St.publish(~V,stream,tick,event))
39	def publish_clocked(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,event:M.Transition<V>,pair:W.World<S,C,R,E> & Tick.Tick) -> W.World<S,C,R,E>:
40	  match pair:
41	    case (world,tick):published(~S,~K,~V,~R,~take,~put,~C,~E,Tick.total(tick),event,W.observe_resource(~S,~C,~R,~E,~St.Stream<V>,~(resource => stream_taken(~S,~K,~V,~R,~take,~put,~C,~E,take(resource))),world))
42	# Stream publication advances administrative time independently of component run ticks.
43	def publish(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,world:W.World<S,C,R,E>,event:M.Transition<V>) -> W.World<S,C,R,E>:
44	  publish_clocked(~S,~K,~V,~R,~take,~put,~C,~E,event,W.advance_clock(~S,~C,~R,~E,world))
45	def last(~V:Data,items:List<&2,M.Transition<V>>,prior:Maybe<&2,M.Transition<V>>) -> Maybe<&2,M.Transition<V>>:
46	  match items:
47	    case []:prior
48	    case value <> tail:last(~V,tail,Some{value})
49	type Opening<S:Data,K:Data,V:Data,C:Type,R:Type,E:Data> is Type:
50	  Opened{world:W.World<S,C,R,E>,reader:St.Reader<S,K>,latest:Maybe<&2,M.Transition<V>>,readThrough:Nat}
51	  OpenRejected{world:W.World<S,C,R,E>,reader:St.Reader<S,K>}
52	def opened_finished(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,world:W.World<S,C,R,E>,latest:Maybe<&2,M.Transition<V>>,tick:Nat,pair:St.Reader<S,K> & St.Stream<V>) -> Opening<S,K,V,C,R,E>:
53	  match pair:
54	    case (reader,stream):Opened{stream_put(~S,~K,~V,~R,~take,~put,~C,~E,world,stream),reader,latest,tick}
55	def opened(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,world:W.World<S,C,R,E>,+tick:Nat,result:St.OpenResult<S,K,V>) -> Opening<S,K,V,C,R,E>:
56	  match result:
57	    case St.ReaderRefused{reader,stream}:OpenRejected{stream_put(~S,~K,~V,~R,~take,~put,~C,~E,world,stream),reader}
58	    case St.Opened{reader,stream,Ev.Reading{values,_}}:opened_finished(~S,~K,~V,~R,~take,~put,~C,~E,world,last(~V,values,None{}),tick,St.finish(~S,~K,~V,reader,stream,tick,True{}))
59	def open_stream(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,reader:St.Reader<S,K>,namespace:U32,+tick:Nat,pair:W.World<S,C,R,E> & St.Stream<V>) -> Opening<S,K,V,C,R,E>:
60	  match pair:
61	    case (world,stream):opened(~S,~K,~V,~R,~take,~put,~C,~E,world,tick,St.open(~S,~K,~V,reader,stream,namespace,tick))
62	def open_clocked(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,reader:St.Reader<S,K>,namespace:U32,pair:W.World<S,C,R,E> & Tick.Tick) -> Opening<S,K,V,C,R,E>:
63	  match pair:
64	    case (world,tick):open_stream(~S,~K,~V,~R,~take,~put,~C,~E,reader,namespace,Tick.total(tick),W.observe_resource(~S,~C,~R,~E,~St.Stream<V>,~(resource => stream_taken(~S,~K,~V,~R,~take,~put,~C,~E,take(resource))),world))
65	def open_namespaced(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,reader:St.Reader<S,K>,pair:W.World<S,C,R,E> & U32) -> Opening<S,K,V,C,R,E>:
66	  match pair:
67	    case (world,namespace):open_clocked(~S,~K,~V,~R,~take,~put,~C,~E,reader,namespace,W.clock(~S,~C,~R,~E,world))
68	def open(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,reader:St.Reader<S,K>,world:W.World<S,C,R,E>) -> Opening<S,K,V,C,R,E>:
69	  open_namespaced(~S,~K,~V,~R,~take,~put,~C,~E,reader,W.namespace(~S,~C,~R,~E,world))
70	def reader_trace(~name:String,state:Facts.State,namespace:U32,+id:U32,lagged:Bool) -> Facts.State:
71	  match state:
72	    case Facts.Off{}:Facts.Off{}
73	    case Facts.On{facts}:Facts.On{Facts.ReaderFact{namespace,id,"machine." ++ name ++ ".initial-marker",id,"machine." ++ name ++ ".transition",lagged} <> facts}
74	def opened_traced(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~name:String,world:W.World<S,C,R,E>,+tick:Nat,result:St.OpenResult<S,K,V>,trace:Facts.State) -> Opening<S,K,V,C,R,E> & Facts.State:
75	  match result:
76	    case St.ReaderRefused{reader,stream}:(opened(~S,~K,~V,~R,~take,~put,~C,~E,world,tick,St.ReaderRefused{reader,stream}),trace)
77	    case St.Opened{St.Reader{+namespace,+id},stream,Ev.Reading{values,+lagged}}:(opened(~S,~K,~V,~R,~take,~put,~C,~E,world,tick,St.Opened{St.Reader{namespace,id},stream,Ev.Reading{values,lagged}}),reader_trace(~name,trace,namespace,id,lagged))
78	def open_stream_traced(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~name:String,reader:St.Reader<S,K>,namespace:U32,+tick:Nat,pair:W.World<S,C,R,E> & St.Stream<V>,trace:Facts.State) -> Opening<S,K,V,C,R,E> & Facts.State:
79	  match pair:
80	    case (world,stream):opened_traced(~S,~K,~V,~R,~take,~put,~C,~E,~name,world,tick,St.open(~S,~K,~V,reader,stream,namespace,tick),trace)
81	def open_clocked_traced(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~name:String,reader:St.Reader<S,K>,namespace:U32,pair:W.World<S,C,R,E> & Tick.Tick,trace:Facts.State) -> Opening<S,K,V,C,R,E> & Facts.State:
82	  match pair:
83	    case (world,tick):open_stream_traced(~S,~K,~V,~R,~take,~put,~C,~E,~name,reader,namespace,Tick.total(tick),W.observe_resource(~S,~C,~R,~E,~St.Stream<V>,~(resource => stream_taken(~S,~K,~V,~R,~take,~put,~C,~E,take(resource))),world),trace)
84	def open_namespaced_traced(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~name:String,reader:St.Reader<S,K>,pair:W.World<S,C,R,E> & U32,trace:Facts.State) -> Opening<S,K,V,C,R,E> & Facts.State:
85	  match pair:
86	    case (world,namespace):open_clocked_traced(~S,~K,~V,~R,~take,~put,~C,~E,~name,reader,namespace,W.clock(~S,~C,~R,~E,world),trace)
87	def open_traced(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~name:String,reader:St.Reader<S,K>,world:W.World<S,C,R,E>,trace:Facts.State) -> Opening<S,K,V,C,R,E> & Facts.State:
88	  open_namespaced_traced(~S,~K,~V,~R,~take,~put,~C,~E,~name,reader,W.namespace(~S,~C,~R,~E,world),trace)
89	def completed_stream(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,world:W.World<S,C,R,E>,pair:St.Reader<S,K> & St.Stream<V>) -> W.World<S,C,R,E> & St.Reader<S,K>:
90	  match pair:
91	    case (reader,stream):(stream_put(~S,~K,~V,~R,~take,~put,~C,~E,world,stream),reader)
92	def complete_taken(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,reader:St.Reader<S,K>,tick:Nat,success:Bool,pair:W.World<S,C,R,E> & St.Stream<V>) -> W.World<S,C,R,E> & St.Reader<S,K>:
93	  match pair:
94	    case (world,stream):completed_stream(~S,~K,~V,~R,~take,~put,~C,~E,world,St.finish(~S,~K,~V,reader,stream,tick,success))
95	def complete_clocked(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,reader:St.Reader<S,K>,success:Bool,pair:W.World<S,C,R,E> & Tick.Tick) -> W.World<S,C,R,E> & St.Reader<S,K>:
96	  match pair:
97	    case (world,tick):complete_taken(~S,~K,~V,~R,~take,~put,~C,~E,reader,Tick.total(tick),success,W.observe_resource(~S,~C,~R,~E,~St.Stream<V>,~(resource => stream_taken(~S,~K,~V,~R,~take,~put,~C,~E,take(resource))),world))
98	def complete(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,reader:St.Reader<S,K>,success:Bool,world:W.World<S,C,R,E>) -> W.World<S,C,R,E> & St.Reader<S,K>:
99	  complete_clocked(~S,~K,~V,~R,~take,~put,~C,~E,reader,success,W.clock(~S,~C,~R,~E,world))
100	type Owners<S:Data,K:Data,V:Data,Q:Data,C:Type,R:Type,E:Data,-runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>> is Type:
101	  Owners{ordinary:Operation.Owners<S,K,V,Q,C,R,E,runner>,reader:St.Reader<S,K>,readThrough:Nat}
102	type ObservedMarkerRun<S:Data,K:Data,V:Data,Q:Data,C:Type,R:Type,E:Data,-runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>> is Type:
103	  ObservedMarkerRun{reader:St.Reader<S,K>,result:Operation.MarkerResult<S,K,V,Q,C,R,E,runner>}
104	def opened_for_owners(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,ordinary:Operation.Owners<S,K,V,Q,C,R,E,runner>,pair:Opening<S,K,V,C,R,E> & Facts.State) -> Operation.Owners<S,K,V,Q,C,R,E,runner> & Opening<S,K,V,C,R,E>:
105	  match pair:
106	    case (opened,trace):(Operation.replaced_trace(~S,~K,~V,~Q,~C,~R,~E,~runner,ordinary,trace),opened)
107	def open_for_owners(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,ordinary:Operation.Owners<S,K,V,Q,C,R,E,runner>,reader:St.Reader<S,K>,world:W.World<S,C,R,E>) -> Operation.Owners<S,K,V,Q,C,R,E,runner> & Opening<S,K,V,C,R,E>:
108	  match ordinary:
109	    case Operation.Pending{entries,trace}:opened_for_owners(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,Operation.Pending{entries,Facts.Off{}},open_traced(~S,~K,~V,~R,~take,~put,~C,~E,~name,reader,world,trace))
110	    case Operation.Unavailable{entries,trace}:opened_for_owners(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,Operation.Unavailable{entries,Facts.Off{}},open_traced(~S,~K,~V,~R,~take,~put,~C,~E,~name,reader,world,trace))
111	    case Operation.Selected{positions,kept,active,phase,trace}:opened_for_owners(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,Operation.Selected{positions,kept,active,phase,Facts.Off{}},open_traced(~S,~K,~V,~R,~take,~put,~C,~E,~name,reader,world,trace))
112	def initial_partition(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,namespace:U32,to:V,partition:B.Partition<S,K,V,Q,C,R,E,runner>,trace:Facts.State) -> Operation.Owners<S,K,V,Q,C,R,E,runner>:
113	  match partition:
114	    case B.Partition{positions,kept,handlers}:Operation.Selected{positions,kept,Phase.Owners{handlers,Phase.InitialReady{to}},H.Enter{},trace}
115	def initial_selected(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,ordinary:Operation.Owners<S,K,V,Q,C,R,E,runner>,opened:Opening<S,K,V,C,R,E>) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
116	  match ordinary opened:
117	    case Operation.Pending{entries,trace} Opened{world,reader,Some{M.Initial{+to}},through}:(Owners{initial_partition(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,0,to,B.partition_initial(~S,~K,~V,~Q,~C,~R,~E,~runner,~same,entries,to),trace),reader,through},Sys.Succeeded{world,Unit{}})
118	    case Operation.Selected{positions,kept,Phase.Owners{handlers,Phase.Idle{}},phase,trace} Opened{world,reader,Some{M.Initial{to}},through}:(Owners{Operation.Selected{positions,kept,Phase.Owners{handlers,Phase.InitialReady{to}},phase,trace},reader,through},Sys.Succeeded{world,Unit{}})
119	    case ordinary Opened{world,reader,_,through}:(Owners{ordinary,reader,through},Sys.Succeeded{world,Unit{}})
120	    case ordinary OpenRejected{world,reader}:(Owners{ordinary,reader,0n},Sys.Failed{world,"InitialReaderRejected"})
121	def initial_opened(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,pair:Operation.Owners<S,K,V,Q,C,R,E,runner> & Opening<S,K,V,C,R,E>) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
122	  match pair:
123	    case (ordinary,opened):initial_selected(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,ordinary,opened)
124	def apply_observed(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,reader:St.Reader<S,K>,result:Operation.Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
125	  match result:
126	    case (ordinary,Sys.Failed{world,error}):(Owners{ordinary,reader,0n},Sys.Failed{world,error})
127	    case (Operation.Unavailable{entries,trace},Sys.Succeeded{world,_}):(Owners{Operation.Unavailable{entries,trace},reader,0n},Sys.Succeeded{world,Unit{}})
128	    case (Operation.Selected{positions,kept,Phase.Owners{handlers,Phase.Ready{from,to,skip}},phase,trace},Sys.Succeeded{world,_}):(Owners{Operation.Selected{positions,kept,Phase.Owners{handlers,Phase.Ready{from,to,skip}},phase,trace},reader,0n},Sys.Succeeded{world,Unit{}})
129	    case (ordinary,Sys.Succeeded{world,_}):initial_opened(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,open_for_owners(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,ordinary,reader,world))
130	def apply(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,owners:Owners<S,K,V,Q,C,R,E,runner>,world:W.World<S,C,R,E>) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
131	  match owners:
132	    case Owners{ordinary,reader,_}:apply_observed(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,reader,Operation.apply(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take_world(~S,~K,~V,~R,~take,~put,~C,~E),~put_world(~S,~K,~V,~R,~take,~put,~C,~E,~same),~publish(~S,~K,~V,~R,~take,~put,~C,~E),~same,~requirement_same,~has,~frame,ordinary,world))
133	def phase_returned(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,reader:St.Reader<S,K>,through:Nat,result:Operation.Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
134	  match result:
135	    case (ordinary,outcome):(Owners{ordinary,reader,through},outcome)
136	def exit(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,owners:Owners<S,K,V,Q,C,R,E,runner>,world:W.World<S,C,R,E>) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
137	  match owners:
138	    case Owners{ordinary,reader,through}:phase_returned(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,reader,through,Operation.exit(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take_world(~S,~K,~V,~R,~take,~put,~C,~E),~put_world(~S,~K,~V,~R,~take,~put,~C,~E,~same),~publish(~S,~K,~V,~R,~take,~put,~C,~E),~same,~requirement_same,~has,~frame,ordinary,world))
139	def checkpoint_opened(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,ordinary:Operation.Owners<S,K,V,Q,C,R,E,runner>,opened:Opening<S,K,V,C,R,E>) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
140	  match opened:
141	    case Opened{world,reader,_,through}:(Owners{ordinary,reader,through},Sys.Succeeded{world,Unit{}})
142	    case OpenRejected{world,reader}:(Owners{ordinary,reader,0n},Sys.Failed{world,"InitialReaderRejected"})
143	def checkpoint_paired(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,pair:Operation.Owners<S,K,V,Q,C,R,E,runner> & Opening<S,K,V,C,R,E>) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
144	  match pair:
145	    case (ordinary,opened):checkpoint_opened(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,ordinary,opened)
146	def transition_returned(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,reader:St.Reader<S,K>,through:Nat,result:Operation.Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
147	  match result:
148	    case (Operation.Selected{positions,kept,Phase.Owners{handlers,Phase.Ready{from,to,skip}},phase,trace},Sys.Succeeded{world,_}):checkpoint_paired(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,open_for_owners(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,Operation.Selected{positions,kept,Phase.Owners{handlers,Phase.Ready{from,to,skip}},phase,trace},reader,world))
149	    case (ordinary,outcome):(Owners{ordinary,reader,through},outcome)
150	def transition(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,owners:Owners<S,K,V,Q,C,R,E,runner>,world:W.World<S,C,R,E>) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
151	  match owners:
152	    case Owners{ordinary,reader,through}:transition_returned(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,reader,through,Operation.transition(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take_world(~S,~K,~V,~R,~take,~put,~C,~E),~put_world(~S,~K,~V,~R,~take,~put,~C,~E,~same),~publish(~S,~K,~V,~R,~take,~put,~C,~E),~same,~requirement_same,~has,~frame,ordinary,world))
153	def enter(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,owners:Owners<S,K,V,Q,C,R,E,runner>,world:W.World<S,C,R,E>) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
154	  match owners:
155	    case Owners{ordinary,reader,through}:phase_returned(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,reader,through,Operation.enter(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take_world(~S,~K,~V,~R,~take,~put,~C,~E),~put_world(~S,~K,~V,~R,~take,~put,~C,~E,~same),~publish(~S,~K,~V,~R,~take,~put,~C,~E),~same,~requirement_same,~has,~frame,ordinary,world))
156	def finished_world(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,namespace:U32,ordinary:Operation.Owners<S,K,V,Q,C,R,E,runner>,steps:List<&2,Sch.Step>,observations:List<&2,Sch.Observation>,error:Maybe<&2,String>,pair:W.World<S,C,R,E> & St.Reader<S,K>) -> ObservedMarkerRun<S,K,V,Q,C,R,E,runner>:
157	  match pair:
158	    case (world,reader):ObservedMarkerRun{reader,Operation.marked(~S,~K,~V,~Q,~C,~R,~E,~runner,steps,observations,Operation.finished(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take_world(~S,~K,~V,~R,~take,~put,~C,~E),~put_world(~S,~K,~V,~R,~take,~put,~C,~E,~same),~publish(~S,~K,~V,~R,~take,~put,~C,~E),~same,~requirement_same,~has,~frame,namespace,ordinary,world,error))}
159	def succeeded(error:Maybe<&2,String>) -> Bool:
160	  match error:
161	    case None{}:True{}
162	    case Some{_}:False{}
163	def finished(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,namespace:U32,owners:Owners<S,K,V,Q,C,R,E,runner>,world:W.World<S,C,R,E>,steps:List<&2,Sch.Step>,observations:List<&2,Sch.Observation>,+error:Maybe<&2,String>) -> ObservedMarkerRun<S,K,V,Q,C,R,E,runner>:
164	  match owners:
165	    case Owners{ordinary,reader,through}:finished_world(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,namespace,ordinary,steps,observations,error,(world,reader))
166	def returned(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,result:Sch.RunResult<S,C,R,E,Owners<S,K,V,Q,C,R,E,runner>,String>) -> ObservedMarkerRun<S,K,V,Q,C,R,E,runner>:
167	  match result:
168	    case Sch.Finished{Sch.Schedule{namespace,_,steps,owners},world,observations}:finished(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,namespace,owners,world,steps,observations,None{})
169	    case Sch.Failed{Sch.Schedule{namespace,_,steps,owners},world,error,observations}:finished(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,namespace,owners,world,steps,observations,Some{error})
170	    case Sch.Rejected{Sch.Schedule{namespace,_,steps,owners},world}:finished(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,namespace,owners,world,steps,[],Some{"schedule-rejected"})
171	def barrier_returned(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,reader:St.Reader<S,K>,through:Nat,pair:Operation.Owners<S,K,V,Q,C,R,E,runner> & W.World<S,C,R,E>) -> Owners<S,K,V,Q,C,R,E,runner> & W.World<S,C,R,E>:
172	  match pair:
173	    case (ordinary,world):(Owners{ordinary,reader,through},world)
174	def barrier(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,owners:Owners<S,K,V,Q,C,R,E,runner>,world:W.World<S,C,R,E>) -> Owners<S,K,V,Q,C,R,E,runner> & W.World<S,C,R,E>:
175	  match owners:
176	    case Owners{ordinary,reader,through}:barrier_returned(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,reader,through,Operation.barrier(~S,~K,~V,~Q,~C,~R,~E,~runner,ordinary,world))
177	def phase_started(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,owners:Owners<S,K,V,Q,C,R,E,runner>,id:U32) -> Owners<S,K,V,Q,C,R,E,runner>:
178	  match owners:
179	    case Owners{ordinary,reader,through}:Owners{Operation.phase_started(~S,~K,~V,~Q,~C,~R,~E,~runner,ordinary,id),reader,through}
180	def dispatch_shared(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,owners:Owners<S,K,V,Q,C,R,E,runner>,world:W.World<S,C,R,E>,+id:U32) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
181	  Ordinary.dispatch(~S,~C,~R,~E,~Owners<S,K,V,Q,C,R,E,runner>,~String,~apply(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame),~exit(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame),~transition(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame),~enter(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame),phase_started(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,owners,id),world,id)
182	def dispatch(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,owners:Owners<S,K,V,Q,C,R,E,runner>,world:W.World<S,C,R,E>,id:U32) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
183	  dispatch_shared(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,owners,world,id)
184	def installed(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,world:W.World<S,C,R,E>,build:Sch.Build<S,C,R,E,Owners<S,K,V,Q,C,R,E,runner>>) -> ObservedMarkerRun<S,K,V,Q,C,R,E,runner>:
185	  match build:
186	    case Sch.Built{schedule}:returned(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,Sch.run_with_barrier(~S,~C,~R,~E,~Owners<S,K,V,Q,C,R,E,runner>,~String,~dispatch(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame),~Ordinary.condition(~S,~C,~R,~E),~barrier(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame),schedule,world))
187	    case Sch.Invalid{owners}:finished(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,0,owners,world,[],[],Some{"invalid"})
188	def checked(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,declaration:Ordinary.Declaration<S>,namespace:U32,reader:St.Reader<S,K>,entries:List<&1,B.Scheduled<S,K,V,Q,C,R,E,runner>>,pair:W.World<S,C,R,E> & List<&2,Q>,trace:Facts.State) -> ObservedMarkerRun<S,K,V,Q,C,R,E,runner>:
189	  match pair:
190	    case (world,[]):installed(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,world,Ordinary.install(~S,~C,~R,~E,~Owners<S,K,V,Q,C,R,E,runner>,~String,declaration,namespace,Owners{Operation.Pending{entries,trace},reader,0n}))
191	    case (world,missing):ObservedMarkerRun{reader,Operation.MarkerResult{B.Returned{B.Bundle{namespace,entries},world,B.MissingRequirements{missing}},[],[],trace}}
192	def gathered(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,declaration:Ordinary.Declaration<S>,namespace:U32,reader:St.Reader<S,K>,world:W.World<S,C,R,E>,pair:List<&1,B.Scheduled<S,K,V,Q,C,R,E,runner>> & List<&2,Q>,trace:Facts.State) -> ObservedMarkerRun<S,K,V,Q,C,R,E,runner>:
193	  match pair:
194	    case (entries,needs):checked(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,declaration,namespace,reader,entries,B.missing(~S,~C,~R,~E,~Q,~has,B.collect(~Q,~requirement_same,needs,[]),world),trace)
195	def allowed(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,declaration:Ordinary.Declaration<S>,yes:Bool,namespace:U32,reader:St.Reader<S,K>,entries:List<&1,B.Scheduled<S,K,V,Q,C,R,E,runner>>,world:W.World<S,C,R,E>,trace:Facts.State) -> ObservedMarkerRun<S,K,V,Q,C,R,E,runner>:
196	  match yes:
197	    case False{}:ObservedMarkerRun{reader,Operation.MarkerResult{B.Returned{B.Bundle{namespace,entries},world,B.ForeignBundle{}},[],[],trace}}
198	    case True{}:gathered(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,declaration,namespace,reader,world,B.requirements(~S,~K,~V,~Q,~C,~R,~E,~runner,entries),trace)
199	def namespaced(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,declaration:Ordinary.Declaration<S>,+namespace:U32,reader:St.Reader<S,K>,entries:List<&1,B.Scheduled<S,K,V,Q,C,R,E,runner>>,pair:W.World<S,C,R,E> & U32,trace:Facts.State) -> ObservedMarkerRun<S,K,V,Q,C,R,E,runner>:
200	  match reader pair:
201	    case St.Reader{+owner,id}, (world,+actual):allowed(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,declaration,Bool.and(U32.is_eq(namespace,actual),U32.is_eq(owner,actual)),namespace,St.Reader{owner,id},entries,world,trace)
202	def run_observed(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,declaration:Ordinary.Declaration<S>,bundle:B.Bundle<S,K,V,Q,C,R,E,runner>,reader:St.Reader<S,K>,world:W.World<S,C,R,E>,trace:Facts.State) -> ObservedMarkerRun<S,K,V,Q,C,R,E,runner>:
203	  match bundle:
204	    case B.Bundle{namespace,entries}:namespaced(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,declaration,namespace,reader,entries,W.namespace(~S,~C,~R,~E,world),trace)
205	type MarkerRun<S:Data,K:Data,V:Data,Q:Data,C:Type,R:Type,E:Data,-runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>> is Type:
206	  MarkerRun{reader:St.Reader<S,K>,result:Classic.MarkerResult<S,K,V,Q,C,R,E,runner>}
207	def classic_returned(~S:Data,~K:Data,~V:Data,~Q:Data,~C:Type,~R:Type,~E:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,value:ObservedMarkerRun<S,K,V,Q,C,R,E,runner>) -> MarkerRun<S,K,V,Q,C,R,E,runner>:
208	  match value:
209	    case ObservedMarkerRun{reader,Operation.MarkerResult{result,steps,observations,_}}:MarkerRun{reader,Classic.MarkerResult{result,steps,observations}}
210	def run(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,declaration:Ordinary.Declaration<S>,bundle:B.Bundle<S,K,V,Q,C,R,E,runner>,reader:St.Reader<S,K>,world:W.World<S,C,R,E>) -> MarkerRun<S,K,V,Q,C,R,E,runner>:
211	  classic_returned(~S,~K,~V,~Q,~C,~R,~E,~runner,run_observed(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~Classic.unobserved(~S,~C,~R,~E,~V,~runner),~"",~same,~requirement_same,~has,~frame,declaration,bundle,reader,world,Facts.Off{}))
212	# Normal application construction allocates its marker reader through World.register.
213	type Application<S:Data,K:Data,V:Data,Q:Data,C:Type,R:Type,E:Data,-runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>> is Type:
214	  Application{world:W.World<S,C,R,E>,bundle:B.Bundle<S,K,V,Q,C,R,E,runner>,reader:St.Reader<S,K>,declaration:Ordinary.Declaration<S>}
215	type Definition<S:Data,K:Data,V:Data,Q:Data,C:Type,R:Type,E:Data,-runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>> is Type:
216	  Bound{app:Application<S,K,V,Q,C,R,E,runner>}
217	  BindRejected{world:W.World<S,C,R,E>,bundle:B.Bundle<S,K,V,Q,C,R,E,runner>,declaration:Ordinary.Declaration<S>}
218	def bound(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,namespace:U32,bundle:B.Bundle<S,K,V,Q,C,R,E,runner>,declaration:Ordinary.Declaration<S>,pair:W.World<S,C,R,E> & W.Registration) -> Definition<S,K,V,Q,C,R,E,runner>:
219	  match pair:
220	    case (world,W.Registered{id}):Bound{Application{world,bundle,St.Reader{namespace,id},declaration}}
221	    case (world,W.RegistrationRejected{_}):BindRejected{world,bundle,declaration}
222	def bind_allowed(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,~initial:OD.Declaration<S,K,V,R,Init.take_slot(~S,~K,~V,~R,~take,~put)>,allowed:Bool,namespace:U32,bundle:B.Bundle<S,K,V,Q,C,R,E,runner>,declaration:Ordinary.Declaration<S>,world:W.World<S,C,R,E>) -> Definition<S,K,V,Q,C,R,E,runner>:
223	  match allowed:
224	    case False{}:BindRejected{world,bundle,declaration}
225	    case True{}:bound(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~same,~requirement_same,~has,~frame,namespace,bundle,declaration,W.register(~S,~C,~R,~E,world,"machine." ++ OD.name(~S,~K,~V,~R,~Init.take_slot(~S,~K,~V,~R,~take,~put),initial) ++ ".initial-marker",["machine." ++ OD.name(~S,~K,~V,~R,~Init.take_slot(~S,~K,~V,~R,~take,~put),initial) ++ ".transition.read"]))
226	def bind_namespaced(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,~initial:OD.Declaration<S,K,V,R,Init.take_slot(~S,~K,~V,~R,~take,~put)>,bundle:B.Bundle<S,K,V,Q,C,R,E,runner>,declaration:Ordinary.Declaration<S>,pair:W.World<S,C,R,E> & U32) -> Definition<S,K,V,Q,C,R,E,runner>:
227	  match bundle pair:
228	    case B.Bundle{+owner,entries}, (world,+namespace):bind_allowed(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~same,~requirement_same,~has,~frame,~initial,U32.is_eq(owner,namespace),namespace,B.Bundle{owner,entries},declaration,world)
229	def bind(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,~initial:OD.Declaration<S,K,V,R,Init.take_slot(~S,~K,~V,~R,~take,~put)>,declaration:Ordinary.Declaration<S>,bundle:B.Bundle<S,K,V,Q,C,R,E,runner>,world:W.World<S,C,R,E>) -> Definition<S,K,V,Q,C,R,E,runner>:
230	  bind_namespaced(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~same,~requirement_same,~has,~frame,~initial,bundle,declaration,W.namespace(~S,~C,~R,~E,world))
231	type AppRun<S:Data,K:Data,V:Data,Q:Data,C:Type,R:Type,E:Data,-runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>> is Type:
232	  Applied{app:Application<S,K,V,Q,C,R,E,runner>,status:B.Status<Q>,steps:List<&2,Sch.Step>,observations:List<&2,Sch.Observation>}
233	  RecoveryRequired{declaration:Ordinary.Declaration<S>,result:MarkerRun<S,K,V,Q,C,R,E,runner>}
234	def app_returned(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,declaration:Ordinary.Declaration<S>,result:MarkerRun<S,K,V,Q,C,R,E,runner>) -> AppRun<S,K,V,Q,C,R,E,runner>:
235	  match result:
236	    case MarkerRun{reader,Classic.MarkerResult{B.Returned{bundle,world,status},steps,observations}}:Applied{Application{world,bundle,reader,declaration},status,steps,observations}
237	    case result:RecoveryRequired{declaration,result}
238	def run_app(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,app:Application<S,K,V,Q,C,R,E,runner>) -> AppRun<S,K,V,Q,C,R,E,runner>:
239	  match app:
240	    case Application{world,bundle,reader,+declaration}:app_returned(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~same,~requirement_same,~has,~frame,declaration,run(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~same,~requirement_same,~has,~frame,declaration,bundle,reader,world))
241	
242	# Application methods retain marker and handler ownership across ordinary setup.
243	def init_app(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,~initial:OD.Declaration<S,K,V,R,Init.take_slot(~S,~K,~V,~R,~take,~put)>,~make:W.World<S,C,R,E> -> W.World<S,C,R,E> & V,app:Application<S,K,V,Q,C,R,E,runner>) -> Application<S,K,V,Q,C,R,E,runner>:
244	  match app:
245	    case Application{world,bundle,reader,declaration}:Application{Init.init_state(~S,~K,~V,~R,~take,~put,~C,~E,~initial,~make,world),bundle,reader,declaration}
246	def insert_app(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,~initial:OD.Declaration<S,K,V,R,Init.take_slot(~S,~K,~V,~R,~take,~put)>,app:Application<S,K,V,Q,C,R,E,runner>,value:V) -> Application<S,K,V,Q,C,R,E,runner>:
247	  match app:
248	    case Application{world,bundle,reader,declaration}:Application{Init.insert_state(~S,~K,~V,~R,~take,~put,~C,~E,~initial,world,value),bundle,reader,declaration}