Receive each child's commitment over its edge and record it after checking
the capture prefix and that it covers exactly the prescribed subtree.
585def nativeTreeReceiveChildren =
586 (lambda unrestricted plan : (family NativeTreeCheckpoint) .
587 (lambda unrestricted fanout : Nat .
588 (lambda unrestricted node : (family ParticipantTreeNode) .
589 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
590 (lambda unrestricted commitment : (pi unrestricted child : Nat . (family RegionFrameLayout)) .
591 (lambda unrestricted stateAt : Nat .
592 (lambda unrestricted agreed : Nat .
593 (lambda unrestricted epoch : (family NativePhysicalOperand) .
594 (lambda unrestricted version : (family NativePhysicalOperand) .
595 (lambda unrestricted tail : (family NativePhysicalCommands) .
596 (let unrestricted own =
597 (stdListLength (family NativeRegionShard) (nativeTreeShards plan))
598 in
599 (stdListFold
600 (family ParticipantTreeNode)
601 (pi unrestricted index : Nat . (family NativePhysicalCommands))
602 (lambda unrestricted child : (family ParticipantTreeNode) .
603 (lambda unrestricted next : (pi unrestricted index : Nat . (family NativePhysicalCommands)) .
604 (lambda unrestricted index : Nat .
605 (let unrestricted role =
606 (participantTreeRoleOf child)
607 in
608 (let unrestricted frame =
609 (commitment role)
610 in
611 (let unrestricted record =
612 (naturalAdd own index)
613 in
614 (nativeFrameInitializeRound
615 frame
616 epoch
617 version
618 (nativePeerPublicationIO
619 (nativeLaunchRecipeSlotValue
620 (nativePeerEdgeConnectionTo edges role))
621 0
622 frame
623 (nativeFrameConsume
624 frame
625 (nativeMemoryCompareRegions
626 stateAt
627 (framePayloadAt frame)
628 agreed
629 nativePeerScratchSlot
630 b"tree-child-position"
631 (nativeMemoryCopyPayload
632 (nativeTreeRecordAt (nativeTreeGroup plan) record)
633 (nativeTreeChildDescriptor
634 role
635 (participantTreeSizeOf child))
636 (nativeMemoryCompareRegions
637 (nativeTreeRecordAt (nativeTreeGroup plan) record)
638 (naturalAdd (framePayloadAt frame) agreed)
639 nativeRegionDescriptorBytes
640 nativePeerScratchSlot
641 b"tree-child-coverage"
642 (nativeMemoryCopyOperands
643 (nativeMemoryState
644 (nativeTreeRecordDigestAt (nativeTreeGroup plan) record))
645 (nativeMemoryState
646 (naturalAdd
647 (framePayloadAt frame)
648 (naturalAdd agreed nativeRegionDescriptorBytes)))
649 checkpointEnvelopeDigestBytes
650 nativePeerScratchSlot
651 b"tree-child-record"
652 (next (succ index)))))))))))))))
653 (lambda unrestricted index : Nat . tail)
654 (participantTreeChildren fanout node)
655 0))))))))))))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.