environment · mutation blind spots

blind-spot: an RTL mutation task the verdicts could not see

Four thousand certified verdicts could not see this mutant

A hardware comparator decides whether two integer vectors are at least 60° apart — u·v ≤ 0 or 4(u·v)² ≤ (u·u)(v·v), eleven 3-bit coordinates a side. A corpus of 14.95 million pairs from finished, certified mathematics is the testbench anyone would reach for first. Then MCY mutates the netlist 400 ways and runs four testbenches of 4,000 pairs against every mutant: a stratified sample of that corpus, and three families built to look where it cannot. The corpus sample misses 98 of the 348 mutations some pair can kill, and for 46 of them only one of the three families sees anything at all. The task is to name a pair that tells the mutant from the design.

There is no answer key, no judge and no tolerance. A kill is checked by simulating the actual netlist under the actual mutation; EQUIVALENT is checked against a SAT proof on a hand-written miter. 348 mutations carry a verified witness, 51 are proved equivalent, and the identity mutation is in the pool as a control that must be recognised rather than killed.

Where the corpus cannot look

400 mutations, by region of the netlist
p = u.v62s = u.u54t = v.v49trivial branch3box check165verdict logic30cmp width guard18cmp multipliers10cmp compare8
covered two or more testbenches see it 302mint only only the minted family sees it 8outbox only only out-of-box inputs see it 35aligned only only aligned inputs see it 3nochange proved equivalent — nothing to see 51identity the unmutated design 1
read the shapes, not the shade a filled dot is a mutation two or more testbenches catch; a ring or a square is one only one constructed family catches; a cross is one a proof says changes nothing. The blind spots are not scattered — 33 of the 46 sit in the box check, the part of the design that only an invalid input drives to refuse, which is where a corpus of valid inputs does not reach. a filled dot is not the corpus MCY tags a mutation COVERED when two or more of its four testbenches kill it, and 52 of the 302 dots get past the corpus sample, caught by the constructed families alone — 98 misses in all, with the 46 rings and squares.

Name a pair yourself

the specification, run here — not the netlist
this is the specification, not the grader it computes what the UNMUTATED design decides: in-box, then p = u·v, then 4p² against s·t. It does not grade a kill. A kill is a simulation of the actual netlist under the actual mutation, and that runs offline — which is the whole point of the environment, and the reason this box cannot tell you whether your pair breaks anything. coordinates are read strictly in −4..3 and a 4 is refused rather than masked to −4. Masking would silently test a pair you did not name, and −4 is a legitimate out-of-box value that half of every recorded kill used.

Knowing the family is not the pair

the reference policies, by class
eight pairs from …
covered
mint only
outbox only
aligned only
nochange
identity
corpus8
31/36
0/17
0/20
0/8
0/22
0/17
mint8
34/36
8/17
0/20
0/8
0/22
0/17
outbox8
1/36
0/17
3/20
0/8
0/22
0/17
aligned8
21/36
0/17
0/20
0/8
0/22
0/17
union8
30/36
3/17
2/20
0/8
0/22
0/17
sat
36/36
17/17
20/20
8/8
22/22
17/17
the out-of-box family sees all 35 of its own mutants as a family of 4,000 pairs — that is what the class means — and 79 of the 348 killable ones overall. Eight random members of it kill 3 of 20 of the mutants only it can see, and every eight-pair shotgun kills 0 of 8 of the aligned-only ones. A mutant on the box check of ONE coordinate is killed only by pairs that spoil THAT coordinate — 8.1–9.6 in a hundred of the family, depending on the coordinate. dotted eight random pairs are one draw of the many a policy could make, seeded by the task; another draw kills other mutants, so every shotgun count is chosen. sat draws nothing, and its row is decided. so the class names the family and the defect names the member and only the member is a kill. That is the whole environment: the profile rung hands the model the family and watches what it does with it.
decided
exact arithmetic backs it
chosen
one member of a set the data admits
why these numbers stand as they do
  • chosen — one seeded draw of eight pairs per task; another draw scores otherwise

The reference table

40 tasks per rung, seed 2026, no API key
policy
located
profile
blind
all
solved
false claims
abstain · answers UNDECIDED to everything
+0.000
+0.000
+0.000
+0.000
0/120
0
never · answers EQUIVALENT to everything
−0.200
−0.450
−0.400
−0.350
39/120
81
random8 · eight random pairs
−0.225
−0.125
−0.150
−0.167
19/120
39
corpus8 · eight pairs drawn from the corpus
−0.125
+0.000
−0.075
−0.067
31/120
39
mint8 · eight from the minted family
−0.125
+0.100
+0.100
+0.025
42/120
39
outbox8 · eight from the out-of-box family
−0.350
−0.250
−0.275
−0.292
4/120
39
aligned8 · eight from the aligned family
−0.225
−0.150
−0.075
−0.150
21/120
39
union8 · eight drawn from all four
−0.100
+0.050
−0.050
−0.033
35/120
39
profile · reads the profile rung, then eight from the first family that sees it
−0.100
+0.625
−0.050
+0.158
47/120
28
sat · the SAT witness, or the proof
+1.000
+1.000
+1.000
+1.000
120/120
0
+1 a pair that flips a pin, or EQUIVALENT on a design the miter proved unchanged. 0 a miss, an UNDECIDED, or a reply that could not be read. −1 a false claim either way — a kill declared on a design that cannot change, or a gap declared closed on one that can. the ceiling is published sat scores +1.000 on every rung, because the environment knows the answer it will not tell you. dotted the rows that draw their pairs at random. The false-claim column does not depend on the draw — a shotgun claims a kill on every task, so it is wrong on every equivalent one — and carries no mark.
why these numbers stand as they do
  • chosen — one seeded draw of eight pairs per task; another draw scores otherwise

Three models

108 calls · refusals counted apart, never reworded
model
located
profile
blind
all
solved
wrong
declined
Opus 5
+1.000
∅
+0.091
+0.500
13
3
16
Sonnet 5
+0.750
+0.167
+0.000
+0.306
15
4
0
Haiku 4.5
+0.417
−0.417
+0.000
+0.000
10
10
0
the profile rung cannot evaluate Opus as written it declined all twelve of them on a content policy, plus three located tasks and one blind task — 16 in all, the declined column — so its profile cell is ∅: there is no mean of nothing. That is recorded as a fact and the prompt was not reworded to get past the classifier — a rung that only scores the models willing to answer it is not measuring what it claims to. half of every kill went outside the box 16 of the 32 kills used a −4 coordinate, which the declared input box excludes. The thesis, showing up as a diagnostic rather than as a score. dotted every model number is one sample of that model’s replies: each reply is graded exactly, but the replies are a draw, and a rerun draws others. two gaps declared closed × Sonnet 5 called mutation 350 EQUIVALENT, and Haiku 4.5 called mutation 180 EQUIVALENT. EQUIVALENT says no valid pair tells that mutant from the design, and the SAT witness on its card above is such a pair — an object you can load, which is why these alone are marked. The other 15 wrong answers declared a kill on a design the miter proved unchanged: refuted by proof, with no pair to exhibit.
why these numbers stand as they do
  • chosen — one sample of the model’s replies — each grade decided, the sample drawn

The controls run before any model does

11 planted, 0 misbehaved
planted submission
must grade
why it is there
identity_declared_killed
WRONG −1.000
eight certified pairs against the unmutated design: nothing can flip, and claiming it costs
equivalent_declared_killed
WRONG −1.000
the miter proved this mutant changes nothing
killable_declared_equivalent
WRONG −1.000
a witness exists and the grader names it
miss_is_not_a_kill
MISSED +0.000
the corpus cannot see this mutant; a miss scores zero, not one and not minus one
nine_pairs
REFUSED_PARSE +0.000
the budget is eight
coordinate_out_of_range
REFUSED_PARSE +0.000
4 is not a 3-bit value; masking it to -4 would test a pair the model did not name
wrong_dimension
REFUSED_PARSE +0.000
the design has eleven coordinates
flat_pair
REFUSED_PARSE +0.000
a pair is {u, v}, not one list
sat_witness_kills
SOLVED +1.000
the SAT counterexample, re-run through the netlist
identity_declared_equivalent
SOLVED +1.000
the unmutated design is equivalent to itself
outbox_kill_uses_validity
SOLVED +1.000
a mutant only the out-of-box family sees, killed by an invalid input, and the grader says so
what each one pins the grade shown is what the control actually graded; every one matched, and three of the eleven deliberately pin only the outcome and leave the reward to follow from it. three of them must SCORE and that is the half people leave out. A simulator that is not live scores every submission as a miss and reports perfect refusal discipline; a suite that fails everything reports perfect coverage. Those are the same mistake, and it is the one this environment is named for.

How a verdict is reached, and what it is worth

One control design carries all 400 mutations under a select input, so a kill is four thousand simulated records a second rather than four hundred rebuilds. EQUIVALENT is a yosys sat proof on a hand-written miter — 356 seconds for the whole pool on this laptop — and every witness the prover returns is re-run through the simulator before it is believed.

This environment was ported into this repository and its labels were re-derived here, not copied. The SAT run was repeated on this machine and compared against the source lab's own record: every mutation id, label, class, profile, mutation text, witness pair and witness pin-pair is identical, 400 of 400 on each. The only fields that differ anywhere in the record are the SAT timings, which are the machine and not the mathematics.

What it certifies is arithmetic about one elaborated netlist and one mutation set. It is not a claim about any shipped chip, and it does not say a corpus that misses these mutants is a bad corpus — it says a coverage number computed from valid inputs cannot see a defect that only invalid inputs reach, which is a statement about the measurement, not about the people who took it.

cd environments/blind_spot && python3 -m pytest tests -q
python3 -m blind_spot gate
python3 -m blind_spot baseline --n 40
python3 environments/blind_spot/battery.py
node playground/build.js

contact

Write to Carlos

Sent by Web3Forms to Carlos’s inbox; nothing stored here.

Or write to carlos@carlostoledo.co, or open the public pilot form on GitHub.