amduat/tier1/pel-1-core.md

640 lines
20 KiB
Markdown
Raw Permalink Normal View History

2025-12-20 12:35:10 +01:00
# PEL/1-CORE — Primitive Execution Layer (Core Semantics)
Status: Approved
Owner: Niklas Rydberg
Version: 0.3.0
SoT: Yes
Last Updated: 2025-11-16
Linked Phase Pack: N/A
Tags: [execution, deterministic]
<!-- Source: /amduat/docs/new/pel1-core.md | Canonical: /amduat/tier1/pel-1-core.md -->
**Document ID:** `PEL/1-CORE`
**Layer:** L1 — Kernel execution semantics (pure value model)
**Depends on (normative):**
* `ASL/1-CORE v0.4.x` — Artifact Substrate (logical value model)
* `SUBSTRATE/STACK-OVERVIEW v0.1.x` — kernel layering and invariants
**Integrates with (informative):**
* `ENC/ASL1-CORE v1` — canonical encodings for Artifacts/References
* `HASH/ASL1 v0.2.x` — ASL1 hash family (identity handles)
* `ASL/1-STORE v0.4.x` — content-addressable store semantics
* `PEL/1-SURF` (planned) — store-backed execution surface
* `PEL/PROGRAM-DAG/1` (planned) — DAG-style program/profile
* `PEL/TRACE-DAG/1` (planned) — structured node-level execution trace
© 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. Conventions
The key words **MUST**, **MUST NOT**, **SHOULD**, **MAY**, etc. are to be interpreted as described in RFC 2119.
`PEL/1-CORE` uses the ASL/1-CORE value model:
```text
Artifact {
bytes: OctetString
type_tag: optional TypeTag
}
TypeTag {
tag_id: uint32
}
Reference {
hash_id: HashId
digest: OctetString
}
HashId = uint16
```
`PEL/1-CORE`:
* does **not** modify Artifact / Reference identity or equality,
* does **not** introduce new identity schemes,
* defines only **logical value semantics** — no storage layouts, protocols, or APIs.
It is independent of:
* any particular encoding profile,
* any hash-family choice,
* any store, graph, or certification system.
---
## 1. Purpose & Scope
### 1.1 Purpose
`PEL/1-CORE` defines the **minimal kernel execution semantics** for Amduat 2.0:
* Execution is expressed as **pure, deterministic functions over Artifacts**.
* A **scheme** defines how a program Artifact and input Artifacts are interpreted.
* For a given scheme, program, inputs, and optional parameters, execution produces:
* a list of **output Artifacts**, and
* a scheme-level **ExecutionResultValue** describing the outcome.
The goal is a **timeless, deterministic, storage- and graph-neutral execution substrate** that:
* can be implemented as “metal-fast” engines (compiled, no dynamic dependency web), and
* can be wired into stores, provenance, and certification without entangling with them on the hot path.
### 1.2 Non-Goals
`PEL/1-CORE` explicitly does **not** define:
* Store semantics (`put`/`get`, authority, replication, GC).
* Graph/provenance edges (`TGK/1` and its profiles).
* Certification, signatures, or trust semantics (`CIL/1`, `FER/1`, `FCT/1`).
* Scheduling, work queues, or distributed orchestration.
* Authentication, authorization, or access control.
* Real-world time, randomness, or I/O APIs.
* Structure of program Artifacts (DAG vs non-DAG) — those are defined by **scheme profiles**.
All of these concerns live **above** or **around** `PEL/1-CORE`.
---
## 2. Core Concepts
### 2.1 SchemeRef
A **scheme** defines a particular execution semantics (language, calling convention, program structure, etc.).
At the core level, a scheme is identified by a `SchemeRef`:
```text
SchemeRef = Reference // ASL/1-CORE Reference
```
* `SchemeRef` refers to a **scheme descriptor Artifact**.
* `PEL/1-CORE` does not prescribe the content or `TypeTag` of that descriptor; those are defined by scheme-specific profiles (`PEL/SCHEME/...`).
* Distinct scheme descriptors MUST have distinct `SchemeRef` values (different content ⇒ different digest under ASL/1-CORE).
### 2.2 Logical Execution Call
At the value level, an execution is modeled as an **ExecutionCall**:
```text
ExecutionCall {
scheme_ref : SchemeRef
program : Artifact
inputs : list<Artifact>
params : optional Artifact
}
```
Where:
* `scheme_ref` selects which schemes semantics apply.
* `program` is the program Artifact.
* `inputs` is an ordered list of input Artifacts.
* `params` is an optional parameters Artifact.
`PEL/1-CORE` does **not** constrain the internal structure of `program`, `inputs`, or `params`; that is scheme-level.
For a scheme `s` identified by `scheme_ref`, there exists a **total** pure function:
```text
Exec_s :
(program: Artifact, inputs: list<Artifact>, params: optional Artifact)
-> (outputs: list<Artifact>, result: ExecutionResultValue)
```
> **PEL/TOTALITY/1**
> For every scheme that an environment claims to support, `Exec_s` MUST be total over all possible `(program, inputs, params)` triples: it MUST always return a well-formed `(outputs, ExecutionResultValue)` pair, never “fall off the edge” (crash, panic) in-model. Invalid combinations must be mapped to appropriate error statuses, not to undefined behavior.
Totality at this level excludes environment failures (see §4.4).
### 2.3 ExecutionStatus and ExecutionErrorKind
`PEL/1-CORE` defines a shared classification of execution outcomes.
```text
ExecutionStatus = uint8
ExecutionErrorKind = uint8
```
`ExecutionStatus` codes:
```text
ExecutionStatus {
OK = 0
SCHEME_UNSUPPORTED = 1
INVALID_PROGRAM = 2
INVALID_INPUTS = 3
RUNTIME_FAILED = 4
}
```
* `OK` — execution completed successfully under the scheme semantics.
* `SCHEME_UNSUPPORTED` — the environment does not implement the scheme identified by `scheme_ref`.
* `INVALID_PROGRAM` — the program Artifact cannot be interpreted as a valid program under the scheme.
* `INVALID_INPUTS` — inputs or parameters are invalid for the scheme.
* `RUNTIME_FAILED` — the scheme executed but signaled a deterministic failure (e.g., explicit error, assertion failure).
`ExecutionErrorKind` refines the source:
```text
ExecutionErrorKind {
NONE = 0
SCHEME = 1 // scheme support/descriptor issues
PROGRAM = 2 // invalid program under scheme
INPUTS = 3 // invalid inputs/params under scheme
RUNTIME = 4 // runtime failure under scheme
}
```
Future values MAY be defined, but MUST maintain compatibility with existing meanings.
### 2.4 ExecutionErrorSummary
`ExecutionErrorSummary` gives a compact, deterministic classification:
```text
ExecutionErrorSummary {
kind : ExecutionErrorKind
status_code : uint32 // 0 for success; non-zero for error
}
```
Semantics:
* If `status = OK`:
* `kind` MUST be `NONE`.
* `status_code` MUST be `0`.
* If `status = SCHEME_UNSUPPORTED`:
* `kind` MUST be `SCHEME`.
* `status_code` SHOULD be the canonical core code `1`.
* If `status = INVALID_PROGRAM`:
* `kind` MUST be `PROGRAM`.
* `status_code` SHOULD be the canonical core code `2`.
* If `status = INVALID_INPUTS`:
* `kind` MUST be `INPUTS`.
* `status_code` SHOULD be the canonical core code `3`.
* If `status = RUNTIME_FAILED`:
* `kind` MUST be `RUNTIME`.
* `status_code` MUST be non-zero.
* The concrete `status_code` is **scheme-defined**, but MUST be deterministic.
Scheme profiles MAY define sub-ranges of `status_code` for category grouping but MUST respect these invariants.
### 2.5 DiagnosticEntry
Schemes MAY provide additional deterministic diagnostics via `DiagnosticEntry`:
```text
DiagnosticEntry {
code : uint32 // scheme-defined code
message : OctetString // scheme-defined bytes (SHOULD be UTF-8 text)
}
```
Requirements:
* For a given execution, the list of `DiagnosticEntry` values MUST be **fully deterministic**.
* Diagnostics MUST NOT include:
* wall-clock timestamps,
* random identifiers,
* host IDs, PIDs, or environment-dependent details.
Diagnostics are optional; their interpretation is scheme- or profile-specific.
### 2.6 ExecutionResultValue (logical)
`ExecutionResultValue` is the scheme-level result produced by `Exec_s`:
```text
ExecutionResultValue {
pel1_version : uint16
status : ExecutionStatus
scheme_ref : SchemeRef
summary : ExecutionErrorSummary
diagnostics : list<DiagnosticEntry>
}
```
Semantics:
* `pel1_version`:
* MUST be set to `1` for this version of `PEL/1-CORE`.
* Future versions MAY introduce new result formats under different encodings or TypeTags but MUST NOT change the meaning of `pel1_version = 1` values.
* `status` and `scheme_ref`:
* `status` reflects the outcome as in §2.3.
* `scheme_ref` MUST equal the scheme identifier used for the call.
* `summary`:
* MUST obey §2.4 for the chosen `status`.
* `diagnostics`:
* MAY be empty.
* MUST be deterministic and scheme-defined.
`ExecutionResultValue` is a logical value; its encoding as an `Artifact` is defined by a separate profile (e.g., `ENC/PEL1-RESULT/1`), not by `PEL/1-CORE`.
---
## 3. Execution Schemes
### 3.1 Scheme definition
A **scheme** is the combination of:
* a `SchemeRef` (descriptor Artifact), and
* a concrete semantics `Exec_s`.
For a given `scheme_ref`, a scheme definition MUST specify:
1. **Program representation**
* How `program : Artifact` is interpreted.
* Which `TypeTag` values (if any) indicate valid program Artifacts.
* Structural validity rules (DAG, bytecode, WASM module, etc.).
2. **Input and parameter representation**
* How `inputs : list<Artifact>` are decoded and mapped into the schemes runtime model (arguments, input buffers, configs, etc.).
* How `params : optional Artifact` is interpreted, if used.
3. **Output representation**
* How produced values are encoded as output `Artifact`s.
* Any constraints on `TypeTag` for outputs.
4. **Failure semantics**
* Conditions under which `status` becomes:
* `INVALID_PROGRAM`,
* `INVALID_INPUTS`,
* `RUNTIME_FAILED`.
* How `status_code` is chosen for `RUNTIME_FAILED`.
* Whether and how outputs are produced in each non-`OK` case.
> **PEL/FAIL-OUTPUT/REC/1 (RECOMMENDED)**
> For `SCHEME_UNSUPPORTED`, `INVALID_PROGRAM`, and `INVALID_INPUTS`, schemes SHOULD produce an empty `outputs` list. For `RUNTIME_FAILED`, schemes MAY produce partial outputs, but MUST define that behavior clearly and deterministically.
5. **Deterministic diagnostics**
* Rules for populating `diagnostics` as deterministic functions of `(program, inputs, params)` and the schemes semantics.
Formally, the scheme MUST define a total function:
```text
Exec_s :
(program: Artifact, inputs: list<Artifact>, params: optional Artifact)
-> (outputs: list<Artifact>, result: ExecutionResultValue)
```
that is pure and deterministic (see §4), and always yields:
* `pel1_version = 1`,
* `scheme_ref` equal to the schemes `SchemeRef`,
* a `status` and `summary` consistent with §2.3§2.4.
### 3.2 Scheme support in an environment
At the core level, an environment either:
* **Supports** a scheme identified by `scheme_ref`, in which case it implements `Exec_s`, or
* Does **not** support it, in which case any attempt to execute that scheme MUST yield an `ExecutionResultValue` with:
* `status = SCHEME_UNSUPPORTED`,
* `scheme_ref = scheme_ref`,
* `summary.kind = SCHEME`,
* `summary.status_code = 1` (canonical).
How scheme support is discovered (registries, configuration) is outside `PEL/1-CORE`.
### 3.3 Scheme profiles
Scheme definitions are typically captured in separate documents (e.g., `PEL/SCHEME/WASM-1`, `PEL/PROGRAM-DAG/1`) that:
* Normatively reference `PEL/1-CORE`.
* Provide:
* concrete program/data models,
* concrete error/status mappings,
* conformance vectors for `Exec_s`.
`PEL/1-CORE` itself remains scheme-agnostic.
---
## 4. Determinism and Purity
### 4.1 Determinism contract
For a given scheme:
```text
Exec_s(program, inputs, params) -> (outputs, result)
```
> **PEL/DET/1 — Determinism Invariant**
> For any two **PEL/1-COREconformant** implementations `I1` and `I2` of that scheme, and for any `program : Artifact`, `inputs : list<Artifact>`, `params : optional Artifact`:
>
> ```text
> Exec_s_I1(program, inputs, params)
> == Exec_s_I2(program, inputs, params)
> ```
>
> where:
>
> * `outputs` lists are the same length and pairwise equal as Artifacts (ASL/1-CORE equality), and
> * `ExecutionResultValue` fields are equal (`pel1_version`, `status`, `scheme_ref`, `summary`, and the sequence of `DiagnosticEntry`s).
Determinism MUST hold across:
* platforms,
* architectures,
* implementation languages,
* runtime environments,
given the same scheme definition and the same Artifacts.
### 4.2 Purity requirement
> **PEL/PURITY/1 — Purity Invariant**
> `Exec_s` MUST be a pure function of `(scheme_ref, program, inputs, params)` and the scheme definition:
* No reads from external mutable state:
* No direct filesystem, network, environment variables, OS state, or external databases.
* Any required data MUST be supplied via Artifacts.
* No writes to external state that influence other executions:
* Execution MUST NOT have side effects visible outside its outputs and `ExecutionResultValue`.
* Logging, metrics, or debugging output MUST NOT affect later runs.
* No dependence on:
* wall-clock time,
* random sources (unless seeds are passed as inputs),
* process IDs, memory addresses, or other non-deterministic identifiers.
If a scheme requires time or randomness, these MUST be expressed as input Artifacts.
### 4.3 No graph, certification, or policy dependencies
> **PEL/HOT-PATH-ISOLATION/1**
> PEL/1-CORE execution semantics MUST NOT require:
* any graph backend (`TGK/1`) or provenance structure to compute outputs,
* any certification or trust system (`CIL/1`, `FER/1`, `FCT/1`),
* any governance or policy engine.
Such concerns may be applied **around** `Exec_s` (e.g., to authorize execution, or to interpret the result), but:
* `Exec_s` MUST be definable and implementable **purely** over ASL/1 Artifacts and scheme semantics, and
* no calls into TGK/1, CIL/1, or similar layers are required on the execution hot path.
### 4.4 Environment failures (out of model)
`PEL/1-CORE` does **not** define semantics for **environment failures** such as:
* out-of-memory,
* OS-level crashes or kills,
* implementation bugs or panics in the host environment.
If such failures occur:
* No `(outputs, ExecutionResultValue)` pair is produced at the PEL/1-CORE level.
* The run is considered **out-of-model**.
Higher layers (orchestration, SRE policy) MAY define:
* logging,
* retries,
* escalation or incident handling,
but such failures are not represented as valid `ExecutionResultValue` values under this spec.
---
## 5. Relationship to Stores and Surfaces (Informative)
### 5.1 Store-backed realizations
`PEL/1-CORE` is storage-neutral, but a typical realization over `ASL/1-STORE` looks like:
1. An engine receives:
* `scheme_ref : SchemeRef`,
* `program_ref : Reference`,
* `input_refs : list<Reference>`,
* `params_ref : optional Reference`.
2. It uses `ASL/1-STORE` `get` to resolve:
* `program_ref` to `program : Artifact`,
* `input_refs` to `inputs : list<Artifact>`,
* `params_ref` (if present) to `params : Artifact`.
3. It calls `Exec_s(program, inputs, params)` per `PEL/1-CORE`.
4. It uses `ASL/1-STORE` `put` to:
* persist `outputs : list<Artifact>` and obtain their `Reference`s,
* encode `ExecutionResultValue` as an `Artifact` and persist it, obtaining a result `Reference`.
A surface specification (e.g., `PEL/1-SURF`) can normatively define:
* the store-backed API (e.g., `run(store, scheme_ref, program_ref, input_refs, params_ref)`),
* mapping of store errors into higher-level envelopes,
* encoding of `ExecutionResultValue` as an Artifact (TypeTag, bytes).
`PEL/1-CORE` does not prescribe these surfaces; it only constrains the pure mapping implemented in step 3.
### 5.2 Mapping errors in surfaces
`PEL/1-CORE` is unaware of store errors like `ERR_NOT_FOUND`, `ERR_INTEGRITY`, or `ERR_UNSUPPORTED`.
Surface profiles (e.g., `PEL/1-SURF`) MAY:
* introduce additional wrapper structures that capture:
* store-level failures,
* missing inputs/programs,
* multi-store scenarios.
* map such failures into rich **surface-level** results (not `ExecutionResultValue`s), potentially with:
* failing `Reference`s,
* store error codes,
* retry hints.
Within `PEL/1-CORE` itself, the only “unavailability” status is `SCHEME_UNSUPPORTED`, strictly about scheme support, not store availability.
---
## 6. Conformance
An implementation is **PEL/1-COREconformant** if and only if it satisfies all of:
1. **Correct use of ASL/1-CORE types**
* Treats `Artifact`, `TypeTag`, and `Reference` exactly as in `ASL/1-CORE v0.4.x`.
* Does not redefine Artifact or Reference identity or equality.
2. **Implements at least one scheme**
* For each supported `scheme_ref`, implements a total function:
```text
Exec_s(program, inputs, params) -> (outputs, result)
```
as described in §3 and §4.
* For unsupported schemes, attempts to execute them yield an `ExecutionResultValue` with:
* `status = SCHEME_UNSUPPORTED`,
* `scheme_ref` equal to the requested scheme,
* `summary.kind = SCHEME`,
* `summary.status_code = 1`.
3. **Satisfies determinism**
* For each supported scheme, satisfies **PEL/DET/1** across all PEL/1-COREconformant implementations.
4. **Satisfies purity**
* For each supported scheme, satisfies **PEL/PURITY/1**.
* Any time or randomness must be supplied as input Artifacts.
5. **Produces valid ExecutionResultValue**
* For every in-model execution, produces an `ExecutionResultValue` with:
* `pel1_version = 1`,
* `scheme_ref` set correctly,
* `status` set according to scheme semantics (§2.3),
* `summary` consistent with `status` (§2.4),
* `diagnostics` deterministic (if present).
6. **Stays independent of higher layers on the hot path**
* Does not require TGK/1, CIL/1, FER/1, FCT/1, or OI/1 to compute `Exec_s`.
* Any provenance edges, receipts, or facts are constructed after execution using Artifacts and `ExecutionResultValue`, not during the core mapping.
7. **Treats environment failures as out-of-model**
* Does not attempt to represent OS/hardware/environment failures as valid `ExecutionResultValue` values.
* Clearly distinguishes:
* valid executions (producing `(outputs, ExecutionResultValue)`), vs
* environment failures (producing neither, handled outside `PEL/1-CORE`).
All other aspects — concrete APIs, store wiring, encoding, hash usage, scheduling, sandboxing, resource limits — belong to surfaces and higher-layer profiles, not to `PEL/1-CORE`, provided they do not contradict the requirements above.
---
## 7. Evolution (Informative)
`PEL/1-CORE` is intended to evolve **additively**:
* New `ExecutionStatus` values MAY be added, but existing codes MUST retain their meaning.
* New `ExecutionErrorKind` variants MAY be added, but existing variants MUST retain their meaning and relationships.
* New result formats MAY be introduced under new `pel1_version` values, but `pel1_version = 1` semantics MUST remain stable.
Any change that would:
* alter the meaning of an existing `ExecutionStatus`, or
* alter the interpretation of an existing `pel1_version = 1` field,
MUST be treated as a **new major kernel surface** (e.g., `PEL/2-CORE`), not an evolution of `PEL/1-CORE`.
This aligns with the broader Amduat principle:
> **Evolve by addition and explicit versioning; never rewrite identity or history.**
---
## Document History
* **0.3.0 (2025-11-16):** Registered as Tier-1 spec and aligned to the Amduat 2.0 substrate baseline.