From 4d772802fe86e5185d5468db86b36472e6c81b96 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 16 Oct 2026 17:40:04 +0100 Subject: [PATCH] feat(research): certify P104 fixed-pair dependency obstruction --- .../p104-endpoint-completion-flow/README.md | 197 +++++++++ .../p104-endpoint-completion-flow/RESULT.json | 170 ++++++++ .../SOURCES.json | 36 ++ .../p104-endpoint-completion-flow/TASK.json | 128 ++++++ .../p104-endpoint-completion-flow/VERIFY.json | 49 +++ .../decisions.tsv | 8 + .../independent.py | 377 ++++++++++++++++++ .../test_verify.py | 164 ++++++++ .../p104-endpoint-completion-flow/verify.py | 276 +++++++++++++ 9 files changed, 1405 insertions(+) create mode 100644 research/p104-endpoint-completion-flow/README.md create mode 100644 research/p104-endpoint-completion-flow/RESULT.json create mode 100644 research/p104-endpoint-completion-flow/SOURCES.json create mode 100644 research/p104-endpoint-completion-flow/TASK.json create mode 100644 research/p104-endpoint-completion-flow/VERIFY.json create mode 100644 research/p104-endpoint-completion-flow/decisions.tsv create mode 100644 research/p104-endpoint-completion-flow/independent.py create mode 100644 research/p104-endpoint-completion-flow/test_verify.py create mode 100644 research/p104-endpoint-completion-flow/verify.py diff --git a/research/p104-endpoint-completion-flow/README.md b/research/p104-endpoint-completion-flow/README.md new file mode 100644 index 0000000000..0299d82a22 --- /dev/null +++ b/research/p104-endpoint-completion-flow/README.md @@ -0,0 +1,197 @@ +# P104 dependency obstruction for all intermediate flag completions + +Changing intermediate bases cannot turn PR2981's fixed 208 matched endpoint +pairs into an X-only monotone correction program. Even an optimistic dependency +graph leaves **3,095 of the 4,992 required coefficients unreachable**. For example, +the correction requires coefficient `-1/2` from `X4` into `Y0`, while every +permitted completion forces that added coefficient to zero. + +This is a scoped obstruction for one named endpoint pairing. PR2981 correctly +certifies static covers, without claiming a correction program. Other pairings, +other endpoint planes, extra lifetimes and changed access contracts are outside +this result. No new lifetime floor, supplier or kappa follows. + +## Contract and exact statement + +Pin PR2981 `3d24b92d8ba057b57cb2d480170ec407520e6882` and its original +PR1972/1991 P104 data paths. For each of its 208 helper records retain only: + +- Its dimension-one source line `L`, dimension-two departure plane `A`, + dimension-seven arrival plane `B` and dimension-eight target hyperplane `H`. +- ZERO and FULL at dimensions zero and nine. + +Allow any complete unit-step flag between these frames. In particular, each +dimension-three through dimension-six frame may be any `V` with `A <= V <= B`. +The published intermediate bases are discarded. The source and target indices +and both endpoint cover choices remain fixed. Changing bases within the same +endpoint spaces is included; changing the endpoint matching is not. + +Retain PR2920/2353's X-only monotone correction contract. X is immutable and +available at its original visited frames. Y is unread and receives additions +at its original visited frames. New helpers have independent arbitrary dirty +entrances and increasing frames. Scalar operations are equal-frame linear +operations with fixed rational coefficients, including mixing, copies, clears +and rescalings. Transports preserve logical coefficient rows. There are no +additional lifetimes, source writes, target feedback, original helper/private +reads, descending transports or uncharged storage. Restoration is required by +the original contract, but is dropped in the relaxation below. + +Under this contract, no choice of intermediate flags, scalar coefficients or +chronological interleaving realizes the prescribed additive correction `I-G/2`. +The independently checked finite predicate is missing directed support, before +coefficient magnitudes, restoration and physical implementation are considered. + +## A necessary dependency graph + +Make nodes `(helper, d)` for dimensions one through eight, with a directed +edge from each node to the next dimension of that helper. At each dimension, +grant a bidirectional contact between two helpers whenever some permitted +common frame exists. Inject source `s` at every node that could equal any +visited frame of `X_s`. Deliver to `Y_t` from every node that could equal any +visited frame of `Y_t`. Also include direct X-to-Y common-frame contacts. +The graph permits every visited data snapshot without checking its time. + +At fixed dimensions the permitted interval is `[V,V]`. At intermediate +dimensions it is `[A,B]`. Two intervals `[A,B]` and `[C,D]` admit a common +dimension-d frame exactly when + +```text +A <= D, C <= B, and dim(A+C) <= d <= dim(B intersect D). +``` + +Necessity follows from `A+C <= V <= B intersect D`. Conversely, those +containments and dimension bounds let a basis of `A+C` extend to d independent +vectors in `B intersect D`. Every resulting V can extend to a full flag within +each helper's fixed A and B. We grant contacts independently, even if one +helper could not realize their different frame choices in a single flag. +This makes the graph more permissive than any actual completion. + +For a particular legal word, map each register state to its helper/dimension +node. A nonzero source coefficient initially exists only on its immutable X +input. A transport follows an upward edge. An equal-frame linear operation +can propagate a source only through a granted contact; a copy, clear or +rescaling cannot create a missing source coefficient. Induction over the +scalar word therefore puts each actual coefficient's support inside graph +reachability. Cancellation can remove support but cannot create a path. +Independent dirty inputs have zero coefficients on all X coordinates, so +dropping their eventual restoration cannot invalidate this necessary test. +Unread targets are sinks and cannot supply further dependencies. + +The checker saturates connected contact components in each dimension, then +propagates upwards. It never propagates a late acquisition backwards. Dimension +zero has no X injection. Dimension nine has no Y delivery and no descending +edge, so neither omitted layer can create an additional source-to-target path. + +## Finite evidence and checks + +[RESULT.json](RESULT.json) retains every target's optimistic source support, +all layer counts and the exact missing-coefficient witness. Contacts at +dimensions one through eight number +`104, 23, 78, 141, 141, 91, 29, 104`. Of 4,992 nonzero entries of `I-G/2`, +1,897 have paths and 3,095 do not. A path is only a necessary condition; +the 1,897 reachable entries are not claimed constructively realizable. + +The primary checker reconstructs the original 4,058-event X/Y paths and uses +the interval criterion. A separately implemented checker enumerates all 374 +subspaces of each five-dimensional quotient `B/A`, lifts them to literal +binary frames and checks common-frame contacts directly. It independently +traces each source through the graph and compares the complete receipt. +Neither checker executes a predecessor implementation. + +Behavioral controls check the contact criterion against every subspace interval +in a three-dimensional binary space, actual CLI replay, an upward relay, +forbidden backward flow, direct X-to-Y access, changed intermediate bases, +Git-free exports, source corruption, changed support masks, duplicate JSON keys +and Boolean/integer confusion. These controls test access semantics and the +real verifier boundary rather than a new multiplication construction. + +The concurrent [fixed-full-flag audit][concurrent] concerns PR2981's exact +published intermediate bases. This contribution instead proves failure for +every intermediate completion of the same endpoint pairs. The two tests are +complementary. The reported program-level lifetime floors in PR2924 would +also exclude 208 helpers under their hypotheses; they are not replayed or +strengthened here. This explicit basis-sensitive test supplies a calibration +and a concrete failed dependency independently of those reported floors. + +## Reproduce and verification limits + +Python 3.12 or later, standard library only, from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/p104-endpoint-completion-flow +``` + +Direct checks also work on a Git-free source export: + +```sh +python3.12 -I -O -Werror -B research/p104-endpoint-completion-flow/verify.py +python3.12 -I -O -Werror -B research/p104-endpoint-completion-flow/independent.py +python3.12 -I -O -Werror -B research/p104-endpoint-completion-flow/test_verify.py +``` + +The primary marker is `PASS_P104_ENDPOINT_COMPLETION_FLOW required=4992 +unreachable=3095 all_intermediate_completions no_new_kappa`. +`verify.py --emit` regenerates the receipt to stdout without changing files. +[SOURCES.json](SOURCES.json) pins exact input bytes and historical provenance; +[TASK.json](TASK.json) records scope, live overlap and verification environment. +Evidence is locally checked with independent internal arithmetic/code review, +without independent human review or formal-kernel proof. Hosted CI is separate. +No native replay, rounded producer, physical hosting, complete cost invoice, +all-size proof or selected cold replay is supplied or required by this scoped +support obstruction. Frozen scientific packages and selected inputs are unchanged. + +## Open next questions + +Does a different compatible endpoint matching pass this necessary contact +test? It matters because static containment alone did not ensure acquisition +for the published matching. A first step is to choose one explicitly named +alternative and evaluate this same optimistic graph before scalar synthesis. +The current proof does not show that every matching fails. Passing this test +would still leave joint flag consistency, chronological acquisition, exact +coefficients, arbitrary dirty restoration and the complete physical bill open. +Do not start another construction campaign from a path-only positive result. +The structured handoff is in TASK.json. Family decision: finish this calibration +and stop; no matching search or construction expansion is included. + +## Credit and engineering notes + +Nick Petalas. Apache-2.0. Substantial automated assistance in analysis, +implementation, internal review and writing is disclosed in TASK.json. +No independent human review is claimed. + +Credit Nick Petalas/PR2981/2920/2909/2896 for the pinned covers and flags; +Arham Tahir's concurrent fixed-flag information-flow audit for the exact-basis +scope; Sudarsh Chaturvedi/PR2924 and Sagar Thakrar's mixer handoff for the +reported program-level floors; Hiroki Kumazaki/PR2889/2353 for the monotone +model; ywz65/PR2614 for departure access; Arham Tahir/PR2675/2682 for coupled +budgets; Philippe Van Velzen for relay constructions and pricing. Retain +Rohan Arun/PR1972, Chafik Boukhalfa/PR1991, Adam Gall/PR1940, Josie +Elliston/PR1071, Ali Romman/PR1125 and their geometry/native/compiler lineage. +No predecessor construction, cover theorem or lifetime floor is claimed as new. + +Build the Lever changed the deliverable to a rerunnable necessary-condition +checker. Prove It Works required literal subspace enumeration independent of +the interval formula. Test Behavior, Not Implementation required positive +relay/direct-access cases alongside rejected controls. Unslop shaped the prose. + +Power of Ten inspection covers only the new package's Python files. Loops are +bounded by 4,058 original events, 104 sources/targets, 208 helpers, eight useful +layers, nine basis vectors or 512 binary points. Each component search visits +at most 208 helper nodes. Checks remain enabled under optimized Python; +subprocess tests have 60-second timeouts and the registered commands are bounded. +Functions remain below 60 physical lines after formatting. No shared source or +repository diagnostic configuration is changed. + +Rule 3 deviation: Python allocates managed objects while checking. The fixed +domains, 2 MB JSON limits and at most 208 helpers bound collections; a resident +service would require fixed-capacity storage. The independent checker retains +at most 376 frames per helper, 78,208 literal masks of at most 512 bits, and +1,664 graph vertices. Its 104 source traversals each queue at most 1,664 nodes. +Rules 8/9 deviation: tests load one local verifier through Python's module +loader; the registered runner gives it a fresh bytecode namespace. JSON parsing +uses one fixed duplicate-key callback. The two mathematical CLIs import only +standard library code and read three authenticated JSON inputs. A stricter +untrusted service would need a static module boundary and a separate capacity audit. +Ruff, warning-as-error compilation and optimized replay cover touched code. + +[concurrent]: https://github.com/CrocSwap/integer-mult-bounds/discussions/2245#discussioncomment-18977808 diff --git a/research/p104-endpoint-completion-flow/RESULT.json b/research/p104-endpoint-completion-flow/RESULT.json new file mode 100644 index 0000000000..27b27986ac --- /dev/null +++ b/research/p104-endpoint-completion-flow/RESULT.json @@ -0,0 +1,170 @@ +{ + "helpers": 208, + "layers": [ + { + "components": 104, + "contacts": 104, + "dimension": 1, + "max_sources": 1 + }, + { + "components": 185, + "contacts": 23, + "dimension": 2, + "max_sources": 2 + }, + { + "components": 136, + "contacts": 78, + "dimension": 3, + "max_sources": 6 + }, + { + "components": 76, + "contacts": 141, + "dimension": 4, + "max_sources": 60 + }, + { + "components": 76, + "contacts": 141, + "dimension": 5, + "max_sources": 60 + }, + { + "components": 122, + "contacts": 91, + "dimension": 6, + "max_sources": 60 + }, + { + "components": 179, + "contacts": 29, + "dimension": 7, + "max_sources": 60 + }, + { + "components": 104, + "contacts": 104, + "dimension": 8, + "max_sources": 67 + } + ], + "reachable_required_pairs": 1897, + "required_pairs": 4992, + "schema_version": 1, + "scope": "All intermediate completions of fixed matched endpoint planes; optimistic untimed contacts, no restoration charge; no new kappa.", + "target_source_masks_hex": [ + "0x6c0fff086ffe25fffeed84122d", + "0x680fff086ffe25fffeed841229", + "0x780fff086ffe25fffeed84122b", + "0x680fff086ffe25fffeed841229", + "0x8000000000020000800040", + "0x680fff086ffe25fffeed841229", + "0x6a2fff086ffe25fffeed843269", + "0x20a182000a040004100005", + "0x40000000090280", + "0x680fff087fff25fffeed861a29", + "0x400000100100000000460800", + "0x400000000040000000490200", + "0x20a182000a040004100005", + "0x2200100000000000000006048", + "0x6a2fff086ffe25fffeed843269", + "0x80000000000000000000020000", + "0x100100000000160800", + "0x40000000098200", + "0x80000000000040000000090200", + "0x100100000002060800", + "0x81000000000000000000000", + "0x200000010000a000", + "0x780fff086ffe25fffeed841b29", + "0x680fff086ffe25fffeeda41239", + "0x680fff086ffe25fffeed841229", + "0x1020a183800a040004500000", + "0x680fffa9effe2ffffeed941229", + "0x680fff086ffe25fffeed841229", + "0x680fff086ffe25fffeed841229", + "0x680fff086ffe25fffeed841229", + "0x680fff086ffe25ffffeda43239", + "0xb000510002400", + "0x680fff086ffe25fffeed845229", + "0x681fff086ffe25fffeedc41229", + "0x680fff086ffe25fffeed841629", + "0x680fff086ffe65fffeed841229", + "0x680fff086ffe25fffeed841229", + "0x680fff086ffe25fffeed841229", + "0x680fffa9effe2ffffeed941229", + "0x20004000000000004000000080", + "0x20000100", + "0x40100410000400000002000000", + "0x2000000000094000100000002", + "0x40900400000400000000000000", + "0x6a0fff086ffeb5fffeed841229", + "0x680fff086ffe25fffeed841269", + "0x680fff086ffe2ffffefd841629", + "0x210012b000410000400", + "0x680fff086ffe25fffeed841229", + "0x6a0fff086ffeb5fffeed841229", + "0x680fff086ffe25fffeed841229", + "0x6a0fff086ffeb5fffeed849229", + "0x8800002100120000000000002", + "0x10010b000410060c00", + "0x4020a182000a050004100000", + "0x200b000410008400", + "0x690fff086ffe25fffeed841229", + "0x680fff086ffe25fffeed841229", + "0x680fff086ffe25fffeed841229", + "0x680fff086ffe25fffeeda41229", + "0x680fff086ffe25fffeed841229", + "0x100000018000000001400000", + "0x1020a183800a040004500000", + "0x684fff086ffe25fffeed841229", + "0x680fff0c6ffe25fffeed841229", + "0x680fff086ffe25fffeed841229", + "0x680fff086ffe2ffffefd841629", + "0x10004000000002000000", + "0x682fff086ffe25fffeed841229", + "0x680fff086ffe25fffeed841229", + "0x680fff086ffe25fffefd841229", + "0x20a382000a040004100000", + "0x6100120000000000000", + "0x680fff28effe25fffeed841229", + "0x41000000080000000400", + "0x22900120000000000000", + "0x41000000200000000000", + "0x780fff086ffe25fffeed841b29", + "0x20b182000a040004100000", + "0x680fff086ffe25fffeed841229", + "0x680fffa9effe2ffffeed941229", + "0x680fff086ffe25fffeed841229", + "0x20004000000000004040000000", + "0x680fff086ffe25fffeed841229", + "0x20a182000a040104100002", + "0x20200000000000000080010", + "0x680fff086ffe25fffeed845229", + "0x680fff086ffe25fffeed841229", + "0x4000000000010000000000000", + "0x8000000000002000800000", + "0x40120400000400000000000010", + "0x680fff086ffe25fffeed841229", + "0x680fff086ffe25fffeed841229", + "0x400000000000010000010000", + "0x1000080000000000000000000", + "0x6a2fff086ffe25fffeed843269", + "0x8800000000080000000000002", + "0x4000000000000001000000004", + "0x10000000401000000000000002", + "0x10000040000000000000000900", + "0x688fff086ffe25fffeed84122b", + "0x6a2fff086ffe25fffeed843269", + "0x680fff086ffe25fffeed841229", + "0x40100600000400000000080000" + ], + "unreachable_required_pairs": 3095, + "witness": { + "optimistic_coefficient": "0", + "required_coefficient": "-1/2", + "source": 4, + "target": 0 + } +} diff --git a/research/p104-endpoint-completion-flow/SOURCES.json b/research/p104-endpoint-completion-flow/SOURCES.json new file mode 100644 index 0000000000..7c6f2da6c2 --- /dev/null +++ b/research/p104-endpoint-completion-flow/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "4450dbbd1d01929022259f523234590f4cce65b9", + "sha256": "ca056a6def333df7afd822c1f34adc2eaa9089b241fc2bdd5803b64066fc9355" + }, + { + "path": "research/p104-joint-unit-flags/CERTIFICATE.json", + "usage": "input", + "git_blob": "0fa7d2d40566e92f3ea1539723abf438ba65adb8", + "sha256": "a98126428a8da6eae91c50afcc42e014a284c82b554ef77e5b3a34fc6d228128" + }, + { + "path": "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "usage": "input", + "git_blob": "86beaf424e9f0f800ae3a62797d94ec9386b7706", + "sha256": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e" + }, + { + "path": "research/p104-native-channel/inputs/P104-FIXTURE.json", + "usage": "input", + "git_blob": "2e16f99b295bb386fd13bd8fbd57b42ef54143a9", + "sha256": "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4" + } + ] +} diff --git a/research/p104-endpoint-completion-flow/TASK.json b/research/p104-endpoint-completion-flow/TASK.json new file mode 100644 index 0000000000..26ff3c000c --- /dev/null +++ b/research/p104-endpoint-completion-flow/TASK.json @@ -0,0 +1,128 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 6, + "base_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11", + "original_card": { + "id": "p104-side-correction", + "question": "Can the proposed P104 joint endpoint flags be realized by a chronological correction program with coefficients, dirty restoration and an affordable complete bill?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/p104-native-channel/README.md", + "research/p104-native-channel/PROOF.md", + "docs/research/community-efficient1000-review.md", + "research/p104-joint-unit-flags/README.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. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the revision-6 family record and #2981 static joint flags, alongside the reviewed #1991 channel. #2981 is an author-checked source archive, not an independently validated executable correction or a refutation of program-level lifetime floors.", + "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": "After checking live handoffs, pin one named collection from #2981 and attach acquisition/delivery times, source dependencies and coefficient requirements. Test legal access and arbitrary dirty restoration; price any completion against the full channel/endpoint/hosting allowance. Stop with the exact missing implication or a scoped counterexample rather than expanding the static cover census.", + "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.", + "Repeating a correction or physical conversion already supplied by a pending follow-up without adding independent coverage or a different unresolved obligation.", + "Repeating the 208-flag static matching or calling a static nested cover a chronological correction program. Independent audit of that certificate is distinct and remains useful." + ], + "overlap_terms": [ + "P104", + "I-G/2", + "side correction", + "native channel", + "1972", + "1991", + "2586", + "endpoint transport", + "physical dual", + "relay composition", + "2981", + "joint unit flags", + "acquisition delivery", + "static nesting" + ] + }, + "scope_status": "refined", + "actual_scope": "All intermediate full-flag completions of the 208 fixed matched departure and arrival planes in PR2981; test an optimistic common-frame dependency graph on frozen X/Y data paths.", + "scope_change_reason": "The live exact-basis audit at Discussion 2245 comment 18977808 covers the published full bases. This contribution tests whether changing intermediate bases can repair dependency access while retaining the matched endpoint planes.", + "bottleneck_link": "Static endpoint coverage is not source acquisition. A missing dependency in a sound relaxation rejects this named endpoint pairing before spending resources on scalar/native synthesis.", + "budget_minutes": 60, + "stop_rule": "Finish one sound necessary-condition audit and controls. Do not search other matchings, expand construction, or treat passing paths as a supplier.", + "outcome": "negative-result", + "evidence": "Both source-bound implementations agree on every receipt field: 3,095 of 4,992 required coefficients are unreachable. Registered CPython 3.12 replay and six behavioral groups pass, including the actual CLIs, every tiny F2^3 subspace interval, upward relay/direct access, backward-flow rejection, basis changes and source/receipt/schema controls. Optimized CPython 3.14 checks, Ruff and warning-as-error source compilation pass.", + "author": "Nick Petalas", + "ai_assistance": "Substantial automated assistance in analysis, code, verification and writing. No independent human review is claimed.", + "open_questions": [ + { + "question": "Does a different compatible endpoint matching pass the optimistic common-frame dependency test?", + "why_it_matters": "The prescribed covers and one static matching do not ensure source acquisition; this obstruction fixes the published pairing.", + "first_step": "Pin one alternative compatible matching and run the same sound relaxation before attempting a chronological scalar program.", + "blocked_by": "No alternative matching is checked here. A passing dependency test still leaves jointly consistent flags, chronology, exact coefficients, dirty restoration and the full physical bill." + } + ], + "canonical_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2245#discussioncomment-18977898", + "selection_nonce": "82cdf8d6a7ffb6ee868db1b93c85b5b7", + "predecessors": { + "2981": "3d24b92d8ba057b57cb2d480170ec407520e6882", + "2920": "b9ea9def949f9d71d59e21294d0e6cfbe0692a73" + }, + "overlap": { + "checked_utc": "2026-10-16T16:32:26Z", + "open_prs": 234, + "closed_prs": 2440, + "discussion_records": 1702, + "complete_pagination": true, + "concurrent_scope": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2245#discussioncomment-18977808", + "limits": "Metadata and local README/TASK/ledger search; arbitrary diffs and unpublished work excluded." + }, + "verification": { + "registered_command": "uv run --python 3.12 --no-project python scripts/research_package.py --package research/p104-endpoint-completion-flow", + "direct_optimized_command": "python3.14 -I -O -Werror -B research/p104-endpoint-completion-flow/test_verify.py", + "lint": "uvx ruff check research/p104-endpoint-completion-flow", + "format": "uvx ruff format --check research/p104-endpoint-completion-flow", + "scope_limits": "No native/full-channel replay, arbitrary matching exclusion, rounded producer, physical invoice, all-size admission, formal-kernel proof or selected cold replay.", + "environment": "macOS 27.0.1 arm64; CPython 3.12.15 with Clang 23.1.3 and CPython 3.14.8; standard library only." + }, + "family_decision": "Finish this bounded fixed-pair calibration and stop; no matching search or construction expansion.", + "freshness": { + "upstream_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11", + "priority_revision": 6, + "checked_utc": "2026-10-16T16:39:27.748733+00:00", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "overlap_coverage": { + "open_prs": { + "fetched_at": "2026-10-16T16:38:05.870371+00:00", + "complete_pagination": true, + "records": 238 + }, + "discussions": { + "fetched_at": "2026-10-16T16:38:35.971529+00:00", + "complete_pagination": true, + "records": 1704 + }, + "closed_prs": { + "fetched_at": "2026-10-16T16:39:00.051021+00:00", + "complete_pagination": true, + "records": 2440 + } + }, + "overlap_warnings": [], + "decision": "Canonical main unchanged. Exact-basis audit remains complementary; no all-intermediate-completion successor found in metadata search." + }, + "internal_review": "A separately implemented literal-enumeration checker and a fresh read-only code/scope review found no substantive defect. The fresh reviewer reran six controls under CPython 3.12 and lint/format checks. No independent human or formal-kernel review." +} diff --git a/research/p104-endpoint-completion-flow/VERIFY.json b/research/p104-endpoint-completion-flow/VERIFY.json new file mode 100644 index 0000000000..da15e9529b --- /dev/null +++ b/research/p104-endpoint-completion-flow/VERIFY.json @@ -0,0 +1,49 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-joint-unit-flags/CERTIFICATE.json", + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "research/p104-native-channel/inputs/P104-FIXTURE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Source-authenticated all-completion interval contact graph and exact full receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 180, + "checks": "Literal quotient-subspace enumeration and independently traced source dependencies." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 180, + "checks": "Six behavioral control groups, exhaustive tiny subspace contacts and actual CLI/source/receipt controls." + } + ] +} diff --git a/research/p104-endpoint-completion-flow/decisions.tsv b/research/p104-endpoint-completion-flow/decisions.tsv new file mode 100644 index 0000000000..6418cac3d3 --- /dev/null +++ b/research/p104-endpoint-completion-flow/decisions.tsv @@ -0,0 +1,8 @@ +timestamp phase decision reason evidence result +2026-10-16T16:33:48.638626+00:00 scope Audit all intermediate completions of the fixed matching Exact published bases already have an active independent audit Discussion 2245 comment 18977808 Complementary scope; no reroll +2026-10-16T16:33:48.638733+00:00 predicate Reject one required dependency in a sound optimistic relaxation Any actual chronological word maps into the relaxation Fixed endpoint planes and original X/Y paths Verify contact feasibility and reachability independently +2026-10-16T16:33:48.638735+00:00 wake Run bounded commands and inspect completion One finite 208-helper experiment; no background loop 120-second package commands No recurring work +2026-10-16T16:33:48.638736+00:00 probe Permit independently chosen intermediate contact frames This overapproximates every intermediate-basis completion Dimension-layer prototype 3755 total source/target pairs reachable; proof-relevant count pending +2026-10-16T16:38:55.650567+00:00 verification Retain all-completion obstruction Primary formula and independent literal enumeration agree Registered Python3.12 replay and six controls; optimized3.14 checks 3095 missing of4992; X4 to Y0 requires -1/2 but is unreachable +2026-10-16T16:39:27.749223+00:00 submission-checkpoint Continue to focused publication Upstream and priority6 unchanged; complementary audit still distinct 238 openPRs;2440 closedPRs;1704 discussion records; complete pagination No input rebase or new scientific baseline required +2026-10-16T16:39:47.971390+00:00 internal-review Keep bounded result Fresh read-only review found no substantive defects Reviewer replayed six CPython 3.12 controls and source/graph checks No claims beyond fixed matching; ready for exact diff review diff --git a/research/p104-endpoint-completion-flow/independent.py b/research/p104-endpoint-completion-flow/independent.py new file mode 100644 index 0000000000..bc342fc95b --- /dev/null +++ b/research/p104-endpoint-completion-flow/independent.py @@ -0,0 +1,377 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Enumerate all allowed frames and independently trace source dependencies.""" + +import hashlib +import json +import sys +from fractions import Fraction +from itertools import combinations, product +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +INPUTS = ( + "research/p104-joint-unit-flags/CERTIFICATE.json", + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "research/p104-native-channel/inputs/P104-FIXTURE.json", +) +PROVENANCE = { + "certificates/selected-result.json", + "docs/research/agent-task-catalog.json", +} +LIMIT = 2_000_000 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def unique(pairs): + result = dict(pairs) + require(len(result) == len(pairs), "duplicate JSON key") + return result + + +def read_bytes(path): + require(path.stat().st_size <= LIMIT, "input size bound") + with path.open("rb") as stream: + raw = stream.read(LIMIT + 1) + require(len(raw) <= LIMIT, "read size bound") + return raw + + +def read_json(path): + return json.loads(read_bytes(path), object_pairs_hook=unique) + + +def authenticated_inputs(): + records = read_json(PACKAGE / "SOURCES.json")["files"] + require(type(records) is list and len(records) == 5, "five source records") + pins = {} + for record in records: + name, usage = record["path"], record["usage"] + require(name not in pins, "unique source records") + require( + (name in INPUTS and usage == "input") + or (name in PROVENANCE and usage == "provenance"), + "fixed source inventory", + ) + pins[name] = record["sha256"] + require(set(pins) == set(INPUTS) | PROVENANCE, "complete source inventory") + result = [] + for name in INPUTS: + raw = read_bytes(ROOT / name) + require(hashlib.sha256(raw).hexdigest() == pins[name], "input SHA256") + result.append(json.loads(raw, object_pairs_hook=unique)) + return result + + +def space(basis): + """Represent the literal members of a binary subspace by a 512-bit integer.""" + require(type(basis) is list and len(basis) <= 9, "basis size") + points = [0] + for vector in basis: + require(type(vector) is int and 0 < vector < 512, "binary vector") + require(vector not in points, "independent basis") + points += [point ^ vector for point in points] + require(len(points) == 1 << len(basis), "span size") + return sum(1 << point for point in points) + + +def dimension(frame): + count = frame.bit_count() + require(count > 0 and count & (count - 1) == 0, "frame cardinality") + return count.bit_length() - 1 + + +def original_paths(word): + names = [f"{kind}{index}" for kind in "XY" for index in range(104)] + paths = {name: [space(word["initial_frames"][name])] for name in names} + require(type(word["program"]) is list and len(word["program"]) == 4058, "word size") + for event in word["program"]: + op, name = event[:2] + if op in {"add", "copy", "zero", "erase"}: + require(not name.startswith("X"), "immutable original X") + if op in {"add", "copy"}: + require(not event[2].startswith("Y"), "unread original Y") + continue + require(op == "transport", "original opcode") + if name not in paths: + continue + old, new = space(event[2]), space(event[3]) + require( + paths[name][-1] == old and old & new == old and old != new, "nested path" + ) + rank = event[4] + require(type(rank) is int and rank == dimension(new) - dimension(old), "rank") + paths[name].append(new) + for name in names: + path = paths[name] + require( + len(path) <= 10 and path[-1] == space(word["final_frames"][name]), + "data exit", + ) + endpoints = (1, 9) if name.startswith("X") else (0, 8) + require( + (dimension(path[0]), dimension(path[-1])) == endpoints, "data endpoints" + ) + require(len({paths[f"X{s}"][0] for s in range(104)}) == 104, "distinct X lines") + require(len({paths[f"Y{t}"][-1] for t in range(104)}) == 104, "distinct Y caps") + return paths + + +def quotient_bases(): + """All reduced row echelon subspaces of the five-dimensional quotient.""" + result = [[] for _ in range(6)] + for size in range(6): + for pivots in combinations(range(5), size): + free = [ + (i, j) + for i, pivot in enumerate(pivots) + for j in range(pivot + 1, 5) + if j not in pivots + ] + require(len(free) <= 6, "RREF free-entry bound") + for bits in range(1 << len(free)): + rows = [1 << pivot for pivot in pivots] + for index, (i, j) in enumerate(free): + if bits >> index & 1: + rows[i] |= 1 << j + result[size].append(rows) + require( + len({space(rows) for rows in result[size]}) == len(result[size]), + "unique quotient spaces", + ) + require( + [len(rows) for rows in result] == [1, 31, 155, 155, 31, 1], "quotient counts" + ) + return result + + +def frame_choices(basis, quotients): + space(basis) + require(len(basis) == 9, "complete flag") + result = {1: {space(basis[:1])}, 8: {space(basis[:8])}} + for d in range(2, 8): + choices = set() + for rows in quotients[d - 2]: + lifted = [] + for row in rows: + vector = 0 + for j in range(5): + if row >> j & 1: + vector ^= basis[2 + j] + lifted.append(vector) + choices.add(space(basis[:2] + lifted)) + require(len(choices) == len(quotients[d - 2]), "lifted quotient bijection") + result[d] = choices + return result + + +def helper_choices(certificate, paths, quotients): + rows = certificate["helpers"] + require(type(rows) is list and len(rows) == 208, "208 helpers") + choices, departures, arrivals = [], set(), set() + for row in rows: + s, a, t, b = [ + row[key] + for key in ("source", "departure_choice", "target", "arrival_choice") + ] + require(all(type(v) is int for v in (s, a, t, b)), "integer slots") + require( + 0 <= s < 104 and 0 <= t < 104 and a in (0, 1) and b in (0, 1), "slot domain" + ) + require((s, a) not in departures and (t, b) not in arrivals, "distinct slots") + departures.add((s, a)) + arrivals.add((t, b)) + frames = frame_choices(row["basis"], quotients) + require(frames[1] == {paths[f"X{s}"][0]}, "prescribed source line") + require(frames[8] == {paths[f"Y{t}"][-1]}, "prescribed target cap") + choices.append(frames) + return choices + + +def literal_graph(choices): + """Contacts are exact common membership masks, without an interval formula.""" + hosts, layers = {}, [] + for d in range(1, 9): + index = {} + for helper in range(208): + for frame in choices[helper][d]: + index.setdefault(frame, []).append(helper) + adjacency = [set() for _ in range(208)] + for helpers in index.values(): + require(len(helpers) <= 208, "frame hosts bound") + for left, right in combinations(helpers, 2): + adjacency[left].add(right) + adjacency[right].add(left) + hosts[d] = index + layers.append(adjacency) + graph = [set() for _ in range(8 * 208)] + for d, layer in enumerate(layers): + for helper, adjacent in enumerate(layer): + node = d * 208 + helper + graph[node] = {d * 208 + other for other in adjacent} + if d < 7: + graph[node].add(node + 208) + return hosts, layers, graph + + +def reachable(graph, starts): + size = len(graph) + require(0 < size <= 1664 and len(starts) <= size, "traversal bound") + seen = set(starts) + require(all(type(node) is int and 0 <= node < size for node in seen), "start nodes") + queue = sorted(seen) + for cursor in range(size): + if cursor == len(queue): + break + for node in graph[queue[cursor]]: + require(0 <= node < size, "graph endpoint") + if node not in seen: + seen.add(node) + queue.append(node) + require(len(seen) == len(queue) <= size, "traversal capacity") + return seen + + +def components(layer): + seen, count = set(), 0 + for helper in range(208): + if helper not in seen: + seen |= reachable(layer, {helper}) + count += 1 + require(len(seen) == 208, "complete layer components") + return count + + +def endpoint_nodes(paths, hosts, kind): + result = [] + for index in range(104): + nodes = set() + for frame in paths[f"{kind}{index}"]: + d = dimension(frame) + if 1 <= d <= 8: + nodes.update( + (d - 1) * 208 + helper for helper in hosts[d].get(frame, []) + ) + result.append(nodes) + return result + + +def trace_sources(paths, hosts, layers, graph): + reads = endpoint_nodes(paths, hosts, "X") + writes = endpoint_nodes(paths, hosts, "Y") + masks, support = [0] * 104, [0] * 1664 + for s in range(104): + reached = reachable(graph, reads[s]) + for node in reached: + support[node] |= 1 << s + for t in range(104): + direct = set(paths[f"X{s}"]) & set(paths[f"Y{t}"]) + if reached & writes[t] or direct: + masks[t] |= 1 << s + summary = [] + for offset, layer in enumerate(layers): + summary.append( + { + "dimension": offset + 1, + "contacts": sum(len(adjacent) for adjacent in layer) // 2, + "components": components(layer), + "max_sources": max( + support[offset * 208 + h].bit_count() for h in range(208) + ), + } + ) + return masks, summary + + +def required_correction(fixture): + roots = set() + for i, j in combinations(range(8), 2): + for sign in (-1, 1): + root = [0] * 8 + root[i], root[j] = 2, 2 * sign + roots.add(tuple(root)) + for signs in product((-1, 1), repeat=7): + if signs.count(-1) % 2 == 0: + roots.add((1, *signs)) + excluded = fixture["section4_explicit_P104"] + ports = sorted(roots - {tuple(root) for root in excluded["F0"] + excluded["C"]}) + require(len(roots) == 120 and len(ports) == 104, "ordered roots") + result = [] + for t in range(104): + for s in range(104): + gram = sum(ports[t][i] * ports[s][i] for i in range(8)) + coefficient = Fraction(8 * int(t == s) - gram, 8) + if coefficient: + result.append((t, s, coefficient)) + require(len(result) == 4992, "correction support count") + return result + + +def enumeration_control(quotients): + first = frame_choices([1, 2, 4, 8, 16, 32, 64, 128, 256], quotients) + second = frame_choices([4, 8, 1, 2, 16, 32, 64, 128, 256], quotients) + require(not first[3] & second[3], "disjoint planes cannot meet at dimension three") + require( + space([1, 2, 4, 8]) in first[4] & second[4], "literal dimension-four contact" + ) + + +def compute(certificate, word, fixture): + paths = original_paths(word) + quotients = quotient_bases() + enumeration_control(quotients) + choices = helper_choices(certificate, paths, quotients) + hosts, layers, graph = literal_graph(choices) + masks, summary = trace_sources(paths, hosts, layers, graph) + required = required_correction(fixture) + missing = [(t, s, value) for t, s, value in required if not masks[t] >> s & 1] + require(bool(missing), "nonempty missing dependency witness") + t, s, coefficient = missing[0] + return { + "schema_version": 1, + "helpers": 208, + "required_pairs": len(required), + "reachable_required_pairs": len(required) - len(missing), + "unreachable_required_pairs": len(missing), + "layers": summary, + "target_source_masks_hex": [hex(mask) for mask in masks], + "witness": { + "source": s, + "target": t, + "required_coefficient": str(coefficient), + "optimistic_coefficient": "0", + }, + "scope": "All intermediate completions of fixed matched endpoint planes; optimistic untimed contacts, no restoration charge; no new kappa.", + } + + +def main(): + require(sys.argv[1:] in ([], ["--emit"]), "usage: independent.py [--emit]") + result = compute(*authenticated_inputs()) + if sys.argv[1:]: + print(json.dumps(result, indent=2, sort_keys=True)) + return + expected = read_json(PACKAGE / "RESULT.json") + require( + json.dumps(result, sort_keys=True) == json.dumps(expected, sort_keys=True), + "all receipt fields", + ) + print( + "PASS_P104_ENDPOINT_COMPLETION_FLOW_INDEPENDENT", + f"required={result['required_pairs']}", + f"unreachable={result['unreachable_required_pairs']}", + "enumerated_quotient_subspaces", + ) + + +if __name__ == "__main__": + try: + main() + except (OSError, ValueError, KeyError, TypeError) as error: + raise SystemExit( + f"FAIL_P104_ENDPOINT_COMPLETION_FLOW_INDEPENDENT: {error}" + ) from error diff --git a/research/p104-endpoint-completion-flow/test_verify.py b/research/p104-endpoint-completion-flow/test_verify.py new file mode 100644 index 0000000000..6b625fdc82 --- /dev/null +++ b/research/p104-endpoint-completion-flow/test_verify.py @@ -0,0 +1,164 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Behavioral controls for the necessary dependency test.""" + +import copy +import importlib.util +import json +import shutil +import subprocess +import sys +import tempfile +import unittest +from itertools import combinations +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("completion_flow", PACKAGE / "verify.py") +flow = importlib.util.module_from_spec(spec) +spec.loader.exec_module(flow) + + +def tiny_spaces(): + spaces = {frozenset({0})} + for size in range(1, 4): + for basis in combinations(range(1, 8), size): + points = {0} + for vector in basis: + points |= {p ^ vector for p in tuple(points)} + spaces.add(frozenset(points)) + return sorted(spaces, key=lambda space: (len(space), sorted(space))) + + +def command(package, script="verify.py", *args): + return subprocess.run( + [sys.executable, "-I", "-O", "-Werror", "-B", str(package / script), *args], + capture_output=True, + text=True, + timeout=60, + check=False, + ) + + +def export(root): + package = root / "research/p104-endpoint-completion-flow" + shutil.copytree(PACKAGE, package, ignore=shutil.ignore_patterns("__pycache__")) + for name in flow.INPUTS: + destination = root / name + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(flow.ROOT / name, destination) + return package + + +class FlowTests(unittest.TestCase): + def test_contact_against_all_small_subspaces(self): + spaces = tiny_spaces() + self.assertEqual(len(spaces), 16) + intervals = [(a, b) for a in spaces for b in spaces if a <= b] + checked = 0 + for left in intervals: + for right in intervals: + for d in range(4): + expected = any( + len(v) == 1 << d + and left[0] <= v <= left[1] + and right[0] <= v <= right[1] + for v in spaces + ) + self.assertEqual(flow.contact(left, right, d), expected) + checked += 1 + self.assertGreater(checked, 10_000) + + def test_relay_and_direct_source_access(self): + bases = ([1, 2, 4, 8, 16, 32, 64, 128, 256], [2, 1, 4, 8, 16, 32, 128, 64, 256]) + planes = [{d: flow.span(basis[:d]) for d in flow.FIXED} for basis in bases] + paths = {f"X{s}": [flow.span([256])] for s in range(104)} + paths.update({f"Y{t}": [flow.span([])] for t in range(104)}) + paths["X0"] = [flow.span([1])] + paths["Y0"] = [planes[1][7]] + outputs, _ = flow.dependency_graph(planes, paths) + self.assertEqual(outputs[0], 1) + # A source at a later layer cannot flow backwards to a target line. + paths["X0"], paths["Y0"] = [planes[0][8]], [flow.span([1])] + outputs, _ = flow.dependency_graph(planes, paths) + self.assertEqual(outputs[0], 0) + # Include direct X-to-Y contacts, even without a usable helper contact. + paths["X0"] = paths["Y0"] = [flow.span([256])] + outputs, _ = flow.dependency_graph(planes, paths) + self.assertEqual(outputs[0], (1 << 104) - 1) + + def test_real_inputs_and_changed_intermediate_basis(self): + certificate, word, fixture = flow.inputs() + result = flow.compute(certificate, word, fixture) + self.assertEqual(result["unreachable_required_pairs"], 3095) + self.assertEqual( + result["witness"], + { + "source": 4, + "target": 0, + "required_coefficient": "-1/2", + "optimistic_coefficient": "0", + }, + ) + changed = copy.deepcopy(certificate) + for row in changed["helpers"]: + row["basis"][2], row["basis"][3] = row["basis"][3], row["basis"][2] + self.assertEqual(flow.compute(changed, word, fixture), result) + changed["helpers"][0]["basis"][0] = True + with self.assertRaisesRegex(ValueError, "vector domain"): + flow.compute(changed, word, fixture) + + def test_both_actual_clis_and_emitted_receipt(self): + for script, marker in ( + ("verify.py", "PASS_P104_ENDPOINT_COMPLETION_FLOW"), + ("independent.py", "PASS_P104_ENDPOINT_COMPLETION_FLOW_INDEPENDENT"), + ): + completed = command(PACKAGE, script) + self.assertEqual(completed.returncode, 0, completed.stderr) + self.assertIn(marker, completed.stdout) + emitted = command(PACKAGE, "verify.py", "--emit") + self.assertEqual(emitted.returncode, 0, emitted.stderr) + self.assertEqual( + json.loads(emitted.stdout), flow.read_json(PACKAGE / "RESULT.json") + ) + + def test_git_free_export_receipt_and_source_controls(self): + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + package = export(root) + for script in ("verify.py", "independent.py"): + self.assertEqual(command(package, script).returncode, 0) + receipt = package / "RESULT.json" + original = receipt.read_bytes() + changed = json.loads(original) + changed["target_source_masks_hex"][0] = "0x0" + receipt.write_text(json.dumps(changed)) + for script in ("verify.py", "independent.py"): + self.assertNotEqual(command(package, script).returncode, 0) + receipt.write_bytes(original) + source = root / flow.INPUTS[0] + source.write_bytes(source.read_bytes() + b"\n") + for script in ("verify.py", "independent.py"): + failure = command(package, script) + self.assertNotEqual(failure.returncode, 0) + self.assertIn("SHA256", failure.stderr) + + def test_duplicate_keys_and_typed_receipt_reject(self): + with tempfile.TemporaryDirectory() as directory: + package = export(Path(directory)) + receipt = package / "RESULT.json" + original = receipt.read_text() + changed = json.loads(original) + changed["schema_version"] = True + receipt.write_text(json.dumps(changed)) + self.assertNotEqual(command(package).returncode, 0) + receipt.write_text( + original.replace('"helpers": 208,', '"helpers": 208, "helpers": 208,') + ) + self.assertNotEqual(command(package).returncode, 0) + invalid = command(PACKAGE, "verify.py", "--unknown") + self.assertNotEqual(invalid.returncode, 0) + self.assertIn("usage:", invalid.stderr) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/p104-endpoint-completion-flow/verify.py b/research/p104-endpoint-completion-flow/verify.py new file mode 100644 index 0000000000..0e49aa424f --- /dev/null +++ b/research/p104-endpoint-completion-flow/verify.py @@ -0,0 +1,276 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Necessary dependency test for every completion of fixed P104 endpoint pairs.""" + +import hashlib +import json +import sys +from fractions import Fraction +from itertools import combinations, product +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +INPUTS = ( + "research/p104-joint-unit-flags/CERTIFICATE.json", + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "research/p104-native-channel/inputs/P104-FIXTURE.json", +) +FIXED = (0, 1, 2, 7, 8, 9) + + +def require(condition, reason): + if not condition: + raise ValueError(reason) + + +def unique(pairs): + result = dict(pairs) + require(len(result) == len(pairs), "duplicate JSON key") + return result + + +def read_json(path): + require(path.stat().st_size <= 2_000_000, "JSON size bound") + return json.loads(path.read_bytes(), object_pairs_hook=unique) + + +def inputs(): + records = read_json(PACKAGE / "SOURCES.json")["files"] + require(len(records) == 5, "source inventory size") + pins = {r["path"]: r["sha256"] for r in records if r["usage"] == "input"} + require(set(pins) == set(INPUTS), "exact input inventory") + values = [] + for name in INPUTS: + path = ROOT / name + require(path.stat().st_size <= 2_000_000, "input size bound") + raw = path.read_bytes() + require(hashlib.sha256(raw).hexdigest() == pins[name], "input SHA256") + values.append(json.loads(raw, object_pairs_hook=unique)) + return values + + +def span(basis): + require(type(basis) is list and len(basis) <= 9, "basis shape") + result = frozenset({0}) + for vector in basis: + require(type(vector) is int and 0 < vector < 512, "vector domain") + require(vector not in result, "independent basis") + result |= frozenset(v ^ vector for v in result) + require(len(result) == 1 << len(basis), "span cardinality") + return result + + +def dimension(space): + size = len(space) + require(size > 0 and size & (size - 1) == 0, "subspace cardinality") + return size.bit_length() - 1 + + +def data_paths(word): + names = [f"{kind}{i}" for kind in "XY" for i in range(104)] + paths = {name: [span(word["initial_frames"][name])] for name in names} + require(len(word["program"]) == 4058, "4058 original events") + for event in word["program"]: + if event[0] != "transport" or event[1] not in paths: + continue + _, name, before, after, rank = event + old, new = span(before), span(after) + require(paths[name][-1] == old and old < new, "increasing data path") + require(type(rank) is int and rank == dimension(new) - dimension(old), "rank") + paths[name].append(new) + for name, chain in paths.items(): + require(len(chain) <= 10, "data path size") + require(chain[-1] == span(word["final_frames"][name]), "data exit") + expected = (1, 9) if name[0] == "X" else (0, 8) + require((dimension(chain[0]), dimension(chain[-1])) == expected, "endpoints") + return paths + + +def endpoint_planes(certificate, paths): + helpers = certificate["helpers"] + require(type(helpers) is list and len(helpers) == 208, "208 helpers") + planes, departures, arrivals = [], set(), set() + for row in helpers: + s, t, a, b = [ + row[k] for k in ("source", "target", "departure_choice", "arrival_choice") + ] + require(all(type(v) is int for v in (s, t, a, b)), "integer slots") + require(0 <= s < 104 and 0 <= t < 104 and a in (0, 1) and b in (0, 1), "slots") + require((s, a) not in departures and (t, b) not in arrivals, "unique slots") + departures.add((s, a)) + arrivals.add((t, b)) + basis = row["basis"] + require(type(basis) is list and len(basis) == 9, "full flag basis") + span(basis) + fixed = {d: span(basis[:d]) for d in FIXED} + require(fixed[1] == paths[f"X{s}"][0], "designated source line") + require(fixed[8] == paths[f"Y{t}"][-1], "designated target hyperplane") + planes.append(fixed) + return planes + + +def interval(fixed, d): + if d in fixed: + return fixed[d], fixed[d] + require(3 <= d <= 6, "intermediate dimension") + return fixed[2], fixed[7] + + +def fits(bounds, d, frame): + low, high = bounds + return dimension(frame) == d and low <= frame <= high + + +def contact(left, right, d): + a, b = left + c, e = right + if not (a <= e and c <= b): + return False + minimum = dimension(a) + dimension(c) - dimension(a & c) + maximum = dimension(b & e) + return minimum <= d <= maximum + + +def components(adjacency): + count, seen, result = len(adjacency), set(), [] + require(count <= 208, "helper bound") + for start in range(count): + if start in seen: + continue + queue, seen = [start], seen | {start} + for offset in range(count): + if offset >= len(queue): + break + for nxt in sorted(adjacency[queue[offset]]): + require(0 <= nxt < count, "contact endpoint") + if nxt not in seen: + seen.add(nxt) + queue.append(nxt) + require(len(queue) <= count, "component capacity") + result.append(queue) + require(len(seen) == count, "complete components") + return result + + +def dependency_graph(planes, paths): + count = len(planes) + require(0 < count <= 208, "helper inventory bound") + support, outputs, layers = [0] * count, [0] * 104, [] + xs = [paths[f"X{s}"] for s in range(104)] + ys = [paths[f"Y{t}"] for t in range(104)] + for t, target in enumerate(ys): + outputs[t] = sum( + 1 << s for s, source in enumerate(xs) if set(source) & set(target) + ) + for d in range(1, 9): + bounds = [interval(fixed, d) for fixed in planes] + adjacency = [set() for _ in planes] + for i in range(count): + support[i] |= sum( + 1 << s + for s, chain in enumerate(xs) + if any(fits(bounds[i], d, f) for f in chain) + ) + for j in range(i): + if contact(bounds[i], bounds[j], d): + adjacency[i].add(j) + adjacency[j].add(i) + groups = components(adjacency) + for group in groups: + joined = 0 + for i in group: + joined |= support[i] + for i in group: + support[i] = joined + for t, chain in enumerate(ys): + for i in range(count): + if any(fits(bounds[i], d, frame) for frame in chain): + outputs[t] |= support[i] + layers.append( + { + "dimension": d, + "contacts": sum(map(len, adjacency)) // 2, + "components": len(groups), + "max_sources": max(v.bit_count() for v in support), + } + ) + return outputs, layers + + +def correction(fixture): + roots = [] + for i, j in combinations(range(8), 2): + for sign in (-1, 1): + row = [0] * 8 + row[i], row[j] = 2, 2 * sign + roots.append(tuple(row)) + roots += [(1, *s) for s in product((-1, 1), repeat=7) if s.count(-1) % 2 == 0] + removed = fixture["section4_explicit_P104"] + ports = sorted(set(roots) - {tuple(v) for v in removed["F0"] + removed["C"]}) + require(len(roots) == 120 and len(ports) == 104, "ordered P104 roots") + return [ + [ + Fraction( + 8 * int(t == s) + - sum(a * b for a, b in zip(ports[t], ports[s], strict=True)), + 8, + ) + for s in range(104) + ] + for t in range(104) + ] + + +def compute(certificate, word, fixture): + paths = data_paths(word) + planes = endpoint_planes(certificate, paths) + outputs, layers = dependency_graph(planes, paths) + matrix = correction(fixture) + required = [(t, s) for t in range(104) for s in range(104) if matrix[t][s]] + missing = [(t, s) for t, s in required if not outputs[t] >> s & 1] + require( + len(required) == 4992 and missing, "nonempty required-dependency obstruction" + ) + t, s = missing[0] + return { + "schema_version": 1, + "helpers": len(planes), + "required_pairs": len(required), + "reachable_required_pairs": len(required) - len(missing), + "unreachable_required_pairs": len(missing), + "layers": layers, + "target_source_masks_hex": [hex(mask) for mask in outputs], + "witness": { + "source": s, + "target": t, + "required_coefficient": str(matrix[t][s]), + "optimistic_coefficient": "0", + }, + "scope": "All intermediate completions of fixed matched endpoint planes; optimistic untimed contacts, no restoration charge; no new kappa.", + } + + +def main(): + require(sys.argv[1:] in ([], ["--emit"]), "usage: verify.py [--emit]") + result = compute(*inputs()) + if sys.argv[1:]: + print(json.dumps(result, indent=2, sort_keys=True)) + return + expected = read_json(PACKAGE / "RESULT.json") + require( + json.dumps(result, sort_keys=True) == json.dumps(expected, sort_keys=True), + "exact receipt", + ) + print( + "PASS_P104_ENDPOINT_COMPLETION_FLOW", + f"required={result['required_pairs']}", + f"unreachable={result['unreachable_required_pairs']}", + "all_intermediate_completions no_new_kappa", + ) + + +if __name__ == "__main__": + try: + main() + except (OSError, ValueError, KeyError, TypeError) as error: + raise SystemExit(f"FAIL_P104_ENDPOINT_COMPLETION_FLOW: {error}") from error