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.
|