A proof belongs to one revision. The day after sign-off, a one-line fix lands, the proof is rerun by nobody, and the package still quotes the old result. From that moment the sign-off describes a design that no longer exists. Staleness is not a rare accident; in an active project it is the default, and only a mechanical check defeats it.
Every ledger row records the source hash it was proved against, and the gate compares those hashes with the current sources before any other check. A mismatch marks the row stale, and a stale row is rerun, not argued about. The rerun is cheap because the suite is incremental: proofs whose cone excludes the changed logic can be identified, but the safe default is rerunning everything, since the full FIFO and arbiter suites complete in seconds.
The script below models the gate: a ledger with per-file hashes against current sources. One file moved on, and the gate names exactly the rows that must rerun. The second half shows the rerun making the ledger current, and a source file that has vanished from the tree being flagged instead of skipped.
# the staleness gate: ledger hashes versus current sources
ledger = [
{"prop": "a_range", "files": {"sync_fifo.sv": "a41f"}, "status": "proven"},
{"prop": "a_wt1", "files": {"rr_arbiter.sv": "9c02"}, "status": "proven"},
{"prop": "a_data", "files": {"hs_bridge.sv": "77bd"}, "status": "inconclusive"},
]
current = {"sync_fifo.sv": "a41f", "rr_arbiter.sv": "9c03", "hs_bridge.sv": "77bd"}
def stale_rows(rows, cur):
stale = []
for r in rows:
for f, h in r["files"].items():
if cur.get(f) != h:
stale.append((r["prop"], f, h, cur.get(f)))
return stale
stale = stale_rows(ledger, current)
assert stale == [("a_wt1", "rr_arbiter.sv", "9c02", "9c03")], stale
# only the arbiter row reruns; the other two keep their status
fresh = [r["prop"] for r in ledger if r["prop"] not in {s[0] for s in stale}]
assert fresh == ["a_range", "a_data"], fresh
# once the rerun is recorded with the new hash the ledger is current again
rerun = [dict(r, files={f: current[f] for f in r["files"]}) for r in ledger]
assert stale_rows(rerun, current) == []
# a source file missing from the tree is flagged too, not silently skipped
assert stale_rows(ledger, {"sync_fifo.sv": "a41f", "hs_bridge.sv": "77bd"}) == [("a_wt1", "rr_arbiter.sv", "9c02", None)]
print("PASS: gate reruns a_wt1 on rr_arbiter.sv 9c02->9c03; others stand; missing file flagged")Every result row carries a source hash, and the gate compares it with the current tree before sign-off.
The rerun policy is written down: what reruns on which change, and who owns the rerun.
No result is quoted for a revision behind the release candidate, however good the numbers.
Keep the hash fine-grained: per file or per module, not per repository, so one fix reruns one proof family instead of the world. Store the ledger beside the sources so the two cannot drift apart. In continuous integration, the gate runs first and fails fast on staleness; human review starts only after the hashes agree, because reviewing numbers for the wrong revision is worse than useless.
Yes under the safe default, because the gate cannot tell comments from logic without parsing. With per-module hashing that ignores comments the rerun can be skipped honestly; without it, rerun and keep the result current.