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