Preserve 55 bounded-kernel assertions under optimized Python (no κ)

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.

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.