diff --git a/research/owned770-descent-pruning/PREDECESSOR.json b/research/owned770-descent-pruning/PREDECESSOR.json new file mode 100644 index 0000000000..25261ef2ba --- /dev/null +++ b/research/owned770-descent-pruning/PREDECESSOR.json @@ -0,0 +1,12 @@ +{ + "author": "DreamingOfClouds", + "credit": "The retained word is DreamingOfClouds' contribution, extending the PR6030/PR5907 words and Ali Romman's PR5827, Mason Hale's PR5811, and the credited P104 lineage. This export preserves the original bytes. Apache-2.0.", + "git_blob": "69b70ee50c697b185ebf585fbe69f2487af32d1d", + "head": "4f3b67e7c37ae270da9584033132866d0cf63e42", + "path": "research/p104-root-relay-descent-2/WORD.json.gz", + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/6144", + "readme": "https://github.com/DreamingOfClouds/integer-mult-bounds/blob/4f3b67e7c37ae270da9584033132866d0cf63e42/research/p104-root-relay-descent-2/README.md", + "repository": "DreamingOfClouds/integer-mult-bounds", + "sha256": "c71985d96bf3d4a35aae111aaba87e376f7367efb4a5686278ef293732757533", + "size": 119901 +} diff --git a/research/owned770-descent-pruning/PROOF.md b/research/owned770-descent-pruning/PROOF.md new file mode 100644 index 0000000000..778ee0e810 --- /dev/null +++ b/research/owned770-descent-pruning/PROOF.md @@ -0,0 +1,114 @@ +# Coalescing the last-read owned copy + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Claim and source + +The claim is a finite exact circuit certificate and a scoped substitution +proof. It does not assert a new exponent saving, a smaller peak-space bound, +or a complete multiplication theorem. + +The input is DreamingOfClouds' PR6144 word at +`4f3b67e7c37ae270da9584033132866d0cf63e42`. `PREDECESSOR.json` records the +original path, Git blob, SHA256 and credit. The byte-identical exported word +is retained in this branch's history. Ali Romman's PR5827 `local.py` is already +on canonical main and is used unchanged. The source word's conditional +supplier and framework claims are cited, not independently audited here. + +All event indices below are zero-based indices in the retained input. + +## General substitution + +Suppose an owned field S contains x, and an initialized owned field D receives +COPY D,S followed by SCALE D,q. Suppose that after this COPY the old S has no +use except a later CLEAR. Replace the COPY and D's initialization by SCALE S,q; +execute D's continuation on S; clear S where D was cleared; delete the old +S CLEAR. Require that S is available before the continuation starts, and that +the continuation does not read the old S separately. + +Immediately after the scaling, the substituted S and old D have equal values +and frames. Every subsequent continuation operation has the same coefficient, +frame and value operands after renaming. Induction over the continuation proves +equality of every other field and the substituted D value. The unread old S +does not influence another field. Both constructions return all owned fields +to the erased state. This is an exact linear argument over any coefficient +field containing q. Its use here is over the dyadic rationals. + +The substituted lifetime starts at the old S initialization and ends at the +old D erasure. While the two lifetimes previously overlapped, the new one +occupies one field. Elsewhere it occupies at most their former union. Thus +this substitution cannot increase live owned occupancy. This statement alone +does not imply that the global peak falls strictly. + +## Literal application + +Old S is role 791, initialized at event 13473 in frame 549 and assigned the +value x of role 173 by event 13474. Its only subsequent reads are + +```text +13475 ADD 121,791,1/2,549 +13659 COPY 770,791,1,549 +``` + +Its only remaining use is CLEAR at event 15591 in frame 549. There are no +hidden reads or writes. `construct.py` checks this complete use list. + +Old D is role 770. The adjacent events at 13658 through 13661 initialize it, +copy x, scale by 1/2 and start its descent from frame 549 to 553. Its +continuation ends with CLEAR in frame 593 at event 15424. It has exactly one +initialization and no use outside that lifetime. The continuation never reads +old 791. Therefore the substitution lemma applies with q = 1/2. The new +scaling occurs just before the old descent, after the retained read at 13475. + +The constructor removes old role 770 from the owned inventory. For every +remaining old role r, the new label is r when r < 770 and r-1 when r > 770. +Uses of old 770 first become old 791, then become new role 790. Only opcode +role positions are renamed; frame IDs and coefficients are unchanged. + +All public initial and final frames, ports, productive outputs and arbitrary +public input coordinates are identical. Initial arbitrary owned contents +cannot affect the result because every reached owned lifetime initializes +before use. The new source-owned lifetime is initialized once and cleared at +the continuation's old endpoint. Both exact row replay and reverse-column +replay check the resulting word in full. + +## Exact account + +The removed INIT costs 2 scalar units, COPY with coefficient 1 costs 8, and +CLEAR costs 2. The same single SCALE by 1/2 remains and costs 2 in either +program. Net savings are 12 scalar units and three events. The original +source-owned CLEAR disappears, and the continuation CLEAR now clears the +substituted field. + +Literal enumeration gives + +```text +events 22818 -> 22815 +local scalar units 189658 -> 189646 +declared owned fields 29 -> 28 +owned lifetimes 31 -> 30 +peak live owned fields 13 -> 13 +``` + +Every MOVE keeps its entry frame, exit frame and ownership flag. Its complete +native operator is therefore the same prescribed operator after role +renaming, including its scalar phase. No new native frame pair is introduced. +Every public endpoint is retained, so every productive rank is retained. +The complete local paid histogram is unchanged and equals +`{1:2215, 2:457, 3:496, 4:99, 5:164, 6:8, 7:9, 8:1}`. +Consequently this edit supplies no new signed-moment or kappa gain. + +## Verification boundary + +The finite checker verifies all 798 columns and 636804 matrix coefficients +of the edited word using the retained sparse forward and dense reverse +implementations. Nine mutation controls cover missing initialization, scaling, +clear, descent and read; wrong scaling sign; hidden source use; a changed COPY; +and incorrect source inventory. Normal and optimized runs retain the checks. + +The semantic native operator list is unchanged; no native operator replay, +complete caller, compiler, outer ledger, rounded error analysis, Lean or Docker +run is part of this result. In particular the retained caller's reserve is +not changed to 28 by this package. All five framework assumptions remain. +The rounded numerical equivalence of copying and subsequently scaling an +existing field is a separate implementation obligation. diff --git a/research/owned770-descent-pruning/README.md b/research/owned770-descent-pruning/README.md new file mode 100644 index 0000000000..37e5bd4ca2 --- /dev/null +++ b/research/owned770-descent-pruning/README.md @@ -0,0 +1,102 @@ +# Coalesce an owned P104 copy and save twelve scalar units + +This contribution was produced by Nick Petalas. Apache-2.0. + +A new exact word coalesces owned register 770 with its source register 791 in +DreamingOfClouds' [PR6144](https://github.com/CrocSwap/integer-mult-bounds/pull/6144) +word. After its last frame-549 read, 791 performs 770's continuation itself. +The duplicate INIT, COPY and CLEAR disappear. The public boundary and every +paid and productive rank remain unchanged. + +```text +Local scalar units 189658 -> 189646 +Events 22818 -> 22815 +Owned fields 29 -> 28 +Owned lifetimes 31 -> 30 +Peak live owned fields 13 -> 13 +``` + +This is a **finite exact circuit certificate and scoped substitution proof**. +There is no new kappa, strict peak-space reduction, supplier admission or +complete multiplication theorem. [PROOF.md](PROOF.md) gives the all-input +substitution argument, exact event anchors, prices and remaining obligations. + +The initial target was an interior descent-stage deletion, taking the +read-rerouting question of JosieElliston's +[PR6136](https://github.com/CrocSwap/integer-mult-bounds/pull/6136). +No paid-profile stage deletion was obtained. The first smaller improvement +was shipped instead. Frames 553 and 1047 remain in the substituted trajectory. +This changes owned lifetime identity, rather than repeating PR6136's chart-only +search or the earlier fixed-word scalar resynthesis. The complete cost profile +and boundary are retained, so no dependent construction expansion is proposed. + +## Reproduction + +From the repository root, with CPython 3.12 and no third-party packages: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -B research/owned770-descent-pruning/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -O -B research/owned770-descent-pruning/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/owned770-descent-pruning +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/owned770-descent-pruning --check-source-history +``` + +A clean `python3.12` may replace that local interpreter path. Direct output is +`PASS_OWNED_LIFETIME_COALESCENCE columns=798 coefficients=636804 controls=9 scalar_saved=12`. +The registered replay runs both ordinary and optimized checks. + +`construct.py` emits the complete word from the unchanged retained input. +The verifier checks all arbitrary-input endpoint and ownership conditions with +Ali Romman's unchanged main-branch checker, including a separate dense reverse +check. It enumerates every literal scalar price and paid rank, compares native +frame-boundary multisets, and rejects nine faults. `RESULT.json` is generated +by this verifier and binds all package files by SHA256. To regenerate a receipt +outside the checkout, pass `--receipt-out /absolute/scratch/RESULT.json`. + +The retained input is byte-identical to the PR6144 word at +`4f3b67e7c37ae270da9584033132866d0cf63e42`. +[PREDECESSOR.json](PREDECESSOR.json) records its original path, blob, size and +hash. It is retained in publication ancestry, so replay does not fetch an +unmerged commit or depend on a shared local object cache. The predecessor's +supplier result is cited; its verifier stack is not rerun as this contribution. + +## Limitations + +The edited word has 798 logical input columns because one owned coordinate is +removed; all 770 public inputs and their exact endpoints are retained. The +existing physical caller's conservative owned reserve is not reduced. Peak +occupancy remains thirteen. There are no new frame pairs, and the formal +native operators are unchanged after renaming, but their actual implementation +is not rerun. Caller/compiler/outer, rounded numerical analysis, the selected +cold replay, Lean and Docker are unrun. The five framework assumptions remain. +Independent human and formal proof-kernel review are unclaimed. + +This verifier uses bounded finite programs and managed Python allocation. +The input has 22818 events and 799 original role coordinates. Its largest dense +matrix has 798 by 798 entries. The one authenticated checker import is the only +dynamic import. These are explicit Python allocation and import deviations +from the Power of Ten rules. The existing frozen checker is unchanged. + +## Open next questions + +- Can a read-rerouting construction actually omit frame 553 or 1047 from this + trajectory? Start with the exact readers 169 and 206, preserve their other + meetings and price the complete changed route. Their current routes do not + permit a direct move to the neighboring owned frame. +- Can the actual caller use the reduced declared inventory? First bind its + alias allocation and lifetime schedule to the 28-field word. The unchanged + global peak and caller reserve prevent claiming physical memory savings here. +- Does a specified rounded implementation admit the same lifetime substitution + with a no-larger error budget? Bind actual COPY/SCALE and erasure semantics; + exact rational equality alone does not settle that numerical question. + +## Credit + +DreamingOfClouds supplies PR6144 and its owned-relay descent, extending that +author's PR6143, PR6030 and PR5907 words. Ali Romman supplies PR5827 and the +unchanged exact checker, building on Mason Hale's PR5811 and the P104 lineage +back through Pierre-Loic Doulcet's PR5565. JosieElliston supplies PR6136's +read-rerouting question. The native, helper, controller and framework +predecessors retain their original credit and notices. Last-read register +coalescence is a standard compiler technique. The contribution here is this +literal legal P104 substitution and its exact complete-word certificate. diff --git a/research/owned770-descent-pruning/RESULT.json b/research/owned770-descent-pruning/RESULT.json new file mode 100644 index 0000000000..849968c014 --- /dev/null +++ b/research/owned770-descent-pruning/RESULT.json @@ -0,0 +1,110 @@ +{ + "after": { + "events": { + "ADD": 18423, + "CLEAR": 30, + "COPY": 22, + "INIT": 30, + "MOVE": 3449, + "SCALE": 861 + }, + "paid": { + "1": 2215, + "2": 457, + "3": 496, + "4": 99, + "5": 164, + "6": 8, + "7": 9, + "8": 1 + }, + "scalar_units": 189646 + }, + "before": { + "events": { + "ADD": 18423, + "CLEAR": 31, + "COPY": 23, + "INIT": 31, + "MOVE": 3449, + "SCALE": 861 + }, + "paid": { + "1": 2215, + "2": 457, + "3": 496, + "4": 99, + "5": 164, + "6": 8, + "7": 9, + "8": 1 + }, + "scalar_units": 189658 + }, + "claim_type": "finite circuit certificate and scoped substitution proof", + "constructed_word_payload_sha256": "27039a0d408cafbe25b7b571dadcfb4f335faab8fab2d276aad1426530ef009a", + "edited_events": 22815, + "limits": [ + "No new kappa or paid-profile improvement.", + "Peak owned occupancy remains thirteen.", + "Rounded, native, physical caller and all-size admission are not replayed." + ], + "local": { + "endpoint_coefficients": 636804, + "helpers": { + "1": 14, + "2": 8, + "3": 4, + "4": 107, + "5": 14, + "6": 2, + "7": 9, + "8": 19, + "9": 385 + }, + "owned_fields": 28, + "owned_lifetimes": 30, + "paid": { + "1": 2215, + "2": 457, + "3": 496, + "4": 99, + "5": 164, + "6": 8, + "7": 9, + "8": 1 + }, + "paid_rank_mass": 5952, + "peak_owned_fields": 13, + "public_inputs": 770, + "real_scalar_allowance": 189646 + }, + "rejection_controls": { + "hidden_source_use": true, + "missing_clear": true, + "missing_descent": true, + "missing_first_read": true, + "missing_half": true, + "missing_source_init": true, + "wrong_copy_anchor": true, + "wrong_half_sign": true, + "wrong_inventory": true + }, + "source_hashes": { + "PREDECESSOR.json": "0e3124a5a565f9252c03bc0b66d890e20a4b93c8dd4f2214e50b47385fee7127", + "PROOF.md": "e0c32bcfa71ee2e21f258311935b5c7c243dd177f555f2ddc860fb2bcef2d105", + "README.md": "54776bf8039dfc2cb96e77cc5bde62d3eca8cbc0c6ac64f9a39d16a5813a5131", + "SOURCES.json": "d3790bfecd02d5d067ad4cae4d532e9e7f883944f12729c7dd0dbc11235cf31a", + "TASK.json": "75c1d3e8a0d98c4400c90b10caea28ae637069d73fde5f38117e6f8d935d913f", + "VERIFY.json": "3fd3ba5ce00eedc9a7377e0a773380068e9129e08ea0778f53bdae6ae825bb06", + "construct.py": "8f498c94e5ffd06b3a7aae5c36f7c47597ccf37ac9eba580ef998dbe905a1809", + "inputs/pr6144-WORD.json.gz": "c71985d96bf3d4a35aae111aaba87e376f7367efb4a5686278ef293732757533", + "verify.py": "df28f65652d4bf00ef7bd918b5a7cc10c2a6d3ef4e7a280875f42713112515e1" + }, + "status": "PASS_OWNED_LIFETIME_COALESCENCE", + "transpose": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 636804, + "columns": 798 + } +} diff --git a/research/owned770-descent-pruning/SOURCES.json b/research/owned770-descent-pruning/SOURCES.json new file mode 100644 index 0000000000..27e3832152 --- /dev/null +++ b/research/owned770-descent-pruning/SOURCES.json @@ -0,0 +1,38 @@ +{ + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "path": "certificates/selected-result.json", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa", + "usage": "provenance" + }, + { + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "path": "docs/research/agent-task-catalog.json", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81", + "usage": "provenance" + }, + { + "git_blob": "b7be846b10c4c54a4e1558d7b563bc8c3a170223", + "path": "research/p104-unread-path-resynthesis/local.py", + "sha256": "7201df8e32f5c99f7403150e8664042322037906088bc754c67293a241368597", + "usage": "input" + }, + { + "git_blob": "69b70ee50c697b185ebf585fbe69f2487af32d1d", + "path": "research/owned770-descent-pruning/inputs/pr6144-WORD.json.gz", + "pin": "head:61297e09be0725e6de603e0ec39b113ec6edb1cd:research/owned770-descent-pruning/inputs/pr6144-WORD.json.gz", + "sha256": "c71985d96bf3d4a35aae111aaba87e376f7367efb4a5686278ef293732757533", + "usage": "input" + }, + { + "git_blob": "25261ef2bae2f6da4441926965a353577636fb8d", + "path": "research/owned770-descent-pruning/PREDECESSOR.json", + "pin": "head:61297e09be0725e6de603e0ec39b113ec6edb1cd:research/owned770-descent-pruning/PREDECESSOR.json", + "sha256": "0e3124a5a565f9252c03bc0b66d890e20a4b93c8dd4f2214e50b47385fee7127", + "usage": "input" + } + ], + "schema_version": 1 +} diff --git a/research/owned770-descent-pruning/TASK.json b/research/owned770-descent-pruning/TASK.json new file mode 100644 index 0000000000..9596eba63b --- /dev/null +++ b/research/owned770-descent-pruning/TASK.json @@ -0,0 +1,129 @@ +{ + "actual_scope": "Coalesce old owned 770 with old owned 791 in the exact PR6144 word; remove one field, one lifetime, three events and twelve scalar units, preserving the full paid/productive profile.", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "author": "Nick Petalas", + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "bottleneck_link": "Scoped ordinary-work and logical-inventory improvement on a proposed P104 word. Every paid/native boundary and productive endpoint is retained; it is not a moment or kappa improvement.", + "budget_minutes": 60, + "evidence": "PROOF.md; RESULT.json; complete 798-column forward/reverse replay and nine rejection controls.", + "open_questions": [ + { + "blocked_by": "Chronological availability and the complete paid/caller bill.", + "first_step": "Bind readers 169 and 206 and their other meetings to a new legal trajectory.", + "question": "Can owned770 descent omit frame 553 or 1047 through actual read rerouting?", + "why_it_matters": "A strict paid-profile gain needs a different route, not just owned coalescence." + }, + { + "blocked_by": "Peak occupancy remains 13 and the current reserve is unchanged.", + "first_step": "Rebuild one caller alias allocation and compare all lifetimes.", + "question": "Can the actual caller reduce its declared reserve for the new 28-field word?", + "why_it_matters": "Logical inventory reduction does not reduce physical peak space by itself." + }, + { + "blocked_by": "A concrete numerical implementation and erasure contract.", + "first_step": "Price and bound the actual source SCALE and old COPY error.", + "question": "Can a specified rounded COPY/SCALE implementation use this substitution?", + "why_it_matters": "Exact rational equality need not preserve a rounded error bound." + } + ], + "original_card": { + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "existing_checks": [ + { + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4133: literal-slot defect", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "status": "author-checked" + }, + { + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4136: uniform commutation gap", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "status": "author-checked" + }, + { + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4140: uniform encoding gap", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "status": "author-checked" + }, + { + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "status": "author-checked" + }, + { + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4154: fiber-tag seam mismatch", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "status": "author-checked" + }, + { + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "status": "reviewed" + } + ], + "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "id": "p104-side-correction", + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "overlap_terms": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.md" + ] + }, + "outcome": "completed", + "priority_revision": 8, + "schema_version": 1, + "scope_change_reason": "Read-rerouting was proposed to remove an interior descent stage. The first verified improvement instead removes a duplicate owned COPY through last-read coalescence. No paid-profile gain was obtained.", + "scope_status": "changed", + "stop_rule": "Ship the first original verified improvement and list further work rather than extending it.", + "task_id": "p104-side-correction" +} diff --git a/research/owned770-descent-pruning/VERIFY.json b/research/owned770-descent-pruning/VERIFY.json new file mode 100644 index 0000000000..46ccb64762 --- /dev/null +++ b/research/owned770-descent-pruning/VERIFY.json @@ -0,0 +1,38 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-B", + "{package}/verify.py" + ], + "checks": "Exact coalesced-word endpoints/ownership, all 798 transpose columns, literal prices, unchanged native boundary list and nine rejection controls.", + "timeout_seconds": 120 + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "checks": "Exact coalesced-word endpoints/ownership, all 798 transpose columns, literal prices, unchanged native boundary list and nine rejection controls.", + "timeout_seconds": 120 + } + ], + "inputs": [ + "research/p104-unread-path-resynthesis/local.py", + "research/owned770-descent-pruning/inputs/pr6144-WORD.json.gz", + "research/owned770-descent-pruning/PREDECESSOR.json" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/owned770-descent-pruning/construct.py b/research/owned770-descent-pruning/construct.py new file mode 100644 index 0000000000..79376a3af4 --- /dev/null +++ b/research/owned770-descent-pruning/construct.py @@ -0,0 +1,61 @@ +"""Coalesce one exact P104 owned lifetime. Produced by Nick Petalas. Apache-2.0.""" +from copy import deepcopy + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def roles(event): + return event[1:3] if event[0] in ("ADD", "COPY") else event[1:2] + + +def compact(event): + """Delete old role 770 after replacing its uses by old role 791.""" + result = event.copy() + indices = (1, 2) if event[0] in ("ADD", "COPY") else (1,) + for index in indices: + value = 791 if result[index] == 770 else result[index] + result[index] = value - int(value > 770) + return result + + +def construct(source): + need(source["public"] == 770 and source["owned_fields"] == 29, + "Exact predecessor inventory") + program = source["program"] + need(len(program) == 22818, "Exact predecessor length") + anchors = { + 13473: ["INIT", 791, 549], + 13474: ["COPY", 791, 173, "1", 549], + 13475: ["ADD", 121, 791, "1/2", 549], + 13658: ["INIT", 770, 549], + 13659: ["COPY", 770, 791, "1", 549], + 13660: ["SCALE", 770, "1/2", 549], + 13661: ["MOVE", 770, 549, 553, True], + 15424: ["CLEAR", 770, 593], + 15591: ["CLEAR", 791, 549], + } + need(all(program[i] == event for i, event in anchors.items()), + "Exact coalescence anchors") + uses = [i for i, event in enumerate(program) if 791 in roles(event)] + need(uses == [13473, 13474, 13475, 13659, 15591], + "Source lifetime has no hidden use") + uses = [i for i, event in enumerate(program) if 770 in roles(event)] + need(uses[0] == 13658 and uses[-1] == 15424, + "Duplicate role has one enclosed lifetime") + need(sum(program[i][0] == "INIT" for i in uses) == 1, + "No second duplicate initialization") + output = [] + for index, event in enumerate(program): + if index in (13658, 13659, 13660, 15591): + continue + if index == 13661: + output.append(compact(["SCALE", 791, "1/2", 549])) + output.append(compact(event)) + result = deepcopy(source) + result["program"] = output + result["owned_fields"] = 28 + need(len(output) == 22815, "Exact edited length") + return result diff --git a/research/owned770-descent-pruning/inputs/pr6144-WORD.json.gz b/research/owned770-descent-pruning/inputs/pr6144-WORD.json.gz new file mode 100644 index 0000000000..69b70ee50c Binary files /dev/null and b/research/owned770-descent-pruning/inputs/pr6144-WORD.json.gz differ diff --git a/research/owned770-descent-pruning/verify.py b/research/owned770-descent-pruning/verify.py new file mode 100644 index 0000000000..0a8890332a --- /dev/null +++ b/research/owned770-descent-pruning/verify.py @@ -0,0 +1,154 @@ +"""Check the new coalesced word, not the predecessor's supplier claim. + +Produced by Nick Petalas. Apache-2.0. The imported checker retains its credit. +""" +import argparse +from collections import Counter +from copy import deepcopy +from fractions import Fraction +from hashlib import sha256 +import gzip +import importlib.util +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +from construct import construct, need + +CHECKER = "research/p104-unread-path-resynthesis/local.py" + + +def digest(path): + return sha256(path.read_bytes()).hexdigest() + + +def sources(): + pins = json.loads((HERE / "SOURCES.json").read_text()) + for pin in pins["files"]: + if pin["usage"] == "input": + need(digest(ROOT / pin["path"]) == pin["sha256"], "Source bytes: " + pin["path"]) + path = ROOT / CHECKER + spec = importlib.util.spec_from_file_location("owned_coalescence_checker", path) + need(spec is not None and spec.loader is not None, "Checker import specification") + checker = importlib.util.module_from_spec(spec) + spec.loader.exec_module(checker) + raw = (HERE / "inputs/pr6144-WORD.json.gz").read_bytes() + predecessor = json.loads((HERE / "PREDECESSOR.json").read_text()) + need(len(raw) == predecessor["size"] and sha256(raw).hexdigest() == predecessor["sha256"], + "Exact retained predecessor word") + return checker, json.loads(gzip.decompress(raw)) + + +def inventory(word): + """Count events and literal prices; no predecessor endpoint replay.""" + need(len(word["program"]) <= 26000, "Finite program bound") + scalar = 0 + paid = Counter() + events = Counter() + for event in word["program"]: + op = event[0] + events[op] += 1 + if op == "MOVE": + paid[abs(len(word["frames"][event[2]]) - len(word["frames"][event[3]]))] += 1 + elif op in ("INIT", "CLEAR"): + scalar += 2 + else: + q = Fraction(event[-2]) + n, d = abs(q.numerator), q.denominator + if op == "SCALE": + scalar += 2 * (abs(n.bit_length() - d.bit_length()) + int(q < 0)) + else: + scalar += 2 * (3 + n.bit_length() - 1 + n.bit_count() + d.bit_length() - 1) + return {"scalar_units": scalar, "paid": dict(sorted(paid.items())), + "events": dict(sorted(events.items()))} + + +def rejected(action): + try: + action() + except (ValueError, IndexError, KeyError): + return True + raise ValueError("Fault was accepted") + + +def controls(checker, source, word): + results = {} + sites = { + "missing_source_init": next(i for i, e in enumerate(word["program"]) if e == ["INIT", 790, 549]), + "missing_half": next(i for i, e in enumerate(word["program"]) if e == ["SCALE", 790, "1/2", 549]), + "missing_clear": next(i for i, e in enumerate(word["program"]) if e == ["CLEAR", 790, 593]), + "missing_descent": next(i for i, e in enumerate(word["program"]) if e == ["MOVE", 790, 549, 553, True]), + "missing_first_read": next(i for i, e in enumerate(word["program"]) if e == ["ADD", 169, 790, "-2", 553]), + } + for name, site in sites.items(): + bad = deepcopy(word) + bad["program"].pop(site) + results[name] = rejected(lambda: checker.replay(bad)) + bad = deepcopy(word) + bad["program"][sites["missing_half"]][2] = "-1/2" + results["wrong_half_sign"] = rejected(lambda: checker.replay(bad)) + bad = deepcopy(source) + bad["program"][14000] = ["ADD", 791, 770, "1", 549] + results["hidden_source_use"] = rejected(lambda: construct(bad)) + bad = deepcopy(source) + bad["program"][13659][3] = "2" + results["wrong_copy_anchor"] = rejected(lambda: construct(bad)) + bad = deepcopy(source) + bad["owned_fields"] = 28 + results["wrong_inventory"] = rejected(lambda: construct(bad)) + return results + + +def run(): + checker, source = sources() + word = construct(source) + before, after = inventory(source), inventory(word) + need(before["scalar_units"] == 189658 and after["scalar_units"] == 189646, + "Exactly twelve scalar units saved") + need(before["paid"] == after["paid"], "Every paid rank count preserved") + moves = lambda w: Counter(tuple(e[2:]) for e in w["program"] if e[0] == "MOVE") + need(moves(source) == moves(word), "Every signed native frame boundary preserved") + need(all(source[key] == word[key] for key in source if key not in ("program", "owned_fields")), + "Every public boundary and frame retained") + local = checker.replay(word) + columns = checker.reverse_columns(word) + need((local["owned_fields"], local["owned_lifetimes"], local["peak_owned_fields"]) == (28, 30, 13), + "New complete ownership inventory") + need(local["real_scalar_allowance"] == after["scalar_units"] and + local["paid"] == after["paid"], "Independent literal counts agree") + faults = controls(checker, source, word) + hashes = {str(p.relative_to(HERE)): digest(p) for p in sorted(HERE.rglob("*")) + if p.is_file() and p.name != "RESULT.json" and "__pycache__" not in p.parts} + word_hash = sha256(json.dumps(word, sort_keys=True, separators=(",", ":")).encode()).hexdigest() + return {"status": "PASS_OWNED_LIFETIME_COALESCENCE", "source_hashes": hashes, + "constructed_word_payload_sha256": word_hash, + "before": before, "after": after, "edited_events": len(word["program"]), + "local": local, "transpose": columns, "rejection_controls": faults, + "claim_type": "finite circuit certificate and scoped substitution proof", + "limits": ["No new kappa or paid-profile improvement.", + "Peak owned occupancy remains thirteen.", + "Rounded, native, physical caller and all-size admission are not replayed."]} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt-out", type=Path) + args = parser.parse_args() + result = run() + payload = (json.dumps(result, sort_keys=True, indent=2) + "\n").encode() + if args.receipt_out: + need(HERE not in args.receipt_out.resolve().parents, "Receipt output belongs outside the package") + args.receipt_out.write_bytes(payload) + else: + need((HERE / "RESULT.json").read_bytes() == payload, "Exact generated receipt") + columns = result["transpose"] + saved = result["before"]["scalar_units"] - result["after"]["scalar_units"] + print(result["status"], f"columns={columns['columns']} coefficients={columns['coefficients']}", + f"controls={len(result['rejection_controls'])} scalar_saved={saved}") + + +if __name__ == "__main__": + main()