The package is an argument, and this lesson is the argument in full: every proof row cites the run that produced it, every planted fault and mutant is killed by a counterexample row, every assumption is registered with the rows that discharge it, and a script checks all of it. The final block prints one line, and prints it only because the check beneath it rejects 23 ways a package can lie.
The proofs make exactly two assumptions. Every input of every design is free, so there are no input rules to discharge.
Assumption | What it says | Discharged by |
|---|---|---|
| Every run starts in a reset cycle: | The reset determinism rows of the register block and the bridge control; for the other four designs it stays an environment statement. |
| The free constant naming the tracked slot or word keeps its value. | The cover rows of the FIFO and the bridge: the tracked trigger can happen with the constant in place. |
Every row lists the first; rows that read a tracked constant list the second. The engine marks the first entry discharged because two rows are proven; it cannot see that four designs (the FIFO, the arbiter, the pipeline and the counter) have no pair proof, so for those the entry stays a statement about the environment, backed by the integration reset check.
# | Injected defect | Complaint the engine must raise |
|---|---|---|
1 | empty ledger |
|
2 | rev field deleted |
|
3 | stale revision |
|
4 | proven row without cover |
|
5 | proven row without kills |
|
6 | bound differs from the run |
|
7 | proven row cites a counterexample run |
|
8 | bounded row below the design minimum |
|
9 | bounded row without a reason |
|
10 | status outside the vocabulary |
|
11 | discharge row not proven |
|
12 | counterexample row deleted |
|
13 | duplicate row |
|
14 | run not in the run table |
|
15 | kill nobody exhibited |
|
16 | tracked constant not declared |
|
17 | cover row without a cover |
|
18 | counterexample row without a kill |
|
19 | unknown design on a bounded row |
|
20 | row omits the reset assumption |
|
21 | assumption not in the register |
|
22 | final package defers a discharge |
|
23 | row cites a run of another design |
|
Each row of the table is one injector on a copy of the reference world, and the block asserts that the engine's list of injections equals this table.
The block holds the whole reference ledger: 37 proof, cover and inconclusive rows and 40 counterexample rows, one per mutant. The run table is generated from the headers of this course's blocks; the bounds of the rows are typed by hand and the engine compares them. It checks the clean ledger, computes the mutation score over the 16 planted faults and over all 40 mutants, injects the defects, and prints one line.
# ---- 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 = {
"fifo-prove": ("prove", 4, "proved", "sync_fifo"),
"fifo-nohelp-bmc": ("bmc", 20, "bounded", "sync_fifo"),
"fifo-nohelp-prove": ("prove", 12, "unproven", "sync_fifo"),
"fifo-cover": ("cover", 8, "reached", "sync_fifo"),
"bridge-prove": ("prove", 4, "proved", "hs_bridge"),
"bridge-nohelp": ("prove", 12, "unproven", "hs_bridge"),
"bridge-cover": ("cover", 5, "reached", "hs_bridge"),
"csr-prove": ("prove", 4, "proved", "csr_block"),
"csr-cover": ("cover", 4, "reached", "csr_block"),
"csr-pair": ("prove", 4, "proved", "csr_block"),
"hs-pair-ctrl": ("prove", 4, "proved", "hs_bridge"),
"hs-pair-written": ("prove", 4, "proved", "hs_bridge"),
"arb-prove": ("prove", 4, "proved", "rr_arbiter"),
"arb-nohelp-k3": ("prove", 3, "unproven", "rr_arbiter"),
"arb-cover": ("cover", 6, "reached", "rr_arbiter"),
"pipe-prove": ("prove", 4, "proved", "pipe3"),
"pipe-k2": ("prove", 2, "unproven", "pipe3"),
"pipe-cover": ("cover", 5, "reached", "pipe3"),
"twin-prove": ("prove", 5, "proved", "pipe3_eq"),
"twin-nohelp-k2": ("prove", 2, "unproven", "pipe3_eq"),
"twin-cover": ("cover", 6, "reached", "pipe3_eq"),
"chain-prove": ("prove", 2, "proved", "sync_fifo"),
"chain-cover": ("cover", 6, "reached", "sync_fifo"),
"eco-scope": ("prove", 2, "proved", "rr_arbiter"),
"eco-cover": ("cover", 6, "reached", "rr_arbiter"),
"ctr-prove": ("prove", 4, "proved", "mod10_counter"),
"ctr-plain-prove": ("prove", 10, "unproven", "mod10_counter"),
"ctr-cover": ("cover", 15, "reached", "mod10_counter"),
"fifo-w1": ("bmc", 7, "counterexample", "sync_fifo"),
"fifo-w2": ("bmc", 3, "counterexample", "sync_fifo"),
"fifo-w3": ("bmc", 5, "counterexample", "sync_fifo"),
"fifo-w4": ("bmc", 4, "counterexample", "sync_fifo"),
"fifo-w5": ("bmc", 3, "counterexample", "sync_fifo"),
"bridge-w1": ("bmc", 4, "counterexample", "hs_bridge"),
"bridge-w2": ("bmc", 4, "counterexample", "hs_bridge"),
"bridge-w3": ("bmc", 4, "counterexample", "hs_bridge"),
"csr-w1": ("bmc", 4, "counterexample", "csr_block"),
"csr-w2": ("bmc", 3, "counterexample", "csr_block"),
"csr-w3": ("bmc", 3, "counterexample", "csr_block"),
"arb-w1": ("bmc", 3, "counterexample", "rr_arbiter"),
"arb-w2": ("bmc", 3, "counterexample", "rr_arbiter"),
"arb-w3": ("bmc", 2, "counterexample", "rr_arbiter"),
"twin-w1": ("bmc", 5, "counterexample", "pipe3_eq"),
"ctr-w1": ("bmc", 11, "counterexample", "mod10_counter"),
"fifo-m-not-both": ("bmc", 2, "counterexample", "sync_fifo"),
"fifo-m-push-inc": ("bmc", 6, "counterexample", "sync_fifo"),
"fifo-m-pop-dec": ("bmc", 7, "counterexample", "sync_fifo"),
"bridge-m-ready-comb": ("bmc", 5, "counterexample", "hs_bridge"),
"csr-m-status-hi": ("bmc", 2, "counterexample", "csr_block"),
"csr-m-rst-ctrl": ("bmc", 3, "counterexample", "csr_block"),
"csr-m-rst-status": ("bmc", 3, "counterexample", "csr_block"),
"csr-m-ctrl-rw": ("bmc", 4, "counterexample", "csr_block"),
"csr-m-data-rw": ("bmc", 4, "counterexample", "csr_block"),
"csr-m-w1c-zero": ("bmc", 5, "counterexample", "csr_block"),
"csr-m-isolate-ctrl": ("bmc", 4, "counterexample", "csr_block"),
"csr-m-isolate-data": ("bmc", 4, "counterexample", "csr_block"),
"csr-m-race": ("bmc", 4, "counterexample", "csr_block"),
"arb-m-work-cons": ("bmc", 2, "counterexample", "rr_arbiter"),
"pipe-m-reset-zero": ("bmc", 3, "counterexample", "pipe3"),
"pipe-m-plus-one": ("bmc", 5, "counterexample", "pipe3"),
"arb-bound2": ("bmc", 5, "counterexample", "rr_arbiter"),
"csr-pair-noreset": ("bmc", 4, "counterexample", "csr_block"),
"hs-pair-noreset": ("bmc", 2, "counterexample", "hs_bridge"),
"hs-pair-data": ("bmc", 2, "counterexample", "hs_bridge"),
"chain-w1": ("bmc", 2, "counterexample", "sync_fifo"),
"chain-w2": ("bmc", 2, "counterexample", "sync_fifo"),
"eco-miter": ("bmc", 2, "counterexample", "rr_arbiter"),
"eco-leak": ("bmc", 3, "counterexample", "rr_arbiter"),
}
A0 = ["reset-at-step-0"]
A1 = ["reset-at-step-0", "tracked-constant-stable"]
def R(property, design, status, bound, run, why, cover, kills, assumes=A0):
return dict(property=property, design=design, status=status, bound=bound, run=run, why=why, cover=cover,
kills=list(kills), assumes=list(assumes), rev=3)
def X(mutant, design, label, run, bound): # a counterexample row: one mutant, killed by one property
return dict(property="%s@%s" % (mutant, label), design=design, status="cex", bound=bound, run=run,
why="first fails at step %d" % (bound - 1), cover="", kills=[mutant], assumes=list(A0), rev=3)
ROWS = [
R("fifo-state-and-flags", "sync_fifo", "proven", 4, "fifo-prove", "state properties", "c_full step 5", ["fifo-W1", "fifo-W2", "fifo-W3", "fifo-W4", "fifo-m-not-both"]),
R("fifo-transitions", "sync_fifo", "proven", 4, "fifo-prove", "transition properties", "c_both step 3", ["fifo-m-push-inc", "fifo-m-pop-dec"]),
R("fifo-data-integrity", "sync_fifo", "proven", 4, "fifo-prove", "tracked slot with its helper", "c_tracked_read step 2", ["fifo-W5"], A1),
R("fifo-data-no-helper", "sync_fifo", "bounded", 20, "fifo-nohelp-bmc", "depth 20 is past the farthest control state at step 8; no induction closes without the helper", "c_tracked_read step 2", ["fifo-W5"], A1),
R("fifo-induction-needs-helper", "sync_fifo", "inconclusive", 12, "fifo-nohelp-prove", "the step fails on the data property", "", []),
R("fifo-covers", "sync_fifo", "cover-reached", 8, "fifo-cover", "all four covers reached: three of the earlier sections and the lab's own c_tracked_read", "c_tracked_read step 2, c_both step 3, c_empty_after_use step 4, c_full step 5", []),
R("bridge-conservation", "hs_bridge", "proven", 4, "bridge-prove", "counters and skid rule", "c_skid_used step 3", ["bridge-W1", "bridge-W2"]),
R("bridge-hold-rules", "hs_bridge", "proven", 4, "bridge-prove", "valid hold, data hold, ready", "c_stall step 2", ["bridge-W2", "bridge-W3", "bridge-m-ready-comb"]),
R("bridge-data-integrity", "hs_bridge", "proven", 4, "bridge-prove", "tracked word with its helpers", "c_tracked_out step 2", ["bridge-W3"], A1),
R("bridge-induction-needs-helper", "hs_bridge", "inconclusive", 12, "bridge-nohelp", "the step fails on the data property", "", []),
R("bridge-covers", "hs_bridge", "cover-reached", 5, "bridge-cover", "all five covers reached: four of the earlier sections and the lab's own c_tracked_out", "c_stall step 2, c_flow step 2, c_tracked_out step 2, c_skid_used step 3, c_backpress_full step 3", []),
R("csr-reset-values", "csr_block", "proven", 4, "csr-prove", "reset properties", "step 0 is a reset by the harness", ["csr-W3", "csr-m-rst-ctrl", "csr-m-rst-status"]),
R("csr-readwrite-and-isolation", "csr_block", "proven", 4, "csr-prove", "read-back and isolation", "c_id_write step 1", ["csr-m-ctrl-rw", "csr-m-data-rw", "csr-m-isolate-ctrl", "csr-m-isolate-data"]),
R("csr-id-and-status-read", "csr_block", "proven", 4, "csr-prove", "constant and status read", "c_id_write step 1", ["csr-W2", "csr-m-status-hi"]),
R("csr-w1c-and-race", "csr_block", "proven", 4, "csr-prove", "write-1-to-clear and priority", "c_w1c_clear step 2, c_set_collision step 2", ["csr-W1", "csr-m-w1c-zero", "csr-m-race"]),
R("csr-covers", "csr_block", "cover-reached", 4, "csr-cover", "all four covers reached: three of the earlier sections and the lab's own c_set_collision", "c_id_write step 1, c_w1c_clear step 2, c_both_bits step 2, c_set_collision step 2", []),
R("csr-reset-determinism", "csr_block", "proven", 4, "csr-pair", "two copies with the helper assertion", "c_pair_write step 1", ["csr-pair-noreset"]),
R("bridge-control-determinism", "hs_bridge", "proven", 4, "hs-pair-ctrl", "two copies, control outputs", "c_pair_flow step 1", ["hs-pair-noreset"]),
R("bridge-data-after-write", "hs_bridge", "proven", 4, "hs-pair-written", "two copies with four helper assertions", "c_pair_written step 2", ["hs-pair-data-claim"]),
R("arbiter-structural", "rr_arbiter", "proven", 4, "arb-prove", "one-hot, no phantom grant, work conservation", "c_g0 to c_g3 step 1, c_idle step 1", ["arb-W2", "arb-W3", "arb-m-work-cons"]),
R("arbiter-wait-bound", "rr_arbiter", "proven", 4, "arb-prove", "wait counters with their helpers", "c_contend step 4", ["arb-W1", "arb-m-bound-2"]),
R("arbiter-needs-window-4", "rr_arbiter", "inconclusive", 3, "arb-nohelp-k3", "without helpers the step fails at window 3", "", []),
R("arbiter-covers", "rr_arbiter", "cover-reached", 6, "arb-cover", "all six covers reached", "c_g0 to c_g3 step 1, c_idle step 1, c_contend step 4", []),
R("pipe3-latency", "pipe3", "proven", 4, "pipe-prove", "latency three with input history", "c_y_nonzero step 4", ["pipe-m-plus-one"]),
R("pipe3-reset-zero", "pipe3", "proven", 4, "pipe-prove", "output zero after reset", "step 0 is a reset by the harness", ["pipe-m-reset-zero"]),
R("pipe3-window", "pipe3", "inconclusive", 2, "pipe-k2", "a window of 2 cannot see inputs three cycles back", "", []),
R("pipe3-cover", "pipe3", "cover-reached", 5, "pipe-cover", "first non-zero result", "c_y_nonzero step 4", []),
R("twin-equivalence", "pipe3_eq", "proven", 5, "twin-prove", "miter with the cut helper", "c_nonzero step 4", ["twin-W1"]),
R("twin-needs-cut-helper", "pipe3_eq", "inconclusive", 2, "twin-nohelp-k2", "without the helper a window of 2 fails", "", []),
R("twin-cover", "pipe3_eq", "cover-reached", 6, "twin-cover", "first equal non-zero result", "c_nonzero step 4", []),
R("chain-connectivity", "sync_fifo", "proven", 2, "chain-prove", "four table rows, combinational", "c_chain_fifo_word step 2", ["chain-swap-data", "chain-swap-valid"]),
R("chain-covers", "sync_fifo", "cover-reached", 6, "chain-cover", "chain covers reached", "c_chain_fifo_word step 2", []),
R("eco-outside-the-change", "rr_arbiter", "proven", 2, "eco-scope", "scoped claim on both revisions", "c_agree step 2", ["eco-scope-leak"]),
R("eco-scope-cover", "rr_arbiter", "cover-reached", 6, "eco-cover", "pointers agree with a request present", "c_agree step 2", []),
R("counter-full-set", "mod10_counter", "proven", 4, "ctr-prove", "range helper closes the step", "c_tc step 10, c_wrap step 14", ["ctr-W1"]),
R("counter-needs-helper", "mod10_counter", "inconclusive", 10, "ctr-plain-prove", "the step fails on the never-15 property", "", []),
R("counter-covers", "mod10_counter", "cover-reached", 15, "ctr-cover", "wrap is the deepest cover", "c_nine step 10, c_tc step 10, c_wrap step 14", []),
]
CEX = [
X("fifo-W1", "sync_fifo", "a_range", "fifo-w1", 7),
X("fifo-W2", "sync_fifo", "a_range", "fifo-w2", 3),
X("fifo-W3", "sync_fifo", "a_flags", "fifo-w3", 5),
X("fifo-W4", "sync_fifo", "a_ptr", "fifo-w4", 4),
X("fifo-W5", "sync_fifo", "a_data", "fifo-w5", 3),
X("bridge-W1", "hs_bridge", "a_conserve", "bridge-w1", 4),
X("bridge-W2", "hs_bridge", "a_conserve", "bridge-w2", 4),
X("bridge-W3", "hs_bridge", "a_data", "bridge-w3", 4),
X("csr-W1", "csr_block", "a_w1c_err", "csr-w1", 4),
X("csr-W2", "csr_block", "a_id_const", "csr-w2", 3),
X("csr-W3", "csr_block", "a_rst_data", "csr-w3", 3),
X("arb-W1", "rr_arbiter", "h_wt3", "arb-w1", 3),
X("arb-W2", "rr_arbiter", "a_onehot0", "arb-w2", 3),
X("arb-W3", "rr_arbiter", "a_no_phantom", "arb-w3", 2),
X("twin-W1", "pipe3_eq", "a_equiv", "twin-w1", 5),
X("ctr-W1", "mod10_counter", "a_tc", "ctr-w1", 11),
X("fifo-m-not-both", "sync_fifo", "a_not_both", "fifo-m-not-both", 2),
X("fifo-m-push-inc", "sync_fifo", "a_push_inc", "fifo-m-push-inc", 6),
X("fifo-m-pop-dec", "sync_fifo", "a_pop_dec", "fifo-m-pop-dec", 7),
X("bridge-m-ready-comb", "hs_bridge", "a_no_ready_comb", "bridge-m-ready-comb", 5),
X("csr-m-status-hi", "csr_block", "a_status_hi", "csr-m-status-hi", 2),
X("csr-m-rst-ctrl", "csr_block", "a_rst_ctrl", "csr-m-rst-ctrl", 3),
X("csr-m-rst-status", "csr_block", "a_rst_status", "csr-m-rst-status", 3),
X("csr-m-ctrl-rw", "csr_block", "a_ctrl_rw", "csr-m-ctrl-rw", 4),
X("csr-m-data-rw", "csr_block", "a_data_rw", "csr-m-data-rw", 4),
X("csr-m-w1c-zero", "csr_block", "a_w1c_zero", "csr-m-w1c-zero", 5),
X("csr-m-isolate-ctrl", "csr_block", "a_isolate_ctrl", "csr-m-isolate-ctrl", 4),
X("csr-m-isolate-data", "csr_block", "a_isolate_data", "csr-m-isolate-data", 4),
X("csr-m-race", "csr_block", "a_hw_set", "csr-m-race", 4),
X("arb-m-work-cons", "rr_arbiter", "a_work_cons", "arb-m-work-cons", 2),
X("pipe-m-reset-zero", "pipe3", "a_reset_zero", "pipe-m-reset-zero", 3),
X("pipe-m-plus-one", "pipe3", "a_latency3", "pipe-m-plus-one", 5),
X("arb-m-bound-2", "rr_arbiter", "a_wt3", "arb-bound2", 5),
X("csr-pair-noreset", "csr_block", "h_state", "csr-pair-noreset", 4),
X("hs-pair-noreset", "hs_bridge", "a_det_ctrl", "hs-pair-noreset", 2),
X("hs-pair-data-claim", "hs_bridge", "a_det_data", "hs-pair-data", 2),
X("chain-swap-data", "sync_fifo", "a_row_d1", "chain-w1", 2),
X("chain-swap-valid", "sync_fifo", "a_row_v1", "chain-w2", 2),
dict(X("eco-delta", "rr_arbiter", "a_equiv", "eco-miter", 2), property="eco-intended-difference"),
X("eco-scope-leak", "rr_arbiter", "a_cond", "eco-leak", 3),
]
PLANTED = ["fifo-W1", "fifo-W2", "fifo-W3", "fifo-W4", "fifo-W5", "bridge-W1", "bridge-W2", "bridge-W3", "csr-W1", "csr-W2", "csr-W3", "arb-W1", "arb-W2", "arb-W3", "twin-W1", "ctr-W1"]
EXTRA = ["fifo-m-not-both", "fifo-m-push-inc", "fifo-m-pop-dec", "bridge-m-ready-comb", "csr-m-status-hi", "csr-m-rst-ctrl", "csr-m-rst-status", "csr-m-ctrl-rw", "csr-m-data-rw", "csr-m-w1c-zero", "csr-m-isolate-ctrl", "csr-m-isolate-data", "csr-m-race", "arb-m-work-cons", "pipe-m-reset-zero", "pipe-m-plus-one", "arb-m-bound-2", "csr-pair-noreset", "hs-pair-noreset", "hs-pair-data-claim", "chain-swap-data", "chain-swap-valid", "eco-delta", "eco-scope-leak"]
REQUIRED = ["fifo-state-and-flags", "fifo-transitions", "fifo-data-integrity", "fifo-data-no-helper", "fifo-induction-needs-helper", "fifo-covers", "bridge-conservation", "bridge-hold-rules", "bridge-data-integrity", "bridge-induction-needs-helper", "bridge-covers", "csr-reset-values", "csr-readwrite-and-isolation", "csr-id-and-status-read", "csr-w1c-and-race", "csr-covers", "csr-reset-determinism", "bridge-control-determinism", "bridge-data-after-write", "arbiter-structural", "arbiter-wait-bound", "arbiter-needs-window-4", "arbiter-covers", "pipe3-latency", "pipe3-reset-zero", "pipe3-window", "pipe3-cover", "twin-equivalence", "twin-needs-cut-helper", "twin-cover", "chain-connectivity", "chain-covers", "eco-outside-the-change", "eco-scope-cover", "counter-full-set", "counter-needs-helper", "counter-covers", "eco-intended-difference"]
WORLD = dict(ledger=ROWS + CEX, runs=RUNS, required=REQUIRED, mutants=PLANTED + EXTRA,
register={"reset-at-step-0": ["csr-reset-determinism", "bridge-control-determinism"],
"tracked-constant-stable": ["fifo-covers", "bridge-covers"]},
tracked=["fifo-data-integrity", "fifo-data-no-helper", "bridge-data-integrity"])
WORLD["tracked"] = set(WORLD["tracked"])
assert world_ok(WORLD) == [], world_ok(WORLD)
assert len(PLANTED) == 16 and len(set(PLANTED + EXTRA)) == len(PLANTED + EXTRA)
assert mutation_score(WORLD["ledger"], PLANTED) == 1.0
assert mutation_score(WORLD["ledger"], PLANTED + EXTRA) == 1.0
TABLE = [["empty ledger","missing-row:"],["rev field deleted","missing-field:"],["stale revision","stale:"],["proven row without cover","no-evidence:"],["proven row without kills","no-evidence:"],["bound differs from the run","bound-not-run-depth:"],["proven row cites a counterexample run","status-not-from-run:"],["bounded row below the design minimum","short-bound:"],["bounded row without a reason","unjustified:"],["status outside the vocabulary","bad-status:"],["discharge row not proven","open-assume:"],["counterexample row deleted","survivor:"],["duplicate row","duplicate:"],["run not in the run table","no-such-run:"],["kill nobody exhibited","unsupported-kill:"],["tracked constant not declared","hidden-assume:"],["cover row without a cover","no-evidence:"],["counterexample row without a kill","no-evidence:"],["unknown design on a bounded row","unknown-design:"],["row omits the reset assumption","hidden-assume:"],["assumption not in the register","unregistered-assume:"],["final package defers a discharge","deferred-assume:"],["row cites a run of another design","run-of-another-design:"]]
assert [(n, e) for n, e, v in injections(WORLD)] == [tuple(t) for t in TABLE], "the table of the lesson is the list of injectors"
assert check_injections(WORLD) == 23
print("PASS: formal lab ledger consistent")Expected output is the single line PASS: formal lab ledger consistent. If an injection raises no complaint, the engine is broken; if the clean ledger raises one, a row disagrees with its run.
Question | Answer, with the rows it cites |
|---|---|
Which results stay bounded? | One row: |
Which abstractions were taken? | A tracked slot in the FIFO, a tracked word in the bridge (data independence), the pipeline's input history, and the arbiter's wait counters. |
Which assumptions need confirmation? | None about any input: every input is free. The register holds two entries, each with its rows. Reset at step 0 is proven discharged for two designs only (the register block and the bridge control, by their pair proofs); for the FIFO, the arbiter, the pipeline and the counter it stays a statement about the environment, backed by the integration reset check. |
What reruns on the next change? | Everything: every row carries the revision, and a bump makes the whole ledger stale. |
Not claimed: unbounded liveness (the arbiter has a bounded-response property), behaviour with unknown values (formal here is two-state), and anything outside the six designs.
Run the manifest from the page text, never from a hand copy. If a row disagrees with its run, fix the row: the run table is generated from the headers. Add a design's minimum depth to the engine and its rows to the ledger together.
That every row is well formed, backed by a run that supports it, evidenced and fresh, and that every assumption and mutant is accounted for. It does not claim the designs are perfect.
A register entry is only as good as the rows behind it: if the pair proof did not close, the reset assumption is open and the package must say so.