Re-test formal semantic validation, satisfiability, and exploit-path claims

[Brad-Edwards]

Purpose

Re-run and extend the formal semantic-validation and reachability evidence gate from #168 after the missing whole-scenario satisfiability and exploit-path capabilities ship.

This issue is an evidence/retest gate, not the implementation owner for either capability.

Requirements

• ASR-530 — Claim Falsification And Evidence Gate

Blocked by

• Governed whole-scenario constraint satisfiability and solver evidence #826 — governed whole-scenario constraint satisfiability and solver evidence
• Typed exploit-path semantics and executable path analysis #827 — typed exploit-path semantics and executable path analysis

Test protocol

1. Preserve the issue Test protocol: formal semantic validation and reachability claims #168 protocol, corpus, snapshot, and analysis as immutable version 1 evidence.
2. Create a new protocol and corpus revision that retains every prior positive and negative case.
3. Add governed satisfiable and unsatisfiable whole-scenario cases using the production solver entrypoint.
4. Add valid and invalid exploit-path cases using the production typed attack-graph analyzer.
5. Replay schema, semantic, workflow-reachability, participant-obligation, and parse-to-compile determinism evidence to detect regressions.
6. Record exact commands, versions, configuration, witnesses or certificates, structured diagnostics, digests, and limitations in a new immutable snapshot.
7. Derive claim statuses from the recorded observations without promoting bounded evidence beyond its declared theory, graph semantics, entrypoints, or configuration.

Acceptance criteria

• Governed whole-scenario constraint satisfiability and solver evidence #826 and Typed exploit-path semantics and executable path analysis #827 are merged and their production entrypoints are used directly.
• Every supported positive control passes and every single-defect negative is rejected.
• Satisfiability results include reproducible model or unsatisfiability evidence.
• Exploit-path results include reproducible path witnesses or structured rejection evidence.
• Existing version 1 cases replay without unexplained drift.
• The evidence bundle integrity gate rejects missing joins, changed snapshots, unsupported promotion, and test-local substitutes.
• The resulting analysis records each claim as demonstrated, partial, untested, or refuted with explicit limitations.
• Documentation states what the new evidence does and does not establish.

Related

• Test protocol: formal semantic validation and reachability claims #168 — original evidence gate and immutable version 1 baseline
• Claim falsification and evidence gate (ASR-530) #162 — claim falsification and evidence gate
• Layered Validation And Admission Profiles (ASR-511) #258 — layered validation and admission profiles
• Validation Strength Disclosure (ASR-515) #259 — validation strength disclosure

[Brad-Edwards]

🛠️ Picked up by /implement — driver Claude Code, branch 828-retest-semantic-evidence, 2026-07-20T19:09:57Z.

[Brad-Edwards]

gc workflow phase recorded: preflight (issue #828). 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 #828). 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 #828). 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 #828). 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. Freeze and index coherent releases. Preserve every issue-168 v1 protocol, corpus, snapshot, analysis, and observation byte-for-byte. Replace independent latest-base/latest-supplement selection in tools/check_formal_semantic_validation.py with digest-pinned atomic release records discovered through tools/evidence_bundle_index.py; load and validate every indexed historical release, then select the highest coherent release only for the current result. Keep the existing historical rename accommodations confined to v1 and add no new digest exceptions.

2. Drive the integrity design with failing tests first. Extend implementations/python/tests/test_formal_semantic_validation.py before checker changes. Red tests will require: all historical releases are validated; protocol/snapshot/analysis/evidence SHA-256 pins are enforced; changed historical snapshots fail; missing, duplicate, dangling, or many-to-one case/command/observation/evidence joins fail; unselected evidence artifacts and test-local entrypoints fail; CLI-only labels cannot substitute for production service replay; unsupported or mismatched controls cannot be promoted; and analysis statuses are recomputed rather than copied from expected ceilings.

3. Add the immutable v2 retest corpus and production evidence. Add a v2 protocol and corpus under docs/research/formal-semantic-validation/ that retain every v1 case ID and intent, keep the historical unsupported request controls, and add distinct satisfiable, unsatisfiable, valid-path, and invalid-path cases. Store repository-confined synthetic inputs plus complete ScenarioSatisfiabilityEvidenceModel and ExploitPathAnalysisEvidenceModel envelopes. Record one fixed-argv offline command, one observation, and one evidence artifact per new case, including the exact profiles, source/model/snapshot/graph/query/configuration/evidence digests, artifact SHA-256, versions, witnesses or subset-minimal core / structured invalid-path evidence, and explicit limitations.

4. Replay through production boundaries. Extend the checker to parse stored envelopes with the published contract models, call analyze_scenario_file/replay_satisfiability_evidence and analyze_exploit_path_file/replay_exploit_path_evidence, and invoke the existing raes processor satisfiability and raes processor exploit-path commands with fixed argument arrays, shell=False, bounded timeout/output, repository-confined paths, and no network or environment-selected artifacts. Require CLI envelopes, direct service analysis, replay, observation joins, and stored artifacts to agree. Retained schema, semantic, workflow, participant, and compile-determinism cases continue through their existing issue-168 production entrypoints.

5. Derive bounded claims and document the outcome. Add the v2 execution snapshot and analysis, deriving each ADR-021 status (demonstrated, partial, untested, refuted) from required observations and protocol thresholds, with expected status used only as a ceiling. Update docs/research/formal-semantic-validation/index.md and retain docs/decisions/issue-828-formal-semantic-validation-retest-preflight.md to explain exactly what the finite-domain solver and typed attack-graph evidence establish and do not establish. No published schema, production analyzer semantics, runtime/backend behavior, changelog, or version file changes are planned.

6. Verify proportionately and at repository gates. During TDD, run the focused formal-validation tests and checker with RAES_REQUIREMENT_UID=ASR-530, including mutation cases for all acceptance criteria. Before completion, run RAES_REQUIREMENT_UID=ASR-530 implementations/python/.venv/bin/python tools/check_repo_policy.py, RAES_REQUIREMENT_UID=ASR-530 implementations/python/.venv/bin/python tools/check_requirement_governance.py, and RAES_REQUIREMENT_UID=ASR-530 implementations/python/.venv/bin/python tools/verify_all.py, followed by the configured Ground Control completion, policy, pre-publish review, CI, and Sonar gates. After merge, reconcile ASR-530 IMPLEMENTS/TESTS traceability to the checker, evidence release, and integrity tests.

Repository-wide design checks

• Security: reuse bounded duplicate-rejecting JSON loading, closed shapes, stable IDs, safe_repo_path, digest pins, synthetic public inputs, sanitized PolicyFailure/production diagnostics, fixed argv, bounded subprocess output/time, and no secret/environment/source payload capture. The known production exploit-input duplicate-key limitation is recorded, not silently strengthened here.
• Maintainability: reuse tools/evidence_bundle_index.py, the specification-coverage atomic-manifest pattern, existing formal-validation replay helpers, published evidence models, production analyzers/replay APIs, CLI semantics, canonical JCS digests, and the existing nox gate; introduce no parallel schema, loader, solver, graph model, logger, persistence layer, or workflow.
• Extensibility: make release manifests and observation identities profile/configuration-driven so a future solver/search profile or repeated repository revision adds an immutable release rather than editing prior evidence or checker constants.
• Whole-repo boundary: account for ADR-021/072/086, issue-168/826/827 guidance, satisfiability and exploit-path specs/contracts/CLI, SDL parse/semantic/instantiate/compile paths, participant tests, schema publication parity, JSON artifact checks, docs, policy, requirement governance, OSV, private-key, and gitleaks gates.

[Brad-Edwards]

gc_codex_review — cycle 1 of 1 (pre-push) on issue #828 (branch 828-retest-semantic-evidence)
Diff mode: inline — the complete diff was supplied in one prompt

Core review

Verdict: ship-with-fixes

The atomic, digest-pinned release model is the right architectural shape: it reuses the repository's bounded loaders, path confinement, contract models, production analyzers, replay APIs, and CLI rather than introducing parallel evidence semantics. The production controls and tests pin meaningful behavior. One architecture-fit gap remains at the historical-drift seam: the implementation replays the immutable baseline against current code instead of joining baseline observations to the new release with an explicit drift disposition, which forecloses the documented next variation of an intentional product correction.

Blocking findings (1):

1. [one-off] Historical replay prevents the promised explicit drift workflow — tools/check_formal_semantic_validation.py:985
   Historical release 1.2 is validated with replay enabled against the current implementation, so any legitimate later correction that changes a retained v1 result makes the immutable historical release fail. Meanwhile, the retest path compares retained cases only with their new v2 observations and never joins them to the immutable v1 observations or validates deviations. The gate therefore cannot implement its stated contract of preserving the baseline while recording a bounded old-to-new drift disposition. Validate historical releases for immutable shape and digest integrity without replaying them as current behavior; then join every retained retest case to the selected baseline observation and require a structured disposition whenever outcome, diagnostic, or result digest differs.

Security review

Verdict: ship

This is shaped correctly as a local, offline evidence-integration gate. The security-sensitive seam is the transition from repository-controlled artifacts into production replay: paths remain repository-confined, JSON loading is bounded and duplicate-rejecting, artifacts are digest-pinned, evidence is validated through published contract models, and subprocesses use fixed argument arrays without shell evaluation or inherited environment data. The atomic release record preserves coherent historical selection and accommodates the next analyzer or profile revision without weakening the existing validation boundary.

No blocking findings.

[Brad-Edwards]

gc_codex_review pre-push cycle 1 of 1 complete for issue #828 on branch '828-retest-semantic-evidence'. 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.

[Brad-Edwards]

Review decision record — codex cycle 1 (issue #828)

Reviewer: codex
Cycle: 1

Architectural read:

Core reviewer: The atomic, digest-pinned release model is the right architectural shape: it reuses the repository's bounded loaders, path confinement, contract models, production analyzers, replay APIs, and CLI rather than introducing parallel evidence semantics. The production controls and tests pin meaningful behavior. One architecture-fit gap remains at the historical-drift seam: the implementation replays the immutable baseline against current code instead of joining baseline observations to the new release with an explicit drift disposition, which forecloses the documented next variation of an intentional product correction.

Security reviewer: This is shaped correctly as a local, offline evidence-integration gate. The security-sensitive seam is the transition from repository-controlled artifacts into production replay: paths remain repository-confined, JSON loading is bounded and duplicate-rejecting, artifacts are digest-pinned, evidence is validated through published contract models, and subprocesses use fixed argument arrays without shell evaluation or inherited environment data. The atomic release record preserves coherent historical selection and accommodates the next analyzer or profile revision without weakening the existing validation boundary.

Blocking findings: 1

Finding 1 — one-off

• ID: F1
• Title: [core] Historical replay prevents the promised explicit drift workflow
• Location: tools/check_formal_semantic_validation.py:985
• Decision: fix
• Rationale: Historical release 1.2 is validated with replay enabled against the current implementation, so any legitimate later correction that changes a retained v1 result makes the immutable historical release fail. Meanwhile, the retest path compar…