From 4e4cf7e47f3fc1c40e775d84fb2e7cd2603658cd Mon Sep 17 00:00:00 2001 From: JoyboyBrian Date: Thu, 22 Oct 2026 12:59:07 -0700 Subject: [PATCH] Add paid finite-control key at CRT repair port --- research/crt-paid-key-service/CALLER.json | 38 +++ research/crt-paid-key-service/COMPONENT.json | 62 +++++ research/crt-paid-key-service/PROOF.md | 185 ++++++++++++++ research/crt-paid-key-service/README.md | 108 ++++++++ research/crt-paid-key-service/SOURCES.json | 114 +++++++++ research/crt-paid-key-service/TASK.json | 80 ++++++ research/crt-paid-key-service/VERIFY.json | 48 ++++ research/crt-paid-key-service/service.py | 182 ++++++++++++++ research/crt-paid-key-service/verify.py | 250 +++++++++++++++++++ 9 files changed, 1067 insertions(+) create mode 100644 research/crt-paid-key-service/CALLER.json create mode 100644 research/crt-paid-key-service/COMPONENT.json create mode 100644 research/crt-paid-key-service/PROOF.md create mode 100644 research/crt-paid-key-service/README.md create mode 100644 research/crt-paid-key-service/SOURCES.json create mode 100644 research/crt-paid-key-service/TASK.json create mode 100644 research/crt-paid-key-service/VERIFY.json create mode 100644 research/crt-paid-key-service/service.py create mode 100644 research/crt-paid-key-service/verify.py diff --git a/research/crt-paid-key-service/CALLER.json b/research/crt-paid-key-service/CALLER.json new file mode 100644 index 0000000000..d696e0db53 --- /dev/null +++ b/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 +} diff --git a/research/crt-paid-key-service/COMPONENT.json b/research/crt-paid-key-service/COMPONENT.json new file mode 100644 index 0000000000..467f053e67 --- /dev/null +++ b/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 +} diff --git a/research/crt-paid-key-service/PROOF.md b/research/crt-paid-key-service/PROOF.md new file mode 100644 index 0000000000..a0b84e8d3b --- /dev/null +++ b/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)<`; +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. diff --git a/research/crt-paid-key-service/README.md b/research/crt-paid-key-service/README.md new file mode 100644 index 0000000000..9a6c5e090b --- /dev/null +++ b/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. diff --git a/research/crt-paid-key-service/SOURCES.json b/research/crt-paid-key-service/SOURCES.json new file mode 100644 index 0000000000..8e5db89755 --- /dev/null +++ b/research/crt-paid-key-service/SOURCES.json @@ -0,0 +1,114 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/crt-arbitrary-source-repair/verify.py", + "usage": "input", + "git_blob": "813eafd24f031b046b2d4aaabdcb0950538980f1", + "sha256": "9a646116e430a242fc16c98d6e35c21290a00ccd9951145290b9a4bf5c007d48" + }, + { + "path": "research/crt-dense-guard-scan/machine.py", + "usage": "input", + "git_blob": "ce763898bd7b4401bbab818c640a0593b65c9a82", + "sha256": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7" + }, + { + "path": "research/crt-mask-repair-bridge/SOURCES.json", + "usage": "input", + "git_blob": "079143d6d6a23fdf5be7099176e958f6376c6e52", + "sha256": "5d9989fef3c366914e7a61dd54d53f136a495eb8bc2e1a54798aeb90b95a7277" + }, + { + "path": "research/crt-mask-repair-bridge/bridge.py", + "usage": "input", + "git_blob": "826d62adbb777ceec20974e600a6ea05e03b7828", + "sha256": "573451d94435b6096a88250ca2a9fb75f39bcfa6f0436ffe2363ee07381d8331" + }, + { + "path": "research/crt-mask-repair-bridge/key_subroutine.py", + "usage": "input", + "git_blob": "5771ae55626dbc2a32a95d8c098bdd03d820833c", + "sha256": "ffdbb610be71ae20bf974946dac66b6c1b4d43739cbc3b1eb81cbbeab8784b44" + }, + { + "path": "research/crt-mask-repair-bridge/verify.py", + "usage": "input", + "git_blob": "f98abb0924ff77e865ade42a3ecd85b47887c7eb", + "sha256": "c2b7a98bf309aed8fad949c563c040e053bd4c90760406c85731026b3f37a17f" + }, + { + "path": "research/crt-unary-stencil-producer/README.md", + "usage": "input", + "git_blob": "1abff6e1019a1b46d88447896325ae966db31351", + "sha256": "747255e3c7b58c9f7ba77ccaa82799628e66851091f35c408db1950a6c91bf47" + }, + { + "path": "research/crt-unary-stencil-producer/producer.py", + "usage": "input", + "git_blob": "dd357a0679c244e5d95b2b782bd70ea9f2507795", + "sha256": "8586d019a0a35390d36b944a2b764ec96682040b1abc42e29d740faf5a830bd0" + }, + { + "path": "research/crt-uniform-evaluator/PROOF.md", + "usage": "input", + "git_blob": "7175c780b63378963c00ea29d76a9d1d7f86bbf0", + "sha256": "a67dce487dfaf0f1748458cf052b85203654d63f84c4e362ae78fe1bae1a3d42" + }, + { + "path": "research/crt-uniform-rom-query/PROOF.md", + "usage": "input", + "git_blob": "63b0551a7715b9b67f2b13510183254401eb082f", + "sha256": "736be5e1af590f2195e8b56b958258f0babe5cd6d2cf6f4f5023410112f4d870" + }, + { + "path": "research/crt-uniform-rom-query/machine.py", + "usage": "input", + "git_blob": "88292ce98d31d540c7dba6960bfe4c19f06a8077", + "sha256": "46ee6a635251e498ee9a5d4aff8c0e2a7f1ef2ff951e5b6a2a8953316e9cd02d" + }, + { + "path": "research/pr4100-crt-repair-tariff/README.md", + "usage": "input", + "git_blob": "1eba9122777570041acbd5ddcfee22ceb0e60703", + "sha256": "5953ed2ae02a609744df2274810d7016cd766f2e43bdf8f79047084ae55a0513" + }, + { + "path": "research/unconditional-batched-crt/CRT.md", + "usage": "input", + "git_blob": "d98dd8e368431cac33d5fc1c8c336696663641d6", + "sha256": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b" + }, + { + "path": "research/unconditional-batched-crt/NOTICE.md", + "usage": "input", + "git_blob": "886a8fdee275f01b459cbd68ae2815dc9269502f", + "sha256": "924109837e71c52392191710d49c9deb42780878d1094f0b01e8690dbe799461" + }, + { + "path": "research/unconditional-batched-crt/check_batched_crt.py", + "usage": "input", + "git_blob": "1cf78abccd5e06beecc3ed21ba55f7c03b65fdbc", + "sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e" + }, + { + "path": "research/unconditional-batched-crt/check_compact_crt.py", + "usage": "input", + "git_blob": "4804ceae32103840e7ffe77eb07ff50d393829df", + "sha256": "79ab80d0228af31e501272a7a3a32f1a0e8b99df72c3c550e552deccc3a7472b" + } + ] +} diff --git a/research/crt-paid-key-service/TASK.json b/research/crt-paid-key-service/TASK.json new file mode 100644 index 0000000000..a9edfbfa8a --- /dev/null +++ b/research/crt-paid-key-service/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Replace the host-word key premise at the actual u2,t2,y8 mask-driven repair port with a complete finite-control tape service. Prove correctness for all 12-bit addresses and legal 32-bit source ROMs, count every instruction, and replay one whole source middle layer.", + "scope_change_reason": "The all-size card is narrowed to the actual missing caller adapter after PR4752. PR4637 already joined producer/scanner/repair but left address-to-key arithmetic in host words. A source-bound complete finite-geometry service closes that specific premise without claiming all-size CRT or E(p,ell).", + "bottleneck_link": "The total repair budget requires a paid key at each marked hole. This package discharges the key-service instruction obligation for the retained geometry and identifies the uniform ROM/parameter and outer-control costs still missing.", + "budget_minutes": 60, + "stop_rule": "Stop after the static full-key proof, independent component event replay with fault controls, and one original middle-layer execution pass. Falsify on stale query epochs, truncated carries, ownership failure, key mismatch, missed/double-counted actions or cost above the declared 3.3 million instruction bound. No wider finite census or all-size claim.", + "outcome": "completed", + "evidence": "PROOF.md, COMPONENT.json and CALLER.json: 376 component cases, 4 invalid addresses, 4 behavioral faults, 2 missing-event faults; original middle layer with 4096 payloads and exactly 2944 marked-hole calls. Complete key census and explicit interface subtraction.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance in program construction, proof, independent event audit, caller integration and documentation; supplied through the authorized multi-agent contribution session.", + "open_questions": [ + { + "question": "Can a physically costed source ROM producer and encoded variable widths replace the retained finite geometry?", + "why_it_matters": "The fixed source ROM and widths remain premises of a uniform CRT key evaluator.", + "first_step": "Resolve the source ROM layout and parameters at the actual CRT caller; prove one producer/interface contract before expanding cases.", + "blocked_by": "No all-size ROM reconstruction or encoded variable-width key program is supplied here." + }, + { + "question": "Can the whole producer/scanner/repair caller receive a complete binary control and payload encoding tariff?", + "why_it_matters": "Existing cell invoices omit outer Boolean control and the payload alphabet is wider than the query alphabet.", + "first_step": "Use the exact counter/stream interface subtraction to form disjoint ledgers, then lower the source outer controls and payload symbols.", + "blocked_by": "The source caller uses finite-symbol payload records and a cell-action observer, not a complete binary evaluator." + } + ] +} diff --git a/research/crt-paid-key-service/VERIFY.json b/research/crt-paid-key-service/VERIFY.json new file mode 100644 index 0000000000..978b440c98 --- /dev/null +++ b/research/crt-paid-key-service/VERIFY.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/crt-arbitrary-source-repair/verify.py", + "research/crt-dense-guard-scan/machine.py", + "research/crt-mask-repair-bridge/SOURCES.json", + "research/crt-mask-repair-bridge/bridge.py", + "research/crt-mask-repair-bridge/key_subroutine.py", + "research/crt-mask-repair-bridge/verify.py", + "research/crt-unary-stencil-producer/README.md", + "research/crt-unary-stencil-producer/producer.py", + "research/crt-uniform-evaluator/PROOF.md", + "research/crt-uniform-rom-query/PROOF.md", + "research/crt-uniform-rom-query/machine.py", + "research/pr4100-crt-repair-tariff/README.md", + "research/unconditional-batched-crt/CRT.md", + "research/unconditional-batched-crt/NOTICE.md", + "research/unconditional-batched-crt/check_batched_crt.py", + "research/unconditional-batched-crt/check_compact_crt.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--part", + "components" + ], + "timeout_seconds": 60, + "checks": "Source authentication; static control-flow bound; 376 accepted, four malformed address, four behavioral fault and two missing-event cases; independent complete instruction replay and frozen receipt." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--part", + "caller" + ], + "timeout_seconds": 120, + "checks": "One unchanged actual producer/scanner/repair middle layer with paid key port, 2944 exact hole calls, protected output, ownership/head return, de-duplicated invoice and frozen receipt." + } + ] +} diff --git a/research/crt-paid-key-service/service.py b/research/crt-paid-key-service/service.py new file mode 100644 index 0000000000..726d9523ab --- /dev/null +++ b/research/crt-paid-key-service/service.py @@ -0,0 +1,182 @@ +"""Paid finite-control key at the retained twelve-bit repair port. + +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. +The source query builder and program are supplied from authenticated PR4752 bytes. +""" +from collections import Counter + +OWNED_WIDTHS = {'h': 3, 's': 2, 'offset': 1, 'target': 4, 'out': 1, + 'count': 3, 'col': 4, 'row': 2, 'limit': 5, 'u': 2, 't': 2, 'y': 8} +ROLES = ('counter', 'stream', 'rom', *OWNED_WIDTHS) + + +def assemble(query, target, fault='correct'): + if target not in (0, 1, 2): raise ValueError('retained three-target geometry only') + if fault not in ('correct', 'stale', 'drop_high', 'omit_clear', 'omit_rom_return'): + raise ValueError('unknown verifier mutation') + b = query.Builder(); e = b.emit + returns = []; entries = [] + + def rewind_counter(): + loop, back, done = (b.new(s) for s in ('counter_home', 'counter_back', 'counter_done')) + b.mark(loop); e('read', 'counter', 'scan'); b.branch('scan', '<', done, back) + b.mark(back); e('move', 'counter', -1); e('jump', loop); b.mark(done) + + def at(role, position): + # All arguments and loop bounds in this assembler are finite constants. + b.rewind(role) + for _ in range(position): e('move', role, 1) + + def read_bit(role, bit, reg): + at(role, bit+1); e('read', role, reg); b.rewind(role) + + def clear_fixed(role): + # Each private head is at zero here, even after query rejection. + for _ in range(OWNED_WIDTHS[role]+2): + e('write', role, '_'); e('move', role, 1) + for _ in range(OWNED_WIDTHS[role]+2): e('move', role, -1) + + def constant_word(role, word): + e('write', role, 'L') + for bit in word: e('move', role, 1); e('write', role, bit) + e('move', role, 1); e('write', role, 'R'); b.rewind(role) + + def add_constant(role, width, value, condition): + done, active = b.new('add_done'), b.new('add_active') + b.branch(condition, '1', active, done); b.mark(active) + e('set', 'key_carry', '0'); e('move', role, 1) + for bit in range(width): + e('read', role, 'key_a'); e('set', 'key_b', '1' if (value >> bit) & 1 else '0') + e('xorbit', 'key_a', 'key_b', 'key_ab') + e('xorbit', 'key_ab', 'key_carry', 'key_sum') + e('andbit', 'key_a', 'key_b', 'key_abcarry') + e('andbit', 'key_ab', 'key_carry', 'key_acarry') + e('orbit', 'key_abcarry', 'key_acarry', 'key_carry') + e('write_reg', role, 'key_sum'); e('move', role, 1) + b.rewind(role); b.mark(done) + + def descriptor(): + clear_fixed('offset'); clear_fixed('target') + read_bit('y', 4, 'key_descriptor'); e('write', 'offset', 'L'); e('move', 'offset', 1) + e('write_reg', 'offset', 'key_descriptor'); e('move', 'offset', 1); e('write', 'offset', 'R'); b.rewind('offset') + done = b.new('canonical_done'); labels = [b.new('canonical_width') for _ in range(4)] + for bit in (3, 2, 1): + more = b.new('canonical_smaller'); read_bit('y', bit, 'key_descriptor') + b.branch('key_descriptor', '1', labels[bit], more); b.mark(more) + e('jump', labels[0]) + for width in (1, 2, 3, 4): + b.mark(labels[width-1]); e('write', 'target', 'L'); e('move', 'target', 1) + for bit in range(width): + read_bit('y', bit, 'key_descriptor'); e('write_reg', 'target', 'key_descriptor'); e('move', 'target', 1) + e('write', 'target', 'R'); b.rewind('target'); e('jump', done) + b.mark(done) + + def source(epoch): + if fault != 'stale' or epoch == 1: descriptor() + prefix = b.new('query'); entries.append(prefix+'_entry'); returns.append(prefix+'_return') + b.mark(prefix+'_entry') + for pc, instruction in enumerate(query.PROGRAM): + b.mark(prefix+str(pc)); op, *args = instruction + if op == 'jump': args[0] = prefix+str(args[0]) + elif op == 'branch': args[1], args[2] = prefix+str(args[1]), prefix+str(args[2]) + elif op == 'halt': + e('jump', prefix+'_return' if args[0] == 'accept' else 'service_reject'); continue + e(op, *args) + b.mark(prefix+'_return'); read_bit('out', 0, 'key_source'); clear_fixed('out') + + e('jump', 'service_start'); b.mark('service_start') + constant_word('h', '001'); constant_word('s', '01') + for role, width in (('u', 2), ('t', 2), ('y', 8)): constant_word(role, '0'*width) + e('move', 'counter', 1) + for role, bit in [('u', 1), ('u', 0), ('t', 1), ('t', 0), *[('y', j) for j in range(7, -1, -1)]]: + valid, one = b.new('input_bit'), b.new('input_one') + e('read', 'counter', 'key_input'); b.branch('key_input', '0', valid, one) + b.mark(one); b.branch('key_input', '1', valid, 'service_reject'); b.mark(valid) + at(role, bit+1); e('write_reg', role, 'key_input'); b.rewind(role); e('move', 'counter', 1) + e('read', 'counter', 'key_input'); b.branch('key_input', '>', 'input_done', 'service_reject') + b.mark('input_done'); rewind_counter() + epoch = 0 + for step in range(9, -1, -1): + if step in (9, 4): + epoch += 1; source(epoch) + add_constant('u', 2, 1 if step == 9 else -1, 'key_source') + continue + shear = step if step < 4 else step - 5 + read_bit('u', 0, 'key_z'); read_bit('t', 0, 'key_t0'); read_bit('t', 1, 'key_t1') + read_bit('y', target, 'key_bit') + e('andbit', 'key_z', 'key_t0', 'key_zt0'); e('andbit', 'key_z', 'key_t1', 'key_zt1') + ywidth = target+3 if fault == 'drop_high' else 8 + if shear == 0: + add_constant('y', ywidth, -(1 << (target+1)), 'key_zt0') + add_constant('y', ywidth, -(1 << (target+2)), 'key_zt1') + elif shear == 1: add_constant('t', 2, -1, 'key_bit') + elif shear == 2: + add_constant('y', ywidth, -(1 << target), 'key_z') + add_constant('y', ywidth, 1 << (target+1), 'key_zt0') + add_constant('y', ywidth, 1 << (target+2), 'key_zt1') + else: + e('xorbit', 'key_bit', 'key_z', 'key_digit'); add_constant('t', 2, 1, 'key_digit') + source(3); read_bit('y', target, 'key_bit'); e('xorbit', 'key_bit', 'key_source', 'key_bit') + at('y', target+1); e('write_reg', 'y', 'key_bit'); b.rewind('y') + # The actual bad-stream head advances; no host key string is formed. + for role, bit in [('u', 1), ('u', 0), ('t', 1), ('t', 0), *[('y', j) for j in range(7, -1, -1)]]: + read_bit(role, bit, 'key_output'); e('write_reg', 'stream', 'key_output'); e('move', 'stream', 1) + e('set', 'key_status', '1'); e('jump', 'service_cleanup') + b.mark('service_reject'); e('set', 'key_status', '0') + b.mark('service_cleanup'); rewind_counter() + for role in OWNED_WIDTHS: + if fault != 'omit_clear' or role != 'y': clear_fixed(role) + if fault == 'omit_rom_return': e('move', 'rom', 1) + b.branch('key_status', '1', 'service_accept', 'service_failed') + b.mark('service_accept'); e('halt', 'accept'); b.mark('service_failed'); e('halt', 'reject') + program = b.finish() + return program, {'entries': [b.labels[x] for x in entries], 'returns': [b.labels[x] for x in returns]} + + +class PrivateTape: + """Sparse initially blank tape; integer head is emulator metadata only.""" + def __init__(self): self.cells = {}; self.head = 0 + def read(self): return self.cells.get(self.head, '_') + def write(self, value): self.cells[self.head] = value + def move(self, direction): self.head += direction + + +class Service: + def __init__(self, query, target, rom, fault='correct'): + self.program, self.marks = assemble(query, target, fault) + self.rom = rom + self.private = {name: PrivateTape() for name in OWNED_WIDTHS} + self.calls = 0; self.totals = Counter(); self.last = None + + def evaluate_key(self, counter, stream, meter=None, trace=False): + tapes = dict(self.private, counter=counter, stream=stream, rom=self.rom) + regs = {}; pc = 0; census = Counter(); events = [] if trace else None; interface = 0 + # Fixed finite-control dispatch. No tape lengths, head coordinates, or + # decoded address/descriptor integers are inspected by this executor. + while True: + current = pc; op, *a = self.program[pc]; pc += 1; census[op] += 1; value = None + if op == 'read': value = tapes[a[0]].read(); regs[a[1]] = value + elif op in ('write', 'write_reg'): + value = a[1] if op == 'write' else regs[a[1]]; tapes[a[0]].write(value) + elif op == 'move': tapes[a[0]].move(a[1]) + elif op == 'set': regs[a[0]] = a[1] + elif op == 'copy': regs[a[1]] = regs[a[0]] + elif op == 'eq': regs[a[2]] = regs[a[0]] == a[1] + elif op == 'eq_reg': regs[a[2]] = regs[a[0]] == regs[a[1]] + elif op == 'xorbit': regs[a[2]] = '1' if (regs[a[0]] == '1') != (regs[a[1]] == '1') else '0' + elif op == 'andbit': regs[a[2]] = '1' if regs[a[0]] == '1' and regs[a[1]] == '1' else '0' + elif op == 'orbit': regs[a[2]] = '1' if regs[a[0]] == '1' or regs[a[1]] == '1' else '0' + elif op == 'branch': pc = a[1] if regs[a[0]] else a[2] + elif op == 'jump': pc = a[0] + elif op != 'halt': raise ValueError('unknown opcode') + if op in ('read', 'write', 'write_reg', 'move') and a[0] in ('counter', 'stream'): interface += 1 + if events is not None: events.append((current, value)) + if op == 'halt': status = a[0]; break + self.calls += 1; self.totals.update(census) + self.last = dict(events=events, census=census, registers=regs, status=status, pc=pc, tapes=tapes) + if meter is not None: + meter['calls'] += 1 + # Retain the caller's interface invoice as a subset, never add twice. + meter['interface_actions'] += interface + if status != 'accept': raise ValueError('key-service input rejected after cleanup') + return census diff --git a/research/crt-paid-key-service/verify.py b/research/crt-paid-key-service/verify.py new file mode 100644 index 0000000000..9cd6b46a1a --- /dev/null +++ b/research/crt-paid-key-service/verify.py @@ -0,0 +1,250 @@ +"""Source-bound independent key-event replay and one original caller layer. + +JoyboyBrian with substantial OpenAI Codex assistance. Apache-2.0. +All word decoding, expected keys and address logs here are verification oracles. +""" +import argparse +from collections import Counter +import hashlib +import json +from pathlib import Path +import sys +import types + +P = Path(__file__).resolve().parent +ROOT = P.parents[1] + + +def need(ok, why): + if not ok: raise ValueError(why) + + +def load(name, path, raw): + m = types.ModuleType(name); m.__file__ = str(path); sys.modules[name] = m + exec(compile(raw, str(path), 'exec'), m.__dict__); return m + + +def sources(): + data = {} + for row in json.loads((P/'SOURCES.json').read_text())['files']: + if row['usage'] != 'input': continue + raw = (ROOT/row['path']).read_bytes() + need(hashlib.sha256(raw).hexdigest() == row['sha256'], 'source SHA256 drift') + need(hashlib.sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest() == row['git_blob'], 'source Git blob drift') + data[row['path']] = raw + def pred(name, path): return load(name, ROOT/path, data[path]) + query = pred('paid_query', 'research/crt-uniform-rom-query/machine.py') + native = pred('paid_native', 'research/crt-dense-guard-scan/machine.py') + oracle = pred('paid_oracle', 'research/crt-mask-repair-bridge/key_subroutine.py') + crt = pred('paid_crt', 'research/unconditional-batched-crt/check_batched_crt.py') + caller = pred('paid_caller', 'research/crt-mask-repair-bridge/verify.py') + service = load('paid_service', P/'service.py', (P/'service.py').read_bytes()) + return query, native, oracle, crt, caller, service + + +def schedule(crt): + nets = [crt.benes(crt.rotation(8, 5, (2*a)%5 if a<3 else 0)) for a in range(4)] + result = [] + for index in range(5): + target = nets[0][index][0] + need(all(n[index][0] == target for n in nets), 'source common target') + table = [nets[a][index][1][b] for a in range(4) for b in range(8)] + need(all(table[y] == table[y ^ (1 << target)] for y in range(32)), 'source target independence') + result.append((target, table)) + return result + + +def program_bound(query, service, target): + code, marks = service.assemble(query, target) + ranges = tuple(zip(marks['entries'], marks['returns'])) + need(all(end-start == len(query.PROGRAM) for start,end in ranges), 'unaltered full query instruction ranges') + def inside(pc): return any(start <= pc < end for start,end in ranges) + rewinds = 0 + for pc, inst in enumerate(code): + op, *a = inst + if op in ('read', 'write', 'write_reg', 'move'): + need(a[0] in service.ROLES, 'static tape role') + if op in ('write', 'write_reg'): need(a[0] not in ('counter','rom'), 'no borrowed write') + if op == 'read': need(a[0] != 'stream', 'append port never read') + if op == 'move': need(a[1] in (-1,1), 'unit movement') + destinations = a[1:] if op == 'branch' else a if op == 'jump' else [] + for dest in destinations: + need(type(dest) is int and 0 <= dest < len(code), 'fixed control destination') + if dest <= pc and not inside(pc): + need(op == 'jump' and dest == pc-4, 'outside-query loop is one rewind') + read, eq, branch, move, jump = code[pc-4:pc+1] + need(read[0] == 'read' and eq == ('eq','scan','<' if read[1]=='counter' else 'L','test') + and read[1] in ('counter',*service.OWNED_WIDTHS) and read[2] == 'scan' and branch == ('branch','test',pc+1,pc-1) + and move == ('move',read[1],-1) and jump == ('jump',pc-4), 'exact rewind loop syntax') + rewinds += 1 + outside = len(code)-3*len(query.PROGRAM) + bound = 3*512*(32+1)*(4+2+2)**2 + 14*outside + need(bound <= 3_300_000, 'declared complete instruction majorant') + return dict(target=target, static_instructions=len(code), outside_query_instructions=outside, + rewind_loops=rewinds, proved_instruction_bound=bound) + + +def snapshot(tape): + return dict(tape.cells) if isinstance(tape.cells,dict) else dict(enumerate(tape.cells)) + + +def audit(service, initial, initial_heads, expected_status='accept'): + run = service.last; cells = {role:[data.get(i,'_') for i in range(max(data,default=-1)+1)] for role,data in initial.items()} + heads = dict(initial_heads); regs = {}; pc=0; counts=Counter(); halted=False; epochs=[]; interface=0 + returns = set(service.marks['returns']) + for listed_pc, observed in run['events']: + need(not halted and listed_pc==pc, 'instruction/control continuity') + if pc in returns: + y=sum((cells['y'][j+1]=='1') << j for j in range(8)) + epochs.append(dict(y=y, bit=int(cells['out'][1]))) + op,*a=service.program[pc];pc+=1;counts[op]+=1 + if op in ('read','write','write_reg','move'): + role=a[0];head=heads[role];need(head>=0,'nonnegative head') + if role in ('counter','stream'):interface+=1 + if op=='read': + value=cells[role][head] if head=0,'left boundary') + elif op=='set':regs[a[0]]=a[1] + elif op=='copy':regs[a[1]]=regs[a[0]] + elif op=='eq':regs[a[2]]=regs[a[0]]==a[1] + elif op=='eq_reg':regs[a[2]]=regs[a[0]]==regs[a[1]] + elif op in ('xorbit','andbit','orbit'): + need(regs[a[0]] in '01' and regs[a[1]] in '01','single-bit arithmetic operands') + x=regs[a[0]]=='1';y=regs[a[1]]=='1';value=(x^y) if op=='xorbit' else (x&y) if op=='andbit' else (x|y) + regs[a[2]]='1' if value else '0' + elif op=='branch':need(type(regs[a[0]]) is bool,'Boolean branch');pc=a[1] if regs[a[0]] else a[2] + elif op=='jump':pc=a[0] + elif op=='halt':need(a[0]==expected_status,'halt status');halted=True + else:raise ValueError('unknown audit opcode') + need(halted and counts==run['census'] and pc==run['pc'] and regs==run['registers'],'complete independent instruction replay') + for role,tape in run['tapes'].items(): + need(heads[role]==tape.head,'final head replay') + need({i:x for i,x in enumerate(cells[role]) if x!='_'}=={i:x for i,x in snapshot(tape).items() if x!='_'},'final cell replay') + if role in ('counter','rom'):need(cells[role]==[initial[role][i] for i in range(len(initial[role]))] and heads[role]==0,'borrowed restore') + elif role=='stream': + prefix=initial_heads[role];need(cells[role][:prefix]==[initial[role][i] for i in range(prefix)],'protected prefix') + need(heads[role]==prefix+(12 if expected_status=='accept' else 0),'exact append cursor') + if expected_status=='accept':need(all(x in '01' for x in cells[role][prefix:prefix+12]),'twelve appended bits') + else:need(heads[role]==0 and all(x=='_' for x in cells[role]),'private erasure/head return') + return epochs, interface + + +def case(modules,target,table,address,fault='correct',bad_input=None): + query,native,oracle,crt,caller,impl=modules + raw=format(address,'012b') if bad_input is None else bad_input + counter=native.Tape(['<',*raw,'>']);rom=native.Tape(['L',*map(str,table),'R']) + stream=native.Tape(['<',('R',819),('R',17),'_']);stream.head=3 + service=impl.Service(query,target,rom,fault) + roles=dict(service.private,counter=counter,stream=stream,rom=rom) + initial={r:snapshot(t) for r,t in roles.items()};heads={r:t.head for r,t in roles.items()} + meter={'calls':0,'interface_actions':0};before=counter.actions+stream.actions + if bad_input is not None: + try:service.evaluate_key(counter,stream,meter,trace=True) + except ValueError:pass + else:raise ValueError('malformed address admitted') + audit(service,initial,heads,'reject');return None + service.evaluate_key(counter,stream,meter,trace=True) + epochs,interface=audit(service,initial,heads) + need(meter['interface_actions']==interface==counter.actions+stream.actions-before,'interface subset exact') + ref=oracle.ReverseWordKey(target,table);trace=[];original_source=ref.source + def observed(y): + bit=original_source(y);trace.append(dict(y=y,bit=bit));return bit + ref.source=observed;expected=ref.key_of(raw) + actual=''.join(stream.cells[3:15]);need(actual==expected,'literal reverse-word key oracle') + need(epochs==trace,'three current-state query epochs') + need(sum(service.last['census'].values())<=3_300_000,'complete service instruction bound') + return dict(address=address,target=target,key=actual,epochs=epochs, + instructions=sum(service.last['census'].values()),interface_actions=interface, + census=dict(sorted(service.last['census'].items()))),service,initial,heads + + +def must_fail(call,label): + try:call() + except ValueError:return + raise ValueError('undetected control: '+label) + + +def components(modules): + query,native,oracle,crt,caller,impl=modules + bounds=[program_bound(query,impl,t) for t in (0,1,2)] + rows=[];layers=schedule(crt) + addresses=sorted(set([0,1,2,3,4,7,15,31,63,127,128,254,255,256,257,511,512,767,1023,1024,1535,2047,2048,3071,4094,4095]+[(u<<10)|(t<<8)|y for u in range(4) for t in range(4) for y in (3,124,252)])) + for target,table in layers: + for address in addresses:rows.append(case(modules,target,table,address)[0]) + parity=[(x>>1).bit_count()&1 for x in range(32)] + for address in (0,1,3,7,31,127,255,1023,2047,4094,4095):rows.append(case(modules,0,parity,address)[0]) + controls={} + for fault in ('stale','drop_high','omit_clear','omit_rom_return'): + found=False + for address in addresses: + try:case(modules,0,parity,address,fault) + except ValueError: + controls[fault]=address;found=True;break + need(found,'discriminating service mutant '+fault) + for malformed in ('','0'*11,'0'*13,'000000_00000'): + case(modules,0,parity,0,bad_input=malformed) + row,srv,initial,heads=case(modules,0,parity,1023) + events=list(srv.last['events']);index=next(i for i,(pc,_) in enumerate(events) if srv.program[pc][0]=='eq') + srv.last['events']=events[:index]+events[index+1:];must_fail(lambda:audit(srv,initial,heads),'omitted control event') + srv.last['events']=events[:-1];must_fail(lambda:audit(srv,initial,heads),'omitted return event') + return dict(status='PASS_PAID_KEY_COMPONENT',bounds=bounds,accepted_cases=len(rows),rejected_addresses=4, + behavior_mutants=controls,ledger_mutants=2,total_replayed_instructions=sum(r['instructions'] for r in rows), + min_instructions=min(r['instructions'] for r in rows),max_instructions=max(r['instructions'] for r in rows), + cases_sha256=hashlib.sha256(json.dumps(rows,sort_keys=True).encode()).hexdigest(), + source_layers=[{'target':t,'rom':''.join(map(str,table))} for t,table in layers], + service_sha256=hashlib.sha256((P/'service.py').read_bytes()).hexdigest()) + + +def full_caller(modules): + query,native,oracle,crt,caller,impl=modules + env=caller.Env();layers=caller.schedule(env);target,table=layers[2] + rom=env.BitTape(['L',*map(str,table),'R']);service=impl.Service(query,target,rom) + original_bridge=env.bridge.evaluate_key;observed_calls=[] + def paid_port(counter,out,key_function,meter): + # Observer-only address log, required by the unchanged caller assertions. + # It neither chooses an action nor supplies a key to the tape service. + observed=int(''.join(counter.cells[1:13]),2) + observed_calls.append(observed);key_function.__self__.addresses.append(observed) + before=counter.actions+out.actions + prior=meter['interface_actions'];service.evaluate_key(counter,out,meter,trace=False) + need(meter['interface_actions']-prior==counter.actions+out.actions-before,'caller interface accounting subset') + need(counter.head==rom.head==0 and all(t.head==0 and all(x=='_' for x in t.cells.values()) for t in service.private.values()),'per-call service ownership') + env.bridge.evaluate_key=paid_port + result=caller.run_layer(env,list(range(4096)),target,table) + env.bridge.evaluate_key=original_bridge + need(result['final']==result['ideal'],'actual repaired payload equals ideal layer') + own=result['ownership'] + need(own['all_roles_blank'] and own['all_heads_returned'] and own['protected_payload_stream_kept_length'],'full caller ownership') + need(own['good_addresses_evaluated']==own['hole_addresses_missed']==0 and own['key_calls']==result['bad']==own['distinct_key_addresses']==service.calls,'actual source mask exact calls') + need(rom.cells==['L',*map(str,table),'R'] and rom.head==0,'borrowed source ROM unchanged') + cell_actions=sum(service.totals[x] for x in ('read','write','write_reg','move')) + interface=result['meter']['interface_actions'];need(interface<=cell_actions,'interface subset') + return dict(status='PASS_ACTUAL_MIDDLE_LAYER_PAID_KEY',schedule_index=2,target=target,payloads=4096, + calls=service.calls,marked_holes=result['bad'],good_addresses_evaluated=0,hole_addresses_missed=0, + protected_payload_sha256=caller.digest(result['final']),producer_actions=result['producer_actions'], + scanner_actions=result['scanner_actions'],repair_actions_including_key_interface=result['repair_actions'], + key_instructions=sum(service.totals.values()),key_cell_actions=cell_actions,key_interface_actions=interface, + repair_and_key_cell_actions=result['repair_actions']+cell_actions-interface, + key_census=dict(sorted(service.totals.items())),all_roles_blank=True,all_heads_returned=True, + 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=hashlib.sha256((P/'service.py').read_bytes()).hexdigest()) + + +def main(): + parser=argparse.ArgumentParser();parser.add_argument('--part',choices=('components','caller','all'),default='all');parser.add_argument('--write-result',action='store_true');args=parser.parse_args() + modules=sources() + for name,fn,file in [('components',components,'COMPONENT.json'),('caller',full_caller,'CALLER.json')]: + if args.part not in (name,'all'):continue + result=fn(modules) + if args.write_result:(P/file).write_text(json.dumps(result,sort_keys=True,indent=2)+'\n') + else:need(result==json.loads((P/file).read_text()),'frozen '+name+' receipt') + print(json.dumps(result,sort_keys=True),flush=True) + +if __name__=='__main__':main()