An inconclusive run tempts the team to lengthen the timeout, which works precisely when the proof was about to close and wastes the budget otherwise. The five-minute alternative is diagnosis: read what the run reported and match it to the cause. A counterexample from an illegal start is a modelling error, fixed in the harness. A passing base with a failing step is a non-inductive property, fixed with helpers. A run whose cone holds tens of thousands of bits is true complexity, fixed by reduction. Each cause has its tactic, and the wrong tactic costs the week the right one saves.
Bounded is a result, not a branch of non-convergence: it says no violation within N, honestly reported with its justification. Non-convergence tactics start after that sentence. Measure first: the cone bit count per property, the depth reached against the depth needed, engine progress in frames or clauses, and which obligation failed. Then choose. Reduce when the cone dwarfs the property: abstraction, cut points, smaller parameters. Split when one property covers several behaviours: cases by value range or mode. Strengthen when the step fails from unreachable states: helper invariants from the CTI. Assume last, when nothing else closes the gap: one justified assumption with an owner and a review, never a quiet constraint.
The script classifies eight run reports by the rule the prose states. A counterexample that does not start at reset is a modelling error; one that does is classified as a trace. A proof is filed with vacuity evidence. An inconclusive run with a passing base and a failing step is strengthened, a very large cone is reduced, several behaviours in one property are split, a depth shortfall with none of those is answered by induction or reduction and not by splitting, and only a run with none of these causes reaches the last-resort assumption. The cone limit of 5,000 bits is illustrative. A malformed report is rejected rather than guessed at. The clause-growth check prices depth with illustrative arithmetic: 50,000 gates at depth 30 need 4.56 million clauses and depth 300 needs 45.6 million, and where memory ends a run depends on the tool and the machine.
CONE_LIMIT = 5000 # illustrative: the cone size above which reduction comes first
def triage(r):
outcome = r["outcome"]
if outcome == "counterexample":
# a trace that does not start at a state reset can produce is a modelling error, not a bug
return "classify-trace" if r["starts_at_reset"] else "fix-reset-model"
if outcome == "proven":
return "file-with-vacuity-evidence"
if outcome != "inconclusive":
raise ValueError("unknown outcome: " + outcome)
if r["base"] == "pass" and r["step"] == "fail":
return "strengthen" # non-inductive: read the CTI, write helpers
if r["cone_bits"] > CONE_LIMIT:
return "reduce" # true complexity: abstract, cut, shrink parameters
if r["modes"] > 1:
return "split" # one property, several behaviours
if r["depth_reached"] < r["depth_needed"]:
return "induct-or-reduce" # a depth shortfall is answered by induction or reduction, not by splitting
return "last-resort-assume"
reports = [
({"outcome": "counterexample", "starts_at_reset": False}, "fix-reset-model"),
({"outcome": "counterexample", "starts_at_reset": True}, "classify-trace"),
({"outcome": "proven"}, "file-with-vacuity-evidence"),
({"outcome": "inconclusive", "base": "pass", "step": "fail", "cone_bits": 400,
"modes": 1, "depth_reached": 10, "depth_needed": 10}, "strengthen"),
({"outcome": "inconclusive", "base": "running", "step": "not run", "cone_bits": 20000,
"modes": 1, "depth_reached": 6, "depth_needed": 34}, "reduce"),
({"outcome": "inconclusive", "base": "pass", "step": "timeout", "cone_bits": 400,
"modes": 3, "depth_reached": 12, "depth_needed": 12}, "split"),
({"outcome": "inconclusive", "base": "pass", "step": "timeout", "cone_bits": 400,
"modes": 1, "depth_reached": 12, "depth_needed": 34}, "induct-or-reduce"),
({"outcome": "inconclusive", "base": "pass", "step": "timeout", "cone_bits": 400,
"modes": 1, "depth_reached": 34, "depth_needed": 34}, "last-resort-assume"),
]
for report, expected in reports:
assert triage(report) == expected, (report, triage(report))
# injected data: a malformed report must be rejected, not guessed at
caught = False
try:
triage({"cone_bits": 10})
except KeyError:
caught = True
assert caught, "triage guessed at a malformed report"
# injected data: a non-reset counterexample must not be classified as a design bug
assert triage({"outcome": "counterexample", "starts_at_reset": False}) != "classify-trace"
def clauses(gates, flops, depth):
return (3 * gates + flops) * depth # illustrative: 3 clauses per gate, one link per state bit per step
assert clauses(50000, 2000, 30) == 4560000
assert clauses(50000, 2000, 300) == 45600000
print("PASS: eight reports classified, malformed rejected, 4.56M to 45.6M clauses (illustrative)")Measurement | Reading | Tactic |
|---|---|---|
Counterexample from an illegal start | Modelling error (free initial state) | Fix reset and initial state |
Base passes, step fails (CTI) | Non-inductive property | Strengthen with helpers |
Cone tens of thousands of bits | True complexity | Reduce: abstract, cut, shrink |
One property, several behaviours | Case-shaped problem | Split and prove coverage |
Depth reached below depth needed | Bound too short for the state space | Induct or reduce; splitting does not buy depth |
Nothing closes the gap | Model too big to decide | One justified assumption, last |
Every inconclusive run files its measurements: cone bits, depth reached, failed obligation.
The chosen tactic matches the measurement, and a changed tactic is re-measured, not assumed better.
Assumptions carry owners and justifications; timeouts carry new measurements or they are not extended.
Rerun the classifier after each tactic: a reduction should shrink the cone bits, a split should move the failure to one case, a helper should move the step failure. If no measurement moves, the tactic is not biting: stop and re-diagnose rather than stacking more of the same.
Strengthen: write helpers from the CTI. The rerun should move the failure: the step passes or names a new, smaller gap. If the step failure does not move, re-diagnose.