854 lines
25 KiB
Markdown
854 lines
25 KiB
Markdown
# PEL/1-SURF — Primitive Execution Surface (Store-Backed)
|
||
|
||
Status: Approved
|
||
Owner: Niklas Rydberg
|
||
Version: 0.2.2
|
||
SoT: Yes
|
||
Last Updated: 2025-11-30
|
||
Linked Phase Pack: N/A
|
||
Tags: [execution, deterministic]
|
||
|
||
<!-- Source: /amduat/docs/new/pel1-surf.md | Canonical: /amduat/tier1/pel-1-surf.md -->
|
||
|
||
**Document ID:** `PEL/1-SURF`
|
||
**Layer:** L1 — Execution surface over ASL/1-STORE
|
||
|
||
**Depends on (normative):**
|
||
|
||
* `PEL/1-CORE v0.3.x` — Primitive Execution Layer (core semantics)
|
||
* `ASL/1-CORE v0.4.x` — Artifact Substrate (logical values)
|
||
* `ASL/1-STORE v0.4.x` — Store semantics over `Reference -> Artifact`
|
||
|
||
**Integrates with (informative):**
|
||
|
||
* `ENC/ASL1-CORE v1.0.4` — Canonical encodings for `Artifact` / `Reference`
|
||
* `HASH/ASL1 v0.2.4` — ASL1 hash family (`HashId` assignments)
|
||
* `ENC/PEL1-RESULT/1 v0.1.x` — Canonical encoding for PEL/1 ExecutionResult artifacts
|
||
* `PEL/PROGRAM-DAG/1` (planned) — DAG program scheme
|
||
* `PEL/TRACE-DAG/1` (planned) — Structured execution trace profile
|
||
* `TGK/1-CORE` — Trace Graph Kernel
|
||
* `CIL/1`, `FER/1`, `FCT/1` — Certification, evidence, facts
|
||
|
||
© 2025 Niklas Rydberg.
|
||
|
||
## License
|
||
|
||
Except where otherwise noted, this document (text and diagrams) is licensed under
|
||
the Creative Commons Attribution 4.0 International License (CC BY 4.0).
|
||
|
||
The identifier registries and mapping tables (e.g. TypeTag IDs, HashId
|
||
assignments, EdgeTypeId tables) are additionally made available under CC0 1.0
|
||
Universal (CC0) to enable unrestricted reuse in implementations and derivative
|
||
specifications.
|
||
|
||
Code examples in this document are provided under the Apache License 2.0 unless
|
||
explicitly stated otherwise. Test vectors, where present, are dedicated to the
|
||
public domain under CC0 1.0.
|
||
|
||
|
||
---
|
||
|
||
## 0. Overview and Conventions
|
||
|
||
`PEL/1-SURF` defines the **store-backed execution surface** for PEL:
|
||
|
||
> Given:
|
||
> * a Store Instance,
|
||
> * a scheme (`SchemeRef`),
|
||
> * a program (`program_ref`),
|
||
> * zero or more input references,
|
||
> * and optional parameters,
|
||
>
|
||
> it:
|
||
>
|
||
> * resolves those references via `ASL/1-STORE`,
|
||
> * applies the pure scheme-level function `Exec_s` from `PEL/1-CORE`,
|
||
> * persists outputs and a surface `ExecutionResult` artifact,
|
||
> * and returns the output references and the result reference.
|
||
|
||
This surface:
|
||
|
||
* is what real engines expose,
|
||
* wires PEL’s pure value semantics to the content-addressable store,
|
||
* produces canonical artifacts that TGK/1-CORE, FER/1, FCT/1, and overlays can consume.
|
||
|
||
RFC 2119 terms (**MUST**, **SHOULD**, **MAY**, etc.) apply.
|
||
|
||
`PEL/1-SURF` uses `Artifact`, `TypeTag`, `Reference`, `HashId` exactly as defined in `ASL/1-CORE`.
|
||
|
||
---
|
||
|
||
## 1. Scope and Non-Goals
|
||
|
||
### 1.1 Purpose
|
||
|
||
`PEL/1-SURF` defines:
|
||
|
||
1. The **run operation**:
|
||
|
||
```text
|
||
run(
|
||
store: StoreInstance,
|
||
scheme_ref: SchemeRef,
|
||
program_ref: ProgramRef,
|
||
input_refs: InputRefList,
|
||
params_ref: optional ParamsRef
|
||
) -> {
|
||
output_refs: OutputRefList,
|
||
result_ref: ResultRef
|
||
}
|
||
````
|
||
|
||
2. How `run(...)`:
|
||
|
||
* interacts with `ASL/1-STORE` (`put` / `get`),
|
||
* invokes the PEL/1-CORE scheme function `Exec_s`,
|
||
* maps store-resolution failures into deterministic outcomes,
|
||
* and produces a canonical **surface ExecutionResult artifact**.
|
||
|
||
3. The structure and semantics of the **surface ExecutionResult artifact**, which:
|
||
|
||
* embeds the `ExecutionResultValue` from `PEL/1-CORE`,
|
||
* echoes the full set of input/output refs,
|
||
* optionally attaches store-resolution diagnostics.
|
||
|
||
### 1.2 Explicit Non-Goals
|
||
|
||
`PEL/1-SURF` does **not** define:
|
||
|
||
* Scheme-specific program structures (DAG, bytecode, WASM, etc.).
|
||
* Encoding formats for programs, inputs, params, or outputs (scheme profiles do).
|
||
* Graph/provenance edges (TGK/1-CORE).
|
||
* Certificates, receipts, or fact semantics (CIL/1, FER/1, FCT/1).
|
||
* Scheduling, queuing, or distributed execution strategies.
|
||
* Access control, secrecy, or multi-tenant policies.
|
||
* Encoding details of the ExecutionResult artifact (`ENC/PEL1-RESULT/1` covers this).
|
||
* Store topology, replication, or GC behavior.
|
||
|
||
`PEL/1-SURF` is strictly about:
|
||
|
||
> **Given store + refs + scheme → how to run and what artifacts MUST be created.**
|
||
|
||
---
|
||
|
||
## 2. Types and Dependencies
|
||
|
||
### 2.1 SchemeRef and aliases
|
||
|
||
From `PEL/1-CORE`:
|
||
|
||
```text
|
||
SchemeRef = Reference
|
||
```
|
||
|
||
For readability, `PEL/1-SURF` defines the following aliases (all of which are simply `Reference`):
|
||
|
||
```text
|
||
ProgramRef = Reference
|
||
InputRef = Reference
|
||
OutputRef = Reference
|
||
ParamsRef = Reference
|
||
ResultRef = Reference
|
||
TraceRef = Reference
|
||
```
|
||
|
||
Type aliases for lists:
|
||
|
||
```text
|
||
InputRefList = [InputRef] // ordered, finite
|
||
OutputRefList = [OutputRef] // ordered, finite
|
||
```
|
||
|
||
### 2.2 StoreInstance (from ASL/1-STORE)
|
||
|
||
A **StoreInstance** is any component conforming to `ASL/1-STORE v0.4.x`, with a `StoreConfig`:
|
||
|
||
```text
|
||
StoreConfig {
|
||
encoding_profile: EncodingProfileId // e.g. ASL_ENC_CORE_V1
|
||
hash_id: HashId // e.g. 0x0001 (HASH-ASL1-256)
|
||
}
|
||
```
|
||
|
||
`PEL/1-SURF` interacts with the store only via:
|
||
|
||
```text
|
||
put(A: Artifact) -> Reference
|
||
|
||
get(R: Reference) ->
|
||
Artifact
|
||
| ERR_NOT_FOUND
|
||
| ERR_INTEGRITY
|
||
| ERR_UNSUPPORTED
|
||
```
|
||
|
||
as defined in `ASL/1-STORE`. The store MAY expose more operations, but `PEL/1-SURF` MUST NOT depend on them.
|
||
|
||
All `program_ref`, `input_refs`, `params_ref`, and `result_ref` values are interpreted relative to the `StoreConfig` used by the StoreInstance.
|
||
|
||
---
|
||
|
||
## 3. Surface Execution Model
|
||
|
||
### 3.1 Conceptual run signature
|
||
|
||
At the surface level, a **run** is:
|
||
|
||
```text
|
||
run(
|
||
store: StoreInstance,
|
||
scheme_ref: SchemeRef,
|
||
program_ref: ProgramRef,
|
||
input_refs: InputRefList,
|
||
params_ref: optional ParamsRef
|
||
) -> {
|
||
output_refs: OutputRefList,
|
||
result_ref: ResultRef
|
||
}
|
||
```
|
||
|
||
All references are interpreted relative to `store`’s `StoreConfig`.
|
||
|
||
### 3.2 Relationship to PEL/1-CORE
|
||
|
||
For a supported scheme identified by `scheme_ref`, there exists a pure function `Exec_s` per `PEL/1-CORE`:
|
||
|
||
```text
|
||
Exec_s :
|
||
(program: Artifact, inputs: list<Artifact>, params: optional Artifact)
|
||
-> (outputs: list<Artifact>, result: ExecutionResultValue)
|
||
```
|
||
|
||
`PEL/1-SURF` defines `run(...)` such that, whenever:
|
||
|
||
* `scheme_ref` is supported,
|
||
* `program_ref` and all `input_refs` (and `params_ref`, if provided) resolve successfully from `store`,
|
||
|
||
then:
|
||
|
||
* `run(...)` MUST behave as if it:
|
||
|
||
1. fetched `program`, `inputs`, `params` from `store`,
|
||
2. invoked `Exec_s(program, inputs, params)`, and
|
||
3. persisted `outputs` and `ExecutionResultValue` as Artifacts in `store`.
|
||
|
||
Determinism and purity of `Exec_s` are guaranteed by `PEL/1-CORE`. `PEL/1-SURF` adds the store wiring and the definition of the surface ExecutionResult artifact.
|
||
|
||
---
|
||
|
||
## 4. Surface ExecutionResult Artifact
|
||
|
||
### 4.1 SurfaceExecutionResult (logical structure)
|
||
|
||
`PEL/1-SURF` defines the **logical payload** of the surface ExecutionResult artifact as:
|
||
|
||
```text
|
||
SurfaceExecutionResult {
|
||
pel1_version : uint16
|
||
|
||
core_result : ExecutionResultValue
|
||
|
||
scheme_ref : SchemeRef // echo
|
||
program_ref : ProgramRef
|
||
input_refs : InputRefList
|
||
output_refs : OutputRefList
|
||
|
||
params_ref : optional ParamsRef
|
||
|
||
store_failure: optional StoreFailure
|
||
trace_ref : optional TraceRef
|
||
}
|
||
```
|
||
|
||
Where `ExecutionResultValue` is as defined in `PEL/1-CORE`:
|
||
|
||
```text
|
||
ExecutionResultValue {
|
||
pel1_version : uint16
|
||
status : ExecutionStatus
|
||
scheme_ref : SchemeRef
|
||
summary : ExecutionErrorSummary
|
||
diagnostics : list<DiagnosticEntry>
|
||
}
|
||
```
|
||
|
||
and:
|
||
|
||
* `ExecutionStatus ∈ { OK, SCHEME_UNSUPPORTED, INVALID_PROGRAM, INVALID_INPUTS, RUNTIME_FAILED }`
|
||
* `ExecutionErrorSummary { kind: ExecutionErrorKind, status_code: uint32 }`
|
||
* `DiagnosticEntry { code: uint32, message: OctetString }`
|
||
|
||
(see `PEL/1-CORE` for full semantics).
|
||
|
||
### 4.2 StoreFailure classification
|
||
|
||
`PEL/1-SURF` refines store-resolution errors via `StoreFailure`:
|
||
|
||
```text
|
||
StoreErrorCode = uint8
|
||
|
||
StoreErrorCode {
|
||
NOT_FOUND = 1 // Store returned ERR_NOT_FOUND
|
||
INTEGRITY = 2 // Store returned ERR_INTEGRITY
|
||
UNSUPPORTED = 3 // Store returned ERR_UNSUPPORTED
|
||
}
|
||
|
||
StoreFailurePhase = uint8
|
||
|
||
StoreFailurePhase {
|
||
PROGRAM = 1
|
||
INPUT = 2
|
||
}
|
||
|
||
StoreFailure {
|
||
phase : StoreFailurePhase
|
||
error_code : StoreErrorCode
|
||
failing_ref : Reference
|
||
}
|
||
```
|
||
|
||
Semantics:
|
||
|
||
* `phase = PROGRAM` indicates the failure happened while resolving `program_ref`.
|
||
* `phase = INPUT` indicates it happened while resolving an input or `params_ref`.
|
||
* `failing_ref` MUST be the exact `Reference` passed to `get` that produced the error.
|
||
* `error_code` MUST match the store’s reported error.
|
||
|
||
### 4.3 TypeTag and encoding
|
||
|
||
The concrete surface ExecutionResult artifact is an `Artifact` with:
|
||
|
||
* `type_tag = PEL1_SURFACE_EXECUTION_RESULT_TAG`
|
||
* `bytes` = canonical encoding of `SurfaceExecutionResult` under `ENC/PEL1-RESULT/1`.
|
||
|
||
This specification:
|
||
|
||
* Reserves the symbolic `PEL1_SURFACE_EXECUTION_RESULT_TAG` for this purpose (concretized by `ENC/PEL1-RESULT/1`).
|
||
* Defers the concrete `tag_id`, `CoreResultBytes`, and `SurfaceExecutionResultBytes` layout to `ENC/PEL1-RESULT/1`.
|
||
* Requires that, for any given logical `SurfaceExecutionResult`, there is exactly one canonical encoding, satisfying ASL/1-CORE’s canonical encoding constraints.
|
||
|
||
---
|
||
|
||
## 5. Normative Behavior of `run(...)`
|
||
|
||
### 5.1 High-level phases
|
||
|
||
The behavior of:
|
||
|
||
```text
|
||
run(store, scheme_ref, program_ref, input_refs, params_ref)
|
||
```
|
||
|
||
is defined in terms of five conceptual phases:
|
||
|
||
1. **Scheme support check**
|
||
2. **Program resolution**
|
||
3. **Input and parameter resolution**
|
||
4. **Scheme execution (`Exec_s`)**
|
||
5. **Persistence of outputs and surface result**
|
||
|
||
Implementations MAY pipeline or parallelize internally, but the observable behavior (artifacts written and references returned) MUST match the sequential semantics described here.
|
||
|
||
### 5.2 Scheme support check
|
||
|
||
The engine first determines whether it **supports** the scheme identified by `scheme_ref`:
|
||
|
||
* If the scheme is **not supported**:
|
||
|
||
* The engine MUST NOT attempt to resolve `program_ref` or any `input_refs` / `params_ref`.
|
||
|
||
* It MUST construct `core_result : ExecutionResultValue` with:
|
||
|
||
```text
|
||
pel1_version = 1
|
||
status = SCHEME_UNSUPPORTED
|
||
scheme_ref = scheme_ref
|
||
summary.kind = SCHEME
|
||
summary.status_code = 1 // canonical core code for SCHEME_UNSUPPORTED
|
||
diagnostics = [] // or deterministic scheme-agnostic diagnostics
|
||
```
|
||
|
||
in accordance with `PEL/1-CORE`.
|
||
|
||
* It MUST construct a `SurfaceExecutionResult` with:
|
||
|
||
```text
|
||
pel1_version = 1
|
||
|
||
core_result = (as above)
|
||
scheme_ref = scheme_ref
|
||
program_ref = program_ref // echo input
|
||
input_refs = input_refs // echo input
|
||
output_refs = [] // no outputs
|
||
|
||
params_ref = params_ref // echo input
|
||
|
||
store_failure = absent
|
||
trace_ref = absent
|
||
```
|
||
|
||
* It MUST encode this as an `Artifact` with `type_tag = PEL1_SURFACE_EXECUTION_RESULT_TAG`, and call:
|
||
|
||
```text
|
||
put(surface_result_artifact) -> result_ref
|
||
```
|
||
|
||
* It MUST return:
|
||
|
||
```text
|
||
output_refs = []
|
||
result_ref = result_ref
|
||
```
|
||
|
||
* If the scheme **is supported**, execution proceeds to program resolution.
|
||
|
||
Whether a scheme is supported is implementation-specific (registry, plugin, etc.), but the observable effect MUST match this specification.
|
||
|
||
### 5.3 Program resolution
|
||
|
||
If the scheme is supported, the engine MUST resolve `program_ref`:
|
||
|
||
```text
|
||
get(program_ref) ->
|
||
program : Artifact
|
||
| ERR_NOT_FOUND
|
||
| ERR_INTEGRITY
|
||
| ERR_UNSUPPORTED
|
||
```
|
||
|
||
* If `get(program_ref)` returns an `Artifact`, execution proceeds to input/params resolution.
|
||
|
||
* If it returns an error:
|
||
|
||
* The engine MUST NOT call `Exec_s`.
|
||
|
||
* It MUST map the store error to `StoreErrorCode`:
|
||
|
||
```text
|
||
ERR_NOT_FOUND -> NOT_FOUND
|
||
ERR_INTEGRITY -> INTEGRITY
|
||
ERR_UNSUPPORTED -> UNSUPPORTED
|
||
```
|
||
|
||
* It MUST construct `core_result` with:
|
||
|
||
```text
|
||
pel1_version = 1
|
||
status = INVALID_PROGRAM
|
||
scheme_ref = scheme_ref
|
||
summary.kind = PROGRAM
|
||
summary.status_code = 2 // canonical core code for INVALID_PROGRAM
|
||
diagnostics = [] or deterministic diagnostics
|
||
```
|
||
|
||
obeying the invariants in `PEL/1-CORE`.
|
||
|
||
* It MUST construct `store_failure`:
|
||
|
||
```text
|
||
store_failure = {
|
||
phase = PROGRAM
|
||
error_code = mapped StoreErrorCode
|
||
failing_ref = program_ref
|
||
}
|
||
```
|
||
|
||
* It MUST construct and persist a `SurfaceExecutionResult` with:
|
||
|
||
```text
|
||
pel1_version = 1
|
||
|
||
core_result = as above
|
||
scheme_ref = scheme_ref
|
||
program_ref = program_ref
|
||
input_refs = input_refs
|
||
output_refs = []
|
||
|
||
params_ref = params_ref
|
||
|
||
store_failure = (as above)
|
||
trace_ref = absent
|
||
```
|
||
|
||
* It MUST return `output_refs = []`, `result_ref = put(surface_result_artifact)`.
|
||
|
||
### 5.4 Input and parameter resolution
|
||
|
||
If program resolution succeeded, the engine MUST resolve `input_refs` in order, and, if `params_ref` is present, resolve it as well.
|
||
|
||
For each `input_ref` in `input_refs`:
|
||
|
||
```text
|
||
get(input_ref) ->
|
||
input : Artifact
|
||
| ERR_NOT_FOUND
|
||
| ERR_INTEGRITY
|
||
| ERR_UNSUPPORTED
|
||
```
|
||
|
||
If all `input_refs` resolve to Artifacts, and `params_ref` is absent, or present and resolves successfully via:
|
||
|
||
```text
|
||
get(params_ref) -> params : Artifact | error
|
||
```
|
||
|
||
then execution proceeds to scheme execution (§5.5).
|
||
|
||
If **any** resolution fails:
|
||
|
||
* Let `failing_ref` be the first reference (in the order: all `input_refs` followed by `params_ref`, if present) for which `get` returned an error.
|
||
* Map the store error as in §5.3.
|
||
* The engine MUST NOT call `Exec_s`.
|
||
|
||
It MUST then construct `core_result` with:
|
||
|
||
```text
|
||
pel1_version = 1
|
||
status = INVALID_INPUTS
|
||
scheme_ref = scheme_ref
|
||
summary.kind = INPUTS
|
||
summary.status_code = 3 // canonical core code for INVALID_INPUTS
|
||
diagnostics = [] or deterministic diagnostics
|
||
```
|
||
|
||
It MUST construct `store_failure`:
|
||
|
||
```text
|
||
store_failure = {
|
||
phase = INPUT
|
||
error_code = mapped StoreErrorCode
|
||
failing_ref = failing_ref
|
||
}
|
||
```
|
||
|
||
And construct `SurfaceExecutionResult`:
|
||
|
||
```text
|
||
pel1_version = 1
|
||
|
||
core_result = as above
|
||
scheme_ref = scheme_ref
|
||
program_ref = program_ref
|
||
input_refs = input_refs
|
||
output_refs = [] // no outputs
|
||
|
||
params_ref = params_ref
|
||
|
||
store_failure = (as above)
|
||
trace_ref = absent
|
||
```
|
||
|
||
It MUST persist this artifact and return `output_refs = []`, `result_ref` accordingly.
|
||
|
||
### 5.5 Scheme execution via PEL/1-CORE
|
||
|
||
If:
|
||
|
||
* `scheme_ref` is supported,
|
||
* `program_ref` resolves to `program : Artifact`,
|
||
* all `input_refs` resolve to `inputs : list<Artifact>`,
|
||
* `params_ref`, if present, resolves to `params : Artifact`,
|
||
|
||
then the engine MUST invoke the scheme-level PEL/1-CORE function:
|
||
|
||
```text
|
||
Exec_s(
|
||
program : Artifact,
|
||
inputs : list<Artifact>,
|
||
params : optional Artifact
|
||
) -> (outputs : list<Artifact>, core_result : ExecutionResultValue)
|
||
```
|
||
|
||
with the following constraints:
|
||
|
||
* The `scheme_ref` used for `Exec_s` MUST be the same value passed into `run`.
|
||
* The engine MUST ensure that the scheme implementation of `Exec_s` conforms to `PEL/1-CORE`:
|
||
|
||
* `core_result.pel1_version = 1`,
|
||
* `core_result.scheme_ref = scheme_ref`,
|
||
* `core_result.status`, `core_result.summary`, and `core_result.diagnostics` obey the PEL/1-CORE invariants.
|
||
|
||
If the scheme-level implementation of `Exec_s` violates PEL/1-CORE invariants (e.g., sets `scheme_ref` incorrectly), that is an implementation bug; `PEL/1-SURF` does not attempt to repair it, but conformance tests SHOULD reject such engines.
|
||
|
||
### 5.6 Persisting outputs and surface result
|
||
|
||
Given the `outputs` and `core_result` from `Exec_s`:
|
||
|
||
1. For each output Artifact in `outputs` (in order):
|
||
|
||
```text
|
||
put(output_artifact) -> output_ref
|
||
```
|
||
|
||
Collect the resulting `output_refs : OutputRefList` in the same order.
|
||
|
||
Implementations MUST respect `ASL/1-STORE` semantics: repeated `put` of the same Artifact is idempotent.
|
||
|
||
2. Optionally, schemes MAY define how a separate **trace artifact** is produced (e.g., as one of the outputs). If the engine or scheme logic identifies a dedicated `trace_ref : TraceRef`:
|
||
|
||
* It MAY set the `trace_ref` field in `SurfaceExecutionResult` accordingly.
|
||
* It MUST ensure that any `trace_ref` it sets is resolvable in the same StoreInstance (unless policy explicitly allows otherwise).
|
||
|
||
3. The engine MUST construct a `SurfaceExecutionResult`:
|
||
|
||
```text
|
||
SurfaceExecutionResult {
|
||
pel1_version = 1
|
||
|
||
core_result = core_result // as returned by Exec_s
|
||
|
||
scheme_ref = scheme_ref
|
||
program_ref = program_ref
|
||
input_refs = input_refs
|
||
output_refs = output_refs
|
||
|
||
params_ref = params_ref
|
||
|
||
store_failure = absent
|
||
trace_ref = trace_ref or absent
|
||
}
|
||
```
|
||
|
||
4. It MUST encode this as an `Artifact` with:
|
||
|
||
* `type_tag = PEL1_SURFACE_EXECUTION_RESULT_TAG`
|
||
* `bytes` = canonical encoding per `ENC/PEL1-RESULT/1` (or equivalent profile).
|
||
|
||
Then call:
|
||
|
||
```text
|
||
put(surface_result_artifact) -> result_ref
|
||
```
|
||
|
||
5. It MUST return:
|
||
|
||
```text
|
||
output_refs = output_refs
|
||
result_ref = result_ref
|
||
```
|
||
|
||
### 5.7 Fatal store write failures
|
||
|
||
If any `put(...)` call for:
|
||
|
||
* outputs, or
|
||
* the surface result artifact,
|
||
|
||
fails in a way that prevents the store from persisting the Artifact (e.g., I/O failure, permission error, out-of-space):
|
||
|
||
* `PEL/1-SURF` treats this as an **environment failure**, outside its semantic model.
|
||
* There is no defined `SurfaceExecutionResult` in this case.
|
||
* Implementations MAY signal such errors via implementation-specific APIs, logs, or metrics, but they are not represented as valid ExecutionResult artifacts under this spec.
|
||
|
||
---
|
||
|
||
## 6. Error and Status Semantics
|
||
|
||
### 6.1 Mapping of high-level cases
|
||
|
||
`PEL/1-SURF` distinguishes:
|
||
|
||
1. **Scheme unsupported**
|
||
|
||
* Handled in §5.2.
|
||
* No calls to `get` or `Exec_s`.
|
||
* `core_result.status = SCHEME_UNSUPPORTED`.
|
||
* `store_failure = absent`.
|
||
|
||
2. **Program resolution failure**
|
||
|
||
* Handled in §5.3.
|
||
* `Exec_s` is not invoked.
|
||
* `core_result.status = INVALID_PROGRAM`.
|
||
* `store_failure.phase = PROGRAM`.
|
||
|
||
3. **Input/params resolution failure**
|
||
|
||
* Handled in §5.4.
|
||
* `Exec_s` is not invoked.
|
||
* `core_result.status = INVALID_INPUTS`.
|
||
* `store_failure.phase = INPUT`.
|
||
|
||
4. **Successful scheme execution**
|
||
|
||
* Handled in §5.5–§5.6.
|
||
|
||
* `Exec_s` is invoked and `core_result.status` is determined by scheme semantics:
|
||
|
||
* `OK` — scheme-level success.
|
||
* `INVALID_PROGRAM` — scheme-level program invalidity (e.g., bad DAG, invalid bytecode) after decoding.
|
||
* `INVALID_INPUTS` — scheme-level input invalidity (e.g., type mismatch or decode failure).
|
||
* `RUNTIME_FAILED` — scheme-level runtime error.
|
||
|
||
* `store_failure = absent`.
|
||
|
||
### 6.2 Distinguishing store vs scheme errors
|
||
|
||
Because `INVALID_PROGRAM` and `INVALID_INPUTS` may arise from either:
|
||
|
||
* **Store-level** failures (resolution errors before `Exec_s`), or
|
||
* **Scheme-level** failures (Exec_s returning those statuses),
|
||
|
||
`PEL/1-SURF` uses `store_failure` to distinguish:
|
||
|
||
* If `store_failure` is **present**, the INVALID_* status indicates a **store-resolution** issue.
|
||
* If `store_failure` is **absent**, INVALID_* indicates a **scheme-level** validation error.
|
||
|
||
This allows higher layers (e.g., TGK/1-CORE or FER/1) to tell whether:
|
||
|
||
* they failed to even read the program/inputs, or
|
||
* the scheme rejected them as invalid content.
|
||
|
||
### 6.3 Consistency requirements
|
||
|
||
For any `SurfaceExecutionResult`:
|
||
|
||
* `surface.pel1_version` MUST equal `surface.core_result.pel1_version`.
|
||
* `surface.core_result.scheme_ref` MUST equal `surface.scheme_ref`.
|
||
* `surface.output_refs` length MUST equal the length of `outputs` from `Exec_s` (or zero if `Exec_s` was not called).
|
||
* When `store_failure` is present:
|
||
|
||
* `surface.core_result.status` MUST be either `INVALID_PROGRAM` or `INVALID_INPUTS` as per §5.3–§5.4.
|
||
* `surface.core_result.summary.kind` MUST be `PROGRAM` or `INPUTS` accordingly.
|
||
|
||
---
|
||
|
||
## 7. Determinism and Reproducibility
|
||
|
||
### 7.1 Determinism with respect to store state
|
||
|
||
Fix:
|
||
|
||
* A StoreInstance with state `S`, representing a mapping `Reference -> Artifact` (ignoring environment failures).
|
||
* A tuple of arguments:
|
||
|
||
```text
|
||
(scheme_ref, program_ref, input_refs, params_ref)
|
||
```
|
||
|
||
`PEL/1-SURF` requires:
|
||
|
||
* For any two conformant PEL/1-SURF engines using the same store state `S` and arguments above:
|
||
|
||
* If no environment failures occur (e.g., all `get`/`put` operations conform to `ASL/1-STORE` and succeed or fail deterministically), then:
|
||
|
||
* The set of new Artifacts written to the store by `run(...)` MUST be equal (as `Artifact` values per ASL/1-CORE).
|
||
* The returned `output_refs` MUST be identical (`Reference` values, same order).
|
||
* The returned `result_ref` MUST be identical (`Reference` value).
|
||
* The stored surface result artifacts for the run MUST have equal `SurfaceExecutionResult` payloads.
|
||
|
||
### 7.2 Determinism boundaries
|
||
|
||
Sources of variation explicitly **outside** the PEL/1-SURF model:
|
||
|
||
* Underlying store behavior that violates `ASL/1-STORE` semantics (e.g., non-repeatable `get`/`put`).
|
||
* Environment failures (e.g., abrupt program termination, hardware faults).
|
||
* Nondeterminism in scheme implementations that violate `PEL/1-CORE` purity/determinism.
|
||
|
||
`PEL/1-SURF` assumes:
|
||
|
||
* The store conforms to `ASL/1-STORE`.
|
||
* The scheme implementations conform to `PEL/1-CORE`.
|
||
* Host-level failures are treated as out-of-model.
|
||
|
||
---
|
||
|
||
## 8. Interaction with Higher Layers (Informative)
|
||
|
||
### 8.1 TGK/1-CORE — Trace Graph Kernel
|
||
|
||
TGK/1-CORE can interpret:
|
||
|
||
* `program_ref`, `input_refs`, `output_refs`, `result_ref`, and
|
||
* the surface ExecutionResult artifact,
|
||
|
||
to derive provenance edges such as:
|
||
|
||
* “run R (result_ref) executed program P with inputs I* to produce outputs O*”.
|
||
|
||
The `trace_ref` (if used) or scheme-specific trace artifacts can be used to add fine-grained per-node or per-step edges (e.g., in a DAG program profile).
|
||
|
||
### 8.2 FER/1 and FCT/1 — Evidence and Facts
|
||
|
||
FER/1 and FCT/1 can treat:
|
||
|
||
* `result_ref` as the entry point to the execution evidence,
|
||
* the referenced surface ExecutionResult artifact as core evidence,
|
||
* `output_refs` as the produced artifacts to be certified or turned into facts.
|
||
|
||
The clear separation between store-level failures (`store_failure`) and scheme-level failures (core status) makes it possible to distinguish “we couldn’t even run this” from “we ran it and it failed for domain-specific reasons.”
|
||
|
||
### 8.3 Scheme and profile binding
|
||
|
||
Scheme-specific profiles (e.g., DAG programs, WASM schemes) can:
|
||
|
||
* Define how `program_ref`, `input_refs`, and `params_ref` are expected to be formed.
|
||
* Define structured trace formats and how `trace_ref` is chosen.
|
||
* Provide conformance tests for `Exec_s` and for how schemes map to PEL/1-SURF.
|
||
|
||
`PEL/1-SURF` itself remains agnostic to specific schemes; it only enforces wiring and error classification.
|
||
|
||
---
|
||
|
||
## 9. Conformance
|
||
|
||
An implementation is **PEL/1-SURF–conformant** if, for each StoreInstance it uses and for each supported scheme, it:
|
||
|
||
1. **Implements `run(...)` as specified**
|
||
|
||
* Accepts `(store, scheme_ref, program_ref, input_refs, params_ref)` arguments.
|
||
* Follows the phase structure of §5.
|
||
* Uses only `ASL/1-STORE` `get` / `put` to interact with the store.
|
||
* Does not mutate the store in ways that violate `ASL/1-STORE` semantics (no identity rewrites).
|
||
|
||
2. **Respects PEL/1-CORE semantics**
|
||
|
||
* Uses a PEL/1-CORE-conformant implementation of `Exec_s` for each supported `scheme_ref`.
|
||
* Produces `ExecutionResultValue` conforming to `PEL/1-CORE` requirements.
|
||
* Ensures `core_result.scheme_ref = scheme_ref`.
|
||
|
||
3. **Handles scheme support correctly**
|
||
|
||
* For unsupported schemes, never calls `get` / `Exec_s`, and produces the canonical `SCHEME_UNSUPPORTED` result as in §5.2.
|
||
|
||
4. **Handles store-resolution failures correctly**
|
||
|
||
* Implements program and input/params resolution as in §5.3–§5.4.
|
||
* Maps store errors to `StoreFailure` and `INVALID_PROGRAM` / `INVALID_INPUTS` statuses appropriately.
|
||
* Distinguishes store-level errors using `store_failure`.
|
||
|
||
5. **Persists outputs and surface results correctly**
|
||
|
||
* For successful execution, persists outputs via `put`, collects `output_refs`, constructs a `SurfaceExecutionResult` with:
|
||
|
||
* `core_result` exactly as returned by `Exec_s`,
|
||
* `scheme_ref`, `program_ref`, `input_refs`, `output_refs`, `params_ref` echoed,
|
||
* `store_failure = absent`.
|
||
|
||
* Persists the surface result artifact with `type_tag = PEL1_SURFACE_EXECUTION_RESULT_TAG`.
|
||
|
||
* Returns `output_refs` and `result_ref` matching the store state.
|
||
|
||
6. **Is deterministic with respect to store state**
|
||
|
||
* Satisfies the determinism requirements of §7 across all conformant engines, given the same store state and run arguments.
|
||
|
||
7. **Maintains layering**
|
||
|
||
* Does not depend on TGK/1-CORE, CIL/1, FER/1, FCT/1, or overlay systems on the execution hot path.
|
||
* Treats graph, certificates, and policies as **consumers** of the surface result, not as dependencies of `run`.
|
||
|
||
Everything else — concrete language bindings, protocol endpoints (HTTP, gRPC), orchestration, logging, metrics, sandboxing, resource limits — is implementation or profile behavior and is outside the scope of this specification, provided the normative behavior above is preserved.
|
||
|
||
---
|
||
|
||
*End of `PEL/1-SURF v0.2.1 — Primitive Execution Surface (Store-Backed)`*
|
||
|
||
---
|
||
|
||
## Document History
|
||
|
||
* **0.2.1 (2025-11-16):** Registered as Tier-1 spec and aligned to the Amduat 2.0 substrate baseline.
|
||
|
||
* **0.2.2 (2025-11-30):** Linked surface ExecutionResult artifacts to ENC/PEL1-RESULT/1 profile.
|