"""RUN-038 - Round 35: the certificate format in production, and the frontier that was not kept. Round 35 emits cell 68's certificate in RHCERT-v0.1 (35,940,305 bytes, 2,126,336 vertices) and replays it from the bytes - 9255/9255 - which, with Round 33's dominance audit, makes cell 68 the fifth PUBLICATION-CANDIDATE-SHARD; cells 75 and 76 get their mpmath ledgers (10948/10948, 10932/10932), their markers' replays and their dominance audits, and wait for their bytes. It also finds that the geometry continuation's pending boxes were kept only in runtime-local checkpoints, now gone, so that no closure can be resumed from the counts and volumes that survive; it specifies DFRONT-v0.1 to keep them, and claims no new geometry. Here cell 68's bytes are decoded and every vertex checked in this tree's own integer arithmetic; cells 75 and 76 are certified leaf by leaf on this tree's lifts; markers 75 and 76 against Round 29's files and this tree's certificates; the three dominance audits' state counts on this tree's lifts. Checks A0 anchors the numbers and formulas below occur in Round 35 as written W1 format sec. 0, 2: cell 68's certificate - header, index, order, and each leaf's density and hull count against this tree's certificates of cell 68 (RUN-037) W2 replay sec. 0, 2: every stored vertex in its tagged core here, convexity and the exact area W3 cells sec. 0, 3-4: cells 75 and 76 certified on their intended boxes at the ledgers' densities W4 markers sec. 0, 3-4: markers 75 and 76 against Round 29's files and this tree's certificates W5 states sec. 0: the dominance audits' unique witness-core states on this tree's lifts W6 stages sec. 1, 5-7: the stage counts; the geometry kept at 66; the residual records; DFRONT P1 package the shard and status files, the certificate records, the dashboard and the crystal agree P2 package VALIDATION against the archive; its checks from the data R1 registry Round 35's judgments reviewed Usage: python code/run038_round35_rhcert_production.py [--drill] [--blind CID] """ import argparse import collections import copy import hashlib import io import json import re import zipfile 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 import run037_round34_rhcert as r37 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_35_Package_v0.1.zip!/" DOC = PKG + "AMRAL_Lebesgue_Finite_Closure_Round_35_RHCERT_Mass_Production_Durable_Frontiers_v0.1.md" CRYSTAL = PKG + "AMRAL_LUC_FC_State_Crystal_Round_35_v0.1.md" SHARD68 = PKG + "AMRAL_LUC_FC_Round_35_PUBLICATION_CANDIDATE_SHARD_68.json" STATUS = {n: PKG + f"AMRAL_LUC_FC_Round_35_CELL{n}_STATUS.json" for n in (75, 76)} DASH = PKG + "AMRAL_LUC_FC_Round_35_COVERAGE_DASHBOARD.json" DFRONT = PKG + "AMRAL_LUC_FC_Round_35_DFRONT_SPEC.json" RECOVERY = PKG + "AMRAL_LUC_FC_Round_35_GEOMETRY_RECOVERY_LEDGER.json" VALIDATION = PKG + "AMRAL_LUC_FC_Round_35_VALIDATION.json" CERTZIP = "AMRAL_LUC_FC_Round_35_Cell68_RHCert.zip" CERT = PKG + CERTZIP + "!/" REF = PKG + "AMRAL_LUC_FC_Round_35_reference/" DOMINANCE = {n: REF + f"AMRAL_LUC_FC_Round_33_CROSS_BACKEND_DOMINANCE_CELL{n}.json" for n in (68, 75, 76)} MARKERS_A1 = REF + "AMRAL_LUC_FC_Round_35_MARKER75_76_A1.json" MARKERS = {n: r32.REF + f"marker_{n}.json" for n in (75, 76)} LOG = TREE / "data" / "gate-logs" / "run038-round35-rhcert-production.json" MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json" T = 0.835 PAIR = (75, 76) def replay_compute(cert, cell): scales = r31.root_scales() tn = t_text(7, d_star(r31.TM)) waxes = [a for a, _ in r31.float_sequence(tn, 30)] _, leaves = r37.decode(cert) paths = [p for p, internal in r31.decode_topology(cell["topology"], cell["manifest"]["nodes"]) if not internal] base = r33.base_cores(r35.cell_box(cell["manifest"]["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)) from multiprocessing import Pool with Pool(14) as pool: return pool.map(r37.replay, jobs, chunksize=16) def replay_computed(cert, cell): """cell 68's certificate replayed here from its bytes (RUN-037's replay)""" return r35._cached("run038-replay68.json", [r37.decode, r37.uvarint, r37.replay, replay_compute, r33.base_cores, r35.cell_box, r8, r9, r19, r30, r31, cert + cell["topology"]], lambda: replay_compute(cert, cell)) def markers_computed(markers): return r35._cached("run038-markers.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({str(n): [m["q_rational"], m["final"]["density"]] for n, m in sorted(markers.items())}).encode()], lambda: {str(n): r36.marker_compute(m) for n, m in sorted(markers.items())}) def load_inputs(): blobs = {n: source_bytes(n) for n in SOURCES} r33ref = r36.REF want = set(MARKERS.values()) | {r30.PROGRESS} | {r33ref + f"cell{n}_{k}" for n in (68, 75, 76) for k in ("manifest.json", "topology.bin")} 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"))) z = zipfile.ZipFile(io.BytesIO(outer.read(PKG.split("!/")[1]))).read(CERTZIP) cells = {str(n): {"manifest": json.loads(got[r33ref + f"cell{n}_manifest.json"]), "topology": got[r33ref + f"cell{n}_topology.bin"]} for n in (68, 75, 76)} for n in PAIR: cells[str(n)]["ledger"] = json.loads(got[REF + f"cell{n}_mpmath_leaf_ledger.json"]) cells[str(n)]["ledger_bytes"] = got[REF + f"cell{n}_mpmath_leaf_ledger.json"] cells[str(n)]["ledger_sha256"] = sha(got[REF + f"cell{n}_mpmath_leaf_ledger.json"]) return {"text": got[DOC].decode("utf-8"), "crystal": got[CRYSTAL].decode("utf-8"), "shard68": json.loads(got[SHARD68]), "status": {str(n): json.loads(got[p]) for n, p in STATUS.items()}, "dashboard": json.loads(got[DASH]), "dfront": json.loads(got[DFRONT]), "recovery": json.loads(got[RECOVERY]), "validation": json.loads(got[VALIDATION]), "cert": {"rhcert": got[CERT + "cell68.rhcert"], "rhidx": got[CERT + "cell68.rhidx"], "manifest": json.loads(got[CERT + "rhcert_manifest.json"]), "record": json.loads(got[CERT + "AMRAL_LUC_FC_Round_35_CELL68_RHCERT_REPLAY.json"]), "zip": [len(z), sha(z)], "digests": [sha(got[CERT + "cell68.rhcert"]), sha(got[CERT + "cell68.rhidx"])], "copies_equal": [got[CERT + "rhcert_manifest.json"] == got[REF + "rhcert_manifest.json"], got[CERT + "AMRAL_LUC_FC_Round_35_CELL68_RHCERT_REPLAY.json"] == got[REF + "AMRAL_LUC_FC_Round_35_CELL68_RHCERT_REPLAY.json"]]}, "dominance": {str(n): json.loads(got[p]) for n, p in DOMINANCE.items()}, "markers_a1": json.loads(got[MARKERS_A1]), "markers": {n: json.loads(got[p]) for n, p in MARKERS.items()}, "cells": cells, "progress27": json.loads(got[r30.PROGRESS]), "lift_paths": {str(n): cells[str(n)]["manifest"]["base_path"] for n in r36.LIFTED}, "code": sorted(k[len(PKG):] for k in got 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["cert"]["rhcert"], c["68"]), "cert68_mine": r35.cell_computed(68, c["68"]["manifest"]["base_path"], r37.ledger68(lifts["68"])), "computed": {str(n): r35.cell_computed(n, c[str(n)]["manifest"]["base_path"], c[str(n)]["ledger_bytes"]) for n in PAIR}, "marker_mine": markers_computed(inputs["markers"]), "states": {n: r36.unique_states([p for p, _ in v]) for n, v in lifts.items()}} ANCHORS = { "W1": [r"35{,}940{,}305\text{bytes}.", r"\boxed{2{,}126{,}336}"], "W2": [r"\boxed{9255/9255\text{RHCERTbytes-onlyreplayPASS}}", r"\boxed{2.2329\times10^{-8}>0}", r"\boxed{0\text{replayfailures}}."], "W3": [r"\boxed{10948/10948\text{lowerPASS}}", r"\boxed{10932/10932\text{lowerPASS}}", r"-256:848-512:3609-1024:4609-2048:1545-4096:293-8192:36-16384:8", r"\boxed{6.2518\times10^{-8}>0}.", r"-256:853-512:3568-1024:4700-2048:1474-4096:287-8192:44-16384:6", r"\boxed{2.0477\times10^{-8}>0}."], "W4": [r"0.8349344874879304<0.835.", r"0.8349600023952688<0.835."], "W5": [r"\boxed{1565\text{states},\0\text{failures}}", r"\boxed{1690\text{states},\0\text{failures}}.", r"\boxed{1688\text{states},\0\text{failures}}."], "W6": [r"\{47,48,68,69,70,75,76\}", r"\boxed{\{47,48,68,69,70\}}.", r"\boxed{\{75,76\}}.", r"\boxed{5/77\approx6.49\%}.", r"\boxed{7/77\approx9.09\%}.", r"\boxed{66/77}.", r"(\#\mathrm{pending},V_d)\not\Rightarrow\text{frontierreconstruction}.", r"(k_\phi,m_\phi),(k_x,m_x),(k_y,m_y)", r"\left[\frac{m}{2^k},\frac{m+1}{2^k}\right].", r"這不依賴歷史splitorder。"], "P1": [r"a_{\mathrm{Leb}}\ge0.835\text{NOTCERTIFIED}."], } CLAIMS = { # every leaf's density and hull count in the bytes are this tree's own certificate's under the start bands "format_claim": {"header": ["L34RHC01", 1, 18, 1, 9255], "consumed": True, "index": ["L34RHIDX", 1, True, True, True], "my_leaves": True, "densities_equal": 9255, "hull_counts_equal": 9255, "vertices": 2126336}, # the least [leaf, path, margin] and each chunk's are the record's; the margins within 3e-16 of this tree's certificates "replay_claim": {"pass": 9255, "convex": 9255, "refused": 0, "least": [2126, "00111011001001010000010", 2.232921067369829e-08], "is_record": [True, [True, True, True, True]], "to_mine": 2.6e-16}, "cells_claim": { "75": {"paths": True, "pass": 10948, "refused": 0, "hull_equal": 10948, "margin_difference": 2.6e-16, "bands": [10948, 10948], "least": ["11010110100110111101000001111", 16384, 6.251776139778169e-08], "density_counts": {"256": 848, "512": 3609, "1024": 4609, "2048": 1545, "4096": 293, "8192": 36, "16384": 8}}, "76": {"paths": True, "pass": 10932, "refused": 0, "hull_equal": 10932, "margin_difference": 2.2e-16, "bands": [10932, 10932], "least": ["11010110110100101111001110011", 16384, 2.047726726055077e-08], "density_counts": {"256": 853, "512": 3568, "1024": 4700, "2048": 1474, "4096": 287, "8192": 44, "16384": 6}}}, # [area, active, numerator and denominator bits] with every constraint; this tree's certificates [normals, margin, exact margin] "markers_claim": {"75": {"record": [True, True, True, True], "every_constraint": [0.8349344874879304, 1312, 22932, 22932], "is_replay": True, "is_round29": True, "mine": [128, 7.618893728138815e-05, 0.00013790529424184683], "status_margin": True}, "76": {"record": [True, True, True, True], "every_constraint": [0.8349600023952688, 2593, 42978, 42979], "is_replay": True, "is_round29": True, "mine": [128, 1.7451451239390935e-05, 7.873645672273888e-05], "status_margin": True}}, # [states here, the audit's, leaves in the audit, in the manifest, the audit's status, its failures] "states_claim": {"68": [1565, 1565, 9255, 9255, "PASS", 0], "75": [1690, 1690, 10948, 10948, "PASS", 0], "76": [1688, 1688, 10932, 10932, "PASS", 0]}, "stages_claim": {"cells": [[47, 48, 68, 69, 70], [47, 48, 68, 69, 70, 75, 76], [75, 76]], "counts": [True, True, True, True, True, True, True], "geometry": [66, 11, 0, 51], "residual_records_round27s": True, "dfront": ["[(k_phi,m_phi),(k_x,m_x),(k_y,m_y)]", "[m/2^k,(m+1)/2^k] relative to witness-root coordinate interval", True, 9], "recovery": ["GEOMETRY-FRONTIER-RECOVERY-REQUIRED", "Do not infer pending boxes from counts/volumes; carry geometry coverage unchanged."]}, } def near(a, b, tol): return abs(a - b) <= tol def sig(x, n=4): return float(f"{x:.{n - 1}e}") def mine_at_bands(mine, paths): """this tree's certificate of each leaf, in the given order: [density, hull count, margin] at the first density that passes from the leaf's start band (RUN-037's reading of the emitter's rule)""" area = dict((p, a) for p, a in mine["leaves"]) res = {p: r for (p, _), r in zip(mine["leaves"], mine["results"])} out = [] for p in paths: r = res[p] if r["ledger"]["pass"]: out.append((r35.start_band(area[p] - r30.PKG_PAD - T), r["ledger"]["hull"], r["ledger"]["margin"])) elif r["least"]: out.append((r["least"]["n"], r["least"]["hull"], r["least"]["margin"])) else: out.append((None, None, None)) return out def w1_format(w): """sec. 0, 2: cell 68's certificate - its header, that its leaves consume it, its index, the leaf order (the topology's preorder) - and each leaf's density and hull count against this tree's own certificates of cell 68 under the emitter's start bands (RUN-037)""" out, c = [], w["cert"] head, leaves = r37.decode(c["rhcert"]) ih, offs = r37.decode_index(c["rhidx"]) mine = w["cert68_mine"] paths = [p for p, internal in r31.decode_topology(w["cells"]["68"]["topology"], w["cells"]["68"]["manifest"]["nodes"]) if not internal] dens = mine_at_bands(mine, paths) got = {"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"]]], "my_leaves": sorted(p for p, _ in mine["leaves"]) == sorted(paths), "densities_equal": sum(d == m[0] for (_, d, _), m in zip(leaves, dens)), "hull_counts_equal": sum(len(v) == m[1] for (_, _, v), m in zip(leaves, dens)), "vertices": sum(len(v) for _, _, v in leaves)} if not got["consumed"] or got["index"][2:] != [True, True, True] or not got["my_leaves"] or got != w["format_claim"]: out.append(f"cell 68's certificate: {got}") w["w1"] = got return out def w2_replay(w): """sec. 0, 2: every stored vertex of cell 68 in its tagged core under this tree's integer arithmetic, strict convexity, the exact area; the least margin and each chunk's least against the replay record; the margins against this tree's own certificates""" out, res, rec = [], w["replay"], w["cert"]["record"] k = min(range(len(res)), key=lambda i: res[i]["margin"]) chunks = [min(r["margin"] for r in res[ch["start"]:ch["end"]]) == ch["minimum_margin_decimal"] for ch in rec["chunks"]] paths = [p for p, internal in r31.decode_topology(w["cells"]["68"]["topology"], w["cells"]["68"]["manifest"]["nodes"]) if not internal] minem = [m[2] for m in mine_at_bands(w["cert68_mine"], paths)] got = {"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, paths[k], res[k]["margin"]], "is_record": [res[k]["margin"] == rec["minimum_margin_decimal"], chunks], "to_mine": sig(max(abs(a["margin"] - b) for a, b in zip(res, minem)), 2)} if got["pass"] != len(res) or got["refused"] or not got["is_record"][0] or not all(chunks) or got != w["replay_claim"]: out.append(f"cell 68's replay: {got}") w["w2"] = got return out def w3_cells(w): """sec. 0, 3-4: cells 75 and 76's ledgers - their paths this tree's lift, every leaf certified on its intended box at the ledger's density, the hull counts, the margins; the densities the start bands'; the least margin""" out, got = [], {} for n in map(str, PAIR): comp, led = w["computed"][n], w["cells"][n]["ledger"] byp = {x["path"]: x for x in led} area = dict((p, a) for p, a in comp["leaves"]) res = {p: r for (p, _), r in zip(comp["leaves"], comp["results"])} at = {p: r["ledger"] for p, r in res.items()} rule = [x["density"] == (max(r35.start_band(area[x["path"]] - r30.PKG_PAD - T), res[x["path"]]["least"]["n"]) if res[x["path"]]["least"] else None) for x in led if x["path"] in res] least = min(led, key=lambda x: x["margin_decimal"]) got[n] = {"paths": sorted(byp) == sorted(res), "pass": sum(r["pass"] for r in at.values()), "refused": sum(r["failures"] for r in at.values()), "hull_equal": sum(at[p]["hull"] == x["vertices"] for p, x in byp.items() if p in at), "margin_difference": sig(max(abs(at[p]["margin"] - x["margin_decimal"]) for p, x in byp.items() if p in at), 2), "bands": [sum(rule), len(rule)], "least": [least["path"], least["density"], least["margin_decimal"]], "density_counts": {str(k): v for k, v in sorted(collections.Counter(x["density"] for x in led).items())}} if any(not v["paths"] or v["pass"] != len(w["cells"][n]["ledger"]) or v["refused"] or v["hull_equal"] != v["pass"] or v["margin_difference"] > 1e-15 for n, v in got.items()) or got != w["cells_claim"]: out.append(f"cells 75 and 76: {got}") w["w3"] = got return out def w4_markers(w): """sec. 0, 3-4: markers 75 and 76 - the replay rows against Round 29's files, the full polygons under the package's normals (their active counts and areas), the float-reduced ones Round 29's, this tree's certificates""" out, got = [], {} rows = {x["cell"]: x for x in w["markers_a1"]["markers"]} for n in PAIR: rec, f, mine = rows[n], w["markers"][n]["final"], w["marker_mine"][str(n)] poly = mine["polygons"] got[str(n)] = {"record": [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"]], "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"]], "status_margin": w["status"][str(n)]["marker_upper"]["MPFR_margin_decimal"] == f["margin_decimal"]} if any(not all(v["record"]) or not v["is_replay"] or not v["is_round29"] or not v["status_margin"] for v in got.values()) or got != w["markers_claim"]: out.append(f"markers 75 and 76: {got}") w["w4"] = got return out def w5_states(w): """sec. 0: the dominance audits' unique witness-core states (rotation and half-widths) against this tree's lifts of cells 68, 75 and 76; the audits' own MPFR results, recorded, not recomputed""" out, d = [], w["dominance"] got = {n: [w["states"][n], d[n]["unique_witness_core_states"], d[n]["leaf_count"], w["cells"][n]["manifest"]["leaves"], d[n]["status"], d[n]["witness_core_failures"]] for n in ("68", "75", "76")} if any(v[0] != v[1] or v[2] != v[3] for v in got.values()) or got != w["states_claim"]: out.append(f"the audits' states: {got}") w["w5"] = got return out def w6_stages(w): """sec. 1, 5-7: the stage counts; no new geometry, the residual records Round 27's; DFRONT's box codes read""" out, d, rc, df = [], w["dashboard"], w["recovery"], w["dfront"] ar = d["arithmetic_pipeline"] pc, ac = sorted(ar["publication_candidate_cells"]), sorted(ar["arithmetic_closed_or_better_cells"]) recs = {r["cell"]: r for r in w["progress27"]["currently_without_known_complete_edge"]["cells"]} rr = rc["latest_certified_geometry_summary"]["residual_cells"] got = {"cells": [pc, ac, sorted(ar["cross_backend_audited_missing_RHCERT"])], "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"]["round35_new_geometry_closures"], d["geometry"]["latest_exact_common_budget"]["complete"]], "residual_records_round27s": all((recs[r["cell"]]["last_tested_depth"], recs[r["cell"]]["pending"], recs[r["cell"]]["unresolved_volume"], recs[r["cell"]]["ratio_vs_previous"]) == (r["last_depth"], r["pending"], r["unresolved_volume"], r["ratio_vs_previous"]) for r in rr) and len(rr) == 11, "dfront": [df["box_code"]["entry"], df["box_code"]["axis_semantics"], df["box_code"]["scheduler_independent"], len(df["checkpoint_required"])], "recovery": [rc["status"], rc["soundness_action"]]} if not all(got["counts"]) or not got["residual_records_round27s"] or got != w["stages_claim"]: out.append(f"the stages: {got}") w["w6"] = got return out def p1_package(w): out, c, sh = [], w["cert"], w["shard68"] m, rec, ce = c["manifest"], c["record"], 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 (rec["certificate_sha256"], rec["leaf_count"], rec["vertex_count_total"], rec["minimum_margin_decimal"], rec["failures"]) \ != (m["certificate_sha256"], m["leaf_count"], m["vertex_count_total"], m["minimum_margin_decimal"], 0) \ or [ch["start"] for ch in rec["chunks"]] != [0] + [ch["end"] for ch in rec["chunks"][:-1]] or rec["chunks"][-1]["end"] != m["leaf_count"] \ or min(ch["minimum_margin_decimal"] for ch in rec["chunks"]) != rec["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"], ce["compressed_sha256"]) \ != (m["certificate_sha256"], m["certificate_bytes"], m["index_sha256"], m["leaf_count"], m["vertex_count_total"], m["minimum_margin_decimal"], c["zip"][0], c["zip"][1]) \ or not all(c["copies_equal"]) or sh["geometry"] != w["cells"]["68"]["manifest"] or (sh["status"], sh["publication_candidate"]) != ("PUBLICATION-CANDIDATE-SHARD", True): out.append("cell 68: the manifest, the replay record and the shard file") for n in map(str, PAIR): s, led = w["status"][n], w["cells"][n]["ledger"] least = min(led, key=lambda x: x["margin_decimal"]) lm = s["lower_mpmath"] if (lm["leaves_total"], lm["leaves_pass"], lm["leaves_inconclusive"], lm["minimum_margin_decimal"], lm["minimum_margin_path"], lm["ledger_sha256"], lm["density_counts"]) \ != (len(led), sum(x["status"] == "PASS" for x in led), sum(x["status"] != "PASS" for x in led), least["margin_decimal"], least["path"], w["cells"][n]["ledger_sha256"], {str(k): v for k, v in collections.Counter(x["density"] for x in led).items()}) \ or s["geometry"] != w["cells"][n]["manifest"] or s["cross_backend_dominance"]["unique_witness_core_states"] != w["dominance"][n]["unique_witness_core_states"] \ or (s["status"], s["publication_candidate"]) != ("CROSS-BACKEND-ENCLOSURE-AUDITED-PROTOTYPE", False): out.append(f"cell {n}: the status file against its ledger, manifest and audit") ar = w["dashboard"]["arithmetic_pipeline"] if sorted(ar["publication_candidate_cells"]) != [47, 48, 68, 69, 70] or sorted(ar["cross_backend_audited_missing_RHCERT"]) != [75, 76] or w["dashboard"]["global_lebesgue_claim"]: out.append("the dashboard's cells") crystal = gate.squash(w["crystal"]) for frag in (r"\boxed{\{47,48,68,69,70\}}", r"\boxed{\{47,48,68,69,70,75,76\}}", "-9255RHCERTleaves-2,126,336vertices", "MPFRdominance1565states/0failures", "`DFRONT-v0.1`"): if frag not in crystal: out.append(f"crystal: {frag}") w["p1"] = {"package": c["zip"], "chunks": len(c["record"]["chunks"])} 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 (("round35", 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 (("cell68_candidate_sha256", SHARD68), ("cell75_status_sha256", STATUS[75]), ("cell76_status_sha256", STATUS[76]), ("dashboard_sha256", DASH), ("dfront_sha256", DFRONT), ("recovery_sha256", RECOVERY)): if v[key] != leaves[leaf_id][2]: out.append(f"VALIDATION {key} against the archive") if v["cell68_rhcert_zip_sha256"] != w["cert"]["zip"][1]: out.append("VALIDATION cell68_rhcert_zip_sha256 against the package") sh, st, d = w["shard68"], w["status"], w["dashboard"] ok = lambda led: all(x["status"] == "PASS" for x in led) kc = {"cell68_rhcert_9255": w["cert"]["manifest"]["leaf_count"] == 9255, "cell68_replay_pass": w["cert"]["record"]["status"] == "PASS" and w["cert"]["record"]["failures"] == 0, "cell68_dominance_pass": sh["cross_backend_dominance"]["status"] == "PASS", "cell68_promoted": sh["publication_candidate"] is True, "cell75_all_pass": ok(w["cells"]["75"]["ledger"]), "cell76_all_pass": ok(w["cells"]["76"]["ledger"]), "cell75_upper_dom": st["75"]["marker_upper"]["MPFR_status"] == "PASS" and st["75"]["cross_backend_dominance"]["status"] == "PASS", "cell76_upper_dom": st["76"]["marker_upper"]["MPFR_status"] == "PASS" and st["76"]["cross_backend_dominance"]["status"] == "PASS", "publication_count_5": d["arithmetic_pipeline"]["publication_candidate_count"] == 5, "arith_count_7": d["arithmetic_pipeline"]["arithmetic_closed_or_better_count"] == 7, "geometry_66": d["geometry"]["known_complete"] == 66, "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 _UP = ("the independent replay's full polygon is rebuilt here - its active count and area (W4); the MPFR replay's record is not " "shipped and MPFR is not on this machine") _LOW = "every leaf certified here on this tree's own lift at the ledger's density, the ledger's hull counts, margins to a few units in the last place (W3)" R35_REVIEWS = [ ("PASS", "9255/9255 RHCERT bytes-only replay", "computation", "PASS", "replayed here from the bytes in this tree's integer arithmetic - every vertex in its tagged core, convex, the exact area; the least " "margin and each chunk's are the record's, and every density and hull count is this tree's own certificate's (W1, W2)"), ("PASS", "10948/10948 lower", "computation", "PASS", _LOW), ("PASS", "10932/10932 lower", "computation", "PASS", _LOW), ("PASS", "marker independent upper + MPFR upper", "computation", "PARTIAL", _UP), ("PASS", "marker independent upper + MPFR upper", "computation", "PARTIAL", _UP), ("PUBLICATION-CANDIDATE-SHARD", "cell68 →", "computation", "PASS", "the bytes pass under this tree's arithmetic (W2) and its upper holds (RUN-037); the MPFR dominance is not recomputed here"), ("NOT CERTIFIED", "a_{Leb}≥0.835", "reading", "PASS", "true"), ] def r1_registry(w): return registry.completeness(w["registry"], "R35", w["definitions"], w["reviews"]) CHECKS = {"A0": gate.anchors_check(ANCHORS), "W1": w1_format, "W2": w2_replay, "W3": w3_cells, "W4": w4_markers, "W5": w5_states, "W6": w6_stages, "P1": p1_package, "P2": p2_package, "R1": r1_registry} DEPENDS = {"A0": {"text"}, "W1": {"cert", "cert68_mine", "cells", "format_claim"}, "W2": {"replay", "cert", "cert68_mine", "cells", "replay_claim"}, "W3": {"computed", "cells", "cells_claim"}, "W4": {"markers_a1", "markers", "marker_mine", "status", "markers_claim"}, "W5": {"dominance", "states", "cells", "states_claim"}, "W6": {"dashboard", "recovery", "dfront", "progress27", "stages_claim"}, "P1": {"cert", "shard68", "status", "cells", "dominance", "dashboard", "crystal"}, "P2": {"validation", "manifest", "text", "crystal", "cert", "shard68", "status", "dashboard", "cells"}, "R1": {"registry", "definitions", "reviews"}} def drill_cases(base): text, c, cert = base["text"], base["cells"], base["cert"] def edit(obj, fn): x = copy.deepcopy(obj) fn(x) return x return [ ("K0-unmodified", "control", {}, set()), ("K1-doc-crlf", "control", {"text": text.replace("\n", "\r\n")}, set()), ("K2-dashboard-keys-sorted", "control", {"dashboard": json.loads(json.dumps(base["dashboard"], sort_keys=True))}, set()), ("K3-shard-keys-sorted", "control", {"shard68": json.loads(json.dumps(base["shard68"], sort_keys=True))}, set()), ("M1-doc-states", "mutation", {"text": text.replace(r"\boxed{1688\text{ states}", r"\boxed{1689\text{ states}")}, {"A0"}), ("M2-index-offset", "mutation", {"cert": edit(cert, lambda x: x.update(rhidx=x["rhidx"][:14 + 8 * 50] + bytes([x["rhidx"][14 + 8 * 50] ^ 1]) + x["rhidx"][15 + 8 * 50:]))}, {"W1"}), ("M3-replay-refused", "mutation", {"replay": edit(base["replay"], lambda x: x[20].update(refused=2, **{"pass": False}))}, {"W2"}), ("M4-record-chunk", "mutation", {"cert": edit(cert, lambda x: x["record"]["chunks"][1].update(minimum_margin_decimal=2.8e-7))}, {"W2"}), ("M5-ledger-margin", "mutation", {"cells": edit(c, lambda x: x["75"]["ledger"][30].update(margin_decimal=x["75"]["ledger"][30]["margin_decimal"] + 1e-12))}, {"W3"}), ("M6-ledger-density", "mutation", {"cells": edit(c, lambda x: x["76"]["ledger"][40].update(density=2 * x["76"]["ledger"][40]["density"]))}, {"W3", "P1"}), ("M7-marker-row", "mutation", {"markers_a1": edit(base["markers_a1"], lambda x: x["markers"][1].update(exact_active_constraints=2594))}, {"W4"}), ("M8-audit-states", "mutation", {"dominance": edit(base["dominance"], lambda x: x["75"].update(unique_witness_core_states=1691))}, {"W5", "P1"}), ("M9-dashboard-count", "mutation", {"dashboard": edit(base["dashboard"], lambda x: x["arithmetic_pipeline"].update(geometry_complete_arithmetic_pending_count=60))}, {"W6"}), ("M10-recovery-record", "mutation", {"recovery": edit(base["recovery"], lambda x: x["latest_certified_geometry_summary"]["residual_cells"][2].update(pending=74433))}, {"W6"}), ("M11-shard-bytes", "mutation", {"shard68": edit(base["shard68"], lambda x: x["certificate_entity"].update(compressed_bytes=8041560))}, {"P1"}), ("M12-crystal", "mutation", {"crystal": base["crystal"].replace("1565 states", "1566 states")}, {"P1"}), ("M13-validation-digest", "mutation", {"validation": {**base["validation"], "dfront_sha256": "0" * 64}}, {"P2"}), ("M14-validation-check", "mutation", {"validation": {**base["validation"], "checks": {**base["validation"]["checks"], "geometry_66": False}}}, {"P2"}), ("M15-review-dropped", "mutation", {"reviews": list(R35_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(R35_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)) 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-038", "subject": "Round 35: the certificate format in production, and the frontier that was not kept", "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("R35", "RUN-038", {}, R35_REVIEWS) print(f"registry: {len(R35_REVIEWS)} reviews recorded for R35") if __name__ == "__main__": main()