"""RUN-034 - Round 31: the cross-backend replay and the first publication-candidate shard. Round 31 replays marker 70's whole shard on a second arithmetic backend - libMPFR 4.2.2 and GMP through a small ctypes wrapper - and promotes the shard to PUBLICATION-CANDIDATE-SHARD: the root by a directed bisection, marker 70's upper bound by Round 29's sector support in MPFR, and all 9278 lower leaves by Round 30's second implementation with its core enclosures in MPFR. It records a false negative of the first MPFR marker verifier (R31-MPFR-MARKER-001, U ~ 0.9201), and queues the atlas's 63 geometry-complete cells for the same arithmetic. Here the MPFR root is set between this tree's brackets and Round 28's; marker 70's exact polygon is rebuilt from this tree's integer support bounds with the package's normals and rounding - with every constraint, float-reduced, and with the adjacent pieces the correction removed; the MPFR ledger is set against Round 30's and this tree's certificate; the queue against this tree's atlas and its continuation. Checks A0 anchors the numbers and formulas below occur in Round 31 as written W1 root sec. 0, 4: the MPFR d* and t_n nested between this tree's brackets and Round 28's W2 marker sec. 5-6: marker 70's MPFR polygon rebuilt exactly; the correction's false negative W3 lower sec. 7-10: the MPFR ledger against Round 30's; this tree's certificate at its densities W4 queue sec. 15-17: the migration and residual queues against this tree's atlas (RUN-029, RUN-030) W5 lock sec. 12-13, 20: the lock against the scripts shipped; the correction ledger W6 code what the package ships, read after the rebuild and never run P1 package the replay files, the chunks, the ledger, the shard record, the queue and the crystal agree P2 package VALIDATION against the archive; its checks from the data R1 registry Round 31's judgments reviewed, first-used statuses defined Usage: python code/run034_round31_mpfr_replay.py [--drill] [--blind CID] """ import argparse import ast import collections import copy import hashlib import json import math import re from collections import deque from fractions import Fraction import gate import registry import run030_round27_interval_replay as r30 import run031_round28_exact_root as r31 import run032_round29_marker_upper as r32 import run033_round30_a1_replay as r33 from corpus import SOURCES, TREE, source_bytes, walk_sources from run030_round27_interval_replay import ONE, cos_sin, div_int from run031_round28_exact_root import PI PKG = "main.zip!/AMRAL_LUC_FC_Round_31_Package_v0.1.zip!/" DOC = PKG + "AMRAL_Lebesgue_Finite_Closure_Round_31_Cross_Backend_Publication_Candidate_v0.1.md" CRYSTAL = PKG + "AMRAL_LUC_FC_State_Crystal_Round_31_v0.1.md" ROOT_M = PKG + "AMRAL_LUC_FC_Round_31_MPFR_ROOT_REPLAY.json" MARKER_M = PKG + "AMRAL_LUC_FC_Round_31_MPFR_MARKER70_REPLAY.json" LOWER_M = PKG + "AMRAL_LUC_FC_Round_31_MPFR_LOWER_REPLAY.json" LOCK = PKG + "AMRAL_LUC_FC_Round_31_MPFR_BACKEND_LOCK.json" SHARD = PKG + "AMRAL_LUC_FC_Round_31_PUBLICATION_CANDIDATE_SHARD_70.json" QUEUE = PKG + "AMRAL_LUC_FC_Round_31_BULK_MIGRATION_QUEUE.json" CORRECTIONS = PKG + "AMRAL_LUC_FC_Round_31_CORRECTION_LEDGER.json" VALIDATION = PKG + "AMRAL_LUC_FC_Round_31_VALIDATION.json" REF = PKG + "AMRAL_LUC_FC_Round_31_reference/" LEDGER = REF + "mpfr_lower_ledger.json" LEDGER_COPY = REF + "chunks/mpfr_lower_ledger.json" CHUNKS = REF + "chunks/mpfr_lower_" LOG = TREE / "data" / "gate-logs" / "run034-round31-mpfr-replay.json" MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json" T, T_EXACT = 0.835, Fraction(167, 200) NORMAL_SCALE, SUPPORT_DEN = 10 ** 9, 10 ** 26 SCRIPTS = {"root": "r31_cross_root.py", "marker70": "r31_mpfr_marker70.py", "lower_chunk": "r31_mpfr_lower_chunk.py", "aggregate": "r31_aggregate.py"} # ---------------------------------------------------------------- marker 70, exactly, under the package's conventions def package_normals(N): """sec. 5's normals as the package forms them: round(10^9 (cos, sin)) at 2 pi k / N, reduced by their gcd, each once, in angle order""" out, seen = [], set() for i in range(N): th = 2 * math.pi * i / N a, b = int(round(NORMAL_SCALE * math.cos(th))), int(round(NORMAL_SCALE * math.sin(th))) if a == 0 and b == 0: continue g = math.gcd(abs(a), abs(b)) a, b = a // g, b // g if (a, b) not in seen: seen.add((a, b)) out.append((a, b)) out.sort(key=lambda p: math.atan2(p[1], p[0]) % (2 * math.pi)) return out def full_area(normals, H): """every constraint n.x <= h: the polar points n / h in angle order (the origin is inside), pruned where three consecutive ones do not turn left, until none is left to prune - exactly, no float step; the vertices are consecutive survivors' crossings""" pts = [(Fraction(a) / h, Fraction(b) / h) for (a, b), h in zip(normals, H)] n = len(pts) prev, nxt, alive = [(i - 1) % n for i in range(n)], [(i + 1) % n for i in range(n)], [True] * n todo, count = deque(range(n)), n while todo and count >= 3: j = todo.popleft() if not alive[j]: continue i, k = prev[j], nxt[j] (x1, y1), (x2, y2), (x3, y3) = pts[i], pts[j], pts[k] if (x2 - x1) * (y3 - y1) - (y2 - y1) * (x3 - x1) <= 0: alive[j] = False count -= 1 nxt[i], prev[k] = k, i todo.extend((i, k)) act = [i for i in range(n) if alive[i]] verts = [] for i, j in zip(act, act[1:] + act[:1]): (a1, b1), (a2, b2) = normals[i], normals[j] det = a1 * b2 - a2 * b1 verts.append((Fraction(H[i] * b2 - H[j] * b1, det), Fraction(a1 * H[j] - a2 * H[i], det))) return abs(sum(x1 * y2 - x2 * y1 for (x1, y1), (x2, y2) in zip(verts, verts[1:] + verts[:1]))) / 2, len(act) def adjacent(body, m): """the correction's first verifier: an arc counts wherever its normals' range, or a piece next to it, may hold the normal - within 3 pi / 2m of its axis, not pi / 2m""" corners, centres, _ = body return corners, centres, cos_sin(div_int((3 * PI[0], 3 * PI[1]), 2 * m))[0] def marker_polygons(marker): """marker 70's outer polygon at its density with the package's normals and its ceiling at 10^-26, the supports from this tree's integer-interval upper bounds (RUN-032): with every constraint (sec. 5), with the constraints a float hull proposes (Round 29's emitter), and with the adjacent arcs counted (sec. 6)""" q = [Fraction(x) for x in marker["q_rational"]] normals = package_normals(marker["final"]["density"]) b3, b5 = r32.base_bodies(q) out = {} for key, bodies in (("full", (b3, b5)), ("adjacent", (adjacent(b3, 3), adjacent(b5, 5)))): H26 = [-(-h * SUPPORT_DEN // ONE) for h in r32.half_planes(normals, bodies)] area, active = full_area(normals, [Fraction(h, SUPPORT_DEN) for h in H26]) out[key] = [float(area), active, area.numerator.bit_length(), area.denominator.bit_length()] if key == "full": red, act2 = r32.outer_area(normals, [Fraction(h * ONE, SUPPORT_DEN) for h in H26]) out["reduced"] = [float(red), act2, red.numerator.bit_length(), red.denominator.bit_length()] out["difference"] = float(red - area) return out # ---------------------------------------------------------------- the atlas the queue sorts (RUN-029's and RUN-030's caches) def atlas_facts(): """every cell's closing depth under the package's pad, and each cell still open at 40 with its unresolved volume at 34-40, from RUN-030's continuation over RUN-029's atlas and lifts (their caches)""" inp = r30.load_inputs() comp = r30.computed_all(inp) depths = r30.closing_depths({"computed": comp, "ledger": inp["ledger"]}) path = {c["cell"]: c["path"] for c in inp["ledger"]["cells"]} res = comp["residual"] return {"depths": {str(i): d for i, d in sorted(depths.items())}, "volumes": {str(i): {str(d): r30.vol(res[path[i]]["per"], d) for d in (34, 36, 38, 40)} for i in sorted(depths) if depths[i] is None}} def load_inputs(): blobs = {n: source_bytes(n) for n in SOURCES} want = {r33.MARKER70, r31.ROOTREC, r31.BULK, r30.PROGRESS, r33.LOCK, r33.LOWER_A1} got = {leaf.id: d for leaf, d in walk_sources(blobs, keep=lambda l: l.id.startswith(PKG) or l.id in want) if d is not None} sha = lambda b: hashlib.sha256(b).hexdigest() chunks = sorted((k[len(REF):], json.loads(v)) for k, v in got.items() if k.startswith(CHUNKS) and k != LEDGER_COPY) a1 = r33.load_inputs() return {"text": got[DOC].decode("utf-8"), "crystal": got[CRYSTAL].decode("utf-8"), "root_m": json.loads(got[ROOT_M]), "marker_m": json.loads(got[MARKER_M]), "lower_m": json.loads(got[LOWER_M]), "lock": json.loads(got[LOCK]), "shard": json.loads(got[SHARD]), "queue": json.loads(got[QUEUE]), "corrections": json.loads(got[CORRECTIONS]), "validation": json.loads(got[VALIDATION]), "ledger": json.loads(got[LEDGER]), "ledger_digests": [sha(got[LEDGER]), sha(got[LEDGER_COPY])], "chunks": [list(c) for c in chunks], "marker70": json.loads(got[r33.MARKER70]), "rootrec28": json.loads(got[r31.ROOTREC]), "bulk28": json.loads(got[r31.BULK]), "progress27": json.loads(got[r30.PROGRESS]), "lock30": json.loads(got[r33.LOCK]), "lower30": json.loads(got[r33.LOWER_A1]), "a1_rows": a1["rows"], "root_a1": a1["root_a1"], "marker_a1": a1["marker_a1"], "a1_key": a1["key_bytes"], "code30": a1["code"], "digests": {k[len(REF):]: sha(v) for k, v in got.items() if k.startswith(REF) and k.endswith(".py")}, "code": {k[len(REF):]: v.decode("utf-8") for k, v in got.items() if k.startswith(REF) and k.endswith(".py")}, "manifest": json.loads(MANIFEST.read_text(encoding="utf-8"))} ANCHORS = { "W1": [r"\text{与Round28directedintervals全部overlapPASS}.", r"2.97\times10^{-67}.", r"T_M=\frac{1673}{2000}", r"三者全部与Round28mpmath/libmpintervalsoverlap：", r"\text{exactFraction}\to\text{MPFRdirected}\to\text{exactdyadicFraction}.", r"任何transcendentalendpoint都以MPFRdyadicvalue完整取回。"], "W2": [r"U_{70}^{\rmMPFR}=0.8349075014501105<0.835.", r"9.24985499\times10^{-5}.", r"与Round29显示值一致。", r"唯一更换：", r"Reuleauxsupportsector的directedtranscendentalarithmetic全部由MPFR重新计算。", r"U\approx0.9201.", r"这不是falseproof，", r"只纳入directedsectorinterval真正可能active的pieces。", r"`R31-MPFR-MARKER-001`."], "W3": [r"MPFRreconstructedroot；", r"9278/9278\text{PASS}.", r"3.5423707501\times10^{-9}>0.", r"$$512:8174,$$$$1024:869,$$$$2048:163,$$$$4096:56,$$$$8192:12,$$$$16384:4.$$", r"与Round30A1implementation得到相同densityhistogram。", r"这是因为finitecandidatepolicy相同，", r"但coreenclosurearithmeticbackend不同。"], "W4": [r"\text{ARITHMETIC-MIGRATIONQUEUE}.", r"0\text{leavesrequireresplit}.", r"\Gamma_{B_7}(36)=51/77.", r"\Gamma_{B_7}(38)\ge57,", r"\Gamma_{B_7}(40)\ge63."], "W5": [r"\boxed{\text{libMPFR4.2.2+GMP}}", r"4e3ccf5b442fc91054b0153140fe62939009f98ca1367f45de62376d5b18d28c", r"d15e1585c6c267296459570c8ac217ca9123044bcd4e896d2f686b32333445d2", r"wrapper与replayscripts也全部content-hashed。", r"1.directedroot/pathtwo-backendreplay；", r"6.dependencyhashespinned。", r"\text{ALLLOCALCONDITIONSMET}.", r"firstldconfigparsinghelpergeneratedaninvalid`/`path"], "W6": [r"并以直接CABI/`ctypes`构造最小directed-roundingwrapper。"], "P1": [r"\texttt{PUBLICATION-CANDIDATE-SHARD}", r"\text{publication-candidateshard}\ne\text{globaltheorem}.", r"a_{\mathrm{Leb}}\ge0.835\text{NOTCERTIFIED}."], } CLAIMS = { # [this tree's brackets in the A1 replay's, the A1's in MPFR's, MPFR's in Round 28's]; MPFR's widths; d* a 2^-221 dyadic # bracket from 220 halvings "root_claim": {"nested": {"d": [True, True, True], "t3": [True, True, True], "t5": [True, True, True], "t7": [True, True, True]}, "widths": {"d": 2.967e-67, "t3": 4.241e-67, "t5": 3.307e-67, "t7": 3.13e-67}, "stated": True, "bisection": True, "flags": ["PASS", "MPFR-ctypes", "4.2.2", True, True, True]}, # [area, active constraints, numerator bits, denominator bits]: every constraint gives the MPFR (and A1) polygon, the float # reduction Round 29's, 3.3e-50 apart; the adjacent arcs counted give sec. 6's loose bound "marker_claim": {"record": [True, True, True, True], "every_constraint": [0.8349075014501105, 1317, 22754, 22755], "is_mpfr": True, "float_reduced": [0.8349075014501105, 1284, 21944, 21945], "is_round29": True, "difference": 3.257e-50, "adjacent": [0.9201592354, 1068]}, "lower_claim": {"leaves": 9278, "statuses": ["MPFR-PASS"], "same_as_round30": 9278, "mine_pass": 9278, "least": ["11010110100110101001110111", 2048, 3.5423707500925403e-09]}, # the 63 queued cells are this tree's atlas closed by 40, each at the next even depth (51 by 36, 57 by 38, 63 by 40); # the 14 residual cells those open at 40, their volumes and ratios this tree's continuation's; no marker margin to rank by "queue_claim": {"cells": True, "counts": [63, 63, 63], "depths": 63, "depth_counts": {"30": 7, "32": 12, "34": 19, "36": 13, "38": 6, "40": 6}, "first": [70, "PUBLICATION-CANDIDATE", [70]], "order_by_depth_then_cell": True, "marker_margins": ["None"], "residual": {"cells": True, "counts": [14, 14], "matched": 14, "last_depths": {"36": 5, "38": 8, "40": 1}, "at_40": [14, 0.6077]}}, "lock_claim": {"wrapper": True, "scripts": {"aggregate": True, "lower_chunk": True, "marker70": True, "root": True}, "unpinned": [], "libraries": [True, True, True], "status": ["LIBMPFR-4.2.2-CROSS-v0.1", "PINNED-CROSS-BACKEND"], "not_a_proof": True, "corrections": [["R31-MPFR-MARKER-001", "CORRECTED"], ["R31-BACKEND-LOCK-001", "CORRECTED"]], "safe_side": [True, "NONE"]}, "code_facts": { "r31_aggregate.py": {"lines": 26, "absolute_path": True, "opens": ["AMRAL_LUC_FC_Round_31_MPFR_LOWER_REPLAY.json", "AMRAL_LUC_FC_Round_31_reference"], "not_in_archive": [], "globs_itself": True, "later_file_wins": True}, "r31_cross_root.py": {"lines": 35, "absolute_path": True, "opens": ["AMRAL_LUC_FC_Round_28_ROOT_RECONSTRUCTION.json", "AMRAL_LUC_FC_Round_31_MPFR_ROOT_REPLAY.json"], "not_in_archive": [], "bits": 220, "master": True}, "r31_mpfr_backend.py": {"lines": 153, "absolute_path": False, "opens": [], "not_in_archive": [], "precision": 640, "mpfr_calls": ["mpfr_acos", "mpfr_add", "mpfr_atan2", "mpfr_clear", "mpfr_cmp", "mpfr_const_pi", "mpfr_cos", "mpfr_div", "mpfr_free_str", "mpfr_get_str", "mpfr_init2", "mpfr_mul", "mpfr_set_str", "mpfr_sin", "mpfr_sqrt", "mpfr_sub"], "inputs_to_nearest": True, "sin_cos_by_ends_and_criticals": True}, "r31_mpfr_lower_chunk.py": {"lines": 146, "absolute_path": True, "opens": ["AMRAL_LUC_FC_Round_28_reference/cell0_topology.bin", "AMRAL_LUC_FC_Round_28_reference/witness_axis_stream_2bit.bin", "AMRAL_LUC_FC_Round_29_reference/marker_70.json", "AMRAL_LUC_FC_Round_31_MPFR_ROOT_REPLAY.json", "AMRAL_LUC_FC_Round_31_reference"], "not_in_archive": [], "root_from_mpfr": True, "same_as_a1": ["core_support", "emid", "margin"], "a1_ihull_but_one_point_guard": True, "winner_only": True, "stream_checked": False}, "r31_mpfr_marker70.py": {"lines": 101, "absolute_path": True, "opens": ["AMRAL_LUC_FC_Round_31_MPFR_MARKER70_REPLAY.json", "marker_70.json"], "not_in_archive": [], "normals": [4096, True, True], "sectors": True, "comment_says_adjacent": True}}, } def near(a, b, tol): return abs(a - b) <= tol def sig(x, n=4): return float(f"{x:.{n - 1}e}") def w1_root(w): """sec. 0, 4: the MPFR bisection's d* and its t_n nested between this tree's brackets (and the A1 replay's) and Round 28's intervals; their stated widths; the bisection's 2^-221""" out, rr, ra, r28 = [], w["root_m"], w["root_a1"], w["rootrec28"] keys = ("d", "t3", "t5", "t7") mine = {k: (Fraction(v[0], ONE), Fraction(v[1], ONE)) for k, v in w["scales"].items() if k in keys} mp = {"d": (Fraction(rr["dstar"]["lo"]), Fraction(rr["dstar"]["hi"]))} a1 = {"d": (Fraction(ra["d_star_recomputed"]["lo"]), Fraction(ra["d_star_recomputed"]["hi"]))} old = {"d": (Fraction(r28["d_star_interval"]["lo"]), Fraction(r28["d_star_interval"]["hi"]))} for k in keys[1:]: mp[k] = (Fraction(rr["tmax"][k]["lo"]), Fraction(rr["tmax"][k]["hi"])) a1[k] = (Fraction(ra["tmax_checks"][k]["recomputed_lo"]), Fraction(ra["tmax_checks"][k]["recomputed_hi"])) old[k] = (Fraction(r28["tmax_intervals"][k]["lo"]), Fraction(r28["tmax_intervals"][k]["hi"])) within = lambda a, b: b[0] <= a[0] and a[1] <= b[1] stated = [rr["dstar"]["width"]] + [rr["tmax"][k]["width"] for k in keys[1:]] got = {"nested": {k: [within(mine[k], a1[k]), within(a1[k], mp[k]), within(mp[k], old[k])] for k in keys}, "widths": {k: sig(float(mp[k][1] - mp[k][0])) for k in keys}, "stated": all(near(s, float(mp[k][1] - mp[k][0]), 1e-12 * s) for s, k in zip(stated, keys)), "bisection": mp["d"][1] - mp["d"][0] == Fraction(1, 2 ** 221) and (mp["d"][0] * 2 ** 221).denominator == 1, "flags": [rr["status"], rr["backend"], rr["mpfr_version"]] + [rr["tmax"][k]["overlap_round28"] for k in keys[1:]]} if not all(all(v) for v in got["nested"].values()) or not got["stated"] or not got["bisection"] or got != w["root_claim"]: out.append(f"the root: {got}") w["w1"] = got return out def w2_marker(w): """sec. 5-6: marker 70's MPFR record against its Round 29 file; the exact polygon rebuilt with the package's normals and ceiling from this tree's support bounds - every constraint (the MPFR and A1 replays), float-reduced (the emitter), and with the adjacent arcs counted (the correction's first run)""" out, rec, f29, poly = [], w["marker_m"], w["marker70"]["final"], w["polygons"] got = {"record": [rec["density"] == f29["density"] == rec["normal_count"], rec["outer_area_decimal"] == f29["outer_area_decimal"], rec["margin_decimal"] == f29["margin_decimal"], [rec["round29_outer"], rec["round29_margin"]] == [f29["outer_area_decimal"], f29["margin_decimal"]]], "every_constraint": poly["full"], "is_mpfr": poly["full"] == [rec["outer_area_decimal"], rec["active_constraints"], rec["outer_area_num_bits"], rec["outer_area_den_bits"]] and rec["active_constraints"] == w["marker_a1"]["marker"]["exact_active_constraints"], "float_reduced": poly["reduced"], "is_round29": poly["reduced"] == [f29["outer_area_decimal"], f29["active_constraints"], f29["outer_area_num_bits"], f29["outer_area_den_bits"]], "difference": sig(poly["difference"]), "adjacent": [sig(poly["adjacent"][0], 10), poly["adjacent"][1]]} if not all(got["record"]) or not got["is_mpfr"] or not got["is_round29"] or abs(poly["adjacent"][0] - 0.9201) > 1e-4 or got != w["marker_claim"]: out.append(f"marker 70: {got}") w["w2"] = got return out def w3_lower(w): """sec. 7-10: the MPFR ledger is Round 30's leaf for leaf - path, density, hull count and margin: the same polygons, their membership decided again in MPFR; this tree's certificate (RUN-033) at the same densities""" out, led, a1 = [], w["ledger"], w["a1_rows"] res = w["lower33"] mine = {p: r["ledger"] for (p, _), r in zip(res["leaves"], res["results"])} dens = {x["path"]: x["density"] for x in a1} key = lambda x: (x["path"], x["density"], x["hull_vertices"], x["margin_decimal"]) least = min(led, key=lambda x: x["margin_decimal"]) got = {"leaves": len(led), "statuses": sorted({x["status"] for x in led}), "same_as_round30": sum(key(x) == key(y) for x, y in zip(led, a1)), "mine_pass": sum(mine[x["path"]]["pass"] for x in led if x["path"] in mine and x["density"] == dens.get(x["path"])), "least": [least["path"], least["density"], least["margin_decimal"]]} if len(led) != 9278 or got["same_as_round30"] != 9278 or got["mine_pass"] != 9278 or got != w["lower_claim"]: out.append(f"the lower ledger: {got}") w["w3"] = got return out def w4_queue(w): """sec. 15-17: the 63 queued cells are this tree's cells closed by depth 40, each at the even depth its ledger records; the 14 residual cells are those open at 40, their volumes and ratios this tree's continuation's at the depths recorded; the order within a depth; the marker margins it would rank by""" out, q, at = [], w["queue"], w["atlas"] depths = {int(k): v for k, v in at["depths"].items()} done = {i: d for i, d in depths.items() if d is not None} mq, rq = q["migration_queue"], q["geometry_residual_queue"] rest = mq[1:] vols = at["volumes"] matched = sum(near(vols[str(r["cell"])][str(r["last_depth"])], r["unresolved_volume"], 1e-12 * r["unresolved_volume"]) and near(vols[str(r["cell"])][str(r["last_depth"])] / vols[str(r["cell"])][str(r["last_depth"] - 2)], r["ratio_vs_previous"], 1e-12) for r in rq if str(r["cell"]) in vols) at40 = [vols[k]["40"] / vols[k]["38"] for k in vols] got = {"cells": sorted(x["cell"] for x in mq) == sorted(done), "counts": [len(mq), q["known_geometry_complete_count"], len(done)], "depths": sum(x["closure_depth"] == done[x["cell"]] + done[x["cell"]] % 2 for x in mq if x["cell"] in done), "depth_counts": {str(k): v for k, v in sorted(collections.Counter(x["closure_depth"] for x in mq).items())}, "first": [mq[0]["cell"], mq[0]["status"], q["publication_candidate_cells"]], "order_by_depth_then_cell": [[x["closure_depth"], x["cell"]] for x in rest] == sorted([x["closure_depth"], x["cell"]] for x in rest), "marker_margins": sorted({repr(x["marker_margin"]) for x in mq}), "residual": {"cells": sorted(r["cell"] for r in rq) == sorted(i for i, d in depths.items() if d is None), "counts": [len(rq), q["geometry_residual_count"]], "matched": matched, "last_depths": {str(k): v for k, v in sorted(collections.Counter(r["last_depth"] for r in rq).items())}, "at_40": [len(at40), sig(max(at40))]}} if not got["cells"] or got["depths"] != len(mq) or not got["residual"]["cells"] or matched != len(rq) or got != w["queue_claim"]: out.append(f"the queue: {got}") w["w4"] = got return out def w5_lock(w): """sec. 12-13, 20: the lock's wrapper and script digests against the scripts shipped; the library digests as the document gives them (the binaries are not here); the correction ledger""" out, lock, dg, ce = [], w["lock"], w["digests"], w["corrections"]["entries"] pinned = {lock["wrapper"]["sha256"], *lock["replay_scripts"].values()} got = {"wrapper": lock["wrapper"]["sha256"] == dg["r31_mpfr_backend.py"], "scripts": {k: v == dg[SCRIPTS[k]] for k, v in sorted(lock["replay_scripts"].items())}, "unpinned": sorted(k for k in w["code"] if dg[k] not in pinned), "libraries": [lock["libraries"]["mpfr"]["sha256"] in w["text"], lock["libraries"]["gmp"]["sha256"] in w["text"], [lock["libraries"]["mpfr"]["sha256"], lock["libraries"]["gmp"]["sha256"]] == [w["shard"]["backend_independence"]["backend_B_mpfr_sha256"], w["shard"]["backend_independence"]["backend_B_gmp_sha256"]]], "status": [lock["backend_id"], lock["status"]], "not_a_proof": "not a formal proof" in lock["trust_statement"], "corrections": [[e["id"], e["status"]] for e in ce], "safe_side": ["not a false proof" in ce[0]["soundness"], ce[1]["mathematical_effect"]]} if not got["wrapper"] or not all(got["scripts"].values()) or not all(got["libraries"]) or got != w["lock_claim"]: out.append(f"the lock: {got}") w["w5"] = got return out def _defs(src): """each top-level def's syntax tree, dumped: equal dumps are the same code whatever its layout""" return {node.name: ast.dump(node) for node in ast.parse(src).body if isinstance(node, ast.FunctionDef)} def w6_code(w): """what the package ships, read after the rebuild and never run: the wrapper, and the four replays""" leaves = [row[0] for row in w["manifest"]["leaves"]] code, c30 = w["code"], w["code30"] facts = {} for name, src in sorted(code.items()): opened = sorted({p.replace("\\", "/").rsplit("/", 1)[-1] for p in re.findall(r"open\(\s*'([^']+)'", src)} | set(re.findall(r"ROOT\s*/\s*[\"']([^\"']+)[\"']", src))) facts[name] = {"lines": src.count("\n"), "absolute_path": bool(re.search(r"(?:Path\(|open\(|insert\(0,)\s*[\"']/", src)), "opens": opened, "not_in_archive": [u for u in opened if not any(u.split("/")[-1].split(".")[0].split("*")[0] in leaf for leaf in leaves)]} be, rt, mk, lo, ag = (code[k] for k in ("r31_mpfr_backend.py", "r31_cross_root.py", "r31_mpfr_marker70.py", "r31_mpfr_lower_chunk.py", "r31_aggregate.py")) facts["r31_mpfr_backend.py"].update({ "precision": int(re.search(r"DEFAULT_PREC=(\d+)", be).group(1)), "mpfr_calls": sorted(set(re.findall(r"_LIB\.(mpfr_\w+)\.argtypes", be))), "inputs_to_nearest": "_set_frac(a,fr,RNDN)" in be and "_set_frac(x,a,RNDN);_set_frac(y,b,RNDN)" in be and "10,RNDN)" in be, "sin_cos_by_ends_and_criticals": "_critical_overlap" in be}) facts["r31_cross_root.py"].update({"bits": int(re.search(r"def dstar\(bits=(\d+)\)", rt).group(1)), "master": "Fraction(1673,2000)" in rt}) facts["r31_mpfr_marker70.py"].update({ "normals": [int(re.search(r"^N=(\d+)", mk, re.M).group(1)), "NORMAL_SCALE=10**9" in mk, "SUPPORT_DEN=10**26" in mk], "sectors": "for s in range(s0,s1+1):" in mk, "comment_says_adjacent": "include adjacent sectors defensively" in mk}) facts["r31_mpfr_lower_chunk.py"].update({ "root_from_mpfr": "MPFR_ROOT_REPLAY" in lo and "tmax_intervals" not in lo, "same_as_a1": sorted(k for k, v in _defs(lo).items() if _defs(c30["r30_a1_lower_chunk.py"]).get(k) == v), "a1_ihull_but_one_point_guard": "if len(pts)<=1:return" in c30["r30_a1_lower_chunk.py"] and "if len(pts)<=1" not in lo, "winner_only": "win=np.argmax(np.vstack(ss+[s7]),axis=0)" in lo and "chosen[m]=P[m]" in lo, "stream_checked": "raise RuntimeError" in lo}) facts["r31_aggregate.py"].update({"globs_itself": "REF.glob('mpfr_lower_*.json')" in ag and "mpfr_lower_ledger.json" in ag, "later_file_wins": "byidx[idx]=x" in ag}) w["w6"] = facts return [] if facts == w["code_facts"] else [f"the scripts: {facts}"] def p1_package(w): out, led, low, sh, q = [], w["ledger"], w["lower_m"], w["shard"], w["queue"] # the chunks cover the leaves once, in order, and are the ledger rows, end = [], 0 for name, c in w["chunks"]: s = c["summary"] counts = {str(k): v for k, v in sorted(collections.Counter(x["density"] for x in c["leaves"] if x["status"] == "MPFR-PASS").items())} if s["start"] != end or s["count"] != len(c["leaves"]) or len(c["leaves"]) != s["end"] - s["start"] \ or s["pass"] != sum(x["status"] == "MPFR-PASS" for x in c["leaves"]) \ or s["density_counts"] != counts or name != f"chunks/mpfr_lower_{s['start']:05d}_{s['end']:05d}.json": out.append(f"chunk {name}") end = s["end"] rows += c["leaves"] least = min(led, key=lambda x: x["margin_decimal"]) dens = {str(k): v for k, v in collections.Counter(x["density"] for x in led if x["status"] == "MPFR-PASS").items()} if rows != led or end != 9278 or low["chunk_files"] != len(w["chunks"]) or low["ledger_sha256"] != w["ledger_digests"][0] \ or w["ledger_digests"][0] != w["ledger_digests"][1] or low["missing_indices"] != [] \ or (low["leaves_total"], low["leaves_pass"], low["leaves_inconclusive"], low["density_counts"], low["minimum_margin_decimal"], low["minimum_margin_path"]) \ != (len(led), sum(x["status"] == "MPFR-PASS" for x in led), sum(x["status"] != "MPFR-PASS" for x in led), dens, least["margin_decimal"], least["path"]): out.append("LOWER_REPLAY against the chunks and the ledger") # the shard record against the replays rp, nm, b7, bi = sh["root_path"], sh["necessity_marker_upper"], sh["B7_lower"], sh["backend_independence"] r28, rr, mk, l30 = w["rootrec28"], w["root_m"], w["marker_m"], w["lower30"] if (sh["status"], sh["publication_candidate"], sh["theorem_ready"], sh["global_lebesgue_claim"]) != ("PUBLICATION-CANDIDATE-SHARD", True, False, False) \ or rp["cross_backend_tmax_overlap"] != {k: rr["tmax"][k]["overlap_round28"] for k in ("t3", "t5", "t7")} \ or [rp["path_containment_audit"][f"mpfr_{k}_overlap_round28"] for k in ("t3", "t5", "t7")] != [rr["tmax"][k]["overlap_round28"] for k in ("t3", "t5", "t7")] \ or (rp["path_containment_audit"]["base_path_depth"], rp["path_containment_audit"]["base_axis_trace_length"], rp["path_containment_audit"]["override_count"]) \ != (len(r28["base_path"]), len(r28["base_axis_trace"]), r28["base_override_count"]) \ or (nm["round31_MPFR_outer_area"], nm["round31_MPFR_margin"]) != (mk["outer_area_decimal"], mk["margin_decimal"]) \ or b7["round28_emitter"]["leaves_pass"] != w["bulk28"]["leaves_pass"] \ or (b7["round30_A1"]["leaves_pass"], b7["round30_A1"]["minimum_margin"]) != (l30["leaves_pass"], l30["minimum_margin_decimal"]) \ or (b7["round31_cross_backend"]["leaves_pass"], b7["round31_cross_backend"]["leaves_inconclusive"], b7["round31_cross_backend"]["minimum_margin"], b7["round31_cross_backend"]["minimum_margin_path"]) != (low["leaves_pass"], low["leaves_inconclusive"], low["minimum_margin_decimal"], low["minimum_margin_path"]) \ or [bi["backend_A"], bi["backend_B"], bi["backend_B_mpfr_sha256"], bi["backend_B_gmp_sha256"]] \ != [w["lock30"]["mpmath"]["version"], w["lock"]["backend_id"], w["lock"]["libraries"]["mpfr"]["sha256"], w["lock"]["libraries"]["gmp"]["sha256"]] \ or sh["promotion_rule"]["all_local_requirements_met"] is not True: out.append("the shard record against the replays") # the residual queue is Round 27's record of the cells without a known edge recs = {r["cell"]: r for r in w["progress27"]["currently_without_known_complete_edge"]["cells"]} if any(r["cell"] not in recs or (recs[r["cell"]]["last_tested_depth"], recs[r["cell"]]["unresolved_volume"], recs[r["cell"]]["ratio_vs_previous"]) != (r["last_depth"], r["unresolved_volume"], r["ratio_vs_previous"]) for r in q["geometry_residual_queue"]) or len(recs) != len(q["geometry_residual_queue"]): out.append("the residual queue against Round 27's records") crystal = gate.squash(w["crystal"]) for frag in ("9278/9278", r"3.5423707501\times10^{-9}", w["lock"]["libraries"]["mpfr"]["sha256"], w["lock"]["libraries"]["gmp"]["sha256"], r"\texttt{PUBLICATION-CANDIDATE-SHARD}", "51/77"): if frag not in crystal: out.append(f"crystal: {frag[:40]}") w["p1"] = {"chunks": len(w["chunks"]), "least": [least["path"], least["margin_decimal"]], "density_counts": dens} return out def p2_package(w): out, v = [], w["validation"] leaves = {row[0]: row for row in w["manifest"]["leaves"]} for key, leaf_id, text in (("round31", DOC, w["text"]), ("state_crystal", CRYSTAL, w["crystal"])): rec, (_, size, digest) = v[key], leaves[leaf_id] n = text.count("$$") if rec["sha256"] != digest or rec["bytes"] != size or not rec["utf8"] or rec["file"] != leaf_id.split("/")[-1] \ or rec["double_dollar_count"] != n or rec["double_dollar_even"] != (n % 2 == 0) \ or rec["contains_unicode_escape_sequence"] != bool(re.search(r"\\u[0-9a-fA-F]{4}", text)) \ or rec["contains_bracket_math_delimiter"] != bool(re.search(r"\\[\[\]()]", text)): out.append(f"VALIDATION {key} against the archive and the document") for key, leaf_id in (("MPFR_root_sha256", ROOT_M), ("MPFR_marker70_sha256", MARKER_M), ("MPFR_lower_sha256", LOWER_M), ("MPFR_backend_lock_sha256", LOCK), ("publication_candidate_sha256", SHARD), ("bulk_queue_sha256", QUEUE), ("correction_ledger_sha256", CORRECTIONS), ("MPFR_lower_ledger_sha256", LEDGER)): if v[key] != leaves[leaf_id][2]: out.append(f"VALIDATION {key} against the archive") rr, mk, led, low, sh, q, lock = w["root_m"], w["marker_m"], w["ledger"], w["lower_m"], w["shard"], w["queue"], w["lock"] kc = {"mpfr_root_pass": rr["status"] == "PASS", "all_tmax_overlap": all(x["overlap_round28"] for x in rr["tmax"].values()), "marker70_mpfr_pass": mk["status"] == "PASS" and mk["margin_decimal"] > 0, "mpfr_lower_all_9278": len(led) == 9278 and all(x["status"] == "MPFR-PASS" for x in led), "mpfr_lower_no_inconclusive": not any(x["status"] != "MPFR-PASS" for x in led), "mpfr_lower_min_margin_positive": min(x["margin_decimal"] for x in led) > 0, "mpfr_backend_pinned": all(len(x["sha256"]) == 64 for x in lock["libraries"].values()), "publication_candidate_true": sh["publication_candidate"] is True, "local_theorem_ready_false": sh["theorem_ready"] is False, "global_claim_false": sh["global_lebesgue_claim"] is False, "bulk_queue_has_publication_candidate_70": 70 in q["publication_candidate_cells"] and q["migration_queue"][0]["cell"] == 70, "ledger_hash_matches": low["ledger_sha256"] == w["ledger_digests"][0]} if kc != v["checks"] or v["status"] != "PASS": out.append(f"VALIDATION checks {kc}") w["p2"] = kc return out R31_DEFINITIONS = { "R31-MPFR-MARKER-001": ("in-line", "sec. 6, 20: the first MPFR marker verifier counted the pieces next to the active sector - a safe, loose " "upper bound (about 0.9201) and a false negative, corrected"), "ALL LOCAL CONDITIONS MET": ("in-line", "sec. 13: marker 70's shard meets the six conditions of the local publication-candidate gate"), "ARITHMETIC-MIGRATION QUEUE": ("in-line", "sec. 16: the geometry-complete cells, queued for the arithmetic workflow up to publication candidate"), } _ROOT = ("nested: this tree's brackets inside the A1 replay's, those inside MPFR's 2^-221 bisection, and that inside Round 28's " "intervals (W1)") _UPPER = ("the MPFR polygon is the one this tree's own support bounds give under the package's normals and ceiling - 1,317 " "constraints, the exact area's numerator and denominator to the bit (W2)") _LOWER = ("the MPFR ledger is Round 30's, leaf for leaf and margin for margin - the same polygons, their membership decided again " "in MPFR; every leaf passes this tree's certificate at these densities (W3, RUN-033)") _R30 = "Round 30's three replays, passing here too (RUN-033)" _PROMOTED = ("the six conditions hold as sec. 13 sets them (W1-W5, RUN-033); the wrapper rounds its inputs to nearest, so its " "enclosures hold at 2^-640 in practice, not by construction (W6) - this tree's integer replays of the three parts do not " "depend on it") R31_REVIEWS = [ ("PASS", "t_3,t_5,t_7 与 Round28 directed intervals 全部 overlap", "computation", "PASS", _ROOT), ("PASS", "9278/9278", "computation", "PASS", _LOWER), ("PASS", "", "computation", "PASS", _ROOT), ("PASS", "MPFR root", "computation", "PASS", _ROOT), ("PASS", "MPFR upper", "computation", "PASS", _UPPER), ("PASS", "9278/9278 MPFR lower", "computation", "PASS", _LOWER), ("PASS", "root", "computation", "PASS", _R30), ("PASS", "marker upper", "computation", "PASS", _R30), ("PASS", "9278/9278 lower", "computation", "PASS", _R30), ("ARITHMETICALLY-CLOSED-PROTOTYPE", "19. Current local status lattice", "n/a", "n/a", "a state of the lattice, defined in Round 30; not a judgment"), ("A1-VERIFIED-PINNED-PROTOTYPE", "19. Current local status lattice", "n/a", "n/a", "a state of the lattice, defined in Round 30; not a judgment"), ("PUBLICATION-CANDIDATE-SHARD", "13. Publication-candidate gate", "n/a", "n/a", "the gate's definition, its six conditions stated there; not a judgment"), ("PUBLICATION-CANDIDATE-SHARD", "", "computation", "PASS", _PROMOTED), ("PUBLICATION-CANDIDATE-SHARD", "", "computation", "PASS", _PROMOTED), ("PUBLICATION-CANDIDATE-SHARD", "", "computation", "PASS", _PROMOTED), ("NOT CERTIFIED", "a_{Leb}≥0.835", "reading", "PASS", "true"), ("R31-MPFR-MARKER-001", "6. Initial conservative marker false negative", "computation", "PASS", "reproduced: counting the arcs next to the active piece gives 0.92016 here, a safe bound that cannot certify; the shipped " "script counts only the sectors the interval spans, though its comment still says adjacent ones (W2, W6)"), ("REFERENCE-COMPLETE", "19. Current local status lattice", "n/a", "n/a", "a state of the lattice; not a judgment"), ("ALL LOCAL CONDITIONS MET", "", "computation", "PASS", "root and upper under both backends and this tree's integers (W1, W2); the lower under a second implementation (RUN-033) and a " "second backend (W3); strict throughout; the scripts pinned by digest, the libraries' binaries not here to check (W5)"), ("ARITHMETIC-MIGRATION QUEUE", "", "computation", "PASS", "its 63 cells and their depths are this tree's atlas closed by 40, its 14 residual cells those still open (W4); the marker " "margins it would rank by are all null, so its order is by depth and cell number"), ] def r1_registry(w): return registry.completeness(w["registry"], "R31", w["definitions"], w["reviews"]) CHECKS = {"A0": gate.anchors_check(ANCHORS), "W1": w1_root, "W2": w2_marker, "W3": w3_lower, "W4": w4_queue, "W5": w5_lock, "W6": w6_code, "P1": p1_package, "P2": p2_package, "R1": r1_registry} DEPENDS = {"A0": {"text"}, "W1": {"root_m", "root_a1", "rootrec28", "scales", "root_claim"}, "W2": {"marker_m", "marker70", "marker_a1", "polygons", "marker_claim"}, "W3": {"ledger", "a1_rows", "lower33", "lower_claim"}, "W4": {"queue", "atlas", "queue_claim"}, "W5": {"lock", "digests", "code", "corrections", "shard", "text", "lock_claim"}, "W6": {"code", "code30", "manifest", "code_facts"}, "P1": {"ledger", "lower_m", "shard", "queue", "chunks", "ledger_digests", "rootrec28", "root_m", "marker_m", "lower30", "bulk28", "lock30", "lock", "progress27", "crystal"}, "P2": {"validation", "manifest", "text", "crystal", "root_m", "marker_m", "ledger", "lower_m", "shard", "queue", "lock", "ledger_digests"}, "R1": {"registry", "definitions", "reviews"}} def world(inputs, with_atlas=True): return {**inputs, "scales": r31.root_scales(), "polygons": marker_polygons(inputs["marker70"]), "lower33": r33.computed(inputs["a1_rows"], inputs["a1_key"]), "atlas": atlas_facts() if with_atlas else None} def drill_cases(base): text, led, q = base["text"], base["ledger"], base["queue"] k_thin = next(k for k, x in enumerate(led) if x["path"] == "11010110100110101001110111") k_512 = next(k for k, x in enumerate(led) if x["density"] == 512) def edit(obj, fn): x = copy.deepcopy(obj) fn(x) return x def fail_leaf(res): res["results"][0]["ledger"]["pass"] = False return [ ("K0-unmodified", "control", {}, set()), ("K1-doc-crlf", "control", {"text": text.replace("\n", "\r\n")}, set()), ("K2-queue-keys-sorted", "control", {"queue": json.loads(json.dumps(q, sort_keys=True))}, set()), ("K3-shard-keys-sorted", "control", {"shard": json.loads(json.dumps(base["shard"], sort_keys=True))}, set()), ("M1-doc-margin", "mutation", {"text": text.replace(r"3.5423707501\times", r"3.5423707502\times")}, {"A0"}), ("M2-root-interval", "mutation", {"root_m": edit(base["root_m"], lambda x: x["tmax"]["t5"].update(hi=x["tmax"]["t5"]["lo"]))}, {"W1"}), ("M3-root-width", "mutation", {"root_m": edit(base["root_m"], lambda x: x["dstar"].update(width=2 * x["dstar"]["width"]))}, {"W1"}), ("M4-marker-area", "mutation", {"marker_m": edit(base["marker_m"], lambda x: x.update(outer_area_decimal=x["outer_area_decimal"] + 1e-12))}, {"W2", "P1"}), ("M5-marker-bits", "mutation", {"marker_m": edit(base["marker_m"], lambda x: x.update(outer_area_num_bits=x["outer_area_num_bits"] + 1))}, {"W2"}), ("M6-ledger-margin", "mutation", {"ledger": edit(led, lambda x: x[k_thin].update(margin_decimal=3.5e-9))}, {"W3", "P1"}), ("M7-ledger-density", "mutation", {"ledger": edit(led, lambda x: x[k_512].update(density=1024))}, {"W3", "P1"}), ("M8-certificate", "mutation", {"lower33": edit(base["lower33"], fail_leaf)}, {"W3"}), ("M9-queue-depth", "mutation", {"queue": edit(q, lambda x: x["migration_queue"][5].update(closure_depth=x["migration_queue"][5]["closure_depth"] + 2))}, {"W4"}), ("M10-queue-volume", "mutation", {"queue": edit(q, lambda x: x["geometry_residual_queue"][0].update(unresolved_volume=x["geometry_residual_queue"][0]["unresolved_volume"] * 1.001))}, {"W4", "P1"}), ("M11-lock-script", "mutation", {"lock": edit(base["lock"], lambda x: x["replay_scripts"].update(root="0" * 64))}, {"W5"}), ("M12-correction", "mutation", {"corrections": edit(base["corrections"], lambda x: x["entries"][1].update(mathematical_effect="SOME"))}, {"W5"}), ("M13-code-claim", "mutation", {"code_facts": {}}, {"W6"}), ("M14-chunk-summary", "mutation", {"chunks": edit(base["chunks"], lambda x: x[4][1]["summary"].update(**{"pass": x[4][1]["summary"]["pass"] - 1}))}, {"P1"}), ("M15-shard-margin", "mutation", {"shard": edit(base["shard"], lambda x: x["necessity_marker_upper"].update(round31_MPFR_margin=9.2e-5))}, {"P1"}), ("M16-crystal", "mutation", {"crystal": base["crystal"].replace("9278/9278", "9277/9278")}, {"P1"}), ("M17-validation-digest", "mutation", {"validation": {**base["validation"], "bulk_queue_sha256": "0" * 64}}, {"P2"}), ("M18-validation-check", "mutation", {"validation": {**base["validation"], "checks": {**base["validation"]["checks"], "ledger_hash_matches": False}}}, {"P2"}), ("M19-review-dropped", "mutation", {"reviews": list(R31_REVIEWS[1:])}, {"R1"}), ] def main(): ap = argparse.ArgumentParser() ap.add_argument("--drill", action="store_true") ap.add_argument("--blind", metavar="CID") args = ap.parse_args() base = world(load_inputs()) def build(): return {**base, "registry": registry.load(), "definitions": dict(R31_DEFINITIONS), "reviews": list(R31_REVIEWS), **copy.deepcopy(CLAIMS)} 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 ("w1", "w2", "w3", "w4", "w5", "w6", "p1", "p2"): print(key, json.dumps(w.get(key), default=float, ensure_ascii=False)[:2000]) if not args.drill: return cases = drill_cases(base) 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-034", "subject": "Round 31: the cross-backend replay and the first publication-candidate shard", "document": DOC, "checks": {c: {"pass": not f, "failures": f} for c, f in results.items()}, **{k: w.get(k) for k in ("w1", "w2", "w3", "w4", "w5", "w6", "p1", "p2")}, "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("R31", "RUN-034", R31_DEFINITIONS, R31_REVIEWS) print(f"registry: {len(R31_DEFINITIONS)} definitions, {len(R31_REVIEWS)} reviews recorded for R31") if __name__ == "__main__": main()