core/docs/decisions/ADR-0117-solution-trace-verifier.md

ADR-0117 — SolutionTrace Verifier

Status: Accepted Date: 2026-05-22 Author: CORE agents + reviewers Depends on: ADR-0114, ADR-0114a, ADR-0115, ADR-0116

---

Context

ADR-0116 shipped the solver and emitted SolutionTrace records with per-step before_value / after_value / pack_lemma_id, byte- deterministic canonical_bytes(). The solver itself enforces correctness at construction time, but the solver could be buggy, tampered with after the fact, or replaced by a different implementation. ADR-0114a Obligation #3 requires that every correct answer ship with a replay-equal trace, and that requirement is only load-bearing if a verifier independent of the solver can reproduce the answer from the trace.

ADR-0117 ships that verifier.

---

Decision

generate/math_verifier.py

Exposes verify(graph, trace) -> VerifierVerdict. Pure function; same (graph, trace) always returns a byte-equal verdict.

The verifier runs six named checks in order, accumulating each one's result in verdict.checks:

Check name	What it verifies
graph_canonical_hash_matches	trace.graph_canonical_hash equals a fresh sha256(graph.canonical_bytes())
pack_id_matches	trace.pack_id == "en_arithmetic_v1"
pack_lemmas_resolve	The arithmetic pack loads and provides every required lemma
step_pack_lemma_ids_match_bindings	Every step's pack_lemma_id equals the resolved binding for its operation_kind
step_replay_matches_before_after	Replaying each step from the graph's initial state reproduces every before_value, after_value, target_before, target_after byte-equal
answer_value_reproduces	The verifier's resolved Unknown equals trace.answer_value

VerifierVerdict.passed is True only if every check held. On failure, reason names the first failed check; checks holds the full per-check record for audit.

Independence from the solver

The verifier imports only the operation-semantics constants and the pack resolver from math_solver. It does NOT call solve(). It re-derives every value the trace claims using a fresh state machine that lives in _verify_step. If a solver bug produced a wrong after_value, the verifier catches it. If a tamperer rewrote answer_value post-solve, the verifier catches it. If the input graph's bytes were edited but the trace was not re-signed, the graph_canonical_hash check catches it.

The verifier deliberately re-implements the operation semantics documented in ADR-0116 rather than importing the solver's apply function. This is belt-and-suspenders for adversarial replacement of the solver.

What a tampered trace looks like

Tamper	Verdict
Mutate before_value of step N	step_replay_matches_before_after: step N declares before_value=X, verifier computed Y
Mutate after_value of step N	step_replay_matches_before_after: step N declares after_value=X, verifier computed Y
Mutate operand.value of step N	step_replay_matches_before_after (cascades through after_value)
Mutate pack_lemma_id of step N	step_pack_lemma_ids_match_bindings: step N declares ...
Mutate graph_canonical_hash	graph_canonical_hash_matches: trace declares X but graph hashes to Y
Mutate answer_value	answer_value_reproduces: verifier resolved X, trace declared Y
Mutate pack_id	pack_id_matches: trace declares X, expected en_arithmetic_v1
Mutate target_before / target_after of transfer step	step_replay_matches_before_after: step N declares target_*=X, verifier computed Y

Every named tamper class is pinned by a test in tests/test_math_verifier.py.

---

Invariants

adr_0117_solver_traces_verify

For every case in evals/gsm8k_parser_dev/cases.jsonl, the verifier accepts the solver's own trace with verdict.passed=True. Tested parametrized over all 50 cases.

adr_0117_tampered_trace_rejected

For each named tamper class, a mutated SolutionTrace produces verdict.passed=False with a reason naming the offending check. Pinned by seven TestTamperDetection cases.

adr_0117_verifier_independent_of_solver

The verifier does not invoke solve() and re-derives every value from graph + trace alone. Inspected by import structure: the verifier imports _resolve_pack_lemmas, REQUIRED_PACK_ID, and the typed dataclasses, but NOT solve itself.

adr_0117_determinism

Two verify(graph, trace) calls produce byte-equal VerifierVerdict.canonical_bytes(). Tested directly.

---

ADR-0114a obligation discharge update

ADR-0116 discharged Obligation #3 at solver fidelity (the solver itself emits a trace that, when replayed in-process, reproduces the answer). ADR-0117 now discharges Obligation #3 at verifier fidelity: a third party with only the graph + trace and a re-installation of the arithmetic pack reproduces the answer byte-equal.

Obligation	Status
#1 Sealed-holdout discipline	Substrate present; per-lane enforcement deferred to ADR-0119
#2 OOD surface variation	In flight (delegated to Codex, ADR-0118a)
#3 Replay-equal trace	Discharged at verifier fidelity (was solver-fidelity under ADR-0116)
#4 Typed refusal	Discharged at solver layer (ADR-0116)
#5 Reasoning-isolation perturbation suite	Future ADR
#6 Compositional-depth curve	Measurement-only at promotion
#7 Frontier-baseline comparison	Deferred to ADR-0119
#8 Adversarial generation	Deferred to ADR-0119
#9 Determinism	Discharged at solver + verifier layers
#10 Operation provenance via pack	Discharged in full (ADR-0116); verifier re-checks

Five obligations now have load-bearing implementations: #3 (now at verifier fidelity), #4, #9, #10, plus the in-flight #2 from Codex's ADR-0118a work.

---

Acceptance evidence

Accepted when:

• generate/math_verifier.py exports verify, VerifierVerdict, VerificationError
• tests/test_math_verifier.py (62 cases) is green
• Verifier passes all 50 dev-set solver traces
• Every named tamper class is caught by the test suite
• Smoke suite is green
• ADR linked from docs/decisions/README.md index and frontier

---

Consequences

• The promise "every correct answer reproduces from disk byte-for-byte" is now mechanically verifiable by anyone — including a reviewer who does not trust the solver. The trace + the graph + the pack are sufficient.
• The audit story strengthens: ADR-0114a Obligation #3 is no longer an in-process invariant; it's a cross-process invariant. A future expert promotion (ADR-0120) can require that every "correct" row in its evidence bundle ship with a verifier verdict, not just a solver outcome.
• The verifier is the substrate for ADR-0119's GSM8K eval lane: every case's answer goes through verify() before scoring. A problem with a wrong trace (replay drift) is treated as a wrong outcome, not correct — closing the loophole where a buggy solver could produce coincidentally-correct answers via wrong steps.

---

Out of scope

• Stepped-realizer prose (ADR-0118) — distinct concern; consumes the same trace.
• GSM8K eval lane (ADR-0119) — uses this verifier as scoring substrate.
• Multi-pack verifier (verifier currently checks en_arithmetic_v1 hardcoded; future domains may have their own operator packs).
• Property-based fuzzing the verifier against adversarial traces. Could be a follow-up if real-world traces ever produce surprises.