amduat/tier1/fer-1.md

184 lines
5.9 KiB
Markdown
Raw Permalink Normal View History

2026-02-22 00:25:56 +01:00
# FER/1 — Execution Receipts and Evidence (Core Semantics)
Status: Draft
Owner: Architecture
Version: 0.1.0
SoT: Yes
Last Updated: 2026-02-21
Linked Phase Pack: PH07
Tags: [evidence, receipt, deterministic, execution]
**Document ID:** `FER/1`
**Layer:** L2 — Evidence receipts over PEL/1 execution
**Depends on (normative):**
* `ASL/1-CORE v0.4.x` — value model (`Artifact`, `Reference`)
* `PEL/1-SURF v0.2.x` — surface execution results
* `TGK/1-CORE v0.7.x` — trace graph kernel
* `ENC/FER1-RECEIPT/1` — canonical receipt encoding
* `DDS` (FER/1 layout and validation rules)
---
## 0. Purpose & Scope
`FER/1` defines **receipt semantics** for deterministic execution evidence. It
standardizes the logical fields of execution receipts and the minimal execution
artifacts that higher layers can rely on, while delegating concrete encodings to
`ENC/FER1-RECEIPT/1` and DDS.
`FER/1` does **not** define policy, intent, authority, or certification rules
(those belong to `FCT/1` and higher layers).
---
## 1. Core Concepts
### 1.1 Execution Artifacts (logical schemas)
`FER/1` uses four logical artifact shapes. Each is an ASL/1 `Artifact` whose
encoding is profile-defined (not specified here).
**ExecutionIntent** — records the inputs and environment for a run:
```
ExecutionIntent {
function_ref : Reference // FCS/1 descriptor or equivalent
program_ref : Reference // program artifact (scheme-specific)
input_manifest_ref : Reference // GS/1 manifest (ordered, deduped)
params_ref : optional Reference
snapshot_id : uint64 // snapshot identity (0 if absent)
execution_config_ref : optional Reference // snapshot-scoped config
environment_ref : Reference // environment capsule (ICD/1 / PH03)
}
```
**ExecutionOutput** — binds outputs to a run (used when outputs are multiple or
need explicit naming):
```
ExecutionOutput {
output_refs : list<Reference> // ordered
result_ref : Reference // surface ExecutionResult artifact
trace_ref : optional Reference
}
```
**ExecutionReceipt** — evidence of a run (canonical encoding in
`ENC/FER1-RECEIPT/1`):
```
ExecutionReceipt {
function_ref : Reference
input_manifest_ref : Reference
environment_ref : Reference
evaluator_id : bytes
output_ref : Reference
executor_refs : list<Reference>
parity_entries : list<ParityEntry>
started_at : uint64
completed_at : uint64
// optional fields per FER/1 v1.1 (DDS): executor_fingerprint, logs,
// determinism_level, rng_seed, limits, parent, context, witnesses, run_id,
// signature, signature_ext
}
```
**ExecutionObservation** — optional, typed evidence produced alongside a run:
```
ExecutionObservation {
kind : enum // e.g. stderr, stdout, metrics, trace
payload_ref : Reference // artifact containing the observation payload
payload_sha256 : bytes[32]
}
```
### 1.2 Program and input conventions
* `function_ref` MUST reference the **function descriptor** used for evaluation
(e.g., FCS/1 descriptor).
* `program_ref` MUST reference the program artifact used by that descriptor.
* `input_manifest_ref` MUST reference a **canonical manifest artifact** that
enumerates inputs in deterministic order.
* `params_ref`, when present, MUST be an immutable artifact included in the
input manifest.
### 1.3 Snapshot binding
All receipts are **snapshot-bound**:
* `snapshot_id` in the intent MUST be the snapshot identity used for input
resolution (0 when absent).
* Receipts and outputs are interpreted relative to that snapshot.
---
## 2. Output Reference Fallback
`ExecutionReceipt.output_ref` is a single reference. The value MUST resolve as:
1. The sole output artifact, **if the run produces exactly one output**; or
2. An `ExecutionOutput` artifact when there are multiple outputs; or
3. The surface `ExecutionResult` artifact, **only** if outputs are empty and
the result is the only durable artifact.
This rule keeps receipts stable while supporting multi-output runs and
zero-output executions.
---
## 3. TGK Traceability Edges (FER/1 profile)
When ingesting receipts, a `TGK/FER/1` profile SHOULD emit traceability edges
using TGK edge artifacts. Edge type assignments are defined by the profile; the
semantics are:
* `EDGE_EXECUTION`: `program_ref -> output_ref`
* `EDGE_CONSUMED_BY`: `input_ref -> output_ref`
* `EDGE_PRODUCED_BY`: `output_ref -> receipt_ref`
* `EDGE_REALIZES`: `receipt_ref -> function_ref`
* `EDGE_OBSERVED_BY`: `output_ref -> observation_ref` (optional)
Edges MUST be derivable solely from receipt content and referenced artifacts.
---
## 4. Determinism & Validation (FER/1 v1.1)
`FER/1` v1.1 receipts are **parity-first** and deterministic. Implementations
MUST enforce the DDS validation rules, including:
* Strict TLV order and no unknown tags.
* `executor_set` and `parity_vector` ordered byte-lexicographically and aligned.
* `parity_entries[i].output_ref` equals the top-level `output_ref`.
* `started_at <= completed_at` and monotonic time envelope.
* Determinism level defaults to `D1_bit_exact`; any other level requires an
explicit `rng_seed`.
* `run_id`, when present, MUST equal the deterministic hash over
`{function_ref, input_manifest_ref, environment_ref, executor_fingerprint}`.
* Receipts MUST NOT encode policy, intent, or authority metadata.
The canonical binary layout for receipts is defined in
`ENC/FER1-RECEIPT/1` and DDS.
---
## 5. Interactions
* `PEL/1-SURF` provides the surface `ExecutionResult` artifact referenced by
`ExecutionOutput.result_ref`.
* `FCT/1` binds policy, authority, and certification to one or more FER/1
receipts.
---
## 6. Conformance
An implementation is **FER/1conformant** if it:
* Produces receipts that validate under `ENC/FER1-RECEIPT/1` and DDS rules.
* Uses the output reference fallback rules in §2.
* Emits TGK edges (when enabled) that are derivable from receipt content.