A candidate is asked whether a block that proves in three seconds can be trusted. They say yes, the tool is fast on small blocks. That is one sentence of mechanism and nothing else, and it scores 3 out of 16. The same candidate, given the four-part shape, lists what the speed could be hiding: no traffic, a disconnected property, a hidden assumption. Strong answers are not longer; they spend one sentence on each dimension the rubric grades.
Job of this lesson: teach the rubric anchors, score one weak and one strong answer to the fast-proof question, and give the five checks, with target numbers, that turn speed from a suspicion into evidence.
Each dimension scores 0 when absent, 1 when vague or wrong, 2 when right but generic, 3 when specific and mostly correct, and 4 when specific, correct, and anticipating failure modes with checks. The total is 16: 13 or more is a strong answer, 9 to 12 acceptable, below 9 misses a dimension. Panels calibrate differently, but the shape is stable: specifics earn 3s, failure modes earn 4s.
Dimension | Scores 2 (generic) | Scores 3 (specific) | Scores 4 (anticipates failure) |
|---|---|---|---|
Assumption | Some assumptions were made. | Reset is synchronous active high for one cycle; inputs are free except the named protocol rule. | Plus: the excluded input class and where it is verified instead. |
Mechanism | The tool unrolls the design. | Bounded check to depth N; induction base plus step at k; the failing step named. | Plus: why that k closes and what a counterexample to induction would mean. |
Trade-off | We could try harder. | Bounded to 20 versus full induction; small parameter versus tracked-slot abstraction. | Plus: what flips the choice, with the cost in the same units. |
Evidence | It passes and covers pass. | Antecedent cover reached at step S; mutation kills the property; cone lists the signals. | Plus: the ledger entry tying result to RTL revision and assumption list. |
The fast-proof question answered weakly: the block is small, so three seconds is plausible, and it passed, so it is clean. Assumption 1, Mechanism 1, Trade-off 0, Evidence 1: total 3. Answered strongly: the speed is consistent with the 4-entry FIFO property set closing at induction depth 2, but speed is also the signature of vacuity, so the answer lists the five checks below and the number each must show. Assumption 3, Mechanism 3, Trade-off 3, Evidence 4: total 13.
No proof is believed until all five hold, each with a number to show.
Check | What it catches | Acceptance evidence (target) |
|---|---|---|
Antecedent cover | A trigger that never fires | 100 per cent of antecedent covers reached, each with its step. |
Activity cover | Reset held or an idle environment | At least one real-traffic cover reached within the bound. |
Cone contents | A disconnected property | Every signal the property names is in its cone; none missing. |
Mutation | A property that cannot fail | 100 per cent of the injected bugs, one per property class, killed at stated steps. |
Assumption list | An assume that hides a bug | Zero unowned assumptions: each has an owner and a neighbour assertion. |
The scorer adds the four dimensions and refuses a total when any dimension is missing, because a missing dimension is the commonest way a correct answer fails. The second call shows the guard working: a mechanism-only answer is rejected, not scored low.
def score(answer):
dims = ["assumption", "mechanism", "tradeoff", "evidence"]
for d in dims:
assert d in answer, "missing dimension: " + d
assert 0 <= answer[d] <= 4, "out of range: " + d
return sum(answer[d] for d in dims)
weak = {"assumption": 1, "mechanism": 1, "tradeoff": 0, "evidence": 1}
assert score(weak) == 3, score(weak)
strong = {"assumption": 3, "mechanism": 3, "tradeoff": 3, "evidence": 4}
assert score(strong) == 13, score(strong)
# The failing variant: a mechanism-only answer must be rejected, not totalled.
try:
score({"mechanism": 4})
raise SystemExit("scorer accepted a missing dimension")
except AssertionError as e:
assert "missing dimension" in str(e), e
print("PASS: weak 3/16, strong 13/16, missing dimension rejected")Every dimension is visible: assumptions before the mechanism uses them, an alternative costed, a check named.
Numbers come from runs: depths, steps and cone sizes are quoted with the run that produced them.
A bounded result is never filed as a proof: it says bounded to N with its justification beside it.
Nearly: reached covers plus a fast proof fit a small cone, but belief also needs mutation and the assumption list, because covers do not catch an assumption that hides a bug.