module Runtime.NativeTelemetryPublication import Compiler.MachineX86Native import Compiler.MachineX86NativeAssembly import Data.Bytes import Model.Word64 import Observe.Value import Runtime.NativeLaunchRecipeLoad import Runtime.NativePhysicalProgram import Runtime.NativeTelemetry import Runtime.NativeTelemetryCapture import Runtime.NativeTelemetryIdentity import Runtime.NativeTelemetrySeal import Runtime.TelemetryCapture import Runtime.TelemetryIdentity import Runtime.TelemetryPublication import Runtime.TelemetryPublicationRoutine import Std.Natural import Runtime.NativeWordDigest -- Single-writer safe-boundary publication. Preparing copies occupied records, -- never unused capacity. Acquisition cannot run concurrently with prepare, -- sealing or commit. The plan certifies the capture, identity, padded body, -- record, zero-timespec and hash work areas together. -- Prepare ABI: control, queue, identities, publication arena, queue extent, -- publication extent. Commit ABI: control, publication arena, sink descriptor, -- sealed record, record length, containing-directory descriptor. -- -- A full write followed by file AND directory fsync permits reclamation. Any -- failed/short write or sync poisons this sink and retains the queue/cumulative -- counters: appending a retry behind a torn tail would corrupt the journal. -- The caller receives a decision and owns its declared optional/required -- capture response. Publication never exits the application on its behalf. -- This is x86-64 Linux acquisition of filesystem durability, not GPU capture. def publicationCompare = (lambda unrestricted left : (family X86NativeRegister64) . (lambda unrestricted right : (family X86NativeRegister64) . (digestEmit (constructor X86NativeInstruction X86NativeCompareRegister64 right left)))) def publicationSubtract = (lambda unrestricted left : (family X86NativeRegister64) . (lambda unrestricted right : (family X86NativeRegister64) . (digestEmit (constructor X86NativeInstruction X86NativeSubtractRegister64 right left)))) def publicationJump = (lambda unrestricted name : Bytes . (lambda unrestricted tail : (family X86NativeAssembly) . (constructor X86NativeAssembly X86NativeAssemblyJump name tail))) -- System V realization; syscall operations belong to the host adapter. def publicationX86JumpIf = (lambda unrestricted condition : (family TelemetryPublicationCondition) . (digestJumpIf (eliminate TelemetryPublicationCondition (lambda unrestricted current : (family TelemetryPublicationCondition) . (family X86NativeCondition)) condition (branch TelemetryPublicationZero . (constructor X86NativeCondition X86NativeConditionZero)) (branch TelemetryPublicationNotZero . (constructor X86NativeCondition X86NativeConditionNotZero)) (branch TelemetryPublicationBelow . (constructor X86NativeCondition X86NativeConditionBelow)) (branch TelemetryPublicationAbove . (constructor X86NativeCondition X86NativeConditionAbove))))) def publicationX86Write = (lambda unrestricted tail : (family X86NativeAssembly) . (digestMovImm digestRAX 1 (digestEmit (constructor X86NativeInstruction X86NativeSystemCall) tail))) def publicationX86Sync = (lambda unrestricted tail : (family X86NativeAssembly) . (digestMovImm digestRAX 74 (digestEmit (constructor X86NativeInstruction X86NativeSystemCall) tail))) def publicationX86Backend = (constructor TelemetryPublicationBackend TelemetryPublicationBackendValue (family X86NativeAssembly) (family X86NativeRegister64) digestMovImm digestMov digestLoad64 digestStore64 digestStore8 digestCmpImm publicationCompare publicationSubtract digestOr digestAdd digestAddImm digestMulImm digestShr publicationX86JumpIf publicationJump digestLabel digestReturn publicationX86Write publicationX86Sync digestEnd digestRAX digestRDI digestRSI digestRDX digestRCX digestR8 digestR9 digestR10 digestR11 digestR12 digestR13 digestR14 digestR15) def nativeTelemetryPublicationRoutineFor = (lambda unrestricted kind : (family TelemetryPublicationRoutineKind) . (compiler-native-encode (family X86NativeAssembly) (telemetryPublicationAssemblyFor (family X86NativeAssembly) (family X86NativeRegister64) publicationX86Backend kind))) -- A scalar snapshot fits in any admitted larger body bound. The typed drain -- can replace the copied scalar payload before sealing; this routine itself -- still prepares version-two scalar bytes and never claims typed admission. def nativeTelemetryPublicationPrepareRoutineForBody = (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted bodyBytes : Nat . (aosChoose Bytes (naturalAnd (naturalLessOrEqual (publicationBodyMaximumBytes ordinaryCapacity reservedCapacity) bodyBytes) (naturalLessOrEqual (publicationRecordBytes bodyBytes) publicationMaximumFrameBytes)) (nativeTelemetryPublicationRoutineFor (constructor TelemetryPublicationRoutineKind TelemetryPublicationPrepareRoutine ordinaryCapacity reservedCapacity bodyBytes)) b"")))) def nativeTelemetryPublicationPrepareRoutine = (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (nativeTelemetryPublicationPrepareRoutineForBody ordinaryCapacity reservedCapacity (publicationBodyMaximumBytes ordinaryCapacity reservedCapacity)))) -- Replaces version/length/padding in a prepared snapshot. The shared -- algorithm checks the exact arena before access and clears accessible -- readiness on refusal. This byte mechanism does not validate JSON meaning. def nativeTelemetryPublicationTypedPaddingRoutineForBody = (lambda unrestricted bodyBytes : Nat . (aosChoose Bytes (naturalAnd (naturalLessOrEqual publicationPayloadRecordsAt bodyBytes) (naturalLessOrEqual (publicationRecordBytes bodyBytes) publicationMaximumFrameBytes)) (nativeTelemetryPublicationRoutineFor (constructor TelemetryPublicationRoutineKind TelemetryPublicationTypedPaddingRoutine bodyBytes)) b"")) def nativeTelemetryPublicationCommitRoutine : Bytes = (nativeTelemetryPublicationRoutineFor (constructor TelemetryPublicationRoutineKind TelemetryPublicationCommitRoutine)) -- All external operands are declared host descriptors. The containing-directory -- descriptor must be the directory used to open the sink, not an unrelated -- descriptor whose fsync merely happens to succeed. def publicationStateAddress = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted relative : Nat . (constructor NativePhysicalOperand NativePhysicalStateAddress (modelWord64FromNaturalTruncated (naturalAdd (publicationBase applicationBytes ordinaryCapacity reservedCapacity) relative))))))) def publicationStateLoad = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted relative : Nat . (constructor NativePhysicalOperand NativePhysicalStateLoad64 (modelWord64FromNaturalTruncated (naturalAdd (publicationBase applicationBytes ordinaryCapacity reservedCapacity) relative))))))) def publicationCopyPayload = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted relative : Nat . (lambda unrestricted payload : Bytes . (lambda unrestricted identity : Bytes . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalCopyPayloadToState (modelWord64FromNaturalTruncated (naturalAdd (publicationBase applicationBytes ordinaryCapacity reservedCapacity) relative)) (modelWord64FromNaturalTruncated (bytes-length payload)) payload) identity))))))) def publicationSealAndCommitCommandsForBody = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted bodyBytes : Nat . (lambda unrestricted sink : (family NativePhysicalOperand) . (lambda unrestricted directory : (family NativePhysicalOperand) . (lambda unrestricted resultSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted (publicationStateLoad applicationBytes ordinaryCapacity reservedCapacity publicationReadyAt)) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine nativeTelemetrySealRoutine (constructor NativePhysicalArguments NativePhysicalArgumentsValue (publicationStateAddress applicationBytes ordinaryCapacity reservedCapacity publicationBodyAt) (publicationStateLoad applicationBytes ordinaryCapacity reservedCapacity publicationBlockCountAt) (publicationStateAddress applicationBytes ordinaryCapacity reservedCapacity (publicationRecordAtForBody bodyBytes)) (publicationStateLoad applicationBytes ordinaryCapacity reservedCapacity publicationBodyLengthAt) (publicationStateAddress applicationBytes ordinaryCapacity reservedCapacity (publicationZeroClockAtForBody bodyBytes)) (publicationStateAddress applicationBytes ordinaryCapacity reservedCapacity (publicationSealWorkAtForBody bodyBytes))) (constructor NativePhysicalResultBinding NativePhysicalDiscardResult)) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine nativeTelemetryPublicationCommitRoutine (constructor NativePhysicalArguments NativePhysicalArgumentsValue (constructor NativePhysicalOperand NativePhysicalStateAddress (modelWord64FromNaturalTruncated (captureControlAt applicationBytes))) (publicationStateAddress applicationBytes ordinaryCapacity reservedCapacity 0) sink (publicationStateAddress applicationBytes ordinaryCapacity reservedCapacity (publicationRecordAtForBody bodyBytes)) (publicationStateLoad applicationBytes ordinaryCapacity reservedCapacity publicationRecordLengthAt) directory) (nativeLaunchRecipeStore resultSlot)) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatEnd) identity tail))))))))))))) def publicationSealAndCommitCommands = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (publicationSealAndCommitCommandsForBody applicationBytes ordinaryCapacity reservedCapacity (publicationBodyMaximumBytes ordinaryCapacity reservedCapacity))))) def nativeTelemetryPublicationPrepareCommandsForBody = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted bodyBytes : Nat . (lambda unrestricted terminal : Nat . (lambda unrestricted resultSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (publicationCopyPayload applicationBytes ordinaryCapacity reservedCapacity publicationBodyAt publicationBodyPrefix identity (publicationCopyPayload applicationBytes ordinaryCapacity reservedCapacity (publicationRecordAtForBody bodyBytes) nativeTelemetryMagic identity (publicationCopyPayload applicationBytes ordinaryCapacity reservedCapacity (publicationZeroClockAtForBody bodyBytes) (dataBytesRepeatByte (byte 0) publicationZeroClockBytes) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalStoreWord64 (publicationStateAddress applicationBytes ordinaryCapacity reservedCapacity publicationReadyAt) (nativeLaunchRecipeImmediate 0)) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalStoreWord64 (publicationStateAddress applicationBytes ordinaryCapacity reservedCapacity publicationTerminalRequestAt) (nativeLaunchRecipeImmediate terminal)) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine (aosChoose Bytes (naturalAnd (naturalAnd (publicationStorageCertificateForBody applicationBytes ordinaryCapacity reservedCapacity bodyBytes) (naturalEqual captureControlBytes (bytes-length (nativeTelemetryEncodeCounters publicationEmptyCounters)))) (naturalLessOrEqual terminal 1)) (nativeTelemetryPublicationPrepareRoutineForBody ordinaryCapacity reservedCapacity bodyBytes) b"") (constructor NativePhysicalArguments NativePhysicalArgumentsValue (constructor NativePhysicalOperand NativePhysicalStateAddress (modelWord64FromNaturalTruncated (captureControlAt applicationBytes))) (constructor NativePhysicalOperand NativePhysicalStateAddress (modelWord64FromNaturalTruncated (captureQueueAt applicationBytes))) (constructor NativePhysicalOperand NativePhysicalStateAddress (modelWord64FromNaturalTruncated (captureIdentityAt applicationBytes ordinaryCapacity reservedCapacity))) (publicationStateAddress applicationBytes ordinaryCapacity reservedCapacity 0) (nativeLaunchRecipeImmediate (captureQueueBytes ordinaryCapacity reservedCapacity)) (nativeLaunchRecipeImmediate (publicationArenaBytesForBody bodyBytes))) (nativeLaunchRecipeStore resultSlot)) identity tail)))))))))))))) def nativeTelemetryPublicationCommandsForBody = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted bodyBytes : Nat . (lambda unrestricted terminal : Nat . (lambda unrestricted sink : (family NativePhysicalOperand) . (lambda unrestricted directory : (family NativePhysicalOperand) . (lambda unrestricted resultSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeTelemetryPublicationPrepareCommandsForBody applicationBytes ordinaryCapacity reservedCapacity bodyBytes terminal resultSlot identity (publicationSealAndCommitCommandsForBody applicationBytes ordinaryCapacity reservedCapacity bodyBytes sink directory resultSlot identity tail)))))))))))) def nativeTelemetryPublicationCommands = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (nativeTelemetryPublicationCommandsForBody applicationBytes ordinaryCapacity reservedCapacity (publicationBodyMaximumBytes ordinaryCapacity reservedCapacity)))))