diff --git a/research/qq16-f17-scan-bill/CERTIFICATE.json b/research/qq16-f17-scan-bill/CERTIFICATE.json new file mode 100644 index 0000000000..1a273c3cc8 --- /dev/null +++ b/research/qq16-f17-scan-bill/CERTIFICATE.json @@ -0,0 +1,39 @@ +{ + "schema_version": 1, + "status": "PASS_QQ16_F17_SCAN_BILL", + "producer": "F_0_then_B_1_2", + "consumer": "PR2707_zero_retention_decoder_in_F17", + "priced_term": "block_scale_scan", + "physical_bill": "F17 direct Boolean block-scale scan gate evaluations", + "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, + "p": 137, + "popcount_span": 392, + "popcount_sum": 1628, + "lines": 336, + "scan_per_line_nd": 4232, + "scan_per_line_const": 2415, + "scan_nd_coefficient": 1421952, + "scan_owner_coefficient": 811440, + "control_W": 456, + "control_w": 453, + "control_p": 122, + "control_scan_per_line_nd": 3624, + "control_scan_per_line_const": 1984, + "control_scan_nd_coefficient": 1217664, + "control_scan_owner_coefficient": 666624, + "selected_kappa": "0.001672660197076918", + "kappa_changed": false +} diff --git a/research/qq16-f17-scan-bill/MASTER-HANDOFF.md b/research/qq16-f17-scan-bill/MASTER-HANDOFF.md new file mode 100644 index 0000000000..5fca8adc42 --- /dev/null +++ b/research/qq16-f17-scan-bill/MASTER-HANDOFF.md @@ -0,0 +1,15 @@ +# Handoff + +Pinned CrocSwap main: `6f100d4bb5083f8c35d96fd95a539811c62f245c`. +Selected kappa, unchanged: `0.001672660197076918`. + +Did not switch cards. The scan term of #3374 was not evaluated at `W=532` +on that main. The pair-kernel and field-bit coefficients stay the submitted +#3374 values. + +Claim: at `lambda=1`, `f=64`, `e=0`, `beta=64`, `W=532`, the F17 decoder's +common block-scale scans cost at most `1421952 N D + 811440 N` gate +evaluations. That is the scan subtotal of the direct Boolean arithmetic bill. + +Stop. Scalar ADDs, wrappers, maps, addressing, movement and cleanup remain +unpaid. This is not a new kappa. diff --git a/research/qq16-f17-scan-bill/NOTICE.md b/research/qq16-f17-scan-bill/NOTICE.md new file mode 100644 index 0000000000..70c5ebcfee --- /dev/null +++ b/research/qq16-f17-scan-bill/NOTICE.md @@ -0,0 +1,11 @@ +# 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 +and the common block-scale scan keep their original attribution. + +Prepared by Wentao Li with substantial AI assistance. +No independent human review is claimed. diff --git a/research/qq16-f17-scan-bill/PROOF.md b/research/qq16-f17-scan-bill/PROOF.md new file mode 100644 index 0000000000..d5ba67065a --- /dev/null +++ b/research/qq16-f17-scan-bill/PROOF.md @@ -0,0 +1,76 @@ +# One block-scale scan term at the exact F0/B_1_2 entry width + +The selected conditional kappa remains **0.001672660197076918**. This note +does not change it. + +## Why this term + +Pinned main `6f100d4bb5083f8c35d96fd95a539811c62f245c` records Arham Tahir's +common block-scale scan in `research/qq16-block-scale-scan`. Its stated +invoice is evaluated at the published finite-format example `W=456`, +`w=453`, `p=122`. A search of that tree finds no evaluation at decoder +width `W=532`. The pair-kernel coefficient `26744256` and the named-field +bit coefficient `493696` are the submitted #3374 terms and are left +untouched. The incorporated scalar-ADD count `5408*N*D` does not depend on +`W`, so repeating it would reprint that receipt. The scan polynomial does +depend on the entry width, and it is the term priced here. + +## Inherited width + +The literal producer is exact **F0 followed by B_1_2**, and the consumer is +ywz65's PR2707 decoder, which reads X in F17 and Y in `F17 C_q^{-1}`. Nick +Petalas's entry contract, at `lambda=1`, `f=64`, `e=0`, `beta=64`, gives + +```text +Q0 = 80, b = 79, k = 137, Qmax = 497, E = 15, W = 532. +``` + +The scan proof binds `p=k` and `w=W-3`. At this width that is `w=529` and +`p=137`, with `0 <= p < w`. The largest emitted exponent is `w-1-p=391`, +which lies in the scan proof's stated range `[0, w]`. + +## The scan polynomial + +The pinned formula, for `q` signed `w`-bit components and reserve `p`, is + +```text +G_scan(w,q,p) = w*(4q+2) - 2p + S(w-p) + 3, +S(n) = sum_{0 <= i < n} popcount(i). +``` + +One owner-local line scans `q=2D` real components once. The `D` coefficient +is `8w` and the remaining term is `2w - 2p + S(w-p) + 3`. The same proof's +gate roles (absolute-value ripples, magnitude ORs, leading-bit hits, +constant-bit ORs, low ORs, and three flag gates) sum to this polynomial. +At `w=529` and `p=137`, `S(392)=1628`, so one scan costs + +```text +4232 D + 2415 +``` + +gates. The unchanged 336-line decoder, one scan per line per owner, costs + +```text +1421952 N D + 811440 N +``` + +gate evaluations. The published control `w=453`, `p=122` still costs +`3624 D + 1984` per line and `1217664 N D + 666624 N` for 336 lines. + +These counts are irreversible AND/XOR/OR/NOT evaluations in the scan +model. Wires, constants and fan-out stay free there. The count is an exact +invoice of that construction, with redundant gates retained. + +## Which physical bill changes + +The term that changes is the **common block-scale scan subtotal** of the +F17 zero-retention decoder's direct Boolean arithmetic bill. At the +published `W=456` example that subtotal is `1217664 N D + 666624 N`. At the +exact entry width `W=532` it is `1421952 N D + 811440 N`. Scalar ADDs, +wrappers, maps, addressing, movement and cleanup stay unpaid. The pair +kernel and the 464-field bit count stay the submitted #3374 coefficients. + +## Stop + +Stop after this one scan term and this one parameter tuple. A scan subtotal +is not a complete consumer, a recursive rank tariff, or a new kappa. diff --git a/research/qq16-f17-scan-bill/README.md b/research/qq16-f17-scan-bill/README.md new file mode 100644 index 0000000000..6897821c5f --- /dev/null +++ b/research/qq16-f17-scan-bill/README.md @@ -0,0 +1,101 @@ +# One F17 block-scale scan at the exact F0/B_1_2 entry width + +**Same card, one unpaid term.** #3374 already binds the F17 runtime pair +kernel and the 464-field bit count at `lambda=1`, `f=64`, `e=0`, `beta=64`, +`W=532`. This package prices the common block-scale **scan** at those +parameters. Selected kappa remains `0.001672660197076918`. + +The incorporated scan polynomial, with `w=W-3=529` and `p=k=137`, gives one +owner-local line + +```text +4232 D + 2415 +``` + +gates. Across the 336-line decoder, one scan per line per owner, the scan +subtotal is + +```text +1421952 N D + 811440 N +``` + +gate evaluations. The published `W=456` control remains +`1217664 N D + 666624 N`. The physical bill that changes is that scan +subtotal of the F17 direct Boolean arithmetic invoice. + +```sh +python3.12 -I -B research/qq16-f17-scan-bill/verify.py +``` + +Expected: + +```text +PASS_QQ16_F17_SCAN_BILL W=532 scan=1421952*N*D+811440*N control=1217664*N*D+666624*N no_new_kappa +``` + +## What is bound + +`W=532` is the published example in Nick Petalas's exact F0/B_1_2 entry +contract. Arham Tahir's block-scale scan states + +```text +G_scan(w,q,p) = w*(4q+2) - 2p + S(w-p) + 3 +``` + +and binds `p=k`, `w=W-3`, `q=2D`, and one scan per line per owner on the +336-line decoder. The proof is in [PROOF.md](PROOF.md). The receipt is +[CERTIFICATE.json](CERTIFICATE.json). + +## What stays unpaid + +Scalar ADDs, wrappers, maps, addressing, movement and cleanup remain +outside this scan count. The pair-kernel and named-field coefficients stay +the submitted #3374 values. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -I -B research/qq16-f17-scan-bill/verify.py +python3.12 -I -O -B research/qq16-f17-scan-bill/verify.py +python3.12 -I -B research/qq16-f17-scan-bill/independent.py +python3.12 -I -B research/qq16-f17-scan-bill/test_package.py +python3.12 -B scripts/research_package.py --package research/qq16-f17-scan-bill +``` + +Default verification is read-only. `--write` creates a missing certificate +and refuses to overwrite one. + +## Open next questions + +1. **Scalar ADDs under a width-dependent model.** The incorporated finite + format already charges `5408*N*D` real ADD/subtracts, and that count does + not use `W`. It matters because a Boolean ADD circuit at `w=529` would be + a different unit from that real-operation count. The first step is to pin + one incorporated ADD circuit whose gate count is a stated function of the + component width. The blocker is that no such width-dependent ADD circuit + is the formula already attached to these 2,704 sites. + +2. **Wrappers and maps at W=532.** The scan proof leaves exact signed + coordinate wrappers and the 464 full-cover maps as separate charges. The + first step is to instantiate one pinned wrapper or map tariff at `w=529`. + The blocker is that the scan invoice treats those permutations as unpaid + routing. + +3. **Addressing, movement and cleanup.** The scan model gives wires and + fan-out for free and does not erase the exponent. The first step is to + bind one admitted caller layout and charge address travel plus exponent + cleanup in that layout. The blocker is that neither pinned word supplies + that physical lifetime. + +## Credit + +Arham Tahir supplied the block-scale scan polynomial and its `W=456` +evaluation. Nick Petalas supplied the exact F0/B_1_2 entry contract and the +finite-format width `w=W-3`. ywz65 supplied the PR2707 F17 decoder. The +#3374 pair-kernel and field-bit coefficients are used only as the terms this +package does not recompute. 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-scan-bill/SOURCES.json b/research/qq16-f17-scan-bill/SOURCES.json new file mode 100644 index 0000000000..90bb82aad4 --- /dev/null +++ b/research/qq16-f17-scan-bill/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/qq16-block-scale-scan/README.md", + "usage": "input", + "git_blob": "8e57abbf0fa1649d1359a74c987e6017218b9c41", + "sha256": "86b082070985c89efc43448bd0a8d3426f74720ff0d901a48b81b205432f17ec" + }, + { + "path": "research/qq16-producer-entry-contract/README.md", + "usage": "input", + "git_blob": "d3f66aac46ac8edbc6660715e586276909b0eac4", + "sha256": "83029c16c55be649e223bd583a14529d26a9c2e44afcf2766a3f70504b641ffe" + } + ] +} diff --git a/research/qq16-f17-scan-bill/TASK.json b/research/qq16-f17-scan-bill/TASK.json new file mode 100644 index 0000000000..f55f26036c --- /dev/null +++ b/research/qq16-f17-scan-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": "The catalogue asks for one literal producer and an affordable physical consumer. The pair-kernel and named-field coefficients at the exact F0/B_1_2 entry width are already submitted, and the incorporated scalar-ADD count does not depend on that width. This package instantiates only the incorporated block-scale scan polynomial at W=532.", + "actual_scope": "At lambda=1, f=64, e=0, beta=64 and the inherited decoder width W=532, evaluate the incorporated common block-scale scan once per line per owner for the 336-line F17 decoder, and name that scan subtotal as the physical bill term that changes.", + "bottleneck_link": "The entry width and the scan gate polynomial are already proved, while the scan subtotal of the F17 Boolean bill was instantiated only at the W=456 example.", + "stop_rule": "Stop after the scan term at lambda=1, f=64, e=0, beta=64, h=73. Leave scalar ADDs, wrappers, maps, addressing, movement and cleanup unpaid, and do not recompute the pair-kernel or field-bit coefficients.", + "evidence": "Exact integer evaluation of the pinned G_scan polynomial at w=W-3 and p=k, checked against the published W=456 scan total, with source-text checks that one scan is charged per line per owner.", + "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 Boolean gate count do the 2,704 scalar ADD sites have at component width w=529?", + "why_it_matters": "The incorporated real-operation count 5408*N*D does not use W, so it does not price those sites in the same gate model as the scan.", + "first_step": "Pin one incorporated ADD circuit whose gate count is a stated function of the component width and instantiate it at w=529.", + "blocked_by": "The finite-format ADD charge is a real-operation count, and no width-dependent ADD circuit is attached to these sites on the pinned main." + }, + { + "question": "What do the exact signed wrappers and 464 full-cover maps cost at W=532?", + "why_it_matters": "The scan proof preserves the line maximum under exact wrappers and still leaves their routing unpaid.", + "first_step": "Instantiate one pinned wrapper or map tariff at w=529 and 464 maps.", + "blocked_by": "The scan invoice treats permutations as separate routing rather than gates inside G_scan." + }, + { + "question": "What addressing, movement and exponent cleanup does one admitted caller pay for this scan?", + "why_it_matters": "The scan model leaves wires and fan-out free and does not erase the shared exponent.", + "first_step": "Bind one admitted caller layout and charge address travel plus exponent cleanup in that layout.", + "blocked_by": "Neither the entry contract nor the scan proof supplies that physical lifetime." + } + ] +} diff --git a/research/qq16-f17-scan-bill/VERIFY.json b/research/qq16-f17-scan-bill/VERIFY.json new file mode 100644 index 0000000000..64a742f951 --- /dev/null +++ b/research/qq16-f17-scan-bill/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/qq16-producer-entry-contract/README.md", + "research/qq16-block-scale-scan/README.md" + ], + "commands": [ + { + "argv": ["{python}", "-Werror", "-I", "-B", "{package}/verify.py"], + "timeout_seconds": 60, + "checks": "Recompute the exact-entry F17 block-scale scan subtotal and the published W=456 control." + }, + { + "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 scan integers from the pinned polynomial 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-scan-bill/independent.py b/research/qq16-f17-scan-bill/independent.py new file mode 100644 index 0000000000..304a4b1807 --- /dev/null +++ b/research/qq16-f17-scan-bill/independent.py @@ -0,0 +1,129 @@ +#!/usr/bin/env python3 +"""Second evaluation of the F17 block-scale scan at the exact entry width. + +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-block-scale-scan/README.md": + "86b082070985c89efc43448bd0a8d3426f74720ff0d901a48b81b205432f17ec", +} + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def locate(): + marker = Path("research/qq16-block-scale-scan/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 ones_below(limit): + """Count set bits in 0..limit-1 by complete dyadic blocks.""" + need(type(limit) is int and 0 <= limit <= 10000, "span") + total = 0 + shift = 0 + remaining = limit + while remaining: + block = 1 << shift + if block > remaining: + break + # Numbers with this bit set come in the upper half of each 2^(shift+1) window. + window = block << 1 + total += (limit // window) * block + tail = limit % window + if tail > block: + total += tail - block + shift += 1 + direct = 0 + for value in range(limit): + direct += value.bit_count() + need(total == direct, "ones table") + return total + + +def polynomial(width, reserve): + """Return (coefficient of D, constant) for q=2D in G_scan.""" + need(0 <= reserve < width, "reserve") + span = width - reserve + ones = ones_below(span) + constant = width * 2 - 2 * reserve + ones + 3 + return 8 * width, constant, ones + + +def roles(width, reserve): + """Same roles as the scan proof, evaluated at q=2 and doubled into the D slope.""" + ones = ones_below(width - reserve) + at_two = 3 * width * 2 + width + 3 * (width - reserve) + ones + reserve + 3 + at_four = 3 * width * 4 + 3 * width + 3 * (width - reserve) + ones + reserve + 3 + slope = at_four - at_two + need(slope == 8 * width, "two extra complex coordinates add 8w gates") + stated = width * (4 * 2 + 2) - 2 * reserve + ones + 3 + need(at_two == stated, "role sum matches the polynomial at q=2") + return at_two + + +def main(): + root = locate() + entry = text_of(root, "research/qq16-producer-entry-contract/README.md") + scan = text_of(root, "research/qq16-block-scale-scan/README.md") + need("W=532" in entry and "k=137" in entry and "Q0=80" in entry, "published width") + need("W = Qmax + e + 35" in entry and "B < 2^(e+15)" in entry, "width formula") + need("X is in F17 and Y in F17" in entry, "F17 charts") + need("G_scan(w,q,p) = w*(4q+2) - 2p + S(w-p) + 3" in scan, "scan polynomial") + need("one scan per line per owner, not per factor" in scan, "scan multiplicity") + need("multiply by 336" in scan and "1,217,664*N*D + 666,624*N" in scan, "published control") + need("With `w=W-3`" in scan and "supplies `p=k`" in scan, "width binding") + q0 = 64 + (1 + 1) // 2 + 6 + 9 * 1 + relative = 64 + 15 + precision = relative + 22 + 0 + 73 // 2 + qmax = q0 + 3 * precision + 6 + width = qmax + 0 + 35 + need(q0 == 80 and relative == 79 and precision == 137 and qmax == 497 and width == 532, "chain") + need(17628 < 2 ** 15, "entry exponent slack") + component = width - 3 + need(component == 529 and precision < component, "scan domain") + per_nd, per_const, ones = polynomial(component, precision) + roles(component, precision) + need(ones == 1628 and per_nd == 4232 and per_const == 2415, "one line") + need(336 * per_nd == 1421952 and 336 * per_const == 811440, "decoder scans") + control_nd, control_const, _control_ones = polynomial(453, 122) + roles(453, 122) + need(control_nd == 3624 and control_const == 1984, "W=456 line") + need(336 * control_nd == 1217664 and 336 * control_const == 666624, "W=456 decoder") + print( + "PASS_QQ16_F17_SCAN_BILL_INDEPENDENT " + f"W={width} scan={336 * per_nd}*N*D+{336 * per_const}*N " + f"control={336 * control_nd}*N*D+{336 * control_const}*N no_new_kappa" + ) + + +if __name__ == "__main__": + try: + main() + except (OSError, UnicodeError, ValueError) as exc: + raise SystemExit("FAIL_QQ16_F17_SCAN_BILL_INDEPENDENT " + str(exc)) diff --git a/research/qq16-f17-scan-bill/test_package.py b/research/qq16-f17-scan-bill/test_package.py new file mode 100644 index 0000000000..25e94c7ebf --- /dev/null +++ b/research/qq16-f17-scan-bill/test_package.py @@ -0,0 +1,107 @@ +#!/usr/bin/env python3 +"""Reject certificate corruption and duplicate JSON keys for the F17 scan 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-block-scale-scan/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_SCAN_BILL", outcome.stdout) + self.assertIn("1421952*N*D+811440*N", outcome.stdout) + self.assertIn("no_new_kappa", 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["scan_nd_coefficient"] = 1217664 + replacements = [ + json.dumps(payload).encode(), + b'{"schema_version": 1, "schema_version": 1}\n', + b'{"W": true}\n', + b'{"status": "PASS_QQ16_F17_SCAN_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, replacement) + self.assertIn("FAIL_QQ16_F17_SCAN_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_SCAN_BILL_INDEPENDENT", outcome.stdout) + source = (HERE / "independent.py").read_text(encoding="utf-8") + self.assertNotIn("import verify", source) + self.assertNotIn("from verify", source) + self.assertNotIn("importlib", source) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/qq16-f17-scan-bill/verify.py b/research/qq16-f17-scan-bill/verify.py new file mode 100644 index 0000000000..cf5648cb98 --- /dev/null +++ b/research/qq16-f17-scan-bill/verify.py @@ -0,0 +1,294 @@ +#!/usr/bin/env python3 +"""Price one F17 block-scale scan term at the exact F0/B_1_2 entry width. + +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 +LINES = 336 +PARAMETERS = {"h": 73, "lambda": 1, "f": 64, "e": 0, "beta": 64} +INPUTS = { + "research/qq16-producer-entry-contract/README.md": + "83029c16c55be649e223bd583a14529d26a9c2e44afcf2766a3f70504b641ffe", + "research/qq16-block-scale-scan/README.md": + "86b082070985c89efc43448bd0a8d3426f74720ff0d901a48b81b205432f17ec", +} +EXPECTED = { + "schema_version": 1, + "status": "PASS_QQ16_F17_SCAN_BILL", + "producer": "F_0_then_B_1_2", + "consumer": "PR2707_zero_retention_decoder_in_F17", + "priced_term": "block_scale_scan", + "physical_bill": "F17 direct Boolean block-scale scan gate evaluations", + "parameters": PARAMETERS, + "Q0": 80, + "b": 79, + "k": 137, + "Qmax": 497, + "E": 15, + "W": 532, + "w": 529, + "p": 137, + "popcount_span": 392, + "popcount_sum": 1628, + "lines": 336, + "scan_per_line_nd": 4232, + "scan_per_line_const": 2415, + "scan_nd_coefficient": 1421952, + "scan_owner_coefficient": 811440, + "control_W": 456, + "control_w": 453, + "control_p": 122, + "control_scan_per_line_nd": 3624, + "control_scan_per_line_const": 1984, + "control_scan_nd_coefficient": 1217664, + "control_scan_owner_coefficient": 666624, + "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(): + marker = "research/qq16-block-scale-scan/README.md" + for candidate in (Path.cwd(), *PACKAGE.parents): + 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(): + raw = read_bytes(root / name) + 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"] + scan = texts["research/qq16-block-scale-scan/README.md"] + for phrase in ( + "norm <= B = 17628*H", + "Q0 = f + ceil(lambda/2) + 6 + 9*lambda", + "B < 2^(e+15)", + "k = beta+37 + ceil_log2(lambda) + floor(73*lambda/2)", + "Qmax = Q0 + 3*k + 6", + "W = Qmax + e + 35", + "W=532", + "Q0=80", + "k=137", + "X is in F17 and Y in F17", + ): + need(phrase in entry, "missing entry phrase: " + phrase) + for phrase in ( + "G_scan(w,q,p) = w*(4q+2) - 2p + S(w-p) + 3", + "S(n) = sum_{0 <= i < n} popcount(i)", + "one scan costs `3624D + 1984` gates", + "supplies `p=k`", + "With `w=W-3`", + "one scan per line per owner, not per factor", + "unchanged 336-line decoder, multiply by 336", + "1,217,664*N*D + 666,624*N", + ): + need(phrase in scan, "missing scan 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 popcount_sum(limit): + """S(limit) = sum of popcount(i) for 0 <= i < limit.""" + need(type(limit) is int and limit >= 0, "popcount span") + total = 0 + bit = 0 + while (1 << bit) < limit or (bit == 0 and limit > 0): + period = 1 << (bit + 1) + half = 1 << bit + total += (limit // period) * half + max(0, (limit % period) - half) + bit += 1 + need(bit <= limit.bit_length() + 2, "popcount bit walk") + if (1 << bit) >= limit and bit > 0: + break + return total + + +def scan_formula(width, components, reserve): + """Stated polynomial G_scan(w,q,p) = w*(4q+2) - 2p + S(w-p) + 3.""" + need(type(width) is int and width >= 1, "scan width") + need(type(components) is int and components >= 0, "component count") + need(type(reserve) is int and 0 <= reserve < width, "scan reserve") + return width * (4 * components + 2) - 2 * reserve + popcount_sum(width - reserve) + 3 + + +def scan_breakdown(width, components, reserve): + """Gate roles stated in the scan proof, summed separately from the polynomial.""" + need(type(components) is int and components >= 1, "breakdown components") + absolute = 3 * width * components + magnitude_or = (components - 1) * width + leading = 3 * (width - reserve) + exponent_or = popcount_sum(width - reserve) + low_or = reserve + flags = 3 + return absolute + magnitude_or + leading + exponent_or + low_or + flags + + +def check_popcount_table(): + for limit in range(0, 513): + direct = sum(value.bit_count() for value in range(limit)) + need(popcount_sum(limit) == direct, "popcount table: " + str(limit)) + + +def scan_invoice(component_bits, reserve): + need(scan_formula(component_bits, 1, reserve) == scan_breakdown(component_bits, 1, reserve), + "one-component identity") + need(scan_formula(component_bits, 2, reserve) == scan_breakdown(component_bits, 2, reserve), + "two-component identity") + need(scan_formula(component_bits, 4, reserve) == scan_breakdown(component_bits, 4, reserve), + "four-component identity") + # q = 2D real components. The D coefficient is 8w; the rest is independent of D. + per_line_nd = 8 * component_bits + per_line_const = scan_formula(component_bits, 0, reserve) + need(per_line_const == 2 * component_bits - 2 * reserve + popcount_sum(component_bits - reserve) + 3, + "constant term") + need(0 <= component_bits - 1 - reserve <= component_bits, "exponent fits the signed kernel range") + return { + "popcount_span": component_bits - reserve, + "popcount_sum": popcount_sum(component_bits - reserve), + "scan_per_line_nd": per_line_nd, + "scan_per_line_const": per_line_const, + "scan_nd_coefficient": LINES * per_line_nd, + "scan_owner_coefficient": LINES * per_line_const, + } + + +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") + 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 + exponent + 35 + need(width == qmax + entry_exponent + 20, "format width identity") + component_bits = width - 3 + reserve = precision + check_popcount_table() + invoice = scan_invoice(component_bits, reserve) + control = scan_invoice(453, 122) + bill = { + "Q0": q0, + "b": relative, + "k": precision, + "Qmax": qmax, + "E": entry_exponent, + "W": width, + "w": component_bits, + "p": reserve, + "lines": LINES, + "control_W": 456, + "control_w": 453, + "control_p": 122, + "control_scan_per_line_nd": control["scan_per_line_nd"], + "control_scan_per_line_const": control["scan_per_line_const"], + "control_scan_nd_coefficient": control["scan_nd_coefficient"], + "control_scan_owner_coefficient": control["scan_owner_coefficient"], + } + bill.update(invoice) + for key, value in bill.items(): + need(value == EXPECTED[key], "recomputed bill mismatch: " + key) + return bill + + +def certificate_matches(bill): + raw = read_bytes(PACKAGE / "CERTIFICATE.json") + 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 not type(data[key]) is bool 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) + + +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(bill) + print( + "PASS_QQ16_F17_SCAN_BILL " + f"W={bill['W']} scan={bill['scan_nd_coefficient']}*N*D+" + f"{bill['scan_owner_coefficient']}*N " + f"control={bill['control_scan_nd_coefficient']}*N*D+" + f"{bill['control_scan_owner_coefficient']}*N no_new_kappa" + ) + + +if __name__ == "__main__": + try: + main() + except (OSError, ValueError, KeyError, TypeError, json.JSONDecodeError) as exc: + raise SystemExit("FAIL_QQ16_F17_SCAN_BILL " + str(exc))