589def nativePhysicalValidateOperation =
590 (lambda unrestricted operation : (family NativePhysicalOperation) .
591 (eliminate
592 NativePhysicalOperation
593 (lambda unrestricted current : (family NativePhysicalOperation) .
594 (family NativePhysicalOperationValidation))
595 operation
596 (branch
597 NativePhysicalSystemCall
598 number
599 arguments
600 payload
601 result
602 .
603 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
604 (branch
605 NativePhysicalCopyPayloadToState
606 destination
607 extent
608 payload
609 .
610 (eliminate
611 NativePhysicalOperationValidation
612 (lambda unrestricted current : (family NativePhysicalOperationValidation) .
613 (family NativePhysicalOperationValidation))
614 (nativePhysicalRequireBytes
615 payload
616 (constructor NativePhysicalErrorCode NativePhysicalCopyPayloadEmpty))
617 (branch
618 NativePhysicalOperationValid
619 .
620 (nat-eliminate
621 (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
622 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)
623 (lambda unrestricted predecessor : Nat .
624 (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
625 (constructor
626 NativePhysicalOperationValidation
627 NativePhysicalOperationInvalid
628 (constructor NativePhysicalErrorCode NativePhysicalCopyExtentZero))))
629 (modelWord64IsZero extent)))
630 (branch
631 NativePhysicalOperationInvalid
632 error
633 .
634 (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid error))))
635 (branch
636 NativePhysicalMachineRoutine
637 code
638 arguments
639 result
640 .
641 (nativePhysicalRequireBytes
642 code
643 (constructor NativePhysicalErrorCode NativePhysicalMachineCodeEmpty)))
644 (branch
645 NativePhysicalFencePoll
646 address
647 expected
648 maximumPolls
649 .
650 (nat-eliminate
651 (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
652 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)
653 (lambda unrestricted predecessor : Nat .
654 (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
655 (constructor
656 NativePhysicalOperationValidation
657 NativePhysicalOperationInvalid
658 (constructor NativePhysicalErrorCode NativePhysicalFencePollCountZero))))
659 (modelWord64IsZero maximumPolls)))
660 (branch
661 NativePhysicalTelemetryAppend
662 path
663 record
664 .
665 (eliminate
666 NativePhysicalOperationValidation
667 (lambda unrestricted current : (family NativePhysicalOperationValidation) .
668 (family NativePhysicalOperationValidation))
669 (nativePhysicalRequireBytes
670 path
671 (constructor NativePhysicalErrorCode NativePhysicalTelemetryPathEmpty))
672 (branch
673 NativePhysicalOperationValid
674 .
675 (nativePhysicalRequireBytes
676 record
677 (constructor NativePhysicalErrorCode NativePhysicalTelemetryRecordEmpty)))
678 (branch
679 NativePhysicalOperationInvalid
680 error
681 .
682 (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid error))))
683 (branch
684 NativePhysicalAssertEqual
685 left
686 right
687 error
688 .
689 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
690 (branch
691 NativePhysicalAssertOneOf
692 observed
693 first
694 second
695 error
696 .
697 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
698 (branch
699 NativePhysicalHaltSuccess
700 .
701 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
702 (branch
703 NativePhysicalRepeatBegin
704 count
705 .
706 (nat-eliminate
707 (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
708 (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid
709 (constructor NativePhysicalErrorCode NativePhysicalRepeatCountZero))
710 (lambda unrestricted predecessor : Nat .
711 (lambda unrestricted induction : (family NativePhysicalOperationValidation) .
712 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)))
713 (naturalIsZero (modelWord64IsZero count))))
714 (branch
715 NativePhysicalRepeatEnd
716 .
717 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
718 (branch
719 NativePhysicalStoreWord64
720 destination
721 value
722 .
723 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
724 (branch
725 NativePhysicalFenceWait
726 address
727 expected
728 maximumPolls
729 interval
730 .
731 (nat-eliminate
732 (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
733 (nat-eliminate
734 (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
735 (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid
736 (constructor NativePhysicalErrorCode NativePhysicalFenceWaitIntervalInvalid))
737 (lambda unrestricted predecessor : Nat .
738 (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
739 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)))
740 (nativePhysicalFenceWaitIntervalValid interval))
741 (lambda unrestricted predecessor : Nat .
742 (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
743 (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid
744 (constructor NativePhysicalErrorCode NativePhysicalFenceWaitCountZero))))
745 (modelWord64IsZero maximumPolls)))
746 (branch NativePhysicalRepeatBeginCounted count .
747 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
748 (branch NativePhysicalAddWord64 destination left right .
749 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
750 (branch NativePhysicalFloat64 operation destination left right .
751 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))))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.