module Runtime.NativePhysicalProgram import Model.Parameter import Model.Word32 import Runtime.NativeTelemetry import Std.Natural import Model.Word64 family NativePhysicalErrorCode : Type 0 constructor NativePhysicalIdentityInvalid constructor NativePhysicalFallbackObserved constructor NativePhysicalCommandCountMismatch constructor NativePhysicalStateExtentZero constructor NativePhysicalCopyPayloadEmpty constructor NativePhysicalCopyExtentZero constructor NativePhysicalMachineCodeEmpty constructor NativePhysicalFencePollCountZero constructor NativePhysicalTelemetryPathEmpty constructor NativePhysicalTelemetryRecordEmpty constructor NativePhysicalResultSlotUnavailable constructor NativePhysicalExecutionAssertionFailed constructor NativePhysicalRepeatCountZero constructor NativePhysicalRepeatUnbalanced constructor NativePhysicalFenceWaitCountZero constructor NativePhysicalFenceWaitIntervalInvalid end-family family NativePhysicalSlot : Type 0 constructor NativePhysicalSlotValue field unrestricted nativePhysicalSlotIndex : (family ModelWord64) end-family family NativePhysicalOperand : Type 0 constructor NativePhysicalImmediate field unrestricted nativePhysicalImmediateValue : (family ModelWord64) constructor NativePhysicalResultValue field unrestricted nativePhysicalResultValueSlot : (family NativePhysicalSlot) constructor NativePhysicalResultAddress field unrestricted nativePhysicalResultAddressSlot : (family NativePhysicalSlot) field unrestricted nativePhysicalResultAddressOffset : (family ModelWord64) constructor NativePhysicalStateAddress field unrestricted nativePhysicalStateAddressOffset : (family ModelWord64) constructor NativePhysicalStateLoad64 field unrestricted nativePhysicalStateLoadOffset : (family ModelWord64) constructor NativePhysicalPayloadAddress field unrestricted nativePhysicalPayloadAddressOffset : (family ModelWord64) constructor NativePhysicalPayloadLoad64 field unrestricted nativePhysicalPayloadLoadOffset : (family ModelWord64) constructor NativePhysicalProcessArgument field unrestricted nativePhysicalProcessArgumentIndex : (family ModelWord64) -- base + iteration * stride, where iteration counts the enclosing repeat's -- completed passes from zero. Outside a repeat the iteration is zero. constructor NativePhysicalLoopAffine field unrestricted nativePhysicalLoopAffineBase : (family ModelWord64) field unrestricted nativePhysicalLoopAffineStride : (family ModelWord64) end-family family NativePhysicalArguments : Type 0 constructor NativePhysicalArgumentsValue field unrestricted nativePhysicalArgument0 : (family NativePhysicalOperand) field unrestricted nativePhysicalArgument1 : (family NativePhysicalOperand) field unrestricted nativePhysicalArgument2 : (family NativePhysicalOperand) field unrestricted nativePhysicalArgument3 : (family NativePhysicalOperand) field unrestricted nativePhysicalArgument4 : (family NativePhysicalOperand) field unrestricted nativePhysicalArgument5 : (family NativePhysicalOperand) end-family family NativePhysicalResultBinding : Type 0 constructor NativePhysicalDiscardResult constructor NativePhysicalStoreResult field unrestricted nativePhysicalStoredResultSlot : (family NativePhysicalSlot) end-family -- The binary64 operations the host computes with (IEEE 754, round to -- nearest even; x86 SSE2): the sum, difference, product and quotient of -- the left and right operands' words read as binary64; the square root of -- the right one; the left word, a natural below 2^63, as the nearest -- binary64; the left binary64 rounded to the nearest binary32 (its word -- zero-extended); the left word's low half, a binary32, as the binary64 of -- the same value. (Binary32 +, -, *, / and square root are these binary64 -- operations rounded to binary32: 53 bits hold 2 x 24 + 2, so the double -- rounding is exact.) family NativePhysicalFloat64Operation : Type 0 constructor NativePhysicalFloat64Add constructor NativePhysicalFloat64Subtract constructor NativePhysicalFloat64Multiply constructor NativePhysicalFloat64Divide constructor NativePhysicalFloat64SquareRoot constructor NativePhysicalFloat64FromNatural constructor NativePhysicalFloat64ToBinary32 constructor NativePhysicalFloat64FromBinary32 end-family family NativePhysicalOperation : Type 0 constructor NativePhysicalSystemCall field unrestricted nativePhysicalSystemCallNumber : (family NativePhysicalOperand) field unrestricted nativePhysicalSystemCallArguments : (family NativePhysicalArguments) field unrestricted nativePhysicalSystemCallPayload : Bytes field unrestricted nativePhysicalSystemCallResult : (family NativePhysicalResultBinding) constructor NativePhysicalCopyPayloadToState field unrestricted nativePhysicalCopyDestinationOffset : (family ModelWord64) field unrestricted nativePhysicalCopyExtent : (family ModelWord64) field unrestricted nativePhysicalCopyPayload : Bytes constructor NativePhysicalMachineRoutine field unrestricted nativePhysicalMachineCode : Bytes field unrestricted nativePhysicalMachineArguments : (family NativePhysicalArguments) field unrestricted nativePhysicalMachineResult : (family NativePhysicalResultBinding) constructor NativePhysicalFencePoll field unrestricted nativePhysicalFenceAddress : (family NativePhysicalOperand) field unrestricted nativePhysicalFenceExpected : (family NativePhysicalOperand) field unrestricted nativePhysicalFenceMaximumPolls : (family ModelWord64) constructor NativePhysicalTelemetryAppend field unrestricted nativePhysicalTelemetryPath : Bytes field unrestricted nativePhysicalTelemetryRecord : Bytes constructor NativePhysicalAssertEqual field unrestricted nativePhysicalAssertLeft : (family NativePhysicalOperand) field unrestricted nativePhysicalAssertRight : (family NativePhysicalOperand) field unrestricted nativePhysicalAssertError : (family NativePhysicalErrorCode) constructor NativePhysicalAssertOneOf field unrestricted nativePhysicalAssertOneOfObserved : (family NativePhysicalOperand) field unrestricted nativePhysicalAssertOneOfFirst : (family NativePhysicalOperand) field unrestricted nativePhysicalAssertOneOfSecond : (family NativePhysicalOperand) field unrestricted nativePhysicalAssertOneOfError : (family NativePhysicalErrorCode) constructor NativePhysicalHaltSuccess -- Execute the commands up to the matching RepeatEnd count times. Repeats do -- not nest; the runtime keeps one iteration counter and the loop-affine -- operands read it. constructor NativePhysicalRepeatBegin field unrestricted nativePhysicalRepeatCount : (family ModelWord64) constructor NativePhysicalRepeatEnd -- Store the 64-bit value of an operand at the address another operand -- resolves to (a state or result address): how a repeat body places a -- loop-affine value where a system call can read it. constructor NativePhysicalStoreWord64 field unrestricted nativePhysicalStoreDestination : (family NativePhysicalOperand) field unrestricted nativePhysicalStoreValue : (family NativePhysicalOperand) -- Wait until the 64-bit word at an address equals the expected value, -- sleeping intervalNanoseconds between polls (a nanosleep, so the host does -- not spin), at most maximumPolls times: how a host waits on device state -- (a completion semaphore) instead of on the clock. A timeout is a command -- failure -- it never yields a ready value. The interval must be below one -- second so the timespec is a single nanosecond field. constructor NativePhysicalFenceWait field unrestricted nativePhysicalFenceWaitAddress : (family NativePhysicalOperand) field unrestricted nativePhysicalFenceWaitExpected : (family NativePhysicalOperand) field unrestricted nativePhysicalFenceWaitMaximumPolls : (family ModelWord64) field unrestricted nativePhysicalFenceWaitIntervalNanoseconds : (family ModelWord64) -- A repeat whose count an operand gives at run time (a state word): a -- count of zero skips the body, so it is how a block is made conditional -- on what the host has read. constructor NativePhysicalRepeatBeginCounted field unrestricted nativePhysicalRepeatCountOperand : (family NativePhysicalOperand) -- The 64-bit sum (modulo 2^64) of two operands, stored at the address a -- third resolves to. constructor NativePhysicalAddWord64 field unrestricted nativePhysicalAddDestination : (family NativePhysicalOperand) field unrestricted nativePhysicalAddLeft : (family NativePhysicalOperand) field unrestricted nativePhysicalAddRight : (family NativePhysicalOperand) -- A binary64 operation on two operands' words, the result's word stored at -- the address a third resolves to. constructor NativePhysicalFloat64 field unrestricted nativePhysicalFloat64Operation : (family NativePhysicalFloat64Operation) field unrestricted nativePhysicalFloat64Destination : (family NativePhysicalOperand) field unrestricted nativePhysicalFloat64Left : (family NativePhysicalOperand) field unrestricted nativePhysicalFloat64Right : (family NativePhysicalOperand) end-family family NativePhysicalCommand : Type 0 constructor NativePhysicalCommandValue field unrestricted nativePhysicalCommandOperation : (family NativePhysicalOperation) field unrestricted nativePhysicalCommandErrorIdentity : Bytes end-family family NativePhysicalCommands : Type 0 constructor NativePhysicalCommandsEnd constructor NativePhysicalCommandsNext field unrestricted nativePhysicalCommandHead : (family NativePhysicalCommand) recursive unrestricted nativePhysicalCommandTail end-family family NativePhysicalProgram : Type 0 constructor NativePhysicalProgramValue field unrestricted nativePhysicalProgramStateExtent : (family ModelWord64) field unrestricted nativePhysicalProgramResultSlots : (family ModelWord64) field unrestricted nativePhysicalProgramCommands : (family NativePhysicalCommands) field unrestricted nativePhysicalProgramExpectedCommands : Nat field unrestricted nativePhysicalProgramIdentity : Bytes field unrestricted nativePhysicalProgramFallbacks : Nat end-family family NativePhysicalCounts : Type 0 constructor NativePhysicalCountsValue field unrestricted nativePhysicalCountCommands : Nat field unrestricted nativePhysicalCountSystemCalls : Nat field unrestricted nativePhysicalCountCopies : Nat field unrestricted nativePhysicalCountMachineRoutines : Nat field unrestricted nativePhysicalCountFencePolls : Nat field unrestricted nativePhysicalCountTelemetryAppends : Nat field unrestricted nativePhysicalCountAssertions : Nat field unrestricted nativePhysicalCountHalts : Nat field unrestricted nativePhysicalCountPayloadBytes : Nat end-family family NativePhysicalOperationValidation : Type 0 constructor NativePhysicalOperationValid constructor NativePhysicalOperationInvalid field unrestricted nativePhysicalOperationError : (family NativePhysicalErrorCode) end-family family NativePhysicalCommandsValidation : Type 0 constructor NativePhysicalCommandsValid field unrestricted nativePhysicalValidatedCommands : Nat constructor NativePhysicalCommandsInvalid field unrestricted nativePhysicalCommandsError : (family NativePhysicalErrorCode) field unrestricted nativePhysicalCommandsErrorOrdinal : Nat end-family family NativePhysicalValidationTelemetry : Type 0 constructor NativePhysicalValidationTelemetryValue field unrestricted nativePhysicalValidationCounts : (family NativePhysicalCounts) field unrestricted nativePhysicalValidationExpectedCommands : Nat field unrestricted nativePhysicalValidationStateExtent : (family ModelWord64) field unrestricted nativePhysicalValidationResultSlots : (family ModelWord64) field unrestricted nativePhysicalValidationFallbacks : Nat field unrestricted nativePhysicalValidationIdentity : Bytes field unrestricted nativePhysicalValidationFailures : Nat field unrestricted nativePhysicalValidationFailureOrdinal : Nat field unrestricted nativePhysicalValidationFailureCode : Bytes end-family family NativePhysicalProgramValidation : Type 0 constructor NativePhysicalProgramValidated field unrestricted nativePhysicalValidatedProgram : (family NativePhysicalProgram) field unrestricted nativePhysicalValidatedTelemetry : (family NativePhysicalValidationTelemetry) constructor NativePhysicalProgramRejected field unrestricted nativePhysicalRejectedError : (family NativePhysicalErrorCode) field unrestricted nativePhysicalRejectedTelemetry : (family NativePhysicalValidationTelemetry) end-family def nativePhysicalErrorCodeBytes = (lambda unrestricted code : (family NativePhysicalErrorCode) . (eliminate NativePhysicalErrorCode (lambda unrestricted current : (family NativePhysicalErrorCode) . Bytes) code (branch NativePhysicalIdentityInvalid . b"ALPHA-PHYS-001") (branch NativePhysicalFallbackObserved . b"ALPHA-PHYS-002") (branch NativePhysicalCommandCountMismatch . b"ALPHA-PHYS-003") (branch NativePhysicalStateExtentZero . b"ALPHA-PHYS-004") (branch NativePhysicalCopyPayloadEmpty . b"ALPHA-PHYS-005") (branch NativePhysicalCopyExtentZero . b"ALPHA-PHYS-006") (branch NativePhysicalMachineCodeEmpty . b"ALPHA-PHYS-007") (branch NativePhysicalFencePollCountZero . b"ALPHA-PHYS-008") (branch NativePhysicalTelemetryPathEmpty . b"ALPHA-PHYS-009") (branch NativePhysicalTelemetryRecordEmpty . b"ALPHA-PHYS-010") (branch NativePhysicalResultSlotUnavailable . b"ALPHA-PHYS-011") (branch NativePhysicalExecutionAssertionFailed . b"ALPHA-PHYS-012") (branch NativePhysicalRepeatCountZero . b"ALPHA-PHYS-013") (branch NativePhysicalRepeatUnbalanced . b"ALPHA-PHYS-014") (branch NativePhysicalFenceWaitCountZero . b"ALPHA-PHYS-015") (branch NativePhysicalFenceWaitIntervalInvalid . b"ALPHA-PHYS-016"))) def nativePhysicalZeroCounts : (family NativePhysicalCounts) = (constructor NativePhysicalCounts NativePhysicalCountsValue zero zero zero zero zero zero zero zero zero) def nativePhysicalAddCounts = (lambda unrestricted left : (family NativePhysicalCounts) . (lambda unrestricted right : (family NativePhysicalCounts) . (eliminate NativePhysicalCounts (lambda unrestricted current : (family NativePhysicalCounts) . (family NativePhysicalCounts)) left (branch NativePhysicalCountsValue leftCommands leftSystemCalls leftCopies leftRoutines leftFences leftTelemetry leftAssertions leftHalts leftPayload . (eliminate NativePhysicalCounts (lambda unrestricted current : (family NativePhysicalCounts) . (family NativePhysicalCounts)) right (branch NativePhysicalCountsValue rightCommands rightSystemCalls rightCopies rightRoutines rightFences rightTelemetry rightAssertions rightHalts rightPayload . (constructor NativePhysicalCounts NativePhysicalCountsValue (naturalAdd leftCommands rightCommands) (naturalAdd leftSystemCalls rightSystemCalls) (naturalAdd leftCopies rightCopies) (naturalAdd leftRoutines rightRoutines) (naturalAdd leftFences rightFences) (naturalAdd leftTelemetry rightTelemetry) (naturalAdd leftAssertions rightAssertions) (naturalAdd leftHalts rightHalts) (naturalAdd leftPayload rightPayload)))))))) def nativePhysicalOperationCounts = (lambda unrestricted operation : (family NativePhysicalOperation) . (eliminate NativePhysicalOperation (lambda unrestricted current : (family NativePhysicalOperation) . (family NativePhysicalCounts)) operation (branch NativePhysicalSystemCall number arguments payload result . (constructor NativePhysicalCounts NativePhysicalCountsValue (succ zero) (succ zero) zero zero zero zero zero zero (bytes-length payload))) (branch NativePhysicalCopyPayloadToState destination extent payload . (constructor NativePhysicalCounts NativePhysicalCountsValue (succ zero) zero (succ zero) zero zero zero zero zero (bytes-length payload))) (branch NativePhysicalMachineRoutine code arguments result . (constructor NativePhysicalCounts NativePhysicalCountsValue (succ zero) zero zero (succ zero) zero zero zero zero (bytes-length code))) (branch NativePhysicalFencePoll address expected maximumPolls . (constructor NativePhysicalCounts NativePhysicalCountsValue (succ zero) zero zero zero (succ zero) zero zero zero zero)) (branch NativePhysicalTelemetryAppend path record . (constructor NativePhysicalCounts NativePhysicalCountsValue (succ zero) zero zero zero zero (succ zero) zero zero (naturalAdd (bytes-length path) (bytes-length record)))) (branch NativePhysicalAssertEqual left right error . (constructor NativePhysicalCounts NativePhysicalCountsValue (succ zero) zero zero zero zero zero (succ zero) zero zero)) (branch NativePhysicalAssertOneOf observed first second error . (constructor NativePhysicalCounts NativePhysicalCountsValue (succ zero) zero zero zero zero zero (succ zero) zero zero)) (branch NativePhysicalHaltSuccess . (constructor NativePhysicalCounts NativePhysicalCountsValue (succ zero) zero zero zero zero zero zero (succ zero) zero)) (branch NativePhysicalRepeatBegin count . (constructor NativePhysicalCounts NativePhysicalCountsValue (succ zero) zero zero zero zero zero zero zero zero)) (branch NativePhysicalRepeatEnd . (constructor NativePhysicalCounts NativePhysicalCountsValue (succ zero) zero zero zero zero zero zero zero zero)) (branch NativePhysicalStoreWord64 destination value . (constructor NativePhysicalCounts NativePhysicalCountsValue (succ zero) zero zero zero zero zero zero zero zero)) (branch NativePhysicalFenceWait address expected maximumPolls interval . (constructor NativePhysicalCounts NativePhysicalCountsValue (succ zero) zero zero zero zero zero zero zero zero)) (branch NativePhysicalRepeatBeginCounted count . (constructor NativePhysicalCounts NativePhysicalCountsValue (succ zero) zero zero zero zero zero zero zero zero)) (branch NativePhysicalAddWord64 destination left right . (constructor NativePhysicalCounts NativePhysicalCountsValue (succ zero) zero zero zero zero zero zero zero zero)) (branch NativePhysicalFloat64 operation destination left right . (constructor NativePhysicalCounts NativePhysicalCountsValue (succ zero) zero zero zero zero zero zero zero zero)))) def nativePhysicalCommandCounts = (lambda unrestricted command : (family NativePhysicalCommand) . (eliminate NativePhysicalCommand (lambda unrestricted current : (family NativePhysicalCommand) . (family NativePhysicalCounts)) command (branch NativePhysicalCommandValue operation errorIdentity . (nativePhysicalOperationCounts operation)))) def nativePhysicalCommandsCounts = (lambda unrestricted commands : (family NativePhysicalCommands) . (eliminate NativePhysicalCommands (lambda unrestricted current : (family NativePhysicalCommands) . (family NativePhysicalCounts)) commands (branch NativePhysicalCommandsEnd . nativePhysicalZeroCounts) (branch NativePhysicalCommandsNext head tail induction . (nativePhysicalAddCounts (nativePhysicalCommandCounts head) induction)))) def nativePhysicalRequireBytes = (lambda unrestricted payload : Bytes . (lambda unrestricted error : (family NativePhysicalErrorCode) . (nat-eliminate (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation)) (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid error) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family NativePhysicalOperationValidation) . (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))) (bytes-length payload)))) -- A wait interval is valid when it is at least one nanosecond and below one -- second (999,999,999 nanoseconds), so a timespec with a zero seconds field -- carries it. def nativePhysicalFenceWaitIntervalValid = (lambda unrestricted interval : (family ModelWord64) . (naturalAnd (naturalIsZero (modelWord64IsZero interval)) (modelWord64LessThan interval (modelWord64FromNaturalTruncated 1000000000)))) def nativePhysicalValidateOperation = (lambda unrestricted operation : (family NativePhysicalOperation) . (eliminate NativePhysicalOperation (lambda unrestricted current : (family NativePhysicalOperation) . (family NativePhysicalOperationValidation)) operation (branch NativePhysicalSystemCall number arguments payload result . (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)) (branch NativePhysicalCopyPayloadToState destination extent payload . (eliminate NativePhysicalOperationValidation (lambda unrestricted current : (family NativePhysicalOperationValidation) . (family NativePhysicalOperationValidation)) (nativePhysicalRequireBytes payload (constructor NativePhysicalErrorCode NativePhysicalCopyPayloadEmpty)) (branch NativePhysicalOperationValid . (nat-eliminate (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation)) (constructor NativePhysicalOperationValidation NativePhysicalOperationValid) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family NativePhysicalOperationValidation) . (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid (constructor NativePhysicalErrorCode NativePhysicalCopyExtentZero)))) (modelWord64IsZero extent))) (branch NativePhysicalOperationInvalid error . (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid error)))) (branch NativePhysicalMachineRoutine code arguments result . (nativePhysicalRequireBytes code (constructor NativePhysicalErrorCode NativePhysicalMachineCodeEmpty))) (branch NativePhysicalFencePoll address expected maximumPolls . (nat-eliminate (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation)) (constructor NativePhysicalOperationValidation NativePhysicalOperationValid) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family NativePhysicalOperationValidation) . (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid (constructor NativePhysicalErrorCode NativePhysicalFencePollCountZero)))) (modelWord64IsZero maximumPolls))) (branch NativePhysicalTelemetryAppend path record . (eliminate NativePhysicalOperationValidation (lambda unrestricted current : (family NativePhysicalOperationValidation) . (family NativePhysicalOperationValidation)) (nativePhysicalRequireBytes path (constructor NativePhysicalErrorCode NativePhysicalTelemetryPathEmpty)) (branch NativePhysicalOperationValid . (nativePhysicalRequireBytes record (constructor NativePhysicalErrorCode NativePhysicalTelemetryRecordEmpty))) (branch NativePhysicalOperationInvalid error . (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid error)))) (branch NativePhysicalAssertEqual left right error . (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)) (branch NativePhysicalAssertOneOf observed first second error . (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)) (branch NativePhysicalHaltSuccess . (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)) (branch NativePhysicalRepeatBegin count . (nat-eliminate (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation)) (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid (constructor NativePhysicalErrorCode NativePhysicalRepeatCountZero)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family NativePhysicalOperationValidation) . (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))) (naturalIsZero (modelWord64IsZero count)))) (branch NativePhysicalRepeatEnd . (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)) (branch NativePhysicalStoreWord64 destination value . (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)) (branch NativePhysicalFenceWait address expected maximumPolls interval . (nat-eliminate (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation)) (nat-eliminate (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation)) (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid (constructor NativePhysicalErrorCode NativePhysicalFenceWaitIntervalInvalid)) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family NativePhysicalOperationValidation) . (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))) (nativePhysicalFenceWaitIntervalValid interval)) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family NativePhysicalOperationValidation) . (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid (constructor NativePhysicalErrorCode NativePhysicalFenceWaitCountZero)))) (modelWord64IsZero maximumPolls))) (branch NativePhysicalRepeatBeginCounted count . (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)) (branch NativePhysicalAddWord64 destination left right . (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)) (branch NativePhysicalFloat64 operation destination left right . (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)))) -- Repeats must pair and never nest: 0 means balanced, 1 means a repeat is -- still open, 2 means an end without a begin or a begin inside a repeat. def nativePhysicalRepeatBalance = (lambda unrestricted commands : (family NativePhysicalCommands) . (app (eliminate NativePhysicalCommands (lambda unrestricted current : (family NativePhysicalCommands) . (pi unrestricted open : Nat . Nat)) commands (branch NativePhysicalCommandsEnd . (lambda unrestricted open : Nat . open)) (branch NativePhysicalCommandsNext head tail induction . (lambda unrestricted open : Nat . (eliminate NativePhysicalCommand (lambda unrestricted current : (family NativePhysicalCommand) . Nat) head (branch NativePhysicalCommandValue operation errorIdentity . (eliminate NativePhysicalOperation (lambda unrestricted current : (family NativePhysicalOperation) . Nat) operation (branch NativePhysicalSystemCall number arguments payload result . (induction open)) (branch NativePhysicalCopyPayloadToState destination extent payload . (induction open)) (branch NativePhysicalMachineRoutine code arguments result . (induction open)) (branch NativePhysicalFencePoll address expected polls . (induction open)) (branch NativePhysicalTelemetryAppend path record . (induction open)) (branch NativePhysicalAssertEqual left right error . (induction open)) (branch NativePhysicalAssertOneOf observed first second error . (induction open)) (branch NativePhysicalHaltSuccess . (induction open)) (branch NativePhysicalRepeatBegin count . (nat-eliminate (lambda unrestricted current : Nat . Nat) (induction (succ zero)) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat . 2)) open)) (branch NativePhysicalRepeatEnd . (nat-eliminate (lambda unrestricted current : Nat . Nat) 2 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat . (nat-eliminate (lambda unrestricted current : Nat . Nat) (induction zero) (lambda unrestricted deeper : Nat . (lambda unrestricted ignoredDeeper : Nat . 2)) predecessor))) open)) (branch NativePhysicalStoreWord64 destination value . (induction open)) (branch NativePhysicalFenceWait address expected polls interval . (induction open)) (branch NativePhysicalRepeatBeginCounted count . (nat-eliminate (lambda unrestricted current : Nat . Nat) (induction (succ zero)) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat . 2)) open)) (branch NativePhysicalAddWord64 destination left right . (induction open)) (branch NativePhysicalFloat64 operation destination left right . (induction open)))))))) zero)) def nativePhysicalValidateCommands = (lambda unrestricted commands : (family NativePhysicalCommands) . (eliminate NativePhysicalCommands (lambda unrestricted current : (family NativePhysicalCommands) . (family NativePhysicalCommandsValidation)) commands (branch NativePhysicalCommandsEnd . (constructor NativePhysicalCommandsValidation NativePhysicalCommandsValid zero)) (branch NativePhysicalCommandsNext head tail induction . (eliminate NativePhysicalCommand (lambda unrestricted current : (family NativePhysicalCommand) . (family NativePhysicalCommandsValidation)) head (branch NativePhysicalCommandValue operation errorIdentity . (eliminate NativePhysicalOperationValidation (lambda unrestricted current : (family NativePhysicalOperationValidation) . (family NativePhysicalCommandsValidation)) (nativePhysicalValidateOperation operation) (branch NativePhysicalOperationValid . (eliminate NativePhysicalCommandsValidation (lambda unrestricted current : (family NativePhysicalCommandsValidation) . (family NativePhysicalCommandsValidation)) induction (branch NativePhysicalCommandsValid completed . (constructor NativePhysicalCommandsValidation NativePhysicalCommandsValid (succ completed))) (branch NativePhysicalCommandsInvalid error ordinal . (constructor NativePhysicalCommandsValidation NativePhysicalCommandsInvalid error (succ ordinal))))) (branch NativePhysicalOperationInvalid error . (constructor NativePhysicalCommandsValidation NativePhysicalCommandsInvalid error zero)))))))) def nativePhysicalValidationTelemetryFor = (lambda unrestricted program : (family NativePhysicalProgram) . (lambda unrestricted failures : Nat . (lambda unrestricted ordinal : Nat . (lambda unrestricted code : Bytes . (eliminate NativePhysicalProgram (lambda unrestricted current : (family NativePhysicalProgram) . (family NativePhysicalValidationTelemetry)) program (branch NativePhysicalProgramValue stateExtent resultSlots commands expected identity fallbacks . (constructor NativePhysicalValidationTelemetry NativePhysicalValidationTelemetryValue (nativePhysicalCommandsCounts commands) expected stateExtent resultSlots fallbacks identity failures ordinal code))))))) def nativePhysicalReject = (lambda unrestricted program : (family NativePhysicalProgram) . (lambda unrestricted error : (family NativePhysicalErrorCode) . (lambda unrestricted ordinal : Nat . (constructor NativePhysicalProgramValidation NativePhysicalProgramRejected error (nativePhysicalValidationTelemetryFor program (succ zero) ordinal (nativePhysicalErrorCodeBytes error)))))) def nativePhysicalValidateProgram = (lambda unrestricted program : (family NativePhysicalProgram) . (eliminate NativePhysicalProgram (lambda unrestricted current : (family NativePhysicalProgram) . (family NativePhysicalProgramValidation)) program (branch NativePhysicalProgramValue stateExtent resultSlots commands expected identity fallbacks . (nat-eliminate (lambda unrestricted current : Nat . (family NativePhysicalProgramValidation)) (nativePhysicalReject program (constructor NativePhysicalErrorCode NativePhysicalIdentityInvalid) zero) (lambda unrestricted identityPredecessor : Nat . (lambda unrestricted ignoredIdentity : (family NativePhysicalProgramValidation) . (nat-eliminate (lambda unrestricted current : Nat . (family NativePhysicalProgramValidation)) (nativePhysicalReject program (constructor NativePhysicalErrorCode NativePhysicalFallbackObserved) zero) (lambda unrestricted fallbackPredecessor : Nat . (lambda unrestricted ignoredFallback : (family NativePhysicalProgramValidation) . (nat-eliminate (lambda unrestricted current : Nat . (family NativePhysicalProgramValidation)) (eliminate NativePhysicalCommandsValidation (lambda unrestricted current : (family NativePhysicalCommandsValidation) . (family NativePhysicalProgramValidation)) (nat-eliminate (lambda unrestricted current : Nat . (family NativePhysicalCommandsValidation)) (nativePhysicalValidateCommands commands) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignoredBalance : (family NativePhysicalCommandsValidation) . (constructor NativePhysicalCommandsValidation NativePhysicalCommandsInvalid (constructor NativePhysicalErrorCode NativePhysicalRepeatUnbalanced) zero))) (nativePhysicalRepeatBalance commands)) (branch NativePhysicalCommandsValid completed . (nat-eliminate (lambda unrestricted current : Nat . (family NativePhysicalProgramValidation)) (nativePhysicalReject program (constructor NativePhysicalErrorCode NativePhysicalCommandCountMismatch) zero) (lambda unrestricted countPredecessor : Nat . (lambda unrestricted ignoredCount : (family NativePhysicalProgramValidation) . (constructor NativePhysicalProgramValidation NativePhysicalProgramValidated program (nativePhysicalValidationTelemetryFor program zero zero b"")))) (naturalEqual completed expected))) (branch NativePhysicalCommandsInvalid error ordinal . (nativePhysicalReject program error ordinal))) (lambda unrestricted statePredecessor : Nat . (lambda unrestricted ignoredState : (family NativePhysicalProgramValidation) . (nativePhysicalReject program (constructor NativePhysicalErrorCode NativePhysicalStateExtentZero) zero))) (modelWord64IsZero stateExtent)))) (naturalEqual fallbacks zero)))) (naturalEqual (bytes-length identity) (byte-to-nat (byte 64)))))))