1module Runtime.Protocol
2
3import Runtime.RegionTransfer
4import Std.Natural
5import Std.List
6
7-- Decision selectors have their own type: a learning operation or payload
8-- cannot accidentally stand in for a branch predicate. Unconditional protocols
9-- use this uninhabited type, so no unavailable selector is replaced by a value.
10family ProtocolNoDecision : Type 0
11
12end-family
13
14-- Routes form an ordered dissemination tree after admission. The sender must
15-- already know the decision, and each receiver is introduced exactly once.
16-- This represents declared edges, not every member of the execution fleet.
17family ProtocolAnnouncements : Type 0
18parameter erased announcementPayload : Type 0
19constructor ProtocolAnnouncementsEnd
20constructor ProtocolAnnouncementsNext
21field unrestricted announcementIdentity : (family RegionTransferIdentity)
22field unrestricted announcementBinding : announcementPayload
23recursive unrestricted announcementRest
24
25end-family
26
27-- The global syntax describes dependency order, independent of a device or
28-- learning algorithm. Repeated and conditional bodies remain shared syntax.
29family GlobalProtocol : Type 0
30parameter erased protocolOperation : Type 0
31parameter erased protocolPayload : Type 0
32parameter erased protocolDecision : Type 0
33constructor GlobalProtocolEnd
34constructor GlobalProtocolLocal
35field unrestricted globalLocalParticipant : Nat
36field unrestricted globalLocalOperation : protocolOperation
37recursive unrestricted globalLocalRest
38constructor GlobalProtocolTransfer
39field unrestricted globalTransferIdentity : (family RegionTransferIdentity)
40field unrestricted globalTransferPayload : protocolPayload
41recursive unrestricted globalTransferRest
42constructor GlobalProtocolRepeat
43field unrestricted globalRepeatCount : Nat
44recursive unrestricted globalRepeatBody
45recursive unrestricted globalRepeatRest
46constructor GlobalProtocolChoice
47field unrestricted globalChoiceIdentity : (family RegionTransferIdentity)
48field unrestricted globalChoiceSelector : protocolDecision
49field unrestricted globalChoiceAnnouncements : (family ProtocolAnnouncements protocolPayload)
50recursive unrestricted globalChoiceZero
51recursive unrestricted globalChoiceOne
52recursive unrestricted globalChoiceRest
53
54end-family
55
56family ProtocolDirection : Type 0
57constructor ProtocolSend
58constructor ProtocolReceive
59
60end-family
61
62family ParticipantProtocol : Type 0
63parameter erased participantOperation : Type 0
64parameter erased participantPayload : Type 0
65parameter erased participantDecision : Type 0
66constructor ParticipantProtocolEnd
67constructor ParticipantProtocolLocal
68field unrestricted participantLocalOperation : participantOperation
69recursive unrestricted participantLocalRest
70constructor ParticipantProtocolTransfer
71field unrestricted participantTransferDirection : (family ProtocolDirection)
72field unrestricted participantTransferIdentity : (family RegionTransferIdentity)
73field unrestricted participantTransferPayload : participantPayload
74recursive unrestricted participantTransferRest
75constructor ParticipantProtocolRepeat
76field unrestricted participantRepeatCount : Nat
77recursive unrestricted participantRepeatBody
78recursive unrestricted participantRepeatRest
79constructor ParticipantProtocolChoice
80field unrestricted participantChoiceRole : Nat
81field unrestricted participantChoiceIdentity : (family RegionTransferIdentity)
82field unrestricted participantChoiceSelector : participantDecision
83field unrestricted participantChoiceAnnouncements : (family ProtocolAnnouncements participantPayload)
84recursive unrestricted participantChoiceZero
85recursive unrestricted participantChoiceOne
86recursive unrestricted participantChoiceRest
87
88end-family
89
90family ProtocolFailure : Type 0
91constructor ProtocolMembershipBounds
92constructor ProtocolParticipantBounds
93constructor ProtocolSenderBounds
94constructor ProtocolReceiverBounds
95constructor ProtocolSelfTransfer
96constructor ProtocolRepeatBounds
97constructor ProtocolLocalUnavailable
98constructor ProtocolTransferUnavailable
99constructor ProtocolChoiceAuthority
100constructor ProtocolChoiceRoutes
101constructor ProtocolChoiceUninformed
102constructor ProtocolChoiceUnavailable
103
104end-family
105
106def protocolNoDecision =
107 (lambda erased payload : Type 0 .
108 (lambda unrestricted owner : Nat .
109 (lambda unrestricted selector : (family ProtocolNoDecision) .
110 (lambda unrestricted announcements : (family ProtocolAnnouncements payload) .
111 (eliminate
112 ProtocolNoDecision
113 (lambda unrestricted current : (family ProtocolNoDecision) . Nat)
114 selector)))))
115
116def participantProtocolEmpty =
117 (lambda erased operation : Type 0 .
118 (lambda erased payload : Type 0 .
119 (lambda erased decision : Type 0 .
120 (lambda unrestricted program : (family ParticipantProtocol operation payload decision) .
121 (eliminate
122 ParticipantProtocol
123 (lambda unrestricted current : (family ParticipantProtocol operation payload decision) .
124 Nat)
125 program
126 (branch ParticipantProtocolEnd . 1)
127 (branch ParticipantProtocolLocal value rest induction . 0)
128 (branch ParticipantProtocolTransfer direction identity value rest induction . 0)
129 (branch ParticipantProtocolRepeat count body rest bodyInduction restInduction . 0)
130 (branch
131 ParticipantProtocolChoice
132 role
133 identity
134 selector
135 announcements
136 zeroBody
137 oneBody
138 rest
139 zeroInduction
140 oneInduction
141 restInduction
142 .
143 0))))))
144
145def protocolAnnouncementsEmpty =
146 (lambda erased payload : Type 0 .
147 (lambda unrestricted announcements : (family ProtocolAnnouncements payload) .
148 (eliminate
149 ProtocolAnnouncements
150 (lambda unrestricted current : (family ProtocolAnnouncements payload) . Nat)
151 announcements
152 (branch ProtocolAnnouncementsEnd . 1)
153 (branch ProtocolAnnouncementsNext identity value rest induction . 0))))
154
155-- The authority is encoded once, in the canonical choice identity. That
156-- anchor names the owner in both route fields; real announcements substitute
157-- their own sender/receiver while preserving every other identity component.
158def protocolInformed =
159 (lambda erased payload : Type 0 .
160 (lambda unrestricted anchor : (family RegionTransferIdentity) .
161 (lambda unrestricted announcements : (family ProtocolAnnouncements payload) .
162 (lambda unrestricted role : Nat .
163 (naturalOr
164 (naturalEqual role (regionTransferSender anchor))
165 (eliminate
166 ProtocolAnnouncements
167 (lambda unrestricted current : (family ProtocolAnnouncements payload) . Nat)
168 announcements
169 (branch ProtocolAnnouncementsEnd . 0)
170 (branch
171 ProtocolAnnouncementsNext
172 identity
173 value
174 rest
175 induction
176 .
177 (naturalOr (naturalEqual role (regionTransferReceiver identity)) induction))))))))
178
179def projectProtocolAnnouncements =
180 (lambda erased payload : Type 0 .
181 (lambda unrestricted role : Nat .
182 (lambda unrestricted announcements : (family ProtocolAnnouncements payload) .
183 (eliminate
184 ProtocolAnnouncements
185 (lambda unrestricted current : (family ProtocolAnnouncements payload) .
186 (family ProtocolAnnouncements payload))
187 announcements
188 (branch
189 ProtocolAnnouncementsEnd
190 .
191 (constructor ProtocolAnnouncements ProtocolAnnouncementsEnd payload))
192 (branch
193 ProtocolAnnouncementsNext
194 identity
195 value
196 rest
197 induction
198 .
199 (nat-eliminate
200 (lambda unrestricted flag : Nat . (family ProtocolAnnouncements payload))
201 induction
202 (lambda unrestricted prior : Nat .
203 (lambda unrestricted ignored : (family ProtocolAnnouncements payload) .
204 (constructor
205 ProtocolAnnouncements
206 ProtocolAnnouncementsNext
207 payload
208 identity
209 value
210 induction)))
211 (naturalOr
212 (naturalEqual role (regionTransferSender identity))
213 (naturalEqual role (regionTransferReceiver identity)))))))))
214
215def protocolLocal =
216 (lambda erased operation : Type 0 .
217 (lambda erased payload : Type 0 .
218 (lambda erased decision : Type 0 .
219 (lambda unrestricted owner : Nat .
220 (lambda unrestricted value : operation .
221 (lambda unrestricted rest : (family GlobalProtocol operation payload decision) .
222 (constructor
223 GlobalProtocol
224 GlobalProtocolLocal
225 operation
226 payload
227 decision
228 owner
229 value
230 rest)))))))
231
232def protocolTransfer =
233 (lambda erased operation : Type 0 .
234 (lambda erased payload : Type 0 .
235 (lambda erased decision : Type 0 .
236 (lambda unrestricted identity : (family RegionTransferIdentity) .
237 (lambda unrestricted value : payload .
238 (lambda unrestricted rest : (family GlobalProtocol operation payload decision) .
239 (constructor
240 GlobalProtocol
241 GlobalProtocolTransfer
242 operation
243 payload
244 decision
245 identity
246 value
247 rest)))))))
248
249def protocolRepeat =
250 (lambda erased operation : Type 0 .
251 (lambda erased payload : Type 0 .
252 (lambda erased decision : Type 0 .
253 (lambda unrestricted count : Nat .
254 (lambda unrestricted body : (family GlobalProtocol operation payload decision) .
255 (lambda unrestricted rest : (family GlobalProtocol operation payload decision) .
256 (constructor
257 GlobalProtocol
258 GlobalProtocolRepeat
259 operation
260 payload
261 decision
262 count
263 body
264 rest)))))))
265
266def protocolChoice =
267 (lambda erased operation : Type 0 .
268 (lambda erased payload : Type 0 .
269 (lambda erased decision : Type 0 .
270 (lambda unrestricted identity : (family RegionTransferIdentity) .
271 (lambda unrestricted selector : decision .
272 (lambda unrestricted announcements : (family ProtocolAnnouncements payload) .
273 (lambda unrestricted zeroBody : (family GlobalProtocol operation payload decision) .
274 (lambda unrestricted oneBody : (family GlobalProtocol operation payload decision) .
275 (lambda unrestricted rest : (family GlobalProtocol operation payload decision) .
276 (constructor
277 GlobalProtocol
278 GlobalProtocolChoice
279 operation
280 payload
281 decision
282 identity
283 selector
284 announcements
285 zeroBody
286 oneBody
287 rest))))))))))
288
289-- Lift reusable local semantics into a system operation type. Transfers,
290-- choices and repetition retain their identities and order unchanged.
291def mapGlobalProtocolOperations =
292 (lambda erased source : Type 0 .
293 (lambda erased target : Type 0 .
294 (lambda erased payload : Type 0 .
295 (lambda erased decision : Type 0 .
296 (lambda unrestricted transform : (pi unrestricted value : source . target) .
297 (lambda unrestricted program : (family GlobalProtocol source payload decision) .
298 (eliminate
299 GlobalProtocol
300 (lambda unrestricted current : (family GlobalProtocol source payload decision) .
301 (family GlobalProtocol target payload decision))
302 program
303 (branch
304 GlobalProtocolEnd
305 .
306 (constructor GlobalProtocol GlobalProtocolEnd target payload decision))
307 (branch
308 GlobalProtocolLocal
309 role
310 value
311 rest
312 induction
313 .
314 (constructor
315 GlobalProtocol
316 GlobalProtocolLocal
317 target
318 payload
319 decision
320 role
321 (transform value)
322 induction))
323 (branch
324 GlobalProtocolTransfer
325 identity
326 value
327 rest
328 induction
329 .
330 (constructor
331 GlobalProtocol
332 GlobalProtocolTransfer
333 target
334 payload
335 decision
336 identity
337 value
338 induction))
339 (branch
340 GlobalProtocolRepeat
341 count
342 body
343 rest
344 bodyResult
345 restResult
346 .
347 (constructor
348 GlobalProtocol
349 GlobalProtocolRepeat
350 target
351 payload
352 decision
353 count
354 bodyResult
355 restResult))
356 (branch
357 GlobalProtocolChoice
358 identity
359 selector
360 announcements
361 zeroBody
362 oneBody
363 rest
364 zeroResult
365 oneResult
366 restResult
367 .
368 (constructor
369 GlobalProtocol
370 GlobalProtocolChoice
371 target
372 payload
373 decision
374 identity
375 selector
376 announcements
377 zeroResult
378 oneResult
379 restResult)))))))))
380
381-- Declared transfer storage occurrences, for local allocation/setup. Repeats
382-- contribute their body once; both choice arms remain visible. This does not
383-- report runtime completions or authorize rearming an unselected transfer.
384def participantProtocolPayloads =
385 (lambda erased operation : Type 0 .
386 (lambda erased payload : Type 0 .
387 (lambda erased decision : Type 0 .
388 (lambda unrestricted program : (family ParticipantProtocol operation payload decision) .
389 (eliminate
390 ParticipantProtocol
391 (lambda unrestricted current : (family ParticipantProtocol operation payload decision) .
392 (family StdList payload))
393 program
394 (branch ParticipantProtocolEnd . (constructor StdList StdListEmpty payload))
395 (branch ParticipantProtocolLocal value rest induction . induction)
396 (branch
397 ParticipantProtocolTransfer
398 direction
399 identity
400 value
401 rest
402 induction
403 .
404 (constructor StdList StdListCons payload value induction))
405 (branch
406 ParticipantProtocolRepeat
407 count
408 body
409 rest
410 bodyResult
411 restResult
412 .
413 (stdListAppend payload bodyResult restResult))
414 (branch
415 ParticipantProtocolChoice
416 role
417 identity
418 selector
419 announcements
420 zeroBody
421 oneBody
422 rest
423 zeroResult
424 oneResult
425 restResult
426 .
427 (stdListAppend
428 payload
429 (eliminate
430 ProtocolAnnouncements
431 (lambda unrestricted current : (family ProtocolAnnouncements payload) .
432 (family StdList payload))
433 announcements
434 (branch ProtocolAnnouncementsEnd . (constructor StdList StdListEmpty payload))
435 (branch
436 ProtocolAnnouncementsNext
437 identity
438 value
439 rest
440 induction
441 .
442 (constructor StdList StdListCons payload value induction)))
443 (stdListAppend payload zeroResult (stdListAppend payload oneResult restResult)))))))))
444
445-- Append once at the outer continuation. Repeated/conditional bodies keep
446-- their original ends; appending there would duplicate the continuation.
447def appendGlobalProtocol =
448 (lambda erased operation : Type 0 .
449 (lambda erased payload : Type 0 .
450 (lambda erased decision : Type 0 .
451 (lambda unrestricted program : (family GlobalProtocol operation payload decision) .
452 (lambda unrestricted tail : (family GlobalProtocol operation payload decision) .
453 (eliminate
454 GlobalProtocol
455 (lambda unrestricted current : (family GlobalProtocol operation payload decision) .
456 (family GlobalProtocol operation payload decision))
457 program
458 (branch GlobalProtocolEnd . tail)
459 (branch
460 GlobalProtocolLocal
461 role
462 value
463 rest
464 induction
465 .
466 (constructor
467 GlobalProtocol
468 GlobalProtocolLocal
469 operation
470 payload
471 decision
472 role
473 value
474 induction))
475 (branch
476 GlobalProtocolTransfer
477 identity
478 value
479 rest
480 induction
481 .
482 (constructor
483 GlobalProtocol
484 GlobalProtocolTransfer
485 operation
486 payload
487 decision
488 identity
489 value
490 induction))
491 (branch
492 GlobalProtocolRepeat
493 count
494 body
495 rest
496 bodyResult
497 restResult
498 .
499 (constructor
500 GlobalProtocol
501 GlobalProtocolRepeat
502 operation
503 payload
504 decision
505 count
506 body
507 restResult))
508 (branch
509 GlobalProtocolChoice
510 identity
511 selector
512 announcements
513 zeroBody
514 oneBody
515 rest
516 zeroResult
517 oneResult
518 restResult
519 .
520 (constructor
521 GlobalProtocol
522 GlobalProtocolChoice
523 operation
524 payload
525 decision
526 identity
527 selector
528 announcements
529 zeroBody
530 oneBody
531 restResult))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.