diff --git a/research/r439-twisted-star-absorption-seed02/EXPECTED.json b/research/r439-twisted-star-absorption-seed02/EXPECTED.json new file mode 100644 index 0000000000..e11da70965 --- /dev/null +++ b/research/r439-twisted-star-absorption-seed02/EXPECTED.json @@ -0,0 +1,995 @@ +{ + "census": { + "PR1062": { + "A_writer_pairs": 481, + "admitted": [ + [ + 506, + 374, + 288, + [ + 69 + ] + ], + [ + 507, + 355, + 290, + [ + 72 + ] + ], + [ + 514, + 367, + 304, + [ + 360 + ] + ] + ], + "centres": 162, + "d_tail_dirty_boundary_preserved": 148, + "d_tail_gains": [ + 0 + ], + "d_tail_same_centre_pairs": 148, + "dirty_boundary_preserved": 481, + "edges_with_A_writer": 236, + "first_centre_read": { + "A": 230, + "scatter": 6 + }, + "frame_by_gain": { + "-1": { + "frame_illegal": 192 + }, + "-10": { + "frame_illegal": 1 + }, + "-2": { + "frame_illegal": 45 + }, + "-3": { + "frame_illegal": 12 + }, + "-4": { + "frame_illegal": 6 + }, + "-5": { + "frame_illegal": 30 + }, + "-6": { + "frame_illegal": 25 + }, + "-7": { + "frame_illegal": 1 + }, + "-8": { + "frame_illegal": 1 + }, + "0": { + "frame_illegal": 116, + "frame_legal": 2, + "paths_changed": 2 + }, + "1": { + "frame_illegal": 45, + "frame_legal": 3 + } + }, + "gain_histogram": { + "-1": 192, + "-10": 1, + "-2": 45, + "-3": 12, + "-4": 6, + "-5": 30, + "-6": 25, + "-7": 1, + "-8": 1, + "0": 120, + "1": 48 + }, + "positive": 48, + "positive_outcomes": { + "admitted": 3, + "frame_illegal": 45 + }, + "star_edges": 236, + "substitute_size_histogram": { + "1": 109, + "10": 1, + "11": 2, + "2": 239, + "3": 56, + "4": 10, + "5": 4, + "6": 31, + "7": 27, + "8": 2 + } + }, + "PR1122": { + "A_writer_pairs": 489, + "admitted": [ + [ + 506, + 374, + 288, + [ + 69 + ] + ], + [ + 507, + 355, + 290, + [ + 72 + ] + ], + [ + 514, + 367, + 304, + [ + 360 + ] + ] + ], + "centres": 162, + "d_tail_dirty_boundary_preserved": 148, + "d_tail_gains": [ + 0 + ], + "d_tail_same_centre_pairs": 148, + "dirty_boundary_preserved": 489, + "edges_with_A_writer": 236, + "first_centre_read": { + "A": 230, + "scatter": 6 + }, + "frame_by_gain": { + "-1": { + "frame_illegal": 203 + }, + "-10": { + "frame_illegal": 2 + }, + "-2": { + "frame_illegal": 50 + }, + "-3": { + "frame_illegal": 27 + }, + "-4": { + "frame_illegal": 10 + }, + "-5": { + "frame_illegal": 14 + }, + "-6": { + "frame_illegal": 7 + }, + "-7": { + "frame_illegal": 2 + }, + "-8": { + "frame_illegal": 1 + }, + "-9": { + "frame_illegal": 2 + }, + "0": { + "frame_illegal": 119, + "frame_legal": 2, + "paths_changed": 2 + }, + "1": { + "frame_illegal": 45, + "frame_legal": 3 + } + }, + "gain_histogram": { + "-1": 203, + "-10": 2, + "-2": 50, + "-3": 27, + "-4": 10, + "-5": 14, + "-6": 7, + "-7": 2, + "-8": 1, + "-9": 2, + "0": 123, + "1": 48 + }, + "positive": 48, + "positive_outcomes": { + "admitted": 3, + "frame_illegal": 45 + }, + "star_edges": 236, + "substitute_size_histogram": { + "1": 109, + "10": 2, + "11": 3, + "2": 243, + "3": 60, + "4": 27, + "5": 10, + "6": 22, + "7": 11, + "8": 2 + } + }, + "PR1188": { + "A_writer_pairs": 470, + "admitted": [ + [ + 506, + 374, + 288, + [ + 69 + ] + ], + [ + 507, + 355, + 290, + [ + 72 + ] + ], + [ + 514, + 367, + 304, + [ + 360 + ] + ] + ], + "centres": 162, + "d_tail_dirty_boundary_preserved": 148, + "d_tail_gains": [ + 0 + ], + "d_tail_same_centre_pairs": 148, + "dirty_boundary_preserved": 470, + "edges_with_A_writer": 236, + "first_centre_read": { + "A": 230, + "scatter": 6 + }, + "frame_by_gain": { + "-1": { + "frame_illegal": 195 + }, + "-10": { + "frame_illegal": 2 + }, + "-2": { + "frame_illegal": 52 + }, + "-3": { + "frame_illegal": 20 + }, + "-4": { + "frame_illegal": 8 + }, + "-5": { + "frame_illegal": 13 + }, + "-6": { + "frame_illegal": 5 + }, + "-7": { + "frame_illegal": 2 + }, + "-8": { + "frame_illegal": 1 + }, + "-9": { + "frame_illegal": 2 + }, + "0": { + "frame_illegal": 119, + "frame_legal": 2, + "paths_changed": 2 + }, + "1": { + "frame_illegal": 44, + "frame_legal": 3 + } + }, + "gain_histogram": { + "-1": 195, + "-10": 2, + "-2": 52, + "-3": 20, + "-4": 8, + "-5": 13, + "-6": 5, + "-7": 2, + "-8": 1, + "-9": 2, + "0": 123, + "1": 47 + }, + "positive": 47, + "positive_outcomes": { + "admitted": 3, + "frame_illegal": 44 + }, + "star_edges": 236, + "substitute_size_histogram": { + "1": 109, + "10": 2, + "11": 3, + "2": 238, + "3": 61, + "4": 20, + "5": 10, + "6": 17, + "7": 8, + "8": 2 + } + }, + "PR967": { + "A_writer_pairs": 445, + "admitted": [ + [ + 506, + 374, + 288, + [ + 69 + ] + ], + [ + 507, + 355, + 290, + [ + 72 + ] + ], + [ + 514, + 367, + 304, + [ + 360 + ] + ] + ], + "centres": 157, + "d_tail_dirty_boundary_preserved": 128, + "d_tail_gains": [ + 0 + ], + "d_tail_same_centre_pairs": 128, + "dirty_boundary_preserved": 445, + "edges_with_A_writer": 221, + "first_centre_read": { + "A": 215, + "scatter": 6 + }, + "frame_by_gain": { + "-1": { + "frame_illegal": 169 + }, + "-10": { + "frame_illegal": 1 + }, + "-2": { + "frame_illegal": 45 + }, + "-3": { + "frame_illegal": 15 + }, + "-4": { + "frame_illegal": 5 + }, + "-5": { + "frame_illegal": 25 + }, + "-6": { + "frame_illegal": 21 + }, + "-7": { + "frame_illegal": 1 + }, + "-8": { + "frame_illegal": 1 + }, + "0": { + "frame_illegal": 110, + "frame_legal": 2, + "paths_changed": 2 + }, + "1": { + "frame_illegal": 45, + "frame_legal": 3 + } + }, + "gain_histogram": { + "-1": 169, + "-10": 1, + "-2": 45, + "-3": 15, + "-4": 5, + "-5": 25, + "-6": 21, + "-7": 1, + "-8": 1, + "0": 114, + "1": 48 + }, + "positive": 48, + "positive_outcomes": { + "admitted": 3, + "frame_illegal": 45 + }, + "star_edges": 221, + "substitute_size_histogram": { + "1": 104, + "10": 1, + "11": 2, + "2": 216, + "3": 55, + "4": 13, + "5": 4, + "6": 27, + "7": 22, + "8": 1 + } + } + }, + "inputs": { + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3", + "research/e8-bit-p111-tuned/code/xcheck_p.py": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e", + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f", + "research/r439-abc-star-composition/candidate.json.gz": "2b09a7a3851cdf2a7f19350d1555cf75788d001c9507a37e459cd931881ee066", + "research/r439-bsection-stars-seed01/candidate.json.gz": "b452d2c2b0b2a546d1105b1da9769aa78e5c54d6f00e97b30c77e3f54ce445ee", + "research/r439-gl5-shortest/candidate.json.gz": "4e7904d01ebdbfc60a26472b4e0d2e813c19c2fe1a4bb8ab390c12746a1da359", + "research/r439-helper-stars-seed19/candidate.json.gz": "d8b08885e8ce9868200b2645189d15ed18a27fc2742e54990b3257a0ca4df6b8" + }, + "instances": { + "PR1062": { + "chronology": { + "absorbing_gate_is_first_A_touch": true, + "cuts": 3270, + "cuts_with_difference": 459, + "differing_centres_stay_at_zero_frame": true, + "frames_identical_at_every_cut": true, + "max_registers_differing": 3 + }, + "columns": 661, + "controls": [ + [ + "omit restorations without the A edit", + "dirty endpoint wrong on 102 registers {'helper': 3, 'target': 99}; clean-helper endpoint passes" + ], + [ + "A edit with the literal cleanup of the edited A", + "dirty helpers [506, 507, 514] end as centre+leaf; clean helpers pass" + ], + [ + "A edit with literal cleanup, owner checker", + "owner checker rejects: helpers not restored: [506, 507, 514]" + ], + [ + "absorption after the first centre read (A[1218] for centre 514)", + "dirty boundary fails" + ], + [ + "wrong substitute register ([72] instead of [69] at A[288])", + "dirty boundary fails" + ], + [ + "frame-illegal substitution (centre 234, A[247], new [9])", + "illegal frame move: register 9 frame 115 -> 11" + ], + [ + "splice absorbed A/B/C with PR589 D", + "owner checker rejects: helpers not restored: [506, 507, 514]" + ], + [ + "corrupted source pin", + "source pin mismatch: research/r439-bsection-stars-seed01/candidate.json.gz" + ] + ], + "directions": 2, + "exporter": { + "absorbed": { + "ADD": 11497, + "B": 5858638, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 25717, + "MOVE": 2911, + "payload_bits": 95, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "record_sha256": "c44b7709940a9256293cbd21a29e819382426ea15c02b90b0d39ca096bc53620", + "records": 14426 + }, + "base": { + "ADD": 11500, + "B": 5911840, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 25717, + "MOVE": 2911, + "payload_bits": 95, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "record_sha256": "80bb888427eb8bf158dd4279aa56340d20cf573c296f15632b22afabedf0967d", + "records": 14429 + } + }, + "first_climbs": { + "absorbed": { + "helpers_climbing_from_zero": 439, + "non_own_value": [ + 506, + 507, + 514 + ], + "targets_climbing_in_D_or_A": 0 + }, + "base": { + "helpers_climbing_from_zero": 439, + "non_own_value": [], + "targets_climbing_in_D_or_A": 0 + } + }, + "literal": { + "absorbed": { + "ADDs": 11497, + "A_ADDs": 2130, + "B": 5858638, + "C_ADDs": 2495, + "D_ADDs": 5545, + "F": 25717, + "local_bits": 95, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 182 + }, + "base": { + "ADDs": 11500, + "A_ADDs": 2130, + "B": 5911840, + "C_ADDs": 2495, + "D_ADDs": 5548, + "F": 25717, + "local_bits": 95, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 182 + } + }, + "moves": [ + [ + 506, + 374, + 288, + [ + 69 + ] + ], + [ + 507, + 355, + 290, + [ + 72 + ] + ], + [ + 514, + 367, + 304, + [ + 360 + ] + ] + ], + "owner": { + "absorbed_false": [ + "H2_D_frame0_targets_from_helpers", + "H4_C_literal_reverse_at_full", + "K_equals_D", + "C_is_U_inverse" + ], + "absorbed_true": 5, + "base_false": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D" + ], + "original_D_splice_all_true": true + }, + "paths_registers": 661, + "payload": "absorbed-pr1062.json.gz", + "payload_sha256": "b6b2acfc7293ac1910fdf8b087ab62f002809eaec7760b7dcaae9aa754738062", + "perturbations_rejected": 1980, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "twisted": { + "absorbed": { + "C_Uprime_T_identity": true, + "C_Uprime_identity": false, + "C_full_frame_z_only": true, + "D_entry_frame_zero": true, + "D_frame_zero": true, + "D_no_target_feeds_helper": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_y_plus_Nh": true, + "J_identity": true, + "N_equals_Kprime": false, + "N_equals_KprimeT": true, + "N_targets_touched": 111, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": false, + "T_offdiagonal": [ + [ + 506, + 374 + ], + [ + 507, + 355 + ], + [ + 514, + 367 + ] + ], + "U_block_form": true, + "V_identity": true, + "final_targets_y_plus_x": true + }, + "base": { + "C_Uprime_T_identity": true, + "C_Uprime_identity": true, + "C_full_frame_z_only": true, + "D_entry_frame_zero": true, + "D_frame_zero": true, + "D_no_target_feeds_helper": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_y_plus_Nh": true, + "J_identity": true, + "N_equals_Kprime": true, + "N_equals_KprimeT": true, + "N_targets_touched": 111, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "T_offdiagonal": [], + "U_block_form": true, + "V_identity": true, + "final_targets_y_plus_x": true + } + } + }, + "PR1188": { + "chronology": { + "absorbing_gate_is_first_A_touch": true, + "cuts": 2821, + "cuts_with_difference": 459, + "differing_centres_stay_at_zero_frame": true, + "frames_identical_at_every_cut": true, + "max_registers_differing": 3 + }, + "columns": 661, + "controls": [ + [ + "omit restorations without the A edit", + "dirty endpoint wrong on 102 registers {'helper': 3, 'target': 99}; clean-helper endpoint passes" + ], + [ + "A edit with the literal cleanup of the edited A", + "dirty helpers [506, 507, 514] end as centre+leaf; clean helpers pass" + ], + [ + "A edit with literal cleanup, owner checker", + "owner checker rejects: helpers not restored: [506, 507, 514]" + ], + [ + "absorption after the first centre read (A[853] for centre 506)", + "dirty boundary fails" + ], + [ + "wrong substitute register ([72] instead of [69] at A[288])", + "dirty boundary fails" + ], + [ + "frame-illegal substitution (centre 234, A[247], new [9])", + "illegal frame move: register 9 frame 115 -> 11" + ], + [ + "splice absorbed A/B/C with PR589 D", + "owner checker rejects: helpers not restored: [506, 507, 514]" + ], + [ + "corrupted source pin", + "source pin mismatch: research/r439-gl5-shortest/candidate.json.gz" + ] + ], + "directions": 2, + "exporter": { + "absorbed": { + "ADD": 10489, + "B": 3748680, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 13667, + "MOVE": 2911, + "payload_bits": 91, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "record_sha256": "2b4da8c826c816b58ea05f1b2906df46379e20da8d1e2bbd7e84430d99f0973f", + "records": 13418 + }, + "base": { + "ADD": 10492, + "B": 3758418, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 13667, + "MOVE": 2911, + "payload_bits": 91, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "record_sha256": "2df55087c71725651b7fc531323a371810f6c8c6d49d84d2c397bdc2d1862133", + "records": 13421 + } + }, + "first_climbs": { + "absorbed": { + "helpers_climbing_from_zero": 439, + "non_own_value": [ + 506, + 507, + 514 + ], + "targets_climbing_in_D_or_A": 0 + }, + "base": { + "helpers_climbing_from_zero": 439, + "non_own_value": [], + "targets_climbing_in_D_or_A": 0 + } + }, + "literal": { + "absorbed": { + "ADDs": 10489, + "A_ADDs": 1626, + "B": 3748680, + "C_ADDs": 1991, + "D_ADDs": 5545, + "F": 13667, + "local_bits": 91, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 175 + }, + "base": { + "ADDs": 10492, + "A_ADDs": 1626, + "B": 3758418, + "C_ADDs": 1991, + "D_ADDs": 5548, + "F": 13667, + "local_bits": 91, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 175 + } + }, + "moves": [ + [ + 506, + 374, + 288, + [ + 69 + ] + ], + [ + 507, + 355, + 290, + [ + 72 + ] + ], + [ + 514, + 367, + 304, + [ + 360 + ] + ] + ], + "owner": { + "absorbed_false": [ + "H2_D_frame0_targets_from_helpers", + "H4_C_literal_reverse_at_full", + "K_equals_D", + "C_is_U_inverse" + ], + "absorbed_true": 5, + "base_false": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D" + ], + "original_D_splice_all_true": true + }, + "paths_registers": 661, + "payload": "absorbed-pr1188.json.gz", + "payload_sha256": "72a28b93811e7f175dd824079f776dfde41eda7482bb86db01e153d84cff3931", + "perturbations_rejected": 1980, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "twisted": { + "absorbed": { + "C_Uprime_T_identity": true, + "C_Uprime_identity": false, + "C_full_frame_z_only": true, + "D_entry_frame_zero": true, + "D_frame_zero": true, + "D_no_target_feeds_helper": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_y_plus_Nh": true, + "J_identity": true, + "N_equals_Kprime": false, + "N_equals_KprimeT": true, + "N_targets_touched": 111, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": false, + "T_offdiagonal": [ + [ + 506, + 374 + ], + [ + 507, + 355 + ], + [ + 514, + 367 + ] + ], + "U_block_form": true, + "V_identity": true, + "final_targets_y_plus_x": true + }, + "base": { + "C_Uprime_T_identity": true, + "C_Uprime_identity": true, + "C_full_frame_z_only": true, + "D_entry_frame_zero": true, + "D_frame_zero": true, + "D_no_target_feeds_helper": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_y_plus_Nh": true, + "J_identity": true, + "N_equals_Kprime": true, + "N_equals_KprimeT": true, + "N_targets_touched": 111, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "T_offdiagonal": [], + "U_block_form": true, + "V_identity": true, + "final_targets_y_plus_x": true + } + } + } + }, + "new_kappa_claim": false, + "status": "PASS_R439_TWISTED_STAR_ABSORPTION" +} diff --git a/research/r439-twisted-star-absorption-seed02/PROOF.md b/research/r439-twisted-star-absorption-seed02/PROOF.md new file mode 100644 index 0000000000..16c44dc821 --- /dev/null +++ b/research/r439-twisted-star-absorption-seed02/PROOF.md @@ -0,0 +1,215 @@ +# Twisted helper contract and single-edge absorption: proofs + +This note proves four statements: + +1. the scalar twisted-contract lemma; +2. uniqueness of the substitute register set; +3. the single-edge absorption criterion; +4. the chronological per-cut comparison for the two instances. + +It also names the inherited physical premise that the instances use for helpers. Item 4 and that +premise are confined to the two fixed words. The scalar lemma does not by itself give a +chronological bridge for an arbitrary word that satisfies the twisted contract. `verify.py` checks +every finite fact used here. + +## Notation + +A word has `n = 2v + R` registers: sources `x` (v of them), targets `y` (v) and helpers `h` (R). +Write `z = (x, h)`. Here `v = 111`, `R = 439` and `n = 661`. The word runs D, then A, then the +scatter, then B, then C. The scatter is realised literally: COPY one retained helper into a clean +temporary, ADD that temporary into the listed targets, then ERASE it. Each ADD `d ^= s` is an +elementary transvection over F2. + +Let M be any F2-module. This includes arbitrary F2-valued streams under pointwise addition. A +finite product of elementary transvections has coefficients in F2 and acts on `M^n` through those +coefficients. Two such programs therefore agree on every M exactly when their coefficient matrices +agree, and the n unit columns over F2 determine a coefficient matrix. "Boundary" below always means +the complete coefficient matrix on all 661 columns. Helper inputs are arbitrary ("dirty"), never +assumed to be zero. + +The raw word is `W0' = (A, scatter, B)`, without D and without C. Its block form is described below. +The inherited checker conditions (eumemic's PR555 adaptation, `xcheck_p.py`) are: + +- **H1**: no gate anywhere whose destination is a z register reads a target. +- **H3**: A writes only z registers. The scatter reads only retained helpers and writes only targets. + Each B gate either writes a z register from z registers, or writes a target. +- **H5**: the target-to-target block V of `W0'` is the identity. +- **J**: the raw source response J is the identity. As PR1194 noted, H1–H5 alone do not imply this + for an arbitrary word, so it is checked separately. + +## 1. The twisted contract + +The contract keeps H1, H3, H5 and `J = I`, and replaces H2, H4 and the K check by: + +- **H2-tw.** Every D gate is at the zero frame. Its operands are distinct targets and helpers only, + so D is source-free. D contains no COPY, ERASE or climb: targets and helpers enter D at the zero + frame and stay there. D's complete operator is + `(x, y, h) -> (x, y + N h, T h)` + for a binary v-by-R matrix N and an invertible binary R-by-R matrix T. T acts on helpers only. +- **H4-tw.** Every C gate has a z destination, reads only z registers and runs at the full frame. + All z registers end at the full frame. On z, C satisfies + `C · U' · (I_x ⊕ T) = I`. +- **K-tw.** `N = K' T`, where K' is the helper block of the raw target response of `W0'`. + +**Lemma.** Under H1, H2-tw, H3, H4-tw, H5, `J = I` and K-tw, the complete word maps +`(x, y, h) -> (x, y + x, h)` on every F2-module M. Assume the kept conditions and the structural +clauses of H2-tw (D's operator form) and of H4-tw (C z-only at the full frame). Then the equations +`C U' (I ⊕ T) = I` and `N = K'T` are also necessary for this boundary. + +*Proof.* By H1 and H3, no z register is ever written from a target in A or B, and the scatter +writes only targets. By induction over the gates, every z output of `W0'` is a combination of z +inputs. This gives the block form + + z' = U' z, y' = V y + J x + K' h. + +D sends `(x, y, h)` to `(x, y + N h, T h)`. Applying `W0'` to that state gives + + z' = U' (x, T h) = U' (I ⊕ T) z, + y' = V (y + N h) + J x + K' T h = y + x + (N + K' T) h, + +using `V = J = I`. C writes and reads only z registers, so it leaves y unchanged. It sends z' to +`C U' (I ⊕ T) z = z`. The final state is `(x, y + x + (N + K'T) h, h)`, and `N + K'T = 0` by K-tw. +Every coefficient lies in F2, so the identity holds on every M. + +For necessity, assume the kept conditions and the boundary `(x, y + x, h)`. On the z unit columns +in F2 the z rows give `C U' (I ⊕ T) = I`, and on the helper unit columns the target rows give +`N + K'T = 0`. ∎ + +**Strict weakening.** Setting `T = I` turns H2-tw into PR1194's H2-sem condition 3, +`(x, y, h) -> (x, y + N h, h)`. H4-tw becomes `C U' = I`, the `C = U^-1` conclusion that PR1194 +draws from the literal-reverse H4. K-tw becomes `N = K`. Every word meeting PR1194's contract +therefore meets the twisted contract with `T = I`. The two instances below meet the twisted contract +with `T ≠ I`. They fail H2-sem because D leaves three helpers unrestored. They also fail `C U' = I` +and the literal H4. The weakening is therefore strict. + +**The cleanup is weakened even at `T = I`.** The converse of the containment above fails already +at `T = I`. There, H4-tw is the semantic `C U' = I`, whereas PR1194 keeps the literal-reverse H4. +PR1311's stale-cleanup control (PR1122's word with PR589's C) satisfies every twisted condition +with `T = I` and the dirty boundary, yet the lineage rejects it. Endpoint success alone does not give +a chronological bridge for a non-literal full-frame cleanup. + +The instances avoid this: their C is byte-identical to the base word's literal C, and section 4 +bridges them cut by cut. Adopting H4-tw as a general interface would need such a bridge for +non-literal cleanups. + +## 2. The substitute set is unique + +Start the replay from the identity state. The state at a cut is the 661-by-661 matrix whose rows +are the current register values as vectors over the input columns. No temporary is live inside D +or A. Each ADD multiplies this matrix by an elementary transvection. The state is therefore +invertible over F2 at every D/A cut. + +For any vector δ there is then exactly one register set S whose current values XOR to δ. Its +indicator is `δ^T` times the inverse state matrix. `verify.py` maintains the inverse column by +column: `d ^= s` maps inverse column s to `col_s + col_d`. It then checks every computed S by +direct summation. + +## 3. Single-edge absorption criterion + +Let `e` be a trailing D restoration `a ^= b`. Let δ be b's value just before e; on all four lineage +words this is b's own input column. Let g be a later gate writing a, with source set Sg, such that +no gate strictly between e and g reads a. Let S be the unique set with value sum δ at the cut just +before g in the original word W. Suppose a is not in S. + +**Criterion.** Delete e and change only g's source set to some S' with a not in S'. The resulting +word W'' has W's complete boundary (forward literal COPY/ERASE replay, all 661 dirty columns) if +and only if + + S' = Sg ⊕ S. + +The ADD saving is `1 + |Sg| − |Sg ⊕ S|`. If `Sg ⊕ S` is empty, g is deleted as well. + +*Proof.* The two replays agree up to e. Between e and g, induction over the gates shows that W'' +differs from W only in register a, by exactly δ. No gate in that window reads a. A gate writing a +uses identical source values in both words, and every other gate sees identical operands. At g, +all registers other than a agree, so the S' sum is the same in both replays. After g, + + a_W = a + Σ Sg, a_W'' = a + δ + Σ S'. + +These are equal exactly when `Σ (S' ⊕ Sg) = δ` in W's state. By uniqueness this holds exactly when +`S' ⊕ Sg = S`. + +After g, W and W'' execute the same instruction sequence. If their states agree after g, their +complete boundaries agree, including the clean-temporary conditions. Conversely, the common suffix +is injective on states where those conditions hold. An ADD is invertible on rows. A COPY into a +zero temporary and the matching ERASE are mutually inverse on that domain. Equal final boundaries +therefore force equal states after g. The reverse replay is the inverse program, so the forward +statement transfers to it. ∎ + +Frame legality is a separate constraint. The new operands of g must be able to climb monotonically +to g's frame, and the ordered frame paths must stay unchanged. The census therefore classifies each +move twice: by its F2 boundary (always exact under the criterion) and by its frame legality. + +**Census class.** For each trailing restoration of a lineage word, the census considers every A +gate g that writes the centre a before a's first read. On all four words, each centre is first +read in A or by the scatter COPY, so no B or C gate can precede that read. The only other writers +of a before the read are the other restorations of the same centre in the D tail. Leaves are never +written in D, so for those pairs `S = {b}` and the saving is `1 + 1 − 2 = 0`. The census replays and +counts these pairs separately. Preparations of a are separated from e by target-block reads of a. +`verify.py` checks every part of this case analysis. + +**Joint moves.** Several moves with distinct centres and distinct gates compose provided every +`S_i` avoids the other centres whose differences are still pending at `g_i`. The two instances +satisfy this. The lockstep replay in Section 4 checks it directly. + +## 4. Chronological per-cut comparison for the instances + +Let W be the PR1062 or PR1188 word and W' its absorbed word. W' deletes three restorations and +edits A gates 288, 290 and 304. `verify.py` replays the D and A prefixes of W and W' in lockstep, +with frames, and checks the following at every cut (3,270 cuts for PR1062 and 2,821 for PR1188): + +- The registers that differ are exactly the centres whose restoration has been deleted and whose + absorbing gate has not yet run. Each differs by exactly its leaf's input column. At most three + registers differ, at 459 cuts. +- Every register is at the same frame in W and W' at every cut. This is stronger than equal ordered + frame paths, and the exporter's ordered per-register MOVE records also agree. +- Every differing centre stays at the zero frame until its absorbing gate. Each absorbing gate is + the first A gate that touches its centre. +- After A[304] the full states are equal. The remaining scatter, B and C instructions are + identical. + +**Physical reading.** For W, the chronological realization comes from PR1194. A proof-only word +with W's A/scatter/B/C and PR589's target-only D passes every inherited owner flag. Its zero-frame D +and W's D have the same complete operator, values and frames, so they give pointwise identical +states before the unchanged continuation. `verify.py` re-checks this splice and the D-operator +equality for both base words. PR1311 did the same for PR1122. + +W' and W agree in logical value and frame at every cut except the three pending centres. Each of +those centres sits at the zero frame holding `a + b` (its own input column plus the leaf's input +column). It then climbs to its absorbing gate's frame f, and at that frame immediately receives the +compensating ADD from registers already at f. + +The step from equal logical states to equal physical states after that gate uses one inherited +premise: + +> **Common-frame / climb additivity.** Identical ordered per-register frame paths plus identical +> logical values give identical physical states, across nonzero frames. Equivalently, the physical +> climb of a sum is the sum of the climbs, and additions at a common frame are additive. + +Targets already rely on this premise: after D they climb holding the dirty combination `y + N h`. +PR1194 deliberately restricted its own substitution to frame-zero prefixes and did not apply the +premise to helpers. This package newly uses it for helpers. The verifier's first-climb census +locates the use exactly. On both base words, every helper's first climb out of the zero frame +carries its own input column. On both absorbed words, exactly helpers 506, 507 and 514 first climb +carrying a non-own value, and none of them climbs again before its compensation. + +Nothing more is claimed physically. The verifier does not evaluate the premise numerically. Native +5/9/11-stage replay, hosted emission, all-size compiler, rounding/tape and analytic obligations +remain inherited and unexecuted here. + +## Accounting consequence + +Only three D ADDs disappear, so the D ADDs fall from 5,548 to 5,545. The three absorbing A gates +keep one source each, and C is byte-identical to the base word's C. That C is the literal reverse +of the original A/B z-gates, which is why the inherited literal H4 and `C_is_U_inverse` flags are +false. + +The following are all unchanged: + +- frames and climbs; +- COPY ranks; +- the paid profile `{1:1323, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:19}`, rank mass 5,129; +- 2,911 MOVE records. + +The forward positive bound F is unchanged and the reverse bound B falls slightly. Both strict +precision guards keep their bit lengths. Exact values are in `EXPECTED.json` and `README.md`. diff --git a/research/r439-twisted-star-absorption-seed02/README.md b/research/r439-twisted-star-absorption-seed02/README.md new file mode 100644 index 0000000000..84bd783832 --- /dev/null +++ b/research/r439-twisted-star-absorption-seed02/README.md @@ -0,0 +1,247 @@ +# Twisted helper contract: helper-star restorations absorbed into A + +**Replacement-interface result with finite R439 instances. No new κ, and the bit side does not +bind.** The selected result, the selected bit supplier (PR589) and `upstream/` are unchanged. + +## The interface result + +PR1194's semantic-D contract lets D mix helpers temporarily. D must still return every helper: +`(x, y, h) -> (x, y + N h, h)`. This package weakens that requirement. D may leave the helpers +**twisted** by any invertible helper-only map T, provided the cleanup absorbs the twist: + +| | inherited / PR1194 | twisted contract | +|---|---|---| +| D operator | `(x, y + N h, h)` | `(x, y + N h, T h)`, T helper-only and invertible | +| D shape | zero frame, source-free, no COPY/ERASE/climb | same | +| cleanup C | literal reverse of A/B z-gates, so `C U = I` | z-only at the full frame, `C · U' · (I ⊕ T) = I` on z | +| target response | `N = K` | `N = K' T` | +| H1, H3, H5, `J = I` | kept | kept | + +Block algebra gives `y + x + (N + K'T) h = y + x` on every F2-module. Assume the kept conditions +and the structural clauses (D's operator form, and C being z-only at the full frame). Then the two +new equations are necessary and sufficient for the dirty boundary `(x, y, h) -> (x, y + x, h)`. + +**How it weakens PR1194, in two places.** + +- **The cleanup is weakened even at `T = I`.** Every PR1194 word meets the twisted contract with + `T = I`, but the converse fails at `T = I`. H4-tw replaces the literal-reverse cleanup by the + semantic condition `C U' (I ⊕ T) = I`. PR1311's stale-cleanup control satisfies the twisted + contract at `T = I`, yet the lineage rejects it: an endpoint alone does not give a chronological + bridge for a non-literal cleanup. +- **The helpers may stay twisted.** The instances below have `T ≠ I`. + +The two instances are not exposed to the first point. Their C is byte-identical to the base word's +literal C, and they are bridged cut by cut. + +[PROOF.md](PROOF.md) gives the lemma, the uniqueness of the substitute register set, the exact +single-edge criterion and the chronological per-cut argument. + +**Newly used premise.** The instances rely on the inherited common-frame / climb-additivity +premise, now applied to helpers: identical ordered per-register frame paths plus identical logical +values give identical physical states, across nonzero frames. Targets already rely on it, since +they climb holding `y + N h`. PR1194 deliberately restricted its substitution to frame-zero prefixes. +Here exactly three helpers (506, 507, 514) make their first climb out of the zero frame while +holding `centre + leaf`. Each does so at its absorbing gate, which immediately compensates. Nothing +beyond this premise is claimed about physical realization. + +## The helper-mixing word + +A helper-star restoration is the D gate `a ^= b` (centre a, leaf b). Delete it, and replace the +source set Sg of an A gate that writes a before a's first read by `Sg ⊕ S`. Here S is the unique +register set whose current values sum to b's input column. The state is invertible over F2 at every +cut, so S is unique. This preserves the whole boundary **if and only if** the new source set is +exactly `Sg ⊕ S`. + +The three frame-legal positive moves are the same on every lineage word: + +| deleted D restoration | absorbing A gate | old sources | new sources | +|---|---|---|---| +| `506 ^= 374` | A[288] at frame 71 | `[374]` | `[69]` | +| `507 ^= 355` | A[290] at frame 74 | `[355]` | `[72]` | +| `514 ^= 367` | A[304] at frame 65 | `[367]` | `[360]` | + +In each case A has already performed `leaf ^= substitute` at the same frame. The centre therefore +reads the substitute in place of the updated leaf. C is left byte-identical. The words are +[absorbed-pr1062.json.gz](absorbed-pr1062.json.gz) and [absorbed-pr1188.json.gz](absorbed-pr1188.json.gz). + +| complete local quantity | PR1062 word | absorbed | PR1188 word | absorbed | +|---|---:|---:|---:|---:| +| ADDs | 11,500 | **11,497** | 10,492 | **10,489** | +| D / A / C ADDs | 5,548 / 2,130 / 2,495 | 5,545 / 2,130 / 2,495 | 5,548 / 1,626 / 1,991 | 5,545 / 1,626 / 1,991 | +| exporter records (ADD / COPY / ERASE / MOVE) | 14,429 (11,500 / 9 / 9 / 2,911) | 14,426 (11,497 / 9 / 9 / 2,911) | 13,421 (10,492 / 9 / 9 / 2,911) | 13,418 (10,489 / 9 / 9 / 2,911) | +| forward / reverse positive bound F / B | 25,717 / 5,911,840 | 25,717 / 5,858,638 | 13,667 / 3,758,418 | 13,667 / 3,748,680 | +| local / nine-stage bits (strict caps 104 / 192) | 95 / 182 | 95 / 182 | 91 / 175 | 91 / 175 | + +For both absorbed words, `verify.py` checks the following: + +- **Boundary and frames.** The boundary is `(x, y, h) -> (x, y + x, h)` on all 661 dirty columns, + forward and reverse, through the literal COPY/ERASE stream. Every register has the same frame at + every D/A cut. The ordered per-register frame paths and exporter MOVE records are identical to + the base word's and to PR589's. +- **Paid profile.** It is `{1:1323, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:19}`, rank mass 5,129, with + nine rank-7 COPYs. It is recomputed from frame paths and from the pinned exporter + (`research/e8-bit-carrier-skeleton/code/bit/export_records.py`). +- **Owner checker.** The unchanged `research/e8-bit-p111-tuned/code/xcheck_p.py` accepts the + complete geometry and endpoint. Exactly four flags are false: + `H2_D_frame0_targets_from_helpers`, `H4_C_literal_reverse_at_full`, `K_equals_D` and + `C_is_U_inverse`. All five others are true. The base words carry only the first and third. +- **Twisted identities.** `T ≠ I`, with off-diagonal entries exactly (506,374), (507,355) and + (514,367). T is invertible and helper-only. The checks also give `C U' (I_x ⊕ T) = I` and + `C U' ≠ I`, + `N = K'T` and `N ≠ K'`, and `V = J = I` with U in block form. D is frame-zero and source-free, + and C is z-only at the full frame. +- **Base-word bridge.** The PR1194-style splice of each base word with PR589's D passes every owner + flag, and each base D operator equals PR589's on all 661 columns. +- **Chronology.** A lockstep replay covers 3,270 cuts (PR1062) and 2,821 cuts (PR1188). At each cut + the differing registers are exactly the pending centres, each off by its leaf column. At most + three registers differ, at 459 cuts, and they stay at the zero frame. Each absorbing gate is the + first A gate touching its centre. +- **Uniqueness.** All 1,980 one-register perturbations of the three new source sets break the dirty + boundary. + +## Single-edge census + +The census covers every pair (trailing D restoration, A gate writing its centre before the centre's +first read) on four lineage words. Every pair's edited word is replayed on all 661 dirty columns in +both directions, and all of them preserve the boundary, as the criterion predicts. Frame legality +and the ordered frame paths are then checked separately. + +| word | star edges | pairs | gain histogram | positive | frame-illegal | admitted | +|---|---:|---:|---|---:|---:|---:| +| PR967 | 221 | 445 | −10:1 −8:1 −7:1 −6:21 −5:25 −4:5 −3:15 −2:45 −1:169 0:114 +1:48 | 48 | 45 | 3 | +| PR1062 | 236 | 481 | −10:1 −8:1 −7:1 −6:25 −5:30 −4:6 −3:12 −2:45 −1:192 0:120 +1:48 | 48 | 45 | 3 | +| PR1122 | 236 | 489 | −10:2 −9:2 −8:1 −7:2 −6:7 −5:14 −4:10 −3:27 −2:50 −1:203 0:123 +1:48 | 48 | 45 | 3 | +| PR1188 | 236 | 470 | −10:2 −9:2 −8:1 −7:2 −6:5 −5:13 −4:8 −3:20 −2:52 −1:195 0:123 +1:47 | 47 | 44 | 3 | + +On every word the three admitted moves are the triples above. Every negative-gain move is +frame-illegal. Among the gain-0 moves, two keep identical paths, two are legal but change paths, +and the rest are frame-illegal. + +Some centres are never read in A: on each word, 6 star edges have a centre that is first read by +the scatter COPY. The only other writers of a centre before its first read are its other D-tail +restorations: 128 pairs on PR967 and 148 on the others. All of them have gain exactly 0 and are replayed exactly. No B or +C gate precedes a first read. All counts are pinned in [EXPECTED.json](EXPECTED.json). + +## Controls (each instance; all must fail or be rejected) + +1. **Omit the restorations without the A edit.** The dirty endpoint is wrong on 102 registers + (99 targets and 3 helpers). The clean-helper endpoint passes, which makes this a dirty-input + counterexample. +2. **A edit with the literal cleanup of the edited A** (inherited literal H4 enforced). The result + fails exactly on dirty helpers 506, 507 and 514, which end as centre + leaf. It passes on clean + helpers, and the owner checker rejects it with `helpers not restored: [506, 507, 514]`. +3. **Absorption after the first centre read** (PR1062 A[1218] for centre 514; PR1188 A[853] for + centre 506). The dirty boundary fails. +4. **Wrong substitute register** (`[72]` instead of `[69]` at A[288]). The dirty boundary fails. +5. **One frame-illegal substitution** (centre 234, A[247], new source `[9]`). Its F2 boundary is + exact, but the frame replay rejects it: register 9 cannot move from frame 115 to frame 11. +6. **PR1194/PR1311-style splice** (absorbed A/B/C with PR589's target-only D). The owner checker + rejects it with `helpers not restored: [506, 507, 514]`. +7. **Corrupted source pin.** The SHA-256 check rejects it. + +## Reproduce + +From the repository root (standard library only, about 20 s per run on an Apple-silicon Mac): + +```sh +python3 -I -B research/r439-twisted-star-absorption-seed02/verify.py +python3 -I -O -B research/r439-twisted-star-absorption-seed02/verify.py +python3 scripts/research_package.py --package research/r439-twisted-star-absorption-seed02 --check-only +python3.12 scripts/research_package.py --package research/r439-twisted-star-absorption-seed02 +``` + +The expected final line is: + +```text +PASS_R439_TWISTED_STAR_ABSORPTION words=4 instances=2 ADDs 11500->11497 10492->10489 columns=661 controls=16 no_new_kappa (… s) +``` + +All seven inputs are pinned by SHA-256 in [SOURCES.json](SOURCES.json): four lineage words, +PR589's word, the owner checker and the exporter. The verifier refuses drifted bytes. It executes +the owner checker from the verified bytes in-process; that checker raises its own `Reject`, not +`assert`. It runs the exporter from the verified bytes in a child interpreter without `-O`. Checks +raise `ValueError`, so `-O` cannot weaken them. The report must equal EXPECTED.json exactly, and +the committed absorbed words must equal the rebuilt ones. `--write` regenerates both. The report is +identical under CPython 3.12.15 and 3.14.8. + +## Scope and limits + +- **Class.** The census covers only the single-edge, single-writer class: one deleted restoration + absorbed by one edited gate. Joint application of the three admitted moves is checked; this is + not a global minimum or an unrestricted circuit optimum. +- **New result.** The new content is the interface lemma, its finite instances and the census. The + three-ADD saving is a small finite consequence. It does not change the paid profile, the selected + moment or κ. +- **Not run.** Native 5/9/11-stage C++ replay was not run on the absorbed words. Open PR #1509's + checked `cpp_int` stand-in may make that possible on hosts without Boost. Hosted + emission/invoice and outer assembly were not rerun either. All-size compiler, + common-label/mutable-source, rounding/tape and analytic obligations remain inherited. +- **Physical realization.** It is argued only for the two instances. The argument uses the + per-cut comparison with the PR1194-bridged base words and the climb-additivity premise stated + above. The scalar lemma alone is not a chronological bridge for arbitrary twisted words. +- **Terminal-restoration exclusions.** Open PRs #1580 and #1592 rule out moving restorations to + the end of C and arbitrary terminal compensation. Absorption happens before the centre's first + read and changes A, so it lies outside their terminal domain and is consistent with them. + #1592's stated next question was to move the cut earlier and change the continuation; this + package answers it for the centre-writer class. + +## Concurrent work on the same card and words + +None of these uses the twisted mechanism: none leaves helpers twisted (`T ≠ I`), and none edits A +to absorb a D restoration. + +- **Same base word, other mechanisms.** These open PRs work on PR1062's 11,500-ADD word: + - #1543 (ToikY): two nonpositive helper moves, 11,500 → 11,489; + - #1709 (Cinna Davis, @1337isnot1337): a five-helper cycle, 11,500 → 11,488; + - #1704 (Ross Richardson): a two-copy scatter under a replacement immutable-temporary interface, + 11,500 → 11,380. + + Their scalar savings are larger than this package's three ADDs. Whether the three absorptions + compose with them has not been tested. +- **Restored-helper (H2-sem) work.** #1782 (Aaron Wang) and #1805 (VictorLiwentao) admit and price + PR848's helper-sharing wraps under PR1194's contract, with `N = K` and `T = I`. That is a + different object. +- **Terminal deferral.** Discussion #1743 (Cinna Davis) claimed compensated terminal deferral; it + expired with no PR. That domain is the terminal one PR1592 already excludes. + +## Open next questions + +The structured versions are in [TASK.json](TASK.json). + +1. **Multi-gate splits and the neutral moves.** Can a restoration be absorbed by splitting S across + two or more centre writers, or by chaining one of the gain-0 moves (two path-preserving per + word) with a positive one? The single-edge census excludes these by construction. *First step:* + extend the census to two-writer splits of S, on the same frame-legality filter. +2. **Native replay of the absorbed words.** *First step:* run PR1188's native 5/9/11-stage + checkers on `absorbed-pr1188.json.gz`, with Boost or PR #1509's stand-in. *Blocker:* a host with + Boost or an accepted stand-in. +3. **Feedback results with a twisted helper exit.** PR1706 (with PR1306/PR1557) finds no + target-feedback saving for fully restored dirty shears, which is the `T = I` case. Does any + feedback or shear gain appear once the helper exit may be permuted or twisted (`T ≠ I`) and + absorbed by C? *First step:* rerun the 3-by-3 shear census allowing any helper exit T in + `GL(R, 2)`, and charge the C absorption. +4. **Adoption of the twisted contract.** Would maintainers accept H2-tw/H4-tw/K-tw, together with + the helper climb premise, as the interface for hosted admission? + - *Why it needs more than the premise:* adopting H4-tw as a general interface also needs a + chronological bridge for non-literal full-frame cleanups. PR1311 declined to infer one from + endpoint success, and the helper climb premise does not cover it. + - *How the instances avoid it:* they keep the base word's literal C. + - *Blocker:* a maintainer decision, then a hosted emission of an absorbed word. + +## Credit + +- **Interface and checker lineage.** woklerx's PR1194 semantic-D contract and frame-zero + substitution argument; Arham Tahir's PR1311 bridge on the composed word; Zhihao Chen's PR425 + scalar-interface lemma; eumemic's PR555 checker adaptation (`xcheck_p.py`); Dylan Crow's exporter. +- **Lineage words.** Sricharan Vagvala (@theon199): PR967 helper stars. Sagar Thakrar: PR1062 + B-block and helper-star D composition. Gareth Davidson (@bitplane): PR1122 A/B/star composition + and PR1188 GL5 windows. Aaron Wang's PR1015 and Ross Richardson's PR923 B circuits are inside + those words. DreamingOfClouds' PR589 tuning sits on eumemic's PR555 punctured word. +- **Terminal-restoration exclusions.** Arham Tahir's open PRs #1580 and #1592. +- **Restoration-coalescing lineage.** #1155 (Aaron Wang, open), #1199 (Sagar Thakrar), #1203 + (mightyOil) and #1205 (Adam Gall). +- **Concurrent same-card work.** Cited above: #1543, #1704, #1709, #1782, #1805 and the #1743 + claim. #1592's next question motivated the early-cut absorption. + +Prepared by Sagar Thakrar with substantial Anthropic Claude assistance (Claude Code, including +subagents for the probes). No independent human review. New work is Apache-2.0. diff --git a/research/r439-twisted-star-absorption-seed02/SOURCES.json b/research/r439-twisted-star-absorption-seed02/SOURCES.json new file mode 100644 index 0000000000..aa18fb221c --- /dev/null +++ b/research/r439-twisted-star-absorption-seed02/SOURCES.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/bit/export_records.py", + "usage": "input", + "git_blob": "3632d370486a02f5456f7643ced03f8c925b2350", + "sha256": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3" + }, + { + "path": "research/e8-bit-p111-tuned/code/xcheck_p.py", + "usage": "input", + "git_blob": "184f5dcf94a486cc7db91ca4db5865916bf26009", + "sha256": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e" + }, + { + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "usage": "input", + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + { + "path": "research/r439-abc-star-composition/candidate.json.gz", + "usage": "input", + "git_blob": "0ab597fefd68bfefecc85d631b172d174bdaeb70", + "sha256": "2b09a7a3851cdf2a7f19350d1555cf75788d001c9507a37e459cd931881ee066" + }, + { + "path": "research/r439-bsection-stars-seed01/candidate.json.gz", + "usage": "input", + "git_blob": "9a17b4920334878d6c949191f6931bd97126fe3c", + "sha256": "b452d2c2b0b2a546d1105b1da9769aa78e5c54d6f00e97b30c77e3f54ce445ee" + }, + { + "path": "research/r439-gl5-shortest/candidate.json.gz", + "usage": "input", + "git_blob": "0d4dd2fb241a00cab1b57b17991db82bc06edd91", + "sha256": "4e7904d01ebdbfc60a26472b4e0d2e813c19c2fe1a4bb8ab390c12746a1da359" + }, + { + "path": "research/r439-helper-stars-seed19/candidate.json.gz", + "usage": "input", + "git_blob": "8b0210d8b8e9524182e5f54f9bf93c28f4719735", + "sha256": "d8b08885e8ce9868200b2645189d15ed18a27fc2742e54990b3257a0ca4df6b8" + } + ] +} diff --git a/research/r439-twisted-star-absorption-seed02/TASK.json b/research/r439-twisted-star-absorption-seed02/TASK.json new file mode 100644 index 0000000000..9fc2bbd7c8 --- /dev/null +++ b/research/r439-twisted-star-absorption-seed02/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "refined", + "actual_scope": "Replace the inherited H2/K (and literal H4) interface by a twisted contract: frame-zero, source-free D may leave the helpers in any invertible helper-only state T, provided C U' (I_x ⊕ T) = I on z and N = K'T. Prove it, exhibit one precisely specified helper-mixing word (three helper-star restorations of the PR1062 and PR1188 words absorbed into A gates before the centres' first reads) with full dirty boundary, unchanged frame paths and paid profile, and run an exhaustive single-edge single-writer census on the PR967, PR1062, PR1122 and PR1188 words.", + "scope_change_reason": "PR1194 and PR1311 already cover the T = I semantic-D replacement for words whose D restores every helper. This package narrows, as the card allows, to one helper-star absorption class and weakens the contract further to unrestored (twisted) helpers, which the absorbed words need. It does not attempt hosted adoption, native replay or a global optimum.", + "bottleneck_link": "Side result on the bit supplier. A legitimate replacement interface admits a cheaper helper-mixing word (3 complete ADDs fewer) with an unchanged paid profile and rank mass, so the selected moment and kappa are unchanged; the bit side does not bind.", + "budget_minutes": 60, + "stop_rule": "Stop after the twisted lemma, the two fixed instances, the single-edge single-writer census on four lineage words and the seven controls; no multi-gate search, native replay or hosted emission.", + "outcome": "completed", + "evidence": "EXPECTED.json, PROOF.md, absorbed-pr1062.json.gz and absorbed-pr1188.json.gz; python3 -I -B research/r439-twisted-star-absorption-seed02/verify.py prints PASS_R439_TWISTED_STAR_ABSORPTION.", + "author": "Sagar Thakrar", + "ai_assistance": "Prepared by Sagar Thakrar with substantial Anthropic Claude assistance (Claude Code, including subagents for the exploratory probes and package assembly). No independent human review.", + "open_questions": [ + { + "question": "Can a helper-star restoration be absorbed by splitting its substitute set across two or more centre writers, or by chaining one of the gain-0 neutral moves (120 on the PR1062 word, two of them path-preserving) with a positive move?", + "why_it_matters": "The census is exhaustive only for one deleted restoration and one edited gate; multi-gate absorption could admit further frame-legal savings under the same twisted contract.", + "first_step": "Extend the census to two-writer splits of S before the first centre read, with the same frame-path filter.", + "blocked_by": "Search budget only; the candidate space grows quadratically in the centre writers per edge." + }, + { + "question": "Do the absorbed words pass the native 5/9/11-stage C++ checkers that PR1122 and PR1188 ran on their base words?", + "why_it_matters": "This package checks local scalar, frame and precision facts only; native multistage replay is the next layer of evidence.", + "first_step": "Run the PR1188 native checkers on absorbed-pr1188.json.gz with Boost, or with open PR #1509's checked cpp_int stand-in.", + "blocked_by": "A host with Boost headers or an accepted stand-in; not run here." + }, + { + "question": "Do target-feedback or shear savings appear once the helper exit may be twisted (T != I) and absorbed by C?", + "why_it_matters": "PR1706 (with PR1306 and PR1557) finds no feedback saving for fully restored dirty shears, the T = I case; the twisted contract enlarges that model.", + "first_step": "Rerun the 3-by-3 shear census allowing any helper exit T in GL(R,2) and charge the C absorption.", + "blocked_by": "A cost convention for the C absorption that is consistent with the scalar shear model." + }, + { + "question": "Will maintainers accept the twisted contract, together with the helper common-frame/climb-additivity premise, as an interface for hosted admission?", + "why_it_matters": "Without acceptance the absorbed words remain scoped finite constructions, not supplier candidates.", + "first_step": "Review PROOF.md section 4 against the inherited chronological lemma and PR1194's frame-zero restriction.", + "blocked_by": "Maintainer decision, then a hosted emission and invoice of an absorbed word." + } + ] +} diff --git a/research/r439-twisted-star-absorption-seed02/VERIFY.json b/research/r439-twisted-star-absorption-seed02/VERIFY.json new file mode 100644 index 0000000000..56ae525231 --- /dev/null +++ b/research/r439-twisted-star-absorption-seed02/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/e8-bit-carrier-skeleton/code/bit/export_records.py", + "research/e8-bit-p111-tuned/code/xcheck_p.py", + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "research/r439-abc-star-composition/candidate.json.gz", + "research/r439-bsection-stars-seed01/candidate.json.gz", + "research/r439-gl5-shortest/candidate.json.gz", + "research/r439-helper-stars-seed19/candidate.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "SHA-256 input pins; single-edge census on four lineage words with every move replayed on all 661 dirty columns; two absorbed instances (literal boundary both directions, per-cut frames, MOVE records, paid profile, exporter bill, 104/192-bit guards, owner flags, twisted identities, chronology, 1,980 perturbations each); seven controls per instance; EXPECTED.json and payload equality." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "The same verification under -O: every check raises ValueError and the pinned exporter child runs without -O." + } + ] +} diff --git a/research/r439-twisted-star-absorption-seed02/absorbed-pr1062.json.gz b/research/r439-twisted-star-absorption-seed02/absorbed-pr1062.json.gz new file mode 100644 index 0000000000..7656a7996e Binary files /dev/null and b/research/r439-twisted-star-absorption-seed02/absorbed-pr1062.json.gz differ diff --git a/research/r439-twisted-star-absorption-seed02/absorbed-pr1188.json.gz b/research/r439-twisted-star-absorption-seed02/absorbed-pr1188.json.gz new file mode 100644 index 0000000000..ff8d2cfd04 Binary files /dev/null and b/research/r439-twisted-star-absorption-seed02/absorbed-pr1188.json.gz differ diff --git a/research/r439-twisted-star-absorption-seed02/verify.py b/research/r439-twisted-star-absorption-seed02/verify.py new file mode 100644 index 0000000000..20119640e4 --- /dev/null +++ b/research/r439-twisted-star-absorption-seed02/verify.py @@ -0,0 +1,853 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +# Prepared by Sagar Thakrar with substantial Anthropic Claude assistance. +"""Twisted helper-star absorption on fixed R439 bit words: exact finite verification. + +Checks, from SHA-256-pinned repository inputs only: +* the single-edge census on the PR967, PR1062, PR1122 and PR1188 words: delete one trailing D + helper-star restoration a ^= b, and replace the source set Sg of one A gate writing the centre a + before the first read of a by Sg xor S, where S is the unique register set whose current values + sum to b's input column. Every move is replayed on all 661 dirty columns forward and reverse; + every one-register perturbation of the three admitted new source sets is rejected (iff criterion); +* the two instances (PR1062 and PR1188 words with the three frame-legal positive moves): literal + COPY/ERASE boundary (x,y,h) -> (x,y+x,h) both directions, ordered per-register frame paths and + exporter MOVE records identical to the base word, paid profile and rank mass, exporter bill, + strict 104/192-bit precision guards, the unchanged owner checker's flag pattern, the twisted + identities (T != I, C U' diag(I_x, T) = I, N = K' T, V = J = I), the chronological per-cut state difference + and the first-climb census that isolates the newly used helper climb premise; +* seven controls that must fail or be rejected. +Standard library only. Every check raises ValueError (never assert), so -O cannot weaken it. The +pinned exporter uses assert, so it runs from its verified bytes in a child interpreter without -O. +""" +import argparse +import gzip +import hashlib +import json +import os +import struct +import subprocess +import sys +import tempfile +import time +import types +from collections import Counter +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + +WORDS = { + 'PR967': 'research/r439-helper-stars-seed19/candidate.json.gz', + 'PR1062': 'research/r439-bsection-stars-seed01/candidate.json.gz', + 'PR1122': 'research/r439-abc-star-composition/candidate.json.gz', + 'PR1188': 'research/r439-gl5-shortest/candidate.json.gz', +} +PR589 = 'research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz' +CHECKER = 'research/e8-bit-p111-tuned/code/xcheck_p.py' +EXPORTER = 'research/e8-bit-carrier-skeleton/code/bit/export_records.py' +INPUTS = sorted([*WORDS.values(), PR589, CHECKER, EXPORTER]) + +INSTANCES = {'PR1062': ('absorbed-pr1062.json.gz', 11500, 11497), + 'PR1188': ('absorbed-pr1188.json.gz', 10492, 10489)} +# (centre a, leaf b, absorbing A index, new source set of that A gate) +TRIPLES = [[506, 374, 288, [69]], [507, 355, 290, [72]], [514, 367, 304, [360]]] +PROFILE = {1: 1323, 2: 1342, 3: 79, 4: 44, 5: 102, 6: 11, 7: 19} +OWNER_FALSE = ['H2_D_frame0_targets_from_helpers', 'H4_C_literal_reverse_at_full', 'K_equals_D', 'C_is_U_inverse'] +LOCAL_CAP, NINE_CAP = 104, 192 + + +def need(cond, msg): + if not cond: + raise ValueError(msg) + + +def canonical(w): + return json.dumps(w, sort_keys=True, separators=(',', ':')).encode() + + +def sha(b): + return hashlib.sha256(b).hexdigest() + + +# ------------------------------------------------------------------ pinned inputs + +def check_pin(path, data, pinned): + need(sha(data) == pinned, 'source pin mismatch: ' + path) + + +def load_inputs(): + src = json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8')) + pins = {r['path']: r['sha256'] for r in src['files'] if r['usage'] == 'input'} + need(sorted(pins) == INPUTS, 'SOURCES.json input set differs from the verifier inputs') + man = json.loads((HERE / 'VERIFY.json').read_text(encoding='utf-8')) + need(sorted(man['inputs']) == INPUTS, 'VERIFY.json input set differs from the verifier inputs') + data = {} + for p in INPUTS: + b = (ROOT / p).read_bytes() + check_pin(p, b, pins[p]) + data[p] = b + return data, pins + + +def owner_module(code): + mod = types.ModuleType('r439_owner_xcheck_p') + mod.__file__ = CHECKER + exec(compile(code, CHECKER, 'exec'), mod.__dict__) + return mod + + +# ------------------------------------------------------------------ geometry + +def rank_q(rows): + m = [[Fraction(x) for x in r] for r in rows] + rk = 0 + for col in range(len(m[0]) if m else 0): + p = next((i for i in range(rk, len(m)) if m[i][col] != 0), None) + if p is None: + continue + m[rk], m[p] = m[p], m[rk] + for i in range(len(m)): + if i != rk and m[i][col] != 0: + f = m[i][col] / m[rk][col] + m[i] = [a - f * b for a, b in zip(m[i], m[rk])] + rk += 1 + return rk + + +class Geo: + def __init__(self, w): + self.v, self.R = w['v'], w['R'] + self.n = 2 * self.v + self.R + self.fs = [frozenset(f) for f in w['frames']] + self.fdim = [rank_q([w['lines'][i] for i in f]) if f else 0 for f in w['frames']] + zero = [k for k, d in enumerate(self.fdim) if d == 0] + full = [k for k, d in enumerate(self.fdim) if d == 8] + need(len(zero) == 1 and len(full) == 1, 'one zero and one full frame') + self.ZERO, self.FULL = zero[0], full[0] + self.X = (1 << self.v) - 1 + self.Y = self.X << self.v + self.H = ((1 << self.R) - 1) << (2 * self.v) + + def is_y(self, r): + return self.v <= r < 2 * self.v + + +def same_geometry(a, b): + return all(a[k] == b[k] for k in ('v', 'R', 'h', 'lines', 'frames', 'start', 'final', 'ret', 'scatter')) + + +def frame_paths(w, geo): + fs = geo.fs + ps = [[f] for f in w['start']] + for sec in 'DABC': + for f, d, ss in w[sec]: + for r in (d, *ss): + if ps[r][-1] != f: + need(fs[ps[r][-1]] < fs[f], 'illegal frame move: register %d frame %d -> %d' % (r, ps[r][-1], f)) + ps[r].append(f) + for r, f in enumerate(w['final']): + if ps[r][-1] != f: + need(fs[ps[r][-1]] < fs[f], 'illegal final move: register %d' % r) + ps[r].append(f) + return ps + + +def copy_ranks(w, geo): + cur = list(w['start']) + for sec in 'DA': + for f, d, ss in w[sec]: + for r in (d, *ss): + cur[r] = f + return [geo.fdim[cur[q]] for q in w['ret']] + + +def paid_profile(w, geo): + prof = Counter(geo.fdim[b] - geo.fdim[a] for p in frame_paths(w, geo) for a, b in zip(p, p[1:])) + prof.update(copy_ranks(w, geo)) + return {k: prof[k] for k in sorted(prof)} + + +# ------------------------------------------------------------------ literal F2 stream + +def stream(w): + v, tmp = w['v'], 2 * w['v'] + w['R'] + out = [(0, d, s) for sec in 'DA' for _, d, ss in w[sec] for s in ss] + for j, centre in enumerate(w['ret']): + out.append((1, tmp, centre)) + out += [(0, v + i, tmp) for i, row in enumerate(w['scatter']) if j in row] + out.append((2, tmp, centre)) + out += [(0, d, s) for sec in 'BC' for _, d, ss in w[sec] for s in ss] + return out + + +def literal(w, reverse=False, clean_helpers=False): + """Set-valued (bitmask) replay of the literal ADD/COPY/ERASE stream on all formal columns.""" + v, n = w['v'], 2 * w['v'] + w['R'] + rows = [0 if clean_helpers and r >= 2 * v else 1 << r for r in range(n)] + [0] + ins = stream(w) + for kind, d, s in (reversed(ins) if reverse else ins): + if reverse and kind: + kind = 3 - kind + if kind == 0: + rows[d] ^= rows[s] + elif kind == 1: + need(not rows[d], 'COPY into a live temporary') + rows[d] = rows[s] + else: + need(rows[d] == rows[s], 'ERASE of a changed copy') + rows[d] = 0 + need(not rows[-1], 'temporary not erased') + return rows[:-1] + + +def wanted(w, clean_helpers=False): + v, n = w['v'], 2 * w['v'] + w['R'] + out = [] + for r in range(n): + if v <= r < 2 * v: + out.append((1 << r) | (1 << (r - v))) + else: + out.append(0 if clean_helpers and r >= 2 * v else 1 << r) + return out + + +def boundary_ok(w): + want = wanted(w) + try: + return all(literal(w, rev) == want for rev in (False, True)) + except ValueError: + return False + + +def bounds(w): + peaks = [] + ins = stream(w) + for reverse in (False, True): + val = [1] * (2 * w['v'] + w['R'] + 1) + peak = 1 + for kind, d, s in (reversed(ins) if reverse else ins): + if reverse and kind: + kind = 3 - kind + val[d] = val[d] + val[s] if kind == 0 else (val[s] if kind == 1 else 0) + peak = max(peak, val[d]) + peaks.append(peak) + F, B = peaks + local, nine = 64 * F**3 * B**2, (1 << 18) * F**5 * B**4 + return dict(ADDs=sum(k == 0 for k, _, _ in ins), D_ADDs=sum(len(g[2]) for g in w['D']), + A_ADDs=sum(len(g[2]) for g in w['A']), C_ADDs=sum(len(g[2]) for g in w['C']), + F=F, B=B, local_bits=local.bit_length(), nine_stage_bits=nine.bit_length(), + local_ok=local < 1 << LOCAL_CAP, nine_ok=nine < 1 << NINE_CAP) + + +def guards(b): + need(b['local_ok'] and b['nine_ok'], 'precision guard') + + +def run_values(w, secs, start=None): + v, n = w['v'], 2 * w['v'] + w['R'] + val = list(start) if start is not None else [1 << r for r in range(n)] + for sec in secs: + if sec == 'scatter': + cp = [val[q] for q in w['ret']] + for t, row in enumerate(w['scatter']): + for j in row: + val[v + t] ^= cp[j] + else: + for f, d, ss in w[sec]: + acc = 0 + for s in ss: + acc ^= val[s] + val[d] ^= acc + return val + + +def bits(x): + out = [] + while x: + low = x & -x + out.append(low.bit_length() - 1) + x ^= low + return out + + +def f2_rank(rows): + rows = [r for r in rows if r] + rk = 0 + while rows: + p = rows.pop() + if not p: + continue + rk += 1 + low = p & -p + rows = [r ^ p if r & low else r for r in rows] + rows = [r for r in rows if r] + return rk + + +# ------------------------------------------------------------------ helper-star structure and census + +def stars(w, geo): + v, H0, D = geo.v, 2 * geo.v, w['D'] + nh2 = sum(1 for g in D if g[1] >= H0) + need(nh2 % 2 == 0, 'helper gate count') + nh = nh2 // 2 + prep, rest, mid = D[:nh], D[len(D) - nh:], D[nh:len(D) - nh] + need(all(g[0] == geo.ZERO and g[1] >= H0 and len(g[2]) == 1 and g[2][0] >= H0 for g in prep), 'star preparation shape') + need(rest == prep[::-1], 'restorations are the reversed preparations') + need(all(g[0] == geo.ZERO and geo.is_y(g[1]) and all(s >= v for s in g[2]) for g in mid), 'target block shape') + centres = Counter(g[1] for g in prep) + leaves = [g[2][0] for g in prep] + need(len(set(leaves)) == nh and not set(leaves) & set(centres), 'leaves distinct and never centres') + need(all(any(c in g[2] for g in mid) for c in centres), 'every centre is read by the target block') + return nh, centres + + +def census(w, geo): + v, n, D, A = geo.v, geo.n, w['D'], w['A'] + nh, centres = stars(w, geo) + tail0 = len(D) - nh + val = [1 << i for i in range(n)] + icol = [1 << i for i in range(n)] # columns of the inverse state matrix + + def apply(d, ss): + for s in ss: + val[d] ^= val[s] + icol[s] ^= icol[d] + + def unique_set(delta): + S = [j for j in range(n) if (icol[j] & delta).bit_count() & 1] + acc = 0 + for j in S: + acc ^= val[j] + need(acc == delta, 'inverse state representation') + return S + + for g in D[:tail0]: + apply(g[1], g[2]) + edges, dtail = [], [] + by_centre = {} + for i in range(tail0, len(D)): + f, a, ss = D[i] + by_centre.setdefault(a, []).append((i, ss[0])) + for i in range(tail0, len(D)): + f, a, ss = D[i] + b = ss[0] + need(val[b] == 1 << b, 'leaf holds its own input at its restoration') + need(not any(a in D[j][2] for j in range(i + 1, len(D))), 'centre read later in the D tail') + for e, b2 in by_centre[a]: + if e != i: # D-tail alternative writer: absorb restoration e into this restoration i + S = unique_set(1 << b2) + new = sorted(set(ss) ^ set(S)) + dtail.append((e, i, new, 1 + 1 - len(new))) + edges.append((i, a, b, 1 << b)) + apply(a, ss) + read, moves = {}, [] + for k, (f, d, ss) in enumerate(A): + for i, a, b, delta in edges: + if i in read: + continue + if a in ss: + read[i] = 'A' + continue + if d == a: + S = unique_set(delta) + new = sorted(set(ss) ^ set(S)) + moves.append(dict(restoration=i, edge=[a, b], k=k, S=S, new=new, gain=1 + len(ss) - len(new), + a_in_S=a in S)) + apply(d, ss) + for i, a, b, _ in edges: + if i not in read: + need(a in w['ret'], 'centre never read before B') + read[i] = 'scatter' + return dict(nh=nh, centres=centres, edges=edges, read=read, moves=moves, dtail=dtail) + + +def edit(w, moves): + """Delete each move's restoration and give its A gate the move's new source set.""" + dels = {m['restoration'] for m in moves} + need(len(dels) == len(moves) and len({m['k'] for m in moves}) == len(moves), 'one move per edge and gate') + out = dict(w) + out['D'] = [g for i, g in enumerate(w['D']) if i not in dels] + A = [list(g) for g in w['A']] + for m in moves: + f, d, ss = A[m['k']] + need(d == m['edge'][0], 'move gate writes the centre') + A[m['k']] = [f, d, list(m['new'])] if m['new'] else None + out['A'] = [g for g in A if g is not None] + return out + + +def classify(w2, geo, base_paths): + try: + ps = frame_paths(w2, geo) + except ValueError: + return 'frame_illegal' + if ps != base_paths: + return 'paths_changed' + return 'frame_legal' + + +def census_report(name, w, geo, base_paths): + c = census(w, geo) + moves = c['moves'] + need(not any(m['a_in_S'] for m in moves), 'a centre in its own substitute set') + boundary_pass = 0 + legal_by_gain = {} + outcomes = Counter() + admitted = [] + first_illegal = None + for m in moves: + w2 = edit(w, [m]) + need(boundary_ok(w2), '%s move %s at A[%d] breaks the boundary' % (name, m['edge'], m['k'])) + boundary_pass += 1 + cls = classify(w2, geo, base_paths) + m['frame'] = cls + row = legal_by_gain.setdefault(m['gain'], Counter()) + row[cls] += 1 + if m['gain'] > 0: + if cls == 'frame_legal': + b = bounds(w2) + cls = 'admitted' if b['local_ok'] and b['nine_ok'] else 'guard_fail' + if cls == 'admitted': + admitted.append(m) + elif cls == 'frame_illegal' and first_illegal is None: + first_illegal = m + outcomes[cls] += 1 + # D-tail same-centre alternatives (the only other writers of a before its first read) never gain. + for e, i, new, gain in c['dtail']: + D = [list(g) for g in w['D']] + D[i] = [D[i][0], D[i][1], new] + need(gain == 0 and boundary_ok(dict(w, D=[g for j, g in enumerate(D) if j != e])), 'D-tail alternative') + return c, dict( + star_edges=len(c['edges']), centres=len(c['centres']), + first_centre_read=dict(sorted(Counter(c['read'].values()).items())), + A_writer_pairs=len(moves), edges_with_A_writer=len({m['restoration'] for m in moves}), + gain_histogram={str(g): n for g, n in sorted(Counter(m['gain'] for m in moves).items())}, + substitute_size_histogram={str(s): n for s, n in sorted(Counter(len(m['S']) for m in moves).items())}, + frame_by_gain={str(g): dict(sorted(r.items())) for g, r in sorted(legal_by_gain.items())}, + dirty_boundary_preserved=boundary_pass, + positive=sum(m['gain'] > 0 for m in moves), positive_outcomes=dict(sorted(outcomes.items())), + admitted=[[m['edge'][0], m['edge'][1], m['k'], m['new']] for m in sorted(admitted, key=lambda m: m['edge'])], + d_tail_same_centre_pairs=len(c['dtail']), d_tail_gains=sorted({x[3] for x in c['dtail']}), + d_tail_dirty_boundary_preserved=len(c['dtail'])), admitted, first_illegal + + +# ------------------------------------------------------------------ twisted contract identities + +def twisted(w, geo): + v, n, R, H0 = geo.v, geo.n, geo.R, 2 * geo.v + X, Y, H = geo.X, geo.Y, geo.H + z = [r for r in range(n) if not geo.is_y(r)] + out = {} + out['D_frame_zero'] = all(g[0] == geo.ZERO for g in w['D']) + out['D_source_free'] = all(g[1] >= v and all(s >= v for s in g[2]) for g in w['D']) + out['D_no_target_feeds_helper'] = not any(g[1] >= H0 and any(geo.is_y(s) for s in g[2]) for g in w['D']) + out['D_entry_frame_zero'] = all(w['start'][r] == geo.ZERO for r in range(v, n)) + Dm = run_values(w, ['D']) + out['D_sources_identity'] = all(Dm[s] == 1 << s for s in range(v)) + out['T_helper_only'] = all(Dm[h] & ~H == 0 for h in range(H0, n)) + out['T_invertible'] = f2_rank([Dm[h] for h in range(H0, n)]) == R + out['T_is_identity'] = all(Dm[h] == 1 << h for h in range(H0, n)) + out['T_offdiagonal'] = sorted([h, j] for h in range(H0, n) for j in bits(Dm[h] ^ (1 << h))) + out['D_targets_y_plus_Nh'] = all(Dm[v + t] & ~H == 1 << (v + t) for t in range(v)) + N = [Dm[v + t] & H for t in range(v)] + raw = run_values(w, ['A', 'scatter', 'B']) + out['U_block_form'] = all(raw[r] & Y == 0 for r in z) + out['V_identity'] = all(raw[v + t] & Y == 1 << (v + t) for t in range(v)) + out['J_identity'] = all(raw[v + t] & X == 1 << t for t in range(v)) + Kp = [raw[v + t] & H for t in range(v)] + KpT = [] + for t in range(v): + acc = 0 + for j in bits(Kp[t]): + acc ^= Dm[j] & H + KpT.append(acc) + out['N_equals_KprimeT'] = N == KpT + out['N_equals_Kprime'] = N == Kp + out['C_full_frame_z_only'] = all(g[0] == geo.FULL and not geo.is_y(g[1]) and not any(geo.is_y(s) for s in g[2]) + for g in w['C']) + after_C = run_values(w, ['C'], raw) + out['C_Uprime_identity'] = all(after_C[r] == 1 << r for r in z) + full = run_values(w, ['D', 'A', 'scatter', 'B', 'C']) + out['C_Uprime_T_identity'] = all(full[r] == 1 << r for r in z) + out['final_targets_y_plus_x'] = all(full[v + t] == (1 << (v + t)) | (1 << t) for t in range(v)) + out['N_targets_touched'] = sum(1 for t in range(v) if N[t]) + return out + + +TWISTED_REQUIRED = ['D_frame_zero', 'D_source_free', 'D_no_target_feeds_helper', 'D_entry_frame_zero', + 'D_sources_identity', 'T_helper_only', 'T_invertible', 'D_targets_y_plus_Nh', 'U_block_form', + 'V_identity', 'J_identity', 'N_equals_KprimeT', 'C_full_frame_z_only', 'C_Uprime_T_identity', + 'final_targets_y_plus_x'] + + +# ------------------------------------------------------------------ chronology + +def per_cut(w0, w1, geo, moves): + """Lockstep D/A replay of the base word w0 and absorbed word w1, with frames.""" + dels = {m['restoration']: m for m in moves} + edits = {m['k']: m for m in moves} + seq0 = [('D', i, g) for i, g in enumerate(w0['D'])] + [('A', k, g) for k, g in enumerate(w0['A'])] + n = geo.n + vals = [[1 << r for r in range(n)], [1 << r for r in range(n)]] + curs = [list(w0['start']), list(w0['start'])] + pending = {} + cuts = diff_cuts = 0 + frames_equal = True + maxpend = 0 + + def gate(side, f, d, ss): + for r in (d, *ss): + if curs[side][r] != f: + need(geo.fs[curs[side][r]] < geo.fs[f], 'per-cut frame climb') + curs[side][r] = f + acc = 0 + for s in ss: + acc ^= vals[side][s] + vals[side][d] ^= acc + + for sec, i, g in seq0: + gate(0, *g) + if sec == 'D' and i in dels: + m = dels[i] + pending[m['edge'][0]] = 1 << m['edge'][1] + elif sec == 'A' and i in edits: + m = edits[i] + gate(1, g[0], g[1], m['new']) + need(m['edge'][0] in pending, 'absorption before its restoration') + del pending[m['edge'][0]] + else: + gate(1, *g) + cuts += 1 + diff = {r: vals[0][r] ^ vals[1][r] for r in range(n) if vals[0][r] != vals[1][r]} + need(diff == pending, 'state difference at a cut is not exactly the pending leaf columns') + diff_cuts += bool(diff) + maxpend = max(maxpend, len(diff)) + frames_equal &= curs[0] == curs[1] + need(all(curs[1][c] == geo.ZERO for c in pending), 'a differing centre left the zero frame') + need(not pending and vals[0] == vals[1], 'states equal after the last absorption') + need(frames_equal, 'register frames identical at every cut') + first_touch = all(min(k for k, g in enumerate(w1['A']) if m['edge'][0] in (g[1], *g[2])) == m['k'] for m in moves) + need(first_touch, 'each absorbing gate is the first A gate touching its centre') + return dict(cuts=cuts, cuts_with_difference=diff_cuts, max_registers_differing=maxpend, + frames_identical_at_every_cut=frames_equal, differing_centres_stay_at_zero_frame=True, + absorbing_gate_is_first_A_touch=first_touch) + + +def first_climbs(w, geo): + """Helpers whose first climb out of the zero frame (in D/A) carries a value other than their own column.""" + n, H0 = geo.n, 2 * geo.v + val = [1 << r for r in range(n)] + cur = list(w['start']) + seen = {} + for sec in 'DA': + for f, d, ss in w[sec]: + for r in (d, *ss): + if cur[r] != f and r not in seen and cur[r] == geo.ZERO: + seen[r] = val[r] + cur[r] = f + acc = 0 + for s in ss: + acc ^= val[s] + val[d] ^= acc + hel = [r for r in seen if r >= H0] + return dict(helpers_climbing_from_zero=len(hel), non_own_value=sorted(r for r in hel if seen[r] != 1 << r), + targets_climbing_in_D_or_A=sum(1 for r in seen if geo.is_y(r))) + + +# ------------------------------------------------------------------ owner checker and exporter + +def owner_flags(own, w): + try: + _, _, _, hyp, con, _ = own.check(w) + except own.Reject as e: + raise ValueError('owner checker rejects: %s' % e) + flags = {**hyp, **con} + return flags + + +def exporter(code, w, work, name): + d = work / name + d.mkdir() + (d / 'export_records.py').write_bytes(code) + (d / 'word.json.gz').write_bytes(gzip.compress(canonical(w), mtime=0)) + env = {k: x for k, x in os.environ.items() if k != 'PYTHONOPTIMIZE'} + subprocess.run([sys.executable, '-I', '-B', str(d / 'export_records.py'), str(d / 'word.json.gz'), str(d / 'rec')], + check=True, capture_output=True, text=True, env=env) + raw = (d / 'rec/249-records.bin').read_bytes() + need(len(raw) % 24 == 0, 'record alignment') + rec = list(struct.iter_unpack('<6i', raw)) + peaks = [] + for reverse in (False, True): + norm, peak, open_ = [1] * (2 * w['v'] + w['R'] + 1), 1, False + for op, a, b, c, _, _ in (reversed(rec) if reverse else rec): + if op == 0: + continue + if reverse and op in (2, 3): + op = 5 - op + if op == 1: + norm[a] += abs(c) * norm[b] + peak = max(peak, norm[a]) + elif op == 2: + need(not open_, 'nested copy') + norm[b], open_ = norm[a], True + elif op == 3: + need(open_, 'erase without copy') + norm[b], open_ = 0, False + else: + raise ValueError('record opcode') + need(not open_, 'unclosed copy') + peaks.append(peak) + moves = {} + for r in rec: + if r[0] == 0: + moves.setdefault(r[1], []).append((r[2], r[3], r[4])) + prof = Counter(r[4] for r in rec if r[0] == 0) + prof.update(r[5] for r in rec if r[0] == 2) + return dict(records=len(rec), ADD=sum(r[0] == 1 for r in rec), COPY=sum(r[0] == 2 for r in rec), + ERASE=sum(r[0] == 3 for r in rec), MOVE=sum(r[0] == 0 for r in rec), + COPY_ranks=[r[5] for r in rec if r[0] == 2], F=peaks[0], B=peaks[1], + payload_bits=(64 * peaks[0]**3 * peaks[1]**2).bit_length(), + profile={k: prof[k] for k in sorted(prof)}, record_sha256=sha(raw)), moves + + +# ------------------------------------------------------------------ controls + +def rejected(label, fn, out): + try: + detail = fn() + except ValueError as e: + out.append([label, str(e)[:120]]) + return + raise ValueError('control accepted: %s (%s)' % (label, detail)) + + +def controls(name, base, absorbed, moves, geo, own, p589, first_illegal, data, pins): + out = [] + v = geo.v + # 1. omit the restorations without the A edit: dirty endpoint fails, clean-helper endpoint passes. + omit = dict(base, D=absorbed['D']) + rows = literal(omit) + bad = [r for r, (x, y) in enumerate(zip(rows, wanted(omit))) if x != y] + need(literal(omit, clean_helpers=True) == wanted(omit, True), 'omit-only control: clean helpers must pass') + kinds = Counter('source' if r < v else 'target' if r < 2 * v else 'helper' for r in bad) + + def omit_check(): + need(rows == wanted(omit), 'dirty endpoint wrong on %d registers %s; clean-helper endpoint passes' + % (len(bad), dict(sorted(kinds.items())))) + rejected('omit restorations without the A edit', omit_check, out) + # 2. the A edit with the literal cleanup of the edited A (inherited literal H4 enforced). + zg = [[geo.FULL, g[1], list(g[2])] for sec in 'AB' for g in absorbed[sec] if not geo.is_y(g[1])] + lit = dict(absorbed, C=zg[::-1]) + rows2 = literal(lit) + bad2 = [r for r, (x, y) in enumerate(zip(rows2, wanted(lit))) if x != y] + need(bad2 == [m['edge'][0] for m in moves] and all(rows2[m['edge'][0]] == (1 << m['edge'][0]) | (1 << m['edge'][1]) + for m in moves), 'literal-H4 control fails exactly on the centres') + need(literal(lit, clean_helpers=True) == wanted(lit, True), 'literal-H4 control passes on clean helpers') + + def lit_check(): + need(rows2 == wanted(lit), 'dirty helpers %s end as centre+leaf; clean helpers pass' % bad2) + rejected('A edit with the literal cleanup of the edited A', lit_check, out) + rejected('A edit with literal cleanup, owner checker', lambda: owner_flags(own, lit), out) + # 3. absorption after the first centre read. + late = None + for m in moves: + a = m['edge'][0] + first = next(k for k, g in enumerate(base['A']) if a in g[2]) + k = next((k for k, g in enumerate(base['A']) if k > first and g[1] == a), None) + if k is not None: + late = (m, k) + break + need(late is not None, 'a late writer exists') + m, k = late + # Same recipe at a writer after the first read: S represents the leaf column at that cut of the + # base word, but the pending difference has already leaked through the read. + ref = run_values(dict(base, A=base['A'][:k]), ['D', 'A']) + S = solve_set(ref, 1 << m['edge'][1], geo.n) + need(m['edge'][0] not in S, 'late control substitute avoids the centre') + late_word = edit(base, [dict(m, k=k, new=sorted(set(base['A'][k][2]) ^ set(S)))]) + rejected('absorption after the first centre read (A[%d] for centre %d)' % (k, m['edge'][0]), + lambda: need(boundary_ok(late_word), 'dirty boundary fails'), out) + # 4. wrong substitute register. + wrong = [dict(x) for x in moves] + wrong[0]['new'] = sorted(moves[1]['new']) + wrong_word = edit(base, wrong) + rejected('wrong substitute register (%s instead of %s at A[%d])' % (wrong[0]['new'], moves[0]['new'], moves[0]['k']), + lambda: need(boundary_ok(wrong_word), 'dirty boundary fails'), out) + # 5. one frame-illegal substitution (its F2 boundary is exact; frames reject it). + need(first_illegal is not None, 'a frame-illegal positive move exists') + ill = edit(base, [first_illegal]) + need(boundary_ok(ill), 'frame-illegal control has an exact F2 boundary') + rejected('frame-illegal substitution (centre %d, A[%d], new %s)' % (first_illegal['edge'][0], first_illegal['k'], + first_illegal['new']), + lambda: frame_paths(ill, geo), out) + # 6. PR1194/PR1311-style splice: absorbed A/B/C with PR589's target-only D. + rejected('splice absorbed A/B/C with PR589 D', lambda: owner_flags(own, dict(absorbed, D=p589['D'])), out) + # 7. corrupted source pin. + b = bytearray(data[WORDS[name]]) + b[len(b) // 2] ^= 1 + rejected('corrupted source pin', lambda: check_pin(WORDS[name], bytes(b), pins[WORDS[name]]), out) + return out + + +def solve_set(val, target, n): + """Unique register set whose current values sum to target (Gaussian elimination over F2).""" + piv = {} + for r in range(n): + x, tag = val[r], 1 << r + while x: + low = x & -x + if low not in piv: + piv[low] = (x, tag) + break + px, pt = piv[low] + x ^= px + tag ^= pt + need(x, 'state not invertible') + x, tag = target, 0 + while x: + low = x & -x + px, pt = piv[low] + x ^= px + tag ^= pt + return bits(tag) + + +# ------------------------------------------------------------------ instances + +def perturbations(base, moves, geo): + """Every one-register change of each admitted new source set breaks the dirty boundary.""" + tried = 0 + for idx, m in enumerate(moves): + for r in range(geo.n): + if r == m['edge'][0]: + continue + alt = [dict(x) for x in moves] + alt[idx]['new'] = sorted(set(m['new']) ^ {r}) + need(not boundary_ok(edit(base, alt)), 'perturbed source set accepted: move %d register %d' % (idx, r)) + tried += 1 + return tried + + +def instance(name, base, admitted, geo, own, p589, code, work, first_illegal, data, pins): + fname, adds0, adds1 = INSTANCES[name] + moves = sorted(admitted, key=lambda m: m['k']) + need([[m['edge'][0], m['edge'][1], m['k'], m['new']] for m in moves] == TRIPLES, name + ' admitted triples') + centres = {m['edge'][0] for m in moves} + need(not any(set(m['S']) & (centres - {m['edge'][0]}) for m in moves), 'joint substitutes avoid other centres') + w = edit(base, moves) + for k in base: + if k not in ('A', 'D'): + need(w[k] == base[k], '%s field %s changed' % (name, k)) + need(len(w['D']) == len(base['D']) - 3 and len(w['A']) == len(base['A']), name + ' edit shape') + for rev in (False, True): + need(literal(w, rev) == wanted(w), '%s boundary (%s)' % (name, 'reverse' if rev else 'forward')) + ps0, ps1 = frame_paths(base, geo), frame_paths(w, geo) + need(ps1 == ps0, name + ' ordered frame paths') + need(same_geometry(p589, base) and frame_paths(p589, geo) == ps0, name + ' frame paths equal PR589') + prof0, prof1 = paid_profile(base, geo), paid_profile(w, geo) + need(prof0 == prof1 == PROFILE and sum(k * x for k, x in prof1.items()) == 5129, name + ' paid profile') + b0, b1 = bounds(base), bounds(w) + need(b0['ADDs'] == adds0 and b1['ADDs'] == adds1, name + ' ADD count') + guards(b0) + guards(b1) + e0, mv0 = exporter(code, base, work, name + '-base') + e1, mv1 = exporter(code, w, work, name + '-absorbed') + for e, b in ((e0, b0), (e1, b1)): + need(e['ADD'] == b['ADDs'] and e['COPY'] == e['ERASE'] == 9 and e['F'] == b['F'] and e['B'] == b['B'], + name + ' exporter bill') + need(e['profile'] == PROFILE, name + ' exporter profile') + need(mv0 == mv1, name + ' ordered per-register MOVE records') + f0, f1 = owner_flags(own, base), owner_flags(own, w) + need([k for k, x in f0.items() if not x] == ['H2_D_frame0_targets_from_helpers', 'K_equals_D'], name + ' base owner') + need([k for k, x in f1.items() if not x] == OWNER_FALSE, name + ' absorbed owner flags') + bridge = owner_flags(own, dict(base, D=p589['D'])) + need(all(bridge.values()), name + ' PR1194-style original-D splice on the base word') + need(run_values(base, ['D']) == run_values(p589, ['D']), name + ' base D operator equals PR589 D') + t0, t1 = twisted(base, geo), twisted(w, geo) + for t in (t0, t1): + need(all(t[k] for k in TWISTED_REQUIRED), name + ' twisted contract') + need(t0['T_is_identity'] and t0['C_Uprime_identity'] and t0['N_equals_Kprime'], name + ' base is the T = I case') + need(not t1['T_is_identity'] and not t1['C_Uprime_identity'] and not t1['N_equals_Kprime'] + and t1['T_offdiagonal'] == sorted([m['edge'][0], m['edge'][1]] for m in moves), name + ' T != I exactly on the stars') + chron = per_cut(base, w, geo, moves) + fc0, fc1 = first_climbs(base, geo), first_climbs(w, geo) + need(fc0['non_own_value'] == [] and fc1['non_own_value'] == sorted(centres), name + ' first-climb census') + tried = perturbations(base, moves, geo) + ctl = controls(name, base, w, moves, geo, own, p589, first_illegal, data, pins) + return w, dict( + payload=fname, payload_sha256=sha(canonical(w)), moves=TRIPLES, + literal=dict(base=b0, absorbed=b1), exporter=dict(base=e0, absorbed=e1), + profile=prof1, rank_mass=sum(k * x for k, x in prof1.items()), + paths_registers=len(ps1), columns=geo.n, directions=2, + owner=dict(base_false=[k for k, x in f0.items() if not x], absorbed_false=[k for k, x in f1.items() if not x], + absorbed_true=sum(1 for x in f1.values() if x), original_D_splice_all_true=True), + twisted=dict(base=t0, absorbed=t1), chronology=chron, first_climbs=dict(base=fc0, absorbed=fc1), + perturbations_rejected=tried, controls=ctl) + + +# ------------------------------------------------------------------ driver + +def run(write=False): + data, pins = load_inputs() + words = {k: json.loads(gzip.decompress(data[p])) for k, p in WORDS.items()} + p589 = json.loads(gzip.decompress(data[PR589])) + own = owner_module(data[CHECKER]) + geo = Geo(p589) + for k, w in words.items(): + need(same_geometry(w, p589), k + ' geometry differs from PR589') + rep = dict(status='PASS_R439_TWISTED_STAR_ABSORPTION', inputs={p: pins[p] for p in INPUTS}, census={}, instances={}) + built = {} + with tempfile.TemporaryDirectory(prefix='r439-twisted-') as tmp: + work = Path(tmp) + for name, w in words.items(): + ps = frame_paths(w, geo) + _, summary, admitted, first_illegal = census_report(name, w, geo, ps) + need(summary['admitted'] == TRIPLES, name + ': exactly the three frame-legal positive moves') + need(set(summary['first_centre_read']) <= {'A', 'scatter'}, name + ': every centre is first read in A or the scatter') + rep['census'][name] = summary + if name in INSTANCES: + built[name], rep['instances'][name] = instance(name, w, admitted, geo, own, p589, data[EXPORTER], work, + first_illegal, data, pins) + rep['new_kappa_claim'] = False + rep = json.loads(json.dumps(rep)) + if write: + for name, w in built.items(): + (HERE / INSTANCES[name][0]).write_bytes(gzip.compress(canonical(w), mtime=0)) + (HERE / 'EXPECTED.json').write_text(json.dumps(rep, indent=1, sort_keys=True) + '\n', encoding='utf-8') + for name, w in built.items(): + committed = json.loads(gzip.decompress((HERE / INSTANCES[name][0]).read_bytes())) + need(canonical(committed) == canonical(w), 'committed payload differs from the rebuilt word: ' + name) + need(json.loads((HERE / 'EXPECTED.json').read_text(encoding='utf-8')) == rep, 'EXPECTED.json mismatch') + return rep + + +def main(): + ap = argparse.ArgumentParser(description=__doc__.split('\n')[0]) + ap.add_argument('--write', action='store_true', help='regenerate EXPECTED.json and the absorbed payloads') + a = ap.parse_args() + t0 = time.perf_counter() + rep = run(write=a.write) + for name, c in rep['census'].items(): + print('census %-6s star_edges=%d A_writer_pairs=%d gains=%s positive=%d outcomes=%s admitted=%d' % ( + name, c['star_edges'], c['A_writer_pairs'], json.dumps(c['gain_histogram'], separators=(',', ':')), + c['positive'], json.dumps(c['positive_outcomes'], separators=(',', ':')), len(c['admitted']))) + for name, x in rep['instances'].items(): + b0, b1 = x['literal']['base'], x['literal']['absorbed'] + print('instance %-6s ADDs %d -> %d F/B %d/%d -> %d/%d bits %d/%d -> %d/%d profile %s mass %d owner_false=%s ' + 'controls=%d perturbations=%d' % ( + name, b0['ADDs'], b1['ADDs'], b0['F'], b0['B'], b1['F'], b1['B'], b0['local_bits'], + b0['nine_stage_bits'], b1['local_bits'], b1['nine_stage_bits'], + json.dumps(x['profile'], separators=(',', ':')), x['rank_mass'], ','.join(x['owner']['absorbed_false']), + len(x['controls']), x['perturbations_rejected'])) + for label, why in x['controls']: + print(' control rejected: %s -- %s' % (label, why)) + print('PASS_R439_TWISTED_STAR_ABSORPTION words=%d instances=%d ADDs 11500->11497 10492->10489 columns=661 ' + 'controls=%d no_new_kappa (%.1f s)' % (len(rep['census']), len(rep['instances']), + sum(len(x['controls']) for x in rep['instances'].values()), + time.perf_counter() - t0)) + + +if __name__ == '__main__': + main()