diff --git a/research/p104-flag1-side-correction-bill/CERTIFICATE.json b/research/p104-flag1-side-correction-bill/CERTIFICATE.json new file mode 100644 index 0000000000..27a7d7018e --- /dev/null +++ b/research/p104-flag1-side-correction-bill/CERTIFICATE.json @@ -0,0 +1,3537 @@ +{ + "basis_head": 232, + "bill": { + "E": { + "X0_frame_rank_before_correction": 9, + "Y7_final_X0": "0", + "Y7_final_row_is_identity": false, + "Y7_frame_rank_before_correction": 9, + "added_rank_by_register": {}, + "added_vs_base": { + "events": 1, + "rank_mass": 0, + "scalar_adds": 1, + "transport_occurrences": 0 + }, + "added_vs_published": { + "events": 1, + "rank_mass": 2, + "scalar_adds": 1, + "transport_occurrences": 0 + }, + "base": "R1", + "changed_final_rows": [ + "Y7" + ], + "correction_adds": 1, + "correction_chart_ranks": [ + 9 + ], + "delivering_update_chart_rank": 9, + "distinct_native_edges": 741, + "endpoint_adapters": 208, + "events": 4059, + "head_in_correction_charts": true, + "head_in_delivering_update_chart": true, + "native_validate_coefficient_zero": "PASS", + "paid_profile": { + "1": 1074, + "2": 58, + "3": 86, + "4": 104, + "5": 48, + "6": 23, + "7": 8, + "8": 9 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "profile_delta_vs_base": {}, + "rank_mass": 2370, + "real_word_rejected_by_unchanged_checker_at": "full physical boundary endpoint Y7", + "scalar_adds": 2625, + "transport_occurrences": 1410 + }, + "Erow": { + "X0_frame_rank_before_correction": 9, + "Y7_final_X0": "0", + "Y7_final_row_is_identity": true, + "Y7_frame_rank_before_correction": 9, + "added_rank_by_register": {}, + "added_vs_base": { + "events": 48, + "rank_mass": 0, + "scalar_adds": 48, + "transport_occurrences": 0 + }, + "added_vs_published": { + "events": 48, + "rank_mass": 2, + "scalar_adds": 48, + "transport_occurrences": 0 + }, + "base": "R1", + "changed_final_rows": [ + "Y7" + ], + "correction_adds": 48, + "correction_chart_ranks": [ + 9 + ], + "delivering_update_chart_rank": 9, + "distinct_native_edges": 741, + "endpoint_adapters": 208, + "events": 4106, + "head_in_correction_charts": true, + "head_in_delivering_update_chart": true, + "native_validate_coefficient_zero": "PASS", + "paid_profile": { + "1": 1074, + "2": 58, + "3": 86, + "4": 104, + "5": 48, + "6": 23, + "7": 8, + "8": 9 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "profile_delta_vs_base": {}, + "rank_mass": 2370, + "real_word_rejected_by_unchanged_checker_at": "full physical boundary endpoint Y7", + "scalar_adds": 2672, + "transport_occurrences": 1410 + }, + "P": { + "X0_frame_rank_before_correction": 9, + "Y7_final_X0": "0", + "Y7_final_row_is_identity": false, + "Y7_frame_rank_before_correction": 3, + "added_rank_by_register": { + "C": 1 + }, + "added_vs_base": { + "events": 5, + "rank_mass": 1, + "scalar_adds": 1, + "transport_occurrences": 1 + }, + "added_vs_published": { + "events": 6, + "rank_mass": 3, + "scalar_adds": 1, + "transport_occurrences": 2 + }, + "base": "R0", + "changed_final_rows": [ + "Y7" + ], + "correction_adds": 1, + "correction_chart_ranks": [ + 8 + ], + "delivering_update_chart_rank": 3, + "distinct_native_edges": 743, + "endpoint_adapters": 208, + "events": 4064, + "head_in_correction_charts": true, + "head_in_delivering_update_chart": true, + "native_validate_coefficient_zero": "PASS", + "paid_profile": { + "1": 1074, + "2": 60, + "3": 86, + "4": 104, + "5": 49, + "6": 23, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 9, + "erase": 9, + "zero": 9 + }, + "profile_delta_vs_base": { + "1": 1 + }, + "rank_mass": 2371, + "real_word_rejected_by_unchanged_checker_at": "full physical boundary endpoint Y7", + "scalar_adds": 2625, + "transport_occurrences": 1412 + }, + "R0": { + "distinct_native_edges": 742, + "endpoint_adapters": 208, + "events": 4059, + "paid_profile": { + "1": 1073, + "2": 60, + "3": 86, + "4": 104, + "5": 49, + "6": 23, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "rank_mass": 2370, + "scalar_adds": 2624, + "transport_occurrences": 1411 + }, + "R1": { + "distinct_native_edges": 741, + "endpoint_adapters": 208, + "events": 4058, + "paid_profile": { + "1": 1074, + "2": 58, + "3": 86, + "4": 104, + "5": 48, + "6": 23, + "7": 8, + "8": 9 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "rank_mass": 2370, + "scalar_adds": 2624, + "transport_occurrences": 1410 + }, + "S": { + "X0_frame_rank_before_correction": 9, + "Y7_final_X0": "0", + "Y7_final_row_is_identity": false, + "Y7_frame_rank_before_correction": 3, + "added_rank_by_register": { + "X0": 2 + }, + "added_vs_base": { + "events": 3, + "rank_mass": 2, + "scalar_adds": 1, + "transport_occurrences": 2 + }, + "added_vs_published": { + "events": 4, + "rank_mass": 4, + "scalar_adds": 1, + "transport_occurrences": 3 + }, + "base": "R0", + "changed_final_rows": [ + "Y7" + ], + "correction_adds": 1, + "correction_chart_ranks": [ + 8 + ], + "delivering_update_chart_rank": 3, + "distinct_native_edges": 744, + "endpoint_adapters": 208, + "events": 4062, + "head_in_correction_charts": true, + "head_in_delivering_update_chart": true, + "native_validate_coefficient_zero": "PASS", + "paid_profile": { + "1": 1075, + "2": 60, + "3": 86, + "4": 104, + "5": 49, + "6": 23, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "profile_delta_vs_base": { + "1": 2 + }, + "rank_mass": 2372, + "real_word_rejected_by_unchanged_checker_at": "full physical boundary endpoint Y7", + "scalar_adds": 2625, + "transport_occurrences": 1413 + }, + "T": { + "X0_frame_rank_before_correction": 9, + "Y7_final_X0": "0", + "Y7_final_row_is_identity": false, + "Y7_frame_rank_before_correction": 3, + "added_rank_by_register": { + "Y7": 2 + }, + "added_vs_base": { + "events": 2, + "rank_mass": 2, + "scalar_adds": 1, + "transport_occurrences": 1 + }, + "added_vs_published": { + "events": 3, + "rank_mass": 4, + "scalar_adds": 1, + "transport_occurrences": 2 + }, + "base": "R0", + "changed_final_rows": [ + "Y7" + ], + "correction_adds": 1, + "correction_chart_ranks": [ + 9 + ], + "delivering_update_chart_rank": 3, + "distinct_native_edges": 743, + "endpoint_adapters": 208, + "events": 4061, + "head_in_correction_charts": true, + "head_in_delivering_update_chart": true, + "native_validate_coefficient_zero": "PASS", + "paid_profile": { + "1": 1074, + "2": 60, + "3": 86, + "4": 104, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "profile_delta_vs_base": { + "1": 1, + "5": -1, + "6": 1 + }, + "rank_mass": 2372, + "real_word_rejected_by_unchanged_checker_at": "full physical boundary endpoint Y7", + "scalar_adds": 2625, + "transport_occurrences": 1412 + }, + "Tend": { + "X0_frame_rank_before_correction": 9, + "Y7_final_X0": "0", + "Y7_final_row_is_identity": false, + "Y7_frame_rank_before_correction": 2, + "added_rank_by_register": { + "Y7": 2 + }, + "added_vs_base": { + "events": 2, + "rank_mass": 2, + "scalar_adds": 1, + "transport_occurrences": 1 + }, + "added_vs_published": { + "events": 2, + "rank_mass": 2, + "scalar_adds": 1, + "transport_occurrences": 1 + }, + "base": "published", + "changed_final_rows": [ + "Y7" + ], + "correction_adds": 1, + "correction_chart_ranks": [ + 9 + ], + "delivering_update_chart_rank": 2, + "distinct_native_edges": 741, + "endpoint_adapters": 208, + "events": 4060, + "head_in_correction_charts": true, + "head_in_delivering_update_chart": false, + "native_validate_coefficient_zero": "PASS", + "paid_profile": { + "1": 1075, + "2": 58, + "3": 86, + "4": 104, + "5": 48, + "6": 23, + "7": 9, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "profile_delta_vs_base": { + "1": 1, + "6": -1, + "7": 1 + }, + "rank_mass": 2370, + "real_word_rejected_by_unchanged_checker_at": "full physical boundary endpoint Y7", + "scalar_adds": 2625, + "transport_occurrences": 1411 + }, + "Trow": { + "X0_frame_rank_before_correction": 9, + "Y7_final_X0": "0", + "Y7_final_row_is_identity": true, + "Y7_frame_rank_before_correction": 3, + "added_rank_by_register": { + "Y7": 2 + }, + "added_vs_base": { + "events": 49, + "rank_mass": 2, + "scalar_adds": 48, + "transport_occurrences": 1 + }, + "added_vs_published": { + "events": 50, + "rank_mass": 4, + "scalar_adds": 48, + "transport_occurrences": 2 + }, + "base": "R0", + "changed_final_rows": [ + "Y7" + ], + "correction_adds": 48, + "correction_chart_ranks": [ + 9 + ], + "delivering_update_chart_rank": 3, + "distinct_native_edges": 743, + "endpoint_adapters": 208, + "events": 4108, + "head_in_correction_charts": true, + "head_in_delivering_update_chart": true, + "native_validate_coefficient_zero": "PASS", + "paid_profile": { + "1": 1074, + "2": 60, + "3": 86, + "4": 104, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "profile_delta_vs_base": { + "1": 1, + "5": -1, + "6": 1 + }, + "rank_mass": 2372, + "real_word_rejected_by_unchanged_checker_at": "full physical boundary endpoint Y7", + "scalar_adds": 2672, + "transport_occurrences": 1412 + }, + "published": { + "distinct_native_edges": 740, + "endpoint_adapters": 208, + "events": 4058, + "paid_profile": { + "1": 1074, + "2": 58, + "3": 86, + "4": 104, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "rank_mass": 2368, + "scalar_adds": 2624, + "transport_occurrences": 1410 + } + }, + "claim_id": "p104-flag1-side-correction-bill", + "corrections": { + "R0": { + "P": { + "route": "one added private lifetime under the inherited private-copy contract: copy X0 into C at the full chart, descend C to Y7's final hyperplane, deliver, discard", + "splices": [ + { + "events": [ + [ + "transport", + "Y7", + [ + 95, + 486, + 232 + ], + [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ], + 5 + ], + [ + "zero", + "C", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "copy", + "C", + "X0", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "transport", + "C", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ], + 1 + ], + [ + "add", + "Y7", + "C", + "1/2", + [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ] + ], + [ + "erase", + "C", + [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ] + ] + ], + "published": [ + [ + "transport", + "Y7", + [ + 95, + 486, + 232 + ], + [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ], + 5 + ] + ], + "published_range": [ + 3474, + 3475 + ] + } + ] + }, + "S": { + "route": "source detour: Y7 takes R0's terminal transport, X0 descends to Y7's final hyperplane for one ADD and returns to the full chart before its next read", + "splices": [ + { + "events": [ + [ + "transport", + "Y7", + [ + 95, + 486, + 232 + ], + [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ], + 5 + ], + [ + "transport", + "X0", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ], + 1 + ], + [ + "add", + "Y7", + "X0", + "1/2", + [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ] + ], + [ + "transport", + "X0", + [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 1 + ] + ], + "published": [ + [ + "transport", + "Y7", + [ + 95, + 486, + 232 + ], + [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ], + 5 + ] + ], + "published_range": [ + 3474, + 3475 + ] + } + ] + }, + "T": { + "route": "target lift at R0's cut: Y7 leaves the co-hosted chart [95,486,232] for the full chart, takes the entry from X0 there, then descends to its final hyperplane", + "splices": [ + { + "events": [ + [ + "transport", + "Y7", + [ + 95, + 486, + 232 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 6 + ], + [ + "add", + "Y7", + "X0", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "transport", + "Y7", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ], + 1 + ] + ], + "published": [ + [ + "transport", + "Y7", + [ + 95, + 486, + 232 + ], + [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ], + 5 + ] + ], + "published_range": [ + 3474, + 3475 + ] + } + ] + }, + "Trow": { + "route": "whole Y7 row of I - G/2 on T's lift: every off-diagonal source entry -G[7,s]/2 is added while Y7 sits in the full chart", + "splices": [ + { + "events": [ + [ + "transport", + "Y7", + [ + 95, + 486, + 232 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 6 + ], + [ + "add", + "Y7", + "X0", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X1", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X2", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X8", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X9", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X10", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X11", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X13", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X15", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X20", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X22", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X24", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X29", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X31", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X34", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X35", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X38", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X39", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X40", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X41", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X44", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X45", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X49", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X50", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X53", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X54", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X55", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X56", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X59", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X60", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X65", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X66", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X69", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X70", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X71", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X72", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X75", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X76", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X81", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X84", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X85", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X86", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X87", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X90", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X94", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X96", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X100", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X102", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "transport", + "Y7", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ], + 1 + ] + ], + "published": [ + [ + "transport", + "Y7", + [ + 95, + 486, + 232 + ], + [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ], + 5 + ] + ], + "published_range": [ + 3474, + 3475 + ] + } + ] + } + }, + "R1": { + "E": { + "route": "in-chart entry at R1's co-hosted update: Y7 and X0 already share the full chart at the relocated delivering ADD, so the entry is one extra ADD there", + "splices": [ + { + "events": [ + [ + "add", + "Y7", + "D17", + "1/4", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X0", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ] + ], + "published": [ + [ + "add", + "Y7", + "D17", + "1/4", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ] + ], + "published_range": [ + 3611, + 3612 + ] + } + ] + }, + "Erow": { + "route": "whole Y7 row of I - G/2 at R1's co-hosted update: all 48 off-diagonal entries are added in the full chart right after the delivering ADD", + "splices": [ + { + "events": [ + [ + "add", + "Y7", + "D17", + "1/4", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X0", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X1", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X2", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X8", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X9", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X10", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X11", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X13", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X15", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X20", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X22", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X24", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X29", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X31", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X34", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X35", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X38", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X39", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X40", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X41", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X44", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X45", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X49", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X50", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X53", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X54", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X55", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X56", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X59", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X60", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X65", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X66", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X69", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X70", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X71", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X72", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X75", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X76", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X81", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X84", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X85", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X86", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X87", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X90", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X94", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X96", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X100", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y7", + "X102", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ] + ], + "published": [ + [ + "add", + "Y7", + "D17", + "1/4", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ] + ], + "published_range": [ + 3611, + 3612 + ] + } + ] + } + }, + "published": { + "Tend": { + "route": "end-cut control on the published word: Y7 leaves [95,486] for the full chart at its terminal transport, takes the entry there, then descends", + "splices": [ + { + "events": [ + [ + "transport", + "Y7", + [ + 95, + 486 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 7 + ], + [ + "add", + "Y7", + "X0", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "transport", + "Y7", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ], + 1 + ] + ], + "published": [ + [ + "transport", + "Y7", + [ + 95, + 486 + ], + [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ], + 6 + ] + ], + "published_range": [ + 3473, + 3474 + ] + } + ] + } + } + }, + "end_cut_comparison": { + "R0_correction_added_rank": 2, + "R0_terminal_transport": [ + 3474, + 5 + ], + "R1_correction_added_rank": 0, + "cohost_discount_R0": 0, + "cohost_discount_R1": 2, + "joint_cohosted_and_corrected_vs_published": { + "R0+P": 3, + "R0+S": 4, + "R0+T": 4, + "R1+E": 2, + "published+Tend_not_cohosted": 2 + }, + "published_detour_added_rank": 2, + "published_terminal_transport": [ + 3473, + 6 + ] + }, + "flag_index": 1, + "no_new_kappa": true, + "obstruction": { + "delivering_add_dropped_in_sweeps": 2797, + "delivering_add_window_slots": 1116, + "entry": { + "correction_coefficient": "1/2", + "diagonal_gram": 2, + "gram": -1, + "source": "X0", + "target": "Y7" + }, + "exit_partner": "G18", + "flag_head_in_target_final": true, + "forcing_chain": [ + [ + 616, + "X7", + "G11" + ], + [ + 679, + "G11", + "X20" + ], + [ + 1070, + "X20", + "G18" + ], + [ + 1074, + "G18", + "X0" + ] + ], + "forcing_source": "X7", + "forcing_source_gram_with_target": 2, + "forcing_source_head": [ + 387 + ], + "non_private_registers_at_rank_floor": 280, + "order_preserving_cohost_single_register_rescues": [ + "D17" + ], + "order_preserving_joint_first_obstruction": { + "D17": [ + [ + 0, + [ + 22, + "Y8" + ] + ], + [ + 20, + [ + 23, + "Y8" + ] + ], + [ + 21, + [ + 2014, + "Y8" + ] + ], + [ + 841, + [ + 2014, + "Y8" + ] + ], + [ + 1075, + [ + 1075, + "Y7" + ] + ], + [ + 1312, + [ + 1312, + "Y7" + ] + ], + [ + 1486, + [ + 1486, + "Y7" + ] + ], + [ + 1691, + [ + 1691, + "Y7" + ] + ], + [ + 1793, + [ + 1793, + "Y7" + ] + ], + [ + 1904, + [ + 1904, + "Y7" + ] + ], + [ + 1990, + [ + 1990, + "Y7" + ] + ], + [ + 2014, + [ + 2014, + "Y7" + ] + ], + [ + 2147, + [ + 2147, + "Y7" + ] + ], + [ + 2527, + [ + 2527, + "Y7" + ] + ], + [ + 2798, + [ + 2798, + "Y7" + ] + ], + [ + 3643, + [ + 3643, + "Y7" + ] + ], + [ + 3799, + [ + 3799, + "Y7" + ] + ], + [ + 3851, + [ + 3851, + "Y7" + ] + ], + [ + 3955, + [ + 3955, + "Y7" + ] + ] + ], + "none": [ + [ + 0, + [ + 22, + "Y8" + ] + ], + [ + 20, + [ + 23, + "Y8" + ] + ], + [ + 21, + [ + 2014, + "Y8" + ] + ], + [ + 841, + [ + 2014, + "Y8" + ] + ], + [ + 1075, + [ + 1075, + "Y7" + ] + ], + [ + 1312, + [ + 1312, + "Y7" + ] + ], + [ + 1486, + [ + 1486, + "Y7" + ] + ], + [ + 1691, + [ + 1691, + "Y7" + ] + ], + [ + 1793, + [ + 1793, + "Y7" + ] + ], + [ + 1904, + [ + 1904, + "Y7" + ] + ], + [ + 1990, + [ + 1990, + "Y7" + ] + ], + [ + 2014, + [ + 2014, + "Y7" + ] + ], + [ + 2147, + [ + 2147, + "Y7" + ] + ], + [ + 2527, + [ + 2527, + "Y7" + ] + ], + [ + 2798, + [ + 2798, + "Y7" + ] + ], + [ + 3643, + [ + 2799, + "Y8" + ] + ], + [ + 3799, + [ + 2799, + "Y8" + ] + ], + [ + 3851, + [ + 2799, + "Y8" + ] + ], + [ + 3955, + [ + 2799, + "Y8" + ] + ] + ] + }, + "outside_heads_have_even_gram": true, + "private_early_delivery_cuts": 5, + "private_early_first_obstruction": [ + [ + 0, + [ + 22, + "Y8" + ] + ], + [ + 20, + [ + 23, + "Y8" + ] + ], + [ + 21, + [ + 2014, + "Y8" + ] + ], + [ + 2014, + [ + 2147, + "Y8" + ] + ], + [ + 2147, + [ + 2528, + "Y8" + ] + ] + ], + "published_private_lifetimes": [ + 2461, + 2524 + ], + "row_7_offdiagonal_nonzero": 48, + "source_first_read": [ + 840, + [ + "add", + "G25", + "X0", + 2 + ] + ], + "source_forced_frame_at_exit": [ + 256, + 128, + 64, + 32, + 8, + 3 + ], + "source_forced_full_from": 1690, + "source_forced_rank_at_events": [ + [ + 840, + "G25", + 2 + ], + [ + 1074, + "G18", + 6 + ], + [ + 1311, + "G0", + 7 + ], + [ + 1485, + "G12", + 8 + ], + [ + 1690, + "G25", + 9 + ], + [ + 1792, + "G18", + 9 + ], + [ + 1903, + "G0", + 9 + ], + [ + 1989, + "G12", + 9 + ], + [ + 3642, + "Q0", + 9 + ], + [ + 3798, + "Q3", + 9 + ], + [ + 3850, + "Q4", + 9 + ], + [ + 3954, + "Q6", + 9 + ] + ], + "source_leaves_target_final_at": [ + 1074, + [ + "add", + "G18", + "X0", + -2 + ] + ], + "sources_with_head_outside_target_final": 56, + "strict_cut_classes": 18, + "strict_first_obstruction": [ + [ + 0, + [ + 22, + "Y8" + ] + ], + [ + 20, + [ + 23, + "Y8" + ] + ], + [ + 21, + [ + 2014, + "Y8" + ] + ], + [ + 841, + [ + 2014, + "Y8" + ] + ], + [ + 1075, + [ + 1075, + "Y7" + ] + ], + [ + 1312, + [ + 1312, + "Y7" + ] + ], + [ + 1486, + [ + 1486, + "Y7" + ] + ], + [ + 1691, + [ + 1691, + "Y7" + ] + ], + [ + 1793, + [ + 1793, + "Y7" + ] + ], + [ + 1904, + [ + 1904, + "Y7" + ] + ], + [ + 1990, + [ + 1990, + "Y7" + ] + ], + [ + 2014, + [ + 2014, + "Y7" + ] + ], + [ + 2147, + [ + 2147, + "Y7" + ] + ], + [ + 2527, + [ + 2527, + "Y7" + ] + ], + [ + 3643, + [ + 3643, + "Y7" + ] + ], + [ + 3799, + [ + 3799, + "Y7" + ] + ], + [ + 3851, + [ + 3851, + "Y7" + ] + ], + [ + 3955, + [ + 3955, + "Y7" + ] + ] + ], + "strict_published_order_first_obstruction": [ + [ + 0, + [ + 22, + "Y8" + ] + ], + [ + 20, + [ + 23, + "Y8" + ] + ], + [ + 21, + [ + 2014, + "Y8" + ] + ], + [ + 841, + [ + 2014, + "Y8" + ] + ], + [ + 1075, + [ + 1075, + "Y7" + ] + ], + [ + 1312, + [ + 1312, + "Y7" + ] + ], + [ + 1486, + [ + 1486, + "Y7" + ] + ], + [ + 1691, + [ + 1691, + "Y7" + ] + ], + [ + 1793, + [ + 1793, + "Y7" + ] + ], + [ + 1904, + [ + 1904, + "Y7" + ] + ], + [ + 1990, + [ + 1990, + "Y7" + ] + ], + [ + 2014, + [ + 2014, + "Y7" + ] + ], + [ + 2147, + [ + 2147, + "Y7" + ] + ], + [ + 2527, + [ + 2527, + "Y7" + ] + ], + [ + 2798, + [ + 2798, + "Y7" + ] + ], + [ + 3643, + [ + 3643, + "Y7" + ] + ], + [ + 3799, + [ + 3799, + "Y7" + ] + ], + [ + 3851, + [ + 3851, + "Y7" + ] + ], + [ + 3955, + [ + 3955, + "Y7" + ] + ] + ], + "target_final_frame": [ + 256, + 128, + 64, + 33, + 17, + 9, + 5, + 2 + ] + }, + "pinned_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "repair_source": { + "head": "8fecbf7df7b48c9004bd10a0da6a81f33d455737", + "pr": 3532, + "vendored": [ + "research/p104-flag1-side-correction-bill/inputs/pr3532/CERTIFICATE.json", + "research/p104-flag1-side-correction-bill/inputs/pr3532/REPAIR-RECIPES.json" + ] + }, + "requested_pin": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "schema_version": 1, + "selected_kappa": "0.001672660197076918" +} diff --git a/research/p104-flag1-side-correction-bill/CORRECTION-RECIPES.json b/research/p104-flag1-side-correction-bill/CORRECTION-RECIPES.json new file mode 100644 index 0000000000..38eac1d078 --- /dev/null +++ b/research/p104-flag1-side-correction-bill/CORRECTION-RECIPES.json @@ -0,0 +1,300 @@ +{ + "clifford_exact_sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "compiler_sha256": "9d2fc2d81962ddb0b4dd7d6482d9918a87a6b05759690317dea79939ca5656a3", + "recipes": [ + { + "new": [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + "old": [ + 257, + 128, + 65, + 32, + 17, + 9, + 5, + 3 + ], + "rank": 1, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 3, + 5, + 9, + 17, + 33, + 64, + 129, + 256, + 1 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 1, + "right": { + "linear_Z4": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ], + "matrix_rows": [ + 257, + 256, + 258, + 260, + 264, + 272, + 32, + 320, + 128 + ], + "offset": 3, + "phase": 0, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + } + }, + { + "new": [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + "old": [ + 263, + 133, + 30 + ], + "rank": 6, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 2, + 3, + 3, + 2, + 2, + 0, + 0, + 0 + ], + "matrix_rows": [ + 65, + 130, + 260, + 8, + 14, + 16, + 32, + 5, + 7 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 2, + 9, + 12, + 14, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 6, + "right": { + "linear_Z4": [ + 0, + 0, + 2, + 0, + 0, + 2, + 2, + 1, + 0 + ], + "matrix_rows": [ + 145, + 146, + 4, + 24, + 32, + 64, + 272, + 384, + 400 + ], + "offset": 434, + "phase": 1, + "quadratic_rows": [ + 384, + 272, + 400, + 16, + 142, + 0, + 0, + 149, + 7 + ] + } + } + }, + { + "new": [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + "old": [ + 281, + 133 + ], + "rank": 7, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 2, + 3, + 3, + 3, + 2, + 2, + 0, + 0 + ], + "matrix_rows": [ + 129, + 2, + 260, + 8, + 16, + 32, + 64, + 5, + 25 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 28, + 0, + 5, + 25, + 25, + 0, + 0, + 0, + 0 + ] + }, + "rank": 7, + "right": { + "linear_Z4": [ + 0, + 2, + 0, + 0, + 0, + 2, + 2, + 1, + 0 + ], + "matrix_rows": [ + 129, + 2, + 260, + 264, + 272, + 32, + 64, + 256, + 384 + ], + "offset": 358, + "phase": 3, + "quadratic_rows": [ + 384, + 0, + 128, + 256, + 256, + 0, + 0, + 389, + 153 + ] + } + } + } + ], + "schema_version": 1, + "scope": "Native recipes for the transport edges used by the flag-1 corrections (T, S, P, Trow on #3532's R0; E, Erow on R1; Tend on the published word) that are absent from the published p104-native-channel recipe set and from #3532's REPAIR-RECIPES.json. Lowered with the pinned compile.py / vendor/clifford_exact.py; checked by the published check_native.validate() during replay." +} diff --git a/research/p104-flag1-side-correction-bill/MASTER-HANDOFF.md b/research/p104-flag1-side-correction-bill/MASTER-HANDOFF.md new file mode 100644 index 0000000000..ad11cf868d --- /dev/null +++ b/research/p104-flag1-side-correction-bill/MASTER-HANDOFF.md @@ -0,0 +1,153 @@ +# Master handoff — `research/p104-flag1-side-correction-bill/` + +## Candidate + +- Branch: `cursor/flag1-side-correction-bill-988a` (VictorLiwentao fork). The + `-988a` suffix is this worker's environment-required branch suffix, not + `-60b9`. +- Content tip: `f5c09d4688c848f02d546a08191b047cd7b3687f`. This commit holds the + full scientific package. +- Packaging tip: the child commit that adds only this handoff file. Read its SHA + with `git rev-parse origin/cursor/flag1-side-correction-bill-988a`. +- Package: `research/p104-flag1-side-correction-bill/` +- Base: CrocSwap main `20ecf2891d80b5acf18d980b2164fb44ea7faa90`. It contains + merged #3508 and #3451. The requested pin `6f100d4bb5083f8c35d96fd95a539811c62f245c` + is an ancestor. +- #3532 inputs: open #3532 is not on any main. Its `CERTIFICATE.json` and + `REPAIR-RECIPES.json` are vendored byte-identically under `inputs/pr3532/` + from head `8fecbf7df7b48c9004bd10a0da6a81f33d455737`. `SOURCES.json` carries + `head:` provenance pins for those files and #3601's README, and both scanners + check the vendored SHA-256. The registry pin check needs those head commits + in the local object store. +- Card: `p104-side-correction` (refined), priority revision 6. The card is + byte-identical to the catalogue at the base. +- κ: unchanged at `0.001672660197076918`. +- Author and committer: Wentao Li ``. A hook-injected + co-author trailer was stripped with `git commit-tree`. +- No CrocSwap PR has been opened. + +## Claim + +This is the flag-1 analogue of #3601. Flag 1's entry is `(7, 0)`, and +`G[7,0] = −1`, so the `I − G/2` correction adds `+1/2·X0` into `Y7`. It is +priced at both of #3532's co-hosted charts: + +| Word | Base | Δ events | Δ ADDs | Δ transports | Δ rank vs base | vs published | +|---|---|---:|---:|---:|---:|---:| +| E: one ADD in FULL after R1's relocated delivering ADD | R1 | +1 | +1 | 0 | 0 | +2 | +| Erow: all 48 row-7 entries there | R1 | +48 | +48 | 0 | 0 | +2 | +| T: `Y7: A3→FULL`, ADD, `FULL→F7` | R0 | +2 | +1 | +1 | +2 | +4 | +| S: `X0: FULL→F7→FULL` detour | R0 | +3 | +1 | +2 | +2 | +4 | +| P: one private-copy lifetime | R0 | +5 | +1 | +1 | +1 | +3 | +| Trow: all 48 entries on T's lift | R0 | +49 | +48 | +1 | +2 | +4 | +| Tend: end-cut control | published | +2 | +1 | +1 | +2 | +2 | + +The co-host discount is **0 at R0**, as for flag 43, and **2 at R1**. The +discount at R1 is new for flag 1: R1's relocation already lifts `Y7` into the +full chart where `X0` sits, so the correction rides on R1's +2. + +All seven words pass the unchanged `check_native.validate()` with coefficients +set to `0`. That includes three newly lowered recipes, 208 adapters, 280 rows +and 72 dirty helpers. On each real word the checker fails only at `Y7`'s +endpoint, and exact replay changes only `Y7`. + +**Obstruction (flag-1-specific forcing).** `X7`'s own head `387` is outside +`F7` because `G[7,7] = 2` is even. It reaches `X0` at event 1074 along +`X7 –616– G11 –679– X20 –1070– G18 –1074– X0`. A least-frame sweep with the +delivering ADD dropped blocks all 18 insertion classes, so it covers every one +of the 1,116 placements of the delivering ADD. Per-register mass is even, so +the strict minimum is exactly 2. + +**Joint theorem.** Consider words that both co-host the head and apply the +correction. + +- With relocation, the minimum is exactly 2 (R1+E). +- Order-preserving strict words need at least 4 non-private rank, and R0+T and + R0+S attain 4. Only `D17`'s freedom rescues co-hosting alone, and with `D17` + free all 19 correction classes stay blocked. + +The private route costs exactly 1: all 5 early delivery classes are blocked. + +## PASS lines + +```text +PASS_P104_FLAG1_SIDE_CORRECTION_BILL flag=1 entry=(7,0) gram=-1 coefficient=+1/2 zero_mass_placements=0/18(delivery_anywhere_in_1116_slots) forcing=X7(387)-616-G11-679-X20-1070-G18-1074-X0 strict_min_added_rank=2 R0:T=+1transport+1add+2rank S=+2transport+1add+2rank P=+1rank+1private_lifetime Trow=+48add+2rank R1:E=+0transport+1add+0rank Erow=+48add+0rank row7=identity cohost_discount_R0=0 cohost_discount_R1=2 joint_min_relocated=2 joint_min_order_preserving_strict=4 native_validate=7/7 no_new_kappa +PASS_P104_FLAG1_SIDE_CORRECTION_BILL_INDEPENDENT entry=(7,0) coefficient=+1/2 strict_classes_obstructed=18/18(delivery_dropped)+19/19(published_order) early_private_obstructed=5/5 forcing_head=387(X7) R0:T,S,Trow=+2rank P=+1rank R1:E,Erow=+0rank Tend=+2rank joint_order_preserving_single_rescue=none rows_changed=Y7_only row7=identity new_recipes=3 no_new_kappa +PASS_P104_FLAG1_SIDE_CORRECTION_BILL_TESTS cases=18 clean_read_only=1 scanners=2 +PASS_REGISTERED_RESEARCH_PACKAGE research/p104-flag1-side-correction-bill outcome=completed +``` + +## Commands + +```sh +python3.12 -I -B research/p104-flag1-side-correction-bill/verify.py +python3.12 -I -O -Werror -B research/p104-flag1-side-correction-bill/verify.py +python3.12 -I -O -Werror -B research/p104-flag1-side-correction-bill/independent.py +python3.12 -I -O -Werror -B research/p104-flag1-side-correction-bill/test_package.py +python3.12 -B scripts/research_package.py --package research/p104-flag1-side-correction-bill +``` + +Run times: `verify.py` about 60 s, `independent.py` about 6 s, +`test_package.py` about 200 s with 4 workers, and the registry check about +270 s. The default replay is read-only. Admission goes through `need()`, so it +still fires under `-O`, and the package contains no `assert` statements. +Duplicate JSON keys are rejected. Rejection reasons were spot-checked: E in the +wrong chart fails at the common-chart rule, an empty rescue list fails the +census, and the #3532 byte flip fails the pin. + +## Closest priors (cite only) + +- [#3601](https://github.com/CrocSwap/integer-mult-bounds/pull/3601) (open). + Flag 43's bill at #3508's cut, with co-host discount 0. Its format, class Z + and sweep are reused here. +- [#3532](https://github.com/CrocSwap/integer-mult-bounds/pull/3532) (open). + R0, R1, the delivering-update window and the +2 co-host floor, used as + vendored inputs. The late-slot open question 1 is untouched. +- [#3451](https://github.com/CrocSwap/integer-mult-bounds/pull/3451) (merged). + Flag 1's chronology. It is not reprinted here. +- [#3508](https://github.com/CrocSwap/integer-mult-bounds/pull/3508) (merged). + The method and class Z. +- `research/p104-side-correction-rank-obstruction`. Its end-cut +2 invoice + matches Tend. + +## Soft-overlap risks + +- Code shape. `verify.py`, `independent.py` and `test_package.py` follow + #3601's structure closely: same helpers, sweep and bill layout. A reviewer + may read this as a template clone, the same pattern for which the flag-9 + repair was deferred. The new checkable facts are flag-1-specific: + - the R1 free ride (discount 2, versus 0 for flag 43); + - the joint theorem (2 with relocation versus 4 order-preserving), backed by + the single-register census; + - a different forcing chain (the self-head `387` via `G11`/`X20`/`G18`, + instead of `X12`'s `131` via `G9`); + - coverage of every delivering-ADD placement. + If maintainers prefer, these facts could fold into #3601 or #3532 after merge + together with a shared helper module. +- Dependency on open #3532. If #3532 changes its head, the vendored bytes and + pins must be refreshed. +- The end-cut +2 (Tend) is not new on its own. It is a control. +- Open-PR searches for "flag 1 side correction", "I-G/2 flag-1" and "3532" + found only #3532 and #3601. `scripts/find_overlap.py --task + p104-side-correction` had no flag-1 side-correction hit. + +## Open question + +The headline open question is whether flag 1 has a co-hosted and corrected +word with joint added mass 1. That needs a zero-mass late relocation (#3532's +open question 1) plus a private-copy correction. The strict joint minimum with +relocation is 2. Two further questions are open: + +- whether every present-head row needs +2 for its strict entry; +- the H-weighted comparison of R1+E (`H8 − H6`) against Tend + (`H1 − H6 + H7`). + +See `TASK.json`. + +## Limits + +This covers one entry and one target row on the charts of two repairs of one +finite word. The class keeps every published ADD and coefficient. Theorem 3 +bounds non-private mass for strict words; R0+P reaches 3 under the inherited +private-copy discard. There is no global hosting, precision or supplier, and +no κ change. diff --git a/research/p104-flag1-side-correction-bill/NOTICE.md b/research/p104-flag1-side-correction-bill/NOTICE.md new file mode 100644 index 0000000000..4ce3794be8 --- /dev/null +++ b/research/p104-flag1-side-correction-bill/NOTICE.md @@ -0,0 +1,15 @@ +# Notice + +This package applies explicit corrections to #3532's repaired P104 words R0 +and R1 and to the published word in memory, and checks them with the published +native checker and a second scanner. It does not modify frozen upstream sources +or any other package. `inputs/pr3532/CERTIFICATE.json` and +`inputs/pr3532/REPAIR-RECIPES.json` are byte-identical copies of #3532's files +at head `8fecbf7df7b48c9004bd10a0da6a81f33d455737` (Wentao Li; open PR), kept +unchanged. The three recipes in `CORRECTION-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-flag1-side-correction-bill/PROOF.md b/research/p104-flag1-side-correction-bill/PROOF.md new file mode 100644 index 0000000000..51e908d72b --- /dev/null +++ b/research/p104-flag1-side-correction-bill/PROOF.md @@ -0,0 +1,247 @@ +# Proof: the flag-1 side-correction entry at #3532's co-hosted charts + +## Setup + +The base is CrocSwap main `20ecf2891d80b5acf18d980b2164fb44ea7faa90`. The +requested pin `6f100d4b…` is an ancestor of it. The newer base contains merged +#3508 and #3451, which this package cites. + +Inputs, all hash-pinned: + +- the reviewed #1991 witness, recipes and checker in + `research/p104-native-channel/`; +- the #2981 flag matching (flag 1: `X0 → Y7`, basis head `232`); +- #3532's `CERTIFICATE.json` (R0 and R1 splices) and `REPAIR-RECIPES.json`. + +#3532 is still open, so neither file is on main. Both are vendored +byte-identically under `inputs/pr3532/` from #3532's head +`8fecbf7df7b48c9004bd10a0da6a81f33d455737`. `SOURCES.json` records their Git +blobs at that head (`head:` pins), and both scanners check their SHA-256. + +The channel rules are those of `research/p104-native-channel/PROOF.md` §2–§3, +as in #3508, #3532 and #3601: + +- A transport is nested and pays `|dim B − dim A|`. +- An ADD or copy needs both registers in one frame. +- The private register `C` is created by zero, filled by copy and closed by + erase. + +At the end, each target row is `y_t + Σ_s G[t,s] x_s / 2`. The side correction +must add `(I − G/2)x`. Flag 1's entry is `(7, 0)`. Since `G[7,0] = −1`, the +entry is `+1/2`. `Y7`'s only `X0` delivery is 2797 (`Y7 += D17/4`, carrying +`−1/2`). No event reads `Y7`. + +## 1. The corrected words + +Let `F7` be `Y7`'s final frame `[484,232,12,55,75,24,7,2]`. It has rank 8 and +contains `232`. Let FULL be the rank-9 chart, `A2 = [95,486]` and +`A3 = [95,486,232]`. + +**On R0** (#3532's order-preserving repair): + +- `Y7` is in `A3` from 2796 until its terminal transport 3474 + (`A3 → F7`, rank 5); +- `X0` is in FULL from 1486, with later reads at 3643, 3799, 3851 and 3955; +- `C` has no lifetime after 2524. + +Every R0 correction replaces event 3474: + +- **T:** `Y7: A3 → FULL` (rank 6); `Y7 += 1/2·X0` in FULL; `Y7: FULL → F7` + (rank 1). +- **S:** R0's transport; `X0: FULL → F7` (rank 1); `Y7 += 1/2·X0` in `F7`; + `X0: F7 → FULL` (rank 1). +- **P:** R0's transport; `zero C` in FULL; `copy C ← X0`; `C: FULL → F7` + (rank 1); `Y7 += 1/2·C` in `F7`; `erase C`. +- **Trow:** as T, but with all 48 ADDs `Y7 += −G[7,s]/2 · X_s` for `s ≠ 7` + with `G[7,s] ≠ 0`. All 48 sources are in FULL at 3474. + +**On R1** (#3532's relocated repair), event 3610 is `Y7: [95] → FULL` +(rank 8), 3611 is `Y7 += D17/4` in FULL, and 3612 is `Y7: FULL → F7`. `X0` is +in FULL there. Each R1 correction keeps 3611 and inserts after it: + +- **E:** `Y7 += 1/2·X0` in FULL. +- **Erow:** the 48 row-7 ADDs in FULL. All 48 sources are in FULL at 3611. + +**Control on the published word.** Tend replaces 3473 (`Y7: A2 → F7`, +rank 6) with `Y7: A2 → FULL` (rank 7), `Y7 += 1/2·X0` in FULL, and +`Y7: FULL → F7`. + +`FULL → F7` and `[95] → FULL` are #3532's committed recipes. `build.py` lowers +the other three new edges with the pinned compiler: `A3 → FULL`, `A2 → FULL` +and `F7 → FULL`. They are committed in `CORRECTION-RECIPES.json`. + +**Native validation.** As in #3601, `verify.py` runs the published checker +twice per word: + +1. `validate()` runs unchanged on the word with every inserted ADD coefficient + set to `0`. It checks every edge's complete Clifford operator, every + transport binding and rank, all 208 endpoint adapters and the framed + induction over all 280 rows. Every ADD and copy must be in a common chart, + every endpoint frame must match, and the 72 dirty helpers and `C`'s storage + must be restored. None of these depends on ADD coefficients. +2. The real word is replayed with exact rational rows and every final row is + compared with its base word's. + +`Y7` is the only changed row. In E, T, S, P and Tend it changes by exactly +`+1/2·X0`. In Erow and Trow, `Y7`'s final row is exactly `{Y7: 1, X7: 1}`. As a +control, the unchanged `validate()` rejects each real word with +`full physical boundary endpoint Y7`. + +**Bill.** All counts come from the validated words. + +| | events | ADDs | transports | rank mass | edges | profile Δ vs base | added rank by register | +|---|---:|---:|---:|---:|---:|---|---| +| published | 4,058 | 2,624 | 1,410 | 2,368 | 740 | — | — | +| R0 (#3532) | 4,059 | 2,624 | 1,411 | 2,370 | 742 | — | `D17: 2` vs published | +| R1 (#3532) | 4,058 | 2,624 | 1,410 | 2,370 | 741 | — | `Y7: 2` vs published | +| E | 4,059 | 2,625 | 1,410 | 2,370 | 741 | none | none | +| Erow | 4,106 | 2,672 | 1,410 | 2,370 | 741 | none | none | +| T | 4,061 | 2,625 | 1,412 | 2,372 | 743 | `+H1 − H5 + H6` | `Y7: 2` | +| S | 4,062 | 2,625 | 1,413 | 2,372 | 744 | `+2H1` | `X0: 2` | +| P | 4,064 | 2,625 | 1,412 | 2,371 | 743 | `+H1` | `C: 1` | +| Trow | 4,108 | 2,672 | 1,412 | 2,372 | 743 | `+H1 − H5 + H6` | `Y7: 2` | +| Tend | 4,060 | 2,625 | 1,411 | 2,370 | 741 | `+H1 − H6 + H7` | `Y7: 2` | + +P raises the private zero, copy and erase counts from 8 to 9 each. + +## 2. Obstruction + +**Class Z_c.** A word is in Z_c when it meets all of these conditions: + +1. it keeps every published ADD and copy (registers and coefficients) in + published relative order, except that the delivering ADD 2797 may sit + anywhere in its commutation window. That window is #3532's, bounded by + `D17`'s writes at 2497 and 3613, and holds 1,116 placements; +2. it inserts at least one correction ADD between `X0` and `Y7`; +3. transports of non-private registers may be inserted, removed or + retargeted; +4. every endpoint frame is kept; +5. `C`'s published events are kept. + +E, Erow and Tend are in Z_c, and so are R0 plus T, S or Trow. + +**Lemma 1 (parity; as in #3532 and #3601).** All 280 non-private registers sit +at their rank floor on the published word (checked). Over a nested path, mass +minus floor is even. So in Z_c each non-private register's added mass is a +non-negative even integer. It is zero exactly when the register's path is +monotone. + +**Lemma 2 (least frames).** Fix a placement and suppose the non-private paths +are monotone. A forward sweep starts from the initial frames. At each ADD +between non-private registers it sets both frames to their join, and at the +correction ADD it joins `X0` and `Y7`. `C` and any register declared free are +skipped, which only removes constraints. Every feasible repair has frames that +contain the sweep's. So the placement is infeasible if any swept frame leaves +its register's final frame. Dropping an ADD from the sweep, or freeing a +register, also only removes constraints. An infeasible verdict therefore +survives adding the dropped ADD back at any position. + +**Forcing chain.** `X0`'s forced rank is 2 at event 840 (`G25 += 2·X0`), 6 at +1074 (`G18 −= 2·X0`), 7 at 1311, 8 at 1485, and 9 from 1690. At 1074 the swept +frame is `[256,128,64,32,8,3]`, which is not inside `F7`. The cause is `X7`'s +head `387`. It reaches `G18` along `616: X7–G11`, `679: G11–X20` and +`1070: X20–G18` (earliest time-respecting chain), and it reaches `X0` at +`1074: G18–X0`. `G[7,7] = 2` is even, so the binary pairing of `387` with +`Y7`'s root is even and `387 ∉ F7`. Of the 56 source heads outside `F7`, all +of which have even `G[7,s]`, `X7`'s is the only one that reaches `X0` by 1074. + +**Theorem 1.** No member of Z_c has zero added non-private rank mass. The +minimum added rank mass over Z_c is exactly 2, attained by Tend and by E and +Erow (each +2 over the published word). + +*Proof.* Drop the delivering ADD from the sweep. The outcome is then constant +between consecutive `X0`/`Y7` ADD events, which leaves 18 insertion classes. +`verify.py` and `independent.py` sweep each one with the meeting +`frame_X0(u) = frame_Y7(u)` added: + +- **`u ≤ 841` (4 classes).** The meeting puts `232` into `Y7` from `u` on. + `Y7`'s updates then push it into `Q1`/`Q4` (events 19 and 20) or `D5` + (event 2013). The sweep fails at `Y8` at event 22, 23 or 2014. +- **`u ≥ 1075` (14 classes).** The merged frame contains `387`, so the sweep + fails at `u`, at `Y7`. + +By Lemma 2 each verdict holds for every placement of the delivering ADD. Extra +correction ADDs, as in Erow and Trow, only add constraints. As a cross-check, +the 19 published-order classes, which include 2798, are all obstructed. By +Lemma 1 the minimum is at least 2, and Tend, E and Erow attain 2. ∎ + +**Theorem 2 (joint, relocated).** Among words in Z_c whose delivering ADD runs +in a chart spanning `232`, the minimum added rank mass is exactly 2. R1+E +attains it. + +*Proof.* The lower bound follows from Theorem 1. R1+E co-hosts at 3611 (FULL) +and adds 2 over the published word. ∎ + +**Theorem 3 (joint, order-preserving).** Restrict Z_c to words that keep the +delivering ADD at 2797, with a chart spanning `232`, and add no private +lifetime. Every such word has added non-private rank mass at least 4. R0+T and +R0+S attain exactly 4. + +*Proof.* By Lemma 1, a word with non-private added mass 2 has exactly one +non-monotone non-private register `r`. Free `r` (and `C`) in the sweep. The +co-hosting constraint joins `Y7`, `D17` and `232` at 2797. + +- With nothing free, the co-hosting sweep fails, as in #3532. +- Free each of the 280 registers in turn. The co-hosting sweep still fails for + every choice except `r = D17`. +- With `D17` free, adding the correction meeting at any of the 19 + published-order classes fails again: at `Y8` for `u ≤ 841` and at `Y7` for + `u ≥ 1075`. + +So no single non-monotone register suffices, and the non-private added mass is +at least 4. ∎ + +**Co-host discount.** Tend adds 2 on the published word. + +- At R0's cut, T adds 2, so the discount is 0. +- At R1's co-hosted update, E adds 0, so the discount is 2. + +**Private route.** Let Z_cᴾ be Z_c with the correction ADD replaced by one +added private lifetime: zero, copy from `X0` at time `t`, transports, ADD into +`Y7` at time `t′`, erase. + +- If any non-private register adds mass, that costs at least 2. +- Otherwise `C`'s path costs at least 1 unless its copy chart equals its + delivery chart. + - For `t ≥ 1075`, the copy chart contains `387 ∉ F7`. + - For `t ≤ 1074`, the lifetime must end before `C`'s published lifetimes + start at 2461. Then `Y7` hosts `232` from `t′ < 2461` on. All 5 such + delivery classes fail the sweep at `Y8`, with the delivering ADD dropped. + +So the minimum over Z_cᴾ is exactly 1. P on R0 adds 1 over R0. The same route +at the published end cut would add 1 over the published word. P's +1 relies on +the inherited private-copy discard. + +## Controls + +`test_package.py` copies the package and its six pinned main inputs into a +temporary tree and runs both scanners there under `-O`. The clean tree must +pass and stay byte-identical. Eighteen mutations must be rejected by both +scanners: + +- seven certificate fields (T bill, E per-register mass, forcing head, exit + event, one strict-sweep row, the co-host rescue list, the R1 discount); +- a duplicate JSON key; +- a witness byte flip; +- a byte flip in the vendored #3532 certificate; +- a phase flip in a new recipe; +- T with a wrong coefficient, and T with an undercharged lift; +- S with the ADD in the wrong chart, and S with an unrestored source; +- P with an unclosed private lifetime; +- E with the ADD in `A3` (no common chart), and E with the wrong sign. + +## Limits + +- This covers one entry, one target row and the charts of two repairs of one + finite word. It does not price the other 103 rows, global hosting, idle + children or precision. It does not supply a supplier and does not change κ. +- Z_c keeps every published ADD and coefficient. A fused correction that + retunes existing deliveries is outside it. +- Theorem 3 bounds non-private mass for strict words. With P's inherited + private-copy discard, R0+P reaches 3. +- The joint minimum with an added private lifetime is between 1 and 2. It + equals 1 only if a zero-mass co-hosting relocation exists in #3532's 247 + late slots, which is #3532's open question 1. +- R0 and R1 come from open #3532. If #3532's head changes, the vendored pins + must be refreshed. +- `H_r` is left symbolic. diff --git a/research/p104-flag1-side-correction-bill/README.md b/research/p104-flag1-side-correction-bill/README.md new file mode 100644 index 0000000000..1c71626678 --- /dev/null +++ b/research/p104-flag1-side-correction-bill/README.md @@ -0,0 +1,158 @@ +# Flag 1's `I − G/2` entry rides free on #3532's relocated co-host, but costs +2 at its order-preserving one + +**Exact bill plus a sharp obstruction. No new exponent.** + +Open [#3532](https://github.com/CrocSwap/integer-mult-bounds/pull/3532) gives +two repairs of the published P104 word that co-host flag 1's basis head `232` +at `Y7`'s delivering update (`Y7 += D17/4`, published event 2797): + +- R0 keeps the published order and runs the ADD in `A3 = [95,486,232]`; +- R1 relocates it into `D17`'s full-chart window (new index 3611). + +Each costs +2 rank mass. #3532 leaves the `I − G/2` side correction open. Open +[#3601](https://github.com/CrocSwap/integer-mult-bounds/pull/3601) priced flag +43's entry at #3508's co-hosted cut and found a co-host discount of 0. This +package prices flag 1's entry at both of #3532's co-hosted charts. It cites +#3532, #3601 and [#3451](https://github.com/CrocSwap/integer-mult-bounds/pull/3451) +without re-deriving R0, R1 or the published chronology. #3532's two input files +are vendored byte-identically from its head (see [PROOF.md](PROOF.md)). + +## The entry + +Flag 1's entry is `(t, s) = (7, 0)`. `G[7,0] = = −1`, so the channel +leaves `X0` in `Y7` with coefficient `−1/2`, all of it delivered at 2797. The +`I − G/2` entry is `+1/2` (the opposite sign from flag 43's `−1/2`). Applying it +leaves `Y7` with `X0` coefficient `0`. `Y7` is never read, so no other row +changes. + +## Result + +| Word | Base | Correction | Δ events | Δ ADDs | Δ transports | Δ rank vs base | Δ rank vs published | +|---|---|---|---:|---:|---:|---:|---:| +| **E** | R1 | one ADD `Y7 += X0/2` in FULL right after the relocated delivering ADD | +1 | +1 | 0 | **0** | **+2** | +| **Erow** | R1 | E carrying all 48 off-diagonal entries `−G[7,s]/2` of row 7 | +48 | +48 | 0 | **0** | +2 | +| **T** | R0 | `Y7: A3→FULL`, ADD in FULL, `Y7: FULL→F7` | +2 | +1 | +1 | **+2** | +4 | +| **S** | R0 | R0's transport, then `X0: FULL→F7`, ADD, `X0: F7→FULL` | +3 | +1 | +2 | **+2** | +4 | +| **P** | R0 | one private lifetime: zero `C`, copy `X0`, `C: FULL→F7`, ADD, erase | +5 | +1 | +1 | +1 | +3 | +| **Trow** | R0 | T carrying all 48 row-7 entries | +49 | +48 | +1 | +2 | +4 | +| **Tend** | published | end-cut control: `Y7: A2→FULL`, ADD, `Y7: FULL→F7` | +2 | +1 | +1 | +2 | +2 | + +Here `F7` is `Y7`'s final rank-8 frame. In R1, `Y7` is already in FULL at the +relocated delivering ADD, and so is `X0`, so E needs no transport. In R0, `Y7` +sits in the rank-3 chart `A3` until its terminal transport, which is where T, S +and P act. + +The published `check_native.validate()` runs unchanged on all seven words with +the inserted coefficients set to `0`. It passes every native edge, including +three newly lowered recipes (`A3→FULL`, `A2→FULL`, `F7→FULL`), all 208 endpoint +adapters, all 280 framed rows and the restoration of the 72 dirty helpers. On +each real word the same checker fails only at +`full physical boundary endpoint Y7`. Exact rational replay confirms that `Y7` +is the only row that changes: + +- in E, T, S, P and Tend it changes by exactly `+1/2 X0`; +- in Erow and Trow, `Y7`'s final row becomes exactly `y7 + x7`, the identity row. + +**Co-host discount.** On the published word, the end-cut correction Tend +costs +2. + +- At R0's chart `A3` the correction also costs +2, so the discount is **0**, + as for flag 43. +- At R1's full chart it costs 0, so the discount is **2**. + +## Obstruction + +**Forcing chain.** Event 1074 is `G18 −= 2·X0`. By then the head `387` of `X7`, +the target's own source, has reached `G18` along the time-ordered chain +`X7 –616– G11 –679– X20 –1070– G18`. In any repair where those registers add no +rank, `X0`'s frame contains `387` from event 1074 on. From event 1690 it is the +full chart. Since `G[7,7] = 2` is even, `387` is outside `F7`. Of the 56 source +heads outside `F7`, `X7`'s is the only one that reaches `X0` by 1074. + +**Strict correction.** Take the class that: + +- keeps every published ADD; +- lets the delivering ADD sit anywhere in its 1,116-slot window; +- inserts one correction ADD between `X0` and `Y7`; +- moves transports freely; +- keeps every endpoint frame and `C`'s published events. + +No member of this class has zero added rank mass. A least-frame sweep with the +delivering ADD dropped checks 18 insertion classes. Dropping the ADD only +removes constraints, so the sweep covers every placement of it. + +- For the 4 classes up to event 841, the meeting puts `232` into `Y7` early. + `Y7`'s own updates then push it into `Y8`, at event 22, 23 or 2014. +- For the 14 classes from 1075 on, the merged frame contains `387` and leaves + `F7` at once. + +Each register's added mass is even, so the strict minimum is exactly **2**. +Tend and R1+E attain it. + +**Joint co-hosting and correction.** + +- **With relocation:** the joint minimum is **2**, attained by R1+E. It cannot + be lower, because the correction alone already costs 2. +- **Order-preserving:** if the delivering ADD stays at 2797 and co-hosts, the + joint non-private minimum is **4**, attained by R0+T and R0+S. A joint +2 + would leave exactly one register non-monotone. The census rules that out: + - letting any single one of the 280 non-private registers move freely still + blocks co-hosting, except for `D17`; + - with `D17` free, all 19 correction classes stay blocked. + +So for flag 1, co-hosting and correcting can share one +2 excursion, but only +when the delivering ADD is relocated (`Y7`'s lift to FULL pays for both). +Order-preserving co-hosting cannot share it. + +**Private route.** P relies on the inherited private-copy contract, under which +`C` is discarded while still holding a copy. Under that contract, the cheapest +added private lifetime costs exactly 1. Copies taken after event 1074 carry +`387`. Copies taken earlier must be delivered before `C`'s published lifetimes +start at 2461, and all 5 such delivery classes are blocked at `Y8`. + +Selected κ stays `0.001672660197076918`. Details and limits are in +[PROOF.md](PROOF.md). + +## Reproduce + +```sh +python3.12 -I -B research/p104-flag1-side-correction-bill/verify.py +python3.12 -I -O -Werror -B research/p104-flag1-side-correction-bill/verify.py +python3.12 -I -O -Werror -B research/p104-flag1-side-correction-bill/independent.py +python3.12 -I -O -Werror -B research/p104-flag1-side-correction-bill/test_package.py +python3.12 -B scripts/research_package.py --package research/p104-flag1-side-correction-bill +``` + +`verify.py` is read-only. It loads the pinned `check_native.py` by path, and +its admission checks go through `need()`, so they still fire under `-O`. It +takes about one minute. `independent.py` imports neither `verify.py` nor the +native checker. `test_package.py` corrupts temporary copies and checks that +both scanners reject all 18 corruptions. `build.py` is the producer and is not +part of the replay. + +## Credit + +Credit #3532 for R0, R1 and the delivering-update window (vendored inputs, +cited only), #3451 for flag 1's chronology, and #3601 and #3508 for the +side-correction bill format, class Z and the least-frame sweep reused here. +Credit `research/p104-side-correction-rank-obstruction` for the end-cut +invoices. Credit Nick Petalas / #2981 for the flag matching. Credit the reviewed +#1991 native channel (Chafik Boukhalfa) for the witness, checker and compiler, +and Rohan Arun / PR1972 for the scalar channel. Prepared by Wentao Li with +substantial AI assistance. + +## Open next questions + +1. Is there a co-hosted and corrected word for flag 1 with joint added mass 1? + It would need a zero-mass late relocation (#3532's open question 1) plus a + private route like P, so it is open exactly when that question is. +2. Does every other row with a present-head flag need +2 for its correction? + Flag 43 and flag 1 both do, each through a different forced head. Running + this sweep over all `(t, s)` with `G[t,s] ≠ 0` would decide whether strict + per-target corrections cost 208 in total. +3. Which repair is cheaper under the repo's actual per-rank weights: R1+E + (profile `H8 − H6`) or the uncorrected R0 (profile `−H1 + 2H2 + H5 − H6`)? + With relocation the correction adds no rank, so it is now part of that + comparison. + +[TASK.json](TASK.json) gives first steps and blockers. diff --git a/research/p104-flag1-side-correction-bill/SOURCES.json b/research/p104-flag1-side-correction-bill/SOURCES.json new file mode 100644 index 0000000000..d4413cfadd --- /dev/null +++ b/research/p104-flag1-side-correction-bill/SOURCES.json @@ -0,0 +1,151 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "requested_base_commit": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "base_note": "The requested pin is an ancestor of the base. The base contains merged #3508 and #3451. #3532 (an input) is open, so its two input files are vendored byte-identically under inputs/pr3532/ from its head 8fecbf7df; the head: provenance rows bind those bytes, and both scanners check the vendored SHA-256.", + "vendored": [ + { + "path": "research/p104-flag1-side-correction-bill/inputs/pr3532/CERTIFICATE.json", + "from": "head:8fecbf7df7b48c9004bd10a0da6a81f33d455737:research/p104-flag1-head-step-repair/CERTIFICATE.json", + "sha256": "5f29955e692d3fdb628ab0562c87defd21318c31cc2a8cafd6693f8004404359" + }, + { + "path": "research/p104-flag1-side-correction-bill/inputs/pr3532/REPAIR-RECIPES.json", + "from": "head:8fecbf7df7b48c9004bd10a0da6a81f33d455737:research/p104-flag1-head-step-repair/REPAIR-RECIPES.json", + "sha256": "13d2b2f45d75697d137aca1baf953b2bdf482bc8b02da6887ebb492f18470209" + } + ], + "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 coefficient-0 corrected word" + }, + { + "path": "research/p104-native-channel/vendor/native_verify.py", + "usage": "input", + "git_blob": "2c209dfa9cfade3bc20ac5fc9d876b433a147f8c", + "sha256": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38", + "credit": "Independent native interpreter used by check_native.py and by independent.py" + }, + { + "path": "research/p104-joint-unit-flags/CERTIFICATE.json", + "usage": "input", + "git_blob": "0fa7d2d40566e92f3ea1539723abf438ba65adb8", + "sha256": "a98126428a8da6eae91c50afcc42e014a284c82b554ef77e5b3a34fc6d228128", + "credit": "Nick Petalas, PR #2981 flag matching (flag 1 identity)" + }, + { + "path": "research/p104-flag1-head-step-repair/CERTIFICATE.json", + "usage": "provenance", + "git_blob": "80c35a9f6743b91cadd14224de6a385b136bdc3e", + "sha256": "5f29955e692d3fdb628ab0562c87defd21318c31cc2a8cafd6693f8004404359", + "pin": "head:8fecbf7df7b48c9004bd10a0da6a81f33d455737:research/p104-flag1-head-step-repair/CERTIFICATE.json", + "credit": "#3532 R0/R1 splices (open leave-alone prior; vendored byte-identically as inputs/pr3532/CERTIFICATE.json, cited, not re-derived)" + }, + { + "path": "research/p104-flag1-head-step-repair/REPAIR-RECIPES.json", + "usage": "provenance", + "git_blob": "18e2a0d1090c15af38597eeeeb4fa1ee365ed734", + "sha256": "13d2b2f45d75697d137aca1baf953b2bdf482bc8b02da6887ebb492f18470209", + "pin": "head:8fecbf7df7b48c9004bd10a0da6a81f33d455737:research/p104-flag1-head-step-repair/REPAIR-RECIPES.json", + "credit": "#3532 new-edge recipes (vendored byte-identically as inputs/pr3532/REPAIR-RECIPES.json; FULL->F7 and [95]->FULL reused)" + }, + { + "path": "research/p104-flag1-head-step-repair/README.md", + "usage": "provenance", + "git_blob": "80b16f99b0c3ae62447aa14388719549e3dea8d3", + "sha256": "7faadcd1407c59b39eca6218d743c721fc004d312f43af11a8a4901c4b2e0c3b", + "pin": "head:8fecbf7df7b48c9004bd10a0da6a81f33d455737:research/p104-flag1-head-step-repair/README.md", + "credit": "#3532 statement of R0/R1, the +2 co-hosting bill and the late-slot open question" + }, + { + "path": "research/p104-flag43-side-correction-bill/README.md", + "usage": "provenance", + "git_blob": "f11056d48c71d2203a77499abe8a517fa7b89514", + "sha256": "8ddaaf0c028f44dff042d17954baa00fd34267dd3f9aba0a4c96db330a05f981", + "pin": "head:26394881f0a183ca0df3d986ec58aa56900ada6c:research/p104-flag43-side-correction-bill/README.md", + "credit": "#3601 flag-43 side-correction bill (format, class Z, least-frame sweep, co-host discount 0); compared, not re-run" + }, + { + "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 three 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, owned private lifetimes, paid rank per transport" + }, + { + "path": "research/p104-present-head-flag1-audit/README.md", + "usage": "provenance", + "git_blob": "48e105431a55f1a59f30633bad3287d888d1aef2", + "sha256": "5b62f77b4db9a6124aceb2f9df487242f50fff93ecb5daf3d87b3a02f586d49c", + "pin": "base_commit:research/p104-present-head-flag1-audit/README.md", + "credit": "#3451 flag-1 chronology (leave-alone prior; cited only)" + }, + { + "path": "research/p104-flag43-head-step-repair/README.md", + "usage": "provenance", + "git_blob": "37f19da438b2a7e0b1ffb401de50df8a4323efca", + "sha256": "5d63d2a0a6842e182ba0dc7e9984b1ef66bae1c51b34fa732b380dbf83465cb6", + "pin": "base_commit:research/p104-flag43-head-step-repair/README.md", + "credit": "#3508 head-step repair method and class Z (merged; cited only)" + }, + { + "path": "research/p104-side-correction-rank-obstruction/README.md", + "usage": "provenance", + "git_blob": "7266bdce51f11bf1ee646b34516b79b76e939b33", + "sha256": "5a54ed54cae2cd08517f787e4085f8a3dfeda6c03a330e9e8e3bc88c01158f7a", + "pin": "base_commit:research/p104-side-correction-rank-obstruction/README.md", + "credit": "Prior end-cut side-correction invoices (+2 rank per target); compared, not re-run" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0", + "pin": "base_commit:docs/research/agent-task-catalog.json", + "credit": "Priority revision 6 task catalogue at the pinned base" + } + ] +} diff --git a/research/p104-flag1-side-correction-bill/TASK.json b/research/p104-flag1-side-correction-bill/TASK.json new file mode 100644 index 0000000000..7e733a6c22 --- /dev/null +++ b/research/p104-flag1-side-correction-bill/TASK.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 6, + "selected_kappa": "0.001672660197076918", + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "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 the flag-1 entry of the I - G/2 side correction (Y7 += -G[7,0]/2 X0 = +1/2 X0) at both co-hosted charts of open #3532: R0's order-preserving chart [95,486,232] (correction at R0's terminal Y7 transport) and R1's relocated full chart (correction next to the relocated delivering ADD). Build and natively validate seven words (T, S, P, Trow on R0; E, Erow on R1; end-cut control Tend on the published word), give exact bills, prove that no zero-added-mass placement of the correction exists at any of 18 insertion classes for any of the 1,116 placements of the delivering ADD (strict minimum 2), and prove the joint co-hosting-plus-correction minimum: 2 with relocation (R1+E), 4 for order-preserving strict words (R0+T, R0+S).", + "scope_change_reason": "#3532 (open) co-hosts flag 1's head at its delivering update via R0/R1 at +2 rank mass and leaves the I - G/2 side correction unpriced; #3601 (open) priced flag 43's entry at #3508's cut and reported co-host discount 0. This package answers the same question for flag 1's entry and row at both #3532 charts. It cites #3532/#3601/#3451 as leave-alone priors, vendors #3532's two input files byte-identically from its head, and does not re-derive R0, R1 or the published chronology.", + "bottleneck_link": "For flag 1 the side correction and head co-hosting can share one +2 excursion, but only through relocation: R1 already lifts Y7 into the full chart where X0 lives, so the entry costs 0 there (co-host discount 2), while at R0's order-preserving chart it costs +2 (discount 0, as for flag 43) and the order-preserving joint minimum is 4. The strict correction alone still needs +2 because X7's own head 387 (outside Y7's final hyperplane) is forced into X0 at event 1074 via G11/X20/G18. Neither result is a supplier.", + "budget_minutes": 60, + "stop_rule": "Stop after flag 1: one entry, one target row, the charts of #3532's R0 and R1, seven validated words, the zero-mass obstruction over all insertion classes and delivering-ADD placements, and the single-register joint census. Do not touch flags 0, 9 or 43, the other 103 target rows, global hosting, precision or kappa.", + "outcome": "completed", + "evidence": "Flag-1 entry: G[7,0]=-1, so I-G/2 needs +1/2 X0 in Y7. R1-based E: one ADD in the full chart after R1's relocated delivering ADD: +1 event, +1 ADD, 0 transports, 0 rank vs R1 (+2 vs published); Erow carries all 48 off-diagonal entries at 0 rank, Y7's row becomes y7+x7. R0-based T: Y7 A3->FULL (6), ADD, FULL->F7 (1): +2 events, +1 ADD, +1 transport, +2 rank (profile H1-H5+H6); S: X0 FULL->F7->FULL detour, +2 rank (2H1); P: one private lifetime, +1 rank; Trow: 48 ADDs on T's lift, +2 rank. Tend on the published word: +2 rank. The unchanged check_native.validate() passes all seven coefficient-0 words (three newly lowered recipes A3->FULL, A2->FULL, F7->FULL; 208 adapters; 280 framed rows; 72 dirty helpers) and rejects each real word only at 'full physical boundary endpoint Y7'; exact replay changes only Y7. Co-host discount 0 at R0, 2 at R1. Obstruction: X7's head 387 (G[7,7]=2, outside F7) reaches X0 at 1074 via 616 X7-G11, 679 G11-X20, 1070 X20-G18; least-frame sweep with the delivering ADD dropped blocks all 18 insertion classes (u<=841 at Y8; u>=1075 at Y7), hence every one of 1,116 delivery placements; strict minimum 2 (Tend, R1+E). Joint: relocation minimum 2 (R1+E); order-preserving strict non-private minimum 4 (only D17 rescues co-hosting alone, and with D17 free all 19 correction classes stay blocked). Private route minimum 1 (5/5 early deliveries blocked). Selected kappa unchanged.", + "author": "Wentao Li", + "ai_assistance": "Substantial AI assistance for derivation, implementation, checking and writing.", + "no_new_kappa": true, + "open_questions": [ + { + "question": "Is there a co-hosted and corrected flag-1 word with joint added mass 1 (zero-mass late relocation plus a private-copy correction)?", + "why_it_matters": "The strict joint minimum is 2 with relocation; with an added private lifetime the lower bound is only 1. Closing the gap decides whether co-hosting can ever be cheaper than the end-cut correction alone.", + "first_step": "Combine #3532's late-slot relaxed sweep (247 slots after 3366) with this package's private-route sweep, keeping C's published lifetimes, and test whether any slot admits a monotone non-private schedule.", + "blocked_by": "#3532's open question 1 (no zero-mass construction in the late window is known)." + }, + { + "question": "Does every present-head target row need +2 for its strict side-correction entry?", + "why_it_matters": "Flags 43 and 1 both need +2, through different forced heads (X12's 131 via G9; X7's own 387 via G11/X20/G18). If every row does, strict per-target corrections cost 208 rank mass in total, matching the end-cut invoice.", + "first_step": "Run this package's sweep() for every (target, source) pair with G[t,s] != 0 on the published word and record the first forcing source head outside the target's final hyperplane.", + "blocked_by": "Flag 9 is deferred elsewhere; this package treats flag 1 only." + }, + { + "question": "Under the repo's actual per-rank weights, is R1+E (profile H8-H6 over published, correction included) cheaper than R0 alone or the published word plus Tend?", + "why_it_matters": "With relocation the correction is free, so R1+E is a complete co-hosted and corrected entry at the parity floor; whether it beats the end-cut Tend (H1-H6+H7) depends on H.", + "first_step": "Evaluate H8-H6 against H1-H6+H7 under the cost model used by the selected record's transport pricing.", + "blocked_by": "H_r is symbolic in the native channel package." + } + ] +} diff --git a/research/p104-flag1-side-correction-bill/VERIFY.json b/research/p104-flag1-side-correction-bill/VERIFY.json new file mode 100644 index 0000000000..63663bdd33 --- /dev/null +++ b/research/p104-flag1-side-correction-bill/VERIFY.json @@ -0,0 +1,52 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "research/p104-native-channel/inputs/P104-FIXTURE.json", + "research/p104-native-channel/NATIVE-RECIPES.json.gz", + "research/p104-native-channel/check_native.py", + "research/p104-native-channel/vendor/native_verify.py", + "research/p104-joint-unit-flags/CERTIFICATE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Builds #3532's R0 and R1 from the vendored pinned splices, applies corrections T, S, P, Trow (R0), E, Erow (R1) and the end-cut control Tend (published), runs the published check_native.validate() unchanged on each coefficient-0 word (native edges incl. three committed new-edge recipes, 208 endpoint adapters, all 280 framed rows and dirty-helper restorations), replays the real words with exact rational rows, confirms the unchanged checker rejects each real word only at Y7's endpoint, recomputes bills, profiles, the X7->G11->X20->G18->X0 forcing chain, the least-frame sweep over 18 insertion classes with the delivering ADD dropped (plus 19 published-order classes and 5 early private deliveries), and the single-register order-preserving joint census, and requires equality with CERTIFICATE.json" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 180, + "checks": "Separately written replay with XOR-closure frames and exact rational rows: common-chart ADD/copy, nested transports paying their gap, owned private lifetimes, endpoint frames; base target rows equal G/2; each correction changes only Y7 by exactly +1/2 X0 (row variants: y7+x7); even non-private added mass; E/Erow share the full chart with X0 at zero added rank; direct native check of the three new recipes; closure-set sweeps for 18+19 strict classes, 5 early private deliveries, the 387 forcing fact and the co-host rescue census" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 600, + "checks": "Temp-tree clean pass with byte-identical tree; 18 rejections by both scanners under -O: certificate bill/obstruction/census/discount corruptions, duplicate JSON key, witness and vendored #3532 certificate byte flips, new-recipe phase corruption, wrong coefficient/sign, undercharged lift, wrong common chart (S and E), unrestored source and unclosed private lifetime" + } + ] +} diff --git a/research/p104-flag1-side-correction-bill/build.py b/research/p104-flag1-side-correction-bill/build.py new file mode 100644 index 0000000000..f7372a69a8 --- /dev/null +++ b/research/p104-flag1-side-correction-bill/build.py @@ -0,0 +1,83 @@ +#!/usr/bin/env python3 +"""Producer for CERTIFICATE.json and CORRECTION-RECIPES.json (not part of replay). + +Generates the corrections on #3532's R0 and R1 and the end-cut control on the +published word, lowers every transport edge that is absent from both the +published recipe set and #3532's REPAIR-RECIPES.json 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" + + +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", "CORRECTION-RECIPES.json"): + V.need(args.force or not (HERE / name).exists(), name + " exists") + root = V.ROOT + load("flag1_side_clifford_pin", root / V.NATIVE / "vendor/clifford_exact.py", CLIFFORD_SHA256) + co = load("flag1_side_native_compile", root / V.NATIVE / "compile.py", COMPILER_SHA256) + witness, fixture, recipes, _flags, repair, repair_recipes = V.load_inputs(root) + physical = V.physical_map(recipes) + program = witness["program"] + bases = {"published": program} + for name in ("R0", "R1"): + bases[name] = V.apply_splices(program, repair["repairs"][name]["splices"]) + spec = V.corrections(program, bases["R0"], bases["R1"], witness["final_frames"], V.ports(fixture)) + known = {(tuple(r["old"]), tuple(r["new"])) for r in recipes["transports"]} + known |= {(tuple(r["old"]), tuple(r["new"])) for r in repair_recipes} + new = {} + for base_name, group in spec.items(): + for name, item in group.items(): + prog = V.apply_splices(bases[base_name], item["splices"]) + for e in prog: + if e[0] != "transport": + continue + key = (physical(e[2]), physical(e[3])) + if key in known 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 the flag-1 corrections (T, S, P, Trow on #3532's R0; E, Erow on R1; Tend on the published word) that are absent from the published p104-native-channel recipe set and from #3532's REPAIR-RECIPES.json. 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, {"corrections": spec}, recs) + (HERE / "CORRECTION-RECIPES.json").write_text(json.dumps(payload, indent=1, sort_keys=True) + "\n") + (HERE / "CERTIFICATE.json").write_text(json.dumps(got, indent=2, sort_keys=True) + "\n") + print("WROTE", len(recs), "new recipes") + + +if __name__ == "__main__": + main() diff --git a/research/p104-flag1-side-correction-bill/independent.py b/research/p104-flag1-side-correction-bill/independent.py new file mode 100644 index 0000000000..787f4eb50b --- /dev/null +++ b/research/p104-flag1-side-correction-bill/independent.py @@ -0,0 +1,311 @@ +#!/usr/bin/env python3 +"""Independent replay of the flag-1 side-correction bill. + +Imports neither verify.py nor check_native.py. Frames are XOR-closed sets of +compressed labels. #3532's R0 and R1 and every corrected word are replayed with +exact rational rows under the channel rules (common-chart ADD and copy, nested +transports paying their frame gap, owned private lifetimes, endpoint frames). +The committed new-edge recipes are checked directly with the pinned +independent Gaussian interpreter. The forced-frame obstruction, the forcing +chain and the order-preserving joint census are recomputed by a separate +forward sweep over closure sets. Key receipts are compared with CERTIFICATE.json. +""" + +import gzip +import hashlib +import importlib.util +import itertools +import json +import sys +from fractions import Fraction +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" +PR3532 = f"{PKG}/inputs/pr3532" +PINS = { + f"{NATIVE}/inputs/LOWRANK-WITNESS.json": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e", + f"{NATIVE}/inputs/P104-FIXTURE.json": "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4", + f"{NATIVE}/NATIVE-RECIPES.json.gz": "a1c4d83d3d5fe1338e99b59272e8cf5d43244c33888597da340b2aa7fef5b3e8", + f"{NATIVE}/vendor/native_verify.py": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38", + "research/p104-joint-unit-flags/CERTIFICATE.json": "a98126428a8da6eae91c50afcc42e014a284c82b554ef77e5b3a34fc6d228128", + f"{PR3532}/CERTIFICATE.json": "5f29955e692d3fdb628ab0562c87defd21318c31cc2a8cafd6693f8004404359", +} +MARKER = ( + "PASS_P104_FLAG1_SIDE_CORRECTION_BILL_INDEPENDENT entry=(7,0) coefficient=+1/2 " + "strict_classes_obstructed=18/18(delivery_dropped)+19/19(published_order) early_private_obstructed=5/5 " + "forcing_head=387(X7) R0:T,S,Trow=+2rank P=+1rank R1:E,Erow=+0rank Tend=+2rank " + "joint_order_preserving_single_rescue=none rows_changed=Y7_only row7=identity new_recipes=3 no_new_kappa" +) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def strict(pairs): + out = {} + for k, v in pairs: + need(k not in out, "duplicate JSON key: " + str(k)) + out[k] = v + return out + + +def read(root, rel, gz=False): + raw = (root / rel).read_bytes() + if rel in PINS: + need(hashlib.sha256(raw).hexdigest() == PINS[rel], "pin: " + rel) + return json.loads(gzip.decompress(raw) if gz else raw, object_pairs_hook=strict) + + +def closure(vectors): + s = {0} + for v in vectors: + if v not in s: + s |= {x ^ v for x in s} + return frozenset(s) + + +def grow(s, vectors): + s = set(s) + for v in vectors: + if v not in s: + s |= {x ^ v for x in s} + return frozenset(s) + + +def dim(s): + return len(s).bit_length() - 1 + + +def splice(program, rows): + out = list(program) + for row in sorted(rows, key=lambda r: -r["published_range"][0]): + a, b = row["published_range"] + need(out[a:b] == row["published"], "splice anchor") + out[a:b] = row["events"] + return out + + +def gram_rows(fixture): + lines = set() + for i, j in itertools.combinations(range(8), 2): + for s in (-1, 1): + v = [0] * 8 + v[i], v[j] = 2, 2 * s + lines.add(tuple(v)) + for s in itertools.product((-1, 1), repeat=7): + if s.count(-1) % 2 == 0: + lines.add((1,) + s) + gone = {tuple(r) for r in fixture["F0"] + fixture["C"]} + ps = [r for r in sorted(lines) if r not in gone] + need(len(ps) == 104, "104 ports") + return lambda t, s: sum(x * y for x, y in zip(ps[t], ps[s])) // 4 + + +def replay(witness, program, watch=None): + frames = {n: closure(f) for n, f in witness["initial_frames"].items()} + rows = {n: {n: Fraction(1)} for n in witness["initial_frames"]} + paid, adds, private = {}, 0, {"zero": 0, "copy": 0, "erase": 0} + mass = {} + shared = [] + for i, e in enumerate(program): + op = e[0] + if op == "transport": + _, r, a, b, k = e + fa, fb = closure(a), closure(b) + need(frames[r] == fa, "transport starts at live frame") + need(fa <= fb or fb <= fa, "nested transport") + need(abs(dim(fb) - dim(fa)) == k and k > 0, "rank equals frame gap") + frames[r] = fb + paid[k] = paid.get(k, 0) + 1 + mass[r] = mass.get(r, 0) + k + elif op == "zero": + need(e[1] == "C" and "C" not in frames, "owned private zero") + frames["C"], rows["C"] = closure(e[2]), {} + private["zero"] += 1 + elif op == "erase": + need(frames.get("C") == closure(e[2]), "owned private erase") + frames.pop("C") + rows.pop("C") + private["erase"] += 1 + elif op == "copy": + need(not rows["C"] and frames["C"] == frames[e[2]] == closure(e[3]), "common-chart copy") + rows["C"] = dict(rows[e[2]]) + private["copy"] += 1 + else: + need(op == "add", "known opcode") + _, dst, src, a, f = e + need(dst != src and frames[dst] == frames[src] == closure(f), "common-chart add") + if watch and dst == watch[0] and src == watch[1]: + shared.append((i, dim(frames[dst]))) + for k, v in rows[src].items(): + z = rows[dst].get(k, Fraction(0)) + Fraction(a) * v + if z: + rows[dst][k] = z + else: + rows[dst].pop(k, None) + adds += 1 + need("C" not in frames, "private storage closed") + for n, f in witness["final_frames"].items(): + need(frames[n] == closure(f), "endpoint frame " + n) + return rows, {"events": len(program), "adds": adds, "transports": sum(paid.values()), + "rank_mass": sum(k * v for k, v in paid.items()), "profile": paid, + "private": private, "mass": mass, "shared": shared} + + +def lower_sweep(witness, program, inject=(), skip=(), free=()): + free = {"C"} | set(free) + cur = {n: closure(f) for n, f in witness["initial_frames"].items()} + fin = {n: closure(f) for n, f in witness["final_frames"].items()} + plan = {} + for u, regs, extra in inject: + plan.setdefault(u, []).append(([r for r in regs if r not in free], extra)) + for i in range(len(program) + 1): + for regs, extra in plan.get(i, ()): + m = closure(extra) + for r in regs: + m = grow(m, cur[r]) + for r in regs: + cur[r] = m + if not m <= fin[r]: + return i, r + if i == len(program): + return None + e = program[i] + if i in skip or e[0] != "add" or free & {e[1], e[2]}: + continue + a, b = e[1], e[2] + m = cur[a] if cur[b] <= cur[a] else cur[b] if cur[a] <= cur[b] else grow(cur[a], cur[b]) + cur[a] = cur[b] = m + for r in (a, b): + if not m <= fin[r]: + return i, r + + +def main(root=ROOT): + witness = read(root, f"{NATIVE}/inputs/LOWRANK-WITNESS.json") + fixture = read(root, f"{NATIVE}/inputs/P104-FIXTURE.json")["section4_explicit_P104"] + recipes = read(root, f"{NATIVE}/NATIVE-RECIPES.json.gz", gz=True) + flags = read(root, "research/p104-joint-unit-flags/CERTIFICATE.json") + repair = read(root, f"{PR3532}/CERTIFICATE.json") + cert = json.loads((HERE / "CERTIFICATE.json").read_bytes(), object_pairs_hook=strict) + new = json.loads((HERE / "CORRECTION-RECIPES.json").read_bytes(), object_pairs_hook=strict)["recipes"] + raw = (root / NATIVE / "vendor/native_verify.py").read_bytes() + need(hashlib.sha256(raw).hexdigest() == PINS[f"{NATIVE}/vendor/native_verify.py"], "interpreter pin") + spec = importlib.util.spec_from_file_location("flag1_side_independent_native", root / NATIVE / "vendor/native_verify.py") + N = importlib.util.module_from_spec(spec) + spec.loader.exec_module(N) + + flag = flags["helpers"][1] + need((flag["source"], flag["target"], flag["basis"][0]) == (0, 7, 232), "flag 1") + G = gram_rows(fixture) + need(G(7, 0) == -1 and G(7, 7) == 2, "Gram entries") + program = witness["program"] + f7 = closure(witness["final_frames"]["Y7"]) + need(232 in f7, "head inside F7") + bases = {"published": program} + for name in ("R0", "R1"): + bases[name] = splice(program, repair["repairs"][name]["splices"]) + rows_b, bill_b = {}, {} + for name, prog in bases.items(): + rows_b[name], bill_b[name] = replay(witness, prog) + for t in range(104): + want = {"Y%d" % t: Fraction(1)} + want.update({"X%d" % s: Fraction(G(t, s), 2) for s in range(104) if G(t, s)}) + need(all(rows_b[n]["Y%d" % t] == want for n in bases), "base target rows G/2") + need([bill_b[n]["rank_mass"] for n in ("published", "R0", "R1")] == [2368, 2370, 2370], "base rank mass") + + iso = recipes["label_isometry"] + dual, orth = iso["compressed_dual_gram"], iso["orthonormal_basis_compressed"] + + def to_phys(x): + dx = sum((((row & x).bit_count()) & 1) << i for i, row in enumerate(dual)) + return sum((((v & dx).bit_count()) & 1) << j for j, v in enumerate(orth)) + + phys = lambda f: closure(to_phys(x) for x in f) + for rec in new: + need(rec["rank"] == abs(len(rec["old"]) - len(rec["new"])) == rec["recipe"]["rank"], "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") + full = [1 << k for k in range(9)] + keys = {(closure(r["old"]), closure(r["new"])) for r in new} + want_keys = {(phys(witness["final_frames"]["Y7"]), phys(full)), (phys([95, 486, 232]), phys(full)), (phys([95, 486]), phys(full))} + need(keys == want_keys, "new edges are F7->FULL, A3->FULL and A2->FULL") + + want = {"T": ("R0", (2, 1, 1, 2)), "S": ("R0", (3, 1, 2, 2)), "P": ("R0", (5, 1, 1, 1)), + "Trow": ("R0", (49, 48, 1, 2)), "E": ("R1", (1, 1, 0, 0)), "Erow": ("R1", (48, 48, 0, 0)), + "Tend": ("published", (2, 1, 1, 2))} + for name, (base, (ev, ad, tr, rm)) in want.items(): + item = cert["corrections"][base][name] + prog = splice(bases[base], item["splices"]) + rows, b = replay(witness, prog, watch=("Y7", "X0")) + b0 = bill_b[base] + got = (b["events"] - b0["events"], b["adds"] - b0["adds"], b["transports"] - b0["transports"], b["rank_mass"] - b0["rank_mass"]) + need(got == (ev, ad, tr, rm), name + " added bill") + changed = sorted(k for k in rows_b[base] if rows[k] != rows_b[base][k]) + need(changed == ["Y7"], name + " changes only Y7") + if name.endswith("row"): + need(rows["Y7"] == {"Y7": Fraction(1), "X7": Fraction(1)}, name + " row 7 identity") + else: + need("X0" not in rows["Y7"], name + " entry applied") + diff = {k: rows["Y7"].get(k, 0) - rows_b[base]["Y7"].get(k, 0) for k in set(rows["Y7"]) | set(rows_b[base]["Y7"])} + need({k: v for k, v in diff.items() if v} == {"X0": Fraction(1, 2)}, name + " exact entry") + c = cert["bill"][name] + need([c["added_vs_base"][k] for k in ("events", "scalar_adds", "transport_occurrences", "rank_mass")] == [ev, ad, tr, rm], name + " certificate bill") + dm = {r: b["mass"].get(r, 0) - b0["mass"].get(r, 0) for r in set(b["mass"]) | set(b0["mass"])} + dm = {r: v for r, v in dm.items() if v} + need(all(v % 2 == 0 for r, v in dm.items() if r != "C"), name + " even non-private mass") + need(c["added_rank_by_register"] == dm, name + " per-register mass") + if name in ("E", "Erow"): + need(b["shared"] and all(d == 9 for _i, d in b["shared"]), name + " Y7 and X0 share the full chart") + need(not dm, name + " no added rank") + need(cert["bill"]["P"]["private_events"] == {"zero": 9, "copy": 9, "erase": 9}, "P lifetime") + + need(all(lower_sweep(witness, p) is None for p in bases.values()), "bases feasible") + d = 2797 + need(program[d] == ["add", "Y7", "D17", "1/4", [95, 486]], "published delivering ADD") + touch = lambda regs, skip: sorted({0} | {i + 1 for i, e in enumerate(program) + if i not in skip and e[0] in ("add", "copy") and set(regs) & {e[1], e[2]}}) + cuts = touch(("X0", "Y7"), {d}) + need(len(cuts) == 18, "18 classes without the delivering ADD") + blocked = [lower_sweep(witness, program, [(u, ("X0", "Y7"), ())], skip={d}) for u in cuts] + need(all(blocked), "no zero-mass correction for any delivery placement") + need([[u, list(x)] for u, x in zip(cuts, blocked)] == cert["obstruction"]["strict_first_obstruction"], "strict table") + pub_cuts = touch(("X0", "Y7"), set()) + pub_blocked = [lower_sweep(witness, program, [(u, ("X0", "Y7"), ())]) for u in pub_cuts] + need(len(pub_cuts) == 19 and all(pub_blocked), "published-order classes obstructed") + early = [u for u in touch(("Y7",), {d}) if u < 2461] + pblocked = [lower_sweep(witness, program, [(u, ("Y7",), (232,))], skip={d}) for u in early] + need(len(early) == 5 and all(pblocked), "early private deliveries obstructed") + + cur = {n: closure(f) for n, f in witness["initial_frames"].items()} + carriers = {"X7"} + for i, e in enumerate(program[:1075]): + if e[0] == "add" and "C" not in (e[1], e[2]): + if {e[1], e[2]} & carriers: + carriers |= {e[1], e[2]} + cur[e[1]] = cur[e[2]] = grow(cur[e[1]], cur[e[2]]) + if i == 1073: + need(cur["X0"] <= f7, "X0 inside F7 before 1074") + need(witness["initial_frames"]["X7"] == [387] and 387 not in f7, "X7 head outside F7") + need("X0" in carriers and 387 in cur["X0"] and not cur["X0"] <= f7, "387 reaches X0 by 1074") + ob = cert["obstruction"] + need(ob["forcing_source_head"] == [387] and ob["source_leaves_target_final_at"][0] == 1074, "certificate forcing") + + force = (d, ("Y7", "D17"), (232,)) + rescue = [r for r in sorted(witness["initial_frames"]) if lower_sweep(witness, program, [force], free=(r,)) is None] + need(rescue == ["D17"] == ob["order_preserving_cohost_single_register_rescues"], "only D17 rescues co-hosting") + for r in ((), ("D17",)): + need(all(lower_sweep(witness, program, [force, (u, ("X0", "Y7"), ())], free=r) for u in pub_cuts), + "joint order-preserving obstructed with %s free" % (r or "nothing")) + ec = cert["end_cut_comparison"] + need((ec["cohost_discount_R0"], ec["cohost_discount_R1"]) == (0, 2), "co-host discounts") + need(cert["selected_kappa"] == "0.001672660197076918" and cert["no_new_kappa"] is True, "kappa") + print(MARKER) + + +if __name__ == "__main__": + main(Path(sys.argv[1]).resolve() if len(sys.argv) > 1 else ROOT) diff --git a/research/p104-flag1-side-correction-bill/inputs/pr3532/CERTIFICATE.json b/research/p104-flag1-side-correction-bill/inputs/pr3532/CERTIFICATE.json new file mode 100644 index 0000000000..80c35a9f67 --- /dev/null +++ b/research/p104-flag1-side-correction-bill/inputs/pr3532/CERTIFICATE.json @@ -0,0 +1,1179 @@ +{ + "basis_head": 232, + "bill": { + "R0": { + "added_events": 1, + "added_rank_mass": 2, + "added_scalar_adds": 0, + "added_transport_occurrences": 1, + "distinct_native_edges": 742, + "dropped_native_edges": 2, + "endpoint_adapters": 208, + "events": 4059, + "formal_boundary_columns": 280, + "new_native_edges": 4, + "paid_profile": { + "1": 1073, + "2": 60, + "3": 86, + "4": 104, + "5": 49, + "6": 23, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "private_events_unchanged": true, + "profile_delta": { + "1": -1, + "2": 2, + "5": 1, + "6": -1 + }, + "rank_mass": 2370, + "register_mass_delta": { + "D17": 2 + }, + "scalar_adds": 2624, + "transport_occurrences": 1411 + }, + "R1": { + "added_events": 0, + "added_rank_mass": 2, + "added_scalar_adds": 0, + "added_transport_occurrences": 0, + "distinct_native_edges": 741, + "dropped_native_edges": 1, + "endpoint_adapters": 208, + "events": 4058, + "formal_boundary_columns": 280, + "new_native_edges": 2, + "paid_profile": { + "1": 1074, + "2": 58, + "3": 86, + "4": 104, + "5": 48, + "6": 23, + "7": 8, + "8": 9 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "private_events_unchanged": true, + "profile_delta": { + "6": -1, + "8": 1 + }, + "rank_mass": 2370, + "register_mass_delta": { + "Y7": 2 + }, + "scalar_adds": 2624, + "transport_occurrences": 1410 + }, + "published": { + "distinct_native_edges": 740, + "endpoint_adapters": 208, + "events": 4058, + "formal_boundary_columns": 280, + "paid_profile": { + "1": 1074, + "2": 58, + "3": 86, + "4": 104, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "rank_mass": 2368, + "scalar_adds": 2624, + "transport_occurrences": 1410 + } + }, + "claim_id": "p104-flag1-head-step-repair", + "flag_index": 1, + "forced_hosting": { + "head_closure_table": [ + { + "event": 19, + "first_obstruction": [ + "Y8", + 22, + "final frame excludes head" + ], + "must_change": 272, + "obstructions": 56, + "partner": "Q1", + "private_registers_forced": [] + }, + { + "event": 20, + "first_obstruction": [ + "Y8", + 23, + "final frame excludes head" + ], + "must_change": 268, + "obstructions": 56, + "partner": "Q4", + "private_registers_forced": [] + }, + { + "event": 2013, + "first_obstruction": [ + "Y8", + 2014, + "final frame excludes head" + ], + "must_change": 141, + "obstructions": 56, + "partner": "D5", + "private_registers_forced": [ + [ + "C", + 2465 + ] + ] + }, + { + "event": 2146, + "first_obstruction": [ + "Y8", + 2147, + "final frame excludes head" + ], + "must_change": 141, + "obstructions": 56, + "partner": "D17", + "private_registers_forced": [ + [ + "C", + 2465 + ] + ] + }, + { + "event": 2526, + "first_obstruction": [ + "Y8", + 2528, + "final frame excludes head" + ], + "must_change": 58, + "obstructions": 23, + "partner": "D5", + "private_registers_forced": [] + }, + { + "event": 2797, + "first_obstruction": [ + "Y8", + 2799, + "final frame excludes head" + ], + "must_change": 37, + "obstructions": 14, + "partner": "D17", + "private_registers_forced": [] + } + ], + "least_frame_order_preserving_infeasible": { + "19": [ + "Y0", + "Y1", + "Y101", + "Y102", + "Y103", + "Y11", + "Y13", + "Y14", + "Y16", + "Y19", + "Y21", + "Y22", + "Y23", + "Y25", + "Y28", + "Y3", + "Y30", + "Y31", + "Y32", + "Y33", + "Y35", + "Y36", + "Y38", + "Y40", + "Y42", + "Y45", + "Y47", + "Y49", + "Y52", + "Y54", + "Y56", + "Y58", + "Y59", + "Y6", + "Y61", + "Y63", + "Y65", + "Y68", + "Y70", + "Y72", + "Y74", + "Y75", + "Y77", + "Y8", + "Y80", + "Y82", + "Y84", + "Y86", + "Y88", + "Y90", + "Y92", + "Y93", + "Y94", + "Y95", + "Y97", + "Y99" + ], + "20": [ + "Y0", + "Y1", + "Y101", + "Y102", + "Y103", + "Y11", + "Y13", + "Y14", + "Y16", + "Y19", + "Y21", + "Y22", + "Y23", + "Y25", + "Y28", + "Y3", + "Y30", + "Y31", + "Y32", + "Y33", + "Y35", + "Y36", + "Y38", + "Y40", + "Y42", + "Y45", + "Y47", + "Y49", + "Y52", + "Y54", + "Y56", + "Y58", + "Y59", + "Y6", + "Y61", + "Y63", + "Y65", + "Y68", + "Y70", + "Y72", + "Y74", + "Y75", + "Y77", + "Y8", + "Y80", + "Y82", + "Y84", + "Y86", + "Y88", + "Y90", + "Y92", + "Y93", + "Y94", + "Y95", + "Y97", + "Y99" + ], + "2013": [ + "Y1", + "Y101", + "Y102", + "Y103", + "Y11", + "Y13", + "Y14", + "Y16", + "Y19", + "Y21", + "Y22", + "Y23", + "Y25", + "Y28", + "Y3", + "Y30", + "Y31", + "Y32", + "Y33", + "Y35", + "Y36", + "Y38", + "Y40", + "Y42", + "Y45", + "Y47", + "Y49", + "Y52", + "Y54", + "Y56", + "Y58", + "Y59", + "Y61", + "Y63", + "Y65", + "Y68", + "Y70", + "Y72", + "Y74", + "Y75", + "Y77", + "Y8", + "Y80", + "Y82", + "Y84", + "Y86", + "Y88", + "Y90", + "Y92", + "Y93", + "Y94", + "Y95", + "Y97", + "Y99" + ], + "2146": [ + "Y1", + "Y101", + "Y102", + "Y103", + "Y13", + "Y14", + "Y16", + "Y21", + "Y22", + "Y23", + "Y25", + "Y28", + "Y3", + "Y30", + "Y31", + "Y32", + "Y33", + "Y35", + "Y36", + "Y38", + "Y40", + "Y42", + "Y45", + "Y47", + "Y49", + "Y52", + "Y54", + "Y56", + "Y58", + "Y59", + "Y61", + "Y63", + "Y65", + "Y68", + "Y70", + "Y72", + "Y74", + "Y75", + "Y77", + "Y8", + "Y80", + "Y82", + "Y84", + "Y86", + "Y88", + "Y90", + "Y92", + "Y93", + "Y94", + "Y95", + "Y97", + "Y99" + ], + "2526": [ + "Y103", + "Y13", + "Y14", + "Y16", + "Y21", + "Y22", + "Y31", + "Y32", + "Y33", + "Y35", + "Y56", + "Y58", + "Y59", + "Y61", + "Y63", + "Y65", + "Y68", + "Y70", + "Y8", + "Y88", + "Y90", + "Y92", + "Y93" + ], + "2797": [ + "Y103", + "Y13", + "Y16", + "Y21", + "Y31", + "Y32", + "Y33", + "Y35", + "Y59", + "Y61", + "Y8", + "Y88", + "Y90", + "Y92" + ] + }, + "least_frame_relocation_scan": { + "obstructed_slots": 868, + "partner_row_writes_bounding_window": [ + 2497, + 3613 + ], + "relaxed_feasible_slots": 247, + "runs": [ + { + "after_published_first": 2497, + "after_published_last": 2525, + "infeasible": [ + "Y103", + "Y13", + "Y14", + "Y16", + "Y21", + "Y22", + "Y31", + "Y32", + "Y33", + "Y35", + "Y56", + "Y58", + "Y59", + "Y61", + "Y63", + "Y65", + "Y68", + "Y70", + "Y8", + "Y88", + "Y90", + "Y92", + "Y93" + ], + "infeasible_count": 23, + "slots": 29 + }, + { + "after_published_first": 2526, + "after_published_last": 2798, + "infeasible": [ + "Y103", + "Y13", + "Y16", + "Y21", + "Y31", + "Y32", + "Y33", + "Y35", + "Y59", + "Y61", + "Y8", + "Y88", + "Y90", + "Y92" + ], + "infeasible_count": 14, + "slots": 272 + }, + { + "after_published_first": 2799, + "after_published_last": 2802, + "infeasible": [ + "Y103", + "Y13", + "Y16", + "Y21", + "Y31", + "Y32", + "Y33", + "Y35", + "Y59", + "Y61", + "Y88", + "Y90", + "Y92" + ], + "infeasible_count": 13, + "slots": 4 + }, + { + "after_published_first": 2803, + "after_published_last": 2806, + "infeasible": [ + "Y103", + "Y16", + "Y21", + "Y31", + "Y32", + "Y33", + "Y35", + "Y59", + "Y61", + "Y88", + "Y90", + "Y92" + ], + "infeasible_count": 12, + "slots": 4 + }, + { + "after_published_first": 2807, + "after_published_last": 2810, + "infeasible": [ + "Y103", + "Y21", + "Y31", + "Y32", + "Y33", + "Y35", + "Y59", + "Y61", + "Y88", + "Y90", + "Y92" + ], + "infeasible_count": 11, + "slots": 4 + }, + { + "after_published_first": 2811, + "after_published_last": 2814, + "infeasible": [ + "Y103", + "Y31", + "Y32", + "Y33", + "Y35", + "Y59", + "Y61", + "Y88", + "Y90", + "Y92" + ], + "infeasible_count": 10, + "slots": 4 + }, + { + "after_published_first": 2815, + "after_published_last": 2816, + "infeasible": [ + "Y103", + "Y31", + "Y32", + "Y35", + "Y59", + "Y61", + "Y88", + "Y90", + "Y92" + ], + "infeasible_count": 9, + "slots": 2 + }, + { + "after_published_first": 2817, + "after_published_last": 2818, + "infeasible": [ + "Y103", + "Y31", + "Y32", + "Y59", + "Y61", + "Y88", + "Y90", + "Y92" + ], + "infeasible_count": 8, + "slots": 2 + }, + { + "after_published_first": 2819, + "after_published_last": 2820, + "infeasible": [ + "Y103", + "Y31", + "Y32", + "Y59", + "Y61", + "Y90", + "Y92" + ], + "infeasible_count": 7, + "slots": 2 + }, + { + "after_published_first": 2821, + "after_published_last": 3183, + "infeasible": [ + "Y103", + "Y31", + "Y59", + "Y61" + ], + "infeasible_count": 4, + "slots": 363 + }, + { + "after_published_first": 3184, + "after_published_last": 3187, + "infeasible": [ + "Y103", + "Y59", + "Y61" + ], + "infeasible_count": 3, + "slots": 4 + }, + { + "after_published_first": 3188, + "after_published_last": 3363, + "infeasible": [ + "Y103", + "Y59" + ], + "infeasible_count": 2, + "slots": 176 + }, + { + "after_published_first": 3364, + "after_published_last": 3365, + "infeasible": [ + "Y103" + ], + "infeasible_count": 1, + "slots": 2 + }, + { + "after_published_first": 3366, + "after_published_last": 3612, + "infeasible": [], + "infeasible_count": 0, + "slots": 247 + } + ], + "slots": 1115 + }, + "non_private_registers_at_rank_floor": 280 + }, + "head_cohosting": { + "R0": { + "cohosted_target_updates": [ + 2797 + ], + "delivering_update": 2797, + "delivering_update_event": [ + "add", + "Y7", + "D17", + "1/4", + [ + 95, + 486, + 232 + ] + ], + "source_delivery_into_target": [ + [ + 2797, + "D17", + "-1/2", + "-1/2" + ] + ], + "source_events_after_update": [ + 3643, + 3799, + 3851, + 3955 + ], + "source_frame_rank_at_update": 9, + "source_spans_head_at_update": true, + "target_updates": [ + 19, + 20, + 2013, + 2146, + 2526, + 2797 + ], + "update_chart_rank": 3 + }, + "R1": { + "cohosted_target_updates": [ + 3611 + ], + "delivering_update": 3611, + "delivering_update_event": [ + "add", + "Y7", + "D17", + "1/4", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + "source_delivery_into_target": [ + [ + 3611, + "D17", + "-1/2", + "-1/2" + ] + ], + "source_events_after_update": [ + 3642, + 3798, + 3850, + 3954 + ], + "source_frame_rank_at_update": 9, + "source_spans_head_at_update": true, + "target_updates": [ + 19, + 20, + 2013, + 2146, + 2526, + 3611 + ], + "update_chart_rank": 9 + }, + "partner_row_writes": [ + 2497, + 3613 + ], + "published_head_hosting_target_updates": [], + "published_source_delivery_into_target": [ + [ + 2797, + "D17", + "-1/2", + "-1/2" + ] + ], + "published_target_updates": [ + 19, + 20, + 2013, + 2146, + 2526, + 2797 + ], + "target_read_events": [] + }, + "no_new_kappa": true, + "pinned_main": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "repairs": { + "R0": { + "class": "order-preserving: every published event kept in published order with the same ADD registers and coefficients; one downward D17 transport inserted after the delivering ADD", + "rule": "D17 and Y7 enter the published 2797 chart plus the head (rank 3) at their last transports before 2797; D17 drops back to the published chart immediately after; Y7's terminal transport starts from the rank-3 chart", + "splices": [ + { + "events": [ + [ + "transport", + "D17", + [ + 486 + ], + [ + 95, + 486, + 232 + ], + 2 + ] + ], + "published": [ + [ + "transport", + "D17", + [ + 486 + ], + [ + 95, + 486 + ], + 1 + ] + ], + "published_range": [ + 2795, + 2796 + ] + }, + { + "events": [ + [ + "transport", + "Y7", + [ + 95 + ], + [ + 95, + 486, + 232 + ], + 2 + ] + ], + "published": [ + [ + "transport", + "Y7", + [ + 95 + ], + [ + 95, + 486 + ], + 1 + ] + ], + "published_range": [ + 2796, + 2797 + ] + }, + { + "events": [ + [ + "add", + "Y7", + "D17", + "1/4", + [ + 95, + 486, + 232 + ] + ], + [ + "transport", + "D17", + [ + 95, + 486, + 232 + ], + [ + 95, + 486 + ], + 1 + ] + ], + "published": [ + [ + "add", + "Y7", + "D17", + "1/4", + [ + 95, + 486 + ] + ] + ], + "published_range": [ + 2797, + 2798 + ] + }, + { + "events": [ + [ + "transport", + "Y7", + [ + 95, + 486, + 232 + ], + [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ], + 5 + ] + ], + "published": [ + [ + "transport", + "Y7", + [ + 95, + 486 + ], + [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ], + 6 + ] + ], + "published_range": [ + 3473, + 3474 + ] + } + ] + }, + "R1": { + "class": "relocation: the delivering ADD (with Y7's 2796 and 3473 transports) moves into D17's full-chart window between its lift at 3612 and its restoration at 3613; no event added or removed", + "rule": "Y7 lifts from [95] to the full chart, takes Y7 += D17/4 there, then drops to its final frame", + "splices": [ + { + "events": [], + "published": [ + [ + "transport", + "Y7", + [ + 95 + ], + [ + 95, + 486 + ], + 1 + ], + [ + "add", + "Y7", + "D17", + "1/4", + [ + 95, + 486 + ] + ] + ], + "published_range": [ + 2796, + 2798 + ] + }, + { + "events": [], + "published": [ + [ + "transport", + "Y7", + [ + 95, + 486 + ], + [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ], + 6 + ] + ], + "published_range": [ + 3473, + 3474 + ] + }, + { + "events": [ + [ + "transport", + "D17", + [ + 95, + 447, + 6, + 32, + 20 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 4 + ], + [ + "transport", + "Y7", + [ + 95 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 8 + ], + [ + "add", + "Y7", + "D17", + "1/4", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "transport", + "Y7", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ], + 1 + ] + ], + "published": [ + [ + "transport", + "D17", + [ + 95, + 447, + 6, + 32, + 20 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 4 + ] + ], + "published_range": [ + 3612, + 3613 + ] + } + ] + } + }, + "schema_version": 1, + "selected_kappa": "0.001672660197076918", + "source_register": "X0", + "target_register": "Y7" +} diff --git a/research/p104-flag1-side-correction-bill/inputs/pr3532/REPAIR-RECIPES.json b/research/p104-flag1-side-correction-bill/inputs/pr3532/REPAIR-RECIPES.json new file mode 100644 index 0000000000..18e2a0d109 --- /dev/null +++ b/research/p104-flag1-side-correction-bill/inputs/pr3532/REPAIR-RECIPES.json @@ -0,0 +1,563 @@ +{ + "clifford_exact_sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "compiler_sha256": "9d2fc2d81962ddb0b4dd7d6482d9918a87a6b05759690317dea79939ca5656a3", + "recipes": [ + { + "new": [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + "old": [ + 133 + ], + "rank": 8, + "recipe": { + "left": { + "linear_Z4": [ + 3, + 2, + 3, + 2, + 2, + 2, + 2, + 2, + 0 + ], + "matrix_rows": [ + 257, + 2, + 4, + 8, + 16, + 32, + 64, + 5, + 128 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 5, + 0, + 5, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 8, + "right": { + "linear_Z4": [ + 0, + 2, + 0, + 2, + 2, + 2, + 2, + 1, + 2 + ], + "matrix_rows": [ + 1, + 2, + 132, + 8, + 16, + 32, + 64, + 256, + 128 + ], + "offset": 507, + "phase": 2, + "quadratic_rows": [ + 128, + 0, + 128, + 0, + 0, + 0, + 0, + 133, + 0 + ] + } + } + }, + { + "new": [ + 263, + 133, + 30 + ], + "old": [ + 133 + ], + "rank": 2, + "recipe": { + "left": { + "linear_Z4": [ + 3, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 7, + 9, + 17, + 34, + 2, + 64, + 128, + 256, + 3 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 1, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 2, + "right": { + "linear_Z4": [ + 0, + 1, + 1, + 3, + 2, + 0, + 0, + 0, + 2 + ], + "matrix_rows": [ + 7, + 9, + 257, + 274, + 276, + 24, + 32, + 64, + 128 + ], + "offset": 2, + "phase": 1, + "quadratic_rows": [ + 270, + 279, + 279, + 25, + 14, + 0, + 0, + 0, + 7 + ] + } + } + }, + { + "new": [ + 257, + 128, + 65, + 32, + 17, + 9, + 5, + 3 + ], + "old": [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + "rank": 1, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 1, + "right": { + "linear_Z4": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 1, + 3, + 5, + 9, + 17, + 32, + 65, + 128, + 257 + ], + "offset": 350, + "phase": 1, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + } + }, + { + "new": [ + 257, + 128, + 65, + 32, + 17, + 9, + 5, + 3 + ], + "old": [ + 263, + 133, + 30 + ], + "rank": 5, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 3, + 2, + 3, + 2, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 39, + 67, + 133, + 265, + 15, + 16, + 1, + 5, + 6 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 2, + 15, + 10, + 14, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 5, + "right": { + "linear_Z4": [ + 1, + 3, + 3, + 3, + 0, + 2, + 2, + 1, + 1 + ], + "matrix_rows": [ + 385, + 477, + 91, + 264, + 32, + 335, + 384, + 128, + 272 + ], + "offset": 348, + "phase": 1, + "quadratic_rows": [ + 329, + 150, + 22, + 217, + 142, + 0, + 137, + 474, + 385 + ] + } + } + }, + { + "new": [ + 281, + 133 + ], + "old": [ + 263, + 133, + 30 + ], + "rank": 1, + "recipe": { + "left": { + "linear_Z4": [ + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 2, + 5, + 9, + 17, + 1, + 32, + 64, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 1, + "right": { + "linear_Z4": [ + 0, + 3, + 3, + 3, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 14, + 17, + 2, + 4, + 24, + 32, + 64, + 128, + 272 + ], + "offset": 1, + "phase": 0, + "quadratic_rows": [ + 16, + 14, + 14, + 30, + 9, + 0, + 0, + 0, + 0 + ] + } + } + }, + { + "new": [ + 263, + 133, + 30 + ], + "old": [ + 412 + ], + "rank": 2, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 6, + 9, + 16, + 34, + 66, + 128, + 256, + 1, + 3 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 2, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 2, + "right": { + "linear_Z4": [ + 3, + 1, + 2, + 1, + 1, + 0, + 0, + 3, + 3 + ], + "matrix_rows": [ + 402, + 137, + 385, + 18, + 148, + 280, + 256, + 32, + 64 + ], + "offset": 123, + "phase": 0, + "quadratic_rows": [ + 265, + 386, + 144, + 409, + 284, + 0, + 0, + 142, + 283 + ] + } + } + } + ], + "schema_version": 1, + "scope": "Native recipes for the transport edges used by repairs R0 and R1 that are absent from the published p104-native-channel recipe set. Lowered with the pinned compile.py / vendor/clifford_exact.py; checked by the published check_native.validate() during replay." +} diff --git a/research/p104-flag1-side-correction-bill/test_package.py b/research/p104-flag1-side-correction-bill/test_package.py new file mode 100644 index 0000000000..dbb08a1e2e --- /dev/null +++ b/research/p104-flag1-side-correction-bill/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 os +import shutil +import subprocess +import sys +import tempfile +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PKG = HERE.relative_to(ROOT).as_posix() +NATIVE = "research/p104-native-channel" +COPY = [ + f"{NATIVE}/inputs/LOWRANK-WITNESS.json", + f"{NATIVE}/inputs/P104-FIXTURE.json", + f"{NATIVE}/NATIVE-RECIPES.json.gz", + f"{NATIVE}/check_native.py", + f"{NATIVE}/vendor/native_verify.py", + "research/p104-joint-unit-flags/CERTIFICATE.json", +] +SCANNERS = ("verify.py", "independent.py") +FULL = [1, 2, 4, 8, 16, 32, 64, 128, 256] + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def tree(base): + for rel in COPY: + (base / rel).parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / rel, base / rel) + shutil.copytree(HERE, base / PKG, ignore=shutil.ignore_patterns("__pycache__")) + return base + + +def run(base, scanner): + p = subprocess.run([sys.executable, "-I", "-O", "-Werror", "-B", str(base / PKG / scanner), str(base)], + capture_output=True, text=True, timeout=600) + return p.returncode, p.stdout + p.stderr + + +def digest(base): + return {p.relative_to(base).as_posix(): hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(base.rglob("*")) if p.is_file()} + + +def edit_json(path, fn): + data = json.loads(path.read_text()) + fn(data) + path.write_text(json.dumps(data, indent=2, sort_keys=True) + "\n") + + +def cert_edit(fn): + return lambda base: edit_json(base / PKG / "CERTIFICATE.json", fn) + + +def events(d, base, name): + return d["corrections"][base][name]["splices"][0]["events"] + + +def set_event(base, name, k, field, value): + def fn(d): + events(d, base, name)[k][field] = value + return cert_edit(fn) + + +def drop_event(base, name, k): + def fn(d): + del events(d, base, name)[k] + return cert_edit(fn) + + +def dup_key(base): + p = base / PKG / "CERTIFICATE.json" + text = p.read_text() + p.write_text(text.replace('"schema_version": 1', '"schema_version": 1,\n "schema_version": 1', 1)) + + +def flip(rel, offset): + def fn(base): + p = base / rel + raw = bytearray(p.read_bytes()) + raw[offset] ^= 1 + p.write_bytes(bytes(raw)) + return fn + + +def recipe_phase(base): + p = base / PKG / "CORRECTION-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_T_rank_mass": cert_edit(lambda d: d["bill"]["T"]["added_vs_base"].update(rank_mass=0)), + "bill_E_register_mass": cert_edit(lambda d: d["bill"]["E"].update(added_rank_by_register={"Y7": 2})), + "forcing_head": cert_edit(lambda d: d["obstruction"].update(forcing_source_head=[131])), + "exit_event": cert_edit(lambda d: d["obstruction"]["source_leaves_target_final_at"].__setitem__(0, 1311)), + "strict_row": cert_edit(lambda d: d["obstruction"]["strict_first_obstruction"].__setitem__(5, [1312, None])), + "cohost_rescue": cert_edit(lambda d: d["obstruction"].update(order_preserving_cohost_single_register_rescues=[])), + "cohost_discount": cert_edit(lambda d: d["end_cut_comparison"].update(cohost_discount_R1=0)), + "duplicate_key": dup_key, + "witness_byte": flip(f"{NATIVE}/inputs/LOWRANK-WITNESS.json", 4096), + "pr3532_certificate_byte": flip(f"{PKG}/inputs/pr3532/CERTIFICATE.json", 2048), + "recipe_phase": recipe_phase, + "T_wrong_coefficient": set_event("R0", "T", 1, 3, "1/4"), + "T_undercharged_lift": set_event("R0", "T", 0, 4, 5), + "S_wrong_chart": set_event("R0", "S", 2, 4, FULL), + "S_source_not_restored": drop_event("R0", "S", 3), + "P_private_not_erased": drop_event("R0", "P", 5), + "E_wrong_chart": set_event("R1", "E", 1, 4, [95, 486, 232]), + "E_wrong_sign": set_event("R1", "E", 1, 3, "-1/2"), +} + + +def case(name): + with tempfile.TemporaryDirectory() as tmp: + base = tree(Path(tmp)) + CASES[name](base) + results = [run(base, s) for s in SCANNERS] + return name, [code != 0 for code, _ in results] + + +def main(): + with tempfile.TemporaryDirectory() as tmp: + base = tree(Path(tmp)) + before = digest(base) + for s in SCANNERS: + code, out = run(base, s) + need(code == 0 and "PASS_P104_FLAG1_SIDE_CORRECTION_BILL" in out, "clean pass: " + s + "\n" + out) + need(digest(base) == before, "scanners are read-only") + workers = max(2, min(8, os.cpu_count() or 2)) + with concurrent.futures.ThreadPoolExecutor(max_workers=workers) as pool: + results = dict(pool.map(case, CASES)) + for name, rejected in sorted(results.items()): + need(all(rejected), "mutation accepted: %s %s" % (name, rejected)) + print("PASS_P104_FLAG1_SIDE_CORRECTION_BILL_TESTS cases=%d clean_read_only=1 scanners=%d" % (len(CASES), len(SCANNERS))) + + +if __name__ == "__main__": + main() diff --git a/research/p104-flag1-side-correction-bill/verify.py b/research/p104-flag1-side-correction-bill/verify.py new file mode 100644 index 0000000000..9bb88d9a0e --- /dev/null +++ b/research/p104-flag1-side-correction-bill/verify.py @@ -0,0 +1,694 @@ +#!/usr/bin/env python3 +"""Read-only replay of the flag-1 side-correction bill at #3532's co-hosted charts. + +Builds #3532's repairs R0 (order-preserving, Y7 += D17/4 in [95,486,232]) and +R1 (relocated, the same ADD in the full chart) from the vendored, hash-pinned +splices, then adds the (7, 0) entry of I - G/2 (Y7 += +1/2 X0) and, for the +row variants, the whole Y7 row. For each corrected word it runs the published +check_native.validate() unchanged on the coefficient-0 copy (chart legality, +native edges, endpoint adapters and all 280 framed rows do not depend on the +inserted coefficient), replays the real word with exact rational rows, and +confirms that validate() rejects the real word only at Y7's endpoint. It then +recomputes the bills, the X7 -> X20 -> G18 -> X0 forcing chain, the least-frame +sweep that rules out a zero-added-mass correction at every insertion class and +every placement of the delivering ADD, and the single-register census that +rules out an order-preserving co-hosted correction at +2. Admission uses need() +and stays active under python -O. Nothing is written. +""" + +import copy +import gzip +import hashlib +import importlib.util +import itertools +import json +import sys +from fractions import Fraction +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" +PR3532 = f"{PKG}/inputs/pr3532" +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", + f"{PR3532}/CERTIFICATE.json": "5f29955e692d3fdb628ab0562c87defd21318c31cc2a8cafd6693f8004404359", + f"{PR3532}/REPAIR-RECIPES.json": "13d2b2f45d75697d137aca1baf953b2bdf482bc8b02da6887ebb492f18470209", +} +FLAG_INDEX = 1 +DELIVERY = 2797 +SELECTED_KAPPA = "0.001672660197076918" +FULL = [1, 2, 4, 8, 16, 32, 64, 128, 256] +A2 = [95, 486] +A3 = [95, 486, 232] +PRIVATE_SPAN = (2461, 2524) +MARKER = ( + "PASS_P104_FLAG1_SIDE_CORRECTION_BILL flag=1 entry=(7,0) gram=-1 coefficient=+1/2 " + "zero_mass_placements=0/18(delivery_anywhere_in_1116_slots) forcing=X7(387)-616-G11-679-X20-1070-G18-1074-X0 " + "strict_min_added_rank=2 " + "R0:T=+1transport+1add+2rank S=+2transport+1add+2rank P=+1rank+1private_lifetime Trow=+48add+2rank " + "R1:E=+0transport+1add+0rank Erow=+48add+0rank row7=identity " + "cohost_discount_R0=0 cohost_discount_R1=2 joint_min_relocated=2 joint_min_order_preserving_strict=4 " + "native_validate=7/7 no_new_kappa" +) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def pairs_unique(pairs): + out = {} + for key, value in pairs: + need(key not in out, "duplicate JSON key: " + str(key)) + out[key] = value + return out + + +def loads(raw): + return json.loads(raw, object_pairs_hook=pairs_unique) + + +def pinned_bytes(root, rel): + raw = (root / rel).read_bytes() + need(hashlib.sha256(raw).hexdigest() == PINS[rel], "pinned input changed: " + rel) + return raw + + +def load_checker(root): + pinned_bytes(root, f"{NATIVE}/check_native.py") + pinned_bytes(root, f"{NATIVE}/vendor/native_verify.py") + name = "flag1_side_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")) + repair = loads(pinned_bytes(root, f"{PR3532}/CERTIFICATE.json")) + repair_recipes = loads(pinned_bytes(root, f"{PR3532}/REPAIR-RECIPES.json"))["recipes"] + return witness, fixture, recipes, flags, repair, repair_recipes + + +# --- GF(2) frames ----------------------------------------------------------- + +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 join(a, b): + return canon(tuple(a) + tuple(b)) + + +def inside(a, b): + return len(join(a, b)) == len(canon(b)) + + +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) + + +# --- roots ------------------------------------------------------------------- + +def ports(fixture): + lines = set() + for i, j in itertools.combinations(range(8), 2): + for sign in (-1, 1): + v = [0] * 8 + v[i], v[j] = 2, 2 * sign + lines.add(tuple(v)) + for signs in itertools.product((-1, 1), repeat=7): + if signs.count(-1) % 2 == 0: + lines.add((1, *signs)) + removed = {tuple(r) for r in fixture["F0"] + fixture["C"]} + out = [r for r in sorted(lines) if r not in removed] + need(len(out) == 104, "P104 ports") + return out + + +def gram(ps, t, s): + return sum(x * y for x, y in zip(ps[t], ps[s])) // 4 + + +# --- 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") + need(len(row["published"]) == stop - start, "splice covers its range") + for k, old in enumerate(row["published"]): + need(program[start + k] == old, "splice binds event %d" % (start + k)) + out[start:stop] = copy.deepcopy(row["events"]) + last = start + return out + + +def is_correction(e): + return e[0] == "add" and e[1] == "Y7" and (e[2].startswith("X") or e[2] == "C") + + +def last_transport(program, reg): + return max(i for i, e in enumerate(program) if e[0] == "transport" and e[1] == reg) + + +def delivering_add(program): + hits = [i for i, e in enumerate(program) if e[0] == "add" and e[1] == "Y7" and e[2] == "D17" and e[3] == "1/4"] + need(len(hits) == 1, "one delivering Y7 += D17/4") + return hits[0] + + +def corrections(program, r0, r1, final, ps): + f7 = final["Y7"] + row = [["add", "Y7", "X%d" % s, str(Fraction(-gram(ps, 7, s), 2)), FULL] + for s in range(104) if s != 7 and gram(ps, 7, s)] + entry = ["add", "Y7", "X0", str(Fraction(-gram(ps, 7, 0), 2)), FULL] + + def one(base, at, events): + return [{"published_range": [at, at + 1], "published": [base[at]], "events": events}] + + c0 = last_transport(r0, "Y7") + need(r0[c0] == ["transport", "Y7", A3, r0[c0][3], 5], "R0 terminal Y7 transport leaves the rank-3 co-hosted chart") + t7 = r0[c0][3] + need(canon(t7) == canon(f7), "terminal chart is Y7's final frame") + d1 = delivering_add(r1) + need(r1[d1] == ["add", "Y7", "D17", "1/4", FULL], "R1 delivers in the full chart") + cp = last_transport(program, "Y7") + need(program[cp] == ["transport", "Y7", A2, t7, 6], "published terminal Y7 transport") + lift0 = [["transport", "Y7", A3, FULL, 6]] + drop = [["transport", "Y7", FULL, t7, 1]] + return { + "R0": { + "T": { + "route": "target lift at R0's cut: Y7 leaves the co-hosted chart [95,486,232] for the full chart, takes the entry from X0 there, then descends to its final hyperplane", + "splices": one(r0, c0, lift0 + [entry] + drop), + }, + "S": { + "route": "source detour: Y7 takes R0's terminal transport, X0 descends to Y7's final hyperplane for one ADD and returns to the full chart before its next read", + "splices": one(r0, c0, [r0[c0], ["transport", "X0", FULL, t7, 1], + ["add", "Y7", "X0", entry[3], t7], ["transport", "X0", t7, FULL, 1]]), + }, + "P": { + "route": "one added private lifetime under the inherited private-copy contract: copy X0 into C at the full chart, descend C to Y7's final hyperplane, deliver, discard", + "splices": one(r0, c0, [r0[c0], ["zero", "C", FULL], ["copy", "C", "X0", FULL], + ["transport", "C", FULL, t7, 1], ["add", "Y7", "C", entry[3], t7], + ["erase", "C", t7]]), + }, + "Trow": { + "route": "whole Y7 row of I - G/2 on T's lift: every off-diagonal source entry -G[7,s]/2 is added while Y7 sits in the full chart", + "splices": one(r0, c0, lift0 + row + drop), + }, + }, + "R1": { + "E": { + "route": "in-chart entry at R1's co-hosted update: Y7 and X0 already share the full chart at the relocated delivering ADD, so the entry is one extra ADD there", + "splices": one(r1, d1, [r1[d1], entry]), + }, + "Erow": { + "route": "whole Y7 row of I - G/2 at R1's co-hosted update: all 48 off-diagonal entries are added in the full chart right after the delivering ADD", + "splices": one(r1, d1, [r1[d1]] + row), + }, + }, + "published": { + "Tend": { + "route": "end-cut control on the published word: Y7 leaves [95,486] for the full chart at its terminal transport, takes the entry there, then descends", + "splices": one(program, cp, [["transport", "Y7", A2, FULL, 7], entry] + drop), + }, + }, + } + + +def zeroed(program): + out = copy.deepcopy(program) + for e in out: + if is_correction(e): + e[3] = "0" + return out + + +def assemble(recipes, program, extra, physical): + pub = {(tuple(r["old"]), tuple(r["new"])): r for r in recipes["transports"]} + more = {} + for r in extra: + key = (tuple(r["old"]), tuple(r["new"])) + need(key not in more and key not in pub, "extra recipes are unique new edges") + more[key] = r + edges = {} + for i, e in enumerate(program): + if e[0] == "transport": + edges.setdefault((physical(e[2]), physical(e[3])), []).append(i) + used = set() + out = [] + for key in sorted(edges): + if key in pub: + rec = dict(pub[key]) + else: + need(key in more, "missing native recipe for edge") + rec = dict(more[key]) + used.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 + + +def bill(result, program): + 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"].get(k, 0) for k in ("zero", "copy", "erase")}, + "transport_occurrences": sum(profile.values()), + "rank_mass": result["rank_mass"], + "paid_profile": profile, + "distinct_native_edges": result["transports"], + "endpoint_adapters": result["intrinsic_endpoint_adapters"], + } + + +def delta(a, b): + out = {} + for k in sorted({int(x) for x in a["paid_profile"]} | {int(x) for x in b["paid_profile"]}): + d = b["paid_profile"].get(str(k), 0) - a["paid_profile"].get(str(k), 0) + if d: + out[str(k)] = d + return out + + +def added(a, b): + return {k: b[k] - a[k] for k in ("events", "scalar_adds", "transport_occurrences", "rank_mass")} + + +def rows(witness, program): + state = {n: {n: Fraction(1)} for n in witness["initial_frames"]} + for e in program: + if e[0] == "zero": + state[e[1]] = {} + elif e[0] == "erase": + state.pop(e[1]) + elif e[0] == "copy": + state[e[1]] = dict(state[e[2]]) + elif e[0] == "add": + _, dst, src, a, _f = e + 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 + + +def register_mass(program): + out = {} + for e in program: + if e[0] == "transport": + out[e[1]] = out.get(e[1], 0) + e[4] + return out + + +def frames_before(witness, program, at, regs): + hist = {} + for e in program[:at]: + if e[0] == "transport": + hist[e[1]] = e[3] + return {r: list(canon(hist.get(r, witness["initial_frames"][r]))) for r in regs} + + +# --- least monotone lower bounds --------------------------------------------- + +def sweep(witness, program, inject=(), skip=(), relax=()): + """Least frames of a repair in which every non-relaxed non-private path is monotone. + + The private register C and every register in `relax` are left unconstrained + (their ADDs impose nothing), which only removes constraints. Events in `skip` + are dropped, which also only removes constraints. inject = [(u, regs, extra)]: + just before event u the listed registers share one frame that also contains + `extra`. Returns [event, register] for the first forced frame that leaves the + register's final frame, or None. + """ + free = {"C"} | set(relax) + init = {k: canon(v) for k, v in witness["initial_frames"].items()} + final = {k: canon(v) for k, v in witness["final_frames"].items()} + cur = dict(init) + at = {} + for u, regs, extra in inject: + at.setdefault(u, []).append(([r for r in regs if r not in free], tuple(extra))) + for i in range(len(program) + 1): + for regs, extra in at.get(i, ()): + m = canon(extra + tuple(x for r in regs for x in cur[r])) + for r in regs: + cur[r] = m + for r in regs: + if not inside(m, final[r]): + return [i, r] + if i == len(program): + break + e = program[i] + if i in skip or e[0] != "add" or free & {e[1], e[2]}: + continue + m = join(cur[e[1]], cur[e[2]]) + cur[e[1]] = cur[e[2]] = m + for r in e[1:3]: + if not inside(m, final[r]): + return [i, r] + return None + + +def forced_frames(witness, program, reg): + cur = {k: canon(v) for k, v in witness["initial_frames"].items()} + out = [] + for i, e in enumerate(program): + if e[0] == "add" and "C" not in e[1:3]: + m = join(cur[e[1]], cur[e[2]]) + cur[e[1]] = cur[e[2]] = m + if reg in e[1:3]: + out.append([i, e[1] if e[2] == reg else e[2], len(m)]) + return out + + +def head_chain(witness, program, source, stop): + """Earliest time-respecting ADD chain carrying `source`'s head into each register before `stop`.""" + came = {source: None} + for i, e in enumerate(program[:stop]): + if e[0] != "add" or "C" in e[1:3]: + continue + a, b = e[1], e[2] + if (a in came) != (b in came): + new, old = (a, b) if b in came else (b, a) + came[new] = (i, old) + return came + + +def trace(came, reg): + out = [] + while came.get(reg) is not None: + i, prev = came[reg] + out.append([i, prev, reg]) + reg = prev + return out[::-1] + + +def classes(program, regs, skip=()): + ev = [i for i, e in enumerate(program) + if i not in skip and e[0] in ("add", "copy") and set(regs) & {e[1], e[2]}] + return sorted({0} | {i + 1 for i in ev}) + + +# --- receipt ----------------------------------------------------------------- + +def receipt(root, cert, new_recipes): + ck = load_checker(root) + witness, fixture, recipes, flags, repair, repair_recipes = load_inputs(root) + helper = flags["helpers"][FLAG_INDEX] + head = helper["basis"][0] + need(("X%d" % helper["source"], "Y%d" % helper["target"], head) == ("X0", "Y7", 232), "flag 1 identity") + need(repair["claim_id"] == "p104-flag1-head-step-repair", "R0/R1 source is #3532") + ps = ports(fixture) + physical = physical_map(recipes) + program = witness["program"] + final = witness["final_frames"] + f7 = canon(final["Y7"]) + bases = {"published": program} + for name in ("R0", "R1"): + bases[name] = apply_splices(program, repair["repairs"][name]["splices"]) + base_bill = {"published": bill(ck.validate(recipes, witness, fixture, False), program)} + for name in ("R0", "R1"): + w = dict(witness) + w["program"] = bases[name] + c, _ = assemble(recipes, bases[name], repair_recipes, physical) + base_bill[name] = bill(ck.validate(c, w, fixture, False), bases[name]) + spec = corrections(program, bases["R0"], bases["R1"], final, ps) + need(cert.get("corrections") == spec, "committed corrections equal the generated ones") + need(all(not (e[0] in ("add", "copy") and e[2] == "Y7") for b in bases.values() for e in b), "Y7 is never read") + extra = list(repair_recipes) + list(new_recipes) + new_keys = {(tuple(r["old"]), tuple(r["new"])) for r in new_recipes} + need(len(new_keys) == len(new_recipes), "unique correction recipes") + used_all = set() + out = {} + for base_name, group in spec.items(): + base = bases[base_name] + expected = rows(witness, base) + mass0 = register_mass(base) + for name, item in group.items(): + prog = apply_splices(base, item["splices"]) + zero = zeroed(prog) + wz = dict(witness) + wz["program"] = zero + cz, used = assemble(recipes, zero, extra, physical) + used_all |= used & new_keys + b = bill(ck.validate(cz, wz, fixture, False), prog) + wr = dict(witness) + wr["program"] = prog + try: + ck.validate(cz, wr, fixture, False) + except ValueError as exc: + rejection = str(exc) + else: + rejection = None + got = rows(witness, prog) + changed = sorted(k for k in expected if got.get(k) != expected[k]) + y = got["Y7"] + mass1 = register_mass(prog) + added_mass = {r: mass1.get(r, 0) - mass0.get(r, 0) for r in sorted(set(mass0) | set(mass1)) + if mass1.get(r, 0) != mass0.get(r, 0)} + at = item["splices"][0]["published_range"][0] + fb = frames_before(witness, prog, at, ("Y7", "X0")) + corr = [e for e in prog if is_correction(e)] + hist = {} + for i, e in enumerate(prog): + if e[0] == "transport": + hist[e[1]] = e[3] + if e[0] == "add" and e[1] == "Y7" and e[2] == "D17" and e[3] == "1/4": + deliver_chart = canon(e[4]) + r = dict(b) + r.update({ + "base": base_name, + "native_validate_coefficient_zero": "PASS", + "real_word_rejected_by_unchanged_checker_at": rejection, + "changed_final_rows": changed, + "Y7_final_X0": str(y.get("X0", Fraction(0))), + "Y7_final_row_is_identity": y == {"Y7": Fraction(1), "X7": Fraction(1)}, + "correction_adds": len(corr), + "correction_chart_ranks": sorted({len(canon(e[4])) for e in corr}), + "head_in_correction_charts": all(inside([head], e[4]) for e in corr), + "delivering_update_chart_rank": len(deliver_chart), + "head_in_delivering_update_chart": inside([head], deliver_chart), + "added_rank_by_register": added_mass, + "Y7_frame_rank_before_correction": len(fb["Y7"]), + "X0_frame_rank_before_correction": len(fb["X0"]), + "added_vs_base": added(base_bill[base_name], b), + "added_vs_published": added(base_bill["published"], b), + "profile_delta_vs_base": delta(base_bill[base_name], b), + }) + out[name] = r + need(len(used_all) == len(new_recipes), "every committed correction recipe is used") + + # Forcing chain and the zero-added-mass obstruction. + init = witness["initial_frames"] + lb = forced_frames(witness, program, "X0") + leave = [i for i, e in enumerate(program) if e[0] == "add" and "X0" in e[1:3]] + cur = {k: canon(v) for k, v in init.items()} + leave_at = None + for i, e in enumerate(program): + if e[0] == "add" and "C" not in e[1:3]: + m = join(cur[e[1]], cur[e[2]]) + cur[e[1]] = cur[e[2]] = m + if "X0" in e[1:3] and not inside(m, f7): + leave_at = i + leave_frame = m + break + need(leave_at is not None and leave_at in leave, "X0's forced frame leaves final(Y7) at an X0 read") + partner = program[leave_at][1] + outside = sorted(s for s in range(104) if not inside(canon(init["X%d" % s]), f7)) + reach = {} + for s in outside: + came = head_chain(witness, program, "X%d" % s, leave_at + 1) + if "X0" in came: + reach["X%d" % s] = trace(came, "X0") + need(len(reach) == 1, "one outside head reaches X0 at its exit") + (witness_source, chain), = reach.items() + dskip = {DELIVERY} + cls = classes(program, ("X0", "Y7"), skip=dskip) + strict = [[u, sweep(witness, program, inject=[(u, ("X0", "Y7"), ())], skip=dskip)] for u in cls] + need(all(x[1] for x in strict), "every strict placement is obstructed") + strict_pub = [[u, sweep(witness, program, inject=[(u, ("X0", "Y7"), ())])] for u in classes(program, ("X0", "Y7"))] + early = [u for u in classes(program, ("Y7",), skip=dskip) if u < PRIVATE_SPAN[0]] + private = [[u, sweep(witness, program, inject=[(u, ("Y7",), (head,))], skip=dskip)] for u in early] + need(all(x[1] for x in private), "every early private delivery is obstructed") + need(all(sweep(witness, b) is None for b in bases.values()), "published, R0 and R1 feasible") + need(sweep(witness, program, skip=dskip) is None, "published feasible without the delivering ADD") + force = (DELIVERY, ("Y7", "D17"), (head,)) + regs = sorted(init) + cohost_rescue = [r for r in regs if sweep(witness, program, inject=[force], relax=(r,)) is None] + need(sweep(witness, program, inject=[force]) is not None, "order-preserving co-hosting needs added mass") + joint = {} + for r in [None] + cohost_rescue: + rel = () if r is None else (r,) + joint["none" if r is None else r] = [ + [u, sweep(witness, program, inject=[force, (u, ("X0", "Y7"), ())], relax=rel)] + for u in classes(program, ("X0", "Y7"))] + need(all(x[1] for v in joint.values() for x in v), "no single-register order-preserving joint repair") + nz = [s for s in range(104) if s != 7 and gram(ps, 7, s)] + obstruction = { + "entry": {"target": "Y7", "source": "X0", "gram": gram(ps, 7, 0), + "correction_coefficient": str(Fraction(-gram(ps, 7, 0), 2)), "diagonal_gram": gram(ps, 7, 7)}, + "row_7_offdiagonal_nonzero": len(nz), + "target_final_frame": list(f7), + "flag_head_in_target_final": inside([head], f7), + "sources_with_head_outside_target_final": len(outside), + "outside_heads_have_even_gram": all(gram(ps, 7, s) % 2 == 0 for s in outside), + "source_first_read": [leave[0], program[leave[0]][:4]], + "source_leaves_target_final_at": [leave_at, program[leave_at][:4]], + "source_forced_frame_at_exit": list(leave_frame), + "exit_partner": partner, + "forcing_source": witness_source, + "forcing_source_head": list(canon(init[witness_source])), + "forcing_source_gram_with_target": gram(ps, 7, int(witness_source[1:])), + "forcing_chain": chain, + "source_forced_rank_at_events": lb, + "source_forced_full_from": [i for i, _p, r in lb if r == 9][0], + "delivering_add_dropped_in_sweeps": DELIVERY, + "delivering_add_window_slots": 1116, + "strict_cut_classes": len(cls), + "strict_first_obstruction": strict, + "strict_published_order_first_obstruction": strict_pub, + "private_early_delivery_cuts": len(private), + "private_early_first_obstruction": private, + "published_private_lifetimes": list(PRIVATE_SPAN), + "non_private_registers_at_rank_floor": sum( + 1 for r in init if register_mass(program).get(r, 0) == len(canon(final[r])) - len(canon(init[r]))), + "order_preserving_cohost_single_register_rescues": cohost_rescue, + "order_preserving_joint_first_obstruction": joint, + } + pub_cut = program[last_transport(program, "Y7")] + r0_cut = bases["R0"][last_transport(bases["R0"], "Y7")] + end_cut = { + "published_terminal_transport": [last_transport(program, "Y7"), pub_cut[4]], + "published_detour_added_rank": out["Tend"]["added_vs_base"]["rank_mass"], + "R0_terminal_transport": [last_transport(bases["R0"], "Y7"), r0_cut[4]], + "R0_correction_added_rank": out["T"]["added_vs_base"]["rank_mass"], + "R1_correction_added_rank": out["E"]["added_vs_base"]["rank_mass"], + "cohost_discount_R0": out["Tend"]["added_vs_base"]["rank_mass"] - out["T"]["added_vs_base"]["rank_mass"], + "cohost_discount_R1": out["Tend"]["added_vs_base"]["rank_mass"] - out["E"]["added_vs_base"]["rank_mass"], + "joint_cohosted_and_corrected_vs_published": { + "R0+T": out["T"]["added_vs_published"]["rank_mass"], + "R0+S": out["S"]["added_vs_published"]["rank_mass"], + "R0+P": out["P"]["added_vs_published"]["rank_mass"], + "R1+E": out["E"]["added_vs_published"]["rank_mass"], + "published+Tend_not_cohosted": out["Tend"]["added_vs_published"]["rank_mass"], + }, + } + return { + "schema_version": 1, + "claim_id": "p104-flag1-side-correction-bill", + "pinned_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "requested_pin": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "repair_source": {"pr": 3532, "head": "8fecbf7df7b48c9004bd10a0da6a81f33d455737", + "vendored": [f"{PR3532}/CERTIFICATE.json", f"{PR3532}/REPAIR-RECIPES.json"]}, + "flag_index": FLAG_INDEX, + "basis_head": head, + "corrections": spec, + "bill": {"published": base_bill["published"], "R0": base_bill["R0"], "R1": base_bill["R1"], **out}, + "obstruction": obstruction, + "end_cut_comparison": end_cut, + "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, ob, ec = cert["bill"], cert["obstruction"], cert["end_cut_comparison"] + need(ob["entry"] == {"target": "Y7", "source": "X0", "gram": -1, "correction_coefficient": "1/2", "diagonal_gram": 2}, "entry") + need(ob["row_7_offdiagonal_nonzero"] == 48 and ob["flag_head_in_target_final"], "row 7 and head inside F7") + need(ob["source_first_read"][0] == 840 and ob["source_leaves_target_final_at"][0] == 1074 and ob["exit_partner"] == "G18", "exit event") + need(ob["forcing_source"] == "X7" and ob["forcing_source_head"] == [387] and ob["forcing_source_gram_with_target"] == 2, "X7 head 387 forces the exit") + need(ob["forcing_chain"][-2:] == [[1070, "X20", "G18"], [1074, "G18", "X0"]], "chain ends X20 -> G18 -> X0") + need(ob["source_forced_full_from"] == 1690, "X0 forced full from 1690") + need(ob["strict_cut_classes"] == 18 and all(x[1] for x in ob["strict_first_obstruction"]), "18/18 strict classes obstructed") + need(len(ob["strict_published_order_first_obstruction"]) == 19 and all(x[1] for x in ob["strict_published_order_first_obstruction"]), "19/19 published-order classes obstructed") + need(ob["forcing_chain"][0] == [616, "X7", "G11"], "chain starts at X7") + need(ob["private_early_delivery_cuts"] == 5 and all(x[1] for x in ob["private_early_first_obstruction"]), "5/5 early private deliveries obstructed") + need(ob["non_private_registers_at_rank_floor"] == 280, "rank floor") + need(ob["order_preserving_cohost_single_register_rescues"] == ["D17"], "only D17 rescues order-preserving co-hosting") + for name, base, want in (("T", "R0", [2, 1, 1, 2]), ("S", "R0", [3, 1, 2, 2]), ("P", "R0", [5, 1, 1, 1]), + ("Trow", "R0", [49, 48, 1, 2]), ("E", "R1", [1, 1, 0, 0]), ("Erow", "R1", [48, 48, 0, 0]), + ("Tend", "published", [2, 1, 1, 2])): + r = b[name] + need(r["base"] == base, name + " base") + need([r["added_vs_base"][k] for k in ("events", "scalar_adds", "transport_occurrences", "rank_mass")] == want, name + " bill") + need(r["native_validate_coefficient_zero"] == "PASS", name + " native") + need(r["real_word_rejected_by_unchanged_checker_at"] == "full physical boundary endpoint Y7", name + " rejection site") + need(r["changed_final_rows"] == ["Y7"], name + " only Y7 changes") + need(r["X0_frame_rank_before_correction"] == 9, name + " source in the full chart") + if name in ("Trow", "Erow"): + need(r["Y7_final_row_is_identity"] and r["correction_adds"] == 48, name + " row 7 becomes y + x") + else: + need(r["Y7_final_X0"] == "0" and r["correction_adds"] == 1, name + " entry applied") + for name in ("T", "S", "P", "Trow", "E", "Erow"): + need(b[name]["head_in_delivering_update_chart"], name + " delivering update co-hosts the head") + need(not b["Tend"]["head_in_delivering_update_chart"], "published delivering update does not co-host") + need(b["E"]["added_rank_by_register"] == {} and b["Erow"]["added_rank_by_register"] == {}, "E rides free on R1") + need(b["E"]["correction_chart_ranks"] == [9] and b["E"]["delivering_update_chart_rank"] == 9, "E in R1's full chart") + need(b["T"]["added_rank_by_register"] == {"Y7": 2} and b["S"]["added_rank_by_register"] == {"X0": 2}, "even per-register mass") + need(b["P"]["added_rank_by_register"] == {"C": 1} and b["P"]["private_events"] == {"zero": 9, "copy": 9, "erase": 9}, "P private lifetime") + need(b["T"]["profile_delta_vs_base"] == {"1": 1, "5": -1, "6": 1}, "T profile") + need(b["S"]["profile_delta_vs_base"] == {"1": 2}, "S profile") + need(b["E"]["profile_delta_vs_base"] == {} and b["Erow"]["profile_delta_vs_base"] == {}, "E profile unchanged") + need((ec["cohost_discount_R0"], ec["cohost_discount_R1"]) == (0, 2), "co-host discounts") + need(ec["joint_cohosted_and_corrected_vs_published"] == {"R0+T": 4, "R0+S": 4, "R0+P": 3, "R1+E": 2, + "published+Tend_not_cohosted": 2}, "joint bills") + 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 / "CORRECTION-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)