core-labs/core
1
0
Fork 0
Code Issues Pull requests 1 Projects Releases Packages Wiki Activity Actions

feat: ADR-0117 — SolutionTrace verifier (solver-independent)

Browse source 
Phase 3 of the ADR-0114 expert-capability roadmap. Re-applies every
step of a SolutionTrace from the input graph's initial state and
asserts byte-equal reproduction of answer_value. Pure function; same
(graph, trace) → byte-equal VerifierVerdict.

Why this is distinct from the solver

ADR-0116's solver enforces correctness at construction. ADR-0117's
verifier is a SECOND, INDEPENDENT implementation that re-derives
every value the trace claims. The verifier does NOT call solve(). It
re-implements the operation semantics from ADR-0116 directly inside
_verify_step. If the solver had a bug or was tampered with after the
fact, the verifier catches it.

Six checks per verdict (named, ordered, audit-logged):
  1. graph_canonical_hash_matches
  2. pack_id_matches
  3. pack_lemmas_resolve
  4. step_pack_lemma_ids_match_bindings
  5. step_replay_matches_before_after
  6. answer_value_reproduces

Seven named tamper classes all caught:
  - mutated before_value / after_value / operand of any step
  - mutated pack_lemma_id of any step
  - mutated graph_canonical_hash
  - mutated answer_value
  - mutated pack_id
  - mutated target_before / target_after of transfer step

ADR-0114a obligation update

  #3 Replay-equal trace — now discharged at VERIFIER FIDELITY
     (was solver-only under ADR-0116). A third party with only
     (graph, trace, pack) can reproduce the answer byte-equal.

Five of ten obligations now load-bearing: #3, #4, #9, #10 plus
in-flight #2 (Codex's ADR-0118a OOD generator).

Tests: 62/62 verifier suite green; 67/67 smoke green; existing
solver + parser + schema suites unaffected.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This commit is contained in:
Shay 2026-05-22 16:40:38 -07:00
parent 83a3824d65
commit 4336490731
4 changed files with 673 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

181
docs/decisions/ADR-0117-solution-trace-verifier.md Normal file
View file

@ -0,0 +1,181 @@
# 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.

2
docs/decisions/README.md
View file

@ -38,6 +38,7 @@ ADRs record significant architectural decisions: what was decided, why, what alt
| [ADR-0114a](ADR-0114a-anti-overfitting-proof-obligations.md) | Anti-Overfitting Proof Obligations for `expert` Promotion | Accepted (2026-05-22) |
| [ADR-0115](ADR-0115-math-problem-parser-and-graph.md) | Math Problem Parser and Typed Proposition Graph | Phase 1.1+1.2+1.3 Accepted (2026-05-22) |
| [ADR-0116](ADR-0116-deterministic-solver.md) | Deterministic Solver (`MathProblemGraph` → `SolutionTrace`) | Accepted (2026-05-22) |
| [ADR-0117](ADR-0117-solution-trace-verifier.md) | `SolutionTrace` Verifier (independent of solver) | Accepted (2026-05-22) |
| [ADR-0122](ADR-0122-systems-software-audit-passed-deferred.md) | `systems_software` Audit-Passed Promotion: Deferred | Accepted (2026-05-22) |
---
@ -73,6 +74,7 @@ The ADR-0091..0114 slate is fully accepted (0091..0113) plus one proposed-roadma
- Math Problem Parser & Typed Graph (Phase 1.1 schema + 5 seeds + Phase 1.2 45 more cases + Phase 1.3 parser engine; 50/50 byte-equal) — ADR-0115
- Anti-Overfitting Proof Obligations for any future `expert` promotion (10-point falsifiable framework) — ADR-0114a
- Deterministic Solver (Phase 2; SolutionTrace + en_arithmetic_v1 pack; discharges ADR-0114a obligations #3, #4, #9, #10) — ADR-0116
- SolutionTrace Verifier (Phase 3; solver-independent replay; lifts ADR-0114a Obligation #3 to verifier fidelity) — ADR-0117
ADR-0080 has also landed: Contemplation Loop Phase 1 adds a read-only frontier-compare miner that emits `SPECULATIVE` findings only.

302
generate/math_verifier.py Normal file
View file

@ -0,0 +1,302 @@
"""ADR-0117 — `SolutionTrace` verifier.
Re-applies every step of a :class:`SolutionTrace` from the input graph's
initial state and asserts byte-equal reproduction of ``answer_value``.
Hardens ADR-0114a Obligation #3 (every correct answer ships with a
replay-equal trace) at verifier fidelity.
The verifier is **independent of the solver**. The solver could be
buggy, malicious, or tampered with after the fact; the verifier
re-derives the answer using only:
- the input :class:`MathProblemGraph`
- the operation semantics documented in ADR-0116 (add / subtract /
transfer / multiply / divide)
- the per-step ``actor`` / ``operand`` / ``target`` declared in each
:class:`SolutionStep`
It then cross-checks against the values the trace claims:
- ``graph_canonical_hash`` matches a fresh hash of the graph
- per-step ``before_value`` / ``after_value`` match the verifier's
fresh computation
- ``answer_value`` matches the verifier's resolved unknown
- every step's ``pack_lemma_id`` resolves to a real lexicon entry in
the loaded pack (ADR-0114a Obligation #10 re-checked at verify
time)
Any mismatch raises :class:`VerificationError` with the offending step
index and a typed reason. Same input always produces the same verdict
(determinism).
"""
from __future__ import annotations
import hashlib
import json
from dataclasses import dataclass
from typing import Any
from generate.math_problem_graph import MathProblemGraph, Unknown
from generate.math_solver import (
REQUIRED_PACK_ID,
SolutionStep,
SolutionTrace,
SolveError,
_resolve_pack_lemmas,
)
class VerificationError(ValueError):
"""Raised when a trace fails to verify against its graph."""
@dataclass(frozen=True, slots=True)
class VerifierVerdict:
"""Typed outcome of a verification pass.
``passed`` is ``True`` only if every check held. ``reason`` is
empty on pass and names the first failed check on fail. ``checks``
records every check the verifier ran (in order) along with the
pass/fail status of each, so external readers can audit which
invariants held.
"""
passed: bool
reason: str
checks: tuple[tuple[str, bool, str], ...] # (name, passed, detail)
graph_canonical_hash: str
trace_answer_value: float
verifier_answer_value: float
def as_json(self) -> dict[str, Any]:
return {
"passed": self.passed,
"reason": self.reason,
"checks": [
{"name": n, "passed": p, "detail": d}
for n, p, d in self.checks
],
"graph_canonical_hash": self.graph_canonical_hash,
"trace_answer_value": self.trace_answer_value,
"verifier_answer_value": self.verifier_answer_value,
}
def canonical_bytes(self) -> bytes:
return json.dumps(
self.as_json(), sort_keys=True, separators=(",", ":")
).encode("utf-8")
def verify(graph: MathProblemGraph, trace: SolutionTrace) -> VerifierVerdict:
"""Run all verifier checks against ``trace`` for ``graph``.
Pure function: same (graph, trace) -> byte-equal verdict.
"""
checks: list[tuple[str, bool, str]] = []
fresh_hash = hashlib.sha256(graph.canonical_bytes()).hexdigest()
# Check 1 — graph hash matches
hash_ok = trace.graph_canonical_hash == fresh_hash
checks.append(
(
"graph_canonical_hash_matches",
hash_ok,
(
""
if hash_ok
else f"trace declares {trace.graph_canonical_hash!r} but graph hashes to {fresh_hash!r}"
),
)
)
# Check 2 — pack id matches
pack_ok = trace.pack_id == REQUIRED_PACK_ID
checks.append(
(
"pack_id_matches",
pack_ok,
(
""
if pack_ok
else f"trace declares pack {trace.pack_id!r}, expected {REQUIRED_PACK_ID!r}"
),
)
)
# Check 3 — pack lemma ids resolve
try:
pack_bindings = _resolve_pack_lemmas()
lemmas_ok = True
lemma_detail = ""
except SolveError as exc:
pack_bindings = {}
lemmas_ok = False
lemma_detail = f"pack resolution failed: {exc}"
checks.append(("pack_lemmas_resolve", lemmas_ok, lemma_detail))
# Check 4 — every step's pack_lemma_id matches the resolved binding
if lemmas_ok:
step_binding_ok = True
step_binding_detail = ""
for step in trace.steps:
expected = pack_bindings.get(step.operation_kind)
if expected is None:
step_binding_ok = False
step_binding_detail = (
f"step {step.step_index} declares unknown operation kind "
f"{step.operation_kind!r}"
)
break
if step.pack_lemma_id != expected:
step_binding_ok = False
step_binding_detail = (
f"step {step.step_index} declares pack_lemma_id "
f"{step.pack_lemma_id!r}, expected {expected!r}"
)
break
checks.append(
(
"step_pack_lemma_ids_match_bindings",
step_binding_ok,
step_binding_detail,
)
)
else:
checks.append(
(
"step_pack_lemma_ids_match_bindings",
False,
"skipped: pack resolution failed",
)
)
# Check 5 — replay every step from the graph's initial state
state: dict[tuple[str, str], float] = {}
for p in graph.initial_state:
state[(p.entity, p.quantity.unit)] = float(p.quantity.value)
replay_ok = True
replay_detail = ""
for step in trace.steps:
try:
_verify_step(step, state)
except VerificationError as exc:
replay_ok = False
replay_detail = str(exc)
break
checks.append(("step_replay_matches_before_after", replay_ok, replay_detail))
# Check 6 — verifier's resolved answer matches trace's answer
verifier_answer = _resolve_answer(
Unknown(entity=trace.answer_entity, unit=trace.answer_unit), state
)
answer_ok = (
replay_ok
and verifier_answer is not None
and verifier_answer == trace.answer_value
)
checks.append(
(
"answer_value_reproduces",
answer_ok,
(
""
if answer_ok
else (
f"verifier resolved {verifier_answer!r}, trace declared "
f"{trace.answer_value!r}"
)
),
)
)
all_passed = all(p for _, p, _ in checks)
reason = ""
if not all_passed:
for name, p, detail in checks:
if not p:
reason = f"{name}: {detail}" if detail else name
break
return VerifierVerdict(
passed=all_passed,
reason=reason,
checks=tuple(checks),
graph_canonical_hash=fresh_hash,
trace_answer_value=trace.answer_value,
verifier_answer_value=(
verifier_answer if verifier_answer is not None else float("nan")
),
)
def _verify_step(step: SolutionStep, state: dict[tuple[str, str], float]) -> None:
key = (step.actor, step.operand.unit)
fresh_before = state.get(key, 0.0)
if fresh_before != step.before_value:
raise VerificationError(
f"step {step.step_index} declares before_value={step.before_value}, "
f"verifier computed {fresh_before}"
)
v = float(step.operand.value)
if step.operation_kind == "add":
fresh_after = fresh_before + v
state[key] = fresh_after
elif step.operation_kind == "subtract":
fresh_after = fresh_before - v
state[key] = fresh_after
elif step.operation_kind == "transfer":
if step.target is None:
raise VerificationError(
f"step {step.step_index} kind=transfer has no target"
)
fresh_after = fresh_before - v
state[key] = fresh_after
tgt_key = (step.target, step.operand.unit)
fresh_target_before = state.get(tgt_key, 0.0)
if (
step.target_before is None
or fresh_target_before != step.target_before
):
raise VerificationError(
f"step {step.step_index} declares target_before="
f"{step.target_before}, verifier computed {fresh_target_before}"
)
fresh_target_after = fresh_target_before + v
state[tgt_key] = fresh_target_after
if (
step.target_after is None
or fresh_target_after != step.target_after
):
raise VerificationError(
f"step {step.step_index} declares target_after="
f"{step.target_after}, verifier computed {fresh_target_after}"
)
elif step.operation_kind == "multiply":
fresh_after = fresh_before * v
state[key] = fresh_after
elif step.operation_kind == "divide":
if v == 0:
raise VerificationError(
f"step {step.step_index} divides by zero"
)
fresh_after = fresh_before / v
state[key] = fresh_after
else:
raise VerificationError(
f"step {step.step_index} declares unknown kind {step.operation_kind!r}"
)
if fresh_after != step.after_value:
raise VerificationError(
f"step {step.step_index} declares after_value={step.after_value}, "
f"verifier computed {fresh_after}"
)
def _resolve_answer(
unknown: Unknown, state: dict[tuple[str, str], float]
) -> float | None:
if unknown.entity is None:
return sum(v for (_, unit), v in state.items() if unit == unknown.unit)
return state.get((unknown.entity, unknown.unit))

188
tests/test_math_verifier.py Normal file
View file

@ -0,0 +1,188 @@
"""ADR-0117 — solution-trace verifier invariants.
Pins five load-bearing invariants:
1. **Every dev-set solver trace verifies.** All 50 cases produce a
:class:`SolutionTrace` whose verifier verdict is ``passed=True``.
2. **Tampered traces are caught.** Mutating any single field of a
step (operand, before, after, target_before, target_after,
pack_lemma_id, operation_kind) produces ``passed=False`` with a
reason that names the offending check.
3. **Tampered graph hash is caught.** A trace whose
``graph_canonical_hash`` does not match the input graph fails.
4. **Tampered answer is caught.** A trace whose ``answer_value`` does
not match the verifier's resolved unknown fails.
5. **Determinism.** Two verifications produce byte-equal verdict bytes.
The verifier is **independent of the solver**: it re-derives every
value the trace claims, using only the input graph and the operation
semantics documented in ADR-0116. ADR-0114a Obligation #3 is now
discharged at verifier fidelity (in addition to solver fidelity from
ADR-0116).
"""
from __future__ import annotations
import dataclasses
import json
from pathlib import Path
import pytest
from generate.math_parser import parse_problem
from generate.math_problem_graph import MathProblemGraph, Quantity
from generate.math_solver import SolutionTrace, solve
from generate.math_verifier import VerifierVerdict, verify
_REPO_ROOT = Path(__file__).resolve().parent.parent
_CASES_PATH = _REPO_ROOT / "evals" / "gsm8k_parser_dev" / "cases.jsonl"
def _load_cases() -> list[dict]:
return [
json.loads(line) for line in _CASES_PATH.read_text().splitlines() if line.strip()
]
def _build_simple_case() -> tuple[MathProblemGraph, SolutionTrace]:
g = parse_problem(
"Sam has 5 apples. He buys 3 more. How many apples does Sam have?"
)
return g, solve(g)
class TestAllDevSetCasesVerify:
@pytest.mark.parametrize("case", _load_cases(), ids=lambda c: c["id"])
def test_solver_trace_verifies(self, case: dict) -> None:
graph = parse_problem(case["problem"])
trace = solve(graph)
verdict = verify(graph, trace)
assert verdict.passed, (
f"{case['id']}: verifier rejected solver's own trace — {verdict.reason}"
)
assert verdict.trace_answer_value == case["expected_answer"]
class TestTamperDetection:
def test_tampered_after_value_caught(self) -> None:
g, t = _build_simple_case()
tampered_step = dataclasses.replace(t.steps[0], after_value=999.0)
tampered = dataclasses.replace(t, steps=(tampered_step,))
verdict = verify(g, tampered)
assert verdict.passed is False
assert "after_value" in verdict.reason or "step_replay" in verdict.reason
def test_tampered_before_value_caught(self) -> None:
g, t = _build_simple_case()
tampered_step = dataclasses.replace(t.steps[0], before_value=42.0)
tampered = dataclasses.replace(t, steps=(tampered_step,))
verdict = verify(g, tampered)
assert verdict.passed is False
assert "before_value" in verdict.reason
def test_tampered_operand_caught(self) -> None:
g, t = _build_simple_case()
tampered_step = dataclasses.replace(t.steps[0], operand=Quantity(99, "apples"))
tampered = dataclasses.replace(t, steps=(tampered_step,))
verdict = verify(g, tampered)
assert verdict.passed is False
def test_tampered_pack_lemma_id_caught(self) -> None:
g, t = _build_simple_case()
tampered_step = dataclasses.replace(
t.steps[0], pack_lemma_id="some_other_pack:add"
)
tampered = dataclasses.replace(t, steps=(tampered_step,))
verdict = verify(g, tampered)
assert verdict.passed is False
assert "pack_lemma" in verdict.reason
def test_tampered_graph_hash_caught(self) -> None:
g, t = _build_simple_case()
tampered = dataclasses.replace(t, graph_canonical_hash="0" * 64)
verdict = verify(g, tampered)
assert verdict.passed is False
assert "graph_canonical_hash" in verdict.reason
def test_tampered_answer_caught(self) -> None:
g, t = _build_simple_case()
tampered = dataclasses.replace(t, answer_value=42.0)
verdict = verify(g, tampered)
assert verdict.passed is False
assert "answer" in verdict.reason
def test_tampered_pack_id_caught(self) -> None:
g, t = _build_simple_case()
tampered = dataclasses.replace(t, pack_id="some_other_pack")
verdict = verify(g, tampered)
assert verdict.passed is False
assert "pack_id" in verdict.reason
class TestDeterminism:
def test_two_verifications_produce_byte_equal_verdict(self) -> None:
g, t = _build_simple_case()
v1 = verify(g, t)
v2 = verify(g, t)
assert v1.canonical_bytes() == v2.canonical_bytes()
assert v1 == v2
class TestVerdictShape:
def test_verdict_records_every_check(self) -> None:
g, t = _build_simple_case()
verdict = verify(g, t)
check_names = {name for name, _, _ in verdict.checks}
# At minimum these named invariants must be in the verdict
assert "graph_canonical_hash_matches" in check_names
assert "pack_id_matches" in check_names
assert "pack_lemmas_resolve" in check_names
assert "step_pack_lemma_ids_match_bindings" in check_names
assert "step_replay_matches_before_after" in check_names
assert "answer_value_reproduces" in check_names
assert isinstance(verdict, VerifierVerdict)
def test_passing_verdict_has_empty_reason(self) -> None:
g, t = _build_simple_case()
verdict = verify(g, t)
assert verdict.passed is True
assert verdict.reason == ""
class TestTotalAcrossAnswer:
def test_multi_entity_sum_question_verifies(self) -> None:
g = parse_problem(
"Tom has 4 stickers. Sara has 7 stickers. "
"How many stickers do they have in total?"
)
t = solve(g)
verdict = verify(g, t)
assert verdict.passed is True
assert t.answer_value == 11.0
assert t.answer_entity is None
class TestTransferStepVerifiesBothSides:
def test_transfer_target_before_and_after_must_match(self) -> None:
g = parse_problem(
"Anna has 8 marbles. She gives 3 to Ben. "
"How many marbles does Anna have now?"
)
t = solve(g)
assert t.steps[0].operation_kind == "transfer"
assert t.steps[0].target_before == 0.0
assert t.steps[0].target_after == 3.0
verdict = verify(g, t)
assert verdict.passed is True
# Tamper target_after — verifier catches it
tampered_step = dataclasses.replace(t.steps[0], target_after=999.0)
tampered = dataclasses.replace(t, steps=(tampered_step,))
verdict_bad = verify(g, tampered)
assert verdict_bad.passed is False
assert "target_after" in verdict_bad.reason