module Runtime.TelemetryValue

import Data.Bytes
import Observe.Value
import Runtime.TelemetryCapture
import Std.Natural

-- A fixed-width JSON cell contains canonical quoted decimal digits followed
-- by JSON whitespace OUTSIDE the closing quote. Source integers therefore
-- stay canonical even as a value grows from one to twenty digits. Reserving
-- leading zeroes inside the string would violate AOS-JSON-004. These cells
-- are drain storage, not a new AOS value or acquisition representation.
def telemetryDecimalDigits : Nat =
  (bytes-length (naturalDecimalBytesWithin 20 aosU64Maximum))

def telemetryDecimalCellBytes : Nat =
  (naturalAdd 2 telemetryDecimalDigits)

def telemetryDecimalCell =
  (lambda unrestricted negative : Nat .
    (lambda unrestricted magnitude : Nat .
      (let unrestricted digits =
        (bytes-append
          (aosChoose Bytes negative b"-" b"")
          (naturalDecimalBytesWithin telemetryDecimalDigits magnitude))
        in
        (bytes-append
          b"\""
          (bytes-append
            digits
            (bytes-append
              b"\""
              (dataBytesRepeatByte
                (byte 32)
                (naturalSaturatingSubtract telemetryDecimalDigits (bytes-length digits)))))))))

def telemetryUnsignedCell =
  (lambda unrestricted value : Nat .
    (aosChoose Bytes (naturalLessOrEqual value aosU64Maximum) (telemetryDecimalCell 0 value) b""))

def telemetrySignedCell =
  (lambda unrestricted negative : Nat .
    (lambda unrestricted magnitude : Nat .
      (aosChoose
        Bytes
        (naturalAnd
          (naturalLessOrEqual negative 1)
          (aosChoose
            Nat
            negative
            (naturalAnd
              (naturalNonzero magnitude)
              (naturalLessOrEqual magnitude aosI64MinimumMagnitude))
            (naturalLessOrEqual magnitude aosI64Maximum)))
        (telemetryDecimalCell negative magnitude)
        b"")))

-- Hex cells retain fixed-width bytes: identities use memory order; float
-- bits use most-significant-byte first. The caller declares which operation
-- it needs. A numerical value is never inferred from a raw byte sequence.
def telemetryHexSourceMaximumBytes : Nat =
  captureValuesBytes

def telemetryHexCellBytes =
  (lambda unrestricted width : Nat . (naturalAdd 2 (naturalMultiply 2 width)))

def telemetryHexCell =
  (lambda unrestricted value : Bytes .
    (aosChoose
      Bytes
      (naturalAnd
        (naturalNonzero (bytes-length value))
        (naturalLessOrEqual (bytes-length value) telemetryHexSourceMaximumBytes))
      (bytes-append b"\"" (bytes-append (dataBytesRenderHex value) b"\""))
      b""))

-- Admission is checked before touching either buffer. Source and destination
-- disjointness is a caller layout obligation, certified alongside application
-- and publication storage. Codes: 0 admitted, 4 refused; no durability claim.
def telemetryHexCellAdmission =
  (lambda unrestricted width : Nat .
    (lambda unrestricted reverse : Nat .
      (lambda unrestricted sourceExtent : Nat .
        (lambda unrestricted destinationExtent : Nat .
          (aosChoose
            Nat
            (naturalAnd
              (naturalNonzero width)
              (naturalAnd
                (naturalLessOrEqual width telemetryHexSourceMaximumBytes)
                (naturalAnd
                  (naturalLessOrEqual reverse 1)
                  (naturalAnd
                    (naturalLessOrEqual width sourceExtent)
                    (naturalLessOrEqual
                      width
                      (naturalDivideUnchecked (naturalSaturatingSubtract destinationExtent 2) 2))))))
            0
            4)))))

-- Subtract only after retaining the offset bound. This is equivalent to
-- offset + width <= extent over naturals, without overflowing machine-word
-- evaluation when a rejected caller supplies a maximal offset or width.
def telemetryRangeFits =
  (lambda unrestricted offset : Nat .
    (lambda unrestricted width : Nat .
      (lambda unrestricted extent : Nat .
        (naturalAnd
          (naturalLessOrEqual offset extent)
          (naturalLessOrEqual width (naturalSaturatingSubtract extent offset))))))

def telemetryWordCellAdmission =
  (lambda unrestricted offset : Nat .
    (lambda unrestricted sourceExtent : Nat .
      (lambda unrestricted destinationExtent : Nat .
        (aosChoose
          Nat
          (naturalAnd
            (telemetryRangeFits offset captureWordBytes captureRecordBytes)
            (naturalAnd
              (telemetryRangeFits offset captureWordBytes sourceExtent)
              (naturalLessOrEqual telemetryDecimalCellBytes destinationExtent)))
          0
          4))))

def telemetryHexSliceCellAdmission =
  (lambda unrestricted width : Nat .
    (lambda unrestricted reverse : Nat .
      (lambda unrestricted offset : Nat .
        (lambda unrestricted sourceExtent : Nat .
          (lambda unrestricted destinationExtent : Nat .
            (aosChoose
              Nat
              (naturalAnd
                (telemetryRangeFits offset width captureRecordBytes)
                (telemetryRangeFits offset width sourceExtent))
              (telemetryHexCellAdmission width reverse width destinationExtent)
              4))))))