From 9c24e52e0041baf6742beddb21ecb54e8d851c29 Mon Sep 17 00:00:00 2001 From: unpaidmoon <131542171+unpaidmoon@users.noreply.github.com> Date: Tue, 20 Oct 2026 01:05:37 +0000 Subject: [PATCH] Price flag 9's head-step co-host at exactly +2 rank mass On the published P104 word, an order-preserving repair co-hosts basis head 196 on X4 and Y23 at the delivering update for two added rank units, and zero is impossible in that class. A relocation comparison also costs +2. No new kappa. Co-authored-by: unpaidmoon --- .../CERTIFICATE.json | 749 ++++++++++++++++++ research/p104-flag9-head-step-repair/PROOF.md | 184 +++++ .../p104-flag9-head-step-repair/README.md | 103 +++ .../REPAIR-RECIPES.json | 571 +++++++++++++ .../p104-flag9-head-step-repair/SOURCES.json | 81 ++ .../p104-flag9-head-step-repair/TASK.json | 102 +++ .../p104-flag9-head-step-repair/VERIFY.json | 52 ++ research/p104-flag9-head-step-repair/build.py | 116 +++ .../independent.py | 306 +++++++ .../test_package.py | 147 ++++ .../p104-flag9-head-step-repair/verify.py | 517 ++++++++++++ 11 files changed, 2928 insertions(+) create mode 100644 research/p104-flag9-head-step-repair/CERTIFICATE.json create mode 100644 research/p104-flag9-head-step-repair/PROOF.md create mode 100644 research/p104-flag9-head-step-repair/README.md create mode 100644 research/p104-flag9-head-step-repair/REPAIR-RECIPES.json create mode 100644 research/p104-flag9-head-step-repair/SOURCES.json create mode 100644 research/p104-flag9-head-step-repair/TASK.json create mode 100644 research/p104-flag9-head-step-repair/VERIFY.json create mode 100644 research/p104-flag9-head-step-repair/build.py create mode 100644 research/p104-flag9-head-step-repair/independent.py create mode 100644 research/p104-flag9-head-step-repair/test_package.py create mode 100644 research/p104-flag9-head-step-repair/verify.py diff --git a/research/p104-flag9-head-step-repair/CERTIFICATE.json b/research/p104-flag9-head-step-repair/CERTIFICATE.json new file mode 100644 index 0000000000..9a02c80e99 --- /dev/null +++ b/research/p104-flag9-head-step-repair/CERTIFICATE.json @@ -0,0 +1,749 @@ +{ + "basis_head": 196, + "bill": { + "R0": { + "added_events": 1, + "added_rank_mass": 2, + "added_scalar_adds": 0, + "added_transport_occurrences": 1, + "distinct_native_edges": 742, + "dropped_native_edges": 2, + "endpoint_adapters": 208, + "events": 4059, + "formal_boundary_columns": 280, + "new_native_edges": 4, + "paid_profile": { + "1": 1073, + "2": 60, + "3": 86, + "4": 105, + "5": 47, + "6": 24, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "profile_delta": { + "1": -1, + "2": 2, + "4": 1, + "5": -1 + }, + "rank_mass": 2370, + "register_rank_mass_delta": { + "D28": 2 + }, + "scalar_adds": 2624, + "transport_occurrences": 1411 + }, + "R1": { + "added_events": 0, + "added_rank_mass": 2, + "added_scalar_adds": 0, + "added_transport_occurrences": 0, + "distinct_native_edges": 741, + "dropped_native_edges": 1, + "endpoint_adapters": 208, + "events": 4058, + "formal_boundary_columns": 280, + "new_native_edges": 2, + "paid_profile": { + "1": 1074, + "2": 58, + "3": 86, + "4": 104, + "5": 47, + "6": 24, + "7": 9, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "profile_delta": { + "5": -1, + "7": 1 + }, + "rank_mass": 2370, + "register_rank_mass_delta": { + "Y23": 2 + }, + "scalar_adds": 2624, + "transport_occurrences": 1410 + }, + "published": { + "distinct_native_edges": 740, + "endpoint_adapters": 208, + "events": 4058, + "formal_boundary_columns": 280, + "paid_profile": { + "1": 1074, + "2": 58, + "3": 86, + "4": 104, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "rank_mass": 2368, + "scalar_adds": 2624, + "transport_occurrences": 1410 + } + }, + "claim_id": "p104-flag9-head-step-repair", + "flag_index": 9, + "forced_hosting": { + "admissible_updates": [], + "non_private_registers_at_rank_floor": 280, + "slot_independently_obstructed_updates": [ + 74, + 75, + 76, + 2070, + 2160, + 2296, + 2640, + 2826, + 3124 + ], + "table": [ + { + "admissible": false, + "event": 74, + "first_obstruction": [ + "Y24", + 77, + "final frame excludes head" + ], + "forced": null, + "must_change": 268, + "partner": "Q2", + "private_registers_forced": [ + [ + "C", + 2462 + ] + ], + "registers_without_prior_transport": 104, + "slot_independent_obstructions": 56 + }, + { + "admissible": false, + "event": 75, + "first_obstruction": [ + "Y24", + 79, + "final frame excludes head" + ], + "forced": null, + "must_change": 256, + "partner": "Q5", + "private_registers_forced": [ + [ + "C", + 2462 + ] + ], + "registers_without_prior_transport": 89, + "slot_independent_obstructions": 56 + }, + { + "admissible": false, + "event": 76, + "first_obstruction": [ + "Y24", + 80, + "final frame excludes head" + ], + "forced": null, + "must_change": 237, + "partner": "Q7", + "private_registers_forced": [ + [ + "C", + 2462 + ] + ], + "registers_without_prior_transport": 79, + "slot_independent_obstructions": 56 + }, + { + "admissible": false, + "event": 2070, + "first_obstruction": [ + "Y28", + 2071, + "final frame excludes head" + ], + "forced": null, + "must_change": 139, + "partner": "D20", + "private_registers_forced": [ + [ + "C", + 2464 + ] + ], + "registers_without_prior_transport": 36, + "slot_independent_obstructions": 56 + }, + { + "admissible": false, + "event": 2160, + "first_obstruction": [ + "Y28", + 2161, + "final frame excludes head" + ], + "forced": null, + "must_change": 139, + "partner": "D10", + "private_registers_forced": [ + [ + "C", + 2464 + ] + ], + "registers_without_prior_transport": 23, + "slot_independent_obstructions": 56 + }, + { + "admissible": false, + "event": 2296, + "first_obstruction": [ + "Y28", + 2297, + "final frame excludes head" + ], + "forced": null, + "must_change": 139, + "partner": "D28", + "private_registers_forced": [ + [ + "C", + 2464 + ] + ], + "registers_without_prior_transport": 5, + "slot_independent_obstructions": 56 + }, + { + "admissible": false, + "event": 2640, + "first_obstruction": [ + "Y28", + 2642, + "final frame excludes head" + ], + "forced": null, + "must_change": 59, + "partner": "D20", + "private_registers_forced": [], + "registers_without_prior_transport": 0, + "slot_independent_obstructions": 23 + }, + { + "admissible": false, + "event": 2826, + "first_obstruction": [ + "Y28", + 2828, + "final frame excludes head" + ], + "forced": null, + "must_change": 37, + "partner": "D10", + "private_registers_forced": [], + "registers_without_prior_transport": 0, + "slot_independent_obstructions": 14 + }, + { + "admissible": false, + "event": 3124, + "first_obstruction": [ + "Y28", + 3126, + "final frame excludes head" + ], + "forced": null, + "must_change": 10, + "partner": "D28", + "private_registers_forced": [], + "registers_without_prior_transport": 0, + "slot_independent_obstructions": 5 + } + ] + }, + "head_cohosting": { + "R0": { + "chart": [ + 447, + 127, + 192, + 196 + ], + "chart_rank": 4, + "cohosted_target_updates": [ + 3124 + ], + "partner": "D28", + "source_delivery_into_target": [ + [ + 3124, + "D28", + "-1/2", + "-1/2" + ] + ], + "source_events_after_update": [ + 3696, + 3803, + 3855, + 3959, + 4010 + ], + "source_frame_rank": 9, + "source_spans_head": true, + "update": 3124 + }, + "R1": { + "chart": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + "chart_rank": 9, + "cohosted_target_updates": [ + 3633 + ], + "partner": "D28", + "source_delivery_into_target": [ + [ + 3633, + "D28", + "-1/2", + "-1/2" + ] + ], + "source_events_after_update": [ + 3695, + 3802, + 3854, + 3958, + 4009 + ], + "source_frame_rank": 9, + "source_spans_head": true, + "update": 3633 + }, + "published_head_hosting_target_updates": [] + }, + "no_new_kappa": true, + "pinned_main": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "repairs": { + "R0": { + "class": "order-preserving: every published event kept in published order with the same ADD registers and coefficients; one downward D28 transport inserted after the delivering ADD", + "rule": "D28 and Y23 enter the published 3124 chart plus the head at their last transports before 3124; D28 drops back to that chart before Y28 reads it; Y23's terminal transport starts from the rank-4 chart", + "splices": [ + { + "events": [ + [ + "transport", + "D28", + [ + 447, + 192 + ], + [ + 447, + 127, + 192, + 196 + ], + 2 + ] + ], + "published": [ + [ + "transport", + "D28", + [ + 447, + 192 + ], + [ + 447, + 127, + 192 + ], + 1 + ] + ], + "published_range": [ + 3122, + 3123 + ] + }, + { + "events": [ + [ + "transport", + "Y23", + [ + 447, + 127 + ], + [ + 447, + 127, + 192, + 196 + ], + 2 + ] + ], + "published": [ + [ + "transport", + "Y23", + [ + 447, + 127 + ], + [ + 447, + 127, + 192 + ], + 1 + ] + ], + "published_range": [ + 3123, + 3124 + ] + }, + { + "events": [ + [ + "add", + "Y23", + "D28", + "1/4", + [ + 447, + 127, + 192, + 196 + ] + ], + [ + "transport", + "D28", + [ + 447, + 127, + 192, + 196 + ], + [ + 447, + 127, + 192 + ], + 1 + ] + ], + "published": [ + [ + "add", + "Y23", + "D28", + "1/4", + [ + 447, + 127, + 192 + ] + ] + ], + "published_range": [ + 3124, + 3125 + ] + }, + { + "events": [ + [ + "transport", + "Y23", + [ + 447, + 127, + 192, + 196 + ], + [ + 467, + 27, + 196, + 12, + 124, + 3, + 7, + 1 + ], + 4 + ] + ], + "published": [ + [ + "transport", + "Y23", + [ + 447, + 127, + 192 + ], + [ + 467, + 27, + 196, + 12, + 124, + 3, + 7, + 1 + ], + 5 + ] + ], + "published_range": [ + 3489, + 3490 + ] + } + ] + }, + "R1": { + "class": "relocation: the delivering ADD, Y23's 3123 transport and Y23's 3489 terminal transport move into D28's full-chart window immediately after D28's lift at 3634; no event added or removed", + "rule": "Y23 lifts from [447, 127] to the full chart, takes Y23 += D28/4 there, then drops to its final frame", + "splices": [ + { + "events": [], + "published": [ + [ + "transport", + "Y23", + [ + 447, + 127 + ], + [ + 447, + 127, + 192 + ], + 1 + ], + [ + "add", + "Y23", + "D28", + "1/4", + [ + 447, + 127, + 192 + ] + ] + ], + "published_range": [ + 3123, + 3125 + ] + }, + { + "events": [], + "published": [ + [ + "transport", + "Y23", + [ + 447, + 127, + 192 + ], + [ + 467, + 27, + 196, + 12, + 124, + 3, + 7, + 1 + ], + 5 + ] + ], + "published_range": [ + 3489, + 3490 + ] + }, + { + "events": [ + [ + "transport", + "D28", + [ + 95, + 447, + 6, + 32, + 20, + 192 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 3 + ], + [ + "transport", + "Y23", + [ + 447, + 127 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 7 + ], + [ + "add", + "Y23", + "D28", + "1/4", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "transport", + "Y23", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + [ + 467, + 27, + 196, + 12, + 124, + 3, + 7, + 1 + ], + 1 + ] + ], + "published": [ + [ + "transport", + "D28", + [ + 95, + 447, + 6, + 32, + 20, + 192 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 3 + ] + ], + "published_range": [ + 3634, + 3635 + ] + } + ] + } + }, + "schema_version": 1, + "selected_kappa": "0.001672660197076918", + "source_register": "X4", + "source_span": { + "head_in_every_source_frame": true, + "literal_drop_after_lists_head": false, + "literal_drop_event": 500, + "source_event_count": 21, + "source_frame_count": 7, + "span_relation": "196 = 64 XOR 132" + }, + "target_register": "Y23" +} diff --git a/research/p104-flag9-head-step-repair/PROOF.md b/research/p104-flag9-head-step-repair/PROOF.md new file mode 100644 index 0000000000..c917d835a3 --- /dev/null +++ b/research/p104-flag9-head-step-repair/PROOF.md @@ -0,0 +1,184 @@ +# Proof: flag-9 head-step repair, its bill, and the order-preserving floor + +## Setup + +Pin CrocSwap main `bb4bccbf42844d2801487450727c2f63e10d1d0f`. Inputs: + +- The #2981 flag matching (`research/p104-joint-unit-flags/CERTIFICATE.json`). + Flag 9 has source 4, target 23 and basis head `196`. +- The reviewed #1991 witness, recipes and checker in `research/p104-native-channel/`. + +All of these are hash-pinned. The channel semantics are those of +`research/p104-native-channel/PROOF.md` §2–§3: a transport changes only the +frame and pays the absolute dimension gap; an ADD is allowed only in a common +frame and changes only the destination row. + +#3443 records that the published word lists `196` on `Y23` only in the +after-frame of the terminal transport at event 3489, and that the generator +list of `X4` drops `196` at event 500. This note does not rerun that literal +census. It uses span membership, which is the chart-independent reading. + +## 1. The source drop is a chart change + +Event 500 transports `X4` from `[196]` to `[8, 64, 132, 260]`. The after-list +does not contain `196`, but + +```text +64 XOR 132 = 196. +``` + +So `196` stays in the span. Direct inspection of all 7 source frames (the +initial frame and six transports) and of the live frame at all 21 events that +name `X4` finds `196` in every one. From event 1326 on, that frame is the +rank-9 full chart. The present-head obstruction on this flag is entirely on +the target side. This is the same phenomenon #3451 found for flag 1, which +#3443's generator-only wording does not record. + +`Y23` does not span `196` at any of its nine ADDs. Its final frame does. +`Y28`'s final frame does not. + +## 2. The delivering update + +The only ADD into `Y23` that carries a nonzero `X4` coefficient is event 3124, + +```text +Y23 += D28/4 in the chart [447, 127, 192]. +``` + +`D28`'s row contributes `-1/2`, and that ADD leaves `Y23`'s `X4` coefficient +at its final value `-1/2`. No earlier `Y23` ADD carries `X4`. The next event +that names `D28` is 3126, `Y28 += D28/4`, in the same chart. Event 3125 does +not name `D28`. + +## 3. Repair R0 + +Let `CH3 = [447, 127, 192]` and `CH4 = CH3 + [196]`. Rank(`CH3`) is 3 and +rank(`CH4`) is 4. `CH4` is contained in `Y23`'s final frame. R0 keeps every +published event in order, with the same ADD registers and coefficients, and +inserts one transport: + +| Published index | Published | R0 | +|---|---|---| +| 3122 | `D28: [447, 192] -> CH3`, rank 1 | `D28: [447, 192] -> CH4`, rank 2 | +| 3123 | `Y23: [447, 127] -> CH3`, rank 1 | `Y23: [447, 127] -> CH4`, rank 2 | +| 3124 | `Y23 += D28/4` in `CH3` | same ADD in `CH4`, then `D28: CH4 -> CH3`, rank 1 | +| 3489 | `Y23: CH3 -> final`, rank 5 | `Y23: CH4 -> final`, rank 4 | + +Every changed transport is nested, and its rank equals the frame gap. `Y23` +has no event between 3124 and 3489, so it stays in `CH4` until the terminal +transport. `D28` is back in `CH3` before event 3126, so `Y28`, `Y29`, `Y22`, +`Y31` and `Y103` keep their published charts. + +`verify.py` builds this word in memory and calls the published +`check_native.validate()` unchanged. That checks every native edge (two +published edges drop out and four new ones enter; 742 distinct edges), all +208 endpoint adapters, and all 280 framed rows, including restoration of the +72 dirty helpers. `independent.py` replays both words with exact rational rows +and finds all 280 final rows equal to the published rows. In R0 the ADD at +index 3124 runs in `CH4` while `X4` is in the full chart, and `X4` still has +reads at repaired indices 3696, 3803, 3855, 3959 and 4010. + +Per-register rank mass changes only on `D28`, by `+2` (the extra rank on the +way into `CH4`, and the rank-1 drop back). `Y23`'s entry grows by 1 and its +terminal transport shrinks by 1. The paid-profile delta is + +```text +-H1 + 2 H2 + H4 - H5. +``` + +For an affine price `H(r) = a + b r` this is `a + 2b`: one added transport +occurrence and two added rank units. For `H(r) = r^2` the same delta is `-2`. +The sign is not uniform across convex prices. + +## 4. Repair R1 + +R1 deletes the published events 3123, 3124 and 3489 and, immediately after +`D28`'s lift to the full chart at 3634 and before `D28 += Q7`, inserts + +```text +Y23: [447, 127] -> FULL, rank 7 +Y23 += D28/4 in FULL +Y23: FULL -> final, rank 1 +``` + +`D28` is not written between 3124 and 3635, so the same coefficient still +delivers `-1/2`. Nothing reads `Y23`, so moving that single ADD does not +change any other row. Event count, ADD count and transport count stay at the +published values. Rank mass grows by 2, all of it on `Y23`. The profile delta +is `H7 - H5`, which is `2b` for every affine price and `+24` for `H(r) = r^2`. +The published checker passes, with 741 distinct native edges. The co-hosted +ADD is at repaired index 3633, and `X4` still has its five later reads. + +R1 is not order-preserving: it moves the delivering ADD. It matches R0's rank +mass and removes R0's extra event. Under a positive per-event price it is the +cheaper of the two exhibited repairs. Under a steep convex rank price, R0's +profile can cost less. + +## 5. Order-preserving floor + +**Class P.** A repair is in class P when: + +1. every published event is kept, in published order, with the same opcode, + registers and ADD coefficient (transport frames may change, ADD chart + fields may change, and transports may be inserted); +2. every initial and final frame is kept; +3. every transport rank equals the absolute dimension gap of a nested pair. + +**Parity.** On one register the sum of absolute dimension gaps is congruent +modulo 2 to `rank(final) - rank(initial)`, because every descent has to be +matched by a later ascent. All 280 non-private registers of the published word +already meet that floor, so every class-P repair adds a nonnegative even +integer of rank mass on each of them. The total added rank mass is therefore +0 or at least 2. + +**Zero is impossible for the delivering ADD.** Suppose a class-P repair adds +no rank mass. Then every non-private path is monotone: a vector that enters a +frame stays in every later frame of that register. The delivering ADD is still +`Y23 += D28/4`, still followed, after whatever transports are inserted, by the +published event 3126 `Y28 += D28/4`. Co-hosting requires `196` in `D28`'s +frame at the ADD. + +- If some inserted transport removes `196` from `D28` before event 3126, that + transport is a descent, so `D28`'s mass is at least 2 above its floor. +- If not, `D28` still spans `196` at event 3126, so the common chart forces + `Y28` to span `196` there. `Y28`'s final frame does not span `196`, and a + monotone path cannot drop it. So `Y28`'s mass is at least 2 above its floor. + +Thus every class-P repair that co-hosts `196` on `X4` and `Y23` at the +delivering ADD adds at least 2 rank units. R0 adds exactly 2, so that floor +is sharp. R0's extra unit is the descent on `D28`; `Y23` pays nothing because +its final frame already contains `CH4`. + +The same monotone closure, applied to all nine `Y23` ADDs on the published +word, finds no admissible update. Each forces the head into at least one +register whose final frame excludes it: + +| Update | Partner | Final-excluding registers | First | +|---:|---|---:|---| +| 74 | `Q2` | 56 | `Y24` at 77 | +| 75 | `Q5` | 56 | `Y24` at 79 | +| 76 | `Q7` | 56 | `Y24` at 80 | +| 2070 | `D20` | 56 | `Y28` at 2071 | +| 2160 | `D10` | 56 | `Y28` at 2161 | +| 2296 | `D28` | 56 | `Y28` at 2297 | +| 2640 | `D20` | 23 | `Y28` at 2642 | +| 2826 | `D10` | 14 | `Y28` at 2828 | +| 3124 | `D28` | 5 | `Y28` at 3126 | + +`verify.py` computes this closure with a worklist. `independent.py` recomputes +the final-excluding part with a forward sweep. The two agree on all nine rows. + +## 6. What this does not say + +Class P does not include repairs that reorder ADDs, change ADD coefficients, +or change a final frame. R1 shows one legal reordering and still pays `+2`. +It does not prove that every reordering pays `+2`. A zero-mass repair would +have to introduce `196` on `D28` only after every later partner whose final +frame excludes `196` has already read `D28`, and then keep `196` on the +monotone path to `D28`'s full final frame. No such schedule is constructed +or excluded here. + +Neither repair is an `I - G/2` correction, a dirty-restoration program, or a +change to the selected conditional κ `0.001672660197076918`. The channel still +implements the published `G/2` map. The co-hosted chart only removes the +geometric obstruction recorded for this one flag. diff --git a/research/p104-flag9-head-step-repair/README.md b/research/p104-flag9-head-step-repair/README.md new file mode 100644 index 0000000000..14d6491498 --- /dev/null +++ b/research/p104-flag9-head-step-repair/README.md @@ -0,0 +1,103 @@ +# Flag 9's delivering update can be co-hosted for exactly two added rank units + +**Finite repaired words with an exact bill, plus a sharp order-preserving floor. No new exponent.** + +Open [#3443](https://github.com/CrocSwap/integer-mult-bounds/pull/3443) shows that +on the published 4,058-event P104 word, present-head flag 9 (`X4` → `Y23`, +basis head `196`) never updates `Y23` while both endpoints list the head. Its +open question asks what a changed schedule that co-hosts the head would cost. +The same question is open for this flag in +[#3508](https://github.com/CrocSwap/integer-mult-bounds/pull/3508) and was released +without a submission. Flag 1's repair is the separate open +[#3532](https://github.com/CrocSwap/integer-mult-bounds/pull/3532); this package +does not recompute it. Flag 43's zero-mass repair is the method being followed, +not the result: flag 9 has no zero-mass order-preserving repair. + +## Result + +The published source "drop" at event 500 does not remove `196` from the span. +The after-list is `[8, 64, 132, 260]` and `64 XOR 132 = 196`. All 7 source +frames and all 21 events that name `X4` span `196`. The obstruction is on +`Y23` only. + +The only `Y23` update that carries `X4` is event 3124, `Y23 += D28/4`. It +delivers `-1/2` and settles `Y23`'s final `X4` coefficient. Two repaired words +make that ADD co-host `196` while `X4` is in its rank-9 chart and still has +five later reads. The published `check_native.validate()` passes on both. + +- **R0 (order-preserving).** `D28` and `Y23` enter the published 3124 chart + plus `196`. The ADD runs there. One inserted transport drops `D28` back + before `Y28` reads it. `Y23` keeps the head until its terminal transport. + Added rank mass is `+2`, all of it on `D28`. +- **R1 (relocation).** The delivering ADD moves into `D28`'s full-chart window + just after event 3634. `Y23` lifts from `[447, 127]` to the full chart, takes + the ADD, and drops to its final frame. No event is added or removed. Added + rank mass is `+2`, all of it on `Y23`. + +| Bill term | Published | R0 | R1 | +|---|---:|---:|---:| +| Events | 4,058 | 4,059 | 4,058 | +| Scalar ADDs | 2,624 | 2,624 | 2,624 | +| Transport occurrences | 1,410 | 1,411 | 1,410 | +| Rank mass | 2,368 | 2,370 | 2,370 | +| Distinct native edges | 740 | 742 | 741 | +| Where the +2 sits | — | `D28` | `Y23` | +| Paid profile delta | — | `-H1 + 2H2 + H4 - H5` | `H7 - H5` | + +Under an affine price `H(r) = a + b r`, R0 costs `a + 2b` and R1 costs `2b`. +Under `H(r) = r^2`, R0 costs `-2` and R1 costs `+24`. R1 is cheaper when each +event has a positive price. R0 can be cheaper for a steep convex rank price. + +In the order-preserving class (published events kept in order, endpoint frames +kept, nested rank-gap transports, insertions allowed), added rank mass is even, +and zero is impossible: keeping `196` on `D28` through event 3126 forces it +into `Y28`, whose final frame excludes it, and dropping it before 3126 costs +2 on `D28`. R0 meets the floor. The same closure obstructs all nine `Y23` +updates. Reordering those reads is not ruled out and is not given a zero-mass +schedule here. + +Selected κ stays `0.001672660197076918`. The argument is in [PROOF.md](PROOF.md). + +## Reproduce + +From the repository root, CPython 3.12: + +```sh +python3.12 -I -B research/p104-flag9-head-step-repair/verify.py +python3.12 -I -O -Werror -B research/p104-flag9-head-step-repair/verify.py +python3.12 -I -O -Werror -B research/p104-flag9-head-step-repair/independent.py +python3.12 -I -O -Werror -B research/p104-flag9-head-step-repair/test_package.py +python3.12 -B scripts/research_package.py --package research/p104-flag9-head-step-repair +``` + +`verify.py` is read-only. It loads the pinned `check_native.py` by path and runs +its `validate()` on each repaired word built in memory. Admission goes through +`need()` and still fires under `-O`. `independent.py` imports neither `verify.py` +nor the native checker. `test_package.py` corrupts temporary copies and checks +that both scanners reject all 10 mutations, including deletion of R0's return +transport and an undercharged terminal rank. `build.py` is the producer and is +not part of the replay. + +## Credit + +Credit #3443 for flag 9's published literal chronology, #3451 for the span +reading on flag 1, and #3508 for the head-step repair method and the class-P +closure rule. Credit #3349 for the present-head census. Credit Nick Petalas / +#2981 for the flag matching, and the reviewed #1991 native channel (Chafik +Boukhalfa) for the witness, checker and compiler. #3532 is the flag-1 repair +this package deliberately does not repeat; its open question 3 asks for this +flag. Prepared by unpaidmoon with substantial Cursor Grok assistance. No +independent human or formal-kernel review is claimed. Apache-2.0. + +## Open next questions + +1. Is there a zero-added-mass co-hosting repair that reorders `D28`'s reads? + Every partner whose final frame excludes `196` would have to read `D28` + before `196` enters, and `196` would then have to stay on `D28`'s monotone + path to the full chart. R1 still pays `+2`, so the exhibited relocation is + not that schedule. +2. Can a side correction use R0's chart `[447, 127, 192, 196]` at the repaired + index 3124, or R1's full chart at 3633, to restore `X4` into `Y23`, and what + does the `I - G/2` correction cost at that cut? +3. Which of R0 and R1 is cheaper under the channel's actual per-rank weights? + Affine prices prefer R1; `H(r) = r^2` prefers R0. diff --git a/research/p104-flag9-head-step-repair/REPAIR-RECIPES.json b/research/p104-flag9-head-step-repair/REPAIR-RECIPES.json new file mode 100644 index 0000000000..a48b898b29 --- /dev/null +++ b/research/p104-flag9-head-step-repair/REPAIR-RECIPES.json @@ -0,0 +1,571 @@ +{ + "clifford_exact_sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "compiler_sha256": "9d2fc2d81962ddb0b4dd7d6482d9918a87a6b05759690317dea79939ca5656a3", + "recipes": [ + { + "new": [ + 256, + 160, + 96, + 16, + 8, + 4, + 2, + 1 + ], + "old": [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + "rank": 1, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 2, + 4, + 8, + 16, + 32, + 1, + 64, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 1, + "right": { + "linear_Z4": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 32, + 1, + 2, + 4, + 8, + 16, + 96, + 160, + 256 + ], + "offset": 192, + "phase": 1, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + } + }, + { + "new": [ + 256, + 168, + 16, + 5 + ], + "old": [ + 256, + 168 + ], + "rank": 2, + "recipe": { + "left": { + "linear_Z4": [ + 3, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 5, + 8, + 1, + 16, + 2, + 32, + 64, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 2, + "right": { + "linear_Z4": [ + 1, + 0, + 2, + 0, + 2, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 1, + 16, + 5, + 2, + 8, + 32, + 64, + 128, + 256 + ], + "offset": 2, + "phase": 1, + "quadratic_rows": [ + 5, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + } + }, + { + "new": [ + 256, + 160, + 96, + 16, + 8, + 4, + 2, + 1 + ], + "old": [ + 256, + 168, + 16, + 5 + ], + "rank": 4, + "recipe": { + "left": { + "linear_Z4": [ + 3, + 2, + 2, + 3, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 17, + 2, + 1, + 36, + 64, + 140, + 8, + 4, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 1, + 0, + 8, + 12, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 4, + "right": { + "linear_Z4": [ + 0, + 2, + 0, + 0, + 0, + 2, + 3, + 3, + 0 + ], + "matrix_rows": [ + 1, + 2, + 232, + 160, + 4, + 128, + 16, + 224, + 256 + ], + "offset": 19, + "phase": 1, + "quadratic_rows": [ + 4, + 0, + 1, + 96, + 0, + 136, + 72, + 160, + 0 + ] + } + } + }, + { + "new": [ + 256, + 168, + 5 + ], + "old": [ + 256, + 168, + 16, + 5 + ], + "rank": 1, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 2, + 4, + 8, + 16, + 1, + 32, + 64, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 1, + "right": { + "linear_Z4": [ + 0, + 0, + 0, + 0, + 2, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 16, + 1, + 2, + 4, + 8, + 32, + 64, + 128, + 256 + ], + "offset": 0, + "phase": 3, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + } + }, + { + "new": [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + "old": [ + 256, + 173 + ], + "rank": 7, + "recipe": { + "left": { + "linear_Z4": [ + 3, + 2, + 3, + 3, + 2, + 3, + 2, + 0, + 0 + ], + "matrix_rows": [ + 129, + 2, + 4, + 8, + 16, + 32, + 64, + 45, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 45, + 0, + 45, + 45, + 0, + 45, + 0, + 0, + 0 + ] + }, + "rank": 7, + "right": { + "linear_Z4": [ + 0, + 2, + 0, + 0, + 2, + 0, + 2, + 1, + 0 + ], + "matrix_rows": [ + 1, + 2, + 132, + 136, + 16, + 160, + 64, + 128, + 256 + ], + "offset": 82, + "phase": 3, + "quadratic_rows": [ + 128, + 0, + 128, + 128, + 0, + 128, + 0, + 173, + 0 + ] + } + } + }, + { + "new": [ + 256, + 168, + 16, + 5 + ], + "old": [ + 256, + 173 + ], + "rank": 2, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 5, + 8, + 17, + 33, + 2, + 65, + 128, + 1, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 2, + "right": { + "linear_Z4": [ + 1, + 0, + 2, + 1, + 2, + 1, + 0, + 2, + 0 + ], + "matrix_rows": [ + 169, + 16, + 133, + 2, + 128, + 136, + 160, + 64, + 256 + ], + "offset": 2, + "phase": 1, + "quadratic_rows": [ + 45, + 0, + 1, + 41, + 0, + 41, + 0, + 0, + 0 + ] + } + } + } + ], + "schema_version": 1, + "scope": "Native recipes for the transport edges used by flag-9 repairs R0 and R1 that are absent from the published p104-native-channel recipe set. Lowered with the pinned compile.py / vendor/clifford_exact.py; checked by the published check_native.validate() during replay." +} diff --git a/research/p104-flag9-head-step-repair/SOURCES.json b/research/p104-flag9-head-step-repair/SOURCES.json new file mode 100644 index 0000000000..8989de3bf7 --- /dev/null +++ b/research/p104-flag9-head-step-repair/SOURCES.json @@ -0,0 +1,81 @@ +{ + "schema_version": 1, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "upstream": "CrocSwap/integer-mult-bounds", + "files": [ + { + "path": "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "usage": "input", + "git_blob": "86beaf424e9f0f800ae3a62797d94ec9386b7706", + "sha256": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e", + "credit": "Reviewed #1991 native channel witness (PR1972 word)" + }, + { + "path": "research/p104-native-channel/inputs/P104-FIXTURE.json", + "usage": "input", + "git_blob": "2e16f99b295bb386fd13bd8fbd57b42ef54143a9", + "sha256": "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4", + "credit": "P104 fixture used by the published native checker" + }, + { + "path": "research/p104-native-channel/NATIVE-RECIPES.json.gz", + "usage": "input", + "git_blob": "ab129678c2df4f0d39b02b88457d02c37de0d9b6", + "sha256": "a1c4d83d3d5fe1338e99b59272e8cf5d43244c33888597da340b2aa7fef5b3e8", + "credit": "Published native recipes (Chafik Boukhalfa, PR1991)" + }, + { + "path": "research/p104-native-channel/check_native.py", + "usage": "input", + "git_blob": "f8e54afbf146cd6f250063bcb1b9dabf0cbc42ea", + "sha256": "e67b874a061a4a28007b9a0fabaf30c8db4a587b1e1c7dd9396c77ff1e3a9fe6", + "credit": "Published native checker; its validate() is run unchanged on each repaired word" + }, + { + "path": "research/p104-native-channel/vendor/native_verify.py", + "usage": "input", + "git_blob": "2c209dfa9cfade3bc20ac5fc9d876b433a147f8c", + "sha256": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38", + "credit": "Independent native interpreter used by check_native.py and by independent.py" + }, + { + "path": "research/p104-joint-unit-flags/CERTIFICATE.json", + "usage": "input", + "git_blob": "0fa7d2d40566e92f3ea1539723abf438ba65adb8", + "sha256": "a98126428a8da6eae91c50afcc42e014a284c82b554ef77e5b3a34fc6d228128", + "credit": "Nick Petalas, PR #2981 flag matching (flag 9 identity)" + }, + { + "path": "research/p104-native-channel/compile.py", + "usage": "provenance", + "git_blob": "840d7608d6795d12ba174620279f88d8a6f727b4", + "sha256": "9d2fc2d81962ddb0b4dd7d6482d9918a87a6b05759690317dea79939ca5656a3", + "pin": "base_commit:research/p104-native-channel/compile.py", + "credit": "Native compiler used by build.py to lower the new edges" + }, + { + "path": "research/p104-native-channel/vendor/clifford_exact.py", + "usage": "provenance", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "pin": "base_commit:research/p104-native-channel/vendor/clifford_exact.py", + "credit": "Exact Clifford lowering used by build.py" + }, + { + "path": "research/p104-native-channel/PROOF.md", + "usage": "provenance", + "git_blob": "a69311b74f74a2f8e8f411c1451baacd9bacddce", + "sha256": "5d743145d389ffdfaffc66096fa7e32c7155b18f73d74755403151d0435bb94c", + "pin": "base_commit:research/p104-native-channel/PROOF.md", + "credit": "Binary-frame semantics: nested transports, adds only in a common chart, paid rank per transport" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0", + "pin": "base_commit:docs/research/agent-task-catalog.json", + "credit": "Priority revision 6 task catalogue at the pinned base" + } + ] +} diff --git a/research/p104-flag9-head-step-repair/TASK.json b/research/p104-flag9-head-step-repair/TASK.json new file mode 100644 index 0000000000..4b677b5e12 --- /dev/null +++ b/research/p104-flag9-head-step-repair/TASK.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 6, + "selected_kappa": "0.001672660197076918", + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "original_card": { + "id": "p104-side-correction", + "question": "Can the proposed P104 joint endpoint flags be realized by a chronological correction program with coefficients, dirty restoration and an affordable complete bill?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/p104-native-channel/README.md", + "research/p104-native-channel/PROOF.md", + "docs/research/community-efficient1000-review.md", + "research/p104-joint-unit-flags/README.md" + ], + "methods": [ + "Construct one side-correction word at an explicit chronological cut with the needed frames still available.", + "Derive a lower bound on the side correction and hosting costs that decides whether this channel can beat the selected budget." + ], + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the revision-6 family record and #2981 static joint flags, alongside the reviewed #1991 channel. #2981 is an author-checked source archive, not an independently validated executable correction or a refutation of program-level lifetime floors.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "After checking live handoffs, pin one named collection from #2981 and attach acquisition/delivery times, source dependencies and coefficient requirements. Test legal access and arbitrary dirty restoration; price any completion against the full channel/endpoint/hosting allowance. Stop with the exact missing implication or a scoped counterexample rather than expanding the static cover census.", + "bottleneck_link": "Completing an already realized changed channel tests a concrete construction opportunity, instead of refining the incumbent packing. A positive local result still needs global and all-size admission.", + "allowed_variations": [ + "One correction factorization, one chronological cut, or one explicit hosting obstruction.", + "A changed correction schedule with an updated full bill and native frame contract." + ], + "scope_change_triggers": [ + "Recompiling the already certified low-rank channel without closing a new obligation.", + "Treating a pending ancestor, local histogram or unpriced side correction as an admitted global supplier.", + "Repeating a correction or physical conversion already supplied by a pending follow-up without adding independent coverage or a different unresolved obligation.", + "Repeating the 208-flag static matching or calling a static nested cover a chronological correction program. Independent audit of that certificate is distinct and remains useful." + ], + "overlap_terms": [ + "P104", + "I-G/2", + "side correction", + "native channel", + "1972", + "1991", + "2586", + "endpoint transport", + "physical dual", + "relay composition", + "2981", + "joint unit flags", + "acquisition delivery", + "static nesting" + ], + "existing_checks": [ + { + "scope": "PR #2981 reports static joint endpoint flags and a matching of 208 departure and arrival flags; archival intake is not independent verification.", + "evidence": "research/p104-joint-unit-flags/README.md", + "remaining": "Independent flag check and a chronological coefficient program with dirty restoration and a complete cost.", + "status": "author-checked", + "source_commit": "3d24b92d8ba057b57cb2d480170ec407520e6882", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "On the published #1991 word, price an order-preserving schedule that co-hosts present-head flag 9's basis head 196 on X4 and Y23 at the single update that delivers X4, and prove that two added rank units is the minimum in that class.", + "scope_change_reason": "The card asks for a chronological correction with a complete bill. Live overlap shows flag 43's zero-mass head-step repair is already on main (#3508) and flag 1's +2 repair is the open PR #3532. The released flag-9 question, and #3532's open question 3, ask only for this flag's added rank mass. This package answers that cut. It does not build an I-G/2 word or rerun the fixed-cover support cut.", + "bottleneck_link": "Flag 9 is one of the four present-head flags whose published channel never co-hosts the basis head at a target update. Showing that the delivering update can be co-hosted for exactly +2 rank mass, and that zero is impossible while the published event order is kept, prices the geometric obstruction #3443 left open. It does not admit a P104 supplier.", + "budget_minutes": 60, + "stop_rule": "Stop after flag 9: one order-preserving repair, one relocation comparison, both natively validated, and the closure of all nine Y23 updates. Do not rebuild flag 1 or flag 43, and do not search a reordered zero-mass schedule.", + "outcome": "completed", + "evidence": "X4 spans 196 at all 21 source events; the literal drop at event 500 satisfies 196 = 64 XOR 132. The only X4 delivery into Y23 is event 3124, coefficient -1/2. R0 inserts one D28 return transport and adds rank mass 2, all on D28, with profile delta -H1+2H2+H4-H5. R1 relocates the ADD into D28's full chart and adds rank mass 2, all on Y23, with profile delta H7-H5 and no added event. Published check_native.validate() passes on both words (742 and 741 native edges). All 280 final rows match. All nine Y23 updates are closure-obstructed; 3124's first obstruction is Y28 at 3126. All 280 non-private registers sit at their rank floor, so class-P added mass is even and the delivering co-host costs at least 2. Selected kappa unchanged.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance for the closure computation, the two repaired schedules, the native-recipe lowering and the write-up. No independent human or formal-kernel review claimed.", + "no_new_kappa": true, + "open_questions": [ + { + "question": "Is there a zero-added-mass co-hosting repair that reorders D28's reads so every final-excluding partner reads D28 before 196 enters, with 196 then staying on D28's monotone path to the full chart?", + "why_it_matters": "R0 shows +2 is sharp only inside the order-preserving class. A zero-mass reordering would remove the rank cost of this flag's geometric obstruction.", + "first_step": "List D28's partners whose final frames exclude 196 and test whether each of those ADDs can move to a published D28 chart that does not span 196 without raising another register off its rank floor.", + "blocked_by": "No such reordering was constructed or excluded. R1, which moves only the delivering ADD, still pays +2." + }, + { + "question": "Can a side correction use R0's chart [447, 127, 192, 196] at repaired index 3124, or R1's full chart at 3633, to restore X4 into Y23, and what does the I-G/2 correction cost at that cut?", + "why_it_matters": "The co-hosted chart removes #3443's geometric reason for this one flag. The supplier question is the correction's own bill, not another channel retiming.", + "first_step": "Price one X4-to-Y23 transfer in R0's common head chart against the channel allowance, keeping X4's full-chart frame explicit.", + "blocked_by": "No side-correction word is built here. The channel still implements G/2, not I." + }, + { + "question": "Which of R0 and R1 is cheaper under the channel's actual per-rank weights?", + "why_it_matters": "Affine prices H(r)=a+br prefer R1 (2b against a+2b). H(r)=r^2 prefers R0 (-2 against +24). The repository weight decides which repair is the one to build on.", + "first_step": "Evaluate both profile deltas on the paid rank prices used by the selected P104 channel invoice.", + "blocked_by": "This package reports the two profiles and does not import an external weight vector." + } + ] +} diff --git a/research/p104-flag9-head-step-repair/VERIFY.json b/research/p104-flag9-head-step-repair/VERIFY.json new file mode 100644 index 0000000000..9c94b8605d --- /dev/null +++ b/research/p104-flag9-head-step-repair/VERIFY.json @@ -0,0 +1,52 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "research/p104-native-channel/inputs/P104-FIXTURE.json", + "research/p104-native-channel/NATIVE-RECIPES.json.gz", + "research/p104-native-channel/check_native.py", + "research/p104-native-channel/vendor/native_verify.py", + "research/p104-joint-unit-flags/CERTIFICATE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Applies repairs R0 and R1 in memory, runs published check_native.validate() on each, and requires the bill, X4 span correction, delivery of -1/2 and the nine-update closure to match CERTIFICATE.json" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Separately written XOR-closure replay: nested rank-gap transports, 280/280 final rows, profile deltas, native check of each new recipe, source span 196 = 64 XOR 132, and the forward-sweep closure" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 300, + "checks": "Temp-tree clean pass with a byte-identical tree; 10 rejections by both scanners under -O, including a missing D28 return transport and an undercharged terminal rank" + } + ] +} diff --git a/research/p104-flag9-head-step-repair/build.py b/research/p104-flag9-head-step-repair/build.py new file mode 100644 index 0000000000..2e97896be7 --- /dev/null +++ b/research/p104-flag9-head-step-repair/build.py @@ -0,0 +1,116 @@ +#!/usr/bin/env python3 +"""Producer for CERTIFICATE.json and REPAIR-RECIPES.json (not part of replay). + +Defines the two changed schedules as splices of the published witness, +lowers each transport edge absent from the published recipe set with the +pinned native compiler, and writes the receipt computed by verify.py. +Refuses to overwrite existing outputs unless --force is given. +""" + +import argparse +import hashlib +import importlib.util +import json +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import verify as V # noqa: E402 + +COMPILER_SHA256 = "9d2fc2d81962ddb0b4dd7d6482d9918a87a6b05759690317dea79939ca5656a3" +CLIFFORD_SHA256 = "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + +CH3 = [447, 127, 192] +CH4 = [447, 127, 192, 196] +B2 = [447, 192] +Y2 = [447, 127] +FULL = [1, 2, 4, 8, 16, 32, 64, 128, 256] + + +def splices(program, final): + def one(i, event): + return {"published_range": [i, i + 1], "published": [program[i]], "events": [event]} + + r0 = [ + one(3122, ["transport", "D28", B2, CH4, 2]), + one(3123, ["transport", "Y23", Y2, CH4, 2]), + {"published_range": [3124, 3125], "published": [program[3124]], + "events": [["add", "Y23", "D28", "1/4", CH4], ["transport", "D28", CH4, CH3, 1]]}, + one(3489, ["transport", "Y23", CH4, final["Y23"], 4]), + ] + r1 = [ + {"published_range": [3123, 3125], "published": program[3123:3125], "events": []}, + {"published_range": [3489, 3490], "published": [program[3489]], "events": []}, + {"published_range": [3634, 3635], "published": [program[3634]], + "events": [program[3634], + ["transport", "Y23", Y2, FULL, 7], + ["add", "Y23", "D28", "1/4", FULL], + ["transport", "Y23", FULL, final["Y23"], 1]]}, + ] + return { + "R0": { + "class": "order-preserving: every published event kept in published order with the same ADD registers and coefficients; one downward D28 transport inserted after the delivering ADD", + "rule": "D28 and Y23 enter the published 3124 chart plus the head at their last transports before 3124; D28 drops back to that chart before Y28 reads it; Y23's terminal transport starts from the rank-4 chart", + "splices": r0, + }, + "R1": { + "class": "relocation: the delivering ADD, Y23's 3123 transport and Y23's 3489 terminal transport move into D28's full-chart window immediately after D28's lift at 3634; no event added or removed", + "rule": "Y23 lifts from [447, 127] to the full chart, takes Y23 += D28/4 there, then drops to its final frame", + "splices": r1, + }, + } + + +def load(name, path, digest): + raw = path.read_bytes() + V.need(hashlib.sha256(raw).hexdigest() == digest, "pinned compiler module: " + str(path)) + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--force", action="store_true") + args = ap.parse_args() + for name in ("CERTIFICATE.json", "REPAIR-RECIPES.json"): + V.need(args.force or not (HERE / name).exists(), name + " exists") + root = V.ROOT + load("flag9_clifford_pin", root / V.NATIVE / "vendor/clifford_exact.py", CLIFFORD_SHA256) + co = load("flag9_native_compile", root / V.NATIVE / "compile.py", COMPILER_SHA256) + witness, _fixture, recipes, _flags = V.load_inputs(root) + cert = {"repairs": splices(witness["program"], witness["final_frames"])} + physical = V.physical_map(recipes) + pub = {(tuple(r["old"]), tuple(r["new"])) for r in recipes["transports"]} + new = {} + for name in ("R0", "R1"): + prog = V.apply_splices(witness["program"], cert["repairs"][name]["splices"]) + for e in prog: + if e[0] != "transport": + continue + key = (physical(e[2]), physical(e[3])) + if key in pub or key in new: + continue + actual = co.CE.canonical_frame(9, key[0]).adjoint().then(co.CE.canonical_frame(9, key[1])) + record, _ = co.CE.lower_child(actual) + V.need(record["rank"] == e[4], "native rank equals frame gap") + new[key] = {"old": list(key[0]), "new": list(key[1]), "rank": e[4], "recipe": record} + recs = [new[k] for k in sorted(new)] + payload = { + "schema_version": 1, + "scope": "Native recipes for the transport edges used by flag-9 repairs R0 and R1 that are absent from the published p104-native-channel recipe set. Lowered with the pinned compile.py / vendor/clifford_exact.py; checked by the published check_native.validate() during replay.", + "compiler_sha256": COMPILER_SHA256, + "clifford_exact_sha256": CLIFFORD_SHA256, + "recipes": recs, + } + got = V.receipt(root, cert, recs) + (HERE / "REPAIR-RECIPES.json").write_text(json.dumps(payload, indent=1, sort_keys=True) + "\n") + (HERE / "CERTIFICATE.json").write_text(json.dumps(got, indent=2, sort_keys=True) + "\n") + print("WROTE", len(recs), "new recipes") + + +if __name__ == "__main__": + main() diff --git a/research/p104-flag9-head-step-repair/independent.py b/research/p104-flag9-head-step-repair/independent.py new file mode 100644 index 0000000000..dca614b3fd --- /dev/null +++ b/research/p104-flag9-head-step-repair/independent.py @@ -0,0 +1,306 @@ +#!/usr/bin/env python3 +"""Second scanner for the flag-9 head-step repair bill. + +Does not import verify.py, check_native.py or the compiler. Frames are +XOR-closure sets. Both repaired words are replayed with exact rational rows +and compared with the published final rows. Transport ranks are the frame +gaps. New native recipes are checked with the vendored interpreter. The +forced-hosting closure is a forward sweep. Admission uses need() and stays +active under python -O. +""" + +import gzip +import hashlib +import importlib.util +import json +import sys +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +NATIVE = "research/p104-native-channel" +PINS = { + f"{NATIVE}/inputs/LOWRANK-WITNESS.json": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e", + f"{NATIVE}/NATIVE-RECIPES.json.gz": "a1c4d83d3d5fe1338e99b59272e8cf5d43244c33888597da340b2aa7fef5b3e8", + f"{NATIVE}/vendor/native_verify.py": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38", + "research/p104-joint-unit-flags/CERTIFICATE.json": "a98126428a8da6eae91c50afcc42e014a284c82b554ef77e5b3a34fc6d228128", +} +HEAD = 196 +SOURCE = "X4" +TARGET = "Y23" +MARKER = ( + "PASS_P104_FLAG9_HEAD_STEP_REPAIR_INDEPENDENT flag=9 head=196 " + "R0_added_rank_mass=2 R1_added_rank_mass=2 rows_equal=280/280 " + "updates_obstructed=9/9 source_events_keep_head=21/21 no_new_kappa" +) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def strict(pairs): + seen = {} + for k, v in pairs: + need(k not in seen, "duplicate JSON key: " + str(k)) + seen[k] = v + return seen + + +def read(root, rel, gz=False): + raw = (root / rel).read_bytes() + need(hashlib.sha256(raw).hexdigest() == PINS[rel], "source hash: " + rel) + return json.loads(gzip.decompress(raw) if gz else raw, object_pairs_hook=strict) + + +def closure(vectors): + out = frozenset([0]) + for v in vectors: + out = out | frozenset(x ^ v for x in out) + return out + + +def dim(s): + n = len(s) + need(n and n & (n - 1) == 0, "closure size is a power of two") + return n.bit_length() - 1 + + +def splice(program, rows): + out = list(program) + edits = sorted(((r["published_range"][0], r["published_range"][1], r) for r in rows), reverse=True) + prev = len(program) + for a, b, r in edits: + need(b <= prev and a < b, "disjoint splices") + need(program[a:b] == r["published"], "splice binding at %d" % a) + out[a:b] = [list(e) for e in r["events"]] + prev = a + return out + + +def replay(witness, program): + rows = {n: {n: Fraction(1)} for n in witness["initial_frames"]} + frames = {n: closure(f) for n, f in witness["initial_frames"].items()} + profile = {} + adds = 0 + for i, e in enumerate(program): + op = e[0] + if op == "transport": + _, r, old, new, k = e + a, b = closure(old), closure(new) + need(frames[r] == a, "transport before-frame continuity at %d" % i) + need(a <= b or b <= a, "nested transport at %d" % i) + need(k == abs(dim(b) - dim(a)) and k > 0, "paid rank equals frame gap at %d" % i) + frames[r] = b + profile[k] = profile.get(k, 0) + 1 + elif op == "zero": + need(e[1] not in frames, "fresh private") + rows[e[1]] = {} + frames[e[1]] = closure(e[2]) + elif op == "erase": + need(frames[e[1]] == closure(e[2]), "erase chart") + rows.pop(e[1]) + frames.pop(e[1]) + elif op == "copy": + need(not rows[e[1]] and frames[e[1]] == frames[e[2]] == closure(e[3]), "copy chart") + rows[e[1]] = dict(rows[e[2]]) + else: + need(op == "add", "opcode") + _, d, s, c, f = e + need(d != s and frames[d] == frames[s] == closure(f), "common chart at %d" % i) + adds += 1 + for n, v in rows[s].items(): + z = rows[d].get(n, Fraction(0)) + Fraction(c) * v + if z: + rows[d][n] = z + else: + rows[d].pop(n, None) + for n, f in witness["final_frames"].items(): + need(frames[n] == closure(f), "final frame " + n) + return rows, frames, profile, adds + + +def frames_over_time(witness, program, reg): + out = [(-1, closure(witness["initial_frames"][reg]))] + for i, e in enumerate(program): + if e[0] == "transport" and e[1] == reg: + out.append((i, closure(e[3]))) + return out + + +def frame_before(seq, t): + cur = seq[0][1] + for i, f in seq: + if i < t: + cur = f + return cur + + +def sweep(witness, program, target, start, head): + hosting = {target: start} + for j in range(start, len(program)): + e = program[j] + if e[0] not in ("add", "copy"): + continue + a, b = e[1], e[2] + if a in hosting or b in hosting: + for r in (a, b): + hosting.setdefault(r, j) + change = {} + seqs = {} + for r, t in hosting.items(): + if r == "C": + continue + seqs[r] = frames_over_time(witness, program, r) + if head not in frame_before(seqs[r], t): + change[r] = t + return change, seqs + + +def deliveries(witness, program): + rows = {n: {n: Fraction(1)} for n in witness["initial_frames"]} + seen = [] + coef = Fraction(0) + for i, e in enumerate(program): + if e[0] == "zero": + rows[e[1]] = {} + elif e[0] == "erase": + rows.pop(e[1]) + elif e[0] == "copy": + rows[e[1]] = dict(rows[e[2]]) + elif e[0] == "add": + if e[1] == TARGET and rows[e[2]].get(SOURCE): + carried = Fraction(e[3]) * rows[e[2]][SOURCE] + coef += carried + seen.append([i, e[2], str(carried), str(coef)]) + for n, v in rows[e[2]].items(): + z = rows[e[1]].get(n, Fraction(0)) + Fraction(e[3]) * v + if z: + rows[e[1]][n] = z + else: + rows[e[1]].pop(n, None) + return seen + + +def main(root=ROOT): + cert = json.loads((HERE / "CERTIFICATE.json").read_bytes(), object_pairs_hook=strict) + recipes_new = json.loads((HERE / "REPAIR-RECIPES.json").read_bytes(), object_pairs_hook=strict)["recipes"] + witness = read(root, f"{NATIVE}/inputs/LOWRANK-WITNESS.json") + published_recipes = read(root, f"{NATIVE}/NATIVE-RECIPES.json.gz", gz=True) + flags = read(root, "research/p104-joint-unit-flags/CERTIFICATE.json") + raw = (root / NATIVE / "vendor/native_verify.py").read_bytes() + need(hashlib.sha256(raw).hexdigest() == PINS[f"{NATIVE}/vendor/native_verify.py"], "native interpreter pin") + spec = importlib.util.spec_from_file_location("flag9_independent_native", root / NATIVE / "vendor/native_verify.py") + N = importlib.util.module_from_spec(spec) + spec.loader.exec_module(N) + + h = flags["helpers"][9] + need((h["basis"][0], "X%d" % h["source"], "Y%d" % h["target"]) == (HEAD, SOURCE, TARGET), "flag 9") + need(cert["basis_head"] == HEAD and cert["source_register"] == SOURCE, "certificate flag") + P = witness["program"] + base_rows, _, base_profile, base_adds = replay(witness, P) + bill = cert["bill"] + need(sum(base_profile.values()) == bill["published"]["transport_occurrences"] == 1410, "published transports") + need(sum(k * v for k, v in base_profile.items()) == bill["published"]["rank_mass"] == 2368, "published rank mass") + need(base_adds == bill["published"]["scalar_adds"] == 2624, "published adds") + + iso = published_recipes["label_isometry"] + dual, orth = iso["compressed_dual_gram"], iso["orthonormal_basis_compressed"] + + def to_phys(x): + bx = sum(((((row & x).bit_count()) & 1) << i) for i, row in enumerate(dual)) + return sum((((v & bx).bit_count()) & 1) << j for j, v in enumerate(orth)) + + pub_edges = {(closure(r["old"]), closure(r["new"])) for r in published_recipes["transports"]} + new_edges = {} + for rec in recipes_new: + key = (closure(rec["old"]), closure(rec["new"])) + need(key not in pub_edges and key not in new_edges, "new edge is new and unique") + need(rec["rank"] == rec["recipe"]["rank"] == abs(dim(key[1]) - dim(key[0])), "new recipe rank") + N.equal(N.recipe(rec["recipe"]), N.adjoint(N.frame(tuple(rec["old"]), 9)) + N.frame(tuple(rec["new"]), 9), "new native edge") + new_edges[key] = rec + + drop = P[500] + need(drop[0] == "transport" and drop[1] == SOURCE, "event 500") + need(HEAD not in drop[3] and (64 ^ 132) == HEAD and 64 in drop[3] and 132 in drop[3], "196 = 64 XOR 132") + source_events = [i for i, e in enumerate(P) if SOURCE in (e[1:3] if e[0] in ("add", "copy") else e[1:2])] + sseq_pub = frames_over_time(witness, P, SOURCE) + need(len(source_events) == 21 and all(HEAD in frame_before(sseq_pub, i) for i in source_events), "source span") + need(HEAD in closure(witness["final_frames"][TARGET]) and HEAD not in closure(witness["final_frames"]["Y28"]), "finals") + need(all("D28" not in e[1:3] for e in P[3125:3126]), "gap before Y28") + + used = set() + out = {} + for name in ("R0", "R1"): + prog = splice(P, cert["repairs"][name]["splices"]) + rows, _, profile, adds = replay(witness, prog) + same = sum(1 for n in base_rows if rows[n] == base_rows[n]) + need(same == len(base_rows) == 280, "every final row equals the published row") + for e in prog: + if e[0] == "transport": + key = (closure(to_phys(x) for x in e[2]), closure(to_phys(x) for x in e[3])) + if key not in pub_edges: + need(key in new_edges, "repaired edge has a committed recipe") + used.add(key) + b = bill[name] + need(b["events"] == len(prog) and b["scalar_adds"] == adds, name + " counts") + need(b["transport_occurrences"] == sum(profile.values()), name + " transports") + need(b["rank_mass"] == sum(k * v for k, v in profile.items()), name + " rank mass") + need(b["paid_profile"] == {str(k): v for k, v in sorted(profile.items())}, name + " profile") + delta = {str(k): profile.get(k, 0) - base_profile.get(k, 0) + for k in sorted(set(profile) | set(base_profile)) if profile.get(k, 0) != base_profile.get(k, 0)} + need(b["profile_delta"] == delta, name + " delta") + mass = {} + for e in prog: + if e[0] == "transport": + mass[e[1]] = mass.get(e[1], 0) + e[4] + base_mass = {} + for e in P: + if e[0] == "transport": + base_mass[e[1]] = base_mass.get(e[1], 0) + e[4] + reg_delta = {r: mass.get(r, 0) - base_mass.get(r, 0) for r in set(mass) | set(base_mass) if mass.get(r, 0) != base_mass.get(r, 0)} + need(b["register_rank_mass_delta"] == reg_delta, name + " register mass") + out[name] = prog + need(used == set(new_edges), "every committed recipe used") + + need(bill["R0"]["added_rank_mass"] == 2 and bill["R0"]["added_events"] == 1, "R0 bill") + need(bill["R0"]["register_rank_mass_delta"] == {"D28": 2}, "R0 register") + need(bill["R0"]["profile_delta"] == {"1": -1, "2": 2, "4": 1, "5": -1}, "R0 profile") + need(bill["R1"]["added_rank_mass"] == 2 and bill["R1"]["added_events"] == 0, "R1 bill") + need(bill["R1"]["register_rank_mass_delta"] == {"Y23": 2}, "R1 register") + need(bill["R1"]["profile_delta"] == {"5": -1, "7": 1}, "R1 profile") + + hc = cert["head_cohosting"] + for name, prog, update in (("R0", out["R0"], 3124), ("R1", out["R1"], 3633)): + tseq = frames_over_time(witness, prog, TARGET) + sseq = frames_over_time(witness, prog, SOURCE) + adds = [i for i, e in enumerate(prog) if e[0] == "add" and e[1] == TARGET] + co = [i for i in adds if HEAD in frame_before(tseq, i) and HEAD in frame_before(sseq, i)] + block = hc[name] + need(co == block["cohosted_target_updates"] == [update], name + " co-host index") + need(block["source_spans_head"] and dim(frame_before(sseq, update)) == 9, name + " source rank") + need(deliveries(witness, prog) == block["source_delivery_into_target"], name + " delivery") + need(hc["published_head_hosting_target_updates"] == [], "published head-free") + need(hc["R0"]["source_delivery_into_target"] == [[3124, "D28", "-1/2", "-1/2"]], "R0 coefficient") + + finals = {n: closure(f) for n, f in witness["final_frames"].items()} + table = {row["event"]: row for row in cert["forced_hosting"]["table"]} + need(sorted(table) == [i for i, e in enumerate(P) if e[0] == "add" and e[1] == TARGET], "every target update") + obstructed = 0 + for t0, row in table.items(): + change, seqs = sweep(witness, P, TARGET, t0, HEAD) + hard = sorted([[r, t] for r, t in change.items() if r in finals and HEAD not in finals[r]], key=lambda x: (x[1], x[0])) + need(row["slot_independent_obstructions"] == len(hard), "obstruction count at %d" % t0) + need(row["first_obstruction"] == (hard[0] + ["final frame excludes head"] if hard else None), "first obstruction at %d" % t0) + need(row["admissible"] is False, "not admissible at %d" % t0) + if hard: + obstructed += 1 + need(obstructed == 9 and table[3124]["first_obstruction"][0] == "Y28", "closure verdict") + need(cert["selected_kappa"] == "0.001672660197076918" and cert["no_new_kappa"] is True, "kappa") + print(MARKER) + + +if __name__ == "__main__": + main(Path(sys.argv[1]).resolve() if len(sys.argv) > 1 else ROOT) diff --git a/research/p104-flag9-head-step-repair/test_package.py b/research/p104-flag9-head-step-repair/test_package.py new file mode 100644 index 0000000000..ba94c34d8e --- /dev/null +++ b/research/p104-flag9-head-step-repair/test_package.py @@ -0,0 +1,147 @@ +#!/usr/bin/env python3 +"""Behavioural tests: corruption, negative controls and read-only replay. + +Each case copies the package and its pinned inputs into a temporary tree, +mutates one thing and runs both scanners there under python -O. The scanners +must reject every mutation; the clean tree must pass and stay byte-identical. +""" + +import concurrent.futures +import hashlib +import json +import shutil +import subprocess +import sys +import tempfile +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PKG = HERE.relative_to(ROOT).as_posix() +NATIVE = "research/p104-native-channel" +COPY = [ + f"{NATIVE}/inputs/LOWRANK-WITNESS.json", + f"{NATIVE}/inputs/P104-FIXTURE.json", + f"{NATIVE}/NATIVE-RECIPES.json.gz", + f"{NATIVE}/check_native.py", + f"{NATIVE}/vendor/native_verify.py", + "research/p104-joint-unit-flags/CERTIFICATE.json", +] +SCANNERS = ("verify.py", "independent.py") + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def tree(base): + for rel in COPY: + (base / rel).parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / rel, base / rel) + shutil.copytree(HERE, base / PKG, ignore=shutil.ignore_patterns("__pycache__")) + return base + + +def run(base, scanner): + p = subprocess.run([sys.executable, "-I", "-O", "-Werror", "-B", str(base / PKG / scanner), str(base)], + capture_output=True, text=True, timeout=180) + return p.returncode, p.stdout + p.stderr + + +def digest(base): + return {p.relative_to(base).as_posix(): hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(base.rglob("*")) if p.is_file()} + + +def edit_json(path, fn): + data = json.loads(path.read_text()) + fn(data) + path.write_text(json.dumps(data, indent=2, sort_keys=True) + "\n") + + +def cert_field(fn): + return lambda base: edit_json(base / PKG / "CERTIFICATE.json", fn) + + +def dup_key(base): + p = base / PKG / "CERTIFICATE.json" + text = p.read_text() + p.write_text(text.replace('"basis_head": 196,', '"basis_head": 196,\n "basis_head": 196,', 1)) + + +def flip_witness(base): + p = base / f"{NATIVE}/inputs/LOWRANK-WITNESS.json" + raw = bytearray(p.read_bytes()) + raw[len(raw) // 2] ^= 1 + p.write_bytes(bytes(raw)) + + +def bad_phase(base): + p = base / PKG / "REPAIR-RECIPES.json" + data = json.loads(p.read_text()) + left = data["recipes"][0]["recipe"]["left"] + left["phase"] = (left["phase"] + 1) % 4 + p.write_text(json.dumps(data, indent=1, sort_keys=True) + "\n") + + +def drop_return(c): + for row in c["repairs"]["R0"]["splices"]: + if row["published_range"][0] == 3124: + row["events"] = row["events"][:1] + + +def undercharge(c): + for row in c["repairs"]["R0"]["splices"]: + if row["published_range"][0] == 3489: + row["events"][0][4] = 1 + + +CASES = { + "bill_rank_mass": (cert_field(lambda c: c["bill"]["R0"].__setitem__("rank_mass", 2369)), None), + "bill_profile_delta": (cert_field(lambda c: c["bill"]["R0"]["profile_delta"].__setitem__("2", 9)), None), + "cohosted_updates": (cert_field(lambda c: c["head_cohosting"]["R0"].__setitem__("cohosted_target_updates", [])), None), + "delivery": (cert_field(lambda c: c["head_cohosting"]["R0"]["source_delivery_into_target"][-1].__setitem__(2, "1/4")), None), + "admissible_3124": (cert_field(lambda c: [r.__setitem__("admissible", True) for r in c["forced_hosting"]["table"] if r["event"] == 3124]), None), + "duplicate_key": (dup_key, "duplicate JSON key"), + "witness_byte": (flip_witness, None), + "recipe_phase": (bad_phase, None), + "control_without_drop": (cert_field(drop_return), "common chart"), + "control_undercharge": (cert_field(undercharge), "frame gap"), +} + + +def case(name): + mutate, expect = CASES[name] + with tempfile.TemporaryDirectory(prefix="flag9-repair-") as d: + base = tree(Path(d)) + mutate(base) + for scanner in SCANNERS: + code, out = run(base, scanner) + need(code != 0, f"{name}: {scanner} accepted a mutation") + need("PASS_" not in out, f"{name}: {scanner} printed a pass marker") + if expect: + need(expect in out, f"{name}: {scanner} rejected for the wrong reason: {out[-400:]}") + return name + + +def clean(): + with tempfile.TemporaryDirectory(prefix="flag9-repair-") as d: + base = tree(Path(d)) + before = digest(base) + for scanner in SCANNERS: + code, out = run(base, scanner) + need(code == 0 and "PASS_P104_FLAG9_HEAD_STEP_REPAIR" in out, f"clean {scanner}: {out[-500:]}") + need(digest(base) == before, "scanners modified the tree") + + +def main(): + clean() + with concurrent.futures.ThreadPoolExecutor(max_workers=4) as pool: + done = list(pool.map(case, sorted(CASES))) + need(len(done) == len(CASES), "all cases ran") + print(f"PASS_P104_FLAG9_HEAD_STEP_REPAIR_TESTS cases={len(CASES)} clean_read_only=1 scanners=2") + + +if __name__ == "__main__": + main() diff --git a/research/p104-flag9-head-step-repair/verify.py b/research/p104-flag9-head-step-repair/verify.py new file mode 100644 index 0000000000..b608b62b73 --- /dev/null +++ b/research/p104-flag9-head-step-repair/verify.py @@ -0,0 +1,517 @@ +#!/usr/bin/env python3 +"""Read-only replay of the flag-9 head-step repair bill. + +Applies two changed schedules to the published 4,058-event P104 witness in +memory, assembles their native recipe sets from the published recipes plus +the committed new-edge recipes, and runs the published native checker's +complete validate() on each. It then recomputes the bill, the head +co-hosting facts, the X4 span correction, and the forced-hosting closure of +every Y23 update, and compares the receipt with CERTIFICATE.json. Admission +uses need() and stays active under python -O. Nothing is written. +""" + +import bisect +import copy +import gzip +import hashlib +import importlib.util +import json +import sys +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +NATIVE = "research/p104-native-channel" +PINS = { + f"{NATIVE}/inputs/LOWRANK-WITNESS.json": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e", + f"{NATIVE}/inputs/P104-FIXTURE.json": "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4", + f"{NATIVE}/NATIVE-RECIPES.json.gz": "a1c4d83d3d5fe1338e99b59272e8cf5d43244c33888597da340b2aa7fef5b3e8", + f"{NATIVE}/check_native.py": "e67b874a061a4a28007b9a0fabaf30c8db4a587b1e1c7dd9396c77ff1e3a9fe6", + f"{NATIVE}/vendor/native_verify.py": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38", + "research/p104-joint-unit-flags/CERTIFICATE.json": "a98126428a8da6eae91c50afcc42e014a284c82b554ef77e5b3a34fc6d228128", +} +FLAG_INDEX = 9 +HEAD = 196 +SOURCE = "X4" +TARGET = "Y23" +SELECTED_KAPPA = "0.001672660197076918" +MARKER = ( + "PASS_P104_FLAG9_HEAD_STEP_REPAIR flag=9 head=196 delivering_update=3124 " + "R0_added_events=1 R0_added_rank_mass=2 R0_mass_register=D28 " + "R1_added_events=0 R1_added_rank_mass=2 R1_mass_register=Y23 " + "profile_R0=-H1+2H2+H4-H5 profile_R1=H7-H5 " + "native_validate=PASS updates_obstructed=9/9 source_events_keep_head=21/21 " + "no_new_kappa" +) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def pairs_unique(pairs): + out = {} + for key, value in pairs: + need(key not in out, "duplicate JSON key: " + str(key)) + out[key] = value + return out + + +def loads(raw): + return json.loads(raw, object_pairs_hook=pairs_unique) + + +def pinned_bytes(root, rel): + raw = (root / rel).read_bytes() + need(hashlib.sha256(raw).hexdigest() == PINS[rel], "pinned input changed: " + rel) + return raw + + +def load_checker(root): + pinned_bytes(root, f"{NATIVE}/check_native.py") + pinned_bytes(root, f"{NATIVE}/vendor/native_verify.py") + name = "flag9_repair_check_native" + spec = importlib.util.spec_from_file_location(name, root / NATIVE / "check_native.py") + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def load_inputs(root): + witness = loads(pinned_bytes(root, f"{NATIVE}/inputs/LOWRANK-WITNESS.json")) + fixture = loads(pinned_bytes(root, f"{NATIVE}/inputs/P104-FIXTURE.json"))["section4_explicit_P104"] + recipes = loads(gzip.decompress(pinned_bytes(root, f"{NATIVE}/NATIVE-RECIPES.json.gz"))) + flags = loads(pinned_bytes(root, "research/p104-joint-unit-flags/CERTIFICATE.json")) + return witness, fixture, recipes, flags + + +def span(vectors): + out = {0} + for v in vectors: + out |= {x ^ v for x in tuple(out)} + return frozenset(out) + + +def dim(vectors): + n = len(span(vectors)) + need(n and n & (n - 1) == 0, "frame span is not a subspace") + return n.bit_length() - 1 + + +def rank_of_independent(vectors): + piv = {} + for x in vectors: + while x: + j = x.bit_length() - 1 + if j in piv: + x ^= piv[j] + else: + piv[j] = x + break + return len(piv) + + +def canon(values): + piv = {} + for x in values: + while x: + j = x.bit_length() - 1 + if j in piv: + x ^= piv[j] + else: + piv[j] = x + break + for j in sorted(piv): + for k in piv: + if k > j and piv[k] >> j & 1: + piv[k] ^= piv[j] + return tuple(piv[j] for j in sorted(piv, reverse=True)) + + +def physical_map(recipes): + iso = recipes["label_isometry"] + dual = iso["compressed_dual_gram"] + orth = iso["orthonormal_basis_compressed"] + + def mv(rows, x): + return sum((((row & x).bit_count()) & 1) << i for i, row in enumerate(rows)) + + def convert(x): + return sum(((x & mv(dual, v)).bit_count() & 1) << j for j, v in enumerate(orth)) + + return lambda frame: canon(convert(x) for x in frame) + + +def apply_splices(program, splices): + out = list(program) + last = len(program) + 1 + for row in sorted(splices, key=lambda r: -r["published_range"][0]): + start, stop = row["published_range"] + need(0 <= start < stop <= len(program) and stop <= last, "ordered disjoint splices") + for k, old in enumerate(row["published"]): + need(program[start + k] == old, "splice binds published event %d" % (start + k)) + need(len(row["published"]) == stop - start, "splice covers its range") + out[start:stop] = copy.deepcopy(row["events"]) + last = start + return out + + +def check_program_frames(witness, program): + frames = {n: span(f) for n, f in witness["initial_frames"].items()} + profile = {} + adds = 0 + for i, e in enumerate(program): + op = e[0] + if op == "transport": + _, reg, old, new, k = e + a, b = span(old), span(new) + need(frames[reg] == a, "transport before-frame continuity at %d" % i) + need(a <= b or b <= a, "nested transport at %d" % i) + need(k == abs(dim(new) - dim(old)) and k > 0, "paid rank equals frame gap at %d" % i) + frames[reg] = b + profile[k] = profile.get(k, 0) + 1 + elif op == "zero": + frames[e[1]] = span(e[2]) + elif op == "erase": + frames.pop(e[1]) + elif op == "copy": + need(frames[e[1]] == frames[e[2]] == span(e[3]), "copy chart at %d" % i) + elif op == "add": + _, dst, src, _a, fr = e + need(frames[dst] == frames[src] == span(fr), "common chart at %d" % i) + adds += 1 + else: + need(False, "opcode at %d" % i) + for name, final in witness["final_frames"].items(): + need(frames[name] == span(final), "final frame " + name) + return profile, adds + + +def assemble(recipes, program, new_recipes, physical): + pub = {(tuple(r["old"]), tuple(r["new"])): r for r in recipes["transports"]} + extra = {(tuple(r["old"]), tuple(r["new"])): r for r in new_recipes} + need(len(extra) == len(new_recipes), "unique new-edge recipes") + need(not (set(pub) & set(extra)), "new recipes are new edges") + edges = {} + for i, e in enumerate(program): + if e[0] == "transport": + edges.setdefault((physical(e[2]), physical(e[3])), []).append(i) + used_new = set() + out = [] + for key in sorted(edges): + if key in pub: + rec = dict(pub[key]) + else: + need(key in extra, "missing native recipe for new edge") + rec = dict(extra[key]) + used_new.add(key) + rec["events"] = edges[key] + out.append(rec) + profile = {} + for rec in out: + profile[rec["rank"]] = profile.get(rec["rank"], 0) + len(rec["events"]) + c = dict(recipes) + c["transports"] = out + c["paid_profile"] = {str(k): v for k, v in sorted(profile.items())} + return c, used_new, len(set(pub) - set(edges)) + + +def bill(result, program, n_edges): + profile = {str(k): v for k, v in sorted(result["paid_profile"].items())} + return { + "events": len(program), + "scalar_adds": result["scalar_events"]["add"], + "private_events": {k: result["scalar_events"][k] for k in ("zero", "copy", "erase")}, + "transport_occurrences": sum(int(v) for v in profile.values()), + "rank_mass": result["rank_mass"], + "paid_profile": profile, + "distinct_native_edges": n_edges, + "endpoint_adapters": result["intrinsic_endpoint_adapters"], + "formal_boundary_columns": result["formal_boundary_columns"], + } + + +def profile_delta(a, b): + keys = sorted({int(k) for k in a["paid_profile"]} | {int(k) for k in b["paid_profile"]}) + out = {} + for k in keys: + d = b["paid_profile"].get(str(k), 0) - a["paid_profile"].get(str(k), 0) + if d: + out[str(k)] = d + return out + + +def frame_history(witness, program): + hist = {n: [(-1, span(f))] for n, f in witness["initial_frames"].items()} + for i, e in enumerate(program): + if e[0] == "transport": + hist[e[1]].append((i, span(e[3]))) + elif e[0] == "zero": + hist.setdefault(e[1], []).append((i, span(e[2]))) + return hist + + +def frame_at(hist, reg, t): + h = hist[reg] + k = bisect.bisect_left([x[0] for x in h], t) - 1 + return h[k][1] + + +def register_mass(program): + mass = {} + for e in program: + if e[0] == "transport": + mass[e[1]] = mass.get(e[1], 0) + e[4] + return mass + + +def deliveries(witness, program): + state = {n: {n: Fraction(1)} for n in witness["initial_frames"]} + seen = [] + for i, e in enumerate(program): + op = e[0] + if op == "zero": + state[e[1]] = {} + elif op == "erase": + state.pop(e[1]) + elif op == "copy": + state[e[1]] = dict(state[e[2]]) + elif op == "add": + _, dst, src, a, _f = e + if dst == TARGET: + carried = Fraction(a) * state[src].get(SOURCE, Fraction(0)) + before = state[TARGET].get(SOURCE, Fraction(0)) + if carried: + seen.append([i, src, str(carried), str(before + carried)]) + for name, v in list(state[src].items()): + z = state[dst].get(name, Fraction(0)) + Fraction(a) * v + if z: + state[dst][name] = z + else: + state[dst].pop(name, None) + return state, seen + + +def closure_table(witness, program, target, head): + hist = frame_history(witness, program) + finals = {n: span(f) for n, f in witness["final_frames"].items()} + monotone = {r: r != "C" and all(a[1] <= b[1] for a, b in zip(h, h[1:])) for r, h in hist.items()} + touch = {} + for i, e in enumerate(program): + if e[0] in ("add", "copy"): + for r in (e[1], e[2]): + touch.setdefault(r, []).append(i) + rows = [] + for i, e in enumerate(program): + if e[0] != "add" or e[1] != target: + continue + host = {target: i} + work = [target] + while work: + r = work.pop() + t = host[r] + for j in touch.get(r, []): + if j < t: + continue + other = program[j][2] if program[j][1] == r else program[j][1] + if other not in host or host[other] > j: + host[other] = j + work.append(other) + change = {r: t for r, t in host.items() if head not in frame_at(hist, r, t)} + hard, slot, private = [], [], [] + for r, t in sorted(change.items(), key=lambda x: (x[1], x[0])): + if not monotone.get(r, False): + private.append([r, t]) + elif r in finals and head not in finals[r]: + hard.append([r, t, "final frame excludes head"]) + elif not any(-1 < j < t for j, _ in hist[r]): + slot.append([r, t]) + rows.append({ + "event": i, + "partner": e[2], + "must_change": len(change), + "slot_independent_obstructions": len(hard), + "first_obstruction": hard[0] if hard else None, + "registers_without_prior_transport": len(slot), + "private_registers_forced": private, + "admissible": not hard and not slot and not private, + "forced": {r: t for r, t in sorted(change.items(), key=lambda x: (x[1], x[0]))} if not hard else None, + }) + return rows + + +def cohost_facts(witness, program, published_hist_target): + hist = frame_history(witness, program) + adds = [i for i, e in enumerate(program) if e[0] == "add" and e[1] == TARGET] + hosting = [i for i in adds if HEAD in frame_at(hist, TARGET, i) and HEAD in frame_at(hist, SOURCE, i)] + need(len(hosting) == 1, "one co-hosted target update") + last = hosting[0] + later = [i for i, e in enumerate(program) if i > last and SOURCE in e[1:3]] + _state, seen = deliveries(witness, program) + return { + "cohosted_target_updates": hosting, + "update": last, + "partner": program[last][2], + "chart": program[last][4], + "chart_rank": dim(program[last][4]), + "source_frame_rank": rank_of_independent(frame_at(hist, SOURCE, last) - {0}), + "source_spans_head": HEAD in frame_at(hist, SOURCE, last), + "source_events_after_update": later, + "source_delivery_into_target": seen, + "published_head_hosting_target_updates": [ + i for i, e in enumerate(witness["program"]) + if e[0] == "add" and e[1] == TARGET and HEAD in frame_at(published_hist_target, TARGET, i) + ], + } + + +def receipt(root, cert, new_recipes): + ck = load_checker(root) + witness, fixture, recipes, flags = load_inputs(root) + helper = flags["helpers"][FLAG_INDEX] + head = helper["basis"][0] + source, target = "X%d" % helper["source"], "Y%d" % helper["target"] + need((source, target, head) == (SOURCE, TARGET, HEAD), "flag 9 identity") + physical = physical_map(recipes) + program = witness["program"] + published = ck.validate(recipes, witness, fixture, False) + need(published["transports"] == len(recipes["transports"]) == 740, "published native edges") + out = {"published": bill(published, program, published["transports"])} + pub_hist = frame_history(witness, program) + repaired = {} + used = set() + for name in ("R0", "R1"): + prog = apply_splices(program, cert["repairs"][name]["splices"]) + check_program_frames(witness, prog) + w2 = dict(witness) + w2["program"] = prog + c2, used_new, dropped = assemble(recipes, prog, new_recipes, physical) + used |= used_new + result = ck.validate(c2, w2, fixture, False) + out[name] = bill(result, prog, result["transports"]) + out[name]["new_native_edges"] = len(used_new) + out[name]["dropped_native_edges"] = dropped + repaired[name] = prog + need(len(used) == len(new_recipes), "every committed recipe is used") + pub_mass = register_mass(program) + for name in ("R0", "R1"): + out[name]["profile_delta"] = profile_delta(out["published"], out[name]) + for key in ("events", "scalar_adds", "transport_occurrences", "rank_mass"): + out[name]["added_" + key] = out[name][key] - out["published"][key] + mass = register_mass(repaired[name]) + out[name]["register_rank_mass_delta"] = { + r: mass.get(r, 0) - pub_mass.get(r, 0) + for r in sorted(set(mass) | set(pub_mass)) + if mass.get(r, 0) != pub_mass.get(r, 0) + } + facts = cohost_facts(witness, repaired[name], pub_hist) + out[name]["cohosting"] = facts + + # Literal generator drop versus span. 196 = 64 XOR 132. + drop = program[500] + need(drop[:2] == ["transport", SOURCE], "event 500 is the X4 transport") + after = drop[3] + need(HEAD not in after and 64 in after and 132 in after and (64 ^ 132) == HEAD, "literal drop keeps 196 in span") + source_frames = pub_hist[SOURCE] + source_events = [ + i for i, e in enumerate(program) + if SOURCE in (e[1:3] if e[0] in ("add", "copy") else e[1:2]) + ] + need(all(HEAD in sp for _t, sp in source_frames), "X4 spans 196 in every source frame") + need(all(HEAD in frame_at(pub_hist, SOURCE, i) for i in source_events), "X4 spans 196 at every source event") + need(len(source_events) == 21 and len(source_frames) == 7, "source event and frame counts") + target_final = span(witness["final_frames"][TARGET]) + partner_final = span(witness["final_frames"]["Y28"]) + need(HEAD in target_final and HEAD not in partner_final, "Y23 final hosts 196 and Y28 final does not") + between = [e for e in program[3125:3126]] + need(all("D28" not in e[1:3] for e in between), "no D28 event between the delivering ADD and Y28") + + gain = register_mass(program) + floor = [r for r in witness["initial_frames"] + if gain.get(r, 0) == dim(witness["final_frames"][r]) - dim(witness["initial_frames"][r])] + need(len(floor) == len(witness["initial_frames"]) == 280, "every non-private register at its rank floor") + table = closure_table(witness, program, TARGET, HEAD) + return { + "schema_version": 1, + "claim_id": "p104-flag9-head-step-repair", + "pinned_main": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "flag_index": FLAG_INDEX, + "source_register": SOURCE, + "target_register": TARGET, + "basis_head": HEAD, + "source_span": { + "head_in_every_source_frame": True, + "source_frame_count": len(source_frames), + "source_event_count": len(source_events), + "literal_drop_event": 500, + "literal_drop_after_lists_head": False, + "span_relation": "196 = 64 XOR 132", + }, + "repairs": cert["repairs"], + "bill": {k: {kk: vv for kk, vv in out[k].items() if kk != "cohosting"} for k in ("published", "R0", "R1")}, + "head_cohosting": { + "published_head_hosting_target_updates": out["R0"]["cohosting"]["published_head_hosting_target_updates"], + "R0": {k: v for k, v in out["R0"]["cohosting"].items() if k != "published_head_hosting_target_updates"}, + "R1": {k: v for k, v in out["R1"]["cohosting"].items() if k != "published_head_hosting_target_updates"}, + }, + "forced_hosting": { + "non_private_registers_at_rank_floor": len(floor), + "table": table, + "admissible_updates": [row["event"] for row in table if row["admissible"]], + "slot_independently_obstructed_updates": [row["event"] for row in table if row["slot_independent_obstructions"]], + }, + "selected_kappa": SELECTED_KAPPA, + "no_new_kappa": True, + } + + +def admit(root, cert, new_recipes): + got = json.loads(json.dumps(receipt(root, cert, new_recipes))) + need(got == cert, "receipt differs from committed certificate") + b, hc, fh = cert["bill"], cert["head_cohosting"], cert["forced_hosting"] + pub, r0, r1 = b["published"], b["R0"], b["R1"] + need(pub["events"] == 4058 and pub["scalar_adds"] == 2624, "published counts") + need(pub["transport_occurrences"] == 1410 and pub["rank_mass"] == 2368, "published mass") + need(pub["distinct_native_edges"] == 740, "published edges") + need([r0["added_" + k] for k in ("events", "scalar_adds", "transport_occurrences", "rank_mass")] == [1, 0, 1, 2], "R0 bill") + need(r0["profile_delta"] == {"1": -1, "2": 2, "4": 1, "5": -1}, "R0 profile delta") + need(r0["register_rank_mass_delta"] == {"D28": 2}, "R0 mass sits on D28") + need(r0["distinct_native_edges"] == 742, "R0 edges") + need([r1["added_" + k] for k in ("events", "scalar_adds", "transport_occurrences", "rank_mass")] == [0, 0, 0, 2], "R1 bill") + need(r1["profile_delta"] == {"5": -1, "7": 1}, "R1 profile delta") + need(r1["register_rank_mass_delta"] == {"Y23": 2}, "R1 mass sits on Y23") + need(r1["distinct_native_edges"] == 741, "R1 edges") + need(hc["published_head_hosting_target_updates"] == [], "published updates are head-free") + r0h, r1h = hc["R0"], hc["R1"] + need(r0h["cohosted_target_updates"] == [3124] and r0h["partner"] == "D28", "R0 co-hosts at 3124") + need(r0h["chart"] == [447, 127, 192, 196] and r0h["chart_rank"] == 4, "R0 chart") + need(r0h["source_spans_head"] and r0h["source_frame_rank"] == 9, "R0 source still spans the head at full rank") + need(r0h["source_events_after_update"] == [3696, 3803, 3855, 3959, 4010], "R0 source still live") + need(r0h["source_delivery_into_target"] == [[3124, "D28", "-1/2", "-1/2"]], "R0 delivers -1/2 once") + need(r1h["update"] == 3633 and r1h["partner"] == "D28" and r1h["chart_rank"] == 9, "R1 co-hosts in the full chart") + need(r1h["source_spans_head"] and r1h["source_delivery_into_target"] == [[3633, "D28", "-1/2", "-1/2"]], "R1 delivery") + need(r1h["source_events_after_update"] == [3695, 3802, 3854, 3958, 4009], "R1 source still live") + need(fh["admissible_updates"] == [], "no zero-mass admissible update") + need(len(fh["slot_independently_obstructed_updates"]) == 9, "all nine updates obstructed") + row = [r for r in fh["table"] if r["event"] == 3124][0] + need(row["first_obstruction"] == ["Y28", 3126, "final frame excludes head"], "3124 forces Y28") + need(row["slot_independent_obstructions"] == 5, "3124 has five final-excluding registers") + need(cert["source_span"]["source_frame_count"] == 7 and cert["source_span"]["source_event_count"] == 21, "span counts") + need(cert["source_span"]["span_relation"] == "196 = 64 XOR 132", "span correction") + need(fh["non_private_registers_at_rank_floor"] == 280, "rank floor") + need(cert["selected_kappa"] == SELECTED_KAPPA and cert["no_new_kappa"] is True, "kappa unchanged") + return got + + +def main(root=ROOT): + cert = loads((HERE / "CERTIFICATE.json").read_bytes()) + new_recipes = loads((HERE / "REPAIR-RECIPES.json").read_bytes())["recipes"] + admit(root, cert, new_recipes) + print(MARKER) + + +if __name__ == "__main__": + main(Path(sys.argv[1]).resolve() if len(sys.argv) > 1 else ROOT)