From 937b132f3f143ce0f2621b3b12e1ebc413e66730 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 14 Oct 2026 21:57:18 +0100 Subject: [PATCH] feat(research): price escape from refined P104 intervals --- .../p104-refinement-rank-budget/EXPECTED.json | 53 ++++ .../p104-refinement-rank-budget/README.md | 103 +++++++ .../p104-refinement-rank-budget/SOURCES.json | 36 +++ .../p104-refinement-rank-budget/TASK.json | 100 +++++++ .../p104-refinement-rank-budget/VERIFY.json | 33 +++ .../test_verify.py | 138 ++++++++++ .../p104-refinement-rank-budget/verify.py | 256 ++++++++++++++++++ 7 files changed, 719 insertions(+) create mode 100644 research/p104-refinement-rank-budget/EXPECTED.json create mode 100644 research/p104-refinement-rank-budget/README.md create mode 100644 research/p104-refinement-rank-budget/SOURCES.json create mode 100644 research/p104-refinement-rank-budget/TASK.json create mode 100644 research/p104-refinement-rank-budget/VERIFY.json create mode 100644 research/p104-refinement-rank-budget/test_verify.py create mode 100644 research/p104-refinement-rank-budget/verify.py diff --git a/research/p104-refinement-rank-budget/EXPECTED.json b/research/p104-refinement-rank-budget/EXPECTED.json new file mode 100644 index 0000000000..71cdafbf8e --- /dev/null +++ b/research/p104-refinement-rank-budget/EXPECTED.json @@ -0,0 +1,53 @@ +{ + "conditional_no_progress_credit_budget": { + "added_rank_lower_bound_per_call": 48, + "baseline_rank_mass": 60408, + "calls": 9, + "capacity": 60736, + "completed_rank_mass_lower_bound": 60840, + "credit_needed_for_strict_positive_saving_gt": "104/9", + "headroom_per_call": "328/9", + "roles": 832, + "width": 73, + "zero_saving_moment_lower_bound": "585/584" + }, + "original_boundary_progress": 2312, + "original_entering_crossings": 8, + "original_local_rank_mass": 2368, + "original_operations": { + "add": 2624, + "copy": 8, + "erase": 8, + "transport": 1410, + "zero": 8 + }, + "other_side_sources": 56, + "rejected_controls": [ + "uncharged_bridge", + "nonnested_bridge", + "new_interval_is_not_original", + "ninth_original_descent", + "false_original_rank" + ], + "status": "PASS_P104_REFINEMENT_RANK_BUDGET", + "survivor_lines": [ + 95, + 127, + 243, + 383, + 447, + 486, + 500, + 502 + ], + "survivor_span_dimension": 8, + "target_side_sources": 48, + "target_side_targets": 104, + "transport_occurrences": 1410, + "upward_interval_cases": { + "last_step_to_full": 144, + "lower_has_two_survivors": 136, + "upper_has_at_most_one_survivor": 701, + "upper_inside_hull": 421 + } +} diff --git a/research/p104-refinement-rank-budget/README.md b/research/p104-refinement-rank-budget/README.md new file mode 100644 index 0000000000..778291e4f9 --- /dev/null +++ b/research/p104-refinement-rank-budget/README.md @@ -0,0 +1,103 @@ +# P104 nested refinements need at least 48 added paid ranks + +Identity completion in the model below requires **at least 48 added paid ranks per call**. Under the retained no-progress-credit coverage contract, the completed zero-saving moment is at least **585/584 > 1**. This excludes a positive saving within that contract, even with free scalar work and ideal idle packing. + +This is a quantitative extension of [Tairitsu-Aya's PR2136](https://github.com/CrocSwap/integer-mult-bounds/pull/2136), head `9b8689e0153e038b2c1179b06026adfaa7f7593b`. Its survivor separator and 56-array unaugmented bound are not new here. The new step prices arbitrary added nested transports around arbitrary refinements of the retained intervals. The bound is not claimed sharp. There is no new supplier or kappa. + +## Model and boundary + +The input is the 4,058-event PR1972 channel retained by PR1991 at `research/p104-native-channel/inputs/LOWRANK-WITNESS.json`, SHA256 `0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e`. It implements the low-rank `G/2` channel, not identity. + +Retain each of its 1,410 transport occurrences as a single-array obligation. Replace any occurrence `L -> U` by an arbitrary monotone nested chain between those same endpoints. Each original obligation is consumed once and cannot branch into independent arrays. Grant arbitrary valid interleaving, common-chart linear resynthesis, and arbitrary fresh source-independent storage, including same-chart copy/discard. Scalar coefficients and dirty restoration restrictions are relaxed for this lower bound. Source and final target endpoints remain fixed. + +In addition, allow arbitrary **added** nested transport steps on any available arrays, including persistent buffers and new storage. A step between distinct charts has paid rank equal to their dimension difference, or a larger charge. Their total added rank is `B`. Added paths need not be globally monotone: every step is charged. Refining an original monotone interval preserves its original total rank. + +Every cross-chart operation must be either a retained obligation's refinement or an added paid step. No original obligation may be removed, fused away, duplicated or credited against the added bill. A changed producer, a free cross-chart map, or a branching original descent is outside this model. In particular, the replacement mechanisms in [Discussion2131](https://github.com/CrocSwap/integer-mult-bounds/discussions/2131) and [PR2139](https://github.com/CrocSwap/integer-mult-bounds/pull/2139) are not excluded. + +This differs from [Ross Richardson's PR2127](https://github.com/CrocSwap/integer-mult-bounds/pull/2127), head `befebf0f4ae7a3f69fe9c5e136262559dcac125f`, whose 96-added-transport bound keeps the original occurrences unsplit. Here arbitrary intermediate subspaces inside their nested intervals are allowed. Neither theorem justifies a new coverage credit. + +## Inherited separator, checked from the source + +Let `a_0,...,a_7` be the private descent survivor labels and `A` their binary span. The reconstructed survivor set is + +```text +{95, 127, 243, 383, 447, 486, 500, 502}. +``` + +It has dimension eight. Label a chart `W` target-side, or T, precisely when it is proper and either `W <= A` or it contains at least two survivors. All other charts are R, including the full chart. This uses binary subspace membership, not ordinary dot products on compressed labels. + +The verifier reconstructs literal XOR spans without importing a predecessor checker and confirms: + +- 56 initial singleton sources are R and the other 48 are T. +- All 104 final target hyperplanes are T. +- The eight original descents start outside A, end in their survivor line, and their starting hyperplanes contain exactly one survivor each. +- Every upward original interval satisfies one of the following sufficient conditions. + +| Condition, applied in order | Occurrences | +| --- | ---: | +| Upper chart contains at most one survivor | 701 | +| Upper chart is contained in A | 421 | +| Lower chart contains at least two survivors | 136 | +| Dimension-eight chart to full chart | 144 | + +These are PR2136's separator premises, independently reconstructed here. In the first case ascent cannot enter A from outside A, and no chart contains two survivors. In the second all charts are T. In the third every proper chart is T and full is R. The last case has no strict intermediate chart. Thus no upward refinement enters T from R. Each descending refinement enters A exactly once and cannot leave it again. It therefore crosses R to T exactly once, carrying one array, irrespective of its seven paid ranks. + +## Added-rank theorem + +Let each register carry a `d`-dimensional vector over a characteristic-zero field containing the native constants. Vary only the 56 R-side source inputs; fix the other inputs to zero. Every initial T-side register is independent of those inputs. + +Record an array whenever information crosses R to T. The original refined obligations contribute exactly eight such array positions. Each added strict transport step contributes at most one, and its paid rank is at least one. Consequently added steps contribute at most `B` positions, even when arbitrary common-chart copies, storage and feedback are allowed. + +Induction through execution shows that every T-side value is a linear function of transcript entries already received. T-to-R feedback can affect later entries, but cannot increase the number of entering positions. The final target dependence on the 56 varying inputs therefore has rank at most + +```text +rank(X_R -> Y) <= (8 + B)d. +``` + +Identity transfer on that source block has rank `56d`, so **B >= 48**. Invertible per-register native endpoint adapters do not change this rank. Granting non-restored dirty helpers only enlarges the class, so imposing restoration cannot invalidate the lower bound. + +This also covers subdivided **added** rank-r intervals. A strict monotone refinement has at most r steps, hence at most r entering positions. It is unsafe to count just one crossing per added obligation: the verifier exhibits a descending path from full to zero whose side sequence is `R,T,R,T`. Its ranks are `6,2,1`, so it enters twice but pays nine ranks. The theorem counts paid rank, not endpoint side changes or the number of new obligations. + +The transcript implication is a written proof, not a proof-assistant certificate. A single rank-r native child transports one whole array; it is not assumed to transport r independent arrays. Bounding its contribution by r is a favorable relaxation for the lower bound. + +## Conditional complete-mass screen + +Use the explicit no-progress-credit contract of [David Arias's PR2082](https://github.com/CrocSwap/integer-mult-bounds/pull/2082), head `60f4e337ffba470e09727dd435b1f1be3b67d03d`: width `m=73`, `W=8*104=832` families, `N=9` calls per replica, mandatory original coverage `72W+56N`, and no reduction of that baseline from the added transports. No chronological P104 hosting construction is asserted by this assumption. + +The independently recounted local mass is `2368 = 2312 + 56`. Monotone refinements preserve it. The complete replica bound is + +| Quantity | Rank mass | +| --- | ---: | +| Capacity `73*832` | 60,736 | +| Mandatory baseline `72*832+56*9` | 60,408 | +| Necessary addition `48*9` | 432 | +| Completed lower bound | 60,840 | + +Thus `M(0) >= 60840/60736 = 585/584`. For every admissible child rank `0 < r <= 73` and saving `0 <= a < 1`, `(r/73)^(1-a) >= r/73`. No regrouping of this paid mass or nonnegative overhead can restore acceptance. The 48-rank requirement exceeds the `328/9` per-call headroom. + +A changed coverage proof must credit **more than 104/9 rank units per call** even to make the raw moment strictly below one at this minimum added cost. In general it must credit more than `B-328/9`. This is a necessary condition, not permission to subtract that credit from idle work. A different template, removal/fusion of old obligations, or justified credit for new monotone progress needs a separate bill. Neither the rank theorem nor this conditional screen rules out all P104 suppliers. + +## Reproduce + +Standard-library Python, no network or producer/compiler imports: + +```sh +python3.12 -I -B research/p104-refinement-rank-budget/verify.py +python3.12 -I -O -B research/p104-refinement-rank-budget/verify.py +python3.12 -I -B research/p104-refinement-rank-budget/test_verify.py +python3.12 scripts/research_package.py --package research/p104-refinement-rank-budget +``` + +The default verifier is read-only and compares the entire computed receipt with `EXPECTED.json`. `--out NEW_FILE` writes exclusively. The registered hook runs both assertion modes and the CLI/export tests. Source pins and task provenance are in `SOURCES.json` and `TASK.json`. + +Five semantic controls reject uncharged or nonnested bridges, treating a new crossing interval as an old interval, a ninth old descent and a falsified original rank. Positive controls exhibit a real paid bypass and the two-entry descending path. Nine tests check normal/optimized replay, missing/corrupt/oversized input, receipt corruption, read-only behavior, exclusive output and the two-entry counterexample. No native phase, original scalar endpoint, chronological owners, precision/tape, all-size or full selected cold replay is newly checked. The selected record is unchanged. + +## Open next questions + +A useful next candidate must either remove or fuse an original obligation, or justify enough new coverage credit to overcome this bound. Start by identifying the exact displaced idle progress and a complete source/target path with independent dirty inputs. The blocker is a physical hosting/coverage lemma, not the rational mass calculation. `TASK.json` records the structured question. Computing the sharp capacity of the refinement-only model is not needed for this no-credit decision and is not proposed as a separate task. + +## Credit and engineering limits + +Nick Petalas prepared the added-rank implication and conditional budget extension. Tairitsu-Aya/PR2136 supplies the interval separator. Ross Richardson/PR2127, David Arias/PR2082, Jeremy Diviney/PR2113 and Adam Gall/PR2090 supply the earlier access cuts. Rohan Arun/PR1972 supplies the channel, Chafik Boukhalfa/PR1991 its native realization, and Adam Gall/PR1940 its schedule. Geometry credit continues through Josie Elliston/PR1071, Ali Romman/PR1125 and the lineage retained by PR1991. The coverage model retains Dominik Scholz's paired-chain model, Sagar Thakrar's PR1012 and Douglas Colkitt's PR1240. No predecessor files are modified or vendored. Apache-2.0. + +The verifier uses no recursion and has functions below 60 lines. Source geometry is fixed to nine bits, 280 persistent roles and 4,058 events. Python's managed allocation is a Power of Ten rule-3 deviation; live space sets contain at most 512 labels and at most 1,410 transport records are retained. Tests use one bounded subprocess at a time with a 30-second timeout, scoped temporary storage and one explicit dynamic module import. The verifier's four indirect control calls have fixed local targets. These are scoped rule-8/9 deviations; no runtime registration or external code loading is used. Follow up with direct calls if that fixed control table changes. Python warnings are errors in the registered CLI tests. No static type checker or linter was available locally; no repository-wide configuration was changed. diff --git a/research/p104-refinement-rank-budget/SOURCES.json b/research/p104-refinement-rank-budget/SOURCES.json new file mode 100644 index 0000000000..926769b3c6 --- /dev/null +++ b/research/p104-refinement-rank-budget/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/p104-native-channel/README.md", + "usage": "input", + "git_blob": "f187d1ac0b7792d08d2dedf4561380b798e541b5", + "sha256": "ef874f86415c98b553bda9199d5f8f2f7a4dd4f6a23e53712c3c1f7268ec5b23" + }, + { + "path": "research/p104-native-channel/inputs/LOWRANK-RESULT.json", + "usage": "input", + "git_blob": "cbd1c6bdc9e34b25c64b2636ccd6acd2392232d4", + "sha256": "7143ec7780f6f38a8c294df8009c3621936b281d05ae79946ce22f581b73d1b1" + }, + { + "path": "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "usage": "input", + "git_blob": "86beaf424e9f0f800ae3a62797d94ec9386b7706", + "sha256": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e" + } + ] +} diff --git a/research/p104-refinement-rank-budget/TASK.json b/research/p104-refinement-rank-budget/TASK.json new file mode 100644 index 0000000000..cd1be4c94a --- /dev/null +++ b/research/p104-refinement-rank-budget/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "p104-side-correction", + "question": "Can the native P104 low-rank channel be completed with a legal, fully charged I-G/2 side correction?", + "starting_points": [ + "research/p104-native-channel/README.md", + "research/p104-native-channel/PROOF.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct one side-correction word at an explicit chronological cut with the needed frames still available.", + "Derive a lower bound on the side correction and hosting costs that decides whether this channel can beat the selected budget." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the P104 open next questions and its fixed local histogram; inspect why appending I-G/2 after source completion is not justified. #1991 supplies the checked native channel, not the missing correction.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Choose one exact side-correction cut and bound its allowed cost from a favorable completed moment at a declared target. Stop or hand off if the necessary source/target access cannot be justified or even the optimistic total misses the target.", + "bottleneck_link": "Completing an already realized changed channel tests a concrete construction opportunity, instead of refining the incumbent packing. A positive local result still needs global and all-size admission.", + "allowed_variations": [ + "One correction factorization, one chronological cut, or one explicit hosting obstruction.", + "A changed correction schedule with an updated full bill and native frame contract." + ], + "scope_change_triggers": [ + "Recompiling the already certified low-rank channel without closing a new obligation.", + "Treating a pending ancestor, local histogram or unpriced side correction as an admitted global supplier." + ], + "overlap_terms": [ + "P104", + "I-G/2", + "side correction", + "native channel", + "1972", + "1991" + ] + }, + "scope_status": "changed", + "actual_scope": "Price escape from PR2136's survivor separator when original P104 transport obligations admit arbitrary nested refinements, with arbitrary added nested transports and source-independent storage.", + "scope_change_reason": "Fresh overlap covers terminal and frozen-path corrections. This extends PR2136's unpriced refinement obstruction to an added-rank lower bound and a conditional full-mass decision; it does not construct the task card's supplier.", + "bottleneck_link": "A 48-rank necessary addition exceeds the retained 328/9 no-progress-credit headroom, so merely subdividing the old paths plus adding uncredited transports cannot complete an improving supplier.", + "budget_minutes": 60, + "stop_rule": "Stop after the added-rank implication, exact no-credit full-mass screen and meaningful verifier controls. No sharp-capacity search, native construction or supplier adoption.", + "outcome": "negative-result", + "evidence": "README.md proves B>=48; verify.py independently reconstructs the inherited separator premises and produces EXPECTED.json, including the exact 585/584 zero-saving moment lower bound.", + "author": "Nick Petalas", + "ai_assistance": "Omitted under the contributor's attribution policy.", + "assignment_nonce": "eec2345ed4f51606ac0c25c5bbe37f74", + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2144", + "upstream_checkpoint": { + "commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "checked_at_utc": "2026-10-14T20:54:12Z", + "change_from_scientific_base": "none" + }, + "overlap_checkpoint": { + "checked_at_utc": "2026-10-14T20:54:12Z", + "open_prs": 399, + "discussion_records": 816, + "complete_pagination": true, + "warnings": [], + "limits": "Open PR titles/bodies and Discussion bodies/replies, local package notes and ledger; not arbitrary code diffs. The nearest predecessor heads were rechecked live and unchanged." + }, + "verification": { + "environment": "Linux x86_64, CPython 3.12.15 and 3.13.5, standard library only", + "commands": [ + "python3.12 scripts/research_package.py --package research/p104-refinement-rank-budget", + "python3.12 -I -O -X dev -W error -B research/p104-refinement-rank-budget/test_verify.py", + "python3.12 -B -m unittest discover -s tests -p 'test_research_*.py'", + "python3 -I -O -X dev -W error -B research/p104-refinement-rank-budget/verify.py", + "python3.12 -B scripts/research_baseline.py" + ], + "results": "Registered normal/optimized replay, nine tests in both assertion modes, 65 research workflow tests, Python 3.13 optimized replay and selected source bindings pass.", + "unrun_obligations": "No native phases, original scalar endpoint, owners/hosting, precision/tape, all-size lifting, proof-assistant theorem or full selected cold replay." + }, + "predecessor_heads": { + "2136": "9b8689e0153e038b2c1179b06026adfaa7f7593b", + "2127": "befebf0f4ae7a3f69fe9c5e136262559dcac125f", + "2082": "60f4e337ffba470e09727dd435b1f1be3b67d03d", + "1972": "fd82d172f46933fd253c2c6de4bd5eaff5429cfd" + }, + "open_questions": [ + { + "question": "Can a physically hosted corrected word replace an original obligation or prove enough credited progress to escape the 48-rank/no-credit bound?", + "why_it_matters": "Under this template, even a minimum-rank repair must credit more than 104/9 ranks per call to make the raw moment strictly favorable.", + "first_step": "Identify a specific displaced idle obligation and show its legal source/target path and arbitrary dirty-state restoration, then recompute the complete profile.", + "blocked_by": "No coverage/hosting lemma currently credits that progress; a graph bypass alone is insufficient." + } + ] +} diff --git a/research/p104-refinement-rank-budget/VERIFY.json b/research/p104-refinement-rank-budget/VERIFY.json new file mode 100644 index 0000000000..52376acee1 --- /dev/null +++ b/research/p104-refinement-rank-budget/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-native-channel/README.md", + "research/p104-native-channel/inputs/LOWRANK-RESULT.json", + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-X", "dev", "-W", "error", "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Reconstruct source-bound separator premises, added-rank lower bound, full no-credit mass and semantic controls." + }, + { + "argv": ["{python}", "-I", "-O", "-X", "dev", "-W", "error", "-B", "{package}/verify.py"], + "timeout_seconds": 60, + "checks": "Identical full receipt with Python assertions disabled." + }, + { + "argv": ["{python}", "-I", "-X", "dev", "-W", "error", "-B", "{package}/test_verify.py"], + "timeout_seconds": 60, + "checks": "Nine CLI/export and semantic tests, including malformed/oversized sources and exclusive output." + } + ] +} diff --git a/research/p104-refinement-rank-budget/test_verify.py b/research/p104-refinement-rank-budget/test_verify.py new file mode 100644 index 0000000000..6118cf1b63 --- /dev/null +++ b/research/p104-refinement-rank-budget/test_verify.py @@ -0,0 +1,138 @@ +#!/usr/bin/env python3 +"""CLI and semantic failure tests for the scoped P104 rank-budget checker.""" +from __future__ import annotations + +from fractions import Fraction +import hashlib +import importlib.util +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def load_checker(): + spec = importlib.util.spec_from_file_location("p104_rank_budget", PACKAGE / "verify.py") + if spec is None or spec.loader is None: + raise RuntimeError("cannot load the local checker") + checker = importlib.util.module_from_spec(spec) + spec.loader.exec_module(checker) + return checker + + +class ReplayTests(unittest.TestCase): + def setUp(self): + self.temporary = tempfile.TemporaryDirectory(prefix="p104-budget-test-") + self.addCleanup(self.temporary.cleanup) + self.root = Path(self.temporary.name) + self.package = self.root / PACKAGE.relative_to(ROOT) + self.package.mkdir(parents=True) + for filename in ("verify.py", "SOURCES.json", "EXPECTED.json"): + shutil.copyfile(PACKAGE / filename, self.package / filename) + sources = json.loads((PACKAGE / "SOURCES.json").read_text()) + self.files = list(self.package.iterdir()) + for record in sources["files"]: + if record["usage"] == "input": + destination = self.root / record["path"] + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / record["path"], destination) + self.files.append(destination) + + def run_cli(self, *arguments, optimized=False): + flags = ["-I", "-X", "dev", "-W", "error", "-B"] + if optimized: + flags.append("-O") + return subprocess.run( + [sys.executable, *flags, str(self.package / "verify.py"), *arguments], + cwd=self.root, text=True, capture_output=True, timeout=30, check=False, + ) + + def assert_pass(self, process): + self.assertEqual(process.returncode, 0, process.stderr) + self.assertEqual(process.stderr, "") + result = json.loads(process.stdout) + self.assertEqual(result["status"], "PASS_P104_REFINEMENT_RANK_BUDGET") + bill = result["conditional_no_progress_credit_budget"] + self.assertEqual(bill["added_rank_lower_bound_per_call"], 48) + self.assertEqual(bill["zero_saving_moment_lower_bound"], "585/584") + self.assertEqual(bill["credit_needed_for_strict_positive_saving_gt"], "104/9") + self.assertEqual(len(result["rejected_controls"]), 5) + return result + + def test_normal_replay_is_read_only(self): + before = {path: hashlib.sha256(path.read_bytes()).digest() for path in self.files} + self.assert_pass(self.run_cli()) + self.assertEqual({path: hashlib.sha256(path.read_bytes()).digest() for path in self.files}, before) + self.assertEqual({path for path in self.root.rglob("*") if path.is_file()}, set(self.files)) + + def test_optimized_replay(self): + self.assert_pass(self.run_cli(optimized=True)) + + def test_missing_source_rejects(self): + source = self.root / "research/p104-native-channel/inputs/LOWRANK-WITNESS.json" + source.unlink() + process = self.run_cli() + self.assertNotEqual(process.returncode, 0) + self.assertIn("FileNotFoundError", process.stderr) + self.assertIn("LOWRANK-WITNESS.json", process.stderr) + + def test_corrupt_source_rejects_before_geometry(self): + source = self.root / "research/p104-native-channel/inputs/LOWRANK-WITNESS.json" + source.write_bytes(b"not json") + process = self.run_cli() + self.assertNotEqual(process.returncode, 0) + self.assertIn("source hash mismatch", process.stderr) + self.assertNotIn("JSONDecodeError", process.stderr) + + def test_oversized_source_rejects_before_hashing(self): + source = self.root / "research/p104-native-channel/inputs/LOWRANK-WITNESS.json" + source.write_bytes(b"x" * 1_048_577) + process = self.run_cli() + self.assertNotEqual(process.returncode, 0) + self.assertIn("input size limit", process.stderr) + self.assertNotIn("source hash mismatch", process.stderr) + + def test_count_preserving_receipt_corruption_rejects(self): + path = self.package / "EXPECTED.json" + receipt = json.loads(path.read_text()) + receipt["survivor_lines"][0] ^= 1 + path.write_text(json.dumps(receipt)) + process = self.run_cli() + self.assertNotEqual(process.returncode, 0) + self.assertIn("complete expected receipt", process.stderr) + + def test_output_is_exclusive(self): + path = self.root / "receipt.json" + result = self.assert_pass(self.run_cli("--out", str(path))) + self.assertEqual(json.loads(path.read_text()), result) + original = path.read_bytes() + process = self.run_cli("--out", str(path)) + self.assertNotEqual(process.returncode, 0) + self.assertIn("FileExistsError", process.stderr) + self.assertEqual(path.read_bytes(), original) + + def test_raw_mass_boundary(self): + checker = load_checker() + self.assertEqual(Fraction(checker.budget(44, 8)["zero_saving_moment_lower_bound"]), + Fraction(15183, 15184)) + self.assertEqual(Fraction(checker.budget(45, 8)["zero_saving_moment_lower_bound"]), + Fraction(60741, 60736)) + + def test_two_entering_crossings_need_rank_not_endpoint_count(self): + checker = load_checker() + survivors = frozenset(1 << i for i in range(8)) + hull = frozenset(range(256)) + path = [checker.FULL, checker.span([256, 1, 2]), checker.span([256]), checker.span([])] + self.assertEqual(checker.charged_path(path, [6, 2, 1], survivors, hull), 2) + with self.assertRaisesRegex(ValueError, "charged its rank"): + checker.charged_path(path, [1, 1, 1], survivors, hull) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/p104-refinement-rank-budget/verify.py b/research/p104-refinement-rank-budget/verify.py new file mode 100644 index 0000000000..0be5b83a61 --- /dev/null +++ b/research/p104-refinement-rank-budget/verify.py @@ -0,0 +1,256 @@ +#!/usr/bin/env python3 +"""Check the P104 survivor separator and its added-rank budget. + +Nick Petalas. Apache-2.0. The separator is Tairitsu-Aya's PR2136 result; +the added-rank transcript implication is proved in README.md. +No predecessor verifier/compiler imports, floating point, or network access. +""" +from __future__ import annotations + +import argparse +from collections import Counter +from fractions import Fraction +import hashlib +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +WITNESS = "research/p104-native-channel/inputs/LOWRANK-WITNESS.json" +RESULT = "research/p104-native-channel/inputs/LOWRANK-RESULT.json" +FULL = frozenset(range(512)) + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def span(vectors: list[int]) -> frozenset[int]: + require(len(vectors) <= 9, "at most nine basis vectors") + values = {0} + for vector in vectors: + require(type(vector) is int and 0 < vector < 512, "nine-bit label") + require(vector not in values, "independent frame basis") + values.update(value ^ vector for value in tuple(values)) + return frozenset(values) + + +def dimension(space: frozenset[int]) -> int: + return len(space).bit_length() - 1 + + +def read_inputs() -> dict: + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + records = [item for item in manifest["files"] if item["usage"] == "input"] + require(len(records) == 3, "three declared live inputs") + inputs = {} + for item in records: + path = ROOT / item["path"] + require(path.stat().st_size <= 1_048_576, "input size limit") + raw = path.read_bytes() + require(hashlib.sha256(raw).hexdigest() == item["sha256"], + "source hash mismatch: " + item["path"]) + if item["path"].endswith(".json"): + inputs[item["path"]] = json.loads(raw) + return inputs + + +def trace(word: dict) -> tuple: + entry = {name: span(rows) for name, rows in word["initial_frames"].items()} + final = {name: span(rows) for name, rows in word["final_frames"].items()} + require(len(entry) == 280 and entry.keys() == final.keys(), "280 persistent roles") + require(all(name in entry for name in [f"X{i}" for i in range(104)] + + [f"Y{i}" for i in range(104)]), "source and target role names") + live, moves, private, kinds = dict(entry), [], [], Counter() + require(len(word["program"]) == 4058, "4058 original events") + for index, event in enumerate(word["program"]): + op, name = event[:2] + kinds[op] += 1 + if op == "transport": + before, after = span(event[2]), span(event[3]) + require(live[name] == before, "transport continuity") + require(before < after or after < before, "strict nested transport") + rank = abs(dimension(after) - dimension(before)) + require(type(event[4]) is int and event[4] == rank, "transport rank") + moves.append((index, name, before, after, rank)) + live[name] = after + elif op == "zero": + require(name == "C" and name not in live, "fresh private C") + live[name] = span(event[-1]) + private.append([op]) + elif op in ("add", "copy"): + require(live[name] == live[event[2]] == span(event[-1]), "common chart") + if op == "copy": + require(name == "C" and private[-1] == ["zero"], "private copy") + private[-1].append(op) + elif op == "erase": + require(name == "C" and live[name] == span(event[-1]), "private discard") + require(private[-1] == ["zero", "copy"], "private lifetime") + private[-1].append(op) + del live[name] + else: + raise ValueError("unknown operation") + require(live == final, "final frame endpoints") + require(len(private) == 8 and all(p == ["zero", "copy", "erase"] for p in private), + "eight private lifetimes") + return entry, final, moves, kinds + + +def separator(moves: list[tuple]) -> tuple: + drops = [move for move in moves if move[3] < move[2]] + require(len(drops) == 8, "eight original descents") + lines = [] + for _, name, before, after, rank in drops: + require(name == "C" and len(before) == 256 and len(after) == 2 and rank == 7, + "private hyperplane-to-line descent") + lines.append(next(value for value in after if value)) + hull = span(lines) + survivors = frozenset(lines) + for _, _, before, after, _ in drops: + require(len(before & survivors) == 1 and not before <= hull and after <= hull, + "descent enters survivor span with exactly one survivor") + return drops, survivors, hull + + +def target_side(space: frozenset[int], survivors: frozenset[int], + hull: frozenset[int]) -> bool: + return space != FULL and (space <= hull or len(space & survivors) >= 2) + + +def interval_case(lower: frozenset[int], upper: frozenset[int], + survivors: frozenset[int], hull: frozenset[int]) -> str: + require(lower < upper, "upward nested interval") + if len(upper & survivors) <= 1: + return "upper_has_at_most_one_survivor" + if upper <= hull: + return "upper_inside_hull" + if len(lower & survivors) >= 2: + return "lower_has_two_survivors" + if len(lower) == 256 and upper == FULL: + return "last_step_to_full" + raise ValueError("interval can bypass the inherited separator") + + +def budget(outside_sources: int, original_crossings: int) -> dict: + needed = max(0, outside_sources - original_crossings) + width, roles, calls, copy = 73, 8 * 104, 9, 56 + capacity = width * roles + baseline = (width - 1) * roles + calls * copy + completed = baseline + calls * needed + return { + "width": width, "roles": roles, "calls": calls, + "baseline_rank_mass": baseline, "capacity": capacity, + "headroom_per_call": str(Fraction(capacity - baseline, calls)), + "added_rank_lower_bound_per_call": needed, + "completed_rank_mass_lower_bound": completed, + "zero_saving_moment_lower_bound": str(Fraction(completed, capacity)), + "credit_needed_for_strict_positive_saving_gt": str( + Fraction(completed - capacity, calls)), + } + + +def analyze(word: dict, source_result: dict) -> dict: + entry, final, moves, kinds = trace(word) + drops, survivors, hull = separator(moves) + classes = Counter(interval_case(before, after, survivors, hull) + for _, _, before, after, _ in moves if before < after) + sources = [entry[f"X{i}"] for i in range(104)] + targets = [final[f"Y{i}"] for i in range(104)] + require(all(len(space) == 2 for space in sources), "104 singleton sources") + require(all(len(space) == 256 and target_side(space, survivors, hull) + for space in targets), "104 target-side hyperplanes") + outside = sum(not target_side(space, survivors, hull) for space in sources) + profile = Counter(rank for _, _, _, _, rank in moves) + mass = sum(rank * count for rank, count in profile.items()) + progress = sum(dimension(final[name]) - dimension(space) + for name, space in entry.items()) + require({str(k): v for k, v in profile.items()} == source_result["paid_profile"], + "recounted profile agrees with predecessor receipt") + require(mass == source_result["rank_mass"] and mass - progress == 56, + "original rank mass is boundary progress plus COPY56") + return { + "status": "PASS_P104_REFINEMENT_RANK_BUDGET", + "original_operations": dict(sorted(kinds.items())), + "transport_occurrences": len(moves), "upward_interval_cases": dict(sorted(classes.items())), + "survivor_lines": sorted(survivors), "survivor_span_dimension": dimension(hull), + "target_side_sources": 104 - outside, "other_side_sources": outside, + "target_side_targets": len(targets), "original_entering_crossings": len(drops), + "original_local_rank_mass": mass, "original_boundary_progress": progress, + "conditional_no_progress_credit_budget": budget(outside, len(drops)), + } + + +def charged_path(path: list[frozenset[int]], ranks: list[int], + survivors: frozenset[int], hull: frozenset[int]) -> int: + require(1 <= len(ranks) <= 9 and len(path) == len(ranks) + 1, "bounded chain") + direction = dimension(path[-1]) - dimension(path[0]) + require(direction != 0, "strict monotone path endpoints") + arrivals = 0 + for before, after, rank in zip(path, path[1:], ranks): + require((before < after if direction > 0 else after < before), "monotone chain") + require(type(rank) is int and rank == abs(dimension(after) - dimension(before)), + "every strict step is charged its rank") + arrivals += not target_side(before, survivors, hull) and target_side(after, survivors, hull) + require(arrivals <= sum(ranks), "entering transcript capacity is bounded by paid rank") + return arrivals + + +def controls(word: dict, receipt: dict) -> list[str]: + _, _, moves, _ = trace(word) + drops, survivors, hull = separator(moves) + labels = sorted(survivors) + outsider = min(FULL - hull) + one, two, three = span([outsider]), span([outsider, labels[0]]), span([outsider, *labels[:2]]) + require(charged_path([one, two, three], [1, 1], survivors, hull) == 1, "actual added bridge") + # Full-to-zero can enter T twice. Counting each new obligation only once is unsafe. + require(charged_path([FULL, three, one, span([])], [6, 2, 1], survivors, hull) == 2, + "two-entry descending counterexample") + rejected = [] + for name, expected_error, operation in ( + ("uncharged_bridge", "every strict step is charged its rank", + lambda: charged_path([two, three], [0], survivors, hull)), + ("nonnested_bridge", "monotone chain", + lambda: charged_path([one, span(labels[:2])], [1], survivors, hull)), + ("new_interval_is_not_original", "interval can bypass the inherited separator", + lambda: interval_case(one, three, survivors, hull)), + ("ninth_original_descent", "eight original descents", lambda: separator(moves + drops[:1])), + ): + try: + operation() + except ValueError as error: + require(str(error) == expected_error, "control fails for its intended reason: " + name) + rejected.append(name) + else: + raise ValueError("control accepted: " + name) + changed = json.loads(json.dumps(word)) + changed["program"][moves[0][0]][4] += 1 + try: + trace(changed) + except ValueError as error: + require(str(error) == "transport rank", "rank control fails for its intended reason") + rejected.append("false_original_rank") + else: + raise ValueError("false rank accepted") + bill = receipt["conditional_no_progress_credit_budget"] + require(bill["added_rank_lower_bound_per_call"] == 48, "56 independent inputs minus eight crossings") + require(Fraction(bill["zero_saving_moment_lower_bound"]) == Fraction(585, 584), "literal full bill") + return rejected + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--out", type=Path, help="write a receipt exclusively to a new file") + args = parser.parse_args() + inputs = read_inputs() + receipt = analyze(inputs[WITNESS], inputs[RESULT]) + receipt["rejected_controls"] = controls(inputs[WITNESS], receipt) + require(receipt == json.loads((PACKAGE / "EXPECTED.json").read_text()), "complete expected receipt") + if args.out: + with args.out.open("x", encoding="utf-8") as handle: + handle.write(json.dumps(receipt, sort_keys=True, indent=2) + "\n") + print(json.dumps(receipt, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()