diff --git a/research/p104-selected-scalar-pair/README.md b/research/p104-selected-scalar-pair/README.md new file mode 100644 index 0000000000..8e2823e5e8 --- /dev/null +++ b/research/p104-selected-scalar-pair/README.md @@ -0,0 +1,188 @@ +# Six fewer scalar allowance units after P104 sign normalization + +One exact replacement removes an ADD macro from both the selected #5599 +word and its published #5750 sign normalization. It reduces the latter's +retained real scalar allowance from **219258 to 219252**, adding six units +to Sricharan Vagvala's credited 974-unit saving. It preserves all 748 public +inputs, all helper targets, the eight owned-role slots and every one of the +3447 paid MOVE occurrences. The complete paid and productive rank profiles +are identical, so no new kappa is claimed. + +| Pinned word | Events before | Events after | Scalar before | Scalar after | +| --- | ---: | ---: | ---: | ---: | +| Selected #5599 | 25475 | 25474 | 220232 | 220226 | +| Sign-normalized #5750 | 25253 | 25252 | 219258 | 219252 | + +Claim type: **exact finite circuit improvement with a scoped all-input +algebraic proof**. Search stopped at this first verified improvement. +Publication overlap checking then identified #5750. The same literal block +survives there, allowing composition without another improvement search. + +## The replacement + +In `research/p104-helper-subspace-splits/WORD.json.gz`, replace zero-based +events 9751 through 9754, inclusive. The identical block is at events 9627 +through 9630 in `research/p104-sign-gauge/WORD.json.gz`: + +```text +225 += -234 +229 += 234 +227 += 234 +225 += -234 +``` + +with: + +```text +225 += -2 * 234 +229 += 234 +227 += 234 +``` + +Every operation uses frame 267. The actual source prefix places all four +roles in that frame. Role 234 remains unchanged, and neither intervening +operation reads role 225. For arbitrary initial values a,b,c,d in roles +225,229,227,234, both blocks therefore return + +```text +(a - 2d, b + d, c + d, d). +``` + +This identity holds over the complex payload space at every tensor width. +The prefix and suffix of the complete word are retained verbatim. Composing +either block with those identical contexts gives the same complete endpoint, +including arbitrary dirty inputs and every helper output. This argument +permits arbitrary native maps outside the block; it does not need to replay +or assume any new identity between those maps. + +The new value of each role at each macro boundary already occurs for that +role at some old boundary. In particular, the earlier value a-2d is the old +block's final value. Thus this replacement does not increase the maximum +per-role magnitude at scalar macro boundaries. Internal primitive states, +rounding sites and error propagation are separate questions. + +The executable constructor in [verify.py](verify.py) authenticates the source +bytes and replaces only this literal block, in memory. The canonical JSON +hash of the constructed sign-normalized word is +`bc123d9989d919caa48086b19a342fa83d8470d6a56e6ceb8d73b43f4ee84f9d`. +No regenerated gzip container is required. + +## Exact cost and unchanged recursive bill + +The retained `local.py` scalar tariff charges an ADD with nonzero dyadic +coefficient q, numerator magnitude n and positive denominator d, by + +```text +2 * (3 + bit_length(n) - 1 + popcount(n) + bit_length(d) - 1). +``` + +An ADD with coefficient -1 costs 8; coefficient -2 costs 10. The removed +pair costs 16 and its replacement costs 10. The other two ADDs remain. +The complete scalar allowance consequently falls by exactly six units +for each pinned source. The verifier independently sums this tariff over +the original and replacement in both cases, +including their SCALE, COPY, INIT and CLEAR charges. + +Every non-ADD event is retained in its original order, with identical ports, +frames and ownership flags. No additional native map, source acquisition, +helper basis change or allocation is required. Setup and dispatch for a +physical caller still need that caller's own accounting; six units is a +saving in the stated scalar allowance, not a measured runtime saving. + +## Evidence and reproduction + +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 -I -B research/p104-selected-scalar-pair/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -O -B research/p104-selected-scalar-pair/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-selected-scalar-pair +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-selected-scalar-pair --check-source-history +``` + +Another CPython 3.12 interpreter may replace the local path. The expected +status is `PASS_P104_SELECTED_SCALAR_PAIR`, with `scalar_saving` equal to 6. +The verifier writes no files. Its stdout receipt binds all five package +files and each compressed and decompressed source hash. + +The checks include exact rational four-role matrices and every local prefix, +the actual common-frame cut, identical contexts and non-ADD occurrences, +and complete normalized 756-row coefficient propagation for each source +and its replacement. +Normalization treats MOVE as a chart identification. That last comparison +corroborates the scalar endpoint; it does not compute native Gaussian actions +or phases. The local identity and identical-context proof establish equality +in the presence of the actual unchanged native operations. + +Eleven controls per source reject wrong coefficients, sign, source, +destination or frame; a missing fanout; changed helper metadata or paid transport; an +intervening source update or target observation; and a changed source block. +All controls use explicit exceptions and remain active under `-O`. + +## Scope, provenance and credit + +The source base is canonical main +`19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision 8. Exact Git +blobs and SHA256 pins are in [SOURCES.json](SOURCES.json). The selected +record and catalogue are provenance, so subsequent priority updates do not +change this fixed result. The two source words are the only runtime inputs. + +This is a changed `p104-side-correction` experiment aimed at the current +complex supplier. Its result is a scalar circuit improvement. No later +supplier word is optimized, and no full selected replay, compiler admission, native +phase replay, rounded multiplier or proof-kernel build is performed. +The selected construction's five framework assumptions remain. Exact +algebraic equivalence does not assert equality of two rounded executions. + +This contribution was **produced by Nick Petalas**. Ali Romman supplied the +selected #5599 independent-helper-split word. Pierre-Loic Doulcet supplied +the #5565 commuting-contact lineage; David Arias the coalesced word; Gareth +Davidson its composition; and Cinna Davis the private reuse and productive +controller lineage. The source README retains the full P104, native, +geometry, caller, compiler and pricing attribution. + +Cinna Davis's #4692 already supplied commuting-ADD compression and triangle +rewrites for an older 632-public-input word. The commutation method keeps +that credit. Sricharan Vagvala / theon199 supplied the published #5750 +sign-normalized word and its 974-unit saving. The new artifact is this +literal six-unit reduction, including its composition with that word. +No predecessor executable is imported or modified. Independent human and +formal proof-kernel review are unclaimed. +Apache-2.0. + +## Verification bounds and deviations + +All loops are bounded by the authenticated source: at most 25475 events, +1089 frames, 756 symbolic rows and 756 columns per row. The local check uses +four roles and at most four events; there are eleven fixed controls per source. +Reads are capped at 256 KiB compressed and 4 MiB decompressed. No recursion, +dynamic code loading, subprocess, network access or mutable shared state +is used. Functions remain below 60 lines. Warning-strict normal and optimized +execution, Ruff 0.17.2 checks and syntax and indentation diagnostics check +the touched code. + +Power of Ten rule 3 deviation: Python and Fraction allocate during this +bounded offline calculation. The exact source hash and the explicit bounds +above constrain live collections; the verifier has no service loop or +unbounded input domain. A fixed-capacity implementation would be needed +before reusing this checker in a streaming or real-time component. The +registered timeout is an additional execution guard, not a proof of a +memory or arithmetic complexity bound. + +Rule 9 deviation: the rejection-control helper accepts one of three fixed +checker functions, `local_identity`, `boundaries` or `construct`. This is the +control substitution boundary; no source data selects a callable. Its fixed +call sites and eleven rejection cases constrain and exercise every target. +Replace it with explicit dispatch if the control interface ever accepts +external definitions. + +## Open next questions + +1. Can a later scalar rewrite eliminate an actual paid frame transition? + Specify one different block's complete entry and exit frames, and price + every changed native occurrence. The present scalar saving does not + change the signed recursive moment; no later block was searched. +2. Does an active successor retain this exact block? Locate it by roles, + coefficients and frame in one pinned successor, then establish its legal + boundary. Event indices alone cannot transfer the patch, and successor + helper bases may differ. No such transfer is supplied or reserved. diff --git a/research/p104-selected-scalar-pair/SOURCES.json b/research/p104-selected-scalar-pair/SOURCES.json new file mode 100644 index 0000000000..88960850ab --- /dev/null +++ b/research/p104-selected-scalar-pair/SOURCES.json @@ -0,0 +1,60 @@ +{ + "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-helper-subspace-splits/WORD.json.gz", + "usage": "input", + "git_blob": "e325091e3051afe37a2d9c82f85afe9028510edb", + "sha256": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099" + }, + { + "path": "research/p104-helper-subspace-splits/local.py", + "usage": "provenance", + "git_blob": "e6e28bacdad7cb51400d827b9a6e02f2b605d357", + "sha256": "ef430511ce36fc658ab711bd84cd2d7b484b8af173238ff89cbfec6139fefbad" + }, + { + "path": "research/p104-helper-subspace-splits/README.md", + "usage": "provenance", + "git_blob": "f6303a881379723e1f6512dfe153fafeecbf62dd", + "sha256": "a83c5c3ae7a31a5dfbc3c7c59669ee55cc15f966a0cb4405cb48cb8fa2a94f56" + }, + { + "path": "research/scalar-trace-compression/README.md", + "usage": "provenance", + "git_blob": "c85993d7048b287cdf2b4a1852dfb2dc18eb320f", + "sha256": "5ccdab3e70502840fabcb4b234db88c024ee3f28ff9ca7e2e7e4dc3c3115a794" + }, + { + "path": "research/p104-sign-gauge/WORD.json.gz", + "usage": "input", + "git_blob": "8d58e759a8650b0280f1f9ff82b60330035b6a24", + "sha256": "4df09a16721231d6329ebf48779319a6d2c4ff059e6fb939fd272af18f9dc674" + }, + { + "path": "research/p104-sign-gauge/README.md", + "usage": "provenance", + "git_blob": "a13bbdfd90eb097ff4df18d032d90ecf5fb11eea", + "sha256": "467138707f6ea693d9f11c06e5fa214a73d00e8271f7d3e7a4804cd81400cad3" + }, + { + "path": "research/p104-sign-gauge/NOTICE", + "usage": "provenance", + "git_blob": "8f9470a9e0b94599916e5029b74b062db0a379ef", + "sha256": "f1280483dc93b1219c867c4e9b963ef2ae2e90cc66ec364abcf1378422c2b122" + } + ] +} diff --git a/research/p104-selected-scalar-pair/TASK.json b/research/p104-selected-scalar-pair/TASK.json new file mode 100644 index 0000000000..a7fb81f0b3 --- /dev/null +++ b/research/p104-selected-scalar-pair/TASK.json @@ -0,0 +1,147 @@ +{ + "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": "Replace one verified commuting equal-ADD pair in the selected #5599 word and compose that same six-unit saving with the published #5750 sign-normalized word. No further improvement search.", + "scope_change_reason": "The initially inspected connector-alphabet card did not supply an unclaimed question. This original experiment attacks the current complex supplier through the P104 scalar word, and stops at its first verified local circuit improvement.", + "bottleneck_link": "Reduces the selected supplier scalar implementation allowance while retaining its entire productive and paid recursive profile. This is a local circuit improvement, not a kappa gain.", + "budget_minutes": 60, + "stop_rule": "Stop searching as soon as one exact same-chart rewrite strictly lowers the retained scalar tariff. Package only that first rewrite; do not optimize further.", + "outcome": "completed", + "evidence": "README.md local identity and context proof; verify.py exact rational local matrices, complete normalized dirty-endpoint comparisons, frame/paid-occurrence preservation, enumerated tariffs and eleven rejecting controls per pinned word.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a later legal scalar rewrite change an actual paid frame transition rather than only the scalar allowance?", + "why_it_matters": "The six-unit saving leaves the signed recursive moment unchanged.", + "first_step": "Select a different local block, specify its complete entry and exit frames, and price every changed native occurrence.", + "blocked_by": "No later search or complete changed native invoice is supplied here." + }, + { + "question": "Does an active successor retain this exact four-operation block?", + "why_it_matters": "The patch is bound to two exact published words and cannot be transferred by matching event indices.", + "first_step": "Identify the block by its roles, coefficients and common frame in one exact successor, then prove its legal boundary.", + "blocked_by": "Successor words and their independent target bases may differ; none is optimized here." + } + ], + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19221530", + "claim_type": "exact finite circuit improvement with a scoped all-input algebraic proof", + "environment": { + "python": "CPython 3.12.15", + "platform": "Darwin arm64", + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12" + }, + "predecessors": [ + { + "pr": 5599, + "author": "Ali Romman", + "role": "Selected P104 word, independent targets and tariff" + }, + { + "pr": 5750, + "author": "Sricharan Vagvala / theon199", + "role": "Published sign-normalized selected word; its 974-unit saving is inherited" + }, + { + "pr": 4692, + "author": "Cinna Davis", + "role": "Commuting-ADD compression precedent on a different older word" + } + ] +} diff --git a/research/p104-selected-scalar-pair/VERIFY.json b/research/p104-selected-scalar-pair/VERIFY.json new file mode 100644 index 0000000000..8dda4308af --- /dev/null +++ b/research/p104-selected-scalar-pair/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper-subspace-splits/WORD.json.gz", + "research/p104-sign-gauge/WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact local all-input identity, complete normalized endpoint equality, unchanged native events and boundaries, exact six-unit scalar saving and semantic rejection controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat the complete check with assertions disabled." + } + ] +} diff --git a/research/p104-selected-scalar-pair/verify.py b/research/p104-selected-scalar-pair/verify.py new file mode 100644 index 0000000000..36ea63c76c --- /dev/null +++ b/research/p104-selected-scalar-pair/verify.py @@ -0,0 +1,258 @@ +#!/usr/bin/env python3 +"""Check one smaller selected P104 circuit. Produced by Nick Petalas. + +Apache-2.0. The source word and tariff retain the credits in README.md. +No predecessor executable is imported, and no source file is changed. +""" +import gzip +import io +import json +import sys +from collections import Counter +from copy import deepcopy +from fractions import Fraction +from hashlib import sha256 +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +CASES = ( + ("selected", "research/p104-helper-subspace-splits/WORD.json.gz", + 9751, 25475, 220232, 220226), + ("sign_gauge", "research/p104-sign-gauge/WORD.json.gz", + 9627, 25253, 219258, 219252), +) +BEFORE = [ + ["ADD", 225, 234, "-1", 267], + ["ADD", 229, 234, "1", 267], + ["ADD", 227, 234, "1", 267], + ["ADD", 225, 234, "-1", 267], +] +AFTER = [ + ["ADD", 225, 234, "-2", 267], + ["ADD", 229, 234, "1", 267], + ["ADD", 227, 234, "1", 267], +] +ROLES = (225, 227, 229, 234) + + +def need(value, message): + if not value: + raise ValueError(message) + + +def digest(value): + raw = json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + return sha256(raw).hexdigest() + + +def source_word(source, events): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + pin = next(row for row in manifest["files"] if row["path"] == source) + with (ROOT / source).open("rb") as stream: + raw = stream.read(262145) + need(len(raw) <= 262144, "Compressed source bound") + need(sha256(raw).hexdigest() == pin["sha256"], "Source hash") + with gzip.GzipFile(fileobj=io.BytesIO(raw)) as stream: + payload = stream.read(4194305) + need(len(payload) <= 4194304, "Uncompressed source bound") + word = json.loads(payload) + need(word["public"] == 748, "Exact public boundary") + need(len(word["program"]) == events <= 25475, "Exact source length") + need(len(word["frames"]) == 1089, "Exact frame inventory") + return word, sha256(raw).hexdigest(), sha256(payload).hexdigest() + + +def construct(word, start): + need(word["program"][start:start + 4] == BEFORE, "Exact source block") + changed = deepcopy(word) + changed["program"][start:start + 4] = deepcopy(AFTER) + return changed + + +def local_prefixes(program): + need(0 < len(program) <= 4, "Local length bound") + rows = {r: tuple(Fraction(r == s) for s in ROLES) for r in ROLES} + prefixes = [dict(rows)] + for event in program: + need(event[0] == "ADD" and len(event) == 5, "Local ADD grammar") + _, dst, src, coefficient, frame = event + need(dst in ROLES and src in ROLES and dst != src, "Local ports") + need(frame == 267, "One local chart") + q = Fraction(coefficient) + rows[dst] = tuple(a + q*b for a, b in zip(rows[dst], rows[src], strict=True)) + prefixes.append(dict(rows)) + return prefixes + + +def local_identity(before, after): + old, new = local_prefixes(before), local_prefixes(after) + need(old[-1] == new[-1], "Exact dirty local endpoint") + for role in ROLES: + values = {prefix[role] for prefix in old} + need(all(prefix[role] in values for prefix in new), + "No new macro-boundary row value") + return {"roles": len(ROLES), "basis_columns": len(ROLES), + "before_prefixes": len(old), "after_prefixes": len(new)} + + +def boundaries(word, changed, start): + need({k: v for k, v in word.items() if k != "program"} == + {k: v for k, v in changed.items() if k != "program"}, + "All boundary metadata unchanged") + need(word["program"][:start] == changed["program"][:start], "Same prefix") + need(word["program"][start + 4:] == changed["program"][start + 3:], + "Same suffix") + current = word["initial"][:] + [None]*8 + for event in word["program"][:start]: + if event[0] == "MOVE": + current[event[1]] = event[3] + elif event[0] == "INIT": + current[event[1]] = event[2] + elif event[0] == "CLEAR": + current[event[1]] = None + need(all(current[r] == 267 for r in ROLES), "Actual common-frame cut") + old = [e for e in word["program"] if e[0] != "ADD"] + new = [e for e in changed["program"] if e[0] != "ADD"] + need(old == new, "Every non-ADD occurrence unchanged") + paid = [e for e in old if e[0] == "MOVE"] + profile = Counter(abs(len(word["frames"][e[3]]) - + len(word["frames"][e[2]])) for e in paid) + return {"paid_occurrences": len(paid), "paid_profile": dict(profile), + "public_inputs": word["public"], "owned_role_slots": 8} + + +def add_row(destination, source, coefficient): + for column, value in source.items(): + total = destination.get(column, Fraction(0)) + coefficient*value + if total: + destination[column] = total + else: + destination.pop(column, None) + + +def normalized_endpoint(word): + """Compare complete coefficients; MOVE is a chart identification here. + + The separate local context proof covers arbitrary actual native maps. + This diagnostic is not a replay of their Gaussian action or phases. + """ + count = word["public"] + 8 + need(count == 756 and len(word["program"]) <= 25475, "Endpoint bounds") + rows = [{r: Fraction(1)} for r in range(count)] + for event in word["program"]: + op, dst = event[:2] + need(0 <= dst < count, "Endpoint destination bound") + if op == "MOVE": + continue + if op in ("INIT", "CLEAR"): + rows[dst] = {} + elif op == "SCALE": + q = Fraction(event[-2]) + rows[dst] = {c: q*v for c, v in rows[dst].items()} + else: + need(op in ("ADD", "COPY"), "Endpoint opcode") + src, q = event[2], Fraction(event[-2]) + need(0 <= src < count and src != dst, "Endpoint source bound") + if op == "COPY": + rows[dst] = {c: q*v for c, v in rows[src].items()} + else: + add_row(rows[dst], rows[src], q) + return rows + + +def scalar_tariff(program): + total = 0 + for event in program: + op = event[0] + if op == "MOVE": + continue + if op in ("INIT", "CLEAR"): + total += 2 + continue + q = Fraction(event[-2]) + n, d = abs(q.numerator), q.denominator + need(n > 0 and d & (d - 1) == 0, "Nonzero dyadic scalar") + if op == "SCALE": + need(n & (n - 1) == 0, "Dyadic unit scale") + total += 2*(abs(n.bit_length() - d.bit_length()) + int(q < 0)) + else: + need(op in ("ADD", "COPY"), "Tariff opcode") + total += 2*(3 + n.bit_length() - 1 + n.bit_count() + + d.bit_length() - 1) + return total + + +def rejects(function, *args): + try: + function(*args) + except ValueError: + return 1 + raise ValueError("A semantic mutation was accepted") + + +def controls(word, changed, start): + count = 0 + for position, replacement in ((3, "-1"), (3, "2"), (1, 229), + (2, 229), (4, 266)): + wrong = deepcopy(AFTER) + wrong[0][position] = replacement + count += rejects(local_identity, BEFORE, wrong) + count += rejects(local_identity, BEFORE, AFTER[:2]) + wrong = deepcopy(changed) + wrong["final"][225] = wrong["initial"][225] + count += rejects(boundaries, word, wrong, start) + wrong = deepcopy(changed) + move = next(e for e in wrong["program"] if e[0] == "MOVE") + move[3] = (move[3] + 1) % len(word["frames"]) + count += rejects(boundaries, word, wrong, start) + # A source update and a target observation block this shortcut. + for middle in (("ADD", 234, 229, "1", 267), + ("ADD", 229, 225, "1", 267)): + before = [BEFORE[0], list(middle), BEFORE[-1]] + after = [AFTER[0], list(middle)] + count += rejects(local_identity, before, after) + wrong = deepcopy(word) + wrong["program"][start][3] = "1" + count += rejects(construct, wrong, start) + return count + + +def run_case(case): + name, source, start, events, expected_old, expected_new = case + word, source_hash, payload_hash = source_word(source, events) + changed = construct(word, start) + local = local_identity(BEFORE, AFTER) + boundary = boundaries(word, changed, start) + old_rows = normalized_endpoint(word) + new_rows = normalized_endpoint(changed) + need(old_rows == new_rows, "Complete normalized dirty endpoint equality") + old_cost = scalar_tariff(word["program"]) + new_cost = scalar_tariff(changed["program"]) + need((old_cost, new_cost) == (expected_old, expected_new), + "Exact full scalar tariff") + need(len(changed["program"]) == events - 1, "One removed scalar macro") + endpoint = [[[c, str(v)] for c, v in sorted(row.items())] for row in new_rows] + return {"case": name, "local": local, + "boundary": boundary, "normalized_rows": len(new_rows), + "normalized_endpoint_sha256": digest(endpoint), + "source_sha256": source_hash, "source_payload_sha256": payload_hash, + "candidate_canonical_json_sha256": digest(changed), + "events_before": len(word["program"]), + "events_after": len(changed["program"]), + "scalar_before": old_cost, "scalar_after": new_cost, + "scalar_saving": old_cost - new_cost, + "rejecting_controls": controls(word, changed, start)} + + +def run(): + need(len(sys.argv) == 1, "No command-line arguments accepted") + files = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + return {"status": "PASS_P104_SELECTED_SCALAR_PAIR", + "cases": [run_case(case) for case in CASES], + "package_sha256": {f: sha256((HERE / f).read_bytes()).hexdigest() + for f in files}} + + +if __name__ == "__main__": + print(json.dumps(run(), indent=2, sort_keys=True))