From 8514cdf994b0a90bfb3a19a4c9d3a32b2c911e4d Mon Sep 17 00:00:00 2001 From: Wentao Li Date: Sat, 17 Oct 2026 23:33:12 +0000 Subject: [PATCH] Bind the exact F0/B1 entry width to one F17 pair-kernel bill. The selected stock coefficient is already registered, so this records the joint-query arithmetic subtotal at W=532 and the dirty-ledger grid obstruction. --- research/qq16-f17-pair-bill/CERTIFICATE.json | 30 ++ research/qq16-f17-pair-bill/MASTER-HANDOFF.md | 17 ++ research/qq16-f17-pair-bill/NOTICE.md | 12 + research/qq16-f17-pair-bill/PROOF.md | 124 +++++++++ research/qq16-f17-pair-bill/README.md | 113 ++++++++ research/qq16-f17-pair-bill/SOURCES.json | 36 +++ research/qq16-f17-pair-bill/TASK.json | 89 ++++++ research/qq16-f17-pair-bill/VERIFY.json | 34 +++ research/qq16-f17-pair-bill/independent.py | 100 +++++++ research/qq16-f17-pair-bill/test_package.py | 106 ++++++++ research/qq16-f17-pair-bill/verify.py | 257 ++++++++++++++++++ 11 files changed, 918 insertions(+) create mode 100644 research/qq16-f17-pair-bill/CERTIFICATE.json create mode 100644 research/qq16-f17-pair-bill/MASTER-HANDOFF.md create mode 100644 research/qq16-f17-pair-bill/NOTICE.md create mode 100644 research/qq16-f17-pair-bill/PROOF.md create mode 100644 research/qq16-f17-pair-bill/README.md create mode 100644 research/qq16-f17-pair-bill/SOURCES.json create mode 100644 research/qq16-f17-pair-bill/TASK.json create mode 100644 research/qq16-f17-pair-bill/VERIFY.json create mode 100644 research/qq16-f17-pair-bill/independent.py create mode 100644 research/qq16-f17-pair-bill/test_package.py create mode 100644 research/qq16-f17-pair-bill/verify.py diff --git a/research/qq16-f17-pair-bill/CERTIFICATE.json b/research/qq16-f17-pair-bill/CERTIFICATE.json new file mode 100644 index 0000000000..88ee209797 --- /dev/null +++ b/research/qq16-f17-pair-bill/CERTIFICATE.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "status": "PASS_QQ16_F17_PAIR_BILL", + "producer": "F_0_then_B_1_2", + "consumer": "PR2707_zero_retention_decoder_in_F17", + "parameters": { + "h": 73, + "lambda": 1, + "f": 64, + "e": 0, + "beta": 64 + }, + "Q0": 80, + "b": 79, + "k": 137, + "Qmax": 497, + "E": 15, + "W": 532, + "w": 529, + "L": 531, + "exponent_bits": 10, + "gates_per_pair": 159192, + "pair_kernel_coefficient": 26744256, + "field_bit_coefficient": 493696, + "control_gates_per_pair": 124028, + "control_pair_kernel_coefficient": 20836704, + "dirty_width_supplied": false, + "selected_kappa": "0.001672660197076918", + "kappa_changed": false +} diff --git a/research/qq16-f17-pair-bill/MASTER-HANDOFF.md b/research/qq16-f17-pair-bill/MASTER-HANDOFF.md new file mode 100644 index 0000000000..eaf0626efd --- /dev/null +++ b/research/qq16-f17-pair-bill/MASTER-HANDOFF.md @@ -0,0 +1,17 @@ +# Handoff + +Pinned CrocSwap main: `6f100d4bb5083f8c35d96fd95a539811c62f245c`. +Selected kappa, unchanged: `0.001672660197076918`. + +The selected stock coefficient was not rederived. `8194`, `6748` and the +lcm reserve are already registered, and the `m=73` shape lemma is already +an obstruction. This package switched to `joint-query-controller`. + +Claim: at the exact F0 then B_1_2 entry parameters `lambda=1`, `f=64`, +`e=0`, `beta=64`, the F17 zero-retention decoder's runtime pair kernel is +at most `26744256 lambda N D` gates and its 464 named fields use at most +`493696 N D` data bits. The dirty-helper magnitude ledger does not supply +the width those counts use. + +Stop. Do not treat this as a complete consumer, a new precision constant, +or a new kappa. diff --git a/research/qq16-f17-pair-bill/NOTICE.md b/research/qq16-f17-pair-bill/NOTICE.md new file mode 100644 index 0000000000..ec87a23c63 --- /dev/null +++ b/research/qq16-f17-pair-bill/NOTICE.md @@ -0,0 +1,12 @@ +# Notice + +New derivation, checker, tests and prose in this directory are Apache-2.0, +following the repository license. + +Predecessor files are not modified. Their authors and licenses remain as +recorded in those packages. In particular, the exact F0/B_1_2 entry contract, +the finite dyadic format, the rounded pair circuit and the rounded producer +envelope keep their original attribution. + +Prepared by Wentao Li with substantial AI assistance. +No independent human review is claimed. diff --git a/research/qq16-f17-pair-bill/PROOF.md b/research/qq16-f17-pair-bill/PROOF.md new file mode 100644 index 0000000000..ee3aaf773a --- /dev/null +++ b/research/qq16-f17-pair-bill/PROOF.md @@ -0,0 +1,124 @@ +# Exact-producer width of one F17 decoder arithmetic bill + +The selected conditional kappa remains **0.001672660197076918**. This note +does not change it. + +## Why this is not a stock-coefficient package + +On the pinned main, the selected ordinary BIT parent reserve is already +derived: Adam Gall's package gives the conditional coefficient 8194, Nick +Petalas's ceiling-free refinement gives 6748, and the later lcm-reserve +package binds `269241600 |GL_64(F_q)| q^(4096(w-1))` to the same depth +recurrence. The complex `m=73` shape coefficients `A`, `B` and `rho` are +already recorded as unbound. Repeating those derivations is not a new fact. +The open joint-query obligation is the one taken below. + +## Pinned producer and consumer + +The literal producer is the exact full-cover word **F0 followed by B_1_2** +in the retained joint-query certificate, as used by Nick Petalas's +producer-entry contract and by the #2965 defect transfer. The consumer of +its completed charts is ywz65's PR2707 zero-retention decoder. At the +completed B1 cut that word reads X in chart F17 and Y in chart +`F17 C_q^{-1}`, and it returns the original 224 logical arrays **in F17**. +F17 means the product of the signed Fourier lines on address axes 0 through +16. This package does not replay the producer or the decoder word. + +## Inherited exact entry + +Under the entry contract's hypotheses (exact producer arithmetic, the +inherited helper contract, `h=73` address axes, and positive tensor depth), +post-B1 fields satisfy + +```text +B = 17628*H < 2^(e+15), +Q0 = f + ceil(lambda/2) + 6 + 9*lambda, +``` + +whenever `H <= 2^e`. The displayed `17628` is the predecessor's triangle +bound. This note checks the slack `17628 < 2^15`, which is what makes +`B < 2^(e+15)` follow from `H <= 2^e`. For an original-input error `H 2^{-beta}`, +that contract sets the decoder's relative target to `b = beta+15` and quotes +PR2807's width + +```text +k = beta+37 + ceil_log2(lambda) + floor(73 lambda / 2), +Qmax = Q0 + 3k + 6, +W = Qmax + e + 35. +``` + +At `lambda=1`, `f=64`, `e=0`, `beta=64` this is + +```text +Q0 = 80, b = 79, k = 137, Qmax = 497, E = 15, W = 532. +``` + +`E = e+15` is the entry exponent in PR2807's notation `B <= 2^E`. The same +proof's completed-field majorant is `32369 B`. Because `32369 < 2^15` and +`B < 2^E`, that majorant is strictly below `2^(E+15)`, so the inherited +overflow argument still applies at this `E`. + +## Pair inputs at this width + +PR2807 bounds every common-grid component by `2^(Qmax+E+16) = 2^(W-4)` and +every pair numerator by `2^(Qmax+E+18) = 2^(W-2)`, strictly. Signed `w`-bit +integers hold absolute values strictly below `2^(w-1)`. The choice + +```text +w = W-3, L = w+2 = W-1 +``` + +therefore stores the components and the numerators. At `W=532` this is +`w=529`, `L=531`. The published `W=456` control is the same rule: +`w=453`, `L=455`. + +PR2811's runtime-exponent circuit, for `k = bit_length(L-2)`, has + +```text +24 L k + 52 L + 4 * 2^k + 4 k + 4 +``` + +gates. The control is `k=9` and **124,028** gates. There are 336 lines and +at most `lambda D / 2` pairs per line per owner, so the kernel coefficient +is `gates * 168`. The control coefficient is `124028 * 168 = 20836704`, +matching the published `20836704 lambda N D` subtotal. + +At `L=531`, `k = bit_length(529) = 10` and the gate count is **159,192**. +The kernel subtotal is at most + +```text +159192 * 168 * lambda * N * D = 26744256 lambda N D +``` + +gate evaluations. PR2807's named-field representation uses at most +`2 * 464 * N * D * W` data bits. At this width that coefficient is + +```text +2 * 464 * 532 = 493696, +``` + +so at most `493696 N D` data bits for the 224 borrowed arrays, 224 outputs +and sixteen private arrays. + +These two coefficients are sufficient conditional upper bounds in the +incorporated gate and register models. They are not tape time, not a +recursive rank tariff, and not a complete machine invoice. + +## Dirty-helper ledger does not supply the width + +The rounded-producer envelope is the registered intermediate +magnitude/dirty-state ledger for this same literal producer. It bounds the +noisy all-cut B1 norm by `2^(delta+80) H` and states that component +representation, the entry grid, and subsequent F17 consumption are unknown. +PR2807 states that a norm bound alone does not determine the adaptive line +exponent: inputs `2^{-j}` can have bounded norm and arbitrarily negative +exponent. Substituting `E = delta+80` into `W` is therefore not licensed. +The missing bound is a proved entry grid `2^{-Q0} Z` for the actual dirty +helpers. `dirty_width_supplied` is false. + +## What remains outside the bill + +Scans, the 2,704 scalar ADDs, wrappers, cover maps, address arithmetic, +movement, cleanup and a later endpoint adapter are unpaid here. A caller +that does not accept F17 outputs still needs its own frame conversion. +The entry contract already says that adapter is a separate invoice. diff --git a/research/qq16-f17-pair-bill/README.md b/research/qq16-f17-pair-bill/README.md new file mode 100644 index 0000000000..a2ddf3a0b3 --- /dev/null +++ b/research/qq16-f17-pair-bill/README.md @@ -0,0 +1,113 @@ +# One F17 pair-kernel bill at the exact F0/B_1_2 entry width + +**Switched card.** The selected stock coefficient is already registered: +Adam Gall's parent reserve gives conditional `sigma=8194`, Nick Petalas's +ceiling-free refinement gives `6748`, and the lcm-reserve package binds the +same depth recurrence to `269241600 |GL_64(F_q)| q^(4096(w-1))`. The complex +`m=73` coefficients `A`, `B` and `rho` are already recorded as unbound. +This package takes card `joint-query-controller` instead. + +**Partial arithmetic bill; no new kappa.** For the literal exact producer +F0 followed by B_1_2, the inherited entry contract at + +```text +lambda=1, f=64, e=0, beta=64, h=73 +``` + +gives decoder width `W=532`. Under the incorporated runtime-exponent pair +model, the F17 zero-retention decoder's pair kernel costs at most + +```text +26744256 lambda N D +``` + +gate evaluations, and its 464 named fields use at most + +```text +493696 N D +``` + +data bits. The registered dirty-helper magnitude ledger does **not** supply +this width. The selected kappa remains `0.001672660197076918`. + +```sh +python3.12 -I -B research/qq16-f17-pair-bill/verify.py +``` + +Expected: + +```text +PASS_QQ16_F17_PAIR_BILL W=532 gates_per_pair=159192 pair_kernel=26744256*lambda*N*D field_bits=493696*N*D dirty_width=unsupplied control_gates=124028 +``` + +## What is bound + +The producer and the post-B1 norm `B=17628*H < 2^(e+15)` are Nick Petalas's +exact entry contract. The width chain `Q0=80`, `b=79`, `k=137`, `Qmax=497`, +`W=532` is that contract's published example, recomputed here. PR2807's +component and numerator bounds give signed pair inputs `w=W-3=529` and +`L=531`. PR2811's runtime gate formula then gives `159192` gates per pair. +The published control `L=455` still gives `124028` gates and kernel +coefficient `20836704`. The field-bit formula `2*464*N*D*W` is PR2807's. + +The consumer is the PR2707 decoder: it reads the producer's F17 and +`F17 C_q^{-1}` charts and returns the original arrays in F17. The proof is +in [PROOF.md](PROOF.md). The receipt is [CERTIFICATE.json](CERTIFICATE.json). + +## What the dirty ledger does not give + +The rounded-producer envelope already records this producer's intermediate +magnitude and dirty-helper state, including the all-cut bound +`2^(delta+80) H`. It leaves the component grid and F17 consumption unknown. +PR2807 states that a norm bound alone does not determine the adaptive line +exponent. That is the obstruction: the dirty ledger cannot be substituted +for `E` and `Q0`. No second magnitude table is computed here. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -I -B research/qq16-f17-pair-bill/verify.py +python3.12 -I -O -B research/qq16-f17-pair-bill/verify.py +python3.12 -I -B research/qq16-f17-pair-bill/independent.py +python3.12 -I -B research/qq16-f17-pair-bill/test_package.py +python3.12 -B scripts/research_package.py --package research/qq16-f17-pair-bill +``` + +Default verification is read-only. `--write` creates a missing certificate +and refuses to overwrite one. + +## Open next questions + +1. **Entry grid for the dirty ledger.** The question is which proved grid + `2^{-Q0} Z` and exponent `E` the rounded F0/B_1_2 helpers actually meet. + It matters because without them the pair-kernel count above does not + apply to the noisy contract. The first step is to pin one finite producer + implementation and prove its completed components lie on that grid. The + blocker is that the rounded envelope leaves the grid unknown. + +2. **The remaining physical terms at W=532.** Scans, scalar ADDs, wrappers, + maps, addressing, movement and cleanup are still unpaid. The first step + is to apply the incorporated finite-format operation counts at this width. + The blocker is that the pair-circuit proof leaves those terms outside its + gate count, and the navigation scan formula is a separate pending model. + +3. **Whether the caller accepts F17.** A caller that needs the original + `C_q`/`I` frames pays an additional frame conversion. The first step is + to bind one admitted caller to either the F17 output contract or that + adapter tariff. The blocker is that neither pinned word chooses the caller. + +## Credit + +Nick Petalas supplied the #2965 defect transfer, the exact F0/B_1_2 entry +contract, PR2807's finite format and PR2811's pair circuit, and the +rounded-producer magnitude ledger. ywz65 supplied the PR2707 F17 decoder. +Arham Tahir supplied the logical inverse that decoder lowers. Ali Romman and +the retained joint-query authors supplied the literal F0/B_1_2 words. +Adam Gall and Nick Petalas supplied the selected BIT stock coefficients that +this package does not repeat. Hiroki KUMAZAKI's cutoff chain remains the +stock-margin record. Predecessor files are unchanged. + +Prepared by Wentao Li with substantial AI assistance. +No independent human review is claimed. New work is Apache-2.0. diff --git a/research/qq16-f17-pair-bill/SOURCES.json b/research/qq16-f17-pair-bill/SOURCES.json new file mode 100644 index 0000000000..f6b89e5be6 --- /dev/null +++ b/research/qq16-f17-pair-bill/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/qq16-producer-entry-contract/README.md", + "usage": "input", + "git_blob": "d3f66aac46ac8edbc6660715e586276909b0eac4", + "sha256": "83029c16c55be649e223bd583a14529d26a9c2e44afcf2766a3f70504b641ffe" + }, + { + "path": "research/qq16-finite-dyadic-format/README.md", + "usage": "input", + "git_blob": "7ea32799751829d5ff2c313406284c428299e10e", + "sha256": "916cb7e48b28bf6940822c0aca375bb1558ae5282cb4246fd3e9b19e4f41a9e6" + }, + { + "path": "research/qq16-rounded-pair-bit-circuit/README.md", + "usage": "input", + "git_blob": "2c3fecb98944bf3703e567a99671308c8bc7a72a", + "sha256": "7357e10ce43ab8eaea5f39f00a9166877bd6e13803c1ab0a1aeec890b02d6646" + }, + { + "path": "research/qq16-rounded-producer-envelope/README.md", + "usage": "input", + "git_blob": "2624a443e21a53b63fbedfd3d602892c5f33b6aa", + "sha256": "7e45a72f4d5a160d4b62478259c6d6b664d22799e98b0dd997be75367636edac" + } + ] +} diff --git a/research/qq16-f17-pair-bill/TASK.json b/research/qq16-f17-pair-bill/TASK.json new file mode 100644 index 0000000000..fc5552df9f --- /dev/null +++ b/research/qq16-f17-pair-bill/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "base_commit": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "author": "Wentao Li", + "ai_assistance": "Substantial AI assistance for derivation, implementation, checking and writing.", + "scope_status": "refined", + "scope_change_reason": "Registered packages already derive the selected BIT stock coefficients 8194 and 6748 and the lcm reserve, and selected-stock-envelope-m73 already records the missing m=73 shape lemma. This package therefore takes the joint-query handoff for one literal producer. It instantiates one F17 consumer arithmetic bill at the inherited exact entry width and isolates the dirty-helper ledger's missing grid, rather than optimizing another decoder precision constant.", + "actual_scope": "For the literal exact F0 followed by B_1_2 producer, instantiate the F17 zero-retention decoder's direct runtime pair-kernel gate subtotal and named-field bit count at the inherited entry width, and show that the dirty-helper magnitude ledger does not supply that width.", + "bottleneck_link": "The exact producer supplies a post-B1 norm and component grid, but the F17 decoder's pair-kernel bill was not instantiated at that width; the dirty magnitude ledger still lacks the entry grid the format proof requires.", + "stop_rule": "Stop after this one producer, the parameter tuple lambda=1, f=64, e=0, beta=64, h=73, and the two cost coefficients below. Do not optimize k, search another B pair, or treat the subtotal as a complete consumer invoice.", + "evidence": "Exact integer recomputation of the inherited width chain, the runtime pair-gate formula and the 464-field bit count, checked against the published 124028-gate control, plus source-text checks that the dirty ledger states only a norm bound and that the format proof refuses to turn a norm bound into an adaptive exponent.", + "outcome": "partial", + "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" + ] + }, + "open_questions": [ + { + "question": "What entry component grid and dirty-helper range make the same width theorem apply to the rounded F0/B_1_2 magnitude ledger?", + "why_it_matters": "The all-cut bound 2^(delta+80) H does not determine the adaptive line exponent, so it does not determine the pair-kernel gate count.", + "first_step": "Pin one finite producer implementation and prove its completed components lie on a stated grid 2^(-Q0) Z with a proved E.", + "blocked_by": "The rounded-producer envelope records the norm ledger and explicitly leaves the component grid unknown." + }, + { + "question": "What is the charged cost of block scans, scalar ADDs, wrappers, maps, addressing, movement and cleanup at W=532?", + "why_it_matters": "The pair-kernel coefficient and the 464-field bit count are two terms, not a complete physical bill.", + "first_step": "Apply the incorporated finite-format operation counts at this W, then add only a scan model whose proof is already incorporated.", + "blocked_by": "PR2811 leaves scans, movement and control outside its gate count, and the navigation scan formula is a separate pending model." + }, + { + "question": "Does the caller accept the decoder's F17 outputs, or must it pay the entry-frame adapters?", + "why_it_matters": "A caller that requires the original C_q/I frames pays an additional native rank mass that this arithmetic bill does not include.", + "first_step": "Bind one admitted caller to either the F17 output contract or the entry-frame tariff.", + "blocked_by": "No selected caller in the pinned producer or decoder word chooses that endpoint." + } + ] +} diff --git a/research/qq16-f17-pair-bill/VERIFY.json b/research/qq16-f17-pair-bill/VERIFY.json new file mode 100644 index 0000000000..7e37cff963 --- /dev/null +++ b/research/qq16-f17-pair-bill/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/qq16-producer-entry-contract/README.md", + "research/qq16-finite-dyadic-format/README.md", + "research/qq16-rounded-pair-bit-circuit/README.md", + "research/qq16-rounded-producer-envelope/README.md" + ], + "commands": [ + { + "argv": ["{python}", "-Werror", "-I", "-B", "{package}/verify.py"], + "timeout_seconds": 60, + "checks": "Recompute the exact-producer F17 width, pair-kernel coefficient and field-bit coefficient, and authenticate the dirty-ledger obstruction." + }, + { + "argv": ["{python}", "-Werror", "-I", "-O", "-B", "{package}/verify.py"], + "timeout_seconds": 60, + "checks": "Repeat the primary check with assertions disabled." + }, + { + "argv": ["{python}", "-Werror", "-I", "-B", "{package}/independent.py"], + "timeout_seconds": 60, + "checks": "Recompute the same integers and source obligations in a separate program." + }, + { + "argv": ["{python}", "-Werror", "-I", "-B", "{package}/test_package.py"], + "timeout_seconds": 120, + "checks": "Reject certificate corruption, duplicate JSON keys and drifted source bytes, including under -O." + } + ] +} diff --git a/research/qq16-f17-pair-bill/independent.py b/research/qq16-f17-pair-bill/independent.py new file mode 100644 index 0000000000..98dffbd823 --- /dev/null +++ b/research/qq16-f17-pair-bill/independent.py @@ -0,0 +1,100 @@ +#!/usr/bin/env python3 +"""Second arithmetic check of the F17 pair-kernel bill. + +This program is separate from the primary checker and from predecessor checkers. +Wentao Li, with substantial AI assistance. Apache-2.0. +""" + +import hashlib +import re +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +MAX_BYTES = 1_048_576 +DIGESTS = { + "research/qq16-producer-entry-contract/README.md": + "83029c16c55be649e223bd583a14529d26a9c2e44afcf2766a3f70504b641ffe", + "research/qq16-finite-dyadic-format/README.md": + "916cb7e48b28bf6940822c0aca375bb1558ae5282cb4246fd3e9b19e4f41a9e6", + "research/qq16-rounded-pair-bit-circuit/README.md": + "7357e10ce43ab8eaea5f39f00a9166877bd6e13803c1ab0a1aeec890b02d6646", + "research/qq16-rounded-producer-envelope/README.md": + "7e45a72f4d5a160d4b62478259c6d6b664d22799e98b0dd997be75367636edac", +} + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def locate(): + marker = Path("research/qq16-finite-dyadic-format/README.md") + for candidate in (Path.cwd(), *PACKAGE.parents): + if (candidate / marker).is_file(): + return candidate + need(False, "repository root") + return None + + +def text_of(root, name): + path = root / name + need(path.is_file() and not path.is_symlink(), "plain source") + raw = path.read_bytes() + need(len(raw) <= MAX_BYTES, "source capacity") + need(hashlib.sha256(raw).hexdigest() == DIGESTS[name], "source hash") + return re.sub(r"\s+", " ", raw.decode("utf-8")) + + +def pair_gates(length): + exponent_bits = (length - 2).bit_length() + total = (24 * length * exponent_bits) + (52 * length) + total += 4 * (2 ** exponent_bits) + 4 * exponent_bits + 4 + return total, exponent_bits + + +def main(): + root = locate() + entry = text_of(root, "research/qq16-producer-entry-contract/README.md") + finite = text_of(root, "research/qq16-finite-dyadic-format/README.md") + pair = text_of(root, "research/qq16-rounded-pair-bit-circuit/README.md") + dirty = text_of(root, "research/qq16-rounded-producer-envelope/README.md") + need("17628*H" in entry and "W=532" in entry and "X is in F17 and Y in F17" in entry, "entry contract") + need("2^(e+15)" in entry, "entry exponent") + need("A norm bound alone would not bound PR2771's adaptive exponent" in finite, "format obstruction") + need("2*464*N*D*W" in finite and "W = Qmax + E + 20" in finite, "storage formula") + need("24Lk+52L+4*2^k+4k+4" in pair and "20836704*lambda*N*D" in pair, "pair formula") + need("B1 is below `2^(delta+80) H`" in dirty, "dirty norm") + need("component representation/grid" in dirty and "subsequent F17 consumption are unknown" in dirty, + "dirty grid gap") + # lambda=1, f=64, e=0, beta=64, h=73. ceil(lambda/2)=1 and ceil_log2(1)=0. + q0 = 64 + 1 + 6 + 9 + relative_b = 64 + 15 + k = relative_b + 22 + 0 + (73 // 2) + qmax = q0 + 3 * k + 6 + width = qmax + 0 + 35 + need(q0 == 80 and relative_b == 79 and k == 137 and qmax == 497 and width == 532, "width chain") + need(17628 < 32768 and 32369 < 32768, "power-of-two slack") + component_width = width - 3 + length = component_width + 2 + gates, exponent_bits = pair_gates(length) + need(component_width == 529 and length == 531 and exponent_bits == 10, "pair shape") + need(gates == 159192 and gates * 168 == 26744256, "kernel coefficient") + need(2 * 464 * width == 493696, "field bits") + control, control_bits = pair_gates(455) + need(control_bits == 9 and control == 124028 and control * 168 == 20836704, "control") + # The dirty all-cut norm is not an entry exponent. The format proof blocks that substitution. + need("dirty_width_supplied" not in dirty, "ledger must not already claim this flag") + print( + "PASS_QQ16_F17_PAIR_BILL_INDEPENDENT " + f"W={width} gates_per_pair={gates} " + f"pair_kernel={gates * 168}*lambda*N*D " + f"field_bits={2 * 464 * width}*N*D dirty_width=unsupplied" + ) + + +if __name__ == "__main__": + try: + main() + except (OSError, UnicodeError, ValueError) as exc: + raise SystemExit("FAIL_QQ16_F17_PAIR_BILL_INDEPENDENT " + str(exc)) diff --git a/research/qq16-f17-pair-bill/test_package.py b/research/qq16-f17-pair-bill/test_package.py new file mode 100644 index 0000000000..8da583da02 --- /dev/null +++ b/research/qq16-f17-pair-bill/test_package.py @@ -0,0 +1,106 @@ +#!/usr/bin/env python3 +"""Reject certificate corruption and duplicate JSON keys for the F17 pair bill.""" + +import json +import os +import shutil +import subprocess +import sys +import tempfile +import unittest +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +INPUTS = ( + "research/qq16-producer-entry-contract/README.md", + "research/qq16-finite-dyadic-format/README.md", + "research/qq16-rounded-pair-bit-circuit/README.md", + "research/qq16-rounded-producer-envelope/README.md", +) + + +def run(root, optimized=False): + package = root / "research" / HERE.name + environment = dict(os.environ, PYTHONPYCACHEPREFIX=str(root / ".cache")) + flags = ["-Werror", "-I", "-B"] + if optimized: + flags.insert(2, "-O") + return subprocess.run( + [sys.executable, *flags, str(package / "verify.py")], + cwd=root, env=environment, capture_output=True, text=True, timeout=60, + ) + + +class PackageTests(unittest.TestCase): + def test_live_package_passes(self): + outcome = run(ROOT) + self.assertEqual(outcome.returncode, 0, outcome.stderr) + self.assertIn("PASS_QQ16_F17_PAIR_BILL", outcome.stdout) + self.assertIn("dirty_width=unsupplied", outcome.stdout) + + def copy_tree(self, root): + package = root / "research" / HERE.name + shutil.copytree(HERE, package, ignore=shutil.ignore_patterns("__pycache__")) + for name in INPUTS: + destination = root / name + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / name, destination) + return package + + def test_temp_copy_certificate_corruption(self): + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + package = self.copy_tree(root) + self.assertEqual(run(root).returncode, 0) + self.assertEqual(run(root, optimized=True).returncode, 0) + original = (package / "CERTIFICATE.json").read_bytes() + payload = json.loads(original) + payload["W"] = 531 + replacements = [ + json.dumps(payload).encode(), + b'{"schema_version": 1, "schema_version": 1}\n', + b'{"W": true}\n', + b'{"status": "PASS_QQ16_F17_PAIR_BILL"}\n', + ] + for replacement in replacements: + (package / "CERTIFICATE.json").write_bytes(replacement) + for optimized in (False, True): + outcome = run(root, optimized=optimized) + self.assertNotEqual(outcome.returncode, 0) + self.assertIn("FAIL_QQ16_F17_PAIR_BILL", outcome.stderr) + (package / "CERTIFICATE.json").write_bytes(original) + self.assertEqual(run(root, optimized=True).returncode, 0) + + def test_duplicate_json_key_message(self): + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + package = self.copy_tree(root) + (package / "CERTIFICATE.json").write_text('{"W": 532, "W": 456}\n', encoding="utf-8") + outcome = run(root, optimized=True) + self.assertNotEqual(outcome.returncode, 0) + self.assertIn("duplicate JSON key", outcome.stderr) + + def test_source_drift_and_independent(self): + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + self.copy_tree(root) + source = root / INPUTS[0] + source.write_bytes(source.read_bytes() + b"\n") + outcome = run(root) + self.assertNotEqual(outcome.returncode, 0) + self.assertIn("source hash", outcome.stderr) + environment = dict(os.environ, PYTHONPYCACHEPREFIX=str(ROOT / ".cache-independent")) + outcome = subprocess.run( + [sys.executable, "-Werror", "-I", "-B", str(HERE / "independent.py")], + cwd=ROOT, env=environment, capture_output=True, text=True, timeout=60, + ) + self.assertEqual(outcome.returncode, 0, outcome.stderr) + self.assertIn("PASS_QQ16_F17_PAIR_BILL_INDEPENDENT", outcome.stdout) + source = (HERE / "independent.py").read_text(encoding="utf-8") + self.assertNotIn("import verify", source) + self.assertNotIn("from verify", source) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/qq16-f17-pair-bill/verify.py b/research/qq16-f17-pair-bill/verify.py new file mode 100644 index 0000000000..3c4ea4edf7 --- /dev/null +++ b/research/qq16-f17-pair-bill/verify.py @@ -0,0 +1,257 @@ +#!/usr/bin/env python3 +"""Bind the exact F0/B_1_2 entry width to one F17 decoder arithmetic bill. + +Wentao Li, with substantial AI assistance. Apache-2.0. +Predecessor verifiers are not imported. Admission uses need(), including under -O. +""" + +import argparse +import hashlib +import json +import re +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +MAX_BYTES = 1_048_576 +PARAMETERS = {"h": 73, "lambda": 1, "f": 64, "e": 0, "beta": 64} +INPUTS = { + "research/qq16-producer-entry-contract/README.md": + "83029c16c55be649e223bd583a14529d26a9c2e44afcf2766a3f70504b641ffe", + "research/qq16-finite-dyadic-format/README.md": + "916cb7e48b28bf6940822c0aca375bb1558ae5282cb4246fd3e9b19e4f41a9e6", + "research/qq16-rounded-pair-bit-circuit/README.md": + "7357e10ce43ab8eaea5f39f00a9166877bd6e13803c1ab0a1aeec890b02d6646", + "research/qq16-rounded-producer-envelope/README.md": + "7e45a72f4d5a160d4b62478259c6d6b664d22799e98b0dd997be75367636edac", +} +EXPECTED = { + "schema_version": 1, + "status": "PASS_QQ16_F17_PAIR_BILL", + "producer": "F_0_then_B_1_2", + "consumer": "PR2707_zero_retention_decoder_in_F17", + "parameters": PARAMETERS, + "Q0": 80, + "b": 79, + "k": 137, + "Qmax": 497, + "E": 15, + "W": 532, + "w": 529, + "L": 531, + "exponent_bits": 10, + "gates_per_pair": 159192, + "pair_kernel_coefficient": 26744256, + "field_bit_coefficient": 493696, + "control_gates_per_pair": 124028, + "control_pair_kernel_coefficient": 20836704, + "dirty_width_supplied": False, + "selected_kappa": "0.001672660197076918", + "kappa_changed": False, +} + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def unique(pairs): + result = {} + for key, value in pairs: + need(key not in result, "duplicate JSON key") + result[key] = value + return result + + +def root_dir(): + candidates = [Path.cwd(), *PACKAGE.parents] + marker = "research/qq16-finite-dyadic-format/README.md" + for candidate in candidates: + if (candidate / marker).is_file(): + return candidate + need(False, "repository root") + return None + + +def read_bytes(path): + need(path.is_file() and not path.is_symlink(), "expected plain file: " + path.name) + with path.open("rb") as source: + raw = source.read(MAX_BYTES + 1) + need(len(raw) <= MAX_BYTES, "file byte capacity: " + path.name) + return raw + + +def normalized(text): + return re.sub(r"\s+", " ", text) + + +def load_sources(root): + texts = {} + for name, digest in INPUTS.items(): + path = root / name + raw = read_bytes(path) + need(hashlib.sha256(raw).hexdigest() == digest, "source hash: " + name) + texts[name] = normalized(raw.decode("utf-8")) + return texts + + +def require_phrases(texts): + entry = texts["research/qq16-producer-entry-contract/README.md"] + finite = texts["research/qq16-finite-dyadic-format/README.md"] + pair = texts["research/qq16-rounded-pair-bit-circuit/README.md"] + dirty = texts["research/qq16-rounded-producer-envelope/README.md"] + for phrase in ( + "norm <= B = 17628*H", + "B < 2^(e+15)", + "ceil(lambda/2) + 6 + 9*lambda", + "k = beta+37 + ceil_log2(lambda) + floor(73*lambda/2)", + "W = Qmax + e + 35", + "W=532", + "X is in F17 and Y in F17", + "physical endpoint adapter or consumer still needs its own invoice", + ): + need(phrase in entry, "missing entry phrase: " + phrase) + for phrase in ( + "Qmax = Q0 + 3*k + 6", + "W = Qmax + E + 20", + "2*464*N*D*W", + "32369*B < 2^(E+15)", + "less than `2^(E+16)`", + "smaller than `2^(Qmax+E+16)`", + "smaller than `2^(Qmax+E+18)`", + "W=456", + "A norm bound alone would not bound PR2771's adaptive exponent", + ): + need(phrase in finite, "missing format phrase: " + phrase) + for phrase in ( + "24Lk+52L+4*2^k+4k+4", + "124,028", + "w=453", + "L=455", + "20836704*lambda*N*D", + ): + need(phrase in pair, "missing pair phrase: " + phrase) + for phrase in ( + "B1 is below `2^(delta+80) H`", + "component representation/grid", + "subsequent F17 consumption are unknown", + "a paid F17 consumer", + ): + need(phrase in dirty, "missing dirty-ledger phrase: " + phrase) + + +def ceil_log2(value): + need(type(value) is int and value >= 1, "ceil_log2 domain") + if value == 1: + return 0 + return (value - 1).bit_length() + + +def runtime_gates(length): + """PR2811 runtime-exponent pair count: 24*L*k+52*L+4*2^k+4*k+4.""" + need(type(length) is int and length >= 3, "pair length") + bits = (length - 2).bit_length() + gates = 24 * length * bits + 52 * length + 4 * (1 << bits) + 4 * bits + 4 + return gates, bits + + +def derive(): + h = PARAMETERS["h"] + lam = PARAMETERS["lambda"] + fractional = PARAMETERS["f"] + exponent = PARAMETERS["e"] + beta = PARAMETERS["beta"] + need(17628 < 2 ** 15, "post-B1 norm does not fit E=e+15") + need(32369 < 2 ** 15, "completed-field majorant does not fit E") + # Q0 uses ceil(lambda/2), which is not ceil_log2(lambda) except at lambda=1. + q0 = fractional + (lam + 1) // 2 + 6 + 9 * lam + relative = beta + 15 + precision = relative + 22 + ceil_log2(lam) + (h * lam) // 2 + qmax = q0 + 3 * precision + 6 + entry_exponent = exponent + 15 + width = qmax + entry_exponent + 20 + need(width == qmax + exponent + 35, "entry-contract width identity") + component_bits = width - 3 + length = component_bits + 2 + gates, bits = runtime_gates(length) + # Strict component bound abs < 2^(W-4) fits in signed (W-3) bits. + need(component_bits - 1 == width - 4, "component width slack") + need(length - 1 == width - 2, "numerator width slack") + coefficient = gates * 168 + field_bits = 2 * 464 * width + control_gates, control_bits = runtime_gates(455) + need(control_bits == 9 and control_gates == 124028, "published pair control") + need(control_gates * 168 == 20836704, "published kernel coefficient") + bill = { + "Q0": q0, + "b": relative, + "k": precision, + "Qmax": qmax, + "E": entry_exponent, + "W": width, + "w": component_bits, + "L": length, + "exponent_bits": bits, + "gates_per_pair": gates, + "pair_kernel_coefficient": coefficient, + "field_bit_coefficient": field_bits, + "control_gates_per_pair": control_gates, + "control_pair_kernel_coefficient": control_gates * 168, + "dirty_width_supplied": False, + } + for key, value in bill.items(): + need(value == EXPECTED[key], "recomputed bill mismatch: " + key) + return bill + + +def certificate_matches(root, bill): + path = PACKAGE / "CERTIFICATE.json" + raw = read_bytes(path) + data = json.loads(raw, object_pairs_hook=unique) + need(type(data) is dict, "certificate object") + need(set(data) == set(EXPECTED), "certificate keys") + for key, value in EXPECTED.items(): + if key == "parameters": + need(type(data[key]) is dict and set(data[key]) == set(PARAMETERS), "parameters") + for name, item in PARAMETERS.items(): + need(type(data[key][name]) is int and data[key][name] == item, name) + elif type(value) is int: + need(type(data[key]) is int and data[key] == bill.get(key, value), key) + elif type(value) is bool: + need(type(data[key]) is bool and data[key] is value, key) + else: + need(type(data[key]) is str and data[key] == value, key) + need(root.is_dir(), "root") + + +def canonical_certificate(): + return json.dumps(EXPECTED, indent=2, ensure_ascii=False) + "\n" + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--write", action="store_true") + args = parser.parse_args() + root = root_dir() + texts = load_sources(root) + require_phrases(texts) + bill = derive() + destination = PACKAGE / "CERTIFICATE.json" + if args.write: + need(not destination.exists(), "certificate already exists") + destination.write_text(canonical_certificate(), encoding="utf-8") + certificate_matches(root, bill) + print( + "PASS_QQ16_F17_PAIR_BILL " + f"W={bill['W']} gates_per_pair={bill['gates_per_pair']} " + f"pair_kernel={bill['pair_kernel_coefficient']}*lambda*N*D " + f"field_bits={bill['field_bit_coefficient']}*N*D " + "dirty_width=unsupplied control_gates=124028" + ) + + +if __name__ == "__main__": + try: + main() + except (OSError, ValueError, KeyError, TypeError, json.JSONDecodeError) as exc: + raise SystemExit("FAIL_QQ16_F17_PAIR_BILL " + str(exc))