Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
81 changes: 81 additions & 0 deletions docs/decisions/issue-1357-v2-governed-admission-preflight.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,81 @@
# Issue #1357 — v2 governed admission preflight

Scope: the public Python `admit_participant_decision_surface_selection_v2()`
entry point. The GitHub issue is the contract. This note records boundaries for
implementation; it does not change runtime behavior or ADR-095 semantics.

## Architecture decision

The v2 selection binder owns agreement with the delivered surface; ordinary
participant-action admission owns caller and ingress-crossing authority. Keep
that sequence. Forward the caller's original identity and crossing evidence
through the v2 entry point to `admit_participant_action()` together with the
bound request and existing retry context. The v1 selection entry point and
`ParticipantSubmissionOptions` already provide the submission-context pattern.
The v2 path currently forwards only `idempotency_key` and
`request_fingerprint`, so a configured governed ingress cannot receive the
identity and evidence that ordinary admission requires. Keep one canonical
submission-options vocabulary and shape check; do not create a v2 authority DTO.

`ParticipantActionAdmissionRequest` is the backend-neutral action request, not
the caller's authenticated identity or crossing evidence. The v2 selection is
a participant choice bound to a surface id, decision epoch, view digest and
delivery ref; it grants no new authority. The surface's derivation cut and
delivery cut are distinct from the fresh ingress crossing cut. Preserve their
participant/episode, action, audience, policy and occurrence identities through
the existing validators. Neither a selected action nor a delivery record may
synthesize caller authority, required evidence or a crossing occurrence.

## Cross-cutting boundaries

| Layer | Existing owner and required behavior |
| --- | --- |
| Published shape and proposal | `contracts/schemas/control-plane/participant-decision-surface-v2.json`, `raes_contracts.contracts.participant_decision_surface_v2`, `raes_contracts.participant_binding_v2` and `ParticipantActionAdmissionRequest` own surface/selection fields, agreement, apparatus resolution and governed argument-shape validation. Use their typed carriers and existing checks; no duplicate schema or parser. |
| Exact-cut and disclosure | `validate_participant_decision_surface_v2_anchor()` re-resolves the derivation anchor; `validate_participant_decision_surface_v2_delivery()` re-resolves authoritative delivery. ADR-095 and SEM-226 keep projection, disclosure, delivery, participant observation, selection and admission distinct. Never put assurance-only refs or crossing evidence in the participant-facing view. |
| Submission and authentication | `ParticipantSubmissionOptions.from_fields()` owns optional submission shape. `ControlPlaneIdentity` and `_require_crossing_identity()` own authenticated principal, target, role and exact participant/controller binding. A governed ingress requires the original typed identity; `operation_actor_scope(None)` denotes a trusted embedded process and must not replace a served caller. |
| Crossing and policy | `ParticipantCrossingEvidence` supplies caller-owned evidence metadata; `action_crossing_intent()`, `prepare_participant_crossing()`, `participant_crossing_policy`, `participant_flow_sink` and API-424 control mediation derive and validate the live occurrence, policy, evidence, capability, audience and final-sink decisions. Evidence refs are claims to check against trusted resolver context, not proof by presence. Unknown, stale, mismatched or unauthorized context fails closed. |
| State and effect | `RuntimeMutationAuthority`, `control_plane_mutation()`, `external_control_plane_call()`, `expected_participant_history_heads()`, the operation record and atomic store commit own serialized state cuts, re-entry fencing, replay and durable crossing/action history. Preserve the existing pre-mutation check and recheck under the mutation permit; do not dispatch a backend action before the governed decision and claim. |
| Failure and observation | `_participant_binding_diagnostic()`, `_reject_diagnostics()`, `OperationReceipt`, `operation_admission_context()` and crossing denial audit own the current rejection forms. Bind early rejections to the supplied actor where available, and keep audit details and returned diagnostics bounded and value-free. Do not wrap ordinary `PermissionError`/`ValueError` into a new exception hierarchy or expose raw evidence/policy payloads. |

The public v2 method is a Python control-plane API; the current HTTP adapter
does not expose this admission method. Thus no new HTTP request body, auth
dependency, error envelope, configuration or environment binding is in scope.
If an HTTP route is later introduced, it must use `ControlPlaneSecurityConfig`
and the existing API authentication and response machinery, with typed identity
coming from the auth dependency rather than the request body. This change
needs no credential lookup, secret value, subprocess argument or environment
variable. Do not pass identity or evidence through `argv`, logging, diagnostic
text or participant-visible serialization. Existing operation commitments and
audit records remain the persistence surface; no new journal or cache.

## Verification boundary and anti-patterns

The targeted v2 runtime test should show a valid delivered selection reaches
governed ordinary admission with the correct authenticated actor and crossing
occurrence, then reject absent identity/evidence, stale surface or crossing
cut, wrong participant/episode/action/audience/controller, and unauthorized
role/target/subject. Check that rejection leaves action/behavior history and
backend effects absent, except for the incumbent denial audit or crossing
record where that boundary intentionally records one. Reuse the existing
`participant_crossing_fixtures.py` resolver, identity and evidence fixtures
alongside `test_sem_220_participant_decision_surface_v2_runtime.py`; preserve
the mutation/concurrency and replay tests for the same path. Run only targeted
local checks under `.ground-control.yaml`, `.gc/plan-rules.md` and `noxfile.py`;
broad suites belong to CI. The published schema is governed by
`contracts/schema-publication-manifest.json` and
`tools/check_generated_schemas.py`; this forwarding change does not call for a
schema edit or a second contract artifact.

Do not copy RUN-319 crossing validation into the v2 binder, infer a controller
from the chosen action, use the decision epoch as policy order, treat the
delivery ref as ingress evidence, turn a rejected crossing into success, or
relax an existing validator to fit a forwarded value. The next submission
context variation belongs in the shared `ParticipantSubmissionOptions` seam
and then passes through both selection entry points and ordinary admission;
it should not require another v2-only options parser.

Non-goals: changing the v2 wire schema, ADR-095, v1 historical meaning,
participant projection or delivery rules, policy semantics, backend execution,
HTTP routing, secret/config handling, or store formats. A separate mixed-runtime
support change must resolve the current v2 target guard against the ordinary
action path's mixed-runtime guard before claiming mixed admission support.
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,10 @@ For each participant choice:
9. Accept a selection only when it binds surface id, decision epoch, canonical
participant-view digest, and delivery ref.
10. At admission, re-resolve the derivation anchor, delivery record, apparatus,
and existing participant-action constraints before writing behavior.
and existing participant-action constraints before writing behavior. Pass
the authenticated caller identity and, for governed ingress, the caller's
crossing evidence to the v2 admission method. The selection and delivery
record do not supply either authority or ingress evidence.

The reference entry points are:

Expand Down
155 changes: 155 additions & 0 deletions docs/research/formal-semantic-validation/analysis-v45.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,155 @@
{
"analysis_id": "issue-1357-analysis-v45",
"claim": {
"allowed_evidence": [
"production parser and semantic-validator results",
"canonical compiled digests",
"participant contract regression tests",
"pinned protocol, corpus, and execution snapshot"
],
"claim_id": "asr-530-formal-semantic-validation-retest",
"disallowed_evidence": [
"schema success as semantic proof",
"workflow reachability as network or exploit reachability",
"FM labels as gate outcomes",
"attribution as counterfactual proof",
"formal prose or maintainer confidence alone"
],
"evidence_artifacts": [
"docs/research/formal-semantic-validation/protocol-v2.json",
"docs/research/formal-semantic-validation/corpus/manifest-v4.json",
"docs/research/formal-semantic-validation/execution-snapshot-v45.json",
"docs/research/formal-semantic-validation/evidence/finite-domain-satisfiable-v4.json",
"docs/research/formal-semantic-validation/evidence/finite-domain-unsatisfiable-v4.json",
"docs/research/formal-semantic-validation/evidence/typed-exploit-path-valid-v4.json",
"docs/research/formal-semantic-validation/evidence/typed-exploit-path-invalid-v4.json"
],
"falsification_protocol": "Replay every retained and new case through its production entrypoint, require complete digest and evidence joins, execute participant fixtures, and derive status from the recorded outcomes.",
"objective_fail_criteria": "A supported negative passes, a positive fails, an observation drifts, a required participant case is missing, or weaker evidence is promoted to solver, exploit-path, runtime-stability, or counterfactual assurance.",
"objective_pass_criteria": "Every claim class has positive and negative cases, all supported cases reproduce the frozen outcome, every participant obligation has passing positive and negative fixtures, and unsupported classes remain untested.",
"statement": "At the recorded source-state digest, the retained RAES controls have the bounded statuses recorded here; historical releases are integrity evidence, not current replay evidence.",
"threats_to_validity": [
"The issue-specific corpus is intentionally small and does not enumerate every validator invariant.",
"The participant fixtures exercise reference production contracts and tests, not every independent backend realization.",
"The replay gate runs on one Python reference configuration and one pinned RAES revision.",
"Unsupported solver-level classes have protocol cases but no executable observations."
]
},
"claim_results": [
{
"case_count": 2,
"claim_class_id": "schema-validity",
"evidence_status": "demonstrated",
"limitations": [
"Bounded to the named source/model structural controls."
],
"matching_case_count": 2,
"participant_obligation_count": 0,
"replayable_case_count": 2,
"unsupported_case_count": 0
},
{
"case_count": 4,
"claim_class_id": "semantic-consistency",
"evidence_status": "partial",
"limitations": [
"Partial coverage of named static semantics and participant obligations, not universal consistency."
],
"matching_case_count": 4,
"participant_obligation_count": 7,
"replayable_case_count": 4,
"unsupported_case_count": 0
},
{
"case_count": 2,
"claim_class_id": "graph-reachability",
"evidence_status": "partial",
"limitations": [
"Partial workflow control-flow reachability only; not network, service, or exploit reachability."
],
"matching_case_count": 2,
"participant_obligation_count": 0,
"replayable_case_count": 2,
"unsupported_case_count": 0
},
{
"case_count": 4,
"claim_class_id": "constraint-satisfiability",
"evidence_status": "demonstrated",
"limitations": [
"Demonstrated only for raes-finite-domain-satisfiability-v1 and its pinned solver configuration."
],
"matching_case_count": 4,
"participant_obligation_count": 0,
"replayable_case_count": 2,
"unsupported_case_count": 2
},
{
"case_count": 4,
"claim_class_id": "exploit-path-validity",
"evidence_status": "demonstrated",
"limitations": [
"Demonstrated only for the admitted snapshot, typed graph, query, semantics, and bounded search profile."
],
"matching_case_count": 4,
"participant_obligation_count": 0,
"replayable_case_count": 2,
"unsupported_case_count": 2
},
{
"case_count": 2,
"claim_class_id": "determinism-stability",
"evidence_status": "partial",
"limitations": [
"Partial parse-to-compile repeatability only; runtime and backend determinism are untested."
],
"matching_case_count": 2,
"participant_obligation_count": 0,
"replayable_case_count": 2,
"unsupported_case_count": 0
},
{
"case_count": 2,
"claim_class_id": "counterfactual-necessity",
"evidence_status": "untested",
"limitations": [
"Untested because no governed intervention or ablation entrypoint ran."
],
"matching_case_count": 2,
"participant_obligation_count": 0,
"replayable_case_count": 0,
"unsupported_case_count": 2
}
],
"corpus_revision": "4.0.0",
"evidence_status": "partial",
"execution_id": "issue-1357-execution-v45",
"generated_at": "2026-09-24",
"limitations": [
"Satisfiability is limited to raes-finite-domain-satisfiability-v1 and its exact translation, theory, and Z3 configuration.",
"The subset-minimal unsatisfiable core is not a universal proof certificate.",
"Exploit-path results are limited to the admitted snapshot, normalized graph, query, transition semantics, and bounded search profile.",
"A valid path is not backend execution and an invalid path is not real-world non-exploitability.",
"The production exploit-path JSON loader permits duplicate keys; the research loader rejects them without claiming stronger production behavior.",
"Participant replay inherits the host environment and is not described as hermetic.",
"Counterfactual necessity remains untested.",
"Scoped observation demand is not a claim class in this preregistration and is not promoted to demonstrated by this retest.",
"EXP-732 provenance joins are verified by their dedicated regression suite; this retained corpus makes no universal run, apparatus, source, or augmentation assurance claim.",
"This retained corpus does not establish native backend attestation fidelity; materialization contract checks remain separate operational provenance, not experimental observations.",
"Capture admission and evidence-proof authority are verified by issue-1237 regression tests, not promoted to a new claim class by this retained corpus.",
"Evidence-requirement refinement lineage is outside this retained formal claim set; this retest refreshes integrated source provenance without promoting that feature to a formal claim.",
"Authoring-adapter transport behavior is outside this retained formal claim set.",
"Operational recovery observation and startup reconciliation are verified by their API-404 regression suite, not promoted to a new formal claim class by this retained corpus.",
"Single-owner store admission, immutable target/run scope, and provider shutdown ordering are verified by their API-404 CP-5 regression suite, not promoted to a formal claim by this retained corpus.",
"Mixed and staged trial admission is verified by its SEM-234/SCE-002/API-407 regression suite, not promoted to a new formal claim class by this retained corpus.",
"Offline control-plane maintenance, readiness, and bounded audit behavior are verified by issue #1186 runtime tests, not promoted to a formal claim by this retained corpus.",
"Issue #1187 control-plane crash/profile conformance and HTTP security changes are covered by their dedicated regression suite, not promoted to new claims by this retained corpus.",
"Issue #1189 profile declarations and capability admission are covered by dedicated runtime tests; the retained formal corpus does not execute control-plane profile composition.",
"Issue #1016 mixed-runtime coordination is covered by dedicated runtime tests; the retained formal corpus does not establish backend-native mixed realization, multi-controller coordination, IFC, or equivalence.",
"Issue #610's reconciliation demonstration harness is covered by its dedicated processor and CLI suite, not promoted to new claims by the retained language corpus.",
"Participant identity, organization ownership, and participant assignment are separated by issue #1338. This retained offline corpus does not establish participant autonomy, execution authority, live backend fidelity, or causal attribution.",
"This source replay includes issue #1357 governed v2 admission, which is tested by its dedicated runtime suite; this retained formal corpus makes no additional crossing-authorization claim."
],
"plain_language_outcome": "The retained formal semantic-validation corpus replays its existing obligations on the current implementation. Governed v2 decision admission is tested separately; this release adds no new authorization claim.",
"protocol_revision": "2.0.0"
}
Loading
Loading