module Runtime.TelemetryDrainRoutine import Observe.Value import Runtime.NativeTelemetry import Runtime.TelemetryCapture import Runtime.TelemetryDrain import Runtime.TelemetryPublication import Runtime.TelemetryRecord import Std.Natural -- Single-writer staging and private route metadata, shared across host ISAs. -- The caller supplies live disjoint certified arenas and serializes capture, -- drain and commit. Extent checks precede loads/stores where the ABI supplies -- an extent. A failed accessible append/read clears readiness; an inaccessible -- publication extent must not dereference its pointer. Success only grants -- private staging: none of these routines writes a file or acknowledges data. -- Word operations wrap at 64 bits, comparisons are unsigned, and Divide uses -- Result with zero Argument2 as its dividend and positive Scratch0 divisor. -- Set retains its admitted 32-bit immediate, AddImmediate sign-extends it. family TelemetryDrainCondition : Type 0 constructor TelemetryDrainZero constructor TelemetryDrainNotZero constructor TelemetryDrainBelow constructor TelemetryDrainAbove end-family family TelemetryDrainRoutineKind : Type 0 constructor TelemetryDrainReadyRoutine constructor TelemetryDrainAppendRoutine field unrestricted drainAppendBound : Nat constructor TelemetryDrainCommitTagRoutine field unrestricted drainCommitOrdinary : Nat field unrestricted drainCommitReserved : Nat field unrestricted drainCommitRole : Nat field unrestricted drainCommitTag : Nat constructor TelemetryDrainReadTagRoutine field unrestricted drainReadOrdinary : Nat field unrestricted drainReadReserved : Nat field unrestricted drainReadRoutes : (family TelemetryRecordRoutes) constructor TelemetryDrainMatchTagRoutine field unrestricted drainMatchTag : Nat end-family family TelemetryDrainBackend : Type 0 parameter erased A : Type 0 parameter erased R : Type 0 constructor TelemetryDrainBackendValue field unrestricted backendDrainSet : (pi unrestricted register : R . (pi unrestricted value : Nat . (pi unrestricted tail : A . A))) field unrestricted backendDrainMove : (pi unrestricted left : R . (pi unrestricted right : R . (pi unrestricted tail : A . A))) field unrestricted backendDrainLoad : (pi unrestricted destination : R . (pi unrestricted base : R . (pi unrestricted offset : Nat . (pi unrestricted tail : A . A)))) field unrestricted backendDrainStore64 : (pi unrestricted base : R . (pi unrestricted offset : Nat . (pi unrestricted value : R . (pi unrestricted tail : A . A)))) field unrestricted backendDrainStore8 : (pi unrestricted base : R . (pi unrestricted offset : Nat . (pi unrestricted value : R . (pi unrestricted tail : A . A)))) field unrestricted backendDrainCompareImmediate : (pi unrestricted register : R . (pi unrestricted value : Nat . (pi unrestricted tail : A . A))) field unrestricted backendDrainCompare : (pi unrestricted left : R . (pi unrestricted right : R . (pi unrestricted tail : A . A))) field unrestricted backendDrainSubtract : (pi unrestricted left : R . (pi unrestricted right : R . (pi unrestricted tail : A . A))) field unrestricted backendDrainAdd : (pi unrestricted left : R . (pi unrestricted right : R . (pi unrestricted tail : A . A))) field unrestricted backendDrainAddImmediate : (pi unrestricted register : R . (pi unrestricted value : Nat . (pi unrestricted tail : A . A))) field unrestricted backendDrainMultiplyImmediate : (pi unrestricted register : R . (pi unrestricted value : Nat . (pi unrestricted tail : A . A))) field unrestricted backendDrainDivide : (pi unrestricted divisor : R . (pi unrestricted tail : A . A)) field unrestricted backendDrainJumpIf : (pi unrestricted condition : (family TelemetryDrainCondition) . (pi unrestricted name : Bytes . (pi unrestricted tail : A . A))) field unrestricted backendDrainJump : (pi unrestricted name : Bytes . (pi unrestricted tail : A . A)) field unrestricted backendDrainLabel : (pi unrestricted name : Bytes . (pi unrestricted tail : A . A)) field unrestricted backendDrainReturn : (pi unrestricted tail : A . A) field unrestricted backendDrainEnd : A field unrestricted backendDrainResult : R field unrestricted backendDrainArgument0 : R field unrestricted backendDrainArgument1 : R field unrestricted backendDrainArgument2 : R field unrestricted backendDrainArgument3 : R field unrestricted backendDrainArgument4 : R field unrestricted backendDrainArgument5 : R field unrestricted backendDrainScratch0 : R field unrestricted backendDrainScratch1 : R end-family def telemetryDrainAssemblyFor = (lambda erased A : Type 0 . (lambda erased R : Type 0 . (lambda unrestricted backend : (family TelemetryDrainBackend A R) . (lambda unrestricted kind : (family TelemetryDrainRoutineKind) . (eliminate TelemetryDrainBackend (lambda unrestricted current : (family TelemetryDrainBackend A R) . A) backend (branch TelemetryDrainBackendValue drainSet drainMove drainLoad drainStore64 drainStore8 drainCompareImmediate drainCompare drainSubtract drainAdd drainAddImmediate drainMultiplyImmediate drainDivide drainJumpIf drainJump drainLabel drainReturn drainEnd drainResult drainArgument0 drainArgument1 drainArgument2 drainArgument3 drainArgument4 drainArgument5 drainScratch0 drainScratch1 . (let unrestricted drainAllowedTagsWith = (lambda unrestricted routes : (family TelemetryRecordRoutes) . (lambda unrestricted tail : A . (eliminate TelemetryRecordRoutes (lambda unrestricted current : (family TelemetryRecordRoutes) . A) routes (branch TelemetryRecordRoutesEnd . (drainJump b"route-read-invalid" tail)) (branch TelemetryRecordRoutesNext tag recipe following induction . (drainCompareImmediate drainResult tag (drainJumpIf (constructor TelemetryDrainCondition TelemetryDrainZero) b"route-read-valid" induction)))))) in (eliminate TelemetryDrainRoutineKind (lambda unrestricted current : (family TelemetryDrainRoutineKind) . A) kind (branch TelemetryDrainReadyRoutine . (drainLoad drainResult drainArgument0 publicationReadyAt (drainCompareImmediate drainResult 1 (drainJumpIf (constructor TelemetryDrainCondition TelemetryDrainNotZero) b"drain-not-ready" (drainSet drainResult 1 (drainReturn (drainLabel b"drain-not-ready" (drainSet drainResult 0 (drainReturn drainEnd))))))))) (branch TelemetryDrainAppendRoutine bound . (drainCompareImmediate drainArgument3 (publicationArenaBytesForBody bound) (drainJumpIf (constructor TelemetryDrainCondition TelemetryDrainNotZero) b"drain-append-inaccessible" (drainCompareImmediate drainArgument2 bound (drainJumpIf (constructor TelemetryDrainCondition TelemetryDrainAbove) b"drain-append-refused" (drainMove drainResult drainArgument2 (drainAddImmediate drainResult telemetryRecordAt (drainCompare drainArgument4 drainResult (drainJumpIf (constructor TelemetryDrainCondition TelemetryDrainBelow) b"drain-append-refused" (drainLoad drainResult drainArgument0 publicationReadyAt (drainCompareImmediate drainResult 1 (drainJumpIf (constructor TelemetryDrainCondition TelemetryDrainNotZero) b"drain-append-refused" (drainLoad drainResult drainArgument1 0 (drainCompareImmediate drainResult 0 (drainJumpIf (constructor TelemetryDrainCondition TelemetryDrainNotZero) b"drain-append-refused" (drainLoad drainResult drainArgument0 publicationBodyLengthAt (drainCompareImmediate drainResult publicationPayloadRecordsAt (drainJumpIf (constructor TelemetryDrainCondition TelemetryDrainBelow) b"drain-append-refused" (drainCompareImmediate drainResult bound (drainJumpIf (constructor TelemetryDrainCondition TelemetryDrainAbove) b"drain-append-refused" (drainMove drainScratch0 drainResult (drainAdd drainScratch0 drainArgument2 (drainAddImmediate drainScratch0 1 (drainCompareImmediate drainScratch0 bound (drainJumpIf (constructor TelemetryDrainCondition TelemetryDrainAbove) b"drain-append-refused" (drainMove drainScratch1 drainArgument0 (drainAddImmediate drainScratch1 publicationBodyAt (drainAdd drainScratch1 drainResult (drainStore64 drainArgument0 publicationSavedR12At drainScratch1 (drainAdd drainScratch1 drainArgument2 (drainSet drainResult 10 (drainStore8 drainScratch1 0 drainResult (drainStore64 drainArgument0 publicationBodyLengthAt drainScratch0 (drainSet drainResult nativeTelemetryEmptyErrorPayloadAt (drainSubtract drainScratch0 drainResult (drainStore64 drainArgument0 (naturalAdd publicationBodyAt nativeTelemetryEmptyErrorPayloadExtentAt) drainScratch0 (drainSet drainResult 1 (drainReturn (drainLabel b"drain-append-refused" (drainSet drainResult 0 (drainStore64 drainArgument0 publicationReadyAt drainResult (drainLabel b"drain-append-inaccessible" (drainSet drainResult 0 (drainReturn drainEnd)))))))))))))))))))))))))))))))))))))))))))) (branch TelemetryDrainCommitTagRoutine ordinaryCapacity reservedCapacity role tag . (drainCompareImmediate drainArgument2 4 (drainJumpIf (constructor TelemetryDrainCondition TelemetryDrainAbove) b"route-tag-invalid" (drainCompareImmediate drainArgument2 1 (drainJumpIf (constructor TelemetryDrainCondition TelemetryDrainNotZero) b"route-tag-not-queued" (drainCompareImmediate drainArgument3 (telemetryDispatchTagsBytes ordinaryCapacity reservedCapacity) (drainJumpIf (constructor TelemetryDrainCondition TelemetryDrainNotZero) b"route-tag-invalid" (drainLoad drainResult drainArgument0 captureOrdinaryCapacityAt (drainCompareImmediate drainResult ordinaryCapacity (drainJumpIf (constructor TelemetryDrainCondition TelemetryDrainNotZero) b"route-tag-invalid" (drainLoad drainResult drainArgument0 captureReservedCapacityAt (drainCompareImmediate drainResult reservedCapacity (drainJumpIf (constructor TelemetryDrainCondition TelemetryDrainNotZero) b"route-tag-invalid" (drainLoad drainResult drainArgument0 (aosChoose Nat role captureReservedUsedAt captureOrdinaryUsedAt) (drainCompareImmediate drainResult 0 (drainJumpIf (constructor TelemetryDrainCondition TelemetryDrainZero) b"route-tag-invalid" (drainCompareImmediate drainResult (aosChoose Nat role reservedCapacity ordinaryCapacity) (drainJumpIf (constructor TelemetryDrainCondition TelemetryDrainAbove) b"route-tag-invalid" (drainSet drainScratch0 1 (drainSubtract drainResult drainScratch0 (drainAddImmediate drainResult (naturalMultiply role ordinaryCapacity) (drainMultiplyImmediate drainResult captureWordBytes (drainAdd drainResult drainArgument1 (drainSet drainScratch0 tag (drainStore64 drainResult 0 drainScratch0 (drainSet drainResult 1 (drainReturn (drainLabel b"route-tag-invalid" (drainSet drainResult 4 (drainReturn (drainLabel b"route-tag-not-queued" (drainMove drainResult drainArgument2 (drainReturn drainEnd))))))))))))))))))))))))))))))))) (branch TelemetryDrainReadTagRoutine ordinaryCapacity reservedCapacity routes . (drainCompareImmediate drainArgument4 (telemetryDispatchTagsBytes ordinaryCapacity reservedCapacity) (drainJumpIf (constructor TelemetryDrainCondition TelemetryDrainNotZero) b"route-read-invalid" (drainCompare drainArgument1 drainArgument2 (drainJumpIf (constructor TelemetryDrainCondition TelemetryDrainBelow) b"route-read-invalid" (drainMove drainResult drainArgument1 (drainSubtract drainResult drainArgument2 (drainSet drainArgument2 0 (drainSet drainScratch0 captureRecordBytes (drainDivide drainScratch0 (drainCompareImmediate drainArgument2 0 (drainJumpIf (constructor TelemetryDrainCondition TelemetryDrainNotZero) b"route-read-invalid" (drainCompareImmediate drainResult (naturalAdd ordinaryCapacity reservedCapacity) (drainJumpIf (constructor TelemetryDrainCondition TelemetryDrainAbove) b"route-read-invalid" (drainJumpIf (constructor TelemetryDrainCondition TelemetryDrainZero) b"route-read-invalid" (drainMultiplyImmediate drainResult captureWordBytes (drainAdd drainResult drainArgument3 (drainLoad drainResult drainResult 0 (drainAllowedTagsWith routes (drainLabel b"route-read-valid" (drainStore64 drainArgument5 0 drainResult (drainSet drainResult 1 (drainReturn (drainLabel b"route-read-invalid" (drainSet drainResult 0 (drainStore64 drainArgument0 publicationReadyAt drainResult (drainStore64 drainArgument5 0 drainResult (drainReturn drainEnd)))))))))))))))))))))))))))) (branch TelemetryDrainMatchTagRoutine tag . (drainLoad drainResult drainArgument0 0 (drainCompareImmediate drainResult tag (drainJumpIf (constructor TelemetryDrainCondition TelemetryDrainNotZero) b"route-unmatched" (drainSet drainResult 1 (drainReturn (drainLabel b"route-unmatched" (drainSet drainResult 0 (drainReturn drainEnd)))))))))))))))))