diff --git a/research/rank7-cleanup-dirty-identity/BACKWARD.json b/research/rank7-cleanup-dirty-identity/BACKWARD.json new file mode 100644 index 0000000000..ebc75084ce --- /dev/null +++ b/research/rank7-cleanup-dirty-identity/BACKWARD.json @@ -0,0 +1,33 @@ +{ + "cases": [ + { + "dual": false, + "input": "research/rank7-joint-endframes/data/WORD-base.json.gz", + "peak_covector_registers": 54, + "private_columns": 91, + "private_rows": 91 + }, + { + "dual": true, + "input": "research/rank7-joint-endframes/data/WORD-base.json.gz", + "peak_covector_registers": 54, + "private_columns": 91, + "private_rows": 91 + }, + { + "dual": false, + "input": "research/rank7-joint-endframes/data/WORD-extra.json.gz", + "peak_covector_registers": 54, + "private_columns": 91, + "private_rows": 91 + }, + { + "dual": true, + "input": "research/rank7-joint-endframes/data/WORD-extra.json.gz", + "peak_covector_registers": 54, + "private_columns": 91, + "private_rows": 91 + } + ], + "status": "PASS_RANK7_CLEANUP_BACKWARD" +} diff --git a/research/rank7-cleanup-dirty-identity/README.md b/research/rank7-cleanup-dirty-identity/README.md new file mode 100644 index 0000000000..e666b9ccb5 --- /dev/null +++ b/research/rank7-cleanup-dirty-identity/README.md @@ -0,0 +1,213 @@ +# PR2979 cleanup fixes arbitrary dirty private arrays + +For the original PR #2979 cleanup, all 91 private arrays return to their own +entrance values, even when those values are dirty. No private entrance value +leaks into a live output. This holds for arbitrary live entrance arrays, in +both providers and both orientations, without a reachable-state premise from +the prefix. + +This closes the explicit unrun arbitrary-cleanup-entrance question in +[PR #3238](https://github.com/CrocSwap/integer-mult-bounds/pull/3238). It also +strengthens zero-return to a dirty-private identity. It is a finite algebraic +certificate, not a complete native, physical or multiplication theorem audit. +There is no new kappa, supplier admission or selected-frontier change. + +## Exact statement + +Let `V` be any vector space over the rationals. The 632 live arrays and 91 +private arrays are distinct and disjoint copies of `V`. Run the literal +5,207 cleanup gates under their FULL-frame scalar/linear-map interpretation. +For either orientation, the cleanup operator has block form + +```text + live entrance private entrance +live output A 0 +private output 0 I_91 +``` + +The live block `A` is not asserted to be identity. All 112 target arrays are +unchanged. Each private array equals its own arbitrary entrance at its last +literal cleanup touch, including a final read rather than a final write. +Zero entrance therefore implies zero at every corresponding return boundary, +provided the native schedule binds that boundary to this last touch. + +The 72 cleanup warp sites may be arbitrary linear maps, independently. No +commutation, phase normalization, inverse identity or native Clifford recipe +is used in this statement. For the physical dual interpretation, instantiate +them with the appropriate inverse-transpose maps. The literal dual scalar +rules are `s -= q*t` for `t += q*s`, and reciprocal scaling. + +The two providers have byte-identical cleanup lists but different warp +recipes. Their canonical cleanup SHA256, using JSON with separators `,` and +`:`, is `af0fd40c22a5fa100525f68e16228ea2ebcc1ae4e5ca1f0e7564f277fe299c79`. +Checking both source files authenticates both assignments; it is not two +independent cleanup constructions. + +## Proof and certificate + +Work in the free associative algebra over the rationals on the signed warp +names. A polynomial term is an entrance-array symbol preceded by an ordered +word of map symbols. The two symbols `i` and `-i` are independent. The checker +never cancels inverse pairs and never exchanges operators. + +Initialize all 723 rows as independent entrance symbols, including the 91 +private rows. For each gate: + +- ADD replaces its target row by the target plus the rational coefficient + times the source row. +- SCALE multiplies its row by the exact rational coefficient. +- WARP prepends its formal map symbol to every term in its row. + +Induction over the ordered gate list proves that each row is the literal +cleanup's linear expression in all entrance arrays. The source-bound replay +then checks that each private row is exactly its own symbol, every live row +has zero coefficients on all private symbols, and every target row is its +own symbol. These are exact polynomial identities, not sampled numerical +agreements. Substitution of arbitrary linear maps preserves each identity. +The last-touch assertions follow because no later gate reads or writes the +returned private array. + +`verify.py` performs that full forward row propagation. `RESULT.json` binds +the complete formal matrix with deterministic hashes and records every private +last touch. The maximum intermediate row has 112 terms forward and 120 dual. +The live block changes 429 rows forward and 397 dual, so this certificate must +not be read as a proof of the complete invocation's live endpoint. + +`backward.py` is a separately implemented check with no import of the forward +interpreter or any predecessor verifier. It pulls 91 private output covectors +back through the reversed gate list, multiplying map symbols on the right. +It also pulls them through the transposed program, independently checking the +91 private input columns. Formal transpose reverses operator words; it assumes +no symmetry of a map. All 728 row/column checks across the two providers and +two orientations give unit vectors. The peak covector support is recorded in +`BACKWARD.json`. This is algorithmic cross-checking by the same contributor, +not independent human review or formal-kernel verification. + +## A control that clean-only replay misses + +The last touch of private array 1003 is cleanup gate 4844, zero-indexed: + +```text +live[302] -= private[1003] / 4 +``` + +Doubling that coefficient leaves the complete cleanup map unchanged whenever +all private entrances are zero. The clean-only replay therefore accepts this +mutant. With arbitrary dirty private entrances, its exact difference from the +original is + +```text +live[302] -= private_entrance[1003] / 4 +private[930] += private_entrance[1003] / 8 +private[934] += private_entrance[1003] / 8 +``` + +Setting only private entrance 1003 to one gives an explicit witness, with no +warp assignment needed. The dirty-identity check rejects it. This establishes +new failure coverage beyond zero-return under clean allocation. + +Other controls reject a dropped closing gate, a changed closing coefficient, +a premature return, private leakage and private scaling, malformed geometry, +non-FULL frames, removed-register access, invalid scalars/operators, source +corruption, duplicate JSON keys and a changed receipt. Noncommuting toy words +check both interpreters' multiplication order and transpose handling. +A changed live-only warp can preserve the private contract while changing +the live matrix hash. That control explicitly prevents treating private +success as certification of all native/live semantics. + +## Sources, overlap and scope + +Base canonical main is `463113d675af7410ac91d53a4fed51ec6494eb9a`, priority +revision 6. Both live inputs match PR #2979 head +`be191346391661f4d35fc0d1508d0a6029572576` byte for byte. `SOURCES.json` pins +the compressed inputs with Git blobs and SHA256, plus catalogue and selected +record provenance. Frozen inputs and existing packages are unchanged. + +The [canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/2612#discussioncomment-19002977) +identifies this refinement of `independent-moment`. Its first working baseline +command passed. The complete overlap snapshot at entry covered 284 open PRs +at 2026-10-17 18:59:06 UTC and 2,059 Discussion records at 18:59:36 UTC. +The searches included the task, `arbitrary cleanup entrance`, `rank7 cleanup` +and `3238`; they do not cover every diff or unpublished work. The pre-submission +fetch at 2026-10-17 19:08 UTC found canonical main unchanged, with no guidance, +selected-record or relevant source delta. Refreshed complete snapshots covered +288 open PRs at 19:08:36 UTC and 2,067 Discussion records at 19:09:05 UTC; +no new overlapping arbitrary-dirty-cleanup result was found. + +Nearest predecessor coverage: + +- PR #3238, head `3c689aac34ff240f82e27dcc7f0247b96b8676af`, proves the + original words' clean zero returns at actual native frees, relative to the + original inputs and their expanded prefix dependency cone. It explicitly + leaves arbitrary cleanup entrance unrun. No executable from it is imported. +- PR #3208, head `87d63a82defff1ffeea173743106fb97903cbbd6`, proves arbitrary + live entrance with clean private buffers for PR #3044's different R2 + cleanup. Its 5,208 gates are not this 5,207-gate cleanup; it independently + checks native recipes, which this package does not. No code is copied. +- PR #2979's existing auditor checks a whole invocation with clean private + buffers and derives cleanup from the preceding word. This package checks + the isolated cleanup and arbitrary dirty private inputs directly. + +A possible consumer may borrow dirty arrays instead of supplying clean ones +under this scalar/linear contract. That is only an interface corollary. The +unchanged schedule still requires 91 distinct arrays disjoint from live +storage, and their intermediate values need not equal their entrances. +Acquisition, backing ownership, movement, finite precision and native +allocation/free legality are unpriced. No stock, role or recursive-rank +saving follows here. Prefix/native phases, complete supplier/outer replay, +all-size/compiler/analytic obligations and hosted CI are not checked. + +## Reproduce + +Python 3.12 standard library, no third-party dependencies: + +```sh +python3.12 -I -O -Werror -B research/rank7-cleanup-dirty-identity/verify.py +python3.12 -I -O -Werror -B research/rank7-cleanup-dirty-identity/backward.py +python3.12 -I -O -Werror -B research/rank7-cleanup-dirty-identity/test_verify.py +python3.12 -B scripts/research_package.py --package research/rank7-cleanup-dirty-identity +ruff check research/rank7-cleanup-dirty-identity +``` + +`--emit` on either interpreter reconstructs its JSON receipt on stdout. +Normal replay is read-only. Local checks pass on CPython 3.12.15 and 3.13.5, +Linux 6.6.87.2-microsoft-standard-WSL2 x86_64; Ruff 0.17.1 passes. Tests use +explicit exceptions for acceptance, including under `-O`. + +## Open next questions + +1. Can one of these dirty-private arrays be acquired, kept disjoint and returned + under an actual paid native owner contract? Start with one literal private + interval from PR #3238 and price its physical backing and arithmetic range. + The current block identity does not supply that contract or a cost saving. +2. Can the 91-array boundary contract simplify the original native dependency + cone? Compose it with the already checked native event/warp bindings and + compare the exact required premises with PR #3238. A rechecked native + schedule and its linear-map conventions are prerequisites; do not infer + correctness of the live prefix from this isolated cleanup. + +## Credit and engineering limits + +Nick Petalas. Apache-2.0. Credit Marius-Paul Dumitrean for PR #2979/#2942's +words; Jeremy Kothe for the inverse cleanup, frame and rewrite lineage; +Mason Hale and Jeremy Diviney for PR #2917/#2908's paired extraction chain; +commdata2338 for PR #3238's explicit arbitrary-entrance handoff and original +private-free audit; 24kHandsome1201 for PR #3208's separate R2 result and +method context; ToikY for PR #3038's source/native machinery; and the retained +source geometry, compiler and owner contributors credited in PR #2979. +New code imports no predecessor implementation. Research, implementation and +checking used substantial automated assistance; no independent human review +is claimed. + +Build the Lever led to the retained full-matrix and reverse-covector tools. +Prove It Works required literal source replay and the clean-only blind-spot +control. Power-of-Ten constraints bound source payloads to 4 MB, gates to 6,000, +registers to 800, terms per polynomial to 4,096, word length to 256, and rational +numerator/denominator sizes to 4,096 bits. Capacity failures raise errors; +functions remain below 60 physical lines. Registered commands have finite +timeouts. The Python managed-runtime deviation from fixed post-initialization +allocation is restricted to these bounded polynomials and fixtures. Python's +ordinary dynamic dispatch and unittest framework are the corresponding +rules 8/9 deviations, with only the two named local interpreters as test +imports and no dynamic predecessor loading. Reassess these capacities and +resource contracts before enlarging the domain or adopting a physical caller. diff --git a/research/rank7-cleanup-dirty-identity/RESULT.json b/research/rank7-cleanup-dirty-identity/RESULT.json new file mode 100644 index 0000000000..9da0157b47 --- /dev/null +++ b/research/rank7-cleanup-dirty-identity/RESULT.json @@ -0,0 +1,430 @@ +{ + "cases": { + "base": [ + { + "changed_live_rows": 429, + "gates": 5207, + "last_touches": { + "1002": 4484, + "1003": 4844, + "1008": 4913, + "1011": 4326, + "1013": 4348, + "1015": 4709, + "1018": 4344, + "1024": 4867, + "1027": 4193, + "1029": 4944, + "1031": 4945, + "1034": 4207, + "1035": 4825, + "1041": 4045, + "1043": 4047, + "1045": 4065, + "1050": 4061, + "1057": 3903, + "1059": 3905, + "1061": 3923, + "1066": 3919, + "1067": 5185, + "1073": 3761, + "1075": 3763, + "1077": 3781, + "1082": 3777, + "1089": 3619, + "1091": 3621, + "1093": 3639, + "1098": 3635, + "1099": 5206, + "1112": 4736, + "1116": 4806, + "1128": 4760, + "1132": 4783, + "1152": 1137, + "1153": 1136, + "1154": 1135, + "1155": 1134, + "1156": 1133, + "1157": 1132, + "1158": 1131, + "1159": 1130, + "1188": 1075, + "1189": 1073, + "1202": 4712, + "1203": 4934, + "1204": 4691, + "1205": 4694, + "1212": 1021, + "1213": 1019, + "1214": 4945, + "1215": 4889, + "1216": 4661, + "1217": 4657, + "1235": 1198, + "1236": 971, + "1237": 969, + "1247": 1194, + "1258": 4637, + "1259": 1206, + "1260": 921, + "1261": 919, + "1270": 1211, + "1271": 1202, + "1276": 4664, + "1277": 4642, + "1278": 4647, + "1279": 4644, + "1284": 4667, + "1285": 4650, + "1286": 4653, + "1287": 4670, + "1288": 891, + "1289": 890, + "1290": 4639, + "1291": 886, + "1292": 4640, + "1293": 882, + "1294": 1211, + "1295": 878, + "930": 5087, + "932": 5103, + "934": 5157, + "953": 4973, + "955": 5030, + "969": 5067, + "971": 5002, + "981": 4625, + "986": 4621, + "997": 4488 + }, + "live": 632, + "matrix_sha256": "f4d62579fca138df6e34aedac731bc66593eb66f76a71f4c4d18a02bc2c2702a", + "max_row_terms": 112, + "orientation": "forward", + "private": 91, + "private_identity": true, + "private_to_live_zero": true, + "target_identity_count": 112 + }, + { + "changed_live_rows": 397, + "gates": 5207, + "last_touches": { + "1002": 4484, + "1003": 4844, + "1008": 4913, + "1011": 4326, + "1013": 4348, + "1015": 4709, + "1018": 4344, + "1024": 4867, + "1027": 4193, + "1029": 4944, + "1031": 4945, + "1034": 4207, + "1035": 4825, + "1041": 4045, + "1043": 4047, + "1045": 4065, + "1050": 4061, + "1057": 3903, + "1059": 3905, + "1061": 3923, + "1066": 3919, + "1067": 5185, + "1073": 3761, + "1075": 3763, + "1077": 3781, + "1082": 3777, + "1089": 3619, + "1091": 3621, + "1093": 3639, + "1098": 3635, + "1099": 5206, + "1112": 4736, + "1116": 4806, + "1128": 4760, + "1132": 4783, + "1152": 1137, + "1153": 1136, + "1154": 1135, + "1155": 1134, + "1156": 1133, + "1157": 1132, + "1158": 1131, + "1159": 1130, + "1188": 1075, + "1189": 1073, + "1202": 4712, + "1203": 4934, + "1204": 4691, + "1205": 4694, + "1212": 1021, + "1213": 1019, + "1214": 4945, + "1215": 4889, + "1216": 4661, + "1217": 4657, + "1235": 1198, + "1236": 971, + "1237": 969, + "1247": 1194, + "1258": 4637, + "1259": 1206, + "1260": 921, + "1261": 919, + "1270": 1211, + "1271": 1202, + "1276": 4664, + "1277": 4642, + "1278": 4647, + "1279": 4644, + "1284": 4667, + "1285": 4650, + "1286": 4653, + "1287": 4670, + "1288": 891, + "1289": 890, + "1290": 4639, + "1291": 886, + "1292": 4640, + "1293": 882, + "1294": 1211, + "1295": 878, + "930": 5087, + "932": 5103, + "934": 5157, + "953": 4973, + "955": 5030, + "969": 5067, + "971": 5002, + "981": 4625, + "986": 4621, + "997": 4488 + }, + "live": 632, + "matrix_sha256": "409b731776a869e906dc54afe075e2b2f1d70be33129a0b0644152d6a0e05738", + "max_row_terms": 120, + "orientation": "dual", + "private": 91, + "private_identity": true, + "private_to_live_zero": true, + "target_identity_count": 112 + } + ], + "extra": [ + { + "changed_live_rows": 429, + "gates": 5207, + "last_touches": { + "1002": 4484, + "1003": 4844, + "1008": 4913, + "1011": 4326, + "1013": 4348, + "1015": 4709, + "1018": 4344, + "1024": 4867, + "1027": 4193, + "1029": 4944, + "1031": 4945, + "1034": 4207, + "1035": 4825, + "1041": 4045, + "1043": 4047, + "1045": 4065, + "1050": 4061, + "1057": 3903, + "1059": 3905, + "1061": 3923, + "1066": 3919, + "1067": 5185, + "1073": 3761, + "1075": 3763, + "1077": 3781, + "1082": 3777, + "1089": 3619, + "1091": 3621, + "1093": 3639, + "1098": 3635, + "1099": 5206, + "1112": 4736, + "1116": 4806, + "1128": 4760, + "1132": 4783, + "1152": 1137, + "1153": 1136, + "1154": 1135, + "1155": 1134, + "1156": 1133, + "1157": 1132, + "1158": 1131, + "1159": 1130, + "1188": 1075, + "1189": 1073, + "1202": 4712, + "1203": 4934, + "1204": 4691, + "1205": 4694, + "1212": 1021, + "1213": 1019, + "1214": 4945, + "1215": 4889, + "1216": 4661, + "1217": 4657, + "1235": 1198, + "1236": 971, + "1237": 969, + "1247": 1194, + "1258": 4637, + "1259": 1206, + "1260": 921, + "1261": 919, + "1270": 1211, + "1271": 1202, + "1276": 4664, + "1277": 4642, + "1278": 4647, + "1279": 4644, + "1284": 4667, + "1285": 4650, + "1286": 4653, + "1287": 4670, + "1288": 891, + "1289": 890, + "1290": 4639, + "1291": 886, + "1292": 4640, + "1293": 882, + "1294": 1211, + "1295": 878, + "930": 5087, + "932": 5103, + "934": 5157, + "953": 4973, + "955": 5030, + "969": 5067, + "971": 5002, + "981": 4625, + "986": 4621, + "997": 4488 + }, + "live": 632, + "matrix_sha256": "f4d62579fca138df6e34aedac731bc66593eb66f76a71f4c4d18a02bc2c2702a", + "max_row_terms": 112, + "orientation": "forward", + "private": 91, + "private_identity": true, + "private_to_live_zero": true, + "target_identity_count": 112 + }, + { + "changed_live_rows": 397, + "gates": 5207, + "last_touches": { + "1002": 4484, + "1003": 4844, + "1008": 4913, + "1011": 4326, + "1013": 4348, + "1015": 4709, + "1018": 4344, + "1024": 4867, + "1027": 4193, + "1029": 4944, + "1031": 4945, + "1034": 4207, + "1035": 4825, + "1041": 4045, + "1043": 4047, + "1045": 4065, + "1050": 4061, + "1057": 3903, + "1059": 3905, + "1061": 3923, + "1066": 3919, + "1067": 5185, + "1073": 3761, + "1075": 3763, + "1077": 3781, + "1082": 3777, + "1089": 3619, + "1091": 3621, + "1093": 3639, + "1098": 3635, + "1099": 5206, + "1112": 4736, + "1116": 4806, + "1128": 4760, + "1132": 4783, + "1152": 1137, + "1153": 1136, + "1154": 1135, + "1155": 1134, + "1156": 1133, + "1157": 1132, + "1158": 1131, + "1159": 1130, + "1188": 1075, + "1189": 1073, + "1202": 4712, + "1203": 4934, + "1204": 4691, + "1205": 4694, + "1212": 1021, + "1213": 1019, + "1214": 4945, + "1215": 4889, + "1216": 4661, + "1217": 4657, + "1235": 1198, + "1236": 971, + "1237": 969, + "1247": 1194, + "1258": 4637, + "1259": 1206, + "1260": 921, + "1261": 919, + "1270": 1211, + "1271": 1202, + "1276": 4664, + "1277": 4642, + "1278": 4647, + "1279": 4644, + "1284": 4667, + "1285": 4650, + "1286": 4653, + "1287": 4670, + "1288": 891, + "1289": 890, + "1290": 4639, + "1291": 886, + "1292": 4640, + "1293": 882, + "1294": 1211, + "1295": 878, + "930": 5087, + "932": 5103, + "934": 5157, + "953": 4973, + "955": 5030, + "969": 5067, + "971": 5002, + "981": 4625, + "986": 4621, + "997": 4488 + }, + "live": 632, + "matrix_sha256": "409b731776a869e906dc54afe075e2b2f1d70be33129a0b0644152d6a0e05738", + "max_row_terms": 120, + "orientation": "dual", + "private": 91, + "private_identity": true, + "private_to_live_zero": true, + "target_identity_count": 112 + } + ] + }, + "scope": "Literal FULL-frame scalar/free-associative-operator cleanup; no native or physical admission.", + "status": "PASS_RANK7_CLEANUP_DIRTY_IDENTITY" +} diff --git a/research/rank7-cleanup-dirty-identity/SOURCES.json b/research/rank7-cleanup-dirty-identity/SOURCES.json new file mode 100644 index 0000000000..212d5b608e --- /dev/null +++ b/research/rank7-cleanup-dirty-identity/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/rank7-joint-endframes/data/WORD-base.json.gz", + "usage": "input", + "git_blob": "d9aa96a93fea5f7395e7783aef0bc117c0a0ae89", + "sha256": "abaf67bfcb257528658c906b612f57025617592bd7889828f92b97a5f4f4300d" + }, + { + "path": "research/rank7-joint-endframes/data/WORD-extra.json.gz", + "usage": "input", + "git_blob": "74f6cb64595c21f7726ae77e69437868620bdcee", + "sha256": "e0eaf64c4d5d324693d43889bce1b9e53e8da00402105c8c978fd102f208bed7" + } + ] +} diff --git a/research/rank7-cleanup-dirty-identity/TASK.json b/research/rank7-cleanup-dirty-identity/TASK.json new file mode 100644 index 0000000000..fe1a2d76b4 --- /dev/null +++ b/research/rank7-cleanup-dirty-identity/TASK.json @@ -0,0 +1,91 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 6, + "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json", + "research/rank7-joint-endframes/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering" + ] + }, + "scope_status": "refined", + "actual_scope": "Prove or falsify the original PR2979 isolated cleanup's block identity on arbitrary live and arbitrary dirty private entrance arrays, answering PR3238's explicit unrun question. Both providers, both orientations, all 91 private rows/columns and literal last touches; no prefix or complete native/physical admission.", + "scope_change_reason": "Existing joint/single, group-A native, full private-free and R2 cleanup audits already cover the older entry points. PR3238 explicitly leaves arbitrary cleanup entrance unrun on the original words; strengthen its clean zero-return boundary to a dirty-private identity rather than repeating pricing or the prefix cone.", + "bottleneck_link": "Removes the preceding-prefix reachable-state premise from a specific cleanup proof and establishes a conditional dirty-borrowing interface. It does not eliminate any physical arrays or establish a cheaper paid profile.", + "budget_minutes": 60, + "stop_rule": "Stop after the literal finite block identity, separate backward row/column check and semantic failure controls. No new lowering census, native source regeneration or supplier expansion.", + "outcome": "completed", + "evidence": "README.md written proof; RESULT.json full formal-matrix hashes and last touches; BACKWARD.json 728 separately implemented row/column checks; test_verify.py eleven behavioral groups, including a dirty-only fault invisible to clean replay.", + "author": "Nick Petalas", + "ai_assistance": "Substantial automated assistance was used. No independent human or proof-kernel review is claimed.", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2612#discussioncomment-19002977", + "predecessor_heads": { + "2979": "be191346391661f4d35fc0d1508d0a6029572576", + "3238": "3c689aac34ff240f82e27dcc7f0247b96b8676af", + "3208": "87d63a82defff1ffeea173743106fb97903cbbd6" + }, + "overlap": { + "queries": ["--task independent-moment", "arbitrary cleanup entrance", "rank7 cleanup", "3238"], + "open_prs": {"records": 284, "fetched_at": "2026-10-17T18:59:06.262982+00:00", "complete_pagination": true}, + "discussions": {"records": 2059, "fetched_at": "2026-10-17T18:59:36.541458+00:00", "complete_pagination": true}, + "limits": "Titles/bodies/comments and local package notes; no arbitrary diff or unpublished-work coverage.", + "submission_refresh": { + "canonical_main": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "checked_at": "2026-10-17T19:08:36Z", + "guidance_or_source_delta": "none", + "open_prs": {"records": 288, "fetched_at": "2026-10-17T19:08:36.075393+00:00", "complete_pagination": true}, + "discussions": {"records": 2067, "fetched_at": "2026-10-17T19:09:05.450270+00:00", "complete_pagination": true} + } + }, + "open_questions": [ + { + "question": "Can one dirty-private array be acquired and returned under an actual paid native owner contract?", + "why_it_matters": "Only a complete physical caller can turn the dirty-private identity into a resource or stock saving.", + "first_step": "Pin one literal private interval from PR3238 and price its disjoint backing, access and arithmetic range.", + "blocked_by": "Borrowing, hosting, finite precision and native allocation/free contracts are not supplied here." + }, + { + "question": "Can this entrance-independent identity simplify the original native private-return dependency cone?", + "why_it_matters": "A source-bound composition could remove unnecessary prefix assumptions from the finite audit.", + "first_step": "Join the literal cleanup to PR3238's native event/warp bindings and compare the exact resulting premises.", + "blocked_by": "The actual native schedule and linear-map conventions need binding; no live-prefix theorem follows from this cleanup alone." + } + ] +} diff --git a/research/rank7-cleanup-dirty-identity/VERIFY.json b/research/rank7-cleanup-dirty-identity/VERIFY.json new file mode 100644 index 0000000000..910a8030ce --- /dev/null +++ b/research/rank7-cleanup-dirty-identity/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/rank7-joint-endframes/data/WORD-base.json.gz", + "research/rank7-joint-endframes/data/WORD-extra.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Source-bound literal free-associative full matrix, dirty-private identity/no leakage, target identities, last touches and deterministic receipt." + }, + { + "argv": ["{python}", "-I", "-O", "-Werror", "-B", "{package}/backward.py"], + "timeout_seconds": 60, + "checks": "Separate reverse right-polynomial propagation of 728 private output rows and input columns; no forward interpreter or predecessor import." + }, + { + "argv": ["{python}", "-I", "-O", "-Werror", "-B", "{package}/test_verify.py"], + "timeout_seconds": 60, + "checks": "Eleven behavioral groups, actual closing faults, dirty-only leakage missed by clean replay, early return, noncommuting/transpose fixtures, source/schema/capacity and receipt controls." + } + ] +} diff --git a/research/rank7-cleanup-dirty-identity/backward.py b/research/rank7-cleanup-dirty-identity/backward.py new file mode 100644 index 0000000000..f96769a135 --- /dev/null +++ b/research/rank7-cleanup-dirty-identity/backward.py @@ -0,0 +1,138 @@ +#!/usr/bin/env python3 +"""Separate free-associative right-covector check; no forward interpreter import.""" + +import gzip +import hashlib +import io +import json +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def check(condition, message): + if not condition: + raise ValueError(message) + + +def append_letter(word, operator): + result = word + (operator,) + check(len(result) <= 256, "backward word bound") + return result + + +def reverse_row(gates, output, dual): + """Pull one output covector backwards, multiplying operators on the right.""" + check(len(gates) <= 6000, "backward gate bound") + covector = {output: {(): Fraction(1)}} + peak = 1 + for raw in reversed(gates): + kind, target = raw[:2] + if kind == "add": + source, coefficient = raw[2], Fraction(raw[3], raw[4]) + if dual: + target, source, coefficient = source, target, -coefficient + if target in covector: + terms = covector.setdefault(source, {}) + for word, value in covector[target].items(): + total = terms.get(word, 0) + coefficient * value + if total: + terms[word] = total + else: + terms.pop(word, None) + if not terms: + del covector[source] + elif kind == "scale": + coefficient = Fraction(raw[3], raw[2]) if dual else Fraction(raw[2], raw[3]) + if target in covector: + covector[target] = {w: coefficient * c for w, c in covector[target].items()} + elif kind == "warp": + if target in covector: + # In dual mode the alphabet denotes independent K_i^(-T) operators. + covector[target] = {append_letter(w, raw[2]): c + for w, c in covector[target].items()} + else: + raise ValueError("backward unknown gate") + check(len(covector) <= 800, "backward register bound") + touched = (target, source) if kind == "add" else (target,) + for register in touched: + polynomial = covector.get(register, {}) + check(len(polynomial) <= 4096, "backward polynomial bound") + check(all(abs(c.numerator).bit_length() <= 4096 and c.denominator.bit_length() <= 4096 + for c in polynomial.values()), "backward coefficient bound") + peak = max(peak, len(covector)) + return covector, peak + + +def transposed_program(gates, dual): + """Reverse order and transpose each gate, with an independent transpose alphabet.""" + check(len(gates) <= 6000, "transpose gate bound") + result = [] + for raw in reversed(gates): + gate = list(raw) + if gate[0] == "add": + if dual: + gate[3] = -gate[3] + else: + gate[1], gate[2] = gate[2], gate[1] + elif gate[0] == "scale" and dual: + gate[2], gate[3] = gate[3], gate[2] + result.append(gate) + return result + + +def load_entries(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + entries = [entry for entry in manifest["files"] if entry["usage"] == "input"] + check(len(entries) == 2, "backward provider count") + return entries + + +def load_source(entry): + path = ROOT / entry["path"] + check(path.stat().st_size <= 4_000_000, "backward source capacity") + raw = path.read_bytes() + check(hashlib.sha256(raw).hexdigest() == entry["sha256"], "backward source hash") + with gzip.GzipFile(fileobj=io.BytesIO(raw)) as stream: + data = stream.read(4_000_001) + check(len(data) <= 4_000_000, "backward payload capacity") + word = json.loads(data) + check(word["report"]["v"] == 112 and word["report"]["R"] == 480, "backward geometry") + check(len(word["cleanup"]) == 5207, "backward cleanup length") + return word + + +def audit(): + cases = [] + for entry in load_entries(): + word = load_source(entry) + private = sorted(int(r) + 704 for r in word["helper_final"]) + check(len(private) == len(set(private)) == 91, "backward private count") + for dual in (False, True): + peak = 1 + columns = transposed_program(word["cleanup"], dual) + for register in private: + row, size = reverse_row(word["cleanup"], register, dual) + check(row == {register: {(): Fraction(1)}}, "backward private row failed") + column, column_size = reverse_row(columns, register, False) + check(column == {register: {(): Fraction(1)}}, "backward private column failed") + peak = max(peak, size, column_size) + cases.append({"input": entry["path"], "dual": dual, "private_rows": 91, + "private_columns": 91, "peak_covector_registers": peak}) + return {"status": "PASS_RANK7_CLEANUP_BACKWARD", "cases": cases} + + +if __name__ == "__main__": + import argparse + + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true") + args = parser.parse_args() + result = audit() + if args.emit: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + check(result == json.loads((HERE / "BACKWARD.json").read_text()), "backward receipt mismatch") + print("PASS_RANK7_CLEANUP_BACKWARD private_covectors=728 rows_and_columns right_operator_multiplication") diff --git a/research/rank7-cleanup-dirty-identity/test_verify.py b/research/rank7-cleanup-dirty-identity/test_verify.py new file mode 100644 index 0000000000..83ee9a86bf --- /dev/null +++ b/research/rank7-cleanup-dirty-identity/test_verify.py @@ -0,0 +1,171 @@ +#!/usr/bin/env python3 +"""Behavioral controls for the literal contract and the two algebra interpreters.""" + +import copy +import sys +import tempfile +import unittest +from dataclasses import replace +from fractions import Fraction as Q +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import backward +import verify as v + + +def execute(model, dual=False, dirty=True): + rows = {r: v.identity(r) for r in model.live} + rows.update({r: v.identity(r) if dirty else {} for r in model.private}) + for gate in model.gates: + v.apply(v.oriented(gate, dual), rows) + return rows + + +class CleanupTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + entries = [e for e in v.read_json(v.PACKAGE / "SOURCES.json")["files"] + if e["usage"] == "input"] + cls.entry = entries[0] + cls.word = v.read_word(v.ROOT, cls.entry) + cls.model = v.decode(cls.word) + + def test_literal_positive_and_receipts(self): + self.assertEqual(v.audit(), v.read_json(v.PACKAGE / "RESULT.json")) + self.assertEqual(backward.audit(), v.read_json(v.PACKAGE / "BACKWARD.json")) + + def test_source_and_duplicate_json_fail_closed(self): + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + source = root / self.entry["path"] + source.parent.mkdir(parents=True) + source.write_bytes((v.ROOT / self.entry["path"]).read_bytes() + b"x") + with self.assertRaisesRegex(ValueError, "source hash"): + v.read_word(root, self.entry) + duplicate = root / "duplicate.json" + duplicate.write_text('{"x": 1, "x": 2}') + with self.assertRaisesRegex(ValueError, "duplicate JSON"): + v.read_json(duplicate) + + def test_literal_contract_mutations(self): + for mutation in ("length", "frame", "register", "private", "denominator", "operator"): + word = copy.deepcopy(self.word) + if mutation == "length": + word["cleanup"].pop() + elif mutation == "frame": + word["cleanup"][0][-1] = [] + elif mutation == "register": + word["cleanup"][0][1] = word["removed"][0] + elif mutation == "private": + word["helper_final"].pop(next(iter(word["helper_final"]))) + elif mutation == "denominator": + word["cleanup"][0][4] = 0 + else: + next(g for g in word["cleanup"] if g[0] == "warp")[2] = 0 + with self.subTest(mutation=mutation), self.assertRaises(ValueError): + v.decode(word) + + def test_actual_gate_deletion_and_coefficient(self): + closing = v.last_touches(self.model)[930] + mutations = [] + gates = list(self.model.gates) + gates[closing] = replace(gates[closing], coefficient=-gates[closing].coefficient) + mutations.append(gates) + gates = list(self.model.gates) + gates.pop(closing) + mutations.append(gates) + for index, gates in enumerate(mutations): + with self.subTest(index=index), self.assertRaises(ValueError): + v.replay(replace(self.model, gates=tuple(gates)), False) + + def test_warp_fault_changes_live_map_not_private_contract(self): + index = next(i for i, gate in enumerate(self.model.gates) if gate.kind == "warp") + gates = list(self.model.gates) + gates[index] = replace(gates[index], operator=-gates[index].operator) + result = v.replay(replace(self.model, gates=tuple(gates)), False) + original = v.replay(self.model, False) + self.assertTrue(result["private_identity"]) + self.assertNotEqual(result["matrix_sha256"], original["matrix_sha256"]) + + def test_dirty_only_leak_is_invisible_to_clean_replay(self): + # The last use of private 1003 reads it into live 302. It is zero for + # clean entrance, but is exactly its arbitrary entrance for dirty input. + index = v.last_touches(self.model)[1003] + self.assertEqual(index, 4844) + gates = list(self.model.gates) + self.assertEqual((gates[index].target, gates[index].source), (302, 1003)) + gates[index] = replace(gates[index], coefficient=2 * gates[index].coefficient) + mutant = replace(self.model, gates=tuple(gates)) + self.assertEqual(execute(mutant, dirty=False), execute(self.model, dirty=False)) + with self.assertRaises(ValueError): + v.replay(mutant, False) + original_rows, changed_rows = execute(self.model), execute(mutant) + differences = {} + for register in changed_rows: + keys = set(changed_rows[register]) | set(original_rows[register]) + delta = {key: changed_rows[register].get(key, 0) - original_rows[register].get(key, 0) + for key in keys} + delta = {key: value for key, value in delta.items() if value} + if delta: + differences[register] = delta + self.assertEqual(differences, {302: {(1003, ()): -Q(1, 4)}, + 930: {(1003, ()): Q(1, 8)}, + 934: {(1003, ()): Q(1, 8)}}) + + def test_early_return_is_not_an_endpoint_identity(self): + rows = {r: v.identity(r) for r in self.model.live + self.model.private} + for gate in self.model.gates[:3]: + v.apply(gate, rows) + self.assertNotEqual(rows[1099], v.identity(1099)) + self.assertGreater(v.last_touches(self.model)[1099], 2) + + def test_left_and_right_interpreters_on_noncommuting_word(self): + raw = [["add", 0, 1, 1, 2, v.FULL], ["warp", 0, 1, v.FULL], + ["warp", 0, 2, v.FULL], ["add", 2, 0, -3, 2, v.FULL], + ["warp", 0, -1, v.FULL], ["scale", 1, 1, -2, v.FULL]] + gates = tuple(v.parse_gate(g, {0, 1, 2}, 2) for g in raw) + for dual in (False, True): + rows = execute(v.Model(gates, (0, 1, 2), ()), dual) + for output in range(3): + covector, _ = backward.reverse_row(raw, output, dual) + expected = {(source, word): value for source, polynomial in covector.items() + for word, value in polynomial.items()} + self.assertEqual(rows[output], expected) + column, _ = backward.reverse_row(backward.transposed_program(raw, dual), output, False) + expected_column = {(target, word[::-1]): value for target, polynomial in column.items() + for word, value in polynomial.items()} + actual_column = {(target, word): value for target, polynomial in rows.items() + for (source, word), value in polynomial.items() if source == output} + self.assertEqual(actual_column, expected_column) + rows = execute(v.Model(gates, (0, 1, 2), ())) + self.assertIn((0, (-1, 2, 1)), rows[0]) + self.assertNotIn((0, (2,)), rows[0]) + + def test_no_inverse_cancellation_and_capacity(self): + self.assertEqual(v.prepend(-3, (3, 2)), (-3, 3, 2)) + self.assertEqual(backward.append_letter((2, 3), -3), (2, 3, -3)) + self.assertEqual(v.prepend(-3, (2, 3)), (-3, 2, 3)) + with self.assertRaisesRegex(ValueError, "word capacity"): + v.prepend(1, (1,) * 256) + with self.assertRaisesRegex(ValueError, "polynomial capacity"): + v.bounded({(r, ()): Q(1) for r in range(v.MAX_TERMS + 1)}) + with self.assertRaisesRegex(ValueError, "coefficient capacity"): + v.bounded({(0, ()): Q(1 << 4096)}) + + def test_private_input_leak_and_dirty_private_scaling(self): + live, private = self.model.live[0], self.model.private[0] + for gate in (v.Gate("add", live, private), + v.Gate("scale", private, coefficient=Q(2))): + mutant = replace(self.model, gates=self.model.gates + (gate,)) + with self.subTest(kind=gate.kind), self.assertRaises(ValueError): + v.replay(mutant, False) + + def test_receipt_corruption(self): + result = v.read_json(v.PACKAGE / "RESULT.json") + result["cases"]["base"][0]["last_touches"]["930"] -= 1 + self.assertNotEqual(v.audit(), result) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/rank7-cleanup-dirty-identity/verify.py b/research/rank7-cleanup-dirty-identity/verify.py new file mode 100644 index 0000000000..dbf3fd13d5 --- /dev/null +++ b/research/rank7-cleanup-dirty-identity/verify.py @@ -0,0 +1,255 @@ +#!/usr/bin/env python3 +"""Exact private/live block identity for PR2979's literal cleanup only.""" + +from __future__ import annotations + +import argparse +import gzip +import hashlib +import io +import json +from dataclasses import dataclass +from fractions import Fraction +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +MAX_BYTES = 4_000_000 +MAX_REGISTERS = 800 +MAX_GATES = 6000 +MAX_TERMS = 4096 +MAX_WORD = 256 +FULL = [256, 128, 64, 32, 16, 8, 4, 2, 1] +Term = tuple[int, tuple[int, ...]] +Polynomial = dict[Term, Fraction] + + +@dataclass(frozen=True) +class Gate: + kind: str + target: int + source: int = 0 + coefficient: Fraction = Fraction(1) + operator: int = 0 + + +@dataclass(frozen=True) +class Model: + gates: tuple[Gate, ...] + live: tuple[int, ...] + private: tuple[int, ...] + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def unique_object(pairs: list[tuple[str, object]]) -> dict: + result = {} + for key, value in pairs: + require(key not in result, f"duplicate JSON key: {key}") + result[key] = value + return result + + +def read_json(path: Path) -> dict: + require(path.stat().st_size <= MAX_BYTES, "input file too large") + result = json.loads(path.read_bytes(), object_pairs_hook=unique_object) + require(isinstance(result, dict), "expected JSON object") + return result + + +def read_word(root: Path, entry: dict) -> dict: + path = root / entry["path"] + require(path.stat().st_size <= MAX_BYTES, "compressed source too large") + raw = path.read_bytes() + require(hashlib.sha256(raw).hexdigest() == entry["sha256"], "source hash mismatch") + with gzip.GzipFile(fileobj=io.BytesIO(raw)) as stream: + payload = stream.read(MAX_BYTES + 1) + require(len(payload) <= MAX_BYTES, "decompressed source too large") + word = json.loads(payload, object_pairs_hook=unique_object) + require(isinstance(word, dict), "word must be an object") + return word + + +def integer(value: object) -> int: + require(type(value) is int and abs(value) <= 1_000_000, "invalid bounded integer") + return value + + +def parse_gate(raw: list, allowed: set[int], operators: int) -> Gate: + require(isinstance(raw, list) and len(raw) in (4, 5, 6), "gate shape") + require(raw[-1] == FULL, "cleanup gate is not at FULL") + kind, target = raw[0], integer(raw[1]) + require(target in allowed, "invalid target register") + if kind == "warp": + require(len(raw) == 4, "warp shape") + op = integer(raw[2]) + require(0 < abs(op) <= operators, "invalid warp operator") + return Gate(kind, target, operator=op) + require(kind in ("add", "scale"), "unknown gate kind") + require(len(raw) == (6 if kind == "add" else 5), "scalar gate shape") + numerator, denominator = map(integer, raw[-3:-1]) + require(denominator != 0, "zero denominator") + coefficient = Fraction(numerator, denominator) + denominator = coefficient.denominator + require(denominator & (denominator - 1) == 0, "dyadic denominator") + require(coefficient != 0, "zero scalar") + if kind == "scale": + numerator = abs(coefficient.numerator) + require(numerator & (numerator - 1) == 0, "nonunit scale") + return Gate(kind, target, coefficient=coefficient) + source = integer(raw[2]) + require(source in allowed and source != target, "invalid ADD source") + return Gate(kind, target, source, coefficient) + + +def decode(word: dict) -> Model: + require(word["kind"] == "BORROW-WORD", "wrong word kind") + report = word["report"] + require((report["v"], report["h"], report["R"]) == (112, 9, 480), "wrong geometry") + removed = tuple(map(integer, word["removed"])) + require(len(set(removed)) == len(removed) == 72, "removed inventory") + require(all(224 <= r < 704 for r in removed), "removed range") + live = tuple(r for r in range(704) if r not in removed) + helpers = tuple(sorted(int(r) for r in word["helper_final"])) + require(len(helpers) == len(set(helpers)) == 91, "private inventory") + require(all(r in live and r >= 224 for r in helpers), "private owner range") + private = tuple(r + 704 for r in helpers) + require(len(live) == 632 and len(live + private) <= MAX_REGISTERS, "register bound") + require(1 <= len(word["warps"]) <= 256, "operator count") + require(len(word["cleanup"]) == 5207, "literal cleanup length") + allowed = set(live + private) + gates = tuple(parse_gate(g, allowed, len(word["warps"])) for g in word["cleanup"]) + return Model(gates, live, private) + + +def oriented(gate: Gate, dual: bool) -> Gate: + if not dual: + return gate + if gate.kind == "add": + return Gate("add", gate.source, gate.target, -gate.coefficient) + if gate.kind == "scale": + return Gate("scale", gate.target, coefficient=1 / gate.coefficient) + # These symbols denote K_i^(-T), not K_i or K_i^T. + return gate + + +def prepend(operator: int, word: tuple[int, ...]) -> tuple[int, ...]: + # Signed names are independent generators. No inverse or commutation law. + result = (operator,) + word + require(len(result) <= MAX_WORD, "operator word capacity") + return result + + +def bounded(polynomial: Polynomial) -> None: + require(len(polynomial) <= MAX_TERMS, "polynomial capacity") + require(all(abs(v.numerator).bit_length() <= 4096 and v.denominator.bit_length() <= 4096 + for v in polynomial.values()), "coefficient capacity") + + +def apply(gate: Gate, rows: dict[int, Polynomial]) -> None: + target = rows[gate.target] + if gate.kind == "add": + for key, value in rows[gate.source].items(): + total = target.get(key, Fraction(0)) + gate.coefficient * value + if total: + target[key] = total + else: + target.pop(key, None) + elif gate.kind == "scale": + rows[gate.target] = {k: gate.coefficient * v for k, v in target.items()} + elif gate.kind == "warp": + rows[gate.target] = {(r, prepend(gate.operator, w)): v + for (r, w), v in target.items()} + else: + raise ValueError("unknown internal gate") + bounded(rows[gate.target]) + + +def identity(register: int) -> Polynomial: + return {(register, ()): Fraction(1)} + + +def last_touches(model: Model) -> dict[int, int]: + touches = {} + private = set(model.private) + for index, gate in enumerate(model.gates): + registers = (gate.target, gate.source) if gate.kind == "add" else (gate.target,) + for register in registers: + if register in private: + touches[register] = index + require(set(touches) == private, "untouched private array") + return touches + + +def matrix_digest(rows: dict[int, Polynomial]) -> str: + digest = hashlib.sha256() + for register, polynomial in sorted(rows.items()): + for (source, word), value in sorted(polynomial.items()): + digest.update(json.dumps([register, source, word, str(value)], + separators=(",", ":")).encode()) + digest.update(b"\n") + return digest.hexdigest() + + +def replay(model: Model, dual: bool) -> dict: + require(len(model.gates) <= MAX_GATES, "gate capacity") + require(len(model.live + model.private) <= MAX_REGISTERS, "register capacity") + rows = {r: identity(r) for r in model.live + model.private} + touches = last_touches(model) + by_index = {} + for register, index in touches.items(): + by_index.setdefault(index, []).append(register) + max_terms = 1 + for index, raw in enumerate(model.gates): + gate = oriented(raw, dual) + apply(gate, rows) + max_terms = max(max_terms, len(rows[gate.target])) + for register in by_index.get(index, ()): + require(rows[register] == identity(register), f"dirty private last touch: {register}") + require(all(rows[r] == identity(r) for r in model.private), "private block is not identity") + private = set(model.private) + require(all(source not in private for r in model.live for source, _ in rows[r]), + "private input leaked to live output") + targets = [r for r in model.live if 112 <= r < 224] + require(all(rows[r] == identity(r) for r in targets), "cleanup changed targets") + return {"orientation": "dual" if dual else "forward", "gates": len(model.gates), + "live": len(model.live), "private": len(model.private), + "private_identity": True, "private_to_live_zero": True, + "target_identity_count": len(targets), "max_row_terms": max_terms, + "changed_live_rows": sum(rows[r] != identity(r) for r in model.live), + "matrix_sha256": matrix_digest(rows), + "last_touches": {str(r): index for r, index in sorted(touches.items())}} + + +def audit(root: Path = ROOT) -> dict: + sources = read_json(PACKAGE / "SOURCES.json") + entries = [e for e in sources["files"] if e["usage"] == "input"] + require(len(entries) == 2, "expected exactly two providers") + cases = {} + for entry in entries: + model = decode(read_word(root, entry)) + provider = "base" if entry["path"].endswith("WORD-base.json.gz") else "extra" + require(provider not in cases, "duplicate provider") + cases[provider] = [replay(model, dual) for dual in (False, True)] + require(set(cases) == {"base", "extra"}, "provider coverage") + return {"status": "PASS_RANK7_CLEANUP_DIRTY_IDENTITY", "cases": cases, + "scope": "Literal FULL-frame scalar/free-associative-operator cleanup; no native or physical admission."} + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true", help="print receipt instead of comparing it") + args = parser.parse_args() + result = audit() + if args.emit: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + require(result == read_json(PACKAGE / "RESULT.json"), "receipt mismatch") + print("PASS_RANK7_CLEANUP_DIRTY_IDENTITY providers=2 orientations=2 private=91 arbitrary_dirty_entrance") + + +if __name__ == "__main__": + main()