Why it matters

A nightly run hit its time limit on three properties and the dashboard counted them as not-failed, which the team read as proven for a month. The properties covered the reset values of a data register. The bug that shipped was a wrong reset value. The failure was not the timeout; timeouts happen. The failure was the reporting.

Job of this lesson: set budgets that fit the work, and make a timeout impossible to misread.

The core idea

Every property gets a time budget and every run gets a total budget; small bounded checks and covers run per commit in minutes, full proofs run nightly. Parallel tasks split the set so one slow property cannot starve the rest. The result vocabulary has exactly three outcomes, proven, counterexample and inconclusive, and a timeout or an undecided engine lands in the third. The ledger records the outcome plus the depth, so a bounded result is never filed where a proof belongs.

Worked example: the planner and the reporting rule

The planner below assigns budgets from the property list and places them on the parallel tasks inside the nightly window. A total that fits is necessary but not sufficient: three 100-minute properties on two tasks with a 150-minute window total 300 minutes against 300 available, and cannot be placed, so the planner packs them first-fit rather than only adding. Budgets are illustrative planning numbers, not measured runtimes. The second half is the reporting rule: a function that takes a result line, as a flow writes it, and rejects a proven line whose reason is a timeout, a line with no depth, and any status outside the three outcomes. It is applied to a clean line and to three mislabelled ones:

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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57

props = [
    {"name": "a_id_const", "budget_min": 5},
    {"name": "a_w1c_done", "budget_min": 5},
    {"name": "a_conserve", "budget_min": 60},
    {"name": "a_data", "budget_min": 120},
]

def total_fits(props, window_min, tasks):
    return sum(p["budget_min"] for p in props) <= window_min * tasks

def pack(props, window_min, tasks):
    loads = [0] * tasks
    for p in sorted(props, key=lambda p: -p["budget_min"]):
        for i in range(tasks):
            if loads[i] + p["budget_min"] <= window_min:
                loads[i] += p["budget_min"]
                break
        else:
            return False
    return True

assert pack(props, 240, 2)
greedy = [dict(p) for p in props]
greedy[3]["budget_min"] = 500
assert not pack(greedy, 240, 2)
three = [{"name": "p" + str(i), "budget_min": 100} for i in range(3)]
assert total_fits(three, 150, 2) and not pack(three, 150, 2)    # necessary, not sufficient

OUTCOMES = ("proven", "counterexample", "inconclusive")

def check_line(line):
    if line.get("status") not in OUTCOMES:
        raise ValueError("status is not one of the three outcomes")
    if line.get("depth") is None:
        raise ValueError("no depth recorded")
    if line["status"] == "proven" and line.get("reason") in ("timeout", "budget", "killed"):
        raise ValueError("a timeout cannot be filed as proven")
    return line

def rejects(line):
    try:
        check_line(line)
    except ValueError:
        return True
    return False

def file_result(raw, depth):
    status = {"pass": "proven", "fail": "counterexample"}.get(raw, "inconclusive")
    return {"status": status, "depth": depth, "reason": raw}

assert not rejects({"status": "proven", "depth": 8, "reason": "induction closed"})
assert file_result("timeout", 40)["status"] == "inconclusive"
assert not rejects(file_result("timeout", 40))
assert rejects({"status": "proven", "depth": 40, "reason": "timeout"})
assert rejects({"status": "proven", "reason": "induction closed"})
assert rejects({"status": "timeout-pass", "depth": 40})
print("PASS: budgets are packed, not just added; a timeout filed as proven is rejected")

What the review looks for

• Every property has a budget, and the nightly plan packs onto the tasks inside the window, not merely adds up.

• The ledger shows three outcomes only, each with a depth; no timeout is filed as proven.

• A property that times out has a triage note: reduce, split, strengthen, or a justified bound.

Verify and debug

Inject a tiny time limit once per quarter and read the summary: if anything downstream counts it as a pass, the reporting chain is broken. When a property first exceeds its budget, triage it as a slow proof before raising anything; budgets are set from history, and history is allowed to say the proof needs work.

Related topics

• Earlier: Diagnosing a Slow Proof

• Later: CI for Formal