"""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 re 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"]} c10 = log_of("RUN-010")["findings"]["certificate"] s["round09_candidate_least_certified_width"] = { "value": float(c10["candidate_least_at_most"]) - float(c10["candidate_least_at_least"]), "rule": "difference of the certified upper and lower ends of the candidate's least", "reads": ["run010 findings.certificate.candidate_least_at_most", "run010 findings.certificate.candidate_least_at_least"]} s["round09_certified_margin_over_gain"] = { "value": float(c10["certified_margin_at_least"]) / float(log_of("RUN-010")["findings"]["difference_60_digits"]), "rule": "the certified margin over the event five-link divided by the high-precision gain s270 - s0", "reads": ["run010 findings.certificate.certified_margin_at_least", "run010 findings.difference_60_digits"]} from decimal import ROUND_CEILING, ROUND_FLOOR, Decimal def cut(v, sig, up): d = Decimal(v) q = Decimal(1).scaleb(d.adjusted() - sig + 1) return str(d.quantize(q, rounding=ROUND_CEILING if up else ROUND_FLOOR)).replace("E", "e") c14 = log_of("RUN-014")["findings"]["certificate"] c15 = log_of("RUN-015")["findings"]["certificate"] c16_ = log_of("RUN-016")["findings"]["certificate"] s["certified_gains_cut_to_five_digits"] = { "round13_over_round08_at_least": cut(c14["gain_over_round08_at_least"], 5, False), "round13_over_round08_at_most": cut(c14["gain_over_round08_at_most"], 5, True), "split_over_round13_at_least": cut(c15["gain_over_round13_at_least"], 5, False), "round15_over_round13_at_least": cut(c16_["gain_over_round13_at_least"], 5, False), "round15_over_round13_at_most": cut(c16_["gain_over_round13_at_most"], 5, True), "rule": "each certified gain cut toward its safe side at five significant digits: lower bounds down, upper " "bounds up", "reads": ["run014 findings.certificate.gain_over_round08_at_least / at_most", "run015 findings.certificate.gain_over_round13_at_least", "run016 findings.certificate.gain_over_round13_at_least / at_most"]} s["round15_candidate_over_split_curve_at_least"] = { "value": float(Decimal(c16_["target"]) - Decimal(c15["s270_at_most"])), "rule": "the candidate's certified lower bound less the split curve's certified upper bound (its s(3pi/2))", "reads": ["run016 findings.certificate.target", "run015 findings.certificate.s270_at_most"]} tb = log_of("RUN-009")["findings"]["best_true_branches_at_tracked_phases"] s["round08_true_branch_spread"] = { "value": max(tb) - min(tb), "rule": "largest less least of the four true branch values", "reads": ["run009 findings.best_true_branches_at_tracked_phases"]} c16 = log_of("RUN-016")["findings"]["certificate"] s["round15_candidate_certified_least_below_one"] = { "value": 1 - float(c16["target"]), "rule": "one less the certified lower bound of the eight-mode candidate's least", "reads": ["run016 findings.certificate.target"]} s["round15_candidate_certified_least_squared_below_one"] = { "value": 1 - float(c16["target"]) ** 2, "rule": "one less the square of that lower bound: the shortfall in area of the homothet it bounds", "reads": ["run016 findings.certificate.target"]} f11 = log_of("RUN-011")["findings"] s["round10_smooth_minimum_above_least"] = { "value": float(f11["interval_9_minimum"]["scale"]) - float(f11["certificate"]["s270_at_most"]), "rule": "the smooth minimum's scale less the certified upper end of s(3pi/2)", "reads": ["run011 findings.interval_9_minimum.scale", "run011 findings.certificate.s270_at_most"]} f12 = log_of("RUN-012")["findings"] s["switch_counts"] = { "round10_switches": len(f11["switches"]), "round11_neighbourhoods": len(f12["neighbourhoods"]), "round11_neighbourhoods_not_enclosing": len(f12["neighbourhoods_not_enclosing"]), "rule": "lengths of the logged lists", "reads": ["run011 findings.switches", "run012 findings.neighbourhoods", "run012 findings.neighbourhoods_not_enclosing"]} sw = [r for r in log_of("RUN-011")["findings"]["switches"] if r["interior"]] pairs = [] for r in sw: el, er = float(r["exact_left"]), float(r["exact_right"]) sl, sr = el + float(r["stated_left_minus_exact"]), er + float(r["stated_right_minus_exact"]) pairs.append((abs(el - er), abs(sl - sr), min(abs(float(r["stated_left_minus_exact"])), abs(float(r["stated_right_minus_exact"]))))) s["round10_wing_switches"] = { "switches": len(sw), "exact_one_sided_agree_to": max(p[0] for p in pairs), "stated_pair_apart_least": min(p[1] for p in pairs), "stated_pair_apart_largest": max(p[1] for p in pairs), "nearer_stated_value_off_by_at_most": max(p[2] for p in pairs), "rule": "over the switches where a wing's interior support meets a corner: the largest gap between the two exact " "one-sided derivatives, the least and largest gap between the two stated ones, and the largest distance " "of the nearer stated value from the exact derivative", "reads": ["run011 findings.switches[].exact_left / exact_right / stated_left_minus_exact / stated_right_minus_exact"]} return s def parameter(script, pattern, groups=1): """a figure a run's script fixes, read from its text as written, with the line it stands on""" (path,) = (TREE / "code").glob(script) for i, ln in enumerate(path.read_text(encoding="utf-8").split("\n"), 1): m = re.search(pattern, ln) if m: vals = [float(g) if "." in g else int(g) for g in m.groups()] return {"value": vals[0] if groups == 1 else vals, "script": f"code/{path.name}", "line": i, "text": ln.strip()} raise KeyError((script, pattern)) def parameters(): return { "run010_quadrature_digits": parameter("run010_*.py", r'def s270\(w, method="quad", dps=(\d+)\)'), "run011_stationary_scan_fractions": { **parameter("run011_*.py", r"mp\.mpf\(k\) / (\d+) for k in range\((\d+)\)\} \| \{mp\.mpf\(10\) \*\* -e for e in range\(1, (\d+)\)", 3), "geometric_points_each_end": 15, "points_in_all": 95, "rule": "the fractions k/64 for k = 0..64 (65 points), and 10^-e and 1 - 10^-e for e = 1..15 (range(1, 16)): " "15 points toward each end, 95 in all"}, "run011_one_sign_pieces": parameter("run011_*.py", r"def one_sign\(pts, a_, b_, sign, pieces=(\d+)\)"), "run008_limit_power": parameter("run008_*.py", r"for power in \(10\.0, 40\.0, (\d+)\.0\)"), "run009_candidate_ledger_grid": parameter("run009_*.py", r'"best", B\["parameters"\], B\["epsilon"\], B\["curvature_ledger"\], (\d+)\)'), "run014_certificate_target_offset": parameter("run014_*.py", r'mp\.mpf\("(1\.5e-10)"\)'), "run016_simpson_constant": parameter("run016_*.py", r"e_ = hi\(h \*\* 5 / (\d+) \*"), "run011_wing_alpha_checkpoint_u": parameter("run011_*.py", r'wing_angle_within_of_alpha_at_u_([\d.]+)"'), "run011_wing_beta_checkpoint_u": parameter("run011_*.py", r'wing_angle_within_of_beta_at_u_([\d.]+)"'), } 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 個"), ("round09_wing_length", "round-v0.9", "Moser_Skew_Lab_v0.9/reports/ROUND_09_REPORT.md", "w=0.3361057714712081"), ("round09_beta", "round-v0.9", "Moser_Skew_Lab_v0.9/reports/ROUND_09_REPORT.md", "\\beta=1.405382794839393"), ("round09_delta", "round-v0.9", "Moser_Skew_Lab_v0.9/reports/ROUND_09_REPORT.md", "\\delta=0.05204734906280986"), ("round09_centre", "round-v0.9", "Moser_Skew_Lab_v0.9/reports/ROUND_09_REPORT.md", "c=0.5801781668857768"), ("round09_event_l1", "round-v0.9", "Moser_Skew_Lab_v0.9/data/round09_summary.json", "\"l1\": \"0.19431311615307248\""), ("round09_event_l2", "round-v0.9", "Moser_Skew_Lab_v0.9/data/round09_summary.json", "\"l2\": \"0.1415930791195921\""), ("round09_event_beta", "round-v0.9", "Moser_Skew_Lab_v0.9/data/round09_summary.json", "\"beta\": \"1.4082767308631334\""), ("round09_event_delta", "round-v0.9", "Moser_Skew_Lab_v0.9/data/round09_summary.json", "\"delta\": \"0.04759059497406796\""), ("round12_balls_stated", "round-v0.12", "Moser_Skew_Lab_v0.12/reports/ROUND_12_IV_REPLAY_AUDIT.md", "解析邊界：19/19"), ("round13_stated_wing_length", "round-v0.13", "Moser_Skew_Lab_v0.13/data/round13_summary.json", "\"wing_length\": 0.33610428455831365"), ("round13_stated_beta", "round-v0.13", "Moser_Skew_Lab_v0.13/data/round13_summary.json", "\"beta_radians\": 1.4054077050409917"), ("round13_stated_delta", "round-v0.13", "Moser_Skew_Lab_v0.13/data/round13_summary.json", "\"delta_radians\": 0.05200850038234944"), ("round13_stated_centre", "round-v0.13", "Moser_Skew_Lab_v0.13/data/round13_summary.json", "\"transition_center\": 0.5801647299465723"), ("round13_stated_epsilon", "round-v0.13", "Moser_Skew_Lab_v0.13/data/round13_summary.json", "\"epsilon\": 0.03682334435307599"), *[(f"round15_parameter_{i}", "round-v0.15", "Moser_Skew_Lab_v0.15/data/final_candidate.json", v) for i, v in enumerate(["0.3361039495856486", "1.4054231629110312", "0.051972968077192816", "0.5802095527303379", "0.036983383487424734"])], *[(f"round15_coefficient_P{n}", "round-v0.15", "Moser_Skew_Lab_v0.15/data/final_candidate.json", f"_P{n}\": {v}") for n, v in enumerate(["0.000636097039547498", "0.01763543356796946", "0.004755842498620271", "-0.0752235430432821", "0.010666503454247333", "0.057547527232882936", "-0.019001897723771536", "-0.08299176521743751"], 1)], ("round15_multiplier", "round-v0.15", "Moser_Skew_Lab_v0.15/data/final_candidate.json", "\"multiplier\": 3.2275"), ("round07_best_segmented", "round-v0.7", "Moser_Skew_Lab_v0.7/README.md", "0.998839177646286"), ("round07_m2_search", "round-v0.7", "Moser_Skew_Lab_v0.7/reports/ROUND_07_SEARCH_AUDIT.md", "s=0.998530736905809."), ("round07_arc_deficit", "round-v0.7", "Moser_Skew_Lab_v0.7/README.md", "4.135963741603e-05."), ("round08_peak_curvature", "round-v0.8.3", "Moser_Skew_Lab_v0.8/reports/ROUND_08_REPORT.md", "2.092618923824"), ("round08_width", "round-v0.8.3", "Moser_Skew_Lab_v0.8/reports/ROUND_08_REPORT.md", "0.036579511462"), ("round08_audit_gain", "round-v0.8.3", "Moser_Skew_Lab_v0.8/reports/ROUND_08_FINITE_WIDTH_AUDIT.md", "s_*-s_0=1.045806040811e-05."), ("round13_jacobian_largest", "round-v0.13", "Moser_Skew_Lab_v0.13/data/round13_summary.json", "429267986.0"), ("round13_jacobian_smallest", "round-v0.13", "Moser_Skew_Lab_v0.13/data/round13_summary.json", "11.3975365"), ("round13_jacobian_condition", "round-v0.13", "Moser_Skew_Lab_v0.13/data/round13_summary.json", "\"jacobian_condition_number\": 37663225.38208147"), ("round14_profile_coefficient", "round-v0.14", "Moser_Skew_Lab_v0.14/reports/ROUND_14_REPORT.md", "-0.033794468"), ("round10_guard_samples", "round-v0.10", "Moser_Skew_Lab_v0.10/README.md", "257、1025、4097"), ("round10_switch_9", "round-v0.10", "Moser_Skew_Lab_v0.10/reports/ROUND_10_REPORT.md", "| 9 | 3.028226470697 |"), ("round10_switch_9_left_derivative", "round-v0.10", "Moser_Skew_Lab_v0.10/reports/ROUND_10_REPORT.md", "| cusp_minimum | -0.006893 |"), ("round11_derivative_boxes", "round-v0.11", "Moser_Skew_Lab_v0.11/README.md", "自適應導數盒：579"), ("round11_margin_switch_1", "round-v0.11", "Moser_Skew_Lab_v0.11/reports/ROUND_11_REPORT.md", "-2.691e-02"), ("round11_margin_switch_2", "round-v0.11", "Moser_Skew_Lab_v0.11/reports/ROUND_11_REPORT.md", "-2.297e-02"), ("round11_margin_switch_3", "round-v0.11", "Moser_Skew_Lab_v0.11/reports/ROUND_11_REPORT.md", "-7.712e-04"), ("round11_margin_switch_10", "round-v0.11", "Moser_Skew_Lab_v0.11/reports/ROUND_11_REPORT.md", "7.391e-02"), ("round12_s270_interval", "round-v0.12", "Moser_Skew_Lab_v0.12/reports/ROUND_12_REPORT.md", "s_{270}\\in[0.9989143389428913213797012975,0.9989143392263741131243407093]"), ("round12_difference_interval", "round-v0.12", "Moser_Skew_Lab_v0.12/reports/ROUND_12_REPORT.md", "[1.584622955726897820027e-9,1.692045182662177229601e-9]"), ("round12_margin_interval", "round-v0.12", "Moser_Skew_Lab_v0.12/reports/ROUND_12_REPORT.md", "[0.00001058181038264642457147,0.00001058209386543816921088]"), ]: 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(), "parameters": parameters(), "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()