Runtime.NativeProtocol

1module Runtime.NativeProtocol
2
3import Runtime.Protocol
4import Runtime.RegionTransfer
5import Runtime.RegionFrame
6import Compiler.Planning.RegionFrame
7import Runtime.NativeBranch
8import Runtime.NativeRegionFrame
9import Runtime.NativeMemoryPlan
10import Runtime.NativePhysicalProgram
11import Runtime.NativeLaunchRecipeLoad
12import Std.Foundation
13import Std.Natural
14
15-- The predicate and its scratch word are separate from frame storage. Only
16-- the authority evaluates the selector. Followers install the validated wire
17-- word, and forwarding participants publish that exact installed value.
18family NativeProtocolDecisionBinding : Type 0
19parameter erased nativeDecisionSelector : Type 0
20parameter erased nativeDecisionPayload : Type 0
21constructor NativeProtocolDecisionBindingOf
22field unrestricted nativeDecisionSource : (pi unrestricted selector : nativeDecisionSelector . (family NativePhysicalOperand))
23field unrestricted nativeDecisionState : (pi unrestricted selector : nativeDecisionSelector . Nat)
24field unrestricted nativeDecisionScratchSlot : Nat
25field unrestricted nativeDecisionFrame : (pi unrestricted value : nativeDecisionPayload . (family RegionFrameLayout))
26
27end-family
28
29-- A transfer binding must reproduce the canonical route, identity and extent
30-- from the global protocol. A matching local buffer size alone is insufficient.
31def nativeProtocolFrameAdmitted =
32  (lambda unrestricted identity : (family RegionTransferIdentity) .
33    (lambda unrestricted layout : (family RegionFrameLayout) .
34      (eliminate
35        StdResult
36        (lambda unrestricted result : (family StdResult (family RegionFrameFailure) Bytes) . Nat)
37        (regionFrameHeader identity (framePayloadBytes layout) (bytes-length (frameHeader layout)))
38        (branch StdFailure error . 0)
39        (branch StdSuccess header . (bytes-equal header (frameHeader layout))))))
40
41def nativeProtocolDecisionSource =
42  (lambda erased decision : Type 0 .
43    (lambda erased payload : Type 0 .
44      (lambda unrestricted binding : (family NativeProtocolDecisionBinding decision payload) .
45        (eliminate
46          NativeProtocolDecisionBinding
47          (lambda unrestricted current : (family NativeProtocolDecisionBinding decision payload) .
48            (pi unrestricted selector : decision . (family NativePhysicalOperand)))
49          binding
50          (branch NativeProtocolDecisionBindingOf source state scratch frame . source)))))
51
52def nativeProtocolDecisionState =
53  (lambda erased decision : Type 0 .
54    (lambda erased payload : Type 0 .
55      (lambda unrestricted binding : (family NativeProtocolDecisionBinding decision payload) .
56        (eliminate
57          NativeProtocolDecisionBinding
58          (lambda unrestricted current : (family NativeProtocolDecisionBinding decision payload) .
59            (pi unrestricted selector : decision . Nat))
60          binding
61          (branch NativeProtocolDecisionBindingOf source state scratch frame . state)))))
62
63def nativeProtocolDecisionScratch =
64  (lambda erased decision : Type 0 .
65    (lambda erased payload : Type 0 .
66      (lambda unrestricted binding : (family NativeProtocolDecisionBinding decision payload) .
67        (eliminate
68          NativeProtocolDecisionBinding
69          (lambda unrestricted current : (family NativeProtocolDecisionBinding decision payload) .
70            Nat)
71          binding
72          (branch NativeProtocolDecisionBindingOf source state scratch frame . scratch)))))
73
74def nativeProtocolDecisionFrame =
75  (lambda erased decision : Type 0 .
76    (lambda erased payload : Type 0 .
77      (lambda unrestricted binding : (family NativeProtocolDecisionBinding decision payload) .
78        (eliminate
79          NativeProtocolDecisionBinding
80          (lambda unrestricted current : (family NativeProtocolDecisionBinding decision payload) .
81            (pi unrestricted value : payload . (family RegionFrameLayout)))
82          binding
83          (branch NativeProtocolDecisionBindingOf source state scratch frame . frame)))))
84
85def nativeProtocolNoFrameDecisions =
86  (constructor
87    NativeProtocolDecisionBinding
88    NativeProtocolDecisionBindingOf
89    (family ProtocolNoDecision)
90    (family RegionFrameLayout)
91    (lambda unrestricted selector : (family ProtocolNoDecision) .
92      (eliminate
93        ProtocolNoDecision
94        (lambda unrestricted current : (family ProtocolNoDecision) . (family NativePhysicalOperand))
95        selector))
96    (lambda unrestricted selector : (family ProtocolNoDecision) .
97      (eliminate
98        ProtocolNoDecision
99        (lambda unrestricted current : (family ProtocolNoDecision) . Nat)
100        selector))
101    0
102    (lambda unrestricted frame : (family RegionFrameLayout) . frame))
103
104-- The choice payload is a single canonical word. Admission checks every
105-- declared announcement binding before either participant artifact is emitted.
106-- The decision word must be disjoint from frame storage: framing/hash work may
107-- overwrite its scratch/header bytes while an authority is still forwarding.
108-- The complete host arena and result-slot capacities remain outer admission facts.
109def nativeProtocolDecisionAdmitted =
110  (lambda erased decision : Type 0 .
111    (lambda erased payload : Type 0 .
112      (lambda unrestricted binding : (family NativeProtocolDecisionBinding decision payload) .
113        (lambda unrestricted owner : Nat .
114          (lambda unrestricted selector : decision .
115            (lambda unrestricted announcements : (family ProtocolAnnouncements payload) .
116              (let unrestricted state =
117                (nativeProtocolDecisionState decision payload binding selector)
118                in
119                (let unrestricted wordBytes =
120                  (bytes-length (regionFrameWord 0))
121                  in
122                  (naturalAnd
123                    (naturalLessOrEqual
124                      state
125                      (naturalSaturatingSubtract regionFrameWordLimit wordBytes))
126                    (eliminate
127                      ProtocolAnnouncements
128                      (lambda unrestricted current : (family ProtocolAnnouncements payload) . Nat)
129                      announcements
130                      (branch ProtocolAnnouncementsEnd . 1)
131                      (branch
132                        ProtocolAnnouncementsNext
133                        identity
134                        value
135                        rest
136                        induction
137                        .
138                        (let unrestricted frame =
139                          (nativeProtocolDecisionFrame decision payload binding value)
140                          in
141                          (naturalAnd
142                            (nativeProtocolFrameAdmitted identity frame)
143                            (naturalAnd
144                              (naturalEqual (framePayloadBytes frame) wordBytes)
145                              (naturalAnd
146                                (naturalOr
147                                  (naturalLessOrEqual
148                                    (naturalAdd state wordBytes)
149                                    (frameBase frame))
150                                  (naturalLessOrEqual (frameEnd frame) state))
151                                (naturalAnd induction 1))))))))))))))))
152
153def nativeProtocolRequireDecision =
154  (lambda unrestricted value : (family NativePhysicalOperand) .
155    (lambda unrestricted label : Bytes .
156      (lambda unrestricted tail : (family NativePhysicalCommands) .
157        (nativeLaunchRecipeCommand
158          (constructor
159            NativePhysicalOperation
160            NativePhysicalAssertOneOf
161            value
162            (nativeLaunchRecipeImmediate 0)
163            (nativeLaunchRecipeImmediate 1)
164            (constructor NativePhysicalErrorCode NativePhysicalExecutionAssertionFailed))
165          label
166          tail))))
167
168-- A received frame is consumed before its value can control local work. A
169-- forwarder reuses that installed value, never its own selector. Each edge
170-- advances its own invocation version, so repeats and nested choices retain
171-- replay protection without introducing another native repeat frame.
172def nativeProtocolAnnouncements =
173  (lambda erased decision : Type 0 .
174    (lambda erased payload : Type 0 .
175      (lambda unrestricted binding : (family NativeProtocolDecisionBinding decision payload) .
176        (lambda unrestricted selector : decision .
177          (lambda unrestricted role : Nat .
178            (lambda unrestricted transfer : (pi unrestricted direction : (family ProtocolDirection) . (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))))) .
179              (lambda unrestricted label : Bytes .
180                (lambda unrestricted announcements : (family ProtocolAnnouncements payload) .
181                  (eliminate
182                    ProtocolAnnouncements
183                    (lambda unrestricted current : (family ProtocolAnnouncements payload) .
184                      (pi unrestricted tail : (family NativePhysicalCommands) .
185                        (family NativePhysicalCommands)))
186                    announcements
187                    (branch
188                      ProtocolAnnouncementsEnd
189                      .
190                      (lambda unrestricted tail : (family NativePhysicalCommands) . tail))
191                    (branch
192                      ProtocolAnnouncementsNext
193                      identity
194                      value
195                      rest
196                      induction
197                      .
198                      (lambda unrestricted tail : (family NativePhysicalCommands) .
199                        (let unrestricted frame =
200                          (nativeProtocolDecisionFrame decision payload binding value)
201                          in
202                          (let unrestricted state =
203                            (nativeProtocolDecisionState decision payload binding selector)
204                            in
205                            (nat-eliminate
206                              (lambda unrestricted flag : Nat . (family NativePhysicalCommands))
207                              (transfer
208                                (constructor ProtocolDirection ProtocolReceive)
209                                identity
210                                value
211                                (nativeFrameConsume
212                                  frame
213                                  (nativeMemoryStoreWord64
214                                    label
215                                    state
216                                    (nativeMemoryLoad (framePayloadAt frame))
217                                    (nativeProtocolRequireDecision
218                                      (nativeMemoryLoad state)
219                                      label
220                                      (nativeFrameAdvance
221                                        frame
222                                        (constructor NativeFrameTerminal NativeFrameConsumeComplete)
223                                        (nativeProtocolDecisionScratch decision payload binding)
224                                        (induction tail))))))
225                              (lambda unrestricted prior : Nat .
226                                (lambda unrestricted ignored : (family NativePhysicalCommands) .
227                                  (nativeMemoryStoreWord64
228                                    label
229                                    (framePayloadAt frame)
230                                    (nativeMemoryLoad state)
231                                    (transfer
232                                      (constructor ProtocolDirection ProtocolSend)
233                                      identity
234                                      value
235                                      (nativeFrameAdvance
236                                        frame
237                                        (constructor NativeFrameTerminal NativeFrameSendComplete)
238                                        (nativeProtocolDecisionScratch decision payload binding)
239                                        (induction tail))))))
240                              (naturalEqual role (regionTransferSender identity))))))))))))))))
241
242-- Lower admitted projections only. Callbacks may realize local computation or
243-- declared transfers but cannot introduce hidden network dependencies. The
244-- selector is evaluated once by the authority before any outgoing announcement.
245-- Native repeat admission remains the shared encoder's responsibility.
246def nativeProtocolCommands =
247  (lambda erased operation : Type 0 .
248    (lambda erased payload : Type 0 .
249      (lambda erased decision : Type 0 .
250        (lambda unrestricted local : (pi unrestricted value : operation . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))) .
251          (lambda unrestricted transfer : (pi unrestricted direction : (family ProtocolDirection) . (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))))) .
252            (lambda unrestricted binding : (family NativeProtocolDecisionBinding decision payload) .
253              (lambda unrestricted label : Bytes .
254                (lambda unrestricted program : (family ParticipantProtocol operation payload decision) .
255                  (eliminate
256                    ParticipantProtocol
257                    (lambda unrestricted current : (family ParticipantProtocol operation payload decision) .
258                      (pi unrestricted tail : (family NativePhysicalCommands) .
259                        (family NativePhysicalCommands)))
260                    program
261                    (branch
262                      ParticipantProtocolEnd
263                      .
264                      (lambda unrestricted tail : (family NativePhysicalCommands) . tail))
265                    (branch
266                      ParticipantProtocolLocal
267                      value
268                      rest
269                      induction
270                      .
271                      (lambda unrestricted tail : (family NativePhysicalCommands) .
272                        (local value (induction tail))))
273                    (branch
274                      ParticipantProtocolTransfer
275                      direction
276                      identity
277                      value
278                      rest
279                      induction
280                      .
281                      (lambda unrestricted tail : (family NativePhysicalCommands) .
282                        (transfer direction identity value (induction tail))))
283                    (branch
284                      ParticipantProtocolRepeat
285                      count
286                      body
287                      rest
288                      bodyLowering
289                      restLowering
290                      .
291                      (lambda unrestricted tail : (family NativePhysicalCommands) .
292                        (nat-eliminate
293                          (lambda unrestricted flag : Nat . (family NativePhysicalCommands))
294                          (restLowering tail)
295                          (lambda unrestricted prior : Nat .
296                            (lambda unrestricted ignored : (family NativePhysicalCommands) .
297                              (nativeLaunchRecipeCommand
298                                (constructor
299                                  NativePhysicalOperation
300                                  NativePhysicalRepeatBeginCounted
301                                  (nativeLaunchRecipeImmediate count))
302                                (bytes-append label b":begin")
303                                (bodyLowering
304                                  (nativeLaunchRecipeCommand
305                                    (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
306                                    (bytes-append label b":end")
307                                    (restLowering tail))))))
308                          count)))
309                    (branch
310                      ParticipantProtocolChoice
311                      role
312                      identity
313                      selector
314                      announcements
315                      zeroBody
316                      oneBody
317                      rest
318                      zeroLowering
319                      oneLowering
320                      restLowering
321                      .
322                      (lambda unrestricted tail : (family NativePhysicalCommands) .
323                        (let unrestricted state =
324                          (nativeProtocolDecisionState decision payload binding selector)
325                          in
326                          (let unrestricted selected =
327                            (nativeProtocolAnnouncements
328                              decision
329                              payload
330                              binding
331                              selector
332                              role
333                              transfer
334                              label
335                              announcements
336                              (nativeIfEqual
337                                (nativeMemoryLoad state)
338                                (nativeLaunchRecipeImmediate 0)
339                                label
340                                (zeroLowering
341                                  (constructor NativePhysicalCommands NativePhysicalCommandsEnd))
342                                (oneLowering
343                                  (constructor NativePhysicalCommands NativePhysicalCommandsEnd))
344                                (restLowering tail)))
345                            in
346                            (nat-eliminate
347                              (lambda unrestricted flag : Nat . (family NativePhysicalCommands))
348                              selected
349                              (lambda unrestricted prior : Nat .
350                                (lambda unrestricted ignored : (family NativePhysicalCommands) .
351                                  (nativeMemoryStoreWord64
352                                    label
353                                    state
354                                    (nativeProtocolDecisionSource decision payload binding selector)
355                                    (nativeProtocolRequireDecision
356                                      (nativeMemoryLoad state)
357                                      label
358                                      selected))))
359                              (naturalEqual role (regionTransferSender identity))))))))))))))))
360
361-- Setup traverses every declared frame once per occurrence, without executing
362-- choices or repeat counts. The callback is for setup, not runtime advancement:
363-- an unselected branch has no completed transfer to rearm. Reinitializing an
364-- already live frame through this traversal is forbidden by the frame contract.
365def nativeProtocolFrames =
366  (lambda erased operation : Type 0 .
367    (lambda erased payload : Type 0 .
368      (lambda erased decision : Type 0 .
369        (lambda unrestricted transfer : (pi unrestricted direction : (family ProtocolDirection) . (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))))) .
370          (lambda unrestricted program : (family ParticipantProtocol operation payload decision) .
371            (eliminate
372              ParticipantProtocol
373              (lambda unrestricted current : (family ParticipantProtocol operation payload decision) .
374                (pi unrestricted tail : (family NativePhysicalCommands) .
375                  (family NativePhysicalCommands)))
376              program
377              (branch
378                ParticipantProtocolEnd
379                .
380                (lambda unrestricted tail : (family NativePhysicalCommands) . tail))
381              (branch ParticipantProtocolLocal value rest induction . induction)
382              (branch
383                ParticipantProtocolTransfer
384                direction
385                identity
386                value
387                rest
388                induction
389                .
390                (lambda unrestricted tail : (family NativePhysicalCommands) .
391                  (transfer direction identity value (induction tail))))
392              (branch
393                ParticipantProtocolRepeat
394                count
395                body
396                rest
397                bodyFrames
398                restFrames
399                .
400                (lambda unrestricted tail : (family NativePhysicalCommands) .
401                  (bodyFrames (restFrames tail))))
402              (branch
403                ParticipantProtocolChoice
404                role
405                identity
406                selector
407                announcements
408                zeroBody
409                oneBody
410                rest
411                zeroFrames
412                oneFrames
413                restFrames
414                .
415                (lambda unrestricted tail : (family NativePhysicalCommands) .
416                  (app
417                    (eliminate
418                      ProtocolAnnouncements
419                      (lambda unrestricted current : (family ProtocolAnnouncements payload) .
420                        (pi unrestricted tail : (family NativePhysicalCommands) .
421                          (family NativePhysicalCommands)))
422                      announcements
423                      (branch
424                        ProtocolAnnouncementsEnd
425                        .
426                        (lambda unrestricted tail : (family NativePhysicalCommands) . tail))
427                      (branch
428                        ProtocolAnnouncementsNext
429                        identity
430                        value
431                        rest
432                        induction
433                        .
434                        (lambda unrestricted tail : (family NativePhysicalCommands) .
435                          (transfer
436                            (nat-eliminate
437                              (lambda unrestricted flag : Nat . (family ProtocolDirection))
438                              (constructor ProtocolDirection ProtocolReceive)
439                              (lambda unrestricted prior : Nat .
440                                (lambda unrestricted ignored : (family ProtocolDirection) .
441                                  (constructor ProtocolDirection ProtocolSend)))
442                              (naturalEqual role (regionTransferSender identity)))
443                            identity
444                            value
445                            (induction tail)))))
446                    (zeroFrames (oneFrames (restFrames tail))))))))))))