ASR-535 — Participant Information-Flow And Relation Assurance

[Brad-Edwards]

Requirements

• ASR-535

Bounded outcome

Add falsifiable assurance and backend conformance for participant information-flow/control claims without promoting finite evidence into universal relations.

Non-goals

• Mandatory universal noninterference, equivalence, simulation, refinement, or bisimulation proof.
• A separate conformance runner, report family, relation registry, or proof vocabulary.
• Treating schema validity or capability declarations as runtime realization.

Dependencies

• Assess and design formal participant I/O control with information-flow and bisimulation semantics #794
• SEM-230 — Participant Information-Flow And Control Semantics #796 (SEM-230)
• RUN-319 — Participant Information-Flow Policy Enforcement #799 (RUN-319)
• Declare participant I/O policy capability and realization support (API-407) #801 (API-407 capability declarations)

Acceptance criteria

• Cover denial, withholding, redaction, governed declassification, transformation, stale/revoked policy, cross-participant leakage, participant-directed inject delivery, backend weakening, and unsupported capability.
• Bind every report to the exact relation, participant/projection/policy revision, quantifiers, model/case boundary, time/order and scheduler/environment assumptions, assurance state, evidence, limitations, and explicit nonclaims.
• Reuse BackendConformanceReport and existing fixture/target runners; include adversarial overclaiming targets.
• Model-check/proof claims name their model, bound or universal domain, tool/version, artifact digest, assumptions, counterexamples, and reproducibility procedure.
• Update the participant section of docs/explain/sdl/lineage.md with this issue's adopted intellectual lineage, exact ACES artifact mappings, delivery status, evidence links, and explicit nonclaims; update contracts/provenance/sdl-lineage-ledger-v1.json and its source audit only when normative derivation or compatibility claims change.

Required assurance evidence

• Negative and property tests.
• Bounded model-check artifacts where claimed.
• Adversarial backend probes and conformance reports with finite scope and nonclaims.
• Behavioral-relation policy and scientific-completeness reconciliation.

Parent program: #794.

[Brad-Edwards]

ASR-535 now has explicit follow-on ownership for previously optional or missing assurance surfaces: #810 owns opacity design, #811 must create a downstream mandatory machine-checkable bisimulation result for one selected theorem target, #812 owns intentional-subversion/adaptive-control evaluation design, and #813 owns cross-backend demonstration design. ASR-535 finite tests and bounded conformance remain nonproofs; proof or opacity status may advance only from the artifacts created under the new requirement-backed programs.

[Brad-Edwards]

🛠️ Picked up by /implement - driver claude-code, branch 800-participant-flow-assurance, 2026-07-28T04:03:00.084Z.

[Brad-Edwards]

gc workflow phase recorded: preflight (issue #800). Posted by the MCP server to enforce ordering between workflow steps (issue #794 MVP-2). Do not edit or delete — used by downstream tools to gate phase prerequisites.

[Brad-Edwards]

gc workflow phase recorded: plan (issue #800). Posted by the MCP server to enforce ordering between workflow steps (issue #794 MVP-2). Do not edit or delete — used by downstream tools to gate phase prerequisites.

ASR-535 implementation plan

Branch 800-participant-flow-assurance. All workflow commands run with
RAES_REQUIREMENT_UID=ASR-535 (the branch carries no UID).

Framing

The preflight note
(docs/decisions/issue-800-asr-535-participant-information-flow-relation-assurance-preflight.md)
is binding. The required architecture already exists; ASR-535 composes it. No new
ADR, report family, relation registry, proof vocabulary, runner, store, or
exception hierarchy is introduced.

Formal-lane decision (explicit). ASR-535 makes no model-check and no proof
claim. policy-noninterference keeps proof_status: deliberately-unproved.
Exhaustive enumeration over a declared finite domain is recorded as finite
falsification evidence (evidence_scope: finite, quantifier_scope: finite-cases), never as model-checked. The proof-bearing target stays owned by
#811; opacity by #810; adversarial-control evaluation by #812; cross-backend
demonstration by #813. Acceptance criterion 4 is therefore satisfied by making
no such claim and saying so in the catalog, the report claim, and lineage.

Four assurance lanes, kept independent

1. Semantic falsification — the SEM-230 test-local model, extended with
   negative-leakage/declassification property and exhaustive bounded-enumeration
   cases. Refutes a bounded model only.
2. Runtime enforcement — probes drive the real RuntimeControlPlane,
   ParticipantCrossingPolicyResolver, authenticated identity/subject binding,
   RUN-319 mediation, capability admission, append-only store, and the
   action/egress/control/inject boundaries.
3. Backend conformance — the existing target runner drives a named target
   through that same boundary and reports declared versus effective strength.
4. Formal verification — deliberately not entered (see above).

No lane promotes another; each carries its own assurance status and boundary.

Production changes

raes_conformance/conformance/participant_policy_probes.py (new).
Backend-neutral participant-policy probe harness plus the finite case set. A
positive API-407 participant-policy declaration with no harness supplied
yields an unsupported, non-passing case — never a silent skip or pass.
_UnavailableConformanceCrossingPolicyResolver is never positive evidence.

conformance/target.py + _TargetConformanceOptions. The single extension
seam: an injected participant_policy_harness option consumed by
run_target_conformance() / _known_profile_report(). No backend name or
feature id becomes a dispatch branch.

conformance/report.py. Extend ConformanceCaseResult in place so the
issue-#800 coordinates are machine-reviewable rather than encoded in case names:
taxonomy/relation revision; participant, audience, episode or declared
cross-episode memory scope; projection ref/revision; policy id, revision,
decision ref, state-cut ref, declassification schedule; left/right carrier refs
for the varied high/low pair; quantifier scope; a closed assumptions record
(order model, scheduler class, environment class, nondeterminism, termination,
progress, timing, probability, partial order); counterexample ref; assurance
status. backend_conformance_report_payload() projects them.

Add one cross-field validation seam run before serialization/persistence:
validates the claim against the catalog, requires every claimed case to be
present (including failed, unsupported, and counterexample cases), rejects a
universal quantifier backed only by finite evidence, and blocks
native_conformance or a stronger assurance status from being inferred from
fixture-only or hermetic evidence. Report-level relation stays
bounded-probe-success; a policy case may reference the
policy-noninterference obligation it attempts to falsify without changing the
report's relation.

Diagnostic-leak repair (defect found by preflight).
conformance/validators.py, target.py, target_probes.py, semantics.py,
participant_execution_probes.py, and time_semantics.py concatenate raw
str(exc) into Diagnostic.message. For a Pydantic ValidationError that
carries input_value, so rejected participant/policy payload content can reach
a persisted report. Generalize the existing profiles.py::_sanitize_load_error
pattern into a shared sanitizer in conformance/diagnostics.py and apply it at
every report-bound site, repointing profiles.py at the shared helper. Fixing
this is a precondition for routing policy/backend failures into reports.

Finite obligations covered (acceptance criterion 1)

denial · withholding · redaction · governed declassification · transformation ·
stale/revoked policy · cross-participant leakage · participant-directed inject
delivery · backend weakening · unsupported capability · adversarial overclaim.

Each adversarial fixture injects exactly one prohibited behavior behind the
real RuntimeTarget/RuntimeControlPlane/store boundary — no dishonest mode is
added to a production backend and the gate under test is never monkeypatched.
Every negative case asserts semantic refusal and side-effect boundaries:
portable snapshot/store history, participant-visible result, backend call
ledger, audit event, and report claim. A denied case that still called the
backend or serialized a hidden value fails.

Tests (TDD, red first)

• implementations/python/tests/test_asr_535_participant_flow_assurance.py —
  the eleven obligations, overclaim detection, report cross-field binding,
  claim-strength rejection, and diagnostic sanitization (a rejected payload must
  not reach a report).
• Negative-leakage and declassification property/counterexample cases plus
  exhaustive bounded enumeration over sem230_information_flow_model, reported
  with explored-case counts and counterexample refs as finite evidence.
• Adversarial single-fault targets/resolvers as test fixtures.

Governance reconciliation

• contracts/concept-authority/behavioral-relations-v1.json (and its
  byte-identical fixture contracts/fixtures/concept-authority/behavioral-relations-v1/valid/reference.json):
  advance policy-noninterference.assurance.implementation_status from
  not-implemented to implemented — RUN-319 shipped reference-runtime
  enforcement — with evidence refs; add the ASR-535 bounded evidence entry; keep
  test_status: bounded and proof_status: deliberately-unproved; add the
  explicit nonclaim that ASR-535 finite and bounded-conformance evidence is not
  proof and that Design participant-relative opacity and supervisor-observation security semantics #810–Design cross-backend participant control against simulation and cyber-range precedents #813 own any stronger status. The published schema shape
  is unchanged, so no schema-publication last_change entry is due.
• specs/formal/assurance-fulfillment.yaml — record the ASR-535 delivered
  artifacts under the participant-semantics FM3 subsystem.
• contracts/profiles/scientific-completeness/delivery-assessment-*.json —
  attach ASR-535 evidence to participant-action-observation,
  portable-behavior-contracts, and behavioral-relation-taxonomy without
  promoting any concern's status on the strength of finite evidence.
• docs/explain/reference/backend-conformance.md — document the
  participant-policy harness seam and its evidence boundary.
• docs/explain/sdl/lineage.md, participant section — ASR-535 adopted
  lineage, exact ACES artifact mappings, delivery status, evidence links, and
  explicit nonclaims. contracts/provenance/sdl-lineage-ledger-v1.json and its
  source audit are not changed: ASR-535 adds evidence, not a normative
  derivation or compatibility claim.

Security, maintainability, extensibility, whole-repo view

• Security — deny-first independent gates with NOT_APPLICABLE at a
  required gate treated as unresolved rather than permit; exact state-cut
  binding so stale/revoked policy and post-advance replay fail closed;
  participant/audience binding checked before serialization; sanitized
  diagnostics; the shared redaction_violations() gate before any durable
  write, via the root-confined run-id path and atomic writer; no secrets,
  policy bodies, hidden state, or payloads in argv, env, filenames, or logs.
  Default probes are hermetic — no network, daemon, socket, or privilege.
• Maintainability — reuses BackendConformanceReport,
  ConformanceCaseResult, BehavioralClaimBindingModel,
  _bounded_conformance_claim(), run_fixture_suite(),
  run_target_conformance(), resolve_participant_feature_support(),
  ControlPlaneStore.commit_participant_transition(), Diagnostic, and the
  existing report serializer.
• Extensibility — another policy model, memory scope, order model,
  scheduler/environment class, crossing kind, target, or observer plugs into the
  harness and case policy without editing the conformance engine.
• Whole-repo view — repo policy, requirement governance, behavioral-relation
  claim policy, SDL lineage policy, concept-authority/fixture parity,
  generated-schema parity, docs build, and tools/verify_all.py all see these
  artifacts. Prose in scanned roots binds relation identity plus an evidence
  boundary, or is stated as an explicit nonclaim, so
  tools/check_behavioral_relation_claims.py stays green on merit.

No CHANGELOG.md edit and no version edit. PR title will be a valid
Conventional Commit that passes tools/check_pr_title.py.

Completion gates

RAES_REQUIREMENT_UID=ASR-535 with
implementations/python/.venv/bin/python tools/check_repo_policy.py,
tools/check_requirement_governance.py, tools/verify_all.py, then the
configured nox -s verify and make policy.

[Brad-Edwards]

gc_codex_review — cycle 1 of 1 (pre-push) on issue #800 (branch 800-participant-flow-assurance)
Diff mode: inline — the complete diff was supplied in one prompt

Core review

Verdict: don't-ship

The intended shape is sound: extend the incumbent target runner and report family, preserve bounded-probe-success, inject a typed policy harness, and centralize durable-diagnostic sanitization. Two load-bearing boundaries are nevertheless self-attested rather than enforced: the harness can substitute a reference stub for the named target, and per-case relation coordinates bypass the canonical behavioral-claim authority. As written, the report can describe target-backed, catalog-bound conformance without either fact being true; this also breaks the obvious next variation of evaluating another backend through the same seam.

Blocking findings (2):

1. [one-off] The probe harness can pass without exercising the report target — implementations/python/packages/raes_conformance/conformance/participant_policy_probes.py:357
participant_policy_cases() delegates execution entirely to no-argument observe callbacks and independently verifies neither the target used nor the returned side-effect ledger. The supplied ASR-535 harness demonstrates the failure: cases() discards the RuntimeTarget, every probe constructs a separate fixture control plane or stub target, and the shared observation helper hard-codes history_mutated=False while inferring backend invocation indirectly from behavior history. A backend named by run_target_conformance() can therefore receive passing exact-support cases without ever being called. Make the runner bind operations and observations to the supplied target and derive the release, invocation, mutation, and audit facts from runner-owned state or call ledgers.
2. [one-off] Participant policy bindings bypass the canonical claim authority — implementations/python/packages/raes_conformance/conformance/report.py:29
ParticipantPolicyBinding recreates taxonomy, relation, quantifier, evidence-scope, and assurance-status fields as unconstrained strings. validate_backend_conformance_report() validates only report.claim, while serialization publishes every case binding verbatim; _unprobed_binding() already emits the invented relation id capability-declaration. This contradicts the one-claim-authority design and permits malformed or non-catalog relation claims in durable reports. Represent these coordinates through BehavioralClaimBindingModel, or add catalog-backed validation for every case binding at the report seam and define unsupported capability without inventing a behavioral relation.

Security review

Verdict: don't-ship

The change appropriately extends the existing conformance runner and report family and centralizes diagnostic sanitization. However, the new participant-policy seam delegates both execution and observation to an unbound callback, so the report cannot establish that the backend named by the report was exercised. That breaks the security-assurance boundary at its load-bearing seam and allows the new evidence and implementation-status claims to overstate backend enforcement.

Blocking findings (2):

1. [one-off] Policy probes can certify a backend they never execute — implementations/python/packages/raes_conformance/conformance/participant_policy_probes.py:95
   Attacker model: a backend under conformance evaluation that correctly handles the ordinary adapter probes but omits or weakens participant information-flow enforcement. The probe contract accepts a zero-argument observation callback, and the supplied ParticipantPolicyConformanceHarness discards the RuntimeTarget passed to cases() and constructs separate stub RuntimeControlPlane instances. The runner then trusts the callback's self-reported declared/effective strength and side-effect ledger. Consequently, the evaluated backend's participant-policy implementation is never called: it can leak participant data or execute denied actions while receiving passing policy cases based on the reference stub. The ledger further infers backend invocation from behavior-history changes and hardcodes history_mutated=False, so even a callback made against the target would not reliably detect backend calls or rolled-back side effects. Fix the seam so the runner owns target-bound execution and derives observations from the supplied target, its call ledger, and before/after store state. Bind each result to the target/profile/execution basis and reject callbacks that cannot demonstrate that binding. The regression test should use an instrumented or adversarial RuntimeTarget and assert that its participant runtime was actually invoked or refused as required.
2. [one-off] Sanitizer persists attacker-controlled validation keys — implementations/python/packages/raes_conformance/conformance/diagnostics.py:39
   Attacker model: a producer of malformed conformance input whose rejected payload is more restricted than the persisted report's readership. Pydantic includes an unknown extra-field key in ValidationError.loc. This line treats any alphanumeric, underscore, dot, or hyphen segment up to 64 characters as safe and echoes it into the diagnostic. A credential, participant identifier, or other sensitive value placed in an object key matching that grammar therefore survives sanitized_failure_message and is serialized into BackendConformanceReport, despite the stated guarantee that rejected input is never copied into durable diagnostics. The current regression covers a secret as a value, not as the field name that reaches loc. Do not trust string locations based on character shape: either render only error counts/types and numeric indexes, or retain a segment only after verifying it against the validated model's schema and redact every unknown/extra key. Add a regression with the secret marker used as an extra-field name.