Execute paid CRT key service at the actual repair port

research/crt-paid-key-service/CALLER.json

@@ -0,0 +1,38 @@
+{
+  "all_heads_returned": true,
+  "all_roles_blank": true,
+  "calls": 2944,
+  "good_addresses_evaluated": 0,
+  "hole_addresses_missed": 0,
+  "key_cell_actions": 39360192,
+  "key_census": {
+    "andbit": 235392,
+    "branch": 32726376,
+    "copy": 5132496,
+    "eq": 30341736,
+    "eq_reg": 2384640,
+    "halt": 2944,
+    "jump": 14725632,
+    "move": 17780512,
+    "orbit": 94144,
+    "read": 19826960,
+    "set": 3306592,
+    "write": 1513216,
+    "write_reg": 239504,
+    "xorbit": 197120
+  },
+  "key_instructions": 128507264,
+  "key_interface_actions": 229632,
+  "marked_holes": 2944,
+  "payloads": 4096,
+  "producer_actions": 841,
+  "protected_payload_sha256": "9f13ccbf0d3940fa161b3244829da3505176477991775910ee543db889e2df64",
+  "repair_actions_including_key_interface": 13314027,
+  "repair_and_key_cell_actions": 52444587,
+  "scanner_actions": 454830,
+  "schedule_index": 2,
+  "scope": "One original middle layer, unchanged source producer/scanner/repair with only evaluate_key replaced; raw macro/ROM preparation and outer Boolean control costs remain external.",
+  "service_sha256": "ff06c6305c9f650a694e5c42baa4c7d841decf844a4f44f6776acc10a8400083",
+  "status": "PASS_ACTUAL_MIDDLE_LAYER_PAID_KEY",
+  "target": 2
+}

research/crt-paid-key-service/COMPONENT.json

@@ -0,0 +1,62 @@
+{
+  "accepted_cases": 376,
+  "behavior_mutants": {
+    "drop_high": 892,
+    "omit_clear": 0,
+    "omit_rom_return": 0,
+    "stale": 892
+  },
+  "bounds": [
+    {
+      "outside_query_instructions": 3057,
+      "proved_instruction_bound": 3286830,
+      "rewind_loops": 244,
+      "static_instructions": 5313,
+      "target": 0
+    },
+    {
+      "outside_query_instructions": 3067,
+      "proved_instruction_bound": 3286970,
+      "rewind_loops": 244,
+      "static_instructions": 5323,
+      "target": 1
+    },
+    {
+      "outside_query_instructions": 3077,
+      "proved_instruction_bound": 3287110,
+      "rewind_loops": 244,
+      "static_instructions": 5333,
+      "target": 2
+    }
+  ],
+  "cases_sha256": "ac434579c0cad0a6c5c7bf3ff7a619b17a5dca033913a220afcf0af1021eb278",
+  "ledger_mutants": 2,
+  "max_instructions": 44928,
+  "min_instructions": 41395,
+  "rejected_addresses": 4,
+  "service_sha256": "ff06c6305c9f650a694e5c42baa4c7d841decf844a4f44f6776acc10a8400083",
+  "source_layers": [
+    {
+      "rom": "00000000000000000000000000000000",
+      "target": 0
+    },
+    {
+      "rom": "00000000000010100000000000000000",
+      "target": 1
+    },
+    {
+      "rom": "00000000001000101000100000000000",
+      "target": 2
+    },
+    {
+      "rom": "00000000111110101010000000000000",
+      "target": 1
+    },
+    {
+      "rom": "00000000110000001111000000000000",
+      "target": 0
+    }
+  ],
+  "status": "PASS_PAID_KEY_COMPONENT",
+  "total_replayed_instructions": 16345420
+}

research/crt-paid-key-service/PROOF.md

@@ -0,0 +1,185 @@
+# Complete key service at the retained repair port
+
+JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0.
+
+This is a fixed-geometry program theorem, with a replay of its actual caller.
+The domain is the existing u2,t2,y8 fixture, not arbitrary CRT parameters.
+
+## Proposition and port contract
+
+Fix J in {0,1,2} and any 32-bit ROM F satisfying
+`F[v] = F[v xor 2^J]` for 0 <= v < 32. Define `f(y)=F[y mod 32]`.
+For every address `q=(u,t,y)` with 0 <= u,t < 4 and 0 <= y < 256,
+`Service.evaluate_key` appends the twelve MSB-first bits of `T(S^-1(q))`
+to the existing bad stream. Here S is exactly the ten-shear word from the
+pinned `key_subroutine.py` / `check_batched_crt.py`, and T is the ideal
+switch `(u,t,y) -> (u,t,y xor (f(y)<<J))`. No good-set test is used by the
+service: the caller supplies only marked holes.
+
+The borrowed `counter` contains `<` followed by exactly twelve bits and `>`;
+its head starts at zero. The borrowed `rom` contains `L`, exactly 32 bits,
+and `R`, also at head zero. These framed finite records and the initially
+blank owned tapes are the contract. The stream head is at the first free
+key cell after an opaque payload record, with twelve blank cells available.
+Its prior prefix may contain the caller's existing payloads and keys.
+
+On acceptance, counter/ROM cells are unchanged and both heads are zero;
+the stream prefix is unchanged and its head has advanced exactly twelve;
+all private cells are blank and all private heads zero. The stream is an
+append port, so returning *its* head to zero would violate the original
+bridge interface. The service never reads the stream.
+
+There are 15 tape roles. The twelve owned roles and their maximum payload
+widths are:
+
+| Role | h | s | offset | target | out | count | col | row | limit | u | t | y |
+| --- | ---: | ---: | ---: | ---: | ---: | ---: | ---: | ---: | ---: | ---: | ---: | ---: |
+| Width | 3 | 2 | 1 | 4 | 1 | 3 | 4 | 2 | 5 | 2 | 2 | 8 |
+
+Two framing cells are reserved for each owned record. These finite extents,
+including formerly used markers, are erased on every return. The query roles
+h,s,offset,target are borrowed *by the nested query*, but owned by this service.
+The service creates their headers through charged writes on every invocation.
+
+## Program versus host observer
+
+`assemble` emits one of three fixed programs for J=0,1,2: respectively
+5,313, 5,323 and 5,333 instructions. Its Python loops, shifts and constants
+are assembly-time operations over this fixed geometry. The evaluator has no
+instruction to obtain a tape's length, head coordinate, address integer,
+decoded descriptor, Python list index from data, or host key result. Runtime
+registers contain one symbol/bit or a Boolean, and the PC destinations are
+fixed integers. `xorbit`, `andbit` and `orbit` are Boolean operations on two
+one-bit operands. Every read, write, unit move, equality, bit operation,
+register operation, branch, jump and halt contributes one to the census.
+
+Python dictionaries, physical tape-head integers, instruction addresses and
+counters implement the emulator/observer. They are never exposed as data to
+the program. A tape read uses only its current cell. The `trace` option changes
+logging only. `verify.py` independently decodes output, key epochs and the
+caller's address log to compare results; none of those decoded values feeds
+back to the executor. The actual caller adapter adds an address to the original
+oracle's observer list because its existing assertions inspect that list; it
+never calls that oracle's `key_of`, nor supplies its result to the service.
+
+This is not a uniform compiler in u/t/y widths: those widths and J are fixed
+when the three programs are assembled. The ROM is a parameter supplied in tape
+form; its construction is not computed by this package.
+
+## Correctness of current-state queries and shears
+
+The input copy reads the twelve counter cells and writes u,t,y as separate
+little-endian bit records. It checks every payload symbol and the exact right
+marker. Invalid finite twelve-cell framing paths enter cleanup before any
+stream append. Four such rejection controls are replayed; arbitrary unframed
+inputs with missing left markers are outside the port contract.
+
+At every source access, the descriptor is rebuilt from the *current* y.
+Offset is y4, and target is y0..y3 with its highest nonzero position selected
+by finite tests (zero is one `0` digit). The service writes h=4 and s=2 in
+canonical little-endian form. The unchanged 752-instruction program from
+`crt-uniform-rom-query/machine.py` therefore returns
+`F[offset*16+target] = F[y mod 32]`. All 32 source cells are scanned; there is
+no dynamic table lookup. This reasoning is for every legal F, not just the
+five ROMs replayed. Each nested query clears count/col/row/limit and returns
+all ten query heads. The service reads and clears out before continuing.
+
+To invert the ten-shear word, process steps 9 down to 0. At step 9 add f(y)
+to u modulo 4; at step 4 subtract f(y). At other steps, let
+`r=step` for step<4 and `r=step-5` otherwise. Read z=u0, digit=t0+2t1,
+and bit=yJ from the current records. The inverse update is:
+
+| r | Update |
+| --- | --- |
+| 0 | y -= 2*z*digit*2^J modulo 256 |
+| 1 | t -= bit modulo 4 |
+| 2 | y -= z*2^J; y += 2*z*digit*2^J modulo 256 |
+| 3 | t += (bit xor z) modulo 4 |
+
+The two digit-dependent y terms are decomposed into conditional constants
+`2^(J+1)` and `2^(J+2)`, guarded by z AND t0 or z AND t1. For each chosen
+constant the full-width carry recurrence is
+`sum=a xor b xor carry`,
+`nextcarry=(a AND b) OR ((a xor b) AND carry)`.
+Discarding only the final width-2/width-8 carry implements the stated modular
+addition, including negative constants encoded modulo the full word width.
+There is no truncated low-window update. After ten steps, a third current-y
+source query gives f(y), and XOR on yJ applies T. Physical reads then copy the
+u,t,y bits directly to the stream in MSB order. No host key string is formed.
+
+All operations in the table are inverse shears because the controlling
+coordinates do not change in their update; for r=0,2 the multiplier of 2^J
+is even in r=0 and has parity z in r=2, as in the original compact word.
+More directly, the formulas are the literal reverse order and negated offsets
+of the pinned ten-shear source. Target independence of F is the original
+ideal-switch condition. The final result is exactly T(S^-1(q)).
+
+The private cleanup performs fixed writes over every reserved cell, then fixed
+moves home. This includes headers created by the service and query scratch
+already erased by the nested query. Counter rewind scans only the finite
+retained record. No early halt precedes cleanup.
+
+## Static complete instruction bound
+
+The pinned query proof gives, for legal h,s and ROM,
+`Q <= 512*(s*2^h+1)*(h+bit_length(s)+2)^2`.
+Here h=4, s=2, so `Q <= 1,081,344`. Replacing each nested halt by one jump to
+the service continuation does not increase this count. There are exactly three
+queries on every valid input, for at most 3,244,032 instructions.
+
+Remove the three disjoint 752-instruction query ranges. The remaining static
+instruction counts D are 3,057, 3,067 and 3,077. `program_bound` checks their
+actual control-flow targets: every backward edge outside a query is exactly
+the five-instruction rewind sequence `read,eq,branch,move(-1),jump`, and every
+other edge is forward. Rewinds do not nest and no outer loop revisits a query.
+Each of the 244 rewind sites is on counter or private roles; no rewind is on
+the arbitrary-position stream. The counter head never exceeds 13, and outside
+queries private heads never exceed 10. Starting at distance d<=13, a rewind
+visits each instruction at most d+1<=14 times (its terminal read/test/branch
+are included). All other outside instructions execute at most once. Thus
+
+`T <= 3*1,081,344 + 14*D <= 3,287,110 < 3,300,000`.
+
+This charges full finite control, all header/descriptor construction, carry
+work, input copy, all three ROM scans, stream append and final erasure/return.
+The observed 41,395–44,928 instructions in COMPONENT.json are merely a much
+smaller sampled range; they are not used to prove the bound. The bound covers
+all 4,096 addresses and all target-independent 32-bit F in the stated domain.
+
+The executed census is this finite-alphabet instruction model. This package
+makes **no numerical binary-action claim for the whole service/caller**.
+In particular the caller's stream has opaque 12-bit payload symbols, so the
+query component's three-bit/32-action local lowering must not be silently
+reused for the full port alphabet. A complete binary encoding of the joined
+caller and its outer controls remains separate work.
+
+## Actual caller composition and accounting
+
+`verify.py --part caller` instantiates the pinned original Env and calls its
+unchanged `run_layer`, at the middle of the actual five-layer schedule
+(target 2), on all 4,096 identity-labelled payloads. Only the function installed
+at `env.bridge.evaluate_key` changes. The same source producer constructs the
+stencil, the same scanner constructs the mask, and the same repair partitions,
+sorts marked-hole records by appended keys and refills the stream. Its 2,944
+key invocations all use the actual counter/stream objects. All holes are called
+once, no good address is called, the final payload matches the ideal layer,
+and all owned caller/service tapes and heads are returned. This is one whole
+source layer, not a replay of all five layers or the ten-layer round trip.
+
+The source repair tape invoice already counts the key service's counter and
+stream cell actions. The service census counts them too. The exact disjoint
+cell invoice is therefore
+
+`repair_and_key = repair_actions + key_cell_actions - key_interface_actions`.
+
+The frozen receipt gives 13,314,027 + 39,360,192 - 229,632 = 52,444,587.
+The service's separate complete instruction total is 128,507,264. These are
+different ledgers; it would be incorrect to call their sum a fully priced
+joined program. Producer 841 and scanner 454,830 are retained cell invoices.
+The existing caller's bit-weight meter is not a complete binary lowering.
+
+The raw post-S stream, ideal-output oracle and initial source ROM are supplied
+by the unchanged host harness. The program constructing S, all-size CRT/ROM
+reconstruction, source-layout conversion, outer producer/scanner/repair Boolean
+controls and uniform all-parameter E(p,ell) are outside this result. Removing
+the host-word key premise at this finite port does not discharge those costs.

research/crt-paid-key-service/README.md

@@ -0,0 +1,108 @@
+# Paid finite-control key at the actual CRT repair port
+
+This package replaces the host-integer `evaluate_key` premise of
+[the mask-driven repair bridge](../crt-mask-repair-bridge/README.md) with an
+actual finite-control tape service for its retained u2,t2,y8 geometry. It
+executes all ten inverse shears, three current-state source queries, the ideal
+switch, and direct twelve-bit stream append. Borrowed counter/ROM cells are
+preserved; scratch is erased and its heads returned. The append head advances
+twelve cells as required by the existing interface.
+
+The scoped [proof](PROOF.md) covers every 12-bit address and every
+target-independent 32-bit source ROM, for target 0, 1 or 2, with a complete
+instruction bound below **3,300,000 per key**. This is a fixed-geometry theorem
+and an actual caller replay, not an all-size CRT theorem or an E(p,ell) closure.
+
+## New result and predecessor boundary
+
+[PR #4637](https://github.com/CrocSwap/integer-mult-bounds/pull/4637), exact head
+`60d0b09f13a9f9ebdd93d98d83d16ce6907d70b6`, joins producer, scanner and repair
+but leaves the address-to-key function in host integer arithmetic.
+[PR #4739](https://github.com/CrocSwap/integer-mult-bounds/pull/4739), exact head
+`26ccde014218f7d906d1251dc295fbc1437ede8a`, charges transported key bit work
+in a different finite fixture without eliminating host control.
+[PR #4752](https://github.com/CrocSwap/integer-mult-bounds/pull/4752), exact head
+`e8bdf35809eecfb0b8db7b5e141cb1ba0f4f6a1c`, gives the uniform encoded ROM query
+but explicitly leaves its caller descriptor adapter and remaining key work open.
+
+The new [service](service.py) rebuilds descriptors from the current tape y at
+all three epochs and inlines that query program. Its executor never decodes
+an address/word or inspects head coordinates, tape lengths or a host key.
+Assembly is finite for the three retained targets. Fifteen tape roles include
+the original counter/stream, one borrowed ROM and twelve owned tapes.
+[SOURCES.json](SOURCES.json) pins the complete live dependency closure to
+base `624de9dc66858af0945e5f8a0942488d62280d43`; predecessors are reused unchanged.
+The selected result is unchanged. Archive merging is not scientific approval.
+
+## Evidence and cost boundary
+
+[COMPONENT.json](COMPONENT.json) records 376 accepted cases across all five
+actual source-layer ROMs plus a parity source. A separate event interpreter
+replays **16,345,420 instructions**, checks all three source epochs, borrowed
+contents, direct append and private erasure. Four malformed addresses reject;
+four behavioral faults (stale descriptor, truncated carry, omitted erase,
+omitted ROM return) and two incomplete event logs are detected. Sampled key
+costs range from 41,395 to 44,928 instructions; the proof uses static charging,
+not that sampled maximum.
+
+[CALLER.json](CALLER.json) records the unchanged original middle-layer
+producer→scanner→repair execution with only the key port replaced:
+
+| Quantity | Exact value |
+| --- | ---: |
+| Protected payloads | 4,096 |
+| Marked holes / service calls | 2,944 |
+| Good addresses called / holes missed | 0 / 0 |
+| Complete key-service instructions | 128,507,264 |
+| Key-service cell actions | 39,360,192 |
+| Interface cell actions already in repair invoice | 229,632 |
+| Original repair cell invoice including interface | 13,314,027 |
+| De-duplicated repair + key cell actions | 52,444,587 |
+| Producer / scanner cell invoices | 841 / 454,830 |
+
+The full protected output equals the source ideal layer and every required
+caller/service scratch tape and head is restored. Only this middle layer was
+fully replayed; component tests use all five source ROMs.
+
+These instruction and cell ledgers are distinct. The raw macro S, supplied
+ROM construction/layout, outer producer/scanner/repair Boolean control,
+all-size parameter handling and total E(p,ell) remain external. No numerical
+binary-action bound is claimed for the joined port: opaque payload symbols
+need a wider encoding than the query component's five-symbol alphabet.
+Verifier-only host arrays and address logs never feed back into the service.
+
+## Reproduce
+
+Python 3.12, standard library, one CPU; no Lean, Docker or historical suite.
+From the repository root:
+
+```sh
+python3.12 scripts/research_package.py --package research/crt-paid-key-service --check-only
+python3.12 scripts/research_package.py --package research/crt-paid-key-service
+python3.12 -O -B research/crt-paid-key-service/verify.py
+```
+
+The registered hook compares both frozen receipts and authenticates all live
+inputs. It runs components (60-second cap) and the one caller layer (120-second
+cap) sequentially. The source caller producer run took 36.7 seconds locally;
+runtime is environment-dependent, not a complexity claim. Receipts are only
+rewritten with explicit `--write-result`. See [TASK.json](TASK.json) for the
+refined scope and [VERIFY.json](VERIFY.json) for the commands.
+
+## Open next questions
+
+1. Supply the 32-bit source ROM through a physically costed producer, then
+   generalize the encoded parameter and bit-word widths. Start by identifying
+   the source ROM layout at the actual CRT caller; a larger finite census does
+   not establish this uniform construction.
+2. Price or lower all control in the joined producer/scanner/repair and its
+   opaque-payload alphabet. Start from the exact interface subtraction above;
+   counting only cell operations leaves a different obligation from the now
+   complete key-service instruction census.
+
+## Credit
+
+JoyboyBrian, with substantial OpenAI Codex assistance. New work Apache-2.0.
+Retain the upstream authorship and [source-specific notice](../unconditional-batched-crt/NOTICE.md)
+for the original construction, the repair/tape packages and their pinned source
+files. This package imports their code and preserves their source bytes.