184 lines
5.9 KiB
Markdown
184 lines
5.9 KiB
Markdown
# 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/1–conformant** 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.
|