Skip to content

Commit eeb94f8

Browse files
authored
Merge branch 'dev' into 487-participant-invariant-oracle
2 parents dbd1242 + 47993c1 commit eeb94f8

11 files changed

Lines changed: 2510 additions & 5 deletions

File tree

changelog.d/485.added.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
Added an assurance fulfillment gate (`specs/formal/assurance-fulfillment.yaml`, enforced by `tools/check_assurance_policy.py` via `nox -s policy`): every classified formal-spec subsystem must deliver — or explicitly waive with an ISO date and tracking reference — each verification artifact kind required by its FM level, so a subsystem can no longer be classified FM3 with no executable artifacts while CI stays green.

changelog.d/486.changed.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
Added executable participant-runtime invariant oracle evidence for ADR-054 / ASR-505.
Lines changed: 131 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,131 @@
1+
# Issue 485 Assurance Fulfillment Preflight
2+
3+
Date: 2026-06-13
4+
5+
Issue: #485.
6+
7+
Requirement: none. The issue title, body, and acceptance criteria are the
8+
contract.
9+
10+
This note records architecture preflight guardrails for adding the assurance
11+
fulfillment gate. It is guidance for the implementation and does not implement
12+
the checker, the fulfillment map, or the tests.
13+
14+
## Binding Sources
15+
16+
- ADR-007 defines the FM0-FM3 assurance ladder and required artifact kinds.
17+
- ADR-018 establishes `specs/formal/assurance-policy.yaml` and
18+
`tools/check_assurance_policy.py` as the canonical machine-readable policy
19+
seam.
20+
- `docs/explain/reference/fm-classification-ledger.yaml` is a per-change ADR
21+
classification ledger. It is related evidence, not the subsystem fulfillment
22+
map this issue requires.
23+
- `specs/formal/<domain>/` is the formal-domain artifact tree whose classified
24+
subsystems need delivered-or-waived fulfillment records.
25+
26+
## Architecture Decisions
27+
28+
- Fulfillment is a classified-formal-subsystem concern, not a per-change ADR
29+
concern. Keep it separate from `fm-classification-ledger.yaml` even if the
30+
checker reuses similar validation helpers.
31+
- Add one machine-readable fulfillment surface next to
32+
`assurance-policy.yaml`, preferably `specs/formal/assurance-fulfillment.yaml`
33+
unless extending `assurance-policy.yaml` keeps the shape clearer. If a sibling
34+
file is used, it must carry `policy_ref: specs/formal/assurance-policy.yaml`
35+
and ADR-007 / ADR-018 references.
36+
- Make the "classified subsystem" set explicit and data-driven. The artifact
37+
should distinguish the subsystem registry (`id`, `path`, `fm_level`) from the
38+
fulfillment map keyed by subsystem id; the checker can then fail when a
39+
classified subsystem has no fulfillment entry without hard-coding the current
40+
list in Python.
41+
- Derive required artifact kinds from `assurance-policy.yaml` by FM level.
42+
Do not duplicate the FM3 artifact list in the fulfillment schema, tests, or
43+
docs.
44+
- Treat status as a per-required-artifact-kind value:
45+
`delivered` requires at least one concrete non-empty repo-relative path, and
46+
`waived` requires an ISO date plus at least one tracking reference.
47+
- The current issue contract names these classified subsystems: delivered
48+
`workflows`, `planner`, `assessment`, `objectives`, `experiment-core`;
49+
waived `participant-runtime`, `participant-semantics`, and `realization`.
50+
`runtime-contracts` is also a formal domain; do not silently include or omit
51+
it. Either include it if the chosen classified-subsystem registry treats it as
52+
classified, or make the registry's boundary explicit.
53+
54+
## Required Incumbents
55+
56+
- Reuse `tools/check_assurance_policy.py`; do not add a second policy CLI or
57+
nox session.
58+
- Reuse `tools.policy.common.PolicyFailure`, `failures_to_json`,
59+
`load_exceptions`, `apply_exceptions`, and `safe_repo_path`.
60+
- Extend `implementations/python/tests/test_assurance_policy.py` using the
61+
existing temp-repo seeding and mutation style.
62+
- Keep `nox -s policy` as the workflow entrypoint through the existing
63+
`noxfile.py` policy session.
64+
- Keep ADR-007, ADR-018, `docs/specs/formal.md`, and
65+
`docs/explain/reference/coding-standards.md` as policy consumers; do not
66+
weaken accepted ADR text in place without the ADR-059 amendment and pin gate.
67+
68+
## Cross-Cutting Layers
69+
70+
- YAML/config parser: use `yaml.safe_load` and explicit mapping/list/string
71+
shape checks. Never evaluate YAML content or coerce malformed fields into
72+
empty structures that let checks pass.
73+
- Repo-path security: every path from the fulfillment file must be
74+
repo-relative, non-escaping, and resolved through `safe_repo_path` or the same
75+
invariant. Absolute paths, `..`, and symlink escapes must fail.
76+
- Artifact existence: a delivered artifact must point to concrete evidence that
77+
exists and is non-empty. A domain README can satisfy an artifact kind only
78+
when the map deliberately names that README for that kind; it must not be a
79+
blanket substitute for missing executable or model artifacts.
80+
- Waiver authority: fulfillment waivers are first-class records in the
81+
fulfillment map. `tools/policy/exceptions.yaml` remains only for policy-gate
82+
exceptions and must not become the FM gap tracker.
83+
- Error envelope: all failures should be `PolicyFailure` instances and respect
84+
the existing `--json` output. Do not add a new exception hierarchy or raw
85+
traceback output.
86+
- Workflow gate: the new validation must run through the existing assurance
87+
policy checker so `nox -s policy` and `verify` fail on invisible gaps.
88+
- Secret and host exposure: this design should not read secrets, environment
89+
bindings, auth tokens, or network state. Tracking refs are issue identifiers,
90+
not credentials or live GitHub lookups, and no token should appear in process
91+
argv, logs, JSON output, or policy failure messages.
92+
93+
## Extension Boundary
94+
95+
The extension seam is the policy YAML plus the classified-subsystem registry:
96+
97+
- adding an FM4 derives its required artifacts from `assurance-policy.yaml`;
98+
- adding an artifact kind requires one policy-level YAML addition and
99+
fulfillment entries for classified subsystems at levels that inherit it;
100+
- adding a formal subsystem requires one registry entry plus one fulfillment
101+
map entry, and omission of either side should fail the gate;
102+
- adding more waiver evidence should extend a list of tracking refs or
103+
evidence refs, not add ad hoc waiver fields.
104+
105+
## Gotchas And Anti-Patterns
106+
107+
Avoid:
108+
109+
- conflating ADR-level classification fulfillment with formal-domain
110+
subsystem fulfillment;
111+
- hard-coding the current subsystem list or FM3 artifact list in Python when it
112+
can be derived from YAML;
113+
- using `tools/policy/exceptions.yaml` to hide known FM gaps;
114+
- marking participant-runtime or participant-semantics delivered just because
115+
a README contains design prose while the issue calls out missing executable
116+
abstract models;
117+
- accepting empty files, empty directories, absolute paths, parent traversal,
118+
or paths outside the repo as delivered evidence;
119+
- adding a new nox session, new policy failure type, duplicate YAML parser,
120+
duplicate waiver schema, or duplicate test harness;
121+
- editing accepted ADR-018 in place for this issue without following ADR-059.
122+
123+
## Non-Goals
124+
125+
- Implementing the fulfillment checker, tests, or YAML contents in this
126+
preflight note.
127+
- Delivering the missing participant-runtime, participant-semantics, or
128+
realization formal artifacts.
129+
- Reclassifying FM levels or changing ADR-007's required artifacts.
130+
- Adding API, auth, persistence, logging, schema-generation, or runtime
131+
behavior.

docs/explain/reference/fm-classification-ledger.yaml

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -386,11 +386,10 @@ entries:
386386
path: implementations/python/tests/test_runtime_control_plane.py
387387
- kind: typed_ir_or_contract_coverage
388388
path: implementations/python/tests/test_runtime_contracts.py
389-
waived_artifacts:
390389
- kind: property_based_or_differential_tests
391-
rationale: Historical backfill records current evidence; no dedicated property-based or differential artifact was recorded for this accepted ADR.
390+
path: implementations/python/tests/test_participant_runtime_invariants.py
392391
- kind: abstract_state_machine_model
393-
rationale: Historical backfill records current evidence; no abstract state-machine artifact was recorded for this accepted ADR.
392+
path: implementations/python/tests/test_participant_runtime_invariants.py
394393
- adr: ADR-055
395394
surface: Experiment core contract boundary
396395
fm_level: FM2

docs/specs/formal.md

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,12 @@ The canonical mapping is
3131
which is the structural source of truth and gates CI via
3232
`tools/check_assurance_policy.py`.
3333

34+
Whether each classified domain above actually fulfills the artifact kinds its FM
35+
level requires — delivered, or explicitly waived with an ISO date and tracking
36+
reference — is recorded per subsystem in
37+
[`specs/formal/assurance-fulfillment.yaml`](../../specs/formal/assurance-fulfillment.yaml)
38+
and gated by the same checker.
39+
3440
| Level | Scope | Required artifacts |
3541
|-------|-------|--------------------|
3642
| FM0 | Structural (parsing, schema, local validation) | Unit tests |

0 commit comments

Comments
 (0)