diff --git a/research/qq16-f0-rounded-scalar/README.md b/research/qq16-f0-rounded-scalar/README.md new file mode 100644 index 0000000000..9dc05b5b38 --- /dev/null +++ b/research/qq16-f0-rounded-scalar/README.md @@ -0,0 +1,130 @@ +# Correct rounding can lose data in the F0 scalar projection + +The literal QQ16 F0 **common-chart scalar projection**, executed with ordinary +binary64 arithmetic, loses a unit data input despite exactly restoring every +dirty helper. This supplies a concrete rounding example beyond the freely +admissible relative fault in [PR2995](https://github.com/CrocSwap/integer-mult-bounds/pull/2995) +and its [PR3017 native binding](https://github.com/CrocSwap/integer-mult-bounds/pull/3017). +Those packages explicitly leave concrete rounding open. + +This result is about the scalar projection only. It does not replace native +operators by identities in the physical producer or exhibit its rounding failure. + +## Exact experiment + +Use all 26,099 events obtained by concatenating the certificate's forward core +and F0 wrappers. There are 21,025 scalar instructions. As in the predecessor's +common-chart projection, omit the 3,486 climbs, 1,090 adapters, 480 residual +adapters, ten phase tags and eight new native lines. Flatten each private +sweep's scalar body in literal order. Event indices below are zero-based in +that expanded projection, including omitted events. + +Registers L0..L111 are X, L112..L223 are Y, L224..L703 are the 480 borrowed +helpers, and C0..C7 are the owned private fields. Initialize + +```text +Y0 = 1, L224 = T = 2^65; every other input = 0. +``` + +Exact rational execution returns precisely that entry state. With 53-bit +significands and round-to-nearest, ties-to-even, the result instead is + +```text +Y0 = 0, +Y2 = Y25 = Y78 = Y99 = -1/2, +L224 = 2^65; +every other output = 0. +``` + +All 480 borrowed helpers restore **exactly**, and all eight private outputs +are zero. The maximum absolute data error is one. There is no overflow or +underflow in the binary64 replay. + +Exactly two ADD instructions round: events 3887 and 4060, targeting L112 and +L139. At each, the stored target is 1/2, source L224 is T, and coefficient is +-1/2. Hence the exact operation result is `(1-T)/2`; binary64 stores `-T/2`, +with error -1/2. Every other scalar instruction is exact on the computed path. +The complete signed continuation produces the five differences above. +The two faults are consequences of the specified arithmetic, not chosen errors. + +For the first rounding decision, the representable number immediately toward +zero from `-2^64` is `-2^64+2^11`. The exact result `-2^64+1/2` is strictly +closer to `-2^64`. Thus this example does not depend on a tie-breaking accident. + +## Evidence and controls + +[RESULT.json](RESULT.json) records the full projection hash, both fault records, +every case's final 712-coordinate digest and chronological changed-field trace +digests. Exact, rounded, clean-helper and wider executions are recomputed. + +- The exact rational rounding interpreter implements a single correctly rounded + completed `target + coefficient*source`, with unbounded exponents. Actual + Python binary64, using separate multiplication and ADD, agrees at **every + scalar instruction** and on every final coordinate for the 53-bit witness. + These are two implementations of the arithmetic, not two native producers. +- Four checked cases use p=8,24,53,113 and T=2^(p+12). They have the same two + faults and five errors. This is finite coverage, not an all-p theorem. +- For each case, p+12 significand bits reproduce the exact endpoint with zero + rounded instructions. The exact trace's largest required significand is + precisely p+12. This is a sufficient escape for these inputs, not a general + F0 precision bound. Removing the dirty input also removes every fault. +- A separately implemented, explicitly enumerated finite binary number system + checks 7,740 nearest-rounding decisions, with additional signed tie controls. + Sign and power-of-two input scaling, changed/omitted literal gates, corrupted + source/receipt, and an optimized Git-free public replay are tested. + +Run from the repository root with standard-library Python 3.12: + +```sh +python3.12 -Werror -I -B scripts/research_package.py \ + --package research/qq16-f0-rounded-scalar +``` + +Direct normal or optimized `verify.py` execution also works without Git when +the package and its single declared scientific input are copied together. +Default replay is read-only. `--write` creates an absent receipt and refuses +to overwrite one. Source hashes and originating task/selected-record provenance +are in [SOURCES.json](SOURCES.json); actual scope and next questions are in +[TASK.json](TASK.json). + +## Implication and limits + +Exact dirty restoration does not ensure data accuracy for this literal scalar +implementation. A producer contract needs an actual range/grid/precision policy +if it relies on this projection. The completed-output transfer in +[PR2965](https://github.com/CrocSwap/integer-mult-bounds/pull/2965) is unchanged: +it assumes, rather than establishes, producer accuracy. + +The omitted native maps generally make intermediate physical vectors nonconstant. +Consequently the scalar rounding operation need not represent component rounding +in those vectors. PR3017's binding of a freely admissible defect does not bind +the two deterministic rounding errors here. That new implication remains open. +No native child interiors, B1, decoder replay, all-size realization, physical +ownership/movement, consumer invoice, selected cold replay or multiplication +theorem is verified here. No supplier or new kappa is claimed. + +Family decision: **narrow and stop** after this concrete arithmetic witness. +No construction expansion or full favorable budget is asserted; physical +costs remain unknown. + +## Open next questions + +Can the two deterministic scalar roundings be realized by an actual native +producer? Track physical frame vectors and component arithmetic at both marked +cuts, then replay their continuation and helper restoration. The blocker is +numerical conjugacy, not another arbitrary-defect sensitivity calculation. + +Alternatively, can a pinned native producer avoid this loss with a sufficiently +wide common grid and bounded dirty range? Supply its actual all-cut range, +rounded-child and restoration contracts before charging a complete consumer. +The p+12 control above is evidence only for this scalar input family. + +## Attribution + +New witness, implementation and tests: Arham Tahir, with substantial OpenAI Codex +assistance. Apache-2.0. No independent human or formal-kernel review is claimed. +Credit Nick Petalas/PR2965 for the producer-error handoff, Arham Tahir/PR2995 for +the earlier scalar relative-fault audit, Tekalign (tekuuu)/PR3017 for its native +binding, Ali Romman and the QQ16 team for the reviewed producer, and Sagar Thakrar, +DLamdata and the supplier/native/scalar lineage retained in +[the original notice](../joint-query/NOTICE.md). Frozen predecessors are unchanged. diff --git a/research/qq16-f0-rounded-scalar/RESULT.json b/research/qq16-f0-rounded-scalar/RESULT.json new file mode 100644 index 0000000000..d41cf011ad --- /dev/null +++ b/research/qq16-f0-rounded-scalar/RESULT.json @@ -0,0 +1,447 @@ +{ + "schema_version": 1, + "scope": "F0 common-chart scalar projection only", + "event_count": 26099, + "inventory": { + "adapter": 1090, + "climb": 3486, + "native_line": 8, + "phase": 10, + "residual_adapter": 480, + "scalar": 21025 + }, + "projection_sha256": "4c1ee518a6513c115741a3834c49490c6e8e68f5e2357af8dac782c3d40958e7", + "cases": [ + { + "precision": 8, + "dirty_exponent": 20, + "difference": [ + [ + 112, + "-1" + ], + [ + 114, + "-1/2" + ], + [ + 137, + "-1/2" + ], + [ + 190, + "-1/2" + ], + [ + 211, + "-1/2" + ] + ], + "ideal": { + "faults": [], + "trace_sha256": "50ed0240ca2846c171254a451739c129c434de6bcf59dba9dc09b39be9f79406", + "peak_exact_operation_precision": 20, + "first_peak_event": 3887, + "endpoint_sha256": "7cfdeac7484c2b55f8344b3d3ffc17c06b0ad4546b5175054b1e4bd9d3230667" + }, + "rounded": { + "faults": [ + { + "event": 3887, + "gate": [ + "add", + [ + "L", + 112 + ], + [ + "L", + 224 + ], + -1, + 2 + ], + "before": "1/2", + "exact": "-1048575/2", + "rounded": "-524288", + "error": "-1/2" + }, + { + "event": 4060, + "gate": [ + "add", + [ + "L", + 139 + ], + [ + "L", + 224 + ], + -1, + 2 + ], + "before": "1/2", + "exact": "-1048575/2", + "rounded": "-524288", + "error": "-1/2" + } + ], + "trace_sha256": "be22e3e7c2b886a1178a8a01d98274d88349f3a73e4bda4ad053cffecf05df4c", + "peak_exact_operation_precision": 20, + "first_peak_event": 3887, + "endpoint_sha256": "7440cd21b1e39a4629a7604c75c2a57dff1edbb0fee73592c2117be5a47ebb4c" + }, + "wide": { + "faults": [], + "trace_sha256": "50ed0240ca2846c171254a451739c129c434de6bcf59dba9dc09b39be9f79406", + "peak_exact_operation_precision": 20, + "first_peak_event": 3887, + "endpoint_sha256": "7cfdeac7484c2b55f8344b3d3ffc17c06b0ad4546b5175054b1e4bd9d3230667" + }, + "clean": { + "faults": [], + "trace_sha256": "8f59675dfb180cf2c289c3154b363fadf46cb0e54c437b4dc15261d5da11bcce", + "peak_exact_operation_precision": 1, + "first_peak_event": 5, + "endpoint_sha256": "b72318a38fcf4eb61205d5784d06284a8b3c7eec95c652bd25fa4be3c83894f9" + }, + "binary64": null + }, + { + "precision": 24, + "dirty_exponent": 36, + "difference": [ + [ + 112, + "-1" + ], + [ + 114, + "-1/2" + ], + [ + 137, + "-1/2" + ], + [ + 190, + "-1/2" + ], + [ + 211, + "-1/2" + ] + ], + "ideal": { + "faults": [], + "trace_sha256": "6b19efc901187b7c109c1c5aa380063648fd80984ccb9058276e448b7a9f3f3e", + "peak_exact_operation_precision": 36, + "first_peak_event": 3887, + "endpoint_sha256": "378437605530fa0f8b1270cbc68f4f721f7e39242f04e15c635e1141ee8f8a31" + }, + "rounded": { + "faults": [ + { + "event": 3887, + "gate": [ + "add", + [ + "L", + 112 + ], + [ + "L", + 224 + ], + -1, + 2 + ], + "before": "1/2", + "exact": "-68719476735/2", + "rounded": "-34359738368", + "error": "-1/2" + }, + { + "event": 4060, + "gate": [ + "add", + [ + "L", + 139 + ], + [ + "L", + 224 + ], + -1, + 2 + ], + "before": "1/2", + "exact": "-68719476735/2", + "rounded": "-34359738368", + "error": "-1/2" + } + ], + "trace_sha256": "4bedeea4e43dcb4634dc2448f93e66d78e522c4cf4d53d345fe2867a7fd92b75", + "peak_exact_operation_precision": 36, + "first_peak_event": 3887, + "endpoint_sha256": "40a93bc3034a61e2df63f0ae651f08741d49a468e2d2e7d0053c46ebef959403" + }, + "wide": { + "faults": [], + "trace_sha256": "6b19efc901187b7c109c1c5aa380063648fd80984ccb9058276e448b7a9f3f3e", + "peak_exact_operation_precision": 36, + "first_peak_event": 3887, + "endpoint_sha256": "378437605530fa0f8b1270cbc68f4f721f7e39242f04e15c635e1141ee8f8a31" + }, + "clean": { + "faults": [], + "trace_sha256": "8f59675dfb180cf2c289c3154b363fadf46cb0e54c437b4dc15261d5da11bcce", + "peak_exact_operation_precision": 1, + "first_peak_event": 5, + "endpoint_sha256": "b72318a38fcf4eb61205d5784d06284a8b3c7eec95c652bd25fa4be3c83894f9" + }, + "binary64": null + }, + { + "precision": 53, + "dirty_exponent": 65, + "difference": [ + [ + 112, + "-1" + ], + [ + 114, + "-1/2" + ], + [ + 137, + "-1/2" + ], + [ + 190, + "-1/2" + ], + [ + 211, + "-1/2" + ] + ], + "ideal": { + "faults": [], + "trace_sha256": "d1c0f0166266d986277e921326d17f1bfb25cdb36d841cb060f381371bd383dd", + "peak_exact_operation_precision": 65, + "first_peak_event": 3887, + "endpoint_sha256": "028d12161c7de4fd0462d995e22bbc6bfb0bedee45376aedd70222acd4c0b74a" + }, + "rounded": { + "faults": [ + { + "event": 3887, + "gate": [ + "add", + [ + "L", + 112 + ], + [ + "L", + 224 + ], + -1, + 2 + ], + "before": "1/2", + "exact": "-36893488147419103231/2", + "rounded": "-18446744073709551616", + "error": "-1/2" + }, + { + "event": 4060, + "gate": [ + "add", + [ + "L", + 139 + ], + [ + "L", + 224 + ], + -1, + 2 + ], + "before": "1/2", + "exact": "-36893488147419103231/2", + "rounded": "-18446744073709551616", + "error": "-1/2" + } + ], + "trace_sha256": "8a0330568b75834ba7364fe23f6f07cb2108379ec39c6ff0c4bef4a5cbc1a1a7", + "peak_exact_operation_precision": 65, + "first_peak_event": 3887, + "endpoint_sha256": "89ee2e68b13681a54454a47a5adc4b3a1c3fd98284d5256ad0fd1be4588c8af9" + }, + "wide": { + "faults": [], + "trace_sha256": "d1c0f0166266d986277e921326d17f1bfb25cdb36d841cb060f381371bd383dd", + "peak_exact_operation_precision": 65, + "first_peak_event": 3887, + "endpoint_sha256": "028d12161c7de4fd0462d995e22bbc6bfb0bedee45376aedd70222acd4c0b74a" + }, + "clean": { + "faults": [], + "trace_sha256": "8f59675dfb180cf2c289c3154b363fadf46cb0e54c437b4dc15261d5da11bcce", + "peak_exact_operation_precision": 1, + "first_peak_event": 5, + "endpoint_sha256": "b72318a38fcf4eb61205d5784d06284a8b3c7eec95c652bd25fa4be3c83894f9" + }, + "binary64": { + "faults": [ + { + "event": 3887, + "gate": [ + "add", + [ + "L", + 112 + ], + [ + "L", + 224 + ], + -1, + 2 + ], + "before": "1/2", + "exact": "-36893488147419103231/2", + "rounded": "-18446744073709551616", + "error": "-1/2" + }, + { + "event": 4060, + "gate": [ + "add", + [ + "L", + 139 + ], + [ + "L", + 224 + ], + -1, + 2 + ], + "before": "1/2", + "exact": "-36893488147419103231/2", + "rounded": "-18446744073709551616", + "error": "-1/2" + } + ], + "trace_sha256": "8a0330568b75834ba7364fe23f6f07cb2108379ec39c6ff0c4bef4a5cbc1a1a7", + "peak_exact_operation_precision": 65, + "first_peak_event": 3887, + "endpoint_sha256": "89ee2e68b13681a54454a47a5adc4b3a1c3fd98284d5256ad0fd1be4588c8af9" + } + }, + { + "precision": 113, + "dirty_exponent": 125, + "difference": [ + [ + 112, + "-1" + ], + [ + 114, + "-1/2" + ], + [ + 137, + "-1/2" + ], + [ + 190, + "-1/2" + ], + [ + 211, + "-1/2" + ] + ], + "ideal": { + "faults": [], + "trace_sha256": "aadfbb01f59ee5df10fcdb9b64fc0e7518442613e52726717ec92add47cd8ada", + "peak_exact_operation_precision": 125, + "first_peak_event": 3887, + "endpoint_sha256": "d2c2fe878f246fb37f33b623c3171ff0a2fd8b0522adda2162dc43e281102989" + }, + "rounded": { + "faults": [ + { + "event": 3887, + "gate": [ + "add", + [ + "L", + 112 + ], + [ + "L", + 224 + ], + -1, + 2 + ], + "before": "1/2", + "exact": "-42535295865117307932921825928971026431/2", + "rounded": "-21267647932558653966460912964485513216", + "error": "-1/2" + }, + { + "event": 4060, + "gate": [ + "add", + [ + "L", + 139 + ], + [ + "L", + 224 + ], + -1, + 2 + ], + "before": "1/2", + "exact": "-42535295865117307932921825928971026431/2", + "rounded": "-21267647932558653966460912964485513216", + "error": "-1/2" + } + ], + "trace_sha256": "603ff88005ef375a85e05f86ca736713693333839ffe4c08e85289e31e4d8c2a", + "peak_exact_operation_precision": 125, + "first_peak_event": 3887, + "endpoint_sha256": "d32f677a1065c9041174d45090bda45745a0c90ecc78b4baf188b48a511e6240" + }, + "wide": { + "faults": [], + "trace_sha256": "aadfbb01f59ee5df10fcdb9b64fc0e7518442613e52726717ec92add47cd8ada", + "peak_exact_operation_precision": 125, + "first_peak_event": 3887, + "endpoint_sha256": "d2c2fe878f246fb37f33b623c3171ff0a2fd8b0522adda2162dc43e281102989" + }, + "clean": { + "faults": [], + "trace_sha256": "8f59675dfb180cf2c289c3154b363fadf46cb0e54c437b4dc15261d5da11bcce", + "peak_exact_operation_precision": 1, + "first_peak_event": 5, + "endpoint_sha256": "b72318a38fcf4eb61205d5784d06284a8b3c7eec95c652bd25fa4be3c83894f9" + }, + "binary64": null + } + ] +} diff --git a/research/qq16-f0-rounded-scalar/SOURCES.json b/research/qq16-f0-rounded-scalar/SOURCES.json new file mode 100644 index 0000000000..358b3e0e00 --- /dev/null +++ b/research/qq16-f0-rounded-scalar/SOURCES.json @@ -0,0 +1,25 @@ +{ + "schema_version": 1, + "base_commit": "d8e0f83f00191df62174b641e9fff055c357f641", + "files": [ + { + "path": "research/joint-query/certificate.json.gz", + "sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7", + "payload_sha256": "2efe83c59978aa9c0db2c3e4eccc14cbfdcd3c9ce499432601b5dd34083472ef", + "git_blob": "c6e876d8b48d768214deee265ade428f8983b566", + "usage": "input" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] +} diff --git a/research/qq16-f0-rounded-scalar/TASK.json b/research/qq16-f0-rounded-scalar/TASK.json new file mode 100644 index 0000000000..cddc764679 --- /dev/null +++ b/research/qq16-f0-rounded-scalar/TASK.json @@ -0,0 +1,158 @@ +{ + "task_id": "joint-query-controller", + "scope_key": "qq16-f0-common-chart-correct-rounding", + "scope_status": "refined", + "scope_reason": "Test an actual correctly rounded scalar realization, rather than another freely chosen relative defect. Native instruction binding remains a separate obligation.", + "base_commit": "d8e0f83f00191df62174b641e9fff055c357f641", + "priority_revision": 6, + "picker_nonce": "5c1f4fc0976d13aef89f707d4bfac411", + "question": "Can the literal F0 common-chart scalar word lose bounded data under correctly rounded binary ADDs when a restored helper is large?", + "method": "Exact rational reference and integer round-to-nearest-ties-to-even execution of the full F0 scalar projection, with no exponent limits, one nonzero data coordinate and one nonzero dirty helper.", + "domain": "Pinned F0 scalar projection, all 712 endpoint coordinates; four finite significand sizes 8,24,53,113 and T=2^(p+12), plus clean, wider, signed and scaled controls.", + "nearest_predecessors": [ + { + "pr": 2965, + "head": "526f2c242202b31b15e09a7502dfb8ff757b2bad", + "credit": "Nick Petalas", + "delta": "Completed-output error transfer assumes producer errors; no producer arithmetic." + }, + { + "pr": 2995, + "head": "8ba0358b62edbeb16a0842473500c468d8c0759b", + "credit": "Arham Tahir", + "delta": "Freely admissible relative ADD fault; explicitly not a concrete rounding algorithm." + }, + { + "pr": 3017, + "head": "0f493f4c264fbc70ee14364b68af260d858c143c", + "credit": "Tekalign (tekuuu)", + "delta": "Native binding of the relative-fault witness; explicitly leaves actual rounding open." + } + ], + "budget": "No supplier saving is claimed. A counterexample to scalar accuracy is useful; full native range/grid and physical costs remain unknown.", + "success": "A reproducible actual rounding failure, exact ideal endpoint and dirty/private endpoint ledger, first lost-data cut, and an independently checked rounding oracle.", + "falsification": "Exact or sufficiently wide arithmetic reproduces the ideal data and helper endpoints; local nearest-rounding oracle agrees with native binary64 on finite in-range fixtures.", + "stop_rule": "Stop after one concrete arithmetic witness or a precise missing implication. No decoder optimization, physical supplier implementation or family expansion. Reserve final quarter of the session for verification and publication.", + "overlap": "Live canonical thread 2727 read through PR3017; full overlap refresh in progress. No actual correctly-rounded producer witness found in available PR/discussion bodies. No-match searches do not prove novelty.", + "author": "Arham Tahir with substantial OpenAI Codex assistance", + "license": "Apache-2.0", + "schema_version": 1, + "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" + ] + }, + "actual_scope": "One concrete correctly rounded binary execution of the literal F0 common-chart scalar projection with exact dirty-helper restoration.", + "scope_change_reason": "Test an actual correctly rounded scalar realization, rather than another freely chosen relative defect. Native instruction binding remains a separate obligation.", + "bottleneck_link": "Closes the concrete scalar-rounding gap left outside PR2995/3017, while explicitly retaining native numerical binding and producer range/grid/cost obligations.", + "budget_minutes": 60, + "outcome": "completed", + "evidence": "Full exact and rounded trace receipts for four precisions, cutwise binary64 agreement, five behavioral groups and independent 7740-case rounding oracle.", + "ai_assistance": "Substantial OpenAI Codex assistance in research, implementation, testing and writing; no independent human or formal-kernel review claimed.", + "open_questions": [ + { + "question": "Can both deterministic rounding errors occur in the actual native producer?", + "why_it_matters": "Scalar arithmetic and rounding do not automatically commute with native frame changes.", + "first_step": "Bind both marked cuts to physical component roundings and replay their exact continuation and helper restoration.", + "blocked_by": "Missing numerical conjugacy of the actual native operators." + }, + { + "question": "Can a bounded native producer avoid the loss with an affordable grid and dirty range?", + "why_it_matters": "The scalar wide-precision control is not a general producer format or a complete cost certificate.", + "first_step": "Derive native all-cut magnitude, grid and completed child contracts, then price the producer and consumer together.", + "blocked_by": "Actual finite native child implementation and physical cost ledger." + } + ], + "coordination": { + "canonical_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2727#discussioncomment-18981671", + "entry_overlap_utc": "2026-10-16T19:42:09Z", + "coverage": "277 open PRs, 2440 closed PR bodies, 1760 Discussion records; complete pagination. No actual rounding witness found; excludes arbitrary diffs/unpublished work.", + "submission_upstream_commit": "d8e0f83f00191df62174b641e9fff055c357f641", + "submission_refresh_utc": "2026-10-16T19:47:23.051484+00:00", + "submission_priority_revision": 6, + "submission_overlap": { + "coverage": { + "open_prs": { + "fetched_at": "2026-10-16T19:46:22.818656+00:00", + "complete_pagination": true, + "records": 277 + }, + "discussions": { + "fetched_at": "2026-10-16T19:46:59.665956+00:00", + "complete_pagination": true, + "records": 1766 + }, + "closed_prs": { + "fetched_at": "2026-10-16T19:47:22.891917+00:00", + "complete_pagination": true, + "records": 2440 + } + }, + "warnings": [], + "limits": "Remote PR scope includes open and closed/merged titles and bodies, with separate coverage and timestamps. State changes are deduplicated by latest PR update; snapshots are not atomic. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "decision": "13 textual leads inspected: own package/claim, PR2995/3017 predecessors, unrelated P104 rounding and arithmetic-audit records. No overlapping F0 concrete-rounding witness identified. PR3017 exact head reconfirmed unchanged." + } + }, + "family_expansion": { + "decision": "narrow and stop", + "proved_here": "Finite concrete scalar-rounding witness and exact restored-helper endpoint.", + "unknown": "Native rounding realization, complete range/grid and child contracts, physical consumer bill." + }, + "validation": { + "registered_replay": "Passed on CPython 3.12.14, including five optimized behavioral groups.", + "optimized_secondary": "CPython 3.14.7 optimized behavioral replay passed.", + "environment": "macOS-26.3.1-arm64-arm-64bit-Mach-O", + "lint": "Ruff unavailable locally; no installation attempted.", + "baseline": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY; full selected cold replay unrun." + } +} diff --git a/research/qq16-f0-rounded-scalar/VERIFY.json b/research/qq16-f0-rounded-scalar/VERIFY.json new file mode 100644 index 0000000000..8f43f37cf7 --- /dev/null +++ b/research/qq16-f0-rounded-scalar/VERIFY.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": ["research/joint-query/certificate.json.gz"], + "commands": [ + { + "argv": ["{python}", "-Werror", "-I", "-B", "{package}/verify.py"], + "timeout_seconds": 90, + "checks": "Four exact and correctly rounded complete scalar projections, all helper/private endpoints, exact wider/clean controls, complete cutwise native binary64 comparison and immutable receipt." + }, + { + "argv": ["{python}", "-Werror", "-I", "-O", "-B", "{package}/test_verify.py"], + "timeout_seconds": 180, + "checks": "Independent finite number-system oracle, scaling/sign controls, real-word semantic mutations, optimized Git-free CLI and source/receipt corruption." + } + ] +} diff --git a/research/qq16-f0-rounded-scalar/test_verify.py b/research/qq16-f0-rounded-scalar/test_verify.py new file mode 100644 index 0000000000..cb5e26e522 --- /dev/null +++ b/research/qq16-f0-rounded-scalar/test_verify.py @@ -0,0 +1,124 @@ +"""Independent rounding oracle and public-command behavior. + +Arham Tahir, with substantial OpenAI Codex assistance. Apache-2.0. +""" + +from bisect import bisect_left +from fractions import Fraction as Q +import importlib.util +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("rounded_f0", HERE / "verify.py") +v = importlib.util.module_from_spec(spec) +spec.loader.exec_module(v) + + +def nearest_table(value, candidates, bits): + """Definition-level finite set oracle; no logarithm or quotient rounding.""" + index = bisect_left(candidates, value) + if candidates[index] == value: + return value + low, high = candidates[index - 1:index + 1] + distance_low, distance_high = value - low, high - value + if distance_low != distance_high: + return low if distance_low < distance_high else high + # Determine parity by expressing each endpoint on the shared local grid. + step = high - low + return low if (low / step).denominator == 1 and int(low / step) % 2 == 0 else high + + +class RoundedF0Tests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.events, _ = v.load_events() + + def test_rounding_against_enumerated_number_system(self): + checks = 0 + for bits in range(2, 8): + positive = {Q(m) * Q(2) ** e for e in range(-20, 8) + for m in range(2 ** (bits - 1), 2 ** bits)} + candidates = sorted(positive | {-x for x in positive} | {Q(0)}) + for denominator_power in range(10): + for numerator in range(-64, 65): + value = Q(numerator, 2 ** denominator_power) + self.assertEqual(v.rn(value, bits), nearest_table(value, candidates, bits)) + checks += 1 + self.assertEqual(checks, 7740) + # Explicit ties across a binade boundary, including negative values. + self.assertEqual(v.rn(Q(15, 8), 3), Q(2)) + self.assertEqual(v.rn(Q(-15, 8), 3), Q(-2)) + self.assertEqual(v.rn(Q(9, 8), 3), Q(1)) + self.assertEqual(v.rn(Q(11, 8), 3), Q(3, 2)) + + def test_power_of_two_scaling_and_sign(self): + baseline, _ = v.execute(self.events, v.initial(53), 53) + for scale in (Q(-1), Q(1, 128), Q(16)): + entry = v.initial(53, signal=scale) + actual, info = v.execute(self.events, entry, 53) + self.assertEqual(actual, [scale * x for x in baseline]) + self.assertEqual(actual[224:], entry[224:]) + self.assertEqual([f["event"] for f in info["faults"]], [3887, 4060]) + + def test_real_word_semantic_controls(self): + # A changed sign or an omitted dirty cancellation must fail the original + # endpoint contract, rather than merely change a cosmetic trace hash. + for at, replacement in ((3887, None), (4060, None), (3887, 1)): + altered = self.events.copy() + if replacement is None: + altered.pop(at) + else: + gate = altered[at][1].copy() + gate[3] = replacement + altered[at] = ["scalar", gate, altered[at][2]] + with self.assertRaisesRegex(ValueError, "Exact witness endpoint"): + v.witness(altered, 53) + + def test_git_free_optimized_public_cli_and_corruption(self): + with tempfile.TemporaryDirectory() as temp: + root = Path(temp) + package = root / "research" / HERE.name + shutil.copytree(HERE, package, ignore=shutil.ignore_patterns("__pycache__")) + source_rel = "research/joint-query/certificate.json.gz" + source = root / source_rel + source.parent.mkdir(parents=True) + shutil.copyfile(v.ROOT / source_rel, source) + command = [sys.executable, "-Werror", "-I", "-O", "-B", str(package / "verify.py")] + + def run(): + return subprocess.run(command, text=True, capture_output=True, timeout=90) + + good = run() + self.assertEqual(good.returncode, 0, good.stderr) + self.assertIn("PASS_QQ16_F0_ROUNDED_SCALAR", good.stdout) + receipt = package / "RESULT.json" + original = receipt.read_bytes() + receipt.write_bytes(original.replace(b'"event_count": 26099', b'"event_count": 26098')) + bad_receipt = run() + self.assertNotEqual(bad_receipt.returncode, 0) + self.assertIn("Receipt mismatch", bad_receipt.stderr) + receipt.write_bytes(original) + source.write_bytes(b"wrong immutable input") + bad_source = run() + self.assertNotEqual(bad_source.returncode, 0) + self.assertIn("Source hash mismatch", bad_source.stderr) + + def test_numeric_and_namespace_boundaries(self): + for bits in (1, 257, True): + with self.assertRaisesRegex(ValueError, "Precision range"): + v.rn(Q(1), bits) + with self.assertRaisesRegex(ValueError, "Non-dyadic"): + v.rn(Q(1, 3), 53) + for token in (("X", 0), ("C", 8), ("L", -1)): + with self.assertRaises(ValueError): + v.register(token) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/qq16-f0-rounded-scalar/verify.py b/research/qq16-f0-rounded-scalar/verify.py new file mode 100644 index 0000000000..d54e587101 --- /dev/null +++ b/research/qq16-f0-rounded-scalar/verify.py @@ -0,0 +1,227 @@ +"""A correctly rounded F0 *scalar projection* counterexample. + +Arham Tahir, with substantial OpenAI Codex assistance. Apache-2.0. +Native non-scalar events are explicitly omitted, not certified as identities. +""" + +import argparse +from collections import Counter +from fractions import Fraction as Q +import gzip +from hashlib import sha256 +from io import BytesIO +import json +from pathlib import Path +import sys + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent +PRECISIONS = (8, 24, 53, 113) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def encoded(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def unique(pairs): + out = {} + for key, value in pairs: + need(key not in out, "Duplicate JSON key") + out[key] = value + return out + + +def read_json(path, limit=1_000_000): + raw = path.read_bytes() + need(len(raw) <= limit, "Oversized JSON") + return json.loads(raw, object_pairs_hook=unique) + + +def load_events(): + pins = [row for row in read_json(PACKAGE / "SOURCES.json")["files"] + if row["usage"] == "input"] + need(len(pins) == 1, "Exactly one scientific input") + pin = pins[0] + need(pin["path"] == "research/joint-query/certificate.json.gz", "Source path") + raw = (ROOT / pin["path"]).read_bytes() + need(len(raw) < 1_000_000 and sha256(raw).hexdigest() == pin["sha256"], + "Source hash mismatch") + with gzip.GzipFile(fileobj=BytesIO(raw)) as stream: + payload = stream.read(12_000_001) + need(len(payload) <= 12_000_000, "Oversized source payload") + need(sha256(payload).hexdigest() == pin["payload_sha256"], "Payload hash mismatch") + packet = json.loads(payload, object_pairs_hook=unique) + outer = packet["programs"]["F_0"] + need(outer[0][:3] == ["retained_core", "forward", 0], "F0 core binding") + events = list(packet["core_words"]["forward"]) + need(Counter(e[0] for e in outer[1:]) == {"cover_sweep": 5, "private_sweep": 8}, + "F0 wrapper shape") + for sweep in outer[1:]: + events.extend(sweep[2]) + counts = Counter(e[0] for e in events) + need(counts == {"scalar": 21025, "climb": 3486, "adapter": 1090, + "residual_adapter": 480, "phase": 10, "native_line": 8}, + "Full projection event inventory") + return events, dict(sorted(counts.items())) + + +def register(token): + kind, at = token + need(kind in ("L", "C") and type(at) is int, "Register kind") + need(0 <= at < (704 if kind == "L" else 8), "Register range") + return at + (704 if kind == "C" else 0) + + +def precision(value): + """Minimum binary significand length of a nonzero dyadic rational.""" + n, d = abs(value.numerator), value.denominator + need(d & (d - 1) == 0, "Non-dyadic state") + return n.bit_length() - (n & -n).bit_length() + 1 if n else 0 + + +def rn(value, bits): + """Exact nearest-even rounding, with an unbounded binary exponent.""" + need(type(bits) is int and 2 <= bits <= 256, "Precision range") + precision(value) + if not value: + return value + sign = -1 if value < 0 else 1 + x = abs(value) + exponent = x.numerator.bit_length() - x.denominator.bit_length() + if x < Q(2) ** exponent: + exponent -= 1 + quantum = Q(2) ** (exponent - bits + 1) + scaled = x / quantum + n, r = divmod(scaled.numerator, scaled.denominator) + if 2 * r > scaled.denominator or (2 * r == scaled.denominator and n % 2): + n += 1 + return sign * n * quantum + + +def initial(bits, dirty=True, signal=Q(1)): + state = [Q(0)] * 712 + state[112] = signal + state[224] = signal * (2 ** (bits + 12)) if dirty else Q(0) + return state + + +def execute(events, entry, bits=None, binary64=False): + state = list(map(float, entry)) if binary64 else entry.copy() + faults = [] + trace = sha256() + peak_precision = 0 + peak_at = None + for index, event in enumerate(events): + if event[0] != "scalar": + need(event[0] in ("climb", "adapter", "residual_adapter", "phase", "native_line"), + "Unknown omitted non-scalar event") + continue + gate = event[1] + at = register(gate[1]) + before = Q(state[at]) + op = gate[0] + if op == "clear": + need(at >= 704, "Only owned private CLEAR") + exact = Q(0) + actual = 0.0 if binary64 else exact + elif op == "scale": + coefficient = Q(gate[2], gate[3]) + need(abs(coefficient.numerator) & (abs(coefficient.numerator) - 1) == 0, + "SCALE power of two") + exact = before * coefficient + actual = state[at] * float(coefficient) if binary64 else exact + else: + need(op == "add", "Known scalar gate") + source = register(gate[2]) + need(source != at, "Distinct ADD operands") + coefficient = Q(gate[3], gate[4]) + exact = before + Q(state[source]) * coefficient + actual = (state[at] + state[source] * float(coefficient)) if binary64 else exact + if binary64: + # Separate hardware multiplication and ADD must match the favorable + # single-round completed ADD model at EVERY instruction, not just exit. + need(Q(actual) == rn(exact, 53), "Binary64/model cut mismatch") + elif bits is not None: + actual = rn(exact, bits) + count = precision(exact) + if count > peak_precision: + peak_precision, peak_at = count, index + if Q(actual) != exact: + faults.append({"event": index, "gate": gate, "before": str(before), + "exact": str(exact), "rounded": str(Q(actual)), + "error": str(Q(actual) - exact)}) + state[at] = actual + trace.update(encoded([index, at, str(Q(actual))]) + b"\n") + result = list(map(Q, state)) + return result, {"faults": faults, "trace_sha256": trace.hexdigest(), + "peak_exact_operation_precision": peak_precision, + "first_peak_event": peak_at, + "endpoint_sha256": sha256(encoded(list(map(str, result)))).hexdigest()} + + +def witness(events, bits): + entry = initial(bits) + ideal, exact_info = execute(events, entry) + need(ideal == entry, "Exact witness endpoint, including all helpers/private fields") + actual, rounded_info = execute(events, entry, bits) + delta = [[i, str(a - b)] for i, (a, b) in enumerate(zip(actual, ideal)) if a != b] + need(delta == [[112, "-1"], [114, "-1/2"], [137, "-1/2"], + [190, "-1/2"], [211, "-1/2"]], "Five-field data error") + need(actual[224:704] == entry[224:704], "Every borrowed helper restores") + need(actual[704:] == [0] * 8, "Every private output is zero") + need([f["event"] for f in rounded_info["faults"]] == [3887, 4060], + "Exactly two actual rounding sites") + need(all(f["error"] == "-1/2" for f in rounded_info["faults"]), "Fault values") + wide, wide_info = execute(events, entry, bits + 12) + need(wide == ideal and not wide_info["faults"], "Wider exact arithmetic escape") + clean, clean_info = execute(events, initial(bits, dirty=False), bits) + need(clean == initial(bits, dirty=False) and not clean_info["faults"], + "Zero-dirty control") + need(exact_info["peak_exact_operation_precision"] == bits + 12, + "Witness-specific exact precision") + binary64_info = None + if bits == 53: + machine, binary64_info = execute(events, entry, binary64=True) + need(machine == actual, "Native binary64 complete endpoint") + return {"precision": bits, "dirty_exponent": bits + 12, "difference": delta, + "ideal": exact_info, "rounded": rounded_info, + "wide": wide_info, "clean": clean_info, "binary64": binary64_info} + + +def compute(): + need(sys.float_info.mant_dig == 53 and sys.float_info.radix == 2, + "Native comparison requires binary64 Python float") + events, inventory = load_events() + return {"schema_version": 1, "scope": "F0 common-chart scalar projection only", + "event_count": len(events), "inventory": inventory, + "projection_sha256": sha256(encoded(events)).hexdigest(), + "cases": [witness(events, bits) for bits in PRECISIONS]} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="Create an absent RESULT.json") + args = parser.parse_args() + result = compute() + path = PACKAGE / "RESULT.json" + if args.write: + with path.open("x", encoding="utf-8") as stream: + stream.write(json.dumps(result, indent=2) + "\n") + else: + need(read_json(path) == result, "Receipt mismatch") + print("PASS_QQ16_F0_ROUNDED_SCALAR cases=4 rounding_sites=2 data_errors=5 " + "restored_helpers=480 native_binding=UNRUN no_new_kappa") + + +if __name__ == "__main__": + try: + main() + except (ValueError, OSError, KeyError, TypeError) as error: + print("FAIL_QQ16_F0_ROUNDED_SCALAR: " + str(error), file=sys.stderr) + raise SystemExit(1) from error