From 1a2ef236d5aeb255af441804a9e37c4aeb350204 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Mon, 2 Nov 2026 19:33:11 +0000 Subject: [PATCH] feat(research): obstruct single-stop P104 helper respanning --- .../p104-respan-stop-obstruction/PROOF.md | 117 ++++++++ .../p104-respan-stop-obstruction/README.md | 86 ++++++ .../p104-respan-stop-obstruction/SOURCES.json | 36 +++ .../p104-respan-stop-obstruction/TASK.json | 128 +++++++++ .../VALIDATION.md | 57 ++++ .../p104-respan-stop-obstruction/VERIFY.json | 37 +++ .../p104-respan-stop-obstruction/verify.py | 262 ++++++++++++++++++ 7 files changed, 723 insertions(+) create mode 100644 research/p104-respan-stop-obstruction/PROOF.md create mode 100644 research/p104-respan-stop-obstruction/README.md create mode 100644 research/p104-respan-stop-obstruction/SOURCES.json create mode 100644 research/p104-respan-stop-obstruction/TASK.json create mode 100644 research/p104-respan-stop-obstruction/VALIDATION.md create mode 100644 research/p104-respan-stop-obstruction/VERIFY.json create mode 100644 research/p104-respan-stop-obstruction/verify.py diff --git a/research/p104-respan-stop-obstruction/PROOF.md b/research/p104-respan-stop-obstruction/PROOF.md new file mode 100644 index 0000000000..41f1a827cf --- /dev/null +++ b/research/p104-respan-stop-obstruction/PROOF.md @@ -0,0 +1,117 @@ +# A fixed contact obstructs a stop deletion + +## Model and claim + +An epoch is a visit by one register to one frame between consecutive MOVE +events. INIT starts a new owned lifetime and CLEAR ends it. An intermediate +stop is an epoch with both an incoming and an outgoing MOVE in the same +lifetime. Initial and terminal epochs are excluded. + +Freeze the word in DreamingOfClouds's PR6345, at the source bytes recorded in +SOURCES.json. Let S be its public non-main registers with exactly one MOVE. +The main registers are `live` and `112 + live`, as in the predecessor contract. + +Consider the following simultaneous relaxation. + +1. Every register in S may replace both endpoint frames by arbitrary binary + subspaces, retaining its unique MOVE at its original position among scalar + events. These endpoint choices need not belong to the published catalogue. +2. Choose one intermediate stop U of a different register r. Replace its two + neighboring transports A -> U -> C by one transport A -> C. This transport + may occur at any cut between the retained surrounding epochs. In particular, + the scalar events formerly at U may be divided between A and C. +3. All other epochs retain their frames, and scalar coefficients, operands, + operations, lifetime boundaries and scalar order are fixed. Scalar chart + annotations may be rewritten, but each ADD or COPY still requires equal + source and destination frames. Additional transports are excluded. + +The new result is a scoped impossibility statement. No such assignment exists +for any intermediate stop of this word. There are exactly 2,660 such stops, +2,654 public and six owned, and S has 42 members. This is a stronger endpoint +freedom than choosing just one helper from the existing native catalogue. + +This statement concerns deletion of one stop while the other non-S epochs +remain fixed. It does not exclude coordinated changes to two non-S registers, +changed scalar schedules, new transports or a different word. + +## Fixed-contact lemma + +Suppose an intermediate stop U of r contains an ADD or COPY involving another +register s. Suppose s is outside S and its epoch at that event stays fixed at +U. If U differs from both neighboring frames A and C, deleting the visit to U +is impossible under the model above. + +Proof. At the contact, the common-chart rule forces r's frame to equal s's +fixed frame U. After replacing A -> U -> C by A -> C, r's frame at every +scalar event between the surrounding epochs is either A or C. Neither is U. +Thus the contact cannot satisfy the common-chart rule. This argument permits +any position of the merged transport and does not depend on the new endpoint +frames of registers in S. QED. + +## Exact application to the frozen word + +`certificate` in verify.py indexes every constant-frame epoch and each +ADD/COPY contact. For every intermediate stop it chooses the first contact +whose other register is outside S. The direct contact itself is the witness; +no transitive equality inference or optimization solver is needed. + +Each witness has seven integers: + +```text +[register, lifetime, stop ordinal, event index, + partner register, partner lifetime, partner epoch ordinal] +``` + +Event indices and public lifetime numbers start at zero. Owned lifetimes start +at one. Stop ordinal k means the epoch after the kth MOVE of that lifetime. +For each candidate, explicit binary spans show strict nesting of the three +neighboring frames, increasing for public registers and decreasing for owned +registers. In particular U differs from A and C as subspaces, irrespective of +frame labels or basis choices. + +Every one of the 2,660 candidates has a direct fixed-partner contact. A second +streaming implementation, `check_certificate`, discovers its candidate set by +recording the epoch left by every MOVE after the first MOVE of a lifetime. +It checks exact candidate coverage, unique witnesses, actual event operands, +both current epoch identities, the common chart and the partner's exclusion +from S. It does not call the primary trace builder or domain enumerator. +The fixed-contact lemma therefore applies separately to every candidate. + +The generated receipt contains every witness and hashes of the input, +decompressed payload and package files. The receipt is generated on request +outside the checkout. Reproduction computes all witnesses anew. + +## Consequence for the open question + +PR6345 asks whether a re-spanned helper can enable a stop drop elsewhere. +For the stated fixed-schedule, single-stop move, even all 42 one-step helpers +together cannot do so. A successful continuation must alter at least one +additional non-S epoch at a blocking contact, change the scalar incidence or +schedule, introduce another transport, or change the word. This is a necessary +change of scope, not a sufficiency theorem for any of these alternatives. + +The predecessor's legality, paid invoice and reported crossing are premises, +not results re-established here. No price calculation or native operator replay +is needed to rule out a move that already fails a necessary chart equality. +No new kappa, supplier admission or complete multiplication theorem is claimed. + +Ali Romman's PR5590 already supplies an all-frame price floor with all scalar +contact frames fixed on PR5580. That theorem is credited rather than repeated. +The present finite step concerns the different PR6345 word and allows helper +contact charts to vary with the 42 re-spanned helpers. It finds a different, +fixed-partner contact at each stop. Common-chart equality is inherited syntax; +the new contribution is its complete source-bound obstruction in this move +domain, not a new general theory of frame transport. + +## Controls and limits + +The verifier rejects an omitted witness, a duplicate witness, five incorrect +contact/epoch fields, a free-helper partner, an unanchored toy and a collapsed +toy with a fixed contact. Two positive toy controls demonstrate an anchored +stop and an actual unanchored stop deletion enabled by helper respanning. +These toys test chart constraints only, not complete productive suppliers. + +The two implementations are new code by the same contributor. They do not +constitute independent scientific review or formal proof-kernel checking. + +New result, proof and implementation produced by Nick Petalas. Apache-2.0. diff --git a/research/p104-respan-stop-obstruction/README.md b/research/p104-respan-stop-obstruction/README.md new file mode 100644 index 0000000000..7268acb89c --- /dev/null +++ b/research/p104-respan-stop-obstruction/README.md @@ -0,0 +1,86 @@ +# One-step helper respanning cannot unlock a single P104 stop deletion + +This package proves a new scoped obstruction for the exact word of +[PR6345](https://github.com/CrocSwap/integer-mult-bounds/pull/6345). +Even if all 42 one-step helpers may change both endpoint subspaces at once, +none of its 2,660 intermediate stops can be deleted while all other epochs +outside those helpers retain their frames and the scalar schedule is fixed. +The count includes 2,654 public stops and six owned stops. + +Every stop has an explicit ADD/COPY contact with another register whose epoch +stays fixed. That contact forces the original intermediate frame to be visited. +[PROOF.md](PROOF.md) states the exact model and proves the implication. +This is a scoped proof with a finite structural certificate. No new kappa is +claimed, and the selected frontier is unchanged. + +This extends PR6345's second Open next question. The predecessor establishes +price-null helper freedom; the new step is an obstruction to using that freedom +alone to remove one stop elsewhere. Existing word legality, native operators, +invoice and supplier assumptions are premises, not review deliverables here. + +Ali Romman's [PR5590](https://github.com/CrocSwap/integer-mult-bounds/pull/5590) +already proves a price floor for the older PR5580 word when every scalar contact +frame is fixed. Here contacts involving freely re-spanned helpers may change +charts. The new certificate finds a contact with a fixed partner at every +candidate stop of the different PR6345 word. The common-chart equality itself +is an inherited rule, not a new general theorem. + +## Reproduce + +From the repository root, with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/p104-respan-stop-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/p104-respan-stop-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-respan-stop-obstruction +``` + +Expected: `PASS_P104_RESPAN_STOP_OBSTRUCTION`, 2,660 stops, 42 free helpers, +ten semantic rejections, two positive toy controls, and +`PASS_REGISTERED_RESEARCH_PACKAGE` from the registered runner. + +Pass `--receipt /absolute/path/outside/checkout/receipt.json` to the direct +verifier to save every contact witness with source and package file hashes. +The verifier generates this receipt; no retained receipt is required. +In a sparse checkout, materialize +`research/p104-frontier-symmetric-ladders` first. + +## Scope + +The helper MOVE positions, scalar operands/order and all non-selected epochs +outside the one-step helpers stay fixed. The merged transport replacing the +selected stop may be placed at any intervening cut. The proof allows arbitrary +new helper endpoint subspaces, including ones absent from the native catalogue. +It rules out this local move before pricing or native synthesis matters. + +Coordinated changes to multiple epochs outside the one-step helper set, +changed scalar schedules, additional transports and other words remain open. +The package does not +classify optimal frame assignments or prove a global price ceiling. The five +inherited framework assumptions remain. Full native, caller, compiler, rounded +execution and all-size replays are outside this obstruction's claim and were +not run. [VALIDATION.md](VALIDATION.md) records checks and implementation bounds. + +## Open next questions + +- Can changing a blocking partner epoch together with the selected stop admit + a legal two-register deletion? Start with one generated contact witness and + trace the partner's other contacts. Full frame legality, productive target + changes and the complete signed bill are unresolved. +- Can moving one helper's unique MOVE across scalar contacts evade the fixed + schedule obstruction without adding paid work? Start with an explicit + reordered scalar program and preserve every arbitrary public input. + Chronology, restoration and full pricing are blockers. + +The structured versions are in [TASK.json](TASK.json). + +## Credit and coordination + +The new obstruction, proof and verifier were produced by Nick Petalas. +The input word, price-null freedom and open question are DreamingOfClouds's +PR6345. Its predecessor is Ali Romman's PR6167 retained-operand construction +over DreamingOfClouds's PR6144/PR6143 and the retained P104/native/caller lineage. +Their source files and credit remain unchanged. No predecessor implementation +is imported or copied into the verifier. All new work is Apache-2.0. + +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19358834). diff --git a/research/p104-respan-stop-obstruction/SOURCES.json b/research/p104-respan-stop-obstruction/SOURCES.json new file mode 100644 index 0000000000..ed6b574c08 --- /dev/null +++ b/research/p104-respan-stop-obstruction/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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" + }, + { + "path": "research/p104-frontier-symmetric-ladders/README.md", + "usage": "input", + "git_blob": "5c8f2af74ba2f44485fb446027c02ef00ccbe666", + "sha256": "7606e0c63a4a958fc0da9aba0a6fcadb947ef4575b846774b824f12e0d16b45a" + }, + { + "path": "research/p104-frontier-symmetric-ladders/WORD.json.gz", + "usage": "input", + "git_blob": "613301460170b30f7185cf1df5b99c767541568a", + "sha256": "b525237058cdb30d358f5332987fa5f72dc966579f55becd1b6702f62829eda8" + }, + { + "path": "research/p104-fixed-contact-ceiling/README.md", + "usage": "provenance", + "git_blob": "1570338984271f48d18084fcd1d1ac1c322565f4", + "sha256": "125cf485ba91fba3d3a87fae503782c95d72b20039adf7f7a7ee753ed72c0c06" + } + ] +} diff --git a/research/p104-respan-stop-obstruction/TASK.json b/research/p104-respan-stop-obstruction/TASK.json new file mode 100644 index 0000000000..fccca732dc --- /dev/null +++ b/research/p104-respan-stop-obstruction/TASK.json @@ -0,0 +1,128 @@ +{ + "schema_version": 1, + "task_id": "scalar-to-moment", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "scalar-to-moment", + "question": "Can a scalar/frame rewrite improve the complete signed moment through paid jobs, productive targets, or both?", + "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", + "docs/research/recursive-invoice-preflight.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": "Require a legal chronological rewrite and favorable complete signed target-minus-paid moment with all extra charges. Unchanged ADD counts or unchanged paid-call counts alone decide neither success nor failure. Compiler, native and outer admission remain separate obligations.", + "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": "Construct one legal source-bound rewrite and compare complete before/after P and T. Charge restoration, source windows and owned helpers. A paid call need not disappear: a legal target split or rank redistribution may win. Stop if the signed moment is unchanged or the consumer repays the gain. Do not extend a scalar-only census on ADD counts.", + "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": [ + "signed moment", + "target split", + "rank exchange", + "scalar rewrite" + ], + "existing_checks": [ + { + "scope": "PR #3998: consecutive A2 scalar contraction", + "evidence": "research/staged544-a2-graph-rewrite/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "389268a6b5e0373a3125d5c6fcd6995f4ea324f5", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4019: separated A2 sites with unchanged recursive histogram", + "evidence": "research/staged544-separated-a2/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "f408e09df300b575235f7f77f81948071397e16d", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4112: composition audit", + "evidence": "research/staged544-a2-composition-audit/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "205b7380656ba4b6316a8a493b1a3c679b8f7a0e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4152: A1858 contraction audit", + "evidence": "research/staged544-a1858-contraction-audit/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "caaa14cde5962adc372fdca71f63d0f29e73c8b2", + "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": "refined", + "actual_scope": "Fixed-contact obstruction to deleting one intermediate stop of the exact PR6345 word, even with simultaneous arbitrary endpoint respanning of all 42 one-step helpers.", + "scope_change_reason": "The user requests original work, not an audit. This answers a bounded version of PR6345's second open question by a new necessary-chart obstruction; no predecessor replay is the deliverable.", + "bottleneck_link": "The current complex supplier needs changed productive/paid moments. This excludes one proposed way of turning price-null helper freedom into a paid-stop improvement and identifies which additional epoch or schedule premise must change.", + "budget_minutes": 60, + "stop_rule": "Ship the first exact obstruction, without expanding to coupled epoch changes or a larger search.", + "outcome": "completed", + "evidence": "PROOF.md proves the fixed-contact lemma. verify.py generates and separately checks all 2660 direct-contact witnesses, including 2654 public and six owned stops, with ten semantic rejections and two positive toy controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a blocking partner epoch change together with the selected stop to admit a legal two-register stop deletion?", + "why_it_matters": "The new obstruction forces a successful continuation to change another non-one-step epoch or leave the fixed-schedule model.", + "first_step": "Take one generated direct-contact witness, jointly change its two epochs and trace every other scalar contact.", + "blocked_by": "Joint frame legality, arbitrary-input restoration, productive debits and the complete signed bill remain unresolved." + }, + { + "question": "Can moving a one-step helper MOVE across scalar contacts enable a profitable stop deletion?", + "why_it_matters": "The obstruction fixes that MOVE position; changing contact incidence is a different mechanism.", + "first_step": "Write one explicit reordered scalar program preserving every independent public input and price all transports.", + "blocked_by": "Chronology, frame compatibility, restoration and complete native/caller pricing remain unresolved." + } + ], + "claim_type": "scoped proof with finite structural certificate", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19358834", + "source_question": { + "pr": 6345, + "author": "DreamingOfClouds", + "question": "Can a re-spanned helper enable a stop drop elsewhere?", + "source_head": "776bd2ecf9cb18a88a0db27e43a2e876856e9fd9" + }, + "freshness": { + "canonical_main": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "checked_at_utc": "2026-11-02T19:32:00Z", + "priority_revision": 8, + "overlap_limitations": "Live open-PR and Discussion snapshots report complete pagination; sparse local overlap notes cover 102 of 8917 HEAD note records. Additional main README and merged PR searches covered respanning, stop drops, price-null and frame assignments. No search covers unpublished work or every code diff." + }, + "predecessor_scope": "PR5590 proves a fixed-contact price floor on the older PR5580 word. Common-chart equality is inherited syntax. The new claim is complete direct-partner anchoring of the PR6345 stop-deletion domain while one-step helper contact charts may vary." +} diff --git a/research/p104-respan-stop-obstruction/VALIDATION.md b/research/p104-respan-stop-obstruction/VALIDATION.md new file mode 100644 index 0000000000..7636d2ea8b --- /dev/null +++ b/research/p104-respan-stop-obstruction/VALIDATION.md @@ -0,0 +1,57 @@ +# Validation and implementation bounds + +The verifier is new standard-library code. It imports no predecessor constructor, +replay engine or optimizer. The input is the exact PR6345 WORD.json.gz already +on main. The source package's mathematical and supplier claims are premises. +The live README pin identifies the question; it is not a proof dependency. + +Direct normal and optimized CPython 3.12.15 runs pass with warnings treated as +errors. They generate 2,660 distinct contact witnesses, including six owned +stops, and identify 42 one-step helpers. The separate streaming checker checks +the exact full candidate set and every contact witness. Ten semantic rejection +controls and two positive toy controls run in both modes. No Python assertion +implements a proof obligation, so optimized mode retains all checks. + +Registered command timings and publication-byte/history checks are recorded in +the PR body. Each registered command has a 120-second timeout. Neither local +checks nor future hosted checks constitute independent scientific acceptance. +The source's full native/caller/compiler/all-size replays are intentionally +outside this local chart obstruction and were not executed. + +## Power of Ten inspection + +The changed code has no recursion or unbounded search. Production inputs have +at most 26,000 events, 1,024 total fields, 2,048 frames and nine basis vectors +per frame. A frame span has at most 512 elements. Every lifetime and epoch is +created by an input event. There are at most 27,024 epochs and 52,000 contact +ends. The bounded controls use fixed-size mutations of the enumerated witness +set. The compressed and expanded word are limited to 16 MiB each. Source hashes +are checked before parsing the frozen word. Metadata and other local package +files are trusted repository inputs, not a general untrusted-data service. + +Every function is under 60 physical lines. Explicit contracts check source +binding, active lifetimes, chart equalities, neighboring subspaces, complete +coverage and witness uniqueness. The certificate checker separately discovers +its candidate set. There is no generated code or dynamic import. File writes +occur only for an explicitly requested receipt outside the checkout, and errors +propagate. Normal and optimized warnings-as-errors runs provide the interpreted +language diagnostics used here; no third-party static analyzer is required. + +Two language/runtime deviations are explicit. + +- Rule 3, fixed allocation. CPython allocates dictionaries, tuples, arbitrary + integers and JSON objects during replay. This is restricted to the finite + input and witness capacities above, with one synchronous execution and no + background tasks. The ten controls copy at most one bounded certificate at + a time. Fixed-capacity storage would require a different runtime; a future + untrusted service must supply a separately reviewed memory budget. +- Rule 9, indirect calls. `reject` invokes one of three explicit local functions + for bounded semantic controls. The target set is `trace`, `certificate` and + `check_certificate`; no external callback or runtime registration is accepted. + The normal and optimized verifier runs execute every target. Production proof + computation uses direct calls. If the controls are moved to a separate test + module, remove this test-only dispatch from the production verifier. + +Receipt hashes bind all package files present when the command executes. A +receipt generated before a documentation edit describes those earlier bytes; +regenerate it after edits when retaining a final publication receipt. diff --git a/research/p104-respan-stop-obstruction/VERIFY.json b/research/p104-respan-stop-obstruction/VERIFY.json new file mode 100644 index 0000000000..1cccb2fef1 --- /dev/null +++ b/research/p104-respan-stop-obstruction/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-frontier-symmetric-ladders/README.md", + "research/p104-frontier-symmetric-ladders/WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Generate all fixed-contact witnesses, independently stream-check the full stop domain, and execute ten semantic rejection and two positive toy controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Generate all fixed-contact witnesses, independently stream-check the full stop domain, and execute ten semantic rejection and two positive toy controls with assertions disabled." + } + ] +} diff --git a/research/p104-respan-stop-obstruction/verify.py b/research/p104-respan-stop-obstruction/verify.py new file mode 100644 index 0000000000..6ca243e60c --- /dev/null +++ b/research/p104-respan-stop-obstruction/verify.py @@ -0,0 +1,262 @@ +"""Certify fixed scalar contacts obstructing one P104 stop deletion. + +New proof and implementation produced by Nick Petalas. Apache-2.0. +Input word and question: DreamingOfClouds PR6345 over Ali Romman's PR6167. +""" + +import argparse +from collections import Counter +import gzip +from hashlib import sha256 +from io import BytesIO +import json +from pathlib import Path +import platform + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +WORD = "research/p104-frontier-symmetric-ladders/WORD.json.gz" +MAX_RAW = 16 * 1024 * 1024 +STATUS = "PASS_P104_RESPAN_STOP_OBSTRUCTION" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def digest(raw): + return sha256(raw).hexdigest() + + +def authenticated_word(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + for row in manifest["files"]: + if row["usage"] == "input": + raw = (ROOT / row["path"]).read_bytes() + need(digest(raw) == row["sha256"], "Source hash: " + row["path"]) + raw = (ROOT / WORD).read_bytes() + need(len(raw) <= MAX_RAW, "Compressed input size") + with gzip.GzipFile(fileobj=BytesIO(raw)) as stream: + payload = stream.read(MAX_RAW + 1) + need(len(payload) <= MAX_RAW, "Expanded input size") + word = json.loads(payload) + need(0 < len(word["program"]) <= 26000, "Event capacity") + need(0 < len(word["initial"]) <= 1024, "Public capacity") + need(len(word["initial"]) + word["owned_fields"] <= 1024, "Field capacity") + need(0 < len(word["frames"]) <= 2048, "Frame capacity") + need(word["public"] == len(word["initial"]), "Public declaration") + return word, digest(raw), digest(payload) + + +def frame_spans(word): + spans = [] + for basis in word["frames"]: + need(len(basis) <= 9, "Ambient dimension") + values = {0} + for vector in basis: + need(type(vector) is int and 0 < vector < 512, "Binary vector range") + need(vector not in values, "Independent frame basis") + values |= {x ^ vector for x in values} + spans.append(frozenset(values)) + return spans + + +def free_helpers(word): + moves = Counter(e[1] for e in word["program"] if e[0] == "MOVE") + main = set(word["live"]) | {r + 112 for r in word["live"]} + return {r for r in range(len(word["initial"])) + if r not in main and moves[r] == 1} + + +def trace(word): + """Index constant-frame epochs, keeping owned lives separate.""" + public = len(word["initial"]) + lives = Counter() + chains = {(r, 0): [f] for r, f in enumerate(word["initial"])} + active = {r: (r, 0, 0) for r in range(public)} + contacts = [] + for index, event in enumerate(word["program"]): + op, r = event[:2] + if op == "INIT": + need(r >= public and r not in active, "Fresh owned life") + lives[r] += 1 + chains[r, lives[r]] = [event[2]] + active[r] = (r, lives[r], 0) + continue + need(r in active, "Active destination") + key = active[r] + chain = chains[key[:2]] + if op == "MOVE": + need(chain[-1] == event[2], "MOVE source frame") + need(event[4] == int(r >= public), "MOVE ownership") + active[r] = (r, lives[r], len(chain)) + chain.append(event[3]) + elif op == "CLEAR": + need(r >= public and chain[-1] == event[2], "Owned exit") + del active[r] + else: + need(op in ("ADD", "COPY", "SCALE"), "Scalar opcode") + need(chain[-1] == event[-1], "Scalar destination chart") + if op in ("ADD", "COPY"): + s = event[2] + need(s != r and s in active, "Active scalar source") + partner = active[s] + need(chains[partner[:2]][-1] == event[-1], "Common scalar chart") + contacts.append((index, key, partner)) + need(set(active) == set(range(public)), "Completed owned lives") + need([chains[r, 0][-1] for r in range(public)] == word["final"], + "Final frame declarations") + return chains, contacts + + +def stop_domain(word, chains): + spans = frame_spans(word) + stops = set() + for (r, life), chain in chains.items(): + for k in range(1, len(chain) - 1): + before, middle, after = (spans[f] for f in chain[k - 1:k + 2]) + ordered = before < middle < after if r < len(word["initial"]) \ + else after < middle < before + need(ordered, "Strict neighboring stop subspaces") + stops.add((r, life, k)) + return stops + + +def certificate(word): + chains, contacts = trace(word) + stops = stop_domain(word, chains) + free = free_helpers(word) + anchors = {} + for index, a, b in contacts: + for stop, partner in ((a, b), (b, a)): + if stop in stops and partner[0] not in free: + anchors.setdefault(stop, (index, partner)) + need(set(anchors) == stops, "Unanchored intermediate stop") + return [list(stop) + [anchors[stop][0]] + list(anchors[stop][1]) + for stop in sorted(stops)] + + +def check_certificate(word, records): + """Separate streaming checker; no primary trace or domain is used.""" + public = len(word["initial"]) + totals = [0] * (public + word["owned_fields"]) + for event in word["program"]: + if event[0] == "MOVE": + totals[event[1]] += 1 + mains = set(word["live"] + [r + 112 for r in word["live"]]) + free = {r for r in range(public) if r not in mains and totals[r] == 1} + requested, declared = {}, set() + for row in records: + need(len(row) == 7, "Witness arity") + stop = tuple(row[:3]) + need(stop not in declared, "Duplicate stop witness") + declared.add(stop) + requested.setdefault(row[3], []).append(row) + lives = [0] * len(totals) + ordinal = [0] * len(totals) + current = dict(enumerate(word["initial"])) + candidates, checked = set(), set() + for index, event in enumerate(word["program"]): + op, r = event[:2] + if op == "INIT": + lives[r] += 1 + ordinal[r] = 0 + current[r] = event[2] + elif op == "MOVE": + if ordinal[r] > 0: + candidates.add((r, lives[r], ordinal[r])) + ordinal[r] += 1 + current[r] = event[3] + elif op == "CLEAR": + del current[r] + for row in requested.get(index, []): + need(op in ("ADD", "COPY"), "Witness must be a contact") + s = event[2] + ends = ((r, lives[r], ordinal[r]), (s, lives[s], ordinal[s])) + stop, partner = tuple(row[:3]), tuple(row[4:]) + need((stop, partner) in (ends, ends[::-1]), "Actual contact epochs") + need(partner[0] not in free, "Partner must be fixed") + need(current[r] == current[s] == event[-1], "Actual common chart") + checked.add(stop) + need(declared == candidates == checked, "Complete exact stop coverage") + return dict(stops=len(candidates), + public_stops=sum(r < public for r, _, _ in candidates), + owned_stops=sum(r >= public for r, _, _ in candidates), + free_helpers=sorted(free)) + + +def reject(call, *args): + try: + call(*args) + except ValueError: + return 1 + raise ValueError("Semantic control was accepted") + + +def toy(anchored): + program = [["MOVE", 0, 0, 1, 0], ["ADD", 0, 1, "1", 1]] + if anchored: + program.append(["ADD", 0, 2, "1", 1]) + program += [["MOVE", 0, 1, 2, 0], ["MOVE", 1, 1, 2, 0]] + return dict(frames=[[], [1], [1, 2]], initial=[0, 1, 1], + final=[2, 2, 1], public=3, owned_fields=0, live=[], + program=program) + + +def controls(word, records): + checks = reject(check_certificate, word, records[:-1]) + checks += reject(check_certificate, word, records + [records[0]]) + for column, value in ((0, -1), (2, -1), (3, -1), (4, -1), (6, -1)): + mutant = [list(row) for row in records] + mutant[0][column] = value + checks += reject(check_certificate, word, mutant) + mutant = [list(row) for row in records] + mutant[0][4:] = [min(free_helpers(word)), 0, 0] + checks += reject(check_certificate, word, mutant) + anchored = toy(True) + need(check_certificate(anchored, certificate(anchored))["stops"] == 1, + "Anchored toy positive control") + checks += reject(certificate, toy(False)) + collapsed = toy(False) + collapsed["initial"][1] = 0 + collapsed["program"] = [["ADD", 0, 1, "1", 0], + ["MOVE", 0, 0, 2, 0], ["MOVE", 1, 0, 2, 0]] + need(check_certificate(collapsed, certificate(collapsed))["stops"] == 0, + "Unanchored toy admits helper respanning and stop removal") + blocked = toy(True) + blocked["initial"][1] = 0 + blocked["program"] = collapsed["program"][:1] + \ + [["ADD", 0, 2, "1", 0]] + collapsed["program"][1:] + checks += reject(trace, blocked) + return checks + + +def run(receipt_path): + word, compressed_hash, payload_hash = authenticated_word() + records = certificate(word) + result = check_certificate(word, records) + need((result["stops"], result["public_stops"], result["owned_stops"], + len(result["free_helpers"])) == (2660, 2654, 6, 42), "Frozen question domain") + checks = controls(word, records) + need(checks == 10, "Complete rejection control count") + result.update(status=STATUS, claim_type="scoped proof with finite certificate", + semantic_rejections=checks, positive_toy_controls=2, + source_sha256=compressed_hash, payload_sha256=payload_hash, + events=len(word["program"]), python=platform.python_version(), + witness_sha256=digest(json.dumps(records).encode())) + if receipt_path is not None: + output = receipt_path.resolve() + need(not output.is_relative_to(ROOT), "Receipt must be outside checkout") + hashes = {p.name: digest(p.read_bytes()) for p in sorted(HERE.iterdir()) + if p.is_file()} + receipt = dict(result, package_sha256=hashes, anchors=records) + output.write_text(json.dumps(receipt, sort_keys=True, indent=2) + "\n") + print(json.dumps(result, sort_keys=True)) + return result + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path) + run(parser.parse_args().receipt)