Why it matters

Two blocks report full cone coverage. One is proven unboundedly; the other is bounded to 12 with its induction step still open and several assumptions it leans on. The numbers match and the evidence does not. This lesson is the sceptic's checklist that stops the first block's number being spent on the second block's proof.

The core idea

Coverage numbers do not measure proof depth or assumption quality, and they cannot, because they count what was examined, not how hard it was examined. Every coverage claim therefore travels with companions: the bound each proof reached with its justification, the assumption list with its influence table, and the mutation score. A sign-off row with coverage but no bound is rejected by the ledger check below, automatically and without debate.

Worked example: the same number, different evidence

Two illustrative designs, both at full cone coverage. One proved every property by induction; the other is bounded to 12 with the induction step still open. The script rejects any sign-off row that claims coverage without a bound, and rejects bounded rows without a justification. The numbers are illustrative; the gate is the point.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34

# illustrative: sign-off gate rejects coverage without a bound
rows = [
    {"block": "alu-a", "cone_cov": 1.0, "status": "proven", "bound": None,
     "just": "k-induction proof", "mut": 1.0},
    {"block": "alu-b", "cone_cov": 1.0, "status": "bounded", "bound": 12,
     "just": None, "mut": 0.8},
]

def gate(row):
    if row["cone_cov"] < 1.0:
        return "incomplete coverage"
    if row["status"] == "bounded" and row["bound"] is None:
        return "coverage without a bound"
    if row["status"] == "bounded" and not row["just"]:
        return "bounded without justification"
    if row["status"] == "proven" and not row["just"]:
        return "proven without an argument"
    if row["mut"] < 1.0:
        return "surviving mutants"
    return "ok"

assert gate(rows[0]) == "ok"
# the bounded row fails the gate: no justification is recorded
assert gate(rows[1]) == "bounded without justification", gate(rows[1])
# a bounded row with no bound at all is coverage without a bound
assert gate(dict(rows[1], bound=None)) == "coverage without a bound"
# a proven row with no argument is rejected too
assert gate(dict(rows[0], just=None)) == "proven without an argument"
# with a justification the row passes the bound rules and now fails only on its mutation score
fixed = dict(rows[1], just="reset 1 + trigger 6 + latency 4 + 1 = 12")
assert gate(fixed) == "surviving mutants", gate(fixed)
# and with every mutant killed it ships
assert gate(dict(fixed, mut=1.0)) == "ok"
print("PASS: proven row accepted; unjustified, unbounded and surviving-mutant rows each rejected")

What the reviewer looks for

• No coverage number appears without its bound, its assumption count, and its mutation score on the same row.

• Bounded rows carry a justification reference; unproven rows carry a waiver, never a bare number.

• Two identical coverage numbers with different companions are never treated as equal evidence.

Verify and debug

Audit the report, not the design: pick three rows and reproduce each companion by hand. Re-run one proof at its stated bound, remove one load-bearing assumption and watch the result move, and re-inject one killed mutant. If any companion does not reproduce, the row is decoration and the sign-off stops until it is repaired.

Related topics

• Bounded Proof Signoff: The Proof Status Ledger

• The Formal Signoff Package: The Signoff Checklist in Full