Runtime.NativePhysicalProgram

1008def nativePhysicalValidateOperation =
1009  (lambda unrestricted rest : (family NativePhysicalCommands) .
1010    (lambda unrestricted operation : (family NativePhysicalOperation) .
1011      (eliminate
1012        NativePhysicalOperation
1013        (lambda unrestricted current : (family NativePhysicalOperation) .
1014          (family NativePhysicalOperationValidation))
1015        operation
1016        (branch
1017          NativePhysicalSystemCall
1018          number
1019          arguments
1020          payload
1021          result
1022          .
1023          (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1024        (branch
1025          NativePhysicalCopyPayloadToState
1026          destination
1027          extent
1028          payload
1029          .
1030          (eliminate
1031            NativePhysicalOperationValidation
1032            (lambda unrestricted current : (family NativePhysicalOperationValidation) .
1033              (family NativePhysicalOperationValidation))
1034            (nativePhysicalRequireBytes
1035              payload
1036              (constructor NativePhysicalErrorCode NativePhysicalCopyPayloadEmpty))
1037            (branch
1038              NativePhysicalOperationValid
1039              .
1040              (nat-eliminate
1041                (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
1042                (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)
1043                (lambda unrestricted predecessor : Nat .
1044                  (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
1045                    (constructor
1046                      NativePhysicalOperationValidation
1047                      NativePhysicalOperationInvalid
1048                      (constructor NativePhysicalErrorCode NativePhysicalCopyExtentZero))))
1049                (modelWord64IsZero extent)))
1050            (branch
1051              NativePhysicalOperationInvalid
1052              error
1053              .
1054              (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid error))))
1055        (branch
1056          NativePhysicalMachineRoutine
1057          code
1058          arguments
1059          result
1060          .
1061          (nativePhysicalRequireBytes
1062            code
1063            (constructor NativePhysicalErrorCode NativePhysicalMachineCodeEmpty)))
1064        (branch
1065          NativePhysicalFencePoll
1066          address
1067          expected
1068          maximumPolls
1069          .
1070          (nat-eliminate
1071            (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
1072            (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)
1073            (lambda unrestricted predecessor : Nat .
1074              (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
1075                (constructor
1076                  NativePhysicalOperationValidation
1077                  NativePhysicalOperationInvalid
1078                  (constructor NativePhysicalErrorCode NativePhysicalFencePollCountZero))))
1079            (modelWord64IsZero maximumPolls)))
1080        (branch
1081          NativePhysicalTelemetryAppend
1082          path
1083          record
1084          .
1085          (eliminate
1086            NativePhysicalOperationValidation
1087            (lambda unrestricted current : (family NativePhysicalOperationValidation) .
1088              (family NativePhysicalOperationValidation))
1089            (nativePhysicalRequireBytes
1090              path
1091              (constructor NativePhysicalErrorCode NativePhysicalTelemetryPathEmpty))
1092            (branch
1093              NativePhysicalOperationValid
1094              .
1095              (nativePhysicalRequireBytes
1096                record
1097                (constructor NativePhysicalErrorCode NativePhysicalTelemetryRecordEmpty)))
1098            (branch
1099              NativePhysicalOperationInvalid
1100              error
1101              .
1102              (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid error))))
1103        (branch
1104          NativePhysicalAssertEqual
1105          left
1106          right
1107          error
1108          .
1109          (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1110        (branch
1111          NativePhysicalAssertOneOf
1112          observed
1113          first
1114          second
1115          error
1116          .
1117          (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1118        (branch
1119          NativePhysicalHaltSuccess
1120          .
1121          (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1122        (branch
1123          NativePhysicalRepeatBegin
1124          count
1125          .
1126          (nat-eliminate
1127            (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
1128            (constructor
1129              NativePhysicalOperationValidation
1130              NativePhysicalOperationInvalid
1131              (constructor NativePhysicalErrorCode NativePhysicalRepeatCountZero))
1132            (lambda unrestricted predecessor : Nat .
1133              (lambda unrestricted induction : (family NativePhysicalOperationValidation) .
1134                (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)))
1135            (naturalIsZero (modelWord64IsZero count))))
1136        (branch
1137          NativePhysicalSkipUnlessEqual
1138          left
1139          right
1140          count
1141          .
1142          (nat-eliminate
1143            (lambda unrestricted valid : Nat . (family NativePhysicalOperationValidation))
1144            (constructor
1145              NativePhysicalOperationValidation
1146              NativePhysicalOperationInvalid
1147              (constructor NativePhysicalErrorCode NativePhysicalBranchTargetInvalid))
1148            (lambda unrestricted previous : Nat .
1149              (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
1150                (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)))
1151            (nativePhysicalBranchWindowValid count rest)))
1152        (branch
1153          NativePhysicalRepeatEnd
1154          .
1155          (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1156        (branch
1157          NativePhysicalRepeatEndWhen
1158          observed
1159          expected
1160          .
1161          (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1162        (branch
1163          NativePhysicalStoreWord64
1164          destination
1165          value
1166          .
1167          (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1168        (branch
1169          NativePhysicalFenceWait
1170          address
1171          expected
1172          maximumPolls
1173          interval
1174          .
1175          (nat-eliminate
1176            (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
1177            (nat-eliminate
1178              (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
1179              (constructor
1180                NativePhysicalOperationValidation
1181                NativePhysicalOperationInvalid
1182                (constructor NativePhysicalErrorCode NativePhysicalFenceWaitIntervalInvalid))
1183              (lambda unrestricted predecessor : Nat .
1184                (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
1185                  (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)))
1186              (nativePhysicalFenceWaitIntervalValid interval))
1187            (lambda unrestricted predecessor : Nat .
1188              (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
1189                (constructor
1190                  NativePhysicalOperationValidation
1191                  NativePhysicalOperationInvalid
1192                  (constructor NativePhysicalErrorCode NativePhysicalFenceWaitCountZero))))
1193            (modelWord64IsZero maximumPolls)))
1194        (branch
1195          NativePhysicalRepeatBeginCounted
1196          count
1197          .
1198          (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1199        (branch
1200          NativePhysicalAddWord64
1201          destination
1202          left
1203          right
1204          .
1205          (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1206        (branch
1207          NativePhysicalFloat64
1208          operation
1209          destination
1210          left
1211          right
1212          .
1213          (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)))))