diff --git a/research/staged544-a2-cone-composition/.gitattributes b/research/staged544-a2-cone-composition/.gitattributes new file mode 100644 index 0000000000..f2f3bbc695 --- /dev/null +++ b/research/staged544-a2-cone-composition/.gitattributes @@ -0,0 +1,2 @@ +frozen/** -text whitespace=blank-at-eol,blank-at-eof,space-before-tab,cr-at-eol +inputs/** -text diff --git a/research/staged544-a2-cone-composition/.gitignore b/research/staged544-a2-cone-composition/.gitignore new file mode 100644 index 0000000000..7a60b85e14 --- /dev/null +++ b/research/staged544-a2-cone-composition/.gitignore @@ -0,0 +1,2 @@ +__pycache__/ +*.pyc diff --git a/research/staged544-a2-cone-composition/PROOF.md b/research/staged544-a2-cone-composition/PROOF.md new file mode 100644 index 0000000000..d8d8bce979 --- /dev/null +++ b/research/staged544-a2-cone-composition/PROOF.md @@ -0,0 +1,139 @@ +# Eight-site A2 transfer and owner-cone composition + +Chris R / Clear1nsight, with substantial OpenAI Codex assistance. Apache-2.0. + +## Exact statement + +The two current PR3945 words at `91f81d131252db704f945891da1ea54e29d46b8b` +admit all eight fixed contractions in ToikY PR4019 +`f408e09df300b575235f7f77f81948071397e16d`, including the A1858 contraction +credited to PR3998 `389268a6b5e0373a3125d5c6fcd6995f4ea324f5`. +This is a new source-specific applicability certificate; the identities and +selected sites are inherited. Native operators, role identities, cut, entrance +and terminal frames remain fixed. No register or dirty buffer is allocated. + +The complete profile remains `{1:2482,2:712,3:218,4:109,5:20,8:8}`: +3,549 recursive children and rank mass 5,160. The helper inventory remains +`{5:28,6:18,7:53,8:96,9:213}` across 408 roles. Relative to the already credited +PR3998 contraction, the additional saving is seven forward and five projected +inverse-cleanup ADD records. Against the raw current provider, it is eight and +six. These rational scalar counts are not a physical/native or runtime tariff. + +Moreover, each contracted site's two-gate frame itinerary is forced at fixed +neighbor boundaries. Composing all eight changes with the precise PR4016 +`08c8990f7022b94cf63207229465fb8fa0e8fc75` forced-intersection terminal-cone +domain leaves its finite outcome unchanged after remapping B indices. Five +survivors remove H1 locally but require at least H1 more owner idle cost under +the credited packing dual. Therefore the composition has no positive complete +optimistic allowance at the source endpoint. This is not a universal graph, +terminal or scalar-frame obstruction, nor a supplier or kappa admission. + +## Local equality, gathering and cleanup + +The sites are the original zero-based triples A(1858,1859,1860), +B(4,53,54), B(7,49,50), and restore(20,21,36), (22,23,38), +(26,27,51), (30,31,62), (32,33,73). Every gate and replacement is retained in +RESULT.json. The exact PR4019 proof is retained at frozen/sep/PROOF.md. + +For distinct x,y,z, let S(a) act by y+=a*z, T(b) by x+=b*y and U(c) +by x+=c*z. In chronological order, +`[S(a),T(b),U(-ab)]=[T(b),S(a)]` and +`[U(ab),T(b),S(a)]=[S(a),T(b)]` over the rationals. Both identities hold +on arbitrary dirty inputs, with no zero-input assumption. Both the primary +rational matrix check and ToikY's separate coordinate-column implementation +recompute each identity on the new source words. + +All intervening unselected events avoid every register in the selected support, +including reads. They commute with the selected triple. All eight supports are +pairwise disjoint. No prelude, target/centre, section or native event boundary +is crossed. Gather at the first selected position and substitute the two gates; +all other events survive in their original order. B native positions are remapped +to exactly the same surviving event cuts, and all native operator descriptors +and ordered frames stay identical. Every other top-level field compares equal. + +The non-target subsystem is autonomous because the current words satisfy the +inherited target-read hygiene. Full operator equality implies equality of its +non-target block and inverse. Literal cleanup is regenerated from that projection, +with unchanged protected-buffer renaming. Thus the composition preserves every +arbitrary dirty buffer, no buffer-to-live leakage and all endpoints. The five +new restore contractions each save one cleanup ADD; the two B contractions +remove target-writing ADDs and save no cleanup ADD. The credited old A site +saves one further forward and cleanup ADD. + +## Why there is exactly one compatible local frame itinerary + +Fix the frame just before the first selected use and the first unchanged +successor frame for each of the three touched registers. Include every climb +through that successor in the local invoice. Intervening events are disjoint, +so they impose no additional use of those registers. The source's required +checks and native entrance anchors remain fixed; the local relaxation already +includes their successor frames. + +The replacement has two gates whose supports share one register. Write their +common frames as F1 and F2; monotonic containment along the shared register +requires F1 contained in F2. The lower bound for F1 is the span of its two input +frames. Its upper bound is the intersection of **all three** fixed successor +frames: the third successor caps F2 and therefore also F1. This backward cap is +necessary; using only the first gate's two successors would retain dead ends. +On each of the eight sites this lower bound equals that upper bound. Thus F1 +is forced. After that assignment, the second gate's lower bound is the span of +its current input frames; its upper bound is the intersection of its two +successors. Those bounds also coincide. The forced pair is the original common +frame, up to equivalent basis order. Both implementations verify these set +identities and every local charge on both providers. + +Each support is disjoint from every other selected support, so the eight local +problems compose without a shared frame variable or omitted successor charge. +There is one complete flag for the fixed composite graph. Its profile agrees +rank by rank with the source, hence at every exponent, not just numerically at +one endpoint. This does not rule out optional changes outside the local bounds. + +## Changed graph and the owner-aware cone + +The exact forced-cone algorithm and tariff proof are retained from PR4016 in +frozen/cone/verify.py, tariff.py and PROOF.md. Their algorithms are reused, +not advertised as independent implementations. For every protected terminal +hyperplane, shrink its last scalar frame by intersection; propagate necessary +intersections to scalar predecessors. Reaching an incompatible immutable +entrance/native exit or a fixed check rejects. The successful assignment is +the greatest feasible one below the original scalar frames. It does not search +additional optional frame shrinks, arbitrary rotations or coupled terminals. + +Both original and combined current words yield the same 13,285 hyperplanes: +2,688 fail start containment; 10,023 reach an incompatible entrance/native; +552 reach a fixed check; 17 are the separately credited direct-refund class; +five have a changed scalar cone. The five helpers are 282, 293, 298, 309 and 373. +The entire candidate records agree except B event indices are reduced by two, +accounting for the two deleted B records before all five events. Each witness +has exactly one changed SCALE frame and terminal, local delta -H1, and width +5 to 4. All ten literal combined witnesses are reconstructed, invoiced and +checked with arbitrary-dirty forward/dual semantics and cleanup boundaries. + +At the source endpoint k=1730663236534549309146/10^24, write h(r)=r^(1-k). +The PR4016/3988 packing dual has pi4-pi5=h(1)=1. Its feasibility is rechecked +for all 2,551 capacity 8/16/32/48, width 4..9 patterns: 12 exact equalities and +2,539 strict rational interval bounds. The retained incumbent aggregate attains +the dual across 725,760 bins. Hence even fractional repacking after a width 5 to 4 +change increases the owner idle lower bound by H1. It cancels the local saving +exactly. These checks reuse the credited exact tariff engine. Actual physical +owner chronology remains inherited. Other unknown costs are not assigned zero. +The 17 direct refunds are excluded from the changed-cone claim and remain +credited to PR3988; this package does not newly audit their whole lifecycle. + +## Evidence boundaries + +The primary performs all 723-input ordinary, dual, reverse pullback and both +cleanup-boundary checks for original, credited-only and combined words for both +providers, comparing full ordinary and dual operator digests. The separate +checker reuses ToikY's no-primary-import point-set/coordinate engine on the new +inputs, reconstructs the word and cleanup digests, verifies all 149 complete +register-frame boundary states and recomputes the entire profile. A new separate +chronological timeline verifies the backward-cap singleton proof. This is +independence of representation from the primary, not fresh independent authorship +of the retained engines or a second full free-operator replay. + +Physical owner/holding/routing/control/tape costs, changed intermediate growth, +finite precision and signed-floor errors, concrete native phases/lowering, +uniform stock, all-size compilation, outer consumption and analytic/BIT +obligations remain inherited or unproved. No full multiplication theorem, +human/formal-kernel review, merger or selected-frontier change is claimed. diff --git a/research/staged544-a2-cone-composition/README.md b/research/staged544-a2-cone-composition/README.md new file mode 100644 index 0000000000..8d6d112c65 --- /dev/null +++ b/research/staged544-a2-cone-composition/README.md @@ -0,0 +1,108 @@ +# Current-provider A2 transfer with no new owner-cone allowance + +The exact current PR3945 providers admit ToikY PR4019's seven separated A2 +contractions together with the credited PR3998 A1858 contraction. Relative to +that already credited contraction, this removes **seven forward and five inverse +cleanup scalar ADDs**. Both complete paid profiles remain +`{1:2482,2:712,3:218,4:109,5:20,8:8}`: 3,549 children and rank mass 5,160. +There is no recursive-moment, runtime or kappa improvement. + +This answers PR4019's explicit later-word handoff and tests the requested +combination with PR4016's forced scalar cones and owner dual. The eight-site +changed graph has exactly one compatible two-gate frame assignment per site at +fixed neighboring boundaries. Backward cap propagation proves this directly; +first-step flags that cannot reach the second gate are excluded. Its terminal +cone census reproduces PR4016 exactly after B-index remapping: 13,285 hyperplanes, +five changed-cone survivors, each local -H1 canceled by at least +H1 owner idle +cost. The owner bound allows arbitrary fractional repacking. The 17 prior direct +refund cases are retained as a separate credited class, not re-admitted here. + +This is a bounded combination certificate, not a general graph search or proof +that optional interior changes, coupled terminal edits, rotations or changed +native interfaces cannot work. The complete favorable allowance stops further +dependent expansion of this fixed composite. + +## Frozen sources and credit + +- PR3945 `91f81d131252db704f945891da1ea54e29d46b8b`: the two current input words, + native descriptors and lineage notice, by Dugongue with retained predecessors. +- ToikY PR4019 `f408e09df300b575235f7f77f81948071397e16d`: the seven separated + sites, local identity/composition proof and separate point-set checker. +- Chris R/Clear1nsight PR3998 `389268a6b5e0373a3125d5c6fcd6995f4ea324f5`: + A2 graph identity, credited consecutive A1858 contraction and current-source + source exports; dataisfire PR3734 supplies the older literal-word lineage. +- PR4016 `08c8990f7022b94cf63207229465fb8fa0e8fc75`: exact forced-cone and + owner-dual algorithms; PR3988, PR3969 and PR3815/3862/3890 retain tariff, + owner aggregate and packing-dual credit. Jeremy Kothe, zxv, RossRichardson, + ErwanSecousses and hexapode retain related profile/packing credit. +- Sagar Thakrar, roger-sato and Arham Tahir retain auditor/frame/native lineage; + unchanged notices are in `frozen/`. PR1865 by 1337isnot1337 retains the earlier + distinct nonconsecutive commuting-C3 precedent. + +Canonical base is `20ecf2891d80b5acf18d980b2164fb44ea7faa90`. Fourteen exact +package-local exports are authenticated with SHA256, length and Git blob before +execution. `SOURCES.json` records original source paths and commits. No pending +source history or network access is needed for execution. Only documented pure +helpers are invoked from retained modules; their older input-specific CLI +entrypoints are not used. In particular the old PR3734 manifest/constants +inside retained PR4019 files are historical context, not current-word pins. +Actual current inputs are independently hard-pinned by the second checker. + +## Proof and evidence + +`PROOF.md` gives exact scope, local gathering, projected inverse cleanup, +unique complete frame flags and owner-aware cone composition. `RESULT.json` +binds every site, reconstructed word/cleanup, full profile, cone candidate and +operator digest. The native descriptor order and frames, all helper entrances +and roles, and all other source fields remain unchanged; B positions account +only for deletion of the two selected B records. + +The primary checker reuses the credited rational dirty-state auditor, PR4019 +local checker and PR4016 cone/tariff engines. It replays source, credited-only and +combined current words on all 723 formal inputs, ordinary and dual operators, +reverse pullback and cleanup boundaries. Ten further combined cone witnesses +receive arbitrary-dirty forward/dual and cleanup-boundary checks. + +The second checker imports only ToikY's separate point-set/coordinate engine, +recomputes all 16 local identities, reconstructs all six words, compares their +cleanup digests and149 full-register frame states, and computes their complete +invoices. Its new chronological timeline separately verifies all 16 unique +complete frame flags. Fourteen inherited semantic controls plus six production +semantic controls and two actual optimized-CLI source/owner-receipt mutations +must reject. This is credited independent representation, not a newly independent +full-word interpreter or human/formal-kernel acceptance. + +Run from the repository root: + +```sh +python3 -B scripts/research_package.py --package research/staged544-a2-cone-composition +``` + +The five registered commands verify base, extra, the 2,551-pattern owner dual, +the separate composition checker and controls. Python 3.12 standard library; +no optional packages. Full generation is explicit `verify.py --record`; normal +verification is read-only. `--quick` omits full dirty semantics and is for bounded +controls only. A passing certificate is not full supplier admission. + +Physical owner/holding/routing/control/tape costs, changed intermediate precision +and signed-floor behavior, concrete native phases/lowering, uniform stock, +all-size compilation, outer consumption and analytic/BIT obligations are inherited +or unproved, never priced as zero. No scalar/native unit-cost equivalence or +measured speedup is asserted. + +## Open next questions + +- Can a genuinely different graph or changed native/check boundary remove a + charged transition? Specify that exact boundary and a positive complete + owner-aware allowance before expanding a search. This eight-site composition + supplies neither; another adjacent census is not justified by these ties. +- Can the current producer adopt the verified scalar saving with its concrete + native/precision/owner implementation? First independently replay the frozen + transfer and audit intermediate growth. This package preserves formal operator + and frame contracts but does not admit those physical obligations. + +New transfer/composition work by Chris R/Clear1nsight with substantial OpenAI +Codex assistance. Apache-2.0. No merge, closure of others' work or selected-frontier +change. Entry overlap covered all 733 open PR bodies at 10:46:04 UTC, bounded live +handoffs and relevant predecessor claims; broader Discussion/code coverage is +partial. `TASK.json` retains the actual narrowed task and stopping decision. diff --git a/research/staged544-a2-cone-composition/RESULT.json b/research/staged544-a2-cone-composition/RESULT.json new file mode 100644 index 0000000000..72308407cd --- /dev/null +++ b/research/staged544-a2-cone-composition/RESULT.json @@ -0,0 +1,3344 @@ +{ + "schema_version": 1, + "tariff": { + "patterns": 2551, + "tight": 12, + "strict": 2539, + "refund_debit": "H1 exactly", + "incumbent_bins": 725760 + }, + "providers": { + "base": { + "provider": "base", + "sites": [ + { + "section": "A", + "indices": [ + 1858, + 1859, + 1860 + ], + "removed_position": 2, + "known": true, + "support": [ + 456, + 457, + 475 + ], + "gates": [ + [ + "add", + 457, + 475, + -1, + 1, + [ + 82, + 42 + ] + ], + [ + "add", + 456, + 457, + 1, + 1, + [ + 82, + 42 + ] + ], + [ + "add", + 456, + 475, + 1, + 1, + [ + 82, + 42 + ] + ] + ], + "replacement": [ + [ + "add", + 456, + 457, + 1, + 1, + [ + 42, + 82 + ] + ], + [ + "add", + 457, + 475, + -1, + 1, + [ + 42, + 82 + ] + ] + ], + "crossed_disjoint_events": 0 + }, + { + "section": "B", + "indices": [ + 4, + 53, + 54 + ], + "removed_position": 0, + "known": false, + "support": [ + 196, + 518, + 588 + ], + "gates": [ + [ + "add", + 196, + 518, + 1, + 1, + [ + 30 + ] + ], + [ + "add", + 196, + 588, + -1, + 1, + [ + 30 + ] + ], + [ + "add", + 588, + 518, + -1, + 1, + [ + 30 + ] + ] + ], + "replacement": [ + [ + "add", + 588, + 518, + -1, + 1, + [ + 30 + ] + ], + [ + "add", + 196, + 588, + -1, + 1, + [ + 30 + ] + ] + ], + "crossed_disjoint_events": 48 + }, + { + "section": "B", + "indices": [ + 7, + 49, + 50 + ], + "removed_position": 0, + "known": false, + "support": [ + 187, + 506, + 586 + ], + "gates": [ + [ + "add", + 187, + 506, + 1, + 1, + [ + 30 + ] + ], + [ + "add", + 187, + 586, + 1, + 2, + [ + 30 + ] + ], + [ + "add", + 586, + 506, + 2, + 1, + [ + 30 + ] + ] + ], + "replacement": [ + [ + "add", + 586, + 506, + 2, + 1, + [ + 30 + ] + ], + [ + "add", + 187, + 586, + 1, + 2, + [ + 30 + ] + ] + ], + "crossed_disjoint_events": 41 + }, + { + "section": "restore", + "indices": [ + 20, + 21, + 36 + ], + "removed_position": 2, + "known": false, + "support": [ + 231, + 448, + 484 + ], + "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 + ] + ] + ], + "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 + ] + ] + ], + "crossed_disjoint_events": 14 + }, + { + "section": "restore", + "indices": [ + 22, + 23, + 38 + ], + "removed_position": 2, + "known": false, + "support": [ + 226, + 449, + 485 + ], + "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 + ] + ] + ], + "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 + ] + ] + ], + "crossed_disjoint_events": 14 + }, + { + "section": "restore", + "indices": [ + 26, + 27, + 51 + ], + "removed_position": 2, + "known": false, + "support": [ + 228, + 451, + 509 + ], + "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 + ] + ] + ], + "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 + ] + ] + ], + "crossed_disjoint_events": 23 + }, + { + "section": "restore", + "indices": [ + 30, + 31, + 62 + ], + "removed_position": 2, + "known": false, + "support": [ + 7, + 453, + 533 + ], + "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 + ] + ] + ], + "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 + ] + ] + ], + "crossed_disjoint_events": 30 + }, + { + "section": "restore", + "indices": [ + 32, + 33, + 73 + ], + "removed_position": 2, + "known": false, + "support": [ + 236, + 454, + 556 + ], + "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 + ] + ] + ], + "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 + ] + ] + ], + "crossed_disjoint_events": 39 + } + ], + "words": { + "source": { + "profile": { + "1": 2482, + "2": 712, + "3": 218, + "4": 109, + "5": 20, + "8": 8 + }, + "helper_widths": { + "5": 28, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + }, + "lengths": { + "A": 4079, + "B": 1870, + "restore": 212, + "cleanup": 5225 + }, + "primitive_counts": { + "A": { + "add": 3557, + "scale": 498, + "warp": 24 + }, + "B": { + "add": 1796, + "scale": 74, + "warp": 0 + }, + "restore": { + "add": 196, + "scale": 16, + "warp": 0 + }, + "cleanup": { + "add": 4633, + "scale": 520, + "warp": 72 + } + }, + "canonical_word_sha256": "cee1ddcbdf3cdcba99146f281cbb452440dd1ed641aa3a47ccc3343680ae7ddc", + "cleanup_sha256": "c3a820f5d4aeb3ae9b3c6deff4dcf377a50299295783217dd86313b3bcb208af", + "native_operations": 72, + "semantics": { + "live_inputs": 632, + "arbitrary_dirty_buffers": 91, + "matrix_dimension": 723, + "ordinary_matrix_sha256": "c8ea87b1598c9bbc2b0be63217772110ff450ad12eff19aaf05a84239eb5d380", + "dual_matrix_sha256": "9bace9fb7525f64d5418ab54af173df7d320c898e980e89be8a90d280adb3744", + "ordinary": true, + "dual": true, + "reverse_equals_ordinary": true, + "cleanup_boundary_both_directions": true, + "buffer_to_live_leaks": 0, + "buffer_self_map": "identity" + } + }, + "credited_3998": { + "profile": { + "1": 2482, + "2": 712, + "3": 218, + "4": 109, + "5": 20, + "8": 8 + }, + "helper_widths": { + "5": 28, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + }, + "lengths": { + "A": 4078, + "B": 1870, + "restore": 212, + "cleanup": 5224 + }, + "primitive_counts": { + "A": { + "add": 3556, + "scale": 498, + "warp": 24 + }, + "B": { + "add": 1796, + "scale": 74, + "warp": 0 + }, + "restore": { + "add": 196, + "scale": 16, + "warp": 0 + }, + "cleanup": { + "add": 4632, + "scale": 520, + "warp": 72 + } + }, + "canonical_word_sha256": "72701332e9b0281850e47916d929fd3d9bd9e14f3fafb1ee14d4c3ae3fc6b5d9", + "cleanup_sha256": "1fe863366ac0a277b32795c4d88aa9544313248ff29c5e0dea7c36e3adcfd878", + "native_operations": 72, + "semantics": { + "live_inputs": 632, + "arbitrary_dirty_buffers": 91, + "matrix_dimension": 723, + "ordinary_matrix_sha256": "c8ea87b1598c9bbc2b0be63217772110ff450ad12eff19aaf05a84239eb5d380", + "dual_matrix_sha256": "9bace9fb7525f64d5418ab54af173df7d320c898e980e89be8a90d280adb3744", + "ordinary": true, + "dual": true, + "reverse_equals_ordinary": true, + "cleanup_boundary_both_directions": true, + "buffer_to_live_leaks": 0, + "buffer_self_map": "identity" + } + }, + "combined": { + "profile": { + "1": 2482, + "2": 712, + "3": 218, + "4": 109, + "5": 20, + "8": 8 + }, + "helper_widths": { + "5": 28, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + }, + "lengths": { + "A": 4078, + "B": 1868, + "restore": 207, + "cleanup": 5219 + }, + "primitive_counts": { + "A": { + "add": 3556, + "scale": 498, + "warp": 24 + }, + "B": { + "add": 1794, + "scale": 74, + "warp": 0 + }, + "restore": { + "add": 191, + "scale": 16, + "warp": 0 + }, + "cleanup": { + "add": 4627, + "scale": 520, + "warp": 72 + } + }, + "canonical_word_sha256": "20252290a5be71f5e226a37e635d2979d38196e2d843320050b4259a083447fc", + "cleanup_sha256": "f124a485bc57cc2e9426c255e554bffd6a54b6efb0d48cbae2c515c8330f270f", + "native_operations": 72, + "semantics": { + "live_inputs": 632, + "arbitrary_dirty_buffers": 91, + "matrix_dimension": 723, + "ordinary_matrix_sha256": "c8ea87b1598c9bbc2b0be63217772110ff450ad12eff19aaf05a84239eb5d380", + "dual_matrix_sha256": "9bace9fb7525f64d5418ab54af173df7d320c898e980e89be8a90d280adb3744", + "ordinary": true, + "dual": true, + "reverse_equals_ordinary": true, + "cleanup_boundary_both_directions": true, + "buffer_to_live_leaks": 0, + "buffer_self_map": "identity" + } + } + }, + "fixed_boundary_frames": [ + { + "section": "A", + "indices": [ + 1858, + 1859, + 1860 + ], + "unique_flag": [ + [ + 42, + 82 + ], + [ + 42, + 82 + ] + ], + "intervals": [ + { + "lower": [ + 42, + 82 + ], + "upper": [ + 42, + 82 + ] + }, + { + "lower": [ + 42, + 82 + ], + "upper": [ + 42, + 82 + ] + } + ], + "profile_delta": {} + }, + { + "section": "B", + "indices": [ + 4, + 53, + 54 + ], + "unique_flag": [ + [ + 30 + ], + [ + 30 + ] + ], + "intervals": [ + { + "lower": [ + 30 + ], + "upper": [ + 30 + ] + }, + { + "lower": [ + 30 + ], + "upper": [ + 30 + ] + } + ], + "profile_delta": {} + }, + { + "section": "B", + "indices": [ + 7, + 49, + 50 + ], + "unique_flag": [ + [ + 30 + ], + [ + 30 + ] + ], + "intervals": [ + { + "lower": [ + 30 + ], + "upper": [ + 30 + ] + }, + { + "lower": [ + 30 + ], + "upper": [ + 30 + ] + } + ], + "profile_delta": {} + }, + { + "section": "restore", + "indices": [ + 20, + 21, + 36 + ], + "unique_flag": [ + [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ], + [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ] + ], + "intervals": [ + { + "lower": [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ], + "upper": [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ] + }, + { + "lower": [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ], + "upper": [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ] + } + ], + "profile_delta": {} + }, + { + "section": "restore", + "indices": [ + 22, + 23, + 38 + ], + "unique_flag": [ + [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ], + [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ] + ], + "intervals": [ + { + "lower": [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ], + "upper": [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ] + }, + { + "lower": [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ], + "upper": [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ] + } + ], + "profile_delta": {} + }, + { + "section": "restore", + "indices": [ + 26, + 27, + 51 + ], + "unique_flag": [ + [ + 1, + 10, + 20, + 38, + 64, + 128, + 256 + ], + [ + 1, + 10, + 20, + 38, + 64, + 128, + 256 + ] + ], + "intervals": [ + { + "lower": [ + 1, + 10, + 20, + 38, + 64, + 128, + 256 + ], + "upper": [ + 1, + 10, + 20, + 38, + 64, + 128, + 256 + ] + }, + { + "lower": [ + 1, + 10, + 20, + 38, + 64, + 128, + 256 + ], + "upper": [ + 1, + 10, + 20, + 38, + 64, + 128, + 256 + ] + } + ], + "profile_delta": {} + }, + { + "section": "restore", + "indices": [ + 30, + 31, + 62 + ], + "unique_flag": [ + [ + 6, + 11, + 19, + 32, + 64, + 128, + 256 + ], + [ + 6, + 11, + 19, + 32, + 64, + 128, + 256 + ] + ], + "intervals": [ + { + "lower": [ + 6, + 11, + 19, + 32, + 64, + 128, + 256 + ], + "upper": [ + 6, + 11, + 19, + 32, + 64, + 128, + 256 + ] + }, + { + "lower": [ + 6, + 11, + 19, + 32, + 64, + 128, + 256 + ], + "upper": [ + 6, + 11, + 19, + 32, + 64, + 128, + 256 + ] + } + ], + "profile_delta": {} + }, + { + "section": "restore", + "indices": [ + 32, + 33, + 73 + ], + "unique_flag": [ + [ + 3, + 8, + 21, + 37, + 64, + 128, + 256 + ], + [ + 3, + 8, + 21, + 37, + 64, + 128, + 256 + ] + ], + "intervals": [ + { + "lower": [ + 3, + 8, + 21, + 37, + 64, + 128, + 256 + ], + "upper": [ + 3, + 8, + 21, + 37, + 64, + 128, + 256 + ] + }, + { + "lower": [ + 3, + 8, + 21, + 37, + 64, + 128, + 256 + ], + "upper": [ + 3, + 8, + 21, + 37, + 64, + 128, + 256 + ] + } + ], + "profile_delta": {} + } + ], + "cone": { + "total_hyperplanes": 13285, + "rejected": { + "credited-direct-refund": 17, + "fixed-check": 552, + "fixed-entrance/native": 10023, + "start-terminal": 2688 + }, + "candidates": [ + { + "register": 282, + "old_terminal": [ + 388, + 67, + 33, + 18, + 8 + ], + "new_terminal": [ + 26, + 41, + 75, + 388 + ], + "edits": [ + { + "section": "B", + "index": 533, + "old": [ + 388, + 67, + 33, + 18, + 8 + ], + "new": [ + 26, + 41, + 75, + 388 + ] + } + ], + "width_before": 5, + "width_after": 4, + "local_delta": { + "1": -1 + }, + "owner_debit": { + "1": 1 + }, + "optimistic_complete_delta": {} + }, + { + "register": 293, + "old_terminal": [ + 273, + 145, + 85, + 51, + 8 + ], + "new_terminal": [ + 51, + 85, + 145, + 273 + ], + "edits": [ + { + "section": "B", + "index": 552, + "old": [ + 273, + 145, + 85, + 51, + 8 + ], + "new": [ + 51, + 85, + 145, + 273 + ] + } + ], + "width_before": 5, + "width_after": 4, + "local_delta": { + "1": -1 + }, + "owner_debit": { + "1": 1 + }, + "optimistic_complete_delta": {} + }, + { + "register": 298, + "old_terminal": [ + 273, + 145, + 85, + 51, + 8 + ], + "new_terminal": [ + 51, + 85, + 145, + 273 + ], + "edits": [ + { + "section": "B", + "index": 557, + "old": [ + 273, + 145, + 85, + 51, + 8 + ], + "new": [ + 51, + 85, + 145, + 273 + ] + } + ], + "width_before": 5, + "width_after": 4, + "local_delta": { + "1": -1 + }, + "owner_debit": { + "1": 1 + }, + "optimistic_complete_delta": {} + }, + { + "register": 309, + "old_terminal": [ + 385, + 66, + 36, + 22, + 8 + ], + "new_terminal": [ + 30, + 44, + 74, + 385 + ], + "edits": [ + { + "section": "B", + "index": 578, + "old": [ + 385, + 66, + 36, + 22, + 8 + ], + "new": [ + 30, + 44, + 74, + 385 + ] + } + ], + "width_before": 5, + "width_after": 4, + "local_delta": { + "1": -1 + }, + "owner_debit": { + "1": 1 + }, + "optimistic_complete_delta": {} + }, + { + "register": 373, + "old_terminal": [ + 257, + 137, + 67, + 37, + 22 + ], + "new_terminal": [ + 22, + 37, + 67, + 392 + ], + "edits": [ + { + "section": "B", + "index": 680, + "old": [ + 257, + 137, + 67, + 37, + 22 + ], + "new": [ + 22, + 37, + 67, + 392 + ] + } + ], + "width_before": 5, + "width_after": 4, + "local_delta": { + "1": -1 + }, + "owner_debit": { + "1": 1 + }, + "optimistic_complete_delta": {} + } + ] + }, + "cone_witnesses": [ + { + "register": 282, + "word_sha256": "d0ffb118893388f92e95246566488777176b0c731939ca2d05ba06fbc8787905", + "local_delta": { + "1": -1 + }, + "owner_debit": { + "1": 1 + }, + "optimistic_complete_delta": {} + }, + { + "register": 293, + "word_sha256": "528e5c22dc7ceb3af76f994f2a6b170b39f0a07b3df60a7d2b91aa24e54a8185", + "local_delta": { + "1": -1 + }, + "owner_debit": { + "1": 1 + }, + "optimistic_complete_delta": {} + }, + { + "register": 298, + "word_sha256": "745ca3bdad2f529a031b3dc87541835f8ddb41ee44429460014ba12ed1210597", + "local_delta": { + "1": -1 + }, + "owner_debit": { + "1": 1 + }, + "optimistic_complete_delta": {} + }, + { + "register": 309, + "word_sha256": "3bd7e39c693da212e462c31eace2a5b06482fc6f455307b6ceb9006b4a1137f8", + "local_delta": { + "1": -1 + }, + "owner_debit": { + "1": 1 + }, + "optimistic_complete_delta": {} + }, + { + "register": 373, + "word_sha256": "e1a9a42c93a8226806e1f9e88f0834a02f13e98c37adbcc829e4ed98ac6a7ab7", + "local_delta": { + "1": -1 + }, + "owner_debit": { + "1": 1 + }, + "optimistic_complete_delta": {} + } + ], + "scalar_saving_vs_3998": { + "forward": 7, + "cleanup": 5 + }, + "new_kappa": false + }, + "extra": { + "provider": "extra", + "sites": [ + { + "section": "A", + "indices": [ + 1858, + 1859, + 1860 + ], + "removed_position": 2, + "known": true, + "support": [ + 456, + 457, + 475 + ], + "gates": [ + [ + "add", + 457, + 475, + -1, + 1, + [ + 82, + 42 + ] + ], + [ + "add", + 456, + 457, + 1, + 1, + [ + 82, + 42 + ] + ], + [ + "add", + 456, + 475, + 1, + 1, + [ + 82, + 42 + ] + ] + ], + "replacement": [ + [ + "add", + 456, + 457, + 1, + 1, + [ + 42, + 82 + ] + ], + [ + "add", + 457, + 475, + -1, + 1, + [ + 42, + 82 + ] + ] + ], + "crossed_disjoint_events": 0 + }, + { + "section": "B", + "indices": [ + 4, + 53, + 54 + ], + "removed_position": 0, + "known": false, + "support": [ + 196, + 518, + 588 + ], + "gates": [ + [ + "add", + 196, + 518, + 1, + 1, + [ + 30 + ] + ], + [ + "add", + 196, + 588, + -1, + 1, + [ + 30 + ] + ], + [ + "add", + 588, + 518, + -1, + 1, + [ + 30 + ] + ] + ], + "replacement": [ + [ + "add", + 588, + 518, + -1, + 1, + [ + 30 + ] + ], + [ + "add", + 196, + 588, + -1, + 1, + [ + 30 + ] + ] + ], + "crossed_disjoint_events": 48 + }, + { + "section": "B", + "indices": [ + 7, + 49, + 50 + ], + "removed_position": 0, + "known": false, + "support": [ + 187, + 506, + 586 + ], + "gates": [ + [ + "add", + 187, + 506, + 1, + 1, + [ + 30 + ] + ], + [ + "add", + 187, + 586, + 1, + 2, + [ + 30 + ] + ], + [ + "add", + 586, + 506, + 2, + 1, + [ + 30 + ] + ] + ], + "replacement": [ + [ + "add", + 586, + 506, + 2, + 1, + [ + 30 + ] + ], + [ + "add", + 187, + 586, + 1, + 2, + [ + 30 + ] + ] + ], + "crossed_disjoint_events": 41 + }, + { + "section": "restore", + "indices": [ + 20, + 21, + 36 + ], + "removed_position": 2, + "known": false, + "support": [ + 231, + 448, + 484 + ], + "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 + ] + ] + ], + "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 + ] + ] + ], + "crossed_disjoint_events": 14 + }, + { + "section": "restore", + "indices": [ + 22, + 23, + 38 + ], + "removed_position": 2, + "known": false, + "support": [ + 226, + 449, + 485 + ], + "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 + ] + ] + ], + "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 + ] + ] + ], + "crossed_disjoint_events": 14 + }, + { + "section": "restore", + "indices": [ + 26, + 27, + 51 + ], + "removed_position": 2, + "known": false, + "support": [ + 228, + 451, + 509 + ], + "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 + ] + ] + ], + "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 + ] + ] + ], + "crossed_disjoint_events": 23 + }, + { + "section": "restore", + "indices": [ + 30, + 31, + 62 + ], + "removed_position": 2, + "known": false, + "support": [ + 7, + 453, + 533 + ], + "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 + ] + ] + ], + "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 + ] + ] + ], + "crossed_disjoint_events": 30 + }, + { + "section": "restore", + "indices": [ + 32, + 33, + 73 + ], + "removed_position": 2, + "known": false, + "support": [ + 236, + 454, + 556 + ], + "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 + ] + ] + ], + "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 + ] + ] + ], + "crossed_disjoint_events": 39 + } + ], + "words": { + "source": { + "profile": { + "1": 2482, + "2": 712, + "3": 218, + "4": 109, + "5": 20, + "8": 8 + }, + "helper_widths": { + "5": 28, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + }, + "lengths": { + "A": 4079, + "B": 1870, + "restore": 212, + "cleanup": 5225 + }, + "primitive_counts": { + "A": { + "add": 3557, + "scale": 498, + "warp": 24 + }, + "B": { + "add": 1796, + "scale": 74, + "warp": 0 + }, + "restore": { + "add": 196, + "scale": 16, + "warp": 0 + }, + "cleanup": { + "add": 4633, + "scale": 520, + "warp": 72 + } + }, + "canonical_word_sha256": "cc1826748ed24cd085a5756b46f0090d5a43ad54820c025366cf2848aca589b2", + "cleanup_sha256": "c3a820f5d4aeb3ae9b3c6deff4dcf377a50299295783217dd86313b3bcb208af", + "native_operations": 72, + "semantics": { + "live_inputs": 632, + "arbitrary_dirty_buffers": 91, + "matrix_dimension": 723, + "ordinary_matrix_sha256": "c8ea87b1598c9bbc2b0be63217772110ff450ad12eff19aaf05a84239eb5d380", + "dual_matrix_sha256": "9bace9fb7525f64d5418ab54af173df7d320c898e980e89be8a90d280adb3744", + "ordinary": true, + "dual": true, + "reverse_equals_ordinary": true, + "cleanup_boundary_both_directions": true, + "buffer_to_live_leaks": 0, + "buffer_self_map": "identity" + } + }, + "credited_3998": { + "profile": { + "1": 2482, + "2": 712, + "3": 218, + "4": 109, + "5": 20, + "8": 8 + }, + "helper_widths": { + "5": 28, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + }, + "lengths": { + "A": 4078, + "B": 1870, + "restore": 212, + "cleanup": 5224 + }, + "primitive_counts": { + "A": { + "add": 3556, + "scale": 498, + "warp": 24 + }, + "B": { + "add": 1796, + "scale": 74, + "warp": 0 + }, + "restore": { + "add": 196, + "scale": 16, + "warp": 0 + }, + "cleanup": { + "add": 4632, + "scale": 520, + "warp": 72 + } + }, + "canonical_word_sha256": "9c47d4c86244d533553fd60cdcf587677b3236a8d2b90e8d6b255b0917531f4c", + "cleanup_sha256": "1fe863366ac0a277b32795c4d88aa9544313248ff29c5e0dea7c36e3adcfd878", + "native_operations": 72, + "semantics": { + "live_inputs": 632, + "arbitrary_dirty_buffers": 91, + "matrix_dimension": 723, + "ordinary_matrix_sha256": "c8ea87b1598c9bbc2b0be63217772110ff450ad12eff19aaf05a84239eb5d380", + "dual_matrix_sha256": "9bace9fb7525f64d5418ab54af173df7d320c898e980e89be8a90d280adb3744", + "ordinary": true, + "dual": true, + "reverse_equals_ordinary": true, + "cleanup_boundary_both_directions": true, + "buffer_to_live_leaks": 0, + "buffer_self_map": "identity" + } + }, + "combined": { + "profile": { + "1": 2482, + "2": 712, + "3": 218, + "4": 109, + "5": 20, + "8": 8 + }, + "helper_widths": { + "5": 28, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + }, + "lengths": { + "A": 4078, + "B": 1868, + "restore": 207, + "cleanup": 5219 + }, + "primitive_counts": { + "A": { + "add": 3556, + "scale": 498, + "warp": 24 + }, + "B": { + "add": 1794, + "scale": 74, + "warp": 0 + }, + "restore": { + "add": 191, + "scale": 16, + "warp": 0 + }, + "cleanup": { + "add": 4627, + "scale": 520, + "warp": 72 + } + }, + "canonical_word_sha256": "b3a3b0573a50c39e05f40e0efb7612940049b6b990db7ac7ed9a8c66aa7dfcb7", + "cleanup_sha256": "f124a485bc57cc2e9426c255e554bffd6a54b6efb0d48cbae2c515c8330f270f", + "native_operations": 72, + "semantics": { + "live_inputs": 632, + "arbitrary_dirty_buffers": 91, + "matrix_dimension": 723, + "ordinary_matrix_sha256": "c8ea87b1598c9bbc2b0be63217772110ff450ad12eff19aaf05a84239eb5d380", + "dual_matrix_sha256": "9bace9fb7525f64d5418ab54af173df7d320c898e980e89be8a90d280adb3744", + "ordinary": true, + "dual": true, + "reverse_equals_ordinary": true, + "cleanup_boundary_both_directions": true, + "buffer_to_live_leaks": 0, + "buffer_self_map": "identity" + } + } + }, + "fixed_boundary_frames": [ + { + "section": "A", + "indices": [ + 1858, + 1859, + 1860 + ], + "unique_flag": [ + [ + 42, + 82 + ], + [ + 42, + 82 + ] + ], + "intervals": [ + { + "lower": [ + 42, + 82 + ], + "upper": [ + 42, + 82 + ] + }, + { + "lower": [ + 42, + 82 + ], + "upper": [ + 42, + 82 + ] + } + ], + "profile_delta": {} + }, + { + "section": "B", + "indices": [ + 4, + 53, + 54 + ], + "unique_flag": [ + [ + 30 + ], + [ + 30 + ] + ], + "intervals": [ + { + "lower": [ + 30 + ], + "upper": [ + 30 + ] + }, + { + "lower": [ + 30 + ], + "upper": [ + 30 + ] + } + ], + "profile_delta": {} + }, + { + "section": "B", + "indices": [ + 7, + 49, + 50 + ], + "unique_flag": [ + [ + 30 + ], + [ + 30 + ] + ], + "intervals": [ + { + "lower": [ + 30 + ], + "upper": [ + 30 + ] + }, + { + "lower": [ + 30 + ], + "upper": [ + 30 + ] + } + ], + "profile_delta": {} + }, + { + "section": "restore", + "indices": [ + 20, + 21, + 36 + ], + "unique_flag": [ + [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ], + [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ] + ], + "intervals": [ + { + "lower": [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ], + "upper": [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ] + }, + { + "lower": [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ], + "upper": [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ] + } + ], + "profile_delta": {} + }, + { + "section": "restore", + "indices": [ + 22, + 23, + 38 + ], + "unique_flag": [ + [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ], + [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ] + ], + "intervals": [ + { + "lower": [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ], + "upper": [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ] + }, + { + "lower": [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ], + "upper": [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ] + } + ], + "profile_delta": {} + }, + { + "section": "restore", + "indices": [ + 26, + 27, + 51 + ], + "unique_flag": [ + [ + 1, + 10, + 20, + 38, + 64, + 128, + 256 + ], + [ + 1, + 10, + 20, + 38, + 64, + 128, + 256 + ] + ], + "intervals": [ + { + "lower": [ + 1, + 10, + 20, + 38, + 64, + 128, + 256 + ], + "upper": [ + 1, + 10, + 20, + 38, + 64, + 128, + 256 + ] + }, + { + "lower": [ + 1, + 10, + 20, + 38, + 64, + 128, + 256 + ], + "upper": [ + 1, + 10, + 20, + 38, + 64, + 128, + 256 + ] + } + ], + "profile_delta": {} + }, + { + "section": "restore", + "indices": [ + 30, + 31, + 62 + ], + "unique_flag": [ + [ + 6, + 11, + 19, + 32, + 64, + 128, + 256 + ], + [ + 6, + 11, + 19, + 32, + 64, + 128, + 256 + ] + ], + "intervals": [ + { + "lower": [ + 6, + 11, + 19, + 32, + 64, + 128, + 256 + ], + "upper": [ + 6, + 11, + 19, + 32, + 64, + 128, + 256 + ] + }, + { + "lower": [ + 6, + 11, + 19, + 32, + 64, + 128, + 256 + ], + "upper": [ + 6, + 11, + 19, + 32, + 64, + 128, + 256 + ] + } + ], + "profile_delta": {} + }, + { + "section": "restore", + "indices": [ + 32, + 33, + 73 + ], + "unique_flag": [ + [ + 3, + 8, + 21, + 37, + 64, + 128, + 256 + ], + [ + 3, + 8, + 21, + 37, + 64, + 128, + 256 + ] + ], + "intervals": [ + { + "lower": [ + 3, + 8, + 21, + 37, + 64, + 128, + 256 + ], + "upper": [ + 3, + 8, + 21, + 37, + 64, + 128, + 256 + ] + }, + { + "lower": [ + 3, + 8, + 21, + 37, + 64, + 128, + 256 + ], + "upper": [ + 3, + 8, + 21, + 37, + 64, + 128, + 256 + ] + } + ], + "profile_delta": {} + } + ], + "cone": { + "total_hyperplanes": 13285, + "rejected": { + "credited-direct-refund": 17, + "fixed-check": 552, + "fixed-entrance/native": 10023, + "start-terminal": 2688 + }, + "candidates": [ + { + "register": 282, + "old_terminal": [ + 388, + 67, + 33, + 18, + 8 + ], + "new_terminal": [ + 26, + 41, + 75, + 388 + ], + "edits": [ + { + "section": "B", + "index": 533, + "old": [ + 388, + 67, + 33, + 18, + 8 + ], + "new": [ + 26, + 41, + 75, + 388 + ] + } + ], + "width_before": 5, + "width_after": 4, + "local_delta": { + "1": -1 + }, + "owner_debit": { + "1": 1 + }, + "optimistic_complete_delta": {} + }, + { + "register": 293, + "old_terminal": [ + 273, + 145, + 85, + 51, + 8 + ], + "new_terminal": [ + 51, + 85, + 145, + 273 + ], + "edits": [ + { + "section": "B", + "index": 552, + "old": [ + 273, + 145, + 85, + 51, + 8 + ], + "new": [ + 51, + 85, + 145, + 273 + ] + } + ], + "width_before": 5, + "width_after": 4, + "local_delta": { + "1": -1 + }, + "owner_debit": { + "1": 1 + }, + "optimistic_complete_delta": {} + }, + { + "register": 298, + "old_terminal": [ + 273, + 145, + 85, + 51, + 8 + ], + "new_terminal": [ + 51, + 85, + 145, + 273 + ], + "edits": [ + { + "section": "B", + "index": 557, + "old": [ + 273, + 145, + 85, + 51, + 8 + ], + "new": [ + 51, + 85, + 145, + 273 + ] + } + ], + "width_before": 5, + "width_after": 4, + "local_delta": { + "1": -1 + }, + "owner_debit": { + "1": 1 + }, + "optimistic_complete_delta": {} + }, + { + "register": 309, + "old_terminal": [ + 385, + 66, + 36, + 22, + 8 + ], + "new_terminal": [ + 30, + 44, + 74, + 385 + ], + "edits": [ + { + "section": "B", + "index": 578, + "old": [ + 385, + 66, + 36, + 22, + 8 + ], + "new": [ + 30, + 44, + 74, + 385 + ] + } + ], + "width_before": 5, + "width_after": 4, + "local_delta": { + "1": -1 + }, + "owner_debit": { + "1": 1 + }, + "optimistic_complete_delta": {} + }, + { + "register": 373, + "old_terminal": [ + 257, + 137, + 67, + 37, + 22 + ], + "new_terminal": [ + 22, + 37, + 67, + 392 + ], + "edits": [ + { + "section": "B", + "index": 680, + "old": [ + 257, + 137, + 67, + 37, + 22 + ], + "new": [ + 22, + 37, + 67, + 392 + ] + } + ], + "width_before": 5, + "width_after": 4, + "local_delta": { + "1": -1 + }, + "owner_debit": { + "1": 1 + }, + "optimistic_complete_delta": {} + } + ] + }, + "cone_witnesses": [ + { + "register": 282, + "word_sha256": "a65eb7e21c433d54fa428e39fb4e404d76adf824f82987391b57465f8ef902bc", + "local_delta": { + "1": -1 + }, + "owner_debit": { + "1": 1 + }, + "optimistic_complete_delta": {} + }, + { + "register": 293, + "word_sha256": "f6e3cb5a3e44ce8c5cf97c7fffdd42226d2136650c8b6044347766a8f2efa56a", + "local_delta": { + "1": -1 + }, + "owner_debit": { + "1": 1 + }, + "optimistic_complete_delta": {} + }, + { + "register": 298, + "word_sha256": "485ccb290800b2326c6667980facc0d41cc691ef0633fff632f50f710cddddcf", + "local_delta": { + "1": -1 + }, + "owner_debit": { + "1": 1 + }, + "optimistic_complete_delta": {} + }, + { + "register": 309, + "word_sha256": "0d789467dc07d1ac52b734287da410a1e6a0df696620ea66e0fd9125f9e39cf1", + "local_delta": { + "1": -1 + }, + "owner_debit": { + "1": 1 + }, + "optimistic_complete_delta": {} + }, + { + "register": 373, + "word_sha256": "f32e49001079480ab61b6ea732a9f5ff7bd26ed8e8594f5fc710f05606fd5111", + "local_delta": { + "1": -1 + }, + "owner_debit": { + "1": 1 + }, + "optimistic_complete_delta": {} + } + ], + "scalar_saving_vs_3998": { + "forward": 7, + "cleanup": 5 + }, + "new_kappa": false + } + } +} diff --git a/research/staged544-a2-cone-composition/SOURCES.json b/research/staged544-a2-cone-composition/SOURCES.json new file mode 100644 index 0000000000..d2d89bff1a --- /dev/null +++ b/research/staged544-a2-cone-composition/SOURCES.json @@ -0,0 +1,147 @@ +{ + "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-a2-cone-composition/frozen/sep/verify.py", + "origin_repository": "CrocSwap/integer-mult-bounds", + "origin_commit": "f408e09df300b575235f7f77f81948071397e16d", + "origin_path": "research/staged544-separated-a2/verify.py", + "bytes": 15525, + "sha256": "515039e0fc2eab00802a04327066aa2ba7aff7b59ebe156369b60309635a8d43", + "git_blob": "877e57b88394fad56d8131641ce5bda5f1d1e09d" + }, + { + "path": "research/staged544-a2-cone-composition/frozen/sep/independent.py", + "origin_repository": "CrocSwap/integer-mult-bounds", + "origin_commit": "f408e09df300b575235f7f77f81948071397e16d", + "origin_path": "research/staged544-separated-a2/independent.py", + "bytes": 17545, + "sha256": "47bc548f28200f86d28f1f5f8eb466e588bdc01e31f70580280ea6ac72f400a6", + "git_blob": "501c54c11c5fea0337ecd51fa8b0491f19cb7581" + }, + { + "path": "research/staged544-a2-cone-composition/frozen/sep/PROOF.md", + "origin_repository": "CrocSwap/integer-mult-bounds", + "origin_commit": "f408e09df300b575235f7f77f81948071397e16d", + "origin_path": "research/staged544-separated-a2/PROOF.md", + "bytes": 10813, + "sha256": "8da3652a4e30dc79cd41c61b81315f864fe39e748d2420d74300a17d8d5c76ea", + "git_blob": "d39dd7eff0fb2acb99927254fb480f3876655ca4" + }, + { + "path": "research/staged544-a2-cone-composition/frozen/sep/README.md", + "origin_repository": "CrocSwap/integer-mult-bounds", + "origin_commit": "f408e09df300b575235f7f77f81948071397e16d", + "origin_path": "research/staged544-separated-a2/README.md", + "bytes": 5334, + "sha256": "69b1e9054227f707a63c952f213d7894fda0c77ef47a0c30223ee70a1df4eb23", + "git_blob": "4e2874528367344b877f3563492c8d05adf4ddbf" + }, + { + "path": "research/staged544-a2-cone-composition/frozen/cone/verify.py", + "origin_repository": "CrocSwap/integer-mult-bounds", + "origin_commit": "08c8990f7022b94cf63207229465fb8fa0e8fc75", + "origin_path": "research/staged544-scalar-interior-refit/verify.py", + "bytes": 7538, + "sha256": "46cacc806fb31c866d6c0865dc309c1fe6b6cd24cd6b43f134c541ff5e56d7d5", + "git_blob": "54402df9f1113f979cc2c5acd13731d761e16be5" + }, + { + "path": "research/staged544-a2-cone-composition/frozen/cone/tariff.py", + "origin_repository": "CrocSwap/integer-mult-bounds", + "origin_commit": "08c8990f7022b94cf63207229465fb8fa0e8fc75", + "origin_path": "research/staged544-scalar-interior-refit/tariff.py", + "bytes": 3158, + "sha256": "518d4cf986f1cc043959c7dfb4d02620faa5cf23508338f9e5fcde385574ef98", + "git_blob": "06c22dab77193881bc5b8ab9a9f59fc4992e42ca" + }, + { + "path": "research/staged544-a2-cone-composition/frozen/cone/PROOF.md", + "origin_repository": "CrocSwap/integer-mult-bounds", + "origin_commit": "08c8990f7022b94cf63207229465fb8fa0e8fc75", + "origin_path": "research/staged544-scalar-interior-refit/PROOF.md", + "bytes": 7665, + "sha256": "aa2b7516741cfb4600442a5dbc3c7784e94ebf30db85dc7bfc7810ff9d73e790", + "git_blob": "2a5078d8862cb2c9a65c9dc41cf98c9f48803062" + }, + { + "path": "research/staged544-a2-cone-composition/frozen/cone/OWNER-PATTERNS.json", + "origin_repository": "CrocSwap/integer-mult-bounds", + "origin_commit": "08c8990f7022b94cf63207229465fb8fa0e8fc75", + "origin_path": "research/staged544-scalar-interior-refit/OWNER-PATTERNS.json", + "bytes": 1397, + "sha256": "0ffae1b949bab97e7d5a6313c3936be248d75a43ba06593bc45faca4fb686e99", + "git_blob": "858a0225cae00233f0959675393a94660b41c69a" + }, + { + "path": "research/staged544-a2-cone-composition/frozen/cone/frozen/retiming.py", + "origin_repository": "CrocSwap/integer-mult-bounds", + "origin_commit": "08c8990f7022b94cf63207229465fb8fa0e8fc75", + "origin_path": "research/staged544-scalar-interior-refit/frozen/retiming.py", + "bytes": 10391, + "sha256": "591d7278541ac4de9e9b6fc1e17aba23b205ac4b6c81824a28fc08294658ef0d", + "git_blob": "c33d7bbcdf2435056b3a56526e8e43f6513e381b" + }, + { + "path": "research/staged544-a2-cone-composition/frozen/cone/frozen/audit_core.py", + "origin_repository": "CrocSwap/integer-mult-bounds", + "origin_commit": "08c8990f7022b94cf63207229465fb8fa0e8fc75", + "origin_path": "research/staged544-scalar-interior-refit/frozen/audit_core.py", + "bytes": 19364, + "sha256": "888679ca8502cdcb100420fe5382a052529a494bf76cb332928b86e62612b951", + "git_blob": "8b5e1d5f2a106402f036b63028ecef31a4e4c462" + }, + { + "path": "research/staged544-a2-cone-composition/frozen/cone/frozen/SOURCE-CREDITS.md", + "origin_repository": "CrocSwap/integer-mult-bounds", + "origin_commit": "08c8990f7022b94cf63207229465fb8fa0e8fc75", + "origin_path": "research/staged544-scalar-interior-refit/frozen/SOURCE-CREDITS.md", + "bytes": 2882, + "sha256": "d4a13d8b8ed9cdb594f00efb3d1a336e09d934423330f02a1514308a720c278b", + "git_blob": "c054fad87eeaa510865e682ee0c976c4cd728da2" + }, + { + "path": "research/staged544-a2-cone-composition/inputs/WORD-base.json.gz", + "origin_repository": "CrocSwap/integer-mult-bounds", + "origin_commit": "91f81d131252db704f945891da1ea54e29d46b8b", + "origin_path": "research/staged544-terminal-gap-fill/inputs/NEW-base.json.gz", + "bytes": 74428, + "sha256": "08e6c96fbe3dfec96cb8451b3867ef8c1a214109ecd1e5af7fcc28e0f05728d0", + "git_blob": "806784bf99d9d15004d2d227d06268556a0726c8" + }, + { + "path": "research/staged544-a2-cone-composition/inputs/WORD-extra.json.gz", + "origin_repository": "CrocSwap/integer-mult-bounds", + "origin_commit": "91f81d131252db704f945891da1ea54e29d46b8b", + "origin_path": "research/staged544-terminal-gap-fill/inputs/NEW-extra.json.gz", + "bytes": 74425, + "sha256": "d83c2ec9cecc0ad092d34ea4080b28a4fd7199579356b6d5a8fc6cd53ff93299", + "git_blob": "c531be7383ad3ba941600c7ced14e5e10d6d1c67" + }, + { + "path": "research/staged544-a2-cone-composition/frozen/PR3945-NATIVE-LINEAGE-NOTICE", + "origin_repository": "CrocSwap/integer-mult-bounds", + "origin_commit": "91f81d131252db704f945891da1ea54e29d46b8b", + "origin_path": "research/staged544-terminal-gap-fill/native/NATIVE-LINEAGE-NOTICE", + "bytes": 2456, + "sha256": "ee0c73ca35877aad0e0b6adc560a3881cb82276dba4cf2d4fc58cd19e57cc420", + "git_blob": "380e979f0e84e00a22bd890615d87cc4684ad740" + } + ], + "source_export_contract": "Exact package-local exports authenticated before loading source. Only documented pure helpers are invoked from retained sep/cone modules, not their old input-specific CLIs. No foreign pending history dependency. Retained algorithms are credited reuse, not new independent interpreters." +} diff --git a/research/staged544-a2-cone-composition/TASK.json b/research/staged544-a2-cone-composition/TASK.json new file mode 100644 index 0000000000..94e3818146 --- /dev/null +++ b/research/staged544-a2-cone-composition/TASK.json @@ -0,0 +1,78 @@ +{ + "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": "refined", + "actual_scope": "Transfer the fixed PR4019/3998 eight-site composite to both current PR3945 words; prove the unique compatible local frame flags and test the changed graph against PR4016 forced-cone/owner allowance.", + "scope_change_reason": "Explicit donor combination request and PR4019 later-word handoff. No new sites or larger Gaussian census; current-source transfer plus complete owner-aware composition is the contribution.", + "bottleneck_link": "Scalar graph savings do not automatically change the recursive bill. This combined current-source experiment gives unique local flags and the same zero-net forced-cone allowance.", + "budget_minutes": 60, + "stop_rule": "Science freeze11:31UTC and final handoff by11:46UTC2026-10-19. Stop dependent expansion if the complete favorable profile/cone plus owner allowance is nonpositive.", + "outcome": "partial", + "evidence": "Exact16local identities, six full723ordinary/dual/reverse/cleanup replays,16unique complete frame flags,26570terminal cases,2551packing patterns and10literal cone witnesses; credited separate point-set checker.", + "author": "Chris R / Clear1nsight", + "ai_assistance": "Substantial OpenAI Codex assistance in implementation, proof and checks. Source algorithms credited as reuse; no human/formal review claim.", + "selection": { + "method": "Explicit assigned combination and PR4019 later-word handoff", + "entry_open_pr_bodies": 733, + "entry_checked_at_utc": "2026-10-19T10:46:04Z", + "coverage_limit": "All open PR bodies and bounded live handoff/source discussion. Broader Discussion/code coverage partial.", + "predecessors": [ + 4019, + 3998, + 3945, + 4016 + ] + }, + "open_questions": [ + { + "question": "Can a changed graph/native/check boundary yield positive complete owner-aware allowance?", + "why_it_matters": "Fixed eight-site graph has unique local flags and no new cone allowance.", + "first_step": "Specify one materially changed boundary and full favorable invoice before expanding.", + "blocked_by": "No such positive candidate supplied here." + }, + { + "question": "Can the scalar saving be integrated into the physical current producer?", + "why_it_matters": "Exact formal words do not certify concrete native cost or precision.", + "first_step": "Replay frozen transfer independently and audit changed intermediate growth.", + "blocked_by": "Native phases, owner chronology, precision and uniform outer obligations remain inherited." + } + ] +} diff --git a/research/staged544-a2-cone-composition/VERIFY.json b/research/staged544-a2-cone-composition/VERIFY.json new file mode 100644 index 0000000000..03b28d0f9d --- /dev/null +++ b/research/staged544-a2-cone-composition/VERIFY.json @@ -0,0 +1,59 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--provider", + "base" + ], + "timeout_seconds": 240, + "checks": "Current base source, credited and combined full723operator/cleanup checks and fivecone witnesses." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--provider", + "extra" + ], + "timeout_seconds": 240, + "checks": "Current extra source, credited and combined full723operator/cleanup checks and fivecone witnesses." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--tariff" + ], + "timeout_seconds": 180, + "checks": "Exact2551packingpattern dual and incumbent attainment." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/check_composition.py" + ], + "timeout_seconds": 120, + "checks": "Credited separate pointset representation and new timeline uniquecompleteframe proof;14semantic controls." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/check_controls.py" + ], + "timeout_seconds": 180, + "checks": "Production positives, sixsemantic rejections and twoactualoptimizedCLI source/ownerreceipt rejections." + } + ] +} diff --git a/research/staged544-a2-cone-composition/check_composition.py b/research/staged544-a2-cone-composition/check_composition.py new file mode 100644 index 0000000000..7163d74625 --- /dev/null +++ b/research/staged544-a2-cone-composition/check_composition.py @@ -0,0 +1,84 @@ +#!/usr/bin/env python3 +"""Second representation for current-word composition and singleton frames. +Uses ToikY PR4019's separately implemented point-set/coordinate checker, +unchanged and credited. No primary verifier, trace or dirty auditor is imported. +Chris R / Clear1nsight, substantial OpenAI Codex assistance; Apache-2.0. +""" +from pathlib import Path +from collections import Counter +import gzip,hashlib,json,types +ROOT=Path(__file__).resolve().parent +PINS={'base':'08e6c96fbe3dfec96cb8451b3867ef8c1a214109ecd1e5af7fcc28e0f05728d0','extra':'d83c2ec9cecc0ad092d34ea4080b28a4fd7199579356b6d5a8fc6cd53ff93299'} +CHECKER_SHA='47bc548f28200f86d28f1f5f8eb466e588bdc01e31f70580280ea6ac72f400a6' +PROFILE={'1':2482,'2':712,'3':218,'4':109,'5':20,'8':8} +WIDTHS={'5':28,'6':18,'7':53,'8':96,'9':213} +def need(ok,msg): + if not ok:raise ValueError(msg) +def load(): + path=ROOT/'frozen/sep/independent.py';raw=path.read_bytes();need(hashlib.sha256(raw).hexdigest()==CHECKER_SHA,'separate checker source') + m=types.ModuleType('credited_point_set_checker');m.__file__=str(path);exec(compile(raw,str(path),'exec'),m.__dict__);return m + +def timelines(w,I): + live=sorted(set(range(704))-set(w['removed']));zero=frozenset((0,));full=frozenset(range(512));current={};finish={};seq={r:[] for r in live} + for r in live: + current[r]=I.span((w['ports'][r],)) if r<112 else zero + finish[r]=frozenset(x for x in range(512) if (x&w['ports'][r-112]).bit_count()%2==0) if 112<=r<224 else full + for r,b in w['start_extra'].items():current[int(r)]=I.span(tuple(b)) + for r,b in w['helper_final'].items():finish[int(r)]=I.span(tuple(b)) + def event(r,address,frame): + seq[r].append((address,current[r],frame));current[r]=frame + def scalar(section,i,g): + for r in I.support(g):event(r,(section,i),I.span(tuple(g[-1]))) + for i,g in enumerate(w['A']): + if g[0]=='warp': + event(g[1],('A-native-in',i),I.span(tuple(g[3])));event(g[1],('A-native-out',i),I.span(tuple(g[4]))) + else:scalar('A',i,g) + levels={112+int(r):I.span(tuple(b)) for r,b in w['target_levels'].items()} + for r in range(112,224):event(r,('target',r),levels.get(r,zero)) + for r,b in zip(w['centers'],w['center_frames']):event(r,('centre',r),I.span(tuple(b))) + warps={} + for j,warp in enumerate(w['warps']):warps.setdefault(warp[0],[]).append((j,warp)) + for i in range(len(w['B'])+1): + for j,g in warps.get(i,[]): + event(g[1],('B-native-in',j),I.span(tuple(g[3])));event(g[1],('B-native-out',j),I.span(tuple(g[4]))) + if i> 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-a2-cone-composition/frozen/cone/frozen/retiming.py b/research/staged544-a2-cone-composition/frozen/cone/frozen/retiming.py new file mode 100644 index 0000000000..c33d7bbcdf --- /dev/null +++ b/research/staged544-a2-cone-composition/frozen/cone/frozen/retiming.py @@ -0,0 +1,269 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Exact, fixed-neighbour single-ADD retiming relaxation. + +Chris R / Clear1nsight, with substantial OpenAI assistance. The BORROW-WORD +frame contract and scalar-retiming mechanism are credited in README.md. +This module does not import the retained auditor or a numerical optimiser. +""" +from bisect import bisect_left +from collections import Counter +from copy import deepcopy +from fractions import Fraction +from functools import lru_cache + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +@lru_cache(maxsize=None) +def span(vectors): + points = {0} + for v in vectors: + need(type(v) is int and 0 <= v < 512, 'invalid frame vector') + points |= {x ^ v for x in tuple(points)} + return sum(1 << x for x in points) + + +@lru_cache(maxsize=None) +def basis(mask): + answer = [] + have = 1 + for v in range(1, 512): + if (mask >> v) & 1 and not (have >> v) & 1: + answer.append(v) + have = span(tuple(answer)) + need(have == mask, 'not a binary subspace') + return tuple(answer) + + +@lru_cache(maxsize=None) +def join(a, b): + return span(basis(a) + basis(b)) + + +@lru_cache(maxsize=None) +def rank(mask): + n = mask.bit_count() + need(n > 0 and n & (n - 1) == 0, 'invalid subspace cardinality') + return n.bit_length() - 1 + + +def contained(a, b): + return not a & ~b + + +def touched(gate): + return gate[1:3] if gate[0] == 'add' else gate[1:2] + + +def tracing(word): + """Own chronological trace; centre descent is NOT persistent state. + + A check node is a fixed boundary, not a charged instruction. The census + relaxes it to a virtual climb. Every legal witness has zero such charge. + """ + full = (1 << 512) - 1 + live = set(range(704)) - set(word['removed']) + start, end = {}, {} + for r in live: + if r < 112: + start[r], end[r] = span((word['ports'][r],)), full + elif r < 224: + p = word['ports'][r - 112] + start[r] = 1 + end[r] = sum(1 << x for x in range(512) if (x & p).bit_count() % 2 == 0) + else: + start[r], end[r] = 1, full + for r, fr in word['start_extra'].items(): + start[int(r)] = span(tuple(fr)) + for r, fr in word['helper_final'].items(): + end[int(r)] = span(tuple(fr)) + current = dict(start) + nodes = {r: [] for r in live} + where = {} + bill = Counter() + + def event(r, frame, address, kind='climb'): + before = current[r] + if kind != 'map': + need(contained(before, frame), 'source frame containment') + d = rank(frame) - rank(before) + if kind == 'check': + need(d == 0, 'source fixed boundary') + elif d: + bill[d] += 1 + if kind == 'climb': + where[(address, r)] = len(nodes[r]) + nodes[r].append((address, kind, before, frame)) + current[r] = frame + + for i, gate in enumerate(word['A']): + if gate[0] == 'warp': + event(gate[1], span(tuple(gate[3])), ('check-A', i), 'check') + event(gate[1], span(tuple(gate[4])), ('map-A', i), 'map') + else: + for r in touched(gate): + event(r, span(tuple(gate[-1])), ('A', i)) + levels = {112 + int(r): span(tuple(fr)) for r, fr in word['target_levels'].items()} + for r in range(112, 224): + event(r, levels.get(r, 1), ('target-cut', r), 'check') + for r, fr in zip(word['centers'], word['center_frames']): + u = span(tuple(fr)) + event(r, u, ('centre-cut', r), 'check') + served = {levels.get(g[1], 1) for g in word['cut'] if g[2] == r} + for v in sorted(served, key=lambda x: -rank(x)): + need(contained(v, u), 'centre nesting') + if rank(u) > rank(v): + bill[rank(u) - rank(v)] += 1 + u = v + # The main forward register remains at its declared centre entry. + warps = {} + for j, rec in enumerate(word['warps']): + warps.setdefault(rec[0], []).append((j, rec)) + for i in range(len(word['B']) + 1): + for j, rec in warps.get(i, []): + event(rec[1], span(tuple(rec[3])), ('check-B', j), 'check') + event(rec[1], span(tuple(rec[4])), ('map-B', j), 'map') + if i < len(word['B']): + gate = word['B'][i] + for r in touched(gate): + event(r, span(tuple(gate[-1])), ('B', i)) + for i, gate in enumerate(word['restore']): + for r in touched(gate): + event(r, span(tuple(gate[-1])), ('restore', i)) + for r in live: + event(r, end[r], ('end',)) + return nodes, where, dict(sorted(bill.items())) + + +def crosses(g, h): + """Sufficient exact scalar normal form, not all algebraic commutations.""" + if h[0] == 'add': + return g[1] != h[2] and h[1] != g[2] + return h[0] == 'scale' and h[2] != 0 + + +def segments(word, section): + if section == 'A': + cuts = [word['prelude_events'], len(word['A'])] + elif section == 'B': + cuts = sorted({0, len(word['B'])} | {rec[0] for rec in word['warps']}) + else: + cuts = [0, len(word[section])] + return list(zip(cuts, cuts[1:])) + + +def caps(delta): + return [sum(n * min(r, k) for r, n in enumerate(delta)) for k in range(1, 10)] + + +def all_power_nonnegative(delta): + """Sufficient exact certificate using decreasing positive curvatures.""" + values = caps(delta) + prefix = 0 + for value in values[:-1]: + prefix += value + if prefix < 0: + return False + return values[-1] == 0 + + +def census(word): + nodes, where, bill = tracing(word) + deltas = Counter() + counts = {} + for section in ('A', 'B', 'restore'): + gates = word[section] + count = 0 + for lo, hi in segments(word, section): + occurrences = {} + for i in range(lo, hi): + need(gates[i][0] in ('add', 'scale'), 'unexpected scalar segment') + for r in touched(gates[i]): + occurrences.setdefault(r, []).append(i) + for i in range(lo, hi): + g = gates[i] + if g[0] != 'add': + continue + lower = i + while lower > lo and crosses(g, gates[lower - 1]): + lower -= 1 + upper = i + 1 + while upper < hi and crosses(g, gates[upper]): + upper += 1 + removal = [0] * 10 + reduced, entries, exits = {}, {}, {} + for r in touched(g): + seq = nodes[r] + pos = where[((section, i), r)] + _, _, p, u = seq[pos] + need(pos + 1 < len(seq) and seq[pos + 1][1] != 'map', 'missing successor') + q = seq[pos + 1][3] + removal[rank(u) - rank(p)] -= 1 + removal[rank(q) - rank(u)] -= 1 + removal[rank(q) - rank(p)] += 1 + indices = occurrences[r] + reduced[r] = [x for x in indices if x != i] + entries[r] = seq[where[((section, indices[0]), r)]][2] + last = where[((section, indices[-1]), r)] + need(seq[last + 1][1] != 'map', 'missing exit check') + exits[r] = seq[last + 1][3] + for cut in range(lower, upper + 1): + if cut == i + 1: # Same placement as cut i, counted once. + continue + boundaries = [] + for r in touched(g): + indices = reduced[r] + j = bisect_left(indices, cut) + p = span(tuple(gates[indices[j - 1]][-1])) if j else entries[r] + q = span(tuple(gates[indices[j]][-1])) if j < len(indices) else exits[r] + boundaries.append((p, q)) + lower_frame = join(boundaries[0][0], boundaries[1][0]) + upper_frame = boundaries[0][1] & boundaries[1][1] + if not contained(lower_frame, upper_frame): + continue + dims = [(rank(p), rank(q)) for p, q in boundaries] + for d in range(rank(lower_frame), rank(upper_frame) + 1): + delta = removal.copy() + for p, q in dims: + delta[q - p] -= 1 + delta[d - p] += 1 + delta[q - d] += 1 + delta[0] = 0 + need(sum(r * n for r, n in enumerate(delta)) == 0, 'rank mass drift') + deltas[tuple(delta)] += 1 + count += 1 + counts[section] = count + return {'per_section': counts, 'candidates': sum(counts.values()), + 'source_profile': bill, + 'deltas': [{'delta': {r: n for r, n in enumerate(d) if n}, 'count': n, + 'caps': caps(d), 'certificate': all_power_nonnegative(d)} + for d, n in sorted(deltas.items())]} + + +def apply_move(word, section, index, cut, frame): + """Apply one exact scalar retiming. Caller must rederive cleanup and audit.""" + need(section in ('A', 'B', 'restore'), 'unknown section') + gates = word[section] + need(type(index) is int and 0 <= index < len(gates), 'bad source index') + need(type(cut) is int and 0 <= cut <= len(gates), 'bad insertion cut') + need(any(lo <= index < hi and lo <= cut <= hi for lo, hi in segments(word, section)), + 'crosses prelude or native warp boundary') + g = deepcopy(gates[index]) + need(g[0] == 'add', 'only ADD moves are covered') + crossed = gates[index + 1:cut] if cut > index else gates[cut:index] + need(all(crosses(g, h) for h in crossed), 'noncommuting scalar barrier') + coefficient = Fraction(g[3], g[4]) + for h in crossed: + if h[0] == 'scale' and h[1] in touched(g): + power = (1 if h[1] == g[1] else -1) * (1 if cut > index else -1) + coefficient *= Fraction(h[2], h[3]) ** power + g[3:5] = [coefficient.numerator, coefficient.denominator] + g[-1] = list(basis(span(tuple(frame)))) + result = deepcopy(word) + result[section].pop(index) + result[section].insert(cut - (cut > index), g) + # Segment length and all warp cuts are unchanged. No warp is crossed. + return result diff --git a/research/staged544-a2-cone-composition/frozen/cone/tariff.py b/research/staged544-a2-cone-composition/frozen/cone/tariff.py new file mode 100644 index 0000000000..06c22dab77 --- /dev/null +++ b/research/staged544-a2-cone-composition/frozen/cone/tariff.py @@ -0,0 +1,71 @@ +"""Exact tariff arithmetic adapted from PR3988, Chris R with OpenAI Codex. +Dual credited to PR3815/3862/3890. Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as Q +from functools import lru_cache +from pathlib import Path +import argparse, gzip, hashlib, importlib.util, json, math +ROOT=Path(__file__).resolve().parent +K=Q(1730663236534549309146,10**24) + +def need(ok,why): + if not ok: raise ValueError(why) +def read(p): + b=p.read_bytes();return json.loads(gzip.decompress(b) if p.suffix=='.gz' else b) +def sha(p):return hashlib.sha256(p.read_bytes()).hexdigest() +def add(*terms): + out=Counter() + for factor,v in terms: + for r,c in v.items():out[r]+=factor*c + return {r:c for r,c in out.items() if c and r} +def h(r):return {r:Q(1)} if r else {} +def log_ratio(x): + z=(x-1)/(x+1);n=50 + value=2*sum((z**(2*j+1)/Q(2*j+1) for j in range(n)),Q(0)) + tail=2*z**(2*n+1)/(Q(2*n+1)*(1-z*z)) + return value,value+tail +@lru_cache(None) +def power(r): + if r==0:return Q(0),Q(0) + j=r.bit_length()-1;l2,u2=log_ratio(Q(2));lr,ur=log_ratio(Q(r,2**j)) + a,b=K*(j*l2+lr),K*(j*u2+ur) + need(0<=a<=b<1,'exponential range') + def exp_minus(x,n):return sum(((-x)**i/Q(math.factorial(i)) for i in range(n+1)),Q(0)) + return r*exp_minus(b,19),r*exp_minus(a,20) +def interval(v): + lo=hi=Q(0) + for r,c in v.items(): + a,b=power(r);lo+=c*(a if c>=0 else b);hi+=c*(b if c>=0 else a) + return lo,hi +def brief(ab): + scale=10**24;lo,hi=ab + return {'lower_numerator':lo.numerator*scale//lo.denominator,'upper_numerator':-((-hi.numerator*scale)//hi.denominator),'denominator':scale} +def patterns(): + for cap in (8,16,32,48): + def rec(i,ns,left): + if i==5: + yield cap,tuple(ns),left;return + for n in range(left//(i+5)+1):yield from rec(i+1,ns+[n],left-n*(i+5)) + yield from rec(0,[],cap) +def dual(): + q={48:Q(1,20),3:Q(-1,20),5:Q(-1,4)} + pi={w:add((-1,h(5)),(-(w-5),q)) for w in range(5,10)} + mu={8:add((-1,pi[8])),16:add((-2,pi[8])),32:add((-4,pi[8])),48:h(48)} + return q,pi,mu +def reduced(cap,ns,left,pi,mu):return add((1,h(left)),(-1,mu[cap]),*((-n,pi[w]) for w,n in zip(range(5,10),ns))) +def dual_check(): + q,pi,mu=dual();tight=[];strict=[] + for cap,ns,left in patterns(): + v=reduced(cap,ns,left,pi,mu) + if not v:tight.append([cap,list(ns),left]) + else: + ab=interval(v);need(ab[0]>0,'dual infeasibility');strict.append(ab) + gap=interval(add((1,h(9)),(-1,h(8)),(-1,q)));need(gap[0]>Q(6,1000),'terminal budget gap') + # Independently test every discrete marginal, not only the analytic minimum. + for r in range(1,10):need(interval(add((1,h(r)),(-1,h(r-1)),(-1,q)))[0]>0,'marginal budget') + return {'patterns':len(tight)+len(strict),'tight_patterns':tight,'strict_patterns':len(strict), + 'minimum_strict_reduced_cost':brief((min(x[0] for x in strict),min(x[1] for x in strict))), + 'idle_credit_per_dimension':brief(interval(q)), + 'minimum_terminal_charge_per_dimension':brief(interval(add((1,h(9)),(-1,h(8))))), + 'mandatory_interior_saving_per_dimension':brief(gap)} diff --git a/research/staged544-a2-cone-composition/frozen/cone/verify.py b/research/staged544-a2-cone-composition/frozen/cone/verify.py new file mode 100644 index 0000000000..54402df9f1 --- /dev/null +++ b/research/staged544-a2-cone-composition/frozen/cone/verify.py @@ -0,0 +1,128 @@ +"""Bounded scalar-cone refits, Chris R with substantial OpenAI Codex, Apache-2.0. +Trace/bitset helpers are credited frozen code; this is not an independent audit. +""" +from pathlib import Path +from collections import Counter +import sys,json,gzip,copy,hashlib,argparse +ROOT=Path(__file__).resolve().parent +sys.path.insert(0,str(ROOT/'frozen')) +import retiming as t +import audit_core as audit +import tariff as v +need=v.need + +def read(p):return json.loads(gzip.decompress(p.read_bytes()) if p.suffix=='.gz' else p.read_bytes()) +def canonical(w):return hashlib.sha256(json.dumps(w,sort_keys=True,separators=(',',':')).encode()).hexdigest() +def hyperplanes(mask): + bs=t.basis(mask) + for linear in range(1,1<>j&1 else 0) for j in range(len(bs)) if j!=pivot)) + +def prepare(w): + nodes,where,bill=t.tracing(w);gates={};preds={};fixed=set();edges=[] + for r,seq in nodes.items(): + before=None + for addr,kind,p,u in seq: + scalar=addr[0] in ('A','B','restore') and kind=='climb' + key=addr if scalar else ('terminal',r) if addr==('end',) else None + if scalar:gates[key]=u;preds.setdefault(key,[]).append((before,p)) + if kind=='check' and before is not None:fixed.add(before) + if kind=='climb':edges.append((before,p,key,u)) + before=key + return nodes,gates,preds,fixed,edges,bill + +def cone(gates,preds,fixed,targetkey,target): + changes={targetkey:target};queue=[targetkey] + while queue: + key=queue.pop();cap=changes[key] + if key in fixed:return None,'fixed-check' + for pred,mask in preds[key]: + pmask=changes.get(pred,mask) + if t.contained(pmask,cap):continue + if pred is None:return None,'fixed-entrance/native' + changes[pred]=pmask∩queue.append(pred) + return changes,None + +def census(w): + nodes,gates,preds,fixed,edges,bill=prepare(w);out=[];reject=Counter();total=0 + need(bill==audit.frame_bill(w)[0],'trace versus source auditor') + for sr,fr in sorted(w['helper_final'].items(),key=lambda x:int(x[0])): + r=int(sr);seq=nodes[r];last=seq[-2][0];old=t.span(tuple(fr));width=t.rank(old)-t.rank(seq[0][2]) + need(last in gates,'protected last event is not scalar') + seen=set() + for new in hyperplanes(old): + need(new not in seen,'duplicate hyperplane');seen.add(new);total+=1 + need(t.rank(new)==t.rank(old)-1 and t.contained(new,old),'invalid hyperplane') + if not t.contained(seq[0][2],new):reject['start-terminal']+=1;continue + if t.contained(gates[last],new):reject['credited-direct-refund']+=1;continue + changes,reason=cone(gates,preds,fixed,last,gates[last]&new) + if changes is None:reject[reason]+=1;continue + changes[('terminal',r)]=new;delta=Counter() + for pred,p,key,u in edges: + if pred not in changes and key not in changes:continue + a=changes.get(pred,p);b=changes.get(key,u) + need(t.contained(a,b),'propagation lost containment') + delta[t.rank(u)-t.rank(p)]-=1;delta[t.rank(b)-t.rank(a)]+=1 + delta={str(r):n for r,n in delta.items() if r and n} + need(width==5 and delta=={'1':-1},'unpriced feasible cone') + edits=[{'section':k[0],'index':k[1],'old':list(w[k[0]][k[1]][-1]),'new':list(t.basis(m))} for k,m in sorted(changes.items()) if k[0]!='terminal' and gates[k]!=m] + out.append({'register':r,'old_terminal':fr,'new_terminal':list(t.basis(new)),'edits':edits,'width_before':5,'width_after':4,'local_delta':delta,'owner_debit':{'1':1},'optimistic_complete_delta':{}}) + need(len(seen)==(1<0,'tariff dual infeasible');strict+=1 + else:tight+=1 + need((tight,strict)==(12,2539),'tariff domain') + need(not v.add((1,pi[4]),(-1,pi[5]),(-1,v.h(1))),'exact refund tariff') + # Frozen aggregate incumbent is dual-tight. Full owner chronology is inherited. + receipt=read(ROOT/'OWNER-PATTERNS.json');count=0;demand=Counter();bins=Counter() + for cap,ns,left,n in receipt['patterns']: + need(sum(w*c for w,c in zip(range(5,10),ns))+left==cap,'incumbent capacity') + need(not v.reduced(cap,ns,left,pi,mu),'incumbent attainment');count+=n;bins[cap]+=n + for width,c in zip(range(5,10),ns):demand[width]+=n*c + need(count==725760 and bins=={8:241920,16:161280,32:161280,48:161280},'incumbent bins') + need(demand=={5:90720,6:58320,7:171720,8:311040,9:690120},'incumbent demand') + return {'patterns':tight+strict,'tight':tight,'strict':strict,'refund_debit':'H1 exactly','incumbent_bins':count} + +def main(): + p=argparse.ArgumentParser();p.add_argument('--quick',action='store_true');p.add_argument('--record',action='store_true');a=p.parse_args() + for name,digest in read(ROOT/'FROZEN.json').items():need(hashlib.sha256((ROOT/name).read_bytes()).hexdigest()==digest,'frozen source hash') + result={'tariff':tariff_check(),'providers':{}};witnesses=[] + for tag in ('base','extra'): + w=read(ROOT/f'frozen/WORD-{tag}.json.gz');result['providers'][tag]=census(w) + for row in result['providers'][tag]['candidates']: + x=apply(w,row) + if not a.quick:semantics(x) + witnesses.append({'provider':tag,'register':row['register'],'canonical_sha256':canonical(x)}) + result['witnesses']=witnesses + if a.record:(ROOT/'RESULT.json').write_text(json.dumps(result,indent=2)+'\n') + else:need(result==read(ROOT/'RESULT.json'),'result mismatch') + print(json.dumps({'status':'PASS_SCALAR_CONE_BUDGET','hyperplanes_each':13285,'literal_witnesses':len(witnesses),'exact_dirty_replayed':not a.quick,'complete_gain':0},sort_keys=True)) +if __name__=='__main__':main() diff --git a/research/staged544-a2-cone-composition/frozen/sep/PROOF.md b/research/staged544-a2-cone-composition/frozen/sep/PROOF.md new file mode 100644 index 0000000000..d39dd7eff0 --- /dev/null +++ b/research/staged544-a2-cone-composition/frozen/sep/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-a2-cone-composition/frozen/sep/README.md b/research/staged544-a2-cone-composition/frozen/sep/README.md new file mode 100644 index 0000000000..4e28745283 --- /dev/null +++ b/research/staged544-a2-cone-composition/frozen/sep/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-a2-cone-composition/frozen/sep/independent.py b/research/staged544-a2-cone-composition/frozen/sep/independent.py new file mode 100644 index 0000000000..501c54c11c --- /dev/null +++ b/research/staged544-a2-cone-composition/frozen/sep/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-a2-cone-composition/frozen/sep/verify.py b/research/staged544-a2-cone-composition/frozen/sep/verify.py new file mode 100644 index 0000000000..877e57b883 --- /dev/null +++ b/research/staged544-a2-cone-composition/frozen/sep/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]=54,'cone remap domain');e['index']-=2 + need(expected==new,'cone candidates not exact remapping') + if full: + for name,x in (('source',w),('credited_3998',known),('combined',changed)): + receipts[name]['semantics']=sep.semantics(core,x);print('CHECKED',tag,name,'full723',flush=True) + need(len({r['semantics']['ordinary_matrix_sha256'] for r in receipts.values()})==1 and len({r['semantics']['dual_matrix_sha256'] for r in receipts.values()})==1,'full operator equality') + witnesses=[] + for row in new_cone['candidates']: + x=cone.apply(changed,row) + if full:cone.semantics(x) + witnesses.append({'register':row['register'],'word_sha256':digest(x),'local_delta':row['local_delta'],'owner_debit':row['owner_debit'],'optimistic_complete_delta':row['optimistic_complete_delta']}) + return {'provider':tag,'sites':records,'words':receipts,'fixed_boundary_frames':frames,'cone':new_cone,'cone_witnesses':witnesses,'scalar_saving_vs_3998':{'forward':7,'cleanup':5},'new_kappa':False} + +def audit(tag,full=True): + actual=provider(tag,full);expected=read(ROOT/'RESULT.json')['providers'][tag] + if not full: + expected=deepcopy(expected) + for r in expected['words'].values():r.pop('semantics',None) + need(canonical(actual)==canonical(expected),'result mismatch');return actual + +def main(): + p=argparse.ArgumentParser();p.add_argument('--provider',choices=('base','extra'),default='base');p.add_argument('--quick',action='store_true');p.add_argument('--record',action='store_true');p.add_argument('--tariff',action='store_true');a=p.parse_args() + if a.record: + t,c,v,k,s=load_engines();result={'schema_version':1,'tariff':k.tariff_check(),'providers':{tag:provider(tag,True) for tag in ('base','extra')}} + (ROOT/'RESULT.json').write_text(json.dumps(result,indent=2)+'\n');print('WROTE combined result') + elif a.tariff: + t,c,v,k,s=load_engines();need(k.tariff_check()==read(ROOT/'RESULT.json')['tariff'],'tariff mismatch');print('PASS_OWNER_DUAL_2551_PATTERNS exact_net_zero') + else: + audit(a.provider,not a.quick);print('PASS_A2_CONE_COMPOSITION',a.provider,'full='+str(not a.quick),'no_new_kappa') +if __name__=='__main__': + try:main() + except Exception as e:print('FAIL_A2_CONE_COMPOSITION '+str(e),file=sys.stderr);raise SystemExit(1)