Refine the complete fixed CRT repair into literal binary control

research/crt-complete-binary-refinement/PROOF.md

@@ -0,0 +1,193 @@
+# Complete binary refinement of the fixed CRT repair program
+
+Prepared by JoyboyBrian with substantial OpenAI Codex assistance. Apache-2.0.
+
+## Statement and inherited hypotheses
+
+Let P be the exact 8,242-instruction program assembled by the pinned PR5105
+`machine.py` and `compiler.py`, with its 31 distinct tape roles. Assume the
+successful input contract in its pinned PROOF.md: unary geometry
+(G,H,K,Y,J,B)=(2,2,6,8,2,0); a framed, target-independent 32-bit ROM;
+4,096 opaque 12-bit record labels in the supplied raw post-S order; zero
+heads; and private blank tapes. We inherit its source-algorithm correctness,
+allocation and successful-domain theorem. We do not infer those from one run.
+
+The program emitted by `lower.py` operates through the unchanged PR4982
+`Machine` and `BitTape`: one-bit reads/writes, unit bit-head movement,
+one-bit Boolean gates, one-bit assignments, branches, jumps and halts.
+Neither a runtime decoded symbol nor a runtime host tape-role selection is
+an instruction. The instruction's tape name is always a literal fixed role.
+Program counters and emulated head coordinates are configuration machinery.
+
+The emitted program refines every source step on the stated successful
+domain and therefore returns the same ideal-T payload order. It preserves
+borrowed geometry/ROM, erases the same private roles, returns every physical
+head, and clears all 14,839 finite-control bits. It has 557,123 static
+instructions. If the source executes T instructions, including its halt,
+then the complete binary invocation costs at most
+
+    101391 T + 29679
+
+charged bit/control actions. This includes initialization and final control
+erasure. The source theorem's symbolic bound for T can be substituted
+without running the full binary layer. This is a fixed-program refinement,
+not a variable-geometry E(p,ell), a complete physical multiplier, or a
+claim that the full binary layer was executed.
+
+## Finite closure and encoding
+
+`closure` starts each source register at {None}; every tape contains blank,
+the six headers also contain `<`, `>`, `1`, ROM contains its markers/bits,
+and data contains `<`, `>` and all 4,096 records. It propagates possible
+values monotonically through **every** source instruction, including loop
+back edges implicitly by repeated saturation. Reads take the union of the
+possible named tapes; writes enlarge those tapes; copies and finite tuple
+expressions propagate their values; field projection propagates each
+defined tuple component; comparisons/record/not yield Boolean values;
+bit-string gates yield `0` or `1`. Branches and jumps produce no values.
+All constants and nested operand expressions are included in the codebook.
+Unsupported operations, large Cartesian products or exhausted code space
+fail compilation; they do not silently truncate the domain.
+
+The saturation terminates after four rounds for this exact P. By induction
+on executed steps, registers and tapes remain in the saturated domains.
+This is an overapproximation, including transient None alternatives that
+are not reachable at many instruction sites. In the successful source
+execution all tape operands are actual roles and all field operands are
+tuples of the appropriate length. The latter follows specifically from
+the producer's returned role products and the scanner's producer-owned
+stencil: after the END test, each token is an admitted five-field atom.
+We do not claim string indexing or malformed arbitrary source states are
+refined by the tuple-field blocks. Undefined/unadmitted dispatch and field
+values reject. This preserves the original successful-domain restriction.
+
+Python equality identifies False with 0 and True with 1, recursively in
+tuples. `canon` makes precisely that identification. The source uses no
+Boolean identity/type test; its only type-sensitive operation is `record`.
+Every reachable record is `('R', n)` with integer 0<=n<4096; canonicalization
+preserves this predicate, truthiness, equality, tuple construction and
+projection. Thus the canonical state is a sufficient source-state quotient.
+
+There are 4,932 canonical values. Blank `_` has code zero. Records have
+code 4096+n; all other values have distinct codes below 4096. Codes use
+13 little-endian bits. In particular record recognition is exactly the
+high code bit, and all 4,096 payload labels remain distinct. There is no
+record-pair lookup table. Unused bit patterns are outside the entry
+contract. Source cell j occupies positions 13j through 13j+12. At source
+instruction boundaries each physical head is at 13 times its source head.
+
+## Instruction simulation
+
+Each source register is a 13-bit finite-control word. Temporary control
+bits are reused between source instructions: names beginning `$` are
+disjoint from the actual source register namespace. No temporary is read
+before its block assigns it. At entry, explicit set instructions initialize
+source words to code(None) and scratch to zero. Both successful and
+rejecting exits share explicit all-zero control tails; rejecting exits
+have no data rollback promise.
+
+* **Constants, copies and products.** A constant writes its 13 code bits.
+  Copies preserve every bit, including when source and destination alias.
+  A finite product evaluates all component words before its decision chain.
+  For each statically enumerated tuple, conjunction of component equalities
+  selects its unique code; injectivity proves exactly one match for an
+  admitted operand. This includes nested role products and five-field
+  stencil atoms. Static enumeration is compilation, not execution.
+* **Equality, inequality, membership and truth.** XOR each pair of code
+  bits, OR the differences, then negate: this is equality of canonical
+  values. Inequality reverses the result. Membership ORs the finitely many
+  element comparisons. Truth excludes exactly the finitely encoded falsy
+  values (None and zero here). Boolean results are encoded as canonical
+  integer zero/one. Inputs are evaluated before an aliased destination is
+  overwritten.
+* **Field and record.** The field block compares the whole input code
+  against every admitted tuple alternative and emits the chosen component
+  code. Its defined branches therefore implement tuple projection. Record
+  uses the high bit, whose exactness follows from the entire code inventory.
+  This does not decode a payload integer into a runtime address.
+* **String-bit gates.** Compare each operand against the code of string
+  `1`; apply XOR/AND/OR to those Boolean flags; emit the code of string
+  `0` or `1`. This is the precise source semantics, including its treatment
+  of operands other than string `1`. It does not confuse integer one with
+  string `1`.
+* **Tape role dispatch.** A literal role chooses its fixed tape directly.
+  A role register is compared against its statically possible fixed roles;
+  each matching arm names a literal tape in every emitted instruction.
+  For this P each role register's valid role set is a singleton (None may
+  also occur in the overapproximation); the validation chain remains
+  explicit. No host lookup uses the runtime role word. Role selection
+  finishes before a read can overwrite an aliased operand register.
+* **Read/write/move.** A read or write visits the 13 consecutive bits and
+  then rewinds twelve positions to the cell start. It realizes exactly one
+  source symbol access without altering other cells. A source unit move
+  emits thirteen unit bit moves. Thus the head invariant is preserved,
+  including append/blank regions and arbitrary existing payload contents.
+* **Control.** Internal decision chains have forward edges only and leave
+  at the designated block end. Source branch/jump targets are relocated
+  to exact source-block starts, including backward loop edges. A source
+  halt goes to its shared erase tail and corresponding final halt.
+
+These cases cover all sixteen opcodes actually emitted by P. They also
+explain operand aliasing: every value needed for a result or role arm is
+read before a destructive result write. The verifier executes alias
+controls, but the cases above establish the quantified step relation.
+Induction through arbitrary repeated source loops composes the relation;
+finite tests are corroboration, not the induction argument.
+
+## Cost, storage and composition
+
+The exact generated source-block intervals have maximum length 101,391.
+Every internal edge goes forward; the only source back edges terminate a
+block at another source boundary. Therefore every simulated source step
+uses at most this many binary actions, regardless of the runtime branch.
+Initialization writes 14,839 control bits; the terminal tail writes them
+again and executes one halt. Consequently the bound is
+101391*T + 2*14839 + 1. The block maximum is deliberately conservative,
+dominated by overapproximated aggregate alternatives, not an optimization
+or observed maximum for a production input. Shared exit tails avoid
+replicating all control erasure at every rejecting source site.
+
+If the source's visited retained tape backing is B cells, its bit encoding
+uses 13B cells, plus 14,839 finite-control bits and the fixed program.
+Moving through a source cell's encoding visits only its own 13 bits;
+there is no hidden record gather or payload transpose. Private source
+blanks become actual zero bits; source marker disposal thus erases the
+entire corresponding codeword. All heads zero at source exit implies all
+physical heads zero. The ambient/private blank-storage grant is inherited;
+we do not establish initialization of arbitrary dirty exterior storage.
+
+Input serialization, fixed program construction, the ROM producer and raw-S
+production remain external prerequisites. Static compilation here takes no
+input payload, ROM contents or runtime address. It emits one fixed program
+for the specified source, not a program regenerated per payload.
+
+## Executed evidence and its limits
+
+`verify.py` authenticates every declared source before assembly. Its
+microchecks use the **original PR5105 executor** as the reference, including
+aliased destinations, all operator classes, typed equality, stencil fields,
+dynamic role selection, bit strides and complete exit-control cleanup.
+Three executable faults omit a bit stride, retain control, or route to the
+wrong physical tape. The code inventory covers all 4,096 record labels.
+
+Two longer comparisons run the complete fixed-program blocks on persistent
+encoded tape objects, checking each source boundary's changed register,
+write and head plus the complete endpoint. One executes the actual producer
+through its scanner handoff. The other starts at the key-entry state
+obtained from the actual complete source producer/scanner/split and executes
+its whole current-inverse key to the real continuation. That cut is encoded
+once at entry; it is not evidence of binary scanner execution. No borrowed
+or output stream is reconstructed between the bit instructions in a cut.
+
+We did not execute the full binary mask, all 2,944 keys, all sorting passes
+or whole-layer endpoint. Their binary correctness follows conditionally
+from the source theorem and the step proof above, not a claimed full replay.
+No independent human or formal-kernel acceptance is asserted.
+
+## Attribution
+
+PR5105 supplies complete finite control and the source caller proof. PR4982
+supplies the unchanged binary executor and earlier key simulation; PR5015
+supplies the isolated radix refinement. We preserve the CRT/key/scanner/
+repair lineage of Cinna Davis, Hiroki KUMAZAKI, ToikY, Jose Manuel, Ryanson
+Jonathan, unpaidmoon, codyw912, Douglas Colkitt and the retained notices.

research/crt-complete-binary-refinement/README.md

@@ -0,0 +1,76 @@
+# Complete binary refinement of the fixed CRT repair caller
+
+This answers PR5105's first Open next question: lower its **complete**
+finite-symbol program to a literal bit-operation program, including stencil
+products, role registers, split/key, sorting, reinsertion and disposal.
+It reuses PR4982's unchanged bit executor. PR4982's key and PR5015's isolated
+radix algorithm are not rebuilt or claimed again.
+
+The written [proof](PROOF.md) establishes source-step simulation for the
+actual admitted u2/t2/y8 caller, arbitrary opaque 12-bit payload labels and
+its admitted 32-bit ROM. A four-round static closure finds 4,932 canonical
+values, all encodable in 13 bits. The complete 8,242-instruction source
+compiles to 557,123 bit instructions using 31 tape roles and 14,839 finite
+control bits. For T source instructions, its complete invocation bound is
+
+    binary actions <= 101391 T + 29679.
+
+Every runtime tape operand is a literal role selected by bit tests, and
+every data access is one-bit read/write or unit bit-head movement. Stencil
+field projection and role products are compiled finite decision chains.
+The conservative constant includes the largest overapproximated aggregate
+block; this is no speedup or new kappa claim. Input/ROM serialization,
+raw-S production and variable geometry remain external.
+
+The verifier uses the original PR5105 executor as its independent reference
+for 63 instruction/alias/dispatch cases, checks all 4,096 payload encodings,
+and detects wrong-role, short-stride and retained-control faults. It executes
+2,862 actual producer boundaries and 43,130 complete key-cut boundaries on
+persistent encoded tape objects. The key cut comes from the actual source
+producer/scanner/split state and reaches its real continuation. Its entry
+is encoded once; the scanner is not binary-replayed.
+
+**The full binary layer is not executed.** Its correctness follows
+conditionally from the complete source theorem and the written per-step
+proof, not from claiming that the bounded cuts cover 2,944 keys or all
+sorting passes. Source and proof review are AI-assisted, not independent
+human or formal-kernel acceptance. Selected PR5413 and frozen sources stay
+unchanged.
+
+## Reproduce
+
+Python 3.12, standard library only, a few seconds locally:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/crt-complete-binary-refinement
+python3.12 -O -B research/crt-complete-binary-refinement/verify.py
+```
+
+All declared live sources authenticate before assembly. Normal replay
+compares the typed frozen receipt; only `--write-result` authors it.
+Direct replay works in the official Git-free export. Compilation is fixed
+source preprocessing; no input payload or ROM is an assembler argument.
+The private blank backing and valid encoded entry contract are inherited;
+this does not provide arbitrary-dirty-storage allocation or malformed-input
+rollback.
+
+## Open next questions
+
+1. Budget a complete binary-layer replay using the source instruction census
+   before spending billions of literal steps. This would corroborate the
+   proof with a whole endpoint; it is not a prerequisite disguised as a
+   passing partial replay here.
+2. Bind encoded ROM/descriptor construction and raw-S production to this
+   exact representation and ownership contract. Those missing producers,
+   variable geometry and the full E(p,ell) bill block a uniform CRT claim.
+
+Exact pins and structured questions are in SOURCES.json and TASK.json.
+Canonical claim: [Discussion4709](https://github.com/CrocSwap/integer-mult-bounds/discussions/4709#discussioncomment-19172880).
+Fresh entry overlap covered 342 open PRs and 4,736 discussion records.
+Unpublished work and arbitrary diffs are outside that coverage.
+
+Prepared by JoyboyBrian with substantial OpenAI Codex assistance; Apache-2.0.
+Retain PR5105/PR4982/PR5015 and the credited Cinna Davis, Hiroki KUMAZAKI,
+ToikY, Jose Manuel, Ryanson Jonathan, unpaidmoon, codyw912, Douglas Colkitt
+and underlying CRT/repair notices. Source retention is not scientific
+acceptance.

research/crt-complete-binary-refinement/RESULT.json

@@ -0,0 +1,87 @@
+{
+  "status": "PASS_COMPLETE_BINARY_REFINEMENT",
+  "sources": {
+    "research/crt-binary-key-port/PROOF.md": "c1fb60178576f64f170c1c0867c2a109c15a993a7bdc3ad52e1ff70c8a58faa0",
+    "research/crt-binary-key-port/binary.py": "50a3dea7fc087715b4e605e85629566ed31903026540f916df6b8cbaa536182d",
+    "research/crt-binary-radix-consumer/PROOF.md": "b2f9230f8bd435a3fae006cd8eea760912ec2eb3eab56824411f92b2875aba6f",
+    "research/crt-complete-repair-control/PROOF.md": "151211f34d80c8edd03512dd18af27b9b5b1dfe6f9fda9f904bfd59c4ab1a807",
+    "research/crt-complete-repair-control/compiler.py": "1186cdefed22890a987c1f289290c6db4c19446a29461c1db46257f318b05156",
+    "research/crt-complete-repair-control/machine.py": "afa110ed2fdba62e810fd794e5fd62a07ec4caf18e8919066275523713353cc7",
+    "research/crt-dense-guard-scan/PROOF.md": "c075a3c261bb824884f0da9f99fed227b15f9fac087bbdeb2c2cb861d4091f11",
+    "research/crt-dense-guard-scan/machine.py": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7",
+    "research/crt-mask-repair-bridge/PROOF.md": "c74f93a65f7b28e751a9c93aa37fc7f74f7ce42cd96e31fa3d1212c94991769c",
+    "research/crt-mask-repair-bridge/bridge.py": "573451d94435b6096a88250ca2a9fb75f39bcfa6f0436ffe2363ee07381d8331",
+    "research/crt-mask-repair-bridge/key_subroutine.py": "ffdbb610be71ae20bf974946dac66b6c1b4d43739cbc3b1eb81cbbeab8784b44",
+    "research/crt-paid-key-service/PROOF.md": "1a4ac02653eb6c1b20807033a910f27bf9484cc972bf2629941f589275a87325",
+    "research/crt-paid-key-service/service.py": "ff06c6305c9f650a694e5c42baa4c7d841decf844a4f44f6776acc10a8400083",
+    "research/crt-unary-stencil-producer/PROOF.md": "4076e6041bedce5269c1d4e3d62f0e4213a4b2e790fe270b89b4b4f3363e08aa",
+    "research/crt-unary-stencil-producer/producer.py": "8586d019a0a35390d36b944a2b764ec96682040b1abc42e29d740faf5a830bd0",
+    "research/crt-uniform-rom-query/PROOF.md": "736be5e1af590f2195e8b56b958258f0babe5cd6d2cf6f4f5023410112f4d870",
+    "research/crt-uniform-rom-query/machine.py": "46ee6a635251e498ee9a5d4aff8c0e2a7f1ef2ff951e5b6a2a8953316e9cd02d",
+    "research/unconditional-batched-crt/CRT.md": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b",
+    "research/unconditional-batched-crt/NOTICE.md": "924109837e71c52392191710d49c9deb42780878d1094f0b01e8690dbe799461",
+    "research/unconditional-batched-crt/check_batched_crt.py": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e"
+  },
+  "closure_rounds": 4,
+  "source_instructions": 8242,
+  "source_opcodes": {
+    "andbit": 200,
+    "branch": 1060,
+    "copy": 1717,
+    "eq": 863,
+    "field": 13,
+    "halt": 47,
+    "jump": 867,
+    "move": 1613,
+    "ne": 142,
+    "not": 9,
+    "notin": 1,
+    "orbit": 92,
+    "read": 887,
+    "record": 5,
+    "write": 539,
+    "xorbit": 187
+  },
+  "tape_roles": 31,
+  "codes": 4932,
+  "binary_instructions": 557123,
+  "control_bits": 14839,
+  "max_block": 101391,
+  "source_program_sha256": "192f2e099d8c82cfc2c4d531e615ca52ee15218e620f44df776fcee782511599",
+  "binary_program_sha256": "ba95a86c5e119438144119a33211d58122d638085804a0454c0e325fe6bdd2e7",
+  "micro": {
+    "cases": 63,
+    "binary_actions": 6457,
+    "mutants": [
+      "short_stride",
+      "keep_control",
+      "wrong_role"
+    ],
+    "dynamic_role_pc": 899
+  },
+  "structural": {
+    "control_edges": 518607,
+    "dirty_initialization_bits": 14839,
+    "rejected": [
+      "receipt_boolean",
+      "receipt_float",
+      "unknown_source_opcode",
+      "wrong_source_relocation"
+    ]
+  },
+  "cuts": {
+    "producer": {
+      "source_boundaries": 2862,
+      "binary_actions": 132662,
+      "tape_actions": 22452,
+      "encoded_tapes": "4818bd8ec2b09102a7e3d66e675a3b11c199525d989d3395de0b61abb473dfaa"
+    },
+    "actual_scanner_split_key": {
+      "source_boundaries": 43130,
+      "binary_actions": 1728409,
+      "tape_actions": 343742,
+      "encoded_tapes": "75a29b41535e58d987a34345aad8794fd2be9379ef85e9d11cebbe00f2815839"
+    },
+    "boundary": "Key entry is source-generated and encoded once; scanner itself is not binary-replayed."
+  }
+}