module Runtime.TelemetryDrain

import Data.Bytes
import Data.JSON
import Observe.Interchange
import Observe.Stream
import Observe.Value
import Runtime.ArenaCertificate
import Runtime.TelemetryCapture
import Runtime.TelemetryIdentity
import Runtime.TelemetryPublication
import Runtime.TelemetryRecord
import Std.List
import Std.Natural

-- Source declarations own record recipes. The fixed-recipe plan keeps the
-- compact existing layout; the routed plan adds one bounded tag per physical
-- capture slot. Neither infers a schema from payload values or queue position.
-- A Ready value is validated compiled data, not an unforgeable proof token.
-- Construct with compile-time (telemetryDrainPlan ...), as for record plans.
family TelemetryDrainPlan : Type 0
constructor TelemetryDrainReady
field unrestricted telemetryDrainOrdinaryCapacity : Nat
field unrestricted telemetryDrainReservedCapacity : Nat
field unrestricted telemetryDrainOrdinaryRecord : (family TelemetryRecordPlan)
field unrestricted telemetryDrainReservedRecord : (family TelemetryRecordPlan)
field unrestricted telemetryDrainDescriptors : Bytes
field unrestricted telemetryDrainBodyBound : Nat
constructor TelemetryDrainRefused
field unrestricted telemetryDrainRefusal : Bytes

end-family

-- Tags are private acquisition metadata, never taken from a payload word.
-- Zero is the uncommitted marker. Global tag uniqueness catches a source that
-- accidentally binds one tag to different recipes or to both queue roles.
family TelemetryRouteDeclarations : Type 0
constructor TelemetryRouteDeclarationsEnd
constructor TelemetryRouteDeclarationsNext
field unrestricted telemetryRouteDeclaredTag : Nat
field unrestricted telemetryRouteDeclaredContext : Bytes
field unrestricted telemetryRouteDeclaredRecord : (family TelemetryRecordDeclaration)
recursive unrestricted telemetryRouteDeclarationsTail

end-family

family TelemetryRecordRoutes : Type 0
constructor TelemetryRecordRoutesEnd
constructor TelemetryRecordRoutesNext
field unrestricted telemetryRouteTag : Nat
field unrestricted telemetryRouteRecord : (family TelemetryRecordPlan)
recursive unrestricted telemetryRecordRoutesTail

end-family

family TelemetryDispatchPlan : Type 0
constructor TelemetryDispatchReady
field unrestricted telemetryDispatchOrdinaryCapacity : Nat
field unrestricted telemetryDispatchReservedCapacity : Nat
field unrestricted telemetryDispatchOrdinaryRoutes : (family TelemetryRecordRoutes)
field unrestricted telemetryDispatchReservedRoutes : (family TelemetryRecordRoutes)
field unrestricted telemetryDispatchOrdinaryMaximum : (family TelemetryRecordPlan)
field unrestricted telemetryDispatchReservedMaximum : (family TelemetryRecordPlan)
field unrestricted telemetryDispatchDescriptors : Bytes
field unrestricted telemetryDispatchBound : Nat
constructor TelemetryDispatchRefused
field unrestricted telemetryDispatchReason : Bytes

end-family

def telemetryDrainMaximum =
  (lambda unrestricted left : Nat .
    (lambda unrestricted right : Nat . (aosChoose Nat (naturalLessOrEqual left right) right left)))

def telemetryDrainRecordBytes =
  (lambda unrestricted plan : (family TelemetryRecordPlan) .
    (eliminate
      TelemetryRecordPlan
      (lambda unrestricted current : (family TelemetryRecordPlan) . Nat)
      plan
      (branch TelemetryRecordReady parts template . (bytes-length template))
      (branch TelemetryRecordRefused reason . 0)))

def telemetryDrainDescriptorAdmission =
  (lambda unrestricted line : Bytes .
    (naturalAnd
      (telemetryRecordBytesAdmission line)
      (eliminate
        AosLine
        (lambda unrestricted current : (family AosLine) . Nat)
        (aosClassifyLine line)
        (branch AosLineInvalid code . 0)
        (branch
          AosLineValid
          record
          .
          (naturalAnd
            (bytes-equal (aosMemberBytes b"type" record) b"descriptor")
            (naturalAnd
              (naturalIsZero (bytes-equal (aosMemberBytes b"kind" record) b"attempt"))
              (aosChoose
                Nat
                (bytes-equal (aosMemberBytes b"kind" record) b"schema")
                (naturalAnd
                  (naturalNonzero
                    (bytes-length (aosMemberBytes b"schema_id" (aosMemberValue b"body" record))))
                  (aosIsRecordClass
                    (aosMemberBytes b"record_class" (aosMemberValue b"body" record))))
                1)))))))

-- Source plans declare an inventory once. Refuse duplicate descriptor IDs and
-- schema revision aliases within that inventory; replay across native batches
-- still repeats identical declarations through the strict collector normally.
def telemetryDrainDistinctDescriptor =
  (lambda unrestricted line : Bytes .
    (lambda unrestricted following : (family StdList Bytes) .
      (eliminate
        AosLine
        (lambda unrestricted current : (family AosLine) . Nat)
        (aosClassifyLine line)
        (branch AosLineInvalid code . 0)
        (branch
          AosLineValid
          record
          .
          (eliminate
            StdList
            (lambda unrestricted current : (family StdList Bytes) . Nat)
            following
            (branch StdListEmpty . 1)
            (branch
              StdListCons
              head
              tail
              induction
              .
              (naturalAnd
                induction
                (eliminate
                  AosLine
                  (lambda unrestricted current : (family AosLine) . Nat)
                  (aosClassifyLine head)
                  (branch AosLineInvalid code . 0)
                  (branch
                    AosLineValid
                    other
                    .
                    (naturalAnd
                      (naturalIsZero
                        (bytes-equal
                          (aosMemberBytes b"descriptor_id" record)
                          (aosMemberBytes b"descriptor_id" other)))
                      (aosChoose
                        Nat
                        (naturalAnd
                          (bytes-equal (aosMemberBytes b"kind" record) b"schema")
                          (bytes-equal (aosMemberBytes b"kind" other) b"schema"))
                        (naturalIsZero
                          (bytes-equal
                            (aosMemberBytes b"schema_id" (aosMemberValue b"body" record))
                            (aosMemberBytes b"schema_id" (aosMemberValue b"body" other))))
                        1)))))))))))

def telemetryDrainDescriptorsAdmission =
  (lambda unrestricted descriptors : (family StdList Bytes) .
    (eliminate
      StdList
      (lambda unrestricted current : (family StdList Bytes) . Nat)
      descriptors
      (branch StdListEmpty . 1)
      (branch
        StdListCons
        head
        tail
        induction
        .
        (naturalAnd
          induction
          (naturalAnd
            (telemetryDrainDescriptorAdmission head)
            (telemetryDrainDistinctDescriptor head tail))))))

def telemetryDrainSchemaAdmission =
  (lambda unrestricted declaration : (family TelemetryRecordDeclaration) .
    (lambda unrestricted descriptors : (family StdList Bytes) .
      (eliminate
        TelemetryRecordDeclaration
        (lambda unrestricted current : (family TelemetryRecordDeclaration) . Nat)
        declaration
        (branch
          TelemetryRecordDeclarationValue
          schema
          recordClass
          policy
          origin
          method
          payload
          .
          (eliminate
            StdList
            (lambda unrestricted current : (family StdList Bytes) . Nat)
            descriptors
            (branch StdListEmpty . 0)
            (branch
              StdListCons
              head
              tail
              induction
              .
              (naturalOr
                induction
                (eliminate
                  AosLine
                  (lambda unrestricted current : (family AosLine) . Nat)
                  (aosClassifyLine head)
                  (branch AosLineInvalid code . 0)
                  (branch
                    AosLineValid
                    record
                    .
                    (naturalAnd
                      (bytes-equal (aosMemberBytes b"kind" record) b"schema")
                      (naturalAnd
                        (bytes-equal
                          schema
                          (aosMemberBytes b"schema_id" (aosMemberValue b"body" record)))
                        (bytes-equal
                          recordClass
                          (aosMemberBytes b"record_class" (aosMemberValue b"body" record))))))))))))))

def telemetryDrainBound =
  (lambda unrestricted ordinaryCapacity : Nat .
    (lambda unrestricted reservedCapacity : Nat .
      (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
        (lambda unrestricted reserved : (family TelemetryRecordPlan) .
          (lambda unrestricted descriptors : Bytes .
            (telemetryDrainMaximum
              (publicationBodyMaximumBytes ordinaryCapacity reservedCapacity)
              (naturalAdd
                publicationPayloadRecordsAt
                (naturalAdd
                  (bytes-length descriptors)
                  (naturalAdd
                    (naturalMultiply ordinaryCapacity (succ (telemetryDrainRecordBytes ordinary)))
                    (naturalMultiply reservedCapacity (succ (telemetryDrainRecordBytes reserved))))))))))))

def telemetryDrainPlanAtContexts =
  (lambda unrestricted ordinaryContext : Bytes .
    (lambda unrestricted reservedContext : Bytes .
      (lambda unrestricted ordinaryCapacity : Nat .
        (lambda unrestricted reservedCapacity : Nat .
          (lambda unrestricted ordinary : (family TelemetryRecordDeclaration) .
            (lambda unrestricted reserved : (family TelemetryRecordDeclaration) .
              (lambda unrestricted descriptors : (family StdList Bytes) .
                (let unrestricted ordinaryPlan =
                  (telemetryRecordPlanAtContext ordinaryContext ordinary)
                  in
                  (let unrestricted reservedPlan =
                    (telemetryRecordPlanAtContext reservedContext reserved)
                    in
                    (let unrestricted descriptorBytes =
                      (publicationTypedRecordBytes descriptors)
                      in
                      (let unrestricted bound =
                        (telemetryDrainBound
                          ordinaryCapacity
                          reservedCapacity
                          ordinaryPlan
                          reservedPlan
                          descriptorBytes)
                        in
                        (aosChoose
                          (family TelemetryDrainPlan)
                          (naturalAnd
                            (naturalLessOrEqual 2 reservedCapacity)
                            (naturalAnd
                              (naturalLessOrEqual
                                (naturalAdd
                                  (naturalAdd ordinaryCapacity reservedCapacity)
                                  (aosListLength descriptors))
                                1024)
                              (naturalAnd
                                (naturalNonzero (telemetryDrainRecordBytes ordinaryPlan))
                                (naturalAnd
                                  (naturalNonzero (telemetryDrainRecordBytes reservedPlan))
                                  (naturalAnd
                                    (telemetryDrainDescriptorsAdmission descriptors)
                                    (naturalAnd
                                      (telemetryDrainSchemaAdmission ordinary descriptors)
                                      (naturalAnd
                                        (telemetryDrainSchemaAdmission reserved descriptors)
                                        (naturalLessOrEqual
                                        (publicationRecordBytes bound)
                                        publicationMaximumFrameBytes))))))))
                          (constructor
                            TelemetryDrainPlan
                            TelemetryDrainReady
                            ordinaryCapacity
                            reservedCapacity
                            ordinaryPlan
                            reservedPlan
                            descriptorBytes
                            bound)
                          (constructor
                            TelemetryDrainPlan
                            TelemetryDrainRefused
                            b"native-typed-drain-declaration-refused")))))))))))))

def telemetryDrainPlan =
  (telemetryDrainPlanAtContexts b"" b"")

def telemetryDrainScratchBytesForCapacities =
  (lambda unrestricted ordinaryCapacity : Nat .
    (lambda unrestricted reservedCapacity : Nat .
      (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
        (lambda unrestricted reserved : (family TelemetryRecordPlan) .
          (naturalAdd
            telemetryRecordAt
            (telemetryDrainMaximum
              (aosChoose
                Nat
                (naturalNonzero ordinaryCapacity)
                (telemetryDrainRecordBytes ordinary)
                0)
              (aosChoose
                Nat
                (naturalNonzero reservedCapacity)
                (telemetryDrainRecordBytes reserved)
                0)))))))

def telemetryDrainScratchBytes =
  (telemetryDrainScratchBytesForCapacities 1 1)

def telemetryDrainScratchAt =
  (lambda unrestricted applicationBytes : Nat .
    (lambda unrestricted ordinaryCapacity : Nat .
      (lambda unrestricted reservedCapacity : Nat .
        (lambda unrestricted bound : Nat .
          (captureAlign
            (publicationWholeArenaBytesForBody
              applicationBytes
              ordinaryCapacity
              reservedCapacity
              bound))))))

def telemetryDrainArenaBytes =
  (lambda unrestricted applicationBytes : Nat .
    (lambda unrestricted ordinaryCapacity : Nat .
      (lambda unrestricted reservedCapacity : Nat .
        (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
          (lambda unrestricted reserved : (family TelemetryRecordPlan) .
            (lambda unrestricted bound : Nat .
              (naturalAdd
                (telemetryDrainScratchAt applicationBytes ordinaryCapacity reservedCapacity bound)
                (telemetryDrainScratchBytesForCapacities
                  ordinaryCapacity
                  reservedCapacity
                  ordinary
                  reserved))))))))

def telemetryDrainResidents =
  (lambda unrestricted applicationBytes : Nat .
    (lambda unrestricted ordinaryCapacity : Nat .
      (lambda unrestricted reservedCapacity : Nat .
        (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
          (lambda unrestricted reserved : (family TelemetryRecordPlan) .
            (lambda unrestricted bound : Nat .
              (constructor
                ArenaResidents
                ArenaResidentsNext
                (constructor
                  ArenaResident
                  ArenaResidentValue
                  b"typed-drain-record"
                  (telemetryDrainScratchAt applicationBytes ordinaryCapacity reservedCapacity bound)
                  (telemetryDrainScratchBytesForCapacities
                    ordinaryCapacity
                    reservedCapacity
                    ordinary
                    reserved)
                  captureWordBytes)
                (publicationWholeArenaResidentsForBody
                  applicationBytes
                  ordinaryCapacity
                  reservedCapacity
                  bound))))))))

def telemetryDrainArenaCertificate =
  (lambda unrestricted applicationBytes : Nat .
    (lambda unrestricted ordinaryCapacity : Nat .
      (lambda unrestricted reservedCapacity : Nat .
        (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
          (lambda unrestricted reserved : (family TelemetryRecordPlan) .
            (lambda unrestricted bound : Nat .
              (naturalAnd
                (publicationStorageCertificateForBody
                  applicationBytes
                  ordinaryCapacity
                  reservedCapacity
                  bound)
                (naturalAnd
                  (naturalLessOrEqual
                    (telemetryDrainArenaBytes
                      applicationBytes
                      ordinaryCapacity
                      reservedCapacity
                      ordinary
                      reserved
                      bound)
                    captureExtentMaximum)
                  (arenaCertificate
                    (telemetryDrainArenaBytes
                      applicationBytes
                      ordinaryCapacity
                      reservedCapacity
                      ordinary
                      reserved
                      bound)
                    (telemetryDrainResidents
                      applicationBytes
                      ordinaryCapacity
                      reservedCapacity
                      ordinary
                      reserved
                      bound))))))))))

-- Append preflight's byte contract; the native realization additionally checks
-- the rendered status and readiness before touching staged event bytes.
def telemetryDrainAppendAdmission =
  (lambda unrestricted ready : Nat .
    (lambda unrestricted status : Nat .
      (lambda unrestricted bodyBytes : Nat .
        (lambda unrestricted recordBytes : Nat .
          (lambda unrestricted bound : Nat .
            (lambda unrestricted publicationExtent : Nat .
              (lambda unrestricted recordExtent : Nat .
                (naturalAnd
                  (naturalEqual publicationExtent (publicationArenaBytesForBody bound))
                  (naturalAnd
                    (naturalLessOrEqual recordBytes bound)
                    (naturalAnd
                      (naturalLessOrEqual (naturalAdd telemetryRecordAt recordBytes) recordExtent)
                      (naturalAnd
                        (naturalEqual ready 1)
                        (naturalAnd
                          (naturalEqual status 0)
                          (naturalAnd
                            (naturalLessOrEqual publicationPayloadRecordsAt bodyBytes)
                            (naturalLessOrEqual (naturalAdd bodyBytes (succ recordBytes)) bound))))))))))))))

def telemetryRouteDeclaredContains =
  (lambda unrestricted wanted : Nat .
    (lambda unrestricted declarations : (family TelemetryRouteDeclarations) .
      (eliminate
        TelemetryRouteDeclarations
        (lambda unrestricted current : (family TelemetryRouteDeclarations) . Nat)
        declarations
        (branch TelemetryRouteDeclarationsEnd . 0)
        (branch
          TelemetryRouteDeclarationsNext
          tag
          context
          declaration
          tail
          induction
          .
          (naturalOr (naturalEqual tag wanted) induction)))))

def telemetryRouteDeclarationsCount =
  (lambda unrestricted declarations : (family TelemetryRouteDeclarations) .
    (eliminate
      TelemetryRouteDeclarations
      (lambda unrestricted current : (family TelemetryRouteDeclarations) . Nat)
      declarations
      (branch TelemetryRouteDeclarationsEnd . 0)
      (branch
        TelemetryRouteDeclarationsNext
        tag
        context
        declaration
        tail
        induction
        .
        (succ induction))))

def telemetryRouteContextAdmission =
  (lambda unrestricted context : Bytes .
    (lambda unrestricted descriptors : (family StdList Bytes) .
      (aosChoose
        Nat
        (bytes-equal context b"")
        1
        (eliminate
          StdList
          (lambda unrestricted current : (family StdList Bytes) . Nat)
          descriptors
          (branch StdListEmpty . 0)
          (branch
            StdListCons
            head
            tail
            induction
            .
            (naturalOr
              induction
              (eliminate
                AosLine
                (lambda unrestricted current : (family AosLine) . Nat)
                (aosClassifyLine head)
                (branch AosLineInvalid code . 0)
                (branch
                  AosLineValid
                  record
                  .
                  (naturalAnd
                    (bytes-equal (aosMemberBytes b"kind" record) b"context")
                    (bytes-equal
                      context
                      (aosMemberBytes b"context_id" (aosMemberValue b"body" record))))))))))))

def telemetryRouteDeclarationsAdmission =
  (lambda unrestricted declarations : (family TelemetryRouteDeclarations) .
    (lambda unrestricted other : (family TelemetryRouteDeclarations) .
      (lambda unrestricted descriptors : (family StdList Bytes) .
        (eliminate
          TelemetryRouteDeclarations
          (lambda unrestricted current : (family TelemetryRouteDeclarations) . Nat)
          declarations
          (branch TelemetryRouteDeclarationsEnd . 1)
          (branch
            TelemetryRouteDeclarationsNext
            tag
            context
            declaration
            tail
            induction
            .
            (naturalAnd
              induction
              (naturalAnd
                (naturalNonzero tag)
                (naturalAnd
                  (naturalLessOrEqual tag 1024)
                  (naturalAnd
                    (naturalIsZero (telemetryRouteDeclaredContains tag tail))
                    (naturalAnd
                      (naturalIsZero (telemetryRouteDeclaredContains tag other))
                      (naturalAnd
                        (telemetryRouteContextAdmission context descriptors)
                        (naturalAnd
                          (telemetryDrainSchemaAdmission declaration descriptors)
                          (naturalNonzero
                            (telemetryDrainRecordBytes
                              (telemetryRecordPlanAtContext context declaration)))))))))))))))

def telemetryCompileRecordRoutes =
  (lambda unrestricted declarations : (family TelemetryRouteDeclarations) .
    (eliminate
      TelemetryRouteDeclarations
      (lambda unrestricted current : (family TelemetryRouteDeclarations) .
        (family TelemetryRecordRoutes))
      declarations
      (branch
        TelemetryRouteDeclarationsEnd
        .
        (constructor TelemetryRecordRoutes TelemetryRecordRoutesEnd))
      (branch
        TelemetryRouteDeclarationsNext
        tag
        context
        declaration
        tail
        induction
        .
        (constructor
          TelemetryRecordRoutes
          TelemetryRecordRoutesNext
          tag
          (telemetryRecordPlanAtContext context declaration)
          induction))))

def telemetryRecordRouteContains =
  (lambda unrestricted wanted : Nat .
    (lambda unrestricted routes : (family TelemetryRecordRoutes) .
      (eliminate
        TelemetryRecordRoutes
        (lambda unrestricted current : (family TelemetryRecordRoutes) . Nat)
        routes
        (branch TelemetryRecordRoutesEnd . 0)
        (branch
          TelemetryRecordRoutesNext
          tag
          recipe
          tail
          induction
          .
          (naturalOr (naturalEqual tag wanted) induction)))))

def telemetryRouteMaximumRecord =
  (lambda unrestricted routes : (family TelemetryRecordRoutes) .
    (eliminate
      TelemetryRecordRoutes
      (lambda unrestricted current : (family TelemetryRecordRoutes) . (family TelemetryRecordPlan))
      routes
      (branch
        TelemetryRecordRoutesEnd
        .
        (constructor TelemetryRecordPlan TelemetryRecordRefused b"no-record-route"))
      (branch
        TelemetryRecordRoutesNext
        tag
        recipe
        tail
        induction
        .
        (aosChoose
          (family TelemetryRecordPlan)
          (naturalLessOrEqual
            (telemetryDrainRecordBytes induction)
            (telemetryDrainRecordBytes recipe))
          recipe
          induction))))

def telemetryDispatchPlan =
  (lambda unrestricted ordinaryCapacity : Nat .
    (lambda unrestricted reservedCapacity : Nat .
      (lambda unrestricted ordinary : (family TelemetryRouteDeclarations) .
        (lambda unrestricted reserved : (family TelemetryRouteDeclarations) .
          (lambda unrestricted descriptors : (family StdList Bytes) .
            (let unrestricted ordinaryRoutes =
              (telemetryCompileRecordRoutes ordinary)
              in
              (let unrestricted reservedRoutes =
                (telemetryCompileRecordRoutes reserved)
                in
                (let unrestricted ordinaryMaximum =
                  (telemetryRouteMaximumRecord ordinaryRoutes)
                  in
                  (let unrestricted reservedMaximum =
                    (telemetryRouteMaximumRecord reservedRoutes)
                    in
                    (let unrestricted descriptorBytes =
                      (publicationTypedRecordBytes descriptors)
                      in
                      (let unrestricted bound =
                        (telemetryDrainBound
                          ordinaryCapacity
                          reservedCapacity
                          ordinaryMaximum
                          reservedMaximum
                          descriptorBytes)
                        in
                        (aosChoose
                          (family TelemetryDispatchPlan)
                          (naturalAnd
                            (naturalLessOrEqual 2 reservedCapacity)
                            (naturalAnd
                              (naturalLessOrEqual
                                (naturalAdd
                                  (naturalAdd ordinaryCapacity reservedCapacity)
                                  (aosListLength descriptors))
                                1024)
                              (naturalAnd
                                (naturalLessOrEqual
                                  (naturalAdd
                                    (telemetryRouteDeclarationsCount ordinary)
                                    (telemetryRouteDeclarationsCount reserved))
                                  1024)
                                (naturalAnd
                                  (naturalOr
                                    (naturalIsZero ordinaryCapacity)
                                    (naturalNonzero (telemetryDrainRecordBytes ordinaryMaximum)))
                                  (naturalAnd
                                    -- Reserved capacity protects recorder bookkeeping even
                                    -- when this program declares no reserved event routes.
                                    -- An empty route inventory cannot enqueue a reserved
                                    -- record; every declared route still needs a valid plan.
                                    (naturalOr
                                      (naturalIsZero (telemetryRouteDeclarationsCount reserved))
                                      (naturalNonzero (telemetryDrainRecordBytes reservedMaximum)))
                                    (naturalAnd
                                      (telemetryDrainDescriptorsAdmission descriptors)
                                      (naturalAnd
                                        (telemetryRouteDeclarationsAdmission
                                        ordinary
                                        reserved
                                        descriptors)
                                        (naturalAnd
                                        (telemetryRouteDeclarationsAdmission
                                        reserved
                                        ordinary
                                        descriptors)
                                        (naturalLessOrEqual
                                        (publicationRecordBytes bound)
                                        publicationMaximumFrameBytes)))))))))
                          (constructor
                            TelemetryDispatchPlan
                            TelemetryDispatchReady
                            ordinaryCapacity
                            reservedCapacity
                            ordinaryRoutes
                            reservedRoutes
                            ordinaryMaximum
                            reservedMaximum
                            descriptorBytes
                            bound)
                          (constructor
                            TelemetryDispatchPlan
                            TelemetryDispatchRefused
                            b"native-typed-route-declaration-refused")))))))))))))

-- Route tags and one private dispatch word follow the existing derived arena.
-- Capture values, identities and the version-two wire shape remain unchanged.
def telemetryDispatchTagsAt =
  (lambda unrestricted applicationBytes : Nat .
    (lambda unrestricted ordinaryCapacity : Nat .
      (lambda unrestricted reservedCapacity : Nat .
        (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
          (lambda unrestricted reserved : (family TelemetryRecordPlan) .
            (lambda unrestricted bound : Nat .
              (captureAlign
                (telemetryDrainArenaBytes
                  applicationBytes
                  ordinaryCapacity
                  reservedCapacity
                  ordinary
                  reserved
                  bound))))))))

def telemetryDispatchTagsBytes =
  (lambda unrestricted ordinaryCapacity : Nat .
    (lambda unrestricted reservedCapacity : Nat .
      (naturalMultiply (naturalAdd ordinaryCapacity reservedCapacity) captureWordBytes)))

def telemetryDispatchTagScratchAt =
  (lambda unrestricted applicationBytes : Nat .
    (lambda unrestricted ordinaryCapacity : Nat .
      (lambda unrestricted reservedCapacity : Nat .
        (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
          (lambda unrestricted reserved : (family TelemetryRecordPlan) .
            (lambda unrestricted bound : Nat .
              (naturalAdd
                (telemetryDispatchTagsAt
                  applicationBytes
                  ordinaryCapacity
                  reservedCapacity
                  ordinary
                  reserved
                  bound)
                (telemetryDispatchTagsBytes ordinaryCapacity reservedCapacity))))))))

def telemetryDispatchArenaBytes =
  (lambda unrestricted applicationBytes : Nat .
    (lambda unrestricted ordinaryCapacity : Nat .
      (lambda unrestricted reservedCapacity : Nat .
        (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
          (lambda unrestricted reserved : (family TelemetryRecordPlan) .
            (lambda unrestricted bound : Nat .
              (naturalAdd
                captureWordBytes
                (telemetryDispatchTagScratchAt
                  applicationBytes
                  ordinaryCapacity
                  reservedCapacity
                  ordinary
                  reserved
                  bound))))))))

def telemetryDispatchResidents =
  (lambda unrestricted applicationBytes : Nat .
    (lambda unrestricted ordinaryCapacity : Nat .
      (lambda unrestricted reservedCapacity : Nat .
        (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
          (lambda unrestricted reserved : (family TelemetryRecordPlan) .
            (lambda unrestricted bound : Nat .
              (constructor
                ArenaResidents
                ArenaResidentsNext
                (constructor
                  ArenaResident
                  ArenaResidentValue
                  b"typed-drain-route-tags"
                  (telemetryDispatchTagsAt
                    applicationBytes
                    ordinaryCapacity
                    reservedCapacity
                    ordinary
                    reserved
                    bound)
                  (naturalAdd
                    captureWordBytes
                    (telemetryDispatchTagsBytes ordinaryCapacity reservedCapacity))
                  captureWordBytes)
                (telemetryDrainResidents
                  applicationBytes
                  ordinaryCapacity
                  reservedCapacity
                  ordinary
                  reserved
                  bound))))))))

def telemetryDispatchArenaCertificate =
  (lambda unrestricted applicationBytes : Nat .
    (lambda unrestricted ordinaryCapacity : Nat .
      (lambda unrestricted reservedCapacity : Nat .
        (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
          (lambda unrestricted reserved : (family TelemetryRecordPlan) .
            (lambda unrestricted bound : Nat .
              (naturalAnd
                (telemetryDrainArenaCertificate
                  applicationBytes
                  ordinaryCapacity
                  reservedCapacity
                  ordinary
                  reserved
                  bound)
                (naturalAnd
                  (naturalLessOrEqual
                    (telemetryDispatchArenaBytes
                      applicationBytes
                      ordinaryCapacity
                      reservedCapacity
                      ordinary
                      reserved
                      bound)
                    captureExtentMaximum)
                  (arenaCertificate
                    (telemetryDispatchArenaBytes
                      applicationBytes
                      ordinaryCapacity
                      reservedCapacity
                      ordinary
                      reserved
                      bound)
                    (telemetryDispatchResidents
                      applicationBytes
                      ordinaryCapacity
                      reservedCapacity
                      ordinary
                      reserved
                      bound))))))))))

-- An excluded policy site has no compiled route. This explicit refusal is
-- harmless only when its source operands and renderer are pruned by selection.
def telemetryRecordRouteLookup =
  (lambda unrestricted wanted : Nat .
    (lambda unrestricted routes : (family TelemetryRecordRoutes) .
      (eliminate
        TelemetryRecordRoutes
        (lambda unrestricted current : (family TelemetryRecordRoutes) .
          (family TelemetryRecordPlan))
        routes
        (branch
          TelemetryRecordRoutesEnd
          .
          (constructor
            TelemetryRecordPlan
            TelemetryRecordRefused
            b"capture-site-excluded-or-undeclared"))
        (branch
          TelemetryRecordRoutesNext
          tag
          recipe
          following
          induction
          .
          (aosChoose (family TelemetryRecordPlan) (naturalEqual wanted tag) recipe induction)))))