Add PEL tier1 specifications
This commit is contained in:
Carl Niklas Rydberg
parent
f69742dc0b
commit
4dae7a32d2
734
tier1/enc-pel-program-dag-1.md
Normal file
734
tier1/enc-pel-program-dag-1.md
Normal file
|
|
@ -0,0 +1,734 @@
|
|||
# ENC/PEL-PROGRAM-DAG/1 — Canonical Encoding for DAG Programs
|
||||
|
||||
Status: Approved
|
||||
Owner: Niklas Rydberg
|
||||
Version: 0.2.0
|
||||
SoT: Yes
|
||||
Last Updated: 2025-11-16
|
||||
Linked Phase Pack: N/A
|
||||
Tags: [binary-minimalism, deterministic]
|
||||
|
||||
<!-- Source: /amduat/docs/new/enc-pel-program-dag-1.md | Canonical: /amduat/tier1/enc-pel-program-dag-1.md -->
|
||||
|
||||
**Document ID:** `ENC/PEL-PROGRAM-DAG/1`
|
||||
**Profile ID:** `PEL_ENC_PROGRAM_DAG_V1 = 0x0101`
|
||||
**Layer:** Scheme Encoding Profile (on top of ASL/1-CORE + PEL/PROGRAM-DAG/1)
|
||||
|
||||
**Depends on (normative):**
|
||||
|
||||
* `ASL/1-CORE v0.4.x` — value model (`Artifact`, `TypeTag`, `Reference`, integers, `OctetString`)
|
||||
* `ENC/ASL1-CORE v1.0.3` — canonical encoding conventions (integers, `OctetString`, streaming constraints)
|
||||
* `PEL/PROGRAM-DAG/1 v0.3.1` — DAG Program scheme (`Program` / `Node` model, semantics, canonical topological order)
|
||||
|
||||
**Integrates with (informative):**
|
||||
|
||||
* `PEL/1-CORE v0.3.x` — primitive execution layer (`Exec_s` / `Exec_DAG`)
|
||||
* `PEL/1-SURF v0.2.x` — store-backed execution surface
|
||||
* `HASH/ASL1 v0.2.4` — reference formation over canonical encodings
|
||||
* TypeTag registry (for `TYPE_TAG_PEL_PROGRAM_DAG_1`)
|
||||
* Operation registries (e.g. `OPREG/PEL1-KERNEL` and param profiles)
|
||||
|
||||
> **Note:** The Profile ID `PEL_ENC_PROGRAM_DAG_V1` is a configuration label.
|
||||
> It is **not** embedded in the encoded Program bytes. Selection of this encoding profile is done by context (scheme descriptor, store or engine configuration), not per value.
|
||||
|
||||
© 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
|
||||
|
||||
`ENC/PEL-PROGRAM-DAG/1` defines the **canonical binary encoding** of the `Program` structure defined in `PEL/PROGRAM-DAG/1`:
|
||||
|
||||
```text
|
||||
Program {
|
||||
nodes: list<Node>
|
||||
roots: list<RootRef>
|
||||
}
|
||||
````
|
||||
|
||||
and its sub-structures:
|
||||
|
||||
* `OperationId`
|
||||
* `DagInputExternal`, `DagInputNode`, `DagInput`
|
||||
* `Node`
|
||||
* `RootRef`
|
||||
|
||||
This encoding:
|
||||
|
||||
* is **injective** with respect to the logical `Program` model — distinct Programs → distinct byte strings under this profile,
|
||||
* is **stable and deterministic** across implementations and time,
|
||||
* is **streaming-friendly** — encoders and decoders can operate in a single forward pass,
|
||||
* fixes a **canonical topological ordering** for `nodes` (matching the scheme spec).
|
||||
|
||||
The result is used as the payload (`Artifact.bytes`) of Program Artifacts for the `PEL/PROGRAM-DAG/1` scheme, with:
|
||||
|
||||
```text
|
||||
Artifact.type_tag = TYPE_TAG_PEL_PROGRAM_DAG_1
|
||||
Artifact.bytes = ProgramBytes
|
||||
```
|
||||
|
||||
Identity of Program Artifacts is then derived via `HASH/ASL1` over `ArtifactBytes` as usual.
|
||||
|
||||
---
|
||||
|
||||
## 1. Scope & Layering
|
||||
|
||||
### 1.1 Purpose
|
||||
|
||||
This specification defines:
|
||||
|
||||
* The concrete binary layout of:
|
||||
|
||||
* `ProgramBytes`
|
||||
* `NodeBytes`
|
||||
* `DagInputBytes`
|
||||
* `RootRefBytes`
|
||||
* `OperationIdBytes`
|
||||
|
||||
* Canonicalization rules:
|
||||
|
||||
* Node ordering (canonical topological order),
|
||||
* fixed field ordering,
|
||||
* integer widths and encodings.
|
||||
|
||||
It does **not** define:
|
||||
|
||||
* The logical semantics of Programs (DAG evaluation, error statuses, etc.) — those are in `PEL/PROGRAM-DAG/1` and `PEL/1-CORE`.
|
||||
* The ASL/1 `Artifact` or `Reference` layouts — those are in `ASL/1-CORE` and `ENC/ASL1-CORE`.
|
||||
* How Programs are used in store-backed execution — that belongs to `PEL/1-SURF`.
|
||||
|
||||
### 1.2 Layering constraints
|
||||
|
||||
In line with `SUBSTRATE/STACK-OVERVIEW`:
|
||||
|
||||
* `ENC/PEL-PROGRAM-DAG/1` is a **scheme-specific encoding profile**.
|
||||
|
||||
* It MUST NOT redefine:
|
||||
|
||||
* `Artifact`, `TypeTag`, `Reference`, or `HashId` (from `ASL/1-CORE`),
|
||||
* the logical `Program` / `Node` / `DagInput` / `RootRef` model (from `PEL/PROGRAM-DAG/1`).
|
||||
|
||||
* It is **storage-neutral** and **policy-neutral**.
|
||||
|
||||
* It defines exactly one canonical encoding for `Program` values for this scheme under the profile ID `PEL_ENC_PROGRAM_DAG_V1`.
|
||||
|
||||
---
|
||||
|
||||
## 2. Conventions
|
||||
|
||||
RFC 2119 terms (**MUST**, **SHOULD**, **MAY**, etc.) are normative.
|
||||
|
||||
### 2.1 Integer encodings
|
||||
|
||||
All multi-byte integers are encoded as **big-endian** (network byte order), as in `ENC/ASL1-CORE`:
|
||||
|
||||
* `u8` — 1 byte
|
||||
* `u16` — 2 bytes
|
||||
* `u32` — 4 bytes
|
||||
* `u64` — 8 bytes
|
||||
|
||||
Only **fixed-width** integers are used in this specification.
|
||||
|
||||
### 2.2 Utf8String
|
||||
|
||||
This specification defines a canonical `Utf8String` encoding:
|
||||
|
||||
```text
|
||||
Utf8String = length (u32) || bytes[0..length-1]
|
||||
```
|
||||
|
||||
* `length` is the number of bytes of UTF-8 data.
|
||||
* `length` MAY be zero.
|
||||
* Decoders MUST validate that the byte sequence is well-formed UTF-8.
|
||||
* There is no padding or terminator.
|
||||
|
||||
All strings in this profile (`OperationId.name`) are encoded as `Utf8String`.
|
||||
|
||||
### 2.3 Parameter bytes
|
||||
|
||||
For operation parameters, this profile uses a compact `ParamsBytes` encoding:
|
||||
|
||||
```text
|
||||
ParamsBytes = length (u32) || bytes[0..length-1]
|
||||
```
|
||||
|
||||
* `bytes` is an opaque blob whose interpretation is defined per operation in the operation registry.
|
||||
* `length` MAY be zero (empty params).
|
||||
|
||||
> This differs from the general `OctetString` encoding (which uses `u64` length and is defined in `ENC/ASL1-CORE`).
|
||||
> Using `u32` length here is acceptable because this structure lives *inside* the Program Artifact payload, not as an ASL/1 top-level value.
|
||||
|
||||
#### 2.3.1 Parameter profiles and canonicality
|
||||
|
||||
When a `Program` is interpreted under a concrete operation registry + parameter profile set:
|
||||
|
||||
* For each operation `(name, version)`:
|
||||
|
||||
* There MUST be a well-defined abstract parameter model (`ParamsValue`).
|
||||
* There MUST be exactly one canonical encode/decode pair:
|
||||
|
||||
```text
|
||||
encode_params_op : ParamsValue -> ParamsBytes
|
||||
decode_params_op : ParamsBytes -> ParamsValue | error
|
||||
```
|
||||
|
||||
* All conformant implementations of that operation MUST:
|
||||
|
||||
* decode `ParamsBytes` into the same `ParamsValue`, or
|
||||
* deterministically detect decoding failures.
|
||||
|
||||
Kernel parameter profiles (e.g. `OPREG/PEL1-KERNEL-PARAMS/1`) MUST ensure:
|
||||
|
||||
* `encode_params_op` followed by `decode_params_op` round-trips exactly.
|
||||
* Any `ParamsBytes` that fails `decode_params_op` MUST be treated as a **program-level validation error** (`INVALID_PROGRAM`) under `PEL/PROGRAM-DAG/1`, not as a runtime failure.
|
||||
|
||||
### 2.4 Lists
|
||||
|
||||
A list of values of some type `T` is encoded as:
|
||||
|
||||
```text
|
||||
List<T> = count (u32) || element_0 || element_1 || ... || element_{count-1}
|
||||
```
|
||||
|
||||
* `count` is the number of elements (MAY be zero).
|
||||
* Elements are encoded in order, using the canonical encoding of `T`.
|
||||
|
||||
### 2.5 Encoding version field
|
||||
|
||||
`ProgramBytes` includes a `program_version (u16)` field:
|
||||
|
||||
* In this profile, `program_version` MUST be `1`.
|
||||
* Any future incompatible change to the layout of `ProgramBytes` under the same profile ID MUST be reflected by a new `program_version` value (and corresponding decoder support).
|
||||
* Adding fields in a backward-compatible, strictly-append-only way SHOULD be done via a new encoding profile rather than overloading `program_version = 1`.
|
||||
|
||||
Decoders MUST reject any `program_version` they do not implement.
|
||||
|
||||
---
|
||||
|
||||
## 3. Logical Model Reference
|
||||
|
||||
For convenience, the logical types from `PEL/PROGRAM-DAG/1` are restated informally (normative source remains that document):
|
||||
|
||||
```text
|
||||
OperationId {
|
||||
name: string
|
||||
version: uint32
|
||||
}
|
||||
|
||||
DagInputExternal {
|
||||
input_index: uint32
|
||||
}
|
||||
|
||||
DagInputNode {
|
||||
node_id: NodeId // uint32
|
||||
output_index: uint32
|
||||
}
|
||||
|
||||
DagInput =
|
||||
DagInputExternal
|
||||
| DagInputNode
|
||||
|
||||
Node {
|
||||
id: NodeId // uint32
|
||||
op: OperationId
|
||||
inputs: list<DagInput>
|
||||
params: Params // abstract; serialized as ParamsBytes in this profile
|
||||
}
|
||||
|
||||
RootRef {
|
||||
node_id: NodeId // uint32
|
||||
output_index: uint32
|
||||
}
|
||||
|
||||
Program {
|
||||
nodes: list<Node>
|
||||
roots: list<RootRef>
|
||||
}
|
||||
|
||||
NodeId = uint32
|
||||
```
|
||||
|
||||
`PEL/PROGRAM-DAG/1` further defines:
|
||||
|
||||
* Structural validity rules (unique NodeIds, acyclicity, etc.).
|
||||
* Canonical topological order of Nodes.
|
||||
|
||||
This encoding profile assumes the logical model and validity rules as given there. It **does not** re-check them at the encoding-layer; that is scheme-level responsibility.
|
||||
|
||||
---
|
||||
|
||||
## 4. Program Encoding
|
||||
|
||||
### 4.1 Program header and overall layout
|
||||
|
||||
The canonical encoding of a `Program` value is:
|
||||
|
||||
```text
|
||||
ProgramBytes ::
|
||||
program_version (u16)
|
||||
node_count (u32)
|
||||
nodes (NodeBytes[0..node_count-1])
|
||||
root_count (u32)
|
||||
roots (RootRefBytes[0..root_count-1])
|
||||
```
|
||||
|
||||
Constraints:
|
||||
|
||||
* `program_version` MUST currently be `1`.
|
||||
|
||||
Decoders:
|
||||
|
||||
* MUST accept `program_version = 1`.
|
||||
* MUST reject any other value as an unsupported encoding version.
|
||||
|
||||
* `node_count` and `root_count` are the number of elements in the corresponding lists.
|
||||
|
||||
* `nodes` MUST be encoded in the **canonical topological order** defined in `PEL/PROGRAM-DAG/1 §4`. Encoders MUST perform this ordering; decoders MAY rely on it but are not required to re-check DAG properties.
|
||||
|
||||
* `roots` MUST be encoded in the same order as the logical `Program.roots` list.
|
||||
|
||||
### 4.2 Node encoding
|
||||
|
||||
Each `Node` is encoded as:
|
||||
|
||||
```text
|
||||
NodeBytes ::
|
||||
node_id (u32)
|
||||
op_name (Utf8String)
|
||||
op_version (u32)
|
||||
input_count (u32)
|
||||
inputs (DagInputBytes[0..input_count-1])
|
||||
params_len (u32)
|
||||
params_bytes (byte[0..params_len-1])
|
||||
```
|
||||
|
||||
Field meanings:
|
||||
|
||||
1. `node_id (u32)`
|
||||
|
||||
* Encodes `Node.id`.
|
||||
* MUST be unique across all Nodes in a Program (scheme-level requirement).
|
||||
|
||||
2. `op_name (Utf8String)`
|
||||
|
||||
* Encodes `OperationId.name` as UTF-8.
|
||||
|
||||
3. `op_version (u32)`
|
||||
|
||||
* Encodes `OperationId.version`.
|
||||
|
||||
4. `input_count (u32)`
|
||||
|
||||
* Number of input references consumed by this Node.
|
||||
|
||||
5. `inputs`
|
||||
|
||||
* Exactly `input_count` entries, each encoded as `DagInputBytes` (see §4.3) in order.
|
||||
|
||||
6. `params_len (u32)` and `params_bytes`
|
||||
|
||||
* `params_len` = length of the operation-specific parameter blob.
|
||||
* `params_bytes` is an opaque blob whose interpretation is defined by the operation’s parameter profile.
|
||||
* A `params_len` of `0` encodes an empty parameter blob.
|
||||
|
||||
> **Injectivity requirement (Node)**
|
||||
> For a fixed interpretation of `ParamsBytes` and `OperationId`, distinct logical `Node` values (differing in any field) MUST produce distinct `NodeBytes`.
|
||||
> Given `NodeBytes` and the corresponding operation registry, a canonical decoder MUST reconstruct exactly the same logical `Node`.
|
||||
|
||||
### 4.3 DagInput encoding
|
||||
|
||||
Each `DagInput` is encoded as a tagged union:
|
||||
|
||||
```text
|
||||
DagInputBytes ::
|
||||
kind (u8)
|
||||
payload(...)
|
||||
```
|
||||
|
||||
Where `kind` is:
|
||||
|
||||
```text
|
||||
0x00 => DagInputExternal
|
||||
0x01 => DagInputNode
|
||||
```
|
||||
|
||||
#### 4.3.1 DagInputExternal
|
||||
|
||||
For:
|
||||
|
||||
```text
|
||||
DagInputExternal {
|
||||
input_index: uint32
|
||||
}
|
||||
```
|
||||
|
||||
Encoding:
|
||||
|
||||
```text
|
||||
kind = 0x00
|
||||
input_index (u32)
|
||||
```
|
||||
|
||||
`input_index` is the 0-based index into the `inputs` list passed to `Exec_DAG`.
|
||||
|
||||
#### 4.3.2 DagInputNode
|
||||
|
||||
For:
|
||||
|
||||
```text
|
||||
DagInputNode {
|
||||
node_id: NodeId // uint32
|
||||
output_index: uint32
|
||||
}
|
||||
```
|
||||
|
||||
Encoding:
|
||||
|
||||
```text
|
||||
kind = 0x01
|
||||
node_id (u32)
|
||||
output_index (u32)
|
||||
```
|
||||
|
||||
`node_id` MUST refer to some `Node.id` in the same Program (scheme-level validity).
|
||||
`output_index` is the 0-based index into that Node’s output list.
|
||||
|
||||
#### 4.3.3 Decoder behavior
|
||||
|
||||
Decoders MUST:
|
||||
|
||||
* Treat any `kind` value other than `0x00` or `0x01` as an encoding error (invalid `DagInput`).
|
||||
* For `kind = 0x00`, read exactly one `u32` as `input_index`.
|
||||
* For `kind = 0x01`, read exactly two `u32` values (`node_id`, `output_index`).
|
||||
* Reject truncated encodings (insufficient bytes for the payload).
|
||||
|
||||
Structural validity of indices (e.g., `node_id` existence, output arity) is enforced at the scheme level, not the encoding layer.
|
||||
|
||||
### 4.4 RootRef encoding
|
||||
|
||||
For:
|
||||
|
||||
```text
|
||||
RootRef {
|
||||
node_id: NodeId
|
||||
output_index: uint32
|
||||
}
|
||||
```
|
||||
|
||||
Encoding:
|
||||
|
||||
```text
|
||||
RootRefBytes ::
|
||||
node_id (u32)
|
||||
output_index (u32)
|
||||
```
|
||||
|
||||
* `RootRefBytes` is identical to the payload of `DagInputNode`, but without a `kind` byte.
|
||||
Roots are always Node outputs, so no variant tag is needed.
|
||||
|
||||
* The `roots` list in `ProgramBytes` MUST encode each `RootRef` in the logical order of `Program.roots`.
|
||||
|
||||
Decoders MUST reject truncated entries (insufficient bytes for both `u32` values).
|
||||
|
||||
---
|
||||
|
||||
## 5. Canonicality Requirements
|
||||
|
||||
### 5.1 Node ordering in Program
|
||||
|
||||
Encoders MUST:
|
||||
|
||||
* encode `Program.nodes` in the **canonical topological order** defined by `PEL/PROGRAM-DAG/1 §4`:
|
||||
|
||||
* Dependencies appear before dependents.
|
||||
* Ties are broken by smallest `NodeId` (numeric, ascending).
|
||||
|
||||
* ensure that the `node_count` written in `ProgramBytes` equals the number of encoded `NodeBytes`.
|
||||
|
||||
Decoders:
|
||||
|
||||
* MAY assume the encoded order corresponds to the canonical topological order.
|
||||
* MAY perform additional checks (e.g., verifying acyclicity), but this is not required for basic decoding.
|
||||
|
||||
### 5.2 Field ordering
|
||||
|
||||
Field ordering in all structures is fixed and MUST NOT vary:
|
||||
|
||||
* `ProgramBytes` — `program_version`, `node_count`, `nodes…`, `root_count`, `roots…`
|
||||
* `NodeBytes` — `node_id`, `op_name`, `op_version`, `input_count`, `inputs…`, `params_len`, `params_bytes…`
|
||||
* `DagInputBytes` — `kind`, then variant-specific payload.
|
||||
* `RootRefBytes` — `node_id`, `output_index`.
|
||||
|
||||
Any deviation MUST be treated as an encoding error.
|
||||
|
||||
### 5.3 Injectivity and stability
|
||||
|
||||
The mapping:
|
||||
|
||||
```text
|
||||
Program -> ProgramBytes
|
||||
```
|
||||
|
||||
defined by this profile MUST be:
|
||||
|
||||
* **Injective** — if `P1 != P2` as logical `Program` values (per `PEL/PROGRAM-DAG/1`), then `ProgramBytes(P1) != ProgramBytes(P2)`.
|
||||
|
||||
* **Stable** — the same logical `Program` MUST encode to the same `ProgramBytes` across:
|
||||
|
||||
* different implementations,
|
||||
* platforms,
|
||||
* executions,
|
||||
* and times,
|
||||
|
||||
given the same version of this encoding profile and the same underlying operation/param profiles.
|
||||
|
||||
Encoders MUST NOT:
|
||||
|
||||
* reorder Nodes other than by the canonical topological order,
|
||||
* reorder inputs within a Node,
|
||||
* reorder roots,
|
||||
* introduce alternative encodings for integers, strings, or params.
|
||||
|
||||
---
|
||||
|
||||
## 6. Program Artifact Binding
|
||||
|
||||
### 6.1 TypeTag
|
||||
|
||||
Program Artifacts for this scheme MUST be encoded as:
|
||||
|
||||
```text
|
||||
Artifact {
|
||||
bytes = ProgramBytes
|
||||
type_tag = TYPE_TAG_PEL_PROGRAM_DAG_1
|
||||
}
|
||||
```
|
||||
|
||||
Where:
|
||||
|
||||
* `TYPE_TAG_PEL_PROGRAM_DAG_1` is a `TypeTag` with a concrete `tag_id` assigned in the global TypeTag registry.
|
||||
|
||||
This encoding profile:
|
||||
|
||||
* uses `TYPE_TAG_PEL_PROGRAM_DAG_1` symbolically, and
|
||||
* does not assign a specific numeric `tag_id`; that is done in a registry document.
|
||||
|
||||
### 6.2 Identity via ASL/1-CORE and HASH/ASL1
|
||||
|
||||
Given `ENC/ASL1-CORE v1` as the canonical encoding for `Artifact` and some chosen ASL1 hash algorithm `H` (e.g. `HASH-ASL1-256` under `HashId = 0x0001`):
|
||||
|
||||
1. The canonical `ArtifactBytes` for a Program Artifact is given by `ENC/ASL1-CORE v1`:
|
||||
|
||||
```text
|
||||
ArtifactBytes =
|
||||
encode_artifact_core_v1(
|
||||
Artifact{ bytes = ProgramBytes, type_tag = TYPE_TAG_PEL_PROGRAM_DAG_1 }
|
||||
)
|
||||
```
|
||||
|
||||
2. The canonical `Reference` for that Artifact under `HashId = HID` is:
|
||||
|
||||
```text
|
||||
digest = H(ArtifactBytes)
|
||||
reference = Reference { hash_id = HID, digest = digest }
|
||||
```
|
||||
|
||||
All conformant implementations MUST agree on:
|
||||
|
||||
* `ProgramBytes` for a given logical `Program`,
|
||||
* `ArtifactBytes` for the Program Artifact,
|
||||
* the resulting `Reference` for any fixed `(HashId, H)`.
|
||||
|
||||
---
|
||||
|
||||
## 7. Error Handling (Encoding Level)
|
||||
|
||||
This encoding profile defines only **structural encoding errors**. Handling of scheme-level validity errors (`INVALID_PROGRAM`, etc.) is done by `PEL/PROGRAM-DAG/1` and `PEL/1-CORE`.
|
||||
|
||||
Decoders MUST treat as encoding errors:
|
||||
|
||||
1. **Truncated fields**
|
||||
|
||||
* Not enough bytes to read any declared integer, string, list, or params blob.
|
||||
|
||||
2. **Unsupported `program_version`**
|
||||
|
||||
* `program_version != 1`.
|
||||
|
||||
3. **Invalid `DagInput.kind`**
|
||||
|
||||
* `kind` is not `0x00` or `0x01`.
|
||||
|
||||
4. **Invalid `Utf8String`**
|
||||
|
||||
* `op_name` bytes are not valid UTF-8.
|
||||
|
||||
5. **Inconsistent list lengths**
|
||||
|
||||
* Fewer or more `NodeBytes` than indicated by `node_count`.
|
||||
* Fewer or more `RootRefBytes` than indicated by `root_count`.
|
||||
|
||||
These are **encoding-layer** issues. The exact error codes surfaced to callers (e.g., `ERR_PEL_ENC_INVALID`) are implementation-specific but MUST result in rejection of the Program bytes as malformed under this encoding profile.
|
||||
|
||||
---
|
||||
|
||||
## 8. Streaming and Implementation Notes
|
||||
|
||||
Implementations MUST be able to:
|
||||
|
||||
* Encode any `Program` using a single forward pass over the canonical node order:
|
||||
|
||||
* compute canonical topological order first (requires holding `Program` structure),
|
||||
* then write fields in the order defined above.
|
||||
|
||||
* Decode any `ProgramBytes` sequentially:
|
||||
|
||||
* no backtracking or multi-pass parsing is required,
|
||||
* all length prefixes appear before their content.
|
||||
|
||||
For very large Programs:
|
||||
|
||||
* Implementations MAY:
|
||||
|
||||
* stream Nodes one by one into an internal representation,
|
||||
* stream `params_bytes` to a buffer or directly into an operation-registry decoder.
|
||||
|
||||
* They MUST ensure that any observable behavior (including error reporting) is independent of chunking or I/O strategy: two conformant decoders seeing the same `ProgramBytes` MUST reconstruct the same logical `Program` or the same encoding error.
|
||||
|
||||
---
|
||||
|
||||
## 9. Conformance
|
||||
|
||||
An implementation is **ENC/PEL-PROGRAM-DAG/1–conformant** if it:
|
||||
|
||||
1. **Implements `ProgramBytes` encoding/decoding**
|
||||
|
||||
* Encodes and decodes `ProgramBytes` exactly as defined in §4.
|
||||
* Treats `program_version = 1` as the only supported version.
|
||||
* Treats deviations (unknown version, malformed fields) as encoding errors.
|
||||
|
||||
2. **Respects canonical ordering**
|
||||
|
||||
* When encoding `Program` values, orders `nodes` in the canonical topological order defined in `PEL/PROGRAM-DAG/1`.
|
||||
* Preserves the logical order of `roots`.
|
||||
|
||||
3. **Uses canonical field encodings**
|
||||
|
||||
* Uses `u32` lengths for lists and params as specified.
|
||||
* Uses `Utf8String` for operation names.
|
||||
* Uses `u8` discriminants and the specified payload layout for `DagInput`.
|
||||
|
||||
4. **Preserves injectivity and stability**
|
||||
|
||||
* Ensures distinct logical Programs (per `PEL/PROGRAM-DAG/1`) produce distinct `ProgramBytes`.
|
||||
* Ensures the same logical Program consistently produces the same `ProgramBytes` under this profile.
|
||||
|
||||
5. **Binds to Program Artifacts correctly**
|
||||
|
||||
* When forming Program Artifacts for `PEL/PROGRAM-DAG/1`, sets:
|
||||
|
||||
* `Artifact.bytes = ProgramBytes`
|
||||
* `Artifact.type_tag = TYPE_TAG_PEL_PROGRAM_DAG_1`
|
||||
|
||||
* Uses `ENC/ASL1-CORE v1` and `HASH/ASL1` for ASL/1 identity.
|
||||
|
||||
Everything else — storage, transport, operation registries, traces — is outside the scope of this encoding profile, provided it does not contradict the requirements above.
|
||||
|
||||
---
|
||||
|
||||
## 10. Informative Example
|
||||
|
||||
> This example is non-normative and uses abbreviated hex.
|
||||
> It illustrates only the field layout, not exact ASCII/UTF-8 bytes.
|
||||
|
||||
Consider a tiny Program:
|
||||
|
||||
* Nodes:
|
||||
|
||||
1. `N0` — `id = 1`
|
||||
|
||||
* `op = (name = "add64", version = 1)`
|
||||
* `inputs = [ DagInputExternal{input_index = 0}, DagInputExternal{input_index = 1} ]`
|
||||
* `params =` empty
|
||||
|
||||
2. `N1` — `id = 2`
|
||||
|
||||
* `op = (name = "mul64", version = 1)`
|
||||
* `inputs = [ DagInputNode{node_id = 1, output_index = 0}, DagInputExternal{input_index = 2} ]`
|
||||
* `params =` empty
|
||||
|
||||
* Roots:
|
||||
|
||||
* `RootRef{ node_id = 2, output_index = 0 }`
|
||||
|
||||
Canonical topological order:
|
||||
|
||||
* Node 1 has only external inputs → first.
|
||||
* Node 2 depends on Node 1 → second.
|
||||
|
||||
ProgramBytes (pseudo-annotated):
|
||||
|
||||
```text
|
||||
program_version = 0001 ; u16 = 1
|
||||
|
||||
node_count = 00000002 ; 2 nodes
|
||||
|
||||
; Node 0 (id = 1)
|
||||
node_id = 00000001
|
||||
op_name = 00000005 "add64" ; length=5, bytes 'a','d','d','6','4'
|
||||
op_version = 00000001
|
||||
input_count = 00000002
|
||||
; input 0: external(0)
|
||||
kind = 00
|
||||
input_index = 00000000
|
||||
; input 1: external(1)
|
||||
kind = 00
|
||||
input_index = 00000001
|
||||
params_len = 00000000 ; empty params
|
||||
|
||||
; Node 1 (id = 2)
|
||||
node_id = 00000002
|
||||
op_name = 00000005 "mul64"
|
||||
op_version = 00000001
|
||||
input_count = 00000002
|
||||
; input 0: node(1,0)
|
||||
kind = 01
|
||||
node_id = 00000001
|
||||
output_index = 00000000
|
||||
; input 1: external(2)
|
||||
kind = 00
|
||||
input_index = 00000002
|
||||
params_len = 00000000 ; empty params
|
||||
|
||||
root_count = 00000001
|
||||
; root 0: (node 2, output 0)
|
||||
node_id = 00000002
|
||||
output_index = 00000000
|
||||
```
|
||||
|
||||
These bytes become `Artifact.bytes` for a Program Artifact with `type_tag = TYPE_TAG_PEL_PROGRAM_DAG_1`. All conformant encoders under `PEL_ENC_PROGRAM_DAG_V1` MUST produce the same byte sequence for this logical Program.
|
||||
|
||||
---
|
||||
|
||||
**End of `ENC/PEL-PROGRAM-DAG/1 v0.2.0 — Canonical Encoding for DAG Programs`**
|
||||
|
||||
---
|
||||
|
||||
## Document History
|
||||
|
||||
* **0.2.0 (2025-11-16):** Registered as Tier-1 spec and aligned to the Amduat 2.0 substrate baseline.
|
||||
835
tier1/enc-pel-trace-dag-1.md
Normal file
835
tier1/enc-pel-trace-dag-1.md
Normal file
|
|
@ -0,0 +1,835 @@
|
|||
# ENC/PEL-TRACE-DAG/1 — Canonical Encoding for DAG Execution Traces
|
||||
|
||||
Status: Approved
|
||||
Owner: Niklas Rydberg
|
||||
Version: 0.1.0
|
||||
SoT: Yes
|
||||
Last Updated: 2025-11-16
|
||||
Linked Phase Pack: N/A
|
||||
Tags: [binary-minimalism, traceability]
|
||||
|
||||
<!-- Source: /amduat/docs/new/enc-pel-trace-dag-1.md | Canonical: /amduat/tier1/enc-pel-trace-dag-1.md -->
|
||||
|
||||
**Document ID:** `ENC/PEL-TRACE-DAG/1`
|
||||
**Profile ID:** `PEL_ENC_TRACE_DAG_V1 = 0x0102`
|
||||
**Layer:** Scheme Encoding Profile (Trace)
|
||||
|
||||
**Depends on (normative):**
|
||||
|
||||
* `ASL/1-CORE v0.3.2` — value model (`Artifact`, `TypeTag`, `Reference`, integers, `OctetString`)
|
||||
* `ENC/ASL1-CORE v1.0.3` — canonical encodings for `Artifact` and `Reference`
|
||||
* `PEL/1-CORE v0.1.0` — primitive execution layer (ExecutionStatus, ExecutionErrorSummary)
|
||||
* `PEL/PROGRAM-DAG/1 v0.2.0` — DAG Program scheme (Program, Node, NodeId, canonical node order)
|
||||
* `PEL/TRACE-DAG/1 v0.1.0` — DAG execution trace profile (logical data model)
|
||||
|
||||
**Integrates with (informative):**
|
||||
|
||||
* `PEL/1-SURF v0.1.0` — store-backed execution surface
|
||||
* `HASH/ASL1 v0.2.3` — ASL1 hash family for trace artifact identity
|
||||
* TypeTag registry (for `TYPE_TAG_PEL_TRACE_DAG_1`)
|
||||
|
||||
> The Profile ID `PEL_ENC_TRACE_DAG_V1` is a configuration label.
|
||||
> It is **not** embedded into trace payloads. Encoders and decoders select this encoding profile by context (scheme descriptor, engine/store configuration), not per value.
|
||||
|
||||
© 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
|
||||
|
||||
`ENC/PEL-TRACE-DAG/1` defines the **canonical binary encoding** of the `TraceDAGValue` structure specified in `PEL/TRACE-DAG/1`, and all of its nested components:
|
||||
|
||||
* `TraceDAGValue`
|
||||
* `NodeTraceDAG`
|
||||
* `DiagnosticEntry`
|
||||
|
||||
This encoding:
|
||||
|
||||
* is **injective** — distinct logical trace values → distinct byte strings;
|
||||
* is **stable and deterministic** — same value → same bytes across implementations and time;
|
||||
* is **streaming-friendly** — encoders/decoders can operate in a single forward pass;
|
||||
* embeds ASL/1 `Reference` values using their canonical `ReferenceBytes` encoding (`ENC/ASL1-CORE v1`) inside length-prefixed frames.
|
||||
|
||||
The encoded payload (`TraceDAGBytes`) is used as the `bytes` field of a trace Artifact for the `PEL/TRACE-DAG/1` profile, with:
|
||||
|
||||
```text
|
||||
Artifact.type_tag = TYPE_TAG_PEL_TRACE_DAG_1
|
||||
Artifact.bytes = TraceDAGBytes
|
||||
````
|
||||
|
||||
Trace Artifact identity is then derived by hashing canonical `ArtifactBytes` with `"ASL1"` hash algorithms (typically `HASH-ASL1-256`).
|
||||
|
||||
---
|
||||
|
||||
## 1. Scope & Layering
|
||||
|
||||
### 1.1 Purpose
|
||||
|
||||
This specification defines:
|
||||
|
||||
* The **binary layout** of:
|
||||
|
||||
* `TraceDAGBytes`
|
||||
* `NodeTraceDAGBytes`
|
||||
* `DiagnosticEntryBytes`
|
||||
* An internal “encoded Reference” wrapper for use inside trace payloads
|
||||
|
||||
* The canonical **field ordering**, integer widths, and list framing.
|
||||
|
||||
It does **not** define:
|
||||
|
||||
* The logical semantics of traces — those are in `PEL/TRACE-DAG/1`.
|
||||
* The ASL/1 `Artifact` / `Reference` encodings — these are in `ENC/ASL1-CORE v1.0.3`.
|
||||
* How traces are produced or when they are enabled — that is governed by `PEL/1-CORE`, `PEL/1-SURF`, and policy profiles.
|
||||
|
||||
### 1.2 Layering constraints
|
||||
|
||||
In line with `SUBSTRATE/STACK-OVERVIEW`:
|
||||
|
||||
* `ENC/PEL-TRACE-DAG/1` is a **scheme-specific encoding profile**.
|
||||
|
||||
* It MUST NOT redefine:
|
||||
|
||||
* `Artifact`, `TypeTag`, `Reference`, `HashId` (`ASL/1-CORE`),
|
||||
* the `TraceDAGValue` logical structure (`PEL/TRACE-DAG/1`).
|
||||
|
||||
* It is **storage-neutral** and **policy-neutral**.
|
||||
|
||||
* It defines exactly one canonical encoding for `TraceDAGValue` values in this scheme.
|
||||
|
||||
---
|
||||
|
||||
## 2. Conventions
|
||||
|
||||
The RFC 2119 terms **MUST**, **SHOULD**, **MAY**, etc. are normative.
|
||||
|
||||
### 2.1 Integer encodings
|
||||
|
||||
All multi-byte integers are encoded as **big-endian** (network byte order), as in `ENC/ASL1-CORE`:
|
||||
|
||||
* `u8` — 1 byte
|
||||
* `u16` — 2 bytes
|
||||
* `u32` — 4 bytes
|
||||
* `u64` — 8 bytes
|
||||
|
||||
Only **fixed-width** integers are used in this specification.
|
||||
|
||||
### 2.2 Lists
|
||||
|
||||
A list of values of some type `T` is encoded as:
|
||||
|
||||
```text
|
||||
List<T> =
|
||||
count (u32)
|
||||
element_0
|
||||
element_1
|
||||
...
|
||||
element_{count-1}
|
||||
```
|
||||
|
||||
* `count` is the number of elements (MAY be zero).
|
||||
* Elements are encoded in order, using the canonical encoding for `T`.
|
||||
|
||||
### 2.3 UTF-8 string
|
||||
|
||||
`Utf8String` is encoded as:
|
||||
|
||||
```text
|
||||
Utf8String =
|
||||
length (u32)
|
||||
bytes[0..length-1]
|
||||
```
|
||||
|
||||
* `length` is the number of bytes.
|
||||
* `bytes` MUST be well-formed UTF-8.
|
||||
* There is no terminator or padding.
|
||||
|
||||
### 2.4 Octet blob (32-bit length)
|
||||
|
||||
For diagnostics and other opaque fields, we use a generic blob:
|
||||
|
||||
```text
|
||||
Blob32 =
|
||||
length (u32)
|
||||
bytes[0..length-1]
|
||||
```
|
||||
|
||||
`bytes` is an arbitrary `OctetString`; interpretation is profile-specific. `length` MAY be zero.
|
||||
|
||||
### 2.5 Embedded Reference
|
||||
|
||||
Within this encoding, `Reference` values are embedded using a length-prefixed wrapper over canonical `ReferenceBytes` from `ENC/ASL1-CORE v1.0.3`.
|
||||
|
||||
We define:
|
||||
|
||||
```text
|
||||
EncodedRef =
|
||||
ref_len (u32)
|
||||
ref_bytes (byte[0..ref_len-1]) // canonical ReferenceBytes
|
||||
```
|
||||
|
||||
Where:
|
||||
|
||||
* `ref_bytes` MUST be the canonical `ReferenceBytes` encoding for a `Reference` value, as defined in `ENC/ASL1-CORE v1.0.3`:
|
||||
|
||||
```text
|
||||
ReferenceBytes ::
|
||||
hash_id (u16)
|
||||
digest (byte[...]) // remaining bytes
|
||||
```
|
||||
|
||||
* `ref_len` MUST be the exact length (in bytes) of `ref_bytes` (MUST be ≥ 2).
|
||||
|
||||
Decoders MUST:
|
||||
|
||||
* Read `ref_len (u32)`, then `ref_bytes[0..ref_len-1]`.
|
||||
* Decode `ref_bytes` as `ReferenceBytes` per `ENC/ASL1-CORE v1.0.3`.
|
||||
* Reject encodings where:
|
||||
|
||||
* `ref_len < 2`, or
|
||||
* `ref_bytes` is not a valid `ReferenceBytes` sequence (e.g., truncated).
|
||||
|
||||
#### 2.5.1 Optional EncodedRef
|
||||
|
||||
For optional `Reference` fields, we use:
|
||||
|
||||
```text
|
||||
OptionalEncodedRef =
|
||||
has_ref (u8)
|
||||
[ EncodedRef ] // only if has_ref = 0x01
|
||||
```
|
||||
|
||||
* `has_ref = 0x00` → no value present; no `EncodedRef` follows.
|
||||
* `has_ref = 0x01` → exactly one `EncodedRef` follows.
|
||||
|
||||
Other `has_ref` values MUST be treated as encoding errors.
|
||||
|
||||
---
|
||||
|
||||
## 3. Logical Model Reference
|
||||
|
||||
This section restates the logical structures from `PEL/TRACE-DAG/1` (source of truth) in condensed form.
|
||||
|
||||
### 3.1 DiagnosticEntry
|
||||
|
||||
```text
|
||||
DiagnosticEntry {
|
||||
code: uint32 // diagnostic or error code
|
||||
message: OctetString // typically UTF-8 text; interpretation is profile-specific
|
||||
}
|
||||
```
|
||||
|
||||
### 3.2 NodeTraceStatus
|
||||
|
||||
```text
|
||||
NodeTraceStatus = uint8
|
||||
|
||||
NodeTraceStatus {
|
||||
NODE_OK = 0
|
||||
NODE_FAILED = 1
|
||||
NODE_SKIPPED = 2
|
||||
}
|
||||
```
|
||||
|
||||
### 3.3 NodeTraceDAG
|
||||
|
||||
```text
|
||||
NodeTraceDAG {
|
||||
node_id: NodeId // uint32
|
||||
op_name: string
|
||||
op_version: uint32
|
||||
|
||||
status: NodeTraceStatus
|
||||
status_code: uint32 // 0 = success; non-zero = op-specific failure code
|
||||
|
||||
output_refs: list<Reference>
|
||||
diagnostics: list<DiagnosticEntry>
|
||||
}
|
||||
```
|
||||
|
||||
### 3.4 TraceDAGValue
|
||||
|
||||
```text
|
||||
TraceDAGValue {
|
||||
pel1_version: uint16 // MUST be 1 for this version
|
||||
scheme_ref: Reference // SchemeRef_DAG_1
|
||||
program_ref: Reference // Program Artifact reference
|
||||
|
||||
status: ExecutionStatus
|
||||
summary: ExecutionErrorSummary {
|
||||
kind: ExecutionErrorKind
|
||||
status_code: uint32
|
||||
}
|
||||
|
||||
exec_result_ref: optional Reference
|
||||
|
||||
input_refs: list<Reference>
|
||||
params_ref: optional Reference
|
||||
|
||||
node_traces: list<NodeTraceDAG> // one per Node in canonical node order
|
||||
}
|
||||
```
|
||||
|
||||
All semantics (how these fields are populated for different run outcomes) are defined in `PEL/TRACE-DAG/1`.
|
||||
|
||||
---
|
||||
|
||||
## 4. Encoding
|
||||
|
||||
### 4.1 DiagnosticEntry encoding
|
||||
|
||||
Logical:
|
||||
|
||||
```text
|
||||
DiagnosticEntry {
|
||||
code: uint32
|
||||
message: OctetString
|
||||
}
|
||||
```
|
||||
|
||||
Canonical encoding:
|
||||
|
||||
```text
|
||||
DiagnosticEntryBytes ::
|
||||
code (u32)
|
||||
message (Blob32)
|
||||
```
|
||||
|
||||
Where `Blob32` is as defined in §2.4.
|
||||
|
||||
* `code (u32)` encodes the diagnostic or error code.
|
||||
* `message` is an opaque byte blob; profile users MAY agree to use UTF-8 here, but this encoding does not enforce it.
|
||||
|
||||
Decoders MUST:
|
||||
|
||||
* Read `code (u32)`.
|
||||
* Read `message` as `Blob32`.
|
||||
* Treat truncated blobs as encoding errors.
|
||||
|
||||
---
|
||||
|
||||
### 4.2 NodeTraceDAG encoding
|
||||
|
||||
Logical:
|
||||
|
||||
```text
|
||||
NodeTraceDAG {
|
||||
node_id: NodeId
|
||||
op_name: string
|
||||
op_version: uint32
|
||||
|
||||
status: NodeTraceStatus
|
||||
status_code: uint32
|
||||
|
||||
output_refs: list<Reference>
|
||||
diagnostics: list<DiagnosticEntry>
|
||||
}
|
||||
```
|
||||
|
||||
Canonical encoding:
|
||||
|
||||
```text
|
||||
NodeTraceDAGBytes ::
|
||||
node_id (u32)
|
||||
op_name (Utf8String)
|
||||
op_version (u32)
|
||||
|
||||
status (u8) // NodeTraceStatus
|
||||
status_code (u32)
|
||||
|
||||
output_ref_count (u32)
|
||||
output_refs (EncodedRef[0..output_ref_count-1])
|
||||
|
||||
diag_count (u32)
|
||||
diagnostics (DiagnosticEntryBytes[0..diag_count-1])
|
||||
```
|
||||
|
||||
Field semantics:
|
||||
|
||||
1. `node_id (u32)`
|
||||
|
||||
* Encodes `NodeTraceDAG.node_id`.
|
||||
|
||||
2. `op_name (Utf8String)`
|
||||
|
||||
* Encodes `NodeTraceDAG.op_name` as UTF-8 (see §2.3).
|
||||
|
||||
3. `op_version (u32)`
|
||||
|
||||
* Encodes `NodeTraceDAG.op_version`.
|
||||
|
||||
4. `status (u8)`
|
||||
|
||||
* Encodes `NodeTraceStatus`:
|
||||
|
||||
```text
|
||||
0x00 -> NODE_OK
|
||||
0x01 -> NODE_FAILED
|
||||
0x02 -> NODE_SKIPPED
|
||||
```
|
||||
|
||||
* Other values MUST be treated as encoding errors.
|
||||
|
||||
5. `status_code (u32)`
|
||||
|
||||
* MUST be:
|
||||
|
||||
* `0` if `status = NODE_OK` or `NODE_SKIPPED`.
|
||||
* non-zero if `status = NODE_FAILED`.
|
||||
|
||||
* Conformance to these rules is a semantic requirement, not a decoding requirement. Decoders MAY choose to validate and reject inconsistent encodings.
|
||||
|
||||
6. `output_ref_count (u32)` and `output_refs`
|
||||
|
||||
* Number of output references for this node.
|
||||
* Each entry is an `EncodedRef` (§2.5).
|
||||
|
||||
7. `diag_count (u32)` and `diagnostics`
|
||||
|
||||
* Number of diagnostic entries.
|
||||
* Each entry is encoded using `DiagnosticEntryBytes` (§4.1).
|
||||
|
||||
#### 4.2.1 Canonical ordering of node_traces
|
||||
|
||||
In `TraceDAGBytes`, the `node_traces` list (see §4.4) MUST:
|
||||
|
||||
* contain each `NodeTraceDAG` exactly once for each Program `Node`,
|
||||
* appear in the canonical node order defined by `PEL/PROGRAM-DAG/1` (canonical topological order with `NodeId` as tie-breaker).
|
||||
|
||||
Encoders MUST enforce this; decoders MAY assume it.
|
||||
|
||||
---
|
||||
|
||||
### 4.3 Summary and status encoding
|
||||
|
||||
From `TraceDAGValue`:
|
||||
|
||||
```text
|
||||
summary: ExecutionErrorSummary {
|
||||
kind: ExecutionErrorKind
|
||||
status_code: uint32
|
||||
}
|
||||
status: ExecutionStatus
|
||||
```
|
||||
|
||||
These are encoded in `TraceDAGBytes` as:
|
||||
|
||||
```text
|
||||
status (u8) // ExecutionStatus
|
||||
summary_kind (u8) // ExecutionErrorKind
|
||||
summary_status_code (u32)
|
||||
```
|
||||
|
||||
The exact value sets of `ExecutionStatus` and `ExecutionErrorKind` are defined in `PEL/1-CORE` and `PEL/TRACE-DAG/1`; this spec treats them as small enums in `u8` space.
|
||||
|
||||
Decoders MUST:
|
||||
|
||||
* Read `status (u8)`, `summary_kind (u8)`, `summary_status_code (u32)` as raw fields.
|
||||
* Treat `status` and `summary_kind` values outside the agreed ranges as encoding errors or map them to an “unknown” variant at the semantic layer.
|
||||
|
||||
---
|
||||
|
||||
### 4.4 TraceDAGValue encoding
|
||||
|
||||
Logical:
|
||||
|
||||
```text
|
||||
TraceDAGValue {
|
||||
pel1_version: uint16
|
||||
scheme_ref: Reference
|
||||
program_ref: Reference
|
||||
|
||||
status: ExecutionStatus
|
||||
summary: ExecutionErrorSummary
|
||||
|
||||
exec_result_ref: optional Reference
|
||||
|
||||
input_refs: list<Reference>
|
||||
params_ref: optional Reference
|
||||
|
||||
node_traces: list<NodeTraceDAG>
|
||||
}
|
||||
```
|
||||
|
||||
Canonical encoding:
|
||||
|
||||
```text
|
||||
TraceDAGBytes ::
|
||||
pel1_version (u16)
|
||||
|
||||
scheme_ref (EncodedRef)
|
||||
program_ref (EncodedRef)
|
||||
|
||||
status (u8) // ExecutionStatus
|
||||
summary_kind (u8) // ExecutionErrorKind
|
||||
summary_status_code (u32) // ExecutionErrorSummary.status_code
|
||||
|
||||
has_exec_result (u8)
|
||||
[ exec_result (EncodedRef) ] // if has_exec_result == 0x01
|
||||
|
||||
input_ref_count (u32)
|
||||
input_refs (EncodedRef[0..input_ref_count-1])
|
||||
|
||||
has_params_ref (u8)
|
||||
[ params_ref (EncodedRef) ] // if has_params_ref == 0x01
|
||||
|
||||
node_trace_count (u32)
|
||||
node_traces (NodeTraceDAGBytes[0..node_trace_count-1])
|
||||
```
|
||||
|
||||
Field semantics:
|
||||
|
||||
1. `pel1_version (u16)`
|
||||
|
||||
* MUST be `1` for traces produced under `PEL/TRACE-DAG/1 v0.1.0`.
|
||||
* Decoders:
|
||||
|
||||
* MUST accept `pel1_version = 1`.
|
||||
* MUST treat other values as encoding errors for this profile revision.
|
||||
|
||||
2. `scheme_ref (EncodedRef)`
|
||||
|
||||
* Encodes the `Reference` to the scheme descriptor; for this profile MUST be `SchemeRef_DAG_1`.
|
||||
|
||||
3. `program_ref (EncodedRef)`
|
||||
|
||||
* Encodes the `Reference` of the Program Artifact executed in this run.
|
||||
|
||||
4. `status`, `summary_kind`, `summary_status_code (u32)`
|
||||
|
||||
* As described in §4.3.
|
||||
|
||||
5. `has_exec_result (u8)` and `exec_result (EncodedRef)`
|
||||
|
||||
* Encodes `exec_result_ref : optional Reference`:
|
||||
|
||||
* `has_exec_result = 0x00` → absent, no `exec_result` bytes follow.
|
||||
* `has_exec_result = 0x01` → exactly one `EncodedRef` follows, encoding `exec_result_ref`.
|
||||
* Other values MUST be treated as encoding errors.
|
||||
|
||||
6. `input_ref_count (u32)` and `input_refs (EncodedRef[..])`
|
||||
|
||||
* Number and encoded values of the `input_refs` list.
|
||||
* Encodes `TraceDAGValue.input_refs` in order.
|
||||
|
||||
7. `has_params_ref (u8)` and `params_ref (EncodedRef)`
|
||||
|
||||
* Encodes `params_ref : optional Reference`:
|
||||
|
||||
* `has_params_ref = 0x00` → absent.
|
||||
* `has_params_ref = 0x01` → present, encoded as `EncodedRef`.
|
||||
* Other values MUST be treated as encoding errors.
|
||||
|
||||
8. `node_trace_count (u32)` and `node_traces (NodeTraceDAGBytes[..])`
|
||||
|
||||
* Number and encoded values of `node_traces`.
|
||||
* **Canonical requirement:** encoders MUST set `node_trace_count` equal to the number of `Node`s in the Program (for runs where at least one node is attempted), and MUST encode node traces in canonical node order (§4.2.1).
|
||||
|
||||
---
|
||||
|
||||
## 5. Canonicality & Injectivity
|
||||
|
||||
### 5.1 Injectivity
|
||||
|
||||
The mapping:
|
||||
|
||||
```text
|
||||
TraceDAGValue -> TraceDAGBytes
|
||||
```
|
||||
|
||||
defined by this profile MUST be **injective**:
|
||||
|
||||
* If `T1 != T2` as logical `TraceDAGValue` instances (per `PEL/TRACE-DAG/1`), then their encodings MUST differ:
|
||||
|
||||
```text
|
||||
T1 != T2 ⇒ TraceDAGBytes(T1) != TraceDAGBytes(T2)
|
||||
```
|
||||
|
||||
This is ensured by:
|
||||
|
||||
* fixed field ordering and explicit presence flags,
|
||||
* deterministic list ordering,
|
||||
* inclusion of all logically relevant fields.
|
||||
|
||||
### 5.2 Stability
|
||||
|
||||
The same logical trace value MUST always yield the same `TraceDAGBytes` across:
|
||||
|
||||
* implementations,
|
||||
* platforms,
|
||||
* time.
|
||||
|
||||
Encoders MUST NOT:
|
||||
|
||||
* reorder any list elements (e.g., `input_refs`, `node_traces`, `output_refs`, `diagnostics`),
|
||||
* introduce alternative encodings for integers or strings,
|
||||
* omit or reorder fields.
|
||||
|
||||
### 5.3 Node ordering
|
||||
|
||||
For runs where at least one node is attempted and the Program is structurally valid:
|
||||
|
||||
* `node_traces` MUST have exactly one entry per Program `Node` (per `PEL/PROGRAM-DAG/1`) in canonical node order.
|
||||
|
||||
If the Program cannot be decoded or is structurally invalid:
|
||||
|
||||
* `node_traces` MAY be empty; if non-empty, any node entries MUST still follow canonical node order for the subset present.
|
||||
|
||||
---
|
||||
|
||||
## 6. Trace Artifact Binding
|
||||
|
||||
### 6.1 TypeTag
|
||||
|
||||
Trace Artifacts for this profile MUST be ASL/1 Artifacts with:
|
||||
|
||||
```text
|
||||
Artifact {
|
||||
bytes = TraceDAGBytes
|
||||
type_tag = TYPE_TAG_PEL_TRACE_DAG_1
|
||||
}
|
||||
```
|
||||
|
||||
Where:
|
||||
|
||||
* `TYPE_TAG_PEL_TRACE_DAG_1` is a `TypeTag` with a concrete `tag_id` assigned in the global TypeTag registry for DAG traces.
|
||||
|
||||
This encoding profile:
|
||||
|
||||
* Refers to `TYPE_TAG_PEL_TRACE_DAG_1` symbolically.
|
||||
* Does not assign a numeric `tag_id`; that is handled in a separate registry.
|
||||
|
||||
### 6.2 Identity via ASL/1-CORE
|
||||
|
||||
With `ENC/ASL1-CORE v1` and `"ASL1"` hashes (`HASH/ASL1`):
|
||||
|
||||
1. Canonical `ArtifactBytes` for a trace Artifact:
|
||||
|
||||
```text
|
||||
ArtifactBytes =
|
||||
encode_artifact_core_v1(
|
||||
Artifact{
|
||||
bytes = TraceDAGBytes,
|
||||
type_tag = TYPE_TAG_PEL_TRACE_DAG_1
|
||||
}
|
||||
)
|
||||
```
|
||||
|
||||
2. Canonical `Reference` for the trace Artifact under some `HashId = HID`:
|
||||
|
||||
```text
|
||||
digest = H(ArtifactBytes) // H from HASH/ASL1, for HID
|
||||
reference = Reference { hash_id = HID,
|
||||
digest = digest }
|
||||
```
|
||||
|
||||
All conformant implementations MUST agree on:
|
||||
|
||||
* `TraceDAGBytes` for a given logical `TraceDAGValue`,
|
||||
* `ArtifactBytes` for the resulting trace Artifact,
|
||||
* the resulting `Reference` for any fixed `HashId` and hash algorithm.
|
||||
|
||||
---
|
||||
|
||||
## 7. Error Handling (Encoding Layer)
|
||||
|
||||
Decoders for this profile MUST treat as **encoding errors**:
|
||||
|
||||
1. Truncated values:
|
||||
|
||||
* Any attempt to read a declared integer, length-prefixed blob (`Blob32`, `Utf8String`, `EncodedRef`), or list entry that runs out of bytes.
|
||||
|
||||
2. Invalid `pel1_version`:
|
||||
|
||||
* `pel1_version != 1`.
|
||||
|
||||
3. Invalid `NodeTraceStatus`:
|
||||
|
||||
* `status` not in `{ 0x00, 0x01, 0x02 }`.
|
||||
|
||||
4. Invalid optional flags:
|
||||
|
||||
* `has_exec_result` or `has_params_ref` not in `{ 0x00, 0x01 }`.
|
||||
|
||||
5. Invalid `EncodedRef`:
|
||||
|
||||
* `ref_len < 2`, or
|
||||
* `ref_bytes` cannot be decoded as `ReferenceBytes` (per `ENC/ASL1-CORE v1.0.3`).
|
||||
|
||||
6. Invalid `Utf8String` in `op_name`:
|
||||
|
||||
* `op_name` bytes not valid UTF-8.
|
||||
|
||||
7. Inconsistent list counts:
|
||||
|
||||
* Not enough elements following a list count (e.g. `input_ref_count`, `node_trace_count`, `output_ref_count`, `diag_count`).
|
||||
|
||||
Mapping from these encoding errors to external error codes (e.g. `ERR_PEL_TRACE_ENC_INVALID`) is implementation-specific.
|
||||
|
||||
Semantic inconsistencies (e.g. mismatched `summary` vs `status`) are semantic-layer issues; decoders MAY validate them but are not required to at the encoding layer.
|
||||
|
||||
---
|
||||
|
||||
## 8. Streaming & Implementation Notes
|
||||
|
||||
Implementation requirements:
|
||||
|
||||
* **Single-pass encoding**:
|
||||
|
||||
* Encoders MUST be able to generate `TraceDAGBytes` in a single forward pass over the logical `TraceDAGValue`, assuming they have the structure in memory.
|
||||
* They MAY need to precompute counts or sizes (e.g., `node_trace_count`), but this is standard.
|
||||
|
||||
* **Single-pass decoding**:
|
||||
|
||||
* Decoders MUST be able to decode `TraceDAGBytes` in a single forward pass, with no backtracking.
|
||||
* All length prefixes appear before their content.
|
||||
|
||||
For large traces:
|
||||
|
||||
* Implementations MAY:
|
||||
|
||||
* stream `NodeTraceDAGBytes` entries to consumers as they decode,
|
||||
* stream diagnostic message blobs.
|
||||
|
||||
* They MUST ensure that any observable behavior (including error reporting and any reconstructed `TraceDAGValue`) is independent of chunking or I/O strategy.
|
||||
|
||||
---
|
||||
|
||||
## 9. Conformance
|
||||
|
||||
An implementation is **ENC/PEL-TRACE-DAG/1–conformant** if it:
|
||||
|
||||
1. **Implements the encoding layout**
|
||||
|
||||
* Encodes and decodes `TraceDAGBytes` exactly as described in §4.
|
||||
* Treats `pel1_version = 1` as the only supported version for this profile revision.
|
||||
* Enforces validity of discriminants and presence flags at the encoding layer.
|
||||
|
||||
2. **Preserves canonical ordering**
|
||||
|
||||
* When encoding, preserves:
|
||||
|
||||
* order of `input_refs`,
|
||||
* canonical order of `node_traces` (per `PEL/PROGRAM-DAG/1`),
|
||||
* order of `output_refs` and `diagnostics` within each `NodeTraceDAG`.
|
||||
|
||||
3. **Uses canonical sub-encodings**
|
||||
|
||||
* Uses `Utf8String` and `Blob32` exactly as in §2.
|
||||
* Uses `EncodedRef` as defined in §2.5, with `ReferenceBytes` from `ENC/ASL1-CORE v1.0.3`.
|
||||
|
||||
4. **Ensures injectivity & stability**
|
||||
|
||||
* Ensures distinct logical `TraceDAGValue`s produce distinct `TraceDAGBytes`.
|
||||
* Ensures the same logical value always encodes to the same bytes (no configuration affecting layout).
|
||||
|
||||
5. **Binds to trace Artifacts correctly**
|
||||
|
||||
* When forming trace Artifacts for `PEL/TRACE-DAG/1`, sets:
|
||||
|
||||
* `Artifact.bytes = TraceDAGBytes`
|
||||
* `Artifact.type_tag = TYPE_TAG_PEL_TRACE_DAG_1`
|
||||
|
||||
* Uses `ENC/ASL1-CORE v1` and `HASH/ASL1` for identity.
|
||||
|
||||
Everything else — storage, transport, policy, and graph interpretation — is delegated to other specifications.
|
||||
|
||||
---
|
||||
|
||||
## 10. Informative Example
|
||||
|
||||
> This example illustrates field layout only.
|
||||
> Hex and values are illustrative, not normative test vectors.
|
||||
|
||||
Assume a simple run:
|
||||
|
||||
* `pel1_version = 1`
|
||||
* `scheme_ref = S` (an ASL/1 Reference)
|
||||
* `program_ref = P`
|
||||
* `status = OK (0)`
|
||||
* `summary.kind = NONE (0)`, `summary.status_code = 0`
|
||||
* `exec_result_ref = R`
|
||||
* Inputs: three `Reference`s `[I0, I1, I2]`
|
||||
* No params (`params_ref = absent`)
|
||||
* Program has two nodes in canonical order, with traces:
|
||||
|
||||
* Node 1: OK, produced one output `[O0]`
|
||||
* Node 2: OK, produced one output `[O1]`
|
||||
|
||||
Simplified encoding sketch:
|
||||
|
||||
```text
|
||||
pel1_version = 0001 ; u16
|
||||
|
||||
scheme_ref = EncodedRef(S) ; 4-byte length + ReferenceBytes(S)
|
||||
program_ref = EncodedRef(P)
|
||||
|
||||
status = 00 ; OK
|
||||
summary_kind = 00 ; NONE
|
||||
summary_status_code = 00000000 ; status_code = 0
|
||||
|
||||
has_exec_result = 01
|
||||
exec_result = EncodedRef(R)
|
||||
|
||||
input_ref_count = 00000003
|
||||
input_refs = EncodedRef(I0) EncodedRef(I1) EncodedRef(I2)
|
||||
|
||||
has_params_ref = 00 ; none
|
||||
|
||||
node_trace_count = 00000002
|
||||
|
||||
; NodeTrace #0
|
||||
node_id = 00000001
|
||||
op_name = 00000005 "add64"
|
||||
op_version = 00000001
|
||||
status = 00 ; NODE_OK
|
||||
status_code = 00000000
|
||||
output_ref_count = 00000001
|
||||
output_refs = EncodedRef(O0)
|
||||
diag_count = 00000000
|
||||
|
||||
; NodeTrace #1
|
||||
node_id = 00000002
|
||||
op_name = 00000005 "mul64"
|
||||
op_version = 00000001
|
||||
status = 00 ; NODE_OK
|
||||
status_code = 00000000
|
||||
output_ref_count = 00000001
|
||||
output_refs = EncodedRef(O1)
|
||||
diag_count = 00000000
|
||||
```
|
||||
|
||||
Where each `EncodedRef(X)` is:
|
||||
|
||||
```text
|
||||
ref_len(X) (u32) || ReferenceBytes(X)
|
||||
```
|
||||
|
||||
with `ReferenceBytes(X)` = `hash_id (u16)` + `digest` bytes per `ENC/ASL1-CORE v1`.
|
||||
|
||||
All conformant encoders MUST produce the same `TraceDAGBytes` for this logical trace value; all conformant decoders MUST reconstruct the same `TraceDAGValue`.
|
||||
|
||||
---
|
||||
|
||||
**End of `ENC/PEL-TRACE-DAG/1 v0.1.0 — Canonical Encoding for DAG Execution Traces`**
|
||||
|
||||
---
|
||||
|
||||
## Document History
|
||||
|
||||
* **0.1.0 (2025-11-16):** Registered as Tier-1 spec and aligned to the Amduat 2.0 substrate baseline.
|
||||
1108
tier1/enc-pel1-result-1.md
Normal file
1108
tier1/enc-pel1-result-1.md
Normal file
File diff suppressed because it is too large
Load diff
674
tier1/opreg-pel1-kernel-params-1.md
Normal file
674
tier1/opreg-pel1-kernel-params-1.md
Normal file
|
|
@ -0,0 +1,674 @@
|
|||
# OPREG/PEL1-KERNEL-PARAMS/1 — Kernel Operation Parameter Encodings
|
||||
|
||||
Status: Approved
|
||||
Owner: Niklas Rydberg
|
||||
Version: 0.1.1
|
||||
SoT: Yes
|
||||
Last Updated: 2025-11-16
|
||||
Linked Phase Pack: N/A
|
||||
Tags: [registry, binary-minimalism]
|
||||
|
||||
<!-- Source: /amduat/docs/new/opreg-pel1-kernel-params-1.md | Canonical: /amduat/tier1/opreg-pel1-kernel-params-1.md -->
|
||||
|
||||
**Document ID:** `OPREG/PEL1-KERNEL-PARAMS/1`
|
||||
**Layer:** L1 Profile (Parameter Encoding for `OPREG/PEL1-KERNEL`)
|
||||
|
||||
**Depends on (normative):**
|
||||
|
||||
* `ASL/1-CORE v0.3.x` — `Artifact`, `TypeTag`, `Reference`, `HashId`
|
||||
* `HASH/ASL1 v0.2.x` — ASL1 hash family (for `HashId` constraints)
|
||||
* `OPREG/PEL1-KERNEL v0.1.1` — kernel operation semantics
|
||||
|
||||
**Integrates with (informative):**
|
||||
|
||||
* `PEL/PROGRAM-DAG/1` — DAG program scheme (Node parameters)
|
||||
* `PEL/1-CORE` — primitive execution semantics
|
||||
|
||||
© 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. Purpose and Scope
|
||||
|
||||
`OPREG/PEL1-KERNEL-PARAMS/1` defines the **canonical binary encodings** for the logical Params types used by the kernel operations in `OPREG/PEL1-KERNEL` v0.1.1:
|
||||
|
||||
* `pel.bytes.concat/1`
|
||||
* `pel.bytes.slice/1`
|
||||
* `pel.bytes.const/1`
|
||||
* `pel.bytes.hash.asl1/1`
|
||||
|
||||
It specifies, for each operation:
|
||||
|
||||
1. The **logical Params value type** (e.g. `SliceParams`).
|
||||
|
||||
2. The **canonical encoding** function:
|
||||
|
||||
```text
|
||||
encode_params(OpParams) -> OctetString
|
||||
```
|
||||
|
||||
3. The **canonical decoding** function:
|
||||
|
||||
```text
|
||||
decode_params(OctetString) -> OpParams | error
|
||||
```
|
||||
|
||||
4. How **decode errors** must be treated in the context of `PEL/PROGRAM-DAG/1`
|
||||
(always as `INVALID_PROGRAM` for these kernel ops).
|
||||
|
||||
This document is deliberately independent of any **Program encoding** format.
|
||||
A Program representation (e.g. `ENC/PEL-PROGRAM-DAG/1`) simply needs to:
|
||||
|
||||
* store the operation’s Params as an **opaque OctetString**, and
|
||||
* feed that OctetString into the encoders/decoders defined here.
|
||||
|
||||
For each Params type, the encoding defined here is the only canonical encoding; engines MUST NOT accept alternative layouts.
|
||||
|
||||
---
|
||||
|
||||
## 1. Conventions
|
||||
|
||||
### 1.1 Base types
|
||||
|
||||
From `ASL/1-CORE`:
|
||||
|
||||
```text
|
||||
OctetString = finite sequence of bytes (0x00–0xFF)
|
||||
|
||||
HashId = uint16
|
||||
```
|
||||
|
||||
In this document, OctetString is the logical type ‘sequence of bytes’. When we encode an OctetString as part of Params (e.g. ConstParams.bytes), we use [u64 length][bytes].
|
||||
|
||||
This document introduces the following fixed-width integer types:
|
||||
|
||||
```text
|
||||
u8 = unsigned 8-bit integer
|
||||
u16 = unsigned 16-bit integer
|
||||
u32 = unsigned 32-bit integer
|
||||
u64 = unsigned 64-bit integer
|
||||
```
|
||||
|
||||
### 1.2 Byte order and integer encoding
|
||||
|
||||
All multi-byte integers in parameter encodings are encoded:
|
||||
|
||||
* as **big-endian** (most significant byte first),
|
||||
* using a **fixed width** (1, 2, 4, or 8 bytes).
|
||||
|
||||
Conversions:
|
||||
|
||||
* `u16` → 2 bytes
|
||||
* `u32` → 4 bytes
|
||||
* `u64` → 8 bytes
|
||||
|
||||
### 1.3 Boolean encoding
|
||||
|
||||
Booleans are encoded as:
|
||||
|
||||
```text
|
||||
false -> 0x00
|
||||
true -> 0x01
|
||||
```
|
||||
|
||||
Any other value is invalid and MUST be treated as a decode error.
|
||||
|
||||
### 1.4 OctetString encoding (embedded)
|
||||
|
||||
When an OctetString is encoded as part of Params, it uses:
|
||||
|
||||
```text
|
||||
[length: u64] [bytes: b[length]]
|
||||
```
|
||||
|
||||
* `length` is the number of bytes.
|
||||
* `length` MAY be zero.
|
||||
* There is no terminator or padding.
|
||||
|
||||
### 1.5 Param payload
|
||||
|
||||
For each Node in a Program, the scheme-level “Params” field is represented as an **OctetString `params_bytes`**.
|
||||
|
||||
This document defines, for kernel operations, what it means for `params_bytes` to represent:
|
||||
|
||||
* `Unit` (no parameters),
|
||||
* `SliceParams`,
|
||||
* `ConstParams`,
|
||||
* `HashParams`.
|
||||
|
||||
Other operations (non-kernel) may use other param-encoding profiles.
|
||||
|
||||
### 1.6 Error handling model
|
||||
|
||||
For all kernel operations:
|
||||
|
||||
> **Any param decode error MUST be treated as a static program error (`INVALID_PROGRAM`) in `PEL/PROGRAM-DAG/1`, not as a runtime error.**
|
||||
|
||||
Concretely:
|
||||
|
||||
* If `decode_params` fails for a Node during Program validation,
|
||||
`Exec_DAG` MUST treat the Program as invalid and produce `status = INVALID_PROGRAM`, not `RUNTIME_FAILED`.
|
||||
|
||||
### 1.7 Relationship to `ENC/PEL-PROGRAM-DAG/1` and size bounds
|
||||
|
||||
In contexts that use `ENC/PEL-PROGRAM-DAG/1`, each `Node` carries an operation-specific parameter payload in its `params_bytes` field. For kernel operations defined in `OPREG/PEL1-KERNEL`:
|
||||
|
||||
* The `params_bytes` field of a `Node` **MUST** be exactly the byte sequence returned by the corresponding `encode_params_*` function for that Node’s operation.
|
||||
* Engines validating or executing a `PEL/PROGRAM-DAG/1` `Program` **MUST** feed `params_bytes` into the matching `decode_params_*` function for that operation.
|
||||
|
||||
Because `ENC/PEL-PROGRAM-DAG/1` represents `params_bytes` with a `params_len : u32` length prefix, all `encode_params_*` functions defined in this document **MUST** produce parameter payloads whose length is ≤ `0xFFFF_FFFF` (2³² − 1) bytes. Any logical parameter value that would require a larger encoding **MUST** either:
|
||||
|
||||
* be rejected at parameter construction time, or
|
||||
* be represented via separate input `Artifact`s instead of being inlined as Node parameters.
|
||||
|
||||
For kernel operations, any failure to decode `params_bytes` with the corresponding `decode_params_*` function (including violations of the size bound above) **MUST** be reported to the `PEL/PROGRAM-DAG/1` layer as a parameter-decoding error and treated as an **invalid Program**, not as a runtime failure during execution.
|
||||
|
||||
---
|
||||
|
||||
## 2. Operation Param Types (Logical)
|
||||
|
||||
For reference (from `OPREG/PEL1-KERNEL`):
|
||||
|
||||
```text
|
||||
// pel.bytes.concat/1
|
||||
ConcatParams = Unit
|
||||
|
||||
// pel.bytes.slice/1
|
||||
SliceParams {
|
||||
offset: u64
|
||||
length: u64
|
||||
}
|
||||
|
||||
// pel.bytes.const/1
|
||||
ConstParams {
|
||||
bytes: OctetString
|
||||
has_tag: bool
|
||||
tag_id: u32 optional // only meaningful when has_tag = true
|
||||
}
|
||||
|
||||
// pel.bytes.hash.asl1/1
|
||||
HashParams {
|
||||
hash_id: HashId // uint16
|
||||
}
|
||||
```
|
||||
|
||||
This specification does **not** change these logical types; it only provides their canonical encodings.
|
||||
|
||||
---
|
||||
|
||||
## 3. Unit Params Encoding (`pel.bytes.concat`)
|
||||
|
||||
Applies to:
|
||||
|
||||
* `pel.bytes.concat/1`
|
||||
|
||||
### 3.1 Logical type
|
||||
|
||||
```text
|
||||
Unit = ()
|
||||
```
|
||||
|
||||
There is a single value.
|
||||
|
||||
### 3.2 Encoding
|
||||
|
||||
```text
|
||||
encode_params_unit(Unit) -> OctetString
|
||||
```
|
||||
|
||||
Definition:
|
||||
|
||||
```text
|
||||
encode_params_unit(()) = "" // zero-length OctetString
|
||||
```
|
||||
|
||||
That is, `params_bytes` MUST be an empty byte sequence.
|
||||
|
||||
### 3.3 Decoding
|
||||
|
||||
```text
|
||||
decode_params_unit(params_bytes: OctetString) -> Unit | error
|
||||
```
|
||||
|
||||
Algorithm:
|
||||
|
||||
1. If `len(params_bytes) != 0`:
|
||||
|
||||
* return `error`.
|
||||
|
||||
2. Otherwise:
|
||||
|
||||
* return `()`.
|
||||
|
||||
### 3.4 Conformance rule
|
||||
|
||||
For `pel.bytes.concat/1`:
|
||||
|
||||
* `params_bytes` MUST be encoded using `encode_params_unit`.
|
||||
* Any non-empty `params_bytes` MUST be treated as a **decode error** and thus `INVALID_PROGRAM` in `PEL/PROGRAM-DAG/1`.
|
||||
|
||||
---
|
||||
|
||||
## 4. SliceParams Encoding (`pel.bytes.slice`)
|
||||
|
||||
Applies to:
|
||||
|
||||
* `pel.bytes.slice/1`
|
||||
|
||||
### 4.1 Logical type
|
||||
|
||||
```text
|
||||
SliceParams {
|
||||
offset: u64 // 0-based byte offset
|
||||
length: u64 // number of bytes
|
||||
}
|
||||
```
|
||||
|
||||
### 4.2 Encoding
|
||||
|
||||
```text
|
||||
encode_params_slice(SliceParams) -> OctetString
|
||||
```
|
||||
|
||||
Given:
|
||||
|
||||
```text
|
||||
SliceParams { offset, length }
|
||||
```
|
||||
|
||||
The encoding is:
|
||||
|
||||
```text
|
||||
[offset: u64] [length: u64]
|
||||
```
|
||||
|
||||
where both `offset` and `length` are encoded as big-endian `u64`.
|
||||
|
||||
So:
|
||||
|
||||
* Total length of `params_bytes` MUST be exactly 16 bytes.
|
||||
|
||||
### 4.3 Decoding
|
||||
|
||||
```text
|
||||
decode_params_slice(params_bytes: OctetString) -> SliceParams | error
|
||||
```
|
||||
|
||||
Algorithm:
|
||||
|
||||
1. If `len(params_bytes) != 16`:
|
||||
|
||||
* return `error`.
|
||||
|
||||
2. Parse the first 8 bytes as `offset: u64` (big-endian).
|
||||
|
||||
3. Parse the next 8 bytes as `length: u64` (big-endian).
|
||||
|
||||
4. Construct:
|
||||
|
||||
```text
|
||||
SliceParams { offset, length }
|
||||
```
|
||||
|
||||
and return it.
|
||||
|
||||
This decoding does **not** apply any semantic checks on `offset` or `length` (such as “must be in range for a particular input”). Those checks are done at operation runtime and mapped to `RANGE_OUT_OF_BOUNDS` (`status_code = 0x0002_0001`) as specified in `OPREG/PEL1-KERNEL`.
|
||||
|
||||
### 4.4 Conformance rule
|
||||
|
||||
* `params_bytes` for a `pel.bytes.slice/1` Node MUST be exactly 16 bytes, encoded as described.
|
||||
* Any other length or malformed encoding MUST be treated as a **decode error** ⇒ `INVALID_PROGRAM`.
|
||||
|
||||
---
|
||||
|
||||
## 5. ConstParams Encoding (`pel.bytes.const`)
|
||||
|
||||
Applies to:
|
||||
|
||||
* `pel.bytes.const/1`
|
||||
|
||||
### 5.1 Logical type
|
||||
|
||||
```text
|
||||
ConstParams {
|
||||
bytes: OctetString
|
||||
has_tag: bool
|
||||
tag_id: u32 optional
|
||||
}
|
||||
```
|
||||
|
||||
Semantics:
|
||||
|
||||
* If `has_tag == false`:
|
||||
|
||||
* The output Artifact will have `type_tag = None`.
|
||||
|
||||
* If `has_tag == true`:
|
||||
|
||||
* The output Artifact will have `type_tag = Some(TypeTag{ tag_id })`.
|
||||
|
||||
### 5.2 Encoding
|
||||
|
||||
```text
|
||||
encode_params_const(ConstParams) -> OctetString
|
||||
```
|
||||
|
||||
Given:
|
||||
|
||||
```text
|
||||
ConstParams { bytes = B, has_tag, tag_id? }
|
||||
```
|
||||
|
||||
The encoding is:
|
||||
|
||||
```text
|
||||
[has_tag: u8] [tag_id: u32?] [len: u64] [B: b[len]]
|
||||
```
|
||||
|
||||
Where:
|
||||
|
||||
1. `has_tag: u8`
|
||||
|
||||
* `0x00` if `has_tag == false`.
|
||||
* `0x01` if `has_tag == true`.
|
||||
|
||||
2. `tag_id: u32` (only when `has_tag == true`)
|
||||
|
||||
* Encoded as big-endian `u32`.
|
||||
* Omitted entirely when `has_tag == false`.
|
||||
|
||||
3. `len: u64`
|
||||
|
||||
* Length in bytes of `B`.
|
||||
* Encoded as big-endian `u64`.
|
||||
|
||||
4. `B: b[len]`
|
||||
|
||||
* The raw bytes of the payload.
|
||||
|
||||
So:
|
||||
|
||||
* If `has_tag == false`, layout is:
|
||||
|
||||
```text
|
||||
[0x00] [len: u64] [B: b[len]]
|
||||
```
|
||||
|
||||
* If `has_tag == true`, layout is:
|
||||
|
||||
```text
|
||||
[0x01] [tag_id: u32] [len: u64] [B: b[len]]
|
||||
```
|
||||
|
||||
### 5.3 Decoding
|
||||
|
||||
```text
|
||||
decode_params_const(params_bytes: OctetString) -> ConstParams | error
|
||||
```
|
||||
|
||||
Algorithm:
|
||||
|
||||
1. If `len(params_bytes) < 1`:
|
||||
|
||||
* return `error`.
|
||||
|
||||
2. Read the first byte as `flag: u8`.
|
||||
|
||||
* If `flag == 0x00`, then `has_tag = false`.
|
||||
* If `flag == 0x01`, then `has_tag = true`.
|
||||
* Otherwise (any other value): return `error`.
|
||||
|
||||
3. If `has_tag == false`:
|
||||
|
||||
1. Ensure at least `1 + 8` bytes are present:
|
||||
|
||||
* If `len(params_bytes) < 1 + 8`: return `error`.
|
||||
|
||||
2. Parse the next 8 bytes as `len: u64` (big-endian).
|
||||
|
||||
3. Compute `expected_total = 1 + 8 + len`.
|
||||
|
||||
* If `len(params_bytes) != expected_total`: return `error`.
|
||||
|
||||
4. Let `B` be the remaining `len` bytes.
|
||||
|
||||
5. Return:
|
||||
|
||||
```text
|
||||
ConstParams {
|
||||
bytes = B
|
||||
has_tag = false
|
||||
tag_id = (absent)
|
||||
}
|
||||
```
|
||||
|
||||
4. If `has_tag == true`:
|
||||
|
||||
1. Ensure at least `1 + 4 + 8` bytes are present:
|
||||
|
||||
* If `len(params_bytes) < 1 + 4 + 8`: return `error`.
|
||||
|
||||
2. Parse next 4 bytes as `tag_id: u32` (big-endian).
|
||||
|
||||
3. Parse next 8 bytes as `len: u64` (big-endian).
|
||||
|
||||
4. Compute `expected_total = 1 + 4 + 8 + len`.
|
||||
|
||||
* If `len(params_bytes) != expected_total`: return `error`.
|
||||
|
||||
5. Let `B` be the remaining `len` bytes.
|
||||
|
||||
6. Return:
|
||||
|
||||
```text
|
||||
ConstParams {
|
||||
bytes = B
|
||||
has_tag = true
|
||||
tag_id = tag_id
|
||||
}
|
||||
```
|
||||
|
||||
### 5.4 Conformance rule
|
||||
|
||||
* For `pel.bytes.const/1`, `params_bytes` MUST be encoded according to `encode_params_const`.
|
||||
* Any malformed encoding (invalid `has_tag`, truncated data, mismatched length, etc.) MUST be treated as a **decode error** ⇒ `INVALID_PROGRAM`.
|
||||
|
||||
---
|
||||
|
||||
## 6. HashParams Encoding (`pel.bytes.hash.asl1`)
|
||||
|
||||
Applies to:
|
||||
|
||||
* `pel.bytes.hash.asl1/1`
|
||||
|
||||
### 6.1 Logical type
|
||||
|
||||
```text
|
||||
HashParams {
|
||||
hash_id: HashId // uint16
|
||||
}
|
||||
```
|
||||
|
||||
### 6.2 Encoding
|
||||
|
||||
```text
|
||||
encode_params_hash(HashParams) -> OctetString
|
||||
```
|
||||
|
||||
Given:
|
||||
|
||||
```text
|
||||
HashParams { hash_id }
|
||||
```
|
||||
|
||||
The encoding is:
|
||||
|
||||
```text
|
||||
[hash_id: u16]
|
||||
```
|
||||
|
||||
Where:
|
||||
|
||||
* `hash_id` is encoded as big-endian `u16`.
|
||||
|
||||
So `params_bytes` MUST be exactly 2 bytes.
|
||||
|
||||
### 6.3 Decoding
|
||||
|
||||
```text
|
||||
decode_params_hash(params_bytes: OctetString) -> HashParams | error
|
||||
```
|
||||
|
||||
Algorithm:
|
||||
|
||||
1. If `len(params_bytes) != 2`: return `error`.
|
||||
|
||||
2. Parse the 2 bytes as `hash_id: u16` (big-endian).
|
||||
|
||||
3. For `pel.bytes.hash.asl1/1` **in this version**:
|
||||
|
||||
* If `hash_id != 0x0001`:
|
||||
|
||||
* return `error`.
|
||||
|
||||
* Else:
|
||||
|
||||
* return `HashParams { hash_id }`.
|
||||
|
||||
Rationale:
|
||||
|
||||
* `OPREG/PEL1-KERNEL` constrains `pel.bytes.hash.asl1/1` to `hash_id = 0x0001` (`HASH-ASL1-256`) for cross-implementation determinism.
|
||||
* Supporting additional `HashId`s requires a new operation version (e.g. `pel.bytes.hash.asl1/2`) and/or an updated parameter profile.
|
||||
|
||||
### 6.4 Conformance rule
|
||||
|
||||
* For `pel.bytes.hash.asl1/1`, `params_bytes` MUST:
|
||||
|
||||
* be exactly 2 bytes long, and
|
||||
* encode `hash_id = 0x0001`.
|
||||
|
||||
* Any other length or `hash_id` MUST be treated as a **decode error** ⇒ `INVALID_PROGRAM`.
|
||||
|
||||
---
|
||||
|
||||
## 7. Integration with PEL/PROGRAM-DAG/1 (Informative)
|
||||
|
||||
In a `PEL/PROGRAM-DAG/1` Program:
|
||||
|
||||
* Each `Node` has:
|
||||
|
||||
* an `OperationId { name, version }`, and
|
||||
* a `params_bytes: OctetString` (representation-specific; this spec does not define the layout of the Node itself).
|
||||
|
||||
* For Nodes whose `OperationId` is one of the kernel ops from `OPREG/PEL1-KERNEL`:
|
||||
|
||||
* The engine MUST:
|
||||
|
||||
1. Select the appropriate `decode_params_*` function from this document based on `OperationId.name` and `version`.
|
||||
|
||||
2. Pass `params_bytes` to that function.
|
||||
|
||||
3. If decoding fails, treat the Program as `INVALID_PROGRAM` as per `PEL/PROGRAM-DAG/1`:
|
||||
|
||||
```text
|
||||
ExecutionStatus = INVALID_PROGRAM
|
||||
ExecutionErrorKind = PROGRAM
|
||||
summary.status_code = 2
|
||||
```
|
||||
|
||||
4. If decoding succeeds, use the resulting Params value for the operation semantics.
|
||||
|
||||
* For non-kernel operations, other param profiles apply; they MUST NOT conflict with these definitions.
|
||||
|
||||
---
|
||||
|
||||
## 8. Conformance
|
||||
|
||||
An implementation is **OPREG/PEL1-KERNEL-PARAMS/1–conformant** if and only if:
|
||||
|
||||
1. **Encoding/decoding correctness**
|
||||
|
||||
* For each kernel operation:
|
||||
|
||||
* `encode_params_*` and `decode_params_*` are implemented exactly as specified.
|
||||
|
||||
* For all valid Params values:
|
||||
|
||||
```text
|
||||
decode_params_*(encode_params_*(value)) == value
|
||||
```
|
||||
|
||||
* For all `params_bytes` accepted by `decode_params_*`, the result is well-defined and deterministic.
|
||||
|
||||
2. **Error handling**
|
||||
|
||||
* Any malformed or non-canonical `params_bytes` detected by `decode_params_*` is treated as a **decode error**.
|
||||
* Decode errors for kernel operations MUST be mapped to `INVALID_PROGRAM` in `PEL/PROGRAM-DAG/1`, not `RUNTIME_FAILED`.
|
||||
|
||||
3. **Consistency with OPREG/PEL1-KERNEL**
|
||||
|
||||
* The logical Params types used in the engine’s implementation of kernel operations match those defined in `OPREG/PEL1-KERNEL`.
|
||||
* Runtime failures for kernel operations are **not** caused by param decode errors; they are caused only by data-dependent conditions specified in `OPREG/PEL1-KERNEL` (e.g. slice out-of-bounds).
|
||||
|
||||
4. **Determinism**
|
||||
|
||||
* For any given `params_bytes`, `decode_params_*` MUST return the same result (or error) across all conformant implementations.
|
||||
|
||||
5. **Layering**
|
||||
|
||||
* The implementation does not depend on any particular Program encoding.
|
||||
* It only consumes `params_bytes` as an OctetString and produces/consumes logical Params as defined here.
|
||||
|
||||
---
|
||||
|
||||
## 9. Change Log (Informative)
|
||||
|
||||
**v0.1.1 (2025-11-15)**
|
||||
|
||||
* Aligned with `OPREG/PEL1-KERNEL v0.1.1`:
|
||||
|
||||
* Removed `pel.bytes.clone/1` from the normative scope of this profile; the kernel parameter profile now covers only:
|
||||
|
||||
* `pel.bytes.concat/1`
|
||||
* `pel.bytes.slice/1`
|
||||
* `pel.bytes.const/1`
|
||||
* `pel.bytes.hash.asl1/1`
|
||||
|
||||
* Updated the informative reference in §4.3 so that `RANGE_OUT_OF_BOUNDS` now points to `status_code = 0x0002_0001`, reflecting the reassigned `kernel_op_code` for `pel.bytes.slice/1`.
|
||||
|
||||
* Clarified the dependency on `OPREG/PEL1-KERNEL v0.1.1` in the header.
|
||||
|
||||
**v0.1.0 (2025-11-15)**
|
||||
|
||||
* Introduced canonical parameter encodings for:
|
||||
|
||||
* `pel.bytes.clone/1` (Unit → empty `params_bytes`)
|
||||
* `pel.bytes.concat/1` (Unit → empty `params_bytes`)
|
||||
* `pel.bytes.slice/1` (`SliceParams { offset, length }` → 16-byte payload)
|
||||
* `pel.bytes.const/1` (`ConstParams` → `[has_tag][tag_id?][len][bytes]`)
|
||||
* `pel.bytes.hash.asl1/1` (`HashParams { hash_id }` → 2-byte payload; restricted to `0x0001`)
|
||||
|
||||
* Locked the rule that **all kernel param decode failures imply `INVALID_PROGRAM`**, not runtime failure.
|
||||
|
||||
* Kept the profile independent from any particular Program encoding (`ENC/PEL-PROGRAM-DAG/1`).
|
||||
|
||||
---
|
||||
|
||||
## Document History
|
||||
|
||||
* **0.1.1 (2025-11-16):** Registered as Tier-1 spec and aligned to the Amduat 2.0 substrate baseline.
|
||||
639
tier1/pel-1-core.md
Normal file
639
tier1/pel-1-core.md
Normal file
|
|
@ -0,0 +1,639 @@
|
|||
# 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 scheme’s 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 scheme’s 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 scheme’s 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 scheme’s `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-CORE–conformant** 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-CORE–conformant** 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-CORE–conformant 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.
|
||||
853
tier1/pel-1-surf.md
Normal file
853
tier1/pel-1-surf.md
Normal file
|
|
@ -0,0 +1,853 @@
|
|||
# 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.
|
||||
836
tier1/pel-program-dag-1.md
Normal file
836
tier1/pel-program-dag-1.md
Normal file
|
|
@ -0,0 +1,836 @@
|
|||
# PEL/PROGRAM-DAG/1 — DAG Program Scheme for PEL
|
||||
|
||||
Status: Approved
|
||||
Owner: Niklas Rydberg
|
||||
Version: 0.3.1
|
||||
SoT: Yes
|
||||
Last Updated: 2025-11-16
|
||||
Linked Phase Pack: N/A
|
||||
Tags: [execution, composition]
|
||||
|
||||
<!-- Source: /amduat/docs/new/pel-program-dag-1.md | Canonical: /amduat/tier1/pel-program-dag-1.md -->
|
||||
|
||||
**Document ID:** `PEL/PROGRAM-DAG/1`
|
||||
**Layer:** L1 Scheme Profile (on top of PEL/1-CORE)
|
||||
|
||||
**Depends on (normative):**
|
||||
|
||||
* `ASL/1-CORE v0.4.x` — Artifact Substrate (value model)
|
||||
* `PEL/1-CORE v0.3.x` — Primitive Execution Layer (core semantics)
|
||||
|
||||
**Integrates with (informative):**
|
||||
|
||||
* `PEL/1-SURF v0.2.x` — Store-backed execution surface
|
||||
* `ENC/PEL-PROGRAM-DAG/1` (planned) — Canonical encoding for DAG programs
|
||||
* `PEL/TRACE-DAG/1` (planned) — Node-level execution trace profile
|
||||
* `OPREG/PEL1-KERNEL` (planned) — Operation registry for DAG ops
|
||||
* `SUBSTRATE/STACK-OVERVIEW v0.1.x` — Kernel / near-core layering
|
||||
|
||||
© 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
|
||||
|
||||
RFC 2119 terms (**MUST**, **MUST NOT**, **SHOULD**, **MAY**, etc.) are normative.
|
||||
|
||||
From `ASL/1-CORE`:
|
||||
|
||||
```text
|
||||
Artifact {
|
||||
bytes: OctetString
|
||||
type_tag: optional TypeTag
|
||||
}
|
||||
|
||||
TypeTag {
|
||||
tag_id: uint32
|
||||
}
|
||||
|
||||
Reference {
|
||||
hash_id: HashId
|
||||
digest: OctetString
|
||||
}
|
||||
|
||||
HashId = uint16
|
||||
````
|
||||
|
||||
From `PEL/1-CORE` (summary):
|
||||
|
||||
```text
|
||||
SchemeRef = Reference
|
||||
|
||||
ExecutionStatus = uint8
|
||||
ExecutionErrorKind = uint8
|
||||
|
||||
ExecutionErrorSummary {
|
||||
kind: ExecutionErrorKind
|
||||
status_code: uint32
|
||||
}
|
||||
|
||||
DiagnosticEntry {
|
||||
code: uint32
|
||||
message: OctetString
|
||||
}
|
||||
|
||||
ExecutionResultValue {
|
||||
pel1_version : uint16
|
||||
status : ExecutionStatus
|
||||
scheme_ref : SchemeRef
|
||||
summary : ExecutionErrorSummary
|
||||
diagnostics : list<DiagnosticEntry>
|
||||
}
|
||||
```
|
||||
|
||||
`PEL/1-CORE` defines the following shared enums:
|
||||
|
||||
```text
|
||||
ExecutionStatus {
|
||||
OK = 0
|
||||
SCHEME_UNSUPPORTED= 1
|
||||
INVALID_PROGRAM = 2
|
||||
INVALID_INPUTS = 3
|
||||
RUNTIME_FAILED = 4
|
||||
}
|
||||
|
||||
ExecutionErrorKind {
|
||||
NONE = 0
|
||||
SCHEME = 1
|
||||
PROGRAM = 2
|
||||
INPUTS = 3
|
||||
RUNTIME = 4
|
||||
}
|
||||
```
|
||||
|
||||
For **this scheme**:
|
||||
|
||||
* `Exec_DAG` uses only the following `ExecutionStatus` values:
|
||||
|
||||
```text
|
||||
OK
|
||||
INVALID_PROGRAM
|
||||
INVALID_INPUTS
|
||||
RUNTIME_FAILED
|
||||
```
|
||||
|
||||
(`SCHEME_UNSUPPORTED` is never produced by `Exec_DAG`; surfaces like `PEL/1-SURF` handle that before calling the scheme.)
|
||||
|
||||
* It uses only the following `ExecutionErrorKind` values:
|
||||
|
||||
```text
|
||||
NONE
|
||||
PROGRAM
|
||||
INPUTS
|
||||
RUNTIME
|
||||
```
|
||||
|
||||
The status ↔ kind mapping for this scheme is:
|
||||
|
||||
```text
|
||||
status = OK -> summary.kind = NONE
|
||||
status = INVALID_PROGRAM -> summary.kind = PROGRAM
|
||||
status = INVALID_INPUTS -> summary.kind = INPUTS
|
||||
status = RUNTIME_FAILED -> summary.kind = RUNTIME
|
||||
```
|
||||
|
||||
`summary.status_code` is scheme-defined but MUST be deterministic and respect:
|
||||
|
||||
* `status = OK` → `status_code = 0`
|
||||
* `status = INVALID_PROGRAM` → `status_code = 2` (canonical core code)
|
||||
* `status = INVALID_INPUTS` → `status_code = 3` (canonical core code)
|
||||
* `status = RUNTIME_FAILED` → `status_code` MUST be non-zero and MUST NOT be `2` or `3`
|
||||
(operation/scheme–defined runtime code).
|
||||
|
||||
Exact non-zero runtime codes come from operation registries and/or a future error code profile; this spec only constrains ranges and mapping to `ExecutionStatus` / `ExecutionErrorKind`.
|
||||
|
||||
---
|
||||
|
||||
## 1. Purpose & Non-Goals
|
||||
|
||||
### 1.1 Purpose
|
||||
|
||||
`PEL/PROGRAM-DAG/1` defines a **concrete PEL scheme** where:
|
||||
|
||||
* Programs are **acyclic computation graphs** (DAGs) of operations (**Nodes**).
|
||||
|
||||
* Nodes read from:
|
||||
|
||||
* **external inputs** (by index into the `inputs` list given to `Exec_DAG`), and
|
||||
* **outputs of other Nodes** (by `NodeId` + `output_index`).
|
||||
|
||||
* Programs designate **root outputs** as the scheme-level outputs.
|
||||
|
||||
This profile provides:
|
||||
|
||||
1. A precise **program value model**: `Program`, `Node`, `DagInput`, `RootRef`.
|
||||
2. **Structural validity** rules for such programs.
|
||||
3. A **canonical topological ordering** for deterministic evaluation.
|
||||
4. A binding of `PEL/1-CORE`’s `Exec_s` to a specific function:
|
||||
|
||||
```text
|
||||
Exec_DAG :
|
||||
(program: Artifact, inputs: list<Artifact>, params: optional Artifact)
|
||||
-> (outputs: list<Artifact>, result: ExecutionResultValue)
|
||||
```
|
||||
|
||||
`Exec_DAG` is pure and store-neutral; store-backed execution is handled by `PEL/1-SURF`.
|
||||
|
||||
### 1.2 Non-Goals
|
||||
|
||||
This scheme does **not** define:
|
||||
|
||||
* Graph/provenance edges (`TGK/1-CORE`).
|
||||
* Store semantics (`ASL/1-STORE`) or surfaces (`PEL/1-SURF`).
|
||||
* Concrete binary layouts (`ENC/PEL-PROGRAM-DAG/1`).
|
||||
* Trace artifact formats (`PEL/TRACE-DAG/1`).
|
||||
* Operation registries (`OPREG/PEL1-KERNEL` / extensions) or specific operation semantics.
|
||||
|
||||
Those are separate profiles layered on top of this scheme.
|
||||
|
||||
---
|
||||
|
||||
## 2. Core Model
|
||||
|
||||
### 2.1 OperationId
|
||||
|
||||
Operations are identified by a logical `OperationId`:
|
||||
|
||||
```text
|
||||
OperationId {
|
||||
name: String // logical text identifier
|
||||
version: uint32 // monotonic per name
|
||||
}
|
||||
```
|
||||
|
||||
* `String` here is a **logical** UTF-8 string; its concrete encoding into bytes is defined by
|
||||
`ENC/PEL-PROGRAM-DAG/1`.
|
||||
* For a given `(name, version)` **within a given operation registry**, semantics MUST be immutable once published. Any semantic change MUST be expressed as a new `version`.
|
||||
|
||||
At this scheme level, `OperationId` is opaque. A registry profile (e.g. `OPREG/PEL1-KERNEL`) defines a function:
|
||||
|
||||
```text
|
||||
OpSemantics(name, version) :
|
||||
(inputs: list<Artifact>, params: ParamsValue)
|
||||
-> Ok(list<Artifact>) | Err(status_code: uint32, diagnostics: list<DiagnosticEntry>)
|
||||
```
|
||||
|
||||
### 2.2 Params
|
||||
|
||||
Each `Node` carries **params** as an opaque parameter blob:
|
||||
|
||||
```text
|
||||
ParamsBytes = OctetString // raw bytes in the Program encoding
|
||||
ParamsValue = scheme-defined structured value
|
||||
```
|
||||
|
||||
Requirements:
|
||||
|
||||
* For each operation `(name, version)`:
|
||||
|
||||
* There MUST exist a well-defined abstract parameter model (`ParamsValue`).
|
||||
* There MUST be exactly one canonical encode/decode between `ParamsValue` and `ParamsBytes`.
|
||||
|
||||
* All conformant implementations of that operation MUST:
|
||||
|
||||
* decode the same `ParamsBytes` into the same `ParamsValue`, or
|
||||
* deterministically signal a decode failure.
|
||||
|
||||
**Static vs dynamic errors (guidance):**
|
||||
|
||||
* **Static param errors** (invalid structure, missing mandatory fields, invalid enums, out-of-range constants)
|
||||
SHOULD be treated as `INVALID_PROGRAM`.
|
||||
* **Dynamic errors** that depend on runtime inputs (e.g. “division by zero” because an input argument is zero, even though the param is syntactically valid) MUST be treated as `RUNTIME_FAILED` and surfaced via `status_code` and `diagnostics`.
|
||||
|
||||
This spec requires determinism and the status mapping (§0); it only gives guidance on where to draw the static/dynamic line. Parameter profiles MAY formalize this split more strictly.
|
||||
|
||||
The concrete placement of `ParamsBytes` (embedded in the Program vs separate Artifacts referenced from the Program) is defined by `ENC/PEL-PROGRAM-DAG/1`.
|
||||
|
||||
### 2.3 NodeId
|
||||
|
||||
```text
|
||||
NodeId = uint32
|
||||
```
|
||||
|
||||
Constraints:
|
||||
|
||||
* `NodeId` MUST be unique within a single `Program`.
|
||||
* When ordering Nodes, `NodeId` is compared as an unsigned integer (`0 < 1 < 2 < … < 2^32 − 1`).
|
||||
|
||||
### 2.4 DAG Inputs and Roots
|
||||
|
||||
Logical input references inside the Program:
|
||||
|
||||
```text
|
||||
DagInputExternal {
|
||||
input_index: uint32 // 0-based index into Exec_DAG.inputs
|
||||
}
|
||||
|
||||
DagInputNode {
|
||||
node_id: NodeId // must exist in Program.nodes
|
||||
output_index: uint32 // 0-based index into that Node's outputs
|
||||
}
|
||||
|
||||
DagInput =
|
||||
DagInputExternal
|
||||
| DagInputNode
|
||||
```
|
||||
|
||||
Scheme outputs (what `Exec_DAG` returns as `outputs`) are designated by:
|
||||
|
||||
```text
|
||||
RootRef {
|
||||
node_id: NodeId
|
||||
output_index: uint32
|
||||
}
|
||||
```
|
||||
|
||||
`RootRef` is interpreted like `DagInputNode`, but only in the final output selection step.
|
||||
|
||||
### 2.5 Node
|
||||
|
||||
A **Node** is a single operation application:
|
||||
|
||||
```text
|
||||
Node {
|
||||
id: NodeId
|
||||
op: OperationId
|
||||
inputs: list<DagInput>
|
||||
params: ParamsBytes
|
||||
}
|
||||
```
|
||||
|
||||
Constraints:
|
||||
|
||||
* `id` MUST be unique within the Program.
|
||||
* `inputs` MAY be empty (nullary operations).
|
||||
* All `DagInputNode.node_id` MUST refer to some `Node.id` in `Program.nodes`.
|
||||
|
||||
Semantics:
|
||||
|
||||
* When evaluated, the Node:
|
||||
|
||||
* resolves each `DagInput` to an input `Artifact`,
|
||||
* decodes `params` into a `ParamsValue` according to `op`,
|
||||
* applies the operation’s pure function to the input Artifacts and decoded params,
|
||||
* yields zero or more output Artifacts.
|
||||
|
||||
The number and meaning of outputs per operation are defined in the operation registry, not here.
|
||||
|
||||
### 2.6 Program
|
||||
|
||||
A **Program** is an acyclic graph:
|
||||
|
||||
```text
|
||||
Program {
|
||||
nodes: list<Node>
|
||||
roots: list<RootRef>
|
||||
}
|
||||
```
|
||||
|
||||
Constraints (structural validity is detailed in §3):
|
||||
|
||||
* All `Node.id` are unique.
|
||||
* All `DagInputNode.node_id` and `RootRef.node_id` refer to some Node in `nodes`.
|
||||
* The dependency graph induced by `DagInputNode` is a DAG (no cycles).
|
||||
|
||||
### 2.7 Program Artifact and TypeTag
|
||||
|
||||
At the ASL/1 layer:
|
||||
|
||||
* A **Program Artifact** is an `Artifact` such that:
|
||||
|
||||
* `type_tag = TYPE_TAG_PEL_PROGRAM_DAG_1` (symbolic constant), and
|
||||
* `bytes` encode exactly one `Program` value under `ENC/PEL-PROGRAM-DAG/1`.
|
||||
|
||||
`ENC/PEL-PROGRAM-DAG/1` MUST:
|
||||
|
||||
* assign a concrete numeric `tag_id` for `TYPE_TAG_PEL_PROGRAM_DAG_1`,
|
||||
* define an injective, deterministic, streaming-friendly encoding for `Program`,
|
||||
* ensure that all conformant engines decode/encode Programs identically.
|
||||
|
||||
This scheme assumes such an encoding exists and is canonical; it does not define the layout itself.
|
||||
|
||||
---
|
||||
|
||||
## 3. Structural Validity
|
||||
|
||||
A `Program` is **structurally valid** for this scheme if and only if all of the following hold:
|
||||
|
||||
1. **Unique NodeIds**
|
||||
|
||||
* For all `Node A`, `Node B` in `nodes`:
|
||||
|
||||
```text
|
||||
A.id == B.id ⇒ A and B are the same Node
|
||||
```
|
||||
|
||||
2. **Node references are in range**
|
||||
|
||||
* For every `DagInputNode{ node_id, ... }` in any `Node.inputs`:
|
||||
|
||||
* There exists a `Node` in `nodes` with `id = node_id`.
|
||||
|
||||
3. **Roots are in range**
|
||||
|
||||
* For every `RootRef{ node_id, ... }` in `roots`:
|
||||
|
||||
* There exists a `Node` in `nodes` with `id = node_id`.
|
||||
|
||||
4. **Acyclic dependency graph**
|
||||
|
||||
* Define a directed graph `G`:
|
||||
|
||||
* vertices: all `NodeId` values in `nodes`,
|
||||
* edge from `N.id` to `M.id` if `N.inputs` contains `DagInputNode{ node_id = M.id, ... }`.
|
||||
|
||||
* `G` MUST be acyclic (a DAG).
|
||||
|
||||
* Equivalently, there exists at least one topological ordering of Nodes where all dependencies of a Node appear before it.
|
||||
|
||||
5. **OperationId syntax is well-formed**
|
||||
|
||||
* Each `Node.op` is syntactically well-formed as:
|
||||
|
||||
* a valid `name` string (logical UTF-8 as per `ENC/PEL-PROGRAM-DAG/1`), and
|
||||
* a `uint32` `version`.
|
||||
|
||||
* Whether `(name, version)` is defined in the operation registry is an **execution-time** concern (§5.3).
|
||||
|
||||
6. **Parameter profile is available for each Node**
|
||||
|
||||
* For every `Node` in `nodes`:
|
||||
|
||||
* The active operation/parameter registry (e.g. `OPREG/PEL1-KERNEL` + parameter profiles) **MUST** provide a parameter-decoding function for that Node’s `OperationId`.
|
||||
|
||||
### 3.1 Parameter decoding and INVALID_PROGRAM
|
||||
|
||||
Program validity depends both on graph structure and on **decodability** of Node params under the chosen operation registry.
|
||||
|
||||
Given:
|
||||
|
||||
* a `Program` value,
|
||||
* an operation registry for this scheme, and
|
||||
* a set of parameter profiles,
|
||||
|
||||
validation MUST include parameter decoding for every Node:
|
||||
|
||||
1. For each `Node` in `Program.nodes`:
|
||||
|
||||
* Let `op` be its `OperationId`.
|
||||
* Let `params_bytes` be its `ParamsBytes`.
|
||||
* Let `decode_params_op` be the param-decoding function associated with `op`.
|
||||
|
||||
2. The engine MUST conceptually invoke `decode_params_op(params_bytes)` during Program validation.
|
||||
|
||||
3. If decoding fails for any Node (including any length, range, or structural violations defined by `decode_params_op`):
|
||||
|
||||
* the Program MUST be classified as structurally invalid for this scheme, and
|
||||
* any execution attempt MUST yield `status = INVALID_PROGRAM` (independent of the `inputs`).
|
||||
|
||||
Implementations MAY:
|
||||
|
||||
* eagerly validate all params before any node evaluation, or
|
||||
* lazily decode on first use of a Node’s params,
|
||||
|
||||
as long as the **observable semantics** is:
|
||||
|
||||
> For a fixed `program` Artifact, either all Node params are decodable (and execution can proceed), or every call to `Exec_DAG` on that `program` yields `status = INVALID_PROGRAM`, regardless of `inputs` and `params`.
|
||||
|
||||
A Program Artifact whose `bytes` cannot be decoded as a `Program` under `ENC/PEL-PROGRAM-DAG/1` is treated as “not a Program” and MUST also produce `status = INVALID_PROGRAM`.
|
||||
|
||||
---
|
||||
|
||||
## 4. Canonical Topological Order
|
||||
|
||||
### 4.1 Definition
|
||||
|
||||
Given a structurally valid Program:
|
||||
|
||||
1. Construct the dependency graph `G` as in §3.4.
|
||||
2. While unplaced Nodes remain:
|
||||
|
||||
* Let `C` be the set of Nodes whose dependencies are already in the order (i.e., all `DagInputNode` target `NodeId`s are in the placed set).
|
||||
* From `C`, choose the Node with smallest `NodeId` (numeric ascending).
|
||||
* Append that Node to the canonical order.
|
||||
* Mark it as placed, and iterate.
|
||||
|
||||
The resulting sequence of Nodes is the **canonical topological order** and is unique given the Program.
|
||||
|
||||
### 4.2 Use
|
||||
|
||||
All references in this spec to:
|
||||
|
||||
* “Nodes in canonical order”, or
|
||||
* “evaluating Nodes in order”,
|
||||
|
||||
refer to this ordering.
|
||||
|
||||
Implementations MAY evaluate Nodes in parallel or with different internal scheduling, but the **observable behavior** (outputs and `ExecutionResultValue`) MUST be equivalent to evaluating Nodes **sequentially** in canonical topological order.
|
||||
|
||||
---
|
||||
|
||||
## 5. Scheme Binding to PEL/1-CORE
|
||||
|
||||
### 5.1 Scheme identity
|
||||
|
||||
This scheme is identified by a `SchemeRef` pointing to a **scheme descriptor Artifact**, denoted:
|
||||
|
||||
```text
|
||||
SchemeRef_DAG_1 : SchemeRef
|
||||
```
|
||||
|
||||
The descriptor Artifact (its `TypeTag`, bytes, and meaning) is defined in a separate descriptor document (e.g. `PEL/PROGRAM-DAG-DESC/1`). All conformant engines MUST agree on:
|
||||
|
||||
* the descriptor Artifact bytes, and
|
||||
* the resulting `Reference` (`SchemeRef_DAG_1`).
|
||||
|
||||
In PEL/1-CORE terms, this scheme binds:
|
||||
|
||||
```text
|
||||
SchemeRef = SchemeRef_DAG_1
|
||||
Exec_s = Exec_DAG
|
||||
```
|
||||
|
||||
### 5.2 Exec_DAG signature
|
||||
|
||||
For this scheme, `Exec_s` is instantiated as:
|
||||
|
||||
```text
|
||||
Exec_DAG(
|
||||
program: Artifact, // Program Artifact
|
||||
inputs: list<Artifact>, // external input Artifacts
|
||||
params: optional Artifact // optional global parameters
|
||||
) -> (outputs: list<Artifact>, result: ExecutionResultValue)
|
||||
```
|
||||
|
||||
Interpretation:
|
||||
|
||||
* `program` MUST be an Artifact with `type_tag = TYPE_TAG_PEL_PROGRAM_DAG_1` and decodable as a `Program`. Otherwise, `status = INVALID_PROGRAM`.
|
||||
* `inputs` is the list of external inputs referenced by `DagInputExternal.input_index`.
|
||||
* `params`, if present, is a scheme-specific Artifact that MAY:
|
||||
|
||||
* be interpreted as global configuration, or
|
||||
* be ignored,
|
||||
|
||||
depending on the scheme descriptor.
|
||||
|
||||
The scheme MUST be deterministic:
|
||||
|
||||
> For fixed `program.bytes`, `inputs` list, and `params.bytes`, all conformant implementations of `Exec_DAG` MUST produce identical `outputs` and `ExecutionResultValue`.
|
||||
|
||||
### 5.3 High-level semantics of Exec_DAG
|
||||
|
||||
`Exec_DAG` MUST proceed conceptually in the following steps:
|
||||
|
||||
1. **Decode and validate Program**
|
||||
|
||||
* Attempt to decode `program.bytes` as a `Program` under `ENC/PEL-PROGRAM-DAG/1`.
|
||||
|
||||
* If decoding fails:
|
||||
|
||||
* `outputs = []`.
|
||||
|
||||
* `result`:
|
||||
|
||||
```text
|
||||
pel1_version = 1
|
||||
status = INVALID_PROGRAM
|
||||
scheme_ref = SchemeRef_DAG_1
|
||||
summary.kind = PROGRAM
|
||||
summary.status_code = 2
|
||||
diagnostics = [ deterministic diagnostic entries ]
|
||||
```
|
||||
|
||||
* Return.
|
||||
|
||||
* If decoding succeeds but the Program violates any structural validity rule (§3):
|
||||
|
||||
* Same as above: `status = INVALID_PROGRAM`.
|
||||
|
||||
2. **Resolve operation semantics and validate params**
|
||||
|
||||
* For each `Node.op` in `Program.nodes`, resolve `(Node.op.name, Node.op.version)` against the operation registry for this scheme.
|
||||
|
||||
* If any `OperationId` used in the Program is not defined:
|
||||
|
||||
* Treat the Program as invalid:
|
||||
|
||||
* `outputs = []`.
|
||||
* `result` as `INVALID_PROGRAM` (status_code = 2) with diagnostics indicating unknown operations.
|
||||
|
||||
* Return.
|
||||
|
||||
* For each Node:
|
||||
|
||||
* Decode its `ParamsBytes` using the parameter profile for its `OperationId`.
|
||||
|
||||
* If decoding fails:
|
||||
|
||||
* Treat as `INVALID_PROGRAM`:
|
||||
|
||||
* `outputs = []`.
|
||||
* `result` as `INVALID_PROGRAM` (status_code = 2) with appropriate diagnostics.
|
||||
|
||||
* Return.
|
||||
|
||||
* Otherwise, conceptually store the decoded `ParamsValue` for use in evaluation.
|
||||
|
||||
3. **Evaluate Nodes in canonical order**
|
||||
|
||||
* Compute the canonical topological order (§4) of Nodes.
|
||||
|
||||
* Maintain:
|
||||
|
||||
```text
|
||||
node_outputs : NodeId -> list<Artifact>
|
||||
```
|
||||
|
||||
* For each Node `N` in canonical order:
|
||||
|
||||
1. **Resolve Node inputs**
|
||||
|
||||
* For each `DagInput` in `N.inputs`:
|
||||
|
||||
* If `DagInputExternal{ input_index }`:
|
||||
|
||||
* If `input_index >= len(inputs)`:
|
||||
|
||||
* This is an **input error**:
|
||||
|
||||
* `outputs = []`.
|
||||
* `result`:
|
||||
|
||||
```text
|
||||
pel1_version = 1
|
||||
status = INVALID_INPUTS
|
||||
scheme_ref = SchemeRef_DAG_1
|
||||
summary.kind = INPUTS
|
||||
summary.status_code = 3
|
||||
diagnostics = [ deterministic diagnostic for missing input_index ]
|
||||
```
|
||||
|
||||
* Return.
|
||||
|
||||
* Otherwise use `inputs[input_index]` as that input Artifact.
|
||||
|
||||
* If `DagInputNode{ node_id, output_index }`:
|
||||
|
||||
* Let `outs = node_outputs[node_id]` (must exist because canonical order ensures dependencies are evaluated first).
|
||||
|
||||
* If `output_index >= len(outs)`:
|
||||
|
||||
* This is a **program error** (operation output arity mismatch):
|
||||
|
||||
* `outputs = []`.
|
||||
* `result` as `INVALID_PROGRAM` (status_code = 2) with suitable diagnostics.
|
||||
|
||||
* Return.
|
||||
|
||||
* Collect the resolved input Artifacts into `node_input_artifacts`.
|
||||
|
||||
2. **Apply operation semantics**
|
||||
|
||||
* Let `params_value` be the decoded `ParamsValue` for Node `N`.
|
||||
|
||||
* Invoke the operation semantics:
|
||||
|
||||
```text
|
||||
Op(N.op)(
|
||||
node_input_artifacts: list<Artifact>,
|
||||
params_value: ParamsValue
|
||||
) -> Ok(list<Artifact>) | Err(status_code: uint32, diagnostics: list<DiagnosticEntry>)
|
||||
```
|
||||
|
||||
* Implementation requirements:
|
||||
|
||||
* `Op(N.op)` MUST be pure and deterministic.
|
||||
* It MUST NOT perform I/O, consult time, or depend on mutable global state.
|
||||
|
||||
* If `Ok(outputs_for_node)`:
|
||||
|
||||
* Set `node_outputs[N.id] = outputs_for_node`.
|
||||
|
||||
* If `Err(status_code, diag)`:
|
||||
|
||||
* This is a **runtime failure**; `Exec_DAG` MUST:
|
||||
|
||||
* Set `outputs = []` (this scheme is **fail-fast**; it does not define partial outputs).
|
||||
* Set `result`:
|
||||
|
||||
```text
|
||||
pel1_version = 1
|
||||
status = RUNTIME_FAILED
|
||||
scheme_ref = SchemeRef_DAG_1
|
||||
summary.kind = RUNTIME
|
||||
summary.status_code = status_code // non-zero, operation-defined
|
||||
diagnostics = diag // or diag plus additional scheme diagnostics
|
||||
```
|
||||
|
||||
* No further Nodes are evaluated.
|
||||
|
||||
* Return.
|
||||
|
||||
4. **Compute scheme outputs (success case)**
|
||||
|
||||
* If all Nodes have been evaluated successfully (no early return):
|
||||
|
||||
* Initialise `outputs = []`.
|
||||
|
||||
* For each `RootRef` in `Program.roots` (in order):
|
||||
|
||||
* Let `outs = node_outputs[root.node_id]`.
|
||||
|
||||
* If `root.output_index >= len(outs)`:
|
||||
|
||||
* Treat as `INVALID_PROGRAM`:
|
||||
|
||||
* `outputs = []`.
|
||||
* `result` as in step 1 with suitable diagnostics.
|
||||
|
||||
* Return.
|
||||
|
||||
* Otherwise, append `outs[root.output_index]` to `outputs`.
|
||||
|
||||
* When all roots resolve successfully:
|
||||
|
||||
* `outputs` is the list of root Artifacts in `Program.roots` order.
|
||||
* `result`:
|
||||
|
||||
```text
|
||||
pel1_version = 1
|
||||
status = OK
|
||||
scheme_ref = SchemeRef_DAG_1
|
||||
summary.kind = NONE
|
||||
summary.status_code = 0
|
||||
diagnostics = []
|
||||
```
|
||||
|
||||
5. **Return**
|
||||
|
||||
* Return `(outputs, result)`.
|
||||
|
||||
### 5.4 Determinism guarantees
|
||||
|
||||
For fixed:
|
||||
|
||||
* `program.bytes`,
|
||||
* `inputs` list (sequence and values),
|
||||
* `params` presence and `params.bytes`,
|
||||
|
||||
and given:
|
||||
|
||||
* a fixed canonical encoding profile (`ENC/PEL-PROGRAM-DAG/1`),
|
||||
* a fixed operation registry (`OPREG/PEL1-KERNEL` + extension registries) for this scheme,
|
||||
|
||||
all conformant implementations of `Exec_DAG` MUST produce:
|
||||
|
||||
* identical logical `outputs` (as `Artifact` values), and
|
||||
* identical `ExecutionResultValue` payloads.
|
||||
|
||||
No implementation-specific identifiers, timestamps, or environment details may appear in `result` or in the contents of `outputs`.
|
||||
|
||||
---
|
||||
|
||||
## 6. Interaction with PEL/1-SURF (Informative)
|
||||
|
||||
When this scheme is used with `PEL/1-SURF`:
|
||||
|
||||
* The surface layer provides `program_ref`, `input_refs`, `params_ref` and a StoreInstance.
|
||||
* It resolves those references to `program`, `inputs`, `params` via `ASL/1-STORE` `get`.
|
||||
* It invokes `Exec_DAG(program, inputs, params)` as defined here.
|
||||
* It persists:
|
||||
|
||||
* each element of `outputs` via `put`, producing `output_refs`, and
|
||||
* a surface ExecutionResult artifact containing `ExecutionResultValue` plus context.
|
||||
|
||||
Store-resolution failures (`ERR_NOT_FOUND`, `ERR_INTEGRITY`, `ERR_UNSUPPORTED`) are handled by `PEL/1-SURF`, which maps them to `INVALID_PROGRAM` / `INVALID_INPUTS` with `store_failure` metadata, **without** calling `Exec_DAG`.
|
||||
|
||||
`Exec_DAG` only sees Programs and input/param Artifacts that have successfully been loaded from the store.
|
||||
|
||||
---
|
||||
|
||||
## 7. Interaction with Trace Profiles (Informative)
|
||||
|
||||
A trace profile such as `PEL/TRACE-DAG/1` MAY:
|
||||
|
||||
* Capture per-node inputs, outputs, and error states.
|
||||
* Encode these in a `TraceValue` Artifact with its own `TypeTag`.
|
||||
* Specify that `Exec_DAG` (or the surface) produces a trace Artifact as one of the outputs, and that `PEL/1-SURF` exposes its `Reference` as `trace_ref` in surface results.
|
||||
|
||||
`PEL/PROGRAM-DAG/1` itself does not mandate traces; it only ensures evaluation order and deterministic behavior so that a trace profile can be layered cleanly.
|
||||
|
||||
---
|
||||
|
||||
## 8. Conformance
|
||||
|
||||
An implementation is **PEL/PROGRAM-DAG/1–conformant** if it:
|
||||
|
||||
1. **Program handling**
|
||||
|
||||
* Correctly decodes and encodes `Program` values according to this spec and `ENC/PEL-PROGRAM-DAG/1`.
|
||||
* Checks structural validity as in §3, including parameter decodability.
|
||||
* Treats structurally invalid or undecodable Programs as `INVALID_PROGRAM` in `Exec_DAG`.
|
||||
|
||||
2. **Scheme binding**
|
||||
|
||||
* Recognizes `SchemeRef_DAG_1` as the scheme identifier.
|
||||
* Implements `Exec_DAG` exactly as in §5 for this scheme.
|
||||
* Ensures that `result.scheme_ref = SchemeRef_DAG_1` and `result.pel1_version = 1`.
|
||||
|
||||
3. **Operation registry integration**
|
||||
|
||||
* Uses a registry for `(OperationId -> OpSemantics)` where:
|
||||
|
||||
* each `OpSemantics` is pure and deterministic,
|
||||
* param encodings are canonical and deterministic,
|
||||
* runtime errors are mapped to non-zero `status_code`s and deterministic diagnostics.
|
||||
|
||||
* Treats unknown `OperationId` values in a Program as `INVALID_PROGRAM`.
|
||||
|
||||
4. **Status mapping**
|
||||
|
||||
* Produces `ExecutionResultValue.status` only from:
|
||||
|
||||
* `OK`,
|
||||
* `INVALID_PROGRAM`,
|
||||
* `INVALID_INPUTS`,
|
||||
* `RUNTIME_FAILED`.
|
||||
|
||||
* Ensures `summary.kind` and `summary.status_code` follow the mapping in §0 and §5.3.
|
||||
|
||||
5. **Determinism and purity**
|
||||
|
||||
* Satisfies PEL/1-CORE’s determinism contract:
|
||||
|
||||
* For fixed inputs, all conformant implementations produce identical `outputs` and `ExecutionResultValue`.
|
||||
|
||||
* Does not consult time, randomness, external I/O, or mutable global state as part of `Exec_DAG` semantics.
|
||||
|
||||
6. **Layering**
|
||||
|
||||
* Does not depend on any particular store, graph, certification, or overlay behavior.
|
||||
* Treats store resolution, provenance, certification, and overlays as responsibilities of other specs (`PEL/1-SURF`, `TGK/1-CORE`, `CIL/1`, `FER/1`, `FCT/1`).
|
||||
|
||||
---
|
||||
|
||||
**End of `PEL/PROGRAM-DAG/1 v0.3.1 — DAG Program Scheme for PEL`**
|
||||
|
||||
---
|
||||
|
||||
## Document History
|
||||
|
||||
* **0.3.1 (2025-11-16):** Registered as Tier-1 spec and aligned to the Amduat 2.0 substrate baseline.
|
||||
781
tier1/pel-program-dag-desc-1.md
Normal file
781
tier1/pel-program-dag-desc-1.md
Normal file
|
|
@ -0,0 +1,781 @@
|
|||
# PEL/PROGRAM-DAG-DESC/1 — Scheme Descriptor for DAG Program Scheme
|
||||
|
||||
Status: Approved
|
||||
Owner: Niklas Rydberg
|
||||
Version: 0.1.6
|
||||
SoT: Yes
|
||||
Last Updated: 2025-11-16
|
||||
Linked Phase Pack: N/A
|
||||
Tags: [composition, registry]
|
||||
|
||||
<!-- Source: /amduat/docs/new/pel-program-dag-desc.md | Canonical: /amduat/tier1/pel-program-dag-desc-1.md -->
|
||||
|
||||
**Document ID:** `PEL/PROGRAM-DAG-DESC/1`
|
||||
**Layer:** L1 Scheme Descriptor (binds PEL scheme to ASL values)
|
||||
|
||||
**Depends on (normative):**
|
||||
|
||||
* `ASL/1-CORE v0.4.x` — Artifact substrate (`Artifact`, `TypeTag`, `Reference`, `EncodingProfileId`)
|
||||
* `ENC/ASL1-CORE v1.0.x` — canonical encoding profile (`ASL_ENC_CORE_V1`)
|
||||
* `PEL/1-CORE v0.3.x` — primitive execution layer (schemes and `Exec_s`)
|
||||
* `PEL/PROGRAM-DAG/1 v0.3.x` — DAG program scheme (`Program`, `Node`, `Exec_DAG`, symbolic `SchemeRef_DAG_1`)
|
||||
* `ENC/PEL-PROGRAM-DAG/1 v0.2.x` — canonical encoding for DAG programs (Program Artifacts, profile ID `PEL_ENC_PROGRAM_DAG_V1`)
|
||||
|
||||
**References (informative):**
|
||||
|
||||
* `HASH/ASL1 v0.2.x` — ASL1 hash family (`HashId` assignments, `HASH-ASL1-256`)
|
||||
* `SUBSTRATE/STACK-OVERVIEW v0.3.x` — stack layering and kernel invariants
|
||||
* `ENC/PEL-TRACE-DAG/1 v0.1.x` — canonical encoding for DAG traces (Trace Artifacts)
|
||||
* `OPREG/PEL1-KERNEL` and related param profiles — operation registry for DAG ops (context only)
|
||||
|
||||
© 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
|
||||
|
||||
`PEL/PROGRAM-DAG/1` defines the **DAG program scheme** for PEL/1-CORE and refers to its scheme identifier symbolically as `SchemeRef_DAG_1`.
|
||||
|
||||
`PEL/PROGRAM-DAG-DESC/1` defines:
|
||||
|
||||
* the **logical descriptor value** for the DAG scheme,
|
||||
* its realization as a concrete **ASL/1 Artifact** (the *descriptor Artifact*), and
|
||||
* how engines derive and recognize `SchemeRef_DAG_1` as the scheme’s `SchemeRef`.
|
||||
|
||||
In particular, this document:
|
||||
|
||||
* binds the DAG scheme semantics (`Exec_DAG`) to a specific `SchemeRef` value;
|
||||
* specifies the descriptor’s **TypeTag** and internal structure;
|
||||
* specifies how `SchemeRef_DAG_1` is derived from the descriptor Artifact under `ASL_ENC_CORE_V1` and a chosen hash algorithm; and
|
||||
* fixes a **canonical** `SchemeRef_DAG_1` for the Amduat 2.0 baseline profile using `HASH-ASL1-256` (`HashId = 0x0001`),
|
||||
|
||||
without introducing dependencies on stores, TGK, certificates, facts, or overlays.
|
||||
|
||||
---
|
||||
|
||||
## 1. Scope & Layering
|
||||
|
||||
### 1.1 Purpose
|
||||
|
||||
This specification defines:
|
||||
|
||||
* The **logical structure** of the DAG scheme descriptor value (`DagSchemeDescriptor`).
|
||||
|
||||
* The **descriptor Artifact** that carries this value:
|
||||
|
||||
* its `type_tag` (a “PEL scheme descriptor” `TypeTag`), and
|
||||
* its canonical `bytes` layout.
|
||||
|
||||
* The **derivation** of `SchemeRef_DAG_1` as a `Reference` to that descriptor Artifact.
|
||||
|
||||
* The **binding** between `SchemeRef_DAG_1` and the DAG scheme defined in `PEL/PROGRAM-DAG/1`.
|
||||
|
||||
It does **not** redefine:
|
||||
|
||||
* DAG program semantics or structure (`Program`, `Node`, `Exec_DAG`),
|
||||
* Program or trace encodings (`ENC/PEL-PROGRAM-DAG/1`, `ENC/PEL-TRACE-DAG/1`),
|
||||
* hash algorithms or `HashId` (`HASH/ASL1`),
|
||||
* store, graph, certification, or provenance behavior.
|
||||
|
||||
### 1.2 Layering constraints
|
||||
|
||||
In line with `SUBSTRATE/STACK-OVERVIEW`:
|
||||
|
||||
* `PEL/PROGRAM-DAG-DESC/1` is a **scheme descriptor**:
|
||||
|
||||
* it binds a PEL scheme (`PEL/PROGRAM-DAG/1`) to a specific ASL/1 `Reference`; and
|
||||
* it describes how engines recognize and interpret that scheme.
|
||||
|
||||
* It MUST NOT introduce dependencies on:
|
||||
|
||||
* stores (`ASL/1-STORE`),
|
||||
* graph kernels or graph stores (`TGK/1-CORE`, `TGK/STORE/1`),
|
||||
* certification, evidence, facts, or overlays (`CIL/1`, `FER/1`, `FCT/1`, `OI/1`).
|
||||
|
||||
* It MAY refer informatively to:
|
||||
|
||||
* canonical trace encodings (`ENC/PEL-TRACE-DAG/1`),
|
||||
* operation registries and parameter profiles (`OPREG/PEL1-KERNEL`, etc.),
|
||||
|
||||
but MUST NOT depend on them for its core semantics.
|
||||
|
||||
---
|
||||
|
||||
## 2. Dependencies, Terminology & Conventions
|
||||
|
||||
RFC 2119 terms (**MUST**, **SHOULD**, **MAY**, etc.) are normative.
|
||||
|
||||
### 2.1 From ASL/1-CORE
|
||||
|
||||
```text
|
||||
Artifact {
|
||||
bytes: OctetString
|
||||
type_tag: optional TypeTag
|
||||
}
|
||||
|
||||
TypeTag {
|
||||
tag_id: uint32
|
||||
}
|
||||
|
||||
Reference {
|
||||
hash_id: HashId
|
||||
digest: OctetString
|
||||
}
|
||||
|
||||
HashId = uint16
|
||||
EncodingProfileId = uint16
|
||||
```
|
||||
|
||||
This spec treats:
|
||||
|
||||
* `Artifact` as the unit of identity and content,
|
||||
* `TypeTag` as the typing hint for `Artifact.bytes`,
|
||||
* `Reference` as the content address for Artifacts, and
|
||||
* `EncodingProfileId` as the identifier of encoding profiles (e.g. `ASL_ENC_CORE_V1`, `PEL_ENC_PROGRAM_DAG_V1`).
|
||||
|
||||
### 2.2 From ENC/ASL1-CORE v1
|
||||
|
||||
`ENC/ASL1-CORE v1` defines:
|
||||
|
||||
* `ArtifactBytes = encode_artifact_core_v1(Artifact)` — canonical encoding for Artifacts.
|
||||
* `ReferenceBytes = encode_reference_core_v1(Reference)` — canonical encoding for References.
|
||||
|
||||
It also instantiates the generic ASL rule:
|
||||
|
||||
```text
|
||||
ArtifactBytes = encode_P(A)
|
||||
digest = H(ArtifactBytes)
|
||||
Reference = { hash_id = HID, digest = digest }
|
||||
```
|
||||
|
||||
for `P = ASL_ENC_CORE_V1` and any hash algorithm `H` with `HashId = HID`.
|
||||
|
||||
### 2.3 From PEL/1-CORE and PEL/PROGRAM-DAG/1
|
||||
|
||||
From `PEL/1-CORE`:
|
||||
|
||||
```text
|
||||
SchemeRef = Reference
|
||||
|
||||
Exec_s :
|
||||
(program: Artifact, inputs: list<Artifact>, params: optional Artifact)
|
||||
-> (outputs: list<Artifact>, result: ExecutionResultValue)
|
||||
```
|
||||
|
||||
From `PEL/PROGRAM-DAG/1`:
|
||||
|
||||
* The DAG scheme is a concrete scheme over PEL/1-CORE:
|
||||
|
||||
```text
|
||||
Exec_DAG :
|
||||
(program: Artifact, inputs: list<Artifact>, params: optional Artifact)
|
||||
-> (outputs: list<Artifact>, result: ExecutionResultValue)
|
||||
```
|
||||
|
||||
* This scheme is identified symbolically as `SchemeRef_DAG_1`, with:
|
||||
|
||||
```text
|
||||
SchemeRef = SchemeRef_DAG_1
|
||||
Exec_s = Exec_DAG
|
||||
```
|
||||
|
||||
`PEL/PROGRAM-DAG-DESC/1` makes this symbolic `SchemeRef_DAG_1` concrete.
|
||||
|
||||
### 2.4 Conventions
|
||||
|
||||
Unless stated otherwise:
|
||||
|
||||
* Integers:
|
||||
|
||||
* `u8` — 1 byte, unsigned.
|
||||
* `u16` — 2 bytes, unsigned, big-endian.
|
||||
* `u32` — 4 bytes, unsigned, big-endian.
|
||||
|
||||
* `Utf8String` is encoded as:
|
||||
|
||||
```text
|
||||
Utf8String =
|
||||
length (u32)
|
||||
bytes[0..length-1]
|
||||
```
|
||||
|
||||
where:
|
||||
|
||||
* `length` is the number of bytes,
|
||||
* `bytes` MUST be well-formed UTF-8,
|
||||
* there is no terminator or padding.
|
||||
|
||||
* Embedded `Reference` values use a length-prefixed wrapper over canonical `ReferenceBytes` from `ENC/ASL1-CORE v1`:
|
||||
|
||||
```text
|
||||
EncodedRef =
|
||||
ref_len (u32)
|
||||
ref_bytes (byte[0..ref_len-1]) // canonical ReferenceBytes
|
||||
```
|
||||
|
||||
where:
|
||||
|
||||
* `ref_bytes` MUST be the canonical `ReferenceBytes` for some `Reference` value under `ENC/ASL1-CORE v1`,
|
||||
* `ref_len` MUST be the exact length of `ref_bytes` (MUST be ≥ 2).
|
||||
|
||||
Decoders MUST:
|
||||
|
||||
* treat `ref_len < 2` as an encoding error, and
|
||||
* decode `ref_bytes` using `decode_reference_core_v1`. Any failure in that decoding (including, when `HASH/ASL1` is implemented, a digest-length mismatch for a known `hash_id`) MUST be treated as an encoding error for `DagSchemeDescriptorBytes`.
|
||||
|
||||
* Optional `Reference` fields use:
|
||||
|
||||
```text
|
||||
OptionalEncodedRef =
|
||||
has_ref (u8)
|
||||
[ EncodedRef ] // only if has_ref == 0x01
|
||||
```
|
||||
|
||||
with:
|
||||
|
||||
* `has_ref = 0x00` → no value present (no `EncodedRef` follows),
|
||||
* `has_ref = 0x01` → exactly one `EncodedRef` follows,
|
||||
* other `has_ref` values are encoding errors.
|
||||
|
||||
---
|
||||
|
||||
## 3. Descriptor Logical Model
|
||||
|
||||
### 3.1 DagSchemeDescriptor (logical)
|
||||
|
||||
At the logical level, the DAG scheme descriptor is modeled as:
|
||||
|
||||
```text
|
||||
DagSchemeDescriptor {
|
||||
pel1_version: uint16
|
||||
|
||||
scheme_name: String // logical identifier, e.g. "PEL/PROGRAM-DAG/1"
|
||||
|
||||
program_type_tag: TypeTag // TYPE_TAG_PEL_PROGRAM_DAG_1
|
||||
program_enc_profile: EncodingProfileId
|
||||
// PEL_ENC_PROGRAM_DAG_V1 (0x0101)
|
||||
|
||||
trace_profile_ref: optional Reference
|
||||
// to a trace-profile descriptor (e.g. PEL/TRACE-DAG-DESC/1)
|
||||
opreg_ref: optional Reference
|
||||
// to a canonical operation-registry descriptor (e.g. OPREG/PEL1-KERNEL)
|
||||
}
|
||||
```
|
||||
|
||||
This structure is **logical**; the descriptor’s concrete bytes are defined in §4.
|
||||
|
||||
The `program_type_tag` / `program_enc_profile` pair tells engines **how to interpret Program Artifacts** for this scheme:
|
||||
|
||||
* `program_type_tag` ⇒ which `TypeTag` marks an Artifact as a DAG Program for this scheme;
|
||||
* `program_enc_profile` ⇒ which Program encoding profile (specifically, `PEL_ENC_PROGRAM_DAG_V1` from `ENC/PEL-PROGRAM-DAG/1`) to use when decoding/encoding those Artifacts.
|
||||
|
||||
This pair is independent from the **ASL-level encoding profile** used for the descriptor Artifact itself, which is always `ASL_ENC_CORE_V1` when deriving `SchemeRef_DAG_1` (§5.2).
|
||||
|
||||
This document does not require engines to inspect all fields at runtime. In particular:
|
||||
|
||||
* engines that already know `SchemeRef_DAG_1`, `TYPE_TAG_PEL_PROGRAM_DAG_1`, and `PEL_ENC_PROGRAM_DAG_V1` MAY treat the descriptor as metadata; and
|
||||
* the canonical binding to `PEL/PROGRAM-DAG/1` is via `SchemeRef_DAG_1` and the `program_type_tag` / `program_enc_profile` pair, not via `scheme_name` or the optional references.
|
||||
|
||||
### 3.2 Field semantics & invariants
|
||||
|
||||
For the **Amduat 2.0 baseline DAG scheme descriptor** (the one used to define `SchemeRef_DAG_1`) the following invariants apply:
|
||||
|
||||
* `pel1_version`:
|
||||
|
||||
* MUST be `1`.
|
||||
* Indicates the descriptor is written against `PEL/1-CORE` version 1 semantics.
|
||||
* Future PEL versions MAY introduce new descriptor formats, but MUST NOT change the meaning of `pel1_version = 1`.
|
||||
|
||||
* `scheme_name`:
|
||||
|
||||
* MUST be the UTF-8 string `"PEL/PROGRAM-DAG/1"`, compared byte-for-byte and case-sensitively.
|
||||
* Serves as a human-readable identifier and sanity check.
|
||||
* Changing `scheme_name` (while keeping other fields identical) changes the descriptor value and therefore its `Reference`.
|
||||
|
||||
* `program_type_tag`:
|
||||
|
||||
* MUST equal the `TypeTag` used for DAG Program Artifacts, symbolically:
|
||||
|
||||
```text
|
||||
program_type_tag = TYPE_TAG_PEL_PROGRAM_DAG_1
|
||||
```
|
||||
|
||||
* The concrete numeric `tag_id` is assigned by the TypeTag registry and is not restated here.
|
||||
|
||||
* `program_enc_profile`:
|
||||
|
||||
* MUST be the `EncodingProfileId` of `ENC/PEL-PROGRAM-DAG/1`, symbolically:
|
||||
|
||||
```text
|
||||
program_enc_profile = PEL_ENC_PROGRAM_DAG_V1
|
||||
```
|
||||
|
||||
* In the current encoding profile, this is `0x0101`, but this spec treats it symbolically; the numeric value comes from the encoding profile registry.
|
||||
|
||||
* `trace_profile_ref`:
|
||||
|
||||
* Optionally points at a descriptor Artifact that defines a canonical trace profile for this scheme (e.g. a future `PEL/TRACE-DAG-DESC/1`).
|
||||
|
||||
* For the **canonical Amduat 2.0 baseline descriptor used to define `SchemeRef_DAG_1`**, this field is **absent**:
|
||||
|
||||
```text
|
||||
trace_profile_ref = None
|
||||
```
|
||||
|
||||
* Future companion descriptors MAY set this field, but those will not be the descriptor used for `SchemeRef_DAG_1`.
|
||||
|
||||
* `opreg_ref`:
|
||||
|
||||
* Optionally points at a descriptor Artifact for the canonical operation registry for this scheme (e.g. `OPREG/PEL1-KERNEL`).
|
||||
|
||||
* For the **canonical Amduat 2.0 baseline descriptor used to define `SchemeRef_DAG_1`**, this field is **absent**:
|
||||
|
||||
```text
|
||||
opreg_ref = None
|
||||
```
|
||||
|
||||
* As with `trace_profile_ref`, future descriptors MAY set this field, but those will define distinct `SchemeRef` values, not `SchemeRef_DAG_1`.
|
||||
|
||||
### 3.3 Canonical descriptor value for the DAG scheme
|
||||
|
||||
Let:
|
||||
|
||||
```text
|
||||
DagSchemeDescriptor_DAG_1 : DagSchemeDescriptor
|
||||
```
|
||||
|
||||
denote the unique logical descriptor value that satisfies:
|
||||
|
||||
```text
|
||||
DagSchemeDescriptor_DAG_1 {
|
||||
pel1_version = 1
|
||||
|
||||
scheme_name = "PEL/PROGRAM-DAG/1"
|
||||
|
||||
program_type_tag = TYPE_TAG_PEL_PROGRAM_DAG_1
|
||||
program_enc_profile = PEL_ENC_PROGRAM_DAG_V1
|
||||
|
||||
trace_profile_ref = None
|
||||
opreg_ref = None
|
||||
}
|
||||
```
|
||||
|
||||
All Amduat 2.0 baseline components MUST agree on this logical value as “the” DAG scheme descriptor for binding `PEL/PROGRAM-DAG/1` to a `SchemeRef`.
|
||||
|
||||
Any descriptor with different logical contents (including differing optional fields) describes either:
|
||||
|
||||
* a different scheme, or
|
||||
* a different profile or version of the DAG scheme,
|
||||
|
||||
and MUST NOT be used to derive `SchemeRef_DAG_1`.
|
||||
|
||||
Because the descriptor is carried in an ASL/1 Artifact and scheme references are content-addressed, any change to this descriptor (even in optional fields) yields a different `Reference`; `SchemeRef_DAG_1` is therefore permanently tied to exactly this v1 descriptor.
|
||||
|
||||
---
|
||||
|
||||
## 4. Descriptor Artifact & Encoding
|
||||
|
||||
### 4.1 Descriptor TypeTag
|
||||
|
||||
The DAG scheme descriptor is carried by an ASL/1 Artifact with a dedicated TypeTag:
|
||||
|
||||
```text
|
||||
TYPE_TAG_PEL_SCHEME_DESC_1 : TypeTag
|
||||
```
|
||||
|
||||
* `TYPE_TAG_PEL_SCHEME_DESC_1` is a symbolic constant for a `TypeTag.tag_id` assigned by the global `TypeTag` registry.
|
||||
* This `TypeTag` MUST be used for the DAG scheme descriptor Artifact defined in this document.
|
||||
* Other PEL scheme descriptors MAY reuse this `TypeTag` and the encoding in §4.2, but such reuse MUST be specified in their own descriptor documents.
|
||||
|
||||
The descriptor Artifact for the DAG scheme has the shape:
|
||||
|
||||
```text
|
||||
DagSchemeDescriptorArtifact_DAG_1 : Artifact {
|
||||
type_tag = TYPE_TAG_PEL_SCHEME_DESC_1
|
||||
bytes = DagSchemeDescriptorBytes_DAG_1
|
||||
}
|
||||
```
|
||||
|
||||
where `DagSchemeDescriptorBytes_DAG_1` is the canonical encoding of `DagSchemeDescriptor_DAG_1` defined in §4.2.
|
||||
|
||||
This Artifact itself is encoded to `ArtifactBytes` using `ASL_ENC_CORE_V1` when deriving `SchemeRef_DAG_1` (§5.2). That use of `ASL_ENC_CORE_V1` is **independent** of the `program_enc_profile` field, which is about how Program Artifacts are encoded.
|
||||
|
||||
### 4.2 Descriptor encoding layout
|
||||
|
||||
The descriptor value `DagSchemeDescriptor` is encoded into `DagSchemeDescriptorBytes` using a small, fixed layout over primitive types:
|
||||
|
||||
```text
|
||||
DagSchemeDescriptorBytes ::
|
||||
pel1_version (u16)
|
||||
|
||||
scheme_name (Utf8String)
|
||||
|
||||
program_type_tag (u32) // TypeTag.tag_id
|
||||
program_enc_profile (u16) // EncodingProfileId
|
||||
|
||||
has_trace_profile (u8)
|
||||
[ trace_profile_ref (EncodedRef) ] // if has_trace_profile == 0x01
|
||||
|
||||
has_opreg_ref (u8)
|
||||
[ opreg_ref (EncodedRef) ] // if has_opreg_ref == 0x01
|
||||
```
|
||||
|
||||
Constraints:
|
||||
|
||||
* `pel1_version` MUST be `1` for descriptors governed by this document.
|
||||
|
||||
* `scheme_name` MUST be encoded as a `Utf8String` (§2.4).
|
||||
|
||||
* `program_type_tag` encodes `TypeTag.tag_id` for `TYPE_TAG_PEL_PROGRAM_DAG_1`.
|
||||
|
||||
* `program_enc_profile` encodes the `EncodingProfileId` for `PEL_ENC_PROGRAM_DAG_V1` as defined in `ENC/PEL-PROGRAM-DAG/1`.
|
||||
|
||||
* `has_trace_profile`:
|
||||
|
||||
* `0x00` → `trace_profile_ref` is absent; no bytes for it follow.
|
||||
* `0x01` → `trace_profile_ref` is present and encoded as `EncodedRef`.
|
||||
* Any other value is an encoding error.
|
||||
|
||||
* `has_opreg_ref`:
|
||||
|
||||
* `0x00` → `opreg_ref` is absent.
|
||||
* `0x01` → `opreg_ref` is present and encoded as `EncodedRef`.
|
||||
* Any other value is an encoding error.
|
||||
|
||||
For the **canonical baseline descriptor**:
|
||||
|
||||
```text
|
||||
pel1_version = 1
|
||||
scheme_name = "PEL/PROGRAM-DAG/1"
|
||||
program_type_tag = TYPE_TAG_PEL_PROGRAM_DAG_1.tag_id
|
||||
program_enc_profile = PEL_ENC_PROGRAM_DAG_V1
|
||||
has_trace_profile = 0x00
|
||||
has_opreg_ref = 0x00
|
||||
```
|
||||
|
||||
The resulting bytes are `DagSchemeDescriptorBytes_DAG_1`.
|
||||
|
||||
### 4.3 Encoding and decoding (normative)
|
||||
|
||||
Let:
|
||||
|
||||
```text
|
||||
encode_dag_scheme_descriptor_v1 : DagSchemeDescriptor -> OctetString
|
||||
decode_dag_scheme_descriptor_v1 : OctetString -> DagSchemeDescriptor | error
|
||||
```
|
||||
|
||||
be the encoding and decoding functions for this profile.
|
||||
|
||||
**Encoding:**
|
||||
|
||||
Given a `DagSchemeDescriptor` value:
|
||||
|
||||
1. Emit `pel1_version (u16)`.
|
||||
|
||||
2. Emit `scheme_name` as `Utf8String`.
|
||||
|
||||
3. Emit `program_type_tag.tag_id` as `u32`.
|
||||
|
||||
4. Emit `program_enc_profile` as `u16`.
|
||||
|
||||
5. For `trace_profile_ref`:
|
||||
|
||||
* If absent:
|
||||
|
||||
* emit `has_trace_profile = 0x00`.
|
||||
|
||||
* If present:
|
||||
|
||||
* emit `has_trace_profile = 0x01`,
|
||||
* emit `trace_profile_ref` as `EncodedRef` (u32 length + `ReferenceBytes`).
|
||||
|
||||
6. For `opreg_ref`:
|
||||
|
||||
* If absent:
|
||||
|
||||
* emit `has_opreg_ref = 0x00`.
|
||||
|
||||
* If present:
|
||||
|
||||
* emit `has_opreg_ref = 0x01`,
|
||||
* emit `opreg_ref` as `EncodedRef`.
|
||||
|
||||
The concatenation of all emitted bytes is `DagSchemeDescriptorBytes`.
|
||||
|
||||
**Decoding:**
|
||||
|
||||
Given an `OctetString` known to contain exactly one `DagSchemeDescriptorBytes` value:
|
||||
|
||||
1. Read `pel1_version (u16)`.
|
||||
|
||||
* If `pel1_version != 1`, decoders that only implement this version MUST treat this as an encoding error. Future decoders MAY support additional versions but MUST NOT reinterpret `pel1_version = 1`.
|
||||
|
||||
2. Read `scheme_name` as `Utf8String` and validate UTF-8.
|
||||
|
||||
3. Read `program_type_tag (u32)` and construct `TypeTag { tag_id = program_type_tag }`.
|
||||
|
||||
4. Read `program_enc_profile (u16)`.
|
||||
|
||||
5. Read `has_trace_profile (u8)`:
|
||||
|
||||
* `0x00` → `trace_profile_ref = None`.
|
||||
* `0x01` → read `trace_profile_ref` as `EncodedRef` and decode to `Reference`.
|
||||
* other values → encoding error.
|
||||
|
||||
6. Read `has_opreg_ref (u8)`:
|
||||
|
||||
* `0x00` → `opreg_ref = None`.
|
||||
* `0x01` → read `opreg_ref` as `EncodedRef` and decode to `Reference`.
|
||||
* other values → encoding error.
|
||||
|
||||
7. If there are trailing bytes after successfully decoding all fields, decoders MAY treat this as an encoding error in contexts expecting a single `DagSchemeDescriptorBytes` value.
|
||||
|
||||
The mapping between `DagSchemeDescriptor` and `DagSchemeDescriptorBytes` defined here is the only encoding/decoding pair permitted by this profile.
|
||||
|
||||
### 4.4 Canonicality and injectivity
|
||||
|
||||
The mapping:
|
||||
|
||||
```text
|
||||
DagSchemeDescriptor -> DagSchemeDescriptorBytes
|
||||
```
|
||||
|
||||
defined above MUST be:
|
||||
|
||||
* **Injective** — distinct logical descriptor values MUST produce distinct byte strings.
|
||||
* **Stable** — the same logical descriptor MUST always encode to the same bytes across implementations and time.
|
||||
* **Streaming-friendly** — encoders and decoders MUST be implementable in a single forward pass; all length prefixes appear before their content.
|
||||
|
||||
In particular:
|
||||
|
||||
* Field ordering MUST NOT vary.
|
||||
* No alternative encodings (e.g. different integer widths, string formats, or positions) are permitted.
|
||||
* `EncodedRef` MUST always use canonical `ReferenceBytes` from `ENC/ASL1-CORE v1` (and therefore, when `HASH/ASL1` is present, inherit its digest-length consistency checks).
|
||||
|
||||
For the canonical DAG scheme, `DagSchemeDescriptor_DAG_1` encodes to a single, immutable `DagSchemeDescriptorBytes_DAG_1`. That byte sequence MUST NOT change once published.
|
||||
|
||||
### 4.5 Error handling (encoding layer)
|
||||
|
||||
Decoders for this profile MUST treat as **encoding errors** at the descriptor level:
|
||||
|
||||
1. **Unsupported `pel1_version`**
|
||||
|
||||
* `pel1_version != 1`.
|
||||
|
||||
2. **Invalid presence flags**
|
||||
|
||||
* `has_trace_profile` or `has_opreg_ref` not in `{ 0x00, 0x01 }`.
|
||||
|
||||
3. **Invalid `EncodedRef`**
|
||||
|
||||
* `ref_len < 2`, or
|
||||
* insufficient bytes to read `ref_bytes`, or
|
||||
* `ref_bytes` cannot be decoded as `ReferenceBytes` under `ENC/ASL1-CORE v1` (including digest-length mismatches for known `hash_id`s when `HASH/ASL1` is implemented).
|
||||
|
||||
4. **Invalid `Utf8String` for `scheme_name`**
|
||||
|
||||
* `scheme_name` bytes are not valid UTF-8.
|
||||
|
||||
5. **Truncation and over-long payloads**
|
||||
|
||||
* Not enough bytes to read any declared field.
|
||||
* In contexts expecting a single descriptor value, additional trailing bytes after decoding all fields.
|
||||
|
||||
Mapping from these encoding errors to external error codes (e.g. `ERR_PEL_SCHEME_DESC_INVALID`) is implementation-specific.
|
||||
|
||||
---
|
||||
|
||||
## 5. Definition of `SchemeRef_DAG_1`
|
||||
|
||||
### 5.1 General derivation from the descriptor Artifact
|
||||
|
||||
Let `DagSchemeDescriptorArtifact` be any Artifact of the form:
|
||||
|
||||
```text
|
||||
Artifact {
|
||||
type_tag = TYPE_TAG_PEL_SCHEME_DESC_1
|
||||
bytes = DagSchemeDescriptorBytes
|
||||
}
|
||||
```
|
||||
|
||||
such that `DagSchemeDescriptorBytes` decodes to some `DagSchemeDescriptor` value via `decode_dag_scheme_descriptor_v1`.
|
||||
|
||||
Given:
|
||||
|
||||
* encoding profile `P = ASL_ENC_CORE_V1`,
|
||||
* hash algorithm `H` with `HashId = HID`,
|
||||
|
||||
the scheme reference for this descriptor under `(P, H)` is:
|
||||
|
||||
```text
|
||||
ArtifactBytes = encode_artifact_core_v1(DagSchemeDescriptorArtifact)
|
||||
digest = H(ArtifactBytes)
|
||||
SchemeRef = Reference { hash_id = HID, digest = digest }
|
||||
```
|
||||
|
||||
This is `ASL/CORE-REF-DERIVE/1` instantiated with `ASL_ENC_CORE_V1`.
|
||||
|
||||
### 5.2 Canonical `SchemeRef_DAG_1` for Amduat 2.0
|
||||
|
||||
For the Amduat 2.0 baseline DAG scheme, we choose:
|
||||
|
||||
* `DagSchemeDescriptorArtifact = DagSchemeDescriptorArtifact_DAG_1`,
|
||||
* `P = ASL_ENC_CORE_V1` (EncodingProfileId = 0x0001),
|
||||
* `H = HASH-ASL1-256` (the mandatory ASL1-256 algorithm),
|
||||
* `HashId(H) = 0x0001`.
|
||||
|
||||
Then:
|
||||
|
||||
```text
|
||||
ArtifactBytes_DAG_1 = encode_artifact_core_v1(DagSchemeDescriptorArtifact_DAG_1)
|
||||
digest_DAG_1 = HASH-ASL1-256(ArtifactBytes_DAG_1)
|
||||
SchemeRef_DAG_1 = Reference { hash_id = 0x0001, digest = digest_DAG_1 }
|
||||
```
|
||||
|
||||
In the Amduat 2.0 baseline:
|
||||
|
||||
* `PEL/PROGRAM-DAG/1` binds its scheme symbol:
|
||||
|
||||
```text
|
||||
SchemeRef = SchemeRef_DAG_1
|
||||
Exec_s = Exec_DAG
|
||||
```
|
||||
|
||||
to this `Reference`.
|
||||
|
||||
* Engines that implement the Amduat 2.0 baseline DAG scheme MUST treat this specific `Reference` as “the” scheme identifier for `PEL/PROGRAM-DAG/1`.
|
||||
|
||||
### 5.3 Alternative deployments (non-baseline)
|
||||
|
||||
Other deployments MAY derive alternative scheme references from:
|
||||
|
||||
* the same descriptor Artifact but a different `(EncodingProfileId, HashId)` pair, or
|
||||
* a different descriptor Artifact (e.g. one with additional optional references or different metadata).
|
||||
|
||||
Such configurations:
|
||||
|
||||
* are not the Amduat 2.0 baseline, and
|
||||
* MUST NOT reuse the name `SchemeRef_DAG_1` for any scheme reference other than the one defined in §5.2.
|
||||
|
||||
Profiles MAY define their own symbolic names (e.g. `SchemeRef_DAG_1_PQ`) for alternate `(EncodingProfileId, HashId)` combinations, but those are outside the scope of this document.
|
||||
|
||||
---
|
||||
|
||||
## 6. Layering & Usage
|
||||
|
||||
### 6.1 Engine behavior
|
||||
|
||||
A PEL/1-CORE engine that claims support for the DAG scheme in the Amduat 2.0 baseline:
|
||||
|
||||
* MUST recognize `SchemeRef_DAG_1` (as defined in §5.2) as the scheme identifier corresponding to `PEL/PROGRAM-DAG/1`.
|
||||
|
||||
* MUST implement:
|
||||
|
||||
```text
|
||||
Exec_s = Exec_DAG
|
||||
```
|
||||
|
||||
when invoked with `scheme_ref = SchemeRef_DAG_1`.
|
||||
|
||||
* MUST treat Program Artifacts for this scheme as ASL/1 Artifacts whose `type_tag` equals the `program_type_tag` from the descriptor (i.e. `TYPE_TAG_PEL_PROGRAM_DAG_1`). The `program_enc_profile` field gives the encoding profile ID that engines use to select the appropriate Program encoding/decoding logic; in the Amduat 2.0 baseline this ID is `PEL_ENC_PROGRAM_DAG_V1` as defined in `ENC/PEL-PROGRAM-DAG/1`.
|
||||
|
||||
* MUST treat the descriptor Artifact as immutable metadata. Engines MAY bake in `SchemeRef_DAG_1` and the associated `TypeTag` and profile IDs at build time; they are not required to fetch or decode the descriptor on the execution hot path.
|
||||
|
||||
Nothing in this document requires engines to use `trace_profile_ref` or `opreg_ref` at runtime. Those fields exist so that tooling and profiles can discover related descriptors in a stable, content-addressed way.
|
||||
|
||||
### 6.2 Configuration and discovery
|
||||
|
||||
Tooling and configuration systems MAY use the descriptor to:
|
||||
|
||||
* discover:
|
||||
|
||||
* which `TypeTag` is used for DAG Programs,
|
||||
* which encoding profile ID applies to those Programs,
|
||||
* optional references to trace and operation-registry descriptors;
|
||||
|
||||
* populate engine configuration tables, e.g.:
|
||||
|
||||
```text
|
||||
scheme_table[SchemeRef_DAG_1] = {
|
||||
program_type_tag = TYPE_TAG_PEL_PROGRAM_DAG_1,
|
||||
program_enc_profile = PEL_ENC_PROGRAM_DAG_V1,
|
||||
trace_profile_ref = None,
|
||||
opreg_ref = None,
|
||||
}
|
||||
```
|
||||
|
||||
This document:
|
||||
|
||||
* MUST NOT introduce any store-level behavior, TGK edge semantics, certification rules, fact semantics, or overlay semantics.
|
||||
* ONLY binds PEL-level scheme semantics (`Exec_DAG`) to ASL-level values (`Artifact`, `TypeTag`, `Reference`).
|
||||
|
||||
---
|
||||
|
||||
## 7. Conformance
|
||||
|
||||
An implementation is **PEL/PROGRAM-DAG-DESC/1–conformant** if it satisfies all of:
|
||||
|
||||
1. **Descriptor encoding & decoding**
|
||||
|
||||
* Implements `encode_dag_scheme_descriptor_v1` / `decode_dag_scheme_descriptor_v1` as in §4.2–§4.3.
|
||||
* Treats `pel1_version = 1` as the only supported version for this descriptor profile.
|
||||
* Enforces presence flags and `EncodedRef` structure as defined in §2.4 and §4.5.
|
||||
|
||||
2. **Recognition of the descriptor Artifact**
|
||||
|
||||
* Recognizes `TYPE_TAG_PEL_SCHEME_DESC_1` as the PEL scheme descriptor tag for this document.
|
||||
* For `type_tag = TYPE_TAG_PEL_SCHEME_DESC_1`, is able to decode `bytes` as `DagSchemeDescriptorBytes` and obtain a `DagSchemeDescriptor`.
|
||||
* Recognizes `DagSchemeDescriptor_DAG_1` (per §3.3) as the canonical descriptor value for the DAG scheme in Amduat 2.0 (e.g. by comparing decoded fields).
|
||||
|
||||
3. **Derivation of `SchemeRef_DAG_1`**
|
||||
|
||||
* When configured with `ASL_ENC_CORE_V1` and `HASH-ASL1-256` (`HashId = 0x0001`), derives `SchemeRef_DAG_1` exactly as in §5.2 from `DagSchemeDescriptorArtifact_DAG_1`.
|
||||
* Does not derive `SchemeRef_DAG_1` from any other Artifact or under any other `(EncodingProfileId, HashId)` pair.
|
||||
|
||||
4. **Scheme binding**
|
||||
|
||||
* For `SchemeRef = SchemeRef_DAG_1`, implements `Exec_s` as `Exec_DAG` per `PEL/PROGRAM-DAG/1`.
|
||||
* Uses `program_type_tag` and `program_enc_profile` from the descriptor when interpreting Program Artifacts for this scheme (at build time or configuration time; not necessarily on every execution).
|
||||
|
||||
5. **Layering discipline**
|
||||
|
||||
* Does not introduce store, TGK, certificate, fact, or overlay semantics into the descriptor logic.
|
||||
* Treats this document purely as a binding between:
|
||||
|
||||
* the PEL scheme (`PEL/PROGRAM-DAG/1`),
|
||||
* its program representation (`TYPE_TAG_PEL_PROGRAM_DAG_1` + `PEL_ENC_PROGRAM_DAG_V1`),
|
||||
* and an ASL/1 `SchemeRef` (`SchemeRef_DAG_1`).
|
||||
|
||||
Everything else — store wiring, TGK edges, receipts, facts, overlays, and domain semantics — is delegated to other specifications.
|
||||
|
||||
---
|
||||
|
||||
## 8. Version History
|
||||
|
||||
* **0.1.6 — 2025-11-16** — Marked `ENC/PEL-PROGRAM-DAG/1` as a normative dependency and clarified that `program_enc_profile` is specifically `PEL_ENC_PROGRAM_DAG_V1`.
|
||||
* **0.1.5 — 2025-11-16** — Clarified the role of `program_enc_profile` vs `ASL_ENC_CORE_V1` and tightened wording around how Program Artifacts are interpreted.
|
||||
* **0.1.4 — 2025-11-16** — Tightened decoding wording, clarified the uniqueness of the encoding/decoding pair, and polished streaming/injectivity language.
|
||||
* **0.1.3 — 2025-11-16** — Clarified RFC 2119 usage, layering around program encoding, and tightened conformance wording.
|
||||
* **0.1.2 — 2025-11-16** — Refined encoding error rules, clarified `TYPE_TAG_PEL_SCHEME_DESC_1` reuse, and described engine usage more explicitly.
|
||||
* **0.1.1 — 2025-11-16** — Added logical descriptor model, descriptor Artifact & encoding, canonical descriptor value, and explicit `SchemeRef_DAG_1` derivation.
|
||||
* **0.1.0 — 2025-11-16** — Initial skeleton with structure, roles, and high-level field model for the DAG scheme descriptor.
|
||||
|
||||
---
|
||||
|
||||
## Document History
|
||||
|
||||
* **0.1.6 (2025-11-16):** Registered as Tier-1 spec and aligned to the Amduat 2.0 substrate baseline.
|
||||
748
tier1/pel-trace-dag-1.md
Normal file
748
tier1/pel-trace-dag-1.md
Normal file
|
|
@ -0,0 +1,748 @@
|
|||
# PEL/TRACE-DAG/1 — DAG Execution Trace Profile
|
||||
|
||||
Status: Approved
|
||||
Owner: Niklas Rydberg
|
||||
Version: 0.2.1
|
||||
SoT: Yes
|
||||
Last Updated: 2025-11-16
|
||||
Linked Phase Pack: N/A
|
||||
Tags: [execution, traceability]
|
||||
|
||||
<!-- Source: /amduat/docs/new/pel-trace-dag-1.md | Canonical: /amduat/tier1/pel-trace-dag-1.md -->
|
||||
|
||||
**Document ID:** `PEL/TRACE-DAG/1`
|
||||
**Layer:** L1 Scheme Trace Profile (on top of PEL/1-CORE + PEL/PROGRAM-DAG/1)
|
||||
|
||||
**Depends on (normative):**
|
||||
|
||||
* `ASL/1-CORE v0.4.x` — value model (`Artifact`, `Reference`, `TypeTag`, integers, `OctetString`)
|
||||
* `PEL/1-CORE v0.3.x` — primitive execution layer (`ExecutionStatus`, `ExecutionErrorSummary`, diagnostics)
|
||||
* `PEL/PROGRAM-DAG/1 v0.3.1` — DAG Program scheme (`Program`, `Node`, `NodeId`, canonical topological order)
|
||||
|
||||
**Integrates with (informative):**
|
||||
|
||||
* `PEL/1-SURF v0.2.x` — store-backed execution surface
|
||||
* `ENC/PEL-TRACE-DAG/1` (planned) — canonical encoding for DAG traces
|
||||
* `TGK/1-CORE` — trace graph kernel (execution edges)
|
||||
* `ENC/ASL1-CORE v1.0.x` — canonical Artifact encoding
|
||||
* `HASH/ASL1 v0.2.4` — ASL1 hash family
|
||||
|
||||
© 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
|
||||
|
||||
`PEL/TRACE-DAG/1` defines a **standard trace value** for executions of the `PEL/PROGRAM-DAG/1` scheme:
|
||||
|
||||
* It records **per-node status and outputs** in **canonical node order**.
|
||||
* It links the trace to:
|
||||
|
||||
* the **Program Artifact** (`program_ref`),
|
||||
* the **inputs** and optional **params** used by the run,
|
||||
* the overall **scheme** and (optionally) the **ExecutionResult** Artifact.
|
||||
|
||||
The trace is represented as a single ASL/1 Artifact (a **TraceArtifact**) whose payload is a `TraceDAGValue` (defined below) and whose `TypeTag` is dedicated to this profile.
|
||||
|
||||
The trace is:
|
||||
|
||||
* **Optional** — some deployments may choose not to record it.
|
||||
* **Deterministic** — for fixed inputs and Program, all conformant implementations produce identical traces.
|
||||
* **Graph-friendly** — TGK/1 can interpret it into node-level execution edges for provenance.
|
||||
|
||||
Binary layout and `TypeTag` assignment are defined in a companion encoding profile (`ENC/PEL-TRACE-DAG/1`); this document specifies only the **logical model and semantics**.
|
||||
|
||||
---
|
||||
|
||||
## 1. Purpose & Non-Goals
|
||||
|
||||
### 1.1 Purpose
|
||||
|
||||
The goals of `PEL/TRACE-DAG/1` are to:
|
||||
|
||||
1. Provide a **canonical node-level trace** for `PEL/PROGRAM-DAG/1` runs.
|
||||
2. Capture for each `Node`:
|
||||
|
||||
* whether it was executed,
|
||||
* whether it succeeded or failed,
|
||||
* the **`Reference`s** of any Artifacts it produced,
|
||||
* deterministic diagnostic entries.
|
||||
|
||||
3. Link node-level information to:
|
||||
|
||||
* the **Program** that defined the DAG,
|
||||
* the **input** and **params** Artifacts,
|
||||
* the run-level `ExecutionStatus` / `ExecutionErrorSummary`.
|
||||
|
||||
This trace enables:
|
||||
|
||||
* reconstruction of **per-node execution edges** in TGK/1,
|
||||
* human and machine debugging of runs,
|
||||
* post-hoc provenance analysis and selective re-execution.
|
||||
|
||||
### 1.2 Non-Goals
|
||||
|
||||
This profile does **not** define:
|
||||
|
||||
* Graph/provenance edges themselves — TGK/1 defines how traces become edges.
|
||||
* Concrete binary encodings — these belong to `ENC/PEL-TRACE-DAG/1`.
|
||||
* How and when traces are **enabled** — that is a policy/configuration decision.
|
||||
* Store interactions — those belong to `ASL/1-STORE` and `PEL/1-SURF`.
|
||||
* Semantics of operations (`OperationId`), parameter schemas, or error codes — those belong to operation registries (e.g. `OPREG/PEL1-KERNEL` and extensions).
|
||||
|
||||
---
|
||||
|
||||
## 2. Context and Layering
|
||||
|
||||
### 2.1 Relationship to PEL/PROGRAM-DAG/1
|
||||
|
||||
`PEL/PROGRAM-DAG/1` defines:
|
||||
|
||||
* The **Program** data model (`Program`, `Node`, `NodeId`, `RootRef`).
|
||||
* Structural validity rules (unique `NodeId`s, DAG constraint, etc.).
|
||||
* A canonical **topological order** of Nodes.
|
||||
|
||||
`PEL/TRACE-DAG/1` assumes:
|
||||
|
||||
* The run was performed against a particular Program Artifact (`program_ref`).
|
||||
* The Program is **structurally valid** under `PEL/PROGRAM-DAG/1`.
|
||||
* Node evaluation order is the scheme’s canonical topological order.
|
||||
|
||||
This profile adds:
|
||||
|
||||
* A `TraceDAGValue` expressed in terms of that Program’s `NodeId`s and operations.
|
||||
|
||||
### 2.2 Relationship to PEL/1-CORE and PEL/1-SURF
|
||||
|
||||
At the PEL/1 level, a scheme `s` is bound to a pure function:
|
||||
|
||||
```text
|
||||
Exec_s(
|
||||
program: Artifact,
|
||||
inputs: list<Artifact>,
|
||||
params: optional Artifact
|
||||
) -> (outputs: list<Artifact>, result: ExecutionResultValue)
|
||||
````
|
||||
|
||||
For the DAG scheme (`PEL/PROGRAM-DAG/1`):
|
||||
|
||||
* `Exec_DAG` plays that role.
|
||||
|
||||
`PEL/TRACE-DAG/1` sits just above:
|
||||
|
||||
* It defines the shape of a `TraceDAGValue` that can be produced **in addition to** the `outputs` and `ExecutionResultValue`.
|
||||
* A PEL/1 surface (e.g. `PEL/1-SURF`) that implements this profile:
|
||||
|
||||
* persists this trace as an Artifact with a dedicated `TypeTag`,
|
||||
* obtains its `Reference` via `ASL/1-STORE.put`,
|
||||
* exposes that `Reference` as `trace_ref` in its surface-level `ExecutionResult` Artifact.
|
||||
|
||||
If `Exec_DAG` is **not** invoked at all (e.g. due to store-level failures handled in `PEL/1-SURF`), then `PEL/TRACE-DAG/1` is simply **not applied**: no `TraceDAGValue` and no trace Artifact are produced for that run.
|
||||
|
||||
### 2.3 Relationship to TGK/1
|
||||
|
||||
TGK/1 can treat a `TraceDAGValue` as:
|
||||
|
||||
* A **per-node execution log**, keyed by `program_ref` and `NodeId`.
|
||||
* A list of **produced Artifacts** (`output_refs` per node).
|
||||
* A basis for edges like:
|
||||
|
||||
* “node N (operation O) produced artifact A by reading B, C, …”,
|
||||
* “this run (ExecutionResult) used Program P and generated outputs X, Y, …”.
|
||||
|
||||
This document does not prescribe exact edge types; it only ensures traces are **structured enough** for TGK/1 to derive such edges deterministically.
|
||||
|
||||
---
|
||||
|
||||
## 3. Data Model
|
||||
|
||||
### 3.1 Reused Types
|
||||
|
||||
From `ASL/1-CORE`:
|
||||
|
||||
```text
|
||||
Reference {
|
||||
hash_id: HashId
|
||||
digest: OctetString
|
||||
}
|
||||
|
||||
HashId = uint16
|
||||
```
|
||||
|
||||
From `PEL/1-CORE`:
|
||||
|
||||
```text
|
||||
ExecutionStatus = uint8
|
||||
ExecutionErrorKind = uint8
|
||||
|
||||
ExecutionErrorSummary {
|
||||
kind: ExecutionErrorKind
|
||||
status_code: uint32
|
||||
}
|
||||
```
|
||||
|
||||
`PEL/1-CORE` defines the shared meanings of:
|
||||
|
||||
```text
|
||||
ExecutionStatus {
|
||||
OK = 0
|
||||
SCHEME_UNSUPPORTED= 1
|
||||
INVALID_PROGRAM = 2
|
||||
INVALID_INPUTS = 3
|
||||
RUNTIME_FAILED = 4
|
||||
}
|
||||
|
||||
ExecutionErrorKind {
|
||||
NONE = 0
|
||||
SCHEME = 1
|
||||
PROGRAM = 2
|
||||
INPUTS = 3
|
||||
RUNTIME = 4
|
||||
}
|
||||
```
|
||||
|
||||
From `PEL/PROGRAM-DAG/1`:
|
||||
|
||||
```text
|
||||
NodeId = uint32
|
||||
|
||||
Program { nodes: list<Node>; roots: list<RootRef>; }
|
||||
|
||||
Node {
|
||||
id: NodeId
|
||||
op: OperationId
|
||||
inputs: list<DagInput>
|
||||
params: ParamsBytes
|
||||
}
|
||||
|
||||
OperationId {
|
||||
name: string // logical UTF-8 name
|
||||
version: uint32
|
||||
}
|
||||
```
|
||||
|
||||
The encoding of `string` and `ParamsBytes` is defined by `ENC/PEL-PROGRAM-DAG/1`.
|
||||
|
||||
### 3.2 DiagnosticEntry
|
||||
|
||||
For trace-level diagnostics, this profile reuses the generic diagnostic shape used in PEL/1:
|
||||
|
||||
```text
|
||||
DiagnosticEntry {
|
||||
code: uint32 // scheme- or op-specific diagnostic code
|
||||
message: OctetString // often UTF-8 text; interpretation is profile-specific
|
||||
}
|
||||
```
|
||||
|
||||
Requirements:
|
||||
|
||||
* `code` is intended for machine use; `message` is for human-readable information.
|
||||
* Both MUST be deterministic for a given run.
|
||||
|
||||
### 3.3 NodeTraceStatus
|
||||
|
||||
Node-level status distinguishes whether the node:
|
||||
|
||||
* ran and succeeded,
|
||||
* ran and failed at runtime,
|
||||
* did not run due to an earlier failure.
|
||||
|
||||
```text
|
||||
NodeTraceStatus = uint8
|
||||
|
||||
NodeTraceStatus {
|
||||
NODE_OK = 0 // Node executed successfully
|
||||
NODE_FAILED = 1 // Node executed and failed (runtime failure)
|
||||
NODE_SKIPPED = 2 // Node was not executed due to earlier run-level failure
|
||||
}
|
||||
```
|
||||
|
||||
Invariants per status:
|
||||
|
||||
* `NODE_OK`:
|
||||
|
||||
* The node’s operation executed successfully.
|
||||
* `status_code` MUST be `0`.
|
||||
* `output_refs` MAY be empty or non-empty, depending on the operation.
|
||||
|
||||
* `NODE_FAILED`:
|
||||
|
||||
* The node’s operation was invoked and returned a **runtime error**.
|
||||
* `status_code` MUST be non-zero.
|
||||
* `output_refs` MUST be empty (this profile treats failing nodes as producing no durable outputs).
|
||||
|
||||
* `NODE_SKIPPED`:
|
||||
|
||||
* The node was not executed because the run terminated early (`RUNTIME_FAILED`, `INVALID_INPUTS`, or `INVALID_PROGRAM`).
|
||||
* `status_code` MUST be `0`.
|
||||
* `output_refs` MUST be empty.
|
||||
* `diagnostics` MAY contain a short deterministic explanation, but SHOULD be empty in minimal profiles.
|
||||
|
||||
Relation to run-level `ExecutionStatus`:
|
||||
|
||||
* If the run-level `status = OK`, then every `NodeTraceDAG.status` MUST be `NODE_OK`.
|
||||
* If any `NodeTraceDAG.status = NODE_FAILED`, then the run-level `status` MUST be `RUNTIME_FAILED`.
|
||||
* For `status ∈ { INVALID_PROGRAM, INVALID_INPUTS }`, node statuses MAY be `NODE_OK` (for nodes that executed before the invalid condition was detected) or `NODE_SKIPPED`, but MUST NOT be `NODE_FAILED` (runtime failures always map to `RUNTIME_FAILED`).
|
||||
|
||||
### 3.4 NodeTraceDAG
|
||||
|
||||
A node-level trace entry:
|
||||
|
||||
```text
|
||||
NodeTraceDAG {
|
||||
node_id: NodeId
|
||||
op_name: string // duplicate of Program.nodes[i].op.name
|
||||
op_version: uint32 // duplicate of Program.nodes[i].op.version
|
||||
|
||||
status: NodeTraceStatus
|
||||
status_code: uint32 // 0 = success; non-zero = op-specific failure code for NODE_FAILED
|
||||
|
||||
output_refs: list<Reference> // artifacts produced by this node (if any) in store space
|
||||
diagnostics: list<DiagnosticEntry>
|
||||
}
|
||||
```
|
||||
|
||||
Requirements:
|
||||
|
||||
* `node_id` MUST correspond to some `Node.id` in the Program identified by `program_ref`.
|
||||
|
||||
* `op_name` / `op_version` MUST match the `OperationId` of that `Node` as decoded from the Program Artifact. They are a **denormalized copy** so traces remain understandable even if the Program is not immediately available.
|
||||
|
||||
* `output_refs`:
|
||||
|
||||
* MUST list, in order, the `Reference`s obtained when persisting this node’s output Artifacts (via `ASL/1-STORE.put`) in the Store used for this run.
|
||||
* MAY be empty if the operation logically has no outputs, or the node failed / was skipped.
|
||||
|
||||
* `diagnostics`:
|
||||
|
||||
* For `NODE_OK`, MAY be empty or contain non-fatal diagnostics (e.g. warnings) if the operation registry defines them.
|
||||
* For `NODE_FAILED`, SHOULD contain at least one entry describing the failure.
|
||||
* For `NODE_SKIPPED`, MAY be empty or contain a short deterministic explanation.
|
||||
|
||||
### 3.5 TraceDAGValue
|
||||
|
||||
The top-level trace for a DAG run:
|
||||
|
||||
```text
|
||||
TraceDAGValue {
|
||||
pel1_version: uint16 // MUST be 1 for this version
|
||||
scheme_ref: Reference // MUST be SchemeRef_DAG_1
|
||||
program_ref: Reference // Program Artifact used by this run
|
||||
|
||||
status: ExecutionStatus
|
||||
summary: ExecutionErrorSummary
|
||||
|
||||
exec_result_ref: optional Reference // Reference to surface ExecutionResult Artifact (if available)
|
||||
|
||||
input_refs: list<Reference> // in the same order as Exec_DAG.inputs
|
||||
params_ref: optional Reference // params Artifact used for this run, if any
|
||||
|
||||
node_traces: list<NodeTraceDAG> // node-level traces in canonical node order
|
||||
}
|
||||
```
|
||||
|
||||
Constraints:
|
||||
|
||||
* `pel1_version`:
|
||||
|
||||
* MUST be `1` for traces produced under this version of the spec.
|
||||
|
||||
* `scheme_ref`:
|
||||
|
||||
* MUST equal `SchemeRef_DAG_1` for this scheme.
|
||||
|
||||
* `program_ref`:
|
||||
|
||||
* MUST be the `Reference` of the Program Artifact passed to the run.
|
||||
|
||||
* `status` and `summary`:
|
||||
|
||||
* MUST match the `ExecutionStatus` and `ExecutionErrorSummary` of the run-level `ExecutionResultValue` produced by `Exec_DAG`.
|
||||
* `summary.kind` and `summary.status_code` MUST obey the mapping defined for `PEL/PROGRAM-DAG/1`.
|
||||
|
||||
* `exec_result_ref`:
|
||||
|
||||
* If the run produced a surface-level `ExecutionResult` Artifact (as in `PEL/1-SURF`), this SHOULD be its `Reference`.
|
||||
* If no such Artifact exists or is not persisted, it MUST be absent.
|
||||
|
||||
* `input_refs`:
|
||||
|
||||
* MUST be the list of `Reference`s corresponding to the `inputs` passed to `Exec_DAG`, in the same order.
|
||||
|
||||
* `params_ref`:
|
||||
|
||||
* If a params Artifact was provided for the run, MUST be that `Reference`.
|
||||
* If no params Artifact was provided (or the scheme ignores params), MUST be absent.
|
||||
|
||||
* `node_traces`:
|
||||
|
||||
* If the Program was **successfully decoded and structurally valid** and at least one Node was attempted, `node_traces` MUST contain:
|
||||
|
||||
* exactly one `NodeTraceDAG` per `Node` in the Program, and
|
||||
* in the **canonical node order** defined by `PEL/PROGRAM-DAG/1`.
|
||||
|
||||
* For runs that fail before any Node is attempted (e.g. `INVALID_PROGRAM` due to decode failure, or `INVALID_INPUTS` detected before the first Node), `node_traces` MUST be empty, because no node evaluation took place.
|
||||
|
||||
---
|
||||
|
||||
## 4. Trace Semantics for a Single Run
|
||||
|
||||
This section defines how a conformant engine or surface SHOULD construct `TraceDAGValue` for a single `PEL/PROGRAM-DAG/1` run, assuming `Exec_DAG` was actually invoked.
|
||||
|
||||
We consider a run characterized by:
|
||||
|
||||
* `program_ref : Reference`
|
||||
* `program_artifact : Artifact` (whose `bytes` decode to a `Program` under `PEL/PROGRAM-DAG/1` + its encoding profile)
|
||||
* `input_refs : list<Reference>`
|
||||
* `inputs : list<Artifact>` (resolved from a Store)
|
||||
* `params_ref : optional Reference`
|
||||
* `params_artifact : optional Artifact`
|
||||
* `status : ExecutionStatus`
|
||||
* `summary : ExecutionErrorSummary`
|
||||
* Internal records of per-node results:
|
||||
|
||||
* `node_outputs : NodeId -> list<Artifact>` (for nodes that executed successfully),
|
||||
* `node_runtime_errors : NodeId -> (status_code, diagnostics)` (for nodes that failed at runtime),
|
||||
* and a notion of **which Nodes were evaluated**.
|
||||
|
||||
Implementations MAY organize their internal state differently; the following is conceptual.
|
||||
|
||||
### 4.1 Trace for successful runs (`status = OK`)
|
||||
|
||||
If `status = OK`:
|
||||
|
||||
1. **Program and ordering**
|
||||
|
||||
* The Program MUST be structurally valid (per `PEL/PROGRAM-DAG/1`).
|
||||
* The engine MUST know the canonical node order (topological order with `NodeId` tie-breakers).
|
||||
|
||||
2. **Node traces**
|
||||
|
||||
* For each `Node` in canonical order:
|
||||
|
||||
```text
|
||||
NodeTraceDAG {
|
||||
node_id = Node.id
|
||||
op_name = Node.op.name
|
||||
op_version = Node.op.version
|
||||
status = NODE_OK
|
||||
status_code = 0
|
||||
output_refs = [ R_0, ..., R_(k-1) ] // refs from store.put on each output Artifact
|
||||
diagnostics = D // deterministic diagnostics, possibly empty
|
||||
}
|
||||
```
|
||||
|
||||
* No nodes are `NODE_FAILED` or `NODE_SKIPPED` in a run with `status = OK`.
|
||||
|
||||
3. **Top-level fields**
|
||||
|
||||
* `TraceDAGValue` MUST be:
|
||||
|
||||
```text
|
||||
pel1_version = 1
|
||||
scheme_ref = SchemeRef_DAG_1
|
||||
program_ref = program_ref
|
||||
|
||||
status = OK
|
||||
summary.kind = NONE
|
||||
summary.status_code = 0
|
||||
|
||||
exec_result_ref = execution_result_ref (if available, else absent)
|
||||
|
||||
input_refs = input_refs (exact order used in run)
|
||||
params_ref = params_ref (if any)
|
||||
|
||||
node_traces = [ NodeTraceDAG in canonical node order ]
|
||||
```
|
||||
|
||||
### 4.2 Trace for runtime failures (`status = RUNTIME_FAILED`)
|
||||
|
||||
If `status = RUNTIME_FAILED` and at least one Node executed:
|
||||
|
||||
1. **Nodes before the first failing node**
|
||||
|
||||
* For Nodes that executed successfully before the failure:
|
||||
|
||||
* Same as in §4.1: `status = NODE_OK`, `status_code = 0`, `output_refs` as persisted.
|
||||
|
||||
2. **Failing node**
|
||||
|
||||
* For the first Node that failed at runtime:
|
||||
|
||||
```text
|
||||
NodeTraceDAG {
|
||||
node_id = Node.id
|
||||
op_name = Node.op.name
|
||||
op_version = Node.op.version
|
||||
status = NODE_FAILED
|
||||
status_code = runtime_status_code // from operation semantics
|
||||
output_refs = [] // no durable outputs recorded
|
||||
diagnostics = runtime_diagnostics // deterministic list
|
||||
}
|
||||
```
|
||||
|
||||
3. **Nodes after the failing node**
|
||||
|
||||
* For all Nodes that were not executed because the run terminated:
|
||||
|
||||
```text
|
||||
NodeTraceDAG {
|
||||
node_id = Node.id
|
||||
op_name = Node.op.name
|
||||
op_version = Node.op.version
|
||||
status = NODE_SKIPPED
|
||||
status_code = 0
|
||||
output_refs = []
|
||||
diagnostics = [] // MAY contain a short deterministic message, but SHOULD be empty
|
||||
}
|
||||
```
|
||||
|
||||
4. **Top-level fields**
|
||||
|
||||
* `TraceDAGValue` MUST set:
|
||||
|
||||
```text
|
||||
status = RUNTIME_FAILED
|
||||
summary.kind = RUNTIME
|
||||
summary.status_code = status_code // non-zero, matching ExecutionResultValue.summary.status_code
|
||||
|
||||
// other fields as in §4.1
|
||||
```
|
||||
|
||||
### 4.3 Trace for invalid inputs / invalid program
|
||||
|
||||
For `status = INVALID_INPUTS` or `status = INVALID_PROGRAM` (as produced by `Exec_DAG`, not by store-level surfaces):
|
||||
|
||||
* If no Node is executed at all:
|
||||
|
||||
* `node_traces` MUST be empty.
|
||||
* `status` and `summary` MUST match the run-level `ExecutionResultValue`.
|
||||
* It is RECOMMENDED to include at least one diagnostic (in `summary` or operation-level diagnostics) indicating the error (e.g., which input index was missing, or why the Program was invalid).
|
||||
|
||||
* If the engine partially evaluates the Program before detecting an invalid condition (allowed only where consistent with `PEL/PROGRAM-DAG/1`):
|
||||
|
||||
* Node traces for executed Nodes MUST be recorded with `status = NODE_OK` (no runtime failure).
|
||||
* Nodes that were never reached MUST be marked `NODE_SKIPPED`.
|
||||
* No `NodeTraceDAG` MAY have `status = NODE_FAILED` in runs where `status ∈ { INVALID_PROGRAM, INVALID_INPUTS }`.
|
||||
|
||||
In all cases, the mapping from the precise validation failure to node-level traces MUST be deterministic for a given run and MUST be consistent with the run-level `status` and `summary`.
|
||||
|
||||
---
|
||||
|
||||
## 5. Determinism
|
||||
|
||||
### 5.1 Determinism contract
|
||||
|
||||
For fixed:
|
||||
|
||||
* `program_artifact.bytes`,
|
||||
* `input_refs` + the contents of their referenced Artifacts in the Store,
|
||||
* `params_ref` + its Artifact contents (if present),
|
||||
* the same operation registries and parameter profiles for all `OperationId`s referenced in the Program,
|
||||
|
||||
then:
|
||||
|
||||
> All conformant implementations that:
|
||||
>
|
||||
> * execute the run under the `PEL/PROGRAM-DAG/1` scheme, and
|
||||
> * produce a `TraceDAGValue` under `PEL/TRACE-DAG/1`
|
||||
>
|
||||
> MUST produce identical `TraceDAGValue` logical values.
|
||||
|
||||
This implies:
|
||||
|
||||
* Identical `status` and `summary`.
|
||||
* Identical `input_refs`, `params_ref`, and `program_ref`.
|
||||
* Identical `node_traces` sequence, with:
|
||||
|
||||
* same `node_id`, `op_name`, `op_version`,
|
||||
* same `NodeTraceStatus`, `status_code`,
|
||||
* identical `output_refs` (same `Reference`s, same order),
|
||||
* identical `diagnostics`.
|
||||
|
||||
### 5.2 No ambient environment
|
||||
|
||||
Trace construction MUST NOT depend on:
|
||||
|
||||
* host clocks, random number generators, environment variables,
|
||||
* process IDs, thread IDs, or other non-deterministic identifiers,
|
||||
* non-deterministic logging or scheduling.
|
||||
|
||||
Any data that appears in diagnostics or `status_code` MUST be determined solely by:
|
||||
|
||||
* the Program value,
|
||||
* input/params Artifacts,
|
||||
* deterministic operation semantics,
|
||||
* and deterministic scheme-level logic.
|
||||
|
||||
---
|
||||
|
||||
## 6. Interaction with PEL/1-SURF (Informative)
|
||||
|
||||
A PEL/1 surface that implements this profile typically proceeds as follows for runs where `Exec_DAG` is invoked:
|
||||
|
||||
1. **Resolve inputs**
|
||||
|
||||
* Use `ASL/1-STORE.get` to resolve `program_ref`, `input_refs`, and `params_ref` (if present).
|
||||
* Handle Store-level errors per `PEL/1-SURF` (mapping to `INVALID_INPUTS` / `INVALID_PROGRAM` and **not** calling `Exec_DAG`).
|
||||
In these cases, **no trace Artifact is produced** under this profile.
|
||||
|
||||
2. **Run Exec_DAG**
|
||||
|
||||
* Call:
|
||||
|
||||
```text
|
||||
(outputs, exec_result_value) =
|
||||
Exec_DAG(program_artifact, input_artifacts, params_artifact?)
|
||||
```
|
||||
|
||||
* Persist `outputs` and the surface-level `ExecutionResult` Artifact, yielding `output_refs` and `exec_result_ref`.
|
||||
|
||||
3. **Construct TraceDAGValue**
|
||||
|
||||
* Using:
|
||||
|
||||
* `program_ref`,
|
||||
* `input_refs`,
|
||||
* `params_ref`,
|
||||
* `exec_result_ref`,
|
||||
* `exec_result_value.status` and `summary`,
|
||||
* node-level outputs and errors recorded during execution,
|
||||
|
||||
* Construct `TraceDAGValue` as in §3–§4.
|
||||
|
||||
4. **Persist TraceArtifact**
|
||||
|
||||
* Encode `TraceDAGValue` as an ASL/1 Artifact:
|
||||
|
||||
```text
|
||||
TraceArtifact {
|
||||
bytes = TraceDAGBytes // per ENC/PEL-TRACE-DAG/1
|
||||
type_tag = TYPE_TAG_PEL_TRACE_DAG_1
|
||||
}
|
||||
```
|
||||
|
||||
* Call `ASL/1-STORE.put(TraceArtifact)` to obtain `trace_ref`.
|
||||
|
||||
5. **Expose trace_ref**
|
||||
|
||||
* Include `trace_ref` in the surface-level `ExecutionResult` Artifact (as an optional field).
|
||||
* TGK/1 and higher layers can then traverse from `ExecutionResult` → `trace_ref` → `TraceDAGValue` → per-node `output_refs`.
|
||||
|
||||
This flow is informative; implementations MAY pipeline or optimize, provided the observable `TraceDAGValue` is unchanged.
|
||||
|
||||
---
|
||||
|
||||
## 7. Conformance
|
||||
|
||||
An implementation is **PEL/TRACE-DAG/1–conformant** if it:
|
||||
|
||||
1. **Implements the TraceDAGValue model**
|
||||
|
||||
* Produces trace values that satisfy all field constraints in §3.
|
||||
* Sets `pel1_version = 1` and `scheme_ref = SchemeRef_DAG_1`.
|
||||
|
||||
2. **Respects status alignment**
|
||||
|
||||
* Ensures `TraceDAGValue.status` and `TraceDAGValue.summary` always match the run-level `ExecutionResultValue` produced for the same run.
|
||||
* Ensures that the rules relating `NodeTraceStatus` and run-level `ExecutionStatus` (§3.3, §4) are upheld.
|
||||
|
||||
3. **Maintains canonical node order and coverage**
|
||||
|
||||
* For structurally valid Programs where `Exec_DAG` evaluated at least one Node, emits `node_traces`:
|
||||
|
||||
* in the canonical topological order defined by `PEL/PROGRAM-DAG/1`, and
|
||||
* with exactly one `NodeTraceDAG` per Program `Node`.
|
||||
|
||||
* For runs where no Node is attempted, emits `node_traces = []`.
|
||||
|
||||
4. **Uses NodeTraceStatus correctly**
|
||||
|
||||
* Uses `NODE_OK`, `NODE_FAILED`, `NODE_SKIPPED` with semantics defined in §3.3 and §4.
|
||||
* Ensures `status_code` and `output_refs` obey the rules for each status.
|
||||
|
||||
5. **Ensures determinism**
|
||||
|
||||
* For fixed inputs and Program, always produces identical `TraceDAGValue` (across runs, machines, implementations).
|
||||
* Does not inject host or environment variability into the trace.
|
||||
|
||||
6. **Separates concerns**
|
||||
|
||||
* Does not conflate Store-level errors (e.g., `ERR_NOT_FOUND`) with node-level runtime failures; Store errors are handled in `PEL/1-SURF` and MUST NOT produce spurious `NodeTraceDAG` entries.
|
||||
* Does not encode provenance graph semantics in the trace; it only provides structured data that TGK/1 can interpret.
|
||||
|
||||
---
|
||||
|
||||
## 8. Security and Privacy Considerations
|
||||
|
||||
1. **Information exposure**
|
||||
|
||||
* `TraceDAGValue` includes:
|
||||
|
||||
* references to input Artifacts,
|
||||
* references to intermediate outputs,
|
||||
* per-node diagnostics.
|
||||
|
||||
* Anyone with access to the trace and the Store may gain insight into:
|
||||
|
||||
* data flow,
|
||||
* intermediate values,
|
||||
* failure modes.
|
||||
|
||||
* Domains concerned with secrecy MUST treat trace Artifacts as sensitive and control access appropriately (e.g., by Store policy or overlays).
|
||||
|
||||
2. **Trace volume**
|
||||
|
||||
* Large Programs with many Nodes and outputs can produce large traces.
|
||||
|
||||
* Implementations SHOULD consider:
|
||||
|
||||
* trace sampling or truncation (but MUST keep it deterministic if used),
|
||||
* separate “debug” vs “production” trace policies.
|
||||
|
||||
* Any truncation or sampling profile MUST be expressed as a separate spec/profile; this baseline assumes full traces.
|
||||
|
||||
3. **Integrity**
|
||||
|
||||
* Trace integrity is rooted in:
|
||||
|
||||
* `HASH/ASL1` (for Artifact identity),
|
||||
* Store semantics (`ASL/1-STORE`),
|
||||
* optional certification (`CIL/1`).
|
||||
|
||||
* Tampering with trace Artifacts is detectable via mismatches between:
|
||||
|
||||
* ExecutionResult,
|
||||
* trace,
|
||||
* Program,
|
||||
* and actual Store content.
|
||||
|
||||
4. **Non-repudiation**
|
||||
|
||||
* By itself, `TraceDAGValue` does not prove that a run occurred in any particular environment; it is just data.
|
||||
* Non-repudiation requires certification and policy layers (`FER/1`, `FCT/1`, `CIL/1`).
|
||||
|
||||
---
|
||||
|
||||
**End of `PEL/TRACE-DAG/1 v0.2.1 — DAG Execution Trace Profile`**
|
||||
|
||||
---
|
||||
|
||||
## Document History
|
||||
|
||||
* **0.2.1 (2025-11-16):** Registered as Tier-1 spec and aligned to the Amduat 2.0 substrate baseline.
|
||||
Loading…
Reference in a new issue