{"data":{"kind":"file","path":"README.md","version_id":"akyogo3f72mzawtodfye6x8z","entry":{"name":"README.md","path":"README.md","is_directory":false,"size":23953,"modified_at":"2026-09-10T13:25:29.066000","content_hash":"2cb6adab729faac11bac31ffda6a5be750e181e9d8ae6c206e693bdc1a598f0d"},"entries":[],"content":"# blind-spot\n\nFourteen million certified verdicts could not see this mutant. Name the input\npair that does, or prove there is none.\n\n```bash\npip install blind-spot\n```\n\n```python\nimport verifiers as vf\nenv = vf.load_environment(\"blind-spot\")          # a SingleTurnEnv over the mutation pool\n```\n\nNeeds `yosys`, `iverilog` and `vvp` on PATH (`brew install yosys icarus-verilog`);\n`design.tools_missing()` names them if they are absent rather than failing\nsomewhere deeper. The four hundred SAT labels ship with the package; the\nsimulator is a compiled binary and is built on first use, about forty seconds\n(`python -m blind_spot sim` does it explicitly).\n\n**There is no answer key.** A kill is verified by simulating the actual netlist\nunder the actual mutation; EQUIVALENT is checked against a SAT proof on a\nhand-written miter. Nothing is matched against a stored string, so there is\nnothing to leak.\n\n---\n\n## The fact this environment is built from\n\nThe kissing predicate — `u.v <= 0 or 4(u.v)^2 <= (u.u)(v.v)` for two vectors in\nZ^11 with 3-bit coordinates — was put into RTL and proved sound over every\ninput. Then yosys mutated the netlist four hundred times, one bent bit of one\ncell's port each, and the testbench everyone would reach for first was run\nagainst every mutant: **14,951,649 pair verdicts from finished, certified\nmathematics**, 1,468,680 of them exactly on the decision boundary.\n\nIt could not see the comparator constant. Replacing the 4 with a 3 or a 2\nchanges zero of fourteen million verdicts, because every vector in that corpus\nhas norm 4. A testbench drawn from certified mathematics contains only valid\ninputs, so it cannot test the code that rejects invalid ones; it never varies\nthe norms, so it cannot see a defect that only shows when they differ; it never\nmakes a large dot product, so the high bits of the multipliers are dark. Four\nconstructed families — near-boundary pairs with different norms, pairs with a\ncoordinate out of the declared box, pairs with `|u.v|` near its maximum, and\nthe corpus itself — each named by what survived the last, got to zero survivors.\n\n**The interesting region is measure-zero to a sampler and reachable by hand.**\nThat is the fact. This environment asks whether a model can reach it.\n\n---\n\n## The task\n\nOne mutation may have been applied to the netlist, or none. The model is asked\nfor **one to eight input pairs on which the mutant's three output pins differ\nfrom the original's**, or for the claim **EQUIVALENT** — no pair with valid = 1\ncan tell them apart — or **UNDECIDED**.\n\nThere is no answer key, no judge model, and no tolerance anywhere:\n\n- a **KILL** is verified by simulating the actual netlist under the actual\n  mutation (yosys `mutate -ctrl`, one control design carrying the whole pool,\n  Icarus, a batch of four thousand pairs a second);\n- **EQUIVALENT** is checked against a SAT proof — a miter of mutant against\n  original over all inputs, MiniSAT through `yosys sat`, complete for a\n  combinational design, a quarter of a second each;\n- and every label is **certified twice**: for every mutant the miter can\n  distinguish, its counterexample is re-run through the simulator and must\n  kill. A label the simulator disagrees with raises. Killable means *here is\n  the pair*; equivalent means *proved*.\n\nThe **identity mutation** — the unmutated design — is in the pool as a class\nof its own. A testbench that fails everything reports perfect coverage, and a\nmodel that claims a kill on every task is doing the same thing. The identity is\nwhere that costs.\n\n### One dial, three rungs: how much of the defect is stated\n\n| rung | what the task gives |\n|---|---|\n| `located` | the mutation named — cell type, port, bit, how it is bent — and the netlist statement it sits in, with wire widths. Everything a verification engineer has. |\n| `profile` | the location withheld. Instead: which of the four testbench families killed the mutant and which did not. This is the move that closed the core's survivors — *the class names the family* — posed as a task. |\n| `blind` | nothing but the design. The only sound moves are to know where mutants hide, or to abstain. |\n\nNothing in a prompt names the rung's class or the label.\n\n### Scoring\n\n| outcome | reward | when |\n|---|---|---|\n| `SOLVED` | **+1** | a submitted pair flips a pin in simulation; or EQUIVALENT on a mutant the miter proved equivalent |\n| `MISSED` | 0 | KILL claimed, no pair flips a pin, and the mutant **is** killable |\n| `UNDECIDED` | 0 | |\n| `REFUSED_PARSE` | 0 | no verdict, more than eight pairs, a wrong dimension, or a coordinate no 3-bit pin can carry — **never masked** |\n| `WRONG` | **−1** | KILL on a design proved unchanged (a false alarm); or EQUIVALENT on a mutant a pair can distinguish (a gap declared closed) |\n\nTwo diagnostics ride along at weight zero: `false_claim`, the specific failure\nthe environment exists to price, and `in_box_kill`, whether the killing pair was\na valid input — a kill that used an out-of-box coordinate used the one input the\ncertified corpus can never contain.\n\n---\n\n## The pool\n\n`python -m blind_spot pool` imports MCY's four hundred mutations from the\ncoverage run's own database, elaborates them into one control design, labels\neach by SAT and verifies each witness. On this machine:\n\n    348 killable, every witness verified in simulation\n     51 proved equivalent\n      1 identity (mutation 1, `mutate -mode none`)\n    494 s of SAT in total; labels agree with MCY's miter on 400 of 400\n\nEvery class here is a class from the published coverage run: `COVERED` (the\ncorpus kills it), `MINT_ONLY`, `OUTBOX_ONLY`, `ALIGNED_ONLY` (only that\nconstructed family does), `NOCHANGE` (proved equivalent), `IDENTITY`. Tasks are\ndrawn by class with the rare classes weighted up: three `ALIGNED_ONLY` mutants\nin four hundred would otherwise appear once in a hundred tasks.\n\nEquivalence is decided with `valid` held at 1, because that is what the task\nstates. A mutant that differs only when the design is not being asked is\nlisted in the pool summary under `valid0_only` rather than hidden. There are\nnone in this pool.\n\n---\n\n## What the environment scores before anything is spent\n\nTen reference policies, 40 tasks per rung, same seeds a model run uses. Each\nreads only what the prompt shows and is graded by the same simulation.\n\n| policy | `located` | `profile` | `blind` | all | solved | false claims |\n|---|---|---|---|---|---|---|\n| `abstain` — UNDECIDED always | 0.000 | 0.000 | 0.000 | 0.000 | 0/120 | 0 |\n| `never` — EQUIVALENT always | −0.200 | −0.450 | −0.400 | −0.350 | 39/120 | 81 |\n| `random8` — eight uniform in-box pairs | −0.225 | −0.125 | −0.150 | −0.167 | 19/120 | 39 |\n| `corpus8` — eight pairs from the certified corpus | −0.125 | 0.000 | −0.075 | −0.067 | 31/120 | 39 |\n| `mint8` — eight near-boundary pairs | −0.125 | +0.100 | +0.100 | +0.025 | 42/120 | 39 |\n| `outbox8` — eight out-of-box pairs | −0.350 | −0.250 | −0.275 | −0.292 | 4/120 | 39 |\n| `aligned8` — eight aligned pairs | −0.225 | −0.150 | −0.075 | −0.150 | 21/120 | 39 |\n| `union8` — two from each family | −0.100 | +0.050 | −0.050 | −0.033 | 35/120 | 39 |\n| `profile` — reads the profile rung; EQUIVALENT if no family sees it, else eight of the first that does | −0.100 | **+0.625** | −0.050 | +0.158 | 47/120 | 28 |\n| `sat` — the witness, or the proof | +1.000 | +1.000 | +1.000 | **+1.000** | 120/120 | 0 |\n\nSolved by class, all rungs:\n\n| policy | covered | mint only | outbox only | aligned only | equivalent | identity |\n|---|---|---|---|---|---|---|\n| `random8` | 19/36 | 0/17 | 0/20 | 0/8 | 0/22 | 0/17 |\n| `corpus8` | 31/36 | 0/17 | 0/20 | 0/8 | 0/22 | 0/17 |\n| `mint8` | 34/36 | 8/17 | 0/20 | 0/8 | 0/22 | 0/17 |\n| `outbox8` | 1/36 | 0/17 | 3/20 | 0/8 | 0/22 | 0/17 |\n| `union8` | 30/36 | 3/17 | 2/20 | 0/8 | 0/22 | 0/17 |\n| `profile` | 31/36 | 3/17 | 2/20 | 0/8 | 5/22 | 6/17 |\n| `sat` | 36/36 | 17/17 | 20/20 | 8/8 | 22/22 | 17/17 |\n\nThree things to read off it.\n\n**`corpus8` is the published blindness as a row.** Thirty-one of thirty-six in\nthe class the corpus already saw, and zero in every class it was blind to.\n\n**Knowing the family is not enough; the pair has to be constructed.** The\nout-of-box family kills 97 % of mutants as a family of four thousand, and eight\nrandom members of it kill almost nothing — three of twenty `OUTBOX_ONLY` mutants\n— because a mutant on the box check of one coordinate is killed only by a pair\nthat spoils *that* coordinate, about one in ten of the family. Same for\n`ALIGNED_ONLY`: zero for every shotgun. The profile tells you which family; the\ndefect tells you which member; only the second is a kill.\n\n**Every shotgun pays 39 for the same reason.** Eight pairs cannot say\nEQUIVALENT, so every one of them takes −1 on all 39 equivalent-or-identity\ntasks. `never` takes 81 the other way. Only checking wins, which is the\nbehaviour worth rewarding: an auditor that always finds something is exactly as\nuseless as one that never does. `sat` is published on purpose — this is a\nmeasurement of whether an answer checks, not a puzzle that is hard for a\nprogram.\n\n---\n\n## Controls\n\nTwo kinds, planted before any model is called, and both are needed. A forgery\nmust not score; a positive control must. A grader that always fails would pass\nevery forgery and look perfect — the exact shape of the mistake this\nenvironment is named for — so three submissions have to succeed or the run\nrefuses to report.\n\n| control | must come out | why |\n|---|---|---|\n| `identity_declared_killed` | WRONG −1 | eight certified pairs against the unmutated design: nothing can flip, and claiming it costs |\n| `equivalent_declared_killed` | WRONG −1 | the miter proved this mutant changes nothing |\n| `killable_declared_equivalent` | WRONG −1 | a witness exists and the grader names it |\n| `miss_is_not_a_kill` | MISSED 0 | eight corpus pairs on a mutant only the mint sees: zero, not one, not minus one |\n| `nine_pairs` | REFUSED_PARSE | the budget is eight |\n| `coordinate_out_of_range` | REFUSED_PARSE | a 4 masked to three bits is −4, a legitimate out-of-box value; the grader would test a pair the model never named |\n| `wrong_dimension` | REFUSED_PARSE | eleven coordinates |\n| `flat_pair` | REFUSED_PARSE | a pair is `{u, v}`, not one list |\n| `sat_witness_kills` | **SOLVED +1** | the SAT counterexample, re-run through the netlist |\n| `identity_declared_equivalent` | **SOLVED +1** | the unmutated design is equivalent to itself |\n| `outbox_kill_uses_validity` | **SOLVED +1**, `in_box_kill` false | the out-of-box pair that kills an `OUTBOX_ONLY` mutant, and the grader says the kill was an invalid input |\n\n**11 planted, 11 behaved.**\n\nThe last one was written first as *eight random out-of-box pairs* and failed —\nMISSED — which is the finding in the table above arriving as a control before it\narrived as a number. The control now submits the family member that kills, so\nit tests the grader and not the odds.\n\n---\n\n## Layout\n\n```\nblind_spot/\n├── design.py       where the design lives (BLIND_SPOT_MUT, then the package copy, then\n│                   the repository's corpus), the pin map, the design described in words\n├── families.py     the four testbench families, read from the hex MCY ran\n├── sim.py          one control design for the whole pool; simulate (mutsel, u, v) batches\n├── pool.py         import MCY's mutations, label each by SAT, verify each witness; ensure_sim()\n├── taskset.py      Task / Taskset, three rungs, grade()\n├── policies.py     ten reference policies\n├── baseline.py     the reference table, one simulator run per task\n├── forgeries.py    the controls, both kinds\n├── api.py          the framework-free surface every consumer shares: parse_reply,\n│                   task_row, sample, score, preflight\n├── adapters_v0.py  load_environment — the ONLY module that imports verifiers\n└── __main__.py     pool / sim / gate / baseline / tasks\ntests/              17 tests across four files; the controls are the suite. Eleven run\n                    without verifiers installed; the six binding tests SKIP rather than\n                    pass, because a binding test that passes without the framework is\n                    the same lie as a control that cannot fire.\neval/               run_models.py (direct API), run_verifiers.py (through the framework),\n                    page_data.py, baseline.json, results.json, verifiers-*.json\npool/               pool.json — the SAT record, committed. Everything else in here is a\n                    build artefact rebuilt from the pinned design in ~40 s.\n```\n\n`import blind_spot` is standard library only; `verifiers` is imported lazily and\nonly by `adapters_v0`, which `tests/test_framework_free.py` proves by blocking\nevery third-party import and grading a submission anyway.\n\nStandard library only. The tools are `yosys`, `iverilog` and `vvp`; `design.py`\nnames them if they are missing rather than failing somewhere else.\n\n```bash\npython3 -m blind_spot pool                 # ~6 min: 400 SAT labels + 348 witness checks\npython3 -m blind_spot sim                  # ~40 s: only the simulator, from labels on disk\npython3 -m blind_spot gate                 # the 11 controls, 3 of them positive\npython3 -m blind_spot baseline --n 40      # the reference table, ~1 min\npython3 -m pytest tests/ -q                # 17 with verifiers; 11 + 6 skipped without it\npython3 ../../environments/blind_spot/battery.py   # the whole thing, gated, ~60 s\n\n# spends money, never called by a battery:\npython3 eval/run_models.py --n 12 --live           # the direct-API run\npython3 eval/run_verifiers.py --n 36 --model claude-opus-5 --effort low\n\n# the page:\nPYTHONPATH=. python3 eval/page_data.py && (cd ../.. && node playground/build.js)\n```\n\n## Results\n\n108 calls per run, 12 tasks per rung, seed 2026, three models at low effort.\nTask mix: 9 `COVERED`, 4 `MINT_ONLY`, 10 `OUTBOX_ONLY`, 2 `ALIGNED_ONLY`,\n5 `NOCHANGE`, 6 `IDENTITY` — 25 killable, 11 equivalent.\n\n**Mean reward** (refusals excluded from the mean and counted on their own):\n\n| model | `located` | `profile` | `blind` | all answered | solved | wrong | refused |\n|---|---|---|---|---|---|---|---|\n| Opus 5 | **+1.000** (9/9) | — (12/12 refused) | +0.091 | +0.500 | 13 | 3 | 16 |\n| Sonnet 5 | +0.750 | +0.167 | 0.000 | +0.306 | 15 | 4 | 0 |\n| Haiku 4.5 | +0.417 | −0.417 | 0.000 | 0.000 | 10 | 10 | 0 |\n\n**Solved by class**, all rungs, answered tasks only:\n\n| model | covered | mint only | outbox only | aligned only | equivalent | identity |\n|---|---|---|---|---|---|---|\n| Opus 5 | 5/6 | 0/2 | 5/6 | 1/1 | 0/1 | 2/4 |\n| Sonnet 5 | 5/9 | 0/4 | 6/10 | 2/2 | 0/5 | 2/6 |\n| Haiku 4.5 | 4/9 | 1/4 | 3/10 | 0/2 | 0/5 | 2/6 |\n\n### What separates them\n\n**`located` is solvable, and the ladder separates on it.** Given the cell, the\nbent wire and its drivers, Opus constructed a killing pair on all nine tasks it\nanswered — including all four `OUTBOX_ONLY` mutants, where the pair has to put\n−4 on exactly the coordinate whose box check was bent, and the `ALIGNED_ONLY`\none, where it has to drive a high bit of the dot product. Sonnet 10 of 12,\nHaiku 6 of 12. Every model said EQUIVALENT on the identity when the record read\n`mutate -mode none`.\n\n**`blind` is where confidence is priced, and every model paid.** With nothing\nbut the design, all three claimed KILL on the equivalent and identity tasks —\nOpus 3, Sonnet 3, Haiku 3 false alarms out of the four such tasks each saw —\nand their eight pairs were, in their own words, \"the corpus blind spots:\nunequal norms, out-of-box −4, near-maximal |u.v|, the 4p² = st tie\". That is\nthe right list of families, submitted against a design that has no defect. A\nshotgun cannot say EQUIVALENT; the `never` policy and the `union8` policy\nbracket exactly this.\n\n**`profile` is where the models come apart.** Sonnet read the profile and\nabstained six times, tried six and killed two. Haiku claimed KILL on six tasks\nwhose profile said *no family sees it* — the profile was telling it the answer\nwas EQUIVALENT, and it submitted pairs anyway, for −6. Opus did not answer the\nrung at all.\n\n**Half of every model's kills used validity.** Of the killing pairs, 6 of 11\n(Opus), 6 of 13 (Sonnet) and 4 of 8 (Haiku) contained a −4 — the input the\ncertified corpus can never contain. That is `in_box_kill`, and it is the\nenvironment's thesis appearing as a diagnostic.\n\n### Opus declined the `profile` rung\n\nAll twelve `profile` calls, and three of twelve `located`, came back\n`stop_reason: refusal`, category `cyber`: *\"This request triggered restrictions\non violative cyber content.\"* The prompt describes a mutated netlist and four\ntestbenches that killed or did not kill it. **It has not been reworded to get\npast a classifier** — that cannot be told apart from rewording for clarity from\nthe inside — so the wording stands, the refusals are recorded as refusals with\nthe API's own explanation kept in `raw`, and the consequence is stated plainly:\n**as written, the `profile` rung cannot evaluate Opus.**\n\n### The first `located` run measured the prompt\n\nThe run above is the second `located` run; the first is kept in\n`eval/results-run1.json`. In the first, Opus solved 4 of 6 answered and missed\n2, Sonnet 5 of 12, Haiku 3 of 12 — and the misses were located correctly and\nkilled nothing. One reply said *\"bit 15 of the in-box AND-reduce is the v4 range\ncheck; v4 = −4 is no longer refused\"*, and spoiled v4. The mutation record said\n`-wire \\$80 -wirebit 0`, which is **u4's** check: after optimisation the bits of\na cell's port are not in the order the Verilog concatenation lists them, and the\nprompt had given the port bit and not the wire. The `located` prompt now states\nthe bent wire with its definition and one level of drivers. Same models, same\nseeds, same tasks: Opus 9 of 9, Sonnet 10 of 12, Haiku 6 of 12.\n\nThat is the same lesson as the reference table, one level up: the class names\nthe family, the record names the wire, and only the wire names the coordinate.\n\n## The page\n\n`/instruments/blind-spot`, built by `playground/blind-spot/build.js` from\n`eval/page.json`. Every number on it comes from the pool, the controls, the\nreference table and the stored runs; none is typed.\n\nThe blind-spot map is the centrepiece: one mark per mutation, placed in the\nregion of the netlist its cell was elaborated from, and **the mark carries the\nclass by SHAPE** — a filled dot when the certified corpus kills it, a ring when\nonly a constructed family does, a cross when the miter proved it changes\nnothing. A reader who cannot separate two greys can still separate a mutation\nthe corpus sees from one it does not. The map shows the finding rather than\nasserting it: the blind spots are not scattered, they sit in the `box check`.\n\n**Click a mark** (or pick from the list, which is what a keyboard reaches) and\nthe card below gives that mutation in words, the netlist statement, the bent\nwire and its drivers, the class, the four-family profile, and the SAT witness\nwith the pins it flips.\n\n**Name a pair** runs the *specification* — the predicate the unmutated design\ncomputes — on two vectors you type, and shows the arithmetic that decided it:\nin-box, then `p = u·v`, then `4p²` against `s·t`. **It does not grade a kill.**\nA kill is a simulation of the netlist under the mutation and runs offline, which\nis the whole point of the environment and the reason the box cannot tell you\nwhether your pair breaks anything. Coordinates are read strictly in −4..3 and a\n4 is refused rather than masked, the same rule the grader applies.\n\nLoad a selected mutant's witness into that box and the demonstration lands on\nits own: for an `OUTBOX_ONLY` mutation the specification answers **REFUSED**,\nbecause the witness uses a −4. The pair that kills the mutant is a pair the\ndesign declines to decide — which is exactly where a corpus of valid inputs\ncannot go.\n\n---\n\n## The framework binding is verified, not written from a doc\n\n`blind_spot/adapters_v0.py` exposes `load_environment` (a `SingleTurnEnv` with a\n`Rubric`). **It was written against a live `verifiers` install and then run\nagainst live models — not written from documentation.** Writing one from the doc\nhad already produced three defects in the sibling environment, two of them\nsilent: `load_environment` never exported from `__init__` (the Hub's own command\nwould have raised on arrival); a plain-string `task` column aborting every\nrollout; and scoring handed pydantic message objects, so a `.get(\"content\")`\nmissed and **a whole eval printed 0.000 with no error raised**. Each is designed\nout here and each has a test. `tests/test_verifiers_binding.py` SKIPS when\n`verifiers` is absent rather than passing without it.\n\nA fourth defect turned up only when the wheel was installed: `sim.simulate`\npassed the case file by absolute path, and the testbench holds that plusarg in\n`reg [1023:0] f` — 128 characters. A source tree seventy characters deep always\nworked; a site-packages path two hundred deep truncated it, `$readmemh` read\nnothing, the memory stayed X and every verdict came back `xxx` with nothing\nraised. `tests/test_long_path.py` holds the fix and was checked to fail against\nthe old call.\n\n## Run against live models\n\n`eval/run_verifiers.py` runs the real path — dataset, prompt, live model,\ncompletion, rubric — and then re-scores the framework's own completions offline.\n**108 rollouts across three models, 0 disagreements**: the framework's reward is\nthis package's reward on every one, so the framework layer owns no scoring of\nits own. `battery.py` re-scores all 108 from their stored replies on every build.\n\n| model | `located` | `profile` | `blind` |\n|---|---|---|---|\n| Claude Opus 5 | **+0.833** | +0.500 | −0.083 |\n| Claude Sonnet 5 | +0.417 | +0.250 | −0.083 |\n| Claude Haiku 4.5 | +0.417 | −0.167 | −0.167 |\n\n36 rollouts each, eval seed 4243, effort `low` (Haiku 4.5 rejects the `effort`\nparameter outright, so it runs without it). The ladder is the same shape the\ndirect-API run showed through an entirely different code path: `located` is\nsolvable and separates the models, `blind` is **negative for all three** —\nevery one of them claims a kill it cannot back — and `profile` splits them.\n\nFour things that run found and no amount of reading would have:\n\n- **Opus 5 declines the `profile` rung** — `stop_reason: refusal`, category\n  `cyber`, zero content blocks, zero output tokens. The direct-API run found the\n  same thing. The prompt was not reworded to get past the classifier, and a rung\n  that only scores the models willing to answer it is not measuring what it\n  claims to.\n- **verifiers 0.3.1 does not surface a refusal.** Its Anthropic client reports\n  `EmptyModelResponseError(\"Model returned no content and did not call any\n  tools\")`, which reads as an infrastructure fault rather than a policy decline —\n  so a retry setting will pay to retry something that can never succeed. The\n  environment still scores it 0 with `well_formed` 0, which is right: a decline\n  is not a wrong answer.\n- Its `ANTHROPIC_ADAPTIVE_THINKING_MODELS` list predates Claude Opus 5, so\n  thinking depth has to be set through `output_config.effort` in `sampling_args`.\n- The client uses `messages.create` rather than streaming, so `max_tokens` above\n  roughly 16000 fails with \"Streaming is required\" before any call is made.\n\n## What this does not claim\n\nOne predicate, one netlist, one mutation operator. Nothing here is a claim about\nthe chip, about the search it serves, or about hardware verification at large.\nIt is a claim about testbenches — a corpus can be enormous, certified and blind,\nand the blindness has a shape — and about whether a model can see that shape\nfrom a description of the design, from a profile, or from nothing.\n","encoding":"utf-8","truncated":false,"total_bytes":23953},"status":null}