diff --git a/research/staged544-separated-a2/.gitattributes b/research/staged544-separated-a2/.gitattributes new file mode 100644 index 0000000000..3d3239d3bc --- /dev/null +++ b/research/staged544-separated-a2/.gitattributes @@ -0,0 +1,2 @@ +source/** -text whitespace=blank-at-eol,blank-at-eof,space-before-tab,cr-at-eol +inputs/** -text diff --git a/research/staged544-separated-a2/.gitignore b/research/staged544-separated-a2/.gitignore new file mode 100644 index 0000000000..7a60b85e14 --- /dev/null +++ b/research/staged544-separated-a2/.gitignore @@ -0,0 +1,2 @@ +__pycache__/ +*.pyc diff --git a/research/staged544-separated-a2/LEDGER.json b/research/staged544-separated-a2/LEDGER.json new file mode 100644 index 0000000000..83f3f87837 --- /dev/null +++ b/research/staged544-separated-a2/LEDGER.json @@ -0,0 +1,36 @@ +{ + "scope": "two exact PR3734 words; seven separated inverse-A2 blocks plus credited PR3998 consecutive A1858 block", + "proved_or_exactly_recomputed": { + "local_maps": "Exact rational3x3 identities on arbitrary dirty values, proved compositionally under strictdisjointsupport; no nativeeventcrossing.", + "scalar_delta_vs_PR3998": { + "forward_ADDs": -7, + "cleanup_ADDs": -5 + }, + "scalar_delta_vs_PR3734": { + "forward_ADDs": -8, + "cleanup_ADDs": -6 + }, + "paid_profile": { + "1": 2440, + "2": 725, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "rank_mass": 5134, + "children": 3519, + "native_descriptors": "All72nativewarps/operatorrecords perprovider retained in order; onlyBpositionsremapped for deleted gates withinfixedcuts.", + "allocation": "No new register/helper/buffer. Helperwidthinventory unchanged.", + "unchanged_fields": "All top-level fields except A,B,restore,warps positions and derivedcleanup mustcompareequal." + }, + "unknown_or_inherited": { + "physical_implementation": "Native scalar realization and owner/holding/routing/control/tape costs not newly admitted.", + "precision": "Changed intermediate coefficientgrowth/signed-floor/error ledger is not certified by scalar algebra alone.", + "native_phases": "No fresh concrete Clifford/Gaussian globalphase or inverse-lowering replay; unchangedoperators are freeformal symbols in wholeword replay.", + "later_words": "No applicability toPR3945or later words is claimed.", + "full_supplier": "Uniformwidths, stock, allsizecompiler, outer/analytic/BIT and fullmultiplicationtheorem remain inherited/unproved here.", + "performance": "No measuredruntimeor practicalspeedup claim." + }, + "decision": "Retain focused scalar simplification and exact unchangedrecursiveprofile. Stop dependent graph/native expansion; this does not improve recursive moment or kappa." +} diff --git a/research/staged544-separated-a2/PROOF.md b/research/staged544-separated-a2/PROOF.md new file mode 100644 index 0000000000..d39dd7eff0 --- /dev/null +++ b/research/staged544-separated-a2/PROOF.md @@ -0,0 +1,196 @@ +# Fixed separated A2 contractions and their complete unchanged frame bill + +ToikY, with substantial OpenAI Codex assistance. Apache-2.0. + +## Statement and frozen domain + +This certificate supplies seven fixed nonconsecutive scalar contractions on +each of the two PR3734 providers retained by PR3998. It also reproduces, and +credits to PR3998, the existing consecutive contraction at A1858. Its input +providers are PR3734 `fa041037a3374eaa08feeca0b26a5d6893194147`, exported +byte-exactly by PR3998 `389268a6b5e0373a3125d5c6fcd6995f4ea324f5`. +The package is based on canonical main +`20ecf2891d80b5acf18d980b2164fb44ea7faa90`; none of these attribution pins +asserts ancestry of a pending contribution. `SOURCES.json` binds the complete +local source closure. The retained PR3945 notice supplies lineage, not +applicability to the later PR3945 words. + +On arbitrary rational live inputs and dirty buffers, the changed word has the +same full operator as its source. It uses the same registers, native maps, +wrappers, target cut, initial corrections and helper entrance/exit frames. Its +complete paid profile is unchanged. Relative to PR3998's one-site contraction, +it removes seven forward scalar ADD records and five inverse-cleanup ADD +records. This is a fixed constructive simplification, with no recursive-moment +or kappa improvement. It is not an exhaustive separated-motif search, a graph +normal-form theorem, a runtime result or fresh native/supplier admission. + +Original zero-based sites are: + +| Section | Selected indices | Removed central position | Credit | +|---|---|---|---| +| A | 1858,1859,1860 | last | PR3998 | +| B | 4,53,54 | first | new fixed witness | +| B | 7,49,50 | first | new fixed witness | +| restore | 20,21,36 | last | new fixed witness | +| restore | 22,23,38 | last | new fixed witness | +| restore | 26,27,51 | last | new fixed witness | +| restore | 30,31,62 | last | new fixed witness | +| restore | 32,33,73 | last | new fixed witness | + +`data.json` retains every original gate, replacement, support and canonical +word/cleanup digest. The seven new replacements retain the exact original +ordered frame lists. For the credited old A1858 replacement only, the +publication's basis order `[42,82]` is reproduced instead of the raw source's +`[82,42]`; these span the same subspace. The old site's two canonical edited +word hashes are checked against PR3998's publication before applying the seven +additional changes. + +## Exact three-coordinate identity and legal gathering + +An ADD `(destination,source,c)` means +`x_destination <- x_destination + c*x_source`. A chronological list acts in +listed order, so its matrix product has the last event on the left. +For three distinct registers `x,y,z`, put + +``` +S(a): y += a*z T(b): x += b*y U(c): x += c*z. +``` + +The two relevant chronological identities, valid over the rationals, are + +``` +[S(a), T(b), U(-ab)] = [T(b), S(a)] +[U(ab), T(b), S(a)] = [S(a), T(b)]. +``` + +In the first identity both sides end at +`(x+b*y, y+a*z, z)` in terms of the initial coordinates. In the second both end +at `(x+b*y+ab*z, y+a*z, z)`. Thus these equalities preserve arbitrary dirty +inputs, rather than assuming any operand is zero. The primary checker compares +exact rational matrices; `independent.py` separately propagates the three +independent coordinate columns with `Fraction` arithmetic. Equality of these +three columns proves equality of the entire three-coordinate linear operator. + +At every selected site the three ADDs use one common frame. Every intervening +unselected scalar event reads and writes registers outside the entire selected +three-register support. Such an event commutes with every selected ADD as an +operator on the full register space. The selected triple can therefore be +gathered at its first old position, contracted by one of the identities above, +and followed by the unchanged intervening events. The checker includes both +reads and writes in the disjointness test; write-only independence would be +insufficient. + +All eight supports are pairwise disjoint. This also permits the overlapping +index windows of different sites to be contracted simultaneously. No selected +window crosses the A prelude, a section boundary, the target cut or a B native +warp cut. Reconstructed B warp indices change only to locate the same native +event after the same surviving source events. Native lender registers, map +columns, ordered entry/exit frames and native order remain identical. + +Each local identity embeds as that exact operator on its three registers and +the identity on every other live or buffer coordinate. Composing these +equalities with unchanged surrounding operators proves full operator equality +on all 632 live coordinates plus 91 independent dirty buffers. This argument +does not inspect or simplify a native map, commute across a native event, or +assume a native phase convention. It holds with any common linear realization +of the unchanged surrounding operators. Native realizability and their inherited +signed phases are separate obligations. + +## Projected inverse cleanup + +The word contract's ordinary forward sequence is A after `prelude_events`, +then B with its interleaved native events, then restore. No non-target scalar +instruction reads a target. This hygiene rule makes the non-target subsystem +autonomous: deleting target-writing events leaves its invertible operator +`F_N`. Literal cleanup reverses that projected program, negating ADD +coefficients, reciprocating nonzero scales and inverting native symbols. +For each protected helper `r`, the fixed renaming `r -> r+704` applies to both +sources and destinations of this inverse. It names the inherited private dirty +buffer; it is not a new allocation by this construction. + +Equal full forward operators have equal autonomous non-target blocks. +Consequently their projected inverses, under the same buffer renaming, are +equal. Regenerating literal cleanup from the edited ordinary sequence therefore +preserves its buffer action and every endpoint. The checker compares the entire +regenerated cleanup list and its canonical digest, rather than retaining an old +cleanup solely because the forward endpoint matches. + +For both new B sites, the first two original ADDs write a target, while the +third writes a helper. Their contraction changes the target part but retains +the same single helper ADD in the projection. These sites save two forward +ADD records and no cleanup records. Each of the five restore sites is wholly +non-target, saving one forward and one cleanup ADD record. Thus the new saving +is exactly `7+5=12` scalar ADD records versus PR3998. The old A1858 site adds +the separately credited `1+1`; against raw PR3734 the combined saving is +`8+6=14` records. + +These are rational scalar ADD records. Some coefficients are `2` or `1/2`. +The count is not an asserted unit-native instruction saving or physical tariff. +No zero buffer, unchanged helper or caller-boundary assumption is introduced +by the local identities. + +## Complete chronological frame bill + +Algebraic equality alone does not establish a legal or favorable framed +program. The primary auditor recomputes the entire chronological bill and +hygiene for each source, credited-only and final word. The independent checker +implements a second binary trace using explicit immutable point sets in +`F_2^9`, without importing the primary or retained executable. It authenticates +the two compressed input byte strings before loading either provider. + +A frame is the XOR closure of its listed vectors. A scalar event requires +every touched register's current frame to be contained in the event frame. +Each positive dimension difference contributes one recursive child of that +rank. The trace includes initial frames, the fixed target-cut levels, center +entry and nested borrowed descents, every native entry and binary frame image, +the restore stage, and all final successor climbs. Center descent views do +not replace the persistent main register state. Native frame images are +checked by enumerating all 512 binary vectors; this is a binary-frame check, +not signed Clifford verification. + +The independent checker compares 149 complete live-register frame states for +each source/credited/final word: entrance, A exit, both sides of all 72 B native +events, B exit, restore exit and terminal. All agree. It separately recomputes +every charge, including intermediate charges that those boundary comparisons +alone would not determine. The full profile for both providers is + +``` +{1:2440, 2:725, 3:224, 4:102, 5:20, 8:8}. +``` + +There are 3,519 recursive children and rank mass 5,134. Helper widths remain +`{4:26,5:2,6:18,7:53,8:96,9:213}`. No rank count changes, so the recursive +moment agrees identically at every exponent where the inherited profile price +is defined; no numerical optimization is required. Unchanged cleanup widths +and native descriptors do not certify physical scheduling, finite precision, +stock/tape, all-size compilation or outer/BIT obligations. Those remain +inherited or unknown, rather than being assigned cost zero. + +## Evidence, controls and attribution + +The primary replay uses the authenticated, unchanged predecessor +`audit_core.py`. For each provider it freshly checks all three words on the +full 723-input ordinary and dual free-operator matrices, reverse pullback, +cleanup boundaries, buffer identity and absence of buffer-to-live leakage. +This is reuse of a credited interpreter, not a newly independent full-word +interpreter. The independent checker proves the changes compositionally, +reconstructs the complete edited word and cleanup, matches their canonical +digests to `data.json`, and independently certifies the complete frame invoices. +It does not claim a second full free-operator matrix replay. + +Seven in-memory controls per provider must reject: wrong A2 sign, an intervening +read dependency, duplicate/overlapping support, a crossed native cut, a changed +common ordered frame, stale cleanup, and an omitted retained gate. Rejection +uses explicit exceptions and remains active under Python `-O`. These bounded +controls supplement the exact certificate; they do not imply universal test +coverage or independent human acceptance. + +Chris R / Clear1nsight PR3998 supplies the A2 identity, the old consecutive +A1858 contraction, and retained proof/source exports. Dataisfire supplies the +PR3734 literal words. Sagar Thakrar, roger-sato and Arham Tahir supply the +retained auditor lineage. Jeremy Kothe and Dugongue supply rank-profile and +paid-budget context, including PR3945/3863. PR1865 by 1337isnot1337 is earlier +nonconsecutive commuting C3 work with a different identity and source; this +certificate claims no general priority for commuting graph rewrites. +Original notices remain under `source/`. This package neither merges a PR nor +changes the selected frontier. diff --git a/research/staged544-separated-a2/README.md b/research/staged544-separated-a2/README.md new file mode 100644 index 0000000000..4e28745283 --- /dev/null +++ b/research/staged544-separated-a2/README.md @@ -0,0 +1,106 @@ +# Seven separated A2 contractions with an unchanged paid profile + +On each exact PR3734 provider, seven separated three-ADD blocks contract to +two ADDs without crossing a native event. Beyond PR3998's credited consecutive +A1858 contraction, this removes **seven forward and five inverse-cleanup ADDs**. +Against the original PR3734 words the combined saving is eight forward and six +cleanup ADDs. The entire recursive histogram remains +`{1:2440,2:725,3:224,4:102,5:20,8:8}`: 3,519 children and rank mass 5,134. +There is **no recursive-moment or kappa gain**, and no measured runtime claim. + +The changed premise is a literal event-graph contraction across strictly +disjoint scalar events. This is outside PR3998's consecutive domain and the +fixed-graph retiming domains. The seven new blocks retain their exact original ordered frames; +every intervening event must avoid all three selected registers. Prelude, +centre and native-warp boundaries remain fixed. It allocates no register or +buffer. The complete favorable frame bill already gives no recursive saving, +so this result stops at the frozen scalar witness rather than opening another +dependent optimization round. + +## Exact frozen scope + +Sources are PR3998 head `389268a6b5e0373a3125d5c6fcd6995f4ea324f5`, +which retains the two PR3734 providers at +`fa041037a3374eaa08feeca0b26a5d6893194147`. All source bytes, blobs and hashes +are bound in `SOURCES.json`; package-local exports remove any pending-history +dependency. Only those two old providers are certified. The retained PR3945 +notice is attribution, not an applicability claim about its later words. + +Seven new sites use original zero-based coordinates: + +| Section | Three ADD indices | +|---|---| +| B | 4, 53, 54 | +| B | 7, 49, 50 | +| restore | 20, 21, 36 | +| restore | 22, 23, 38 | +| restore | 26, 27, 51 | +| restore | 30, 31, 62 | +| restore | 32, 33, 73 | + +For example, at B4/B53/B54, all three frames are span(30): + +``` +196 += 518; 196 -= 588; 588 -= 518 + equals +588 -= 518; 196 -= 588 +``` + +The equality holds over the rationals on arbitrary dirty inputs. Selected +events can be gathered because every intervening event is disjoint from all +three registers. Every source gate, replacement, index and canonical edited +word/cleanup digest is retained in `data.json`; full words are reconstructed +in memory without modifying inputs. This is a fixed witness certificate, +not a complete search or a graph-normal-form theorem. + +## Evidence and reproduction + +Python 3.12 or later, standard library only: + +``` +python3 -B scripts/research_package.py --package research/staged544-separated-a2 +``` + +`PROOF.md` gives local composition, frame-boundary and projected inverse-cleanup +arguments. The separate checker compares all 149 complete live-register frame +states at fixed boundaries for source, credited and final words in each provider, +and recomputes every intermediate charge. It supplies seven semantic rejection +controls per provider, alongside 40 production API/CLI controls. The primary verifier reuses the authenticated, unchanged credited +`audit_core.py` for the complete frame bill, hygiene and free-operator +ordinary/dual/reverse/cleanup replay. This reuse is not a new independent +interpreter. `independent.py` supplies separately implemented scoped checks; +`test_verify.py` exercises semantic and damaged-input controls. Registered +commands are read-only and Git-free. Exact measured validation and publication +receipts are recorded in the PR and handoff; a PASS is not full supplier admission. + +All native descriptors and their order, helper entrances/exits, cut, wrappers, +initial corrections and nonedited fields are retained. Warp event indices only +account for deleted B instructions within their original cut. Physical owner +scheduling, signed native lowering, finite-width precision/stock/tapes and +all-size/outer/BIT obligations are inherited or unknown, never zero. + +## Open next questions + +- Can a different graph remove a paid frame transition? First specify the + replacement boundary and complete favorable bill. These seven sites leave + every rank count unchanged; another seed or larger separated scan is not + justified by this result alone. +- Does one later exact source word admit these contractions? Pin it and recheck + every source index, boundary, cleanup and full invoice before claiming reuse. + No PR3945 or later-word applicability is established here. + +## Credit and status + +Chris R / Clear1nsight PR3998 supplies the A2 identity, consecutive A1858 +contraction, proof context and authenticated source exports. Dataisfire supplies +the PR3734 literal providers. Sagar Thakrar, roger-sato and Arham Tahir supply +the retained auditor lineage. Jeremy Kothe and Dugongue's PR3945/3863 supply +rank-profile and complete-budget context. PR1865 by 1337isnot1337 is an earlier +nonconsecutive commuting C3 fanout construction, with a different identity and +source; no general priority for nonconsecutive commuting rewrites is claimed. +Full native/compiler/owner/source lineage is retained unchanged under `source/`. + +New fixed-witness contraction and checks by ToikY with substantial OpenAI Codex +assistance, including separate AI proof and test contexts. Apache-2.0. No +independent human or formal-kernel acceptance, new supplier, merge, closure or +selected-frontier change is claimed. diff --git a/research/staged544-separated-a2/SOURCES.json b/research/staged544-separated-a2/SOURCES.json new file mode 100644 index 0000000000..1080b57e70 --- /dev/null +++ b/research/staged544-separated-a2/SOURCES.json @@ -0,0 +1,107 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ], + "source_exports": [ + { + "path": "research/staged544-separated-a2/inputs/BORROW-WORD-base.json.gz", + "origin_repository": "Clear1nsight/integer-mult-bounds", + "origin_commit": "389268a6b5e0373a3125d5c6fcd6995f4ea324f5", + "origin_path": "research/staged544-a2-graph-rewrite/inputs/BORROW-WORD-43base.json.gz", + "git_blob": "674ea18ade4af85ca865fb08dc973637a09e30e6", + "sha256": "5ca4be99851f8878cbfe0fd6c454df926b11218f17feefa1664721cf03156699", + "bytes": 72769, + "usage": "Byte-exact package-local frozen predecessor export. PR3734 words and credited auditor reused; source3998 retains full attribution." + }, + { + "path": "research/staged544-separated-a2/inputs/BORROW-WORD-extra.json.gz", + "origin_repository": "Clear1nsight/integer-mult-bounds", + "origin_commit": "389268a6b5e0373a3125d5c6fcd6995f4ea324f5", + "origin_path": "research/staged544-a2-graph-rewrite/inputs/BORROW-WORD-43extra.json.gz", + "git_blob": "b17e2be67e327f04802fd034c344fe4253c13a4a", + "sha256": "965268a9be73d3f62e7ef680d18f108cf064bfe1f44b82157baa61443232904e", + "bytes": 72766, + "usage": "Byte-exact package-local frozen predecessor export. PR3734 words and credited auditor reused; source3998 retains full attribution." + }, + { + "path": "research/staged544-separated-a2/source/audit_core.py", + "origin_repository": "Clear1nsight/integer-mult-bounds", + "origin_commit": "389268a6b5e0373a3125d5c6fcd6995f4ea324f5", + "origin_path": "research/staged544-a2-graph-rewrite/vendor/audit_core.py", + "git_blob": "8b5e1d5f2a106402f036b63028ecef31a4e4c462", + "sha256": "888679ca8502cdcb100420fe5382a052529a494bf76cb332928b86e62612b951", + "bytes": 19364, + "usage": "Byte-exact package-local frozen predecessor export. PR3734 words and credited auditor reused; source3998 retains full attribution." + }, + { + "path": "research/staged544-separated-a2/source/SOURCE-CREDITS.md", + "origin_repository": "Clear1nsight/integer-mult-bounds", + "origin_commit": "389268a6b5e0373a3125d5c6fcd6995f4ea324f5", + "origin_path": "research/staged544-a2-graph-rewrite/vendor/SOURCE-CREDITS.md", + "git_blob": "c054fad87eeaa510865e682ee0c976c4cd728da2", + "sha256": "d4a13d8b8ed9cdb594f00efb3d1a336e09d934423330f02a1514308a720c278b", + "bytes": 2882, + "usage": "Byte-exact package-local frozen predecessor export. PR3734 words and credited auditor reused; source3998 retains full attribution." + }, + { + "path": "research/staged544-separated-a2/source/PR3998-PROOF.md", + "origin_repository": "Clear1nsight/integer-mult-bounds", + "origin_commit": "389268a6b5e0373a3125d5c6fcd6995f4ea324f5", + "origin_path": "research/staged544-a2-graph-rewrite/PROOF.md", + "git_blob": "afa6241fdaee6da1e567eb5ba74b780f9121ba8d", + "sha256": "0bbec6ba5b03e40e571f7f4a89e5776441a33b6ede41beeb80153ffad39d124f", + "bytes": 11251, + "usage": "Byte-exact package-local frozen predecessor export. PR3734 words and credited auditor reused; source3998 retains full attribution." + }, + { + "path": "research/staged544-separated-a2/source/PR3998-README.md", + "origin_repository": "Clear1nsight/integer-mult-bounds", + "origin_commit": "389268a6b5e0373a3125d5c6fcd6995f4ea324f5", + "origin_path": "research/staged544-a2-graph-rewrite/README.md", + "git_blob": "dcd14ef45bcfb102d030e3f87a0bb2bf80d57ade", + "sha256": "d935e7d10e2935ca82a3ba952308d73b78e76a9039cb335682f1fc5ea3b580d7", + "bytes": 6498, + "usage": "Byte-exact package-local frozen predecessor export. PR3734 words and credited auditor reused; source3998 retains full attribution." + }, + { + "path": "research/staged544-separated-a2/source/PR3945-NATIVE-LINEAGE-NOTICE", + "origin_repository": "Clear1nsight/integer-mult-bounds", + "origin_commit": "389268a6b5e0373a3125d5c6fcd6995f4ea324f5", + "origin_path": "research/staged544-a2-graph-rewrite/vendor/PR3945-NATIVE-LINEAGE-NOTICE", + "git_blob": "380e979f0e84e00a22bd890615d87cc4684ad740", + "sha256": "ee0c73ca35877aad0e0b6adc560a3881cb82276dba4cf2d4fc58cd19e57cc420", + "bytes": 2456, + "usage": "Byte-exact package-local frozen predecessor export. PR3734 words and credited auditor reused; source3998 retains full attribution." + } + ], + "source_export_contract": "No foreign pending commit is a Git-history dependency. Seven exact exports are package-local; all SHA256/blob pins are recorded here. Primary authenticates core/words before execution; separate checker authenticates its own input closure. audit_core is unchanged credited reuse, not a new independent interpreter. Generic source-history checks cover canonical provenance, not scientific acceptance.", + "published_predecessor_comparison": { + "repository": "Clear1nsight/integer-mult-bounds", + "commit": "389268a6b5e0373a3125d5c6fcd6995f4ea324f5", + "field_pointer": "/census/contractions/records/0/canonical_word_sha256", + "base": { + "path": "research/staged544-a2-graph-rewrite/RESULT-base.json", + "git_blob": "a7ba2d9a7cdc5455841c5fe4a926cedb80f97324", + "canonical_word_sha256": "32415e93a50f0fdab5fa144da05977fe34bc8340bf967b91c7f7f0bc312df994" + }, + "extra": { + "path": "research/staged544-a2-graph-rewrite/RESULT-extra.json", + "git_blob": "c8b81e77e0ccf00a909e36f1083eddf9b29822a4", + "canonical_word_sha256": "439ce3544b68e3dffdb0cb4496fbc92330e825592515bc28c95580807c9d232d" + }, + "status": "Live inspected publishedfields; fullRESULTfiles are not runtime inputs. Primary reconstructs the credited word, compares these hardcoded targets and replays its semantics." + } +} diff --git a/research/staged544-separated-a2/TASK.json b/research/staged544-separated-a2/TASK.json new file mode 100644 index 0000000000..cbd9a1b8a9 --- /dev/null +++ b/research/staged544-separated-a2/TASK.json @@ -0,0 +1,85 @@ +{ + "schema_version": 1, + "task_id": "scalar-to-moment", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "scalar-to-moment", + "question": "Can one known scalar simplification be converted into an actual paid-profile improvement?", + "starting_points": [ + "research/r439-bsection-stars-seed01/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Derive the changed legal frame itinerary and exact child histogram.", + "Prove a scoped obstruction showing why that scalar gain cannot change the paid contract." + ], + "acceptance_gate": "An unchanged histogram is not a kappa gain; record any separate runtime or proof benefit explicitly.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Observe that the positive control improves scalar counts while retaining the paid histogram.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one simplification and derive the complete changed frame itinerary, or prove why it cannot change the histogram.", + "bottleneck_link": "A legal change to the histogram, not addition count alone, is the bridge to an exponent gain.", + "allowed_variations": [ + "One existing scalar simplification and one proposed frame-path change." + ], + "scope_change_triggers": [ + "Submitting only another scalar count as completion of a paid-profile task." + ], + "overlap_terms": [ + "scalar simplification", + "paid profile", + "R439" + ] + }, + "scope_status": "changed", + "actual_scope": "Seven strict separated inverse-A2 contractions on each frozen PR3734 provider, layered on PR3998 consecutive contraction; exact scalar/cleanup saving and unchanged full recursive histogram.", + "scope_change_reason": "Handoff-first/source inspection found separated events explicitly outside PR3998. The historical R439 first command was attempted from an available sparse retained checkout and failed because build.py is omitted; no unrelated closure repair was attempted. The credited PR3998 A1858 contraction is the source-bound positive control for the changed word.", + "bottleneck_link": "Tests the bridge from changed literal scalar graph to recursive paid cost. Twelve fewer executed ADDs than PR3998 have no paid-profile gain; stop dependent optimization rather than infer a kappa improvement.", + "budget_minutes": 60, + "stop_rule": "Freeze seven separated sites plus credited A1858; certify both exact words and cleanup. Stop further search/construction if paid histogram is unchanged and finish verification of this partial result; stop entirely on semantic/frame failure or covered scope. Science cutoff09:41:56UTC; final15minutes reserved for verification and handoff.", + "outcome": "partial", + "evidence": "Written arbitrary-input composition and projected-cleanup proof; exact rational local maps, frozen-word free-operator replay, complete credited invoice/hygiene and separate checker with semantic controls.", + "author": "ToikY", + "ai_assistance": "Substantial OpenAI Codex assistance in implementation, proof, testing and separate AI review contexts. No independent human or formal-kernel acceptance.", + "selection": { + "method": "handoff-first followed by named catalogue provenance; no random reroll", + "handoff": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/pull/3998#issuecomment-6263605648", + "checked_at_utc": "2026-10-19T09:02:33Z", + "entry_open_pr_bodies_including_drafts": 711, + "pagination": "seven100-record pages plus11-recordpage8 and emptypage9, all711uniqueIDs", + "decision": "Narrow after exact bill: useful frozen scalar-graph contraction with unchanged paid histogram; no dependent native construction. Original3998 owns A1858 identity, C3/fanout predecessor1865 has a different identity and source; fixed-graph retiming predecessors do not cover new contractions.", + "coverage_limit": "All open PR titles/bodies including drafts, repository overlap helper, bounded live1166/active-board/source comments and targeted main ledger checked. Broader Discussions, closed diffs and arbitrary code coverage partial.", + "pre_submission": { + "checked_at_utc": "2026-10-19T09:12:43Z", + "canonical_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "priority_revision": 6, + "source_head": "389268a6b5e0373a3125d5c6fcd6995f4ea324f5", + "newest_open_pr_bodies": 100, + "latest_new_pr": 4018, + "decision": "Continue frozen PR3734 witness. Main/catalogue/selected hashes unchanged. Source3998 author new local-only PR3945 Gaussian3\u20138window handoff explicitly distinguishes our separatedA2class/source and releases its scope. PR4016fixednativecone refits and4017rankfive dirtylattice are different premises; no applicability or dependent expansion inferred." + } + }, + "open_questions": [ + { + "question": "Can a changed graph reduce an actual paid frame transition rather than only scalar ADD count?", + "why_it_matters": "The entire histogram is unchanged by this frozen construction, so the recursive moment cannot improve.", + "first_step": "Specify a different graph/boundary and a complete favorable bill before any new dependent search.", + "blocked_by": "This package provides neither such a candidate nor native/owner/precision admission." + }, + { + "question": "Does this scalar contraction apply to a later source word?", + "why_it_matters": "Only the two pinned PR3734 providers are certified; PR3945 applicability must not be inferred.", + "first_step": "Pin the later exact word and recheck sites, all boundaries, cleanup, invoice and inherited assumptions.", + "blocked_by": "Later source and physical contracts are outside this session; no automatic expansion is requested." + } + ] +} diff --git a/research/staged544-separated-a2/VERIFY.json b/research/staged544-separated-a2/VERIFY.json new file mode 100644 index 0000000000..e42e1c972a --- /dev/null +++ b/research/staged544-separated-a2/VERIFY.json @@ -0,0 +1,49 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--provider", + "base" + ], + "timeout_seconds": 240, + "checks": "Authenticated frozen base word; rational local witnesses, frame bill/hygiene, ordinary+dual/reverse/cleanup semantics with all723formalinputs; typedreceipt." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--provider", + "extra" + ], + "timeout_seconds": 240, + "checks": "Authenticated frozen extra word; rational local witnesses, frame bill/hygiene, ordinary+dual/reverse/cleanup semantics with all723formalinputs; typedreceipt." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Separate exact local/composition/projected-cleanup checker; no credited interpreter imported." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Semantic graph, cut, frame, source and receipt damage controls; normal and optimized rejection behavior." + } + ] +} diff --git a/research/staged544-separated-a2/data.json b/research/staged544-separated-a2/data.json new file mode 100644 index 0000000000..f91c78bed3 --- /dev/null +++ b/research/staged544-separated-a2/data.json @@ -0,0 +1,1839 @@ +{ + "providers": { + "base": { + "additional_cleanup_add_saving": 5, + "additional_forward_add_saving": 7, + "known_sites": 1, + "native_operators_changed": false, + "new_kappa": false, + "new_sites": 7, + "new_supplier": false, + "provider": "base", + "recursive_moment_changed": false, + "schema_version": 1, + "sites": [ + { + "crossed_disjoint_events": 0, + "gates": [ + [ + "add", + 457, + 475, + -1, + 1, + [ + 82, + 42 + ] + ], + [ + "add", + 456, + 457, + 1, + 1, + [ + 82, + 42 + ] + ], + [ + "add", + 456, + 475, + 1, + 1, + [ + 82, + 42 + ] + ] + ], + "indices": [ + 1858, + 1859, + 1860 + ], + "known": true, + "removed_position": 2, + "replacement": [ + [ + "add", + 456, + 457, + 1, + 1, + [ + 42, + 82 + ] + ], + [ + "add", + 457, + 475, + -1, + 1, + [ + 42, + 82 + ] + ] + ], + "section": "A", + "support": [ + 456, + 457, + 475 + ] + }, + { + "crossed_disjoint_events": 48, + "gates": [ + [ + "add", + 196, + 518, + 1, + 1, + [ + 30 + ] + ], + [ + "add", + 196, + 588, + -1, + 1, + [ + 30 + ] + ], + [ + "add", + 588, + 518, + -1, + 1, + [ + 30 + ] + ] + ], + "indices": [ + 4, + 53, + 54 + ], + "known": false, + "removed_position": 0, + "replacement": [ + [ + "add", + 588, + 518, + -1, + 1, + [ + 30 + ] + ], + [ + "add", + 196, + 588, + -1, + 1, + [ + 30 + ] + ] + ], + "section": "B", + "support": [ + 196, + 518, + 588 + ] + }, + { + "crossed_disjoint_events": 41, + "gates": [ + [ + "add", + 187, + 506, + 1, + 1, + [ + 30 + ] + ], + [ + "add", + 187, + 586, + 1, + 2, + [ + 30 + ] + ], + [ + "add", + 586, + 506, + 2, + 1, + [ + 30 + ] + ] + ], + "indices": [ + 7, + 49, + 50 + ], + "known": false, + "removed_position": 0, + "replacement": [ + [ + "add", + 586, + 506, + 2, + 1, + [ + 30 + ] + ], + [ + "add", + 187, + 586, + 1, + 2, + [ + 30 + ] + ] + ], + "section": "B", + "support": [ + 187, + 506, + 586 + ] + }, + { + "crossed_disjoint_events": 14, + "gates": [ + [ + "add", + 448, + 231, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ], + [ + "add", + 484, + 448, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ], + [ + "add", + 484, + 231, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ] + ], + "indices": [ + 20, + 21, + 36 + ], + "known": false, + "removed_position": 2, + "replacement": [ + [ + "add", + 484, + 448, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ], + [ + "add", + 448, + 231, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ] + ], + "section": "restore", + "support": [ + 231, + 448, + 484 + ] + }, + { + "crossed_disjoint_events": 14, + "gates": [ + [ + "add", + 449, + 226, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ], + [ + "add", + 485, + 449, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ], + [ + "add", + 485, + 226, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ] + ], + "indices": [ + 22, + 23, + 38 + ], + "known": false, + "removed_position": 2, + "replacement": [ + [ + "add", + 485, + 449, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ], + [ + "add", + 449, + 226, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ] + ], + "section": "restore", + "support": [ + 226, + 449, + 485 + ] + }, + { + "crossed_disjoint_events": 23, + "gates": [ + [ + "add", + 451, + 228, + -1, + 1, + [ + 256, + 128, + 64, + 38, + 20, + 10, + 1 + ] + ], + [ + "add", + 509, + 451, + -1, + 1, + [ + 256, + 128, + 64, + 38, + 20, + 10, + 1 + ] + ], + [ + "add", + 509, + 228, + -1, + 1, + [ + 256, + 128, + 64, + 38, + 20, + 10, + 1 + ] + ] + ], + "indices": [ + 26, + 27, + 51 + ], + "known": false, + "removed_position": 2, + "replacement": [ + [ + "add", + 509, + 451, + -1, + 1, + [ + 256, + 128, + 64, + 38, + 20, + 10, + 1 + ] + ], + [ + "add", + 451, + 228, + -1, + 1, + [ + 256, + 128, + 64, + 38, + 20, + 10, + 1 + ] + ] + ], + "section": "restore", + "support": [ + 228, + 451, + 509 + ] + }, + { + "crossed_disjoint_events": 30, + "gates": [ + [ + "add", + 453, + 7, + -1, + 1, + [ + 256, + 128, + 64, + 32, + 19, + 11, + 6 + ] + ], + [ + "add", + 533, + 453, + 2, + 1, + [ + 256, + 128, + 64, + 32, + 19, + 11, + 6 + ] + ], + [ + "add", + 533, + 7, + 2, + 1, + [ + 256, + 128, + 64, + 32, + 19, + 11, + 6 + ] + ] + ], + "indices": [ + 30, + 31, + 62 + ], + "known": false, + "removed_position": 2, + "replacement": [ + [ + "add", + 533, + 453, + 2, + 1, + [ + 256, + 128, + 64, + 32, + 19, + 11, + 6 + ] + ], + [ + "add", + 453, + 7, + -1, + 1, + [ + 256, + 128, + 64, + 32, + 19, + 11, + 6 + ] + ] + ], + "section": "restore", + "support": [ + 7, + 453, + 533 + ] + }, + { + "crossed_disjoint_events": 39, + "gates": [ + [ + "add", + 454, + 236, + -1, + 1, + [ + 256, + 128, + 64, + 37, + 21, + 8, + 3 + ] + ], + [ + "add", + 556, + 454, + 2, + 1, + [ + 256, + 128, + 64, + 37, + 21, + 8, + 3 + ] + ], + [ + "add", + 556, + 236, + 2, + 1, + [ + 256, + 128, + 64, + 37, + 21, + 8, + 3 + ] + ] + ], + "indices": [ + 32, + 33, + 73 + ], + "known": false, + "removed_position": 2, + "replacement": [ + [ + "add", + 556, + 454, + 2, + 1, + [ + 256, + 128, + 64, + 37, + 21, + 8, + 3 + ] + ], + [ + "add", + 454, + 236, + -1, + 1, + [ + 256, + 128, + 64, + 37, + 21, + 8, + 3 + ] + ] + ], + "section": "restore", + "support": [ + 236, + 454, + 556 + ] + } + ], + "words": { + "credited_3998": { + "canonical_word_sha256": "32415e93a50f0fdab5fa144da05977fe34bc8340bf967b91c7f7f0bc312df994", + "cleanup_sha256": "7c2a181ac7fc6a087f5c7cce346650e0bb773f5dafa82ca966081a4a6440c336", + "helper_widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + }, + "lengths": { + "A": 4078, + "B": 1869, + "cleanup": 5223, + "restore": 212 + }, + "native_operations": 72, + "primitive_counts": { + "A": { + "add": 3556, + "scale": 498, + "warp": 24 + }, + "B": { + "add": 1796, + "scale": 73, + "warp": 0 + }, + "cleanup": { + "add": 4632, + "scale": 519, + "warp": 72 + }, + "restore": { + "add": 196, + "scale": 16, + "warp": 0 + } + }, + "profile": { + "1": 2440, + "2": 725, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "semantics": { + "arbitrary_dirty_buffers": 91, + "buffer_self_map": "identity", + "buffer_to_live_leaks": 0, + "cleanup_boundary_both_directions": true, + "dual": true, + "dual_matrix_sha256": "9bace9fb7525f64d5418ab54af173df7d320c898e980e89be8a90d280adb3744", + "live_inputs": 632, + "matrix_dimension": 723, + "ordinary": true, + "ordinary_matrix_sha256": "c8ea87b1598c9bbc2b0be63217772110ff450ad12eff19aaf05a84239eb5d380", + "reverse_equals_ordinary": true + } + }, + "separated": { + "canonical_word_sha256": "0a36faedd98f7b80304469c16e6c2f074850d6bd054030366713a08805cd3300", + "cleanup_sha256": "a20cef30d1adbaa529d96f2055bf3f203cbf1f15438de04ec34c3fb7a7372906", + "helper_widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + }, + "lengths": { + "A": 4078, + "B": 1867, + "cleanup": 5218, + "restore": 207 + }, + "native_operations": 72, + "primitive_counts": { + "A": { + "add": 3556, + "scale": 498, + "warp": 24 + }, + "B": { + "add": 1794, + "scale": 73, + "warp": 0 + }, + "cleanup": { + "add": 4627, + "scale": 519, + "warp": 72 + }, + "restore": { + "add": 191, + "scale": 16, + "warp": 0 + } + }, + "profile": { + "1": 2440, + "2": 725, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "semantics": { + "arbitrary_dirty_buffers": 91, + "buffer_self_map": "identity", + "buffer_to_live_leaks": 0, + "cleanup_boundary_both_directions": true, + "dual": true, + "dual_matrix_sha256": "9bace9fb7525f64d5418ab54af173df7d320c898e980e89be8a90d280adb3744", + "live_inputs": 632, + "matrix_dimension": 723, + "ordinary": true, + "ordinary_matrix_sha256": "c8ea87b1598c9bbc2b0be63217772110ff450ad12eff19aaf05a84239eb5d380", + "reverse_equals_ordinary": true + } + }, + "source": { + "canonical_word_sha256": "a140d980692fb1688b6b85021e06e2aea7d97eb3fd2b09cbd6c47afb0cc7f9da", + "cleanup_sha256": "cfcb7fbc44fb3e14c6edd781f1fb57ea25ade9a96c0ef4873bf8d4c1eb7a02e2", + "helper_widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + }, + "lengths": { + "A": 4079, + "B": 1869, + "cleanup": 5224, + "restore": 212 + }, + "native_operations": 72, + "primitive_counts": { + "A": { + "add": 3557, + "scale": 498, + "warp": 24 + }, + "B": { + "add": 1796, + "scale": 73, + "warp": 0 + }, + "cleanup": { + "add": 4633, + "scale": 519, + "warp": 72 + }, + "restore": { + "add": 196, + "scale": 16, + "warp": 0 + } + }, + "profile": { + "1": 2440, + "2": 725, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "semantics": { + "arbitrary_dirty_buffers": 91, + "buffer_self_map": "identity", + "buffer_to_live_leaks": 0, + "cleanup_boundary_both_directions": true, + "dual": true, + "dual_matrix_sha256": "9bace9fb7525f64d5418ab54af173df7d320c898e980e89be8a90d280adb3744", + "live_inputs": 632, + "matrix_dimension": 723, + "ordinary": true, + "ordinary_matrix_sha256": "c8ea87b1598c9bbc2b0be63217772110ff450ad12eff19aaf05a84239eb5d380", + "reverse_equals_ordinary": true + } + } + } + }, + "extra": { + "additional_cleanup_add_saving": 5, + "additional_forward_add_saving": 7, + "known_sites": 1, + "native_operators_changed": false, + "new_kappa": false, + "new_sites": 7, + "new_supplier": false, + "provider": "extra", + "recursive_moment_changed": false, + "schema_version": 1, + "sites": [ + { + "crossed_disjoint_events": 0, + "gates": [ + [ + "add", + 457, + 475, + -1, + 1, + [ + 82, + 42 + ] + ], + [ + "add", + 456, + 457, + 1, + 1, + [ + 82, + 42 + ] + ], + [ + "add", + 456, + 475, + 1, + 1, + [ + 82, + 42 + ] + ] + ], + "indices": [ + 1858, + 1859, + 1860 + ], + "known": true, + "removed_position": 2, + "replacement": [ + [ + "add", + 456, + 457, + 1, + 1, + [ + 42, + 82 + ] + ], + [ + "add", + 457, + 475, + -1, + 1, + [ + 42, + 82 + ] + ] + ], + "section": "A", + "support": [ + 456, + 457, + 475 + ] + }, + { + "crossed_disjoint_events": 48, + "gates": [ + [ + "add", + 196, + 518, + 1, + 1, + [ + 30 + ] + ], + [ + "add", + 196, + 588, + -1, + 1, + [ + 30 + ] + ], + [ + "add", + 588, + 518, + -1, + 1, + [ + 30 + ] + ] + ], + "indices": [ + 4, + 53, + 54 + ], + "known": false, + "removed_position": 0, + "replacement": [ + [ + "add", + 588, + 518, + -1, + 1, + [ + 30 + ] + ], + [ + "add", + 196, + 588, + -1, + 1, + [ + 30 + ] + ] + ], + "section": "B", + "support": [ + 196, + 518, + 588 + ] + }, + { + "crossed_disjoint_events": 41, + "gates": [ + [ + "add", + 187, + 506, + 1, + 1, + [ + 30 + ] + ], + [ + "add", + 187, + 586, + 1, + 2, + [ + 30 + ] + ], + [ + "add", + 586, + 506, + 2, + 1, + [ + 30 + ] + ] + ], + "indices": [ + 7, + 49, + 50 + ], + "known": false, + "removed_position": 0, + "replacement": [ + [ + "add", + 586, + 506, + 2, + 1, + [ + 30 + ] + ], + [ + "add", + 187, + 586, + 1, + 2, + [ + 30 + ] + ] + ], + "section": "B", + "support": [ + 187, + 506, + 586 + ] + }, + { + "crossed_disjoint_events": 14, + "gates": [ + [ + "add", + 448, + 231, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ], + [ + "add", + 484, + 448, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ], + [ + "add", + 484, + 231, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ] + ], + "indices": [ + 20, + 21, + 36 + ], + "known": false, + "removed_position": 2, + "replacement": [ + [ + "add", + 484, + 448, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ], + [ + "add", + 448, + 231, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ] + ], + "section": "restore", + "support": [ + 231, + 448, + 484 + ] + }, + { + "crossed_disjoint_events": 14, + "gates": [ + [ + "add", + 449, + 226, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ], + [ + "add", + 485, + 449, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ], + [ + "add", + 485, + 226, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ] + ], + "indices": [ + 22, + 23, + 38 + ], + "known": false, + "removed_position": 2, + "replacement": [ + [ + "add", + 485, + 449, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ], + [ + "add", + 449, + 226, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ] + ], + "section": "restore", + "support": [ + 226, + 449, + 485 + ] + }, + { + "crossed_disjoint_events": 23, + "gates": [ + [ + "add", + 451, + 228, + -1, + 1, + [ + 256, + 128, + 64, + 38, + 20, + 10, + 1 + ] + ], + [ + "add", + 509, + 451, + -1, + 1, + [ + 256, + 128, + 64, + 38, + 20, + 10, + 1 + ] + ], + [ + "add", + 509, + 228, + -1, + 1, + [ + 256, + 128, + 64, + 38, + 20, + 10, + 1 + ] + ] + ], + "indices": [ + 26, + 27, + 51 + ], + "known": false, + "removed_position": 2, + "replacement": [ + [ + "add", + 509, + 451, + -1, + 1, + [ + 256, + 128, + 64, + 38, + 20, + 10, + 1 + ] + ], + [ + "add", + 451, + 228, + -1, + 1, + [ + 256, + 128, + 64, + 38, + 20, + 10, + 1 + ] + ] + ], + "section": "restore", + "support": [ + 228, + 451, + 509 + ] + }, + { + "crossed_disjoint_events": 30, + "gates": [ + [ + "add", + 453, + 7, + -1, + 1, + [ + 256, + 128, + 64, + 32, + 19, + 11, + 6 + ] + ], + [ + "add", + 533, + 453, + 2, + 1, + [ + 256, + 128, + 64, + 32, + 19, + 11, + 6 + ] + ], + [ + "add", + 533, + 7, + 2, + 1, + [ + 256, + 128, + 64, + 32, + 19, + 11, + 6 + ] + ] + ], + "indices": [ + 30, + 31, + 62 + ], + "known": false, + "removed_position": 2, + "replacement": [ + [ + "add", + 533, + 453, + 2, + 1, + [ + 256, + 128, + 64, + 32, + 19, + 11, + 6 + ] + ], + [ + "add", + 453, + 7, + -1, + 1, + [ + 256, + 128, + 64, + 32, + 19, + 11, + 6 + ] + ] + ], + "section": "restore", + "support": [ + 7, + 453, + 533 + ] + }, + { + "crossed_disjoint_events": 39, + "gates": [ + [ + "add", + 454, + 236, + -1, + 1, + [ + 256, + 128, + 64, + 37, + 21, + 8, + 3 + ] + ], + [ + "add", + 556, + 454, + 2, + 1, + [ + 256, + 128, + 64, + 37, + 21, + 8, + 3 + ] + ], + [ + "add", + 556, + 236, + 2, + 1, + [ + 256, + 128, + 64, + 37, + 21, + 8, + 3 + ] + ] + ], + "indices": [ + 32, + 33, + 73 + ], + "known": false, + "removed_position": 2, + "replacement": [ + [ + "add", + 556, + 454, + 2, + 1, + [ + 256, + 128, + 64, + 37, + 21, + 8, + 3 + ] + ], + [ + "add", + 454, + 236, + -1, + 1, + [ + 256, + 128, + 64, + 37, + 21, + 8, + 3 + ] + ] + ], + "section": "restore", + "support": [ + 236, + 454, + 556 + ] + } + ], + "words": { + "credited_3998": { + "canonical_word_sha256": "439ce3544b68e3dffdb0cb4496fbc92330e825592515bc28c95580807c9d232d", + "cleanup_sha256": "7c2a181ac7fc6a087f5c7cce346650e0bb773f5dafa82ca966081a4a6440c336", + "helper_widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + }, + "lengths": { + "A": 4078, + "B": 1869, + "cleanup": 5223, + "restore": 212 + }, + "native_operations": 72, + "primitive_counts": { + "A": { + "add": 3556, + "scale": 498, + "warp": 24 + }, + "B": { + "add": 1796, + "scale": 73, + "warp": 0 + }, + "cleanup": { + "add": 4632, + "scale": 519, + "warp": 72 + }, + "restore": { + "add": 196, + "scale": 16, + "warp": 0 + } + }, + "profile": { + "1": 2440, + "2": 725, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "semantics": { + "arbitrary_dirty_buffers": 91, + "buffer_self_map": "identity", + "buffer_to_live_leaks": 0, + "cleanup_boundary_both_directions": true, + "dual": true, + "dual_matrix_sha256": "9bace9fb7525f64d5418ab54af173df7d320c898e980e89be8a90d280adb3744", + "live_inputs": 632, + "matrix_dimension": 723, + "ordinary": true, + "ordinary_matrix_sha256": "c8ea87b1598c9bbc2b0be63217772110ff450ad12eff19aaf05a84239eb5d380", + "reverse_equals_ordinary": true + } + }, + "separated": { + "canonical_word_sha256": "0cc6001f57d842b39ccc8d508d26d86a8e2eda976161130940746f4b1d02bd96", + "cleanup_sha256": "a20cef30d1adbaa529d96f2055bf3f203cbf1f15438de04ec34c3fb7a7372906", + "helper_widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + }, + "lengths": { + "A": 4078, + "B": 1867, + "cleanup": 5218, + "restore": 207 + }, + "native_operations": 72, + "primitive_counts": { + "A": { + "add": 3556, + "scale": 498, + "warp": 24 + }, + "B": { + "add": 1794, + "scale": 73, + "warp": 0 + }, + "cleanup": { + "add": 4627, + "scale": 519, + "warp": 72 + }, + "restore": { + "add": 191, + "scale": 16, + "warp": 0 + } + }, + "profile": { + "1": 2440, + "2": 725, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "semantics": { + "arbitrary_dirty_buffers": 91, + "buffer_self_map": "identity", + "buffer_to_live_leaks": 0, + "cleanup_boundary_both_directions": true, + "dual": true, + "dual_matrix_sha256": "9bace9fb7525f64d5418ab54af173df7d320c898e980e89be8a90d280adb3744", + "live_inputs": 632, + "matrix_dimension": 723, + "ordinary": true, + "ordinary_matrix_sha256": "c8ea87b1598c9bbc2b0be63217772110ff450ad12eff19aaf05a84239eb5d380", + "reverse_equals_ordinary": true + } + }, + "source": { + "canonical_word_sha256": "309e6b90bad582081b90cce08f820da62ab11602a8298852cb7ef6f16b8942c8", + "cleanup_sha256": "cfcb7fbc44fb3e14c6edd781f1fb57ea25ade9a96c0ef4873bf8d4c1eb7a02e2", + "helper_widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + }, + "lengths": { + "A": 4079, + "B": 1869, + "cleanup": 5224, + "restore": 212 + }, + "native_operations": 72, + "primitive_counts": { + "A": { + "add": 3557, + "scale": 498, + "warp": 24 + }, + "B": { + "add": 1796, + "scale": 73, + "warp": 0 + }, + "cleanup": { + "add": 4633, + "scale": 519, + "warp": 72 + }, + "restore": { + "add": 196, + "scale": 16, + "warp": 0 + } + }, + "profile": { + "1": 2440, + "2": 725, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "semantics": { + "arbitrary_dirty_buffers": 91, + "buffer_self_map": "identity", + "buffer_to_live_leaks": 0, + "cleanup_boundary_both_directions": true, + "dual": true, + "dual_matrix_sha256": "9bace9fb7525f64d5418ab54af173df7d320c898e980e89be8a90d280adb3744", + "live_inputs": 632, + "matrix_dimension": 723, + "ordinary": true, + "ordinary_matrix_sha256": "c8ea87b1598c9bbc2b0be63217772110ff450ad12eff19aaf05a84239eb5d380", + "reverse_equals_ordinary": true + } + } + } + } + }, + "schema_version": 1 +} diff --git a/research/staged544-separated-a2/independent.py b/research/staged544-separated-a2/independent.py new file mode 100644 index 0000000000..501c54c11c --- /dev/null +++ b/research/staged544-separated-a2/independent.py @@ -0,0 +1,409 @@ +#!/usr/bin/env python3 +"""Independent fixed-site A2, cleanup and point-set frame certificate. + +No primary or predecessor executable is imported. The proof is compositional +on arbitrary inputs, rather than a second full free-operator interpreter. +Standard library, Python 3.9+. Apache-2.0; ToikY with OpenAI Codex assistance. +""" +import argparse +from collections import Counter +from copy import deepcopy +from fractions import Fraction +from functools import lru_cache +import gzip +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +N, V = 704, 112 +FULL_BASIS = [256, 128, 64, 32, 16, 8, 4, 2, 1] +PINS = { + 'base': '5ca4be99851f8878cbfe0fd6c454df926b11218f17feefa1664721cf03156699', + 'extra': '965268a9be73d3f62e7ef680d18f108cf064bfe1f44b82157baa61443232904e', +} +# This is the fixed witness, not a census or a search algorithm. +PLAN = ( + ('A', (1858, 1859, 1860), 2), + ('B', (4, 53, 54), 0), ('B', (7, 49, 50), 0), + ('restore', (20, 21, 36), 2), ('restore', (22, 23, 38), 2), + ('restore', (26, 27, 51), 2), ('restore', (30, 31, 62), 2), + ('restore', (32, 33, 73), 2), +) +PROFILE = {'1': 2440, '2': 725, '3': 224, '4': 102, '5': 20, '8': 8} +WIDTHS = {'4': 26, '5': 2, '6': 18, '7': 53, '8': 96, '9': 213} +KNOWN = { + 'base': '32415e93a50f0fdab5fa144da05977fe34bc8340bf967b91c7f7f0bc312df994', + 'extra': '439ce3544b68e3dffdb0cb4496fbc92330e825592515bc28c95580807c9d232d', +} + + +class Rejected(ValueError): + pass + + +def require(condition, message): + if not condition: + raise Rejected(message) + + +def no_duplicates(pairs): + answer = {} + for key, value in pairs: + require(key not in answer, 'duplicate JSON key') + answer[key] = value + return answer + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':')).encode('ascii') + + +def sha(value): + return hashlib.sha256(canonical(value)).hexdigest() + + +def target(r): + return V <= r < 2 * V + + +def support(gate): + require(gate[0] in ('add', 'scale'), 'non-scalar barrier') + registers = gate[1:3] if gate[0] == 'add' else gate[1:2] + require(all(type(r) is int and 0 <= r < N for r in registers), 'register domain') + return frozenset(registers) + + +def scalar(gate): + i = 3 if gate[0] == 'add' else 2 + a, b = gate[i:i + 2] + require(type(a) is int and type(b) is int and b != 0 and a != 0, 'nonzero rational') + return Fraction(a, b) + + +def coefficients(gates, registers): + """Propagate three independent coordinate columns using exact fractions.""" + result = [] + for column in range(len(registers)): + values = {r: Fraction(k == column) for k, r in enumerate(registers)} + for gate in gates: + require(gate[0] == 'add', 'A2 alphabet') + values[gate[1]] += scalar(gate) * values[gate[2]] + result.append(tuple(values[r] for r in registers)) + return tuple(result) + + +def certified_sites(word, plan=PLAN): + records, occupied = [], set() + for number, (section, indices, central) in enumerate(plan): + require(section in ('A', 'B', 'restore'), 'section domain') + require(len(indices) == 3 and all(type(i) is int for i in indices) + and 0 <= indices[0] < indices[1] < indices[2] < len(word[section]), 'site indices') + require(type(central) is int and central in (0, 1, 2), 'central position') + if section == 'A': + require(indices[0] >= word['prelude_events'], 'prelude barrier') + if section == 'B': + require(not any(indices[0] < w[0] <= indices[-1] for w in word['warps']), + 'native warp barrier') + gates = [word[section][i] for i in indices] + require(all(g[0] == 'add' and len(g) == 6 for g in gates), 'three ADDs') + touched = frozenset().union(*(support(g) for g in gates)) + require(len(touched) == 3 and len({tuple(g[1:3]) for g in gates}) == 3, + 'three distinct directed A2 edges') + require(not occupied.intersection(touched), 'overlapping site support') + occupied.update(touched) + require(gates[0][-1] == gates[1][-1] == gates[2][-1], 'common ordered frame') + for i in range(indices[0], indices[-1] + 1): + if i not in indices: + require(not support(word[section][i]).intersection(touched), 'intervening dependency') + replacement = [deepcopy(g) for j, g in reversed(list(enumerate(gates))) if j != central] + require(coefficients(gates, sorted(touched)) == coefficients(replacement, sorted(touched)), + 'exact three-coordinate identity') + # Match the credited PR3998 publication's basis order on this old site. + known = (section, indices, central) == PLAN[0] + if known: + for gate in replacement: + gate[-1] = [42, 82] + records.append({'section': section, 'indices': list(indices), 'removed_position': central, + 'known': known, 'support': sorted(touched), 'gates': deepcopy(gates), + 'replacement': replacement, + 'crossed_disjoint_events': indices[-1] - indices[0] - 2}) + return records + + +def ordinary_events(word): + yield from word['A'][word['prelude_events']:] + positions = {} + for k, warp in enumerate(word['warps'], 1): + positions.setdefault(warp[0], []).append(['warp', warp[1], k]) + for i in range(len(word['B']) + 1): + yield from positions.get(i, ()) + if i < len(word['B']): + yield word['B'][i] + yield from word['restore'] + + +def inverse_cleanup(word): + """Invert autonomous non-target block, then rename protected buffers.""" + protected = {int(r) for r in word['helper_final']} + rename = lambda r: N + r if r in protected else r + answer = [] + for gate in reversed(list(ordinary_events(word))): + kind, dst = gate[:2] + if kind == 'warp': + answer.append(['warp', rename(dst), -gate[2], FULL_BASIS[:]]) + elif not target(dst): + if kind == 'add': + require(not target(gate[2]), 'non-target reads target') + answer.append(['add', rename(dst), rename(gate[2]), -gate[3], gate[4], FULL_BASIS[:]]) + else: + require(kind == 'scale', 'cleanup alphabet') + answer.append(['scale', rename(dst), gate[3], gate[2], FULL_BASIS[:]]) + return answer + + +def reconstruct(word, records): + edited = deepcopy(word) + for section in ('A', 'B', 'restore'): + selected = [r for r in records if r['section'] == section] + first = {r['indices'][0]: r['replacement'] for r in selected} + suppressed = {i for r in selected for i in r['indices']} + edited[section], old_to_new = [], {} + for i, gate in enumerate(word[section]): + old_to_new[i] = len(edited[section]) + if i in first: + edited[section].extend(deepcopy(first[i])) + elif i not in suppressed: + edited[section].append(deepcopy(gate)) + old_to_new[len(word[section])] = len(edited[section]) + if section == 'B': + for warp in edited['warps']: + warp[0] = old_to_new[warp[0]] + edited['cleanup'] = inverse_cleanup(edited) + require(all(edited[k] == word[k] for k in word if k not in ('A', 'B', 'restore', 'cleanup', 'warps')), + 'unrelated field changed') + require([w[1:] for w in edited['warps']] == [w[1:] for w in word['warps']], 'native record changed') + return edited + + +@lru_cache(maxsize=None) +def span(basis): + result = {0} + for vector in basis: + require(type(vector) is int and 0 <= vector < 512, 'binary vector domain') + result |= {point ^ vector for point in result} + return frozenset(result) + + +def rank(points): + length = len(points) + require(length > 0 and length & (length - 1) == 0, 'binary subspace cardinality') + return length.bit_length() - 1 + + +FULL = frozenset(range(512)) +ZERO = frozenset([0]) + + +def binary_map(columns): + require(len(columns) == 9, 'binary map dimension') + table = [] + for vector in range(512): + image = 0 + for j, column in enumerate(columns): + if vector & (1 << j): + image ^= column + table.append(image) + require(len(set(table)) == 512, 'singular binary map') + return table + + +def frame_audit(word): + """Separate point-set trace; receipt includes full states at fixed cuts.""" + live = tuple(r for r in range(N) if r not in word['removed']) + require(len(live) == 632 and len(word['helper_final']) == 91, 'fixed all-input scope') + maps = [binary_map(w[2]) for w in word['warps']] + for w, table in zip(word['warps'], maps): + require(0 <= w[0] <= len(word['B']), 'warp position') + old, new = span(tuple(w[3])), span(tuple(w[4])) + require(rank(old) == len(w[3]) == len(w[4]) == rank(new), 'warp frame bases') + require(frozenset(table[x] for x in old) == new, 'binary warp frame action') + start, finish = {}, {} + for r in live: + if r < V: + start[r], finish[r] = span((word['ports'][r],)), FULL + elif target(r): + port = word['ports'][r - V] + start[r], finish[r] = ZERO, frozenset(x for x in range(512) if bin(x & port).count('1') % 2 == 0) + else: + start[r], finish[r] = ZERO, FULL + for r, basis in word['start_extra'].items(): + start[int(r)] = span(tuple(basis)) + for r, basis in word['helper_final'].items(): + finish[int(r)] = span(tuple(basis)) + current, paid, boundaries = start.copy(), Counter(), [] + def snapshot(label): + boundaries.append((label, tuple(tuple(sorted(current[r])) for r in live))) + def climb(register, frame): + require(register in current and current[register] <= frame, 'frame containment') + delta = rank(frame) - rank(current[register]) + if delta: + paid[delta] += 1 + current[register] = frame + def ordinary(gate): + for r in support(gate): + if not target(gate[1]) and gate[0] == 'add': + require(not target(gate[2]), 'non-target reads target') + climb(r, span(tuple(gate[-1]))) + snapshot('entrance') + for i, gate in enumerate(word['A']): + if gate[0] == 'warp': + require(i < word['prelude_events'], 'A native warp outside prelude') + _, r, op, before, after = gate + table = maps[abs(op) - 1] + if op < 0: + inverse = [0] * 512 + for x, y in enumerate(table): + inverse[y] = x + table = inverse + require(current[r] == span(tuple(before)), 'prelude entry') + require(frozenset(table[x] for x in current[r]) == span(tuple(after)), 'prelude binary image') + current[r] = span(tuple(after)) + else: + ordinary(gate) + snapshot('A_exit') + levels = {V + int(r): span(tuple(frame)) for r, frame in word['target_levels'].items()} + require(all(current[r] == levels.get(r, ZERO) for r in range(V, 2 * V)), 'target cut frame') + for r, frame in zip(word['centers'], word['center_frames']): + view = span(tuple(frame)) + require(current[r] == view, 'center entry') + served = {levels.get(g[1], ZERO) for g in word['cut'] if g[2] == r} + for child in sorted(served, key=lambda points: -rank(points)): + require(child <= view, 'center descent containment') + delta = rank(view) - rank(child) + if delta: + paid[delta] += 1 + view = child + at = {} + for k, warp in enumerate(word['warps']): + at.setdefault(warp[0], []).append(k) + for i in range(len(word['B']) + 1): + for k in at.get(i, ()): + _, r, _, before, after = word['warps'][k] + snapshot(('before_native', k)) + require(current[r] == span(tuple(before)), 'native entry') + current[r] = span(tuple(after)) + snapshot(('after_native', k)) + if i < len(word['B']): + ordinary(word['B'][i]) + snapshot('B_exit') + for gate in word['restore']: + ordinary(gate) + snapshot('restore_exit') + for r in live: + climb(r, finish[r]) + snapshot('terminal') + widths = Counter(rank(finish[r]) - rank(start[r]) for r in live if r >= 2 * V) + return ({str(k): v for k, v in sorted(paid.items())}, + {str(k): v for k, v in sorted(widths.items())}, boundaries) + + +def word_receipt(word): + profile, widths, boundaries = frame_audit(word) + require(word['cleanup'] == inverse_cleanup(word), 'literal projected inverse cleanup') + require(profile == PROFILE and widths == WIDTHS, 'complete fixed recursive bill') + counts = {s: {op: sum(g[0] == op for g in word[s]) for op in ('add', 'scale', 'warp')} + for s in ('A', 'B', 'restore', 'cleanup')} + return {'profile': profile, 'helper_widths': widths, 'lengths': {s: len(word[s]) for s in counts}, + 'primitive_counts': counts, 'canonical_word_sha256': sha(word), + 'cleanup_sha256': sha(word['cleanup']), 'native_operations': len(word['warps'])}, boundaries + + +def rejected(function): + try: + function() + except Rejected: + return + raise Rejected('negative control escaped') + + +def controls(word, records, contracted): + wrong = deepcopy(word) + wrong['B'][4][3] *= -1 + rejected(lambda: certified_sites(wrong)) + dependent = deepcopy(word) + dependent['B'][5][2] = 518 + rejected(lambda: certified_sites(dependent)) + rejected(lambda: certified_sites(word, PLAN + PLAN[:1])) + crossed = deepcopy(word) + crossed['warps'][0][0] = 8 + rejected(lambda: certified_sites(crossed)) + framed = deepcopy(word) + framed['B'][4][-1] = [31] + rejected(lambda: certified_sites(framed)) + stale = deepcopy(contracted) + stale['cleanup'] = deepcopy(word['cleanup']) + rejected(lambda: require(stale['cleanup'] == inverse_cleanup(stale), 'stale inverse cleanup')) + omitted = deepcopy(records) + omitted[1]['replacement'] = omitted[1]['replacement'][:1] + rejected(lambda: require(coefficients(records[1]['gates'], records[1]['support']) == + coefficients(omitted[1]['replacement'], records[1]['support']), 'missing retained gate')) + return 7 + + +def audit(root): + expected = json.loads((root / 'data.json').read_bytes(), object_pairs_hook=no_duplicates) + require(isinstance(expected, dict) and set(expected) == {'schema_version', 'providers'}, + 'certificate root schema') + require(type(expected['schema_version']) is int and expected['schema_version'] == 1, + 'typed certificate schema version') + require(isinstance(expected['providers'], dict) and set(expected['providers']) == {'base', 'extra'}, + 'certificate providers') + result = {} + for provider in ('base', 'extra'): + source = root / 'inputs' / ('BORROW-WORD-' + provider + '.json.gz') + require(not source.is_symlink(), 'input symlink') + raw = source.read_bytes() + require(hashlib.sha256(raw).hexdigest() == PINS[provider], 'source bytes') + word = json.loads(gzip.decompress(raw), object_pairs_hook=no_duplicates) + records = certified_sites(word) + known, changed = reconstruct(word, records[:1]), reconstruct(word, records) + require(sha(known) == KNOWN[provider], 'published PR3998 word') + require(expected['providers'][provider]['sites'] == records, 'literal fixed-site receipt') + receipts, traces = {}, [] + for name, candidate in (('source', word), ('credited_3998', known), ('separated', changed)): + receipt, trace = word_receipt(candidate) + reference = {k: v for k, v in expected['providers'][provider]['words'][name].items() + if k != 'semantics'} + require(receipt == reference, 'independent complete word/cleanup/frame receipt: ' + name) + receipts[name], traces = receipt, traces + [trace] + require(traces[0] == traces[1] == traces[2], 'all fixed whole-register boundary frames') + before, after = receipts['credited_3998']['primitive_counts'], receipts['separated']['primitive_counts'] + delta = sum(before[s]['add'] - after[s]['add'] for s in ('A', 'B', 'restore')) + cleanup_delta = before['cleanup']['add'] - after['cleanup']['add'] + require((delta, cleanup_delta) == (7, 5), 'additional exact scalar record saving') + negative_count = controls(word, records, changed) + result[provider] = {'new_sites': 7, 'known_sites': 1, 'inputs': 723, + 'local_exact_identities': 8, 'boundary_states': len(traces[0]), + 'negative_controls': negative_count, + 'forward_add_saving_vs_3998': delta, + 'cleanup_add_saving_vs_3998': cleanup_delta, + 'profile': PROFILE, 'helper_widths': WIDTHS} + return result + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--root', type=Path, default=HERE, help='explicit package root for private checking') + args = parser.parse_args() + result = audit(args.root) + print('PASS_INDEPENDENT_SEPARATED_A2 ' + json.dumps(result, sort_keys=True, separators=(',', ':'))) + + +if __name__ == '__main__': + try: + main() + except Exception as error: + import sys + print('FAIL_INDEPENDENT_SEPARATED_A2 ' + str(error), file=sys.stderr) + raise SystemExit(1) diff --git a/research/staged544-separated-a2/inputs/BORROW-WORD-base.json.gz b/research/staged544-separated-a2/inputs/BORROW-WORD-base.json.gz new file mode 100644 index 0000000000..674ea18ade Binary files /dev/null and b/research/staged544-separated-a2/inputs/BORROW-WORD-base.json.gz differ diff --git a/research/staged544-separated-a2/inputs/BORROW-WORD-extra.json.gz b/research/staged544-separated-a2/inputs/BORROW-WORD-extra.json.gz new file mode 100644 index 0000000000..b17e2be67e Binary files /dev/null and b/research/staged544-separated-a2/inputs/BORROW-WORD-extra.json.gz differ diff --git a/research/staged544-separated-a2/source/PR3945-NATIVE-LINEAGE-NOTICE b/research/staged544-separated-a2/source/PR3945-NATIVE-LINEAGE-NOTICE new file mode 100644 index 0000000000..380e979f0e --- /dev/null +++ b/research/staged544-separated-a2/source/PR3945-NATIVE-LINEAGE-NOTICE @@ -0,0 +1,14 @@ +Anticipatory dirty borrowing: PR2226 (Cinna Davis / 1337isnot1337, with substantial OpenAI Codex assistance) is credited first. Its alias rule, changed-reference K_G handoffs, initial compensation and exact free-operator replay (vendored under new/code/borrow/vendor, see new/code/borrow/NOTICE-PR2226.md) are applied here to the T74 pivot-566+554 words; the native lowering, window-exact owner fill and independent audit of the borrow words are new in this package. Bootstrap carried-cutoff repair: PR1956 (Josie Elliston); Lemma G label/adapter checks and X/Y/Z mutants: PR1964 (thakrarsagar), extended here with borrow warp/zero-buffer controls. + +New research prepared by Rohan Arun with substantial OpenAI Codex assistance. Apache-2.0. Parent words and build recipe method derive from Jeremy Kothe PR1274 and Rohan Arun PR1218, with lineage credited in README.md. All inherited mathematical qualifications are retained. +Additional pivot555 and567 composition by Rohan Arun with substantial OpenAI Codex assistance. + +T74 exact-fill owner construction by Rohan Arun with substantial OpenAI Codex assistance. + +PR1377 grid refinement credited to Jeremy Kothe. Outer witness refinement by Rohan Arun with OpenAI Codex assistance; construction unchanged. + +Pivot-566 kernel, words, edits, rebuild.py and rebind.py: PR1625 (mdumitrean). Endpoint/outer-witness stacking, fine_cache.py and oracle stage by jeremykothe2 with oh-my-pi assistance. + +The preceding paragraphs are inherited source notices, not attribution of this derivative. +This joint twelve-source construction, generator, independent replay, hosting composition and package: Tekalign (@tekuuu), with substantial OpenAI Codex assistance. No independent human review claimed. +Credits: Cinna Davis/PR2226 anticipatory dirty borrowing; Tekalign/PR2436 four lifted targets; Jeremy Kothe/PR2462,2588,2673 source pipeline, source-label swap and order/fill; zxv/PR2530 eight aliases; Mason Hale/PR2696 concentrated source-partner assignment and independent local interpreter; Philippe Van Velzen/PR2559,2679 evacuation, six pre-life hosts and refit/alias; themilkman216/PR2621 priority order; Marius-Paul Dumitrean/PR2733 independent concentrated/pre-life composition; Vlado Vojdanovski/PR2322 generator utilities. PR2720's fixed-old-path cut obstruction motivates the changed premise. The retained owner/native/bit/modern outer lineage and their notices remain in the pinned source. New work Apache-2.0. diff --git a/research/staged544-separated-a2/source/PR3998-PROOF.md b/research/staged544-separated-a2/source/PR3998-PROOF.md new file mode 100644 index 0000000000..afa6241fda --- /dev/null +++ b/research/staged544-separated-a2/source/PR3998-PROOF.md @@ -0,0 +1,206 @@ +# Consecutive A2 graph rewrites with fixed staged544 boundaries + +Chris R / Clear1nsight, with substantial OpenAI Codex assistance. Apache-2.0. + +## Scope and statement + +The inputs are the exact `43base` and `43extra` PR3734 BORROW-WORDs at +`fa041037a3374eaa08feeca0b26a5d6893194147`. The domain consists of consecutive +nonzero ADD pairs in A **after** `prelude_events`, B strictly inside the intervals +cut by native warp positions, and restore. A prelude, native warp, or intervening +scalar instruction is not crossed. The two ADDs involve three distinct registers +and form a directed path. Every other event, scalar coefficient, entrance/exit +frame, caller state, role and native map is fixed. This is a change of event graph, +not a retiming of two retained ADDs. + +For every such pair, replace it by the reversed pair plus the exact central ADD +below, at each of its three possible positions. Jointly choose **all** common +binary subspaces for the three ADDs, subject to monotone register frames and fixed +neighbouring frames. The output records every compatible flag and separately +reports rejection by exact whole-word boundary checks. Every compatible flag +already has a non-improving recursive invoice for every `0 1+3` implementation target and overhead discipline; +this package does not claim to realize that target or to originate its budget +certificate. Full upstream notices are retained in vendor/SOURCE-CREDITS.md. diff --git a/research/staged544-separated-a2/source/PR3998-README.md b/research/staged544-separated-a2/source/PR3998-README.md new file mode 100644 index 0000000000..dcd14ef45b --- /dev/null +++ b/research/staged544-separated-a2/source/PR3998-README.md @@ -0,0 +1,119 @@ +# A literal A2 graph contraction and its exact staged544 frame budget + +The A2 root-system identity yields a concrete simplification on both frozen +PR3734 staged544 providers: replace the three ADDs at A1858 by two ADDs, +removing **one forward and one inverse-cleanup ADD**. The full chronological +recursive profile is unchanged. Every dirty-input and caller boundary is +preserved. The same literal contraction is independently checked on both +current PR3945 terminal-gap-filled words at 91f81d13, with their own complete +profiles and full dirty-word replay. This supplies a reproducible scalar +simplification, **no new κ**. + +The same package completes the complementary consecutive two-to-three A2 +rewrite search. Each provider has 168 directed two-ADD motifs. All three central +commutator positions and every compatible binary-frame flag are included. +All 460 legal flags have non-improving recursive moments for every `0 1+3` implementation target and paid-overhead discipline; the present +scalar contraction does not realize that rank exchange. See `SOURCES.json` and +`vendor/SOURCE-CREDITS.md` for exact pins and full lineage. + +Chris R / Clear1nsight, with substantial OpenAI Codex assistance. Apache-2.0. +Author-checked finite construction/certificate; no independent human review, +formal-kernel proof, supplier admission or selected-frontier change claimed. diff --git a/research/staged544-separated-a2/source/SOURCE-CREDITS.md b/research/staged544-separated-a2/source/SOURCE-CREDITS.md new file mode 100644 index 0000000000..c054fad87e --- /dev/null +++ b/research/staged544-separated-a2/source/SOURCE-CREDITS.md @@ -0,0 +1,14 @@ +# Source credit and independence + +New work: dataisfire with substantial OpenAI Codex assistance, Apache-2.0. No independent human review, fresh third-party AI review or proof-kernel verification is claimed. + +The construction extends [PR3682](https://github.com/CrocSwap/integer-mult-bounds/pull/3682), head431e6c6023ef352c41696469de7fb614cd4ded8c. Its retimed word, actual T360 source clock and immutable native/parent framework are retained. The complete new source/receipt snapshot is bound by REPLAY-INPUTS.json. The new ordinary source stage is an explicit pinned record applied after the unchanged predecessor reconstruction. + +- [PR3605](https://github.com/CrocSwap/integer-mult-bounds/pull/3605), Ross Richardson, supplies the staged-entrance mechanism, literal cleanup and exact Gaussian residual-check pattern. staged_pair.py is retained; the new544 shear and its proof are separate. +- [PR3638](https://github.com/CrocSwap/integer-mult-bounds/pull/3638), head d62e1acd7518a231440383f0d0dddf54d6edf8c1, supplies the T360 source-window clock, chronological aggregate model and integral-network/literal construction, with its retained PR3605 and earlier credits. The new inventory, integer incumbent and literal fill are recomputed. No predecessor owner receipt is used as proof of the new fill. +- [PR3687](https://github.com/CrocSwap/integer-mult-bounds/pull/3687) and [PR3693](https://github.com/CrocSwap/integer-mult-bounds/pull/3693), Sagar Thakrar and roger-sato with their credited AI assistance, supply audit_core.py and the whole-word semantics adapter audit_verify.py. These bytes are retained and reused. They are independent of the current constructor in the stated interpreter scope, not a newly written independent audit or new reviewer approval. +- The coupled-word source lineage includes PR3133, PR2979, Marius-Paul Dumitrean, dcharb78, Jeremy Kothe and the retained native/owner/block-norm/outer authors. All notices and scientific engines inside the source snapshot remain intact. + +owner_audit.py is a standalone standard-library adaptation of the source-window/family/prefix/invoice predicates in PR3638's independent_literal.py. It imports no producer, optimizer or retained owner checker. Its source template, plan and actual native canonical words are authenticated inputs. Three controls mutate actual literal roles and must fail for the intended reason. It shares the credited contract interpretation; it is not evidence of independent human agreement. + +The rational finite-price enclosure is retained from the PR3682 sources. New script adapters bind it to the actual finite histogram. Native forward/backward scalar replay, wrapper/phase lowering and all-column warp recipes were freshly run for both new words; unchanged native and parent ancestry is explicitly reused. The separate new544 span(414,51) residual check includes global Gaussian phase. diff --git a/research/staged544-separated-a2/source/audit_core.py b/research/staged544-separated-a2/source/audit_core.py new file mode 100644 index 0000000000..8b5e1d5f2a --- /dev/null +++ b/research/staged544-separated-a2/source/audit_core.py @@ -0,0 +1,480 @@ +"""Independent exact semantics and binary-frame bill for the BORROW-WORD format. + +Standard library only. Nothing is imported from the audited authors' code +(PR3133/PR3605 producers, cleanup generator, evaluator or frame solver); the word +format and its semantic contract were read from those pinned sources and are +credited there. The frame-bill and free-word structure (point-set spans, warp +frame and lifted-frame checks, target levels keyed by register, dual symbol +naming) re-implements, without importing, Arham Tahir's +research/coupled-carrier-independent-audit/verify.py (Apache-2.0) and shares its +reading of the contract, so this module is not independent of that audit. + +Sagar Thakrar (thakrarsagar), with substantial AI assistance from Claude +(Anthropic, Claude Opus 5.5). Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as Q + +V, N, H = 112, 704, 9 # sources 0..111, targets 112..223, helpers 224..703 +DUAL = 10 ** 6 # offset naming the independent dual symbols D_k = K_k^(-T) + + +class AuditFailure(Exception): + """Explicit failure; never disabled by python -O.""" + + +def need(ok, *why): + if not ok: + raise AuditFailure(' '.join(map(str, why))) + + +def is_target(r): + return V <= r < 2 * V + + +def touched(g): + return g[1:3] if g[0] == 'add' else g[1:2] + + +# ---------------------------------------------------------------------------- +# Binary frames: a subspace of F_2^9 is stored as a 512-bit point-set mask +# (bit x set iff x lies in the subspace). Containment is mask inclusion. +# ---------------------------------------------------------------------------- +_SPAN = {} + + +def span(vectors): + key = tuple(vectors) + mask = _SPAN.get(key) + if mask is None: + points = {0} + for u in key: + need(type(u) is int and 0 <= u < 512, 'frame vector out of range', u) + if u not in points: + points |= {p ^ u for p in points} + mask = sum(1 << p for p in points) + _SPAN[key] = mask + return mask + + +def points(mask): + return [x for x in range(512) if mask >> x & 1] + + +def dim(mask): + size = bin(mask).count('1') + need(size and size & (size - 1) == 0, 'not a subspace point set') + return size.bit_length() - 1 + + +FULL = (1 << 512) - 1 +ZERO = 1 + + +def hyperplane(port): + return sum(1 << x for x in range(512) if bin(x & port).count('1') % 2 == 0) + + +def warp_images(columns): + """Images of all 512 vectors under the F_2-linear map with columns G e_i.""" + need(len(columns) == H and all(type(c) is int and 0 <= c < 512 for c in columns), 'warp columns') + images = [0] * 512 + for x in range(1, 512): + low = x & -x + images[x] = images[x ^ low] ^ columns[low.bit_length() - 1] + need(len(set(images)) == 512, 'singular warp') + return images + + +def image_mask(images, mask): + return sum(1 << images[x] for x in points(mask)) + + +def lagrangian_action_ok(images, U, E): + """K_G(x,z)=(Gx, Gx+G^{-T}(x+z)) is symplectic and maps L_U to L_E, L_0 and L_FULL to themselves. + + L_U={(x,x+p): x in U, p in U^perp}. This is the binary frame action only; it + is not a Clifford phase or Gaussian-product certificate. For invertible G with + G(U)=E it is implied by the frame-map check ( = ), so it is a + consistency check of the implementation, not extra evidence. + """ + inverse = [0] * 512 + for x, y in enumerate(images): + inverse[y] = x + # G^{-T} z: bit j of the result is . + git = lambda z: sum((bin(inverse[1 << j] & z).count('1') & 1) << j for j in range(H)) + lift = lambda x, z: (images[x], images[x] ^ git(x ^ z)) + pair = lambda a, b: (bin(a[0] & b[1]).count('1') + bin(a[1] & b[0]).count('1')) & 1 + basis = [(1 << i, 0) for i in range(H)] + [(0, 1 << i) for i in range(H)] + lifted = [lift(*b) for b in basis] + if any(pair(lifted[i], lifted[j]) != pair(basis[i], basis[j]) for i in range(18) for j in range(i + 1, 18)): + return False + + def frame(mask): + us = points(mask) + perp = [p for p in range(512) if all(bin(p & u).count('1') % 2 == 0 for u in us)] + return {(u, u ^ p) for u in us for p in perp} + return all({lift(*pt) for pt in frame(a)} == frame(b) for a, b in ((ZERO, ZERO), (FULL, FULL), (U, E))) + + +# ---------------------------------------------------------------------------- +# Chronological binary-frame bill (BORROW-WORD contract) +# ---------------------------------------------------------------------------- +def frame_bill(w, lagrangian=False): + rep = w['report'] + need((rep['v'], 2 * rep['v'] + rep['R'], rep['h']) == (V, N, H), 'word geometry') + removed = set(w['removed']) + need(len(removed) == len(w['removed']) and all(2 * V <= r < N for r in removed), 'removed helpers') + live = [r for r in range(N) if r not in removed] + liveset = set(live) + B, warps = w['B'], w['warps'] + for k, (pos, lender, cols, U, E) in enumerate(warps, 1): + need(0 <= pos <= len(B), 'warp position', k) + need(lender in liveset and not is_target(lender), 'warp lender', k) + images = warp_images(cols) + su, se = span(U), span(E) + need(dim(su) == len(U) == len(E) == dim(se), 'warp frame bases', k) + need(image_mask(images, su) == se, 'warp does not map its frame', k) + if lagrangian: + need(lagrangian_action_ok(images, su, se), 'lifted frame action', k) + for name in ('A', 'B', 'restore'): + for g in w[name]: + if g[0] != 'warp': + need(all(r in liveset for r in touched(g)), 'removed/out-of-range register', name, g) + if g[0] == 'add' and not is_target(g[1]): + need(not is_target(g[2]), 'non-target reads a target', name, g) + need(all(g[-1] is None and is_target(g[1]) and g[0] == 'add' for g in w['cut']), 'cut gates') + need(all(g[-1] == [] and is_target(g[1]) for g in w['precondition'] + w['compensation']), 'zero-frame wrapper writes') + need(all(not is_target(g[1]) for g in w['restore']), 'restore writes a target') + + ports = w['ports'] + start, end = {}, {} + for r in live: + if r < V: + start[r], end[r] = span((ports[r],)), FULL + elif r < 2 * V: + start[r], end[r] = ZERO, hyperplane(ports[r - V]) + else: + start[r], end[r] = ZERO, FULL + for q, U in w['start_extra'].items(): + need(int(q) in liveset and int(q) >= 2 * V, 'entrance names a live helper', q) + start[int(q)] = span(U) + for q, U in w['helper_final'].items(): + need(int(q) in liveset and int(q) >= 2 * V, 'terminal names a live helper', q) + end[int(q)] = span(U) + + current, bill, chain = dict(start), Counter(), {} + + def climb(r, mask, where): + need(current[r] & ~mask == 0, 'frame containment fails', where, r) + d = dim(mask) - dim(current[r]) + if d: + bill[d] += 1 + chain.setdefault(r, []).append((where, d, mask)) + current[r] = mask + + npre = w['prelude_events'] + for i, g in enumerate(w['A']): + if g[0] == 'warp': + need(i < npre and len(g) == 5, 'warp outside the prelude', i) + _, r, op, fr, to = g + need(op != 0 and abs(op) <= len(warps) and warps[abs(op) - 1][1] == r, 'prelude warp lender', i) + images = warp_images(warps[abs(op) - 1][2]) + if op < 0: + inverse = [0] * 512 + for x, y in enumerate(images): + inverse[y] = x + images = inverse + need(image_mask(images, span(fr)) == span(to), 'prelude warp frame action', i) + need(current[r] == span(fr), 'prelude warp entry frame', i, r) + current[r] = span(to) + chain.setdefault(r, []).append((('A', i), 'warp', span(to))) + else: + if i < npre: + need(is_target(g[1]), 'prelude scalar writes a non-target', i) + for r in touched(g): + climb(r, span(g[-1]), ('A', i)) + levels = {V + int(t): span(U) for t, U in w['target_levels'].items()} + need(all(current[t] == levels.get(t, ZERO) for t in range(V, 2 * V)), 'target cut levels') + for q, U in zip(w['centers'], w['center_frames']): + U = span(U) + need(current[q] == U, 'centre entry frame', q) + served = {levels.get(g[1], ZERO) for g in w['cut'] if g[2] == q} + for T in sorted(served, key=lambda m: -dim(m)): + need(T & ~U == 0, 'centre descent not nested', q) + d = dim(U) - dim(T) + if d: + bill[d] += 1 + chain.setdefault(q, []).append((('centre',), d, T)) + U = T + at = {} + for k, rec in enumerate(warps, 1): + at.setdefault(rec[0], []).append(k) + for p in range(len(B) + 1): + for k in at.get(p, ()): + _, lender, _, U, E = warps[k - 1] + need(current[lender] == span(U), 'native warp entry frame', k, lender) + current[lender] = span(E) + chain.setdefault(lender, []).append((('warp', k), 'warp', span(E))) + if p < len(B): + for r in touched(B[p]): + climb(r, span(B[p][-1]), ('B', p)) + for i, g in enumerate(w['restore']): + for r in touched(g): + climb(r, span(g[-1]), ('restore', i)) + for r in live: + climb(r, end[r], ('end',)) + restored = set(map(int, w['helper_final'])) + need(all(end[r] == FULL for r in live if r not in restored and not is_target(r)), 'a FULL-cleanup register ends low') + widths = Counter(dim(end[r]) - dim(start[r]) for r in live if r >= 2 * V) + return dict(sorted(bill.items())), dict(sorted(widths.items())), chain, start, end + + +def hygiene(w): + """Inherited structural contract: dyadic scalars, power-of-two scales, wrapper and correction access.""" + entering = set(map(int, w['start_extra'])) + restored = set(map(int, w['helper_final'])) + live = set(range(N)) - set(w['removed']) + for name in ('precondition', 'compensation', 'A', 'cut', 'B', 'restore', 'cleanup'): + for g in w[name]: + if g[0] == 'warp': + continue + q = Q(g[3], g[4]) if g[0] == 'add' else Q(g[2], g[3]) + need(q != 0 and q.denominator & (q.denominator - 1) == 0, 'non-dyadic scalar', name, g) + if g[0] == 'scale': + need(abs(q.numerator) & (abs(q.numerator) - 1) == 0, 'non power-of-two scale', name, g) + for g in w['precondition'] + w['compensation']: + need(not any(r in entering | restored for r in touched(g)), 'wrapper touches an entering or restored helper', g) + for c in w['initial_corrections']: + word = c['operator_word'] + need(is_target(c['target']) and c['source'] in live and c['source'] >= 2 * V + and c['source'] not in entering, 'correction access', c) + need(word and all(w['warps'][abs(o) - 1][1] == c['source'] for o in word), 'correction operator lender', c) + q = Q(c['coefficient']) + need(q != 0 and q.denominator & (q.denominator - 1) == 0, 'correction coefficient', c) + return True + + +# ---------------------------------------------------------------------------- +# Literal inverse cleanup, derived from the contract +# ---------------------------------------------------------------------------- +def ordinary_forward(w): + """Chronological non-wrapper actions whose inverse forms cleanup.""" + out = [g for g in w['A'][w['prelude_events']:]] + at = {} + for k, rec in enumerate(w['warps'], 1): + at.setdefault(rec[0], []).append(['warp', rec[1], k]) + for p in range(len(w['B']) + 1): + out += at.get(p, []) + if p < len(w['B']): + out.append(w['B'][p]) + return out + list(w['restore']) + + +def derive_cleanup(w): + restored = set(map(int, w['helper_final'])) + buf = lambda r: r + N if r in restored else r + full = [256, 128, 64, 32, 16, 8, 4, 2, 1] + out = [] + for g in reversed(ordinary_forward(w)): + if g[0] == 'warp': + out.append(['warp', buf(g[1]), -g[2], full]) + elif is_target(g[1]): + continue + elif g[0] == 'add': + out.append(['add', buf(g[1]), buf(g[2]), -g[3], g[4], full]) + else: + need(g[0] == 'scale', 'unknown primitive', g) + out.append(['scale', buf(g[1]), g[3], g[2], full]) + return out + + +def same_cleanup(a, b): + norm = lambda c: [(g[:-1], span(g[-1])) for g in c] + return len(a) == len(b) and norm(a) == norm(b) + + +# ---------------------------------------------------------------------------- +# Exact free-operator semantics. A value is a dict {(input, word): Fraction}; +# word is a reduced tuple of signed operator ids (leftmost = applied last). +# ---------------------------------------------------------------------------- +def program(w, cleanup=None): + """Literal executed sequence: corrections, wrapper, A, cut, B+warps, restore | cleanup.""" + items = [('corr', c['target'], c['source'], tuple(c['operator_word']), Q(c['coefficient'])) + for c in w['initial_corrections']] + items += w['precondition'] + w['compensation'] + w['A'] + w['cut'] + at = {} + for k, rec in enumerate(w['warps'], 1): + at.setdefault(rec[0], []).append(['warp', rec[1], k]) + for p in range(len(w['B']) + 1): + items += at.get(p, []) + if p < len(w['B']): + items.append(w['B'][p]) + items += w['restore'] + return items, list(w['cleanup'] if cleanup is None else cleanup) + + +def dual_op(op): + return (1 if op > 0 else -1) * (abs(op) + DUAL) + + +def _left(op, word): + return word[1:] if word and word[0] == -op else (op,) + word + + +def _right(word, op): + return word[:-1] if word and word[-1] == -op else word + (op,) + + +def _axpy(dst, src, q): + for key, x in src.items(): + y = dst.get(key, 0) + q * x + if y: + dst[key] = y + else: + dst.pop(key, None) + + +def forward_rows(w, cleanup=None, dual=False, symbolic_buffers=True, snapshot=None): + """Schrodinger pass: every register's value as a combination of initial inputs. + + Live inputs are independent symbols. Private buffers are independent symbols + when symbolic_buffers is set (dirty), otherwise zero. The optional snapshot + callback sees the rows at the cleanup boundary. + """ + removed = set(w['removed']) + live = [r for r in range(N) if r not in removed] + restored = sorted(map(int, w['helper_final'])) + rows = {r: {(r, ()): Q(1)} for r in live} + for c in restored: + rows[c + N] = {(c + N, ()): Q(1)} if symbolic_buffers else {} + prefix, tail = program(w, cleanup) + + def apply(g): + kind = g[0] + if kind == 'add': + t, s, q = g[1], g[2], Q(g[3], g[4]) + need(t != s and q, 'add gate', g) + if dual: + t, s, q = s, t, -q + _axpy(rows[t], rows[s], q) + elif kind == 'scale': + q = Q(g[2], g[3]) + need(q != 0, 'zero scale', g) + if dual: + q = 1 / q + rows[g[1]] = {k: q * x for k, x in rows[g[1]].items()} + elif kind == 'warp': + op = dual_op(g[2]) if dual else g[2] + rows[g[1]] = {(var, _left(op, word)): x for (var, word), x in rows[g[1]].items()} + elif kind == 'corr': + _, t, s, word, c = g + if dual: + src, ops, dst, c = rows[t], [-dual_op(o) for o in word], s, -c + else: + src, ops, dst = rows[s], list(reversed(word)), t + moved = {} + for (var, wd), x in src.items(): + for o in ops: + wd = _left(o, wd) + moved[var, wd] = x + _axpy(rows[dst], moved, c) + else: + raise AuditFailure('unknown primitive ' + repr(g)) + + for g in prefix: + apply(g) + if snapshot is not None: + snapshot(rows) + for g in tail: + apply(g) + return rows + + +def reverse_columns(w, cleanup=None, upto_cleanup=False): + """Heisenberg pull-back: process the forward program backwards. + + cols[s] = {(output, word): coefficient}: the final output register 'output' + contains coefficient*word*x_s. Words grow on the right. Every live input and + every private buffer is an independent symbol. + """ + removed = set(w['removed']) + live = [r for r in range(N) if r not in removed] + restored = sorted(map(int, w['helper_final'])) + regs = live + [c + N for c in restored] + cols = {r: {(r, ()): Q(1)} for r in regs} + prefix, tail = program(w, cleanup) + seq = prefix if upto_cleanup else prefix + tail + for g in reversed(seq): + kind = g[0] + if kind == 'add': + t, s, q = g[1], g[2], Q(g[3], g[4]) + need(t != s and q, 'add gate', g) + _axpy(cols[s], cols[t], q) + elif kind == 'scale': + q = Q(g[2], g[3]) + need(q != 0, 'zero scale', g) + cols[g[1]] = {k: q * x for k, x in cols[g[1]].items()} + elif kind == 'warp': + op = g[2] + cols[g[1]] = {(out, _right(word, op)): x for (out, word), x in cols[g[1]].items()} + elif kind == 'corr': + _, t, s, word, c = g + moved = {} + for (out, wd), x in cols[t].items(): + for o in word: + wd = _right(wd, o) + moved[out, wd] = x + _axpy(cols[s], moved, c) + else: + raise AuditFailure('unknown primitive ' + repr(g)) + return cols + + +def transpose(cols): + rows = {} + for s, col in cols.items(): + for (r, word), x in col.items(): + rows.setdefault(r, {})[s, word] = x + return rows + + +def endpoint_defects(w, rows, dual=False): + """Compare final rows with the contract on the zero-buffer (live-input) domain. + + Returns (bad live registers, dirty buffers, buffer->live leaks, buffer self-map identity). + """ + removed = set(w['removed']) + live = [r for r in range(N) if r not in removed] + restored = sorted(map(int, w['helper_final'])) + bad = [] + for r in live: + expect = {(r, ()): Q(1)} + if dual and r < V: + expect[r + V, ()] = Q(-1) + if not dual and is_target(r): + expect[r - V, ()] = Q(1) + got = {k: x for k, x in rows.get(r, {}).items() if k[0] < N} + if got != expect: + bad.append(r) + dirty = [c for c in restored if any(k[0] < N for k in rows.get(c + N, {}))] + leaks = sorted({r for r in live for k in rows.get(r, {}) if k[0] >= N}) + buffer_identity = all({k: x for k, x in rows.get(c + N, {}).items() if k[0] >= N} == {(c + N, ()): Q(1)} + for c in restored) + return bad, dirty, leaks, buffer_identity + + +def boundary_defects(w, rows): + """Contract at the cleanup boundary (forward): targets sheared, restored helpers clean and isolated.""" + restored = set(map(int, w['helper_final'])) + out = [] + for t in range(V, 2 * V): + if {k: x for k, x in rows[t].items() if k[0] < N} != {(t, ()): Q(1), (t - V, ()): Q(1)}: + out.append(('target', t)) + for c in restored: + if rows[c] != {(c, ()): Q(1)}: + out.append(('restored', c)) + for r, row in rows.items(): + if r < N and r not in restored and any(k[0] in restored for k in row): + out.append(('restored input read', r)) + return out diff --git a/research/staged544-separated-a2/test_verify.py b/research/staged544-separated-a2/test_verify.py new file mode 100644 index 0000000000..4a0686dc62 --- /dev/null +++ b/research/staged544-separated-a2/test_verify.py @@ -0,0 +1,228 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Bounded mutation controls for the fixed separated-A2 witnesses. + +Uses the submitted verifier as the subject under test; it is not an independent +matrix or full-word semantics proof. Every required check uses explicit errors, +so the same suite remains effective with Python's optimization enabled. +""" +import argparse +from copy import deepcopy +import importlib.util +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + + +class TestFailure(Exception): + pass + + +def need(ok, message): + if not ok: + raise TestFailure(message) + + +def import_subject(root): + sys.path.insert(0, str(root)) + spec = importlib.util.spec_from_file_location('separated_a2_subject', root / 'verify.py') + subject = importlib.util.module_from_spec(spec) + spec.loader.exec_module(subject) + return subject + + +def writable_copy(source, destination): + """Fresh files only; never relax permissions on a frozen source export.""" + shutil.copytree(source, destination, copy_function=shutil.copyfile) + for path in destination.rglob('*'): + path.chmod(0o755 if path.is_dir() else 0o644) + destination.chmod(0o755) + + +def run_cli(root, provider='base'): + command = [sys.executable, '-I', '-B'] + if not __debug__: + command.append('-O') + command.extend([str(root / 'verify.py'), '--provider', provider, '--quick']) + return subprocess.run(command, cwd=root, capture_output=True, text=True) + + +class Controls: + def __init__(self, errors): + self.errors = errors + self.rejected = [] + + def rejects(self, name, action): + try: + action() + except self.errors: + self.rejected.append(name) + return + except Exception as error: + raise TestFailure(name + ' crashed with ' + type(error).__name__ + ': ' + str(error)) from error + raise TestFailure(name + ' was accepted') + + def cli_rejects(self, name, fixture): + result = run_cli(fixture) + need(result.returncode != 0, name + ' CLI accepted the altered fixture') + need('FAIL' in result.stderr, name + ' CLI did not report an explicit validation failure: ' + result.stderr[-500:]) + self.rejected.append(name) + + +def tree_bytes(root): + return {str(path.relative_to(root)): hashlib.sha256(path.read_bytes()).hexdigest() + for path in root.rglob('*') if path.is_file()} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--package', type=Path, default=Path(__file__).resolve().parent) + args = parser.parse_args() + root = args.package.resolve() + before = tree_bytes(root) + subject = import_subject(root) + core = subject.authenticate() + controls = Controls((ValueError, core.AuditFailure)) + source = subject.load_word('base') + sites = list(subject.SITES) + separated = next(site for site in sites if not site['known'] and site['section'] == 'B') + known = next(site for site in sites if site['known']) + indices = separated['indices'] + gap = next(i for i in range(indices[0], indices[2]) if i not in indices) + support = subject.certify_site(source, separated)['support'] + + def site_control(name, mutate): + word, site = deepcopy(source), deepcopy(separated) + mutate(word, site) + controls.rejects(name, lambda: subject.certify_site(word, site)) + + def set_site(field, value): + return lambda _word, site: site.__setitem__(field, value) + + site_control('duplicate selected index', set_site('indices', [indices[0], indices[0], indices[2]])) + site_control('reversed selected indices', set_site('indices', list(reversed(indices)))) + site_control('boolean selected index', set_site('indices', [True, indices[1], indices[2]])) + site_control('selected index outside section', set_site('indices', [indices[0], indices[1], len(source['B'])])) + site_control('boolean removed position', set_site('removed_position', False)) + site_control('integer known-site flag', set_site('known', 0)) + site_control('unexpected site field', set_site('unproved', True)) + site_control('uncovered section', set_site('section', 'cut')) + + def alter_selected(word, site, position, action): + action(word[site['section']][site['indices'][position]]) + + site_control('wrong A2 sign', lambda w, s: alter_selected(w, s, 0, lambda g: g.__setitem__(3, -g[3]))) + site_control('wrong A2 product', lambda w, s: alter_selected(w, s, 2, lambda g: g.__setitem__(3, 2 * g[3]))) + site_control('boolean A2 coefficient', lambda w, s: alter_selected(w, s, 0, lambda g: g.__setitem__(3, True))) + site_control('zero A2 denominator', lambda w, s: alter_selected(w, s, 0, lambda g: g.__setitem__(4, 0))) + site_control('mismatched original frame', lambda w, s: alter_selected(w, s, 0, lambda g: g.__setitem__(-1, [512]))) + site_control('self ADD edge', lambda w, s: alter_selected(w, s, 0, lambda g: g.__setitem__(2, g[1]))) + site_control('unknown selected primitive', lambda w, s: alter_selected(w, s, 0, lambda g: g.__setitem__(0, 'copy'))) + site_control('unknown intervening primitive', lambda w, s: w['B'].__setitem__(gap, ['copy', 0, 1, 1, 1, []])) + site_control('intervening support dependency', lambda w, s: w['B'].__setitem__(gap, ['scale', support[0], 2, 1, []])) + site_control('native warp cut crossing', lambda w, s: w['warps'][0].__setitem__(0, indices[0] + 1)) + cut_word = deepcopy(source) + cut_word['prelude_events'] = known['indices'][0] + 1 + controls.rejects('prelude cut crossing', lambda: subject.certify_site(cut_word, deepcopy(known))) + controls.rejects('boolean include-known flag', lambda: subject.contract(source, 1)) + controls.rejects('unrecognized provider', lambda: subject.load_word('unproved')) + + positive = [] + changed_base = None + for provider in ('base', 'extra'): + original = subject.load_word(provider) + changed = subject.contract(original) + info = subject.inspect_word(core, changed) + need(info['lengths'] == {'A': 4078, 'B': 1867, 'restore': 207, 'cleanup': 5218}, + 'fixed contraction lengths changed for ' + provider) + need(changed['cleanup'] == core.derive_cleanup(changed), 'positive cleanup not literal inverse') + need(all(a[1:] == b[1:] for a, b in zip(original['warps'], changed['warps'])), + 'positive contraction changed native maps or frames') + positive.append(provider + ' fixed contractions, literal cleanup, complete bill') + if provider == 'base': + changed_base = changed + + def word_control(name, mutate): + word = deepcopy(changed_base) + mutate(word) + controls.rejects(name, lambda: subject.inspect_word(core, word)) + + word_control('omitted inverse cleanup ADD', lambda w: w['cleanup'].pop()) + word_control('duplicated inverse cleanup ADD', lambda w: w['cleanup'].append(deepcopy(w['cleanup'][-1]))) + word_control('wrong inverse cleanup sign', lambda w: w['cleanup'][0].__setitem__(3, -w['cleanup'][0][3])) + word_control('stale original inverse cleanup', lambda w: w.__setitem__('cleanup', deepcopy(source['cleanup']))) + word_control('forged declared paid profile', lambda w: w['report']['local_profile'].__setitem__('1', 2439)) + + certificate = subject.compute('base', False) + subject.audit('base', False, certificate=certificate) + positive.append('exact quick certificate accepted') + + def receipt_control(name, mutate): + receipt = deepcopy(certificate) + mutate(receipt) + controls.rejects(name, lambda: subject.audit('base', False, certificate=receipt)) + + receipt_control('forged forward saving', lambda r: r.__setitem__('additional_forward_add_saving', 8)) + receipt_control('forged cleanup saving', lambda r: r.__setitem__('additional_cleanup_add_saving', 6)) + receipt_control('integer false kappa flag', lambda r: r.__setitem__('new_kappa', 0)) + receipt_control('unsupported kappa claim', lambda r: r.__setitem__('new_kappa', True)) + receipt_control('unsupported native claim', lambda r: r.__setitem__('native_operators_changed', True)) + receipt_control('forged result hash', lambda r: r['words']['separated'].__setitem__('canonical_word_sha256', '0' * 64)) + receipt_control('forged helper inventory', lambda r: r['words']['separated']['helper_widths'].__setitem__(9, 214)) + receipt_control('extra unverified receipt field', lambda r: r.__setitem__('proved_by_assert', True)) + + # CLI controls run against fresh writable copies; retained source bytes and + # the package under test are never changed, even on a read-only export. + with tempfile.TemporaryDirectory(prefix='separated-a2-negative-') as directory: + fixture = Path(directory) / 'package' + writable_copy(root, fixture) + baseline = run_cli(fixture) + need(baseline.returncode == 0 and 'PASS_STAGED544_SEPARATED_A2' in baseline.stdout, + 'unaltered CLI fixture failed: ' + baseline.stderr[-500:]) + positive.append('unaltered copied CLI fixture accepted') + + for relative in ('source/audit_core.py', 'inputs/BORROW-WORD-base.json.gz'): + path = fixture / relative + raw = path.read_bytes() + path.write_bytes(raw + b'\n') + controls.cli_rejects('CLI altered frozen ' + relative, fixture) + path.write_bytes(raw) + + receipt_path = fixture / 'data.json' + receipt_bytes = receipt_path.read_bytes() + data = json.loads(receipt_bytes) + forged = deepcopy(data) + forged['providers']['base']['additional_cleanup_add_saving'] = 6 + receipt_path.write_text(json.dumps(forged) + '\n') + controls.cli_rejects('CLI forged cleanup saving', fixture) + forged = deepcopy(data) + forged['schema_version'] = True + receipt_path.write_text(json.dumps(forged) + '\n') + controls.cli_rejects('CLI boolean root schema', fixture) + receipt_path.write_text('{"schema_version":1,"schema_version":1,"providers":' + json.dumps(data['providers']) + '}\n') + controls.cli_rejects('CLI duplicate JSON key', fixture) + receipt_path.write_bytes(receipt_bytes) + source_path = fixture / 'source/audit_core.py' + source_bytes = source_path.read_bytes() + sibling = Path(directory) / 'same-audit-core.py' + sibling.write_bytes(source_bytes) + source_path.unlink() + source_path.symlink_to(sibling) + controls.cli_rejects('CLI symlink source substitution', fixture) + + need(tree_bytes(root) == before, 'the package under test changed') + print('PASS_SEPARATED_A2_NEGATIVE_CONTROLS ' + json.dumps( + {'positive_controls': len(positive), 'expected_rejections': len(controls.rejected), + 'positive_names': positive, 'rejection_names': controls.rejected, + 'package_bytes_unchanged': True, 'optimized': not __debug__}, sort_keys=True)) + + +if __name__ == '__main__': + try: + main() + except TestFailure as error: + raise SystemExit('FAIL: ' + str(error)) diff --git a/research/staged544-separated-a2/verify.py b/research/staged544-separated-a2/verify.py new file mode 100644 index 0000000000..877e57b883 --- /dev/null +++ b/research/staged544-separated-a2/verify.py @@ -0,0 +1,308 @@ +#!/usr/bin/env python3 +"""Seven fixed separated A2 contractions, with complete unchanged paid invoices. + +Apache-2.0. ToikY with substantial OpenAI Codex assistance. The exact whole-word +arithmetic and frame engine is credited retained audit_core.py; this is not a +new independent interpreter or native/supplier audit. The replay adapter follows +the ordinary/dual/reverse contract of roger-sato's retained audit_verify.py. +""" +from __future__ import annotations +import argparse +from copy import deepcopy +from fractions import Fraction as Q +import gzip +import hashlib +import json +from pathlib import Path +import types + +HERE = Path(__file__).resolve().parent +# Exact frozen exports: PR3734 fa041037..., PR3998 389268a6..., PR3945 91f81d13... +PINS = { + 'source/audit_core.py': (19364,'888679ca8502cdcb100420fe5382a052529a494bf76cb332928b86e62612b951','8b5e1d5f2a106402f036b63028ecef31a4e4c462'), + 'source/SOURCE-CREDITS.md': (2882,'d4a13d8b8ed9cdb594f00efb3d1a336e09d934423330f02a1514308a720c278b','c054fad87eeaa510865e682ee0c976c4cd728da2'), + 'source/PR3998-README.md': (6498,'d935e7d10e2935ca82a3ba952308d73b78e76a9039cb335682f1fc5ea3b580d7','dcd14ef45bcfb102d030e3f87a0bb2bf80d57ade'), + 'source/PR3998-PROOF.md': (11251,'0bbec6ba5b03e40e571f7f4a89e5776441a33b6ede41beeb80153ffad39d124f','afa6241fdaee6da1e567eb5ba74b780f9121ba8d'), + 'source/PR3945-NATIVE-LINEAGE-NOTICE': (2456,'ee0c73ca35877aad0e0b6adc560a3881cb82276dba4cf2d4fc58cd19e57cc420','380e979f0e84e00a22bd890615d87cc4684ad740'), + 'inputs/BORROW-WORD-base.json.gz': (72769,'5ca4be99851f8878cbfe0fd6c454df926b11218f17feefa1664721cf03156699','674ea18ade4af85ca865fb08dc973637a09e30e6'), + 'inputs/BORROW-WORD-extra.json.gz': (72766,'965268a9be73d3f62e7ef680d18f108cf064bfe1f44b82157baa61443232904e','b17e2be67e327f04802fd034c344fe4253c13a4a'), +} +SITES = ( + {'section':'A','indices':[1858,1859,1860],'removed_position':2,'known':True}, + {'section':'B','indices':[4,53,54],'removed_position':0,'known':False}, + {'section':'B','indices':[7,49,50],'removed_position':0,'known':False}, + {'section':'restore','indices':[20,21,36],'removed_position':2,'known':False}, + {'section':'restore','indices':[22,23,38],'removed_position':2,'known':False}, + {'section':'restore','indices':[26,27,51],'removed_position':2,'known':False}, + {'section':'restore','indices':[30,31,62],'removed_position':2,'known':False}, + {'section':'restore','indices':[32,33,73],'removed_position':2,'known':False}, +) +# These are PR3998's published canonical known-contraction words, including its +# ordered basis [42,82] rather than the older source's [82,42]. +KNOWN_WORD = {'base':'32415e93a50f0fdab5fa144da05977fe34bc8340bf967b91c7f7f0bc312df994', + 'extra':'439ce3544b68e3dffdb0cb4496fbc92330e825592515bc28c95580807c9d232d'} + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def unique(pairs): + result = {} + for key,value in pairs: + need(key not in result,'duplicate JSON key') + result[key] = value + return result + + +def load_json(path): + return json.loads(path.read_bytes(),object_pairs_hook=unique) + + +def canonical(value): + return json.dumps(value,sort_keys=True,separators=(',',':')) + + +def digest(value): + return hashlib.sha256(canonical(value).encode()).hexdigest() + + +def authenticate(): + for relative,(length,sha,blob) in PINS.items(): + path = HERE / relative + need(not path.is_symlink(),'source symlink: '+relative) + raw = path.read_bytes() + need(len(raw)==length and hashlib.sha256(raw).hexdigest()==sha,'source bytes: '+relative) + need(hashlib.sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest()==blob, + 'source Git blob: '+relative) + path = HERE / 'source/audit_core.py' + core = types.ModuleType('credited_staged544_audit_core') + core.__file__ = str(path) + exec(compile(path.read_bytes(),str(path),'exec'),core.__dict__) + return core + + +def load_word(provider): + need(provider in ('base','extra'),'provider domain') + authenticate() + return json.loads(gzip.decompress((HERE/'inputs'/('BORROW-WORD-'+provider+'.json.gz')).read_bytes()), + object_pairs_hook=unique) + + +def touched(gate): + need(isinstance(gate,(tuple,list)) and gate,'scalar operation tuple') + kind = gate[0] + need(kind in ('add','scale'),'unknown scalar primitive barrier') + need(len(gate)==(6 if kind=='add' else 5),'scalar operation arity') + registers = gate[1:3] if kind=='add' else gate[1:2] + need(all(type(r) is int and 0<=r<704 for r in registers),'scalar register domain') + if kind=='add': + need(registers[0]!=registers[1],'self ADD') + return set(registers) + + +def matrix(gates, registers): + rows = {r:{s:Q(r==s) for s in registers} for r in registers} + for gate in gates: + need(gate[0]=='add','A2 ADD alphabet') + need(type(gate[3]) is int and type(gate[4]) is int and gate[4]>0 and gate[3]!=0, + 'typed nonzero rational coefficient') + destination,source = gate[1:3] + coefficient = Q(gate[3],gate[4]) + donor = rows[source].copy() + rows[destination] = {r:rows[destination][r]+coefficient*donor[r] for r in registers} + return rows + + +def segments(word,section): + if section=='A': + cuts = [word['prelude_events'],len(word['A'])] + elif section=='B': + cuts = sorted({0,len(word['B'])}|{record[0] for record in word['warps']}) + else: + cuts = [0,len(word['restore'])] + return list(zip(cuts,cuts[1:])) + + +def certify_site(word,site): + need(isinstance(site,dict) and set(site)=={'section','indices','removed_position','known'},'site schema') + section,indices,position = site['section'],site['indices'],site['removed_position'] + need(section in ('A','B','restore'),'site section') + need(isinstance(indices,(tuple,list)) and len(indices)==3 and + all(type(i) is int for i in indices),'typed site indices') + need(0<=indices[0]