"""RUN-037 - Round 34: replayable rational-hull certificates, and two more publication candidates. Round 34 writes cells 47 and 48's lower certificates as bytes - RHCERT-v0.1: each leaf's hull vertices on a 10^-18 grid, delta- and zigzag-varint coded with a body tag each, in the topology's leaf order, with a random-access index - and replays them by a verifier that reads only the bytes: each vertex inside its tagged core (the mpmath cores quantized outward to a 10^-40 grid), strict convexity, the exact shoelace. 9228/9228 and 9285/9285 pass, and with Round 33's dominance audit both cells become PUBLICATION-CANDIDATE-SHARD; cell 68 gets its mpmath lower and marker 68 its replays. Here both certificates are decoded from the specification alone and every vertex is checked in this tree's own integer-interval enclosures on the intended boxes - no mpmath, no MPFR; cell 68's summary is rebuilt from this tree's certificates; marker 68 against Round 29's file and this tree's certificate. Checks A0 anchors the numbers and formulas below occur in Round 34 as written W1 format sec. 2-5: the headers, the index, the leaf order and each leaf's density and vertex count W2 replay sec. 6-12: every stored vertex in its tagged core here, convexity and the exact area W3 size sec. 11-12, 15: the raw and packaged sizes and their per-vertex rates W4 cell 68 sec. 16: the summary from this tree's certificates under the emitter's start bands W5 marker 68 sec. 16: its replay record, its exact polygon, this tree's certificate W6 stages sec. 13-14, 17-18: the promotion's conditions and the stage counts W7 code what the package ships, read after the rebuild and never run P1 package the manifests, summaries, shard files, economics, dashboard and crystal agree P2 package VALIDATION against the archive; its checks from the data R1 registry Round 34's judgments reviewed Usage: python code/run037_round34_rhcert.py [--drill] [--blind CID] """ import argparse import collections import copy import hashlib import io import json import re import struct import zipfile from fractions import Fraction from multiprocessing import Pool import gate import registry import run008_round05_saturation_gate as r8 import run009_round06_witness_exchange as r9 import run019_round16_global_pilot as r19 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 import run034_round31_mpfr_replay as r34 import run035_round32_bulk_wave as r35 import run036_round33_dominance as r36 from corpus import SOURCES, TREE, source_bytes, walk_sources from run010_round07_minimizer_atlas import d_star, t_text PKG = "main.zip!/AMRAL_LUC_FC_Round_34_Package_v0.1.zip!/" DOC = PKG + "AMRAL_Lebesgue_Finite_Closure_Round_34_RHCERT_Publication_Candidates_v0.1.md" CRYSTAL = PKG + "AMRAL_LUC_FC_State_Crystal_Round_34_v0.1.md" SPEC = PKG + "AMRAL_LUC_FC_Round_34_RHCERT_FORMAT_SPEC.json" SHARD = {n: PKG + f"AMRAL_LUC_FC_Round_34_PUBLICATION_CANDIDATE_SHARD_{n}.json" for n in (47, 48)} PROTO68 = PKG + "AMRAL_LUC_FC_Round_34_ARITHMETIC_PROTOTYPE_SHARD_68.json" DASH = PKG + "AMRAL_LUC_FC_Round_34_COVERAGE_DASHBOARD.json" ECON = PKG + "AMRAL_LUC_FC_Round_34_CERTIFICATE_SIZE_ECONOMICS.json" VALIDATION = PKG + "AMRAL_LUC_FC_Round_34_VALIDATION.json" MARKER68_A1 = PKG + "AMRAL_LUC_FC_Round_34_MARKER68_A1.json" LOWER68 = PKG + "AMRAL_LUC_FC_Round_34_CELL68_LOWER_MIGRATION.json" CERTZIP = {n: f"AMRAL_LUC_FC_Round_34_Cell{n}_RHCert.zip" for n in (47, 48)} CERT = {n: PKG + CERTZIP[n] + "!/" for n in (47, 48)} MARKER68 = r32.REF + "marker_68.json" LOG = TREE / "data" / "gate-logs" / "run037-round34-rhcert.json" MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json" T, T_EXACT, Q = 0.835, Fraction(167, 200), 10 ** 18 CELLS = (47, 48) # ---------------------------------------------------------------- RHCERT-v0.1, decoded from sec. 2-5 and the spec file alone def uvarint(b, i): x = s = 0 while True: c = b[i] i += 1 x |= (c & 0x7F) << s if c < 0x80: return x, i s += 7 def decode(b): """the global header (<8sHBBI: magic, version, coordinate exponent, tag bytes, leaf count), then per leaf a density and a vertex count as uvarints and per vertex zigzag-uvarint deltas and a tag byte; each leaf's starting offset; where the last leaf ends""" magic, version, exp, tagb, count = struct.unpack_from("<8sHBBI", b, 0) i, leaves = struct.calcsize("<8sHBBI"), [] for _ in range(count): start = i dens, i = uvarint(b, i) n, i = uvarint(b, i) x = y = 0 verts = [] for _ in range(n): dx, i = uvarint(b, i) dy, i = uvarint(b, i) x += (dx >> 1) ^ -(dx & 1) y += (dy >> 1) ^ -(dy & 1) verts.append((x, y, b[i])) i += 1 leaves.append((start, dens, verts)) return {"magic": magic.decode(), "version": version, "exponent": exp, "tag_bytes": tagb, "count": count, "end": i}, leaves def decode_index(b): magic, version, count = struct.unpack_from("<8sHI", b, 0) head = struct.calcsize("<8sHI") return {"magic": magic.decode(), "version": version, "count": count, "size_matches": head + 8 * count == len(b)}, list(struct.unpack_from(f"<{count}Q", b, head)) def replay(args): """one leaf, from its bytes: every vertex inside the core its tag names - the disc exactly, a Reuleaux core against this tree's integer-interval enclosure over the intended box - strict convexity at every vertex, and the exact shoelace against 167/200""" verts, box, base = 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])} n = len(verts) turns = [(verts[(k + 1) % n][0] - verts[k][0]) * (verts[(k + 2) % n][1] - verts[k][1]) - (verts[(k + 1) % n][1] - verts[k][1]) * (verts[(k + 2) % n][0] - verts[k][0]) for k in range(n)] refused = sum(not (4 * (x * x + y * y) < Q * Q if t == 0 else t in cores and r30.inside((r30.exact(Fraction(x, Q)), r30.exact(Fraction(y, Q))), *cores[t])) for x, y, t in verts) S = abs(sum(verts[k][0] * verts[(k + 1) % n][1] - verts[(k + 1) % n][0] * verts[k][1] for k in range(n))) return {"convex": min(turns) > 0, "refused": refused, "pass": min(turns) > 0 and not refused and 200 * S > 167 * 2 * Q * Q, "margin": float(Fraction(S, 2 * Q * Q) - T_EXACT)} def replay_compute(certs, cells): scales = r31.root_scales() tn = t_text(7, d_star(r31.TM)) waxes = [a for a, _ in r31.float_sequence(tn, 30)] out = {} with Pool(14) as pool: for n in map(str, CELLS): _, leaves = decode(certs[n]["rhcert"]) m = cells[n]["manifest"] paths = [p for p, internal in r31.decode_topology(cells[n]["topology"], m["nodes"]) if not internal] base = r33.base_cores(r35.cell_box(m["base_path"]), scales) jobs = [] for (_, _, verts), p in zip(leaves, paths): wlo, whi = r31.fractions(p, waxes, 3) jobs.append((verts, r31.directed_box(wlo, whi, r31.WITNESS, scales), base)) out[n] = pool.map(replay, jobs, chunksize=16) return out def replay_computed(certs, cells): """both certificates replayed here from their bytes (the leaf boxes from this tree's root and the shipped topology, the cores from this tree's integer intervals)""" return r35._cached("run037-replay.json", [decode, uvarint, replay, replay_compute, r33.base_cores, r35.cell_box, r8, r9, r19, r30, r31, b"".join(certs[str(n)]["rhcert"] + cells[str(n)]["topology"] for n in CELLS)], lambda: replay_compute(certs, cells)) # ---------------------------------------------------------------- cell 68 and marker 68 def ledger68(lift): """a ledger for cell 68 from this tree's lift: each leaf at the emitter's start band for its slack""" return json.dumps([{"path": p, "density": r35.start_band(a - r30.PKG_PAD - T)} for p, a in lift]).encode() def marker68_computed(m): return r35._cached("run037-marker68.json", [r36.marker_compute, r32.certify, r32.half_planes, r32.outer_area, r32.support_hi, r34.marker_polygons, r34.full_area, r34.package_normals, r8, r9, r19, r30, r31, json.dumps([m["q_rational"], m["final"]["density"]]).encode()], lambda: r36.marker_compute(m)) def load_inputs(): blobs = {n: source_bytes(n) for n in SOURCES} r33ref = r36.REF want = {MARKER68, r33ref + "cell68_topology.bin"} | {r33ref + f"cell{n}_manifest.json" for n in r36.LIFTED} \ | {r33ref + f"cell{n}_{k}" for n in CELLS for k in ("manifest.json", "topology.bin", "mpmath_leaf_ledger.json")} 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() outer = zipfile.ZipFile(io.BytesIO(source_bytes("main.zip"))) pkg = zipfile.ZipFile(io.BytesIO(outer.read(PKG.split("!/")[1]))) certs, cells = {}, {} for n in CELLS: z = pkg.read(CERTZIP[n]) certs[str(n)] = {"rhcert": got[CERT[n] + f"cell{n}.rhcert"], "rhidx": got[CERT[n] + f"cell{n}.rhidx"], "manifest": json.loads(got[CERT[n] + "rhcert_manifest.json"]), "summary": json.loads(got[CERT[n] + "rhcert_replay_summary.json"]), "zip": [len(z), sha(z)], "digests": [sha(got[CERT[n] + f"cell{n}.rhcert"]), sha(got[CERT[n] + f"cell{n}.rhidx"])]} cells[str(n)] = {"manifest": json.loads(got[r33ref + f"cell{n}_manifest.json"]), "topology": got[r33ref + f"cell{n}_topology.bin"], "ledger": json.loads(got[r33ref + f"cell{n}_mpmath_leaf_ledger.json"])} cells["68"] = {"manifest": json.loads(got[r33ref + "cell68_manifest.json"]), "topology": got[r33ref + "cell68_topology.bin"]} return {"text": got[DOC].decode("utf-8"), "crystal": got[CRYSTAL].decode("utf-8"), "spec": json.loads(got[SPEC]), "shards": {str(n): json.loads(got[p]) for n, p in SHARD.items()}, "proto68": json.loads(got[PROTO68]), "dashboard": json.loads(got[DASH]), "economics": json.loads(got[ECON]), "validation": json.loads(got[VALIDATION]), "marker68_a1": json.loads(got[MARKER68_A1]), "lower68": json.loads(got[LOWER68]), "marker68": json.loads(got[MARKER68]), "certs": certs, "cells": cells, "lift_paths": {str(n): json.loads(got[r33ref + f"cell{n}_manifest.json"])["base_path"] for n in r36.LIFTED}, "code": {k[len(PKG):]: v.decode("utf-8") for k, v in got.items() if k.startswith(PKG) and k.endswith(".py")}, "manifest": json.loads(MANIFEST.read_text(encoding="utf-8"))} def world(inputs): c = inputs["cells"] lifts = r36.lifts_computed(inputs["lift_paths"]) return {**inputs, "replay": replay_computed(inputs["certs"], c), "cell68": r35.cell_computed(68, c["68"]["manifest"]["base_path"], ledger68(lifts["68"])), "lift68": lifts["68"], "marker_mine": marker68_computed(inputs["marker68"])} ANCHORS = { "W1": [r"\boxed{\texttt{RHCERT-v0.1}}", r"magic8bytesL34RHC01", r"coordinate_expuint818", r"x=X/10^{18},\qquady=Y/10^{18},", r"uvarintdensityuvarintvertex_countrepeatvertex_count:zigzag-uvarintdelta_xzigzag-uvarintdelta_yuint8source_tag", r"0=diameter-onediskcore1=B3commoncore2=B5commoncore3=B7commoncore", r"L+1"], "W2": [r"Q_C=10^{40}.", r"G_{\rmquantized}\subseteqG_{\rmdirected}.", r"D^2_{\max}0.", r"200|S|>167(2\cdot10^{36}).", r"\boxed{9228/9228\text{leavesPASS}}", r"\boxed{2{,}163{,}069}", r"6.75024723\times10^{-9}>0.", r"\boxed{9285/9285\text{leavesPASS}}", r"\boxed{2{,}109{,}700}", r"1.03164178\times10^{-7}>0."], "W3": [r"rawcertificate：约34.8MiB。", r"rawcertificate：约34.0MiB。", r"36{,}506{,}484.", r"8.1\text{MiB}.", r"35{,}657{,}092\text{bytes}.", r"7.6\text{MiB}.", r"\sim16.88\text{rawbytes/vertex}.", r"\sim16.90\text{rawbytes/vertex}.", r"3.5\text{--}3.9\text{bytes/vertex}."], "W4": [r"\boxed{9255/9255\text{mpmath/libmplowerPASS}}", r"\boxed{2.23292\times10^{-8}.}"], "W6": [r"\boxed{5/77\approx6.49\%.}", r"\boxed{4/77\approx5.19\%.}", r"\boxed{\{47,48,68,69,70\}}", r"\boxed{\{47,48,69,70\}}", r"\boxed{2/77\to4/77.}"], "P1": [r"a_{\mathrm{Leb}}\ge0.835\text{NOTCERTIFIED}."], } CLAIMS = { # [magic, version, exponent, tag bytes, leaves]; the leaves end where the file does; the index [magic, version, L + 1 offsets, # its size, each offset a leaf's start]; the ledger's order is the topology's; the ledger's densities and hull counts "format_claim": {"47": {"header": ["L34RHC01", 1, 18, 1, 9228], "consumed": True, "index": ["L34RHIDX", 1, True, True, True], "order": True, "densities_equal": 9228, "vertices": [9228, 2163069], "tags": [0, 1, 2, 3]}, "48": {"header": ["L34RHC01", 1, 18, 1, 9285], "consumed": True, "index": ["L34RHIDX", 1, True, True, True], "order": True, "densities_equal": 9285, "vertices": [9285, 2109700], "tags": [0, 1, 2, 3]}, "spec": ["<8sHBBI", "L34RHC01", 1, 18, 1, "L34RHIDX", True]}, # every leaf replayed here from its bytes; the least [leaf, path, margin] is the summary's to the bit; margins within 3e-17 # of the Round 32/33 ledgers' "replay_claim": {"47": {"pass": 9228, "convex": 9228, "refused": 0, "least": [4820, "10001101101111110111", 6.75024723062513e-09], "is_summary": [True, True], "to_ledger": 2.6e-17}, "48": {"pass": 9285, "convex": 9285, "refused": 0, "least": [6986, "110101101001101011111010", 1.0316417842561089e-07], "is_summary": [True, True], "to_ledger": 2.7e-17}}, # raw [bytes, per vertex, MiB]; package [bytes, its digest the shard's, per vertex, MiB - sec. 11-12 say 8.1 and 7.6] "size_claim": {"47": {"raw": [36506484, 16.8772, 34.82], "package": [8411289, True, 3.8886, 8.02], "economics": [True, True, True, True, True]}, "48": {"raw": [35657092, 16.9015, 34.01], "package": [7909374, True, 3.7491, 7.54], "economics": [True, True, True, True, True]}}, "cell68_claim": {"leaves": 9255, "decided": 9255, "density_counts": {"256": 820, "512": 3429, "1024": 3632, "2048": 1140, "4096": 181, "8192": 46, "16384": 7}, "least": ["00111011001001010000010", 16384, 2.2329210691926833e-08], "to_summary": [True, 2.6e-17]}, "marker_claim": {"record": [True, True, True, True, True], "every_constraint": [0.8348955547544915, 1317, 22748, 22749], "is_replay": True, "float_reduced": [0.8348955547544915, 1284, 22014, 22015], "is_round29": True, "mine": [128, 9.961572239094077e-05, 0.0001612202817038444], "shard_margin": True}, "stages_claim": {"cells": [[47, 48, 69, 70], [47, 48, 68, 69, 70]], "counts": [True, True, True, True, True, True, True], "geometry": [66, 11, 51], "conditions": {"47": {"bytes_replayed_here": True, "mpfr_marker": "PASS", "mpfr_dominance": "PASS"}, "48": {"bytes_replayed_here": True, "mpfr_marker": "PASS", "mpfr_dominance": "PASS"}}}, "code_facts": {"emit": {"grid": True, "rounds_binary64": True, "starts_at_ledger_density": True, "dps": 90, "reads_unshipped": ["leaves_reference.json", "r26_full77_results"]}, "assemble": {"chunk_index": True, "global_index": True}, "verify": {"dps": 80, "grid40": True, "outward": True, "strict_convexity": True, "root_round28": True, "decimal_into_interval": True}, "lines": {"r34_assemble_rhcert.py": 27, "r34_emit_chunk.py": 146, "r34_verify_chunk.py": 101}}, } def near(a, b, tol): return abs(a - b) <= tol def sig(x, n=4): return float(f"{x:.{n - 1}e}") def w1_format(w): """sec. 2-5 and the spec file: each certificate's header, that the leaves consume it exactly, its index (magic, version, L + 1 offsets, each the start of a leaf), the leaf order (the topology's preorder, the ledger's order) and each leaf's density and vertex count against Round 33's ledger""" out, got, sp = [], {}, w["spec"] for n in map(str, CELLS): c, cell = w["certs"][n], w["cells"][n] head, leaves = decode(c["rhcert"]) ih, offs = decode_index(c["rhidx"]) led = cell["ledger"] paths = [p for p, internal in r31.decode_topology(cell["topology"], cell["manifest"]["nodes"]) if not internal] got[n] = {"header": [head["magic"], head["version"], head["exponent"], head["tag_bytes"], head["count"]], "consumed": head["end"] == len(c["rhcert"]), "index": [ih["magic"], ih["version"], ih["count"] == head["count"] + 1, ih["size_matches"], offs == [s for s, _, _ in leaves] + [head["end"]]], "order": [x["path"] for x in led] == paths, "densities_equal": sum(d == x["density"] for (_, d, _), x in zip(leaves, led)), "vertices": [sum(len(v) == x["vertices"] for (_, _, v), x in zip(leaves, led)), sum(len(v) for _, _, v in leaves)], "tags": sorted({t for _, _, v in leaves for _, _, t in v})} gh = sp["global_header"] got["spec"] = [gh["struct"], gh["magic"], gh["version"], gh["coordinate_scale_exponent"], gh["source_tag_bytes"], sp["index_format"]["magic"], sp["fail_closed"]] ok = all(v["consumed"] and v["index"][2:] == [True, True, True] and v["order"] and v["densities_equal"] == len(w["cells"][n]["ledger"]) and v["vertices"][0] == len(w["cells"][n]["ledger"]) for n, v in got.items() if n != "spec") if not ok or got != w["format_claim"]: out.append(f"the certificates' format: {got}") w["w1"] = got return out def w2_replay(w): """sec. 6-12: this tree's replay of both certificates from their bytes - every vertex in its tagged core under this tree's integer-interval enclosure (no mpmath, no MPFR), strict convexity, the exact area; the least margin and its leaf against the replay summary; the margins against Round 32/33's ledger""" out, got = [], {} for n in map(str, CELLS): res, led, s = w["replay"][n], w["cells"][n]["ledger"], w["certs"][n]["summary"] k = min(range(len(res)), key=lambda i: res[i]["margin"]) got[n] = {"pass": sum(r["pass"] for r in res), "convex": sum(r["convex"] for r in res), "refused": sum(r["refused"] for r in res), "least": [k, led[k]["path"], res[k]["margin"]], "is_summary": [k == s["minimum_margin_leaf_index"], res[k]["margin"] == s["minimum_margin_decimal"]], "to_ledger": sig(max(abs(r["margin"] - x["margin_decimal"]) for r, x in zip(res, led)), 2)} if any(v["pass"] != len(w["cells"][n]["ledger"]) or v["refused"] or not all(v["is_summary"]) for n, v in got.items()) or got != w["replay_claim"]: out.append(f"the replay: {got}") w["w2"] = got return out def w3_size(w): """sec. 11-12, 15: raw bytes and bytes per vertex; the packaged certificates' bytes, digest and bytes per vertex, in MiB against sec. 11-12's round figures""" out, got, e = [], {}, w["economics"]["cells"] for n in map(str, CELLS): c = w["certs"][n] v = c["manifest"]["vertex_count_total"] z = c["zip"] got[n] = {"raw": [len(c["rhcert"]), round(len(c["rhcert"]) / v, 4), round(len(c["rhcert"]) / 2 ** 20, 2)], "package": [z[0], z[1] == w["shards"][n]["certificate_entity"]["compressed_sha256"], round(z[0] / v, 4), round(z[0] / 2 ** 20, 2)], "economics": [e[n]["raw_bytes"] == len(c["rhcert"]), e[n]["zip_bytes"] == z[0], near(e[n]["raw_bytes_per_vertex"], len(c["rhcert"]) / v, 1e-12), near(e[n]["zip_bytes_per_vertex"], z[0] / v, 1e-12), near(e[n]["compression_ratio"], z[0] / len(c["rhcert"]), 1e-12)]} if not all(all(v["economics"]) and v["package"][1] for v in got.values()) or got != w["size_claim"]: out.append(f"the sizes: {got}") w["w3"] = got return out def w4_cell68(w): """sec. 16: cell 68's summary - the density counts and the least margin - from this tree's certificates on this tree's lift: each leaf at the first density that passes from its slack's start band (the emitter's rule, RUN-035)""" out, comp, rec = [], w["cell68"], w["lower68"] start = {p: r35.start_band(a - r30.PKG_PAD - T) for p, a in w["lift68"]} rows = [] for (p, _), r in zip(comp["leaves"], comp["results"]): if r["ledger"]["pass"]: rows.append((p, start[p], r["ledger"]["margin"])) elif r["least"] and r["least"]["n"] > start[p]: rows.append((p, r["least"]["n"], r["least"]["margin"])) else: rows.append((p, None, None)) least = min((x for x in rows if x[2] is not None), key=lambda x: x[2]) got = {"leaves": len(rows), "decided": sum(x[1] is not None for x in rows), "density_counts": {str(k): v for k, v in sorted(collections.Counter(x[1] for x in rows).items(), key=lambda x: x[0] or 0)}, "least": [least[0], least[1], least[2]], "to_summary": [least[0] == rec["minimum_margin_path"], sig(abs(least[2] - rec["minimum_margin_decimal"]), 2)]} if got["decided"] != rec["leaves_total"] or got["density_counts"] != rec["density_counts"] or not got["to_summary"][0] or got["to_summary"][1] > 1e-15 \ or got != w["cell68_claim"]: out.append(f"cell 68: {got}") w["w4"] = got return out def w5_marker(w): """sec. 16: marker 68's replay record against Round 29's file; its exact polygon under the package's normals and ceiling, every constraint kept and float-reduced; this tree's certificate""" out, rec, f, mine = [], w["marker68_a1"], w["marker68"]["final"], w["marker_mine"] poly = mine["polygons"] got = {"record": [rec["cell"] == 68, rec["density"] == f["density"] == rec["full_constraint_count"], rec["outer_area_decimal"] == f["outer_area_decimal"], rec["margin_decimal"] == f["margin_decimal"], rec["pass"] is True], "every_constraint": poly["full"], "is_replay": poly["full"][:2] == [rec["outer_area_decimal"], rec["exact_active_constraints"]], "float_reduced": poly["reduced"], "is_round29": poly["reduced"] == [f["outer_area_decimal"], f["active_constraints"], f["outer_area_num_bits"], f["outer_area_den_bits"]], "mine": [mine["certificate"]["ladder"]["N"], mine["certificate"]["ladder"]["margin"], T - mine["certificate"]["exact"]], "shard_margin": w["proto68"]["marker_upper"]["MPFR_margin_decimal"] == f["margin_decimal"]} if not all(got["record"]) or not got["is_replay"] or not got["is_round29"] or not got["shard_margin"] or got != w["marker_claim"]: out.append(f"marker 68: {got}") w["w5"] = got return out def w6_stages(w): """sec. 13-14, 17-18: the stage counts; and of sec. 14's eight conditions for cells 47 and 48, which hold here - the trees (RUN-035/036), the upper replays (Round 29 and 33 against their files), the bytes and their replay (here, and by this tree's arithmetic) - and which rest on MPFR""" out, d = [], w["dashboard"] ar = d["arithmetic_pipeline"] pc, ac = sorted(ar["publication_candidate_cells"]), sorted(ar["arithmetic_closed_or_better_cells"]) got = {"cells": [pc, ac], "counts": [ar["publication_candidate_count"] == len(pc), ar["arithmetic_closed_or_better_count"] == len(ac), ar["geometry_complete_arithmetic_pending_count"] == d["geometry"]["known_complete"] - len(ac), near(ar["publication_candidate_fraction_global"], len(pc) / 77, 1e-15), near(ar["publication_candidate_fraction_of_geometry_complete"], len(pc) / 66, 1e-15), near(ar["arithmetic_closed_or_better_fraction_global"], len(ac) / 77, 1e-15), near(ar["arithmetic_closed_or_better_fraction_of_geometry_complete"], len(ac) / 66, 1e-15)], "geometry": [d["geometry"]["known_complete"], d["geometry"]["residual"], d["geometry"]["latest_exact_common_budget"]["complete"]], "conditions": {n: {"bytes_replayed_here": all(r["pass"] for r in w["replay"][n]) and not any(r["refused"] for r in w["replay"][n]), "mpfr_marker": w["shards"][n]["marker_upper"]["MPFR_status"], "mpfr_dominance": w["shards"][n]["cross_backend_dominance"]["status"]} for n in map(str, CELLS)}} if not all(got["counts"]) or got != w["stages_claim"]: out.append(f"the stages: {got}") w["w6"] = got return out def w7_code(w): """what the package ships, read after the rebuild and never run: the emitter, the assembler, the verifier""" em, asm, ver = (w["code"][k] for k in ("reference/r34_emit_chunk.py", "reference/r34_assemble_rhcert.py", "reference/r34_verify_chunk.py")) facts = {"emit": {"grid": "Q=10**18" in em, "rounds_binary64": "int(round(float(P[idx,0])*Q))" in em, "starts_at_ledger_density": "hint=int(ledger[i]['density'])" in em, "dps": int(re.search(r"mp\.iv\.dps=(\d+)", em).group(1)), "reads_unshipped": sorted({"leaves_reference.json", "r26_full77_results"} & set(re.findall(r"leaves_reference\.json|r26_full77_results", em)))}, "assemble": {"chunk_index": "struct.pack('<8sHII',b'L34RHCIX'" in em, "global_index": "struct.pack('<8sHI',b'L34RHIDX',1,len(offsets))" in asm}, "verify": {"dps": int(re.search(r"mp\.iv\.dps=(\d+)", ver).group(1)), "grid40": "QC=10**40" in ver, "outward": "def fl(fr):return (fr.numerator*QC)//fr.denominator" in ver and "def ce(fr):return -((-fr.numerator*QC)//fr.denominator)" in ver, "strict_convexity": "orient(pts[j-1],pts[j],pts[(j+1)%nv])<=0" in ver, "root_round28": "AMRAL_LUC_FC_Round_28_ROOT_RECONSTRUCTION.json" in ver, "decimal_into_interval": "mp.iv.mpf([fs(e.lo),fs(e.hi)])" in ver}, "lines": {k.split("/")[-1]: v.count("\n") for k, v in sorted(w["code"].items())}} w["w7"] = facts return [] if facts == w["code_facts"] else [f"the scripts: {facts}"] def p1_package(w): out = [] for n in map(str, CELLS): c, sh = w["certs"][n], w["shards"][n] m, s, ce = c["manifest"], c["summary"], sh["certificate_entity"] if (m["certificate_sha256"], m["index_sha256"], m["certificate_bytes"], m["index_bytes"]) != (c["digests"][0], c["digests"][1], len(c["rhcert"]), len(c["rhidx"])) \ or (s["certificate_sha256"], s["index_sha256"], s["leaf_count"], s["vertex_count_total"], s["density_counts"], s["minimum_margin_decimal"]) \ != (m["certificate_sha256"], m["index_sha256"], m["leaf_count"], m["vertex_count_total"], m["density_counts"], m["minimum_margin_decimal"]) \ or (ce["raw_sha256"], ce["raw_bytes"], ce["index_sha256"], ce["leaf_count"], ce["vertex_count_total"], ce["minimum_margin_decimal"], ce["compressed_bytes"]) \ != (m["certificate_sha256"], m["certificate_bytes"], m["index_sha256"], m["leaf_count"], m["vertex_count_total"], m["minimum_margin_decimal"], c["zip"][0]) \ or m["density_counts"] != {str(k): v for k, v in sorted(collections.Counter(x["density"] for x in w["cells"][n]["ledger"]).items())} \ or (sh["status"], sh["publication_candidate"], sh["global_lebesgue_claim"]) != ("PUBLICATION-CANDIDATE-SHARD", True, False): out.append(f"cell {n}: the manifest, the summary and the shard file") p, lo, mk = w["proto68"], w["lower68"], w["marker68_a1"] if {k: p["lower_mpmath"][k] for k in lo} != lo or p["geometry"] != w["cells"]["68"]["manifest"] or p["marker_upper"]["MPFR_margin_decimal"] != mk["margin_decimal"] \ or (p["status"], p["publication_candidate"]) != ("ARITHMETICALLY-CLOSED-PROTOTYPE", False): out.append("cell 68's prototype file against its migration record, manifest and marker") d = w["dashboard"]["arithmetic_pipeline"] if sorted(d["publication_candidate_cells"]) != [47, 48, 69, 70] or sorted(d["arithmetic_closed_or_better_cells"]) != [47, 48, 68, 69, 70] or w["dashboard"]["global_lebesgue_claim"]: out.append("the dashboard's cells") crystal = gate.squash(w["crystal"]) for frag in ("36{,}506{,}484\\text{bytes}", "35{,}657{,}092\\text{bytes}", "9228/9228\\text{replayPASS}", "9285/9285\\text{replayPASS}", "\\boxed{\\{47,48,69,70\\}}", "Q=10^{18}."): if frag not in crystal: out.append(f"crystal: {frag}") w["p1"] = {"cells": {n: w["certs"][n]["manifest"]["certificate_sha256"][:16] for n in map(str, CELLS)}} return out def p2_package(w): out, v = [], w["validation"] leaves = {row[0]: row for row in w["manifest"]["leaves"]} for key, leaf_id in (("round34_sha256", DOC), ("state_sha256", CRYSTAL), ("format_spec_sha256", SPEC), ("cell47_candidate_sha256", SHARD[47]), ("cell48_candidate_sha256", SHARD[48]), ("cell68_prototype_sha256", PROTO68), ("coverage_sha256", DASH), ("size_economics_sha256", ECON), ("cell47_rhcert_sha256", CERT[47] + "cell47.rhcert"), ("cell48_rhcert_sha256", CERT[48] + "cell48.rhcert")): if v[key] != leaves[leaf_id][2]: out.append(f"VALIDATION {key} against the archive") sh, lo, mk, p, d = w["shards"], w["lower68"], w["marker68_a1"], w["proto68"], w["dashboard"] kc = {"cell47_replay_pass": w["certs"]["47"]["summary"]["status"] == "PASS" and w["certs"]["47"]["summary"]["failures"] == 0, "cell48_replay_pass": w["certs"]["48"]["summary"]["status"] == "PASS" and w["certs"]["48"]["summary"]["failures"] == 0, "cell47_dominance_pass": sh["47"]["cross_backend_dominance"]["status"] == "PASS", "cell48_dominance_pass": sh["48"]["cross_backend_dominance"]["status"] == "PASS", "cell47_pub": sh["47"]["publication_candidate"] is True, "cell48_pub": sh["48"]["publication_candidate"] is True, "cell68_lower_9255": lo["leaves_pass"] == lo["leaves_total"] == 9255, "cell68_marker_a1": mk["pass"] is True, "cell68_marker_mpfr": p["marker_upper"]["MPFR_status"] == "PASS", "pub_count_4": d["arithmetic_pipeline"]["publication_candidate_count"] == 4, "no_global_claim": d["global_lebesgue_claim"] is False} if kc != v["checks"] or v["status"] != "PASS": out.append(f"VALIDATION checks {kc}") w["p2"] = kc return out _REPLAY = ("replayed here from the bytes alone in this tree's integer arithmetic - every vertex in its tagged core, strictly convex, " "the exact area above 167/200 on every leaf; the least margin and its leaf are the summary's, to the bit (W1, W2)") _C68 = ("the summary comes back from this tree's certificates on its own lift under the emitter's start bands: the density counts, " "and the least margin on the same leaf to 1e-16 (W4)") _M68 = "the record is Round 29's file; the full polygon under the package's normals is rebuilt here, 1,317 constraints and its area (W5)" _PC = ("the concrete bytes pass under this tree's own arithmetic as under the package's verifier (W2) - a second backend on the " "certificate itself; the MPFR marker replay and dominance audit are not recomputed here (W6)") R34_REVIEWS = [ ("PASS", "9228/9228 leaves", "computation", "PASS", _REPLAY), ("PASS", "9285/9285 leaves", "computation", "PASS", _REPLAY), ("PASS", "9255/9255 mpmath/libmp lower", "computation", "PASS", _C68), ("PASS", "9255/9255", "computation", "PASS", _C68), ("PASS", "independent exact-polar upper", "computation", "PASS", _M68), ("PASS", "MPFR upper", "computation", "UNMEASURED", "no MPFR record is shipped and MPFR is not on this machine; the polygon it computes is rebuilt here exactly (W5)"), ("ARITHMETICALLY-CLOSED-PROTOTYPE", "", "computation", "PASS", "cell 68's lower and upper hold here (W4, W5)"), ("ARITHMETICALLY-CLOSED-PROTOTYPE", "68 →", "computation", "PASS", "cell 68's lower and upper hold here (W4, W5)"), ("PUBLICATION-CANDIDATE-SHARD", "", "computation", "PASS", _PC), ("PUBLICATION-CANDIDATE-SHARD", "47,48 →", "computation", "PASS", _PC), ("NOT CERTIFIED", "a_{Leb}≥0.835", "reading", "PASS", "true"), ("NOT CERTIFIED", "a_{Leb}≥0.835", "reading", "PASS", "true"), ] def r1_registry(w): return registry.completeness(w["registry"], "R34", w["definitions"], w["reviews"]) CHECKS = {"A0": gate.anchors_check(ANCHORS), "W1": w1_format, "W2": w2_replay, "W3": w3_size, "W4": w4_cell68, "W5": w5_marker, "W6": w6_stages, "W7": w7_code, "P1": p1_package, "P2": p2_package, "R1": r1_registry} DEPENDS = {"A0": {"text"}, "W1": {"certs", "cells", "spec", "format_claim"}, "W2": {"replay", "cells", "certs", "replay_claim"}, "W3": {"certs", "economics", "shards", "size_claim"}, "W4": {"cell68", "lift68", "lower68", "cell68_claim"}, "W5": {"marker68_a1", "marker68", "marker_mine", "proto68", "marker_claim"}, "W6": {"dashboard", "shards", "replay", "cells", "certs", "stages_claim", "replay_claim"}, "W7": {"code", "code_facts"}, "P1": {"certs", "shards", "cells", "proto68", "lower68", "marker68_a1", "dashboard", "crystal"}, "P2": {"validation", "manifest", "certs", "shards", "lower68", "marker68_a1", "proto68", "dashboard"}, "R1": {"registry", "definitions", "reviews"}} def drill_cases(base): text, c, certs = base["text"], base["cells"], base["certs"] def edit(obj, fn): x = copy.deepcopy(obj) fn(x) return x def flip(b, at): return b[:at] + bytes([b[at] ^ 1]) + b[at + 1:] return [ ("K0-unmodified", "control", {}, set()), ("K1-doc-crlf", "control", {"text": text.replace("\n", "\r\n")}, set()), ("K2-economics-keys-sorted", "control", {"economics": json.loads(json.dumps(base["economics"], sort_keys=True))}, set()), ("K3-dashboard-keys-sorted", "control", {"dashboard": json.loads(json.dumps(base["dashboard"], sort_keys=True))}, set()), ("M1-doc-count", "mutation", {"text": text.replace(r"\boxed{2{,}109{,}700}", r"\boxed{2{,}109{,}701}")}, {"A0"}), ("M2-header-exponent", "mutation", {"certs": edit(certs, lambda x: x["47"].update(rhcert=x["47"]["rhcert"][:10] + bytes([17]) + x["47"]["rhcert"][11:]))}, {"W1"}), ("M3-index-offset", "mutation", {"certs": edit(certs, lambda x: x["48"].update(rhidx=flip(x["48"]["rhidx"], 14 + 8 * 100)))}, {"W1"}), ("M4-replay-refused", "mutation", {"replay": edit(base["replay"], lambda x: x["47"][10].update(refused=1, **{"pass": False}))}, {"W2", "W6"}), ("M5-replay-least", "mutation", {"replay": edit(base["replay"], lambda x: x["48"][0].update(margin=1e-8))}, {"W2"}), ("M6-zip-size", "mutation", {"certs": edit(certs, lambda x: x["47"].update(zip=[x["47"]["zip"][0] + 1, x["47"]["zip"][1]]))}, {"W3", "P1"}), ("M7-economics", "mutation", {"economics": edit(base["economics"], lambda x: x["cells"]["48"].update(raw_bytes_per_vertex=16.8))}, {"W3"}), ("M8-cell68-summary", "mutation", {"lower68": edit(base["lower68"], lambda x: x["density_counts"].update({"256": 821}))}, {"W4", "P1"}), ("M9-marker68", "mutation", {"marker68_a1": edit(base["marker68_a1"], lambda x: x.update(outer_area_decimal=0.8348955547544916))}, {"W5"}), ("M10-dashboard", "mutation", {"dashboard": edit(base["dashboard"], lambda x: x["arithmetic_pipeline"].update(geometry_complete_arithmetic_pending_count=62))}, {"W6"}), ("M11-code-claim", "mutation", {"code_facts": {}}, {"W7"}), ("M12-summary-digest", "mutation", {"certs": edit(certs, lambda x: x["47"]["summary"].update(certificate_sha256="0" * 64))}, {"P1"}), ("M13-crystal", "mutation", {"crystal": base["crystal"].replace("9285/9285", "9284/9285")}, {"P1"}), ("M14-validation-digest", "mutation", {"validation": {**base["validation"], "size_economics_sha256": "0" * 64}}, {"P2"}), ("M15-validation-check", "mutation", {"validation": {**base["validation"], "checks": {**base["validation"]["checks"], "cell68_marker_a1": False}}}, {"P2"}), ("M16-review-dropped", "mutation", {"reviews": list(R34_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": {}, "reviews": list(R34_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", "w7", "p1", "p2"): print(key, "=", json.dumps(w.get(key), default=float, ensure_ascii=False)) 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-037", "subject": "Round 34: replayable rational-hull certificates, and two more publication candidates", "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", "w7", "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("R34", "RUN-037", {}, R34_REVIEWS) print(f"registry: {len(R34_REVIEWS)} reviews recorded for R34") if __name__ == "__main__": main()