module Runtime.NativeObservedJournal

import Data.Bytes
import Model.Word64
import Observe.Value
import Runtime.NativeFileStatus
import Runtime.NativeLaunchRecipeLoad
import Runtime.NativePhysicalProgram
import Runtime.NativeTelemetryPolicy
import Runtime.NativeTelemetryValue
import Runtime.TelemetryCapture
import Runtime.TelemetryDrain
import Runtime.TelemetryIdentity
import Runtime.TelemetryPolicy
import Runtime.TelemetryValue
import Std.Natural

-- One journal per actual producer epoch. Rendering reads the recorder-owned
-- identity only after initialization; application source never receives access
-- to that private arena. Exclusive creation prevents overwriting another run.
-- The quoted hex formatter supplies the digits; openat skips the opening quote
-- and a constant suffix replaces the closing quote. No second entropy draw or
-- PID/time-derived identity is introduced merely to choose a filename.
def nativeObservedJournalSuffix : Bytes =
  b".alphatel\x00"

def nativeObservedJournalNameBytes : Nat =
  (naturalAdd
    (naturalSaturatingSubtract (telemetryHexCellBytes telemetryIdentityBytes) 1)
    (bytes-length nativeObservedJournalSuffix))

-- fstat's result is not interpreted. This is the conservative Linux scratch
-- extent already used by both maintained host ABIs; it is kept disjoint from
-- the filename and recorder storage even when an open fails.
def nativeObservedJournalStatBytes : Nat =
  nativeFileStatusScratchBytes

def nativeObservedJournalStatAt =
  (lambda unrestricted pathAt : Nat . (naturalAdd pathAt nativeObservedJournalNameBytes))

def nativeObservedJournalBytes : Nat =
  (naturalAdd nativeObservedJournalNameBytes nativeObservedJournalStatBytes)

def nativeObservedJournalAdmission =
  (lambda unrestricted applicationBytes : Nat .
    (lambda unrestricted applicationSlots : Nat .
      (lambda unrestricted pathAt : Nat .
        (lambda unrestricted fileSlot : Nat .
          (lambda unrestricted directorySlot : Nat .
            (naturalAnd
              (telemetryRangeFits pathAt nativeObservedJournalBytes applicationBytes)
              (naturalAnd
                (naturalLess fileSlot applicationSlots)
                (naturalAnd
                  (naturalLess directorySlot applicationSlots)
                  (naturalIsZero (naturalEqual fileSlot directorySlot))))))))))

def nativeObservedJournalCall =
  (lambda unrestricted syscall : Nat .
    (lambda unrestricted arguments : (family NativePhysicalArguments) .
      (lambda unrestricted payload : Bytes .
        (lambda unrestricted resultSlot : Nat .
          (lambda unrestricted error : Bytes .
            (nativeLaunchRecipeCommand
              (constructor
                NativePhysicalOperation
                NativePhysicalSystemCall
                (nativeLaunchRecipeImmediate syscall)
                arguments
                payload
                (nativeLaunchRecipeStore resultSlot))
              error))))))

def nativeObservedJournalCheckDescriptor =
  (lambda unrestricted descriptorSlot : Nat .
    (lambda unrestricted pathAt : Nat .
      (lambda unrestricted workSlot : Nat .
        (lambda unrestricted error : Bytes .
          (lambda unrestricted tail : (family NativePhysicalCommands) .
            (nativeObservedJournalCall
              5
              (nativeLaunchRecipeArguments
                (nativeLaunchRecipeSlotValue descriptorSlot)
                (nativeTelemetryPolicyState (nativeObservedJournalStatAt pathAt))
                (nativeLaunchRecipeImmediate 0)
                (nativeLaunchRecipeImmediate 0))
              b""
              workSlot
              error
              (nativeLaunchRecipeAssertEqual
                (nativeLaunchRecipeSlotValue workSlot)
                (nativeLaunchRecipeImmediate 0)
                error
                tail)))))))

def nativeObservedJournalForCapacities =
  (lambda unrestricted applicationBytes : Nat .
    (lambda unrestricted ordinary : Nat .
      (lambda unrestricted reserved : Nat .
        (lambda unrestricted pathAt : Nat .
          (lambda unrestricted fileSlot : Nat .
            (lambda unrestricted directorySlot : Nat .
              (lambda unrestricted workSlot : Nat .
                (lambda unrestricted identity : Bytes .
                  (lambda unrestricted tail : (family NativePhysicalCommands) .
                    (nativeLaunchRecipeCommand
                      (constructor
                        NativePhysicalOperation
                        NativePhysicalMachineRoutine
                        (nativeTelemetryHexCellRoutine telemetryIdentityBytes 0)
                        (nativeLaunchRecipeArguments
                          (nativeTelemetryPolicyState
                            (naturalAdd
                              (captureIdentityAt applicationBytes ordinary reserved)
                              (telemetryIdentityOffset telemetryProducerEpochIndex)))
                          (nativeTelemetryPolicyState pathAt)
                          (nativeLaunchRecipeImmediate telemetryIdentityBytes)
                          (nativeLaunchRecipeImmediate
                            (telemetryHexCellBytes telemetryIdentityBytes)))
                        (nativeLaunchRecipeStore workSlot))
                      identity
                      (nativeLaunchRecipeAssertEqual
                        (nativeLaunchRecipeSlotValue workSlot)
                        (nativeLaunchRecipeImmediate 0)
                        b"telemetry:journal-name-refused"
                        (nativeLaunchRecipeCommand
                          (constructor
                            NativePhysicalOperation
                            NativePhysicalCopyPayloadToState
                            (modelWord64FromNaturalTruncated
                              (naturalAdd
                                pathAt
                                (naturalSaturatingSubtract
                                  (telemetryHexCellBytes telemetryIdentityBytes)
                                  1)))
                            (modelWord64FromNaturalTruncated
                              (bytes-length nativeObservedJournalSuffix))
                            nativeObservedJournalSuffix)
                          identity
                          (nativeObservedJournalCall
                            257
                            (nativeLaunchRecipeArguments
                              (nativeLaunchRecipeImmediate 18446744073709551516)
                              (constructor
                                NativePhysicalOperand
                                NativePhysicalPayloadAddress
                                modelWord64Zero)
                              (nativeLaunchRecipeImmediate 65536)
                              (nativeLaunchRecipeImmediate 0))
                            b".\x00"
                            directorySlot
                            identity
                            (nativeObservedJournalCheckDescriptor
                              directorySlot
                              pathAt
                              workSlot
                              b"telemetry:journal-directory-open"
                              (nativeObservedJournalCall
                                257
                                (nativeLaunchRecipeArguments
                                  (nativeLaunchRecipeSlotValue directorySlot)
                                  (nativeTelemetryPolicyState (succ pathAt))
                                  (nativeLaunchRecipeImmediate 1217)
                                  (nativeLaunchRecipeImmediate 384))
                                b""
                                fileSlot
                                identity
                                (nativeObservedJournalCheckDescriptor
                                  fileSlot
                                  pathAt
                                  workSlot
                                  b"telemetry:journal-open"
                                  tail))))))))))))))))

def nativeObservedJournalCommands =
  (lambda unrestricted applicationBytes : Nat .
    (lambda unrestricted plan : (family TelemetryRoutedPolicyPlan) .
      (lambda unrestricted pathAt : Nat .
        (lambda unrestricted fileSlot : Nat .
          (lambda unrestricted directorySlot : Nat .
            (lambda unrestricted workSlot : Nat .
              (lambda unrestricted identity : Bytes .
                (lambda unrestricted tail : (family NativePhysicalCommands) .
                  (eliminate
                    TelemetryRoutedPolicyPlan
                    (lambda unrestricted current : (family TelemetryRoutedPolicyPlan) .
                      (family NativePhysicalCommands))
                    plan
                    (branch
                      TelemetryRoutedPolicyReady
                      policy
                      sites
                      drain
                      .
                      (eliminate
                        TelemetryDispatchPlan
                        (lambda unrestricted current : (family TelemetryDispatchPlan) .
                          (family NativePhysicalCommands))
                        drain
                        (branch
                          TelemetryDispatchReady
                          ordinary
                          reserved
                          ordinaryRoutes
                          reservedRoutes
                          ordinaryPlan
                          reservedPlan
                          descriptors
                          bound
                          .
                          (nativeObservedJournalForCapacities
                            applicationBytes
                            ordinary
                            reserved
                            pathAt
                            fileSlot
                            directorySlot
                            workSlot
                            identity
                            tail))
                        (branch
                          TelemetryDispatchRefused
                          reason
                          .
                          (constructor NativePhysicalCommands NativePhysicalCommandsEnd))))
                    (branch
                      TelemetryRoutedPolicyRefused
                      reason
                      .
                      (constructor NativePhysicalCommands NativePhysicalCommandsEnd)))))))))))

-- The caller supplies a public scratch result slot for cleanup; private
-- recorder work slots are never exposed as application capabilities.
def nativeObservedJournalClose =
  (lambda unrestricted descriptorSlot : Nat .
    (lambda unrestricted workSlot : Nat .
      (lambda unrestricted error : Bytes .
        (lambda unrestricted tail : (family NativePhysicalCommands) .
          (nativeObservedJournalCall
            3
            (nativeLaunchRecipeArguments
              (nativeLaunchRecipeSlotValue descriptorSlot)
              (nativeLaunchRecipeImmediate 0)
              (nativeLaunchRecipeImmediate 0)
              (nativeLaunchRecipeImmediate 0))
            b""
            workSlot
            error
            (nativeLaunchRecipeAssertEqual
              (nativeLaunchRecipeSlotValue workSlot)
              (nativeLaunchRecipeImmediate 0)
              error
              tail))))))