diff --git a/research/p104-flag43-head-step-repair/CERTIFICATE.json b/research/p104-flag43-head-step-repair/CERTIFICATE.json new file mode 100644 index 0000000000..4047416534 --- /dev/null +++ b/research/p104-flag43-head-step-repair/CERTIFICATE.json @@ -0,0 +1,1368 @@ +{ + "basis_head": 15, + "bill": { + "R0": { + "added_events": 0, + "added_rank_mass": 0, + "added_scalar_adds": 0, + "added_transport_occurrences": 0, + "distinct_native_edges": 740, + "dropped_native_edges": 8, + "endpoint_adapters": 208, + "events": 4058, + "formal_boundary_columns": 280, + "majorized_by_published": true, + "new_native_edges": 8, + "paid_profile": { + "1": 1071, + "2": 63, + "3": 85, + "4": 103, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "profile_delta": { + "1": -3, + "2": 5, + "3": -1, + "4": -1 + }, + "rank_mass": 2368, + "registers_changed": [ + "D17", + "D28", + "Y103", + "Y59" + ], + "relabelled_add_charts": [ + 3364, + 3366, + 3462 + ], + "retargeted_ranks_published": [ + 1, + 1, + 1, + 1, + 1, + 3, + 2, + 4, + 3 + ], + "retargeted_ranks_repaired": [ + 2, + 2, + 2, + 2, + 1, + 2, + 1, + 3, + 2 + ], + "retargeted_transports": [ + 3362, + 3363, + 3365, + 3460, + 3461, + 3525, + 3569, + 3612, + 3634 + ], + "scalar_adds": 2624, + "transport_occurrences": 1410 + }, + "R1": { + "added_events": 1, + "added_rank_mass": 0, + "added_scalar_adds": 0, + "added_transport_occurrences": 1, + "distinct_native_edges": 742, + "dropped_native_edges": 2, + "endpoint_adapters": 208, + "events": 4059, + "formal_boundary_columns": 280, + "new_native_edges": 4, + "paid_profile": { + "1": 1074, + "2": 60, + "3": 86, + "4": 103, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "profile_delta": { + "2": 2, + "4": -1 + }, + "rank_mass": 2368, + "scalar_adds": 2624, + "transport_occurrences": 1411 + }, + "published": { + "distinct_native_edges": 740, + "endpoint_adapters": 208, + "events": 4058, + "formal_boundary_columns": 280, + "paid_profile": { + "1": 1074, + "2": 58, + "3": 86, + "4": 104, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "rank_mass": 2368, + "scalar_adds": 2624, + "transport_occurrences": 1410 + } + }, + "claim_id": "p104-flag43-head-step-repair", + "flag_index": 43, + "forced_hosting": { + "admissible_updates": [ + 3364 + ], + "non_private_registers_at_rank_floor": 280, + "slot_independently_obstructed_updates": [ + 223, + 224, + 225, + 226, + 227, + 2099, + 2191, + 2275, + 2341, + 2393, + 2698, + 2891, + 3076, + 3231 + ], + "table": [ + { + "admissible": false, + "event": 223, + "first_obstruction": [ + "Y67", + 264, + "final frame excludes head" + ], + "forced": null, + "must_change": 274, + "partner": "Q1", + "private_registers_forced": [ + [ + "C", + 2462 + ] + ], + "registers_without_prior_transport": 106, + "slot_independent_obstructions": 56 + }, + { + "admissible": false, + "event": 224, + "first_obstruction": [ + "Y67", + 265, + "final frame excludes head" + ], + "forced": null, + "must_change": 273, + "partner": "Q2", + "private_registers_forced": [ + [ + "C", + 2462 + ] + ], + "registers_without_prior_transport": 102, + "slot_independent_obstructions": 56 + }, + { + "admissible": false, + "event": 225, + "first_obstruction": [ + "Y67", + 267, + "final frame excludes head" + ], + "forced": null, + "must_change": 269, + "partner": "Q4", + "private_registers_forced": [ + [ + "C", + 2462 + ] + ], + "registers_without_prior_transport": 92, + "slot_independent_obstructions": 56 + }, + { + "admissible": false, + "event": 226, + "first_obstruction": [ + "Y67", + 268, + "final frame excludes head" + ], + "forced": null, + "must_change": 266, + "partner": "Q5", + "private_registers_forced": [ + [ + "C", + 2462 + ] + ], + "registers_without_prior_transport": 87, + "slot_independent_obstructions": 56 + }, + { + "admissible": false, + "event": 227, + "first_obstruction": [ + "Y67", + 268, + "final frame excludes head" + ], + "forced": null, + "must_change": 260, + "partner": "Q6", + "private_registers_forced": [ + [ + "C", + 2462 + ] + ], + "registers_without_prior_transport": 83, + "slot_independent_obstructions": 56 + }, + { + "admissible": false, + "event": 2099, + "first_obstruction": [ + "Y96", + 2103, + "final frame excludes head" + ], + "forced": null, + "must_change": 140, + "partner": "D23", + "private_registers_forced": [ + [ + "C", + 2468 + ] + ], + "registers_without_prior_transport": 28, + "slot_independent_obstructions": 56 + }, + { + "admissible": false, + "event": 2191, + "first_obstruction": [ + "Y96", + 2194, + "final frame excludes head" + ], + "forced": null, + "must_change": 140, + "partner": "D20", + "private_registers_forced": [ + [ + "C", + 2473 + ] + ], + "registers_without_prior_transport": 19, + "slot_independent_obstructions": 56 + }, + { + "admissible": false, + "event": 2275, + "first_obstruction": [ + "Y26", + 2336, + "final frame excludes head" + ], + "forced": null, + "must_change": 140, + "partner": "D10", + "private_registers_forced": [ + [ + "C", + 2473 + ] + ], + "registers_without_prior_transport": 13, + "slot_independent_obstructions": 56 + }, + { + "admissible": false, + "event": 2341, + "first_obstruction": [ + "Y56", + 2387, + "final frame excludes head" + ], + "forced": null, + "must_change": 140, + "partner": "D5", + "private_registers_forced": [ + [ + "C", + 2473 + ] + ], + "registers_without_prior_transport": 9, + "slot_independent_obstructions": 56 + }, + { + "admissible": false, + "event": 2393, + "first_obstruction": [ + "Y22", + 2638, + "final frame excludes head" + ], + "forced": null, + "must_change": 133, + "partner": "D17", + "private_registers_forced": [ + [ + "C", + 2497 + ] + ], + "registers_without_prior_transport": 4, + "slot_independent_obstructions": 53 + }, + { + "admissible": false, + "event": 2698, + "first_obstruction": [ + "Y96", + 2706, + "final frame excludes head" + ], + "forced": null, + "must_change": 45, + "partner": "D23", + "private_registers_forced": [], + "registers_without_prior_transport": 0, + "slot_independent_obstructions": 17 + }, + { + "admissible": false, + "event": 2891, + "first_obstruction": [ + "Y96", + 2897, + "final frame excludes head" + ], + "forced": null, + "must_change": 31, + "partner": "D20", + "private_registers_forced": [], + "registers_without_prior_transport": 0, + "slot_independent_obstructions": 12 + }, + { + "admissible": false, + "event": 3076, + "first_obstruction": [ + "Y26", + 3220, + "final frame excludes head" + ], + "forced": null, + "must_change": 17, + "partner": "D10", + "private_registers_forced": [], + "registers_without_prior_transport": 0, + "slot_independent_obstructions": 4 + }, + { + "admissible": false, + "event": 3231, + "first_obstruction": [ + "Y56", + 3348, + "final frame excludes head" + ], + "forced": null, + "must_change": 10, + "partner": "D5", + "private_registers_forced": [], + "registers_without_prior_transport": 0, + "slot_independent_obstructions": 1 + }, + { + "admissible": true, + "event": 3364, + "first_obstruction": null, + "forced": { + "D17": 3364, + "D28": 3462, + "Y103": 3366, + "Y59": 3364 + }, + "must_change": 4, + "partner": "D17", + "private_registers_forced": [], + "registers_without_prior_transport": 0, + "slot_independent_obstructions": 0 + } + ] + }, + "head_cohosting": { + "R0_cohosted_target_updates": [ + 3364 + ], + "R0_last_target_update": 3364, + "R0_source_delivery_into_target": [ + [ + 3076, + "D10", + "1/2", + "1/2" + ], + [ + 3231, + "D5", + "-1/2", + "0" + ], + [ + 3364, + "D17", + "1/2", + "1/2" + ] + ], + "R0_source_events_after_update": [ + 3705, + 3760, + 3811, + 3863 + ], + "R0_source_frame_rank_at_update": 9, + "R0_source_spans_head_at_update": true, + "R0_update_chart": [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + "R0_update_chart_rank": 6, + "R0_update_partner": "D17", + "R1_cohosted_target_updates": [ + 3367 + ], + "R1_last_target_update": 3367, + "published_head_hosting_target_updates": [] + }, + "no_new_kappa": true, + "pinned_main": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "repairs": { + "R0": { + "class": "event-preserving retarget: same events in the same order, same ADD registers and coefficients, only transport frames and ranks and the matching ADD chart fields change", + "rule": "from the forced event on, each changed register's frame is its published frame plus the basis head, until a frame that already spans the head", + "splices": [ + { + "events": [ + [ + "transport", + "D17", + [ + 95, + 447, + 6, + 32 + ], + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + 2 + ] + ], + "published": [ + [ + "transport", + "D17", + [ + 95, + 447, + 6, + 32 + ], + [ + 95, + 447, + 6, + 32, + 20 + ], + 1 + ] + ], + "published_range": [ + 3362, + 3363 + ] + }, + { + "events": [ + [ + "transport", + "Y59", + [ + 95, + 447, + 32, + 20 + ], + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + 2 + ] + ], + "published": [ + [ + "transport", + "Y59", + [ + 95, + 447, + 32, + 20 + ], + [ + 95, + 447, + 6, + 32, + 20 + ], + 1 + ] + ], + "published_range": [ + 3363, + 3364 + ] + }, + { + "events": [ + [ + "add", + "Y59", + "D17", + "1/4", + [ + 95, + 447, + 6, + 32, + 20, + 15 + ] + ] + ], + "published": [ + [ + "add", + "Y59", + "D17", + "1/4", + [ + 95, + 447, + 6, + 32, + 20 + ] + ] + ], + "published_range": [ + 3364, + 3365 + ] + }, + { + "events": [ + [ + "transport", + "Y103", + [ + 95, + 447, + 32, + 20 + ], + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + 2 + ] + ], + "published": [ + [ + "transport", + "Y103", + [ + 95, + 447, + 32, + 20 + ], + [ + 95, + 447, + 6, + 32, + 20 + ], + 1 + ] + ], + "published_range": [ + 3365, + 3366 + ] + }, + { + "events": [ + [ + "add", + "Y103", + "D17", + "1/4", + [ + 95, + 447, + 6, + 32, + 20, + 15 + ] + ] + ], + "published": [ + [ + "add", + "Y103", + "D17", + "1/4", + [ + 95, + 447, + 6, + 32, + 20 + ] + ] + ], + "published_range": [ + 3366, + 3367 + ] + }, + { + "events": [ + [ + "transport", + "D28", + [ + 95, + 447, + 6, + 32, + 192 + ], + [ + 95, + 447, + 6, + 32, + 20, + 192, + 15 + ], + 2 + ] + ], + "published": [ + [ + "transport", + "D28", + [ + 95, + 447, + 6, + 32, + 192 + ], + [ + 95, + 447, + 6, + 32, + 20, + 192 + ], + 1 + ] + ], + "published_range": [ + 3460, + 3461 + ] + }, + { + "events": [ + [ + "transport", + "Y103", + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + [ + 95, + 447, + 6, + 32, + 20, + 192, + 15 + ], + 1 + ] + ], + "published": [ + [ + "transport", + "Y103", + [ + 95, + 447, + 6, + 32, + 20 + ], + [ + 95, + 447, + 6, + 32, + 20, + 192 + ], + 1 + ] + ], + "published_range": [ + 3461, + 3462 + ] + }, + { + "events": [ + [ + "add", + "Y103", + "D28", + "1/4", + [ + 95, + 447, + 6, + 32, + 20, + 192, + 15 + ] + ] + ], + "published": [ + [ + "add", + "Y103", + "D28", + "1/4", + [ + 95, + 447, + 6, + 32, + 20, + 192 + ] + ] + ], + "published_range": [ + 3462, + 3463 + ] + }, + { + "events": [ + [ + "transport", + "Y59", + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + [ + 499, + 27, + 228, + 32, + 112, + 15, + 7, + 1 + ], + 2 + ] + ], + "published": [ + [ + "transport", + "Y59", + [ + 95, + 447, + 6, + 32, + 20 + ], + [ + 499, + 27, + 228, + 32, + 112, + 15, + 7, + 1 + ], + 3 + ] + ], + "published_range": [ + 3525, + 3526 + ] + }, + { + "events": [ + [ + "transport", + "Y103", + [ + 95, + 447, + 6, + 32, + 20, + 192, + 15 + ], + [ + 351, + 80, + 44, + 27, + 3, + 12, + 224, + 6 + ], + 1 + ] + ], + "published": [ + [ + "transport", + "Y103", + [ + 95, + 447, + 6, + 32, + 20, + 192 + ], + [ + 351, + 80, + 44, + 27, + 3, + 12, + 224, + 6 + ], + 2 + ] + ], + "published_range": [ + 3569, + 3570 + ] + }, + { + "events": [ + [ + "transport", + "D17", + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 3 + ] + ], + "published": [ + [ + "transport", + "D17", + [ + 95, + 447, + 6, + 32, + 20 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 4 + ] + ], + "published_range": [ + 3612, + 3613 + ] + }, + { + "events": [ + [ + "transport", + "D28", + [ + 95, + 447, + 6, + 32, + 20, + 192, + 15 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 2 + ] + ], + "published": [ + [ + "transport", + "D28", + [ + 95, + 447, + 6, + 32, + 20, + 192 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 3 + ] + ], + "published_range": [ + 3634, + 3635 + ] + } + ] + }, + "R1": { + "class": "two-register comparison: Y103's transport and update at 3365-3366 move before Y59's, and D17 gets one added rank-1 transport", + "rule": "D17 serves Y103 in the published rank-5 chart, then lifts to the rank-6 head chart for Y59", + "splices": [ + { + "events": [ + [ + "transport", + "Y103", + [ + 95, + 447, + 32, + 20 + ], + [ + 95, + 447, + 6, + 32, + 20 + ], + 1 + ], + [ + "add", + "Y103", + "D17", + "1/4", + [ + 95, + 447, + 6, + 32, + 20 + ] + ], + [ + "transport", + "D17", + [ + 95, + 447, + 6, + 32, + 20 + ], + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + 1 + ], + [ + "transport", + "Y59", + [ + 95, + 447, + 32, + 20 + ], + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + 2 + ], + [ + "add", + "Y59", + "D17", + "1/4", + [ + 95, + 447, + 6, + 32, + 20, + 15 + ] + ] + ], + "published": [ + [ + "transport", + "Y59", + [ + 95, + 447, + 32, + 20 + ], + [ + 95, + 447, + 6, + 32, + 20 + ], + 1 + ], + [ + "add", + "Y59", + "D17", + "1/4", + [ + 95, + 447, + 6, + 32, + 20 + ] + ], + [ + "transport", + "Y103", + [ + 95, + 447, + 32, + 20 + ], + [ + 95, + 447, + 6, + 32, + 20 + ], + 1 + ], + [ + "add", + "Y103", + "D17", + "1/4", + [ + 95, + 447, + 6, + 32, + 20 + ] + ] + ], + "published_range": [ + 3363, + 3367 + ] + }, + { + "events": [ + [ + "transport", + "Y59", + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + [ + 499, + 27, + 228, + 32, + 112, + 15, + 7, + 1 + ], + 2 + ] + ], + "published": [ + [ + "transport", + "Y59", + [ + 95, + 447, + 6, + 32, + 20 + ], + [ + 499, + 27, + 228, + 32, + 112, + 15, + 7, + 1 + ], + 3 + ] + ], + "published_range": [ + 3525, + 3526 + ] + }, + { + "events": [ + [ + "transport", + "D17", + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 3 + ] + ], + "published": [ + [ + "transport", + "D17", + [ + 95, + 447, + 6, + 32, + 20 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 4 + ] + ], + "published_range": [ + 3612, + 3613 + ] + } + ] + } + }, + "schema_version": 1, + "selected_kappa": "0.001672660197076918", + "source_register": "X21", + "target_register": "Y59" +} diff --git a/research/p104-flag43-head-step-repair/MASTER-HANDOFF.md b/research/p104-flag43-head-step-repair/MASTER-HANDOFF.md new file mode 100644 index 0000000000..f9598a3260 --- /dev/null +++ b/research/p104-flag43-head-step-repair/MASTER-HANDOFF.md @@ -0,0 +1,130 @@ +# Master handoff — `research/p104-flag43-head-step-repair/` + +## Candidate + +- Branch: `cursor/dirty-restoration-repair-bill-eed4` (VictorLiwentao fork). The + `-eed4` suffix is this worker's environment-required branch suffix, not `-60b9`. +- Content tip: `cc77db2b62d1eaa6a1f7b9ffec7e694a910bba54`. This is the scientific + package commit, and its parent is the pinned base. +- Packaging tip: the child commit that adds only this handoff file. Read its SHA + with `git rev-parse origin/cursor/dirty-restoration-repair-bill-eed4`. +- Package: `research/p104-flag43-head-step-repair/` +- Base: CrocSwap main `6f100d4bb5083f8c35d96fd95a539811c62f245c` +- Card: `p104-side-correction` (refined), priority revision 6 +- κ: unchanged at `0.001672660197076918` +- Author: Wentao Li ``, with no co-author trailer. + +## Claim + +On present-head flag 43 (`X21` → `Y59`, head `15`), a changed schedule R0 makes +`Y59`'s last update co-host the basis head. That update is event 3364, +`Y59 += D17/4`, the ADD that settles `Y59`'s final `X21` coefficient `1/2`. It now +runs in the chart `[95,447,6,32,20,15]` while `X21` is in the full chart and still +has four later reads. + +R0 keeps every published event in order, with the same ADDs and coefficients. It +retargets nine transports of `Y59`, `D17`, `Y103` and `D28`: each changed frame is +the published frame plus `15`. It also relabels three ADD charts. + +The published `check_native.validate()` passes on the repaired word. Eight +published native edges are swapped for eight newly lowered ones. All 280 framed +rows, the 72 dirty-helper restorations and the 208 endpoint adapters hold. + +**Bill.** Events (4,058), ADDs (2,624), transport occurrences (1,410), rank mass +(2,368) and distinct native edges (740) are all unchanged. The paid profile delta +is `-3H1 + 5H2 - H3 - H4`. The published ranks of the changed transports +majorize the repaired ranks, so the delta is at most zero under any convex +per-rank price and exactly zero under any affine one. + +**Comparison R1.** R1 moves `Y103`'s 3365–3366 ahead of `Y59`'s update and adds +one rank-1 lift to `D17`. It changes only `Y59` and `D17`, at a cost of +1 event, ++1 transport occurrence and a `+2H2 - H4` profile delta. R1 is also natively +validated. + +**Obstruction.** Consider repairs that keep the published event order and ADDs, +keep endpoint frames and add no rank mass; inserted refinement transports are +allowed. All 280 non-private registers sit at their rank floor, so every path in +this class stays monotone. + +- 14 of `Y59`'s 15 updates force the head into a register whose final frame + excludes it. +- 3364 is the only admissible update. It forces exactly `D17` and `Y59` (from + 3364), `Y103` (from 3366) and `D28` (from 3462). + +Without inserted events, all nine retargeted transports are forced. + +## Why this is not a chronology reprint + +The headline is a constructed repaired word, its native validation and its bill. +The package cites, and does not re-derive, the drop/arrive chronologies of +#3456/#3451/#3443/#3392. The only fact it rechecks from #3456 is "no published +`Y59` update hosts the head", because the before/after comparison needs it. + +## Evidence commands + +```sh +python3.12 -I -B research/p104-flag43-head-step-repair/verify.py +python3.12 -I -O -Werror -B research/p104-flag43-head-step-repair/verify.py +python3.12 -I -O -Werror -B research/p104-flag43-head-step-repair/independent.py +python3.12 -I -O -Werror -B research/p104-flag43-head-step-repair/test_package.py +python3.12 -B scripts/research_package.py --package research/p104-flag43-head-step-repair +``` + +Expected markers: + +```text +PASS_P104_FLAG43_HEAD_STEP_REPAIR flag=43 head=15 repaired_update=3364 added_events=0 added_adds=0 added_transports=0 added_rank_mass=0 retargeted_transports=9 forced_registers=4 profile_delta=-3H1+5H2-H3-H4 native_validate=PASS earlier_updates_obstructed=14/14 no_new_kappa +PASS_P104_FLAG43_HEAD_STEP_REPAIR_INDEPENDENT flag=43 head=15 repaired_update=3364 added_events=0 added_adds=0 added_transports=0 added_rank_mass=0 retargeted_transports=9 forced_registers=4 profile_delta=-3H1+5H2-H3-H4 rows_equal=280/280 earlier_updates_obstructed=14/14 no_new_kappa +PASS_P104_FLAG43_HEAD_STEP_REPAIR_TESTS cases=14 clean_read_only=1 scanners=2 +PASS_REGISTERED_RESEARCH_PACKAGE research/p104-flag43-head-step-repair outcome=completed +``` + +The worker ran all five commands on the content tip in the working tree. It ran +the registered package command again in a fresh detached worktree of the pushed +content tip. The runs leave the package and the pinned inputs byte-identical. +`research_package.py --changed-since --check-only` selects only this +package. + +## Closest priors + +- #3456 `p104-present-head-flag43-audit`: flag 43's published obstruction. Its + first open question is answered here, following its suggested first step at + 3363/3364 and the `D17` common-chart constraint. Leave its chronology alone. +- #3451 (flag 1) and #3443 (flag 9): the same open question on other flags. Not + touched. +- #3349: present-head census. Reused, not re-derived. +- #3363: relay census and final coefficients. This package reports only the `X21` + entries of the three `Y59` reads, which the co-hosting statement needs. +- Merged `p104-refinement-rank-budget` and `p104-single-target-acquisition`: + priced added transports and refinements in a different model, namely identity + completion. They are not reused for any number here. + +## Soft-overlap risks + +- #3363: the event-level delivery split (`+1/2` at 3076, `-1/2` at 3231, `+1/2` + at 3364) is a coefficient fact on #3363's turf. A reviewer may ask that the + `R0_source_delivery_into_target` field be cited to #3363 or trimmed. +- #3456: R0 changes four registers' published frames. Any statement in #3456 + about the published word stays true, because only the repaired word differs. +- `Y103` and `D28` are not flag-43 endpoints. Changing their frames could matter + to a future package about flags that target `Y103`. The class-Z table shows that + these changes are forced, not chosen. +- `H_r` is left symbolic. If the repo's actual per-rank weights are strictly + concave on `{1,...,4}`, R0 costs `5H2 - 3H1 - H3 - H4 > 0`. The package does + not evaluate those weights. +- R1 reorders two reads of `D17`. That is legal under the checker, but it sits + outside the class-Z obstruction by design. + +## Open questions + +1. Do flags 1 and 9 admit an event-preserving head-step repair, or are their + closures obstructed? Use a separate package and cite #3451/#3443. +2. Can a side correction exploit R0's co-hosted head chart at 3364, and what + does `I - G/2` cost at that cut? +3. Is R0's profile majorization-minimal among class-Z repairs? + +## Disposition note for master + +This worker produces a fork branch and package only. Do **not** open a CrocSwap +PR from this worker. Master decides whether to publish or defer after an +independent skeptical review. diff --git a/research/p104-flag43-head-step-repair/NOTICE.md b/research/p104-flag43-head-step-repair/NOTICE.md new file mode 100644 index 0000000000..c9e8604aac --- /dev/null +++ b/research/p104-flag43-head-step-repair/NOTICE.md @@ -0,0 +1,12 @@ +# Notice + +This package applies two explicit schedule changes to the published P104 +native-channel witness in memory and checks them with the published native +checker and a second scanner. It does not modify frozen upstream sources. The +nine recipes in `REPAIR-RECIPES.json` were lowered with the pinned +`research/p104-native-channel/compile.py` and `vendor/clifford_exact.py` +(PR1991 lineage, Chafik Boukhalfa), whose notices are retained in that package. + +Prepared by Wentao Li with substantial AI assistance. +Apache-2.0; predecessor notices and exact source pins are retained in +`SOURCES.json`. diff --git a/research/p104-flag43-head-step-repair/PROOF.md b/research/p104-flag43-head-step-repair/PROOF.md new file mode 100644 index 0000000000..e15f68af79 --- /dev/null +++ b/research/p104-flag43-head-step-repair/PROOF.md @@ -0,0 +1,238 @@ +# Proof: flag-43 head-step repair, its bill, and the forced closure + +## Setup + +Pin CrocSwap main `6f100d4bb5083f8c35d96fd95a539811c62f245c`. Inputs: + +- The #2981 flag matching (`research/p104-joint-unit-flags/CERTIFICATE.json`). + Flag 43 has source 21, target 59 and basis `[15, 387, 6, 18, 32, 67, 128, 1, 2]`. +- The reviewed #1991 witness, recipes and checker in `research/p104-native-channel/`. + +All of these are hash-pinned. + +The channel semantics are those of `research/p104-native-channel/PROOF.md` §2–§3: + +- Each register carries a binary frame `W` with canonical chart `Gamma_W`. +- A transport is nested, changes only `W`, and pays one positive child of rank + `|dim B - dim A|`. +- An ADD is allowed only when both registers have the same frame. It changes + only the destination's logical row. + +A register *hosts* `15` when `15` lies in the GF(2) span of its frame. + +Leave-alone priors are cited only. #3456 proves that on the published word none +of the 15 `Y59` updates runs in a chart that spans `15`, while every `X21` +annotation spans it. This package rechecks only the one-line consequence it +needs: no published `Y59` update hosts the head. + +## 1. The repair R0 + +Let: + +- `W4 = [95,447,6,32]` and `W4' = [95,447,32,20]`; +- `W5 = [95,447,6,32,20]` and `W6 = W5 + [15]`; +- `V5 = [95,447,6,32,192]`, `V6 = V5 + [20]` and `W7 = V6 + [15]`. + +R0 replaces exactly these published events (indices are unchanged): + +| Event | Published | R0 | +|---|---|---| +| 3362 | `D17: W4 -> W5`, rank 1 | `D17: W4 -> W6`, rank 2 | +| 3363 | `Y59: W4' -> W5`, rank 1 | `Y59: W4' -> W6`, rank 2 | +| 3364 | `Y59 += D17/4` in `W5` | same ADD in `W6` | +| 3365 | `Y103: W4' -> W5`, rank 1 | `Y103: W4' -> W6`, rank 2 | +| 3366 | `Y103 += D17/4` in `W5` | same ADD in `W6` | +| 3460 | `D28: V5 -> V6`, rank 1 | `D28: V5 -> W7`, rank 2 | +| 3461 | `Y103: W5 -> V6`, rank 1 | `Y103: W6 -> W7`, rank 1 | +| 3462 | `Y103 += D28/4` in `V6` | same ADD in `W7` | +| 3525 | `Y59: W5 -> final`, rank 3 | `Y59: W6 -> final`, rank 2 | +| 3569 | `Y103: V6 -> final`, rank 2 | `Y103: W7 -> final`, rank 1 | +| 3612 | `D17: W5 -> FULL`, rank 4 | `D17: W6 -> FULL`, rank 3 | +| 3634 | `D28: V6 -> FULL`, rank 3 | `D28: W7 -> FULL`, rank 2 | + +The final frames of `Y59` and `Y103` both contain `W6`. `Y103`'s also contains +`V6` and hence `W7`. So every changed transport is nested, and its rank equals its +frame gap. `D17` and `D28` have no other events between their changed transports. + +**Native validation.** `verify.py` builds the R0 word in memory. It assembles a +recipe set from two parts: the published recipes for every edge still in use, and +the committed `REPAIR-RECIPES.json` for every new edge. Eight published edges drop +out and eight new ones enter. Edge `W4' -> W6` is shared by events 3363 and 3365, +as `W4' -> W5` was. The script then calls the published `check_native.validate()` +unchanged. That function: + +- checks every edge's complete Clifford operator, including phase, against the + independent interpreter; +- binds every transport event to its recipe and rank; +- checks all 208 intrinsic endpoint adapters; +- runs the framed scalar induction over all 280 inputs. + +The induction requires every ADD to run in a common chart. It also requires each +source and each of the 72 dirty helper rows to end equal to its original input, +and each target row to end equal to `y_t + sum_s x_s / 2`, with every +final frame matched. R0 passes. `independent.py` separately replays the published +and repaired words with exact rational rows. It finds all 280 final rows equal to +the published ones. + +**Head co-hosting.** In R0, `Y59`'s updates are the published ones. The last, +3364, runs in `W6`, which lists `15`. At 3364, `X21`'s live frame is the +rank-9 full chart. It has later events 3705, 3760, 3811 and 3863, all of them +reads. The rational replay gives the `X21` entries of the rows `Y59` reads: + +| Event | Partner | `X21` carried | `Y59`'s `X21` coefficient after | +|---|---|---:|---:| +| 3076 | `D10` | `1/2` | `1/2` | +| 3231 | `D5` | `-1/2` | `0` | +| 3364 | `D17` | `1/2` | `1/2` | + +So the ADD that leaves `Y59` with its final `X21` coefficient runs in a chart +co-hosting the basis head, while the source hosts it and is still live. #3363's +relay census records the final coefficient. The event-level split is reported +here only because the co-hosting statement needs it. + +## 2. The bill + +Counts come from the validated words: + +- events, scalar ADDs and transport occurrences are unchanged: 4,058, 2,624 and + 1,410; +- rank mass is unchanged at 2,368; +- distinct native edges are unchanged at 740; +- endpoint adapters are unchanged at 208. + +The paid profile changes from `{1:1074, 2:58, 3:86, 4:104, ...}` to +`{1:1071, 2:63, 3:85, 4:103, ...}`. The ranks of 5 to 8 are unchanged. + +Per register, the profile changes are: + +- `Y59`: `-H1 - H3 + 2H2`; +- `D17`: `-H1 - H4 + H2 + H3`; +- `Y103`: no change, since `{1,1,2}` becomes `{2,1,1}`; +- `D28`: `-H1 - H3 + 2H2`. + +The total delta is `Delta = -3H1 + 5H2 - H3 - H4`. + +Sorted in decreasing order, the nine changed ranks go from `(4,3,3,2,1,1,1,1,1)` +to `(3,2,2,2,2,2,2,1,1)`. Both sum to 17, and the repaired prefix sums never +exceed the published ones. So the published vector majorizes the repaired one. +By Karamata's inequality, `Delta <= 0` for every convex rank price `H`. +Directly: convexity gives `2H2 <= H1 + H3` and `3H2 <= 2H1 + H4`, and these two +inequalities add up to `Delta <= 0`. `Delta = 0` for every affine `H(r) = a + br`. + +**R1.** R1 replaces published events 3363–3366 by: + +1. `Y103: W4' -> W5` +2. `Y103 += D17/4` in `W5` +3. `D17: W5 -> W6`, rank 1 (added) +4. `Y59: W4' -> W6`, rank 2 +5. `Y59 += D17/4` in `W6` + +It also sets 3525 to `Y59: W6 -> final` (rank 2) and 3612 to +`D17: W6 -> FULL` (rank 3). The two reads of `D17` into distinct targets commute, +and nothing between them touches `D17`, `Y59` or `Y103`. R1 passes the same native +validation. Its bill: + +- +1 event and +1 transport occurrence; +- rank mass and ADDs unchanged; +- profile delta `+2H2 - H4`; +- 742 distinct edges. + +R1 avoids the `Y103`/`D28` cascade by giving up event preservation. + +## 3. Forced closure + +**Class Z.** A repair is in class Z when: + +1. it keeps the published events in their published order, with the same ADD + registers and coefficients, and may insert transports; +2. it keeps every initial and final frame; +3. it adds no rank mass. + +`verify.py` checks that every one of the 280 non-private registers has published +rank mass equal to `rank(final) - rank(initial)`. A register's rank mass is at +least that floor, and equals it only for a monotone path. So by condition 3 every +non-private register's path in a class-Z repair is monotone. The private register +`C` is reported separately and never counted as an obstruction. + +**Propagation lemma.** Suppose that in a class-Z repair a non-private register +`r` hosts `15` at event `t`. Then it hosts `15` at every later event, by +monotonicity. Any ADD or copy at `j >= t` that involves `r` forces its partner to +host `15` at `j`, because the two frames are equal. + +Starting from a `Y59` update `u`, take the closure of this rule. A register is +*must-change* when its published frame at its forced time does not span `15`. + +- If a must-change register's final frame excludes `15`, no monotone path can + host `15` there, so no class-Z repair makes `u` head-hosting. +- If the closure is unobstructed, the published frames already satisfy every + other forced condition, because published paths are monotone. + +`verify.py` computes the closure with a worklist and `independent.py` with a +single forward sweep. For the 15 `Y59` updates: + +| Update | Partner | Must-change | Obstructions | First obstruction | +|---:|---|---:|---:|---| +| 223–227 | `Q1, Q2, Q4, Q5, Q6` | 260–274 | 56 each | `Y67` (264–268) | +| 2099, 2191 | `D23, D20` | 140 | 56 | `Y96` | +| 2275 | `D10` | 140 | 56 | `Y26` at 2336 | +| 2341 | `D5` | 140 | 56 | `Y56` at 2387 | +| 2393 | `D17` | 133 | 53 | `Y22` at 2638 | +| 2698 | `D23` | 45 | 17 | `Y96` at 2706 | +| 2891 | `D20` | 31 | 12 | `Y96` at 2897 | +| 3076 | `D10` | 17 | 4 | `Y26` at 3220 | +| 3231 | `D5` | 10 | 1 | `Y56` at 3348 | +| 3364 | `D17` | 4 | 0 | none | + +The exact per-update values are in `CERTIFICATE.json`. So 3364 is the only update +that any class-Z repair can make head-hosting. Its must-change set is exactly: + +- `Y59` and `D17` from 3364; +- `Y103` from 3366; +- `D28` from 3462. + +**Minimality in the event-preserving subclass.** With no inserted events, each +must-change register `r` with forced time `t` behaves as follows: + +- its last transport before `t` must gain `15` in its after-frame, since no + published after-frame there spans `15`; +- each later transport of `r` then has a changed before-frame. + +Together these are exactly R0's nine transports: 2 for `Y59`, 2 for `D17`, 3 for +`Y103` and 2 for `D28`. At each forced ADD the shared frame must contain both +published frames and `15`. That gives `span(W5 + 15) = W6` at 3364 and 3366, and +`span(V6 + 15) = W7` at 3462. R0 uses exactly these minimal frames. + +## Controls + +`test_package.py` copies the package and the six pinned inputs into a temporary +tree and runs both scanners there under `-O`. The clean tree must pass and stay +byte-identical. Fourteen mutations must be rejected by both scanners: + +- seven certificate fields; +- a duplicate JSON key; +- a witness byte flip; +- a phase flip in a new recipe; +- an undercharged 3525 transport; +- three truncated cascades: `Y59` lifted alone, without `Y103`/`D28`, and without + `D28`. + +Each truncated cascade must fail at the common-chart rule. + +## Limits + +This is a statement about one finite repaired word for one flag: + +- It does not build or price the `I - G/2` side correction or a supplier. +- It does not perform global hosting or precision analysis. +- It does not change κ. + +"Co-hosting" means span membership in annotated frames. It does not model what the +head direction means inside relay registers. `H_r` is left symbolic. The repo's +actual per-rank weights decide the sign of `Delta` only if they are strictly +concave somewhere on `{1,2,3,4}`. The class-Z obstruction excludes repairs that: + +- reorder events (R1 is one such repair); +- add rank mass; +- change ADDs, coefficients or endpoint frames. + +Optimality of R0's profile among class-Z repairs is not claimed. diff --git a/research/p104-flag43-head-step-repair/README.md b/research/p104-flag43-head-step-repair/README.md new file mode 100644 index 0000000000..37f19da438 --- /dev/null +++ b/research/p104-flag43-head-step-repair/README.md @@ -0,0 +1,123 @@ +# Flag 43's basis head can be co-hosted at its delivering target update at zero added channel cost + +**Finite repaired word with an exact bill, plus a forced-closure obstruction. No new exponent.** + +Open [#3456](https://github.com/CrocSwap/integer-mult-bounds/pull/3456) shows that +on the published 4,058-event P104 word, present-head flag 43 (`X21` → `Y59`, +basis head `15`) never updates `Y59` while both endpoints host the head. Its first +open question asks what a changed schedule that fixes this would cost. The +matching questions in [#3451](https://github.com/CrocSwap/integer-mult-bounds/pull/3451) +(flag 1) and [#3443](https://github.com/CrocSwap/integer-mult-bounds/pull/3443) +(flag 9) are open for the same reason. This package answers it for flag 43 and +cites those chronologies without re-deriving them. + +## Result + +**Repair R0** keeps every published event in its published order, with the same +ADD registers and coefficients. It changes only the frames of nine existing +transports and the chart fields of three ADDs. From the forced event on, each +changed register's frame is its published frame plus `15`: + +| Register | Retargeted transports | Published ranks | Repaired ranks | +|---|---|---|---| +| `Y59` | 3363, 3525 | 1, 3 | 2, 2 | +| `D17` | 3362, 3612 | 1, 4 | 2, 3 | +| `Y103` | 3365, 3461, 3569 | 1, 1, 2 | 2, 1, 1 | +| `D28` | 3460, 3634 | 1, 3 | 2, 2 | + +The published native checker `check_native.validate()` passes unchanged on the +repaired word. That covers every native edge (eight swapped for eight newly +lowered edges, still 740), all 208 endpoint adapters, and all 280 framed rows, +including the restoration of the 72 dirty helpers. + +In R0, `Y59`'s last update (event 3364, `Y59 += D17/4`) runs in the rank-6 chart +`[95, 447, 6, 32, 20, 15]`. At that moment `X21` is in the rank-9 full chart and +has four later reads. That ADD carries `X21` coefficient `1/2` and settles +`Y59`'s final `X21` coefficient. The earlier `+1/2` at 3076 is cancelled at +3231. So the update that delivers the matched source now runs in a chart that +co-hosts the basis head. + +| Bill term | Published | R0 | R1 (comparison) | +|---|---:|---:|---:| +| Events | 4,058 | 4,058 | 4,059 | +| Scalar ADDs | 2,624 | 2,624 | 2,624 | +| Transport occurrences | 1,410 | 1,410 | 1,411 | +| Rank mass | 2,368 | 2,368 | 2,368 | +| Distinct native edges | 740 | 740 | 742 | +| Paid profile delta | — | `-3H1 + 5H2 - H3 - H4` | `+2H2 - H4` | + +R0 adds nothing to any counted bill term. Its only change is the rank profile: +the nine changed ranks `{4,3,3,2,1,1,1,1,1}` become `{3,2,2,2,2,2,2,1,1}`. The +published multiset majorizes the repaired one, so for every convex per-rank price +`H` the delta `5H2 - 3H1 - H3 - H4` is at most zero. It is exactly zero for every +affine price, and positive only for a strictly concave one. + +**Comparison R1** touches only `Y59` and `D17`. It moves `Y103`'s transport and +update (3365–3366) ahead of `Y59`'s and gives `D17` one added rank-1 lift. This +costs one event and one transport occurrence, with rank mass unchanged. R1 is +also natively validated. + +## Obstruction + +Consider the class of repairs that: + +- keep the published event order and ADDs, +- keep the endpoint frames, +- add no rank mass. + +All 280 non-private registers already sit at their rank floor, so in this class +every such path stays monotone. Inserting refinement transports is allowed. Within +this class, only event 3364 among `Y59`'s 15 updates can be made head-hosting. + +- Each of the other 14 forces the head into a register whose final frame excludes + it. The first such register is `Y67`, `Y96`, `Y26`, `Y56` or `Y22`, depending + on the update. At 3231 the single obstruction is `Y56` at event 3348. +- At 3364 the forced must-change set is exactly `Y59` and `D17` (from 3364), + `Y103` (from 3366) and `D28` (from 3462). + +If no events are inserted, all nine transports R0 retargets are forced to change. +R0 therefore uses the minimum number of changed transports and registers in that +class. + +Selected κ stays `0.001672660197076918`. Proof details and limits are in +[PROOF.md](PROOF.md). + +## Reproduce + +```sh +python3.12 -I -B research/p104-flag43-head-step-repair/verify.py +python3.12 -I -O -Werror -B research/p104-flag43-head-step-repair/verify.py +python3.12 -I -O -Werror -B research/p104-flag43-head-step-repair/independent.py +python3.12 -I -O -Werror -B research/p104-flag43-head-step-repair/test_package.py +python3.12 -B scripts/research_package.py --package research/p104-flag43-head-step-repair +``` + +`verify.py` is read-only. It loads the pinned `check_native.py` by path and runs +its `validate()` on each repaired word built in memory. Admission goes through +`need()` and still fires under `-O`. `independent.py` imports neither `verify.py` +nor the native checker. `test_package.py` corrupts temporary copies and checks +that both scanners reject every corruption. It also checks that three truncated +cascades (target only; without `Y103`; without `D28`) fail at the common-chart +rule. `build.py` is the producer and is not part of the replay. + +## Credit + +Credit #3456 for flag 43's published chronology and the `D17` common-chart first +step, which this package follows. Credit #3451 and #3443 for the flag-1 and +flag-9 present-head obstructions, and #3349 for the present-head census. Credit +Nick Petalas / #2981 for the flag matching, the reviewed #1991 native channel +(Chafik Boukhalfa) for the witness, checker and compiler, and #3363 for the relay +census whose coefficient convention is reused. Prepared by Wentao Li with +substantial AI assistance. + +## Open next questions + +1. Do flags 1 and 9 admit the same event-preserving head-step repair, or is their + forced closure obstructed? Answer this in a separate package that cites #3451 + and #3443. +2. Can a side correction use R0's co-hosted head chart at 3364 to restore + `X21`'s contribution to `Y59` dirtily, and what does the `I - G/2` correction + cost at that cut? +3. Is R0's profile majorization-minimal among event-preserving monotone repairs? + +[TASK.json](TASK.json) gives first steps and blockers. diff --git a/research/p104-flag43-head-step-repair/REPAIR-RECIPES.json b/research/p104-flag43-head-step-repair/REPAIR-RECIPES.json new file mode 100644 index 0000000000..c697547694 --- /dev/null +++ b/research/p104-flag43-head-step-repair/REPAIR-RECIPES.json @@ -0,0 +1,880 @@ +{ + "clifford_exact_sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "compiler_sha256": "9d2fc2d81962ddb0b4dd7d6482d9918a87a6b05759690317dea79939ca5656a3", + "recipes": [ + { + "new": [ + 256, + 128, + 65, + 40, + 25, + 5, + 3 + ], + "old": [ + 256, + 128, + 40, + 25, + 5 + ], + "rank": 2, + "recipe": { + "left": { + "linear_Z4": [ + 3, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 6, + 3, + 8, + 16, + 32, + 64, + 1, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 3, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 2, + "right": { + "linear_Z4": [ + 1, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 66, + 65, + 67, + 4, + 8, + 16, + 32, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 3, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + } + }, + { + "new": [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + "old": [ + 256, + 128, + 65, + 40, + 25, + 5, + 3 + ], + "rank": 2, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 5, + 9, + 17, + 34, + 67, + 2, + 1, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 2, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 2, + "right": { + "linear_Z4": [ + 0, + 0, + 0, + 2, + 0, + 1, + 3, + 0, + 0 + ], + "matrix_rows": [ + 97, + 104, + 64, + 66, + 68, + 32, + 112, + 128, + 256 + ], + "offset": 101, + "phase": 2, + "quadratic_rows": [ + 32, + 0, + 0, + 64, + 0, + 97, + 104, + 0, + 0 + ] + } + } + }, + { + "new": [ + 256, + 128, + 65, + 32, + 17, + 8, + 5, + 3 + ], + "old": [ + 256, + 128, + 65, + 40, + 25, + 5, + 3 + ], + "rank": 1, + "recipe": { + "left": { + "linear_Z4": [ + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 3, + 4, + 8, + 17, + 33, + 1, + 64, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 1, + "right": { + "linear_Z4": [ + 3, + 0, + 0, + 2, + 0, + 2, + 0, + 0, + 0 + ], + "matrix_rows": [ + 9, + 33, + 2, + 4, + 32, + 48, + 64, + 128, + 256 + ], + "offset": 50, + "phase": 1, + "quadratic_rows": [ + 41, + 0, + 0, + 33, + 0, + 9, + 0, + 0, + 0 + ] + } + } + }, + { + "new": [ + 256, + 133, + 68, + 40, + 25, + 3 + ], + "old": [ + 256, + 133, + 40, + 25 + ], + "rank": 2, + "recipe": { + "left": { + "linear_Z4": [ + 3, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 5, + 1, + 10, + 16, + 32, + 64, + 2, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 1, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 2, + "right": { + "linear_Z4": [ + 1, + 2, + 1, + 0, + 0, + 0, + 2, + 0, + 0 + ], + "matrix_rows": [ + 1, + 4, + 3, + 68, + 8, + 16, + 32, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 3, + 1, + 68, + 0, + 0, + 0, + 4, + 0, + 0 + ] + } + } + }, + { + "new": [ + 256, + 133, + 68, + 40, + 25, + 3 + ], + "old": [ + 256, + 133, + 68, + 40, + 25 + ], + "rank": 1, + "recipe": { + "left": { + "linear_Z4": [ + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 3, + 1, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 1, + "right": { + "linear_Z4": [ + 1, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 1, + 3, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 3, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + } + }, + { + "new": [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + "old": [ + 256, + 133, + 68, + 40, + 25, + 3 + ], + "rank": 3, + "recipe": { + "left": { + "linear_Z4": [ + 3, + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 9, + 17, + 34, + 68, + 133, + 4, + 2, + 3, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 7, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 3, + "right": { + "linear_Z4": [ + 0, + 0, + 0, + 0, + 0, + 3, + 3, + 0, + 0 + ], + "matrix_rows": [ + 97, + 132, + 232, + 192, + 194, + 64, + 32, + 240, + 256 + ], + "offset": 118, + "phase": 3, + "quadratic_rows": [ + 160, + 0, + 192, + 192, + 0, + 97, + 108, + 13, + 0 + ] + } + } + }, + { + "new": [ + 256, + 128, + 65, + 40, + 25, + 5, + 3 + ], + "old": [ + 256, + 133, + 68, + 40, + 25, + 3 + ], + "rank": 1, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 2, + 4, + 9, + 16, + 32, + 64, + 129, + 1, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 1, + "right": { + "linear_Z4": [ + 2, + 0, + 3, + 0, + 0, + 0, + 0, + 2, + 0 + ], + "matrix_rows": [ + 132, + 5, + 2, + 128, + 8, + 16, + 32, + 192, + 256 + ], + "offset": 131, + "phase": 3, + "quadratic_rows": [ + 4, + 0, + 5, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + } + }, + { + "new": [ + 256, + 132, + 68, + 32, + 16, + 8, + 2, + 1 + ], + "old": [ + 256, + 133, + 68, + 40, + 25, + 3 + ], + "rank": 2, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 5, + 9, + 17, + 34, + 67, + 2, + 128, + 1, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 2, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 2, + "right": { + "linear_Z4": [ + 0, + 0, + 1, + 0, + 0, + 3, + 0, + 1, + 0 + ], + "matrix_rows": [ + 165, + 168, + 128, + 130, + 132, + 32, + 176, + 64, + 256 + ], + "offset": 42, + "phase": 3, + "quadratic_rows": [ + 36, + 0, + 37, + 128, + 0, + 165, + 0, + 168, + 0 + ] + } + } + }, + { + "new": [ + 256, + 133, + 68, + 40, + 25, + 3 + ], + "old": [ + 256, + 133, + 93, + 40 + ], + "rank": 2, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 6, + 3, + 9, + 17, + 33, + 64, + 1, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 2, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 2, + "right": { + "linear_Z4": [ + 1, + 3, + 1, + 1, + 0, + 0, + 2, + 0, + 0 + ], + "matrix_rows": [ + 14, + 81, + 83, + 68, + 88, + 64, + 32, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 3, + 95, + 78, + 94, + 10, + 0, + 14, + 0, + 0 + ] + } + } + } + ], + "schema_version": 1, + "scope": "Native recipes for the transport edges used by repairs R0 and R1 that are absent from the published p104-native-channel recipe set. Lowered with the pinned compile.py / vendor/clifford_exact.py; checked by the published check_native.validate() during replay." +} diff --git a/research/p104-flag43-head-step-repair/SOURCES.json b/research/p104-flag43-head-step-repair/SOURCES.json new file mode 100644 index 0000000000..4389ff657e --- /dev/null +++ b/research/p104-flag43-head-step-repair/SOURCES.json @@ -0,0 +1,81 @@ +{ + "schema_version": 1, + "base_commit": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "upstream": "CrocSwap/integer-mult-bounds", + "files": [ + { + "path": "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "usage": "input", + "git_blob": "86beaf424e9f0f800ae3a62797d94ec9386b7706", + "sha256": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e", + "credit": "Reviewed #1991 native channel witness (PR1972 word)" + }, + { + "path": "research/p104-native-channel/inputs/P104-FIXTURE.json", + "usage": "input", + "git_blob": "2e16f99b295bb386fd13bd8fbd57b42ef54143a9", + "sha256": "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4", + "credit": "P104 fixture used by the published native checker" + }, + { + "path": "research/p104-native-channel/NATIVE-RECIPES.json.gz", + "usage": "input", + "git_blob": "ab129678c2df4f0d39b02b88457d02c37de0d9b6", + "sha256": "a1c4d83d3d5fe1338e99b59272e8cf5d43244c33888597da340b2aa7fef5b3e8", + "credit": "Published native recipes (Chafik Boukhalfa, PR1991)" + }, + { + "path": "research/p104-native-channel/check_native.py", + "usage": "input", + "git_blob": "f8e54afbf146cd6f250063bcb1b9dabf0cbc42ea", + "sha256": "e67b874a061a4a28007b9a0fabaf30c8db4a587b1e1c7dd9396c77ff1e3a9fe6", + "credit": "Published native checker; its validate() is run unchanged on each repaired word" + }, + { + "path": "research/p104-native-channel/vendor/native_verify.py", + "usage": "input", + "git_blob": "2c209dfa9cfade3bc20ac5fc9d876b433a147f8c", + "sha256": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38", + "credit": "Independent native interpreter used by check_native.py and by independent.py" + }, + { + "path": "research/p104-joint-unit-flags/CERTIFICATE.json", + "usage": "input", + "git_blob": "0fa7d2d40566e92f3ea1539723abf438ba65adb8", + "sha256": "a98126428a8da6eae91c50afcc42e014a284c82b554ef77e5b3a34fc6d228128", + "credit": "Nick Petalas, PR #2981 flag matching (flag 43 identity)" + }, + { + "path": "research/p104-native-channel/compile.py", + "usage": "provenance", + "git_blob": "840d7608d6795d12ba174620279f88d8a6f727b4", + "sha256": "9d2fc2d81962ddb0b4dd7d6482d9918a87a6b05759690317dea79939ca5656a3", + "pin": "base_commit:research/p104-native-channel/compile.py", + "credit": "Native compiler used by build.py to lower the new edges" + }, + { + "path": "research/p104-native-channel/vendor/clifford_exact.py", + "usage": "provenance", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "pin": "base_commit:research/p104-native-channel/vendor/clifford_exact.py", + "credit": "Exact Clifford lowering used by build.py" + }, + { + "path": "research/p104-native-channel/PROOF.md", + "usage": "provenance", + "git_blob": "a69311b74f74a2f8e8f411c1451baacd9bacddce", + "sha256": "5d743145d389ffdfaffc66096fa7e32c7155b18f73d74755403151d0435bb94c", + "pin": "base_commit:research/p104-native-channel/PROOF.md", + "credit": "Binary-frame semantics: nested transports, adds only in a common chart, paid rank per transport" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0", + "pin": "base_commit:docs/research/agent-task-catalog.json", + "credit": "Priority revision 6 task catalogue at the pinned base" + } + ] +} diff --git a/research/p104-flag43-head-step-repair/TASK.json b/research/p104-flag43-head-step-repair/TASK.json new file mode 100644 index 0000000000..2d6f96085b --- /dev/null +++ b/research/p104-flag43-head-step-repair/TASK.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 6, + "selected_kappa": "0.001672660197076918", + "base_commit": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "original_card": { + "id": "p104-side-correction", + "question": "Can the proposed P104 joint endpoint flags be realized by a chronological correction program with coefficients, dirty restoration and an affordable complete bill?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/p104-native-channel/README.md", + "research/p104-native-channel/PROOF.md", + "docs/research/community-efficient1000-review.md", + "research/p104-joint-unit-flags/README.md" + ], + "methods": [ + "Construct one side-correction word at an explicit chronological cut with the needed frames still available.", + "Derive a lower bound on the side correction and hosting costs that decides whether this channel can beat the selected budget." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the revision-6 family record and #2981 static joint flags, alongside the reviewed #1991 channel. #2981 is an author-checked source archive, not an independently validated executable correction or a refutation of program-level lifetime floors.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "After checking live handoffs, pin one named collection from #2981 and attach acquisition/delivery times, source dependencies and coefficient requirements. Test legal access and arbitrary dirty restoration; price any completion against the full channel/endpoint/hosting allowance. Stop with the exact missing implication or a scoped counterexample rather than expanding the static cover census.", + "bottleneck_link": "Completing an already realized changed channel tests a concrete construction opportunity, instead of refining the incumbent packing. A positive local result still needs global and all-size admission.", + "allowed_variations": [ + "One correction factorization, one chronological cut, or one explicit hosting obstruction.", + "A changed correction schedule with an updated full bill and native frame contract." + ], + "scope_change_triggers": [ + "Recompiling the already certified low-rank channel without closing a new obligation.", + "Treating a pending ancestor, local histogram or unpriced side correction as an admitted global supplier.", + "Repeating a correction or physical conversion already supplied by a pending follow-up without adding independent coverage or a different unresolved obligation.", + "Repeating the 208-flag static matching or calling a static nested cover a chronological correction program. Independent audit of that certificate is distinct and remains useful." + ], + "overlap_terms": [ + "P104", + "I-G/2", + "side correction", + "native channel", + "1972", + "1991", + "2586", + "endpoint transport", + "physical dual", + "relay composition", + "2981", + "joint unit flags", + "acquisition delivery", + "static nesting" + ], + "existing_checks": [ + { + "scope": "PR #2981 reports static joint endpoint flags and a matching of 208 departure and arrival flags; archival intake is not independent verification.", + "evidence": "research/p104-joint-unit-flags/README.md", + "remaining": "Independent flag check and a chronological coefficient program with dirty restoration and a complete cost.", + "status": "author-checked", + "source_commit": "3d24b92d8ba057b57cb2d480170ec407520e6882", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Price a changed schedule that co-hosts present-head flag 43's basis head (15) in the target Y59 at a target update while the source X21 still hosts it and is still live, answering open question 1 of #3456 (and the matching question of #3451/#3443 for this flag). Construct the repair as an explicit splice of the published #1991 word, run the published p104-native-channel validate() on the repaired word with eight newly lowered native edges, and give the exact before/after bill (events, ADDs, transport occurrences, rank mass, paid H_r profile, native edges). Add the matching obstruction: in the class that keeps the published event order and ADDs, keeps endpoint frames and adds no rank mass, event 3364 is the only Y59 update that can be made head-hosting, and it forces exactly Y59, D17, Y103 and D28 to change.", + "scope_change_reason": "#3451, #3456 and #3443 prove the published word never co-hosts the basis head at a target update on flags 1, 43 and 9, and leave pricing a repair open. This package does not re-derive those chronologies; it cites them and adds the repair, its native validation, its bill and a forced-closure obstruction for flag 43. Flag 43 was chosen because #3456 records that its last target chart is one rank step from the head and names the D17 common-chart constraint.", + "bottleneck_link": "The present-head obstruction on flag 43 is a scheduling artefact, not a cost barrier: the head can be co-hosted at the target update that settles X21's final coefficient without adding any event, ADD, transport or rank unit to the published channel. The remaining cost is a rank-profile reshuffle that is free under any affine per-rank price and weakly favourable under any convex one. This does not supply I-G/2, a side correction or a supplier.", + "budget_minutes": 60, + "stop_rule": "Stop after one flag (43): one event-preserving repair R0 and one order-changing comparison R1, both natively validated and billed, plus the forced-hosting closure of every Y59 update. Do not touch flags 0, 1 or 9, recompute relay coefficients beyond the X21 entries of Y59, or build a side correction.", + "outcome": "completed", + "evidence": "R0 retargets nine published transports (3362, 3363, 3365, 3460, 3461, 3525, 3569, 3612, 3634) and relabels three ADD charts (3364, 3366, 3462); every changed frame is its published frame plus 15. The published check_native.validate() passes on the repaired word: 740 native edges (8 swapped for 8 newly lowered), 208 endpoint adapters, all 280 framed rows and 72 dirty helpers restored. Bill: 4058 events, 2624 ADDs, 1410 transport occurrences and rank mass 2368, all unchanged; paid profile {1:1074,2:58,3:86,4:104} becomes {1:1071,2:63,3:85,4:103}, delta -3H1+5H2-H3-H4; the nine changed ranks {4,3,3,2,1,1,1,1,1} become {3,2,2,2,2,2,2,1,1}, which the published multiset majorizes. In R0 the last Y59 update (3364, D17, coefficient 1/4) runs in chart [95,447,6,32,20,15] while X21 is at the rank-9 full chart with four later reads; that ADD carries X21 coefficient 1/2 and settles Y59's final X21 coefficient 1/2 (after +1/2 at 3076 and -1/2 at 3231). R1 instead moves Y103's 3365-3366 before Y59's update and gives D17 one added rank-1 transport: +1 event, +1 transport occurrence, rank mass unchanged, delta +2H2-H4, 742 native edges. Forced closure on the published word: 14 of 15 Y59 updates force the head into a register whose final frame excludes it (first: Y67, Y96, Y26, Y56 or Y22); only 3364 is admissible, forcing D17 at 3364, Y103 at 3366 and D28 at 3462. All 280 non-private registers sit at their rank floor, so zero added rank mass means monotone paths. Selected kappa unchanged.", + "author": "Wentao Li", + "ai_assistance": "Substantial AI assistance for derivation, implementation, checking and writing.", + "no_new_kappa": true, + "open_questions": [ + { + "question": "Does the same head-step repair exist for present-head flags 1 and 9, and what is the forced closure of their target updates?", + "why_it_matters": "If every present-head flag admits an event-preserving repair, the present-head obstruction recorded by #3451/#3443/#3456 is uniformly a scheduling artefact; a flag whose closure is obstructed would instead need added rank or a reordering, with a priced floor.", + "first_step": "Run this package's closure_table on Y7 (flag 1, head 232) and Y23 (flag 9, head 196) as a separate package citing #3451 and #3443, without re-certifying their chronologies.", + "blocked_by": "This package treats flag 43 only. Flags 1 and 9 are the subjects of open #3451 and #3443." + }, + { + "question": "Can a correction program use the co-hosted head chart at 3364 to restore X21's contribution to Y59 dirtily, and what does the I-G/2 side correction then cost at that cut?", + "why_it_matters": "R0 removes the geometric reason given by #3456 for why chronological dirty restoration cannot use co-hosted head geometry on flag 43. Whether the side correction can exploit it is the actual supplier question.", + "first_step": "At R0's event 3364, price one added X21-to-Y59 transfer in the common head chart (both registers would need a shared frame; X21 is at the full chart) against the channel's existing allowance.", + "blocked_by": "No side-correction word is built here; the channel still implements G/2, not I." + }, + { + "question": "Is R0's rank profile optimal among event-preserving monotone repairs under every convex per-rank price?", + "why_it_matters": "R0 uses the minimal admissible frame at each forced event, but a different choice of intermediate frames could give a profile that the R0 profile does not majorize.", + "first_step": "Enumerate the admissible frames for the nine forced transports inside each register's final span and compare the resulting rank multisets by majorization.", + "blocked_by": "Not enumerated in this package." + } + ] +} diff --git a/research/p104-flag43-head-step-repair/VERIFY.json b/research/p104-flag43-head-step-repair/VERIFY.json new file mode 100644 index 0000000000..f0e005040e --- /dev/null +++ b/research/p104-flag43-head-step-repair/VERIFY.json @@ -0,0 +1,52 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "research/p104-native-channel/inputs/P104-FIXTURE.json", + "research/p104-native-channel/NATIVE-RECIPES.json.gz", + "research/p104-native-channel/check_native.py", + "research/p104-native-channel/vendor/native_verify.py", + "research/p104-joint-unit-flags/CERTIFICATE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Applies repairs R0 and R1 to the published witness in memory, runs the published check_native.validate() on each (every native edge incl. 9 committed new-edge recipes, 208 endpoint adapters, all 280 framed rows and dirty-helper restorations), recomputes the bill, head co-hosting, X21 delivery into Y59 and the forced-hosting closure of all 15 Y59 updates, and requires equality with CERTIFICATE.json" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Separately written replay with XOR-closure frames and exact rational rows: common-chart ADDs, nested transports with paid rank equal to frame gap, 280/280 final rows equal to the published rows, bill and profile delta, majorization, head co-hosting and delivery, forward-sweep forced closure, direct native check of each new recipe" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 600, + "checks": "Temp-tree clean pass with byte-identical tree; 14 rejections by both scanners under -O: certificate field corruptions, duplicate JSON key, witness byte flip, new-recipe phase corruption, three truncated cascades rejected at the common-chart rule, and an undercharged transport" + } + ] +} diff --git a/research/p104-flag43-head-step-repair/build.py b/research/p104-flag43-head-step-repair/build.py new file mode 100644 index 0000000000..bad14e78ab --- /dev/null +++ b/research/p104-flag43-head-step-repair/build.py @@ -0,0 +1,125 @@ +#!/usr/bin/env python3 +"""Producer for CERTIFICATE.json and REPAIR-RECIPES.json (not part of replay). + +Defines the two changed schedules as splices of the published witness, +lowers each transport edge absent from the published recipe set with the +pinned native compiler, and writes the receipt computed by verify.py. +Refuses to overwrite existing outputs unless --force is given. +""" + +import argparse +import hashlib +import importlib.util +import json +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import verify as V # noqa: E402 + +COMPILER_SHA256 = "9d2fc2d81962ddb0b4dd7d6482d9918a87a6b05759690317dea79939ca5656a3" +CLIFFORD_SHA256 = "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + +W4 = [95, 447, 6, 32] +W4P = [95, 447, 32, 20] +W5 = [95, 447, 6, 32, 20] +W6 = W5 + [15] +V5 = [95, 447, 6, 32, 192] +V6 = [95, 447, 6, 32, 20, 192] +W7 = V6 + [15] +FULL = [1, 2, 4, 8, 16, 32, 64, 128, 256] + + +def splices(program, final): + def one(i, event): + return {"published_range": [i, i + 1], "published": [program[i]], "events": [event]} + r0 = [ + one(3362, ["transport", "D17", W4, W6, 2]), + one(3363, ["transport", "Y59", W4P, W6, 2]), + one(3364, ["add", "Y59", "D17", "1/4", W6]), + one(3365, ["transport", "Y103", W4P, W6, 2]), + one(3366, ["add", "Y103", "D17", "1/4", W6]), + one(3460, ["transport", "D28", V5, W7, 2]), + one(3461, ["transport", "Y103", W6, W7, 1]), + one(3462, ["add", "Y103", "D28", "1/4", W7]), + one(3525, ["transport", "Y59", W6, final["Y59"], 2]), + one(3569, ["transport", "Y103", W7, final["Y103"], 1]), + one(3612, ["transport", "D17", W6, FULL, 3]), + one(3634, ["transport", "D28", W7, FULL, 2]), + ] + r1 = [ + {"published_range": [3363, 3367], "published": program[3363:3367], + "events": [program[3365], program[3366], + ["transport", "D17", W5, W6, 1], + ["transport", "Y59", W4P, W6, 2], + ["add", "Y59", "D17", "1/4", W6]]}, + one(3525, ["transport", "Y59", W6, final["Y59"], 2]), + one(3612, ["transport", "D17", W6, FULL, 3]), + ] + return { + "R0": { + "class": "event-preserving retarget: same events in the same order, same ADD registers and coefficients, only transport frames and ranks and the matching ADD chart fields change", + "rule": "from the forced event on, each changed register's frame is its published frame plus the basis head, until a frame that already spans the head", + "splices": r0, + }, + "R1": { + "class": "two-register comparison: Y103's transport and update at 3365-3366 move before Y59's, and D17 gets one added rank-1 transport", + "rule": "D17 serves Y103 in the published rank-5 chart, then lifts to the rank-6 head chart for Y59", + "splices": r1, + }, + } + + +def load(name, path, digest): + raw = path.read_bytes() + V.need(hashlib.sha256(raw).hexdigest() == digest, "pinned compiler module: " + str(path)) + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--force", action="store_true") + args = ap.parse_args() + for name in ("CERTIFICATE.json", "REPAIR-RECIPES.json"): + V.need(args.force or not (HERE / name).exists(), name + " exists") + root = V.ROOT + load("flag43_clifford_pin", root / V.NATIVE / "vendor/clifford_exact.py", CLIFFORD_SHA256) + co = load("flag43_native_compile", root / V.NATIVE / "compile.py", COMPILER_SHA256) + witness, _fixture, recipes, _flags = V.load_inputs(root) + cert = {"repairs": splices(witness["program"], witness["final_frames"])} + physical = V.physical_map(recipes) + pub = {(tuple(r["old"]), tuple(r["new"])) for r in recipes["transports"]} + new = {} + for name in ("R0", "R1"): + prog = V.apply_splices(witness["program"], cert["repairs"][name]["splices"]) + for e in prog: + if e[0] != "transport": + continue + key = (physical(e[2]), physical(e[3])) + if key in pub or key in new: + continue + actual = co.CE.canonical_frame(9, key[0]).adjoint().then(co.CE.canonical_frame(9, key[1])) + record, _ = co.CE.lower_child(actual) + V.need(record["rank"] == e[4], "native rank equals frame gap") + new[key] = {"old": list(key[0]), "new": list(key[1]), "rank": e[4], "recipe": record} + recs = [new[k] for k in sorted(new)] + payload = { + "schema_version": 1, + "scope": "Native recipes for the transport edges used by repairs R0 and R1 that are absent from the published p104-native-channel recipe set. Lowered with the pinned compile.py / vendor/clifford_exact.py; checked by the published check_native.validate() during replay.", + "compiler_sha256": COMPILER_SHA256, + "clifford_exact_sha256": CLIFFORD_SHA256, + "recipes": recs, + } + got = V.receipt(root, cert, recs) + (HERE / "REPAIR-RECIPES.json").write_text(json.dumps(payload, indent=1, sort_keys=True) + "\n") + (HERE / "CERTIFICATE.json").write_text(json.dumps(got, indent=2, sort_keys=True) + "\n") + print("WROTE", len(recs), "new recipes") + + +if __name__ == "__main__": + main() diff --git a/research/p104-flag43-head-step-repair/independent.py b/research/p104-flag43-head-step-repair/independent.py new file mode 100644 index 0000000000..75d219fcfd --- /dev/null +++ b/research/p104-flag43-head-step-repair/independent.py @@ -0,0 +1,305 @@ +#!/usr/bin/env python3 +"""Second, separately written scanner for the flag-43 head-step repair bill. + +Does not import verify.py, check_native.py or the compiler. Frames are explicit +XOR-closure sets; the repaired words are replayed with exact rational rows and +compared register by register with the published word's final rows and frames. +The forced-hosting closure is recomputed by a single forward sweep. The new +native recipes are checked directly with the vendored independent interpreter. +Admission uses need() and stays active under python -O. +""" + +import gzip +import hashlib +import importlib.util +import json +import sys +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +NATIVE = "research/p104-native-channel" +PINS = { + f"{NATIVE}/inputs/LOWRANK-WITNESS.json": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e", + f"{NATIVE}/NATIVE-RECIPES.json.gz": "a1c4d83d3d5fe1338e99b59272e8cf5d43244c33888597da340b2aa7fef5b3e8", + f"{NATIVE}/vendor/native_verify.py": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38", + "research/p104-joint-unit-flags/CERTIFICATE.json": "a98126428a8da6eae91c50afcc42e014a284c82b554ef77e5b3a34fc6d228128", +} +MARKER = ( + "PASS_P104_FLAG43_HEAD_STEP_REPAIR_INDEPENDENT flag=43 head=15 repaired_update=3364 " + "added_events=0 added_adds=0 added_transports=0 added_rank_mass=0 " + "retargeted_transports=9 forced_registers=4 profile_delta=-3H1+5H2-H3-H4 " + "rows_equal=280/280 earlier_updates_obstructed=14/14 no_new_kappa" +) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def strict(pairs): + seen = {} + for k, v in pairs: + need(k not in seen, "duplicate JSON key: " + str(k)) + seen[k] = v + return seen + + +def read(root, rel, gz=False): + raw = (root / rel).read_bytes() + need(hashlib.sha256(raw).hexdigest() == PINS[rel], "source hash: " + rel) + return json.loads(gzip.decompress(raw) if gz else raw, object_pairs_hook=strict) + + +def closure(vectors): + out = frozenset([0]) + for v in vectors: + out = out | frozenset(x ^ v for x in out) + return out + + +def dim(s): + n = len(s) + need(n & (n - 1) == 0, "closure size is a power of two") + return n.bit_length() - 1 + + +def splice(program, rows): + out = list(program) + edits = sorted(((r["published_range"][0], r["published_range"][1], r) for r in rows), reverse=True) + prev = len(program) + for a, b, r in edits: + need(b <= prev and a < b, "disjoint splices") + need(program[a:b] == r["published"], "splice binding at %d" % a) + out[a:b] = [list(e) for e in r["events"]] + prev = a + return out + + +def replay(witness, program): + rows = {n: {n: Fraction(1)} for n in witness["initial_frames"]} + frames = {n: closure(f) for n, f in witness["initial_frames"].items()} + profile = {} + adds = 0 + for i, e in enumerate(program): + op = e[0] + if op == "transport": + _, r, old, new, k = e + a, b = closure(old), closure(new) + need(frames[r] == a, "transport before-frame continuity at %d" % i) + need(a <= b or b <= a, "nested transport at %d" % i) + need(k == abs(dim(b) - dim(a)) and k > 0, "paid rank equals frame gap at %d" % i) + need(len(new) == dim(b) and len(old) == dim(a), "independent frame lists at %d" % i) + frames[r] = b + profile[k] = profile.get(k, 0) + 1 + elif op == "zero": + need(e[1] not in frames, "fresh private") + rows[e[1]] = {} + frames[e[1]] = closure(e[2]) + elif op == "erase": + need(frames[e[1]] == closure(e[2]), "erase chart") + rows.pop(e[1]) + frames.pop(e[1]) + elif op == "copy": + need(not rows[e[1]] and frames[e[1]] == frames[e[2]] == closure(e[3]), "copy chart") + rows[e[1]] = dict(rows[e[2]]) + else: + need(op == "add", "opcode") + _, d, s, c, f = e + need(d != s and frames[d] == frames[s] == closure(f), "common chart at %d" % i) + adds += 1 + for n, v in rows[s].items(): + z = rows[d].get(n, Fraction(0)) + Fraction(c) * v + if z: + rows[d][n] = z + else: + rows[d].pop(n, None) + for n, f in witness["final_frames"].items(): + need(frames[n] == closure(f), "final frame " + n) + return rows, frames, profile, adds + + +def frames_over_time(witness, program, reg): + out = [(-1, closure(witness["initial_frames"][reg]))] + for i, e in enumerate(program): + if e[0] == "transport" and e[1] == reg: + out.append((i, closure(e[3]))) + return out + + +def frame_before(seq, t): + cur = seq[0][1] + for i, f in seq: + if i < t: + cur = f + return cur + + +def sweep(witness, program, target, start, head): + hosting = {target: start} + for j in range(start, len(program)): + e = program[j] + if e[0] not in ("add", "copy"): + continue + a, b = e[1], e[2] + if a in hosting or b in hosting: + for r in (a, b): + hosting.setdefault(r, j) + seqs = {} + change = {} + for r, t in hosting.items(): + if r == "C": + frames = [f for i, f in private_frames(program) if i < t] + if not frames or head not in frames[-1]: + change[r] = t + continue + seqs[r] = frames_over_time(witness, program, r) + if head not in frame_before(seqs[r], t): + change[r] = t + return change, seqs + + +def private_frames(program): + out = [] + for i, e in enumerate(program): + if e[1:2] == ["C"]: + if e[0] == "zero": + out.append((i, closure(e[2]))) + elif e[0] == "transport": + out.append((i, closure(e[3]))) + return out + + +def main(root=ROOT): + cert = json.loads((HERE / "CERTIFICATE.json").read_bytes(), object_pairs_hook=strict) + recipes_new = json.loads((HERE / "REPAIR-RECIPES.json").read_bytes(), object_pairs_hook=strict)["recipes"] + witness = read(root, f"{NATIVE}/inputs/LOWRANK-WITNESS.json") + published_recipes = read(root, f"{NATIVE}/NATIVE-RECIPES.json.gz", gz=True) + flags = read(root, "research/p104-joint-unit-flags/CERTIFICATE.json") + raw = (root / NATIVE / "vendor/native_verify.py").read_bytes() + need(hashlib.sha256(raw).hexdigest() == PINS[f"{NATIVE}/vendor/native_verify.py"], "native interpreter pin") + spec = importlib.util.spec_from_file_location("flag43_independent_native", root / NATIVE / "vendor/native_verify.py") + N = importlib.util.module_from_spec(spec) + spec.loader.exec_module(N) + + h = flags["helpers"][43] + head, src, tgt = h["basis"][0], "X%d" % h["source"], "Y%d" % h["target"] + need((head, src, tgt) == (15, "X21", "Y59"), "flag 43") + need(cert["basis_head"] == head and cert["source_register"] == src and cert["target_register"] == tgt, "certificate flag") + P = witness["program"] + base_rows, _, base_profile, base_adds = replay(witness, P) + bill = cert["bill"] + need(sum(base_profile.values()) == bill["published"]["transport_occurrences"] == 1410, "published transports") + need(sum(k * v for k, v in base_profile.items()) == bill["published"]["rank_mass"] == 2368, "published rank mass") + need(base_adds == bill["published"]["scalar_adds"] == 2624, "published adds") + + # Physical canonical images of the repaired frames, for the native recipe check. + iso = published_recipes["label_isometry"] + dual, orth = iso["compressed_dual_gram"], iso["orthonormal_basis_compressed"] + + def to_phys(x): + bx = sum(((((row & x).bit_count()) & 1) << i) for i, row in enumerate(dual)) + return sum((((v & bx).bit_count()) & 1) << j for j, v in enumerate(orth)) + + pub_edges = {(closure(r["old"]), closure(r["new"])) for r in published_recipes["transports"]} + new_edges = {} + for rec in recipes_new: + key = (closure(rec["old"]), closure(rec["new"])) + need(key not in pub_edges and key not in new_edges, "new edge is new and unique") + need(rec["rank"] == rec["recipe"]["rank"] == abs(dim(key[1]) - dim(key[0])), "new recipe rank") + N.equal(N.recipe(rec["recipe"]), N.adjoint(N.frame(tuple(rec["old"]), 9)) + N.frame(tuple(rec["new"]), 9), "new native edge") + new_edges[key] = rec + + used = set() + out = {} + for name in ("R0", "R1"): + prog = splice(P, cert["repairs"][name]["splices"]) + rows, _, profile, adds = replay(witness, prog) + same = sum(1 for n in base_rows if rows[n] == base_rows[n]) + need(same == len(base_rows) == 280, "every final row equals the published row") + for e in prog: + if e[0] == "transport": + key = (closure(to_phys(x) for x in e[2]), closure(to_phys(x) for x in e[3])) + if key not in pub_edges: + need(key in new_edges, "repaired edge has a committed recipe") + used.add(key) + b = bill[name] + need(b["events"] == len(prog) and b["scalar_adds"] == adds, name + " counts") + need(b["transport_occurrences"] == sum(profile.values()), name + " transports") + need(b["rank_mass"] == sum(k * v for k, v in profile.items()), name + " rank mass") + need(b["paid_profile"] == {str(k): v for k, v in sorted(profile.items())}, name + " profile") + delta = {str(k): profile.get(k, 0) - base_profile.get(k, 0) for k in sorted(set(profile) | set(base_profile)) if profile.get(k, 0) != base_profile.get(k, 0)} + need(b["profile_delta"] == delta, name + " delta") + out[name] = (prog, b) + need(used == set(new_edges), "every committed recipe used") + + prog0, b0 = out["R0"] + need((b0["added_events"], b0["added_scalar_adds"], b0["added_transport_occurrences"], b0["added_rank_mass"]) == (0, 0, 0, 0), "R0 adds nothing counted") + need(b0["profile_delta"] == {"1": -3, "2": 5, "3": -1, "4": -1}, "R0 delta") + moved = [i for i in range(len(P)) if P[i] != prog0[i] and P[i][0] == "transport"] + need(moved == b0["retargeted_transports"] and len(moved) == 9, "nine retargeted transports") + old_r = sorted((P[i][4] for i in moved), reverse=True) + new_r = sorted((prog0[i][4] for i in moved), reverse=True) + need(sum(old_r) == sum(new_r) and all(sum(new_r[:k]) <= sum(old_r[:k]) for k in range(1, 10)), "majorization") + need(sorted({P[i][1] for i in moved}) == b0["registers_changed"] == ["D17", "D28", "Y103", "Y59"], "changed registers") + need((b["added_events"], b["added_transport_occurrences"], b["added_rank_mass"]) == (1, 1, 0) and b["profile_delta"] == {"2": 2, "4": -1}, "R1 bill") + + hc = cert["head_cohosting"] + tseq, sseq = frames_over_time(witness, prog0, tgt), frames_over_time(witness, prog0, src) + pseq = frames_over_time(witness, P, tgt) + upd = [i for i, e in enumerate(prog0) if e[0] == "add" and e[1] == tgt] + need([i for i in upd if head in frame_before(pseq, i)] == hc["published_head_hosting_target_updates"] == [], "published head-free updates") + co = [i for i in upd if head in frame_before(tseq, i) and head in frame_before(sseq, i)] + need(co == hc["R0_cohosted_target_updates"] == [3364] and upd[-1] == 3364, "R0 co-hosted last update") + need(closure(prog0[3364][4]) == closure([95, 447, 6, 32, 20, 15]) and prog0[3364][2] == "D17", "R0 update chart") + need(dim(frame_before(sseq, 3364)) == 9 and [i for i, e in enumerate(prog0) if i > 3364 and src in e[1:3]] == [3705, 3760, 3811, 3863], "source live and full") + coef = Fraction(0) + carried = [] + rows = {n: {n: Fraction(1)} for n in witness["initial_frames"]} + for i, e in enumerate(prog0): + if e[0] == "zero": + rows[e[1]] = {} + elif e[0] == "erase": + rows.pop(e[1]) + elif e[0] == "copy": + rows[e[1]] = dict(rows[e[2]]) + elif e[0] == "add": + if e[1] == tgt and rows[e[2]].get(src): + coef += Fraction(e[3]) * rows[e[2]][src] + carried.append([i, e[2], str(Fraction(e[3]) * rows[e[2]][src]), str(coef)]) + for n, v in rows[e[2]].items(): + z = rows[e[1]].get(n, Fraction(0)) + Fraction(e[3]) * v + if z: + rows[e[1]][n] = z + else: + rows[e[1]].pop(n, None) + need(carried == hc["R0_source_delivery_into_target"] and carried[-1] == [3364, "D17", "1/2", "1/2"], "delivery chronology") + + finals = {n: closure(f) for n, f in witness["final_frames"].items()} + table = {row["event"]: row for row in cert["forced_hosting"]["table"]} + need(sorted(table) == [i for i, e in enumerate(P) if e[0] == "add" and e[1] == tgt], "every target update tabulated") + obstructed = 0 + for t0, row in table.items(): + change, seqs = sweep(witness, P, tgt, t0, head) + hard = sorted([[r, t] for r, t in change.items() if r != "C" and r in finals and head not in finals[r]], key=lambda x: (x[1], x[0])) + private = sorted([[r, t] for r, t in change.items() if r == "C"], key=lambda x: (x[1], x[0])) + slot = [r for r, t in change.items() if r != "C" and not any(-1 < i < t for i, _ in seqs[r]) and [r, t] not in hard and head not in seqs[r][0][1]] + need(row["must_change"] == len(change), "must-change count at %d" % t0) + need(row["slot_independent_obstructions"] == len(hard), "obstruction count at %d" % t0) + need(row["first_obstruction"] == (hard[0] + ["final frame excludes head"] if hard else None), "first obstruction at %d" % t0) + need(row["private_registers_forced"] == private, "private forcing at %d" % t0) + need(row["registers_without_prior_transport"] == len(slot), "slot count at %d" % t0) + need(row["admissible"] == (not hard and not slot and not private), "admissible at %d" % t0) + if hard: + obstructed += 1 + else: + need(row["forced"] == change, "forced set at %d" % t0) + need(obstructed == 14 and table[3364]["forced"] == {"Y59": 3364, "D17": 3364, "Y103": 3366, "D28": 3462}, "closure verdict") + need(cert["selected_kappa"] == "0.001672660197076918" and cert["no_new_kappa"] is True, "kappa") + print(MARKER) + + +if __name__ == "__main__": + main(Path(sys.argv[1]).resolve() if len(sys.argv) > 1 else ROOT) diff --git a/research/p104-flag43-head-step-repair/test_package.py b/research/p104-flag43-head-step-repair/test_package.py new file mode 100644 index 0000000000..935e39776c --- /dev/null +++ b/research/p104-flag43-head-step-repair/test_package.py @@ -0,0 +1,155 @@ +#!/usr/bin/env python3 +"""Behavioural tests: corruption, negative controls and read-only replay. + +Each case copies the package and its pinned inputs into a temporary tree, +mutates one thing and runs both scanners there under python -O. The scanners +must reject every mutation; the clean tree must pass and stay byte-identical. +""" + +import concurrent.futures +import hashlib +import json +import shutil +import subprocess +import sys +import tempfile +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PKG = HERE.relative_to(ROOT).as_posix() +NATIVE = "research/p104-native-channel" +COPY = [ + f"{NATIVE}/inputs/LOWRANK-WITNESS.json", + f"{NATIVE}/inputs/P104-FIXTURE.json", + f"{NATIVE}/NATIVE-RECIPES.json.gz", + f"{NATIVE}/check_native.py", + f"{NATIVE}/vendor/native_verify.py", + "research/p104-joint-unit-flags/CERTIFICATE.json", +] +SCANNERS = ("verify.py", "independent.py") + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def tree(base): + for rel in COPY: + (base / rel).parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / rel, base / rel) + shutil.copytree(HERE, base / PKG, ignore=shutil.ignore_patterns("__pycache__")) + return base + + +def run(base, scanner): + p = subprocess.run([sys.executable, "-I", "-O", "-Werror", "-B", str(base / PKG / scanner), str(base)], + capture_output=True, text=True, timeout=600) + return p.returncode, p.stdout + p.stderr + + +def digest(base): + return {p.relative_to(base).as_posix(): hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(base.rglob("*")) if p.is_file()} + + +def edit_json(path, fn): + data = json.loads(path.read_text()) + fn(data) + path.write_text(json.dumps(data, indent=2, sort_keys=True) + "\n") + + +def drop_splices(events): + def fn(c): + rows = c["repairs"]["R0"]["splices"] + c["repairs"]["R0"]["splices"] = [r for r in rows if r["published_range"][0] not in events] + return fn + + +def set_rank(event, value): + def fn(c): + for r in c["repairs"]["R0"]["splices"]: + if r["published_range"][0] == event: + r["events"][0][4] = value + return fn + + +def cert_field(fn): + return lambda base: edit_json(base / PKG / "CERTIFICATE.json", fn) + + +def dup_key(base): + p = base / PKG / "CERTIFICATE.json" + text = p.read_text() + p.write_text(text.replace('"basis_head": 15,', '"basis_head": 15,\n "basis_head": 15,', 1)) + + +def flip_witness(base): + p = base / f"{NATIVE}/inputs/LOWRANK-WITNESS.json" + raw = bytearray(p.read_bytes()) + k = raw.index(b"3525") if b"3525" in raw else len(raw) // 2 + raw[k] ^= 1 + p.write_bytes(bytes(raw)) + + +def bad_phase(base): + p = base / PKG / "REPAIR-RECIPES.json" + data = json.loads(p.read_text()) + left = data["recipes"][0]["recipe"]["left"] + left["phase"] = (left["phase"] + 1) % 4 + p.write_text(json.dumps(data, indent=1, sort_keys=True) + "\n") + + +CASES = { + "bill_rank_mass": (cert_field(lambda c: c["bill"]["R0"].__setitem__("rank_mass", 2369)), None), + "bill_profile_delta": (cert_field(lambda c: c["bill"]["R0"]["profile_delta"].__setitem__("2", 4)), None), + "cohosted_updates": (cert_field(lambda c: c["head_cohosting"].__setitem__("R0_cohosted_target_updates", [])), None), + "delivery": (cert_field(lambda c: c["head_cohosting"]["R0_source_delivery_into_target"][-1].__setitem__(2, "1/4")), None), + "admissible_3231": (cert_field(lambda c: [r.__setitem__("admissible", True) for r in c["forced_hosting"]["table"] if r["event"] == 3231]), None), + "forced_set": (cert_field(lambda c: [r["forced"].pop("D28") for r in c["forced_hosting"]["table"] if r["event"] == 3364]), None), + "kappa": (cert_field(lambda c: c.__setitem__("selected_kappa", "0.0016726601970769181")), None), + "duplicate_key": (dup_key, "duplicate JSON key"), + "witness_byte": (flip_witness, None), + "recipe_phase": (bad_phase, None), + "control_target_only": (cert_field(drop_splices({3362, 3612, 3365, 3366, 3460, 3461, 3462, 3569, 3634})), "common"), + "control_without_y103": (cert_field(drop_splices({3365, 3366, 3460, 3461, 3462, 3569, 3634})), "common"), + "control_without_d28": (cert_field(drop_splices({3460, 3462, 3634})), "common"), + "control_undercharge": (cert_field(set_rank(3525, 1)), None), +} + + +def case(name): + mutate, expect = CASES[name] + with tempfile.TemporaryDirectory(prefix="flag43-repair-") as d: + base = tree(Path(d)) + mutate(base) + for scanner in SCANNERS: + code, out = run(base, scanner) + need(code != 0, f"{name}: {scanner} accepted a mutation") + need("PASS_" not in out, f"{name}: {scanner} printed a pass marker") + if expect: + need(expect in out, f"{name}: {scanner} rejected for the wrong reason: {out[-300:]}") + return name + + +def clean(): + with tempfile.TemporaryDirectory(prefix="flag43-repair-") as d: + base = tree(Path(d)) + before = digest(base) + for scanner in SCANNERS: + code, out = run(base, scanner) + need(code == 0 and "PASS_P104_FLAG43_HEAD_STEP_REPAIR" in out, f"clean {scanner}: {out[-400:]}") + need(digest(base) == before, "scanners modified the tree") + + +def main(): + clean() + with concurrent.futures.ThreadPoolExecutor(max_workers=4) as pool: + done = list(pool.map(case, sorted(CASES))) + need(len(done) == len(CASES), "all cases ran") + print(f"PASS_P104_FLAG43_HEAD_STEP_REPAIR_TESTS cases={len(CASES)} clean_read_only=1 scanners=2") + + +if __name__ == "__main__": + main() diff --git a/research/p104-flag43-head-step-repair/verify.py b/research/p104-flag43-head-step-repair/verify.py new file mode 100644 index 0000000000..a1cd9408bb --- /dev/null +++ b/research/p104-flag43-head-step-repair/verify.py @@ -0,0 +1,458 @@ +#!/usr/bin/env python3 +"""Read-only replay of the flag-43 head-step repair bill. + +Applies two changed schedules to the published 4,058-event P104 witness in +memory, assembles their native recipe sets from the published recipes plus +the committed new-edge recipes, and runs the published native checker's +complete validate() on each: every native edge, every endpoint adapter, all +280 framed rows and the 72 dirty-helper restorations. It then recomputes the +bill, the head co-hosting facts and the forced-hosting closure of every Y59 +update, and compares the receipt with CERTIFICATE.json. Admission uses need() +and stays active under python -O. Nothing is written. +""" + +import bisect +import copy +import gzip +import hashlib +import importlib.util +import json +import sys +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +NATIVE = "research/p104-native-channel" +PINS = { + f"{NATIVE}/inputs/LOWRANK-WITNESS.json": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e", + f"{NATIVE}/inputs/P104-FIXTURE.json": "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4", + f"{NATIVE}/NATIVE-RECIPES.json.gz": "a1c4d83d3d5fe1338e99b59272e8cf5d43244c33888597da340b2aa7fef5b3e8", + f"{NATIVE}/check_native.py": "e67b874a061a4a28007b9a0fabaf30c8db4a587b1e1c7dd9396c77ff1e3a9fe6", + f"{NATIVE}/vendor/native_verify.py": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38", + "research/p104-joint-unit-flags/CERTIFICATE.json": "a98126428a8da6eae91c50afcc42e014a284c82b554ef77e5b3a34fc6d228128", +} +FLAG_INDEX = 43 +SELECTED_KAPPA = "0.001672660197076918" +MARKER = ( + "PASS_P104_FLAG43_HEAD_STEP_REPAIR flag=43 head=15 repaired_update=3364 " + "added_events=0 added_adds=0 added_transports=0 added_rank_mass=0 " + "retargeted_transports=9 forced_registers=4 profile_delta=-3H1+5H2-H3-H4 " + "native_validate=PASS earlier_updates_obstructed=14/14 no_new_kappa" +) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def pairs_unique(pairs): + out = {} + for key, value in pairs: + need(key not in out, "duplicate JSON key: " + str(key)) + out[key] = value + return out + + +def loads(raw): + return json.loads(raw, object_pairs_hook=pairs_unique) + + +def pinned_bytes(root, rel): + raw = (root / rel).read_bytes() + need(hashlib.sha256(raw).hexdigest() == PINS[rel], "pinned input changed: " + rel) + return raw + + +def load_checker(root): + pinned_bytes(root, f"{NATIVE}/check_native.py") + pinned_bytes(root, f"{NATIVE}/vendor/native_verify.py") + name = "flag43_repair_check_native" + spec = importlib.util.spec_from_file_location(name, root / NATIVE / "check_native.py") + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def load_inputs(root): + witness = loads(pinned_bytes(root, f"{NATIVE}/inputs/LOWRANK-WITNESS.json")) + fixture = loads(pinned_bytes(root, f"{NATIVE}/inputs/P104-FIXTURE.json"))["section4_explicit_P104"] + recipes = loads(gzip.decompress(pinned_bytes(root, f"{NATIVE}/NATIVE-RECIPES.json.gz"))) + flags = loads(pinned_bytes(root, "research/p104-joint-unit-flags/CERTIFICATE.json")) + return witness, fixture, recipes, flags + + +# --- GF(2) frames ----------------------------------------------------------- + +def span(vectors): + out = {0} + for v in vectors: + out |= {x ^ v for x in tuple(out)} + return frozenset(out) + + +def rank(vectors): + piv = {} + for x in vectors: + while x: + j = x.bit_length() - 1 + if j in piv: + x ^= piv[j] + else: + piv[j] = x + break + return len(piv) + + +def canon(values): + piv = {} + for x in values: + while x: + j = x.bit_length() - 1 + if j in piv: + x ^= piv[j] + else: + piv[j] = x + break + for j in sorted(piv): + for k in piv: + if k > j and piv[k] >> j & 1: + piv[k] ^= piv[j] + return tuple(piv[j] for j in sorted(piv, reverse=True)) + + +def physical_map(recipes): + iso = recipes["label_isometry"] + dual = iso["compressed_dual_gram"] + orth = iso["orthonormal_basis_compressed"] + mv = lambda rows, x: sum((((row & x).bit_count()) & 1) << i for i, row in enumerate(rows)) + dot = lambda a, b: (a & mv(dual, b)).bit_count() & 1 + convert = lambda x: sum(dot(x, v) << j for j, v in enumerate(orth)) + return lambda frame: canon(convert(x) for x in frame) + + +# --- schedules --------------------------------------------------------------- + +def apply_splices(program, splices): + out = list(program) + last = len(program) + 1 + for row in sorted(splices, key=lambda r: -r["published_range"][0]): + start, stop = row["published_range"] + need(0 <= start < stop <= len(program) and stop <= last, "ordered disjoint splices") + for k, old in enumerate(row["published"]): + need(program[start + k] == old, "splice binds published event %d" % (start + k)) + need(len(row["published"]) == stop - start, "splice covers its range") + out[start:stop] = copy.deepcopy(row["events"]) + last = start + return out + + +def assemble(recipes, program, new_recipes, physical): + pub = {(tuple(r["old"]), tuple(r["new"])): r for r in recipes["transports"]} + extra = {(tuple(r["old"]), tuple(r["new"])): r for r in new_recipes} + need(len(extra) == len(new_recipes), "unique new-edge recipes") + need(not (set(pub) & set(extra)), "new recipes are new edges") + edges = {} + for i, e in enumerate(program): + if e[0] == "transport": + edges.setdefault((physical(e[2]), physical(e[3])), []).append(i) + used_new = set() + out = [] + for key in sorted(edges): + if key in pub: + rec = dict(pub[key]) + else: + need(key in extra, "missing native recipe for new edge") + rec = dict(extra[key]) + used_new.add(key) + rec["events"] = edges[key] + out.append(rec) + profile = {} + for rec in out: + profile[rec["rank"]] = profile.get(rec["rank"], 0) + len(rec["events"]) + c = dict(recipes) + c["transports"] = out + c["paid_profile"] = {str(k): v for k, v in sorted(profile.items())} + return c, used_new, len(set(pub) - set(edges)) + + +def bill(result, program, n_edges): + profile = {str(k): v for k, v in sorted(result["paid_profile"].items())} + return { + "events": len(program), + "scalar_adds": result["scalar_events"]["add"], + "private_events": {k: result["scalar_events"][k] for k in ("zero", "copy", "erase")}, + "transport_occurrences": sum(profile.values()), + "rank_mass": result["rank_mass"], + "paid_profile": profile, + "distinct_native_edges": n_edges, + "endpoint_adapters": result["intrinsic_endpoint_adapters"], + "formal_boundary_columns": result["formal_boundary_columns"], + } + + +def profile_delta(a, b): + keys = sorted({int(k) for k in a["paid_profile"]} | {int(k) for k in b["paid_profile"]}) + out = {} + for k in keys: + d = b["paid_profile"].get(str(k), 0) - a["paid_profile"].get(str(k), 0) + if d: + out[str(k)] = d + return out + + +def majorized(small, big): + """True when `small` is majorized by `big` (same length and sum).""" + s, b = sorted(small, reverse=True), sorted(big, reverse=True) + if len(s) != len(b) or sum(s) != sum(b): + return False + ps = pb = 0 + for x, y in zip(s, b): + ps += x + pb += y + if ps > pb: + return False + return True + + +# --- frame chronology -------------------------------------------------------- + +def frame_history(witness, program): + hist = {n: [(-1, span(f))] for n, f in witness["initial_frames"].items()} + for i, e in enumerate(program): + if e[0] == "transport": + hist[e[1]].append((i, span(e[3]))) + elif e[0] == "zero": + hist.setdefault(e[1], []).append((i, span(e[2]))) + return hist + + +def frame_at(hist, reg, t): + h = hist[reg] + k = bisect.bisect_left([x[0] for x in h], t) - 1 + return h[k][1] + + +def row_replay(witness, program, watch): + state = {n: {n: Fraction(1)} for n in witness["initial_frames"]} + seen = [] + for i, e in enumerate(program): + op = e[0] + if op == "zero": + state[e[1]] = {} + elif op == "erase": + state.pop(e[1]) + elif op == "copy": + state[e[1]] = dict(state[e[2]]) + elif op == "add": + _, dst, src, a, _f = e + if dst == watch[0]: + carried = Fraction(a) * state[src].get(watch[1], Fraction(0)) + before = state[dst].get(watch[1], Fraction(0)) + seen.append((i, src, carried, before + carried)) + for name, v in list(state[src].items()): + z = state[dst].get(name, Fraction(0)) + Fraction(a) * v + if z: + state[dst][name] = z + else: + state[dst].pop(name, None) + return state, seen + + +def closure_table(witness, program, target, head): + hist = frame_history(witness, program) + finals = {n: span(f) for n, f in witness["final_frames"].items()} + monotone = {r: r != "C" and all(a[1] <= b[1] for a, b in zip(h, h[1:])) for r, h in hist.items()} + touch = {} + for i, e in enumerate(program): + if e[0] in ("add", "copy"): + for r in (e[1], e[2]): + touch.setdefault(r, []).append(i) + rows = [] + for i, e in enumerate(program): + if e[0] != "add" or e[1] != target: + continue + host = {target: i} + work = [target] + while work: + r = work.pop() + t = host[r] + for j in touch.get(r, []): + if j < t: + continue + other = program[j][2] if program[j][1] == r else program[j][1] + if other not in host or host[other] > j: + host[other] = j + work.append(other) + change = {r: t for r, t in host.items() if head not in frame_at(hist, r, t)} + hard, slot, private = [], [], [] + for r, t in sorted(change.items(), key=lambda x: (x[1], x[0])): + if not monotone.get(r, False): + private.append([r, t]) + elif r in finals and head not in finals[r]: + hard.append([r, t, "final frame excludes head"]) + elif not any(-1 < j < t for j, _ in hist[r]): + slot.append([r, t]) + rows.append({ + "event": i, + "partner": e[2], + "must_change": len(change), + "slot_independent_obstructions": len(hard), + "first_obstruction": hard[0] if hard else None, + "registers_without_prior_transport": len(slot), + "private_registers_forced": private, + "admissible": not hard and not slot and not private, + "forced": {r: t for r, t in sorted(change.items(), key=lambda x: (x[1], x[0]))} if not hard else None, + }) + return rows + + +# --- receipt ----------------------------------------------------------------- + +def receipt(root, cert, new_recipes): + ck = load_checker(root) + witness, fixture, recipes, flags = load_inputs(root) + helper = flags["helpers"][FLAG_INDEX] + head = helper["basis"][0] + source, target = "X%d" % helper["source"], "Y%d" % helper["target"] + need((source, target, head) == ("X21", "Y59", 15), "flag 43 identity") + physical = physical_map(recipes) + program = witness["program"] + published = ck.validate(recipes, witness, fixture, False) + need(published["transports"] == len(recipes["transports"]) == 740, "published native edges") + out = {"published": bill(published, program, published["transports"])} + repaired = {} + used = set() + for name in ("R0", "R1"): + prog = apply_splices(program, cert["repairs"][name]["splices"]) + w2 = dict(witness) + w2["program"] = prog + c2, used_new, dropped = assemble(recipes, prog, new_recipes, physical) + used |= used_new + result = ck.validate(c2, w2, fixture, False) + out[name] = bill(result, prog, result["transports"]) + out[name]["new_native_edges"] = len(used_new) + out[name]["dropped_native_edges"] = dropped + repaired[name] = prog + need(len(used) == len(new_recipes), "every committed recipe is used") + for name in ("R0", "R1"): + out[name]["profile_delta"] = profile_delta(out["published"], out[name]) + for key in ("events", "scalar_adds", "transport_occurrences", "rank_mass"): + out[name]["added_" + key] = out[name][key] - out["published"][key] + + # Retargeted transports and the head co-hosting update. + r0 = repaired["R0"] + changed = [i for i, (a, b) in enumerate(zip(program, r0)) if a != b] + retargeted = [i for i in changed if program[i][0] == "transport"] + relabelled = [i for i in changed if program[i][0] == "add"] + for i in relabelled: + need(program[i][:4] == r0[i][:4], "add registers and coefficient unchanged") + for i in retargeted: + a, b = program[i], r0[i] + need(a[1] == b[1], "same register") + need(span(b[3]) == span(list(a[3]) + [head]) or span(b[3]) == span(a[3]), "after-frame is published plus head") + need(span(b[2]) == span(a[2]) or span(b[2]) == span(list(a[2]) + [head]), "before-frame is published plus head") + pub_ranks = [program[i][4] for i in retargeted] + new_ranks = [r0[i][4] for i in retargeted] + hist = frame_history(witness, r0) + adds = [i for i, e in enumerate(r0) if e[0] == "add" and e[1] == target] + last = adds[-1] + chart = r0[last][4] + src_frame = frame_at(hist, source, last) + later_source = [i for i, e in enumerate(r0) if i > last and source in e[1:3]] + _, seen = row_replay(witness, r0, (target, source)) + delivery = [[i, src, str(c), str(after)] for i, src, c, after in seen if c] + pub_hist = frame_history(witness, program) + pub_hosting_updates = [i for i in adds if head in frame_at(pub_hist, target, i)] + hosting_updates = [i for i in adds if head in frame_at(hist, target, i) and head in frame_at(hist, source, i)] + r1 = repaired["R1"] + h1 = frame_history(witness, r1) + adds1 = [i for i, e in enumerate(r1) if e[0] == "add" and e[1] == target] + out["R0"]["retargeted_transports"] = retargeted + out["R0"]["relabelled_add_charts"] = relabelled + out["R0"]["retargeted_ranks_published"] = pub_ranks + out["R0"]["retargeted_ranks_repaired"] = new_ranks + out["R0"]["majorized_by_published"] = majorized(new_ranks, pub_ranks) + out["R0"]["registers_changed"] = sorted({program[i][1] for i in retargeted}) + out["head_cohosting"] = { + "published_head_hosting_target_updates": pub_hosting_updates, + "R0_cohosted_target_updates": hosting_updates, + "R0_last_target_update": last, + "R0_update_partner": r0[last][2], + "R0_update_chart": chart, + "R0_update_chart_rank": rank(chart), + "R0_source_frame_rank_at_update": rank(sorted(src_frame - {0})), + "R0_source_spans_head_at_update": head in src_frame, + "R0_source_events_after_update": later_source, + "R0_source_delivery_into_target": delivery, + "R1_cohosted_target_updates": [i for i in adds1 if head in frame_at(h1, target, i) and head in frame_at(h1, source, i)], + "R1_last_target_update": adds1[-1], + } + table = closure_table(witness, program, target, head) + admissible = [row["event"] for row in table if row["admissible"]] + obstructed = [row["event"] for row in table if row["slot_independent_obstructions"]] + gain = {} + for e in program: + if e[0] == "transport": + gain[e[1]] = gain.get(e[1], 0) + e[4] + floor = [r for r in witness["initial_frames"] + if gain.get(r, 0) == rank(witness["final_frames"][r]) - rank(witness["initial_frames"][r])] + need(len(floor) == len(witness["initial_frames"]) == 280, "every non-private register at its rank floor") + out["forced_hosting"] = { + "non_private_registers_at_rank_floor": len(floor), + "table": table, + "admissible_updates": admissible, + "slot_independently_obstructed_updates": obstructed, + } + return { + "schema_version": 1, + "claim_id": "p104-flag43-head-step-repair", + "pinned_main": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "flag_index": FLAG_INDEX, + "source_register": source, + "target_register": target, + "basis_head": head, + "repairs": cert["repairs"], + "bill": {k: out[k] for k in ("published", "R0", "R1")}, + "head_cohosting": out["head_cohosting"], + "forced_hosting": out["forced_hosting"], + "selected_kappa": SELECTED_KAPPA, + "no_new_kappa": True, + } + + +def admit(root, cert, new_recipes): + got = json.loads(json.dumps(receipt(root, cert, new_recipes))) + need(got == cert, "receipt differs from committed certificate") + b = cert["bill"] + r0, r1, hc, fh = b["R0"], b["R1"], cert["head_cohosting"], cert["forced_hosting"] + need([r0["added_" + k] for k in ("events", "scalar_adds", "transport_occurrences", "rank_mass")] == [0, 0, 0, 0], "R0 adds nothing to the counted bill") + need(r0["profile_delta"] == {"1": -3, "2": 5, "3": -1, "4": -1}, "R0 profile delta") + need(len(r0["retargeted_transports"]) == 9 and r0["majorized_by_published"], "R0 retargets nine transports by majorization") + need(r0["registers_changed"] == ["D17", "D28", "Y103", "Y59"], "R0 changed registers") + need(r1["added_events"] == 1 and r1["added_transport_occurrences"] == 1 and r1["added_rank_mass"] == 0, "R1 bill") + need(r1["profile_delta"] == {"2": 2, "4": -1}, "R1 profile delta") + need(hc["published_head_hosting_target_updates"] == [], "published word has no head-hosting update") + need(hc["R0_cohosted_target_updates"] == [3364] and hc["R0_source_spans_head_at_update"], "R0 co-hosts the head at 3364") + need(hc["R0_source_events_after_update"] == [3705, 3760, 3811, 3863], "source still live") + need(hc["R0_source_delivery_into_target"][-1] == [3364, "D17", "1/2", "1/2"], "3364 settles the source coefficient") + need(hc["R1_cohosted_target_updates"] == [hc["R1_last_target_update"]], "R1 co-hosts at its last update") + need(fh["admissible_updates"] == [3364], "3364 is the only admissible update") + need(len(fh["slot_independently_obstructed_updates"]) == 14, "every earlier update obstructed") + forced = [row for row in fh["table"] if row["event"] == 3364][0]["forced"] + need(forced == {"D17": 3364, "Y59": 3364, "Y103": 3366, "D28": 3462}, "forced register set") + need(cert["selected_kappa"] == SELECTED_KAPPA and cert["no_new_kappa"] is True, "kappa unchanged") + return got + + +def main(root=ROOT): + cert = loads((HERE / "CERTIFICATE.json").read_bytes()) + new_recipes = loads((HERE / "REPAIR-RECIPES.json").read_bytes())["recipes"] + admit(root, cert, new_recipes) + print(MARKER) + + +if __name__ == "__main__": + main(Path(sys.argv[1]).resolve() if len(sys.argv) > 1 else ROOT)