From 0f493f4c264fbc70ee14364b68af260d858c143c Mon Sep 17 00:00:00 2001 From: Tekalign <152792726+tekuuu@users.noreply.github.com> Date: Fri, 16 Oct 2026 20:58:38 +0300 Subject: [PATCH] Audit native realization of the QQ16 dirty-helper fault --- research/qq16-native-dirty-fault/README.md | 214 ++++++++++++ research/qq16-native-dirty-fault/RESULT.json | 245 +++++++++++++ research/qq16-native-dirty-fault/SOURCES.json | 70 ++++ research/qq16-native-dirty-fault/TASK.json | 122 +++++++ research/qq16-native-dirty-fault/VERIFY.json | 38 ++ research/qq16-native-dirty-fault/native.py | 180 ++++++++++ .../qq16-native-dirty-fault/test_verify.py | 120 +++++++ research/qq16-native-dirty-fault/verify.py | 326 ++++++++++++++++++ 8 files changed, 1315 insertions(+) create mode 100644 research/qq16-native-dirty-fault/README.md create mode 100644 research/qq16-native-dirty-fault/RESULT.json create mode 100644 research/qq16-native-dirty-fault/SOURCES.json create mode 100644 research/qq16-native-dirty-fault/TASK.json create mode 100644 research/qq16-native-dirty-fault/VERIFY.json create mode 100644 research/qq16-native-dirty-fault/native.py create mode 100644 research/qq16-native-dirty-fault/test_verify.py create mode 100644 research/qq16-native-dirty-fault/verify.py diff --git a/research/qq16-native-dirty-fault/README.md b/research/qq16-native-dirty-fault/README.md new file mode 100644 index 0000000000..e6cfc11593 --- /dev/null +++ b/research/qq16-native-dirty-fault/README.md @@ -0,0 +1,214 @@ +# A native binding for the QQ16 dirty-helper fault + +**Scoped mathematical audit; no new supplier or κ.** Arham Tahir's +[PR2995](https://github.com/CrocSwap/integer-mult-bounds/pull/2995), head +`8ba0358b62edbeb16a0842473500c468d8c0759b`, exhibits a restoration-preserving +fault in F0's scalar projection but leaves its native binding open. This +package closes that binding **on its particular witness family**, using exact +Gaussian-dyadic vectors and the actual serialized native recipes. + +The resulting native example still has maximum data error **`4 u T`** from +one allowed completed ADD defect, with all 480 helpers restored exactly and +all eight private fields zero. Here the original data norm is one and T is +the initial norm of one borrowed helper. Thus the permissive local relative +ADD contract, even with exact helper restoration, cannot guarantee a producer +error bound depending only on the original data. The scalar witness, its +52-field response and its necessary precision reserve are credited to PR2995; +the new evidence is their native realization and restricted tensor lift. + +This is **not a failure of an implemented rounding algorithm**. Correctly +rounded exact cancellation may produce zero at the marked instruction. +An exact common-grid ADD implementation also avoids the injected defect. +The result rules out an implication from the stated permissive specification, +not every numerical implementation or multiplication algorithm. + +## Exact statement + +Use the reviewed `programs.F_0` in the pinned +[joint-query certificate](../joint-query/certificate.json.gz), with its +retained local native core and completed child operators. At one completed +ADD `d <- d+c s`, permit a destination error e satisfying + +``` +||e|| <= u (||d|| + |c| ||s||), u > 0. +``` + +Norms are payload Hilbert norms, maximized over data fields and cover owners, +as in [Nick Petalas's PR2965](../qq16-producer-defect-transfer/README.md). +All other completed operations are exact. For each positive common tensor +depth λ, let χ be the unit constant payload, uniform across cover owners. +Choose physical input `L112=χ`, `L359=Tχ`, all other fields zero, with T>0. +These are legal local field values under the retained independent-field and +full-cover access contract; no finite grid or global supplier is asserted. + +At expanded, unfiltered, zero-based event **24438**, the literal instruction is + +```json +["scalar", ["add", ["L", 39], ["L", 359], 4, 1], 1] +``` + +The actual native operands are `(-4Tχ,Tχ)`. After their exact cancellation, +insert `e=8uTχ`, saturating the allowance. The complete native continuation +has error `±4uTχ` in exactly 52 data fields and zero error in every helper and +private field. The ideal execution returns this chosen input unchanged. +Thus every physical helper is restored on this witness, including the dirty +helper L359; this is not a statement that arbitrary helper inputs are always +returned to their original physical bits. + +The fault is at **one instruction site**, uniformly over the addressed +payload components/owners. It is not a single hardware-bit or single-address +fault. Such coherent, state-dependent defects are allowed by the stated +completed-ADD contract. For this constant input the same injection also +satisfies the corresponding pointwise component-relative inequality. + +No finite C can therefore make that specification imply data error at most +`C u H` for all dirty inputs when H bounds only the original data: set H=1 +and choose T>C/4. To guarantee PR2965's sufficient F0 tolerance +`H 2^(-beta-8)` against every such allowed defect requires at least + +``` +u <= (H/T) 2^(-beta-10). +``` + +This repeats PR2995's necessary reserve with a native justification. It is +neither a sufficient precision bound nor an optimal reserve. + +## Why the scalar witness lifts + +The general common-frame conjugation argument is predecessor work, including +[the selected native lift](../selected-centre-native-lift/README.md) and +`Stream.conj_matrix`; this package does not claim it as new. Only the vector +identities needed by the present witness are checked here, rather than all +columns of every native operator. + +Let `1` denote the unnormalized 512-entry constant vector and let `T_f` be +the canonical operator for the stored ordered frame f. Define `v_f=T_f 1`. +Both frame 0 (identity) and frame 1 (the full coordinate line product) give +`v_f=1`. Other frame vectors need not be constant. In particular, ignoring +the entry adapter at source port 39 is a rejecting control. + +The checker reconstructs all 1,004 frame vectors from the published +canonical-frame formula. For each of the 2,880 distinct child recipes used +by the forward core, with its exact global phase and normalization, it checks + +``` +(L F_r R) v_old = v_new. +``` + +It also checks all 224 source/target adapter identities on these vectors in +both directions, every core ADD's source and target frame, all 3,486 child +occurrences, and the complete entry/exit conversion multiplicities. Serialized +monomials use `D, P, X, phase` order. Their quadratic form reads each strict +upper-triangle coefficient once; the old symmetric representation and the +new upper-triangle representation have the same meaning. No phase is dropped. + +For the three scalar trajectories (data basis L112, dirty basis L359, and the +unit error injected at the cut), every wrapped helper is zero at both its +residual entrance and exit. All **1,440** such boundary values are checked. +Its actual inverse right/left monomial therefore maps zero to zero. This +avoids assuming that a residual helper's initial and final gauges coincide. +The only nonzero initial helper, L359, has ordinary endpoints `(0,1)` and +both fix the constant vector. Private CLEARs produce zero in their declared +frames and cannot erase ordinary helper errors. + +Induction through the literal core now gives `physical_i=a_i v_frame(i)` +between conversions, where the a_i follow the scalar word. At event 24438 +both operands have frame 1, so their vectors really are constant. The same +induction applies to the injected constant error. Source and target endpoint +adapters return the relevant vectors to constants. In the F0 wrapper there +are no cover-map events; all eight used native line recipes independently +fix `1`. Each wrapper ADD/SCALE/CLEAR preserves the constant subspace. +Consequently the entire scalar witness and its exact restoration statements +hold in the local native word, not only its scalar projection. + +For tensor depth λ, tensor each checked vector identity. Equal frames remain +equal tensors, while each scalar coefficient acts **once**, not to power λ. +Zero residual boundaries remain zero. Normalize the common constant tensor +to χ. This proves the same coefficients and Hilbert-norm bound for every +positive λ; it is not extrapolation from a numerical sample of tensor depths. +Identity spectators and the retained stage-zero chart embeddings preserve +the argument. Uniformity over owners is compatible with their bijective +views/translations. This last interpretation inherits the reviewed +[core embedding and sweep contract](../joint-query/evidence/BRIDGE-REVIEW.md); +it is not a new global placement, hosting or address-cost proof. + +## Reproduction and evidence + +From the repository root, standard-library CPython 3.12: + +```sh +python3.12 -I -B scripts/research_package.py --package research/qq16-native-dirty-fault +``` + +Expected: `PASS_QQ16_NATIVE_DIRTY_FAULT`, eight passing behavioral tests, then +the package runner's success. Registered CPython 3.12.14 passes; a read-only, +Git-free export also passes with optimized CPython 3.14.7. The native vector check and complete replay +take about 30 seconds on the development host. The command authenticates +every declared live input before reading the native archive. It imports no +predecessor executable code and writes no scientific artifact. `--write PATH` +on `verify.py` creates an absent receipt and refuses to overwrite it. + +[RESULT.json](RESULT.json) contains exact source-derived event/frame digests, +the complete 52-field response and replay counts. Independently of the +frame-reduced proof, the same package executes **all 26,099 events** directly +on 512-component Gaussian-dyadic vectors, including inverse residual wrappers. +For `T=256`, `u=2^-20`, `eta=1/512`, all **364,544 endpoint amplitudes** agree +with the stated result; maximum data error is `1/1024`. This literal path +shares the primitive vector evaluator, but does not use scalar projection +or frame vectors to execute the native word. It is a corroborating algorithm +by the same assisted author, not independent human or formal-kernel review. + +Controls reject an altered child global phase, omitted nonconstant adapter, +missing kernel normalization, altered wrapper global phase, wrong fault +location, modified source and marked-instruction sign. An earlier fault at +24434 affects 102 helper outputs and fails the zero residual-boundary test. +Analytic basis-column and quadratic-form controls check primitive conventions. +All eight wrapper recipes also agree with their line operator on a vector +with distinct Gaussian components. Exact/absolute-error and zero-dirty +controls retain the legitimate ways to escape the obstruction. + +## Scope + +This closes the native binding for one F0 fault family. It does not check +every native operator column, arbitrary internal faults, concrete rounded +child implementations, grids/overflow, dirty-input ranges, physical machine +steps/storage, a paid F17 consumer, global hosting, or the full multiplication +theorem. Existing child operator semantics and the reviewed full-cover access +contract are inherited. The selected frontier and every frozen input remain +unchanged; a selected cold replay is therefore not part of this audit. + +## Open next questions + +The useful next question is whether a source-bound finite F0 implementation +can **exclude this fault and meet the complete producer tolerance**. Begin +with its actual dyadic grid, the dirty-input bound and the instructions that +perform rounding. Prove exactness at cancellations where possible, and bound +the remaining native-child defects and the whole physical bill. This matters +because reducing a headline precision constant cannot replace those premises. +The absence of an admitted numerical producer and its paid caller is the +blocker. [TASK.json](TASK.json) records this handoff and the bounded scope. +Family decision: narrow and stop; no new construction search. + +## Provenance and credit + +Scientific base: `836b19bfa309ceafbc8ee32a15e8c4b10dde7e11`, priority +revision 6, OS assignment seed **67** (adversarial mathematical audit). +Submission base: `d8e0f83f00191df62174b641e9fff055c357f641`; the coordination +update leaves all eight live inputs and the selected record unchanged. +[SOURCES.json](SOURCES.json) records exact repository and archive-member pins. +The native archive is the retained source at +`bce54fb3f895cbe5cd4c0eb477c3afeed100190f`, SHA256 +`22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754`. +The canonical [claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/2727#discussioncomment-18978907) +was checked against recent PRs and Discussion comments before posting. + +Credit Arham Tahir/PR2995 for the precise fault and handoff; Nick Petalas/ +PR2965 (`526f2c242202b31b15e09a7502dfb8ff757b2bad`) for the producer-tolerance +contract; Ali Romman and the QQ16 team for the retained program; Sagar Thakrar +for the exact Clifford conventions and selected recipe audit; DLamdata for +the selected native-frame lift; ywz65, starship-s, Ross Richardson, Douglas +Colkitt and the remaining supplier/native lineage retained in the joint-query +notices. The independent evaluator here follows their published semantics; +their native recipe theorem and general conjugation lemma are not new claims. +Prepared by **Tekalign (@tekuuu), with substantial OpenAI Codex assistance**. +Apache-2.0. No independent human review is claimed. diff --git a/research/qq16-native-dirty-fault/RESULT.json b/research/qq16-native-dirty-fault/RESULT.json new file mode 100644 index 0000000000..7e5fbb8853 --- /dev/null +++ b/research/qq16-native-dirty-fault/RESULT.json @@ -0,0 +1,245 @@ +{ + "all_480_physical_helpers_restore_on_witness": true, + "all_8_private_outputs_zero": true, + "data_error": "4*u*T", + "dirty_register": 359, + "event_sha256": "4c1ee518a6513c115741a3834c49490c6e8e68f5e2357af8dac782c3d40958e7", + "expanded_events": 26099, + "fault_index": 24438, + "literal_check": { + "T": "256", + "coordinates": 364544, + "eta": "1/512", + "max_data_error": "1/1024", + "u": "1/1048576" + }, + "local_relative_allowance": "8*u*T", + "meaning": "permissive completed-ADD fault, not a concrete rounding failure", + "native_binding": { + "child_occurrences": 3486, + "data_adapters": 224, + "frame_vector_sha256": "203dc933c37ecfbf6a9d755d9f3310a94afbd5e111956f57be95daf24555821c", + "frame_vectors": 1004, + "local_payload_coordinates": 512, + "residual_records": 36, + "scalar_frame_checks": 20089, + "used_child_recipes": 2880, + "used_edges_sha256": "194cf5c42eefafd898908105331b2545ce6cf024605b217a9b18ee5bbf86f915", + "wrapper_lines": 8 + }, + "original_data_register": 112, + "schema_version": 1, + "scope": "exact local native F0 and tensor/owner lift under retained access contract", + "status": "PASS_QQ16_NATIVE_DIRTY_FAULT", + "unit_fault_response": [ + [ + 2, + "-1/2" + ], + [ + 4, + "-1/2" + ], + [ + 6, + "1/2" + ], + [ + 9, + "-1/2" + ], + [ + 11, + "-1/2" + ], + [ + 13, + "1/2" + ], + [ + 15, + "1/2" + ], + [ + 17, + "-1/2" + ], + [ + 19, + "-1/2" + ], + [ + 23, + "-1/2" + ], + [ + 29, + "-1/2" + ], + [ + 33, + "-1/2" + ], + [ + 35, + "-1/2" + ], + [ + 38, + "-1/2" + ], + [ + 40, + "-1/2" + ], + [ + 41, + "1/2" + ], + [ + 43, + "1/2" + ], + [ + 44, + "1/2" + ], + [ + 47, + "-1/2" + ], + [ + 48, + "-1/2" + ], + [ + 50, + "-1/2" + ], + [ + 52, + "1/2" + ], + [ + 55, + "-1/2" + ], + [ + 58, + "-1/2" + ], + [ + 60, + "-1/2" + ], + [ + 62, + "-1/2" + ], + [ + 65, + "-1/2" + ], + [ + 68, + "1/2" + ], + [ + 71, + "-1/2" + ], + [ + 73, + "1/2" + ], + [ + 75, + "1/2" + ], + [ + 77, + "-1/2" + ], + [ + 81, + "1/2" + ], + [ + 83, + "1/2" + ], + [ + 85, + "-1/2" + ], + [ + 86, + "-1/2" + ], + [ + 87, + "1/2" + ], + [ + 89, + "-1/2" + ], + [ + 91, + "-1/2" + ], + [ + 94, + "-1/2" + ], + [ + 96, + "1/2" + ], + [ + 99, + "1/2" + ], + [ + 101, + "1/2" + ], + [ + 103, + "-1/2" + ], + [ + 105, + "1/2" + ], + [ + 107, + "-1/2" + ], + [ + 109, + "-1/2" + ], + [ + 110, + "1/2" + ], + [ + 119, + "1/2" + ], + [ + 132, + "1/2" + ], + [ + 139, + "1/2" + ], + [ + 148, + "-1/2" + ] + ], + "zero_residual_boundary_checks": 1440 +} diff --git a/research/qq16-native-dirty-fault/SOURCES.json b/research/qq16-native-dirty-fault/SOURCES.json new file mode 100644 index 0000000000..7751ad7893 --- /dev/null +++ b/research/qq16-native-dirty-fault/SOURCES.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "base_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "4450dbbd1d01929022259f523234590f4cce65b9", + "sha256": "ca056a6def333df7afd822c1f34adc2eaa9089b241fc2bdd5803b64066fc9355" + }, + { + "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/BRIDGE-REVIEW.md", + "usage": "input", + "git_blob": "86139908c418235588045324f0873de6ac9f9707", + "sha256": "d01b5f4959f7c91f835496d050dfae3eeab9dee2f581571c316a42571eaa1cd3" + }, + { + "path": "research/joint-query/evidence/NATIVE-REVIEW.md", + "usage": "input", + "git_blob": "525b38dbdefed0e8192a9c5165e802136cc05034", + "sha256": "2247e3cbe73f3f0da55c647ffae15f98dd9445b2366ba9e255b9bebc9f742b70" + }, + { + "path": "research/frontier1094-recipes-exact-seed76/clifford.py", + "usage": "input", + "git_blob": "6f1e6a38febde7eb7a7341d317522e6650d84408", + "sha256": "d5e42ddabd141b7bfbd70fe13908f3c3a06aeccebeab90623596bfb1988b97fb" + }, + { + "path": "research/selected-centre-native-lift/README.md", + "usage": "input", + "git_blob": "98721e3eb4b955129321078f09c4b1b3b2ef5ae0", + "sha256": "aa50f2984b8f0af8781e1b0295f907606b1031bc284a396b683f3e5506148595" + }, + { + "path": "research/joint-query/source_data.py", + "usage": "input", + "git_blob": "c9d465ed47500304bef65fcb588befe356c5cf09", + "sha256": "d23924511e3aed41e5e64511ca70126a636d91c8aa02e656cb61d6ceca1fe0a0" + }, + { + "path": "research/qq16-producer-defect-transfer/README.md", + "usage": "input", + "git_blob": "16903a0090c020d033d24712cce11c633031e688", + "sha256": "30cf4389425f7704b1ed45af6cf4b5165e7b5c04af5077640ac96399c61cd703" + } + ], + "predecessors": { + "2995": "8ba0358b62edbeb16a0842473500c468d8c0759b", + "2965": "526f2c242202b31b15e09a7502dfb8ff757b2bad" + } +} diff --git a/research/qq16-native-dirty-fault/TASK.json b/research/qq16-native-dirty-fault/TASK.json new file mode 100644 index 0000000000..16c3a25bb6 --- /dev/null +++ b/research/qq16-native-dirty-fault/TASK.json @@ -0,0 +1,122 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 6, + "base_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11", + "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", + "research/scatter-export-parity-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", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2977 reported duplicate-scatter counterexample and its opt-in repair. The archive is not a production fix or an independently validated selected-result failure; the selected generator emits unique rows.", + "scope": "Source-binding orientation only; does not replay or validate the reported bug." + }, + "first_experiment": "First check whether the scatter repair has been adopted. If still open, independently reproduce #2977 symbolic-versus-exported parity on the tiny duplicate fixture, compare the selected unique-row positive control, and define either enforced uniqueness or consistent multiplicity semantics. A bounded guard-adoption patch must preserve valid inputs and test the actual exported action. Stop after this obligation; no full historical replay or frontier change follows from the mutant alone.", + "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.", + "Calling a malformed mutant a failure of the selected construction, or importing an opt-in repair without testing the exporter boundary." + ], + "overlap_terms": [ + "owner boundary", + "bridge omission", + "hosting", + "2977", + "scatter export", + "duplicate index", + "parity semantics" + ] + }, + "scope_status": "changed", + "actual_scope": "Bind PR2995's event-24438 scalar dirty-helper fault to F0's exact native word on its constant-input witness family, including intermediate canonical frames and tensor lift.", + "scope_change_reason": "The suggested scatter obligation is already addressed by PR2992/3004. Take the released PR2995 native-binding handoff instead, within the assigned adversarial audit track. This is a pending QQ16 producer implication, not a claimed selected-construction bug.", + "bottleneck_link": "PR2965 leaves producer interiors and dirty bounds open. Establishing the native realization decides whether PR2995's obstruction is an artifact of scalar projection.", + "budget_minutes": 60, + "stop_rule": "One 60-minute round from 2026-10-16 17:31 UTC; orientation at most 12 minutes; final 15 minutes for verification/handoff. Stop after one source-bound native implication. No parameter search or new supplier.", + "outcome": "completed", + "evidence": "Exact frame-vector identities for all 2880 used child recipes, 224 endpoint adapters, complete core frame/role chronology, 1440 zero residual boundaries; literal 26099-event Gaussian-dyadic replay; eight behavioral groups.", + "author": "Tekalign (@tekuuu)", + "ai_assistance": "Substantial OpenAI Codex assistance for research, code, proof, verification and writing; no independent human review.", + "open_questions": [ + { + "question": "Can one finite F0 producer meet the completed tolerance by exact-grid arithmetic and a paid dirty-input bound?", + "why_it_matters": "The permissive relative ADD contract plus helper restoration is insufficient even for this native witness.", + "first_step": "Pin an actual numerical producer, its grid and dirty range; prove exactness of the marked cancellation, then bound its remaining rounded native children and charge the complete caller.", + "blocked_by": "No admitted finite producer with a complete grid/range and physical cost contract is provided here." + } + ], + "assignment": { + "os_seed": 67, + "track": "adversarial mathematical audit", + "fresh_draw": true, + "round": 57 + }, + "candidates": [ + { + "object": "QQ16 F0 event24438", + "predecessor_pr": 2995, + "question": "Does the precise scalar fault survive the native word?", + "decision": "Chosen: explicit released native-binding handoff; exact frame-vector method adds missing evidence." + }, + { + "object": "high-route complete single-cube bill", + "predecessor_pr": 2982, + "question": "Can the all-width encoded-setup and high-ADD tariff be source-bound?", + "decision": "Not pursued: larger cost-contract surface than the bounded native implication." + }, + { + "object": "P104 retained history", + "predecessor_pr": 2999, + "question": "Which priced history or source-assisted cleanup escapes the memoryless collision?", + "decision": "Not pursued: a new cleanup design is needed, not another collision audit." + } + ], + "claim": { + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2727#discussioncomment-18978907", + "expires_utc": "2026-10-16T18:31:00Z" + }, + "overlap": { + "entry": "Full earlier paginated PR corpus plus 100 most recently updated PRs and 40 recently updated Discussions; snapshot spans updates before the preceding complete refresh. Both repository issues checked. Canonical Discussion2727 and 12 most recently updated PRs refreshed immediately before claim. No matching active claim seen.", + "nearest": "PR2995 supplies the scalar witness and explicitly leaves native binding unverified. PR2965 supplies the inherited norm and sufficient tolerance. PR3006/3008 audit a different V45 rank-seven candidate.", + "limitations": "Metadata coverage does not cover arbitrary unpublished work or every diff; this is not a review of every PR theorem." + }, + "family_decision": "narrow and stop", + "freshness": { + "checked_at_utc": "2026-10-16T17:56:23.687150+00:00", + "submission_base": "d8e0f83f00191df62174b641e9fff055c357f641", + "scientific_base": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11", + "priority_revision": 6, + "decision": "Continue and publish the completed narrow audit. Main changed coordination guidance, not selected result or any of the eight live inputs. Original source/card pins remain immutable.", + "metadata": "2698 PRs total at refreshed checkpoint; latest40 updated PRs, both issues and canonical Discussion2727 checked. New PR3015 candidate kappa does not overlap this producer-fault implication; no matching active claim or superseding native binding found." + }, + "verification": { + "registered_cpython": "3.12.14 passed", + "readonly_git_free_export": "Optimized CPython3.14.7 primary and all eight groups passed; final controls rechecked after adding the nonidentity full-frame control.", + "baseline": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY after materializing selected inputs in sparse checkout; not a cold replay", + "python_optimization": "all checks use explicit exceptions; normal/optimized tests pass", + "unrun": [ + "selected cold replay", + "hosted CI", + "independent human review", + "formal-kernel proof" + ] + } +} diff --git a/research/qq16-native-dirty-fault/VERIFY.json b/research/qq16-native-dirty-fault/VERIFY.json new file mode 100644 index 0000000000..2a94ff546c --- /dev/null +++ b/research/qq16-native-dirty-fault/VERIFY.json @@ -0,0 +1,38 @@ +{ + "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/BRIDGE-REVIEW.md", + "research/joint-query/evidence/NATIVE-REVIEW.md", + "research/frontier1094-recipes-exact-seed76/clifford.py", + "research/selected-centre-native-lift/README.md", + "research/joint-query/source_data.py", + "research/qq16-producer-defect-transfer/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact native frame-vector binding and full 26099-event literal Gaussian-dyadic witness; all 364544 final amplitudes." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 60, + "checks": "Eight behavioral groups: phase/normalization/adapter conventions, invalidation, wrong fault location/restoration and legitimate exact/absolute-error escapes." + } + ] +} diff --git a/research/qq16-native-dirty-fault/native.py b/research/qq16-native-dirty-fault/native.py new file mode 100644 index 0000000000..e1976b3a55 --- /dev/null +++ b/research/qq16-native-dirty-fault/native.py @@ -0,0 +1,180 @@ +"""Exact Gaussian-dyadic vectors; no predecessor implementation is imported. + +Conventions follow the credited native Clifford sources in README.md. +Tekalign, with substantial OpenAI Codex assistance. Apache-2.0. +""" +from functools import lru_cache + +DIM = 512 + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def vector(real, imag=None, exponent=0): + real = tuple(real) + imag = tuple(imag) if imag is not None else (0,) * len(real) + need(len(real) == len(imag) == DIM and exponent >= 0, "vector dimensions") + if not any(real) and not any(imag): + return ZERO + while exponent and all(x % 2 == 0 for x in real + imag): + real = tuple(x // 2 for x in real) + imag = tuple(x // 2 for x in imag) + exponent -= 1 + return real, imag, exponent + + +ZERO = ((0,) * DIM, (0,) * DIM, 0) +ONE = ((1,) * DIM, (0,) * DIM, 0) + + +def rotate(a, b, phase): + return ((a, b), (-b, a), (-a, -b), (b, -a))[phase % 4] + + +def rank(rows): + pivots = {} + for value in rows: + while value: + high = value.bit_length() - 1 + if high not in pivots: + pivots[high] = value + break + value ^= pivots[high] + return len(pivots) + + +def transpose(rows): + return tuple(sum(((rows[j] >> i) & 1) << j for j in range(9)) for i in range(9)) + + +def inverse(rows): + aug = [x | (1 << (9 + i)) for i, x in enumerate(rows)] + for i in range(9): + pivot = next((j for j in range(i, 9) if (aug[j] >> i) & 1), None) + need(pivot is not None, "invertible binary map") + aug[i], aug[pivot] = aug[pivot], aug[i] + for j in range(9): + if j != i and (aug[j] >> i) & 1: + aug[j] ^= aug[i] + return tuple(x >> 9 for x in aug) + + +def monomial_key(record, axes=9): + """Reduce identity spectators, checking every discarded coordinate.""" + need(set(record) == {"matrix_rows", "quadratic_rows", "linear_Z4", "offset", "phase"}, + "monomial schema") + rows, quad, linear = (record[k] for k in ("matrix_rows", "quadratic_rows", "linear_Z4")) + need(len(rows) == len(quad) == len(linear) == axes, "monomial axes") + need(all(type(x) is int for x in rows + quad + linear), "integer monomial") + need(all(0 <= x < 2**axes for x in rows + quad) and all(0 <= x < 4 for x in linear), + "monomial coefficient range") + need(0 <= record["offset"] < DIM and 0 <= record["phase"] < 4, "monomial constants") + need(all(x < DIM for x in rows[:9] + quad[:9]), "no low/high coupling") + need(rows[9:] == [1 << i for i in range(9, axes)] + and not any(quad[9:] + linear[9:]), "identity spectators") + need(rank(rows[:9]) == 9, "invertible monomial") + return tuple(rows[:9]), tuple(quad[:9]), tuple(linear[:9]), record["offset"], record["phase"] + + +@lru_cache(256) +def table(key): + rows, quad, linear, offset, phase = key + result = [] + for x in range(DIM): + dest = offset ^ sum(((x & row).bit_count() % 2) << i for i, row in enumerate(rows)) + angle = phase + sum(linear[i] for i in range(9) if (x >> i) & 1) + # Old core stores symmetric Q; wrapper recipes store an upper triangle. + # Both conventions read each strict-upper pair exactly once. + angle += 2 * sum((quad[i] & x & ~((1 << (i + 1)) - 1)).bit_count() + for i in range(9) if (x >> i) & 1) + result.append((dest, angle % 4)) + need(len({dest for dest, _ in result}) == DIM, "monomial permutation") + return tuple(result) + + +def mono(value, key, adjoint=False): + re, im, exponent = value + rr, ii = [0] * DIM, [0] * DIM + for x, (dest, angle) in enumerate(table(key)): + if adjoint: + rr[x], ii[x] = rotate(re[dest], im[dest], -angle) + else: + rr[dest], ii[dest] = rotate(re[x], im[x], angle) + return vector(rr, ii, exponent) + + +def line(value, axis, sign=1, normalize=True): + need(0 < axis < DIM and sign in (-1, 1), "line parameters") + re, im, exponent = value + rr, ii = [], [] + for x in range(DIM): + a, b, c, d = re[x], im[x], re[x ^ axis], im[x ^ axis] + rr.append(a - sign*b + c + sign*d) + ii.append(b + sign*a + d - sign*c) + return vector(rr, ii, exponent + int(normalize)) + + +def recipe(value, record, axes=9): + r = record["rank"] + need(type(r) is int and 0 <= r <= 9, "child rank") + if r: + value = mono(value, monomial_key(record["right"], axes)) + for j in range(r): + value = line(value, 1 << j) + else: + need(record["right"] is None, "rank-zero recipe") + return mono(value, monomial_key(record["left"], axes)) + + +def diagonal(value, quad, linear, sign=1): + key = (tuple(1 << i for i in range(9)), tuple(quad), + tuple((sign*x) % 4 for x in linear), 0, 0) + return mono(value, key) + + +def permute(value, rows): + return mono(value, (tuple(rows), (0,) * 9, (0,) * 9, 0, 0)) + + +def frame(axes): + """T_U applied to the constant vector, using the stored ordered basis.""" + r = len(axes) + need(rank(axes) == r and all(0 < x < DIM for x in axes), "independent frame") + if r in (0, 9): + return ONE # I and the full coordinate C-product both fix constants. + ext = list(axes) + for axis in (1 << i for i in range(9)): + if rank(ext + [axis]) > len(ext): + ext.append(axis) + g = transpose(ext) + gi = inverse(g) + columns = transpose(gi) + quad = tuple((1 << i) ^ sum(((columns[i] & columns[j]).bit_count() % 2) << j + for j in range(9)) for i in range(9)) + linear = tuple((quad[i] >> i) & 1 for i in range(9)) + # Circuit: K^-1, F_r, K; K is P(G) followed by D(Q). + value = permute(diagonal(ONE, quad, linear, -1), gi) + for j in range(r): + value = line(value, 1 << j) + value = diagonal(permute(value, g), quad, linear) + need(sum(x*x for x in value[0] + value[1]) == DIM * 2**(2*value[2]), + "frame preserves squared norm") + return value + + +def scaled(value, coefficient): + n, d = coefficient.numerator, coefficient.denominator + need(d > 0 and d & (d-1) == 0, "dyadic coefficient") + return vector((n*x for x in value[0]), (n*x for x in value[1]), + value[2] + d.bit_length()-1) + + +def plus(left, right): + exponent = max(left[2], right[2]) + shifts = exponent-left[2], exponent-right[2] + return vector(((a << shifts[0]) + (b << shifts[1]) for a, b in zip(left[0], right[0])), + ((a << shifts[0]) + (b << shifts[1]) for a, b in zip(left[1], right[1])), + exponent) diff --git a/research/qq16-native-dirty-fault/test_verify.py b/research/qq16-native-dirty-fault/test_verify.py new file mode 100644 index 0000000000..00202f020d --- /dev/null +++ b/research/qq16-native-dirty-fault/test_verify.py @@ -0,0 +1,120 @@ +#!/usr/bin/env python3 +"""Behavioral controls for the precise native-fault implication. + +Tekalign, with substantial OpenAI Codex assistance. Apache-2.0. +""" +from copy import deepcopy +from fractions import Fraction as Q +from pathlib import Path +import tempfile +import types +import unittest + +HERE = Path(__file__).resolve().parent +V = types.ModuleType("fault_verifier") +V.__file__ = str(HERE / "verify.py") +exec(compile((HERE / "verify.py").read_bytes(), V.__file__, "exec"), V.__dict__) +N = V.N + + +class Controls(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.packet, cls.word, cls.recipes, cls.residuals = V.load(V.ROOT) + cls.events = V.expand(cls.packet) + + def test_global_phase_is_not_discarded(self): + used = next(e for e in self.events if e[0] == "climb") + old, new = used[3:5] + rec = deepcopy(V.recipes_by_key(self.recipes)[0][old, new]) + before, after = N.frame(self.word["frames"][old]), N.frame(self.word["frames"][new]) + self.assertEqual(N.recipe(before, rec), after) + rec["left"]["phase"] = (rec["left"]["phase"] + 1) % 4 + self.assertNotEqual(N.recipe(before, rec), after) + + def test_frame_adapters_cannot_be_ignored(self): + rec = V.recipes_by_key(self.recipes)[1]["source", 39] + image = N.mono(N.ONE, N.monomial_key(rec["left"])) + self.assertEqual(image, N.frame(self.word["frames"][rec["frame"]])) + self.assertNotEqual(image, N.ONE) + self.assertEqual(N.mono(image, N.monomial_key(rec["left"]), True), N.ONE) + + def test_kernel_normalization(self): + self.assertEqual(N.line(N.ONE, 67), N.ONE) + self.assertEqual(N.line(N.ONE, 67, normalize=False), N.scaled(N.ONE, Q(2))) + # Analytic single-basis column, independently specified coefficients. + basis = N.vector([int(i == 0) for i in range(512)]) + want_re, want_im = [0]*512, [0]*512 + want_re[0] = want_re[67] = 1 + want_im[0], want_im[67] = 1, -1 + self.assertEqual(N.line(basis, 67), N.vector(want_re, want_im, 1)) + full = basis + for axis in range(9): + full = N.line(full, 1 << axis) + self.assertNotEqual(full, basis) # full frame is not physical identity + self.assertEqual(sum(x*x for x in full[0] + full[1]), 2**(2*full[2])) + + def test_wrapper_all_input_components(self): + # Distinct tagged components, not the constant-vector positive fixture. + value = N.vector([i*67-1234 for i in range(512)], [i*i-9 for i in range(512)]) + keys = {e[2] for e in self.events if e[0] == "native_line"} + for key in sorted(keys): + entry = self.packet["native_line_recipes"][key] + self.assertEqual(N.recipe(value, entry["recipe"]), N.line(value, entry["label"], entry["sign"])) + rec = deepcopy(self.packet["native_line_recipes"][sorted(keys)[0]]["recipe"]) + rec["left"]["phase"] = (rec["left"]["phase"] + 1) % 4 + self.assertNotEqual(N.recipe(N.ONE, rec), N.ONE) + + def test_monomial_phase_convention(self): + # Symmetric Q and strict-upper Q must encode the same quadratic form. + rows = [1 << i for i in range(9)] + upper = [0]*9 + upper[1] = 1 << 7 + symmetric = upper.copy() + symmetric[7] = 1 << 1 + linear = [0]*9 + key1 = tuple(rows), tuple(upper), tuple(linear), 0, 0 + key2 = tuple(rows), tuple(symmetric), tuple(linear), 0, 0 + self.assertEqual(N.mono(N.ONE, key1), N.mono(N.ONE, key2)) + expected = N.vector([-1 if i & 2 and i & 128 else 1 for i in range(512)]) + self.assertEqual(N.mono(N.ONE, key1), expected) + + def test_error_location_and_restoration(self): + response = V.witness(self.events) + initial = [Q(0)]*712 + earlier, _ = V.scalar_run(self.events, initial, (24434, Q(1))) + self.assertEqual(sum(bool(x) for x in earlier[224:704]), 102) + self.assertNotEqual(earlier, response) + with self.assertRaisesRegex(ValueError, "zero witness at residual boundary"): + V.scalar_run(self.events, initial, (24434, Q(1)), require_zero_wrappers=True) + + def test_exact_and_absolute_error_escapes(self): + response = V.witness(self.events) + for exponent in (0, 67, 256): + initial = [Q(0)]*712 + initial[112], initial[359] = Q(1), Q(2**exponent) + exact, cut = V.scalar_run(self.events, initial) + self.assertEqual(exact, initial) + self.assertEqual(cut, (-4*initial[359], initial[359])) + absolute, _ = V.scalar_run(self.events, initial, (V.FAULT, Q(1, 256))) + self.assertEqual(absolute, [x+q/256 for x, q in zip(initial, response)]) + self.assertEqual(max(abs(a-b) for a, b in zip(absolute[:224], exact[:224])), Q(1, 512)) + initial[359] = 0 + self.assertEqual(V.scalar_run(self.events, initial, (V.FAULT, Q(0)))[0], initial) + + def test_fault_binding_and_source_invalidation(self): + bad = deepcopy(self.packet) + bad["core_words"]["forward"][V.FAULT][1][3] = -4 + with self.assertRaisesRegex(ValueError, "fault event binding"): + V.expand(bad) + with tempfile.TemporaryDirectory() as d: + root = Path(d) + archive = root / "research/community-frontier1042-audit/selected-replay.tar.gz" + archive.parent.mkdir(parents=True) + archive.write_bytes(b"altered source") + with self.assertRaisesRegex(ValueError, "source pin"): + V.load(root) + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/qq16-native-dirty-fault/verify.py b/research/qq16-native-dirty-fault/verify.py new file mode 100644 index 0000000000..38a8f48016 --- /dev/null +++ b/research/qq16-native-dirty-fault/verify.py @@ -0,0 +1,326 @@ +#!/usr/bin/env python3 +"""Native binding of PR2995's F0 dirty-helper fault. Exact and read-only. + +Tekalign, with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from collections import Counter +from fractions import Fraction as Q +import gzip +import hashlib +import json +from pathlib import Path +import tarfile +import types + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +# Compile current local source directly; default-import bytecode is not used. +N = types.ModuleType("native_vectors") +exec(compile((HERE / "native.py").read_bytes(), str(HERE / "native.py"), "exec"), N.__dict__) +need = N.need +FAULT = 24438 +MEMBERS = { + "slots/local/CANONICAL-WORD.json.gz": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219", + "slots/local/CLIFFORD-RECIPES.json": "d0768f2164d5f64a2fdbec422f1cfde4e400818792f1904ca541958377243731", + "slots/local/RESIDUAL-ADAPTERS.json": "383f40aadd00a4ac700dfd0d4c22d6c6c0be9a9863116e4d69c7acd23bafae0c", +} + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def digest(value): + return hashlib.sha256(canonical(value)).hexdigest() + + +def load(root): + sources = json.loads((HERE / "SOURCES.json").read_text()) + for entry in sources["files"]: + if entry["usage"] == "input": + need(hashlib.sha256((root / entry["path"]).read_bytes()).hexdigest() == entry["sha256"], + "source pin: " + entry["path"]) + objects = [] + with tarfile.open(root / "research/community-frontier1042-audit/selected-replay.tar.gz") as archive: + for name, expected in MEMBERS.items(): + matches = [m for m in archive.getmembers() if m.name == name] + need(len(matches) == 1 and matches[0].isfile(), "unique regular source member") + raw = archive.extractfile(matches[0]).read() + need(hashlib.sha256(raw).hexdigest() == expected, "source member pin: " + name) + objects.append(json.loads(gzip.decompress(raw) if name.endswith(".gz") else raw)) + packet = json.loads(gzip.decompress((root / "research/joint-query/certificate.json.gz").read_bytes())) + return packet, *objects + + +def expand(packet): + need(packet["schema"] == "conserved-qq16-full-cover-native-words-v1", "packet schema") + result = [] + for event in packet["programs"]["F_0"]: + if event[0] == "retained_core": + need(event[1:3] == ["forward", 0], "stage-zero forward core") + result.extend(packet["core_words"]["forward"]) + elif event[0] in ("cover_sweep", "private_sweep"): + result.extend(event[2]) + else: + result.append(event) + need(len(result) == 26099 and len(packet["core_words"]["forward"]) == 25155, "event counts") + need(Counter(e[0] for e in result) == { + "scalar": 21025, "climb": 3486, "adapter": 1090, + "residual_adapter": 480, "phase": 10, "native_line": 8}, "complete event inventory") + need(result[FAULT] == ["scalar", ["add", ["L", 39], ["L", 359], 4, 1], 1], + "fault event binding") + return result + + +def reg(token): + need(isinstance(token, list) and len(token) == 2, "register token") + kind, index = token + need(type(index) is int and kind in ("L", "C"), "register type") + need(0 <= index < (704 if kind == "L" else 8), "register bounds") + return index + 704 * (kind == "C") + + +def scalar(state, gate): + kind, dst = gate[0], reg(gate[1]) + if kind == "clear": + need(dst >= 704 and len(gate) == 2, "owned CLEAR") + state[dst] = Q(0) + elif kind == "scale": + need(len(gate) == 4 and gate[2] != 0, "SCALE syntax") + state[dst] *= Q(gate[2], gate[3]) + else: + need(kind == "add" and len(gate) == 5, "ADD syntax") + src = reg(gate[2]) + need(src != dst, "distinct ADD operands") + state[dst] += Q(gate[3], gate[4]) * state[src] + + +def scalar_run(events, initial, inject=None, require_zero_wrappers=False): + state, cut = list(initial), None + for i, event in enumerate(events): + if i == FAULT: + cut = (state[39], state[359]) + if event[0] == "scalar": + scalar(state, event[1]) + elif event[0] == "residual_adapter" and require_zero_wrappers: + need(state[event[2]] == 0, "zero witness at residual boundary") + if inject is not None and i == inject[0]: + state[reg(event[1][1])] += inject[1] + return state, cut + + +def recipes_by_key(recipes): + children = {(r["old"], r["new"]): r for r in recipes["children"]} + adapters = {(r["role"], r["port"]): r for r in recipes["endpoint_adapters"]} + need(len(children) == len(recipes["children"]) and len(adapters) == 224, "unique recipes") + return children, adapters + + +def native_checks(packet, word, recipes, residuals): + """One exact vector per frame, not a claim about every operator column.""" + children, adapters = recipes_by_key(recipes) + events = packet["core_words"]["forward"] + frames = [N.frame(axes) for axes in word["frames"]] + need(frames[0] == frames[1] == N.ONE, "identity/full-frame constant") + used = sorted({tuple(e[3:]) for e in events if e[0] == "climb"}) + for a, b, rank in used: + child = children[a, b] + need(child["rank"] == rank, "child rank binding") + need(N.recipe(frames[a], child) == frames[b], "native frame-vector transition") + for (role, port), entry in adapters.items(): + index = port + 112 * (role == "target") + f = word["start"][index] if role == "source" else word["final"][index] + need(entry["frame"] == f and entry["rank"] == 0 and entry["right"] is None, + "endpoint adapter binding") + key = N.monomial_key(entry["left"]) + need(N.mono(N.ONE, key) == frames[f], "native endpoint frame vector") + need(N.mono(frames[f], key, True) == N.ONE, "endpoint inverse vector") + wrapped = {i for i in range(224, 704) if (word["start"][i], word["final"][i]) != (0, 1)} + wrapper_keys = set() + for i in wrapped: + a, b = word["start"][i], word["final"][i] + key = str(a) if b == 1 else f"{a}:{b}" + rec = residuals["recipes"][key] + need(rec["frame"] == a and rec.get("terminal", 1) == b, "residual binding") + N.monomial_key(rec["left"]) + N.monomial_key(rec["right"]) + wrapper_keys.add(key) + used_lines = sorted({e[2] for e in expand(packet) if e[0] == "native_line"}) + for key in used_lines: + entry = packet["native_line_recipes"][key] + need(entry["rank"] == entry["recipe"]["rank"] == 1, "wrapper line rank") + need(N.recipe(N.ONE, entry["recipe"]) == N.ONE, "native wrapper fixes constant") + # Extended boundary labels prevent treating an adapter as a harmless relabel. + labels = [("preS", i) if i < 112 else ("preW", i) if i in wrapped + else ("T", word["start"][i]) for i in range(704)] + [None] * 8 + conversions = Counter() + for event in events: + kind = event[0] + if kind == "phase": + continue # control labels, not scalar rotations + if kind == "climb": + _, _, i, a, b, _ = event + need(labels[i] == ("T", a), "child entry label") + labels[i] = ("T", b) + elif kind == "scalar": + gate, f = event[1:] + i = reg(gate[1]) + if gate[0] == "clear": + need(i >= 704, "private clear label") + labels[i] = ("T", f) + else: + need(labels[i] == ("T", f), "scalar target frame") + if gate[0] == "add": + need(labels[reg(gate[2])] == ("T", f), "scalar source frame") + elif kind == "adapter": + _, direction, i, f = event + conversions[direction, i] += 1 + if direction == "old_to_new": + need(f == word["start"][i], "entry frame binding") + need(labels[i] == (("preS", i) if i < 112 else ("T", 0)), "entry label") + labels[i] = ("T", f) + else: + need(direction == "new_to_old" and f == word["final"][i], "exit frame binding") + need(labels[i] == ("T", f), "exit label") + if 112 <= i < 224: + labels[i] = ("postT", i) + else: + need(f == 1, "identity exit frame") + elif kind == "residual_adapter": + direction, i, a = event[1:4] + b = event[4] if len(event) == 5 else 1 + need(i in wrapped and (a, b) == (word["start"][i], word["final"][i]), + "residual event binding") + conversions[direction, i] += 1 + if direction == "pre": + need(labels[i] == ("preW", i), "residual entry label") + labels[i] = ("T", a) + else: + need(direction == "post" and labels[i] == ("T", b), "residual exit label") + labels[i] = ("doneW", i) + else: + raise ValueError("unknown core event") + expected = Counter() + for i in range(704): + if i in wrapped: + expected["pre", i] = expected["post", i] = 1 + else: + expected["old_to_new", i] = 1 + if i < 224 or word["final"][i] == 1: + expected["new_to_old", i] = 1 + end = ("T", 1) if i < 112 or (i >= 224 and i not in wrapped) else ( + ("postT", i) if i < 224 else ("doneW", i)) + need(labels[i] == end, "complete native endpoint label") + need(conversions == expected and labels[704:] == [("T", 0)] * 8, "complete conversion multiplicity") + need((word["start"][359], word["final"][359]) == (0, 1), "dirty witness unwrapped") + return {"used_child_recipes": len(used), "child_occurrences": 3486, + "frame_vectors": len(frames), "frame_vector_sha256": digest(frames), + "used_edges_sha256": digest(used), "data_adapters": len(adapters), + "residual_records": len(wrapper_keys), "wrapper_lines": len(used_lines), + "scalar_frame_checks": 20089, "local_payload_coordinates": N.DIM} + + +def physical_run(events, packet, recipes, residuals, initial, inject=None): + """Literal vector execution, without frame reduction or scalar projection.""" + children, adapters = recipes_by_key(recipes) + state = [N.scaled(N.ONE, x) for x in initial] + cut = None + for index, event in enumerate(events): + if index == FAULT: + cut = state[39], state[359] + kind = event[0] + if kind == "scalar": + gate = event[1] + dst = reg(gate[1]) + if gate[0] == "clear": + state[dst] = N.ZERO + elif gate[0] == "scale": + state[dst] = N.scaled(state[dst], Q(gate[2], gate[3])) + else: + need(gate[0] == "add", "physical scalar kind") + state[dst] = N.plus(state[dst], N.scaled(state[reg(gate[2])], Q(gate[3], gate[4]))) + elif kind == "climb": + _, _, dst, old, new, _ = event + if state[dst] != N.ZERO: + state[dst] = N.recipe(state[dst], children[old, new]) + elif kind == "adapter": + _, direction, dst, _ = event + if direction == "old_to_new" and dst < 112: + state[dst] = N.mono(state[dst], N.monomial_key(adapters["source", dst]["left"])) + elif direction == "new_to_old" and 112 <= dst < 224: + state[dst] = N.mono(state[dst], N.monomial_key(adapters["target", dst-112]["left"]), True) + elif kind == "residual_adapter": + direction, dst, a = event[1:4] + b = event[4] if len(event) == 5 else 1 + key = str(a) if b == 1 else f"{a}:{b}" + part = "right" if direction == "pre" else "left" + state[dst] = N.mono(state[dst], N.monomial_key(residuals["recipes"][key][part]), True) + elif kind == "native_line": + dst = reg(event[1]) + state[dst] = N.recipe(state[dst], packet["native_line_recipes"][event[2]]["recipe"]) + else: + need(kind == "phase", "unknown physical event") + if inject is not None and index == inject[0]: + state[reg(event[1][1])] = N.plus(state[reg(event[1][1])], N.scaled(N.ONE, inject[1])) + return state, cut + + +def witness(events): + unit = lambda i: [Q(j == i) for j in range(712)] + dirty, data = unit(359), unit(112) + out_dirty, cut_dirty = scalar_run(events, dirty, require_zero_wrappers=True) + out_data, cut_data = scalar_run(events, data, require_zero_wrappers=True) + need(out_dirty == dirty and out_data == data, "ideal witness endpoints") + need(cut_dirty == (-4, 1) and cut_data == (0, 0), "marked cut coefficients") + response, _ = scalar_run(events, [Q(0)] * 712, (FAULT, Q(1)), require_zero_wrappers=True) + need(sum(bool(x) for x in response) == 52 and not any(response[224:]), "fault support/restoration") + need(set(abs(x) for x in response if x) == {Q(1, 2)} and response[2] == -Q(1, 2), "fault magnitude") + return response + + +def audit(root): + packet, word, recipes, residuals = load(root) + events = expand(packet) + bindings = native_checks(packet, word, recipes, residuals) + response = witness(events) + # The quantified theorem uses the frame identities, not extrapolation in T/u. + initial = [Q(0)] * 712 + initial[112], initial[359] = Q(1), Q(256) + u = Q(1, 2**20) + eta = 8 * u * initial[359] + expected = [x + eta*r for x, r in zip(initial, response)] + physical, cut = physical_run(events, packet, recipes, residuals, initial, (FAULT, eta)) + need(cut == (N.scaled(N.ONE, Q(-1024)), N.scaled(N.ONE, Q(256))), "literal physical cut") + need(physical == [N.scaled(N.ONE, x) for x in expected], "literal complete native witness") + return {"schema_version": 1, "status": "PASS_QQ16_NATIVE_DIRTY_FAULT", + "scope": "exact local native F0 and tensor/owner lift under retained access contract", + "expanded_events": len(events), "event_sha256": digest(events), + "native_binding": bindings, "fault_index": FAULT, + "unit_fault_response": [[i, str(x)] for i, x in enumerate(response) if x], + "dirty_register": 359, "original_data_register": 112, + "zero_residual_boundary_checks": 3*480, + "data_error": "4*u*T", "all_480_physical_helpers_restore_on_witness": True, + "all_8_private_outputs_zero": True, "local_relative_allowance": "8*u*T", + "literal_check": {"T": "256", "u": str(u), "eta": str(eta), + "max_data_error": str(4*u*256), "coordinates": 712*N.DIM}, + "meaning": "permissive completed-ADD fault, not a concrete rounding failure"} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--root", type=Path, default=ROOT) + parser.add_argument("--write", type=Path, help="create an absent receipt") + args = parser.parse_args() + result = audit(args.root.resolve()) + if args.write: + with args.write.open("x") as stream: + stream.write(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + need(json.loads((HERE / "RESULT.json").read_text()) == result, "result receipt mismatch") + print(result["status"]) + print("2880 native transitions; 26099 literal events; 364544 endpoint amplitudes.") + + +if __name__ == "__main__": + main()