From 97682b5de777f29996ee63b052c9922f667cefc7 Mon Sep 17 00:00:00 2001 From: Quang Bui Date: Thu, 23 Jul 2026 15:20:34 +0700 Subject: [PATCH] [6-1] pair dataset schema, builder skeleton, fixture tests Schema + control flow for the equivalence-pair build, with the e-graph engine and the verifier injected as protocols so nothing imports 4-4/4-5 or 2-6 while those are unmerged. Split/leakage/OOD logic is finished rather than stubbed - it needs nothing from other branches. Production >=50k/5k/5k build still waits on 1-8, 4-4/4-5 and 2-6. --- configs/goal6_pairs.yaml | 51 ++++++++ docs/specs/PAIR_DATASET_SPEC.md | 114 ++++++++++++++++++ src/geml/data/pairs/__init__.py | 0 src/geml/data/pairs/generate.py | 186 +++++++++++++++++++++++++++++ src/geml/data/pairs/negatives.py | 102 ++++++++++++++++ src/geml/data/pairs/splits.py | 77 ++++++++++++ tests/data/test_pairs.py | 199 +++++++++++++++++++++++++++++++ 7 files changed, 729 insertions(+) create mode 100644 configs/goal6_pairs.yaml create mode 100644 docs/specs/PAIR_DATASET_SPEC.md create mode 100644 src/geml/data/pairs/__init__.py create mode 100644 src/geml/data/pairs/generate.py create mode 100644 src/geml/data/pairs/negatives.py create mode 100644 src/geml/data/pairs/splits.py create mode 100644 tests/data/test_pairs.py diff --git a/configs/goal6_pairs.yaml b/configs/goal6_pairs.yaml new file mode 100644 index 0000000..9dd2c22 --- /dev/null +++ b/configs/goal6_pairs.yaml @@ -0,0 +1,51 @@ +# configs/goal6_pairs.yaml +# owned by 6-1 +# +# config for the real >=50k/5k/5k pair build. NOT executable yet - it +# needs 1-8's corpus, 4-4/4-5's rule libraries and 2-6's verifier, all +# three still open. this file pins the intended run so the numbers in +# the spec and the numbers we eventually report come from the same place. + +run: + run_id: goal6_pairs_v1 + resume: true + reproduction_command: > + PYTHONPATH=src python3 -m geml.data.pairs.generate + --config configs/goal6_pairs.yaml + +corpus: + manifest_path: data/goal1_corpus/corpus_manifest.json # 1-8's frozen manifest + splits: [train, validation, test_iid, test_ood] + +targets: + # the acceptance floor, not a quota to hit by loosening anything - + # if saturation doesn't reach it, we report the shortfall + train: 50000 + validation: 5000 + test: 5000 + +positives: + mode: SAFE_REAL # 4-1 rewrite mode; POSITIVE_REAL_FORMAL needs recorded assumptions + max_per_source: 8 # cap the fan-out so one heavily-rewritable expression + # can't dominate a split + min_step_distance: 1 + max_step_distance: 12 # longer traces exist; 7-0 wants them stratified, not truncated silently + +negatives: + kind: same_family + size_tolerance: 2 # nodes. tight on purpose - a loose window makes + # "which is bigger" a winning strategy + ratio: 1.0 # one negative per positive + +verification: + tier_order: [egraph_proof, symbolic, numeric] # first tier that answers wins, tier recorded on the pair + require_refutation_for_negatives: true + +output: + path: outputs/final/goal6/pairs/ + shard_size: 25000 # matches 1-5 + +smoke_test: + count: 25 + command: > + PYTHONPATH=src python3 -m pytest tests/data/test_pairs.py -v diff --git a/docs/specs/PAIR_DATASET_SPEC.md b/docs/specs/PAIR_DATASET_SPEC.md new file mode 100644 index 0000000..eb05725 --- /dev/null +++ b/docs/specs/PAIR_DATASET_SPEC.md @@ -0,0 +1,114 @@ +# Equivalence-pair dataset (frozen by 6-1) + +The dataset Goals 6, 7 and 8 all sit on. A pair is two expression ids, a +label, and enough provenance that anyone can replay how we decided the +label. 6-2 tensorizes these records, 7-0 replays the traces into steps, +8-x uses the step distance as a value target - so the shapes below are a +contract, not an implementation detail. + +**Status: partial start.** Schema, builder control flow, negative +matching and split bookkeeping are implemented and tested against fakes +(`tests/data/test_pairs.py`). The production build waits on 1-8 (final +corpus), 4-4/4-5 (rule libraries) and 2-6 (verifier). Those come in +through the two protocols below - this module imports none of them. + +## Records (`src/geml/data/pairs/generate.py`) + +`PairRecord` - one row of the dataset. + +| Field | Notes | +|---|---| +| `pair_id` | `left~right` for positives, `left!right` for negatives | +| `left_expression_id` / `right_expression_id` | 1-2 corpus ids | +| `label` | `"equivalent"` / `"not_equivalent"` | +| `split` | one of 1-2's four splits; both sides must agree, see below | +| `group_id` | the leakage unit - e-class id when 4-2 gives us one, expression id until then | +| `family`, `max_depth`, `left_size`, `right_size` | stratification and OOD slicing | +| `verification` | tier + status, on every pair including negatives | +| `left_signature` | 3-1 signature of the state the trace starts from - 7-0 replays step 0 against it | +| `rule_sequence` | positives only: the ordered `RuleApplication` trace | +| `step_distance` | `len(rule_sequence)`; None for negatives | +| `negative_kind` | negatives only | +| `eval_tags` | `depth_ood` / `family_ood`, assigned by `tag_ood` | + +`RuleApplication` - one rewrite step. `rule_id`, `rule_name`, 4-1 `tier` +and `mode`, the `site_id` it fired on, the `result_signature` after the +step, and any `assumptions` the mode required. **7-0 replays against +`result_signature`**, so a step without one is not replayable and the +pair carrying it is not usable. Chained with `left_signature` this gives +the full state sequence: state 0 is `left_signature`, state *k* is step +*k-1*'s `result_signature`. + +`Verification` - `tier` (`egraph_proof` | `symbolic` | `numeric`) and +`status` (`verified` | `refuted` | `unsupported`). Recorded on every +pair. `unsupported` is a real outcome we keep, not a silent skip. + +`PairError` - retained failure row: expression id, stage, error type, +message. Same fields 1-2's `ErrorRow` wants, without importing it while +that branch is unmerged. + +## Injected interfaces + +Two protocols, both satisfied by objects the owning issues already +describe: + +- `SaturationEngine.equivalents(source) -> Iterable[Equivalent]` - 4-2 + through 4-5. Each `Equivalent` carries the id it reached, its size and + depth, and the full rule sequence that got there. +- `Verifier.verify(left, right, rule_sequence) -> Verification` - 2-6. + +Passing them in is what lets the builder be finished and tested before +either exists. It also means the fixture tests and the production run +exercise the same code path. + +## What gets rejected + +A positive survives only if it has a non-empty trace **and** verification +returns `verified`. Everything else lands in `errors`: + +| Case | Why it isn't a pair | +|---|---| +| engine raised | saturation hit a limit or blew up; recorded with the exception type | +| empty rule sequence | nothing for 7-0 to replay | +| `refuted` / `unsupported` | we don't have the proof, so we don't claim the label | +| negative that verifies as equal | a near-miss edit that preserved meaning - real, and reported, but not a negative | +| no size-matched candidate | reported rather than fixed by widening the tolerance | + +`BuildResult.counts` reports `attempted = pairs + errors`. Attempted is +the denominator, per 4-1's reporting policy. + +## Hard negatives + +Same family, same split, node count within tolerance (default 2, see +`configs/goal6_pairs.yaml`), nearest match wins, ties broken by +expression id so the draw is reproducible. Non-equivalence has to be +positively refuted by the verifier - "we couldn't prove them equal" is +not a negative label. + +The tolerance is the difficulty knob. Widen it and "which side is +bigger" starts being a winning strategy, which is exactly the shortcut +this dataset exists to close off. + +## Splits and leakage + +Both sides of a pair come from the same corpus split - `pair_split` +raises `CrossSplitPair` otherwise. Group splits work on `group_id`, so +an expression and its e-class relatives can never straddle a split. +`find_leaks(pairs)` returns every group that appears in more than one +split; the acceptance criterion is that it returns `{}` on the real +build. + +Until 4-2 merges, `group_id` falls back to the expression id. That +fallback cannot see that two ids are e-class relatives, so the +production build must run with `eclass_id` populated - a clean +`find_leaks` under the fallback is weaker evidence than it looks. + +`tag_ood` measures OOD against what train actually contained: deeper +than any train pair, or a family train never saw. Measured, not +declared, so the tags can't drift away from the data as the corpus +changes. + +## Not in here + +No tensorization (6-2), no step extraction (7-0), no training. This spec +covers the records and how they're built, nothing downstream. diff --git a/src/geml/data/pairs/__init__.py b/src/geml/data/pairs/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/src/geml/data/pairs/generate.py b/src/geml/data/pairs/generate.py new file mode 100644 index 0000000..468db91 --- /dev/null +++ b/src/geml/data/pairs/generate.py @@ -0,0 +1,186 @@ +""" +generate.py - equivalence-pair record schema and the positive-pair builder + +owned by 6-1 + +PARTIAL START. the record shapes, the builder control flow and its +failure accounting live here and are tested against fakes. the real +>=50k/5k/5k build waits on 4-4/4-5 (rule libraries), 2-6 (verifier) and +1-8 (final corpus). none of those are imported - they come in through +the two protocols below, so this module stays importable and testable +before they merge, and binds to the real engine by passing it in. + +the schema here is what 6-2, 7-0 and 8-x consume. RuleApplication in +particular is the trace unit 7-0 replays, so changing it is a contract +change, not a refactor. +""" +from __future__ import annotations +from dataclasses import dataclass, field +from typing import Iterable, Protocol + + +@dataclass(frozen=True) +class RuleApplication: + """one rewrite step inside a positive pair's provenance trace.""" + rule_id: str + rule_name: str + tier: str # 4-1 rule tiers: ALWAYS_SAFE | GUARDED | VERIFIED_GUARDED | ... + mode: str # 4-1 rewrite modes: SAFE_REAL | POSITIVE_REAL_FORMAL + site_id: str # the node / e-class the rule fired on + result_signature: str # exact structural signature after the step - 7-0 replays against this + assumptions: tuple[str, ...] = () + + +@dataclass(frozen=True) +class Verification: + tier: str # "egraph_proof" | "symbolic" | "numeric" + status: str # "verified" | "refuted" | "unsupported" + detail: str | None = None + + +@dataclass(frozen=True) +class SourceExpression: + """the slice of a 1-2 corpus row this builder actually needs.""" + expression_id: str + split: str + family: str + size: int + max_depth: int + signature: str | None = None # 3-1 structural signature - the starting state 7-0 replays from + eclass_id: str | None = None # set once 4-2 e-classes exist; group key falls back to the id + + +@dataclass(frozen=True) +class PairRecord: + pair_id: str + left_expression_id: str + right_expression_id: str + label: str # "equivalent" | "not_equivalent" + split: str + group_id: str # leakage unit - see splits.py + family: str + max_depth: int + left_size: int + right_size: int + verification: Verification + left_signature: str | None = None # state the trace starts from; without it 7-0 can't replay step 0 + rule_sequence: tuple[RuleApplication, ...] = () + step_distance: int | None = None + negative_kind: str | None = None # negatives only, see negatives.py + eval_tags: tuple[str, ...] = () # "depth_ood" | "family_ood" + + +@dataclass(frozen=True) +class PairError: + """retained failure row - same fields 1-2's ErrorRow needs, without importing it.""" + expression_id: str | None + stage: str + error_type: str + message: str + + +@dataclass +class BuildResult: + pairs: list[PairRecord] = field(default_factory=list) + errors: list[PairError] = field(default_factory=list) + + @property + def counts(self) -> dict[str, int]: + # attempted is the denominator we report on - 4-1's reporting policy + return { + "attempted": len(self.pairs) + len(self.errors), + "pairs": len(self.pairs), + "errors": len(self.errors), + } + + +@dataclass(frozen=True) +class Equivalent: + """one saturation hit: an expression equal to the source, plus how we got there.""" + expression_id: str + size: int + max_depth: int + rule_sequence: tuple[RuleApplication, ...] + + +class SaturationEngine(Protocol): + """4-2/4-3/4-4/4-5 side. real implementation runs the e-graph to saturation.""" + + def equivalents(self, source: SourceExpression) -> Iterable[Equivalent]: ... + + +class Verifier(Protocol): + """2-6 side. status is 'verified' when the two sides really are equal.""" + + def verify( + self, left: str, right: str, rule_sequence: tuple[RuleApplication, ...] + ) -> Verification: ... + + +def build_positive_pairs( + sources: Iterable[SourceExpression], + engine: SaturationEngine, + verifier: Verifier, + *, + max_per_source: int | None = None, +) -> BuildResult: + """ + saturate each source, keep every equivalent it reaches as a positive + pair carrying its full rule sequence. + + a pair only survives if verification says 'verified'. anything else - + an engine blow-up, an empty trace, a refuted or unsupported result - + becomes an error row. nothing gets dropped quietly. + """ + result = BuildResult() + for source in sources: + try: + hits = list(engine.equivalents(source)) + except Exception as error: + result.errors.append( + PairError(source.expression_id, "saturation", type(error).__name__, str(error)) + ) + continue + + for hit in hits[:max_per_source] if max_per_source is not None else hits: + if not hit.rule_sequence: + # no trace means nothing for 7-0 to replay, so it isn't a usable positive + result.errors.append( + PairError( + source.expression_id, "provenance", "EmptyRuleSequence", + f"no rule sequence for {hit.expression_id}", + ) + ) + continue + + verification = verifier.verify( + source.expression_id, hit.expression_id, hit.rule_sequence + ) + if verification.status != "verified": + result.errors.append( + PairError( + source.expression_id, "verification", verification.status, + f"{hit.expression_id}: {verification.detail or verification.tier}", + ) + ) + continue + + result.pairs.append( + PairRecord( + pair_id=f"{source.expression_id}~{hit.expression_id}", + left_expression_id=source.expression_id, + right_expression_id=hit.expression_id, + label="equivalent", + split=source.split, + group_id=source.eclass_id or source.expression_id, + family=source.family, + max_depth=max(source.max_depth, hit.max_depth), + left_size=source.size, + right_size=hit.size, + verification=verification, + left_signature=source.signature, + rule_sequence=hit.rule_sequence, + step_distance=len(hit.rule_sequence), + ) + ) + return result diff --git a/src/geml/data/pairs/negatives.py b/src/geml/data/pairs/negatives.py new file mode 100644 index 0000000..bf64eb2 --- /dev/null +++ b/src/geml/data/pairs/negatives.py @@ -0,0 +1,102 @@ +""" +negatives.py - size-matched hard negatives + +owned by 6-1 + +PARTIAL START. the matching and rejection logic is real and runs now; +what waits is the structural edit source (4-3's rewrite machinery, or a +same-family draw from the 1-8 corpus) and the 2-6 verifier that has to +actually refute each candidate. both are passed in. + +"hard" means the negative looks like the positive: same family, size +within tolerance. an easy negative (sin(x) vs 12) teaches a model to +count nodes, which is exactly the shortcut this dataset exists to deny. +""" +from __future__ import annotations +from typing import Iterable, Sequence + +from geml.data.pairs.generate import ( + BuildResult, PairError, PairRecord, SourceExpression, Verifier, +) + + +def size_matched( + target_size: int, + candidates: Sequence[SourceExpression], + *, + tolerance: int, +) -> SourceExpression | None: + """ + closest candidate by node count, ties broken by expression_id so the + same corpus and the same tolerance always pick the same negative. + returns None when nothing lands inside tolerance - the caller reports + that rather than widening the window on its own. + """ + within = [c for c in candidates if abs(c.size - target_size) <= tolerance] + if not within: + return None + return min(within, key=lambda c: (abs(c.size - target_size), c.expression_id)) + + +def build_negative_pairs( + sources: Iterable[SourceExpression], + pool: Sequence[SourceExpression], + verifier: Verifier, + *, + tolerance: int, + negative_kind: str = "same_family", +) -> BuildResult: + """ + one negative per source, drawn from same-family same-split candidates + and confirmed non-equivalent. + + the verifier has to come back 'refuted'. a candidate that verifies as + equal isn't a mistake worth hiding - near-miss edits do sometimes + preserve meaning - but it can't be labelled a negative, so it becomes + an error row instead. + """ + result = BuildResult() + for source in sources: + candidates = [ + c for c in pool + if c.expression_id != source.expression_id + and c.family == source.family + and c.split == source.split + ] + match = size_matched(source.size, candidates, tolerance=tolerance) + if match is None: + result.errors.append( + PairError( + source.expression_id, "negatives", "NoSizeMatch", + f"no same-family candidate within +/-{tolerance} nodes of {source.size}", + ) + ) + continue + + verification = verifier.verify(source.expression_id, match.expression_id, ()) + if verification.status != "refuted": + result.errors.append( + PairError( + source.expression_id, "negatives", f"not_refuted:{verification.status}", + f"{match.expression_id}: {verification.detail or verification.tier}", + ) + ) + continue + + result.pairs.append( + PairRecord( + pair_id=f"{source.expression_id}!{match.expression_id}", + left_expression_id=source.expression_id, + right_expression_id=match.expression_id, + label="not_equivalent", + split=source.split, + group_id=source.eclass_id or source.expression_id, + family=source.family, + max_depth=max(source.max_depth, match.max_depth), + left_size=source.size, + right_size=match.size, + verification=verification, + negative_kind=negative_kind, + ) + ) + return result diff --git a/src/geml/data/pairs/splits.py b/src/geml/data/pairs/splits.py new file mode 100644 index 0000000..b39f0e4 --- /dev/null +++ b/src/geml/data/pairs/splits.py @@ -0,0 +1,77 @@ +""" +splits.py - group splits, leakage detection, OOD tagging + +owned by 6-1 + +this one needs nothing unmerged - it's pure bookkeeping over PairRecords, +so it's finished rather than a skeleton. the group key is the e-class id +when 4-2 gives us one and the expression id until then; that fallback is +weaker (it can't see that two ids are e-class relatives), which is why +the real build must run with eclass_id populated. +""" +from __future__ import annotations +from collections import defaultdict +from dataclasses import replace +from typing import Iterable, Sequence + +from geml.data.pairs.generate import PairRecord + +# frozen by 1-2 - pairs never invent a split name of their own +SPLITS: tuple[str, ...] = ("train", "validation", "test_iid", "test_ood") + + +class CrossSplitPair(ValueError): + """both sides of a pair have to come from the same corpus split.""" + + +def pair_split(left_split: str, right_split: str) -> str: + if left_split != right_split: + raise CrossSplitPair(f"{left_split} != {right_split}") + if left_split not in SPLITS: + raise CrossSplitPair(f"unknown split {left_split!r}") + return left_split + + +def find_leaks(pairs: Iterable[PairRecord]) -> dict[str, tuple[str, ...]]: + """ + group_id -> the splits it shows up in, for every group that shows up + in more than one. empty dict means no leakage. this is the check the + acceptance criterion asks for, so it stays cheap enough to run over + the full 60k set in CI. + """ + seen: dict[str, set[str]] = defaultdict(set) + for pair in pairs: + seen[pair.group_id].add(pair.split) + return {g: tuple(sorted(s)) for g, s in seen.items() if len(s) > 1} + + +def tag_ood(pairs: Sequence[PairRecord]) -> tuple[PairRecord, ...]: + """ + tag the evaluation pairs that sit outside what train actually covered: + deeper than any training pair (depth_ood) or from a family train never + saw (family_ood). both are measured against the train split rather + than declared up front, so the tags can't drift away from the data. + + train pairs are returned untouched - they define the reference, they + can't be OOD relative to themselves. + """ + train = [p for p in pairs if p.split == "train"] + max_train_depth = max((p.max_depth for p in train), default=0) + train_families = {p.family for p in train} + + tagged = [] + for pair in pairs: + if pair.split == "train": + tagged.append(pair) + continue + tags = [] + if pair.max_depth > max_train_depth: + tags.append("depth_ood") + if pair.family not in train_families: + tags.append("family_ood") + tagged.append(pair if not tags else _with_tags(pair, tuple(tags))) + return tuple(tagged) + + +def _with_tags(pair: PairRecord, tags: tuple[str, ...]) -> PairRecord: + return replace(pair, eval_tags=tuple(dict.fromkeys(pair.eval_tags + tags))) diff --git a/tests/data/test_pairs.py b/tests/data/test_pairs.py new file mode 100644 index 0000000..7121d61 --- /dev/null +++ b/tests/data/test_pairs.py @@ -0,0 +1,199 @@ +""" +tests/data/test_pairs.py - owned by 6-1. tiny fixtures only. + +the e-graph and the verifier are faked here on purpose: the point of the +partial start is that the builder's control flow, the negative matching +and the split bookkeeping are provable before 4-4/4-5/2-6 merge. when +they do, the fakes get swapped for the real objects and these tests keep +their meaning. +""" +import pytest + +from geml.data.pairs.generate import ( + Equivalent, PairRecord, RuleApplication, SourceExpression, Verification, + build_positive_pairs, +) +from geml.data.pairs.negatives import build_negative_pairs, size_matched +from geml.data.pairs.splits import CrossSplitPair, find_leaks, pair_split, tag_ood + + +def _expr(expr_id, *, split="train", family="algebraic", size=10, depth=3, eclass=None): + return SourceExpression( + expression_id=expr_id, split=split, family=family, size=size, max_depth=depth, + signature=f"sig:{expr_id}", eclass_id=eclass, + ) + + +def _step(rule_id="R1", site="n0"): + return RuleApplication( + rule_id=rule_id, rule_name="add_zero", tier="ALWAYS_SAFE", mode="SAFE_REAL", + site_id=site, result_signature=f"sig:{rule_id}:{site}", + ) + + +class FakeEngine: + """saturation stand-in. maps expression_id -> the hits it 'reaches'.""" + + def __init__(self, hits, explode=()): + self.hits = hits + self.explode = set(explode) + + def equivalents(self, source): + if source.expression_id in self.explode: + raise RuntimeError("node limit") + return self.hits.get(source.expression_id, []) + + +class FakeVerifier: + """returns whatever status the fixture asks for, defaulting to verified.""" + + def __init__(self, statuses=None, default="verified"): + self.statuses = statuses or {} + self.default = default + + def verify(self, left, right, rule_sequence): + status = self.statuses.get((left, right), self.default) + return Verification(tier="egraph_proof", status=status, detail="fixture") + + +# --------------------------------------------------------------------- +# positives: provenance and honest failure accounting +# --------------------------------------------------------------------- + +def test_positive_pair_carries_replayable_trace(): + source = _expr("e1") + engine = FakeEngine({"e1": [Equivalent("e2", 11, 3, (_step("R1"), _step("R2", "n4")))]}) + result = build_positive_pairs([source], engine, FakeVerifier()) + + assert len(result.pairs) == 1 + pair = result.pairs[0] + assert pair.label == "equivalent" + assert pair.step_distance == 2 == len(pair.rule_sequence) + assert [s.rule_id for s in pair.rule_sequence] == ["R1", "R2"] + assert pair.verification.tier == "egraph_proof" + # 7-0 replays from left_signature; a trace without a starting state is dead weight + assert pair.left_signature == "sig:e1" + + +def test_traceless_equivalent_is_rejected_not_kept(): + """a positive with no rule sequence is useless to 7-0, so it can't be a pair.""" + engine = FakeEngine({"e1": [Equivalent("e2", 10, 3, ())]}) + result = build_positive_pairs([_expr("e1")], engine, FakeVerifier()) + + assert result.pairs == [] + assert result.errors[0].error_type == "EmptyRuleSequence" + + +def test_unverified_equivalent_becomes_an_error_row(): + engine = FakeEngine({"e1": [Equivalent("e2", 10, 3, (_step(),))]}) + verifier = FakeVerifier({("e1", "e2"): "unsupported"}) + result = build_positive_pairs([_expr("e1")], engine, verifier) + + assert result.pairs == [] + assert result.errors[0].stage == "verification" + + +def test_engine_failure_is_retained_and_counted(): + engine = FakeEngine({"e2": [Equivalent("e3", 10, 3, (_step(),))]}, explode=["e1"]) + result = build_positive_pairs([_expr("e1"), _expr("e2")], engine, FakeVerifier()) + + assert result.counts == {"attempted": 2, "pairs": 1, "errors": 1} + assert result.errors[0].error_type == "RuntimeError" + + +def test_max_per_source_caps_the_fan_out(): + hits = [Equivalent(f"e{i}", 10, 3, (_step(),)) for i in range(5)] + result = build_positive_pairs( + [_expr("e0")], FakeEngine({"e0": hits}), FakeVerifier(), max_per_source=2 + ) + assert len(result.pairs) == 2 + + +# --------------------------------------------------------------------- +# negatives: size matching is the whole difficulty knob +# --------------------------------------------------------------------- + +def test_size_match_picks_nearest_and_is_deterministic(): + pool = [_expr("a", size=20), _expr("b", size=12), _expr("c", size=12)] + # b and c tie on distance; expression_id breaks it the same way every run + assert size_matched(11, pool, tolerance=5).expression_id == "b" + assert size_matched(11, pool, tolerance=5) is size_matched(11, list(reversed(pool)), tolerance=5) + + +def test_size_match_refuses_to_widen_the_window(): + assert size_matched(10, [_expr("a", size=40)], tolerance=3) is None + + +def test_negative_pair_needs_a_refutation(): + source = _expr("e1", size=10) + pool = [_expr("e9", size=11)] + result = build_negative_pairs([source], pool, FakeVerifier(default="refuted"), tolerance=2) + + assert len(result.pairs) == 1 + assert result.pairs[0].label == "not_equivalent" + assert result.pairs[0].negative_kind == "same_family" + + +def test_accidentally_equivalent_candidate_is_not_labelled_negative(): + """a near-miss edit that turns out to preserve meaning gets reported, not mislabelled.""" + result = build_negative_pairs( + [_expr("e1", size=10)], [_expr("e9", size=10)], FakeVerifier(default="verified"), + tolerance=2, + ) + assert result.pairs == [] + assert result.errors[0].error_type == "not_refuted:verified" + + +def test_negative_never_crosses_family_or_split(): + source = _expr("e1", size=10, family="trig", split="train") + pool = [_expr("wrong_family", size=10, family="algebraic"), + _expr("wrong_split", size=10, family="trig", split="validation")] + result = build_negative_pairs([source], pool, FakeVerifier(default="refuted"), tolerance=2) + + assert result.pairs == [] + assert result.errors[0].error_type == "NoSizeMatch" + + +# --------------------------------------------------------------------- +# splits: leakage is the acceptance criterion that actually bites +# --------------------------------------------------------------------- + +def _pair(pair_id, *, split, group, family="algebraic", depth=3): + return PairRecord( + pair_id=pair_id, left_expression_id="l", right_expression_id="r", label="equivalent", + split=split, group_id=group, family=family, max_depth=depth, left_size=10, right_size=10, + verification=Verification("egraph_proof", "verified"), + ) + + +def test_cross_split_pair_is_rejected(): + with pytest.raises(CrossSplitPair): + pair_split("train", "validation") + with pytest.raises(CrossSplitPair): + pair_split("dev", "dev") + assert pair_split("train", "train") == "train" + + +def test_clean_splits_report_no_leaks(): + pairs = [_pair("p1", split="train", group="g1"), _pair("p2", split="test_iid", group="g2")] + assert find_leaks(pairs) == {} + + +def test_group_on_both_sides_of_a_split_is_caught(): + pairs = [_pair("p1", split="train", group="g1"), _pair("p2", split="test_iid", group="g1")] + assert find_leaks(pairs) == {"g1": ("test_iid", "train")} + + +def test_ood_tags_are_measured_against_train_not_declared(): + pairs = [ + _pair("t1", split="train", group="g1", family="algebraic", depth=4), + _pair("d1", split="test_ood", group="g2", family="algebraic", depth=9), + _pair("f1", split="test_ood", group="g3", family="trig", depth=2), + _pair("i1", split="test_iid", group="g4", family="algebraic", depth=3), + ] + tagged = {p.pair_id: p.eval_tags for p in tag_ood(pairs)} + + assert tagged["d1"] == ("depth_ood",) + assert tagged["f1"] == ("family_ood",) + assert tagged["i1"] == () # inside train's depth and family coverage + assert tagged["t1"] == () # train defines the reference, can't be OOD against itself