From 6dd2ecbe34847270559316d7f1e3590f9fe11be0 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 21:09:06 +0000 Subject: [PATCH] feat(research): share P104 reads through a dirty output --- research/p104-dirty-anchor-window/README.md | 161 ++++++++++++ .../p104-dirty-anchor-window/SOURCES.json | 30 +++ research/p104-dirty-anchor-window/TASK.json | 117 +++++++++ research/p104-dirty-anchor-window/VERIFY.json | 34 +++ research/p104-dirty-anchor-window/patch.py | 58 +++++ research/p104-dirty-anchor-window/verify.py | 229 ++++++++++++++++++ 6 files changed, 629 insertions(+) create mode 100644 research/p104-dirty-anchor-window/README.md create mode 100644 research/p104-dirty-anchor-window/SOURCES.json create mode 100644 research/p104-dirty-anchor-window/TASK.json create mode 100644 research/p104-dirty-anchor-window/VERIFY.json create mode 100644 research/p104-dirty-anchor-window/patch.py create mode 100644 research/p104-dirty-anchor-window/verify.py diff --git a/research/p104-dirty-anchor-window/README.md b/research/p104-dirty-anchor-window/README.md new file mode 100644 index 0000000000..fd4cee7b4a --- /dev/null +++ b/research/p104-dirty-anchor-window/README.md @@ -0,0 +1,161 @@ +# Two fewer P104 events by sharing through a dirty output + +This contribution was produced by Nick Petalas. + +An exact local replacement on DreamingOfClouds's +[PR5907](https://github.com/CrocSwap/integer-mult-bounds/pull/5907) word removes +two ordinary events and twenty real scalar allowance units. Events fall from +25,998 to 25,996; the complete local scalar allowance falls from 228,664 to +228,644 under the retained PR5827 tariff. This is a scoped exact circuit +construction, with a finite certificate for the complete modified word. +It supplies no new kappa. + +The original question is Matarener's global ordinary-resynthesis next question +in [PR5975](https://github.com/CrocSwap/integer-mult-bounds/pull/5975). +That package's compression and results are cited, not independently checked. +This replacement introduces a dependency between two destinations. It does +not merge repeated ordered ADD pairs, normalize signs or apply a three-gate +triangle identity. The first positive candidate ended the search. + +## Exact replacement + +Indices are zero-based in the pinned PR5907 program. All contacts below use +frame 3, the empty binary basis. Let a be field 159, b field 158, and + +```text +f = field133 + 2 field721 + field21 - 2 field711. +``` + +Remove these four events: + +```text +509: b += -2 field711 +660: b += field133 +663: b += 2 field721 +664: b += field21 +``` + +Keep the four updates accumulating f into a at indices 667, 669, 670 and +671. Immediately before 667 insert `b -= a`; immediately after 671 insert +`b += a`. Every other event is kept in its original order. [patch.py](patch.py) +constructs this exact candidate and checks its window premises. + +Fields a and b both have arbitrary initial values. Neither is read anywhere +in the old window [509,672), and the four sources of f are constant throughout +that window. The only updates to a in the window are its four shared-form +updates. Other updates to b contribute a form h. Thus both circuits have + +```text +a_out = a_in + f +b_out = b_in + h + f. +``` + +In the replacement, the b value just before the final insertion is +`b_in + h - a_in`. Adding `a_in + f` gives the required result. This proves +the identity for every input over the rationals or complexes, including +every dirty a and b. All other rows coincide because the window contains +no observation of either output. No zero temporary or borrowed-state +assumption is used. Equality at this cut composes with the identical prefix +and suffix, so the complete exact linear operator is unchanged. + +The removed coefficients are -2, 1, 2, 1. Under PR5827's ADD allowance + +```text +cost(q) = 2 (3 + bit_length(abs(num(q))) - 1 + + popcount(abs(num(q))) + bit_length(den(q)) - 1), +``` + +they cost 10+8+10+8=36. The two inserted unit ADDs cost 8+8=16. Hence the +saving is exactly twenty units and two events. This is an instruction +allowance comparison, not a timing measurement or an optimality claim. + +## Evidence and reproduction + +Python 3.12 and the standard library suffice. From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/p104-dirty-anchor-window/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B -O research/p104-dirty-anchor-window/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-dirty-anchor-window +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-dirty-anchor-window --check-source-history +``` + +Any CPython 3.12 installation may replace that path. The expected markers are +`PASS_P104_DIRTY_ANCHOR_WINDOW`, `PASS_REGISTERED_RESEARCH_PACKAGE` and +`PASS_RESEARCH_COMMIT_BYTES`. Normal verification writes no files. The verifier +prints a generated JSON receipt containing package SHA256 hashes and the +canonical candidate payload hash. To materialize the candidate, add +`--emit-word /absolute/external/path/WORD.json`. The path must be outside the +checkout and must not exist. + +The verifier authenticates the source before using it, checks exact matrix +equality on all 100 fields touched in the 163-event window, and replays only +the complete modified word on all 799 independent input columns. Its sparse +rational endpoint rows specify all 638,401 matrix entries, including zeros. +Every new ADD has physically available equal frames. All 31 owned lifetimes +return, with peak occupancy 13. Every non-ADD event and every boundary, +frame, port and helper inventory field is byte-for-byte equal as parsed data. +The canonical uncompressed candidate SHA256 is +`5c2ed3597871bcbfa5a00194671e75aab95345ba6a91b1c7c7bd1c78eb1ef495`. + +Four matrix controls reject a wrong cancellation sign, wrong source, omitted +subtraction and omitted addition. Five premise controls reject an intermediate +observation of either output, a shared-source write, a wrong frame and a +changed removed coefficient. The local prefix maximum row l1 norm is 17 in +both versions, relative to independent values at this cut. This is not an +actual-input rounded-error or whole-word precision certificate. + +## Scope and credit + +Base is canonical main `19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority +revision 8. [TASK.json](TASK.json) records the changed scope from helper splits +to a scalar side result. The selected-source baseline was used as orientation, +not a scientific replay. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19227524) +records the question before the search. Live open PRs, recent account PRs, +Discussion claims, local reservations, merged searches and main-tree searches +were inspected. The overlap tool's sparse local coverage is incomplete; +these checks are not a proof of novelty. + +Credit DreamingOfClouds for the PR5907 word; Ali Romman for PR5827's source +word, tariff, exact endpoint convention and retained construction; Mason Hale +for PR5811; Matarener for PR5975's resynthesis question; Cinna Davis for +PR4692's commuting and triangle rewrites; and the retained P104, geometry, +native, caller and compiler contributors credited by those packages. +Dirty-output sharing and elementary row algebra are standard predecessor +techniques. The new contribution is this literal changed dependency window, +its twenty-unit bill and its verifier. Predecessor files and credits are unchanged. +New material is Apache-2.0. Independent human and formal proof-kernel review +are unclaimed. + +The complete paid MOVE sequence and productive boundary are identical, so +the signed recursive moment receives no change from this rewrite. No native +map, physical caller, compiler, outer inequality, rounded precision/tape +contract or complete multiplication theorem is newly certified. In particular, +exact endpoint equality does not certify rounded equivalence of changed +intermediate states. The five framework assumptions remain. No selected +frontier file changes, Lean, Docker or predecessor scientific replay are used. + +## Code constraints + +The two Python files use no recursion, external dependencies, generated code, +background jobs or unbounded search. The replay domain is fixed at 799 fields, +fewer than 26,000 events, and at most 2,048 frame descriptions. Local symbolic +rows have at most 799 coefficients; each function is below sixty lines. + +Power-of-Ten rule 3 has a managed-runtime deviation in the sparse rational +replay and JSON parsing. CPython and Fraction allocate during arithmetic. +The pinned source, fixed event and field counts bound live row storage by +799 squared rational entries. Registered commands have 120-second timeouts; +no retained runtime configuration is changed. Verification exercises the +complete fixed domain. A fixed-allocation native implementation would be a +separate backend if memory limits become a binding requirement. Rule 10 uses +warning-strict normal and optimized execution and the repository package +checks; no project-wide diagnostic configuration is changed. + +## Open next questions + +Does this literal rewrite compose with PR5975 compression to provide useful +headroom for a paid-profile improvement? Start at these four shared-form +contacts in the compressed word, preserve every observer, then price one new +productive or paid change. Neither the composition nor a newly funded change +is supplied here. The structured question and blockers are in TASK.json. diff --git a/research/p104-dirty-anchor-window/SOURCES.json b/research/p104-dirty-anchor-window/SOURCES.json new file mode 100644 index 0000000000..a63ffce33b --- /dev/null +++ b/research/p104-dirty-anchor-window/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-helper468-rung-removal/WORD.json.gz", + "usage": "input", + "git_blob": "7ffe7b500b02b9d0de49a85ec53e36004f1a411f", + "sha256": "b69a9cb3a26d4f40aa7ad14f814b188fe16a782999f6f56292538e447d67b284" + }, + { + "path": "research/p104-unread-path-resynthesis/local.py", + "usage": "provenance", + "git_blob": "b7be846b10c4c54a4e1558d7b563bc8c3a170223", + "sha256": "7201df8e32f5c99f7403150e8664042322037906088bc754c67293a241368597" + } + ] +} diff --git a/research/p104-dirty-anchor-window/TASK.json b/research/p104-dirty-anchor-window/TASK.json new file mode 100644 index 0000000000..09700f7858 --- /dev/null +++ b/research/p104-dirty-anchor-window/TASK.json @@ -0,0 +1,117 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "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": "An exact dirty-output sharing replacement in PR5907 ordinary events 509 through 671, saving two events and twenty scalar allowance units.", + "scope_change_reason": "The source question is PR5975 ordinary resynthesis. This side result changes scalar dependencies on the PR5907 word; it does not split productive helper targets or improve the signed recursive moment.", + "bottleneck_link": "PR5907 has 25998 of the retained 26000 events. A shorter same-boundary ordinary window creates two additional event slots and lowers its scalar allowance, without claiming a Gaussian or exponent saving.", + "budget_minutes": 60, + "stop_rule": "Stop at the first exact scalar or event saving and package it without extending the search.", + "outcome": "completed", + "evidence": "The verifier proves local matrix equality on 100 arbitrary fields, replays the modified word on 799 independent columns, checks unchanged non-ADD events and boundaries, recomputes the full scalar tariff, and rejects four algebraic and five premise mutants.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the literal dirty-anchor rewrite compose with PR5975 compression to create useful event headroom for a paid-profile improvement?", + "why_it_matters": "The saved events do not themselves improve the recursive moment. A new physical rewrite must use them to change the full signed invoice.", + "first_step": "Apply the same local identity at its exact literal contacts in the compressed word, preserve its observations, then price one newly enabled paid-profile change.", + "blocked_by": "Composition with the pending compressed word and any new productive or paid change have not been constructed here." + } + ] +} diff --git a/research/p104-dirty-anchor-window/VERIFY.json b/research/p104-dirty-anchor-window/VERIFY.json new file mode 100644 index 0000000000..81590eb0a5 --- /dev/null +++ b/research/p104-dirty-anchor-window/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper468-rung-removal/WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact arbitrary-input local identity, complete candidate endpoints, frame availability, full scalar allowance, unchanged context and nine rejecting controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact arbitrary-input local identity, complete candidate endpoints, frame availability, full scalar allowance, unchanged context and nine rejecting controls." + } + ] +} diff --git a/research/p104-dirty-anchor-window/patch.py b/research/p104-dirty-anchor-window/patch.py new file mode 100644 index 0000000000..80ba716ec1 --- /dev/null +++ b/research/p104-dirty-anchor-window/patch.py @@ -0,0 +1,58 @@ +"""One dirty-output sharing rewrite on DreamingOfClouds's PR5907 word. + +Produced by Nick Petalas. Apache-2.0. +""" +from copy import deepcopy + +START = 509 +STOP = 672 +REMOVED = { + 509: ["ADD", 158, 711, "-2", 3], + 660: ["ADD", 158, 133, "1", 3], + 663: ["ADD", 158, 721, "2", 3], + 664: ["ADD", 158, 21, "1", 3], +} +ANCHOR_START = 667 +ANCHOR_END = 671 +COMMON = {133: "1", 721: "2", 21: "1", 711: "-2"} + + +def need(condition, reason): + if not condition: + raise ValueError(reason) + + +def check_window(program): + """Check the exact sharing premises, including absence of observations.""" + need(len(program) == 25998, "Expected source event count") + for index, event in REMOVED.items(): + need(program[index] == event, "Literal removed event") + anchor_events = [] + for event in program[START:STOP]: + need(event[0] == "ADD" and event[-1] == 3, "Same-frame ADD window") + _, destination, source, coefficient, _ = event + need(source not in (158, 159), "No intermediate output observation") + need(destination not in COMMON, "Shared sources remain constant") + if destination == 159: + anchor_events.append((source, coefficient)) + need(dict(anchor_events) == COMMON and len(anchor_events) == 4, + "Anchor acquires exactly the shared form") + need(program[ANCHOR_START][1] == program[ANCHOR_END][1] == 159, + "Anchor endpoints") + need(all(event[1] != 159 for event in program[START:ANCHOR_START]), + "No earlier anchor update") + + +def rewrite(word): + check_window(word["program"]) + out = deepcopy(word) + program = [] + for index, event in enumerate(word["program"]): + if index == ANCHOR_START: + program.append(["ADD", 158, 159, "-1", 3]) + if index not in REMOVED: + program.append(event) + if index == ANCHOR_END: + program.append(["ADD", 158, 159, "1", 3]) + out["program"] = program + return out diff --git a/research/p104-dirty-anchor-window/verify.py b/research/p104-dirty-anchor-window/verify.py new file mode 100644 index 0000000000..b0c000a9fc --- /dev/null +++ b/research/p104-dirty-anchor-window/verify.py @@ -0,0 +1,229 @@ +"""Exact local identity and complete modified-word replay; no native replay. + +Produced by Nick Petalas. The scalar tariff and logical endpoint convention +retain Ali Romman's PR5827 lineage, cited in README.md. Apache-2.0. +""" +import argparse +from collections import Counter +from fractions import Fraction +import gzip +from hashlib import sha256 +import json +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from patch import START, STOP +from patch import check_window, need, rewrite + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = "research/p104-helper468-rung-removal/WORD.json.gz" +MAX_EVENTS = 26000 +MAX_FIELDS = 799 + + +def authenticated_word(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + pins = {row["path"]: row["sha256"] for row in manifest["files"]} + raw = (ROOT / SOURCE).read_bytes() + need(len(raw) < 2**20 and sha256(raw).hexdigest() == pins[SOURCE], + "Pinned source bytes") + payload = gzip.decompress(raw) + need(len(payload) < 2**23, "Bounded source payload") + word = json.loads(payload) + need(word["public"] == 770 and word["owned_fields"] == 29, + "Pinned field domain") + need(len(word["program"]) < MAX_EVENTS, "Bounded program") + need(len(word["frames"]) <= 2048, "Bounded frame inventory") + return word + + +def add_row(destination, source, coefficient): + need(destination is not source, "Distinct ADD rows") + for column, value in source.items(): + new = destination.get(column, 0) + coefficient * value + if new: + destination[column] = new + else: + destination.pop(column, None) + + +def local_matrix(events): + roles = sorted({role for event in events for role in event[1:3]}) + need(len(roles) <= MAX_FIELDS and len(events) <= MAX_EVENTS, + "Bounded local matrix") + rows = {role: {role: Fraction(1)} for role in roles} + maximum = Fraction(1) + for event in events: + need(event[0] == "ADD", "Local ADD alphabet") + _, destination, source, coefficient, _ = event + add_row(rows[destination], rows[source], Fraction(coefficient)) + maximum = max(maximum, sum(abs(v) for v in rows[destination].values())) + return rows, maximum + + +def scalar_cost(program): + """The exact integer allowance formula of PR5827 local.replay.""" + total = 0 + for event in program: + op = event[0] + if op in ("INIT", "CLEAR"): + total += 2 + elif op in ("ADD", "COPY", "SCALE"): + q = Fraction(event[-2]) + n, d = abs(q.numerator), q.denominator + need(n > 0 and d & (d - 1) == 0, "Nonzero dyadic coefficient") + if op == "SCALE": + total += 2 * (abs(n.bit_length() - d.bit_length()) + int(q < 0)) + else: + total += 2 * (3 + n.bit_length() - 1 + n.bit_count() + + d.bit_length() - 1) + return total + + +def scalar_event(event, rows, frames, live, public): + op, destination = event[:2] + coefficient, frame = Fraction(event[-2]), event[-1] + need(frames[destination] == frame and coefficient != 0, + "Scalar destination frame") + need(destination < public or destination in live, "Live destination") + if op == "SCALE": + rows[destination] = {k: coefficient * v + for k, v in rows[destination].items()} + return + need(op in ("ADD", "COPY"), "Scalar alphabet") + source = event[2] + need(source != destination and 0 <= source < len(rows), "Scalar source") + need(frames[source] == frame and (source < public or source in live), + "Available common-frame source") + if op == "COPY": + need(destination in live and not rows[destination], "COPY into owned zero") + rows[destination] = {k: coefficient * v for k, v in rows[source].items()} + else: + add_row(rows[destination], rows[source], coefficient) + + +def replay_candidate(word): + """Only the new word is executed, on every independent input column.""" + public, owned = word["public"], word["owned_fields"] + need(public + owned == MAX_FIELDS, "Complete column domain") + rows = [{i: Fraction(1)} for i in range(MAX_FIELDS)] + frames = list(word["initial"]) + [None] * owned + live, paid = set(), Counter() + peak = lifetimes = 0 + for event in word["program"]: + op, destination = event[:2] + need(0 <= destination < MAX_FIELDS, "Destination range") + if op == "MOVE": + _, _, start, end, private = event + need(frames[destination] == start, "MOVE source frame") + need((destination in live) == private, "MOVE ownership") + paid[abs(len(word["frames"][start]) - len(word["frames"][end]))] += 1 + frames[destination] = end + elif op == "INIT": + need(destination >= public and destination not in live, "Owned INIT") + rows[destination], frames[destination] = {}, event[2] + live.add(destination) + peak = max(peak, len(live)) + lifetimes += 1 + elif op == "CLEAR": + need(destination in live and frames[destination] == event[2], + "Owned CLEAR") + rows[destination], frames[destination] = {}, None + live.remove(destination) + else: + scalar_event(event, rows, frames, live, public) + need(not live and frames[:public] == word["final"], "All terminal frames") + for i, row in enumerate(rows): + expected = {i: Fraction(1)} if i < public else {} + if i - 112 in word["live"]: + expected[i - 112] = Fraction(1) + need(row == expected, "Complete modified-word endpoint") + return {"columns": MAX_FIELDS, "endpoint_entries": MAX_FIELDS**2, + "owned_lifetimes": lifetimes, "peak_owned_fields": peak, + "paid_moves": dict(sorted(paid.items()))} + + +def check_context(source, candidate): + need({k: v for k, v in source.items() if k != "program"} + == {k: v for k, v in candidate.items() if k != "program"}, + "Every boundary and inventory field retained") + old, new = source["program"], candidate["program"] + need(old[:START] == new[:START] and old[STOP:] == new[STOP - 2:], + "Identical surrounding context") + need([e for e in old if e[0] != "ADD"] + == [e for e in new if e[0] != "ADD"], "All non-ADD events retained") + old_matrix, old_maximum = local_matrix(old[START:STOP]) + new_matrix, new_maximum = local_matrix(new[START:STOP - 2]) + need(old_matrix == new_matrix, "Exact arbitrary-input local equality") + need(len(new) == 25996, "Two-event saving") + need((scalar_cost(old), scalar_cost(new)) == (228664, 228644), + "Complete scalar allowance and twenty-unit saving") + return {"local_roles": len(old_matrix), "old_local_events": STOP - START, + "new_local_events": STOP - START - 2, + "old_local_prefix_l1": str(old_maximum), + "new_local_prefix_l1": str(new_maximum)} + + +def rejection_controls(word, candidate): + baseline, _ = local_matrix(word["program"][START:STOP]) + altered = candidate["program"][START:STOP - 2] + anchor_indices = [i for i, e in enumerate(altered) + if e[1:3] == [158, 159]] + need(len(anchor_indices) == 2, "Two anchor operations") + bad_minus = [list(e) for e in altered] + bad_minus[anchor_indices[0]][3] = "1" + bad_source = [list(e) for e in altered] + bad_source[anchor_indices[1]][2] = 157 + variants = [bad_minus, bad_source, + altered[:anchor_indices[0]] + altered[anchor_indices[0] + 1:], + altered[:anchor_indices[1]] + altered[anchor_indices[1] + 1:]] + for variant in variants: + rows, _ = local_matrix(variant) + need(rows != baseline, "Reject wrong anchor identity") + for index, replacement in [ + (666, ["ADD", 250, 158, "1", 3]), + (666, ["ADD", 250, 159, "1", 3]), + (666, ["ADD", 133, 250, "1", 3]), + (666, ["ADD", 250, 251, "1", 4]), + (509, ["ADD", 158, 711, "2", 3])]: + program = list(word["program"]) + program[index] = replacement + try: + check_window(program) + except ValueError: + continue + raise ValueError("Unsafe source window accepted") + return {"matrix_mutants_rejected": len(variants), + "premise_mutants_rejected": 5} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit-word", type=Path) + args = parser.parse_args() + source = authenticated_word() + candidate = rewrite(source) + context = check_context(source, candidate) + controls = rejection_controls(source, candidate) + replay = replay_candidate(candidate) + payload = json.dumps(candidate, sort_keys=True, separators=(",", ":")).encode() + if args.emit_word is not None: + target = args.emit_word.resolve() + need(not target.is_relative_to(ROOT), "Emit only outside the checkout") + with target.open("xb") as output: + need(output.write(payload + b"\n") == len(payload) + 1, "Complete export") + hashes = {p.name: sha256(p.read_bytes()).hexdigest() + for p in sorted(HERE.iterdir()) if p.is_file()} + result = {"status": "PASS_P104_DIRTY_ANCHOR_WINDOW", + "candidate_payload_sha256": sha256(payload).hexdigest(), + "old_events": 25998, "new_events": 25996, + "old_scalar_allowance": 228664, "new_scalar_allowance": 228644, + "local": context, "candidate_replay": replay, "controls": controls, + "package_sha256": hashes, "new_kappa_claimed": False} + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()