feat(ADR-0131.1.S): sealed holdout for symbolic equivalence v1

This commit is contained in:
Shay 2026-05-23 10:40:45 -07:00
parent 980213ed62
commit 32c6ec63fb
6 changed files with 502 additions and 0 deletions

View file

@ -0,0 +1,61 @@
# ADR-0131.1.S — Sealed Holdout for Benchmark 1 (Symbolic Equivalence v1)
**Status:** Accepted
**Date:** 2026-05-23
**Author:** CORE agents + reviewers
**Depends on:** ADR-0131 (composite math expert promotion), ADR-0119.7 (sealed GSM8K test set), #167 (symbolic equivalence v1)
---
## Context
Benchmark 1 of [ADR-0131](ADR-0131-math-expert-rebench.md), merged in PR #167, tests whether the engine can determine algebraic equivalence of univariate integer polynomials under exact recall. The benchmark has a 100% baseline correct rate on a curated set of 30 public cases in `cases.jsonl`.
To make the benchmark's claims externally credible, we must prevent the development team from "peeking" at or optimizing against the evaluation cases used to measure expert promotion. Per the methodology proven in [ADR-0119.7](ADR-0119.7-sealed-gsm8k-test.md) for GSM8K, we introduce a sealed holdout split for Benchmark 1 using pyrage age-encryption.
---
## Decision
We establish the Benchmark 1 sealed holdout split:
1. **Crypto Keypair**: Generate a dedicated X25519 key pair for the B1 sealed holdout. The public key is stored in the repo at `evals/math_symbolic_equivalence/v1/sealed_holdout.pubkey`. The private key stays off-repo per the seal discipline of ADR-0119.7.
2. **Sealed Holdout Cases**: Hand-curated 14 new evaluation cases strictly within the v1 univariate integer polynomial scope. The categories strictly match the public cases (e.g. `commutative_add`, `distributive`, `square_of_binomial`, `difference_of_squares`, `collect_like_terms`, `zero_cancellation`, `repeated_addition`, `exponent_combine`, `different_constant`, `sign_flipped`, `distributive_miss`, `out_of_scope_variable`, `out_of_scope_division`).
3. **Disjointness Invariant**: The holdout cases are guaranteed to be disjoint from the public cases — they do not duplicate any `case_id` or any `(expression_a, expression_b)` pair.
4. **Sealed File**: The plaintext cases are encrypted with the public key and written to `evals/math_symbolic_equivalence/v1/sealed_holdout.age`. No plaintext representation of the holdout cases resides in the repository.
5. **Sealed Runner**: We ship `evals/math_symbolic_equivalence/v1/sealed_runner.py` which decrypts the sealed file using the age identity file provided by the `CORE_SEALED_KEY` environment variable. If the environment variable is unset or missing, it fails cleanly with an `EnvironmentError`.
6. **Pass Criterion**: The sealed runner writes its results to `sealed_report.json` and gates the split on:
- `wrong == 0` (no confabulation)
- `correct_rate >= 0.95` (statistical threshold matching public splitter)
---
## Security and Trust Boundaries
Per **Security and Trust Boundaries** in [CLAUDE.md](file:///Users/kaizenpro/Projects/core/CLAUDE.md#L140-L167), we enforce strict trust boundaries on holdout decryption:
- **No plaintext companion files** are written to disk during the runner's execution (only memory-based decryption).
- **No logging or echos** of the decrypted plaintext cases to stdout or stderr are allowed.
- The decryption key `CORE_SEALED_KEY` is never set in standard CI runs; tests requiring decryption gracefully skip when the key is absent to avoid blocking standard pull request flows.
---
## Invariants
### `adr_0131_1_s_sealed_file_present_and_age_formatted`
`evals/math_symbolic_equivalence/v1/sealed_holdout.age` exists, is non-empty, and begins with the `age-encryption.org/` magic header.
### `adr_0131_1_s_no_plaintext_leaks`
No plaintext companion files (`cases_plaintext.jsonl`, etc.) exist in the holdout directory.
### `adr_0131_1_s_runner_refuses_without_key`
The sealed runner fails with `EnvironmentError` when `CORE_SEALED_KEY` is not configured, preventing silent fallback or execution.
### `adr_0131_1_s_decrypted_disjointness`
When decrypted, all holdout cases have distinct `case_id` values and distinct expression pairs compared to the public `cases.jsonl` set.
---
## Consequences
- **Credentialed Claims**: Benchmark 1's validation claims are now externally reviewable and immune to developer-level overfitting.
- **Zero-Confabulation Gate**: `wrong == 0` is strictly enforced against the sealed holdout. Any algebraic regression that triggers a wrong verdict on held-out cases rejects the build.

Binary file not shown.

View file

@ -0,0 +1 @@
age1gur48tg6fr6wua5d5l86gd8mqx6tssx4nwf8wp4qgtksmn87ggzs6dujqk

View file

@ -0,0 +1,132 @@
{
"adr": "0131.1.S",
"benchmark": "symbolic_equivalence_holdout_v1",
"cases_path": "evals/math_symbolic_equivalence/v1/sealed_holdout.age",
"correct_rate": 1.0,
"counts": {
"correct": 14,
"refused": 0,
"wrong": 0
},
"exit_criterion": {
"correct_rate_min": 0.95,
"passed": true,
"wrong_max": 0
},
"per_case": [
{
"actual": "equivalent",
"case_id": "sym-eq-v1-hld-0001",
"category": "commutative_add",
"expected": "equivalent",
"reason": "",
"verdict_class": "correct"
},
{
"actual": "equivalent",
"case_id": "sym-eq-v1-hld-0002",
"category": "commutative_mul",
"expected": "equivalent",
"reason": "",
"verdict_class": "correct"
},
{
"actual": "equivalent",
"case_id": "sym-eq-v1-hld-0003",
"category": "distributive",
"expected": "equivalent",
"reason": "",
"verdict_class": "correct"
},
{
"actual": "equivalent",
"case_id": "sym-eq-v1-hld-0004",
"category": "square_of_binomial",
"expected": "equivalent",
"reason": "",
"verdict_class": "correct"
},
{
"actual": "equivalent",
"case_id": "sym-eq-v1-hld-0005",
"category": "difference_of_squares",
"expected": "equivalent",
"reason": "",
"verdict_class": "correct"
},
{
"actual": "equivalent",
"case_id": "sym-eq-v1-hld-0006",
"category": "collect_like_terms",
"expected": "equivalent",
"reason": "",
"verdict_class": "correct"
},
{
"actual": "equivalent",
"case_id": "sym-eq-v1-hld-0007",
"category": "zero_cancellation",
"expected": "equivalent",
"reason": "",
"verdict_class": "correct"
},
{
"actual": "equivalent",
"case_id": "sym-eq-v1-hld-0008",
"category": "repeated_addition",
"expected": "equivalent",
"reason": "",
"verdict_class": "correct"
},
{
"actual": "equivalent",
"case_id": "sym-eq-v1-hld-0009",
"category": "exponent_combine",
"expected": "equivalent",
"reason": "",
"verdict_class": "correct"
},
{
"actual": "not_equivalent",
"case_id": "sym-eq-v1-hld-0010",
"category": "different_constant",
"expected": "not_equivalent",
"reason": "",
"verdict_class": "correct"
},
{
"actual": "not_equivalent",
"case_id": "sym-eq-v1-hld-0011",
"category": "sign_flipped",
"expected": "not_equivalent",
"reason": "",
"verdict_class": "correct"
},
{
"actual": "not_equivalent",
"case_id": "sym-eq-v1-hld-0012",
"category": "distributive_miss",
"expected": "not_equivalent",
"reason": "",
"verdict_class": "correct"
},
{
"actual": "refused",
"case_id": "sym-eq-v1-hld-0013",
"category": "out_of_scope_variable",
"expected": "refused",
"reason": "",
"verdict_class": "correct"
},
{
"actual": "refused",
"case_id": "sym-eq-v1-hld-0014",
"category": "out_of_scope_division",
"expected": "refused",
"reason": "",
"verdict_class": "correct"
}
],
"sample_count": 14,
"schema_version": 1
}

View file

@ -0,0 +1,169 @@
"""ADR-0131.1.S — Symbolic equivalence sealed holdout runner.
Decrypts ``sealed_holdout.age`` using the identity file specified in the
``CORE_SEALED_KEY`` environment variable, runs symbolic equivalence on each
case, writes a deterministic ``sealed_report.json``, and exits 0/1.
CLI: ``python -m evals.math_symbolic_equivalence.v1.sealed_runner``
"""
from __future__ import annotations
import json
import os
import sys
from dataclasses import dataclass
from pathlib import Path
from typing import Any
from generate.math_symbolic_equivalence import (
Verdict,
check_equivalence,
)
_HERE = Path(__file__).resolve().parent
_SEALED_PATH = _HERE / "sealed_holdout.age"
_REPORT_PATH = _HERE / "sealed_report.json"
_CORRECT_RATE_MIN = 0.95
_WRONG_MAX = 0
@dataclass(frozen=True, slots=True)
class CaseOutcome:
case_id: str
category: str
expected: str
actual: str
verdict_class: str # "correct" | "wrong" | "refused"
reason: str
def as_dict(self) -> dict[str, str]:
return {
"case_id": self.case_id,
"category": self.category,
"expected": self.expected,
"actual": self.actual,
"verdict_class": self.verdict_class,
"reason": self.reason,
}
def _score_one(case: dict[str, Any]) -> CaseOutcome:
expected = case["expected"]
v = check_equivalence(case["expression_a"], case["expression_b"])
actual = v.verdict.value
if actual == expected:
verdict_class = "correct"
reason = ""
elif actual == Verdict.REFUSED.value:
verdict_class = "refused"
reason = v.reason
else:
verdict_class = "wrong"
reason = (
f"engine={actual!r} expected={expected!r}; "
f"canonical_a={v.canonical_a!r} canonical_b={v.canonical_b!r}"
)
return CaseOutcome(
case_id=case["case_id"],
category=case["category"],
expected=expected,
actual=actual,
verdict_class=verdict_class,
reason=reason,
)
def decrypt_cases(sealed_path: Path = _SEALED_PATH) -> list[dict[str, Any]]:
"""Decrypt the sealed file using the key from CORE_SEALED_KEY.
Raises EnvironmentError if the env var is missing or invalid.
"""
key_path_str = os.environ.get("CORE_SEALED_KEY")
if not key_path_str:
raise EnvironmentError(
"CORE_SEALED_KEY environment variable is not set; "
"cannot decrypt sealed holdout."
)
key_path = Path(key_path_str)
if not key_path.exists():
raise EnvironmentError(
f"CORE_SEALED_KEY file path does not exist: {key_path}"
)
try:
import pyrage
from pyrage.x25519 import Identity
except ImportError as exc:
raise RuntimeError("pyrage package is not installed.") from exc
try:
identity = Identity.from_str(key_path.read_text(encoding="utf-8").strip())
plaintext = pyrage.decrypt(sealed_path.read_bytes(), [identity])
except Exception as exc:
raise ValueError(f"Decryption failed: {exc}") from exc
records: list[dict[str, Any]] = []
for line in plaintext.decode("utf-8").splitlines():
line = line.strip()
if not line:
continue
records.append(json.loads(line))
return records
def build_report(cases: list[dict[str, Any]]) -> dict[str, Any]:
outcomes = [_score_one(c) for c in cases]
counts = {"correct": 0, "wrong": 0, "refused": 0}
for o in outcomes:
counts[o.verdict_class] += 1
total = len(outcomes)
correct_rate = counts["correct"] / total if total else 0.0
passed = (correct_rate >= _CORRECT_RATE_MIN) and (counts["wrong"] <= _WRONG_MAX)
return {
"schema_version": 1,
"adr": "0131.1.S",
"benchmark": "symbolic_equivalence_holdout_v1",
"cases_path": str(_SEALED_PATH.relative_to(_HERE.parent.parent.parent)),
"sample_count": total,
"counts": counts,
"correct_rate": correct_rate,
"exit_criterion": {
"correct_rate_min": _CORRECT_RATE_MIN,
"wrong_max": _WRONG_MAX,
"passed": passed,
},
"per_case": [o.as_dict() for o in outcomes],
}
def write_report(report: dict[str, Any], path: Path = _REPORT_PATH) -> None:
path.write_text(
json.dumps(report, indent=2, sort_keys=True) + "\n",
encoding="utf-8",
)
def main() -> int:
try:
cases = decrypt_cases()
except EnvironmentError as exc:
print(f"error: {exc}", file=sys.stderr)
return 2
except Exception as exc:
print(f"error: {exc.__class__.__name__}: {exc}", file=sys.stderr)
return 1
report = build_report(cases)
write_report(report)
return 0 if report["exit_criterion"]["passed"] else 1
if __name__ == "__main__":
sys.exit(main())

View file

@ -0,0 +1,139 @@
"""ADR-0131.1.S — Sealed holdout tests for symbolic equivalence v1.
Pins:
1. Sealed holdout file exists and is age-formatted.
2. Decryption fails (raises EnvironmentError) if CORE_SEALED_KEY is unset or points to a non-existent file.
3. Decryption yields valid JSONL cases matching the schema.
4. The sealed runner passes its exit criterion (wrong == 0, correct_rate >= 0.95).
5. The holdout cases are strictly disjoint from the public cases (no duplicate case_id or expression pairs).
"""
from __future__ import annotations
import json
import os
from pathlib import Path
import pytest
from evals.math_symbolic_equivalence.v1.sealed_runner import (
build_report,
decrypt_cases,
)
_REPO_ROOT = Path(__file__).resolve().parent.parent
_SEALED_PATH = _REPO_ROOT / "evals" / "math_symbolic_equivalence" / "v1" / "sealed_holdout.age"
_PUBLIC_CASES_PATH = _REPO_ROOT / "evals" / "math_symbolic_equivalence" / "v1" / "cases.jsonl"
def _decrypt_or_skip() -> list[dict]:
"""Helper to decrypt cases or skip if key is missing."""
key = os.environ.get("CORE_SEALED_KEY")
if not key:
pytest.skip("CORE_SEALED_KEY not set; skipping decryption test")
key_path = Path(key)
if not key_path.exists():
pytest.skip(f"CORE_SEALED_KEY path {key_path} does not exist; skipping decryption test")
try:
return decrypt_cases(_SEALED_PATH)
except Exception as exc:
pytest.fail(f"Decryption failed: {exc}")
class TestSealedFileExists:
def test_sealed_file_present(self) -> None:
assert _SEALED_PATH.exists(), f"missing sealed file: {_SEALED_PATH}"
assert _SEALED_PATH.is_file()
assert _SEALED_PATH.stat().st_size > 0
def test_sealed_file_is_age_formatted(self) -> None:
head = _SEALED_PATH.read_bytes()[:64]
assert head.startswith(b"age-encryption.org/"), (
f"sealed file does not look age-formatted; head={head!r}"
)
class TestDecryptionGated:
def test_decryption_refuses_without_key(self) -> None:
old_key = os.environ.get("CORE_SEALED_KEY")
if "CORE_SEALED_KEY" in os.environ:
del os.environ["CORE_SEALED_KEY"]
try:
with pytest.raises(EnvironmentError) as excinfo:
decrypt_cases(_SEALED_PATH)
assert "CORE_SEALED_KEY environment variable is not set" in str(excinfo.value)
finally:
if old_key is not None:
os.environ["CORE_SEALED_KEY"] = old_key
def test_decryption_refuses_with_invalid_key_path(self) -> None:
old_key = os.environ.get("CORE_SEALED_KEY")
os.environ["CORE_SEALED_KEY"] = "/nonexistent/path/to/key.txt"
try:
with pytest.raises(EnvironmentError) as excinfo:
decrypt_cases(_SEALED_PATH)
assert "CORE_SEALED_KEY file path does not exist" in str(excinfo.value)
finally:
if old_key is not None:
os.environ["CORE_SEALED_KEY"] = old_key
class TestSealedFileContent:
def test_decrypt_produces_valid_schema(self) -> None:
cases = _decrypt_or_skip()
assert len(cases) >= 10, f"expected at least 10 holdout cases, got {len(cases)}"
for c in cases:
assert "case_id" in c
assert c["case_id"].startswith("sym-eq-v1-hld-")
assert "expression_a" in c
assert isinstance(c["expression_a"], str) and c["expression_a"]
assert "expression_b" in c
assert isinstance(c["expression_b"], str) and c["expression_b"]
assert "expected" in c
assert c["expected"] in ("equivalent", "not_equivalent", "refused")
assert "category" in c
assert isinstance(c["category"], str) and c["category"]
assert "provenance" in c
assert "adr-0131.1" in c["provenance"]
def test_disjointness_from_public_cases(self) -> None:
sealed_cases = _decrypt_or_skip()
# Load public cases
public_cases = []
with _PUBLIC_CASES_PATH.open("r", encoding="utf-8") as fh:
for line in fh:
line = line.strip()
if line:
public_cases.append(json.loads(line))
public_ids = {c["case_id"] for c in public_cases}
public_pairs = {
(c["expression_a"].strip(), c["expression_b"].strip())
for c in public_cases
}
for c in sealed_cases:
assert c["case_id"] not in public_ids, (
f"Duplicate case_id {c['case_id']} found in sealed holdout"
)
pair = (c["expression_a"].strip(), c["expression_b"].strip())
reverse_pair = (c["expression_b"].strip(), c["expression_a"].strip())
assert pair not in public_pairs and reverse_pair not in public_pairs, (
f"Duplicate expression pair {pair} found in sealed holdout"
)
class TestSealedRunnerGate:
def test_runner_passes_exit_criterion(self) -> None:
cases = _decrypt_or_skip()
report = build_report(cases)
assert report["exit_criterion"]["passed"], (
f"Sealed holdout runner failed: correct_rate={report['correct_rate']}, "
f"wrong={report['counts']['wrong']}"
)
assert report["counts"]["wrong"] == 0, "Sealed holdout must have wrong == 0"
assert report["correct_rate"] >= 0.95, "Sealed holdout correct rate must be >= 0.95"