diff --git a/research/qq16-intervention-independent-audit/README.md b/research/qq16-intervention-independent-audit/README.md new file mode 100644 index 0000000000..54c7af31ea --- /dev/null +++ b/research/qq16-intervention-independent-audit/README.md @@ -0,0 +1,189 @@ +# Independent audit of the QQ16 selected-only intervention obstruction + +**Independent verification; no new kappa or supplier.** This package corroborates +[PR2306](https://github.com/CrocSwap/integer-mult-bounds/pull/2306) at +`4d6e08099c11ff06a8585d04ed59453dd5a62d7d`. Its added evidence is a reduced +8-by-8 integer transfer certificate and an explicit association of **14,784 +emitted alignment references** with their actual stage and port. It imports no +predecessor executable and does not repeat the author's Walsh-polynomial paired +execution implementation. The quantified nonlinear statement rests on the +induction below, not on finitely many nonlinear examples. + +The original common-kernel witness is Adam Gall's PR2093 contribution. The +extension to arbitrary deterministic selected-only interventions is PR2306's +contribution. This package independently checks those claims and adds semantic +source-binding coverage; it claims neither result as a new discovery. + +## Exact scope and result + +Keep Ali Romman's conserved QQ16 F/B maps, the A/T/U partition and the retained +19-event ordinary recipe. Controls begin only **after complete F0**. They may +read/write selected fields, available forward histories and identically +initialized auxiliary state, and may be nonlinear, affine, adaptive or +cross-owner. They cannot read or write ordinary fields, inspect an unfinished +local call, or access distinguishing pre-F0 information. The terminal decoder +gets final selected fields, final completed-X descendants, all five forward +histories and the controller transcript. This is precisely the restricted +observation contract being audited. + +Let `r_p` be column p of R and let `chi_v(d)=(-1)^bit_0(d v)` on cover owners. +The fields are constant in payload coordinates, not in owner d. The actual +source has + +``` +r_2 = r_8 + r_85, +b_(2,0)=37, b_(8,0)=38, b_(85,0)=506. +``` + +Set `h_2=-chi_37`, `h_8=chi_38`, `h_85=chi_506`, and other ordinary fields zero. +For every positive stage s the port routes send those three axes to the same +stage axis, so `B_s h=0` for s=1,...,8. This is an exact all-owner cancellation: +right routing sends `chi_v` to `chi_(rho_s(p)v)`. It does not require independence +of all character functions on the owner group. At identity owner, + +``` +B0 h = (2,2,0,0,0,0,2,-2), +-P_(0,A) B0 h = (-1,0,-1,-1,0,1,0,0). +``` + +Choose the initial pair-0 difference +`X_U=h, Y_U=0, X_A=-P_(0,A)B0h, Y_A=-X_A, X_T=Y_T=0`, with other pairs equal. +The exact A-minor inverse `R_A^T/4` cancels the F0 query. Complete F0 leaves +`X_U=Y_U=h` and zero selected/history difference. The required original +individual A input is nevertheless different. Only restoring selected sums +would be a different problem. + +## A small invariant module instead of a large payload replay + +Whenever selected differences vanish and a pair has ordinary difference +`(alpha*h,beta*h)`, equations (1) and (3) of the pinned +[conserved contract](../joint-query/evidence/CONSERVED-QQ16.md) imply, at positive +stages, + +``` +F_s: (alpha,beta) -> (alpha,beta+alpha), +B_s,t: (alpha,beta) -> (alpha-beta,beta). +``` + +Indeed all current/future query differences vanish, so the selected outputs +also agree. The ordinary bridge is +`alpha_dst += c*alpha_src; beta_src -= c*beta_dst`, and terminal is +`(alpha,beta)->(beta,-alpha)`. These formulas close on an eight-dimensional +space: two ordinary coefficients in each of four banks. They apply to the +difference of arbitrary common backgrounds because the retained local maps are +linear. + +Multiplying the actual 18 events after F0 gives, in interleaved bank order, + +``` +(x0,y0,x1,y1,x2,y2,x3,y3) + -> (x0,y0-x0,x1,y1,x2,y2,x3,y3). +``` + +The independently computed matrix and all 19 witness boundary vectors are in +[RESULT.json](RESULT.json). For post-F0 vector `(1,1,0,0,0,0,0,0)`, the final +vector is `(1,0,0,0,0,0,0,0)`. The four preterminal X projections are zero. +After the signed terminal, the nonzero field is the **former-Y** endpoint +`X_(0,U)`, excluded from completed-X observations. The five forward histories +and every selected difference vanish. + +At each allowed boundary both executions therefore give a controller the same +selected state, histories and auxiliary state. A deterministic control step +returns equal state/transcript and leaves the ordinary difference unchanged. +Induction alternates these equality-preserving control steps with the fixed +linear event updates above. Adaptation and common random coins do not break +that equality. Consequently no decoder of the permitted observations can +recover both distinct original A inputs. This is a written indistinguishability +proof, not a randomized-algorithm lower bound or a proof-assistant theorem. + +**A consequential boundary:** ordinary X immediately after F0 differs by h, +even though it temporarily has a completed-X native frame. Such an intermediate +ordinary read is excluded. The allowed completed-X descendants are the final +named Y fields, not every historical completed-X field. Reading B0h or final +former-Y X0U distinguishes this witness; neither read alone is proved sufficient +for full recovery. + +## Added stage/port source-binding audit + +PR2306 reconstructs route matrices and checks membership in an unordered map +registry. Its immutable source hashes already reject changed packet bytes; +this is **not a demonstrated wrong route or a hash-validation vulnerability**. +Membership alone, however, does not establish that a particular program event +uses the matrix for that event's stage and port. + +`route_binding.py` separately constructs each orthogonal frame swap by exchanging +its projections and checks actual `cover_map` references in the entry and exit +alignment blocks. Coverage is all 37 local cases: 9 forward and 28 backward, +1,008 stage/port matrices, 14,784 references in total, with 2,752 in the nine +cases used by the retained schedule. It also binds case parameters, sweep order +and core stage/orientation. F0's identity alignment is checked separately. + +Two mutations preserve the registry itself: swapping the F2 port-2/port-8 map +references, and substituting F4's port-2 reference at F2 port 2. Both fail the +new semantic predicate. An identical matrix under a different registry ID +passes, so the predicate is not just a label comparison. Four further controls +reject a wrong witness sign, wrong F2 pair, missing negative bridge and wrong +terminal sign. The last is checked on the full eight-variable matrix, because +the particular witness alone has zero preterminal X and cannot detect that sign. + +## Reproduce + +Python 3.12, standard library, from the repository root: + +```sh +python3 -I -B scripts/research_package.py --package research/qq16-intervention-independent-audit +``` + +This runs both normal and optimized checks. Direct replay: + +```sh +python3 -I -O -B research/qq16-intervention-independent-audit/verify.py +``` + +Expected: `PASS_QQ16_INDEPENDENT_INTERVENTION_AUDIT`. +Default verification is read-only and compares the entire stored receipt. +Explicit `--write-result NEW_PATH` refuses to overwrite an existing file. + +Base main is `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, priority revision 4. +[SOURCES.json](SOURCES.json) pins live inputs and historical provenance. +The upstream instruction/selected-state refresh and overlap limits are recorded +in [TASK.json](TASK.json). The local task picker was explicitly overridden to the +central QQ16 handoff after live overlap showed its construction follow-ups were +already claimed. This independent audit is a declared change from construction +synthesis, not satisfaction of the catalogue's supplier acceptance gate. + +## Limitations + +The logical maps, native frame interpretation and bridge convention remain +inherited from the pinned source. This does not rederive R from core scalar +operations, replay private-copy relative maps, native phases, scalar sweep +bodies or recursive child kernels. Payload translations fix the witness fields; +their physical implementation is not reverified. There is no full supplier cold +replay, hosting, precision, all-size or multiplication-theorem claim, and no +selected-frontier change. + +## Open next questions + +1. Can a legal ordinary read or input-dependent retention before F0 avoid the + complete kernel? This matters because selected-only controls cannot. Start + with the active coordinate-tap investigation in Discussion 2205, and test the + full restoration contract before pricing. Native access, full injectivity + and the completed bill remain blockers; this audit does not reserve that task. +2. Could the predecessor checker bind each emitted alignment reference directly? + The two registry-preserving mutation fixtures here are a first regression + target. This would clarify which source associations it independently checks; + maintainers decide whether to reuse this separate checker or adapt its method. + +## Attribution + +Adam Gall (PR2093) supplied the three-port witness; Ali Romman (PR1969) supplied +the QQ16 maps, routes and retained schedule; Cinna Davis (PR2216) supplied the +older-witness shear; PR2306 by @CubeJerry supplies the deterministic intervention +obstruction audited here. @commdata2338's PR2174 is adjacent recovery work with +additional observations. The retained supplier/compiler lineage remains credited +in the unchanged source notices. + +Prepared by @EdDiboi with substantial OpenAI Codex assistance in implementation, +mathematical review, verification and writing, including a separate agent review. +This is independent agent verification, not independent human review or maintainer +acceptance. New work is Apache-2.0. diff --git a/research/qq16-intervention-independent-audit/RESULT.json b/research/qq16-intervention-independent-audit/RESULT.json new file mode 100644 index 0000000000..3d993ff4be --- /dev/null +++ b/research/qq16-intervention-independent-audit/RESULT.json @@ -0,0 +1,424 @@ +{ + "detecting_observations": [ + "B0_h", + "final_former_Y_X0U" + ], + "reduced_trajectory": { + "completed_X_projection_before_terminal": [ + [ + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + -1, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + -1, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -1 + ] + ], + "events": [ + { + "event": 0, + "ordinary_h_coefficients": [ + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": 1, + "ordinary_h_coefficients": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": 2, + "ordinary_h_coefficients": [ + 0, + 1, + 0, + -1, + 0, + 0, + 0, + 0 + ] + }, + { + "event": 3, + "ordinary_h_coefficients": [ + 0, + 1, + 0, + -1, + 0, + 0, + 0, + 0 + ] + }, + { + "event": 4, + "ordinary_h_coefficients": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": 5, + "ordinary_h_coefficients": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": 6, + "ordinary_h_coefficients": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": 7, + "ordinary_h_coefficients": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": 8, + "ordinary_h_coefficients": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": 9, + "ordinary_h_coefficients": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": 10, + "ordinary_h_coefficients": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": 11, + "ordinary_h_coefficients": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": 12, + "ordinary_h_coefficients": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": 13, + "ordinary_h_coefficients": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": 14, + "ordinary_h_coefficients": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": 15, + "ordinary_h_coefficients": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": 16, + "ordinary_h_coefficients": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": 17, + "ordinary_h_coefficients": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": 18, + "ordinary_h_coefficients": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + ], + "tail_matrix_after_F0": [ + [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ] + ] + }, + "rejected_controls": { + "column_dependency_sign": true, + "missing_negative_bridge": true, + "wrong_F2_pair": true, + "wrong_terminal_sign": true + }, + "route_binding": { + "bindings_sha256": "90a5104c65916e2a42f3742a17f3e939178e822d0a78ce7041db95e47a11ca7e", + "cases": 37, + "phase_derived_stage_port_matrices": 1008, + "positive_control": "identical map under a new registry ID", + "positive_stage_alignment_references": 14784, + "rejecting_controls": [ + "swap F2 port 2 and 8 map references within unchanged registry", + "use F4 port 2 map reference at F2 port 2" + ], + "retained_nine_case_alignment_references": 2752, + "scope": "Actual emitted alignment owner matrices; not native phases, scalar bodies or translations" + }, + "scope": "Independent audit of PR2306; nonlinear induction is written proof, not sampling; no supplier or kappa claim.", + "status": "PASS_QQ16_INDEPENDENT_INTERVENTION_AUDIT", + "witness": { + "B0_h_at_identity": [ + "2", + "2", + "0", + "0", + "0", + "0", + "2", + "-2" + ], + "original_A_at_identity": [ + "-1", + "0", + "-1", + "-1", + "0", + "1", + "0", + "0" + ] + } +} diff --git a/research/qq16-intervention-independent-audit/SOURCES.json b/research/qq16-intervention-independent-audit/SOURCES.json new file mode 100644 index 0000000000..9c5be868c9 --- /dev/null +++ b/research/qq16-intervention-independent-audit/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/community-frontier1042-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "6f4dc6fe7631d8aacf8081fcaecf32197181685b", + "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754" + }, + { + "path": "research/joint-query/certificate.json.gz", + "usage": "input", + "git_blob": "c6e876d8b48d768214deee265ade428f8983b566", + "sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" + }, + { + "path": "research/joint-query/evidence/CONSERVED-QQ16.md", + "usage": "input", + "git_blob": "4639583c1be02c2fb60ed8a8072c9969ef1569ce", + "sha256": "60f0de3a7205ba5046b5ae7ffa8bf2b1ea42ea46b498face0a77966b59e7f3fb" + } + ] +} diff --git a/research/qq16-intervention-independent-audit/TASK.json b/research/qq16-intervention-independent-audit/TASK.json new file mode 100644 index 0000000000..bca0f5a506 --- /dev/null +++ b/research/qq16-intervention-independent-audit/TASK.json @@ -0,0 +1,98 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "joint-query-controller", + "question": "Can one explicitly changed QQ16 interface recover the missing chart query and close a two-call controller within a favorable full budget?", + "starting_points": [ + "research/joint-query/README.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Add one explicitly priced ordinary-to-selected observation and derive the ordered two-call map and inverse.", + "Change the first local pair or retained state, then test the existing lost-observation witness and price all new operations." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the fixed-first-pair QQ16 witness before designing a controller. The checked #1969 local words do not evade that witness or supply global placement.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Apply the existing witness to one proposed extra observation or changed first pair. If it still loses the required record, stop. Otherwise derive one ordered two-call identity and charge the added read, chart maps and restoration before extending to more stages.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969" + ] + }, + "scope_status": "changed", + "actual_scope": "Independently audit PR2306 deterministic selected-only intervention obstruction using an eight-variable difference module and emitted stage/port route associations.", + "scope_change_reason": "Live QQ16 construction follow-ups were actively claimed. Deliberately independent verification of the new nonlinear obstruction adds a different reduction and a previously unchecked semantic route association.", + "bottleneck_link": "Checks the information-loss premise that rules out a central class of QQ16 controller repairs; no supplier construction is claimed.", + "budget_minutes": 60, + "stop_rule": "One source-pinned audit only; stop on a false invariant or uncovered source association and report it. Do not synthesize a controller or claim a new kappa.", + "outcome": "completed", + "evidence": "RESULT.json, written invariant/indistinguishability proof in README.md, exact route binding and six rejecting controls.", + "author": "EdDiboi (OpenAI Codex assisted)", + "ai_assistance": "Substantial OpenAI Codex assistance, including parallel source/proof review; no independent human review.", + "open_questions": [ + { + "question": "Can a legally accessed ordinary observation or pre-F0 retention repair the complete kernel?", + "why_it_matters": "Selected-only post-F0 intervention is insufficient.", + "first_step": "Follow the active Discussion2205 coordinate-tap task; test its complete restoration kernel.", + "blocked_by": "Full injectivity, native reads, restoration and completed cost." + }, + { + "question": "Should the predecessor checker directly bind emitted stage/port map references?", + "why_it_matters": "Registry membership alone does not check which event uses a matrix.", + "first_step": "Apply the two registry-preserving mutation fixtures in route_binding.py.", + "blocked_by": "Maintainer choice of checker integration; no current wrong frozen route found." + } + ], + "chooser": { + "seed": "e892415e3d0107027a7d61cd81f69a9e", + "explicit_task_override": "joint-query-controller", + "scope_key": "0e34adbc1dd119161c3a" + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2205#discussioncomment-18941516", + "audited_pr": { + "number": 2306, + "head": "4d6e08099c11ff06a8585d04ed59453dd5a62d7d" + }, + "overlap": { + "open_pr_snapshot_count": 539, + "method": "Public REST complete open-PR pagination, targeted live Discussion reads and repository find_overlap.py local records", + "limitations": "Discussion pagination incomplete. find_overlap remote refresh unavailable because gh is not installed; supplemental public REST/browser checks used. No absence-of-overlap guarantee.", + "distinct_active_claims": [ + "QQ16 single ordinary-coordinate tap full kernel", + "QQ16 native shear-prefix line minimum" + ] + }, + "upstream_checkpoint": { + "checked_at_utc": "2026-10-15T05:33:24.636822+00:00", + "main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "status": "unchanged on canonical fetch before submission; audited PR2306 head unchanged" + }, + "validation_environment": "CPython 3.12.14; standard library; normal and optimized registered replays passed." +} diff --git a/research/qq16-intervention-independent-audit/VERIFY.json b/research/qq16-intervention-independent-audit/VERIFY.json new file mode 100644 index 0000000000..2263cedefe --- /dev/null +++ b/research/qq16-intervention-independent-audit/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1042-audit/selected-replay.tar.gz", + "research/joint-query/certificate.json.gz", + "research/joint-query/evidence/CONSERVED-QQ16.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Pinned input integrity, 19-event reduced transfer, 14784 emitted route references, six mutation controls and one route alias control." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same exact verification and complete receipt comparison with assertions disabled." + } + ] +} diff --git a/research/qq16-intervention-independent-audit/route_binding.py b/research/qq16-intervention-independent-audit/route_binding.py new file mode 100644 index 0000000000..affc08a9d8 --- /dev/null +++ b/research/qq16-intervention-independent-audit/route_binding.py @@ -0,0 +1,188 @@ +#!/usr/bin/env python3 +"""Bind QQ16 chart routes to the actual emitted stage/port map occurrences. + +Standard-library independent source-binding audit; imports no predecessor code. +This checks owner matrices for the alignment blocks of all 37 F/B cases, +not scalar bodies, native phases, translations, or the full emitted operators. +Payload-constant witness fields make translations irrelevant to this audit. +Substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +import gzip +import hashlib +import json +from pathlib import Path + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def expected_routes(phases): + """Swap two orthonormal eight-frames using their projections directly.""" + m = phases["m"] + recipes = phases["recipes"] + require(m == 73 and len(recipes) == 112, "phase dimensions") + routes = {} + for p, recipe in enumerate(recipes): + axes = recipe["idle_children"][0]["orthogonal_axes"][:8] + frame = [recipe["q"], *axes] + require(len(frame) == 9 and all(type(v) is int and 0 < v < 512 for v in frame), + "local chart dimensions") + require(all(((u & v).bit_count() % 2) == (i == j) + for i, u in enumerate(frame) for j, v in enumerate(frame)), + "local chart orthonormality") + routes[0, p] = tuple(1 << j for j in range(m)) + for s in range(1, 9): + columns = [] + for j in range(m): + v = 1 << j + swapped = v + for i, b in enumerate(axes): + e = 1 << (9 + 8 * (s - 1) + i) + # Remove the b/e components and reinsert them exchanged. + if ((v & b).bit_count() % 2) != bool(v & e): + swapped ^= b ^ e + columns.append(swapped) + routes[s, p] = tuple(columns) + return routes + + +def check_bindings(packet, phases): + routes = expected_routes(phases) + maps, programs, params = (packet[k] for k in ("map_registry", "programs", "case_parameters")) + T = packet["T_ports"] + require(T == [21, 37, 47, 76, 81, 87, 92, 110], "selected T binding") + expected_cases = {f"F_{s}" for s in range(9)} | { + f"B_{s}_{t}" for s in range(1, 8) for t in range(s + 1, 9)} + require(set(programs) == set(params) == expected_cases, "complete case domain") + bindings = [] + + def block(case, start, fields, stage, description): + events = programs[case] + require(start >= 0 and start + len(fields) <= len(events), "alignment bounds") + for offset, field in enumerate(fields): + index = start + offset + event = events[index] + require(len(event) == 5 and event[:2] == ["cover_map", ["L", field]], + f"{case}:{index}: {description} field/order") + reference = event[2] + require(reference in maps, f"{case}:{index}: missing map") + columns = maps[reference]["owner_right_matrix_columns"] + require(len(columns) == 73 and all(type(c) is int for c in columns), + f"{case}:{index}: matrix schema") + port = field % 112 + require(tuple(columns) == routes[stage, port], + f"{case}:{index}: {description} stage/port owner matrix") + bindings.append([case, index, field, stage, reference]) + + f_names = ["X_A_fused_query", "X_T_query_subtract", "X_A_restore_selected", + "X_T_sign", "X_U_query_subtract"] + b_names = ["future_E_t", "Y_U_from_X_T", "eight_unsigned_swaps", "Y_T_query_subtract"] + for case in sorted(expected_cases): + events, param = programs[case], params[case] + parts = case.split("_") + stage = int(parts[1]) + kind = parts[0] + require(param["stage"] == stage and param["orientation"] == kind, + f"{case}: parameter binding") + sweeps = [(i, e[1]) for i, e in enumerate(events) if e[0] == "cover_sweep"] + cores = [e[:3] for e in events if e[0] == "retained_core"] + require(cores == [["retained_core", "forward" if kind == "F" else "backward", stage]], + f"{case}: retained core binding") + if kind == "F": + require([name for _, name in sweeps] == f_names, f"{case}: forward sweep order") + first, last = sweeps[0][0], sweeps[-1][0] + require(last - first == 4 and events[0][:3] == ["retained_core", "forward", stage], + f"{case}: forward block order") + if stage == 0: + require(first == 1, "F0 has identity alignment") + else: + require(first == 113, f"{case}: forward entry alignment") + block(case, 1, list(range(112)), stage, "forward entry") + block(case, last + 1, list(range(112)), stage, "forward exit") + else: + future = int(parts[2]) + require(param["future"] == future, f"{case}: future binding") + require([name for _, name in sweeps] == b_names, f"{case}: backward sweep order") + future_index, current_first, current_last = sweeps[0][0], sweeps[1][0], sweeps[-1][0] + require(current_last - current_first == 2 and current_first == future_index + 233, + f"{case}: backward block order") + ys = list(range(112, 224)) + block(case, future_index - 112, ys, future, "future entry") + block(case, future_index + 1, ys, future, "future exit") + block(case, current_first - 120, ys + T, stage, "current entry") + block(case, current_last + 1, ys + T, stage, "current exit") + + require(len(bindings) == 14784, "complete alignment reference count") + retained = {"F_0", "B_1_2", "F_2", "B_3_4", "F_4", "B_5_6", "F_6", "B_7_8", "F_8"} + retained_bindings = sum(row[0] in retained for row in bindings) + require(retained_bindings == 2752, "retained schedule alignment count") + encoded = json.dumps(bindings, separators=(",", ":")).encode() + return { + "cases": 37, + "phase_derived_stage_port_matrices": 1008, + "positive_stage_alignment_references": len(bindings), + "retained_nine_case_alignment_references": retained_bindings, + "bindings_sha256": hashlib.sha256(encoded).hexdigest(), + "scope": "Actual emitted alignment owner matrices; not native phases, scalar bodies or translations", + } + + +def run_controls(packet, phases): + """Change references only, preserving every registry matrix and key.""" + controls = [] + program = packet["programs"]["F_2"] + e2, e8 = program[3], program[9] + original2, original8 = e2[2], e8[2] + + def rejected(label, edit, undo): + edit() + try: + try: + check_bindings(packet, phases) + except ValueError as exc: + require("stage/port owner matrix" in str(exc), "control rejected for unexpected reason") + controls.append(label) + else: + raise ValueError("control accepted: " + label) + finally: + undo() + + def swap(): + e2[2], e8[2] = original8, original2 + + def restore(): + e2[2], e8[2] = original2, original8 + + rejected("swap F2 port 2 and 8 map references within unchanged registry", swap, restore) + wrong_stage = packet["programs"]["F_4"][3][2] + rejected("use F4 port 2 map reference at F2 port 2", lambda: e2.__setitem__(2, wrong_stage), restore) + # Positive representation control: map IDs are labels, not mathematics. + alias = "audit_identical_matrix_alias" + require(alias not in packet["map_registry"], "temporary alias collision") + packet["map_registry"][alias] = packet["map_registry"][original2] + e2[2] = alias + try: + check_bindings(packet, phases) + finally: + restore() + del packet["map_registry"][alias] + return {"rejecting_controls": controls, "positive_control": "identical map under a new registry ID"} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("packet", type=Path) + parser.add_argument("phases", type=Path) + args = parser.parse_args() + packet = json.loads(gzip.decompress(args.packet.read_bytes())) + phases = json.loads(args.phases.read_bytes()) + result = check_bindings(packet, phases) + result.update(run_controls(packet, phases)) + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/qq16-intervention-independent-audit/verify.py b/research/qq16-intervention-independent-audit/verify.py new file mode 100644 index 0000000000..e5d5b3df17 --- /dev/null +++ b/research/qq16-intervention-independent-audit/verify.py @@ -0,0 +1,174 @@ +#!/usr/bin/env python3 +"""Independent QQ16 difference-module audit. Apache-2.0; Codex assisted.""" +from copy import deepcopy +from fractions import Fraction as Q +import argparse +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PACKET = "research/joint-query/certificate.json.gz" +ARCHIVE = "research/community-frontier1042-audit/selected-replay.tar.gz" +PHASES = "t16/global/base/work/complex-nine-native/DATA-PHASES.json" +TEMPLATE = "t16/global/base/split-centres/GLOBAL-TEMPLATE.json.gz" +MEMBER_PINS = { + PHASES: "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + TEMPLATE: "a179dad87651aba340a5a8ddbcd86a8e757cad87b8a1f8bad48106fbecd38518", +} +A = [0, 7, 20, 27, 36, 46, 57, 111] +T = [21, 37, 47, 76, 81, 87, 92, 110] +SUPPORT = {2: -1, 8: 1, 85: 1} + + +def require(value, message): + if not value: + raise ValueError(message) + + +def load(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + for entry in manifest["files"]: + if entry["usage"] == "input": + raw = (ROOT / entry["path"]).read_bytes() + require(hashlib.sha256(raw).hexdigest() == entry["sha256"], "source digest: " + entry["path"]) + members = {} + with tarfile.open(ROOT / ARCHIVE, "r:gz") as archive: + for name, digest in MEMBER_PINS.items(): + matches = [m for m in archive.getmembers() if m.name == name] + require(len(matches) == 1 and matches[0].isfile(), "archive member") + raw = archive.extractfile(matches[0]).read() + require(hashlib.sha256(raw).hexdigest() == digest, "member digest") + members[name] = json.loads(gzip.decompress(raw) if name.endswith(".gz") else raw) + return json.loads(gzip.decompress((ROOT / PACKET).read_bytes())), members + + +def witness(packet, phases, coefficients=None): + # All-owner cancellation follows from the separately bound common route + # image, not from sampling owner values or importing Walsh-polynomial code. + coefficients = SUPPORT if coefficients is None else coefficients + R = [[Q(row.get(str(p), 0)) for p in range(112)] for row in packet["R_rows"]] + require((packet["A_ports"], packet["T_ports"]) == (A, T), "selected minors") + require(len(R) == 8, "R dimension") + require(all(sum(R[i][p] * R[j][p] for p in A) == 4 * (i == j) + for i in range(8) for j in range(8)), "A inverse") + axes = {p: phases["recipes"][p]["idle_children"][0]["orthogonal_axes"][0] for p in coefficients} + require(axes == {2: 37, 8: 38, 85: 506}, "witness axes") + require(all(sum(c * R[i][p] for p, c in coefficients.items()) == 0 for i in range(8)), + "common routed column cancellation") + b0 = [sum(c * (-1 if axes[p] & 1 else 1) * R[i][p] + for p, c in coefficients.items()) for i in range(8)] + original_A = [-sum(R[i][p] * b0[i] for i in range(8)) / 4 for p in A] + require(b0 == [2, 2, 0, 0, 0, 0, 2, -2], "B0 at identity") + require(original_A == [-1, 0, -1, -1, 0, 1, 0, 0], "lost original A") + require([sum(R[i][p] * original_A[j] for j, p in enumerate(A)) + b0[i] + for i in range(8)] == [0] * 8, "F0 query cancellation") + return {"B0_h_at_identity": list(map(str, b0)), "original_A_at_identity": list(map(str, original_A))} + + +def recipe_key(event): + if event["kind"] == "local": + return ["B" if event["reverse"] else "F", event["stage"], event["pair"]] + if event["kind"] == "bridge": + return ["bridge", event["src"], event["dst"], event["coefficient"]] + return [event["kind"], event.get("pairs")] + + +EXPECTED_RECIPE = [ + ["F", 0, 0], ["B", 1, 0], ["bridge", 1, 0, 1], ["F", 2, 0], + ["bridge", 1, 0, -1], ["B", 3, 1], ["bridge", 2, 1, 1], ["F", 4, 1], + ["bridge", 2, 1, -1], ["B", 5, 2], ["bridge", 3, 2, 1], ["F", 6, 2], + ["bridge", 3, 2, -1], ["B", 7, 3], ["F", 8, 3], + ["bridge", 2, 3, 1], ["bridge", 1, 2, 1], ["bridge", 0, 1, 1], ["terminal", 4], +] + + +def trajectory(recipe, terminal_sign=-1): + require([recipe_key(e) for e in recipe] == EXPECTED_RECIPE, "stage/pair/bridge schedule") + # Rows are coefficients of h in (x0,y0,x1,y1,x2,y2,x3,y3) after F0. + matrix = [[int(i == j) for j in range(8)] for i in range(8)] + state = [1, 1, 0, 0, 0, 0, 0, 0] + receipt = [{"event": 0, "ordinary_h_coefficients": state}] + before_terminal = None + for index, event in enumerate(recipe[1:], 1): + kind = event["kind"] + if kind == "local": + x = 2 * event["pair"] + if event["reverse"]: + matrix[x] = [a - b for a, b in zip(matrix[x], matrix[x + 1])] + else: + matrix[x + 1] = [a + b for a, b in zip(matrix[x], matrix[x + 1])] + elif kind == "bridge": + s, d, c = 2 * event["src"], 2 * event["dst"], event["coefficient"] + matrix[d] = [a + c * b for a, b in zip(matrix[d], matrix[s])] + matrix[s + 1] = [a - c * b for a, b in zip(matrix[s + 1], matrix[d + 1])] + else: + before_terminal = deepcopy(matrix) + matrix = [row for p in range(4) for row in + (matrix[2 * p + 1], [terminal_sign * a for a in matrix[2 * p]])] + receipt.append({"event": index, "ordinary_h_coefficients": + [sum(a * b for a, b in zip(row, state)) for row in matrix]}) + expected = [[int(i == j) for j in range(8)] for i in range(8)] + expected[1][0] = -1 + require(matrix == expected, "complete eight-variable tail transfer") + require(receipt[-1]["ordinary_h_coefficients"] == [1, 0, 0, 0, 0, 0, 0, 0], "former-Y endpoint") + require(all(sum(a * b for a, b in zip(before_terminal[i], state)) == 0 + for i in (0, 2, 4, 6)), "completed-X observations") + return {"tail_matrix_after_F0": matrix, "events": receipt, + "completed_X_projection_before_terminal": before_terminal[::2]} + + +def rejected(fn): + try: + fn() + except ValueError: + return True + raise ValueError("negative control unexpectedly accepted") + + +def build_result(): + packet, members = load() + phases, recipe = members[PHASES], members[TEMPLATE]["recipe"] + w, tr = witness(packet, phases), trajectory(recipe) + wrong_pair = deepcopy(recipe) + wrong_pair[3]["pair"] = 1 + controls = { + "column_dependency_sign": rejected(lambda: witness(packet, phases, {2: 1, 8: 1, 85: 1})), + "wrong_F2_pair": rejected(lambda: trajectory(wrong_pair)), + "missing_negative_bridge": rejected(lambda: trajectory(recipe[:4] + recipe[5:])), + "wrong_terminal_sign": rejected(lambda: trajectory(recipe, terminal_sign=1)), + } + require(any(Q(v) for v in w["B0_h_at_identity"]), "B0 read must detect") + require(tr["events"][-1]["ordinary_h_coefficients"][0] == 1, "former-Y read must detect") + spec = importlib.util.spec_from_file_location("route_binding", HERE / "route_binding.py") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + route_result = module.check_bindings(packet, phases) + route_result.update(module.run_controls(packet, phases)) + return {"status": "PASS_QQ16_INDEPENDENT_INTERVENTION_AUDIT", "witness": w, + "reduced_trajectory": tr, "route_binding": route_result, + "rejected_controls": controls, "detecting_observations": ["B0_h", "final_former_Y_X0U"], + "scope": "Independent audit of PR2306; nonlinear induction is written proof, not sampling; no supplier or kappa claim."} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-result", type=Path) + args = parser.parse_args() + result = build_result() + if args.write_result: + with args.write_result.open("x") as stream: + json.dump(result, stream, indent=2, sort_keys=True) + stream.write("\n") + else: + require(json.loads((HERE / "RESULT.json").read_text()) == result, "complete receipt") + print(result["status"]) + print("19 events; exact eight-variable tail transfer; nonzero original A; no new kappa") + + +if __name__ == "__main__": + main()