diff --git a/research/mode-preserving-rounding/PROOF.md b/research/mode-preserving-rounding/PROOF.md new file mode 100644 index 0000000000..360cd277d8 --- /dev/null +++ b/research/mode-preserving-rounding/PROOF.md @@ -0,0 +1,109 @@ +# An exact radius-one mode fiber + +This scoped proof was produced by Nick Petalas. Apache-2.0. + +## Contract and source + +Let M be the 112-by-8 integer mode matrix in Dillon Amburgey's +[PR4933](https://github.com/CrocSwap/integer-mult-bounds/pull/4933), head +`d969c458c24278e0fd37e5b4c0ff8a53a496b430`. +Its columns are `mode_columns` in the source-pinned NORMALIZERS.json. +The cited inverse-code identity is A^-1 = I - MM^T/52. That identity +is a predecessor premise; no new check of its factorization is claimed. + +Consider rounding x in R^112 to z in Z^112 subject to + + M^T z = M^T x. + +The rule may use all coordinates, arbitrary nonlinear computation and +arbitrary correlated randomness. There is no coordinatewise rounding premise. +Mode equality is required for each returned output. Equality only in +expectation is a weaker contract and is outside this obstruction. +We require the target mode tuple to have an integer lift. This avoids an +obstruction caused merely by an empty fiber. + +## The witness and exact optimum + +Use zero-based owner indices. Write m_i for row i of M. The source rows are + + m_0 = ( 1, 1, 1, 1, 0, 0, 0, 0), + m_7 = (-1,-1, 1, 1, 0, 0, 0, 0), + m_20 = ( 0, 0, 0, 0, 1,-1, 1, 1), + m_111 = ( 0, 0, 0, 0, 1,-1,-1,-1), + m_48 = ( 0, 0, 1, 1, 1,-1, 0, 0). + +They give the exact relation + + m_0 + m_7 + m_20 + m_111 = 2 m_48. (1) + +Put x = (e_0 + e_7 + e_20 + e_111)/2. Then M^T x = m_48, +so z = e_48 is an integer lift. Its infinity-norm distance from x is one. + +Suppose an integer lift z had ||z-x||_infinity < 1. Every coordinate of x +outside S={0,7,20,111} is zero, so every corresponding integer z_i is zero. +On S, each z_i must be zero or one. Mode 0 and mode 2 now require + + z_0 - z_7 = 0, z_0 + z_7 = 1. (2) + +The first equality follows from the zero target in mode 0. The second +follows from the unit target in mode 2. The rows m_20 and m_111 contribute +zero to both equations. Equations (2) force z_0=z_7=1/2, contradicting +integrality. Consequently + + min { ||z-x||_infinity : z in Z^112, M^T z=M^T x } = 1. (3) + +The same argument applies to each realized integer output of a randomized rule. +Thus no rule can guarantee a smaller uniform radius on all inputs with +nonempty integer mode fibers, even if it is allowed arbitrary correlations. +This does not show that radius one suffices on every such fiber. + +For any h>0 and any n in Z^112, translation and scaling give + + min { ||z-h(n+x)||_infinity : z in h Z^112, + M^T z=M^T h(n+x) } = h. (4) + +Indeed z/h-n is an integer lift of M^T x. The attaining output is +h(n+e_48). Thus retaining exact modes can require twice the usual +half-grid coordinate radius, at every output-grid scale. + +## Why this is a rounding obstruction + +There are exactly sixteen integer outputs inside the open radius-one box. +They are the {0,1} choices on S, zero elsewhere. The verifier enumerates all +sixteen, compares column-oriented and row-oriented mode calculations, and +finds no lift. Equation (2), rather than extrapolation from that census, +proves the exclusion of every integer output in the box. + +If the mode constraint is removed, z=0 has distance 1/2. Even preserving +the ordinary sum does not cause this example's obstruction: e_0+e_20 has +the same sum as x and distance 1/2, but different modes. Allowing radius +one admits e_48. The obstruction therefore retains both its mode and +grid hypotheses and is consistent with an explicit feasible lift. + +## Scope and remaining obligations + +This is a new local precision contract for the cited code. It is not a +claim about every reachable state of a native caller. A caller could avoid +the displayed input, allow mode defects, keep extra residue information, +or round to a finer grid. Those are changed contracts. + +The theorem gives neither the global optimal mode-preserving radius nor +an efficient rounder. The A^-1 factorization motivates preserving M^T x; +it does not imply that a complete inverse implementation must preserve +those modes exactly. No physical correlated-rounding algorithm, native +restoration, tape/storage tariff, complete error propagation, supplier +admission, new kappa or selected-frontier update follows. All five framework +assumptions remain. Independent human and formal proof-kernel review are +unclaimed. + +## Credit + +Dillon Amburgey supplies the actual code and mode representation. JoyboyBrian's +[PR5069](https://github.com/CrocSwap/integer-mult-bounds/pull/5069) supplies +the source-bound fixed-grid inverse context. Dugongue's coded producer and +the retained native, controller and compiler authors retain their credit. +Ali Romman's [PR5838](https://github.com/CrocSwap/integer-mult-bounds/pull/5838) +separates independently adverse completed defects from possible physical +rounding correlations. Its word and error calculation are not inputs here. +The lattice and finite-box arguments are elementary classical methods. +The source-bound witness, exact fiber radius and new contract are proved here. diff --git a/research/mode-preserving-rounding/README.md b/research/mode-preserving-rounding/README.md new file mode 100644 index 0000000000..3106f129d7 --- /dev/null +++ b/research/mode-preserving-rounding/README.md @@ -0,0 +1,89 @@ +# Exact mode preservation can double the coordinate rounding radius + +This scoped mathematical proof with an exact finite certificate was produced by Nick Petalas. + +For the actual eight-mode matrix M of Dillon Amburgey's +[PR4933](https://github.com/CrocSwap/integer-mult-bounds/pull/4933), put + + x = (e_0 + e_7 + e_20 + e_111)/2. + +Among integer outputs z preserving all eight mode sums M^T z=M^T x, +the minimum infinity-norm rounding error is exactly **one**. The output +e_48 attains it. Every integer output at distance less than one is excluded +by z_0-z_7=0 and z_0+z_7=1. Thus arbitrary joint rounding and correlated +randomness cannot retain the usual half-unit error on all feasible mode fibers. +Mode equality is required for every returned output, rather than only in expectation. +Translation and scaling give the same factor-two obstruction on every grid. + +[PROOF.md](PROOF.md) states the boundary, literal five-row identity and +universal argument. This is a new rounding contract, not a replay of a +predecessor theorem. It does not assert that every mode fiber has radius one +or that an actual caller must preserve these modes. Complete kappa is unchanged. + +## Reproduce + +From the repository root, CPython 3.12 and the standard library suffice: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/mode-preserving-rounding/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/mode-preserving-rounding/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/mode-preserving-rounding +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/mode-preserving-rounding --check-source-history +``` + +Other systems may substitute their CPython 3.12 executable. Direct checks +print `PASS_MODE_PRESERVING_ROUNDING`, including sixteen excluded corners, +91 translated/scaled attaining fixtures and nine rejection controls. +The preceding JSON is a fresh receipt binding the source and package files +by SHA256. No receipt is handwritten or stored. Verification writes nothing. +Normal and optimized modes run the same explicit checks. The complete export +with its declared source input also supports Git-free direct replay. + +## Scope and credit + +The matrix is the coded inverse's source, not a claim that this proposed +mode-preserving rounder is installed in the selected construction. The +uniform-transfer-audit card is changed to this precision side result. +The selected binding control passes at conditional kappa .003125804; +it is not an operator replay. [TASK.json](TASK.json) records the original +card, changed scope and next questions. [SOURCES.json](SOURCES.json) pins +the exact live mode table and historical provenance. + +Credit Dillon Amburgey / PR4933 for M and A^-1=I-MM^T/52, +JoyboyBrian / PR5069 for the fixed-grid inverse context, Dugongue for the +coded producer, and their retained native/controller/compiler lineage. +Ali Romman / PR5838 distinguishes possible rounding correlations from its +adverse-defect model; that calculation is not rerun. Classical lattice and +finite-box arguments retain their credit. New work is Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +The result supplies no global rounding-radius optimum, physical correlated +rounder, complete error ledger, restoration, precision/storage/tape bill, +supplier admission or complete multiplication theorem. The five framework +assumptions and selected frontier retain their status. + +## Open next questions + +1. What is the least uniform radius on all nonempty integer fibers of this + exact mode map? Start with a fundamental domain of its kernel lattice; + the lower bound here gives no global upper construction. +2. Can a concrete physical caller exploit approximate mode preservation + rather than exact preservation? Start with one reached state and its + permitted mode-defect budget; reachability, full propagation and tape + costs are still missing. + +## Verifier bounds + +The verifier reads at most one MiB per file and at most 32 package files. +There are eight modes, 112 owners, sixteen corners and 91 scaled fixtures. +No recursion, dynamic code execution, subprocess or output-file write is +used. Functions stay below 60 lines, and errors remain enabled under -O. +Python allocates managed integers, Fractions and containers. This is a +Power of Ten rule 3 deviation bounded by those fixed domains and a registered +30-second timeout. A future arbitrary-dimension implementation must reassess +storage before changing those limits. Warning-strict normal/optimized replay +provides the available diagnostics; no new static-analyzer configuration or +physical-memory bound is claimed. +Rule 9 has a bounded test-control deviation: `reject` calls only the four +locally named functions `parse_modes`, `validate_modes`, `vector` and +`same_modes`, with nine fixed fixtures. Unexpected exceptions propagate. diff --git a/research/mode-preserving-rounding/SOURCES.json b/research/mode-preserving-rounding/SOURCES.json new file mode 100644 index 0000000000..c87d43b6f4 --- /dev/null +++ b/research/mode-preserving-rounding/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/coded-native-caller/NORMALIZERS.json", + "usage": "input", + "git_blob": "bca92c222c395d3d75c047fbb678f3cd0947c60f", + "sha256": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da" + } + ] +} diff --git a/research/mode-preserving-rounding/TASK.json b/research/mode-preserving-rounding/TASK.json new file mode 100644 index 0000000000..3bea14b363 --- /dev/null +++ b/research/mode-preserving-rounding/TASK.json @@ -0,0 +1,110 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove a feasible eight-mode fiber of the actual PR4933 code has exact integer rounding radius one, excluding every smaller joint-rounding radius.", + "scope_change_reason": "Original precision side question: correlated mode-preserving rounding replaces an audit of a selected all-size implication. No predecessor result is reverified as the deliverable.", + "bottleneck_link": "Possible correlated rounding requires its own local error set. Exact preservation of the coded inverse modes cannot be assumed compatible with a half-grid coordinate error; a physical caller and full error invoice remain separate.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified feasible-fiber witness and exact radius proof; leave the global optimum and physical caller to Open next questions.", + "outcome": "completed", + "evidence": "Written two-equation integrality proof; exact live-source five-row relation; all sixteen integer corners; 91 translated/scaled attaining fixtures and nine rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the least uniform radius on all nonempty integer fibers of this exact mode map?", + "why_it_matters": "The witness gives a necessary radius but no global attaining rounder.", + "first_step": "Describe a fundamental domain of the integer kernel lattice and bound its infinity-norm covering radius.", + "blocked_by": "A global upper construction is absent." + }, + { + "question": "Can a concrete physical caller exploit approximate mode preservation?", + "why_it_matters": "Exact mode preservation has a larger coordinate error on this fiber; a different permitted error set may avoid it.", + "first_step": "Specify one reached state and its permitted mode-defect budget, then propagate it through the actual inverse.", + "blocked_by": "Caller reachability, full error propagation and tape costs are unspecified." + } + ], + "claim_type": "Scoped mathematical proof with an exact finite certificate", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19299863", + "question_source": "original", + "predecessors": [ + { + "pr": 4933, + "author": "Dillon Amburgey / dillona", + "head": "d969c458c24278e0fd37e5b4c0ff8a53a496b430", + "use": "Actual eight-mode matrix and cited inverse factorization." + }, + { + "pr": 5069, + "author": "JoyboyBrian", + "use": "Fixed-grid arithmetic context; not replayed." + }, + { + "pr": 5838, + "author": "Ali Romman / aliromman", + "use": "Distinguishes a correlated physical error set from independently adverse defects; no source computation reused." + } + ] +} diff --git a/research/mode-preserving-rounding/VERIFY.json b/research/mode-preserving-rounding/VERIFY.json new file mode 100644 index 0000000000..298013e360 --- /dev/null +++ b/research/mode-preserving-rounding/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/coded-native-caller/NORMALIZERS.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Source-bound feasible fiber, all sixteen integer corners, exact radius attainment, 91 scaled/translated fixtures and nine rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "The same complete explicit checks under optimized Python, with generated source/package hash receipt." + } + ] +} diff --git a/research/mode-preserving-rounding/verify.py b/research/mode-preserving-rounding/verify.py new file mode 100644 index 0000000000..694c10815b --- /dev/null +++ b/research/mode-preserving-rounding/verify.py @@ -0,0 +1,163 @@ +"""Exact mode-preserving rounding obstruction, produced by Nick Petalas.""" + +from fractions import Fraction as Q +import hashlib +import itertools +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +SOURCE = "research/coded-native-caller/NORMALIZERS.json" +SUPPORT = (0, 7, 20, 111) +ROWS = ( + (1, 1, 1, 1, 0, 0, 0, 0), + (-1, -1, 1, 1, 0, 0, 0, 0), + (0, 0, 0, 0, 1, -1, 1, 1), + (0, 0, 0, 0, 1, -1, -1, -1), +) +TARGET = (0, 0, 1, 1, 1, -1, 0, 0) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def bounded_read(path): + need(path.is_file() and not path.is_symlink(), "regular input required") + need(path.stat().st_size <= 1_048_576, "input size limit") + return path.read_bytes() + + +def parse_modes(raw, digest): + need(hashlib.sha256(raw).hexdigest() == digest, "source hash") + modes = json.loads(raw)["mode_columns"] + validate_modes(modes) + return tuple(tuple(column) for column in modes) + + +def validate_modes(modes): + need(type(modes) is list and len(modes) == 8, "eight modes required") + need(all(type(c) is list and len(c) == 112 for c in modes), "owner shape") + need(all(type(v) is int and v in (-1, 0, 1) for c in modes for v in c), + "signed mode entries") + + +def vector(support, value): + need(len(support) <= 112 and len(set(support)) == len(support), "unique owners") + need(all(type(i) is int and 0 <= i < 112 for i in support), "owner range") + out = [Q(0)] * 112 + for i in support: + out[i] = value + return tuple(out) + + +def observe(modes, values): + need(len(values) == 112, "observation shape") + return tuple(sum(c * x for c, x in zip(column, values)) for column in modes) + + +def distance(left, right): + need(len(left) == len(right) == 112, "distance shape") + return max(abs(x - y) for x, y in zip(left, right)) + + +def same_modes(modes, left, right): + need(observe(modes, left) == observe(modes, right), "mode preservation") + + +def reject(label, function, *args): + try: + function(*args) + except ValueError: + return label + raise ValueError("accepted rejection control: " + label) + + +def corner_census(modes, x): + records = [] + for bits in itertools.product((0, 1), repeat=4): + corner = [0] * 112 + for i, bit in zip(SUPPORT, bits): + corner[i] = bit + observed = observe(modes, corner) + need(distance(corner, x) == Q(1, 2), "literal corner distance") + # Independently sum rows to check every returned mode tuple. + by_rows = tuple(sum(bit * row[k] for bit, row in zip(bits, ROWS)) + for k in range(8)) + need(observed == by_rows and observed != TARGET, "corner exclusion") + need(not (corner[0] - corner[7] == 0 and corner[0] + corner[7] == 1), + "integer contradiction") + records.append({"bits": bits, "modes": observed}) + need(len(records) == 16, "complete corner domain") + return records + + +def scaled_fixtures(modes, x, lift): + count = 0 + for exponent in range(-6, 7): + h = Q(2) ** exponent + for shift in range(-3, 4): + translation = tuple(shift * ((i % 5) - 2) for i in range(112)) + current = tuple(h * (a + b) for a, b in zip(translation, x)) + output = tuple(h * (a + b) for a, b in zip(translation, lift)) + same_modes(modes, current, output) + need(distance(current, output) == h, "translated scaled upper witness") + need(all((v / h).denominator == 1 for v in output), "output grid") + count += 1 + return count + + +def controls(modes, raw, digest, x, lift): + malformed = [list(column) for column in modes] + malformed[0][0] = 2 + wrong_lift = vector((0,), Q(1)) + omitted = vector(SUPPORT[:-1], Q(1, 2)) + checks = [ + reject("changed source", parse_modes, raw + b" ", digest), + reject("missing mode", validate_modes, [list(c) for c in modes[:-1]]), + reject("invalid coefficient", validate_modes, malformed), + reject("duplicate owner", vector, (0, 0), Q(1, 2)), + reject("out-of-range owner", vector, (112,), Q(1, 2)), + reject("wrong integer lift", same_modes, modes, x, wrong_lift), + reject("omitted fractional owner", same_modes, modes, omitted, lift), + reject("zero corner", same_modes, modes, x, vector((), Q(0))), + ] + # Sum preservation alone admits a half-unit corner, but the modes do not. + sum_only = vector((0, 20), Q(1)) + need(sum(sum_only) == sum(x) and distance(sum_only, x) == Q(1, 2), + "sum-only positive control") + checks.append(reject("sum-only corner", same_modes, modes, x, sum_only)) + return checks + + +def verify(): + sources = json.loads(bounded_read(HERE / "SOURCES.json")) + source = next(row for row in sources["files"] if row["path"] == SOURCE) + need(source["usage"] == "input", "declared source input") + raw = bounded_read(HERE.parents[1] / SOURCE) + modes = parse_modes(raw, source["sha256"]) + for i, expected in zip(SUPPORT, ROWS): + need(tuple(column[i] for column in modes) == expected, "literal source row") + need(tuple(column[48] for column in modes) == TARGET, "integer lift source row") + x, lift = vector(SUPPORT, Q(1, 2)), vector((48,), Q(1)) + same_modes(modes, x, lift) + need(observe(modes, x) == TARGET and distance(x, lift) == 1, "attainment") + records = corner_census(modes, x) + count = scaled_fixtures(modes, x, lift) + rejected = controls(modes, raw, source["sha256"], x, lift) + paths = sorted(HERE.iterdir()) + need(len(paths) <= 32 and all(p.is_file() and not p.is_symlink() for p in paths), + "bounded regular package inventory") + hashes = {p.name: hashlib.sha256(bounded_read(p)).hexdigest() for p in paths} + receipt = {"minimum_radius": "1", "support": SUPPORT, "integer_lift": 48, + "target_modes": TARGET, "corners": records, "feasible_corners": 0, + "scaled_translated_fixtures": count, "controls": rejected, + "source_sha256": source["sha256"], "package_sha256": hashes} + print(json.dumps(receipt, sort_keys=True)) + print("PASS_MODE_PRESERVING_ROUNDING radius=1 corners=16 fixtures=" + + str(count) + " controls=" + str(len(rejected)) + " no_new_kappa") + + +if __name__ == "__main__": + verify()