From d9913fe24f119f9d431f324dbbe7d90de409a856 Mon Sep 17 00:00:00 2001 From: Hiroki KUMAZAKI Date: Fri, 23 Oct 2026 02:40:38 +0900 Subject: [PATCH] Audit current-state CRT repair queries and cached inverses --- research/crt-repair-query-budget/PROOF.md | 191 +++++++++++ research/crt-repair-query-budget/README.md | 117 +++++++ research/crt-repair-query-budget/RESULT.json | 315 ++++++++++++++++++ research/crt-repair-query-budget/SOURCES.json | 66 ++++ research/crt-repair-query-budget/TASK.json | 74 ++++ research/crt-repair-query-budget/VERIFY.json | 37 ++ research/crt-repair-query-budget/caller.py | 270 +++++++++++++++ research/crt-repair-query-budget/verify.py | 291 ++++++++++++++++ 8 files changed, 1361 insertions(+) create mode 100644 research/crt-repair-query-budget/PROOF.md create mode 100644 research/crt-repair-query-budget/README.md create mode 100644 research/crt-repair-query-budget/RESULT.json create mode 100644 research/crt-repair-query-budget/SOURCES.json create mode 100644 research/crt-repair-query-budget/TASK.json create mode 100644 research/crt-repair-query-budget/VERIFY.json create mode 100644 research/crt-repair-query-budget/caller.py create mode 100644 research/crt-repair-query-budget/verify.py diff --git a/research/crt-repair-query-budget/PROOF.md b/research/crt-repair-query-budget/PROOF.md new file mode 100644 index 0000000000..227d133415 --- /dev/null +++ b/research/crt-repair-query-budget/PROOF.md @@ -0,0 +1,191 @@ +# Current-state CRT queries in an exceptional repair key + +This is a scoped audit of the handoff in Ryanson Jonathan's PR4409, +[`crt-evaluator-independent-check`](../crt-evaluator-independent-check/README.md). +It connects Cinna Davis's PR4100 CRT controls to the explicit reverse word +in PR4169 and amends one accounting expression from unpaidmoon's PR4377. +The exact retained inputs are pinned in [SOURCES.json](SOURCES.json). +There is no new multiplication saving or selected-frontier change. + +## 1. Three query sites in the literal key evaluator + +Use the complete modular address domain and hypotheses of +[PR4169](../crt-arbitrary-source-repair/PROOF.md): the compact controls are +arbitrary dirty fields, the target intervals are disjoint, and every Boolean +source function omits every active target and the borrowed controls. Write +`L(y)=sum_i f_i(y) B^i`. The raw compact word and its literal inverse are + +```text +S: F; u += L(y); F; u -= L(y) +S^-1: u += L(y); F^-1; u -= L(y); F^-1. +``` + +Each assignment is reduced in its complete cyclic field. The existing proof +establishes this inverse for every address, including exceptional addresses; +it does not replace `F^-1` by the guarded XOR formula. + +For an input address `z`, name the successive y fields `y0`, `y1` after +the first `F^-1`, and `y2` after the second. Evaluating the correction key +`R(z)=T(S^-1(z))` therefore has exactly these three source-query sites: + +```text +L(y0), L(y1), and (f_i(y2))_i for the final ideal switch T. +``` + +These are three evaluations of a vector of controls, not three queries per +elementary modular assignment. The current y field must be supplied at each +site. On exceptional addresses, carries can alter non-target coordinates; +the source-independence hypothesis does not make these three vectors equal. +This is a property of the literal evaluator, not a lower bound on every +possible implementation of the same permutation. + +PR763's exceptional-stream theorem already proves that this correction key +places each payload at its ideal destination. We reuse that theorem and +PR4169's explicit inverse; neither generic repair nor inverse correctness is +claimed as a new result here. + +## 2. What can be cached, for every residue vector + +Fix a left child A with m>=1 pairwise coprime integer moduli +`s_0,...,s_(m-1)>=2`. For a target modulus s>=2 outside A, let Q be the +product of the earlier moduli in its right child. Assume all these moduli +are pairwise coprime. Put + +```text +S_A = product_j s_j, P_j = product_(k=s_j`, set the offset to zero, as PR4100 requires. Thus a total query is +`c(a)` on valid left vectors and zero otherwise. Both reconstruction and +the validity test concern the current state. Cached alpha_j, mu, products +and weights remain valid through changes of state; a cached k_A or offset +need not. The target tail remains fixed by the padded rotation. + +One may instead retain the literal `decode_group` arithmetic and replace +only its modular-inverse calls by these cached constants. The budget below +allows a fresh full reconstruction, including fresh inversions, at each +query. It consequently requires no unproved saving from a cache, nor a new +tariff for the fixed-weight formula. In particular, three source-query sites +do **not** imply a lower bound of `3(m+1)` modular inversions. + +## 3. Conditional seven-term source-table allowance + +The following is conditional on PR4377's credited local arithmetic and +Beneš scan tariffs. It does not independently establish their tape model. +Let integers `p>=2`, `ell>=1`, and `q=p+2` be given. Assume at most `8q` +target axes and `m,W<=8q` per axis. Every left modulus and target modulus +must have at most ell bits, as must each padded current coordinate supplied +for comparison. W must cover the complete modulus-prefix operands, +including the right prefix `S_A Q`; the retained W-bit/2W-bit operand +premises must hold for the reconstruction arithmetic. We assume the +per-axis reconstruction allowance + +```text +C_axis = 128 m W^2 + 128 m ell^3 + 16 m W. +``` + +This tariff is a premise, not a consequence merely of `m,W<=8q`. +In particular, W cannot be interpreted as the left-group width while +ignoring a longer right-prefix operand. + +Price the current validity test separately. Assume each copied coordinate +and its fixed modulus are supplied in aligned, zero-padded ell-bit slots, +with both heads at the first prescribed most-significant origin. Sweep all m +slots forward, resetting the local comparison flags at each slot, and return +both heads once after the last slot. A sequential +lexicographic comparison uses two bit reads, two forward head moves and +at most six Boolean/flag operations per bit; returning both heads costs +another two moves per bit. At most four further operations initialize, +retain and combine the comparison flag. Since ell>=1, `12ell+4<=16ell`. +Thus testing all m coordinates and combining their validity flags costs +at most `16m ell` per query and axis, including these local head returns. +This premise supplies the aligned inputs; extracting fragmented coordinates, +copying them into these slots and transporting their descriptors are not +priced by this comparison tariff. + +PR4377 charges C_axis once before building networks from one offset. +For the three current-state queries, allow it three times. Conservatively +build both the positive and negative rotation networks at each query, six +networks per axis. This also avoids assuming a network remains usable after +the left coordinates change. Retain its per-network bound + +```text +25(ell+2)^2 2^ell + 64 ell 2^(2ell). +``` + +This bound survives PR4409's correction of the smaller per-wire estimate: +`4(ell+2)+8(ell+2)^2+8ell <= 25(ell+2)^2` for ell>=1. +Allow three descriptor scans, each bounded by `256q^2`. Substituting the +axis cap and m,W bounds, and adding `3 A 16m ell<=3072q^2 ell` for +the current validity tests, gives the conditional seven-term allowance + +```text +E_src = 768q^2 + 1572864q^4 + 24576q^3 + 24576q^2 ell^3 + + 1200q(ell+2)^2 2^ell + 3072q ell 2^(2ell) + 3072q^2 ell. +``` + +For all the stated parameters, `E_src <= B0 = 2^(4ell)q^16`. To prove this, +each term divided by B0 decreases with q because its q-degree is at most +four. It suffices to take q=4. At ell=1 the seven terms are + +```text +12288, 402653184, 1572864, 393216, 86400, 49152, 49152; +sum = 404816256, B0 = 68719476736, +sum/B0 = 3162627/536870912. +``` + +Each term is at most B0/8. Increasing ell by one multiplies B0 by sixteen; +the seven respective term factors are at most `1,1,1,8,32/9,8,2`. Induction +therefore preserves all seven bounds, and their sum is at most B0. This proves +the full integer tail; finite checks are corroboration, not its justification. + +With `G=64(ell+ceil(log2 q))`, the original amortization follows unchanged: +`2^-G E_src <= 2^(-60ell) q^-48`, since `q^64<=2^(64 ceil(log2 q))`. + +## 4. Evidence and boundary + +[RESULT.json](RESULT.json) records a reduced, genuine CRT switch fixture +after physical reservoir placement. Its literal reverse trace changes a +left reconstruction/offset, and freezing the entry offset gives a different +repair key. This discriminates state refresh from merely recounting calls. +The fixture is not a production-sized parameter instance and cannot disprove +PR4100's asymptotic envelope. Its role is to reject that frozen-offset shortcut. + +The allowance above covers three source-table evaluations under the stated +local tariffs. It does not price the complete key evaluator's modular address +updates, arbitrary descriptor movement, payload extraction/sorting, reservoir +placement, or a complete fixed-tape implementation. Evaluating forward S as +well would add its own two source-query sites. No such extra work is silently +included in E_src, and no full multiplication theorem follows from this bound. + +Credit Cinna Davis for PR4100, unpaidmoon for PR4377's tariffs and envelope, +Ryanson Jonathan for PR4409's independent check and inverse-query handoff, +and ToikY for the predecessor Beneš audit. PR4169 supplies the explicit reverse +word and PR4174 the reservoir placement used by the fixture. John-Michael Smith +and Douglas Colkitt supplied the prior compact carry/repair argument in PR763 +and its construction lineage; the retained source notices remain applicable. +Prepared for Hiroki KUMAZAKI (@kumagi), with substantial OpenAI Codex assistance. +Apache-2.0. No independent human review or proof-assistant acceptance is claimed. diff --git a/research/crt-repair-query-budget/README.md b/research/crt-repair-query-budget/README.md new file mode 100644 index 0000000000..2aedd09665 --- /dev/null +++ b/research/crt-repair-query-budget/README.md @@ -0,0 +1,117 @@ +# Current-state CRT queries in an exceptional repair key + +The literal `T(S^-1(q))` key reads CRT controls at **three current states**: +inside each of the inverse word's two loads, then at the recovered origin for +`T`. Reusing the entry offset can send an exceptional payload to the wrong key. +Modulus-only inverses can nevertheless be prepared once: **m+1 inversions +suffice per fixed left group/target**, with none during subsequent queries. +This is a construction, not an inverse-count lower bound. + +This answers the inverse-macro handoff in +[PR4409](https://github.com/CrocSwap/integer-mult-bounds/pull/4409). +[PROOF.md](PROOF.md) gives the quantified cache identity and query argument. +It also amends PR4377's source-table arithmetic for three reconstructions, +six conservative rotation networks and explicit padded-validity comparisons. +Under the stated inherited local tariffs and aligned-input premise, the +allowance still satisfies `E_src <= 2^(4 ell)(p+2)^16` for every integer +`p>=2, ell>=1`; the existing guard amortization follows with constant one. +This does **not** price the entire key evaluator or establish a new κ. + +## Caller evidence + +[caller.py](caller.py) combines source-authenticated retained CRT/Beneš code, +the PR4169 literal inverse word, and PR4174 reservoir descriptors. The fixture +uses proper prime widths `(4,4,5,5)` and moduli `(11,13,17,19)`. The target is +root axis 2, local Beneš row 6; three bits from inactive axis 3 are exchanged +into the borrowed fields. One left-coordinate bit moves above the target, +where exceptional carries can change its current CRT value. + +Two exact witnesses appear in [RESULT.json](RESULT.json): + +| Input `(u,t,y)` | Offsets at the three live queries | Correct key | Key with entry offset frozen | +| --- | --- | --- | --- | +| `(0,1,4)` | `5,4,4` | `(0,1,30724)` | `(1,1,30724)` | +| `(1,1,4)` | `5,5,4` | `(1,1,30724)` | `(1,1,31236)` | + +Both have valid left coordinates throughout; the padded target domain is +allowed. The second recovers the same inverse origin even with the stale +source, isolating the need to refresh the final `T` query. The mutant still +reads the **current target coordinate**; only its entry CRT offset is frozen. +No claim requires three distinct offsets. + +The frozen receipt checks all 32,768 middle fields and all 131,072 dirty +`(u,t,y)` states of this switch. It verifies literal inverse/forward agreement, +16,384 good states, all 114,688 exceptional keys, and complete repaired payload +correspondence. The back bit is an omitted spectator. A separate inverse spy +permits exactly three setup calls and rejects any later inversion. Four small +fixed-modulus cases cover 548 padded vectors (266 valid), including nontrivial +right prefixes. Controls reject missing invalid-left disabling, dropping the +right-prefix factor and noninvertible fixed data. + +The arithmetic grid covers 7,960 pairs (`p=2..200`, `ell=1..40`). Its largest +exact allowance/envelope ratio is `3162627/536870912`, about 0.005891, at +`p=2, ell=1`. The proof, rather than this finite grid, establishes the unbounded +tail. Host operation counts are not bit-step measurements. + +## Reproduce + +From the repository root, using Python 3.12 and only its standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/crt-repair-query-budget --check-only +python3.12 -B scripts/research_package.py --package research/crt-repair-query-budget +``` + +The registered commands run ordinary and optimized Python with a 120-second +limit each. Both compare the existing receipt without changing it. Direct +replay is `python3.12 -B research/crt-repair-query-budget/verify.py`; the explicit +`--write-result` option is only for authoring a new receipt. Eight live inputs +are checked by SHA256 and Git blob identity before their captured Python bytes +are executed, avoiding predecessor bytecode caches. A Git-free package export +supports direct replay; generic provenance validation requires Git history. + +## Scope, overlap and limitations + +Base: canonical main `b58ad9ef4d4e861b0eaa5dba41742bdc072dca51`, priority revision +7. [TASK.json](TASK.json) records the refined `uniform-transfer-audit` card; +[SOURCES.json](SOURCES.json) pins every retained input. The selected record and +catalogue are historical provenance. Selected conditional #4470 is unchanged. +Coordination: [Discussion #4709](https://github.com/CrocSwap/integer-mult-bounds/discussions/4709). +The live check covered 476 open PR bodies, 3,629 Discussion records and all +5,860 tracked local note records before the claim. PR4650's one-axis arena +tariff and PR4637's mask bridge are complementary; neither supplies this trace. +PR4644 joins the one-target unary producer, reverse keys and repair, but uses +a different key machine and explicitly leaves a reverse-shear bit-step price open. + +This is a reduced fixture with `H=G=1, K=5`, below the production dimension and +guard constants. Its counterexamples reject a frozen-offset shortcut; they +are not counterexamples to the asymptotic construction. The universal cache +identity applies to arbitrary fixed coprime groups, but a finite current-y +lookup table is only a verification accelerator. We do not claim its memory +cost as a runtime algorithm. No physical coordinate materialization, complete +modular address-update cost, tape erasure, extraction/sorting, native lifting, +or outer multiplication theorem is verified here. Forward `S` adds its own +two source queries if included in a larger task. + +## Open next questions + +Bind the three current-state epochs to copied physical descriptors in a +literal complete key evaluator, then meter its address updates, fixed cache +and restoration. Start by joining the interface here to the pending #4650 +shared arena and #4637 repair-mask work. This matters because source-table +arithmetic alone does not discharge CRT total repair. No blocker prevents a +scoped trace, but a full tariff needs their tape/head-movement premises. +See the structured handoff in [TASK.json](TASK.json). + +## Credit + +Cinna Davis supplies #4100's CRT construction; unpaidmoon supplies #4377's +local tariffs and envelope; Ryanson Jonathan supplies #4409's independent +arithmetic check and caller handoff; ToikY supplies the predecessor #4192 +Beneš audit. Our prior #4169/#4174 supply the literal inverse and placement. +The generic exceptional-stream repair follows John-Michael Smith and Douglas +Colkitt's #763 lineage. Those results are reused, not claimed anew. + +Prepared by Hiroki KUMAZAKI (@kumagi), with substantial OpenAI Codex assistance +in research, code, agent review and writing. Apache-2.0. No independent human +review, proof-assistant acceptance or complete theorem acceptance is claimed. diff --git a/research/crt-repair-query-budget/RESULT.json b/research/crt-repair-query-budget/RESULT.json new file mode 100644 index 0000000000..abec4c7eca --- /dev/null +++ b/research/crt-repair-query-budget/RESULT.json @@ -0,0 +1,315 @@ +{ + "authenticated_inputs": 8, + "budget": { + "base_bound": 68719476736, + "base_sum": 404816256, + "base_terms": [ + 12288, + 402653184, + 1572864, + 393216, + 86400, + 49152, + 49152 + ], + "domain": "p>=2, ell>=1 (proof); p=2..200, ell=1..40 (corroborating grid)", + "grid_cases": 7960, + "maximum_checked_ratio": "3162627/536870912", + "networks_per_axis": 6, + "query_sites": 3, + "scope": "conditional source-table tariff only; not complete key/tape cost" + }, + "caller": { + "G": 1, + "H": 1, + "K": 5, + "L": 18, + "back_bit": "spectator, omitted from Word; controls omit it by descriptors", + "destination_blocks": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ], + [ + 17, + 18 + ] + ], + "dynamic_inverse_calls": 0, + "good_addresses": 16384, + "invalid_left_middle_states": 14464, + "invalid_left_mutant": { + "correct_bit": 0, + "correct_offset": 0, + "current_y": 6, + "residues": [ + 12, + 0 + ], + "wrong_bit": 1, + "wrong_offset": 16 + }, + "inverse_permutation_sha256": "31216c12463255fb4bedc1edcbfae0ee3a907d2f8d4d785554ff6104c68ccc16", + "local_bit": 2, + "middle_states": 32768, + "moduli": [ + 11, + 13, + 17, + 19 + ], + "repaired_bad_addresses": 114688, + "repaired_payload_sha256": "927eabc586d23ca3eb257f527a5f30647fc4a465f24e8eb23235efa8f78779fa", + "row": 6, + "setup_inverse_calls": [ + [ + 13, + 11 + ], + [ + 11, + 13 + ], + [ + 143, + 17 + ] + ], + "source_blocks": [ + [ + 2, + 3 + ], + [ + 3, + 4 + ], + [ + 4, + 5 + ] + ], + "stale_offset_witnesses": [ + { + "input": [ + 0, + 1, + 4 + ], + "key": [ + 0, + 1, + 30724 + ], + "origin": [ + 0, + 1, + 31236 + ], + "query_trace": [ + { + "bit": 1, + "coordinates": [ + 8, + 0, + 0 + ], + "current_y": 4, + "k_A": 52, + "local_bit": 2, + "offset": 5, + "residues": [ + 8, + 0 + ], + "row": 6, + "target": 0, + "target_y_bit": 9, + "valid": true + }, + { + "bit": 1, + "coordinates": [ + 9, + 0, + 20 + ], + "current_y": 31236, + "k_A": 130, + "local_bit": 2, + "offset": 4, + "residues": [ + 9, + 0 + ], + "row": 6, + "target": 20, + "target_y_bit": 9, + "valid": true + }, + { + "bit": 1, + "coordinates": [ + 9, + 0, + 20 + ], + "current_y": 31236, + "k_A": 130, + "local_bit": 2, + "offset": 4, + "residues": [ + 9, + 0 + ], + "row": 6, + "target": 20, + "target_y_bit": 9, + "valid": true + } + ], + "stale_key": [ + 1, + 1, + 30724 + ], + "stale_offset": 5, + "stale_origin": [ + 1, + 1, + 30724 + ] + }, + { + "input": [ + 1, + 1, + 4 + ], + "key": [ + 1, + 1, + 30724 + ], + "origin": [ + 1, + 1, + 31236 + ], + "query_trace": [ + { + "bit": 1, + "coordinates": [ + 8, + 0, + 0 + ], + "current_y": 4, + "k_A": 52, + "local_bit": 2, + "offset": 5, + "residues": [ + 8, + 0 + ], + "row": 6, + "target": 0, + "target_y_bit": 9, + "valid": true + }, + { + "bit": 1, + "coordinates": [ + 8, + 0, + 0 + ], + "current_y": 4, + "k_A": 52, + "local_bit": 2, + "offset": 5, + "residues": [ + 8, + 0 + ], + "row": 6, + "target": 0, + "target_y_bit": 9, + "valid": true + }, + { + "bit": 1, + "coordinates": [ + 9, + 0, + 20 + ], + "current_y": 31236, + "k_A": 130, + "local_bit": 2, + "offset": 4, + "residues": [ + 9, + 0 + ], + "row": 6, + "target": 20, + "target_y_bit": 9, + "valid": true + } + ], + "stale_key": [ + 1, + 1, + 31236 + ], + "stale_offset": 5, + "stale_origin": [ + 1, + 1, + 31236 + ] + } + ], + "target_y_bit": 9, + "valid_left_middle_states": 18304, + "widths": [ + 4, + 4, + 5, + 5 + ], + "word_addresses": 131072 + }, + "fixed_reconstruction": { + "dynamic_inverses": 0, + "noninvertible_setups_rejected": 3, + "padded_vectors": 548, + "setup_inverses_per_case": [ + 2, + 3, + 3, + 4 + ], + "valid_vectors": 266, + "wrong_right_prefix": { + "expected": 6, + "moduli": [ + 3, + 5 + ], + "residues": [ + 0, + 1 + ], + "right_prefix": 11, + "target": 7, + "wrong": 3 + } + }, + "status": "PASS_CRT_REPAIR_QUERY_BUDGET" +} diff --git a/research/crt-repair-query-budget/SOURCES.json b/research/crt-repair-query-budget/SOURCES.json new file mode 100644 index 0000000000..14fbcc7814 --- /dev/null +++ b/research/crt-repair-query-budget/SOURCES.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/crt-arbitrary-source-repair/PROOF.md", + "usage": "input", + "git_blob": "147633ce18d41f44cbd6bdc2030fcdf962b415a4", + "sha256": "1b8cb76afc6bf923c31377ba22c7675b3e563e3341fc5db0cd9d1057be4ee624" + }, + { + "path": "research/crt-arbitrary-source-repair/verify.py", + "usage": "input", + "git_blob": "813eafd24f031b046b2d4aaabdcb0950538980f1", + "sha256": "9a646116e430a242fc16c98d6e35c21290a00ccd9951145290b9a4bf5c007d48" + }, + { + "path": "research/crt-evaluator-independent-check/README.md", + "usage": "input", + "git_blob": "5c70326168fe5b5e764c89334c19a6035f4b13d7", + "sha256": "945e3b1f1801166547e362b92c7b86f0fbd1f2bf7c7edeb1cafb05eb68bb098a" + }, + { + "path": "research/crt-reservoir-placement/PROOF.md", + "usage": "input", + "git_blob": "087ab4462282fc68d6f5b8b1f17167383e77df7c", + "sha256": "cea5eec3d4ec1008293e98213f519bdbf88dcd9aa801bff516eaee24340efa68" + }, + { + "path": "research/crt-reservoir-placement/allocator.py", + "usage": "input", + "git_blob": "4b3ad89652a28f7d142248d1b5747272e696493c", + "sha256": "b764195fc6291e3c8fa8297b1f4ceaefc119d5664d8ff348b49eac8a2e79c688" + }, + { + "path": "research/crt-uniform-evaluator/PROOF.md", + "usage": "input", + "git_blob": "7175c780b63378963c00ea29d76a9d1d7f86bbf0", + "sha256": "a67dce487dfaf0f1748458cf052b85203654d63f84c4e362ae78fe1bae1a3d42" + }, + { + "path": "research/unconditional-batched-crt/CRT.md", + "usage": "input", + "git_blob": "d98dd8e368431cac33d5fc1c8c336696663641d6", + "sha256": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b" + }, + { + "path": "research/unconditional-batched-crt/check_batched_crt.py", + "usage": "input", + "git_blob": "1cf78abccd5e06beecc3ed21ba55f7c03b65fdbc", + "sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e" + } + ] +} diff --git a/research/crt-repair-query-budget/TASK.json b/research/crt-repair-query-budget/TASK.json new file mode 100644 index 0000000000..3c9de51b8d --- /dev/null +++ b/research/crt-repair-query-budget/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Audit PR4409's inverse-macro handoff at the literal CRT repair key T(S^-1(q)): current-state reconstruction, fixed inverse caching, and a conditional repeated-query allowance.", + "scope_change_reason": "The broad uniform-transfer card is narrowed to one explicit unfilled PR4409 caller handoff; PR4169/4174 already supply the generic inverse and placement, and PR4650/4637 cover complementary arena/repair-mask work.", + "bottleneck_link": "Correct source controls and an honest query bill are necessary for the unresolved CRT total-repair/fixed-tape interface in proposed #4100. This is a scoped contribution on that proof track, with no improvement or admission of selected #4470.", + "budget_minutes": 60, + "stop_rule": "Stop after a quantified cache identity and query-count argument, one exhaustive transported CRT switch fixture with stale-offset controls, and the conditional arithmetic tail proof. Do not build a full key evaluator or rerun the selected native pipeline.", + "outcome": "completed", + "evidence": "PROOF.md proves three literal query sites, fixed-cache identity, and the all-parameter conditional allowance. RESULT.json freezes 32768 current-state evaluations, 131072 word addresses, two wrong-key witnesses, 548 padded reconstruction vectors, and 7960 exact arithmetic points. Normal and optimized registered replays compare rather than rewrite the receipt.", + "author": "Hiroki KUMAZAKI (@kumagi), with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for orientation, live overlap/coordination, mathematical derivation, Python implementation, independent agent review, verification and documentation; no independent human or proof-assistant acceptance claimed.", + "open_questions": [ + { + "question": "Can a literal complete repair-key evaluator bind its current-state queries to physical copied descriptors and restore fixed-cache/work storage within a complete tape tariff?", + "why_it_matters": "The corrected source-table arithmetic alone does not price modular address updates, coordinate materialization, extraction/sorting or erasure, so it cannot discharge #4100 total repair.", + "first_step": "Compose the state epochs and three callbacks here with the one-axis shared arena in #4650 and the repair-mask interface in #4637; meter one complete exceptional key including descriptor reads and restoration before extrapolating.", + "blocked_by": "No blocker to a scoped caller trace; full cost requires the retained tape/head-movement premises and pending complementary interface work." + } + ] +} diff --git a/research/crt-repair-query-budget/VERIFY.json b/research/crt-repair-query-budget/VERIFY.json new file mode 100644 index 0000000000..e8c72af926 --- /dev/null +++ b/research/crt-repair-query-budget/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/crt-arbitrary-source-repair/PROOF.md", + "research/crt-arbitrary-source-repair/verify.py", + "research/crt-evaluator-independent-check/README.md", + "research/crt-reservoir-placement/PROOF.md", + "research/crt-reservoir-placement/allocator.py", + "research/crt-uniform-evaluator/PROOF.md", + "research/unconditional-batched-crt/CRT.md", + "research/unconditional-batched-crt/check_batched_crt.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate eight inputs; fixed-inverse/current-state CRT controls; exhaustive transported word/repair correspondence; stale-offset and invalid-left controls; exact conditional budget; compare frozen receipt." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same source-bound checks under optimized Python; explicit require checks remain active and receipt is read-only." + } + ] +} diff --git a/research/crt-repair-query-budget/caller.py b/research/crt-repair-query-budget/caller.py new file mode 100644 index 0000000000..641ce5a6fa --- /dev/null +++ b/research/crt-repair-query-budget/caller.py @@ -0,0 +1,270 @@ +"""Current-state CRT controls with modulus-only inverses hoisted explicitly. + +FixedCRT(left_moduli, target_modulus, right_prefix=1, inverse=...) prepares m+1 inverses +once, then evaluate(residues) performs no modular inversion. RootCaller binds +that evaluator to one actual balanced-tree root axis, transported through the +three disjoint exchanges of the retained reservoir construction. Callers pass +already authenticated crt, allocator and Word modules; this module loads no +files, prints nothing, and performs no I/O. + +The root fixture uses widths (4,4,5,5), moduli (11,13,17,19), target axis 2, +reservoir axis 3, L=18, and H=G=1, K=5. These are proper declared widths for +the prime moduli, but the geometry is below the production size cutoff. The +fixture tests actual CRT control semantics, not the production constants or +a machine-time bound. Optional memoization is by the CURRENT y argument. + +Cinna Davis supplies the CRT/network construction; PR4169/4174 supply the +inverse and placement interfaces; PR4377/4409 motivate the query-budget +audit. Hiroki KUMAZAKI (@kumagi), with substantial OpenAI Codex assistance. +Apache-2.0. See README and PROOF for the complete attribution and limits. +""" +from __future__ import annotations + +from dataclasses import asdict, dataclass +from math import prod + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def modular_inverse(value, modulus): + return pow(value, -1, modulus) + + +@dataclass(frozen=True) +class CRTValue: + residues: tuple[int, ...] + valid: bool + k_A: int + offset: int + + +class FixedCRT: + """Locally scaled CRT reconstruction for fixed pairwise-coprime moduli. + + If P_i is the product of the left moduli preceding i, the current input + residue is k_A/P_i modulo s_i. Each term therefore uses + ((residue_i * P_i) mod s_i) * (S/s_i) * (S/s_i)^(-1) mod s_i. + The target offset is k_A * (S*right_prefix)^(-1) modulo target_modulus. + + setup_inverse_calls, evaluation_calls and reconstruction_calls are host + operation counters, not bit-step costs. The first counts exactly the + actual modular-inverse provider calls below. The optional inverse keyword + accepts a two-argument provider; by default it is pow(value,-1,modulus). + evaluate invokes no inverse helper. The setup inversions themselves check + that the required fixed moduli and target prefix are coprime. + Invalid padded residues disable the node's shift, as in CRT.md section 1. + """ + + def __init__(self, left_moduli, target_modulus, right_prefix=1, *, inverse=None): + self.left_moduli = tuple(left_moduli) + require(self.left_moduli and all(type(m) is int and m >= 2 for m in self.left_moduli), + "nonempty left group of integer moduli at least two") + require(type(target_modulus) is int and target_modulus >= 2, "positive target modulus") + require(type(right_prefix) is int and right_prefix >= 1, "positive right-child prefix") + inverse = modular_inverse if inverse is None else inverse + require(callable(inverse), "modular inverse implementation must be callable") + self.target_modulus = target_modulus + self.right_prefix = right_prefix + self.product = prod(self.left_moduli) + self.setup_inverse_calls = 0 + self.evaluation_calls = 0 + self.reconstruction_calls = 0 + self.terms = [] + prefix = 1 + for modulus in self.left_moduli: + complement = self.product // modulus + coefficient_inverse = inverse(complement, modulus) + self.setup_inverse_calls += 1 + require(type(coefficient_inverse) is int + and complement * coefficient_inverse % modulus == 1, + "left complements must be invertible modulo their own moduli") + self.terms.append((modulus, prefix, complement, coefficient_inverse)) + prefix *= modulus + self.terms = tuple(self.terms) + self.prefixes = tuple(term[1] for term in self.terms) + self.complements = tuple(term[2] for term in self.terms) + self.target_inverse = inverse(self.product * right_prefix, target_modulus) + self.setup_inverse_calls += 1 + require(type(self.target_inverse) is int + and self.product * right_prefix * self.target_inverse % target_modulus == 1, + "target prefix must be invertible") + + def evaluate(self, residues): + """Read current residues and return the node's current valid/offset state.""" + residues = tuple(residues) + require(len(residues) == len(self.left_moduli) + and all(type(value) is int and value >= 0 for value in residues), + "one nonnegative current residue per left modulus") + self.evaluation_calls += 1 + valid = all(value < modulus for value, modulus in zip(residues, self.left_moduli)) + if not valid: + return CRTValue(residues, False, 0, 0) + self.reconstruction_calls += 1 + total = 0 + for value, (modulus, prefix, complement, inverse) in zip(residues, self.terms): + total += ((value * prefix) % modulus) * complement * inverse + integer = total % self.product + return CRTValue(residues, True, integer, + integer * self.target_inverse % self.target_modulus) + + def check_reference(self, value, crt): + """Verification-only comparison with the passed retained decode_group.""" + reference = crt.decode_group(value.residues, self.left_moduli) if value.valid else 0 + require(reference == value.k_A, "fixed-inverse reconstruction differs from source") + require(value.offset == reference * self.target_inverse % self.target_modulus, + "fixed-inverse target offset differs from source") + return True + + +@dataclass(frozen=True) +class Query: + """One source-function evaluation at its actual current y state. + + target is the reconstructed target-axis value. bit is the Boolean source + output. local_bit and target_y_bit identify the physical switch target. + coordinates contains the current axes 0, 1 and 2; omitted axis 3 is dirty. + """ + + current_y: int + row: int + coordinates: tuple[int, int, int] + residues: tuple[int, int] + valid: bool + k_A: int + offset: int + target: int + local_bit: int + target_y_bit: int + bit: int + + def record(self): + return asdict(self) + + +class RootCaller: + """Fixed real CRT root-axis fixture, with exact transported coordinates. + + root = RootCaller(crt_module, allocator_module, word_module, inverse=...) + root.rows # local rows having a complete compact guard + root.word(row) # retained Word with the transported target + root.evaluate(row, current_y) # Query with complete current-state trace + root.source(row, trace, cache) # callable y -> (control_bit,) + root.stale_offset_source(row,c) # deliberately wrong fixed-offset callback + + source(..., cache=True) memoizes Query values by its current y argument; + it does not retain the first offset for later, different addresses. Such + finite memoization is a replay accelerator and is not priced as a runtime + algorithm. The source's networks are cached by their actual offset. + """ + + widths = (4, 4, 5, 5) + moduli = (11, 13, 17, 19) + ell = 5 + target_axis = 2 + reservoir_axis = 3 + H = 1 + G = 1 + K = 5 + + def __init__(self, crt, allocator, word_module, *, inverse=None): + self.crt = crt + self.Word = word_module.Word + self.L = sum(self.widths) + self.Y = self.L - 3 * self.H + self.placement = allocator.Placement(self.L, self.H, ((2, 3), (3, 4), (4, 5))) + axes = [] + end = self.L + for width in self.widths: + axes.append((end - width, end)) + end -= width + self.axes = tuple(axes) + self.descriptors = tuple(self.placement.map_interval(*interval) for interval in self.axes) + self._read_parts = tuple(tuple((self.L - part.image_interval[1], + part.image_interval[1] - part.image_interval[0]) + for part in fragments) + for fragments in self.descriptors[:3]) + self.fixed = FixedCRT(self.moduli[:2], self.moduli[self.target_axis], inverse=inverse) + self._networks = {} + self.schedule = tuple(bit for bit, table in self.network(0)) + self.rows = tuple(row for row in range(len(self.schedule)) + if self.target_y_bit(row) + self.K <= self.Y) + + @property + def setup_inverse_calls(self): + return self.fixed.setup_inverse_calls + + @property + def network_builds(self): + return len(self._networks) + + def network(self, offset): + require(type(offset) is int and 0 <= offset < self.moduli[self.target_axis], + "canonical target offset") + if offset not in self._networks: + self._networks[offset] = self.crt.benes(self.crt.rotation( + 1 << self.widths[self.target_axis], self.moduli[self.target_axis], offset)) + return self._networks[offset] + + def target_y_bit(self, row): + require(type(row) is int and 0 <= row < len(self.schedule), "local network row") + original = self.axes[self.target_axis][1] - 1 - self.schedule[row] + physical = self.placement.map_position(original) + require(2 * self.H <= physical < self.L - self.H, "target must be in the middle field") + return self.L - self.H - 1 - physical + + def word(self, row): + require(row in self.rows, "row uses the separate tail branch rather than a complete guard") + return self.Word(self.G, self.H, self.Y, (self.target_y_bit(row),), self.K) + + def coordinates(self, current_y): + require(type(current_y) is int and 0 <= current_y < (1 << self.Y), + "complete current middle field") + placed = current_y << self.H + result = [] + for parts in self._read_parts: + value = 0 + for shift, width in parts: + value = (value << width) | ((placed >> shift) & ((1 << width) - 1)) + result.append(value) + return tuple(result) + + def evaluate(self, row, current_y): + target_y_bit = self.target_y_bit(row) + coordinates = self.coordinates(current_y) + value = self.fixed.evaluate(coordinates[:2]) + local_bit, table = self.network(value.offset)[row] + require(local_bit == self.schedule[row], "common retained Beneš schedule") + return Query(current_y, row, coordinates, value.residues, value.valid, + value.k_A, value.offset, coordinates[2], local_bit, + target_y_bit, table[coordinates[2]]) + + def source(self, row, trace=None, cache=False): + """Return the actual source; optionally append every callback's Query record.""" + self.target_y_bit(row) + values = {} if cache else None + + def callback(current_y): + if values is None: + query = self.evaluate(row, current_y) + else: + if current_y not in values: + values[current_y] = self.evaluate(row, current_y) + query = values[current_y] + if trace is not None: + trace.append(query.record()) + return (query.bit,) + + return callback + + def stale_offset_source(self, row, offset): + """Negative control: query live target values in one incorrectly frozen network.""" + self.target_y_bit(row) + table = self.network(offset)[row][1] + + def callback(current_y): + return (table[self.coordinates(current_y)[2]],) + + return callback diff --git a/research/crt-repair-query-budget/verify.py b/research/crt-repair-query-budget/verify.py new file mode 100644 index 0000000000..6049e5320b --- /dev/null +++ b/research/crt-repair-query-budget/verify.py @@ -0,0 +1,291 @@ +"""Exact caller replay; ordinary and optimized runs compare a frozen receipt. + +Hiroki KUMAZAKI (@kumagi), with substantial OpenAI Codex assistance. Apache-2.0. +Predecessor credit and limits are in README/PROOF. Host arrays accelerate finite +verification; they are not a fixed-tape evaluator or a bit-step cost trace. +""" +from __future__ import annotations + +import argparse +from fractions import Fraction +import hashlib +from itertools import product +import json +from pathlib import Path +import sys +import types + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def authenticate(): + sources = {} + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + for row in manifest["files"]: + if row["usage"] != "input": + continue + data = (ROOT / row["path"]).read_bytes() + require(hashlib.sha256(data).hexdigest() == row["sha256"], + "source SHA256 mismatch: " + row["path"]) + blob = b"blob " + str(len(data)).encode() + b"\0" + data + require(hashlib.sha1(blob).hexdigest() == row["git_blob"], + "source Git blob mismatch: " + row["path"]) + sources[row["path"]] = data + require(len(sources) == 8, "exact eight-input scope") + return sources + + +def module(name, path, data): + """Compile checked bytes, bypassing predecessor bytecode caches.""" + result = types.ModuleType(name) + result.__file__ = str(ROOT / path) + sys.modules[name] = result + exec(compile(data, result.__file__, "exec"), result.__dict__) + return result + + +class InverseSpy: + def __init__(self): + self.calls = [] + self.frozen = False + + def __call__(self, value, modulus): + require(not self.frozen, "modular inverse called after fixed setup") + self.calls.append((value, modulus)) + return pow(value, -1, modulus) + + +def digest(values): + return hashlib.sha256(b"".join(x.to_bytes(4, "little") for x in values)).hexdigest() + + +def fixed_reconstruction(caller, crt): + cases = (((3,), 5, 1), ((3, 5), 7, 11), ((11, 13), 17, 19), + ((3, 5, 7), 11, 13)) + checked = valid = 0 + prefix_mutant = None + for moduli, target, prefix in cases: + spy = InverseSpy() + fixed = caller.FixedCRT(moduli, target, prefix, inverse=spy) + require(len(spy.calls) == len(moduli) + 1, "m+1 setup inversions") + spy.frozen = True + weights = tuple(p*c*a % fixed.product for m, p, c, a in fixed.terms) + for residues in product(*(range(1 << (m-1).bit_length()) for m in moduli)): + value = fixed.evaluate(residues) + expected_valid = all(a < m for a, m in zip(residues, moduli)) + reference = crt.decode_group(residues, moduli) if expected_valid else 0 + require(value.valid == expected_valid and value.k_A == reference, + "cached reconstruction agrees with retained decode_group") + expected = reference * pow(fixed.product*prefix, -1, target) % target + require(value.offset == expected, "target-prefix offset agrees") + if expected_valid: + require(sum(a*w for a, w in zip(residues, weights)) % fixed.product + == reference, "fixed-weight identity") + valid += 1 + wrong = reference * pow(fixed.product, -1, target) % target + if prefix != 1 and wrong != expected and prefix_mutant is None: + prefix_mutant = dict(moduli=moduli, target=target, right_prefix=prefix, + residues=residues, expected=expected, wrong=wrong) + checked += 1 + require(len(spy.calls) == len(moduli) + 1, "no address-dependent inversions") + require(prefix_mutant is not None, "nontrivial-prefix discriminator") + rejected = 0 + for args in (((3, 9), 5), ((3, 5), 5), ((3,), 5, 5)): + try: + caller.FixedCRT(*args) + except ValueError: + rejected += 1 + require(rejected == 3, "noninvertible fixed data rejected") + return dict(padded_vectors=checked, valid_vectors=valid, + setup_inverses_per_case=[2, 3, 3, 4], dynamic_inverses=0, + wrong_right_prefix=prefix_mutant, noninvertible_setups_rejected=rejected) + + +def caller_census(caller, crt, allocator, word_module): + spy = InverseSpy() + root = caller.RootCaller(crt, allocator, word_module, inverse=spy) + require(root.setup_inverse_calls == len(spy.calls) == 3, "root fixed setup") + spy.frozen = True + require(all((m-1).bit_length() == w for m, w in zip(root.moduli, root.widths)), + "proper declared prime-modulus widths") + row = 6 + word = root.word(row) + values = [] + valid_count = 0 + invalid_mutant = None + # Direct bit exchange is independent of fragment concatenation in caller.py. + positions = tuple(root.placement.map_position(i) for i in range(root.L)) + require(sorted(positions) == list(range(root.L)), "placement is a bit permutation") + require(all(2*root.H <= positions[i] < root.L-root.H + for lo, hi in root.axes[:3] for i in range(lo, hi)), + "source coordinates omit u, t and the back field") + reference_networks = {offset: crt.benes(crt.rotation(32, 17, offset)) + for offset in range(17)} + for y in range(1 << root.Y): + query = root.evaluate(row, y) + placed = y << root.H + original = sum(((placed >> (root.L-1-positions[i])) & 1) + << (root.L-1-i) for i in range(root.L)) + coordinates = tuple((original >> (root.L-hi)) & ((1 << (hi-lo))-1) + for lo, hi in root.axes[:3]) + require(query.coordinates == coordinates, "transported current-axis descriptors") + value = root.fixed.evaluate(coordinates[:2]) + root.fixed.check_reference(value, crt) + require((query.valid, query.k_A, query.offset) == (value.valid, value.k_A, value.offset), + "current caller reconstructs current coordinates") + reference_bit, reference_table = reference_networks[value.offset][row] + require(query.local_bit == reference_bit + and query.bit == reference_table[coordinates[2]], + "current control agrees with separately constructed retained network") + valid_count += query.valid + values.append(query.bit) + if not query.valid and invalid_mutant is None: + wrong_offset = (crt.decode_group(query.residues, root.moduli[:2]) + * root.fixed.target_inverse % root.moduli[2]) + wrong_bit = root.network(wrong_offset)[row][1][query.target] + if wrong_bit != query.bit: + invalid_mutant = dict(current_y=y, residues=query.residues, + correct_offset=0, wrong_offset=wrong_offset, + correct_bit=query.bit, wrong_bit=wrong_bit) + require(invalid_mutant is not None, "invalid-left disabling changes an actual control") + source = lambda y: (values[y],) + word.check_source(source) + # A current-y oracle is finite test storage, not a priced runtime cache. + inverse_image = [None]*word.size + repaired = [None]*word.size + ideal = [None]*word.size + good = 0 + for address in range(word.size): + state = word.unpack(address) + origin = word.run(state, source, inverse=True) + require(word.run(origin, source) == state, "literal forward after inverse") + origin_id = word.pack(origin) + inverse_image[address] = origin_id + is_good = word.good(state) + require(word.good(origin) == is_good, "raw good/bad invariance") + key = word.pack(word.ideal(origin, source)) + require(word.good(word.unpack(key)) == is_good, "ideal good/bad invariance") + if is_good: + require(key == address, "raw equals ideal on good set") + good += 1 + destination = address if is_good else key + require(repaired[destination] is None, "exceptional repair key injectivity") + repaired[destination] = origin_id + ideal_destination = word.pack(word.ideal(state, source)) + require(ideal[ideal_destination] is None, "ideal switch injectivity") + ideal[ideal_destination] = address + require(sorted(inverse_image) == list(range(word.size)), "full raw permutation") + require(repaired == ideal and all(x is not None for x in repaired), + "complete exceptional key/payload correspondence") + witnesses = [] + for state in ((0, 1, 4), (1, 1, 4)): + trace = [] + live = root.source(row, trace) + origin = word.run(state, live, inverse=True) + key = word.ideal(origin, live) + require(len(trace) == 3 and all(x["valid"] for x in trace), "three all-valid query sites") + require(not word.good(state), "exceptional-address witness") + stale = root.stale_offset_source(row, trace[0]["offset"]) + wrong_origin = word.run(state, stale, inverse=True) + wrong_key = word.ideal(wrong_origin, stale) + require(key != wrong_key, "frozen entry offset produces a wrong repair key") + require(word.run(origin, root.source(row)) == state, "witness reversibility") + if state[0] == 0: + require(origin != wrong_origin and trace[0]["offset"] != trace[1]["offset"], + "second inverse-load query discriminator") + if state[0] == 1: + require(origin == wrong_origin and trace[0]["offset"] == trace[1]["offset"] + and trace[2]["offset"] != trace[1]["offset"], "final T query discriminator") + witnesses.append(dict(input=state, origin=origin, key=key, query_trace=trace, + stale_offset=trace[0]["offset"], stale_origin=wrong_origin, + stale_key=wrong_key)) + require(len(spy.calls) == 3, "no query-time inversion across full caller replay") + return dict(widths=root.widths, moduli=root.moduli, L=root.L, H=root.H, G=root.G, + K=root.K, row=row, local_bit=root.schedule[row], target_y_bit=word.targets[0], + source_blocks=root.placement.source_blocks, + destination_blocks=root.placement.destination_blocks, + middle_states=len(values), valid_left_middle_states=valid_count, + invalid_left_middle_states=len(values)-valid_count, word_addresses=word.size, + good_addresses=good, repaired_bad_addresses=word.size-good, + back_bit="spectator, omitted from Word; controls omit it by descriptors", + setup_inverse_calls=spy.calls, dynamic_inverse_calls=0, + inverse_permutation_sha256=digest(inverse_image), + repaired_payload_sha256=digest(repaired), invalid_left_mutant=invalid_mutant, + stale_offset_witnesses=witnesses) + + +def cost_terms(p, ell): + q = p+2 + return (768*q*q, 1572864*q**4, 24576*q**3, 24576*q*q*ell**3, + 1200*q*(ell+2)**2*2**ell, 3072*q*ell*4**ell, 3072*q*q*ell) + + +def budget(): + base_terms = cost_terms(2, 1) + base_bound = 2**4*4**16 + require(all(8*t <= base_bound for t in base_terms), "seven induction base bounds") + factors = (Fraction(1), Fraction(1), Fraction(1), Fraction(8), Fraction(32, 9), + Fraction(8), Fraction(2)) + max_ratio = Fraction(0) + cases = 0 + for p in range(2, 201): + q = p+2 + for ell in range(1, 41): + terms = cost_terms(p, ell) + bound = 2**(4*ell)*q**16 + require(all(8*t <= bound for t in terms) and sum(terms) <= bound, + "refreshed source-table allowance") + require(all(n <= f*t for n, f, t in zip(cost_terms(p, ell+1), factors, terms)), + "ell induction factors") + require(all(n*q**16 <= t*(q+1)**16 + for n, t in zip(cost_terms(p+1, ell), terms)), "q monotonic ratios") + require(4*(ell+2)+8*(ell+2)**2+8*ell <= 25*(ell+2)**2, + "corrected per-network polynomial") + G = 64*(ell+(q-1).bit_length()) + require(sum(terms)*q**48 <= 2**(G-60*ell), "guard amortization") + max_ratio = max(max_ratio, Fraction(sum(terms), bound)) + cases += 1 + require(max_ratio == Fraction(sum(base_terms), base_bound), "exact maximum at base") + return dict(domain="p>=2, ell>=1 (proof); p=2..200, ell=1..40 (corroborating grid)", + grid_cases=cases, query_sites=3, networks_per_axis=6, + base_terms=base_terms, base_sum=sum(base_terms), base_bound=base_bound, + maximum_checked_ratio=str(max_ratio), + scope="conditional source-table tariff only; not complete key/tape cost") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-result", action="store_true", help="explicit receipt authoring") + args = parser.parse_args() + sources = authenticate() + loaded = [] + for name, path in (("crt_query_reference", "research/unconditional-batched-crt/check_batched_crt.py"), + ("crt_query_placement", "research/crt-reservoir-placement/allocator.py"), + ("crt_query_word", "research/crt-arbitrary-source-repair/verify.py")): + loaded.append(module(name, path, sources[path])) + path = "research/crt-repair-query-budget/caller.py" + caller = module("crt_query_caller", path, (ROOT/path).read_bytes()) + crt, allocator, word_module = loaded + result = dict(status="PASS_CRT_REPAIR_QUERY_BUDGET", authenticated_inputs=len(sources), + fixed_reconstruction=fixed_reconstruction(caller, crt), + caller=caller_census(caller, crt, allocator, word_module), budget=budget()) + encoded = json.dumps(result, indent=2, sort_keys=True)+"\n" + receipt = PACKAGE/"RESULT.json" + if args.write_result: + receipt.write_text(encoded) + else: + require(receipt.read_text() == encoded, "frozen RESULT.json differs; no files rewritten") + print(result["status"]) + print("131072 word addresses; 32768 current middle states; 3 fixed inversions, 0 query inversions") + print("Three current-state sites; two stale-offset witnesses; conditional ratio " + + result["budget"]["maximum_checked_ratio"]) + + +if __name__ == "__main__": + main()