From 6b17b9b7c76d60726bd87123b9bf9905aa3151dd Mon Sep 17 00:00:00 2001 From: commdata2338 <199849969+commdata2338@users.noreply.github.com> Date: Sat, 17 Oct 2026 13:28:31 -0500 Subject: [PATCH] Research: a sufficient exact grid for the finite QQ16 F0 native reference Proves a conservative sufficient fixed-point format for the complete 26,099-event, 512-coordinate QQ16 F0 native reference. If every real and imaginary entry component of the 224 data and 480 dirty helper fields lies in h Z with magnitude strictly below 2^P h, and the eight private fields start at zero, then integer execution on the working quantum h*2^-35 with signed width P+102 performs every primitive exactly: native butterfly sums, crossed numerators and halvings, constant-product partials and every scalar ADD. A rational bound recurrence and a separately written integer recurrence agree on all 133,628 bound observations (guard 35, range multiplier 42822849617116776290 < 2^66). The direct payload bill is at most 122,667,020 W-bit operations and 730,124 W-bit words including scratch. On the known L112 = 1, L224 = 2^65 dirty fixture the fixed grid is exact, while the retained binary64 engine's output differs in data fields 112, 114, 137, 190 and 211. The guard and width are sufficient, not minimal. Ideal native endpoint semantics are inherited; initial input preparation, B1, arbitrary depth, routing, storage and F17 consumption remain open. No supplier, selected-record or kappa change. Adds research/qq16-native-grid-envelope/ only. Submitted by @commdata2338 with substantial AI assistance (OpenAI Codex research and implementation; packaged with Claude Code). Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_01X86sCSXdoDd61SDFfC1PKG --- .../qq16-native-grid-envelope/CONTROLS.json | 35 ++ research/qq16-native-grid-envelope/README.md | 248 +++++++++++++ .../qq16-native-grid-envelope/RESULT.json | 48 +++ .../qq16-native-grid-envelope/SOURCES.json | 69 ++++ research/qq16-native-grid-envelope/TASK.json | 99 +++++ .../qq16-native-grid-envelope/VERIFY.json | 44 +++ .../qq16-native-grid-envelope/controls.py | 230 ++++++++++++ .../qq16-native-grid-envelope/independent.py | 228 ++++++++++++ research/qq16-native-grid-envelope/verify.py | 344 ++++++++++++++++++ 9 files changed, 1345 insertions(+) create mode 100644 research/qq16-native-grid-envelope/CONTROLS.json create mode 100644 research/qq16-native-grid-envelope/README.md create mode 100644 research/qq16-native-grid-envelope/RESULT.json create mode 100644 research/qq16-native-grid-envelope/SOURCES.json create mode 100644 research/qq16-native-grid-envelope/TASK.json create mode 100644 research/qq16-native-grid-envelope/VERIFY.json create mode 100644 research/qq16-native-grid-envelope/controls.py create mode 100644 research/qq16-native-grid-envelope/independent.py create mode 100644 research/qq16-native-grid-envelope/verify.py diff --git a/research/qq16-native-grid-envelope/CONTROLS.json b/research/qq16-native-grid-envelope/CONTROLS.json new file mode 100644 index 0000000000..481a497f34 --- /dev/null +++ b/research/qq16-native-grid-envelope/CONTROLS.json @@ -0,0 +1,35 @@ +{ + "checks": { + "exhaustive_gaussian_pair_cases": 625, + "grid_and_internal_overflow_controls": 2, + "invalid_contract_controls": 3, + "later_clear_keeps_earlier_obligation": true, + "literal_constant_product_cases": 3859, + "literal_fixed_grid": { + "G": 35, + "P": 66, + "W": 168, + "all_480_chosen_helpers_restore": true, + "all_private_outputs_zero": true, + "binary64_control_differs_in_data_fields": [ + 112, + 114, + 137, + 190, + 211 + ], + "changed_field_cuts": 26089, + "endpoint_sha256": "8c5dd8f939e94cee17e7f12dbba2b9c738ef14d7f35243d0f3923182651f14fc", + "events": 26099, + "first_max_site": [ + 19243, + "constant-numerator" + ], + "max_encoded_magnitude_bits": 104, + "nonzero_exact_divisions": 122240, + "trace_sha256": "c1bcd12645b44b0f5537143559ce8d36fbcfea0c86f606f0b11fc3d7bf6114d7" + }, + "rational_scalar_containment_cases": 4637 + }, + "status": "PASS_QQ16_NATIVE_GRID_CONTROLS" +} diff --git a/research/qq16-native-grid-envelope/README.md b/research/qq16-native-grid-envelope/README.md new file mode 100644 index 0000000000..deb46f4454 --- /dev/null +++ b/research/qq16-native-grid-envelope/README.md @@ -0,0 +1,248 @@ +# A sufficient finite grid for the complete native F0 reference + +**Scoped sufficient-format proof and source-bound audit; no new supplier or κ.** +The literal one-layer QQ16 F0 reference can execute exactly with bounded dirty +inputs. If every real and imaginary input component is an integer multiple of +`h = 2^-b` with absolute value **strictly less than `2^P h`**, then the following +common format suffices: + +``` +working quantum q = h * 2^-35 +signed two's-complement width W = P + 102, P >= 1. +``` + +All 224 data fields and all 480 dirty helper fields may vary independently; +the eight owned private fields start at zero. Each field has 512 complex +coordinates. The bound covers the complete **26,099-event** F0 word, including +native butterfly interiors, residual and endpoint monomials, constant-product +partials, and every intermediate cancellation. It guarantees exact agreement +with the ideal finite reference, hence zero arithmetic defect relative to that +reference. It is a conservative sufficient format, **not a minimum**. + +This closes one part of the finite-producer handoff after +[Ross Richardson's PR3067](https://github.com/CrocSwap/integer-mult-bounds/pull/3067) +and [Sricharan Vagvala's native component audit](../qq16-native-rounded-components/README.md). +Those predecessors exhibit deterministic loss for a particular binary64 input. +They do not give this uniform bounded-input contract. The separate +[PR3189 noise-lattice audit](../qq16-noise-lattice-audit/README.md) permits +independent child errors; here every native primitive is executed exactly on +the finer grid. No noisy-child closure implication is assumed. + +The claim is in discussion [#2727](https://github.com/CrocSwap/integer-mult-bounds/discussions/2727#discussioncomment-19001870). +Base and predecessor heads, Git blobs, and immutable input hashes are in +[SOURCES.json](SOURCES.json); the refined task is in [TASK.json](TASK.json). +Evidence is author-checked and independently reviewable, with a separately +implemented arithmetic recurrence. No independent human review is claimed. + +## Arithmetic reference and exact scope + +We use `programs.F_0` and its retained forward core from the unchanged +[joint-query certificate](../joint-query/certificate.json.gz). Native recipes +come from the pinned selected replay archive. A rank-r recipe applies its +serialized right monomial, r Gaussian coordinate lines, and its left monomial. +The monomials are signed permutations of real and imaginary components; +adjoints have the same range and lattice effects. The source F0 has no added +cover-map events. Phase events are control labels in this retained reference. +The inherited local chart/access interpretation is not proved again. + +The pair-first Gaussian lowering is the one in the native component audit. +For a pair `(a+ib,c+id)`, compute these sums and differences, then halve: + +``` +rp=a+c; ip=b+d; rd=a-c; di=b-d +out0=((rp-di)/2, (ip+rd)/2) +out1=((rp+di)/2, (ip-rd)/2) +``` + +A scalar coefficient is normalized to `n / 2^d`. Compute the signed integer +product first, using binary shifts and additions, then divide exactly by +`2^d`. An ADD then adds that result to its target. The product is not silently +fused with its target, and native halves are not rounded. Only owned private +fields may be cleared. This is a finite direct arithmetic realization; its +cost is not the source's recursive child tariff. + +The exact arithmetic guarantee holds for **arbitrary input components in the +stated box**, including nonconstant vectors and independent dirty helpers. +It is a proof by induction through the bound rules below, not an extrapolation +from the single literal test fixture. Exact helper restoration or data-map +identities transfer only insofar as they hold for the inherited ideal native +reference. We do not reprove that reference's complete symbolic endpoint. + +## Bound invariant and proof + +Let `M` be the maximum absolute integer entry coefficient, so `M < 2^P`. +The verifier assigns each field a pair `(R,g)` meaning that every component x +satisfies + +``` +|x| <= R M h, x belongs to h * 2^-g Z. +``` + +`R` is a nonnegative dyadic rational and `g` is an integer, possibly negative. +A zero field has `(0,0)`. Ordinary inputs have `(1,0)`; private inputs have +`(0,0)`. The case `M=0` is immediate. + +1. A signed permutation preserves `(R,g)`. Each used monomial's binary matrix + is checked invertible; its coefficients and phases are checked to describe + component permutations and sign changes. +2. Adding or subtracting two nonzero fields gives + `(R1+R2, max(g1,g2))`. Zero operands retain the other bound. +3. Scaling by a nonzero dyadic c gives + `(|c| R, g - v2(c))`. For a coefficient numerator n, every binary shifted + term and every partial sum has magnitude at most `|n| R M h` and grid no + finer than the source grid. All terms have the same sign before the one + final coefficient sign change. These temporary bounds are recorded before + the exact denominator division. +4. For a Gaussian line, the first sums have bound `(2R,g)`, the crossed + numerators `(4R,g)`, and the halved outputs `(2R,g+1)`. The pre-halving + numerator cannot be omitted from the range bill. +5. A private CLEAR replaces only its destination bound by zero. Earlier + maximum range and grid obligations remain in the receipt. + +Each rule follows from an integer linear combination or an exact dyadic +scaling. Thus it holds simultaneously for every allowed input, without +assuming cancellation, statistical independence, or a particular native +error pattern. Applying the rules to every source event yields: + +| Quantity | Certified upper bound | First attaining bound location | +| --- | ---: | --- | +| Required fractional guard G | 35 | event 26033, native half in `inverse_0` on C0 | +| Component/temporary magnitude multiplier R | 42,822,849,617,116,776,290 < 2^66 | event 26051, native cross in `inverse_20` on C0 | +| Signed width | P + 102 | combines the two uniform upper bounds | + +These are maxima of the conservative bound recurrence, not demonstrated +maxima of reachable values or necessary precision lower bounds. + +Every recorded lattice contains only multiples of `q=h*2^-35`. In particular, +whenever an operation divides by `2^d`, its output lattice has been included +in G; its encoded numerator is therefore divisible by `2^d`. Induction proves +that integer execution on q performs every division exactly. Moreover, + +``` +|x/q| <= R M 2^35 < 2^(66+P+35) = 2^(W-1). +``` + +The strict input bound makes both signs fit W-bit two's-complement storage, +including sign changes. Binary-product partials and butterfly numerators +were included, so this argument also rules out intermediate overflow. +No floating exponent or significand approximation is used. + +## Direct finite payload bill + +The receipt retains the source inventory: 3,494 native recipes, rank mass +5,530, 7,692 applied monomials, 866 identity adapter labels, and ten phase +labels. The following is a constructive upper bound for one execution on +512-coordinate fields, in operations on **W-bit payload words**: + +| Operation | Count or upper bound | +| --- | ---: | +| Additions/subtractions, including constant products | 33,161,216 | +| Constant left shifts and exact right shifts/halvings | 21,299,200 | +| Negations | at most 18,526,208 | +| Component copies | 49,646,592 | +| Private and final scratch zero writes | 33,804 | +| Sum of these payload operations | at most 122,667,020 | + +A constant with k nonzero binary digits uses k component copies, k−1 +additions, one left shift for each nonzero digit position, at most one sign +change, and at most one exact right shift. For in-place SCALE, save the input +once and reuse it for the later shifted terms. The source ADD leaves its +source intact until the final target update. Native pairs use four input and +four output copies plus eight sums and four halvings. Each monomial writes a +full permutation buffer and then copies it back, so no free pointer relocation +is assumed. Monomial negations are bounded by one per component; this is not +an exact sign census or a circuit minimum. + +Logical payload storage is `712*1024 = 729,088` W-bit words. One 1,024-word +permutation buffer and twelve arithmetic temporary words suffice; they are +written before read and cleared at completion. Thus a sufficient payload +allowance is **730,124 W-bit words**, including that scratch. At P=66, W=168, +this is 122,660,832 payload bits. This is a logical payload bound, not measured +Python memory. Fixed code, addresses, counters, routing and ownership records +are outside this payload subtotal. A fixed-tape/physical implementation must +charge them, and must implement the listed wide-word operations. + +No claim of affordability follows. The arithmetic and payload storage are +constructively bounded; recursive cost, physical placement/movement, all-size +compilation, B1, F17 consumption and the complete supplier invoice remain +unknown. The family decision is **narrow and stop** at this numerical contract. + +## Evidence and reproduction + +From the repository root with standard-library Python 3.12: + +```sh +python3 -I -B scripts/research_package.py --package research/qq16-native-grid-envelope +``` + +Expected markers: + +``` +PASS_QQ16_NATIVE_GRID_ENVELOPE events=26099 grid_guard=35 range_bits=66 signed_width=P+102 +PASS_QQ16_NATIVE_GRID_INTEGER_RECURRENCE observations=133628 +PASS_QQ16_NATIVE_GRID_CONTROLS literal_events=26099 fixed_grid_exact binary64_control_loses_data +PASS_REGISTERED_RESEARCH_PACKAGE research/qq16-native-grid-envelope outcome=completed +``` + +[verify.py](verify.py) uses rational magnitudes and explicit dyadic valuations. +[independent.py](independent.py) imports neither that implementation nor a +predecessor checker: it uses integer magnitudes at each local lattice and +reconstructs the complete trace. Both agree on **all 133,628 bound +observations**, every completed event, final bounds, and the direct operation +counts. This is a separate arithmetic implementation by the same contributor, +not independent human review of native semantics. + +[controls.py](controls.py) checks 4,637 rational scalar containment cases and +all 625 Gaussian pairs in `[-2,2]^4`. A further 3,859 literal binary +constant-product cases cover every source coefficient, including large signed +operands. Rejecting controls cover an off-grid +native half, overflow at a crossed numerator whose final outputs fit, a +nondyadic coefficient, a singular monomial and an attempted borrowed CLEAR. +A later CLEAR is checked not to erase an earlier guard obligation. + +It also actually executes the complete native dirty-helper fixture +`L112=1`, `L224=2^65`, other fields zero, on the uniform grid G=35 with W=168. +Every division and intermediate range is checked. All 26,089 changed-field +cuts are hashed; all 480 chosen helpers return and all private outputs are +zero. The exact data survive. Running the retained binary64 engine on the +same source and input loses data in fields 112,114,137,190,211, as its authors +reported. [CONTROLS.json](CONTROLS.json) records both the escape and its control. +The reused dispatcher and monomial evaluator retain their attribution; this +fixture is not a new discovery of the rounding failure. + +Default replay is read-only. `--write PATH` exclusively creates a new receipt. +The two scientific archives and two reused implementation files are authenticated +and declared in [VERIFY.json](VERIFY.json). The generic package runner, selected +cold replay, source theorem and physical implementation have different scopes; +a passing local replay is not supplier admission or a multiplication theorem. + +## Open next questions + +Can a recursively admitted caller supply this input/dirty bound and grid at an +affordable complete cost? Pin one actual child layout and consumer, then price +its wide-word arithmetic, routing, ownership, storage and F17 consumption +against a complete allowance before optimizing this envelope. This matters +because PR2965 assumes producer accuracy; it does not pay for an exact direct +reference. B1 and arbitrary tensor depth need their own numerical realization. Input +preparation and any error from placing an original real input on the entry +lattice also remain separate. +Those unresolved physical/recursive costs are the blocker. The structured +question and stop rule are in TASK.json; no larger search is proposed. + +## Credit + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. +New derivation, bound interpreters, fixed-grid control and prose are Apache-2.0. +No independent human review or formal-kernel proof is claimed. + +Credit Sricharan Vagvala for the actual pair-first native component lowering +and binary64 corroboration (`946a399d6ae1667236bb395d21c33c749e000877`), +Ross Richardson / PR3067 for the physical-rounding witness and finite-producer +handoff, Tekalign / PR3017 for the native vector evaluator and / PR3189 for +the separate noise-lattice warning, Arham Tahir / PR3036 and PR2995 for the +scalar rounding/fault witnesses, and Nick Petalas / PR2965 for completed-output +error transfer. The runtime control reuses the unchanged native-rounded-components +code and its unchanged Tekalign evaluator, without claiming their implementation +as new. Ali Romman, Sagar Thakrar, DLamdata, ywz65, starship-s, Douglas Colkitt +and the full retained QQ16/native lineage retain the attribution and notices in +[joint-query/NOTICE.md](../joint-query/NOTICE.md). diff --git a/research/qq16-native-grid-envelope/RESULT.json b/research/qq16-native-grid-envelope/RESULT.json new file mode 100644 index 0000000000..492c88f322 --- /dev/null +++ b/research/qq16-native-grid-envelope/RESULT.json @@ -0,0 +1,48 @@ +{ + "additional_scratch_words_upper_bound": 1036, + "completed_bound_sha256": "54a2fd94f34d1936535b955fc353f28be7b406becb86fcd2669dfaf4368cf7f0", + "direct_cost": { + "adapter_identity_labels": 866, + "clear_component_writes": 32768, + "constant_product_additions": 1071104, + "constant_product_calls": 21496832, + "constant_product_component_copies": 22567936, + "constant_product_left_shifts": 3310592, + "constant_product_negations": 10649600, + "constant_product_right_shifts": 12325888, + "final_owned_scratch_clear_writes": 1036, + "monomial_calls": 7692, + "monomial_component_copies": 15753216, + "monomial_component_negations_upper_bound": 7876608, + "native_exact_halvings": 5662720, + "native_gaussian_lines": 5530, + "native_pair_component_copies": 11325440, + "native_real_additions": 11325440, + "native_recipe_calls": 3494, + "phase_labels": 10, + "scalar_real_additions": 20764672 + }, + "event_sha256": "4c1ee518a6513c115741a3834c49490c6e8e68f5e2357af8dac782c3d40958e7", + "events": 26099, + "final_bounds_sha256": "24dae55105ca2598010a20dcb7772af8dc7be7925c9bdc9e16c6f0cf3deb79ac", + "grid_guard": 35, + "grid_site": [ + 26033, + "native-halved" + ], + "logical_payload_words": 729088, + "max_range_exact": "42822849617116776290", + "primitive_bound_observations": 133628, + "primitive_bound_sha256": "013abaed4ac02260e5273c1323e11e4efeda5ca33ba6453a43e14c79c7eb4412", + "range_power_of_two": 66, + "range_site": [ + 26051, + "native-cross" + ], + "schema_version": 1, + "scope": "Finite literal F0 reference, all 704 bounded input fields, private fields zero", + "signed_width_P_plus": 102, + "status": "PASS_QQ16_NATIVE_GRID_ENVELOPE", + "supplier_admission": false, + "validated_distinct_monomials": 3466 +} diff --git a/research/qq16-native-grid-envelope/SOURCES.json b/research/qq16-native-grid-envelope/SOURCES.json new file mode 100644 index 0000000000..1f2016e81c --- /dev/null +++ b/research/qq16-native-grid-envelope/SOURCES.json @@ -0,0 +1,69 @@ +{ + "schema_version": 1, + "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/community-frontier1042-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "6f4dc6fe7631d8aacf8081fcaecf32197181685b", + "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754" + }, + { + "path": "research/joint-query/certificate.json.gz", + "usage": "input", + "git_blob": "c6e876d8b48d768214deee265ade428f8983b566", + "sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" + }, + { + "path": "research/qq16-native-rounded-components/vendor/native.py", + "usage": "input", + "git_blob": "e1976b3a55a40206808405b99a4c443093378bef", + "sha256": "999eb1230798b25821de7771ecfa86381e137124059b30ccef167169d176ee8e" + }, + { + "path": "research/qq16-native-rounded-components/verify.py", + "usage": "input", + "git_blob": "56aedd008f0bda61f18e9475e3c0c65bc5749e3f", + "sha256": "16a6cf984f37adb2d98f5180312dc8637c3f653dd41db9252961c3ca1f3ffdba" + } + ], + "predecessors": [ + { + "name": "Ross Richardson", + "pr": 3067, + "head": "e1e28b4070ae52efa5a9d0aa826bc588be7206f2" + }, + { + "name": "Sricharan Vagvala", + "head": "946a399d6ae1667236bb395d21c33c749e000877", + "package": "research/qq16-native-rounded-components" + }, + { + "name": "Tekalign", + "pr": 3017, + "head": "0f493f4c264fbc70ee14364b68af260d858c143c" + }, + { + "name": "Arham Tahir", + "pr": 3036, + "head": "3717c1e684553c57bc73300410df65438a9ef095" + }, + { + "name": "Nick Petalas", + "pr": 2965, + "head": "526f2c242202b31b15e09a7502dfb8ff757b2bad" + } + ] +} diff --git a/research/qq16-native-grid-envelope/TASK.json b/research/qq16-native-grid-envelope/TASK.json new file mode 100644 index 0000000000..fa01904275 --- /dev/null +++ b/research/qq16-native-grid-envelope/TASK.json @@ -0,0 +1,99 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 6, + "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "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", + "actual_scope": "A sufficient all-input fixed-grid and range contract for the complete one-layer literal F0 native reference, including bounded arbitrary dirty helpers, butterfly interiors and integer-product temporaries; direct payload arithmetic/storage bill.", + "scope_change_reason": "The scalar and native dirty-helper failure witnesses already exist. This closes a different numerical producer obligation by an explicit bounded-input exact-arithmetic realization, rather than another decoder constant or projected child-error census.", + "bottleneck_link": "PR2965 requires a completed F0 output tolerance. This finite reference makes its arithmetic defect zero on the stated bounded lattice; recursive tariff, B1 and paid F17 consumption remain unproved.", + "budget_minutes": 60, + "stop_rule": "Stop after the sufficient finite contract, independent recurrence, literal dirty-witness control and direct payload bill. Do not infer affordability or start recursive implementation while complete physical/consumer costs are unspecified.", + "outcome": "completed", + "evidence": "RESULT.json: 26099 events, 133628 bound observations, G=35, magnitude multiplier 42822849617116776290 < 2^66, signed W=P+102; independent integer recurrence agrees at every observation; CONTROLS.json records rational/native arithmetic controls and a complete fixed-grid escape from the binary64 dirty-helper failure.", + "author": "commdata2338", + "ai_assistance": "Substantial OpenAI Codex (GPT-6 Astra) assistance in derivation, implementation, checking and writing. No independent human or formal-kernel review is claimed.", + "open_questions": [ + { + "question": "Can this sufficient finite F0 contract be supplied by a recursively admitted child/caller at an affordable complete cost?", + "why_it_matters": "Zero arithmetic defect for a direct 512-coordinate reference does not assign it the source recursive tariff or pay for the consumer.", + "first_step": "Pin one caller input/dirty bound and grid, identify the actual native child layout, and compare its full bit-operation, routing, storage and F17 consumption bill with the allowance before optimizing this envelope.", + "blocked_by": "No complete numerical/physical caller and consumer invoice is supplied; B1 and arbitrary-depth realization remain outside this result." + } + ], + "scope_key": "f0-native-all-input-grid-range-direct-bill", + "assignment": { + "track": "recursive-interfaces", + "task_id": "joint-query-controller", + "catalogue_scope_key": "42581d429acc9509d503", + "specific_card_lookup_seed": "00000000000000000000000000000000", + "selection": "Handoff-first refinement of the finite-producer obligation in Discussion #2727 after PR3067; source successors checked before selection." + }, + "declared_milestone": "scoped-proof", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2727#discussioncomment-19001870", + "cost_scope": "Constructive upper bounds for fixed-width payload arithmetic and logical payload storage. Physical addressing/routing, code/control storage, full-cover ownership, recursive child tariffs, B1 and F17 consumer remain unknown; no new kappa or supplier admission.", + "family_expansion_decision": "narrow-and-stop", + "existing_checks": "Catalogue existing_checks is empty (unknown). PR3036/3067/native-rounded-components cover the specific dirty-helper rounding witness; PR3189 audits noise-lattice closure in a scalar projection. This package adds the uniform bounded-input native exactness contract, with no independent reproof of their endpoint semantics.", + "refresh_checkpoint": { + "utc": "2026-10-17T17:43:26Z", + "main": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "priority_revision": 6, + "changes": "No changes to canonical main, guidance, selected record or scientific inputs; frozen pins retained." + }, + "parallel_scope_boundary": "Discussion #2727 comments 19001776 and 19001931 respectively study one B1 native error direction and a two-stage completed-operation error envelope; this result assumes exact finite primitives and proves an F0 lattice/range realization." +} diff --git a/research/qq16-native-grid-envelope/VERIFY.json b/research/qq16-native-grid-envelope/VERIFY.json new file mode 100644 index 0000000000..552645a111 --- /dev/null +++ b/research/qq16-native-grid-envelope/VERIFY.json @@ -0,0 +1,44 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1042-audit/selected-replay.tar.gz", + "research/joint-query/certificate.json.gz", + "research/qq16-native-rounded-components/vendor/native.py", + "research/qq16-native-rounded-components/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Full native F0 all-input primitive grid/range bound and direct payload invoice" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 30, + "checks": "Integer-only independent recurrence; all 133628 observation hashes and static operation counts" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/controls.py" + ], + "timeout_seconds": 180, + "checks": "Rational containment, Gaussian temporary/grid controls, and full literal fixed-grid escape from the binary64 dirty-helper witness" + } + ] +} diff --git a/research/qq16-native-grid-envelope/controls.py b/research/qq16-native-grid-envelope/controls.py new file mode 100644 index 0000000000..c12aca7a42 --- /dev/null +++ b/research/qq16-native-grid-envelope/controls.py @@ -0,0 +1,230 @@ +#!/usr/bin/env python3 +"""Arithmetic controls and literal fixed-grid escape from the known F0 loss. + +The literal event dispatcher and monomial evaluator are credited reuse of +Sricharan Vagvala / Tekalign, not independent native semantics. Apache-2.0. +""" +import argparse +from copy import deepcopy +from fractions import Fraction +import itertools +import json +from pathlib import Path +import sys +import types + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def module(name, path): + obj = types.ModuleType(name) + obj.__file__ = str(path) + sys.modules[name] = obj + exec(compile(path.read_bytes(), str(path), "exec"), obj.__dict__) + return obj + + +V = module("grid_envelope_primary", HERE / "verify.py") + + +def reject(callback, message): + try: + callback() + except ValueError: + return + raise ValueError("Control did not reject: " + message) + + +def contains(bound, x): + grid = Fraction(2**bound.grid) if bound.grid >= 0 else Fraction(1, 2**(-bound.grid)) + return abs(x) <= bound.magnitude and (x * grid).denominator == 1 + + +class Fixed: + """Actual integer execution on the single global grid 2^-G. + + Every displayed primitive checks signed range. Every right shift checks + divisibility. No rounding is permitted and no floating point is used. + """ + zero = ((0,) * 512, (0,) * 512) + + def __init__(self, native, g, width): + self.native = native + self.g = g + self.width = width + self.event = -1 + self.max_encoded_bits = 0 + self.max_site = None + self.nonzero_exact_divisions = 0 + self.changed_cuts = 0 + + def checked(self, values, stage): + limit = 1 << (self.width-1) + for x in values: + V.need(-limit <= x < limit, "Overflow: " + stage) + bits = abs(x).bit_length() + if bits > self.max_encoded_bits: + self.max_encoded_bits = bits + self.max_site = [self.event, stage] + return tuple(values) + + def divide(self, values, denominator, stage): + V.need(denominator > 0, "Positive exact divisor") + V.need(all(x % denominator == 0 for x in values), "Off-grid: " + stage) + self.nonzero_exact_divisions += sum(x != 0 for x in values) if denominator > 1 else 0 + return self.checked([x // denominator for x in values], stage) + + def constant(self, value): + n = Fraction(value) * (1 << self.g) + V.need(n.denominator == 1, "Entry lattice") + return self.checked([n.numerator]*512, "entry"), self.zero[1] + + def canonical(self, value): + return self.native.vector(value[0], value[1], self.g) + + def mono(self, value, key, adjoint=False): + out = self.native.mono((value[0], value[1], 0), key, adjoint) + return (self.checked(out[0], "monomial"), self.checked(out[1], "monomial")) + + def scalar(self, value, n, d, stage): + c = Fraction(n, d) + result = [] + for row in value: + numerator = self.checked([c.numerator*x for x in row], "constant-numerator") + result.append(self.divide(numerator, c.denominator, stage)) + return tuple(result) + + def add(self, left, right): + return tuple(self.checked([x+y for x, y in zip(a, b)], "scalar-add") + for a, b in zip(left, right)) + + def line(self, value, axis): + real, imag = value + out_r, out_i = [0]*512, [0]*512 + for x in range(512): + y = x ^ axis + if x > y: + continue + a, b, c, d = real[x], imag[x], real[y], imag[y] + rp, ip, rd, di = self.checked([a+c, b+d, a-c, b-d], "native-pair") + cross = self.checked([rp-di, ip+rd, rp+di, ip-rd], "native-cross") + out_r[x], out_i[x], out_r[y], out_i[y] = self.divide(cross, 2, "native-halved") + return tuple(out_r), tuple(out_i) + + def recipe(self, value, recipe, axes=9): + if recipe["rank"]: + value = self.mono(value, self.native.monomial_key(recipe["right"], axes)) + for j in range(recipe["rank"]): + value = self.line(value, 1 << j) + return self.mono(value, self.native.monomial_key(recipe["left"], axes)) + + def report(self): + return [] + + +def audit(): + data = V.load() # authenticate the reused implementation before importing it + old = module("credited_rounded_reference", ROOT / "research/qq16-native-rounded-components/verify.py") + checks = {} + # Each stored upper bound is checked against actual independent rational values. + scalar_cases = 0 + for g, j in itertools.product(range(4), repeat=2): + left, right = V.Bound(Fraction(3), g), V.Bound(Fraction(5), j) + result = left.plus(right) + for a, b in itertools.product(range(-3, 4), range(-5, 6)): + V.need(contains(result, Fraction(a, 2**g) + Fraction(b, 2**j)), "Sum envelope") + scalar_cases += 1 + coefficients = {Fraction(*e[1][-2:]) for e in data[0] + if e[0] == "scalar" and e[1][0] != "clear"} + for c in coefficients: + for x in range(-7, 8): + V.need(contains(V.Bound(Fraction(7), 3).scale(c), c*Fraction(x, 8)), "Scale envelope") + scalar_cases += 1 + checks["rational_scalar_containment_cases"] = scalar_cases + product_cases = 0 + for c in coefficients: + n = c.numerator + for x in list(range(-7, 8)) + [2**65-1, 1-2**65]: + terms = [x << j for j in range(abs(n).bit_length()) if (abs(n) >> j) & 1] + total = terms[0] + V.need(abs(total) <= abs(n*x), "First shifted product term") + for term in terms[1:]: + total += term + V.need(abs(total) <= abs(n*x), "Constant-product intermediate") + if n < 0: + total = -total + V.need(total == n*x, "Literal binary constant-product lowering") + product_cases += 1 + checks["literal_constant_product_cases"] = product_cases + native_cases = 0 + for a, b, c, d in itertools.product(range(-2, 3), repeat=4): + pairs = [a+c, b+d, a-c, b-d] + cross = [pairs[0]-pairs[3], pairs[1]+pairs[2], + pairs[0]+pairs[3], pairs[1]-pairs[2]] + outputs = [Fraction(x, 2) for x in cross] + env = V.Envelope() + final = env.line(V.Bound(Fraction(2))) + V.need(all(abs(x) <= 4 for x in pairs) and all(abs(x) <= 8 for x in cross), "Native temporaries") + V.need(all(contains(final, x) for x in outputs), "Native output envelope") + native_cases += 1 + checks["exhaustive_gaussian_pair_cases"] = native_cases + # One basis component genuinely needs a half quantum. + basis = ((1,) + (0,)*511, (0,)*512) + reject(lambda: Fixed(old.N, 0, 32).line(basis, 1), "Native half-grid") + # All four outputs fit signed 3-bit integers, but an internal numerator is 4. + cross_fixture = ((1, 1)+(0,)*510, (-1, 1)+(0,)*510) + reject(lambda: Fixed(old.N, 0, 3).line(cross_fixture, 1), "Cross numerator overflow") + checks["grid_and_internal_overflow_controls"] = 2 + reject(lambda: V.UNIT.scale(Fraction(1, 3)), "Nondyadic coefficient") + reject(lambda: V.check_monomial({"matrix_rows": [1]*9, "quadratic_rows": [0]*9, + "linear_Z4": [0]*9, "offset": 0, "phase": 0}), "Singular monomial") + bad = deepcopy(data) + event = next(e for e in bad[0] if e[0] == "scalar") + event[1] = ["clear", ["L", 0]] + reject(lambda: V.audit(bad), "Borrowed CLEAR") + checks["invalid_contract_controls"] = 3 + env = V.Envelope() + env.line(V.UNIT) + env.observe(V.ZERO, "later-clear") + V.need(env.max_grid == 1 and env.max_range == 4, "Earlier obligations survive CLEAR") + checks["later_clear_keeps_earlier_obligation"] = True + # P=66 is required by the inclusive dirty value 2^65 < 2^66. + literal_data = (data[0], data[1], None, data[2], data[3]) + fixed = Fixed(old.N, 35, 168) + trace = [] + out, faults, _ = old.run(literal_data, engine=fixed, trace=trace) + V.need(out == old.expected(dirty=True, rounded=False), "Fixed-grid exact F0 endpoint") + V.need(not faults and len(trace) == 26089, "Full literal fixed-grid coverage") + binary, _, _ = old.run(literal_data, engine=old.Binary64()) + V.need(binary == old.expected(dirty=True, rounded=True), "Known binary64 loss control") + V.need(binary != out, "Fixed grid must escape the actual rounding failure") + checks["literal_fixed_grid"] = { + "P": 66, "G": 35, "W": 168, + "events": len(data[0]), "changed_field_cuts": len(trace), + "endpoint_sha256": V.digest(out), "trace_sha256": V.digest(trace), + "max_encoded_magnitude_bits": fixed.max_encoded_bits, + "first_max_site": fixed.max_site, + "nonzero_exact_divisions": fixed.nonzero_exact_divisions, + "all_480_chosen_helpers_restore": True, "all_private_outputs_zero": True, + "binary64_control_differs_in_data_fields": [112, 114, 137, 190, 211], + } + return {"status": "PASS_QQ16_NATIVE_GRID_CONTROLS", "checks": checks} + + +def main(): + p = argparse.ArgumentParser(description=__doc__) + p.add_argument("--write", type=Path) + args = p.parse_args() + result = audit() + if args.write: + with args.write.open("x") as f: + json.dump(result, f, indent=2, sort_keys=True) + f.write("\n") + else: + V.need(result == json.loads((HERE / "CONTROLS.json").read_text()), "Control receipt mismatch") + print(result["status"], "literal_events=26099 fixed_grid_exact binary64_control_loses_data") + + +if __name__ == "__main__": + main() diff --git a/research/qq16-native-grid-envelope/independent.py b/research/qq16-native-grid-envelope/independent.py new file mode 100644 index 0000000000..f9d51f73e5 --- /dev/null +++ b/research/qq16-native-grid-envelope/independent.py @@ -0,0 +1,228 @@ +#!/usr/bin/env python3 +"""Integer-only second derivation of every grid/range observation. + +Imports no primary or predecessor implementation. Apache-2.0. +Prepared for commdata2338 with substantial OpenAI Codex assistance. +""" +from collections import Counter +import gzip +import hashlib +import json +from math import gcd +from pathlib import Path +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def require(ok, text): + if not ok: + raise ValueError(text) + + +def encode(obj): + return json.dumps(obj, sort_keys=True, separators=(",", ":")).encode() + + +def sha(obj): + return hashlib.sha256(encode(obj)).hexdigest() + + +def normalize_coefficient(n, d): + require(n != 0 and d != 0, "Nonzero coefficient") + n, d = abs(n), abs(d) + common = gcd(n, d) + n, d = n // common, d // common + require(d & (d-1) == 0, "Power-of-two denominator") + return n, d + + +def scale(pair, n, d=1): + if not pair[0]: + return (0, 0) + n, d = normalize_coefficient(n, d) + shift = d.bit_length()-1 + while n % 2 == 0: + n //= 2 + shift -= 1 + return pair[0] * n, pair[1] + shift + + +def add(left, right): + if not left[0]: + return right + if not right[0]: + return left + g = max(left[1], right[1]) + return ((left[0] << (g-left[1])) + (right[0] << (g-right[1])), g) + + +def text_pair(pair): + n, g = pair + if g < 0: + n <<= -g + g = 0 + while g and n % 2 == 0: + n //= 2 + g -= 1 + return str(n) if g == 0 else str(n) + "/" + str(1 << g) + + +def greater(left, right): + g = max(left[1], right[1]) + return (left[0] << (g-left[1])) > (right[0] << (g-right[1])) + + +def register(token): + return token[1] + (704 if token[0] == "C" else 0) + + +class IntegerLedger: + def __init__(self): + self.trace = hashlib.sha256() + self.max_range = (1, 0) + self.max_grid = 0 + self.range_site = self.grid_site = [-1, "entry"] + self.count = 0 + self.event = -1 + self.lines = self.monomials = self.recipes = 0 + + def mark(self, pair, stage): + self.count += 1 + if pair[0] and pair[1] > self.max_grid: + self.max_grid = pair[1] + self.grid_site = [self.event, stage] + if greater(pair, self.max_range): + self.max_range = pair + self.range_site = [self.event, stage] + self.trace.update(encode([self.event, stage, [text_pair(pair), pair[1]]]) + b"\n") + return pair + + def coefficient(self, pair, n, d): + n, d = normalize_coefficient(n, d) + self.mark((pair[0]*n, pair[1]) if pair[0] else (0, 0), "constant-partials") + product = self.mark(scale(pair, n), "constant-numerator") + return self.mark(scale(product, 1, d), "constant-result") + + def monomial(self, pair): + self.monomials += 1 + return self.mark(pair, "monomial") + + def recipe(self, pair, recipe): + self.recipes += 1 + rank = recipe["rank"] + if rank: + pair = self.monomial(pair) + for _ in range(rank): + pair_sum = self.mark(add(pair, pair), "native-pair") + cross = self.mark(add(pair_sum, pair_sum), "native-cross") + pair = self.mark(scale(cross, 1, 2), "native-halved") + self.lines += 1 + return self.monomial(pair) + + +def audit(): + sources = json.loads((HERE / "SOURCES.json").read_text()) + for p in sources["files"]: + if p["usage"] == "input": + require(hashlib.sha256((ROOT / p["path"]).read_bytes()).hexdigest() == p["sha256"], + "Independent input hash") + packet = json.loads(gzip.decompress((ROOT / "research/joint-query/certificate.json.gz").read_bytes())) + with tarfile.open(ROOT / "research/community-frontier1042-audit/selected-replay.tar.gz") as tf: + recipes = json.load(tf.extractfile("slots/local/CLIFFORD-RECIPES.json")) + children = {(r["old"], r["new"]): r for r in recipes["children"]} + events = packet["core_words"]["forward"][:] + for entry in packet["programs"]["F_0"][1:]: + events += entry[2] + field = [(1, 0)] * 704 + [(0, 0)] * 8 + ledger = IntegerLedger() + cut_digest = hashlib.sha256() + coefficients = [] + adds = clears = labels = 0 + for i, op in enumerate(events): + ledger.event = i + if op[0] == "phase": + continue + if op[0] == "scalar": + gate = op[1] + dest = register(gate[1]) + if gate[0] == "clear": + field[dest] = (0, 0) + clears += 1 + else: + n, d = gate[-2:] + coefficients.append((n, d)) + if gate[0] == "scale": + field[dest] = ledger.coefficient(field[dest], n, d) + else: + source = register(gate[2]) + term = ledger.coefficient(field[source], n, d) + field[dest] = ledger.mark(add(field[dest], term), "scalar-add") + adds += 1 + elif op[0] == "climb": + dest = op[2] + field[dest] = ledger.recipe(field[dest], children[op[3], op[4]]) + elif op[0] == "native_line": + dest = register(op[1]) + field[dest] = ledger.recipe(field[dest], packet["native_line_recipes"][op[2]]["recipe"]) + elif op[0] == "residual_adapter": + dest = op[2] + field[dest] = ledger.monomial(field[dest]) + elif op[0] == "adapter": + dest = op[2] + if (op[1] == "old_to_new" and dest < 112) or ( + op[1] == "new_to_old" and 112 <= dest < 224): + field[dest] = ledger.monomial(field[dest]) + else: + labels += 1 + else: + raise ValueError("Unexpected F0 operation") + ledger.mark(field[dest], "completed-event") + cut_digest.update(encode([i, dest, [text_pair(field[dest]), field[dest][1]]]) + b"\n") + cost = Counter() + for n0, d0 in coefficients: + n, d = normalize_coefficient(n0, d0) + cost["constant_product_calls"] += 1024 + cost["constant_product_component_copies"] += 1024 * n.bit_count() + cost["constant_product_additions"] += 1024 * (n.bit_count()-1) + cost["constant_product_left_shifts"] += 1024 * (n.bit_count()-(n & 1)) + cost["constant_product_negations"] += 1024 * ((n0 < 0) != (d0 < 0)) + cost["constant_product_right_shifts"] += 1024 * (d > 1) + cost.update({ + "scalar_real_additions": 1024*adds, + "clear_component_writes": 1024*clears, + "native_gaussian_lines": ledger.lines, + "native_real_additions": 2048*ledger.lines, + "native_exact_halvings": 1024*ledger.lines, + "native_pair_component_copies": 2048*ledger.lines, + "native_recipe_calls": ledger.recipes, + "monomial_calls": ledger.monomials, + "monomial_component_copies": 2048*ledger.monomials, + "monomial_component_negations_upper_bound": 1024*ledger.monomials, + "adapter_identity_labels": labels, + "phase_labels": sum(e[0] == "phase" for e in events), + "final_owned_scratch_clear_writes": 1036, + }) + result = json.loads((HERE / "RESULT.json").read_text()) + expected = { + "events": len(events), "event_sha256": sha(events), + "grid_guard": ledger.max_grid, "grid_site": ledger.grid_site, + "max_range_exact": text_pair(ledger.max_range), "range_site": ledger.range_site, + "primitive_bound_observations": ledger.count, + "primitive_bound_sha256": ledger.trace.hexdigest(), + "completed_bound_sha256": cut_digest.hexdigest(), + "final_bounds_sha256": sha([[text_pair(p), p[1]] for p in field]), + "direct_cost": dict(cost), + } + n, g = ledger.max_range + expected["range_power_of_two"] = n.bit_length() - (n & (n-1) == 0) - g + expected["signed_width_P_plus"] = expected["range_power_of_two"] + ledger.max_grid + 1 + for key, value in expected.items(): + require(result[key] == value, "Independent disagreement: " + key) + print("PASS_QQ16_NATIVE_GRID_INTEGER_RECURRENCE observations=" + str(ledger.count)) + return expected + + +if __name__ == "__main__": + audit() diff --git a/research/qq16-native-grid-envelope/verify.py b/research/qq16-native-grid-envelope/verify.py new file mode 100644 index 0000000000..ce942b23bc --- /dev/null +++ b/research/qq16-native-grid-envelope/verify.py @@ -0,0 +1,344 @@ +#!/usr/bin/env python3 +"""Conservative finite F0 native grid/range certificate. Apache-2.0. + +Prepared for commdata2338 with substantial OpenAI Codex assistance. +Native semantics and the pair-first lowering are credited in README.md. +This interpreter propagates bounds, not sampled payload values. +""" +import argparse +from collections import Counter +from dataclasses import dataclass +from fractions import Fraction +import gzip +import hashlib +import json +from pathlib import Path +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +DIM = 512 +FIELDS = 712 +MEMBERS = { + "slots/local/CLIFFORD-RECIPES.json": + "d0768f2164d5f64a2fdbec422f1cfde4e400818792f1904ca541958377243731", + "slots/local/RESIDUAL-ADAPTERS.json": + "383f40aadd00a4ac700dfd0d4c22d6c6c0be9a9863116e4d69c7acd23bafae0c", +} + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(obj): + return json.dumps(obj, sort_keys=True, separators=(",", ":")).encode() + + +def digest(obj): + return hashlib.sha256(canonical(obj)).hexdigest() + + +def load(): + pins = json.loads((HERE / "SOURCES.json").read_text()) + for pin in pins["files"]: + if pin["usage"] == "input": + raw = (ROOT / pin["path"]).read_bytes() + need(hashlib.sha256(raw).hexdigest() == pin["sha256"], + "Source hash: " + pin["path"]) + packet = json.loads(gzip.decompress( + (ROOT / "research/joint-query/certificate.json.gz").read_bytes())) + program = packet["programs"]["F_0"] + need(program[0][:3] == ["retained_core", "forward", 0], "F0 retained core") + events = list(packet["core_words"]["forward"]) + for wrapper in program[1:]: + need(wrapper[0] in ("private_sweep", "cover_sweep"), "F0 wrapper") + events.extend(wrapper[2]) + objects = [] + with tarfile.open(ROOT / "research/community-frontier1042-audit/selected-replay.tar.gz") as tf: + for name, sha in MEMBERS.items(): + found = [x for x in tf.getmembers() if x.name == name] + need(len(found) == 1 and found[0].isfile(), "Unique source member") + need(found[0].size < 12_000_000, "Bounded source member") + raw = tf.extractfile(found[0]).read() + need(hashlib.sha256(raw).hexdigest() == sha, "Member hash: " + name) + objects.append(json.loads(raw)) + return events, packet, *objects + + +def reg(token): + need(isinstance(token, list) and len(token) == 2, "Register token") + kind, index = token + need(kind in ("L", "C") and type(index) is int, "Register type") + need(0 <= index < (704 if kind == "L" else 8), "Register index") + return index + (704 if kind == "C" else 0) + + +def valuation(n): + need(type(n) is int and n != 0, "Nonzero integer valuation") + n = abs(n) + return (n & -n).bit_length() - 1 + + +def dyadic(coefficient): + c = Fraction(coefficient) + need(c.denominator & (c.denominator - 1) == 0, "Dyadic coefficient") + return c + + +@dataclass(frozen=True) +class Bound: + """|component| <= magnitude M h; component in h 2^-grid Z. + + A zero bound has grid zero by convention. Grid exponents may be negative. + """ + magnitude: Fraction + grid: int = 0 + + def __post_init__(self): + need(isinstance(self.magnitude, Fraction) and self.magnitude >= 0, + "Nonnegative rational magnitude") + need(type(self.grid) is int, "Integer grid exponent") + need(self.magnitude != 0 or self.grid == 0, "Canonical zero") + + def scale(self, c): + c = dyadic(c) + if not c or not self.magnitude: + return ZERO + return Bound(self.magnitude * abs(c), + self.grid + c.denominator.bit_length() - 1 + - valuation(c.numerator)) + + def plus(self, other): + if not self.magnitude: + return other + if not other.magnitude: + return self + return Bound(self.magnitude + other.magnitude, max(self.grid, other.grid)) + + def record(self): + return [str(self.magnitude), self.grid] + + +ZERO = Bound(Fraction(0)) +UNIT = Bound(Fraction(1)) + + +def ceil_log2(value): + need(value > 0, "Positive logarithm input") + n, d = value.numerator, value.denominator + k = n.bit_length() - d.bit_length() + power = Fraction(1 << k) if k >= 0 else Fraction(1, 1 << -k) + return k if value <= power else k + 1 + + +def binary_rank(rows): + basis = {} + for row in rows: + while row: + k = row.bit_length() - 1 + if k not in basis: + basis[k] = row + break + row ^= basis[k] + return len(basis) + + +def check_monomial(m): + """Signed component permutation, including all 9 active coordinates.""" + need(set(m) == {"matrix_rows", "quadratic_rows", "linear_Z4", "offset", "phase"}, + "Monomial fields") + a, q, z = (m[k] for k in ("matrix_rows", "quadratic_rows", "linear_Z4")) + need(len(a) == len(q) == len(z) == 9, "Nine-axis monomial") + need(all(type(x) is int and 0 <= x < DIM for x in a + q), "Binary rows") + need(all(type(x) is int and 0 <= x < 4 for x in z), "Quarter turns") + need(type(m["offset"]) is int and 0 <= m["offset"] < DIM, "Offset") + need(type(m["phase"]) is int and 0 <= m["phase"] < 4, "Global phase") + need(binary_rank(a) == 9, "Invertible monomial") + + +class Envelope: + def __init__(self): + self.max_grid = 0 + self.max_range = Fraction(1) + self.grid_site = [-1, "entry"] + self.range_site = [-1, "entry"] + self.observations = 0 + self.event = -1 + self.cost = Counter() + self.trace = hashlib.sha256() + self.validated_monomials = set() + + def observe(self, value, stage): + self.observations += 1 + if value.magnitude and value.grid > self.max_grid: + self.max_grid = value.grid + self.grid_site = [self.event, stage] + if value.magnitude > self.max_range: + self.max_range = value.magnitude + self.range_site = [self.event, stage] + self.trace.update(canonical([self.event, stage, value.record()]) + b"\n") + return value + + def multiply(self, value, c): + """Integer constant product first, exact binary division second. + + Shift/add partial products have no larger magnitude than |numerator| + times the input; their grids are no finer than the input. + """ + c = dyadic(c) + need(c != 0, "Nonzero source coefficient") + n, d = c.numerator, c.denominator + self.cost["constant_product_calls"] += 2 * DIM + self.cost["constant_product_component_copies"] += abs(n).bit_count() * 2 * DIM + self.cost["constant_product_additions"] += (abs(n).bit_count()-1) * 2 * DIM + self.cost["constant_product_left_shifts"] += ( + abs(n).bit_count() - (abs(n) & 1)) * 2 * DIM + self.cost["constant_product_negations"] += (n < 0) * 2 * DIM + self.cost["constant_product_right_shifts"] += (d > 1) * 2 * DIM + partial = Bound(value.magnitude * abs(n), value.grid) if value.magnitude else ZERO + self.observe(partial, "constant-partials") + product = self.observe(value.scale(n), "constant-numerator") + return self.observe(product.scale(Fraction(1, d)), "constant-result") + + def line(self, value): + self.cost["native_gaussian_lines"] += 1 + self.cost["native_real_additions"] += 8 * (DIM // 2) + self.cost["native_exact_halvings"] += 4 * (DIM // 2) + self.cost["native_pair_component_copies"] += 8 * (DIM // 2) + pair = self.observe(value.plus(value), "native-pair") + cross = self.observe(pair.plus(pair), "native-cross") + return self.observe(cross.scale(Fraction(1, 2)), "native-halved") + + def mono(self, value, m): + key = digest(m) + if key not in self.validated_monomials: + check_monomial(m) + self.validated_monomials.add(key) + self.cost["monomial_calls"] += 1 + # Write the signed permutation to one buffer and copy it back. + self.cost["monomial_component_copies"] += 4 * DIM + self.cost["monomial_component_negations_upper_bound"] += 2 * DIM + return self.observe(value, "monomial") + + def recipe(self, value, r): + rank = r["rank"] + need(type(rank) is int and 0 <= rank <= 9, "Native rank") + self.cost["native_recipe_calls"] += 1 + if rank: + value = self.mono(value, r["right"]) + for _ in range(rank): + value = self.line(value) + else: + need(r["right"] is None, "Rank-zero right monomial") + return self.mono(value, r["left"]) + + +def audit(data=None): + events, packet, recipes, residuals = data or load() + need(Counter(e[0] for e in events) == { + "scalar": 21025, "climb": 3486, "adapter": 1090, + "residual_adapter": 480, "phase": 10, "native_line": 8}, "F0 event inventory") + children = {(r["old"], r["new"]): r for r in recipes["children"]} + adapters = {(r["role"], r["port"]): r for r in recipes["endpoint_adapters"]} + need(len(children) == len(recipes["children"]), "Unique child recipes") + need(len(adapters) == len(recipes["endpoint_adapters"]), "Unique adapters") + e = Envelope() + state = [UNIT] * 704 + [ZERO] * 8 + cut_hash = hashlib.sha256() + for index, event in enumerate(events): + e.event = index + kind = event[0] + if kind == "scalar": + gate = event[1] + dst = reg(gate[1]) + if gate[0] == "clear": + need(dst >= 704, "Private CLEAR only") + state[dst] = ZERO + e.cost["clear_component_writes"] += 2 * DIM + elif gate[0] == "scale": + state[dst] = e.multiply(state[dst], Fraction(gate[2], gate[3])) + else: + need(gate[0] == "add", "Scalar kind") + src = reg(gate[2]) + term = e.multiply(state[src], Fraction(gate[3], gate[4])) + state[dst] = e.observe(state[dst].plus(term), "scalar-add") + e.cost["scalar_real_additions"] += 2 * DIM + elif kind == "climb": + _, _, dst, old, new, _ = event + need(type(dst) is int and 0 <= dst < 704, "Climb field") + state[dst] = e.recipe(state[dst], children[old, new]) + elif kind == "adapter": + _, direction, dst, _ = event + need(direction in ("old_to_new", "new_to_old") and 0 <= dst < 704, + "Adapter direction/field") + if direction == "old_to_new" and dst < 112: + a = adapters["source", dst] + need(a["rank"] == 0 and a["right"] is None, "Monomial source adapter") + state[dst] = e.mono(state[dst], a["left"]) + elif direction == "new_to_old" and 112 <= dst < 224: + a = adapters["target", dst-112] + need(a["rank"] == 0 and a["right"] is None, "Monomial target adapter") + state[dst] = e.mono(state[dst], a["left"]) + else: + e.cost["adapter_identity_labels"] += 1 + elif kind == "residual_adapter": + direction, dst, a = event[1:4] + need(direction in ("pre", "post") and 224 <= dst < 704, + "Residual direction/field") + b = event[4] if len(event) == 5 else 1 + key = str(a) if b == 1 else f"{a}:{b}" + state[dst] = e.mono(state[dst], residuals["recipes"][key][ + "right" if direction == "pre" else "left"]) + elif kind == "native_line": + dst = reg(event[1]) + state[dst] = e.recipe(state[dst], packet["native_line_recipes"][event[2]]["recipe"]) + else: + need(kind == "phase", "Unknown event") + e.cost["phase_labels"] += 1 + continue + e.observe(state[dst], "completed-event") + cut_hash.update(canonical([index, dst, state[dst].record()]) + b"\n") + b = ceil_log2(e.max_range) + e.cost["final_owned_scratch_clear_writes"] = 2 * DIM + 12 + return { + "schema_version": 1, + "status": "PASS_QQ16_NATIVE_GRID_ENVELOPE", + "scope": "Finite literal F0 reference, all 704 bounded input fields, private fields zero", + "events": len(events), "event_sha256": digest(events), + "grid_guard": e.max_grid, "grid_site": e.grid_site, + "range_power_of_two": b, "range_site": e.range_site, + "max_range_exact": str(e.max_range), + "signed_width_P_plus": e.max_grid + b + 1, + "primitive_bound_observations": e.observations, + "primitive_bound_sha256": e.trace.hexdigest(), + "completed_bound_sha256": cut_hash.hexdigest(), + "final_bounds_sha256": digest([x.record() for x in state]), + "validated_distinct_monomials": len(e.validated_monomials), + "direct_cost": dict(sorted(e.cost.items())), + "logical_payload_words": 2 * DIM * FIELDS, + "additional_scratch_words_upper_bound": 2 * DIM + 12, + "supplier_admission": False, + } + + +def main(): + p = argparse.ArgumentParser(description=__doc__) + p.add_argument("--write", type=Path, help="Exclusively create a receipt") + args = p.parse_args() + result = audit() + if args.write: + with args.write.open("x") as f: + json.dump(result, f, indent=2, sort_keys=True) + f.write("\n") + else: + need(result == json.loads((HERE / "RESULT.json").read_text()), "Receipt mismatch") + print(result["status"], "events=" + str(result["events"]), + "grid_guard=" + str(result["grid_guard"]), + "range_bits=" + str(result["range_power_of_two"]), + "signed_width=P+" + str(result["signed_width_P_plus"])) + + +if __name__ == "__main__": + main()