The requested ordered contribution set is checked independently of the tree.
This refuses missing/duplicated contributors before producing any participant.
578def planOrderedCombineAndDeliver =
579 (lambda erased payload : Type 0 .
580 (lambda unrestricted participants : Nat .
581 (lambda unrestricted members : (family CombineCoverage) .
582 (lambda unrestricted baseAnchor : (family RegionTransferIdentity) .
583 (lambda unrestricted binding : (pi unrestricted stage : (family CombineStage) . (pi unrestricted source : (family CombineReference) . (pi unrestricted destination : (family CombineReference) . (pi unrestricted identity : (family RegionTransferIdentity) . payload)))) .
584 (lambda unrestricted local : (pi unrestricted role : Nat . (pi unrestricted operation : (family OrderedCombineOperation payload) . Nat)) .
585 (lambda unrestricted transfer : (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . Nat)) .
586 (lambda unrestricted delivery : (family CombineDelivery) .
587 (lambda unrestricted tree : (family OrderedCombineTree) .
588 (lambda unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
589 (let unrestricted anchor =
590 (combineCoverageAnchor members baseAnchor)
591 in
592 (combineRequire
593 (family
594 GlobalProtocol
595 (family OrderedCombineOperation payload)
596 payload
597 (family ProtocolNoDecision))
598 (naturalAnd
599 (naturalNonzero participants)
600 (naturalLessOrEqual participants regionFrameWordLimit))
601 (constructor OrderedCombineFailure CombineMembershipBounds)
602 (combineRequire
603 (family
604 GlobalProtocol
605 (family OrderedCombineOperation payload)
606 payload
607 (family ProtocolNoDecision))
608 (combineOwnersValid participants tree)
609 (constructor OrderedCombineFailure CombineOwnerOutsideChildren)
610 (combineRequire
611 (family
612 GlobalProtocol
613 (family OrderedCombineOperation payload)
614 payload
615 (family ProtocolNoDecision))
616 (combineDistinct (combineLeaves tree))
617 (constructor OrderedCombineFailure CombineDuplicateLeaf)
618 (combineRequire
619 (family
620 GlobalProtocol
621 (family OrderedCombineOperation payload)
622 payload
623 (family ProtocolNoDecision))
624 (combineCoverageValid participants members (combineLeaves tree))
625 (constructor OrderedCombineFailure CombineCoverageMismatch)
626 (combineRequire
627 (family
628 GlobalProtocol
629 (family OrderedCombineOperation payload)
630 payload
631 (family ProtocolNoDecision))
632 (combineDeliveryAdmitted delivery tree)
633 (constructor OrderedCombineFailure CombineCoverageMismatch)
634 (combineRequire
635 (family
636 GlobalProtocol
637 (family OrderedCombineOperation payload)
638 payload
639 (family ProtocolNoDecision))
640 (naturalLessOrEqual
641 (combineNodeCount tree)
642 (naturalDivideUnchecked regionFrameWordLimit 3))
643 (constructor OrderedCombineFailure CombineReferenceBounds)
644 (let unrestricted digest =
645 (combineTreeDigest tree)
646 in
647 (combineRequire
648 (family
649 GlobalProtocol
650 (family OrderedCombineOperation payload)
651 payload
652 (family ProtocolNoDecision))
653 (naturalEqual (bytes-length digest) 32)
654 (constructor
655 OrderedCombineFailure
656 CombineIdentityUnavailable)
657 (let unrestricted program =
658 (compileOrderedCombine
659 payload
660 anchor
661 digest
662 binding
663 tree
664 0
665 (compileTreeDelivery
666 payload
667 anchor
668 digest
669 binding
670 delivery
671 tree
672 0
673 tail))
674 in
675 (eliminate
676 StdResult
677 (lambda unrestricted current : (family StdResult (family ProtocolFailure) Nat) .
678 (family
679 StdResult
680 (family OrderedCombineFailure)
681 (family
682 GlobalProtocol
683 (family OrderedCombineOperation payload)
684 payload
685 (family ProtocolNoDecision))))
686 (checkGlobalProtocol
687 (family OrderedCombineOperation payload)
688 payload
689 (family ProtocolNoDecision)
690 participants
691 local
692 transfer
693 (protocolNoDecision payload)
694 program)
695 (branch
696 StdFailure
697 error
698 .
699 (constructor
700 StdResult
701 StdFailure
702 (family OrderedCombineFailure)
703 (family
704 GlobalProtocol
705 (family OrderedCombineOperation payload)
706 payload
707 (family ProtocolNoDecision))
708 (constructor
709 OrderedCombineFailure
710 CombineProtocolRefused
711 error)))
712 (branch
713 StdSuccess
714 value
715 .
716 (constructor
717 StdResult
718 StdSuccess
719 (family OrderedCombineFailure)
720 (family
721 GlobalProtocol
722 (family OrderedCombineOperation payload)
723 payload
724 (family ProtocolNoDecision))
725 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.