"""RUN-035 - Round 32: the first bulk migration wave, and three more closures. Round 32 splits progress into stages. Geometry: cells 31, 27 and 7 close at depths 42, 44 and 46, so 66 of 77 cells are known strict-complete (the common budget stays 51 at depth 36). Arithmetic: cell 69 - marker 70's sibling - gets its explicit tree (15,711 nodes, 7,856 leaves), an mpmath lower ledger, an MPFR ledger in which one leaf needed 65,536 directions, and marker 69's MPFR upper, and becomes the second PUBLICATION-CANDIDATE-SHARD; cell 47 gets its tree (18,455 nodes, 9,228 leaves) and an mpmath ledger, and becomes ARITHMETICALLY-CLOSED-PROTOTYPE. Here the three cells are continued from RUN-030's frontier at 40; cells 69 and 47 are lifted again and every leaf certified on its intended box; cell 69's MPFR ledger is rebuilt from its own rule; markers 69 and 47 against Round 29's files and this tree's certificates. Checks A0 anchors the numbers and formulas below occur in Round 32 as written W1 geometry sec. 1: cells 31, 27 and 7 continued from depth 40 (RUN-030's frontier) to 46 W2 topology sec. 2, 6: cells 69 and 47 lifted here to depth 30 against their trees and manifests W3 emitter sec. 3, 6: every leaf certified on its intended box at the ledger's density; the start bands W4 cross sec. 4: cell 69's MPFR ledger against its rule rebuilt here, to 65,536 directions W5 markers sec. 5-6: markers 69 and 47 against Round 29's files and this tree's certificates W6 dashboard sec. 0, 7-9: the stage counts and the residual records from W1-W5 and the earlier rounds W7 code what the package ships, read after the rebuild and never run P1 package the shard files, the ledgers, the manifests, the dashboard and the crystal agree P2 package VALIDATION against the archive; its checks from the data R1 registry Round 32's judgments reviewed Usage: python code/run035_round32_bulk_wave.py [--drill] [--blind CID] """ import argparse import collections import copy import hashlib import inspect import json import math import re 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 run011_round08_conditional_lift as r11 import run012_round09_adaptive_atlas as r12 import run013_round10_reference_dry_run as r13 import run019_round16_global_pilot as r19 import run023_round20_mixed_escalation as r23 import run027_round24_residual_joint as r27 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 from corpus import SOURCES, TREE, source_bytes, walk_sources from run010_round07_minimizer_atlas import d_star, t_text from run030_round27_interval_replay import ONE PKG = "main.zip!/AMRAL_LUC_FC_Round_32_Package_v0.1.zip!/" DOC = PKG + "AMRAL_Lebesgue_Finite_Closure_Round_32_Bulk_Migration_Wave_v0.1.md" CRYSTAL = PKG + "AMRAL_LUC_FC_State_Crystal_Round_32_v0.1.md" DASH = PKG + "AMRAL_LUC_FC_Round_32_COVERAGE_DASHBOARD.json" SHARD69 = PKG + "AMRAL_LUC_FC_Round_32_PUBLICATION_CANDIDATE_SHARD_69.json" SHARD47 = PKG + "AMRAL_LUC_FC_Round_32_ARITHMETIC_PROTOTYPE_SHARD_47.json" POLICY = PKG + "AMRAL_LUC_FC_Round_32_BULK_MIGRATION_POLICY.json" VALIDATION = PKG + "AMRAL_LUC_FC_Round_32_VALIDATION.json" REF = PKG + "AMRAL_LUC_FC_Round_32_reference/" MARKERS = {n: r32.REF + f"marker_{n}.json" for n in (47, 69)} LOG = TREE / "data" / "gate-logs" / "run035-round32-bulk-wave.json" CACHE = TREE / "data" / "cache" MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json" T, T_EXACT = 0.835, Fraction(167, 200) CELLS = (69, 47) CLOSED = {31: 42, 27: 44, 7: 46} LADDER = (512, 1024, 2048, 4096, 8192, 16384, 32768, 65536) ESCALATED = "011000100000100101100" def cell_box(path): c, h = r23.box(path) return {"path": path, "center": [float(x) for x in c], "half": [float(x) for x in h]} def _cached(name, parts, fn): digest = hashlib.sha256() for p in parts: digest.update(p if isinstance(p, bytes) else inspect.getsource(p).encode() if callable(p) else open(p.__file__, "rb").read()) return r33._cached(CACHE / name, digest.hexdigest(), fn) # ---------------------------------------------------------------- cells 69 and 47: lift and certificates (RUN-031's) def cell_computed(n, path, ledger_bytes): """cell n lifted here to depth 30 (RUN-030's lift under the package's pad) and every leaf certified on its intended box at the ledger's density and on the ladder (RUN-031's migration), with the kernel scan""" ledger = json.loads(ledger_bytes) return _cached(f"run035-cell{n}.json", [cell_box, r31.compute, r8, r9, r11, r12, r13, r19, r23, r27, r30, r31, ledger_bytes, path.encode()], lambda: r31.compute(cell_box(path), ledger)) def winner(args): """RUN-033's rule-rebuild, the ladder carried to 65,536""" c, h, wc, wh, box, base, top = args centres, halves = box cores = {1: base[0], 2: base[1], 3: r31.core_iv(7, centres[0], centres[1], centres[2], [x[1] for x in halves])} rows = [] for n in LADDER: if n > top: break cand = r33.winner_candidates(c, h, wc, wh, n, r31.INWARD) verified = [(x, y) for x, y, b in cand if (Fraction(x) ** 2 + Fraction(y) ** 2 < Fraction(1, 4) if b == 0 else r30.inside((r30.exact(x), r30.exact(y)), *cores[b]))] area, vertices = r30.exact_hull_area(verified) rows.append({"n": n, "failures": len(cand) - len(verified), "hull": vertices, "margin": float(area - T_EXACT), "pass": len(verified) == len(cand) and area > T_EXACT}) if rows[-1]["pass"]: break return rows def winner_compute(path, rows): cell = cell_box(path) scales = r31.root_scales() base = r33.base_cores(cell, scales) tn = t_text(7, d_star(r31.TM)) seq = r31.float_sequence(tn, 30) waxes = [a for a, _ in seq] jobs = [] for row in rows: wc, wh = r31.float_box(row["path"], seq, tn) wlo, whi = r31.fractions(row["path"], waxes, 3) jobs.append((cell["center"], cell["half"], wc, wh, r31.directed_box(wlo, whi, r31.WITNESS, scales), base, row["density"])) with Pool(14) as pool: return pool.map(winner, jobs, chunksize=16) def winner_computed(path, ledger_bytes): """cell 69's MPFR ledger's rule - per direction the union winner's point only - on this tree's contact points and intended boxes, from 512 up to the ledger's density for each path""" return _cached("run035-winner69.json", [cell_box, winner, winner_compute, r33.winner_candidates, r33.base_cores, r33.contact_sets, r8, r9, r11, r12, r13, r19, r23, r30, r31, ledger_bytes, path.encode()], lambda: winner_compute(path, json.loads(ledger_bytes))) # ---------------------------------------------------------------- cells 31, 27 and 7 from depth 40 (RUN-030's frontier) def geometry_compute(): inp = r30.load_inputs() comp = r30.computed_all(inp) path = {c["cell"]: c["path"] for c in inp["ledger"]["cells"]} boxes = {a["path"]: a for a in comp["atlas"]["atlas"]} out = {} with Pool(14) as pool: for n in sorted(CLOSED): lift = comp["residual"][path[n]] a = boxes[path[n]] out[str(n)] = r30.resume(pool, a["center"], a["half"], lift, r30.DEEP, max(CLOSED.values()), r30.PKG_PAD) return out def geometry_computed(): """the three cells continued from RUN-030's boxes open at 40, each split and lifted on to 46 under the package's pad: per depth (nodes, closed, open, least slack closed there). Reads RUN-029's and RUN-030's caches""" return _cached("run035-geometry.json", [geometry_compute, r30.resume, r30.split_sequence, r30.computed_all, r27, r30], geometry_compute) # ---------------------------------------------------------------- markers 69 and 47 def marker_compute(markers): out = {} for n, m in sorted(markers.items()): q = [Fraction(x) for x in m["q_rational"]] out[str(n)] = {"certificate": r32.certify((q, m["final"]["density"])), "polygons": r34.marker_polygons(m) if n == 69 else None} return out def markers_computed(markers): """RUN-032's certificate for markers 69 and 47, and marker 69's exact polygon under the package's normals and ceiling (RUN-034's): with every constraint, float-reduced, adjacent arcs counted""" return _cached("run035-markers.json", [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 markers.items()}).encode()], lambda: marker_compute(markers)) def load_inputs(): blobs = {n: source_bytes(n) for n in SOURCES} want = set(MARKERS.values()) | {r30.PROGRESS, r32.AUDIT, r29_ledger()} 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() cells = {} for n in CELLS: cells[str(n)] = {"manifest": json.loads(got[REF + f"cell{n}_manifest.json"]), "topology": got[REF + f"cell{n}_topology.bin"], "axes": got[REF + f"cell{n}_axis_stream_2bit.bin"], "mpmath": json.loads(got[REF + f"cell{n}_mpmath_leaf_ledger.json"]), "mpmath_bytes": got[REF + f"cell{n}_mpmath_leaf_ledger.json"], "digests": {k: sha(got[REF + f"cell{n}_{k}"]) for k in ("topology.bin", "axis_stream_2bit.bin", "mpmath_leaf_ledger.json")}} cells["69"]["mpfr"] = json.loads(got[REF + "cell69_mpfr_leaf_ledger.json"]) cells["69"]["mpfr_bytes"] = got[REF + "cell69_mpfr_leaf_ledger.json"] cells["69"]["digests"]["mpfr_leaf_ledger.json"] = sha(got[REF + "cell69_mpfr_leaf_ledger.json"]) return {"text": got[DOC].decode("utf-8"), "crystal": got[CRYSTAL].decode("utf-8"), "dashboard": json.loads(got[DASH]), "shard69": json.loads(got[SHARD69]), "shard47": json.loads(got[SHARD47]), "policy": json.loads(got[POLICY]), "validation": json.loads(got[VALIDATION]), "cells": cells, "markers": {n: json.loads(got[p]) for n, p in MARKERS.items()}, "progress27": json.loads(got[r30.PROGRESS]), "audit29": json.loads(got[r32.AUDIT]), "ledger26": json.loads(got[r29_ledger()]), "code": {k[len(REF):]: v.decode("utf-8") for k, v in got.items() if k.startswith(REF) and k.endswith(".py")}, "digests": {k[len(REF):]: sha(v) for k, v in got.items() if k.startswith(REF) and k.endswith(".py")}, "manifest": json.loads(MANIFEST.read_text(encoding="utf-8"))} def r29_ledger(): import run029_round26_full_atlas as r29 return r29.LEDGER def world(inputs, with_geometry=True): c = inputs["cells"] return {**inputs, "computed": {n: cell_computed(int(n), c[n]["manifest"]["base_path"], c[n]["mpmath_bytes"]) for n in c}, "winner": winner_computed(c["69"]["manifest"]["base_path"], c["69"]["mpfr_bytes"]), "marker_mine": markers_computed(inputs["markers"]), "atlas40": r34.atlas_facts() if with_geometry else None, "geometry": geometry_computed() if with_geometry else None} ANCHORS = { "W1": [r"-cell31：depth42；-cell27：depth44；-cell7：depth46。", r"9.43\times10^{-10}\to1.34\times10^{-10}\to1.93\times10^{-12}\to0.", r"\Gamma(38)\ge57,\\Gamma(40)\ge63,\\Gamma(42)\ge64,\\Gamma(44)\ge65,\\Gamma(46)\ge66.", r"\boxed{\Gamma_{B_7}(36)=51/77}."], "W2": [r"\boxed{15711\text{nodes}}", r"\boxed{7856\text{terminalleaves}}", r"explicittopology/split-axisstream与原geometryledger一致。", r"18455\text{nodes},\qquad9228\text{leaves},"], "W3": [r"\boxed{7856/7856\text{PASS}}.", r"\boxed{1.6525\times10^{-9}>0}.", r"\boxed{9228/9228\text{PASS}}.", r"\boxed{6.7502\times10^{-9}>0}."], "W4": [r"011000100000100101100", r"A-167/200\approx-3.07\times10^{-9}.", r"32768\to65536.", r"A-167/200\approx2.5329\times10^{-9}>0.", r"\boxed{7856/7856\text{MPFRPASS}}.", r"\text{increasefinitecertificatedensity}\to\text{increasearithmeticprecision}\to\text{onlythengeometryresplit}."], "W5": [r"0.8349723974082344<0.835.", r"2.76026\times10^{-5}."], "W6": [r"\boxed{66/77}", r"\boxed{11}", r"\boxed{66/77\approx85.71\%}.", r"\text{Publication-Candidate}=2/77", r"\text{Arithmetic-Closed-or-Better}=3/77.", r"\text{GeometryCompletebutArithmeticPending}=63", r"\text{GeometryResidual}=11.", r"=2/77\approx2.60\%.", r"2/66\approx3.03\%.", r"47,48,68,75,76."], "P1": [r"a_{\mathrm{Leb}}\ge0.835\text{NOTCERTIFIED}."], } CLAIMS = { # the three close at 42, 43 and 45 - at the even checkpoints 42, 44 and 46 of sec. 1 - so 64, 65 and 66 by 42, 44 and 46; # cell 7's open volume at 40-46 as sec. 1 prints it; nodes evaluated in each continuation "geometry_claim": {"closing": {"7": 45, "27": 43, "31": 42}, "checkpoint": {"7": 46, "27": 44, "31": 42}, "cell7": [9.435e-10, 1.342e-10, 1.93e-12, 0], "open_at_40": True, "lower_bounds": {"42": 64, "44": 65, "46": 66}, "nodes": {"7": 248823, "27": 199375, "31": 158811}}, # [decoded, manifest, bits] nodes; [decoded, manifest, this tree's] leaves; the least slack here [path, value, distance # from the manifest's] "topology_claim": { "69": {"nodes": [15711, 15711, 15711], "leaves": [7856, 7856, 7856], "internal": [7855, 7855], "leaf_paths_equal": True, "depth": [30, 30], "axes_high_first": True, "base_axes": True, "digests": [True, True], "least_slack": ["011000100000100101100", 4.406770393e-09, 4e-16]}, "47": {"nodes": [18455, 18455, 18455], "leaves": [9228, 9228, 9228], "internal": [9227, 9227], "leaf_paths_equal": True, "depth": [30, 30], "axes_high_first": True, "base_axes": True, "digests": [True, True], "least_slack": ["10001101101111110111", 1.529023796e-08, 6e-16]}}, # the ledgers' densities are the first that pass from the slack's start band on every leaf but cell 69's thinnest, which # passes only at 32,768 - past this tree's ladder "emitter_claim": { "69": {"pass": 7856, "refused": 0, "hull_equal": 7856, "margin_difference": 2.2e-16, "least": ["011000100000100101100", 32768, 1.6525434080154873e-09], "bands": [7855, 7856], "least_here": {"None": 1, "256": 6698, "512": 851, "1024": 228, "2048": 64, "4096": 10, "8192": 4}}, "47": {"pass": 9228, "refused": 0, "hull_equal": 9228, "margin_difference": 2.6e-16, "least": ["10001101101111110111", 16384, 6.750247223280388e-09], "bands": [9228, 9228], "least_here": {"256": 7635, "512": 1254, "1024": 223, "2048": 89, "4096": 16, "8192": 7, "16384": 4}}}, "cross_claim": {"first_equal": 7856, "hull_equal": 7856, "gap": [1.573e-12, 1.67e-12], "refused": 0, "density_counts": {"512": 3805, "1024": 3832, "2048": 175, "4096": 32, "8192": 8, "16384": 3, "65536": 1}, "escalated": [4427, [[512, -0.0002646], [1024, -7.134e-06], [2048, -1.938e-06], [4096, -4.917e-07], [8192, -1.127e-07], [16384, -2.887e-08], [32768, -3.071e-09], [65536, 2.535e-09]]]}, # this tree's certificates [normals, margin, exact margin]; marker 69's full polygon [area, active, numerator and # denominator bits], the shard's figure, the float reduction Round 29's file "marker_claim": {"records": [True, True], "mine": {"69": [128, 5.070240264558226e-06, 6.738115081084128e-05], "47": [256, 1.4996147563446147e-06, 1.856783932985273e-05]}, "polygon69": [[0.8349723974082344, 2611, 42639, 42639], True, True], "audit47": True, "a1_69_shipped": False}, # 66 complete and 11 residual (the records' volumes, ratios and pending counts this tree's); 51 at 36; the higher # budgets' bounds the cells closed by each depth here; candidates {69, 70}, closed or better {47, 69, 70}, every fraction "dashboard_claim": {"complete": [66, 66], "residual": [True, 11, 11], "common36": [51, 51], "lower_bounds": [{"38": 57, "40": 63, "42": 64, "44": 65, "46": 66}, True], "records_matched": 11, "pipeline": [[69, 70], [47, 69, 70], True, True, True, True, True, True]}, "code_facts": { "r32_generate_shard.py": {"lines": 60, "absolute_path": True, "opens": ["AMRAL_LUC_FC_Round_19_reference/continuation_probe.py", "AMRAL_LUC_FC_Round_19_reference/official_exact_kernel_minimal.py", "AMRAL_LUC_FC_Round_29_reference/marker_{cell:02d}.json", "AMRAL_LUC_FC_Round_32_cell{cell:02d}", "r26_full77_results/cell_{cell:02d}.json"], "not_in_archive": ["AMRAL_LUC_FC_Round_32_cell{cell:02d}", "r26_full77_results/cell_{cell:02d}.json"], "kernel_error_falls_back": True, "pad": True}, "r32_mpfr_lower_chunk.py": {"lines": 149, "absolute_path": True, "opens": ["AMRAL_LUC_FC_Round_29_reference/marker_{cell:02d}.json", "AMRAL_LUC_FC_Round_31_MPFR_ROOT_REPLAY.json", "AMRAL_LUC_FC_Round_32_cell{cell:02d}"], "not_in_archive": ["AMRAL_LUC_FC_Round_32_cell{cell:02d}"]}, "r32_mpfr_lower_chunk_hi.py": {"lines": 149, "absolute_path": True, "opens": ["AMRAL_LUC_FC_Round_29_reference/marker_{cell:02d}.json", "AMRAL_LUC_FC_Round_31_MPFR_ROOT_REPLAY.json", "AMRAL_LUC_FC_Round_32_cell{cell:02d}"], "not_in_archive": ["AMRAL_LUC_FC_Round_32_cell{cell:02d}"], "differs_from_lower_only_in": ["DENS"], "ladder": [512, 1024, 2048, 4096, 8192, 16384, 32768, 65536, 131072]}, "r32_mpfr_marker.py": {"lines": 102, "absolute_path": True, "opens": ["marker_{cell:02d}.json", "mpfr_marker.json"], "not_in_archive": ["mpfr_marker.json"]}, "r32_mpmath_emitter_chunk.py": {"lines": 121, "absolute_path": True, "opens": ["AMRAL_LUC_FC_Round_28_ROOT_RECONSTRUCTION.json", "AMRAL_LUC_FC_Round_29_reference/marker_{cell:02d}.json", "AMRAL_LUC_FC_Round_32_cell{cell:02d}", "r25_incremental_wave.py", "r26_full77_results/cell_{cell:02d}.json"], "not_in_archive": ["AMRAL_LUC_FC_Round_32_cell{cell:02d}", "r26_full77_results/cell_{cell:02d}.json"], "dps": 100, "start_band": True, "rationalize_17": True, "decimal_into_interval": True}}, } def near(a, b, tol): return abs(a - b) <= tol def sig(x, n=4): return float(f"{x:.{n - 1}e}") def w1_geometry(w): """sec. 1: cells 31, 27 and 7 continued from their boxes open at 40: each is closed at the even checkpoint sec. 1 gives (the depths are checked in steps of two, as in Round 26's ledger; the exact closing depth is recorded too); cell 7's open volume at 40, 42, 44 and 46; the lower bounds it gives for the higher budgets""" out, g, at = [], w["geometry"], w["atlas40"] depths = {int(k): v for k, v in at["depths"].items()} closing = {n: r30.r28.closing_depth(g[str(n)]["per"]) for n in CLOSED} checkpoint = {n: None if c is None else c + c % 2 for n, c in closing.items()} v7 = [sig(r30.vol(g["7"]["per"], d)) if r30.r28.at(g["7"]["per"], d)[2] else 0 for d in (40, 42, 44, 46)] base = sum(d is not None for d in depths.values()) lower = {str(d): base + sum(1 for n, c in closing.items() if c is not None and c <= d) for d in (42, 44, 46)} got = {"closing": {str(n): c for n, c in sorted(closing.items())}, "checkpoint": {str(n): c for n, c in sorted(checkpoint.items())}, "cell7": v7, "open_at_40": [n for n in CLOSED if depths[n] is None] == list(CLOSED), "lower_bounds": lower, "nodes": {str(n): g[str(n)]["per"][str(max(map(int, g[str(n)]["per"])))][0] for n in sorted(CLOSED)}} if checkpoint != CLOSED or not got["open_at_40"] or lower != {"42": 64, "44": 65, "46": 66} or got != w["geometry_claim"]: out.append(f"the three closures: {got}") w["w1"] = got return out def w2_topology(w): """sec. 2, 6: cells 69 and 47 lifted here to depth 30: the node and leaf counts, the leaf paths, the 2-bit axis stream (high bit first) and the least slack against the trees and manifests shipped""" out, got = [], {} tn = t_text(7, d_star(r31.TM)) seq = r31.float_sequence(tn, 30) for n in map(str, CELLS): c, comp = w["cells"][n], w["computed"][n] m = c["manifest"] try: nodes = r31.decode_topology(c["topology"], m["nodes"]) except ValueError as e: got[n] = {"topology": str(e)} continue internal = [p for p, b in nodes if b] leaves = [p for p, b in nodes if not b] mine = [p for p, _ in comp["leaves"]] slack = min((a - r30.PKG_PAD - T, p) for p, a in comp["leaves"]) got[n] = {"nodes": [len(nodes), m["nodes"], m["topology_bits"]], "leaves": [len(leaves), m["leaves"], len(mine)], "internal": [len(internal), m["internal_nodes"]], "leaf_paths_equal": sorted(leaves) == sorted(mine), "depth": [max(map(len, leaves)), m["closure_depth"]], "axes_high_first": r31.decode_axes(c["axes"], len(internal), True) == [seq[len(p)][0] for p in internal], "base_axes": r31.base_axes(m["base_path"])[0] == m["base_axis_trace"], "digests": [m["topology_sha256"] == c["digests"]["topology.bin"], m["axis_sha256"] == c["digests"]["axis_stream_2bit.bin"]], "least_slack": [slack[1], sig(slack[0], 10), sig(abs(slack[0] - m["worst_reference_slack"]), 1)]} ok = all(isinstance(v, dict) and "nodes" in v and v["leaf_paths_equal"] and v["axes_high_first"] and v["base_axes"] and all(v["digests"]) and len(set(v["nodes"])) == 1 and len(set(v["leaves"])) == 1 and len(set(v["internal"])) == 1 and v["least_slack"][2] < 1e-14 for v in got.values()) if not ok or got != w["topology_claim"]: out.append(f"the two trees: {got}") w["w2"] = got return out def start_band(slack): """the emitter's first density from a leaf's reference slack (read in its code after the rebuild)""" for bound, n in ((1e-3, 256), (2e-4, 512), (5e-5, 1024), (1e-5, 2048), (2e-6, 4096), (3e-7, 8192)): if slack >= bound: return n return 16384 def w3_emitter(w): """sec. 3, 6: every leaf of both cells certified on its intended box at the ledger's density: all pass, the ledger's hull counts, its margins to a few units in the last place; the ledger's densities are the first that pass from a start band chosen by the leaf's reference slack""" out, got = [], {} for n in map(str, CELLS): comp, led = w["computed"][n], w["cells"][n]["mpmath"] 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()} diff = max(abs(at[p]["margin"] - x["margin_decimal"]) for p, x in byp.items() if p in at) rule = [x["density"] == (max(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] = {"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(diff, 2), "least": [least["path"], least["density"], least["margin_decimal"]], "bands": [sum(rule), len(rule)], "least_here": {str(k): v for k, v in sorted(collections.Counter( r["least"]["n"] if r["least"] else None for r in res.values()).items(), key=lambda x: x[0] or 0)}} if any(v["pass"] != len(w["cells"][n]["mpmath"]) or v["refused"] or v["hull_equal"] != v["pass"] or v["margin_difference"] > 1e-15 for n, v in got.items()) or got != w["emitter_claim"]: out.append(f"the emitter ledgers: {got}") w["w3"] = got return out def w4_cross(w): """sec. 4, 8: cell 69's MPFR ledger against its own rule rebuilt here - the density, the hull count and the margin of every leaf; the one leaf escalated, at every density of its ladder""" out, led, lad = [], w["cells"]["69"]["mpfr"], w["winner"] first = [(r[-1]["n"] if r[-1]["pass"] else None) for r in lad] gap = [r[-1]["margin"] - x["margin_decimal"] for r, x in zip(lad, led)] k = next(i for i, x in enumerate(led) if x["path"] == ESCALATED) got = {"first_equal": sum(f == x["density"] for f, x in zip(first, led)), "hull_equal": sum(r[-1]["hull"] == x["hull_vertices"] for r, x in zip(lad, led)), "gap": [sig(min(gap)), sig(max(gap))], "refused": sum(y["failures"] for r in lad for y in r), "density_counts": {str(a): b for a, b in sorted(collections.Counter(first).items(), key=lambda x: x[0] or 0)}, "escalated": [k, [[y["n"], sig(y["margin"])] for y in lad[k]]]} if got["first_equal"] != len(led) or got["hull_equal"] != len(led) or got["refused"] or got != w["cross_claim"]: out.append(f"cell 69's MPFR ledger: {got}") w["w4"] = got return out def w5_markers(w): """sec. 5-6: markers 69 and 47 - the shard files' figures are Round 29's; this tree's certificates; marker 69's polygon under the package's normals and ceiling, every constraint kept (the MPFR script's); marker 47's replay row in Round 29's audit""" out, mk, mine = [], w["markers"], w["marker_mine"] s69, s47 = w["shard69"]["marker_upper"], w["shard47"]["marker_upper"] f69, f47 = mk[69]["final"], mk[47]["final"] aud = [x for x in w["audit29"]["markers"] if x["cell"] == 47] poly = mine["69"]["polygons"] got = {"records": [[s69["outer_area_decimal"], s69["margin_decimal"]] == [f69["outer_area_decimal"], f69["margin_decimal"]], s47["margin_decimal"] == f47["margin_decimal"]], "mine": {n: [mine[n]["certificate"]["ladder"]["N"], mine[n]["certificate"]["ladder"]["margin"], T - mine[n]["certificate"]["exact"]] for n in ("69", "47")}, "polygon69": [poly["full"], poly["full"][0] == s69["outer_area_decimal"], poly["reduced"] == [f69["outer_area_decimal"], f69["active_constraints"], f69["outer_area_num_bits"], f69["outer_area_den_bits"]]], "audit47": bool(aud) and [aud[0]["density"], aud[0]["outer_area_decimal"], aud[0]["margin_decimal"]] == [f47["density"], f47["outer_area_decimal"], f47["margin_decimal"]], "a1_69_shipped": any(x["cell"] == 69 for x in w["audit29"]["markers"])} if not all(got["records"]) or not got["polygon69"][1] or not got["polygon69"][2] or not got["audit47"] or got != w["marker_claim"]: out.append(f"markers 69 and 47: {got}") w["w5"] = got return out def w6_dashboard(w): """sec. 0, 7-9: the stage counts from the facts above - the cells closed by 40 and the three closures, the two publication candidates and the prototype - and the 11 residual records against this tree's continuation at the depths they give""" out, d, at, g = [], w["dashboard"], w["atlas40"], w["geometry"] depths = {int(k): v for k, v in at["depths"].items()} later = {n: r30.r28.closing_depth(g[str(n)]["per"]) for n in CLOSED} complete = {n for n, v in depths.items() if v is not None} | {n for n, c in later.items() if c is not None} residual = sorted(set(depths) - complete) # the higher budgets' lower bounds: the cells closed by each depth, from the atlas and the three continuations mine = {str(b): sum(v is not None and v <= b for v in depths.values()) + sum(c is not None and c <= b for c in later.values()) for b in (38, 40, 42, 44, 46)} geo, ar = d["geometry"], d["arithmetic_pipeline"] recs = geo["residual_cells"] vols = at["volumes"] matched = sum(near(vols[str(r["cell"])][str(r["last_depth"])], r["unresolved_volume"], 1e-12 * r["unresolved_volume"]) and near(vols[str(r["cell"])][str(r["last_depth"])] / vols[str(r["cell"])][str(r["last_depth"] - 2)], r["ratio_vs_previous"], 1e-12) and round(vols[str(r["cell"])][str(r["last_depth"])] * 2 ** r["last_depth"] / r30.ROOT7) == r["pending"] for r in recs if str(r["cell"]) in vols) pc, ac = sorted(ar["publication_candidate_cells"]), sorted(ar["arithmetic_closed_or_better_cells"]) got = {"complete": [len(complete), geo["known_complete"]], "residual": [residual == sorted(r["cell"] for r in recs), len(residual), geo["residual"]], "common36": [sum(v is not None and v <= 36 for v in depths.values()), geo["latest_exact_common_budget"]["complete"]], "lower_bounds": [geo["higher_budget_known_closure_lower_bounds"], mine == geo["higher_budget_known_closure_lower_bounds"]], "records_matched": matched, "pipeline": [pc, ac, ar["geometry_complete_arithmetic_pending_count"] == len(complete) - len(ac), near(ar["publication_candidate_fraction_global"], len(pc) / 77, 1e-15), near(ar["publication_candidate_fraction_of_known_geometry_complete"], len(pc) / len(complete), 1e-15), near(ar["arithmetic_closed_or_better_fraction_global"], len(ac) / 77, 1e-15), near(ar["arithmetic_closed_or_better_fraction_of_known_geometry_complete"], len(ac) / len(complete), 1e-15), near(geo["known_complete_fraction"], len(complete) / 77, 1e-15)]} if len(complete) != geo["known_complete"] or not got["residual"][0] or not got["lower_bounds"][1] or matched != len(recs) or not all(got["pipeline"][2:]) \ or got != w["dashboard_claim"]: out.append(f"the dashboard: {got}") w["w6"] = got return out def w7_code(w): """what the package ships, read after the rebuild and never run""" leaves = [row[0] for row in w["manifest"]["leaves"]] facts = {} for name, src in sorted(w["code"].items()): opened = sorted(set(re.findall(r"ROOT\s*/\s*f?[\"']([^\"']+)[\"']", src)) | {p.rsplit("/", 1)[-1] for p in re.findall(r"open\(\s*f?'([^']+)'", src)}) facts[name] = {"lines": src.count("\n"), "absolute_path": bool(re.search(r"(?:Path\(|open\(f?|insert\(0,)\s*[\"']/", src)), "opens": opened, "not_in_archive": sorted(u for u in opened if not any(u.split("/")[0].split("{")[0].rstrip("_") in leaf for leaf in leaves))} gen, emi, lo, hi = (w["code"][k] for k in ("r32_generate_shard.py", "r32_mpmath_emitter_chunk.py", "r32_mpfr_lower_chunk.py", "r32_mpfr_lower_chunk_hi.py")) facts["r32_generate_shard.py"].update({"kernel_error_falls_back": "except Exception:pass" in gen, "pad": "-1e-10" in gen}) facts["r32_mpmath_emitter_chunk.py"].update({"dps": int(re.search(r"mp\.iv\.dps=(\d+)", emi).group(1)), "start_band": "def startN(sl):" in emi, "rationalize_17": "format(float(v),'.17g')" in emi, "decimal_into_interval": "mp.iv.mpf([fs(e.lo),fs(e.hi)])" in emi}) diff = [a for a, b in zip(lo.splitlines(), hi.splitlines()) if a != b] facts["r32_mpfr_lower_chunk_hi.py"].update({"differs_from_lower_only_in": [re.sub(r"=.*", "", x.split(";")[-1]).strip() for x in diff], "ladder": json.loads(re.search(r"DENS=(\[[0-9,]+\])", hi).group(1))}) w["w7"] = facts return [] if facts == w["code_facts"] else [f"the scripts: {facts}"] def p1_package(w): out, s69, s47, d = [], w["shard69"], w["shard47"], w["dashboard"] for n, sh, ledkey, key in (("69", s69, "mpmath", "lower_emitter"), ("69", s69, "mpfr", "lower_cross_backend"), ("47", s47, "mpmath", "lower_mpmath")): led, rec = w["cells"][n][ledkey], sh[key] passing = [x for x in led if x["status"] in ("PASS", "MPFR-PASS")] least = min(passing, key=lambda x: x["margin_decimal"]) dens = {str(k): v for k, v in collections.Counter(x["density"] for x in passing).items()} if (rec["leaves_total"], rec["leaves_pass"], rec["leaves_inconclusive"], rec["density_counts"], rec["minimum_margin_decimal"], rec["minimum_margin_path"], rec["ledger_sha256"]) \ != (len(led), len(passing), len(led) - len(passing), dens, least["margin_decimal"], least["path"], w["cells"][n]["digests"][f"{ledkey}_leaf_ledger.json"]): out.append(f"shard {n}: {key} against its ledger") esc = s69["lower_cross_backend"]["selective_density_escalation"] led = w["cells"]["69"]["mpfr"] if led[esc["leaf_index"]]["path"] != esc["path"] or led[esc["leaf_index"]]["density"] != esc["to_density"] or led[esc["leaf_index"]]["margin_decimal"] != esc["final_margin_decimal"]: out.append("shard 69: the escalation record against the ledger") for n, sh in (("69", s69), ("47", s47)): m, g = w["cells"][n]["manifest"], sh["geometry"] if (g["closure_depth"], g["nodes"], g["leaves"], g["topology_sha256"], g["axis_sha256"], sh["base_path"]) \ != (m["closure_depth"], m["nodes"], m["leaves"], m["topology_sha256"], m["axis_sha256"], m["base_path"]) \ or m["base_path"] != w["ledger26"]["cells"][int(n)]["path"] or m["marker_file"] != f"marker_{n}.json" or w["markers"][int(n)]["path"] != m["base_path"]: out.append(f"shard {n}: geometry against the manifest and Round 26's ledger") ar = d["arithmetic_pipeline"] if (s69["status"], s69["publication_candidate"], s47["status"], s47["publication_candidate"]) != ("PUBLICATION-CANDIDATE-SHARD", True, "ARITHMETICALLY-CLOSED-PROTOTYPE", False) \ or sorted(ar["publication_candidate_cells"]) != [69, 70] or sorted(ar["arithmetic_closed_or_better_cells"]) != [47, 69, 70] \ or ar["publication_candidate_count"] != 2 or ar["arithmetic_closed_or_better_count"] != 3 or d["global_lebesgue_claim"] or s69["global_lebesgue_claim"] or s47["global_lebesgue_claim"]: out.append("the dashboard's pipeline against the shard files") recs = {r["cell"]: r for r in w["progress27"]["currently_without_known_complete_edge"]["cells"]} if any(r["cell"] not in recs or (recs[r["cell"]]["last_tested_depth"], recs[r["cell"]]["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 d["geometry"]["residual_cells"]) \ or set(recs) - {r["cell"] for r in d["geometry"]["residual_cells"]} != set(CLOSED): out.append("the dashboard's residual records against Round 27's") crystal = gate.squash(w["crystal"]) for frag in (r"\boxed{66/77}.", r"\boxed{\{69,70\}}.", r"\boxed{\{47,69,70\}}.", "7,856leaves", "9,228leaves", r"32768\to65536", r"2.5329\times10^{-9}>0."): if frag not in crystal: out.append(f"crystal: {frag}") w["p1"] = {"escalation": [esc["leaf_index"], esc["path"]], "residual_records": len(d["geometry"]["residual_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, text in (("round32", 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 (("coverage_dashboard_sha256", DASH), ("cell69_candidate_sha256", SHARD69), ("cell47_prototype_sha256", SHARD47), ("bulk_policy_sha256", POLICY), ("cell69_mpmath_ledger_sha256", REF + "cell69_mpmath_leaf_ledger.json"), ("cell69_mpfr_ledger_sha256", REF + "cell69_mpfr_leaf_ledger.json"), ("cell47_mpmath_ledger_sha256", REF + "cell47_mpmath_leaf_ledger.json")): if v[key] != leaves[leaf_id][2]: out.append(f"VALIDATION {key} against the archive") d, s69, s47, c = w["dashboard"], w["shard69"], w["shard47"], w["cells"] ok = lambda led: all(x["status"] in ("PASS", "MPFR-PASS") for x in led) kc = {"geometry_complete_66": d["geometry"]["known_complete"] == 66, "geometry_residual_11": d["geometry"]["residual"] == 11 == len(d["geometry"]["residual_cells"]), "cell69_mpmath_7856": len(c["69"]["mpmath"]) == 7856 and ok(c["69"]["mpmath"]), "cell69_mpfr_7856": len(c["69"]["mpfr"]) == 7856 and ok(c["69"]["mpfr"]), "cell69_selective_65536": s69["lower_cross_backend"]["selective_density_escalation"]["to_density"] == 65536, "cell69_marker_mpfr_pass": s69["marker_upper"]["MPFR_status"] == "PASS" and s69["marker_upper"]["margin_decimal"] > 0, "cell69_publication_candidate": s69["status"] == "PUBLICATION-CANDIDATE-SHARD" and s69["publication_candidate"] is True, "cell47_mpmath_9228": len(c["47"]["mpmath"]) == 9228 and ok(c["47"]["mpmath"]), "cell47_not_publication_candidate": s47["publication_candidate"] is False, "publication_candidate_count_2": d["arithmetic_pipeline"]["publication_candidate_count"] == 2, "no_global_claim": not d["global_lebesgue_claim"] and not s69["global_lebesgue_claim"] and not s47["global_lebesgue_claim"]} if kc != v["checks"] or v["status"] != "PASS": out.append(f"VALIDATION checks {kc}") w["p2"] = kc return out _C69 = ("7,856 of 7,856 here too on this tree's own lift and the intended boxes, the ledger's hull counts, margins within " "2.2e-16 (W2, W3)") _MPFR69 = ("the ledger is its own rule's - per direction the winning body's point - rebuilt here leaf for leaf; the escalated leaf " "goes from -3.07e-9 at 32,768 to +2.53e-9 at 65,536 (W4)") _PC69 = ("its lower under two implementations on two backends (the mpmath emitter, the MPFR winner rule) and its upper under both " "backends hold here (W3-W5); no separate A1 record for marker 69 is shipped - the MPFR script is itself the exact full hull, " "which this tree rebuilds (W5)") _PROTO47 = ("its lower (9,228 of 9,228 here too) and its upper hold here; its MPFR replays are pending, as the shard file says (W3, W5)") R32_REVIEWS = [ ("PASS", "7856/7856", "computation", "PASS", _C69), ("PASS", "7856/7856 MPFR", "computation", "PASS", _MPFR69), ("PASS", "9228/9228", "computation", "PASS", "9,228 of 9,228 here too on this tree's own lift, the ledger's hull counts, margins within 2.6e-16 (W2, W3)"), ("ARITHMETICALLY-CLOSED-PROTOTYPE", "", "computation", "PASS", _PROTO47), ("ARITHMETICALLY-CLOSED-PROTOTYPE", "cell47", "computation", "PASS", _PROTO47), ("PUBLICATION-CANDIDATE-SHARD", "", "computation", "PASS", _PC69), ("PUBLICATION-CANDIDATE-SHARD", "marker70", "computation", "PASS", "Round 31's promotion, checked in RUN-034"), ("PUBLICATION-CANDIDATE-SHARD", "cell69", "computation", "PASS", _PC69), ("NOT CERTIFIED", "a_{Leb}≥0.835", "reading", "PASS", "true"), ] def r1_registry(w): return registry.completeness(w["registry"], "R32", w["definitions"], w["reviews"]) CHECKS = {"A0": gate.anchors_check(ANCHORS), "W1": w1_geometry, "W2": w2_topology, "W3": w3_emitter, "W4": w4_cross, "W5": w5_markers, "W6": w6_dashboard, "W7": w7_code, "P1": p1_package, "P2": p2_package, "R1": r1_registry} DEPENDS = {"A0": {"text"}, "W1": {"geometry", "atlas40", "geometry_claim"}, "W2": {"cells", "computed", "topology_claim"}, "W3": {"cells", "computed", "emitter_claim"}, "W4": {"cells", "winner", "cross_claim"}, "W5": {"markers", "marker_mine", "shard69", "shard47", "audit29", "marker_claim"}, "W6": {"dashboard", "atlas40", "geometry", "dashboard_claim"}, "W7": {"code", "manifest", "code_facts"}, "P1": {"shard69", "shard47", "dashboard", "cells", "markers", "ledger26", "progress27", "crystal"}, "P2": {"validation", "manifest", "text", "crystal", "dashboard", "shard69", "shard47", "cells"}, "R1": {"registry", "definitions", "reviews"}} def drill_cases(base): text, c = base["text"], base["cells"] def edit(obj, fn): x = copy.deepcopy(obj) fn(x) return x def cells_edit(fn): return edit(c, fn) def fail_leaf(comp): comp["69"]["results"][0]["ledger"]["pass"] = False k = next(i for i, x in enumerate(c["69"]["mpfr"]) if x["path"] == ESCALATED) 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-shard69-keys-sorted", "control", {"shard69": json.loads(json.dumps(base["shard69"], sort_keys=True))}, set()), ("M1-doc-margin", "mutation", {"text": text.replace(r"2.5329\times", r"2.5328\times")}, {"A0"}), ("M2-geometry-claim", "mutation", {"geometry_claim": {**(CLAIMS["geometry_claim"] or {}), "closing": {"7": 44}}}, {"W1"}), ("M2b-geometry-open", "mutation", {"geometry": edit(base["geometry"], lambda x: x["31"]["per"][max(x["31"]["per"], key=int)].__setitem__(2, 5))}, {"W1", "W6"}), ("M3-topology-bit", "mutation", {"cells": cells_edit(lambda x: x["69"].update(topology=bytes([x["69"]["topology"][0] ^ 1]) + x["69"]["topology"][1:]))}, {"W2"}), ("M4-axis-stream", "mutation", {"cells": cells_edit(lambda x: x["47"].update(axes=bytes([x["47"]["axes"][0] ^ 0x40]) + x["47"]["axes"][1:]))}, {"W2"}), ("M5-emitter-margin", "mutation", {"cells": cells_edit(lambda x: x["47"]["mpmath"][100].update(margin_decimal=x["47"]["mpmath"][100]["margin_decimal"] + 1e-12))}, {"W3"}), ("M6-certificate", "mutation", {"computed": edit(base["computed"], fail_leaf)}, {"W3"}), ("M7-mpfr-density", "mutation", {"cells": cells_edit(lambda x: x["69"]["mpfr"][k].update(density=32768))}, {"W4", "P1"}), ("M8-marker-area", "mutation", {"shard69": edit(base["shard69"], lambda x: x["marker_upper"].update(outer_area_decimal=0.8349723974082345))}, {"W5"}), ("M9-dashboard-count", "mutation", {"dashboard": edit(base["dashboard"], lambda x: x["geometry"].update(known_complete=65))}, {"W6", "P2"}), ("M9b-dashboard-bound", "mutation", {"dashboard": edit(base["dashboard"], lambda x: x["geometry"]["higher_budget_known_closure_lower_bounds"].update({"44": 66}))}, {"W6"}), ("M10-residual-record", "mutation", {"dashboard": edit(base["dashboard"], lambda x: x["geometry"]["residual_cells"][0].update(pending=x["geometry"]["residual_cells"][0]["pending"] + 1))}, {"W6", "P1"}), ("M11-code-claim", "mutation", {"code_facts": {}}, {"W7"}), ("M12-shard-ledger-digest", "mutation", {"shard47": edit(base["shard47"], lambda x: x["lower_mpmath"].update(ledger_sha256="0" * 64))}, {"P1"}), ("M13-crystal", "mutation", {"crystal": base["crystal"].replace("9,228 leaves", "9,229 leaves")}, {"P1"}), ("M14-validation-digest", "mutation", {"validation": {**base["validation"], "cell69_mpfr_ledger_sha256": "0" * 64}}, {"P2"}), ("M15-validation-check", "mutation", {"validation": {**base["validation"], "checks": {**base["validation"]["checks"], "cell47_not_publication_candidate": False}}}, {"P2"}), ("M16-review-dropped", "mutation", {"reviews": list(R32_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(R32_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)[:2000]) if not args.drill: return cases = drill_cases(base) if args.blind: cases = [c for c in cases if args.blind in c[3]] d = gate.run_drill(build, CHECKS, DEPENDS, cases) summary = gate.summarize(d, CHECKS) print(gate.report_drill(summary)) for x in d: if not x["ok"]: print(" DRILL FAIL", x) if args.blind: n = sum(1 for x in d if args.blind in x["expected"] and args.blind not in x["tripped"]) print(f"blind {args.blind}: drill reported it blind in {n} cases (nothing written)") return log = {"run": "RUN-035", "subject": "Round 32: the first bulk migration wave, and three more closures", "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("R32", "RUN-035", {}, R32_REVIEWS) print(f"registry: {len(R32_REVIEWS)} reviews recorded for R32") if __name__ == "__main__": main()