module Runtime.NativeTelemetryCapture

import Compiler.MachineX86Native
import Compiler.MachineX86NativeAssembly
import Model.Word64
import Runtime.NativeLaunchRecipeLoad
import Runtime.NativePhysicalProgram
import Observe.Value
import Runtime.TelemetryCapture
import Runtime.TelemetryCaptureRoutine
import Std.Natural

-- System V: control, queue, eight values, selected, reserved, queue extent.
-- Single producer, no concurrent drain. All acquisition uses caller-saved
-- registers and performs no syscall, hashing, formatting, or allocation.
-- Control policy is immutable to the application by the arena certificate.
-- A pending return leaves the queue/control unchanged. The caller must retain
-- the pending values and choose retry/pause/failure at its declared boundary;
-- this acquisition primitive cannot silently change application semantics.
-- Extent and overflow checks precede mutations. Return codes match
-- Observe.Capture; a queued return never claims persistence.
def captureRAX =
  (constructor X86NativeRegister64 X86NativeRAX)

def captureRCX =
  (constructor X86NativeRegister64 X86NativeRCX)

def captureRDX =
  (constructor X86NativeRegister64 X86NativeRDX)

def captureRSI =
  (constructor X86NativeRegister64 X86NativeRSI)

def captureRDI =
  (constructor X86NativeRegister64 X86NativeRDI)

def captureR8 =
  (constructor X86NativeRegister64 X86NativeR8)

def captureR9 =
  (constructor X86NativeRegister64 X86NativeR9)

def captureR10 =
  (constructor X86NativeRegister64 X86NativeR10)

def captureR11 =
  (constructor X86NativeRegister64 X86NativeR11)

def captureEmit =
  (lambda unrestricted instruction : (family X86NativeInstruction) .
    (lambda unrestricted tail : (family X86NativeAssembly) .
      (constructor X86NativeAssembly X86NativeAssemblyEmit instruction tail)))

def captureLabel =
  (lambda unrestricted name : Bytes .
    (lambda unrestricted tail : (family X86NativeAssembly) .
      (constructor X86NativeAssembly X86NativeAssemblyLabel name tail)))

def captureJump =
  (lambda unrestricted name : Bytes .
    (lambda unrestricted tail : (family X86NativeAssembly) .
      (constructor X86NativeAssembly X86NativeAssemblyJump name tail)))

def captureJumpIf =
  (lambda unrestricted condition : (family X86NativeCondition) .
    (lambda unrestricted name : Bytes .
      (lambda unrestricted tail : (family X86NativeAssembly) .
        (constructor X86NativeAssembly X86NativeAssemblyJumpCondition condition name tail))))

def captureLoad =
  (lambda unrestricted destination : (family X86NativeRegister64) .
    (lambda unrestricted base : (family X86NativeRegister64) .
      (lambda unrestricted offset : Nat .
        (captureEmit
          (constructor
            X86NativeInstruction
            X86NativeLoadMemory64
            destination
            base
            (x86NativeDisplacement32FromNatural offset))))))

def captureStore =
  (lambda unrestricted base : (family X86NativeRegister64) .
    (lambda unrestricted offset : Nat .
      (lambda unrestricted source : (family X86NativeRegister64) .
        (captureEmit
          (constructor
            X86NativeInstruction
            X86NativeStoreMemory64
            base
            (x86NativeDisplacement32FromNatural offset)
            source)))))

def captureMove =
  (lambda unrestricted destination : (family X86NativeRegister64) .
    (lambda unrestricted source : (family X86NativeRegister64) .
      (captureEmit (constructor X86NativeInstruction X86NativeMoveRegister64 source destination))))

def captureAdd =
  (lambda unrestricted destination : (family X86NativeRegister64) .
    (lambda unrestricted source : (family X86NativeRegister64) .
      (captureEmit (constructor X86NativeInstruction X86NativeAddRegister64 source destination))))

def captureCompare =
  (lambda unrestricted left : (family X86NativeRegister64) .
    (lambda unrestricted right : (family X86NativeRegister64) .
      (captureEmit (constructor X86NativeInstruction X86NativeCompareRegister64 right left))))

def captureCompareImmediate =
  (lambda unrestricted register : (family X86NativeRegister64) .
    (lambda unrestricted value : Nat .
      (captureEmit
        (constructor
          X86NativeInstruction
          X86NativeCompareImmediate64
          register
          (x86NativeImmediate32FromNatural value)))))

def captureSet =
  (lambda unrestricted register : (family X86NativeRegister64) .
    (lambda unrestricted value : Nat .
      (captureEmit
        (constructor
          X86NativeInstruction
          X86NativeMoveImmediate32
          register
          (x86NativeImmediate32FromNatural value)))))

def captureIncrement =
  (lambda unrestricted register : (family X86NativeRegister64) .
    (captureEmit
      (constructor
        X86NativeInstruction
        X86NativeAddImmediate64
        register
        (x86NativeImmediate32FromNatural 1))))

def captureReturnCode =
  (lambda unrestricted code : Nat .
    (lambda unrestricted tail : (family X86NativeAssembly) .
      (captureSet
        captureRAX
        code
        (captureEmit (constructor X86NativeInstruction X86NativeReturn) tail))))

-- CMP r64, imm32 sign-extends all ones to the unsigned 64-bit maximum.
-- This is an ISA encoding operand, not a pasted application quantity.
def captureMaximumCounterImmediate : Nat =
  0xffffffff

def captureCompareMaximum =
  (lambda unrestricted register : (family X86NativeRegister64) .
    (captureCompareImmediate register captureMaximumCounterImmediate))

def captureScale =
  (lambda unrestricted register : (family X86NativeRegister64) .
    (lambda unrestricted stride : Nat .
      (captureEmit
        (constructor
          X86NativeInstruction
          X86NativeMultiplyImmediate64
          register
          (x86NativeImmediate32FromNatural stride)))))

def captureProduct =
  (captureEmit (constructor X86NativeInstruction X86NativeMultiplyRegister64Unsigned captureR10))

def captureBackendJumpIf =
  (lambda unrestricted condition : (family TelemetryCaptureCondition) .
    (captureJumpIf
      (eliminate
        TelemetryCaptureCondition
        (lambda unrestricted current : (family TelemetryCaptureCondition) .
          (family X86NativeCondition))
        condition
        (branch TelemetryCaptureZero . (constructor X86NativeCondition X86NativeConditionZero))
        (branch
          TelemetryCaptureNotZero
          .
          (constructor X86NativeCondition X86NativeConditionNotZero))
        (branch TelemetryCaptureBelow . (constructor X86NativeCondition X86NativeConditionBelow))
        (branch TelemetryCaptureAbove . (constructor X86NativeCondition X86NativeConditionAbove)))))

def captureX86Backend =
  (constructor
    TelemetryCaptureBackend
    TelemetryCaptureBackendValue
    (family X86NativeAssembly)
    (family X86NativeRegister64)
    captureLoad
    captureStore
    captureMove
    captureAdd
    captureCompare
    captureCompareImmediate
    captureCompareMaximum
    captureSet
    captureIncrement
    captureScale
    captureProduct
    captureReturnCode
    captureLabel
    captureJump
    captureBackendJumpIf
    (constructor X86NativeAssembly X86NativeAssemblyEnd)
    captureRAX
    captureRCX
    captureRDX
    captureRSI
    captureRDI
    captureR8
    captureR9
    captureR10
    captureR11)

def captureAssemblyPart0 =
  (telemetryCaptureAssemblyFor
    (family X86NativeAssembly)
    (family X86NativeRegister64)
    captureX86Backend)

def nativeTelemetryCaptureRoutine : Bytes =
  (eliminate
    X86NativeAssemblyResult
    (lambda unrestricted current : (family X86NativeAssemblyResult) . Bytes)
    (x86NativeAssemble captureAssemblyPart0)
    (branch X86NativeAssemblyEncoded code . code)
    (branch X86NativeAssemblyEncodeDuplicateLabel name . b"")
    (branch X86NativeAssemblyEncodeOffsetOverflow . b"")
    (branch X86NativeAssemblyMissingLabel name . b"")
    (branch X86NativeAssemblyDisplacementOutOfRange name . b""))

-- This constructor binds every pointer/extent to the same certified plan.
-- Invalid placements lower to an unavailable routine and fail artifact build;
-- unsupported host targets must refuse this x86 realization, never copy it.
def nativeTelemetryCaptureSelectedCommand =
  (lambda unrestricted applicationBytes : Nat .
    (lambda unrestricted ordinaryCapacity : Nat .
      (lambda unrestricted reservedCapacity : Nat .
        (lambda unrestricted selected : (family NativePhysicalOperand) .
          (lambda unrestricted reserved : Nat .
            (lambda unrestricted resultSlot : Nat .
              (lambda unrestricted identity : Bytes .
                (lambda unrestricted tail : (family NativePhysicalCommands) .
                  (nativeLaunchRecipeCommand
                    (constructor
                      NativePhysicalOperation
                      NativePhysicalMachineRoutine
                      (aosChoose
                        Bytes
                        (captureArenaCertificate applicationBytes ordinaryCapacity reservedCapacity)
                        nativeTelemetryCaptureRoutine
                        b"")
                      (constructor
                        NativePhysicalArguments
                        NativePhysicalArgumentsValue
                        (constructor
                          NativePhysicalOperand
                          NativePhysicalStateAddress
                          (modelWord64FromNaturalTruncated (captureControlAt applicationBytes)))
                        (constructor
                          NativePhysicalOperand
                          NativePhysicalStateAddress
                          (modelWord64FromNaturalTruncated (captureQueueAt applicationBytes)))
                        (constructor
                          NativePhysicalOperand
                          NativePhysicalStateAddress
                          (modelWord64FromNaturalTruncated
                            (captureValuesScratchAt
                              applicationBytes
                              ordinaryCapacity
                              reservedCapacity)))
                        selected
                        (nativeLaunchRecipeImmediate reserved)
                        (nativeLaunchRecipeImmediate
                          (captureQueueBytes ordinaryCapacity reservedCapacity)))
                      (nativeLaunchRecipeStore resultSlot))
                    identity
                    tail)))))))))

def nativeTelemetryCaptureCommand =
  (lambda unrestricted applicationBytes : Nat .
    (lambda unrestricted ordinaryCapacity : Nat .
      (lambda unrestricted reservedCapacity : Nat .
        (lambda unrestricted selected : Nat .
          (nativeTelemetryCaptureSelectedCommand
            applicationBytes
            ordinaryCapacity
            reservedCapacity
            (nativeLaunchRecipeImmediate selected))))))