diff --git a/research/wordram-assertion-portability/PROOF.md b/research/wordram-assertion-portability/PROOF.md new file mode 100644 index 0000000000..b32fca2c39 --- /dev/null +++ b/research/wordram-assertion-portability/PROOF.md @@ -0,0 +1,122 @@ +# Preservation of the fixed bounded-kernel checklist + +The claim is a scoped implementation-preservation proof. It concerns the exact +source closure in SOURCES.json, CPython 3.12, and the normal and `-O` commands +in VERIFY.json. It supplies no new arithmetic theorem or independent scientific +acceptance of the predecessor. + +## Assertion lowering + +For each parsed statement `assert test, message`, replace just that statement by + +```python +if not test: + raise _imb_certificate_assertion_error(message) +``` + +Omit the constructor argument when the assertion has no message. The injected +name denotes the built-in AssertionError class. The parser rejects source that +already contains the reserved name, so source code cannot capture the injected +binding. The fixed sources contain no operation that mutates that binding. + +The replacement evaluates the predicate once and tests its truth value in the +same position. A true predicate skips the message. A false predicate evaluates +the message once, then raises the same exception class with the same arguments. +An exception from evaluating either expression propagates in the same way. +In particular, no-message and explicit-None-message assertions stay distinct. +Surrounding loops, handlers, functions and statement order are unchanged. +Ordinary Python assertion execution therefore agrees with this replacement. +The compiler retains an explicit conditional raise under `-O`. + +The transformation iterates over the parsed tree and replaces statement-list +members of type Assert. It rejects a result containing any remaining Assert. +The receipt records each source line and column, including multiple assertions +on a line. The authenticated closure contains exactly 55 sites. No assertion +is removed without its explicit replacement. + +## Entry and import boundary + +The original entry point has one capability guard that rejects optimized +Python before any scientific work. The adapter recognizes its exact syntax +and error message and replaces its condition by False. It requires exactly +one `__debug__` reference in that entry and none in imported source modules. +This removes only that refusal. All nine entry-point certificate assertions +receive the transformation above. + +Before execution, read and authenticate every original package file against +both the publication source pins and the original MANIFEST.json. The closure +has 33 files, including that manifest. The original entry's own inventory, +hash and retained-result checks still execute. Frozen bytes remain unchanged. + +Every imported source module uses a loader that compiles its authenticated +bytes directly after assertion lowering. The loader does not read bytecode +caches. A clean-interpreter guard rejects preloaded source modules. The final +module-inventory check requires every Python source except the separate NTT +test module, which the unchanged subprocess checklist executes. The NTT +implementation and test module have no bare assertions; their unittest checks +remain method calls under optimization. + +The entry's single NTT subprocess is intercepted at its explicit run boundary. +The wrapper checks the exact original argument list, working directory and +check=True contract. It propagates the requested optimization level, removes +inherited optimization/path overrides, supplies a fresh bytecode-cache prefix, +adds a 180-second limit and requires the complete eight-test success report. +It runs the same unittest discovery domain. No test is filtered or replaced. +Unexpected commands fail. Nonzero exit, timeout or an incomplete report fails. + +## Complete preservation check + +Each invocation first runs the original normal entry point with a fresh +bytecode-cache prefix. It then runs the adapted entry at the invoking +interpreter's optimization level. Compare the entire parsed output object +after removing just the `seconds` clock field. This includes all reported +check counts and the full instruction histogram. The original whole-program +result comparison also remains active inside the adapted entry. + +Normal and optimized executions perform the same complete checklist. Finite +evidence compares eight assertion-evaluation fixtures at compiler levels +0, 1 and 2. Those 24 comparisons include lazy messages, side effects, +missing versus explicit None messages, loop failure, nested functions and +exception handlers. Five boundary controls reject changed source bytes, +oversized input, a reserved binding, an unexpected guard and a missing guard. +Four additional controls introduce wrong results into actual loaded components +and require their retained assertions to fail. They exercise the RAM residue, +circuit, complete-program digit and fixed-point recovery paths. They do not +claim that every assertion has a separately falsifying fixture. + +All controls finish with the original module bindings restored. Finally, +reauthenticate the complete original source closure. A generated stdout receipt +binds the new package files and therefore the source manifest by SHA256. + +## Limits and implementation constraints + +The equivalence argument concerns the fixed code, its executed checklist and +ordinary assertion effects. Traceback formatting, debugger/coverage line events, +code-object identity, frame introspection, AST layout and timing are outside +the claim. It is not a general Python source transformer or an execution +sandbox. The AST guard and import inventory deliberately reject changed sources. +Only full normal and `-O` source replays are registered; level 2 has synthetic +assertion-semantic coverage, not a claimed complete source replay. + +New functions are below 60 physical lines. Inputs are limited to 64 source +rows, one MiB per source and 30,000 AST nodes at depth at most 64. The original +fixed numerical domains and interpreter budgets stay unchanged. Subprocesses +have 180-second limits and each registered invocation has a 240-second limit. +There are no new retries or background jobs. The CLI accepts only an existing +scratch-directory path. Temporary cache directories are scoped and removed; +import hooks, search paths and newly imported source modules are restored on +success or failure. + +Power of Ten deviations are explicit. Python allocates managed ASTs, integers, +fractions and containers. The source whitelist and finite bounds constrain +these live objects; no fixed-allocation or allocator-internals claim is made. +The AST compiler and import protocol are required metaprogramming here. Their +inputs are hash-bound, transformation sites are enumerated, and execution +targets are the fixed module closure. Standard AST location/compiler routines +use bounded library recursion after the depth check. The retained predecessor +circuit evaluator has its existing fixed small-tree recursion; frozen source +is not rewritten beyond the stated assertion transformation. This adapter +does not expand its circuit domain. Callback dispatch is limited to the import +loader, one checked subprocess boundary and four local fault controls. Warning- +strict normal and optimized replays supply interpreter diagnostics. No external +static analyzer or proof kernel was run. diff --git a/research/wordram-assertion-portability/README.md b/research/wordram-assertion-portability/README.md new file mode 100644 index 0000000000..286aa89609 --- /dev/null +++ b/research/wordram-assertion-portability/README.md @@ -0,0 +1,98 @@ +# Preserve bounded-kernel certificate checks under optimized Python + +This contribution was produced by Nick Petalas. New work is Apache-2.0. + +The unchanged PR5466 bounded Word RAM entry point rejects `-O` because its +certificate checks use Python assertions. This opt-in, source-bound adapter +executes its complete checklist under `-O` with all 55 assertion sites retained +as explicit failure branches. Frozen source files and their credit are unchanged. + +Claim type: scoped implementation-preservation proof with finite conformance +evidence. The adapter's complete scientific output equals the original normal +entry point's output after removing its clock field. This is a portability +improvement. It supplies no new arithmetic result, storage improvement, runtime +speedup, supplier admission, kappa or independent predecessor audit. + +[PROOF.md](PROOF.md) explains predicate/message evaluation, the exact entry-guard +change, the import boundary and the full checklist comparison. The new adapter +compiles authenticated source bytes in memory; it never rewrites the predecessor. +Every imported source module bypasses stale bytecode. The separate NTT child +runs its unchanged eight-test discovery domain with the same optimization level +and a fresh bytecode-cache prefix. + +## Evidence and reproduction + +From the repository root, with standard-library CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/wordram-assertion-portability/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/wordram-assertion-portability/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/wordram-assertion-portability +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/wordram-assertion-portability --check-source-history +``` + +Use another CPython 3.12 path elsewhere. `--scratch PATH` puts temporary cache +directories in an existing external directory. The commands emit generated +JSON receipts on stdout and write no package files. Expected markers include +`PASS_WORDRAM_ASSERTION_PORTABILITY`, `PASS_REGISTERED_RESEARCH_PACKAGE` and +`PASS_RESEARCH_COMMIT_BYTES`. The publication command requires committed bytes +and full Git history. + +Each invocation compares against a fresh original normal execution. The retained +checklist covers all eight NTT unittest groups, 65,537 modular-multiply inputs, +5,096 butterfly fixtures, 2,197 circuit fixtures, 277 complete-program cases and +20 approximate-backend pairs at each of two precisions. These are predecessor +coverage domains, preserved here rather than claimed as new mathematical results. + +New checks compare eight assertion-evaluation fixtures at compiler levels 0, 1 +and 2, giving 24 semantic comparisons. Nine controls reject five boundary faults +and wrong RAM, circuit, whole-program and FFT results. The receipt enumerates +every adapted assertion site. A site inventory is not a claim that each site +has a separate falsifying fixture. + +## Scope and sources + +Card `portable-replay`, priority revision 8, is refined to this exact optimized- +interpreter refusal. Base `7c49fe32c55de02c2c873655c804b16e4c3fef0a` contains the +entire 33-file original package closure. [SOURCES.json](SOURCES.json) pins every +file; [VERIFY.json](VERIFY.json) declares every live input. No pending Git object, +network service or predecessor installation is needed. The direct command also +works in a Git-free export containing these declared inputs. + +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19361778). +Live claims, local reservations, open/account/merged PR searches and distinctive +main README searches were checked. The card overlap snapshot covered 380 open +PRs and 6,300 Discussion records with complete remote pagination; its sparse +local scan omitted 8,797 note paths. Main-tree term searches supplemented that +scan. Unpublished work and arbitrary historical diffs remain coverage limits. +PR5886 concerns address liveness and reduced RAM storage, a separate result. + +The scientific statement remains the predecessor's informal theorem and bounded +executable evidence. No selected cold replay, native/compiler/physical replay, +Lean build, Docker run or independent human/proof-kernel review is claimed. +The selected frontier and five framework assumptions remain unchanged. Full +source replays cover normal Python and `-O`; `-OO` has synthetic semantic checks +only. Native Windows execution is unrun. See the proof's explicit restrictions +on introspection, tracebacks, dynamic allocation and controlled metaprogramming. + +## Open next questions + +Can every retained assertion site receive an explicit falsifying fixture without +changing the scientific domain? Start with a site-visit trace and distinguish +unreached contracts from repeated predicates. The present inventory and four +component faults do not establish that stronger coverage. + +Does the same complete command pass on native Windows CPython 3.12? Start from +the committed Git-free export and retain subprocess return codes, output and +file hashes. No platform-specific success follows from the source-preservation +argument alone. + +## Credit + +David Ganz / Dugongue supplied PR5466's bounded kernel, exact NTT, interpreted +Word RAM programs, circuit checks, approximate recovery and complete checklist. +The original tcslib, FastPoly, CatCrypt, mpfx, arithmetic and multiplication +lineages retain all credit in the unchanged NOTICE.txt and source notices. +Python assertion semantics, AST lowering and fresh-cache execution are standard +techniques. The contribution here is their restricted, source-bound adapter and +its preservation checks. Predecessor scientific claims are cited premises. diff --git a/research/wordram-assertion-portability/SOURCES.json b/research/wordram-assertion-portability/SOURCES.json new file mode 100644 index 0000000000..dcef7d03ca --- /dev/null +++ b/research/wordram-assertion-portability/SOURCES.json @@ -0,0 +1,216 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/wordram-ntt-kernel/INTEGRATION-RESULTS.json", + "usage": "input", + "git_blob": "f8df94a147514b0ccf3575e6f0e3654d8da3efe1", + "sha256": "fd866e701664a240059bdb3212898fa97fd5f5a1759e2fb84c37f07947e69d40" + }, + { + "path": "research/wordram-ntt-kernel/LICENSE", + "usage": "input", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "path": "research/wordram-ntt-kernel/MANIFEST.json", + "usage": "input", + "git_blob": "529ff29e326bb27833ea20fee1bde4e477dbca8e", + "sha256": "ab4f000927b8cfe91358f40a6282ec1e65cc1ffe8e6604408192a112ae906afc" + }, + { + "path": "research/wordram-ntt-kernel/NOTICE.txt", + "usage": "input", + "git_blob": "b0dc94cb9d5ed24d2ebddc2eae0f41792a2abe69", + "sha256": "c7a35a43ceeca4d0b820c00e5b3c589d119033748a46de91769f284e869ac33b" + }, + { + "path": "research/wordram-ntt-kernel/PROOF.txt", + "usage": "input", + "git_blob": "d0d0d6486e833fb4711fcdd22a5aaa1853815189", + "sha256": "f1d6549b55337e6704b575806fb6be6cec8bbc9a761a6bf3a320aec40cbee9df" + }, + { + "path": "research/wordram-ntt-kernel/README.md", + "usage": "input", + "git_blob": "8c24538d69695a816a19b9d2910c4cfb13e5afb1", + "sha256": "903f3fd84a09de855dec2a000f4eedab16037c93648d5e8d275475a66c7a9322" + }, + { + "path": "research/wordram-ntt-kernel/SOURCES.json", + "usage": "input", + "git_blob": "a9831371ac8ce67fbdc347ff4ae4f62dbb5aa1f8", + "sha256": "3610732a3a0accd3766c92b1de904ed7a41c05970942e0fe5eb89fa697b26f7d" + }, + { + "path": "research/wordram-ntt-kernel/STANDALONE-VERIFY.json", + "usage": "input", + "git_blob": "3e43a2b044a0e98b9b7ea1634a6dde575f828a14", + "sha256": "e6320251311dc9a6850284a974cb6ddd1dadbcdc45cfeba0787a77c15351c184" + }, + { + "path": "research/wordram-ntt-kernel/TASK.json", + "usage": "input", + "git_blob": "c1d552b810bd575a380f09d5455fc6ce3bc74afd", + "sha256": "33d03eb9b15b920ae29387a91212fcd67d3a95be81723670a5177b3b56fe612e" + }, + { + "path": "research/wordram-ntt-kernel/lean/IntegerKernelRecovery20261024.lean", + "usage": "input", + "git_blob": "1eac839250ca83e0cc73c7548b230dd28be777cc", + "sha256": "1cfed8b805c3236ae205d5774badd79118e5743fa9343ee70313083efc308e9a" + }, + { + "path": "research/wordram-ntt-kernel/lean/STATUS.json", + "usage": "input", + "git_blob": "c8490e586eb2c13bed6bf41c6ff569f2fc94bead", + "sha256": "1b66f49217a082e44d56e97f7ce8e6edc9f3199ffec23cb6b168e9bd26672361" + }, + { + "path": "research/wordram-ntt-kernel/ntt/CATCRYPT-LICENSE.txt", + "usage": "input", + "git_blob": "b724ce4a1cf87f73d4c8d318a087e0180dbc5c19", + "sha256": "1ae0577444a82462c225f35a8cbd770e449ef4507e58f8638e5f121b6238712a" + }, + { + "path": "research/wordram-ntt-kernel/ntt/MANIFEST.json", + "usage": "input", + "git_blob": "6e80e0fca8a33acdbb0a1fe1d5b5fcf2a64bc636", + "sha256": "2cb299d5166af9ea5a849e23af64f92f137a1ae0da5fd85ae83581dce67a9a61" + }, + { + "path": "research/wordram-ntt-kernel/ntt/NTT-APPLICATION.txt", + "usage": "input", + "git_blob": "68a7dd7fb5000d1b8987e7ec52127370d9619935", + "sha256": "09ed4367c0808d786c6a9ca9e552bc4592da1da16b66ffa60812c6a2dd65753a" + }, + { + "path": "research/wordram-ntt-kernel/ntt/TEST-RESULT.json", + "usage": "input", + "git_blob": "1771314511534d67f5602ea8f6c32c6206fd6e53", + "sha256": "16e4463688fd7b08a8056e842e78baeb24091a11136ac2899984d2cd938f6a92" + }, + { + "path": "research/wordram-ntt-kernel/ntt/exact_ntt.py", + "usage": "input", + "git_blob": "5982128975472dfeb472dbe848c5d3617076662b", + "sha256": "b512200d63c736c5d347247028eb1b1f3431cea44aba01c86f2772910d6b41bf" + }, + { + "path": "research/wordram-ntt-kernel/ntt/sources.json", + "usage": "input", + "git_blob": "7c8a205220b453ee815dbf3f109ab454d110a936", + "sha256": "b7ddef8bb58bdcf2c6a5029826291c83dc7492e2b06cbfb66cf0828e7ad017e4" + }, + { + "path": "research/wordram-ntt-kernel/ntt/test_exact_ntt.py", + "usage": "input", + "git_blob": "20e78e7805e5310556799204030bd53c2087deb8", + "sha256": "e2fcd058685ab49f2cec71f806563888452ee5dce6b696e04b0ef0ea84687123" + }, + { + "path": "research/wordram-ntt-kernel/ram/PROOFS.txt", + "usage": "input", + "git_blob": "21907aa9c4aa4c135a49ff5652bbfa08e722b757", + "sha256": "e62d76c0caaa4e24651d2282a7a19cb935c63e16932c90a14cb74182d3934df8" + }, + { + "path": "research/wordram-ntt-kernel/ram/circuit-verification.json", + "usage": "input", + "git_blob": "106316349bc26dc40010eb742dc6881c32ffa5bd", + "sha256": "d7423872b05db58c6157930f9f89ffd5bf36e0059ed51a4a8739900a4ece5d7d" + }, + { + "path": "research/wordram-ntt-kernel/ram/circuit_sharing.py", + "usage": "input", + "git_blob": "21ee1529a5450571f624481c987afae4b53362ed", + "sha256": "0eadf9ef954c5d97aa5e5f0949b6bf90ecb90fbb9d0321f472b2c6e97140c24f" + }, + { + "path": "research/wordram-ntt-kernel/ram/sources.json", + "usage": "input", + "git_blob": "73b132f8473c65c6ec45b7261c71c7e72ef31b8c", + "sha256": "329ce129c36e78d93710104864a94eb0ed1918733e78fd2fcde96ab7f5b58929" + }, + { + "path": "research/wordram-ntt-kernel/ram/verification.json", + "usage": "input", + "git_blob": "d761d6cd06addfed05e1c79a92b21e92eecc4ea7", + "sha256": "8d3efbc0916af425143ae6bd5bd94bb9d70ac72d1de2b920a3b2d4bcc9e3b46b" + }, + { + "path": "research/wordram-ntt-kernel/ram/verify_wordram.py", + "usage": "input", + "git_blob": "d55923ac7686d492256c620f4c127c5d362dbea4", + "sha256": "02b2c09ff1542e6f947aedaad67c9a1872ed0098a447b71076cfbfe14373efbb" + }, + { + "path": "research/wordram-ntt-kernel/ram/wordram_kernel.py", + "usage": "input", + "git_blob": "f5c6e00699db701f02c23c0d776f6db9d8a28854", + "sha256": "b1a6133e505e5faf5832a5274eea23f96b033257c3d16cc24479c4a4c7059a2e" + }, + { + "path": "research/wordram-ntt-kernel/ram_multiplier.py", + "usage": "input", + "git_blob": "09ca74343b741af876043059d0cd0d1db8b393ed", + "sha256": "6c3ae23ad90c92741f5a505ae9dd85a4bbaaafb72ebdf50291e07d1ae4c52476" + }, + { + "path": "research/wordram-ntt-kernel/recovery/REPORT.txt", + "usage": "input", + "git_blob": "ed6d5042a0a9fd84c7b8966977bef44c2de8f358", + "sha256": "eff4e3bdabdf0216604493e2d768cbe9862e40c61cba21c8964d6fc339b85138" + }, + { + "path": "research/wordram-ntt-kernel/recovery/SOURCES.json", + "usage": "input", + "git_blob": "dffae1f418b123558626d67dab9dffbf14ffc506", + "sha256": "3f29acd9aee095197f2b0829774d40ba930e1977fe9ab1a5f7efb4b2935a07c3" + }, + { + "path": "research/wordram-ntt-kernel/recovery/fixedpoint_fft.py", + "usage": "input", + "git_blob": "7ae4b7016ff1ba232e15d741d25d5efe2410e67b", + "sha256": "e9ffceb08684d73e9971b8be9451caefdd2836235eaf059356fc38dc43861bb6" + }, + { + "path": "research/wordram-ntt-kernel/recovery/verification-31bits.json", + "usage": "input", + "git_blob": "f06d2c8f1b91853179eaf3eebbd0b0d7d5943045", + "sha256": "8a56a5bbe68cee7540a39e03ee041ca4fc5a6aaaa2bf39b109002c05fa0adc6b" + }, + { + "path": "research/wordram-ntt-kernel/recovery/verification.json", + "usage": "input", + "git_blob": "3939d4bb3630187bfb9f1298efbd4d3ea0bdc24f", + "sha256": "3593b43218392896cbcccad591b3bfdf2fb65f1b8d1b60d1b28320ebb1134041" + }, + { + "path": "research/wordram-ntt-kernel/verify.py", + "usage": "input", + "git_blob": "6695bdfd46add80e2da99ea78544e7223d8c8d54", + "sha256": "84283f0581ed63f099a453be34e8d615d90a3ca5dd6f24cdc4a38d93710e594a" + }, + { + "path": "research/wordram-ntt-kernel/verify_integration.py", + "usage": "input", + "git_blob": "834cb84e8157170cd05401ab7719fda01da9be93", + "sha256": "ef0f3721a9db3f96985f11f446e7bb0bd9c8e20763344c30e4b39f57cbcaaea5" + } + ] +} diff --git a/research/wordram-assertion-portability/TASK.json b/research/wordram-assertion-portability/TASK.json new file mode 100644 index 0000000000..2eced8dc87 --- /dev/null +++ b/research/wordram-assertion-portability/TASK.json @@ -0,0 +1,81 @@ +{ + "schema_version": 1, + "task_id": "portable-replay", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "portable-replay", + "question": "Can one reproducible environment or artifact-comparison failure be repaired?", + "starting_points": [ + "research/gzip-container-reproducibility/README.md", + "docs/ci-verification.md" + ], + "methods": [ + "Reproduce one portability failure and add a minimal cross-environment fix.", + "Audit one canonical-payload comparison for omitted proof-relevant fields." + ], + "acceptance_gate": "Preserve immutable source hashes and proof-relevant content; a different compressed byte stream alone is not a mathematical mismatch.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Reproduce one specific mismatch or audit one canonical comparison for omitted proof-relevant fields.", + "bottleneck_link": "Portable exact checks prevent environment failures from blocking valid contributions.", + "allowed_variations": [ + "One interpreter/version mismatch or one payload field comparison." + ], + "scope_change_triggers": [ + "Removing immutable-source pins because generated compressed bytes differ." + ], + "overlap_terms": [ + "gzip container", + "reproducibility", + "canonical payload" + ] + }, + "scope_status": "refined", + "actual_scope": "Enable the complete fixed PR5466 checklist under optimized CPython through a hash-bound assertion-preserving source adapter.", + "scope_change_reason": "The card asks for one reproducible environment failure repair. The frozen bounded-kernel entry rejects -O because its certificate checks use assertions. This opt-in adapter changes that execution boundary while retaining the checklist; no mathematical audit or arithmetic/storage extension is the deliverable.", + "bottleneck_link": "Verifier portability side result. It preserves a bounded arithmetic kernel checklist across interpreter optimization; it does not discharge a selected framework assumption or improve the signed supplier moment.", + "budget_minutes": 60, + "stop_rule": "Stop at the first complete normal/optimized preservation pass and its fault controls. Do not extend the arithmetic, allocator, optimized modes or scientific domain.", + "outcome": "completed", + "evidence": "PROOF.md, adapter.py and verify.py; complete original-versus-adapted result comparison, 55 assertion sites, 24 semantic comparisons and nine rejections.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can every retained assertion site receive an explicit falsifying fixture?", + "why_it_matters": "A syntactic site inventory and four component faults do not establish per-site fault coverage.", + "first_step": "Record visits to each site without changing predicate/message evaluation, then classify unreached contracts.", + "blocked_by": "No such per-site fixture suite is supplied." + }, + { + "question": "Does the complete command pass on native Windows CPython 3.12?", + "why_it_matters": "The preservation proof does not establish subprocess/path portability on every operating system.", + "first_step": "Run the committed Git-free export once with both registered interpreter modes and retain return/output/file-hash evidence.", + "blocked_by": "No native Windows execution is available in this contribution." + } + ], + "coordination": { + "source_pr": 5466, + "source_author": "Dugongue", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19361778", + "claim_type": "scoped implementation-preservation proof with finite conformance", + "selected_record": "PR6030; kappa=781451/250000000; unchanged", + "source_policy": "All original files remain unchanged. PR5886 address-liveness allocation is separate context, not the question extended here." + }, + "environment": { + "implementation": "cpython", + "version": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]", + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "local_platform": "macOS arm64", + "dependencies": "standard library only" + } +} diff --git a/research/wordram-assertion-portability/VERIFY.json b/research/wordram-assertion-portability/VERIFY.json new file mode 100644 index 0000000000..c2f1a02779 --- /dev/null +++ b/research/wordram-assertion-portability/VERIFY.json @@ -0,0 +1,68 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/wordram-ntt-kernel/INTEGRATION-RESULTS.json", + "research/wordram-ntt-kernel/LICENSE", + "research/wordram-ntt-kernel/MANIFEST.json", + "research/wordram-ntt-kernel/NOTICE.txt", + "research/wordram-ntt-kernel/PROOF.txt", + "research/wordram-ntt-kernel/README.md", + "research/wordram-ntt-kernel/SOURCES.json", + "research/wordram-ntt-kernel/STANDALONE-VERIFY.json", + "research/wordram-ntt-kernel/TASK.json", + "research/wordram-ntt-kernel/lean/IntegerKernelRecovery20261024.lean", + "research/wordram-ntt-kernel/lean/STATUS.json", + "research/wordram-ntt-kernel/ntt/CATCRYPT-LICENSE.txt", + "research/wordram-ntt-kernel/ntt/MANIFEST.json", + "research/wordram-ntt-kernel/ntt/NTT-APPLICATION.txt", + "research/wordram-ntt-kernel/ntt/TEST-RESULT.json", + "research/wordram-ntt-kernel/ntt/exact_ntt.py", + "research/wordram-ntt-kernel/ntt/sources.json", + "research/wordram-ntt-kernel/ntt/test_exact_ntt.py", + "research/wordram-ntt-kernel/ram/PROOFS.txt", + "research/wordram-ntt-kernel/ram/circuit-verification.json", + "research/wordram-ntt-kernel/ram/circuit_sharing.py", + "research/wordram-ntt-kernel/ram/sources.json", + "research/wordram-ntt-kernel/ram/verification.json", + "research/wordram-ntt-kernel/ram/verify_wordram.py", + "research/wordram-ntt-kernel/ram/wordram_kernel.py", + "research/wordram-ntt-kernel/ram_multiplier.py", + "research/wordram-ntt-kernel/recovery/REPORT.txt", + "research/wordram-ntt-kernel/recovery/SOURCES.json", + "research/wordram-ntt-kernel/recovery/fixedpoint_fft.py", + "research/wordram-ntt-kernel/recovery/verification-31bits.json", + "research/wordram-ntt-kernel/recovery/verification.json", + "research/wordram-ntt-kernel/verify.py", + "research/wordram-ntt-kernel/verify_integration.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Complete normal source-preservation replay, 55 assertion sites, 24 semantic comparisons and nine controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Complete optimized source-preservation replay with the same assertion inventory and controls." + } + ] +} diff --git a/research/wordram-assertion-portability/adapter.py b/research/wordram-assertion-portability/adapter.py new file mode 100644 index 0000000000..8deb6f20cc --- /dev/null +++ b/research/wordram-assertion-portability/adapter.py @@ -0,0 +1,214 @@ +"""Assertion-preserving execution of one authenticated bounded-kernel package.""" +import ast +import contextlib +import hashlib +import importlib.abc +import importlib.machinery +import importlib.util +import io +import json +import os +from pathlib import Path +import subprocess +import sys +import tempfile +import types + +HERE = Path(__file__).resolve().parent +SOURCE = HERE.parent / "wordram-ntt-kernel" +PREFIX = "research/wordram-ntt-kernel/" +ERROR_NAME = "_imb_certificate_assertion_error" +MAX_BYTES, MAX_NODES, MAX_DEPTH = 1_048_576, 30_000, 64 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def authenticate(raw, digest, label): + need(len(raw) <= MAX_BYTES, "source size: " + label) + need(hashlib.sha256(raw).hexdigest() == digest, "source hash: " + label) + return raw + + +def read_sources(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + rows = [row for row in manifest["files"] if row["usage"] == "input"] + need(1 <= len(rows) <= 64, "bounded source inventory") + files = {} + for row in rows: + path = row["path"] + need(path.startswith(PREFIX), "source package boundary") + name = path.removeprefix(PREFIX) + need(name not in files and ".." not in Path(name).parts, "source spelling") + with (SOURCE / name).open("rb") as stream: + raw = stream.read(MAX_BYTES + 1) + files[name] = authenticate(raw, row["sha256"], name) + need("MANIFEST.json" in files and "verify.py" in files, "source roots") + inventory = json.loads(files["MANIFEST.json"])["files"] + need(set(files) == set(inventory) | {"MANIFEST.json"}, "complete source closure") + for name, digest in inventory.items(): + authenticate(files[name], digest, name) + return files + + +def bounded_tree(raw, name): + need(len(raw) <= MAX_BYTES and ERROR_NAME.encode() not in raw, "source boundary") + tree = ast.parse(raw, filename=name) + pending, count = [(tree, 0)], 0 + for _ in range(MAX_NODES + 1): + if not pending: + return tree + node, depth = pending.pop() + count += 1 + need(count <= MAX_NODES and depth <= MAX_DEPTH, "AST capacity") + pending.extend((child, depth + 1) for child in ast.iter_child_nodes(node)) + raise ValueError("AST capacity") + + +def failure_branch(statement): + args = [] if statement.msg is None else [statement.msg] + error = ast.Call(ast.Name(ERROR_NAME, ast.Load()), args, []) + replacement = ast.If(ast.UnaryOp(ast.Not(), statement.test), + [ast.Raise(error, None)], []) + return ast.copy_location(replacement, statement) + + +def lower(raw, name, entry=False, optimize=None): + tree = bounded_tree(raw, name) + nodes = list(ast.walk(tree)) + assertions = [(node.lineno, node.col_offset) for node in nodes + if isinstance(node, ast.Assert)] + need(sum(isinstance(node, ast.Name) and node.id == "__debug__" for node in nodes) + == int(entry), "optimization guard inventory") + guards = 0 + for node in nodes: + if isinstance(node, ast.Name) and node.id == "__debug__": + need(entry, "unexpected optimization guard") + if isinstance(node, ast.If) and ast.dump(node.test) == ( + "UnaryOp(op=Not(), operand=Name(id='__debug__', ctx=Load()))"): + need(entry and len(node.body) == 1 and not node.orelse, "entry guard shape") + need(ast.unparse(node.body[0]) == "raise SystemExit(" + repr( + "Run without Python -O: certificate assertions must be enabled.") + ")", + "entry guard message") + node.test = ast.copy_location(ast.Constant(False), node.test) + guards += 1 + for field, value in ast.iter_fields(node): + if isinstance(value, list): + setattr(node, field, [failure_branch(child) if isinstance(child, ast.Assert) + else child for child in value]) + need(guards == int(entry), "entry guard count") + need(not any(isinstance(node, ast.Assert) for node in ast.walk(tree)), + "no optimizer-removable certificate checks") + ast.fix_missing_locations(tree) + level = sys.flags.optimize if optimize is None else optimize + return compile(tree, name, "exec", dont_inherit=True, optimize=level), assertions + + +class CheckedLoader(importlib.abc.Loader): + def __init__(self, finder, name): + self.finder, self.name = finder, name + + def create_module(self, spec): + return None # Use the standard module allocation. + + def exec_module(self, module): + code, checks = lower(self.finder.files[self.name], str(SOURCE / self.name)) + module.__dict__[ERROR_NAME] = AssertionError + exec(code, module.__dict__) + self.finder.loaded[self.name] = module + self.finder.checks[self.name] = checks + + +class CheckedFinder(importlib.abc.MetaPathFinder): + def __init__(self, files): + self.files, self.loaded, self.checks = files, {}, {} + + def find_spec(self, fullname, path=None, target=None): + spec = importlib.machinery.PathFinder.find_spec(fullname, path) + if spec is None or spec.origin is None: + return None + origin = Path(spec.origin).resolve() + if not origin.is_relative_to(SOURCE): + return None + name = origin.relative_to(SOURCE).as_posix() + need(name in self.files and name.endswith(".py"), "authenticated import") + loader = CheckedLoader(self, name) + return importlib.util.spec_from_file_location(fullname, origin, loader=loader) + + +def ntt_runner(records, scratch): + def run(argv, cwd, check): + expected = [sys.executable, "-B", "-m", "unittest", "discover", + "-s", "ntt", "-p", "test_*.py"] + need(argv == expected and Path(cwd) == SOURCE and check is True, "NTT child ABI") + env = dict(os.environ) + env.pop("PYTHONOPTIMIZE", None) + env.pop("PYTHONPATH", None) + with tempfile.TemporaryDirectory(prefix="ntt-bytecode-", dir=scratch) as cache: + flags = ["-O"] * sys.flags.optimize + command = argv[:1] + flags + ["-X", "pycache_prefix=" + cache] + argv[1:] + result = subprocess.run(command, cwd=cwd, check=True, env=env, + capture_output=True, text=True, timeout=180) + need("Ran 8 tests" in result.stderr and result.stderr.rstrip().endswith("OK"), + "complete NTT unittest checklist") + records.append({"tests": 8, "optimized": sys.flags.optimize, + "stdout": result.stdout}) + return result + return run + + +def replay(files, scratch): + finder, child_records = CheckedFinder(files), [] + code, checks = lower(files["verify.py"], str(SOURCE / "verify.py"), entry=True) + module = types.ModuleType("_imb_bounded_entry") + module.__file__ = str(SOURCE / "verify.py") + module.__dict__[ERROR_NAME] = AssertionError + old_path, old_modules = list(sys.path), set(sys.modules) + need(len(old_modules) <= 2048, "bounded clean interpreter") + for name in old_modules: + filename = getattr(sys.modules[name], "__file__", None) + need(not filename or not Path(filename).resolve().is_relative_to(SOURCE), + "source modules must not be preloaded") + sys.path.insert(0, str(SOURCE)) + sys.meta_path.insert(0, finder) + try: + exec(code, module.__dict__) + module.subprocess = types.SimpleNamespace(run=ntt_runner(child_records, scratch)) + output = io.StringIO() + with contextlib.redirect_stdout(output): + module.main() + result = json.loads(output.getvalue()) + need(len(child_records) == 1, "one complete NTT subprocess") + finder.checks["verify.py"] = checks + expected = {name for name in files if name.endswith(".py")} + expected.remove("ntt/test_exact_ntt.py") + need(set(finder.checks) == expected, "complete adapted module inventory") + need(sum(map(len, finder.checks.values())) == 55, "complete assertion inventory") + return result, finder, child_records + finally: + sys.path[:] = old_path + sys.meta_path.remove(finder) + for name in set(sys.modules) - old_modules: + loaded = sys.modules[name] + filename = getattr(loaded, "__file__", None) + if filename and Path(filename).resolve().is_relative_to(SOURCE): + del sys.modules[name] + + +def reference(scratch): + env = dict(os.environ) + env.pop("PYTHONOPTIMIZE", None) + env.pop("PYTHONPATH", None) + with tempfile.TemporaryDirectory(prefix="wordram-reference-", dir=scratch) as cache: + env["PYTHONPYCACHEPREFIX"] = cache + command = [sys.executable, "-B", "-X", "pycache_prefix=" + cache, + str(SOURCE / "verify.py")] + result = subprocess.run(command, cwd=SOURCE, env=env, capture_output=True, + text=True, check=True, timeout=180) + need("Ran 8 tests" in result.stderr and result.stderr.rstrip().endswith("OK"), + "reference NTT checklist") + output = json.loads(result.stdout) + output.pop("seconds") + return output diff --git a/research/wordram-assertion-portability/verify.py b/research/wordram-assertion-portability/verify.py new file mode 100644 index 0000000000..5da7334f37 --- /dev/null +++ b/research/wordram-assertion-portability/verify.py @@ -0,0 +1,132 @@ +"""Run the complete adapted entry and controls; emit a generated stdout receipt.""" +import argparse +import hashlib +import json +from pathlib import Path +import sys +import tempfile + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from adapter import (ERROR_NAME, HERE, MAX_BYTES, authenticate, bounded_tree, + lower, need, read_sources, reference, replay) + + +def rejected(function, arguments, exception, label): + try: + function(*arguments) + except exception: + return label + raise ValueError("control accepted: " + label) + + +def outcome(code): + environment = {ERROR_NAME: AssertionError} + try: + exec(code, environment) + failure = None + except AssertionError as error: + failure = repr(error.args) + return environment.get("events"), failure + + +def transformation_controls(): + samples = [ + "events=[]\nassert events.append('test') is None, events.append('message')", + "events=[]\nassert events.append('test'), events.append('message')", + "events=[]\nassert False", + "events=[]\nassert False, None", + "events=[]\nassert False, ('message', 2)", + "events=[]\nfor i in range(3):\n events.append(i)\n assert i < 2, i", + "events=[]\ndef f():\n assert False, 'inside function'\nf()", + "events=[]\ntry:\n assert False, 7\nexcept AssertionError as e:\n events.append(e.args)", + ] + compared = 0 + for sample in samples: + expected = outcome(compile(sample, "control", "exec", optimize=0)) + for level in range(3): + code, checks = lower(sample.encode(), "control", optimize=level) + need(len(checks) == 1 and outcome(code) == expected, + "assertion evaluation, message and exception preservation") + compared += 1 + controls = [ + rejected(bounded_tree, (b" " * (MAX_BYTES + 1), "large"), ValueError, "large source"), + rejected(bounded_tree, (ERROR_NAME.encode() + b"=1", "alias"), ValueError, "reserved alias"), + rejected(lower, (b"if not __debug__: pass", "guard"), ValueError, "foreign guard"), + rejected(lower, (b"x=1", "entry", True), ValueError, "missing entry guard"), + rejected(authenticate, (b"changed", "0" * 64, "mutant"), ValueError, "changed source bytes"), + ] + return compared, controls + + +def with_fault(module, name, replacement, call, label): + original = getattr(module, name) + setattr(module, name, replacement) + try: + return rejected(call, (), AssertionError, label) + finally: + setattr(module, name, original) + + +def semantic_controls(finder): + modules = finder.loaded + ram = modules["ram/verify_wordram.py"] + circuit = modules["ram/circuit_sharing.py"] + integration = modules["verify_integration.py"] + recovery = modules["recovery/fixedpoint_fft.py"] + original_run = ram.run + + def bad_ram(*args, **kwargs): + result = original_run(*args, **kwargs) + result.memory[3] ^= 1 + return result + + def bad_circuit(*args, **kwargs): + return (0,) + + original_execute = integration.execute + + def bad_execute(*args, **kwargs): + result, digits = original_execute(*args, **kwargs) + return result, [digits[0] ^ 1, *digits[1:]] + + controls = [with_fault(ram, "run", bad_ram, ram.run_checks, "wrong RAM residue"), + with_fault(circuit, "evaluate", bad_circuit, circuit.check, "wrong circuit value")] + calls = iter((True, False)) + + def one_bad_execute(*args, **kwargs): + if next(calls): + return bad_execute(*args, **kwargs) + return original_execute(*args, **kwargs) + + controls.append(with_fault(integration, "execute", one_bad_execute, + integration.verify, "wrong whole-program digits")) + controls.append(with_fault(recovery, "nearest", lambda value: 0, + lambda: recovery.run(4, 40, 0), "wrong FFT rounding")) + return controls + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--scratch", type=Path, default=Path(tempfile.gettempdir())) + args = parser.parse_args() + need(args.scratch.is_dir(), "scratch directory exists") + files = read_sources() + compared, controls = transformation_controls() + expected = reference(args.scratch) + result, finder, children = replay(files, args.scratch) + controls.extend(semantic_controls(finder)) + need(read_sources() == files, "source files remain unchanged") + result.pop("seconds") # This clock field is not scientific output. + need(result == expected, "complete scientific output equals original normal entry") + hashes = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(HERE.iterdir()) if p.is_file()} + receipt = {"status": "PASS_WORDRAM_ASSERTION_PORTABILITY", "python": sys.version, + "optimization": sys.flags.optimize, "assertion_semantics_cases": compared, + "rejection_controls": controls, "source_result": result, + "adapted_assertions": finder.checks, "NTT_children": children, + "package_sha256": hashes} + print(json.dumps(receipt, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()