diff --git a/research/selected-quadratic-replay/BENCHMARK.json b/research/selected-quadratic-replay/BENCHMARK.json new file mode 100644 index 0000000000..f708a4a6bc --- /dev/null +++ b/research/selected-quadratic-replay/BENCHMARK.json @@ -0,0 +1,90 @@ +{ + "implementation_sha256": { + "benchmark.py": "74741a624954f0f1dd318f1adca9a565b8587ddf91638df8bce22d59ba4e1683", + "binding.py": "4e45c0a3ccabfb0adbf24e10f4b6e2ac3539ad8e1f6ceddd6e4ef10852cd8340", + "checks.py": "b92ac7c366e30f31a5f613f06ef12fec62e5998ae952c5ae80c1b9b88b3dfc5f", + "clifford_fast.py": "db570d2797f6280c8399f6001a4547ab20126353e9fb149e0e93ad0a079453b5", + "cross.py": "a9ea3bdfed7b96dd79cde32edf04aff7167a63712dcd14882b27ed0b06d4de32", + "local_fast.py": "ce9ff9e7bf5981c91642e712bbfec47c872b1260f7da3ea586e65473ceee5156", + "native_fast.py": "f70834109e904cf6046fe55667e4fe29504499aafb7262716b099d75027bd513", + "pins.py": "f1e7b282065aa8b9cea3f501598beb13cdf40b7343e4591393ee172fe8bb5741", + "run.py": "2bd1f562e786fb5c7b77c056d5f304e92cc29642d533a4dfd9dc5d0586cf0ca8", + "state_adapter.py": "ed3390ad0e4484a2e0127d63a1df5fd9c30e51fc7bc6014a8f9498e09702215b", + "verify.py": "4b8b0bb4127b42099494afcfec2062a7061d623a1261466c808bacd98fc6b9b5", + "verify_source.py": "166e680bb8f5729f5bcf984f8667f823a5bdb7fb2aa8f16418b6c770a483b3d5" + }, + "inputs": { + "research/exact-clifford-quadratic-replay/NOTICE.md": "a77adc71861e3b9c73c703c5db5b671f61a1101d85d14cca08547e21d6d8dce4", + "research/exact-clifford-quadratic-replay/PROOF.md": "e5039414a02e36cdeab82fb9803fc4de0c3e0f3997e8812ef9d227e5d417ec91", + "research/exact-clifford-quadratic-replay/quadratic.py": "d406584aed1479b75c387bc964b9e797b2f4f75e5f8c6bbea00df07f7d590a91", + "research/higher-moment-strictification/verify.py": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326", + "research/joint-helper-lattice/CONTROLLER.json": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "research/kappa-rebuild/architecture/mixed_target_probe.py": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a", + "research/p104-helper-subspace-splits/NOTICE": "8bbda66537ac761d632603066bdbb568ab5b26545030ea7979e27a85fcbe040c", + "research/p104-helper-subspace-splits/PROOF.md": "f4c68acf9373e34d88e14e1a7791b4b739c8b5297a1ae4c0121f579a02fde04e", + "research/p104-helper-subspace-splits/README.md": "a83c5c3ae7a31a5dfbc3c7c59669ee55cc15f966a0cb4405cb48cb8fa2a94f56", + "research/p104-helper-subspace-splits/RESULT.json": "1d92e587915052110dfb3aca8890df5afdaf496164efa5a4a52e69ceeb3c70f3", + "research/p104-helper-subspace-splits/SOURCES.json": "3c6dab6b491c904c8c2d2c76d5101ea13223ce7dc9b9a2acd2a37b038d1e6887", + "research/p104-helper-subspace-splits/SPLITS.json": "0bf3cf7d2abe118daa6d319a40f4f1b74b3c993d21b8d0fcb95299624797b244", + "research/p104-helper-subspace-splits/TASK.json": "4e5928f3a40f831668fd759ddc5b131198622e2c6dd2229b3b0d56de89c41ce3", + "research/p104-helper-subspace-splits/VALIDATION.md": "218e0e81fcd70c02fa2a1ae2f24676487ed498d93ce8dbc60f51c51d89e538ce", + "research/p104-helper-subspace-splits/VERIFY.json": "30499c00a5c6a9718561a152e8008ce1a765535647306dc4b2d2a7ce78b7b2ac", + "research/p104-helper-subspace-splits/WORD.json.gz": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099", + "research/p104-helper-subspace-splits/construct.py": "8e1a674ebed7bffb9fd6995555895a9925b665c2dec0e91f2876ff043901006f", + "research/p104-helper-subspace-splits/inputs/PR5565-WORD.json.gz": "3d62828f53e654e3db218bf4611a47aed4a677d48043713dc004db0f8a32990d", + "research/p104-helper-subspace-splits/inputs/PR5580-WORD.json.gz": "b2a98c4bd0dbe86c09e9d15ee060dcf1aab09dbef90aa1e2127676f4039f406b", + "research/p104-helper-subspace-splits/local.py": "ef430511ce36fc658ab711bd84cd2d7b484b8af173238ff89cbfec6139fefbad", + "research/p104-helper-subspace-splits/pricing.py": "637c8b0eea8bf870d866707de8230aa8ddd0c7401b56153f65b60913b025000b", + "research/p104-helper-subspace-splits/search.py": "668022953f53929fd4d95ed1b5c01ac2ba3b4bdf6be7babae511757eb21b7e6a", + "research/p104-helper-subspace-splits/verify.py": "f79c78d009d8a88bc5721644237074569fbb992fe7e49784f4b0c0a97523ea91", + "research/p104-native-channel/vendor/clifford_exact.py": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "research/p104-native-channel/vendor/native_verify.py": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38", + "research/p104-productive-controller/CONTROLLER.json": "a84f6bbd547379597464e56c420cc665f96bc43a9a1351eed4b7cd0fce3cc4b9", + "research/p104-productive-controller/caller.py": "300d40043953e4f6aecfde8f2d1004b8ad6dc5a79ec3c7666c9908c2466c91c8", + "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15", + "research/pr4359-p7-padding/native_inventory.py": "65539acaf45bdfe8c5aee6830f9c9b3d1107c442a60842ef803fdd7688de8f32", + "research/query-thinned-controllers/RESULT.json": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f" + }, + "machine": "arm64", + "median_seconds": { + "literal": 269.0034654160263, + "quadratic": 98.37080179096665 + }, + "median_speedup": 2.7345864882513213, + "platform": "macOS-26.6.1-arm64-arm-64bit", + "python": "3.12.14 (main, Aug 25 2026, 13:50:33) [Clang 22.1.3 ]", + "rows": [ + { + "mode": "literal", + "seconds": 264.334065125091, + "stdout_sha256": "1975d01770a017b3f0b3a98a54c7c79b887d90ba0a2e1a77c37db05c385fa42b" + }, + { + "mode": "quadratic", + "seconds": 80.88713349995669, + "stdout_sha256": "1975d01770a017b3f0b3a98a54c7c79b887d90ba0a2e1a77c37db05c385fa42b" + }, + { + "mode": "quadratic", + "seconds": 98.37080179096665, + "stdout_sha256": "1975d01770a017b3f0b3a98a54c7c79b887d90ba0a2e1a77c37db05c385fa42b" + }, + { + "mode": "literal", + "seconds": 305.8997332500294, + "stdout_sha256": "1975d01770a017b3f0b3a98a54c7c79b887d90ba0a2e1a77c37db05c385fa42b" + }, + { + "mode": "literal", + "seconds": 269.0034654160263, + "stdout_sha256": "1975d01770a017b3f0b3a98a54c7c79b887d90ba0a2e1a77c37db05c385fa42b" + }, + { + "mode": "quadratic", + "seconds": 175.99428945791442, + "stdout_sha256": "1975d01770a017b3f0b3a98a54c7c79b887d90ba0a2e1a77c37db05c385fa42b" + } + ], + "scope": "Complete selected scientific replay; fresh processes, warm OS caches, variable host load. Extra adapter corpus and literal cross-check are separate." +} diff --git a/research/selected-quadratic-replay/CROSS.json b/research/selected-quadratic-replay/CROSS.json new file mode 100644 index 0000000000..bdb31a40fa --- /dev/null +++ b/research/selected-quadratic-replay/CROSS.json @@ -0,0 +1,12 @@ +{ + "actual_state_calls": { + "amplitude_entries": 19988992, + "dense": 32777, + "evaluations": 39041, + "sparse": 6264 + }, + "amplitudes_per_literal_interpreter": 9037312, + "distinct_inputs": 17651, + "input_trace_sha256": "73ac04db73d83151efb474925d48298664cc7490d31bdec7a70dcf79b448f481", + "literal_interpreters": 2 +} diff --git a/research/selected-quadratic-replay/NOTICE b/research/selected-quadratic-replay/NOTICE new file mode 100644 index 0000000000..c84f3ee22e --- /dev/null +++ b/research/selected-quadratic-replay/NOTICE @@ -0,0 +1,31 @@ +New selected-caller integration, format adapter, bounded input cache and checks: +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +The same assistant wrote the code and performed the author-side checks. + +The exact quadratic engine and its proof are retained from Ali Romman PR 5704, +head daa4d9dbd102d2a3677afc5614c56466bd2cf3a2. Its NOTICE.md remains byte-exact +and credits classical stabilizer simulation, Charles Bethin PR 662 and all +native/compiler predecessors. This package does not claim that engine as new. + +The complete selected source is Ali Romman PR 5599, audited source head +09dd0965711ca7eeb169057a420abab1c9052137. Its exact word, receipt, proof and +NOTICE remain inputs. That notice retains Pierre-Loic Doulcet/hexapode, +Joel Pulikkan/GamingPuzzled, DreamingOfClouds, thu-nmrc, Gareth Davidson/bitplane, +David Arias, Cinna Davis, Jacob Alan Sussman, zxv, Cao Yifan and earlier geometry, +BIT and analytic credit. The derived files retain their original module text. + +Classical deterministic memoization and exact affine-support enumeration are +not new general algorithms. The new result is their checked integration into +this complete source replay, with every scalar/native/invoice/compiler check, +independent literal-state evidence and whole-replay measurements. No original +source, selected record, native bill or kappa is changed. Archive inclusion, +local replay and hosted CI are separate from independent mathematical review. + +Native-channel attribution from its pinned README: Rohan Arun PR 1972 supplied +the scalar/frame channel; Adam Gall PR 1940 supplied the schedule. Josie Elliston +PR 1071 supplied the P104 fixture/decoder, with Ali Romman PR 1125 and the retained +PR 968/717/446/595/620 lineage. icekylinx's frame-sa504 retains the exact compiler; +Ali Romman PR 1862/1931 retains the independent Gaussian interpreter. Native +lowering and physical binding were prepared for Chafik Boukhalfa with OpenAI +Codex assistance. These are predecessor contributions, not work of this adapter. +Source: https://github.com/CrocSwap/integer-mult-bounds/blob/553d26d796fde9871ff2661a49ac7732e945410f/research/p104-native-channel/README.md diff --git a/research/selected-quadratic-replay/PORTABILITY.json b/research/selected-quadratic-replay/PORTABILITY.json new file mode 100644 index 0000000000..42a383fa7a --- /dev/null +++ b/research/selected-quadratic-replay/PORTABILITY.json @@ -0,0 +1,27 @@ +{ + "readonly_files_unchanged": 54, + "optimized_git_free": true, + "empty_path": true, + "source_corruption_rejected": true, + "python": "Python 3.12.14", + "science_commit": "83823449895cb1126c246570b92992d45157fe02", + "export_sha256": "7d9369a6870deb505aba75f53fcb5a08db2d2b95dec67d4946f58cc59b7b93f3", + "registered_commands": "Both VERIFY.json commands, serially, with -I -O -B and empty PATH", + "actual_input_controls": [ + { + "path": "research/exact-clifford-quadratic-replay/quadratic.py", + "rejected": true, + "restored_sha256": "d406584aed1479b75c387bc964b9e797b2f4f75e5f8c6bbea00df07f7d590a91" + }, + { + "path": "research/p104-helper-subspace-splits/WORD.json.gz", + "rejected": true, + "restored_sha256": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099" + }, + { + "path": "research/p104-native-channel/vendor/clifford_exact.py", + "rejected": true, + "restored_sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + } + ] +} diff --git a/research/selected-quadratic-replay/PROOF.md b/research/selected-quadratic-replay/PROOF.md new file mode 100644 index 0000000000..e1238892b0 --- /dev/null +++ b/research/selected-quadratic-replay/PROOF.md @@ -0,0 +1,97 @@ +# Exact selected-state adapter + +This package reuses the quadratic-state engine and proof from PR 5704. It does +not change the native compiler, controller, local word or invoice. Its new +claims concern the state-format conversion, bounded cache and complete source +integration. + +## State-format conversion + +The retained engine returns `(n,o,C,p,a,b,d)`. Its nonzero support is +`o + span(C)` over F2. The columns C are independent. For a coefficient vector +z, the amplitude at `o + C*z` is `(a+ib)*i^p(z)/2^d`. Its proof covers each gate +in the retained P/D/X/C/phase grammar and includes the absolute phase. + +The adapter enumerates every z in `{0,1}^len(C)`. Independence makes each address +unique, so assignment to the output map cannot overwrite another amplitude. +All other addresses have amplitude zero. The dense result fills those addresses +with `(0,0)`; the sparse result omits them. Both use the same denominator d. +The engine divides the scalar pair by every common factor of two. Every nonzero +amplitude is a rotation of that pair, so it has the same common factor of two. +Thus this denominator is the same minimal denominator used by both original +literal interpreters. The returned vectors and maps are exactly equal to the +original representations, not merely scalar multiples or the same support. + +The selected native width is 9. Dense conversion therefore retains all 512 +entries. This adapter does not claim polynomial storage for its dense public +interface. The reused engine avoids literal state evolution at each gate; +the final dense result remains available to every original caller check. + +## Bounded cache and invalidation + +Each key contains width, the complete ordered circuit, and the initial basis +address. The key builder copies lists and tuples to nested immutable tuples. +Its only scalar types are exact integers and strings. It rejects booleans, +floats and other objects before cache lookup, so Python numeric aliases cannot +turn a malformed input into a hit on a valid integer key. + +On a miss, the unchanged engine validates and evaluates that exact key. The +result contains only immutable tuples and integers. The function is pure with +respect to these inputs, so a hit has the same value as another evaluation. +Changing a gate, gate order, matrix entry, width or initial address changes the +key. Equal list and tuple forms have the same gate semantics. Each output vector +or map is constructed anew; a caller cannot mutate the cached signature. + +The process holds at most 8192 keys. Eviction removes only a reusable answer; +a later request recomputes it. No entry is saved between processes. The cache +contains neither a selected result nor a claimed invoice. Source authentication +runs before the scientific replay. Every caller check still executes and every +new exact state input is evaluated. This is checked reuse of a pure function, +not reuse of a scientific acceptance decision. + +## Complete source binding + +`binding.py` constructs the expected syntax tree from four exact retained files. +It changes only these sites: + +- The compiler's `Op.zero_state` calls the dense adapter. +- The independent native interpreter's `state` calls the sparse adapter. +- The local verifier loads those two explicit derived modules. +- The top-level verifier uses the derived local module, keeps all original input + paths, accepts an explicit argument list, and rejects its source-write option. +- Every remaining assertion becomes `if not condition: raise AssertionError`. + Its condition and optional message stay unchanged. This retains the check + when Python runs with `-O`. + +All other source syntax must match. A missing native-phase check, a missing +public-row check and an omitted complete pricing call each fail this binding. +The only 13 assertions in the declared Python input closure are in the retained +Clifford compiler. All 13 are retained as explicit failures in its derived copy. +The original files and classes are never patched at runtime. Comments are not +part of the syntax comparison; source files and attribution stay in the export. + +The derived main runs the same selected scientific obligations and compares +both the complete RESULT and regenerated WORD with the retained artifacts. +It preserves all 13 helper cuts, arbitrary rational input rows, dense reverse +columns, native maps and phases, productive target checks, physical contacts, +query and idle work, two moment engines, compiler and all outer inequalities. +The original rejected input/output/target/cost mutations still run. + +## Independent checks and claim boundary + +The small adapter corpus compares 1522 exact states and 22700 amplitude entries +with the original interpreters. Separate controls check type aliases, key +invalidation, mutable outputs, bounded capacity, eviction and source-proof +omissions. `cross.py` reruns the complete selected check and collects every +actual state input. It then compares each distinct input against both original +literal interpreters, including every numerator, zero and denominator. +Repeated equal inputs need one independent comparison; the fresh full replay +still records every call. The trace hash and counts are checked on replay. + +The source's signed Pauli checks stay unchanged. Equality of a valid Clifford +operator's signed Pauli action and one nonzero state fixes its absolute phase; +the adapter does not substitute a zero-column test for those Pauli checks. +The saved selected receipt must stay identical. This retains the existing +conditional kappa statement and its five assumptions. It proves no new supplier, +physical runtime improvement, precision theorem or selected-frontier change. +The engine proof and scientific predecessor results remain credited dependencies. diff --git a/research/selected-quadratic-replay/README.md b/research/selected-quadratic-replay/README.md new file mode 100644 index 0000000000..182bbe84b1 --- /dev/null +++ b/research/selected-quadratic-replay/README.md @@ -0,0 +1,93 @@ +# Complete selected P104 replay with exact quadratic states + +The complete selected scientific replay is 2.73x faster on this host: median +269.00 to 98.37 seconds across three alternating fresh processes per engine. +Every run has identical complete scientific stdout. The original range is +264.33..305.90 s; the new range is 80.89..175.99 s. Host load varies. This is a +verification speedup, not a faster physical multiplier or a new kappa. + +Both original literal interpreters independently match all 17,651 distinct +state inputs from a fresh complete replay. Each comparison covers 9,037,312 +amplitude entries, including every zero and denominator. CROSS.json records +the exact input trace digest. + +The selected P104 verifier compiles 3131 native maps and checks 2923 distinct +frame pairs. Its compiler performs 32777 dense zero-state evaluations, and the +independent native checks perform 6264 sparse evaluations. This package uses the +archived PR 5704 exact quadratic-state engine at those two interfaces. It returns +the original full vectors and maps, so the caller's state checks stay intact. + +A bounded cache stores only exact immutable state signatures, keyed by the full +circuit, width and initial basis. Numeric aliases reject before lookup. Every +new input is validated and evaluated. Returned mutable vectors cannot change +the cache. There is no persistent cache or stored scientific acceptance result. +The [proof](PROOF.md) explains the conversion, denominator, cache and integration. + +## Reproduce + +Python 3.12 and the standard library suffice. From the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/selected-quadratic-replay +python3.12 -B research/selected-quadratic-replay/run.py +python3.12 -B research/selected-quadratic-replay/benchmark.py --output /tmp/selected-benchmark.json +``` + +The registered verifier runs the complete selected result and then the +independent actual-state cross-check, serially. The benchmark runs six fresh +processes in literal/new/new/literal/literal/new order. It requires identical +complete scientific stdout and rejects a changed implementation between runs. +The extra adapter corpus and literal cross-check are separate from the timed +complete source replay. The two-command package audit includes extra literal +work; no speedup is claimed for that larger audit. OS caches can be warm and +host load can vary. + +`binding.py` compares every derived syntax tree with the exact source plus a +small declared transformation. Three omitted scientific checks reject. The +original source files are unchanged. The derived compiler retains every +remaining assertion as an explicit failure, including under `-O`. + +## Scope and evidence + +The complete result retains all 13 helper cuts, rational independent-input rows, +dense reverse columns, exact native maps and global phases, every physical +contact, productive main and helper targets, query and idle costs, both moment +engines, compiler checks and all outer predicates. It retains the source's +wrong-input, wrong-output, wrong-phase, extra-target and unpaid-call controls. +Both the regenerated WORD and complete RESULT must equal the retained artifacts. + +The adapter corpus checks 1522 states and 22700 amplitude entries. Cache controls +cover type aliases, changed matrices/gates/widths/initial bases, mutable outputs, +capacity and eviction. All 39041 source state requests still execute. The process +cache has 21073 hits and 17968 misses, with at most 8192 entries. The source covers +19988992 amplitude entries before the separate independent literal cross-check. + +This changes verification capacity. The selected conditional kappa .00310045, +complete invoice, native construction and five framework assumptions stay the +same. No physical multiplier speedup, new kappa, independent human acceptance or +proof-kernel result is claimed. This opt-in package does not change the selected +frontier or its official reproduction command. + +## Sources and attribution + +Base 553d26d796fde9871ff2661a49ac7732e945410f; frozen priority 7 card. +The submission refresh at de5ec2e7a6074068452f45b1a191b5c72832df4a read +priority 8. Its verification tooling task still calls for measured speed gains +with exact coverage. This result does not repeat the completed admission audit. The selected source is +PR 5599 at audited head 09dd0965711ca7eeb169057a420abab1c9052137. The reused exact +engine is PR 5704 at daa4d9dbd102d2a3677afc5614c56466bd2cf3a2. All 31 live inputs +have Git blob and SHA256 pins in SOURCES.json. The source and engine notices +remain byte-exact. The [canonical investigation](https://github.com/CrocSwap/integer-mult-bounds/discussions/5748) +records scope and plan changes. + +The [NOTICE](NOTICE) retains construction, engine, native, controller, compiler +and classical stabilizer credit. New integration and checks: Ali Romman with +substantial OpenAI Codex assistance. No subagents. Apache-2.0. + +## Open next questions + +- Does the whole-replay speedup hold on Linux and another host? Run the same + serial benchmark and compare exact stdout before making that claim. +- Can a newer reviewed P104 word use this integration? Begin with exact source + pins and a complete syntax-tree binding. A passing older word is not evidence + for a changed caller, bill or native phase. diff --git a/research/selected-quadratic-replay/RESULT.json b/research/selected-quadratic-replay/RESULT.json new file mode 100644 index 0000000000..0ae6024e84 --- /dev/null +++ b/research/selected-quadratic-replay/RESULT.json @@ -0,0 +1,30 @@ +{ + "cache": { + "currsize": 8192, + "hits": 21073, + "maxsize": 8192, + "misses": 17968 + }, + "controls": { + "cache_controls": "Complete keys, type aliases, changed inputs, output mutation, capacity and eviction", + "explicit_assertion_control": "Mismatched widths reject, including under -O", + "literal_amplitude_entries": 22700, + "literal_state_cases": 1522, + "proof_controls": 3 + }, + "derived_files": { + "clifford_fast.py": "db570d2797f6280c8399f6001a4547ab20126353e9fb149e0e93ad0a079453b5", + "local_fast.py": "ce9ff9e7bf5981c91642e712bbfec47c872b1260f7da3ea586e65473ceee5156", + "native_fast.py": "f70834109e904cf6046fe55667e4fe29504499aafb7262716b099d75027bd513", + "verify_source.py": "166e680bb8f5729f5bcf984f8667f823a5bdb7fb2aa8f16418b6c770a483b3d5" + }, + "source_inputs": 31, + "source_scientific_sha256": "1d92e587915052110dfb3aca8890df5afdaf496164efa5a4a52e69ceeb3c70f3", + "source_word_sha256": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099", + "state_evaluations": { + "amplitude_entries": 19988992, + "dense": 32777, + "evaluations": 39041, + "sparse": 6264 + } +} diff --git a/research/selected-quadratic-replay/SOURCES.json b/research/selected-quadratic-replay/SOURCES.json new file mode 100644 index 0000000000..90ca37eac4 --- /dev/null +++ b/research/selected-quadratic-replay/SOURCES.json @@ -0,0 +1,235 @@ +{ + "schema_version": 1, + "base_commit": "553d26d796fde9871ff2661a49ac7732e945410f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/exact-clifford-quadratic-replay/NOTICE.md", + "usage": "input", + "git_blob": "b96b400e5ca04b3a9003a8b2c70a2461972d39d7", + "sha256": "a77adc71861e3b9c73c703c5db5b671f61a1101d85d14cca08547e21d6d8dce4", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/exact-clifford-quadratic-replay/NOTICE.md" + }, + { + "path": "research/exact-clifford-quadratic-replay/PROOF.md", + "usage": "input", + "git_blob": "559f9f4b207783c6eb908450b63eed3431594c22", + "sha256": "e5039414a02e36cdeab82fb9803fc4de0c3e0f3997e8812ef9d227e5d417ec91", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/exact-clifford-quadratic-replay/PROOF.md" + }, + { + "path": "research/exact-clifford-quadratic-replay/quadratic.py", + "usage": "input", + "git_blob": "ce3c86ec07fd5767741e02ff0c88b93ba9164fb4", + "sha256": "d406584aed1479b75c387bc964b9e797b2f4f75e5f8c6bbea00df07f7d590a91", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/exact-clifford-quadratic-replay/quadratic.py" + }, + { + "path": "research/higher-moment-strictification/verify.py", + "usage": "input", + "git_blob": "4b24a5096154736ce060474eb8c72dc64c303699", + "sha256": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/higher-moment-strictification/verify.py" + }, + { + "path": "research/joint-helper-lattice/CONTROLLER.json", + "usage": "input", + "git_blob": "49a2f0675819f9deeea27ed77be2c2b6ff2e87e5", + "sha256": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/joint-helper-lattice/CONTROLLER.json" + }, + { + "path": "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json", + "usage": "input", + "git_blob": "d9a4f84211182ca200c081ea061d724c8a2cfb70", + "sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json" + }, + { + "path": "research/kappa-rebuild/architecture/mixed_target_probe.py", + "usage": "input", + "git_blob": "4fc05ab08138218ba9f09e5c89b649afae7c914e", + "sha256": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/kappa-rebuild/architecture/mixed_target_probe.py" + }, + { + "path": "research/p104-helper-subspace-splits/NOTICE", + "usage": "input", + "git_blob": "f34687ff7eab377d5433f7b0c18274a816d2b73c", + "sha256": "8bbda66537ac761d632603066bdbb568ab5b26545030ea7979e27a85fcbe040c", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/p104-helper-subspace-splits/NOTICE" + }, + { + "path": "research/p104-helper-subspace-splits/PROOF.md", + "usage": "input", + "git_blob": "ca979984444a431b02b62da7094a3b23d5341742", + "sha256": "f4c68acf9373e34d88e14e1a7791b4b739c8b5297a1ae4c0121f579a02fde04e", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/p104-helper-subspace-splits/PROOF.md" + }, + { + "path": "research/p104-helper-subspace-splits/README.md", + "usage": "input", + "git_blob": "f6303a881379723e1f6512dfe153fafeecbf62dd", + "sha256": "a83c5c3ae7a31a5dfbc3c7c59669ee55cc15f966a0cb4405cb48cb8fa2a94f56", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/p104-helper-subspace-splits/README.md" + }, + { + "path": "research/p104-helper-subspace-splits/RESULT.json", + "usage": "input", + "git_blob": "35f75c8555193c6e845cd52cc562ca23fd5924cb", + "sha256": "1d92e587915052110dfb3aca8890df5afdaf496164efa5a4a52e69ceeb3c70f3", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/p104-helper-subspace-splits/RESULT.json" + }, + { + "path": "research/p104-helper-subspace-splits/SOURCES.json", + "usage": "input", + "git_blob": "f83bf3c8184bc2d40451ac6ba5e8f46e7bee89c1", + "sha256": "3c6dab6b491c904c8c2d2c76d5101ea13223ce7dc9b9a2acd2a37b038d1e6887", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/p104-helper-subspace-splits/SOURCES.json" + }, + { + "path": "research/p104-helper-subspace-splits/SPLITS.json", + "usage": "input", + "git_blob": "5108daabf7b30043b36da2875dcb30aee2fa7012", + "sha256": "0bf3cf7d2abe118daa6d319a40f4f1b74b3c993d21b8d0fcb95299624797b244", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/p104-helper-subspace-splits/SPLITS.json" + }, + { + "path": "research/p104-helper-subspace-splits/TASK.json", + "usage": "input", + "git_blob": "a230fe5b901af6abc3e3b2e20ca92273ce294d3a", + "sha256": "4e5928f3a40f831668fd759ddc5b131198622e2c6dd2229b3b0d56de89c41ce3", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/p104-helper-subspace-splits/TASK.json" + }, + { + "path": "research/p104-helper-subspace-splits/VALIDATION.md", + "usage": "input", + "git_blob": "7f73fd1454ba67cc05dd03edcbe9bfb79ee41630", + "sha256": "218e0e81fcd70c02fa2a1ae2f24676487ed498d93ce8dbc60f51c51d89e538ce", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/p104-helper-subspace-splits/VALIDATION.md" + }, + { + "path": "research/p104-helper-subspace-splits/VERIFY.json", + "usage": "input", + "git_blob": "f02fe9b97043e626e9906346d230508247a5871d", + "sha256": "30499c00a5c6a9718561a152e8008ce1a765535647306dc4b2d2a7ce78b7b2ac", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/p104-helper-subspace-splits/VERIFY.json" + }, + { + "path": "research/p104-helper-subspace-splits/WORD.json.gz", + "usage": "input", + "git_blob": "e325091e3051afe37a2d9c82f85afe9028510edb", + "sha256": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/p104-helper-subspace-splits/WORD.json.gz" + }, + { + "path": "research/p104-helper-subspace-splits/construct.py", + "usage": "input", + "git_blob": "698a4cbcc0d7afbba8dccfb7f453315ed7230795", + "sha256": "8e1a674ebed7bffb9fd6995555895a9925b665c2dec0e91f2876ff043901006f", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/p104-helper-subspace-splits/construct.py" + }, + { + "path": "research/p104-helper-subspace-splits/inputs/PR5565-WORD.json.gz", + "usage": "input", + "git_blob": "4ebe6fcb7adf319bf6b247cf23d89eb1ca4cd914", + "sha256": "3d62828f53e654e3db218bf4611a47aed4a677d48043713dc004db0f8a32990d", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/p104-helper-subspace-splits/inputs/PR5565-WORD.json.gz" + }, + { + "path": "research/p104-helper-subspace-splits/inputs/PR5580-WORD.json.gz", + "usage": "input", + "git_blob": "9434855e7dad0d0236d23210b3e71a2b83a9ae64", + "sha256": "b2a98c4bd0dbe86c09e9d15ee060dcf1aab09dbef90aa1e2127676f4039f406b", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/p104-helper-subspace-splits/inputs/PR5580-WORD.json.gz" + }, + { + "path": "research/p104-helper-subspace-splits/local.py", + "usage": "input", + "git_blob": "e6e28bacdad7cb51400d827b9a6e02f2b605d357", + "sha256": "ef430511ce36fc658ab711bd84cd2d7b484b8af173238ff89cbfec6139fefbad", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/p104-helper-subspace-splits/local.py" + }, + { + "path": "research/p104-helper-subspace-splits/pricing.py", + "usage": "input", + "git_blob": "0b54ad3f16e3c1068e9e36ee83187e150325a791", + "sha256": "637c8b0eea8bf870d866707de8230aa8ddd0c7401b56153f65b60913b025000b", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/p104-helper-subspace-splits/pricing.py" + }, + { + "path": "research/p104-helper-subspace-splits/search.py", + "usage": "input", + "git_blob": "1bf5329658683919a97430138b57860751da7ba9", + "sha256": "668022953f53929fd4d95ed1b5c01ac2ba3b4bdf6be7babae511757eb21b7e6a", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/p104-helper-subspace-splits/search.py" + }, + { + "path": "research/p104-helper-subspace-splits/verify.py", + "usage": "input", + "git_blob": "547751915ad09b2229bacf29af02241b0ef29696", + "sha256": "f79c78d009d8a88bc5721644237074569fbb992fe7e49784f4b0c0a97523ea91", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/p104-helper-subspace-splits/verify.py" + }, + { + "path": "research/p104-native-channel/vendor/clifford_exact.py", + "usage": "input", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/p104-native-channel/vendor/clifford_exact.py" + }, + { + "path": "research/p104-native-channel/vendor/native_verify.py", + "usage": "input", + "git_blob": "2c209dfa9cfade3bc20ac5fc9d876b433a147f8c", + "sha256": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/p104-native-channel/vendor/native_verify.py" + }, + { + "path": "research/p104-productive-controller/CONTROLLER.json", + "usage": "input", + "git_blob": "cc539db709cf7a6c42872c4380902736ad453af3", + "sha256": "a84f6bbd547379597464e56c420cc665f96bc43a9a1351eed4b7cd0fce3cc4b9", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/p104-productive-controller/CONTROLLER.json" + }, + { + "path": "research/p104-productive-controller/caller.py", + "usage": "input", + "git_blob": "6ac5e735691555ecafe2afbcff71edd923178113", + "sha256": "300d40043953e4f6aecfde8f2d1004b8ad6dc5a79ec3c7666c9908c2466c91c8", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/p104-productive-controller/caller.py" + }, + { + "path": "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py", + "usage": "input", + "git_blob": "340e1f0ffb8a1a9c38fbbd9119580b6d23e01b59", + "sha256": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py" + }, + { + "path": "research/pr4359-p7-padding/native_inventory.py", + "usage": "input", + "git_blob": "8d2d96e3998254c2333c43fe47cdfd074cbd811e", + "sha256": "65539acaf45bdfe8c5aee6830f9c9b3d1107c442a60842ef803fdd7688de8f32", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/pr4359-p7-padding/native_inventory.py" + }, + { + "path": "research/query-thinned-controllers/RESULT.json", + "usage": "input", + "git_blob": "e0695152c98d727edfd0d2034b58a1c7e8682c0c", + "sha256": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f", + "pin": "head:553d26d796fde9871ff2661a49ac7732e945410f:research/query-thinned-controllers/RESULT.json" + } + ] +} diff --git a/research/selected-quadratic-replay/TASK.json b/research/selected-quadratic-replay/TASK.json new file mode 100644 index 0000000000..e96bf44f60 --- /dev/null +++ b/research/selected-quadratic-replay/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 7, + "base_commit": "553d26d796fde9871ff2661a49ac7732e945410f", + "original_card": { + "id": "replay-runtime", + "question": "Can one measured replay bottleneck be sped up without dropping coverage?", + "starting_points": [ + "scripts/run_isolated_tests.py", + "scripts/verify_replay_coverage.py", + "certificates/selected-result.json" + ], + "methods": [ + "Profile one isolated replay and optimize the measured bottleneck.", + "Design source-bound reuse with explicit dependency invalidation and negative controls." + ], + "acceptance_gate": "Report before/after wall time on the same fixture, retained checks and invalidation behavior.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected reproduction command and choose a single replay stage for profiling.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Measure one unchanged fixture, preserve check coverage, and test one optimization with invalidation controls.", + "bottleneck_link": "Faster trustworthy replays increase review throughput and let mechanism candidates be checked sooner.", + "allowed_variations": [ + "Profile one stage or design one source-bound cache boundary." + ], + "scope_change_triggers": [ + "Skipping coverage or comparing different fixtures to claim speedup." + ], + "overlap_terms": [ + "replay runtime", + "cache invalidation", + "isolated tests" + ] + }, + "scope_status": "refined", + "actual_scope": "Complete selected P104 replay with exact quadratic-state format adapters and bounded input-keyed memoization", + "scope_change_reason": "The selected native compiler is the measured bottleneck. A full uncached quadratic replay passed in 180.42 seconds. Bounded pure-function reuse was then added, with typed-key and mutation controls. The public claim records this change.", + "bottleneck_link": "Faster full selected native and invoice verification reduces the cost of checking changed P104 constructions.", + "budget_minutes": 120, + "stop_rule": "Stop if complete source checks or exact scientific results differ, or if the whole source replay does not improve.", + "outcome": "completed", + "evidence": "All complete source checks pass with unchanged RESULT and WORD. Six alternating fresh processes give medians of 269.00 seconds literal and 98.37 seconds new (2.7346x). Both original literal interpreters independently match all 17,651 distinct actual inputs and 9,037,312 amplitude entries each. See RESULT.json, CROSS.json and BENCHMARK.json.", + "author": "Ali Romman with substantial OpenAI Codex assistance", + "ai_assistance": "Ali Romman with substantial OpenAI Codex assistance; no subagents.", + "open_questions": [ + { + "question": "Does the complete speedup hold on the registered Linux host?", + "why_it_matters": "Replay capacity depends on the full caller, not one state kernel.", + "first_step": "Run the same six fresh processes and compare every scientific stdout hash.", + "blocked_by": "Independent host execution has not been run." + }, + { + "question": "Can the next reviewed P104 word reuse this explicit integration?", + "why_it_matters": "Fast complete checks can shorten construction and review loops.", + "first_step": "Pin its full source and assert a complete syntax-tree diff before using the adapter.", + "blocked_by": "A changed source needs its own source binding and full scientific replay." + } + ], + "priority_refresh": { + "commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "revision": 8, + "decision": "Keep the assigned verification optimization. Revision 8 requests measured replay gains with exact coverage. The selected admission itself is already complete." + } +} diff --git a/research/selected-quadratic-replay/VALIDATION.md b/research/selected-quadratic-replay/VALIDATION.md new file mode 100644 index 0000000000..f6d8fff595 --- /dev/null +++ b/research/selected-quadratic-replay/VALIDATION.md @@ -0,0 +1,63 @@ +# Validation record + +Base 553d26d796fde9871ff2661a49ac7732e945410f. Registered interpreter: +`/Users/aliromman/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3`, +Python 3.12.14 on macOS arm64. + +Completed before the final benchmark: + +- The unchanged complete selected source passes and matches both saved artifacts. + Its first cold measurement was 391.93981024995446 s. This single measurement is + orientation evidence; it is not substituted for the alternating benchmark. +- The uncached quadratic prototype passes the full selected replay in 180.42 s. + This is not the final implementation or final speedup figure. +- The bounded-cache implementation passes the complete source and all new controls. + RESULT.json records 39041 state requests,19988992 amplitude entries,21073 cache + hits and 17968 misses. The cache holds at most 8192 entries. +- The adapter checks compare 1522 literal states and 22700 amplitudes. Changed keys, + invalid numeric aliases, mutable outputs, capacity and eviction controls pass. +- Three actual source-proof omissions reject. The width-mismatch assertion rejects + under optimized Python. All 13 assertions in the declared input closure are + retained as explicit failures in the derived compiler. +- `scripts/research_package.py --package research/selected-quadratic-replay --check-only` + passes metadata and pins. This is not scientific acceptance. + +The serial six-process benchmark passes with identical stdout SHA256 +`1975d01770a017b3f0b3a98a54c7c79b887d90ba0a2e1a77c37db05c385fa42b` in every run. +Medians:269.0034654160263 s literal and 98.37080179096665 s new; ratio 2.7345864882513213. +BENCHMARK.json retains every run, source input and implementation digest. + +The complete actual-state audit passes: 17,651 distinct inputs and 9,037,312 +amplitude entries per original literal interpreter. Both interpreters agree +with every new state numerator, zero and denominator. The trace SHA256 is +`73ac04db73d83151efb474925d48298664cc7490d31bdec7a70dcf79b448f481`. + +The canonical-main refresh at de5ec2e7a6074068452f45b1a191b5c72832df4a +read priority 8. At 16:25 UTC, the overlap cache covered all 312 open PRs and +5,110 Discussion records. The only matching active claim was this investigation. +The local scan covered 7,840 main notes at the frozen base. Later main notes +require a separate search before submission. + +The scientific commit is `83823449895cb1126c246570b92992d45157fe02`. +The byte/mode preflight and official 53-file export pass. Its sealed export +(including the export manifest) passes both registered commands serially with +Python 3.12.14, `-I -O -B`, empty PATH, no Git, files mode 444 and directories +mode 555. All 54 file bytes and modes remain unchanged. PORTABILITY.json records +the export digest. Separate corruptions of the actual quadratic engine, selected +WORD and native compiler each reject before evaluation and restore exactly. + +A second live overlap refresh at 16:35 UTC covers 313 open PRs and 5,114 +Discussion records. Only this investigation matches the scoped terms. A separate +Git search of the latest canonical main at de5ec2e7 finds no matching package; +all 31 exact input bytes still match that main. Priority 8 is unchanged. + +The checkout is shallow. The optional full-history source-ancestry preflight +is not run. Explicit source bytes and Git blobs, committed export and Git-free +replay are checked. This is an export-availability check, not full Git history. + +The standard `scripts/research_package.py --package` runner also passes both +commands under Python 3.12.14 with `PASS_REGISTERED_RESEARCH_PACKAGE`. +Only documentation, TASK wording and the portability receipt change after the +scientific commit. All 12 Python implementation hashes still match BENCHMARK.json. +See the canonical Discussion for the final published head and readback status. +Hosted CI, independent human review and proof-kernel acceptance are separate. diff --git a/research/selected-quadratic-replay/VERIFY.json b/research/selected-quadratic-replay/VERIFY.json new file mode 100644 index 0000000000..c632da8aaa --- /dev/null +++ b/research/selected-quadratic-replay/VERIFY.json @@ -0,0 +1,59 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/exact-clifford-quadratic-replay/NOTICE.md", + "research/exact-clifford-quadratic-replay/PROOF.md", + "research/exact-clifford-quadratic-replay/quadratic.py", + "research/higher-moment-strictification/verify.py", + "research/joint-helper-lattice/CONTROLLER.json", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json", + "research/kappa-rebuild/architecture/mixed_target_probe.py", + "research/p104-helper-subspace-splits/NOTICE", + "research/p104-helper-subspace-splits/PROOF.md", + "research/p104-helper-subspace-splits/README.md", + "research/p104-helper-subspace-splits/RESULT.json", + "research/p104-helper-subspace-splits/SOURCES.json", + "research/p104-helper-subspace-splits/SPLITS.json", + "research/p104-helper-subspace-splits/TASK.json", + "research/p104-helper-subspace-splits/VALIDATION.md", + "research/p104-helper-subspace-splits/VERIFY.json", + "research/p104-helper-subspace-splits/WORD.json.gz", + "research/p104-helper-subspace-splits/construct.py", + "research/p104-helper-subspace-splits/inputs/PR5565-WORD.json.gz", + "research/p104-helper-subspace-splits/inputs/PR5580-WORD.json.gz", + "research/p104-helper-subspace-splits/local.py", + "research/p104-helper-subspace-splits/pricing.py", + "research/p104-helper-subspace-splits/search.py", + "research/p104-helper-subspace-splits/verify.py", + "research/p104-native-channel/vendor/clifford_exact.py", + "research/p104-native-channel/vendor/native_verify.py", + "research/p104-productive-controller/CONTROLLER.json", + "research/p104-productive-controller/caller.py", + "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py", + "research/pr4359-p7-padding/native_inventory.py", + "research/query-thinned-controllers/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Authenticate sources, retain every source proof check, check state conversion and cache invalidation, replay the complete selected caller and compare both saved scientific artifacts." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/cross.py" + ], + "timeout_seconds": 600, + "checks": "Collect every actual state input from the complete selected replay and independently compare every literal amplitude and denominator for all distinct inputs." + } + ] +} diff --git a/research/selected-quadratic-replay/benchmark.py b/research/selected-quadratic-replay/benchmark.py new file mode 100644 index 0000000000..de7db07593 --- /dev/null +++ b/research/selected-quadratic-replay/benchmark.py @@ -0,0 +1,58 @@ +"""Time serial fresh processes with identical complete scientific output.""" +import argparse +from hashlib import sha256 +import json +from pathlib import Path +import platform +import statistics +import subprocess +import sys +import time + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +from pins import authenticate + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--output', type=Path, required=True) + args = parser.parse_args() + authenticate() + implementation = {p.name: sha256(p.read_bytes()).hexdigest() for p in sorted(HERE.glob('*.py'))} + rows = [] + expected = None + for mode in ('literal', 'quadratic', 'quadratic', 'literal', 'literal', 'quadratic'): + authenticate() + if implementation != {p.name: sha256(p.read_bytes()).hexdigest() for p in sorted(HERE.glob('*.py'))}: + raise ValueError('Benchmark implementation changed between processes') + path = (ROOT / 'research/p104-helper-subspace-splits/verify.py' + if mode == 'literal' else HERE / 'run.py') + start = time.perf_counter() + run = subprocess.run([sys.executable, '-B', str(path)], cwd=ROOT, + capture_output=True, timeout=600) + elapsed = time.perf_counter() - start + if run.returncode or run.stderr: + raise ValueError('Benchmark replay failed: ' + run.stderr.decode(errors='replace')) + digest = sha256(run.stdout).hexdigest() + if expected is None: + expected = digest + if digest != expected: + raise ValueError('Complete scientific stdout differs') + row = {'mode': mode, 'seconds': elapsed, 'stdout_sha256': digest} + rows.append(row) + print(json.dumps(row, sort_keys=True), flush=True) + medians = {mode: statistics.median(r['seconds'] for r in rows if r['mode'] == mode) + for mode in ('literal', 'quadratic')} + result = {'python': sys.version, 'platform': platform.platform(), 'machine': platform.machine(), + 'implementation_sha256': implementation, + 'rows': rows, 'median_seconds': medians, + 'median_speedup': medians['literal'] / medians['quadratic'], + 'scope': 'Complete selected scientific replay; fresh processes, warm OS caches, variable host load. Extra adapter corpus and literal cross-check are separate.', + 'inputs': {r['path']: r['sha256'] for r in json.loads((HERE / 'SOURCES.json').read_bytes())['files'] if r['usage'] == 'input'}} + args.output.write_text(json.dumps(result, indent=2, sort_keys=True) + '\n', encoding='utf-8') + + +if __name__ == '__main__': + main() diff --git a/research/selected-quadratic-replay/binding.py b/research/selected-quadratic-replay/binding.py new file mode 100644 index 0000000000..6e20fb67c9 --- /dev/null +++ b/research/selected-quadratic-replay/binding.py @@ -0,0 +1,87 @@ +"""Bind explicit derived files to the complete retained selected verifier. + +Only the declared state methods, input paths, imports and CLI guards differ. +All remaining assertions become explicit failures so that -O retains them. +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +import ast +from hashlib import sha256 +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = 'research/p104-helper-subspace-splits' +PAIRS = { + 'clifford_fast.py': 'research/p104-native-channel/vendor/clifford_exact.py', + 'native_fast.py': 'research/p104-native-channel/vendor/native_verify.py', + 'local_fast.py': SOURCE + '/local.py', + 'verify_source.py': SOURCE + '/verify.py', +} + + +def replace(text, old, new, count=1): + if text.count(old) != count: + raise ValueError('Unexpected source integration site: ' + old) + return text.replace(old, new) + + +class ExplicitAssertions(ast.NodeTransformer): + def visit_Assert(self, node): + args = [] if node.msg is None else [node.msg] + return ast.copy_location(ast.If(ast.UnaryOp(ast.Not(), node.test), + [ast.Raise(ast.Call(ast.Name('AssertionError', ast.Load()), args, []), None)], []), node) + + +def expected(filename): + text = (ROOT / PAIRS[filename]).read_text(encoding='utf-8') + if filename in ('local_fast.py', 'verify_source.py'): + text = replace(text, 'ROOT = HERE.parents[1]', + "ROOT = HERE.parents[1]\nHERE = ROOT / '" + SOURCE + "'") + if filename == 'local_fast.py': + text = replace(text, 'research/p104-native-channel/vendor/clifford_exact.py', + 'research/selected-quadratic-replay/clifford_fast.py') + text = replace(text, 'research/p104-native-channel/vendor/native_verify.py', + 'research/selected-quadratic-replay/native_fast.py') + if filename == 'verify_source.py': + text = replace(text, 'import local as L', 'import local_fast as L') + text = replace(text, 'sys.path.insert(0, str(HERE))', + 'sys.path.insert(0, str(HERE))\n sys.path.insert(0, str(Path(__file__).resolve().parent))') + text = replace(text, 'def main():', 'def main(argv=None):') + text = replace(text, 'args = parser.parse_args()', + "args = parser.parse_args(argv)\n need(not args.write, 'Derived replay cannot write source artifacts')") + tree = ast.parse(text) + if filename == 'clifford_fast.py': + tree.body.insert(1, ast.parse('from state_adapter import dense_state').body[0]) + cls, = [n for n in tree.body if isinstance(n, ast.ClassDef) and n.name == 'Op'] + method, = [n for n in cls.body if isinstance(n, ast.FunctionDef) and n.name == 'zero_state'] + method.body = ast.parse('return dense_state(self.n, self.circuit, basis)').body + if filename == 'native_fast.py': + tree.body.insert(1, ast.parse('from state_adapter import sparse_state').body[0]) + method, = [n for n in tree.body if isinstance(n, ast.FunctionDef) and n.name == 'state'] + method.body = ast.parse('return sparse_state(circuit, basis)').body + return ast.fix_missing_locations(ExplicitAssertions().visit(tree)) + + +def check(overrides=None): + result = {} + for filename in PAIRS: + raw = (overrides or {}).get(filename, (HERE / filename).read_text(encoding='utf-8')) + if ast.dump(ast.parse(raw), include_attributes=False) != ast.dump(expected(filename), include_attributes=False): + raise ValueError('Undeclared selected proof change: ' + filename) + result[filename] = sha256(raw.encode('utf-8')).hexdigest() + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write-derived', action='store_true') + args = parser.parse_args() + if args.write_derived: + for filename in PAIRS: + (HERE / filename).write_text(ast.unparse(expected(filename)) + '\n', encoding='utf-8') + print('PASS_SELECTED_SOURCE_BINDING', check()) + + +if __name__ == '__main__': + main() diff --git a/research/selected-quadratic-replay/checks.py b/research/selected-quadratic-replay/checks.py new file mode 100644 index 0000000000..2d2b9d5f56 --- /dev/null +++ b/research/selected-quadratic-replay/checks.py @@ -0,0 +1,105 @@ +"""Check exact state conversion, complete cache keys and source-proof guards.""" +import importlib.util +from pathlib import Path +import sys + +import binding +import state_adapter as A + +ROOT = Path(__file__).resolve().parents[2] + + +def load(name, path): + spec = importlib.util.spec_from_file_location(name, ROOT / path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def rejects(action): + try: + action() + except (ValueError, AssertionError): + return + raise ValueError('Invalid state or proof was accepted') + + +def run(): + C = load('selected_literal_compiler', 'research/p104-native-channel/vendor/clifford_exact.py') + V = load('selected_literal_native', 'research/p104-native-channel/vendor/native_verify.py') + cases = entries = 0 + for n in range(1, 5): + gates = [('phase', j) for j in range(4)] + gates += [('X', q) for q in range(1 << n)] + gates += [('C', q, s) for q in range(1, 1 << n) for s in (-1, 1)] + gates += [('P', tuple(1 << ((i + shift) % n) for i in range(n))) for shift in range(n)] + for mask in range(1 << n): + rows = tuple((1 << i) if mask >> i & 1 else 0 for i in range(n)) + gates.append(('D', rows, tuple((mask >> i) & 1 for i in range(n)))) + for j in range(len(gates)): + circuit = tuple(gates[k % len(gates)] for k in (j, 3 * j + 1, 7 * j + 2)) + operator = C.Op(n, V.tableau(circuit, n), list(circuit)) + for initial in range(1 << n): + expected = operator.zero_state(initial) + need(A.dense_state(n, circuit, initial) == expected, 'Literal dense amplitude or denominator') + cases += 1 + entries += 1 << n + for initial in (0, 1, 17, 511): + circuit = (('C', 511, 1), ('C', 17, -1), ('phase', 3), ('X', 39)) + need(A.sparse_state(circuit, initial) == V.state(circuit, initial), 'Literal sparse state') + cases += 1 + entries += 512 + + A.signature.cache_clear() + circuit = [['C', 1, 1]] + first = A.dense_state(2, circuit) + need(A.signature.cache_info().misses == 1, 'Cold cache') + need(A.dense_state(2, circuit) == first and A.signature.cache_info().hits == 1, 'Exact key reuse') + circuit.append(['phase', 1]) + need(A.dense_state(2, circuit) != first and A.signature.cache_info().misses == 2, 'Changed gate invalidates') + need(A.dense_state(2, circuit, 2) != A.dense_state(2, circuit, 0), 'Changed initial basis invalidates') + need(len(A.dense_state(3, circuit)[0]) == 8, 'Changed width invalidates') + # Numeric aliases must fail even after their integer counterpart is cached. + A.dense_state(1, [('X', 1)], 0) + for n, gates, initial in ((True, [('X', 1)], 0), (1, [('X', True)], 0), + (1, [('X', 1)], False), (1, [('X', 1.0)], 0)): + rejects(lambda n=n, gates=gates, initial=initial: A.dense_state(n, gates, initial)) + matrix = [[1, 2]] + A.dense_state(2, [('P', matrix[0])]) + matrix[0][0] = 0 + rejects(lambda: A.dense_state(2, [('P', matrix[0])])) + dense, _ = A.dense_state(2, [('C', 1, 1)]) + dense[0] = (99, 99) + need(A.dense_state(2, [('C', 1, 1)])[0][0] != (99, 99), 'Dense output cannot mutate cache') + sparse, _ = A.sparse_state((('phase', 0),)) + sparse.clear() + need(A.sparse_state((('phase', 0),))[0] == {0: (1, 0)}, 'Sparse output cannot mutate cache') + for phase in range(8200): + A.dense_state(0, [('phase', phase)]) + need(A.signature.cache_info().currsize == 8192, 'Bounded cache capacity') + misses = A.signature.cache_info().misses + A.dense_state(0, [('phase', 0)]) + need(A.signature.cache_info().misses == misses + 1, 'Evicted key is recomputed') + + native = (binding.HERE / 'native_fast.py').read_text() + rejects(lambda: binding.check({'native_fast.py': native.replace( + 'require(state(actual) == state(expected),', 'require(True,')})) + source = (binding.HERE / 'verify_source.py').read_text() + rejects(lambda: binding.check({'verify_source.py': source.replace( + 'costs = P.run(local, native, controller, physical)', 'costs = {}')})) + local = (binding.HERE / 'local_fast.py').read_text() + rejects(lambda: binding.check({'local_fast.py': local.replace( + "need(row == expected, 'All public and owned rows')", 'pass')})) + fast = load('selected_derived_compiler_check', 'research/selected-quadratic-replay/clifford_fast.py') + rejects(lambda: fast.ident(1).then(fast.ident(2))) + A.signature.cache_clear() + A.COUNTS.clear() + return {'literal_state_cases': cases, 'literal_amplitude_entries': entries, + 'cache_controls': 'Complete keys, type aliases, changed inputs, output mutation, capacity and eviction', + 'proof_controls': 3, 'explicit_assertion_control': 'Mismatched widths reject, including under -O'} diff --git a/research/selected-quadratic-replay/clifford_fast.py b/research/selected-quadratic-replay/clifford_fast.py new file mode 100644 index 0000000000..045034c843 --- /dev/null +++ b/research/selected-quadratic-replay/clifford_fast.py @@ -0,0 +1,249 @@ +"""Small exact Gaussian-dyadic Clifford compiler, independent of gx internals. +Paulis use i^p X^x Z^z. State vectors use integer Gaussian numerators / 2^d. +The tableau is supplemented by a literal circuit, so global phases are kept. +""" +from state_adapter import dense_state +from dataclasses import dataclass + +def parity(x): + return x.bit_count() & 1 + +def rank(rows): + p = {} + for x in rows: + while x: + b = x.bit_length() - 1 + if b not in p: + p[b] = x + break + x ^= p[b] + return len(p) + +def transpose(rows, n): + return tuple((sum(((rows[j] >> i & 1) << j for j in range(n))) for i in range(n))) + +def mv(rows, x): + return sum((parity(r & x) << i for i, r in enumerate(rows))) + +def inv(rows, n): + a = [r | 1 << n + i for i, r in enumerate(rows)] + for j in range(n): + k = next((i for i in range(j, n) if a[i] >> j & 1)) + a[j], a[k] = (a[k], a[j]) + for i in range(n): + if i != j and a[i] >> j & 1: + a[i] ^= a[j] + if not [r & (1 << n) - 1 for r in a] == [1 << i for i in range(n)]: + raise AssertionError() + return tuple((r >> n for r in a)) + +def basis_extend(cols, n): + out = [] + for x in list(cols) + [1 << i for i in range(n)]: + if rank(out + [x]) > len(out): + out.append(x) + if not len(out) == n: + raise AssertionError() + return tuple(out) + +def nullspace(rows, n): + a = list(rows) + p = [] + k = 0 + for j in range(n): + t = next((i for i in range(k, len(a)) if a[i] >> j & 1), None) + if t is None: + continue + a[t], a[k] = (a[k], a[t]) + for i in range(len(a)): + if i != k and a[i] >> j & 1: + a[i] ^= a[k] + p.append(j) + k += 1 + return tuple((1 << j | sum(((a[i] >> j & 1) << v for i, v in enumerate(p))) for j in range(n) if j not in p)) + +def pmul(a, b): + x, z, p = a + y, w, q = b + return (x ^ y, z ^ w, (p + q + 2 * parity(z & y)) % 4) + +def identity(n): + return tuple([(1 << i, 0, 0) for i in range(n)] + [(0, 1 << i, 0) for i in range(n)]) + +def apply(T, p): + n = len(T) // 2 + x, z, ph = p + out = (0, 0, ph) + for i in range(n): + if x >> i & 1: + out = pmul(out, T[i]) + for i in range(n): + if z >> i & 1: + out = pmul(out, T[n + i]) + return out + +def compose(A, B): + return tuple((apply(A, p) for p in B)) + +def inverse(T): + n = len(T) // 2 + cols = [x | z << n for x, z, p in T] + rows = transpose(cols, 2 * n) + cols_inv = transpose(inv(rows, 2 * n), 2 * n) + out = [] + for j, w in enumerate(cols_inv): + x = w & (1 << n) - 1 + z = w >> n + u, v, p = apply(T, (x, z, 0)) + if not (u, v) == identity(n)[j][:2]: + raise AssertionError() + out.append((x, z, -p % 4)) + return tuple(out) + +def qvalue(Q, alpha, x, n): + return (sum((alpha[i] for i in range(n) if x >> i & 1)) + 2 * sum((parity(Q[i] >> i + 1 & x >> i + 1) for i in range(n) if x >> i & 1))) % 4 + +def mul_i(a, p): + x, y = a + p %= 4 + return [(x, y), (-y, x), (-x, -y), (y, -x)][p] + +@dataclass +class Op: + n: int + tab: tuple + circuit: list + + def then(self, b): + if not self.n == b.n: + raise AssertionError() + return Op(self.n, compose(b.tab, self.tab), self.circuit + b.circuit) + + def adjoint(self): + circ = [] + for e in reversed(self.circuit): + if e[0] == 'P': + circ.append(('P', inv(e[1], self.n))) + elif e[0] == 'D': + circ.append(('D', e[1], tuple((-x % 4 for x in e[2])))) + elif e[0] == 'C': + circ.append(('C', e[1], -e[2])) + elif e[0] == 'phase': + circ.append(('phase', -e[1] % 4)) + else: + circ.append(e) + return Op(self.n, inverse(self.tab), circ) + + def zero_state(self, basis=0): + return dense_state(self.n, self.circuit, basis) + +def ident(n): + return Op(n, identity(n), []) + +def perm(n, G): + cols = transpose(G, n) + gi = inv(G, n) + return Op(n, tuple([(a, 0, 0) for a in cols] + [(0, a, 0) for a in gi]), [('P', tuple(G))]) + +def diag(n, Q, alpha=None): + Q = tuple(Q) + if not transpose(Q, n) == Q: + raise AssertionError() + alpha = tuple(alpha) if alpha is not None else tuple((Q[i] >> i & 1 for i in range(n))) + if not all((alpha[i] % 2 == Q[i] >> i & 1 for i in range(n))): + raise AssertionError() + return Op(n, tuple([(1 << i, Q[i], alpha[i]) for i in range(n)] + [(0, 1 << i, 0) for i in range(n)]), [('D', Q, alpha)]) + +def cgate(n, q, sgn=1): + return Op(n, tuple([(1 << i, 0, 0) for i in range(n)] + [(q if q >> i & 1 else 0, 1 << i, 3 * sgn % 4 if q >> i & 1 else 0) for i in range(n)]), [('C', q, sgn)]) + +def xgate(n, b): + return Op(n, tuple([(1 << i, 0, 0) for i in range(n)] + [(0, 1 << i, 2 * (b >> i & 1)) for i in range(n)]), [('X', b)]) + +def fourier(n, axes=None): + out = ident(n) + for i in range(n) if axes is None else axes: + out = out.then(cgate(n, 1 << i)) + return out + +def hadamard(n, axes): + axes = list(axes) + Q = tuple((1 << i if i in axes else 0 for i in range(n))) + S = diag(n, Q) + return S.then(fourier(n, axes)).then(S) + +def canonical_frame(n, U): + r = len(U) + if r == 0: + return ident(n) + if r == n: + return fourier(n) + G = transpose(basis_extend(U, n), n) + gi = inv(G, n) + Q = tuple((1 << i ^ sum((parity(gi_i & gi_j) << j for j, gi_j in enumerate(transpose(gi, n)))) for i, gi_i in enumerate(transpose(gi, n)))) + K = perm(n, G).then(diag(n, Q)) + return K.adjoint().then(fourier(n, range(r))).then(K) + +def monomial(op): + n = op.n + T = op.tab + if not all((x == 0 and p % 2 == 0 for x, z, p in T[n:])): + raise AssertionError() + G = transpose([x for x, z, p in T[:n]], n) + b = mv(G, sum((p // 2 << i for i, (x, z, p) in enumerate(T[n:])))) + gt = transpose(G, n) + cols = [mv(gt, z) for x, z, p in T[:n]] + Q = transpose(cols, n) + alpha = [(p - 2 * parity(b & z)) % 4 for x, z, p in T[:n]] + out = diag(n, Q, alpha).then(perm(n, G)).then(xgate(n, b)) + if not out.tab == T: + raise AssertionError() + vec, den = op.zero_state() + if not (den == 0 and all((a == (0, 0) for i, a in enumerate(vec) if i != b))): + raise AssertionError() + phase = [(1, 0), (0, 1), (-1, 0), (0, -1)].index(vec[b]) + out = out.then(Op(n, identity(n), [('phase', phase)])) + if not out.zero_state() == op.zero_state(): + raise AssertionError() + return (out, dict(matrix_rows=G, offset=b, quadratic_rows=Q, linear_Z4=alpha, phase=phase)) + +def lower_child(op): + n = op.n + Bcols = [x for x, z, p in op.tab[n:]] + r = rank(Bcols) + if not r: + mon, rec = monomial(op) + return (dict(rank=0, left=rec, right=None), mon) + G = transpose(basis_extend(Bcols, n), n) + A = inv(G, n) + PA = perm(n, A) + part = op.then(PA) + Bcols = [x for x, z, p in part.tab[n:]] + Dcols = [z for x, z, p in part.tab[n:]] + picks = [] + selected = [] + for j, x in enumerate(Bcols): + if rank(selected + [x]) > len(selected): + picks.append(j) + selected.append(x) + if not (len(picks) == r and all((x >> r == 0 for x in Bcols))): + raise AssertionError() + Br = transpose(selected, r) + Bi = inv(Br, r) + Dr = transpose([Dcols[j] & (1 << r) - 1 for j in picks], r) + Qsmall = tuple((sum((parity(row & col) << j for j, col in enumerate(transpose(Bi, r)))) for row in Dr)) + Q = Qsmall + (0,) * (n - r) + DQ = diag(n, Q) + V = part.then(DQ).then(hadamard(n, range(r))) + if not all((x == 0 for x, z, p in V.tab[n:])): + raise AssertionError() + Vmon, Vrec = monomial(V) + S = diag(n, tuple((1 << i if i < r else 0 for i in range(n)))) + left = S.adjoint().then(DQ.adjoint()).then(PA.adjoint()) + right = Vmon.then(S.adjoint()).then(xgate(n, (1 << r) - 1)) + lmon, lrec = monomial(left) + rmon, rrec = monomial(right) + compiled = rmon.then(fourier(n, range(r))).then(lmon) + if not (compiled.tab == op.tab and compiled.zero_state() == op.zero_state()): + raise AssertionError() + return (dict(rank=r, left=lrec, right=rrec), compiled) diff --git a/research/selected-quadratic-replay/cross.py b/research/selected-quadratic-replay/cross.py new file mode 100644 index 0000000000..bb28d8c39e --- /dev/null +++ b/research/selected-quadratic-replay/cross.py @@ -0,0 +1,51 @@ +"""Compare every actual state input with both retained literal interpreters.""" +import argparse +from hashlib import sha256 +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +from pins import authenticate + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--record', action='store_true') + args = parser.parse_args() + authenticate() + import binding + import checks + import state_adapter as A + import verify_source + binding.check() + A.TRACE = set() + verify_source.main([]) + trace = sorted(A.TRACE) + A.TRACE = None + calls = dict(A.COUNTS) + C = checks.load('selected_cross_literal_compiler', 'research/p104-native-channel/vendor/clifford_exact.py') + V = checks.load('selected_cross_literal_native', 'research/p104-native-channel/vendor/native_verify.py') + entries = 0 + for n, circuit, initial in trace: + checks.need(n == 9, 'Actual selected native width') + literal = C.Op(n, V.tableau(circuit, n), list(circuit)).zero_state(initial) + checks.need(A.dense_state(n, circuit, initial) == literal, 'Actual dense amplitude and denominator') + expected = ({i: pair for i, pair in enumerate(literal[0]) if pair != (0, 0)}, literal[1]) + checks.need(A.sparse_state(circuit, initial) == expected == V.state(circuit, initial), + 'Actual sparse amplitudes and both literal denominators') + entries += 1 << n + result = {'actual_state_calls': calls, 'distinct_inputs': len(trace), + 'amplitudes_per_literal_interpreter': entries, 'literal_interpreters': 2, + 'input_trace_sha256': sha256(json.dumps(trace, separators=(',', ':')).encode()).hexdigest()} + path = HERE / 'CROSS.json' + if args.record: + path.write_text(json.dumps(result, sort_keys=True, indent=2) + '\n', encoding='utf-8') + elif result != json.loads(path.read_bytes()): + raise ValueError('Actual selected state coverage changed') + print('PASS_ALL_SELECTED_LITERAL_STATES', json.dumps(result, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/selected-quadratic-replay/local_fast.py b/research/selected-quadratic-replay/local_fast.py new file mode 100644 index 0000000000..30322e24f1 --- /dev/null +++ b/research/selected-quadratic-replay/local_fast.py @@ -0,0 +1,202 @@ +"""Check the complete P104 word with an independent helper inventory. + +Adapted from Ali Romman's PR5544/5545. David Arias supplied the word; +Cinna Davis supplied private reuse; Gareth Davidson supplied composition. +Prepared by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as Q +from functools import lru_cache +from hashlib import sha256 +from pathlib import Path +import gzip +import importlib.util +import json +import sys +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +HERE = ROOT / 'research/p104-helper-subspace-splits' + +def need(ok, why): + if not ok: + raise ValueError(why) + +def read(path): + raw = path.read_bytes() + return json.loads(gzip.decompress(raw) if path.suffix == '.gz' else raw) + +def load(path, name): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + +def add(dst, src, q): + for k, v in tuple(src.items()): + value = dst.get(k, 0) + q * v + if value: + dst[k] = value + else: + dst.pop(k, None) + +def span(basis): + out = {0} + for v in basis: + need(type(v) is int and 0 < v < 512 and (v not in out), 'Independent binary basis') + out |= {x ^ v for x in tuple(out)} + return frozenset(out) + +def replay(w): + public = w['public'] + need(type(public) is int and 735 <= public <= 750, 'Public inventory bound') + need(len(w['initial']) == len(w['final']) == public, 'Public boundary size') + need(len(w['program']) < 26000, 'Fixed operation bound') + frames = [span(x) for x in w['frames']] + rows = [{r: Q(1)} for r in range(public + 8)] + current = list(w['initial']) + [None] * 8 + paid, scalar, live_owned, peak = (Counter(), 0, set(), 0) + lifetimes = 0 + for e in w['program']: + op, r = e[:2] + need(0 <= r < public + 8, 'Role index') + if op == 'MOVE': + _, r, a, b, private = e + need(current[r] == a and (r in live_owned) == private, 'Transport source and ownership') + need(frames[b] < frames[a] if private else frames[a] < frames[b], 'Nested chronological transport') + paid[abs(len(w['frames'][b]) - len(w['frames'][a]))] += 1 + current[r] = b + elif op == 'INIT': + need(r >= public and r not in live_owned, 'Owned initialization') + live_owned.add(r) + lifetimes += 1 + peak = max(peak, len(live_owned)) + rows[r] = {} + current[r] = e[2] + scalar += 2 + elif op == 'CLEAR': + need(r in live_owned and current[r] == e[2], 'Owned erasure at declared frame') + rows[r] = {} + current[r] = None + live_owned.remove(r) + scalar += 2 + else: + q, f = (Q(e[-2]), e[-1]) + need(q and current[r] == f, 'Scalar destination and coefficient') + n, d = (abs(q.numerator), q.denominator) + need(d & d - 1 == 0, 'Dyadic scalar coefficient') + need(abs(q) + 1 < 2 ** 16, 'Fixed scalar growth bound') + if op == 'SCALE': + need(n & n - 1 == 0, 'Dyadic unit SCALE') + rows[r] = {k: q * x for k, x in rows[r].items()} + scalar += 2 * (abs(n.bit_length() - d.bit_length()) + int(q < 0)) + else: + s = e[2] + need(s != r and 0 <= s < public + 8 and (current[s] == f), 'Common scalar chart') + if op == 'COPY': + need(r in live_owned and (not rows[r]), 'COPY into cleared owned field') + rows[r] = {k: q * x for k, x in rows[s].items()} + else: + need(op == 'ADD', 'Scalar opcode') + add(rows[r], rows[s], q) + scalar += 2 * (3 + n.bit_length() - 1 + n.bit_count() + d.bit_length() - 1) + need(not live_owned and peak == 1 and (current[:public] == w['final']), 'All public and owned exits') + live = set(w['live']) + for r, row in enumerate(rows): + expected = {r: Q(1)} if r < public else {} + if r - 112 in live: + expected[r - 112] = Q(1) + need(row == expected, 'All public and owned rows') + main = live | {r + 112 for r in live} + helpers = Counter((len(w['frames'][w['final'][r]]) - len(w['frames'][w['initial'][r]]) for r in range(public) if r not in main)) + need(len(live) == len(w['ports']) == 104 and len(main) == 208 and (min(helpers) > 0), 'Independent productive inputs') + return {'paid': dict(paid), 'helpers': dict(helpers), 'public_inputs': public, 'owned_lifetimes': lifetimes, 'peak_owned_fields': peak, 'real_scalar_allowance': scalar, 'endpoint_coefficients': (public + 8) * (public + 8), 'paid_rank_mass': sum((r * count for r, count in paid.items()))} + +def reverse_columns(w): + """Check the transpose with dense dyadic rows and the reverse chronology.""" + public = w['public'] + n = public + 8 + rows = [[int(i == j) for j in range(n)] for i in range(n)] + exponents = [0] * n + for e in reversed(w['program']): + op, r = e[:2] + if op == 'MOVE': + continue + if op in ('INIT', 'CLEAR'): + rows[r] = [0] * n + exponents[r] = 0 + continue + q = Q(e[-2]) + qe = q.denominator.bit_length() - 1 + if op == 'SCALE': + rows[r] = [q.numerator * x for x in rows[r]] + exponents[r] += qe + else: + s = e[2] + level = max(exponents[s], exponents[r] + qe) + a, b = (1 << level - exponents[s], q.numerator << level - exponents[r] - qe) + rows[s] = [a * x + b * y for x, y in zip(rows[s], rows[r])] + exponents[s] = level + if op == 'COPY': + rows[r] = [0] * n + exponents[r] = 0 + r = s + while exponents[r] and (not any((x & 1 for x in rows[r]))): + rows[r] = [x // 2 for x in rows[r]] + exponents[r] -= 1 + for r, row in enumerate(rows): + expected = [0] * n + if r < public: + expected[r] = 1 << exponents[r] + if r in w['live']: + expected[r + 112] = 1 << exponents[r] + need(row == expected, 'Independent dense transpose columns') + return {'columns': n, 'coefficients': n * n, 'arithmetic': 'Dense integer rows with binary denominators; reverse chronology'} + +def native(w): + n = w['public'] + C = load(ROOT / 'research/selected-quadratic-replay/clifford_fast.py', 'p104_productive_clifford') + V = load(ROOT / 'research/selected-quadratic-replay/native_fast.py', 'p104_productive_gaussian') + + @lru_cache(None) + def chart(i): + return C.canonical_frame(9, tuple(w['frames'][i])) + recipes = {} + + def check(a, b): + if (a, b) not in recipes: + recipe, _ = C.lower_child(chart(a).adjoint().then(chart(b))) + expected = V.adjoint(V.frame(w['frames'][a], 9)) + V.frame(w['frames'][b], 9) + V.equal(V.recipe(recipe), expected, 'Native chart change and exact global phase') + need(recipe['rank'] == abs(len(w['frames'][a]) - len(w['frames'][b])), 'Native boundary rank') + recipes[a, b] = recipe + return recipes[a, b] + for e in w['program']: + if e[0] == 'MOVE': + check(e[2], e[3]) + main = set(w['live']) | {r + 112 for r in w['live']} + helper_profile = Counter() + for r in range(n): + if r not in main: + helper_profile[check(w['initial'][r], w['final'][r])['rank']] += 1 + adapters = [] + for r, q in zip(w['live'], w['ports']): + need(w['frames'][w['initial'][r]] == [q], 'Literal central port') + need(span(w['frames'][w['final'][r + 112]]) == frozenset((x for x in range(512) if not (x & q).bit_count() % 2)), 'Literal output hyperplane') + tests = [(C.cgate(9, q, 1).adjoint().then(chart(w['initial'][r])), V.adjoint((('C', q, 1),)) + V.frame(w['frames'][w['initial'][r]], 9)), (chart(w['final'][r + 112]).adjoint().then(C.cgate(9, q, -1).then(C.fourier(9))), V.adjoint(V.frame(w['frames'][w['final'][r + 112]], 9)) + (('C', q, -1),) + V.fourier(9))] + for actual, expected in tests: + recipe, _ = C.lower_child(actual) + need(recipe['rank'] == 0, 'Free intrinsic main adapter') + V.equal(V.recipe(recipe), expected, 'Main endpoint phase') + adapters.append(recipe) + bad = json.loads(json.dumps(next(iter(recipes.values())))) + bad['left']['phase'] = (bad['left']['phase'] + 1) % 4 + a, b = next(iter(recipes)) + try: + V.equal(V.recipe(bad), V.adjoint(V.frame(w['frames'][a], 9)) + V.frame(w['frames'][b], 9), 'Wrong phase control') + except ValueError: + pass + else: + raise ValueError('Wrong native phase accepted') + payload = [[a, b, recipes[a, b]] for a, b in sorted(recipes)] + adapters + return {'distinct_maps': len(recipes), 'main_adapters': len(adapters), 'helper_normalizers': 2 * sum(helper_profile.values()), 'helpers': dict(helper_profile), 'recipe_payload_sha256': sha256(json.dumps(payload, sort_keys=True, separators=(',', ':')).encode()).hexdigest(), 'wrong_phase_rejected': True, 'proof': 'Every signed Pauli image and exact global phase; frame induction at every positive tensor width'} diff --git a/research/selected-quadratic-replay/native_fast.py b/research/selected-quadratic-replay/native_fast.py new file mode 100644 index 0000000000..b2a5289c47 --- /dev/null +++ b/research/selected-quadratic-replay/native_fast.py @@ -0,0 +1,206 @@ +"""Check native operators with exact Gaussian dyadic arithmetic. + +The interpreter is adapted from the independent campaign native review. +It does not import the source-code producer or the Clifford compiler. +Research used OpenAI Codex under the user's direction. +""" +from state_adapter import sparse_state +from functools import lru_cache + +def require(condition, label): + if not condition: + raise ValueError(label) + +def parity(value): + return value.bit_count() % 2 + +def mul(matrix, vector): + return sum((parity(row & vector) << i for i, row in enumerate(matrix))) + +def transpose(matrix): + return tuple((sum(((row >> j & 1) << i for i, row in enumerate(matrix))) for j in range(len(matrix)))) + +def inverse(matrix): + n = len(matrix) + rows = [row | 1 << n + i for i, row in enumerate(matrix)] + for j in range(n): + pivot = next((i for i in range(j, n) if rows[i] >> j & 1), None) + require(pivot is not None, 'singular binary chart') + rows[j], rows[pivot] = (rows[pivot], rows[j]) + for i in range(n): + if i != j and rows[i] >> j & 1: + rows[i] ^= rows[j] + require([row & (1 << n) - 1 for row in rows] == [1 << i for i in range(n)], 'binary inverse') + return tuple((row >> n for row in rows)) + +def extend(vectors, n): + columns, pivots = ([], {}) + for value in tuple(vectors) + tuple((1 << i for i in range(n))): + reduced = value + while reduced: + j = reduced.bit_length() - 1 + if j not in pivots: + pivots[j] = reduced + columns.append(value) + break + reduced ^= pivots[j] + require(len(columns) == n, 'frame basis extension') + return tuple(columns) + +def adjoint(circuit): + out = [] + for gate in reversed(circuit): + if gate[0] == 'P': + out.append(('P', inverse(gate[1]))) + elif gate[0] == 'D': + out.append(('D', gate[1], tuple((-a % 4 for a in gate[2])))) + elif gate[0] == 'C': + out.append(('C', gate[1], -gate[2])) + elif gate[0] == 'phase': + out.append(('phase', -gate[1] % 4)) + else: + require(gate[0] == 'X', 'adjoint gate type') + out.append(gate) + return tuple(out) + +def fourier(rank): + return tuple((('C', 1 << i, 1) for i in range(rank))) + +def frame(vectors, n): + rank = len(vectors) + if rank == 0: + return () + if rank == n: + return fourier(n) + matrix = transpose(extend(vectors, n)) + columns = transpose(inverse(matrix)) + quadratic = tuple((1 << i ^ sum((parity(a & b) << j for j, b in enumerate(columns))) for i, a in enumerate(columns))) + diagonal = tuple((row >> i & 1 for i, row in enumerate(quadratic))) + chart = (('P', matrix), ('D', quadratic, diagonal)) + return adjoint(chart) + fourier(rank) + chart + +def monomial(record): + matrix = tuple(record['matrix_rows']) + quadratic = tuple(record['quadratic_rows']) + linear = tuple(record['linear_Z4']) + require(transpose(quadratic) == quadratic, 'quadratic symmetry') + require(len(matrix) == len(quadratic) == len(linear) == 9, 'monomial dimension') + require(all((a % 2 == quadratic[i] >> i & 1 for i, a in enumerate(linear))), 'diagonal parity') + inverse(matrix) + return (('D', quadratic, linear), ('P', matrix), ('X', record['offset']), ('phase', record['phase'])) + +def recipe(record): + rank = record['rank'] + require(isinstance(rank, int) and 0 <= rank <= 9, 'child rank') + if rank == 0: + require(record['right'] is None, 'rank zero right factor') + return monomial(record['left']) + return monomial(record['right']) + fourier(rank) + monomial(record['left']) + +def tableau(circuit, n=9): + rows = [(1 << i, 0, 0) for i in range(n)] + [(0, 1 << i, 0) for i in range(n)] + for gate in circuit: + tag = gate[0] + out = [] + inverse_transpose = transpose(inverse(gate[1])) if tag == 'P' else None + for x, z, phase in rows: + if tag == 'P': + x, z = (mul(gate[1], x), mul(inverse_transpose, z)) + elif tag == 'X': + phase += 2 * parity(z & gate[1]) + elif tag == 'C': + if parity(z & gate[1]): + x ^= gate[1] + phase += 3 * gate[2] + elif tag == 'D': + quadratic, linear = gate[1:] + phase += sum((linear[i] for i in range(n) if x >> i & 1)) + phase += 2 * sum((parity(quadratic[i] >> i + 1 & x >> i + 1) for i in range(n) if x >> i & 1)) + z ^= mul(quadratic, x) + else: + require(tag == 'phase', 'tableau gate type') + out.append((x, z, phase % 4)) + rows = out + return tuple(rows) + +@lru_cache(maxsize=512) +def action(gate): + if gate[0] == 'P': + return tuple((mul(gate[1], x) for x in range(512))) + require(gate[0] == 'D', 'state action type') + quadratic, linear = gate[1:] + return tuple(((sum((linear[i] for i in range(9) if x >> i & 1)) + 2 * sum((parity(quadratic[i] >> i + 1 & x >> i + 1) for i in range(9) if x >> i & 1))) % 4 for x in range(512))) + +def rotate(pair, power): + a, b = pair + return ((a, b), (-b, a), (-a, -b), (b, -a))[power % 4] + +def state(circuit, basis=0): + return sparse_state(circuit, basis) + +def equal(actual, expected, label): + require(tableau(actual) == tableau(expected), label + ': signed Pauli action') + require(state(actual) == state(expected), label + ': exact global phase') + +def verify(data, certificate): + word = data['word'] + original, clean = (data['programs'], data['clean_programs']) + source_recipes = data['recipes'] + residuals = data['residuals']['recipes'] + native_tags = {'climb', 'adapter', 'residual_adapter'} + for orientation in ('forward', 'backward'): + native = [event for event in clean[orientation] if event[0] in native_tags] + require(native == [event for event in original[orientation] if event[0] in native_tags], 'A retained native event changed') + require(len(native) == 5056, 'The retained native event count changed') + frames = [frame(tuple(vectors), 9) for vectors in word['frames']] + used = {(event[3], event[4]) for program in clean.values() for event in program if event[0] == 'climb'} + children = {(record['old'], record['new']): record for record in source_recipes['children']} + require(len(children) == len(source_recipes['children']) and used <= set(children), 'The retained child recipe coverage is incomplete') + for old, new in sorted(used): + record = children[old, new] + require(record['rank'] == len(word['frames'][new]) - len(word['frames'][old]), 'A retained child has the wrong rank') + equal(recipe(record), adjoint(frames[old]) + frames[new], 'Retained child') + endpoints = {(record['role'], record['port']): record for record in source_recipes['endpoint_adapters']} + require(len(endpoints) == len(source_recipes['endpoint_adapters']) and set(endpoints) == {(role, p) for role in ('source', 'target') for p in range(112)}, 'The endpoint adapter coverage is incomplete') + for (role, port), record in endpoints.items(): + direction = word['ports'][port] + conventional = (('C', direction, 1),) if role == 'source' else (('C', direction, -1),) + fourier(9) + index = word['start'][port] if role == 'source' else word['final'][112 + port] + require(record['frame'] == index and record['rank'] == 0, 'An endpoint frame changed') + equal(recipe(record), adjoint(conventional) + frames[index], 'Endpoint adapter') + used_residuals = set() + for program in clean.values(): + for event in program: + if event[0] != 'residual_adapter': + continue + _, position, register, entry, *tail = event + terminal = tail[0] if tail else 1 + key = str(entry) if terminal == 1 else str(entry) + ':' + str(terminal) + require(key in residuals and position in ('pre', 'post'), 'A residual binding changed') + require(entry == word['start'][register] and terminal == word['final'][register], 'A residual endpoint changed') + used_residuals.add(key) + for key in sorted(used_residuals): + record = residuals[key] + equal(recipe(record), adjoint(frames[record['frame']]) + frames[record.get('terminal', 1)], 'Residual adapter') + records = certificate['input_recipes'] + ports = certificate['compensation_ports'] + require([record['port'] for record in records] == ports and len(records) == 8, 'The eight input recipes changed') + columns = 0 + for item in records: + port, label = (item['port'], item['label']) + require(label == word['ports'][port] and item['canonical_start_frame_id'] == word['start'][port], 'An input recipe has the wrong supplier label') + record = item['recipe'] + require(record['rank'] == 1, 'An input copy has the wrong child rank') + for side in ('left', 'right'): + factor = record[side] + require(factor['quadratic_rows'] == [0] * 9 and factor['linear_Z4'] == [0] * 9 and (factor['offset'] == factor['phase'] == 0), 'An input factor is not an address permutation') + actual, expected = (recipe(record), (('C', label, 1),)) + equal(actual, expected, 'Positive inherited input line') + for basis in range(512): + require(state(actual, basis) == state(expected, basis), 'A complete input Gaussian column differs') + columns += 1 + negative = monomial(record['right']) + (('C', 1, -1),) + monomial(record['left']) + require(tableau(negative) != tableau(expected) or state(negative) != state(expected), 'An inverse input child was not detected') + phased = actual + (('phase', 1),) + require(tableau(phased) == tableau(actual) and state(phased) != state(expected), 'An input phase-only error was not detected') + return {'status': 'PASS_EXACT_INPUT_NATIVE_FRAMES', 'retained_native_events_per_orientation': 5056, 'retained_child_recipes': len(used), 'endpoint_adapter_recipes': len(endpoints), 'residual_adapter_recipes': len(used_residuals), 'new_input_recipes': len(records), 'new_exact_gaussian_columns': columns, 'inverse_input_child_controls': len(records), 'phase_only_controls': len(records), 'address_permutation_factors': 2 * len(records), 'method': 'Independent signed Pauli and exact Gaussian interpretation; no compiler import', 'scope': 'Positive inherited input frames before every retained adapter. No recursive hosting claim.'} diff --git a/research/selected-quadratic-replay/pins.py b/research/selected-quadratic-replay/pins.py new file mode 100644 index 0000000000..9acb0df4f9 --- /dev/null +++ b/research/selected-quadratic-replay/pins.py @@ -0,0 +1,21 @@ +"""Authenticate every retained input before the selected replay imports it.""" +from hashlib import sha1, sha256 +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def authenticate(): + count = 0 + for row in json.loads((HERE / 'SOURCES.json').read_bytes())['files']: + if row['usage'] != 'input': + continue + raw = (ROOT / row['path']).read_bytes() + if sha256(raw).hexdigest() != row['sha256']: + raise ValueError('Selected adapter source hash: ' + row['path']) + if sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() != row['git_blob']: + raise ValueError('Selected adapter source blob: ' + row['path']) + count += 1 + return count diff --git a/research/selected-quadratic-replay/run.py b/research/selected-quadratic-replay/run.py new file mode 100644 index 0000000000..1f1aa047dd --- /dev/null +++ b/research/selected-quadratic-replay/run.py @@ -0,0 +1,21 @@ +"""Run the complete selected scientific check with explicit state adapters.""" +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import binding +from pins import authenticate +import verify_source + + +def main(): + if sys.argv[1:]: + raise ValueError('No arguments are accepted') + authenticate() + binding.check() + verify_source.main([]) + + +if __name__ == '__main__': + main() diff --git a/research/selected-quadratic-replay/state_adapter.py b/research/selected-quadratic-replay/state_adapter.py new file mode 100644 index 0000000000..5268a977c1 --- /dev/null +++ b/research/selected-quadratic-replay/state_adapter.py @@ -0,0 +1,62 @@ +"""Return the retained dense and sparse state formats from exact quadratic data. + +The engine and its stabilizer proof are from Ali Romman's PR5704. +This selected-caller adapter is by Ali Romman with OpenAI Codex assistance. +Apache-2.0. The bounded process cache uses every exact state input as its key. +""" +from collections import Counter +from functools import lru_cache +from pathlib import Path +import runpy + +ROOT = Path(__file__).resolve().parents[2] +ENGINE = runpy.run_path(str(ROOT / 'research/exact-clifford-quadratic-replay/quadratic.py')) +COUNTS = Counter() +TRACE = None + + +def frozen(value): + """Copy supported values into an immutable key; reject numeric aliases.""" + if type(value) in (int, str): + return value + if type(value) in (tuple, list): + return tuple(frozen(item) for item in value) + raise ValueError('State input must contain only exact integers, strings and sequences') + + +@lru_cache(maxsize=8192) +def signature(n, circuit, initial): + return ENGINE['signature'](n, circuit, initial) + + +def support(n, circuit, initial): + key = frozen(n), frozen(circuit), frozen(initial) + state = signature(*key) + if TRACE is not None: + TRACE.add(key) + _, offset, columns, terms, real, imag, denominator = state + polynomial = dict(terms) + values = {} + for mask in range(1 << len(columns)): + address = offset + for j in ENGINE['bits'](mask): + address ^= columns[j] + values[address] = ENGINE['multiply_i']((real, imag), ENGINE['value'](polynomial, mask)) + COUNTS['evaluations'] += 1 + COUNTS['amplitude_entries'] += 1 << n + return values, denominator + + +def dense_state(n, circuit, initial=0): + values, denominator = support(n, circuit, initial) + result = [(0, 0)] * (1 << n) + for address, pair in values.items(): + result[address] = pair + COUNTS['dense'] += 1 + return result, denominator + + +def sparse_state(circuit, initial=0): + result = support(9, circuit, initial) + COUNTS['sparse'] += 1 + return result diff --git a/research/selected-quadratic-replay/verify.py b/research/selected-quadratic-replay/verify.py new file mode 100644 index 0000000000..d9c760591c --- /dev/null +++ b/research/selected-quadratic-replay/verify.py @@ -0,0 +1,39 @@ +"""Check source binding, state conversion and the complete selected result.""" +import argparse +from hashlib import sha256 +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +from pins import authenticate + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--record', action='store_true') + args = parser.parse_args() + inputs = authenticate() + import binding + import checks + import state_adapter as A + import verify_source + bound = binding.check() + controls = checks.run() + verify_source.main([]) + source = HERE.parents[1] / binding.SOURCE + result = {'source_inputs': inputs, 'derived_files': bound, 'controls': controls, + 'source_scientific_sha256': sha256((source / 'RESULT.json').read_bytes()).hexdigest(), + 'source_word_sha256': sha256((source / 'WORD.json.gz').read_bytes()).hexdigest(), + 'state_evaluations': dict(A.COUNTS), 'cache': A.signature.cache_info()._asdict()} + path = HERE / 'RESULT.json' + if args.record: + path.write_text(json.dumps(result, sort_keys=True, indent=2) + '\n', encoding='utf-8') + elif result != json.loads(path.read_bytes()): + raise ValueError('Selected quadratic replay receipt changed') + print('PASS_COMPLETE_SELECTED_QUADRATIC_REPLAY') + + +if __name__ == '__main__': + main() diff --git a/research/selected-quadratic-replay/verify_source.py b/research/selected-quadratic-replay/verify_source.py new file mode 100644 index 0000000000..22c95b346b --- /dev/null +++ b/research/selected-quadratic-replay/verify_source.py @@ -0,0 +1,128 @@ +"""Verify independent helper splits, all native maps and complete kappa. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from collections import Counter +from copy import deepcopy +from hashlib import sha1, sha256 +import gzip +import json +from pathlib import Path +import sys +import tempfile +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +HERE = ROOT / 'research/p104-helper-subspace-splits' + +def need(ok, why): + if not ok: + raise ValueError(why) + +def authenticate(): + count = 0 + manifest = json.loads((HERE / 'SOURCES.json').read_bytes()) + for row in manifest['files']: + if row['usage'] == 'input': + raw = (ROOT / row['path']).read_bytes() + need(sha256(raw).hexdigest() == row['sha256'], 'Source SHA256: ' + row['path']) + need(sha1(b'blob ' + str(len(raw)).encode() + b'\x00' + raw).hexdigest() == row['git_blob'], 'Source Git blob: ' + row['path']) + count += 1 + for row in manifest['external_inputs']: + retained_path = (HERE.relative_to(ROOT) / row['local_path']).as_posix() + retained, = [r for r in manifest['files'] if r['path'] == retained_path] + need(retained['usage'] == 'input', 'Copied source is a declared live input') + need((retained['sha256'], retained['git_blob']) == (row['sha256'], row['git_blob']), 'Retained bytes equal the recorded published source') + return count + +def rejected(action): + try: + action() + except ValueError as error: + return str(error) + raise ValueError('An invalid claim was accepted') + +def run(): + pins = authenticate() + sys.path.insert(0, str(HERE)) + sys.path.insert(0, str(Path(__file__).resolve().parent)) + import local_fast as L + import construct as R + import pricing as P + C = L.load(ROOT / 'research/p104-productive-controller/caller.py', 'subspace_p104_caller') + predecessor = L.replay(L.read(HERE / 'inputs/PR5580-WORD.json.gz')) + source = L.read(HERE / 'inputs/PR5565-WORD.json.gz') + witnesses = L.read(HERE / 'SPLITS.json') + need(len(witnesses) == 13, 'Thirteen explicit independent splits') + baseline = L.replay(source) + source_delta = {} + for name, expected in (('paid', {1: -8, 3: -1, 4: -2, 5: 4}), ('helpers', {8: -1, 9: 1})): + delta = Counter(baseline[name]) + delta.subtract(predecessor[name]) + source_delta[name] = {r: n for r, n in delta.items() if n} + need(source_delta[name] == expected, 'Exact published PR5565 ' + name + ' change') + word, cuts = R.construct(source, witnesses) + local = L.replay(word) + need((local['public_inputs'], local['owned_lifetimes'], local['peak_owned_fields']) == (748, 8, 1), 'Complete public and owned inventory') + need(local['helpers'] == {1: 2, 2: 5, 4: 89, 5: 11, 7: 5, 8: 16, 9: 412}, 'Exact helper histogram') + delta = Counter(local['helpers']) + delta.subtract(baseline['helpers']) + delta = {r: n for r, n in delta.items() if n} + need(delta == {1: 2, 2: 5, 4: 6, 5: 6, 7: 5, 8: 2, 9: -13}, 'All split credits and removed targets') + need(local['paid'] == baseline['paid'], 'Same complete local paid histogram') + columns = L.reverse_columns(word) + print('PASS 13 prefix/suffix cuts, every independent row and dense reverse columns', flush=True) + native = L.native(word) + controller = C.construct() + need(controller == L.read(ROOT / 'research/p104-productive-controller/CONTROLLER.json'), 'Same complete caller') + physical = C.physical(controller, word) + print('PASS every native phase, productive target and physical caller contact', flush=True) + costs = P.run(local, native, controller, physical) + controls = C.controls(controller) + bad = deepcopy(witnesses[0]) + key = next(iter(bad['a'])) + bad['a'][key] = str(L.Q(bad['a'][key]) + 1) + controls['contaminated_prefix'] = rejected(lambda: R.check_cut(source, bad)) + bad = deepcopy(witnesses[0]) + key = next(iter(bad['b'])) + bad['b'][key] = str(L.Q(bad['b'][key]) + 1) + controls['contaminated_suffix'] = rejected(lambda: R.check_cut(source, bad)) + bad = deepcopy(word) + bad['program'].pop(0) + controls['missing_input_basis'] = rejected(lambda: L.replay(bad)) + bad = deepcopy(word) + bad['program'].pop() + controls['missing_output_basis'] = rejected(lambda: L.replay(bad)) + bad = deepcopy(word) + bad['final'][648] = 127 + controls['unearned_whole_target'] = rejected(lambda: L.replay(bad)) + bad = deepcopy(local) + bad['helpers'][1] += 1 + controls['extra_helper_credit'] = rejected(lambda: P.assemble(bad, native, controller, physical)) + bad = deepcopy(local) + bad['paid'][1] -= 1 + controls['unpaid_gaussian'] = rejected(lambda: P.assemble(bad, native, controller, physical)) + result = {'status': 'PASS_P104_HELPER_SUBSPACE_KAPPA_00310045', 'authenticated_inputs': pins, 'splits': cuts, 'local_helper_delta': delta, 'published_source_delta': source_delta, 'local': local, 'separate_columns': columns, 'native': native, 'physical_caller': physical, 'complete_cost': costs, 'negative_controls': controls, 'limits': ['The five selected framework assumptions and helper-endpoint contract remain.', 'No complete rounded multiplier or enormous uniform compiler word is materialized.', 'No independent human or proof-kernel acceptance or global optimality is claimed.']} + return (P.encode(result), word) + +def main(argv=None): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true') + args = parser.parse_args(argv) + need(not args.write, 'Derived replay cannot write source artifacts') + with tempfile.TemporaryDirectory(prefix='p104-subspace-bytecode-') as cache: + sys.pycache_prefix = cache + result, word = run() + for name, value in (('RESULT.json', result), ('WORD.json.gz', word)): + path = HERE / name + if args.write: + raw = (json.dumps(value, sort_keys=True, indent=None if name.endswith('.gz') else 2) + '\n').encode() + path.write_bytes(gzip.compress(raw, mtime=0) if name.endswith('.gz') else raw) + else: + raw = path.read_bytes() + need(json.loads(gzip.decompress(raw) if name.endswith('.gz') else raw) == value, 'Exact saved artifact: ' + name) + print(result['status']) + print(json.dumps({k: result['complete_cost'][k] for k in ('kappa', 'gain', 'raw_root_interval', 'productive_fields', 'paid_calls')}, sort_keys=True)) +if __name__ == '__main__': + main()