module Runtime.TelemetryIdentity

import Observe.Value
import Runtime.ArenaCertificate
import Runtime.TelemetryCapture
import Std.Natural

-- AOS-ID-003 fixes a 128-bit, nonzero identity (32 lowercase hex digits on
-- interchange). Native memory retains its sixteen binary bytes, not text.
-- Run/attempt/producer may be assigned by an admitted execution coordinator;
-- only producer_epoch is renewed at every process start. Uploads mint none.
def telemetryIdentityBytes : Nat =
  (naturalDivideUnchecked 32 2)

def telemetryRunIdentityIndex : Nat =
  0

def telemetryAttemptIdentityIndex : Nat =
  (succ telemetryRunIdentityIndex)

def telemetryProducerIdentityIndex : Nat =
  (succ telemetryAttemptIdentityIndex)

def telemetryProducerEpochIndex : Nat =
  (succ telemetryProducerIdentityIndex)

def telemetryIdentityOffset =
  (lambda unrestricted index : Nat . (naturalMultiply index telemetryIdentityBytes))

def telemetryIdentitySetBytes : Nat =
  (telemetryIdentityOffset (succ telemetryProducerEpochIndex))

def telemetryIdentityBindingBytes : Nat =
  (telemetryIdentityOffset telemetryProducerEpochIndex)

-- The supplied transport contains exactly the three assigned binary roles.
-- A short read or any trailing byte refuses binding before epoch entropy is
-- acquired. This proves framing, not the caller's coordinator authority.
def telemetryAssignedBindingAdmission =
  (lambda unrestricted received : Nat .
    (lambda unrestricted trailing : Nat .
      (naturalAnd
        (naturalEqual received telemetryIdentityBindingBytes)
        (naturalIsZero trailing))))

def telemetryBinaryIdentityValid =
  (lambda unrestricted value : Bytes .
    (naturalAnd
      (naturalEqual (bytes-length value) telemetryIdentityBytes)
      (aosAnyByte (lambda unrestricted b : Byte . (naturalIsZero (byte-equal b (byte 0)))) value)))

-- 0 admitted, 1 insufficient destination, 2 incomplete entropy, 3 zero
-- identity, 4 unsupported contract. A successful byte count alone is not
-- permission to publish; every role must meet the AOS identity contract.
def telemetryIdentityAdmission =
  (lambda unrestricted version : Nat .
    (lambda unrestricted extent : Nat .
      (lambda unrestricted received : Nat .
        (lambda unrestricted valid : Nat .
          (aosChoose
            Nat
            (naturalAnd (naturalEqual version 1) (naturalLessOrEqual valid 1))
            (aosChoose
              Nat
              (naturalLessOrEqual telemetryIdentitySetBytes extent)
              (aosChoose
                Nat
                (naturalEqual received telemetryIdentitySetBytes)
                (aosChoose Nat valid 0 3)
                2)
              1)
            4)))))

-- A supplied binding is three binary roles, already loaded into the identity
-- arena. Epoch initialization retains those bytes and acquires only the last
-- role. Admission proves the count/shape decision, not coordinator authority
-- or entropy provenance. The native initializer validates the binding before
-- asking the kernel for entropy and validates all four roles afterwards.
def telemetryEpochAdmission =
  (lambda unrestricted version : Nat .
    (lambda unrestricted extent : Nat .
      (lambda unrestricted received : Nat .
        (lambda unrestricted valid : Nat .
          (aosChoose
            Nat
            (naturalAnd (naturalEqual version 1) (naturalLessOrEqual valid 1))
            (aosChoose
              Nat
              (naturalLessOrEqual telemetryIdentitySetBytes extent)
              (aosChoose
                Nat
                (naturalEqual received telemetryIdentityBytes)
                (aosChoose Nat valid 0 3)
                2)
              1)
            4)))))

-- Extend the capture arena, rather than reserving an unrelated absolute
-- address. The application and acquisition residents keep their owner.
def captureIdentityAt =
  (lambda unrestricted applicationBytes : Nat .
    (lambda unrestricted ordinaryCapacity : Nat .
      (lambda unrestricted reservedCapacity : Nat .
        (captureAlign (captureArenaBytes applicationBytes ordinaryCapacity reservedCapacity)))))

def captureWithIdentityArenaBytes =
  (lambda unrestricted applicationBytes : Nat .
    (lambda unrestricted ordinaryCapacity : Nat .
      (lambda unrestricted reservedCapacity : Nat .
        (naturalAdd
          (captureIdentityAt applicationBytes ordinaryCapacity reservedCapacity)
          telemetryIdentitySetBytes))))

def captureWithIdentityArenaResidents =
  (lambda unrestricted applicationBytes : Nat .
    (lambda unrestricted ordinaryCapacity : Nat .
      (lambda unrestricted reservedCapacity : Nat .
        (constructor
          ArenaResidents
          ArenaResidentsNext
          (constructor
            ArenaResident
            ArenaResidentValue
            b"telemetry-identities"
            (captureIdentityAt applicationBytes ordinaryCapacity reservedCapacity)
            telemetryIdentitySetBytes
            captureWordBytes)
          (captureArenaResidents applicationBytes ordinaryCapacity reservedCapacity)))))

def captureWithIdentityArenaCertificate =
  (lambda unrestricted applicationBytes : Nat .
    (lambda unrestricted ordinaryCapacity : Nat .
      (lambda unrestricted reservedCapacity : Nat .
        (naturalAnd
          (captureArenaCertificate applicationBytes ordinaryCapacity reservedCapacity)
          (naturalAnd
            (naturalLessOrEqual
              (captureWithIdentityArenaBytes applicationBytes ordinaryCapacity reservedCapacity)
              captureExtentMaximum)
            (arenaCertificate
              (captureWithIdentityArenaBytes applicationBytes ordinaryCapacity reservedCapacity)
              (captureWithIdentityArenaResidents applicationBytes ordinaryCapacity reservedCapacity)))))))