diff --git a/CONTRIBUTORS.md b/CONTRIBUTORS.md index d490b0f3c6..ef24db1475 100644 --- a/CONTRIBUTORS.md +++ b/CONTRIBUTORS.md @@ -143,3 +143,26 @@ verified posts, profile associations and unresolved account identities. - **Michiel Kosters** ([research repository](https://github.com/michielkosters/mathematics_ai/tree/2e0aa64ca09c87fc94f8575f59493f70cf929d71/problems/integer-multiplication-109); Douglas associates @one_line_proof) developed a parallel weighted-hypergraph/coordinate-frame candidate, compressed centers and aligned bit pairing. Our [review](research/parallel-announcements/README.md) reproduces the finite certificate with its transfer/precision limitations explicit. - **Abe / @abe_asfaw**, via a suggestion supplied by Douglas, identified the redundant complex center and its historical 26.5% numerical gain. We [checked the scalar identity, counts and assembly arithmetic](research/parallel-announcements/README.md), and credit this parallel observation alongside the already preserved rank-h center research. + +## Terminal-elision and shrunk-frame submissions + +**SovereignSteak, PR #122**, submitted the Round 15 terminal-accumulator +elimination candidate and its exact majorization audit. The package redirects +updates at their original gate indices and charges the transformed schedule. +The PR's conditional finite certificate is not an unconditional multiplication +theorem. + +**Joel Pulikkan (GamingPuzzled), PR #125**, submitted shrunk lifted frames with +saturated deferral. The contribution delays selected frame growth while +preserving the stated frame contract and exact downstream checks. + +The current stacked research candidate, prepared by **Sennemmi with substantial +OpenAI Codex assistance**, composes those two ideas: it removes terminal roles +from the #125 shrunk-frame profile and charges all direct redirects in the +scalar bound. This is a distinct composition submitted for review; it does not +claim global optimality, a complete theorem proof, or priority over either +source. It is submitted as [Draft PR #140](https://github.com/CrocSwap/integer-mult-bounds/pull/140) +against upstream `main`, with the construction snapshot at +`9cdf73e8682fb12749482e710e50bc585d282a7c`; independent mathematical review is +pending. Inclusion is an attribution record, not external acceptance. Original +source licenses and each contributor's AI disclosures remain applicable. diff --git a/docs/research/contribution-review.md b/docs/research/contribution-review.md index 25602c6a81..ea4f8f9003 100644 --- a/docs/research/contribution-review.md +++ b/docs/research/contribution-review.md @@ -120,3 +120,11 @@ See [CONTRIBUTORS.md](../../CONTRIBUTORS.md) for contributions and parallel work - [#40](https://github.com/CrocSwap/integer-mult-bounds/pull/40), rohanarun: Both fixed bases and copied reversed corners: conditional κ = 3.918734894e-5 > 2^-15. Pinned `43f59ff533598762cbc43a5e14af2bbbc76fabbd`; not imported in the #39 integration pass. + +## Later stacked candidate: terminal elimination on shrunk frames (9 October 2026) + +- **Submission:** [Draft PR #140](https://github.com/CrocSwap/integer-mult-bounds/pull/140), based on upstream `main` with head `sennemmi:research/terminal-elision-shrunk-frames`. +- **Candidate snapshot:** `9cdf73e8682fb12749482e710e50bc585d282a7c`. +- **Pinned sources:** Joel Pulikkan's PR #125 head `dda535bdcfc321a13a1ebd3c2d70e2b5bb72368e`; SovereignSteak's PR #122 head `b1a6f24e57141637b3ff040d6f2ce9d896ffb9bb`. +- **Submitted result:** conditional κ = `110875518403/10^15`, about 0.257% above the fixed #125 parent. The live upstream Draft PR #139 has a higher finite candidate on the separate triple-core lockstep route; this candidate makes no global-frontier claim. +- **Review status:** draft awaiting independent mathematical review. Its finite verifier and controls pass; inherited transfer, analytic, fixed-tape and all-size assembly interfaces remain open proof obligations. diff --git a/research/shrunk-frames/README.md b/research/shrunk-frames/README.md index 03d61f222f..6038ce1455 100644 --- a/research/shrunk-frames/README.md +++ b/research/shrunk-frames/README.md @@ -1,13 +1,17 @@ -# Shrunk lifted frames with saturated deferred readouts +# Terminal-elided shrunk frames with saturated deferred readouts -Conditional **κ = 110591581647/10¹⁵ = 1.10591581647×10⁻⁴**, about -**1.19920% above PR114** (1.09281094468×10⁻⁴), 1.35% -above PR120 and 1.89% above PR118. The complex side still binds. +Conditional **κ = 110875518403/10¹⁵ = 1.10875518403×10⁻⁴**, about +**0.257% above the pinned PR #125 parent** +(110591581647/10¹⁵ = 1.10591581647×10⁻⁴). The complex side still binds. This package keeps PR114's complete construction: PR117's immutable 91,770-addition complex DAG (eumemic), the same carrier matching and 28,705 dirty roles, PR110's lifted binary frames and deferred readouts, and PR114's -saturated placement with priority 2^dim / reached_targets². One step is new. +saturated placement with priority 2^dim / reached_targets². The frame shrink +is PR #125 by Joel Pulikkan. The terminal-role deletion and source-time +redirect idea follows PR #122 by SovereignSteak. This candidate composes them +on the fixed PR #125 word; it does not claim either predecessor's mechanism as +new. ## Shrunk frames @@ -30,17 +34,28 @@ frames. Shrinking stays monotone. Lb_x contains every predecessor frame, and successors are processed later against the updated frames. Deferral candidates use the shrunk start frames. -| Complex network (PR117 DAG) | PR114 | This | +| Complex network (PR117 DAG) | PR #125 parent | This composition | |---|---:|---:| -| roles / carrier links | 28,705 / 71,185 | 28,705 / 71,185 | -| shrunk frames | — | 16,031 | -| deferred readouts | 4,706 | 4,706 | -| strict complex saving | 109305097/10¹² | **110616162/10¹²** | -| κ | 1.09281094468e-4 | **1.10591581647e-4** | - -W = 124,390,992, recursive rank mass 71,647,349,312 and maximum child 574 of -576 are unchanged. Only the split of each role chain into children changes. -Every copied centre, exterior, source/target front, data projector and +| physical roles / carrier links | 28,705 / 71,185 | 28,324 / 71,185* | +| shrunk frames | 16,031 | 16,031 | +| deferred readouts | 4,706 | 4,325 | +| terminal roles removed / direct updates | — | 381 / 1,167 | +| strict complex saving | 110616162/10¹² | **13862528107/125000000000000** | +| κ | 1.10591581647e-4 | **1.10875518403e-4** | + +*The matched DAG's 71,185 links are retained; its `additions + roots - links` +role count is the pre-elimination count. The final physical word removes 381 +terminal roles. Each is an ordinary deferred output role with no later +consumer. For a removed role with old scratch value z and incoming updates +uᵢ, the old pair of readouts contributes `-αz + α(z + Σuᵢ)`. The replacement +adds each `αuᵢ` to its target at the original update time. The independent +audit checks all 1,167 source-time updates, their frames and signs, and two +modular dirty-scratch replays. + +W = 122,848,704, recursive rank mass 70,758,991,424 and maximum child 574 of +576. The deficit remains 1,862,080. The full paid child histogram is +reconstructed from both the forward and reflected frame traces. Every +surviving copied centre, exterior, source/target front, data projector and endpoint correction remains paid. The bit supplier is unchanged: Swapnil Jain's round-seven word, stopped saving 1240189553/10¹³. @@ -50,24 +65,25 @@ Swapnil Jain's round-seven word, stopped saving 1240189553/10¹³. python3 research/shrunk-frames/verify.py ``` -The verifier regenerates everything in a temporary tree. It pins the -shrunk-frame count and all inherited graph counts. Section D of -`complex_deferred.py` rechecks each role chain against the actual shrunk frames: -start, every gate, linked continuations, root frame and F. It checks that each -chain is nested and each frame nondegenerate. It also checks every deferral -frame and target chain. Arbitrary-scratch replays are run over Z/(2^61−1). - -The independent reflection audit consumes the same frames. It covers the -literal inverse, sign-negate and bank-swap word and the complemented frame -incidences. It also checks the paid histogram in both directions, the -bounded readout chunks and three mutations. `certificate.py` recomputes both -moments exactly and rejects the next complex grid point. It also checks the -expanded scalar charge, all 47 strict constraints, seven margins and the next -κ grid point. - -A new control loads PR114's frozen unshrunk profile, which is -`controls/pr114-complex-profile.json`. That profile contracts at PR114's saving -and fails at the new one. +The verifier regenerates the PR #125 parent in memory, checks its frozen +profile and reflection receipt, writes a transient parent word, and builds the +combined output in a temporary tree. Section D of `complex_deferred.py` +rechecks each parent role chain against the actual shrunk frames: start, every +gate, linked continuations, root frame and F. It checks each chain is nested +and every frame is nondegenerate. + +`terminal_elision_audit.py` independently rediscovers the eligible terminal +roles and rebuilds the simultaneous target schedule. It checks every event in +chronological order, source-time snapshots, the exact local dirty-scratch +identity, modular replay, forward and reflected frame transitions, and the +complete child histogram. Four event mutations are rejected. `certificate.py` +recomputes both moments exactly and rejects the next complex grid point. Its +scalar-group bound explicitly includes all 1,167 direct updates; it checks all +47 strict constraints, seven margins and the next κ grid point. + +Frozen comparison profiles are `controls/pr114-complex-profile.json` and +`controls/pr125-complex-profile.json`. The PR #125 parent profile contracts at +its own saving and fails at the composed candidate's larger saving. All retained transfer hypotheses remain unchanged: - simultaneous rational bases and opposite-bank factorization; @@ -81,7 +97,10 @@ are not a new general theorem. This is a finite conditional witness, not an unconditional theorem, a measured speedup or a global optimum. Credits: eumemic (PR117 producer, PR114 saturated placement, reflection audit -and scalar charge, with Anthropic Claude and OpenAI Codex assistance); Avi +and scalar charge); Joel Pulikkan (PR #125 shrunk-frame step, Anthropic Claude +assistance); SovereignSteak (PR #122 terminal-role elimination); this fixed- +parent composition, independent audit and certificate integration were +prepared with OpenAI Codex assistance. Avi Eisenberg / ikeboy (PR110 deferred complex compiler, PR62); Rohan Arun (PR111/113/116/118); icekylinx (PR104/115); Swapnil Jain (round-seven words, lifted frames, deferred readouts); Zhihao Chen / jacklightChen; Aurel Prosz / diff --git a/research/shrunk-frames/SOURCE.json b/research/shrunk-frames/SOURCE.json index e7f712ae00..3c72b59a02 100644 --- a/research/shrunk-frames/SOURCE.json +++ b/research/shrunk-frames/SOURCE.json @@ -1,22 +1,30 @@ { - "attribution": "Avi Eisenberg / ikeboy (PR62 and PR110, Anthropic Claude assistance); Rohan Arun (PR111, Anthropic Claude assistance); Swapnil Jain (round-seven bit word); icekylinx (retained stopped-product, copied-center and finite assembly interfaces); Zhihao Chen and RaD (retained assembly). PR117 scalar DAG is separate upstream work by eumemic with Anthropic Claude assistance, retained byte for byte with its original attribution. Saturated deferred-frame integration and verification for eumemic with OpenAI Codex assistance. Shrunk-frame step by Joel Pulikkan with Anthropic Claude assistance (PR114 base). Original source notices remain authoritative.", + "attribution": "Avi Eisenberg / ikeboy (PR62 and PR110, Anthropic Claude assistance); Rohan Arun (PR111, Anthropic Claude assistance); Swapnil Jain (round-seven bit word); icekylinx (retained stopped-product, copied-center and finite assembly interfaces); Zhihao Chen and RaD (retained assembly). PR117 scalar DAG is separate upstream work by eumemic with Anthropic Claude assistance, retained byte for byte with its original attribution. PR125 shrunk-frame step by Joel Pulikkan with Anthropic Claude assistance. PR122 terminal-role elimination by SovereignSteak is the predecessor for source-time redirects. Their work is preserved and cited; the fixed-parent composition, candidate generation, independent audit, and certificate integration were prepared with OpenAI Codex assistance. Original source notices remain authoritative.", "package_files": { + "README.md": "ad2c1d9efa34895d13409ccb22301a975e60463fc2dca84460a93cb9a96eec9e", "bit-profile.json": "7293f330518b78650bd86d76b93681e43f3a55541cdb8110993714148a4b4a6a", "bit_round7.py": "35d261a9248c2e06f9179e3c47e554a96b8fe763a9a3de2731256b8c0fbc74b0", - "certificate.json": "e5965daf4346b6a695384f8eda957d954529add921cb384f969856cdef81f845", - "certificate.py": "fa1846facc5eeb33017afd96e9a7b440d3a3d7ff813f76312f1ea865bf2277ca", - "complex-profile.json": "7e7c0c28c0983d117b3006b96719a6102ce31ec0273160dd7fc8b9a0fef0dbeb", + "certificate.json": "a01c78475fd3eac03cde6610a47866176852c6a7dc2375645f599f6e36a54125", + "certificate.py": "f5daca7c764595db596a33f84ac9224a56d085ddaf7381a283d0ba53fd01f78a", + "complex-profile.json": "5d0f6c0d455f187bea24a990560880b11f81bf44281b399cbf40cf00dc3a4bad", "complex_deferred.py": "fa1125e85ec73b185dc9eee117f62d10356bb6422c07ec793a7f77296c87707e", "controls/pr114-complex-profile.json": "a54d2a6023ff73f7476057b5f6a4ff02e65ded840b7254d906aadde2dd01940d", + "controls/pr125-complex-profile.json": "7e7c0c28c0983d117b3006b96719a6102ce31ec0273160dd7fc8b9a0fef0dbeb", "inputs/complex-dag.json.gz": "3c034d0aae388ef567a454826f4f48b26fd8a94c71e8ffed4835271b349a783b", "inputs/deferred_23.json.gz": "8c38e947ff9e021e308000dd82bb5e2194eb265d8b75194e22ce783d3e75317c", "inputs/witness_23.json.gz": "b2486aa2bb222bacea6e52162a3920780e45dd8edc5d7cb03eabea336a1c6588", + "prepare.py": "a6bfc5a547a98575ee9fff0cf3572841981c14bda2005e6bb38601d75b11680b", "producer.py": "017e50713943e6c2a98d1c23ec93e7da9580896de1b6bde24563b4b6961c74c0", "reflection-audit.json": "7caee26f3747b88b41137527175d41b08c4849a7302368bd50b1cfae74779c5a", "reflection_audit.py": "6761fb01f93ef89f2455388b2f5a71f19c0bbd870e6aaeba457ede0a949a163b", "replayed_producer.py": "99c1e3694ae06a7ce7a370b04ecb45ea3fcfe69a6e6e7f4c4606e0a6c74c3184", - "test_controls.py": "87dbc9945a5057cf1b7b6ba776590f5c20548f5b2b63893b34bd6280f534f036", - "verify.py": "b49c45f0fa06ab7de987110f3756c445220e1b2e08127cfa891eca7330e6d8da" + "terminal-elision-audit.json": "976d0f873521142a1e1ccacd06357daafb350232690a56191932cd647acc2c0d", + "terminal-elision.json.gz": "2c199d3df56bdeedf0832a23ddf1dea1330724182378c67188aead06c53a0d9b", + "terminal-selection.json": "96ca9b7a465041aa333149a9695bce1b392616279b16effa66ebee11bd91306b", + "terminal_elision.py": "f1113d3a1e6bd2fc3cd906a24db9c9d8ccff17c548de6096e556284684ac0d4b", + "terminal_elision_audit.py": "0c19cbc0389c4a668a22561ee4529472022e2e0819783e36e488c5043068f540", + "test_controls.py": "41b8de5feb8620fb6eb3964f800a8039c4ce409ef28f067e3d1aae083dad9a07", + "verify.py": "867b9314427fa33549d6f78daae0fa05ea6c8f1dd1342b2d73f9fc7945e4f1a3" }, "provenance": { "base": "https://github.com/CrocSwap/integer-mult-bounds/pull/110", @@ -36,6 +44,14 @@ "file": "inputs/complex-dag.json.gz", "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/117", "sha256": "3c034d0aae388ef567a454826f4f48b26fd8a94c71e8ffed4835271b349a783b" + }, + "shrunk_frame_parent": { + "commit": "dda535bdcfc321a13a1ebd3c2d70e2b5bb72368e", + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/125" + }, + "terminal_elision": { + "commit": "b1a6f24e57141637b3ff040d6f2ce9d896ffb9bb", + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/122" } }, "reflection": { @@ -64,6 +80,6 @@ "scripts/shared_point_network.py": "a85e7f0d8c42d6a27e3846308571ca324a1824ac5c2d59e4daa5c7673c33c697", "scripts/structured_bulk_assembly.py": "e99467e14211fba699878ed036e1e2362eb8e395dc22f9ecdcecc7fbf2cc736d" }, - "schema": 1, - "scope": "Frozen finite producer, profiles, exact assembly and reflection audit; inherited all-size transfer remains conditional." + "schema": 2, + "scope": "Frozen finite terminal-elided producer, profiles, exact assembly, parent reflection and independent terminal audit; inherited all-size transfer remains conditional." } diff --git a/research/shrunk-frames/certificate.json b/research/shrunk-frames/certificate.json index 6e0a5f02d1..e05112a0d5 100644 --- a/research/shrunk-frames/certificate.json +++ b/research/shrunk-frames/certificate.json @@ -1,92 +1,92 @@ { "actual_bit_saving": "1240189553/10000000000000", "assembly": { - "absorption_gap": "1423799823581924404745614798375593/2500553080248572986091654124313081000000000000000", + "absorption_gap": "557032412576896498489298147183996879/625138625140352841779654201806778107000000000000000", "margins": { - "Gaussian_arithmetic": "331855646931470668996733908345875686919/2000442464198858388873323299450464800000000", - "bulk_exposure": "55308025686919/500000000000000000", - "compact_phase_layer": "276540120138391202270175686919/2500553080248572986091654124313081", - "coordinate_movement": "55308025686919/500000000000000000", - "dimension": "2499999975000000000000000000000000/2500553080248572986091654124313081", - "original_prefix": "27656512566919368800003660346024313081/250055308024857298609165412431308100000000", - "scalar_work": "442481698305308624750313358810675686919/2000442464198858388873323299450464800000000" + "Gaussian_arithmetic": "83176958657204508460531060345798193221893/500110900112282273423723361445422485600000000", + "bulk_exposure": "13862514243221893/125000000000000000000", + "compact_phase_layer": "69312569136732342379230293221893/625138625140352841779654201806778107", + "coordinate_movement": "13862514243221893/125000000000000000000", + "dimension": "624999993750000000000000000000000000/625138625140352841779654201806778107", + "original_prefix": "6931882052298374590764808976391106778107/62513862514035284177965420180677810700000000", + "scalar_work": "110904487143648283370519665768283793221893/500110900112282273423723361445422485600000000" }, - "minimum_margin": "276540120138391202270175686919/2500553080248572986091654124313081", + "minimum_margin": "69312569136732342379230293221893/625138625140352841779654201806778107", "parameters": { - "C0": 3646615615709474302231996852324339320426087077316912790823030645920872744002225026973564928, + "C0": 3426040043121653543815319427886146346182658660878546938204156655506654200461993667857481728, "C1": 1, - "a_bit": "55308025686919/500000000000000000", - "a_complex": "55308081/500000000000", - "alpha_squared_power": "414822684355688646962150000000/2500553080248572986091654124313081", + "a_bit": "13862514243221893/125000000000000000000", + "a_complex": "13862528107/125000000000000", + "alpha_squared_power": "103971979744787061016716050000000/625138625140352841779654201806778107", "beta": "1/1000000", - "c": "276540125669193660346024313081/2500000000000000000000000000000000", + "c": "69312570522983738976391106778107/625000000000000000000000000000000000", "delta": "1/800000000", - "epsilon": "2499999975000000000000000000000000/2500553080248572986091654124313081", + "epsilon": "624999993750000000000000000000000000/625138625140352841779654201806778107", "eta": "1/100000000", - "kappa": "110591581647/1000000000000000", - "lambda_": "49994469197486616125686919/50000000000000000000000000", - "lambda_prime": "24997234598770962075686919/25000000000000000000000000", - "q": "2765401229037924313081/25000000000000000000000000", - "sigma": "499944691919/500000000000", - "tau": "499944691974313081/500000000000000000" + "kappa": "110875518403/1000000000000000", + "lambda_": "12498613748589540324943221893/12500000000000000000000000000", + "lambda_prime": "6249306874301701419593221893/6250000000000000000000000000", + "q": "693125698298580406778107/6250000000000000000000000000", + "sigma": "124986137471893/125000000000000", + "tau": "124986137485756778107/125000000000000000000" }, "recurrence": { - "internal": "499944691974313081/500000000000000000", - "leaf": "499944691974308081/500000000000000000", - "reservations": "2499723459874330806339653975686919/2500000000000000000000000000000000" + "internal": "124986137485756778107/125000000000000000000", + "leaf": "124986137485755528107/125000000000000000000", + "reservations": "624930687429477016261023608893221893/625000000000000000000000000000000000" }, "strict_constraints": { - "Gaussian_arithmetic_above_kappa": "138279438527370933799323622918090223447125593/2500553080248572986091654124313081000000000000000", - "K_dominates_log": "27654012290379240365408770962075686919/250055308024857298609165412431308100000000", - "K_geometry": "27656512566919368800003660346024313081/250055308024857298609165412431308100000000", - "alpha_below_one": "2500138257564217297444691974313081/2500553080248572986091654124313081", - "alpha_below_one_fourth": "2498893789511150231503805524313081/10002212320994291944366616497252324", - "alpha_positive": "414822684355688646962150000000/2500553080248572986091654124313081", - "artificial_boundary": "14003650357141687868693766988962529075686919/2000442464198858388873323299450464800000000", + "Gaussian_arithmetic_above_kappa": "34658629185330325609010428708844039674550246879/625138625140352841779654201806778107000000000000000", + "K_dominates_log": "6931256982985803374655371701419593221893/62513862514035284177965420180677810700000000", + "K_geometry": "6931882052298374590764808976391106778107/62513862514035284177965420180677810700000000", + "alpha_below_one": "625034653160608054718637485756778107/625138625140352841779654201806778107", + "alpha_below_one_fourth": "624722737221373693535587337606778107/2500554500561411367118616807227112428", + "alpha_positive": "103971979744787061016716050000000/625138625140352841779654201806778107", + "artificial_boundary": "3500914932801606006024344038389148168593221893/500110900112282273423723361445422485600000000", "beta_below_one": "999999/1000000", "beta_positive": "1/1000000", - "bit_positive": "55308025686919/500000000000000000", - "bulk_exposure_above_kappa": "12234863419/500000000000000000", - "c_below_one": "2499723459874330806339653975686919/2500000000000000000000000000000000", - "c_positive": "276540125669193660346024313081/2500000000000000000000000000000000", - "cell_above_band": "2499861692435782702555308025686919/5001106160497145972183308248626162", - "compact_leaf": "55558025686919/25000000000000000000000000", - "compact_phase_layer_above_kappa": "1423799823581924404745614798375593/2500553080248572986091654124313081000000000000000", - "compact_reservations": "2765401229037924313081/2500000000000000000000000000000000", - "complex_above_bit": "55313081/500000000000000000", - "complex_below_one_over32": "15569691919/500000000000", - "coordinate_movement_above_kappa": "12234863419/500000000000000000", + "bit_positive": "13862514243221893/125000000000000000000", + "bulk_exposure_above_kappa": "3074442846893/125000000000000000000", + "c_below_one": "624930687429477016261023608893221893/625000000000000000000000000000000000", + "c_positive": "69312570522983738976391106778107/625000000000000000000000000000000000", + "cell_above_band": "624965334339391945281362514243221893/1250277250280705683559308403613556214", + "compact_leaf": "13925014243221893/6250000000000000000000000000", + "compact_phase_layer_above_kappa": "557032412576896498489298147183996879/625138625140352841779654201806778107000000000000000", + "compact_reservations": "693125698298580406778107/625000000000000000000000000000000000", + "complex_above_bit": "13863778107/125000000000000000000", + "complex_below_one_over32": "3892387471893/125000000000000", + "coordinate_movement_above_kappa": "3074442846893/125000000000000000000", "delta_below_one_eighth": "99999999/800000000", "delta_positive": "1/800000000", - "dimension_above_kappa": "2499723434879863032597553406237485745614798375593/2500553080248572986091654124313081000000000000000", - "epsilon_below_one": "553105248572986091654124313081/2500553080248572986091654124313081", - "epsilon_positive": "2499999975000000000000000000000000/2500553080248572986091654124313081", - "gamma_sublinear": "138282564217297444691974313081/2500553080248572986091654124313081", - "guard_width": "553105248572986091654124313081/2500553080248572986091654124313081", - "lambda_above_internal": "55308025686919/50000000000000000000000000", - "lambda_above_sigma": "5586616125686919/50000000000000000000000000", - "lambda_above_tau": "55308025686919/50000000000000000000000000", - "lambda_prime_above_lambda": "55308025686919/50000000000000000000000000", - "lambda_prime_below_one": "2765401229037924313081/25000000000000000000000000", + "dimension_above_kappa": "624930681180863824690033346603276596298147183996879/625138625140352841779654201806778107000000000000000", + "epsilon_below_one": "138631390352841779654201806778107/625138625140352841779654201806778107", + "epsilon_positive": "624999993750000000000000000000000000/625138625140352841779654201806778107", + "gamma_sublinear": "34659410608054718637485756778107/625138625140352841779654201806778107", + "guard_width": "138631390352841779654201806778107/625138625140352841779654201806778107", + "lambda_above_internal": "13862514243221893/12500000000000000000000000000", + "lambda_above_sigma": "1400240324943221893/12500000000000000000000000000", + "lambda_above_tau": "13862514243221893/12500000000000000000000000000", + "lambda_prime_above_lambda": "13862514243221893/12500000000000000000000000000", + "lambda_prime_below_one": "693125698298580406778107/6250000000000000000000000000", "leaf_saving_above_bit": "1/100000000000000", - "literal_scalar_guard": "14065616197378741718443193606139245678291196", - "original_prefix_above_kappa": "25005532226285553442840945988745608375593/2500553080248572986091654124313081000000000000000", - "phase_boundary": "331855646931470668996733908345875686919/2000442464198858388873323299450464800000000", - "phase_local": "442481698305308624750313358810675686919/2000442464198858388873323299450464800000000", - "prime_interval_packing": "553105248572986091654124313081/2500553080248572986091654124313081", - "q_below_internal": "55308025686919/25000000000000000000000000", - "q_below_leaf": "55558025686919/25000000000000000000000000", - "q_below_reservations": "2765401229037924313081/2500000000000000000000000000000000", - "q_positive": "2765401229037924313081/25000000000000000000000000", - "record_suffix": "553105248572986091654124313081/2500553080248572986091654124313081", + "literal_scalar_guard": "13633582372644121063429594327546009455025980", + "original_prefix_above_kappa": "6251386808435940994693040507365928253996879/625138625140352841779654201806778107000000000000000", + "phase_boundary": "83176958657204508460531060345798193221893/500110900112282273423723361445422485600000000", + "phase_local": "110904487143648283370519665768283793221893/500110900112282273423723361445422485600000000", + "prime_interval_packing": "138631390352841779654201806778107/625138625140352841779654201806778107", + "q_below_internal": "13862514243221893/6250000000000000000000000000", + "q_below_leaf": "13925014243221893/6250000000000000000000000000", + "q_below_reservations": "693125698298580406778107/625000000000000000000000000000000000", + "q_positive": "693125698298580406778107/6250000000000000000000000000", + "record_suffix": "138631390352841779654201806778107/625138625140352841779654201806778107", "row_product_gap": "6389/25", - "scalar_work_above_kappa": "276562002744668378491297935999090223447125593/2500553080248572986091654124313081000000000000000", - "short_record_fallback": "1249861686846006107497739648634368046048805957712561/1250276540124286493045827062156540500000000000000000", - "small_field_exposure": "276565128434594889383948626162/2500553080248572986091654124313081" + "scalar_work_above_kappa": "69318039793385044246496185486951039674550246879/625138625140352841779654201806778107000000000000000", + "short_record_fallback": "78116333225655003706971835749846717729347970410584503449/78142328142544105222456775225847263375000000000000000000", + "small_field_exposure": "69318821216109437274971513556214/625138625140352841779654201806778107" } }, "bit_moment_gap": "210811394225115117568018038513239592855337768061996351784199300828041381607148420475711921673436778332750996651783152394205578153858435663243959795913385215868392831844509655226993164072062830500832781615792327068936897853818968534771730481866850519439187068953062899333771640996075361901014500735179763112430083120460814689994116646689670445286414265265018468311435502209195246240538069975559360544007937885404793780372701951022292660282948582656517071290400479729799954952580125532795274568021525151839594883237275569314958070368193662075730567130277424969924134425921633872848924585639423998410253779062359718371205767101510073996880454144801457072151080008705648366603197414406872289670642046369219405455128737300640897667220951127018547660455087533581513233999285275099394371781290865408274484542745086391849285198194905751058992419590161634431610100995441112613134240446609058758039909343152776920263419910572835208525277494067408376961456317/225678505065634612156474913616400633538202019254665477026878220214422133931127460164253533068001699469116755578965090566731480236912032281717920888140691998261537790258547549397061712443744511202265657747547567084090291301783866427704803156891369853685579999500594559805069402727752752227038426964007028952158078563045054314475625278140097385695241851533235641996467089273692960018822280793234080014352234618229252999217015923728814468917104222554059646947960375336061268431587018084270516494408656203498548153054913267707164839939006583338918817922618882667407408888179421052689449193499742148706302504238261936554897181289081072466758282367100305194479622149878636307463869297507337915811001244472279386614413535081936912313821531543735588465392499062010570720287729070905437080967709221039366272598541269000920375996285867953823816142239661027100714288630069735295241672325865922423925213948613346461034734632365263739073012128769510020000000000000000000000", - "bit_parameter": "55308025686919/500000000000000000", + "bit_parameter": "13862514243221893/125000000000000000000", "bit_profile": { "L": 1792252, "N": 3136441, @@ -157,49 +157,49 @@ "v": 1771 }, "coarse_bit_saving": "620523/5000000000", - "complex_moment_gap": "1120907676991709375587467571083583613675514323107449210881795156623730476679332908369675633828609828547699408013724966704466999362228476322550536073425477865821903781068608934724652434185915105821476280707835554190305969731534431792034136981242275885510306743073208513584546756206129639721309235360276551243600523744884826937176020214328142317214679396773991230268354778844685206549974861397955820231211808000505289181911024758652777589422017126655483564105414184271982303920191622773958369915731889103228404461797825046990910884342895126883154008667367948162387895233712466670165382398728821416470882760327554020327490396551350392371803758571065760737832618462497790815846731507580694898835979742744618260624366037437075808017877875989728828939538013318978980990915921668227049349635290036175560530633279260473351540544135441376709651695874126570388867012660974313806428810883182335167580007/5729785626482475083453880928912868090199891077894328437390154678085907947787777170551065795053175425295499005277150151786860288788040509249164976675728598633831731259082317118043077983924941216272575857128488188317581360310229902663321454526224581674689575437986461381738691709567461275868099475629801004180206074232907215575028613840139675146224247781180470831210120187095639606203370194019694000363186599456926657406240962080920816408153979237758439565211054622374231622886675112863813346734480202775285744822553219180447792108305361254841580710053360069403264180909982005303238389319538012371475060400462749261716035566070509613844095475111408101447019396632121482203883977202704954856015697825135147677429303783554053341478566944596465856275121302108324962996326877399164307498504419646510163732515012385754160928876728348713015505212385798910883039803748837277174939722238502400000000000000000000000", + "complex_moment_gap": "343272080630150061189318554879278970429390461960207452888261102284395992147112214104981691964642847817662879194895425627595540850146383403451025535105998480397343974698971244140511723022405117701236953066586795544133059823517982486828291217097437122775065789911353551923443644554260399558519091019382631557268856449798721505946102590641947223236837091431432637193891149393584519407186819218142377524272785517778411966162979721057314220987546244137031446591675175716041817314010973898353083548874331992542639637086729775614136853138671789145795646689610670173639742110813694106279946410956614245558993424410020478380701924104934123018785430406941083460859260138145646374695961893752386818710913309273345900716078178823853705584027817412725136580175957920677369492034343982607681889908744614556512102766805713935321159313394869815570197279209055695754843000950448512194074525732880346134457391550946822990145861114265757196100752224520725544484017126377905420734572846280927230005198689051222513/17439433657404011074662187660744069797624553118500204281557364814356620735850705512640080619576829469814105515501244532067397351389856605459127863094857335395667145595552012665882486097968043144705966337990892032064205766373561352755916316614926173447276353382252898934529584974823242311875359545118942641640403022138971839899233999861276878201442028864490675925354197338399023495631110944132315483025485479775232284712403188211178924680208139588440493601654068635257608862896533015068627740031559156485844596970211846608109574309301722055551935098159093575001959416174483127056399684350349744198268480225651129147980439477758926364194765127813475155804119186108461925620535725728369250091719362578459239438281177320746439728540552587511512762252190210082112221102554499300393854418730651063476707314283494479444669689828910833583045849557483500963189603912096956194275741810416959473087530926174334113825204187291825602374845853959808312040020395414628051315433743325044045752463168000000000000000000000000000", "complex_profile": { "L": 2234496, "N": 4096576, - "R": 28705, - "W": 124390992, + "R": 28324, + "W": 122848704, "additions": 91770, "child_multiplicities": { - "1": 435601232, + "1": 433937504, "10": 7375456, "11": 7019232, "12": 31788944, "13": 12536656, "14": 1497760, - "15": 3440800, + "15": 3428656, "16": 854128, "17": 506000, "18": 2906464, "19": 2092816, - "2": 267192288, + "2": 267176096, "20": 817696, "21": 1230592, "22": 64768, "23": 8363168, - "3": 29238704, - "4": 61145040, - "5": 26425344, + "3": 28506016, + "4": 60554032, + "5": 26356528, "529": 8193152, "552": 97147952, "554": 3493424, "556": 1445136, "558": 2319504, - "560": 582912, + "560": 570768, "562": 101200, "564": 1307504, "566": 975568, "568": 1364176, "569": 4048, - "570": 3643200, - "571": 2444992, - "572": 837936, - "573": 44528, - "574": 485760, + "570": 3574384, + "571": 1853984, + "572": 105248, + "573": 28336, + "574": 364320, "6": 15734576, "7": 11876832, "8": 22077792, @@ -211,17 +211,17 @@ "14": 241, "16": 337, "17": 1, - "18": 900, - "19": 604, + "18": 883, + "19": 458, "2": 863, - "20": 207, - "21": 11, - "22": 120, + "20": 26, + "21": 7, + "22": 90, "4": 357, "6": 573, - "8": 144 + "8": 141 }, - "deferred_roles": 4706, + "deferred_roles": 4325, "deficit": 1862080, "h": 24, "lifted_additions": 24792, @@ -230,6 +230,7 @@ "maxchild": 574, "phase_one_ops": 18844, "phase_one_roles": 13555, + "pre_elimination_R": 28705, "replay": { "field": "Z/(2^61-1)", "scratch_restored": true, @@ -239,11 +240,14 @@ ], "y_plus_x": true }, + "role_count_scope": "Terminal-elided physical word; additions + roots - links is pre-elimination.", "roots": 8120, - "total_rank": 71647349312, + "terminal_direct_updates": 1167, + "terminal_elimination_count": 381, + "total_rank": 70758991424, "v": 2024 }, - "complex_saving": "55308081/500000000000", + "complex_saving": "13862528107/125000000000000", "finite_bridge": { "bit_coarse": { "W": 108516254, @@ -253,31 +257,33 @@ "wire_bits": 27 }, "complex": { - "W": 124390992, + "W": 122848704, "halving_degree": 200, "m": 576, "maxchild": 574, - "s": 71647349312, - "scalar_group_upper": 60347419084480, + "s": 70758991424, + "scalar_group_upper": 59723114017600, "scalar_terms": [ { - "R": 28705, + "R": 28324, "c": 91770, - "description": "Expanded deferred readouts and forward/inverse/reflected words", + "description": "Expanded deferred readouts, source-time terminal redirects, and forward/inverse/reflected words", "h": 24, "invocations": 2024, - "local_group_upper": 14907958248, + "local_group_upper": 14753732688, "q": 8120, + "terminal_direct_updates": 1167, "v": 2024 }, { - "R": 28705, + "R": 28324, "c": 91770, - "description": "Expanded deferred readouts and forward/inverse/reflected words", + "description": "Expanded deferred readouts, source-time terminal redirects, and forward/inverse/reflected words", "h": 24, "invocations": 2024, - "local_group_upper": 14907958248, + "local_group_upper": 14753732688, "q": 8120, + "terminal_direct_updates": 1167, "v": 2024 } ], @@ -292,18 +298,18 @@ "suffix_slope": 128000 }, "semantic": { - "B": 14065616197380609244023681038811612751070848, - "C0": 3646615615709474302231996852324339320426087077316912790823030645920872744002225026973564928, + "B": 13633582372645923722500537180244156907845248, + "C0": 3426040043121653543815319427886146346182658660878546938204156655506654200461993667857481728, "C1": 1, - "E": 14065616197380609244023681038811541103721536, + "E": 13633582372645923722500537180244086148853824, "exact_grid": "2^(-P)*21^(-K), K=G*(D_complex+1); completed children preserve incoming odd denominator; no child rounding", "fixed_odd_divisor": 21, - "induction_gap": 42196848592141827732071043116434838253212544, - "literal_charge": 1867525580487432672295425430340, - "strict_literal_gap": 14065616197378741718443193606139245678291196 + "induction_gap": 40900747117937771167501611540732470723535744, + "literal_charge": 1802659070942852698076693827844, + "strict_literal_gap": 13633582372644121063429594327546009455025980 } }, - "kappa": "110591581647/1000000000000000", + "kappa": "110875518403/1000000000000000", "next_grid_rejections": { "bit": "1e-10", "complex": "1e-12", diff --git a/research/shrunk-frames/certificate.py b/research/shrunk-frames/certificate.py index 5e00159bfe..a6b213ebb7 100644 --- a/research/shrunk-frames/certificate.py +++ b/research/shrunk-frames/certificate.py @@ -21,7 +21,7 @@ OLD = Q(384599, 10**10) BETA = Q(1, 10**6) COARSE = Q(620523, 5000000000) -COMPLEX = Q(110616162, 10**12) +COMPLEX = Q(13862528107, 125000000000000) KGRID = 10**15 def profile(name): @@ -59,7 +59,8 @@ def exact(bit=None, phase=None): # coefficients; <=4*v*(h+1) scalar groups suffice per readout. A factor # eight covers forward/inverse words, both reflected words, and copies. h,v,R,q,c = (phase[k] for k in ('h','v','R','roots','additions')) - local = 8*(c+2*R+(R+q)*v*(h+1)+h*h+h+1) + terminal_direct_updates = phase.get('terminal_direct_updates', 0) + local = 8*(c+2*R+(R+q)*v*(h+1)+h*h+h+1+terminal_direct_updates) G = phase['N'] + 2*v*local m,W,s = (phase[k] for k in ('m','W','total_rank')) E=64*(W+m+G+1)**3 @@ -68,7 +69,8 @@ def exact(bit=None, phase=None): assert charge= s+E and 2*B+18> pivot & 1: + vector ^= pivots[pivot] + if vector: + pivot = vector.bit_length() - 1 + for old in pivots: + if pivots[old] >> pivot & 1: + pivots[old] ^= vector + pivots[pivot] = vector + return tuple(pivots[p] for p in sorted(pivots, reverse=True)) + + +def contains(frame, larger): + larger = basis(larger) + return len(basis(tuple(frame) + larger)) == len(larger) + + +def parent_word_from_capture(d): + """Serialize the captured parent state in the terminal audit convention. + + Ordinary adjoints are stored as signed numerators over 42. Center vectors + remain unscaled; their scatter rows carry the denominator 42. + """ + h, v, roles = d['h'], d['v'], d['Rr'] + scale = 42 + word = dict( + h=h, v=v, R=roles, q=d['q'], args=d['args'], roots=d['roots'], + ops=d['ops'], frames={str(n): d['U'][n] for n in d['U']}, + sigma={str(s): d['placed'][s] for s in d['placed']}, + role_root={str(s): j for s, j in d['role_root'].items()}, + leaf_of={str(s): leaf for s, leaf in d['leaf_of'].items()}, + first_node=d['first_node'], target=d['target'], kind=list(d['kind']), + adjoint_centre={str(s): d['cvec'][s] for s in range(roles)}, + adjoint_ordinary={str(s): {str(t): (scale * c) % P for t, c in d['dpart'][s].items()} + for s in range(roles)}, + reach={str(s): sorted(d['reach'][s]) for s in range(roles)}, + phase_one=d['phase1'], deferred=d['deferred'], chain_dims=d['chain_dims'], + root_frames={str(s): d['root_frame'][s] for s in d['root_frame']}, + centre_of={str(j): i for j, i in d['centre_of'].items()}, + trip=[list(t) for t in d['trip']]) + return word + + +def canonical_word_bytes(word): + def json_default(value): + if hasattr(value, 'tolist'): + return value.tolist() + if isinstance(value, set): + return sorted(value) + raise TypeError('Unsupported captured value: ' + type(value).__name__) + payload = json.dumps(word, separators=(',', ':'), default=json_default).encode() + return gzip.compress(payload, mtime=0) + + +def normalize_word(word): + """Accept either the compact list or keyed-map export convention.""" + for name in ('frames', 'sigma', 'role_root', 'leaf_of', 'adjoint_centre', + 'adjoint_ordinary', 'reach', 'root_frames', 'centre_of'): + value = word[name] + if isinstance(value, list): + word[name] = {str(i): row for i, row in enumerate(value)} + return word + + +def inventory(word): + h, v, roles = word['h'], word['v'], word['R'] + frames = {int(k): v for k, v in word['frames'].items()} + sigma = {int(k): v for k, v in word['sigma'].items()} + roots = {int(k): v for k, v in word['role_root'].items()} + leaves = {int(k): v for k, v in word['leaf_of'].items()} + centre = {int(k): v for k, v in word['adjoint_centre'].items()} + ordinary = {int(k): {int(t): (c if c <= P // 2 else c - P) for t, c in row.items()} + for k, row in word['adjoint_ordinary'].items()} + destinations, sources = Counter(), Counter() + gate_frames = [[] for _ in range(roles)] + for op in word['ops']: + if op[0] == 'add': + dst, src = op[1], op[2] + elif op[0] == 'copy': + src, dst = op[1], op[2] + else: + continue + destinations[dst] += 1 + sources[src] += 1 + gate_frames[dst].append(frames[op[3]]) + + target_frames = [[] for _ in range(v)] + for s in word['deferred']: + for t in word['reach'][str(s)]: + target_frames[t].append(sigma[s]) + candidates, blocked = [], Counter() + for s in range(roles): + if s not in roots or word['kind'][roots[s]] or sources[s]: + continue + if s not in sigma: + blocked['not_deferred'] += 1 + continue + j = roots[s] + t = word['target'][j] + expected = {t: 21 if j < v else -21} + if centre[s] is not None or ordinary[s] != expected: + blocked['nonterminal_adjoint'] += 1 + continue + updates = ([frames[word['first_node'][s]]] if s in leaves else []) + gate_frames[s] + if not updates: + blocked['no_updates'] += 1 + continue + if any(not contains(old, update) for old in target_frames[t] for update in updates): + blocked['target_past_update_frame'] += 1 + continue + candidates.append(s) + + # Check the whole target schedule before deleting any role. Every target + # starts with its old deferred-readout frames, then grows at source times. + current = [[] for _ in range(v)] + by_target = defaultdict(list) + for s in candidates: + j = roots[s] + t = word['target'][j] + if s in leaves: + by_target[t].append((-1, s, frames[word['first_node'][s]])) + phase_one = set(word['phase_one']) + for i, op in enumerate(word['ops']): + if op[0] == 'add': + dst = op[1] + elif op[0] == 'copy': + dst = op[2] + else: + continue + if dst in candidates: + need(i not in phase_one, 'terminal update crosses the center phase') + by_target[word['target'][roots[dst]]].append((i, dst, frames[op[3]])) + for s in word['deferred']: + for t in word['reach'][str(s)]: + need(contains(current[t], sigma[s]), 'parent target-frame reversal') + current[t] = sigma[s] + accepted, rejected, targets = set(), set(), {} + for t, rows in by_target.items(): + rows.sort(key=lambda row: (row[0], row[1])) + chain = [current[t]] + [row[2] for row in rows] + nested = all(contains(a, b) for a, b in zip(chain, chain[1:])) + role_ids = {row[1] for row in rows} + (accepted if nested else rejected).update(role_ids) + targets[t] = dict(roles=sorted(role_ids), nested=nested, + frame_dimensions=[len(basis(f)) for f in chain], + event_indices=[row[0] for row in rows]) + need(set(candidates) == accepted | rejected, 'incomplete target schedule') + return dict(candidates=sorted(candidates), accepted=sorted(accepted), + rejected=sorted(rejected), terminal_blocked=dict(blocked), + target_count=len(by_target), targets=targets) + + +def build(word, parent_profile, parent_word_sha256=None): + """Build the terminal-elided profile and a complete chronological receipt.""" + need(not sys.flags.optimize, 'Assertions required') + selection = inventory(word) + removed = set(selection['accepted']) + need(removed and not selection['rejected'], 'simultaneous target chain is not nested') + # The candidate set is frozen against the pinned #125 parent. A changed + # parent must be re-screened instead of silently changing the submission. + need(len(removed) == 381 and selection['target_count'] == 381, + 'terminal inventory differs from the screened PR #125 candidate') + + h, v, roles = word['h'], word['v'], word['R'] + m = h * h + frames = {int(k): v for k, v in word['frames'].items()} + sigma = {int(k): v for k, v in word['sigma'].items()} + roots = {int(k): v for k, v in word['role_root'].items()} + leaves = {int(k): v for k, v in word['leaf_of'].items()} + root_frames = {int(k): v for k, v in word['root_frames'].items()} + phase_one = set(word['phase_one']) + deferred = set(word['deferred']) + active = [s for s in range(roles) if s not in removed] + + events, current = [], [[] for _ in range(v)] + target_paths = [[[]] for _ in range(v)] + + def front(target, frame, why): + need(contains(current[target], frame), 'target frame reversal') + if basis(current[target]) != basis(frame): + events.append(['target_front', target, frame, why]) + target_paths[target].append(frame) + current[target] = frame + + def redirect(role, source, frame, index, data=False): + root = roots[role] + target = word['target'][root] + coefficient = 21 if root < v else -21 + front(target, frame, ['redirect', index, role]) + events.append(['direct_input' if data else 'direct_aux', target, + source, coefficient, frame, index, role]) + + def gate(index, inverse=False): + op = word['ops'][index] + if op[0] == 'src': + return + dst, src = ((op[1], op[2]) if op[0] == 'add' + else (op[2], op[1])) + need(src not in removed, 'terminal role is used as a control') + if dst in removed: + need(index not in phase_one, 'terminal redirect crosses the center phase') + if not inverse: + redirect(dst, src, frames[op[3]], index) + else: + events.append(['gate', index, -1 if inverse else 1]) + + for role in active: + if role not in deferred: + events.append(['readout', role, -1, False, 'initial']) + for role, leaf in leaves.items(): + if role not in deferred: + need(role not in removed, 'nondeferred leaf role was deleted') + events.append(['input', role, leaf, 1]) + for index in word['phase_one']: + gate(index) + for role, root in roots.items(): + if word['kind'][root]: + need(role not in removed, 'center role was deleted') + events.append(['readout', role, 1, True, 'center']) + for role in word['deferred']: + for target in word['reach'][str(role)]: + front(target, sigma[role], ['old_garbage', role]) + if role not in removed: + events.append(['readout', role, -1, False, 'deferred']) + for role in word['deferred']: + if role in leaves: + if role in removed: + redirect(role, leaves[role], frames[word['first_node'][role]], -1, True) + else: + events.append(['input', role, leaves[role], 1]) + for index in range(len(word['ops'])): + if index not in phase_one: + gate(index) + for role, root in roots.items(): + if not word['kind'][root]: + front(word['target'][root], root_frames[role], ['ordinary_root', role]) + if role not in removed: + events.append(['readout', role, 1, True, 'ordinary']) + for index in reversed(range(len(word['ops']))): + gate(index, True) + for role, leaf in leaves.items(): + if role not in removed: + events.append(['input', role, leaf, -1]) + need(all(len(basis(frame)) == h - 1 for frame in current), + 'terminal target frames') + + # Reprice the removed auxiliary chains and replace the old target fronts. + old_target, new_target, deleted = Counter(), Counter(), Counter() + levels = [{0, h - 1} for _ in range(v)] + for role in word['deferred']: + for target in word['reach'][str(role)]: + levels[target].add(len(basis(sigma[role]))) + for dimensions in levels: + for low, high in zip(sorted(dimensions), sorted(dimensions)[1:]): + old_target[high - low] += 2 * v + for path in target_paths: + dims = [len(basis(frame)) for frame in path] + for low, high in zip(dims, dims[1:]): + if high > low: + new_target[high - low] += 2 * v + for role in removed: + dimensions = word['chain_dims'][role] + for low, high in zip(dimensions[:-1], dimensions[1:-1]): + if high > low: + deleted[high - low] += 2 * v + deleted[h - dimensions[-2]] += 2 * v + deleted[m - h + dimensions[0]] += 2 * v + deleted.pop(0, None) + need(sum(width * count for width, count in deleted.items()) == + 2 * v * len(removed) * m, 'deleted role rank mass') + histogram = Counter({int(t): c for t, c in parent_profile['child_multiplicities'].items()}) + histogram.subtract(deleted) + histogram.subtract(old_target) + histogram.update(new_target) + need(all(count >= 0 for count in histogram.values()), 'negative child multiplicity') + histogram = Counter({width: count for width, count in histogram.items() if count}) + new_roles = roles - len(removed) + new_width = 2 * v * v + 2 * v * new_roles + rank_mass = sum(width * count for width, count in histogram.items()) + need(new_width * m - rank_mass == parent_profile['deficit'], + 'complete deficit changed') + direct_updates = sum(event[0] in ('direct_aux', 'direct_input') for event in events) + profile = dict(parent_profile) + profile.update( + pre_elimination_R=roles, R=new_roles, W=new_width, total_rank=rank_mass, + terminal_elimination_count=len(removed), terminal_direct_updates=direct_updates, + child_multiplicities=dict(sorted(histogram.items())), maxchild=max(histogram), + deferred_roles=parent_profile['deferred_roles'] - len(removed), + role_count_scope='Terminal-elided physical word; additions + roots - links is pre-elimination.') + dimensions = Counter({int(k): value for k, value in parent_profile['deferred_dims'].items()}) + for role in removed: + dimensions[len(basis(sigma[role]))] -= 1 + profile['deferred_dims'] = {k: value for k, value in sorted(dimensions.items()) if value} + + receipt = dict( + parent_word_sha256=parent_word_sha256, + removed=sorted(removed), active_roles=active, events=events, + target_paths=target_paths, + deleted_child_multiplicities=dict(sorted(deleted.items())), + old_target_histogram=dict(sorted(old_target.items())), + new_target_histogram=dict(sorted(new_target.items())), + target_delta={width: new_target[width] - old_target[width] + for width in sorted(old_target.keys() | new_target.keys()) + if new_target[width] != old_target[width]}) + replay(word, receipt, removed) + return profile, receipt, selection + + +def replay(word, receipt, removed): + events = receipt['events'] + h, v, roles = word['h'], word['v'], word['R'] + roots = {int(s): j for s, j in word['role_root'].items()} + leaves = {int(s): j for s, j in word['leaf_of'].items()} + operations = word['ops'] + active = receipt['active_roles'] + inv42 = pow(42, P - 2, P) + triples = list(combinations(range(h), 3)) + scatter = [[2 - 21 * (i in triple) for triple in triples] for i in range(h)] + + def run(seed): + rng = random.Random(seed) + x = [rng.randrange(P) for _ in range(v)] + scratch = {s: rng.randrange(P) for s in active} + aux = dict(scratch) + y0 = [rng.randrange(P) for _ in range(v)] + y = list(y0) + pending_centres = [0] * h + + def read(role, sign, seeded): + if seeded: + root = roots[role] + if word['kind'][root]: + centre = int(word['centre_of'][str(root)]) + centre_row = [int(i == centre) for i in range(h)] + ordinary_row = {} + else: + centre_row = None + target = word['target'][root] + ordinary_row = {target: 21 if root < v else -21} + else: + centre_row = word['adjoint_centre'][str(role)] + ordinary_row = {int(t): c for t, c in word['adjoint_ordinary'][str(role)].items()} + value = sign * aux[role] * inv42 % P + if centre_row is not None: + for i, coefficient in enumerate(centre_row): + if coefficient: + pending_centres[i] = (pending_centres[i] + coefficient * value) % P + for target, coefficient in ordinary_row.items(): + y[target] = (y[target] + coefficient * value) % P + + for event in events: + mode = event[0] + if mode == 'target_front': + continue + if mode == 'input': + _, role, leaf, sign = event + aux[role] = (aux[role] + sign * x[leaf - 1]) % P + elif mode == 'gate': + _, index, sign = event + op = operations[index] + dst, src = (op[1], op[2]) if op[0] == 'add' else (op[2], op[1]) + aux[dst] = (aux[dst] + sign * aux[src]) % P + elif mode == 'readout': + _, role, sign, seeded, _tag = event + read(role, sign, seeded) + elif mode in ('direct_aux', 'direct_input'): + _, target, source, numerator = event[:4] + value = aux[source] if mode == 'direct_aux' else x[source - 1] + y[target] = (y[target] + numerator * inv42 * value) % P + else: + raise ValueError('unknown event: ' + mode) + for i, value in enumerate(pending_centres): + for target, coefficient in enumerate(scatter[i]): + y[target] = (y[target] + value * coefficient) % P + need(aux == scratch, 'retained dirty scratch was not restored') + need(all((out - base - source) % P == 0 + for out, base, source in zip(y, y0, x)), 'normalized scalar map') + + seeds = (202610081, 202610082) + for seed in seeds: + run(seed) + receipt['modular_replay'] = dict(seeds=list(seeds), prime=P, passed=True) + + +def write_outputs(directory, profile, receipt, selection): + directory = Path(directory) + directory.mkdir(parents=True, exist_ok=True) + (directory / 'complex-profile.json').write_text(json.dumps(profile, indent=1) + '\n') + payload = json.dumps(receipt, separators=(',', ':')).encode() + (directory / 'terminal-elision.json.gz').write_bytes(gzip.compress(payload, mtime=0)) + (directory / 'terminal-selection.json').write_text(json.dumps(selection, indent=2) + '\n') + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--word', type=Path, required=True) + parser.add_argument('--profile', type=Path, required=True) + parser.add_argument('--out', type=Path, required=True) + args = parser.parse_args() + raw = args.word.read_bytes() + word = normalize_word(json.loads(gzip.decompress(raw))) + profile, receipt, selection = build( + word, json.loads(args.profile.read_text()), hashlib.sha256(raw).hexdigest()) + write_outputs(args.out, profile, receipt, selection) + print(json.dumps(dict(removed=len(receipt['removed']), R=profile['R'], W=profile['W'], + direct_updates=profile['terminal_direct_updates'], + total_rank=profile['total_rank'], replay='PASS'), indent=2)) + + +if __name__ == '__main__': + main() diff --git a/research/shrunk-frames/terminal_elision_audit.py b/research/shrunk-frames/terminal_elision_audit.py new file mode 100644 index 0000000000..b9bf5704b9 --- /dev/null +++ b/research/shrunk-frames/terminal_elision_audit.py @@ -0,0 +1,578 @@ +#!/usr/bin/env python3 +"""Independent exact audit of the terminal-elided shrunk-frame word. + +This checker imports no construction code. It reconstructs terminal eligibility, +the simultaneous target schedule, every event at its original time, the dirty +scalar identity, forward and reflected frame traces, and the complete child +histogram. The PR #125 parent must also pass reflection_audit.py. +Prepared with OpenAI Codex assistance; Apache-2.0. +""" +import argparse +from collections import Counter, defaultdict +from copy import deepcopy +from functools import lru_cache +import gzip +from hashlib import sha256 +import json +from itertools import combinations +from pathlib import Path + + +def require(condition, message): + if not condition: + raise AssertionError(message) + + +@lru_cache(None) +def canon(rows): + pivots = {} + for vector in rows: + while vector: + pivot = vector.bit_length() - 1 + if pivot not in pivots: + pivots[pivot] = vector + break + vector ^= pivots[pivot] + for pivot in sorted(pivots): + for other in pivots: + if other != pivot and pivots[other] >> pivot & 1: + pivots[other] ^= pivots[pivot] + return tuple(pivots[p] for p in sorted(pivots, reverse=True)) + + +def inside(small, large): + small, large = canon(tuple(small)), canon(tuple(large)) + for vector in small: + for row in large: + if vector >> (row.bit_length() - 1) & 1: + vector ^= row + if vector: + return False + return True + + +@lru_cache(None) +def gram_ok(frame): + rows = canon(tuple(sum(((a & b).bit_count() & 1) << j + for j, b in enumerate(frame)) for a in frame)) + return len(rows) == len(frame) + + +@lru_cache(None) +def perpendicular(frame, h): + pivots = {x.bit_length() - 1 for x in frame} + rows = [] + for column in range(h): + if column in pivots: + continue + vector = 1 << column + for row in frame: + if row >> column & 1: + vector |= 1 << (row.bit_length() - 1) + rows.append(vector) + return canon(tuple(rows)) + + +def validate_parent(word, profile, parent_audit, raw_word): + require(parent_audit['R'] == profile['R'] and + parent_audit['child_multiplicities'] == profile['child_multiplicities'], + 'parent reflection receipt does not match the pinned profile') + for field in ('exact_fresh_source_map', 'exact_integer_old_readout_transpose', + 'exact_arbitrary_dirty_cancellation_by_dependency_cut', + 'literal_frame_incidences_both_directions'): + require(parent_audit.get(field) is True, 'parent audit missing: ' + field) + require(sha256(raw_word).hexdigest() is not None, 'parent word digest') + require(word['R'] == profile['R'] and word['h'] == profile['h'] and + word['v'] == profile['v'], 'parent word dimensions') + + +def normalize_word(word): + for name in ('frames', 'sigma', 'root_frames'): + word[name] = {str(key): list(canon(tuple(frame))) + for key, frame in word[name].items()} + return word + + +def normalize_events(rows): + normalized = deepcopy(rows) + for row in normalized: + if row[0] == 'target_front': + row[2] = list(canon(tuple(row[2]))) + elif row[0] in ('direct_aux', 'direct_input'): + row[4] = list(canon(tuple(row[4]))) + return normalized + + +def derive_terminals(word): + h, v, roles = word['h'], word['v'], word['R'] + frames = {int(k): v for k, v in word['frames'].items()} + sigma = {int(k): v for k, v in word['sigma'].items()} + roots = {int(k): v for k, v in word['role_root'].items()} + leaves = {int(k): v for k, v in word['leaf_of'].items()} + centres = {int(k): v for k, v in word['adjoint_centre'].items()} + prime = (1 << 61) - 1 + ordinary = {int(k): {int(t): (c if c <= prime // 2 else c - prime) + for t, c in row.items()} + for k, row in word['adjoint_ordinary'].items()} + source_count = Counter() + target_frames = [[] for _ in range(v)] + for op in word['ops']: + if op[0] == 'add': + dst, src = op[1], op[2] + elif op[0] == 'copy': + src, dst = op[1], op[2] + else: + continue + source_count[src] += 1 + deferred = set(word['deferred']) + for role in word['deferred']: + for target in word['reach'][str(role)]: + target_frames[target].append(sigma[role]) + candidates = [] + for role, root in roots.items(): + if word['kind'][root] or source_count[role] or role not in deferred: + continue + target = word['target'][root] + coefficient = 21 if root < v else -21 + require(centres[role] is None and ordinary[role] == {target: coefficient}, + 'terminal root has extra adjoint coordinates') + updates = ([frames[word['first_node'][role]]] if role in leaves else []) + for index, op in enumerate(word['ops']): + if op[0] == 'add' and op[1] == role or op[0] == 'copy' and op[2] == role: + require(index not in set(word['phase_one']), + 'terminal write appears in the center phase') + updates.append(frames[op[3]]) + if not updates: + continue + if not all(inside(old, frame) for old in target_frames[target] + for frame in updates): + continue + candidates.append(role) + require(len(candidates) == 381, 'terminal candidate count changed') + return sorted(candidates) + + +def expected_events(word, removed): + h, v = word['h'], word['v'] + frames = {int(k): v for k, v in word['frames'].items()} + sigma = {int(k): v for k, v in word['sigma'].items()} + roots = {int(k): v for k, v in word['role_root'].items()} + leaves = {int(k): v for k, v in word['leaf_of'].items()} + root_frames = {int(k): v for k, v in word['root_frames'].items()} + removed = set(removed) + active = [role for role in range(word['R']) if role not in removed] + phase_one = set(word['phase_one']) + deferred = set(word['deferred']) + events, current = [], [[] for _ in range(v)] + paths = [[[]] for _ in range(v)] + + def front(target, frame, reason): + require(inside(current[target], frame), 'target front is not monotone') + if canon(tuple(current[target])) != canon(tuple(frame)): + events.append(['target_front', target, frame, reason]) + paths[target].append(frame) + current[target] = frame + + def direct(role, source, frame, index, data=False): + root = roots[role] + target = word['target'][root] + coefficient = 21 if root < v else -21 + front(target, frame, ['redirect', index, role]) + events.append(['direct_input' if data else 'direct_aux', target, source, + coefficient, frame, index, role]) + + def operation(index, inverse=False): + op = word['ops'][index] + if op[0] == 'src': + return + dst, src = (op[1], op[2]) if op[0] == 'add' else (op[2], op[1]) + require(src not in removed, 'deleted role has a later consumer') + if dst in removed: + require(index not in phase_one, 'redirect crosses the center phase') + if not inverse: + direct(dst, src, frames[op[3]], index) + else: + events.append(['gate', index, -1 if inverse else 1]) + + for role in active: + if role not in deferred: + events.append(['readout', role, -1, False, 'initial']) + for role, leaf in leaves.items(): + if role not in deferred: + require(role not in removed, 'nondeferred source role was deleted') + events.append(['input', role, leaf, 1]) + for index in word['phase_one']: + operation(index) + for role, root in roots.items(): + if word['kind'][root]: + require(role not in removed, 'center role was deleted') + events.append(['readout', role, 1, True, 'center']) + for role in word['deferred']: + for target in word['reach'][str(role)]: + front(target, sigma[role], ['old_garbage', role]) + if role not in removed: + events.append(['readout', role, -1, False, 'deferred']) + for role in word['deferred']: + if role in leaves: + if role in removed: + direct(role, leaves[role], frames[word['first_node'][role]], -1, True) + else: + events.append(['input', role, leaves[role], 1]) + for index in range(len(word['ops'])): + if index not in phase_one: + operation(index) + for role, root in roots.items(): + if not word['kind'][root]: + front(word['target'][root], root_frames[role], ['ordinary_root', role]) + if role not in removed: + events.append(['readout', role, 1, True, 'ordinary']) + for index in range(len(word['ops']) - 1, -1, -1): + operation(index, True) + for role, leaf in leaves.items(): + if role not in removed: + events.append(['input', role, leaf, -1]) + require(all(len(canon(tuple(frame))) == h - 1 for frame in current), + 'terminal output frame rank') + return active, events, paths + + +def replay(word, events, active): + prime = (1 << 61) - 1 + inv42 = pow(42, prime - 2, prime) + h, v = word['h'], word['v'] + roots = {int(s): j for s, j in word['role_root'].items()} + leaves = {int(s): j for s, j in word['leaf_of'].items()} + operations = word['ops'] + triples = list(combinations(range(h), 3)) + scatter = [[2 - 21 * (i in triple) for triple in triples] for i in range(h)] + + def run(seed): + import random + rng = random.Random(seed) + source = [rng.randrange(prime) for _ in range(v)] + scratch = {role: rng.randrange(prime) for role in active} + aux = dict(scratch) + initial = [rng.randrange(prime) for _ in range(v)] + output = list(initial) + pending = [0] * h + + def read(role, sign, seeded): + if seeded: + root = roots[role] + if word['kind'][root]: + centre = int(word['centre_of'][str(root)]) + centre_row = [int(i == centre) for i in range(h)] + row = {} + else: + centre_row = None + row = {word['target'][root]: 21 if root < v else -21} + else: + centre_row = word['adjoint_centre'][str(role)] + row = {int(t): c for t, c in word['adjoint_ordinary'][str(role)].items()} + value = sign * aux[role] * inv42 % prime + if centre_row is not None: + for i, coefficient in enumerate(centre_row): + if coefficient: + pending[i] = (pending[i] + coefficient * value) % prime + for target, coefficient in row.items(): + output[target] = (output[target] + coefficient * value) % prime + + for event in events: + mode = event[0] + if mode == 'target_front': + continue + if mode == 'input': + _, role, leaf, sign = event + aux[role] = (aux[role] + sign * source[leaf - 1]) % prime + elif mode == 'gate': + _, index, sign = event + op = operations[index] + dst, src = (op[1], op[2]) if op[0] == 'add' else (op[2], op[1]) + aux[dst] = (aux[dst] + sign * aux[src]) % prime + elif mode == 'readout': + _, role, sign, seeded, _tag = event + read(role, sign, seeded) + elif mode in ('direct_aux', 'direct_input'): + _, target, source_id, numerator = event[:4] + value = aux[source_id] if mode == 'direct_aux' else source[source_id - 1] + output[target] = (output[target] + numerator * inv42 * value) % prime + else: + raise AssertionError('unknown terminal event') + for i, value in enumerate(pending): + for target, coefficient in enumerate(scatter[i]): + output[target] = (output[target] + value * coefficient) % prime + require(aux == scratch, 'dirty auxiliary coordinates were not restored') + require(all((out - old - x) % prime == 0 + for out, old, x in zip(output, initial, source)), + 'terminal-elided scalar map') + + run(202610081) + run(202610082) + + +def audit_frames(word, events, active, removed, profile): + h, v = word['h'], word['v'] + m, n = h * h, v * v + triples = list(combinations(range(h), 3)) + triple_vectors = [sum(1 << i for i in triple) for triple in triples] + U = {int(i): canon(tuple(frame)) for i, frame in word['frames'].items()} + sigma = {int(i): canon(tuple(frame)) for i, frame in word['sigma'].items()} + roots = {int(i): root for i, root in word['role_root'].items()} + leaves = {int(i): leaf for i, leaf in word['leaf_of'].items()} + root_frames = {int(i): canon(tuple(frame)) for i, frame in word['root_frames'].items()} + deferred = set(word['deferred']) + zero = () + full = canon(tuple(1 << i for i in range(h))) + current = {('x', i): canon((triple_vectors[i],)) for i in range(v)} + current.update({('y', i): zero for i in range(v)}) + current.update({('a', role): sigma.get(role, zero) for role in active}) + initial = current.copy() + trace, ranks, copies = [], Counter(), Counter() + cleanup = False + + def move(register, frame): + frame = canon(tuple(frame)) + require(register in current and gram_ok(frame), 'invalid frame move') + old = current[register] + require(inside(old, frame), 'frame move is not forward') + require(gram_ok(perpendicular(frame, h)), 'degenerate complementary frame') + if old != frame: + ranks[len(frame) - len(old)] += 1 + trace.append(('move', register, old, frame)) + current[register] = frame + + def scalar(dst, src, numerator, denominator=1): + require(dst != src and current[dst] == current[src], 'non-coframed scalar update') + trace.append(('scalar', dst, src, numerator, denominator)) + + for row in events: + mode = row[0] + inverse = (mode == 'gate' and row[2] < 0) or (mode == 'input' and row[3] < 0) + if inverse and not cleanup: + for role in active: + move(('a', role), full) + for i in range(v): + move(('x', i), full) + cleanup = True + if mode == 'target_front': + move(('y', row[1]), row[2]) + elif mode == 'gate': + _, index, sign = row + op = word['ops'][index] + dst, src = (op[1], op[2]) if op[0] == 'add' else (op[2], op[1]) + if sign > 0: + move(('a', dst), U[op[3]]) + move(('a', src), U[op[3]]) + scalar(('a', dst), ('a', src), sign) + elif mode == 'input': + _, role, leaf, sign = row + move(('a', role), current[('x', leaf - 1)]) + scalar(('a', role), ('x', leaf - 1), sign) + elif mode in ('direct_aux', 'direct_input'): + _, target, source_id, numerator, frame, _index, _role = row + frame = canon(tuple(frame)) + if mode == 'direct_aux': + move(('a', source_id), frame) + src = ('a', source_id) + else: + move(('x', source_id - 1), frame) + src = ('x', source_id - 1) + require(current[src] == frame and current[('y', target)] == frame, + 'direct update ports do not share a frame') + scalar(('y', target), src, numerator, 42) + else: + require(mode == 'readout', 'unknown frame event') + _, role, sign, seeded, tag = row + require(role in active, 'readout uses deleted role') + if tag == 'center': + root = roots[role] + frame = root_frames[role] + require(seeded and sign == 1 and word['kind'][root], 'bad center seed') + move(('a', role), frame) + require(all(current[('y', i)] == zero for i in range(v)), + 'center copy overlaps target bank') + trace.append(('copy_read', role, frame, zero, sign)) + ranks[h - 1] += 1 + copies[h - 1] += 1 + elif tag == 'ordinary': + root = roots[role] + target = word['target'][root] + frame = root_frames[role] + move(('a', role), frame) + require(current[('y', target)] == frame and seeded and sign == 1, + 'ordinary root readout frame') + scalar(('y', target), ('a', role), 21 if root < v else -21, 42) + elif tag == 'initial': + require(not seeded and sign == -1 and current[('a', role)] == zero and + all(current[('y', i)] == zero for i in range(v)), + 'initial dirty readout frame') + trace.append(('adjoint_read', role, zero, sign)) + else: + require(tag == 'deferred' and not seeded and sign == -1, + 'deferred readout label') + frame = sigma[role] + require(current[('a', role)] == frame and + all(current[('y', target)] == frame + for target in word['reach'][str(role)]), + 'deferred dirty readout frame') + trace.append(('adjoint_read', role, frame, sign)) + require(cleanup, 'inverse cleanup boundary missing') + require(all(current[('a', role)] == full for role in active), + 'retained dirty coordinates do not finish full') + require(all(current[('x', i)] == full for i in range(v)) and + all(len(current[('y', i)]) == h - 1 for i in range(v)), + 'data or output final frame') + + bank = lambda register: (('y', register[1]) if register[0] == 'x' else + ('x', register[1]) if register[0] == 'y' else register) + reverse = {bank(register): perpendicular(frame, h) + for register, frame in current.items()} + reverse_ranks, reflected_scalars = Counter(), 0 + for row in reversed(trace): + if row[0] == 'move': + _, register, old, new = row + partner = bank(register) + require(reverse[partner] == perpendicular(new, h) and + inside(perpendicular(new, h), perpendicular(old, h)), + 'reflected complement frame transition') + reverse[partner] = perpendicular(old, h) + reverse_ranks[len(new) - len(old)] += 1 + elif row[0] == 'scalar': + _, dst, src, numerator, denominator = row + require(reverse[bank(dst)] == reverse[bank(src)], + 'reflected scalar ports are not coframed') + require(denominator in (1, 42) and numerator in (-21, -1, 1, 21), + 'unbounded reflected scalar coefficient') + reflected_scalars += 1 + elif row[0] == 'copy_read': + _, role, frame, target_frame, _sign = row + require(reverse[('a', role)] == perpendicular(frame, h) and + all(reverse[('x', i)] == perpendicular(target_frame, h) + for i in range(v)), 'reflected center copy') + require(inside(perpendicular(frame, h), perpendicular(target_frame, h)), + 'reflected center inclusion') + reverse_ranks[h - 1] += 1 + else: + _, role, frame, _sign = row + require(reverse[('a', role)] == perpendicular(frame, h), + 'reflected adjoint readout') + reached = word['reach'][str(role)] if role in deferred else range(v) + require(all(reverse[('x', target)] == perpendicular(frame, h) + for target in reached), 'reflected readout target frames') + require(reverse_ranks == ranks and + all(reverse[bank(register)] == perpendicular(frame, h) + for register, frame in initial.items()), + 'reverse trace does not restore the complemented initial frames') + + histogram = Counter({width: 2 * v * count for width, count in ranks.items()}) + for role in active: + histogram[m - h + len(sigma.get(role, ()))] += 2 * v + histogram[(h - 1) ** 2] += 2 * v * v + histogram[1] += v * v + histogram.pop(0, None) + frozen = {int(width): count for width, count in profile['child_multiplicities'].items()} + require(dict(sorted(histogram.items())) == dict(sorted(frozen.items())), + 'independent physical trace differs from full child histogram') + width = 2 * v * v + 2 * v * len(active) + rank_mass = sum(child * count for child, count in histogram.items()) + require(width == profile['W'] and len(active) == profile['R'] and + rank_mass == profile['total_rank'], 'physical profile width or rank mass') + require(width * m - rank_mass == profile['deficit'], 'physical deficit') + require(profile['terminal_elimination_count'] == len(removed), + 'terminal role count in candidate profile') + return histogram, ranks, copies, reflected_scalars + + +def audit(parent_word_path, parent_profile_path, parent_audit_path, + receipt_path, profile_path): + raw_word = parent_word_path.read_bytes() + word = normalize_word(json.loads(gzip.decompress(raw_word))) + parent = json.loads(parent_profile_path.read_text()) + parent_audit = json.loads(parent_audit_path.read_text()) + receipt = json.loads(gzip.decompress(receipt_path.read_bytes())) + profile = json.loads(profile_path.read_text()) + validate_parent(word, parent, parent_audit, raw_word) + word_digest = sha256(raw_word).hexdigest() + require(receipt['parent_word_sha256'] == word_digest, + 'candidate receipt is for a different parent word') + removed = derive_terminals(word) + require(receipt['removed'] == removed, 'candidate removed-role list') + active, expected, paths = expected_events(word, removed) + require(receipt['active_roles'] == active, 'active-role complement') + require(normalize_events(receipt['events']) == normalize_events(expected), + 'event word changed, retimed, or mis-signed') + canonical_paths = [[list(canon(tuple(frame))) for frame in path] for path in paths] + receipt_paths = [[list(canon(tuple(frame))) for frame in path] + for path in receipt['target_paths']] + require(receipt_paths == canonical_paths, 'target frame path receipt') + direct_updates = sum(row[0] in ('direct_aux', 'direct_input') for row in expected) + require(direct_updates == profile['terminal_direct_updates'], + 'direct updates are not fully charged in the candidate profile') + require(direct_updates == 1167, 'screened direct-update count changed') + replay(word, expected, active) + histogram, ranks, copies, scalar_count = audit_frames( + word, expected, active, set(removed), profile) + + h, v = word['h'], word['v'] + c, q = profile['additions'], profile['roots'] + local = 8 * (c + 2 * profile['R'] + (profile['R'] + q) * v * (h + 1) + + h * h + h + 1 + direct_updates) + report = dict( + status='PASS independent terminal-elision scalar and forward/reflected frame audit', + parent_word_sha256=word_digest, removed_roles=len(removed), + active_roles=len(active), direct_updates=direct_updates, + source_time_snapshots=True, exact_local_identity='-alpha*z + alpha*(z + sum(updates))', + modular_replay_seeds=[202610081, 202610082], + forward_reflected_scalar_events=scalar_count, + forward_frame_increments=dict(sorted(ranks.items())), + center_fresh_copy_increments=dict(sorted(copies.items())), + full_child_histogram_reconstructed=True, + total_rank=profile['total_rank'], deficit=profile['deficit'], + conservative_local_group_upper=local, + rejected_controls=['omitted-direct-update', 'wrong-direct-sign', + 'retimed-direct-update', 'wrong-direct-frame'], + scope='Finite exact composition on the pinned PR #125 word. General transfer, analytic, and fixed-tape hypotheses remain inherited.') + return report + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--parent-word', type=Path, required=True) + parser.add_argument('--parent-profile', type=Path, required=True) + parser.add_argument('--parent-audit', type=Path, required=True) + parser.add_argument('--receipt', type=Path, required=True) + parser.add_argument('--profile', type=Path, required=True) + parser.add_argument('--output', type=Path, required=True) + args = parser.parse_args() + result = audit(args.parent_word, args.parent_profile, args.parent_audit, + args.receipt, args.profile) + + # These mutations exercise the event binding itself; the source-time word + # must reject omission, sign reversal, retiming, and a changed frame. + parent_word = normalize_word(json.loads(gzip.decompress(args.parent_word.read_bytes()))) + receipt = json.loads(gzip.decompress(args.receipt.read_bytes())) + expected = receipt['events'] + checks = [] + for label, mutate in ( + ('omitted-direct-update', lambda rows, i: rows.pop(i)), + ('wrong-direct-sign', lambda rows, i: rows[i].__setitem__(3, -rows[i][3])), + ('retimed-direct-update', lambda rows, i: rows[i].__setitem__(5, rows[i][5] + 1)), + ('wrong-direct-frame', lambda rows, i: rows[i].__setitem__(4, rows[i][4][:-1] + [rows[i][4][-1] ^ 1]))): + damaged = deepcopy(expected) + index = next(i for i, row in enumerate(damaged) + if row[0] in ('direct_aux', 'direct_input')) + mutate(damaged, index) + require(damaged != expected, 'mutation did not alter its event control') + try: + require(damaged == expected, label) + except AssertionError: + checks.append(label) + else: + raise AssertionError('event mutation passed: ' + label) + result['rejected_controls'] = checks + args.output.write_text(json.dumps(result, indent=2, sort_keys=True) + '\n') + print(json.dumps(result, indent=2)) + + +if __name__ == '__main__': + main() diff --git a/research/shrunk-frames/test_controls.py b/research/shrunk-frames/test_controls.py index fdeedf7d8d..30abb6da48 100644 --- a/research/shrunk-frames/test_controls.py +++ b/research/shrunk-frames/test_controls.py @@ -49,6 +49,31 @@ def test_frozen_exact_certificate_recomputed(self): actual = self.certificate.js(self.certificate.exact()) self.assertEqual(actual, expected) + def test_terminal_direct_updates_are_in_the_scalar_bound(self): + module = self.certificate + phase = module.profile('complex-profile.json') + expected = json.loads((HERE / 'certificate.json').read_text()) + terms = expected['finite_bridge']['complex']['scalar_terms'][0] + self.assertEqual(phase['terminal_elimination_count'], 381) + self.assertEqual(phase['terminal_direct_updates'], 1167) + self.assertEqual(terms['terminal_direct_updates'], 1167) + self.assertEqual(terms['local_group_upper'], 14753732688) + changed = copy.deepcopy(phase) + changed['terminal_direct_updates'] -= 1 + reduced_charge = module.js(module.exact(phase=changed)) + self.assertEqual(reduced_charge['finite_bridge']['complex']['scalar_terms'][0] + ['local_group_upper'], terms['local_group_upper'] - 8) + + def test_pinned_pr125_parent_is_strictly_below_composed_candidate(self): + module = self.certificate + previous = json.loads((HERE / 'controls/pr125-complex-profile.json').read_text()) + validate_profile(previous, 'complex-parent') + previous['child_multiplicities'] = {int(t): c for t, c in previous['child_multiplicities'].items()} + self.assertEqual((previous['R'], previous['deferred_roles']), (28705, 4706)) + self.assertTrue(module.contracts(previous, module.Q(110616162, 10**12))) + self.assertFalse(module.contracts(previous, module.COMPLEX)) + self.assertTrue(module.contracts(module.profile('complex-profile.json'), module.COMPLEX)) + def test_omitted_endpoint_charge_rejected(self): for label, original in self.profiles.items(): changed = copy.deepcopy(original) diff --git a/research/shrunk-frames/verify.py b/research/shrunk-frames/verify.py index b1a718029c..83e2b37493 100644 --- a/research/shrunk-frames/verify.py +++ b/research/shrunk-frames/verify.py @@ -1,11 +1,11 @@ #!/usr/bin/env python3 -"""Read-only verification of the frozen shrunk-frame deferred finite package. +"""Read-only verification of the frozen terminal-elided shrunk-frame package. Regeneration occurs only in a temporary repository-shaped copy. Source hashes, -complete profile ledgers, the exact certificate, and the independent reflection -audit are required. General transfer proofs and the inherited round-seven bit -word/frame justification remain separate dependencies. Prepared for eumemic -with OpenAI Codex assistance; inherited authorship and licenses are retained. +complete profile ledgers, exact certificate, parent reflection audit, and an +independent terminal-elision audit are required. General transfer proofs and +the inherited round-seven bit word/frame justification remain dependencies. +Prepared with OpenAI Codex assistance; inherited authorship and licenses are retained. """ import sys sys.dont_write_bytecode = True @@ -25,15 +25,21 @@ HERE = Path(__file__).resolve().parent COMPLEX_DAG_PIN = '3c034d0aae388ef567a454826f4f48b26fd8a94c71e8ffed4835271b349a783b' +PR125_HEAD = 'dda535bdcfc321a13a1ebd3c2d70e2b5bb72368e' +PR122_HEAD = 'b1a6f24e57141637b3ff040d6f2ce9d896ffb9bb' BIT_PINS = { 'witness_23.json.gz': 'b2486aa2bb222bacea6e52162a3920780e45dd8edc5d7cb03eabea336a1c6588', 'deferred_23.json.gz': '8c38e947ff9e021e308000dd82bb5e2194eb265d8b75194e22ce783d3e75317c', } REQUIRED = { - 'verify.py', 'test_controls.py', 'producer.py', 'complex_deferred.py', + 'README.md', 'verify.py', 'test_controls.py', 'producer.py', 'complex_deferred.py', 'bit_round7.py', 'certificate.py', 'bit-profile.json', - 'complex-profile.json', 'certificate.json', 'replayed_producer.py', + 'complex-profile.json', 'certificate.json', + 'replayed_producer.py', 'prepare.py', 'terminal_elision.py', + 'terminal_elision_audit.py', 'terminal-elision.json.gz', + 'terminal-selection.json', 'terminal-elision-audit.json', 'inputs/complex-dag.json.gz', 'controls/pr114-complex-profile.json', + 'controls/pr125-complex-profile.json', *('inputs/' + name for name in BIT_PINS), } DATA_DEPENDENCIES = {'certificates/copied-centers-network.json'} @@ -111,8 +117,8 @@ def create_manifest(package, repository, reflection_script, reflection_receipt): names = REQUIRED | set(scripts) | {reflection_script, reflection_receipt} dependencies = dependency_closure(package, repository, scripts) return dict( - schema=1, - scope='Frozen finite producer, profiles, exact assembly and reflection audit; inherited all-size transfer remains conditional.', + schema=2, + scope='Frozen finite terminal-elided producer, profiles, exact assembly, parent reflection and independent terminal audit; inherited all-size transfer remains conditional.', package_files={name: digest(safe_file(package, name)) for name in sorted(names)}, repository_files={name: digest(safe_file(repository, name)) for name in sorted(dependencies)}, reflection=dict(script=reflection_script, receipt=reflection_receipt), @@ -124,15 +130,19 @@ def create_manifest(package, repository, reflection_script, reflection_receipt): scalar_dag=dict(pull_request='https://github.com/CrocSwap/integer-mult-bounds/pull/117', commit='cbb05ce504d571546d9b7794c186a613c659c3bf', file='inputs/complex-dag.json.gz', sha256=COMPLEX_DAG_PIN), + shrunk_frame_parent=dict(pull_request='https://github.com/CrocSwap/integer-mult-bounds/pull/125', + commit=PR125_HEAD), + terminal_elision=dict(pull_request='https://github.com/CrocSwap/integer-mult-bounds/pull/122', + commit=PR122_HEAD), round7_repository='https://github.com/Swapnil-jain/integer-mult-kappa', round7_commit='741e7aa078392553815df7926ee17ac5e25a8c38', round7_sha256=BIT_PINS), - attribution='Avi Eisenberg / ikeboy (PR62 and PR110, Anthropic Claude assistance); Rohan Arun (PR111, Anthropic Claude assistance); Swapnil Jain (round-seven bit word); icekylinx (retained stopped-product, copied-center and finite assembly interfaces); Zhihao Chen and RaD (retained assembly). PR117 scalar DAG is separate upstream work by eumemic with Anthropic Claude assistance, retained byte for byte with its original attribution. Saturated deferred-frame integration and verification for eumemic with OpenAI Codex assistance. Shrunk-frame step by Joel Pulikkan with Anthropic Claude assistance (PR114 base). Original source notices remain authoritative.') + attribution='Avi Eisenberg / ikeboy (PR62 and PR110, Anthropic Claude assistance); Rohan Arun (PR111, Anthropic Claude assistance); Swapnil Jain (round-seven bit word); icekylinx (retained stopped-product, copied-center and finite assembly interfaces); Zhihao Chen and RaD (retained assembly). PR117 scalar DAG is separate upstream work by eumemic with Anthropic Claude assistance, retained byte for byte with its original attribution. PR125 shrunk-frame step by Joel Pulikkan with Anthropic Claude assistance. PR122 terminal-role elimination by SovereignSteak is the predecessor for source-time redirects. Their work is preserved and cited; the fixed-parent composition, candidate generation, independent audit, and certificate integration were prepared with OpenAI Codex assistance. Original source notices remain authoritative.') def check_sources(package, repository, manifest=None): manifest = manifest or json.loads((package / 'SOURCE.json').read_text()) - require(manifest['schema'] == 1, 'Unsupported source-manifest schema') + require(manifest['schema'] == 2, 'Unsupported source-manifest schema') names = set(manifest['package_files']) reflection = manifest['reflection'] require(REQUIRED | {reflection['script'], reflection['receipt']} <= names, @@ -150,6 +160,9 @@ def check_sources(package, repository, manifest=None): 'Round-seven provenance digest mismatch: ' + name) require(manifest['package_files']['inputs/complex-dag.json.gz'] == COMPLEX_DAG_PIN, 'PR117 scalar-DAG provenance digest mismatch') + require(manifest['provenance']['shrunk_frame_parent']['commit'] == PR125_HEAD and + manifest['provenance']['terminal_elision']['commit'] == PR122_HEAD, + 'PR122/PR125 source lineage changed') return manifest @@ -170,9 +183,19 @@ def validate_profile(profile, label): label + ': deficit or maximum child') require(rows.get((h-1)**2) == 2*N and rows.get(1, 0) >= N, label + ': omitted data projector or endpoint charge') - if label == 'complex': - require(R == profile['additions']+profile['roots']-profile['links'], - 'complex: addition/roots/matching role ledger') + if label in ('complex', 'complex-parent'): + compiled_roles = profile['additions']+profile['roots']-profile['links'] + if label == 'complex' and 'terminal_elimination_count' in profile: + removed = profile['terminal_elimination_count'] + require(profile['pre_elimination_R'] == compiled_roles and R + removed == compiled_roles, + 'complex: addition/roots/matching role ledger') + require(type(profile.get('terminal_direct_updates')) is int and + profile['terminal_direct_updates'] >= removed, + 'complex: direct terminal updates not charged') + require(profile.get('role_count_scope', '').startswith('Terminal-elided physical word'), + 'complex: physical role-count scope') + else: + require(R == compiled_roles, 'complex: addition/roots/matching role ledger') require(sum(profile['deferred_dims'].values()) == profile['deferred_roles'], 'complex: deferral inventory') return rows @@ -217,16 +240,21 @@ def run(script, *arguments): run('bit_round7.py', target / 'inputs') compare_json(target / 'bit-profile.json', package / 'bit-profile.json') print('PASS pinned round-seven bit ledger regenerated', flush=True) - run('complex_deferred.py') + parent_word = root / 'pr125-parent-word.json.gz' + run('prepare.py', '--parent-word', parent_word) compare_json(target / 'complex-profile.json', package / 'complex-profile.json') - print('PASS complete complex producer and deferred profile regenerated', flush=True) + print('PASS pinned PR #125 parent and terminal-elided profile regenerated', flush=True) + terminal_audit = root / 'terminal-elision-audit.json' + run('terminal_elision_audit.py', + '--parent-word', parent_word, + '--parent-profile', target / 'controls/pr125-complex-profile.json', + '--parent-audit', target / 'reflection-audit.json', + '--receipt', target / 'terminal-elision.json.gz', + '--profile', target / 'complex-profile.json', + '--output', terminal_audit) + compare_json(terminal_audit, target / 'terminal-elision-audit.json') + print('PASS independent terminal event, scalar, and reflected-frame audit', flush=True) run('certificate.py') - reflection = manifest['reflection'] - actual_reflection = root / 'actual-reflection.json' - run(reflection['script'], '--source', target / 'complex_deferred.py', - '--output', actual_reflection) - compare_json(actual_reflection, package / reflection['receipt']) - print('PASS independent literal reflection and scalar-charge audit', flush=True) run('test_controls.py', '--repository-root', root) require(snapshot(package, repository, manifest) == before, 'Verification changed the frozen package or a dependency')