diff --git a/.github/workflows/p104-native-channel.yml b/.github/workflows/p104-native-channel.yml new file mode 100644 index 0000000000..b3c64ed80f --- /dev/null +++ b/.github/workflows/p104-native-channel.yml @@ -0,0 +1,42 @@ +name: P104 exact native low-rank channel + +on: + pull_request: + paths: + - research/p104-native-channel/** + - .github/workflows/p104-native-channel.yml + push: + branches: + - codex/p104-native-channel-20261014 + paths: + - research/p104-native-channel/** + - .github/workflows/p104-native-channel.yml + workflow_dispatch: + +permissions: + contents: read + +jobs: + verify: + runs-on: ubuntu-latest + timeout-minutes: 8 + strategy: + fail-fast: false + matrix: + python: ['3.11', '3.12', '3.14'] + steps: + - uses: actions/checkout@v4 + with: + fetch-depth: 0 + - uses: actions/setup-python@v5 + with: + python-version: ${{ matrix.python }} + - name: Validate registered package metadata + run: python scripts/research_package.py --package research/p104-native-channel --check-only + - name: Independent native replay and complete regeneration + run: python -I -O -B research/p104-native-channel/verify.py --regenerate --out "$RUNNER_TEMP/native-channel.json" + - uses: actions/upload-artifact@v4 + with: + name: p104-native-channel-${{ matrix.python }} + path: ${{ runner.temp }}/native-channel.json + if-no-files-found: error diff --git a/research/p104-native-channel/EXPECTED.json b/research/p104-native-channel/EXPECTED.json new file mode 100644 index 0000000000..c7c818d402 --- /dev/null +++ b/research/p104-native-channel/EXPECTED.json @@ -0,0 +1,35 @@ +{ + "all_physical_pairings": 14400, + "all_private_copy_gaussian_columns": 4096, + "controls": { + "global_phase": true, + "missing_final_query_cleanup": true, + "missing_initial_query_compensation": true, + "missing_transport": true, + "physical_label": true + }, + "formal_boundary_columns": 280, + "intrinsic_endpoint_adapters": 208, + "paid_profile": { + "1": 1074, + "2": 58, + "3": 86, + "4": 104, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "rank_mass": 2368, + "recipes_raw_sha256": "0aa152945ffe3797e8295cd17d4ec6646ba24a93372ec35b16c0b164d9858529", + "scalar_events": { + "add": 2624, + "copy": 8, + "erase": 8, + "zero": 8 + }, + "scope": "Concrete finite Clifford primitives plus a complete framed induction over all 280 arbitrary channel inputs, source gathering and 72 dirty helper restorations. No I-G/2 side correction, global helper assignment, precision, all-size admission or new kappa.", + "source_witness_sha256": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e", + "status": "PASS_CONCRETE_NATIVE_P104_LOW_RANK_CHANNEL", + "transports": 740 +} diff --git a/research/p104-native-channel/NATIVE-RECIPES.json.gz b/research/p104-native-channel/NATIVE-RECIPES.json.gz new file mode 100644 index 0000000000..ab129678c2 Binary files /dev/null and b/research/p104-native-channel/NATIVE-RECIPES.json.gz differ diff --git a/research/p104-native-channel/PROOF.md b/research/p104-native-channel/PROOF.md new file mode 100644 index 0000000000..a69311b74f --- /dev/null +++ b/research/p104-native-channel/PROOF.md @@ -0,0 +1,100 @@ +# Finite native realization and its boundary + +## 1. Physical labels + +Reconstruct the 120 root lines from doubled integer E8 coordinates. Write +`B[i,j] = (+1) mod 2`. Its rank is nine. Select nine independent +principal coordinates as recorded in `label_isometry`. The compressed labels +`l_i` do **not** use the ordinary dot product: their pairing matrix is `J`, +the inverse of the recorded nonsingular compressed Gram matrix. + +Find a `J`-orthonormal basis `v_0,...,v_8` and set +`q(l)_a = l^t J v_a`. The independent checker reconstructs the roots and Gram +matrix without producer imports, checks the inverse and orthonormality, and +verifies every one of the 120^2 identities +`q(l_i) dot q(l_j) = B[i,j]`. +The map is a linear isometry on the whole nine-dimensional binary space, so +it applies to every intermediate frame, including labels outside the 120 roots. +Each root label is odd because `B[i,i]=1`. + +This is a concrete finite choice of physical labels. It is not an all-size +admission proof for an extended label alphabet. + +## 2. Complete primitive identities + +Use the retained canonical chart `Gamma_W` for a binary frame `W`. A literal +transport from `A` to `B` is `Gamma_B Gamma_A^-1`. Every transport is nested. +The exact compiler emits a Gaussian monomial, one positive child of rank +`|dim B-dim A|`, and another Gaussian monomial. No rank is inferred merely +from scalar event counts. There are 740 distinct recipes and 1410 paid uses; +the checker binds every use to its literal source-witness event and rank. + +The independent interpreter imports no Clifford compiler. It compares signed +Pauli conjugations and an exact Gaussian state column. Equal signed Pauli +actions determine a Clifford up to scalar phase; equality on the nonzero state +column fixes that phase. Thus this checks the complete operator, not only its +unsigned symplectic matrix. In addition, all 512 Gaussian columns of each of +the eight rank-seven private drops are compared directly: 4096 columns total. + +Let `C_q = ((1+i)I+(1-i)X_q)/2` and `F9 = product_a C_ea`. +For each source root the intrinsic input chart is `C_q`; its recorded adapter +is `Gamma_ C_q^-1`. For each target the intrinsic output chart is +`F9 C_q^-1`; its adapter is `F9 C_q^-1 Gamma_(q-perp)^-1`. +All 208 operators independently check as rank-zero Gaussian monomials, +including their phases. The final source and dirty-helper full charts are +already `F9`. Monomial endpoints add no positive child to this finite invoice. + +## 3. Full channel induction + +For each live register maintain a rational row `a_r` over the 280 independent +logical inputs. Its physical value is `Gamma_(W_r) a_r z`. +The entry adapters establish this invariant for the 104 intrinsic source +inputs. All other inputs start in the zero frame. + +- A verified native transport changes only `W_r`, retaining `a_r`. +- A literal scalar addition is allowed only in a common physical chart; it + changes `a_r` by the stated exact rational row addition. +- Owned private initialization creates the zero row, copying requires that + zero row and the same chart, and discard requires the prescribed owned + private register and chart. These are the inherited private-copy semantics, + not a claim that a live copy was reversibly uncomputed to zero. + +Inducting through every event proves the complete physical composition. The +checker reconstructs the expected ordinary Gram matrix directly from root +coordinates. At the end each source and each of the 72 dirty helper rows is +its original logical input; each target row is +`y_t + sum_s x_s/2`. +Every endpoint frame also matches. Applying the target exit adapters gives +the stated intrinsic output charts. This covers arbitrary address functions, +not only scalar samples: the rows are identities of operators under the +verified common-chart invariant. + +The source witness is hash-pinned to PR1972. None of its gather, dirty +compensation, delivery or query-cleanup algorithms is newly claimed here. +The new step proves that its abstract chart cancellations have this particular +exact native realization. + +## 4. Accounting and controls + +The independent occurrence recount gives +`{1:1074,2:58,3:86,4:104,5:48,6:24,7:8,8:8}`. +Rank mass is `2368`; the monotone boundary coverage is +`104*8 + 104*8 + 72*9 = 2312`, leaving eight rank-seven private descents. +There are 2624 scalar additions and eight each of private initialization, +copy and discard, for 4058 total events. No additional rank-zero endpoint +child is inserted. + +Five actual faults reject: change a native recipe's global phase; remove a +transport recipe; corrupt a physical root image; set the first initial-query +compensation coefficient to zero; set the last query-cleanup coefficient to +zero. The last two preserve every transport index and are rejected by the +complete endpoint induction, not merely by an event-index mismatch. + +## 5. Unresolved supplier obligations + +This channel implements `G/2`, not `I`. A compatible `I-G/2` correction must +be integrated and priced. The 72 dirty width-nine roles are a local inventory, +not a chronological global owner map. The finite native identities do not +establish recursive precision, arbitrary-size lifting, all global residual +children or an improved recursive moment. No new kappa follows from this +certificate alone. diff --git a/research/p104-native-channel/README.md b/research/p104-native-channel/README.md new file mode 100644 index 0000000000..f187d1ac0b --- /dev/null +++ b/research/p104-native-channel/README.md @@ -0,0 +1,91 @@ +# Native P104 low-rank channel + +Concrete finite Clifford recipes for the complete low-rank channel in +[Rohan Arun's PR1972](https://github.com/CrocSwap/integer-mult-bounds/pull/1972), +head `fd82d172f46933fd253c2c6de4bd5eaff5429cfd`. Its scalar/frame construction +is retained, not claimed new. This package replaces its conditional free-chart +realization with exact Gaussian-dyadic primitive recipes and intrinsic data +endpoint adapters. + +**No complete P104 supplier or new kappa.** The `I-G/2` side correction, +chronological global hosting, precision and all-size admission remain open. +The selected frontier is unchanged. + +## Result + +For the frozen 104 root ports, source logical values `x`, target values `y` +and 72 independent arbitrary dirty helpers, the channel implements +`y <- y + (G/2)x`, with the prescribed source/target transports. All 72 helper +logical values are restored at the full frame. A separate owned private copy +has eight explicit allocate/copy/descend/discard lifetimes under the inherited +private-copy contract; it is not one of the 72 dirty inputs. + +[EXPECTED.json](EXPECTED.json) records: + +- 740 distinct native transport recipes covering all 1410 paid occurrences; +- 208 monomial data endpoint adapters: 104 source entries and 104 target exits; +- all 280 arbitrary register input columns in a complete framed induction; +- 14,400 physical root-pairing checks and 4096 exact Gaussian private-drop columns; +- five rejecting controls, including global phase and missing query compensation/cleanup. + +The exact profile remains +`1074 H1 + 58 H2 + 86 H3 + 104 H4 + 48 H5 + 24 H6 + 8 H7 + 8 H8`. +Its rank mass is **2368 = 2312 boundary coverage + COPY56**. This is the same +local boundary invoice as PR1972, not a globally hosted recursive price. + +The compressed root labels require a nontrivial Gram isometry before using +ordinary physical binary dot products. [PROOF.md](PROOF.md) gives that binding, +the native operator check and the full-word induction. + +## Reproduce + +Standard-library Python. Default replay is read-only, needs no network or Git, +and imports neither the channel producer nor the Clifford compiler: + +```sh +python3 -I -O -B research/p104-native-channel/verify.py +``` + +Also rebuild every recipe in temporary storage and compare the complete +decompressed payload: + +```sh +python3 -I -O -B research/p104-native-channel/verify.py --regenerate +``` + +The registered hook runs both checks with a 300-second limit: + +```sh +python3 scripts/research_package.py --package research/p104-native-channel --check-only +python3 scripts/research_package.py --package research/p104-native-channel +``` + +The generic metadata check needs Git provenance. The direct command also works +from a read-only source export. `--out PATH` writes a receipt exclusively to a +new caller-selected file. Source hashes and exact origins are in +[SOURCES.json](SOURCES.json); [TASK.json](TASK.json) records the changed audit scope. +Compression bytes are not used to compare regenerated mathematics. + +## Open next questions + +Integrate a fully charged `I-G/2` side word while the required source/target +frames remain available. Appending it after source completion is not justified. +Then assign actual chronological owners to the completed word, count all idle +and residual children, and compare the exact recursive moment. Those steps, +plus precision and all-size lifting, are required before a supplier or kappa +claim. Concrete first steps and blockers are in `TASK.json`. + +## Credit + +Rohan Arun / PR1972 supplies the complete scalar/frame channel; Adam Gall / +PR1940 supplies the schedule. The P104 fixture and decoder derive from Josie +Elliston / PR1071, with Ali Romman / PR1125 and the PR968/717/446/595/620 lineage. +The exact compiler is retained through icekylinx's frame-sa504 package; the +independent Gaussian interpreter comes from Ali Romman's PR1862, also retained +in PR1931. Exact predecessor notices are under `notices/`. + +Native lowering, the independent physical binding and framed induction were +prepared for Chafik Boukhalfa with substantial OpenAI Codex assistance. +Apache-2.0. No independent human review, proof assistant or literature-priority +guarantee is claimed. The fresh overlap screen covered 470 open PRs and 614 +discussions; its limits are recorded in `SOURCES.json`. diff --git a/research/p104-native-channel/SOURCES.json b/research/p104-native-channel/SOURCES.json new file mode 100644 index 0000000000..901ad0fb42 --- /dev/null +++ b/research/p104-native-channel/SOURCES.json @@ -0,0 +1,87 @@ +{ + "schema_version": 1, + "base_commit": "25c80aa5345afa3867ff4bc81108a8e182669abd", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + } + ], + "vendored_inputs": [ + { + "path": "inputs/LOWRANK-WITNESS.json", + "sha256": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e", + "head": "fd82d172f46933fd253c2c6de4bd5eaff5429cfd", + "upstream_path": "research/p104-restored-dirty-delivery/LOWRANK-WITNESS.json", + "role": "Rohan Arun / PR1972: complete frame-model low-rank channel" + }, + { + "path": "inputs/LOWRANK-RESULT.json", + "sha256": "7143ec7780f6f38a8c294df8009c3621936b281d05ae79946ce22f581b73d1b1", + "head": "fd82d172f46933fd253c2c6de4bd5eaff5429cfd", + "upstream_path": "research/p104-restored-dirty-delivery/LOWRANK-RESULT.json", + "role": "PR1972 exact invoice; independently recounted" + }, + { + "path": "inputs/P104-FIXTURE.json", + "sha256": "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4", + "head": "fd82d172f46933fd253c2c6de4bd5eaff5429cfd", + "upstream_path": "research/p104-restored-dirty-delivery/source/research/biframe-decoder-ladder/RESULTS.json", + "role": "Josie Elliston / PR1071 fixture through PR1940 and PR1972" + }, + { + "path": "vendor/clifford_exact.py", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "head": "25c80aa5345afa3867ff4bc81108a8e182669abd", + "upstream_path": "research/frame-sa504/vendor/clifford/clifford_exact.py", + "role": "Exact compiler through icekylinx PR531; PR523/514/507/425/433 ancestry" + }, + { + "path": "vendor/native_verify.py", + "sha256": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38", + "head": "bb29ea73ad9be9a0c3d53cdcb1d22b2ee9ffe42f", + "upstream_path": "research/native-source-codes/native_verify.py", + "role": "PR1862 independent exact Gaussian interpreter, also retained through PR1931" + } + ], + "predecessors": [ + { + "pr": 1972, + "head": "fd82d172f46933fd253c2c6de4bd5eaff5429cfd", + "role": "Entire scalar/frame low-rank construction and dirty-helper cancellation; not invented here" + }, + { + "pr": 1940, + "head": "a9b7dfe2809092a9a4c90784d12bb60061e995e8", + "role": "Adam Gall: 32-chain target-order schedule" + }, + { + "pr": 1931, + "head": "7c9b37812b6803fe64bf4427dee7ab82c0155513", + "role": "Retained exact Gaussian interpreter distribution; not the reflection construction" + } + ], + "disclosure": "Native lowering, independent physical binding and framed induction prepared for Chafik Boukhalfa with substantial OpenAI Codex assistance. No independent human review or formal proof assistant.", + "overlap": { + "checked_utc": "2026-10-14T16:12:30Z", + "open_prs": 470, + "discussions": 614, + "pagination_complete": true, + "terms": [ + "P104", + "Clifford", + "dirty-restored" + ], + "closest_predecessor": 1972, + "difference": "Replace free-chart conditional replay by concrete Gaussian-dyadic primitive recipes and intrinsic endpoint adapters. No scalar construction or kappa improvement claimed.", + "limits": "Open PR bodies, discussion bodies/comments and local metadata; no complete code or literature novelty search." + } +} diff --git a/research/p104-native-channel/SUMMARY.json b/research/p104-native-channel/SUMMARY.json new file mode 100644 index 0000000000..fba272d33b --- /dev/null +++ b/research/p104-native-channel/SUMMARY.json @@ -0,0 +1,23 @@ +{ + "status": "COMPILED_EXACT_P104_LOW_RANK_CHANNEL", + "source_pr": 1972, + "source_head": "fd82d172f46933fd253c2c6de4bd5eaff5429cfd", + "upstream_schedule_pr": 1940, + "upstream_schedule_head": "a9b7dfe2809092a9a4c90784d12bb60061e995e8", + "source_witness_sha256": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e", + "source_compiler_sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "source_native_checker_sha256": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38", + "paid_profile": { + "3": 86, + "1": 1074, + "4": 104, + "8": 8, + "2": 58, + "5": 48, + "6": 24, + "7": 8 + }, + "rank_mass": 2368, + "private_drop_basis_columns": 4096, + "scope": "Concrete finite Clifford transport and endpoint adapters for the complete low-rank G/2 channel, including gathering and all 72 dirty helper restorations. Not I-G/2 side correction, chronological global hosting, all-size compilation, precision or a new supplier/kappa." +} diff --git a/research/p104-native-channel/TASK.json b/research/p104-native-channel/TASK.json new file mode 100644 index 0000000000..7dfcf778e4 --- /dev/null +++ b/research/p104-native-channel/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 3, + "base_commit": "25c80aa5345afa3867ff4bc81108a8e182669abd", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Does one selected supplier obligation follow from its actual source-bound checks?", + "starting_points": [ + "certificates/selected-result.json", + "research/owner-boundary-audit/README.md" + ], + "methods": [ + "Trace one hypothesis through the source, checker and complete caller.", + "Construct one semantically invalid but superficially well-formed fixture and test rejection." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "first_step": { + "command": [ + "python3", + "-B", + "research/owner-boundary-audit/verify.py" + ], + "expected": "PASS_PR626_NEXT_TOUCH_BOUNDARY_AUDIT", + "inspect": "Identify why the timing-only omission passes but the full production controller still rejects it.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one current supplier obligation and trace whether its acceptance depends on an independent check.", + "bottleneck_link": "Closing a current acceptance gap or proof obligation strengthens reliability even without changing kappa.", + "allowed_variations": [ + "Audit one named current condition using a new semantic counterexample." + ], + "scope_change_triggers": [ + "Reporting the historical timing-only diagnostic as a new current acceptance bug." + ], + "overlap_terms": [ + "owner boundary", + "bridge omission", + "hosting" + ] + }, + "scope_status": "changed", + "actual_scope": "Construct and independently verify finite native Clifford recipes for PR1972 complete P104 low-rank G/2 channel.", + "scope_change_reason": "The user assigned continuing frontier research. This component targets a pending changed supplier rather than the selected supplier; PR1972 explicitly leaves concrete native realization open.", + "bottleneck_link": "P104 COPY56 is a possible changed centre interface. Concrete phase-correct native delivery and gather are required before side-word integration, global hosting and any moment gain can be tested.", + "budget_minutes": 120, + "stop_rule": "Stop this component when all native transports/endpoints and all 280 input columns replay independently, or a concrete obstruction appears; keep the full kappa=1 research objective open.", + "outcome": "completed", + "evidence": "EXPECTED.json: 740 native transports, 208 rank-zero endpoints, 280 arbitrary input columns, 4096 exact private-drop Gaussian columns, five mutation controls.", + "author": "Chafik Boukhalfa", + "ai_assistance": "Substantial OpenAI Codex assistance; standard-library exact integer and Fraction arithmetic. No independent human review or formal proof assistant.", + "open_questions": [ + { + "question": "Can an I-G/2 side-correction word be integrated with these source and target frame paths?", + "why_it_matters": "The G/2 channel alone is not the identity-transfer component required by a complete supplier.", + "first_step": "Derive the actual P104 side word and interleave its events before the affected source/target frames become unavailable; independently replay all dirty inputs.", + "blocked_by": "No complete compatible side word or fully charged profile supplied." + }, + { + "question": "Can all 72 width-nine dirty roles and private-copy lifetimes be hosted chronologically with a net moment gain?", + "why_it_matters": "Boundary coverage and COPY56 do not price the full recursive network.", + "first_step": "Assign real owners to the completed local word, include all residual/idle children and compare the exact whole-word moment.", + "blocked_by": "Requires a completed side-corrected word, global owner allocation, all-size lifting and precision accounting." + } + ] +} diff --git a/research/p104-native-channel/VERIFY.json b/research/p104-native-channel/VERIFY.json new file mode 100644 index 0000000000..963883dbe7 --- /dev/null +++ b/research/p104-native-channel/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py", + "--regenerate" + ], + "timeout_seconds": 300, + "checks": "All physical pairings; every native edge and endpoint including global phase; all 280 columns and dirty-helper endpoints; all 4096 private-copy Gaussian columns; five mutations; complete regenerated recipe payload." + } + ] +} diff --git a/research/p104-native-channel/check_native.py b/research/p104-native-channel/check_native.py new file mode 100644 index 0000000000..f8e54afbf1 --- /dev/null +++ b/research/p104-native-channel/check_native.py @@ -0,0 +1,141 @@ +"""Read-only native boundary proof: no compiler or producer imports. + +Each literal transport is verified as a complete Clifford operator, including +its scalar phase. A separate frame-invariant scalar replay composes the full +channel, including source query formation. The side correction is outside it. +""" +from pathlib import Path +from fractions import Fraction as Q +from itertools import combinations,product +from collections import Counter +import argparse,copy,gzip,hashlib,importlib.util,json +H=Path(__file__).resolve().parent +P=H/'inputs' +NP=H/'vendor/native_verify.py' +sp=importlib.util.spec_from_file_location('independent_gaussian',NP);N=importlib.util.module_from_spec(sp);sp.loader.exec_module(N) + +def need(ok,why): + if not ok:raise ValueError(why) + +def roots(): + lines=set() + for i,j in combinations(range(8),2): + for sign in (-1,1): + v=[0]*8;v[i]=2;v[j]=2*sign;lines.add(tuple(v)) + for signs in product((-1,1),repeat=7): + if signs.count(-1)%2==0:lines.add((1,*signs)) + need(len(lines)==120,'independent E8 roots');return sorted(lines) + +def span(vs): + out={0} + for v in vs:out|={x^v for x in tuple(out)} + return tuple(sorted(out)) + +def validate(c,w,fixture,full_gaussian=False): + rr=roots();inner=lambda a,b:sum(x*y for x,y in zip(a,b))//4 + binary=[sum(((inner(a,b)+1)&1)<>j)&1)<>j)&1),'all 14400 physical binary pairings') + labels=dict(zip(rr,q));pairs=[(tuple(a),tuple(b))for a,b in fixture['pairs_doubled_coordinates']];removed={tuple(r)for r in fixture['F0']+fixture['C']};ports=[r for r in rr if r not in removed] + need(len(pairs)==8 and len(ports)==104,'P104 fixture binding') + key=lambda f:span(convert(v)for v in f) + charts={};edges={};covered={};paid=Counter();gaussian_columns=0 + def chart(f): + k=span(f);need(len(k)==1<0,'exact native jump rank') + expected=N.adjoint(N.frame(a,9))+N.frame(b,9);N.equal(N.recipe(rec['recipe']),expected,'independent native boundary edge') + if full_gaussian and len(a)==8 and len(b)==1: + for j in range(512):need(N.state(N.recipe(rec['recipe']),j)==N.state(expected,j),'all private-copy basis columns');gaussian_columns+=1 + for i in rec['events']: + need(i not in covered and 0<=ij and piv[k]>>j&1:piv[k]^=piv[j] + return tuple(piv[j]for j in sorted(piv,reverse=True)) + +def label_isometry(): + roots=root_lines();matrix=[sum(((inner(a,b)+1)&1)<len(rows):indices.append(i);rows.append(row) + need(len(indices)==9,'symmetric pairing rank nine') + labels=[sum(((row>>j)&1)<>j)&1),'all physical binary pairings') + return roots,labels,physical,transform,dict(pivot_root_indices=indices,compressed_gram=gram,compressed_dual_gram=dual,orthonormal_basis_compressed=orthogonal,physical_root_labels=physical) + +def main(): + ap=argparse.ArgumentParser();ap.add_argument('--out-dir',type=Path,required=True);args=ap.parse_args();destination=args.out_dir;destination.mkdir(parents=True,exist_ok=True) + need(not any((destination/f).exists()for f in ['NATIVE-RECIPES.json.gz','SUMMARY.json']),'output files already exist') + started=time.monotonic();need(hashlib.sha256(CP.read_bytes()).hexdigest()=='2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962','pinned native compiler') + roots,labels,physical,transform,iso=label_isometry();word=json.loads((P/'LOWRANK-WITNESS.json').read_text());fixture=json.loads((P/'P104-FIXTURE.json').read_text())['section4_explicit_P104'];removed={tuple(r)for r in fixture['F0']+fixture['C']};geom={'ports':[r for r in roots if r not in removed]};byroot=dict(zip(roots,physical)) + frame=lambda f:canon(transform(x)for x in f) + all_frames={frame(f)for f in word['initial_frames'].values()}|{frame(f)for f in word['final_frames'].values()} + edges={} + for index,e in enumerate(word['program']): + if e[0]=='transport': + old,new=frame(e[2]),frame(e[3]);edges.setdefault((old,new),dict(rank=e[4],events=[]))['events'].append(index);all_frames.update((old,new)) + @lru_cache(None) + def chart(f):return CE.canonical_frame(9,f) + recs=[];copy_keys=set();full=tuple(1<>i)&1)<>j&1);a[j],a[k]=a[k],a[j] + for i in range(n): + if i!=j and a[i]>>j&1:a[i]^=a[j] + assert [r&((1<>n for r in a) +def basis_extend(cols,n): + out=[] + for x in list(cols)+[1<len(out):out.append(x) + assert len(out)==n + return tuple(out) +def nullspace(rows,n): + a=list(rows);p=[];k=0 + for j in range(n): + t=next((i for i in range(k,len(a)) if a[i]>>j&1),None) + if t is None:continue + a[t],a[k]=a[k],a[t] + for i in range(len(a)): + if i!=k and a[i]>>j&1:a[i]^=a[k] + p.append(j);k+=1 + return tuple((1<>j)&1)<>i&1:out=pmul(out,T[i]) + for i in range(n): + if z>>i&1:out=pmul(out,T[n+i]) + return out +def compose(A,B):return tuple(apply(A,p) for p in B) +def inverse(T): + n=len(T)//2;cols=[x|(z<>n;u,v,p=apply(T,(x,z,0));assert (u,v)==identity(n)[j][:2];out.append((x,z,(-p)%4)) + return tuple(out) +def qvalue(Q,alpha,x,n): + return (sum(alpha[i] for i in range(n) if x>>i&1)+2*sum(parity((Q[i]>>(i+1))&(x>>(i+1))) for i in range(n) if x>>i&1))%4 +def mul_i(a,p): + x,y=a;p%=4 + return [(x,y),(-y,x),(-x,-y),(y,-x)][p] +@dataclass +class Op: + n:int + tab:tuple + circuit:list + def then(self,b): + assert self.n==b.n + return Op(self.n,compose(b.tab,self.tab),self.circuit+b.circuit) + def adjoint(self): + circ=[] + for e in reversed(self.circuit): + if e[0]=='P':circ.append(('P',inv(e[1],self.n))) + elif e[0]=='D':circ.append(('D',e[1],tuple((-x)%4 for x in e[2]))) + elif e[0]=='C':circ.append(('C',e[1],-e[2])) + elif e[0]=='phase':circ.append(('phase',(-e[1])%4)) + else:circ.append(e) + return Op(self.n,inverse(self.tab),circ) + def zero_state(self,basis=0): + N=1<>i)&1 for i in range(n)) + assert all(alpha[i]%2==(Q[i]>>i)&1 for i in range(n)) + return Op(n,tuple([(1<>i&1 else 0,1<>i&1 else 0) for i in range(n)]),[('C',q,sgn)]) +def xgate(n,b):return Op(n,tuple([(1<>i)&1)) for i in range(n)]),[('X',b)]) +def fourier(n,axes=None): + out=ident(n) + for i in range(n) if axes is None else axes:out=out.then(cgate(n,1<len(selected):picks.append(j);selected.append(x) + assert len(picks)==r and all(x>>r==0 for x in Bcols) + Br=transpose(selected,r);Bi=inv(Br,r);Dr=transpose([Dcols[j]&((1<> j) & 1) << i for i, row in enumerate(matrix)) for j in range(len(matrix))) + + +def inverse(matrix): + n = len(matrix) + rows = [row | (1 << (n+i)) for i, row in enumerate(matrix)] + for j in range(n): + pivot = next((i for i in range(j, n) if rows[i] >> j & 1), None) + require(pivot is not None, 'singular binary chart') + rows[j], rows[pivot] = rows[pivot], rows[j] + for i in range(n): + if i != j and rows[i] >> j & 1: + rows[i] ^= rows[j] + require([row & ((1 << n)-1) for row in rows] == [1 << i for i in range(n)], 'binary inverse') + return tuple(row >> n for row in rows) + + +def extend(vectors, n): + columns, pivots = [], {} + for value in tuple(vectors) + tuple(1 << i for i in range(n)): + reduced = value + while reduced: + j = reduced.bit_length()-1 + if j not in pivots: + pivots[j] = reduced + columns.append(value) + break + reduced ^= pivots[j] + require(len(columns) == n, 'frame basis extension') + return tuple(columns) + + +def adjoint(circuit): + out = [] + for gate in reversed(circuit): + if gate[0] == 'P': + out.append(('P', inverse(gate[1]))) + elif gate[0] == 'D': + out.append(('D', gate[1], tuple(-a % 4 for a in gate[2]))) + elif gate[0] == 'C': + out.append(('C', gate[1], -gate[2])) + elif gate[0] == 'phase': + out.append(('phase', -gate[1] % 4)) + else: + require(gate[0] == 'X', 'adjoint gate type') + out.append(gate) + return tuple(out) + + +def fourier(rank): + return tuple(('C', 1 << i, 1) for i in range(rank)) + + +def frame(vectors, n): + rank = len(vectors) + if rank == 0: + return () + if rank == n: + return fourier(n) + matrix = transpose(extend(vectors, n)) + columns = transpose(inverse(matrix)) + quadratic = tuple((1 << i) ^ sum(parity(a & b) << j for j, b in enumerate(columns)) for i, a in enumerate(columns)) + diagonal = tuple((row >> i) & 1 for i, row in enumerate(quadratic)) + chart = (('P', matrix), ('D', quadratic, diagonal)) + return adjoint(chart) + fourier(rank) + chart + + +def monomial(record): + matrix = tuple(record['matrix_rows']) + quadratic = tuple(record['quadratic_rows']) + linear = tuple(record['linear_Z4']) + require(transpose(quadratic) == quadratic, 'quadratic symmetry') + require(len(matrix) == len(quadratic) == len(linear) == 9, 'monomial dimension') + require(all(a % 2 == (quadratic[i] >> i) & 1 for i, a in enumerate(linear)), 'diagonal parity') + inverse(matrix) + return (('D', quadratic, linear), ('P', matrix), ('X', record['offset']), ('phase', record['phase'])) + + +def recipe(record): + rank = record['rank'] + require(isinstance(rank, int) and 0 <= rank <= 9, 'child rank') + if rank == 0: + require(record['right'] is None, 'rank zero right factor') + return monomial(record['left']) + return monomial(record['right']) + fourier(rank) + monomial(record['left']) + + +def tableau(circuit, n=9): + rows = [(1 << i, 0, 0) for i in range(n)] + [(0, 1 << i, 0) for i in range(n)] + for gate in circuit: + tag = gate[0] + out = [] + inverse_transpose = transpose(inverse(gate[1])) if tag == 'P' else None + for x, z, phase in rows: + if tag == 'P': + x, z = mul(gate[1], x), mul(inverse_transpose, z) + elif tag == 'X': + phase += 2 * parity(z & gate[1]) + elif tag == 'C': + if parity(z & gate[1]): + x ^= gate[1] + phase += 3 * gate[2] + elif tag == 'D': + quadratic, linear = gate[1:] + phase += sum(linear[i] for i in range(n) if x >> i & 1) + phase += 2 * sum(parity((quadratic[i] >> (i+1)) & (x >> (i+1))) for i in range(n) if x >> i & 1) + z ^= mul(quadratic, x) + else: + require(tag == 'phase', 'tableau gate type') + out.append((x, z, phase % 4)) + rows = out + return tuple(rows) + + +@lru_cache(maxsize=512) +def action(gate): + if gate[0] == 'P': + return tuple(mul(gate[1], x) for x in range(512)) + require(gate[0] == 'D', 'state action type') + quadratic, linear = gate[1:] + return tuple((sum(linear[i] for i in range(9) if x >> i & 1) + + 2 * sum(parity((quadratic[i] >> (i+1)) & (x >> (i+1))) for i in range(9) if x >> i & 1)) % 4 for x in range(512)) + + +def rotate(pair, power): + a, b = pair + return ((a, b), (-b, a), (-a, -b), (b, -a))[power % 4] + + +def state(circuit, basis=0): + value, denominator = {basis: (1, 0)}, 0 + for gate in circuit: + tag = gate[0] + result = {} + if tag == "C": + direction, sign = gate[1:] + for address, (a, b) in value.items(): + for target, pair in ((address, (a - sign*b, b + sign*a)), + (address ^ direction, (a + sign*b, b - sign*a))): + old = result.get(target, (0, 0)) + result[target] = (old[0] + pair[0], old[1] + pair[1]) + denominator += 1 + else: + for address, pair in value.items(): + if tag == "P": + target = mul(gate[1], address) + elif tag == "X": + target = address ^ gate[1] + else: + target = address + if tag == "D": + pair = rotate(pair, action(gate)[address]) + else: + require(tag == "phase", "Unknown Gaussian state gate") + pair = rotate(pair, gate[1]) + require(target not in result, "A monomial address map is not injective") + result[target] = pair + value = {address: pair for address, pair in result.items() if pair != (0, 0)} + while denominator and all((a | b) % 2 == 0 for a, b in value.values()): + denominator -= 1 + value = {address: (a//2, b//2) for address, (a, b) in value.items()} + return value, denominator + + +def equal(actual, expected, label): + require(tableau(actual) == tableau(expected), label + ": signed Pauli action") + require(state(actual) == state(expected), label + ": exact global phase") + + +def verify(data, certificate): + word = data["word"] + original, clean = data["programs"], data["clean_programs"] + source_recipes = data["recipes"] + residuals = data["residuals"]["recipes"] + native_tags = {"climb", "adapter", "residual_adapter"} + for orientation in ("forward", "backward"): + native = [event for event in clean[orientation] if event[0] in native_tags] + require(native == [event for event in original[orientation] if event[0] in native_tags], + "A retained native event changed") + require(len(native) == 5056, "The retained native event count changed") + frames = [frame(tuple(vectors), 9) for vectors in word["frames"]] + used = {(event[3], event[4]) for program in clean.values() + for event in program if event[0] == "climb"} + children = {(record["old"], record["new"]): record for record in source_recipes["children"]} + require(len(children) == len(source_recipes["children"]) and used <= set(children), + "The retained child recipe coverage is incomplete") + for old, new in sorted(used): + record = children[old, new] + require(record["rank"] == len(word["frames"][new]) - len(word["frames"][old]), + "A retained child has the wrong rank") + equal(recipe(record), adjoint(frames[old]) + frames[new], "Retained child") + endpoints = {(record["role"], record["port"]): record + for record in source_recipes["endpoint_adapters"]} + require(len(endpoints) == len(source_recipes["endpoint_adapters"]) + and set(endpoints) == {(role, p) for role in ("source", "target") for p in range(112)}, + "The endpoint adapter coverage is incomplete") + for (role, port), record in endpoints.items(): + direction = word["ports"][port] + conventional = (("C", direction, 1),) if role == "source" else ( + ("C", direction, -1),) + fourier(9) + index = word["start"][port] if role == "source" else word["final"][112 + port] + require(record["frame"] == index and record["rank"] == 0, "An endpoint frame changed") + equal(recipe(record), adjoint(conventional) + frames[index], "Endpoint adapter") + used_residuals = set() + for program in clean.values(): + for event in program: + if event[0] != "residual_adapter": + continue + _, position, register, entry, *tail = event + terminal = tail[0] if tail else 1 + key = str(entry) if terminal == 1 else str(entry) + ":" + str(terminal) + require(key in residuals and position in ("pre", "post"), "A residual binding changed") + require(entry == word["start"][register] and terminal == word["final"][register], + "A residual endpoint changed") + used_residuals.add(key) + for key in sorted(used_residuals): + record = residuals[key] + equal(recipe(record), adjoint(frames[record["frame"]]) + frames[record.get("terminal", 1)], + "Residual adapter") + records = certificate["input_recipes"] + ports = certificate["compensation_ports"] + require([record["port"] for record in records] == ports and len(records) == 8, + "The eight input recipes changed") + columns = 0 + for item in records: + port, label = item["port"], item["label"] + require(label == word["ports"][port] and item["canonical_start_frame_id"] == word["start"][port], + "An input recipe has the wrong supplier label") + record = item["recipe"] + require(record["rank"] == 1, "An input copy has the wrong child rank") + for side in ("left", "right"): + factor = record[side] + require(factor["quadratic_rows"] == [0] * 9 and factor["linear_Z4"] == [0] * 9 + and factor["offset"] == factor["phase"] == 0, + "An input factor is not an address permutation") + actual, expected = recipe(record), (("C", label, 1),) + equal(actual, expected, "Positive inherited input line") + for basis in range(512): + require(state(actual, basis) == state(expected, basis), "A complete input Gaussian column differs") + columns += 1 + negative = monomial(record["right"]) + (("C", 1, -1),) + monomial(record["left"]) + require(tableau(negative) != tableau(expected) or state(negative) != state(expected), + "An inverse input child was not detected") + phased = actual + (("phase", 1),) + require(tableau(phased) == tableau(actual) and state(phased) != state(expected), + "An input phase-only error was not detected") + return {"status": "PASS_EXACT_INPUT_NATIVE_FRAMES", "retained_native_events_per_orientation": 5056, + "retained_child_recipes": len(used), "endpoint_adapter_recipes": len(endpoints), + "residual_adapter_recipes": len(used_residuals), "new_input_recipes": len(records), + "new_exact_gaussian_columns": columns, "inverse_input_child_controls": len(records), + "phase_only_controls": len(records), "address_permutation_factors": 2 * len(records), + "method": "Independent signed Pauli and exact Gaussian interpretation; no compiler import", + "scope": "Positive inherited input frames before every retained adapter. No recursive hosting claim."} diff --git a/research/p104-native-channel/verify.py b/research/p104-native-channel/verify.py new file mode 100644 index 0000000000..ba41aa0476 --- /dev/null +++ b/research/p104-native-channel/verify.py @@ -0,0 +1,34 @@ +"""Read-only exact native channel replay; no network, Git or producer imports. + +--regenerate also runs the compiler in temporary storage and compares the +complete decompressed certificate. Ordinary replay uses only the independent +native interpreter and framed scalar induction. +""" +from pathlib import Path +import argparse,gzip,hashlib,importlib.util,json,subprocess,sys,tempfile +P=Path(__file__).resolve().parent + +def need(ok,why): + if not ok:raise ValueError(why) + +def main(): + ap=argparse.ArgumentParser();ap.add_argument('--out',type=Path);ap.add_argument('--regenerate',action='store_true');args=ap.parse_args() + sources=json.loads((P/'SOURCES.json').read_text()) + for item in sources['vendored_inputs']: + need(hashlib.sha256((P/item['path']).read_bytes()).hexdigest()==item['sha256'],'pinned source changed: '+item['path']) + spec=importlib.util.spec_from_file_location('p104_independent_channel',P/'check_native.py');checker=importlib.util.module_from_spec(spec);spec.loader.exec_module(checker) + result=json.loads(json.dumps(checker.replay(True))) + need(result==json.loads((P/'EXPECTED.json').read_text()),'independent replay differs from expected exact receipt') + if args.regenerate: + with tempfile.TemporaryDirectory(prefix='p104-native-')as directory: + subprocess.run([sys.executable,'-I','-O','-B',str(P/'compile.py'),'--out-dir',directory],check=True,timeout=300) + for filename in ['NATIVE-RECIPES.json.gz','SUMMARY.json']: + a=(P/filename).read_bytes();b=(Path(directory)/filename).read_bytes() + if filename.endswith('.gz'):a,b=gzip.decompress(a),gzip.decompress(b) + need(a==b,'regenerated complete payload differs: '+filename) + out=json.dumps(result,sort_keys=True,indent=2)+'\n' + if args.out: + with args.out.open('x')as handle:handle.write(out) + print(out,end='') + +if __name__=='__main__':main()