1	import Base
2	import ./change_tick.bend as Tick
3	import ./reader_parameter.bend as RP
4	import ./world.bend as W
5	import ./event_runtime.bend as Ev
6	import ./event_stream.bend as Stream
7	import ./event_family_routing.bend as Route
8	import ./event_family_runtime.bend as Family
9	import ./event_notice_runtime.bend as Mixed
10	import ./relation_commands.bend as Notice
11	import ./ordinary_event_declaration.bend as Event
12	import ./relation_failure_reader.bend as KDecl
13	import ./relation_failure_runtime.bend as K
14	import ./relation_failure_disposal.bend as KDispose
15	import ./internal/relation_failures/domains.bend as KD
16	import ./internal/relation_failures/readings.bend as KRead
17	import ./ordinary_removal_provision.bend as Provision
18	import ./ordinary_declaration.bend as Identity
19	import ./removals.bend as Rm
20	
21	# These parameters read one shared route context. Per-system owners contain
22	# reader identity and cursor metadata; all retained histories stay centralized.
23	type EventView<S:Data,E:Data> is Data:
24	  EventView{reading:Ev.Reading<E>}
25	type RemovalView<S:Data,P:Type> is Data:
26	  RemovalView{records:List<&2,Rm.Record<S,Identity.Declaration<S,P>>>}
27	type RelationView<S:Data,P:Data> is Data:
28	  RelationView{readings:List<&2,KRead.KeyReading<S,Notice.Notice<S,P>>>}
29	type RelationDelta is Data:
30	  RelationDelta{id:Maybe<&2,U32>,readThrough:Nat}
31	
32	type EventOwner<S:Data,C:Type,R:Type,P:Data,E:Data,F:Type,H:Type,
33	  -take:F -> F & Stream.Stream<S,E>,
34	  -put:F -> Stream.Stream<S,E> -> F> is Type:
35	  EventOwner{facts:RP.RegistrationFacts,reader:Route.Reader<S,E,F,take,put>}
36	type RemovalOwner<S:Data,P:Type,E:Data,
37	  -select:E -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,P>>>> is Type:
38	  RemovalOwner{facts:RP.RegistrationFacts,reader:Rm.Reader<S,E,Identity.Declaration<S,P>,select>}
39	type RelationOwner<S:Data,P:Data> is Type:
40	  RelationOwner{facts:RP.RegistrationFacts,id:Maybe<&2,U32>,keys:List<&2,KD.DescriptorKey<S>>}
41	
42	def access_member(+wanted:String,access:List<&2,String>) -> Bool:
43	  match access:
44	    case []:False{}
45	    case name <> rest:Bool.or(String.eq(wanted,name),access_member(wanted,rest))
46	def access_subset(wanted:List<&2,String>,+access:List<&2,String>) -> Bool:
47	  match wanted:
48	    case []:True{}
49	    case name <> rest:Bool.and(access_member(name,access),access_subset(rest,access))
50	
51	# Keep the affine World returned by the normal registration check.
52	def registered_context_checked(~S:Data,~C:Type,~R:Type,~E:Data,
53	  namespace:U32,currentNamespace:U32,checked:W.World<S,C,R,E> & Bool) -> W.World<S,C,R,E> & Bool:
54	  match checked:
55	    case (world,matched):(world,Bool.and(U32.is_eq(namespace,currentNamespace),matched))
56	def registered_context_named(~S:Data,~C:Type,~R:Type,~E:Data,
57	  id:U32,name:String,access:List<&2,String>,factsNamespace:U32,
58	  named:W.World<S,C,R,E> & U32) -> W.World<S,C,R,E> & Bool:
59	  match named:
60	    case (world,currentNamespace):
61	      registered_context_checked(~S,~C,~R,~E,factsNamespace,currentNamespace,
62	        W.registration_matches(~S,~C,~R,~E,world,id,name,access))
63	def registered_context(~S:Data,~C:Type,~R:Type,~E:Data,
64	  world:W.World<S,C,R,E>,facts:RP.RegistrationFacts) -> W.World<S,C,R,E> & Bool:
65	  match facts:
66	    case RP.RegistrationFacts{namespace,id,name,access}:
67	      registered_context_named(~S,~C,~R,~E,id,name,access,namespace,
68	        W.namespace(~S,~C,~R,~E,world))
69	
70	# Event stream readers use the existing central Leaf.Stream identity allocator.
71	def event_access(~S:Data,~E:Data,declaration:Event.Declaration<S,E>) -> List<&2,String>:
72	  [Event.access(~S,~E,declaration)]
73	def event_readable(~S:Data,~E:Data,declaration:Event.Declaration<S,E>) -> Bool:
74	  match declaration:
75	    case Event.Declaration{_,Event.Read{}}:True{}
76	    case Event.Declaration{_,Event.Write{}}:False{}
77	def event_domain_matches(~S:Data,~E:Data,
78	  declaration:Event.Declaration<S,E>,
79	  domain:Event.Domain<S,E>) -> Bool:
80	  match declaration domain:
81	    case Event.Declaration{Event.Domain{expected},Event.Read{}} Event.Domain{actual}:String.eq(expected,actual)
82	    case _ _:False{}
83	
84	def event_selected_domain(~S:Data,~P:Data,~E:Data,~F:Type,~H:Type,
85	  ~take:F -> F & Stream.Stream<S,E>,
86	  ~put:F -> Stream.Stream<S,E> -> F,
87	  declaration:Event.Declaration<S,E>,
88	  selected:Mixed.State<S,P,F,H> & Stream.Stream<S,E>) -> Mixed.State<S,P,F,H> & Bool:
89	  match selected:
90	    case (state,+stream):
91	      (Mixed.put(~S,~E,~P,~F,~H,~put,state,stream),
92	       event_domain_matches(~S,~E,declaration,Stream.domain(~S,~E,stream)))
93	
94	def event_validate_values(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
95	  ~take:F -> F & Stream.Stream<S,E>,
96	  ~put:F -> Stream.Stream<S,E> -> F,
97	  ~declaration:Event.Declaration<S,E>,tick:Nat,facts:RP.RegistrationFacts,
98	  reader:Route.Reader<S,E,F,take,put>,
99	  world:W.World<S,C,R,Notice.Notice<S,P>>,registered:Bool,state:Mixed.State<S,P,F,H>,domainMatches:Bool) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (EventOwner<S,C,R,P,E,F,H,take,put> & Bool):
100	  match facts:
101	    case RP.RegistrationFacts{+expectedNamespace,+registryIdExpected,_,+access}:
102	      match reader:
103	        case Route.Reader{+namespace,+readerId,+registryId}:
104	          +valid=Bool.and(event_readable(~S,~E,declaration),
105	            Bool.and(registered,Bool.and(access_subset(event_access(~S,~E,declaration),access),
106	              Bool.and(U32.is_eq(namespace,expectedNamespace),
107	                Bool.and(U32.is_gt(readerId,0),
108	                  Bool.and(U32.is_eq(registryId,registryIdExpected),domainMatches))))))
109	          (Route.Runtime{world,state,tick},(EventOwner{facts,reader},valid))
110	
111	def event_validate_domain(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
112	  ~take:F -> F & Stream.Stream<S,E>,
113	  ~put:F -> Stream.Stream<S,E> -> F,
114	  ~declaration:Event.Declaration<S,E>,tick:Nat,facts:RP.RegistrationFacts,
115	  reader:Route.Reader<S,E,F,take,put>,
116	  registered:W.World<S,C,R,Notice.Notice<S,P>> & Bool,
117	  selected:Mixed.State<S,P,F,H> & Bool) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (EventOwner<S,C,R,P,E,F,H,take,put> & Bool):
118	  match registered:
119	    case (world,isRegistered):
120	      match selected:
121	        case (state,domainMatches):event_validate_values(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration,tick,facts,reader,world,isRegistered,state,domainMatches)
122	
123	def event_validate_registered(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
124	  ~take:F -> F & Stream.Stream<S,E>,
125	  ~put:F -> Stream.Stream<S,E> -> F,
126	  ~declaration:Event.Declaration<S,E>,tick:Nat,facts:RP.RegistrationFacts,
127	  reader:Route.Reader<S,E,F,take,put>,
128	  registered:W.World<S,C,R,Notice.Notice<S,P>> & Bool,
129	  selected:Mixed.State<S,P,F,H> & Bool) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (EventOwner<S,C,R,P,E,F,H,take,put> & Bool):
130	  event_validate_domain(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration,tick,facts,reader,registered,selected)
131	
132	def event_validate_join(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
133	  ~take:F -> F & Stream.Stream<S,E>,
134	  ~put:F -> Stream.Stream<S,E> -> F,
135	  ~declaration:Event.Declaration<S,E>,
136	  tick:Nat,facts:RP.RegistrationFacts,
137	  reader:Route.Reader<S,E,F,take,put>,
138	  registeredContext:W.World<S,C,R,Notice.Notice<S,P>> & Bool,
139	  selectedDomain:Mixed.State<S,P,F,H> & Bool) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (EventOwner<S,C,R,P,E,F,H,take,put> & Bool):
140	  event_validate_registered(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration,tick,facts,reader,registeredContext,selectedDomain)
141	
142	def validate_event(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
143	  ~take:F -> F & Stream.Stream<S,E>,
144	  ~put:F -> Stream.Stream<S,E> -> F,
145	  ~declaration:Event.Declaration<S,E>,
146	  context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
147	  owner:EventOwner<S,C,R,P,E,F,H,take,put>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (EventOwner<S,C,R,P,E,F,H,take,put> & Bool):
148	  match context owner:
149	    case Route.Runtime{world,state,tick} EventOwner{+facts,reader}:
150	      event_validate_join(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration,tick,facts,reader,
151	        registered_context(~S,~C,~R,~Notice.Notice<S,P>,world,facts),
152	        event_selected_domain(~S,~P,~E,~F,~H,~take,~put,declaration,
153	          Mixed.take(~S,~E,~P,~F,~H,~take,state)))
154	
155	def event_reading_loaded(~S:Data,~P:Data,~E:Data,~F:Type,~H:Type,selected:Mixed.State<S,P,F,H>,
156	  viewed:Stream.Stream<S,E> & Ev.Reading<E>) -> Mixed.State<S,P,F,H> & (Stream.Stream<S,E> & Ev.Reading<E>):
157	  match viewed:
158	    case (stream,reading):(selected,(stream,reading))
159	
160	def event_read_selected_from(~S:Data,~P:Data,~E:Data,~F:Type,~H:Type,
161	  ~take:F -> F & Stream.Stream<S,E>,
162	  id:U32,tick:Nat,
163	  selected:Mixed.State<S,P,F,H> & Stream.Stream<S,E>) -> Mixed.State<S,P,F,H> & (Stream.Stream<S,E> & Ev.Reading<E>):
164	  match selected:
165	    case (held,stream):event_reading_loaded(~S,~P,~E,~F,~H,held,Stream.reading(~S,~E,stream,id,tick))
166	
167	def event_read_selected(~S:Data,~P:Data,~E:Data,~F:Type,~H:Type,
168	  ~take:F -> F & Stream.Stream<S,E>,
169	  state:Mixed.State<S,P,F,H>,id:U32,tick:Nat) -> Mixed.State<S,P,F,H> & (Stream.Stream<S,E> & Ev.Reading<E>):
170	  event_read_selected_from(~S,~P,~E,~F,~H,~take,id,tick,Mixed.take(~S,~E,~P,~F,~H,~take,state))
171	
172	def event_prepared(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
173	  ~take:F -> F & Stream.Stream<S,E>,
174	  ~put:F -> Stream.Stream<S,E> -> F,
175	  world:W.World<S,C,R,Notice.Notice<S,P>>,+tick:Nat,
176	  owner:EventOwner<S,C,R,P,E,F,H,take,put>,
177	  selected:Mixed.State<S,P,F,H> & (Stream.Stream<S,E> & Ev.Reading<E>)) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (EventOwner<S,C,R,P,E,F,H,take,put> & (EventView<S,E> & Nat)):
178	  # A first attempted read owns retention even if its callback fails. Keep
179	  # cursor zero until commit; completed(False) only activates the position.
180	  match owner:
181	    case EventOwner{facts,Route.Reader{namespace,+id,registryId}}:
182	      match selected:
183	        case (state,(stream,reading)):
184	          (Route.Runtime{world,Mixed.put(~S,~E,~P,~F,~H,~put,state,
185	            Stream.completed(~S,~E,stream,id,Nat.sub(tick,1n),False{})),tick},
186	           (EventOwner{facts,Route.Reader{namespace,id,registryId}},(EventView{reading},Nat.sub(tick,1n))))
187	
188	def prepare_event(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
189	  ~take:F -> F & Stream.Stream<S,E>,
190	  ~put:F -> Stream.Stream<S,E> -> F,
191	  ~declaration:Event.Declaration<S,E>,
192	  context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,+cursor:Maybe<&2,Tick.Tick>,
193	  owner:EventOwner<S,C,R,P,E,F,H,take,put>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (EventOwner<S,C,R,P,E,F,H,take,put> & (EventView<S,E> & Nat)):
194	  match context owner:
195	    case Route.Runtime{world,state,+tick} EventOwner{facts,reader}:
196	      match reader:
197	        case Route.Reader{namespace,+id,registryId}:
198	          event_prepared(~S,~C,~R,~P,~E,~F,~H,~take,~put,world,tick,EventOwner{facts,Route.Reader{namespace,id,registryId}},
199	            event_read_selected(~S,~P,~E,~F,~H,~take,state,id,tick))
200	
201	def event_advanced_selected(~S:Data,~P:Data,~E:Data,~F:Type,~H:Type,
202	  ~put:F -> Stream.Stream<S,E> -> F,id:U32,readThrough:Nat,
203	  selected:Mixed.State<S,P,F,H> & Stream.Stream<S,E>) -> Mixed.State<S,P,F,H>:
204	  match selected:
205	    case (state,stream):Mixed.put(~S,~E,~P,~F,~H,~put,state,Stream.advance(~S,~E,stream,id,readThrough))
206	
207	def event_advanced(~S:Data,~P:Data,~E:Data,~F:Type,~H:Type,
208	  ~take:F -> F & Stream.Stream<S,E>,
209	  ~put:F -> Stream.Stream<S,E> -> F,
210	  state:Mixed.State<S,P,F,H>,id:U32,readThrough:Nat) -> Mixed.State<S,P,F,H>:
211	  event_advanced_selected(~S,~P,~E,~F,~H,~put,id,readThrough,Mixed.take(~S,~E,~P,~F,~H,~take,state))
212	
213	def commit_event(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
214	  ~take:F -> F & Stream.Stream<S,E>,
215	  ~put:F -> Stream.Stream<S,E> -> F,
216	  context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
217	  owner:EventOwner<S,C,R,P,E,F,H,take,put>,readThrough:Nat,+cursor:Tick.Tick) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & EventOwner<S,C,R,P,E,F,H,take,put>:
218	  match context owner:
219	    case Route.Runtime{world,state,tick} EventOwner{facts,reader}:
220	      match reader:
221	        case Route.Reader{namespace,+id,registryId}:
222	          (Route.Runtime{world,event_advanced(~S,~P,~E,~F,~H,~take,~put,state,id,readThrough),tick},
223	           EventOwner{facts,Route.Reader{namespace,id,registryId}})
224	
225	def event_release_stream(~S:Data,~P:Data,~E:Data,~F:Type,~H:Type,
226	  ~put:F -> Stream.Stream<S,E> -> F,id:U32,tick:Nat,
227	  selected:Mixed.State<S,P,F,H> & Stream.Stream<S,E>) -> Mixed.State<S,P,F,H>:
228	  match selected:
229	    case (state,stream):
230	      match stream:
231	        case Stream.Stream{domain,batches,positions,nextReader,frameStart,boundary,capacity,dropped}:
232	          Mixed.put(~S,~E,~P,~F,~H,~put,state,
233	            Stream.Stream{domain,batches,Ev.update(positions,id,tick,True{}),nextReader,frameStart,boundary,capacity,dropped})
234	
235	def event_release_ready(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
236	  ~take:F -> F & Stream.Stream<S,E>,~put:F -> Stream.Stream<S,E> -> F,readerId:U32,
237	  context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>:
238	  match context:
239	    case Route.Runtime{world,state,+tick}:
240	      Route.Runtime{world,event_release_stream(~S,~P,~E,~F,~H,~put,readerId,tick,
241	        Mixed.take(~S,~E,~P,~F,~H,~take,state)),tick}
242	
243	def event_release_decided(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
244	  ~take:F -> F & Stream.Stream<S,E>,~put:F -> Stream.Stream<S,E> -> F,
245	  allowed:Bool,context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,readerId:U32) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>:
246	  match allowed:
247	    case False{}:context
248	    case True{}:event_release_ready(~S,~C,~R,~P,~E,~F,~H,~take,~put,readerId,context)
249	
250	def event_release_validated(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
251	  ~take:F -> F & Stream.Stream<S,E>,~put:F -> Stream.Stream<S,E> -> F,
252	  context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,+readerId:U32) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>:
253	  event_release_decided(~S,~C,~R,~P,~E,~F,~H,~take,~put,U32.is_gt(readerId,0),context,readerId)
254	
255	def release_event(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
256	  ~take:F -> F & Stream.Stream<S,E>,~put:F -> Stream.Stream<S,E> -> F,
257	  context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
258	  owner:EventOwner<S,C,R,P,E,F,H,take,put>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>:
259	  match context owner:
260	    case Route.Runtime{world,state,tick} EventOwner{_,reader}:
261	      match reader:
262	        case Route.Reader{namespace,+readerId,registryId}:
263	          event_release_validated(~S,~C,~R,~P,~E,~F,~H,~take,~put,
264	            Route.Runtime{world,state,tick},readerId)
265	
266	def event_param(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
267	  ~take:F -> F & Stream.Stream<S,E>,
268	  ~put:F -> Stream.Stream<S,E> -> F,
269	  ~declaration:Event.Declaration<S,E>) -> RP.Param<Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,EventOwner<S,C,R,P,E,F,H,take,put>,EventView<S,E>,Nat,
270	  validate_event(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration),prepare_event(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration),commit_event(~S,~C,~R,~P,~E,~F,~H,~take,~put),release_event(~S,~C,~R,~P,~E,~F,~H,~take,~put)>:
271	  RP.make(~Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,~EventOwner<S,C,R,P,E,F,H,take,put>,~EventView<S,E>,~Nat,
272	    ~validate_event(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration),
273	    ~prepare_event(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration),
274	    ~commit_event(~S,~C,~R,~P,~E,~F,~H,~take,~put),
275	    ~release_event(~S,~C,~R,~P,~E,~F,~H,~take,~put),
276	    event_access(~S,~E,declaration))
277	
278	def event_registered_leaf(~S:Data,~P:Data,~E:Data,~F:Type,~H:Type,
279	  ~put:F -> Stream.Stream<S,E> -> F,
280	  selected:Mixed.State<S,P,F,H>,
281	  registered:Stream.Stream<S,E> & U32) -> Mixed.State<S,P,F,H> & U32:
282	  match registered:
283	    case (stream,id):(Mixed.put(~S,~E,~P,~F,~H,~put,selected,stream),id)
284	
285	def event_registered_selected(~S:Data,~P:Data,~E:Data,~F:Type,~H:Type,
286	  ~put:F -> Stream.Stream<S,E> -> F,tick:Nat,
287	  selected:Mixed.State<S,P,F,H> & Stream.Stream<S,E>) -> Mixed.State<S,P,F,H> & U32:
288	  match selected:
289	    case (state,stream):event_registered_leaf(~S,~P,~E,~F,~H,~put,state,Stream.registered(~S,~E,stream,tick))
290	
291	def event_registered(~S:Data,~P:Data,~E:Data,~F:Type,~H:Type,
292	  ~take:F -> F & Stream.Stream<S,E>,
293	  ~put:F -> Stream.Stream<S,E> -> F,
294	  state:Mixed.State<S,P,F,H>,tick:Nat) -> Mixed.State<S,P,F,H> & U32:
295	  event_registered_selected(~S,~P,~E,~F,~H,~put,tick,Mixed.take(~S,~E,~P,~F,~H,~take,state))
296	
297	def event_initialized_registered(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
298	  ~take:F -> F & Stream.Stream<S,E>,
299	  ~put:F -> Stream.Stream<S,E> -> F,
300	  ~declaration:Event.Declaration<S,E>,
301	  world:W.World<S,C,R,Notice.Notice<S,P>>,+tick:Nat,
302	  facts:RP.RegistrationFacts,
303	  registered:Mixed.State<S,P,F,H> & U32) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (EventOwner<S,C,R,P,E,F,H,take,put> & RP.Param<Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,EventOwner<S,C,R,P,E,F,H,take,put>,EventView<S,E>,Nat,
304	  validate_event(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration),prepare_event(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration),commit_event(~S,~C,~R,~P,~E,~F,~H,~take,~put),release_event(~S,~C,~R,~P,~E,~F,~H,~take,~put)>):
305	  match facts:
306	    case RP.RegistrationFacts{+namespace,+registryId,_,_}:
307	      match registered:
308	        case (state,id):
309	          (Route.Runtime{world,state,tick},
310	           (EventOwner{facts,Route.Reader{namespace,id,registryId}},event_param(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration)))
311	
312	def initialize_event_selected(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
313	  ~take:F -> F & Stream.Stream<S,E>,
314	  ~put:F -> Stream.Stream<S,E> -> F,
315	  ~declaration:Event.Declaration<S,E>,
316	  readable:Bool,
317	  context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
318	  facts:RP.RegistrationFacts) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (EventOwner<S,C,R,P,E,F,H,take,put> & RP.Param<Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,EventOwner<S,C,R,P,E,F,H,take,put>,EventView<S,E>,Nat,
319	  validate_event(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration),prepare_event(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration),commit_event(~S,~C,~R,~P,~E,~F,~H,~take,~put),release_event(~S,~C,~R,~P,~E,~F,~H,~take,~put)>):
320	  match readable context facts:
321	    case False{} Route.Runtime{world,state,tick} RP.RegistrationFacts{+namespace,+registryId,_,_}:
322	      (Route.Runtime{world,state,tick},
323	       (EventOwner{facts,Route.Reader{namespace,0,registryId}},event_param(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration)))
324	    case True{} Route.Runtime{world,state,+tick} RP.RegistrationFacts{+namespace,+registryId,_,_}:
325	      event_initialized_registered(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration,
326	        world,tick,facts,
327	        event_registered(~S,~P,~E,~F,~H,~take,~put,state,tick))
328	
329	def initialize_event(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
330	  ~take:F -> F & Stream.Stream<S,E>,
331	  ~put:F -> Stream.Stream<S,E> -> F,
332	  ~declaration:Event.Declaration<S,E>,
333	  context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
334	  facts:RP.RegistrationFacts) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (EventOwner<S,C,R,P,E,F,H,take,put> & RP.Param<Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,EventOwner<S,C,R,P,E,F,H,take,put>,EventView<S,E>,Nat,
335	  validate_event(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration),prepare_event(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration),commit_event(~S,~C,~R,~P,~E,~F,~H,~take,~put),release_event(~S,~C,~R,~P,~E,~F,~H,~take,~put)>):
336	  initialize_event_selected(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration,
337	    event_readable(~S,~E,declaration),context,facts)
338	
339	# Removal declarations retain their nominal component identity and selector.
340	def removal_name(~S:Data,~Payload:Type,~E:Data,
341	  ~inject:Identity.Declaration<S,Payload> -> W.Handle<S> -> E,
342	  ~select:E -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
343	  selection:Provision.Selection<S,Payload,E,inject,select>) -> String:
344	  match selection:
345	    case Provision.Selection{identity}:Identity.key(~S,~Payload,identity)
346	
347	def removal_identity(~S:Data,~Payload:Type,~E:Data,
348	  ~inject:Identity.Declaration<S,Payload> -> W.Handle<S> -> E,
349	  ~select:E -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
350	  selection:Provision.Selection<S,Payload,E,inject,select>) -> Identity.Declaration<S,Payload>:
351	  match selection:
352	    case Provision.Selection{identity}:identity
353	def removal_access(~S:Data,~Payload:Type,~E:Data,
354	  ~inject:Identity.Declaration<S,Payload> -> W.Handle<S> -> E,
355	  ~select:E -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
356	  selection:Provision.Selection<S,Payload,E,inject,select>) -> List<&2,String>:
357	  ["removal",removal_name(~S,~Payload,~E,~inject,~select,selection)]
358	
359	def removal_validate_checked(~S:Data,~C:Type,~R:Type,~P:Data,~Payload:Type,~F:Type,~H:Type,
360	  ~inject:Identity.Declaration<S,Payload> -> W.Handle<S> -> Notice.Notice<S,P>,
361	  ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
362	  ~selection:Provision.Selection<S,Payload,Notice.Notice<S,P>,inject,select>,
363	  state:Mixed.State<S,P,F,H>,tick:Nat,facts:RP.RegistrationFacts,
364	  reader:Rm.Reader<S,Notice.Notice<S,P>,Identity.Declaration<S,Payload>,select>,
365	  registered:W.World<S,C,R,Notice.Notice<S,P>> & Bool) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (RemovalOwner<S,Payload,Notice.Notice<S,P>,select> & Bool):
366	  match facts:
367	    case RP.RegistrationFacts{+expectedNamespace,+expectedId,_,+access}:
368	      match reader:
369	        case Rm.Reader{+namespace,+id,+name,cursor}:
370	          match registered:
371	            case (world,isRegistered):
372	              +expected=removal_access(~S,~Payload,~Notice.Notice<S,P>,~inject,~select,selection)
373	              +valid=Bool.and(isRegistered,Bool.and(access_subset(expected,access),
374	                Bool.and(U32.is_eq(namespace,expectedNamespace),
375	                  Bool.and(U32.is_eq(id,expectedId),String.eq(name,removal_name(~S,~Payload,~Notice.Notice<S,P>,~inject,~select,selection))))))
376	              (Route.Runtime{world,state,tick},(RemovalOwner{facts,Rm.Reader{namespace,id,name,cursor}},valid))
377	
378	def validate_removal(~S:Data,~C:Type,~R:Type,~P:Data,~Payload:Type,~F:Type,~H:Type,
379	  ~inject:Identity.Declaration<S,Payload> -> W.Handle<S> -> Notice.Notice<S,P>,
380	  ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
381	  ~selection:Provision.Selection<S,Payload,Notice.Notice<S,P>,inject,select>,
382	  context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
383	  owner:RemovalOwner<S,Payload,Notice.Notice<S,P>,select>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (RemovalOwner<S,Payload,Notice.Notice<S,P>,select> & Bool):
384	  match context owner:
385	    case Route.Runtime{world,state,tick} RemovalOwner{+facts,reader}:
386	      removal_validate_checked(~S,~C,~R,~P,~Payload,~F,~H,~inject,~select,~selection,
387	        state,tick,facts,reader,registered_context(~S,~C,~R,~Notice.Notice<S,P>,world,facts))
388	
389	def removal_prepared(~S:Data,~C:Type,~R:Type,~P:Data,~Payload:Type,~F:Type,~H:Type,
390	  ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
391	  state:Mixed.State<S,P,F,H>,tick:Nat,owner:RemovalOwner<S,Payload,Notice.Notice<S,P>,select>,
392	  observed:W.World<S,C,R,Notice.Notice<S,P>> & List<&2,Notice.Notice<S,P>>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (RemovalOwner<S,Payload,Notice.Notice<S,P>,select> & (RemovalView<S,Payload> & Nat)):
393	  match owner:
394	    case RemovalOwner{facts,reader}:
395	      match reader:
396	        case Rm.Reader{namespace,id,name,+cursor}:
397	          match observed:
398	            case (world,+values):
399	              +records=Rm.since(~S,~Notice.Notice<S,P>,~Identity.Declaration<S,Payload>,~select,values,cursor)
400	              (Route.Runtime{world,state,tick},
401	                (RemovalOwner{facts,Rm.Reader{namespace,id,name,cursor}},
402	                 (RemovalView{records},Rm.count(~Notice.Notice<S,P>,values))))
403	
404	def prepare_removal(~S:Data,~C:Type,~R:Type,~P:Data,~Payload:Type,~F:Type,~H:Type,
405	  ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
406	  context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,+cursor:Maybe<&2,Tick.Tick>,
407	  owner:RemovalOwner<S,Payload,Notice.Notice<S,P>,select>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (RemovalOwner<S,Payload,Notice.Notice<S,P>,select> & (RemovalView<S,Payload> & Nat)):
408	  match context:
409	    case Route.Runtime{world,state,tick}:
410	      removal_prepared(~S,~C,~R,~P,~Payload,~F,~H,~select,state,tick,owner,
411	        W.events_view(~S,~C,~R,~Notice.Notice<S,P>,world))
412	
413	def commit_removal(~S:Data,~C:Type,~R:Type,~P:Data,~Payload:Type,~F:Type,~H:Type,
414	  ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
415	  context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
416	  owner:RemovalOwner<S,Payload,Notice.Notice<S,P>,select>,observedCount:Nat,+cursor:Tick.Tick) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & RemovalOwner<S,Payload,Notice.Notice<S,P>,select>:
417	  match context owner:
418	    case context RemovalOwner{facts,reader}:
419	      match reader:
420	        case Rm.Reader{namespace,id,name,_}:
421	          (context,RemovalOwner{facts,Rm.Reader{namespace,id,name,observedCount}})
422	
423	def removal_access_member(access:List<&2,String>) -> Bool:
424	  match access:
425	    case []:False{}
426	    case first <> rest:Bool.or(String.eq("removal",first),removal_access_member(rest))
427	def removal_registration_remains(entries:List<&2,W.RegistrationMeta>) -> Bool:
428	  match entries:
429	    case []:False{}
430	    case W.RegistrationMeta{_,_,access} <> rest:
431	      Bool.or(removal_access_member(access),removal_registration_remains(rest))
432	def removal_event_selected(~S:Data,~P:Data,~Payload:Type,
433	  selected:Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
434	  +event:Notice.Notice<S,P>,rest:List<&2,Notice.Notice<S,P>>) -> List<&2,Notice.Notice<S,P>>:
435	  match selected:
436	    case None{}:event <> rest
437	    case Some{_}:rest
438	def removal_event_kept(~S:Data,~P:Data,~Payload:Type,
439	  ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
440	  +event:Notice.Notice<S,P>,rest:List<&2,Notice.Notice<S,P>>) -> List<&2,Notice.Notice<S,P>>:
441	  removal_event_selected(~S,~P,~Payload,select(event),event,rest)
442	def removal_events_kept(~S:Data,~P:Data,~Payload:Type,
443	  ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
444	  events:List<&2,Notice.Notice<S,P>>) -> List<&2,Notice.Notice<S,P>>:
445	  match events:
446	    case []:[]
447	    case event <> rest:removal_event_kept(~S,~P,~Payload,~select,event,removal_events_kept(~S,~P,~Payload,~select,rest))
448	def removal_release_world_checked(~S:Data,~C:Type,~R:Type,~P:Data,~Payload:Type,
449	  ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
450	  retained:Bool,world:W.World<S,C,R,Notice.Notice<S,P>>) -> W.World<S,C,R,Notice.Notice<S,P>>:
451	  match retained world:
452	    case True{} world:world
453	    case False{} W.World{namespace,allocator,store,resource,events,pending,registrations,nextSystemId,clock}:
454	      W.World{namespace,allocator,store,resource,
455	        removal_events_kept(~S,~P,~Payload,~select,events),pending,registrations,nextSystemId,clock}
456	def removal_world_retained(~S:Data,~C:Type,~R:Type,~P:Data,
457	  world:W.World<S,C,R,Notice.Notice<S,P>>) -> W.World<S,C,R,Notice.Notice<S,P>> & Bool:
458	  match world:
459	    case W.World{+namespace,allocator,store,resource,+events,pending,+registrations,+nextSystemId,+clock}:
460	      (W.World{namespace,allocator,store,resource,events,pending,registrations,nextSystemId,clock},
461	        removal_registration_remains(registrations))
462	def removal_release_world(~S:Data,~C:Type,~R:Type,~P:Data,~Payload:Type,
463	  ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
464	  world:W.World<S,C,R,Notice.Notice<S,P>>) -> W.World<S,C,R,Notice.Notice<S,P>>:
465	  match world:
466	    case W.World{namespace,allocator,store,resource,events,pending,+registrations,nextSystemId,clock}:
467	      removal_release_world_checked(~S,~C,~R,~P,~Payload,~select,
468	        removal_registration_remains(registrations),
469	        W.World{namespace,allocator,store,resource,events,pending,registrations,nextSystemId,clock})
470	
471	def removal_publication_selected_value(~S:Data,~P:Data,~Payload:Type,
472	  selected:Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>) -> Bool:
473	  match selected:
474	    case None{}:True{}
475	    case Some{_}:False{}
476	def removal_publication_kept(~S:Data,~P:Data,~Payload:Type,
477	  ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
478	  +publication:P) -> Bool:
479	  removal_publication_selected_value(~S,~P,~Payload,select(Notice.Original{publication}))
480	def removal_publication_retain(~P:Data,keep:Bool,publication:P,rest:List<&2,P>) -> List<&2,P>:
481	  match keep:
482	    case True{}:publication <> rest
483	    case False{}:rest
484	def removal_publications_kept(~S:Data,~P:Data,~Payload:Type,
485	  ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
486	  publications:List<&2,P>) -> List<&2,P>:
487	  match publications:
488	    case []:[]
489	    case +publication <> rest:
490	      removal_publication_retain(~P,
491	        removal_publication_kept(~S,~P,~Payload,~select,publication),publication,
492	        removal_publications_kept(~S,~P,~Payload,~select,rest))
493	def removal_batch_kept(~S:Data,~P:Data,~Payload:Type,
494	  ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
495	  batch:Ev.Batch<P>) -> Ev.Batch<P>:
496	  match batch:
497	    case Ev.Batch{tick,values}:Ev.Batch{tick,removal_publications_kept(~S,~P,~Payload,~select,values)}
498	def removal_batches_kept(~S:Data,~P:Data,~Payload:Type,
499	  ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
500	  batches:List<&2,Ev.Batch<P>>) -> List<&2,Ev.Batch<P>>:
501	  match batches:
502	    case []:[]
503	    case batch <> rest:removal_batch_kept(~S,~P,~Payload,~select,batch) <> removal_batches_kept(~S,~P,~Payload,~select,rest)
504	def removal_release_state_checked(~S:Data,~P:Data,~Payload:Type,~F:Type,~H:Type,
505	  ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
506	  retained:Bool,state:Mixed.State<S,P,F,H>) -> Mixed.State<S,P,F,H>:
507	  match retained state:
508	    case True{} state:state
509	    case False{} Mixed.State{Family.State{family,owners,journal,frameStart},failures}:
510	      Mixed.State{Family.State{family,owners,removal_batches_kept(~S,~P,~Payload,~select,journal),frameStart},failures}
511	def removal_release_context_checked(~S:Data,~C:Type,~R:Type,~P:Data,~Payload:Type,~F:Type,~H:Type,
512	  ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
513	  state:Mixed.State<S,P,F,H>,tick:Nat,checked:W.World<S,C,R,Notice.Notice<S,P>> & Bool) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>:
514	  match checked:
515	    case (world,+retained):
516	      Route.Runtime{removal_release_world_checked(~S,~C,~R,~P,~Payload,~select,retained,world),
517	        removal_release_state_checked(~S,~P,~Payload,~F,~H,~select,retained,state),tick}
518	
519	def release_removal(~S:Data,~C:Type,~R:Type,~P:Data,~Payload:Type,~F:Type,~H:Type,
520	  ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
521	  context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
522	  owner:RemovalOwner<S,Payload,Notice.Notice<S,P>,select>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>:
523	  match context owner:
524	    case Route.Runtime{world,state,tick} RemovalOwner{_,_}:
525	      removal_release_context_checked(~S,~C,~R,~P,~Payload,~F,~H,~select,state,tick,
526	        removal_world_retained(~S,~C,~R,~P,world))
527	
528	def removal_param(~S:Data,~C:Type,~R:Type,~P:Data,~Payload:Type,~F:Type,~H:Type,
529	  ~inject:Identity.Declaration<S,Payload> -> W.Handle<S> -> Notice.Notice<S,P>,
530	  ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
531	  ~selection:Provision.Selection<S,Payload,Notice.Notice<S,P>,inject,select>) -> RP.Param<Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,RemovalOwner<S,Payload,Notice.Notice<S,P>,select>,RemovalView<S,Payload>,Nat,
532	  validate_removal(~S,~C,~R,~P,~Payload,~F,~H,~inject,~select,~selection),prepare_removal(~S,~C,~R,~P,~Payload,~F,~H,~select),commit_removal(~S,~C,~R,~P,~Payload,~F,~H,~select),release_removal(~S,~C,~R,~P,~Payload,~F,~H,~select)>:
533	  RP.make(~Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,~RemovalOwner<S,Payload,Notice.Notice<S,P>,select>,~RemovalView<S,Payload>,~Nat,
534	    ~validate_removal(~S,~C,~R,~P,~Payload,~F,~H,~inject,~select,~selection),
535	    ~prepare_removal(~S,~C,~R,~P,~Payload,~F,~H,~select),
536	    ~commit_removal(~S,~C,~R,~P,~Payload,~F,~H,~select),
537	    ~release_removal(~S,~C,~R,~P,~Payload,~F,~H,~select),
538	    removal_access(~S,~Payload,~Notice.Notice<S,P>,~inject,~select,selection))
539	
540	def initialize_removal(~S:Data,~C:Type,~R:Type,~P:Data,~Payload:Type,~F:Type,~H:Type,
541	  ~inject:Identity.Declaration<S,Payload> -> W.Handle<S> -> Notice.Notice<S,P>,
542	  ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
543	  ~selection:Provision.Selection<S,Payload,Notice.Notice<S,P>,inject,select>,
544	  context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
545	  facts:RP.RegistrationFacts) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (RemovalOwner<S,Payload,Notice.Notice<S,P>,select> & RP.Param<Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,RemovalOwner<S,Payload,Notice.Notice<S,P>,select>,RemovalView<S,Payload>,Nat,
546	  validate_removal(~S,~C,~R,~P,~Payload,~F,~H,~inject,~select,~selection),prepare_removal(~S,~C,~R,~P,~Payload,~F,~H,~select),commit_removal(~S,~C,~R,~P,~Payload,~F,~H,~select),release_removal(~S,~C,~R,~P,~Payload,~F,~H,~select)>):
547	  match facts:
548	    case RP.RegistrationFacts{+namespace,+id,_,_}:
549	      (context,
550	       (RemovalOwner{facts,Rm.Reader{namespace,id,Identity.key(~S,~Payload,removal_identity(~S,~Payload,~Notice.Notice<S,P>,~inject,~select,selection)),0n}},
551	        removal_param(~S,~C,~R,~P,~Payload,~F,~H,~inject,~select,~selection)))
552	
553	# Relation-failure cursors use the shared K allocator; queues and positions stay
554	# in Mixed.Failures and are only projected during prepare.
555	def relation_access(~S:Data,declarations:List<&2,KDecl.Declaration<S>>) -> List<&2,String>:
556	  KDecl.accesses(~S,declarations)
557	def relation_keys_equal(~S:Data,left:List<&2,KD.DescriptorKey<S>>,right:List<&2,KD.DescriptorKey<S>>) -> Bool:
558	  match left:
559	    case []:
560	      match right:
561	        case []:True{}
562	        case _ <> _:False{}
563	    case a <> restA:
564	      match right:
565	        case []:False{}
566	        case b <> restB:Bool.and(KD.key_equal(~S,a,b),relation_keys_equal(~S,restA,restB))
567	def has_reader(id:Maybe<&2,U32>) -> Bool:
568	  match id:
569	    case None{}:False{}
570	    case Some{_}:True{}
571	
572	def relation_validated(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
573	  ~declarations:List<&2,KDecl.Declaration<S>>,
574	  state:Mixed.State<S,P,F,H>,tick:Nat,facts:RP.RegistrationFacts,
575	  +id:Maybe<&2,U32>,+keys:List<&2,KD.DescriptorKey<S>>,
576	  registered:W.World<S,C,R,Notice.Notice<S,P>> & Bool) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (RelationOwner<S,P> & Bool):
577	  match facts:
578	    case RP.RegistrationFacts{_,_,_,+access}:
579	      match registered:
580	        case (world,isRegistered):
581	          +expected=relation_access(~S,declarations)
582	          +valid=Bool.and(isRegistered,Bool.and(access_subset(expected,access),
583	            Bool.and(relation_keys_equal(~S,keys,KDecl.keys(~S,declarations)),has_reader(id))))
584	          (Route.Runtime{world,state,tick},(RelationOwner{facts,id,keys},valid))
585	
586	def validate_relation(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
587	  ~declarations:List<&2,KDecl.Declaration<S>>,
588	  context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
589	  owner:RelationOwner<S,P>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (RelationOwner<S,P> & Bool):
590	  match context owner:
591	    case Route.Runtime{world,state,tick} RelationOwner{+facts,id,keys}:
592	      relation_validated(~S,~C,~R,~P,~F,~H,~declarations,state,tick,facts,id,keys,
593	        registered_context(~S,~C,~R,~Notice.Notice<S,P>,world,facts))
594	
595	def relation_prepared(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
596	  context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
597	  owner:RelationOwner<S,P>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (RelationOwner<S,P> & (RelationView<S,P> & RelationDelta)):
598	  match context owner:
599	    case Route.Runtime{world,Mixed.State{typed,Mixed.Failures{+domains,+positions,+tick,frameStart,boundary,capacity,nextReader}},routeTick} RelationOwner{facts,+id,+keys}:
600	      match id:
601	        case None{}:
602	          +readThrough=tick
603	          (Route.Runtime{world,Mixed.State{typed,Mixed.Failures{domains,positions,tick,frameStart,boundary,capacity,nextReader}},routeTick},
604	            (RelationOwner{facts,id,keys},(RelationView{[]},RelationDelta{id,readThrough})))
605	        case Some{+readerId}:
606	          +position=K.position_or(Ev.lookup(positions,readerId),readerId,tick)
607	          +readings=KRead.all(~S,~Notice.Notice<S,P>,keys,domains,position)
608	          +readThrough=tick
609	          # Match standalone failed reads: activation retains unread input,
610	          # while only the successful commit advances its cursor.
611	          (Route.Runtime{world,Mixed.State{typed,Mixed.Failures{
612	            KRead.activate(~S,~Notice.Notice<S,P>,keys,domains,readerId),
613	            Ev.activate(positions,readerId,tick),tick,frameStart,boundary,capacity,nextReader}},routeTick},
614	            (RelationOwner{facts,id,keys},(RelationView{readings},RelationDelta{id,readThrough})))
615	
616	def prepare_relation(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
617	  ~declarations:List<&2,KDecl.Declaration<S>>,
618	  context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,+cursor:Maybe<&2,Tick.Tick>,
619	  owner:RelationOwner<S,P>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (RelationOwner<S,P> & (RelationView<S,P> & RelationDelta)):
620	  relation_prepared(~S,~C,~R,~P,~F,~H,context,owner)
621	
622	def relation_commit_match(~S:Data,~P:Data,
623	  domains:List<&2,KD.Domain<S,Notice.Notice<S,P>>>,positions:List<&2,Ev.Position>,
624	  keys:List<&2,KD.DescriptorKey<S>>, +readerId:U32,+readThrough:Nat,matched:Bool) -> List<&2,KD.Domain<S,Notice.Notice<S,P>>> & List<&2,Ev.Position>:
625	  match matched:
626	    case True{}:
627	      (KRead.activate(~S,~Notice.Notice<S,P>,keys,domains,readerId),
628	       Ev.update(Ev.activate(positions,readerId,readThrough),readerId,readThrough,False{}))
629	    case False{}:(domains,positions)
630	
631	def relation_commit_selected(~S:Data,~P:Data,domains:List<&2,KD.Domain<S,Notice.Notice<S,P>>>,
632	  positions:List<&2,Ev.Position>,keys:List<&2,KD.DescriptorKey<S>>,id:Maybe<&2,U32>,
633	  delta:RelationDelta) -> List<&2,KD.Domain<S,Notice.Notice<S,P>>> & List<&2,Ev.Position>:
634	  match id delta:
635	    case Some{+readerId} RelationDelta{Some{deltaId},readThrough}:
636	      relation_commit_match(~S,~P,domains,positions,keys,readerId,readThrough,U32.is_eq(readerId,deltaId))
637	    case _ _:(domains,positions)
638	
639	def relation_commit_updated(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
640	  world:W.World<S,C,R,Notice.Notice<S,P>>,typed:Family.State<P,F,H>,
641	  tick:Nat,frameStart:Nat,boundary:Nat,capacity:Nat,nextReader:U32,routeTick:Nat,
642	  facts:RP.RegistrationFacts,id:Maybe<&2,U32>,keys:List<&2,KD.DescriptorKey<S>>,
643	  updated:List<&2,KD.Domain<S,Notice.Notice<S,P>>> & List<&2,Ev.Position>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & RelationOwner<S,P>:
644	  match updated:
645	    case (updatedDomains,updatedPositions):
646	      (Route.Runtime{world,Mixed.State{typed,Mixed.Failures{updatedDomains,updatedPositions,tick,frameStart,boundary,capacity,nextReader}},routeTick},
647	       RelationOwner{facts,id,keys})
648	
649	def relation_commit_state(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
650	  world:W.World<S,C,R,Notice.Notice<S,P>>,typed:Family.State<P,F,H>,
651	  failures:Mixed.Failures<S,P>,routeTick:Nat,facts:RP.RegistrationFacts,
652	  +id:Maybe<&2,U32>,+keys:List<&2,KD.DescriptorKey<S>>,delta:RelationDelta) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & RelationOwner<S,P>:
653	  match failures:
654	    case Mixed.Failures{domains,positions,tick,frameStart,boundary,capacity,nextReader}:
655	      relation_commit_updated(~S,~C,~R,~P,~F,~H,world,typed,tick,frameStart,boundary,capacity,nextReader,routeTick,facts,id,keys,
656	        relation_commit_selected(~S,~P,domains,positions,keys,id,delta))
657	
658	def relation_release_selected(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
659	  context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
660	  id:Maybe<&2,U32>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>:
661	  match context id:
662	    case Route.Runtime{world,Mixed.State{typed,Mixed.Failures{domains,positions,+tick,frameStart,boundary,capacity,nextReader}},routeTick} None{}:
663	      Route.Runtime{world,Mixed.State{typed,Mixed.Failures{domains,positions,tick,frameStart,boundary,capacity,nextReader}},routeTick}
664	    case Route.Runtime{world,Mixed.State{typed,Mixed.Failures{domains,positions,+tick,frameStart,boundary,capacity,nextReader}},routeTick} Some{+readerId}:
665	      Route.Runtime{world,
666	        Mixed.State{typed,Mixed.Failures{
667	          KDispose.release(~S,~Notice.Notice<S,P>,domains,readerId),
668	          Ev.update(positions,readerId,tick,True{}),tick,frameStart,boundary,capacity,nextReader}},routeTick}
669	
670	def release_relation(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
671	  context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
672	  owner:RelationOwner<S,P>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>:
673	  match context owner:
674	    case context RelationOwner{_,id,_}:relation_release_selected(~S,~C,~R,~P,~F,~H,context,id)
675	
676	def commit_relation(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
677	  context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
678	  owner:RelationOwner<S,P>,delta:RelationDelta,+cursor:Tick.Tick) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & RelationOwner<S,P>:
679	  match context owner:
680	    case Route.Runtime{world,Mixed.State{typed,failures},routeTick} RelationOwner{facts,id,keys}:
681	      relation_commit_state(~S,~C,~R,~P,~F,~H,world,typed,failures,routeTick,facts,id,keys,delta)
682	
683	def relation_param(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
684	  ~declarations:List<&2,KDecl.Declaration<S>>) -> RP.Param<Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,RelationOwner<S,P>,RelationView<S,P>,RelationDelta,
685	  validate_relation(~S,~C,~R,~P,~F,~H,~declarations),prepare_relation(~S,~C,~R,~P,~F,~H,~declarations),commit_relation(~S,~C,~R,~P,~F,~H),release_relation(~S,~C,~R,~P,~F,~H)>:
686	  RP.make(~Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,~RelationOwner<S,P>,~RelationView<S,P>,~RelationDelta,
687	    ~validate_relation(~S,~C,~R,~P,~F,~H,~declarations),
688	    ~prepare_relation(~S,~C,~R,~P,~F,~H,~declarations),
689	    ~commit_relation(~S,~C,~R,~P,~F,~H),
690	    ~release_relation(~S,~C,~R,~P,~F,~H),
691	    relation_access(~S,declarations))
692	
693	def relation_initialized_id(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
694	  ~declarations:List<&2,KDecl.Declaration<S>>,
695	  context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
696	  facts:RP.RegistrationFacts,id:Maybe<&2,U32>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (RelationOwner<S,P> & RP.Param<Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,RelationOwner<S,P>,RelationView<S,P>,RelationDelta,
697	  validate_relation(~S,~C,~R,~P,~F,~H,~declarations),prepare_relation(~S,~C,~R,~P,~F,~H,~declarations),commit_relation(~S,~C,~R,~P,~F,~H),release_relation(~S,~C,~R,~P,~F,~H)>):
698	  (context,(RelationOwner{facts,id,KDecl.keys(~S,declarations)},relation_param(~S,~C,~R,~P,~F,~H,declarations)))
699	
700	def relation_initialized(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
701	  ~declarations:List<&2,KDecl.Declaration<S>>,
702	  facts:RP.RegistrationFacts,
703	  reserved:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & Maybe<&2,U32>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (RelationOwner<S,P> & RP.Param<Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,RelationOwner<S,P>,RelationView<S,P>,RelationDelta,
704	  validate_relation(~S,~C,~R,~P,~F,~H,~declarations),prepare_relation(~S,~C,~R,~P,~F,~H,~declarations),commit_relation(~S,~C,~R,~P,~F,~H),release_relation(~S,~C,~R,~P,~F,~H)>):
705	  match reserved:
706	    case (context,id):relation_initialized_id(~S,~C,~R,~P,~F,~H,~declarations,context,facts,id)
707	
708	def initialize_relation(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
709	  ~declarations:List<&2,KDecl.Declaration<S>>,
710	  context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
711	  facts:RP.RegistrationFacts) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (RelationOwner<S,P> & RP.Param<Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,RelationOwner<S,P>,RelationView<S,P>,RelationDelta,
712	  validate_relation(~S,~C,~R,~P,~F,~H,~declarations),prepare_relation(~S,~C,~R,~P,~F,~H,~declarations),commit_relation(~S,~C,~R,~P,~F,~H),release_relation(~S,~C,~R,~P,~F,~H)>):
713	  relation_initialized(~S,~C,~R,~P,~F,~H,~declarations,facts,
714	    Mixed.reserve_failure_reader(~S,~C,~R,~P,~F,~H,context))