"""RUN-014 - Round 11: global atlas partition and certificate sharding. Round 11 turns the proof state into a complete prefix-free frontier of seed boxes: a seed may be replaced by its two children at any time (Thm 5.1), any complete frontier covers the root (Thm 4.1), shards that partition it can be verified apart and merged (Thm 8.1), and a forest of S roots has N = 2L - S nodes. Shards are bound by SHA-256 of a canonical payload and a Merkle root. The reference run splits Round 10's four base leaves into three shards. Here the combinatorics are tested on random frontiers, the reference shards are checked against Round 10's certificate (replayed in RUN-013), their digests are re-derived, sec. 19's depth forecast is tested at the global root, and the facts about Mishra's code are read at the commit his paper pins. Checks A0 anchors the formulas and numbers below occur in Round 11 as written X1 repository Mishra's forest identity check, seed depth 22 and re-queued DFS stacks W1 frontier sec. 2-5, 8: prefix-free and complete (Kraft sum 1); replacement keeps both; a complete frontier's boxes cover the root; a partition into shards covers it W2 forest sec. 10-11: N = 2L - S; replacing a seed by k descendants adds k - 1 roots W3 reference sec. 25-28: the frontier and its shards; the seed boxes are Round 10's base leaves; the certificates are Round 10's bytes; the counts; RUN-013's replay W4 binding sec. 12-13: each payload digest and the Merkle root re-derived W5 forecast sec. 19: the depth forecast at the global root, against the seed inside it P1 package GLOBAL_SHARD_SPEC against the text; the reference manifests against sec. 30-31 P2 package the package's self-description of its files matches the archive R1 registry Round 11's judgments reviewed, first-used statuses defined Usage: python code/run014_round11_global_shards.py [--refresh] [--drill] [--blind CID] """ import argparse import datetime import hashlib import json import math import re import numpy as np import gate import registry from corpus import SOURCES, TREE, source_bytes, walk_sources from run009_round06_witness_exchange import hull_pieces from run010_round07_minimizer_atlas import COMMIT, REPO from run012_round09_adaptive_atlas import R5, base_pieces, root_box, tau_star from run013_round10_reference_dry_run import base_leaves PKG = "main.zip!/AMRAL_LUC_FC_Round_11_Package_v0.1.zip!/" REF = PKG + "AMRAL_LUC_FC_Round_11_reference_shards/" DOC = PKG + "AMRAL_Lebesgue_Finite_Closure_Round_11_Global_Shards_v0.1.md" CRYSTAL = PKG + "AMRAL_LUC_FC_State_Crystal_Round_11_v0.1.md" VALIDATION = PKG + "AMRAL_LUC_FC_Round_11_VALIDATION.json" SPEC = PKG + "AMRAL_LUC_FC_Round_11_GLOBAL_SHARD_SPEC.json" GLOBAL = REF + "global_manifest.json" MERGE = REF + "merge_verification_summary.json" SHARDS = {s: REF + f"shards/{s}.json" for s in ("shard-A", "shard-B", "shard-C")} R10_CERT = "main.zip!/AMRAL_LUC_FC_Round_10_Package_v0.1.zip!/AMRAL_LUC_FC_Round_10_reference_cert/" SNAPSHOT = TREE / "data" / "external" / "round11-repository.json" ROUND07 = TREE / "data" / "external" / "round07-citations.json" RUN013 = TREE / "data" / "gate-logs" / "run013-round10-reference-dry-run.json" LOG = TREE / "data" / "gate-logs" / "run014-round11-global-shards.json" MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json" T1 = 0.835 ANCHORS = { "W1": [r"B(p)\subseteqB(p0)\cupB(p1).", r"B(\epsilon)\subseteq\bigcup_{p\in\mathcalP}B(p).", r"\mathcalP'=(\mathcalP\setminus\{p\})\cup\{p0,p1\}.", r"\mathcalP=\bigsqcup_{a=1}^s\mathcalP_a,"], "W2": [r"N=2L-S.", r"2L-n_{\rmseed}=N", r"S=|\mathcalP_{\rmfinal}|."], "W3": [r"\mathcalP=\{00,01,10,11\}.", r"\{00,11\}", r"2(5688)-4=11372=N.", r"N_A=2833+2853=5686,", r"L_A=1417+1427=2844.", r"2L_A-2=5686.", r"N_B=2853,", r"L_B=1427.", r"2L_B-1=2853.", r"N_C=2833,", r"L_C=1417.", r"2L_C-1=2833."], "W5": [r"r_{\rmpred}(C)=\max\left\{0,\left\lceil\log_2\frac{S(C)}{\tau_\star(m,T)}\right\rceil\right\}.", r"theorem-derivedupper-depthforecast", r"|t_3|\le0.194856180909,", r"|t_5|\le0.197820670401."], "X1": [r"d=22", r"2^{22}"], } REPO_FACTS = { # short phrases only, from the files at the pinned commit "src/verifyB.py": {"forest_identity": r"if 2\*leaves - nseed != nodes:", "forest_report": r"forest identity 2L - nseed"}, "src/certemitB.py": {"seed_depth": r"depth = int\(sys\.argv\[4\]\) if len\(sys\.argv\) > 4 else 22"}, "src/certgen.py": {"requeue": r"RETURNS ITS UNFINISHED\s+DFS STACK, which is re-queued"}, } SEC30 = ["program_id", "round", "target", "root_domain_hash", "split_policy_hash", "arithmetic_policy_hash", "witness_catalog_hash", "shard_id", "shard_status", "seed_entries", "payload_sha256"] SEC30_SEED = ["seed_path", "seed_box_hash", "certificate_hash", "nodes", "leaves", "worst_slack"] SEC31 = ["global_root_hash", "target", "proof_policy_version", "frontier_seed_paths", "shards", "shard_merkle_root", "verifier_requirements"] SEC22 = { # sec. 22's merge checklist, and the spec's wording of each item "global manifest hash": None, "target and policy agree": None, "frontier prefix-free": "frontier prefix-free", "frontier complete": "frontier complete", "every seed exactly once": "every terminal seed exactly once", "shard payload hashes": "shard hash valid", "Merkle root": "Merkle root valid", "seed root boxes": "seed box identity valid", "seed certificates": "every seed certificate verifies", "per-shard forest identity": "per-shard forest identity", "global forest identity": "global forest identity", "no expanded, failed or unresolved terminal state": "no pending/expanded/failed terminal state", "verifier and arithmetic compatibility": "arithmetic policy compatible"} # ---------------------------------------------------------------- frontiers def prefix_free(P): return not any(p != q and q.startswith(p) for p in P for q in P) def complete(P): """a finite prefix-free set of binary paths is complete exactly when its Kraft sum is 1""" return prefix_free(P) and sum(2.0 ** -len(p) for p in P) == 1.0 def complete_by_descent(P, limit=64): """the text's definition, read directly: from the root, stop at a frontier path, else both children must go on and meet the frontier""" def ok(p): if p in P: return True if len(p) >= limit or not any(q.startswith(p) for q in P): return False return ok(p + "0") and ok(p + "1") return prefix_free(P) and ok("") def random_frontier(rng, steps, replace): P = {""} for _ in range(steps): p = sorted(P)[int(rng.integers(0, len(P)))] P = replace(P, p) return P def box_of(path, center, half, axes): """the box of a path under a fixed cyclic split order: bit 0 the lower half""" c, h = np.array(center, dtype=float), np.array(half, dtype=float) for i, b in enumerate(path): a = axes[i % len(axes)] h[a] /= 2 c[a] += (2 * int(b) - 1) * h[a] return c, h # ---------------------------------------------------------------- digests def canonical(payload): return json.dumps(payload, sort_keys=True, separators=(",", ":")) def merkle(hex_hashes, odd="duplicate", as_text=False): """sorted leaves; a parent is SHA-256 of its two children's bytes (or, as_text, of their hex strings); an odd node is paired with itself, or promoted""" level = sorted(hex_hashes) if as_text else [bytes.fromhex(h) for h in sorted(hex_hashes)] join = (lambda a, b: hashlib.sha256((a + b).encode()).hexdigest()) if as_text \ else (lambda a, b: hashlib.sha256(a + b).digest()) while len(level) > 1: if len(level) % 2 and odd == "duplicate": level = level + [level[-1]] nxt = [join(level[i], level[i + 1]) for i in range(0, len(level) - 1, 2)] if len(level) % 2: nxt.append(level[-1]) level = nxt return level[0] if as_text else level[0].hex() # ---------------------------------------------------------------- checks def x1_repository(w): out, facts = [], w["snapshot"]["facts"] for path, names in REPO_FACTS.items(): for name in names: if not facts.get(path, {}).get(name): out.append(f"{path}: {name} not found at the pinned commit") if w["mishra_seed_depth"] != 22 or "22" not in (facts.get("src/certemitB.py", {}).get("seed_depth") or ""): out.append(f"Mishra's default seed depth is not {w['mishra_seed_depth']}") return out def w1_frontier(w): out, rng = [], np.random.default_rng(111) replace = w["replace"] for k in range(200): P = random_frontier(rng, int(rng.integers(0, 40)), replace) if not (complete(P) and complete_by_descent(P)): out.append(f"frontier {k}: replacement left an incomplete or non-prefix-free frontier") break # coverage: the boxes of a complete frontier cover the root; with a random partition into shards too c0, h0 = root_box() for k in range(20): P = sorted(random_frontier(rng, int(rng.integers(1, 30)), replace)) boxes = [box_of(p, c0, h0, (2, 3, 4, 0, 1)) for p in P] labels = rng.integers(0, 3, len(P)) shards = [[b for b, l in zip(boxes, labels) if l == s] for s in range(3)] pts = c0 + rng.uniform(-1, 1, (400, 5)) * h0 inside = lambda b, x: bool(np.all(np.abs(x - b[0]) <= b[1] * (1 + 1e-12))) if not all(sum(inside(b, x) for b in boxes) >= 1 for x in pts): out.append(f"frontier {k}: a root point outside every frontier box") break if not all(any(inside(b, x) for s in shards for b in s) for x in pts): out.append(f"frontier {k}: a root point outside every shard") break return out def node_count(leaves): """the nodes of a binary tree given by its leaf paths: every prefix of a leaf""" return len({l[:i] for l in leaves for i in range(len(l) + 1)}) def w2_forest(w): out, rng = [], np.random.default_rng(113) split = lambda P, p: (P - {p}) | {p + "0", p + "1"} for _ in range(200): S = int(rng.integers(1, 8)) trees = [random_frontier(rng, int(rng.integers(0, 30)), split) for _ in range(S)] L, N = sum(len(t) for t in trees), sum(node_count(t) for t in trees) if N != w["forest"](L, S): out.append(f"{S} trees, {L} leaves: {N} nodes, the identity gives {w['forest'](L, S)}") break # sec. 11: cut the first tree at depth d; the subtrees below the cut become roots t, d = trees[0], int(rng.integers(0, 6)) cut = {l[:d] for l in t} subs = [{l[len(f):] for l in t if l.startswith(f)} for f in cut] S2 = S - 1 + len(subs) N2 = N - node_count(t) + sum(node_count(s) for s in subs) if N2 != w["forest"](L, S2): out.append(f"after a reshard into {len(subs)} roots: {N2} nodes, the identity gives {w['forest'](L, S2)}") break return out def w3_reference(w): out, g = [], w["global"]["payload"] P = g["frontier_seed_paths"] if not complete(set(P)) or len(P) != len(set(P)): out.append(f"the reference frontier {P} is not complete and prefix-free") seeds = [s for sh in g["shards"] for s in sh["seed_paths"]] if sorted(seeds) != sorted(P) or len(seeds) != len(set(seeds)): out.append(f"the shards' seeds {seeds} do not partition the frontier") leaves = base_leaves(g["root_base_domain"]["center"], g["root_base_domain"]["halfwidth"]) r10 = {c["base_cell_id"]: c for c in w["r10_manifest"]["lift_certificates"]} r10_summary = {p["base_cell_id"]: p for p in w["r10_summary"]["per_leaf"]} merged = {p["shard_id"]: p for p in w["merge"]["per_shard"]} totals, rows = [0, 0], {} for sh in g["shards"]: payload = w["shards"][sh["shard_id"]]["payload"] n = l = 0 worst = math.inf for e in payload["seed_entries"]: k = e["seed_path"] c, h = leaves[k] if np.max(np.abs(np.array(e["base_center"]) - c)) > 1e-18 or list(h) != e["base_halfwidth"]: out.append(f"{sh['shard_id']} seed {k}: its box is not Round 10's base leaf {k}") data = w["shard_bins"][e["lift_certificate_file"]] if hashlib.sha256(data).hexdigest() != e["lift_certificate_sha256"] or data != w["r10_bins"][k] \ or e["lift_certificate_sha256"] != r10[k]["sha256"]: out.append(f"{sh['shard_id']} seed {k}: the certificate is not Round 10's") if (e["nodes"], e["leaves"], e["max_depth"]) != (r10[k]["nodes"], r10[k]["leaves"], r10[k]["max_depth"]): out.append(f"{sh['shard_id']} seed {k}: counts differ from Round 10's") if w["run013"]["w3"]["trees"][k]["exact_failures"] != 0: out.append(f"seed {k}: RUN-013's replay found failing leaves") n, l, worst = n + e["nodes"], l + e["leaves"], min(worst, r10_summary[k]["worst_verified_slack"]) S = len(payload["seed_entries"]) rows[sh["shard_id"]] = (S, n, l) if n != w["forest"](l, S): out.append(f"{sh['shard_id']}: {n} nodes, {l} leaves, {S} seeds") m = merged[sh["shard_id"]] if (m["seed_count"], m["nodes"], m["leaves"]) != (S, n, l) or m["worst_verified_slack"] != worst: out.append(f"{sh['shard_id']}: the merge summary's row differs from its seeds") if tuple(w["shard_table"][sh["shard_id"]]) != (S, n, l): out.append(f"{sh['shard_id']}: the text's counts {w['shard_table'][sh['shard_id']]} differ from {(S, n, l)}") totals[0], totals[1] = totals[0] + n, totals[1] + l if (w["merge"]["total_nodes"], w["merge"]["total_leaves"]) != tuple(totals) \ or totals[0] != w["forest"](totals[1], len(P)): out.append(f"global counts {totals} with {len(P)} seeds") w["w3"] = {"shards": rows, "totals": totals} return out def w4_binding(w): out, g = [], w["global"] for sid, doc in w["shards"].items(): if hashlib.sha256(w["canonical"](doc["payload"]).encode()).hexdigest() != doc["payload_sha256"]: out.append(f"{sid}: its payload digest is not SHA-256 of the canonical payload") listed = next(s for s in g["payload"]["shards"] if s["shard_id"] == sid) if listed["payload_sha256"] != doc["payload_sha256"]: out.append(f"{sid}: the global manifest lists another digest") if hashlib.sha256(w["canonical"](g["payload"]).encode()).hexdigest() != g["payload_sha256"]: out.append("the global manifest's own digest does not match its payload") hashes = [s["payload_sha256"] for s in g["payload"]["shards"]] root = w["merkle"](hashes) if root != g["payload"]["shard_merkle_root"] or root != w["merge"]["shard_merkle_root"]: out.append("the Merkle root does not re-derive") others = {"odd node promoted": merkle(hashes, odd="promote"), "hex strings concatenated": merkle(hashes, as_text=True)} collision = merkle(hashes + [max(hashes)]) == merkle(hashes) w["w4"] = {"other_readings_reproduce": {k: v == g["payload"]["shard_merkle_root"] for k, v in others.items()}, "largest_shard_repeated_same_root": collision} return out def w5_forecast(w): out = [] c0, h0 = root_box() area = hull_pieces(base_pieces(c0), 2048)[0] m = area - T1 S0 = max(math.hypot(h0[0], h0[1]), math.hypot(h0[3], h0[4]) + R5 * h0[2]) r_pred = max(0, math.ceil(math.log2(S0 / tau_star(m, T1)))) if m > 0 else None seed = np.array(w["round07"]["repository"]["reuleaux"]["placement"], dtype=float) seed[2] %= 2 * math.pi / 5 inside = bool(np.all(np.abs(seed - c0) <= h0)) seed_area = hull_pieces(base_pieces(seed), 2048)[0] bound = r_pred is None or not (inside and seed_area < T1) # a finite forecast over a cell that never closes if bound != w["forecast_is_upper_bound"]: out.append(f"the root's forecast is {r_pred} cycles; the seed inside it has base area {seed_area:.7f}") w["w5"] = {"root_centre_base_area": area, "root_margin": m, "S0": S0, "forecast_cycles": r_pred, "seed_inside_root": inside, "seed_base_area": seed_area} return out def p1_package(w): out, spec, g = [], w["spec"], w["global"]["payload"] if spec["target"] != T1 or spec["terminal_shard_states"] != ["COMPLETE"] \ or not {"FAILED", "UNRESOLVED"} <= set(spec["forbidden_final_states"]): out.append("the spec's target or shard states differ from sec. 21") if spec["production_seed_identity"]["preferred"] != "explicit_axis_side_path": out.append("the spec does not prefer sec. 14's Mode B") merge_missing = sorted(k for k, v in SEC22.items() if v not in spec["global_merge_checks"]) if merge_missing != sorted(w["spec_merge_missing"]): out.append(f"the spec's merge checks leave out {merge_missing}, recorded {w['spec_merge_missing']}") shard_keys = set(w["shards"]["shard-A"]["payload"]) | {"payload_sha256"} seed_keys = set(w["shards"]["shard-A"]["payload"]["seed_entries"][0]) renamed = {"certificate_hash": "lift_certificate_sha256", "seed_box_hash": "base_center"} missing30 = sorted(f for f in SEC30 if f not in shard_keys) + sorted( f"seed_entries.{f}" for f in SEC30_SEED if f not in seed_keys and renamed.get(f) not in seed_keys) missing31 = sorted(f for f in SEC31 if f not in g and not (f == "global_root_hash" and "root_base_domain" in g)) if sorted(missing30) != sorted(w["shard_missing"]) or missing31 != sorted(w["global_missing"]): out.append(f"the reference leaves out {missing30} and {missing31}; recorded {w['shard_missing']}, {w['global_missing']}") w["p1"] = {"shard_fields_missing": sorted(missing30), "global_fields_missing": missing31, "spec_merge_checks_missing": merge_missing} return out def p2_package(w): out, leaves = [], {row[0]: row for row in w["manifest"]["leaves"]} v = w["validation"] for rec, leaf_id, text in ((v["round11"], DOC, w["text"]), (v["state_crystal"], CRYSTAL, w["crystal"])): _, size, digest = leaves[leaf_id] if rec["sha256"] != digest or rec["bytes"] != size: out.append(f"{rec['file']}: recorded sha256/bytes differ from the archive") n = text.count("$$") if rec["double_dollar_count"] != n or rec["double_dollar_even"] != (n % 2 == 0): out.append(f"{rec['file']}: recorded {rec['double_dollar_count']} $$, document has {n}") if rec["contains_unicode_escape_sequence"] != bool(re.search(r"\\u[0-9a-fA-F]{4}", text)): out.append(f"{rec['file']}: unicode-escape flag differs") if rec["contains_bracket_math_delimiter"] != bool(re.search(r"\\[\[\]()]", text)): out.append(f"{rec['file']}: bracket-delimiter flag differs") if v["global_spec_sha256"] != leaves[SPEC][2]: out.append("global_spec_sha256: recorded digest differs from the archive") if v["reference_merge_summary"] != w["merge"]: out.append("VALIDATION's copy of the merge summary differs from the reference's") return out # ---------------------------------------------------------------- registry (Round 11) TOKEN = "a shard or ledger state of sec. 19-24 or C11-5, defined there; not a judgment" R11_DEFINITIONS = { "IMPLEMENTED": ("contextual", "sec. 39: built and exercised on the reference shards; not a theorem"), "COMPLETE": ("in-line", "sec. 21: a shard whose every terminal seed has a complete certificate"), "EXPANDED": ("in-line", "sec. 21: a shard that claims nothing and returns a complete descendant frontier"), "ACTIVE/HARD": ("in-line", "sec. 19: a cell without a positive representative margin, given no depth forecast"), "FAILED": ("in-line", "sec. 21: invalid geometry, an arithmetic failure, a corrupt stream or an inconsistent root"), "GLOBAL-CERTIFICATE-CANDIDATE": ("in-line", "C11-5: what a global merge may output once nothing is pending and " "every shard passes; still before an arithmetic audit"), } R11_REVIEWS = [ ("PROVED", "Prefix-free frontier theorem", "analytic", "PASS", "Thm 4.1 by induction on the frontier tree; W1"), ("PROVED", "Frontier replacement invariant", "analytic", "PASS", "Thm 5.1; the Kraft sum is unchanged (W1)"), ("PROVED", "Shard partition theorem", "analytic", "PASS", "Thm 8.1; only 'no missing seed' is needed for soundness, the rest is bookkeeping (W1)"), ("PROVED", "Global forest identity", "analytic", "PASS", "each full binary tree has 2L - 1 nodes; W2; Mishra's " "verifyB.py checks the same (X1)"), ("PASS", "Reference shard replay", "computation", "PASS", "W3: the shards partition Round 10's frontier and carry its bytes; RUN-013 replayed every leaf"), ("CLOSED", "SHARDED CERTIFICATE ARCHITECTURE", "reading", "PARTIAL", "the theorems hold, but a second verifier cannot rebuild the digests or the lift boxes from the text and " "manifests alone: the canonical JSON form, the Merkle odd-level rule, and the lift split's tie-break and child " "order are only in code, and the reference shards carry none of sec. 30's policy hashes (W4, P1; RUN-013)"), ("COMPUTE-DEFERRED", "Global 0.835 heavy run", "n/a", "n/a", ""), ("COMPUTE-DEFERRED", "GLOBAL 0.8350 HEAVY RUN", "n/a", "n/a", "sec. 0's boxed summary; read from census v3 on (RUN-003)"), ("IMPLEMENTED", "Content-addressed shard binding", "computation", "PASS", "W4: SHA-256 of the payload as compact JSON with sorted keys; the form is not stated in the text"), ("IMPLEMENTED", "Merkle root binding", "computation", "PASS", "W4: sorted leaves, parents hash the children's bytes, an odd node is paired with itself; so repeating the " "largest shard leaves the root unchanged, and sec. 22's 'exactly once' check is what catches it"), ("REJECTED", "24. Shard ancestry", "n/a", "n/a", TOKEN), ("COMPLETE", "", "n/a", "n/a", TOKEN), ("COMPLETE", "`FAILED`", "n/a", "n/a", TOKEN), ("CORRECTED", "24. Shard ancestry", "n/a", "n/a", TOKEN), ("EXPANDED", "", "n/a", "n/a", TOKEN), ("ACTIVE/HARD", "19. Difficulty forecast from Round 09", "n/a", "n/a", TOKEN), ("FAILED", "", "n/a", "n/a", TOKEN), ("GLOBAL-CERTIFICATE-CANDIDATE", "C11-5 — Global merge", "n/a", "n/a", TOKEN), ] def r1_registry(w): return registry.completeness(w["registry"], "R11", w["definitions"], w["reviews"]) # ---------------------------------------------------------------- world, checks, drill CHECKS = {"A0": gate.anchors_check(ANCHORS), "X1": x1_repository, "W1": w1_frontier, "W2": w2_forest, "W3": w3_reference, "W4": w4_binding, "W5": w5_forecast, "P1": p1_package, "P2": p2_package, "R1": r1_registry} DEPENDS = {"A0": {"text"}, "X1": {"snapshot", "mishra_seed_depth"}, "W1": {"replace"}, "W2": {"forest"}, "W3": {"global", "shards", "merge", "r10_manifest", "r10_summary", "r10_bins", "shard_bins", "run013", "forest", "shard_table"}, "W4": {"global", "shards", "merge", "canonical", "merkle"}, "W5": {"round07", "forecast_is_upper_bound"}, "P1": {"spec", "global", "shards", "spec_merge_missing", "shard_missing", "global_missing"}, "P2": {"validation", "text", "crystal", "manifest", "merge"}, "R1": {"registry", "definitions", "reviews"}} CLAIMS = { "mishra_seed_depth": 22, "replace": lambda P, p: (P - {p}) | {p + "0", p + "1"}, "forest": lambda L, S: 2 * L - S, "shard_table": {"shard-A": (2, 5686, 2844), "shard-B": (1, 2853, 1427), "shard-C": (1, 2833, 1417)}, "canonical": canonical, "merkle": merkle, "forecast_is_upper_bound": False, "spec_merge_missing": ["global manifest hash", "target and policy agree"], "shard_missing": ["arithmetic_policy_hash", "program_id", "root_domain_hash", "round", "shard_status", "split_policy_hash", "witness_catalog_hash", "seed_entries.worst_slack"], "global_missing": ["proof_policy_version", "verifier_requirements"], } def load_inputs(): blobs = {n: source_bytes(n) for n in SOURCES} r10_bins = {k: R10_CERT + f"lift_{k}.bin" for k in ("00", "01", "10", "11")} want = {DOC, CRYSTAL, VALIDATION, SPEC, GLOBAL, MERGE, *SHARDS.values(), R10_CERT + "manifest.json", R10_CERT + "verification_summary.json", *r10_bins.values()} want |= {REF + f"source/AMRAL_LUC_FC_Round_10_reference_cert/lift_{k}.bin" for k in r10_bins} got = {leaf.id: d for leaf, d in walk_sources(blobs, keep=lambda l: l.id in want) if d is not None} shard_bins = {f"source/AMRAL_LUC_FC_Round_10_reference_cert/lift_{k}.bin": got[REF + f"source/AMRAL_LUC_FC_Round_10_reference_cert/lift_{k}.bin"] for k in r10_bins} return {"text": got[DOC].decode("utf-8"), "crystal": got[CRYSTAL].decode("utf-8"), "validation": json.loads(got[VALIDATION]), "spec": json.loads(got[SPEC]), "global": json.loads(got[GLOBAL]), "merge": json.loads(got[MERGE]), "shards": {s: json.loads(got[p]) for s, p in SHARDS.items()}, "r10_manifest": json.loads(got[R10_CERT + "manifest.json"]), "r10_summary": json.loads(got[R10_CERT + "verification_summary.json"]), "r10_bins": {k: got[p] for k, p in r10_bins.items()}, "shard_bins": shard_bins, "manifest": json.loads(MANIFEST.read_text(encoding="utf-8"))} def fetch_repository_facts(): facts = {} for path, pats in REPO_FACTS.items(): src = gate.fetch_github_file(REPO, COMMIT, path) found = {name: re.search(p, src) for name, p in pats.items()} facts[path] = {name: (re.sub(r"\s+", " ", m.group(0)) if m else None) for name, m in found.items()} return {"retrieved": datetime.date.today().isoformat(), "repo": REPO, "commit": COMMIT, "facts": facts} def main(): ap = argparse.ArgumentParser() ap.add_argument("--refresh", action="store_true") ap.add_argument("--drill", action="store_true") ap.add_argument("--blind", metavar="CID") args = ap.parse_args() if args.refresh or not SNAPSHOT.exists(): SNAPSHOT.write_text(json.dumps(fetch_repository_facts(), ensure_ascii=False, indent=1) + "\n", encoding="utf-8") snapshot = json.loads(SNAPSHOT.read_text(encoding="utf-8")) inputs = load_inputs() round07 = json.loads(ROUND07.read_text(encoding="utf-8")) run013 = json.loads(RUN013.read_text(encoding="utf-8")) def build(): return {**{k: (json.loads(json.dumps(v)) if isinstance(v, (dict, list)) and k not in ("r10_bins", "shard_bins") else v) for k, v in inputs.items()}, "snapshot": json.loads(json.dumps(snapshot)), "round07": round07, "run013": run013, "registry": registry.load(), "definitions": dict(R11_DEFINITIONS), "reviews": list(R11_REVIEWS), **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 ("w3", "w4", "w5", "p1"): print(key, w.get(key)) if not args.drill: return g, table = inputs["global"], CLAIMS["shard_table"] cases = [ ("K0-unmodified", "control", {}, set()), ("K1-doc-crlf", "control", {"text": inputs["text"].replace("\n", "\r\n")}, set()), ("K2-forest-rewritten", "control", {"forest": lambda L, S: L + (L - S)}, set()), ("K3-replacement-as-union", "control", {"replace": lambda P, p: {q for q in P if q != p} | {p + b for b in "01"}}, set()), ("M1-doc-shard-count", "mutation", {"text": inputs["text"].replace("2L_B-1=2853", "2L_B-1=2835") .replace("2L_B\n-\n1\n=\n2853", "2L_B\n-\n1\n=\n2835")}, {"A0"}), ("M2-seed-depth", "mutation", {"mishra_seed_depth": 20}, {"X1"}), ("M3-replacement-drops-a-child", "mutation", {"replace": lambda P, p: (P - {p}) | {p + "0"}}, {"W1"}), ("M4-forest-single-root", "mutation", {"forest": lambda L, S: 2 * L - 1}, {"W2", "W3"}), ("M5-seed-in-two-shards", "mutation", {"global": {**g, "payload": {**g["payload"], "shards": [ {**s, "seed_paths": s["seed_paths"] + ["01"]} if s["shard_id"] == "shard-C" else s for s in g["payload"]["shards"]]}}}, {"W3", "W4"}), # the manifest's own digest no longer matches ("M6-text-shard-count", "mutation", {"shard_table": {**table, "shard-A": (2, 5686, 2845)}}, {"W3"}), ("M7-unsorted-canonical", "mutation", {"canonical": lambda p: json.dumps(p, separators=(",", ":"))}, {"W4"}), ("M8-merkle-odd-promoted", "mutation", {"merkle": lambda hs: merkle(hs, odd="promote")}, {"W4"}), ("M9-forecast-claimed-a-bound", "mutation", {"forecast_is_upper_bound": True}, {"W5"}), ("M10-shard-fields-assumed", "mutation", {"shard_missing": []}, {"P1"}), ("M11-spec-merge-checks-complete", "mutation", {"spec_merge_missing": []}, {"P1"}), ("M12-spec-digest", "mutation", {"validation": {**inputs["validation"], "global_spec_sha256": "0" * 64}}, {"P2"}), ("M13-review-dropped", "mutation", {"reviews": list(R11_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-014", "subject": "Round 11: global atlas partition and certificate sharding", "document": DOC, "snapshot_retrieved": snapshot["retrieved"], "checks": {c: {"pass": not f, "failures": f} for c, f in results.items()}, **{k: w.get(k) for k in ("w3", "w4", "w5", "p1")}, "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("R11", "RUN-014", R11_DEFINITIONS, R11_REVIEWS) print(f"registry: {len(R11_DEFINITIONS)} definitions, {len(R11_REVIEWS)} reviews recorded for R11") if __name__ == "__main__": main()