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
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164

# ---- 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 = {"tog-prove": ("prove", 4, "proved"), "tog-bmc": ("bmc", 6, "bounded"),
        "tog-w1": ("bmc", 3, "counterexample"), "tog-cover": ("cover", 3, "reached")}
def row(**k):
    base = dict(assumes=["reset-at-step-0"], cover="", kills=[], rev=3, why="")
    base.update(k)
    return base
DEMO = dict(
    ledger=[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")],
    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"})
def manifest(world, expect_injections=23):
    problems = world_ok(world)
    assert problems == [], problems
    caught = check_injections(world)
    assert caught == expect_injections, caught
    return caught
YOUR_WORLD = None        # assemble your own ledger, runs, required rows, mutants, register and tracked rows
if YOUR_WORLD is not None:
    manifest(YOUR_WORLD)
    print("PASS: formal lab ledger consistent")
else:
    n = manifest(DEMO)
    # the manifest refuses what it must refuse: an empty world, and a world with a stale row
    assert world_ok(dict(DEMO, ledger=[])) != []
    assert world_ok(dict(DEMO, ledger=[dict(r, rev=2) for r in DEMO["ledger"]])) != []
    print("PASS: the manifest accepts the demonstration ledger and refuses %d injected defects" % n)