diff --git a/docs/ci-verification.md b/docs/ci-verification.md index 63ba3e9aa8..52b62d0481 100644 --- a/docs/ci-verification.md +++ b/docs/ci-verification.md @@ -1,8 +1,25 @@ # CI verification -## Current selected-family replay: #6030 +## Current selected-family replay: #7000 with #7001 The [selected record](../certificates/selected-result.json) binds conditional +κ = 0.00363005817 to the [application review](research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md), +[validation receipts](research/pr-intake-evidence/pr7000-application/VALIDATION.json), +and [explicit source closure](../certificates/frontier7000-source.json). +`make frontier7000-verify` follows that exact-source selected replay. The review +reuses eleven authenticated preceding executions and records seven fresh serial +application, scalar and complete native-catalogue executions. The earlier +monolithic timeout is retained separately and is not completed coverage. +Consult the receipts for exact commands, source heads and limits. + +The five inherited framework assumptions remain. No complete uniform word, +literal multiplier execution, independent human proof or formal-kernel proof +is asserted. Routine research submissions do not need to rerun this +selected-family replay. The sections below preserve historical checkpoints. + +## Historical selected-family replay: #6030 + +The [historical checkpoint](../certificates/checkpoints/frontier6030.json) binds conditional κ = 0.003125804 to the [proof review](research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md), [validation receipts](research/pr-intake-evidence/pr6030-audit/VALIDATION.json), and [explicit source closure](../certificates/frontier6030-source.json). diff --git a/research/encoded-crt-leaf-payload/INPUT-PINS.json b/research/encoded-crt-leaf-payload/INPUT-PINS.json new file mode 100644 index 0000000000..41f6f41c98 --- /dev/null +++ b/research/encoded-crt-leaf-payload/INPUT-PINS.json @@ -0,0 +1,115 @@ +{ + "base": "e54523517d0f03e58352e647c403a5af3e525a57", + "canonical": [ + { + "path": "research/r437-preparation-composition/predecessor4025/source/words.py", + "sha256": "5c37f57708ba3131bdcb03139f9dbc29886bee44569c09cbba51b68f75acd7f9", + "git_blob": "8d4ba37e2778acb35b34e0719df2caf138fbeb50", + "bytes": 13794 + }, + { + "path": "research/r437-preparation-composition/predecessor4025/source/records.py", + "sha256": "0c9c4b23e998597fb877bb1a29da69ac869b68262abe635b162b4dba9c69b372", + "git_blob": "4f00467a0ff580954ad2fd0c7380240c753ddef3", + "bytes": 9888 + }, + { + "path": "research/encoded-crt-entry-lifecycle/entry.py", + "sha256": "0537ec98f306270c8ff6a424841886cf53f675d9947029347090c7dc779616d7", + "git_blob": "1fa2b0cb88320d4f5b623554bb0fc6de332b773c", + "bytes": 6377 + }, + { + "path": "research/encoded-current-crt/producer.py", + "sha256": "88dab4ca02a92164a67826db361214fa1405e4b4a588f8c4279a21bcee95ab76", + "git_blob": "a327b0161eca57a1cc44ec2aa8e3defed2167ddc", + "bytes": 7891 + }, + { + "path": "research/crt-persistent-numerical-owner/owner.py", + "sha256": "1d73f432f8de9c791260c43335eb207d82bbb3f5b190cc76d0d914a4db076f41", + "git_blob": "20ef3519b6fef691ec92b7315e320b5e8ce9bf18", + "bytes": 2980 + }, + { + "path": "research/crt-mixed-row-entry/bridge.py", + "sha256": "89c38638c0d66da731566c903c32e7fa1ad31088d29cfd2634fce823dd07c1f9", + "git_blob": "57f6853e262a6136bc616f1e47a31d0ace28495c", + "bytes": 3864 + }, + { + "path": "research/crt-current-row-query/join.py", + "sha256": "11c9ac1175a45edae80869b22c041e31a1b5cc75f4389ec2e073de37e547bf35", + "git_blob": "676582b4a376db375237ec52df84a3ddaf231827", + "bytes": 9955 + }, + { + "path": "research/crt-encoded-benes-rom-producer/microcode.py", + "sha256": "d4af5350854a87b67484840800b94e1e53cff82c78ec0f2a91753fed9ea70af7", + "git_blob": "052b01a83bc910c176b83a012b9f46f0e9525b9d", + "bytes": 23823 + }, + { + "path": "research/crt-uniform-rom-query/machine.py", + "sha256": "46ee6a635251e498ee9a5d4aff8c0e2a7f1ef2ff951e5b6a2a8953316e9cd02d", + "git_blob": "88292ce98d31d540c7dba6960bfe4c19f06a8077", + "bytes": 12431 + }, + { + "path": "research/crt-binary-key-port/binary.py", + "sha256": "50a3dea7fc087715b4e605e85629566ed31903026540f916df6b8cbaa536182d", + "git_blob": "ec574f26d6f64ead00d7c2cf5b808c0498b460cf", + "bytes": 5658 + }, + { + "path": "research/crt-binary-radix-consumer/radix.py", + "sha256": "f4200a495d9c445474275214254d46e9a8e03967a635263905a4c9192bb36f1f", + "git_blob": "f558019fe70c46bcb2f087464c1d2aa021b7188d", + "bytes": 4072 + }, + { + "path": "research/crt-paid-row-reentry/RESULT.json", + "sha256": "d818bffac4647dffaf525ed68dbb79dc575a00303af3315c6d4fe39b60f49a13", + "git_blob": "832d3312df223d1b151e5c620cc3d4e295f49e05", + "bytes": 15482 + } + ], + "retained": [ + { + "path": "research/encoded-balanced-crt-inverse/source/research/encoded-balanced-crt-entry/frontend.py", + "sha256": "6ec9aab626a9d7a229b6f13ce6863e1ca77fa30ef65a4a66ae03a6ffaf2ee78c", + "git_blob": "8adbe2cfef74da9854ed0b70b6c221f5746efa9f", + "bytes": 10737, + "file": "frontend.py", + "repository": "CubeJerry/integer-mult-bounds", + "commit": "8c0e55c9ba25ff2c8199b01539a4d56ae71a1473" + }, + { + "path": "research/encoded-balanced-crt-inverse/source/research/encoded-balanced-crt-endpoint/endpoint.py", + "sha256": "c24ae2c90d175d276120438809e7c7401b8a8c04dec139f1b7345e9778984ced", + "git_blob": "b084d893bdb2ce5571ef00196a9ec6a60e723964", + "bytes": 6038, + "file": "endpoint.py", + "repository": "CubeJerry/integer-mult-bounds", + "commit": "8c0e55c9ba25ff2c8199b01539a4d56ae71a1473" + }, + { + "path": "research/encoded-balanced-crt-inverse/inverse_frontend.py", + "sha256": "0e5f4c9450372c90000f5ebf3c22dfbe7241dd53da9ae9bcce310af859b009ef", + "git_blob": "17abfb8500043bcdeb656094bb0213d911d986fc", + "bytes": 2167, + "file": "inverse_frontend.py", + "repository": "CubeJerry/integer-mult-bounds", + "commit": "8c0e55c9ba25ff2c8199b01539a4d56ae71a1473" + }, + { + "path": "research/encoded-balanced-crt-inverse/inverse_producer.py", + "sha256": "6acdebee7134fbc8e2d121060286bd05e7282900da8a28a78c80937dde7ea178", + "git_blob": "46bf6ef4e2dfa53bca17ac668914b1a842eaba9e", + "bytes": 8041, + "file": "inverse_producer.py", + "repository": "CubeJerry/integer-mult-bounds", + "commit": "8c0e55c9ba25ff2c8199b01539a4d56ae71a1473" + } + ] +} diff --git a/research/encoded-crt-leaf-payload/README.md b/research/encoded-crt-leaf-payload/README.md new file mode 100644 index 0000000000..03b23be98a --- /dev/null +++ b/research/encoded-crt-leaf-payload/README.md @@ -0,0 +1,125 @@ +# Route a marked payload from an encoded CRT leaf + +The live encoded CRT leaf now drives the existing Beneš row query and +literal binary radix mover for one padded right-axis fiber. On the +retained non-root fixture, slots 0 and 1 exchange their payloads and +padded slots 2 and 3 preserve theirs. The inverse restores the same +physical payload tape, its keys, the encoded source, and their heads. + +| Boundary | Source coordinates | Payload tags in physical order | +| --- | --- | --- | +| Input | (3, 2, 1, 1) | 293, 730, 905, 3681 | +| Forward | (3, 2, 1, 0) | 730, 293, 905, 3681 | +| Inverse | (3, 2, 1, 1) | 293, 730, 905, 3681 | + +The input uses moduli (5, 7, 3, 2) and declared widths (3, 3, 2, 2) from +the `nonroot_roundtrip` case of [#5625](https://github.com/CrocSwap/integer-mult-bounds/pull/5625). +Each payload is an opaque 12-bit record in the binary radix format. +The replay checks the entire frame, including its two-bit position +keys and its physical backing identity. It also checks the source's +metadata and inaccessible historical tail. + +## Source and payload join + +1. Acquire the retained encoded iterator and its clean private roles. + Select its last leaf at the level with unary half length one, with + a nonempty axis prefix. Retire earlier numerical leases without + writing their coordinates. Both directions pay for every visited + lease, including the skipped leases. +2. While the selected lease is live, scan the actual right record for + its unary width and modulus and copy the offset from the numerical + result stream using the existing precision guide. The measured + fields give width 2, modulus 2, precision 5 and offset 1 in both + directions. The source and result return to their entry heads + with their bytes preserved before source staging. +3. Run the unchanged encoded Beneš producer on those framed headers. + For each physical input slot, follow all produced rows by the + existing row-bit query. The adapter keeps the slot address on a + binary tape, walks the target bit from low to high and back, and + writes the destination as an MSB-first key in the allocated + radix cells. It reads the row tape backwards by rows for the + inverse, keeping the bits of each row in wire order. +4. Run the literal radix pass once per unary width mark. Its stable + last-bit pass rotates that bit to the front, so two passes sort + the two-bit destination keys and return them to their initial + orientation. Each tag moves with its key on the actual bit tape. + Stage the coordinate result, retire the numerical lease, commit + the source and clear the adapter and bucket storage. + +For the selected leaf the left modulus and coordinate are 3 and 1. +The direct CRT oracle solves 3c ≡ 1 modulo 2, giving c = 1. It maps +valid positions x to (x+c) modulo 2 and fixes the two padded positions. +The offset depends on the left child, which is preserved here. The +inverse therefore uses the same offset and the switch layers in reverse +order. Every switch layer is its own inverse, so the reversed layer +product undoes the forward product. The independent oracle checks the +nonidentity forward placement before checking exact restoration. + +The input positions are enumerated by an encoded counter. The adapter +uses the existing key cells for storage and derives its addresses from +physical positions. Fixture serialization and all independent +observers are outside the measured runtime. + +## Measured work and storage + +| Quantity | Forward | Inverse | +| --- | ---: | ---: | +| Encoded source symbol actions, including numerical work | 113,295 | 372,489 | +| Adapter symbol actions | 3,481 | 3,817 | +| Beneš producer instructions | 2,363,816 | 2,363,816 | +| Payload adapter bit actions | 1,694 | 1,694 | +| Literal radix instructions, including finite control | 43,162 | 43,162 | +| Retained private symbol roles | 136 | 136 | +| Retained private symbol cells | 2,253 | 2,633 | +| Retained bucket bit extent | 208 | 208 | +| Retained radix register bits | 144 | 144 | +| Retained Beneš registers | 15 | 15 | + +The symbol counts include header and key-address preparation, row +scans, source staging and retirement. The bit counts include the +physical key writes and bucket initialization and retirement, with +radix instructions counted separately. Both directions' private roles +remain retained for the measurement. They share one 57-cell source +and the original payload tape, whose visited extent is 183 bits. +These are observations in the respective execution models. A common +literal tariff for the combined source controller and payload path +requires further lowering. + +## Replay and source credit + +From a checkout or an official Git-free export with the declared +inputs, run: + +```sh +python3.12 -I -B research/encoded-crt-leaf-payload/replay.py +``` + +[RESULT.json](RESULT.json) records the observed headers, exact +endpoints, cost and backing. The checks include a separate direct CRT +oracle, noncommuting layers that distinguish reverse traversal, a +truncated layer stream that must fail, and suppressed switches that +must fail the forward-placement check. + +[INPUT-PINS.json](INPUT-PINS.json) binds the runtime to canonical main +`e54523517d0f03e58352e647c403a5af3e525a57` and four byte-exact +runtime files from CubeJerry's [#7352](https://github.com/CrocSwap/integer-mult-bounds/pull/7352) +at `8c0e55c9ba25ff2c8199b01539a4d56ae71a1473`. The forward writer +is also byte-identical to the one in [#7351](https://github.com/CrocSwap/integer-mult-bounds/pull/7351). +Ali Romman's [#5625](https://github.com/CrocSwap/integer-mult-bounds/pull/5625) +supplies the fixture and the paid retirement boundary. +JoyboyBrian's [#5092](https://github.com/CrocSwap/integer-mult-bounds/pull/5092), +[#5496](https://github.com/CrocSwap/integer-mult-bounds/pull/5496) +and [#5015](https://github.com/CrocSwap/integer-mult-bounds/pull/5015) +supply the encoded producer, physical row query and literal payload +consumer, respectively. OpenAI Codex and ChatGPT Pro materially assisted +the work. Pro produced a separate witness with the same placement and +restoration using different tags and a different input-key policy. +Apache-2.0. + +## Open next questions + +A complete balanced payload stage must route all right-axis fibers in +order, including idle and padded rows. A concrete next test is to +bind one retained multi-target fixture and check its synchronized +row and header streams. This package establishes one finite fiber. +A full integer product and a combined cost proof remain open. diff --git a/research/encoded-crt-leaf-payload/RESULT.json b/research/encoded-crt-leaf-payload/RESULT.json new file mode 100644 index 0000000000..8503cd80b7 --- /dev/null +++ b/research/encoded-crt-leaf-payload/RESULT.json @@ -0,0 +1,98 @@ +{ + "benes_program_instructions": 10648, + "control_cases": [ + "noncommuting rows distinguish traversal order", + "truncated width-two layer stream rejected", + "suppressed switches fail the forward oracle" + ], + "fixture": "nonroot_roundtrip", + "forward_and_inverse": [ + { + "adapter_symbol_actions": 3481, + "benes_instructions": 2363816, + "direction": "forward", + "encoded_source_symbol_actions": 113295, + "observed_headers": { + "h": "L01000R", + "modulus": "L01000R", + "offsets": "L10000|R", + "selected_layer": "L00000R", + "width": "L11R" + }, + "payload_adapter_bit_actions": 1694, + "radix_bit_control_instructions": 43162, + "radix_passes": 2, + "retained_benes_registers": 15, + "retained_bucket_bits": 208, + "retained_radix_register_bits": 144, + "retained_symbol_cells": 2253, + "retained_symbol_roles": 136, + "selected_nodes": 1, + "skipped_nodes": 1 + }, + { + "adapter_symbol_actions": 3817, + "benes_instructions": 2363816, + "direction": "inverse", + "encoded_source_symbol_actions": 372489, + "observed_headers": { + "h": "L01000R", + "modulus": "L01000R", + "offsets": "L10000|R", + "selected_layer": "L00000R", + "width": "L11R" + }, + "payload_adapter_bit_actions": 1694, + "radix_bit_control_instructions": 43162, + "radix_passes": 2, + "retained_benes_registers": 15, + "retained_bucket_bits": 208, + "retained_radix_register_bits": 144, + "retained_symbol_cells": 2633, + "retained_symbol_roles": 136, + "selected_nodes": 1, + "skipped_nodes": 2 + } + ], + "forward_destinations": [ + 1, + 0, + 2, + 3 + ], + "forward_source": [ + 3, + 2, + 1, + 0 + ], + "forward_tags": [ + 730, + 293, + 905, + 3681 + ], + "input_tags": [ + 293, + 730, + 905, + 3681 + ], + "moduli": [ + 5, + 7, + 3, + 2 + ], + "payload_bits_visited": 183, + "radix_program_instructions": 3885, + "restored_source_and_payload": true, + "source_cells_retained": 57, + "status": "PASS_ENCODED_CRT_LEAF_PAYLOAD", + "widths": [ + 3, + 3, + 2, + 2 + ] +} diff --git a/research/encoded-crt-leaf-payload/SOURCES.json b/research/encoded-crt-leaf-payload/SOURCES.json new file mode 100644 index 0000000000..acfe3ca127 --- /dev/null +++ b/research/encoded-crt-leaf-payload/SOURCES.json @@ -0,0 +1,90 @@ +{ + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "git_blob": "8d4ba37e2778acb35b34e0719df2caf138fbeb50", + "path": "research/r437-preparation-composition/predecessor4025/source/words.py", + "sha256": "5c37f57708ba3131bdcb03139f9dbc29886bee44569c09cbba51b68f75acd7f9", + "usage": "input" + }, + { + "git_blob": "4f00467a0ff580954ad2fd0c7380240c753ddef3", + "path": "research/r437-preparation-composition/predecessor4025/source/records.py", + "sha256": "0c9c4b23e998597fb877bb1a29da69ac869b68262abe635b162b4dba9c69b372", + "usage": "input" + }, + { + "git_blob": "1fa2b0cb88320d4f5b623554bb0fc6de332b773c", + "path": "research/encoded-crt-entry-lifecycle/entry.py", + "sha256": "0537ec98f306270c8ff6a424841886cf53f675d9947029347090c7dc779616d7", + "usage": "input" + }, + { + "git_blob": "a327b0161eca57a1cc44ec2aa8e3defed2167ddc", + "path": "research/encoded-current-crt/producer.py", + "sha256": "88dab4ca02a92164a67826db361214fa1405e4b4a588f8c4279a21bcee95ab76", + "usage": "input" + }, + { + "git_blob": "20ef3519b6fef691ec92b7315e320b5e8ce9bf18", + "path": "research/crt-persistent-numerical-owner/owner.py", + "sha256": "1d73f432f8de9c791260c43335eb207d82bbb3f5b190cc76d0d914a4db076f41", + "usage": "input" + }, + { + "git_blob": "57f6853e262a6136bc616f1e47a31d0ace28495c", + "path": "research/crt-mixed-row-entry/bridge.py", + "sha256": "89c38638c0d66da731566c903c32e7fa1ad31088d29cfd2634fce823dd07c1f9", + "usage": "input" + }, + { + "git_blob": "676582b4a376db375237ec52df84a3ddaf231827", + "path": "research/crt-current-row-query/join.py", + "sha256": "11c9ac1175a45edae80869b22c041e31a1b5cc75f4389ec2e073de37e547bf35", + "usage": "input" + }, + { + "git_blob": "052b01a83bc910c176b83a012b9f46f0e9525b9d", + "path": "research/crt-encoded-benes-rom-producer/microcode.py", + "sha256": "d4af5350854a87b67484840800b94e1e53cff82c78ec0f2a91753fed9ea70af7", + "usage": "input" + }, + { + "git_blob": "88292ce98d31d540c7dba6960bfe4c19f06a8077", + "path": "research/crt-uniform-rom-query/machine.py", + "sha256": "46ee6a635251e498ee9a5d4aff8c0e2a7f1ef2ff951e5b6a2a8953316e9cd02d", + "usage": "input" + }, + { + "git_blob": "ec574f26d6f64ead00d7c2cf5b808c0498b460cf", + "path": "research/crt-binary-key-port/binary.py", + "sha256": "50a3dea7fc087715b4e605e85629566ed31903026540f916df6b8cbaa536182d", + "usage": "input" + }, + { + "git_blob": "f558019fe70c46bcb2f087464c1d2aa021b7188d", + "path": "research/crt-binary-radix-consumer/radix.py", + "sha256": "f4200a495d9c445474275214254d46e9a8e03967a635263905a4c9192bb36f1f", + "usage": "input" + }, + { + "git_blob": "832d3312df223d1b151e5c620cc3d4e295f49e05", + "path": "research/crt-paid-row-reentry/RESULT.json", + "sha256": "d818bffac4647dffaf525ed68dbb79dc575a00303af3315c6d4fe39b60f49a13", + "usage": "input" + }, + { + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "path": "certificates/selected-result.json", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1", + "usage": "provenance" + }, + { + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "path": "docs/research/agent-task-catalog.json", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81", + "usage": "provenance" + } + ], + "schema_version": 1 +} diff --git a/research/encoded-crt-leaf-payload/TASK.json b/research/encoded-crt-leaf-payload/TASK.json new file mode 100644 index 0000000000..e64c896a07 --- /dev/null +++ b/research/encoded-crt-leaf-payload/TASK.json @@ -0,0 +1,83 @@ +{ + "actual_scope": "One nonroot mixed-width padded right fiber from #5625, with live #7352 encoded fields, physical four-tag forward placement and inverse restoration, and measured separate source, ROM and radix costs.", + "ai_assistance": "OpenAI Codex and ChatGPT Pro materially assisted formulation, independent audit and replay.", + "author": "Clear1nsight", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "Join an actual encoded CRT address-state node to physical payload movement at one admitted leaf boundary.", + "budget_minutes": 60, + "evidence": "Direct CRT oracle, byte-for-byte source and literal payload round trip, exact header receipt, two actual producer calls, four literal radix passes, and three targeted failure/order controls.", + "open_questions": [ + { + "blocked_by": "The current join addresses one fiber. The multi-target layout, compilation bill and integer recovery remain separate obligations.", + "first_step": "Pin one multi-target fixture, then show that the ordered row and header streams deliver every marked record and retire each borrow.", + "question": "Can a mixed-width node with more than one right axis use the same physical payload boundary?", + "why_it_matters": "A complete balanced payload stage needs synchronization across the right-axis fibers." + } + ], + "original_card": { + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "existing_checks": [ + { + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "status": "author-checked" + }, + { + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "status": "reviewed" + } + ], + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "id": "uniform-transfer-audit", + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ] + }, + "outcome": "completed", + "priority_revision": 8, + "schema_version": 1, + "scope_change_reason": "Continue the encoded balanced inverse at one released nonroot payload boundary, using the existing physical ROM query and literal radix consumer.", + "scope_status": "refined", + "stop_rule": "Stop at the released nonroot fixture and its one marked right-axis fiber. Charge all actual leases, metadata, tape work and retained backing.", + "task_id": "uniform-transfer-audit" +} diff --git a/research/encoded-crt-leaf-payload/VERIFY.json b/research/encoded-crt-leaf-payload/VERIFY.json new file mode 100644 index 0000000000..498e3a0316 --- /dev/null +++ b/research/encoded-crt-leaf-payload/VERIFY.json @@ -0,0 +1,32 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Replay live encoded node, unchanged ROM and literal radix, independent tagged endpoints, retirement and backing, order and missing-switch controls.", + "timeout_seconds": 70 + } + ], + "inputs": [ + "research/r437-preparation-composition/predecessor4025/source/words.py", + "research/r437-preparation-composition/predecessor4025/source/records.py", + "research/encoded-crt-entry-lifecycle/entry.py", + "research/encoded-current-crt/producer.py", + "research/crt-persistent-numerical-owner/owner.py", + "research/crt-mixed-row-entry/bridge.py", + "research/crt-current-row-query/join.py", + "research/crt-encoded-benes-rom-producer/microcode.py", + "research/crt-uniform-rom-query/machine.py", + "research/crt-binary-key-port/binary.py", + "research/crt-binary-radix-consumer/radix.py", + "research/crt-paid-row-reentry/RESULT.json" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/encoded-crt-leaf-payload/frozen/endpoint.py b/research/encoded-crt-leaf-payload/frozen/endpoint.py new file mode 100644 index 0000000000..b084d893bd --- /dev/null +++ b/research/encoded-crt-leaf-payload/frozen/endpoint.py @@ -0,0 +1,157 @@ +"""Paid whole-node CRT result projection into the actual encoded source. + +Prepared for Jerry Chen / CubeJerry with substantial OpenAI assistance. +Apache-2.0. The fixed predecessor providers are pinned in INPUT-PINS.json. +No coordinate, modulus, width, level or axis count enters host control. +""" + + +class Endpoint: + """One encoded forward balanced address-state traversal, 79 owned roles.""" + + def __init__(self, frontend, words, records, entry, numeric, owner, + canonical, source): + self.w, self.r, self.source = words, records, source + self.iterator = frontend.Iterator(words, records, entry, numeric, + owner, canonical, source) + self.staging = entry.Port(words) + self.staging.retire() + self.pending = False + + def _copy(self, expected): + w = self.w + w.need(self.source.read() == expected, 'preserved source delimiter') + self.staging.append(expected) + self.source.step(1) + + def _field(self, width): + w = self.w + while width.read() == w.ONE: + bit = self.source.read() + w.need(bit in (w.ZERO, w.ONE), 'source padded bit') + self.staging.append(bit) + self.source.step(1) + width.step(1) + w.need(width.read() == w.RIGHT, 'source width extent') + width.rewind() + + def _updated(self, width, result, guide): + w, r = self.w, self.r + w.need(result.read() == r.ROOT, 'whole-node result record') + result.step(1) + while guide.read() == w.ONE: + w.need(result.read() in (w.ZERO, w.ONE), 'offset bit') + result.step(1) + guide.step(1) + w.need(guide.read() == w.BLANK and result.read() == r.WORD_END, + 'whole offset consumed') + result.step(1) + guide.rewind() + while width.read() == w.ONE: + old, new = self.source.read(), result.read() + w.need(old in (w.ZERO, w.ONE) and new in (w.ZERO, w.ONE), + 'current and updated coordinate bits') + w.need(guide.read() == w.ONE, 'updated field covers source width') + self.staging.append(new) + self.source.step(1) + result.step(1) + width.step(1) + guide.step(1) + w.need(width.read() == w.RIGHT, 'updated source width') + width.rewind() + while guide.read() == w.ONE: + w.need(result.read() == w.ZERO, 'updated value fits declared width') + result.step(1) + guide.step(1) + w.need(guide.read() == w.BLANK and result.read() == r.WORD_END, + 'complete updated field') + result.step(1) + guide.rewind() + w.need(result.read() == r.RECORD_END, 'whole-node result end') + result.step(1) + + def _record(self, result=None, guide=None): + w, r = self.w, self.r + width = self.iterator.counters['width'] + self._copy(r.ROOT) + seen = False + while self.source.read() == w.ONE: + seen = True + self.staging.append(w.ONE) + width.append(w.ONE) + self.source.step(1) + w.need(seen, 'positive source width') + self._copy(r.WORD_END) + width.append(w.RIGHT) + width.rewind() + self._field(width) + self._copy(r.WORD_END) + if result is None: + self._field(width) + else: + self._updated(width, result, guide) + self._copy(r.RECORD_END) + width.clear() + + def stage(self, lease): + """Snapshot the next complete source while its numerical lease is live.""" + w, r, it = self.w, self.r, self.iterator + w.need(it.live and not self.pending, 'one live unstaged node result') + self.staging.step(-1) + w.need(self.staging.read() == w.BLANK, 'retired staging origin') + self.staging.write(w.LEFT) + self.staging.step(1) + axis, half = it.counters['axis'], it.counters['half'] + result, guide = lease.actual.result['stream'], lease.actual.guide + while axis.read() != r.STEP: + w.need(axis.read() == w.ONE, 'current node prefix') + self._record() + axis.step(1) + for selected in (False, True): + while half.read() == w.ONE: + w.need(axis.read() in (w.ONE, r.STEP), 'complete current node') + self._record(result if selected else None, guide) + axis.step(1) + half.step(1) + w.need(half.read() == w.RIGHT, 'current node half extent') + half.rewind() + w.need(result.read() == w.RIGHT, 'all right-coordinate results consumed') + while self.source.read() != w.RIGHT: + w.need(axis.read() in (w.ONE, r.VALUE), 'unchanged source suffix') + self._record() + axis.step(1) + w.need(axis.read() == w.RIGHT, 'complete source and cursor extents') + self.staging.append(w.RIGHT) + self.staging.rewind() + self.source.rewind() + axis.rewind() + result.rewind() + self.pending = True + + def commit(self): + """After retirement, overwrite equal-length source and erase the copy.""" + w, it = self.w, self.iterator + w.need(self.pending and not it.live and not it.bank.busy, + 'source update follows numerical retirement') + while self.staging.read() != w.RIGHT: + self.source.write(self.staging.read()) + self.source.step(1) + self.staging.step(1) + w.need(self.source.read() == w.RIGHT, 'preserved full source extent') + self.source.rewind() + self.staging.retire() + self.pending = False + + def step(self): + self.w.need(not self.pending, 'previous staged update must commit') + lease = self.iterator.next() + if lease is None: + return False + self.stage(lease) + lease.close() + self.commit() + return True + + def run(self): + while self.step(): + pass diff --git a/research/encoded-crt-leaf-payload/frozen/frontend.py b/research/encoded-crt-leaf-payload/frozen/frontend.py new file mode 100644 index 0000000000..8adbe2cfef --- /dev/null +++ b/research/encoded-crt-leaf-payload/frozen/frontend.py @@ -0,0 +1,277 @@ +"""Tape-driven balanced-node selection into the unchanged CRT numerical entry. + +No runtime width, axis count, start, level or precision is decoded. All variable +iteration is driven by local symbols on the supplied source or owned unary +tapes. Numeric arithmetic and its 63-role bank are pinned predecessor code. +Prepared for CubeJerry with substantial OpenAI assistance. Apache-2.0. +""" +from types import SimpleNamespace + + +COUNTERS = ('axis', 'depth', 'halve_a', 'halve_b', 'half', 'double', 'width') +GUARDS = ('g0', 'g1', 'g2', 'g3', 'g4', 'g5', 'g6', 'g7') + + +class Iterator: + """One numerical result at a time; source contents stay read-only. + +The supplied source has the #5353 tagged padded-axis encoding and enters at +head one. Construction charges shape manufacture. next() takes no geometry +arguments. The physical interface is linear-use: consume the current lease +once before the next result and relinquish its borrowed aliases. Historical +Python-handle identity checks are interpreter guards, not a tape service. +""" + def __init__(self, words, records, entry, numeric, owner, canonical, source): + self.w, self.r, self.e = words, records, entry + self.numeric, self.canonical, self.source = numeric, canonical, source + self.bank = owner.Bank(words, entry) + self.guards = tuple(entry.Port(words) for _ in GUARDS) + for port in self.guards: + port.retire() + self.counters = {name: entry.Port(words) for name in COUNTERS} + self.live, self.closed = False, False + try: + self._shape() + except ValueError: + # Source framing errors and nondyadic counts precede numerical entry. + source.rewind() + for port in self.counters.values(): + port.retire() + self.closed = True + raise + + def _record(self, target=None, guide=None): + """Read one exact axis record; optionally project its canonical pair.""" + w, r, source = self.w, self.r, self.source + width = self.counters['width'] + width.clear() + w.need(source.read() == r.ROOT, 'axis tag') + source.step(1) + if target is not None: + target.append(r.ROOT) + seen = False + while source.read() == w.ONE: + seen = True + width.append(w.ONE) + if guide is not None: + guide.append(w.ONE) + source.step(1) + w.need(seen and source.read() == r.WORD_END, 'positive unary width') + source.step(1) + width.append(w.RIGHT) + width.rewind() + for delimiter in (r.WORD_END, r.RECORD_END): + while width.read() == w.ONE: + bit = source.read() + w.need(bit in (w.ZERO, w.ONE), 'padded source bit') + if target is not None: + target.append(bit) + source.step(1) + width.step(1) + w.need(width.read() == w.RIGHT and source.read() == delimiter, + 'exact source field extent') + source.step(1) + width.rewind() + if target is not None: + self.canonical.canonical_end(target, w, r) + if target is not None: + target.append(r.RECORD_END) + width.clear() + + def _many(self, port): + w = self.w + w.need(port.read() == w.ONE, 'nonempty reduction count') + port.step(1) + symbol = port.read() + w.need(symbol in (w.ONE, w.RIGHT), 'unary reduction shape') + port.rewind() + return symbol == w.ONE + + def _shape(self): + w, source = self.w, self.source + axis, depth = self.counters['axis'], self.counters['depth'] + current, spare = self.counters['halve_a'], self.counters['halve_b'] + while source.read() != w.RIGHT: + self._record() + axis.append(w.ONE) + current.append(w.ONE) + source.rewind() + axis.append(w.RIGHT) + axis.rewind() + current.append(w.RIGHT) + current.rewind() + w.need(self._many(current), 'at least two source axes') + while self._many(current): + depth.append(w.ONE) + odd = False + while current.read() == w.ONE: + odd = not odd + if not odd: + spare.append(w.ONE) + current.step(1) + w.need(current.read() == w.RIGHT and not odd, 'dyadic source axis count') + spare.append(w.RIGHT) + spare.rewind() + current.clear() + current, spare = spare, current + current.clear() + spare.clear() + depth.append(w.RIGHT) + depth.rewind() + half = self.counters['half'] + half.append(w.ONE) + half.append(w.RIGHT) + half.rewind() + w.need(axis.read() == w.ONE, 'first axis') + axis.write(self.r.STEP) # Unique current-node marker. + + def _prepare_guards(self, guide): + w = self.w + for port in self.guards: + port.step(-1) + w.need(port.read() == w.BLANK, 'retired protected marker') + port.write(w.LEFT) + port.step(1) + while guide.read() == w.ONE: + w.need(port.read() == w.BLANK, 'retired protected body') + port.write(w.ZERO) + port.step(1) + guide.step(1) + w.need(guide.read() == w.BLANK and port.read() == w.BLANK, + 'current protected extent') + port.write(w.RIGHT) + port.rewind() + guide.rewind() + + def _entry(self, w, r, adapter, numeric, source, dirty, + widths, ell, level, start, row): + # Bank.open's fixed call signature is preserved. Geometry is never supplied. + w.need(widths is None and ell is None and level is None and + start is None and row is None, 'no host geometry arguments') + w.need(source is self.source and dirty is self.guards, 'actual borrowed ports') + return NodeEntry(self, adapter) + + def next(self): + self.w.need(not self.live, 'previous node result must close') + if self.closed: + return None + self.w.need(self.counters['depth'].read() == self.w.ONE, 'active encoded level') + self.live = True + bridge = SimpleNamespace(RowEntry=self._entry) + lease = self.bank.open(self.r, self.numeric, bridge, self.source, self.guards, + None, None, None, None, None) + return NodeLease(self, lease) + + def _double_half(self): + w = self.w + half, temporary = self.counters['half'], self.counters['double'] + while half.read() == w.ONE: + temporary.append(w.ONE) + half.step(1) + w.need(half.read() == w.RIGHT, 'half-size delimiter') + half.write(w.BLANK) + temporary.append(w.RIGHT) + temporary.rewind() + while temporary.read() == w.ONE: + half.append(w.ONE) + temporary.step(1) + w.need(temporary.read() == w.RIGHT, 'copied half size') + half.append(w.RIGHT) + half.rewind() + temporary.clear() + + def _advance(self, last): + w, r = self.w, self.r + axis, depth = self.counters['axis'], self.counters['depth'] + while axis.read() != r.STEP: + w.need(axis.read() == w.ONE, 'preserved current cursor') + axis.step(1) + axis.write(w.ONE) + if last: + while axis.read() != w.RIGHT: + w.need(axis.read() == w.ONE, 'last-node suffix') + axis.step(1) + axis.rewind() + depth.step(1) + if depth.read() == w.RIGHT: + self.close() + return + w.need(depth.read() == w.ONE, 'next encoded level') + self._double_half() + axis.write(r.STEP) + else: + while axis.read() != r.VALUE: + w.need(axis.read() == w.ONE, 'next-node interval') + axis.step(1) + axis.write(r.STEP) + axis.rewind() + + def close(self): + self.w.need(not self.live and not self.closed, 'retired iterator closes once') + for port in self.counters.values(): + port.retire() + self.closed = True + + +class NodeEntry: + """Actual canonical streams and precision guide into unchanged Entry.""" + def __init__(self, iterator, adapter): + self.iterator = iterator + w, r, source = iterator.w, iterator.r, iterator.source + self.guide, self.left, self.right = (adapter.Port(w), adapter.Port(w), adapter.Port(w)) + self.inputs = (self.guide, self.left, self.right) + self.active = True + axis, half = iterator.counters['axis'], iterator.counters['half'] + while axis.read() != r.STEP: + w.need(axis.read() == w.ONE, 'prefix cursor') + iterator._record() + axis.step(1) + for target in (self.left, self.right): + while half.read() == w.ONE: + w.need(axis.read() in (w.ONE, r.STEP), 'complete selected node') + iterator._record(target, self.guide) + axis.step(1) + half.step(1) + w.need(half.read() == w.RIGHT, 'encoded half extent') + half.rewind() + target.append(w.RIGHT) + target.rewind() + self.last = axis.read() == w.RIGHT + if not self.last: + w.need(axis.read() == w.ONE, 'following source axis') + axis.write(r.VALUE) # Pending next cursor; current cursor survives handoff. + axis.rewind() + source.rewind() + self.guide.append(w.ONE) + self.guide.rewind() + iterator._prepare_guards(self.guide) + self.context = adapter.Entry(w, r, self.guide, iterator.guards) + self.result = self.context.invoke(iterator.numeric, self.left, self.right) + + def close(self): + self.context.consume(self.result) + self.context.close() + for port in self.inputs: + port.retire() + for port in self.iterator.guards: + port.retire() + + +class NodeLease: + """Interpreter wrapper for the single current linear-use continuation. + +The closed flag also guards stale Python references, but the fixed-role +physical theorem does not implement an unbounded stale-handle history. +""" + def __init__(self, iterator, lease): + self.iterator, self.lease = iterator, lease + self.actual = lease.actual + self.closed = False + + def close(self): + self.iterator.w.need(not self.closed, 'node lease closes once') + last = self.actual.last + self.lease.close() + self.closed = True + self.iterator.live = False + self.iterator._advance(last) diff --git a/research/encoded-crt-leaf-payload/frozen/inverse_frontend.py b/research/encoded-crt-leaf-payload/frozen/inverse_frontend.py new file mode 100644 index 0000000000..17abfb8500 --- /dev/null +++ b/research/encoded-crt-leaf-payload/frozen/inverse_frontend.py @@ -0,0 +1,52 @@ +"""Encoded descending balanced levels through the existing frontend hook. + +Prepared for Jerry Chen / CubeJerry with substantial OpenAI assistance. +Apache-2.0. See SEAMS.json for the exact inherited interface. +""" +from types import SimpleNamespace + + +def bind(forward): + """Bind one fixed provider; no geometry or numeric value is an argument.""" + class Iterator(forward.Iterator): + def __init__(self, words, records, entry, numeric, owner, canonical, source): + super().__init__(words, records, entry, numeric, owner, canonical, source) + # The inherited shape proof gives k depth tokens and half=1. + # Skip one token, then double once per remaining token: d/2. + depth = self.counters['depth'] + depth.step(1) + while depth.read() == self.w.ONE: + forward.Iterator._double_half(self) + depth.step(1) + self.w.need(depth.read() == self.w.RIGHT, 'complete reverse depth') + depth.rewind() + + def _double_half(self): + """Compatibility hook: the inherited next-level call now halves. + + Startup calls the base doubling method explicitly; every call + through this hook is a descending transition after a level ends. + """ + w = self.w + half = self.counters['half'] + temporary = self.counters['double'] + odd = False + while half.read() == w.ONE: + odd = not odd + if not odd: + temporary.append(w.ONE) + half.step(1) + w.need(half.read() == w.RIGHT and not odd, 'even reverse half size') + temporary.append(w.RIGHT) + temporary.rewind() + w.need(temporary.read() == w.ONE, 'nonempty next reverse half') + half.clear() + while temporary.read() == w.ONE: + half.append(w.ONE) + temporary.step(1) + w.need(temporary.read() == w.RIGHT, 'complete halved size') + half.append(w.RIGHT) + half.rewind() + temporary.clear() + + return SimpleNamespace(Iterator=Iterator) diff --git a/research/encoded-crt-leaf-payload/frozen/inverse_producer.py b/research/encoded-crt-leaf-payload/frozen/inverse_producer.py new file mode 100644 index 0000000000..46bf6ef4e2 --- /dev/null +++ b/research/encoded-crt-leaf-payload/frozen/inverse_producer.py @@ -0,0 +1,174 @@ +# Inverse specialization for CubeJerry with OpenAI assistance. Apache-2.0. +# Exactly one scientific line differs from the pinned #5053 producer. +"""Encoded current-child CRT reconstruction and complete right-node update. + +JoyboyBrian, substantial OpenAI Codex assistance. Apache-2.0. +Only finite symbols/carries and fixed register ownership enter host control. +""" + +class Arithmetic: + """New loose-width residue interface; the frozen Ring guard is unchanged.""" + def __init__(self, arena, words): + self.arena, self.w = arena, words + self.raw = words.Unsigned(arena) + self.one = arena.literal(1) + + def admit(self, modulus): + self.w.need(self.raw.compare(modulus, self.one) > 0, 'CRT modulus exceeds one') + modulus.msb(); high = modulus.read(); modulus.rewind() + self.w.need(high == self.w.ZERO, 'CRT modulus high-bit margin') + + def remainder(self, value, modulus): + quotient, rest = self.raw.divmod(value, modulus) + self.arena.free(quotient) + return rest + + def add(self, left, right, modulus): + total, carry = self.raw.add(left, right) + self.w.need(not carry, 'modular addition margin') + if self.raw.compare(total, modulus) >= 0: + reduced = self.raw.subtract_exact(total, modulus) + self.arena.free(total); total = reduced + return total + + def subtract(self, left, right, modulus): + if self.raw.compare(left, right) >= 0: + return self.raw.subtract_exact(left, right) + larger, carry = self.raw.add(left, modulus) + self.w.need(not carry, 'modular subtraction margin') + result = self.raw.subtract_exact(larger, right) + self.arena.free(larger) + return result + + def multiply(self, left, right, modulus): + scan, result = self.arena.copy(right), self.arena.zero() + scan.msb() + while scan.read() != self.w.LEFT: + doubled = self.add(result, result, modulus) + self.arena.free(result); result = doubled + if scan.read() == self.w.ONE: + added = self.add(result, left, modulus) + self.arena.free(result); result = added + scan.step(-1) + scan.step(1); self.arena.free(scan) + return result + + def inverse(self, value, modulus): + r0, r1 = self.arena.copy(modulus), self.arena.copy(value) + t0, t1 = self.arena.zero(), self.arena.copy(self.one) + while not r1.zero(): + quotient, r2 = self.raw.divmod(r0, r1) + qmod = self.remainder(quotient, modulus) + product = self.multiply(qmod, t1, modulus) + t2 = self.subtract(t0, product, modulus) + self.arena.free_many(quotient, qmod, product, r0, t0) + r0, r1, t0, t1 = r1, r2, t1, t2 + unit = self.raw.compare(r0, self.one) == 0 + self.arena.free_many(r0, r1, t1) + if unit: return t0 + self.arena.free(t0) + return None + + def product(self, left, right): + scan, result = self.arena.copy(right), self.arena.zero() + scan.msb() + while scan.read() != self.w.LEFT: + doubled, carry = self.raw.add(result, result) + self.w.need(not carry, 'CRT product word capacity') + self.arena.free(result); result = doubled + if scan.read() == self.w.ONE: + added, carry = self.raw.add(result, left) + self.w.need(not carry, 'CRT product word capacity') + self.arena.free(result); result = added + scan.step(-1) + scan.step(1); self.arena.free(scan) + result.msb(); high = result.read(); result.rewind() + self.w.need(high == self.w.ZERO, 'CRT complete product high-bit margin') + return result + + +def produce(arena, left, right, words, records, *, fault=None): + """Both borrowed streams contain ROOT + two fixed-width words + RECORD_END. + + LEFT is unique at cell zero, RIGHT terminates the stream; heads enter at one. + Return owned lower/product words and (offset,new-value) records. The right + prefix includes all preceding right moduli, exactly as source balanced(). + """ + w = words + w.need(left is not right, 'distinct CRT descriptor roles') + protected = set(arena.live) + w.need(arena.capacity == 64 and arena.bits >= 4 and len(protected) <= 8, + 'fixed CRT numerical entry inventory') + output = records.Tape(); keep = set(); succeeded = False + + def pair(stream): + w.need(stream.read() == records.ROOT, 'CRT paired descriptor tag') + stream.step(1) + modulus = records.read_word(stream, arena) + value = records.read_word(stream, arena) + w.need(stream.read() == records.RECORD_END, 'CRT paired descriptor end') + stream.step(1) + return modulus, value + + try: + a = Arithmetic(arena, words) + lower, prefix = arena.zero(), arena.copy(a.one) + valid, seen_left = True, False + while left.read() != w.RIGHT: + seen_left = True + modulus, value = pair(left); a.admit(modulus) + valid = valid and a.raw.compare(value, modulus) < 0 + base = a.remainder(prefix, modulus) + inverse = a.inverse(base, modulus) + w.need(inverse is not None, 'pairwise coprime CRT prefix') + local = a.remainder(lower, modulus) + scaled = a.multiply(local, inverse, modulus) + digit = a.remainder(value, modulus) + adjustment = arena.copy(digit) if fault == 'treat_current_as_original' else a.subtract(digit, scaled, modulus) + term = a.product(prefix, adjustment) + updated, carry = a.raw.add(lower, term) + w.need(not carry, 'CRT reconstruction capacity') + total = a.product(prefix, modulus) + arena.free_many(modulus, value, base, inverse, local, scaled, digit, + adjustment, term, lower, prefix) + lower, prefix = updated, total + w.need(seen_left, 'nonempty current CRT left group') + if not valid: + arena.free(lower); lower = arena.zero() + left_product = arena.copy(prefix) + seen_right = False + while right.read() != w.RIGHT: + seen_right = True + modulus, value = pair(right); a.admit(modulus) + base = a.remainder(prefix, modulus) + inverse = a.inverse(base, modulus) + w.need(inverse is not None, 'pairwise coprime CRT right prefix') + local = a.remainder(lower, modulus) + offset = a.multiply(local, inverse, modulus) + if fault == 'omit_right_prefix': + arena.free(offset) + original_base = a.remainder(left_product, modulus) + original_inverse = a.inverse(original_base, modulus) + offset = a.multiply(local, original_inverse, modulus) + arena.free_many(original_base, original_inverse) + if a.raw.compare(value, modulus) < 0 or fault == 'rotate_padding': + canonical = a.remainder(value, modulus) + updated = a.subtract(canonical, offset, modulus) + arena.free(canonical) + else: updated = arena.copy(value) + output.append(records.ROOT) + records.append_word(output, offset); records.append_word(output, updated) + output.append(records.RECORD_END) + total = a.product(prefix, modulus) + arena.free_many(modulus, value, base, inverse, local, offset, updated, prefix) + prefix = total + w.need(seen_right, 'nonempty current CRT right group') + output.append(w.RIGHT); output.rewind() + keep = {lower.slot, left_product.slot}; succeeded = True + return dict(lower=lower, product=left_product, stream=output, left_valid=valid) + finally: + left.rewind(); right.rewind() + for slot in tuple(arena.live): + if slot not in protected and slot not in keep: + arena.free(arena.words[slot]) + if not succeeded: output.clear() diff --git a/research/encoded-crt-leaf-payload/replay.py b/research/encoded-crt-leaf-payload/replay.py new file mode 100644 index 0000000000..75ad727054 --- /dev/null +++ b/research/encoded-crt-leaf-payload/replay.py @@ -0,0 +1,392 @@ +"""Source-bound finite replay of one encoded CRT payload fiber. Apache-2.0.""" + +from argparse import ArgumentParser +from contextlib import contextmanager +from hashlib import sha1, sha256 +from pathlib import Path +from types import ModuleType, SimpleNamespace +import json +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PINS = json.loads((HERE / 'INPUT-PINS.json').read_text()) +TAGS = (0x125, 0x2DA, 0x389, 0xE61) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def authenticate(path, pin): + data = path.read_bytes() + need(len(data) == pin['bytes'] and sha256(data).hexdigest() == pin['sha256'], + f'source bytes changed: {pin["path"]}') + git_blob = b'blob ' + str(len(data)).encode() + b'\0' + data + need(sha1(git_blob).hexdigest() == pin['git_blob'], 'source Git blob changed') + + +def load(name, path): + module = ModuleType(name) + module.__file__ = str(path) + sys.modules[name] = module + exec(compile(path.read_bytes(), str(path), 'exec'), module.__dict__) + return module + + +def modules(): + for pin in PINS['canonical']: + authenticate(ROOT / pin['path'], pin) + for pin in PINS['retained']: + authenticate(HERE / 'frozen' / pin['file'], pin) + canonical = {Path(p['path']).name: ROOT / p['path'] for p in PINS['canonical']} + w = load('words', canonical['words.py']) # The retained records module imports this name. + r = load('payload_records', canonical['records.py']) + e = load('payload_entry', canonical['entry.py']) + numeric = load('payload_numeric', canonical['producer.py']) + owner = load('payload_owner', canonical['owner.py']) + bridge = load('payload_bridge', canonical['bridge.py']) + f = load('payload_forward_frontend', HERE / 'frozen/frontend.py') + reverse = load('payload_reverse_frontend', HERE / 'frozen/inverse_frontend.py').bind(f) + writer = load('payload_writer', HERE / 'frozen/endpoint.py') + subtractive = load('payload_subtractive', HERE / 'frozen/inverse_producer.py') + join = load('payload_query', canonical['join.py']) + rom = load('payload_benes', canonical['microcode.py']) + binary = load('payload_binary', canonical['binary.py']) + radix = load('payload_radix', canonical['radix.py']) + builder = load('payload_radix_builder', canonical['machine.py']) + program, _, registers = binary.compile_program(radix.assemble(builder), lifecycle=True) + route = load('payload_route', HERE / 'route.py') + fixture = next(case for case in json.loads(canonical['RESULT.json'].read_text())['cases'] + if case['name'] == 'nonroot_roundtrip') + + class MeasuredBitTape(binary.BitTape): + def __init__(self, initial=()): + super().__init__(initial) + self.extent = max(1, len(initial)) + + def move(self, direction): + super().move(direction) + self.extent = max(self.extent, self.head + 1) + + return SimpleNamespace(w=w, r=r, e=e, numeric=numeric, owner=owner, bridge=bridge, + f=f, reverse=reverse, writer=writer, subtractive=subtractive, + join=join, rom=rom, binary=binary, program=program, + registers=registers, rom_program=rom.producer_program(), + route=route, fixture=fixture, bit_tape=MeasuredBitTape) + + +@contextmanager +def seal_numerical_roles(m): + def deny(*_args, **_kwargs): + raise ValueError('new numerical role or host word inspection during execution') + + owners = ((m.e.Port, '__init__'), (m.w.Word, '__init__'), (m.w.Arena, '__init__'), + (m.w.Word, 'inspect')) + originals = [getattr(kind, method) for kind, method in owners] + for kind, method in owners: + setattr(kind, method, deny) + try: + yield + finally: + for (kind, method), original in zip(owners, originals, strict=True): + setattr(kind, method, original) + + +def bit_actions(tapes): + return sum(sum(tape.actions.values()) for tape in tapes) + + +def meter_actions(meter): + return meter.reads + meter.writes + meter.moves + + +def literal_radix(m, record, width, buckets): + for bucket in buckets: + origin = m.route.RecordTape(m.binary, bucket) + origin.emit('<') + origin.move_word(-1) + + tapes = dict(zip(('bad', 'b0', 'b1'), (record.tape, *buckets))) + before = bit_actions(tapes.values()) + machines = [] + width.step(1) + while width.read() == '1': + machine = m.binary.Machine(m.program, len(m.registers), tapes) + need(machine.run() == 'accept', 'retained binary consumer accepts') + machines.append(machine) + width.step(1) + need(width.read() == 'R', 'encoded radix pass limit') + width.rewind() + low_level_radix = bit_actions(tapes.values()) - before + for bucket in buckets: + origin = m.route.RecordTape(m.binary, bucket) + for _ in origin.codes['<']: + bucket.write(0) + bucket.move(1) + origin.move_word(-1) + return machines, low_level_radix + + +def run_leg(m, source, payload, reverse): + """Execute one actual selected leaf. Geometry and destination keys come from tapes.""" + source_before = meter_actions(source.meter) + borrowed_source = bytes(source.cells), source.head + payload_before = bit_actions((payload,)) + front = m.reverse if reverse else m.f + numeric = m.subtractive if reverse else m.numeric + endpoint = m.writer.Endpoint(front, m.w, m.r, m.e, numeric, m.owner, m.bridge, source) + it = endpoint.iterator + numeric_ports = (*it.bank.ports, *it.guards, *it.counters.values(), endpoint.staging) + + headers = {name: m.join.Tape() for name in ('h', 'modulus', 'selected_layer', 'offsets')} + width, index, address, countdown, row = (m.join.Tape() for _ in range(5)) + service = {name: ['_'] for name in (*m.rom.REGS, 'arena', 'spool', 'layers', 'rom')} + service.update({name: port.cells for name, port in headers.items()}) + layers, rom = m.join.Tape(service['layers']), m.join.Tape(service['rom']) + adapter_ports = (*headers.values(), width, index, address, countdown, row, layers, rom) + record = m.route.RecordTape(m.binary, payload) + buckets = (m.bit_tape(), m.bit_tape()) + arena_meters = [] + + with seal_numerical_roles(m): + lease = it.next() + while lease is not None: + arena_meters.append(lease.actual.context.arena.meter) + if m.route.selected_leaf(it, lease): + break + lease.close() + lease = it.next() + need(lease is not None, 'selected physical nonroot leaf') + borrowed_result = lease.actual.result['stream'] + result_before = bytes(borrowed_result.cells), borrowed_result.head + m.route.emit_headers(m.join, it, lease, headers, width) + observed_headers = {name: ''.join(tape.cells) for name, tape in headers.items()} + observed_headers['width'] = ''.join(width.cells) + produced = m.rom.execute(m.rom_program, service) + need(produced['status'] == 'accept' and all(h == 0 for h in produced['heads'].values()), + 'actual encoded ROM production and head return') + m.route.prepare_keys(m.join, record, layers, width, index, address, countdown, row, reverse) + machines, radix_tape_actions = literal_radix(m, record, width, buckets) + need((bytes(source.cells), source.head) == borrowed_source and + (bytes(borrowed_result.cells), borrowed_result.head) == result_before and + lease.actual.guide.head == 1 and it.counters['axis'].head == 1 and + it.counters['half'].head == 1, + 'live source, result and borrowed heads preserved before staging') + endpoint.stage(lease) + lease.close() + endpoint.commit() + if not it.closed: + it.close() + + width.erase() + layers.erase() + rom.erase() + for tape in headers.values(): + tape.erase() + need(all(p.head == 1 and all(c == m.w.BLANK for c in p.cells) for p in numeric_ports), + 'all acquired encoded CRT ports retired') + need(all(p.head == 0 and all(c == '_' for c in p.cells) for p in adapter_ports) + and all(all(c == '_' for c in cells) for cells in service.values()), + 'all encoded metadata and ROM histories retired') + need(all(t.head == 0 and not t.cells for t in buckets) and + all(machine.status == 'accept' and not any(machine.registers) for machine in machines), + 'all literal bucket and finite control histories retired') + need(source.head == 1 and payload.head == 0, 'both physical boundary heads returned') + + symbol_cells = [p.cells for p in numeric_ports] + symbol_cells += [width.cells, index.cells, address.cells, countdown.cells, row.cells] + symbol_cells += list(service.values()) + need(len({id(cells) for cells in symbol_cells}) == len(symbol_cells), + 'disjoint retained symbol roles') + receipt = dict( + direction='inverse' if reverse else 'forward', + selected_nodes=1, + skipped_nodes=len(arena_meters) - 1, + observed_headers=observed_headers, + encoded_source_symbol_actions=sum(meter_actions(p.meter) for p in (source, *numeric_ports)) + - source_before + sum(meter_actions(meter) for meter in arena_meters), + adapter_symbol_actions=sum(p.actions for p in adapter_ports), + benes_instructions=produced['steps'], + radix_bit_control_instructions=sum(sum(machine.census.values()) for machine in machines), + radix_passes=len(machines), + payload_adapter_bit_actions=bit_actions((payload, *buckets)) - payload_before - radix_tape_actions, + retained_symbol_roles=len(symbol_cells), + retained_symbol_cells=sum(map(len, symbol_cells)), + retained_bucket_bits=sum(t.extent for t in buckets), + retained_radix_register_bits=sum(len(machine.registers) for machine in machines), + retained_benes_registers=len(produced['registers']), + ) + return receipt, (symbol_cells, buckets, machines, produced) + + +def initial_fixture(m): + # External fixture encoding happens before the measured input boundary. + case = m.fixture + source, coordinates = m.e.Port(m.w), [] + for width, modulus, value in zip(case['widths'], case['moduli'], case['initial'], strict=True): + source.append(m.r.ROOT) + for _ in range(width): + source.append(m.w.ONE) + source.append(m.r.WORD_END) + for bit in range(width): + source.append((modulus >> bit) & 1) + source.append(m.r.WORD_END) + cells = [] + for bit in range(width): + cells.append(source.head) + source.append((value >> bit) & 1) + coordinates.append(tuple(cells)) + source.append(m.r.RECORD_END) + source.append(m.w.RIGHT) + source.rewind() + source.cells.extend([m.w.ONE, m.w.ZERO, m.w.BLANK] * 3) + + width = case['widths'][-1] + need(len(TAGS) == 1 << width and len(set(TAGS)) == len(TAGS) and all(TAGS), 'marked fixture') + symbols = ['<'] + for position, tag in enumerate(TAGS): + symbols.extend((('R', tag), *format(position, f'0{width}b'))) + symbols.append('>') + packet = tuple(bit for symbol in symbols for bit in m.binary.bits(symbol)) + return source, m.bit_tape(packet), coordinates + + +def coordinates(source, fields): + return [sum(source.cells[cell] << bit for bit, cell in enumerate(field)) for field in fields] + + +def observe_payload(tape, width): + # The observer sees sparse physical bit backing. The runtime above never decodes a key. + def codeword(position): + return sum(tape.cells.get(13 * position + bit, 0) << bit for bit in range(13)) + need(codeword(0) == 5, 'observed payload origin') + observed = [] + at = 1 + while codeword(at) != 6: + payload = codeword(at) + need(4096 <= payload < 8192, 'observed opaque code') + key = 0 + at += 1 + for _ in range(width): + symbol = codeword(at) + need(symbol in (2, 3), 'observed key bit') + key = 2 * key + symbol - 2 + at += 1 + observed.append((key, payload - 4096)) + return observed + + +def direct_oracle(case): + start = case['start'] + left, right = case['moduli'][start:start + 2] + lower = case['initial'][start] + need(case['level'] == 1 and lower < left, 'oracle for a valid two-axis leaf') + offset, = [i for i in range(right) if (left * i - lower) % right == 0] + dest = [(x + offset) % right if x < right else x for x in range(len(TAGS))] + need(len(set(dest)) == len(TAGS), 'direct CRT permutation') + return dest, sorted(zip(dest, TAGS, strict=True)) + + +def reverse_order_control(m): + # Two noncommuting involutions make the control sensitive to row order, + # since the fixture's modulus-two rotation alone cannot distinguish it. + def observed(reverse): + out = [] + for initial in range(4): + address = m.join.Tape(list('L' + format(initial, '02b')[::-1] + 'R')) + layers = m.join.Tape(list('L1100|0101|0000|R')) + width = m.join.Tape(list('L11R')) + m.route.route_address(m.join, layers, width, address, m.join.Tape(), m.join.Tape(), reverse) + out.append(sum(int(bit) << i for i, bit in enumerate(address.cells[1:3]))) + return out + need(observed(False) == [3, 0, 2, 1] and observed(True) == [1, 3, 2, 0], + 'reversed noncommuting row control') + return 'noncommuting rows distinguish traversal order' + + +def truncated_layers_control(m): + try: + m.route.route_address(m.join, m.join.Tape(list('L1100|R')), m.join.Tape(list('L11R')), + m.join.Tape(list('L00R')), m.join.Tape(), m.join.Tape(), False) + except ValueError as exc: + need(str(exc) == 'missing descending ROM layers', 'specific truncated-layer rejection') + return 'truncated width-two layer stream rejected' + raise ValueError('truncated layer stream accepted') + + +def replay(m): + source, payload, fields = initial_fixture(m) + source_cells, payload_cells = id(source.cells), id(payload.cells) + source_initial = bytes(source.cells), source.head + payload_initial = dict(payload.cells), payload.head + oracle_dest, oracle_forward = direct_oracle(m.fixture) + forward, first = run_leg(m, source, payload, False) + observed = observe_payload(payload, m.fixture['widths'][-1]) + need(observed == oracle_forward and oracle_dest != list(range(len(TAGS))), + 'independent nonidentity forward payload placement') + need(coordinates(source, fields) == m.fixture['forward'], 'retained independent source endpoint') + coordinate_cells = set().union(*fields) + need(len(source.cells) == len(source_initial[0]) and + all(source.cells[i] == bit for i, bit in enumerate(source_initial[0]) + if i not in coordinate_cells), 'source metadata and inaccessible tail unchanged') + inverse, second = run_leg(m, source, payload, True) + need((bytes(source.cells), source.head) == source_initial and id(source.cells) == source_cells, + 'actual full source and head restored') + need((payload.cells, payload.head) == payload_initial and id(payload.cells) == payload_cells, + 'actual full payload frame, keys and head restored') + all_symbol_cells = [*first[0], *second[0]] + need(len({id(c) for c in all_symbol_cells}) == len(all_symbol_cells), + 'both directions retain distinct symbol histories') + + expected_headers = {'h': 'L01000R', 'modulus': 'L01000R', 'selected_layer': 'L00000R', + 'offsets': 'L10000|R', 'width': 'L11R'} + need(forward['observed_headers'] == inverse['observed_headers'] == expected_headers, + 'same live encoded offset and width in both directions') + controls = [reverse_order_control(m), truncated_layers_control(m)] + prior_query = m.join.select_row_bit + def suppress(*args): + prior_query(*args) + return '0' + try: + m.join.select_row_bit = suppress + bad_source, bad_payload, _ = initial_fixture(m) + run_leg(m, bad_source, bad_payload, False) + need(observe_payload(bad_payload, m.fixture['widths'][-1]) == list(enumerate(TAGS)) + and list(enumerate(TAGS)) != oracle_forward, + 'no-switch control must fail the forward oracle') + finally: + m.join.select_row_bit = prior_query + controls.append('suppressed switches fail the forward oracle') + return { + 'status': 'PASS_ENCODED_CRT_LEAF_PAYLOAD', + 'fixture': m.fixture['name'], + 'moduli': m.fixture['moduli'], + 'widths': m.fixture['widths'], + 'input_tags': TAGS, + 'forward_destinations': oracle_dest, + 'forward_tags': [value for _, value in observed], + 'forward_source': m.fixture['forward'], + 'restored_source_and_payload': True, + 'source_cells_retained': len(source.cells), + 'payload_bits_visited': payload.extent, + 'forward_and_inverse': [forward, inverse], + 'control_cases': controls, + 'benes_program_instructions': len(m.rom_program), + 'radix_program_instructions': len(m.program), + } + + +if __name__ == '__main__': + parser = ArgumentParser(description=__doc__) + parser.add_argument('--write-result', type=Path) + args = parser.parse_args() + result = replay(modules()) + text = json.dumps(result, indent=2, sort_keys=True) + '\n' + if args.write_result: + with args.write_result.open('x') as stream: + stream.write(text) + else: + need(text == (HERE / 'RESULT.json').read_text(), 'exact committed payload receipt') + print(result['status'], 'markers=4 padded=2 forward_and_inverse=2 controls=3') diff --git a/research/encoded-crt-leaf-payload/route.py b/research/encoded-crt-leaf-payload/route.py new file mode 100644 index 0000000000..b6b5e1573a --- /dev/null +++ b/research/encoded-crt-leaf-payload/route.py @@ -0,0 +1,277 @@ +"""Join an encoded CRT leaf to the existing physical payload mover. Apache-2.0.""" + +BITS = ('0', '1') + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def end_word(tape): + tape.write('R') + tape.rewind() + + +def increment(tape): + """Increment a framed little-endian binary word, returning its carry.""" + tape.step(1) + carry = True + while tape.read() != 'R': + bit = tape.read() + need(bit in BITS, 'binary counter bit') + if carry: + tape.write('0' if bit == '1' else '1') + carry = bit == '1' + tape.step(1) + tape.rewind() + return carry + + +def copy_bits(source, target): + target.emit('L') + source.step(1) + while source.read() != 'R': + bit = source.read() + need(bit in BITS, 'framed binary word') + target.emit(bit) + source.step(1) + source.rewind() + end_word(target) + + +def zero_header(target, guide, words): + target.emit('L') + while guide.read() == words.ONE: + target.emit('0') + guide.step(1) + need(guide.read() == words.BLANK, 'precision guide terminator') + guide.rewind() + end_word(target) + + +def selected_leaf(iterator, lease): + half, axis = iterator.counters['half'], iterator.counters['axis'] + words = iterator.w + need(half.read() == words.ONE, 'nonempty current half') + half.step(1) + one = half.read() == words.RIGHT + half.rewind() + return one and lease.actual.last and axis.read() != iterator.r.STEP + + +def emit_headers(join, iterator, lease, headers, width): + words, records, source = iterator.w, iterator.r, iterator.source + axis = iterator.counters['axis'] + guide = lease.actual.guide + result = lease.actual.result['stream'] + zero_header(headers['h'], guide, words) + zero_header(headers['selected_layer'], guide, words) + while axis.read() != records.STEP: + need(axis.read() == words.ONE, 'encoded nonroot prefix') + iterator._record() + axis.step(1) + iterator._record() # The admitted leaf has exactly one left record. + + need(source.read() == records.ROOT, 'right axis record') + source.step(1) + width.emit('L') + while source.read() == words.ONE: + width.emit('1') + need(not increment(headers['h']), 'encoded width fits precision guide') + source.step(1) + need(source.read() == records.WORD_END, 'right width delimiter') + source.step(1) + end_word(width) + + modulus = headers['modulus'] + modulus.emit('L') + width.step(1) + while width.read() == '1': + bit = source.read() + need(bit in (words.ZERO, words.ONE) and guide.read() == words.ONE, + 'right modulus fits precision guide') + modulus.emit('1' if bit == words.ONE else '0') + source.step(1) + guide.step(1) + width.step(1) + need(width.read() == 'R' and source.read() == records.WORD_END, + 'right modulus delimiter') + width.rewind() + source.step(1) + while guide.read() == words.ONE: + modulus.emit('0') + guide.step(1) + need(guide.read() == words.BLANK, 'modulus padding terminator') + end_word(modulus) + guide.rewind() + + width.step(1) + while width.read() == '1': + need(source.read() in (words.ZERO, words.ONE), 'right coordinate bit') + width.step(1) + source.step(1) + need(width.read() == 'R' and source.read() == records.RECORD_END, + 'right coordinate delimiter') + source.step(1) + need(source.read() == words.RIGHT, 'selected right axis is last') + source.rewind() + axis.rewind() + width.rewind() + + need(result.read() == records.ROOT, 'actual offset record') + result.step(1) + join.copy_numeric_field(result, headers['offsets'], guide, words, records.WORD_END, '|') + result.rewind() + + +def toggle_target(width, address, switch): + # The physical mark records the current target. Both counters are scanned + # by their symbols, and the width head returns to the marked bit. + need(width.read() == '1', 'target is a width cell') + width.write('|') + width.rewind() + width.step(1) + address.step(1) + while width.read() == '1': + width.step(1) + address.step(1) + bit = address.read() + need(width.read() == '|' and bit in BITS and switch in BITS, 'target bit') + if switch == '1': + address.write('1' if bit == '0' else '0') + width.write('1') + address.rewind() + + +def next_target(width, ascending): + width.step(1 if ascending else -1) + if ascending and width.read() == 'R': + width.step(-1) + width.step(-1) + ascending = False + need(width.read() == '1', 'more layers than encoded target positions') + return ascending + + +def previous_delimiter(layers): + layers.step(-1) + while layers.read() in BITS: + layers.step(-1) + need(layers.read() in ('L', '|'), 'physical layer prefix') + + +def route_address(join, layers, width, address, countdown, row, reverse): + """Follow all physical rows using the retained selected-row query.""" + layers.step(1) + if reverse: + while layers.read() != 'R': + need(layers.read() in (*BITS, '|'), 'complete layer tape') + layers.step(1) + layers.step(-1) + width.step(1) + ascending = True + while True: + if reverse: + need(layers.read() == '|', 'reverse layer end') + previous_delimiter(layers) + layers.step(1) + row.emit('L') + seen = False + while layers.read() in BITS: + seen = True + row.emit(layers.read()) + layers.step(1) + need(seen and layers.read() == '|', 'nonempty delimited ROM row') + end_word(row) + copy_bits(address, countdown) + switch = join.select_row_bit(row, countdown) + toggle_target(width, address, switch) + row.erase() + + if reverse: + previous_delimiter(layers) + done = layers.read() == 'L' + else: + layers.step(1) + done = layers.read() == 'R' + if done: + break + ascending = next_target(width, ascending) + if ascending: + width.step(1) + need(width.read() == 'R', 'missing descending ROM layers') + width.step(-1) + width.step(-1) + need(width.read() == 'L', 'complete palindromic target sequence') + layers.rewind() + + +class RecordTape: + """Paid scans and writes on the retained literal radix ABI.""" + def __init__(self, binary, tape): + self.tape = tape + self.codes = {symbol: binary.bits(symbol) for symbol in ('<', '>', '0', '1')} + + def move_word(self, direction): + for _ in self.codes['<']: + self.tape.move(direction) + + def matches(self, symbol): + equal = True + for bit in self.codes[symbol]: + actual = self.tape.read() + equal = equal and actual == bit + self.tape.move(1) + self.move_word(-1) + return equal + + def emit(self, symbol): + for bit in self.codes[symbol]: + self.tape.write(bit) + self.tape.move(1) + + def pass_payload(self): + # Twelve opaque bits and one tag, in the pinned 13-bit ABI. + for _ in range(12): + self.tape.move(1) + need(self.tape.read() == 1, 'actual opaque payload codeword') + self.tape.move(1) + + def rekey(self, address): + address.step(1) + while address.read() in BITS: + address.step(1) + need(address.read() == 'R', 'destination key terminator') + address.step(-1) + while address.read() != 'L': + bit = address.read() + need(bit in BITS and (self.matches('0') or self.matches('1')), + 'one allocated key bit') + self.emit(bit) + address.step(-1) + + +def prepare_keys(join, record, layers, width, index, address, countdown, row, reverse): + need(record.matches('<'), 'physical payload frame begins at origin') + record.move_word(1) + index.emit('L') + width.step(1) + while width.read() == '1': + index.emit('0') + width.step(1) + need(width.read() == 'R', 'encoded payload width') + width.rewind() + end_word(index) + while True: + record.pass_payload() + copy_bits(index, address) + route_address(join, layers, width, address, countdown, row, reverse) + record.rekey(address) + address.erase() + if increment(index): + break + need(record.matches('>'), 'payload occupies precisely the padded rectangle') + while not record.matches('<'): + record.move_word(-1) + index.erase() diff --git a/research/encoded-crt-two-target-payload/README.md b/research/encoded-crt-two-target-payload/README.md new file mode 100644 index 0000000000..bd3066a36e --- /dev/null +++ b/research/encoded-crt-two-target-payload/README.md @@ -0,0 +1,123 @@ +# Fuse two encoded CRT payload sorts + +One live balanced CRT root now routes both right axes of the retained +`two_short_first` fixture. One combined destination key sorts its complete +16-record right-side rectangle in four literal radix passes. A matched +forward execution that sorts after each axis reaches the same exact frame in +eight passes. The fused inverse restores the entire input frame, encoded +source, physical backing and entry heads. + +The fixture has moduli `(5,7,3,2)`, declared widths `(3,3,2,2)` and input +source `(1,5,2,1)`. The source becomes `(1,5,0,0)` and then returns to +`(1,5,2,1)`. Original tag `293` moves from slot 0 to slot 5. The independent +CRT oracle checks all 16 slots before accepting restoration. The primary +execution covers one fixed left state and its full padded right rectangle. + +## Source and payload join + +1. Select the live root from the retained #7352 iterator. The encoded axis + cursor is at its first marker and the lease ends at the source suffix. + The forward leg pays for two earlier read-only leaves. The inverse sees + the root first and retires the remaining iterator after the root. +2. Walk the borrowed right source and numerical result in the same order. + Copy each physical unary width and modulus and the corresponding P-bit + offset. Consume each complete updated-coordinate field and require both + terminal markers. The width sum supplies the radix pass count. Check that + the borrowed tapes and their heads are unchanged before staging. +3. Run the existing encoded Beneš program once for each target on the same + private and output backing. For each call, scan the actual payload tape. + Two encoded position counters identify the current slot. Query all + physical switch rows for the selected axis and write only that axis's key + field. Skip the other field using its live unary width. Clear both ROM + outputs and the active headers before reusing the bank. +4. Sort the entire frame once with the unchanged literal binary radix + program. Stage the whole-node result, retire the numerical lease, then + commit the source. The inverse reverses the row sequence within each + target and repeats the same frame procedure. + +For the fixed current left source, the independent oracle solves +`k ≡ 1 mod 5` and `k ≡ 5*5 mod 7`, so `k = 11` in `[0,35)`. For the two +right axes it solves `35*c ≡ 11 mod 3` and `105*c ≡ 11 mod 2`. Both +positive offsets are 1. The two axis maps on their padded four-slot +coordinates are `f = [1,2,0,3]` and `g = [1,0,2,3]`. A padded coordinate +is fixed on its own axis while the other coordinate can still move. + +At physical position `4*a+b` the fused scan writes `f(a)` and `g(b)` into +the two fields before any record moves. The staged sort first puts that +record at `4*f(a)+b` with the key for its new physical slot. Counting +positions afresh at the second scan gives the same full key `4*f(a)+g(b)`. +This argument uses that the permutations act on separate fields and that +the offsets depend on the preserved left source and modulus prefix. Reversing +the layers of each axis inverts its permutation. Four stable last-bit passes +both sort the four-bit keys and restore their bit order. + +## Observed work and storage + +| Quantity | Fused forward | Staged forward | Fused inverse | +| --- | ---: | ---: | ---: | +| Literal radix passes | 4 | 8 | 4 | +| Literal radix bit and control instructions | 492,724 | 985,448 | 492,724 | +| Payload adapter bit actions, including bucket markers | 19,272 | 19,428 | 19,272 | +| Adapter symbol actions | 25,906 | 25,928 | 28,594 | +| Encoded source symbol actions | 373,976 | 373,976 | 264,989 | +| Beneš producer instructions | 9,681,707 | 9,681,707 | 9,681,707 | +| Actual row queries | 96 | 96 | 96 | +| Retained private symbol cells | 4,309 | 4,309 | 4,308 | +| Retained literal radix register bits | 288 | 576 | 288 | + +The forward comparison saves 492,724 radix instructions and 156 bit-tape +marker actions. The comparator uses the same full-frame radix ABI and +performs one complete sort after each of the two axis scans. It models this +specific staged route. The shared ROM backing retains 3,031 private/output +cells at the end of either target, apart from the charged header storage. +Each execution retains 30 Beneš register symbols, 1,092 bucket bits and 143 +private symbol roles. The fused round trip shares one 57-cell source and one +payload tape with a visited extent of 1,067 bits. The two legs retain their +private banks separately. + +Counts use the respective source, symbol and binary execution models. +Fixture serialization and independent observers sit outside the measured +call. A common literal tariff, a complete multiplication caller and a +change in the asymptotic saving κ remain open. + +## Replay and source credit + +Run the registered package or direct replay with Python 3.12. + +```sh +python3.12 -B scripts/research_package.py --package research/encoded-crt-two-target-payload +python3.12 -I -B research/encoded-crt-two-target-payload/replay.py +``` + +[RESULT.json](RESULT.json) records all three executions and the exact maps. +The dropped fast target control still commits the correct source but puts +tag `293` in slot 4. The retained `growing_bank` case separately checks +unequal widths and unequal offsets on the live header path. Reusing its +first offset for its second fails the ordered header oracle. The replay +also retains the noncommuting inverse-row-order and truncated-row controls. + +[SOURCES.json](SOURCES.json) binds the live inputs to canonical main +`e54523517d0f03e58352e647c403a5af3e525a57` and the exact [#7388 predecessor](https://github.com/CrocSwap/integer-mult-bounds/pull/7388) +`d6f4a69202ad0bba4a915f4d4f3eaba1fe431c86`. This package imports its loader, +full-layer row traversal and literal radix wrapper without copying them. +The retained #7388 pins identify CubeJerry's [#7352](https://github.com/CrocSwap/integer-mult-bounds/pull/7352) +encoded endpoint and the shared forward writer from [#7351](https://github.com/CrocSwap/integer-mult-bounds/pull/7351). +Commdata2338's [#5519](https://github.com/CrocSwap/integer-mult-bounds/pull/5519) +at `53a034436f17ef5b8fdf7a02f5066528cdfe5446` supplies the fixture and +shared-bank alignment invariant. Ali Romman's +[#5625](https://github.com/CrocSwap/integer-mult-bounds/pull/5625) supplies +predecessor retirement evidence. JoyboyBrian's [#5092](https://github.com/CrocSwap/integer-mult-bounds/pull/5092), +[#5496](https://github.com/CrocSwap/integer-mult-bounds/pull/5496) and +[#5015](https://github.com/CrocSwap/integer-mult-bounds/pull/5015) supply +the producer, row query and literal consumer. OpenAI Codex and ChatGPT Pro +materially assisted. Pro derived the independent slot map and checked the +isolated radix component with supplied keys. Apache-2.0. + +## Open next questions + +To transfer this result into an actual multiplier, first bind a caller's +full normalized transform returns, payload layout and original-coordinate +extraction to the encoded source contract across left states. The next +product-level acceptance check +must use a production-admitted catalogue, consume the actual transform +returns and recover an exact integer product through CRT and carry. diff --git a/research/encoded-crt-two-target-payload/RESULT.json b/research/encoded-crt-two-target-payload/RESULT.json new file mode 100644 index 0000000000..e73d1fc197 --- /dev/null +++ b/research/encoded-crt-two-target-payload/RESULT.json @@ -0,0 +1,265 @@ +{ + "controls": { + "dropped_fast_first_tag_actual_slot": 4, + "dropped_fast_first_tag_required_slot": 5, + "noncommuting_row_order": true, + "ordered_header_alignment": { + "case": "growing_bank", + "headers": [ + { + "h": "L01000000000R", + "modulus": "L11000000000R", + "offsets": "L00000000000|R", + "selected_layer": "L00000000000R", + "width": "L11R" + }, + { + "h": "L11000000000R", + "modulus": "L11100000000R", + "offsets": "L10100000000|R", + "selected_layer": "L00000000000R", + "width": "L111R" + } + ], + "stale_second_offset_rejected": true + }, + "truncated_layers_rejected": true + }, + "executions": [ + { + "adapter_symbol_actions": 25906, + "benes_instructions": 9681707, + "encoded_source_symbol_actions": 373976, + "headers": [ + { + "h": "L01000000000R", + "modulus": "L11000000000R", + "offsets": "L10000000000|R", + "selected_layer": "L00000000000R", + "width": "L11R" + }, + { + "h": "L01000000000R", + "modulus": "L01000000000R", + "offsets": "L10000000000|R", + "selected_layer": "L00000000000R", + "width": "L11R" + } + ], + "mode": "fused_forward", + "payload_adapter_bit_actions": 19272, + "payload_visited_bits": 1067, + "producer_calls": 2, + "radix_bit_control_instructions": 492724, + "radix_instructions_by_pass": [ + 123181, + 123181, + 123181, + 123181 + ], + "retained_benes_registers": 30, + "retained_bucket_bits": 1092, + "retained_radix_register_bits": 288, + "retained_rom_bank_cells_after_each_target": [ + 3031, + 3031 + ], + "retained_symbol_cells": 4309, + "retained_symbol_roles": 143, + "row_queries": 96, + "skipped_leases": 2 + }, + { + "adapter_symbol_actions": 28594, + "benes_instructions": 9681707, + "encoded_source_symbol_actions": 264989, + "headers": [ + { + "h": "L01000000000R", + "modulus": "L11000000000R", + "offsets": "L10000000000|R", + "selected_layer": "L00000000000R", + "width": "L11R" + }, + { + "h": "L01000000000R", + "modulus": "L01000000000R", + "offsets": "L10000000000|R", + "selected_layer": "L00000000000R", + "width": "L11R" + } + ], + "mode": "fused_inverse", + "payload_adapter_bit_actions": 19272, + "payload_visited_bits": 1067, + "producer_calls": 2, + "radix_bit_control_instructions": 492724, + "radix_instructions_by_pass": [ + 123181, + 123181, + 123181, + 123181 + ], + "retained_benes_registers": 30, + "retained_bucket_bits": 1092, + "retained_radix_register_bits": 288, + "retained_rom_bank_cells_after_each_target": [ + 3031, + 3031 + ], + "retained_symbol_cells": 4308, + "retained_symbol_roles": 143, + "row_queries": 96, + "skipped_leases": 0 + }, + { + "adapter_symbol_actions": 25928, + "benes_instructions": 9681707, + "encoded_source_symbol_actions": 373976, + "headers": [ + { + "h": "L01000000000R", + "modulus": "L11000000000R", + "offsets": "L10000000000|R", + "selected_layer": "L00000000000R", + "width": "L11R" + }, + { + "h": "L01000000000R", + "modulus": "L01000000000R", + "offsets": "L10000000000|R", + "selected_layer": "L00000000000R", + "width": "L11R" + } + ], + "mode": "staged_forward", + "payload_adapter_bit_actions": 19428, + "payload_visited_bits": 1067, + "producer_calls": 2, + "radix_bit_control_instructions": 985448, + "radix_instructions_by_pass": [ + 123181, + 123181, + 123181, + 123181, + 123181, + 123181, + 123181, + 123181 + ], + "retained_benes_registers": 30, + "retained_bucket_bits": 1092, + "retained_radix_register_bits": 576, + "retained_rom_bank_cells_after_each_target": [ + 3031, + 3031 + ], + "retained_symbol_cells": 4309, + "retained_symbol_roles": 143, + "row_queries": 96, + "skipped_leases": 2 + } + ], + "fixture": "two_short_first", + "forward_destinations": [ + 5, + 4, + 6, + 7, + 9, + 8, + 10, + 11, + 1, + 0, + 2, + 3, + 13, + 12, + 14, + 15 + ], + "forward_radix_instructions_saved": 492724, + "forward_source": [ + 1, + 5, + 0, + 0 + ], + "forward_tags": [ + 1472, + 1341, + 1603, + 1734, + 424, + 293, + 555, + 686, + 948, + 817, + 1079, + 1210, + 1996, + 1865, + 2127, + 2258 + ], + "input_source": [ + 1, + 5, + 2, + 1 + ], + "input_tags": [ + 293, + 424, + 555, + 686, + 817, + 948, + 1079, + 1210, + 1341, + 1472, + 1603, + 1734, + 1865, + 1996, + 2127, + 2258 + ], + "inverse_destinations": [ + 9, + 8, + 10, + 11, + 1, + 0, + 2, + 3, + 5, + 4, + 6, + 7, + 13, + 12, + 14, + 15 + ], + "moduli": [ + 5, + 7, + 3, + 2 + ], + "reconstructed_left": 11, + "restored_source_and_payload": true, + "source_retained_cells": 57, + "status": "PASS_ENCODED_CRT_TWO_TARGET_PAYLOAD", + "widths": [ + 3, + 3, + 2, + 2 + ] +} diff --git a/research/encoded-crt-two-target-payload/SOURCES.json b/research/encoded-crt-two-target-payload/SOURCES.json new file mode 100644 index 0000000000..b89191873a --- /dev/null +++ b/research/encoded-crt-two-target-payload/SOURCES.json @@ -0,0 +1,145 @@ +{ + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "git_blob": "8d4ba37e2778acb35b34e0719df2caf138fbeb50", + "path": "research/r437-preparation-composition/predecessor4025/source/words.py", + "sha256": "5c37f57708ba3131bdcb03139f9dbc29886bee44569c09cbba51b68f75acd7f9", + "usage": "input" + }, + { + "git_blob": "4f00467a0ff580954ad2fd0c7380240c753ddef3", + "path": "research/r437-preparation-composition/predecessor4025/source/records.py", + "sha256": "0c9c4b23e998597fb877bb1a29da69ac869b68262abe635b162b4dba9c69b372", + "usage": "input" + }, + { + "git_blob": "1fa2b0cb88320d4f5b623554bb0fc6de332b773c", + "path": "research/encoded-crt-entry-lifecycle/entry.py", + "sha256": "0537ec98f306270c8ff6a424841886cf53f675d9947029347090c7dc779616d7", + "usage": "input" + }, + { + "git_blob": "a327b0161eca57a1cc44ec2aa8e3defed2167ddc", + "path": "research/encoded-current-crt/producer.py", + "sha256": "88dab4ca02a92164a67826db361214fa1405e4b4a588f8c4279a21bcee95ab76", + "usage": "input" + }, + { + "git_blob": "20ef3519b6fef691ec92b7315e320b5e8ce9bf18", + "path": "research/crt-persistent-numerical-owner/owner.py", + "sha256": "1d73f432f8de9c791260c43335eb207d82bbb3f5b190cc76d0d914a4db076f41", + "usage": "input" + }, + { + "git_blob": "57f6853e262a6136bc616f1e47a31d0ace28495c", + "path": "research/crt-mixed-row-entry/bridge.py", + "sha256": "89c38638c0d66da731566c903c32e7fa1ad31088d29cfd2634fce823dd07c1f9", + "usage": "input" + }, + { + "git_blob": "676582b4a376db375237ec52df84a3ddaf231827", + "path": "research/crt-current-row-query/join.py", + "sha256": "11c9ac1175a45edae80869b22c041e31a1b5cc75f4389ec2e073de37e547bf35", + "usage": "input" + }, + { + "git_blob": "052b01a83bc910c176b83a012b9f46f0e9525b9d", + "path": "research/crt-encoded-benes-rom-producer/microcode.py", + "sha256": "d4af5350854a87b67484840800b94e1e53cff82c78ec0f2a91753fed9ea70af7", + "usage": "input" + }, + { + "git_blob": "88292ce98d31d540c7dba6960bfe4c19f06a8077", + "path": "research/crt-uniform-rom-query/machine.py", + "sha256": "46ee6a635251e498ee9a5d4aff8c0e2a7f1ef2ff951e5b6a2a8953316e9cd02d", + "usage": "input" + }, + { + "git_blob": "ec574f26d6f64ead00d7c2cf5b808c0498b460cf", + "path": "research/crt-binary-key-port/binary.py", + "sha256": "50a3dea7fc087715b4e605e85629566ed31903026540f916df6b8cbaa536182d", + "usage": "input" + }, + { + "git_blob": "f558019fe70c46bcb2f087464c1d2aa021b7188d", + "path": "research/crt-binary-radix-consumer/radix.py", + "sha256": "f4200a495d9c445474275214254d46e9a8e03967a635263905a4c9192bb36f1f", + "usage": "input" + }, + { + "git_blob": "832d3312df223d1b151e5c620cc3d4e295f49e05", + "path": "research/crt-paid-row-reentry/RESULT.json", + "sha256": "d818bffac4647dffaf525ed68dbb79dc575a00303af3315c6d4fe39b60f49a13", + "usage": "input" + }, + { + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "path": "certificates/selected-result.json", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1", + "usage": "provenance" + }, + { + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "path": "docs/research/agent-task-catalog.json", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81", + "usage": "provenance" + }, + { + "git_blob": "41f6f41c98cd3728abc21a560543938b58b303e2", + "path": "research/encoded-crt-leaf-payload/INPUT-PINS.json", + "pin": "head:d6f4a69202ad0bba4a915f4d4f3eaba1fe431c86:research/encoded-crt-leaf-payload/INPUT-PINS.json", + "sha256": "2e06f6515bef4166f987f06d678ae3bbb2837e4da6c48514c1ca7d82d86614fd", + "usage": "input" + }, + { + "git_blob": "75ad7270542d18704ae5b1f8b6ffa29e58741d00", + "path": "research/encoded-crt-leaf-payload/replay.py", + "pin": "head:d6f4a69202ad0bba4a915f4d4f3eaba1fe431c86:research/encoded-crt-leaf-payload/replay.py", + "sha256": "31e6f9e4b91fb67c40ee27e4d8ee6b4d1b2674efd9bb7e361bf7de879c188761", + "usage": "input" + }, + { + "git_blob": "b6b5e1573a7984ee7189b85709085c73254e1569", + "path": "research/encoded-crt-leaf-payload/route.py", + "pin": "head:d6f4a69202ad0bba4a915f4d4f3eaba1fe431c86:research/encoded-crt-leaf-payload/route.py", + "sha256": "d17eecceb43c5327a35dd7b903e33f48aef46c803d6b8a54dfc6ec54c2ec9b36", + "usage": "input" + }, + { + "git_blob": "b084d893bdb2ce5571ef00196a9ec6a60e723964", + "path": "research/encoded-crt-leaf-payload/frozen/endpoint.py", + "pin": "head:d6f4a69202ad0bba4a915f4d4f3eaba1fe431c86:research/encoded-crt-leaf-payload/frozen/endpoint.py", + "sha256": "c24ae2c90d175d276120438809e7c7401b8a8c04dec139f1b7345e9778984ced", + "usage": "input" + }, + { + "git_blob": "8adbe2cfef74da9854ed0b70b6c221f5746efa9f", + "path": "research/encoded-crt-leaf-payload/frozen/frontend.py", + "pin": "head:d6f4a69202ad0bba4a915f4d4f3eaba1fe431c86:research/encoded-crt-leaf-payload/frozen/frontend.py", + "sha256": "6ec9aab626a9d7a229b6f13ce6863e1ca77fa30ef65a4a66ae03a6ffaf2ee78c", + "usage": "input" + }, + { + "git_blob": "17abfb8500043bcdeb656094bb0213d911d986fc", + "path": "research/encoded-crt-leaf-payload/frozen/inverse_frontend.py", + "pin": "head:d6f4a69202ad0bba4a915f4d4f3eaba1fe431c86:research/encoded-crt-leaf-payload/frozen/inverse_frontend.py", + "sha256": "0e5f4c9450372c90000f5ebf3c22dfbe7241dd53da9ae9bcce310af859b009ef", + "usage": "input" + }, + { + "git_blob": "46bf6ef4e2dfa53bca17ac668914b1a842eaba9e", + "path": "research/encoded-crt-leaf-payload/frozen/inverse_producer.py", + "pin": "head:d6f4a69202ad0bba4a915f4d4f3eaba1fe431c86:research/encoded-crt-leaf-payload/frozen/inverse_producer.py", + "sha256": "6acdebee7134fbc8e2d121060286bd05e7282900da8a28a78c80937dde7ea178", + "usage": "input" + }, + { + "git_blob": "81633db5c1fa0e4614891e7091d0ca82acd5f3c9", + "path": "research/crt-multitarget-row-audit/verify.py", + "sha256": "971111b8418d9b3234b0441bbfb424ede574bc45b9996839093a377b694c0a41", + "usage": "input" + } + ], + "schema_version": 1 +} diff --git a/research/encoded-crt-two-target-payload/TASK.json b/research/encoded-crt-two-target-payload/TASK.json new file mode 100644 index 0000000000..51ffcddb5b --- /dev/null +++ b/research/encoded-crt-two-target-payload/TASK.json @@ -0,0 +1,83 @@ +{ + "actual_scope": "One fixed-left, four-axis mixed-width root with two nonidentity right permutations and 16 marked records. Execute the fused forward and inverse, and the matched staged forward comparison.", + "ai_assistance": "OpenAI Codex and ChatGPT Pro materially assisted the formulation, audit, and verification.", + "author": "Clear1nsight", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "Route a full padded right rectangle from one actual two-target encoded CRT root and measure a one-sort versus two-sort execution.", + "budget_minutes": 60, + "evidence": "Separate CRT oracle, exact source and physical payload round trip, measured four versus eight literal passes, shared ROM histories and four controls.", + "open_questions": [ + { + "blocked_by": "The retained padded slice has a fixed left state. A complete normalized caller and common literal cost bound are outside this result.", + "first_step": "Bind one production-admitted catalogue, actual transform returns, original-coordinate extraction and the final CRT/carry boundary.", + "question": "Can a production normalized CRT/Tensor caller feed exact integer recovery?", + "why_it_matters": "The next product-level gate must compare the complete physical output against exact integer multiplication." + } + ], + "original_card": { + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "existing_checks": [ + { + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "status": "author-checked" + }, + { + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "status": "reviewed" + } + ], + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "id": "uniform-transfer-audit", + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ] + }, + "outcome": "completed", + "priority_revision": 8, + "schema_version": 1, + "scope_change_reason": "Extend the previously executed #7388 leaf seam to the retained #5519 two_short_first root, using actual right headers and both key fields.", + "scope_status": "refined", + "stop_rule": "Stop at the retained one-root payload slice, its matched staged forward comparator and targeted controls. Preserve separate tariffs and do not infer a new bound.", + "task_id": "uniform-transfer-audit" +} diff --git a/research/encoded-crt-two-target-payload/VERIFY.json b/research/encoded-crt-two-target-payload/VERIFY.json new file mode 100644 index 0000000000..6bbd7be557 --- /dev/null +++ b/research/encoded-crt-two-target-payload/VERIFY.json @@ -0,0 +1,40 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Compare the exact live two-target source/payload round trip and staged forward; check same bank, paid counts and four controls.", + "timeout_seconds": 120 + } + ], + "inputs": [ + "research/r437-preparation-composition/predecessor4025/source/words.py", + "research/r437-preparation-composition/predecessor4025/source/records.py", + "research/encoded-crt-entry-lifecycle/entry.py", + "research/encoded-current-crt/producer.py", + "research/crt-persistent-numerical-owner/owner.py", + "research/crt-mixed-row-entry/bridge.py", + "research/crt-current-row-query/join.py", + "research/crt-encoded-benes-rom-producer/microcode.py", + "research/crt-uniform-rom-query/machine.py", + "research/crt-binary-key-port/binary.py", + "research/crt-binary-radix-consumer/radix.py", + "research/crt-paid-row-reentry/RESULT.json", + "research/encoded-crt-leaf-payload/INPUT-PINS.json", + "research/encoded-crt-leaf-payload/replay.py", + "research/encoded-crt-leaf-payload/route.py", + "research/encoded-crt-leaf-payload/frozen/endpoint.py", + "research/encoded-crt-leaf-payload/frozen/frontend.py", + "research/encoded-crt-leaf-payload/frozen/inverse_frontend.py", + "research/encoded-crt-leaf-payload/frozen/inverse_producer.py", + "research/crt-multitarget-row-audit/verify.py" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/encoded-crt-two-target-payload/replay.py b/research/encoded-crt-two-target-payload/replay.py new file mode 100644 index 0000000000..63614e3d9f --- /dev/null +++ b/research/encoded-crt-two-target-payload/replay.py @@ -0,0 +1,414 @@ +"""Replay a live two-target CRT root through the retained literal mover. Apache-2.0.""" + +from argparse import ArgumentParser +import ast +from hashlib import sha256 +from importlib.util import module_from_spec, spec_from_file_location +from itertools import product +import json +from math import prod +from pathlib import Path +from unittest.mock import patch + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +FIXTURE_SOURCE = 'research/crt-multitarget-row-audit/verify.py' +PREDECESSOR = 'research/encoded-crt-leaf-payload/replay.py' +TAGS = tuple(293 + 131 * i for i in range(16)) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load(name, path): + spec = spec_from_file_location(name, path) + module = module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def authenticate(): + for pin in json.loads((HERE / 'SOURCES.json').read_text())['files']: + if pin['usage'] == 'input': + content = (ROOT / pin['path']).read_bytes() + need(sha256(content).hexdigest() == pin['sha256'], f'input drift: {pin["path"]}') + + +def retained_cases(): + """Read the exact fixture literals without importing the audit's verifier.""" + tree = ast.parse((ROOT / FIXTURE_SOURCE).read_bytes()) + cases, = [statement.value for statement in tree.body if isinstance(statement, ast.Assign) + and any(isinstance(name, ast.Name) and name.id == 'CASES' for name in statement.targets)] + result = {} + for entry in cases.elts: + need(isinstance(entry, ast.Call) and isinstance(entry.func, ast.Name) + and entry.func.id == 'dict' and not entry.args, 'literal predecessor fixture') + case = {item.arg: ast.literal_eval(item.value) for item in entry.keywords} + result[case['name']] = case + return result + + +def source_fixture(m, case): + """Encode the fixed test input outside the measured call boundary.""" + source, fields = m.e.Port(m.w), [] + for width, modulus, value in zip(case['widths'], case['moduli'], case['state'], strict=True): + source.append(m.r.ROOT) + for _ in range(width): + source.append(m.w.ONE) + source.append(m.r.WORD_END) + for bit in range(width): + source.append((modulus >> bit) & 1) + source.append(m.r.WORD_END) + cells = [] + for bit in range(width): + cells.append(source.head) + source.append((value >> bit) & 1) + fields.append(cells) + source.append(m.r.RECORD_END) + source.append(m.w.RIGHT) + source.rewind() + source.cells.extend([m.w.ONE, m.w.ZERO, m.w.BLANK] * 3) + return source, fields + + +def packet(m, width, tags): + need(len(tags) == 1 << width and len(set(tags)) == len(tags) + and all(0 < t < 4096 for t in tags), 'all slots have distinct nonzero markers') + symbols = ['<'] + for position, tag in enumerate(tags): + symbols.extend((('R', tag), *format(position, f'0{width}b'))) + symbols.append('>') + return tuple(bit for symbol in symbols for bit in m.binary.bits(symbol)) + + +def oracle(case): + """Solve the left congruences by enumeration, then rotate each valid axis.""" + moduli, widths, state = case['moduli'], case['widths'], case['state'] + need(len(state) == 4 and all(x < p for x, p in zip(state[:2], moduli[:2])), + 'independent oracle for the retained valid-left four-axis root') + left, = [z for z in range(prod(moduli[:2])) if all( + (z - state[i] * prod(moduli[:i])) % moduli[i] == 0 for i in range(2))] + offsets = [] + for i in (2, 3): + modulus, prefix = moduli[i], prod(moduli[:i]) + c, = [v for v in range(modulus) if (prefix * v - left) % modulus == 0] + offsets.append(c) + + def shift(x, i, sign): + modulus = moduli[i + 2] + return (x + sign * offsets[i]) % modulus if x < modulus else x + + slow, fast = (1 << width for width in widths[2:]) + maps = [[fast * shift(a, 0, sign) + shift(b, 1, sign) + for a, b in product(range(slow), range(fast))] for sign in (1, -1)] + need(all(maps[1][j] == i for i, j in enumerate(maps[0])), 'direct inverse permutation') + updated = state[:2] + [shift(state[i + 2], i, 1) for i in range(2)] + return left, offsets, updated, maps + + +def expected_headers(case, offsets): + precision = 1 + sum(case['widths']) + + def word(number, suffix='R'): + return 'L' + format(number, f'0{precision}b')[::-1] + suffix + + return [dict(h=word(width), modulus=word(modulus), selected_layer=word(0), + offsets=word(offset, '|R'), width='L' + '1' * width + 'R') + for width, modulus, offset in zip(case['widths'][2:], case['moduli'][2:], offsets, strict=True)] + + +def new_headers(m, route): + headers = tuple({name: m.join.Tape() for name in route.HEADER_NAMES} for _ in range(2)) + return headers, (m.join.Tape(), m.join.Tape()), m.join.Tape() + + +def observe_headers(headers, widths): + return [dict({name: ''.join(tape.cells) for name, tape in header.items()}, + width=''.join(width.cells)) for header, width in zip(headers, widths, strict=True)] + + +def borrowed_ports(it, lease): + actual = lease.actual + return (it.source, actual.result['stream'], actual.guide, actual.left, actual.right, + it.counters['axis'], it.counters['half']) + + +def state_of(ports): + return [(id(t.cells), bytes(t.cells), t.head, t.meter.writes) for t in ports] + + +def make_endpoint(m, source, reverse): + return m.writer.Endpoint(m.reverse if reverse else m.f, m.w, m.r, m.e, + m.subtractive if reverse else m.numeric, m.owner, m.bridge, source) + + +def run_leg(previous, m, route, source, payload, *, reverse=False, staged=False): + source_before = previous.meter_actions(source.meter) + payload_before = previous.bit_actions((payload,)) + endpoint = make_endpoint(m, source, reverse) + it = endpoint.iterator + numeric_ports = (*it.bank.ports, *it.guards, *it.counters.values(), endpoint.staging) + headers, widths, combined = new_headers(m, route) + indices = tuple(m.join.Tape() for _ in range(2)) + scratch = tuple(m.join.Tape() for _ in range(3)) + header_ports = tuple(t for header in headers for t in header.values()) + bank = {name: ['_'] for name in (*m.rom.REGS, 'arena', 'spool', 'layers', 'rom')} + bank_ids = tuple(map(id, bank.values())) + layers, rom = m.join.Tape(bank['layers']), m.join.Tape(bank['rom']) + adapter = (*header_ports, *widths, combined, *indices, *scratch, layers, rom) + record = m.route.RecordTape(m.binary, payload) + buckets = m.bit_tape(), m.bit_tape() + runs, machines, bank_history, pass_counts = [], [], [], [] + radix_tape_actions = 0 + select_row_bit = m.join.select_row_bit + row_queries = 0 + + def count_query(row, countdown): + nonlocal row_queries + row_queries += 1 + return select_row_bit(row, countdown) + + with previous.seal_numerical_roles(m), patch.object(m.join, 'select_row_bit', count_query): + lease, arena_meters = route.open_root(it) + borrowed = borrowed_ports(it, lease) + need(all(port.head == 1 for port in borrowed), 'actual root borrow entry heads') + before = state_of(borrowed) + route.emit_root_headers(m, it, lease, headers, widths, combined) + header_receipt = observe_headers(headers, widths) + for target, header in enumerate(headers): + need(tuple(map(id, bank.values())) == bank_ids + and all(all(c == '_' for c in cells) for cells in bank.values()), + 'same blank ROM bank including old tails') + active = {name: tape.cells for name, tape in header.items()} + service = bank | active + run = m.rom.execute(m.rom_program, service) + need(run['status'] == 'accept' and all(h == 0 for h in run['heads'].values()), + 'live encoded producer accepts and returns every head') + need(tuple(map(id, bank.values())) == bank_ids + and all(service[name] is cells for name, cells in bank.items()), + 'producer retained the same backing identities') + need(all(''.join(cells).rstrip('_') == header_receipt[target][name] + for name, cells in active.items()), 'actual producer preserves each active header') + runs.append(run) + bank_history.append(sum(map(len, bank.values()))) + route.rekey_axis(m, record, layers, widths, indices, scratch, target, reverse) + layers.erase() + rom.erase() + for tape in header.values(): + tape.erase() + if staged or target == len(headers) - 1: + current_machines, tape_actions = previous.literal_radix(m, record, combined, buckets) + machines.extend(current_machines) + radix_tape_actions += tape_actions + pass_counts.extend(sum(machine.census.values()) for machine in current_machines) + need(state_of(borrowed) == before, 'actual borrows preserved before staging') + endpoint.stage(lease) + need(state_of(borrowed) == before, 'borrowed source still unchanged while staging') + lease.close() + endpoint.commit() + if not it.closed: + it.close() + + combined.erase() + for width in widths: + width.erase() + need(all(p.head == 1 and all(c == m.w.BLANK for c in p.cells) for p in numeric_ports), + 'all owned encoded CRT tapes retired') + need(all(p.head == 0 and all(c == '_' for c in p.cells) for p in adapter) + and all(all(c == '_' for c in cells) for cells in bank.values()), + 'all header, routing and shared ROM tapes retired') + need(all(t.head == 0 and not t.cells for t in buckets) + and all(machine.status == 'accept' and not any(machine.registers) for machine in machines), + 'all literal bucket and control histories retired') + need(source.head == 1 and payload.head == 0, 'both physical entry heads returned') + + symbol_cells = [p.cells for p in numeric_ports] + symbol_cells += [p.cells for p in adapter if p is not layers and p is not rom] + symbol_cells += list(bank.values()) + need(len({id(cells) for cells in symbol_cells}) == len(symbol_cells), 'no duplicate symbol backing') + receipt = dict( + mode='staged_forward' if staged else 'fused_inverse' if reverse else 'fused_forward', + headers=header_receipt, producer_calls=len(runs), row_queries=row_queries, + skipped_leases=len(arena_meters) - 1, + encoded_source_symbol_actions=sum(previous.meter_actions(p.meter) for p in (source, *numeric_ports)) + - source_before + sum(previous.meter_actions(meter) for meter in arena_meters), + adapter_symbol_actions=sum(p.actions for p in adapter), + benes_instructions=sum(run['steps'] for run in runs), + radix_bit_control_instructions=sum(pass_counts), radix_instructions_by_pass=pass_counts, + payload_adapter_bit_actions=previous.bit_actions((payload, *buckets)) + - payload_before - radix_tape_actions, + retained_symbol_roles=len(symbol_cells), retained_symbol_cells=sum(map(len, symbol_cells)), + retained_rom_bank_cells_after_each_target=bank_history, + retained_benes_registers=sum(len(run['registers']) for run in runs), + retained_radix_register_bits=sum(len(machine.registers) for machine in machines), + retained_bucket_bits=sum(tape.extent for tape in buckets), payload_visited_bits=payload.extent, + ) + return receipt, (symbol_cells, buckets, machines, runs) + + +def check_frame(m, previous, payload, expected, width): + need(previous.observe_payload(payload, width) == list(enumerate(expected)) + and payload.cells == m.bit_tape(packet(m, width, expected)).cells, + 'direct CRT forward frame mismatch') + + +def header_probe(previous, m, route, case): + source, _ = source_fixture(m, case) + it = make_endpoint(m, source, False).iterator + headers, widths, combined = new_headers(m, route) + with previous.seal_numerical_roles(m): + lease, _ = route.open_root(it) + ports = borrowed_ports(it, lease) + before = state_of(ports) + route.emit_root_headers(m, it, lease, headers, widths, combined) + need(state_of(ports) == before, 'control preserves live headers and source') + lease.close() + if not it.closed: + it.close() + observed = observe_headers(headers, widths) + for header, width in zip(headers, widths, strict=True): + for tape in (*header.values(), width): + tape.erase() + combined.erase() + return observed + + +def check_header_alignment(previous, m, route, case): + _, offsets, _, _ = oracle(case) + expected = expected_headers(case, offsets) + need(case['widths'][2] != case['widths'][3] and len(set(offsets)) == 2, + 'control distinguishes both ordered widths and offsets') + observed = header_probe(previous, m, route, case) + need(observed == expected, 'distinct live header alignment') + copy = m.join.copy_numeric_field + first = None + + def stale_offset(source, target, guide, words, delimiter, suffix): + nonlocal first + copy(source, target, guide, words, delimiter, suffix) + if first is None: + first = target + return + first.step(1) + target.step(1) + while first.read() in m.route.BITS: + target.write(first.read()) + first.step(1) + target.step(1) + need(first.read() == target.read() == '|', 'stale control preserves field shape') + first.rewind() + target.rewind() + + with patch.object(m.join, 'copy_numeric_field', stale_offset): + mutated = header_probe(previous, m, route, case) + need(mutated[0] == expected[0] and mutated[1] == (expected[1] | {'offsets': expected[0]['offsets']}) + and mutated != expected, 'stale offset must fail ordered header oracle') + return dict(case=case['name'], headers=observed, stale_second_offset_rejected=True) + + +def replay(previous, m, route, cases): + case = cases['two_short_first'] + left, offsets, forward_state, maps = oracle(case) + width = sum(case['widths'][2:]) + initial_packet = packet(m, width, TAGS) + forward_tags = [tag for _, tag in sorted(zip(maps[0], TAGS, strict=True))] + expected = expected_headers(case, offsets) + source, fields = source_fixture(m, case) + payload = m.bit_tape(initial_packet) + source_initial, payload_initial = bytes(source.cells), dict(payload.cells) + source_id, payload_id = id(source.cells), id(payload.cells) + target_source = bytearray(source_initial) + for field, value in zip(fields, forward_state, strict=True): + for bit, cell in enumerate(field): + target_source[cell] = (value >> bit) & 1 + + forward, forward_keep = run_leg(previous, m, route, source, payload) + check_frame(m, previous, payload, forward_tags, width) + need(bytes(source.cells) == target_source and id(source.cells) == source_id + and id(payload.cells) == payload_id, 'exact forward source and same backing') + inverse, inverse_keep = run_leg(previous, m, route, source, payload, reverse=True) + need(bytes(source.cells) == source_initial and payload.cells == payload_initial + and id(source.cells) == source_id and id(payload.cells) == payload_id, + 'exact inverse source, payload and backing') + need({id(c) for c in forward_keep[0]}.isdisjoint(id(c) for c in inverse_keep[0]), + 'only actual boundary tapes are shared across legs') + + staged_source, _ = source_fixture(m, case) + staged_payload = m.bit_tape(initial_packet) + staged, _staged_keep = run_leg(previous, m, route, staged_source, staged_payload, staged=True) + check_frame(m, previous, staged_payload, forward_tags, width) + need(bytes(staged_source.cells) == target_source, 'staged forward same source') + need(all(leg['headers'] == expected and leg['producer_calls'] == 2 for leg in (forward, inverse, staged)), + 'both independently checked live headers on every leg') + need(forward['row_queries'] == inverse['row_queries'] == staged['row_queries'] == 96, + 'all physical row queries executed') + same_forward = ('benes_instructions', 'encoded_source_symbol_actions', + 'retained_rom_bank_cells_after_each_target', 'retained_symbol_cells', + 'retained_bucket_bits', 'payload_visited_bits') + need(all(forward[key] == staged[key] for key in same_forward), 'matched source and routing work') + need(all(forward[key] <= staged[key] for key in ('adapter_symbol_actions', + 'payload_adapter_bit_actions', 'retained_radix_register_bits')), 'no measured adapter tradeoff') + need([len(leg['radix_instructions_by_pass']) for leg in (forward, inverse, staged)] == [4, 4, 8], + 'literal fused and staged pass counts') + need(forward['skipped_leases'] == staged['skipped_leases'] == 2 and inverse['skipped_leases'] == 0, + 'actual encoded forward and reverse root lease schedules') + need(staged['radix_bit_control_instructions'] > forward['radix_bit_control_instructions'], + 'strictly lower measured radix instruction count') + + drop_source, _ = source_fixture(m, case) + drop_payload = m.bit_tape(initial_packet) + rekey = route.rekey_axis + + def omit_fast(m, record, layers, widths, indices, scratch, target, reverse): + if target == 0: + rekey(m, record, layers, widths, indices, scratch, target, reverse) + + with patch.object(route, 'rekey_axis', omit_fast): + drop, _drop_keep = run_leg(previous, m, route, drop_source, drop_payload) + dropped_tags = [tag for _, tag in previous.observe_payload(drop_payload, width)] + dropped_slot = dropped_tags.index(TAGS[0]) + need(dropped_slot == 4 and maps[0][0] == 5 + and dropped_tags != forward_tags and bytes(drop_source.cells) == target_source + and drop['headers'] == expected and drop['row_queries'] == 48, + 'missing fast target fails physical placement despite correct source update') + previous.reverse_order_control(m) + previous.truncated_layers_control(m) + alignment = check_header_alignment(previous, m, route, cases['growing_bank']) + + return dict(status='PASS_ENCODED_CRT_TWO_TARGET_PAYLOAD', fixture=case['name'], + moduli=case['moduli'], widths=case['widths'], reconstructed_left=left, + input_source=case['state'], forward_source=forward_state, + input_tags=list(TAGS), forward_tags=forward_tags, + forward_destinations=maps[0], inverse_destinations=maps[1], + restored_source_and_payload=True, source_retained_cells=len(source.cells), + executions=[forward, inverse, staged], + forward_radix_instructions_saved=staged['radix_bit_control_instructions'] + - forward['radix_bit_control_instructions'], + controls=dict(dropped_fast_first_tag_actual_slot=dropped_slot, + dropped_fast_first_tag_required_slot=maps[0][0], + noncommuting_row_order=True, truncated_layers_rejected=True, + ordered_header_alignment=alignment)) + + +def main(): + parser = ArgumentParser(description=__doc__) + parser.add_argument('--write-result', action='store_true') + args = parser.parse_args() + authenticate() + previous = load('leaf_replay', ROOT / PREDECESSOR) + route = load('two_target_route', HERE / 'route.py') + result = replay(previous, previous.modules(), route, retained_cases()) + result_file = HERE / 'RESULT.json' + serialized = json.dumps(result, sort_keys=True, indent=2) + '\n' + if args.write_result: + result_file.write_text(serialized) + else: + need(result_file.read_text() == serialized, 'committed exact result differs') + print(f'{result["status"]} records=16 radix_passes=4/8 ' + f'radix_instructions_saved={result["forward_radix_instructions_saved"]} controls=4') + + +if __name__ == '__main__': + main() diff --git a/research/encoded-crt-two-target-payload/route.py b/research/encoded-crt-two-target-payload/route.py new file mode 100644 index 0000000000..8bbbd51c2e --- /dev/null +++ b/research/encoded-crt-two-target-payload/route.py @@ -0,0 +1,150 @@ +"""Tape adapter for a two-target encoded CRT root. Apache-2.0.""" + +HEADER_NAMES = ('h', 'modulus', 'selected_layer', 'offsets') + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def open_root(iterator): + """Find the root by the encoded node cursor and the lease's suffix flag.""" + meters = [] + while (lease := iterator.next()) is not None: + meters.append(lease.actual.context.arena.meter) + if iterator.counters['axis'].read() == iterator.r.STEP and lease.actual.last: + return lease, meters + lease.close() + raise ValueError('encoded root lease missing') + + +def emit_axis(m, iterator, guide, header, width, combined): + """Consume the next physical right record and emit its width and modulus.""" + leaf = m.route + w, r, source = iterator.w, iterator.r, iterator.source + leaf.zero_header(header['h'], guide, w) + leaf.zero_header(header['selected_layer'], guide, w) + need(source.read() == r.ROOT, 'ordered right source record') + source.step(1) + need(source.read() == w.ONE, 'positive right source width') + width.emit('L') + while source.read() == w.ONE: + width.emit('1') + combined.emit('1') + need(not leaf.increment(header['h']), 'source width fits precision guide') + source.step(1) + need(source.read() == r.WORD_END, 'right source width delimiter') + source.step(1) + leaf.end_word(width) + + modulus = header['modulus'] + modulus.emit('L') + width.step(1) + while width.read() == '1': + bit = source.read() + need(bit in (w.ZERO, w.ONE) and guide.read() == w.ONE, + 'right modulus fits precision guide') + modulus.emit('1' if bit == w.ONE else '0') + source.step(1) + guide.step(1) + width.step(1) + need(width.read() == 'R' and source.read() == r.WORD_END, 'right modulus delimiter') + width.rewind() + source.step(1) + while guide.read() == w.ONE: + modulus.emit('0') + guide.step(1) + need(guide.read() == w.BLANK, 'modulus padding delimiter') + leaf.end_word(modulus) + guide.rewind() + + width.step(1) + while width.read() == '1': + need(source.read() in (w.ZERO, w.ONE), 'right coordinate bit') + source.step(1) + width.step(1) + need(width.read() == 'R' and source.read() == r.RECORD_END, + 'complete padded right source record') + width.rewind() + source.step(1) + + +def emit_root_headers(m, iterator, lease, headers, widths, combined): + """Copy ordered headers, consuming both fields of each live result record.""" + w, r, source = iterator.w, iterator.r, iterator.source + axis, half = iterator.counters['axis'], iterator.counters['half'] + guide, result = lease.actual.guide, lease.actual.result['stream'] + need(axis.read() == r.STEP and lease.actual.last, 'complete root interval') + while half.read() == w.ONE: + iterator._record() + half.step(1) + need(half.read() == w.RIGHT, 'complete left half') + half.rewind() + + combined.emit('L') + for header, width in zip(headers, widths, strict=True): + need(half.read() == w.ONE, 'two encoded right targets') + emit_axis(m, iterator, guide, header, width, combined) + need(result.read() == r.ROOT, 'ordered right result record') + result.step(1) + m.join.copy_numeric_field(result, header['offsets'], guide, w, r.WORD_END, '|') + m.join.skip_numeric_field(result, guide, w, r.WORD_END) + need(result.read() == r.RECORD_END, 'both right result fields consumed') + result.step(1) + half.step(1) + need(half.read() == w.RIGHT and source.read() == w.RIGHT and result.read() == w.RIGHT, + 'all right source and result records consumed') + half.rewind() + source.rewind() + result.rewind() + m.route.end_word(combined) + + +def initialize_index(leaf, index, width): + index.emit('L') + width.step(1) + while width.read() == '1': + index.emit('0') + width.step(1) + need(width.read() == 'R', 'complete encoded position width') + width.rewind() + leaf.end_word(index) + + +def skip_key_field(record, width): + width.step(1) + while width.read() == '1': + need(record.matches('0') or record.matches('1'), 'untouched key field bit') + record.move_word(1) + width.step(1) + need(width.read() == 'R', 'complete untouched key field') + width.rewind() + + +def rekey_axis(m, record, layers, widths, indices, scratch, target, reverse): + """Assign this target's field using current physical positions as inputs.""" + leaf = m.route + address, countdown, row = scratch + slow, fast = indices + for index, width in zip(indices, widths, strict=True): + initialize_index(leaf, index, width) + need(record.matches('<'), 'physical payload frame origin') + record.move_word(1) + while True: + record.pass_payload() + if target == 1: + skip_key_field(record, widths[0]) + leaf.copy_bits(indices[target], address) + leaf.route_address(m.join, layers, widths[target], address, countdown, row, reverse) + record.rekey(address) + address.erase() + if target == 0: + skip_key_field(record, widths[1]) + if leaf.increment(fast) and leaf.increment(slow): + break + need(record.matches('>'), 'payload occupies precisely the padded right rectangle') + while not record.matches('<'): + record.move_word(-1) + for index in indices: + index.erase() diff --git a/research/historical-selected-replay-gap/README.md b/research/historical-selected-replay-gap/README.md index 55d8cc3b49..36d9a873ca 100644 --- a/research/historical-selected-replay-gap/README.md +++ b/research/historical-selected-replay-gap/README.md @@ -69,7 +69,11 @@ python3 -B scripts/research_package.py --package research/historical-selected-re The direct command prints `PASS_HISTORICAL_SELECTED_REPLAY_GAP`. A registered replay prints `PASS_REGISTERED_RESEARCH_PACKAGE`. Both require Git history -containing the two inspected commits. +containing the two inspected commits and the source and manifest objects at +`2485805a6d47f36ea83ddde6327d453ac82d44dc`. The verifier uses a temporary +sparse checkout of that commit, checks the declared source digests there, and +uses its planner and manifest inventory. The recorded rejections and selection +therefore remain reproducible after later changes to the live Makefile or CI guide. ## Open next questions diff --git a/research/historical-selected-replay-gap/SOURCES.json b/research/historical-selected-replay-gap/SOURCES.json index c1010eec95..62bb8b3950 100644 --- a/research/historical-selected-replay-gap/SOURCES.json +++ b/research/historical-selected-replay-gap/SOURCES.json @@ -4,13 +4,13 @@ "files": [ { "path": "Makefile", - "usage": "input", + "usage": "provenance", "git_blob": "0d683a06b9e7ee162496108ce9a7c5d2ee94fccf", "sha256": "4f2d4f2dcd15139ec82658a975f85ed300897385f85799218539f4c8d60567da" }, { "path": "certificates/partial-swap-network.json", - "usage": "input", + "usage": "provenance", "git_blob": "eccafa830c16170c36faf93045ddf1f638f7bcd4", "sha256": "4c0b9d37e1034b2076e30a70f8e514416298c462d9ee98bc87fe6556b14df786" }, @@ -22,7 +22,7 @@ }, { "path": "docs/ci-verification.md", - "usage": "input", + "usage": "provenance", "git_blob": "63ba3e9aa8bdc5e942b56e34244b92b16f854085", "sha256": "c7d3027e9ad8bcbff68f07aa9576b30fb2f3c76c44d876d40c7fdbf4a3e2228a" }, @@ -34,163 +34,163 @@ }, { "path": "research/clifford-state-performance/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "6f98a0061a5104dfab82c9e806f819b41811f684", "sha256": "396d0f08df24952248140d5c65c51b8c902ef1c580892ff7ea182890530f67ee" }, { "path": "research/community-batch1047-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "5e0f92af463ec12c5e1dcc3effd44081a88af647", "sha256": "07a9daeaf2bda308a92e9a4684f13d5fc766c7772d74801fceb7f4599fdab226" }, { "path": "research/community-batch1099-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "9e13266bf85e627f1b7dc225e9530ea69fd2c7f0", "sha256": "421e1211fb1897c45621dc6801c276e53f2e6f335583c9c9049e535f87c0a3b1" }, { "path": "research/community-batch932-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "cc4d03eb59b9ab3f952735f7e88ff18c2d15d7af", "sha256": "184629cac91a5cfaca50330a88596008b824221433867dcf8117539c913c284a" }, { "path": "research/community-batch970-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "8b9f4111badf7de5d97684799560b55110e9da79", "sha256": "23188ed920e38a54006cb883e181585620821c63bf7e8b5e05d32719417cc37e" }, { "path": "research/community-frontier741-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "a5300d4e7a5381a3f443fc54c768ca6f0f236d68", "sha256": "3c820fb30e1b4d9bcfc6a7ab524375e5b2abd66b940af2c509146104f0bcd79c" }, { "path": "research/community-frontier890-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "d7ff6d777b01d69b6ce84caf25d3b7e4a4d2f211", "sha256": "6b185a9902652f893f3ebd8ada92d2f11b6de6533a9a4d11718a8a4496101128" }, { "path": "research/community-hyperplane599-audit/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "546f37d326d10a99910ae8f908e71ef768524d98", "sha256": "65099d764bfcc39bda5e4d9966783611b094c3522dbdd1435cd498d657a8ef8e" }, { "path": "research/community-k492-audit/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "e538481e4cb16ed936d3195f2dfb5b5a9ca0a76b", "sha256": "2c0f4fa5bc150d05658af2e7c54c4d2c337dd52b7efd3d69530ae73bcbdf452a" }, { "path": "research/community-reconciliation92-audit/MANIFEST.json", - "usage": "input", + "usage": "provenance", "git_blob": "2a2e93685173d5f13cbb5abe740f5d90352e0228", "sha256": "5f501f3c118131e7d069f30ad77186eb2ad6961f9680a0ef105f4514ed41808a" }, { "path": "research/partial-swap-digest/baseline.py", - "usage": "input", + "usage": "provenance", "git_blob": "a2f0190704db83bd8ef48e46e723c49b925804fe", "sha256": "81e9af92cdf38243a540cdcff2062778e449467848d444da37a9553c12ca4c34" }, { "path": "research/r420-two-sided-basis/SOURCES.json", - "usage": "input", + "usage": "provenance", "git_blob": "5d718e11e62f4bcadecf1e02d6b61f87dbe190b0", "sha256": "d9810b0d139c5a1211fd2c1f0d142187cc1fca30026e1e7bc4f9ecfacf1596d1" }, { "path": "research/skip-clones/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "8d1bb3b9c8189e35e5d8bfdfa632d7473e8be0d5", "sha256": "0b68e63e35a97ce6b0cdb6e291b88ebaa8f2dd4afb70b2498f10ee89428258dc" }, { "path": "research/split-skip/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "2ab610b6ea2edd2865fda793ef2168b0c76afb4f", "sha256": "7c2b4646a3ecfef6f881da5c43e4bd0fa9a4d1b00548b8ab458d897e16735134" }, { "path": "scripts/historical-ci-inputs/Makefile", - "usage": "input", + "usage": "provenance", "git_blob": "aff68409021c9d401a6f8013b9dfd7dbcc30f2a8", "sha256": "ea8830dd79da493e2d75baf753d733ff7efbcf2b4794afe41fae0ac8f3055646" }, { "path": "scripts/historical-ci-inputs/ledger-batch932-run_isolated_tests.py", - "usage": "input", + "usage": "provenance", "git_blob": "65db599ab0b1dea0312c4ca048e0bd0f44c3736f", "sha256": "96ea543e6c707424afe247e77bd86c82152f90fc76a0773c4232145da5cdf8d1" }, { "path": "scripts/historical-ci-inputs/ledger-batch932-test_isolated_test_runner.py", - "usage": "input", + "usage": "provenance", "git_blob": "34820a8f24678f918f4d0e7a35380d8013fc3495", "sha256": "628391b6abfbc8674ceec1751867a4392f2cc0b5b66886243e139af86cf355ac" }, { "path": "scripts/historical-ci-inputs/ledger-batch970-verify_selected_result.py", - "usage": "input", + "usage": "provenance", "git_blob": "c755b76e0d44ba4917aa94440ebe54daefce5b2a", "sha256": "d7fd929726b326aeeaf0a3996475adec88eee9aac09ae0bebeeaa0bc1fc8f199" }, { "path": "scripts/historical-ci-inputs/ledger-frontier741-ci-verification.md", - "usage": "input", + "usage": "provenance", "git_blob": "7f3c012504187917a728b9fe87043f0fc8cd006a", "sha256": "a854022e0e1d5d4db4d60e586be3ea56005013ef14a1fc06d02bc06e8529c4b0" }, { "path": "scripts/historical-ci-inputs/partial-swap-context.json", - "usage": "input", + "usage": "provenance", "git_blob": "ad65114886bf34a4fd27e79f3be502389e689faa", "sha256": "833a9642f33aeab2ffea17ec9c6b82e0a953f90192b2c82e10bef21538dccba9" }, { "path": "scripts/historical-ci-inputs/partial-swap-network.json", - "usage": "input", + "usage": "provenance", "git_blob": "52075f2463f60af5e16571347f24274fce73a1ea", "sha256": "f3c4be597b2f2136da4ae2cc80c7454f63c90aa01f84e5b8131cee4dd55de815" }, { "path": "scripts/partial_swap/shared.py", - "usage": "input", + "usage": "provenance", "git_blob": "44a0e454c70f9c4b98e258b8443612e6a119904b", "sha256": "5a0646a50b9f3e8ea55168620a78e8853b0ab810517cefc8cfb8696aedee278a" }, { "path": "scripts/replay_historical_check.py", - "usage": "input", + "usage": "provenance", "git_blob": "1e92fff2782970ef71378f594f2350d245a4db26", "sha256": "5467619c78183d3adc82b0cb55af28e5c1a01fca2b0588677816244b53e2bafd" }, { "path": "scripts/research_package.py", - "usage": "input", + "usage": "provenance", "git_blob": "091b4c8f58bac9a9580d76025b887dc5c873d05f", "sha256": "e1256016e7f51827d04fa2179255989f639ae1d97afaa9c16265f85a0c6abd70" }, { "path": "scripts/run_isolated_tests.py", - "usage": "input", + "usage": "provenance", "git_blob": "a96ab35b315ce492e7fbbfd6c5ae211aa066b541", "sha256": "49eb56dd0fc0d8d8ffdb209970a7adf2176223580646f575d5c22e59543b381c" }, { "path": "scripts/verify_selected_result.py", - "usage": "input", + "usage": "provenance", "git_blob": "6882a4700e410dec569b51ae2eaf1a19cc019195", "sha256": "d6b305eac5b9bdb8172c469ad30a1655a60fa0aceac8b1bf610e1b73f51babd8" }, { "path": "tests/test_isolated_test_runner.py", - "usage": "input", + "usage": "provenance", "git_blob": "343b24abf6719b81805eba5a84c74e57634c8288", "sha256": "3a5470d0b139828b90e19bf9583ddeafcd69f8e34f2824664eb3a2958a52e34d" } diff --git a/research/historical-selected-replay-gap/VERIFY.json b/research/historical-selected-replay-gap/VERIFY.json index 98553e72ed..ab7efa3471 100644 --- a/research/historical-selected-replay-gap/VERIFY.json +++ b/research/historical-selected-replay-gap/VERIFY.json @@ -4,36 +4,7 @@ "python": "3.12", "requirements": [], "inputs": [ - "Makefile", - "certificates/partial-swap-network.json", - "docs/ci-verification.md", - "research/clifford-state-performance/SOURCE.json", - "research/community-batch1047-audit/CONTENT-COVERAGE.json", - "research/community-batch1099-audit/CONTENT-COVERAGE.json", - "research/community-batch932-audit/CONTENT-COVERAGE.json", - "research/community-batch970-audit/CONTENT-COVERAGE.json", - "research/community-frontier741-audit/CONTENT-COVERAGE.json", - "research/community-frontier890-audit/CONTENT-COVERAGE.json", - "research/community-hyperplane599-audit/SOURCE.json", - "research/community-k492-audit/SOURCE.json", - "research/community-reconciliation92-audit/MANIFEST.json", - "research/partial-swap-digest/baseline.py", - "research/r420-two-sided-basis/SOURCES.json", - "research/skip-clones/SOURCE.json", - "research/split-skip/SOURCE.json", - "scripts/historical-ci-inputs/Makefile", - "scripts/historical-ci-inputs/ledger-batch932-run_isolated_tests.py", - "scripts/historical-ci-inputs/ledger-batch932-test_isolated_test_runner.py", - "scripts/historical-ci-inputs/ledger-batch970-verify_selected_result.py", - "scripts/historical-ci-inputs/ledger-frontier741-ci-verification.md", - "scripts/historical-ci-inputs/partial-swap-context.json", - "scripts/historical-ci-inputs/partial-swap-network.json", - "scripts/partial_swap/shared.py", - "scripts/replay_historical_check.py", - "scripts/research_package.py", - "scripts/run_isolated_tests.py", - "scripts/verify_selected_result.py", - "tests/test_isolated_test_runner.py" + "scripts/research_package.py" ], "commands": [ { diff --git a/research/historical-selected-replay-gap/verify.py b/research/historical-selected-replay-gap/verify.py index 83b995941a..9d266c5a4e 100644 --- a/research/historical-selected-replay-gap/verify.py +++ b/research/historical-selected-replay-gap/verify.py @@ -6,8 +6,10 @@ """ import hashlib import importlib.util +import json import subprocess import sys +import tempfile from pathlib import Path ROOT = Path(__file__).resolve().parents[2] @@ -61,31 +63,47 @@ def require(ok, message): raise SystemExit(message) -def load_checker(): - path = ROOT / "scripts/replay_historical_check.py" - spec = importlib.util.spec_from_file_location("historical_selected_replay_gap_checker", path) +def load_module(path): + spec = importlib.util.spec_from_file_location(path.stem, path) module = importlib.util.module_from_spec(spec) spec.loader.exec_module(module) return module +def checkout_snapshot(snapshot, sources, runner, env): + paths = [runner.canonical_relative_path(row["path"]) for row in sources["files"]] + git = ["git", "-c", "maintenance.auto=false", "-c", "gc.auto=0", + "-c", "core.autocrlf=false"] + subprocess.run([*git, "clone", "--quiet", "--shared", "--no-tags", "--no-checkout", + "--", str(ROOT), str(snapshot)], cwd=ROOT, env=env, check=True) + subprocess.run([*git, "update-ref", "--no-deref", "HEAD", INSPECTED], + cwd=snapshot, env=env, check=True) + # The pinned planner reads omitted manifests from the sparse HEAD/index. + patterns = "".join(f"/{path.as_posix()}\n" for path in paths) + subprocess.run([*git, "sparse-checkout", "set", "--no-cone", "--stdin"], + cwd=snapshot, env=env, input=patterns.encode("utf-8"), check=True) + subprocess.run([*git, "read-tree", "-mu", "HEAD"], cwd=snapshot, env=env, check=True) + for path, row in zip(paths, sources["files"], strict=True): + require(hashlib.sha256((snapshot / path).read_bytes()).hexdigest() == row["sha256"], + "historical checkout source digest changed: " + path.as_posix()) + + def entries(checker): for name, config in checker.CONFIG.items(): for entry in [config, *config.get("additional_inputs", [])]: yield name, entry -def reject(checker, entry): +def reject(root, checker, entry): try: - checker.authenticated_input(ROOT, entry) + checker.authenticated_input(root, entry) except ValueError as exc: return str(exc) raise SystemExit("historical input was admitted: " + entry["path"]) -def main(): - require(not sys.flags.optimize, "assertions must stay enabled") - checker = load_checker() +def check_snapshot(root, env): + checker = load_module(root / "scripts/replay_historical_check.py") selected = [entry for name, entry in entries(checker) if name == "tooling-ledger" and entry["path"] == SELECTED_PATH] require(len(selected) == 1, "selected-result checker overlay is not unique") @@ -94,7 +112,7 @@ def main(): require(entry["accepted_live_sha256"] == [SELECTED_ACCEPTED], "accepted selected-checker successors changed") frozen = (checker.INPUTS / entry["input"]).read_bytes() - live = (ROOT / SELECTED_PATH).read_bytes() + live = (root / SELECTED_PATH).read_bytes() require(hashlib.sha256(frozen).hexdigest() == SELECTED_PIN, "frozen selected checker bytes changed") require(hashlib.sha256(live).hexdigest() == SELECTED_LIVE, "live selected checker digest changed") require(SELECTED_LIVE not in (SELECTED_PIN, SELECTED_ACCEPTED), "live checker was already admitted") @@ -102,7 +120,7 @@ def main(): # live successor, not a broken comparison. require(SELECTED_PIN in (SELECTED_PIN, *entry["accepted_live_sha256"]), "pin membership control failed") - require(reject(checker, entry) == REJECTIONS[SELECTED_PATH][1], + require(reject(root, checker, entry) == REJECTIONS[SELECTED_PATH][1], "selected checker rejection text changed") counts = {path: 0 for path in REJECTIONS} @@ -110,7 +128,7 @@ def main(): for _name, item in entries(checker): if item["path"] not in REJECTIONS: continue - message = reject(checker, item) + message = reject(root, checker, item) counts[item["path"]] += 1 messages.setdefault(item["path"], message) for path, (count, message) in REJECTIONS.items(): @@ -118,20 +136,31 @@ def main(): require(messages[path] == message, "rejection text changed for " + path) require(sum(counts.values()) == 19, "rejection total changed") ci = [item for _name, item in entries(checker) if item["path"] == CI_PATH] - require(len(ci) == 1 and hashlib.sha256((ROOT / CI_PATH).read_bytes()).hexdigest() == CI_LIVE, + require(len(ci) == 1 and hashlib.sha256((root / CI_PATH).read_bytes()).hexdigest() == CI_LIVE, "selected CI note digest changed") diff = subprocess.check_output( - ["git", "diff", "--name-only", PARENT, INSPECTED], cwd=ROOT, text=True) + ["git", "diff", "--name-only", PARENT, INSPECTED], cwd=root, env=env, text=True) changed = sorted(name for name in diff.splitlines() if name) require(changed == CHANGED, "inspected commit diff changed") - sys.path.insert(0, str(ROOT / "scripts")) - from research_package import plan_details - details = plan_details(ROOT, set(changed)) + planner = load_module(root / "scripts/research_package.py") + details = planner.plan_details(root, set(changed)) require([row["package"] for row in details] == PLAN_PACKAGES, "helper plan selection changed") matched = {name for row in details for names in row["causes"].values() for name in names} require(sorted(set(changed) - matched) == UNMATCHED, "unmatched plan paths changed") - require(plan_details(ROOT, set()) == [], "empty change set selected a package") + require(planner.plan_details(root, set()) == [], "empty change set selected a package") + + +def main(): + require(not sys.flags.optimize, "assertions must stay enabled") + sources = json.loads(Path(__file__).with_name("SOURCES.json").read_bytes()) + require(sources["base_commit"] == INSPECTED, "historical checkout base changed") + runner = load_module(ROOT / "scripts/research_package.py") + env = runner.git_source_env() + with tempfile.TemporaryDirectory(prefix="historical-selected-replay-") as temporary: + snapshot = Path(temporary) / "snapshot" + checkout_snapshot(snapshot, sources, runner, env) + check_snapshot(snapshot, env) print("PASS_HISTORICAL_SELECTED_REPLAY_GAP") print("selected_checker_live=" + SELECTED_LIVE) print("rejections=19 distinct_paths=7 plan_packages=9")