Observe.Execution

1module Observe.Execution
2
3import Data.JSON
4import Observe.Interchange
5import Observe.Value
6import Std.Natural
7
8-- Explicit caller declarations remain visible, including conflicts. Generic
9-- invocation defaults describe only runs whose semantic declaration has not
10-- been delegated to an assigned native producer. Unknown flags fail closed.
11def aosExecutionDeclarationAdmission =
12  (lambda unrestricted explicit : Nat .
13    (lambda unrestricted owns : Nat .
14      (lambda unrestricted delegated : Nat .
15        (naturalAnd
16          (naturalAnd
17            (naturalLessOrEqual explicit 1)
18            (naturalAnd (naturalLessOrEqual owns 1) (naturalLessOrEqual delegated 1)))
19          (naturalOr
20            (naturalEqual explicit 1)
21            (naturalAnd (naturalEqual owns 1) (naturalEqual delegated 0)))))))
22
23-- One-based argument insertion for an explicitly requested native assignment.
24-- The launcher must have a recorder, and may append one position after the
25-- supplied arguments. Bounds are checked before compiling or creating a file.
26def aosProgramAssignmentArgumentAdmission =
27  (lambda unrestricted argument : Nat .
28    (lambda unrestricted supplied : Nat .
29      (lambda unrestricted recorder : Nat .
30        (naturalAnd
31          (naturalEqual recorder 1)
32          (naturalAnd
33            (naturalLess 0 argument)
34            (naturalAnd
35              (naturalLessOrEqual argument 4096)
36              (naturalLessOrEqual argument (succ supplied))))))))
37
38-- Explicit local output selections require a recorder and bounded valid paths.
39-- Selecting a file associates it with a launch; it does not prove who wrote it.
40def aosProgramOutputSelectionAdmission =
41  (lambda unrestricted count : Nat .
42    (lambda unrestricted recorder : Nat .
43      (lambda unrestricted paths : Nat .
44        (naturalAnd
45          (naturalLessOrEqual count 64)
46          (naturalAnd
47            (naturalEqual paths 1)
48            (naturalAnd
49              (naturalLessOrEqual recorder 1)
50              (naturalOr (naturalEqual count 0) (naturalEqual recorder 1))))))))
51
52-- Presentation metadata has no identity, authorization or execution-outcome
53-- authority. Only a declaration bound to its source run with every admitted
54-- field may contribute a name. Unknown validation flags fail closed.
55def aosExecutionAdmission =
56  (lambda unrestricted identity : Nat .
57    (lambda unrestricted namespace : Nat .
58      (lambda unrestricted name : Nat .
59        (lambda unrestricted kind : Nat .
60          (lambda unrestricted origin : Nat .
61            (naturalAnd
62              (naturalEqual identity 1)
63              (naturalAnd
64                (naturalEqual namespace 1)
65                (naturalAnd
66                  (naturalEqual name 1)
67                  (naturalAnd (naturalEqual kind 1) (naturalEqual origin 1))))))))))
68
69-- A compiled program cannot know its future run identity. This immutable
70-- source declaration is carried unchanged in its ALPHATEL journal. Import
71-- binds it to the owning frame and emits AOS-EXECUTION/1 beside the original;
72-- names remain reported metadata and never become execution/outcome evidence.
73-- Rendering this tree grants no admission: the native importer validates all
74-- fields using the same execution reader as ordinary catalogue declarations.
75def aosExecutionTemplate =
76  (lambda unrestricted identity : Bytes .
77    (lambda unrestricted name : Bytes .
78      (lambda unrestricted kind : Bytes .
79        (lambda unrestricted namespace : Bytes .
80          (aosDescriptorRecord
81            b"execution-template"
82            identity
83            (constructor
84              JSON
85              JSONObject
86              (constructor
87                JSON
88                JSONObjectMember
89                b"format"
90                (constructor JSON JSONString b"AOS-EXECUTION-TEMPLATE/1")
91                (constructor
92                  JSON
93                  JSONObjectMember
94                  b"name"
95                  (constructor JSON JSONString name)
96                  (constructor
97                    JSON
98                    JSONObjectMember
99                    b"workload_kind"
100                    (constructor JSON JSONString kind)
101                    (constructor
102                      JSON
103                      JSONObjectMember
104                      b"namespace"
105                      (constructor JSON JSONString namespace)
106                      (constructor
107                        JSON
108                        JSONObjectMember
109                        b"origin"
110                        (constructor
111                          JSON
112                          JSONObject
113                          (constructor
114                            JSON
115                            JSONObjectMember
116                            b"kind"
117                            (constructor JSON JSONString b"reported")
118                            (constructor
119                              JSON
120                              JSONObjectMember
121                              b"method"
122                              (constructor
123                                JSON
124                                JSONString
125                                b"maintained Alpha source execution declaration")
126                              (constructor JSON JSONObjectEnd))))
127                        (constructor JSON JSONObjectEnd))))))))))))
128
129-- Configuration is immutable source metadata scoped by its owning stream.
130-- Keeping the tagged values preserves integer precision and float bits. This
131-- descriptor deliberately carries no state/update/outcome claim: a compiled
132-- request policy may never be selected by the request that actually runs.
133def aosExecutionConfiguration =
134  (lambda unrestricted identity : Bytes .
135    (lambda unrestricted configuration : (family AosValue) .
136      (aosDescriptorRecord
137        b"execution-configuration"
138        identity
139        (constructor
140          JSON
141          JSONObject
142          (aosField
143            b"format"
144            (aosJSONText b"AOS-EXECUTION-CONFIGURATION/1")
145            (aosField
146              b"basis"
147              (aosJSONText b"compiled-program")
148              (aosField
149                b"configuration"
150                (aosValueJSON configuration)
151                (aosField
152                  b"origin"
153                  (constructor
154                    JSON
155                    JSONObject
156                    (aosField
157                      b"kind"
158                      (aosJSONText b"reported")
159                      (aosField
160                        b"method"
161                        (aosJSONText b"maintained Alpha source compiled configuration")
162                        aosObjectEnd)))
163                  aosObjectEnd))))))))
164
165-- Process exit and exec refusal are different observations. Phase zero is an
166-- exec refusal, phase one a completed wait. Flags are exact: invalid present
167-- values (two) never count as absence (zero). Signals use signed exit values.
168def aosProgramEndAdmission =
169  (lambda unrestricted phase : Nat .
170    (lambda unrestricted exitCode : Nat .
171      (lambda unrestricted errorText : Nat .
172        (naturalOr
173          (naturalAnd
174            (naturalEqual phase 0)
175            (naturalAnd (naturalEqual exitCode 0) (naturalEqual errorText 1)))
176          (naturalAnd
177            (naturalEqual phase 1)
178            (naturalAnd (naturalEqual exitCode 1) (naturalEqual errorText 0)))))))