diff --git a/research/crt-binary-radix-consumer/PROOF.md b/research/crt-binary-radix-consumer/PROOF.md new file mode 100644 index 0000000000..600822d5a6 --- /dev/null +++ b/research/crt-binary-radix-consumer/PROOF.md @@ -0,0 +1,170 @@ +# A literal binary pass at the CRT repair consumer + +JoyboyBrian, substantial OpenAI Codex assistance; Apache-2.0. + +## Boundary and quantified claim + +Take any n>=0 records `(v_i,k_i)` with `0<=v_i<4096` and nonempty finite +binary key strings k_i. Set K=sum |k_i| and D=n+K. The bad tape is +`< (R,v_1) k_1 ... (R,v_n) k_n >`, followed by blank cells. Each bucket +has just the permanent `<` at cell zero and is otherwise blank. All three +heads start at cell zero. Source symbols use the exact 4104-symbol alphabet +of #4982; in particular, the other eight symbols are `_ L 0 1 R < > =`. +The physical input consists of those symbols' thirteen-bit predecessor +codewords, source cell j at physical cells 13j..13j+12. Codes 8..4095 are +unused and excluded from this entry contract. Misaligned heads, dirty +buckets, missing/duplicate outer markers and arbitrary unused binary codewords are +not admitted inputs. Finite control may initially be arbitrary bits. + +The emitted fixed program returns the stable concatenation of the records +with last key bit zero and then those with last key bit one. Each output +key is rotated from a_1...a_l to a_l a_1...a_(l-1). The payload bits are +opaque and unchanged. The bad tape has exactly the same occupied extent; +its final END stays in source cell D+1. Both buckets become blank except +for their permanent `<`. All heads and all finite-control bits return to +zero. There are three physical tape roles, 72 one-bit control registers, +180 source instructions and 3885 static binary instructions. This is one +fixed program for all n and key lengths, not one program per test input. + +For a finite stream with exactly one LEFT (at cell zero), exactly one +final END, and other symbols in the declared alphabet, validation rejects +any malformed record/key structure before +writing output. It returns the bad head and clears finite control, while +bad and the empty buckets remain unchanged. Missing/duplicate LEFT or END and a nonzero initial head are outside +the contract, not promised rejection cases. Unique LEFT is essential to +the rewind invariant: an interior LEFT would stop a rejection rewind early. + +## Stable symbolic algorithm + +`radix.py` assembles the source algorithm in the unchanged #4752 Builder. +The eight reserved-symbol comparisons recognize a record because the +entry alphabet is precisely the eight reserved symbols plus 4096 records. +No payload value is inspected or used as an address. First validate every +record, followed by at least one key bit, and the final END; all validation +reads only bad. Rewind bad before starting the output. Thus failure cannot +partially change either stream. + +During partition the main invariant is that bad points to the next record +or END, the completed records have appeared in order in their chosen +buckets, and both bucket heads point to the next unused cell. Hold the +payload in one finite register. Walk to the next record/END, step back to +the final key bit, save it, and walk back across the key to its payload. +The key is nonempty, so both scans terminate without crossing LEFT. +Append payload and final bit to its chosen bucket. Hold the first original +key bit; before each further key bit is consumed, append the held bit and +replace it by the current bit. On the first nonbit, the final held bit is +the original final key bit and is deliberately not appended again. This +appends precisely the other l-1 bits and returns bad to the next payload. +This also covers l=1: the inner append loop has no iteration. + +The invariant gives stable order within each bucket, including repeated +keys and repeated payloads. Write an END on each bucket, rewind, and copy +bucket zero followed by bucket one to bad. Exactly D data cells are copied; +write the final END in D+1, then rewind all three. Erase bucket data and +END, return their heads, preserve permanent LEFT. This proves the endpoint +by induction on records and cells. It is the same endpoint as the retained +`bridge.one_pass`, although validation and fixed-control branching have +additional paid work. No assertion about an identical event trace is made. + +If all keys have length L>=1, repeat this same program L times on the same +tapes. Pass j stably sorts on original bit L-j+1 and rotates it to the +front. Induction is the standard stable LSD radix invariant; after L +passes key orientation is restored and order is stable lexicographic +ascending on the original keys. Buckets and control satisfy the next +invocation's entry contract after each pass. The n=0 case also returns. + +## Full source-control and bit-action bill + +A source instruction is one read, write, unit symbol-head move, finite +assignment/copy, equality, branch, jump or halt. There is no host integer +key, length, address lookup, source-cell dictionary access or sort inside +the emitted program. The assembler sees only the predecessor Builder; +it receives no record, parameter n or L. Tape dictionaries, PC indices +and counters in the emulator are observer metadata. + +For the 180-instruction source program, call a transfer backward when its +next PC is no greater than its current PC. Between two backward transfers +the PC strictly increases, so at most 180 instructions execute. The +following are **all** backward transfers on a legal invocation. Bucket +stream lengths D0,D1 satisfy D0+D1=D. Each rewind counts a jump for each +source-cell step left, including the final END position. + +| Control section | Backward transfers | +|---|---:| +| Validation key/next-record branches | K | +| Validation rewind from END | D+1 | +| Right and left key scans | 2K | +| Key rotation append loops | K-n | +| Return to next record | n | +| First three rewinds | 2D+3 | +| Bucket copies | D | +| Second three rewinds | 2D+3 | +| Forward bucket erasure loops | D | +| Final bucket rewinds | D+2 | + +Summing gives exactly B=4K+8D+9, including B=9 for the empty stream. +The rejection rewind is unreachable on a legal input; it is not omitted +from the program. Therefore source execution T satisfies + +`T <= 180*(B+1) = 180*(8n+12K+10)`. + +This bound is constructive and covers validation, comparisons, both +choices of bucket, marker writes, all explicit branches/jumps, merge, +erasure and return. It is deliberately conservative because increasing +PC segments often skip instructions. No measured runtime is used to +prove it. The verifier checks the independent source execution at every +compiled instruction boundary in three fixtures and corroborates the +exact B formula there. + +Use #4982's unchanged `compile_program(..., lifecycle=True)` and bit +machine. Its fourteen-bit tagged registers distinguish symbols from +Booleans. Each core source instruction expands to at most 43 actions: +single-bit read/write, unit physical head move, one-bit assignment/copy, +Boolean operation, branch, jump or halt. The exact local simulation is +retained in its pinned PROOF.md: writes set every one of thirteen bits; +read/write returns to the aligned cell start; a source move is thirteen +unit physical moves; full tagged equality handles destination aliasing. +Our source uses only read/write/move/copy/eq/branch/jump/halt and its +private names avoid `$different` and `$xor`. Every reachable branch +operand is the Boolean result of equality. Hence its induction applies +for every input here, including arbitrary initially dirty finite control. + +Initialization and the reached halt suffix each assign all 72 one-bit +control registers. These 144 actions are paid, not emulator allocation. +Consequently one complete pass costs at most + +`43*180*(8n+12K+10)+144 = 7740*(8n+12K+10)+144` + +literal actions. For fixed width L this is +`7740*(n*(12L+8)+10)+144`. L repeated passes cost at most L times that +quantity. This is a sequential finite-tape bit program bill, not merely a +symbol-cell meter. Static code construction and initial serialization +are outside the invocation contract. They have not become free globally. + +## Actual caller and remaining ledger + +The actual fixture retains #4982's original `bridge.split`, actual raw +middle-layer payloads/mask, two complete bit-level key executions and +continuation to the third marked address. The predecessor fixture closes +the captured completed prefix with END as explicit verifier setup. Our +adapter replaces its subsequent `bridge.one_pass` call, receiving the +**same** `bad.raw`, `b0.raw`, `b1.raw` objects. It neither decodes a key +into a program parameter nor materializes a replacement tape. The +original caller's postchecks inspect payloads, rotated keys and heads; +we also check bucket and control erasure. The enclosing split's symbol +facades remain an unlowered outer boundary. This demonstrates one actual +local connection, not complete repair or production geometry admission. + +| Obligation | Status | +|---|---| +| Stable consumer action and cleanup for all valid finite encoded streams | proved here; explicit finite upper bound | +| Inherited thirteen-bit compiler's block simulation | retained pinned premise; observer corroboration here | +| Original two key calls and continuation before new consumer | executed bounded fixture, predecessor source proof retained | +| Full 2944-hole layer and complete sort/reinsert | unrun; not discharged by the captured prefix | +| Split/reinsert binary control, uniform geometry and descriptor/ROM construction | unknown here | +| Physical tape placement, whole CRT tariff E(p,ell), compiler creation cost and all-size supplier transfer | unknown here | + +No new kappa, selected supplier, complete multiplication theorem, native +implementation or formal proof-kernel acceptance follows. The declared +family decision is narrow: close this explicit consumer boundary and +stop, rather than authorize an automatic full-repair expansion. diff --git a/research/crt-binary-radix-consumer/README.md b/research/crt-binary-radix-consumer/README.md new file mode 100644 index 0000000000..7f61d55f82 --- /dev/null +++ b/research/crt-binary-radix-consumer/README.md @@ -0,0 +1,128 @@ +# A literal binary radix consumer for the CRT repair stream + +This closes **Open next question 1 of [PR4982](https://github.com/CrocSwap/integer-mult-bounds/pull/4982)**: +execute the next actual sparse-repair consumer in bit control. The fixed +[program](radix.py) uses the unchanged predecessor compiler/bit machine to +lower the retained `bridge.one_pass` stable-radix algorithm. The entry +representation, payload semantics and actual caller are preserved. + +The [written proof](PROOF.md) covers **every finite stream** with n opaque +12-bit payloads and nonempty binary keys of total length K. One pass has +complete literal bit-action bound + +``` +7740 * (8*n + 12*K + 10) + 144. +``` + +It includes framing validation, all bit reads/writes and unit head moves, +finite Boolean/control steps, stable bucket partition/merge, bucket erasure, +head return, and initialization/erasure of all 72 finite-control bits. +For equal key width L, L repeated passes stably sort the full keys and +restore their orientation. This is an explicit finite-tape program and a +uniform source-control proof, not an extrapolation of a symbolic cell meter. + +The program is static: 180 source instructions, 3885 binary instructions, +three tape roles, and no input n, L, key integer or decoded stream in the +assembler/executor. It recognizes opaque records using the declared source +alphabet, without inspecting their payload value. Entry requires aligned +13-bit predecessor codewords and clean owned buckets. Unused codewords, +dirty buckets, missing/duplicate outer markers and misaligned entry heads are outside this +port contract. Record/key grammar errors inside a uniquely LEFT/END-framed +stream reject +before output, preserving the borrowed input and clearing finite control. + +## Evidence + +[RESULT.json](RESULT.json) records these independent endpoint/representation +checks, executed in both ordinary and optimized Python: + +- All 371 streams with up to four one-bit-key records, or two keys of width + one through four; both empty buckets, all-zero/all-one partitions and + duplicate keys are covered. Distinct payloads detect loss of stability. +- Three complete source-instruction-boundary simulations against the + predecessor's independently represented source semantics. Every physical + head scale, register result and written codeword matches. The exact + backward-transfer counts corroborate the all-size control proof. +- Complete stable sorting through three and 37 passes, width-one keys, + payload boundary values 0/4095 and variable positive key lengths for a + single pass. Every legal endpoint also matches the original literal + `bridge.one_pass` and an independent stable sort/rotation oracle. +- Five faults reject: reverse bucket order, wrong key rotation, retained + bucket data, short physical cell strides and omitted control erasure. + Eight malformed uniquely framed packets reject with borrowed data and bucket + preservation, returned heads and cleared control. +- **Actual source caller connection:** original `bridge.split` emits two + completed pairs through the real bit-level key service, then continues + to the third marked address. Its completed prefix is explicitly closed + by verifier setup. The new radix consumer receives those **same physical + tape objects**, uses 37,969 actions, and returns the expected payloads, + key rotations, heads, blank buckets and cleared control. The outer + caller's facades remain an unlowered boundary. No whole layer is implied. + +Finite tests corroborate the quantified written proof; they are not formal +kernel verification. The static 43-action compiler-block simulation is a +pinned predecessor premise. This package adds source-control proof and +consumer/caller checks instead of rerunning its complete alphabet census. + +## Reproduce + +From the repository root, Python 3.12, standard library only: + +```sh +python3.12 -B scripts/research_package.py --package research/crt-binary-radix-consumer --check-only +python3.12 -B scripts/research_package.py --package research/crt-binary-radix-consumer +``` + +The registered hook runs ordinary and optimized checks, authenticates all +thirteen live inputs and compares every proof-relevant receipt field. +Direct `verify.py` replay also works in the package's standard Git-free +export; `--write-result` alone regenerates its receipt. + +## Family decision, sources and overlap + +**Narrow, then stop:** this is one named actual-consumer obligation. Full +binary split/reinsert, physical descriptor and ROM production, variable CRT +geometry, compiler creation/serialization and whole CRT E(p,ell) remain +unknown. The inherited fixed key fixture does not become a uniform key +compiler. No complete 2944-hole layer, historical suite, Lean/Docker or +selected supplier replay is run. No new kappa or selected-frontier change +is claimed. + +[SOURCES.json](SOURCES.json) pins canonical base +`bee95ce88f9f19802f0613f92838895cd0e14a1f`, priority revision 7, and all +imported source bytes. The key/binary predecessor is PR4982 at +`67154122b2867e6dee5b9b25f2f1c862a3e81e95`; its PROOF.md supplies the +compiler simulation. The original bridge and key/source lineage remain +unchanged. Pending PR4990 supplies a two-target unary stencil, a different +producer boundary. Symbol-level repair and abstract radix predecessors +already supply stable sorting; that algorithm is not claimed as new. + +Initial overlap covered all 6690 current tracked notes, 310 open/draft PR +bodies at 2026-10-23 06:05:59 UTC and 4096 Discussion records at 06:06:48 +UTC, with complete inventory/pagination. The targeted `one_pass`/`binary` +search found only PR4982's README/TASK and its canonical result. Arbitrary +diffs and unpublished work remain outside coverage; no novelty guarantee +is claimed. Canonical coordination is [Discussion4709](https://github.com/CrocSwap/integer-mult-bounds/discussions/4709#discussioncomment-19139345); [TASK.json](TASK.json) +retains the scoped card, stopping rule and next questions. + +## Open next questions + +1. Specify one complete actual encoded split/sort/reinsert caller, with its + transport and restoration obligations, before expanding implementation. + This decides whether local stages can share one complete paid invoice. +2. Specify the encoded variable-geometry key/ROM producer and its lifecycle + allowance. A different finite key seed would not resolve the current + uniform producer/serialization gap. + +The structured questions and blockers are in TASK.json. Neither is claimed +or implicitly assigned by this package. + +## Credit + +Prepared by JoyboyBrian with substantial OpenAI Codex assistance; Apache-2.0. +Retain PR4982/PR4795/PR4752 authorship and the original PR4637 scanner/repair +lineage: Cinna Davis, ToikY, Hiroki KUMAZAKI, Ryanson Jonathan, unpaidmoon, +Jose Manuel, Douglas Colkitt and John-Michael Smith (PR763 lineage). The +[source-specific notice](../unconditional-batched-crt/NOTICE.md) remains in +its declared source inputs. All frozen predecessors are unchanged. No +independent human or formal proof-kernel acceptance is claimed. diff --git a/research/crt-binary-radix-consumer/RESULT.json b/research/crt-binary-radix-consumer/RESULT.json new file mode 100644 index 0000000000..3ec3147a38 --- /dev/null +++ b/research/crt-binary-radix-consumer/RESULT.json @@ -0,0 +1,124 @@ +{ + "actual_caller": { + "calls": [ + { + "address": 0, + "binary_actions": 859622, + "key": "000000000000", + "payload": 0 + }, + { + "address": 1, + "binary_actions": 859888, + "key": "000000000001", + "payload": 1 + } + ], + "consumer": "new binary radix pass on same physical tapes of two completed captured pairs", + "continued_to_address": 2, + "full_layer_replayed": false, + "radix": { + "binary_actions": 37969, + "same_physical_tapes": true + }, + "source_target": 2 + }, + "behavior_controls": [ + "reverse_buckets", + "wrong_rotation", + "keep_buckets", + "short_move", + "keep_control" + ], + "binary_envelope": "43*180*(8*n+12*K+10)+144", + "binary_instructions": 3885, + "bit_registers": 72, + "complete_bounded_cases": 371, + "examples": [ + { + "actions": 51609, + "audited_backward_edges": 361, + "audited_source_steps": 2483, + "key_cells": 24, + "passes": 1, + "records": 8 + }, + { + "actions": 5977, + "audited_backward_edges": 29, + "audited_source_steps": 268, + "key_cells": 1, + "passes": 1, + "records": 1 + }, + { + "actions": 2541, + "audited_backward_edges": 9, + "audited_source_steps": 105, + "key_cells": 0, + "passes": 1, + "records": 0 + }, + { + "actions": 154739, + "audited_backward_edges": 0, + "audited_source_steps": 0, + "key_cells": 24, + "passes": 3, + "records": 8 + }, + { + "actions": 4046357, + "audited_backward_edges": 0, + "audited_source_steps": 0, + "key_cells": 74, + "passes": 37, + "records": 2 + }, + { + "actions": 19447, + "audited_backward_edges": 0, + "audited_source_steps": 0, + "key_cells": 8, + "passes": 1, + "records": 3 + } + ], + "program_sha256": "f4200a495d9c445474275214254d46e9a8e03967a635263905a4c9192bb36f1f", + "rejections": [ + { + "actions": 1006, + "status": "reject" + }, + { + "actions": 550, + "status": "reject" + }, + { + "actions": 1323, + "status": "reject" + }, + { + "actions": 1911, + "status": "reject" + }, + { + "actions": 506, + "status": "reject" + }, + { + "actions": 1006, + "status": "reject" + }, + { + "actions": 1675, + "status": "reject" + }, + { + "actions": 462, + "status": "reject" + } + ], + "source_instructions": 180, + "status": "PASS_LITERAL_BINARY_RADIX_CONSUMER" +} diff --git a/research/crt-binary-radix-consumer/SOURCES.json b/research/crt-binary-radix-consumer/SOURCES.json new file mode 100644 index 0000000000..6951fb3a04 --- /dev/null +++ b/research/crt-binary-radix-consumer/SOURCES.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "base_commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "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-binary-key-port/PROOF.md", + "usage": "input", + "git_blob": "c7bffebbc1cef2420e2ba910b4cbf6e9b3110994", + "sha256": "c1fb60178576f64f170c1c0867c2a109c15a993a7bdc3ad52e1ff70c8a58faa0" + }, + { + "path": "research/crt-binary-key-port/SOURCES.json", + "usage": "input", + "git_blob": "27b3e26f723ceb5ab0c573b0ede7cbead54a04be", + "sha256": "dcc5e8d0bf7b64fd93261e953d4d9b32db87e9a75afd6d775dd7fba2cad48c7d" + }, + { + "path": "research/crt-binary-key-port/binary.py", + "usage": "input", + "git_blob": "ec574f26d6f64ead00d7c2cf5b808c0498b460cf", + "sha256": "50a3dea7fc087715b4e605e85629566ed31903026540f916df6b8cbaa536182d" + }, + { + "path": "research/crt-binary-key-port/verify.py", + "usage": "input", + "git_blob": "eb93b173a8aa9f386be9d6fcf523ecfaff7dc443", + "sha256": "6b97737ad6901b8b49d13db5d75b9102147d77693e8c1966b0d97b3347384748" + }, + { + "path": "research/crt-dense-guard-scan/machine.py", + "usage": "input", + "git_blob": "ce763898bd7b4401bbab818c640a0593b65c9a82", + "sha256": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7" + }, + { + "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-paid-key-service/PROOF.md", + "usage": "input", + "git_blob": "a0b84e8d3bd80d760a1be9e801fc57939b6f24e9", + "sha256": "1a4ac02653eb6c1b20807033a910f27bf9484cc972bf2629941f589275a87325" + }, + { + "path": "research/crt-paid-key-service/service.py", + "usage": "input", + "git_blob": "726d9523ab7dd4a16697f9201b0224f2da1f2517", + "sha256": "ff06c6305c9f650a694e5c42baa4c7d841decf844a4f44f6776acc10a8400083" + }, + { + "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/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" + } + ] +} diff --git a/research/crt-binary-radix-consumer/TASK.json b/research/crt-binary-radix-consumer/TASK.json new file mode 100644 index 0000000000..4eef330e5f --- /dev/null +++ b/research/crt-binary-radix-consumer/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "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": "Close PR4982 Open next question 1: emit and execute the actual CRT stable-radix consumer in literal binary control, with a uniform all-stream action bound and restored bucket/control lifecycle.", + "scope_change_reason": "The generic all-size audit is narrowed to the named actual-consumer gap after the fixed-geometry key port. It changes the executed outer boundary rather than enlarging its finite key census.", + "bottleneck_link": "Sorting is part of CRT total repair; the source key service leaves its consumer symbol-decoded. A literal complete local consumer supplies one missing fixed-tape implication, while full repair/producer and tariff obligations remain unknown.", + "budget_minutes": 60, + "stop_rule": "Stop after the source-bound radix-consumer theorem, actual key-return fixture and complete local action/cleanup ledger. Do not automatically expand to a whole repair layer.", + "outcome": "completed", + "evidence": "PROOF.md; RESULT.json; 371 complete small stream cases, source-boundary and literal original consumer checks, actual same-tape split/key/radix fixture, rejection and behavioral controls.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance with design, implementation, proof, verification and documentation; no independent human or proof-kernel review claimed.", + "open_questions": [ + { + "question": "Which actual CRT caller can supply a fully encoded split/sort/reinsert boundary and pay all transport and restoration?", + "why_it_matters": "This consumer closes one local binary stage, not the whole CRT repair tariff.", + "first_step": "Specify one complete actual caller with encoded input/output roles and price split and reinsertion before another implementation expansion.", + "blocked_by": "Unlowered outer split/reinsert and descriptor/ROM production; no common full bit-step invoice." + }, + { + "question": "Can a variable-geometry key producer return the same 13-bit stream without external serialization?", + "why_it_matters": "The retained key service is fixed u2,t2,y8 whereas this consumer supports arbitrary finite stream and key lengths.", + "first_step": "State the encoded parameter/ROM producer contract and full lifecycle allowance, then test one nontrivial changed geometry.", + "blocked_by": "No uniform physical key/ROM construction or initial serialization cost is supplied here." + } + ] +} diff --git a/research/crt-binary-radix-consumer/VERIFY.json b/research/crt-binary-radix-consumer/VERIFY.json new file mode 100644 index 0000000000..d62d5b43c3 --- /dev/null +++ b/research/crt-binary-radix-consumer/VERIFY.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/crt-binary-key-port/PROOF.md", + "research/crt-binary-key-port/SOURCES.json", + "research/crt-binary-key-port/binary.py", + "research/crt-binary-key-port/verify.py", + "research/crt-dense-guard-scan/machine.py", + "research/crt-mask-repair-bridge/bridge.py", + "research/crt-mask-repair-bridge/key_subroutine.py", + "research/crt-paid-key-service/PROOF.md", + "research/crt-paid-key-service/service.py", + "research/crt-uniform-rom-query/PROOF.md", + "research/crt-uniform-rom-query/machine.py", + "research/unconditional-batched-crt/NOTICE.md", + "research/unconditional-batched-crt/check_batched_crt.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Pinned source authentication, source-instruction boundary simulation and exact loop census, complete small key domains, original one_pass and independent stable-sort endpoints, physical caller continuation, lifecycle, five behavioral faults, eight uniquely framed grammar rejections and frozen receipt." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "All controls and exact frozen receipt again with assertions disabled." + } + ] +} diff --git a/research/crt-binary-radix-consumer/radix.py b/research/crt-binary-radix-consumer/radix.py new file mode 100644 index 0000000000..f558019fe7 --- /dev/null +++ b/research/crt-binary-radix-consumer/radix.py @@ -0,0 +1,92 @@ +"""Finite assembly for the retained CRT stable radix pass. + +JoyboyBrian with substantial OpenAI Codex assistance. Apache-2.0. +The assembler receives the predecessor Builder, never a stream or its length. +""" + +RESERVED = ('_', 'L', '0', '1', 'R', '<', '>', '=') + + +def assemble(query, fault=None): + b = query.Builder(); e = b.emit + + def jump(label): e('jump', label) + + def rewind(tape): + loop, done, back = (b.new(x) for x in ('rewind', 'home', 'back')) + b.mark(loop); e('read', tape, 'scan') + b.branch('scan', '<', done, back) + b.mark(back); e('move', tape, -1); jump(loop) + b.mark(done) + + def bit(reg, yes, no): + other = b.new('maybe_one') + b.branch(reg, '0', yes, other) + b.mark(other); b.branch(reg, '1', yes, no) + + def record(reg, yes, no): + # The entry alphabet is the authenticated predecessor's 4104 symbols. + for symbol in RESERVED: + more = b.new('record_next') + b.branch(reg, symbol, no, more); b.mark(more) + jump(yes) + + def erase(tape): + loop, more, end = (b.new(x) for x in ('erase', 'erase_more', 'erase_end')) + e('move', tape, 1); b.mark(loop); e('read', tape, 'scan') + e('write', tape, '_'); b.branch('scan', '>', end, more) + b.mark(more); e('move', tape, 1); jump(loop) + b.mark(end); rewind(tape) + + # Validate the whole framed stream before changing any output cell. + e('move', 'bad', 1) + b.mark('validate_record'); e('read', 'bad', 'scan') + b.branch('scan', '>', 'validated', 'validate_payload') + b.mark('validate_payload'); record('scan', 'validate_key_first', 'reject') + b.mark('validate_key_first'); e('move', 'bad', 1); e('read', 'bad', 'scan') + bit('scan', 'validate_key_more', 'reject') + b.mark('validate_key_more'); e('move', 'bad', 1); e('read', 'bad', 'scan') + bit('scan', 'validate_key_more', 'validate_record') + b.mark('validated'); rewind('bad') + for tape in ('bad', 'b0', 'b1'): e('move', tape, 1) + + b.mark('outer'); e('read', 'bad', 'payload') + b.branch('payload', '>', 'buckets_done', 'find_last') + b.mark('find_last'); e('move', 'bad', 1) + b.mark('seek_end'); e('read', 'bad', 'scan') + bit('scan', 'seek_more', 'at_end') + b.mark('seek_more'); e('move', 'bad', 1); jump('seek_end') + b.mark('at_end'); e('move', 'bad', -1); e('read', 'bad', 'last') + b.mark('seek_payload'); e('read', 'bad', 'scan') + bit('scan', 'seek_back', 'choose_bucket') + b.mark('seek_back'); e('move', 'bad', -1); jump('seek_payload') + b.mark('choose_bucket'); b.branch('last', '1', 'append_b1', 'append_b0') + + for tape in ('b0', 'b1'): + loop, more, done = (b.new(x) for x in ('append_loop', 'append_more', 'append_done')) + b.mark('append_' + tape) + e('write_reg', tape, 'payload'); e('move', tape, 1) + e('write_reg', tape, 'last'); e('move', tape, 1) + e('move', 'bad', 1); e('read', 'bad', 'held'); e('move', 'bad', 1) + b.mark(loop); e('read', 'bad', 'scan'); bit('scan', more, done) + b.mark(more); e('write_reg', tape, 'last' if fault == 'wrong_rotation' else 'held'); e('move', tape, 1) + e('copy', 'scan', 'held'); e('move', 'bad', 1); jump(loop) + b.mark(done); jump('outer') + + b.mark('buckets_done') + for tape in ('b0', 'b1'): e('write', tape, '>') + for tape in ('bad', 'b0', 'b1'): rewind(tape) + e('move', 'bad', 1) + for tape in (('b1', 'b0') if fault == 'reverse_buckets' else ('b0', 'b1')): + loop, more, done = (b.new(x) for x in ('copy', 'copy_more', 'copy_done')) + e('move', tape, 1); b.mark(loop); e('read', tape, 'scan') + b.branch('scan', '>', done, more) + b.mark(more); e('write_reg', 'bad', 'scan'); e('move', 'bad', 1) + e('move', tape, 1); jump(loop); b.mark(done) + e('write', 'bad', '>') + for tape in ('bad', 'b0', 'b1'): rewind(tape) + if fault != 'keep_buckets': + for tape in ('b0', 'b1'): erase(tape) + e('halt', 'accept') + b.mark('reject'); rewind('bad'); e('halt', 'reject') + return b.finish() diff --git a/research/crt-binary-radix-consumer/verify.py b/research/crt-binary-radix-consumer/verify.py new file mode 100644 index 0000000000..19749b259a --- /dev/null +++ b/research/crt-binary-radix-consumer/verify.py @@ -0,0 +1,169 @@ +"""Source-bound bit execution, original consumer and independent stable oracle. + +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. +All symbol decoding, key sorting and integer arithmetic below are observer-only. +""" +import argparse +from collections import Counter +import hashlib +import itertools +import json +from pathlib import Path +import sys +import types + +P = Path(__file__).resolve().parent +ROOT = P.parents[1] + + +def need(ok, message): + if not ok: raise ValueError(message) + + +def load(name, path): + m = types.ModuleType(name); m.__file__ = str(path); sys.modules[name] = m + exec(compile(path.read_bytes(), str(path), 'exec'), m.__dict__) + return m + + +def modules(): + 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') + old = load('radix_predecessor_observer', ROOT/'research/crt-binary-key-port/verify.py') + mod = old.modules() + mod['old'] = old; mod['radix'] = load('radix_program', P/'radix.py') + return mod + + +class SymbolTape: + def __init__(self, symbols): self.cells = dict(enumerate(symbols)); 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 + + +def symbols(rows): return ['<', *[x for value, key in rows for x in [('R', value), *key]], '>'] + + +def canonical_cells(cells): return {k:v for k,v in cells.items() if v} + + +def bit_expected(old, stream): return canonical_cells(dict(enumerate(old.packet(stream)))) + + +def run(mod, rows, *, audit=False, fault=None, repeated=1, malformed=None): + old, b = mod['old'], mod['binary'] + source = mod['radix'].assemble(mod['query'], fault) + program, starts, regs = b.compile_program(source, 'short_move' if fault == 'short_move' else 'keep_control' if fault == 'keep_control' else None, lifecycle=True) + incoming = symbols(rows) if malformed is None else malformed + tapes = {'bad':b.BitTape(old.packet(incoming)), 'b0':b.BitTape(old.packet(['<'])), 'b1':b.BitTape(old.packet(['<']))} + originals = [SymbolTape(incoming), SymbolTape(['<']), SymbolTape(['<'])] + want = list(rows); lengths = [len(key) for _,key in rows] + d = sum(1+length for length in lengths) + totals = Counter(); source_steps = backward = 0 + for invocation in range(repeated): + machine = b.Machine(program, len(regs), tapes); machine.registers[:] = [1]*len(regs) + before_steps, before_backward = source_steps, backward + if audit: + state = (0, {}, {role:dict(enumerate(incoming if role == 'bad' else ['<'])) for role in tapes}, dict.fromkeys(tapes,0)) + for _ in range(starts[0]): machine.step() + while machine.status is None: + pc = state[0]; op,*args = source[pc] + need(machine.pc == starts[pc], 'relocated source control boundary') + state = old.source_step(source, state) + for _ in range(starts[pc+1]-starts[pc]): machine.step() + source_steps += 1; backward += int(state[0] <= pc) + if op != 'halt': need(machine.pc == starts[state[0]], 'source next PC') + for role in tapes: need(tapes[role].head == 13*state[3][role], 'unit-move head scaling') + if op in ('write', 'write_reg'): + role = args[0]; cell = state[3][role] + need(old.physical_word(tapes[role],cell) == old.encode(state[2][role][cell]), 'complete dirty word write') + dest = args[1] if op in ('read','copy') else args[0] if op == 'set' else args[2] if op in ('eq','eq_reg') else None + if dest is not None: need(old.observe_register(machine,regs,dest) == old.encode_value(state[1][dest]), 'independent register semantics') + else: + # A failed movement mutant may not terminate; the observer watchdog is not machine work. + for _ in range(2_000_000): + if machine.status is not None: break + machine.step() + need(machine.status is not None, 'observer watchdog; no accepted execution') + need(not any(machine.registers), 'finite control is explicitly erased') + need(all(t.head == 0 for t in tapes.values()), 'all heads returned') + if malformed is not None: + need(machine.status == 'reject', 'malformed framing rejected') + need(tapes['bad'].cells == bit_expected(old,incoming), 'rejection preserves borrowed input') + need(all(tapes[r].cells == bit_expected(old,['<']) for r in ('b0','b1')), 'rejection preserves empty buckets') + return dict(status='reject', actions=sum(machine.census.values())) + need(machine.status == 'accept', 'accept legal stream') + # Independent mathematical oracle; stable sort is observer-only. + want = [(v,k[-1]+k[:-1]) for v,k in sorted(want,key=lambda row:row[1][-1])] + mod['bridge'].one_pass(*originals, frozenset()) + need(tapes['bad'].cells == bit_expected(old,symbols(want)), 'independent stable rotation endpoint') + for role, tape in zip(('bad','b0','b1'), originals): + expected = {i:v for i,v in enumerate(old.packet([tape.cells.get(j,'_') for j in range(max(tape.cells)+1)])) if v} + need(tapes[role].cells == expected and tapes[role].head == 13*tape.head, 'literal original one_pass endpoint') + need(all(tapes[r].cells == bit_expected(old,['<']) for r in ('b0','b1')), 'owned bucket contents erased') + actions = sum(machine.census.values()); totals.update(machine.census) + need(actions <= 43*len(source)*(8*len(rows)+12*sum(lengths)+10)+2*len(regs), 'proved full binary envelope') + if audit: + need(backward-before_backward == 4*sum(lengths)+8*d+9, 'exact proof backward-transfer count') + need(source_steps-before_steps <= len(source)*(backward-before_backward+1), 'strictly increasing PC segments') + incoming = symbols(want) + if repeated and lengths and len(set(lengths)) == 1 and repeated == lengths[0]: + need(want == sorted(rows,key=lambda row:row[1]), 'complete stable LSD sort, original key orientation') + return dict(records=len(rows), key_cells=sum(lengths), passes=repeated, actions=sum(totals.values()), audited_source_steps=source_steps, audited_backward_edges=backward) + + +def actual_caller(mod): + saved = mod['bridge'].one_pass; rows = [] + source = mod['radix'].assemble(mod['query']) + program,_,regs = mod['binary'].compile_program(source,lifecycle=True) + def invoke(bad,b0,b1,flags): + need(not flags,'actual caller has ordinary flags') + machine = mod['binary'].Machine(program,len(regs),{'bad':bad.raw,'b0':b0.raw,'b1':b1.raw}) + machine.registers[:] = [1]*len(regs); machine.run() + need(machine.status == 'accept' and not any(machine.registers), 'same-tape actual binary consumer') + need(all(t.raw.head == 0 for t in (bad,b0,b1)), 'actual consumer head return') + need(all(t.raw.cells == bit_expected(mod['old'],['<']) for t in (b0,b1)), 'actual consumer bucket erasure') + rows.append(dict(binary_actions=sum(machine.census.values()),same_physical_tapes=True)) + mod['bridge'].one_pass = invoke + try: observed = mod['old'].caller_port(mod) + finally: mod['bridge'].one_pass = saved + need(len(rows) == 1, 'actual caller invokes new consumer') + observed['consumer'] = 'new binary radix pass on same physical tapes of two completed captured pairs' + observed['radix'] = rows[0] + return observed + + +def main(): + ap=argparse.ArgumentParser();ap.add_argument('--write-result',action='store_true');args=ap.parse_args() + mod=modules(); source=mod['radix'].assemble(mod['query']) + program,starts,regs=mod['binary'].compile_program(source,lifecycle=True) + need(max(starts[i+1]-starts[i] for i,x in enumerate(source) if x[0]!='halt')==43,'inherited compiler maximum') + fixture=[(4095,'101'),(0,'000'),(18,'001'),(234,'001'),(3,'111'),(51,'010'),(1024,'100'),(5,'011')] + examples=[run(mod,fixture,audit=True),run(mod,[(4095,'1')],audit=True),run(mod,[],audit=True),run(mod,fixture,repeated=3)] + # All words up to four records for one-bit keys; all two-record keys through width four. + cases=0 + for n in range(5): + for keys in itertools.product(('0','1'),repeat=n): + run(mod,[(4095-i,key) for i,key in enumerate(keys)]);cases+=1 + for width in range(1,5): + keys=[format(i,f'0{width}b') for i in range(2**width)] + for k0,k1 in itertools.product(keys,repeat=2): + run(mod,[(0,k0),(4095,k1)]);cases+=1 + examples.extend([run(mod,[(21,'0'*37),(22,'1'*37)],repeated=37),run(mod,[(1,'1'),(2,'01010'),(3,'00')])]) + malformed=[['<',('R',0),'>'],['<','0','>'],['<',('R',0),'0','_','>'],['<',('R',0),'1',('R',1),'>'],['<','L','>'],['<',('R',0),'R','>'],['<',('R',0),'1','=','>'],['<','_','>']] + rejects=[run(mod,[],malformed=row) for row in malformed] + controls=[] + for fault in ('reverse_buckets','wrong_rotation','keep_buckets','short_move','keep_control'): + try:run(mod,fixture,fault=fault) + except (ValueError,KeyError,IndexError):controls.append(fault) + else:raise ValueError('missed behavioral fault '+fault) + result=dict(status='PASS_LITERAL_BINARY_RADIX_CONSUMER',source_instructions=len(source),binary_instructions=len(program),bit_registers=len(regs),binary_envelope=f'43*{len(source)}*(8*n+12*K+10)+{2*len(regs)}',complete_bounded_cases=cases,examples=examples,rejections=rejects,behavior_controls=controls,actual_caller=actual_caller(mod),program_sha256=hashlib.sha256((P/'radix.py').read_bytes()).hexdigest()) + if args.write_result:(P/'RESULT.json').write_text(json.dumps(result,sort_keys=True,indent=2)+'\n') + else:need(json.dumps(result,sort_keys=True)==json.dumps(json.loads((P/'RESULT.json').read_text()),sort_keys=True),'frozen result drift') + print(json.dumps(result,sort_keys=True)) + +if __name__=='__main__':main()