module Observe.Execution

import Data.JSON
import Observe.Interchange
import Observe.Value
import Std.Natural

-- Explicit caller declarations remain visible, including conflicts. Generic
-- invocation defaults describe only runs whose semantic declaration has not
-- been delegated to an assigned native producer. Unknown flags fail closed.
def aosExecutionDeclarationAdmission =
  (lambda unrestricted explicit : Nat .
    (lambda unrestricted owns : Nat .
      (lambda unrestricted delegated : Nat .
        (naturalAnd
          (naturalAnd
            (naturalLessOrEqual explicit 1)
            (naturalAnd (naturalLessOrEqual owns 1) (naturalLessOrEqual delegated 1)))
          (naturalOr
            (naturalEqual explicit 1)
            (naturalAnd (naturalEqual owns 1) (naturalEqual delegated 0)))))))

-- One-based argument insertion for an explicitly requested native assignment.
-- The launcher must have a recorder, and may append one position after the
-- supplied arguments. Bounds are checked before compiling or creating a file.
def aosProgramAssignmentArgumentAdmission =
  (lambda unrestricted argument : Nat .
    (lambda unrestricted supplied : Nat .
      (lambda unrestricted recorder : Nat .
        (naturalAnd
          (naturalEqual recorder 1)
          (naturalAnd
            (naturalLess 0 argument)
            (naturalAnd
              (naturalLessOrEqual argument 4096)
              (naturalLessOrEqual argument (succ supplied))))))))

-- Explicit local output selections require a recorder and bounded valid paths.
-- Selecting a file associates it with a launch; it does not prove who wrote it.
def aosProgramOutputSelectionAdmission =
  (lambda unrestricted count : Nat .
    (lambda unrestricted recorder : Nat .
      (lambda unrestricted paths : Nat .
        (naturalAnd
          (naturalLessOrEqual count 64)
          (naturalAnd
            (naturalEqual paths 1)
            (naturalAnd
              (naturalLessOrEqual recorder 1)
              (naturalOr (naturalEqual count 0) (naturalEqual recorder 1))))))))

-- Presentation metadata has no identity, authorization or execution-outcome
-- authority. Only a declaration bound to its source run with every admitted
-- field may contribute a name. Unknown validation flags fail closed.
def aosExecutionAdmission =
  (lambda unrestricted identity : Nat .
    (lambda unrestricted namespace : Nat .
      (lambda unrestricted name : Nat .
        (lambda unrestricted kind : Nat .
          (lambda unrestricted origin : Nat .
            (naturalAnd
              (naturalEqual identity 1)
              (naturalAnd
                (naturalEqual namespace 1)
                (naturalAnd
                  (naturalEqual name 1)
                  (naturalAnd (naturalEqual kind 1) (naturalEqual origin 1))))))))))

-- A compiled program cannot know its future run identity. This immutable
-- source declaration is carried unchanged in its ALPHATEL journal. Import
-- binds it to the owning frame and emits AOS-EXECUTION/1 beside the original;
-- names remain reported metadata and never become execution/outcome evidence.
-- Rendering this tree grants no admission: the native importer validates all
-- fields using the same execution reader as ordinary catalogue declarations.
def aosExecutionTemplate =
  (lambda unrestricted identity : Bytes .
    (lambda unrestricted name : Bytes .
      (lambda unrestricted kind : Bytes .
        (lambda unrestricted namespace : Bytes .
          (aosDescriptorRecord
            b"execution-template"
            identity
            (constructor
              JSON
              JSONObject
              (constructor
                JSON
                JSONObjectMember
                b"format"
                (constructor JSON JSONString b"AOS-EXECUTION-TEMPLATE/1")
                (constructor
                  JSON
                  JSONObjectMember
                  b"name"
                  (constructor JSON JSONString name)
                  (constructor
                    JSON
                    JSONObjectMember
                    b"workload_kind"
                    (constructor JSON JSONString kind)
                    (constructor
                      JSON
                      JSONObjectMember
                      b"namespace"
                      (constructor JSON JSONString namespace)
                      (constructor
                        JSON
                        JSONObjectMember
                        b"origin"
                        (constructor
                          JSON
                          JSONObject
                          (constructor
                            JSON
                            JSONObjectMember
                            b"kind"
                            (constructor JSON JSONString b"reported")
                            (constructor
                              JSON
                              JSONObjectMember
                              b"method"
                              (constructor
                                JSON
                                JSONString
                                b"maintained Alpha source execution declaration")
                              (constructor JSON JSONObjectEnd))))
                        (constructor JSON JSONObjectEnd))))))))))))

-- Configuration is immutable source metadata scoped by its owning stream.
-- Keeping the tagged values preserves integer precision and float bits. This
-- descriptor deliberately carries no state/update/outcome claim: a compiled
-- request policy may never be selected by the request that actually runs.
def aosExecutionConfiguration =
  (lambda unrestricted identity : Bytes .
    (lambda unrestricted configuration : (family AosValue) .
      (aosDescriptorRecord
        b"execution-configuration"
        identity
        (constructor
          JSON
          JSONObject
          (aosField
            b"format"
            (aosJSONText b"AOS-EXECUTION-CONFIGURATION/1")
            (aosField
              b"basis"
              (aosJSONText b"compiled-program")
              (aosField
                b"configuration"
                (aosValueJSON configuration)
                (aosField
                  b"origin"
                  (constructor
                    JSON
                    JSONObject
                    (aosField
                      b"kind"
                      (aosJSONText b"reported")
                      (aosField
                        b"method"
                        (aosJSONText b"maintained Alpha source compiled configuration")
                        aosObjectEnd)))
                  aosObjectEnd))))))))

-- Process exit and exec refusal are different observations. Phase zero is an
-- exec refusal, phase one a completed wait. Flags are exact: invalid present
-- values (two) never count as absence (zero). Signals use signed exit values.
def aosProgramEndAdmission =
  (lambda unrestricted phase : Nat .
    (lambda unrestricted exitCode : Nat .
      (lambda unrestricted errorText : Nat .
        (naturalOr
          (naturalAnd
            (naturalEqual phase 0)
            (naturalAnd (naturalEqual exitCode 0) (naturalEqual errorText 1)))
          (naturalAnd
            (naturalEqual phase 1)
            (naturalAnd (naturalEqual exitCode 1) (naturalEqual errorText 0)))))))