Lower admitted projections only. Callbacks may realize local computation or
declared transfers but cannot introduce hidden network dependencies. The
selector is evaluated once by the authority before any outgoing announcement.
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))))))))))))))))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.