"""RUN-033 - Round 30: the independent whole-shard replay and the backend lock. Round 30 replays marker 70's whole shard with a second implementation: the root by its own directed bisection - after a verifier bug, an ultra-narrow rational interval cast to binary64, was caught and recorded as R30-A1-ROOT-001 - marker 70's upper bound by a full exact cyclic polar hull, and all 9278 lower leaves with a new candidate generator (defining disks and their circle intersections, a 10^-17 grid, an exact integer hull): 9278/9278 A1-PASS, the least margin 3.5424e-9 on another leaf than Round 28's. It pins the mpmath/libmp backend by version and source hashes, and keeps the shard short of publication-candidate because both implementations share that backend. Here the replay's root is set against this tree's brackets, which share nothing with mpmath; marker 70 against RUN-032's certificate; and every one of the 9278 leaves is certified again by this tree's integer-interval polygons at the replay's density. The replay's own rule - per direction only the point of the body that wins it - is rebuilt on this tree's contact points and gives back its ledger leaf for leaf; the rule drops every body exposed on the hull over less than one step, and that loss, not the geometry, makes its thinnest leaf. Checks A0 anchors the numbers and formulas below occur in Round 30 as written W1 root sec. 0, 12-13: the replay's d* and t_n nested between this tree's brackets and Round 28's; the correction's cause reproduced; the tree walked is Round 28's W2 marker sec. 0, 19: marker 70's replay against its Round 29 file, Round 29's audit and this tree's certificate W3 lower sec. 2-11: all 9278 leaves at the replay's densities under this tree's certificate; the replay's rule rebuilt; where that rule loses area W4 lock sec. 14-16: the lock's script digests against the scripts shipped; its libmp digests against the stock mpmath where this machine runs the version pinned W5 code what the package ships, read after the rebuild and never run W6 backend sec. 21's open item on this tree's side: its certificates' use of mpmath P1 package the replay files, the chunks, the shard record, the ledger, the crystal and the text agree P2 package VALIDATION against the archive; its checks from the data R1 registry Round 30's judgments reviewed, first-used statuses defined Usage: python code/run033_round30_a1_replay.py [--drill] [--blind CID] """ import argparse import collections import copy import hashlib import inspect import json import math from fractions import Fraction from multiprocessing import Pool import numpy as np from scipy.spatial import ConvexHull import gate import registry import run008_round05_saturation_gate as r8 import run009_round06_witness_exchange as r9 import run011_round08_conditional_lift as r11 import run012_round09_adaptive_atlas as r12 import run013_round10_reference_dry_run as r13 import run019_round16_global_pilot as r19 import run023_round20_mixed_escalation as r23 import run029_round26_full_atlas as r29 import run030_round27_interval_replay as r30 import run031_round28_exact_root as r31 import run032_round29_marker_upper as r32 from corpus import SOURCES, TREE, source_bytes, walk_sources from run010_round07_minimizer_atlas import d_star, t_text from run030_round27_interval_replay import ONE PKG = "main.zip!/AMRAL_LUC_FC_Round_30_Package_v0.1.zip!/" DOC = PKG + "AMRAL_Lebesgue_Finite_Closure_Round_30_A1_Backend_Pinning_v0.1.md" CRYSTAL = PKG + "AMRAL_LUC_FC_State_Crystal_Round_30_v0.1.md" ROOT_A1 = PKG + "AMRAL_LUC_FC_Round_30_A1_ROOT_REPLAY.json" MARKER_A1 = PKG + "AMRAL_LUC_FC_Round_30_A1_MARKER70_REPLAY.json" LOWER_A1 = PKG + "AMRAL_LUC_FC_Round_30_A1_LOWER_REPLAY.json" LOCK = PKG + "AMRAL_LUC_FC_Round_30_BACKEND_LOCK.json" SHARD_A1 = PKG + "AMRAL_LUC_FC_Round_30_A1_WHOLE_SHARD_70.json" CORRECTIONS = PKG + "AMRAL_LUC_FC_Round_30_CORRECTION_LEDGER.json" VALIDATION = PKG + "AMRAL_LUC_FC_Round_30_VALIDATION.json" REF = PKG + "AMRAL_LUC_FC_Round_30_reference/" MARKER70 = r32.REF + "marker_70.json" R29_A1_SCRIPT = r32.PKG + "r29_marker_a1_verify.py" LOG = TREE / "data" / "gate-logs" / "run033-round30-a1-replay.json" CACHE = TREE / "data" / "cache" / "run033-lower.json" WINNER_CACHE = TREE / "data" / "cache" / "run033-winner.json" MARKER_CACHE = TREE / "data" / "cache" / "run033-marker70.json" MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json" T, T_EXACT = 0.835, Fraction(167, 200) CELL0 = "0001110001100111000100010001001111011111" A1_LADDER = (512, 1024, 2048, 4096, 8192, 16384, 32768) BODIES = ("disc", "B3", "B5", "B7") def cell0(): """cell 0 as this tree's binary64 split builds it from the D3 root (RUN-023's box)""" c, h = r23.box(CELL0) return {"path": CELL0, "center": [float(x) for x in c], "half": [float(x) for x in h]} def base_cores(cell, scales): """RUN-031's intended base box of the cell and its two directed cores""" axes, _, _ = r31.base_axes(cell["path"]) lo, hi = r31.fractions(cell["path"], axes, 5) bc, bh = r31.directed_box(lo, hi, r31.BASE, scales) return (r31.core_iv(3, r30.exact(0), bc[0], bc[1], [0, bh[0][1], bh[1][1]]), r31.core_iv(5, bc[2], bc[3], bc[4], [bh[2][1], bh[3][1], bh[4][1]])) def contact_sets(c, h, wc, wh, directions): """each body's contact point and support at the directions 2 pi k / directions: the disc, B3, B5, B7""" th = 2 * np.pi * np.arange(directions) / directions u = np.stack([np.cos(th), np.sin(th)], axis=1) k3, k5 = r19.cores(np.asarray(c, dtype=float), np.asarray(h, dtype=float)) kn = r12.core_pieces(r11.placed_vertices(7, wc[0], wc[1:3]), 1 - r23.delta_n(7, wh))[0] pts = [r13.contact_points(body, th) for body in (r9.placed_disc(), k3, k5, kn)] return th, pts, [np.sum(p * u, axis=1) for p in pts] def winner_candidates(c, h, wc, wh, directions, inward): """sec. 5's rule on this tree's contact points: per direction only the point of the body whose support wins it, moved inward toward its body's centre as RUN-030's are; the float hull's vertices""" _, pts, sup = contact_sets(c, h, wc, wh, directions) ctrs = ((0.0, 0.0), c[0:2], c[3:5], wc[1:3]) win = np.argmax(np.stack(sup), axis=0) chosen = np.array([pts[b][i] + inward * (np.asarray(ctrs[b], dtype=float) - pts[b][i]) for i, b in enumerate(win)]) return [(float(chosen[i][0]), float(chosen[i][1]), int(win[i])) for i in ConvexHull(chosen).vertices] def winner(args): """one leaf under the replay's rule on its intended box: from 512 up to the replay's density, each candidate checked inside its own body and the exact hull of those that pass; stops at the first density with no candidate refused and the area above 167/200""" c, h, wc, wh, box, base, top = args centres, halves = box cores = {1: base[0], 2: base[1], 3: r31.core_iv(7, centres[0], centres[1], centres[2], [x[1] for x in halves])} rows = [] for n in A1_LADDER: if n > top: break cand = winner_candidates(c, h, wc, wh, n, r31.INWARD) verified = [(x, y) for x, y, b in cand if (Fraction(x) ** 2 + Fraction(y) ** 2 < Fraction(1, 4) if b == 0 else r30.inside((r30.exact(x), r30.exact(y)), *cores[b]))] area, vertices = r30.exact_hull_area(verified) rows.append({"n": n, "failures": len(cand) - len(verified), "hull": vertices, "margin": float(area - T_EXACT), "pass": len(verified) == len(cand) and area > T_EXACT}) if rows[-1]["pass"]: break return rows def exposures(c, h, wc, wh, directions): """where the winner-only polygon loses area against all contact points (binary64 hulls; the geometry, not a certificate): runs of the full hull's vertices outside the winner-only hull, each run's cut, the window over which it is exposed, the directions inside that window, and its two edges""" th, pts, sup = contact_sets(c, h, wc, wh, directions) win = np.argmax(np.stack(sup), axis=0) owner = np.concatenate([[b] * directions for b in range(4)]) full, part = np.vstack(pts), np.array([pts[b][i] for i, b in enumerate(win)]) hull, eq = ConvexHull(full), ConvexHull(part).equations v, n = full[hull.vertices], len(hull.vertices) out = [float(np.max(eq[:, :2] @ p + eq[:, 2])) > 1e-13 for p in v] runs, k = [], 0 while k < n: if out[k]: j = k while j + 1 < n and out[j + 1]: j += 1 runs.append([k, j]) k = j + 1 else: k += 1 if len(runs) > 1 and out[0] and out[-1]: runs[0] = [runs[-1][0], runs[0][1] + n] runs.pop() rows = [] for a, b in runs: poly = v[[q % n for q in range(a - 1, b + 2)]] cut = 0.5 * abs(sum(poly[q][0] * poly[(q + 1) % len(poly)][1] - poly[(q + 1) % len(poly)][0] * poly[q][1] for q in range(len(poly)))) e1, e2 = v[a % n] - v[(a - 1) % n], v[(b + 1) % n] - v[b % n] n1, n2 = math.atan2(-e1[0], e1[1]) % (2 * math.pi), math.atan2(-e2[0], e2[1]) % (2 * math.pi) window = (n2 - n1) % (2 * math.pi) rows.append({"bodies": sorted({BODIES[owner[hull.vertices[q % n]]] for q in range(a, b + 1)}), "vertices": b - a + 1, "cut": cut, "window": window, "inside": sum(1 for t in th if 0 < (t - n1) % (2 * math.pi) < window), "edges": [float(np.hypot(*e1)), float(np.hypot(*e2))], "half_edges_window": 0.5 * float(np.hypot(*e1) * np.hypot(*e2)) * window}) return {"difference": float(hull.volume - ConvexHull(part).volume), "runs": rows} def compute_winner(rows, extra): """sec. 4-5 rebuilt on this tree's side: every leaf of the replay under its own rule, and the exposure breakdown on the leaves named""" cell = cell0() scales = r31.root_scales() base = base_cores(cell, scales) tn = t_text(7, d_star(r31.TM)) seq = r31.float_sequence(tn, 30) waxes = [a for a, _ in seq] jobs, geo = [], [] for row in rows: wc, wh = r31.float_box(row["path"], seq, tn) wlo, whi = r31.fractions(row["path"], waxes, 3) jobs.append((cell["center"], cell["half"], wc, wh, r31.directed_box(wlo, whi, r31.WITNESS, scales), base, row["density"])) if row["path"] in extra: geo.append([row["path"], row["density"], exposures(cell["center"], cell["half"], wc, wh, row["density"])]) with Pool(14) as pool: ladder = pool.map(winner, jobs, chunksize=16) return {"ladder": ladder, "exposures": geo} def _cached(path, key, fn): if path.exists(): cached = json.loads(path.read_text(encoding="utf-8")) if cached.get("key") == key: return cached["results"] results = json.loads(json.dumps(fn())) path.parent.mkdir(parents=True, exist_ok=True) path.write_text(json.dumps({"key": key, "results": results}) + "\n", encoding="utf-8") return results def computed(rows, key_bytes): """RUN-031's migration - this tree's lift of cell 0, every leaf certified on its intended box - at the replay's density for each path, and on the ladder from 256""" digest = hashlib.sha256() digest.update(inspect.getsource(cell0).encode()) for fn in (r31.compute,): digest.update(inspect.getsource(fn).encode()) for mod in (r8, r9, r19, r23, r30, r31): digest.update(open(mod.__file__, "rb").read()) digest.update(key_bytes) return _cached(CACHE, digest.hexdigest(), lambda: r31.compute(cell0(), rows)) def winner_computed(rows, key_bytes, extra): digest = hashlib.sha256() for fn in (cell0, base_cores, contact_sets, winner_candidates, winner, exposures, compute_winner): digest.update(inspect.getsource(fn).encode()) for mod in (r8, r9, r11, r12, r13, r19, r23, r30, r31): digest.update(open(mod.__file__, "rb").read()) digest.update(key_bytes + json.dumps(sorted(extra)).encode()) return _cached(WINNER_CACHE, digest.hexdigest(), lambda: compute_winner(rows, extra)) def load_inputs(): blobs = {n: source_bytes(n) for n in SOURCES} want = {MARKER70, R29_A1_SCRIPT, r31.ROOTREC, r31.TOPO, r31.AXES, r31.BULK, r32.AUDIT} 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} chunks = sorted((k, json.loads(v)) for k, v in got.items() if k.startswith(REF + "a1_lower_")) rows = [x for _, c in chunks for x in c["leaves"]] return {"text": got[DOC].decode("utf-8"), "crystal": got[CRYSTAL].decode("utf-8"), "root_a1": json.loads(got[ROOT_A1]), "marker_a1": json.loads(got[MARKER_A1]), "lower_a1": json.loads(got[LOWER_A1]), "lock": json.loads(got[LOCK]), "shard_a1": json.loads(got[SHARD_A1]), "corrections": json.loads(got[CORRECTIONS]), "validation": json.loads(got[VALIDATION]), "chunks": [[k[len(REF):], c["summary"]] for k, c in chunks], "rows": rows, "marker70": json.loads(got[MARKER70]), "rootrec28": json.loads(got[r31.ROOTREC]), "bulk28": json.loads(got[r31.BULK]), "audit29": json.loads(got[r32.AUDIT]), "digests": {"marker70": hashlib.sha256(got[MARKER70]).hexdigest(), "r29_a1_script": hashlib.sha256(got[R29_A1_SCRIPT]).hexdigest(), "topology28": hashlib.sha256(got[r31.TOPO]).hexdigest(), "axes28": hashlib.sha256(got[r31.AXES]).hexdigest(), **{k[len(REF):]: hashlib.sha256(v).hexdigest() 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")}, "key_bytes": b"".join(got[k] for k in sorted(got) if k.startswith(REF + "a1_lower_")), "manifest": json.loads(MANIFEST.read_text(encoding="utf-8")), "local": local_backend()} def marker_computed(marker): """RUN-032's certificate for marker 70 alone: the exact area at its point, this tree's polygon with the bridging normals on the ladder, and the uniform normals at the package's density and half of it""" digest = hashlib.sha256() for fn in (r32.reuleaux_iv, r32.dot_hi, r32.dot_lo, r32.support_hi, r32.base_bodies, r32.half_planes, r32.outer_area, r32.uniform_normals, r32.bridge_normals, r32.certify): digest.update(inspect.getsource(fn).encode()) for mod in (r8, r9, r11, r12, r13, r19, r30, r31): digest.update(open(mod.__file__, "rb").read()) digest.update(json.dumps([marker["q_rational"], marker["final"]["density"]]).encode()) return _cached(MARKER_CACHE, digest.hexdigest(), lambda: r32.certify(([Fraction(x) for x in marker["q_rational"]], marker["final"]["density"]))) def local_backend(): """this machine's mpmath and Python: the versions, the libmp sources' digests, and whole-package digests formed in a few natural ways (the lock does not say how its own is formed). No path leaves this function""" import fractions import pathlib import platform import mpmath root = pathlib.Path(mpmath.__file__).parent files = sorted((p.relative_to(root).as_posix(), p.read_bytes()) for p in root.rglob("*.py") if "__pycache__" not in p.parts) h = lambda b: hashlib.sha256(b).hexdigest() whole = {} for label, sel in (("all", files), ("no tests", [f for f in files if not f[0].startswith("tests/")])): whole[label + ": path, NUL, bytes"] = h(b"".join(r.encode() + b"\0" + b for r, b in sel)) whole[label + ": path:digest lines"] = h("".join(f"{r}:{h(b)}\n" for r, b in sel).encode()) whole[label + ": sha256sum lines"] = h("".join(f"{h(b)} {r}\n" for r, b in sel).encode()) whole[label + ": digests concatenated"] = h("".join(h(b) for _, b in sel).encode()) whole[label + ": raw digests concatenated"] = h(b"".join(hashlib.sha256(b).digest() for _, b in sel)) whole[label + ": JSON path to digest"] = h(json.dumps({r: h(b) for r, b in sel}, sort_keys=True).encode()) return {"mpmath": mpmath.__version__, "python": platform.python_version(), "libmp": {r[len("libmp/"):]: h(b) for r, b in files if r.startswith("libmp/") and r.count("/") == 1}, "whole": whole, "fractions": h(pathlib.Path(fractions.__file__).read_bytes())} ANCHORS = { "W1": [r"T_M=\frac{1673}{2000}", r"\text{全部overlapPASS}.", r"把宽度约$10^{-64}$的exactrational$d_\star$interval先cast成binary64。", r"这直接把interval位置扰动到$10^{-17}$级。", r"\boxed{\text{overlapPASS}.}", r"\text{exact}\to\text{float}\to\text{interval}"], "W2": [r"$$0.8349075014501105.$$", r"9.24985499\times10^{-5}.", r"直接以全部rationalsupportconstraints做exactcyclicpolarhull。", r"Round30whole-shard只需要marker70A1，"], "W3": [r"9278/9278\text{A1-PASS}.", r"3.54237075\times10^{-9}>0.", r"11010110100110101001110111", r"这与Round28emitter的最薄leaf不同。", r"##512$$8174$$", r"##1024$$869.$$", r"##2048$$163.$$", r"##4096$$56.$$", r"##8192$$12.$$", r"##16384$$4.$$", r"Round30没有leaf需要32768。", r"3.1949\times10^{-8}.", r"3.5424\times10^{-9}.", r"只表示不同innerpolygonapproximation有不同loss。", r"Q=10^{17}.", r"10^{-17}\mathbbZ^2.", r"D_{\max}^2<\rho_{\rmlo}^2.", r"p(u)=\arg\max_iu\cdotp_i(u).", r"V_j+\rhou."], "W4": [r"\texttt{PINNED-MPMATH-LIBMP-PROTOTYPE-v0.1}.", r"mpmathversion；", r"entirempmathPython-sourcepackagehash；", r"每个`libmp/*.py`hash；", r"`fractions.py`hash；", r"A1verifierscripthashes。", r"\texttt{PINNED-REPRODUCIBLE-PROTOTYPE}", r"\texttt{TRUST-AUDIT-OPEN}.", r"\text{reproducibility}\ne\text{backendtrustproof}."], "W5": [r"两套实现虽然独立，但仍共享同一个mpmath.iv/libmpdirectedarithmeticbackend。", r"`Body.support/contact`candidategenerator；", r"SciPyconvex-hullcandidatereduction；", r"Round28densitydecision；", r"Round28Fractionhullcode。"], "W6": [r"1.用MPFR/MPFI重播directedgeometry；", r"只要第二backend能重放："], "P1": [r"a_{\mathrm{Leb}}\ge0.835\text{remainsNOTCERTIFIED}.", r"\texttt{A1-VERIFIED-PINNED-PROTOTYPE-SHARD}", r"51/77\text{at}d=36."], } CLAIMS = { # this tree's brackets (1e-90) inside the replay's d* and t_n, the replay's inside Round 28's: nested, not only overlapping; # the widths [the replay's, Round 28's]; d* through binary64 moves 1.7e-17 and every t_n lands outside Round 28's interval, # [outside, least and most distance above it]; the tree walked is Round 28's "root_claim": {"target": True, "nested": {"d": [True, True], "t3": [True, True], "t5": [True, True], "t7": [True, True]}, "widths": {"d": [2.83e-73, 3.112e-61], "t3": [4.044e-73, 4.343e-64], "t5": [3.154e-73, 3.387e-64], "t7": [2.985e-73, 3.205e-64]}, "stated": True, "flags": ["PASS", True, True, True], "cast": {"shift": [1.702e-17, 1.702e-17], "t3": [True, 2.433e-17, 2.433e-17], "t5": [True, 1.897e-17, 1.897e-17], "t7": [True, 1.795e-17, 1.795e-17]}, "correction": True, "tree": [True, True, True]}, # the replay is Round 29's audit row; active counts [replay, emitter file, this tree's uniform normals at 4096]; the exact # area at the marker; this tree's uniform polygon within 5.2e-11 of the replay's; this tree's certificate [normals, margin, # bridging normals] "marker_claim": {"audit_row": True, "file": [True, True, True], "input": True, "all_constraints": True, "active": [1317, 1284, 1284], "above_exact": True, "exact": 0.8348018420315643, "uniform_difference": 5.22e-11, "mine": [128, 0.00013675030022222711, 11]}, # every body's contact points: all pass at the replay's densities, each margin above the replay's by 2.1e-8 to 1.6e-4; the # least is Round 28's thinnest leaf, its margin within 2e-19 of Round 28's; the replay's thinnest leaf has 2.2e-5 here; on # the common ladder (from 512) the replay's density is above this tree's least on 974 leaves, below on none. # the replay's rule rebuilt: its density and hull count on every leaf, the margin 1.6e-12 above (1e-12 inward here, 2e-12 # there). Its losses: runs of the full hull's vertices exposed over less than one step, their cuts summing to the difference "lower_claim": { "all_points": {"leaves": 9278, "same_paths": True, "pass": 9278, "refused": 0, "above": 9278, "gap": [2.111246498919578e-08, 0.00015677548448447376], "least": ["1101011010010011111001110", 16384, 3.194892273812446e-08], "least_is_round28s": [True, 1.9e-19], "thinnest": ["11010110100110101001110111", 2048, 3.5423707500925403e-09, 2.221117597766235e-05], "densities": {"replay_higher": 974, "replay_lower": 0, "none_passing": 0}}, "rule": {"first_equal": 9278, "hull_equal": 9278, "gap": [1.5735052150134266e-12, 1.6701004728475466e-12], "refused": 0, "density_counts": {"512": 8174, "1024": 869, "2048": 163, "4096": 56, "8192": 12, "16384": 4}, "least": ["11010110100110101001110111", 2048, 3.54403351648527e-09]}, # [the replay's margin, every contact point's here, the replay's rule's here] "exposures": [{"path": "00000", "density": 512, "margins": [0.0013094480928614774, 0.001326824192892529, 0.0013094480944934733], "difference": 1.738e-05, "runs": 6, "sub_step": True, "sum_is_difference": True, "largest": [["B3"], 4.269e-06, 0.002629, [0.265, 0.01226], 4.269e-06]}, {"path": "1101011010010011111001110", "density": 16384, "margins": [6.779501363957614e-09, 3.194892273812446e-08, 6.78116921701634e-09], "difference": 2.517e-08, "runs": 12, "sub_step": True, "sum_is_difference": True, "largest": [["B3"], 8.255e-09, 0.0001206, [0.0003831, 0.3575], 8.255e-09]}, {"path": "11010110100110101001110111", "density": 2048, "margins": [3.5423707500925403e-09, 2.221117597766235e-05, 3.54403351648527e-09], "difference": 2.221e-05, "runs": 10, "sub_step": True, "sum_is_difference": True, "largest": [["disc"], 2.105e-05, 0.001853, [0.2669, 0.084], 2.077e-05]}]}, # the two digests are the scripts shipped; the marker driver is not pinned; no shipped script computes the root "lock_claim": {"lower": True, "marker": True, "unpinned": ["r30_marker_a1_chunk.py"], "root_script": [], "pinned": ["1.3.0", "3.13.5", 9], "status": "PINNED-REPRODUCIBLE-PROTOTYPE / TRUST-AUDIT-OPEN", "not_an_audit": True}, "code_facts": { "r29_marker_a1_verify.py": {"lines": 92, "absolute_path": True, "uses": ["AMRAL_LUC_FC_Round_29_A1_MARKER_AUDIT.json", "AMRAL_LUC_FC_Round_29_reference"], "not_in_archive": [], "mpmath_iv": True, "round29_bytes": True, "sector_support": True, "imports_scipy": False, "method_string": True}, "r30_a1_lower_chunk.py": {"lines": 212, "absolute_path": True, "uses": ["AMRAL_LUC_FC_Round_28_ROOT_RECONSTRUCTION.json", "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_30_reference"], "not_in_archive": [], "mpmath_iv": True, "dps": 75, "grid": "10**17", "inward": 2e-12, "ladder": [512, 1024, 2048, 4096, 8192, 16384, 32768], "root_from_round28": True, "winner_only": True, "decimal_into_interval": True}, "r30_marker_a1_chunk.py": {"lines": 10, "absolute_path": True, "uses": ["AMRAL_LUC_FC_Round_30_reference", "r29_marker_a1_verify"], "not_in_archive": [], "mpmath_iv": False, "writes": ["marker_a1_{a:02d}_{b:02d}.json"], "outputs_shipped": False}}, "backend_claim": {"functions": 33, "mpmath_in": ["acos_iv", "d_star_iv"], "then_asserted": ["acos_iv", "d_star_iv"], "machin_in_60_decimals": True}, } def near(a, b, tol): return abs(a - b) <= tol def sig(x, n=4): """x to n significant digits: the geometry's binary64 figures, kept from drifting with the last bits""" return float(f"{x:.{n - 1}e}") def w1_root(w): """sec. 0, 12-13: the replay's d* and t_n intervals against this tree's brackets and Round 28's, their stated widths, the correction's cause - d* through binary64 before t_n - reproduced with this tree's t_n, and the tree the lower replay walks: Round 28's""" out, a1, r28 = [], w["root_a1"], w["rootrec28"] fr = lambda s: Fraction(*map(int, s.split("/"))) keys = ("d", "t3", "t5", "t7") mine = {k: (Fraction(int(v[0]), ONE), Fraction(int(v[1]), ONE)) for k, v in w["computed"]["scales"].items() if k in keys} rep = {"d": (fr(a1["d_star_recomputed"]["lo"]), fr(a1["d_star_recomputed"]["hi"]))} old = {"d": (fr(r28["d_star_interval"]["lo"]), fr(r28["d_star_interval"]["hi"]))} for k in keys[1:]: rep[k] = (fr(a1["tmax_checks"][k]["recomputed_lo"]), fr(a1["tmax_checks"][k]["recomputed_hi"])) old[k] = (fr(r28["tmax_intervals"][k]["lo"]), fr(r28["tmax_intervals"][k]["hi"])) within = lambda a, b: b[0] <= a[0] and a[1] <= b[1] stated = [a1["d_star_recomputed"]["width_decimal"]] + [a1["tmax_checks"][k]["recomputed_width_decimal"] for k in keys[1:]] cast = {} for k, n in (("t3", 3), ("t5", 5), ("t7", 7)): rows = [] for end in (*old["d"], *rep["d"]): t = r31.t_iv(n, r30.exact(Fraction(float(end)))) t = (Fraction(t[0], ONE), Fraction(t[1], ONE)) rows.append((t[0] > old[k][1] or t[1] < old[k][0], float(t[0] - old[k][1]) if t[0] > old[k][1] else float(t[1] - old[k][0]))) cast[k] = [all(r[0] for r in rows), sig(min(r[1] for r in rows)), sig(max(r[1] for r in rows))] shift = [float(Fraction(float(e)) - e) for e in (*old["d"], *rep["d"])] got = {"target": a1["master_target_exact"] == r28["master_target_exact"] == "1673/2000", "nested": {k: [within(mine[k], rep[k]), within(rep[k], old[k])] for k in keys}, "widths": {k: [sig(float(rep[k][1] - rep[k][0])), sig(float(old[k][1] - old[k][0]))] for k in keys}, "stated": all(near(s, float(rep[k][1] - rep[k][0]), 1e-12 * s) for s, k in zip(stated, keys)), "flags": [a1["status"]] + [a1["tmax_checks"][k]["round28_overlap"] for k in keys[1:]], "cast": {"shift": [sig(min(shift)), sig(max(shift))], **cast}, "correction": a1["correction"] == w["corrections"]["entries"][0] and a1["correction"]["id"] == "R30-A1-ROOT-001", "tree": [a1["topology_sha256"] == w["digests"]["topology28"] == r28["witness_tree"]["topology_sha256"], a1["axis_stream_sha256"] == w["digests"]["axes28"] == r28["witness_tree"]["axis_stream_sha256"], a1["base_path_depth"] == a1["base_axis_trace_length"] == len(r28["base_path"]) == len(r28["base_axis_trace"]) == 40]} ok = got["target"] and all(all(v) for v in got["nested"].values()) and got["stated"] and all(c[0] for c in cast.values()) \ and got["correction"] and all(got["tree"]) if not ok or got != w["root_claim"]: out.append(f"the root: {got}") w["w1"] = got return out def w2_marker(w): """sec. 0, 19: marker 70's replay against its Round 29 file, Round 29's audit row and this tree's own certificate (RUN-032's, for this marker)""" out, rec, f, mine = [], w["marker_a1"]["marker"], w["marker70"]["final"], w["marker_mine"] got = {"audit_row": [x for x in w["audit29"]["markers"] if x["cell"] == 70] == [rec], "file": [rec["density"] == f["density"], rec["outer_area_decimal"] == f["outer_area_decimal"], rec["margin_decimal"] == f["margin_decimal"]], "input": w["marker_a1"]["input_marker_sha256"] == w["digests"]["marker70"], "all_constraints": rec["full_constraint_count"] == rec["density"], "active": [rec["exact_active_constraints"], f["active_constraints"], mine["uniform"]["active"]], "above_exact": rec["outer_area_decimal"] > mine["exact"], "exact": mine["exact"], "uniform_difference": sig(abs(rec["outer_area_decimal"] - mine["uniform"]["area"])), "mine": [mine["ladder"]["N"], mine["ladder"]["margin"], mine["bridges"]]} if not (got["audit_row"] and all(got["file"]) and got["input"] and got["all_constraints"] and got["above_exact"] and rec["pass"]) \ or not near(rec["margin_decimal"], T - rec["outer_area_decimal"], 2e-16) or got != w["marker_claim"]: out.append(f"marker 70: {got}") w["w2"] = got return out def w3_lower(w): """sec. 2-11: the replay's 9278 paths are this tree's lift of cell 0; every leaf passes at the replay's density under this tree's certificate (every body's contact point), above the replay's margin; the replay's own rule - per direction the union winner's point only - rebuilt on this tree's contact points reproduces its ledger; and where that rule loses area: bodies exposed over less than one step""" out, rows, res, win, bulk = [], w["rows"], w["computed"], w["winner"], w["bulk28"] a1 = {r["path"]: r for r in rows} mine = {p: r for (p, _), r in zip(res["leaves"], res["results"])} at = {p: r["ledger"] for p, r in mine.items()} gap = [at[p]["margin"] - a1[p]["margin_decimal"] for p in a1 if p in at] least = min(at, key=lambda p: at[p]["margin"]) thin = min(a1, key=lambda p: a1[p]["margin_decimal"]) common = [(a1[p]["density"], max(mine[p]["least"]["n"], A1_LADDER[0])) for p in a1 if p in mine and mine[p]["least"]] rule = dict(zip([r["path"] for r in w["winner_rows"]], win["ladder"])) first = {p: (lad[-1]["n"] if lad[-1]["pass"] else None) for p, lad in rule.items()} rgap = [rule[p][-1]["margin"] - a1[p]["margin_decimal"] for p in a1 if p in rule] rleast = min(rule, key=lambda p: rule[p][-1]["margin"]) expo = [] for path, n, g in win["exposures"]: top = max(g["runs"], key=lambda r: r["cut"]) expo.append({"path": path, "density": n, "margins": [a1[path]["margin_decimal"], at[path]["margin"], rule[path][-1]["margin"]], "difference": sig(g["difference"]), "runs": len(g["runs"]), "sub_step": all(r["inside"] == 0 and r["window"] < 2 * math.pi / n for r in g["runs"]), "sum_is_difference": near(sum(r["cut"] for r in g["runs"]), g["difference"], 1e-12), "largest": [top["bodies"], sig(top["cut"]), sig(top["window"]), [sig(e) for e in top["edges"]], sig(top["half_edges_window"])]}) got = {"all_points": {"leaves": len(rows), "same_paths": sorted(mine) == sorted(a1), "pass": sum(at[p]["pass"] for p in a1 if p in at), "refused": sum(at[p]["failures"] for p in a1 if p in at), "above": sum(g > 0 for g in gap), "gap": [min(gap), max(gap)], "least": [least, a1[least]["density"], at[least]["margin"]], "least_is_round28s": [least == bulk["minimum_exact_rational_margin_path"], sig(abs(at[least]["margin"] - bulk["minimum_exact_rational_margin_decimal"]), 2)], "thinnest": [thin, a1[thin]["density"], a1[thin]["margin_decimal"], at[thin]["margin"]], "densities": {"replay_higher": sum(a > b for a, b in common), "replay_lower": sum(a < b for a, b in common), "none_passing": sum(1 for p in mine if not mine[p]["least"])}}, "rule": {"first_equal": sum(first.get(p) == a1[p]["density"] for p in a1), "hull_equal": sum(rule[p][-1]["hull"] == a1[p]["hull_vertices"] for p in a1 if p in rule), "gap": [min(rgap), max(rgap)], "refused": sum(x["failures"] for lad in rule.values() for x in lad), "density_counts": {str(k): v for k, v in sorted(collections.Counter(first.values()).items(), key=lambda x: x[0] or 0)}, "least": [rleast, rule[rleast][-1]["n"], rule[rleast][-1]["margin"]]}, "exposures": expo} ap, ru = got["all_points"], got["rule"] if len(rows) != 9278 or not ap["same_paths"] or ap["pass"] != 9278 or ap["refused"] or ap["above"] != 9278 or ap["densities"]["replay_lower"] \ or ru["first_equal"] != 9278 or ru["hull_equal"] != 9278 or ru["refused"] or not all(e["sub_step"] and e["sum_is_difference"] for e in expo) \ or got != w["lower_claim"]: out.append(f"the lower replay: {got}") w["w3"] = got return out def w4_lock(w): """sec. 14-16: the lock's script digests against the scripts shipped, and what it leaves out; its libmp digests against the stock mpmath and its whole-package digest, where this machine runs the version pinned (compared only there)""" out, lock, dg, code, here = [], w["lock"], w["digests"], w["code"], w["local"] sc = lock["proof_critical_scripts"] pinned = (sc["lower_A1_script_sha256"], sc["marker_A1_script_sha256"]) version, py = lock["mpmath"]["version"], lock["python"]["version"].split()[0] same = here["mpmath"] == version libmp = ("equal" if here["libmp"] == lock["mpmath"]["libmp_source_hashes"] else "differs") if same else "not compared" got = {"lower": sc["lower_A1_script_sha256"] == dg["r30_a1_lower_chunk.py"], "marker": sc["marker_A1_script_sha256"] == dg["r29_marker_a1_verify.py"] == dg["r29_a1_script"], "unpinned": sorted(k for k in code if dg[k] not in pinned), "root_script": sorted(k for k, src in code.items() if "1673" in src or "d_star" in src), "pinned": [version, py, len(lock["mpmath"]["libmp_source_hashes"])], "status": lock["status"], "not_an_audit": any("does not constitute an independent formal audit" in s for s in lock["trust_statement"])} w["w4"] = {**got, "here": {"mpmath": here["mpmath"], "python": here["python"], "libmp": libmp, "whole_package": {"tried": len(here["whole"]), "reproduced": sum(v == lock["mpmath"]["all_python_sources_merkle_like_sha256"] for v in here["whole"].values())} if same else "not compared", "fractions": here["fractions"] == lock["exact_arithmetic"]["fractions_sha256"] if here["python"] == py else "not compared"}} if not (got["lower"] and got["marker"]) or libmp == "differs" or got != w["lock_claim"]: out.append(f"the lock: {w['w4']}") return out def w5_code(w): """what the package ships, read after the rebuild and never run: three scripts; the facts that matter to what the replays share""" import re leaves = [row[0] for row in w["manifest"]["leaves"]] facts = {} for name, src in sorted(w["code"].items()): uses = sorted(set(re.findall(r"ROOT\s*/\s*[\"']([^\"']+)[\"']", src)) | set(re.findall(r"^import (r\d+_\w+)", src, re.M))) facts[name] = {"lines": src.count("\n"), "absolute_path": bool(re.search(r"Path\(\s*[\"']/", src)), "uses": uses, "not_in_archive": [u for u in uses if not any(u.split("/")[-1].split(".")[0] in leaf for leaf in leaves)], "mpmath_iv": "mp.iv" in src} low, mk, drv = (w["code"][k] for k in ("r30_a1_lower_chunk.py", "r29_marker_a1_verify.py", "r30_marker_a1_chunk.py")) facts["r30_a1_lower_chunk.py"].update({ "dps": int(re.search(r"mp\.iv\.dps=(\d+)", low).group(1)), "grid": re.search(r"\bQ=(10\*\*\d+)", low).group(1), "inward": float(re.search(r"INWARD=([0-9.e-]+)", low).group(1)), "ladder": json.loads(re.search(r"DENS=(\[[0-9,]+\])", low).group(1)), "root_from_round28": "Round_28_ROOT_RECONSTRUCTION" in low and 'root["tmax_intervals"]' in low, "winner_only": "win=np.argmax(stackS,axis=0)" in low and "chosen[m]=P[m]" in low, "decimal_into_interval": "Decimal(fr.numerator)/Decimal(fr.denominator)" in low and "mp.iv.mpf([fstr(" in low}) facts["r29_marker_a1_verify.py"].update({"round29_bytes": w["digests"]["r29_marker_a1_verify.py"] == w["digests"]["r29_a1_script"], "sector_support": "mp.iv.atan2(ivc(b),ivc(a))" in mk, "imports_scipy": bool(re.search(r"^\s*(?:import|from) scipy", mk, re.M)), "method_string": "no scipy candidate reduction" in mk}) facts["r30_marker_a1_chunk.py"].update({"writes": re.findall(r'f"(marker_a1_[^"]*)"', drv), "outputs_shipped": any("Round_30_reference/marker_a1_" in leaf for leaf in leaves)}) w["w5"] = facts return [] if facts == w["code_facts"] else [f"the scripts: {facts}"] PROOF_FNS = (r30.down, r30.up, r30.exact, r30.add, r30.mul, r30.div_int, r30.cos_sin, r30.inside, r30.exact_hull_area, r31.atan_inv, r31.machin_pi, r31.radius, r31.sub, r31.neg, r31.sqrt_iv, r31.recip, r31.acos_iv, r31.apriori, r31.d_star_iv, r31.t_iv, r31.root_scales, r31.fractions, r31.directed_box, r31.core_iv, r31.migrate, r32.reuleaux_iv, r32.dot_hi, r32.dot_lo, r32.support_hi, r32.base_bodies, r32.half_planes, r32.outer_area) def w6_backend(w): """sec. 21's open item, on this tree's side: the functions its root, marker and lower certificates rest on use mpmath only for a 150-digit guess, which each then brackets and checks in Python integers; its pi is Machin's, inside RUN-030's 60 decimals""" fns = PROOF_FNS + (winner,) uses = [fn.__name__ for fn in fns if "mpmath" in inspect.getsource(fn)] got = {"functions": len(fns), "mpmath_in": uses, "then_asserted": [n for n in uses if "assert" in inspect.getsource(getattr(r31, n, winner))], "machin_in_60_decimals": r30.PI[0] <= r31.PI[0] and r31.PI[1] <= r30.PI[1]} w["w6"] = got return [] if got == w["backend_claim"] and got["mpmath_in"] == got["then_asserted"] else [f"this tree's backend: {got}"] def p1_package(w): out, rows, low, sh, dg = [], w["rows"], w["lower_a1"], w["shard_a1"], w["digests"] leaves = {row[0]: row for row in w["manifest"]["leaves"]} for name, s in w["chunks"]: part = rows[s["start"]:s["end"]] counts = {str(k): v for k, v in sorted(collections.Counter(x["density"] for x in part if x["status"] == "A1-PASS").items())} if name != f"a1_lower_{s['start']:05d}_{s['end']:05d}.json" or s["count"] != len(part) or s["pass"] != sum(x["status"] == "A1-PASS" for x in part) \ or s["inconclusive"] != len(part) - s["pass"] or s["density_counts"] != counts: out.append(f"chunk {name} against its rows") low_counts = {str(k): v for k, v in collections.Counter(x["density"] for x in rows).items()} least = min(rows, key=lambda x: x["margin_decimal"]) if low["chunks"] != [n for n, _ in w["chunks"]] or (low["leaves_total"], low["leaves_pass"], low["leaves_inconclusive"]) \ != (len(rows), sum(x["status"] == "A1-PASS" for x in rows), sum(x["status"] != "A1-PASS" for x in rows)) \ or low["density_counts"] != low_counts or (low["minimum_margin_decimal"], low["minimum_margin_path"]) != (least["margin_decimal"], least["path"]) \ or low["inconclusive_examples"] != []: out.append("LOWER_REPLAY against the chunks") m = w["marker_a1"]["marker"] for key, leaf_id in (("root_path_A1", ROOT_A1), ("marker_upper_A1", MARKER_A1), ("lift_lower_A1", LOWER_A1), ("backend_lock", LOCK)): if sh[key]["sha256"] != leaves[leaf_id][2] or sh[key]["file"] != leaf_id.split("/")[-1]: out.append(f"shard: {key} against the archive") ll, ev = sh["lift_lower_A1"], sh["emitter_vs_A1"] if (sh["marker_upper_A1"]["outer_area_decimal"], sh["marker_upper_A1"]["margin_decimal"]) != (m["outer_area_decimal"], m["margin_decimal"]) \ or (ll["leaves_total"], ll["leaves_pass"], ll["leaves_inconclusive"], ll["minimum_A1_margin_decimal"], ll["minimum_A1_margin_path"]) \ != (low["leaves_total"], low["leaves_pass"], low["leaves_inconclusive"], low["minimum_margin_decimal"], low["minimum_margin_path"]) \ or (ev["round28_emitter_leaf_pass"], ev["round30_A1_leaf_pass"]) != (w["bulk28"]["leaves_pass"], low["leaves_pass"]) \ or (sh["result_status"], sh["publication_candidate"], sh["theorem_ready"], sh["global_lebesgue_claim"]) \ != ("A1-VERIFIED-PINNED-PROTOTYPE-SHARD", False, False, False) or sh["backend_lock"]["status"] != w["lock"]["status"]: out.append("shard against the replay files") scope = [e for e in w["corrections"]["entries"] if e["id"] == "R30-A1-SCOPE-001"] if not scope or scope[0]["status"] != "CLOSED-AS-SCOPE-BOUNDARY" or "backend trust independence OPEN" not in scope[0]["resolution"]: out.append("the correction ledger's scope entry") crystal = gate.squash(w["crystal"]) for frag in ("9278/9278", r"3.54237075\times10^{-9}>0.", "11010110100110101001110111", "PINNED-REPRODUCIBLE-PROTOTYPE/TRUST-AUDIT-OPEN"): if frag not in crystal: out.append(f"crystal: {frag}") w["p1"] = {"density_counts": low_counts, "least": [least["path"], least["margin_decimal"]]} return out def p2_package(w): import re out, v = [], w["validation"] leaves = {row[0]: row for row in w["manifest"]["leaves"]} for key, leaf_id, text in (("round30", 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 (("root_A1_sha256", ROOT_A1), ("marker70_A1_sha256", MARKER_A1), ("lower_A1_sha256", LOWER_A1), ("backend_lock_sha256", LOCK), ("whole_shard_A1_sha256", SHARD_A1), ("correction_ledger_sha256", CORRECTIONS)): if v[key] != leaves[leaf_id][2]: out.append(f"VALIDATION {key} against the archive") rows, sh, lock = w["rows"], w["shard_a1"], w["lock"] kc = {"root_A1_pass": w["root_a1"]["status"] == "PASS" and all(x["round28_overlap"] for x in w["root_a1"]["tmax_checks"].values()), "marker70_A1_pass": w["marker_a1"]["status"] == "PASS" and w["marker_a1"]["marker"]["pass"] is True, "lower_A1_9278": len(rows) == 9278 and all(x["status"] == "A1-PASS" for x in rows), "lower_A1_no_inconclusive": not any(x["status"] == "A1-INCONCLUSIVE" for x in rows), "lower_A1_margin_positive": min(x["margin_decimal"] for x in rows) > 0, "backend_pinned": bool(lock["mpmath"]["libmp_source_hashes"]) and lock["backend_id"].startswith("PINNED"), "backend_trust_open": "TRUST-AUDIT-OPEN" in lock["status"] and sh["backend_lock"]["trust_audit_open"] is True, "not_publication_candidate": sh["publication_candidate"] is False, "not_theorem_ready": sh["theorem_ready"] is False, "no_global_claim": sh["global_lebesgue_claim"] is False} if kc != v["checks"] or v["status"] != "PASS": out.append(f"VALIDATION checks {kc}") w["p2"] = kc return out R30_DEFINITIONS = { "A1-VERIFIED-PINNED-PROTOTYPE": ("in-line", "sec. 18: a second implementation's replay passes and the arithmetic backend's source is pinned"), "A1-INCONCLUSIVE": ("in-line", "sec. 7: a leaf whose membership the second verifier cannot decide at the densities it tries"), "R30-A1-ROOT-001": ("in-line", "sec. 12: the root replay's verifier fix - an exact d* interval cast to binary64 before t_max had " "given a false non-overlap"), "A1-VERIFIED-PINNED-PROTOTYPE-SHARD": ("in-line", "sec. 0, 17: marker 70's whole shard - root, upper, 9278 lower leaves - passing the second " "implementation, the backend pinned, its trust audit open"), "A1-PASS": ("in-line", "sec. 0, 9: a leaf the second implementation certifies"), "PINNED": ("in-line", "sec. 17: the arithmetic backend's versions and source digests locked"), "PINNED-REPRODUCIBLE-PROTOTYPE": ("in-line", "sec. 16: the backend state - locked for reproducibility, not audited"), "TRUST-AUDIT-OPEN": ("in-line", "sec. 16: no independent audit or second-backend replay of the arithmetic yet"), } _ROOT = ("the replay's t3, t5, t7 lie inside Round 28's intervals and this tree's 1e-90 brackets inside both - nested, not only " "overlapping (W1)") _LOWER = ("9278 of 9278 here too at the replay's densities, every margin above the replay's; its own rule rebuilt here gives its " "density and hull count on every leaf (W3)") _MARKER = ("Round 29's audit row for marker 70, field for field, from the same script; an upper bound over the exact area, and " "this tree's own polygon certifies the marker (W2)") _MARKER_A1 = ("the bound holds and this tree's own polygon certifies it (W2), but as sec. 1's second implementation only in part: the " "replay is Round 29's audit script, carrying the emitter's support routine, normals and density - independent in its hull (W2, W5)") _SHARD = ("the lower replay is a second implementation (W3, W5); the upper one is Round 29's audit, independent of the emitter only in its " "hull (W2, W5); the root replay's script is not shipped (W4). Every part passes on this tree's own implementation (W1-W3, W6)") R30_REVIEWS = [ ("PASS", "全部 overlap", "computation", "PASS", _ROOT), ("PASS", "", "computation", "PASS", _MARKER), ("PASS", "overlap", "computation", "PASS", _ROOT), ("PASS", "root", "computation", "PASS", _ROOT), ("PASS", "upper", "computation", "PASS", _MARKER), ("PASS", "9278/9278 lower", "computation", "PASS", _LOWER), ("OPEN", "Independent backend trust", "reading", "PASS", "true of the package - both implementations run on mpmath.iv/libmp (W4, W5); this tree's certificates use none of it (W6)"), ("PUBLICATION-CANDIDATE", "9278 lower leaves full A1", "reading", "PASS", "true: not raised, the backend shared (W4)"), ("PUBLICATION-CANDIDATE", "", "n/a", "n/a", "a state of sec. 18, defined there; not a judgment"), ("ARITHMETICALLY-CLOSED-PROTOTYPE", "", "n/a", "n/a", "a state of sec. 18, defined there; not a judgment"), ("A1-VERIFIED-PINNED-PROTOTYPE", "", "n/a", "n/a", "a state of sec. 18, defined there; not a judgment"), ("PUBLICATION-CANDIDATE-SHARD", "16. Backend trust state", "reading", "PASS", "true: not raised, the trust audit open (W4)"), ("PUBLICATION-CANDIDATE-SHARD", "", "n/a", "n/a", "the goal of sec. 21, its condition stated there; not a judgment"), ("THEOREM-READY", "", "n/a", "n/a", "a state of sec. 18, defined there; not a judgment"), ("A1-INCONCLUSIVE", "7. Directed point membership", "computation", "PASS", "none here either: no candidate refused at any density (W3)"), ("NOT CERTIFIED", "a_{Leb}≥0.835", "reading", "PASS", "true"), ("NOT CERTIFIED", "a_{Leb}≥0.835", "reading", "PASS", "true"), ("R30-A1-ROOT-001", "12. Root A1 verifier bug", "computation", "PASS", "the cause reproduced: d* through binary64 moves 1.7e-17 and puts t3, t5, t7 outside Round 28's intervals; sec. 12's " "width 'about 1e-64' is Round 28's t_n intervals' - the d* intervals are 3.1e-61 (Round 28) and 2.8e-73 (the replay) wide (W1)"), ("A1 PASS", "Root/path", "computation", "PASS", _ROOT), ("A1 PASS", "Marker upper", "computation", "PARTIAL", _MARKER_A1), ("A1 PASS", "B7 lower", "computation", "PASS", _LOWER), ("A1-VERIFIED-PINNED-PROTOTYPE-SHARD", "", "computation", "PARTIAL", _SHARD), ("A1-VERIFIED-PINNED-PROTOTYPE-SHARD", "", "computation", "PARTIAL", _SHARD), ("A1-VERIFIED-PINNED-PROTOTYPE-SHARD", "", "computation", "PARTIAL", _SHARD), ("A1-PASS", "9278/9278", "computation", "PASS", _LOWER), ("PINNED", "Arithmetic backend", "computation", "PASS", "the lock's libmp digests are the stock mpmath 1.3.0's, file for file; its whole-package digest says not how it is " "formed and is not reproduced here (W4)"), ("PINNED-REPRODUCIBLE-PROTOTYPE", "", "computation", "PASS", "reproducible: the lower ledger comes back from its own rule on another implementation, to the hull vertex (W3)"), ("TRUST-AUDIT-OPEN", "", "reading", "PASS", "true: no audit and no second backend in the package (W4)"), ] def r1_registry(w): return registry.completeness(w["registry"], "R30", w["definitions"], w["reviews"]) CHECKS = {"A0": gate.anchors_check(ANCHORS), "W1": w1_root, "W2": w2_marker, "W3": w3_lower, "W4": w4_lock, "W5": w5_code, "W6": w6_backend, "P1": p1_package, "P2": p2_package, "R1": r1_registry} DEPENDS = {"A0": {"text"}, "W1": {"root_a1", "rootrec28", "computed", "corrections", "digests", "root_claim"}, "W2": {"marker_a1", "marker70", "marker_mine", "audit29", "digests", "marker_claim"}, "W3": {"rows", "computed", "winner", "winner_rows", "bulk28", "lower_claim"}, "W4": {"lock", "digests", "code", "local", "lock_claim"}, "W5": {"code", "digests", "manifest", "code_facts"}, "W6": {"backend_claim"}, "P1": {"rows", "chunks", "lower_a1", "shard_a1", "marker_a1", "bulk28", "corrections", "crystal", "lock", "manifest"}, "P2": {"validation", "manifest", "text", "crystal", "rows", "shard_a1", "lock", "root_a1", "marker_a1"}, "R1": {"registry", "definitions", "reviews"}} 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() thin = min(inputs["rows"], key=lambda x: x["margin_decimal"])["path"] lower = computed(inputs["rows"], inputs["key_bytes"]) rule = winner_computed(inputs["rows"], inputs["key_bytes"], {thin, inputs["bulk28"]["minimum_exact_rational_margin_path"], inputs["rows"][0]["path"]}) marker = marker_computed(inputs["marker70"]) def build(): return {**inputs, "computed": lower, "winner": rule, "winner_rows": inputs["rows"], "marker_mine": marker, "registry": registry.load(), "definitions": dict(R30_DEFINITIONS), "reviews": list(R30_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)[:1800]) if not args.drill: return rows, text, lock = inputs["rows"], inputs["text"], inputs["lock"] k_thin = next(k for k, x in enumerate(rows) if x["path"] == thin) k_512 = next(k for k, x in enumerate(rows) if x["density"] == 512) def edit(obj, fn): x = copy.deepcopy(obj) fn(x) return x cases = [ ("K0-unmodified", "control", {}, set()), ("K1-doc-crlf", "control", {"text": text.replace("\n", "\r\n")}, set()), ("K2-lower-keys-sorted", "control", {"lower_a1": json.loads(json.dumps(inputs["lower_a1"], sort_keys=True))}, set()), ("K3-shard-keys-sorted", "control", {"shard_a1": json.loads(json.dumps(inputs["shard_a1"], sort_keys=True))}, set()), ("M1-doc-margin", "mutation", {"text": text.replace(r"3.54237075\times", r"3.54237076\times")}, {"A0"}), ("M2-root-interval", "mutation", {"root_a1": edit(inputs["root_a1"], lambda x: x["tmax_checks"]["t5"].update(recomputed_hi=x["tmax_checks"]["t5"]["recomputed_lo"]))}, {"W1"}), ("M3-root-correction", "mutation", {"corrections": edit(inputs["corrections"], lambda x: x["entries"][0].update(mathematical_claim_changed=True))}, {"W1"}), ("M4-tree-digest", "mutation", {"root_a1": {**inputs["root_a1"], "topology_sha256": "0" * 64}}, {"W1"}), ("M5-marker-area", "mutation", {"marker_a1": edit(inputs["marker_a1"], lambda x: x["marker"].update(outer_area_decimal=x["marker"]["outer_area_decimal"] + 1e-12))}, {"W2", "P1"}), ("M6-marker-input", "mutation", {"marker_a1": {**inputs["marker_a1"], "input_marker_sha256": "0" * 64}}, {"W2"}), ("M7-lower-margin", "mutation", {"rows": edit(rows, lambda x: x[k_thin].update(margin_decimal=3.5e-9))}, {"W3", "P1"}), ("M8-lower-density", "mutation", {"rows": edit(rows, lambda x: x[k_512].update(density=1024))}, {"W3", "P1"}), ("M9-lock-script", "mutation", {"lock": edit(lock, lambda x: x["proof_critical_scripts"].update(lower_A1_script_sha256="0" * 64))}, {"W4"}), ("M10-lock-libmp", "mutation", {"lock": edit(lock, lambda x: x["mpmath"]["libmp_source_hashes"].update({"libmpi.py": "0" * 64}))}, {"W4"}), ("M11-code-claim", "mutation", {"code_facts": {}}, {"W5"}), ("M12-backend-claim", "mutation", {"backend_claim": {**CLAIMS["backend_claim"], "mpmath_in": []}}, {"W6"}), ("M13-chunk-summary", "mutation", {"chunks": edit(inputs["chunks"], lambda x: x[3][1].update(**{"pass": x[3][1]["pass"] - 1}))}, {"P1"}), ("M14-shard-digest", "mutation", {"shard_a1": edit(inputs["shard_a1"], lambda x: x["lift_lower_A1"].update(sha256="0" * 64))}, {"P1"}), ("M15-crystal", "mutation", {"crystal": inputs["crystal"].replace("9278/9278", "9277/9278")}, {"P1"}), ("M16-validation-digest", "mutation", {"validation": {**inputs["validation"], "lower_A1_sha256": "0" * 64}}, {"P2"}), ("M17-validation-check", "mutation", {"validation": {**inputs["validation"], "checks": {**inputs["validation"]["checks"], "backend_trust_open": False}}}, {"P2"}), ("M18-review-dropped", "mutation", {"reviews": list(R30_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-033", "subject": "Round 30: the independent whole-shard replay and the backend lock", "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("R30", "RUN-033", R30_DEFINITIONS, R30_REVIEWS) print(f"registry: {len(R30_DEFINITIONS)} definitions, {len(R30_REVIEWS)} reviews recorded for R30") if __name__ == "__main__": main()