module Runtime.NativeTelemetryValue

import Compiler.MachineX86Native
import Compiler.MachineX86NativeAssembly
import Observe.Value
import Runtime.NativeTelemetrySeal
import Runtime.TelemetryCapture
import Runtime.TelemetryValue
import Std.Natural
import Runtime.TelemetryValueRoutine
import Runtime.NativeWordDigest

-- System V realization of the shared formatter algorithm. The original
-- register assignment and instruction encodings are intentionally preserved.
def valueX86Compare =
  (lambda unrestricted left : (family X86NativeRegister64) .
    (lambda unrestricted right : (family X86NativeRegister64) .
      (digestEmit (constructor X86NativeInstruction X86NativeCompareRegister64 right left))))

def valueX86Subtract =
  (lambda unrestricted left : (family X86NativeRegister64) .
    (lambda unrestricted right : (family X86NativeRegister64) .
      (digestEmit (constructor X86NativeInstruction X86NativeSubtractRegister64 right left))))

def valueX86Divide =
  (lambda unrestricted divisor : (family X86NativeRegister64) .
    (digestEmit (constructor X86NativeInstruction X86NativeDivideRegister64Unsigned divisor)))

def valueX86JumpIf =
  (lambda unrestricted condition : (family TelemetryValueCondition) .
    (digestJumpIf
      (eliminate
        TelemetryValueCondition
        (lambda unrestricted current : (family TelemetryValueCondition) .
          (family X86NativeCondition))
        condition
        (branch TelemetryValueZero . (constructor X86NativeCondition X86NativeConditionZero))
        (branch TelemetryValueNotZero . (constructor X86NativeCondition X86NativeConditionNotZero))
        (branch TelemetryValueBelow . (constructor X86NativeCondition X86NativeConditionBelow))
        (branch TelemetryValueAbove . (constructor X86NativeCondition X86NativeConditionAbove)))))

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

def valueX86Backend =
  (constructor
    TelemetryValueBackend
    TelemetryValueBackendValue
    (family X86NativeAssembly)
    (family X86NativeRegister64)
    digestLoad64
    digestLoad8
    digestStore8
    digestMov
    digestMovImm
    digestCmpImm
    valueX86Compare
    digestAdd
    digestAddImm
    valueX86Subtract
    digestShr
    digestAndImm
    valueX86Divide
    valueX86JumpIf
    valueX86Jump
    digestLabel
    digestReturn
    digestEnd
    digestRAX
    digestRDI
    digestRSI
    digestRDX
    digestRCX
    digestR8
    digestR9
    digestR10
    digestR11)

def nativeTelemetryDecimalCellRoutine =
  (lambda unrestricted signed : Nat .
    (aosChoose
      Bytes
      (naturalLessOrEqual signed 1)
      (compiler-native-encode
        (family X86NativeAssembly)
        (telemetryValueAssemblyFor
          (family X86NativeAssembly)
          (family X86NativeRegister64)
          valueX86Backend
          (constructor TelemetryValueRoutineKind TelemetryValueDecimalRoutine signed)))
      b""))

def nativeTelemetryHexCellRoutine =
  (lambda unrestricted width : Nat .
    (lambda unrestricted reverse : Nat .
      (aosChoose
        Bytes
        (naturalAnd
          (naturalNonzero width)
          (naturalAnd
            (naturalLessOrEqual width telemetryHexSourceMaximumBytes)
            (naturalLessOrEqual reverse 1)))
        (compiler-native-encode
          (family X86NativeAssembly)
          (telemetryValueAssemblyFor
            (family X86NativeAssembly)
            (family X86NativeRegister64)
            valueX86Backend
            (constructor TelemetryValueRoutineKind TelemetryValueHexRoutine width reverse)))
        b"")))

def nativeTelemetryDecimalWordCellRoutine =
  (lambda unrestricted signed : Nat .
    (lambda unrestricted offset : Nat .
      (aosChoose
        Bytes
        (naturalAnd
          (naturalLessOrEqual signed 1)
          (naturalLessOrEqual (naturalAdd offset captureWordBytes) captureRecordBytes))
        (compiler-native-encode
          (family X86NativeAssembly)
          (telemetryValueAssemblyFor
            (family X86NativeAssembly)
            (family X86NativeRegister64)
            valueX86Backend
            (constructor TelemetryValueRoutineKind TelemetryValueWordRoutine signed offset)))
        b"")))

def nativeTelemetryHexSliceCellRoutine =
  (lambda unrestricted width : Nat .
    (lambda unrestricted reverse : Nat .
      (lambda unrestricted offset : Nat .
        (aosChoose
          Bytes
          (naturalAnd
            (naturalNonzero width)
            (naturalAnd
              (naturalLessOrEqual width telemetryHexSourceMaximumBytes)
              (naturalAnd
                (naturalLessOrEqual reverse 1)
                (naturalLessOrEqual (naturalAdd offset width) captureRecordBytes))))
          (compiler-native-encode
            (family X86NativeAssembly)
            (telemetryValueAssemblyFor
              (family X86NativeAssembly)
              (family X86NativeRegister64)
              valueX86Backend
              (constructor
                TelemetryValueRoutineKind
                TelemetryValueSliceRoutine
                width
                reverse
                offset)))
          b""))))