module Runtime.TelemetryRecordRoutine

import Observe.Value
import Runtime.TelemetryCapture
import Runtime.TelemetryIdentity
import Runtime.TelemetryRecord
import Std.Natural

-- Read-only admission for a closed record recipe. Extents are checked before
-- any source read; all four bound identities and required 128-bit references
-- must be nonzero. A caller supplies live disjoint buffers, keeps the source
-- and identities stable through rendering, and checks the returned status.
-- Success here grants rendering, never publication or durable acknowledgement.
-- Word loads and OR operate on exact 64-bit words; extent comparisons are
-- unsigned. Emitters preserve the host interpreter's persistent registers.
family TelemetryRecordRoutineKind : Type 0
constructor TelemetryRecordAdmissionRoutine
field unrestricted recordAdmissionParts : (family TelemetryRecordParts)
constructor TelemetryRecordStatusRoutine

end-family

family TelemetryRecordBackend : Type 0
parameter erased A : Type 0
parameter erased R : Type 0
constructor TelemetryRecordBackendValue
field unrestricted backendRecordLoad64 : (pi unrestricted destination : R . (pi unrestricted base : R . (pi unrestricted offset : Nat . (pi unrestricted tail : A . A))))
field unrestricted backendRecordOr : (pi unrestricted left : R . (pi unrestricted right : R . (pi unrestricted tail : A . A)))
field unrestricted backendRecordCompareImmediate : (pi unrestricted register : R . (pi unrestricted value : Nat . (pi unrestricted tail : A . A)))
field unrestricted backendRecordJumpZero : (pi unrestricted name : Bytes . (pi unrestricted tail : A . A))
field unrestricted backendRecordJumpBelow : (pi unrestricted name : Bytes . (pi unrestricted tail : A . A))
field unrestricted backendRecordSet : (pi unrestricted register : R . (pi unrestricted value : Nat . (pi unrestricted tail : A . A)))
field unrestricted backendRecordLabel : (pi unrestricted name : Bytes . (pi unrestricted tail : A . A))
field unrestricted backendRecordReturn : (pi unrestricted tail : A . A)
field unrestricted backendRecordEnd : A
field unrestricted backendRecordResult : R
field unrestricted backendRecordScratch : R
field unrestricted backendRecordSource : R
field unrestricted backendRecordIdentities : R
field unrestricted backendRecordSourceExtent : R
field unrestricted backendRecordIdentityExtent : R
field unrestricted backendRecordOutputExtent : R

end-family

def telemetryRecordAssemblyFor =
  (lambda erased A : Type 0 .
    (lambda erased R : Type 0 .
      (lambda unrestricted backend : (family TelemetryRecordBackend A R) .
        (lambda unrestricted kind : (family TelemetryRecordRoutineKind) .
          (eliminate
            TelemetryRecordBackend
            (lambda unrestricted current : (family TelemetryRecordBackend A R) . A)
            backend
            (branch
              TelemetryRecordBackendValue
              recordLoad64
              recordOr
              recordCompareImmediate
              recordJumpZero
              recordJumpBelow
              recordSet
              recordLabel
              recordReturn
              recordEnd
              recordResult
              recordScratch
              recordSource
              recordIdentities
              recordSourceExtent
              recordIdentityExtent
              recordOutputExtent
              .
              (let unrestricted recordCheckNonzero =
                (lambda unrestricted base : R .
                  (lambda unrestricted offset : Nat .
                    (lambda unrestricted tail : A .
                      (recordLoad64
                        recordResult
                        base
                        offset
                        (recordLoad64
                          recordScratch
                          base
                          (naturalAdd offset captureWordBytes)
                          (recordOr
                            recordResult
                            recordScratch
                            (recordCompareImmediate
                              recordResult
                              0
                              (recordJumpZero b"record-refused" tail))))))))
                in
                (let unrestricted recordCheckParts =
                  (lambda unrestricted parts : (family TelemetryRecordParts) .
                    (eliminate
                      TelemetryRecordParts
                      (lambda unrestricted current : (family TelemetryRecordParts) . A)
                      parts
                      (branch
                        TelemetryRecordEnd
                        .
                        (recordSet
                          recordResult
                          1
                          (recordReturn
                            (recordLabel
                              b"record-refused"
                              (recordSet recordResult 0 (recordReturn recordEnd))))))
                      (branch TelemetryRecordLiteral bytes tail induction . induction)
                      (branch TelemetryRecordDecimal signed offset tail induction . induction)
                      (branch
                        TelemetryRecordHex
                        source
                        offset
                        width
                        reverse
                        nonzero
                        tail
                        induction
                        .
                        (aosChoose
                          A
                          nonzero
                          (recordCheckNonzero
                            (aosChoose R source recordIdentities recordSource)
                            offset
                            induction)
                          induction))))
                  in
                  (let unrestricted recordAdmissionAssembly =
                    (lambda unrestricted parts : (family TelemetryRecordParts) .
                      (recordCompareImmediate
                        recordSourceExtent
                        captureRecordBytes
                        (recordJumpBelow
                          b"record-refused"
                          (recordCompareImmediate
                            recordIdentityExtent
                            telemetryIdentitySetBytes
                            (recordJumpBelow
                              b"record-refused"
                              (recordCompareImmediate
                                recordOutputExtent
                                (bytes-length (telemetryRecordPartBytes parts))
                                (recordJumpBelow
                                  b"record-refused"
                                  (nat-eliminate
                                    (lambda unrestricted current : Nat . A)
                                    (recordCheckParts parts)
                                    (lambda unrestricted index : Nat .
                                      (lambda unrestricted induction : A .
                                        (recordCheckNonzero
                                        recordIdentities
                                        (telemetryIdentityOffset index)
                                        induction)))
                                    (succ telemetryProducerEpochIndex)))))))))
                    in
                    (eliminate
                      TelemetryRecordRoutineKind
                      (lambda unrestricted current : (family TelemetryRecordRoutineKind) . A)
                      kind
                      (branch
                        TelemetryRecordAdmissionRoutine
                        parts
                        .
                        (recordAdmissionAssembly parts))
                      (branch
                        TelemetryRecordStatusRoutine
                        .
                        (recordLoad64 recordResult recordSource 0 (recordReturn recordEnd)))))))))))))