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()