1module Compiler.Planning.Protocol
2
3import Runtime.Protocol
4import Runtime.RegionTransfer
5import Runtime.RegionFrame
6import Std.Foundation
7import Std.Natural
8
9-- Every admission check precedes local program emission. A backend supplies
10-- capability checks for its typed operations and transfer bindings; an absent
11-- lowering is a refusal, never an empty command or a host substitution.
12def protocolAccepted : (family StdResult (family ProtocolFailure) Nat) =
13 (constructor StdResult StdSuccess (family ProtocolFailure) Nat 1)
14
15def protocolRequire =
16 (lambda unrestricted flag : Nat .
17 (lambda unrestricted failure : (family ProtocolFailure) .
18 (lambda unrestricted next : (family StdResult (family ProtocolFailure) Nat) .
19 (nat-eliminate
20 (lambda unrestricted current : Nat . (family StdResult (family ProtocolFailure) Nat))
21 (constructor StdResult StdFailure (family ProtocolFailure) Nat failure)
22 (lambda unrestricted previous : Nat .
23 (lambda unrestricted ignored : (family StdResult (family ProtocolFailure) Nat) . next))
24 flag))))
25
26def protocolCheckThen =
27 (lambda unrestricted first : (family StdResult (family ProtocolFailure) Nat) .
28 (lambda unrestricted next : (family StdResult (family ProtocolFailure) Nat) .
29 (eliminate
30 StdResult
31 (lambda unrestricted current : (family StdResult (family ProtocolFailure) Nat) .
32 (family StdResult (family ProtocolFailure) Nat))
33 first
34 (branch
35 StdFailure
36 error
37 .
38 (constructor StdResult StdFailure (family ProtocolFailure) Nat error))
39 (branch StdSuccess value . next))))
40
41-- A topologically ordered tree has one authority and one incoming decision
42-- per receiver. Admission checks the declared edges only. The current source
43-- implementation uses a persistent membership predicate (quadratic in edges
44-- in the worst case); hierarchical fleet planning must bound per-cell edges.
45def protocolAnnouncementsAdmitted =
46 (lambda erased payload : Type 0 .
47 (lambda unrestricted participants : Nat .
48 (lambda unrestricted anchor : (family RegionTransferIdentity) .
49 (lambda unrestricted transfer : (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . Nat)) .
50 (lambda unrestricted announcements : (family ProtocolAnnouncements payload) .
51 (app
52 (eliminate
53 ProtocolAnnouncements
54 (lambda unrestricted current : (family ProtocolAnnouncements payload) .
55 (pi unrestricted known : (pi unrestricted role : Nat . Nat) . Nat))
56 announcements
57 (branch
58 ProtocolAnnouncementsEnd
59 .
60 (lambda unrestricted known : (pi unrestricted role : Nat . Nat) . 1))
61 (branch
62 ProtocolAnnouncementsNext
63 identity
64 value
65 rest
66 induction
67 .
68 (lambda unrestricted known : (pi unrestricted role : Nat . Nat) .
69 (naturalAnd
70 (known (regionTransferSender identity))
71 (naturalAnd
72 (naturalEqual (known (regionTransferReceiver identity)) 0)
73 (naturalAnd
74 (naturalLess (regionTransferReceiver identity) participants)
75 (naturalAnd
76 (regionTransferIdentityEqual
77 (regionTransferWithRoute
78 anchor
79 (regionTransferSender identity)
80 (regionTransferReceiver identity))
81 identity)
82 (naturalAnd
83 (transfer identity value)
84 (naturalAnd
85 (induction
86 (lambda unrestricted role : Nat .
87 (naturalOr
88 (known role)
89 (naturalEqual role (regionTransferReceiver identity)))))
90 1)))))))))
91 (lambda unrestricted role : Nat . (naturalEqual role (regionTransferSender anchor)))))))))
92
93-- Every participant mentioned in either conditional body must know the
94-- decision, including forwarding-only roles of a nested choice. No guessing
95-- or implicit merging of unrelated branch schedules is permitted.
96def globalProtocolCovered =
97 (lambda erased operation : Type 0 .
98 (lambda erased payload : Type 0 .
99 (lambda erased decision : Type 0 .
100 (lambda unrestricted known : (pi unrestricted role : Nat . Nat) .
101 (lambda unrestricted program : (family GlobalProtocol operation payload decision) .
102 (eliminate
103 GlobalProtocol
104 (lambda unrestricted current : (family GlobalProtocol operation payload decision) .
105 Nat)
106 program
107 (branch GlobalProtocolEnd . 1)
108 (branch
109 GlobalProtocolLocal
110 role
111 value
112 rest
113 induction
114 .
115 (naturalAnd (known role) induction))
116 (branch
117 GlobalProtocolTransfer
118 identity
119 value
120 rest
121 induction
122 .
123 (naturalAnd
124 (known (regionTransferSender identity))
125 (naturalAnd (known (regionTransferReceiver identity)) (naturalAnd induction 1))))
126 (branch
127 GlobalProtocolRepeat
128 count
129 body
130 rest
131 bodyCheck
132 restCheck
133 .
134 (naturalAnd bodyCheck restCheck))
135 (branch
136 GlobalProtocolChoice
137 identity
138 selector
139 announcements
140 zeroBody
141 oneBody
142 rest
143 zeroCheck
144 oneCheck
145 restCheck
146 .
147 (naturalAnd
148 (known (regionTransferSender identity))
149 (naturalAnd
150 (eliminate
151 ProtocolAnnouncements
152 (lambda unrestricted current : (family ProtocolAnnouncements payload) . Nat)
153 announcements
154 (branch ProtocolAnnouncementsEnd . 1)
155 (branch
156 ProtocolAnnouncementsNext
157 edge
158 value
159 tail
160 induction
161 .
162 (naturalAnd
163 (known (regionTransferSender edge))
164 (naturalAnd
165 (known (regionTransferReceiver edge))
166 (naturalAnd induction 1)))))
167 (naturalAnd zeroCheck (naturalAnd oneCheck (naturalAnd restCheck 1))))))))))))
168
169def checkGlobalProtocol =
170 (lambda erased operation : Type 0 .
171 (lambda erased payload : Type 0 .
172 (lambda erased decision : Type 0 .
173 (lambda unrestricted participants : Nat .
174 (lambda unrestricted local : (pi unrestricted owner : Nat . (pi unrestricted value : operation . Nat)) .
175 (lambda unrestricted transfer : (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . Nat)) .
176 (lambda unrestricted choice : (pi unrestricted owner : Nat . (pi unrestricted selector : decision . (pi unrestricted announcements : (family ProtocolAnnouncements payload) . Nat))) .
177 (lambda unrestricted program : (family GlobalProtocol operation payload decision) .
178 (protocolRequire
179 (naturalAnd
180 (naturalNonzero participants)
181 (naturalLessOrEqual participants regionFrameWordLimit))
182 (constructor ProtocolFailure ProtocolMembershipBounds)
183 (eliminate
184 GlobalProtocol
185 (lambda unrestricted current : (family GlobalProtocol operation payload decision) .
186 (family StdResult (family ProtocolFailure) Nat))
187 program
188 (branch GlobalProtocolEnd . protocolAccepted)
189 (branch
190 GlobalProtocolLocal
191 participant
192 value
193 rest
194 induction
195 .
196 (protocolRequire
197 (naturalLess participant participants)
198 (constructor ProtocolFailure ProtocolParticipantBounds)
199 (protocolRequire
200 (local participant value)
201 (constructor ProtocolFailure ProtocolLocalUnavailable)
202 induction)))
203 (branch
204 GlobalProtocolTransfer
205 identity
206 value
207 rest
208 induction
209 .
210 (protocolRequire
211 (naturalLess (regionTransferSender identity) participants)
212 (constructor ProtocolFailure ProtocolSenderBounds)
213 (protocolRequire
214 (naturalLess (regionTransferReceiver identity) participants)
215 (constructor ProtocolFailure ProtocolReceiverBounds)
216 (protocolRequire
217 (naturalEqual
218 (naturalEqual
219 (regionTransferSender identity)
220 (regionTransferReceiver identity))
221 0)
222 (constructor ProtocolFailure ProtocolSelfTransfer)
223 (protocolRequire
224 (transfer identity value)
225 (constructor ProtocolFailure ProtocolTransferUnavailable)
226 induction)))))
227 (branch
228 GlobalProtocolRepeat
229 count
230 body
231 rest
232 bodyCheck
233 restCheck
234 .
235 (protocolRequire
236 (naturalLessOrEqual count regionFrameWordLimit)
237 (constructor ProtocolFailure ProtocolRepeatBounds)
238 (protocolCheckThen
239 bodyCheck
240 (protocolCheckThen restCheck protocolAccepted))))
241 (branch
242 GlobalProtocolChoice
243 identity
244 selector
245 announcements
246 zeroBody
247 oneBody
248 rest
249 zeroCheck
250 oneCheck
251 restCheck
252 .
253 (protocolRequire
254 (naturalAnd
255 (naturalLess (regionTransferSender identity) participants)
256 (naturalEqual
257 (regionTransferSender identity)
258 (regionTransferReceiver identity)))
259 (constructor ProtocolFailure ProtocolChoiceAuthority)
260 (protocolRequire
261 (protocolAnnouncementsAdmitted
262 payload
263 participants
264 identity
265 transfer
266 announcements)
267 (constructor ProtocolFailure ProtocolChoiceRoutes)
268 (protocolRequire
269 (naturalAnd
270 (globalProtocolCovered
271 operation
272 payload
273 decision
274 (protocolInformed payload identity announcements)
275 zeroBody)
276 (globalProtocolCovered
277 operation
278 payload
279 decision
280 (protocolInformed payload identity announcements)
281 oneBody))
282 (constructor ProtocolFailure ProtocolChoiceUninformed)
283 (protocolRequire
284 (choice (regionTransferSender identity) selector announcements)
285 (constructor ProtocolFailure ProtocolChoiceUnavailable)
286 (protocolCheckThen
287 zeroCheck
288 (protocolCheckThen
289 oneCheck
290 (protocolCheckThen restCheck protocolAccepted))))))))))))))))))
291
292-- Projection preserves bodies once, and does not enumerate fleet membership.
293-- This helper requires admission; planParticipantProtocol is the checked entry.
294def projectGlobalProtocol =
295 (lambda erased operation : Type 0 .
296 (lambda erased payload : Type 0 .
297 (lambda erased decision : Type 0 .
298 (lambda unrestricted participant : Nat .
299 (lambda unrestricted program : (family GlobalProtocol operation payload decision) .
300 (eliminate
301 GlobalProtocol
302 (lambda unrestricted current : (family GlobalProtocol operation payload decision) .
303 (family ParticipantProtocol operation payload decision))
304 program
305 (branch
306 GlobalProtocolEnd
307 .
308 (constructor ParticipantProtocol ParticipantProtocolEnd operation payload decision))
309 (branch
310 GlobalProtocolLocal
311 owner
312 value
313 rest
314 induction
315 .
316 (nat-eliminate
317 (lambda unrestricted flag : Nat .
318 (family ParticipantProtocol operation payload decision))
319 induction
320 (lambda unrestricted prior : Nat .
321 (lambda unrestricted ignored : (family ParticipantProtocol operation payload decision) .
322 (constructor
323 ParticipantProtocol
324 ParticipantProtocolLocal
325 operation
326 payload
327 decision
328 value
329 induction)))
330 (naturalEqual participant owner)))
331 (branch
332 GlobalProtocolTransfer
333 identity
334 value
335 rest
336 induction
337 .
338 (nat-eliminate
339 (lambda unrestricted flag : Nat .
340 (family ParticipantProtocol operation payload decision))
341 (nat-eliminate
342 (lambda unrestricted flag : Nat .
343 (family ParticipantProtocol operation payload decision))
344 induction
345 (lambda unrestricted prior : Nat .
346 (lambda unrestricted ignored : (family ParticipantProtocol operation payload decision) .
347 (constructor
348 ParticipantProtocol
349 ParticipantProtocolTransfer
350 operation
351 payload
352 decision
353 (constructor ProtocolDirection ProtocolReceive)
354 identity
355 value
356 induction)))
357 (naturalEqual participant (regionTransferReceiver identity)))
358 (lambda unrestricted prior : Nat .
359 (lambda unrestricted ignored : (family ParticipantProtocol operation payload decision) .
360 (constructor
361 ParticipantProtocol
362 ParticipantProtocolTransfer
363 operation
364 payload
365 decision
366 (constructor ProtocolDirection ProtocolSend)
367 identity
368 value
369 induction)))
370 (naturalEqual participant (regionTransferSender identity))))
371 (branch
372 GlobalProtocolRepeat
373 count
374 body
375 rest
376 bodyProjection
377 restProjection
378 .
379 (nat-eliminate
380 (lambda unrestricted flag : Nat .
381 (family ParticipantProtocol operation payload decision))
382 restProjection
383 (lambda unrestricted prior : Nat .
384 (lambda unrestricted ignored : (family ParticipantProtocol operation payload decision) .
385 (constructor
386 ParticipantProtocol
387 ParticipantProtocolRepeat
388 operation
389 payload
390 decision
391 count
392 bodyProjection
393 restProjection)))
394 (naturalMultiply
395 count
396 (naturalEqual
397 (participantProtocolEmpty operation payload decision bodyProjection)
398 0))))
399 (branch
400 GlobalProtocolChoice
401 identity
402 selector
403 announcements
404 zeroBody
405 oneBody
406 rest
407 zeroProjection
408 oneProjection
409 restProjection
410 .
411 (let unrestricted projectedAnnouncements =
412 (projectProtocolAnnouncements payload participant announcements)
413 in
414 (nat-eliminate
415 (lambda unrestricted flag : Nat .
416 (family ParticipantProtocol operation payload decision))
417 (constructor
418 ParticipantProtocol
419 ParticipantProtocolChoice
420 operation
421 payload
422 decision
423 participant
424 identity
425 selector
426 projectedAnnouncements
427 zeroProjection
428 oneProjection
429 restProjection)
430 (lambda unrestricted prior : Nat .
431 (lambda unrestricted ignored : (family ParticipantProtocol operation payload decision) .
432 restProjection))
433 (naturalAnd
434 (protocolAnnouncementsEmpty payload projectedAnnouncements)
435 (naturalAnd
436 (participantProtocolEmpty operation payload decision zeroProjection)
437 (participantProtocolEmpty operation payload decision oneProjection))))))))))))
438
439def planParticipantProtocol =
440 (lambda erased operation : Type 0 .
441 (lambda erased payload : Type 0 .
442 (lambda erased decision : Type 0 .
443 (lambda unrestricted participants : Nat .
444 (lambda unrestricted participant : Nat .
445 (lambda unrestricted local : (pi unrestricted owner : Nat . (pi unrestricted value : operation . Nat)) .
446 (lambda unrestricted transfer : (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . Nat)) .
447 (lambda unrestricted choice : (pi unrestricted owner : Nat . (pi unrestricted selector : decision . (pi unrestricted announcements : (family ProtocolAnnouncements payload) . Nat))) .
448 (lambda unrestricted program : (family GlobalProtocol operation payload decision) .
449 (eliminate
450 StdResult
451 (lambda unrestricted current : (family StdResult (family ProtocolFailure) Nat) .
452 (family
453 StdResult
454 (family ProtocolFailure)
455 (family ParticipantProtocol operation payload decision)))
456 (protocolRequire
457 (naturalLess participant participants)
458 (constructor ProtocolFailure ProtocolParticipantBounds)
459 (checkGlobalProtocol
460 operation
461 payload
462 decision
463 participants
464 local
465 transfer
466 choice
467 program))
468 (branch
469 StdFailure
470 error
471 .
472 (constructor
473 StdResult
474 StdFailure
475 (family ProtocolFailure)
476 (family ParticipantProtocol operation payload decision)
477 error))
478 (branch
479 StdSuccess
480 accepted
481 .
482 (constructor
483 StdResult
484 StdSuccess
485 (family ProtocolFailure)
486 (family ParticipantProtocol operation payload decision)
487 (projectGlobalProtocol operation payload decision participant program)))))))))))))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.