Every later lesson ends with the same step: a ledger slice and an engine verdict. The ledger is a plain list of rows; the engine is a handful of checks with no hidden state. The engine cannot call the proof tool, so it checks what you claim against what you ran: each row cites a run, typed from the runner's line, and the engine refuses a row whose claim the run cannot support.
Job of this lesson: read the row format, run the engine on a small demonstration ledger, and watch every check raise its complaint when one defect is injected.
A run is a triple: kind (prove, bmc or cover), the depth in the header, and the outcome the runner printed. A row is a claim about one run, and the engine accepts the claim only when the run can support it.
Status | The run must be | Also required |
|---|---|---|
proven | a | cover evidence and the mutants the property kills |
bounded | a | a written reason, depth at least the design minimum (9 for the FIFO), cover, kills |
cex | a counterexample | the mutant it kills |
cover-reached | a | the cover names and steps |
inconclusive | a | nothing more: it is a filable result |
The three course outcomes map onto these: proven, counterexample (cex), and inconclusive, which covers a bounded pass, an induction that did not close, and an unreached cover. The bound of a row equals the depth of its run, so a depth is never claimed that was not run.
The block below embeds the engine (it is repeated in every lesson that uses it, so each block runs on its own), builds a ledger for a made-up one-bit toggle design (illustrative: it is not one of the six designs), and checks that the clean ledger raises nothing. It then injects twenty-three defects one at a time and asserts that each raises its named complaint.
# ---- formal lab results ledger, engine v2: every row cites a typed run (kind, depth, outcome[, design]) ----
STATUS = ("proven", "bounded", "cex", "cover-reached", "inconclusive")
FROM_RUN = {"proven": {("prove", "proved")},
"bounded": {("bmc", "bounded")},
"cex": {("bmc", "counterexample"), ("prove", "counterexample")},
"cover-reached": {("cover", "reached")},
"inconclusive": {("prove", "unproven"), ("cover", "not-reached")}}
NEED = {"sync_fifo": 9, "rr_arbiter": 5, "hs_bridge": 4, "csr_block": 3,
"pipe3": 5, "pipe3_eq": 5, "mod10_counter": 15, "toggle_demo": 4}
KEYS = ("property", "design", "status", "bound", "why", "run", "assumes", "cover", "kills", "rev")
REV = 3
ALWAYS = "reset-at-step-0"
TRACKED = "tracked-constant-stable"
def row_problems(e, runs, tracked):
n = e.get("property", "?")
miss = [k for k in KEYS if k not in e]
if miss:
return ["missing-field:%s:%s" % (n, ",".join(miss))]
if e["status"] not in STATUS:
return ["bad-status:" + n]
p = []
if e["rev"] != REV:
p.append("stale:" + n)
if e["run"] not in runs:
return p + ["no-such-run:" + n]
kind, depth, outcome = runs[e["run"]][:3]
if len(runs[e["run"]]) > 3 and runs[e["run"]][3] != e["design"]:
p.append("run-of-another-design:" + n) # a run typed with its design may be cited only by that design's rows
if (kind, outcome) not in FROM_RUN[e["status"]]:
p.append("status-not-from-run:" + n)
if e["bound"] != depth:
p.append("bound-not-run-depth:" + n)
has_cover = bool(str(e["cover"]).strip())
if e["status"] in ("proven", "bounded") and not (has_cover and e["kills"]):
p.append("no-evidence:" + n)
if e["status"] == "cover-reached" and not has_cover:
p.append("no-evidence:" + n)
if e["status"] == "cex" and not e["kills"]:
p.append("no-evidence:" + n)
if e["status"] == "bounded":
if e["design"] not in NEED:
p.append("unknown-design:" + n)
elif depth < NEED[e["design"]]:
p.append("short-bound:" + n)
if len(str(e["why"]).strip()) < 12:
p.append("unjustified:" + n)
if ALWAYS not in e["assumes"]:
p.append("hidden-assume:%s:%s" % (n, ALWAYS))
if n in tracked and TRACKED not in e["assumes"]:
p.append("hidden-assume:%s:%s" % (n, TRACKED))
return p
def ledger_ok(ledger, runs, required, mutants, register, tracked, final=True):
names = [e.get("property") for e in ledger]
bad = ["duplicate:" + n for n in sorted({n for n in names if names.count(n) > 1})]
bad += ["missing-row:" + r for r in sorted(set(required) - set(names))]
bad += [q for e in ledger for q in row_problems(e, runs, tracked)]
good = [e for e in ledger if not row_problems(e, runs, tracked)] # only a row without complaints counts as evidence
solid = {e["property"] for e in good if e["status"] in ("proven", "cover-reached")}
for a, rows in sorted(register.items()):
if rows is None:
if final:
bad.append("deferred-assume:" + a) # a stage may defer a discharge; a final package may not
elif not (rows and all(r in solid for r in rows)):
bad.append("open-assume:" + a)
bad += ["unregistered-assume:%s:%s" % (e.get("property"), a) for e in ledger
for a in e.get("assumes", []) if a not in register]
killed = {m for e in good if e["status"] == "cex" for m in e["kills"]}
bad += ["survivor:" + m for m in sorted(set(mutants) - killed)]
bad += ["unsupported-kill:%s:%s" % (e.get("property"), m) for e in ledger
if e.get("status") in ("proven", "bounded") for m in e.get("kills", []) if m not in killed]
return bad
def mutation_score(ledger, mutants):
assert mutants, "no mutants registered"
killed = {m for e in ledger if e.get("status") == "cex" for m in e.get("kills", [])}
return len(killed & set(mutants)) / len(mutants)
import copy
def world_ok(w):
return ledger_ok(w["ledger"], w["runs"], w["required"], w["mutants"], w["register"], w["tracked"])
def pick(w, status):
return next(e for e in w["ledger"] if e["status"] == status)
def injections(w):
out = []
def add(name, expect, fn):
v = copy.deepcopy(w)
fn(v)
out.append((name, expect, v))
def short_bound(v):
e = pick(v, "bounded")
e["bound"] = NEED[e["design"]] - 1
v["runs"][e["run"]] = ("bmc", e["bound"], "bounded")
add("empty ledger", "missing-row:", lambda v: v["ledger"].clear())
add("rev field deleted", "missing-field:", lambda v: pick(v, "proven").pop("rev"))
add("stale revision", "stale:", lambda v: pick(v, "proven").update(rev=REV - 1))
add("proven row without cover", "no-evidence:", lambda v: pick(v, "proven").update(cover=""))
add("proven row without kills", "no-evidence:", lambda v: pick(v, "proven").update(kills=[]))
add("bound differs from the run", "bound-not-run-depth:", lambda v: pick(v, "cex").update(bound=pick(v, "cex")["bound"] + 1))
add("proven row cites a counterexample run", "status-not-from-run:",
lambda v: pick(v, "proven").update(run=pick(v, "cex")["run"]))
add("bounded row below the design minimum", "short-bound:", short_bound)
add("bounded row without a reason", "unjustified:", lambda v: pick(v, "bounded").update(why="ok"))
add("status outside the vocabulary", "bad-status:", lambda v: pick(v, "proven").update(status="done"))
add("discharge row not proven", "open-assume:",
lambda v: next(e for e in v["ledger"] if e["property"] == v["register"][ALWAYS][0]).update(status="inconclusive"))
add("counterexample row deleted", "survivor:", lambda v: v["ledger"].remove(pick(v, "cex")))
add("duplicate row", "duplicate:", lambda v: v["ledger"].append(copy.deepcopy(pick(v, "proven"))))
add("run not in the run table", "no-such-run:", lambda v: pick(v, "proven").update(run="run-never-made"))
add("kill nobody exhibited", "unsupported-kill:", lambda v: pick(v, "proven")["kills"].append("mutant-nobody-ran"))
def other_design(v):
e = pick(v, "proven")
other = [r for r, t in v["runs"].items() if len(t) > 3 and t[3] != e["design"] and t[0] == "prove" and t[2] == "proved"]
if not other:
v["runs"]["run-elsewhere"] = ("prove", e["bound"], "proved", e["design"] + "_elsewhere")
other = ["run-elsewhere"]
e["run"] = other[0]
add("tracked constant not declared", "hidden-assume:",
lambda v: v["ledger"][[e["property"] for e in v["ledger"]].index(sorted(v["tracked"])[0])]["assumes"].remove(TRACKED))
add("cover row without a cover", "no-evidence:", lambda v: next(e for e in v["ledger"] if e["status"] == "cover-reached").update(cover=""))
add("counterexample row without a kill", "no-evidence:", lambda v: pick(v, "cex").update(kills=[]))
add("unknown design on a bounded row", "unknown-design:", lambda v: pick(v, "bounded").update(design="no_such_design"))
add("row omits the reset assumption", "hidden-assume:", lambda v: pick(v, "proven").update(assumes=[]))
add("assumption not in the register", "unregistered-assume:", lambda v: pick(v, "proven")["assumes"].append("inputs-are-legal"))
add("final package defers a discharge", "deferred-assume:", lambda v: v["register"].update({ALWAYS: None}))
add("row cites a run of another design", "run-of-another-design:", other_design)
return out
def check_injections(w):
assert world_ok(w) == [], world_ok(w)
done = injections(w)
for name, expect, v in done:
got = world_ok(v)
assert any(c.startswith(expect) for c in got), (name, expect, got)
return len(done)
# runs typed from the runner's lines (illustrative design: a one-bit toggle)
RUNS = {"tog-prove": ("prove", 4, "proved"), "tog-bmc": ("bmc", 6, "bounded"),
"tog-w1": ("bmc", 3, "counterexample"), "tog-cover": ("cover", 3, "reached"),
"tog-nohelp": ("prove", 8, "unproven")}
def row(**k):
base = dict(assumes=["reset-at-step-0"], cover="", kills=[], rev=3, why="")
base.update(k)
return base
LEDGER_ROWS = [
row(property="tog-flips", design="toggle_demo", status="proven", bound=4, why="induction closes", run="tog-prove",
cover="c_flip step 2", kills=["tog-W1"]),
row(property="tog-deep", design="toggle_demo", status="bounded", bound=6, why="depth 6 is past the cover at step 2",
run="tog-bmc", cover="c_flip step 2", kills=["tog-W1"], assumes=["reset-at-step-0", "tracked-constant-stable"]),
row(property="tog-W1@a_flip", design="toggle_demo", status="cex", bound=3, why="fails at step 2", run="tog-w1", kills=["tog-W1"]),
row(property="tog-covers", design="toggle_demo", status="cover-reached", bound=3, why="witness", run="tog-cover", cover="c_flip step 2"),
row(property="tog-nohelp", design="toggle_demo", status="inconclusive", bound=8, why="the step fails", run="tog-nohelp")]
WORLD = dict(ledger=LEDGER_ROWS, runs=RUNS, required=["tog-flips", "tog-covers"], mutants=["tog-W1"],
register={"reset-at-step-0": ["tog-covers"], "tracked-constant-stable": ["tog-flips"]},
tracked={"tog-deep"})
assert world_ok(WORLD) == [], world_ok(WORLD)
n = check_injections(WORLD)
assert n == 23
print("PASS: clean ledger raises nothing; %d injected defects each raise their complaint" % n)Expected output is the single PASS line. The inconclusive row is accepted: a run that did not close is a result, not an error. If an assert fails, the engine has a hole, not your ledger: fix the engine first.
Complaint | Meaning | Fix |
|---|---|---|
missing-field, bad-status | A row lacks a field or uses a status outside the five words. | Complete the row; use the vocabulary. |
no-such-run, status-not-from-run, bound-not-run-depth, run-of-another-design | The run is not in the run table, cannot support the status, has another depth, or (when the run table names its design) belongs to another design. | Cite the run you made for this design, at its own depth. |
stale | The row ran on an older revision. | Rerun on the current revision. |
no-evidence | A proof or bounded row without cover evidence or kills, a cover row without a cover, or a counterexample without a kill. | Add the cover step and the mutant it kills. |
short-bound, unjustified, unknown-design | A bounded depth below the design minimum, without a reason, or for a design the engine has no minimum for. | Run deeper or narrow the claim; write the reason. |
hidden-assume, unregistered-assume, open-assume, deferred-assume | An assumption the proof uses but the row omits, one not in the register, one whose discharging rows are absent or not proven, or one a final package still defers. | List it, register it, and prove or cover its discharge; only a stage may defer. |
duplicate, missing-row | A row name used twice, or a required row absent. | One row per obligation. |
survivor, unsupported-kill | A registered mutant no counterexample row kills, or a row claiming a kill nobody exhibited. | Run the mutant; add the counterexample row. |
# ---- formal lab results ledger, engine v2: every row cites a typed run (kind, depth, outcome[, design]) ----
STATUS = ("proven", "bounded", "cex", "cover-reached", "inconclusive")
FROM_RUN = {"proven": {("prove", "proved")},
"bounded": {("bmc", "bounded")},
"cex": {("bmc", "counterexample"), ("prove", "counterexample")},
"cover-reached": {("cover", "reached")},
"inconclusive": {("prove", "unproven"), ("cover", "not-reached")}}
NEED = {"sync_fifo": 9, "rr_arbiter": 5, "hs_bridge": 4, "csr_block": 3,
"pipe3": 5, "pipe3_eq": 5, "mod10_counter": 15, "toggle_demo": 4}
KEYS = ("property", "design", "status", "bound", "why", "run", "assumes", "cover", "kills", "rev")
REV = 3
ALWAYS = "reset-at-step-0"
TRACKED = "tracked-constant-stable"
def row_problems(e, runs, tracked):
n = e.get("property", "?")
miss = [k for k in KEYS if k not in e]
if miss:
return ["missing-field:%s:%s" % (n, ",".join(miss))]
if e["status"] not in STATUS:
return ["bad-status:" + n]
p = []
if e["rev"] != REV:
p.append("stale:" + n)
if e["run"] not in runs:
return p + ["no-such-run:" + n]
kind, depth, outcome = runs[e["run"]][:3]
if len(runs[e["run"]]) > 3 and runs[e["run"]][3] != e["design"]:
p.append("run-of-another-design:" + n) # a run typed with its design may be cited only by that design's rows
if (kind, outcome) not in FROM_RUN[e["status"]]:
p.append("status-not-from-run:" + n)
if e["bound"] != depth:
p.append("bound-not-run-depth:" + n)
has_cover = bool(str(e["cover"]).strip())
if e["status"] in ("proven", "bounded") and not (has_cover and e["kills"]):
p.append("no-evidence:" + n)
if e["status"] == "cover-reached" and not has_cover:
p.append("no-evidence:" + n)
if e["status"] == "cex" and not e["kills"]:
p.append("no-evidence:" + n)
if e["status"] == "bounded":
if e["design"] not in NEED:
p.append("unknown-design:" + n)
elif depth < NEED[e["design"]]:
p.append("short-bound:" + n)
if len(str(e["why"]).strip()) < 12:
p.append("unjustified:" + n)
if ALWAYS not in e["assumes"]:
p.append("hidden-assume:%s:%s" % (n, ALWAYS))
if n in tracked and TRACKED not in e["assumes"]:
p.append("hidden-assume:%s:%s" % (n, TRACKED))
return p
def ledger_ok(ledger, runs, required, mutants, register, tracked, final=True):
names = [e.get("property") for e in ledger]
bad = ["duplicate:" + n for n in sorted({n for n in names if names.count(n) > 1})]
bad += ["missing-row:" + r for r in sorted(set(required) - set(names))]
bad += [q for e in ledger for q in row_problems(e, runs, tracked)]
good = [e for e in ledger if not row_problems(e, runs, tracked)] # only a row without complaints counts as evidence
solid = {e["property"] for e in good if e["status"] in ("proven", "cover-reached")}
for a, rows in sorted(register.items()):
if rows is None:
if final:
bad.append("deferred-assume:" + a) # a stage may defer a discharge; a final package may not
elif not (rows and all(r in solid for r in rows)):
bad.append("open-assume:" + a)
bad += ["unregistered-assume:%s:%s" % (e.get("property"), a) for e in ledger
for a in e.get("assumes", []) if a not in register]
killed = {m for e in good if e["status"] == "cex" for m in e["kills"]}
bad += ["survivor:" + m for m in sorted(set(mutants) - killed)]
bad += ["unsupported-kill:%s:%s" % (e.get("property"), m) for e in ledger
if e.get("status") in ("proven", "bounded") for m in e.get("kills", []) if m not in killed]
return bad
def mutation_score(ledger, mutants):
assert mutants, "no mutants registered"
killed = {m for e in ledger if e.get("status") == "cex" for m in e.get("kills", [])}
return len(killed & set(mutants)) / len(mutants)
rows = [dict(status="cex", kills=["tog-W1"]), dict(status="cex", kills=["tog-W2"]), dict(status="proven", kills=["tog-W3"])]
assert mutation_score(rows, ["tog-W1", "tog-W2"]) == 1.0
assert mutation_score(rows, ["tog-W1", "tog-W2", "tog-W3"]) == 2 / 3, "a proven row's claim is not a kill"
assert mutation_score(rows[:1], ["tog-W1", "tog-W2"]) == 0.5
try:
mutation_score(rows, [])
silent = True
except AssertionError:
silent = False
assert not silent, "an empty mutant set must fail, not score 1.0"
print("PASS: the mutation score counts only counterexample rows")Only a counterexample row kills a mutant, and an empty mutant set fails loudly.
Read the property name after the colon first: it names the row to open. Reproduce the run at the stated depth before editing the ledger; most bound complaints are unfinished runs.
unjustified: depth 40 exceeds every minimum, but a bounded claim without a written reason is still a complaint. Depth is not a justification.
A discharging row: the register names rows that must be proven or covered, and one of them is not. A passing proof that leans on an undischarged assumption proves its design only conditionally.