"""The figures the crystallized Moser papers add up, count or quote, which no single gate log holds. python code/paper_figures.py (from moser-verification-xuanheng/) Writes data/paper-figures.json. It runs nothing of the programme and computes no mathematics of its own; it reads what the sixteen runs already wrote and the inventory. Its entries are of three kinds and never mixed: sums a sum or a difference of gate-log fields; each entry names the fields it reads. counts counts over the drill records of the gate logs — for the whole tree, and for the runs each paper draws on — and over the inventory (crystal/data/inventory.json, by SHA-256). quoted_from_programme figures a paper cites from the programme's own documents, as the document writes them, with the package, the member, its SHA-256 and the line. Nothing here recomputed them; the shared checker counts them apart from recomputed evidence. Re-run, the file is byte-identical. """ import hashlib import json import sys from collections import Counter from pathlib import Path TREE = Path(__file__).resolve().parents[1] LOGS = TREE / "data" / "gate-logs" OUT = TREE / "data" / "paper-figures.json" INVENTORY = TREE / "crystal" / "data" / "inventory.json" sys.path.insert(0, str(TREE / "code")) import corpus # noqa: E402 # the runs each paper draws on (census/moser in the crystallization repository) PAPERS = { "M01": ["RUN-002", "RUN-003", "RUN-004", "RUN-005", "RUN-006", "RUN-007"], "M02": ["RUN-010", "RUN-011", "RUN-012", "RUN-013"], "M03": ["RUN-008", "RUN-009", "RUN-014", "RUN-015", "RUN-016"], } DRILL = ["plants", "plants_caught_by_named_checks", "controls", "controls_undisturbed", "must_stay_green_assertions", "must_stay_green_held"] def log_of(run): (path,) = LOGS.glob(f"run{run[-3:]}-*.json") return json.loads(path.read_text(encoding="utf-8")) def drill(runs): t = Counter() for run in runs: lg = log_of(run) for k in DRILL: t[k] += lg["drill"][k] t["checks"] += len(lg["checks"]) return {"runs": runs, **{k: t[k] for k in DRILL + ["checks"]}, "rule": "sums over the runs' drill blocks; checks is the total of the checks each run lists"} def counts(): raw = INVENTORY.read_bytes() records = json.loads(raw.decode("utf-8")) every = [f"RUN-{n:03d}" for n in range(1, 17)] out = {"drill_whole_tree": drill(every)} for paper, runs in PAPERS.items(): out[f"drill_{paper}"] = drill(runs) inv = {"sha256": hashlib.sha256(raw).hexdigest(), "runs": len(records), "items": sum(len(r["items"]) for r in records), "correction_rows": sum(len(r["corrections"]) for r in records), "by_strength": dict(sorted(Counter(i["strength"] for r in records for i in r["items"]).items()))} for paper, runs in PAPERS.items(): rs = [r for r in records if r["run"] in runs] inv[paper] = {"items": sum(len(r["items"]) for r in rs), "correction_rows": sum(len(r["corrections"]) for r in rs), "by_strength": dict(sorted(Counter(i["strength"] for r in rs for i in r["items"]).items()))} out["inventory"] = inv return out def quote(round_id, member, needle): """A figure as the programme's document writes it: the line it stands on, by package member and line number.""" data = corpus.source_bytes(round_id) for m, b in corpus.members(round_id, data, keep=lambda m: m.path == member): if b is None: continue lines = b.decode("utf-8").split("\n") hits = [i for i, ln in enumerate(lines, 1) if needle in ln] assert len(hits) >= 1, (round_id, member, needle) return {"value": needle, "package": corpus.SOURCES[round_id][0], "member": member, "member_sha256": m.sha256, "line": hits[0], "text": lines[hits[0] - 1].strip()} raise KeyError((round_id, member)) def sums(): s = {} f = log_of("RUN-004")["findings"] five = max(r["value"] for r in f["five_link_search"]["runs"]) seven = max(r["value"] for r in f["seven_link_search"]["runs"]) s["seven_link_search_above_five_link_search"] = { "value": seven - five, "rule": "difference of the best values of the two searches", "reads": ["run004 findings.five_link_search.runs[].value", "run004 findings.seven_link_search.runs[].value"]} f2 = log_of("RUN-002")["findings"] c = f2["candidate"] s["round01_candidate_recorded_above_scanned_minimum"] = { "value": c["recorded"] - c["scanned_min_over_rotations"], "rule": "difference", "reads": ["run002 findings.candidate.recorded", "run002 findings.candidate.scanned_min_over_rotations"]} above = sorted(((r["record"] - r["program_scanned_min"], r["curve"], r["container"]) for r in f2["defined_curves"]), reverse=True) s["round01_records_above_scanned_minimum"] = { "records": len(above), "above": sum(d > 0 for d, _, _ in above), "largest_nine": [{"curve": cv, "container": ct, "above_by": d} for d, cv, ct in above[:9]], "next_two": [{"curve": cv, "container": ct, "above_by": d} for d, cv, ct in above[9:11]], "rule": "record minus the program's scanned minimum for every rebuildable record, sorted, largest first", "reads": ["run002 findings.defined_curves[].record", "run002 findings.defined_curves[].program_scanned_min"]} return s def manifest_counts(): m = json.loads((TREE / "data" / "SOURCE_MANIFEST.v1.json").read_text(encoding="utf-8")) return {"packages": len(m["packages"]), "members": len(m["leaves"]), "rule": "counts over data/SOURCE_MANIFEST.v1.json"} def environment(): """The interpreter and libraries the runs and this script were run under, major.minor.""" import platform from importlib import metadata mm = lambda v: ".".join(v.split(".")[:2]) # noqa: E731 return {"python": mm(platform.python_version()), **{p: mm(metadata.version(p)) for p in ("mpmath", "numpy", "scipy", "sympy")}} def quoted(): q = {} for key, rid, member, needle in [ ("round01_grid_directions", "round-v0.1", "Moser_Skew_Lab_v0.1/reports/ROUND_01_REPORT.md", "192 個支撐方向"), ("round02_grid_candidate_exact", "round-v0.2.2", "Moser_Skew_Lab_v0.2/reports/ROUND_02_EXACT_ADDENDUM.md", "1.000837369637"), ("round02_reoptimized_mirror", "round-v0.2.2", "Moser_Skew_Lab_v0.2/reports/ROUND_02_CHIRALITY_CORRECTION.md", "0.952938974740"), ("round03_five_over_three_gain", "round-v0.3", "Moser_Skew_Lab_v0.3/README.md", "1.799969565222e-04"), ("round04_tracked_level", "round-v0.4.1", "Moser_Skew_Lab_v0.4/README.md", "2.734812376559e-12"), ("round05_sigma_min", "round-v0.5", "Moser_Skew_Lab_v0.5/reports/ROUND_05_REPORT.md", "3.607219048175e-02"), ("round05_condition_number", "round-v0.5", "Moser_Skew_Lab_v0.5/reports/ROUND_05_REPORT.md", "162.781733366"), ("round06_gap_outer_length", "round-v0.6.1", "Moser_Skew_Lab_v0.6/reports/ROUND_06_REPORT.md", "1.686411486e-03"), ("round06_gap_inner_length", "round-v0.6.1", "Moser_Skew_Lab_v0.6/reports/ROUND_06_REPORT.md", "2.448355423e-03"), ("round06_gap_outer_angle", "round-v0.6.1", "Moser_Skew_Lab_v0.6/reports/ROUND_06_REPORT.md", "1.328757456e-02"), ("round06_gap_inner_angle", "round-v0.6.1", "Moser_Skew_Lab_v0.6/reports/ROUND_06_REPORT.md", "5.369528921e-03"), ("round06_census_samples", "round-v0.6.1", "Moser_Skew_Lab_v0.6/reports/ROUND_06_REPORT.md", "1600 條一般五連桿"), ("round06_audit_samples", "round-v0.6.1", "Moser_Skew_Lab_v0.6/reports/ROUND_06_LOCAL_ESCAPE_AUDIT.md", "總計 6300 個"), ]: q[key] = quote(rid, member, needle) return q def main(): doc = {"about": "figures the Moser papers add up, count or quote; see code/paper_figures.py", "environment": environment(), "counts": {**counts(), "manifest": manifest_counts()}, "sums": sums(), "quoted_from_programme": quoted()} OUT.write_text(json.dumps(doc, ensure_ascii=False, indent=1) + "\n", encoding="utf-8", newline="\n") print("wrote", OUT.relative_to(TREE).as_posix()) if __name__ == "__main__": main()