Declare and validate backend participant-opacity realization

[Brad-Edwards]

Requirements

• SEM-231
• API-407
• ASR-535

Bounded outcome

Extend the incumbent API-407 participant-feature support pattern for the opacity profiles actually supported by the reference runtime in #964. Declare strength, required contracts, limitations, disclosures, and evidence; then add bounded backend conformance cases that distinguish declaration, native realization, and observed conformance.

Backend reports reference the shared SEM-231 profile and behavioral claim binding. They do not copy the relation, secret predicate, observer model, or possible worlds. Missing required contracts or evidence rejects selection; authorized weakening removes the stronger claim and records its audience-visible limitation.

Negative cases

• A manifest boolean or method presence is treated as opacity realization.
• The backend passes payload-redaction cases but leaks decisions, failures, timing, retries, or policy-change effects.
• A declared profile is never exercised and is reported conformant.
• Reference-runtime mediation is mistaken for backend-native realization.
• A bounded conformance run is promoted to a model check or proof.
• Secret values, policy bodies, participant memory, or raw witnesses enter reports, logs, argv, or diagnostics.

Evidence required

• Manifest/schema round trips and required-contract mapping for named opacity features.
• Positive and adversarial target cases with exact backend/profile/tool/environment digests.
• Separate backend-declaration, backend-realization, and backend-conformance claim bindings and explicit limitations.
• Safe counterexample/evidence refs and sanitized failure messages.

Explicit nonclaims

No universal backend opacity, mathematical proof, cross-backend equivalence, timed/quantitative opacity, or support beyond named profiles and executions. Capability declaration, runtime mediation, native realization, and bounded conformance remain independent states.

Dependencies

Blocked by #810, #961, #962, and #964.

[Brad-Edwards]

🛠️ Picked up by /implement - driver codex, branch 965-backend-participant-opacity, 2026-08-01T17:24:51.101Z.

[Brad-Edwards]

gc workflow phase recorded: preflight (issue #965). 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: preflight (issue #965). 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: preflight (issue #965). 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 #965). 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.

Implementation plan

1. Drive the API-407 contract change with failing tests.

   • Add issue-965 tests for the governed participant_predicate_opacity feature, backend-manifest v2 model/schema/fixture round trips, exact required-contract closure, below-exact limitations/disclosures/evidence, and stub/reference declaration parity.
   • Prove that feature-list membership, a boolean, a method, or an unexercised declaration cannot establish realization or conformance.

2. Publish the bounded declaration through incumbent authority surfaces.

   • Extend the controlled participant behavior vocabulary and manifest-authority mappings with one relation-assurance feature kept outside PARTICIPANT_RUNTIME_POLICY_FEATURES.
   • Generalize the evidence-required feature predicate once, update the reference backend’s bounded declaration and unsupported backend fixtures, regenerate the hand-governed backend-manifest schema, and record its publication hash/ledger entry.
   • Preserve historical behavioral-catalog/profile coordinates while advancing the current catalog/profile revision only as required for the three new backend assurance axes.

3. Extend the existing target conformance seam.

   • Add typed profile-bound opacity case inputs/measurements modeled on the participant-policy and realization-honesty harnesses; the runner instruments and invokes the target and owns every verdict.
   • Exercise paired secret/nonsecret cases over decisions/failures, action availability, delivery/omission opportunity, retry/replay, logical timing/order, policy/release effects, and external effects.
   • Hold runtime configuration fixed and include a dishonest backend case so RUN-319 mediation, target naming, method presence, or native-live cannot masquerade as backend-native realization.

4. Keep claim and report honesty generic.

   • Extend ConformanceCaseResult with the smallest generic collection of existing BehavioralClaimBindingModel values plus realization-owner and exact backend/manifest/profile/configuration/tool/environment/probe digests.
   • Construct and validate independent backend-declaration/declared/structural, backend-realization/realized, and backend-conformance/conformant/finite bindings while leaving the report relation bounded-probe-success.
   • Retain failed, unsupported, weakened, and counterexample cases; authorized weakening removes stronger claims and records an audience-visible limitation.

5. Protect the evidence boundary and document it.

   • Reuse sanitized diagnostics, the shared report validator/redaction gate, root-confined run-artifact path, and atomic writer. Add negative tests proving secrets, raw witnesses, exception text, host paths, environment dumps, policy bodies, and backend objects never reach reports or diagnostics.
   • Update ADR-099/backend-conformance and participant-opacity delivery documentation to describe the bounded native realization/conformance lane and explicit nonclaims; retain the preflight note as binding guidance.

6. Verify every clause and repository gate.

   • Run narrow issue-965, backend-manifest, conformance, claim, schema-generation, and persistence tests during TDD.
   • Before completion run RAES_REQUIREMENT_UID=SEM-231 implementations/python/.venv/bin/python tools/check_repo_policy.py, RAES_REQUIREMENT_UID=SEM-231 implementations/python/.venv/bin/python tools/check_requirement_governance.py, RAES_REQUIREMENT_UID=SEM-231 implementations/python/.venv/bin/python tools/verify_all.py, plus the configured completion and policy commands through the Ground Control gate.

Design checks

• Security: External manifests still pass bounded UTF-8 JSON parsing, Pydantic shape validation, governed vocabulary/contract checks, exact root-confined profile resolution, behavioral-claim validation, API-423 context validation, identity/audience gates where runtime mediation is exercised, sanitized diagnostics, redaction, and atomic persistence. Only allowlisted nonsecret coordinates are digested.
• Maintainability: Reuse ParticipantFeatureSupport, the canonical required-contract map, exact profile loaders, run_target_conformance, the existing report family, diagnostic sanitizer, and artifact writer. No second manifest, claim type, runner, report, registry, store, logger, endpoint, or exception hierarchy.
• Extensibility: The seam is parameterized by feature, exact profile revision/digest, support strength, realization owner, execution basis, backend/config/tool/environment identity, and finite case policy. Another profile or backend changes those values without another feature boolean or report family.
• Whole-repo view: Changes may span concept authority/history, runtime relation profiles/history, backend manifest dataclass/Pydantic/schema/fixtures/publication entry, reference/stub manifests, conformance runner/report/harness, operations persistence, focused tests, ADR/reference docs, package exports, and generated-schema/claim/concept/policy gates. CHANGELOG.md and the generated version file remain untouched.

[Brad-Edwards]

gc_codex_review — cycle 1 of 1 (pre-push) on issue #965 (branch 965-backend-participant-opacity)
Diff mode: manifest — the complete diff exceeded one prompt and was reviewed as 2/2 inline slice(s) (file-slices) covering 46/46 file(s)

Core review

Verdict: ship-with-fixes

Slice 1/2: Architecture-fit: the change sensibly extends the existing manifest, behavioral-claim, target-conformance, and profile-history seams rather than creating an opacity subsystem. Code-quality: the runner has the right broad separation between a typed harness and report validation, but two missing admission gates let the bounded declaration/conformance contract overstate what was actually exercised.

Slice 2/2: This slice cleanly advances the authority revision and defines the backend-opacity assurance seam around explicit, provenance-bound probe execution: declaration alone remains insufficient, while backend-native realization and bounded conformance are emitted only after the harness observes the runtime. The tests exercise the important negative paths—missing evidence/contracts, forged provenance, mediation, weakening, adversarial divergence, and report sanitization—without turning finite evidence into a universal claim. The shape leaves the obvious next variation (another backend/profile-specific harness) open without speculative abstraction.

Blocking findings (2):

1. [one-off] Reject a declared opacity capability when its harness yields no cases — implementations/python/packages/raes_conformance/conformance/participant_opacity_probes.py:315
   When a bounded participant_predicate_opacity declaration has a non-null harness whose cases() returns an empty tuple, this function returns no opacity case at all. _known_profile_report() then includes no failing opacity result and its all(...) check can pass, despite the declaration never having been exercised. Emit the existing explicit unsupported/non-passing case for an empty case set (and ideally reject it as an invalid harness) so a declared profile cannot disappear from the report.
2. [one-off] Bind each probe profile to the manifest's declared support constraint — implementations/python/packages/raes_conformance/conformance/participant_opacity_probes.py:203
   The runner verifies that case.manifest_digest matches the target manifest, but never verifies that case.profile_id@case.profile_revision is one of the manifest declaration's profile constraints. A harness can therefore submit and pass a different opacity profile while the report carries the declaration claim for a manifest whose bounded support is limited to another profile. Resolve and enforce the declared profile constraint before running the case, so declaration, realization, and conformance actually join on the same exact profile.

Security review

Verdict: ship

Slice 1/2: This slice adds a governed participant-opacity capability, revisioned profile lineage, and a backend-neutral conformance seam that separates declaration, realization, and finite conformance claims. The cross-cutting contract, manifest, profile, and reporting changes preserve the intended fail-closed validation boundaries; no concrete exploitable security regression is evident in this slice.

Slice 2/2: This slice completes the verification and assurance surface for a bounded backend participant-opacity capability: it updates revision expectations, adds adversarial conformance cases for observation mismatch, forged provenance, runtime mediation, weakened declarations, and report sanitization, and records the corresponding contract semantics. The design seam is the conformance harness versus the backend-native runtime; that separation supports the obvious next variation of additional backends or bounded profiles without expanding the declared claim. No concrete exploitable security issue is introduced in this slice.

No blocking findings.

[Brad-Edwards]

gc_codex_review pre-push cycle 1 of 1 complete for issue #965 on branch '965-backend-participant-opacity'. Posted by the MCP server to enforce the pre-push hard-cap-1 contract (issues #796, #804, #906). Do not edit or delete — used by the next gc_codex_review (uncommitted) invocation to count cycles.