From a3df7015a9571752430314afdaf5212704b2f5dc Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Fri, 30 Oct 2026 13:40:04 +0000 Subject: [PATCH] Record that selected MOVE absolute phases scale as i^{p f} On the #6030 word, each MOVE chart change has global phase i^p, and the column-multiplicity operator carries i^{p f}. 1809 of 2886 operators have p not 0, including 78 endpoint pairs absent from the #5599 all-width certificate. Co-authored-by: unpaidmoon --- research/move-chart-phase-power/PROOF.md | 78 +++++++ research/move-chart-phase-power/README.md | 74 +++++++ research/move-chart-phase-power/SOURCES.json | 42 ++++ research/move-chart-phase-power/TASK.json | 89 ++++++++ research/move-chart-phase-power/VERIFY.json | 23 +++ research/move-chart-phase-power/verify.py | 205 +++++++++++++++++++ 6 files changed, 511 insertions(+) create mode 100644 research/move-chart-phase-power/PROOF.md create mode 100644 research/move-chart-phase-power/README.md create mode 100644 research/move-chart-phase-power/SOURCES.json create mode 100644 research/move-chart-phase-power/TASK.json create mode 100644 research/move-chart-phase-power/VERIFY.json create mode 100644 research/move-chart-phase-power/verify.py diff --git a/research/move-chart-phase-power/PROOF.md b/research/move-chart-phase-power/PROOF.md new file mode 100644 index 0000000000..59358df2f1 --- /dev/null +++ b/research/move-chart-phase-power/PROOF.md @@ -0,0 +1,78 @@ +# MOVE absolute phase on the selected word is i^{p f} + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. +No new κ. Assumption ID: `native_all_columns`. This is one implication, not that assumption and not the other four. + +## 1. Proposition + +Let the selected word be `research/p104-helper470-twin-rung-removal/WORD.json.gz` on canonical main `2485805a6d47f36ea83ddde6327d453ac82d44dc` (PR #6030, κ = 781451/250000000). Its schema is `p104-accumulated-block-composition/2`. Each register carries a chart index. At column multiplicity `f ≥ 1` the physical operator of a width-1 Clifford `U` on `(C^2)^{⊗9}` is the tensor power `U^{(⊗)f}` on `f` consecutive 9-qubit blocks. + +A `MOVE` from frame `a` to frame `b` denotes + +```text +U = chart(a)^† chart(b), +``` + +where `chart(i)` is `canonical_frame(9, frames[i])` from `research/p104-native-channel/vendor/clifford_exact.py`. `lower_child(U)` splits `U` into monomial factors. `native_verify.recipe` turns those factors into a circuit. On this word every such circuit has left monomial phase `0`, and the right monomial contributes a single nontrivial residue `p ∈ {0,1,2,3}` together with a harmless `('phase', 0)` gate from the left factor. The global phase of `U` is `i^p`. + +**Proposition.** For every integer `f ≥ 1`, + +```text +U^{(⊗)f} = i^{p f} U_0^{(⊗)f}, +``` + +where `U_0` is `U` with its global phase gates removed. The equality `i^{p f} = i^p` holds for every `f ≥ 1` if and only if `p = 0`. The selected word has 1,809 distinct MOVE operators, and 2,117 MOVE events, with `p ≠ 0`. + +The identity `i^{p f}` is the global-phase case of the monomial lift already written for the older #5599 word in `research/p104-allwidth-native-certificate/PROOF.md` (`i^{p f + Σ_j q(x_j)}`). That certificate's pair set is not this word's pair set. The census below is the binding for the selected caller. + +## 2. Lemmas + +**Lemma A (global phase).** A gate `('phase', p)` multiplies every amplitude by `i^p` and commutes with every gate in the circuit. Therefore `U = i^p U_0`. + +*Proof.* `clifford_exact.Op.zero_state` and `native_verify.state` both apply that gate by `mul_i` / `rotate` on every stored amplitude, with no address change. A scalar multiple of the identity commutes with every linear map, so the gates may be collected at the front. `monomial` appends the phase only after a phase-free tableau representative, and `lower_child` preserves the operator, including `zero_state`. ∎ + +**Lemma B (tensor power).** For every integer `f ≥ 1`, `U^{(⊗)f} = i^{p f} U_0^{(⊗)f}`. + +*Proof.* For a scalar `c` and a linear map `A`, `(c A)^{(⊗)f} = c^f A^{(⊗)f}`. Take `c = i^p` and `A = U_0`. ∎ + +**Lemma C (the width-1 integer is not invariant).** `i^{p f} = i^p` for every integer `f ≥ 1` if and only if `p ≡ 0 (mod 4)`. + +*Proof.* The case `f = 2` says `2p ≡ p (mod 4)`, hence `p ≡ 0 (mod 4)`. If `p ≡ 0 (mod 4)`, then `i^{p f} = 1 = i^p` for every `f`. The residues recorded by this compiler lie in `{0,1,2,3}`, so the condition is `p = 0`. ∎ + +The three nontrivial residues already fail at width 2: + +| `p` | width-1 factor | width-2 factor | +|---:|---|---| +| 1 | `i` | `i^2 = -1` | +| 2 | `-1` | `i^4 = 1` | +| 3 | `-i` | `i^6 = -1` | + +## 3. Binding to the selected caller + +`verify.py` walks every event. A `MOVE` is accepted only when its source frame is the role's current chart, its private flag matches owned-slot membership, and the frame span strictly shrinks (private) or grows (public). The walk ends on the declared public exit charts. It counts 3,453 `MOVE`s and 18,404 `ADD`s. A source-frame edit and a reversed public nesting are rejected. + +`lower_child` on the 2,886 distinct endpoint pairs, cached per chart, gives: + +| `p` | distinct pairs | events | +|---:|---:|---:| +| 0 | 1077 | 1336 | +| 1 | 994 | 1255 | +| 2 | 239 | 246 | +| 3 | 576 | 616 | +| total | 2886 | 3453 | + +For every pair the left phase is 0, the child rank equals the absolute frame-length gap, and the sum of the recipe's phase gates equals `p`. One operator of each residue is compared in `native_verify.state`: deleting the phase gates and rotating the phase-free image by `p` reproduces the original state, and rotating by `p+1` does not. Those four states are controls for Lemma A. Lemmas B and C are the identities above; they do not depend on a finite width sample. + +The #5599 word at `research/p104-helper-subspace-splits/WORD.json.gz` has 3,447 `MOVE`s and 2,887 endpoint pairs. It shares 2,808 pairs with the selected word, leaves 79 pairs behind, and misses 78 pairs that the selected word uses. Those 78 pairs have phase counts 23, 17, 20, 18 and occur as 103 events (42, 18, 24, 19). #5974's dense certificate names the #5599 pairs, including the payload hash of that word's recipes. It does not name these 78 operators. + +## 4. What remains + +Per-column execution of the width-1 circuit, phase gate included on each column, is exactly `U^{(⊗)f}`. Lemma B says that implementation is consistent. The false reading is that the integer `p` stored for width 1 is itself the joint phase at every multiplicity. + +This does not re-prove the width-1 identity between `U` and the frame formula `adjoint(frame(a)) + frame(b)`. The selected review already records that the primary checked signed native maps and absolute phases at width 1. That check is not an all-width theorem. Spectators, whole-job adapters and fixed-tape tariffs stay open. + +`owned_erasure`, `compiler`, `precision_tape` and `analytic_recovery` are untouched. #5625 (CRT row reentry) and #5707 (root-prefix lowering) are partial interfaces of other callers. #5837 lifts `SCALE` / `ADD` / `COPY` on the #5599 word. #5974 (`research/p104-allwidth-native-certificate`) certifies factorwise tensor lift, including absolute phase, for that same #5599 word and shows one termwise closed form that does not lift. #5442 is the group-algebra lift for the older #5413 caller. None of those three is a census of this #6030 word. No outer row, admitted BIT budget or selected κ changes. + +## 5. Downstream effect + +An all-width certificate that copies the width-1 phase integer into one joint recipe, without replacing `p` by `p f (mod 4)`, mis-signs every nontrivial `MOVE` at width 2. A correct certificate tensors the width-1 operator, or raises each global phase in that way. The 1,336 phase-zero events are the only `MOVE`s on this word for which the two readings agree at every positive multiplicity. diff --git a/research/move-chart-phase-power/README.md b/research/move-chart-phase-power/README.md new file mode 100644 index 0000000000..fae5789268 --- /dev/null +++ b/research/move-chart-phase-power/README.md @@ -0,0 +1,74 @@ +# MOVE absolute phase on the selected word scales as i^{p f} + +**Scoped partial result; no new κ.** Assumption ID `native_all_columns`, one implication. The selected conditional exponent stays κ = 781451/250000000. + +On the selected #6030 word, a `MOVE` from frame `a` to frame `b` is the width-1 operator `U = chart(a)^† chart(b)`. Its global phase is `i^p` with `p ∈ {0,1,2,3}`. At column multiplicity `f ≥ 1`, + +```text +U^{(⊗)f} = i^{p f} U_0^{(⊗)f}. +``` + +That joint phase equals the width-1 factor `i^p` for every `f ≥ 1` exactly when `p = 0`. Exhaustive compilation of this word gives 1,077 phase-zero operators (1,336 events) and 1,809 operators with `p ≠ 0` (2,117 events). Width 2 already separates the two readings: `i^{2} = -1`, `i^{4} = 1`, and `i^{6} = -1`. + +Per-column execution of the width-1 circuit is the tensor power, so it is consistent with the identity. The obstructed reading is a joint recipe that copies the width-1 phase integer unchanged. + +#5974 already records the factor `i^{p f}` for monomials of the older #5599 word. That word has 3,447 `MOVE`s and 2,887 endpoint pairs. The selected word shares 2,808 of those pairs, drops 79, and adds 78. The added pairs have phases 23 / 17 / 20 / 18 and occur as 103 events. #5974's payload hash does not cover them. + +This is not a paid-profile change, a κ improvement, or a discharge of `native_all_columns`. + +## Scope and evidence + +Original card: `uniform-transfer-audit`. Scope status: **refined**. The card asks for one assumption and one quantified implication at the actual caller. The implication is Lemma B of [PROOF.md](PROOF.md), bound to `research/p104-helper470-twin-rung-removal/WORD.json.gz`. + +| `p` | distinct pairs | events | +|---:|---:|---:| +| 0 | 1077 | 1336 | +| 1 | 994 | 1255 | +| 2 | 239 | 246 | +| 3 | 576 | 616 | + +The chart walk accepts 3,453 `MOVE`s only along recorded frames. A wrong source frame and a non-nested destination are rejected. One operator of each residue matches `native_verify.state` after a global rotation by `p`, and fails after a rotation by `p+1`. + +Pins are in [SOURCES.json](SOURCES.json). The catalogue and selected record are provenance at `2485805a6d47f36ea83ddde6327d453ac82d44dc`. + +## Reproduce + +```sh +python3 -B research/move-chart-phase-power/verify.py +python3 -B scripts/research_package.py --package research/move-chart-phase-power +``` + +Observed marker: + +```text +PASS_MOVE_CHART_PHASE_POWER pairs=2886 events=3453 phase0_pairs=1077 phase0_events=1336 nontrivial_pairs=1809 nontrivial_events=2117 only_new_pairs=78 only_new_events=103 +``` + +The Clifford census takes about two minutes on CPython 3.12. Lemmas B and C are the written argument. The four state comparisons are controls, not a substitute for those lemmas. + +Not run: the #6030 primary native replay, `make` frontier verification, Lean, and Docker. + +## Credit + +DreamingOfClouds supplied the selected #6030 word. Ali Romman supplied the #5599 word used as the predecessor pair set. The chart compiler is the retained `clifford_exact.py` / `native_verify.py` native channel. #5837 (unpaidmoon) lifted `SCALE`, `ADD` and `COPY` on that #5599 word. #5974 (Mark / Matarener) certifies factorwise all-width lift for the #5599 native layer, including the monomial factor `i^{p f}`. #5442 (Mark / Matarener) is the group-algebra lift for the older #5413 caller. The selected review is Douglas Colkitt's `docs/research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md`. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. + +## Open next questions + +Does any joint recipe in the #6030 primary copy a nontrivial width-1 phase integer `p` instead of `p f`? The first step is to compare one lowered recipe with `p ≠ 0` against the `f`-column operator. The primary payload is not a live input here. + +Separately, does the predecessor #5907 word, which has 3,454 `MOVE`s, carry the same phase histogram? The first step is the same census on `research/p104-helper470-twin-rung-removal/inputs/pr5907-WORD.json.gz`. + +## Ordered eligible list + +Session r62, item 5. Recent #1166 comments in the fetched window are claims and released results, not an open request for this implication. The 19 October handoff index is already delivered or closed by later work, including unpaidmoon #4123/#4127 on the typed actual-width handoff. The revision-8 "Next bounded decisions" table then orders the open rows: + +1. Complex helpers (`p104-side-correction`, `coverage-law-change`) +2. BIT `bit-helper-contract` +3. New decoders and interfaces +4. Supplier audit (`#5717` / `#5719`, with `#5718` left uncovered) +5. All-size assumption formalization — this item +6. Verification tooling + +#5837 already proved the scalar half of `native_all_columns` for the older #5599 word. This item stays open for a different implication on the current selected caller. Rows 1–4 and 6 were left to the other sessions. Catalogue cards after the table were not reached. diff --git a/research/move-chart-phase-power/SOURCES.json b/research/move-chart-phase-power/SOURCES.json new file mode 100644 index 0000000000..39a704f984 --- /dev/null +++ b/research/move-chart-phase-power/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "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-helper-subspace-splits/WORD.json.gz", + "usage": "input", + "git_blob": "e325091e3051afe37a2d9c82f85afe9028510edb", + "sha256": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099" + }, + { + "path": "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "usage": "input", + "git_blob": "22f9ab02d1b73ea0aa4b07ce445a14cc2602c760", + "sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f" + }, + { + "path": "research/p104-native-channel/vendor/clifford_exact.py", + "usage": "input", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + }, + { + "path": "research/p104-native-channel/vendor/native_verify.py", + "usage": "input", + "git_blob": "2c209dfa9cfade3bc20ac5fc9d876b433a147f8c", + "sha256": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38" + } + ] +} diff --git a/research/move-chart-phase-power/TASK.json b/research/move-chart-phase-power/TASK.json new file mode 100644 index 0000000000..da90738629 --- /dev/null +++ b/research/move-chart-phase-power/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "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" + ], + "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": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "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": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "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": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "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": "On the selected #6030 word, the absolute phase of each MOVE chart change U=chart(a)^\u2020 chart(b) satisfies U^{(\u2297)f}=i^{p f} U_0^{(\u2297)f}, and i^{p f}=i^p for every column multiplicity f\u22651 if and only if p=0. 1809 of 2886 distinct MOVE operators have p\u22600.", + "scope_change_reason": "The card asks for one assumption ID and one quantified implication at the actual caller. The assumption is native_all_columns. The implication is the tensor-power phase of MOVE, not a discharge of all five assumptions. #5837 already lifted SCALE/ADD/COPY on the older #5599 word; this word is the selected #6030 program.", + "bottleneck_link": "Side result; no new kappa. An all-width reading of native_all_columns that keeps the width-1 phase integer mis-signs 2117 MOVE events at width 2. The corrected phase is i^{p f}. The other four assumptions and the selected exponent stay in place.", + "budget_minutes": 60, + "stop_rule": "Stop after this phase law and the exhaustive census of the selected word's MOVE operators. Do not rerun the width-1 native replay or search for a new helper split.", + "outcome": "partial", + "evidence": "PROOF.md Lemmas A-C. verify.py prints PASS_MOVE_CHART_PHASE_POWER with nontrivial_pairs=1809, nontrivial_events=2117, only_new_pairs=78 and only_new_events=103.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance.", + "open_questions": [ + { + "question": "Which of the 2117 nontrivial MOVE events on this word have a width-1 phase that the primary's signed-map check recorded, and does any joint recipe in that check copy p rather than p*f?", + "why_it_matters": "Lemma B is harmless for per-column execution. It bites only a certificate that reuses the width-1 phase integer on the joint system.", + "first_step": "Locate one lowered recipe in the #6030 primary whose phase gate is p\u22600 and compare it with the f-column operator, without rerunning the full native replay.", + "blocked_by": "The primary's recipe payload is not pinned as a live input of this package." + }, + { + "question": "Does the predecessor #5907 word have the same right-monomial phase histogram on its 3454 MOVE events?", + "why_it_matters": "The helper-470 edit removes one MOVE. A changed phase would be an edit effect; an unchanged histogram would say the obstruction already sat on the previous selected word.", + "first_step": "Run the same lower_child census on research/p104-helper470-twin-rung-removal/inputs/pr5907-WORD.json.gz.", + "blocked_by": "None. It is a different caller and was left out of this census." + } + ] +} diff --git a/research/move-chart-phase-power/VERIFY.json b/research/move-chart-phase-power/VERIFY.json new file mode 100644 index 0000000000..17018141db --- /dev/null +++ b/research/move-chart-phase-power/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper-subspace-splits/WORD.json.gz", + "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "research/p104-native-channel/vendor/clifford_exact.py", + "research/p104-native-channel/vendor/native_verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 400, + "checks": "SHA256 of the selected #6030 word and of the #5599 word; chart walk of all 3453 MOVE events with recorded frames, ownership flags and strict span nesting; rejection of a wrong source frame and of a non-nested destination; lower_child phase census of all 2886 distinct operators (left phase 0, right phase histogram 1077/994/239/576, event histogram 1336/1255/246/616, rank equal to the frame-length gap); 78 endpoint pairs absent from the #5599 word, with phase histogram 23/17/20/18 and 103 events; one state-rotation control per residue and an off-by-one failure; width-2 witness that p*2 ≡ p (mod 4) exactly for p=0." + } + ] +} diff --git a/research/move-chart-phase-power/verify.py b/research/move-chart-phase-power/verify.py new file mode 100644 index 0000000000..f503669a7f --- /dev/null +++ b/research/move-chart-phase-power/verify.py @@ -0,0 +1,205 @@ +#!/usr/bin/env python3 +"""Absolute phase of selected MOVE chart changes scales as i^{p f}. + +The all-width statement is Lemma 2 in PROOF.md. This program binds it to the +selected #6030 word and checks the phase gates on that word's own operators. +""" + +from collections import Counter +from hashlib import sha256 +import gzip +import importlib.util +import json +import sys +from pathlib import Path + + +ROOT = Path(__file__).resolve().parents[2] +WORD = ROOT / "research/p104-helper470-twin-rung-removal/WORD.json.gz" +PREVIOUS = ROOT / "research/p104-helper-subspace-splits/WORD.json.gz" +CLIFFORD = ROOT / "research/p104-native-channel/vendor/clifford_exact.py" +NATIVE = ROOT / "research/p104-native-channel/vendor/native_verify.py" +WORD_SHA256 = "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f" +PREVIOUS_SHA256 = "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099" +PAIR_PHASE = {0: 1077, 1: 994, 2: 239, 3: 576} +EVENT_PHASE = {0: 1336, 1: 1255, 2: 246, 3: 616} +ONLY_NEW_PAIRS = {0: 23, 1: 17, 2: 20, 3: 18} +ONLY_NEW_EVENTS = {0: 42, 1: 18, 2: 24, 3: 19} + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def load(path, name): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def span(basis): + out = {0} + for value in basis: + need(type(value) is int and 0 < value < 512 and value not in out, "Independent frame vector") + out |= {point ^ value for point in tuple(out)} + return frozenset(out) + + +def walk(word): + """Chart transport of the selected word. Returns MOVE endpoint pairs.""" + public = word["public"] + owned = word["owned_fields"] + need(word.get("schema") == "p104-accumulated-block-composition/2", "Selected word schema") + need(public == 770 and owned == 29, "Selected inventory") + need(len(word["initial"]) == len(word["final"]) == public, "Public boundary") + frames = [span(row) for row in word["frames"]] + current = list(word["initial"]) + [None] * owned + live = set() + moves = [] + counts = Counter() + for event in word["program"]: + need(isinstance(event, list) and event, "Event shape") + op, role = event[0], event[1] + need(op in ("MOVE", "INIT", "CLEAR", "ADD", "SCALE", "COPY"), "Opcode") + need(isinstance(role, int) and 0 <= role < public + owned, "Role") + counts[op] += 1 + if op == "MOVE": + need(len(event) == 5 and type(event[4]) is bool, "MOVE shape") + source, destination, private = event[2], event[3], event[4] + need(current[role] == source, "MOVE leaves the recorded chart") + need((role in live) is private, "MOVE ownership flag") + need(0 <= source < len(frames) and 0 <= destination < len(frames), "Frame index") + if private: + need(frames[destination] < frames[source], "Private transport shrinks the chart") + else: + need(frames[source] < frames[destination], "Public transport enlarges the chart") + current[role] = destination + moves.append((source, destination, abs(len(word["frames"][destination]) - len(word["frames"][source])))) + elif op == "INIT": + need(len(event) == 3 and role >= public and role not in live, "INIT") + live.add(role) + current[role] = event[2] + elif op == "CLEAR": + need(len(event) == 3 and role in live and current[role] == event[2], "CLEAR") + live.remove(role) + current[role] = None + else: + frame = event[-1] + need(current[role] == frame, "Scalar destination chart") + if op != "SCALE": + source = event[2] + need(isinstance(source, int) and source != role, "Scalar source") + need(current[source] == frame, "Common scalar chart") + need(not live and current[:public] == word["final"], "Public exit charts") + need(counts["MOVE"] == 3453 and counts["ADD"] == 18404, "Selected opcode counts") + return moves + + +def reject(word, mutate): + trial = json.loads(json.dumps(word)) + mutate(trial) + try: + walk(trial) + except ValueError: + return + raise ValueError("Mutated word was accepted") + + +def rotate_state(native, state, power): + value, denominator = state + return {addr: native.rotate(pair, power) for addr, pair in value.items()}, denominator + + +def move_pairs(word): + pairs = [] + for event in word["program"]: + if event[0] != "MOVE": + continue + need(len(event) == 5, "MOVE shape") + pairs.append((event[2], event[3])) + return pairs + + +def main(): + raw = WORD.read_bytes() + need(sha256(raw).hexdigest() == WORD_SHA256, "Selected word bytes") + previous_raw = PREVIOUS.read_bytes() + need(sha256(previous_raw).hexdigest() == PREVIOUS_SHA256, "PR5599 word bytes") + word = json.loads(gzip.decompress(raw)) + previous = json.loads(gzip.decompress(previous_raw)) + need(previous.get("schema") == "p104-productive-source/1", "PR5599 schema") + moves = walk(word) + previous_pairs = move_pairs(previous) + need(len(previous_pairs) == 3447, "PR5599 MOVE count") + first_move = next(i for i, event in enumerate(word["program"]) if event[0] == "MOVE") + + def bad_source(trial): + trial["program"][first_move][2] = (trial["program"][first_move][2] + 1) % len(trial["frames"]) + + def bad_nesting(trial): + # Keep the recorded source chart and destroy strict span nesting. + trial["program"][first_move][3] = trial["program"][first_move][2] + + reject(word, bad_source) + reject(word, bad_nesting) + + clifford = load(CLIFFORD, "move_phase_clifford") + native = load(NATIVE, "move_phase_native") + used = {frame for source, destination, _rank in moves for frame in (source, destination)} + charts = {i: clifford.canonical_frame(9, tuple(word["frames"][i])) for i in used} + pair_phase = {} + samples = {} + for source, destination, rank in moves: + key = (source, destination) + if key in pair_phase: + need(pair_phase[key][0] == rank, "Repeated MOVE rank") + continue + record, _compiled = clifford.lower_child(charts[source].adjoint().then(charts[destination])) + recipe = native.recipe(record) + gates = [gate[1] for gate in recipe if gate[0] == "phase"] + right = 0 if record["right"] is None else record["right"]["phase"] + phase = sum(gates) % 4 + need(record["left"]["phase"] == 0 and right == phase and record["rank"] == rank, "Phase and rank") + need(phase in PAIR_PHASE, "Phase residue") + pair_phase[key] = (rank, phase, recipe) + samples.setdefault(phase, (source, destination, recipe)) + need(len(pair_phase) == 2886, "Distinct MOVE operators") + pairs = Counter(phase for _rank, phase, _recipe in pair_phase.values()) + events = Counter(pair_phase[(source, destination)][1] for source, destination, _rank in moves) + need(dict(pairs) == PAIR_PHASE and dict(events) == EVENT_PHASE, "Phase census") + selected_pairs = set(pair_phase) + earlier_pairs = set(previous_pairs) + only_new = selected_pairs - earlier_pairs + need(len(earlier_pairs) == 2887 and len(only_new) == 78, "Certificate pair gap") + need(len(earlier_pairs - selected_pairs) == 79 and len(earlier_pairs & selected_pairs) == 2808, "Shared charts") + only_new_pairs = Counter(pair_phase[key][1] for key in only_new) + only_new_events = Counter( + pair_phase[(source, destination)][1] + for source, destination, _rank in moves + if (source, destination) in only_new + ) + need(dict(only_new_pairs) == ONLY_NEW_PAIRS and dict(only_new_events) == ONLY_NEW_EVENTS, "New-pair phases") + for phase, (source, destination, recipe) in samples.items(): + stripped = tuple(gate for gate in recipe if gate[0] != "phase") + full = native.state(recipe) + free = native.state(stripped) + need(rotate_state(native, free, phase) == full, "Global phase gate") + need(rotate_state(native, free, (phase + 1) % 4) != full, "Off-by-one phase") + need(((2 * phase) % 4 == phase) is (phase == 0), "Width-2 phase witness") + need(source != destination, "Sample endpoints") + nontrivial_pairs = sum(count for phase, count in PAIR_PHASE.items() if phase) + nontrivial_events = sum(count for phase, count in EVENT_PHASE.items() if phase) + print( + "PASS_MOVE_CHART_PHASE_POWER" + f" pairs={len(pair_phase)} events={len(moves)}" + f" phase0_pairs={PAIR_PHASE[0]} phase0_events={EVENT_PHASE[0]}" + f" nontrivial_pairs={nontrivial_pairs} nontrivial_events={nontrivial_events}" + f" only_new_pairs=78 only_new_events=103" + ) + + +if __name__ == "__main__": + main()