#!/usr/bin/env python3 """receipt_differential.py: two verifiers of job receipts, held to each other and to the corpus (wai/quantum-conformance/receipts/README.md). python3 -I receipt_differential.py --reference PATH/wai-quantum [--extra DIR ...] python3 -I receipt_differential.py --reference PATH/wai-quantum --plant NAME python3 -I receipt_differential.py --second-only [--plant NAME] The reference is `wai-quantum verify --json` (and `--lines`); the second verifier is receipt_verify.py beside this file, written from wai/extensions/quantum-providers.md section 8 alone. For every receipt of the corpus, both must report exactly the reasons the manifest gives. Then every valid receipt of the corpus is changed one member at a time, each member of its request, its result, its receipt and its unsealed envelope, by removing it and by replacing its value, and both must report the same reasons for every change. Two oracles hold beside agreement: a change inside the request or the result is never valid, and a change to the envelope, or a member added to the receipt, never changes the verdict. `--extra DIR` adds receipts a person holds and does not publish (one with an account number in it): both verifiers must find each valid. `--second-only` holds the second verifier to the manifest alone, with no build of the reference, and changes nothing. `--plant NAME` runs the second verifier with one of its planted defects (`receipt_verify.py --plant`), and succeeds only when the differential catches it: the proof that the check can fail. `--second FILE` holds another second verifier (a mutant of receipt_verify.py) to the same stages; `--wasmq-only` keeps to what holds a wasmQ job (its receipts, their one-member changes, the rules stage and the labelled cases); `--first` stops at the first stage that disagrees; and `RD_CACHE=DIR` keeps each verifier's answers, so that a run over many mutants of one verifier asks the other once (`wasmq_mutants.py`). Exit status 0 only when everything agrees (or, with --plant, when the plant is caught). Standard library only, Python 3.9+. """ import argparse import base64 import copy import hashlib import importlib.util import json import os import re import subprocess import sys import tempfile from collections import Counter HERE = os.path.dirname(os.path.abspath(__file__)) CORPUS = os.path.join(HERE, "..", "receipts") SECOND = os.path.join(HERE, "receipt_verify.py") ORIGINAL_SECOND = SECOND def compact(v): return json.dumps(v, ensure_ascii=False, separators=(",", ":")) def spelt(v, raw): """A line of v's text, each `raw` literal as it is written.""" if isinstance(v, raw): return v.literal if isinstance(v, dict): return "{" + ",".join(json.dumps(k, ensure_ascii=False) + ":" + spelt(x, raw) for k, x in v.items()) + "}" if isinstance(v, list): return "[" + ",".join(spelt(x, raw) for x in v) + "]" return compact(v) def verdicts(lines_text, json_lines): out = [] for line in lines_text.splitlines(): line = line.strip() if line: out.append(json.loads(line)) if len(out) != json_lines: raise SystemExit("a verifier gave %d verdicts for %d receipts" % (len(out), json_lines)) return out def _who(cmd): """What decides a verifier's answers, for the cache: the reference binary (its path, size and time) and the mutant it is asked to be, or the second verifier's text and its plant.""" h = hashlib.sha256() script = any(part.endswith(".py") for part in cmd) for part in cmd: h.update(part.encode() + b"\0") if part.endswith(".py") and os.path.isfile(part): with open(part, "rb") as f: h.update(f.read()) elif os.path.isfile(part) and os.access(part, os.X_OK): st = os.stat(part) h.update(("%d %d" % (st.st_size, st.st_mtime_ns)).encode()) if not script: h.update(os.environ.get("WQ_MUTANT", "").encode()) return h.hexdigest() def cached(cmd, inputs, compute): """compute(), or what it gave before for the same verifier and the same inputs when RD_CACHE names a directory: a run of many mutants of one verifier asks the other the same questions each time.""" d = os.environ.get("RD_CACHE") if not d: return compute() h = hashlib.sha256(_who(cmd).encode()) for b in inputs: h.update(hashlib.sha256(b).digest()) path = os.path.join(d, h.hexdigest() + ".json") try: with open(path, encoding="utf-8") as f: return json.load(f) except (OSError, ValueError): pass out = compute() os.makedirs(d, exist_ok=True) with open(path + ".tmp%d" % os.getpid(), "w", encoding="utf-8") as f: json.dump(out, f) os.replace(path + ".tmp%d" % os.getpid(), path) return out def _contents(files): out = [] for f in files: with open(f, "rb") as h: out.append(h.read()) return out def held_args(held, corpus): """A verifier's arguments for what a receipt is held to beside its seal (section 8.8): the manifest's `held`, its trust list a file of the corpus. Both verifiers take them alike.""" out = [] if held and "trust" in held: out += ["--trust", os.path.join(corpus, held["trust"])] if held and "at_ms" in held: out += ["--at", str(held["at_ms"])] if held and "skew_ms" in held: out += ["--skew-ms", str(held["skew_ms"])] return out def _held_inputs(args): """What decides a held receipt's verdict beside its own text, for the cache: the arguments, and the trust list they name.""" out = [" ".join(args).encode()] for a, b in zip(args, args[1:]): if a == "--trust": out += _contents([b]) return out def run_reference_files(ref, files, held=None, corpus=CORPUS): """The reference's verdict of each file; `held`, when given, is what each is held to.""" held = held or [None] * len(files) def compute(): out = [] for f, h in zip(files, held): p = subprocess.run([ref, "verify", "--json", f] + held_args(h, corpus), capture_output=True, text=True) if p.returncode not in (0, 1) or not p.stdout.strip(): raise SystemExit("the reference failed on %s (status %d): %s" % (f, p.returncode, p.stderr.strip()[:400])) out.append(json.loads(p.stdout.strip().splitlines()[-1])) return out return cached([ref, "verify", "--json"], _contents(files) + [x for h in held for x in _held_inputs(held_args(h, corpus))], compute) def run_second_files(files, plant, held=None, corpus=CORPUS): """The second verifier's verdict of each file: those held to nothing in one run, and those held to something one run for each thing they are held to.""" cmd = [sys.executable, "-I", SECOND] + (["--plant", plant] if plant else []) held = held or [None] * len(files) groups = {} for i, h in enumerate(held): groups.setdefault(tuple(held_args(h, corpus)), []).append(i) def compute(): out = [None] * len(files) for args, members in groups.items(): p = subprocess.run(cmd + list(args) + [files[i] for i in members], capture_output=True, text=True) if p.returncode not in (0, 1): raise SystemExit("the second verifier failed (status %d): %s" % (p.returncode, p.stderr.strip()[:400])) for i, v in zip(members, verdicts(p.stdout, len(members))): out[i] = v return out return cached(cmd, _contents(files) + [x for h in held for x in _held_inputs(held_args(h, corpus))], compute) def held_stage(ref, plant, corpus, entries): """Each receipt the manifest judges held to a trust list or a time beside its seal (section 8.8), given to each verifier with what it is held to: both must give the reasons written for it, and say the same of what they held it to.""" problems = [] here = set("held/" + n for n in os.listdir(os.path.join(corpus, "held")) if n.endswith(".json")) if os.path.isdir(os.path.join(corpus, "held")) else set() named = set(e["file"] for e in entries) for f in sorted(here - named): problems.append("%s is in the corpus and not in the manifest" % f) entries = [e for e in entries if os.path.isfile(os.path.join(corpus, e["file"])) or problems.append("%s is in the manifest and not in the corpus" % e["file"])] files = [os.path.join(corpus, e["file"]) for e in entries] held = [e["held"] for e in entries] r2 = run_second_files(files, plant, held, corpus) r1 = run_reference_files(ref, files, held, corpus) if ref else r2 agree = 0 for e, x, y in zip(entries, r1, r2): want = tuple(sorted(e["reasons"])) if said(x) != said(y) or said(x)[0] != want: problems.append("%s, held to %s: the manifest says %s; the reference %s; the second verifier %s" % (e["file"], json.dumps(e["held"], sort_keys=True), list(want), list(said(x)), list(said(y)))) else: agree += 1 print("held: %d receipts held to a trust list or a time (%d valid, %d not), %d agree %s" % (len(entries), sum(1 for e in entries if not e["reasons"]), sum(1 for e in entries if e["reasons"]), agree, "three ways" if ref else "with the manifest (second verifier only)")) return problems def trust_stage(ref, plant, corpus, lists): """Each trust list of the corpus given to each verifier with one valid receipt: one the manifest says a verifier reads gives a verdict, and one it does not read judges nothing, with the status 2 (section 8.8).""" problems = [] receipt = os.path.join(corpus, "jobs", "crafted-time-issued.json") present = set(n for n in os.listdir(os.path.join(corpus, "trust")) if n.endswith(".json")) if os.path.isdir(os.path.join(corpus, "trust")) else set() named = set(os.path.basename(e["file"]) for e in lists) for n in sorted(present - named): problems.append("trust/%s is in the corpus and not in the manifest" % n) for n in sorted(named - present): problems.append("trust/%s is in the manifest and not in the corpus" % n) read = 0 for e in lists: if os.path.basename(e["file"]) not in present: continue path = os.path.join(corpus, e["file"]) who = [("the second verifier", [sys.executable, "-I", SECOND] + (["--plant", plant] if plant else []) + ["--trust", path, receipt])] if ref: who.append(("the reference", [ref, "verify", "--json", receipt, "--trust", path])) for name, cmd in who: p = subprocess.run(cmd, capture_output=True, text=True) judged = p.returncode in (0, 1) and p.stdout.strip() != "" refused = p.returncode == 2 and p.stdout.strip() == "" if e["reads"] and not judged: problems.append("%s: a trust list a verifier reads, and %s did not judge by it (status %d)" % (e["file"], name, p.returncode)) elif not e["reads"] and not refused: problems.append("%s: a trust list a verifier does not read (%s), and %s gave status %d%s" % (e["file"], e["what"], name, p.returncode, " and a verdict" if p.stdout.strip() else "")) read += 1 print("trust lists: %d, %d a verifier reads and %d it refuses whole by the manifest; %d not so %s" % (read, sum(1 for e in lists if e["reads"]), sum(1 for e in lists if not e["reads"]), len(problems), "to the second verifier" if not ref else "to one verifier or the other")) return problems def run_lines(cmd, path, n): def compute(): p = subprocess.run(cmd + [path], capture_output=True, text=True) if p.returncode not in (0, 1): raise SystemExit("%s failed (status %d): %s" % (cmd[0], p.returncode, p.stderr.strip()[:400])) return verdicts(p.stdout, n) return cached(cmd, _contents([path]), compute) def rules_of(v): """The numbers of the rules of a wasmQ job's form a verdict states as broken (each problem names its rule first), or None when it states none or only the first of many.""" w = v.get("wasmq") if not isinstance(w, dict) or not isinstance(w.get("problems"), list): return None out = set() for p in w["problems"]: if not isinstance(p, str) or p.startswith("and "): return None m = re.match(r"rule (\d+): ", p) if not m: return None out.add(int(m.group(1))) return out def same_rules(what, x, y, problems): """Both verifiers state the same rules broken, where both state them in full.""" rx, ry = rules_of(x), rules_of(y) if rx is not None and ry is not None and rx != ry: problems.append("%s: the reference states rules %s broken; the second verifier %s" % (what, sorted(rx), sorted(ry))) def _same_number(v): """A stated value with each number past 2^53 read as the double both verifiers hold it as, so that one writing it whole and the other as a double agree.""" if isinstance(v, bool) or v is None: return v if isinstance(v, int): return float(v) if abs(v) > 2 ** 53 else v if isinstance(v, dict): return dict((k, _same_number(x)) for k, x in v.items()) if isinstance(v, list): return [_same_number(x) for x in v] return v def said(v): """What a verdict says that both verifiers must agree on: its reasons, its key and form, what it reads of a provider's result, of a job under a contract the choice, the class wanted and the class given, what was kept, the stable choice, and the shadow (whether it ran and its total variation), the time its receipt seals (section 8.2), and what it was held to beside its seal (section 8.8).""" p = v.get("provider") or {} c = v.get("planner") or {} return (tuple(sorted(v.get("reasons", []))), v.get("key"), v.get("form"), p.get("form"), p.get("read_as"), p.get("counts_source"), c.get("choice"), c.get("wanted"), c.get("class"), c.get("stable_choice"), _same_number(c.get("kept")), c.get("shadow_ran"), _same_number(c.get("shadow_total_variation")), json.dumps(v.get("time"), sort_keys=True), json.dumps(v.get("trust"), sort_keys=True), v.get("checked_at_ms"), v.get("skew_ms")) # ----------------------------------------------------------------- one change at a time def mutations(body): """(what, changed body, expected): each member removed, and each value replaced; expected is `invalid` for a change inside the request, the result or the receipt, and `unchanged` for one to the envelope or a member added to the receipt, which is ignored.""" out = [] def other(v): if isinstance(v, bool): return not v if isinstance(v, int): return v + 1 if isinstance(v, float): # v * 2 + 1 is v itself at -1.0, which would change nothing. return v * 2 + 1 if v != -1.0 else 0.5 if isinstance(v, str): return v + "x" if v is None: return 0 if isinstance(v, list): return v + [copy.deepcopy(v[-1]) if v else 0] added = dict(v) added["z_added"] = 1 return added def walk(v, path): if isinstance(v, dict): for k in list(v): yield path + (k,), v[k], True for x in walk(v[k], path + (k,)): yield x elif isinstance(v, list): for i in sorted({0, len(v) - 1} if v else set()): yield path + (i,), v[i], True for x in walk(v[i], path + (i,)): yield x def set_at(b, path, value=None, remove=False): o = b for k in path[:-1]: o = o[k] if remove: del o[path[-1]] else: o[path[-1]] = value for path, v, removable in walk(body, ()): envelope = path[0] not in ("request", "result") name = "/".join(map(str, path)) b = copy.deepcopy(body) set_at(b, path, other(v)) added_to_receipt = path == ("result", "receipt") and isinstance(v, dict) # A set's item (section 8.6): its index, request, result, error and path are # read; anything else it holds is the host's, unsealed, as an item added to # is, and a member added to its own receipt is ignored as one added to a job's. in_item = len(path) >= 3 and path[:2] == ("result", "items") and body["result"].get("format") == "wai.quantum.set/1" item_extra = in_item and (len(path) == 3 and isinstance(v, dict) or len(path) >= 4 and path[3] not in ("index", "request", "result", "error", "path")) item_receipt = in_item and len(path) >= 5 and path[3:5] == ("result", "receipt") and (len(path) == 5 and isinstance(v, dict) or len(path) >= 6 and path[5] not in ("alg", "canon", "key", "digest", "signature", "time")) # A member of the receipt beyond its five and its time is ignored (section 8.2). ignored = len(path) >= 3 and path[:2] == ("result", "receipt") and path[2] not in ("alg", "canon", "key", "digest", "signature", "time") out.append((name + " replaced", b, "unchanged" if envelope or added_to_receipt or ignored or item_extra or item_receipt else "invalid")) if removable: b = copy.deepcopy(body) set_at(b, path, remove=True) out.append((name + " removed", b, "unchanged" if envelope or ignored or (item_extra and len(path) >= 4) or (item_receipt and len(path) >= 6) else "invalid")) return out # Whole numbers past what a double holds, and others a verifier might cap or round. EDGES = (2 ** 53, 2 ** 53 + 1, 1e16, 1e30, -1, -0.0, 0.5) SHOTS = (2 ** 53, 1e16, "300", 300.0, 0, None) def generator(): """generate.py, for its seal: it holds the published demo seed.""" spec = importlib.util.spec_from_file_location("receipts_generate", os.path.join(CORPUS, "generate.py")) module = importlib.util.module_from_spec(spec) spec.loader.exec_module(module) return module def edges(body, seal): """(what, changed body, "agree"): a provider's result, each number set to each of EDGES, and its shots in both its request and its result set to each of SHOTS. There is no oracle here but the other verifier: the point is a limit one has and the other does not. Those the demo key sealed are also sealed again, so that each is judged by what it says and not only by its digest.""" out = [] if not (isinstance(body.get("result"), dict) and body["result"].get("method") == "provider"): return out def numbers(v, path): if isinstance(v, dict): for k in v: if not (path == ("result",) and k == "receipt"): yield from numbers(v[k], path + (k,)) elif isinstance(v, list): for i in sorted({0, len(v) - 1} if v else set()): yield from numbers(v[i], path + (i,)) elif isinstance(v, (int, float)) and not isinstance(v, bool): yield path demo = seal is not None and isinstance(body["result"].get("receipt"), dict) and body["result"]["receipt"].get("key") == seal[1] def both(name, b): out.append((name, b, "agree")) if demo: out.append((name + ", sealed again", seal[0](b), "agree")) for path in numbers({"request": body.get("request"), "result": body["result"]}, ()): for value in EDGES: b = copy.deepcopy(body) o = b for k in path[:-1]: o = o[k] o[path[-1]] = value both("/".join(map(str, path)) + " set to %r" % (value,), b) for value in SHOTS: b = copy.deepcopy(body) b["request"]["shots"] = value b["result"]["shots"] = value both("the shots of both set to %r" % (value,), b) return out # ------------------------------------------------- the rules of a wasmQ job's form def rule_cases(corpus, seal): """(what, body, expected reasons): for each rule of quantum-wasmq section 6.5, the genuine wasmQ jobs of the corpus changed at the rule's bound, on both sides of it where it has two, and sealed again with the demo key, so that the rule alone decides. Each expected verdict is written here by hand from the text, as the manifest's are: none is copied from a verifier. A verifier with a rule dropped, or a bound moved, gives some case here another verdict.""" def load(name): with open(os.path.join(corpus, "jobs", name), encoding="utf-8") as f: return json.load(f) run, fault, init, job, frun, prior = (load("cli-wasmq-%s.json" % n) for n in ("run", "fault", "fault-init", "state-job", "fault-run", "fault-prior")) out = [] g = generator() def case(rule, what, base, edit, valid, respell=None): b = copy.deepcopy(base) edit(b) # With no call returned, the transcript the writer gives the result as changed # (rule 35), unless the change was to the transcript. sealed = seal(g.retranscribed(base, b)) if respell: # After the seal: another spelling of a number, not another value, so it holds. respell(sealed) sealed = spelt(sealed, g.Raw) out.append(("rule %s, %s" % (rule, what), sealed, [] if valid else ["wasmq_form"])) def contract(b): return b["request"]["wasmq"] def budget(name, value): def f(b): contract(b)["run"]["fuel"][name] = value b["result"]["fuel"]["budget"][name] = value return f def stretches(b): return sum(2 + len(m["priors"]) for m in contract(b)["modules"]) def second_module(bytes0, bytes1, named=True): def f(b): c = contract(b) c["modules"][0]["bytes"] = bytes0 c["modules"].append({"name": "second", "blake3": "cd" * 32, "bytes": bytes1, "priors": []}) b["result"]["modules"].append({"name": "second", "blake3": "cd" * 32}) if named: c["callouts"].append({"extern": "g", "module": 1, "export": "g"}) return f def each(*edits): def f(b): for e in edits: e(b) return f def at(path, value): def f(b): o = b for k in path[:-1]: o = o[k] o[path[-1]] = value return f def calls(b): (name, e), = b["result"]["fuel"]["callouts"].items() return e def passed(b): # What passing every prior to one shot's instances takes at the least (rule 21): # cabi_realloc, 2 at least, its bytes, and wasmq-prior, 1 at least. return sum(p["bytes"] + 3 for m in contract(b)["modules"] for p in m["priors"]) def shots(n): def f(b): width = len(next(iter(b["result"]["counts"]))) contract(b)["run"]["shots"] = b["result"]["shots"] = b["result"]["shots_run"] = n b["result"]["counts"] = {"1" * width: n} fuel = b["result"]["fuel"] more = max(0, n * passed(b) - fuel["instances"]) fuel.update(instances=fuel["instances"] + more, used=fuel["used"] + more) return f def later_shot(shot, state=None, instances=1, fuel=1, calls=None): # The init fault moved to `shot`, after that many shots of one call each. def f(b): n = shot if calls is None else calls if state: contract(b)["run"]["state"] = state b["result"].update(shots_run=shot, counts={"0": shot} if shot else {}, callouts=n) b["result"]["fuel"].update(instances=instances, callouts={"f": {"calls": n, "fuel": n, "max": 1}} if n else {}, used=instances + n) b["result"]["fault"].update(shot=shot, fuel=fuel) return f def fault_module(name): def f(b): second_module(57, 57)(b) b["result"]["fault"]["module"] = name return f def counts(width, n): return lambda b: b["result"].update(counts={"0" * width: n}) def work_left(b): # The most per_job the rest of rule 30's work leaves room for. c, r = contract(b), b["result"] n, s = r["qubits"], c["run"]["shots"] inst = 1 if c["run"]["state"] == "job" else s rest = s * 2 * n * max(1, -(-n // 32)) + inst * sum(4096 * (1 + 2 * len(m["priors"])) + m["bytes"] for m in c["modules"]) + 131072 * sum(m["bytes"] for m in c["modules"]) + 4097 * r["callouts"] return (2 ** 42 - rest) // 8 def frames(b): c = contract(b) return c["program"]["bytes"] + sum(m["bytes"] + sum(p["bytes"] for p in m["priors"]) for m in c["modules"]) def most_prior(b): # The most bytes the first prior may have: 2^27 less the envelope's other bytes, its # magic and lengths, its manifest, its contract and its other frames (rule 31). c, r = contract(b), b["result"] c["modules"][0]["priors"][0]["bytes"] = 10 ** 8 manifest = 192 + sum(len(str(x)) for x in (r["qubits"], c["run"]["shots"], c["run"]["seed"])) rest = 20 + manifest + len(g.text(c).encode("utf-8")) + frames(b) - 10 ** 8 return 2 ** 27 - rest def calls_of(n, max_fuel=1): # n calls of the run's one callout, each of 1 but the most. def f(b): b["result"]["callouts"] = n calls(b).update(calls=n, fuel=n - 1 + max_fuel, max=max_fuel) b["result"]["fuel"]["used"] = b["result"]["fuel"]["instances"] + calls(b)["fuel"] return f def own_prior(nbytes): # The first module given a prior of nbytes. return lambda b: contract(b)["modules"][0].update(priors=[{"name": "p", "blake3": "ef" * 32, "bytes": nbytes}]) def fault_of(reason, fuel): # The call's fault of `fault`, stopped for reason after fuel. def f(b): b["result"]["fault"].update(reason=reason, fuel=fuel) b["result"]["fault"].pop("budget", None) calls(b).update(calls=1, fuel=fuel, max=fuel) b["result"]["fuel"]["used"] = fuel return f def own_fuel(delta): def f(b): e = calls(b) e["fuel"] = e["max"] + delta b["result"]["fuel"]["used"] = b["result"]["fuel"]["instances"] + e["fuel"] return f R, F = ("result",), ("result", "fuel") # 1: no number past 2^53 - 1 (it breaks another rule too: each place a number may be holds it) case(1, "an input of 2^53", run, lambda b: contract(b)["program"].update(inputs={"n": 2 ** 53}), False) # 2: the request case(2, "a member the request does not define", run, at(("request", "x"), 1), False) case(2, "envelope_blake3 not a digest", run, lambda b: b["request"].update(envelope_blake3=b["request"]["envelope_blake3"].upper()), False) # 3, 4: the contract's members and profile case(3, "a member the contract does not define", run, lambda b: contract(b).update(x=1), False) case(3, "a member the run does not define", run, lambda b: contract(b)["run"].update(x=1), False) case(4, "another profile", run, lambda b: contract(b).update(profile="wai.quantum.wasmq/2"), False) # 5: the program case(5, "a program of 2^20 bytes", run, lambda b: contract(b)["program"].update(bytes=2 ** 20), True) case(5, "a program of 2^20 + 1 bytes", run, lambda b: contract(b)["program"].update(bytes=2 ** 20 + 1), False) case(5, "a program of 0 bytes", run, lambda b: contract(b)["program"].update(bytes=0), False) case(5, "a program of 1 byte", run, lambda b: contract(b)["program"].update(bytes=1), True) case(5, "an input of 2^53 - 1", run, lambda b: contract(b)["program"].update(inputs={"n": 2 ** 53 - 1}), True) case(5, "an input of -(2^53 - 1)", run, lambda b: contract(b)["program"].update(inputs={"n": -(2 ** 53 - 1)}), True) case(5, "an input of 0.5", run, lambda b: contract(b)["program"].update(inputs={"n": 0.5}), False) # 6: the modules and their priors case(6, "a module of 1 byte", run, lambda b: contract(b)["modules"][0].update(bytes=1), True) case(6, "a module of 0 bytes", run, lambda b: contract(b)["modules"][0].update(bytes=0), False) case(6, "a prior of 0 bytes", run, lambda b: contract(b)["modules"][0]["priors"][0].update(bytes=0), True) case(6, "a prior of 0.5 bytes", prior, lambda b: contract(b)["modules"][0]["priors"][0].update(bytes=0.5), False) case(6, "a module of 2^19 bytes", run, lambda b: contract(b)["modules"][0].update(bytes=2 ** 19), True) case(6, "a module of 2^19 + 1 bytes", run, lambda b: contract(b)["modules"][0].update(bytes=2 ** 19 + 1), False) case(6, "a module's priors null", run, lambda b: contract(b)["modules"][0].update(priors=None), False) case(6, "a prior's name null", run, lambda b: contract(b)["modules"][0]["priors"][0].update(name=None), False) case(6, "a module's name null, alike in the result", run, lambda b: (contract(b)["modules"][0].update(name=None), b["result"]["modules"][0].update(name=None)), False) case(6, "modules of 2^19 bytes together", run, second_module(2 ** 18, 2 ** 18), True) case(6, "modules of 2^19 + 1 bytes together", run, second_module(2 ** 18, 2 ** 18 + 1), False) # 7: the callouts case(7, "a module no callout names", run, second_module(39442, 1, named=False), False) case(7, "two callouts of one extern", run, lambda b: contract(b)["callouts"].append({"extern": "decode64", "module": 0, "export": "x"}), False) case(7, "a callout of a module the contract does not hold", run, lambda b: contract(b)["callouts"][0].update(module=1), False) case(7, "a callout of the module past the last, beside one of each module", run, lambda b: contract(b)["callouts"].append({"extern": "g", "module": 1, "export": "g"}), False) case(7, "a callout of the last module, beside one of each module", run, second_module(39442, 57), True) # No module and no callout: rule 7's first clause alone holds it, its others vacuous. def nothing(b): contract(b).update(modules=[], callouts=[]) b["result"].update(modules=[], callouts=0) b["result"]["fuel"].update(callouts={}, instances=0, used=0) case(7, "no module and no callout", run, nothing, False) case(7, "no module, null for the modules, and no callout", run, each(nothing, lambda b: contract(b).update(modules=None)), False) # 8: the run case(8, "2^20 shots", run, shots(2 ** 20), True) case(8, "2^20 + 1 shots", run, shots(2 ** 20 + 1), False) for name in ("per_call", "per_instance", "per_job"): # per_job at 2^39 is past rule 30's work beside any module: it is held there. case(30 if name == "per_job" else 8, "the budget %s at 2^39" % name, run, budget(name, 2 ** 39), name != "per_job") case(30 if name == "per_job" else 8, "the budget %s at 2^39 + 1" % name, run, budget(name, 2 ** 39 + 1), False) case(8, "a seed of 0, alike in the result", run, lambda b: (contract(b)["run"].update(seed=0), b["result"].update(seed=0)), True) case(8, "a seed below 0, alike in the result", run, lambda b: (contract(b)["run"].update(seed=-1), b["result"].update(seed=-1)), False) case(8, "a seed of 2^53 - 1, alike in the result", run, lambda b: (contract(b)["run"].update(seed=2 ** 53 - 1), b["result"].update(seed=2 ** 53 - 1)), True) case(8, "1 shot", run, shots(1), True) case(8, "0 shots", job, lambda b: (contract(b)["run"].update(shots=0), b["result"].update(shots=0, shots_run=0, counts={}, callouts=0), b["result"]["fuel"].update(callouts={}, used=b["result"]["fuel"]["instances"])), False) case(8, "a budget of 0", fault, budget("per_instance", 0), True) case(8, "a call's budget of 0, its one call stopped at once", fault, each(budget("per_call", 0), lambda b: (calls(b).update(fuel=0, max=0), b["result"]["fuel"].update(used=0), b["result"]["fault"].update(fuel=0))), True) case(8, "another state", run, at(("request", "wasmq", "run", "state"), "call"), False) # 9, 10: the result's members, and the form of its seal case(9, "a member the result does not define", run, at(R + ("x",), 1), False) first = copy.deepcopy(run) out.append(("rule 10, sealed in the first form", seal(first, form="first"), ["wasmq_form"])) # 11: what the result repeats case(11, "another seed in the result", run, lambda b: b["result"].update(seed=b["result"]["seed"] + 1), False) case(11, "another shots in the result", run, lambda b: b["result"].update(shots=b["result"]["shots"] + 1), False) case(11, "another accuracy", run, at(R + ("accuracy",), {"class": "exact", "x": 1}), False) case(11, "another energy", run, at(R + ("energy",), {"unmetered": "a meter"}), False) # 12: qubits case(12, "2^15 qubits", run, at(R + ("qubits",), 2 ** 15), True) case(12, "1 qubit", run, at(R + ("qubits",), 1), True) case(12, "0 qubits", run, at(R + ("qubits",), 0), False) case(12, "qubits null", run, at(R + ("qubits",), None), False) case(12, "2^15 + 1 qubits", run, at(R + ("qubits",), 2 ** 15 + 1), False) # 13: the fuel's budget and what it used case(13, "used equal to per_job", run, lambda b: budget("per_job", b["result"]["fuel"]["used"])(b), True) case(13, "used past per_job", run, lambda b: budget("per_job", b["result"]["fuel"]["used"] - 1)(b), False) case(13, "a budget the contract does not give", run, lambda b: b["result"]["fuel"]["budget"].update(per_call=b["result"]["fuel"]["budget"]["per_call"] + 1), False) # 14: each callout's fuel case(14, "a call's largest equal to per_call", run, lambda b: budget("per_call", calls(b)["max"])(b), True) case(14, "a call's largest past per_call", run, lambda b: budget("per_call", calls(b)["max"] - 1)(b), False) case(14, "a call's largest equal to its fuel", fault, own_fuel(0), True) case(14, "a call's largest past its fuel", run, own_fuel(-1), False) case(14, "a callout with no call", run, lambda b: (calls(b).update(calls=0, fuel=0, max=0), b["result"].update(callouts=0), b["result"]["fuel"].update(used=b["result"]["fuel"]["instances"])), False) case(20, "fuel past its calls of their largest", run, lambda b: (calls(b).update(fuel=calls(b)["calls"] * calls(b)["max"] + 1), b["result"]["fuel"].update(used=b["result"]["fuel"]["instances"] + calls(b)["fuel"])), False) # 15: what adds up case(15, "a call more than the fuel counts", run, lambda b: b["result"].update(callouts=b["result"]["callouts"] + 1), False) # 16: the result's modules case(16, "a module of the result named otherwise", run, lambda b: b["result"]["modules"][0].update(name="other"), False) # 17: what the instances could be given case(17, "a fault's instance counted: one, given 1 each stretch", init, budget("per_instance", 1), True) case(17, "one instance for the run, at its bound", job, lambda b: budget("per_instance", -(-b["result"]["fuel"]["instances"] // stretches(b)))(b), True) case(17, "one instance for the run, past its bound", job, lambda b: budget("per_instance", (b["result"]["fuel"]["instances"] - 1) // stretches(b))(b), False) # 18: how it ended case(18, "a fault in init within its phase's budget", init, each(budget("per_instance", 2), at(F + ("instances",), 2), at(F + ("used",), 2), at(R + ("fault", "fuel"), 2)), True) case(18, "a fault in init past its phase's budget", init, each(budget("per_instance", 1), at(F + ("instances",), 2), at(F + ("used",), 2), at(R + ("fault", "fuel"), 2)), False) case(18, "a fault after every shot", fault, lambda b: (b["result"].update(shots_run=32, counts={"0": 32}), b["result"]["fault"].update(shot=32)), False) case(18, "a fault in another shot than the next", fault, at(R + ("fault", "shot"), 1), False) case(28, "a call's fuel fault of the run's budget, with the run's budget not spent", fault, at(R + ("fault", "budget"), "run"), False) case(18, "a call's fuel fault of the instance's budget", fault, at(R + ("fault", "budget"), "instance"), False) case(18, "a fault in init that names a callout", init, at(R + ("fault", "callout"), "f"), False) case(18, "a call's fault the fuel counts no call of", fault, lambda b: (b["result"].update(callouts=0), b["result"]["fuel"].update(callouts={}, instances=400)), False) case(18, "a call that stopped at its callout's largest", fault, lambda b: (b["result"].update(callouts=2), b["result"]["fuel"]["callouts"]["f"].update(calls=2, fuel=401, max=400), b["result"]["fuel"].update(used=401)), True) case(18, "a call that stopped past its callout's largest", fault, lambda b: (b["result"].update(callouts=2), b["result"]["fuel"]["callouts"]["f"].update(calls=2, fuel=401, max=399), b["result"]["fuel"].update(used=401)), False) case(18, "a lifecycle fault whose callout is null", init, at(R + ("fault", "callout"), None), False) case(18, "a trap whose budget is null", init, at(R + ("fault", "budget"), None), False) case(18, "a trap in seed", init, at(R + ("fault", "phase"), "seed"), True) case(18, "a fault in another phase", init, at(R + ("fault", "phase"), "start"), False) case(18, "a trap of another reason the profile names", init, at(R + ("fault", "reason"), "invalid_conversion_to_integer"), True) case(18, "a fault in a shot after shots_run", frun, at(R + ("fault", "shot"), 1), False) case(18, "a fault in a module named null", init, at(R + ("fault", "module"), None), False) case(18, "a trap that names a budget", init, at(R + ("fault", "budget"), "instance"), False) case(18, "an ok result whose fault is null", run, at(R + ("fault",), None), False) case(18, "a call's fault whose callout is null", fault, at(R + ("fault", "callout"), None), False) case(18, "a fuel fault whose budget is null", fault, at(R + ("fault", "budget"), None), False) # 19: the counts case(19, "outcomes of two widths", run, lambda b: (b["result"]["counts"].update({next(iter(b["result"]["counts"])): b["result"]["counts"][next(iter(b["result"]["counts"]))] - 1}), b["result"]["counts"].update({"0": 1})), False) case(19, "a count of 0", run, lambda b: b["result"]["counts"].update({"0" * len(next(iter(b["result"]["counts"]))): 0}), False) case(19, "an outcome of no bits", run, counts(0, 32), True) case(19, "an outcome holding a 2", run, lambda b: b["result"].update(counts={"012": 32}), False) case(19, "counts null", fault, at(R + ("counts",), None), False) # Round 4's labelled cases, each where a weakening of one rule moves a verdict. case(2, "envelope_blake3 of 65 digits", run, lambda b: b["request"].update(envelope_blake3=b["request"]["envelope_blake3"] + "0"), False) case(12, "transcript_blake3 of 63 digits", run, lambda b: b["result"].update(transcript_blake3=b["result"]["transcript_blake3"][:63]), False) case(3, "run's fuel a member more, the budget alike", run, budget("z", 1), False) case(3, "the program a member more", run, lambda b: contract(b)["program"].update(z=1), False) case(4, "a profile one letter longer", run, lambda b: contract(b).update(profile="wai.quantum.wasmq/1x"), False) case(5, "inputs null", run, lambda b: contract(b)["program"].update(inputs=None), False) case(5, "the program's bytes 1104.5", run, lambda b: contract(b)["program"].update(bytes=1104.5), False) case(5, "an input that is true", run, lambda b: contract(b)["program"].update(inputs={"n": True}), False) case(6, "a module's bytes 39442.5", run, lambda b: contract(b)["modules"][0].update(bytes=39442.5), False) case(7, "an export null", run, lambda b: contract(b)["callouts"][0].update(export=None), False) case(7, "an extern null, with no call made", init, lambda b: contract(b)["callouts"][0].update(extern=None), False) case(7, "a callout of module 0.5", run, lambda b: contract(b)["callouts"].append({"extern": "g", "module": 0.5, "export": "g"}), False) def respell(path, text, value): def f(s): o = s for k in path[:-1]: o = o[k] o[path[-1]] = g.Raw(text, value) return f case(11, "the result's seed written 1234.0", run, lambda b: None, True, respell(R + ("seed",), "1234.0", run["result"]["seed"])) case(12, "qubits written 17.0", run, lambda b: None, True, respell(R + ("qubits",), "17.0", 17)) case(13, "a budget written 1e7", run, lambda b: None, True, respell(F + ("budget", "per_call"), "1e7", 10000000)) case(14, "the callouts' fuel null", init, at(F + ("callouts",), None), False) case(14, "the callouts' fuel an array", init, at(F + ("callouts",), []), False) case(15, "a call fewer than the fuel counts", run, lambda b: b["result"].update(callouts=b["result"]["callouts"] - 1), False) case(16, "the result's modules in another order", run, lambda b: (second_module(39442, 1)(b), b["result"].update(modules=b["result"]["modules"][::-1])), False) case(17, "the instances' fuel past 32 x S x per_instance", run, budget("per_instance", 2583), False) case(17, "one instance for the run, a fault, past 1 x S x per_instance", init, each(at(("request", "wasmq", "run", "state"), "job"), budget("per_instance", 1), at(F + ("instances",), 3), at(F + ("used",), 3)), False) case(25, "an init fault's fuel past what was used", init, at(R + ("fault", "fuel"), 2), False) case(18, "a call's fault past its callout's max", frun, at(R + ("fault", "fuel"), 24), False) case(18, "an ok result one shot past its shots", run, lambda b: (b["result"]["counts"].update({next(iter(b["result"]["counts"])): b["result"]["counts"][next(iter(b["result"]["counts"]))] + 1}), b["result"].update(shots_run=33)), False) # 20: the fuel of the calls that returned, each 1 to the most one used case(20, "calls that returned using 1 each", run, lambda b: (calls(b).update(fuel=32, max=1), b["result"]["fuel"].update(used=b["result"]["fuel"]["instances"] + 32)), True) case(20, "calls that returned using nothing", run, lambda b: (calls(b).update(fuel=0, max=0), b["result"]["fuel"].update(used=b["result"]["fuel"]["instances"])), False) case(20, "two calls that returned and one that stopped, in 6", frun, each(budget("per_job", 6), lambda b: (calls(b).update(fuel=6, max=4), b["result"]["fuel"].update(used=6))), True) case(20, "two calls that returned and one that stopped, in 5", frun, each(budget("per_job", 5), lambda b: (calls(b).update(fuel=5, max=4), b["result"]["fuel"].update(used=5))), False) case(20, "calls that returned at the most one used", frun, lambda b: calls(b).update(max=23), True) case(20, "calls that returned past the most one used", frun, lambda b: calls(b).update(max=21), False) case(20, "the one call, the one that stopped, its fuel more than the fault's", fault, lambda b: (b["result"]["fault"].update(reason="unreachable", fuel=10), b["result"]["fault"].pop("budget")), False) case(20, "the one call, the one that stopped, its fuel the fault's", fault, lambda b: (b["result"]["fault"].update(reason="unreachable", fuel=10), b["result"]["fault"].pop("budget"), calls(b).update(fuel=10, max=10), b["result"]["fuel"].update(used=10)), True) # 21: the priors passed to each shot's instances case(21, "instances that passed each prior at the least", run, lambda b: b["result"]["fuel"].update(instances=32 * passed(b), used=32 * passed(b) + calls(b)["fuel"]), True) case(21, "instances that passed the priors in less", run, lambda b: b["result"]["fuel"].update(instances=32 * passed(b) - 1, used=32 * passed(b) - 1 + calls(b)["fuel"]), False) case(21, "one instance for the run, its prior in less", job, lambda b: b["result"]["fuel"].update(instances=passed(b) - 1, used=passed(b) - 1 + calls(b)["fuel"]), False) case(21, "a prior's fault: no prior passed whole", prior, lambda b: None, True) # 22: a call's fault in its callout's module case(22, "a call's fault in its callout's module, beside another", fault, fault_module("m"), True) case(22, "a call's fault in the other module", fault, fault_module("second"), False) # 23, 24: a phase against the module's priors, a reason against its phase case(23, "a prior's fault in a module with none", init, at(R + ("fault", "phase"), "prior"), False) case(24, "a bad_result while a prior is passed", prior, at(R + ("fault", "reason"), "bad_result"), True) case(24, "a bad_result in a call", fault, each(at(R + ("fault", "reason"), "bad_result"), lambda b: b["result"]["fault"].pop("budget")), True) case(24, "a bad_result in init", init, at(R + ("fault", "reason"), "bad_result"), False) case(24, "a bad_result in seed", init, each(at(R + ("fault", "reason"), "bad_result"), at(R + ("fault", "phase"), "seed")), False) # 25, 26, 27: a lifecycle fault against the instances, the state and the calls case(25, "an init fault in shot 1 within the instances' fuel", init, later_shot(1, instances=3, fuel=2), True) case(25, "an init fault in shot 1, shot 0's init uncounted", init, later_shot(1, instances=2, fuel=2), False) case(25, "an init fault in shot 1 past the instances' fuel", init, later_shot(1, instances=1, fuel=2), False) case(26, "one instance for the run, failing in shot 0", init, at(("request", "wasmq", "run", "state"), "job"), True) case(26, "one instance for the run, failing in shot 2", init, later_shot(2, state="job"), False) case(26, "a fresh instance each shot, failing in shot 2", init, later_shot(2, instances=3), True) case(27, "the first shot's instances failing after a call", init, later_shot(0, calls=1), False) # 28: a fuel fault used its whole limit case(28, "a call's fuel fault at its limit", fault, each(budget("per_call", 10), lambda b: (calls(b).update(fuel=10, max=10), b["result"]["fuel"].update(used=10), b["result"]["fault"].update(fuel=10))), True) case(28, "a call's fuel fault under its limit", fault, lambda b: (calls(b).update(fuel=10, max=10), b["result"]["fuel"].update(used=10), b["result"]["fault"].update(fuel=10)), False) case(28, "an instance's fuel fault at its limit", init, each(budget("per_instance", 1), at(R + ("fault", "reason"), "fuel_exhausted"), at(R + ("fault", "budget"), "instance")), True) case(28, "an instance's fuel fault under its limit", init, each(at(R + ("fault", "reason"), "fuel_exhausted"), at(R + ("fault", "budget"), "instance")), False) case(28, "the run's budget run out, not all used", frun, budget("per_job", 51), False) case(28, "the run's budget the limit, under the call's own", frun, each(budget("per_call", 24), at(R + ("fault", "fuel"), 23), lambda b: calls(b).update(max=23)), True) case(28, "the run's budget the limit, at the call's own", frun, each(budget("per_call", 23), at(R + ("fault", "fuel"), 23)), False) case(28, "an instance's run budget, at the instance's own", init, each(budget("per_job", 1), budget("per_instance", 1), at(R + ("fault", "reason"), "fuel_exhausted"), at(R + ("fault", "budget"), "run")), False) case(28, "an instance's run budget, under the instance's own", init, each(budget("per_job", 1), budget("per_instance", 2), at(R + ("fault", "reason"), "fuel_exhausted"), at(R + ("fault", "budget"), "run")), True) # 29: the bits of a shot, and of the shots case(29, "outcomes of 2^20 bits", run, counts(2 ** 20, 32), True) case(29, "outcomes of 2^20 + 1 bits", run, counts(2 ** 20 + 1, 32), False) case(29, "2^20 shots of 256 bits", frun, each(lambda b: (contract(b)["run"].update(shots=2 ** 20), b["result"].update(shots=2 ** 20)), counts(256, 2)), True) case(29, "2^20 shots of 257 bits", frun, each(lambda b: (contract(b)["run"].update(shots=2 ** 20), b["result"].update(shots=2 ** 20)), counts(257, 2)), False) # 30: the work a receipt shows case(30, "per_job at the most the rest leaves", run, lambda b: budget("per_job", work_left(b))(b), True) case(30, "per_job one past it", run, lambda b: budget("per_job", work_left(b) + 1)(b), False) case(30, "2^15 qubits over 2^20 shots", frun, each(lambda b: (contract(b)["run"].update(shots=2 ** 20), b["result"].update(shots=2 ** 20, qubits=2 ** 15))), False) case(30, "one instance for the run: its instance counted once", job, lambda b: budget("per_job", work_left(b))(b), True) # 31: the envelope case(31, "an envelope of 2^27 bytes", prior, lambda b: contract(b)["modules"][0]["priors"][0].update(bytes=most_prior(b)), True) case(31, "an envelope of 2^27 + 1 bytes", prior, lambda b: contract(b)["modules"][0]["priors"][0].update(bytes=most_prior(b) + 1), False) case(31, "frames one short of 2^27, the envelope past it", prior, lambda b: contract(b)["modules"][0]["priors"][0].update(bytes=2 ** 27 - 1 - (frames(b) - contract(b)["modules"][0]["priors"][0]["bytes"])), False) # 20: the most one call used, a returned call's, and each other 1 at least case(20, "32 calls, the most 21751, in 21751 + 31", run, calls_of(32, 21751), True) case(20, "32 calls, the most 21751, in 21751 + 30", run, each(calls_of(32, 21751), lambda b: (calls(b).update(fuel=21751 + 30), b["result"]["fuel"].update(used=b["result"]["fuel"]["instances"] + 21751 + 30))), False) case(20, "two returned, the most 23, beside a stopped call of 4, in 28", frun, each(budget("per_job", 28), lambda b: (calls(b).update(fuel=28, max=23), b["result"]["fuel"].update(used=28))), True) case(20, "two returned, the most 23, beside a stopped call of 4, in 27", frun, each(budget("per_job", 27), lambda b: (calls(b).update(fuel=27, max=23), b["result"]["fuel"].update(used=27))), False) case(20, "one returned in 5, then one stopped at 0, the run's budget spent", frun, each(budget("per_job", 5), lambda b: (b["result"].update(callouts=2), calls(b).update(calls=2, fuel=5, max=5), b["result"]["fuel"].update(used=5), b["result"]["fault"].update(fuel=0))), True) case(20, "two returned in 11, the most 10, then one stopped at 0", frun, each(budget("per_job", 11), lambda b: (calls(b).update(fuel=11, max=10), b["result"]["fuel"].update(used=11), b["result"]["fault"].update(fuel=0))), True) case(20, "two returned in 10, the most 10, then one stopped at 0", frun, each(budget("per_job", 10), lambda b: (calls(b).update(fuel=10, max=10), b["result"]["fuel"].update(used=10), b["result"]["fault"].update(fuel=0))), False) # 21, 25: what a lifecycle fault shows of the set it stopped case(25, "an init stopped after its 100-byte prior, in 104", init, each(own_prior(100), at(F + ("instances",), 104), at(F + ("used",), 104)), True) case(25, "an init stopped after its 100-byte prior, in 103", init, each(own_prior(100), at(F + ("instances",), 103), at(F + ("used",), 103)), False) case(21, "an init stopped after its 100-byte prior, in 102", init, each(own_prior(100), at(F + ("instances",), 102), at(F + ("used",), 102)), False) case(25, "a seed stopped after its 100-byte prior's module, passed none", init, each(own_prior(100), at(R + ("fault", "phase"), "seed")), True) case(25, "the second module's init stopped after the first's prior, in 104", init, each(second_module(50, 57), own_prior(100), at(R + ("fault", "module"), "second"), at(F + ("instances",), 104), at(F + ("used",), 104)), True) case(25, "the second module's init stopped after the first's prior, in 103", init, each(second_module(50, 57), own_prior(100), at(R + ("fault", "module"), "second"), at(F + ("instances",), 103), at(F + ("used",), 103)), False) case(25, "a seed stopped in shot 1, shot 0's seed shown", init, each(later_shot(1, instances=2, fuel=1), at(R + ("fault", "phase"), "seed")), True) case(25, "a seed stopped in shot 1, shot 0's seed uncounted", init, each(later_shot(1, instances=1, fuel=1), at(R + ("fault", "phase"), "seed")), False) # 29: the longest name, in characters case(29, "two widths, the longer past 2^20", run, lambda b: b["result"].update(counts={next(iter(b["result"]["counts"])): 31, "0" * (2 ** 20 + 1): 1}), False) case(19, "2^20 shots of a name of 256 characters in 257 bytes", frun, each(lambda b: (contract(b)["run"].update(shots=2 ** 20), b["result"].update(shots=2 ** 20)), lambda b: b["result"].update(counts={"\u00e9" + "0" * 255: 2})), False) case(29, "2^20 shots of a name of 257 characters", frun, each(lambda b: (contract(b)["run"].update(shots=2 ** 20), b["result"].update(shots=2 ** 20)), lambda b: b["result"].update(counts={"\u00e9" + "0" * 256: 2})), False) # 32: the calls a shot can make case(32, "32 shots of 2^21 calls", run, calls_of(32 * 2 ** 21), True) case(32, "32 shots of 2^21 calls and one more", run, calls_of(32 * 2 ** 21 + 1), False) case(32, "a call's fault in the first shot, after 2^21 - 1 calls", fault, lambda b: (b["result"].update(callouts=2 ** 21), calls(b).update(calls=2 ** 21, fuel=2 ** 21 - 1 + 400), b["result"]["fuel"].update(used=2 ** 21 - 1 + 400)), True) case(32, "a call's fault in the first shot, after 2^21 calls", fault, lambda b: (b["result"].update(callouts=2 ** 21 + 1), calls(b).update(calls=2 ** 21 + 1, fuel=2 ** 21 + 400), b["result"]["fuel"].update(used=2 ** 21 + 400)), False) # 33: a prior passed whole within one lifecycle call's limit case(33, "a prior of 87 bytes under 90 a lifecycle call", run, each(budget("per_instance", 90), at(F + ("instances",), 32 * 90), at(F + ("used",), 32 * 90 + 588348)), True) case(33, "a prior of 87 bytes under 89 a lifecycle call", run, each(budget("per_instance", 89), at(F + ("instances",), 32 * 90), at(F + ("used",), 32 * 90 + 588348)), False) case(33, "an init stopped after its 100-byte prior, under 103", init, each(own_prior(100), budget("per_instance", 103), at(F + ("instances",), 104), at(F + ("used",), 104)), True) case(33, "an init stopped after its 100-byte prior, under 102", init, each(own_prior(100), budget("per_instance", 102), at(F + ("instances",), 104), at(F + ("used",), 104)), False) # 34: what a fault's reason shows was charged case(34, "a trap after nothing charged", init, each(at(R + ("fault", "fuel"), 0)), False) case(34, "a result that is not one, after 2", fault, fault_of("bad_result", 2), True) case(34, "a result that is not one, after 1", fault, fault_of("bad_result", 1), False) case(34, "the stack past 2^23 after 788", fault, each(budget("per_call", 1000), fault_of("stack_exhausted", 788)), True) case(34, "the stack past 2^23 after 787", fault, each(budget("per_call", 1000), fault_of("stack_exhausted", 787)), False) # 35: the transcript of no returned call case(35, "an ok run of no call, its transcript the prefix's", run, lambda b: (b["result"].update(callouts=0), b["result"]["fuel"].update(callouts={}, used=b["result"]["fuel"]["instances"])), True) case(35, "an ok run of no call, its transcript the calls'", run, lambda b: (b["result"].update(callouts=0, transcript_blake3=b["result"]["transcript_blake3"][::-1]), b["result"]["fuel"].update(callouts={}, used=b["result"]["fuel"]["instances"])), False) case(35, "a call's fault of no returned call, another transcript", fault, at(R + ("transcript_blake3",), "ab" * 32), False) case(35, "a lifecycle fault, another transcript", init, at(R + ("transcript_blake3",), "ab" * 32), False) # Places where a member's own rule and another's both read it: each verifier must state # every rule it breaks, so that one reading it otherwise in one rule shows. case(13, "per_job 2^53, alike in the result", run, budget("per_job", 2 ** 53), False) case(6, "a module's blake3 in upper case, alike in the result", run, lambda b: (contract(b)["modules"][0].update(blake3=contract(b)["modules"][0]["blake3"].upper()), b["result"]["modules"][0].update(blake3=b["result"]["modules"][0]["blake3"].upper())), False) def named_one(b): contract(b)["modules"][0]["name"] = 1 b["result"]["modules"][0]["name"] = 1 if "fault" in b["result"]: b["result"]["fault"]["module"] = 1 case(6, "a module named 1, the result's module 1.0", run, named_one, False, respell(R + ("modules", 0, "name"), "1.0", 1)) case(6, "a module named 1, an init's fault in 1.0", init, named_one, False, respell(R + ("fault", "module"), "1.0", 1)) case(6, "a module named 1, a prior's fault in 1.0", prior, named_one, False, respell(R + ("fault", "module"), "1.0", 1)) case(26, "one instance for the run, a fault in shot 0.5", init, each(at(("request", "wasmq", "run", "state"), "job"), at(R + ("fault", "shot"), 0.5)), False) case(18, "a fault in shot 0.5, after a call", init, each(at(R + ("fault", "shot"), 0.5), at(R + ("callouts",), 1)), False) # A lifecycle fault is one that has a phase: null among them, absent not. case(26, "a fault whose phase is null, in shot 2 of one instance for the run", init, each(later_shot(2, state="job"), at(R + ("fault", "phase"), None)), False) case(18, "a fault with no phase, in shot 2 of one instance for the run", init, each(later_shot(2, state="job"), lambda b: b["result"]["fault"].pop("phase")), False) # The second version (quantum-wasmq section 11.6): rules 4, 8, 11, 12 and 30 as it reads # them, and 36, its energy (section 11.5), each case one of the second version's genuine # jobs (the command line's, from its envelopes) changed at the rule's bound and sealed # again. Its other rules are the first version's, held above. tof, stab = (load("cli-wasmq2-%s.json" % n) for n in ("t-toffoli", "stabilizer")) E = ("result", "energy") V1_ENERGY = {"unmetered": "the runner reads no energy meter; fuel is the profile's measure of work"} def reading(joules=1200, ppm=None, window=9000, provenance="OnChipCounter", **more): # A reading at the floor unless told otherwise: joules x ppm >= 288 676. f = {"joules_micro": joules, "energy_provenance": provenance, "energy_uncertainty": {"relative_ppm": -(-288676 // max(joules, 1)) if ppm is None else ppm, "window_us": window}} f.update(more) return f def method(m, accuracy=None): def f(b): contract(b)["run"]["method"] = m b["result"]["method"] = m if accuracy is not None: b["result"]["accuracy"] = {"class": accuracy} return f def called(b): return sorted(b["result"]["fuel"]["callouts"]) def exact_shots_left(b): # The most shots rule 30 leaves the exact method at the job's qubits: each shot's # fresh state of 2 x 2^n, and its instances, beside the rest of the work. c, r = contract(b), b["result"] inst = sum(4096 * (1 + 2 * len(m["priors"])) + m["bytes"] for m in c["modules"]) one = c["run"]["state"] == "job" fixed = (inst if one else 0) + 131072 * sum(m["bytes"] for m in c["modules"]) + 4097 * r["callouts"] + 8 * c["run"]["fuel"]["per_job"] return (2 ** 42 - fixed) // (2 * 2 ** r["qubits"] + (0 if one else inst)) def at_26(extra): def f(b): b["result"]["qubits"] = 26 shots(exact_shots_left(b) + extra)(b) return f # 4, 8, 11: the profile, the methods, the accuracy each method states case(4, "v2: a job as the second version writes it", tof, lambda b: None, True) case(4, "v2: the first version's profile in a second version's contract", tof, lambda b: contract(b).update(profile="wai.quantum.wasmq/1"), False) case(8, "v2: a method of neither version", tof, method("statevector"), False) case(8, "v2: the exact method asked of a Clifford program, bit-exact", stab, method("exact", "bit-exact"), True) case(11, "v2: an exact run said to be exact", tof, at(R + ("accuracy",), {"class": "exact"}), False) case(11, "v2: a stabilizer run said to be bit-exact", stab, at(R + ("accuracy",), {"class": "bit-exact"}), False) case(11, "v2: the result's profile the first version's", tof, at(R + ("profile",), "wai.quantum.wasmq/1"), False) case(11, "v2: the result's method not the contract's", stab, at(R + ("method",), "exact"), False) case(11, "v2: a second version's job whose result's format is the first's", tof, at(R + ("format",), "wai.quantum.wasmq.result/1"), False) # 12: the exact method's 26 qubits case(12, "v2: the exact method at 26 qubits", tof, at(R + ("qubits",), 26), True) case(12, "v2: the exact method at 27 qubits", tof, at(R + ("qubits",), 27), False) case(12, "v2: the stabilizer method at 27 qubits", stab, at(R + ("qubits",), 27), True) # 30: the exact method's fresh state, each shot case(30, "v2: 26 qubits by the exact method, the most shots the work leaves", tof, at_26(0), True) case(30, "v2: 26 qubits by the exact method, one shot more", tof, at_26(1), False) case(30, "v2: 26 qubits by the stabilizer method, past the exact method's shots", stab, at_26(1), True) # 36: the energy, a figure for the run and one for each callout the run called case(36, "v2: the run unmetered, saying why", tof, at(E + ("run",), {"unmetered": "no meter here"}), True) case(36, "v2: the run unmetered, saying nothing", tof, at(E + ("run",), {"unmetered": ""}), False) case(36, "v2: the run unmetered, its reason null", tof, at(E + ("run",), {"unmetered": None}), False) case(36, "v2: the run unmetered beside a figure of 0", tof, at(E + ("run",), {"unmetered": "no meter", "joules_micro": 0}), False) case(36, "v2: a reading of 1 microjoule at the floor", tof, at(E + ("run",), reading(1, 288676)), True) case(36, "v2: a reading of 1 microjoule one ppm below the floor", tof, at(E + ("run",), reading(1, 288675)), False) case(36, "v2: a reading of 288676 microjoules at 1 ppm", tof, at(E + ("run",), reading(288676, 1)), True) case(36, "v2: a reading of 288675 microjoules at 1 ppm", tof, at(E + ("run",), reading(288675, 1)), False) case(36, "v2: a reading of 0 microjoules", tof, at(E + ("run",), reading(0, 1)), False) case(36, "v2: a reading of 1200.5 microjoules", tof, at(E + ("run",), reading(1200.5, 241)), False) case(36, "v2: an estimate as a reading", tof, at(E + ("run",), reading(provenance="Estimator")), False) case(36, "v2: the legacy HwShunt as a reading's class", tof, at(E + ("run",), reading(provenance="HwShunt")), True) case(36, "v2: a reading that says more", tof, at(E + ("run",), reading(coverage="whole", attribution="none")), True) case(36, "v2: a reading of no window", tof, at(E + ("run",), reading(window=0)), False) case(36, "v2: a reading over a window of 1 microsecond", tof, at(E + ("run",), reading(window=1)), True) case(36, "v2: a reading with no uncertainty", tof, at(E + ("run",), {"joules_micro": 1200, "energy_provenance": "OnChipCounter"}), False) case(36, "v2: no run's figure", tof, lambda b: b["result"]["energy"].pop("run"), False) case(36, "v2: a callout's figure a reading", tof, lambda b: b["result"]["energy"]["callouts"].update({called(b)[0]: reading()}), True) case(36, "v2: no figure for a callout the run called", tof, lambda b: b["result"]["energy"]["callouts"].pop(called(b)[0]), False) case(36, "v2: a figure for a callout the run did not call", tof, lambda b: b["result"]["energy"]["callouts"].update(other={"unmetered": "no meter"}), False) case(36, "v2: a callout's figure of 0 microjoules", tof, lambda b: b["result"]["energy"]["callouts"].update({called(b)[0]: reading(0, 1)}), False) case(36, "v2: the callouts' energy an array", tof, at(E + ("callouts",), []), False) case(36, "v2: the energy a member more", tof, at(E + ("total",), 1), False) case(36, "v2: the first version's energy", tof, at(E, V1_ENERGY), False) case(36, "v2: no call made, and no callout's energy", tof, lambda b: (b["result"].update(callouts=0), b["result"]["fuel"].update(callouts={}, used=b["result"]["fuel"]["instances"]), b["result"]["energy"].update(callouts={})), True) case(1, "v2: a reading of 2^53 microjoules", tof, at(E + ("run",), reading(2 ** 53, 1)), False) # The format decides the version: a first-version job named the second's throughout is # held to the second's rules and keeps them; named by its format alone, it breaks them. def as_second(b): contract(b)["profile"] = "wai.quantum.wasmq/2" b["result"].update(format="wai.quantum.wasmq.result/2", profile="wai.quantum.wasmq/2") b["result"]["energy"] = {"run": {"unmetered": "no meter"}, "callouts": dict((k, {"unmetered": "no meter"}) for k in called(b))} case("versions", "a first-version job named the second's throughout", run, as_second, True) # Each number of a reading is a count: one written with a fraction, or below 0, is none. case(36, "v2: a reading's relative_ppm below 0", tof, at(E + ("run",), reading(1, -288676)), False) case(36, "v2: a reading's relative_ppm with a fraction", tof, at(E + ("run",), reading(1, 288676.5)), False) case(36, "v2: a reading's window_us below 0", tof, at(E + ("run",), reading(window=-9000)), False) case(36, "v2: a reading's window_us with a fraction", tof, at(E + ("run",), reading(window=9000.5)), False) # 11: what the result repeats is compared as JSON values, numbers by value. case(11, "v2: the result's shots written 64.0", tof, lambda b: None, True, respell(R + ("shots",), "64.0", tof["result"]["shots"])) # 30: the exact method's work at 2^42 exactly, the budget per_job taking up what is left. def exact_at_the_bound(extra): def f(b): b["result"]["qubits"] = 26 n = exact_shots_left(b) c, r = contract(b), b["result"] inst = sum(4096 * (1 + 2 * len(m["priors"])) + m["bytes"] for m in c["modules"]) one = c["run"]["state"] == "job" def work(shots_n, per_job): return (shots_n * 2 * 2 ** 26 + (1 if one else shots_n) * inst + 131072 * sum(m["bytes"] for m in c["modules"]) + 4097 * r["callouts"] + 8 * per_job) per_job = c["run"]["fuel"]["per_job"] while (2 ** 42 - work(n, per_job)) % 8: n -= 1 shots(n)(b) budget("per_job", per_job + (2 ** 42 - work(n, per_job)) // 8 + extra)(b) return f case(30, "v2: the exact method's work at 2^42 exactly", tof, exact_at_the_bound(0), True) case(30, "v2: the exact method's work 8 past 2^42", tof, exact_at_the_bound(1), False) # 31: the envelope a second-version contract names, at its bound and one byte past it. case(31, "v2: an envelope of 2^27 bytes", prior, lambda b: (as_second(b), contract(b)["modules"][0]["priors"][0].update(bytes=most_prior(b))), True) case(31, "v2: an envelope of 2^27 + 1 bytes", prior, lambda b: (as_second(b), contract(b)["modules"][0]["priors"][0].update(bytes=most_prior(b) + 1)), False) case("versions", "a first-version job named the second's by its format alone", run, at(R + ("format",), "wai.quantum.wasmq.result/2"), False) case("versions", "a first-version job with the second's energy", run, at(E, {"run": {"unmetered": "no meter"}, "callouts": {}}), False) # Every member of each genuine job given a value of another kind (half a unit off, below # 0, past 2^53 - 1, null, a digest in upper case), sealed again. No member of a wasmQ job # holds such a value: each verifier must refuse each, and both must state the same rules # broken (the differential holds them to that), so that a rule's check read loosely in # one, or a null read as absent, shows wherever another rule's check also refuses it. def leaves(v, path): if isinstance(v, dict): for k, x in v.items(): yield path + (k,), x for y in leaves(x, path + (k,)): yield y elif isinstance(v, list): for i, x in enumerate(v[:1]): yield path + (i,), x for y in leaves(x, path + (i,)): yield y for name, base in (("run", run), ("fault", fault), ("init", init), ("fault-run", frun), ("prior", prior), ("state-job", job), ("v2-t-toffoli", tof), ("v2-stabilizer", stab)): for part in ("request", "result"): for path, v in leaves(base[part], (part,)): # The receipt is the seal's; the format says what kind of job it is; and a # second version's reading may say more than rule 36 reads (section 11.5), # held by the cases above. if "receipt" in path or path == ("result", "format") or path[:2] == ("result", "energy"): continue where = "%s %s" % (name, "/".join(map(str, path))) if isinstance(v, (int, float)) and not isinstance(v, bool): case("kinds", "%s + 0.5" % where, base, at(path, v + 0.5), False) case("kinds", "%s at -1" % where, base, at(path, -1), False) case("kinds", "%s at 2^53" % where, base, at(path, 2 ** 53), False) if isinstance(v, str) and re.fullmatch("[0-9a-f]{64}", v): case("kinds", "%s in upper case" % where, base, at(path, v.upper()), False) case("kinds", "%s null" % where, base, at(path, None), False) return out def main(): ap = argparse.ArgumentParser() ap.add_argument("--reference", help="the wai-quantum binary") ap.add_argument("--second-only", action="store_true", help="the second verifier against the manifest alone") ap.add_argument("--corpus", default=CORPUS) ap.add_argument("--extra", action="append", default=[], help="a directory of receipts both must find valid") ap.add_argument("--plant", help="run the second verifier with this planted defect; succeed only if it is caught") ap.add_argument("--second", help="another second verifier's file in place of receipt_verify.py (a mutant of it)") ap.add_argument("--wasmq-only", action="store_true", help="only what holds a wasmQ job: its receipts, their changes, the rules and the labelled cases") ap.add_argument("--first", action="store_true", help="stop at the first stage that finds a disagreement") a = ap.parse_args() global SECOND if a.second: SECOND = os.path.abspath(a.second) if not a.second_only and not a.reference: ap.error("--reference is required, unless --second-only") ref = os.path.abspath(a.reference) if a.reference else None with open(os.path.join(a.corpus, "manifest.json"), encoding="utf-8") as f: whole = json.load(f) manifest, held_entries, trust_lists = whole["entries"], whole.get("held", []), whole.get("trust_lists", []) problems = [] listed = {e["file"] for e in manifest} present = {"jobs/" + n for n in os.listdir(os.path.join(a.corpus, "jobs")) if n.endswith(".json")} for f in sorted(present - listed): problems.append("%s is in the corpus and not in the manifest" % f) for f in sorted(listed - present): problems.append("%s is in the manifest and not in the corpus" % f) # The corpus: both verifiers and the manifest, receipt by receipt. entries = [e for e in manifest if e["file"] in present and (not a.wasmq_only or "wasmq" in e["file"])] files = [os.path.join(a.corpus, e["file"]) for e in entries] r2 = run_second_files(files, a.plant) r1 = r2 if a.second_only else run_reference_files(ref, files) agree = 0 for e, x, y in zip(entries, r1, r2): if not a.second_only: same_rules(e["file"], x, y, problems) want = tuple(sorted(e["reasons"])) if said(x) != said(y) or said(x)[0] != want: problems.append("%s: the manifest says %s; the reference %s; the second verifier %s" % (e["file"], list(want), list(said(x)), list(said(y)))) else: agree += 1 # A crafted wasmQ receipt that names one rule breaks that rule alone: one problem from the # reference, and that rule alone from the second verifier, which numbers its rules. alone = 0 for e, x, y in zip(entries, r1, r2): m = re.search(r"\(rule (\d+)\)$", e.get("what", "")) if not m or not e["file"].startswith("jobs/crafted-wasmq-"): continue alone += 1 for who, v in ((None if a.second_only else "the reference", x), ("the second verifier", y)): if who and rules_of(v) != {int(m.group(1))}: problems.append("%s breaks rule %s alone, but %s states %s" % (e["file"], m.group(1), who, (v.get("wasmq") or {}).get("problems"))) print("corpus: %d crafted wasmQ receipts each break the one rule they name, and no other" % alone) valid = sum(1 for e in entries if not e["reasons"]) if not a.wasmq_only: problems += held_stage(None if a.second_only else ref, a.plant, a.corpus, held_entries) problems += trust_stage(None if a.second_only else ref, a.plant, a.corpus, trust_lists) print("corpus: %d receipts (%d valid, %d not), %d agree %s" % (len(entries), valid, len(entries) - valid, agree, "with the manifest (second verifier only)" if a.second_only else "three ways (manifest, reference, second)")) if a.second_only: g = generator() problems += rules_stage(None, a.plant, (g.seal, g.public_key(g.DEMO).hex())) problems += labelled_stage(None, a.plant) return finish(a, problems) if a.first and problems: return finish(a, problems) # The rules and the labelled cases first: each is short, and each has its verdict written. g = generator() seal = (g.seal, g.public_key(g.DEMO).hex()) problems += rules_stage(ref, a.plant, seal) if a.first and problems: return finish(a, problems) problems += labelled_stage(ref, a.plant) if a.first and problems: return finish(a, problems) # Receipts a person holds: both must find them valid. extra = [] for d in a.extra: extra += [os.path.join(d, n) for n in sorted(os.listdir(d)) if n.endswith(".json")] if extra: x1, x2 = run_reference_files(ref, extra), run_second_files(extra, a.plant) for f, x, y in zip(extra, x1, x2): if said(x) != said(y) or said(x)[0]: problems.append("%s (extra): the reference %s; the second verifier %s" % (os.path.basename(f), list(said(x)), list(said(y)))) print("extra: %d receipts held outside the corpus, %d valid to both" % (len(extra), sum(1 for x, y in zip(x1, x2) if not said(x)[0] and said(x) == said(y)))) # Every valid receipt, one member changed at a time. lines, meta = [], [] for e in entries: if e["reasons"]: continue try: with open(os.path.join(a.corpus, e["file"]), encoding="utf-8") as f: body = json.load(f) except ValueError: continue if not isinstance(body, dict): continue for what, b, expected in mutations(body) + edges(body, seal): lines.append(compact(b)) meta.append((e["file"], what, expected)) with tempfile.TemporaryDirectory() as tmp: path = os.path.join(tmp, "changed.jsonl") with open(path, "w", encoding="utf-8") as f: f.write("\n".join(lines) + "\n") m1 = run_lines([ref, "verify", "--lines"], path, len(lines)) m2 = run_lines([sys.executable, "-I", SECOND] + (["--plant", a.plant] if a.plant else []) + ["--lines"], path, len(lines)) agree, caught, held, compared = 0, 0, 0, 0 reasons = Counter() for (fname, what, expected), x, y in zip(meta, m1, m2): sx, sy = said(x), said(y) same_rules("%s, %s" % (fname, what), x, y, problems) if sx != sy: problems.append("%s, %s: the reference %s; the second verifier %s" % (fname, what, list(sx), list(sy))) continue agree += 1 reasons.update(sx[0]) if expected == "invalid" and not sx[0]: problems.append("%s, %s: a change inside the request, the result or the receipt was found valid by both" % (fname, what)) elif expected == "unchanged" and sx[0]: problems.append("%s, %s: a change that is not sealed changed the verdict: %s" % (fname, what, list(sx[0]))) elif expected == "invalid": caught += 1 elif expected == "agree": compared += 1 else: held += 1 print("changed: %d receipts from %d valid ones; %d agree (%d refused, as every change inside the seal must be; %d valid, as every change outside it must be; %d at the edges of a number, judged only by the other verifier)" % (len(lines), valid, agree, caught, held, compared)) print("reasons given to the changed receipts: " + ", ".join("%s %d" % kv for kv in sorted(reasons.items()))) return finish(a, problems) def rules_stage(ref, plant, seal): """Each verifier given every case of rule_cases: each must give the reasons written for it (the second alone with --second-only).""" cases = rule_cases(CORPUS, seal[0]) with tempfile.TemporaryDirectory() as tmp: path = os.path.join(tmp, "rules.jsonl") with open(path, "w", encoding="utf-8") as f: f.write("\n".join(b if isinstance(b, str) else compact(b) for _, b, _ in cases) + "\n") second = run_lines([sys.executable, "-I", SECOND] + (["--plant", plant] if plant else []) + ["--lines"], path, len(cases)) first = run_lines([ref, "verify", "--lines"], path, len(cases)) if ref else second problems = [] for (what, _, want), x, y in zip(cases, first, second): if ref: same_rules(what, x, y, problems) rule = re.match(r"rule (\d+), ", what) for who, v in (("the reference", x), ("the second verifier", y)): if tuple(sorted(v.get("reasons", []))) != tuple(want): problems.append("%s: written %s; %s %s" % (what, want, who, sorted(v.get("reasons", [])))) elif want and rule and rules_of(v) is not None and int(rule.group(1)) not in rules_of(v): problems.append("%s: %s finds it breaks rules %s, not the rule it is written for" % (what, who, sorted(rules_of(v)))) rules = len({w.split(",")[0] for w, _, _ in cases if re.match(r"rule \d+,", w)}) kinds = sum(1 for w, _, _ in cases if w.startswith("rule kinds,")) print("rules: %d cases, %d at the bounds of %d rules of a wasmQ job's form and %d of members of another kind, sealed again; %d as written, the same rules broken by both" % (len(cases), len(cases) - kinds, rules, kinds, len(cases) - len({p.split(":")[0] for p in problems}))) return problems def labelled_stage(ref, plant): """The second verifier's own hand-labelled wasmQ cases (`receipt_verify.py --wasmq-cases`), each as its exact text, given to both verifiers: each must give the reasons its author wrote, so that one labelled corpus binds both. The labels come from receipt_verify.py as written, whichever second verifier is under test.""" with tempfile.TemporaryDirectory() as tmp: out = os.path.join(tmp, "cases.jsonl") p = subprocess.run([sys.executable, "-I", ORIGINAL_SECOND, "--wasmq-cases", out], capture_output=True, text=True) if p.returncode != 0: raise SystemExit("receipt_verify.py --wasmq-cases failed: %s" % p.stderr.strip()[:400]) with open(out, encoding="utf-8") as f: cases = [json.loads(line) for line in f if line.strip()] files = [] for i, c in enumerate(cases): path = os.path.join(tmp, "case-%04d.json" % i) with open(path, "wb") as f: f.write(base64.b64decode(c["raw"])) files.append(path) second = run_second_files(files, plant) first = run_reference_files(ref, files) if ref else second problems = [] for c, x, y in zip(cases, first, second): if ref: same_rules("labelled %s" % c["name"], x, y, problems) want = sorted(c["reasons"]) for who, v in (("the reference", x), ("the second verifier", y)): if sorted(v.get("reasons", [])) != want: problems.append("labelled %s: written %s; %s %s" % (c["name"], want, who, sorted(v.get("reasons", [])))) print("labelled: %d of the second verifier's hand-labelled wasmQ cases, given to both; %d as written" % (len(cases), len(cases) - len({p.split(":")[0] for p in problems}))) return problems def finish(a, problems): if a.plant: if problems: print("plant %s: caught, by %d disagreements; the first: %s" % (a.plant, len(problems), problems[0])) return 0 print("plant %s: NOT caught: the differential cannot tell this defect from the spec" % a.plant) return 1 for p in problems[:60]: print("DISAGREE " + p) if problems: print("%d disagreements" % len(problems)) return 1 print("receipt_differential: the two verifiers and the manifest agree on every receipt") return 0 if __name__ == "__main__": sys.exit(main())