From 053bff9e760e05354687cc669461dd6d8effed18 Mon Sep 17 00:00:00 2001 From: Wentao Li Date: Sun, 18 Oct 2026 04:38:48 +0000 Subject: [PATCH 1/2] Research: flag-1 head-step repair co-hosts at update 2797 for exactly two added rank units (no new kappa) Answer #3451's open question 1 for present-head flag 1 (X0 -> Y7, head 232) with two natively validated repaired words: R0 keeps the event order (+1 event, +1 transport, +2 rank on D17) and R1 relocates the delivering ADD into D17's full window (0 events, 0 transports, +2 rank on Y7). An exact least-frame sweep shows zero added non-private mass is infeasible for all six order-preserving Y7 updates and for 868 of 1,115 relocation slots, so +2 is the parity floor there. Method follows #3508; selected kappa unchanged. --- .../CERTIFICATE.json | 1179 +++++++++++++++++ .../p104-flag1-head-step-repair/NOTICE.md | 14 + research/p104-flag1-head-step-repair/PROOF.md | 196 +++ .../p104-flag1-head-step-repair/README.md | 128 ++ .../REPAIR-RECIPES.json | 563 ++++++++ .../p104-flag1-head-step-repair/SOURCES.json | 81 ++ .../p104-flag1-head-step-repair/TASK.json | 102 ++ .../p104-flag1-head-step-repair/VERIFY.json | 52 + research/p104-flag1-head-step-repair/build.py | 113 ++ .../independent.py | 322 +++++ .../test_package.py | 179 +++ .../p104-flag1-head-step-repair/verify.py | 533 ++++++++ 12 files changed, 3462 insertions(+) create mode 100644 research/p104-flag1-head-step-repair/CERTIFICATE.json create mode 100644 research/p104-flag1-head-step-repair/NOTICE.md create mode 100644 research/p104-flag1-head-step-repair/PROOF.md create mode 100644 research/p104-flag1-head-step-repair/README.md create mode 100644 research/p104-flag1-head-step-repair/REPAIR-RECIPES.json create mode 100644 research/p104-flag1-head-step-repair/SOURCES.json create mode 100644 research/p104-flag1-head-step-repair/TASK.json create mode 100644 research/p104-flag1-head-step-repair/VERIFY.json create mode 100644 research/p104-flag1-head-step-repair/build.py create mode 100644 research/p104-flag1-head-step-repair/independent.py create mode 100644 research/p104-flag1-head-step-repair/test_package.py create mode 100644 research/p104-flag1-head-step-repair/verify.py diff --git a/research/p104-flag1-head-step-repair/CERTIFICATE.json b/research/p104-flag1-head-step-repair/CERTIFICATE.json new file mode 100644 index 0000000000..80c35a9f67 --- /dev/null +++ b/research/p104-flag1-head-step-repair/CERTIFICATE.json @@ -0,0 +1,1179 @@ +{ + "basis_head": 232, + "bill": { + "R0": { + "added_events": 1, + "added_rank_mass": 2, + "added_scalar_adds": 0, + "added_transport_occurrences": 1, + "distinct_native_edges": 742, + "dropped_native_edges": 2, + "endpoint_adapters": 208, + "events": 4059, + "formal_boundary_columns": 280, + "new_native_edges": 4, + "paid_profile": { + "1": 1073, + "2": 60, + "3": 86, + "4": 104, + "5": 49, + "6": 23, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "private_events_unchanged": true, + "profile_delta": { + "1": -1, + "2": 2, + "5": 1, + "6": -1 + }, + "rank_mass": 2370, + "register_mass_delta": { + "D17": 2 + }, + "scalar_adds": 2624, + "transport_occurrences": 1411 + }, + "R1": { + "added_events": 0, + "added_rank_mass": 2, + "added_scalar_adds": 0, + "added_transport_occurrences": 0, + "distinct_native_edges": 741, + "dropped_native_edges": 1, + "endpoint_adapters": 208, + "events": 4058, + "formal_boundary_columns": 280, + "new_native_edges": 2, + "paid_profile": { + "1": 1074, + "2": 58, + "3": 86, + "4": 104, + "5": 48, + "6": 23, + "7": 8, + "8": 9 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "private_events_unchanged": true, + "profile_delta": { + "6": -1, + "8": 1 + }, + "rank_mass": 2370, + "register_mass_delta": { + "Y7": 2 + }, + "scalar_adds": 2624, + "transport_occurrences": 1410 + }, + "published": { + "distinct_native_edges": 740, + "endpoint_adapters": 208, + "events": 4058, + "formal_boundary_columns": 280, + "paid_profile": { + "1": 1074, + "2": 58, + "3": 86, + "4": 104, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "rank_mass": 2368, + "scalar_adds": 2624, + "transport_occurrences": 1410 + } + }, + "claim_id": "p104-flag1-head-step-repair", + "flag_index": 1, + "forced_hosting": { + "head_closure_table": [ + { + "event": 19, + "first_obstruction": [ + "Y8", + 22, + "final frame excludes head" + ], + "must_change": 272, + "obstructions": 56, + "partner": "Q1", + "private_registers_forced": [] + }, + { + "event": 20, + "first_obstruction": [ + "Y8", + 23, + "final frame excludes head" + ], + "must_change": 268, + "obstructions": 56, + "partner": "Q4", + "private_registers_forced": [] + }, + { + "event": 2013, + "first_obstruction": [ + "Y8", + 2014, + "final frame excludes head" + ], + "must_change": 141, + "obstructions": 56, + "partner": "D5", + "private_registers_forced": [ + [ + "C", + 2465 + ] + ] + }, + { + "event": 2146, + "first_obstruction": [ + "Y8", + 2147, + "final frame excludes head" + ], + "must_change": 141, + "obstructions": 56, + "partner": "D17", + "private_registers_forced": [ + [ + "C", + 2465 + ] + ] + }, + { + "event": 2526, + "first_obstruction": [ + "Y8", + 2528, + "final frame excludes head" + ], + "must_change": 58, + "obstructions": 23, + "partner": "D5", + "private_registers_forced": [] + }, + { + "event": 2797, + "first_obstruction": [ + "Y8", + 2799, + "final frame excludes head" + ], + "must_change": 37, + "obstructions": 14, + "partner": "D17", + "private_registers_forced": [] + } + ], + "least_frame_order_preserving_infeasible": { + "19": [ + "Y0", + "Y1", + "Y101", + "Y102", + "Y103", + "Y11", + "Y13", + "Y14", + "Y16", + "Y19", + "Y21", + "Y22", + "Y23", + "Y25", + "Y28", + "Y3", + "Y30", + "Y31", + "Y32", + "Y33", + "Y35", + "Y36", + "Y38", + "Y40", + "Y42", + "Y45", + "Y47", + "Y49", + "Y52", + "Y54", + "Y56", + "Y58", + "Y59", + "Y6", + "Y61", + "Y63", + "Y65", + "Y68", + "Y70", + "Y72", + "Y74", + "Y75", + "Y77", + "Y8", + "Y80", + "Y82", + "Y84", + "Y86", + "Y88", + "Y90", + "Y92", + "Y93", + "Y94", + "Y95", + "Y97", + "Y99" + ], + "20": [ + "Y0", + "Y1", + "Y101", + "Y102", + "Y103", + "Y11", + "Y13", + "Y14", + "Y16", + "Y19", + "Y21", + "Y22", + "Y23", + "Y25", + "Y28", + "Y3", + "Y30", + "Y31", + "Y32", + "Y33", + "Y35", + "Y36", + "Y38", + "Y40", + "Y42", + "Y45", + "Y47", + "Y49", + "Y52", + "Y54", + "Y56", + "Y58", + "Y59", + "Y6", + "Y61", + "Y63", + "Y65", + "Y68", + "Y70", + "Y72", + "Y74", + "Y75", + "Y77", + "Y8", + "Y80", + "Y82", + "Y84", + "Y86", + "Y88", + "Y90", + "Y92", + "Y93", + "Y94", + "Y95", + "Y97", + "Y99" + ], + "2013": [ + "Y1", + "Y101", + "Y102", + "Y103", + "Y11", + "Y13", + "Y14", + "Y16", + "Y19", + "Y21", + "Y22", + "Y23", + "Y25", + "Y28", + "Y3", + "Y30", + "Y31", + "Y32", + "Y33", + "Y35", + "Y36", + "Y38", + "Y40", + "Y42", + "Y45", + "Y47", + "Y49", + "Y52", + "Y54", + "Y56", + "Y58", + "Y59", + "Y61", + "Y63", + "Y65", + "Y68", + "Y70", + "Y72", + "Y74", + "Y75", + "Y77", + "Y8", + "Y80", + "Y82", + "Y84", + "Y86", + "Y88", + "Y90", + "Y92", + "Y93", + "Y94", + "Y95", + "Y97", + "Y99" + ], + "2146": [ + "Y1", + "Y101", + "Y102", + "Y103", + "Y13", + "Y14", + "Y16", + "Y21", + "Y22", + "Y23", + "Y25", + "Y28", + "Y3", + "Y30", + "Y31", + "Y32", + "Y33", + "Y35", + "Y36", + "Y38", + "Y40", + "Y42", + "Y45", + "Y47", + "Y49", + "Y52", + "Y54", + "Y56", + "Y58", + "Y59", + "Y61", + "Y63", + "Y65", + "Y68", + "Y70", + "Y72", + "Y74", + "Y75", + "Y77", + "Y8", + "Y80", + "Y82", + "Y84", + "Y86", + "Y88", + "Y90", + "Y92", + "Y93", + "Y94", + "Y95", + "Y97", + "Y99" + ], + "2526": [ + "Y103", + "Y13", + "Y14", + "Y16", + "Y21", + "Y22", + "Y31", + "Y32", + "Y33", + "Y35", + "Y56", + "Y58", + "Y59", + "Y61", + "Y63", + "Y65", + "Y68", + "Y70", + "Y8", + "Y88", + "Y90", + "Y92", + "Y93" + ], + "2797": [ + "Y103", + "Y13", + "Y16", + "Y21", + "Y31", + "Y32", + "Y33", + "Y35", + "Y59", + "Y61", + "Y8", + "Y88", + "Y90", + "Y92" + ] + }, + "least_frame_relocation_scan": { + "obstructed_slots": 868, + "partner_row_writes_bounding_window": [ + 2497, + 3613 + ], + "relaxed_feasible_slots": 247, + "runs": [ + { + "after_published_first": 2497, + "after_published_last": 2525, + "infeasible": [ + "Y103", + "Y13", + "Y14", + "Y16", + "Y21", + "Y22", + "Y31", + "Y32", + "Y33", + "Y35", + "Y56", + "Y58", + "Y59", + "Y61", + "Y63", + "Y65", + "Y68", + "Y70", + "Y8", + "Y88", + "Y90", + "Y92", + "Y93" + ], + "infeasible_count": 23, + "slots": 29 + }, + { + "after_published_first": 2526, + "after_published_last": 2798, + "infeasible": [ + "Y103", + "Y13", + "Y16", + "Y21", + "Y31", + "Y32", + "Y33", + "Y35", + "Y59", + "Y61", + "Y8", + "Y88", + "Y90", + "Y92" + ], + "infeasible_count": 14, + "slots": 272 + }, + { + "after_published_first": 2799, + "after_published_last": 2802, + "infeasible": [ + "Y103", + "Y13", + "Y16", + "Y21", + "Y31", + "Y32", + "Y33", + "Y35", + "Y59", + "Y61", + "Y88", + "Y90", + "Y92" + ], + "infeasible_count": 13, + "slots": 4 + }, + { + "after_published_first": 2803, + "after_published_last": 2806, + "infeasible": [ + "Y103", + "Y16", + "Y21", + "Y31", + "Y32", + "Y33", + "Y35", + "Y59", + "Y61", + "Y88", + "Y90", + "Y92" + ], + "infeasible_count": 12, + "slots": 4 + }, + { + "after_published_first": 2807, + "after_published_last": 2810, + "infeasible": [ + "Y103", + "Y21", + "Y31", + "Y32", + "Y33", + "Y35", + "Y59", + "Y61", + "Y88", + "Y90", + "Y92" + ], + "infeasible_count": 11, + "slots": 4 + }, + { + "after_published_first": 2811, + "after_published_last": 2814, + "infeasible": [ + "Y103", + "Y31", + "Y32", + "Y33", + "Y35", + "Y59", + "Y61", + "Y88", + "Y90", + "Y92" + ], + "infeasible_count": 10, + "slots": 4 + }, + { + "after_published_first": 2815, + "after_published_last": 2816, + "infeasible": [ + "Y103", + "Y31", + "Y32", + "Y35", + "Y59", + "Y61", + "Y88", + "Y90", + "Y92" + ], + "infeasible_count": 9, + "slots": 2 + }, + { + "after_published_first": 2817, + "after_published_last": 2818, + "infeasible": [ + "Y103", + "Y31", + "Y32", + "Y59", + "Y61", + "Y88", + "Y90", + "Y92" + ], + "infeasible_count": 8, + "slots": 2 + }, + { + "after_published_first": 2819, + "after_published_last": 2820, + "infeasible": [ + "Y103", + "Y31", + "Y32", + "Y59", + "Y61", + "Y90", + "Y92" + ], + "infeasible_count": 7, + "slots": 2 + }, + { + "after_published_first": 2821, + "after_published_last": 3183, + "infeasible": [ + "Y103", + "Y31", + "Y59", + "Y61" + ], + "infeasible_count": 4, + "slots": 363 + }, + { + "after_published_first": 3184, + "after_published_last": 3187, + "infeasible": [ + "Y103", + "Y59", + "Y61" + ], + "infeasible_count": 3, + "slots": 4 + }, + { + "after_published_first": 3188, + "after_published_last": 3363, + "infeasible": [ + "Y103", + "Y59" + ], + "infeasible_count": 2, + "slots": 176 + }, + { + "after_published_first": 3364, + "after_published_last": 3365, + "infeasible": [ + "Y103" + ], + "infeasible_count": 1, + "slots": 2 + }, + { + "after_published_first": 3366, + "after_published_last": 3612, + "infeasible": [], + "infeasible_count": 0, + "slots": 247 + } + ], + "slots": 1115 + }, + "non_private_registers_at_rank_floor": 280 + }, + "head_cohosting": { + "R0": { + "cohosted_target_updates": [ + 2797 + ], + "delivering_update": 2797, + "delivering_update_event": [ + "add", + "Y7", + "D17", + "1/4", + [ + 95, + 486, + 232 + ] + ], + "source_delivery_into_target": [ + [ + 2797, + "D17", + "-1/2", + "-1/2" + ] + ], + "source_events_after_update": [ + 3643, + 3799, + 3851, + 3955 + ], + "source_frame_rank_at_update": 9, + "source_spans_head_at_update": true, + "target_updates": [ + 19, + 20, + 2013, + 2146, + 2526, + 2797 + ], + "update_chart_rank": 3 + }, + "R1": { + "cohosted_target_updates": [ + 3611 + ], + "delivering_update": 3611, + "delivering_update_event": [ + "add", + "Y7", + "D17", + "1/4", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + "source_delivery_into_target": [ + [ + 3611, + "D17", + "-1/2", + "-1/2" + ] + ], + "source_events_after_update": [ + 3642, + 3798, + 3850, + 3954 + ], + "source_frame_rank_at_update": 9, + "source_spans_head_at_update": true, + "target_updates": [ + 19, + 20, + 2013, + 2146, + 2526, + 3611 + ], + "update_chart_rank": 9 + }, + "partner_row_writes": [ + 2497, + 3613 + ], + "published_head_hosting_target_updates": [], + "published_source_delivery_into_target": [ + [ + 2797, + "D17", + "-1/2", + "-1/2" + ] + ], + "published_target_updates": [ + 19, + 20, + 2013, + 2146, + 2526, + 2797 + ], + "target_read_events": [] + }, + "no_new_kappa": true, + "pinned_main": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "repairs": { + "R0": { + "class": "order-preserving: every published event kept in published order with the same ADD registers and coefficients; one downward D17 transport inserted after the delivering ADD", + "rule": "D17 and Y7 enter the published 2797 chart plus the head (rank 3) at their last transports before 2797; D17 drops back to the published chart immediately after; Y7's terminal transport starts from the rank-3 chart", + "splices": [ + { + "events": [ + [ + "transport", + "D17", + [ + 486 + ], + [ + 95, + 486, + 232 + ], + 2 + ] + ], + "published": [ + [ + "transport", + "D17", + [ + 486 + ], + [ + 95, + 486 + ], + 1 + ] + ], + "published_range": [ + 2795, + 2796 + ] + }, + { + "events": [ + [ + "transport", + "Y7", + [ + 95 + ], + [ + 95, + 486, + 232 + ], + 2 + ] + ], + "published": [ + [ + "transport", + "Y7", + [ + 95 + ], + [ + 95, + 486 + ], + 1 + ] + ], + "published_range": [ + 2796, + 2797 + ] + }, + { + "events": [ + [ + "add", + "Y7", + "D17", + "1/4", + [ + 95, + 486, + 232 + ] + ], + [ + "transport", + "D17", + [ + 95, + 486, + 232 + ], + [ + 95, + 486 + ], + 1 + ] + ], + "published": [ + [ + "add", + "Y7", + "D17", + "1/4", + [ + 95, + 486 + ] + ] + ], + "published_range": [ + 2797, + 2798 + ] + }, + { + "events": [ + [ + "transport", + "Y7", + [ + 95, + 486, + 232 + ], + [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ], + 5 + ] + ], + "published": [ + [ + "transport", + "Y7", + [ + 95, + 486 + ], + [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ], + 6 + ] + ], + "published_range": [ + 3473, + 3474 + ] + } + ] + }, + "R1": { + "class": "relocation: the delivering ADD (with Y7's 2796 and 3473 transports) moves into D17's full-chart window between its lift at 3612 and its restoration at 3613; no event added or removed", + "rule": "Y7 lifts from [95] to the full chart, takes Y7 += D17/4 there, then drops to its final frame", + "splices": [ + { + "events": [], + "published": [ + [ + "transport", + "Y7", + [ + 95 + ], + [ + 95, + 486 + ], + 1 + ], + [ + "add", + "Y7", + "D17", + "1/4", + [ + 95, + 486 + ] + ] + ], + "published_range": [ + 2796, + 2798 + ] + }, + { + "events": [], + "published": [ + [ + "transport", + "Y7", + [ + 95, + 486 + ], + [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ], + 6 + ] + ], + "published_range": [ + 3473, + 3474 + ] + }, + { + "events": [ + [ + "transport", + "D17", + [ + 95, + 447, + 6, + 32, + 20 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 4 + ], + [ + "transport", + "Y7", + [ + 95 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 8 + ], + [ + "add", + "Y7", + "D17", + "1/4", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "transport", + "Y7", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ], + 1 + ] + ], + "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": "X0", + "target_register": "Y7" +} diff --git a/research/p104-flag1-head-step-repair/NOTICE.md b/research/p104-flag1-head-step-repair/NOTICE.md new file mode 100644 index 0000000000..da13aab69f --- /dev/null +++ b/research/p104-flag1-head-step-repair/NOTICE.md @@ -0,0 +1,14 @@ +# 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 +six 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. +The repair method and bill format follow open #3508 (flag-43 repair); the +flag-1 published chronology is #3451. + +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-flag1-head-step-repair/PROOF.md b/research/p104-flag1-head-step-repair/PROOF.md new file mode 100644 index 0000000000..a74765cc09 --- /dev/null +++ b/research/p104-flag1-head-step-repair/PROOF.md @@ -0,0 +1,196 @@ +# Proof: flag-1 head-step repairs, their bill, and the zero-mass obstruction + +## Setup + +Pin CrocSwap main `6f100d4bb5083f8c35d96fd95a539811c62f245c`. Inputs: + +- The #2981 flag matching (`research/p104-joint-unit-flags/CERTIFICATE.json`). + Flag 1 has source 0, target 7 and basis `[232, 256, 7, 11, 19, 35, 64, 2, 1]`. +- 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, as in #3508: + +- Each register carries a binary frame. +- A transport is nested (up or down) and pays rank `|dim B - dim A|`. +- An ADD needs both registers in the same frame, and it changes only the + destination's row. + +A register *hosts* `232` when `232` lies in the GF(2) span of its frame. + +#3451 proves that on the published word no `Y7` update hosts the head, while +every `X0` annotation spans it. That chronology is cited, not re-derived. This +package rechecks only the one-line consequence it needs. + +## 1. The delivering update and its commutation window + +The rational replay finds that among the six `Y7` updates (19, 20, 2013, 2146, +2526, 2797), only 2797 (`Y7 += D17/4`, chart `[95, 486]`) carries any `X0` +entry. It carries `-1/2`, which is `Y7`'s final `X0` coefficient. `D17` is the +destination of exactly two events, 2497 (`D17 += C`) and 3613 (`D17 += -Q4`). +No event reads `Y7`. + +So placing the ADD anywhere after 2497 and before 3613 gives the same final rows. +This window has 1,115 slots besides the published one. + +## 2. The repairs + +Write `A2 = [95, 486]`, `A3 = A2 + [232]` and `FULL` for the rank-9 chart. + +**R0** replaces these published events (later indices shift by one): + +| Event | Published | R0 | +|---|---|---| +| 2795 | `D17: [486] -> A2`, rank 1 | `D17: [486] -> A3`, rank 2 | +| 2796 | `Y7: [95] -> A2`, rank 1 | `Y7: [95] -> A3`, rank 2 | +| 2797 | `Y7 += D17/4` in `A2` | same ADD in `A3`, then inserted `D17: A3 -> A2`, rank 1 | +| 3473 | `Y7: A2 -> final`, rank 6 | `Y7: A3 -> final`, rank 5 | + +`span(A3)` lies in `final(Y7)`, so `Y7` stays monotone and its mass is unchanged +(`1 + 6 = 2 + 5`). `D17` goes up and back down once, which adds exactly 2. + +**R1** deletes published 2796, 2797 and 3473. After 3612 (`D17: W5 -> FULL`) it +inserts three events: `Y7: [95] -> FULL` (rank 8), `Y7 += D17/4` in `FULL`, and +`Y7: FULL -> final` (rank 1, downward). `Y7`'s mass goes from `1 + 1 + 6` to +`1 + 8 + 1`, adding 2. No other register changes, and the event count is +unchanged. + +**Native validation.** `verify.py` builds each 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 each of the six new edges (four in +R0, two in R1). It then calls the published `check_native.validate()` +unchanged. That function: + +- checks every edge's full Clifford operator, phase included; +- binds every transport to its recipe and rank; +- checks all 208 endpoint adapters; +- runs the framed scalar induction over all 280 inputs. + +The induction includes the common-chart rule, the restoration of every source +and dirty helper, and each target's final row and frame. Both words pass. +`independent.py` replays both words with exact rational rows and finds all 280 +final rows equal to the published ones. + +**Co-hosting.** + +- In R0, the ADD at 2797 runs in `A3`, which spans `232`. +- In R1, it runs in `FULL` (new index 3611). +- In both, `X0` is in its rank-9 frame and has four later events, all reads. +- In both, this is the only co-hosted `Y7` update, and it delivers `X0`'s + `-1/2`. + +## 3. The bill + +All counts come from the validated words. + +| | Events | ADDs | Transports | Rank mass | Edges | Profile delta | +|---|---:|---:|---:|---:|---:|---| +| R0 | +1 | 0 | +1 | +2 | 742 | `-H1 + 2H2 + H5 - H6` | +| R1 | 0 | 0 | 0 | +2 | 741 | `-H6 + H8` | + +For affine `H(r) = a + b·r` the deltas are `a + 2b` and `2b`. For nondecreasing +`H`, `H8 - H6 >= 0`. R0's delta equals `H2 + (H2 - H1) - (H6 - H5)`. It is at +most `H2` for convex `H`, and its sign is not fixed: it is `+2` at `H = r` and +`-4` at `H = r²`. The private register `C` has identical events in all three +words. + +## 4. The zero-mass obstruction + +**Classes.** Both classes keep: + +- every ADD (same registers and coefficients); +- every endpoint frame; +- `C` completely unconstrained. + +Transports of non-private registers may be inserted, retargeted or removed +freely. + +- **Class Z₀** keeps the published relative order of all ADDs and copies. +- **Class Z₁** is Z₀, except that the delivering ADD may sit at any slot of its + commutation window (§1). + +**Parity lemma.** Take a non-private register's nested path from `init` to +`final`. Its mass is `sum |Δ_i|`, which is at least `|sum Δ_i| = rank(final) - +rank(init)` and has the same parity. Equality holds iff every step goes up, +which means the frames grow by inclusion. All 280 non-private registers meet +this floor on the published word (checked). So a repair whose non-private mass +equals the published mass has monotone non-private paths. Any other repair adds +an even amount, at least 2. + +**Least-frame sweep.** Fix a placement of the ADDs and a forced ADD `u`. Walk +the ADDs in order with `L(r) = init(r)`, skipping any ADD that involves `C`. At +each ADD between `a` and `b`, set both `L(a)` and `L(b)` to `L(a) + L(b)`, and at +`u` add `232` as well. + +By induction, in any monotone solution each register's frame at each ADD +contains its `L`, so the final frame must contain the end value of `L`. If some +`L(r)` is not inside `final(r)`, no zero-surcharge repair of that placement +co-hosts at `u`. Skipping `C`'s ADDs only removes constraints, so this verdict +stays sound with `C` free. With nothing forced, the published word passes this +check. + +**Results** (exact lists are in `CERTIFICATE.json`): + +| Placement | Infeasible registers | First (sorted) | +|---|---:|---| +| Z₀, update 19 / 20 | 56 / 56 | `Y0` | +| Z₀, update 2013 / 2146 | 54 / 52 | `Y1` | +| Z₀, update 2526 | 23 | `Y103` | +| Z₀, update 2797 | 14 | `Y103` | +| Z₁, slots after 2497–3365 (868) | 23 down to 1 | `Y103` in every slot | +| Z₁, slots after 3366–3612 (247) | 0 | — | + +#3508's head-closure rule gives the same verdict for all six Z₀ updates. It +finds 56, 56, 56, 56, 23 and 14 registers whose final frame excludes the head, +the first being `Y8` each time. `independent.py` recomputes both tests with +separate code, including a fresh full replay for every Z₁ slot. + +**Consequences.** + +1. No Z₀ repair with zero added non-private mass co-hosts at any `Y7` update. + By parity, every co-hosting Z₀ repair adds at least 2, and R0 adds exactly 2. +2. Neither does any Z₁ placement before 3366, so the same floor of 2 holds + there. +3. For placements after 3366 the relaxed sweep is feasible, so no bound is + claimed. R1 sits in this window at +2. + +The least solution there leaves `D17` empty at all of its reads. The published +word instead holds `D17` at rank 2, then 4, then 5. Realizing a low-frame word +would need re-framing large parts of the schedule. The direct attempt +intersects every frame in `D17`'s backward cone with `final(Y7)`. It reaches 208 +registers, including `C`, and needs 56 source initial frames inside `final(Y7)`, +which they are not. So that attempt fails. Open question 1 asks whether some +other construction succeeds. + +## 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. Seventeen mutations must be rejected by both scanners: + +- ten certificate fields (bill, profile, register mass, co-hosting, delivery, + closure, sweep, scan window, scan count, κ); +- a duplicate JSON key, a witness byte flip, and a phase flip in a new recipe; +- R0 without the inserted drop, and R0 with only `Y7` lifted. Both must fail at + the common-chart rule. +- an undercharged 2795 transport; +- R1 placed after `D17`'s restoration at 3613, which breaks `Y7`'s final row. + +## Limits + +This is a statement about finite repaired words 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. `H_r` is left symbolic. +The obstruction covers Z₀ and Z₁ before 3366, with `C` relaxed. It does not +cover: + +- reorders of other events; +- changed ADDs or endpoint frames; +- the 247 late slots. + +The +2 floor is stated for non-private mass. Both repairs leave `C` unchanged, +so their total and non-private surcharges agree. diff --git a/research/p104-flag1-head-step-repair/README.md b/research/p104-flag1-head-step-repair/README.md new file mode 100644 index 0000000000..80b16f99b0 --- /dev/null +++ b/research/p104-flag1-head-step-repair/README.md @@ -0,0 +1,128 @@ +# Flag 1's basis head can be co-hosted at its delivering target update for exactly two added rank units + +**Finite repaired words with an exact bill, plus a zero-mass obstruction. No new exponent.** + +Open [#3451](https://github.com/CrocSwap/integer-mult-bounds/pull/3451) is the +published obstruction for present-head flag 1 (`X0` → `Y7`, basis head `232`). +Its first open question asks whether a changed schedule can put `232` into +`Y7`'s span by its last update while `X0` is still live, and at what cost. This +package answers that question. It cites #3451's chronology without re-deriving it, +and it follows the method of open +[#3508](https://github.com/CrocSwap/integer-mult-bounds/pull/3508) (the flag-43 +repair). The answer differs from flag 43: flag 1 has no zero-cost repair. + +## Result + +Event 2797, `Y7 += D17/4`, is the only `Y7` update that carries `X0`. It brings +`-1/2` and settles `Y7`'s final `X0` coefficient. `D17`'s row is fixed from its +write at 2497 until its restoration at 3613, and `Y7` is never read. So this ADD +commutes freely within that window. + +Two repaired words make 2797's ADD co-host the head while `X0` sits in its +rank-9 full chart with four later reads. The published `check_native.validate()` +passes unchanged on both. It covers every native edge, all 208 endpoint adapters +and all 280 framed rows, including the restoration of the 72 dirty helpers. + +- **R0 (order-preserving).** `D17` and `Y7` enter `[95, 486, 232]`, the published + 2797 chart plus the head, at their last transports before 2797. The ADD runs + there. One inserted transport then drops `D17` back to `[95, 486]` for its 12 + remaining reads, and `Y7`'s terminal transport starts from the rank-3 chart. +- **R1 (relocation).** `Y7`'s 2796 transport, the ADD and the 3473 transport move + into `D17`'s full-chart window between 3612 and 3613. `Y7` lifts `[95]` to the + full chart, takes the ADD there, then drops to its final frame. No event is + added or removed. + +| Bill term | Published | R0 | R1 | +|---|---:|---:|---:| +| Events | 4,058 | 4,059 | 4,058 | +| Scalar ADDs | 2,624 | 2,624 | 2,624 | +| Transport occurrences | 1,410 | 1,411 | 1,410 | +| Rank mass | 2,368 | 2,370 | 2,370 | +| Distinct native edges | 740 | 742 | 741 | +| Where the +2 sits | — | `D17` | `Y7` | +| Paid profile delta | — | `-H1 + 2H2 + H5 - H6` | `H8 - H6` | + +Under an affine per-rank price `H(r) = a + b·r`, R0 costs `a + 2b` (one transport +plus two rank units) and R1 costs `2b`. The extra cost is positive for any +positive affine price. Under convex prices R1 stays at `H8 - H6 >= 0` for any +nondecreasing `H`. The sign of R0's delta is not fixed: `+2` at `H(r) = r` and +`-4` at `H(r) = r²`. Neither repair touches the private register `C`. + +## Obstruction: zero added mass is blocked + +All 280 non-private registers sit at their rank floor. With no added +non-private rank mass, every non-private path is therefore monotone. Over a +register's path, mass minus floor is always even. So any nonzero surcharge is at +least 2. + +Two independent tests show that zero is impossible in the classes below. + +- **Head closure (the #3508 rule).** All six `Y7` updates (19, 20, 2013, 2146, + 2526, 2797) force the head into a register whose final frame excludes it. For + 2797 there are 14 such registers, the first being `Y8` at 2799, `D17`'s next + read. Flag 43 had one admissible update (3364); flag 1 has none. +- **Exact least-frame sweep.** For each class, a forward pass computes the + least monotone frames forced by the common-chart rule plus the head. The + private register `C` is fully relaxed, so every infeasible verdict is sound. + - Order-preserving class: infeasible for all six updates. + - Relocation class (the delivering ADD moved to any of its 1,115 legal slots + between 2497 and 3613): infeasible at 868 slots. That is every slot before + `Y103`'s read of `D17` at 3366, `D17`'s last rank-5 read; `Y103` is the last + blocker. + +Hence R0 is mass-optimal among order-preserving repairs: +2 is the parity floor +and R0 reaches it. In the 247 slots after 3366 the relaxed sweep is feasible, so +this package does **not** exclude a zero-mass relocation there. The natural +attempt fails. It intersects `D17`'s backward cone with `final(Y7)`, cascades +to 208 registers, and pushes 56 source initial frames outside the chart. That +window is open question 1. + +Selected κ stays `0.001672660197076918`. Proof details and limits are in +[PROOF.md](PROOF.md). + +## Reproduce + +```sh +python3.12 -I -B research/p104-flag1-head-step-repair/verify.py +python3.12 -I -O -Werror -B research/p104-flag1-head-step-repair/verify.py +python3.12 -I -O -Werror -B research/p104-flag1-head-step-repair/independent.py +python3.12 -I -O -Werror -B research/p104-flag1-head-step-repair/test_package.py +python3.12 -B scripts/research_package.py --package research/p104-flag1-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. It uses reduced-basis frames, its own rational replay, +its own head closure and a from-scratch least-frame replay per slot. +`test_package.py` corrupts temporary copies and checks that both scanners reject +all 17 corruptions. Two truncated R0 cascades must fail at the common-chart rule. +Two further controls cover an undercharged transport and R1 moved past `D17`'s +restoration, where the final rows break. `build.py` is the producer and is not +part of the replay. + +## Credit + +Credit #3451 for flag 1's published present-head chronology, and #3508 for the +head-step repair method, the class-Z closure rule and the bill format reused +here. Credit #3443 (flag 9) and #3349 (present-head census). Credit Nick +Petalas / #2981 for the flag matching, and the reviewed #1991 native channel +(Chafik Boukhalfa) for the witness, checker and compiler. #3363's relay census +records final coefficients; only the single `X0` entry delivered at 2797 is +re-reported here. Prepared by Wentao Li with substantial AI assistance. + +## Open next questions + +1. Is there a zero-added-mass co-hosting repair with the delivering ADD after + 3366? The relaxed sweep allows it, but any construction must lower `D17`'s + rank-4 and rank-5 charts (blocks at 3182–3188 and 3362–3366) inside + `final(Y7)` without shrinking a source's initial frame or the private + register's charts. +2. Which choice between R0 and R1, or between other +2 repairs, is cheaper under + the repo's actual per-rank weights? R0 wins for steep convex `H`, R1 for + affine `H`. +3. Does flag 9 (#3443) show the same blocked-at-zero, +2-at-floor pattern? Run + this package's head closure and least-frame sweep on its target, keeping + #3443's generator-only source-drop limit. + +[TASK.json](TASK.json) gives first steps and blockers. diff --git a/research/p104-flag1-head-step-repair/REPAIR-RECIPES.json b/research/p104-flag1-head-step-repair/REPAIR-RECIPES.json new file mode 100644 index 0000000000..18e2a0d109 --- /dev/null +++ b/research/p104-flag1-head-step-repair/REPAIR-RECIPES.json @@ -0,0 +1,563 @@ +{ + "clifford_exact_sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "compiler_sha256": "9d2fc2d81962ddb0b4dd7d6482d9918a87a6b05759690317dea79939ca5656a3", + "recipes": [ + { + "new": [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + "old": [ + 133 + ], + "rank": 8, + "recipe": { + "left": { + "linear_Z4": [ + 3, + 2, + 3, + 2, + 2, + 2, + 2, + 2, + 0 + ], + "matrix_rows": [ + 257, + 2, + 4, + 8, + 16, + 32, + 64, + 5, + 128 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 5, + 0, + 5, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 8, + "right": { + "linear_Z4": [ + 0, + 2, + 0, + 2, + 2, + 2, + 2, + 1, + 2 + ], + "matrix_rows": [ + 1, + 2, + 132, + 8, + 16, + 32, + 64, + 256, + 128 + ], + "offset": 507, + "phase": 2, + "quadratic_rows": [ + 128, + 0, + 128, + 0, + 0, + 0, + 0, + 133, + 0 + ] + } + } + }, + { + "new": [ + 263, + 133, + 30 + ], + "old": [ + 133 + ], + "rank": 2, + "recipe": { + "left": { + "linear_Z4": [ + 3, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 7, + 9, + 17, + 34, + 2, + 64, + 128, + 256, + 3 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 1, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 2, + "right": { + "linear_Z4": [ + 0, + 1, + 1, + 3, + 2, + 0, + 0, + 0, + 2 + ], + "matrix_rows": [ + 7, + 9, + 257, + 274, + 276, + 24, + 32, + 64, + 128 + ], + "offset": 2, + "phase": 1, + "quadratic_rows": [ + 270, + 279, + 279, + 25, + 14, + 0, + 0, + 0, + 7 + ] + } + } + }, + { + "new": [ + 257, + 128, + 65, + 32, + 17, + 9, + 5, + 3 + ], + "old": [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + "rank": 1, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 1, + "right": { + "linear_Z4": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 1, + 3, + 5, + 9, + 17, + 32, + 65, + 128, + 257 + ], + "offset": 350, + "phase": 1, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + } + }, + { + "new": [ + 257, + 128, + 65, + 32, + 17, + 9, + 5, + 3 + ], + "old": [ + 263, + 133, + 30 + ], + "rank": 5, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 3, + 2, + 3, + 2, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 39, + 67, + 133, + 265, + 15, + 16, + 1, + 5, + 6 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 2, + 15, + 10, + 14, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 5, + "right": { + "linear_Z4": [ + 1, + 3, + 3, + 3, + 0, + 2, + 2, + 1, + 1 + ], + "matrix_rows": [ + 385, + 477, + 91, + 264, + 32, + 335, + 384, + 128, + 272 + ], + "offset": 348, + "phase": 1, + "quadratic_rows": [ + 329, + 150, + 22, + 217, + 142, + 0, + 137, + 474, + 385 + ] + } + } + }, + { + "new": [ + 281, + 133 + ], + "old": [ + 263, + 133, + 30 + ], + "rank": 1, + "recipe": { + "left": { + "linear_Z4": [ + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 2, + 5, + 9, + 17, + 1, + 32, + 64, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 1, + "right": { + "linear_Z4": [ + 0, + 3, + 3, + 3, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 14, + 17, + 2, + 4, + 24, + 32, + 64, + 128, + 272 + ], + "offset": 1, + "phase": 0, + "quadratic_rows": [ + 16, + 14, + 14, + 30, + 9, + 0, + 0, + 0, + 0 + ] + } + } + }, + { + "new": [ + 263, + 133, + 30 + ], + "old": [ + 412 + ], + "rank": 2, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 6, + 9, + 16, + 34, + 66, + 128, + 256, + 1, + 3 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 2, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 2, + "right": { + "linear_Z4": [ + 3, + 1, + 2, + 1, + 1, + 0, + 0, + 3, + 3 + ], + "matrix_rows": [ + 402, + 137, + 385, + 18, + 148, + 280, + 256, + 32, + 64 + ], + "offset": 123, + "phase": 0, + "quadratic_rows": [ + 265, + 386, + 144, + 409, + 284, + 0, + 0, + 142, + 283 + ] + } + } + } + ], + "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-flag1-head-step-repair/SOURCES.json b/research/p104-flag1-head-step-repair/SOURCES.json new file mode 100644 index 0000000000..649045ce11 --- /dev/null +++ b/research/p104-flag1-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 1 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-flag1-head-step-repair/TASK.json b/research/p104-flag1-head-step-repair/TASK.json new file mode 100644 index 0000000000..21395e0b3f --- /dev/null +++ b/research/p104-flag1-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": "Answer #3451's first open question for present-head flag 1 (X0 -> Y7, basis head 232): price changed schedules that co-host the head at Y7's delivering update (2797, the only Y7 update carrying X0) while X0 still hosts it and is live. Build two explicit splices of the published #1991 word, run the published p104-native-channel validate() on each with six newly lowered native edges, and give the exact before/after bill (events, ADDs, transport occurrences, rank mass, paid H_r profile, native edges, per-register surcharge). Add the matching obstruction: with zero added non-private rank mass no order-preserving repair co-hosts at any of Y7's six updates, and no relocation of the delivering ADD to any of 868 of its 1,115 legal slots does either; by parity the surcharge floor there is 2.", + "scope_change_reason": "#3451 proves the published word never co-hosts flag 1's basis head at a target update and leaves pricing a repair open; #3508 priced the analogous flag-43 repair at zero added cost. This package cites #3451 and #3508 without re-deriving them, and shows that flag 1 differs: its forced set is blocked at zero mass, so the repair costs two rank units.", + "bottleneck_link": "Unlike flag 43, the present-head obstruction on flag 1 is not a pure scheduling artefact: every order-preserving co-hosting repair needs at least two added rank units, and two natively validated repairs reach exactly that floor (R0 order-preserving +1 event/+1 transport/+2 rank; R1 relocated, 0 events/0 transports/+2 rank). Whether a zero-mass relocation exists after 3366 is left open. This does not supply I-G/2, a side correction or a supplier.", + "budget_minutes": 60, + "stop_rule": "Stop after one flag (1): one order-preserving repair R0 and one relocation R1, both natively validated and billed, plus the head closure and exact least-frame zero-mass sweep for every Y7 update and every relocation slot of the delivering ADD. Do not touch flags 0, 9 or 43, recompute relay coefficients beyond the X0 entry delivered into Y7, or build a side correction.", + "outcome": "completed", + "evidence": "Only 2797 (Y7 += D17/4, chart [95,486]) carries X0 into Y7 (-1/2, its final coefficient); D17's row is written only at 2497 and 3613 and Y7 is never read. R0 retargets 2795 (D17 [486]->[95,486,232], rank 2), 2796 (Y7 [95]->[95,486,232], rank 2), relabels the 2797 chart to [95,486,232], inserts D17 [95,486,232]->[95,486] (rank 1) after it, and retargets 3473 (Y7 -> final, rank 5). R1 moves Y7's 2796/2797/3473 into D17's full window after 3612: Y7 [95]->FULL (rank 8), the ADD in FULL, Y7 FULL->final (rank 1). The published check_native.validate() passes on both (742 and 741 native edges, 208 adapters, 280 framed rows, 72 dirty helpers restored); independent replay gives 280/280 rows equal. Bill: R0 4059 events, 2624 ADDs, 1411 transports, rank mass 2370, profile delta -H1+2H2+H5-H6, +2 on D17; R1 4058 events, 2624 ADDs, 1410 transports, rank mass 2370, delta H8-H6, +2 on Y7; C untouched. Obstruction: all 280 non-private registers sit at their rank floor; the #3508 head closure blocks all six Y7 updates (56,56,56,56,23,14 excluded finals, first Y8); the exact least-frame sweep with C relaxed is infeasible for all six order-preserving updates and for 868/1115 relocation slots (every slot before Y103's read at 3366), feasible for the remaining 247. Selected kappa unchanged.", + "author": "Wentao Li", + "ai_assistance": "Substantial AI assistance for derivation, implementation, checking and writing.", + "no_new_kappa": true, + "open_questions": [ + { + "question": "Is there a zero-added-mass co-hosting repair with flag 1's delivering ADD relocated after 3366?", + "why_it_matters": "The relaxed least-frame sweep allows it; a construction would make flag 1's present-head obstruction a pure scheduling artefact like flag 43's, while a proof of impossibility would make the +2 floor global over relocations.", + "first_step": "Search for frames that place D17's 3182-3188 and 3362-3366 read charts inside final(Y7) by lowering the five partner targets' frames, keeping X sources' initial frames and the private register's charts fixed.", + "blocked_by": "The direct intersection with final(Y7) cascades to 208 registers and needs 56 source initial frames inside final(Y7); no alternative construction is attempted here." + }, + { + "question": "Which +2 repair is cheaper under the repository's actual per-rank weights?", + "why_it_matters": "R0 costs a+2b and R1 costs 2b under affine prices, but R0's delta -H1+2H2+H5-H6 turns negative for steep convex prices (H=r^2 gives -4).", + "first_step": "Evaluate both deltas under the per-rank weights used by the selected channel bill.", + "blocked_by": "H_r is left symbolic here." + }, + { + "question": "Does flag 9 (#3443) follow flag 1's pattern (blocked at zero mass, +2 at the floor) or flag 43's (zero-cost repair)?", + "why_it_matters": "It decides whether the present-head obstruction is uniformly priced or split by flag.", + "first_step": "Run this package's head closure and least-frame sweep on flag 9's target with head 196 in a separate package citing #3443, keeping its generator-only source-drop limit.", + "blocked_by": "Flag 9 is the subject of open #3443 and is not touched here." + } + ] +} diff --git a/research/p104-flag1-head-step-repair/VERIFY.json b/research/p104-flag1-head-step-repair/VERIFY.json new file mode 100644 index 0000000000..937e648555 --- /dev/null +++ b/research/p104-flag1-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": 300, + "checks": "Applies repairs R0 and R1 to the published witness in memory, runs the published check_native.validate() on each (every native edge incl. 6 committed new-edge recipes, 208 endpoint adapters, all 280 framed rows and dirty-helper restorations), recomputes the bill, per-register surcharge, head co-hosting and X0 delivery, the head closure of all six Y7 updates, and the exact least-frame zero-mass sweep (order-preserving and all 1,115 relocation slots), and requires equality with CERTIFICATE.json" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 300, + "checks": "Separately written replay with reduced-basis 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, profile delta and register surcharge, head co-hosting and delivery, single-pass head closure, from-scratch least-frame replay for every order-preserving update and relocation slot, 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; 17 rejections by both scanners under -O: ten certificate field corruptions, duplicate JSON key, witness byte flip, new-recipe phase corruption, two truncated R0 cascades rejected at the common-chart rule, an undercharged transport, and R1 placed after D17's restoration" + } + ] +} diff --git a/research/p104-flag1-head-step-repair/build.py b/research/p104-flag1-head-step-repair/build.py new file mode 100644 index 0000000000..bcc6d7e287 --- /dev/null +++ b/research/p104-flag1-head-step-repair/build.py @@ -0,0 +1,113 @@ +#!/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" + +A2 = [95, 486] +A3 = A2 + [232] +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(2795, ["transport", "D17", [486], A3, 2]), + one(2796, ["transport", "Y7", [95], A3, 2]), + {"published_range": [2797, 2798], "published": [program[2797]], + "events": [["add", "Y7", "D17", "1/4", A3], ["transport", "D17", A3, A2, 1]]}, + one(3473, ["transport", "Y7", A3, final["Y7"], 5]), + ] + r1 = [ + {"published_range": [2796, 2798], "published": program[2796:2798], "events": []}, + {"published_range": [3473, 3474], "published": [program[3473]], "events": []}, + {"published_range": [3612, 3613], "published": [program[3612]], + "events": [program[3612], + ["transport", "Y7", [95], FULL, 8], + ["add", "Y7", "D17", "1/4", FULL], + ["transport", "Y7", FULL, final["Y7"], 1]]}, + ] + return { + "R0": { + "class": "order-preserving: every published event kept in published order with the same ADD registers and coefficients; one downward D17 transport inserted after the delivering ADD", + "rule": "D17 and Y7 enter the published 2797 chart plus the head (rank 3) at their last transports before 2797; D17 drops back to the published chart immediately after; Y7's terminal transport starts from the rank-3 chart", + "splices": r0, + }, + "R1": { + "class": "relocation: the delivering ADD (with Y7's 2796 and 3473 transports) moves into D17's full-chart window between its lift at 3612 and its restoration at 3613; no event added or removed", + "rule": "Y7 lifts from [95] to the full chart, takes Y7 += D17/4 there, then drops to its final frame", + "splices": r1, + }, + } + + +def load(name, path, digest): + raw = path.read_bytes() + V.need(hashlib.sha256(raw).hexdigest() == digest, "pinned compiler module: " + str(path)) + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--force", action="store_true") + args = ap.parse_args() + for name in ("CERTIFICATE.json", "REPAIR-RECIPES.json"): + V.need(args.force or not (HERE / name).exists(), name + " exists") + root = V.ROOT + load("flag1_clifford_pin", root / V.NATIVE / "vendor/clifford_exact.py", CLIFFORD_SHA256) + co = load("flag1_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-flag1-head-step-repair/independent.py b/research/p104-flag1-head-step-repair/independent.py new file mode 100644 index 0000000000..2741085c77 --- /dev/null +++ b/research/p104-flag1-head-step-repair/independent.py @@ -0,0 +1,322 @@ +#!/usr/bin/env python3 +"""Second, separately written scanner for the flag-1 head-step repair bill. + +Does not import verify.py, check_native.py or the compiler. Frames are kept as +reduced GF(2) bases; the repaired words are replayed with exact rational rows +and compared register by register with the published word's final rows and +frames. The zero-mass obstruction is recomputed by a fresh least-frame replay +for each order-preserving target update and for each relocation slot of the +delivering ADD. 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_FLAG1_HEAD_STEP_REPAIR_INDEPENDENT flag=1 head=232 delivering_update=2797 " + "R0 added_events=1 added_transports=1 added_rank_mass=2 R1 added_events=0 added_transports=0 " + "added_rank_mass=2 rows_equal=280/280 zero_mass_order_preserving=0/6 " + "zero_mass_relocation_obstructed=868/1115 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 basis(vectors): + """Reduced row-echelon basis as a sorted tuple; equal subspaces give equal tuples.""" + rows = [] + for v in vectors: + for r in rows: + if v ^ r < v: + v ^= r + if v: + rows = [r ^ v if r ^ v < r else r for r in rows] + rows.append(v) + rows.sort(reverse=True) + return tuple(rows) + + +def inside(a, b): + return basis(b + a) == b + + +def dim(b): + return len(b) + + +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: basis(f) for n, f in witness["initial_frames"].items()} + profile, mass, adds = {}, {}, 0 + for i, e in enumerate(program): + op = e[0] + if op == "transport": + _, r, old, new, k = e + a, b = basis(old), basis(new) + need(frames[r] == a, "transport before-frame continuity at %d" % i) + need(inside(a, b) or inside(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 + mass[r] = mass.get(r, 0) + k + elif op == "zero": + need(e[1] not in frames, "fresh private") + rows[e[1]] = {} + frames[e[1]] = basis(e[2]) + elif op == "erase": + need(frames[e[1]] == basis(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]] == basis(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] == basis(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] == basis(f), "final frame " + n) + return rows, profile, mass, adds + + +def frame_when(witness, program, reg, t): + cur = basis(witness["initial_frames"][reg]) + for i, e in enumerate(program[:t]): + if e[0] == "transport" and e[1] == reg: + cur = basis(e[3]) + return cur + + +def least(witness, program, forced_index, head): + """Least monotone frames when the C-free ADD system is forced to host the head at one ADD.""" + lo = {n: basis(f) for n, f in witness["initial_frames"].items()} + for i, e in enumerate(program): + if e[0] != "add" or "C" in (e[1], e[2]): + continue + j = basis(lo[e[1]] + lo[e[2]] + ((head,) if i == forced_index else ())) + lo[e[1]] = lo[e[2]] = j + finals = {n: basis(f) for n, f in witness["final_frames"].items()} + return sorted(n for n in finals if not inside(lo[n], finals[n])) + + +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("flag1_independent_native", root / NATIVE / "vendor/native_verify.py") + N = importlib.util.module_from_spec(spec) + spec.loader.exec_module(N) + + h = flags["helpers"][1] + head, src, tgt = h["basis"][0], "X%d" % h["source"], "Y%d" % h["target"] + need((head, src, tgt) == (232, "X0", "Y7"), "flag 1") + 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_mass, 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") + for n in witness["initial_frames"]: + need(base_mass.get(n, 0) == dim(basis(witness["final_frames"][n])) - dim(basis(witness["initial_frames"][n])), "rank floor " + n) + + 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 = {(basis(r["old"]), basis(r["new"])) for r in published_recipes["transports"]} + new_edges = {} + for rec in recipes_new: + key = (basis(rec["old"]), basis(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() + progs = {} + for name in ("R0", "R1"): + prog = splice(P, cert["repairs"][name]["splices"]) + rows, profile, mass, 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 = (basis([to_phys(x) for x in e[2]]), basis([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") + md = {r: mass.get(r, 0) - base_mass.get(r, 0) for r in sorted(set(mass) | set(base_mass)) if mass.get(r, 0) != base_mass.get(r, 0)} + need(b["register_mass_delta"] == md, name + " register mass delta") + need([e for e in prog if "C" in e[1:3]] == [e for e in P if "C" in e[1:3]], name + " private register untouched") + progs[name] = prog + need(used == set(new_edges), "every committed recipe used") + need((bill["R0"]["added_events"], bill["R0"]["added_transport_occurrences"], bill["R0"]["added_rank_mass"]) == (1, 1, 2), "R0 bill") + need(bill["R0"]["profile_delta"] == {"1": -1, "2": 2, "5": 1, "6": -1} and bill["R0"]["register_mass_delta"] == {"D17": 2}, "R0 delta") + need((bill["R1"]["added_events"], bill["R1"]["added_transport_occurrences"], bill["R1"]["added_rank_mass"]) == (0, 0, 2), "R1 bill") + need(bill["R1"]["profile_delta"] == {"6": -1, "8": 1} and bill["R1"]["register_mass_delta"] == {"Y7": 2}, "R1 delta") + + hc = cert["head_cohosting"] + upd = [i for i, e in enumerate(P) if e[0] == "add" and e[1] == tgt] + need(upd == hc["published_target_updates"] == [19, 20, 2013, 2146, 2526, 2797], "published Y7 updates") + need([i for i in upd if inside((head,), frame_when(witness, P, tgt, i))] == [] == hc["published_head_hosting_target_updates"], "published head-free updates") + need(hc["published_source_delivery_into_target"] == [[2797, "D17", "-1/2", "-1/2"]], "published delivery record") + need([i for i, e in enumerate(P) if e[0] in ("add", "copy") and e[2] == tgt] == [], "Y7 never read") + need([i for i, e in enumerate(P) if e[0] in ("add", "copy", "zero", "erase") and e[1] == "D17"] == [2497, 3613], "D17 row window") + for name in ("R0", "R1"): + prog = progs[name] + rows = {n: {n: Fraction(1)} for n in witness["initial_frames"]} + carried = [] + for i, e in enumerate(prog): + 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): + carried.append([i, e[2], str(Fraction(e[3]) * rows[e[2]][src])]) + 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(len(carried) == 1 and carried[0][1:] == ["D17", "-1/2"], name + " single delivery of X0 via D17") + u = carried[0][0] + need(hc[name]["delivering_update"] == u, name + " delivering index") + need(hc[name]["source_delivery_into_target"] == [[u, "D17", "-1/2", "-1/2"]], name + " delivery record") + need(hc[name]["delivering_update_event"] == prog[u], name + " delivering event record") + tf, sf = frame_when(witness, prog, tgt, u), frame_when(witness, prog, src, u) + need(inside((head,), tf) and inside((head,), sf) and dim(sf) == 9, name + " co-hosting at the delivering update") + co = [i for i, e in enumerate(prog) if e[0] == "add" and e[1] == tgt + and inside((head,), frame_when(witness, prog, tgt, i)) and inside((head,), frame_when(witness, prog, src, i))] + need(co == [u] == hc[name]["cohosted_target_updates"], name + " only the delivering update is co-hosted") + later = [i for i, e in enumerate(prog) if i > u and src in e[1:3]] + need(later == hc[name]["source_events_after_update"] and len(later) == 4, name + " source live") + need(dim(basis(progs["R0"][2797][4])) == 3 and dim(basis(progs["R1"][hc["R1"]["delivering_update"]][4])) == 9, "update chart ranks") + + fh = cert["forced_hosting"] + finals = {n: basis(f) for n, f in witness["final_frames"].items()} + frames_before = {} + cur = {n: basis(f) for n, f in witness["initial_frames"].items()} + for i, e in enumerate(P): + for r in {e[1], e[2]} if e[0] in ("add", "copy") else (): + frames_before[(r, i)] = cur[r] + if e[0] == "transport": + cur[e[1]] = basis(e[3]) + elif e[0] == "zero": + cur[e[1]] = basis(e[2]) + table = [] + for t0 in upd: + hosting = {} + for j in range(t0, len(P)): + e = P[j] + if e[0] not in ("add", "copy"): + continue + if j == t0 or e[1] in hosting or e[2] in hosting: + for r in (e[1], e[2]): + hosting.setdefault(r, j) + change = {r: t for r, t in hosting.items() if not inside((head,), frames_before[(r, t)])} + order = sorted(change.items(), key=lambda x: (x[1], x[0])) + hard = [[r, t, "final frame excludes head"] for r, t in order if r != "C" and not inside((head,), finals[r])] + table.append({"event": t0, "partner": P[t0][2], "must_change": len(change), "obstructions": len(hard), + "first_obstruction": hard[0] if hard else None, + "private_registers_forced": [[r, t] for r, t in order if r == "C"]}) + need(table == fh["head_closure_table"] and all(row["obstructions"] for row in table), "head-closure table") + sweep = {} + for i in upd: + sweep[str(i)] = least(witness, P, i, head) + need(least(witness, P, -1, head) == [], "published least frames feasible") + need(sweep == fh["least_frame_order_preserving_infeasible"] and all(sweep.values()), "order-preserving zero-mass obstruction") + + add = P[2797] + rest = P[:2797] + P[2798:] + runs = [] + for k in range(2498, 3613): + after = k - 1 if k <= 2797 else k + bad = least(witness, rest[:k] + [add] + rest[k:], k, head) + if runs and runs[-1][3] == bad: + runs[-1][1] = after + runs[-1][2] += 1 + else: + runs.append([after, after, 1, bad]) + scan = fh["least_frame_relocation_scan"] + need([[r["after_published_first"], r["after_published_last"], r["slots"], r["infeasible"]] for r in scan["runs"]] == runs, "relocation runs") + total = sum(r[2] for r in runs) + blocked = sum(r[2] for r in runs if r[3]) + need((total, blocked) == (scan["slots"], scan["obstructed_slots"]) == (1115, 868), "relocation counts") + need(runs[-1][:3] == [3366, 3612, 247] and runs[-1][3] == [], "relaxed-feasible window") + 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-flag1-head-step-repair/test_package.py b/research/p104-flag1-head-step-repair/test_package.py new file mode 100644 index 0000000000..920923f07d --- /dev/null +++ b/research/p104-flag1-head-step-repair/test_package.py @@ -0,0 +1,179 @@ +#!/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") +FULL = [1, 2, 4, 8, 16, 32, 64, 128, 256] + + +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 r0_splice(start): + def get(c): + return [r for r in c["repairs"]["R0"]["splices"] if r["published_range"][0] == start][0] + return get + + +def without_drop(c): + r0_splice(2797)(c)["events"] = r0_splice(2797)(c)["events"][:1] + + +def target_only(c): + without_drop(c) + c["repairs"]["R0"]["splices"] = [r for r in c["repairs"]["R0"]["splices"] if r["published_range"][0] != 2795] + + +def undercharge(c): + r0_splice(2795)(c)["events"][0][4] = 1 + + +def r1_after_restore(c): + rows = c["repairs"]["R1"]["splices"] + last = [r for r in rows if r["published_range"][0] == 3612][0] + lift, add, drop = last["events"][1:] + pub3612 = last["events"][0] + pub3613 = ["add", "D17", "Q4", -1, FULL] + last["published_range"] = [3612, 3614] + last["published"] = [pub3612, pub3613] + last["events"] = [pub3612, pub3613, lift, add, drop] + + +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() + need('"basis_head": 232,' in text, "duplicate-key anchor") + p.write_text(text.replace('"basis_head": 232,', '"basis_head": 232,\n "basis_head": 232,', 1)) + + +def flip_witness(base): + p = base / f"{NATIVE}/inputs/LOWRANK-WITNESS.json" + raw = bytearray(p.read_bytes()) + k = raw.index(b"486") + 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") + + +def scan(c): + return c["forced_hosting"]["least_frame_relocation_scan"] + + +CASES = { + "bill_rank_mass": (cert_field(lambda c: c["bill"]["R0"].__setitem__("rank_mass", 2368)), None), + "bill_profile_delta": (cert_field(lambda c: c["bill"]["R1"]["profile_delta"].__setitem__("8", 0)), None), + "register_mass": (cert_field(lambda c: c["bill"]["R0"].__setitem__("register_mass_delta", {"D17": 1, "Y7": 1})), None), + "cohosted_updates": (cert_field(lambda c: c["head_cohosting"]["R0"].__setitem__("cohosted_target_updates", [])), None), + "delivery": (cert_field(lambda c: c["head_cohosting"]["R1"]["source_delivery_into_target"][0].__setitem__(2, "1/2")), None), + "closure_2797": (cert_field(lambda c: [r.__setitem__("obstructions", 0) for r in c["forced_hosting"]["head_closure_table"] if r["event"] == 2797]), None), + "sweep_2797_feasible": (cert_field(lambda c: c["forced_hosting"]["least_frame_order_preserving_infeasible"].__setitem__("2797", [])), None), + "scan_window_moved": (cert_field(lambda c: scan(c)["runs"][-1].__setitem__("after_published_first", 3364)), None), + "scan_count": (cert_field(lambda c: scan(c).__setitem__("obstructed_slots", 1115)), 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_without_drop": (cert_field(without_drop), "common"), + "control_target_only": (cert_field(target_only), "common"), + "control_undercharge": (cert_field(undercharge), None), + "control_r1_after_restore": (cert_field(r1_after_restore), None), +} + + +def case(name): + mutate, expect = CASES[name] + with tempfile.TemporaryDirectory(prefix="flag1-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="flag1-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_FLAG1_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_FLAG1_HEAD_STEP_REPAIR_TESTS cases={len(CASES)} clean_read_only=1 scanners=2") + + +if __name__ == "__main__": + main() diff --git a/research/p104-flag1-head-step-repair/verify.py b/research/p104-flag1-head-step-repair/verify.py new file mode 100644 index 0000000000..834ddd857d --- /dev/null +++ b/research/p104-flag1-head-step-repair/verify.py @@ -0,0 +1,533 @@ +#!/usr/bin/env python3 +"""Read-only replay of the flag-1 head-step repair bill and its zero-mass obstruction. + +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, the forced-hosting closure of every Y7 +update, the exact least-frame sweep for zero added non-private rank mass +(order-preserving, and for every relocation slot of the delivering ADD), 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 = 1 +SELECTED_KAPPA = "0.001672660197076918" +PRIVATE = "C" +DELIVERY = 2797 +MARKER = ( + "PASS_P104_FLAG1_HEAD_STEP_REPAIR flag=1 head=232 delivering_update=2797 " + "R0=order_preserving added_events=1 added_adds=0 added_transports=1 added_rank_mass=2 " + "profile_delta=-H1+2H2+H5-H6 R1=relocated added_events=0 added_transports=0 added_rank_mass=2 " + "profile_delta=-H6+H8 native_validate=PASS zero_mass_order_preserving=0/6 " + "zero_mass_relocation_obstructed=868/1115 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 = "flag1_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 register_mass(program): + out = {} + for e in program: + if e[0] == "transport": + out[e[1]] = out.get(e[1], 0) + e[4] + return out + + +# --- 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 writes(program, reg): + return [i for i, e in enumerate(program) if e[0] in ("add", "copy", "zero", "erase") and e[1] == reg] + + +# --- forced closure (head propagation, as in the flag-43 package) ------------ + +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 != PRIVATE 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, 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"]) + rows.append({ + "event": i, + "partner": e[2], + "must_change": len(change), + "obstructions": len(hard), + "first_obstruction": hard[0] if hard else None, + "private_registers_forced": private, + }) + return rows + + +# --- exact least-frame sweep (zero added non-private rank mass) --------------- + +def least_step(L, e): + if e[0] != "add" or PRIVATE in (e[1], e[2]): + return + a, b = e[1], e[2] + x, y = L[a], L[b] + j = y if x <= y else x if y <= x else span(list(x) + list(y)) + L[a] = L[b] = j + + +def least_forced(L, a, b, head): + j = span(list(L[a]) + list(L[b]) + [head]) + L[a] = L[b] = j + + +def infeasible(L, finals): + return sorted(r for r in finals if not L[r] <= finals[r]) + + +def least_sweep_order_preserving(witness, program, target, head): + finals = {n: span(f) for n, f in witness["final_frames"].items()} + init = {n: span(f) for n, f in witness["initial_frames"].items()} + L = dict(init) + for e in program: + least_step(L, e) + need(infeasible(L, finals) == [], "published word feasible in the least-frame model") + out = {} + for i, e in enumerate(program): + if e[0] != "add" or e[1] != target: + continue + L = dict(init) + for j, f in enumerate(program): + if j == i: + least_forced(L, f[1], f[2], head) + else: + least_step(L, f) + out[str(i)] = infeasible(L, finals) + return out + + +def relocation_scan(witness, program, delivery, head): + """Move the delivering ADD to every slot inside its row-commutation window.""" + e = program[delivery] + target, partner = e[1], e[2] + w = writes(program, partner) + lo = max(i for i in w if i < delivery) + hi = min(i for i in w if i > delivery) + need(not [i for i, f in enumerate(program) if f[0] in ("add", "copy") and f[2] == target], "target never read") + finals = {n: span(f) for n, f in witness["final_frames"].items()} + init = {n: span(f) for n, f in witness["initial_frames"].items()} + rest = program[:delivery] + program[delivery + 1:] + L = dict(init) + for f in rest[:lo + 1]: + least_step(L, f) + runs = [] + slots = 0 + for k in range(lo + 1, hi): + after = k - 1 if k <= delivery else k + M = dict(L) + least_forced(M, target, partner, head) + for f in rest[k:]: + least_step(M, f) + bad = infeasible(M, finals) + slots += 1 + if runs and runs[-1]["infeasible"] == bad: + runs[-1]["after_published_last"] = after + runs[-1]["slots"] += 1 + else: + runs.append({"after_published_first": after, "after_published_last": after, + "slots": 1, "infeasible": bad}) + least_step(L, rest[k]) + obstructed = sum(r["slots"] for r in runs if r["infeasible"]) + return { + "partner_row_writes_bounding_window": [lo, hi], + "slots": slots, + "obstructed_slots": obstructed, + "relaxed_feasible_slots": slots - obstructed, + "runs": [dict(r, infeasible_count=len(r["infeasible"])) for r in runs], + } + + +# --- 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) == ("X0", "Y7", 232), "flag 1 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") + pub_mass = register_mass(program) + for name in ("R0", "R1"): + out[name]["profile_delta"] = profile_delta(out["published"], out[name]) + for key in ("events", "scalar_adds", "transport_occurrences", "rank_mass"): + out[name]["added_" + key] = out[name][key] - out["published"][key] + mass = register_mass(repaired[name]) + excess = {r: mass.get(r, 0) - pub_mass.get(r, 0) for r in sorted(set(mass) | set(pub_mass)) + if mass.get(r, 0) != pub_mass.get(r, 0)} + out[name]["register_mass_delta"] = excess + out[name]["private_events_unchanged"] = [e for e in repaired[name] if PRIVATE in e[1:3]] == [e for e in program if PRIVATE in e[1:3]] + + gain = register_mass(program) + 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") + + pub_hist = frame_history(witness, program) + pub_adds = [i for i, e in enumerate(program) if e[0] == "add" and e[1] == target] + _, pub_seen = row_replay(witness, program, (target, source)) + cohost = { + "published_target_updates": pub_adds, + "published_head_hosting_target_updates": [i for i in pub_adds if head in frame_at(pub_hist, target, i)], + "published_source_delivery_into_target": [[i, s, str(c), str(a)] for i, s, c, a in pub_seen if c], + "partner_row_writes": writes(program, program[DELIVERY][2]), + "target_read_events": [i for i, e in enumerate(program) if e[0] in ("add", "copy") and e[2] == target], + } + for name in ("R0", "R1"): + prog = repaired[name] + hist = frame_history(witness, prog) + adds = [i for i, e in enumerate(prog) if e[0] == "add" and e[1] == target] + co = [i for i in adds if head in frame_at(hist, target, i) and head in frame_at(hist, source, i)] + _, seen = row_replay(witness, prog, (target, source)) + delivery = [[i, s, str(c), str(a)] for i, s, c, a in seen if c] + need(len(delivery) == 1, name + " single delivering update") + u = delivery[0][0] + cohost[name] = { + "target_updates": adds, + "cohosted_target_updates": co, + "delivering_update": u, + "delivering_update_event": prog[u], + "update_chart_rank": rank(prog[u][4]), + "source_frame_rank_at_update": rank(sorted(frame_at(hist, source, u) - {0})), + "source_spans_head_at_update": head in frame_at(hist, source, u), + "source_events_after_update": [i for i, e in enumerate(prog) if i > u and source in e[1:3]], + "source_delivery_into_target": delivery, + } + + table = closure_table(witness, program, target, head) + sweep_op = least_sweep_order_preserving(witness, program, target, head) + scan = relocation_scan(witness, program, DELIVERY, head) + return { + "schema_version": 1, + "claim_id": "p104-flag1-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": cohost, + "forced_hosting": { + "non_private_registers_at_rank_floor": len(floor), + "head_closure_table": table, + "least_frame_order_preserving_infeasible": sweep_op, + "least_frame_relocation_scan": scan, + }, + "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")] == [1, 0, 1, 2], "R0 bill") + need(r0["profile_delta"] == {"1": -1, "2": 2, "5": 1, "6": -1}, "R0 profile delta") + need(r0["register_mass_delta"] == {"D17": 2} and r0["private_events_unchanged"], "R0 surcharge sits on D17") + need([r1["added_" + k] for k in ("events", "scalar_adds", "transport_occurrences", "rank_mass")] == [0, 0, 0, 2], "R1 bill") + need(r1["profile_delta"] == {"6": -1, "8": 1}, "R1 profile delta") + need(r1["register_mass_delta"] == {"Y7": 2} and r1["private_events_unchanged"], "R1 surcharge sits on Y7") + need(hc["published_head_hosting_target_updates"] == [], "published word has no head-hosting update") + need(hc["published_source_delivery_into_target"] == [[DELIVERY, "D17", "-1/2", "-1/2"]], "2797 delivers the source") + need(hc["partner_row_writes"] == [2497, 3613] and hc["target_read_events"] == [], "commutation window") + need(hc["R0"]["cohosted_target_updates"] == [DELIVERY] == [hc["R0"]["delivering_update"]], "R0 co-hosts at 2797") + need(hc["R0"]["update_chart_rank"] == 3, "R0 chart is the published chart plus the head") + u1 = hc["R1"]["delivering_update"] + need(hc["R1"]["cohosted_target_updates"] == [u1] and hc["R1"]["update_chart_rank"] == 9, "R1 co-hosts in D17's full chart") + for name in ("R0", "R1"): + need(hc[name]["source_spans_head_at_update"] and hc[name]["source_frame_rank_at_update"] == 9, name + " source hosts") + need(len(hc[name]["source_events_after_update"]) == 4, name + " source still live") + need(hc[name]["source_delivery_into_target"] == [[hc[name]["delivering_update"], "D17", "-1/2", "-1/2"]], name + " delivery") + need(all(row["obstructions"] > 0 for row in fh["head_closure_table"]) and len(fh["head_closure_table"]) == 6, "head closure blocks all six updates") + need(all(v for v in fh["least_frame_order_preserving_infeasible"].values()) and len(fh["least_frame_order_preserving_infeasible"]) == 6, "zero mass infeasible for all six order-preserving updates") + scan = fh["least_frame_relocation_scan"] + need((scan["slots"], scan["obstructed_slots"], scan["relaxed_feasible_slots"]) == (1115, 868, 247), "relocation scan counts") + need(scan["runs"][-1]["after_published_first"] == 3366 and scan["runs"][-1]["infeasible"] == [], "relaxed-feasible window starts after 3366") + 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 8fecbf7df7b48c9004bd10a0da6a81f33d455737 Mon Sep 17 00:00:00 2001 From: Wentao Li Date: Sun, 18 Oct 2026 04:43:39 +0000 Subject: [PATCH 2/2] Record master handoff for flag-1 head-step repair package Adds only MASTER-HANDOFF.md: content tip 053bff9e760e05354687cc669461dd6d8effed18, evidence commands, closest priors, soft-overlap risks and open questions. --- .../MASTER-HANDOFF.md | 133 ++++++++++++++++++ 1 file changed, 133 insertions(+) create mode 100644 research/p104-flag1-head-step-repair/MASTER-HANDOFF.md diff --git a/research/p104-flag1-head-step-repair/MASTER-HANDOFF.md b/research/p104-flag1-head-step-repair/MASTER-HANDOFF.md new file mode 100644 index 0000000000..d0674fe3b2 --- /dev/null +++ b/research/p104-flag1-head-step-repair/MASTER-HANDOFF.md @@ -0,0 +1,133 @@ +# Master handoff — `research/p104-flag1-head-step-repair/` + +## Candidate + +- Branch: `cursor/flag1-head-step-repair-0378` (VictorLiwentao fork). The + `-0378` suffix is this worker's environment-required branch suffix, not + `-60b9`. +- Content tip: `053bff9e760e05354687cc669461dd6d8effed18`. This is the + scientific package commit. 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/flag1-head-step-repair-0378`. +- Package: `research/p104-flag1-head-step-repair/` +- Base: CrocSwap main `6f100d4bb5083f8c35d96fd95a539811c62f245c` +- Card: `p104-side-correction` (refined), priority revision 6 +- κ: unchanged at `0.001672660197076918` +- Author and committer: Wentao Li ``, with no co-author + trailer (both commits were built with `git commit-tree`). +- Scratch branch `cursor/p104-flag1-head-step-repair-0378` holds an earlier + agent-identity WIP commit of the same producer. It is superseded and should + not be published. + +## Claim + +On present-head flag 1 (`X0` → `Y7`, head `232`), event 2797 (`Y7 += D17/4`) is +the only `Y7` update that carries `X0`. It brings `-1/2`, the final coefficient. + +Two changed schedules make that ADD co-host the head while `X0` sits in its +rank-9 chart and still has four later reads. The published `check_native.validate()` +passes unchanged on both. That covers all native edges (six newly lowered), 208 +adapters, 280 framed rows and 72 dirty-helper restorations. + +| | Events | ADDs | Transports | Rank mass | Profile delta | Surcharge on | +|---|---:|---:|---:|---:|---|---| +| R0 (order-preserving) | +1 | 0 | +1 | +2 | `-H1 + 2H2 + H5 - H6` | `D17` | +| R1 (relocated into `D17`'s full window) | 0 | 0 | 0 | +2 | `H8 - H6` | `Y7` | + +Under an affine price the extra cost is `a + 2b` for R0 and `2b` for R1, so it is +positive. Under a convex price R0's delta can be negative: it is `-4` at +`H = r²`. + +**Obstruction.** All 280 non-private registers are at their rank floor, and the +excess over the floor is always even. + +- The #3508 head closure blocks all six `Y7` updates. For 2797 the first + obstruction is `Y8` at 2799. +- The exact least-frame sweep (with the private register `C` relaxed, so the + verdicts are sound) says zero added non-private mass is infeasible for all six + order-preserving updates. +- It is also infeasible for 868 of 1,115 relocation slots of the delivering ADD, + namely every slot before `Y103`'s read at 3366. + +So +2 is the floor there, and R0 is mass-optimal among order-preserving +repairs. The 247 later slots are relaxed-feasible and left open. + +## Why this is not a chronology reprint + +The headline is two constructed repaired words, their native validation, their +exact bill and a zero-mass obstruction that flag 43 does not have. #3451's +drop/arrive chronology is cited, not re-derived. The only published fact +rechecked is "no `Y7` update hosts the head", which the before/after comparison +needs. + +## Evidence commands + +```sh +python3.12 -I -B research/p104-flag1-head-step-repair/verify.py +python3.12 -I -O -Werror -B research/p104-flag1-head-step-repair/verify.py +python3.12 -I -O -Werror -B research/p104-flag1-head-step-repair/independent.py +python3.12 -I -O -Werror -B research/p104-flag1-head-step-repair/test_package.py +python3.12 -B scripts/research_package.py --package research/p104-flag1-head-step-repair +``` + +Expected markers: + +```text +PASS_P104_FLAG1_HEAD_STEP_REPAIR flag=1 head=232 delivering_update=2797 R0=order_preserving added_events=1 added_adds=0 added_transports=1 added_rank_mass=2 profile_delta=-H1+2H2+H5-H6 R1=relocated added_events=0 added_transports=0 added_rank_mass=2 profile_delta=-H6+H8 native_validate=PASS zero_mass_order_preserving=0/6 zero_mass_relocation_obstructed=868/1115 no_new_kappa +PASS_P104_FLAG1_HEAD_STEP_REPAIR_INDEPENDENT flag=1 head=232 delivering_update=2797 R0 added_events=1 added_transports=1 added_rank_mass=2 R1 added_events=0 added_transports=0 added_rank_mass=2 rows_equal=280/280 zero_mass_order_preserving=0/6 zero_mass_relocation_obstructed=868/1115 no_new_kappa +PASS_P104_FLAG1_HEAD_STEP_REPAIR_TESTS cases=17 clean_read_only=1 scanners=2 +PASS_REGISTERED_RESEARCH_PACKAGE research/p104-flag1-head-step-repair outcome=completed +``` + +The worker ran all five commands in the working tree. It ran them again, +together with `research_package.py --changed-since --check-only`, in a +fresh detached worktree of the content tip. Those runs leave the tree +byte-identical. The test suite also checks this inside its temp tree. + +## Closest priors + +- #3508 `p104-flag43-head-step-repair`: the method prior. This package reuses + three things from it: the splice/assemble/validate harness, the class-Z head + closure, and the bill format. Flag 43 had a zero-cost event-preserving repair; + flag 1 does not. #3508 itself is left alone. +- #3451 `p104-present-head-flag1-audit`: the published flag-1 obstruction. Its + first open question is answered here. Cited only. +- #3443 (flag 9) and #3349 (census): cited only. +- #3363: relay census. Only the single `X0` entry delivered into `Y7` at 2797 is + re-reported. + +## Soft-overlap risks + +- **Code reuse from #3508.** About 316 of `verify.py`'s 463 non-blank lines + match #3508's `verify.py` line for line: the GF(2) helpers, splice and + assemble, bill, and closure. About 132 of `independent.py`'s 287 non-blank + lines match #3508's `independent.py`, mostly the replay and recipe check. + `independent.py` changes the frame representation (reduced bases instead of + XOR closures). The least-frame sweep and the relocation scan are new. A + reviewer may ask for a shared helper instead of a copy. +- **#3451.** The package restates "no published `Y7` update hosts the head" and + the `Y7` update list (19, 20, 2013, 2146, 2526, 2797). Both appear in #3451's + PROOF items 3–5. They are rechecked only because the bill comparison needs + them. +- **#3363.** The single coefficient fact (`-1/2` at 2797 via `D17`) is on #3363's + turf. A reviewer may want it cited to #3363 or trimmed. It is load-bearing for + "2797 is the delivering update". +- **Flag 0.** It shares source `X0`. No flag-0 or `Y34` coefficient is computed. +- **Relaxed sweep wording.** A reader could take "0 infeasible after 3366" as a + claim that zero cost is achievable. It is not: the relaxation frees `C`, and + the direct construction fails. The README and PROOF say so, and open + question 1 carries it. +- `H_r` is left symbolic. + +## Open questions + +1. Is there a zero-added-mass co-hosting relocation after 3366? +2. Which +2 repair, R0 or R1, is cheaper under the repo's actual per-rank + weights? +3. Does flag 9 (#3443) follow flag 1's pattern or flag 43's? + +## 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.