module Runtime.TelemetryCapture

import Data.Bytes
import Model.Parameter
import Model.Word64
import Observe.Capture
import Observe.Value
import Runtime.ArenaCertificate
import Runtime.NativeTelemetry
import Std.Natural

-- A fixed-shape acquisition buffer for the existing native scalar record.
-- This is capture storage, not a wire encoding or durability acknowledgement.
-- Sequence precedes the native counters; formatting/sealing belongs to drain.
-- The field list owns all offsets. No caller carries a layout-specific number.
def captureWordBytes : Nat =
  (bytes-length (nativeTelemetryWord64Bytes nativeTelemetryZeroWord64))

def captureValuesBytes : Nat =
  (bytes-length
    (nativeTelemetryEncodeCounters
      (constructor NativeTelemetryCounters NativeTelemetryCountersValue 0 0 0 0 0 0 0 0)))

def captureValueWords : Nat =
  (naturalDivideUnchecked captureValuesBytes captureWordBytes)

def captureSequenceAt : Nat =
  0

def captureValuesAt : Nat =
  captureWordBytes

def captureRecordBytes : Nat =
  (naturalAdd captureWordBytes captureValuesBytes)

def captureOrdinaryCapacityIndex : Nat =
  0

def captureOrdinaryCapacityAt : Nat =
  (naturalMultiply captureOrdinaryCapacityIndex captureWordBytes)

def captureReservedCapacityIndex : Nat =
  (succ captureOrdinaryCapacityIndex)

def captureReservedCapacityAt : Nat =
  (naturalMultiply captureReservedCapacityIndex captureWordBytes)

def captureOrdinaryUsedIndex : Nat =
  (succ captureReservedCapacityIndex)

def captureOrdinaryUsedAt : Nat =
  (naturalMultiply captureOrdinaryUsedIndex captureWordBytes)

def captureReservedUsedIndex : Nat =
  (succ captureOrdinaryUsedIndex)

def captureReservedUsedAt : Nat =
  (naturalMultiply captureReservedUsedIndex captureWordBytes)

def captureNextSequenceIndex : Nat =
  (succ captureReservedUsedIndex)

def captureNextSequenceAt : Nat =
  (naturalMultiply captureNextSequenceIndex captureWordBytes)

def captureDroppedIndex : Nat =
  (succ captureNextSequenceIndex)

def captureDroppedAt : Nat =
  (naturalMultiply captureDroppedIndex captureWordBytes)

def captureExcludedIndex : Nat =
  (succ captureDroppedIndex)

def captureExcludedAt : Nat =
  (naturalMultiply captureExcludedIndex captureWordBytes)

def captureRequiredIndex : Nat =
  (succ captureExcludedIndex)

def captureRequiredAt : Nat =
  (naturalMultiply captureRequiredIndex captureWordBytes)

def captureControlBytes : Nat =
  (naturalMultiply (succ captureRequiredIndex) captureWordBytes)

def captureAlign =
  (lambda unrestricted n : Nat .
    (naturalMultiply
      (naturalDivideUnchecked
        (naturalAdd n (naturalSaturatingSubtract captureWordBytes 1))
        captureWordBytes)
      captureWordBytes))

def captureControlAt =
  captureAlign

def captureQueueAt =
  (lambda unrestricted applicationBytes : Nat .
    (naturalAdd (captureControlAt applicationBytes) captureControlBytes))

def captureQueueBytes =
  (lambda unrestricted ordinaryCapacity : Nat .
    (lambda unrestricted reservedCapacity : Nat .
      (naturalMultiply (naturalAdd ordinaryCapacity reservedCapacity) captureRecordBytes)))

def captureValuesScratchAt =
  (lambda unrestricted applicationBytes : Nat .
    (lambda unrestricted ordinaryCapacity : Nat .
      (lambda unrestricted reservedCapacity : Nat .
        (naturalAdd
          (captureQueueAt applicationBytes)
          (captureQueueBytes ordinaryCapacity reservedCapacity)))))

def captureArenaBytes =
  (lambda unrestricted applicationBytes : Nat .
    (lambda unrestricted ordinaryCapacity : Nat .
      (lambda unrestricted reservedCapacity : Nat .
        (naturalAdd
          (captureValuesScratchAt applicationBytes ordinaryCapacity reservedCapacity)
          captureValuesBytes))))

-- A general program may have no application arena. The capture arena
-- must not invent an empty resident merely to certify that valid shape.
def captureArenaResidents =
  (lambda unrestricted applicationBytes : Nat .
    (lambda unrestricted ordinaryCapacity : Nat .
      (lambda unrestricted reservedCapacity : Nat .
        (aosChoose
          (family ArenaResidents)
          (naturalIsZero applicationBytes)
          (constructor
            ArenaResidents
            ArenaResidentsNext
            (constructor
              ArenaResident
              ArenaResidentValue
              b"capture-control"
              (captureControlAt applicationBytes)
              captureControlBytes
              captureWordBytes)
            (constructor
              ArenaResidents
              ArenaResidentsNext
              (constructor
                ArenaResident
                ArenaResidentValue
                b"capture-queue"
                (captureQueueAt applicationBytes)
                (captureQueueBytes ordinaryCapacity reservedCapacity)
                captureWordBytes)
              (constructor
                ArenaResidents
                ArenaResidentsNext
                (constructor
                  ArenaResident
                  ArenaResidentValue
                  b"capture-values"
                  (captureValuesScratchAt applicationBytes ordinaryCapacity reservedCapacity)
                  captureValuesBytes
                  captureWordBytes)
                (constructor ArenaResidents ArenaResidentsEnd))))
          (constructor
            ArenaResidents
            ArenaResidentsNext
            (constructor ArenaResident ArenaResidentValue b"application" 0 applicationBytes 1)
            (constructor
              ArenaResidents
              ArenaResidentsNext
              (constructor
                ArenaResident
                ArenaResidentValue
                b"capture-control"
                (captureControlAt applicationBytes)
                captureControlBytes
                captureWordBytes)
              (constructor
                ArenaResidents
                ArenaResidentsNext
                (constructor
                  ArenaResident
                  ArenaResidentValue
                  b"capture-queue"
                  (captureQueueAt applicationBytes)
                  (captureQueueBytes ordinaryCapacity reservedCapacity)
                  captureWordBytes)
                (constructor
                  ArenaResidents
                  ArenaResidentsNext
                  (constructor
                    ArenaResident
                    ArenaResidentValue
                    b"capture-values"
                    (captureValuesScratchAt applicationBytes ordinaryCapacity reservedCapacity)
                    captureValuesBytes
                    captureWordBytes)
                  (constructor ArenaResidents ArenaResidentsEnd)))))))))

def captureExtentMaximum : Nat =
  18446744073709551615

def captureArenaCertificate =
  (lambda unrestricted applicationBytes : Nat .
    (lambda unrestricted ordinaryCapacity : Nat .
      (lambda unrestricted reservedCapacity : Nat .
        (naturalAnd
          (naturalLessOrEqual
            (captureArenaBytes applicationBytes ordinaryCapacity reservedCapacity)
            captureExtentMaximum)
          (naturalAnd
            (naturalLessOrEqual 2 reservedCapacity)
            (arenaCertificate
              (captureArenaBytes applicationBytes ordinaryCapacity reservedCapacity)
              (captureArenaResidents applicationBytes ordinaryCapacity reservedCapacity)))))))

-- Initialize the owner-controlled policy and counters. Runtime room checks
-- precede every mutation; accepted counts are the sum of the two used fields.
def captureInitialControl =
  (lambda unrestricted ordinaryCapacity : Nat .
    (lambda unrestricted reservedCapacity : Nat .
      (lambda unrestricted required : Nat .
        (aosChoose
          Bytes
          (naturalAnd
            (naturalEqual
              (aosCaptureAdmission 1 0 0 required ordinaryCapacity reservedCapacity 0 0)
              0)
            (naturalLessOrEqual
              (captureQueueBytes ordinaryCapacity reservedCapacity)
              captureExtentMaximum))
          (bytes-append
            (dataBytesWord64LE (modelWord64FromNaturalTruncated ordinaryCapacity))
            (bytes-append
              (dataBytesWord64LE (modelWord64FromNaturalTruncated reservedCapacity))
              (bytes-append
                (dataBytesWord64LE 0)
                (bytes-append
                  (dataBytesWord64LE 0)
                  (bytes-append
                    (dataBytesWord64LE 0)
                    (bytes-append
                      (dataBytesWord64LE 0)
                      (bytes-append
                        (dataBytesWord64LE 0)
                        (dataBytesWord64LE (modelWord64FromNaturalTruncated required)))))))))
          b""))))