diff --git a/research/p104-root2-receiver-obstruction/PROOF.md b/research/p104-root2-receiver-obstruction/PROOF.md new file mode 100644 index 0000000000..fba8116104 --- /dev/null +++ b/research/p104-root2-receiver-obstruction/PROOF.md @@ -0,0 +1,124 @@ +# A receiver-only obstruction to the direct frame-520 deletion + +This contribution was produced by Nick Petalas. The input word and root-relay +construction are DreamingOfClouds's PR #6144, at +`4f3b67e7c37ae270da9584033132866d0cf63e42`, with Ali Romman and the retained +P104 lineage. The new result is the separating input for the attempted edit +below, together with its receiver-only impossibility consequence. + +## Exact model and attempted edit + +Use the retained symbolic scalar convention. Every public input has an +independent coordinate `x_r`. An ADD replaces a row by a linear combination +of rows at the same chart. A MOVE transports its represented row and changes +the chart. INIT and CLEAR concern owned fields. These are the algebraic +conventions of the predecessor's finite word; no new physical primitive is +introduced here. + +All event ordinals in this paragraph are zero-based in the pinned PR6144 word. +The function `proposed` in `verify.py` defines the entire attempted edit: + +1. Remove events 12888, 12932, 12933 and 12934, which move helper 497 through + 519/520 and give it the register-48 and register-228 reads. +2. Before event 12918, move 497 directly from 3 to 737 and add register 228 + there with coefficient 1. Register 228 is still at 737. +3. Remove events 13484, 13485 and 13486. Before event 13487, move owned 772 + directly from 529 to 737 and add it to 497 with coefficient -4. +4. Replace event 15459 by the move of 497 from 737 to 914. + +All other events, boundary charts and fields are unchanged. The edited word +has 22,815 events. Its moves and scalar meetings through the cut considered +below are legal. Its operator is incorrect; it is not offered as a supplier. + +The old register-48 read is the linear form + +`V = x_48 + x_32 + x_98 + x_85`. + +Before original event 15647, `ADD 145,161,-1/2,914`, the edited and original +rows differ only in fields 497 and 161. Their differences are respectively +`-V` and `V/2`. This comparison is over all 799 symbolic input coordinates, +including the formal owned entries before initialization. It checks the +effect of the new edit, not the correctness of the predecessor's theorem. + +## Allowed repairs and theorem + +Freeze the edited prefix through original event 12934 and the chart trajectory +of every field. Freeze every nonreceiver scalar event. Between the cut after +that prefix and the cut immediately before original event 15647, allow any +finite homogeneous linear operations on receiver 161, using any fields +currently at its exact chart. Coefficients may be arbitrary constants; +repeated reads, replacements of its existing scalar operations and SCALEs +are allowed. No workspace, source mutation or changed receiver MOVE is allowed. + +**Theorem.** No such repair gives receiver 161 its original PR6144 row at the +specified consumer cut, for all inputs. + +Take the separating input + +`x_32 = 1, x_5 = -1, x_r = 0 for r not in {32,5}`. + +The exact finite certificate in `RESULT.json` establishes the following facts: + +- The edited receiver is zero at the start of the repair window. +- At every cut in the window, every other field at receiver 161's chart is + zero on this input. +- There is no ADD or COPY reading 161 into another field in the window. +- The original required receiver value at the consumer cut is `-1/2`. + +There are 2,712 cuts, including the entry and consumer cuts. The verifier +checks 241,377 coframed donor occurrences. It inspects every cut, including +ones without an existing receiver operation. Between consecutive cuts no +frozen event changes a donor's value or chart, so extra receiver operations +at arbitrary times have the same donor menu as a checked cut. + +Because the frozen program never reads the receiver into another field in +the window, changing receiver operations cannot change the donor values. +Induct on the frozen events and any interleaved repair operations. The +receiver starts at zero. A homogeneous linear operation on zero arguments +leaves it zero, and moving a zero row leaves zero. Thus it is still zero at +the consumer cut. It cannot equal the required `-1/2`. This proves the theorem. + +Equivalently, the coefficient functional `row[32] - row[5]` annihilates the +receiver's initial row and every available donor row, but evaluates to `-1/2` +on the desired row. This is an exact linear separation certificate, not a +failed coefficient search. + +## Consequence and boundaries + +The direct rerouting cannot be completed by adding or resynthesizing scalar +compensation only on receiver 161 in this window. A successful construction +must change an additional source, trajectory, earlier prefix or consumer +contract. In particular, crediting the saved moves without delivering `V/2` +to the consumer is invalid. + +This does not exclude removing frame 520 by another construction, repairing +outside this window, or accepting and compensating a different value at the +145/161 consumer. It does not address removing frame 737. No complete paid +invoice, new kappa, native implementation, full predecessor replay, supplier +admission, proof-kernel acceptance or complete multiplication theorem is +claimed. The five selected framework assumptions remain. + +## Verification design and bounded code + +The checker authenticates the exact upstream compressed word before decoding +it. One pass evaluates the separating input and checks every common-chart +donor. A separate sparse symbolic interpreter compares all input coefficients +at the consumer cut. Five false-claim controls reject a changed source anchor, +the wrong witness sign, two unavailable reads and a wrong root-read coefficient. +The checks use explicit exceptions and also run with optimization enabled. + +The code has no recursion or asynchronous work. Source dimensions fix 799 +fields, 1,093 charts of dimension at most 9 and 22,818 events; all loops and +collections are bounded by these inventories. The two symbolic states contain +at most 799 squared coefficients each, and no per-cut state is retained. +Each function is shorter than 60 physical lines. + +Power-of-ten rule 3 has a managed-runtime deviation: Python allocates integers, +Fractions, dictionaries and parser objects during replay. The source byte pin +and fixed inventories bound live state; this is a terminating exact checker, +not a steady-state service. Rules 8 and 9 retain the standard JSON decoder +and five finite zero-argument control callbacks. They never evaluate source +code, load plugins or dispatch to external jobs. Follow-up for a constrained +runtime would replace these with fixed arrays and direct control invocations; +the present package does not claim fixed-allocation execution. Warnings-as-errors +and normal/optimized execution supply the available Python diagnostics. diff --git a/research/p104-root2-receiver-obstruction/README.md b/research/p104-root2-receiver-obstruction/README.md new file mode 100644 index 0000000000..f6903dad58 --- /dev/null +++ b/research/p104-root2-receiver-obstruction/README.md @@ -0,0 +1,97 @@ +# A direct root-2 stage deletion needs more than receiver-only compensation + +This contribution was produced by Nick Petalas. It builds on +[DreamingOfClouds's PR #6144](https://github.com/CrocSwap/integer-mult-bounds/pull/6144), +Ali Romman and the retained P104 construction lineage. + +**Scoped proof with an exact finite certificate; no new kappa.** One explicit +attempt to remove owned register 772's frame-520 stage moves helper 497's root +read to frame 737 and removes its earlier register-48 read. The missing form is +`V = x_48 + x_32 + x_98 + x_85`. At the next 145/161 consumer, the resulting +differences are exactly `-V` in 497 and `V/2` in 161; all other rows agree. + +Receiver-only compensation cannot preserve that consumer contract. The input +`x_32=1, x_5=-1`, with all other independent inputs zero, gives zero in receiver +161 and every field it can read throughout the stated repair window. Its +required consumer value is `-1/2`. Arbitrary homogeneous linear compensation +in that window therefore fails, even with unrestricted constant coefficients +and repeated reads. [PROOF.md](PROOF.md) gives the exact edit, window and proof. + +This is a new obstruction to an attempted changed read/trajectory contract. +It does not audit the predecessor or exclude its general open lead. A useful +next construction must change another source, trajectory, earlier prefix or +consumer contract. Frame 737 is unattempted. No new paid invoice, supplier, +native tariff, selected-frontier change or complete multiplication theorem is +claimed. The five inherited framework assumptions remain. + +## Reproduction and evidence + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/p104-root2-receiver-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/p104-root2-receiver-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-root2-receiver-obstruction +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-root2-receiver-obstruction --check-source-history +``` + +Other systems may substitute their CPython 3.12 interpreter. Expected direct +status is `PASS_ROOT2_RECEIVER_OBSTRUCTION`; the registered runner reports +`PASS_REGISTERED_RESEARCH_PACKAGE`. Every registered check is bounded at 120 +seconds. The receipt is generated, binds its verifier and input hashes, and is +compared byte for byte. Regenerate it only to an external path with +`verify.py --output /absolute/scratch/RESULT.json`. + +The verifier checks all 2,712 cuts in the compensation window and 241,377 +coframed donor occurrences. A separate full symbolic interpreter checks the +attempted edit's effect on every one of the 799 input coordinates at the +consumer cut. Five false-claim controls run in normal and optimized mode. +These are finite exact checks supporting the induction proof; they are not +formal proof-kernel or independent human review. No full predecessor, selected +supplier, native, compiler, outer or rounded-multiplier replay is performed. + +The predecessor word is retained byte for byte in `inputs/`. `UPSTREAM.json` +records its author, original head, path, Git blob, size and SHA256. Replay needs +no network or unmerged Git object. Its original compressed bytes were obtained +through GitHub's contents API and checked against the API's Git blob and size. +The task and selected-record provenance are pinned at canonical main +`721c03822c421b7f7fcbb2598993b947c4d88419` in `SOURCES.json`. + +## Related open work + +- PR #6144 poses the root-2 stage-removal lead and supplies the input word; + it supersedes the closed predecessor PR #6143. +- PR #6145 independently descends the 772/731 relay on top of #6143. This + certificate is bound to #6144's different word and claims no transfer to it. +- PR #6136 studies chart-only changes on PR6030. This attempted edit changes + which register 497 reads and where it reads it. +- PR #6084 excludes an endpoint-recoding approach to helper 469. The helper, + read graph and quantified repair class here differ. +- PR #6154 coalesces the 791/770 owned lifetime on PR6144. This certificate + uses the uncoalesced predecessor and concerns the separate 772/497 path. + +The broader P104 scalar and helper-split packages have different contracts. +Their results and credits remain with their authors. The overlap search checks +metadata and scoped main-branch notes; it is not a global novelty certificate. + +## Open next questions + +Can another source or consumer contract remove root 772's frame-520 stage? +A paid complex improvement would matter at the binding supplier. First change +one source trajectory or the 145/161 consumer cut, track both the separating +input and the full missing form, then charge all additional moves and target +changes. No legal all-input construction or favorable complete invoice is +supplied here. The structured question is in `TASK.json`. + +## Credit and license + +The input word, root-relay descent and open lead are by DreamingOfClouds. +PR6030/PR5907 supply the previous rung-removal words; Ali Romman's PR5827 +supplies their checking conventions, following Mason Hale's PR5811 and the +retained lineage through Pierre-Loic Doulcet's PR5565. This package contributes +only the explicit attempted edit, its separating certificate and the scoped +receiver-only theorem. The available-span obstruction method is classical; +Jonathan Capalbo's PR6069 and JoyboyBrian's PR6084 provide related P104 uses. +New material is Apache-2.0. + +Independent human and formal proof-kernel review are unclaimed. diff --git a/research/p104-root2-receiver-obstruction/RESULT.json b/research/p104-root2-receiver-obstruction/RESULT.json new file mode 100644 index 0000000000..18b5a87d0c --- /dev/null +++ b/research/p104-root2-receiver-obstruction/RESULT.json @@ -0,0 +1,39 @@ +{ + "base_window": [ + 12935, + 15647 + ], + "claim_type": "Scoped linear obstruction with an exact finite certificate", + "controls": [ + "changed_source_anchor", + "wrong_witness_sign", + "unavailable_48_read", + "unavailable_497_read", + "wrong_root_read" + ], + "edited_events": 22815, + "edited_window": [ + 12933, + 15644 + ], + "missing_form": { + "32": "1", + "48": "1", + "85": "1", + "98": "1" + }, + "observation": { + "coframed_source_checks": 241377, + "cuts": 2712, + "receiver_value": "0" + }, + "required_receiver_value": "-1/2", + "source_head": "4f3b67e7c37ae270da9584033132866d0cf63e42", + "source_sha256": "c71985d96bf3d4a35aae111aaba87e376f7367efb4a5686278ef293732757533", + "status": "PASS_ROOT2_RECEIVER_OBSTRUCTION", + "verifier_sha256": "9042c7602638a447e5f8a76162c54d7b6a8273859ad33c554ce32c3ff217b371", + "witness": { + "32": "1", + "5": "-1" + } +} diff --git a/research/p104-root2-receiver-obstruction/SOURCES.json b/research/p104-root2-receiver-obstruction/SOURCES.json new file mode 100644 index 0000000000..40f96c767a --- /dev/null +++ b/research/p104-root2-receiver-obstruction/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/p104-root2-receiver-obstruction/TASK.json b/research/p104-root2-receiver-obstruction/TASK.json new file mode 100644 index 0000000000..65c99bae92 --- /dev/null +++ b/research/p104-root2-receiver-obstruction/TASK.json @@ -0,0 +1,121 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "p104-side-correction", + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "existing_checks": [ + { + "scope": "PR #4133: literal-slot defect", + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4136: uniform commutation gap", + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4140: uniform encoding gap", + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4154: fiber-tag seam mismatch", + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove a receiver-only linear obstruction to one explicit root-2 frame-520 deletion on PR6144, with exact dirty-input witnesses.", + "scope_change_reason": "The current bottleneck is paid complex work. This takes PR6144's new root-2 lead and resolves one attempted changed read/itinerary contract, rather than constructing a helper split or reviewing a predecessor.", + "bottleneck_link": "Removing a served root-descent stage could improve the complete complex paid moment. This certificate rules out receiver-only repair of the explicit direct rerouting and identifies the additional source or consumer change it needs.", + "budget_minutes": 60, + "stop_rule": "Stop after the first verified original result or a precise dead end. Do not extend to frame 737.", + "outcome": "negative-result", + "evidence": "PROOF.md; verify.py; generated RESULT.json; exact predecessor bytes in inputs/ and UPSTREAM.json.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a changed source or consumer contract remove root 772's frame-520 stage?", + "why_it_matters": "The direct rerouting cannot be repaired only at receiver 161; a genuine paid-profile gain must bring a nonzero separating signal through another path.", + "first_step": "Change one source trajectory or the 145/161 consumer cut, track x_32-x_5 and the complete missing form, then price all additional calls.", + "blocked_by": "No legal arbitrary-input construction or favorable complete invoice is supplied here." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19246869", + "finding": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19247168" + } +} diff --git a/research/p104-root2-receiver-obstruction/UPSTREAM.json b/research/p104-root2-receiver-obstruction/UPSTREAM.json new file mode 100644 index 0000000000..1d1e006755 --- /dev/null +++ b/research/p104-root2-receiver-obstruction/UPSTREAM.json @@ -0,0 +1,13 @@ +{ + "author": "DreamingOfClouds", + "git_blob": "69b70ee50c697b185ebf585fbe69f2487af32d1d", + "head": "4f3b67e7c37ae270da9584033132866d0cf63e42", + "local_path": "inputs/pr6144-WORD.json.gz", + "path": "research/p104-root-relay-descent-2/WORD.json.gz", + "pr": 6144, + "repository": "DreamingOfClouds/integer-mult-bounds", + "retention": "Exact compressed bytes are retained in this package; the external head is provenance and is not needed in the replay Git history.", + "sha256": "c71985d96bf3d4a35aae111aaba87e376f7367efb4a5686278ef293732757533", + "size": 119901, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6144" +} diff --git a/research/p104-root2-receiver-obstruction/VERIFY.json b/research/p104-root2-receiver-obstruction/VERIFY.json new file mode 100644 index 0000000000..9a4d858eb5 --- /dev/null +++ b/research/p104-root2-receiver-obstruction/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact source binding, full symbolic edit effect, all-cut separating input and rejection controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same mathematical certificate and controls with assertions disabled." + } + ] +} diff --git a/research/p104-root2-receiver-obstruction/inputs/pr6144-WORD.json.gz b/research/p104-root2-receiver-obstruction/inputs/pr6144-WORD.json.gz new file mode 100644 index 0000000000..69b70ee50c Binary files /dev/null and b/research/p104-root2-receiver-obstruction/inputs/pr6144-WORD.json.gz differ diff --git a/research/p104-root2-receiver-obstruction/verify.py b/research/p104-root2-receiver-obstruction/verify.py new file mode 100644 index 0000000000..c4a1f5fde2 --- /dev/null +++ b/research/p104-root2-receiver-obstruction/verify.py @@ -0,0 +1,238 @@ +"""Exact cut obstruction for one proposed P104 descent edit. Apache-2.0. + +Produced by Nick Petalas. Predecessor word: DreamingOfClouds, PR6144; +Ali Romman and the retained P104 lineage. See README.md and PROOF.md. +""" + +import argparse +from copy import deepcopy +from fractions import Fraction +from hashlib import sha1, sha256 +import gzip +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +BEGIN, END = 12935, 15647 +WITNESS = {32: Fraction(1), 5: Fraction(-1)} +ANCHORS = { + 12888: ["MOVE", 497, 3, 519, False], + 12918: ["ADD", 451, 228, "1", 737], + 12932: ["ADD", 497, 48, "1", 519], + 12933: ["MOVE", 497, 519, 520, False], + 12934: ["ADD", 497, 228, "1", 520], + 13484: ["MOVE", 772, 529, 520, True], + 13485: ["ADD", 497, 772, "-4", 520], + 13486: ["MOVE", 772, 520, 737, True], + 13487: ["ADD", 451, 772, "-4", 737], + 15459: ["MOVE", 497, 520, 914, False], + END: ["ADD", 145, 161, "-1/2", 914], +} + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def source(): + pin = json.loads((HERE / "UPSTREAM.json").read_bytes()) + raw = (HERE / "inputs/pr6144-WORD.json.gz").read_bytes() + need(len(raw) == pin["size"], "Source size") + need(sha256(raw).hexdigest() == pin["sha256"], "Source SHA256") + blob = sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw).hexdigest() + need(blob == pin["git_blob"], "Source Git blob") + word = json.loads(gzip.decompress(raw)) + need((word["public"], word["owned_fields"]) == (770, 29), "Role bound") + need(len(word["program"]) == 22818, "Frozen event bound") + need(len(word["frames"]) == 1093, "Frozen frame bound") + return word, pin + + +def proposed(word): + """Return an explicit attempted edit and its base-indexed cut locations.""" + for index, event in ANCHORS.items(): + need(word["program"][index] == event, "Source anchor " + str(index)) + removed = {12888, 12932, 12933, 12934, 13484, 13485, 13486} + events, cuts = [], {} + for index, event in enumerate(word["program"]): + cuts[index] = len(events) + if index in removed: + continue + if index == 12918: + events.extend([["MOVE", 497, 3, 737, False], + ["ADD", 497, 228, "1", 737]]) + if index == 13487: + events.extend([["MOVE", 772, 529, 737, True], + ["ADD", 497, 772, "-4", 737]]) + replacement = ["MOVE", 497, 737, 914, False] + events.append(replacement if index == 15459 else list(event)) + changed = deepcopy(word) + changed["program"] = events + need(all(e[2] != 161 for e in events[cuts[BEGIN]:cuts[END]] + if e[0] in ("ADD", "COPY")), "No receiver feedback in window") + return changed, cuts[BEGIN], cuts[END] + + +def span(basis): + values = {0} + need(len(basis) <= 9, "Frame dimension bound") + for vector in basis: + need(type(vector) is int and 0 < vector < 512, "Binary frame vector") + need(vector not in values, "Independent frame basis") + values |= {x ^ vector for x in tuple(values)} + return values + + +def witness_trace(word, begin, end, witness): + """Scan every cut, including cuts having no existing receiver ADD.""" + frames = [span(basis) for basis in word["frames"]] + current = list(word["initial"]) + [None] * 29 + values = [witness.get(r, Fraction(0)) for r in range(799)] + observed = comparisons = 0 + for index, event in enumerate(word["program"][:end + 1]): + if begin <= index: + need(values[161] == 0, "Receiver starts and stays zero") + for role in range(799): + if role != 161 and current[role] == current[161]: + need(values[role] == 0, "Every available source vanishes") + comparisons += 1 + observed += 1 + if index == end: + break + op, role = event[:2] + if op == "MOVE": + _, role, old, new, private = event + need(current[role] == old, "Move source frame") + need(frames[new] < frames[old] if private else + frames[old] < frames[new], "Nested move") + current[role] = new + elif op in ("INIT", "CLEAR"): + values[role] = Fraction(0) + current[role] = event[2] if op == "INIT" else None + else: + coefficient, frame = Fraction(event[-2]), event[-1] + need(current[role] == frame, "Scalar destination frame") + if op == "SCALE": + values[role] *= coefficient + else: + donor = event[2] + need(current[donor] == frame, "Scalar source frame") + need(op in ("ADD", "COPY"), "Scalar opcode") + value = coefficient * values[donor] + values[role] = value if op == "COPY" else values[role] + value + return {"cuts": observed, "coframed_source_checks": comparisons, + "receiver_value": str(values[161])} + + +def add_row(destination, row, coefficient): + for symbol, value in row.items(): + updated = destination.get(symbol, 0) + coefficient * value + if updated: + destination[symbol] = updated + else: + destination.pop(symbol, None) + + +def symbolic_prefix(word, end): + """Independent full symbolic rows, without the witness observer.""" + rows = [{r: Fraction(1)} for r in range(799)] + for event in word["program"][:end]: + op, role = event[:2] + if op == "MOVE": + continue + if op in ("INIT", "CLEAR"): + rows[role] = {} + elif op == "SCALE": + rows[role] = {s: Fraction(event[-2]) * value + for s, value in rows[role].items()} + elif op == "COPY": + rows[role] = {s: Fraction(event[-2]) * value + for s, value in rows[event[2]].items()} + else: + need(op == "ADD", "Symbolic opcode") + need(role != event[2], "Distinct ADD roles") + add_row(rows[role], rows[event[2]], Fraction(event[-2])) + return rows + + +def rejected(action): + try: + action() + except ValueError: + return + raise ValueError("False-claim control was accepted") + + +def establish(word): + changed, begin, end = proposed(word) + observed = witness_trace(changed, begin, end, WITNESS) + original = symbolic_prefix(word, END) + edited = symbolic_prefix(changed, end) + missing = {r: Fraction(1) for r in (32, 48, 85, 98)} + need(symbolic_prefix(word, 12932)[48] == missing, "Old register-48 read") + differences = {} + for role in range(799): + difference = dict(edited[role]) + add_row(difference, original[role], Fraction(-1)) + if difference: + differences[role] = difference + need(differences == {497: {r: -v for r, v in missing.items()}, + 161: {r: v / 2 for r, v in missing.items()}}, + "Exact full-input effect of this edit at the consumer cut") + target = sum(value * WITNESS.get(r, 0) + for r, value in original[161].items()) + need(target == Fraction(-1, 2), "Nonzero required consumer input") + need(sum(value * WITNESS.get(r, 0) + for r, value in edited[161].items()) == 0, "Symbolic witness") + return changed, begin, end, observed, target, missing + + +def controls(word, changed, begin, end): + bad = deepcopy(word) + bad["program"][12932][-2] = "2" + rejected(lambda: proposed(bad)) + wrong = {32: Fraction(1), 5: Fraction(1)} + rejected(lambda: witness_trace(changed, begin, end, wrong)) + bad = deepcopy(changed) + bad["program"][begin:begin] = [["ADD", 161, 48, "1", 3]] + rejected(lambda: witness_trace(bad, begin, end + 1, WITNESS)) + bad = deepcopy(changed) + bad["program"][begin:begin] = [["ADD", 161, 497, "1", 3]] + rejected(lambda: witness_trace(bad, begin, end + 1, WITNESS)) + bad = deepcopy(changed) + site = bad["program"].index(["ADD", 497, 772, "-4", 737]) + bad["program"][site][-2] = "-3" + rejected(lambda: need(symbolic_prefix(bad, end)[497] == + symbolic_prefix(changed, end)[497], "Root coefficient")) + return ["changed_source_anchor", "wrong_witness_sign", + "unavailable_48_read", "unavailable_497_read", "wrong_root_read"] + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path) + args = parser.parse_args() + word, pin = source() + changed, begin, end, observed, target, missing = establish(word) + result = {"status": "PASS_ROOT2_RECEIVER_OBSTRUCTION", "claim_type": + "Scoped linear obstruction with an exact finite certificate", + "source_sha256": pin["sha256"], "source_head": pin["head"], + "base_window": [BEGIN, END], "edited_window": [begin, end], + "edited_events": len(changed["program"]), + "witness": {str(k): str(v) for k, v in WITNESS.items()}, + "missing_form": {str(k): str(v) for k, v in missing.items()}, + "required_receiver_value": str(target), "observation": observed, + "verifier_sha256": sha256(Path(__file__).read_bytes()).hexdigest(), + "controls": controls(word, changed, begin, end)} + rendered = (json.dumps(result, sort_keys=True, indent=2) + "\n").encode() + if args.output: + need(args.output.write_bytes(rendered) == len(rendered), "Receipt write") + else: + need(rendered == (HERE / "RESULT.json").read_bytes(), + "Exact generated receipt") + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()