niklas/amduat
1
0
Fork 0
Code Issues Pull requests Actions Packages Projects Releases Wiki Activity
amduat/tier1/pel-1-core.md
Carl Niklas Rydberg 4dae7a32d2 Add PEL tier1 specifications
2025-12-20 12:35:10 +01:00

20 KiB
Raw Blame History

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]

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:

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:

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:

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:

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.

ExecutionStatus    = uint8
ExecutionErrorKind = uint8

ExecutionStatus codes:

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:

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:

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:

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:

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 Artifacts.
    • 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:

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:

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:

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

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 References,
    • 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 ExecutionResultValues), potentially with:

    • failing References,
    • 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:

      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.