diff --git a/research/qq16-streamed-decoder-format/README.md b/research/qq16-streamed-decoder-format/README.md new file mode 100644 index 0000000000..f0997fe26e --- /dev/null +++ b/research/qq16-streamed-decoder-format/README.md @@ -0,0 +1,290 @@ +# Independent native-frame and tensor checks for the QQ16 recovery format + +PR4109 already establishes the common finite format and producer composition +for PR4015 and its paired successor. This package independently rederives the +PR4015 baseline, binds it to raw native-frame data and ownership, and executes +the actual q=19 negative line on dense one- and two-factor arrays against a +separate translation-convolution oracle. It also reconciles two explicitly +different numeric counting protocols. No new format theorem or priority is +claimed. The domain is the literal **3,813-event, 224-output streamed word**, +including its nine reused output banks, native interiors and private lifetimes. + +For every integer tensor depth `lambda >= 1`, put `t=lambda-1`. If all 224 +borrowed current X/Y fields have Gaussian-dyadic components in `h Z`, uniformly +bounded in absolute value by `< 2^P h`, the decoder executes exactly with + +``` +q_decoder = h * 2^(-9-3t), W_decoder = P+28+6t. +``` + +Owned output banks are distinct from borrowed inputs and each other. Their +initial contents are discarded only by their literal paid CLEARs. Private F/G +fields are exclusively owned, initialized before use, and cleared to zero +before release. Scalar and native numerical scratch is disjoint and written +before use. The tensor-native, full-cover and functional decoder semantics are +the retained source contracts, not re-established by a capacity calculation. + +Composing with the authenticated PR3303 F0 -> B12 format, now let h and P refer +to its **original 704 persistent input fields**, including its dirty helpers; +its eight private fields enter zero. One common format for the producer and +this complete decoder is + +``` +q_total = h * 2^(-80-22t), W_total = P+242+44t. +``` + +This independently checks the consumer arithmetic conclusion: the represented +reference has zero producer and decoder arithmetic error on the declared lattice. It +does not supply an actual caller's input preparation, literal return of the +producer's dirty helper arrays, or a favorable physical/recursive invoice. +No supplier or kappa claim is made. + +## Sources, new contribution and ownership + +Original arithmetic baseline: `20ecf2891d80b5acf18d980b2164fb44ea7faa90`, +priority revision 6. Submission base is canonical main +`b58ad9ef4d4e861b0eaa5dba41742bdc072dca51`, priority revision 7. Its selected +conditional kappa is 0.00302015 from PR4470. Frozen scientific inputs remain unchanged. +The exact PR4015 source head is `0fff81d8997cef646538bcd4f60d7d455cf93b8e`; +the now-archived canonical WORD is a declared live input. PR4043 at +`aeeca9ffb50203b56924ee3f1325deab4029f4d9` originally identified the certificate +gap; PR4109 at `30dcf52a7722d0919e125f77a4fb921094578242` subsequently closed it +for both schedules and already supplied the same producer substitution. +PR3303's theorem, constants and numeric-reference invoice are inherited with +their original credit. Canonical data and proof pins are in `SOURCES.json`. + +The added evidence is a separately implemented raw native-geometry/phase/ +ownership traversal, all-cut arithmetic corroboration, dense nonconstant tensor +execution at the actual first negative line, and an explicit protocol-cost +reconciliation. PR4109's range, composition and paired-saving results retain +their credit; its paired candidate and approximate-error theorem are outside +this check. No predecessor executable is imported by the new scripts. + +Every write in the literal decoder is to an owned Z/W output or an active +private F/G field. All 224 borrowed current X/Y fields remain bitwise unchanged +in this numerical implementation. All 224 outputs finish in F17. The source's +legacy CLEAR name `wide` means **F17 in this normalized decoder**, not F25. +The independent phase traversal verifies all ADD boundaries with that binding. +These properties concern the consumer; they do not establish common-coordinate +return of all 480 original producer helpers. + +## Proof of the standalone format + +For `z=2^t >= 1`, associate a nonnegative rational polynomial p and integers +g,b with each nonzero field. Maintain + +``` +|component| <= 2^P h p(z), component belongs to h*2^(-g-bt) Z. +``` + +Known zero has an empty polynomial and no grid obligation. Borrowed entries +start with p=1, g=b=0. Owned fields have no usable value until their first +source CLEAR. The following rules apply to arbitrary correlated values: + +- ADD adds the two magnitude polynomials and takes the maximum of the two + grid intercepts and slopes. All literal coefficients are ±1 or ±1/4. + A signed coefficient product is computed before its destination ADD; the + copied source, sign change and exact division are included in the bounds. +- A private or owned CLEAR produces exact zero. It does not erase the already + recorded peak range or grid requirement. No borrowed field may be cleared. +- A signed native coordinate line on x=a+ib and y=c+id has outputs + `((a+c-e(b-d))+i(b+d+e(a-c)))/2` and + `((a+c+e(b-d))+i(b+d-e(a-c)))/2`, with e=±1. Pair sums/differences, + cross numerators and outputs have component bounds 2L, 4L and 2L. + The final halves refine the grid by one bit. +- Applying this line in all lambda tensor layers gives bounding observations + `2zp, 4zp, 2zp`, with grid `(g,b+1), (g,b+1), (g+1,b+1)`. + These bound every intermediate layer: before layer j, the magnitude grows + by at most `2^(j-1)` and the grid by j-1, where j<=lambda. +- The native basis wrappers are permutations, including the negative line's + affine offset q. Full-cover maps are owner/payload bijections and preserve + a component bound uniform over all owners. No owner is silently identified + with another. Scalars act once on a field, not once per tensor factor. + +Source induction through all 3,813 events and **10,336 primitive observations** +gives + +``` +max p(1) = 171043 < 2^18, max degree(p) = 3, +max grid intercept = 9, max grid slope = 3. +``` + +The range maximum is at event 3797, an ADD. The global maxima are conservative +capacity bounds, not optimal formats or demonstrated reachable extrema. +Nonnegative coefficients give `p(z) <= p(1) z^3`, so every component, product +and native numerator has magnitude `< 2^P h 2^(18+3t)`. In units of the proposed +q_decoder it is an integer of magnitude `< 2^(P+27+6t)`. Signed width +`P+28+6t` therefore suffices. Each right-shift result is on the common lattice, +so its numerator is divisible by the required power of two. Strict bounds +also make negation safe at both signed extremes. + +The checker derives the 224 stage/port owner maps from canonical phase data, +checks their complete 73-axis inverses, and verifies all frame transitions. +It checks 114,688 exact signed native basis columns for all 112 labels, including +both signs and the negative affine offset. These are source-bound primitive +checks; the full inverse identity is inherited from PR4015. + +## Composing the actual producer entry + +PR3303 gives, for the original input h and P, + +``` +h_D = h * 2^(-71-19t), +|each producer output component| < 2^P h * 2^(143+19t). +``` + +Thus the decoder's entry parameter may be chosen as +`P_D = P+214+38t`, since the latter magnitude is +`< 2^(P_D) h_D`. Substitute h_D and P_D into the standalone theorem: + +``` +h_D * 2^(-9-3t) = h * 2^(-80-22t), +P_D + 28 + 6t = P + 242 + 44t. +``` + +Execute the producer on this same finer lattice from the beginning; its +previous bounds also fit the enlarged signed width. No boundary rounding or +lossy conversion is needed. Producer current X/Y then enter the decoder +unchanged, and its owned output banks use the same format as its temporary +query sums. For `h=2^-64`, `P=64`, `lambda=1`, one sufficient whole-chain +format is **306-bit signed components on quantum 2^-144**. + +Under the inherited exact source semantics, all implemented producer and +decoder arithmetic defects are zero on this input domain, so the corresponding +completed-error allowances are met for any requested beta. Initial real-input +quantization, caller format admission and physical effects are not deleted by +that statement. The new decoder's exact functional identity is its own +predecessor theorem; the older PR2736 numerical theorem is not substituted for it. + +## Direct numerical bill + +Let `N=2^(73*lambda)` be complex payload coordinates per owner. The protocol +uses a W-bit signed component format throughout. Constant-product terms are +copied, conditionally negated, divided exactly by four when required, and +then added. Each native line pays both basis permutations using a reusable +complex buffer. One Gaussian coordinate line pays 4N real additions, +2N halvings and 4N component copies. Each cover pays 4N conceptual component +transfers separately. The inventory is 2,816 ADDs (1,172 negative, 896 quarter), +416 CLEARs, 224 native lines and 352 maps. + +| Decoder reference charge | W-bit operations per N | +|---|---:| +| Product copies | 5,632 | +| Signed negations | 2,344 | +| Exact quarter shifts | 1,792 | +| Destination additions | 5,632 | +| Owned/private clears | 832 | +| Two native permutation wrappers per line | 1,792 | +| Gaussian interiors and copies | 2,240 lambda | +| Final reusable buffer clear | 2 | + +There are also twelve final arithmetic-scratch zero writes. Therefore the +decoder reference bill is `(18026+2240 lambda)N+12` numeric operations, +`1408N` cover transfers and `930N+12` numeric words. The latter counts +224 borrowed inputs, 224 outputs, at most sixteen private fields, one complex +permutation/cover buffer and twelve scalar temporaries. + +Adding the inherited producer bill without credit for eliminating either +boundary cleanup gives the entire numerical reference: + +``` +work: (390348 + 113000 lambda) N + 24 W-bit numeric operations, +covers: 3520 N conceptual component transfers, +storage: 1890 N + 12 W-bit numeric words. +``` + +The storage bound retains all 704 original persistent producer fields, +including the 480 borrowed helpers; adds 224 recovery outputs; reuses at most +sixteen private fields and one complex buffer. It assumes these logical fields +can be supplied disjointly; it is not a physical placement construction. Code, +address/sign/control work, tape-head motion, representation adapters and +recursive tariffs remain separate costs. No favorable supplier moment follows. + +PR4109 uses a different protocol: signed ADD/subtraction is one operation, its +constant term is not separately copied, each monomial allows 2N sign operations, +cover copies are included in the numeric total, and it reports no final buffer +clear. Recounting that convention from the same WORD gives its published +`(12352+2240 lambda)N` baseline. Our unfused convention, with cover transfers +included for comparison, gives `(19434+2240 lambda)N+12`. The difference is +exactly `7082N+12`: 5632N term copies + 2344N explicit negations - 896N +unnecessary sign allowances for these pure-permutation wrappers + 2N+12 final +scratch clearing. Both are constructive upper protocols, not conflicting +minimum-cost claims or a new speedup. The verifier records and independently +recounts both conventions; mixing them would manufacture a false saving. + +## Verification and reproduction + +Python 3.12 standard library, from the repository root: + +```sh +python3.12 -I -Werror -B research/qq16-streamed-decoder-format/verify.py +python3.12 -I -O -Werror -B research/qq16-streamed-decoder-format/independent.py +python3.12 -I -O -Werror -B research/qq16-streamed-decoder-format/test_format.py +python3.12 scripts/research_package.py --package research/qq16-streamed-decoder-format +``` + +The primary polynomial interpreter authenticates inputs before parsing. The +separate integer/dyadic recurrence imports no primary or predecessor code and +matches all 10,336 one-layer observations; it explicitly repeats native layers +at depths 1,2,3,8,32 and independently checks the reference bill and composition. +The observed grid guards are 9,12,15,30,102. The all-depth theorem comes from +the preceding induction, not extrapolation from these depths. + +Six behavioral groups check 1,250 signed Gaussian pairs, an off-grid half, +an overflowing intermediate with fitting endpoints, the actual source's +ownership/frame mutations, and width/storage substitution. Complete fixed-grid +executions at depths 1,2,8 check all 3,808 changed-field cuts per run on arbitrary +independently chosen complex constants in each borrowed field. Uniformity over +owners and payload coordinates makes these valid source inputs: both signs of +C_q and all cover maps fix constants. The native pair interiors are still +executed and compared against a separate Fraction formula. This is explicitly +a constant-payload control, not a huge-payload execution or a full functional +decoder proof. Independent general primitive checks and induction supply the +capacity guarantee for arbitrary bounded input arrays. + +The additional group binds actual event 1707 (`Z10`, negative q=19) to dense +512- and 262,144-coordinate inputs with independent complex components, for +one and two nine-axis tensor factors. Bounded integer pair-first execution +agrees at every endpoint with a separately expanded sum of 2^lambda translated +inputs. The inverse returns the entire input exactly and the source arrays +remain unchanged. These are the actual local native factors, with identity +spectators omitted, not a full O73 owner-cover or whole-decoder dense run. + +The unchanged PR4015 primary checker was also freshly run under isolated, +optimized, warning-strict Python 3.12: `PASS_QQ16_HOSTED_STREAMING_RECOVERY`. +That is replay of its credited functional/native/ownership certificate, not +an independently invented decoder or human/formal-kernel review. + +## Open next questions + +The October 22 refresh changes the next task. PR4166, retained at +`0b082d22a0e9a442d264ab0633e35ef26c790630`, now proposes an actual installed +caller with encoded acquisition, borrowed-state checks and current-frame +publication. It is author-checked source evidence, not independently replayed +here. Its required current endpoint is G(x,y)=(-y,x+y), rather than merely +recovered original inputs. Earlier PR4105 also distinguishes the first pair's +two helper banks (intersection 40, union 920). The 704-field literal producer +reference and the 1890N+12 storage subtotal above are therefore **not** that +installation's actual physical allocation. + +Revision 7 narrows the next decision to a matched whole-root protocol price or +a changed source-compatible demand. Retain original parent parking/restore, +external Machine.run copying/root return, descendant contexts and all later +root calls. Equal child ranks or outputs do not justify cancelling different +protocols. This package does not supply that comparison, actual tape tariffs, +or admission into the selected PR4470 joint-helper construction. +Another guard refinement is not the missing step. The earlier PR4042/4047 +layout/lease audits retain their scoped credit; their old open-task wording +must not be used to ignore the later installation. + +## Credit + +Nicholas Stone, substantial OpenAI Codex assistance; Apache-2.0. Chris R / +Clear1nsight's PR4015 supplies the streamed decoder and output-bank lifetimes; +PR4043 supplies the original finite-format handoff, and PR4109 establishes +the same format, producer composition and a paired-saving comparison. Nick Petalas's PR3303/3270 +and the independent PR3652 check supply the producer envelope. Credit +commdata2338/PR3226/3235, ywz65/PR2707, Arham Tahir/PR2681, Sricharan Vagvala's +pair-first Gaussian reference, Ali Romman and the retained QQ16/native/geometry +lineage. Their source files and claims are preserved unchanged. This result +is an independent check; no new format theorem, kappa or scientific admission is claimed. diff --git a/research/qq16-streamed-decoder-format/RESULT.json b/research/qq16-streamed-decoder-format/RESULT.json new file mode 100644 index 0000000000..518417dd2e --- /dev/null +++ b/research/qq16-streamed-decoder-format/RESULT.json @@ -0,0 +1,63 @@ +{ + "borrowed_unchanged": 224, + "checkpoints": [ + [ + 2730, + "23733" + ] + ], + "composed_cover_transfers_per_N": 3520, + "composed_grid_intercept": 80, + "composed_grid_slope": 22, + "composed_numeric_storage_per_N": 1890, + "composed_width_offset": 242, + "composed_width_slope": 44, + "composed_wordops_constant": 24, + "composed_wordops_per_N": [ + 390348, + 113000 + ], + "counts": { + "add": 2816, + "begin": 2, + "checkpoint": 1, + "clear": 416, + "end": 2, + "line": 224, + "map": 352, + "negative_ADD": 1172, + "quarter_ADD": 896 + }, + "decoder_cover_transfers_per_N": 1408, + "decoder_numeric_storage_per_N": 930, + "decoder_wordops_constant": 12, + "decoder_wordops_per_N": [ + 18026, + 2240 + ], + "events": 3813, + "grid_intercept": 9, + "grid_slope": 3, + "native_basis_columns": 114688, + "new_supplier_or_kappa": false, + "observations": 10336, + "one_layer_capacity_sha256": "f3002f6b0ba9f2fd3dea868f537668bf19485fa8be4b71ebc640e48f9d930ae3", + "output_banks": 224, + "owner_maps_checked": 224, + "peak_polynomial_at_one": "171043", + "peak_site": [ + 3797, + "add" + ], + "polynomial_degree": 3, + "pr4109_fused_reference_fixed_with_covers_per_N": 12352, + "private_peak": 16, + "protocol_difference_fixed_per_N": 7082, + "range_bits": 18, + "scratch_scalar_words": 12, + "standalone_width_offset": 28, + "standalone_width_slope": 6, + "status": "PASS_QQ16_STREAMED_DECODER_FORMAT", + "trace_sha256": "2868966e944a732754e5727535717054e3165c2874453e3a603d0da9725d7319", + "unfused_reference_fixed_with_covers_per_N": 19434 +} diff --git a/research/qq16-streamed-decoder-format/SOURCES.json b/research/qq16-streamed-decoder-format/SOURCES.json new file mode 100644 index 0000000000..71d49000a1 --- /dev/null +++ b/research/qq16-streamed-decoder-format/SOURCES.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5" + }, + { + "path": "research/community-frontier1042-audit/selected-replay.tar.gz", + "usage": "input", + "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + "git_blob": "6f4dc6fe7631d8aacf8081fcaecf32197181685b" + }, + { + "path": "research/qq16-all-depth-producer-grid/RESULT.json", + "usage": "input", + "sha256": "b954ab5c5a720b21a9ab49bda2e1a0824ab184a482243d6263dab3c4bddb91bb", + "git_blob": "372809009d835ce707eace8d514a667f2301b1d8" + }, + { + "path": "research/qq16-all-depth-producer-grid/PROOF.md", + "usage": "input", + "sha256": "6dd878aa01807eecf4a37f7ce3fbc1105d79f6b1b06791b23d4deeef90b7d994", + "git_blob": "9cf1ec57646fb760fd26f206d754e52c99c347e3" + }, + { + "path": "research/qq16-line-normalized-decoder/verify.py", + "usage": "provenance", + "git_blob": "a8f3c811108414eda0b507d295cfc9301c04d585", + "sha256": "0f6fb86aafb74b9722f20cc97af70a3a3c78bd012c142b2eaa19cb00e02d1fe9" + }, + { + "path": "research/qq16-streaming-recovery/WORD.json", + "usage": "input", + "pin": "head:f626db5c3a3d781d8f7695038776c621651f75e1:research/qq16-streaming-recovery/WORD.json", + "git_blob": "9a57a6f9c2fd8cdc4e5934408d78ef54e5f266b6", + "sha256": "272d8c1bd172c29044eb227ec6d67a882501250978234685e035158f4479aa58" + }, + { + "path": "research/qq16-streaming-recovery/PROOF.md", + "usage": "provenance", + "pin": "head:f626db5c3a3d781d8f7695038776c621651f75e1:research/qq16-streaming-recovery/PROOF.md", + "git_blob": "8fd64e85e3e595403fe3ae4ed60b9ff368c9a3f5", + "sha256": "81f0fa19b19fa7302ba9c61f4f1b2e11758f973b964240ba48c16ae9b6997396" + }, + { + "path": "research/qq16-paired-precision/RESULT.json", + "usage": "input", + "pin": "head:f626db5c3a3d781d8f7695038776c621651f75e1:research/qq16-paired-precision/RESULT.json", + "git_blob": "ab94eda14424220145dbe5c172d70db482a3418f", + "sha256": "f5dcaa599862d60493a1a9a9fcdd5bbfaf814d2cb426d2aa1bcff8183fb6d7bf" + }, + { + "path": "research/qq16-paired-precision/cost-proof.md", + "usage": "provenance", + "pin": "head:f626db5c3a3d781d8f7695038776c621651f75e1:research/qq16-paired-precision/cost-proof.md", + "git_blob": "8ac76aee17f520bde1d72b73293b2950947a318a", + "sha256": "b6c27163ed4c1e20d8f999c8ed1d481ad266cea4834090167c77232a8f7ce998" + }, + { + "path": "research/qq16-caller-install/README.md", + "usage": "provenance", + "pin": "head:f626db5c3a3d781d8f7695038776c621651f75e1:research/qq16-caller-install/README.md", + "git_blob": "d1d42d5e494f22a9db6da8ae4539d9edf2165334", + "sha256": "b781f1cd3ff625c5cf1264f8cf61f9b4413ea3516e35b3984d816bbf45b25fdc" + } + ], + "predecessors": [ + { + "source_path": "research/qq16-streaming-recovery/WORD.json", + "head": "0fff81d8997cef646538bcd4f60d7d455cf93b8e", + "sha256": "272d8c1bd172c29044eb227ec6d67a882501250978234685e035158f4479aa58", + "git_blob": "9a57a6f9c2fd8cdc4e5934408d78ef54e5f266b6", + "credit": "Chris R / Clear1nsight, with OpenAI assistance; PR4015 and retained QQ16 lineage", + "license": "Apache-2.0" + }, + { + "source_path": "research/qq16-streaming-recovery/PROOF.md", + "head": "0fff81d8997cef646538bcd4f60d7d455cf93b8e", + "sha256": "81f0fa19b19fa7302ba9c61f4f1b2e11758f973b964240ba48c16ae9b6997396", + "git_blob": "8fd64e85e3e595403fe3ae4ed60b9ff368c9a3f5", + "credit": "Chris R / Clear1nsight, with OpenAI assistance; PR4015 and retained QQ16 lineage", + "license": "Apache-2.0" + } + ] +} diff --git a/research/qq16-streamed-decoder-format/TASK.json b/research/qq16-streamed-decoder-format/TASK.json new file mode 100644 index 0000000000..89ef05f137 --- /dev/null +++ b/research/qq16-streamed-decoder-format/TASK.json @@ -0,0 +1,139 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "priority_revision": 6, + "task_id": "joint-query-controller", + "original_card": { + "id": "joint-query-controller", + "question": "Can a literal QQ16 producer meet the proposed completed-output error budgets with dirty helpers and an affordable physical consumer?", + "starting_points": [ + "docs/research/research-family-status.md", + "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", + "research/qq16-producer-defect-transfer/README.md" + ], + "methods": [ + "Derive one literal producer's completed-output defects and intermediate dirty-helper bounds, with its physical bill.", + "Design or audit one consumer, retention or hosting boundary and its complete cost for the pinned producer/decoder." + ], + "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. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the revision-6 family record and #2965 producer-defect transfer after the local QQ16 decoder contract. Its author-checked output-error estimate does not implement producer interiors, bound dirty helpers, or pay for the consumer; independently check the implication used.", + "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": "Pin one literal F0/B1 producer and its native-child contracts; derive the actual intermediate magnitude ledger and completed-output defects, including dirty helpers and correlations. Compare with #2965 budgets and price storage, movement, cleanup and F17 consumption. Stop with a precise missing bound if no producer contract supplies it; do not optimize another decoder precision constant in isolation.", + "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.", + "One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain." + ], + "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.", + "Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise.", + "Treating a completed-output defect inequality as a producer-interior, dirty-range or physical-cost certificate." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969", + "2540", + "early record", + "output-bank retention", + "complete native decoder", + "2965", + "producer defect", + "dirty-helper range", + "F17 consumer" + ] + }, + "scope_status": "refined", + "scope_change_reason": "The continued October19 local format derivation overlaps the now-published PR4109 theorem, including producer substitution. Submission is refined to independent source/native execution verification and protocol reconciliation, with full attribution and no new-format priority claim.", + "actual_scope": "Independently bind the archived PR4109/4015 baseline format to raw native geometry, phase/ownership transitions and dense tensor execution; reconcile explicitly different numeric protocols.", + "bottleneck_link": "Verifies the baseline numerical primitive contract without silently transporting it to the later installed caller or cancelling differently implemented costs.", + "stop_rule": "Finish this independent certificate and focused submission. The next family decision requires matched whole-caller pricing, not another guard optimization.", + "outcome": "completed", + "evidence": "Registered CPython3.12 replay passes: raw source phase/ownership and114688 native columns; independent all-cut integer/dyadic recurrence; dense actual q19 tensor arithmetic at512/262144 coordinates against translation convolution; six controls; explicit fused/unfused bill reconciliation.", + "author": "Nicholas Stone", + "ai_assistance": "Substantial OpenAI Codex assistance; separate code/arithmetic checks, not independent human or formal-kernel review.", + "open_questions": [ + { + "question": "Does the installed PR4166 caller win after matching its entire original and external protocols?", + "why_it_matters": "The native-component profile loses, while parent parking/restore on retained calls may provide compensating credit. A standalone component format or storage count cannot decide that comparison.", + "first_step": "Bind actual bank/packet geometries, retain descendant contexts and all later root calls, and compare matched parking, external call, return, routing, recovery and retirement costs.", + "blocked_by": "A complete matched protocol price and compatibility with the newly selected changed recursive interface are not proved here." + } + ], + "overlap": { + "searched_at": "2026-10-22T12:15:22.130499+00:00", + "coverage": { + "local": { + "head": "201e5b59320ff623f98faa9d96924f80ad786279", + "records": 281, + "head_records": 5862, + "complete_head_inventory": false + }, + "open_prs": { + "fetched_at": "2026-10-22T12:09:57.657270+00:00", + "complete_pagination": true, + "records": 404 + }, + "discussions": { + "fetched_at": "2026-10-22T12:11:20.592600+00:00", + "complete_pagination": true, + "records": 3573 + } + }, + "matches_total": 15, + "warnings": [ + "local: 5581 HEAD note paths were not searched; inspect coverage.local.unsearched_head_paths in --json output and materialize relevant notes before treating a lack of matches as evidence.", + "open_prs: offline; cached data may miss current changes", + "discussions: offline; cached data may miss current changes" + ], + "limits": "QQ16 local notes materialized; unrelated sparse notes omitted. Full cached open-PR and Discussion pagination, targeted merged-PR searches and latest named heads inspected; no novelty certificate.", + "assessment": "PR4109 already proves the same format and composition. Retain credit; added raw-geometry/phase binding, dense two-factor integer execution and explicit protocol reconciliation are deliberate independent evidence.", + "related_heads": { + "4015": "0fff81d8997cef646538bcd4f60d7d455cf93b8e", + "4109": "30dcf52a7722d0919e125f77a4fb921094578242", + "4166": "0b082d22a0e9a442d264ab0633e35ef26c790630" + } + }, + "family_decision": "Preserve independently verified numerical reference evidence and stop this line. Use revision7 matched-caller pricing before any implementation expansion.", + "verification": { + "python": "3.12.13 (main, Mar 3 2026, 15:35:03) [Clang 21.1.4 ]", + "new_registered_replay": "PASS_REGISTERED_RESEARCH_PACKAGE outcome=completed", + "predecessor_primary": "PASS_QQ16_HOSTED_STREAMING_RECOVERY", + "primitive_observations": 10336, + "gaussian_signed_basis_columns": 114688, + "owner_maps": 224, + "full_word_constant_payload_runs": 3, + "changed_field_cuts_per_run": 3808, + "controls": 6, + "full_huge_payload_execution": false, + "human_or_formal_kernel_review": false, + "dense_native_coordinate_counts": [ + 512, + 262144 + ], + "final_registered_replay": "PASS_REGISTERED_RESEARCH_PACKAGE outcome=completed" + }, + "freshness": { + "checked_at_utc": "2026-10-22T17:02:39.419836+00:00", + "canonical_main": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "priority_revision": 7, + "selected_kappa": "0.00302015", + "scientific_baseline": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "relevant_change": "Final submission refresh: selected PR4470 is a changed joint-helper interface; pinned arithmetic/word/geometry inputs and applicable package tooling are unchanged. PR4109 format/composition priority and later PR4166 caller scope are explicitly retained." + } +} diff --git a/research/qq16-streamed-decoder-format/VERIFY.json b/research/qq16-streamed-decoder-format/VERIFY.json new file mode 100644 index 0000000000..026edbad5e --- /dev/null +++ b/research/qq16-streamed-decoder-format/VERIFY.json @@ -0,0 +1,50 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1042-audit/selected-replay.tar.gz", + "research/qq16-all-depth-producer-grid/RESULT.json", + "research/qq16-all-depth-producer-grid/PROOF.md", + "research/qq16-streaming-recovery/WORD.json", + "research/qq16-paired-precision/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 90, + "checks": "Literal word, full phase/ownership ledger, signed kernels, polynomial all-depth primitive envelope and exact receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 90, + "checks": "Separate explicit-depth integer/dyadic magnitude and grid recurrence, every completed event and numeric invoice." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_format.py" + ], + "timeout_seconds": 120, + "checks": "Exact primitive controls, actual q=19 negative line on 512 and 262144 nonconstant tensor coordinates, full-word constant-payload executions, ownership/frame mutations and composition." + } + ] +} diff --git a/research/qq16-streamed-decoder-format/independent.py b/research/qq16-streamed-decoder-format/independent.py new file mode 100644 index 0000000000..f2d10d9fca --- /dev/null +++ b/research/qq16-streamed-decoder-format/independent.py @@ -0,0 +1,158 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Separate explicit-depth integer/dyadic capacity recurrence. No primary imports.""" +from collections import Counter +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def check(ok, msg): + if not ok: + raise ValueError(msg) + + +def reduce(n, e): + if not n: + return 0, 0 + while e > 0 and n % 2 == 0: + n //= 2 + e -= 1 + return n, e + + +def add(a, b): + e = max(a[1], b[1]) + return reduce((a[0] << (e-a[1])) + (b[0] << (e-b[1])), e) + + +def times(a, n, e=0): + return reduce(a[0]*n, a[1]+e) + + +def text(a): + return str(a[0]) if a[1] == 0 else str(a[0]) + "/" + str(1 << a[1]) + + +def greater(a, b): + return (a[0] << b[1]) > (b[0] << a[1]) + + +def read_word(): + pins = json.loads((HERE / "SOURCES.json").read_text()) + for row in pins["files"]: + if row["usage"] == "input": + check(hashlib.sha256((ROOT/row["path"]).read_bytes()).hexdigest() == row["sha256"], + "input authentication") + raw = (ROOT / "research/qq16-streaming-recovery/WORD.json").read_bytes() + return json.loads(raw) + + +def run(word, depth): + check(type(depth) is int and depth >= 1, "positive depth") + fields = {s+str(i): ((1, 0), 0) for s in ("X", "Y") for i in range(112)} + owned = {s+str(i) for s in ("Z", "W") for i in range(112)} + active = set() + highest, guard, trace = (1, 0), 0, [] + + def see(i, label, pair): + nonlocal highest, guard + value, g = pair + if greater(value, highest): + highest = value + guard = max(guard, g if value[0] else 0) + trace.append([i, label, text(value), g if value[0] else 0]) + + for i, event in enumerate(word): + kind = event[0] + if kind == "begin": + check(not active, "private overlap") + active = {s+str(j) for s in ("F", "G")[:event[2]//8] for j in range(8)} + elif kind == "end": + check(all(fields.get(n) == ((0, 0), 0) for n in active), "private return") + for n in active: + del fields[n] + active = set() + elif kind == "checkpoint": + check(not active, "private checkpoint") + else: + target = event[1] + check(target in owned | active, "borrowed write") + if kind == "clear": + fields[target] = ((0, 0), 0) + see(i, "clear", fields[target]) + elif kind == "add": + source = event[2] + check(source != target and source in fields and target in fields, "ADD input") + c = event[3] + check(c in ("1", "-1", "1/4", "-1/4"), "scalar") + quarter = 2 if "/" in c else 0 + magnitude, g = fields[source] + see(i, "product-copy", fields[source]) + term = (times(magnitude, 1, quarter), g+quarter) if magnitude[0] else ((0, 0), 0) + see(i, "product-result", term) + old, go = fields[target] + grid = max(go, term[1]) if old[0] and term[0][0] else go if old[0] else term[1] + fields[target] = add(old, term[0]), grid + see(i, "add", fields[target]) + elif kind == "map": + check(not active and target in fields, "map input") + see(i, "cover-map", fields[target]) + elif kind == "line": + check(not active and target in fields, "line input") + see(i, "right-monomial", fields[target]) + for _ in range(depth): + value, g = fields[target] + see(i, "native-pair", (times(value, 2), g)) + see(i, "native-cross", (times(value, 4), g)) + fields[target] = (times(value, 2), g+1) if value[0] else ((0, 0), 0) + see(i, "native-output", fields[target]) + see(i, "left-monomial", fields[target]) + else: + raise ValueError("unknown operation") + check(not active and all(n in fields for n in owned), "complete outputs") + digest = hashlib.sha256(json.dumps(trace, sort_keys=True, separators=(",", ":")).encode()).hexdigest() + return highest, guard, len(trace), digest + + +def main(): + word = read_word() + receipt = json.loads((HERE / "RESULT.json").read_text()) + expected_counts = Counter(e[0] for e in word) + check(all(receipt["counts"][k] == v for k, v in expected_counts.items()), "event inventory") + for depth in (1, 2, 3, 8, 32): + peak, guard, count, digest = run(word, depth) + check(guard == 9+3*(depth-1), "depth grid") + check(not greater(peak, (171043 << (3*(depth-1)), 0)), "polynomial range") + if depth == 1: + check(text(peak) == receipt["peak_polynomial_at_one"] and count == receipt["observations"], + "one-layer capacity") + check(digest == receipt["one_layer_capacity_sha256"], "every one-layer observation") + print("depth", depth, "guard", guard, "range", text(peak), "observations", count) + # Independent inventory of the declared direct numeric protocol. + adds = sum(e[0] == "add" for e in word) + neg = sum(e[0] == "add" and e[3].startswith("-") for e in word) + quarter = sum(e[0] == "add" and "/" in e[3] for e in word) + fixed = 2*adds + 2*adds + 2*neg + 2*quarter + 2*expected_counts["clear"] + fixed += 2*expected_counts["line"]*4 + 2 + check([fixed, 10*expected_counts["line"]] == receipt["decoder_wordops_per_N"], "numeric bill") + fused = 2*adds + 2*quarter + 2*expected_counts["clear"] + fused += 12*expected_counts["line"] + 4*expected_counts["map"] + check(fused == receipt["pr4109_fused_reference_fixed_with_covers_per_N"] == 12352, + "published fused protocol") + check(fixed+4*expected_counts["map"]-fused == receipt["protocol_difference_fixed_per_N"] == 7082, + "explicit protocol difference") + p = json.loads((ROOT/"research/qq16-all-depth-producer-grid/RESULT.json").read_text()) + check(p["grid_intercept_at_one"] + 9 == receipt["composed_grid_intercept"], "composed grid") + check(p["range_bits_at_one"] + p["grid_intercept_at_one"] + 9 + 18 + 1 + == receipt["composed_width_offset"], "composed signed width") + check(p["range_slope"] + p["grid_slope"] + 3 + 3 == receipt["composed_width_slope"], + "composed width slope") + print("PASS_QQ16_DECODER_EXPLICIT_DEPTHS_AND_NUMERIC_BILL") + + +if __name__ == "__main__": + main() diff --git a/research/qq16-streamed-decoder-format/test_format.py b/research/qq16-streamed-decoder-format/test_format.py new file mode 100644 index 0000000000..6ec33bbaec --- /dev/null +++ b/research/qq16-streamed-decoder-format/test_format.py @@ -0,0 +1,211 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact-grid controls, dense tensor-native and full-word constant executions.""" +import copy +from fractions import Fraction as Q +import importlib.util +import json +from pathlib import Path +import random +import sys +import unittest + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("format_primary", HERE/"verify.py") +V = importlib.util.module_from_spec(spec) +sys.modules[spec.name] = V +spec.loader.exec_module(V) + + +class Fixed: + def __init__(self, width): + self.width = width + + def fit(self, x): + if not -(1 << (self.width-1)) <= x < (1 << (self.width-1)): + raise ArithmeticError("intermediate overflow") + return x + + def divide(self, x, d): + self.fit(x) + q, r = divmod(x, d) + if r: + raise ArithmeticError("off-grid division") + return self.fit(q) + + def add(self, a, b): + return self.fit(a+b) + + def gaussian(self, x, y, sign): + a, b = x; c, d = y + sr, si = self.add(a, c), self.add(b, d) + dr, di = self.add(a, -c), self.add(b, -d) + numerators = (self.add(sr, -sign*di), self.add(si, sign*dr), + self.add(sr, sign*di), self.add(si, -sign*dr)) + out = tuple(self.divide(n, 2) for n in numerators) + return out[:2], out[2:] + + +def gaussian_oracle(x, y, sign): + # Direct complex linear combination, separate from pair-first additions. + a, b = map(Q, x); c, d = map(Q, y) + return ((a-sign*b+c+sign*d)/2, (b+sign*a+d-sign*c)/2), \ + ((c-sign*d+a+sign*b)/2, (d+sign*c+b-sign*a)/2) + + +def tensor_fixed(real, imag, label, sign, depth, width): + """Pair-first array execution on actual nine-axis factors and one owned buffer.""" + f = Fixed(width) + real, imag = real[:], imag[:] + for layer in range(depth): + axis = label << (9*layer) + rr, ii = [0]*len(real), [0]*len(real) + for x in range(len(real)): + y = x ^ axis + if x < y: + a, b = f.gaussian((real[x],imag[x]),(real[y],imag[y]),sign) + rr[x], ii[x] = a + rr[y], ii[y] = b + real, imag = rr, ii + return real, imag + + +def convolution_oracle(real, imag, label, sign, depth): + """Expand tensor C directly as a sum of 2^depth translations, not butterflies.""" + terms = [(0,1,0)] + for layer in range(depth): + result = [] + for shift,a,b in terms: + for delta,c,d in ((0,1,sign),(label << (9*layer),1,-sign)): + result.append((shift ^ delta,a*c-b*d,a*d+b*c)) + terms = result + rr, ii = [], [] + for x in range(len(real)): + a = sum(c*real[x^shift]-d*imag[x^shift] for shift,c,d in terms) + b = sum(d*real[x^shift]+c*imag[x^shift] for shift,c,d in terms) + u, ur = divmod(a,1 << depth);v,vr=divmod(b,1 << depth) + if ur or vr: + raise ArithmeticError("oracle denominator") + rr.append(u);ii.append(v) + return rr, ii + + +class Controls(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.word, data = V.load() + cls.labels, cls.maps, _ = V.geometry(data) + + def test_all_small_gaussian_pairs(self): + f = Fixed(16) + count = 0 + for a in range(-2, 3): + for b in range(-2, 3): + for c in range(-2, 3): + for d in range(-2, 3): + for sign in (-1, 1): + actual = f.gaussian((2*a, 2*b), (2*c, 2*d), sign) + want = gaussian_oracle((a,b),(c,d),sign) + self.assertEqual(tuple(tuple(Q(z,2) for z in pair) for pair in actual), want) + count += 1 + self.assertEqual(count, 1250) + + def test_native_numerator_and_grid_failures(self): + with self.assertRaises(ArithmeticError): + Fixed(20).gaussian((1,0),(0,0),1) + self.assertEqual(Fixed(20).gaussian((2,0),(0,0),1), ((1,1),(1,-1))) + # All final outputs fit signed four-bit words, but a numerator is 12. + self.assertEqual(gaussian_oracle((3,-3),(3,3),1), ((Q(6),Q(0)),(Q(0),Q(0)))) + with self.assertRaises(ArithmeticError): + Fixed(4).gaussian((3,-3),(3,3),1) + + def test_actual_negative_line_on_dense_tensor_inputs(self): + self.assertEqual(self.word[1707],["line","Z10",1,-1]) + self.assertEqual(self.labels[1],19) + for depth in (1,2): + size=1 << (9*depth);guard=9+3*(depth-1);width=3+28+6*(depth-1) + rng=random.Random(4015+depth) + real=[rng.randrange(-7,8)*(1 << guard) for _ in range(size)] + imag=[rng.randrange(-7,8)*(1 << guard) for _ in range(size)] + before=(real[:],imag[:]) + got=tensor_fixed(real,imag,19,-1,depth,width) + self.assertEqual(got,convolution_oracle(real,imag,19,-1,depth)) + self.assertEqual((real,imag),before) + self.assertEqual(tensor_fixed(*got,19,1,depth,width),before) + + def test_full_word_constant_payload_arithmetic(self): + # These are actual owner/payload-constant inputs: cover permutations + # and both signed C_q fix constants. Native interiors are still run. + # No general huge-payload execution is inferred from this subspace. + for depth, seed in ((1, 17), (2, 31), (8, 47)): + rng = random.Random(seed) + guard, width = 9+3*(depth-1), 3+28+6*(depth-1) + unit = 1 << guard + fixed = Fixed(width) + exact = {s+str(j): (Q(rng.randrange(-7,8)),Q(rng.randrange(-7,8))) + for s in ("X","Y") for j in range(112)} + bits = {n:tuple(int(x)*unit for x in z) for n,z in exact.items()} + original = dict(bits) + active = set() + changed = 0 + for event in self.word: + op = event[0] + if op == "begin": + active = {s+str(j) for s in ("F","G")[:event[2]//8] for j in range(8)} + elif op == "end": + self.assertTrue(all(bits[n] == (0,0) for n in active)) + for n in active: + del bits[n], exact[n] + active = set() + elif op == "checkpoint": + self.assertFalse(active) + else: + n = event[1] + if op == "clear": + bits[n],exact[n] = (0,0),(Q(0),Q(0)) + elif op == "add": + c = Q(event[3]);src=event[2] + term = tuple(fixed.divide(fixed.fit(c.numerator*x),c.denominator) for x in bits[src]) + bits[n] = tuple(fixed.add(a,b) for a,b in zip(bits[n],term)) + exact[n] = tuple(a+c*b for a,b in zip(exact[n],exact[src])) + elif op == "line": + for _ in range(depth): + out = fixed.gaussian(bits[n],bits[n],event[3]) + want = gaussian_oracle(exact[n],exact[n],event[3]) + self.assertEqual(out[0],out[1]) + bits[n],exact[n] = out[0],want[0] + else: + self.assertEqual(op,"map") + self.assertEqual(tuple(Q(x,unit) for x in bits[n]),exact[n]) + changed += 1 + self.assertEqual(changed,3808) + self.assertTrue(all(bits[n] == z for n,z in original.items())) + self.assertEqual(sum(n[0] in "ZW" for n in bits),224) + + def test_source_ownership_and_frame_mutants(self): + w = copy.deepcopy(self.word) + w.insert(0,["clear","X0","current"]) + with self.assertRaises(ValueError):V.analyze(w,self.labels,self.maps) + w = copy.deepcopy(self.word) + w.pop(next(i for i,e in enumerate(w) if e==["clear","Z2","query2"])) + with self.assertRaises(ValueError):V.analyze(w,self.labels,self.maps) + w = copy.deepcopy(self.word) + w[1707][3] *= -1 + with self.assertRaises(ValueError):V.analyze(w,self.labels,self.maps) + w = copy.deepcopy(self.word) + w.insert(1707,["begin","overlap",8]) + with self.assertRaises(ValueError):V.analyze(w,self.labels,self.maps) + + def test_composed_storage_and_width(self): + for depth in (1,2,3,8,100): + t=depth-1 + # Producer exact encoded magnitude is <2^(P+214+38t) in q_prod. + p=64; entry_p=p+214+38*t + self.assertEqual(entry_p+28+6*t,p+242+44*t) + self.assertEqual(71+19*t+9+3*t,80+22*t) + self.assertEqual(2*(704+224+16+1),1890) + self.assertEqual(2*(224+224+16+1),930) + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/qq16-streamed-decoder-format/verify.py b/research/qq16-streamed-decoder-format/verify.py new file mode 100644 index 0000000000..b9f95022b2 --- /dev/null +++ b/research/qq16-streamed-decoder-format/verify.py @@ -0,0 +1,326 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""All-depth exact format for the literal PR4015 decoder and its producer boundary. + +Nicholas Stone, with substantial OpenAI Codex assistance. No predecessor +executable is imported. Native/decoder functional semantics remain inherited. +""" +import argparse +from collections import Counter +from dataclasses import dataclass +from fractions import Fraction as Q +from functools import lru_cache +import gzip +import hashlib +import json +from pathlib import Path +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +ARCHIVE = "research/community-frontier1042-audit/selected-replay.tar.gz" +WORD = "research/qq16-streaming-recovery/WORD.json" +MEMBER = "t16/global/base/work/complex-nine-native/DATA-PHASES.json" +MEMBER_SHA = "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" +AXES = tuple(1 << j for j in range(73)) +F17 = tuple((v, 1) for v in AXES[:17]) +F16 = tuple((v, 1) for v in AXES[9:25]) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def canon(value): + return json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False) + + +def load(): + pins = json.loads((HERE / "SOURCES.json").read_text()) + for item in pins["files"]: + if item["usage"] == "input": + raw = (ROOT / item["path"]).read_bytes() + need(hashlib.sha256(raw).hexdigest() == item["sha256"], "source mismatch") + with tarfile.open(ROOT / ARCHIVE) as tf: + raw = tf.extractfile(MEMBER).read() + need(hashlib.sha256(raw).hexdigest() == MEMBER_SHA, "phase source mismatch") + return json.loads((ROOT / WORD).read_text()), json.loads(raw) + + +def act(columns, vector): + result = 0 + while vector: + bit = vector & -vector + result ^= columns[bit.bit_length() - 1] + vector ^= bit + return result + + +@lru_cache(None) +def phase(terms): + linear, quadratic = [0]*73, [0]*73 + for v, c in terms: + bits = [j for j in range(73) if v >> j & 1] + for j in bits: + linear[j] = (linear[j] + c) % 4 + if c % 2: + for k in bits: + if k > j: + quadratic[j] ^= 1 << k + return tuple(linear), tuple(quadratic) + + +def tidy(terms): + counts = Counter() + for v, c in terms: + counts[v] += c + return tuple((v, c % 4) for v, c in sorted(counts.items()) if c % 4 and v) + + +def geometry(data): + need(data["m"] == 73 and len(data["recipes"]) == 112, "source geometry") + labels, maps = [], {} + for p, record in enumerate(data["recipes"]): + q = record["q"] + need(record["port"] == p and 0 < q < 512, "source label") + labels.append(q) + basis = (q, *record["idle_children"][0]["orthogonal_axes"][:8]) + need(all(((u & v).bit_count() % 2) == (i == j) + for i, u in enumerate(basis) for j, v in enumerate(basis)), "chart basis") + for stage in (1, 2): + swaps = [basis[j+1] ^ AXES[9+8*(stage-1)+j] for j in range(8)] + columns = tuple(v ^ act(swaps, sum(((v & s).bit_count() % 2) << j + for j, s in enumerate(swaps))) for v in AXES) + need(tuple(act(columns, v) for v in columns) == AXES, "owner involution") + target = F17 if stage == 1 else F16 + ((q, 1),) + moved = phase(tuple((act(columns, v), c) for v, c in F17)) + desired = phase(target) + need(moved[1] == desired[1], "bridge quadratic phase") + delta = tuple((a-b) % 4 for a, b in zip(desired[0], moved[0])) + need(all(x in (0, 2) for x in delta), "bridge shift phase") + shift = sum((x//2) << j for j, x in enumerate(delta)) + maps[stage, p] = columns, shift + # Every signed local native recipe, including the negative affine offset. + columns_checked = 0 + for q in labels: + pivot = (q & -q).bit_length()-1 + basis = (q,) + tuple(1 << j for j in range(9) if j != pivot) + inverse = {act(basis, x): x for x in range(512)} + need(len(inverse) == 512, "native basis inverse") + for sign in (1, -1): + offset = 0 if sign == 1 else q + for x in range(512): + y = inverse[x] + actual = {act(basis, y) ^ offset: (1, 1), + act(basis, y ^ 1) ^ offset: (1, -1)} + need(actual == {x: (1, sign), x ^ q: (1, -sign)}, "native kernel sign") + columns_checked += 1 + return labels, maps, columns_checked + + +@dataclass(frozen=True) +class Bound: + poly: tuple + grid: int = 0 + slope: int = 0 + + def plus(self, other): + if not self.poly: + return other + if not other.poly: + return self + size = max(len(self.poly), len(other.poly)) + return Bound(tuple((self.poly[j] if j < len(self.poly) else 0) + + (other.poly[j] if j < len(other.poly) else 0) + for j in range(size)), max(self.grid, other.grid), + max(self.slope, other.slope)) + + def scale(self, c): + if not self.poly or not c: + return ZERO + n = abs(c.numerator) + need(c.denominator & (c.denominator-1) == 0, "dyadic coefficient") + valuation = (n & -n).bit_length()-1 + return Bound(tuple(abs(c)*x for x in self.poly), + self.grid+c.denominator.bit_length()-1-valuation, self.slope) + + def tensor_line(self, multiplier, halved): + if not self.poly: + return ZERO + return Bound((Q(0),) + tuple(multiplier*x for x in self.poly), + self.grid+int(halved), self.slope+1) + + def record(self): + return [list(map(str, self.poly)), self.grid, self.slope] + + +ZERO, ONE = Bound(()), Bound((Q(1),)) + + +def analyze(word, labels, maps): + borrowed = {s+str(p) for s in ("X", "Y") for p in range(112)} + outputs = {s+str(p) for s in ("Z", "W") for p in range(112)} + state = {n: ONE for n in borrowed} + frames = {n: F17 + (((labels[int(n[1:])], -1),) if n[0] == "Y" else ()) for n in borrowed} + active, initialized = set(), set() + counts, peak, degree, grid, slope = Counter(), Q(1), 0, 0, 0 + peak_site, observations, checkpoints = [-1, "entry"], [], [] + max_private = 0 + + def observe(value, i, label): + nonlocal peak, degree, grid, slope, peak_site + observations.append([i, label, value.record()]) + if value.poly: + degree = max(degree, len(value.poly)-1) + grid, slope = max(grid, value.grid), max(slope, value.slope) + magnitude = sum(value.poly) + if magnitude > peak: + peak, peak_site = magnitude, [i, label] + + def read(n): + need(n in state and n in borrowed | outputs | active, "uninitialized read: " + n) + return state[n] + + for i, e in enumerate(word): + op = e[0] + counts[op] += 1 + if op == "begin": + need(not active and e[2] in (8, 16), "private allocation") + active = {s+str(k) for s in ("F", "G")[:e[2]//8] for k in range(8)} + max_private = max(max_private, len(active)) + elif op == "end": + need(len(active) == e[2] and all(state.get(n) == ZERO and frames.get(n) == () + for n in active), "private zero/identity return") + for n in active: + del state[n], frames[n] + active = set() + elif op == "clear": + need(e[1] in outputs | active, "CLEAR ownership") + f = e[2] + if f in ("current", "wide"): + frame = F17 + elif f == "query2": + frame = F16 + elif f == "identity": + frame = () + else: + need(f.startswith("hole") and 0 <= int(f[4:]) < 112, "clear frame") + frame = F17 + ((labels[int(f[4:])], -1),) + state[e[1]], frames[e[1]] = ZERO, tidy(frame) + initialized.add(e[1]); observe(ZERO, i, "clear") + elif op == "add": + dst, src, c = e[1], e[2], Q(e[3]) + need(dst in outputs | active and dst != src, "ADD ownership") + need(c in (1, -1, Q(1, 4), Q(-1, 4)), "ADD coefficient") + left, right = read(dst), read(src) + need(phase(frames[dst]) == phase(frames[src]), "ADD frame mismatch at " + str(i) + " " + str(e)) + observe(right, i, "product-copy") + term = right.scale(c) + observe(term, i, "product-result") + state[dst] = left.plus(term); observe(state[dst], i, "add") + counts["negative_ADD"] += int(c < 0) + counts["quarter_ADD"] += int(c.denominator == 4) + elif op == "line": + dst, p, sign = e[1:] + need(not active and dst in outputs and type(p) is int and + 0 <= p < 112 and sign in (-1, 1), "native ownership/schema") + value = read(dst) + observe(value, i, "right-monomial") + observe(value.tensor_line(2, False), i, "native-pair") + observe(value.tensor_line(4, False), i, "native-cross") + state[dst] = value.tensor_line(2, True) + observe(state[dst], i, "native-output") + observe(state[dst], i, "left-monomial") + frames[dst] = tidy(frames[dst] + ((labels[p], sign),)) + elif op == "map": + dst, stage, p, inv = e[1:] + need(not active and dst in outputs and (stage, p) in maps and type(inv) is bool, + "map ownership/schema") + observe(read(dst), i, "cover-map") + columns, shift = maps[stage, p] + if inv: + shift = act(columns, shift) + frames[dst] = tidy(tuple((act(columns, v), c) for v, c in frames[dst]) + + tuple((v, 2) for v in AXES if shift & v)) + elif op == "checkpoint": + need(not active and outputs <= state.keys(), "checkpoint state") + checkpoints.append([i, max(sum(state[n].poly) for n in outputs)]) + else: + raise ValueError("unknown instruction") + need(not active and outputs <= initialized, "complete output allocation") + need(all(state[n] == ONE for n in borrowed), "borrowed state changed") + need(all(phase(frames[n]) == phase(F17) for n in outputs), "output frame") + bits = 0 + while 2**bits < peak: + bits += 1 + base_ops = (4*counts["add"] + 2*counts["negative_ADD"] + 2*counts["quarter_ADD"] + + 2*counts["clear"] + 8*counts["line"] + 2) + fused_with_covers = (2*counts["add"] + 2*counts["quarter_ADD"] + 2*counts["clear"] + + 12*counts["line"] + 4*counts["map"]) + result = { + "events": len(word), "counts": dict(sorted(counts.items())), + "observations": len(observations), "peak_polynomial_at_one": str(peak), + "peak_site": peak_site, "polynomial_degree": degree, + "grid_intercept": grid, "grid_slope": slope, "range_bits": bits, + "standalone_width_offset": grid+bits+1, "standalone_width_slope": slope+degree, + "composed_grid_intercept": 71+grid, "composed_grid_slope": 19+slope, + "composed_width_offset": 215+grid+bits, + "composed_width_slope": 38+slope+degree, + "borrowed_unchanged": len(borrowed), "output_banks": len(outputs), + "private_peak": max_private, "checkpoints": [[i, str(v)] for i, v in checkpoints], + "decoder_wordops_per_N": [base_ops, 10*counts["line"]], + "decoder_wordops_constant": 12, "decoder_cover_transfers_per_N": 4*counts["map"], + "pr4109_fused_reference_fixed_with_covers_per_N": fused_with_covers, + "unfused_reference_fixed_with_covers_per_N": base_ops+4*counts["map"], + "protocol_difference_fixed_per_N": base_ops+4*counts["map"]-fused_with_covers, + "decoder_numeric_storage_per_N": 2*(len(borrowed)+len(outputs)+max_private+1), + "composed_wordops_per_N": [372322+base_ops, 110760+10*counts["line"]], + "composed_wordops_constant": 24, "composed_cover_transfers_per_N": 2112+4*counts["map"], + "composed_numeric_storage_per_N": 2*(704+len(outputs)+max_private+1), + "scratch_scalar_words": 12, + "trace_sha256": hashlib.sha256(canon(observations).encode()).hexdigest(), + "one_layer_capacity_sha256": hashlib.sha256(canon([ + [i, label, str(sum(map(Q, value[0]))), value[1] if value[0] else 0] + for i, label, value in observations]).encode()).hexdigest(), + } + return result, observations + + +def compute(): + word, data = load() + producer = json.loads((ROOT / "research/qq16-all-depth-producer-grid/RESULT.json").read_text()) + expected = {"grid_intercept_at_one": 71, "grid_slope": 19, + "range_bits_at_one": 143, "range_slope": 19, + "signed_width_P_plus_at_one": 215, "signed_width_slope": 38, + "tensor_constant_wordops_per_N": 372322, "tensor_linear_wordops_per_N": 110760, + "cover_transfers_per_N": 2112, "scalar_scratch_words": 12} + need(all(producer[k] == v for k, v in expected.items()), "producer boundary constants") + labels, maps, columns = geometry(data) + result, _ = analyze(word, labels, maps) + prior = json.loads((ROOT / "research/qq16-paired-precision/RESULT.json").read_text()) + need(prior["exact_format"]["q"] == "h*2^(-9-3t)" and + prior["exact_format"]["signed_component_bits"] == "P+28+6t" and + prior["conditional_producer_composition"]["joint_q"] == "h*2^(-80-22t)" and + prior["conditional_producer_composition"]["joint_width"] == "P+242+44t", + "published common-format comparison") + result.update(status="PASS_QQ16_STREAMED_DECODER_FORMAT", native_basis_columns=columns, + owner_maps_checked=len(maps), new_supplier_or_kappa=False) + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path) + args = parser.parse_args() + result = compute() + if args.write: + with args.write.open("x") as out: + out.write(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + need(canon(result) == canon(json.loads((HERE / "RESULT.json").read_text())), "receipt mismatch") + print(result["status"], "decoder_guard=9+3t", "composed_guard=80+22t", "width=P+242+44t") + + +if __name__ == "__main__": + main()