2778ddd525
Re-landed from PR #668 (branch wai/quantum-planner-contract, merged with main
495651ddd at 37350335b) as one commit on main, under the land-it model. Five
review rounds; round 5's findings (two high: workers that died as PID 1) were
fixed on the branch, and its CI reds were traced and fixed before landing.
A job may carry a contract (deadline, energy ceiling, cost, accuracy); the
planner chooses a route that meets it or refuses with every route's reason,
and its reasoning is sealed in the receipt. Under #676's reading child the
contract job is planned in the child from the per-method timings the parent
sends, bounded as a job naming its chosen method plus its reasoning, kept
across a restart. Both verifiers (Rust and receipt_verify.py) check the
planner statement beside wasmQ's; the receipts corpus is regenerated with
both kinds (268 crafted receipts, 14 plants caught). The views page carries
its engine raw-deflated and stays under its 1 MiB limit (669,484 bytes).
Passed before the push (Framework, linux; M3, macOS): every repository
check, receipts conformance, breaking, corpora, catalogue, the qpu clients,
energy (wai-rs, wai-quantum full, serve), the CLI tests and clippy, writer,
smoke, cross-simulator corpus, job receipts, wasmQ tests and vectors, the
engine with and without receipts under -D warnings, the docs pages, and the
service suite with clippy.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
1001 lines
63 KiB
Python
1001 lines
63 KiB
Python
#!/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 run_reference_files(ref, files):
|
|
def compute():
|
|
out = []
|
|
for f in files:
|
|
p = subprocess.run([ref, "verify", "--json", f], 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), compute)
|
|
|
|
|
|
def run_second_files(files, plant):
|
|
cmd = [sys.executable, "-I", SECOND] + (["--plant", plant] if plant else [])
|
|
|
|
def compute():
|
|
p = subprocess.run(cmd + files, 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]))
|
|
return verdicts(p.stdout, len(files))
|
|
return cached(cmd, _contents(files), compute)
|
|
|
|
|
|
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, and 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)."""
|
|
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")))
|
|
|
|
|
|
# ----------------------------------------------------------------- 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):
|
|
return v * 2 + 1
|
|
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"))
|
|
# A member of the receipt beyond its five is ignored (section 8.2).
|
|
ignored = len(path) >= 3 and path[:2] == ("result", "receipt") and path[2] not in ("alg", "canon", "key", "digest", "signature")
|
|
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)
|
|
|
|
# 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)):
|
|
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.
|
|
if "receipt" in path or path == ("result", "format"):
|
|
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:
|
|
manifest = json.load(f)["entries"]
|
|
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"])
|
|
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())
|