From cc77db2b62d1eaa6a1f7b9ffec7e694a910bba54 Mon Sep 17 00:00:00 2001 From: Wentao Li Date: Sun, 18 Oct 2026 03:55:44 +0000 Subject: [PATCH 1/2] Research: price a flag-43 head-step repair at zero added channel cost (no new kappa) Retarget nine published transports of Y59, D17, Y103 and D28 so that Y59's last update (event 3364, the ADD that settles X21's final coefficient) runs in a chart co-hosting basis head 15 while X21 is full and live. The published check_native.validate() passes on the repaired word with eight newly lowered edges. Events, ADDs, transport occurrences, rank mass and distinct edges are unchanged; the paid profile moves by -3H1+5H2-H3-H4, majorized by the published ranks. A two-register comparison (R1) costs one added transport. In the order-preserving zero-added-rank class, 3364 is the only head-hostable Y59 update and forces exactly these four registers. --- .../CERTIFICATE.json | 1368 +++++++++++++++++ .../p104-flag43-head-step-repair/NOTICE.md | 12 + .../p104-flag43-head-step-repair/PROOF.md | 238 +++ .../p104-flag43-head-step-repair/README.md | 123 ++ .../REPAIR-RECIPES.json | 880 +++++++++++ .../p104-flag43-head-step-repair/SOURCES.json | 81 + .../p104-flag43-head-step-repair/TASK.json | 102 ++ .../p104-flag43-head-step-repair/VERIFY.json | 52 + .../p104-flag43-head-step-repair/build.py | 125 ++ .../independent.py | 305 ++++ .../test_package.py | 155 ++ .../p104-flag43-head-step-repair/verify.py | 458 ++++++ 12 files changed, 3899 insertions(+) create mode 100644 research/p104-flag43-head-step-repair/CERTIFICATE.json create mode 100644 research/p104-flag43-head-step-repair/NOTICE.md create mode 100644 research/p104-flag43-head-step-repair/PROOF.md create mode 100644 research/p104-flag43-head-step-repair/README.md create mode 100644 research/p104-flag43-head-step-repair/REPAIR-RECIPES.json create mode 100644 research/p104-flag43-head-step-repair/SOURCES.json create mode 100644 research/p104-flag43-head-step-repair/TASK.json create mode 100644 research/p104-flag43-head-step-repair/VERIFY.json create mode 100644 research/p104-flag43-head-step-repair/build.py create mode 100644 research/p104-flag43-head-step-repair/independent.py create mode 100644 research/p104-flag43-head-step-repair/test_package.py create mode 100644 research/p104-flag43-head-step-repair/verify.py diff --git a/research/p104-flag43-head-step-repair/CERTIFICATE.json b/research/p104-flag43-head-step-repair/CERTIFICATE.json new file mode 100644 index 0000000000..4047416534 --- /dev/null +++ b/research/p104-flag43-head-step-repair/CERTIFICATE.json @@ -0,0 +1,1368 @@ +{ + "basis_head": 15, + "bill": { + "R0": { + "added_events": 0, + "added_rank_mass": 0, + "added_scalar_adds": 0, + "added_transport_occurrences": 0, + "distinct_native_edges": 740, + "dropped_native_edges": 8, + "endpoint_adapters": 208, + "events": 4058, + "formal_boundary_columns": 280, + "majorized_by_published": true, + "new_native_edges": 8, + "paid_profile": { + "1": 1071, + "2": 63, + "3": 85, + "4": 103, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "profile_delta": { + "1": -3, + "2": 5, + "3": -1, + "4": -1 + }, + "rank_mass": 2368, + "registers_changed": [ + "D17", + "D28", + "Y103", + "Y59" + ], + "relabelled_add_charts": [ + 3364, + 3366, + 3462 + ], + "retargeted_ranks_published": [ + 1, + 1, + 1, + 1, + 1, + 3, + 2, + 4, + 3 + ], + "retargeted_ranks_repaired": [ + 2, + 2, + 2, + 2, + 1, + 2, + 1, + 3, + 2 + ], + "retargeted_transports": [ + 3362, + 3363, + 3365, + 3460, + 3461, + 3525, + 3569, + 3612, + 3634 + ], + "scalar_adds": 2624, + "transport_occurrences": 1410 + }, + "R1": { + "added_events": 1, + "added_rank_mass": 0, + "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": 1074, + "2": 60, + "3": 86, + "4": 103, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "profile_delta": { + "2": 2, + "4": -1 + }, + "rank_mass": 2368, + "scalar_adds": 2624, + "transport_occurrences": 1411 + }, + "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-flag43-head-step-repair", + "flag_index": 43, + "forced_hosting": { + "admissible_updates": [ + 3364 + ], + "non_private_registers_at_rank_floor": 280, + "slot_independently_obstructed_updates": [ + 223, + 224, + 225, + 226, + 227, + 2099, + 2191, + 2275, + 2341, + 2393, + 2698, + 2891, + 3076, + 3231 + ], + "table": [ + { + "admissible": false, + "event": 223, + "first_obstruction": [ + "Y67", + 264, + "final frame excludes head" + ], + "forced": null, + "must_change": 274, + "partner": "Q1", + "private_registers_forced": [ + [ + "C", + 2462 + ] + ], + "registers_without_prior_transport": 106, + "slot_independent_obstructions": 56 + }, + { + "admissible": false, + "event": 224, + "first_obstruction": [ + "Y67", + 265, + "final frame excludes head" + ], + "forced": null, + "must_change": 273, + "partner": "Q2", + "private_registers_forced": [ + [ + "C", + 2462 + ] + ], + "registers_without_prior_transport": 102, + "slot_independent_obstructions": 56 + }, + { + "admissible": false, + "event": 225, + "first_obstruction": [ + "Y67", + 267, + "final frame excludes head" + ], + "forced": null, + "must_change": 269, + "partner": "Q4", + "private_registers_forced": [ + [ + "C", + 2462 + ] + ], + "registers_without_prior_transport": 92, + "slot_independent_obstructions": 56 + }, + { + "admissible": false, + "event": 226, + "first_obstruction": [ + "Y67", + 268, + "final frame excludes head" + ], + "forced": null, + "must_change": 266, + "partner": "Q5", + "private_registers_forced": [ + [ + "C", + 2462 + ] + ], + "registers_without_prior_transport": 87, + "slot_independent_obstructions": 56 + }, + { + "admissible": false, + "event": 227, + "first_obstruction": [ + "Y67", + 268, + "final frame excludes head" + ], + "forced": null, + "must_change": 260, + "partner": "Q6", + "private_registers_forced": [ + [ + "C", + 2462 + ] + ], + "registers_without_prior_transport": 83, + "slot_independent_obstructions": 56 + }, + { + "admissible": false, + "event": 2099, + "first_obstruction": [ + "Y96", + 2103, + "final frame excludes head" + ], + "forced": null, + "must_change": 140, + "partner": "D23", + "private_registers_forced": [ + [ + "C", + 2468 + ] + ], + "registers_without_prior_transport": 28, + "slot_independent_obstructions": 56 + }, + { + "admissible": false, + "event": 2191, + "first_obstruction": [ + "Y96", + 2194, + "final frame excludes head" + ], + "forced": null, + "must_change": 140, + "partner": "D20", + "private_registers_forced": [ + [ + "C", + 2473 + ] + ], + "registers_without_prior_transport": 19, + "slot_independent_obstructions": 56 + }, + { + "admissible": false, + "event": 2275, + "first_obstruction": [ + "Y26", + 2336, + "final frame excludes head" + ], + "forced": null, + "must_change": 140, + "partner": "D10", + "private_registers_forced": [ + [ + "C", + 2473 + ] + ], + "registers_without_prior_transport": 13, + "slot_independent_obstructions": 56 + }, + { + "admissible": false, + "event": 2341, + "first_obstruction": [ + "Y56", + 2387, + "final frame excludes head" + ], + "forced": null, + "must_change": 140, + "partner": "D5", + "private_registers_forced": [ + [ + "C", + 2473 + ] + ], + "registers_without_prior_transport": 9, + "slot_independent_obstructions": 56 + }, + { + "admissible": false, + "event": 2393, + "first_obstruction": [ + "Y22", + 2638, + "final frame excludes head" + ], + "forced": null, + "must_change": 133, + "partner": "D17", + "private_registers_forced": [ + [ + "C", + 2497 + ] + ], + "registers_without_prior_transport": 4, + "slot_independent_obstructions": 53 + }, + { + "admissible": false, + "event": 2698, + "first_obstruction": [ + "Y96", + 2706, + "final frame excludes head" + ], + "forced": null, + "must_change": 45, + "partner": "D23", + "private_registers_forced": [], + "registers_without_prior_transport": 0, + "slot_independent_obstructions": 17 + }, + { + "admissible": false, + "event": 2891, + "first_obstruction": [ + "Y96", + 2897, + "final frame excludes head" + ], + "forced": null, + "must_change": 31, + "partner": "D20", + "private_registers_forced": [], + "registers_without_prior_transport": 0, + "slot_independent_obstructions": 12 + }, + { + "admissible": false, + "event": 3076, + "first_obstruction": [ + "Y26", + 3220, + "final frame excludes head" + ], + "forced": null, + "must_change": 17, + "partner": "D10", + "private_registers_forced": [], + "registers_without_prior_transport": 0, + "slot_independent_obstructions": 4 + }, + { + "admissible": false, + "event": 3231, + "first_obstruction": [ + "Y56", + 3348, + "final frame excludes head" + ], + "forced": null, + "must_change": 10, + "partner": "D5", + "private_registers_forced": [], + "registers_without_prior_transport": 0, + "slot_independent_obstructions": 1 + }, + { + "admissible": true, + "event": 3364, + "first_obstruction": null, + "forced": { + "D17": 3364, + "D28": 3462, + "Y103": 3366, + "Y59": 3364 + }, + "must_change": 4, + "partner": "D17", + "private_registers_forced": [], + "registers_without_prior_transport": 0, + "slot_independent_obstructions": 0 + } + ] + }, + "head_cohosting": { + "R0_cohosted_target_updates": [ + 3364 + ], + "R0_last_target_update": 3364, + "R0_source_delivery_into_target": [ + [ + 3076, + "D10", + "1/2", + "1/2" + ], + [ + 3231, + "D5", + "-1/2", + "0" + ], + [ + 3364, + "D17", + "1/2", + "1/2" + ] + ], + "R0_source_events_after_update": [ + 3705, + 3760, + 3811, + 3863 + ], + "R0_source_frame_rank_at_update": 9, + "R0_source_spans_head_at_update": true, + "R0_update_chart": [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + "R0_update_chart_rank": 6, + "R0_update_partner": "D17", + "R1_cohosted_target_updates": [ + 3367 + ], + "R1_last_target_update": 3367, + "published_head_hosting_target_updates": [] + }, + "no_new_kappa": true, + "pinned_main": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "repairs": { + "R0": { + "class": "event-preserving retarget: same events in the same order, same ADD registers and coefficients, only transport frames and ranks and the matching ADD chart fields change", + "rule": "from the forced event on, each changed register's frame is its published frame plus the basis head, until a frame that already spans the head", + "splices": [ + { + "events": [ + [ + "transport", + "D17", + [ + 95, + 447, + 6, + 32 + ], + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + 2 + ] + ], + "published": [ + [ + "transport", + "D17", + [ + 95, + 447, + 6, + 32 + ], + [ + 95, + 447, + 6, + 32, + 20 + ], + 1 + ] + ], + "published_range": [ + 3362, + 3363 + ] + }, + { + "events": [ + [ + "transport", + "Y59", + [ + 95, + 447, + 32, + 20 + ], + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + 2 + ] + ], + "published": [ + [ + "transport", + "Y59", + [ + 95, + 447, + 32, + 20 + ], + [ + 95, + 447, + 6, + 32, + 20 + ], + 1 + ] + ], + "published_range": [ + 3363, + 3364 + ] + }, + { + "events": [ + [ + "add", + "Y59", + "D17", + "1/4", + [ + 95, + 447, + 6, + 32, + 20, + 15 + ] + ] + ], + "published": [ + [ + "add", + "Y59", + "D17", + "1/4", + [ + 95, + 447, + 6, + 32, + 20 + ] + ] + ], + "published_range": [ + 3364, + 3365 + ] + }, + { + "events": [ + [ + "transport", + "Y103", + [ + 95, + 447, + 32, + 20 + ], + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + 2 + ] + ], + "published": [ + [ + "transport", + "Y103", + [ + 95, + 447, + 32, + 20 + ], + [ + 95, + 447, + 6, + 32, + 20 + ], + 1 + ] + ], + "published_range": [ + 3365, + 3366 + ] + }, + { + "events": [ + [ + "add", + "Y103", + "D17", + "1/4", + [ + 95, + 447, + 6, + 32, + 20, + 15 + ] + ] + ], + "published": [ + [ + "add", + "Y103", + "D17", + "1/4", + [ + 95, + 447, + 6, + 32, + 20 + ] + ] + ], + "published_range": [ + 3366, + 3367 + ] + }, + { + "events": [ + [ + "transport", + "D28", + [ + 95, + 447, + 6, + 32, + 192 + ], + [ + 95, + 447, + 6, + 32, + 20, + 192, + 15 + ], + 2 + ] + ], + "published": [ + [ + "transport", + "D28", + [ + 95, + 447, + 6, + 32, + 192 + ], + [ + 95, + 447, + 6, + 32, + 20, + 192 + ], + 1 + ] + ], + "published_range": [ + 3460, + 3461 + ] + }, + { + "events": [ + [ + "transport", + "Y103", + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + [ + 95, + 447, + 6, + 32, + 20, + 192, + 15 + ], + 1 + ] + ], + "published": [ + [ + "transport", + "Y103", + [ + 95, + 447, + 6, + 32, + 20 + ], + [ + 95, + 447, + 6, + 32, + 20, + 192 + ], + 1 + ] + ], + "published_range": [ + 3461, + 3462 + ] + }, + { + "events": [ + [ + "add", + "Y103", + "D28", + "1/4", + [ + 95, + 447, + 6, + 32, + 20, + 192, + 15 + ] + ] + ], + "published": [ + [ + "add", + "Y103", + "D28", + "1/4", + [ + 95, + 447, + 6, + 32, + 20, + 192 + ] + ] + ], + "published_range": [ + 3462, + 3463 + ] + }, + { + "events": [ + [ + "transport", + "Y59", + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + [ + 499, + 27, + 228, + 32, + 112, + 15, + 7, + 1 + ], + 2 + ] + ], + "published": [ + [ + "transport", + "Y59", + [ + 95, + 447, + 6, + 32, + 20 + ], + [ + 499, + 27, + 228, + 32, + 112, + 15, + 7, + 1 + ], + 3 + ] + ], + "published_range": [ + 3525, + 3526 + ] + }, + { + "events": [ + [ + "transport", + "Y103", + [ + 95, + 447, + 6, + 32, + 20, + 192, + 15 + ], + [ + 351, + 80, + 44, + 27, + 3, + 12, + 224, + 6 + ], + 1 + ] + ], + "published": [ + [ + "transport", + "Y103", + [ + 95, + 447, + 6, + 32, + 20, + 192 + ], + [ + 351, + 80, + 44, + 27, + 3, + 12, + 224, + 6 + ], + 2 + ] + ], + "published_range": [ + 3569, + 3570 + ] + }, + { + "events": [ + [ + "transport", + "D17", + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 3 + ] + ], + "published": [ + [ + "transport", + "D17", + [ + 95, + 447, + 6, + 32, + 20 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 4 + ] + ], + "published_range": [ + 3612, + 3613 + ] + }, + { + "events": [ + [ + "transport", + "D28", + [ + 95, + 447, + 6, + 32, + 20, + 192, + 15 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 2 + ] + ], + "published": [ + [ + "transport", + "D28", + [ + 95, + 447, + 6, + 32, + 20, + 192 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 3 + ] + ], + "published_range": [ + 3634, + 3635 + ] + } + ] + }, + "R1": { + "class": "two-register comparison: Y103's transport and update at 3365-3366 move before Y59's, and D17 gets one added rank-1 transport", + "rule": "D17 serves Y103 in the published rank-5 chart, then lifts to the rank-6 head chart for Y59", + "splices": [ + { + "events": [ + [ + "transport", + "Y103", + [ + 95, + 447, + 32, + 20 + ], + [ + 95, + 447, + 6, + 32, + 20 + ], + 1 + ], + [ + "add", + "Y103", + "D17", + "1/4", + [ + 95, + 447, + 6, + 32, + 20 + ] + ], + [ + "transport", + "D17", + [ + 95, + 447, + 6, + 32, + 20 + ], + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + 1 + ], + [ + "transport", + "Y59", + [ + 95, + 447, + 32, + 20 + ], + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + 2 + ], + [ + "add", + "Y59", + "D17", + "1/4", + [ + 95, + 447, + 6, + 32, + 20, + 15 + ] + ] + ], + "published": [ + [ + "transport", + "Y59", + [ + 95, + 447, + 32, + 20 + ], + [ + 95, + 447, + 6, + 32, + 20 + ], + 1 + ], + [ + "add", + "Y59", + "D17", + "1/4", + [ + 95, + 447, + 6, + 32, + 20 + ] + ], + [ + "transport", + "Y103", + [ + 95, + 447, + 32, + 20 + ], + [ + 95, + 447, + 6, + 32, + 20 + ], + 1 + ], + [ + "add", + "Y103", + "D17", + "1/4", + [ + 95, + 447, + 6, + 32, + 20 + ] + ] + ], + "published_range": [ + 3363, + 3367 + ] + }, + { + "events": [ + [ + "transport", + "Y59", + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + [ + 499, + 27, + 228, + 32, + 112, + 15, + 7, + 1 + ], + 2 + ] + ], + "published": [ + [ + "transport", + "Y59", + [ + 95, + 447, + 6, + 32, + 20 + ], + [ + 499, + 27, + 228, + 32, + 112, + 15, + 7, + 1 + ], + 3 + ] + ], + "published_range": [ + 3525, + 3526 + ] + }, + { + "events": [ + [ + "transport", + "D17", + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 3 + ] + ], + "published": [ + [ + "transport", + "D17", + [ + 95, + 447, + 6, + 32, + 20 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 4 + ] + ], + "published_range": [ + 3612, + 3613 + ] + } + ] + } + }, + "schema_version": 1, + "selected_kappa": "0.001672660197076918", + "source_register": "X21", + "target_register": "Y59" +} diff --git a/research/p104-flag43-head-step-repair/NOTICE.md b/research/p104-flag43-head-step-repair/NOTICE.md new file mode 100644 index 0000000000..c9e8604aac --- /dev/null +++ b/research/p104-flag43-head-step-repair/NOTICE.md @@ -0,0 +1,12 @@ +# Notice + +This package applies two explicit schedule changes to the published P104 +native-channel witness in memory and checks them with the published native +checker and a second scanner. It does not modify frozen upstream sources. The +nine recipes in `REPAIR-RECIPES.json` were lowered with the pinned +`research/p104-native-channel/compile.py` and `vendor/clifford_exact.py` +(PR1991 lineage, Chafik Boukhalfa), whose notices are retained in that package. + +Prepared by Wentao Li with substantial AI assistance. +Apache-2.0; predecessor notices and exact source pins are retained in +`SOURCES.json`. diff --git a/research/p104-flag43-head-step-repair/PROOF.md b/research/p104-flag43-head-step-repair/PROOF.md new file mode 100644 index 0000000000..e15f68af79 --- /dev/null +++ b/research/p104-flag43-head-step-repair/PROOF.md @@ -0,0 +1,238 @@ +# Proof: flag-43 head-step repair, its bill, and the forced closure + +## Setup + +Pin CrocSwap main `6f100d4bb5083f8c35d96fd95a539811c62f245c`. Inputs: + +- The #2981 flag matching (`research/p104-joint-unit-flags/CERTIFICATE.json`). + Flag 43 has source 21, target 59 and basis `[15, 387, 6, 18, 32, 67, 128, 1, 2]`. +- 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: + +- Each register carries a binary frame `W` with canonical chart `Gamma_W`. +- A transport is nested, changes only `W`, and pays one positive child of rank + `|dim B - dim A|`. +- An ADD is allowed only when both registers have the same frame. It changes + only the destination's logical row. + +A register *hosts* `15` when `15` lies in the GF(2) span of its frame. + +Leave-alone priors are cited only. #3456 proves that on the published word none +of the 15 `Y59` updates runs in a chart that spans `15`, while every `X21` +annotation spans it. This package rechecks only the one-line consequence it +needs: no published `Y59` update hosts the head. + +## 1. The repair R0 + +Let: + +- `W4 = [95,447,6,32]` and `W4' = [95,447,32,20]`; +- `W5 = [95,447,6,32,20]` and `W6 = W5 + [15]`; +- `V5 = [95,447,6,32,192]`, `V6 = V5 + [20]` and `W7 = V6 + [15]`. + +R0 replaces exactly these published events (indices are unchanged): + +| Event | Published | R0 | +|---|---|---| +| 3362 | `D17: W4 -> W5`, rank 1 | `D17: W4 -> W6`, rank 2 | +| 3363 | `Y59: W4' -> W5`, rank 1 | `Y59: W4' -> W6`, rank 2 | +| 3364 | `Y59 += D17/4` in `W5` | same ADD in `W6` | +| 3365 | `Y103: W4' -> W5`, rank 1 | `Y103: W4' -> W6`, rank 2 | +| 3366 | `Y103 += D17/4` in `W5` | same ADD in `W6` | +| 3460 | `D28: V5 -> V6`, rank 1 | `D28: V5 -> W7`, rank 2 | +| 3461 | `Y103: W5 -> V6`, rank 1 | `Y103: W6 -> W7`, rank 1 | +| 3462 | `Y103 += D28/4` in `V6` | same ADD in `W7` | +| 3525 | `Y59: W5 -> final`, rank 3 | `Y59: W6 -> final`, rank 2 | +| 3569 | `Y103: V6 -> final`, rank 2 | `Y103: W7 -> final`, rank 1 | +| 3612 | `D17: W5 -> FULL`, rank 4 | `D17: W6 -> FULL`, rank 3 | +| 3634 | `D28: V6 -> FULL`, rank 3 | `D28: W7 -> FULL`, rank 2 | + +The final frames of `Y59` and `Y103` both contain `W6`. `Y103`'s also contains +`V6` and hence `W7`. So every changed transport is nested, and its rank equals its +frame gap. `D17` and `D28` have no other events between their changed transports. + +**Native validation.** `verify.py` builds the R0 word in memory. It assembles a +recipe set from two parts: the published recipes for every edge still in use, and +the committed `REPAIR-RECIPES.json` for every new edge. Eight published edges drop +out and eight new ones enter. Edge `W4' -> W6` is shared by events 3363 and 3365, +as `W4' -> W5` was. The script then calls the published `check_native.validate()` +unchanged. That function: + +- checks every edge's complete Clifford operator, including phase, against the + independent interpreter; +- binds every transport event to its recipe and rank; +- checks all 208 intrinsic endpoint adapters; +- runs the framed scalar induction over all 280 inputs. + +The induction requires every ADD to run in a common chart. It also requires each +source and each of the 72 dirty helper rows to end equal to its original input, +and each target row to end equal to `y_t + sum_s x_s / 2`, with every +final frame matched. R0 passes. `independent.py` separately replays the published +and repaired words with exact rational rows. It finds all 280 final rows equal to +the published ones. + +**Head co-hosting.** In R0, `Y59`'s updates are the published ones. The last, +3364, runs in `W6`, which lists `15`. At 3364, `X21`'s live frame is the +rank-9 full chart. It has later events 3705, 3760, 3811 and 3863, all of them +reads. The rational replay gives the `X21` entries of the rows `Y59` reads: + +| Event | Partner | `X21` carried | `Y59`'s `X21` coefficient after | +|---|---|---:|---:| +| 3076 | `D10` | `1/2` | `1/2` | +| 3231 | `D5` | `-1/2` | `0` | +| 3364 | `D17` | `1/2` | `1/2` | + +So the ADD that leaves `Y59` with its final `X21` coefficient runs in a chart +co-hosting the basis head, while the source hosts it and is still live. #3363's +relay census records the final coefficient. The event-level split is reported +here only because the co-hosting statement needs it. + +## 2. The bill + +Counts come from the validated words: + +- events, scalar ADDs and transport occurrences are unchanged: 4,058, 2,624 and + 1,410; +- rank mass is unchanged at 2,368; +- distinct native edges are unchanged at 740; +- endpoint adapters are unchanged at 208. + +The paid profile changes from `{1:1074, 2:58, 3:86, 4:104, ...}` to +`{1:1071, 2:63, 3:85, 4:103, ...}`. The ranks of 5 to 8 are unchanged. + +Per register, the profile changes are: + +- `Y59`: `-H1 - H3 + 2H2`; +- `D17`: `-H1 - H4 + H2 + H3`; +- `Y103`: no change, since `{1,1,2}` becomes `{2,1,1}`; +- `D28`: `-H1 - H3 + 2H2`. + +The total delta is `Delta = -3H1 + 5H2 - H3 - H4`. + +Sorted in decreasing order, the nine changed ranks go from `(4,3,3,2,1,1,1,1,1)` +to `(3,2,2,2,2,2,2,1,1)`. Both sum to 17, and the repaired prefix sums never +exceed the published ones. So the published vector majorizes the repaired one. +By Karamata's inequality, `Delta <= 0` for every convex rank price `H`. +Directly: convexity gives `2H2 <= H1 + H3` and `3H2 <= 2H1 + H4`, and these two +inequalities add up to `Delta <= 0`. `Delta = 0` for every affine `H(r) = a + br`. + +**R1.** R1 replaces published events 3363–3366 by: + +1. `Y103: W4' -> W5` +2. `Y103 += D17/4` in `W5` +3. `D17: W5 -> W6`, rank 1 (added) +4. `Y59: W4' -> W6`, rank 2 +5. `Y59 += D17/4` in `W6` + +It also sets 3525 to `Y59: W6 -> final` (rank 2) and 3612 to +`D17: W6 -> FULL` (rank 3). The two reads of `D17` into distinct targets commute, +and nothing between them touches `D17`, `Y59` or `Y103`. R1 passes the same native +validation. Its bill: + +- +1 event and +1 transport occurrence; +- rank mass and ADDs unchanged; +- profile delta `+2H2 - H4`; +- 742 distinct edges. + +R1 avoids the `Y103`/`D28` cascade by giving up event preservation. + +## 3. Forced closure + +**Class Z.** A repair is in class Z when: + +1. it keeps the published events in their published order, with the same ADD + registers and coefficients, and may insert transports; +2. it keeps every initial and final frame; +3. it adds no rank mass. + +`verify.py` checks that every one of the 280 non-private registers has published +rank mass equal to `rank(final) - rank(initial)`. A register's rank mass is at +least that floor, and equals it only for a monotone path. So by condition 3 every +non-private register's path in a class-Z repair is monotone. The private register +`C` is reported separately and never counted as an obstruction. + +**Propagation lemma.** Suppose that in a class-Z repair a non-private register +`r` hosts `15` at event `t`. Then it hosts `15` at every later event, by +monotonicity. Any ADD or copy at `j >= t` that involves `r` forces its partner to +host `15` at `j`, because the two frames are equal. + +Starting from a `Y59` update `u`, take the closure of this rule. A register is +*must-change* when its published frame at its forced time does not span `15`. + +- If a must-change register's final frame excludes `15`, no monotone path can + host `15` there, so no class-Z repair makes `u` head-hosting. +- If the closure is unobstructed, the published frames already satisfy every + other forced condition, because published paths are monotone. + +`verify.py` computes the closure with a worklist and `independent.py` with a +single forward sweep. For the 15 `Y59` updates: + +| Update | Partner | Must-change | Obstructions | First obstruction | +|---:|---|---:|---:|---| +| 223–227 | `Q1, Q2, Q4, Q5, Q6` | 260–274 | 56 each | `Y67` (264–268) | +| 2099, 2191 | `D23, D20` | 140 | 56 | `Y96` | +| 2275 | `D10` | 140 | 56 | `Y26` at 2336 | +| 2341 | `D5` | 140 | 56 | `Y56` at 2387 | +| 2393 | `D17` | 133 | 53 | `Y22` at 2638 | +| 2698 | `D23` | 45 | 17 | `Y96` at 2706 | +| 2891 | `D20` | 31 | 12 | `Y96` at 2897 | +| 3076 | `D10` | 17 | 4 | `Y26` at 3220 | +| 3231 | `D5` | 10 | 1 | `Y56` at 3348 | +| 3364 | `D17` | 4 | 0 | none | + +The exact per-update values are in `CERTIFICATE.json`. So 3364 is the only update +that any class-Z repair can make head-hosting. Its must-change set is exactly: + +- `Y59` and `D17` from 3364; +- `Y103` from 3366; +- `D28` from 3462. + +**Minimality in the event-preserving subclass.** With no inserted events, each +must-change register `r` with forced time `t` behaves as follows: + +- its last transport before `t` must gain `15` in its after-frame, since no + published after-frame there spans `15`; +- each later transport of `r` then has a changed before-frame. + +Together these are exactly R0's nine transports: 2 for `Y59`, 2 for `D17`, 3 for +`Y103` and 2 for `D28`. At each forced ADD the shared frame must contain both +published frames and `15`. That gives `span(W5 + 15) = W6` at 3364 and 3366, and +`span(V6 + 15) = W7` at 3462. R0 uses exactly these minimal frames. + +## Controls + +`test_package.py` copies the package and the six pinned inputs into a temporary +tree and runs both scanners there under `-O`. The clean tree must pass and stay +byte-identical. Fourteen mutations must be rejected by both scanners: + +- seven certificate fields; +- a duplicate JSON key; +- a witness byte flip; +- a phase flip in a new recipe; +- an undercharged 3525 transport; +- three truncated cascades: `Y59` lifted alone, without `Y103`/`D28`, and without + `D28`. + +Each truncated cascade must fail at the common-chart rule. + +## Limits + +This is a statement about one finite repaired word for one flag: + +- It does not build or price the `I - G/2` side correction or a supplier. +- It does not perform global hosting or precision analysis. +- It does not change κ. + +"Co-hosting" means span membership in annotated frames. It does not model what the +head direction means inside relay registers. `H_r` is left symbolic. The repo's +actual per-rank weights decide the sign of `Delta` only if they are strictly +concave somewhere on `{1,2,3,4}`. The class-Z obstruction excludes repairs that: + +- reorder events (R1 is one such repair); +- add rank mass; +- change ADDs, coefficients or endpoint frames. + +Optimality of R0's profile among class-Z repairs is not claimed. diff --git a/research/p104-flag43-head-step-repair/README.md b/research/p104-flag43-head-step-repair/README.md new file mode 100644 index 0000000000..37f19da438 --- /dev/null +++ b/research/p104-flag43-head-step-repair/README.md @@ -0,0 +1,123 @@ +# Flag 43's basis head can be co-hosted at its delivering target update at zero added channel cost + +**Finite repaired word with an exact bill, plus a forced-closure obstruction. No new exponent.** + +Open [#3456](https://github.com/CrocSwap/integer-mult-bounds/pull/3456) shows that +on the published 4,058-event P104 word, present-head flag 43 (`X21` → `Y59`, +basis head `15`) never updates `Y59` while both endpoints host the head. Its first +open question asks what a changed schedule that fixes this would cost. The +matching questions in [#3451](https://github.com/CrocSwap/integer-mult-bounds/pull/3451) +(flag 1) and [#3443](https://github.com/CrocSwap/integer-mult-bounds/pull/3443) +(flag 9) are open for the same reason. This package answers it for flag 43 and +cites those chronologies without re-deriving them. + +## Result + +**Repair R0** keeps every published event in its published order, with the same +ADD registers and coefficients. It changes only the frames of nine existing +transports and the chart fields of three ADDs. From the forced event on, each +changed register's frame is its published frame plus `15`: + +| Register | Retargeted transports | Published ranks | Repaired ranks | +|---|---|---|---| +| `Y59` | 3363, 3525 | 1, 3 | 2, 2 | +| `D17` | 3362, 3612 | 1, 4 | 2, 3 | +| `Y103` | 3365, 3461, 3569 | 1, 1, 2 | 2, 1, 1 | +| `D28` | 3460, 3634 | 1, 3 | 2, 2 | + +The published native checker `check_native.validate()` passes unchanged on the +repaired word. That covers every native edge (eight swapped for eight newly +lowered edges, still 740), all 208 endpoint adapters, and all 280 framed rows, +including the restoration of the 72 dirty helpers. + +In R0, `Y59`'s last update (event 3364, `Y59 += D17/4`) runs in the rank-6 chart +`[95, 447, 6, 32, 20, 15]`. At that moment `X21` is in the rank-9 full chart and +has four later reads. That ADD carries `X21` coefficient `1/2` and settles +`Y59`'s final `X21` coefficient. The earlier `+1/2` at 3076 is cancelled at +3231. So the update that delivers the matched source now runs in a chart that +co-hosts the basis head. + +| Bill term | Published | R0 | R1 (comparison) | +|---|---:|---:|---:| +| Events | 4,058 | 4,058 | 4,059 | +| Scalar ADDs | 2,624 | 2,624 | 2,624 | +| Transport occurrences | 1,410 | 1,410 | 1,411 | +| Rank mass | 2,368 | 2,368 | 2,368 | +| Distinct native edges | 740 | 740 | 742 | +| Paid profile delta | — | `-3H1 + 5H2 - H3 - H4` | `+2H2 - H4` | + +R0 adds nothing to any counted bill term. Its only change is the rank profile: +the nine changed ranks `{4,3,3,2,1,1,1,1,1}` become `{3,2,2,2,2,2,2,1,1}`. The +published multiset majorizes the repaired one, so for every convex per-rank price +`H` the delta `5H2 - 3H1 - H3 - H4` is at most zero. It is exactly zero for every +affine price, and positive only for a strictly concave one. + +**Comparison R1** touches only `Y59` and `D17`. It moves `Y103`'s transport and +update (3365–3366) ahead of `Y59`'s and gives `D17` one added rank-1 lift. This +costs one event and one transport occurrence, with rank mass unchanged. R1 is +also natively validated. + +## Obstruction + +Consider the class of repairs that: + +- keep the published event order and ADDs, +- keep the endpoint frames, +- add no rank mass. + +All 280 non-private registers already sit at their rank floor, so in this class +every such path stays monotone. Inserting refinement transports is allowed. Within +this class, only event 3364 among `Y59`'s 15 updates can be made head-hosting. + +- Each of the other 14 forces the head into a register whose final frame excludes + it. The first such register is `Y67`, `Y96`, `Y26`, `Y56` or `Y22`, depending + on the update. At 3231 the single obstruction is `Y56` at event 3348. +- At 3364 the forced must-change set is exactly `Y59` and `D17` (from 3364), + `Y103` (from 3366) and `D28` (from 3462). + +If no events are inserted, all nine transports R0 retargets are forced to change. +R0 therefore uses the minimum number of changed transports and registers in that +class. + +Selected κ stays `0.001672660197076918`. Proof details and limits are in +[PROOF.md](PROOF.md). + +## Reproduce + +```sh +python3.12 -I -B research/p104-flag43-head-step-repair/verify.py +python3.12 -I -O -Werror -B research/p104-flag43-head-step-repair/verify.py +python3.12 -I -O -Werror -B research/p104-flag43-head-step-repair/independent.py +python3.12 -I -O -Werror -B research/p104-flag43-head-step-repair/test_package.py +python3.12 -B scripts/research_package.py --package research/p104-flag43-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 every corruption. It also checks that three truncated +cascades (target only; without `Y103`; without `D28`) fail at the common-chart +rule. `build.py` is the producer and is not part of the replay. + +## Credit + +Credit #3456 for flag 43's published chronology and the `D17` common-chart first +step, which this package follows. Credit #3451 and #3443 for the flag-1 and +flag-9 present-head obstructions, and #3349 for the present-head census. Credit +Nick Petalas / #2981 for the flag matching, the reviewed #1991 native channel +(Chafik Boukhalfa) for the witness, checker and compiler, and #3363 for the relay +census whose coefficient convention is reused. Prepared by Wentao Li with +substantial AI assistance. + +## Open next questions + +1. Do flags 1 and 9 admit the same event-preserving head-step repair, or is their + forced closure obstructed? Answer this in a separate package that cites #3451 + and #3443. +2. Can a side correction use R0's co-hosted head chart at 3364 to restore + `X21`'s contribution to `Y59` dirtily, and what does the `I - G/2` correction + cost at that cut? +3. Is R0's profile majorization-minimal among event-preserving monotone repairs? + +[TASK.json](TASK.json) gives first steps and blockers. diff --git a/research/p104-flag43-head-step-repair/REPAIR-RECIPES.json b/research/p104-flag43-head-step-repair/REPAIR-RECIPES.json new file mode 100644 index 0000000000..c697547694 --- /dev/null +++ b/research/p104-flag43-head-step-repair/REPAIR-RECIPES.json @@ -0,0 +1,880 @@ +{ + "clifford_exact_sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "compiler_sha256": "9d2fc2d81962ddb0b4dd7d6482d9918a87a6b05759690317dea79939ca5656a3", + "recipes": [ + { + "new": [ + 256, + 128, + 65, + 40, + 25, + 5, + 3 + ], + "old": [ + 256, + 128, + 40, + 25, + 5 + ], + "rank": 2, + "recipe": { + "left": { + "linear_Z4": [ + 3, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 6, + 3, + 8, + 16, + 32, + 64, + 1, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 3, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 2, + "right": { + "linear_Z4": [ + 1, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 66, + 65, + 67, + 4, + 8, + 16, + 32, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 3, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + } + }, + { + "new": [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + "old": [ + 256, + 128, + 65, + 40, + 25, + 5, + 3 + ], + "rank": 2, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 5, + 9, + 17, + 34, + 67, + 2, + 1, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 2, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 2, + "right": { + "linear_Z4": [ + 0, + 0, + 0, + 2, + 0, + 1, + 3, + 0, + 0 + ], + "matrix_rows": [ + 97, + 104, + 64, + 66, + 68, + 32, + 112, + 128, + 256 + ], + "offset": 101, + "phase": 2, + "quadratic_rows": [ + 32, + 0, + 0, + 64, + 0, + 97, + 104, + 0, + 0 + ] + } + } + }, + { + "new": [ + 256, + 128, + 65, + 32, + 17, + 8, + 5, + 3 + ], + "old": [ + 256, + 128, + 65, + 40, + 25, + 5, + 3 + ], + "rank": 1, + "recipe": { + "left": { + "linear_Z4": [ + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 3, + 4, + 8, + 17, + 33, + 1, + 64, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 1, + "right": { + "linear_Z4": [ + 3, + 0, + 0, + 2, + 0, + 2, + 0, + 0, + 0 + ], + "matrix_rows": [ + 9, + 33, + 2, + 4, + 32, + 48, + 64, + 128, + 256 + ], + "offset": 50, + "phase": 1, + "quadratic_rows": [ + 41, + 0, + 0, + 33, + 0, + 9, + 0, + 0, + 0 + ] + } + } + }, + { + "new": [ + 256, + 133, + 68, + 40, + 25, + 3 + ], + "old": [ + 256, + 133, + 40, + 25 + ], + "rank": 2, + "recipe": { + "left": { + "linear_Z4": [ + 3, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 5, + 1, + 10, + 16, + 32, + 64, + 2, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 1, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 2, + "right": { + "linear_Z4": [ + 1, + 2, + 1, + 0, + 0, + 0, + 2, + 0, + 0 + ], + "matrix_rows": [ + 1, + 4, + 3, + 68, + 8, + 16, + 32, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 3, + 1, + 68, + 0, + 0, + 0, + 4, + 0, + 0 + ] + } + } + }, + { + "new": [ + 256, + 133, + 68, + 40, + 25, + 3 + ], + "old": [ + 256, + 133, + 68, + 40, + 25 + ], + "rank": 1, + "recipe": { + "left": { + "linear_Z4": [ + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 3, + 1, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 1, + "right": { + "linear_Z4": [ + 1, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 1, + 3, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 3, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + } + }, + { + "new": [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + "old": [ + 256, + 133, + 68, + 40, + 25, + 3 + ], + "rank": 3, + "recipe": { + "left": { + "linear_Z4": [ + 3, + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 9, + 17, + 34, + 68, + 133, + 4, + 2, + 3, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 7, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 3, + "right": { + "linear_Z4": [ + 0, + 0, + 0, + 0, + 0, + 3, + 3, + 0, + 0 + ], + "matrix_rows": [ + 97, + 132, + 232, + 192, + 194, + 64, + 32, + 240, + 256 + ], + "offset": 118, + "phase": 3, + "quadratic_rows": [ + 160, + 0, + 192, + 192, + 0, + 97, + 108, + 13, + 0 + ] + } + } + }, + { + "new": [ + 256, + 128, + 65, + 40, + 25, + 5, + 3 + ], + "old": [ + 256, + 133, + 68, + 40, + 25, + 3 + ], + "rank": 1, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 2, + 4, + 9, + 16, + 32, + 64, + 129, + 1, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 1, + "right": { + "linear_Z4": [ + 2, + 0, + 3, + 0, + 0, + 0, + 0, + 2, + 0 + ], + "matrix_rows": [ + 132, + 5, + 2, + 128, + 8, + 16, + 32, + 192, + 256 + ], + "offset": 131, + "phase": 3, + "quadratic_rows": [ + 4, + 0, + 5, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + } + }, + { + "new": [ + 256, + 132, + 68, + 32, + 16, + 8, + 2, + 1 + ], + "old": [ + 256, + 133, + 68, + 40, + 25, + 3 + ], + "rank": 2, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 5, + 9, + 17, + 34, + 67, + 2, + 128, + 1, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 2, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 2, + "right": { + "linear_Z4": [ + 0, + 0, + 1, + 0, + 0, + 3, + 0, + 1, + 0 + ], + "matrix_rows": [ + 165, + 168, + 128, + 130, + 132, + 32, + 176, + 64, + 256 + ], + "offset": 42, + "phase": 3, + "quadratic_rows": [ + 36, + 0, + 37, + 128, + 0, + 165, + 0, + 168, + 0 + ] + } + } + }, + { + "new": [ + 256, + 133, + 68, + 40, + 25, + 3 + ], + "old": [ + 256, + 133, + 93, + 40 + ], + "rank": 2, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 6, + 3, + 9, + 17, + 33, + 64, + 1, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 2, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 2, + "right": { + "linear_Z4": [ + 1, + 3, + 1, + 1, + 0, + 0, + 2, + 0, + 0 + ], + "matrix_rows": [ + 14, + 81, + 83, + 68, + 88, + 64, + 32, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 3, + 95, + 78, + 94, + 10, + 0, + 14, + 0, + 0 + ] + } + } + } + ], + "schema_version": 1, + "scope": "Native recipes for the transport edges used by 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-flag43-head-step-repair/SOURCES.json b/research/p104-flag43-head-step-repair/SOURCES.json new file mode 100644 index 0000000000..4389ff657e --- /dev/null +++ b/research/p104-flag43-head-step-repair/SOURCES.json @@ -0,0 +1,81 @@ +{ + "schema_version": 1, + "base_commit": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "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 43 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-flag43-head-step-repair/TASK.json b/research/p104-flag43-head-step-repair/TASK.json new file mode 100644 index 0000000000..2d6f96085b --- /dev/null +++ b/research/p104-flag43-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": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "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": "Price a changed schedule that co-hosts present-head flag 43's basis head (15) in the target Y59 at a target update while the source X21 still hosts it and is still live, answering open question 1 of #3456 (and the matching question of #3451/#3443 for this flag). Construct the repair as an explicit splice of the published #1991 word, run the published p104-native-channel validate() on the repaired word with eight newly lowered native edges, and give the exact before/after bill (events, ADDs, transport occurrences, rank mass, paid H_r profile, native edges). Add the matching obstruction: in the class that keeps the published event order and ADDs, keeps endpoint frames and adds no rank mass, event 3364 is the only Y59 update that can be made head-hosting, and it forces exactly Y59, D17, Y103 and D28 to change.", + "scope_change_reason": "#3451, #3456 and #3443 prove the published word never co-hosts the basis head at a target update on flags 1, 43 and 9, and leave pricing a repair open. This package does not re-derive those chronologies; it cites them and adds the repair, its native validation, its bill and a forced-closure obstruction for flag 43. Flag 43 was chosen because #3456 records that its last target chart is one rank step from the head and names the D17 common-chart constraint.", + "bottleneck_link": "The present-head obstruction on flag 43 is a scheduling artefact, not a cost barrier: the head can be co-hosted at the target update that settles X21's final coefficient without adding any event, ADD, transport or rank unit to the published channel. The remaining cost is a rank-profile reshuffle that is free under any affine per-rank price and weakly favourable under any convex one. This does not supply I-G/2, a side correction or a supplier.", + "budget_minutes": 60, + "stop_rule": "Stop after one flag (43): one event-preserving repair R0 and one order-changing comparison R1, both natively validated and billed, plus the forced-hosting closure of every Y59 update. Do not touch flags 0, 1 or 9, recompute relay coefficients beyond the X21 entries of Y59, or build a side correction.", + "outcome": "completed", + "evidence": "R0 retargets nine published transports (3362, 3363, 3365, 3460, 3461, 3525, 3569, 3612, 3634) and relabels three ADD charts (3364, 3366, 3462); every changed frame is its published frame plus 15. The published check_native.validate() passes on the repaired word: 740 native edges (8 swapped for 8 newly lowered), 208 endpoint adapters, all 280 framed rows and 72 dirty helpers restored. Bill: 4058 events, 2624 ADDs, 1410 transport occurrences and rank mass 2368, all unchanged; paid profile {1:1074,2:58,3:86,4:104} becomes {1:1071,2:63,3:85,4:103}, delta -3H1+5H2-H3-H4; the nine changed ranks {4,3,3,2,1,1,1,1,1} become {3,2,2,2,2,2,2,1,1}, which the published multiset majorizes. In R0 the last Y59 update (3364, D17, coefficient 1/4) runs in chart [95,447,6,32,20,15] while X21 is at the rank-9 full chart with four later reads; that ADD carries X21 coefficient 1/2 and settles Y59's final X21 coefficient 1/2 (after +1/2 at 3076 and -1/2 at 3231). R1 instead moves Y103's 3365-3366 before Y59's update and gives D17 one added rank-1 transport: +1 event, +1 transport occurrence, rank mass unchanged, delta +2H2-H4, 742 native edges. Forced closure on the published word: 14 of 15 Y59 updates force the head into a register whose final frame excludes it (first: Y67, Y96, Y26, Y56 or Y22); only 3364 is admissible, forcing D17 at 3364, Y103 at 3366 and D28 at 3462. All 280 non-private registers sit at their rank floor, so zero added rank mass means monotone paths. Selected kappa unchanged.", + "author": "Wentao Li", + "ai_assistance": "Substantial AI assistance for derivation, implementation, checking and writing.", + "no_new_kappa": true, + "open_questions": [ + { + "question": "Does the same head-step repair exist for present-head flags 1 and 9, and what is the forced closure of their target updates?", + "why_it_matters": "If every present-head flag admits an event-preserving repair, the present-head obstruction recorded by #3451/#3443/#3456 is uniformly a scheduling artefact; a flag whose closure is obstructed would instead need added rank or a reordering, with a priced floor.", + "first_step": "Run this package's closure_table on Y7 (flag 1, head 232) and Y23 (flag 9, head 196) as a separate package citing #3451 and #3443, without re-certifying their chronologies.", + "blocked_by": "This package treats flag 43 only. Flags 1 and 9 are the subjects of open #3451 and #3443." + }, + { + "question": "Can a correction program use the co-hosted head chart at 3364 to restore X21's contribution to Y59 dirtily, and what does the I-G/2 side correction then cost at that cut?", + "why_it_matters": "R0 removes the geometric reason given by #3456 for why chronological dirty restoration cannot use co-hosted head geometry on flag 43. Whether the side correction can exploit it is the actual supplier question.", + "first_step": "At R0's event 3364, price one added X21-to-Y59 transfer in the common head chart (both registers would need a shared frame; X21 is at the full chart) against the channel's existing allowance.", + "blocked_by": "No side-correction word is built here; the channel still implements G/2, not I." + }, + { + "question": "Is R0's rank profile optimal among event-preserving monotone repairs under every convex per-rank price?", + "why_it_matters": "R0 uses the minimal admissible frame at each forced event, but a different choice of intermediate frames could give a profile that the R0 profile does not majorize.", + "first_step": "Enumerate the admissible frames for the nine forced transports inside each register's final span and compare the resulting rank multisets by majorization.", + "blocked_by": "Not enumerated in this package." + } + ] +} diff --git a/research/p104-flag43-head-step-repair/VERIFY.json b/research/p104-flag43-head-step-repair/VERIFY.json new file mode 100644 index 0000000000..f0e005040e --- /dev/null +++ b/research/p104-flag43-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 to the published witness in memory, runs the published check_native.validate() on each (every native edge incl. 9 committed new-edge recipes, 208 endpoint adapters, all 280 framed rows and dirty-helper restorations), recomputes the bill, head co-hosting, X21 delivery into Y59 and the forced-hosting closure of all 15 Y59 updates, and requires equality with CERTIFICATE.json" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Separately written replay with XOR-closure frames and exact rational rows: common-chart ADDs, nested transports with paid rank equal to frame gap, 280/280 final rows equal to the published rows, bill and profile delta, majorization, head co-hosting and delivery, forward-sweep forced closure, direct native check of each new recipe" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 600, + "checks": "Temp-tree clean pass with byte-identical tree; 14 rejections by both scanners under -O: certificate field corruptions, duplicate JSON key, witness byte flip, new-recipe phase corruption, three truncated cascades rejected at the common-chart rule, and an undercharged transport" + } + ] +} diff --git a/research/p104-flag43-head-step-repair/build.py b/research/p104-flag43-head-step-repair/build.py new file mode 100644 index 0000000000..bad14e78ab --- /dev/null +++ b/research/p104-flag43-head-step-repair/build.py @@ -0,0 +1,125 @@ +#!/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" + +W4 = [95, 447, 6, 32] +W4P = [95, 447, 32, 20] +W5 = [95, 447, 6, 32, 20] +W6 = W5 + [15] +V5 = [95, 447, 6, 32, 192] +V6 = [95, 447, 6, 32, 20, 192] +W7 = V6 + [15] +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(3362, ["transport", "D17", W4, W6, 2]), + one(3363, ["transport", "Y59", W4P, W6, 2]), + one(3364, ["add", "Y59", "D17", "1/4", W6]), + one(3365, ["transport", "Y103", W4P, W6, 2]), + one(3366, ["add", "Y103", "D17", "1/4", W6]), + one(3460, ["transport", "D28", V5, W7, 2]), + one(3461, ["transport", "Y103", W6, W7, 1]), + one(3462, ["add", "Y103", "D28", "1/4", W7]), + one(3525, ["transport", "Y59", W6, final["Y59"], 2]), + one(3569, ["transport", "Y103", W7, final["Y103"], 1]), + one(3612, ["transport", "D17", W6, FULL, 3]), + one(3634, ["transport", "D28", W7, FULL, 2]), + ] + r1 = [ + {"published_range": [3363, 3367], "published": program[3363:3367], + "events": [program[3365], program[3366], + ["transport", "D17", W5, W6, 1], + ["transport", "Y59", W4P, W6, 2], + ["add", "Y59", "D17", "1/4", W6]]}, + one(3525, ["transport", "Y59", W6, final["Y59"], 2]), + one(3612, ["transport", "D17", W6, FULL, 3]), + ] + return { + "R0": { + "class": "event-preserving retarget: same events in the same order, same ADD registers and coefficients, only transport frames and ranks and the matching ADD chart fields change", + "rule": "from the forced event on, each changed register's frame is its published frame plus the basis head, until a frame that already spans the head", + "splices": r0, + }, + "R1": { + "class": "two-register comparison: Y103's transport and update at 3365-3366 move before Y59's, and D17 gets one added rank-1 transport", + "rule": "D17 serves Y103 in the published rank-5 chart, then lifts to the rank-6 head chart for Y59", + "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("flag43_clifford_pin", root / V.NATIVE / "vendor/clifford_exact.py", CLIFFORD_SHA256) + co = load("flag43_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 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-flag43-head-step-repair/independent.py b/research/p104-flag43-head-step-repair/independent.py new file mode 100644 index 0000000000..75d219fcfd --- /dev/null +++ b/research/p104-flag43-head-step-repair/independent.py @@ -0,0 +1,305 @@ +#!/usr/bin/env python3 +"""Second, separately written scanner for the flag-43 head-step repair bill. + +Does not import verify.py, check_native.py or the compiler. Frames are explicit +XOR-closure sets; the repaired words are replayed with exact rational rows and +compared register by register with the published word's final rows and frames. +The forced-hosting closure is recomputed by a single forward sweep. The new +native recipes are checked directly with the vendored independent interpreter. +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", +} +MARKER = ( + "PASS_P104_FLAG43_HEAD_STEP_REPAIR_INDEPENDENT flag=43 head=15 repaired_update=3364 " + "added_events=0 added_adds=0 added_transports=0 added_rank_mass=0 " + "retargeted_transports=9 forced_registers=4 profile_delta=-3H1+5H2-H3-H4 " + "rows_equal=280/280 earlier_updates_obstructed=14/14 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 & (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) + need(len(new) == dim(b) and len(old) == dim(a), "independent frame lists 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) + seqs = {} + change = {} + for r, t in hosting.items(): + if r == "C": + frames = [f for i, f in private_frames(program) if i < t] + if not frames or head not in frames[-1]: + change[r] = t + 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 private_frames(program): + out = [] + for i, e in enumerate(program): + if e[1:2] == ["C"]: + if e[0] == "zero": + out.append((i, closure(e[2]))) + elif e[0] == "transport": + out.append((i, closure(e[3]))) + return out + + +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("flag43_independent_native", root / NATIVE / "vendor/native_verify.py") + N = importlib.util.module_from_spec(spec) + spec.loader.exec_module(N) + + h = flags["helpers"][43] + head, src, tgt = h["basis"][0], "X%d" % h["source"], "Y%d" % h["target"] + need((head, src, tgt) == (15, "X21", "Y59"), "flag 43") + need(cert["basis_head"] == head and cert["source_register"] == src and cert["target_register"] == tgt, "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") + + # Physical canonical images of the repaired frames, for the native recipe check. + 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 + + 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") + out[name] = (prog, b) + need(used == set(new_edges), "every committed recipe used") + + prog0, b0 = out["R0"] + need((b0["added_events"], b0["added_scalar_adds"], b0["added_transport_occurrences"], b0["added_rank_mass"]) == (0, 0, 0, 0), "R0 adds nothing counted") + need(b0["profile_delta"] == {"1": -3, "2": 5, "3": -1, "4": -1}, "R0 delta") + moved = [i for i in range(len(P)) if P[i] != prog0[i] and P[i][0] == "transport"] + need(moved == b0["retargeted_transports"] and len(moved) == 9, "nine retargeted transports") + old_r = sorted((P[i][4] for i in moved), reverse=True) + new_r = sorted((prog0[i][4] for i in moved), reverse=True) + need(sum(old_r) == sum(new_r) and all(sum(new_r[:k]) <= sum(old_r[:k]) for k in range(1, 10)), "majorization") + need(sorted({P[i][1] for i in moved}) == b0["registers_changed"] == ["D17", "D28", "Y103", "Y59"], "changed registers") + need((b["added_events"], b["added_transport_occurrences"], b["added_rank_mass"]) == (1, 1, 0) and b["profile_delta"] == {"2": 2, "4": -1}, "R1 bill") + + hc = cert["head_cohosting"] + tseq, sseq = frames_over_time(witness, prog0, tgt), frames_over_time(witness, prog0, src) + pseq = frames_over_time(witness, P, tgt) + upd = [i for i, e in enumerate(prog0) if e[0] == "add" and e[1] == tgt] + need([i for i in upd if head in frame_before(pseq, i)] == hc["published_head_hosting_target_updates"] == [], "published head-free updates") + co = [i for i in upd if head in frame_before(tseq, i) and head in frame_before(sseq, i)] + need(co == hc["R0_cohosted_target_updates"] == [3364] and upd[-1] == 3364, "R0 co-hosted last update") + need(closure(prog0[3364][4]) == closure([95, 447, 6, 32, 20, 15]) and prog0[3364][2] == "D17", "R0 update chart") + need(dim(frame_before(sseq, 3364)) == 9 and [i for i, e in enumerate(prog0) if i > 3364 and src in e[1:3]] == [3705, 3760, 3811, 3863], "source live and full") + coef = Fraction(0) + carried = [] + rows = {n: {n: Fraction(1)} for n in witness["initial_frames"]} + for i, e in enumerate(prog0): + 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] == tgt and rows[e[2]].get(src): + coef += Fraction(e[3]) * rows[e[2]][src] + carried.append([i, e[2], str(Fraction(e[3]) * rows[e[2]][src]), 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) + need(carried == hc["R0_source_delivery_into_target"] and carried[-1] == [3364, "D17", "1/2", "1/2"], "delivery chronology") + + 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] == tgt], "every target update tabulated") + obstructed = 0 + for t0, row in table.items(): + change, seqs = sweep(witness, P, tgt, t0, head) + hard = sorted([[r, t] for r, t in change.items() if r != "C" and r in finals and head not in finals[r]], key=lambda x: (x[1], x[0])) + private = sorted([[r, t] for r, t in change.items() if r == "C"], key=lambda x: (x[1], x[0])) + slot = [r for r, t in change.items() if r != "C" and not any(-1 < i < t for i, _ in seqs[r]) and [r, t] not in hard and head not in seqs[r][0][1]] + need(row["must_change"] == len(change), "must-change count at %d" % t0) + 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["private_registers_forced"] == private, "private forcing at %d" % t0) + need(row["registers_without_prior_transport"] == len(slot), "slot count at %d" % t0) + need(row["admissible"] == (not hard and not slot and not private), "admissible at %d" % t0) + if hard: + obstructed += 1 + else: + need(row["forced"] == change, "forced set at %d" % t0) + need(obstructed == 14 and table[3364]["forced"] == {"Y59": 3364, "D17": 3364, "Y103": 3366, "D28": 3462}, "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-flag43-head-step-repair/test_package.py b/research/p104-flag43-head-step-repair/test_package.py new file mode 100644 index 0000000000..935e39776c --- /dev/null +++ b/research/p104-flag43-head-step-repair/test_package.py @@ -0,0 +1,155 @@ +#!/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=600) + 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 drop_splices(events): + def fn(c): + rows = c["repairs"]["R0"]["splices"] + c["repairs"]["R0"]["splices"] = [r for r in rows if r["published_range"][0] not in events] + return fn + + +def set_rank(event, value): + def fn(c): + for r in c["repairs"]["R0"]["splices"]: + if r["published_range"][0] == event: + r["events"][0][4] = value + return fn + + +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": 15,', '"basis_head": 15,\n "basis_head": 15,', 1)) + + +def flip_witness(base): + p = base / f"{NATIVE}/inputs/LOWRANK-WITNESS.json" + raw = bytearray(p.read_bytes()) + k = raw.index(b"3525") if b"3525" in raw else len(raw) // 2 + raw[k] ^= 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") + + +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", 4)), None), + "cohosted_updates": (cert_field(lambda c: c["head_cohosting"].__setitem__("R0_cohosted_target_updates", [])), None), + "delivery": (cert_field(lambda c: c["head_cohosting"]["R0_source_delivery_into_target"][-1].__setitem__(2, "1/4")), None), + "admissible_3231": (cert_field(lambda c: [r.__setitem__("admissible", True) for r in c["forced_hosting"]["table"] if r["event"] == 3231]), None), + "forced_set": (cert_field(lambda c: [r["forced"].pop("D28") for r in c["forced_hosting"]["table"] if r["event"] == 3364]), None), + "kappa": (cert_field(lambda c: c.__setitem__("selected_kappa", "0.0016726601970769181")), None), + "duplicate_key": (dup_key, "duplicate JSON key"), + "witness_byte": (flip_witness, None), + "recipe_phase": (bad_phase, None), + "control_target_only": (cert_field(drop_splices({3362, 3612, 3365, 3366, 3460, 3461, 3462, 3569, 3634})), "common"), + "control_without_y103": (cert_field(drop_splices({3365, 3366, 3460, 3461, 3462, 3569, 3634})), "common"), + "control_without_d28": (cert_field(drop_splices({3460, 3462, 3634})), "common"), + "control_undercharge": (cert_field(set_rank(3525, 1)), None), +} + + +def case(name): + mutate, expect = CASES[name] + with tempfile.TemporaryDirectory(prefix="flag43-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[-300:]}") + return name + + +def clean(): + with tempfile.TemporaryDirectory(prefix="flag43-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_FLAG43_HEAD_STEP_REPAIR" in out, f"clean {scanner}: {out[-400:]}") + 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_FLAG43_HEAD_STEP_REPAIR_TESTS cases={len(CASES)} clean_read_only=1 scanners=2") + + +if __name__ == "__main__": + main() diff --git a/research/p104-flag43-head-step-repair/verify.py b/research/p104-flag43-head-step-repair/verify.py new file mode 100644 index 0000000000..a1cd9408bb --- /dev/null +++ b/research/p104-flag43-head-step-repair/verify.py @@ -0,0 +1,458 @@ +#!/usr/bin/env python3 +"""Read-only replay of the flag-43 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: every native edge, every endpoint adapter, all +280 framed rows and the 72 dirty-helper restorations. It then recomputes the +bill, the head co-hosting facts and the forced-hosting closure of every Y59 +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 = 43 +SELECTED_KAPPA = "0.001672660197076918" +MARKER = ( + "PASS_P104_FLAG43_HEAD_STEP_REPAIR flag=43 head=15 repaired_update=3364 " + "added_events=0 added_adds=0 added_transports=0 added_rank_mass=0 " + "retargeted_transports=9 forced_registers=4 profile_delta=-3H1+5H2-H3-H4 " + "native_validate=PASS earlier_updates_obstructed=14/14 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 = "flag43_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 + + +# --- GF(2) frames ----------------------------------------------------------- + +def span(vectors): + out = {0} + for v in vectors: + out |= {x ^ v for x in tuple(out)} + return frozenset(out) + + +def rank(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"] + mv = lambda rows, x: sum((((row & x).bit_count()) & 1) << i for i, row in enumerate(rows)) + dot = lambda a, b: (a & mv(dual, b)).bit_count() & 1 + convert = lambda x: sum(dot(x, v) << j for j, v in enumerate(orth)) + return lambda frame: canon(convert(x) for x in frame) + + +# --- schedules --------------------------------------------------------------- + +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 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(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 majorized(small, big): + """True when `small` is majorized by `big` (same length and sum).""" + s, b = sorted(small, reverse=True), sorted(big, reverse=True) + if len(s) != len(b) or sum(s) != sum(b): + return False + ps = pb = 0 + for x, y in zip(s, b): + ps += x + pb += y + if ps > pb: + return False + return True + + +# --- frame chronology -------------------------------------------------------- + +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 row_replay(witness, program, watch): + 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 == watch[0]: + carried = Fraction(a) * state[src].get(watch[1], Fraction(0)) + before = state[dst].get(watch[1], Fraction(0)) + seen.append((i, src, carried, 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 + + +# --- receipt ----------------------------------------------------------------- + +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) == ("X21", "Y59", 15), "flag 43 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"])} + repaired = {} + used = set() + for name in ("R0", "R1"): + prog = apply_splices(program, cert["repairs"][name]["splices"]) + 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") + 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] + + # Retargeted transports and the head co-hosting update. + r0 = repaired["R0"] + changed = [i for i, (a, b) in enumerate(zip(program, r0)) if a != b] + retargeted = [i for i in changed if program[i][0] == "transport"] + relabelled = [i for i in changed if program[i][0] == "add"] + for i in relabelled: + need(program[i][:4] == r0[i][:4], "add registers and coefficient unchanged") + for i in retargeted: + a, b = program[i], r0[i] + need(a[1] == b[1], "same register") + need(span(b[3]) == span(list(a[3]) + [head]) or span(b[3]) == span(a[3]), "after-frame is published plus head") + need(span(b[2]) == span(a[2]) or span(b[2]) == span(list(a[2]) + [head]), "before-frame is published plus head") + pub_ranks = [program[i][4] for i in retargeted] + new_ranks = [r0[i][4] for i in retargeted] + hist = frame_history(witness, r0) + adds = [i for i, e in enumerate(r0) if e[0] == "add" and e[1] == target] + last = adds[-1] + chart = r0[last][4] + src_frame = frame_at(hist, source, last) + later_source = [i for i, e in enumerate(r0) if i > last and source in e[1:3]] + _, seen = row_replay(witness, r0, (target, source)) + delivery = [[i, src, str(c), str(after)] for i, src, c, after in seen if c] + pub_hist = frame_history(witness, program) + pub_hosting_updates = [i for i in adds if head in frame_at(pub_hist, target, i)] + hosting_updates = [i for i in adds if head in frame_at(hist, target, i) and head in frame_at(hist, source, i)] + r1 = repaired["R1"] + h1 = frame_history(witness, r1) + adds1 = [i for i, e in enumerate(r1) if e[0] == "add" and e[1] == target] + out["R0"]["retargeted_transports"] = retargeted + out["R0"]["relabelled_add_charts"] = relabelled + out["R0"]["retargeted_ranks_published"] = pub_ranks + out["R0"]["retargeted_ranks_repaired"] = new_ranks + out["R0"]["majorized_by_published"] = majorized(new_ranks, pub_ranks) + out["R0"]["registers_changed"] = sorted({program[i][1] for i in retargeted}) + out["head_cohosting"] = { + "published_head_hosting_target_updates": pub_hosting_updates, + "R0_cohosted_target_updates": hosting_updates, + "R0_last_target_update": last, + "R0_update_partner": r0[last][2], + "R0_update_chart": chart, + "R0_update_chart_rank": rank(chart), + "R0_source_frame_rank_at_update": rank(sorted(src_frame - {0})), + "R0_source_spans_head_at_update": head in src_frame, + "R0_source_events_after_update": later_source, + "R0_source_delivery_into_target": delivery, + "R1_cohosted_target_updates": [i for i in adds1 if head in frame_at(h1, target, i) and head in frame_at(h1, source, i)], + "R1_last_target_update": adds1[-1], + } + table = closure_table(witness, program, target, head) + admissible = [row["event"] for row in table if row["admissible"]] + obstructed = [row["event"] for row in table if row["slot_independent_obstructions"]] + gain = {} + for e in program: + if e[0] == "transport": + gain[e[1]] = gain.get(e[1], 0) + e[4] + floor = [r for r in witness["initial_frames"] + if gain.get(r, 0) == rank(witness["final_frames"][r]) - rank(witness["initial_frames"][r])] + need(len(floor) == len(witness["initial_frames"]) == 280, "every non-private register at its rank floor") + out["forced_hosting"] = { + "non_private_registers_at_rank_floor": len(floor), + "table": table, + "admissible_updates": admissible, + "slot_independently_obstructed_updates": obstructed, + } + return { + "schema_version": 1, + "claim_id": "p104-flag43-head-step-repair", + "pinned_main": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "flag_index": FLAG_INDEX, + "source_register": source, + "target_register": target, + "basis_head": head, + "repairs": cert["repairs"], + "bill": {k: out[k] for k in ("published", "R0", "R1")}, + "head_cohosting": out["head_cohosting"], + "forced_hosting": out["forced_hosting"], + "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 = cert["bill"] + r0, r1, hc, fh = b["R0"], b["R1"], cert["head_cohosting"], cert["forced_hosting"] + need([r0["added_" + k] for k in ("events", "scalar_adds", "transport_occurrences", "rank_mass")] == [0, 0, 0, 0], "R0 adds nothing to the counted bill") + need(r0["profile_delta"] == {"1": -3, "2": 5, "3": -1, "4": -1}, "R0 profile delta") + need(len(r0["retargeted_transports"]) == 9 and r0["majorized_by_published"], "R0 retargets nine transports by majorization") + need(r0["registers_changed"] == ["D17", "D28", "Y103", "Y59"], "R0 changed registers") + need(r1["added_events"] == 1 and r1["added_transport_occurrences"] == 1 and r1["added_rank_mass"] == 0, "R1 bill") + need(r1["profile_delta"] == {"2": 2, "4": -1}, "R1 profile delta") + need(hc["published_head_hosting_target_updates"] == [], "published word has no head-hosting update") + need(hc["R0_cohosted_target_updates"] == [3364] and hc["R0_source_spans_head_at_update"], "R0 co-hosts the head at 3364") + need(hc["R0_source_events_after_update"] == [3705, 3760, 3811, 3863], "source still live") + need(hc["R0_source_delivery_into_target"][-1] == [3364, "D17", "1/2", "1/2"], "3364 settles the source coefficient") + need(hc["R1_cohosted_target_updates"] == [hc["R1_last_target_update"]], "R1 co-hosts at its last update") + need(fh["admissible_updates"] == [3364], "3364 is the only admissible update") + need(len(fh["slot_independently_obstructed_updates"]) == 14, "every earlier update obstructed") + forced = [row for row in fh["table"] if row["event"] == 3364][0]["forced"] + need(forced == {"D17": 3364, "Y59": 3364, "Y103": 3366, "D28": 3462}, "forced register set") + 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) From 69b13ac1f39d647c9375582541c5a30bc6419354 Mon Sep 17 00:00:00 2001 From: Wentao Li Date: Sun, 18 Oct 2026 03:57:41 +0000 Subject: [PATCH 2/2] Record master handoff for flag-43 head-step repair package --- .../MASTER-HANDOFF.md | 130 ++++++++++++++++++ 1 file changed, 130 insertions(+) create mode 100644 research/p104-flag43-head-step-repair/MASTER-HANDOFF.md diff --git a/research/p104-flag43-head-step-repair/MASTER-HANDOFF.md b/research/p104-flag43-head-step-repair/MASTER-HANDOFF.md new file mode 100644 index 0000000000..f9598a3260 --- /dev/null +++ b/research/p104-flag43-head-step-repair/MASTER-HANDOFF.md @@ -0,0 +1,130 @@ +# Master handoff — `research/p104-flag43-head-step-repair/` + +## Candidate + +- Branch: `cursor/dirty-restoration-repair-bill-eed4` (VictorLiwentao fork). The + `-eed4` suffix is this worker's environment-required branch suffix, not `-60b9`. +- Content tip: `cc77db2b62d1eaa6a1f7b9ffec7e694a910bba54`. This is the scientific + package commit, and its parent is the pinned base. +- Packaging tip: the child commit that adds only this handoff file. Read its SHA + with `git rev-parse origin/cursor/dirty-restoration-repair-bill-eed4`. +- Package: `research/p104-flag43-head-step-repair/` +- Base: CrocSwap main `6f100d4bb5083f8c35d96fd95a539811c62f245c` +- Card: `p104-side-correction` (refined), priority revision 6 +- κ: unchanged at `0.001672660197076918` +- Author: Wentao Li ``, with no co-author trailer. + +## Claim + +On present-head flag 43 (`X21` → `Y59`, head `15`), a changed schedule R0 makes +`Y59`'s last update co-host the basis head. That update is event 3364, +`Y59 += D17/4`, the ADD that settles `Y59`'s final `X21` coefficient `1/2`. It now +runs in the chart `[95,447,6,32,20,15]` while `X21` is in the full chart and still +has four later reads. + +R0 keeps every published event in order, with the same ADDs and coefficients. It +retargets nine transports of `Y59`, `D17`, `Y103` and `D28`: each changed frame is +the published frame plus `15`. It also relabels three ADD charts. + +The published `check_native.validate()` passes on the repaired word. Eight +published native edges are swapped for eight newly lowered ones. All 280 framed +rows, the 72 dirty-helper restorations and the 208 endpoint adapters hold. + +**Bill.** Events (4,058), ADDs (2,624), transport occurrences (1,410), rank mass +(2,368) and distinct native edges (740) are all unchanged. The paid profile delta +is `-3H1 + 5H2 - H3 - H4`. The published ranks of the changed transports +majorize the repaired ranks, so the delta is at most zero under any convex +per-rank price and exactly zero under any affine one. + +**Comparison R1.** R1 moves `Y103`'s 3365–3366 ahead of `Y59`'s update and adds +one rank-1 lift to `D17`. It changes only `Y59` and `D17`, at a cost of +1 event, ++1 transport occurrence and a `+2H2 - H4` profile delta. R1 is also natively +validated. + +**Obstruction.** Consider repairs that keep the published event order and ADDs, +keep endpoint frames and add no rank mass; inserted refinement transports are +allowed. All 280 non-private registers sit at their rank floor, so every path in +this class stays monotone. + +- 14 of `Y59`'s 15 updates force the head into a register whose final frame + excludes it. +- 3364 is the only admissible update. It forces exactly `D17` and `Y59` (from + 3364), `Y103` (from 3366) and `D28` (from 3462). + +Without inserted events, all nine retargeted transports are forced. + +## Why this is not a chronology reprint + +The headline is a constructed repaired word, its native validation and its bill. +The package cites, and does not re-derive, the drop/arrive chronologies of +#3456/#3451/#3443/#3392. The only fact it rechecks from #3456 is "no published +`Y59` update hosts the head", because the before/after comparison needs it. + +## Evidence commands + +```sh +python3.12 -I -B research/p104-flag43-head-step-repair/verify.py +python3.12 -I -O -Werror -B research/p104-flag43-head-step-repair/verify.py +python3.12 -I -O -Werror -B research/p104-flag43-head-step-repair/independent.py +python3.12 -I -O -Werror -B research/p104-flag43-head-step-repair/test_package.py +python3.12 -B scripts/research_package.py --package research/p104-flag43-head-step-repair +``` + +Expected markers: + +```text +PASS_P104_FLAG43_HEAD_STEP_REPAIR flag=43 head=15 repaired_update=3364 added_events=0 added_adds=0 added_transports=0 added_rank_mass=0 retargeted_transports=9 forced_registers=4 profile_delta=-3H1+5H2-H3-H4 native_validate=PASS earlier_updates_obstructed=14/14 no_new_kappa +PASS_P104_FLAG43_HEAD_STEP_REPAIR_INDEPENDENT flag=43 head=15 repaired_update=3364 added_events=0 added_adds=0 added_transports=0 added_rank_mass=0 retargeted_transports=9 forced_registers=4 profile_delta=-3H1+5H2-H3-H4 rows_equal=280/280 earlier_updates_obstructed=14/14 no_new_kappa +PASS_P104_FLAG43_HEAD_STEP_REPAIR_TESTS cases=14 clean_read_only=1 scanners=2 +PASS_REGISTERED_RESEARCH_PACKAGE research/p104-flag43-head-step-repair outcome=completed +``` + +The worker ran all five commands on the content tip in the working tree. It ran +the registered package command again in a fresh detached worktree of the pushed +content tip. The runs leave the package and the pinned inputs byte-identical. +`research_package.py --changed-since --check-only` selects only this +package. + +## Closest priors + +- #3456 `p104-present-head-flag43-audit`: flag 43's published obstruction. Its + first open question is answered here, following its suggested first step at + 3363/3364 and the `D17` common-chart constraint. Leave its chronology alone. +- #3451 (flag 1) and #3443 (flag 9): the same open question on other flags. Not + touched. +- #3349: present-head census. Reused, not re-derived. +- #3363: relay census and final coefficients. This package reports only the `X21` + entries of the three `Y59` reads, which the co-hosting statement needs. +- Merged `p104-refinement-rank-budget` and `p104-single-target-acquisition`: + priced added transports and refinements in a different model, namely identity + completion. They are not reused for any number here. + +## Soft-overlap risks + +- #3363: the event-level delivery split (`+1/2` at 3076, `-1/2` at 3231, `+1/2` + at 3364) is a coefficient fact on #3363's turf. A reviewer may ask that the + `R0_source_delivery_into_target` field be cited to #3363 or trimmed. +- #3456: R0 changes four registers' published frames. Any statement in #3456 + about the published word stays true, because only the repaired word differs. +- `Y103` and `D28` are not flag-43 endpoints. Changing their frames could matter + to a future package about flags that target `Y103`. The class-Z table shows that + these changes are forced, not chosen. +- `H_r` is left symbolic. If the repo's actual per-rank weights are strictly + concave on `{1,...,4}`, R0 costs `5H2 - 3H1 - H3 - H4 > 0`. The package does + not evaluate those weights. +- R1 reorders two reads of `D17`. That is legal under the checker, but it sits + outside the class-Z obstruction by design. + +## Open questions + +1. Do flags 1 and 9 admit an event-preserving head-step repair, or are their + closures obstructed? Use a separate package and cite #3451/#3443. +2. Can a side correction exploit R0's co-hosted head chart at 3364, and what + does `I - G/2` cost at that cut? +3. Is R0's profile majorization-minimal among class-Z repairs? + +## Disposition note for master + +This worker produces a fork branch and package only. Do **not** open a CrocSwap +PR from this worker. Master decides whether to publish or defer after an +independent skeptical review.