Close TODO bug #1: Comparator removes the SafeVerify memory blowup

The DAG-shaped text export + kernel replay have no importModules in the
trusted process and no un-memoized rebuildExpr, retiring both unbounded-memory
sources. mem_limit drops 50g -> 16g pending the §7 peak-RSS measurement.

Author: tadamcz

TODO.md

@@ -2,23 +2,26 @@
 
 ## Known bugs
 
-### 1. SafeVerify peak memory is effectively unbounded on legitimate proofs (un-memoized `rebuildExpr`)
+### 1. SafeVerify peak memory is effectively unbounded on legitimate proofs (un-memoized `rebuildExpr`) — RESOLVED by the Comparator migration
 
-**Severity:** medium — causes deterministic scorer OOM kills (infra errors / lost samples),
-not mis-scoring. Already documented in code; tracked here for visibility.
+**Status:** resolved on the `comparator` branch (see `comparator-migration-plan.md`).
+The verifier no longer materializes the full Mathlib environment or deep-copies
+proof terms: Comparator consumes lean4export's *text* export, which serializes
+terms as a shared DAG (every subterm emitted once, by index) and replays that
+through its kernel. There is no `importModules` in the trusted process and no
+un-memoized `rebuildExpr`, so the two failure sources below are gone. The
+comparator service starts at `mem_limit: 16g` (down from `50g`), to be confirmed
+by the §7 peak-RSS measurement — in particular re-running the `(a+b+c)^16` ring
+case and the three formerly resource-bound gold proofs
+(`RESOURCE_BOUND_STEMS` in `tests/test_gold_proofs.py`).
 
-**Detail** (see `apn/task.py:96-121` and `apn/checker.py:36-44`):
-- `safe_verify` has a large fixed footprint (~27 GiB peak RSS), attributed almost
+**Original detail** (SafeVerify, now retired):
+- `safe_verify` had a large fixed footprint (~27 GiB peak RSS), attributed almost
   entirely to four `importModules` calls (two in the import-superset check, one per
   replayed file), each materializing the full Mathlib environment and never freeing it.
-- On top of that, proof *content* is unbounded: `rebuildExpr` deep-copies proof terms
+- On top of that, proof *content* was unbounded: `rebuildExpr` deep-copied proof terms
   **without memoization**, expanding pointer-shared DAGs (which tactics like `ring`
-  produce routinely) into trees. Measured: `(a+b+c)^16 = (c+b+a)^16 := by ring` compiles
+  produce routinely) into trees. Measured: `(a+b+c)^16 = (c+b+a)^16 := by ring` compiled
   agent-side in 3.5s at 6.4 GiB but blew past a 34 GiB limit in safe_verify before being
-  OOM-killed. Real submissions have reached ~43 GiB in production. `mem_limit` is set to
-  `50g` to cover the worst observation, but no limit can make scorer OOMs impossible.
-- Agent-side compile success does **not** bound the scorer's cost.
-
-**Possible fixes** (in vendored `safeverify`):
-- Memoize `rebuildExpr` so shared sub-terms are copied once.
-- Skip the redundant `importModules` in the import-superset check.
+  OOM-killed. Real submissions reached ~43 GiB in production.
+- Agent-side compile success did **not** bound the scorer's cost.