diff --git a/research/staged544-scalar-interior-refit/FROZEN.json b/research/staged544-scalar-interior-refit/FROZEN.json new file mode 100644 index 0000000000..35903cff78 --- /dev/null +++ b/research/staged544-scalar-interior-refit/FROZEN.json @@ -0,0 +1,8 @@ +{ + "frozen/SOURCE-CREDITS.md": "d4a13d8b8ed9cdb594f00efb3d1a336e09d934423330f02a1514308a720c278b", + "frozen/WORD-base.json.gz": "08e6c96fbe3dfec96cb8451b3867ef8c1a214109ecd1e5af7fcc28e0f05728d0", + "frozen/WORD-extra.json.gz": "d83c2ec9cecc0ad092d34ea4080b28a4fd7199579356b6d5a8fc6cd53ff93299", + "frozen/audit_core.py": "888679ca8502cdcb100420fe5382a052529a494bf76cb332928b86e62612b951", + "frozen/retiming.py": "591d7278541ac4de9e9b6fc1e17aba23b205ac4b6c81824a28fc08294658ef0d", + "OWNER-PATTERNS.json": "0ffae1b949bab97e7d5a6313c3936be248d75a43ba06593bc45faca4fb686e99" +} diff --git a/research/staged544-scalar-interior-refit/LEDGER.json b/research/staged544-scalar-interior-refit/LEDGER.json new file mode 100644 index 0000000000..798fd276ef --- /dev/null +++ b/research/staged544-scalar-interior-refit/LEDGER.json @@ -0,0 +1,77 @@ +{ + "status": "COMPLETE_OPTIMISTIC_BUDGET_REJECTS_DOMAIN", + "source_head": "91f81d131252db704f945891da1ea54e29d46b8b", + "tariff_kappa_rational": { + "numerator": 1730663236534549309146, + "denominator": 1000000000000000000000000 + }, + "selected_kappa_unchanged": "0.001672660197076918", + "per_provider": { + "source_children": 3549, + "source_profile": { + "1": 2482, + "2": 712, + "3": 218, + "4": 109, + "5": 20, + "8": 8 + }, + "after_children": 3548, + "local_delta": { + "1": -1 + }, + "rank_mass_delta": -1, + "width_change": { + "5": -1, + "4": 1 + }, + "dirty_buffers": 91, + "helper_roles": 408, + "native_frames_graph_coefficients": "exactly unchanged", + "cleanup": "regenerated and byte-equivalent" + }, + "full_3240_calls": { + "local_delta": { + "1": -3240 + }, + "owner_idle_lower_bound_delta": { + "1": 3240 + }, + "complete_optimistic_delta": {}, + "new_chronological_placement": false, + "kappa_improvement": null + }, + "proved": [ + "Complete hyperplane partition", + "Forced-cone feasibility/rejection", + "Ten literal dirty/dual/cleanup witnesses", + "2551pattern exact dual and aggregate attainment", + "No favorable budget in priced domain" + ], + "inherited": [ + "Credited trace and dirty interpreter correctness", + "PR3969/3988 owner chronology and aggregate binding", + "Native phase implementation and supplier status" + ], + "unknown_or_outside": [ + "Optional interior edits beyond forced cone", + "Terminal rotations outside incumbent", + "Simultaneous terminal changes", + "Changed native/check/graph", + "New actual owner realization", + "Physical conversion/precision/stock/tape/uniformity/outer/analytic/BIT admission" + ], + "unknown_costs_are_not_zero": true, + "scope_limit": "Greatest forced-intersection assignment for one terminal hyperplane only; not global optimum.", + "baseline_complete_profile": { + "1": 8041680, + "2": 2306880, + "3": 729648, + "4": 353160, + "5": 69120, + "8": 25920, + "48": 137952 + }, + "fixed_native_and_free_instructions": "Literal scalar coefficients/graph, native maps and interface frames are unchanged; no scalar-operation-count improvement is claimed.", + "coefficient_bound": "Inherited finite 4-bit source bound; uniform precision/tape coefficient not derived." +} diff --git a/research/staged544-scalar-interior-refit/OWNER-PATTERNS.json b/research/staged544-scalar-interior-refit/OWNER-PATTERNS.json new file mode 100644 index 0000000000..858a0225ca --- /dev/null +++ b/research/staged544-scalar-interior-refit/OWNER-PATTERNS.json @@ -0,0 +1,137 @@ +{ + "derivation": "All1321920 literal FILL rows; run --source-root to reconstruct. All unoccupied bins counted.", + "patterns": [ + [ + 8, + [ + 0, + 0, + 0, + 1, + 0 + ], + 0, + 241920 + ], + [ + 16, + [ + 0, + 0, + 0, + 2, + 0 + ], + 0, + 2233 + ], + [ + 16, + [ + 0, + 0, + 1, + 0, + 1 + ], + 0, + 159047 + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 3 + ], + 5, + 4320 + ], + [ + 32, + [ + 0, + 0, + 0, + 4, + 0 + ], + 0, + 224 + ], + [ + 32, + [ + 0, + 0, + 1, + 2, + 1 + ], + 0, + 2719 + ], + [ + 32, + [ + 0, + 0, + 2, + 0, + 2 + ], + 0, + 4977 + ], + [ + 32, + [ + 0, + 1, + 0, + 1, + 2 + ], + 0, + 58320 + ], + [ + 32, + [ + 1, + 0, + 0, + 0, + 3 + ], + 0, + 90720 + ], + [ + 48, + [ + 0, + 0, + 0, + 0, + 0 + ], + 48, + 137952 + ], + [ + 48, + [ + 0, + 0, + 0, + 0, + 5 + ], + 3, + 23328 + ] + ] +} diff --git a/research/staged544-scalar-interior-refit/PROOF.md b/research/staged544-scalar-interior-refit/PROOF.md new file mode 100644 index 0000000000..2a5078d886 --- /dev/null +++ b/research/staged544-scalar-interior-refit/PROOF.md @@ -0,0 +1,140 @@ +# Scalar-cone terminal restrictions at fixed native interfaces + +Chris R / Clear1nsight, with substantial OpenAI Codex assistance. Apache-2.0. + +## Scope and changed contract + +The source is both PR3945 provider words at immutable head +`91f81d131252db704f945891da1ea54e29d46b8b`. The previous PR3988 +obstruction fixes all interior frames. Here interior **scalar** frames in A, B and restore may +shrink, together with one protected terminal. Precondition, compensation and +cut operations stay fixed. The literal graph, coefficients, +entrance frames, target and centre checks, native entry/exit frames, removed +registers and 91 protected dirty-buffer identities remain fixed. + +The finite domain chooses every codimension-one subspace of each protected +terminal and propagates its restriction backward through scalar dependencies. +Each scalar frame is constrained to be a subspace of its original frame. +Only the greatest frames forced by this propagation are priced; other optional +shrinks, rotations outside the incumbent frames, simultaneous terminal changes, +changed graph/native/check boundaries and global scalar optimization are outside +this result. No κ improvement is claimed. + +This is one changed-boundary experiment, followed by its permitted mechanism +pivot. The smallest one-gate test already yielded only five exact ties. Allowing +the entire forced scalar dependency cone did not add a feasible candidate. + +## Exact finite domain + +Represent a binary subspace of F2^9 by its 512-bit point-set mask. Intersection +is bitwise AND; containment is exact. For a d-dimensional terminal with ordered +basis b_0,...,b_(d-1), every nonzero linear functional has one kernel hyperplane. +Over F2 there is no nontrivial scalar equivalence, so the 2^d−1 nonzero functionals +enumerate every hyperplane once. For a functional with pivot p, its kernel basis +consists of b_j + ell_j b_p for j≠p. The checker verifies cardinality, uniqueness, +containment and dimension for every generated subspace. + +The chronological trace represents scalar ADD by one common frame variable +shared by its two registers and SCALE by one variable. Native maps introduce +fixed exit anchors. Entrance anchors are fixed. Required target/centre/native +entry checks force the immediately preceding scalar frame to retain its original +value: that value already equals the check boundary in the source. The trace is +adapted from the retained retiming implementation, and its source histogram is +compared with the retained frame auditor; this is **not** claimed as an independent +implementation of those predecessors. + +For a chosen terminal hyperplane T, restrict its last scalar frame U to U∩T. +If a scalar predecessor P is not contained in a restricted successor C, restrict +P to P∩C and revisit its own predecessors. Reaching an immutable anchor outside +C rejects the candidate. Restricting a frame required by a fixed check rejects +it. Otherwise the process terminates: every strict restriction lowers a finite +frame dimension, and all constraints are intersections. + +The result is the greatest feasible assignment below the original frame caps. +Every feasible assignment lies below each intermediate cap by induction, so +rejection at a fixed anchor or check is conclusive for this domain. Success +satisfies every incoming containment constraint; unchanged downstream frames +still contain the restricted predecessors. This establishes feasibility, not +moment optimality among additional optional interior restrictions. + +## Exact census on both providers + +Each provider has 13,285 terminal hyperplanes, partitioned as follows: + +| Outcome | Count | +| --- | ---: | +| Terminal would not contain its fixed entrance | 2,688 | +| Forced cone reaches incompatible fixed entrance/native exit | 10,023 | +| Forced cone would alter a scalar frame fixed by a check | 552 | +| Already fits final scalar frame: credited PR3988 direct refund | 17 | +| Feasible changed scalar cone | 5 | + +The five survivors are identical for the two providers: + +| Helper | B-section index (zero based) | Interior operation | +| --- | ---: | --- | +| 282 | 535 | SCALE −1 | +| 293 | 554 | SCALE −1 | +| 298 | 559 | SCALE −1 | +| 309 | 580 | SCALE −1 | +| 373 | 682 | SCALE −1 | + +Each cone changes exactly this scalar frame and its matching terminal. The exact +new bases and guarded old frames appear in RESULT.json. Each deletes one paid +H1, changes one width5 helper to width4, and preserves all other paid ranks. +The source profile is {1:2482,2:712,3:218,4:109,5:20,8:8}; the new profile lowers +only the first multiplicity to2481. The width inventory changes from +{5:28,6:18,7:53,8:96,9:213} to {4:1,5:27,6:18,7:53,8:96,9:213}. + +## Complete optimistic owner budget + +Use the exact PR3945 endpoint k=1730663236534549309146/10^24 and h(r)=r^(1−k). +Its source convention r(73/r)^k has the same positive common factor73^k. +The credited PR3815/3862/3890 packing dual, rechecked at this endpoint in PR3988, +has q=(h(48)−h(3)−5h(5))/20, pi_w=−h(5)−(w−5)q for5≤w≤9, +and pi_4=1−h(5). Bin prices are mu8=−pi8, mu16=−2pi8, +mu32=−4pi8 and mu48=h48. + +For every capacity8,16,32,48 and every width4..9 packing pattern with idle t, +the checker proves h(t)−mu_cap−sum n_w*pi_w≥0. All2,551 patterns are covered: +12 symbolic equalities and2,539 strict rational interval inequalities. The +interval implementation is adapted from PR3988 and uses exact rational bounds +for logarithms/exponentials; it is not a new independent numerical audit. + +The frozen actual incumbent pattern counts attain this dual. The checker checks +all aggregate capacities, bin totals and demands against the current408-role +inventory across3,240 calls. Literal owner chronology and source authenticity of +that aggregate are inherited from PR3969/3988; they are not replayed here. + +Replacing width5 by width4 changes the dual lower bound on owner idle cost by +pi4−pi5=1=h(1), exactly. Therefore even **arbitrary fractional repacking** must +pay at least the H1 saved inside each surviving module: + + local delta −H1 + owner lower-bound debit +H1 = 0. + +This is a lower bound on after-minus-before cost, so nonnegative means no gain. +The bound is optimistic: actual chronological owner restrictions can only add +cost. No new owner realization, supplier root or κ is asserted, and no owner +search is needed after the complete optimistic bill fails. At3,240 uses the +local reduction is3,240 H1 and the owner debit is at least3,240 H1. + +## Dirty semantics and limits + +For all ten literal provider/candidate words, apply only the declared frame +edits, regenerate cleanup, and run the retained exact forward and dual +arbitrary-dirty checks plus cleanup-boundary check. Cleanup bytes remain exactly +unchanged; all91 protected buffer identities remain present. Native matrices, +frames and phases are not modified. Replaying the predecessor checker is +explicitly credited and does not imply a fresh independent audit of it. + +The positive control verifies a literal witness; rejection controls exercise an +invalid scalar frame, a sign mutation breaking arbitrary-dirty semantics, +an omitted owner debit, and changed pinned source bytes. Optimized execution +must reject too. Unknown physical conversion, native compilation, precision, +stock/tape, uniformity, outer, analytic and BIT obligations are not priced as +zero. The construction stopped at the failed optimistic allowance. + +A useful next contract changes a pinned native/check boundary or the literal +graph, or supplies a distinct interior-saving mechanism whose complete allowance +is favorable before search. This result does not close those tasks or PR3945's +joint native/scalar refits. diff --git a/research/staged544-scalar-interior-refit/README.md b/research/staged544-scalar-interior-refit/README.md new file mode 100644 index 0000000000..c5c2379f2d --- /dev/null +++ b/research/staged544-scalar-interior-refit/README.md @@ -0,0 +1,42 @@ +# Fixed-native scalar-cone terminal refits + +Both exact PR3945 providers admit13,285 protected-terminal hyperplanes. Allowing +the forced backward scalar-frame cone in A/B/restore, while keeping precondition, +compensation, cut, native interfaces and the +literal graph fixed, yields only five new scalar-interior refits. Each saves H1 +locally but incurs at least H1 in the exact packing dual: **no complete gain**. +The17 previous terminal-only refunds are counted separately and excluded. + +This closes one bounded changed-interior construction attempt and identifies +which fixed interfaces prevent expansion. It does not claim a global scalar +optimum, physical supplier admission or any new κ. + +Run the complete source-bound census, tariff proof and all ten exact +arbitrary-dirty witnesses: + +```sh +python3 -B research/staged544-scalar-interior-refit/verify.py +python3 -O -B research/staged544-scalar-interior-refit/check_controls.py +``` + +`--quick` explicitly omits dirty interpreter replay; it is used only by two +source/receipt mutation controls. Default registered replay includes it fully. Default verification is read-only; +`--record` deliberately regenerates RESULT.json and is only a development mode. +See PROOF.md, RESULT.json, LEDGER.json, SOURCES.json and VALIDATION.json. + +Credit: Dugongue's PR3945 construction; dataisfire PR3734 and retained auditor; +Jeremy Kothe's rank7 lineage; ChaloupeMusic/Sagar Thakrar/ToikY dual lineage +(PR3815/3862/3890); PR3988 exact endpoint tariff; PR3969 owner bridge; +zxv/PR3682, RossRichardson/PR3605, ErwanSecousses/PR3815, +hexapode/PR3802/3875, roger-sato and Arham Tahir. Retained SOURCE-CREDITS.md +preserves upstream details. Chris R / Clear1nsight with substantial OpenAI Codex +assistance. Same-session checks/review are not human or proof-kernel acceptance. + +## Open next questions + +Can a changed native/check boundary or literal graph save more than its complete +owner debit? Start with one exact changed interface and its neighboring paid +climbs. Optional interior edits beyond the forced cone remain untested; this +result gives no global scalar optimum. Native phase, physical owner realization, +precision, stock/tape, uniformity, outer, analytic and BIT admission remain +inherited or unknown, not zero-cost obligations. diff --git a/research/staged544-scalar-interior-refit/RESULT.json b/research/staged544-scalar-interior-refit/RESULT.json new file mode 100644 index 0000000000..fe30674661 --- /dev/null +++ b/research/staged544-scalar-interior-refit/RESULT.json @@ -0,0 +1,525 @@ +{ + "tariff": { + "patterns": 2551, + "tight": 12, + "strict": 2539, + "refund_debit": "H1 exactly", + "incumbent_bins": 725760 + }, + "providers": { + "base": { + "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": 535, + "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": 554, + "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": 559, + "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": 580, + "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": 682, + "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": {} + } + ] + }, + "extra": { + "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": 535, + "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": 554, + "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": 559, + "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": 580, + "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": 682, + "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": {} + } + ] + } + }, + "witnesses": [ + { + "provider": "base", + "register": 282, + "canonical_sha256": "3901b650326a08c17334fb2d7987360fe187ebe712a880223c7bd716160f0f14" + }, + { + "provider": "base", + "register": 293, + "canonical_sha256": "4986946faba50f897350697e51f32b48bf66b57615badb456ce65390ebd5d4b1" + }, + { + "provider": "base", + "register": 298, + "canonical_sha256": "6b40e78352fc73505e2d2c7becaa65fd6128fcad9e5107653f26b1da9d565edc" + }, + { + "provider": "base", + "register": 309, + "canonical_sha256": "eaf942bd1fd415f0507d966a5ddc752eb5a6d24849f918220a4f72bde03f5022" + }, + { + "provider": "base", + "register": 373, + "canonical_sha256": "ca0b1d89288a86172cee81b1f811ea95d8797a7ddf60751539bc11586b4bf636" + }, + { + "provider": "extra", + "register": 282, + "canonical_sha256": "da25583d337e61e4c42ddd64697f15f431a680f2ee00d6055ceff30dd4d145a5" + }, + { + "provider": "extra", + "register": 293, + "canonical_sha256": "b6b41b47511514b6afdcc515162180123f98739811a27093412c51e86e813f44" + }, + { + "provider": "extra", + "register": 298, + "canonical_sha256": "9873d1ea4b05be4ba328c1e8dd3d3b328e104b25dcc56338be48967ec93a1c26" + }, + { + "provider": "extra", + "register": 309, + "canonical_sha256": "fb0cb25dd08eb972c58c72792c3fe30cc5f00dc07affe78e2e3574cac468c08f" + }, + { + "provider": "extra", + "register": 373, + "canonical_sha256": "0f09dd5d49c0e1b5725484ce7ebe39b58aa939f39312c75f619c4943b3eae444" + } + ] +} diff --git a/research/staged544-scalar-interior-refit/SOURCES.json b/research/staged544-scalar-interior-refit/SOURCES.json new file mode 100644 index 0000000000..43123649e6 --- /dev/null +++ b/research/staged544-scalar-interior-refit/SOURCES.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + } + ], + "snapshots": [ + { + "local": "frozen/audit_core.py", + "source_path": "research/staged544-producer-return/audit_core.py", + "source_repository": "dataisfire/integer-mult-bounds", + "source_commit": "fa041037a3374eaa08feeca0b26a5d6893194147", + "bytes": 19364, + "sha256": "888679ca8502cdcb100420fe5382a052529a494bf76cb332928b86e62612b951", + "git_blob": "8b5e1d5f2a106402f036b63028ecef31a4e4c462" + }, + { + "local": "frozen/SOURCE-CREDITS.md", + "source_path": "research/staged544-producer-return/SOURCE-CREDITS.md", + "source_repository": "dataisfire/integer-mult-bounds", + "source_commit": "fa041037a3374eaa08feeca0b26a5d6893194147", + "bytes": 2882, + "sha256": "d4a13d8b8ed9cdb594f00efb3d1a336e09d934423330f02a1514308a720c278b", + "git_blob": "c054fad87eeaa510865e682ee0c976c4cd728da2" + }, + { + "local": "frozen/retiming.py", + "source_path": "research/rank-profile-retiming-obstruction/retiming.py", + "source_repository": "Clear1nsight/integer-mult-bounds", + "source_commit": "359fe0fe77d29544972fd22ee674085ed5a3b4d0", + "bytes": 10391, + "sha256": "591d7278541ac4de9e9b6fc1e17aba23b205ac4b6c81824a28fc08294658ef0d", + "git_blob": "c33d7bbcdf2435056b3a56526e8e43f6513e381b" + }, + { + "local": "frozen/WORD-base.json.gz", + "source_repository": "CrocSwap/integer-mult-bounds", + "source_commit": "91f81d131252db704f945891da1ea54e29d46b8b", + "source_path": "research/staged544-terminal-gap-fill/owner/inputs/WORD-base.json.gz", + "bytes": 74428, + "sha256": "08e6c96fbe3dfec96cb8451b3867ef8c1a214109ecd1e5af7fcc28e0f05728d0", + "git_blob": "806784bf99d9d15004d2d227d06268556a0726c8" + }, + { + "local": "frozen/WORD-extra.json.gz", + "source_repository": "CrocSwap/integer-mult-bounds", + "source_commit": "91f81d131252db704f945891da1ea54e29d46b8b", + "source_path": "research/staged544-terminal-gap-fill/owner/inputs/WORD-extra.json.gz", + "bytes": 74425, + "sha256": "d83c2ec9cecc0ad092d34ea4080b28a4fd7199579356b6d5a8fc6cd53ff93299", + "git_blob": "c531be7383ad3ba941600c7ced14e5e10d6d1c67" + }, + { + "local": "OWNER-PATTERNS.json", + "source_repository": "Clear1nsight/integer-mult-bounds", + "source_commit": "7d85649b64243022b3141df00c61027a083a533a", + "source_path": "research/staged544-terminal-extension-budget/OWNER-PATTERNS.json", + "bytes": 1397, + "sha256": "0ffae1b949bab97e7d5a6313c3936be248d75a43ba06593bc45faca4fb686e99", + "git_blob": "858a0225cae00233f0959675393a94660b41c69a" + } + ], + "credited_adaptation": { + "tariff.py": "PR3988 exact rational arithmetic; PR3815/3862/3890 dual, not independent audit", + "cone_checker": "New cone propagation, credited reused chronological trace" + } +} diff --git a/research/staged544-scalar-interior-refit/TASK.json b/research/staged544-scalar-interior-refit/TASK.json new file mode 100644 index 0000000000..de999fefa9 --- /dev/null +++ b/research/staged544-scalar-interior-refit/TASK.json @@ -0,0 +1,68 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json", + "research/rank7-joint-endframes/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering" + ] + }, + "scope_status": "refined", + "actual_scope": "Scalar-interior/terminal forced-intersection contraction on both pinned3945providers, graph/native interfaces fixed; complete optimistic budget rejection.", + "scope_change_reason": "Assigned changed-interior construction. Smallest refits tie; one bounded pivot expands to full forced backward scalar cone.", + "bottleneck_link": "A local terminal gain is useful only if every changed dimension fits an actual chronological owner and its complete recursive bill is paid.", + "budget_minutes": 60, + "stop_rule": "Stop after exact forced-cone domain and optimistic owner debit; no graph/native/optional scalar expansion.", + "outcome": "completed", + "evidence": "RESULT.json, PROOF.md, LEDGER.json, VALIDATION.json", + "author": "Chris R / Clear1nsight with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance; one agent independently implemented checker while root coordinated overlap/publication.", + "open_questions": [ + { + "question": "Can a changed native/check boundary or graph exceed its complete owner debit?", + "why_it_matters": "Five fixed-native scalar cones tie under fractional repacking.", + "first_step": "Price literal changed interface and every neighboring obligation before search.", + "blocked_by": "Needs favorable full allowance and compatible subspaces." + } + ], + "expansion_decision": "One bounded pivot from final scalar gate to forced backward cone, then STOP.", + "bounded_pivot": "Every protected terminal hyperplane; optional interior edits excluded." +} diff --git a/research/staged544-scalar-interior-refit/VALIDATION.json b/research/staged544-scalar-interior-refit/VALIDATION.json new file mode 100644 index 0000000000..ca8fe9f086 --- /dev/null +++ b/research/staged544-scalar-interior-refit/VALIDATION.json @@ -0,0 +1,37 @@ +{ + "status": "PASS_REGISTERED_AND_OPTIMIZED_FULL", + "python": "3.12.3 (main, Aug 31 2026, 10:18:26) [GCC 13.3.0]", + "external": "No network required; exact frozen inputs", + "independence": "New cone proof/propagation; reused credited trace, dirty auditor and tariff arithmetic.", + "runs": [ + { + "label": "registered", + "command": [ + "/usr/bin/python3", + "-B", + "scripts/research_package.py", + "--package", + "research/staged544-scalar-interior-refit" + ], + "seconds": 73.182610914002, + "returncode": 0 + }, + { + "label": "optimized-full", + "command": [ + "/usr/bin/python3", + "-O", + "-B", + "/home/d3lerium/.codex/.chatgpt-projects/g-p-6ad5817fd84881918865926b6fd51453/round3-joint-interior-session/worktree/research/staged544-scalar-interior-refit/verify.py" + ], + "seconds": 39.782545166999626, + "returncode": 0 + } + ], + "controls": "Four rejecting controls plus literal dirty positive; two optimized CLI mutations", + "unrun": [ + "New literal owner assignment", + "Physical native/precision/stock/tape/uniformity/outer/all-size/analytic/BIT admission", + "HostedCI/export/committed-byte receipts reported separately at publication" + ] +} diff --git a/research/staged544-scalar-interior-refit/VERIFY.json b/research/staged544-scalar-interior-refit/VERIFY.json new file mode 100644 index 0000000000..1f2768a6c5 --- /dev/null +++ b/research/staged544-scalar-interior-refit/VERIFY.json @@ -0,0 +1,28 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 360, + "checks": "26570provider/hyperplane pairs,2551pattern tariff, ten literal dirty witnesses." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/check_controls.py" + ], + "timeout_seconds": 180, + "checks": "Positive dirty witness and four rejecting controls, two actual optimized CLI mutations." + } + ] +} diff --git a/research/staged544-scalar-interior-refit/check_controls.py b/research/staged544-scalar-interior-refit/check_controls.py new file mode 100644 index 0000000000..2c4fd3adc9 --- /dev/null +++ b/research/staged544-scalar-interior-refit/check_controls.py @@ -0,0 +1,32 @@ +"""Positive and rejecting controls; no assert, valid under python -O.""" +from pathlib import Path +import copy,json,subprocess,sys,tempfile,shutil +import verify as v + +def reject(call,why): + try:call() + except (ValueError,RuntimeError,v.audit.AuditFailure):return + raise ValueError('accepted mutation: '+why) + +def main(): + root=Path(__file__).resolve().parent;result=v.read(root/'RESULT.json') + w=v.read(root/'frozen/WORD-base.json.gz');row=result['providers']['base']['candidates'][0] + x=v.apply(w,row);v.semantics(x) + bad=copy.deepcopy(row);bad['edits'][0]['new']=[];reject(lambda:v.apply(w,bad),'invalid scalar containment') + bad=copy.deepcopy(x);e=row['edits'][0];bad[e['section']][e['index']][2]=1 + reject(lambda:v.semantics(bad),'scalar sign changes dirty semantics') + for kind in ('owner-debit','source-byte'): + with tempfile.TemporaryDirectory() as td: + target=Path(td)/'pkg';shutil.copytree(root,target) + for p in target.rglob('*'): + if p.is_file():p.chmod(0o600) + elif p.is_dir():p.chmod(0o700) + if kind=='owner-debit': + r=v.read(target/'RESULT.json');r['providers']['base']['candidates'][0]['owner_debit']={};(target/'RESULT.json').write_text(json.dumps(r)) + else: + p=target/'frozen/WORD-base.json.gz';p.write_bytes(p.read_bytes()+b'!') + run=subprocess.run([sys.executable,'-O','-B',str(target/'verify.py'),'--quick'],capture_output=True,text=True) + v.need(run.returncode!=0,'optimized CLI accepted '+kind) + v.need(('result mismatch' if kind=='owner-debit' else 'frozen source hash') in run.stderr,'wrong rejection '+kind) + print(json.dumps({'status':'PASS_POSITIVE_AND_4_REJECTIONS','positive':'literal arbitrary-dirty witness','optimized_cli_mutations':2})) +if __name__=='__main__':main() diff --git a/research/staged544-scalar-interior-refit/frozen/SOURCE-CREDITS.md b/research/staged544-scalar-interior-refit/frozen/SOURCE-CREDITS.md new file mode 100644 index 0000000000..c054fad87e --- /dev/null +++ b/research/staged544-scalar-interior-refit/frozen/SOURCE-CREDITS.md @@ -0,0 +1,14 @@ +# Source credit and independence + +New work: dataisfire with substantial OpenAI Codex assistance, Apache-2.0. No independent human review, fresh third-party AI review or proof-kernel verification is claimed. + +The construction extends [PR3682](https://github.com/CrocSwap/integer-mult-bounds/pull/3682), head431e6c6023ef352c41696469de7fb614cd4ded8c. Its retimed word, actual T360 source clock and immutable native/parent framework are retained. The complete new source/receipt snapshot is bound by REPLAY-INPUTS.json. The new ordinary source stage is an explicit pinned record applied after the unchanged predecessor reconstruction. + +- [PR3605](https://github.com/CrocSwap/integer-mult-bounds/pull/3605), Ross Richardson, supplies the staged-entrance mechanism, literal cleanup and exact Gaussian residual-check pattern. staged_pair.py is retained; the new544 shear and its proof are separate. +- [PR3638](https://github.com/CrocSwap/integer-mult-bounds/pull/3638), head d62e1acd7518a231440383f0d0dddf54d6edf8c1, supplies the T360 source-window clock, chronological aggregate model and integral-network/literal construction, with its retained PR3605 and earlier credits. The new inventory, integer incumbent and literal fill are recomputed. No predecessor owner receipt is used as proof of the new fill. +- [PR3687](https://github.com/CrocSwap/integer-mult-bounds/pull/3687) and [PR3693](https://github.com/CrocSwap/integer-mult-bounds/pull/3693), Sagar Thakrar and roger-sato with their credited AI assistance, supply audit_core.py and the whole-word semantics adapter audit_verify.py. These bytes are retained and reused. They are independent of the current constructor in the stated interpreter scope, not a newly written independent audit or new reviewer approval. +- The coupled-word source lineage includes PR3133, PR2979, Marius-Paul Dumitrean, dcharb78, Jeremy Kothe and the retained native/owner/block-norm/outer authors. All notices and scientific engines inside the source snapshot remain intact. + +owner_audit.py is a standalone standard-library adaptation of the source-window/family/prefix/invoice predicates in PR3638's independent_literal.py. It imports no producer, optimizer or retained owner checker. Its source template, plan and actual native canonical words are authenticated inputs. Three controls mutate actual literal roles and must fail for the intended reason. It shares the credited contract interpretation; it is not evidence of independent human agreement. + +The rational finite-price enclosure is retained from the PR3682 sources. New script adapters bind it to the actual finite histogram. Native forward/backward scalar replay, wrapper/phase lowering and all-column warp recipes were freshly run for both new words; unchanged native and parent ancestry is explicitly reused. The separate new544 span(414,51) residual check includes global Gaussian phase. diff --git a/research/staged544-scalar-interior-refit/frozen/WORD-base.json.gz b/research/staged544-scalar-interior-refit/frozen/WORD-base.json.gz new file mode 100644 index 0000000000..806784bf99 Binary files /dev/null and b/research/staged544-scalar-interior-refit/frozen/WORD-base.json.gz differ diff --git a/research/staged544-scalar-interior-refit/frozen/WORD-extra.json.gz b/research/staged544-scalar-interior-refit/frozen/WORD-extra.json.gz new file mode 100644 index 0000000000..c531be7383 Binary files /dev/null and b/research/staged544-scalar-interior-refit/frozen/WORD-extra.json.gz differ diff --git a/research/staged544-scalar-interior-refit/frozen/audit_core.py b/research/staged544-scalar-interior-refit/frozen/audit_core.py new file mode 100644 index 0000000000..8b5e1d5f2a --- /dev/null +++ b/research/staged544-scalar-interior-refit/frozen/audit_core.py @@ -0,0 +1,480 @@ +"""Independent exact semantics and binary-frame bill for the BORROW-WORD format. + +Standard library only. Nothing is imported from the audited authors' code +(PR3133/PR3605 producers, cleanup generator, evaluator or frame solver); the word +format and its semantic contract were read from those pinned sources and are +credited there. The frame-bill and free-word structure (point-set spans, warp +frame and lifted-frame checks, target levels keyed by register, dual symbol +naming) re-implements, without importing, Arham Tahir's +research/coupled-carrier-independent-audit/verify.py (Apache-2.0) and shares its +reading of the contract, so this module is not independent of that audit. + +Sagar Thakrar (thakrarsagar), with substantial AI assistance from Claude +(Anthropic, Claude Opus 5.5). Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as Q + +V, N, H = 112, 704, 9 # sources 0..111, targets 112..223, helpers 224..703 +DUAL = 10 ** 6 # offset naming the independent dual symbols D_k = K_k^(-T) + + +class AuditFailure(Exception): + """Explicit failure; never disabled by python -O.""" + + +def need(ok, *why): + if not ok: + raise AuditFailure(' '.join(map(str, why))) + + +def is_target(r): + return V <= r < 2 * V + + +def touched(g): + return g[1:3] if g[0] == 'add' else g[1:2] + + +# ---------------------------------------------------------------------------- +# Binary frames: a subspace of F_2^9 is stored as a 512-bit point-set mask +# (bit x set iff x lies in the subspace). Containment is mask inclusion. +# ---------------------------------------------------------------------------- +_SPAN = {} + + +def span(vectors): + key = tuple(vectors) + mask = _SPAN.get(key) + if mask is None: + points = {0} + for u in key: + need(type(u) is int and 0 <= u < 512, 'frame vector out of range', u) + if u not in points: + points |= {p ^ u for p in points} + mask = sum(1 << p for p in points) + _SPAN[key] = mask + return mask + + +def points(mask): + return [x for x in range(512) if mask >> x & 1] + + +def dim(mask): + size = bin(mask).count('1') + need(size and size & (size - 1) == 0, 'not a subspace point set') + return size.bit_length() - 1 + + +FULL = (1 << 512) - 1 +ZERO = 1 + + +def hyperplane(port): + return sum(1 << x for x in range(512) if bin(x & port).count('1') % 2 == 0) + + +def warp_images(columns): + """Images of all 512 vectors under the F_2-linear map with columns G e_i.""" + need(len(columns) == H and all(type(c) is int and 0 <= c < 512 for c in columns), 'warp columns') + images = [0] * 512 + for x in range(1, 512): + low = x & -x + images[x] = images[x ^ low] ^ columns[low.bit_length() - 1] + need(len(set(images)) == 512, 'singular warp') + return images + + +def image_mask(images, mask): + return sum(1 << images[x] for x in points(mask)) + + +def lagrangian_action_ok(images, U, E): + """K_G(x,z)=(Gx, Gx+G^{-T}(x+z)) is symplectic and maps L_U to L_E, L_0 and L_FULL to themselves. + + L_U={(x,x+p): x in U, p in U^perp}. This is the binary frame action only; it + is not a Clifford phase or Gaussian-product certificate. For invertible G with + G(U)=E it is implied by the frame-map check ( = ), so it is a + consistency check of the implementation, not extra evidence. + """ + inverse = [0] * 512 + for x, y in enumerate(images): + inverse[y] = x + # G^{-T} z: bit j of the result is . + git = lambda z: sum((bin(inverse[1 << j] & z).count('1') & 1) << j for j in range(H)) + lift = lambda x, z: (images[x], images[x] ^ git(x ^ z)) + pair = lambda a, b: (bin(a[0] & b[1]).count('1') + bin(a[1] & b[0]).count('1')) & 1 + basis = [(1 << i, 0) for i in range(H)] + [(0, 1 << i) for i in range(H)] + lifted = [lift(*b) for b in basis] + if any(pair(lifted[i], lifted[j]) != pair(basis[i], basis[j]) for i in range(18) for j in range(i + 1, 18)): + return False + + def frame(mask): + us = points(mask) + perp = [p for p in range(512) if all(bin(p & u).count('1') % 2 == 0 for u in us)] + return {(u, u ^ p) for u in us for p in perp} + return all({lift(*pt) for pt in frame(a)} == frame(b) for a, b in ((ZERO, ZERO), (FULL, FULL), (U, E))) + + +# ---------------------------------------------------------------------------- +# Chronological binary-frame bill (BORROW-WORD contract) +# ---------------------------------------------------------------------------- +def frame_bill(w, lagrangian=False): + rep = w['report'] + need((rep['v'], 2 * rep['v'] + rep['R'], rep['h']) == (V, N, H), 'word geometry') + removed = set(w['removed']) + need(len(removed) == len(w['removed']) and all(2 * V <= r < N for r in removed), 'removed helpers') + live = [r for r in range(N) if r not in removed] + liveset = set(live) + B, warps = w['B'], w['warps'] + for k, (pos, lender, cols, U, E) in enumerate(warps, 1): + need(0 <= pos <= len(B), 'warp position', k) + need(lender in liveset and not is_target(lender), 'warp lender', k) + images = warp_images(cols) + su, se = span(U), span(E) + need(dim(su) == len(U) == len(E) == dim(se), 'warp frame bases', k) + need(image_mask(images, su) == se, 'warp does not map its frame', k) + if lagrangian: + need(lagrangian_action_ok(images, su, se), 'lifted frame action', k) + for name in ('A', 'B', 'restore'): + for g in w[name]: + if g[0] != 'warp': + need(all(r in liveset for r in touched(g)), 'removed/out-of-range register', name, g) + if g[0] == 'add' and not is_target(g[1]): + need(not is_target(g[2]), 'non-target reads a target', name, g) + need(all(g[-1] is None and is_target(g[1]) and g[0] == 'add' for g in w['cut']), 'cut gates') + need(all(g[-1] == [] and is_target(g[1]) for g in w['precondition'] + w['compensation']), 'zero-frame wrapper writes') + need(all(not is_target(g[1]) for g in w['restore']), 'restore writes a target') + + ports = w['ports'] + start, end = {}, {} + for r in live: + if r < V: + start[r], end[r] = span((ports[r],)), FULL + elif r < 2 * V: + start[r], end[r] = ZERO, hyperplane(ports[r - V]) + else: + start[r], end[r] = ZERO, FULL + for q, U in w['start_extra'].items(): + need(int(q) in liveset and int(q) >= 2 * V, 'entrance names a live helper', q) + start[int(q)] = span(U) + for q, U in w['helper_final'].items(): + need(int(q) in liveset and int(q) >= 2 * V, 'terminal names a live helper', q) + end[int(q)] = span(U) + + current, bill, chain = dict(start), Counter(), {} + + def climb(r, mask, where): + need(current[r] & ~mask == 0, 'frame containment fails', where, r) + d = dim(mask) - dim(current[r]) + if d: + bill[d] += 1 + chain.setdefault(r, []).append((where, d, mask)) + current[r] = mask + + npre = w['prelude_events'] + for i, g in enumerate(w['A']): + if g[0] == 'warp': + need(i < npre and len(g) == 5, 'warp outside the prelude', i) + _, r, op, fr, to = g + need(op != 0 and abs(op) <= len(warps) and warps[abs(op) - 1][1] == r, 'prelude warp lender', i) + images = warp_images(warps[abs(op) - 1][2]) + if op < 0: + inverse = [0] * 512 + for x, y in enumerate(images): + inverse[y] = x + images = inverse + need(image_mask(images, span(fr)) == span(to), 'prelude warp frame action', i) + need(current[r] == span(fr), 'prelude warp entry frame', i, r) + current[r] = span(to) + chain.setdefault(r, []).append((('A', i), 'warp', span(to))) + else: + if i < npre: + need(is_target(g[1]), 'prelude scalar writes a non-target', i) + for r in touched(g): + climb(r, span(g[-1]), ('A', i)) + levels = {V + int(t): span(U) for t, U in w['target_levels'].items()} + need(all(current[t] == levels.get(t, ZERO) for t in range(V, 2 * V)), 'target cut levels') + for q, U in zip(w['centers'], w['center_frames']): + U = span(U) + need(current[q] == U, 'centre entry frame', q) + served = {levels.get(g[1], ZERO) for g in w['cut'] if g[2] == q} + for T in sorted(served, key=lambda m: -dim(m)): + need(T & ~U == 0, 'centre descent not nested', q) + d = dim(U) - dim(T) + if d: + bill[d] += 1 + chain.setdefault(q, []).append((('centre',), d, T)) + U = T + at = {} + for k, rec in enumerate(warps, 1): + at.setdefault(rec[0], []).append(k) + for p in range(len(B) + 1): + for k in at.get(p, ()): + _, lender, _, U, E = warps[k - 1] + need(current[lender] == span(U), 'native warp entry frame', k, lender) + current[lender] = span(E) + chain.setdefault(lender, []).append((('warp', k), 'warp', span(E))) + if p < len(B): + for r in touched(B[p]): + climb(r, span(B[p][-1]), ('B', p)) + for i, g in enumerate(w['restore']): + for r in touched(g): + climb(r, span(g[-1]), ('restore', i)) + for r in live: + climb(r, end[r], ('end',)) + restored = set(map(int, w['helper_final'])) + need(all(end[r] == FULL for r in live if r not in restored and not is_target(r)), 'a FULL-cleanup register ends low') + widths = Counter(dim(end[r]) - dim(start[r]) for r in live if r >= 2 * V) + return dict(sorted(bill.items())), dict(sorted(widths.items())), chain, start, end + + +def hygiene(w): + """Inherited structural contract: dyadic scalars, power-of-two scales, wrapper and correction access.""" + entering = set(map(int, w['start_extra'])) + restored = set(map(int, w['helper_final'])) + live = set(range(N)) - set(w['removed']) + for name in ('precondition', 'compensation', 'A', 'cut', 'B', 'restore', 'cleanup'): + for g in w[name]: + if g[0] == 'warp': + continue + q = Q(g[3], g[4]) if g[0] == 'add' else Q(g[2], g[3]) + need(q != 0 and q.denominator & (q.denominator - 1) == 0, 'non-dyadic scalar', name, g) + if g[0] == 'scale': + need(abs(q.numerator) & (abs(q.numerator) - 1) == 0, 'non power-of-two scale', name, g) + for g in w['precondition'] + w['compensation']: + need(not any(r in entering | restored for r in touched(g)), 'wrapper touches an entering or restored helper', g) + for c in w['initial_corrections']: + word = c['operator_word'] + need(is_target(c['target']) and c['source'] in live and c['source'] >= 2 * V + and c['source'] not in entering, 'correction access', c) + need(word and all(w['warps'][abs(o) - 1][1] == c['source'] for o in word), 'correction operator lender', c) + q = Q(c['coefficient']) + need(q != 0 and q.denominator & (q.denominator - 1) == 0, 'correction coefficient', c) + return True + + +# ---------------------------------------------------------------------------- +# Literal inverse cleanup, derived from the contract +# ---------------------------------------------------------------------------- +def ordinary_forward(w): + """Chronological non-wrapper actions whose inverse forms cleanup.""" + out = [g for g in w['A'][w['prelude_events']:]] + at = {} + for k, rec in enumerate(w['warps'], 1): + at.setdefault(rec[0], []).append(['warp', rec[1], k]) + for p in range(len(w['B']) + 1): + out += at.get(p, []) + if p < len(w['B']): + out.append(w['B'][p]) + return out + list(w['restore']) + + +def derive_cleanup(w): + restored = set(map(int, w['helper_final'])) + buf = lambda r: r + N if r in restored else r + full = [256, 128, 64, 32, 16, 8, 4, 2, 1] + out = [] + for g in reversed(ordinary_forward(w)): + if g[0] == 'warp': + out.append(['warp', buf(g[1]), -g[2], full]) + elif is_target(g[1]): + continue + elif g[0] == 'add': + out.append(['add', buf(g[1]), buf(g[2]), -g[3], g[4], full]) + else: + need(g[0] == 'scale', 'unknown primitive', g) + out.append(['scale', buf(g[1]), g[3], g[2], full]) + return out + + +def same_cleanup(a, b): + norm = lambda c: [(g[:-1], span(g[-1])) for g in c] + return len(a) == len(b) and norm(a) == norm(b) + + +# ---------------------------------------------------------------------------- +# Exact free-operator semantics. A value is a dict {(input, word): Fraction}; +# word is a reduced tuple of signed operator ids (leftmost = applied last). +# ---------------------------------------------------------------------------- +def program(w, cleanup=None): + """Literal executed sequence: corrections, wrapper, A, cut, B+warps, restore | cleanup.""" + items = [('corr', c['target'], c['source'], tuple(c['operator_word']), Q(c['coefficient'])) + for c in w['initial_corrections']] + items += w['precondition'] + w['compensation'] + w['A'] + w['cut'] + at = {} + for k, rec in enumerate(w['warps'], 1): + at.setdefault(rec[0], []).append(['warp', rec[1], k]) + for p in range(len(w['B']) + 1): + items += at.get(p, []) + if p < len(w['B']): + items.append(w['B'][p]) + items += w['restore'] + return items, list(w['cleanup'] if cleanup is None else cleanup) + + +def dual_op(op): + return (1 if op > 0 else -1) * (abs(op) + DUAL) + + +def _left(op, word): + return word[1:] if word and word[0] == -op else (op,) + word + + +def _right(word, op): + return word[:-1] if word and word[-1] == -op else word + (op,) + + +def _axpy(dst, src, q): + for key, x in src.items(): + y = dst.get(key, 0) + q * x + if y: + dst[key] = y + else: + dst.pop(key, None) + + +def forward_rows(w, cleanup=None, dual=False, symbolic_buffers=True, snapshot=None): + """Schrodinger pass: every register's value as a combination of initial inputs. + + Live inputs are independent symbols. Private buffers are independent symbols + when symbolic_buffers is set (dirty), otherwise zero. The optional snapshot + callback sees the rows at the cleanup boundary. + """ + removed = set(w['removed']) + live = [r for r in range(N) if r not in removed] + restored = sorted(map(int, w['helper_final'])) + rows = {r: {(r, ()): Q(1)} for r in live} + for c in restored: + rows[c + N] = {(c + N, ()): Q(1)} if symbolic_buffers else {} + prefix, tail = program(w, cleanup) + + def apply(g): + kind = g[0] + if kind == 'add': + t, s, q = g[1], g[2], Q(g[3], g[4]) + need(t != s and q, 'add gate', g) + if dual: + t, s, q = s, t, -q + _axpy(rows[t], rows[s], q) + elif kind == 'scale': + q = Q(g[2], g[3]) + need(q != 0, 'zero scale', g) + if dual: + q = 1 / q + rows[g[1]] = {k: q * x for k, x in rows[g[1]].items()} + elif kind == 'warp': + op = dual_op(g[2]) if dual else g[2] + rows[g[1]] = {(var, _left(op, word)): x for (var, word), x in rows[g[1]].items()} + elif kind == 'corr': + _, t, s, word, c = g + if dual: + src, ops, dst, c = rows[t], [-dual_op(o) for o in word], s, -c + else: + src, ops, dst = rows[s], list(reversed(word)), t + moved = {} + for (var, wd), x in src.items(): + for o in ops: + wd = _left(o, wd) + moved[var, wd] = x + _axpy(rows[dst], moved, c) + else: + raise AuditFailure('unknown primitive ' + repr(g)) + + for g in prefix: + apply(g) + if snapshot is not None: + snapshot(rows) + for g in tail: + apply(g) + return rows + + +def reverse_columns(w, cleanup=None, upto_cleanup=False): + """Heisenberg pull-back: process the forward program backwards. + + cols[s] = {(output, word): coefficient}: the final output register 'output' + contains coefficient*word*x_s. Words grow on the right. Every live input and + every private buffer is an independent symbol. + """ + removed = set(w['removed']) + live = [r for r in range(N) if r not in removed] + restored = sorted(map(int, w['helper_final'])) + regs = live + [c + N for c in restored] + cols = {r: {(r, ()): Q(1)} for r in regs} + prefix, tail = program(w, cleanup) + seq = prefix if upto_cleanup else prefix + tail + for g in reversed(seq): + kind = g[0] + if kind == 'add': + t, s, q = g[1], g[2], Q(g[3], g[4]) + need(t != s and q, 'add gate', g) + _axpy(cols[s], cols[t], q) + elif kind == 'scale': + q = Q(g[2], g[3]) + need(q != 0, 'zero scale', g) + cols[g[1]] = {k: q * x for k, x in cols[g[1]].items()} + elif kind == 'warp': + op = g[2] + cols[g[1]] = {(out, _right(word, op)): x for (out, word), x in cols[g[1]].items()} + elif kind == 'corr': + _, t, s, word, c = g + moved = {} + for (out, wd), x in cols[t].items(): + for o in word: + wd = _right(wd, o) + moved[out, wd] = x + _axpy(cols[s], moved, c) + else: + raise AuditFailure('unknown primitive ' + repr(g)) + return cols + + +def transpose(cols): + rows = {} + for s, col in cols.items(): + for (r, word), x in col.items(): + rows.setdefault(r, {})[s, word] = x + return rows + + +def endpoint_defects(w, rows, dual=False): + """Compare final rows with the contract on the zero-buffer (live-input) domain. + + Returns (bad live registers, dirty buffers, buffer->live leaks, buffer self-map identity). + """ + removed = set(w['removed']) + live = [r for r in range(N) if r not in removed] + restored = sorted(map(int, w['helper_final'])) + bad = [] + for r in live: + expect = {(r, ()): Q(1)} + if dual and r < V: + expect[r + V, ()] = Q(-1) + if not dual and is_target(r): + expect[r - V, ()] = Q(1) + got = {k: x for k, x in rows.get(r, {}).items() if k[0] < N} + if got != expect: + bad.append(r) + dirty = [c for c in restored if any(k[0] < N for k in rows.get(c + N, {}))] + leaks = sorted({r for r in live for k in rows.get(r, {}) if k[0] >= N}) + buffer_identity = all({k: x for k, x in rows.get(c + N, {}).items() if k[0] >= N} == {(c + N, ()): Q(1)} + for c in restored) + return bad, dirty, leaks, buffer_identity + + +def boundary_defects(w, rows): + """Contract at the cleanup boundary (forward): targets sheared, restored helpers clean and isolated.""" + restored = set(map(int, w['helper_final'])) + out = [] + for t in range(V, 2 * V): + if {k: x for k, x in rows[t].items() if k[0] < N} != {(t, ()): Q(1), (t - V, ()): Q(1)}: + out.append(('target', t)) + for c in restored: + if rows[c] != {(c, ()): Q(1)}: + out.append(('restored', c)) + for r, row in rows.items(): + if r < N and r not in restored and any(k[0] in restored for k in row): + out.append(('restored input read', r)) + return out diff --git a/research/staged544-scalar-interior-refit/frozen/retiming.py b/research/staged544-scalar-interior-refit/frozen/retiming.py new file mode 100644 index 0000000000..c33d7bbcdf --- /dev/null +++ b/research/staged544-scalar-interior-refit/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-scalar-interior-refit/tariff.py b/research/staged544-scalar-interior-refit/tariff.py new file mode 100644 index 0000000000..06c22dab77 --- /dev/null +++ b/research/staged544-scalar-interior-refit/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-scalar-interior-refit/verify.py b/research/staged544-scalar-interior-refit/verify.py new file mode 100644 index 0000000000..54402df9f1 --- /dev/null +++ b/research/staged544-scalar-interior-refit/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()