module Runtime.TelemetryCaptureRoutine import Runtime.TelemetryCapture import Std.Natural -- One bounded, single-writer acquisition algorithm. The host emitter owns its -- calling convention; this algorithm neither allocates nor performs IO. -- Loads/stores are little-endian 64-bit words and arithmetic wraps at 64 bits. -- Compare supplies unsigned order/equality. Add must also supply Below iff its -- unsigned sum overflowed; no other Add flags are used. CompareMaximum tests -- against the full unsigned 64-bit maximum, independent of ISA immediates. -- Product multiplies ProductLow by Position, replacing ProductLow with the -- low word and ValuesOrOverflow with zero iff the full product fits a word. -- SavedValues preserves the original values pointer across that check. No -- caller state is mutated before all extent and counter checks have succeeded. -- Scale multiplies by the positive record stride with word-wrap semantics. family TelemetryCaptureCondition : Type 0 constructor TelemetryCaptureZero constructor TelemetryCaptureNotZero constructor TelemetryCaptureBelow constructor TelemetryCaptureAbove end-family family TelemetryCaptureBackend : Type 0 parameter erased A : Type 0 parameter erased R : Type 0 constructor TelemetryCaptureBackendValue field unrestricted backendCaptureLoad : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : Nat . (pi unrestricted a3 : A . A)))) field unrestricted backendCaptureStore : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : R . (pi unrestricted a3 : A . A)))) field unrestricted backendCaptureMove : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A))) field unrestricted backendCaptureAdd : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A))) field unrestricted backendCaptureCompare : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A))) field unrestricted backendCaptureCompareImmediate : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A))) field unrestricted backendCaptureCompareMaximum : (pi unrestricted a0 : R . (pi unrestricted a1 : A . A)) field unrestricted backendCaptureSet : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A))) field unrestricted backendCaptureIncrement : (pi unrestricted a0 : R . (pi unrestricted a1 : A . A)) field unrestricted backendCaptureScale : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A))) field unrestricted backendCaptureProduct : (pi unrestricted a0 : A . A) field unrestricted backendCaptureReturnCode : (pi unrestricted a0 : Nat . (pi unrestricted a1 : A . A)) field unrestricted backendCaptureLabel : (pi unrestricted a0 : Bytes . (pi unrestricted a1 : A . A)) field unrestricted backendCaptureJump : (pi unrestricted a0 : Bytes . (pi unrestricted a1 : A . A)) field unrestricted backendCaptureJumpIf : (pi unrestricted a0 : (family TelemetryCaptureCondition) . (pi unrestricted a1 : Bytes . (pi unrestricted a2 : A . A))) field unrestricted backendCaptureEnd : A field unrestricted backendCaptureProductLow : R field unrestricted backendCaptureSelected : R field unrestricted backendCaptureValuesOrOverflow : R field unrestricted backendCaptureQueue : R field unrestricted backendCaptureControl : R field unrestricted backendCaptureReserved : R field unrestricted backendCaptureQueueExtent : R field unrestricted backendCapturePosition : R field unrestricted backendCaptureSavedValues : R end-family def telemetryCaptureAssemblyFor = (lambda erased A : Type 0 . (lambda erased R : Type 0 . (lambda unrestricted backend : (family TelemetryCaptureBackend A R) . (eliminate TelemetryCaptureBackend (lambda unrestricted current : (family TelemetryCaptureBackend A R) . A) backend (branch TelemetryCaptureBackendValue captureLoad captureStore captureMove captureAdd captureCompare captureCompareImmediate captureCompareMaximum captureSet captureIncrement captureScale captureProduct captureReturnCode captureLabel captureJump captureJumpIf captureEnd captureProductLow captureSelected captureValuesOrOverflow captureQueue captureControl captureReserved captureQueueExtent capturePosition captureSavedValues . (let unrestricted captureCopyValues = (lambda unrestricted words : Nat . (lambda unrestricted tail : A . (nat-eliminate (lambda unrestricted n : Nat . A) tail (lambda unrestricted index : Nat . (lambda unrestricted previous : A . (captureLoad captureProductLow captureValuesOrOverflow (naturalMultiply index captureWordBytes) (captureStore capturePosition (naturalAdd captureValuesAt (naturalMultiply index captureWordBytes)) captureProductLow previous)))) words))) in (let unrestricted captureAssemblyPart4 = (captureLabel b"reject" (captureReturnCode 4 captureEnd)) in (let unrestricted captureAssemblyPart3 = (captureJumpIf (constructor TelemetryCaptureCondition TelemetryCaptureNotZero) b"pause" (captureLoad captureProductLow captureControl captureNextSequenceAt (captureCompareMaximum captureProductLow (captureJumpIf (constructor TelemetryCaptureCondition TelemetryCaptureZero) b"reject" (captureMove capturePosition captureProductLow (captureLoad captureProductLow captureControl captureDroppedAt (captureCompareMaximum captureProductLow (captureJumpIf (constructor TelemetryCaptureCondition TelemetryCaptureZero) b"reject" (captureIncrement captureProductLow (captureStore captureControl captureDroppedAt captureProductLow (captureIncrement capturePosition (captureStore captureControl captureNextSequenceAt capturePosition (captureReturnCode 2 (captureLabel b"excluded" (captureCompareImmediate captureReserved 0 (captureJumpIf (constructor TelemetryCaptureCondition TelemetryCaptureNotZero) b"reject" (captureLoad captureProductLow captureControl captureExcludedAt (captureCompareMaximum captureProductLow (captureJumpIf (constructor TelemetryCaptureCondition TelemetryCaptureZero) b"reject" (captureIncrement captureProductLow (captureStore captureControl captureExcludedAt captureProductLow (captureReturnCode 0 (captureLabel b"pause" (captureReturnCode 3 captureAssemblyPart4)))))))))))))))))))))))) in (let unrestricted captureAssemblyPart2 = (captureAdd capturePosition captureProductLow (captureLoad captureProductLow captureControl captureNextSequenceAt (captureCompareMaximum captureProductLow (captureJumpIf (constructor TelemetryCaptureCondition TelemetryCaptureZero) b"reject" (captureStore capturePosition captureSequenceAt captureProductLow (captureCopyValues captureValueWords (captureLoad captureProductLow captureControl captureNextSequenceAt (captureIncrement captureProductLow (captureStore captureControl captureNextSequenceAt captureProductLow (captureCompareImmediate captureReserved 0 (captureJumpIf (constructor TelemetryCaptureCondition TelemetryCaptureNotZero) b"commit-reserved" (captureLoad captureProductLow captureControl captureOrdinaryUsedAt (captureIncrement captureProductLow (captureStore captureControl captureOrdinaryUsedAt captureProductLow (captureJump b"queued" (captureLabel b"commit-reserved" (captureLoad captureProductLow captureControl captureReservedUsedAt (captureIncrement captureProductLow (captureStore captureControl captureReservedUsedAt captureProductLow (captureLabel b"queued" (captureReturnCode 1 (captureLabel b"ordinary-full" (captureLoad captureProductLow captureControl captureRequiredAt (captureCompareImmediate captureProductLow 0 captureAssemblyPart3)))))))))))))))))))))))) in (let unrestricted captureAssemblyPart1 = (captureCompareImmediate captureValuesOrOverflow 0 (captureJumpIf (constructor TelemetryCaptureCondition TelemetryCaptureNotZero) b"reject" (captureCompare captureProductLow captureQueueExtent (captureJumpIf (constructor TelemetryCaptureCondition TelemetryCaptureAbove) b"reject" (captureMove captureValuesOrOverflow captureSavedValues (captureCompareImmediate captureSelected 0 (captureJumpIf (constructor TelemetryCaptureCondition TelemetryCaptureZero) b"excluded" (captureCompareImmediate captureReserved 0 (captureJumpIf (constructor TelemetryCaptureCondition TelemetryCaptureNotZero) b"reserved" (captureLoad captureProductLow captureControl captureOrdinaryUsedAt (captureLoad capturePosition captureControl captureOrdinaryCapacityAt (captureCompare captureProductLow capturePosition (captureJumpIf (constructor TelemetryCaptureCondition TelemetryCaptureZero) b"ordinary-full" (captureJump b"position" (captureLabel b"reserved" (captureLoad captureProductLow captureControl captureReservedUsedAt (captureLoad capturePosition captureControl captureReservedCapacityAt (captureCompare captureProductLow capturePosition (captureJumpIf (constructor TelemetryCaptureCondition TelemetryCaptureZero) b"pause" (captureLoad capturePosition captureControl captureOrdinaryCapacityAt (captureAdd captureProductLow capturePosition (captureLabel b"position" (captureScale captureProductLow captureRecordBytes (captureMove capturePosition captureQueue captureAssemblyPart2)))))))))))))))))))))))) in (let unrestricted captureAssemblyPart0 = (captureMove captureSavedValues captureValuesOrOverflow (captureCompareImmediate captureSelected 1 (captureJumpIf (constructor TelemetryCaptureCondition TelemetryCaptureAbove) b"reject" (captureCompareImmediate captureReserved 1 (captureJumpIf (constructor TelemetryCaptureCondition TelemetryCaptureAbove) b"reject" (captureLoad captureProductLow captureControl captureRequiredAt (captureCompareImmediate captureProductLow 1 (captureJumpIf (constructor TelemetryCaptureCondition TelemetryCaptureAbove) b"reject" (captureLoad captureProductLow captureControl captureOrdinaryUsedAt (captureLoad capturePosition captureControl captureOrdinaryCapacityAt (captureCompare captureProductLow capturePosition (captureJumpIf (constructor TelemetryCaptureCondition TelemetryCaptureAbove) b"reject" (captureLoad captureProductLow captureControl captureReservedUsedAt (captureLoad capturePosition captureControl captureReservedCapacityAt (captureCompare captureProductLow capturePosition (captureJumpIf (constructor TelemetryCaptureCondition TelemetryCaptureAbove) b"reject" (captureLoad captureProductLow captureControl captureOrdinaryCapacityAt (captureLoad capturePosition captureControl captureReservedCapacityAt (captureCompareImmediate capturePosition 2 (captureJumpIf (constructor TelemetryCaptureCondition TelemetryCaptureBelow) b"reject" (captureAdd captureProductLow capturePosition (captureJumpIf (constructor TelemetryCaptureCondition TelemetryCaptureBelow) b"reject" (captureSet capturePosition captureRecordBytes (captureProduct captureAssemblyPart1)))))))))))))))))))))))) in captureAssemblyPart0)))))))))))