Runtime.NativePhysicalProgram

876def nativePhysicalValidateOperation =
877  (lambda unrestricted rest : (family NativePhysicalCommands) .
878    (lambda unrestricted operation : (family NativePhysicalOperation) .
879      (eliminate
880        NativePhysicalOperation
881        (lambda unrestricted current : (family NativePhysicalOperation) .
882          (family NativePhysicalOperationValidation))
883        operation
884        (branch
885          NativePhysicalSystemCall
886          number
887          arguments
888          payload
889          result
890          .
891          (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
892        (branch
893          NativePhysicalCopyPayloadToState
894          destination
895          extent
896          payload
897          .
898          (eliminate
899            NativePhysicalOperationValidation
900            (lambda unrestricted current : (family NativePhysicalOperationValidation) .
901              (family NativePhysicalOperationValidation))
902            (nativePhysicalRequireBytes
903              payload
904              (constructor NativePhysicalErrorCode NativePhysicalCopyPayloadEmpty))
905            (branch
906              NativePhysicalOperationValid
907              .
908              (nat-eliminate
909                (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
910                (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)
911                (lambda unrestricted predecessor : Nat .
912                  (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
913                    (constructor
914                      NativePhysicalOperationValidation
915                      NativePhysicalOperationInvalid
916                      (constructor NativePhysicalErrorCode NativePhysicalCopyExtentZero))))
917                (modelWord64IsZero extent)))
918            (branch
919              NativePhysicalOperationInvalid
920              error
921              .
922              (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid error))))
923        (branch
924          NativePhysicalMachineRoutine
925          code
926          arguments
927          result
928          .
929          (nativePhysicalRequireBytes
930            code
931            (constructor NativePhysicalErrorCode NativePhysicalMachineCodeEmpty)))
932        (branch
933          NativePhysicalFencePoll
934          address
935          expected
936          maximumPolls
937          .
938          (nat-eliminate
939            (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
940            (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)
941            (lambda unrestricted predecessor : Nat .
942              (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
943                (constructor
944                  NativePhysicalOperationValidation
945                  NativePhysicalOperationInvalid
946                  (constructor NativePhysicalErrorCode NativePhysicalFencePollCountZero))))
947            (modelWord64IsZero maximumPolls)))
948        (branch
949          NativePhysicalTelemetryAppend
950          path
951          record
952          .
953          (eliminate
954            NativePhysicalOperationValidation
955            (lambda unrestricted current : (family NativePhysicalOperationValidation) .
956              (family NativePhysicalOperationValidation))
957            (nativePhysicalRequireBytes
958              path
959              (constructor NativePhysicalErrorCode NativePhysicalTelemetryPathEmpty))
960            (branch
961              NativePhysicalOperationValid
962              .
963              (nativePhysicalRequireBytes
964                record
965                (constructor NativePhysicalErrorCode NativePhysicalTelemetryRecordEmpty)))
966            (branch
967              NativePhysicalOperationInvalid
968              error
969              .
970              (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid error))))
971        (branch
972          NativePhysicalAssertEqual
973          left
974          right
975          error
976          .
977          (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
978        (branch
979          NativePhysicalAssertOneOf
980          observed
981          first
982          second
983          error
984          .
985          (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
986        (branch
987          NativePhysicalHaltSuccess
988          .
989          (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
990        (branch
991          NativePhysicalRepeatBegin
992          count
993          .
994          (nat-eliminate
995            (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
996            (constructor
997              NativePhysicalOperationValidation
998              NativePhysicalOperationInvalid
999              (constructor NativePhysicalErrorCode NativePhysicalRepeatCountZero))
1000            (lambda unrestricted predecessor : Nat .
1001              (lambda unrestricted induction : (family NativePhysicalOperationValidation) .
1002                (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)))
1003            (naturalIsZero (modelWord64IsZero count))))
1004        (branch
1005          NativePhysicalSkipUnlessEqual
1006          left
1007          right
1008          count
1009          .
1010          (nat-eliminate
1011            (lambda unrestricted valid : Nat . (family NativePhysicalOperationValidation))
1012            (constructor
1013              NativePhysicalOperationValidation
1014              NativePhysicalOperationInvalid
1015              (constructor NativePhysicalErrorCode NativePhysicalBranchTargetInvalid))
1016            (lambda unrestricted previous : Nat .
1017              (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
1018                (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)))
1019            (nativePhysicalBranchWindowValid count rest)))
1020        (branch
1021          NativePhysicalRepeatEnd
1022          .
1023          (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1024        (branch
1025          NativePhysicalRepeatEndWhen
1026          observed
1027          expected
1028          .
1029          (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1030        (branch
1031          NativePhysicalStoreWord64
1032          destination
1033          value
1034          .
1035          (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1036        (branch
1037          NativePhysicalFenceWait
1038          address
1039          expected
1040          maximumPolls
1041          interval
1042          .
1043          (nat-eliminate
1044            (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
1045            (nat-eliminate
1046              (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
1047              (constructor
1048                NativePhysicalOperationValidation
1049                NativePhysicalOperationInvalid
1050                (constructor NativePhysicalErrorCode NativePhysicalFenceWaitIntervalInvalid))
1051              (lambda unrestricted predecessor : Nat .
1052                (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
1053                  (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)))
1054              (nativePhysicalFenceWaitIntervalValid interval))
1055            (lambda unrestricted predecessor : Nat .
1056              (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
1057                (constructor
1058                  NativePhysicalOperationValidation
1059                  NativePhysicalOperationInvalid
1060                  (constructor NativePhysicalErrorCode NativePhysicalFenceWaitCountZero))))
1061            (modelWord64IsZero maximumPolls)))
1062        (branch
1063          NativePhysicalRepeatBeginCounted
1064          count
1065          .
1066          (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1067        (branch
1068          NativePhysicalAddWord64
1069          destination
1070          left
1071          right
1072          .
1073          (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1074        (branch
1075          NativePhysicalFloat64
1076          operation
1077          destination
1078          left
1079          right
1080          .
1081          (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)))))