diff --git a/research/p104-fused-late-cleanup/PROOF.md b/research/p104-fused-late-cleanup/PROOF.md new file mode 100644 index 0000000000..3538fd855c --- /dev/null +++ b/research/p104-fused-late-cleanup/PROOF.md @@ -0,0 +1,217 @@ +# Fusing late FULL delivery with residual-based dirty cleanup + +## Result and predecessor boundary + +This is one explicit composition of two existing local constructions: +PR3981's late FULL delivery (`cdb7dcf3f7e5f860714a1b12df4c7a5157d8ae3d`) +and PR3943's compressed Q cleanup +(`2cba526a4ebe0ef6c3c0143498adcf67dca97941`). The source-preserving variant also uses PR3940's frozen fused tail +(`51ba88c007cfbcc3d9cf22dd321f5224be3a5bb1`). The encoded correction is PR3882's +frozen builder (`9d56eeedbed5e3e9bbbc8c189d66f14cf15b6067`, publication head +`d76586303e7036baa74f8deb2155038290174ffd`). The contribution is the source-bound +fusion and its complete invoice, not a new discovery of either ingredient. + +The measurable target is fewer than 5472 unit ADDs with the same native mass +2520 and exact old endpoint. The construction achieves **4704 unit ADDs**, +with the same **2616 halves, 2616 doubles, and native mass 2520**. All 280 +independent input columns, all 72 arbitrary dirty helper returns, and the +complete endpoint rows and formal frames are preserved. A second actual source-preserving consumer falls from5856 to5088 unit ADDs +with2712 halves/doubles and the same native mass2520. This is a finite +Gaussian-dyadic module identity, not a new multiplication theorem or kappa. + +## Literal source extraction and the fusion cut + +Use the original 4058-event native-channel witness. Its final 416 events, +zero-based indices 3642 through 4057, are exactly + + Q_k += D[k,i] X_i, + +with 52 nonzero coefficients per query, all ±2, at FULL. Extract D from these +literal events. In the PR3882 pivot order +`J=[0,1,3,6,22,31,93,103]`, set `T=D[:,J]`. The full exact matrix T is in +RESULT.json; it has 32 nonzero entries, all ±2. For the actual Gram block +`A=[[I,B],[B^t,B^t B]]`, direct exact multiplication gives + + D = T [I B]. + +This is checked against PR3943's unchanged T, but the cleanup coefficients +are independently re-extracted from the main-branch witness. The verifier +also checks the state produced by the actual PR3981 schedule, rather than +assuming a possible query preparation. + +Remove the last 416 cleanup events from PR3981's generated word. Its remaining +prefix includes all original public transports, its 104 retimed Y lifts, and +all 416 late Q-to-Y deliveries. Each query was quartered for these unit reads +and then doubled twice, restoring its value before the next step. At this +precise cut all 280 roles are FULL and their normalized rows are + + X=x, Y=v=y+Ax, Q=h-Dx, G=h_G, Dhelpers=h_D. + +Here h, h_G and h_D are independent arbitrary dirty inputs. They are not zero +or source-dependent promises. The two meanings of D (cleanup matrix and +register-family name) are distinguished above and in the verifier. + +## Chronology and reversible linear algebra + +Execute the actual PR3882 tail **without its initial 104 lifts**, because the +prefix has already performed them. Its reads and writes are confined to X,Y. +Writing `q=x_J+B x_N` and `w=x+y`, its endpoint is + + X_J=q, Y_J=w_J, X_N=w_N, Y_N=v_N. + +The residual donors X_J and query recipients Q remain FULL; X_N and Y_J +occupy their indexed target hyperplanes. Q still equals h-Dx. Execute the +actual PR3943 consumer: for each nonzero T[k,b], add the signed X_J donor to +Q_k twice. This uses 64 unit ADDs, no scratch, no scaling, no transport, and +leaves every donor unchanged. Since + + Tq = T(x_J+B x_N) = Dx, + +it restores Q to h. The tail did not touch G or delivery helpers, so all 72 +dirty returns hold simultaneously. Every data endpoint equals PR3981 followed +by the original correction after its old cleanup. The verifier compares all +280 rows, including the retained residuals, rather than only the sum slots. + +The ordering is essential. Late Q-to-Y delivery must finish while the live +queries still carry their source contribution; the quartered donors must be +restored; the correction must then create the actual residual q before Tq is +read. Running Tq cleanup earlier uses x_J rather than q. Running the old Dx +cleanup after the correction attempts reads from consumed/non-FULL X_N. +Neither incorrect reordering is silently admitted. + +## Source-preserving fusion at the actual PR3940 internal cut + +The unchanged `fused(J,N,B)` builder from PR3940 supplies a stronger matched +source-preserving comparison than returning after the encoded exit. Its104 +initial Y lifts are again already present in the late-delivery prefix. Its +remaining program is the actual sequence + +1. Pivot stream: X_J becomes q and Y_J becomes w_J; X_N remains x_N. +2. Scatter `Y_N -= B^t q`, leaving Y_N=y_N. Each temporary half of a pivot + donor is restored by the builder's corresponding double. +3. Inverse pivot stream: `X_J -= B x_N`, restoring x_J. +4. `Y_N += X_N`, producing w_N; drop all104 Y to their indexed hyperplanes. + +Insert the same64-unit Tq cleanup **between steps2 and3**. Its exact internal +cut is1360 tail operations after the removed104 lifts. The verifier compares +the literal prefix against the frozen `pivot_stream + scatter` builders, +checks every X_J donor equals the same exact q row as in the encoded variant, +and checks all donors and Q recipients are FULL. It also checks Q still equals +h−Dx. This excludes both reading a still-halved pivot and reading after the +inverse stream has destroyed q. All X/Y operations otherwise remain unchanged. + +The matched baseline is the entire actual3981 word with its original Q cleanup, +followed by this same3940 fused tail. The new whole word preserves its280 rows +and frames, including every X_i=x_i at FULL, every Y_i=x_i+y_i in H_i, and all72 +dirty returns. Its chronological native subsequence is literally equal to +that baseline's. The correction's scalar counts are1632 ADDs and200 each +half/double:768 pivot-stream ADDs,384 scatter ADDs,384 inverse-stream ADDs, +and96 sum ADDs. Therefore the complete matched invoices are + +| Source-preserving module | Unit ADDs | Halves | Doubles | Native mass | +|---|---:|---:|---:|---:| +| Late delivery + old cleanup + actual3940 fused tail |5856|2712|2712|2520| +| Late delivery +3940 tail with internal Tq cleanup |5088|2712|2712|2520| + +This saves another768 ADDs under the same comparison convention, with no +additional native work. Relative to the encoded fused result, source preservation +costs384 additional ADDs and96 each half/double in these particular words. +It does not require the192-native post-encoding return adapter. The later +comparison with that adapter is context and an actual integration check; +neither alternative is claimed optimal over all source-preserving programs. +Moving the cleanup after step3 instead breaks all8 Q dirty returns, as an +additional whole-word negative control confirms. + +## Physical contract and inherited native evidence + +Each new schedule has **exactly the same chronological native transport +subsequence** as its matched reference (3981 plus3882 or plus3940), including every retimed lift and the +correction's final drops. This is a literal ordered-event equality, not an +inference from an equal histogram. No lift, descent, chart adapter, private +register, or role change is added. The new 64 reads are scalar additions in +a common FULL chart. The independent evaluator verifies every arithmetic +entrance and every nested transport entrance and positive dimension tariff. + +With the inherited invariant `physical_r=Gamma_frame(r)*logical_row_r`, +these scalar identities hold for arbitrary address functions over +`Z[i,1/2]`. The old source and target chart operators retain exactly their +existing meaning. In particular, equality of frame spans is not being used +to donate an unproved physical basis change: the native event sequence itself +is unchanged. PR3981's 104 lift recipes were bound to the ordered canonical +bases from the native certificate and checked for signed Pauli action and +exact phase. That phase evidence is inherited here, not freshly replayed. +PR1991's full historical native realization and the final PR3882 physical, +owner, global, precision and all-size qualifications remain as stated there. +The PR3940 source-preserving tail likewise retains its stated native/admission +qualifications. The present new verifier independently checks the complete scalar/frame +composition; it does not claim a fresh native recipe audit. + +## Complete matched invoice + +Both sides use the same explicit scalar lowering: for an old coefficient +p/2^s, halve its donor s times, perform |p| signed unit ADDs, then double it +s times. New late-delivery batching and the correction's already batched +scalings remain literal. This is a valid upper bound, not a scalar optimum. + +| Complete module | Unit ADDs | Halves | Doubles | Native mass | +|---|---:|---:|---:|---:| +| PR3981 + old cleanup + correction | 5472 | 2616 | 2616 | 2520 | +| Fused prefix + early correction + Tq cleanup | 4704 | 2616 | 2616 | 2520 | +| Difference | -768 | 0 | 0 | 0 | + +The removed 416 coefficients ±2 cost 832 unit ADDs and no scaling. Their +replacement has 32 coefficients ±2, implemented by 64 unit ADDs. Thus the +saving is exactly 832−64=768, with no unpriced return or donor restoration. +All finite scalar counts are recounted from the actual joined event lists. +The retained native profile is +`{1:1282,2:58,3:86,4:104,5:48,6:24,8:8}`. Its rank sum is 2520. +There is no private allocation, copy, or erase. + +For an actual source-preserving downstream contract, the verifier also +appends PR3943's unchanged return adapter to the fused word. It restores +all X_i=x_i at FULL and all Y_i=x_i+y_i in their indexed hyperplanes, with +all 72 dirty helpers restored. This adapter adds its already-known 960 unit +ADDs, 104 halves, 104 doubles and native mass192. The complete returned module +therefore costs **5664 unit ADDs, 2720 halves, 2720 doubles and native mass2712**. +This is an integration check of the actual inherited consumer, not a new +192 lower bound or a claim that it is the cheapest source-preserving correction. +The direct PR3894 I−A correction has a different consumer; its own complete +matched scalar comparison and any optimality claim remain outside this result. +The internal-cut3940 variant above is the actual source-preserving improvement +proved here, with native2520 rather than this adapter route's2712. + +## Global gate and bounded stopping rule + +Under the unchanged favorable corrected two-axis contract of PR3954, calls +number208, per-call endpoint progress is2312, and the anchor allowance is10816. +Scalar fusion changes none of those native quantities. The necessary gate +remains + + 208*(2520-2312)-10816 = 32448 > 0. + +Thus the retained complete native bill remains2997696 over denominator2965248. +This local scalar improvement does not reopen that native gate or justify +further dependent kappa optimization. Newly proposed one-axis/global completion +contracts are separate research tasks; this package neither prices nor admits +them. No selected-frontier change, universal obstruction, global owner theorem, +or all-size admission is claimed. + +## Verification and controls + +The frozen PR3981, PR3943, PR3882 and PR3940 source exports are byte-identical to their +recorded original Git blobs, with explicit source-head and SHA256 metadata. +Only their named schedule/geometry builders are reused. A new sparse Fraction +interpreter evaluates the actual joined words and formal frames on all 280 +independent columns. It separately checks cut states, actual residual donors, +D=T[I B], data outputs, dirty returns, scalar lowering, and native subsequence. + +Eight semantic mutants reject: omitted compressed cleanup, cleanup before q +exists, reuse of old cleanup after source consumption, double cleanup, omission +of one unit update, failure to restore a quartered dirty donor, and correction +before late delivery, plus source-preserving cleanup after q has been +restored to x_J. Separate actual optimized CLI processes first validate +each private fixture and then reject Boolean/float receipt types, duplicate +keys, false savings, changed/missing source, or changed frozen tail bytes. +Read-only official exports are preserved; only private test copies become +writable. Assertions removable by Python optimization are not used to enforce +these checks. diff --git a/research/p104-fused-late-cleanup/README.md b/research/p104-fused-late-cleanup/README.md new file mode 100644 index 0000000000..cc18cfa455 --- /dev/null +++ b/research/p104-fused-late-cleanup/README.md @@ -0,0 +1,56 @@ +# P104 fused late delivery and compressed query cleanup + +Combine the actual PR3981 copy-free late FULL delivery with PR3943's early +correction and compressed Q cleanup. The source-bound composed word preserves +all 280 input columns, every endpoint row/frame, and all 72 arbitrary dirty +helper returns. **Unit ADDs fall from5472 to4704; native mass stays2520**, with +2616 halves and2616 doubles unchanged. No private storage is introduced. + +The point is an executable fusion of already credited ingredients. The +correction now creates residual `q=x_J+B x_N` while Q still equals `h-Dx`; +the actual extracted factorization `D=T[I B]` permits64 unit ADDs to restore Q +instead of the old832. The ordering and donor restoration are checked explicitly. +An actual source-preserving variant inserts the cleanup inside PR3940's fused +tail while q still exists:5856→5088 ADDs,2712 halves/doubles and native2520. +This preserves all X=x FULL and Y=x+y in their hyperplanes. The inherited +post-encoding return adapter also composes, costing5664 ADDs,2720 halves/doubles +and native2712; this is contextual integration, not a new optimality claim. + +See [PROOF.md](PROOF.md), [RESULT.json](RESULT.json), [VERIFY.json](VERIFY.json). +Run `python3.12 -B research/p104-fused-late-cleanup/verify.py` or the registered +package launcher. Native transport events are literally unchanged; prior phase +checks are inherited, not freshly replayed here. The old conditional two-axis +gate still fails32448. No supplier, all-size result or selected-frontier claim. + +## Provenance and overlap + +Canonical main20ecf2891d80b5acf18d980b2164fb44ea7faa90, priority6, fetched and +read at entry. The explicitly assigned task is this bounded composition; no +new dependent native/kappa search follows the failed global gate. The overlap +helper used702 open PR bodies including drafts, complete at08:30:14UTC on +2026-10-19, with49 possible matches. It had no Discussion cache; the root +coordinator separately checked live boards and posted the canonical scoped +claim at https://github.com/CrocSwap/integer-mult-bounds/pull/3954#issuecomment-6263112891 . +This is bounded overlap coverage, not a novelty certificate. The optional +selected-frontier orientation command could not run in this sparse checkout +because its unrelated selected ASSEMBLY archive is omitted; no full selected +replay or successful baseline command is claimed. + +Credit Chris R / Clear1nsight's PR3981 late delivery, PR3943 residual cleanup +and return adapter, PR3882 encoded correction, and PR3940's actual fused source-preserving tail. Unchanged builder exports record +original heads, Git blobs and hashes; they require no unavailable unmerged +commit in a main-only source export. Credit Rohan Arun's PR1972 witness, +Chafik Boukhalfa's PR1991 native realization, Adam Gall's PR1940 delivery, +icekylinx PR531 compiler and PR1862 interpreter lineage, and Josie Elliston, +Sagar Thakrar, Douglas Colkitt and Dominik Scholz's E8/P104 work. PR3954's gate, +PR3965's fixed-consumer audit, and PR3961/3962/3966's distinct boundary/coverage/ +gauge constraints remain credited. PR3956's adapter comparison is not repeated +as a new result. Prepared with substantial OpenAI Codex assistance. Apache-2.0. + +## Open next questions + +An independently proposed changed global caller needs its own physical, +entrance, ownership, coverage, precision and all-size invoice. First test that +caller's full gate with the exact native profile before optimizing scalar +cleanup further. The present result changes no native cost, so another local +scalar tweak cannot resolve the retained two-axis obstruction by itself. diff --git a/research/p104-fused-late-cleanup/RESULT.json b/research/p104-fused-late-cleanup/RESULT.json new file mode 100644 index 0000000000..f6d0546b42 --- /dev/null +++ b/research/p104-fused-late-cleanup/RESULT.json @@ -0,0 +1,176 @@ +{ + "actual3981_endpoint_preserved": true, + "all_input_columns": 280, + "all_size_admission": false, + "cleanup_factor": [ + [ + 2, + 2, + 2, + -2, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 2, + 2, + 2, + -2, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + -2, + -2, + 2 + ], + [ + 2, + 2, + 2, + 2, + 0, + 0, + 0, + 0 + ], + [ + 2, + 2, + -2, + -2, + 0, + 0, + 0, + 0 + ], + [ + 0, + -2, + 0, + -2, + 2, + 0, + -2, + 0 + ], + [ + -2, + 2, + -2, + 2, + 0, + 0, + 0, + 0 + ], + [ + 0, + -2, + 2, + 0, + -2, + 0, + 0, + -2 + ] + ], + "controls": { + "cleanup_before_residual": { + "changed_dirty_roles": 8, + "changed_roles": 8 + }, + "correction_before_late_delivery": "frame-or-owner rejection", + "double_cleanup": { + "changed_dirty_roles": 8, + "changed_roles": 8 + }, + "omit_compressed_cleanup": { + "changed_dirty_roles": 8, + "changed_roles": 8 + }, + "omit_one_unit": { + "changed_dirty_roles": 1, + "changed_roles": 1 + }, + "reuse_old_cleanup_after_source_consumption": "frame-or-owner rejection", + "unrestored_late_donor": { + "changed_dirty_roles": 1, + "changed_roles": 1 + } + }, + "cut_after_original_event": 3641, + "direct_source_preserving_fused_invoice": { + "double": 2712, + "half": 2712, + "positive_native_mass": 2520, + "unit_add": 5088 + }, + "direct_source_preserving_reference_invoice": { + "double": 2712, + "half": 2712, + "positive_native_mass": 2520, + "unit_add": 5856 + }, + "endpoint_sha256": "18d55eb50ebd4e18e7b895c2957acf1d6dd423e4f19576b33802ac915cca740d", + "full_native_subsequence_unchanged": true, + "fused_event_counts": { + "add": 3872, + "double": 120, + "half": 120, + "transport": 1610 + }, + "fused_formal_events": 5722, + "fused_invoice": { + "double": 2616, + "half": 2616, + "positive_native_mass": 2520, + "unit_add": 4704 + }, + "fused_program_sha256": "eab4ad564e440e3b9c7f3e0896c96770c13c2a058f4f13bc4c60e4c60973c1e7", + "inherited_source_preserving_return_invoice": { + "double": 2720, + "half": 2720, + "positive_native_mass": 2712, + "unit_add": 5664 + }, + "literal_old_cleanup_events": 416, + "native_profile": { + "1": 1282, + "2": 58, + "3": 86, + "4": 104, + "5": 48, + "6": 24, + "8": 8 + }, + "native_recipe_replay": false, + "new_cleanup_unit_adds": 64, + "old_cleanup_unit_adds": 832, + "q_cleanup_reads_from_actual_residual": true, + "reference_formal_events": 6074, + "reference_invoice": { + "double": 2616, + "half": 2616, + "positive_native_mass": 2520, + "unit_add": 5472 + }, + "restored_dirty_helpers": 72, + "schema_version": 1, + "scope": "actual3981 late delivery plus3943 compressed cleanup; exact finite formal-frame splice", + "selected_frontier_changed": false, + "source_preserving_fused_program_sha256": "e1a6f47ca82f6263fef77836ae019592c7b15c89f0e82479bf42c5f45fa4e4f2", + "source_preserving_internal_cut_after_tail_ops_without_lifts": 1360, + "source_preserving_late_cleanup_defective_dirty_roles": 8, + "two_axis_gap": 32448, + "unit_adds_saved_against3981": 768 +} diff --git a/research/p104-fused-late-cleanup/SOURCES.json b/research/p104-fused-late-cleanup/SOURCES.json new file mode 100644 index 0000000000..b32233a6eb --- /dev/null +++ b/research/p104-fused-late-cleanup/SOURCES.json @@ -0,0 +1,64 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "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/p104-native-channel/PROOF.md", + "usage": "input", + "git_blob": "a69311b74f74a2f8e8f411c1451baacd9bacddce", + "sha256": "5d743145d389ffdfaffc66096fa7e32c7155b18f73d74755403151d0435bb94c" + }, + { + "path": "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "usage": "input", + "git_blob": "86beaf424e9f0f800ae3a62797d94ec9386b7706", + "sha256": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e" + } + ], + "source_exports": [ + { + "path": "inputs/pr3981_verify.py", + "sha256": "7a4f8953215ec9d39fa3a612ab79dc6c9f8b6f521178f89698665245772bc7a1", + "upstream_head": "cdb7dcf3f7e5f860714a1b12df4c7a5157d8ae3d", + "upstream_path": "research/p104-dirty-catalysis/verify.py", + "upstream_git_blob": "1e0d8323598ea537b07d02945f275b42e93e6913", + "usage": "Unchanged frozen builder only; new independent full-word evaluator." + }, + { + "path": "inputs/pr3943_verify.py", + "sha256": "c662bed19551803e73d1531a789f43d8499b3a61172df87650aebef5ae656821", + "upstream_head": "2cba526a4ebe0ef6c3c0143498adcf67dca97941", + "upstream_path": "research/p104-residual-consumer/verify.py", + "upstream_git_blob": "a63800dadcfc29ecef39027f5d3d0f42b7d010bf", + "usage": "Unchanged frozen builder only; new independent full-word evaluator." + }, + { + "path": "inputs/pr3882_verify.py", + "sha256": "599274dbff5eefd8800e4cf39a25a7675edaaed93dc1490692bdfdbfb703ec3d", + "upstream_head": "9d56eeedbed5e3e9bbbc8c189d66f14cf15b6067", + "upstream_path": "research/p104-role-exchange-residue/verify.py", + "upstream_git_blob": "093e21df60f5f1a02aaa1495da22d881e0c53fa1", + "usage": "Unchanged frozen builder only; new independent full-word evaluator." + }, + { + "path": "inputs/pr3940_verify.py", + "sha256": "f25cfc3ff2a42d4c7a5456d8836deb45ac61c6ae8cfd56ee73f6c8b92f28d3b7", + "upstream_head": "51ba88c007cfbcc3d9cf22dd321f5224be3a5bb1", + "upstream_path": "research/p104-role-exchange-caller-audit/verify.py", + "upstream_git_blob": "11ed66aa8451016e4cc871d419a46a26810c4bac", + "usage": "Unchanged source-preservingfused tailbuilder anditsliteralinternalcut; independentwholewordevaluation." + } + ] +} diff --git a/research/p104-fused-late-cleanup/TASK.json b/research/p104-fused-late-cleanup/TASK.json new file mode 100644 index 0000000000..a08926c297 --- /dev/null +++ b/research/p104-fused-late-cleanup/TASK.json @@ -0,0 +1,88 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "p104-side-correction", + "question": "Can the proposed P104 joint endpoint flags be realized by a chronological correction program with coefficients, dirty restoration and an affordable complete bill?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/p104-native-channel/README.md", + "research/p104-native-channel/PROOF.md", + "docs/research/community-efficient1000-review.md", + "research/p104-joint-unit-flags/README.md" + ], + "methods": [ + "Construct one side-correction word at an explicit chronological cut with the needed frames still available.", + "Derive a lower bound on the side correction and hosting costs that decides whether this channel can beat the selected budget." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the revision-6 family record and #2981 static joint flags, alongside the reviewed #1991 channel. #2981 is an author-checked source archive, not an independently validated executable correction or a refutation of program-level lifetime floors.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "After checking live handoffs, pin one named collection from #2981 and attach acquisition/delivery times, source dependencies and coefficient requirements. Test legal access and arbitrary dirty restoration; price any completion against the full channel/endpoint/hosting allowance. Stop with the exact missing implication or a scoped counterexample rather than expanding the static cover census.", + "bottleneck_link": "Completing an already realized changed channel tests a concrete construction opportunity, instead of refining the incumbent packing. A positive local result still needs global and all-size admission.", + "allowed_variations": [ + "One correction factorization, one chronological cut, or one explicit hosting obstruction.", + "A changed correction schedule with an updated full bill and native frame contract." + ], + "scope_change_triggers": [ + "Recompiling the already certified low-rank channel without closing a new obligation.", + "Treating a pending ancestor, local histogram or unpriced side correction as an admitted global supplier.", + "Repeating a correction or physical conversion already supplied by a pending follow-up without adding independent coverage or a different unresolved obligation.", + "Repeating the 208-flag static matching or calling a static nested cover a chronological correction program. Independent audit of that certificate is distinct and remains useful." + ], + "overlap_terms": [ + "P104", + "I-G/2", + "side correction", + "native channel", + "1972", + "1991", + "2586", + "endpoint transport", + "physical dual", + "relay composition", + "2981", + "joint unit flags", + "acquisition delivery", + "static nesting" + ], + "existing_checks": [ + { + "scope": "PR #2981 reports static joint endpoint flags and a matching of 208 departure and arrival flags; archival intake is not independent verification.", + "evidence": "research/p104-joint-unit-flags/README.md", + "remaining": "Independent flag check and a chronological coefficient program with dirty restoration and a complete cost.", + "status": "author-checked", + "source_commit": "3d24b92d8ba057b57cb2d480170ec407520e6882", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Fuse actual3981 late FULL delivery with3943 residual query cleanup; execute encoded3882 and source-preserving3940 consumers at their legal residual cuts, reducing each by768scalarADDs withnative2520.", + "scope_change_reason": "User explicitly assigned one bounded composition of two compatible existing local constructions.", + "bottleneck_link": "Verifies whether768scalarADD saving survives coupling to actualcopy-free producer/consumer chronology; no nativegate expansion.", + "budget_minutes": 60, + "stop_rule": "Stop after exactword/native-subsequence/dirty proof andcompleteinvoice; oldtwoaxis nativegate remainsfailed.", + "outcome": "partial", + "evidence": "PROOF.md, RESULT.json, independent280-column joinedword/wholeframe comparisons forbothactualconsumers andoptimizedCLIcontrols.", + "author": "Chris R / Clear1nsight with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for literal source extraction, independent evaluator, proof and publication.", + "open_questions": [ + { + "question": "Does a separately proposed changed global caller admit this exactlocalinterface?", + "why_it_matters": "Scalar fusion preserves2520native mass andcannotrepairretained32448gate.", + "first_step": "Writecallerphysical/ownership/coverage/allsizeledger andfullgate beforefurther dependentoptimization.", + "blocked_by": "No newcalleradmissionprovedinthispackage." + } + ] +} diff --git a/research/p104-fused-late-cleanup/VERIFY.json b/research/p104-fused-late-cleanup/VERIFY.json new file mode 100644 index 0000000000..a5d049a6d9 --- /dev/null +++ b/research/p104-fused-late-cleanup/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-native-channel/PROOF.md", + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Both actual280-column fused/reference words; actualsourcecleanupfactor,72dirtyreturns,fullnative-subsequences,completeinvoices,and8semanticfaults." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "SamecompletechecksunderPythonoptimization." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_controls.py" + ], + "timeout_seconds": 300, + "checks": "SevenactualoptimizedCLIprivatefixtures: validbaselinefirst,typed/duplicate/falsecost/source/exportfaultrejections." + } + ] +} diff --git a/research/p104-fused-late-cleanup/inputs/pr3882_verify.py b/research/p104-fused-late-cleanup/inputs/pr3882_verify.py new file mode 100644 index 0000000000..093e21df60 --- /dev/null +++ b/research/p104-fused-late-cleanup/inputs/pr3882_verify.py @@ -0,0 +1,291 @@ +#!/usr/bin/env python3 +"""Exact P104 changed-boundary experiment. Apache-2.0; see README for scope.""" +from __future__ import annotations + +import argparse +import hashlib +import itertools +import json +from collections import Counter +from fractions import Fraction as F +from pathlib import Path + +HERE = Path(__file__).resolve().parent +REPO = HERE.parents[1] +BASE = "20ecf2891d80b5acf18d980b2164fb44ea7faa90" +F0 = [[0,0,0,0,0,0,2,-2],[0,0,0,0,0,0,2,2], + [0,0,0,0,2,-2,0,0],[0,0,0,0,2,2,0,0], + [0,0,2,-2,0,0,0,0],[0,0,2,2,0,0,0,0], + [2,-2,0,0,0,0,0,0],[2,2,0,0,0,0,0,0]] +PUNCTURE_C = [[0,0,0,0,0,2,-2,0],[0,0,0,2,-2,0,0,0], + [0,2,-2,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1], + [1,-1,-1,1,1,1,1,1],[1,1,1,-1,-1,1,1,1], + [1,1,1,1,1,-1,-1,1],[2,0,0,0,0,0,0,-2]] +SOURCE_HASHES = { + "research/p104-native-channel/inputs/P104-FIXTURE.json": + "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4", + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json": + "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e", + "research/p104-native-channel/PROOF.md": + "5d743145d389ffdfaffc66096fa7e32c7155b18f73d74755403151d0435bb94c", +} + + +def need(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def load(path: Path): + def unique(pairs): + out = {} + for key, value in pairs: + need(key not in out, f"duplicate JSON key: {key}") + out[key] = value + return out + return json.loads(path.read_text(), object_pairs_hook=unique) + + +def encoded(value) -> bytes: + return (json.dumps(value, sort_keys=True, separators=(",", ":")) + "\n").encode() + + +def digest(value) -> str: + return hashlib.sha256(encoded(value)).hexdigest() + + +def geometry(): + roots = set() + for i, j in itertools.combinations(range(8), 2): + for sign in (-1, 1): + row = [0] * 8 + row[i], row[j] = 2, 2 * sign + roots.add(tuple(row)) + for tail in itertools.product((-1, 1), repeat=7): + if sum(t < 0 for t in tail) % 2 == 0: + roots.add((1,) + tail) + removed = {tuple(r) for r in F0 + PUNCTURE_C} + need(len(roots) == 120 and len(removed) == 16 and removed <= roots, + "root universe or puncture changed") + ports = sorted(roots - removed) + R = list(map(list, zip(*ports))) + need(len(ports) == 104, "wrong port count") + for a in range(8): + for b in range(8): + need(sum(R[a][i] * R[b][i] for i in range(104)) == 104 * (a == b), + "RR^t is not 104 I") + J = [] + for a, b in ((0, 2), (1, 3), (4, 6), (5, 7)): + for sign in (-1, 1): + r = [0] * 8 + r[a], r[b] = 2, 2 * sign + J.append(ports.index(tuple(r))) + J.sort() + N = [i for i in range(104) if i not in J] + A = [[F(sum(x*y for x,y in zip(r,s)), 8) for s in ports] for r in ports] + need(all(A[i][j] == (i == j) for i in J for j in J), "J not orthogonal") + B = [[A[j][i] for i in N] for j in J] + need(all(v in (F(-1,2), 0, F(1,2)) for row in B for v in row), "B alphabet") + need(sum(v != 0 for row in B for v in row) == 384, "B support") + for a, i in enumerate(N): + for b, k in enumerate(N): + need(A[i][k] == sum(B[j][a] * B[j][b] for j in range(8)), + "A_NN != B^t B") + return R, A, J, N, B + + +def source_binding(J): + data = {} + for path, expected in SOURCE_HASHES.items(): + raw = (REPO / path).read_bytes() + need(hashlib.sha256(raw).hexdigest() == expected, f"source hash: {path}") + data[path] = raw + fixture = json.loads(data[next(iter(SOURCE_HASHES))]) + section = fixture["section4_explicit_P104"] + need(section["F0"] == F0 and section["C"] == PUNCTURE_C, "source extraction") + word = json.loads(data["research/p104-native-channel/inputs/LOWRANK-WITNESS.json"]) + full = [1 << i for i in range(9)] + final = word["final_frames"] + need(all(final[f"X{i}"] == full for i in range(104)), "source exit frame") + helpers = [f"Q{i}" for i in range(8)] + [f"G{i}" for i in range(32)] + [f"D{i}" for i in range(32)] + need(all(final[h] == full for h in helpers), "dirty helper exit frames") + need(all(len(final[f"Y{i}"]) == 8 and binary_rank(final[f"Y{i}"]) == 8 + for i in range(104)), "target exit hyperplane") + proof = data["research/p104-native-channel/PROOF.md"] + need(b"y_t + sum_s x_s/2" in proof, "inherited channel statement") + return {"bound_sources": len(data), "target_frame_digest": digest([final[f"Y{i}"] for i in range(104)]), + "pivot_input_frames": [word["initial_frames"][f"X{i}"] for i in J]} + + +def binary_rank(rows): + pivots = {} + for row in rows: + need(type(row) is int and 0 < row < 512, "invalid binary vector") + while row: + k = row.bit_length() - 1 + if k in pivots: + row ^= pivots[k] + else: + pivots[k] = row + break + return len(pivots) + + +def program(J, N, B): + ops = [("lift", 104+i) for i in range(104)] + for a, i in enumerate(N): + ops.append(("half", i)) + for b, j in enumerate(J): + if B[b][a]: + s = int(2 * B[b][a]) + ops.extend([("add", j, i, s), ("add", 104+j, i, -s)]) + ops.append(("double", i)) + for b, j in enumerate(J): + ops.append(("half", j)) + for a, i in enumerate(N): + if B[b][a]: + ops.append(("add", i, j, -int(2 * B[b][a]))) + ops.append(("double", j)) + ops.extend(("add", i, 104+i, 1) for i in N) + ops.extend(("drop", i) for i in N) + ops.extend(("drop", 104+j) for j in J) + return ops + + +def execute(A, ops): + # The 72 arbitrary dirty inputs are explicit independent columns, not zero. + state = [[F(i == j) for j in range(280)] for i in range(280)] + for i in range(104): + state[104+i][:104] = A[i][:] + frames = [9]*104 + [8]*104 + [9]*72 + max_denominator = max(x.denominator for row in state for x in row) + peak_row_norm = max(sum(abs(x) for x in row) for row in state) + for op in ops: + kind, target = op[:2] + need(type(target) is int and 0 <= target < 208, "helper mutation or bad register") + if kind == "lift": + need(frames[target] == 8, "lift source frame") + frames[target] = 9 + continue + if kind == "drop": + need(frames[target] == 9, "drop source frame") + frames[target] = 8 + continue + need(frames[target] == 9, "arithmetic target not FULL") + if kind == "add": + source, sign = op[2:] + need(source != target and 0 <= source < 208 and frames[source] == 9, + "arithmetic source or frame") + need(type(sign) is int and sign in (-1, 1), "ADD coefficient") + state[target] = [x + sign*y for x,y in zip(state[target], state[source])] + else: + need(kind in ("half", "double"), "unknown operation") + scalar = F(1, 2) if kind == "half" else F(2) + state[target] = [scalar*x for x in state[target]] + max_denominator = max(max_denominator, *(x.denominator for x in state[target])) + peak_row_norm = max(peak_row_norm, sum(abs(x) for x in state[target])) + return state, frames, max_denominator, peak_row_norm + + +def mod_rank(matrix, prime=3): + a = [[int(F(x).numerator * pow(F(x).denominator, -1, prime) % prime) + for x in row] for row in matrix] + rank = 0 + for col in range(len(a[0])): + pivot = next((i for i in range(rank, len(a)) if a[i][col]), None) + if pivot is None: + continue + a[rank], a[pivot] = a[pivot], a[rank] + inv = pow(a[rank][col], -1, prime) + a[rank] = [(v*inv) % prime for v in a[rank]] + for i in range(rank+1, len(a)): + c = a[i][col] + if c: + a[i] = [(x-c*y) % prime for x,y in zip(a[i], a[rank])] + rank += 1 + if rank == len(a): + break + return rank + + +def verify_endpoint(state, frames, A, J, N, B): + for i in range(104): + target = 104+i if i in J else i + expected = [F(k in (i,104+i)) for k in range(280)] + need(state[target] == expected and frames[target] == 8, f"sum endpoint {i}") + for b,j in enumerate(J): + expected = [F(k == j) for k in range(280)] + for a,i in enumerate(N): + expected[i] = B[b][a] + need(state[j] == expected and frames[j] == 9, f"q residual {j}") + for i in N: + expected = [F(k == 104+i) for k in range(280)] + expected[:104] = A[i][:] + need(state[104+i] == expected and frames[104+i] == 9, f"v residual {i}") + for i in range(208,280): + need(state[i] == [F(i == k) for k in range(280)] and frames[i] == 9, + f"dirty helper {i}") + + +def calculate(): + R,A,J,N,B = geometry() + ops = program(J,N,B) + state,frames,den,norm = execute(A,ops) + verify_endpoint(state,frames,A,J,N,B) + # Separate endpoint formula and explicit inverse, not the gate interpreter. + xs = [] + for a,i in enumerate(N): + w = state[i] + v = state[104+i] + xs.append([w[k]-v[k]+sum(B[b][a]*state[j][k] for b,j in enumerate(J)) + for k in range(280)]) + for a,i in enumerate(N): + need(xs[a] == [F(k == i) for k in range(280)], "inverse x_N") + for b,j in enumerate(J): + restored = [state[j][k]-sum(B[b][a]*xs[a][k] for a in range(96)) + for k in range(280)] + need(restored == [F(k == j) for k in range(280)], "inverse x_J") + C = [[F(i == j)-A[i][j] for j in range(104)] for i in range(104)] + naive = [[F(i == j) for j in range(104)]+[F(i == j) for j in range(104)] + for i in range(104)] + naive += [A[i][:]+[F(i == j) for j in range(104)] for i in range(104)] + need(mod_rank(C) == 96 and mod_rank(naive) == 200, "mod-three obstruction") + need(mod_rank([r[:208] for r in state[:208]]) == 208, "repaired rank") + need(mod_rank(R) == 8, "root rank modulo three") + counts = Counter(op[0] for op in ops) + need(counts == Counter(add=1248,half=104,double=104,lift=104,drop=104), "invoice") + need(den == 4, "two-bit transient bound") + return { + "schema_version": 1, "base_commit": BASE, "scope": "changed source-consuming boundary; no supplier or kappa", + "ports": 104, "pivots": J, "nonpivots": N, "root_nonzeros": sum(v != 0 for r in R for v in r), + "B_nonzeros": 384, "program_sha256": digest(ops), "endpoint_sha256": digest([[str(v) for v in r] for r in state]), + "operation_counts": dict(sorted(counts.items())), "total_tail_events": len(ops), + "tail_native_profile": {"1": 208}, "inherited_channel_mass": 2368, "combined_mass": 2576, + "combined_native_profile": [1282,58,86,104,48,24,8,8], + "scalar_real_adds_at_512_complex_words": 1248*1024, + "scalar_real_halves_at_512_complex_words": 104*1024, + "scalar_real_doubles_at_512_complex_words": 104*1024, + "maximum_scalar_coefficient_denominator": den, "maximum_scalar_row_l1": str(norm), + "sum_outputs": 104, "dirty_helpers_restored": 72, + "rank_C_mod3": 96, "rank_naive_mod3": 200, "rank_repaired_mod3": 208, + "minimum_replaced_residual_arrays_in_stated_linear_model": 8, + "det_naive": str(12**8), "native_lowering_replayed": False, "complete_consumer_admitted": False, + } + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--algebra-only", action="store_true", help="Do not claim full-repository source authentication.") + args = parser.parse_args() + result = calculate() + need(encoded(result) == encoded(load(HERE/"RESULT.json")), "typed result mismatch") + if args.algebra_only: + marker = "PASS_P104_ROLE_EXCHANGE_ALGEBRA_ONLY" + else: + print(json.dumps(source_binding(result["pivots"]), sort_keys=True)) + marker = "PASS_P104_ROLE_EXCHANGE_SOURCE_BOUND" + print(f"{marker} replaced=8 sums=104 dirt=72 tail_H1=208 result={digest(result)}") + + +if __name__ == "__main__": + main() diff --git a/research/p104-fused-late-cleanup/inputs/pr3940_verify.py b/research/p104-fused-late-cleanup/inputs/pr3940_verify.py new file mode 100644 index 0000000000..11ed66aa84 --- /dev/null +++ b/research/p104-fused-late-cleanup/inputs/pr3940_verify.py @@ -0,0 +1,422 @@ +#!/usr/bin/env python3 +"""Bounded P104 caller-cut audit. Apache-2.0; see README for scope and credit.""" +from __future__ import annotations + +import argparse +from collections import Counter +from fractions import Fraction as F +import gzip +import hashlib +import itertools +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +FULL = tuple(1 << i for i in range(9)) +FIELDS = ([f"X{i}" for i in range(104)] + [f"Y{i}" for i in range(104)] + + [f"Q{i}" for i in range(8)] + [f"G{i}" for i in range(32)] + + [f"D{i}" for i in range(32)]) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def load(path): + def unique(pairs): + result = {} + for key, value in pairs: + need(key not in result, "duplicate JSON key") + result[key] = value + return result + raw = path.read_bytes() + if path.suffix == ".gz": + raw = gzip.decompress(raw) + return json.loads(raw, object_pairs_hook=unique) + + +def canonical(value): + return (json.dumps(value, sort_keys=True, separators=(",", ":")) + "\n").encode() + + +def digest(value): + return hashlib.sha256(canonical(value)).hexdigest() + + +def blob(raw): + return hashlib.sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw).hexdigest() + + +def space(vectors): + need(all(type(v) is int and 0 < v < 512 for v in vectors), "binary frame vector") + rows = [v for v in vectors if v] + pivot = 0 + for bit in range(8, -1, -1): + found = next((i for i in range(pivot, len(rows)) if (rows[i] >> bit) & 1), None) + if found is None: + continue + rows[pivot], rows[found] = rows[found], rows[pivot] + for i in range(len(rows)): + if i != pivot and (rows[i] >> bit) & 1: + rows[i] ^= rows[pivot] + pivot += 1 + return tuple(sorted(rows[:pivot])) + + +def authenticate(): + pins = load(HERE / "PREDECESSORS.json")["files"] + pins += [row for row in load(HERE / "SOURCES.json")["files"] if row["usage"] == "input"] + result = {} + for row in pins: + path = ROOT / row["path"] + need(not path.is_symlink(), "source symlink") + raw = path.read_bytes() + need(hashlib.sha256(raw).hexdigest() == row["sha256"], "source hash: " + row["path"]) + need(blob(raw) == row["git_blob"], "source blob: " + row["path"]) + result[row["path"]] = row["sha256"] + return result + + +def geometry(): + fixture = load(ROOT / "research/p104-native-channel/inputs/P104-FIXTURE.json") + g = load(HERE / "inputs/3882-geometry.json") + section = fixture["section4_explicit_P104"] + need(section["F0"] == g["F0"] and section["C"] == g["C"], "puncture source") + roots = set() + for a, b in itertools.combinations(range(8), 2): + for sign in (-1, 1): + r = [0] * 8 + r[a], r[b] = 2, 2 * sign + roots.add(tuple(r)) + for signs in itertools.product((-1, 1), repeat=7): + if sum(s < 0 for s in signs) % 2 == 0: + roots.add((1,) + signs) + ports = sorted(roots - {tuple(r) for r in g["F0"] + g["C"]}) + need(len(roots) == 120 and len(ports) == 104, "root count") + A = [[F(sum(x*y for x, y in zip(r, s)), 8) for s in ports] for r in ports] + J = load(HERE / "inputs/3882-result.json")["pivots"] + N = [i for i in range(104) if i not in J] + need(J == [0, 1, 3, 6, 22, 31, 93, 103], "pivot order") + B = [[A[j][i] for i in N] for j in J] + need(sum(v != 0 for row in B for v in row) == 384, "B support") + need(all(v in (F(-1, 2), 0, F(1, 2)) for row in B for v in row), "B alphabet") + need(all(A[j][k] == int(j == k) for j in J for k in J), "pivot block") + need(all(sum(B[a][i]*B[b][i] for i in range(96)) == 12*int(a == b) + for a in range(8) for b in range(8)), "B row rank witness") + for a, i in enumerate(N): + for b, k in enumerate(N): + need(A[i][k] == sum(B[t][a]*B[t][b] for t in range(8)), "Schur block") + return A, J, N, B + + +def plus(a, b, coefficient=F(1)): + out = dict(a) + for key, value in b.items(): + out[key] = out.get(key, F(0)) + coefficient * value + if not out[key]: + del out[key] + return out + + +def source_channel(A): + word = load(ROOT / "research/p104-native-channel/inputs/LOWRANK-WITNESS.json") + state = {name: {i: F(1)} for i, name in enumerate(FIELDS)} + frames = {name: tuple(value) for name, value in word["initial_frames"].items()} + counts, profile = Counter(), Counter() + for op in word["program"]: + kind, target = op[:2] + counts[kind] += 1 + if kind == "transport": + old, new, rank = tuple(op[2]), tuple(op[3]), op[4] + need(space(frames[target]) == space(old) and rank == abs(len(new)-len(old)), "source transport") + need(len(space(old)) == len(old) and len(space(new)) == len(new), "source frame basis") + frames[target] = new + profile[rank] += 1 + elif kind == "add": + source, c, frame = op[2], F(op[3]), tuple(op[4]) + need(space(frames[target]) == space(frames[source]) == space(frame), "source ADD frame") + state[target] = plus(state[target], state[source], c) + elif kind == "zero": + need(target == "C" and target not in state, "owned private creation") + state[target], frames[target] = {}, tuple(op[2]) + elif kind == "copy": + need(target == "C" and not state[target], "owned private COPY destination") + need(space(frames[target]) == space(frames[op[2]]) == space(op[3]), "source COPY frame") + state[target] = dict(state[op[2]]) + elif kind == "erase": + # Inherited owned live-copy disposal; deliberately not a zero-erasure assertion. + need(target == "C" and space(frames[target]) == space(op[2]), "private disposal") + del state[target], frames[target] + else: + raise ValueError("unknown source instruction") + for i, name in enumerate(FIELDS): + expected = {i: F(1)} + if name.startswith("Y"): + expected.update({j: value for j, value in enumerate(A[int(name[1:])]) if value}) + need(state[name] == expected, "source endpoint: " + name) + need(space(frames[name]) == space(word["final_frames"][name]), "source final frame") + if name.startswith("Y"): + need(len(space(frames[name])) == 8, "channel exit target hyperplane") + else: + need(space(frames[name]) == space(FULL), "channel exit source/helper FULL") + need(len(word["program"]) == 4058 and sum(r*n for r, n in profile.items()) == 2368, + "source invoice") + progress = sum(len(word["final_frames"][name])-len(word["initial_frames"][name]) + for name in FIELDS) + need(progress == 2312, "persistent source boundary progress") + return state, frames, {"events": 4058, "operation_counts": dict(counts), + "profile": dict(sorted(profile.items())), "mass": 2368, + "persistent_progress": progress, "private_copy_mass": 2368-progress} + + +def seed(A): + state = [{i: F(1)} for i in range(280)] + for i, row in enumerate(A): + state[104+i].update({j: value for j, value in enumerate(row) if value}) + return state + + +def pivot_stream(J, N, B, restore=False): + ops = [] + for a, i in enumerate(N): + ops.append(["half", i]) + for b, j in enumerate(J): + if B[b][a]: + sign = int(2*B[b][a]) + ops.append(["add", j, i, -sign if restore else sign]) + if not restore: + ops.append(["add", 104+j, i, -sign]) + ops.append(["double", i]) + return ops + + +def scatter(J, N, B, destination): + ops = [] + for b, j in enumerate(J): + ops.append(["half", j]) + for a, i in enumerate(N): + if B[b][a]: + ops.append(["add", destination+i, j, -int(2*B[b][a])]) + ops.append(["double", j]) + return ops + + +def role_tail(J, N, B): + ops = [["lift", 104+i] for i in range(104)] + ops += pivot_stream(J, N, B) + scatter(J, N, B, 0) + ops += [["add", i, 104+i, 1] for i in N] + ops += [["drop", i] for i in N] + [["drop", 104+j] for j in J] + return ops + + +def return_adapter(J, N, B): + ops = [["lift", i] for i in N] + [["add", 104+i, i, -1] for i in N] + ops += scatter(J, N, B, 104) + for a, i in enumerate(N): + ops.append(["half", 104+i]) + for b, j in enumerate(J): + if B[b][a]: + ops.append(["add", j, 104+i, int(2*B[b][a])]) + ops.append(["double", 104+i]) + for i in N: + ops += [["add", i, 104+i, -1], ["add", 104+i, i, 1], ["add", i, 104+i, -1]] + return ops + [["drop", 104+i] for i in N] + + +def inverse_reader(): + return ([["lift", 104+i] for i in range(104)] + + [["add", i, 104+i, -1] for i in range(104)] + + [["drop", 104+i] for i in range(104)]) + + +def fused(J, N, B, consume=False): + ops = [["lift", 104+i] for i in range(104)] + ops += pivot_stream(J, N, B) + scatter(J, N, B, 104) + ops += pivot_stream(J, N, B, restore=True) + ops += [["add", 104+i, i, 1] for i in N] + if consume: + ops += [["add", i, 104+i, -1] for i in range(104)] + return ops + [["drop", 104+i] for i in range(104)] + + +def direct_baseline(correction, consume=False, retime=False): + rows, ops = correction["rows"], [] + if retime: + ops += [["lift", 104+i] for i in range(104)] + ops += [["half", i] for i in range(104)] + for row in rows: + ops += [["add", 104+row["target"], i, int(2*F(c))] for i, c in row["terms"]] + ops += [["double", i] for i in range(104)] + if consume: + ops += [["add", i, 104+i, -1] for i in range(104)] + return ops + [["drop", 104+i] for i in range(104)] + for row in rows: + t = 104 + row["target"] + ops.append(["lift", t]) + for i, c in row["terms"]: + ops.append(["scaled_add", t, i, c]) + ops.append(["drop", t]) + return ops + (inverse_reader() if consume else []) + + +def replay(A, ops, final): + state, frames = seed(A), [FULL]*104 + [None]*104 + [FULL]*72 + for i in range(104): + frames[104+i] = tuple(final[f"Y{i}"]) + counts, peak, holds = Counter(), sum(map(len, frames)), 0 + max_den, max_norm = 1, F(0) + for row in state: + max_den = max(max_den, *(v.denominator for v in row.values())) + max_norm = max(max_norm, sum(map(abs, row.values()))) + for op in ops: + kind, t = op[:2] + need(type(t) is int and 0 <= t < 208, "public arithmetic target") + counts[kind] += 1 + if kind == "lift": + need(len(frames[t]) == 8, "lift entrance") + frames[t] = FULL + elif kind == "drop": + need(frames[t] == FULL, "drop entrance") + frames[t] = tuple(final[f"Y{t % 104}"]) + else: + need(frames[t] == FULL, "arithmetic target frame") + if kind in ("add", "scaled_add"): + s, coefficient = op[2], F(op[3]) + need(type(s) is int and 0 <= s < 208 and s != t, "arithmetic source") + need(frames[s] == FULL, "arithmetic source frame") + need(kind != "add" or coefficient in (-1, 1), "unit ADD") + state[t] = plus(state[t], state[s], coefficient) + else: + need(kind in ("half", "double"), "unknown arithmetic") + c = F(1, 2) if kind == "half" else F(2) + state[t] = {k: c*v for k, v in state[t].items()} + max_den = max(max_den, *(v.denominator for v in state[t].values())) + max_norm = max(max_norm, sum(map(abs, state[t].values()))) + width = sum(map(len, frames)) + peak, holds = max(peak, width), holds + width + return state, frames, {"events": len(ops), "operation_counts": dict(sorted(counts.items())), + "added_H1": counts["lift"]+counts["drop"], + "maximum_coefficient_denominator": max_den, + "maximum_row_l1": str(max_norm), "peak_persistent_frame_coordinates": peak, + "post_event_persistent_frame_coordinate_holds": holds} + + +def endpoint(state, frames, final, consume=False): + for i in range(104): + want_x = {104+i: F(-1)} if consume else {i: F(1)} + need(state[i] == want_x and frames[i] == FULL, "X caller endpoint") + need(state[104+i] == {i: F(1), 104+i: F(1)}, "Y caller endpoint") + need(frames[104+i] == tuple(final[f"Y{i}"]), "Y caller return frame") + for i in range(208, 280): + need(state[i] == {i: F(1)} and frames[i] == FULL, "dirty helper return") + + +def encode_state(state): + return [[[k, str(v)] for k, v in sorted(row.items())] for row in state] + + +def check_baseline(A): + c = load(HERE / "inputs/3894-correction.json") + need(len(c["rows"]) == 104, "baseline row count") + signs = Counter() + for i, row in enumerate(c["rows"]): + need(type(row["target"]) is int and row["target"] == i, "baseline target order") + terms = {j: F(v) for j, v in row["terms"]} + need(len(terms) == len(row["terms"]) == 48, "baseline row support") + need(terms == {j: F(i == j)-v for j, v in enumerate(A[i]) if F(i == j)-v}, + "baseline exact correction coefficients") + signs.update(v for _, v in row["terms"]) + need(signs == {"-1/2": 3376, "1/2": 1616}, "baseline signs") + word = load(ROOT / "research/p104-native-channel/inputs/LOWRANK-WITNESS.json") + need(c["target_output_frames"] == {str(i): word["final_frames"][f"Y{i}"] + for i in range(104)}, "baseline endpoint frame binding") + return c + + +def calculate(): + hashes = authenticate() + caller = (ROOT / "notes/copied-centers-complex.tex").read_text() + need("maps $(x,y)$ to $(-y,x+y)$" in caller, "retained caller equation") + need("Its copy, addition and erasure are paid local work".lower() in caller.lower() + or "its copy, addition and erasure are paid local work" in caller, + "retained caller payment clause") + A, J, N, B = geometry() + _, _, source = source_channel(A) + word = load(ROOT / "research/p104-native-channel/inputs/LOWRANK-WITNESS.json") + final = word["final_frames"] + baseline = check_baseline(A) + old = role_tail(J, N, B) + need(digest(old) == load(HERE / "inputs/3882-result.json")["program_sha256"], "PR3882 schedule") + encoded, encoded_frames, encoded_bill = replay(A, old, final) + for i in range(104): + target = 104+i if i in J else i + need(encoded[target] == {i:F(1),104+i:F(1)} and len(encoded_frames[target]) == 8, + "PR3882 sum and frame") + for b, j in enumerate(J): + q = {j:F(1)} + q.update({i:B[b][a] for a, i in enumerate(N) if B[b][a]}) + need(encoded[j] == q and encoded_frames[j] == FULL, "PR3882 q boundary") + entrance = seed(A) + for i in N: + need(encoded[104+i] == entrance[104+i] and encoded_frames[104+i] == FULL, + "PR3882 v_N boundary") + for i in range(208, 280): + need(encoded[i] == {i:F(1)} and encoded_frames[i] == FULL, "PR3882 dirty boundary") + restoration_floor = sum(abs(len(encoded_frames[i])-9) for i in range(104)) + restoration_floor += sum(abs(len(encoded_frames[104+i])-8) for i in range(104)) + programs = { + "role_then_fixed_return": old + return_adapter(J, N, B), + "role_return_then_reader": old + return_adapter(J, N, B) + inverse_reader(), + "fused_return": fused(J, N, B), + "fused_return_and_reader": fused(J, N, B, True), + "baseline_3894": direct_baseline(baseline), + "baseline_3894_then_reader": direct_baseline(baseline, True), + "retimed_lowered_baseline": direct_baseline(baseline, False, True), + "retimed_lowered_baseline_and_reader": direct_baseline(baseline, True, True), + } + results = {} + for name, ops in programs.items(): + state, frames, bill = replay(A, ops, final) + endpoint(state, frames, final, "reader" in name) + bill["endpoint_sha256"], bill["program_sha256"] = digest(encode_state(state)), digest(ops) + bill["combined_channel_mass"] = 2368 + bill["added_H1"] + bill["bare_280_role_M0"] = str(F(bill["combined_channel_mass"], 9*280)) + results[name] = bill + return {"schema_version": 1, "status": "PASS_P104_ROLE_EXCHANGE_CALLER_AUDIT", + "sources": hashes, "source_channel": source, "programs": results, + "encoded_boundary": {"endpoint_sha256":digest(encode_state(encoded)), **encoded_bill}, + "fixed_location_restoration_minimum_added_rank": restoration_floor, + "restoration_constructed_added_rank": results["role_then_fixed_return"]["added_H1"]-encoded_bill["added_H1"], + "naive_residual_as_source_error_rank_over_Q": 104, + "ports": 104, "independent_inputs": 280, "dirty_helpers": 72, + "scalar_saving_against_retimed_lowered_baseline": 3360, + "additional_halves_and_doubles_each": 96, + "unchanged_paired_chain": {"stages": 9, "width": 73, "families": 832, + "persistent_progress_per_call": 2312, "remaining_coverage": 39096, + "lower_mass": 9*2576+39096, "capacity": 73*832, + "M0": str(F(9*2576+39096, 73*832)), + "scope": "Conditional inherited source-preserving nine-call template only; not a supplied owner embedding."}, + "physical_or_all_size_supplier_admitted": False}, programs + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument("--emit", action="store_true") + ap.add_argument("--write", type=Path) + args = ap.parse_args() + result, programs = calculate() + if args.write: + with args.write.open("xb") as out: + out.write(canonical(result)) + else: + expected = load(HERE / "RESULT.json") + need(type(expected.get("schema_version")) is int, "typed receipt schema") + need(canonical(result) == canonical(expected), "frozen receipt mismatch") + need(canonical(programs) == canonical(load(HERE / "PROGRAMS.json.gz")), "frozen programs mismatch") + print(json.dumps(result, indent=2) if args.emit else result["status"]) + + +if __name__ == "__main__": + main() diff --git a/research/p104-fused-late-cleanup/inputs/pr3943_verify.py b/research/p104-fused-late-cleanup/inputs/pr3943_verify.py new file mode 100644 index 0000000000..a63800dadc --- /dev/null +++ b/research/p104-fused-late-cleanup/inputs/pr3943_verify.py @@ -0,0 +1,357 @@ +#!/usr/bin/env python3 +"""Source-bound P104 query consumer and priced legacy return. Apache-2.0.""" +from __future__ import annotations +import argparse +from collections import Counter +from fractions import Fraction as F +import hashlib +import itertools +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +REPO = HERE.parents[1] +MAIN = '20ecf2891d80b5acf18d980b2164fb44ea7faa90' +PRED = '9d56eeedbed5e3e9bbbc8c189d66f14cf15b6067' +CUT = 3642 +FULL = tuple(1 << i for i in range(9)) +NAMES = [f'{p}{i}' for p,n in [('X',104),('Y',104),('Q',8),('G',32),('D',32)] for i in range(n)] +# Columns are the PR3882 pivots in ascending port order. Derived from the +# actual 416-event suffix, then frozen before the full splice experiment. +T = [[2,2,2,-2,0,0,0,0], [0,0,2,2,2,-2,0,0], + [0,0,0,0,2,-2,-2,2], [2,2,2,2,0,0,0,0], + [2,2,-2,-2,0,0,0,0], [0,-2,0,-2,2,0,-2,0], + [-2,2,-2,2,0,0,0,0], [0,-2,2,0,-2,0,0,-2]] +PINS = { + 'inputs/PR3882_geometry.json':'8212331ef435650469b6fca71448bcc2915a0cab46562acc41c5fc2a3dfa56c7', + 'inputs/PR3882_RESULT.json':'33eaae6c77c10bed705d76b7950e7f8a6d5e09cd5727eadcde6f853c37be3f2b'} +LIVE = { + 'research/p104-native-channel/inputs/P104-FIXTURE.json':'516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4', + 'research/p104-native-channel/inputs/LOWRANK-WITNESS.json':'0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e'} + + +def need(ok, msg): + if not ok: + raise ValueError(msg) + + +def unique(pairs): + d = {} + for k,v in pairs: + need(k not in d, 'duplicate JSON key') + d[k] = v + return d + + +def load(path): + return json.loads(path.read_text(encoding='utf-8'), object_pairs_hook=unique) + + +def canonical(value): + return (json.dumps(value, sort_keys=True, separators=(',',':'))+'\n').encode() + + +def sha(value): + return hashlib.sha256(canonical(value)).hexdigest() + + +def pinned(root, names): + out = {} + for path, digest in names.items(): + raw = (root/path).read_bytes() + need(hashlib.sha256(raw).hexdigest() == digest, 'source hash '+path) + out[path] = json.loads(raw, object_pairs_hook=unique) + return out + + +def geometry(data): + removed = {tuple(v) for v in data['F0']+data['C']} + roots = set() + for a,b in itertools.combinations(range(8),2): + for s in (-1,1): + v = [0]*8 + v[a],v[b] = 2,2*s + roots.add(tuple(v)) + for s in itertools.product((-1,1),repeat=7): + if s.count(-1)%2 == 0: + roots.add((1,)+s) + need(len(roots)==120 and len(removed)==16 and removed<=roots, 'geometry domain') + ports = sorted(roots-removed) + J = [0,1,3,6,22,31,93,103] + N = [i for i in range(104) if i not in J] + A = [[F(sum(a*b for a,b in zip(u,v)),8) for v in ports] for u in ports] + B = [[A[j][n] for n in N] for j in J] + need(all(A[j][k]==(j==k) for j in J for k in J), 'pivot frame') + need(all(A[n][m]==sum(B[j][a]*B[j][b] for j in range(8)) + for a,n in enumerate(N) for b,m in enumerate(N)), 'Gram block factor') + need(sum(x!=0 for row in B for x in row)==384, 'B support') + need(all(x in (0,F(1,2),F(-1,2)) for row in B for x in row), 'B coefficients') + return A,B,J,N + + +def row_add(a,b,c): + out = a.copy() + for k,v in b.items(): + out[k] = out.get(k,F(0))+c*v + if not out[k]: del out[k] + return out + + +def expected_exit(A,B,J,N): + s = {n:{i:F(1)} for i,n in enumerate(NAMES)} + for i in range(104): + s[f'Y{i}'] = {104+i:F(1), **{j:x for j,x in enumerate(A[i]) if x}} + for b,j in enumerate(J): + s[f'X{j}'] = {j:F(1), **{n:B[b][a] for a,n in enumerate(N) if B[b][a]}} + s[f'Y{j}'] = {j:F(1),104+j:F(1)} + for n in N: s[f'X{n}'] = {n:F(1),104+n:F(1)} + return s + + +def expanded_cleanup(B,J,N,t=T): + d = [[F(0)]*104 for _ in range(8)] + for k in range(8): + for b,j in enumerate(J): d[k][j] = F(t[k][b]) + for a,n in enumerate(N): d[k][n] = sum(F(t[k][b])*B[b][a] for b in range(8)) + need(all(x in (-2,0,2) for r in d for x in r), 'cleanup alphabet') + need(all(sum(x!=0 for x in r)==52 for r in d), 'cleanup row supports') + return d + + +def cut_state(A,d): + s = {n:{i:F(1)} for i,n in enumerate(NAMES)} + for i in range(104): + s[f'Y{i}'] = {104+i:F(1), **{j:x for j,x in enumerate(A[i]) if x}} + for k in range(8): + s[f'Q{k}'] = {208+k:F(1), **{j:-x for j,x in enumerate(d[k]) if x}} + frames = {n:('H'+n[1:] if n.startswith('Y') else 'F') for n in NAMES} + return s,frames + + +def tail(B,J,N): + # Same literal tail as PR3882; its two streams must precede X_N overwrite. + ops = [('up',f'Y{i}',i) for i in range(104)] + for a,n in enumerate(N): + ops.append(('scale',f'X{n}','1/2')) + for b,j in enumerate(J): + if B[b][a]: + c = int(2*B[b][a]) + ops += [('add',f'X{j}',f'X{n}',c),('add',f'Y{j}',f'X{n}',-c)] + ops.append(('scale',f'X{n}','2')) + for b,j in enumerate(J): + ops.append(('scale',f'X{j}','1/2')) + for a,n in enumerate(N): + if B[b][a]: ops.append(('add',f'X{n}',f'X{j}',-int(2*B[b][a]))) + ops.append(('scale',f'X{j}','2')) + ops += [('add',f'X{n}',f'Y{n}',1) for n in N] + ops += [('down',f'X{n}',n) for n in N]+[('down',f'Y{j}',j) for j in J] + return ops + + +def consumer(J,t=T): + # Read-only q donors. Each signed 2q is two unit ADDs, without scratch. + return [('add',f'Q{k}',f'X{j}',int(c/abs(c))) + for k,row in enumerate(t) for j,c in zip(J,row) if c for _ in range(abs(c))] + + +def return_adapter(B,J,N): + ops = [('up',f'X{n}',n) for n in N] + for b,j in enumerate(J): + ops.append(('scale',f'X{j}','1/2')) + for a,n in enumerate(N): + if B[b][a]: ops.append(('add',f'Y{n}',f'X{j}',-int(2*B[b][a]))) + ops.append(('scale',f'X{j}','2')) + for n in N: + ops += [('add',f'X{n}',f'Y{n}',-1),('add',f'Y{n}',f'X{n}',1)] + for a,n in enumerate(N): + ops.append(('scale',f'X{n}','1/2')) + for b,j in enumerate(J): + if B[b][a]: ops.append(('add',f'X{j}',f'X{n}',-int(2*B[b][a]))) + ops.append(('scale',f'X{n}','2')) + return ops+[('down',f'Y{n}',n) for n in N] + + +def run(s,frames,ops): + s,frames = {k:v.copy() for k,v in s.items()},frames.copy() + for op in ops: + kind,r = op[:2] + need(r in s, 'unknown register') + if kind=='up': + need(frames[r]=='H'+str(op[2]), 'wrong lift frame') + frames[r] = 'F' + elif kind=='down': + need(frames[r]=='F', 'wrong descent frame') + frames[r] = 'H'+str(op[2]) + else: + need(frames[r]=='F', 'arithmetic target not FULL') + if kind=='scale': + c = F(op[2]); need(c in (F(1,2),F(2)), 'scale alphabet') + s[r] = {i:c*x for i,x in s[r].items()} + else: + need(kind=='add' and r!=op[2] and frames.get(op[2])=='F', 'ADD source frame') + need(type(op[3]) is int and op[3] in (-1,1), 'unit ADD alphabet') + s[r] = row_add(s[r],s[op[2]],F(op[3])) + return s,frames + + +def endpoint_digest(s): + return sha([[str(s[n].get(i,F(0))) for i in range(280)] for n in NAMES]) + + +def desired_frames(J): + return {n:('H'+n[1:] if (n.startswith('Y') and int(n[1:]) in J) + or (n.startswith('X') and int(n[1:]) not in J) else 'F') for n in NAMES} + + +def span(vectors): + out = {0} + for x in vectors: + need(type(x) is int and 00, 'prefix transport tariff') + profile[e[4]]+=1; f[r]=after + elif k=='zero': + need(r=='C' and r not in s, 'private allocation') + s[r]={}; f[r]=tuple(e[2]) + elif k=='copy': + need(r=='C' and not s[r] and span(f[r])==span(f[e[2]])==span(e[3]), 'private copy') + s[r]=s[e[2]].copy() + else: + need(k=='erase' and r=='C' and span(f[r])==span(e[2]), 'owned live-copy erase contract') + del s[r]; del f[r] + need(set(s)==set(NAMES), 'cut live registers') + want,cutframes=cut_state(A,d) + need(s==want, 'actual cut coefficients') + need(all(span(f[n])==span(w['final_frames'][n]) for n in NAMES), 'cut exit frames') + hs=[span(f[f'Y{i}']) for i in range(104)] + need(all(len(h)==256 for h in hs) and len(set(hs))==104, 'distinct target hyperplanes') + need(all(span(f[n])==span(FULL) for n in NAMES if not n.startswith('Y')), 'FULL consumers and sources') + result,ff=run(s,cutframes,ops) + need(result==expected and ff==desired_frames(J), 'actual source-bound splice endpoint') + hist=[profile[r] for r in range(1,9)] + need(hist==[1074,58,86,104,48,24,8,8], 'inherited profile recount') + # Direct old cleanup is a control, not inferred from the new factor. + old={n:r.copy() for n,r in s.items()} + for e in program[CUT:]: old[e[1]]=row_add(old[e[1]],old[e[2]],F(e[3])) + for i in range(208,280): need(old[NAMES[i]]=={i:F(1)}, 'old cleanup dirt control') + return {'original_prefix_events':CUT,'actual_cleanup_events':len(program)-CUT, + 'original_native_profile':hist,'live_cut_registers':len(s), + 'distinct_output_hyperplanes':len(set(hs)), 'actual_endpoint_sha256':endpoint_digest(result), + 'original_cut_sha256':endpoint_digest(s),'prefix_operation_counts':dict(sorted(kinds.items()))} + + +def counts(ops): + c=Counter(e[0] for e in ops) + return {'unit_adds':c['add'],'halves':sum(e[0]=='scale' and e[2]=='1/2' for e in ops), + 'doubles':sum(e[0]=='scale' and e[2]=='2' for e in ops),'rank_one_transports':c['up']+c['down']} + + +def calculate(): + inputs=pinned(HERE,PINS) + A,B,J,N=geometry(inputs['inputs/PR3882_geometry.json']) + pred=inputs['inputs/PR3882_RESULT.json'] + need(pred['pivots']==J and pred['nonpivots']==N and pred['combined_mass']==2576, 'predecessor receipt scope') + d=expanded_cleanup(B,J,N) + s,f=cut_state(A,d) + ops=tail(B,J,N)+consumer(J) + actual,ff=run(s,f,ops) + expected=expected_exit(A,B,J,N) + need(actual==expected and ff==desired_frames(J), 'new consumer endpoint') + need(endpoint_digest(actual)==pred['endpoint_sha256'], 'unchanged predecessor endpoint digest') + returned,rf=run(actual,ff,return_adapter(B,J,N)) + for i in range(104): + need(returned[f'X{i}']=={i:F(1)}, 'legacy source return') + need(returned[f'Y{i}']=={i:F(1),104+i:F(1)}, 'legacy corrected sum') + need(rf[f'X{i}']=='F' and rf[f'Y{i}']=='H'+str(i), 'legacy endpoint frame') + for i in range(208,280): need(returned[NAMES[i]]=={i:F(1)}, 'legacy dirty restoration') + # Explicit separating family for every H_n: only w_n is initially nonzero, + # while requested x_n at FULL must become nonzero. Proof supplies all lengths. + for n in N: + isolated={name:{} for name in NAMES}; isolated[f'X{n}']={0:F(1)} + r,_=run(isolated,desired_frames(J),return_adapter(B,J,N)) + need(r[f'X{n}']=={0:F(1)}, 'return cut separating witness') + mass=pred['combined_mass']; progress=104*8+104*8+72*9 + need(mass-progress==264, 'persistent progress invoice') + # m=8s+1, W=104(s-1); all-p proof is in PROOF.md, not a sampled inference. + budget=[] + for stages in (3,5,9,17): + width=8*stages+1; roles=104*(stages-1) + owed=(width-1)*roles + for extra in (0,192): + paid=stages*(mass+extra)+max(0,owed-stages*progress) + gap=(mass+extra-progress-104)*stages+104 + need(paid-width*roles>=gap>0, 'coverage-gap identity') + budget.append({'stages':stages,'legacy_return':bool(extra),'width':width,'roles':roles, + 'paid_mass_lower_bound':paid,'capacity':width*roles,'gap_lower_bound':gap}) + result={'schema_version':1,'scientific_base':MAIN,'predecessor':PRED, + 'cut':CUT,'pivots':J,'cleanup_factor':T,'old_cleanup_weighted_adds':416, + 'new_cleanup_weighted_adds':32,'old_readonly_unit_adds':832,'new_readonly_unit_adds':64, + 'readonly_unit_adds_saved':768,'real_component_adds_saved_at_512_complex_words':786432, + 'tail':counts(tail(B,J,N)),'consumer':counts(consumer(J)), + 'legacy_return_adapter':counts(return_adapter(B,J,N)), + 'legacy_return_minimum_rank_mass_in_stated_model':192, + 'original_prefix_events':CUT,'new_unit_suffix_events':len(ops), + 'new_joined_events':CUT+len(ops),'weighted_cleanup_joined_events':CUT+len(tail(B,J,N))+32, + 'consumer_program_sha256':sha(consumer(J)), + 'joined_suffix_program_sha256':sha(ops), + 'endpoint_sha256':endpoint_digest(actual),'legacy_endpoint_sha256':endpoint_digest(returned), + 'combined_profile':[1282,58,86,104,48,24,8,8],'combined_mass':mass, + 'legacy_combined_profile':[1474,58,86,104,48,24,8,8],'legacy_combined_mass':mass+192, + 'optimistic_progress_per_call':progress,'residual_gap_slope':160,'residual_gap_intercept':104, + 'legacy_gap_slope':352,'legacy_gap_intercept':104,'sample_budgets':budget, + 'new_native_recipe_replay':False,'affordable_supplier':False,'selected_frontier_changed':False} + need(counts(tail(B,J,N))==dict(unit_adds=1248,halves=104,doubles=104,rank_one_transports=208), 'tail invoice') + need(counts(return_adapter(B,J,N))==dict(unit_adds=960,halves=104,doubles=104,rank_one_transports=192), 'return invoice') + return result,(A,B,J,N,ops,expected) + + +def main(): + parser=argparse.ArgumentParser() + parser.add_argument('--algebra-only',action='store_true',help='Do not claim original-word or source-cut authentication.') + parser.add_argument('--write-result',action='store_true',help='Explicitly regenerate only this package result.') + args=parser.parse_args() + result,context=calculate() + if args.write_result: + (HERE/'RESULT.json').write_text(json.dumps(result,indent=2,sort_keys=True)+'\n') + else: + need(canonical(result)==canonical(load(HERE/'RESULT.json')), 'typed frozen result mismatch') + if not args.algebra_only: + print(json.dumps(source_audit(*context),sort_keys=True)) + mode='ALGEBRA_ONLY' if args.algebra_only else 'SOURCE_BOUND' + print(f'PASS_P104_RESIDUAL_CONSUMER_{mode} cleanup=416_to_32 unit=832_to_64 legacy_rank=192 result={sha(result)}') + +if __name__=='__main__': main() diff --git a/research/p104-fused-late-cleanup/inputs/pr3981_verify.py b/research/p104-fused-late-cleanup/inputs/pr3981_verify.py new file mode 100644 index 0000000000..1e0d832359 --- /dev/null +++ b/research/p104-fused-late-cleanup/inputs/pr3981_verify.py @@ -0,0 +1,201 @@ +#!/usr/bin/env python3 +"""Exact late-FULL dirty-query delivery. Sparse evaluator adapted from #3965.""" +from pathlib import Path +from fractions import Fraction as F +from collections import Counter +import argparse, copy, hashlib, importlib.util, json +P=Path(__file__).resolve().parent +ROOT=P.parents[1] +WIT='research/p104-native-channel/inputs/LOWRANK-WITNESS.json' +WIT_HASH='0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e' + +def need(ok,msg): + if not ok: raise ValueError(msg) + +def load(path): + def pairs(items): + out={} + for k,v in items: + need(k not in out,'duplicate JSON key: '+k) + out[k]=v + return out + return json.loads(path.read_text(),object_pairs_hook=pairs) + +def encoded(value): + return json.dumps(value,sort_keys=True,separators=(',',':')) + +def span(vs): + out={0} + for v in vs: out |= {x^v for x in tuple(out)} + return frozenset(out) + +def add(a,b,c): + out=dict(a) + for k,v in b.items(): + out[k]=out.get(k,F(0))+c*v + if not out[k]: del out[k] + return out + +def replay(word): + rows={k:{k:F(1)} for k in word['initial_frames']} + frames={k:span(v) for k,v in word['initial_frames'].items()} + private=[]; paid=Counter(); counts=Counter(); snapshots={} + for i,e in enumerate(word['program']): + op,r=e[:2];counts[op]+=1 + if op=='transport': + _,r,a,b,n=e;aa,bb=span(a),span(b) + need(frames[r]==aa,'transport entrance') + need(aa<=bb or bb<=aa,'non-nested transport') + need(n==abs(len(a)-len(b)) and len(aa)==2**len(a) and len(bb)==2**len(b),'rank tariff') + frames[r]=bb;paid[n]+=1 + elif op=='zero': + need(r=='C' and r not in rows,'fresh owned private') + rows[r]={};frames[r]=span(e[2]);private.append({'zero':i}) + elif op=='copy': + _,r,s,f=e;need(r=='C' and not rows[r] and frames[r]==frames[s]==span(f),'copy ownership/zero/common chart') + rows[r]=dict(rows[s]);private[-1].update(copy=i,source=s,copy_row=dict(rows[s]),frame=list(f)) + elif op=='erase': + need(r=='C' and frames[r]==span(e[2]),'private erase owner/chart') + private[-1].update(erase=i,erase_row=dict(rows[r]),end_frame=e[2]);del rows[r];del frames[r] + elif op in ('half','double'): + need(frames[r]==span([1<b: + need(e[3]==-1 and e[4]==FULL and i<=CUT,'fixed D cleanup');removed.add(i);clean.append(i) + if e[0]=='add' and e[1].startswith('Y') and e[2] in ds and i>b: + need(i0 and len(sa)==2**len(a) and len(sb)==2**len(b),'positive rank tariff') + paid[k]+=1;frames[r]=sb + elif op=='add': + _,r,s,c,f=e;need(r!=s and frames[r]==frames[s]==span(f),'physical common chart ADD') + rows[r]=plus(rows[r],rows[s],F(c)) + elif op in ('half','double'): + need(frames[r]==span(FULL),'scalar common FULL');c=F(1,2) if op=='half' else F(2);rows[r]={i:c*v for i,v in rows[r].items()} + elif op=='zero': + need(r=='C' and r not in rows,'owned allocation');rows[r]={};frames[r]=span(e[2]) + elif op=='copy': + need(r=='C' and not rows[r] and frames[r]==frames[e[2]]==span(e[3]),'owned zero copy');rows[r]=rows[e[2]].copy() + else: + need(op=='erase' and r=='C' and frames[r]==span(e[2]),'owned private discard');del rows[r];del frames[r] + need(set(rows)==set(NAMES),'all public roles and no private leaks') + return rows,frames,dict(paid),dict(ops) + +def tail_program(w,m): + _,A,J,N,B=m.geometry();out=[] + for e in m.program(J,N,B): + op,r=e[:2];r=NAMES[r] + if op in ('lift','drop'): + i=int(r[1:]);h=w['final_frames'][f'Y{i}'];out.append(['transport',r,h if op=='lift' else FULL,FULL if op=='lift' else h,1]) + elif op=='add':out.append(['add',r,NAMES[e[2]],e[3],FULL]) + else:need(op in ('half','double'),'tail alphabet');out.append([op,r]) + need(out[:104]==[['transport',f'Y{i}',w['final_frames'][f'Y{i}'],FULL,1] for i in range(104)],'old lift prefix') + return out,A,J,N,B + +def invoice(program): + c=Counter() + for e in program: + if e[0]=='add': + z=abs(F(e[3]));need(z.denominator&(z.denominator-1)==0,'dyadic coefficients');c['unit_add']+=z.numerator;s=z.denominator.bit_length()-1;c['half']+=s;c['double']+=s + elif e[0] in ('half','double'):c[e[0]]+=1 + elif e[0]=='transport':c['positive_native_mass']+=e[4] + else:c[e[0]]+=1 + return dict(c) + +def calculate(): + w,mods=source_modules();old3981,old3943,old3882,old3940=mods + late,_,removed=old3981.compile_delivery(w);late=late['program'];suffix=w['program'][3642:] + need(len(suffix)==416 and late[-416:]==suffix,'literal416 cleanup suffix') + prefix=late[:-416];tail,A,J,N,B=tail_program(w,old3882);tail=tail[104:] + D=[[F(0)]*104 for _ in range(8)] + for e in suffix: + need(e[0]=='add' and e[1].startswith('Q') and e[2].startswith('X') and e[4]==FULL and abs(F(e[3]))==2,'actual source cleanup alphabet') + D[int(e[1][1:])][int(e[2][1:])]+=F(e[3]) + T=[[r[j] for j in J] for r in D] + need(T==old3943.T and sum(c!=0 for r in T for c in r)==32,'same actual3943 cleanup factor') + need(all(D[k][n]==sum(T[k][b]*B[b][a] for b in range(8)) for k in range(8) for a,n in enumerate(N)),'D=T[I B]') + cleanup=[['add',r,s,c,FULL] for op,r,s,c in old3943.consumer(J)] + need(len(cleanup)==64 and all(e[3] in (-1,1) for e in cleanup),'64 read-only unit ADDs') + reference=late+tail;fused=prefix+tail+cleanup + old,of,p0,c0=execute(w,reference);new,nf,p1,c1=execute(w,fused) + need(new==old and nf==of and p1==p0,'all280 endpoint rows and exact formal frames/profile') + need([e for e in fused if e[0]=='transport']==[e for e in reference if e[0]=='transport'],'entire native chronological subsequence unchanged') + atcut,cf,_,_=execute(w,prefix) + need(all(f==span(FULL) for f in cf.values()),'all280 roles FULL after late delivery') + for i in range(104): + need(atcut[f'X{i}']=={f'X{i}':F(1)},'literal source at late cut') + want={f'Y{i}':F(1)};want.update({f'X{j}':x for j,x in enumerate(A[i]) if x});need(atcut[f'Y{i}']==want,'late delivery Gram endpoint') + target=f'Y{i}' if i in J else f'X{i}';need(new[target]=={f'X{i}':F(1),f'Y{i}':F(1)},'unchanged sum slot') + for k in range(8): + want={f'Q{k}':F(1)};want.update({f'X{i}':-x for i,x in enumerate(D[k]) if x});need(atcut[f'Q{k}']==want,'actual Q=h-Dx at fusion cut') + intermediate,ff,_,_=execute(w,prefix+tail) + for b,j in enumerate(J): + want={f'X{j}':F(1)};want.update({f'X{n}':B[b][a] for a,n in enumerate(N) if B[b][a]});need(intermediate[f'X{j}']==want and ff[f'X{j}']==span(FULL),'actual residual q donor at FULL') + need(all(new[r]=={r:F(1)} for r in NAMES if r[0] in 'QGD'),'all72 arbitrary dirty returns') + for i in N: + want={f'Y{i}':F(1)};want.update({f'X{j}':x for j,x in enumerate(A[i]) if x}) + need(new[f'Y{i}']==want,'unchanged nonpivot Gram residual') + # Optional actual inherited source-return consumer; no claim its192 tariff is new. + adapter=[] + for e in old3943.return_adapter(B,J,N): + op,r=e[:2] + if op in ('up','down'): + h=w['final_frames'][f'Y{e[2]}'];adapter.append(['transport',r,h if op=='up' else FULL,FULL if op=='up' else h,1]) + elif op=='scale':adapter.append(['half' if F(e[2])==F(1,2) else 'double',r]) + else:need(op=='add','return alphabet');adapter.append(['add',r,e[2],e[3],FULL]) + returned,rf,_,_=execute(w,fused+adapter) + for i in range(104): + need(returned[f'X{i}']=={f'X{i}':F(1)} and rf[f'X{i}']==span(FULL),'source return exact') + need(returned[f'Y{i}']=={f'X{i}':F(1),f'Y{i}':F(1)} and rf[f'Y{i}']==span(w['final_frames'][f'Y{i}']),'legacy sum and frame') + need(all(returned[r]=={r:F(1)} for r in NAMES if r[0] in 'QGD'),'legacy72dirtyreturn') + legacy_invoice=invoice(fused+adapter) + need(legacy_invoice=={'unit_add':5664,'half':2720,'double':2720,'positive_native_mass':2712},'complete legacy return invoice') + # The actual3940 fused source-preserving tail contains q only temporarily. + sp_ops=old3940.fused(J,N,B);pre_ops=old3940.pivot_stream(J,N,B)+old3940.scatter(J,N,B,104) + need(sp_ops[:104]==[['lift',104+i] for i in range(104)] and sp_ops[104:104+len(pre_ops)]==pre_ops,'literal3940internalcut') + def indexed_events(ops): + converted=[] + for e in ops: + op,r=e[:2];r=NAMES[r] + if op in ('lift','drop'): + h=w['final_frames'][f'Y{int(r[1:])}'];converted.append(['transport',r,h if op=='lift' else FULL,FULL if op=='lift' else h,1]) + elif op=='add':converted.append(['add',r,NAMES[e[2]],e[3],FULL]) + else:need(op in ('half','double'),'source-preservingtailalphabet');converted.append([op,r]) + return converted + sp_tail=indexed_events(sp_ops[104:]);sp_cut=len(pre_ops) + sp_reference=late+sp_tail;sp_fused=prefix+sp_tail[:sp_cut]+cleanup+sp_tail[sp_cut:] + sp_old,sp_of,_,_=execute(w,sp_reference);sp_new,sp_nf,_,_=execute(w,sp_fused) + need(sp_old==sp_new==returned and sp_of==sp_nf==rf,'actual3940same source-preservingendpoint') + need([e for e in sp_reference if e[0]=='transport']==[e for e in sp_fused if e[0]=='transport'],'3940matched native subsequence') + liveq,qframes,_,_=execute(w,prefix+sp_tail[:sp_cut]) + need(all(liveq[f'X{j}']==intermediate[f'X{j}'] and qframes[f'X{j}']==span(FULL) for j in J),'source-preservingactualqexistsFULL') + need(all(liveq[f'Q{k}']==atcut[f'Q{k}'] for k in range(8)),'source-preservingQnot prematurelyrestored') + spinv0,spinv1=invoice(sp_reference),invoice(sp_fused) + need(spinv0=={'unit_add':5856,'half':2712,'double':2712,'positive_native_mass':2520},'matched3940baselineinvoice') + need(spinv1=={'unit_add':5088,'half':2712,'double':2712,'positive_native_mass':2520},'source-preservingfusedinvoice') + too_late=execute(w,prefix+sp_tail+cleanup)[0] + need(sum(too_late[f'Q{k}']!=sp_new[f'Q{k}'] for k in range(8))==8,'cleanup after q-restorationmustfail8dirtyreturns') + inv0,inv1=invoice(reference),invoice(fused) + need(inv0=={'unit_add':5472,'half':2616,'double':2616,'positive_native_mass':2520},'exact3981 comparison invoice') + need(inv1=={'unit_add':4704,'half':2616,'double':2616,'positive_native_mass':2520},'fused invoice') + bads={'omit_compressed_cleanup':prefix+tail,'cleanup_before_residual':prefix+cleanup+tail,'reuse_old_cleanup_after_source_consumption':prefix+tail+suffix,'double_cleanup':prefix+suffix+tail+cleanup,'omit_one_unit':prefix+tail+cleanup[:-1]} + # Delivery must read the live query before restoring it to arbitrary dirt. + # Replace quartering's final doubles with nothing: this must fail as well. + broken=copy.deepcopy(prefix);i=next(i for i,e in enumerate(broken) if e==['double','Q0']);del broken[i:i+2];bads['unrestored_late_donor']=broken+tail+cleanup + lift0=next(i for i,e in enumerate(prefix) if e==['transport','Y0',w['final_frames']['Y0'],FULL,1]) + bads['correction_before_late_delivery']=prefix[:lift0+104]+tail+prefix[lift0+104:]+cleanup + controls={} + for name,program in bads.items(): + try:b,bf,_,_=execute(w,program) + except (ValueError,KeyError):controls[name]='frame-or-owner rejection';continue + defects=[r for r in NAMES if b[r]!=old[r]];need(defects or bf!=of,'semantic control accepted '+name);controls[name]={'changed_roles':len(defects),'changed_dirty_roles':sum(r[0] in 'QGD' for r in defects)} + # Inherited paired/two-axis gate is numerically unchanged by scalar fusion. + gap=208*(inv1['positive_native_mass']-2312)-10816;need(gap==32448,'same failing two-axis gate') + return {'schema_version':1,'scope':'actual3981 late delivery plus3943 compressed cleanup; exact finite formal-frame splice','cut_after_original_event':3641,'cleanup_factor':[[int(x) for x in row] for row in T],'literal_old_cleanup_events':416,'new_cleanup_unit_adds':64,'old_cleanup_unit_adds':832,'unit_adds_saved_against3981':768,'reference_invoice':inv0,'fused_invoice':inv1,'inherited_source_preserving_return_invoice':legacy_invoice,'direct_source_preserving_reference_invoice':spinv0,'direct_source_preserving_fused_invoice':spinv1,'source_preserving_internal_cut_after_tail_ops_without_lifts':sp_cut,'source_preserving_late_cleanup_defective_dirty_roles':8,'source_preserving_fused_program_sha256':sha(sp_fused),'native_profile':p1,'fused_formal_events':len(fused),'reference_formal_events':len(reference),'fused_event_counts':c1,'all_input_columns':280,'restored_dirty_helpers':72,'full_native_subsequence_unchanged':True,'actual3981_endpoint_preserved':True,'q_cleanup_reads_from_actual_residual':True,'endpoint_sha256':sha([[str(new[r].get(k,F(0))) for k in NAMES] for r in NAMES]),'fused_program_sha256':sha(fused),'controls':controls,'two_axis_gap':gap,'native_recipe_replay':False,'all_size_admission':False,'selected_frontier_changed':False},fused + +def main(): + ap=argparse.ArgumentParser();ap.add_argument('--write-result',action='store_true');args=ap.parse_args();result,_=calculate() + if args.write_result:(P/'RESULT.json').write_text(json.dumps(result,sort_keys=True,indent=2)+'\n') + else:need(canonical(result)==canonical(load(P/'RESULT.json')),'typed result mismatch') + print('PASS_P104_FUSED_LATE_CLEANUP inputs=280 dirty=72 unit_adds=4704 saved=768 native_mass=2520 source_preserving_adds=5088 controls=8') +if __name__=='__main__':main()