"""RUN-016 - Round 13: the proof-state scheduler and the worker / merger protocol. Round 13 lets workers propose and only a single canonical merger write. A proposal is merged by semantic preconditions, not by its base checkpoint: an expansion only of a pending terminal seed, a certificate of a seed that is pending, or of an ancestor whose current descendants it then replaces (Certified Ancestor Contraction, Thm 10.1). Six primitives keep the frontier complete and prefix-free (Atomic Merge, Thm 20.1). The reference run races an EXPAND and a late CERTIFY of seed 01 from Round 12's V4. Here the two theorems are tested on random primitive sequences, the race is replayed by this tree's own merger and validator, the checkpoints are tied to Round 12's, and the files are read against the round's own rules. Checks A0 anchors the formulas and the race table occur in Round 13 as written W1 merge Thm 10.1, 20.1 on random primitive sequences: frontiers stay complete and prefix-free; theorem_ready implies every seed has a current accepted claim W2 race sec. 28-33: this tree's merger decides the three proposals and its validator the four states, against the files, the summary and the text W3 links the race starts from Round 12's V4 and certifies with V5's claim, byte for byte W4 semantics each race checkpoint's stored aggregate against its own ledger; the late certificate is the bytes V4 rejected (RUN-015), which RUN-013 replayed P1 package the jobs against the job schema; the merge journal against sec. 22; labels P2 package the package's self-description of its files matches the archive R1 registry Round 13's judgments reviewed, first-used statuses defined Usage: python code/run016_round13_autonomous_scheduler.py [--drill] [--blind CID] """ import argparse import copy import json import re import jsonschema import numpy as np import gate import registry from corpus import SOURCES, TREE, source_bytes, walk_sources from run014_round11_global_shards import complete, prefix_free from run015_round12_checkpoint_crystal import sha, validate PKG = "main.zip!/AMRAL_LUC_FC_Round_13_Package_v0.1.zip!/" REF = PKG + "AMRAL_LUC_FC_Round_13_reference_scheduler/" DOC = PKG + "AMRAL_Lebesgue_Finite_Closure_Round_13_Autonomous_Scheduler_v0.1.md" PROTOCOL = PKG + "AMRAL_LUC_FC_Round_13_WORKER_MERGER_PROTOCOL_v0.1.md" CRYSTAL = PKG + "AMRAL_LUC_FC_State_Crystal_Round_13_v0.1.md" VALIDATION = PKG + "AMRAL_LUC_FC_Round_13_VALIDATION.json" SCHEMA = PKG + "AMRAL_LUC_FC_Round_13_JOB_PROPOSAL_SCHEMA.json" MERGER = REF + "reference_scheduler_merger.py" JOBS = REF + "issued_jobs.json" SUMMARY = REF + "race_transition_summary.json" STATES = {"start": "r13_checkpoint_start.json", "after_expand": "r13_checkpoint_after_expand.json", "after_late_certify": "r13_checkpoint_after_late_certify.json", "after_obsolete_expand": "r13_checkpoint_after_obsolete_expand.json"} R12 = "main.zip!/AMRAL_LUC_FC_Round_12_Package_v0.1.zip!/AMRAL_LUC_FC_Round_12_reference_checkpoint/" COPIES = ["checkpoint_v4_rejected_B.json", "checkpoint_v5_corrected_B.json", "checkpoint_validator.py", "shards/shard-A.json", "shards/shard-B.json", "shards/shard-C.json"] RUN013 = TREE / "data" / "gate-logs" / "run013-round10-reference-dry-run.json" LOG = TREE / "data" / "gate-logs" / "run016-round13-autonomous-scheduler.json" MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json" ANCHORS = { "W1": [r"\mathcalP'=(\mathcalP\setminus\mathcalD_p)\cup\{p\}", r"\mathcalP'=(\mathcalP\setminus\{p\})\cup\mathcalD_p.", r"\min\text{canonicalclaimhash}."], "W2": [r"|start|`{00,01,10,11}`|false|", r"|expand|`{00,010,011,10,11}`|false|", r"|latecertify+contraction|`{00,01,10,11}`|true|", r"|lateexpand|unchanged|true|", r"\{010,011\}\to\{01\}."], "P1": [r"\texttt{OBSOLETE-COVERED-BY-CERTIFIED-ANCESTOR}.", r"\texttt{OBSOLETE-COVERED-BY-CERTIFICATE}."], } SEC22 = ["proposal_id", "base_checkpoint_id", "current_checkpoint_id_at_merge", "decision", "reason", "result_checkpoint_id"] # ---------------------------------------------------------------- this tree's merger def below(p, frontier): return [q for q in frontier if q.startswith(p)] def merge(state, proposal, contract): """sec. 7-12, 27: returns (decision, new frontier, claim to append or None). A seed is pending when no accepted claim covers it.""" frontier = state["frontier"] covered = {s for c in state["accepted"] for s in state["claims"][c]} p = proposal["seed_path"] if proposal["type"] == "EXPAND": if p in frontier and p not in covered: return "ACCEPT-EXPAND", sorted(set(frontier) - {p} | set(proposal["descendants"])), None if p in frontier or any(p.startswith(q) for q in frontier if q in covered): return "OBSOLETE-COVERED-BY-CERTIFICATE", frontier, None return "OBSOLETE-EXPANSION", frontier, None if p in frontier and p not in covered: return "ACCEPT-CERTIFY", frontier, proposal["claim"] D = below(p, frontier) if D and p not in frontier and complete({q[len(p):] for q in D}): return "ACCEPT-CERTIFY-ANCESTOR-CONTRACTION", contract(frontier, p, D), proposal["claim"] return "AUXILIARY", frontier, proposal["claim"] def contract_frontier(frontier, p, D): return sorted(set(frontier) - set(D) | {p}) # ---------------------------------------------------------------- checks def w1_merge(w): """random sequences of sec. 20's six primitives on a toy proof state: frontier paths, claims on paths, a current fingerprint""" out, rng = [], np.random.default_rng(131) for run in range(60): P, claims, fp = {""}, {}, 0 # claims: id -> (path, status, fingerprint) for step in range(80): accepted = {cid for cid, (q, st, f) in claims.items() if st == "OK" and f == fp and q in P} covered = {claims[c][0] for c in accepted} pending = sorted(P - covered) move = int(rng.integers(0, 6)) if move == 0 and pending: # 1. pending seed -> verified claim claims[f"c{run}.{step}"] = (pending[int(rng.integers(0, len(pending)))], "OK", fp) elif move == 1 and pending: # 2. pending seed -> complete descendant frontier p = pending[int(rng.integers(0, len(pending)))] if len(p) < 10: P = (P - {p}) | {p + "0", p + "1"} elif move == 2: # 3. descendants -> a certified ancestor ancestors = sorted({q[:i] for q in P for i in range(len(q))} - P) if ancestors: p = ancestors[int(rng.integers(0, len(ancestors)))] P = set(w["contract"](sorted(P), p, below(p, P))) claims[f"c{run}.{step}"] = (p, "OK", fp) elif move == 3 and accepted: # 4. active claim rejected -> pending cid = sorted(accepted)[int(rng.integers(0, len(accepted)))] claims[cid] = (claims[cid][0], "REJECTED", claims[cid][2]) elif move == 4 and covered: # 5. an auxiliary claim claims[f"c{run}.{step}"] = (sorted(covered)[0], "OK", fp) elif move == 5 and rng.uniform() < 0.1: # 6. a proof-critical dependency changes fp += 1 if not (prefix_free(P) and complete(P)): out.append(f"sequence {run}, step {step}: the frontier is no longer complete and prefix-free") return out accepted = {cid for cid, (q, st, f) in claims.items() if st == "OK" and f == fp and q in P} ready = P <= {claims[c][0] for c in accepted} if ready and not all(any(claims[c][0] == q and claims[c][2] == fp for c in accepted) for q in P): out.append(f"sequence {run}, step {step}: ready without a current claim for every seed") return out return out def w2_race(w): out = [] cps = w["checkpoints"] start = cps["start"]["payload"] late = next(c for c in w["r12_v5"]["payload"]["claim_ledger"] if c["claim_id"] == "claim-shard-B-v2-corrected") proposals = [("proposal-expand-01-v1", {"type": "EXPAND", "seed_path": "01", "descendants": ["010", "011"]}), ("proposal-certify-01-late-v1", {"type": "CERTIFY", "seed_path": "01", "claim": late}), ("proposal-expand-01-too-late", {"type": "EXPAND", "seed_path": "01", "descendants": ["010", "011"]})] payload = copy.deepcopy(start) decisions, frontiers, ready = [], [sorted(payload["frontier"]["seed_paths"])], [validate(payload)["theorem_ready"]] for pid, prop in proposals: r = validate(payload) state = {"frontier": payload["frontier"]["seed_paths"], "accepted": r["accepted_claim_ids"], "claims": {c["claim_id"]: c["seed_paths"] for c in payload["claim_ledger"]}} decision, frontier, claim = merge(state, prop, w["contract"]) decisions.append((pid, decision)) payload["frontier"]["seed_paths"] = frontier if claim is not None: payload["claim_ledger"].append(claim) payload["audit_ledger"] += [a for a in w["r12_v5"]["payload"]["audit_ledger"] if a["claim_id"] == claim["claim_id"]] frontiers.append(sorted(frontier)) ready.append(validate(payload)["theorem_ready"]) recorded = [(e["proposal_id"], e["decision"]) for e in w["summary"]["orchestration_ledger"]] if decisions != recorded: out.append(f"decisions {decisions}, recorded {recorded}") names = list(STATES) for i, name in enumerate(names): cp = cps[name]["payload"] mine = validate(cp) if sorted(cp["frontier"]["seed_paths"]) != frontiers[i]: out.append(f"{name}: frontier {cp['frontier']['seed_paths']}, rebuilt {frontiers[i]}") s = w["summary"][name] if mine["theorem_ready"] != ready[i] or s["theorem_ready"] != ready[i] or sorted(s["frontier"]) != frontiers[i]: out.append(f"{name}: theorem_ready rebuilt {ready[i]}, validator {mine['theorem_ready']}, summary {s['theorem_ready']}") if w["text_table"][i] != ready[i]: out.append(f"{name}: the text's table has {w['text_table'][i]}") w["w2"] = {"decisions": decisions, "frontiers": frontiers, "theorem_ready": ready} return out def w3_links(w): out = [] for f in COPIES: if w["copies"][f] != w["r12"][f]: out.append(f"{f}: Round 13's copy differs from Round 12's") v4 = json.loads(w["r12"]["checkpoint_v4_rejected_B.json"])["payload"] start = w["checkpoints"]["start"]["payload"] if start["parent_checkpoint_id"] != v4["checkpoint_id"] or start["claim_ledger"] != v4["claim_ledger"] \ or start["audit_ledger"] != v4["audit_ledger"] or start["dependency_bundle"] != v4["dependency_bundle"]: out.append("the race does not start from Round 12's V4") late = w["checkpoints"]["after_late_certify"]["payload"]["claim_ledger"][-1] v5 = json.loads(w["r12"]["checkpoint_v5_corrected_B.json"])["payload"] if late != next(c for c in v5["claim_ledger"] if c["claim_id"] == late["claim_id"]): out.append("the late certificate is not Round 12's V5 claim") for name, cp in w["checkpoints"].items(): if sha(cp["payload"]) != cp["payload_sha256"]: out.append(f"{name}: its payload digest does not re-derive") return out def w4_semantics(w): out, wrong = [], [] for name, cp in w["checkpoints"].items(): p, r = cp["payload"], validate(cp["payload"]) agg = p["aggregate"] if agg["theorem_ready"] != r["theorem_ready"] or agg.get("active_claim_ids") != r["accepted_claim_ids"] \ or agg["pending_seed_paths"] != r["pending_seed_paths"]: wrong.append(name) p = w["checkpoints"]["after_late_certify"]["payload"] late = p["claim_ledger"][-1] failed = {a["claim_id"] for a in p["audit_ledger"] if a["result"] == "FAIL"} readmitted = any(c["certificate_payload_sha256"] == late["certificate_payload_sha256"] and c["status"] == "REJECTED" and c["claim_id"] in failed for c in p["claim_ledger"]) replayed = w["run013"]["w3"]["trees"]["01"]["exact_failures"] == 0 # sec. 15-16: a second valid certificate of seed 01 is legal and one of the two becomes primary; # under the Round 12 validator's rule (mirrored in RUN-015) the seed is covered twice instead dup = copy.deepcopy(p) second = {**copy.deepcopy(late), "claim_id": "claim-shard-B-v3-duplicate", "supersedes": None} dup["claim_ledger"].append(second) dup["audit_ledger"].append({"audit_id": "audit-duplicate", "claim_id": second["claim_id"], "audit_level": "A1-CANONICAL-INDEPENDENT-REPLAY", "result": "PASS"}) blocked = not validate(dup)["theorem_ready"] if sorted(wrong) != sorted(w["stored_aggregate_wrong"]) or readmitted != w["late_certificate_readmitted"] \ or blocked != w["duplicate_blocks_readiness"]: out.append(f"stored aggregates wrong in {wrong}; late certificate re-admitted {readmitted}; " f"a legal duplicate blocks readiness {blocked}") w["w4"] = {"stored_aggregate_contradicts_ledger": wrong, "late_certificate_is_rejected_bytes": readmitted, "those_bytes_replayed_clean_in_RUN_013": replayed, "legal_duplicate_blocks_readiness": blocked} return out def p1_package(w): out, schema = [], w["schema"] job_schema = {"$schema": schema["$schema"], "$defs": schema["$defs"], "$ref": "#/$defs/job"} bad = [] for job in w["jobs"]: try: jsonschema.validate(job, job_schema) except jsonschema.ValidationError: bad.append(job["job_id"]) if bad: out.append(f"jobs failing the schema: {bad}") journal = w["summary"]["orchestration_ledger"] missing = sorted(f for f in SEC22 if not all(f in e for e in journal)) if missing != sorted(w["journal_missing"]): out.append(f"the merge journal leaves out {missing}, recorded {w['journal_missing']}") labels = sorted(l for l in ("OBSOLETE-COVERED-BY-CERTIFIED-ANCESTOR", "OBSOLETE-COVERED-BY-CERTIFICATE") if l in w["text"]) if (len(labels) == 2) != w["two_labels"]: out.append(f"the text's labels for a late expansion: {labels}") w["p1"] = {"journal_fields_missing": missing, "late_expansion_labels_in_text": labels} return out def p2_package(w): out, leaves = [], {row[0]: row for row in w["manifest"]["leaves"]} v = w["validation"] for rec, leaf_id, text in ((v["round13"], DOC, w["text"]), (v["state_crystal"], CRYSTAL, w["crystal"]), (v["worker_protocol"], PROTOCOL, w["protocol"])): _, size, digest = leaves[leaf_id] if rec["sha256"] != digest or rec["bytes"] != size: out.append(f"{rec['file']}: recorded sha256/bytes differ from the archive") n = text.count("$$") if rec["double_dollar_count"] != n or rec["double_dollar_even"] != (n % 2 == 0): out.append(f"{rec['file']}: recorded {rec['double_dollar_count']} $$, document has {n}") if rec["contains_unicode_escape_sequence"] != bool(re.search(r"\\u[0-9a-fA-F]{4}", text)): out.append(f"{rec['file']}: unicode-escape flag differs") if rec["contains_bracket_math_delimiter"] != bool(re.search(r"\\[\[\]()]", text)): out.append(f"{rec['file']}: bracket-delimiter flag differs") for key, leaf_id in (("job_proposal_schema_sha256", SCHEMA), ("scheduler_merger_sha256", MERGER)): if v[key] != leaves[leaf_id][2]: out.append(f"{key}: recorded digest differs from the archive") if v["race_summary"] != w["summary"]: out.append("VALIDATION's race summary differs from the reference's") return out # ---------------------------------------------------------------- registry (Round 13) TOKEN = "a worker-result category or proposal label of sec. 6, 8, 18 or 36, defined there; not a judgment" R13_DEFINITIONS = { "COUNTEREXAMPLE-CANDIDATE": ("in-line", "sec. 36: a worker's claimed counterexample; rejects a claim only once the " "merger has checked it"), "EXPANSION-CANDIDATE": ("in-line", "sec. 36: a proposed descendant frontier; changes the partition, claims nothing"), "OBSOLETE-EXPANSION": ("in-line", "sec. 8: an expansion of a seed that is no longer a pending terminal seed; not merged"), "PROOF-CANDIDATE": ("in-line", "sec. 36: a worker's proposed certificate; it still needs an A1 replay"), "SEARCH-CANDIDATE": ("in-line", "sec. 36: a numerical result only; closes no seed"), "STALE-PROPOSAL": ("in-line", "sec. 6: a proposal whose dependency fingerprint is not current; not merged"), } R13_REVIEWS = [ ("PROVED", "Ancestor contraction", "analytic", "PASS", "Thm 10.1: the seeds below p form a complete frontier below p, so replacing them by p keeps the Kraft sum; W1"), ("PROVED", "Atomic merge invariants", "analytic", "PASS", "Thm 20.1 by induction over the six primitives; W1. It holds of the computed state; the reference files' stored " "aggregates do not follow it (W4)"), ("PASS", "Reference async race", "computation", "PASS", "W2: this tree's merger and validator reproduce the three decisions and four states; the late certificate is " "Round 12's re-admitted claim (W4), whose bytes RUN-013 replayed"), ("CLOSED", "AUTONOMOUS SCHEDULER / MERGER ABI", "reading", "PARTIAL", "the merge rules are sound (W1, W2), but the reference merger writes the frontier and never the aggregate: all " "four race checkpoints store theorem_ready = true, two while seeds are pending, though the protocol gives the " "merger sole authority over exactly those fields; and the validator it uses turns sec. 15's legal duplicate " "certificate into a coverage conflict instead of choosing a primary (W4)"), ("COMPUTE-DEFERRED", "Global autonomous workers", "n/a", "n/a", ""), ("STILL DEFERRED", "GLOBAL 0.8350 HEAVY COMPUTE", "n/a", "n/a", "sec. 0's boxed summary; read from census v3 on (RUN-003)"), ("FORMALIZED", "Worker/merger authority split", "reading", "PASS", "sec. 1, 21, 37 and the protocol's sec. 1, 14"), ("FORMALIZED", "Lease non-semantic rule", "reading", "PASS", "sec. 4; the jobs mark leases non-semantic (P1)"), ("FORMALIZED", "Late expansion obsolescence", "reading", "PASS", "sec. 12, 32; W2"), ("REJECTED", "18. Audit proposal", "n/a", "n/a", TOKEN), ("TESTED", "CONCURRENT RACE SAFETY", "computation", "PASS", "one race, expand then late certify then late expand (W2); the others are C13-5"), ("COUNTEREXAMPLE-CANDIDATE", "", "n/a", "n/a", TOKEN), ("EXPANSION-CANDIDATE", "", "n/a", "n/a", TOKEN), ("OBSOLETE-EXPANSION", "", "n/a", "n/a", TOKEN), ("PROOF-CANDIDATE", "", "n/a", "n/a", TOKEN), ("SEARCH-CANDIDATE", "", "n/a", "n/a", TOKEN), ("STALE-PROPOSAL", "6. Proposal acceptance第一關", "n/a", "n/a", TOKEN), ] def r1_registry(w): return registry.completeness(w["registry"], "R13", w["definitions"], w["reviews"]) # ---------------------------------------------------------------- world, checks, drill CHECKS = {"A0": gate.anchors_check(ANCHORS), "W1": w1_merge, "W2": w2_race, "W3": w3_links, "W4": w4_semantics, "P1": p1_package, "P2": p2_package, "R1": r1_registry} DEPENDS = {"A0": {"text"}, "W1": {"contract"}, "W2": {"checkpoints", "r12_v5", "summary", "contract", "text_table"}, "W3": {"copies", "r12", "checkpoints"}, "W4": {"checkpoints", "run013", "stored_aggregate_wrong", "late_certificate_readmitted", "duplicate_blocks_readiness"}, "P1": {"schema", "jobs", "summary", "text", "journal_missing", "two_labels"}, "P2": {"validation", "text", "crystal", "protocol", "manifest", "summary"}, "R1": {"registry", "definitions", "reviews"}} CLAIMS = { "contract": contract_frontier, "text_table": [False, False, True, True], "stored_aggregate_wrong": ["start", "after_expand", "after_late_certify", "after_obsolete_expand"], "late_certificate_readmitted": True, "duplicate_blocks_readiness": True, "journal_missing": ["base_checkpoint_id", "current_checkpoint_id_at_merge", "reason", "result_checkpoint_id"], "two_labels": True, } def load_inputs(): blobs = {n: source_bytes(n) for n in SOURCES} want = {DOC, PROTOCOL, CRYSTAL, VALIDATION, SCHEMA, JOBS, SUMMARY, *(REF + f for f in STATES.values()), *(REF + f for f in COPIES), *(R12 + f for f in COPIES)} got = {leaf.id: d for leaf, d in walk_sources(blobs, keep=lambda l: l.id in want) if d is not None} return {"text": got[DOC].decode("utf-8"), "protocol": got[PROTOCOL].decode("utf-8"), "crystal": got[CRYSTAL].decode("utf-8"), "validation": json.loads(got[VALIDATION]), "schema": json.loads(got[SCHEMA]), "jobs": json.loads(got[JOBS]), "summary": json.loads(got[SUMMARY]), "checkpoints": {k: json.loads(got[REF + f]) for k, f in STATES.items()}, "copies": {f: got[REF + f] for f in COPIES}, "r12": {f: got[R12 + f] for f in COPIES}, "r12_v5": json.loads(got[R12 + "checkpoint_v5_corrected_B.json"]), "run013": json.loads(RUN013.read_text(encoding="utf-8")), "manifest": json.loads(MANIFEST.read_text(encoding="utf-8"))} def main(): ap = argparse.ArgumentParser() ap.add_argument("--drill", action="store_true") ap.add_argument("--blind", metavar="CID") args = ap.parse_args() inputs = load_inputs() def build(): return {**{k: (copy.deepcopy(v) if k not in ("copies", "r12") else dict(v)) for k, v in inputs.items()}, "registry": registry.load(), "definitions": dict(R13_DEFINITIONS), "reviews": list(R13_REVIEWS), **copy.deepcopy({k: v for k, v in CLAIMS.items() if k != "contract"}), "contract": CLAIMS["contract"]} if args.blind: CHECKS[args.blind] = lambda w: [] args.drill = True w = build() results = {c: fn(w) for c, fn in CHECKS.items()} for c, f in results.items(): print(f"{c} {'PASS' if not f else 'FAIL'}", *(f"\n {x}" for x in f[:6])) for key in ("w2", "w4", "p1"): print(key, w.get(key)) if not args.drill: return cps = inputs["checkpoints"] cases = [ ("K0-unmodified", "control", {}, set()), ("K1-doc-crlf", "control", {"text": inputs["text"].replace("\n", "\r\n")}, set()), ("K2-contraction-as-filter", "control", {"contract": lambda F, p, D: sorted([q for q in F if not q.startswith(p)] + [p])}, set()), ("K3-jobs-reordered", "control", {"jobs": list(reversed(inputs["jobs"]))}, set()), ("M1-doc-race-row", "mutation", {"text": inputs["text"].replace("| late expand | unchanged | true |", "| late expand | unchanged | false |")}, {"A0"}), ("M2-contraction-keeps-a-descendant", "mutation", {"contract": lambda F, p, D: sorted(set(F) - set(D[1:]) | {p})}, {"W1", "W2"}), ("M3-text-table", "mutation", {"text_table": [False, True, True, True]}, {"W2"}), ("M4-race-summary", "mutation", {"summary": {**inputs["summary"], "after_expand": { **inputs["summary"]["after_expand"], "theorem_ready": True}}}, {"W2", "P2"}), ("M5-start-not-v4", "mutation", {"checkpoints": {**cps, "start": {**cps["start"], "payload": { **cps["start"]["payload"], "parent_checkpoint_id": "AMRAL-LUC-FC-CP-R12-REFERENCE-v1"}}}}, {"W3"}), ("M6-aggregates-assumed-right", "mutation", {"stored_aggregate_wrong": []}, {"W4"}), ("M6b-duplicates-assumed-harmless", "mutation", {"duplicate_blocks_readiness": False}, {"W4"}), ("M7-journal-assumed-complete", "mutation", {"journal_missing": []}, {"P1"}), ("M8-merger-digest", "mutation", {"validation": {**inputs["validation"], "scheduler_merger_sha256": "0" * 64}}, {"P2"}), ("M9-review-dropped", "mutation", {"reviews": list(R13_REVIEWS[1:])}, {"R1"}), ] if args.blind: cases = [c for c in cases if args.blind in c[3]] d = gate.run_drill(build, CHECKS, DEPENDS, cases) summary = gate.summarize(d, CHECKS) print(gate.report_drill(summary)) for x in d: if not x["ok"]: print(" DRILL FAIL", x) if args.blind: n = sum(1 for x in d if args.blind in x["expected"] and args.blind not in x["tripped"]) print(f"blind {args.blind}: drill reported it blind in {n} cases (nothing written)") return log = {"run": "RUN-016", "subject": "Round 13: the proof-state scheduler and the worker / merger protocol", "document": DOC, "checks": {c: {"pass": not f, "failures": f} for c, f in results.items()}, **{k: w.get(k) for k in ("w2", "w4", "p1")}, "drill": summary} LOG.write_text(json.dumps(log, ensure_ascii=False, indent=1, default=float) + "\n", encoding="utf-8") if not results["R1"]: registry.record("R13", "RUN-016", R13_DEFINITIONS, R13_REVIEWS) print(f"registry: {len(R13_DEFINITIONS)} definitions, {len(R13_REVIEWS)} reviews recorded for R13") if __name__ == "__main__": main()