926def nativePhysicalValidateProgram =
927 (lambda unrestricted program : (family NativePhysicalProgram) .
928 (eliminate
929 NativePhysicalProgram
930 (lambda unrestricted current : (family NativePhysicalProgram) .
931 (family NativePhysicalProgramValidation))
932 program
933 (branch
934 NativePhysicalProgramValue
935 stateExtent
936 resultSlots
937 commands
938 expected
939 identity
940 fallbacks
941 .
942 (nat-eliminate
943 (lambda unrestricted current : Nat . (family NativePhysicalProgramValidation))
944 (nativePhysicalReject
945 program
946 (constructor NativePhysicalErrorCode NativePhysicalIdentityInvalid)
947 zero)
948 (lambda unrestricted identityPredecessor : Nat .
949 (lambda unrestricted ignoredIdentity : (family NativePhysicalProgramValidation) .
950 (nat-eliminate
951 (lambda unrestricted current : Nat . (family NativePhysicalProgramValidation))
952 (nativePhysicalReject
953 program
954 (constructor NativePhysicalErrorCode NativePhysicalFallbackObserved)
955 zero)
956 (lambda unrestricted fallbackPredecessor : Nat .
957 (lambda unrestricted ignoredFallback : (family NativePhysicalProgramValidation) .
958 (nat-eliminate
959 (lambda unrestricted current : Nat . (family NativePhysicalProgramValidation))
960 (eliminate
961 NativePhysicalCommandsValidation
962 (lambda unrestricted current : (family NativePhysicalCommandsValidation) .
963 (family NativePhysicalProgramValidation))
964 (nat-eliminate
965 (lambda unrestricted current : Nat . (family NativePhysicalCommandsValidation))
966 (nativePhysicalValidateCommands commands)
967 (lambda unrestricted predecessor : Nat .
968 (lambda unrestricted ignoredBalance : (family NativePhysicalCommandsValidation) .
969 (constructor NativePhysicalCommandsValidation NativePhysicalCommandsInvalid
970 (constructor NativePhysicalErrorCode NativePhysicalRepeatUnbalanced)
971 zero)))
972 (nativePhysicalRepeatBalance commands))
973 (branch
974 NativePhysicalCommandsValid
975 completed
976 .
977 (nat-eliminate
978 (lambda unrestricted current : Nat .
979 (family NativePhysicalProgramValidation))
980 (nativePhysicalReject
981 program
982 (constructor
983 NativePhysicalErrorCode
984 NativePhysicalCommandCountMismatch)
985 zero)
986 (lambda unrestricted countPredecessor : Nat .
987 (lambda unrestricted ignoredCount : (family NativePhysicalProgramValidation) .
988 (constructor
989 NativePhysicalProgramValidation
990 NativePhysicalProgramValidated
991 program
992 (nativePhysicalValidationTelemetryFor program zero zero b""))))
993 (naturalEqual completed expected)))
994 (branch
995 NativePhysicalCommandsInvalid
996 error
997 ordinal
998 .
999 (nativePhysicalReject program error ordinal)))
1000 (lambda unrestricted statePredecessor : Nat .
1001 (lambda unrestricted ignoredState : (family NativePhysicalProgramValidation) .
1002 (nativePhysicalReject
1003 program
1004 (constructor NativePhysicalErrorCode NativePhysicalStateExtentZero)
1005 zero)))
1006 (modelWord64IsZero stateExtent))))
1007 (naturalEqual fallbacks zero))))
1008 (naturalEqual (bytes-length identity) (byte-to-nat (byte 64)))))))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.