module Runtime.NativeTelemetryRecord

import Compiler.MachineX86Native
import Compiler.MachineX86NativeAssembly
import Data.Bytes
import Model.Parameter
import Model.Word64
import Observe.Value
import Runtime.NativeLaunchRecipeLoad
import Runtime.NativePhysicalProgram
import Runtime.NativeTelemetry
import Runtime.NativeTelemetrySeal
import Runtime.NativeTelemetryValue
import Runtime.TelemetryCapture
import Runtime.TelemetryIdentity
import Runtime.TelemetryRecord
import Runtime.TelemetryRecordRoutine
import Runtime.TelemetryValue
import Std.Natural
import Runtime.NativeWordDigest

-- System V realization of the shared read-only admission algorithm. Keep
-- register roles and encodings stable while both targets share the semantics.
def recordX86Backend =
  (constructor
    TelemetryRecordBackend
    TelemetryRecordBackendValue
    (family X86NativeAssembly)
    (family X86NativeRegister64)
    digestLoad64
    digestOr
    digestCmpImm
    (digestJumpIf (constructor X86NativeCondition X86NativeConditionZero))
    (digestJumpIf (constructor X86NativeCondition X86NativeConditionBelow))
    digestMovImm
    digestLabel
    digestReturn
    digestEnd
    digestRAX
    digestR10
    digestRDI
    digestRSI
    digestRCX
    digestR8
    digestR9)

def recordAdmissionAssembly =
  (lambda unrestricted parts : (family TelemetryRecordParts) .
    (telemetryRecordAssemblyFor
      (family X86NativeAssembly)
      (family X86NativeRegister64)
      recordX86Backend
      (constructor TelemetryRecordRoutineKind TelemetryRecordAdmissionRoutine parts)))

def recordAdmissionRoutine =
  (lambda unrestricted parts : (family TelemetryRecordParts) .
    (compiler-native-encode (family X86NativeAssembly) (recordAdmissionAssembly parts)))

def nativeTelemetryRecordAdmissionRoutine =
  (lambda unrestricted program : (family TelemetryRecordPlan) .
    (eliminate
      TelemetryRecordPlan
      (lambda unrestricted current : (family TelemetryRecordPlan) . Bytes)
      program
      (branch TelemetryRecordReady parts template . (recordAdmissionRoutine parts))
      (branch TelemetryRecordRefused reason . b"")))

-- Reads only the caller's private rendering status, never an application value.
def recordStatusRoutine : Bytes =
  (compiler-native-encode
    (family X86NativeAssembly)
    (telemetryRecordAssemblyFor
      (family X86NativeAssembly)
      (family X86NativeRegister64)
      recordX86Backend
      (constructor TelemetryRecordRoutineKind TelemetryRecordStatusRoutine)))

def recordState =
  (lambda unrestricted offset : Nat .
    (constructor
      NativePhysicalOperand
      NativePhysicalStateAddress
      (modelWord64FromNaturalTruncated offset)))

def recordCellCommand =
  (lambda unrestricted routine : Bytes .
    (lambda unrestricted source : (family NativePhysicalOperand) .
      (lambda unrestricted destination : Nat .
        (lambda unrestricted sourceExtent : Nat .
          (lambda unrestricted destinationExtent : Nat .
            (lambda unrestricted identity : Bytes .
              (nativeLaunchRecipeCommand
                (constructor
                  NativePhysicalOperation
                  NativePhysicalMachineRoutine
                  routine
                  (constructor
                    NativePhysicalArguments
                    NativePhysicalArgumentsValue
                    source
                    (recordState destination)
                    (nativeLaunchRecipeImmediate sourceExtent)
                    (nativeLaunchRecipeImmediate destinationExtent)
                    (nativeLaunchRecipeImmediate 0)
                    (nativeLaunchRecipeImmediate 0))
                  (constructor NativePhysicalResultBinding NativePhysicalDiscardResult))
                identity)))))))

-- Offsets are accumulated from the very pieces copied into the output. No
-- caller has a second field-offset table. Admitted field shapes/constant
-- extents make formatting total for all captured machine words. References
-- were validated before this stage and cannot change during the drain.
def recordPatchCommands =
  (lambda unrestricted parts : (family TelemetryRecordParts) .
    (lambda unrestricted source : (family NativePhysicalOperand) .
      (lambda unrestricted identities : (family NativePhysicalOperand) .
        (lambda unrestricted identity : Bytes .
          (eliminate
            TelemetryRecordParts
            (lambda unrestricted current : (family TelemetryRecordParts) .
              (pi unrestricted at : Nat .
                (pi unrestricted commands : (family NativePhysicalCommands) .
                  (family NativePhysicalCommands))))
            parts
            (branch
              TelemetryRecordEnd
              .
              (lambda unrestricted at : Nat .
                (lambda unrestricted commands : (family NativePhysicalCommands) . commands)))
            (branch
              TelemetryRecordLiteral
              bytes
              tail
              induction
              .
              (lambda unrestricted at : Nat .
                (lambda unrestricted commands : (family NativePhysicalCommands) .
                  (induction (naturalAdd at (bytes-length bytes)) commands))))
            (branch
              TelemetryRecordDecimal
              signed
              offset
              tail
              induction
              .
              (lambda unrestricted at : Nat .
                (lambda unrestricted commands : (family NativePhysicalCommands) .
                  (recordCellCommand
                    (nativeTelemetryDecimalWordCellRoutine signed offset)
                    source
                    at
                    captureRecordBytes
                    telemetryDecimalCellBytes
                    identity
                    (induction (naturalAdd at telemetryDecimalCellBytes) commands)))))
            (branch
              TelemetryRecordHex
              sourceKind
              offset
              width
              reverse
              nonzero
              tail
              induction
              .
              (lambda unrestricted at : Nat .
                (lambda unrestricted commands : (family NativePhysicalCommands) .
                  (recordCellCommand
                    (nativeTelemetryHexSliceCellRoutine width reverse offset)
                    (aosChoose (family NativePhysicalOperand) sourceKind identities source)
                    at
                    (aosChoose Nat sourceKind telemetryIdentitySetBytes captureRecordBytes)
                    (telemetryHexCellBytes width)
                    identity
                    (induction (naturalAdd at (telemetryHexCellBytes width)) commands))))))))))

-- A declaration derives its entire envelope, including identity and sequence
-- cells. On refusal, status is four and prior event bytes remain unchanged;
-- callers must not publish those stale bytes. Success is zero, not a durable
-- acknowledgement. The arena's status word and event region have one owner.
def recordRenderCommands =
  (lambda unrestricted parts : (family TelemetryRecordParts) .
    (lambda unrestricted bytes : Bytes .
      (lambda unrestricted source : (family NativePhysicalOperand) .
        (lambda unrestricted identities : (family NativePhysicalOperand) .
          (lambda unrestricted arenaAt : Nat .
            (lambda unrestricted resultSlot : Nat .
              (lambda unrestricted identity : Bytes .
                (lambda unrestricted tail : (family NativePhysicalCommands) .
                  (let unrestricted destination =
                    (naturalAdd arenaAt telemetryRecordAt)
                    in
                    (nativeLaunchRecipeCommand
                      (constructor
                        NativePhysicalOperation
                        NativePhysicalStoreWord64
                        (recordState arenaAt)
                        (nativeLaunchRecipeImmediate 4))
                      identity
                      (nativeLaunchRecipeCommand
                        (constructor
                          NativePhysicalOperation
                          NativePhysicalMachineRoutine
                          (recordAdmissionRoutine parts)
                          (constructor
                            NativePhysicalArguments
                            NativePhysicalArgumentsValue
                            source
                            identities
                            (recordState destination)
                            (nativeLaunchRecipeImmediate captureRecordBytes)
                            (nativeLaunchRecipeImmediate telemetryIdentitySetBytes)
                            (nativeLaunchRecipeImmediate (bytes-length bytes)))
                          (nativeLaunchRecipeStore resultSlot))
                        identity
                        (nativeLaunchRecipeCommand
                          (constructor
                            NativePhysicalOperation
                            NativePhysicalRepeatBeginCounted
                            (nativeLaunchRecipeSlotValue resultSlot))
                          identity
                          (nativeLaunchRecipeCommand
                            (constructor
                              NativePhysicalOperation
                              NativePhysicalCopyPayloadToState
                              (modelWord64FromNaturalTruncated destination)
                              (modelWord64FromNaturalTruncated (bytes-length bytes))
                              bytes)
                            identity
                            (recordPatchCommands
                              parts
                              source
                              identities
                              identity
                              destination
                              (nativeLaunchRecipeCommand
                                (constructor
                                  NativePhysicalOperation
                                  NativePhysicalStoreWord64
                                  (recordState arenaAt)
                                  (nativeLaunchRecipeImmediate 0))
                                identity
                                (nativeLaunchRecipeCommand
                                  (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
                                  identity
                                  (nativeLaunchRecipeCommand
                                    (constructor
                                      NativePhysicalOperation
                                      NativePhysicalMachineRoutine
                                      recordStatusRoutine
                                      (nativeLaunchRecipeArguments
                                        (recordState arenaAt)
                                        (nativeLaunchRecipeImmediate 0)
                                        (nativeLaunchRecipeImmediate 0)
                                        (nativeLaunchRecipeImmediate 0))
                                      (nativeLaunchRecipeStore resultSlot))
                                    identity
                                    tail)))))))))))))))))

def nativeTelemetryRecordCommands =
  (lambda unrestricted program : (family TelemetryRecordPlan) .
    (lambda unrestricted source : (family NativePhysicalOperand) .
      (lambda unrestricted identities : (family NativePhysicalOperand) .
        (lambda unrestricted arenaAt : Nat .
          (lambda unrestricted resultSlot : Nat .
            (lambda unrestricted identity : Bytes .
              (lambda unrestricted tail : (family NativePhysicalCommands) .
                (eliminate
                  TelemetryRecordPlan
                  (lambda unrestricted current : (family TelemetryRecordPlan) .
                    (family NativePhysicalCommands))
                  program
                  (branch
                    TelemetryRecordReady
                    parts
                    template
                    .
                    (recordRenderCommands
                      parts
                      template
                      source
                      identities
                      arenaAt
                      resultSlot
                      identity
                      tail))
                  (branch
                    TelemetryRecordRefused
                    reason
                    .
                    (nativeLaunchRecipeCommand
                      (constructor
                        NativePhysicalOperation
                        NativePhysicalMachineRoutine
                        b""
                        (nativeLaunchRecipeArguments
                          source
                          identities
                          (recordState arenaAt)
                          (nativeLaunchRecipeImmediate 0))
                        (nativeLaunchRecipeStore resultSlot))
                      identity
                      tail))))))))))