diff --git a/research/p104-pr5718-leak-correction/README.md b/research/p104-pr5718-leak-correction/README.md new file mode 100644 index 0000000000..9b665157fe --- /dev/null +++ b/research/p104-pr5718-leak-correction/README.md @@ -0,0 +1,100 @@ +# No inserted carrier correction legalizes a PR5718-shape leak class on the PR6030 P104 word + +**Scoped exact result; no new κ.** Base: canonical main `a2b4b0395e293dded1cb17b4e78910b364af2343`; inputs rechecked unchanged at +`721c03822`. The selected record is unchanged by this package. + +Nick Petalas's [PR #6040](https://github.com/CrocSwap/integer-mult-bounds/pull/6040) (`shapesplit.py`, pinned +here as `inputs/shapesplit.py` from head `1889253f`) finds no PR5718-shape helper split on the PR5907 word. Every +candidate class either *leaks*, meaning the new helper's direction `d = S e_p` reaches a role whose final chart is +not `V`, or fails the pairing. It released step (3) of its claim: output corrections at later meetings. This +package takes that step. It runs on the merged +[PR #6030](https://github.com/CrocSwap/integer-mult-bounds/pull/6030) word (DreamingOfClouds, κ .003125804), which +became the selected word at main `721c03822` while this package was being prepared (the input bytes are unchanged), +and repeats the run on PR5907. + +## Result + +| Word | Leak classes | Carrier sources | Legalized by an inserted carrier correction | +|---|---:|---:|---:| +| PR6030 | 4,033 (390 leak to one role) | **0** | **0** | +| PR5907 | 4,206 (425 leak to one role) | **0** | **0** | + +On both words, no **single** inserted chart-local ADD or SCALE after the cut clears the defect outside `V`, in any +leak class. Neither does any correction program whose sources all lie along the defect direction. The PR6040 +suggestion `r += q·new` (a correction from a pure multiple of the new helper `z`) cannot clear a leak, with any +number of corrections. The z-part alone is easy to satisfy. That is why PR6040's z-only criterion is not a useful +filter once corrections are allowed. + +## Why (exact, from linearity) + +Fix a class: cut after event `i`, helper `p` at chart `F`, `V = final[p]`, `O` = roles whose final chart is not +`V`. Let `ℓ = row_p(i)·X` be the value the split retires. In the split word, field `f` holds +`orig_f(t) + β_f(t)(z − ℓ)` after event `t`. Here `β_f(t)` is the coefficient with which `p`'s cut content reaches +`f`. So the split outputs are `orig + d ⊗ (z − ℓ)`, and a legal split needs the **O-defect** `d_O ⊗ (z − ℓ)` removed +(with `z` still reaching a `V`-final output). Insert ADDs `r'_k += q_k f_k` after events `t_k`. The telescoping +identity for products gives the exact change: `Σ_k q_k S_{t_k} e_{r'_k} ⊗ (corrected value of f_k at t_k)`, where +`S` is the suffix map of the original word. Hence: + +1. **Pure-z sources never suffice.** They add only multiples of `z`, so the `−d_O ⊗ ℓ` part stays. `ℓ ≠ 0` in every + leak class (checked). On PR6030's leak-one classes, the z-part screen finds 124 classes it would pass (all + 4,033 classes, local run: 2,071 pass, 703 by one correction). The direct simulator (`check.py`) confirms for + three of them that the z-leak is cleared while the O output keeps a non-z defect. +2. **A single correction needs a carrier.** For `q v_O ⊗ value_f = −d_O ⊗ (z − ℓ)`, `v_O` must be proportional to + `d_O` and `value_f` to `z − ℓ`. That means `orig_f(t) = 0` with `β_f(t) ≠ 0`. A SCALE is the case `f = r'`. +3. **Carrier programs need a first carrier.** Corrections from carriers add multiples of `z − ℓ` and leave every + `orig_f` unchanged. So the first correction in time needs a carrier of the uncorrected word. + +The census (`leakfix.py`) tracks `β` for every leak class in one forward pass. It finds **no field, at any event +after any cut, that is zero in the original word while carrying the cut content**. Items 2 and 3 then exclude all +4,033 + 4,206 classes. The span machinery (one backward pass of suffix columns) decides the general carrier-source +equation `d_O + Σ μ_k (v_k)_O = 0` exactly over Q. It rejects solutions that erase `z` from every `V`-final output, +and it applies PR6040's pairing test to the corrected `d'_p`. + +**Positive control.** On the PR5713 word, a carrier and a leak are planted after PR5718's own cut (event 14330, +chart 602, helper 708): `INIT s; s += p | cut | s −= p; o += p` with `o = 128`. The class leaks to three roles. The +census finds the single correction `o += s` (μ = −1), and the independent simulator accepts it with no z-leak and no +non-z defect outside `V`. A doubled coefficient is rejected. + +## Reproduce + +Python 3.12, standard library, from the repository root (about 90 s): + +```sh +python3.12 -B research/p104-pr5718-leak-correction/verify.py +python3.12 -B scripts/research_package.py --package research/p104-pr5718-leak-correction +``` + +Marker: `PASS_P104_PR5718_LEAK_CORRECTION`. `--write` regenerates `RESULT.json`. Normal replay is read-only and +compares it byte for byte. The full pure-z screen over all PR6030 classes (`leakfix.run(w, mode='purez')`) takes +about 7 minutes. It is local-only evidence and is not in the verifier. + +A side check (local only, not in the verifier): Matarener's PR5994 `splitcensus.py` and PR6040's census on the +PR6030 word give 0 witnesses each (8,734 evaluations; group and boundary supports; both input rules). + +## Scope and limits + +- Scalar O-defect condition only, at the level of PR5994/PR6040: no `V` normalization legality beyond "z still + reaches `V`", and no native maps, owned lifetimes, caller, compiler, precision or outer checks. +- Covered edits: inserted chart-local ADD/SCALE events after the cut; programs of such events whose sources are all + carriers in the corrected word; any number of pure-z corrections. **Not covered:** several corrections with + non-carrier sources whose rank-one terms combine to `d_O ⊗ (z − ℓ)`; this includes several ADDs into one + target from fields whose combination is a carrier. Rewriting existing events, new MOVEs (paid), and injections + other than PR5718's unit injection `b = e_p` are also not covered. +- The census accepts only the PR6040 class list, so it inherits PR6040's input rule ('empty') and class definition. + +## Open next questions + +- **Combination carriers.** Is some combination of the fields at a chart zero in the original word but nonzero in + `β`, at some event after a cut? That would enable multi-ADD corrections. First step: for each event and touched + chart, test whether appending the `β` column raises the rank of the field rows. Blocked by speed: a direct + Fraction rank test did not finish a 1/50 class subsample in ten minutes. It needs incremental rank maintenance + per chart. +- **Edits that rewrite events.** Changing one existing ADD coefficient after the cut changes the original map and + falls outside the identity above. First step: allow one coefficient change and repeat the defect equation. + +## Credit + +Nick Petalas (PR6040 census and class definition, pinned unmodified), Matarener (PR5994 census and pure-subspace +decision), flyingviper (PR5718 split shape), Ali Romman (PR5599 split criterion) and DreamingOfClouds (PR5907 and +PR6030 words) retain credit; nothing of theirs is modified. Prepared for JosieElliston by Claude Opus 5.5 +(Anthropic) via Claude Code, as one session of an unattended overnight run; no human review. Apache-2.0. diff --git a/research/p104-pr5718-leak-correction/RESULT.json b/research/p104-pr5718-leak-correction/RESULT.json new file mode 100644 index 0000000000..bc32a3cad7 --- /dev/null +++ b/research/p104-pr5718-leak-correction/RESULT.json @@ -0,0 +1,296 @@ +{ + "planted_control": { + "class": { + "cut_after": 14332, + "frame": 602, + "kind": "witness", + "leak": 3, + "pivot": 708 + }, + "correction": { + "after_event": 14334, + "chart": 602, + "mu": "-1", + "source": 752, + "target": 128 + }, + "perturbed_rejected": true, + "z_leak_before": [ + 128, + 156, + 199 + ] + }, + "pr5907_carrier": { + "carrier_sources": 0, + "kinds": { + "unreachable": 4206 + }, + "leak_classes": 4206, + "leak_classes_by_leak_count": { + "1": 425, + "10": 104, + "102": 5, + "105": 3, + "11": 21, + "12": 28, + "14": 35, + "15": 78, + "16": 130, + "17": 18, + "18": 10, + "19": 30, + "2": 793, + "20": 47, + "21": 6, + "23": 14, + "24": 5, + "25": 11, + "26": 23, + "3": 84, + "30": 9, + "32": 10, + "33": 6, + "34": 6, + "35": 3, + "36": 7, + "37": 5, + "38": 3, + "4": 399, + "40": 8, + "42": 7, + "43": 6, + "44": 9, + "45": 31, + "46": 5, + "47": 11, + "49": 52, + "5": 28, + "50": 33, + "51": 121, + "52": 132, + "53": 157, + "54": 3, + "55": 7, + "56": 50, + "57": 56, + "58": 39, + "59": 35, + "6": 26, + "60": 28, + "61": 51, + "62": 16, + "63": 27, + "64": 29, + "65": 23, + "66": 14, + "67": 21, + "68": 34, + "69": 60, + "7": 43, + "70": 18, + "71": 53, + "72": 38, + "73": 3, + "74": 20, + "75": 157, + "76": 26, + "77": 86, + "78": 14, + "79": 19, + "8": 57, + "80": 21, + "81": 24, + "82": 6, + "83": 15, + "85": 13, + "86": 5, + "87": 12, + "88": 4, + "89": 27, + "9": 26, + "90": 25, + "91": 24, + "92": 12, + "94": 2, + "95": 15, + "97": 2, + "98": 2 + }, + "pr6040_counts": { + "evaluations": 8913, + "kind_leak": 4206, + "kind_pairing": 4, + "no_helper_prefix": 6374, + "pivots": 516, + "witnesses": 0 + } + }, + "pr6030_carrier": { + "carrier_sources": 0, + "kinds": { + "unreachable": 4033 + }, + "leak_classes": 4033, + "leak_classes_by_leak_count": { + "1": 390, + "10": 106, + "102": 5, + "105": 1, + "107": 2, + "11": 25, + "116": 2, + "117": 2, + "12": 31, + "14": 44, + "15": 68, + "16": 118, + "17": 16, + "18": 14, + "19": 36, + "2": 810, + "20": 50, + "21": 7, + "23": 13, + "24": 6, + "25": 11, + "26": 23, + "3": 83, + "30": 9, + "32": 10, + "33": 12, + "34": 4, + "35": 3, + "36": 10, + "37": 8, + "38": 4, + "4": 396, + "40": 8, + "42": 7, + "43": 4, + "44": 12, + "45": 22, + "46": 12, + "47": 13, + "49": 65, + "5": 28, + "50": 43, + "51": 117, + "52": 154, + "53": 153, + "55": 7, + "56": 52, + "57": 45, + "58": 35, + "59": 36, + "6": 27, + "60": 36, + "61": 57, + "62": 19, + "63": 28, + "64": 27, + "65": 19, + "66": 9, + "67": 25, + "68": 26, + "69": 54, + "7": 42, + "70": 16, + "71": 50, + "72": 30, + "74": 17, + "75": 73, + "76": 16, + "77": 39, + "78": 9, + "79": 16, + "8": 68, + "80": 16, + "81": 21, + "82": 2, + "83": 6, + "85": 18, + "87": 11, + "88": 1, + "89": 35, + "9": 27, + "90": 25, + "91": 12, + "92": 10, + "94": 2, + "95": 12 + }, + "pr6040_counts": { + "evaluations": 8734, + "kind_leak": 4033, + "kind_pairing": 4, + "no_helper_prefix": 6275, + "pivots": 516, + "witnesses": 0 + } + }, + "pr6030_purez_leak1": { + "classes": 390, + "demonstrations": [ + { + "O_nonz_defect_after": [ + 218 + ], + "correction": { + "after_event": 13741, + "chart": 1049, + "mu": "1", + "source": 681, + "target": 683 + }, + "cut_after": 13741, + "pivot": 681, + "z_leak_before": [ + 218 + ] + }, + { + "O_nonz_defect_after": [ + 153 + ], + "correction": { + "after_event": 14763, + "chart": 1049, + "mu": "1", + "source": 680, + "target": 685 + }, + "cut_after": 13747, + "pivot": 680, + "z_leak_before": [ + 153 + ] + }, + { + "O_nonz_defect_after": [ + 153 + ], + "correction": { + "after_event": 14763, + "chart": 1049, + "mu": "1", + "source": 680, + "target": 685 + }, + "cut_after": 13749, + "pivot": 680, + "z_leak_before": [ + 153 + ] + } + ], + "kinds": { + "erased": 17, + "pairing": 249, + "witness": 124 + }, + "single_and_pairing_witness": 51, + "single_corrections": 298 + }, + "schema": "p104-pr5718-leak-correction/v1" +} diff --git a/research/p104-pr5718-leak-correction/SOURCES.json b/research/p104-pr5718-leak-correction/SOURCES.json new file mode 100644 index 0000000000..8504d441ca --- /dev/null +++ b/research/p104-pr5718-leak-correction/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "a2b4b0395e293dded1cb17b4e78910b364af2343", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "usage": "input", + "sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f", + "git_blob": "22f9ab02d1b73ea0aa4b07ce445a14cc2602c760" + }, + { + "path": "research/p104-helper468-rung-removal/WORD.json.gz", + "usage": "input", + "sha256": "b69a9cb3a26d4f40aa7ad14f814b188fe16a782999f6f56292538e447d67b284", + "git_blob": "7ffe7b500b02b9d0de49a85ec53e36004f1a411f" + }, + { + "path": "research/p104-two-boundary-helper-split/inputs/pr5713-source.tar", + "usage": "input", + "sha256": "c4d8d0bcd6231eb4539a76d66b0dbd465313cbc50d279ca974a55fecb935d544", + "git_blob": "ec8f4bccaca147bc80cec078147fb95bc515036e" + } + ] +} diff --git a/research/p104-pr5718-leak-correction/TASK.json b/research/p104-pr5718-leak-correction/TASK.json new file mode 100644 index 0000000000..ced15ef8a7 --- /dev/null +++ b/research/p104-pr5718-leak-correction/TASK.json @@ -0,0 +1,123 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "a2b4b0395e293dded1cb17b4e78910b364af2343", + "original_card": { + "id": "p104-side-correction", + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "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" + ], + "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." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_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." + }, + "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.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "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." + ], + "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." + ], + "overlap_terms": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "existing_checks": [ + { + "scope": "PR #4133: literal-slot defect", + "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.", + "status": "author-checked", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4136: uniform commutation gap", + "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.", + "status": "author-checked", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4140: uniform encoding gap", + "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.", + "status": "author-checked", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "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.", + "status": "author-checked", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4154: fiber-tag seam mismatch", + "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.", + "status": "author-checked", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "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.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact scalar test, on the merged PR6030 P104 word (PR5907 for comparison), of mid-word corrections for every PR5718-shape leak class of the PR6040 census: inserted chart-local ADDs whose source is (a) a carrier, a field whose original value is zero while it carries the retired helper's cut content (its split value is a multiple of the full defect z - row_p), or (b) a pure multiple of the new helper z (PR6040's r += q*new).", + "scope_change_reason": "Takes PR6040's released step (3), output corrections at later meetings. Adds the non-z part that PR6040 left unmodelled: a pure-z correction clears the z-leak but leaves the defect -d_O x row_p on the original inputs, so the full defect direction must be corrected.", + "bottleneck_link": "Complex currently binds the selected assembly; a zero-paid helper split adds H_r+H_s-H_(r+s) per LOCAL to the productive side. This census says which split shapes remain possible on the latest conditional P104 word.", + "budget_minutes": 60, + "stop_rule": "Stop at one exact correction census with a planted positive control; do not build or price a split.", + "outcome": "completed", + "evidence": "verify.py: pinned inputs; class census equals PR6040's counts on both words; carrier mode: 0 carrier sources in all 4,033 PR6030 and 4,206 PR5907 leak classes; pure-z mode on the 390 PR6030 leak-1 classes: 124 z-part witnesses, three single corrections checked directly to clear the z-leak and leave a non-z O defect; planted carrier+leak on PR5713 at PR5718's cut is found and accepted by the direct simulator, perturbed coefficient rejected; RESULT.json compared.", + "author": "JosieElliston (session 33 of an overnight run)", + "ai_assistance": "Constructed and checked by Claude Opus 5.5 (Anthropic) via Claude Code; independent human and proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can several corrections with non-carrier sources combine to the rank-one defect d_O x (z - row_p) on O outputs?", + "why_it_matters": "This is the only correction route this package leaves open; a single correction or any carrier-source program is excluded on PR6030 and PR5907.", + "first_step": "For one leak-1 class, test at each later event and chart whether a combination of the fields there is zero in the original word but carries the cut content (rank of the field rows with the beta column appended).", + "blocked_by": "Speed: a direct Fraction rank test per event and class did not finish a 1/50 subsample in ten minutes; it needs incremental rank maintenance per chart." + }, + { + "question": "Does a correction that also rewrites an existing event (rather than inserting one) clear a leak class?", + "why_it_matters": "Inserted events are only one edit family; rewriting a coefficient changes the original map and is outside this test.", + "first_step": "Allow one existing ADD coefficient after the cut to change and repeat the defect equation.", + "blocked_by": "None." + } + ] +} \ No newline at end of file diff --git a/research/p104-pr5718-leak-correction/VERIFY.json b/research/p104-pr5718-leak-correction/VERIFY.json new file mode 100644 index 0000000000..5f7a312691 --- /dev/null +++ b/research/p104-pr5718-leak-correction/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "research/p104-helper468-rung-removal/WORD.json.gz", + "research/p104-two-boundary-helper-split/inputs/pr5713-source.tar" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Authenticate inputs and the pinned PR6040 census module; class census equals PR6040's counts on PR6030 and PR5907; no carrier source in any leak class on either word; pure-z screen on PR6030 leak-1 classes with three direct demonstrations of the remaining non-z defect; planted carrier/leak control on the PR5713 word found and directly accepted, perturbed coefficient rejected; RESULT.json compared byte for byte." + } + ] +} \ No newline at end of file diff --git a/research/p104-pr5718-leak-correction/check.py b/research/p104-pr5718-leak-correction/check.py new file mode 100644 index 0000000000..976d3fc360 --- /dev/null +++ b/research/p104-pr5718-leak-correction/check.py @@ -0,0 +1,77 @@ +"""Direct check of an explicit leak correction, independent of the suffix/telescoping algebra. Apache-2.0. + +Python 3.12, standard library only. Simulates the split word forward with one extra input coordinate 'z': +after event `cut`, field p holds z (unit injection); each correction (after_event t, target r', source f, mu) +inserts ADD r' += q f at the chart shared by r' and f, with q = mu / (z-coefficient of f), after checking that +f carries z (and, with pure_sources=True, that f's value is a pure multiple of z). Source eligibility otherwise +needs no check: check() validates the whole corrected map. Returns the final z-column over the public roles and the non-z rows. +""" +from fractions import Fraction as Q + + +def add(dst, src, q): + for k, v in src.items(): + x = dst.get(k, 0) + q * v + if x: + dst[k] = x + else: + dst.pop(k, None) + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def simulate(w, cut, p, corrections=(), pure_sources=False): + n = w['public']; m = w['owned_fields']; N = n + m + rows = [{r: Q(1)} if r < n else {} for r in range(N)] + cur = list(w['initial']) + [None] * m + by_t = {} + for c in corrections: + need(cut is not None and cut <= c['after_event'] < len(w['program']), 'correction inside the program, after the cut') + by_t.setdefault(c['after_event'], []).append(c) + for t, e in enumerate(w['program']): + op, r = e[0], e[1] + if op == 'MOVE': + need(cur[r] == e[2], 'MOVE from the current chart'); cur[r] = e[3] + elif op == 'INIT': + rows[r] = {}; cur[r] = e[2] + elif op == 'CLEAR': + rows[r] = {}; cur[r] = None + elif op == 'SCALE': + rows[r] = {k: v * Q(e[-2]) for k, v in rows[r].items()} + elif op == 'COPY': + need(cur[r] == cur[e[2]], 'COPY is chart-local'); rows[r] = {k: v * Q(e[-2]) for k, v in rows[e[2]].items()} + else: + need(cur[r] == cur[e[2]], 'ADD is chart-local'); add(rows[r], rows[e[2]], Q(e[-2])) + if cut is not None and t == cut: + rows[p] = {'z': Q(1)} + for c in by_t.get(t, ()): + f, r2 = c['source'], c['target'] + need(cur[f] is not None and cur[f] == cur[r2] == c['chart'], 'correction is chart-local') + need(rows[f].get('z'), 'correction source carries z') + need(not pure_sources or set(rows[f]) == {'z'}, 'correction source is a pure multiple of z') + q = Q(c['mu']) / rows[f]['z'] + add(rows[r2], dict(rows[f]), q) + zcol = {r: rows[r]['z'] for r in range(n) if rows[r].get('z')} + nonz = [{k: v for k, v in rows[r].items() if k != 'z'} for r in range(n)] + return zcol, nonz + + +def check(w, cut, p, corrections, full=True, pure_sources=False): + """Exact claims for one corrected split, with V = final[p] and O = roles whose final chart is not V: + z still reaches a V-final output; the z-column vanishes on O; and (full=True) every O output's non-z row equals + the ORIGINAL word's row, i.e. the split leaves no defect outside V. full=False checks only the z-part (the + PR6040 necessary condition). Returns a summary; raises ValueError on failure.""" + V = w['final'][p]; n = w['public'] + O = [r for r in range(n) if w['final'][r] != V] + _, orig = simulate(w, None, p) + z0, nz0 = simulate(w, cut, p) + z1, nz1 = simulate(w, cut, p, corrections, pure_sources) + need(bool({r for r in z1 if w['final'][r] == V}), 'z still reaches a V-final output') + need(all(r not in z1 for r in O), 'no z-leak to a role whose final chart is not V') + defect = [r for r in O if nz1[r] != orig[r]] + if full: + need(not defect, 'no non-z defect on O outputs') + return {'z_leak_before': sorted(r for r in z0 if r in set(O)), 'O_nonz_defect_after': defect} diff --git a/research/p104-pr5718-leak-correction/inputs/shapesplit.py b/research/p104-pr5718-leak-correction/inputs/shapesplit.py new file mode 100644 index 0000000000..6eedc849e7 --- /dev/null +++ b/research/p104-pr5718-leak-correction/inputs/shapesplit.py @@ -0,0 +1,176 @@ +"""Exact census of PR5718-shape helper splits on a P104 word. Apache-2.0. Python 3.12, standard library only. + +Prepared by Nick Petalas. Extends the criterion and pure-subspace decision of Matarener's PR5994 census +(`research/p104-helper-split-exhaustion`, PR5599 PROOF.md section 1) to the shape of flyingviper's PR5718 split. + +Model (one helper p of a boundary group g = (U, V), cut after event i, strictly intermediate chart F holding p): + * input side: a combination a of the prefix rows of the fields at F with a_p != 0 and c = aP supported on the + group, on roles whose initial chart is U, or (in_kind='empty', PR5718's rule) on every role whose initial chart + is zero-dimensional; + * a new independent helper z replaces p after the cut (unit injection b = e_p, as in PR5718); its z-direction + reaches the outputs as d = S e_p (S = suffix columns of the original word); + * output normalisation only at V: every role whose final chart is V (other than p) may be corrected freely, so d + must vanish on O = {roles whose final chart is not V}; the pair needs a.b = c.d' != 0. +Classes whose d leaks into O are reported as `leak`: such a split needs a mid-word correction of that leak. +""" +from collections import defaultdict +from fractions import Fraction as Q +import gzip, json + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def read(path): + raw = open(path, 'rb').read() + return json.loads(gzip.decompress(raw) if str(path).endswith('.gz') else raw) + + +def spans(w): + out = [] + for basis in w['frames']: + s = {0} + for v in basis: + need(type(v) is int and 0 < v < 512 and v not in s, 'independent binary basis') + s |= {x ^ v for x in s} + out.append(frozenset(s)) + return out + + +def add(dst, src, q): + for k, v in src.items(): + x = dst.get(k, 0) + q * v + if x: + dst[k] = x + else: + dst.pop(k, None) + + +def groups_of(w): + n = w['public']; main = set(w['live']) | {r + 112 for r in w['live']} + g = defaultdict(set) + for r in range(n): + if r not in main: + g[(w['initial'][r], w['final'][r])].add(r) + return g + + +def pure_subspace(vecs, roles, support): + """Basis of {x : sum x_r vecs[r] supported in `support`} as (coefficients, image) pairs; kernel vectors included.""" + pivots, out = [], [] + for r in roles: + outside = {k: v for k, v in vecs[r].items() if k not in support} + coef = {r: Q(1)} + for key, prow, pcoef in pivots: + if key in outside: + s = -outside[key]; add(outside, prow, s); add(coef, pcoef, s) + if outside: + key = min(outside); s = 1 / outside[key] + pivots.append((key, {k: v * s for k, v in outside.items()}, {k: v * s for k, v in coef.items()})) + else: + img = {} + for x, q in coef.items(): + add(img, vecs[x], q) + out.append((coef, img)) + return out + + +def functional_witness(A, p, free, rho): + """Exact decision over the span of A. With L1 = a_p, L2 = c_p, L3 = c on the free coordinates and rho = d_p, a + split exists iff some a has L1 != 0 and (L3 != 0 or L1 = rho * L2): free coordinates of d' adjust c.d' at will, + otherwise c.d' = rho * c_p must equal a.b = a_p.""" + L1 = [coef.get(p, Q(0)) for coef, img in A] + L2 = [img.get(p, Q(0)) for coef, img in A] + L3 = [{k: v for k, v in img.items() if k in free} for coef, img in A] + if not any(L1): + return False + if any(L3): + return True + M = [L1[k] - rho * L2[k] for k in range(len(A))] # is L1 nonzero on ker M ? + if not any(M): + return True + j = next(k for k in range(len(A)) if M[k]) + return any(L1[k] * M[j] - L1[j] * M[k] for k in range(len(A))) + + +def census(w, in_kind='empty'): + """Returns (counts, classes). in_kind: 'boundary' (group + roles initial at U) or 'empty' (also every role + initial at a zero-dimensional chart).""" + n = w['public']; m = w.get('owned_fields', max(e[1] for e in w['program']) + 1 - n); N = n + m + prog = w['program']; S = spans(w); dims = [len(f) for f in w['frames']] + groups = groups_of(w) + valid = {g: {f for f in range(len(S)) if S[g[0]] < S[f] < S[g[1]]} for g in groups} + insup = {} + for g, rs in groups.items(): + s = set(rs) | {r for r in range(n) if w['initial'][r] == g[0]} + if in_kind == 'empty': + s |= {r for r in range(n) if dims[w['initial'][r]] == 0} + insup[g] = s + rows = [{r: Q(1)} if r < n else {} for r in range(N)] + cur = list(w['initial']) + [None] * m + at = defaultdict(set) + for r in range(n): + at[cur[r]].add(r) + snaps = defaultdict(list); counts = defaultdict(int) + for i, e in enumerate(prog): + op, r = e[0], e[1] + if op == 'MOVE': + at[e[2]].discard(r); at[e[3]].add(r); cur[r] = e[3]; touched = (e[2], e[3]) + elif op == 'INIT': + rows[r] = {}; cur[r] = e[2]; at[e[2]].add(r); touched = (e[2],) + elif op == 'CLEAR': + rows[r] = {}; at[e[2]].discard(r); cur[r] = None; touched = (e[2],) + elif op == 'SCALE': + rows[r] = {k: v * Q(e[-2]) for k, v in rows[r].items()}; touched = (cur[r],) + elif op == 'COPY': + rows[r] = {k: v * Q(e[-2]) for k, v in rows[e[2]].items()}; touched = (cur[r],) + else: + add(rows[r], rows[e[2]], Q(e[-2])); touched = (cur[r],) + for F in set(touched): + if F is None or not at[F]: + continue + roles = sorted(at[F]) + for g in groups: + if F not in valid[g] or not (groups[g] & at[F]): + continue + counts['evaluations'] += 1 + A = pure_subspace(rows, roles, insup[g]) + hp = [p for p in sorted(groups[g] & at[F]) if any(coef.get(p) for coef, img in A)] + if not any(img for coef, img in A) or not hp: + counts['no_helper_prefix'] += 1 + continue + snaps[i].append((F, g, hp, A)) + pivots = {p for v in snaps.values() for (F, g, hp, A) in v for p in hp} + fin = {p: w['final'][p] for p in pivots} + outside = {p: {r for r in range(n) if w['final'][r] != fin[p]} for p in pivots} + keep = {p: outside[p] | {p} for p in pivots} + cols = [{r: Q(1)} if r < n else {} for r in range(N)] + classes = [] + for i in range(len(prog) - 1, -1, -1): + for (F, g, hp, A) in snaps.get(i, []): + for p in hp: + d = {k: x for k, x in cols[p].items() if k in keep[p]} + leak = sum(1 for k in d if k in outside[p]) + if leak: + counts['kind_leak'] += 1 + kind = 'leak' + else: + free = {r for r in range(n) if r not in keep[p]} + kind = 'witness' if functional_witness(A, p, free, d.get(p, Q(0))) else 'pairing' + counts['kind_' + kind] += 1 + classes.append({'cut_after': i, 'frame': F, 'group': list(g), 'pivot': p, + 'ranks': [dims[F] - dims[g[0]], dims[g[1]] - dims[F]], 'kind': kind, 'leak': leak}) + e = prog[i]; op, r = e[0], e[1] + if op in ('INIT', 'CLEAR'): + cols[r] = {} + elif op == 'COPY': + add(cols[e[2]], cols[r], Q(e[-2])); cols[r] = {} + elif op == 'SCALE': + cols[r] = {k: v * Q(e[-2]) for k, v in cols[r].items()} + elif op == 'ADD': + add(cols[e[2]], cols[r], Q(e[-2])) + counts['witnesses'] = sum(1 for c in classes if c['kind'] == 'witness') + counts['pivots'] = len(pivots) + return dict(counts), sorted(classes, key=lambda c: (c['cut_after'], c['frame'], c['pivot'])) diff --git a/research/p104-pr5718-leak-correction/leakfix.py b/research/p104-pr5718-leak-correction/leakfix.py new file mode 100644 index 0000000000..c54c16899a --- /dev/null +++ b/research/p104-pr5718-leak-correction/leakfix.py @@ -0,0 +1,377 @@ +"""Exact test of mid-word corrections for PR5718-shape helper-split leak classes. Apache-2.0. + +Python 3.12, standard library only. Extends Nick Petalas's PR6040 census (`inputs/shapesplit.py`, pinned), which +builds on Matarener's PR5994 census and flyingviper's PR5718 split shape. + +Setting (PR6040). A class is (cut after event i, chart F, helper p of a boundary group (U, V)). A new independent +helper z replaces p after the cut; its output column is d = S_i e_p (S = suffix columns of the original word). The +class "leaks" when d is nonzero on O = {public roles whose final chart is not V}. + +Corrections. Insert chart-local events ADD r' += q f after an event t >= i, where f is a field whose value in +the split word is a pure multiple of z (zero non-z part), and r' is any field at the same chart at time t. By the +product telescoping identity prod(I+D_k)A - prod A = sum_k (orig suffix after t_k) D_k (corrected state at t_k), +and because such an ADD only adds multiples of z (so every non-z part is unchanged), the corrected z-column is + + d' = d + sum_k mu_k v_k, v_k = S_{t_k} e_{r'_k} (suffix column of the ORIGINAL word), + +with mu_k = q_k * (z-coefficient of f_k at t_k in the corrected word). The non-z columns of the word are unchanged. +The non-z part of f in the split word is row_f(t) - zc_f(t) * row_p(i), where zc_f(t) is the coefficient with +which the content of field p at the cut reaches f at t (by linearity, the original word is the split word with +z := row_p(i)). Hence: + + * first-order sources: fields with zero non-z part and zc != 0 in the uncorrected split word; each correction + from such a source can take any mu (corrections in time order, each q chosen after the earlier ones); + * necessary superset: also fields whose whole split-word value is zero (zc = 0, row = 0), which can only carry z + after an earlier correction wrote into them. Any correction program whose sources are pure-z fields has its + v_k inside this superset span. + +Decision per class: is d_O in -span{(v_k)_O}? If so, the pairing of PR6040 (functional_witness) is tested with +rho = d'_p, which is either fixed by the solution or free (when a combination with zero O-part moves the p +coordinate). 'single' = one correction suffices (some v_O proportional to d_O). + +Scope: the z-part necessary condition of PR6040 only. Corrections whose source carries non-z content, the non-z +part of the split normalization, native maps, caller, compiler and outer checks are not modelled. +""" +from collections import defaultdict +from fractions import Fraction as Q +import importlib.util, sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def _load_shapesplit(): + name = 'pr6040_shapesplit' + if name in sys.modules: + return sys.modules[name] + spec = importlib.util.spec_from_file_location(name, HERE/'inputs'/'shapesplit.py') + mod = importlib.util.module_from_spec(spec); sys.modules[name] = mod; spec.loader.exec_module(mod) + return mod + + +SS = _load_shapesplit() +add, need = SS.add, SS.need + + +def leak_classes(w, in_kind='empty'): + """Re-run the PR6040 forward/backward census, keeping for each class its A, d (full column) and row_p(i). + Returns (classes, counts); counts must equal SS.census(w, in_kind)[0].""" + n = w['public']; m = w.get('owned_fields', max(e[1] for e in w['program']) + 1 - n); N = n + m + prog = w['program']; S = SS.spans(w); dims = [len(f) for f in w['frames']] + groups = SS.groups_of(w) + valid = {g: {f for f in range(len(S)) if S[g[0]] < S[f] < S[g[1]]} for g in groups} + insup = {} + for g, rs in groups.items(): + s = set(rs) | {r for r in range(n) if w['initial'][r] == g[0]} + if in_kind == 'empty': + s |= {r for r in range(n) if dims[w['initial'][r]] == 0} + insup[g] = s + rows = [{r: Q(1)} if r < n else {} for r in range(N)] + cur = list(w['initial']) + [None] * m + at = defaultdict(set) + for r in range(n): + at[cur[r]].add(r) + snaps = defaultdict(list); counts = defaultdict(int) + for i, e in enumerate(prog): + op, r = e[0], e[1] + if op == 'MOVE': + at[e[2]].discard(r); at[e[3]].add(r); cur[r] = e[3]; touched = (e[2], e[3]) + elif op == 'INIT': + rows[r] = {}; cur[r] = e[2]; at[e[2]].add(r); touched = (e[2],) + elif op == 'CLEAR': + rows[r] = {}; at[e[2]].discard(r); cur[r] = None; touched = (e[2],) + elif op == 'SCALE': + rows[r] = {k: v * Q(e[-2]) for k, v in rows[r].items()}; touched = (cur[r],) + elif op == 'COPY': + rows[r] = {k: v * Q(e[-2]) for k, v in rows[e[2]].items()}; touched = (cur[r],) + else: + add(rows[r], rows[e[2]], Q(e[-2])); touched = (cur[r],) + for F in set(touched): + if F is None or not at[F]: + continue + roles = sorted(at[F]) + for g in groups: + if F not in valid[g] or not (groups[g] & at[F]): + continue + counts['evaluations'] += 1 + A = SS.pure_subspace(rows, roles, insup[g]) + hp = [p for p in sorted(groups[g] & at[F]) if any(coef.get(p) for coef, img in A)] + if not any(img for coef, img in A) or not hp: + counts['no_helper_prefix'] += 1 + continue + snaps[i].append((F, g, hp, A, {p: dict(rows[p]) for p in hp})) + pivots = {p for v in snaps.values() for (F, g, hp, A, rp) in v for p in hp} + fin = {p: w['final'][p] for p in pivots} + outside = {p: {r for r in range(n) if w['final'][r] != fin[p]} for p in pivots} + keep = {p: outside[p] | {p} for p in pivots} + cols = [{r: Q(1)} if r < n else {} for r in range(N)] + classes = [] + for i in range(len(prog) - 1, -1, -1): + for (F, g, hp, A, rp) in snaps.get(i, []): + for p in hp: + d = {k: x for k, x in cols[p].items() if k in keep[p]} + leak = sum(1 for k in d if k in outside[p]) + free = {r for r in range(n) if r not in keep[p]} + if leak: + counts['kind_leak'] += 1; kind = 'leak' + else: + kind = 'witness' if SS.functional_witness(A, p, free, d.get(p, Q(0))) else 'pairing' + counts['kind_' + kind] += 1 + classes.append({'cut_after': i, 'frame': F, 'group': g, 'pivot': p, 'kind': kind, 'leak': leak, + 'ranks': [dims[F] - dims[g[0]], dims[g[1]] - dims[F]], + 'A': A, 'd': d, 'dall': dict(cols[p]), 'row_p': rp[p], 'outside': outside[p], 'free': free}) + e = prog[i]; op, r = e[0], e[1] + if op in ('INIT', 'CLEAR'): + cols[r] = {} + elif op == 'COPY': + add(cols[e[2]], cols[r], Q(e[-2])); cols[r] = {} + elif op == 'SCALE': + cols[r] = {k: v * Q(e[-2]) for k, v in cols[r].items()} + elif op == 'ADD': + add(cols[e[2]], cols[r], Q(e[-2])) + counts['witnesses'] = sum(1 for c in classes if c['kind'] == 'witness') + counts['pivots'] = len(pivots) + classes.sort(key=lambda c: (c['cut_after'], c['frame'], c['pivot'])) + return classes, dict(counts) + + +def source_intervals(w, cuts, superset=False, mode='carrier'): + """For each (cut i, pivot p) in `cuts` -> list of (field f, chart X, t0, t1): f has zero non-z part in the split + word at chart X after every event t in [t0, t1], and (unless superset) a nonzero z-coefficient. + One shared forward pass over the original word; z-coefficients zc are tracked per (i, p).""" + n = w['public']; m = w.get('owned_fields', max(e[1] for e in w['program']) + 1 - n); N = n + m + prog = w['program'] + rows = [{r: Q(1)} if r < n else {} for r in range(N)] + cur = list(w['initial']) + [None] * m + starts = defaultdict(list) + for key in cuts: + starts[key[0]].append(key) + zc = {} # key -> {field: coefficient} + rowp = {} # key -> row_p(i) + holders = defaultdict(set) # field -> keys with zc[key][field] != 0 + opened = {} # key -> {field: (chart, t0)} + out = defaultdict(list) + + def pure(key, f): + c = zc[key].get(f, 0) + if c == 0: + return superset and not rows[f] and cur[f] is not None + if mode == 'carrier': # original value zero: split value = c * (z - row_p(i)) + return not rows[f] + rp = rowp[key] + if len(rows[f]) != len(rp): + return False + return all(rows[f].get(k) == c * v for k, v in rp.items()) + + def refresh(key, f, t): + """Update the open interval of f for key after event t.""" + o = opened[key] + if f in o: + X, t0 = o[f] + if not pure(key, f) or cur[f] != X: + out[key].append((f, X, t0, t - 1)); del o[f] + if f not in o and cur[f] is not None and pure(key, f): + o[f] = (cur[f], t) + + for t, e in enumerate(prog): + op, r = e[0], e[1] + changed = {r} + if op == 'MOVE': + cur[r] = e[3] + elif op == 'INIT': + rows[r] = {}; cur[r] = e[2] + elif op == 'CLEAR': + rows[r] = {}; cur[r] = None + elif op == 'SCALE': + rows[r] = {k: v * Q(e[-2]) for k, v in rows[r].items()} + elif op == 'COPY': + rows[r] = {k: v * Q(e[-2]) for k, v in rows[e[2]].items()} + else: + add(rows[r], rows[e[2]], Q(e[-2])) + # z-coefficient propagation, same linear action on the scalar zc[key][*] + aff = set(holders.get(r, ())) + if op in ('ADD', 'COPY'): + aff |= holders.get(e[2], set()) + for key in aff: + z = zc[key]; old = z.get(r, 0) + if op in ('INIT', 'CLEAR'): + new = 0 + elif op == 'SCALE': + new = old * Q(e[-2]) + elif op == 'COPY': + new = Q(e[-2]) * z.get(e[2], 0) + elif op == 'ADD': + new = old + Q(e[-2]) * z.get(e[2], 0) + else: + new = old + if new: + z[r] = new; holders[r].add(key) + else: + z.pop(r, None); holders[r].discard(key) + # interval bookkeeping for keys whose purity of r may have changed + check = aff if not superset else set(opened) + for key in check: + refresh(key, r, t) + # new cuts start after event t + for key in starts.get(t, ()): + i, p = key + zc[key] = {p: Q(1)}; holders[p].add(key); rowp[key] = dict(rows[p]); opened[key] = {} + if superset: + for f in range(N): + if cur[f] is not None and not rows[f] and f != p: + opened[key][f] = (cur[f], t) + refresh(key, p, t) + T = len(prog) - 1 + for key, o in opened.items(): + for f, (X, t0) in o.items(): + out[key].append((f, X, t0, T)) + return out + + +class Span: + """Incremental exact row-echelon basis over Q for sparse dict vectors; coordinate order given by `order`.""" + def __init__(self, order): + self.rank = {k: j for j, k in enumerate(order)} + self.piv = {} # pivot coordinate -> normalized vector + + def reduce(self, v): + v = dict(v) + while v: + k = min(v, key=self.rank.__getitem__) + if k not in self.piv: + return v, k + add(v, self.piv[k], -v[k]) + return v, None + + def insert(self, v): + v, k = self.reduce(v) + if k is None: + return False + s = 1 / v[k] + self.piv[k] = {x: y * s for x, y in v.items()} + return True + + +def correction_spans(w, classes, intervals): + """One backward pass. For every class, the span of v = S_t e_{r'} restricted to O + {p}, over insertion times t + in a source interval and r' at the source's chart. Also flags a single-correction (v_O proportional to d_O).""" + n = w['public']; m = w.get('owned_fields', max(e[1] for e in w['program']) + 1 - n); N = n + m + prog = w['program'] + # chart membership after each event, reconstructed forward then walked backward + cur = list(w['initial']) + [None] * m + for e in prog: + if e[0] == 'MOVE': cur[e[1]] = e[3] + elif e[0] == 'INIT': cur[e[1]] = e[2] + elif e[0] == 'CLEAR': cur[e[1]] = None + at = defaultdict(set) + for f in range(N): + if cur[f] is not None: + at[cur[f]].add(f) + byclass = {} + active_at = defaultdict(list) # t1 -> list of (class index, f, X, t0) + for ci, c in enumerate(classes): + key = (c['cut_after'], c['pivot']) + O = c['outside']; p = c['pivot'] + order = sorted(O) + sorted(r for r in range(n) if r not in O) + byclass[ci] = {'span': Span(order), 'seen': set(), 'single': None, 'n_vectors': 0, 'O': O, + 'dO': {k: x for k, x in c['d'].items() if k in O}, 'd': c['dall']} + for (f, X, t0, t1) in intervals.get(key, ()): + active_at[t1].append((ci, f, X, t0)) + live = [] # currently open (ci, f, X, t0) + version = [0] * N + cols = [{r: Q(1)} if r < n else {} for r in range(N)] + for t in range(len(prog) - 1, -1, -1): + # state: cols = suffix after event t, membership = after event t + live.extend(active_at.get(t, ())) + still = [] + for item in live: + ci, f, X, t0 = item + if t < t0: + continue + still.append(item) + B = byclass[ci] + for r2 in at[X]: + tag = (r2, version[r2]) + if tag in B['seen']: + continue + B['seen'].add(tag) + v = cols[r2] + if not v: + continue + B['n_vectors'] += 1 + O = B['O']; vO = {k: x for k, x in v.items() if k in O} + dO = B['dO'] + if B['single'] is None and vO and set(vO) == set(dO): + k0 = next(iter(dO)); s = -dO[k0] / vO[k0] + if all(dO[k] + s * vO[k] == 0 for k in dO): + rest = dict(B['d']); add(rest, v, s) + if rest: # z must still reach a V-final role (no erasure of the new helper) + B['single'] = {'after_event': t, 'target': r2, 'source': f, 'chart': X, 'mu': str(s)} + B['span'].insert(v) + live = still + e = prog[t]; op, r = e[0], e[1] + # reverse membership of event t + if op == 'MOVE': + at[e[3]].discard(r); at[e[2]].add(r) + elif op == 'INIT': + at[e[2]].discard(r) + elif op == 'CLEAR': + at[e[2]].add(r) + # suffix columns before event t + if op in ('INIT', 'CLEAR'): + cols[r] = {}; version[r] += 1 + elif op == 'COPY': + add(cols[e[2]], cols[r], Q(e[-2])); cols[r] = {}; version[r] += 1; version[e[2]] += 1 + elif op == 'SCALE': + cols[r] = {k: v * Q(e[-2]) for k, v in cols[r].items()}; version[r] += 1 + elif op == 'ADD': + add(cols[e[2]], cols[r], Q(e[-2])); version[e[2]] += 1 + return byclass + + +def decide(c, B): + """Return (kind, rho) for one leak class. 'unreachable': no correction combination clears d on O; + 'erased': only by removing z from every V-final output (the new helper would have no target); otherwise the + PR6040 pairing outcome ('witness' / 'pairing') with rho = d'_p fixed or 'free'.""" + p = c['pivot']; O = c['outside']; sp = B['span'] + r, k = sp.reduce(c['dall']) # O coordinates come first in the elimination order + if k is not None and k in O: + return 'unreachable', None + W = [v for piv, v in sp.piv.items() if piv not in O] # zero O-part: free moves of d' on V-final roles + if not r and not W: + return 'erased', None + rho_free = any(v.get(p) for v in W) + A = c['A']; free = c['free'] + if rho_free: + L1 = [coef.get(p, Q(0)) for coef, img in A] + L2 = [img.get(p, Q(0)) for coef, img in A] + L3 = [{k2: v for k2, v in img.items() if k2 in free} for coef, img in A] + ok = any(L1) and (any(L3) or any(L2)) + return ('witness' if ok else 'pairing'), 'free' + rho = r.get(p, Q(0)) + if not any(v for v in W) and not {x for x in r if x != p} and rho == 0: + return 'erased', None + return ('witness' if SS.functional_witness(A, p, free, rho) else 'pairing'), str(rho) + + +def run(w, in_kind='empty', superset=False, only_leak=True, mode='carrier', select=None): + """mode 'carrier': sources whose ORIGINAL value is zero while carrying p's cut content (their split value is a + multiple of z - row_p(i), the full defect direction); mode 'purez': sources whose split value is a multiple of z + (PR6040's suggested r += q*new; fixes only the z-part).""" + classes, counts = leak_classes(w, in_kind) + todo = [c for c in classes if c['kind'] == 'leak'] if only_leak else classes + if select: + todo = [c for c in todo if select(c)] + cuts = sorted({(c['cut_after'], c['pivot']) for c in todo}) + iv = source_intervals(w, cuts, superset, mode) + spans = correction_spans(w, todo, iv) + res = [] + for ci, c in enumerate(todo): + B = spans[ci] + kind, rho = decide(c, B) + res.append({'cut_after': c['cut_after'], 'frame': c['frame'], 'pivot': c['pivot'], 'group': list(c['group']), + 'ranks': c['ranks'], 'leak': c['leak'], 'sources': len(iv.get((c['cut_after'], c['pivot']), ())), + 'vectors': B['n_vectors'], 'span_rank': len(B['span'].piv), 'kind': kind, 'rho': rho, + 'single': B['single']}) + return counts, res, iv + diff --git a/research/p104-pr5718-leak-correction/verify.py b/research/p104-pr5718-leak-correction/verify.py new file mode 100644 index 0000000000..321062519a --- /dev/null +++ b/research/p104-pr5718-leak-correction/verify.py @@ -0,0 +1,132 @@ +#!/usr/bin/env python3 +"""Verify the mid-word leak-correction census on the PR6030 and PR5907 P104 words. Apache-2.0. + +Python 3.12, standard library only. Checks: + (0) pinned input bytes (the PR6040 census module and the three words); + (1) the re-run class census equals PR6040's own census counts on both words; + (2) every leak class has a nonzero retired value row_p(i); carrier mode: on both words no leak class has a single carrier source (a field whose original value is zero + while carrying the pivot's cut content), so every leak class is 'unreachable' by carrier corrections; + (3) the z-part-only screen (PR6040's r += q*new) on the PR6030 leak-1 classes: it reports z-part witnesses, and + the direct simulator confirms for the first three single corrections that the z-leak is cleared while a non-z + defect remains on an O output (the exact lemma in README.md); + (4) planted positive control on the PR5713 word: a carrier and a leak planted after PR5718's own split cut; carrier + mode finds the single correction and the direct simulator accepts it with no defect outside V; a perturbed + coefficient is rejected; + (5) RESULT.json equals the recomputed receipt. +""" +from collections import Counter +from hashlib import sha256 +from pathlib import Path +import gzip, io, json, sys, tarfile, time + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SHAPESPLIT_SHA256 = '11e8ef691b28fb4f401a8c2e97b6d462e7a004f0e215a28579d6a654b4ca3304' # PR6040 head 1889253f, git blob 6eedc849 +if sha256((HERE/'inputs'/'shapesplit.py').read_bytes()).hexdigest() != SHAPESPLIT_SHA256: + raise SystemExit('pinned PR6040 shapesplit.py does not match') # checked before any imported code runs +sys.path.insert(0, str(HERE)) +import leakfix as L # noqa: E402 +import check as K # noqa: E402 + +W6030 = 'research/p104-helper470-twin-rung-removal/WORD.json.gz' +W5907 = 'research/p104-helper468-rung-removal/WORD.json.gz' +TAR5713 = 'research/p104-two-boundary-helper-split/inputs/pr5713-source.tar' +MEMBER5713 = 'research/p104-temporal-updates/WORD.json.gz' +need = L.need + + +def pins(): + src = json.loads((HERE/'SOURCES.json').read_text()) + for row in src['files']: + need(sha256((ROOT/row['path']).read_bytes()).hexdigest() == row['sha256'], 'pin ' + row['path']) + with tarfile.open(ROOT/TAR5713) as tar: + w5713 = json.loads(gzip.decompress(tar.extractfile(MEMBER5713).read())) + return L.SS.read(ROOT/W6030), L.SS.read(ROOT/W5907), w5713 + + +def carrier_summary(w): + classes, _ = L.leak_classes(w) + need(all(c['row_p'] for c in classes if c['kind'] == 'leak'), 'retired value row_p(i) nonzero in every leak class') + counts, res, iv = L.run(w, mode='carrier') + ref = L.SS.census(w, 'empty')[0] + need(counts == ref, 'class census equals PR6040 census') + need(all(r['sources'] == 0 for r in res), 'no carrier source in any leak class') + need(all(r['kind'] == 'unreachable' for r in res), 'every leak class unreachable by carrier corrections') + return {'pr6040_counts': counts, 'leak_classes': len(res), + 'leak_classes_by_leak_count': {str(k): v for k, v in sorted(Counter(r['leak'] for r in res).items())}, + 'carrier_sources': sum(r['sources'] for r in res), 'kinds': dict(Counter(r['kind'] for r in res))} + + +def purez_screen(w): + counts, res, iv = L.run(w, mode='purez', select=lambda c: c['leak'] == 1) + kinds = dict(sorted(Counter(r['kind'] for r in res).items())) + singles = [r for r in res if r['single'] and r['kind'] == 'witness'] + demos = [] + for r in singles[:3]: + corr = [r['single']] + z_only = K.check(w, r['cut_after'], r['pivot'], corr, full=False, pure_sources=True) + need(z_only['O_nonz_defect_after'], 'pure-z correction leaves a non-z defect on O') + try: + K.check(w, r['cut_after'], r['pivot'], corr, full=True, pure_sources=True) + raise AssertionError('full check unexpectedly passed') + except ValueError as exc: + need(str(exc) == 'no non-z defect on O outputs', 'full check fails on the non-z defect') + demos.append({'cut_after': r['cut_after'], 'pivot': r['pivot'], 'correction': r['single'], + 'z_leak_before': z_only['z_leak_before'], 'O_nonz_defect_after': z_only['O_nonz_defect_after']}) + need(len(demos) == 3, 'three pure-z demonstrations') + return {'classes': len(res), 'kinds': kinds, 'single_corrections': sum(1 for r in res if r['single']), + 'single_and_pairing_witness': len(singles), 'demonstrations': demos} + + +def planted(w): + """PR5713 word with, after PR5718's cut (event 14330, chart 602, helper 708): INIT s; s += p; [cut]; s -= p; + o += p for the O role o = 128 at chart 602. s is a carrier (original 0, carries -p) and o leaks.""" + w = json.loads(json.dumps(w)) + n, m = w['public'], w['owned_fields']; s, p, o, F = n + m, 708, 128, 602 + plant_pre = [['INIT', s, F], ['ADD', s, p, '1', F]] + plant_post = [['ADD', s, p, '-1', F], ['ADD', o, p, '1', F], ['CLEAR', s, F]] + prog = w['program'] + w['program'] = prog[:14331] + plant_pre + plant_post + prog[14331:] + w['owned_fields'] = m + 1 + return w, 14332, p, o + + +def control(w5713): + base = L.SS.census(w5713, 'empty')[0] + need(base['witnesses'] == 7, 'PR6040 calibration on PR5713 (7 witnesses)') + w, cut, p, o = planted(w5713) + counts, res, iv = L.run(w, mode='carrier', select=lambda c: (c['cut_after'], c['pivot']) == (cut, p)) + need(len(res) == 1 and res[0]['leak'] >= 1, 'planted class leaks') + r = res[0] + need(r['kind'] == 'witness' and r['single'] and r['single']['target'] == o, 'carrier mode finds the planted fix') + full = K.check(w, cut, p, [r['single']], full=True) + need(not full['O_nonz_defect_after'] and full['z_leak_before'], 'planted fix: leak before, no defect after') + bad = dict(r['single']); bad['mu'] = str(L.Q(bad['mu']) * 2) + try: + K.check(w, cut, p, [bad], full=True) + raise AssertionError('perturbed correction accepted') + except ValueError: + pass + return {'class': {'cut_after': cut, 'frame': r['frame'], 'pivot': p, 'leak': r['leak'], 'kind': r['kind']}, + 'correction': r['single'], 'z_leak_before': full['z_leak_before'], 'perturbed_rejected': True} + + +def main(): + t0 = time.time() + w6030, w5907, w5713 = pins() + need(len(w6030['program']) == 22803 and len(w5907['program']) == 25998, 'word sizes') + print('pins ok', flush=True) + out = {'schema': 'p104-pr5718-leak-correction/v1'} + out['pr6030_carrier'] = carrier_summary(w6030); print('PR6030 carrier', out['pr6030_carrier']['kinds'], flush=True) + out['pr5907_carrier'] = carrier_summary(w5907); print('PR5907 carrier', out['pr5907_carrier']['kinds'], flush=True) + out['pr6030_purez_leak1'] = purez_screen(w6030); print('PR6030 pure-z leak-1', out['pr6030_purez_leak1']['kinds'], flush=True) + out['planted_control'] = control(w5713); print('planted control', out['planted_control']['correction'], flush=True) + text = json.dumps(out, indent=1, sort_keys=True) + '\n' + if '--write' in sys.argv: + (HERE/'RESULT.json').write_text(text) + need((HERE/'RESULT.json').read_text() == text, 'RESULT.json equals the recomputed receipt') + print('PASS_P104_PR5718_LEAK_CORRECTION (%.0f s)' % (time.time() - t0)) + + +if __name__ == '__main__': + main()