Lower the CRT key service to literal binary instructions at its caller port

research/crt-binary-key-port/PROOF.md

@@ -0,0 +1,177 @@
+# Literal binary key at the retained repair port
+
+JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0.
+
+## Object and claim
+
+This lowers the actual `service.py` program of #4795 (head
+`4e4cf7e47f3fc1c40e775d84fb2e7cd2603658cd`). For each fixed J in {0,1,2},
+its domain remains u2,t2,y8, every 12-bit address, and a supplied 32-bit F
+independent of yJ. The source proof gives the key T(S^-1(q)), three current-y
+queries, borrowed counter/ROM preservation, private erasure/head return,
+append of twelve source bit symbols and at most 3,287,110 source instructions.
+Those source semantics are a retained premise; this package proves their
+literal binary realization and tests its actual caller interface.
+
+There are the same fifteen physical tapes. Each source cell j is represented
+by bits 13j through 13j+12, little-endian; each source head j corresponds to
+physical head 13j. The stream may start at any source-cell boundary after an
+arbitrary legal payload/key prefix. Its twelve-symbol append advances the
+physical head **156** bits, not twelve. No input conversion occurs at a call.
+Packet construction/encoding and ROM supply are external entry premises.
+
+The complete program uses only one-bit reads/writes, unit physical head
+moves, one-bit assignments/copies, XOR (including a literal-bit operand),
+AND, OR, NOT, Boolean branch, jump and halt. Each executed instruction costs
+one action. It is the executable program, not a multiplication of an old
+receipt. A finite instruction transition includes its sequencing; explicit
+branches/jumps are charged instructions as well.
+
+## Encoding, including opaque payloads and finite control
+
+The source symbols have these thirteen-bit integer codes:
+
+| Symbol | blank `_` | `L` | `0` | `1` | `R` | `<` | `>` | `=` |
+| --- | ---: | ---: | ---: | ---: | ---: | ---: | ---: | ---: |
+| Code | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 |
+
+The opaque record `('R',v)` has code 4096+v, for 0<=v<4096. Thus all 4,104
+symbols are distinct, and the all-zero physical background represents blank.
+Codes 8..4095 are unused. The port theorem assumes correctly encoded finite
+records and aligned heads; it is not an arbitrary-bit-string admission theorem.
+`=` is a source finite-control value; including it in the common alphabet is
+harmless even though the retained key program does not write it to a tape.
+
+Each source register uses fourteen one-bit registers. A symbol is its 13-bit
+code followed by tag zero. Boolean false/true has low bit zero/one, twelve
+further zeros, and tag one. This distinguishes Boolean true from symbol `L`
+and Boolean false from blank. The source uses finite-control equality results
+as Boolean branch conditions; tape values and `0`/`1` arithmetic are symbols.
+Dropping the tag makes equality of true and L incorrect even though both have
+low code one. Registers and code locations have fixed finite cardinality.
+The compiled full service has 492 one-bit registers, independent of address,
+source ROM contents or stream-prefix length.
+
+Complete service compilation emits 492 initial zero assignments and another
+492 before each reachable halt. Only one halt is reached per invocation, so
+**984 lifecycle actions** are executed. The verifier deliberately starts the
+emulator registers dirty; input initialization and final erasure are paid.
+No free host allocation/reset is needed in the claimed machine. Primitive
+block tests omit this wrapper to supply arbitrary initial register values.
+
+## Per-block simulation
+
+Take any source state at an instruction boundary, with tape cells/heads and
+initialized register operands represented as above. The following invariant
+holds after each corresponding nonterminal binary block: all source-visible cells,
+registers and heads have exactly the indicated representation, and the binary
+PC is the relocated address of the next source instruction. Compiler-private
+comparison bits are not source-visible and are erased by the final lifecycle.
+
+| Source instruction | Binary implementation | Core actions |
+| --- | --- | ---: |
+| read | 13 single-bit reads, 12 moves right and 12 left, set the symbol tag to zero | 38 |
+| write / write_reg | 13 writes and the same 24 moves; return to cell start | 37 |
+| move ±1 | 13 unit moves in the same direction | 13 |
+| set / copy | fourteen one-bit assignments/copies | 14 |
+| eq / eq_reg | zero accumulator; 14 XOR+OR pairs; 13 Boolean output-tag/upper-bit assignments; NOT accumulator to low output bit | 43 |
+| xorbit / andbit / orbit | one Boolean gate on low operand bits, then 13 assignments to the remaining `0`/`1` symbol-code bits | 14 |
+| branch / jump / halt | one corresponding fixed-control operation | 1 |
+
+Read/write move only inside one encoded cell before returning, so they cannot
+read or overwrite neighboring payloads. Write writes all thirteen bits even
+when the old cell is dirty. The source data bits are codes two and three,
+which differ exactly in their low bit; the other code bits and tag are restored
+by the bit-arithmetic block. It computes the output low bit before assigning
+upper bits, so source/destination aliasing is safe.
+
+For equality, after bit i the scratch accumulator is the OR of all differences
+through i. Negating its final value is exactly equality of the full tagged
+words. All comparisons finish before writing destination bits, so aliasing a
+source and destination register is also safe. The reserved scratch names do
+not occur in the authenticated source program. Copying a word to itself is
+safe. The source's reachable branch operands are Booleans; their low bit is
+therefore the correct decision, and branch targets are statically relocated.
+
+At halt no source instruction remains; the source-visible register correspondence
+is replaced by the promised all-zero control endpoint. Source halt has a separate lifecycle suffix of 492 assignments and the halt
+itself; the table's one-action halt is its core, not a claim that cleanup is
+free. The initial 492 assignments precede the first source block. Labels are
+relocated after these expansions, including jumps across either halt suffix.
+
+Induction on the actual source execution proves the simulation, termination,
+key and ownership result. In particular, all cleared source private cells
+become thirteen zero bits, borrowed cells are unchanged, private/counter/ROM
+heads return to zero and the protected stream prefix is unchanged. All finite
+control bits also finish zero. This argument applies to every legal source
+input; testing a finite subset is corroboration, not the induction hypothesis.
+For a framed input on which the source rejects and cleans up, the same
+simulation gives rejection/cleanup, without claiming the legal-input time
+bound for arbitrary malformed packets.
+
+## Complete bound
+
+Let T be a legal #4795 source execution length, including its one halt, and
+let R=492. Every core block costs at most 43, and initialization/termination
+cost 2R. Therefore
+
+`T_binary <= 43*T + 2R <= 43*3,287,110 + 984 = 141,346,714`.
+
+This includes every executed bit action and Boolean/control instruction,
+current-state descriptor/header work, all three ROM traversals, full carry
+arithmetic, append, private erasure, physical head return and finite-control
+initialization/erasure. No asymptotic compiler bound is asserted: the compiler
+emits one of three fixed finite programs (106,583 / 106,713 / 106,843 bit
+instructions). Its static program size contains two halt cleanup paths; its
+runtime takes only one. The sampled counts near 0.9 million actions/key are
+not used to prove the upper bound.
+
+The interpreter's PC, register-number lookup, sparse tape dictionary indices,
+head coordinates and action census are emulator metadata. `Machine.step`
+never exposes a coordinate, tape length, decoded word or count to the program.
+Runtime values read from tapes or registers are individual bits. There is no
+symbol decoder or original key evaluator inside the binary executor. The
+source is compiled before any address/ROM/payload is supplied. All data paths
+in the executable are the stated primitive bit operations.
+
+## Caller-bound evidence and limits
+
+The verifier constructs the same middle-layer source ROM, raw compact-word
+payload stream and original guard mask as the retained source caller. The
+unchanged `bridge.split` runs on facades whose **only storage is physical bit
+tapes**. Facade reads decode symbols for the unlowered outer controller; facade
+writes/moves perform the corresponding bit operations. This outer decoding
+is an explicit boundary, not part of the binary key program or its tariff.
+
+At the original `evaluate_key(counter,bad,...)` call, the new adapter gives
+`Machine` those same underlying tapes, without reading/converting an address
+into an executor parameter or copying in/out a computed key. Observer-only
+address decoding checks the source reference, but never feeds the executor.
+The first two actual marked-hole calls return, and the original split then
+continues to the third hole at address two. This checks that both 156-bit
+advances and the next opaque payload write obey the original caller contract.
+The verifier interrupts before executing that third key, not after a full
+layer. It then closes the captured two-completed-pair prefix with an END marker
+as explicit verifier setup and passes it to the unchanged original `one_pass`.
+Its radix split preserves the captured payloads, rotates their actual returned
+keys correctly and returns the consumer heads. Closing/projecting the prefix
+is not claimed to be the full split/sort/reinsert algorithm.
+
+The first two caller addresses are simple keys; a separate transported parity
+case at q=892 checks every one of 44,340 source-instruction boundaries, all
+physical head scales, every written block and every defined register result.
+Three further complete binary runs cover nontrivial carry/boundary behavior
+and all retained targets. Primitive checks cover all 4,104 encodings and their
+read/dirty-write blocks, plus 172 equality/Boolean/alias cases. Mutants expose
+short physical moves, incorrect Boolean tagging, a dirty borrowed head and
+omitted finite-control erasure, and a colliding marker code. Three framed malformed
+packets also reject with complete physical/control cleanup. These are new execution/representation checks,
+not a replay of #4795's 376-case census.
+
+Not supplied: a full 2,944-call binary layer, a literal binary lowering or full
+control tariff for the outer producer/scanner/sort/reinsert, physical creation
+of raw S or the source ROM, encoded variable-width CRT parameters, uniform
+compiler/constructor cost, or complete E(p,ell). No multiplication theorem or
+new kappa follows. The fixed-geometry source proof and its predecessor credits
+remain explicit. Other current reservoir/layout or stopped-recursion results
+address different obligations.

research/crt-binary-key-port/README.md

@@ -0,0 +1,119 @@
+# Literal binary execution at the CRT key port
+
+This package compiles and **executes** the complete finite-control key service
+of [PR #4795](https://github.com/CrocSwap/integer-mult-bounds/pull/4795) using
+one-bit tape access, unit bit-head moves and one-bit Boolean/control operations.
+It closes that package's explicit binary-encoding gap for its retained
+u2,t2,y8 geometry and the original repair counter/bad-stream port.
+
+The [scoped proof](PROOF.md) gives
+
+`binary actions per key <= 43*3,287,110 + 984 = 141,346,714`.
+
+The factor 43 is proved per source instruction. The additional 984 actions
+actually initialize and erase all 492 control bits. This is a fixed-geometry
+program theorem, not a uniform CRT compiler, complete outer repair tariff or
+new multiplication result. The selected κ is unchanged.
+
+## Executed representation
+
+[binary.py](binary.py) produces three fixed bit programs, for source targets
+0, 1 and 2, with 106,583 / 106,713 / 106,843 instructions. Every source cell
+uses thirteen physical bits: all 4,096 opaque 12-bit payload labels and eight
+source symbols have distinct codes. A separate register tag distinguishes
+Boolean true/false from symbols. All runtime reads, writes, gates and branches
+operate on individual bits; no host-decoded address/key enters the executor.
+
+The same fifteen tape roles are retained. Source-cell head j is physical head
+13j. Appending twelve source bit symbols advances the stream by **156 physical
+bits**. Private tape bits and heads, borrowed heads and all control bits are
+returned as stated in the proof; borrowed counter/ROM and prior payloads are
+preserved. Serialization of input packets and source ROM creation are explicit
+external prerequisites.
+
+## Evidence at the actual caller
+
+[verify.py](verify.py) independently represents symbol/Boolean values and
+executes source instruction semantics. [RESULT.json](RESULT.json) records:
+
+- All 4,104 codec values; 8,208 literal read and dirty-cell write cases, plus
+  172 equality/Boolean/alias controls.
+- Four complete binary key runs, including a transported parity-source key
+  at address 892. Every one of its 44,340 source-instruction boundaries is
+  checked against the independent observer: control target, physical head,
+  written cell and defined register result.
+- The original `bridge.split` with its actual middle-layer guard mask/raw
+  source stream, calling the binary service on the **same physical tapes**
+  at its first two holes. The source caller then continues to the third hole,
+  at address two, demonstrating the returned head/record boundary.
+- The unchanged original `one_pass` consumes a projection of those two completed
+  pairs and preserves payload/key correspondence. Closing that captured prefix
+  with END is explicit verifier setup; this is not a whole-layer replay.
+- Five discriminating faults: short bit stride, dirty ROM head, omitted control
+  erasure, missing Boolean tag and colliding marker code. Three framed malformed
+  packets reject with borrowed data, blank scratch and cleared controls checked.
+
+The six accepted full key invocations execute **5,348,850 binary actions**.
+The actual two caller invocations take 859,622 and 859,888 actions; the other
+four take 896,367–914,737. These observed counts do not establish the uniform
+bound; the block simulation does. The entire bounded verifier takes about
+three seconds locally, using one CPU and the standard library.
+
+The source caller facade decodes symbols for the **unlowered outer controller**.
+It never converts/copies an address or returned key at the service boundary:
+the service directly sees the facade's underlying bit tapes. Its key execution
+is wholly bit-level. Observer word decoding and oracle arithmetic are outside
+the executor. This package does not price outer control, full sorting/reinsertion,
+raw macro-S creation, ROM construction, variable-width parameters or E(p,ell).
+No full 2,944-call binary layer or historical suite was run.
+
+## Provenance and distinct scope
+
+Exact predecessor #4795 is
+`4e4cf7e47f3fc1c40e775d84fb2e7cd2603658cd`; it is retained unchanged on base
+`b91956876e5b4122fd89179f1b57557ff8378f15`. Its source proof, #4752 ROM program
+and original #4637 bridge/oracle, scanner increment, and original compact word
+are pinned in [SOURCES.json](SOURCES.json). Retention is not scientific approval.
+
+Current #4938 establishes evaluator/layout caps; #4942 and the reservoir-bill
+package price ordinary-interchange wrapper calls; #4946 audits the word-census
+prune; #4965 studies complex stopped recursion. Those do not supply this literal
+binary key executor. [TASK.json](TASK.json) records the refined question and
+bounded stop rule. Canonical coordination is
+[Discussion #4709](https://github.com/CrocSwap/integer-mult-bounds/discussions/4709#discussioncomment-19138317).
+
+## Reproduce
+
+From the repository root, Python 3.12:
+
+```sh
+python3.12 scripts/research_package.py --package research/crt-binary-key-port --check-only
+python3.12 scripts/research_package.py --package research/crt-binary-key-port
+python3.12 -O -B research/crt-binary-key-port/verify.py
+```
+
+The registered command has a 30-second cap and authenticates all declared live
+inputs before executing. Direct replay compares the frozen result; only explicit
+`--write-result` changes it. Source-history/committed-byte checks and the standard
+exporter bind the published files. Direct verification works in a Git-free export;
+the generic provenance-aware package runner itself requires Git history.
+
+## Open next questions
+
+1. Lower a bounded actual sparse-repair consumer (for example one radix pass)
+   into literal bit control using the same 13-bit representation. The current
+   facade still performs outer symbol decoding; a complete invoice must include
+   its branching, routing and lifecycle rather than multiplying a cell count.
+2. Supply physical ROM construction and variable-width parameter handling at
+   the real CRT caller. The fixed-width program and its source theorem do not
+   provide those prerequisites. First establish an encoded producer/consumer
+   contract; a larger finite key census would not resolve it.
+
+## Credit
+
+Prepared by JoyboyBrian with substantial OpenAI Codex assistance; Apache-2.0.
+Retain #4795/#4752 authorship and the #4637 scanner/repair lineage: Cinna Davis,
+ToikY, Hiroki KUMAZAKI, Ryanson Jonathan, unpaidmoon, Jose Manuel and the original
+[source-specific notice](../unconditional-batched-crt/NOTICE.md). All predecessor
+source files are reused unchanged. No independent human or proof-kernel review
+is claimed.