1	import Base
2	import ./machine_handler_phases.bend as Phase
3	import ./machine_handler_phases_context.bend as PhaseContext
4	import ./execution_context.bend as Ctx
5	import ./trace_facts.bend as Facts
6	import ./world.bend as W
7	import ./system.bend as Sys
8	import ./machine.bend as M
9	import ./machine_handlers.bend as H
10	import ./machine_handler_bundle.bend as B
11	import ./schedule.bend as Sch
12	import ./ordinary_machine_schedule.bend as Ordinary
13	
14	# Bundle preflight precedes ordinary barrier; selected registry owners recover authored order.
15	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:
16	  Pending{entries:List<&1,B.Scheduled<S,K,V,Q,C,R,E,runner>>,trace:Facts.State}
17	  Unavailable{entries:List<&1,B.Scheduled<S,K,V,Q,C,R,E,runner>>,trace:Facts.State}
18	  Selected{positions:List<&2,B.Position<S,K,V,Q>>,kept:List<&1,H.Entry<S,C,R,E,V,runner>>,active:Phase.Owners<S,K,V,C,R,E,runner>,phase:H.Phase,trace:Facts.State}
19	type MarkerResult<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:
20	  MarkerResult{result:B.BundleResult<S,K,V,Q,C,R,E,runner>,steps:List<&2,Sch.Step>,observations:List<&2,Sch.Observation>,trace:Facts.State}
21	def unchanged(~S:Data,~C:Type,~R:Type,~E:Data,world:W.World<S,C,R,E>) -> W.World<S,C,R,E>:world
22	def phase_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>,~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,~take:W.World<S,C,R,E> -> W.World<S,C,R,E> & M.Slot<S,K,V>,~put:W.World<S,C,R,E> -> M.Slot<S,K,V> -> W.World<S,C,R,E>,~publish:W.World<S,C,R,E> -> M.Transition<V> -> W.World<S,C,R,E>,~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>,positions:List<&2,B.Position<S,K,V,Q>>,kept:List<&1,H.Entry<S,C,R,E,V,runner>>,phase:H.Phase,result:Phase.Owners<S,K,V,C,R,E,runner> & Sys.Outcome<Ctx.Context<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>:
23	  match result:
24	    case (active,Sys.Succeeded{Ctx.Context{world,trace},output}):(Selected{positions,kept,active,phase,trace},Sys.Succeeded{world,output})
25	    case (active,Sys.Failed{Ctx.Context{world,trace},error}):(Selected{positions,kept,active,phase,trace},Sys.Failed{world,error})
26	def applied(~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>,~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,~take:W.World<S,C,R,E> -> W.World<S,C,R,E> & M.Slot<S,K,V>,~put:W.World<S,C,R,E> -> M.Slot<S,K,V> -> W.World<S,C,R,E>,~publish:W.World<S,C,R,E> -> M.Transition<V> -> W.World<S,C,R,E>,~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>,positions:List<&2,B.Position<S,K,V,Q>>,kept:List<&1,H.Entry<S,C,R,E,V,runner>>,result:Phase.Owners<S,K,V,C,R,E,runner> & Sys.Outcome<Ctx.Context<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>:
27	  phase_returned(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~requirement_same,~has,~frame,positions,kept,H.Exit{},result)
28	def selected(~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>,~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,~take:W.World<S,C,R,E> -> W.World<S,C,R,E> & M.Slot<S,K,V>,~put:W.World<S,C,R,E> -> M.Slot<S,K,V> -> W.World<S,C,R,E>,~publish:W.World<S,C,R,E> -> M.Transition<V> -> W.World<S,C,R,E>,~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>,partition:B.Partition<S,K,V,Q,C,R,E,runner>,trace:Facts.State) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
29	  match partition:
30	    case B.Partition{positions,kept,handlers}:applied(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~requirement_same,~has,~frame,positions,kept,PhaseContext.apply(~S,~K,~V,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~unchanged(~S,~C,~R,~E),Phase.Owners{handlers,Phase.Idle{}},Ctx.Context{world,trace}))
31	def targeted(~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>,~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,~take:W.World<S,C,R,E> -> W.World<S,C,R,E> & M.Slot<S,K,V>,~put:W.World<S,C,R,E> -> M.Slot<S,K,V> -> W.World<S,C,R,E>,~publish:W.World<S,C,R,E> -> M.Transition<V> -> W.World<S,C,R,E>,~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>,entries:List<&1,B.Scheduled<S,K,V,Q,C,R,E,runner>>,pair:W.World<S,C,R,E> & M.Slot<S,K,V>,trace:Facts.State) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
32	  match pair:
33	    case (world,M.Missing{}):(Unavailable{entries,trace},Sys.Succeeded{put(world,M.Missing{}),Unit{}})
34	    case (world,M.Present{current,M.NoPending{},previous,_}):(Pending{entries,trace},Sys.Succeeded{put(world,M.Present{current,M.NoPending{},previous,False{}}),Unit{}})
35	    case (world,M.Present{+current,M.Queued{+to,+skip},previous,changed}):selected(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~requirement_same,~has,~frame,put(world,M.Present{current,M.Queued{to,skip},previous,changed}),B.partition(~S,~K,~V,~Q,~C,~R,~E,~runner,~same,entries,current,to),trace)
36	def apply(~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>,~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,~take:W.World<S,C,R,E> -> W.World<S,C,R,E> & M.Slot<S,K,V>,~put:W.World<S,C,R,E> -> M.Slot<S,K,V> -> W.World<S,C,R,E>,~publish:W.World<S,C,R,E> -> M.Transition<V> -> W.World<S,C,R,E>,~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>:
37	  match owners:
38	    case Pending{entries,trace}:targeted(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~requirement_same,~has,~frame,entries,take(frame(world)),trace)
39	    case owners:(owners,Sys.Succeeded{world,Unit{}})
40	def exit(~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>,~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,~take:W.World<S,C,R,E> -> W.World<S,C,R,E> & M.Slot<S,K,V>,~put:W.World<S,C,R,E> -> M.Slot<S,K,V> -> W.World<S,C,R,E>,~publish:W.World<S,C,R,E> -> M.Transition<V> -> W.World<S,C,R,E>,~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>:
41	  match owners:
42	    case Selected{positions,kept,active,_,trace}:phase_returned(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~requirement_same,~has,~frame,positions,kept,H.Exit{},PhaseContext.exit(~S,~K,~V,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~frame,active,Ctx.Context{world,trace}))
43	    case owners:(owners,Sys.Succeeded{world,Unit{}})
44	def transition(~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>,~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,~take:W.World<S,C,R,E> -> W.World<S,C,R,E> & M.Slot<S,K,V>,~put:W.World<S,C,R,E> -> M.Slot<S,K,V> -> W.World<S,C,R,E>,~publish:W.World<S,C,R,E> -> M.Transition<V> -> W.World<S,C,R,E>,~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>:
45	  match owners:
46	    case Selected{positions,kept,active,_,trace}:phase_returned(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~requirement_same,~has,~frame,positions,kept,H.Transition{},PhaseContext.transition(~S,~K,~V,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~frame,active,Ctx.Context{world,trace}))
47	    case owners:(owners,Sys.Succeeded{world,Unit{}})
48	def enter(~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>,~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,~take:W.World<S,C,R,E> -> W.World<S,C,R,E> & M.Slot<S,K,V>,~put:W.World<S,C,R,E> -> M.Slot<S,K,V> -> W.World<S,C,R,E>,~publish:W.World<S,C,R,E> -> M.Transition<V> -> W.World<S,C,R,E>,~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>:
49	  match owners:
50	    case Selected{positions,kept,active,_,trace}:phase_returned(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~requirement_same,~has,~frame,positions,kept,H.Enter{},PhaseContext.enter(~S,~K,~V,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~frame,active,Ctx.Context{world,trace}))
51	    case owners:(owners,Sys.Succeeded{world,Unit{}})
52	def recovered(~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>,~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,~take:W.World<S,C,R,E> -> W.World<S,C,R,E> & M.Slot<S,K,V>,~put:W.World<S,C,R,E> -> M.Slot<S,K,V> -> W.World<S,C,R,E>,~publish:W.World<S,C,R,E> -> M.Transition<V> -> W.World<S,C,R,E>,~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,positions:List<&2,B.Position<S,K,V,Q>>,kept:List<&1,H.Entry<S,C,R,E,V,runner>>,active:Phase.Owners<S,K,V,C,R,E,runner>,world:W.World<S,C,R,E>,status:B.Status<Q>) -> B.BundleResult<S,K,V,Q,C,R,E,runner>:
53	  match active:
54	    case Phase.Owners{handlers,_}:B.recovered(~S,~K,~V,~Q,~C,~R,~E,~runner,namespace,B.recover(~S,~K,~V,~Q,~C,~R,~E,~runner,positions,kept,handlers),world,status)
55	def finished(~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>,~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,~take:W.World<S,C,R,E> -> W.World<S,C,R,E> & M.Slot<S,K,V>,~put:W.World<S,C,R,E> -> M.Slot<S,K,V> -> W.World<S,C,R,E>,~publish:W.World<S,C,R,E> -> M.Transition<V> -> W.World<S,C,R,E>,~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>,error:Maybe<&2,String>) -> B.BundleResult<S,K,V,Q,C,R,E,runner> & Facts.State:
56	  match owners error:
57	    case Pending{entries,trace} None{}:(B.Returned{B.Bundle{namespace,entries},world,B.Completed{}},trace)
58	    case Pending{entries,trace} Some{_}:(B.Returned{B.Bundle{namespace,entries},world,B.ForeignBundle{}},trace)
59	    case Unavailable{entries,trace} _:(B.Returned{B.Bundle{namespace,entries},world,B.MachineUnavailable{}},trace)
60	    case Selected{positions,kept,active,_,trace} None{}:(recovered(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~requirement_same,~has,~frame,namespace,positions,kept,active,world,B.Completed{}),trace)
61	    case Selected{positions,kept,active,phase,trace} Some{error}:(recovered(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~requirement_same,~has,~frame,namespace,positions,kept,active,world,B.HandlerFailed{phase,error}),trace)
62	def marked(~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>,steps:List<&2,Sch.Step>,observations:List<&2,Sch.Observation>,result:B.BundleResult<S,K,V,Q,C,R,E,runner> & Facts.State) -> MarkerResult<S,K,V,Q,C,R,E,runner>:
63	  match result:
64	    case (result,trace):MarkerResult{result,steps,observations,trace}
65	def 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>,~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,~take:W.World<S,C,R,E> -> W.World<S,C,R,E> & M.Slot<S,K,V>,~put:W.World<S,C,R,E> -> M.Slot<S,K,V> -> W.World<S,C,R,E>,~publish:W.World<S,C,R,E> -> M.Transition<V> -> W.World<S,C,R,E>,~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>) -> MarkerResult<S,K,V,Q,C,R,E,runner>:
66	  match result:
67	    case Sch.Finished{Sch.Schedule{namespace,_,steps,owners},world,observations}:marked(~S,~K,~V,~Q,~C,~R,~E,~runner,steps,observations,finished(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~requirement_same,~has,~frame,namespace,owners,world,None{}))
68	    case Sch.Failed{Sch.Schedule{namespace,_,steps,owners},world,error,observations}:marked(~S,~K,~V,~Q,~C,~R,~E,~runner,steps,observations,finished(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~requirement_same,~has,~frame,namespace,owners,world,Some{error}))
69	    case Sch.Rejected{Sch.Schedule{namespace,_,steps,owners},world}:marked(~S,~K,~V,~Q,~C,~R,~E,~runner,steps,[],finished(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~requirement_same,~has,~frame,namespace,owners,world,Some{"schedule-rejected"}))
70	
71	def replaced_trace(~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>,owners:Owners<S,K,V,Q,C,R,E,runner>,trace:Facts.State) -> Owners<S,K,V,Q,C,R,E,runner>:
72	  match owners:
73	    case Pending{entries,_}:Pending{entries,trace}
74	    case Unavailable{entries,_}:Unavailable{entries,trace}
75	    case Selected{positions,kept,active,phase,_}:Selected{positions,kept,active,phase,trace}
76	def barrier_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>,owners:Owners<S,K,V,Q,C,R,E,runner>,result:W.World<S,C,R,E> & Facts.State) -> Owners<S,K,V,Q,C,R,E,runner> & W.World<S,C,R,E>:
77	  match result:
78	    case (world,trace):(replaced_trace(~S,~K,~V,~Q,~C,~R,~E,~runner,owners,Facts.barrier_finished(trace)),world)
79	def barrier(~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>,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>:
80	  match owners:
81	    case Pending{entries,trace}:barrier_returned(~S,~K,~V,~Q,~C,~R,~E,~runner,Pending{entries,Facts.Off{}},W.barrier_traced(~S,~C,~R,~E,world,Facts.barrier_entered(trace)))
82	    case Unavailable{entries,trace}:barrier_returned(~S,~K,~V,~Q,~C,~R,~E,~runner,Unavailable{entries,Facts.Off{}},W.barrier_traced(~S,~C,~R,~E,world,Facts.barrier_entered(trace)))
83	    case Selected{positions,kept,active,phase,trace}:barrier_returned(~S,~K,~V,~Q,~C,~R,~E,~runner,Selected{positions,kept,active,phase,Facts.Off{}},W.barrier_traced(~S,~C,~R,~E,world,Facts.barrier_entered(trace)))
84	def phase_started(~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>,owners:Owners<S,K,V,Q,C,R,E,runner>,id:U32) -> Owners<S,K,V,Q,C,R,E,runner>:
85	  match owners:
86	    case Pending{entries,trace}:Pending{entries,Facts.phase_boundary(trace,Ordinary.phase_name(id))}
87	    case Unavailable{entries,trace}:Unavailable{entries,Facts.phase_boundary(trace,Ordinary.phase_name(id))}
88	    case Selected{positions,kept,active,phase,trace}:Selected{positions,kept,active,phase,Facts.phase_boundary(trace,Ordinary.phase_name(id))}
89	def dispatch_shared(~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>,~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,~take:W.World<S,C,R,E> -> W.World<S,C,R,E> & M.Slot<S,K,V>,~put:W.World<S,C,R,E> -> M.Slot<S,K,V> -> W.World<S,C,R,E>,~publish:W.World<S,C,R,E> -> M.Transition<V> -> W.World<S,C,R,E>,~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>:
90	  Ordinary.dispatch(~S,~C,~R,~E,~Owners<S,K,V,Q,C,R,E,runner>,~String,~apply(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~requirement_same,~has,~frame),~exit(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~requirement_same,~has,~frame),~transition(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~requirement_same,~has,~frame),~enter(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~requirement_same,~has,~frame),phase_started(~S,~K,~V,~Q,~C,~R,~E,~runner,owners,id),world,id)
91	def dispatch(~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>,~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,~take:W.World<S,C,R,E> -> W.World<S,C,R,E> & M.Slot<S,K,V>,~put:W.World<S,C,R,E> -> M.Slot<S,K,V> -> W.World<S,C,R,E>,~publish:W.World<S,C,R,E> -> M.Transition<V> -> W.World<S,C,R,E>,~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>:
92	  dispatch_shared(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~requirement_same,~has,~frame,owners,world,id)
93	def installed(~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>,~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,~take:W.World<S,C,R,E> -> W.World<S,C,R,E> & M.Slot<S,K,V>,~put:W.World<S,C,R,E> -> M.Slot<S,K,V> -> W.World<S,C,R,E>,~publish:W.World<S,C,R,E> -> M.Transition<V> -> W.World<S,C,R,E>,~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>,world:W.World<S,C,R,E>,built:Sch.Build<S,C,R,E,Owners<S,K,V,Q,C,R,E,runner>>) -> MarkerResult<S,K,V,Q,C,R,E,runner>:
94	  match built:
95	    case Sch.Built{schedule}:returned(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~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,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~requirement_same,~has,~frame),~Ordinary.condition(~S,~C,~R,~E),~barrier(~S,~K,~V,~Q,~C,~R,~E,~runner),schedule,world))
96	    case Sch.Invalid{owners}:marked(~S,~K,~V,~Q,~C,~R,~E,~runner,[],[],finished(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~requirement_same,~has,~frame,0,owners,world,Some{"invalid"}))
97	def checked(~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>,~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,~take:W.World<S,C,R,E> -> W.World<S,C,R,E> & M.Slot<S,K,V>,~put:W.World<S,C,R,E> -> M.Slot<S,K,V> -> W.World<S,C,R,E>,~publish:W.World<S,C,R,E> -> M.Transition<V> -> W.World<S,C,R,E>,~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,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) -> MarkerResult<S,K,V,Q,C,R,E,runner>:
98	  match pair:
99	    case (world,[]):installed(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~requirement_same,~has,~frame,declaration,world,Ordinary.install(~S,~C,~R,~E,~Owners<S,K,V,Q,C,R,E,runner>,~String,declaration,namespace,Pending{entries,trace}))
100	    case (world,missing):MarkerResult{B.Returned{B.Bundle{namespace,entries},world,B.MissingRequirements{missing}},[],[],trace}
101	def gathered(~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>,~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,~take:W.World<S,C,R,E> -> W.World<S,C,R,E> & M.Slot<S,K,V>,~put:W.World<S,C,R,E> -> M.Slot<S,K,V> -> W.World<S,C,R,E>,~publish:W.World<S,C,R,E> -> M.Transition<V> -> W.World<S,C,R,E>,~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,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) -> MarkerResult<S,K,V,Q,C,R,E,runner>:
102	  (entries,needs)=pair
103	  checked(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~requirement_same,~has,~frame,declaration,namespace,entries,B.missing(~S,~C,~R,~E,~Q,~has,B.collect(~Q,~requirement_same,needs,[]),world),trace)
104	def allowed(~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>,~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,~take:W.World<S,C,R,E> -> W.World<S,C,R,E> & M.Slot<S,K,V>,~put:W.World<S,C,R,E> -> M.Slot<S,K,V> -> W.World<S,C,R,E>,~publish:W.World<S,C,R,E> -> M.Transition<V> -> W.World<S,C,R,E>,~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,entries:List<&1,B.Scheduled<S,K,V,Q,C,R,E,runner>>,world:W.World<S,C,R,E>,trace:Facts.State) -> MarkerResult<S,K,V,Q,C,R,E,runner>:
105	  match yes:
106	    case False{}:MarkerResult{B.Returned{B.Bundle{namespace,entries},world,B.ForeignBundle{}},[],[],trace}
107	    case True{}:gathered(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~requirement_same,~has,~frame,declaration,namespace,world,B.requirements(~S,~K,~V,~Q,~C,~R,~E,~runner,entries),trace)
108	def named(~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>,~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,~take:W.World<S,C,R,E> -> W.World<S,C,R,E> & M.Slot<S,K,V>,~put:W.World<S,C,R,E> -> M.Slot<S,K,V> -> W.World<S,C,R,E>,~publish:W.World<S,C,R,E> -> M.Transition<V> -> W.World<S,C,R,E>,~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,entries:List<&1,B.Scheduled<S,K,V,Q,C,R,E,runner>>,pair:W.World<S,C,R,E> & U32,trace:Facts.State) -> MarkerResult<S,K,V,Q,C,R,E,runner>:
109	  (world,actual)=pair
110	  allowed(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~requirement_same,~has,~frame,declaration,U32.is_eq(namespace,actual),namespace,entries,world,trace)
111	def run(~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>,~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,~take:W.World<S,C,R,E> -> W.World<S,C,R,E> & M.Slot<S,K,V>,~put:W.World<S,C,R,E> -> M.Slot<S,K,V> -> W.World<S,C,R,E>,~publish:W.World<S,C,R,E> -> M.Transition<V> -> W.World<S,C,R,E>,~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>,world:W.World<S,C,R,E>,trace:Facts.State) -> MarkerResult<S,K,V,Q,C,R,E,runner>:
112	  match bundle:
113	    case B.Bundle{namespace,entries}:named(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take,~put,~publish,~same,~requirement_same,~has,~frame,declaration,namespace,entries,W.namespace(~S,~C,~R,~E,world),trace)