module Runtime.TelemetryIdentityRoutine

import Runtime.TelemetryCapture
import Runtime.TelemetryIdentity
import Std.Natural

-- Shared binary-role admission and process-birth identity acquisition. The
-- host backend supplies exactly one nonblocking OS entropy request; it may
-- return errors or short counts and must not retry or invent a fallback.
-- AcquireEntropy reads Destination, Extent and VersionOrFlags (then flags),
-- returns the actual signed syscall result in Result, and preserves the saved
-- destination. Load reads a little-endian word relative to Destination.
-- Other word operations wrap at 64 bits; Compare supplies unsigned ordering.
-- Register assignment and the syscall ABI belong exclusively to each emitter.
-- A failed acquisition may have touched bytes. They carry no authority until
-- the count and every nonzero identity role have passed, returning status zero.
family TelemetryIdentityCondition : Type 0
constructor TelemetryIdentityZero
constructor TelemetryIdentityNotZero
constructor TelemetryIdentityBelow

end-family

family TelemetryIdentityRoutineKind : Type 0
constructor TelemetryIdentityValidate
constructor TelemetryIdentityReceipt
constructor TelemetryIdentityCreate
constructor TelemetryIdentityRenewEpoch

end-family

family TelemetryIdentityBackend : Type 0
parameter erased A : Type 0
parameter erased R : Type 0
constructor TelemetryIdentityBackendValue
field unrestricted backendIdentityLoad : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A)))
field unrestricted backendIdentityOr : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A)))
field unrestricted backendIdentityCompare : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A)))
field unrestricted backendIdentityMove : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A)))
field unrestricted backendIdentitySet : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A)))
field unrestricted backendIdentityAddImmediate : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A)))
field unrestricted backendIdentityReturn : (pi unrestricted a0 : Nat . (pi unrestricted a1 : A . A))
field unrestricted backendIdentityLabel : (pi unrestricted a0 : Bytes . (pi unrestricted a1 : A . A))
field unrestricted backendIdentityJumpIf : (pi unrestricted a0 : (family TelemetryIdentityCondition) . (pi unrestricted a1 : Bytes . (pi unrestricted a2 : A . A)))
field unrestricted backendIdentityAcquireEntropy : (pi unrestricted a0 : A . A)
field unrestricted backendIdentityEnd : A
field unrestricted backendIdentityResult : R
field unrestricted backendIdentityReceiptOrWord : R
field unrestricted backendIdentityVersionOrFlags : R
field unrestricted backendIdentityExtent : R
field unrestricted backendIdentityDestination : R
field unrestricted backendIdentitySavedDestination : R

end-family

def telemetryIdentityAssemblyFor =
  (lambda erased A : Type 0 .
    (lambda erased R : Type 0 .
      (lambda unrestricted backend : (family TelemetryIdentityBackend A R) .
        (lambda unrestricted kind : (family TelemetryIdentityRoutineKind) .
          (eliminate
            TelemetryIdentityBackend
            (lambda unrestricted current : (family TelemetryIdentityBackend A R) . A)
            backend
            (branch
              TelemetryIdentityBackendValue
              identityLoad
              identityOr
              identityCompare
              identityMove
              identitySet
              identityAddImmediate
              identityReturn
              identityLabel
              identityJumpIf
              identityAcquireEntropy
              identityEnd
              identityResult
              identityReceiptOrWord
              identityVersionOrFlags
              identityExtent
              identityDestination
              identitySavedDestination
              .
              (let unrestricted identityCheckRole =
                (lambda unrestricted index : Nat .
                  (lambda unrestricted tail : A .
                    (identityLoad
                      identityResult
                      (telemetryIdentityOffset index)
                      (identityLoad
                        identityReceiptOrWord
                        (naturalAdd (telemetryIdentityOffset index) captureWordBytes)
                        (identityOr
                          identityResult
                          identityReceiptOrWord
                          (identityCompare
                            identityResult
                            0
                            (identityJumpIf
                              (constructor TelemetryIdentityCondition TelemetryIdentityZero)
                              b"identity-zero"
                              tail)))))))
                in
                (let unrestricted identityFailures =
                  (identityLabel
                    b"identity-extent"
                    (identityReturn
                      1
                      (identityLabel
                        b"identity-entropy"
                        (identityReturn
                          2
                          (identityLabel
                            b"identity-zero"
                            (identityReturn
                              3
                              (identityLabel b"identity-version" (identityReturn 4 identityEnd))))))))
                  in
                  (let unrestricted identityValidateRoles =
                    (identityCheckRole
                      telemetryRunIdentityIndex
                      (identityCheckRole
                        telemetryAttemptIdentityIndex
                        (identityCheckRole
                          telemetryProducerIdentityIndex
                          (identityCheckRole
                            telemetryProducerEpochIndex
                            (identityReturn 0 identityFailures)))))
                    in
                    (let unrestricted identityAdmission =
                      (lambda unrestricted tail : A .
                        (identityCompare
                          identityVersionOrFlags
                          1
                          (identityJumpIf
                            (constructor TelemetryIdentityCondition TelemetryIdentityNotZero)
                            b"identity-version"
                            (identityCompare
                              identityExtent
                              telemetryIdentitySetBytes
                              (identityJumpIf
                                (constructor TelemetryIdentityCondition TelemetryIdentityBelow)
                                b"identity-extent"
                                tail)))))
                      in
                      (let unrestricted identityValidateAssembly =
                        (identityAdmission identityValidateRoles)
                        in
                        (let unrestricted identityEntropyCountAdmission =
                          (lambda unrestricted expected : Nat .
                            (lambda unrestricted received : R .
                              (identityCompare
                                received
                                expected
                                (identityJumpIf
                                  (constructor TelemetryIdentityCondition TelemetryIdentityNotZero)
                                  b"identity-entropy"
                                  identityValidateRoles))))
                          in
                          (let unrestricted identityEntropyAdmission =
                            (identityEntropyCountAdmission telemetryIdentitySetBytes)
                            in
                            (let unrestricted identityReceiptAssembly =
                              (identityAdmission (identityEntropyAdmission identityReceiptOrWord))
                              in
                              (let unrestricted identityCreateAssembly =
                                (identityAdmission
                                  (identityMove
                                    identitySavedDestination
                                    identityDestination
                                    (identitySet
                                      identityExtent
                                      telemetryIdentitySetBytes
                                      (identitySet
                                        identityVersionOrFlags
                                        1
                                        (identityAcquireEntropy
                                        (identityMove
                                        identityDestination
                                        identitySavedDestination
                                        (identityEntropyAdmission identityResult)))))))
                                in
                                (let unrestricted identityEpochAssembly =
                                  (identityAdmission
                                    (identityCheckRole
                                      telemetryRunIdentityIndex
                                      (identityCheckRole
                                        telemetryAttemptIdentityIndex
                                        (identityCheckRole
                                        telemetryProducerIdentityIndex
                                        (identityMove
                                        identitySavedDestination
                                        identityDestination
                                        (identityAddImmediate
                                        identityDestination
                                        telemetryIdentityBindingBytes
                                        (identitySet
                                        identityExtent
                                        telemetryIdentityBytes
                                        (identitySet
                                        identityVersionOrFlags
                                        1
                                        (identityAcquireEntropy
                                        (identityMove
                                        identityDestination
                                        identitySavedDestination
                                        (identityEntropyCountAdmission
                                        telemetryIdentityBytes
                                        identityResult)))))))))))
                                  in
                                  (eliminate
                                    TelemetryIdentityRoutineKind
                                    (lambda unrestricted current : (family TelemetryIdentityRoutineKind) .
                                      A)
                                    kind
                                    (branch TelemetryIdentityValidate . identityValidateAssembly)
                                    (branch TelemetryIdentityReceipt . identityReceiptAssembly)
                                    (branch TelemetryIdentityCreate . identityCreateAssembly)
                                    (branch TelemetryIdentityRenewEpoch . identityEpochAssembly))))))))))))))))))