Exact round contracts still pass through checkGlobalProtocol: this
producer owns topology/order, not target admission or frame lifecycle.
380def orderedCombineAndReplicate =
381 (lambda erased payload : Type 0 .
382 (lambda unrestricted anchor : (family RegionTransferIdentity) .
383 (lambda unrestricted binding : (pi unrestricted stage : (family CombineStage) . (pi unrestricted source : (family CombineReference) . (pi unrestricted destination : (family CombineReference) . (pi unrestricted identity : (family RegionTransferIdentity) . payload)))) .
384 (lambda unrestricted tree : (family OrderedCombineTree) .
385 (lambda unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
386 (let unrestricted digest =
387 (combineTreeDigest tree)
388 in
389 (compileOrderedCombine
390 payload
391 anchor
392 digest
393 binding
394 tree
395 0
396 (compileTreeReplication payload anchor digest binding tree 0 tail))))))))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.