diff --git a/research/qq16-f0-physical-rounding/README.md b/research/qq16-f0-physical-rounding/README.md new file mode 100644 index 0000000000..07424e0114 --- /dev/null +++ b/research/qq16-f0-physical-rounding/README.md @@ -0,0 +1,178 @@ +# Deterministic rounding in the native QQ16 F0 producer + +The concrete scalar failure in Arham Tahir's [PR3036](https://github.com/CrocSwap/integer-mult-bounds/pull/3036), +head `3717c1e684553c57bc73300410df65438a9ef095`, survives the actual physical +native frame and residual adapters **in the specified mixed arithmetic model**. +This closes its physical binding gap for four finite precisions. It does not +implement rounded native-child interiors or admit a supplier. No new kappa is +claimed. + +At `p = 8, 24, 53, 113`, set physical `L112 = ONE`, +`L224 = 2^(p+12) ONE`, and all other fields zero. `ONE` is the real constant +512-component vector, uniform across cover owners. Execute the literal local +`F_0` program, including every native child and endpoint/residual conversion. +Each real and imaginary scalar ADD result is rounded to a binary significand +of precision p, nearest with ties to even and unbounded exponent. Completed +native recipes, their internal arithmetic, conversions, SCALEs and owned +CLEARs are exact. Every scalar coefficient product in the four rounded +executions is separately checked to be exactly representable at p, so a +separate correctly rounded multiplication gives that same product here. + +Exactly two scalar instructions round; each gives error `-ONE/2`: + +| Zero-based event | Literal instruction | Exact real component | Rounded component | +| --- | --- | --- | --- | +| 3887 | `L112 += -L224/2` | `(1-2^(p+12))/2` | `-2^(p+11)` | +| 4060 | `L139 += -L224/2` | `(1-2^(p+12))/2` | `-2^(p+11)` | + +The exact execution returns the chosen input unchanged. The rounded physical +endpoint differs in exactly these five data fields: + +``` +L112: -ONE +L114,L137,L190,L211: -ONE/2 +``` + +All 480 physical helper values return exactly to their chosen entrance values; +all eight private fields return zero. This is exact amplitude equality on the +stated family, not a claim about arbitrary dirty inputs or IEEE signed-zero, +NaN or storage-bit representations. The largest error norm equals the original +data norm `H=sqrt(512)`, hence the relative error is exactly one. A separate +`-ONE/32` control has squared input and error norms `1/2`; dyadic scaling +therefore supplies a witness with `H<=1`. Unit irrational normalization is not +assumed to commute with binary rounding. + +## Why the physical binding is substantive + +[Tekalign's PR3017](https://github.com/CrocSwap/integer-mult-bounds/pull/3017), +head `0f493f4c264fbc70ee14364b68af260d858c143c`, binds an earlier **permitted** +fault at a different instruction and dirty register. It deliberately does not +claim a concrete rounding failure. PR3036 supplies actual scalar rounding but +omits the non-scalar events. Neither predecessor establishes this implication. +Their native conventions, scalar witness and general frame argument are +credited rather than claimed as new. + +The new verifier executes every event directly on exact Gaussian-dyadic +vectors. It does not replace native maps with frame labels or scalar +projection. Each of the four cases checks all 364,544 complex endpoint +amplitudes against the stated exact result. `RESULT.json` records the full +event digest, exact local rounding values, every nonzero output-error vector +histogram and canonical endpoint digests. `vendor/pr3017/native.py` retains +Tekalign's exact primitive evaluator byte-for-byte, with its source hash and +head in `SOURCES.json`; the new execution/rounding driver is separate. This is +executable reuse, not a second independent Clifford implementation. + +A separate internal rounded-networks specialist rederived the frame argument, +inspected the p=53 literal result, and checked the following finite native +facts with the retained evaluator. Its full source-bound report is local-only and preserved outside the checkout; +public evidence is the literal verifier, receipt, controls and argument below. +No human or formal-kernel review is claimed. + +1. L224 has ordinary endpoint frames `(0,1)` and no residual wrapper. Both + marked ADDs use frame zero, whose physical vector is exactly `ONE`. +2. Every real or imaginary component of the 1,004 canonical vectors + `v_f=T_f ONE` is in `{0,1,-1,2,-2}`. For unbounded-exponent nearest-even + rounding, sign symmetry and power-of-two homogeneity give + `RN_p(a v_f)=RN_p(a) v_f` for real a. This is a written homogeneity lemma + combined with a finite exact frame fact; frames need not be constant. +3. Exact scalar trajectories from unit L112, unit L224 and unit post-ADD + errors at each marked site are zero at all residual boundaries: 1,920 + values in total. Those residual monomials act on zero, so their two gauges + need not coincide. The exact used child and endpoint frame-vector checks + in the retained native binding also pass. +4. A unit post-3887 error reaches `+1` in L112,L114,L137,L139. A unit + post-4060 error reaches `+1` in L112,L190,L211 and `-1` in L139. Multiplying + both by `-1/2` gives the five final errors, with L139 cancelling. + +At each marked cut, the exact component is `-2^(p+11)+1/2`. It is strictly +closer to `-2^(p+11)` than to the next representable value toward zero, which +is `2^11` away. This decision is not a tie. The literal four-case inventory, +not this local calculation alone, establishes that no other ADD rounds. + +## Reproduce + +From the repository root, standard-library Python 3.12: + +```sh +python3.12 -Werror -I -B scripts/research_package.py \ + --package research/qq16-f0-physical-rounding +``` + +The main verifier is read-only and compares the complete canonical receipt; +`--write PATH` exclusively creates an absent receipt. Eight behavioral groups +check an independent nearest-number oracle (2,575 integer decisions), native +line/global-phase conventions, all canonical frames, clean helpers, wider +precision on the **same** dirty input, separate rounding-site effects, dyadic +sign/scale covariance, an occupied nonconstant exit-adapter mutation, and +source/JSON fail-closed behavior. The wider control uses 65 bits on the +original `2^65` dirty input; it is an escape witness, not a minimum precision +for arbitrary inputs. Assertions used for scientific acceptance remain active +under optimization. + +The immutable scientific inputs are the current joint-query certificate and +three authenticated members of the selected replay archive. They are never +modified. No selected cold replay is needed for this unchanged selected +construction; it is not claimed here. + +## Recursive-cost relevance and limits + +The larger mechanism is the zero-retention QQ16 interface: it changes query +retention and the paid producer/decoder structure. Nick Petalas's +[PR2965 output-error bridge](../qq16-producer-defect-transfer/README.md) assumes +completed producer tolerances. This witness prevents replacing its F0 premise +by the stated p-bit scalar arithmetic while leaving dirty magnitudes arbitrary, +even when completed native operations are exact and all helpers return. +It does not contradict that conditional theorem. + +Increasing p while also increasing the dirty value is four separate finite +fixtures. This package proves no all-p, all-tensor-depth, arbitrary-input, +uniform dirty-range or sufficient guard-bit theorem. The domain is one tensor +factor, nine active axes, 512 payload coordinates and the four named p values, +with the inherited local full-cover semantics and uniform owner inputs. + +Exact completed native operations are a material premise. Native internal +rounding, finite exponents/overflow, recursive-child accuracy, physical bit +widths, source access, hosting/movement, storage, all-size compilation, full +B1/decoder consumption and F17 endpoint use remain unresolved. No Boolean or +direct vector work is assigned the original recursive tariff. There is no +favorable complete recursive invoice and no scalar saving, new supplier, +selected-frontier change or new kappa. Family decision: narrow and stop at this +producer obligation; no further search or construction expansion is implied. + +## Open next questions + +Can a finite native F0 implementation exclude these deterministic losses at +its actual dirty range and paid precision? Pin the input grid and dirty bound, +then specify the native-internal rounding and prove exactness or error at +every occupied cut. Next charge that realization, storage, movement, cleanup +and the F17 consumer together. Exact-grid arithmetic is a legitimate escape; +its complete recursive price remains the blocker. `TASK.json` preserves the +structured handoff. + +## Sources, attribution and engineering scope + +Scientific base: `d8e0f83f00191df62174b641e9fff055c357f641`, priority revision 6. +The source manifest pins the selected record and task catalogue as provenance, +the two live inputs, and the exact retained evaluator source. The canonical +[claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/2727#discussioncomment-18983447) +records overlap and lifecycle. Metadata coverage is non-atomic and does not +prove novelty or cover unpublished work. + +New physical rounding driver, integration and checks by Ross Richardson with +substantial OpenAI Codex assistance, including a separate internal +rounded-networks mathematical reviewer. Credit Arham Tahir/PR3036 for the +concrete scalar witness and PR2995 for the earlier fault, Tekalign/PR3017 for +the exact vector evaluator and native binding, Nick Petalas/PR2965 for the +producer-accuracy handoff, Ali Romman/QQ16, Sagar Thakrar, DLamdata, ywz65, +starship-s, Douglas Colkitt and the retained supplier/native lineage. All new +work is Apache-2.0; the evaluator's original header is preserved. + +Verification uses managed Python integers/collections and bounded dynamic +allocation; it is not a fixed-tape machine realization. It traverses 26,099 +events, 712 fields and 512 coordinates per execution; integer rounding cache +is capped at 32,768 entries. Tests traverse 1,004 frames and small finite +number systems. Immutable archive containers and decompressed selected members +are hash authenticated; declared member payloads are capped at 12 MB. Python +library allocation overhead is not profiled. Warning-as-error compilation and +normal/optimized runtime checks are used; no static type or proof-assistant +claim is made. diff --git a/research/qq16-f0-physical-rounding/RESULT.json b/research/qq16-f0-physical-rounding/RESULT.json new file mode 100644 index 0000000000..76b1ca1884 --- /dev/null +++ b/research/qq16-f0-physical-rounding/RESULT.json @@ -0,0 +1,615 @@ +{ + "active_axes": 9, + "cases": [ + { + "all_480_helpers_exactly_restored": true, + "all_8_private_fields_zero": true, + "dirty_amplitude": "1048576", + "endpoint_errors": [ + [ + 112, + { + "imag": { + "0": 512 + }, + "real": { + "-1": 512 + } + } + ], + [ + 114, + { + "imag": { + "0": 512 + }, + "real": { + "-1/2": 512 + } + } + ], + [ + 137, + { + "imag": { + "0": 512 + }, + "real": { + "-1/2": 512 + } + } + ], + [ + 190, + { + "imag": { + "0": 512 + }, + "real": { + "-1/2": 512 + } + } + ], + [ + 211, + { + "imag": { + "0": 512 + }, + "real": { + "-1/2": 512 + } + } + ] + ], + "faults": [ + { + "error": { + "imag": { + "0": 512 + }, + "real": { + "-1/2": 512 + } + }, + "event": 3887, + "exact": { + "imag": { + "0": 512 + }, + "real": { + "-1048575/2": 512 + } + }, + "gate": [ + "add", + [ + "L", + 112 + ], + [ + "L", + 224 + ], + -1, + 2 + ], + "rounded": { + "imag": { + "0": 512 + }, + "real": { + "-524288": 512 + } + } + }, + { + "error": { + "imag": { + "0": 512 + }, + "real": { + "-1/2": 512 + } + }, + "event": 4060, + "exact": { + "imag": { + "0": 512 + }, + "real": { + "-1048575/2": 512 + } + }, + "gate": [ + "add", + [ + "L", + 139 + ], + [ + "L", + 224 + ], + -1, + 2 + ], + "rounded": { + "imag": { + "0": 512 + }, + "real": { + "-524288": 512 + } + } + } + ], + "ideal_endpoint_sha256": "84ba80492b0a33c5350f4099be171115478d1ff8f9081cc47fdece1d840f4cef", + "initial_data_squared_norm": "512", + "maximum_error_squared_norm": "512", + "precision": 8, + "relative_error": "1", + "rounded_endpoint_sha256": "2359f76dc002a456af1eb17bc8ab8636377476063078e076a02c8c0da9912276" + }, + { + "all_480_helpers_exactly_restored": true, + "all_8_private_fields_zero": true, + "dirty_amplitude": "68719476736", + "endpoint_errors": [ + [ + 112, + { + "imag": { + "0": 512 + }, + "real": { + "-1": 512 + } + } + ], + [ + 114, + { + "imag": { + "0": 512 + }, + "real": { + "-1/2": 512 + } + } + ], + [ + 137, + { + "imag": { + "0": 512 + }, + "real": { + "-1/2": 512 + } + } + ], + [ + 190, + { + "imag": { + "0": 512 + }, + "real": { + "-1/2": 512 + } + } + ], + [ + 211, + { + "imag": { + "0": 512 + }, + "real": { + "-1/2": 512 + } + } + ] + ], + "faults": [ + { + "error": { + "imag": { + "0": 512 + }, + "real": { + "-1/2": 512 + } + }, + "event": 3887, + "exact": { + "imag": { + "0": 512 + }, + "real": { + "-68719476735/2": 512 + } + }, + "gate": [ + "add", + [ + "L", + 112 + ], + [ + "L", + 224 + ], + -1, + 2 + ], + "rounded": { + "imag": { + "0": 512 + }, + "real": { + "-34359738368": 512 + } + } + }, + { + "error": { + "imag": { + "0": 512 + }, + "real": { + "-1/2": 512 + } + }, + "event": 4060, + "exact": { + "imag": { + "0": 512 + }, + "real": { + "-68719476735/2": 512 + } + }, + "gate": [ + "add", + [ + "L", + 139 + ], + [ + "L", + 224 + ], + -1, + 2 + ], + "rounded": { + "imag": { + "0": 512 + }, + "real": { + "-34359738368": 512 + } + } + } + ], + "ideal_endpoint_sha256": "b15ef91184d34de805a7c11335b829b21d1fc910a9556b9908cfc37d1bc1f611", + "initial_data_squared_norm": "512", + "maximum_error_squared_norm": "512", + "precision": 24, + "relative_error": "1", + "rounded_endpoint_sha256": "32eb38d61e32a9c41b53ce46a5e6d57a73d4488d92931ab72035e7a78384383a" + }, + { + "all_480_helpers_exactly_restored": true, + "all_8_private_fields_zero": true, + "dirty_amplitude": "36893488147419103232", + "endpoint_errors": [ + [ + 112, + { + "imag": { + "0": 512 + }, + "real": { + "-1": 512 + } + } + ], + [ + 114, + { + "imag": { + "0": 512 + }, + "real": { + "-1/2": 512 + } + } + ], + [ + 137, + { + "imag": { + "0": 512 + }, + "real": { + "-1/2": 512 + } + } + ], + [ + 190, + { + "imag": { + "0": 512 + }, + "real": { + "-1/2": 512 + } + } + ], + [ + 211, + { + "imag": { + "0": 512 + }, + "real": { + "-1/2": 512 + } + } + ] + ], + "faults": [ + { + "error": { + "imag": { + "0": 512 + }, + "real": { + "-1/2": 512 + } + }, + "event": 3887, + "exact": { + "imag": { + "0": 512 + }, + "real": { + "-36893488147419103231/2": 512 + } + }, + "gate": [ + "add", + [ + "L", + 112 + ], + [ + "L", + 224 + ], + -1, + 2 + ], + "rounded": { + "imag": { + "0": 512 + }, + "real": { + "-18446744073709551616": 512 + } + } + }, + { + "error": { + "imag": { + "0": 512 + }, + "real": { + "-1/2": 512 + } + }, + "event": 4060, + "exact": { + "imag": { + "0": 512 + }, + "real": { + "-36893488147419103231/2": 512 + } + }, + "gate": [ + "add", + [ + "L", + 139 + ], + [ + "L", + 224 + ], + -1, + 2 + ], + "rounded": { + "imag": { + "0": 512 + }, + "real": { + "-18446744073709551616": 512 + } + } + } + ], + "ideal_endpoint_sha256": "8c5dd8f939e94cee17e7f12dbba2b9c738ef14d7f35243d0f3923182651f14fc", + "initial_data_squared_norm": "512", + "maximum_error_squared_norm": "512", + "precision": 53, + "relative_error": "1", + "rounded_endpoint_sha256": "1443b3987b3a6a1703ecdfee09776fafc3aa2109f543336a25c94ec508d6bec6" + }, + { + "all_480_helpers_exactly_restored": true, + "all_8_private_fields_zero": true, + "dirty_amplitude": "42535295865117307932921825928971026432", + "endpoint_errors": [ + [ + 112, + { + "imag": { + "0": 512 + }, + "real": { + "-1": 512 + } + } + ], + [ + 114, + { + "imag": { + "0": 512 + }, + "real": { + "-1/2": 512 + } + } + ], + [ + 137, + { + "imag": { + "0": 512 + }, + "real": { + "-1/2": 512 + } + } + ], + [ + 190, + { + "imag": { + "0": 512 + }, + "real": { + "-1/2": 512 + } + } + ], + [ + 211, + { + "imag": { + "0": 512 + }, + "real": { + "-1/2": 512 + } + } + ] + ], + "faults": [ + { + "error": { + "imag": { + "0": 512 + }, + "real": { + "-1/2": 512 + } + }, + "event": 3887, + "exact": { + "imag": { + "0": 512 + }, + "real": { + "-42535295865117307932921825928971026431/2": 512 + } + }, + "gate": [ + "add", + [ + "L", + 112 + ], + [ + "L", + 224 + ], + -1, + 2 + ], + "rounded": { + "imag": { + "0": 512 + }, + "real": { + "-21267647932558653966460912964485513216": 512 + } + } + }, + { + "error": { + "imag": { + "0": 512 + }, + "real": { + "-1/2": 512 + } + }, + "event": 4060, + "exact": { + "imag": { + "0": 512 + }, + "real": { + "-42535295865117307932921825928971026431/2": 512 + } + }, + "gate": [ + "add", + [ + "L", + 139 + ], + [ + "L", + 224 + ], + -1, + 2 + ], + "rounded": { + "imag": { + "0": 512 + }, + "real": { + "-21267647932558653966460912964485513216": 512 + } + } + } + ], + "ideal_endpoint_sha256": "ce90d2d7797158029c33fffc1e57465786f17bf82477fef3139184d6669f74b8", + "initial_data_squared_norm": "512", + "maximum_error_squared_norm": "512", + "precision": 113, + "relative_error": "1", + "rounded_endpoint_sha256": "1ee914051b23eab036c32e65a2e301b6be011fab5ce203602050ea816f0f9ef3" + } + ], + "endpoint_amplitudes_per_case": 364544, + "event_sha256": "4c1ee518a6513c115741a3834c49490c6e8e68f5e2357af8dac782c3d40958e7", + "events": 26099, + "native_operator_internals_rounded": false, + "no_new_kappa": true, + "payload_coordinates": 512, + "schema_version": 1, + "scope": "finite native F0; component RN at scalar ADDs; exact native operators; unbounded exponents", + "selected_frontier_changed": false, + "status": "PASS_QQ16_F0_PHYSICAL_ROUNDING" +} diff --git a/research/qq16-f0-physical-rounding/SOURCES.json b/research/qq16-f0-physical-rounding/SOURCES.json new file mode 100644 index 0000000000..ba8f0232b4 --- /dev/null +++ b/research/qq16-f0-physical-rounding/SOURCES.json @@ -0,0 +1,49 @@ +{ + "schema_version": 1, + "base_commit": "d8e0f83f00191df62174b641e9fff055c357f641", + "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" + } + ], + "vendored_sources": [ + { + "local_path": "vendor/pr3017/native.py", + "repository": "CrocSwap/integer-mult-bounds", + "source_pr": 3017, + "source_head": "0f493f4c264fbc70ee14364b68af260d858c143c", + "source_path": "research/qq16-native-dirty-fault/native.py", + "git_blob": "e1976b3a55a40206808405b99a4c443093378bef", + "sha256": "999eb1230798b25821de7771ecfa86381e137124059b30ccef167169d176ee8e", + "credit": "Tekalign, substantial OpenAI Codex assistance", + "license": "Apache-2.0", + "usage": "exact native vector evaluator reused unchanged; authenticated by verifier before compilation" + } + ], + "predecessors": { + "3036": "3717c1e684553c57bc73300410df65438a9ef095", + "3017": "0f493f4c264fbc70ee14364b68af260d858c143c", + "2965": "526f2c242202b31b15e09a7502dfb8ff757b2bad" + } +} diff --git a/research/qq16-f0-physical-rounding/TASK.json b/research/qq16-f0-physical-rounding/TASK.json new file mode 100644 index 0000000000..e27aac38c0 --- /dev/null +++ b/research/qq16-f0-physical-rounding/TASK.json @@ -0,0 +1,79 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 6, + "base_commit": "d8e0f83f00191df62174b641e9fff055c357f641", + "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": "Deterministic physical component rounding of PR3036\u2019s finite F0 dirty-helper witness under exact completed native operators", + "scope_change_reason": "Take the released PR3036 physical-frame binding handoff within the producer-accuracy obligation; do not repeat the prior scalar or permissive-fault results.", + "bottleneck_link": "The zero-retention producer/decoder changes the recursive interface, but its completed producer accuracy remains a hypothesis. Test an actual arithmetic realization before assigning it the inherited tariff.", + "budget_minutes": 60, + "stop_rule": "Finish four finite-precision native witnesses and controls; stop at native-interior rounding and full paid caller obligations.", + "outcome": "negative-result", + "evidence": "RESULT.json and direct literal native verifier; separate internal mathematical review retained externally", + "author": "Ross Richardson with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance, including one independent internal math-rounded-networks specialist; no independent human or formal-kernel review.", + "open_questions": [ + { + "question": "Can a finite native F0 producer exclude this deterministic loss with its actual dirty-input grid/range and paid precision?", + "why_it_matters": "PR2965\u2019s completed output tolerance is not supplied by p-bit scalar arithmetic with unrestricted dirty magnitudes.", + "first_step": "Pin a finite dirty bound/grid and native-internal rounding, then establish complete occupied-cut exactness/errors and charge physical realization and F17 consumption.", + "blocked_by": "No admitted finite native producer or complete recursive/physical invoice is supplied here." + } + ] +} diff --git a/research/qq16-f0-physical-rounding/VERIFY.json b/research/qq16-f0-physical-rounding/VERIFY.json new file mode 100644 index 0000000000..7fb0f52037 --- /dev/null +++ b/research/qq16-f0-physical-rounding/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1042-audit/selected-replay.tar.gz", + "research/joint-query/certificate.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-Werror", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Four finite precisions; every literal native event and physical endpoint amplitude, two deterministic rounding sites and exact helper/private return." + }, + { + "argv": [ + "{python}", + "-Werror", + "-I", + "-O", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 240, + "checks": "Independent nearest-number oracle, frame/primitive checks, wider/clean/separate-site/scale controls, occupied native adapter mutation and source/receipt failures." + } + ] +} diff --git a/research/qq16-f0-physical-rounding/test_verify.py b/research/qq16-f0-physical-rounding/test_verify.py new file mode 100644 index 0000000000..23df60a55a --- /dev/null +++ b/research/qq16-f0-physical-rounding/test_verify.py @@ -0,0 +1,161 @@ +"""Behavioral controls for the hybrid physical-rounding witness. Apache-2.0.""" +import copy +from fractions import Fraction as Q +from pathlib import Path +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +# Execute source bytes; no stale local bytecode can replace the verifier. +import types +V = types.ModuleType('physical_rounding_checks') +V.__file__ = str(HERE / 'verify.py') +exec(compile((HERE / 'verify.py').read_bytes(), V.__file__, 'exec'), V.__dict__) +N = V.N + + +class PhysicalRounding(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.packet, cls.word, cls.recipes, cls.residuals = V.load() + cls.events = V.expand(cls.packet) + + def execute(self, entry, bits=53, events=None, round_at=None): + return V.execute(self.events if events is None else events, self.packet, + self.recipes, self.residuals, entry, bits, round_at) + + def test_independent_nearest_number_oracle(self): + # Enumerate representable signed integers, then minimize exact distance. + # This uses neither quotient/remainder rounding nor native vector code. + checks = 0 + for bits in range(2, 7): + representable = [0] + for n in range(1, 4097): + odd = n // (n & -n) + if odd.bit_length() <= bits: + representable.extend((n, -n)) + for value in range(-257, 258): + distance = min(abs(value-c) for c in representable) + ties = [c for c in representable if abs(value-c) == distance] + if len(ties) == 1: + want = ties[0] + else: + step = abs(ties[1]-ties[0]) + want = next(c for c in ties if (abs(c)//step) % 2 == 0) + self.assertEqual(V.rn_integer(value, bits), want) + checks += 1 + self.assertEqual(checks, 2575) + for bits in (8, 24, 53, 113): + n = (1 << (bits+12)) + 3 + self.assertEqual(V.rn_integer(n, bits), 1 << (bits+12)) + self.assertEqual(V.rn_integer(-n, bits), -(1 << (bits+12))) + + def test_native_primitive_conventions(self): + # Pairwise direct complex-Fraction formula, independent of the retained + # integer vector evaluator, including both line signs and imaginary data. + re = [((i*11) % 19)-9 for i in range(512)] + im = [((i*7) % 17)-8 for i in range(512)] + vector = N.vector(re, im, 3) + for axis, sign in ((1, 1), (37, -1), (256, 1)): + out = N.line(vector, axis, sign) + for i in range(512): + a, b, c, d = (Q(re[i], 8), Q(im[i], 8), + Q(re[i^axis], 8), Q(im[i^axis], 8)) + self.assertEqual(Q(out[0][i], 2**out[2]), (a-sign*b+c+sign*d)/2) + self.assertEqual(Q(out[1][i], 2**out[2]), (b+sign*a+d-sign*c)/2) + rows = tuple(1 << i for i in range(9)) + key = rows, (0,)*9, (0,)*9, 0, 1 + out = N.mono(vector, key) + self.assertEqual(out, N.vector([-x for x in im], re, 3)) + self.assertEqual(N.mono(out, key, True), vector) + + def test_finite_frame_rounding_intertwiner(self): + frames = [N.frame(axes) for axes in self.word['frames']] + self.assertEqual(len(frames), 1004) + for frame in frames: + self.assertEqual(frame[2], 0) + self.assertTrue(set(frame[0]+frame[1]) <= {0, -2, -1, 1, 2}) + # Scalar sample covers both signs and a nontrivial tie. The written + # homogeneity lemma, rather than this sample, quantifies the identity. + a = Q(33, 8) + lhs = V.rounded(N.scaled(frame, a), 4) + rounded_a = Q(V.rn_integer(33, 4), 8) + self.assertEqual(lhs, N.scaled(frame, rounded_a)) + for i in (3887, 4060): + self.assertEqual(self.events[i][2], 0) + self.assertEqual(frames[0], N.ONE) + + def test_wider_same_dirty_and_clean_controls(self): + entry = V.initial(53) + actual, faults = self.execute(entry, 65) + self.assertEqual(actual, entry) + self.assertEqual(faults, []) + clean = V.initial(53, dirty=False) + actual, faults = self.execute(clean) + self.assertEqual(actual, clean) + self.assertEqual(faults, []) + + def test_each_rounding_site_matters(self): + entry = V.initial(53) + expected_support = {3887: {112: Q(-1, 2), 114: Q(-1, 2), 137: Q(-1, 2), 139: Q(-1, 2)}, + 4060: {112: Q(-1, 2), 139: Q(1, 2), 190: Q(-1, 2), 211: Q(-1, 2)}} + for site in (3887, 4060): + actual, faults = self.execute(entry, round_at={site}) + self.assertEqual([x['event'] for x in faults], [site]) + want = list(entry) + for reg, delta in expected_support[site].items(): + want[reg] = N.plus(want[reg], N.scaled(N.ONE, delta)) + self.assertEqual(actual, want) + self.assertNotEqual(actual, V.expected(entry)) + + def test_dyadic_scale_sign_and_hilbert_bound(self): + signal = Q(-1, 32) + entry = V.initial(53, signal) + actual, faults = self.execute(entry) + self.assertEqual(actual, V.expected(entry, signal)) + self.assertEqual([x['event'] for x in faults], [3887, 4060]) + error = N.plus(actual[112], N.scaled(entry[112], Q(-1))) + self.assertEqual(V.squared_norm(entry[112]), Q(1, 2)) + self.assertEqual(V.squared_norm(error), Q(1, 2)) + + def test_occupied_exit_adapter_semantics(self): + # Removing an occupied, nonconstant target exit adapter must affect + # amplitudes, even though a source adapter on zero input might not. + events = copy.deepcopy(self.events) + index = 17721 + self.assertEqual(events[index][:3], ['adapter', 'new_to_old', 114]) + events[index] = ['phase', 'test_omitted_occupied_adapter'] + actual, faults = self.execute(V.initial(53), events=events) + self.assertEqual([x['event'] for x in faults], [3887, 4060]) + self.assertNotEqual(actual, V.expected(V.initial(53))) + self.assertEqual(actual[224:], V.initial(53)[224:]) + + def test_source_and_receipt_fail_closed(self): + with tempfile.TemporaryDirectory() as temp: + root = Path(temp) + target = root / 'research/joint-query/certificate.json.gz' + target.parent.mkdir(parents=True) + target.write_bytes(b'wrong') + # Inventory order may check the archive first: both live inputs + # are present, so the failure tests bytes rather than absence. + archive = root / 'research/community-frontier1042-audit/selected-replay.tar.gz' + archive.parent.mkdir(parents=True) + archive.write_bytes(b'wrong') + with self.assertRaisesRegex(ValueError, 'source pin'): + V.load(root) + with self.assertRaises(ValueError): + V.unique([('x', 1), ('x', 2)]) + with tempfile.TemporaryDirectory() as temp: + receipt = Path(temp) / 'receipt.json' + receipt.write_text('{"value":true}') + with self.assertRaisesRegex(ValueError, 'receipt mismatch'): + V.verify_receipt(receipt, {'value': 1}) + receipt.write_text('{"value":1,"value":2}') + with self.assertRaisesRegex(ValueError, 'duplicate JSON key'): + V.verify_receipt(receipt, {'value': 1}) + with self.assertRaises(ValueError): + V.rn_integer(1, 1) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/qq16-f0-physical-rounding/vendor/pr3017/native.py b/research/qq16-f0-physical-rounding/vendor/pr3017/native.py new file mode 100644 index 0000000000..e1976b3a55 --- /dev/null +++ b/research/qq16-f0-physical-rounding/vendor/pr3017/native.py @@ -0,0 +1,180 @@ +"""Exact Gaussian-dyadic vectors; no predecessor implementation is imported. + +Conventions follow the credited native Clifford sources in README.md. +Tekalign, with substantial OpenAI Codex assistance. Apache-2.0. +""" +from functools import lru_cache + +DIM = 512 + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def vector(real, imag=None, exponent=0): + real = tuple(real) + imag = tuple(imag) if imag is not None else (0,) * len(real) + need(len(real) == len(imag) == DIM and exponent >= 0, "vector dimensions") + if not any(real) and not any(imag): + return ZERO + while exponent and all(x % 2 == 0 for x in real + imag): + real = tuple(x // 2 for x in real) + imag = tuple(x // 2 for x in imag) + exponent -= 1 + return real, imag, exponent + + +ZERO = ((0,) * DIM, (0,) * DIM, 0) +ONE = ((1,) * DIM, (0,) * DIM, 0) + + +def rotate(a, b, phase): + return ((a, b), (-b, a), (-a, -b), (b, -a))[phase % 4] + + +def rank(rows): + pivots = {} + for value in rows: + while value: + high = value.bit_length() - 1 + if high not in pivots: + pivots[high] = value + break + value ^= pivots[high] + return len(pivots) + + +def transpose(rows): + return tuple(sum(((rows[j] >> i) & 1) << j for j in range(9)) for i in range(9)) + + +def inverse(rows): + aug = [x | (1 << (9 + i)) for i, x in enumerate(rows)] + for i in range(9): + pivot = next((j for j in range(i, 9) if (aug[j] >> i) & 1), None) + need(pivot is not None, "invertible binary map") + aug[i], aug[pivot] = aug[pivot], aug[i] + for j in range(9): + if j != i and (aug[j] >> i) & 1: + aug[j] ^= aug[i] + return tuple(x >> 9 for x in aug) + + +def monomial_key(record, axes=9): + """Reduce identity spectators, checking every discarded coordinate.""" + need(set(record) == {"matrix_rows", "quadratic_rows", "linear_Z4", "offset", "phase"}, + "monomial schema") + rows, quad, linear = (record[k] for k in ("matrix_rows", "quadratic_rows", "linear_Z4")) + need(len(rows) == len(quad) == len(linear) == axes, "monomial axes") + need(all(type(x) is int for x in rows + quad + linear), "integer monomial") + need(all(0 <= x < 2**axes for x in rows + quad) and all(0 <= x < 4 for x in linear), + "monomial coefficient range") + need(0 <= record["offset"] < DIM and 0 <= record["phase"] < 4, "monomial constants") + need(all(x < DIM for x in rows[:9] + quad[:9]), "no low/high coupling") + need(rows[9:] == [1 << i for i in range(9, axes)] + and not any(quad[9:] + linear[9:]), "identity spectators") + need(rank(rows[:9]) == 9, "invertible monomial") + return tuple(rows[:9]), tuple(quad[:9]), tuple(linear[:9]), record["offset"], record["phase"] + + +@lru_cache(256) +def table(key): + rows, quad, linear, offset, phase = key + result = [] + for x in range(DIM): + dest = offset ^ sum(((x & row).bit_count() % 2) << i for i, row in enumerate(rows)) + angle = phase + sum(linear[i] for i in range(9) if (x >> i) & 1) + # Old core stores symmetric Q; wrapper recipes store an upper triangle. + # Both conventions read each strict-upper pair exactly once. + angle += 2 * sum((quad[i] & x & ~((1 << (i + 1)) - 1)).bit_count() + for i in range(9) if (x >> i) & 1) + result.append((dest, angle % 4)) + need(len({dest for dest, _ in result}) == DIM, "monomial permutation") + return tuple(result) + + +def mono(value, key, adjoint=False): + re, im, exponent = value + rr, ii = [0] * DIM, [0] * DIM + for x, (dest, angle) in enumerate(table(key)): + if adjoint: + rr[x], ii[x] = rotate(re[dest], im[dest], -angle) + else: + rr[dest], ii[dest] = rotate(re[x], im[x], angle) + return vector(rr, ii, exponent) + + +def line(value, axis, sign=1, normalize=True): + need(0 < axis < DIM and sign in (-1, 1), "line parameters") + re, im, exponent = value + rr, ii = [], [] + for x in range(DIM): + a, b, c, d = re[x], im[x], re[x ^ axis], im[x ^ axis] + rr.append(a - sign*b + c + sign*d) + ii.append(b + sign*a + d - sign*c) + return vector(rr, ii, exponent + int(normalize)) + + +def recipe(value, record, axes=9): + r = record["rank"] + need(type(r) is int and 0 <= r <= 9, "child rank") + if r: + value = mono(value, monomial_key(record["right"], axes)) + for j in range(r): + value = line(value, 1 << j) + else: + need(record["right"] is None, "rank-zero recipe") + return mono(value, monomial_key(record["left"], axes)) + + +def diagonal(value, quad, linear, sign=1): + key = (tuple(1 << i for i in range(9)), tuple(quad), + tuple((sign*x) % 4 for x in linear), 0, 0) + return mono(value, key) + + +def permute(value, rows): + return mono(value, (tuple(rows), (0,) * 9, (0,) * 9, 0, 0)) + + +def frame(axes): + """T_U applied to the constant vector, using the stored ordered basis.""" + r = len(axes) + need(rank(axes) == r and all(0 < x < DIM for x in axes), "independent frame") + if r in (0, 9): + return ONE # I and the full coordinate C-product both fix constants. + ext = list(axes) + for axis in (1 << i for i in range(9)): + if rank(ext + [axis]) > len(ext): + ext.append(axis) + g = transpose(ext) + gi = inverse(g) + columns = transpose(gi) + quad = tuple((1 << i) ^ sum(((columns[i] & columns[j]).bit_count() % 2) << j + for j in range(9)) for i in range(9)) + linear = tuple((quad[i] >> i) & 1 for i in range(9)) + # Circuit: K^-1, F_r, K; K is P(G) followed by D(Q). + value = permute(diagonal(ONE, quad, linear, -1), gi) + for j in range(r): + value = line(value, 1 << j) + value = diagonal(permute(value, g), quad, linear) + need(sum(x*x for x in value[0] + value[1]) == DIM * 2**(2*value[2]), + "frame preserves squared norm") + return value + + +def scaled(value, coefficient): + n, d = coefficient.numerator, coefficient.denominator + need(d > 0 and d & (d-1) == 0, "dyadic coefficient") + return vector((n*x for x in value[0]), (n*x for x in value[1]), + value[2] + d.bit_length()-1) + + +def plus(left, right): + exponent = max(left[2], right[2]) + shifts = exponent-left[2], exponent-right[2] + return vector(((a << shifts[0]) + (b << shifts[1]) for a, b in zip(left[0], right[0])), + ((a << shifts[0]) + (b << shifts[1]) for a, b in zip(left[1], right[1])), + exponent) diff --git a/research/qq16-f0-physical-rounding/verify.py b/research/qq16-f0-physical-rounding/verify.py new file mode 100644 index 0000000000..3d6e9713bf --- /dev/null +++ b/research/qq16-f0-physical-rounding/verify.py @@ -0,0 +1,265 @@ +"""Deterministic component rounding in the literal native QQ16 F0 word. + +Ross Richardson with substantial OpenAI Codex assistance. Apache-2.0. +Exact vector primitives are retained unchanged from Tekalign/PR3017. +""" +import argparse +from collections import Counter +from fractions import Fraction as Q +from functools import lru_cache +import gzip +import hashlib +import json +from pathlib import Path +import tarfile +import types + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +MEMBERS = { + 'slots/local/CANONICAL-WORD.json.gz': '16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219', + 'slots/local/CLIFFORD-RECIPES.json': 'd0768f2164d5f64a2fdbec422f1cfde4e400818792f1904ca541958377243731', + 'slots/local/RESIDUAL-ADAPTERS.json': '383f40aadd00a4ac700dfd0d4c22d6c6c0be9a9863116e4d69c7acd23bafae0c', +} +N = types.ModuleType('exact_native_pr3017') +_NATIVE = HERE / 'vendor/pr3017/native.py' +# Authenticate source, and compile bytes rather than loading cached bytecode. +if hashlib.sha256(_NATIVE.read_bytes()).hexdigest() != '999eb1230798b25821de7771ecfa86381e137124059b30ccef167169d176ee8e': + raise ValueError('vendored native source pin') +exec(compile(_NATIVE.read_bytes(), str(_NATIVE), 'exec'), N.__dict__) +need = N.need + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':')).encode() + + +def digest(value): + return hashlib.sha256(canonical(value)).hexdigest() + + +def unique(pairs): + result = {} + for key, value in pairs: + need(key not in result, 'duplicate JSON key') + result[key] = value + return result + + +def read_json(path, limit=1_000_000): + raw = path.read_bytes() + need(len(raw) <= limit, 'JSON size bound') + return json.loads(raw, object_pairs_hook=unique) + + +def load(root=ROOT): + sources = read_json(HERE / 'SOURCES.json') + for entry in sources['files']: + if entry['usage'] == 'input': + raw = (root / entry['path']).read_bytes() + need(hashlib.sha256(raw).hexdigest() == entry['sha256'], 'source pin: ' + entry['path']) + objects = [] + with tarfile.open(root / 'research/community-frontier1042-audit/selected-replay.tar.gz') as archive: + for name, expected in MEMBERS.items(): + matches = [m for m in archive.getmembers() if m.name == name] + need(len(matches) == 1 and matches[0].isfile() and matches[0].size <= 12_000_000, + 'unique bounded regular archive member') + raw = archive.extractfile(matches[0]).read() + need(hashlib.sha256(raw).hexdigest() == expected, 'archive member pin: ' + name) + payload = gzip.decompress(raw) if name.endswith('.gz') else raw + need(len(payload) <= 12_000_000, 'archive payload bound') + objects.append(json.loads(payload, object_pairs_hook=unique)) + packet_raw = gzip.decompress((root / 'research/joint-query/certificate.json.gz').read_bytes()) + need(len(packet_raw) <= 12_000_000, 'certificate payload bound') + packet = json.loads(packet_raw, object_pairs_hook=unique) + need(packet['schema'] == 'conserved-qq16-full-cover-native-words-v1', 'certificate schema') + return (packet, *objects) + + +def expand(packet): + events = [] + for event in packet['programs']['F_0']: + if event[0] == 'retained_core': + need(event[1:3] == ['forward', 0], 'forward stage zero') + events.extend(packet['core_words']['forward']) + elif event[0] in ('cover_sweep', 'private_sweep'): + events.extend(event[2]) + else: + events.append(event) + need(len(events) == 26099, 'literal event count') + need(Counter(e[0] for e in events) == { + 'scalar': 21025, 'climb': 3486, 'adapter': 1090, + 'residual_adapter': 480, 'phase': 10, 'native_line': 8}, 'event inventory') + need(events[3887] == ['scalar', ['add', ['L', 112], ['L', 224], -1, 2], 0], 'first rounding site') + need(events[4060] == ['scalar', ['add', ['L', 139], ['L', 224], -1, 2], 0], 'second rounding site') + return events + + +def reg(token): + kind, index = token + need(kind in ('L', 'C') and type(index) is int, 'register token') + need(0 <= index < (704 if kind == 'L' else 8), 'register bound') + return index + 704 * (kind == 'C') + + +@lru_cache(32768) +def rn_integer(n, bits): + """RN-even of an integer significand; exponent is irrelevant and unbounded.""" + need(type(bits) is int and 2 <= bits <= 256, 'significand bound') + sign, a = (-1 if n < 0 else 1), abs(n) + shift = max(0, a.bit_length() - bits) + if not shift: + return n + quotient, remainder = divmod(a, 1 << shift) + if 2 * remainder > 1 << shift or (2 * remainder == 1 << shift and quotient % 2): + quotient += 1 + return sign * (quotient << shift) + + +def rounded(value, bits): + return N.vector((rn_integer(x, bits) for x in value[0]), + (rn_integer(x, bits) for x in value[1]), value[2]) + + +def component_hist(value): + return {part: dict(sorted(Counter(str(Q(x, 2**value[2])) for x in row).items())) + for part, row in zip(('real', 'imag'), value[:2])} + + +def squared_norm(value): + return Q(sum(x*x for x in value[0] + value[1]), 2**(2*value[2])) + + +def initial(bits, signal=Q(1), dirty=True): + state = [N.ZERO] * 712 + state[112] = N.scaled(N.ONE, signal) + if dirty: + state[224] = N.scaled(N.ONE, signal * 2**(bits + 12)) + return state + + +def execute(events, packet, recipes, residuals, state, bits=None, round_at=None): + """Direct physical vectors; no scalar projection or frame reduction executes the word.""" + 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']) and len(adapters) == 224, 'unique native recipes') + state, faults = list(state), [] + for index, event in enumerate(events): + kind = event[0] + if kind == 'scalar': + gate = event[1] + dst = reg(gate[1]) + if gate[0] == 'clear': + need(dst >= 704, 'only owned CLEAR') + state[dst] = N.ZERO + elif gate[0] == 'scale': + coefficient = Q(gate[2], gate[3]) + n = abs(coefficient.numerator) + need(n > 0 and n & (n-1) == 0, 'exact power-of-two SCALE') + state[dst] = N.scaled(state[dst], coefficient) + else: + need(gate[0] == 'add', 'known scalar operation') + src = reg(gate[2]) + need(src != dst, 'distinct ADD operands') + coefficient = Q(gate[3], gate[4]) + product = N.scaled(state[src], coefficient) + if bits is not None: + need(rounded(product, bits) == product, 'exact scalar coefficient product on witness') + exact = N.plus(state[dst], product) + actual = rounded(exact, bits) if bits is not None and ( + round_at is None or index in round_at) else exact + if actual != exact: + delta = N.plus(actual, N.scaled(exact, Q(-1))) + faults.append({'event': index, 'gate': gate, 'exact': component_hist(exact), + 'rounded': component_hist(actual), 'error': component_hist(delta)}) + state[dst] = actual + elif kind == 'climb': + _, _, dst, old, new, rank = event + recipe = children[old, new] + need(recipe['rank'] == rank, 'child rank') + if state[dst] != N.ZERO: + state[dst] = N.recipe(state[dst], recipe) + elif kind == 'adapter': + _, direction, dst, _ = event + if direction == 'old_to_new' and dst < 112: + state[dst] = N.mono(state[dst], N.monomial_key(adapters['source', dst]['left'])) + elif direction == 'new_to_old' and 112 <= dst < 224: + state[dst] = N.mono(state[dst], N.monomial_key(adapters['target', dst-112]['left']), True) + else: + need(direction in ('old_to_new', 'new_to_old'), 'adapter direction') + elif kind == 'residual_adapter': + direction, dst, a = event[1:4] + b = event[4] if len(event) == 5 else 1 + need(direction in ('pre', 'post'), 'residual direction') + key = str(a) if b == 1 else f'{a}:{b}' + part = 'right' if direction == 'pre' else 'left' + state[dst] = N.mono(state[dst], N.monomial_key(residuals['recipes'][key][part]), True) + elif kind == 'native_line': + dst = reg(event[1]) + state[dst] = N.recipe(state[dst], packet['native_line_recipes'][event[2]]['recipe']) + else: + need(kind == 'phase', 'known physical event') # phase events are control markers + return state, faults + + +def expected(entry, signal=Q(1)): + result = list(entry) + for index, error in ((112, -1), (114, Q(-1, 2)), (137, Q(-1, 2)), + (190, Q(-1, 2)), (211, Q(-1, 2))): + result[index] = N.plus(result[index], N.scaled(N.ONE, signal * error)) + return result + + +def witness(events, packet, recipes, residuals, bits): + entry = initial(bits) + ideal, exact_faults = execute(events, packet, recipes, residuals, entry) + need(ideal == entry and not exact_faults, 'exact physical endpoint') + actual, faults = execute(events, packet, recipes, residuals, entry, bits) + need(actual == expected(entry), 'all physical endpoint amplitudes') + need([row['event'] for row in faults] == [3887, 4060], 'only two actual rounding sites') + need(all(row['error'] == {'real': {'-1/2': 512}, 'imag': {'0': 512}} for row in faults), + 'all rounded component errors') + need(actual[224:704] == entry[224:704] and actual[704:] == [N.ZERO]*8, + 'exact physical helper return and private zero') + delta = [[i, component_hist(N.plus(a, N.scaled(b, Q(-1))))] + for i, (a, b) in enumerate(zip(actual, ideal)) if a != b] + return {'precision': bits, 'dirty_amplitude': str(2**(bits+12)), 'faults': faults, + 'endpoint_errors': delta, 'initial_data_squared_norm': '512', + 'maximum_error_squared_norm': '512', 'relative_error': '1', + 'ideal_endpoint_sha256': digest(ideal), 'rounded_endpoint_sha256': digest(actual), + 'all_480_helpers_exactly_restored': True, 'all_8_private_fields_zero': True} + + +def audit(root=ROOT): + packet, word, recipes, residuals = load(root) + events = expand(packet) + cases = [witness(events, packet, recipes, residuals, bits) for bits in (8, 24, 53, 113)] + return {'schema_version': 1, 'status': 'PASS_QQ16_F0_PHYSICAL_ROUNDING', + 'scope': 'finite native F0; component RN at scalar ADDs; exact native operators; unbounded exponents', + 'events': len(events), 'event_sha256': digest(events), 'active_axes': 9, + 'payload_coordinates': N.DIM, 'endpoint_amplitudes_per_case': 712*N.DIM, + 'native_operator_internals_rounded': False, 'cases': cases, + 'selected_frontier_changed': False, 'no_new_kappa': True} + + +def verify_receipt(path, result): + need(canonical(read_json(path)) == canonical(result), 'receipt mismatch') + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--root', type=Path, default=ROOT) + parser.add_argument('--write', type=Path, help='create an absent receipt') + args = parser.parse_args() + result = audit(args.root.resolve()) + if args.write: + with args.write.open('x') as stream: + stream.write(json.dumps(result, sort_keys=True, indent=2) + '\n') + else: + verify_receipt(HERE / 'RESULT.json', result) + print(result['status']) + print('4 finite precisions; 26,099 literal events each; exact helper/private return; no new kappa.') + + +if __name__ == '__main__': + main()