diff --git a/research/observable-connector-repair/CERTIFICATE.json b/research/observable-connector-repair/CERTIFICATE.json new file mode 100644 index 0000000000..811a8253ba --- /dev/null +++ b/research/observable-connector-repair/CERTIFICATE.json @@ -0,0 +1,4562 @@ +{ + "array_evidence": { + "block_lengths": [ + 1, + 2, + 3 + ], + "literal_cases": 904, + "observation_checks": 5696, + "pilot_basis_columns_forward_and_inverse": 648, + "tiny_all_dirty_inputs": 256 + }, + "controls": [ + "omit_output_correction", + "omit_terminal_connector_correction", + "omit_final_B_entry", + "omit_reader_prewrite", + "omit_source_restoration_entry", + "wrong_observable_coset", + "corrupt_lower_bound_potential", + "negative_gate_price", + "out_of_range_reader", + "infeasible_zero_reader", + "unrestored_source_tour", + "early_future_output_is_not_canonical", + "strong_coherence_is_not_asserted", + "direct_product_fusion_is_cheaper" + ], + "demands": [ + { + "coherent_mask": 3, + "demand": 1, + "reader": 9, + "source_mask": 8 + }, + { + "coherent_mask": 5, + "demand": 1, + "reader": 6, + "source_mask": 12 + }, + { + "coherent_mask": 9, + "demand": 0, + "reader": 4, + "source_mask": 14 + }, + { + "coherent_mask": 11, + "demand": 1, + "reader": 11, + "source_mask": 15 + }, + { + "coherent_mask": 8, + "demand": 1, + "reader": 15, + "source_mask": 7 + }, + { + "coherent_mask": 14, + "demand": 1, + "reader": 2, + "source_mask": 3 + }, + { + "coherent_mask": 2, + "demand": 1, + "reader": 3, + "source_mask": 1 + }, + { + "coherent_mask": 0, + "demand": 0, + "reader": 14, + "source_mask": 0 + } + ], + "invoices": { + "coherent": { + "by_kind": { + "B": 14, + "connector_repair": 14, + "reader": 36, + "source": 8 + }, + "data_cells_per_L": 18, + "data_reads_per_L": 144, + "data_writes_per_L": 72, + "dispatches_per_L": 72, + "head_steps_L1": 1484, + "head_steps_polynomial": { + "L": 72, + "L2": 1412 + }, + "instruction_records_per_L": 72, + "online_tariff_polynomial": { + "L": 432, + "L2": 1412 + }, + "scalar_xors": 72, + "word_sha256": "aed50490ed0b98df6963e58f514581397047c093037d5363e57b3d1f5b94217c", + "xor_instructions_per_L": 72 + }, + "direct": { + "by_kind": { + "direct_product": 18, + "source": 8 + }, + "data_cells_per_L": 18, + "data_reads_per_L": 52, + "data_writes_per_L": 26, + "dispatches_per_L": 26, + "head_steps_L1": 562, + "head_steps_polynomial": { + "L": 26, + "L2": 536 + }, + "instruction_records_per_L": 26, + "online_tariff_polynomial": { + "L": 156, + "L2": 536 + }, + "scalar_xors": 26, + "word_sha256": "0dfc9a01f6829e2caa8ae428b2fa7f72f5e1f2b52f2728db87752045915047f8", + "xor_instructions_per_L": 26 + }, + "eager": { + "by_kind": { + "B": 112, + "reader": 36, + "source": 8 + }, + "data_cells_per_L": 18, + "data_reads_per_L": 312, + "data_writes_per_L": 156, + "dispatches_per_L": 156, + "head_steps_L1": 2732, + "head_steps_polynomial": { + "L": 156, + "L2": 2576 + }, + "instruction_records_per_L": 156, + "online_tariff_polynomial": { + "L": 936, + "L2": 2576 + }, + "scalar_xors": 156, + "word_sha256": "1eda62080eba7d6e39d848a894931b26358d1111276dc88c5ec45b61c7e60d1c", + "xor_instructions_per_L": 156 + }, + "mixed": { + "by_kind": { + "B": 14, + "connector_repair": 2, + "output_repair": 1, + "reader": 36, + "source": 8 + }, + "data_cells_per_L": 18, + "data_reads_per_L": 122, + "data_writes_per_L": 61, + "dispatches_per_L": 61, + "head_steps_L1": 1324, + "head_steps_polynomial": { + "L": 61, + "L2": 1263 + }, + "instruction_records_per_L": 61, + "online_tariff_polynomial": { + "L": 366, + "L2": 1263 + }, + "scalar_xors": 61, + "word_sha256": "fb0bab8dc9a3749f498dd389b5a503b327b571b277b7405ba0a9ed626130de14", + "xor_instructions_per_L": 61 + }, + "output_only": { + "by_kind": { + "B": 14, + "output_repair": 6, + "reader": 36, + "source": 8 + }, + "data_cells_per_L": 18, + "data_reads_per_L": 128, + "data_writes_per_L": 64, + "dispatches_per_L": 64, + "head_steps_L1": 1434, + "head_steps_polynomial": { + "L": 64, + "L2": 1370 + }, + "instruction_records_per_L": 64, + "online_tariff_polynomial": { + "L": 384, + "L2": 1370 + }, + "scalar_xors": 64, + "word_sha256": "f978685335479e5b47e73d1b657b880c4512fc0410d2ca4d5db20a8595df867a", + "xor_instructions_per_L": 64 + }, + "strict": { + "by_kind": { + "B": 14, + "connector_repair": 4, + "reader": 36, + "source": 8 + }, + "data_cells_per_L": 18, + "data_reads_per_L": 124, + "data_writes_per_L": 62, + "dispatches_per_L": 62, + "head_steps_L1": 1328, + "head_steps_polynomial": { + "L": 62, + "L2": 1266 + }, + "instruction_records_per_L": 62, + "online_tariff_polynomial": { + "L": 372, + "L2": 1266 + }, + "scalar_xors": 62, + "word_sha256": "2bba32315df4ae4e5c79cd4220de3b3aa7baed2934ca2dc12ea55c722bd201f2", + "xor_instructions_per_L": 62 + } + }, + "optimality": { + "mixed": { + "checked_edges": 704, + "minimum": 3, + "potential": [ + [ + 0, + 1, + 1, + 2, + 1, + 2, + 2, + 3, + 1, + 2, + 2, + 3, + 2, + 3, + 3, + 4 + ], + [ + 1, + 1, + 2, + 2, + 2, + 2, + 3, + 3, + 1, + 2, + 2, + 3, + 2, + 3, + 3, + 4 + ], + [ + 2, + 2, + 2, + 2, + 2, + 2, + 3, + 3, + 2, + 3, + 2, + 3, + 2, + 3, + 3, + 4 + ], + [ + 2, + 2, + 2, + 2, + 3, + 3, + 3, + 3, + 2, + 3, + 2, + 3, + 3, + 4, + 3, + 4 + ], + [ + 3, + 2, + 2, + 3, + 4, + 3, + 3, + 4, + 2, + 3, + 3, + 3, + 3, + 4, + 4, + 4 + ], + [ + 3, + 2, + 2, + 3, + 4, + 3, + 3, + 4, + 2, + 3, + 3, + 3, + 3, + 4, + 4, + 4 + ], + [ + 3, + 3, + 2, + 3, + 4, + 4, + 3, + 4, + 3, + 4, + 3, + 3, + 4, + 5, + 4, + 4 + ], + [ + 3, + 3, + 2, + 3, + 4, + 4, + 3, + 4, + 4, + 4, + 3, + 4, + 5, + 5, + 4, + 5 + ], + [ + 3, + 3, + 3, + 4, + 4, + 4, + 3, + 4, + 4, + 4, + 3, + 4, + 5, + 5, + 4, + 5 + ] + ] + }, + "mixed_quadratic": { + "checked_edges": 704, + "minimum": 45, + "potential": [ + [ + 0, + 11, + 13, + 24, + 15, + 26, + 28, + 39, + 17, + 28, + 30, + 41, + 32, + 43, + 45, + 56 + ], + [ + 19, + 11, + 32, + 24, + 34, + 26, + 47, + 39, + 17, + 28, + 30, + 41, + 32, + 43, + 45, + 56 + ], + [ + 40, + 32, + 32, + 24, + 34, + 26, + 47, + 39, + 38, + 49, + 30, + 41, + 32, + 43, + 45, + 56 + ], + [ + 40, + 32, + 32, + 24, + 55, + 47, + 47, + 39, + 38, + 49, + 30, + 41, + 53, + 64, + 45, + 56 + ], + [ + 43, + 32, + 32, + 43, + 58, + 47, + 47, + 58, + 38, + 49, + 49, + 41, + 53, + 64, + 64, + 56 + ], + [ + 43, + 32, + 32, + 43, + 58, + 47, + 47, + 58, + 38, + 49, + 49, + 41, + 53, + 64, + 64, + 56 + ], + [ + 45, + 56, + 32, + 43, + 60, + 71, + 47, + 58, + 62, + 54, + 49, + 41, + 77, + 69, + 64, + 56 + ], + [ + 45, + 56, + 32, + 43, + 60, + 71, + 47, + 58, + 62, + 54, + 49, + 60, + 77, + 69, + 64, + 75 + ], + [ + 45, + 56, + 58, + 69, + 60, + 71, + 47, + 58, + 62, + 73, + 49, + 60, + 77, + 69, + 64, + 75 + ] + ] + }, + "mixed_tariff_L1": { + "checked_edges": 704, + "minimum": 63, + "potential": [ + [ + 0, + 17, + 19, + 36, + 21, + 38, + 40, + 57, + 23, + 40, + 42, + 59, + 44, + 61, + 63, + 80 + ], + [ + 25, + 17, + 44, + 36, + 46, + 38, + 65, + 57, + 23, + 40, + 42, + 59, + 44, + 61, + 63, + 80 + ], + [ + 52, + 44, + 44, + 36, + 46, + 38, + 65, + 57, + 50, + 67, + 42, + 59, + 44, + 61, + 63, + 80 + ], + [ + 52, + 44, + 44, + 36, + 73, + 65, + 65, + 57, + 50, + 67, + 42, + 59, + 71, + 88, + 63, + 80 + ], + [ + 61, + 44, + 44, + 61, + 82, + 65, + 65, + 82, + 50, + 67, + 67, + 59, + 71, + 88, + 88, + 80 + ], + [ + 61, + 44, + 44, + 61, + 82, + 65, + 65, + 82, + 50, + 67, + 67, + 59, + 71, + 88, + 88, + 80 + ], + [ + 63, + 79, + 44, + 61, + 84, + 100, + 65, + 82, + 85, + 78, + 67, + 59, + 106, + 99, + 88, + 80 + ], + [ + 63, + 79, + 44, + 61, + 84, + 100, + 65, + 82, + 86, + 78, + 67, + 84, + 107, + 99, + 88, + 105 + ], + [ + 63, + 79, + 82, + 98, + 84, + 100, + 65, + 82, + 86, + 102, + 67, + 84, + 107, + 99, + 88, + 105 + ] + ] + }, + "strict": { + "checked_edges": 640, + "minimum": 4, + "potential": [ + [ + 0, + 1, + 1, + 2, + 1, + 2, + 2, + 3, + 1, + 2, + 2, + 3, + 2, + 3, + 3, + 4 + ], + [ + 2, + 1, + 3, + 2, + 3, + 2, + 4, + 3, + 1, + 2, + 2, + 3, + 2, + 3, + 3, + 4 + ], + [ + 4, + 3, + 3, + 2, + 3, + 2, + 4, + 3, + 3, + 4, + 2, + 3, + 2, + 3, + 3, + 4 + ], + [ + 4, + 3, + 3, + 2, + 5, + 4, + 4, + 3, + 3, + 4, + 2, + 3, + 4, + 5, + 3, + 4 + ], + [ + 4, + 3, + 3, + 4, + 5, + 4, + 4, + 5, + 3, + 4, + 4, + 3, + 4, + 5, + 5, + 4 + ], + [ + 4, + 3, + 3, + 4, + 5, + 4, + 4, + 5, + 3, + 4, + 4, + 3, + 4, + 5, + 5, + 4 + ], + [ + 4, + 5, + 3, + 4, + 5, + 6, + 4, + 5, + 5, + 4, + 4, + 3, + 6, + 5, + 5, + 4 + ], + [ + 4, + 5, + 3, + 4, + 5, + 6, + 4, + 5, + 5, + 4, + 4, + 5, + 6, + 5, + 5, + 6 + ], + [ + 4, + 5, + 5, + 6, + 5, + 6, + 4, + 5, + 5, + 6, + 4, + 5, + 6, + 5, + 5, + 6 + ] + ] + }, + "strict_quadratic": { + "checked_edges": 640, + "minimum": 48, + "potential": [ + [ + 0, + 11, + 13, + 24, + 15, + 26, + 28, + 39, + 17, + 28, + 30, + 41, + 32, + 43, + 45, + 56 + ], + [ + 22, + 11, + 35, + 24, + 37, + 26, + 50, + 39, + 17, + 28, + 30, + 41, + 32, + 43, + 45, + 56 + ], + [ + 48, + 37, + 35, + 24, + 37, + 26, + 50, + 39, + 43, + 54, + 30, + 41, + 32, + 43, + 45, + 56 + ], + [ + 48, + 37, + 35, + 24, + 63, + 52, + 50, + 39, + 43, + 54, + 30, + 41, + 58, + 69, + 45, + 56 + ], + [ + 48, + 37, + 35, + 46, + 63, + 52, + 50, + 61, + 43, + 54, + 52, + 41, + 58, + 69, + 67, + 56 + ], + [ + 48, + 37, + 35, + 46, + 63, + 52, + 50, + 61, + 43, + 54, + 52, + 41, + 58, + 69, + 67, + 56 + ], + [ + 48, + 59, + 35, + 46, + 63, + 74, + 50, + 61, + 65, + 54, + 52, + 41, + 80, + 69, + 67, + 56 + ], + [ + 48, + 59, + 35, + 46, + 63, + 74, + 50, + 61, + 65, + 54, + 52, + 63, + 80, + 69, + 67, + 78 + ], + [ + 48, + 59, + 61, + 72, + 63, + 74, + 50, + 61, + 65, + 76, + 52, + 63, + 80, + 69, + 67, + 78 + ] + ] + } + }, + "plans": { + "mixed": { + "cost": 3, + "output_corrections": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "output_prices": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "path": [ + 0, + 2, + 2, + 2, + 2, + 2, + 2, + 0, + 0 + ], + "tables": [ + [ + 0, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null + ], + [ + 1, + 1, + 2, + 2, + 2, + 2, + 3, + 3, + 1, + 3, + 2, + 4, + 2, + 4, + 3, + 5 + ], + [ + 2, + 2, + 2, + 2, + 2, + 2, + 4, + 4, + 2, + 3, + 2, + 3, + 2, + 3, + 4, + 5 + ], + [ + 2, + 2, + 2, + 2, + 3, + 3, + 4, + 4, + 2, + 3, + 2, + 3, + 3, + 4, + 4, + 5 + ], + [ + 3, + 2, + 2, + 3, + 4, + 3, + 3, + 4, + 2, + 4, + 3, + 3, + 3, + 5, + 4, + 4 + ], + [ + 4, + 2, + 2, + 4, + 4, + 4, + 4, + 4, + 2, + 4, + 4, + 3, + 4, + 4, + 4, + 5 + ], + [ + 4, + 3, + 2, + 3, + 5, + 4, + 3, + 4, + 3, + 4, + 3, + 3, + 4, + 5, + 4, + 4 + ], + [ + 4, + 3, + 2, + 4, + 5, + 4, + 3, + 5, + 4, + 4, + 3, + 4, + 5, + 5, + 4, + 5 + ], + [ + 3, + 3, + 3, + 4, + 5, + 5, + 3, + 4, + 5, + 5, + 3, + 4, + 5, + 5, + 5, + 6 + ] + ], + "weights": [ + 1, + 1, + 1, + 1 + ] + }, + "mixed_quadratic": { + "cost": 45, + "output_corrections": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "output_prices": [ + 19, + 21, + 23, + 25, + 27, + 29, + 31, + 33 + ], + "path": [ + 0, + 2, + 2, + 2, + 2, + 2, + 2, + 0, + 0 + ], + "tables": [ + [ + 0, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null + ], + [ + 19, + 11, + 32, + 24, + 34, + 26, + 47, + 39, + 17, + 47, + 30, + 60, + 32, + 62, + 45, + 75 + ], + [ + 40, + 32, + 32, + 24, + 34, + 26, + 68, + 60, + 38, + 49, + 30, + 41, + 32, + 43, + 66, + 77 + ], + [ + 40, + 32, + 32, + 24, + 57, + 49, + 70, + 62, + 38, + 49, + 30, + 41, + 55, + 66, + 68, + 79 + ], + [ + 65, + 32, + 32, + 49, + 80, + 47, + 47, + 64, + 38, + 74, + 55, + 41, + 53, + 89, + 70, + 56 + ], + [ + 70, + 32, + 32, + 70, + 58, + 74, + 74, + 58, + 38, + 76, + 76, + 41, + 80, + 64, + 64, + 83 + ], + [ + 72, + 61, + 32, + 43, + 87, + 76, + 47, + 58, + 67, + 78, + 49, + 41, + 82, + 93, + 64, + 56 + ], + [ + 76, + 56, + 32, + 74, + 91, + 71, + 47, + 89, + 93, + 54, + 49, + 72, + 108, + 69, + 64, + 87 + ], + [ + 45, + 56, + 65, + 76, + 93, + 104, + 47, + 58, + 95, + 87, + 49, + 60, + 77, + 69, + 97, + 108 + ] + ], + "weights": [ + 11, + 13, + 15, + 17 + ] + }, + "mixed_tariff_L1": { + "cost": 63, + "output_corrections": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "output_prices": [ + 25, + 27, + 29, + 31, + 33, + 35, + 37, + 39 + ], + "path": [ + 0, + 2, + 2, + 2, + 2, + 2, + 2, + 0, + 0 + ], + "tables": [ + [ + 0, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null + ], + [ + 25, + 17, + 44, + 36, + 46, + 38, + 65, + 57, + 23, + 65, + 42, + 84, + 44, + 86, + 63, + 105 + ], + [ + 52, + 44, + 44, + 36, + 46, + 38, + 92, + 84, + 50, + 67, + 42, + 59, + 44, + 61, + 90, + 107 + ], + [ + 52, + 44, + 44, + 36, + 75, + 67, + 94, + 86, + 50, + 67, + 42, + 59, + 73, + 90, + 92, + 109 + ], + [ + 83, + 44, + 44, + 67, + 104, + 65, + 65, + 88, + 50, + 98, + 73, + 59, + 71, + 119, + 94, + 80 + ], + [ + 94, + 44, + 44, + 94, + 82, + 98, + 98, + 82, + 50, + 100, + 100, + 59, + 104, + 88, + 88, + 113 + ], + [ + 96, + 79, + 44, + 61, + 117, + 100, + 65, + 82, + 85, + 102, + 67, + 59, + 106, + 123, + 88, + 80 + ], + [ + 100, + 79, + 44, + 98, + 121, + 100, + 65, + 119, + 122, + 78, + 67, + 96, + 143, + 99, + 88, + 117 + ], + [ + 63, + 79, + 83, + 100, + 123, + 139, + 65, + 82, + 125, + 117, + 67, + 84, + 107, + 99, + 127, + 144 + ] + ], + "weights": [ + 17, + 19, + 21, + 23 + ] + }, + "strict": { + "cost": 4, + "output_corrections": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "output_prices": null, + "path": [ + 1, + 2, + 2, + 2, + 2, + 2, + 2, + 0, + 0 + ], + "tables": [ + [ + 0, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null + ], + [ + null, + 1, + null, + 2, + null, + 2, + null, + 3, + 1, + null, + 2, + null, + 2, + null, + 3, + null + ], + [ + null, + null, + 3, + 2, + 3, + 2, + null, + null, + null, + null, + 2, + 3, + 2, + 3, + null, + null + ], + [ + 4, + 3, + 3, + 2, + null, + null, + null, + null, + 3, + 4, + 2, + 3, + null, + null, + null, + null + ], + [ + null, + 3, + 3, + null, + null, + 4, + 4, + null, + 3, + null, + null, + 3, + 4, + null, + null, + 4 + ], + [ + null, + 3, + 3, + null, + 5, + null, + null, + 5, + 3, + null, + null, + 3, + null, + 5, + 5, + null + ], + [ + null, + null, + 3, + 4, + null, + null, + 4, + 5, + null, + null, + 4, + 3, + null, + null, + 5, + 4 + ], + [ + null, + 5, + 3, + null, + null, + 6, + 4, + null, + null, + 4, + 4, + null, + null, + 5, + 5, + null + ], + [ + 4, + 5, + null, + null, + null, + null, + 4, + 5, + null, + null, + 4, + 5, + 6, + 5, + null, + null + ] + ], + "weights": [ + 1, + 1, + 1, + 1 + ] + }, + "strict_quadratic": { + "cost": 48, + "output_corrections": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "output_prices": null, + "path": [ + 1, + 2, + 2, + 2, + 2, + 2, + 2, + 0, + 0 + ], + "tables": [ + [ + 0, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null + ], + [ + null, + 11, + null, + 24, + null, + 26, + null, + 39, + 17, + null, + 30, + null, + 32, + null, + 45, + null + ], + [ + null, + null, + 35, + 24, + 37, + 26, + null, + null, + null, + null, + 30, + 41, + 32, + 43, + null, + null + ], + [ + 48, + 37, + 35, + 24, + null, + null, + null, + null, + 43, + 54, + 30, + 41, + null, + null, + null, + null + ], + [ + null, + 37, + 35, + null, + null, + 52, + 50, + null, + 43, + null, + null, + 41, + 58, + null, + null, + 56 + ], + [ + null, + 37, + 35, + null, + 63, + null, + null, + 61, + 43, + null, + null, + 41, + null, + 69, + 67, + null + ], + [ + null, + null, + 35, + 46, + null, + null, + 50, + 61, + null, + null, + 52, + 41, + null, + null, + 67, + 56 + ], + [ + null, + 59, + 35, + null, + null, + 74, + 50, + null, + null, + 54, + 52, + null, + null, + 69, + 67, + null + ], + [ + 48, + 59, + null, + null, + null, + null, + 50, + 61, + null, + null, + 52, + 63, + 80, + 69, + null, + null + ] + ], + "weights": [ + 11, + 13, + 15, + 17 + ] + } + }, + "schema_version": 1, + "small_exhaustion": { + "demand_sequences": 1555, + "maximum_stages": 4, + "result_sha256": "97e707ef63736e3c3174559e12aa9fc030ed450f032bc77f2e966dae38f74cf2", + "tariff_mode_cases": 6220, + "width": 2 + }, + "source_pins": { + "base": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "predecessor_notes": 3 + }, + "spec": { + "B": [ + 8, + 13, + 6, + 2 + ], + "matrix_draws": 3, + "readers": [ + 9, + 6, + 4, + 11, + 15, + 2, + 3, + 14 + ], + "seed": 50, + "steps": [ + 3, + 2, + 1, + 0, + 3, + 2, + 1, + 0 + ], + "width": 4 + }, + "status": "SCOPED_EXACT_INTERFACE_NO_NEW_KAPPA", + "symbolic_semantics": { + "coherent": { + "basis_columns": 18, + "final_rows": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256, + 538, + 1051, + 2054, + 4119, + 8209, + 16413, + 32789, + 65545, + 131072 + ], + "observation_cuts": 8 + }, + "direct": { + "basis_columns": 18, + "final_rows": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256, + 538, + 1051, + 2054, + 4119, + 8209, + 16413, + 32789, + 65545, + 131072 + ], + "observation_cuts": 8 + }, + "eager": { + "basis_columns": 18, + "final_rows": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256, + 538, + 1051, + 2054, + 4119, + 8209, + 16413, + 32789, + 65545, + 131072 + ], + "observation_cuts": 8 + }, + "mixed": { + "basis_columns": 18, + "final_rows": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256, + 538, + 1051, + 2054, + 4119, + 8209, + 16413, + 32789, + 65545, + 131072 + ], + "observation_cuts": 8 + }, + "output_only": { + "basis_columns": 18, + "final_rows": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256, + 538, + 1051, + 2054, + 4119, + 8209, + 16413, + 32789, + 65545, + 131072 + ], + "observation_cuts": 8 + }, + "strict": { + "basis_columns": 18, + "final_rows": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256, + 538, + 1051, + 2054, + 4119, + 8209, + 16413, + 32789, + 65545, + 131072 + ], + "observation_cuts": 8 + } + }, + "words": { + "coherent": { + "cuts": [ + 30, + 35, + 39, + 44, + 51, + 55, + 60, + 65 + ], + "gates": [ + [ + 9, + 5, + "reader" + ], + [ + 9, + 8, + "reader" + ], + [ + 10, + 6, + "reader" + ], + [ + 10, + 7, + "reader" + ], + [ + 11, + 7, + "reader" + ], + [ + 12, + 5, + "reader" + ], + [ + 12, + 6, + "reader" + ], + [ + 12, + 8, + "reader" + ], + [ + 13, + 5, + "reader" + ], + [ + 13, + 6, + "reader" + ], + [ + 13, + 7, + "reader" + ], + [ + 13, + 8, + "reader" + ], + [ + 14, + 6, + "reader" + ], + [ + 15, + 5, + "reader" + ], + [ + 15, + 6, + "reader" + ], + [ + 16, + 6, + "reader" + ], + [ + 16, + 7, + "reader" + ], + [ + 16, + 8, + "reader" + ], + [ + 5, + 3, + "B" + ], + [ + 6, + 0, + "B" + ], + [ + 6, + 2, + "B" + ], + [ + 6, + 3, + "B" + ], + [ + 7, + 1, + "B" + ], + [ + 7, + 2, + "B" + ], + [ + 8, + 1, + "B" + ], + [ + 3, + 4, + "source" + ], + [ + 5, + 4, + "connector_repair" + ], + [ + 6, + 4, + "connector_repair" + ], + [ + 9, + 5, + "reader" + ], + [ + 9, + 8, + "reader" + ], + [ + 2, + 4, + "source" + ], + [ + 6, + 4, + "connector_repair" + ], + [ + 7, + 4, + "connector_repair" + ], + [ + 10, + 6, + "reader" + ], + [ + 10, + 7, + "reader" + ], + [ + 1, + 4, + "source" + ], + [ + 7, + 4, + "connector_repair" + ], + [ + 8, + 4, + "connector_repair" + ], + [ + 11, + 7, + "reader" + ], + [ + 0, + 4, + "source" + ], + [ + 6, + 4, + "connector_repair" + ], + [ + 12, + 5, + "reader" + ], + [ + 12, + 6, + "reader" + ], + [ + 12, + 8, + "reader" + ], + [ + 3, + 4, + "source" + ], + [ + 5, + 4, + "connector_repair" + ], + [ + 6, + 4, + "connector_repair" + ], + [ + 13, + 5, + "reader" + ], + [ + 13, + 6, + "reader" + ], + [ + 13, + 7, + "reader" + ], + [ + 13, + 8, + "reader" + ], + [ + 2, + 4, + "source" + ], + [ + 6, + 4, + "connector_repair" + ], + [ + 7, + 4, + "connector_repair" + ], + [ + 14, + 6, + "reader" + ], + [ + 1, + 4, + "source" + ], + [ + 7, + 4, + "connector_repair" + ], + [ + 8, + 4, + "connector_repair" + ], + [ + 15, + 5, + "reader" + ], + [ + 15, + 6, + "reader" + ], + [ + 0, + 4, + "source" + ], + [ + 6, + 4, + "connector_repair" + ], + [ + 16, + 6, + "reader" + ], + [ + 16, + 7, + "reader" + ], + [ + 16, + 8, + "reader" + ], + [ + 5, + 3, + "B" + ], + [ + 6, + 0, + "B" + ], + [ + 6, + 2, + "B" + ], + [ + 6, + 3, + "B" + ], + [ + 7, + 1, + "B" + ], + [ + 7, + 2, + "B" + ], + [ + 8, + 1, + "B" + ] + ], + "registers": 18 + }, + "direct": { + "cuts": [ + 3, + 7, + 10, + 14, + 16, + 20, + 23, + 26 + ], + "gates": [ + [ + 3, + 4, + "source" + ], + [ + 9, + 1, + "direct_product" + ], + [ + 9, + 3, + "direct_product" + ], + [ + 2, + 4, + "source" + ], + [ + 10, + 0, + "direct_product" + ], + [ + 10, + 1, + "direct_product" + ], + [ + 10, + 3, + "direct_product" + ], + [ + 1, + 4, + "source" + ], + [ + 11, + 1, + "direct_product" + ], + [ + 11, + 2, + "direct_product" + ], + [ + 0, + 4, + "source" + ], + [ + 12, + 0, + "direct_product" + ], + [ + 12, + 1, + "direct_product" + ], + [ + 12, + 2, + "direct_product" + ], + [ + 3, + 4, + "source" + ], + [ + 13, + 0, + "direct_product" + ], + [ + 2, + 4, + "source" + ], + [ + 14, + 0, + "direct_product" + ], + [ + 14, + 2, + "direct_product" + ], + [ + 14, + 3, + "direct_product" + ], + [ + 1, + 4, + "source" + ], + [ + 15, + 0, + "direct_product" + ], + [ + 15, + 2, + "direct_product" + ], + [ + 0, + 4, + "source" + ], + [ + 16, + 0, + "direct_product" + ], + [ + 16, + 3, + "direct_product" + ] + ], + "registers": 18 + }, + "eager": { + "cuts": [ + 19, + 38, + 55, + 76, + 99, + 116, + 135, + 156 + ], + "gates": [ + [ + 3, + 4, + "source" + ], + [ + 9, + 5, + "reader" + ], + [ + 9, + 8, + "reader" + ], + [ + 5, + 3, + "B" + ], + [ + 6, + 0, + "B" + ], + [ + 6, + 2, + "B" + ], + [ + 6, + 3, + "B" + ], + [ + 7, + 1, + "B" + ], + [ + 7, + 2, + "B" + ], + [ + 8, + 1, + "B" + ], + [ + 9, + 5, + "reader" + ], + [ + 9, + 8, + "reader" + ], + [ + 5, + 3, + "B" + ], + [ + 6, + 0, + "B" + ], + [ + 6, + 2, + "B" + ], + [ + 6, + 3, + "B" + ], + [ + 7, + 1, + "B" + ], + [ + 7, + 2, + "B" + ], + [ + 8, + 1, + "B" + ], + [ + 2, + 4, + "source" + ], + [ + 10, + 6, + "reader" + ], + [ + 10, + 7, + "reader" + ], + [ + 5, + 3, + "B" + ], + [ + 6, + 0, + "B" + ], + [ + 6, + 2, + "B" + ], + [ + 6, + 3, + "B" + ], + [ + 7, + 1, + "B" + ], + [ + 7, + 2, + "B" + ], + [ + 8, + 1, + "B" + ], + [ + 10, + 6, + "reader" + ], + [ + 10, + 7, + "reader" + ], + [ + 5, + 3, + "B" + ], + [ + 6, + 0, + "B" + ], + [ + 6, + 2, + "B" + ], + [ + 6, + 3, + "B" + ], + [ + 7, + 1, + "B" + ], + [ + 7, + 2, + "B" + ], + [ + 8, + 1, + "B" + ], + [ + 1, + 4, + "source" + ], + [ + 11, + 7, + "reader" + ], + [ + 5, + 3, + "B" + ], + [ + 6, + 0, + "B" + ], + [ + 6, + 2, + "B" + ], + [ + 6, + 3, + "B" + ], + [ + 7, + 1, + "B" + ], + [ + 7, + 2, + "B" + ], + [ + 8, + 1, + "B" + ], + [ + 11, + 7, + "reader" + ], + [ + 5, + 3, + "B" + ], + [ + 6, + 0, + "B" + ], + [ + 6, + 2, + "B" + ], + [ + 6, + 3, + "B" + ], + [ + 7, + 1, + "B" + ], + [ + 7, + 2, + "B" + ], + [ + 8, + 1, + "B" + ], + [ + 0, + 4, + "source" + ], + [ + 12, + 5, + "reader" + ], + [ + 12, + 6, + "reader" + ], + [ + 12, + 8, + "reader" + ], + [ + 5, + 3, + "B" + ], + [ + 6, + 0, + "B" + ], + [ + 6, + 2, + "B" + ], + [ + 6, + 3, + "B" + ], + [ + 7, + 1, + "B" + ], + [ + 7, + 2, + "B" + ], + [ + 8, + 1, + "B" + ], + [ + 12, + 5, + "reader" + ], + [ + 12, + 6, + "reader" + ], + [ + 12, + 8, + "reader" + ], + [ + 5, + 3, + "B" + ], + [ + 6, + 0, + "B" + ], + [ + 6, + 2, + "B" + ], + [ + 6, + 3, + "B" + ], + [ + 7, + 1, + "B" + ], + [ + 7, + 2, + "B" + ], + [ + 8, + 1, + "B" + ], + [ + 3, + 4, + "source" + ], + [ + 13, + 5, + "reader" + ], + [ + 13, + 6, + "reader" + ], + [ + 13, + 7, + "reader" + ], + [ + 13, + 8, + "reader" + ], + [ + 5, + 3, + "B" + ], + [ + 6, + 0, + "B" + ], + [ + 6, + 2, + "B" + ], + [ + 6, + 3, + "B" + ], + [ + 7, + 1, + "B" + ], + [ + 7, + 2, + "B" + ], + [ + 8, + 1, + "B" + ], + [ + 13, + 5, + "reader" + ], + [ + 13, + 6, + "reader" + ], + [ + 13, + 7, + "reader" + ], + [ + 13, + 8, + "reader" + ], + [ + 5, + 3, + "B" + ], + [ + 6, + 0, + "B" + ], + [ + 6, + 2, + "B" + ], + [ + 6, + 3, + "B" + ], + [ + 7, + 1, + "B" + ], + [ + 7, + 2, + "B" + ], + [ + 8, + 1, + "B" + ], + [ + 2, + 4, + "source" + ], + [ + 14, + 6, + "reader" + ], + [ + 5, + 3, + "B" + ], + [ + 6, + 0, + "B" + ], + [ + 6, + 2, + "B" + ], + [ + 6, + 3, + "B" + ], + [ + 7, + 1, + "B" + ], + [ + 7, + 2, + "B" + ], + [ + 8, + 1, + "B" + ], + [ + 14, + 6, + "reader" + ], + [ + 5, + 3, + "B" + ], + [ + 6, + 0, + "B" + ], + [ + 6, + 2, + "B" + ], + [ + 6, + 3, + "B" + ], + [ + 7, + 1, + "B" + ], + [ + 7, + 2, + "B" + ], + [ + 8, + 1, + "B" + ], + [ + 1, + 4, + "source" + ], + [ + 15, + 5, + "reader" + ], + [ + 15, + 6, + "reader" + ], + [ + 5, + 3, + "B" + ], + [ + 6, + 0, + "B" + ], + [ + 6, + 2, + "B" + ], + [ + 6, + 3, + "B" + ], + [ + 7, + 1, + "B" + ], + [ + 7, + 2, + "B" + ], + [ + 8, + 1, + "B" + ], + [ + 15, + 5, + "reader" + ], + [ + 15, + 6, + "reader" + ], + [ + 5, + 3, + "B" + ], + [ + 6, + 0, + "B" + ], + [ + 6, + 2, + "B" + ], + [ + 6, + 3, + "B" + ], + [ + 7, + 1, + "B" + ], + [ + 7, + 2, + "B" + ], + [ + 8, + 1, + "B" + ], + [ + 0, + 4, + "source" + ], + [ + 16, + 6, + "reader" + ], + [ + 16, + 7, + "reader" + ], + [ + 16, + 8, + "reader" + ], + [ + 5, + 3, + "B" + ], + [ + 6, + 0, + "B" + ], + [ + 6, + 2, + "B" + ], + [ + 6, + 3, + "B" + ], + [ + 7, + 1, + "B" + ], + [ + 7, + 2, + "B" + ], + [ + 8, + 1, + "B" + ], + [ + 16, + 6, + "reader" + ], + [ + 16, + 7, + "reader" + ], + [ + 16, + 8, + "reader" + ], + [ + 5, + 3, + "B" + ], + [ + 6, + 0, + "B" + ], + [ + 6, + 2, + "B" + ], + [ + 6, + 3, + "B" + ], + [ + 7, + 1, + "B" + ], + [ + 7, + 2, + "B" + ], + [ + 8, + 1, + "B" + ] + ], + "registers": 18 + }, + "mixed": { + "cuts": [ + 29, + 33, + 35, + 39, + 44, + 46, + 49, + 54 + ], + "gates": [ + [ + 9, + 5, + "reader" + ], + [ + 9, + 8, + "reader" + ], + [ + 10, + 6, + "reader" + ], + [ + 10, + 7, + "reader" + ], + [ + 11, + 7, + "reader" + ], + [ + 12, + 5, + "reader" + ], + [ + 12, + 6, + "reader" + ], + [ + 12, + 8, + "reader" + ], + [ + 13, + 5, + "reader" + ], + [ + 13, + 6, + "reader" + ], + [ + 13, + 7, + "reader" + ], + [ + 13, + 8, + "reader" + ], + [ + 14, + 6, + "reader" + ], + [ + 15, + 5, + "reader" + ], + [ + 15, + 6, + "reader" + ], + [ + 16, + 6, + "reader" + ], + [ + 16, + 7, + "reader" + ], + [ + 16, + 8, + "reader" + ], + [ + 5, + 3, + "B" + ], + [ + 6, + 0, + "B" + ], + [ + 6, + 2, + "B" + ], + [ + 6, + 3, + "B" + ], + [ + 7, + 1, + "B" + ], + [ + 7, + 2, + "B" + ], + [ + 8, + 1, + "B" + ], + [ + 3, + 4, + "source" + ], + [ + 9, + 5, + "reader" + ], + [ + 9, + 8, + "reader" + ], + [ + 9, + 4, + "output_repair" + ], + [ + 2, + 4, + "source" + ], + [ + 6, + 4, + "connector_repair" + ], + [ + 10, + 6, + "reader" + ], + [ + 10, + 7, + "reader" + ], + [ + 1, + 4, + "source" + ], + [ + 11, + 7, + "reader" + ], + [ + 0, + 4, + "source" + ], + [ + 12, + 5, + "reader" + ], + [ + 12, + 6, + "reader" + ], + [ + 12, + 8, + "reader" + ], + [ + 3, + 4, + "source" + ], + [ + 13, + 5, + "reader" + ], + [ + 13, + 6, + "reader" + ], + [ + 13, + 7, + "reader" + ], + [ + 13, + 8, + "reader" + ], + [ + 2, + 4, + "source" + ], + [ + 14, + 6, + "reader" + ], + [ + 1, + 4, + "source" + ], + [ + 15, + 5, + "reader" + ], + [ + 15, + 6, + "reader" + ], + [ + 0, + 4, + "source" + ], + [ + 6, + 4, + "connector_repair" + ], + [ + 16, + 6, + "reader" + ], + [ + 16, + 7, + "reader" + ], + [ + 16, + 8, + "reader" + ], + [ + 5, + 3, + "B" + ], + [ + 6, + 0, + "B" + ], + [ + 6, + 2, + "B" + ], + [ + 6, + 3, + "B" + ], + [ + 7, + 1, + "B" + ], + [ + 7, + 2, + "B" + ], + [ + 8, + 1, + "B" + ] + ], + "registers": 18 + }, + "output_only": { + "cuts": [ + 29, + 33, + 35, + 40, + 46, + 49, + 53, + 57 + ], + "gates": [ + [ + 9, + 5, + "reader" + ], + [ + 9, + 8, + "reader" + ], + [ + 10, + 6, + "reader" + ], + [ + 10, + 7, + "reader" + ], + [ + 11, + 7, + "reader" + ], + [ + 12, + 5, + "reader" + ], + [ + 12, + 6, + "reader" + ], + [ + 12, + 8, + "reader" + ], + [ + 13, + 5, + "reader" + ], + [ + 13, + 6, + "reader" + ], + [ + 13, + 7, + "reader" + ], + [ + 13, + 8, + "reader" + ], + [ + 14, + 6, + "reader" + ], + [ + 15, + 5, + "reader" + ], + [ + 15, + 6, + "reader" + ], + [ + 16, + 6, + "reader" + ], + [ + 16, + 7, + "reader" + ], + [ + 16, + 8, + "reader" + ], + [ + 5, + 3, + "B" + ], + [ + 6, + 0, + "B" + ], + [ + 6, + 2, + "B" + ], + [ + 6, + 3, + "B" + ], + [ + 7, + 1, + "B" + ], + [ + 7, + 2, + "B" + ], + [ + 8, + 1, + "B" + ], + [ + 3, + 4, + "source" + ], + [ + 9, + 5, + "reader" + ], + [ + 9, + 8, + "reader" + ], + [ + 9, + 4, + "output_repair" + ], + [ + 2, + 4, + "source" + ], + [ + 10, + 6, + "reader" + ], + [ + 10, + 7, + "reader" + ], + [ + 10, + 4, + "output_repair" + ], + [ + 1, + 4, + "source" + ], + [ + 11, + 7, + "reader" + ], + [ + 0, + 4, + "source" + ], + [ + 12, + 5, + "reader" + ], + [ + 12, + 6, + "reader" + ], + [ + 12, + 8, + "reader" + ], + [ + 12, + 4, + "output_repair" + ], + [ + 3, + 4, + "source" + ], + [ + 13, + 5, + "reader" + ], + [ + 13, + 6, + "reader" + ], + [ + 13, + 7, + "reader" + ], + [ + 13, + 8, + "reader" + ], + [ + 13, + 4, + "output_repair" + ], + [ + 2, + 4, + "source" + ], + [ + 14, + 6, + "reader" + ], + [ + 14, + 4, + "output_repair" + ], + [ + 1, + 4, + "source" + ], + [ + 15, + 5, + "reader" + ], + [ + 15, + 6, + "reader" + ], + [ + 15, + 4, + "output_repair" + ], + [ + 0, + 4, + "source" + ], + [ + 16, + 6, + "reader" + ], + [ + 16, + 7, + "reader" + ], + [ + 16, + 8, + "reader" + ], + [ + 5, + 3, + "B" + ], + [ + 6, + 0, + "B" + ], + [ + 6, + 2, + "B" + ], + [ + 6, + 3, + "B" + ], + [ + 7, + 1, + "B" + ], + [ + 7, + 2, + "B" + ], + [ + 8, + 1, + "B" + ] + ], + "registers": 18 + }, + "strict": { + "cuts": [ + 29, + 34, + 36, + 40, + 45, + 47, + 50, + 55 + ], + "gates": [ + [ + 9, + 5, + "reader" + ], + [ + 9, + 8, + "reader" + ], + [ + 10, + 6, + "reader" + ], + [ + 10, + 7, + "reader" + ], + [ + 11, + 7, + "reader" + ], + [ + 12, + 5, + "reader" + ], + [ + 12, + 6, + "reader" + ], + [ + 12, + 8, + "reader" + ], + [ + 13, + 5, + "reader" + ], + [ + 13, + 6, + "reader" + ], + [ + 13, + 7, + "reader" + ], + [ + 13, + 8, + "reader" + ], + [ + 14, + 6, + "reader" + ], + [ + 15, + 5, + "reader" + ], + [ + 15, + 6, + "reader" + ], + [ + 16, + 6, + "reader" + ], + [ + 16, + 7, + "reader" + ], + [ + 16, + 8, + "reader" + ], + [ + 5, + 3, + "B" + ], + [ + 6, + 0, + "B" + ], + [ + 6, + 2, + "B" + ], + [ + 6, + 3, + "B" + ], + [ + 7, + 1, + "B" + ], + [ + 7, + 2, + "B" + ], + [ + 8, + 1, + "B" + ], + [ + 3, + 4, + "source" + ], + [ + 5, + 4, + "connector_repair" + ], + [ + 9, + 5, + "reader" + ], + [ + 9, + 8, + "reader" + ], + [ + 2, + 4, + "source" + ], + [ + 5, + 4, + "connector_repair" + ], + [ + 6, + 4, + "connector_repair" + ], + [ + 10, + 6, + "reader" + ], + [ + 10, + 7, + "reader" + ], + [ + 1, + 4, + "source" + ], + [ + 11, + 7, + "reader" + ], + [ + 0, + 4, + "source" + ], + [ + 12, + 5, + "reader" + ], + [ + 12, + 6, + "reader" + ], + [ + 12, + 8, + "reader" + ], + [ + 3, + 4, + "source" + ], + [ + 13, + 5, + "reader" + ], + [ + 13, + 6, + "reader" + ], + [ + 13, + 7, + "reader" + ], + [ + 13, + 8, + "reader" + ], + [ + 2, + 4, + "source" + ], + [ + 14, + 6, + "reader" + ], + [ + 1, + 4, + "source" + ], + [ + 15, + 5, + "reader" + ], + [ + 15, + 6, + "reader" + ], + [ + 0, + 4, + "source" + ], + [ + 6, + 4, + "connector_repair" + ], + [ + 16, + 6, + "reader" + ], + [ + 16, + 7, + "reader" + ], + [ + 16, + 8, + "reader" + ], + [ + 5, + 3, + "B" + ], + [ + 6, + 0, + "B" + ], + [ + 6, + 2, + "B" + ], + [ + 6, + 3, + "B" + ], + [ + 7, + 1, + "B" + ], + [ + 7, + 2, + "B" + ], + [ + 8, + 1, + "B" + ] + ], + "registers": 18 + } + } +} diff --git a/research/observable-connector-repair/CLAIM.txt b/research/observable-connector-repair/CLAIM.txt new file mode 100644 index 0000000000..e7c227aa99 --- /dev/null +++ b/research/observable-connector-repair/CLAIM.txt @@ -0,0 +1,13 @@ +CLAIM — Recursive interfaces; OS-random assignment seed 50. + +Question: when a common-B dirty connector spans a known, finally restored source-mutation tour, can the connector carry only the correction visible to each current reader, instead of paying full BC coherence after every mutation? Exact object: four binary connector coordinates, one independent source block u, eight distinct output ports, and correction gates z_j += u (optionally y_t += u). Every dirty row and the source must be restored at batch exit; each completed output must be correct at its observation cut. + +Base: ef5f39403610d231a0c27e8a6b4f08c10209bcd6. Closest predecessor: woklerx PR1439 at 3852c2d03044895cebdc9b31b0c7131a617774d2, whose strong boundary requires BC repair. Credit mightyOil PR1203 reader kernels and Hanson Sun PR1246 paid output defects; no priority claim for either identity. Discussion1489 changes B and source together; this scope keeps B fixed and weakens intermediate coherence using reader-specific affine constraints. Discussion1493 shares dyadic source tours; this scope instead optimizes additive connector corrections. + +Method/domain: exact F2 mask-state dynamic programming versus a separately implemented shortest-path oracle; a fixed seed50 four-coordinate/eight-read pilot; all short two-coordinate demand sequences; arbitrary dirty-column and literal-array forward/inverse replay. Charge both B calls, every read, every source update/restoration, connector/output corrections, preparation, storage, dispatch and a declared tape interpreter. Prove optimality only in the fixed correction-gate alphabet. Stop after one bounded package; no supplier, contracting input-size recurrence or new kappa claim. + +Candidates considered: paid output-frame transport (covered by PR1391/1488); strong full-state source repair (PR1439 and Discussion1489); reader-observable repair (chosen). Selected PR1094 source-binding baseline passes; full selected cold replay is out of scope. Entry overlap: complete cached snapshot of 750 open PRs and 183 discussion records, followed by a live recent-claims read. It does not cover all code diffs or certify novelty. + +Expected artifact: research/observable-connector-repair/ with a written interface, exact cost recurrence/certificate, source pins, negative controls and registered replay. Expected finish 2026-10-14 02:36 UTC; final 12 minutes reserved for verification/handoff. Advisory claim expires 03:00 UTC. + +Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance; Apache-2.0. diff --git a/research/observable-connector-repair/OVERLAP.json b/research/observable-connector-repair/OVERLAP.json new file mode 100644 index 0000000000..1a4b4d5026 --- /dev/null +++ b/research/observable-connector-repair/OVERLAP.json @@ -0,0 +1,311 @@ +{ + "status": "POSSIBLE_OVERLAP_NOT_A_NOVELTY_CERTIFICATE", + "searched_at": "2026-10-14T01:52:15.407931+00:00", + "terms": [ + "projected repair", + "reader kernel", + "connector defect", + "output correction", + "partial coherence" + ], + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T01:52:04.767802+00:00", + "complete_pagination": true, + "records": 750 + }, + "discussions": { + "fetched_at": "2026-10-14T01:51:15.571819+00:00", + "complete_pagination": true, + "records": 183 + } + }, + "local_records": 327, + "warnings": [ + "open_prs: offline; cached data may miss current changes", + "discussions: offline; cached data may miss current changes" + ], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "matches_total": 1, + "matches": [ + { + "kind": "pr", + "number": 1246, + "title": "Research construction: paid nonzero reader-defect repair (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1246", + "head": "5ed1ce17a9df4c853a93f9758ba903d2620c3443", + "updated_at": "2026-10-13T21:04:45Z", + "draft": false, + "state": "open", + "matched_terms": [ + "output correction" + ], + "score": 1, + "excerpt": "ation reader calls can defer restoration even when their reader defects do not cancel, provided the output correction is explicitly implemented and charged. This scoped recursive-interface construction reduces the complete seed-selected dirty echo from **380 to 244 ADD/NEG instructions**. Both source-copy passes, all recursive children and inverses, correction and scratch restoration are included. No new kappa is claimed.\n\nOnly `research/paid-reader-defect-seed58/` is added. It contains the writ" + } + ], + "initial_persistent_boundary": { + "status": "POSSIBLE_OVERLAP_NOT_A_NOVELTY_CERTIFICATE", + "searched_at": "2026-10-14T01:51:15.612851+00:00", + "terms": [ + "persistent-boundary", + "persistent boundary", + "deferred restoration", + "multitype", + "heterogeneous-owner-assembly" + ], + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T01:50:57.828262+00:00", + "complete_pagination": true, + "records": 750 + }, + "discussions": { + "fetched_at": "2026-10-14T01:51:15.571819+00:00", + "complete_pagination": true, + "records": 183 + } + }, + "local_records": 327, + "warnings": [], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "matches_total": 8, + "matches": [ + { + "kind": "local-readme", + "title": "research/heterogeneous-owner-assembly/README.md", + "path": "research/heterogeneous-owner-assembly/README.md", + "sha256": "30f5d93adebc874370b63dddf98069079001fbd7b8f078a023d9eeb5d347c185", + "matched_terms": [ + "deferred restoration", + "heterogeneous-owner-assembly" + ], + "score": 4, + "excerpt": "dard library. Run from the repository\nroot with a fresh output filename:\n\n```sh\npython3 -B research/heterogeneous-owner-assembly/verify.py \\\n --audit-base-tree --out /tmp/heterogeneous-owner-bound.json\n```\n\nExpected result:\n\n```text\nPASS_HETEROGENEOUS_OWNER_CATALOGUE_BOUND records=71 interfaces=25 kappa_grid_upper=0.001661960547713947\n```\n\nThe default check replays the frozen source list. It needs no network or Git\nhistory. `--audit-base-tree` also checks the complete pinned Git tree, using\n`gi" + }, + { + "number": 1328, + "title": "CLAIM: coverage-law relief thresholds for the selected complex local word (Navinor, expires 2026-10-14T00:50Z)", + "kind": "discussion", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1328", + "updated_at": "2026-10-13T23:21:26Z", + "matched_terms": [ + "heterogeneous-owner-assembly" + ], + "score": 1, + "excerpt": ".com/CrocSwap/integer-mult-bounds/pull/1264 (14 words at the unchanged law); Ali Romman's `research/heterogeneous-owner-assembly/` (frozen catalogue bound, which explicitly excludes new helper-inventory interfaces such as PR1004/1005's R489/R480).\n\n**Method / domain.** Independent stdlib exact-rational interval moment (atanh-chain logs, Taylor exp with Lagrange remainder, outward rounding), written code-disjoint from #1240. Domain: u in {1..12} plus exact threshold in (1,12]; c in [0,64]; w in [" + }, + { + "number": 1493, + "title": "CLAIM: distinct dyadic BIT outputs sharing a restored source tour (seed55)", + "kind": "discussion", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1493", + "updated_at": "2026-10-14T01:43:33Z", + "matched_terms": [ + "persistent-boundary" + ], + "score": 1, + "excerpt": "nd Discussion1489), and this shared-source multi-output boundary (chosen). Scope is a refinement of persistent-boundary; the changed premise is permission to permute the common source temporarily. The selected PR1094 binding baseline passes; it is context only, not a full cold replay.\n\nExpected artifact: research/shared-dyadic-source/ with a written interface, exact certificate, source pins and failure controls. Expected finish/claim expiry: 2026-10-14 02:35 UTC (October 13, 10:35 p.m. EDT); fin" + }, + { + "number": 1381, + "title": "Noncommuting workspace drift through a sign-character output", + "kind": "discussion", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1381", + "updated_at": "2026-10-13T23:50:29Z", + "matched_terms": [ + "persistent-boundary" + ], + "score": 1, + "excerpt": "cbe5cd4c0eb477c3afeed100190f` (fresh origin/main).\nChooser seed `d43d0282092e46edce787623f2f939e8`, persistent-boundary card;\nrefinement and exact predecessor heads are in TASK.json.\n\nQuestion: can a six-child noncommuting S3 workspace word carry restoration\nthrough its one-row sign-character output, including canonical-output cuts\ninside the character kernel? Price every correction, both child directions\nand a complete source-only echo. Domain: the regular six-row S3 action,\nthe reduced relatio" + }, + { + "kind": "pr", + "number": 1240, + "title": "Research note: packing ceiling (+0.87%) and 1/99 budget for the selected complex local word (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1240", + "head": "1e136b8c4a552050820334ad113628775182f08c", + "updated_at": "2026-10-13T21:31:09Z", + "draft": false, + "state": "open", + "matched_terms": [ + "heterogeneous-owner-assembly" + ], + "score": 1, + "excerpt": "d packing-ceiling lineage is static44, PR525 and PR643; the catalogue mixture bound is Ali Romman's heterogeneous-owner-assembly. The construction credits are in the selected review. Prepared by Douglas Colkitt with substantial Claude (Anthropic) assistance. Apache-2.0.\n\n\ud83e\udd16 Generated with [Claude Code](https://claude.com/claude-code)\n" + }, + { + "kind": "pr", + "number": 1155, + "title": "Research note: restoration coalescing across a recursion batch (read-free + composable-family boundary; no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1155", + "head": "9821c6e9388f3fc097e94b72be9fa7b41a849527", + "updated_at": "2026-10-13T19:16:57Z", + "draft": false, + "state": "open", + "matched_terms": [ + "deferred restoration" + ], + "score": 1, + "excerpt": "dent\nconditions decide it, both decidable exactly:\n\n- **Correctness (read-free batch).** The single deferred restoration returns the\n same observables (final data and final workspace) if and only if no child reads\n the workspace's intermediate value into an observable. One reader child breaks\n it; a concrete Gaussian-rational counterexample is in the certificate.\n- **Cost (composable family).** The rewrite removes passes only when the\n restoration operators stay cheap under composition: unit" + }, + { + "kind": "pr", + "number": 1203, + "title": "Research: noncommuting reader restoration with a paid dirty-state wrapper", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1203", + "head": "38459854fd5bb93099871a84324413bd0e338d8e", + "updated_at": "2026-10-13T20:01:31Z", + "draft": false, + "state": "open", + "matched_terms": [ + "deferred restoration" + ], + "score": 1, + "excerpt": "ursive interface; no new kappa.** PR1155's pinned note says any read of drifting workspace prevents deferred restoration. Nonzero readers can instead preserve the observed value: for distinct outputs, the exact all-input condition is `H_i(P_(i-1)-I)=0`. With one shared output observed only at batch exit, only the sum of defects must vanish. The note proves both statements and gives explicit compatible and incompatible examples.\n\nA noncommuting eight-coordinate, three-child construction includes " + }, + { + "kind": "pr", + "number": 1348, + "title": "Scoped thresholds: what a coverage-law change must deliver for the selected complex local word (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1348", + "head": "6840924bf22523a9f0a965238a22cc3bcfc7297b", + "updated_at": "2026-10-13T23:20:20Z", + "draft": false, + "state": "open", + "matched_terms": [ + "heterogeneous-owner-assembly" + ], + "score": 1, + "excerpt": "hresholds, the pair obstruction and convexity margins, on the base commit.\n- Ali Romman's `research/heterogeneous-owner-assembly/` bounds the frozen catalogue's 25 cost interfaces and excludes new helper-inventory interfaces (the R489/R480 interfaces of CrocSwap/integer-mult-bounds#1004 and CrocSwap/integer-mult-bounds#1005); these thresholds price what such a new interface must deliver.\n- Distinct from https://github.com/CrocSwap/integer-mult-bounds/discussions/1265 (idle repartitions at a fixe" + } + ] + }, + "manual_nearest_prs": [ + { + "number": 1199, + "head": "85ac2880ea5bda44f28632b71ffa2b4e35ec6b7d" + }, + { + "number": 1203, + "head": "38459854fd5bb93099871a84324413bd0e338d8e" + }, + { + "number": 1246, + "head": "5ed1ce17a9df4c853a93f9758ba903d2620c3443" + }, + { + "number": 1391, + "head": "6ce8017e4c27c8b220b6c3a27a53bb18f138212a" + }, + { + "number": 1439, + "head": "3852c2d03044895cebdc9b31b0c7131a617774d2" + }, + { + "number": 1488, + "head": "13d780ea51248ddd51901cd546b9f59adc76eb43" + } + ], + "current_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1501", + "final_refresh": { + "status": "POSSIBLE_OVERLAP_NOT_A_NOVELTY_CERTIFICATE", + "searched_at": "2026-10-14T02:08:51.193413+00:00", + "terms": [ + "observable connector", + "projected repair", + "connector correction", + "reader defect", + "source-mutation" + ], + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T02:08:30.720710+00:00", + "complete_pagination": true, + "records": 762 + }, + "discussions": { + "fetched_at": "2026-10-14T02:08:51.150383+00:00", + "complete_pagination": true, + "records": 196 + } + }, + "local_records": 329, + "warnings": [], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "matches_total": 5, + "matches": [ + { + "kind": "local-readme", + "title": "research/observable-connector-repair/README.md", + "path": "research/observable-connector-repair/README.md", + "sha256": "7b5a29acae27e492e554e46cde4ac582af64af0f0ab6a5490397c2272a455d58", + "matched_terms": [ + "observable connector", + "connector correction", + "source-mutation" + ], + "score": 3, + "excerpt": "hanging source when the current reader sees\nonly a quotient. The fixed seed-50 example needs **four connector corrections\ninstead of fourteen full-coherence corrections**. Allowing a paid output\ncorrection lowers the exact minimum to **three**: two connector XORs and one\noutput XOR. The complete program has **61 XORs instead of 72**, with the same\nsource mutations, readers, two B calls, and final restoration.\n\nThe contribution refines woklerx's [PR1439](https://github.com/CrocSwap/integer-mult-b" + }, + { + "kind": "local-task", + "title": "research/observable-connector-repair/TASK.json", + "path": "research/observable-connector-repair/TASK.json", + "sha256": "b9834d4bc125c9419ceb9f8b87a63fa7565fde46988c71052d76bf5c41fa5ccc", + "matched_terms": [ + "observable connector", + "connector correction", + "source-mutation" + ], + "score": 3, + "excerpt": "tion\",\n \"multitype\"\n ]\n },\n \"scope_status\": \"refined\",\n \"actual_scope\": \"Optimize reader-observable connector correction masks across a finally restored source-mutation tour, including optional paid output repair.\",\n \"scope_change_reason\": \"Refines persistent-boundary to a fixed common-B batch whose intermediate coherence is required only through each current reader, with complete restoration at exit.\",\n \"bottleneck_link\": \"The pilot removes eleven correction XORs from a full-cohere" + }, + { + "number": 1501, + "title": "CLAIM: reader-observable repair across a restored source tour (seed50)", + "kind": "discussion", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1501", + "updated_at": "2026-10-14T01:54:13Z", + "matched_terms": [ + "connector correction", + "source-mutation" + ], + "score": 2, + "excerpt": "ndom assignment seed 50.\n\nQuestion: when a common-B dirty connector spans a known, finally restored source-mutation tour, can the connector carry only the correction visible to each current reader, instead of paying full BC coherence after every mutation? Exact object: four binary connector coordinates, one independent source block u, eight distinct output ports, and correction gates z_j += u (optionally y_t += u). Every dirty row and the source must be restored at batch exit; each completed out" + }, + { + "number": 1489, + "title": "DONE: paid complex connector reader-change repair, 41 to 33 ADDs (PR1506)", + "kind": "discussion", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1489", + "updated_at": "2026-10-14T01:55:33Z", + "matched_terms": [ + "source-mutation" + ], + "score": 1, + "excerpt": " restoration paid?\nPredecessor: #1439 at 3852c2d03044895cebdc9b31b0c7131a617774d2 (woklerx, fixed B/source-mutation pilot), Ross Richardson's universal-connector package. This changes fixed B and characteristic two; it does not repeat the five-source/two-connector census.\nMethod/domain: derive the exact characteristic-zero adapter for B0->B1 and x+=Cu; symbolic dirty-state replay plus an exhaustive 2x2 binary-coefficient matrix domain interpreted over Q. Price a 3x3 integer fixed-port pilot incl" + }, + { + "kind": "pr", + "number": 1246, + "title": "Research construction: paid nonzero reader-defect repair (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1246", + "head": "5ed1ce17a9df4c853a93f9758ba903d2620c3443", + "updated_at": "2026-10-13T21:04:45Z", + "draft": false, + "state": "open", + "matched_terms": [ + "reader defect" + ], + "score": 1, + "excerpt": "Fixed signed-permutation reader calls can defer restoration even when their reader defects do not cancel, provided the output correction is explicitly implemented and charged. This scoped recursive-interface construction reduces the complete seed-selected dirty echo from **380 to 244 ADD/NEG instructions**. Both source-copy passes, all recursive children and inverses, correction and scratch restoration are included. No new kappa is claimed.\n\nOnly `research/paid-reader-defect-seed58/` is added. I" + } + ] + }, + "new_adjacent_submission": { + "number": 1506, + "head": "d255ec2facc9b5b990b8b71536a0f2d87f7de101", + "distinction": "Characteristic-zero B-change/source-change adapter keeps strong coherence. Our F2 fixed-B batch optimizes reader-observable correction states." + } +} diff --git a/research/observable-connector-repair/PREDECESSORS.json b/research/observable-connector-repair/PREDECESSORS.json new file mode 100644 index 0000000000..55ea903689 --- /dev/null +++ b/research/observable-connector-repair/PREDECESSORS.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "references": [ + { + "pr": 1439, + "head": "3852c2d03044895cebdc9b31b0c7131a617774d2", + "author": "woklerx", + "source_path": "research/mutable-source-persistent-connector/README.md", + "retained_path": "references/PR1439-README.md", + "git_blob": "53ef4d0d3e527ece35b5f09816ec756b6bc9f100", + "sha256": "1cb2636f93330e41cfdbc9436bc4df6706ce1141fe05da8fd7b72f29fe682f4d", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/3852c2d03044895cebdc9b31b0c7131a617774d2/research/mutable-source-persistent-connector/README.md", + "usage": "Context and attribution only; no predecessor executable imported." + }, + { + "pr": 1203, + "head": "38459854fd5bb93099871a84324413bd0e338d8e", + "author": "mightyOil", + "source_path": "research/invariant-reader-restoration/README.md", + "retained_path": "references/PR1203-README.md", + "git_blob": "b884fdff7672cacd8cc9014b75d4b3e1d6c7f606", + "sha256": "039206964404ab6e6a57fca7aa55057796263c0e5cb102d9e2990b38685f7ad1", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/38459854fd5bb93099871a84324413bd0e338d8e/research/invariant-reader-restoration/README.md", + "usage": "Context and attribution only; no predecessor executable imported." + }, + { + "pr": 1246, + "head": "5ed1ce17a9df4c853a93f9758ba903d2620c3443", + "author": "bbMisk", + "source_path": "research/paid-reader-defect-seed58/README.md", + "retained_path": "references/PR1246-README.md", + "git_blob": "e9263fffce7aa51fa0a86821dfbf17f817d50348", + "sha256": "31a9770a4dfa057a84def481132591b5400a58f1f1ccf802747c3f0db2a54b60", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/5ed1ce17a9df4c853a93f9758ba903d2620c3443/research/paid-reader-defect-seed58/README.md", + "usage": "Context and attribution only; no predecessor executable imported." + } + ] +} diff --git a/research/observable-connector-repair/README.md b/research/observable-connector-repair/README.md new file mode 100644 index 0000000000..813732c094 --- /dev/null +++ b/research/observable-connector-repair/README.md @@ -0,0 +1,265 @@ +# Repair the observable part of a persistent connector + +**Scoped recursive-interface construction; no new kappa.** A connector need +not track every component of a changing source when the current reader sees +only a quotient. The fixed seed-50 example needs **four connector corrections +instead of fourteen full-coherence corrections**. Allowing a paid output +correction lowers the exact minimum to **three**: two connector XORs and one +output XOR. The complete program has **61 XORs instead of 72**, with the same +source mutations, readers, two B calls, and final restoration. + +The contribution refines woklerx's [PR1439](https://github.com/CrocSwap/integer-mult-bounds/pull/1439): +its stronger intermediate contract still correctly requires the full BC +adapter. We weaken that contract at explicitly typed observation cuts and +optimize partial connector corrections together with paid output corrections. +Reader kernels, dirty cancellation, source repair and output-defect repair are +predecessor ideas, credited below. The new evidence is this correction-mask +recurrence, its exact finite optimum and the completely emitted comparison. + +This is a fixed-query interface result. Opening the toy matrices and directly +forming each A_i B product costs **26 XORs**, including the same source updates +and observation cuts. That checked control rules out any claim that 61 is a +minimum over arbitrary circuits. No selected supplier requiring these fixed +queries is identified, and no improved multiplication exponent is claimed. + +## Contract and identity + +Work over F2 with L-bit blocks. The distinct rows are d source blocks x, +one independent source block u, d connector blocks z, m output blocks y_i, +and an untouched spectator. All have arbitrary initial values. Fixed binary +B is d by d; a_i is a binary reader row. Source updates x_j += u follow a +known word. Its cumulative mask is q_i at reader i, and q_m=0 at exit. +Thus x_i=x_0+q_i u. The requested output at cut i is + +``` +y_i = y_i_initial + a_i B (x_0 + q_i u). +``` + +Every completed output stays correct at subsequent cuts. Future output ports +are reserved and may be prewritten before their first observation. The open +connector is hidden and reserved. The source may be observed at each completed +stage, with its prescribed current value. At batch exit x, u, z and the +spectator must all be restored. No output aliases another row. Adaptive readers, +unannounced source changes, early observation of future outputs, or reuse of +an open connector are outside this contract. + +Prewrite every output with `y_i += a_i z_initial`, then open the connector +with `z += B x_0`. Let its carried correction be k_i u, so at read i + +``` +z = z_initial + B x_0 + k_i u. +``` + +Apply the second `y_i += a_i z` and, in the enlarged alphabet, an optional +`y_i += p_i u`. The old connector dirt cancels. Correctness for all input +blocks is equivalent to + +``` +a_i k_i + p_i = delta_i, delta_i = a_i B q_i. (1) +``` + +Necessity follows by setting one bit of u to one; sufficiency follows by +substitution. All other dirty variables cancel independently. At exit return +k to zero and close `z += B x` after q has returned to zero. This restores the +entire connector, including the directions hidden from previous readers. +The literal reversed XOR word is the inverse, with every gate paid again. + +Full coherence is the special choice k_i=Bq_i and p_i=0. Equation (1) permits +other representatives of the reader's affine coset. This does not refute the +necessity of BC under PR1439's stronger boundary. It changes the admitted +intermediate state while retaining the exact requested observables. + +## Complete cost recurrence and its scope + +The fixed-query alphabet requires the two B calls, the two reads for every +output, and the prescribed source updates. Only the corrections vary: +`z_j += u`, and optionally `y_i += u` before output i's observation. +No extra source queries, direct A_i B calls, register mixing, clean helper, +free frame change or skipped restoration is allowed. Each allowed complete +call restores private scratch and heads. All correction costs are positive. + +Let w_j(L) price one complete connector correction, and v_i(L) one output +correction. Prices include source/coefficient access, arithmetic, scratch +restoration, routing, frames and dispatch for the chosen implementation. +For h,k in F2^d put + +``` +d_w(h,k) = sum_j w_j(L) [h_j != k_j]. +F_0(0)=0; F_0(k != 0)=infinity. +F_i(k) = min_h (F_(i-1)(h) + d_w(h,k) + v_i(L)*(delta_i + a_i k)). +R(L) = min_k (F_m(k) + d_w(k,0)). (2) +``` + +All sums inside the last bit expression are modulo two. In the connector-only +alphabet, retain only states with `a_i k=delta_i` and omit the v term. +The complete batch charge is + +``` +C(L) = P(L) + I(L) + c_B_open(L) + c_B_close(L) + + sum_i (c_Ai_pre(L) + c_Ai_read(L) + c_source_i(L)) + R(L). (3) +``` + +P pays program/coefficient/plan preparation; I pays layout, admission and +reservation. Every complete child call and both B directions appear. If used +as a forward/inverse echo, charge both words plus that parent's actual copies, +readouts and admission; they are not free or included implicitly in (3). +No separate COPY or helper is used by the emitted batch. Fixed port roles avoid +frame changes in this pilot; a physical supplier must add any required ones. + +To prove optimality in this alphabet, commute corrections between consecutive +observations and cancel repeated toggles. Reaching k from h costs at least +one w_j for each differing bit; toggling those coordinates attains that price. +An output needs parity p_i from (1), so zero or one v_i is optimal. Any schedule +therefore yields a path counted by (2); every such path emits a legal schedule. +Induction on i proves the recurrence. This is a stage recurrence, **not a +contracting input-size supplier recurrence**. + +The independent oracle instead uses a graph with vertices (stage,k), individual +paid coordinate-toggle edges and free/paid observation edges. Stored integer +potentials satisfy every edge inequality. Their value at the terminal zero +state is a lower bound, and the emitted path attains it. No floating-point +search decision or finite replay is used as a proof of the all-L identity. + +## Exact fixed example + +OS seed 50 selected recursive interfaces and the fixture in `model.selected`. +Three bounded matrix draws select the first invertible B; there is no +optimization search over fixtures. Masks use bit j for coordinate j. + +``` +B rows: [8,13,6,2] +a_i: [9,6,4,11,15,2,3,14] +source steps: [3,2,1,0,3,2,1,0] +q_i: [8,12,14,15,7,3,1,0] +Bq_i: [3,5,9,11,8,14,2,0] +delta_i: [1,1,0,1,1,1,1,0] +``` + +Connector-only states at the eight reads are `[1,2,2,2,2,2,2,0]`. +The path starts and ends at zero and costs four XORs. A shorter restored path +would have zero or two toggles. Zero fails the first demand; two toggles could +only hold one coordinate through the first two nonzero demands. Those readers +have disjoint support (`9 & 6 = 0`), so two are impossible. + +The mixed optimum uses `[0,2,2,2,2,2,2,0]`, with a direct correction to the first +output. Fewer than three gates would be at most two output repairs (six are +needed without connector help), or two connector toggles with no output repair +(already excluded). The three-gate witness attains the minimum. The graph +certificate additionally proves the weighted minima used below. + +| Complete fixed fixture | Correction XORs | Total XORs | Data-head steps, L=1 | +|---|---:|---:|---:| +| Separately closed query pairs | 0 | 156 | 2732 | +| Carried full coherence, PR1439-style | 14 | 72 | 1484 | +| Output-only repair | 6 | 64 | 1434 | +| Observable connector repair | 4 | 62 | 1328 | +| Mixed observable/output repair | 3 | 61 | 1324 | +| Direct product fusion, outside the alphabet | 0 | 26 | 562 | + +The new reduction is **72 to 61**, beyond the already credited shared-query +reduction. It saves eleven XORs and 160 data-head steps at L=1. No runtime +speedup follows from these abstract instruction counts. + +## Tape, preparation and storage accounting + +The literal interpreter stores row-major L-bit blocks in one-based tape cells: +x occupies rows 0..3, u row 4, z rows 5..8, outputs rows 9..16, spectator row 17. +For each bitwise XOR it visits source, target, then origin. It charges two +reads, one write, one XOR and one dispatch. The finite-control bit latch is set +when reading the source and reset in the target-write transition; it returns +to its entry state on every gate. No dirty data row is used as scratch. The +interpreter assumes instruction delivery at dispatch; a backend's address +decoding and instruction-tape movement must be included in its complete call +price. The five-unit tariff is not a claim that such delivery is free on a +Turing machine. + +For a block XOR between rows s,t, the data-head travel is exactly +`(2 max(s,t)+1)L^2 + L`; the declared online tariff adds `5L`. +The mixed correction bill is `45L^2+18L`, against full coherence's +`194L^2+84L`. Thus complete online bills are + +``` +full coherence: 1412L^2 + 432L +mixed repair: 1263L^2 + 366L +saving: 149L^2 + 66L. +``` + +The same path minimizes both the quadratic coefficient (45) and gate count +(3), certified separately, hence minimizes this correction tariff for every +positive integer L. Data-head movement and instruction traffic are distinct: +instruction records number `72L` versus `61L`, and data storage is `18L` bits +in both. Records contain two addresses and an opcode, so their representation +uses O(log L) bits each. These are explicit counts for this interpreter, not +an all-size Turing-machine implementation or a free coefficient-access claim. + +For dynamic instances, recurrence (2) examines m*4^d transitions after distance +precomputation. This small reference implementation additionally copies path +tuples for deterministic tie breaking and stores O(m*2^d) entries; discovering +a plan is not charged as zero online work. Fixed B/readers and the selected +plan can be compiled once, with program construction and coefficient storage +charged in P and per-call instruction delivery charged in the complete call prices. The complete advantage survives only if the candidate's +extra P+I cost is less than the saved online bill. An actual recursive backend +must supply its complete costs, layout and precision admission. This package +does not establish that instance. + +## Reproduce and verification boundary + +From the repository root, with Python 3.12 and no third-party dependencies: + +```sh +python3.12 scripts/research_package.py --package research/observable-connector-repair +``` + +Expected: `PASS_OBSERVABLE_CONNECTOR strict=4 mixed=3 coherent=14 +complete_xors=72_to_61 small_cases=6220 controls=14 no_new_kappa`, five passing +package tests, then `PASS_REGISTERED_RESEARCH_PACKAGE`. +A standalone replay is `python3 -I -O -B research/observable-connector-repair/verify.py`. +`--write NEW_PATH` only exports an authoring candidate; ordinary replay compares +every recomputed field against [CERTIFICATE.json](CERTIFICATE.json). + +Coverage: all 1,555 width-two demand sequences of length zero through four, +each in two tariffs and two alphabets (6,220 cases), compared with a separately +implemented shortest-path oracle. Lengths through three also enumerate every +mask path. Six complete pilot programs pass 648 independent array basis-column +checks across L=1,2,3, with literal inverses; a smaller batch checks all 256 +dirty inputs. There are 5,696 observation checks and fourteen semantic/domain +controls. The package tests reject altered minima, missing certificates, +modified predecessor notes and changed live source, and check read-only +relocation plus byte-identical certificate export. Separate implementations +were authored in the same AI-assisted session; this is not independent human +review or proof-assistant formalization. + +Research base: `ef5f39403610d231a0c27e8a6b4f08c10209bcd6`. +The selected certificate still names conditional kappa `0.001672660197076918`; +its source-binding baseline was checked, not its complete cold replay. +[CLAIM.txt](CLAIM.txt), [TASK.json](TASK.json), [SOURCES.json](SOURCES.json), +[PREDECESSORS.json](PREDECESSORS.json) and [OVERLAP.json](OVERLAP.json) record scope, +exact pins and bounded overlap coverage. No selected record, upstream source, +frozen package or review disposition is changed. + +## Open next questions + +Does a real supplier expose a common-B boundary with source mutations and +reserved future outputs matching this contract? It matters because it decides +whether the eleven saved corrections can survive admission and routing costs. +A first step is to extract one actual pair/batch of entry and exit contracts +and compare (3) with its complete existing bill. The blocker is a hosted +supplier instance, not the finite mask optimizer. This question and the +constraint on early output writes are also recorded in TASK.json. + +## Credit + +Prepared by **Hanson Sun (@bbMisk)** with substantial **OpenAI Codex assistance** +in derivation, both implementations, verification and prose. New work is +Apache-2.0. Prose was checked against the source notes and computed evidence. + +Credit woklerx's PR1439 strong coherent source-mutation interface; mightyOil's +PR1203 distinct-reader kernel criterion and dirty wrapper; Hanson's PR1246 +paid output-defect construction; Sagar Thakrar's PR1199/1227 cut and sign-frame +work; Ross Richardson's retained universal-connector/PR934 lineage and the +preceding dirty-echo work. The three most direct pending notes are retained +unchanged with exact heads and hashes. No priority is claimed for cancellation, +reader kernels, BC repair, paid output correction or dynamic programming. +Concurrent PR1506 (Discussion1489) changes both B and source over characteristic +zero while retaining strong connector coherence. Discussion1493 shares dyadic +source-query tours. Neither is incorporated as an assumed result. diff --git a/research/observable-connector-repair/SOURCES.json b/research/observable-connector-repair/SOURCES.json new file mode 100644 index 0000000000..1c8542e738 --- /dev/null +++ b/research/observable-connector-repair/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "research/universal-connector-boundary/README.md", + "usage": "input", + "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f", + "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476" + } + ] +} diff --git a/research/observable-connector-repair/TASK.json b/research/observable-connector-repair/TASK.json new file mode 100644 index 0000000000..89d0076ccb --- /dev/null +++ b/research/observable-connector-repair/TASK.json @@ -0,0 +1,62 @@ +{ + "schema_version": 1, + "task_id": "persistent-boundary", + "priority_revision": 2, + "base_commit": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "original_card": { + "id": "persistent-boundary", + "question": "Can a specified pair of consecutive calls eliminate a restoration that the next call reconstructs?", + "starting_points": [ + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Write typed entry/exit contracts and a contracting multitype recurrence.", + "Derive a lower bound for the compulsory transitions of one proposed typed interface." + ], + "acceptance_gate": "Show actual eliminated work and legal composition; changing a scalar recurrence into a matrix is insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Find a concrete consecutive-call boundary in the selected review and list its entry/exit obligations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Specify two call types and one operation actually removed by composition; derive the normalized recurrence.", + "bottleneck_link": "Eliminating compulsory boundary work can lower recursive cost beyond packing gains.", + "allowed_variations": [ + "A two-type pilot or one explicit deferred restoration." + ], + "scope_change_triggers": [ + "Rewriting the old scalar recurrence as a matrix without eliminating work." + ], + "overlap_terms": [ + "persistent boundary", + "deferred restoration", + "multitype" + ] + }, + "scope_status": "refined", + "actual_scope": "Optimize reader-observable connector correction masks across a finally restored source-mutation tour, including optional paid output repair.", + "scope_change_reason": "Refines persistent-boundary to a fixed common-B batch whose intermediate coherence is required only through each current reader, with complete restoration at exit.", + "bottleneck_link": "The pilot removes eleven correction XORs from a full-coherence interface; a real supplier and contracting input-size recurrence remain uninstantiated.", + "budget_minutes": 48, + "stop_rule": "One seed-selected width-four/eight-read pilot; complete width-two demand sequences of length zero through four; no search for a supplier or kappa.", + "outcome": "completed", + "evidence": "CERTIFICATE.json, model.py, oracle.py, verify.py and test_package.py: exact recurrence, literal complete words, sharp correction minimum and negative controls.", + "author": "Hanson Sun (@bbMisk)", + "ai_assistance": "Substantial OpenAI Codex assistance in derivation, both implementations, verification and prose; no independent human reviewer.", + "open_questions": [ + { + "question": "Does a selected supplier expose a common-B source-mutation batch admitting reader-only intermediate coherence?", + "why_it_matters": "Only such an instance can convert this scoped correction saving into a paid recursive-profile improvement.", + "first_step": "Extract actual entry/exit and observation contracts and price formula (3) including preparation, frames, storage and routing.", + "blocked_by": "No hosted supplier with these fixed queries and permission for early writes to future outputs has been identified." + } + ], + "assignment_seed": 50, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1501" +} diff --git a/research/observable-connector-repair/VALIDATION.json b/research/observable-connector-repair/VALIDATION.json new file mode 100644 index 0000000000..6f52d26a25 --- /dev/null +++ b/research/observable-connector-repair/VALIDATION.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "recorded_at_utc": "2026-10-14T02:10:34.428077+00:00", + "base_commit": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "refreshed_main": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "platform": "macOS-27.0.1-arm64-arm-64bit-Mach-O", + "results": [ + { + "command": "python3.12 scripts/research_package.py --package research/observable-connector-repair", + "python": "3.12.13", + "exit_code": 0, + "result": "Exact verifier and all five package tests passed; registered replay passed." + }, + { + "command": "python3 -I -O -B research/observable-connector-repair/verify.py", + "python": "3.14.6", + "exit_code": 0, + "result": "PASS_OBSERVABLE_CONNECTOR strict=4 mixed=3 coherent=14 complete_xors=72_to_61 small_cases=6220 controls=14 no_new_kappa" + }, + { + "command": "python3 -B scripts/verify_selected_result.py", + "exit_code": 0, + "result": "Selected record, exact kappa, original source inventory and proof supplement passed." + }, + { + "command": "python3 -B scripts/research_baseline.py", + "exit_code": 0, + "result": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY; binding primitive complex." + } + ], + "predecessor_live_bindings": [ + { + "pr": 1439, + "head": "3852c2d03044895cebdc9b31b0c7131a617774d2", + "git_blob": "53ef4d0d3e527ece35b5f09816ec756b6bc9f100", + "match": true + }, + { + "pr": 1203, + "head": "38459854fd5bb93099871a84324413bd0e338d8e", + "git_blob": "b884fdff7672cacd8cc9014b75d4b3e1d6c7f606", + "match": true + }, + { + "pr": 1246, + "head": "5ed1ce17a9df4c853a93f9758ba903d2620c3443", + "git_blob": "e9263fffce7aa51fa0a86821dfbf17f817d50348", + "match": true + } + ], + "certificate_sha256": "8ed639273e14def50a9203108deb92e13d61c8d1f308324d02d4aec4b70f22fa", + "code_sha256": { + "test_package.py": "ea517c912e0bb65bdb52ee42407bb4fc070a089a5fc979e390fdcf137896d956", + "model.py": "c068d5d8f160482a34ba5cf58bff503cb0bdd5d402efbbdb3e0ae9e8774ac4bd", + "oracle.py": "69d2ab5b2ab1774ae652ad5ba6a51c7b8376141c23d295474d45bc75c34b99b7", + "verify.py": "27b2491025c714233f670b1e8ea59f16d1248dc291aaf6bef09d052e2684f87c" + }, + "not_run": [ + "Selected full cold replay make frontier1094-verify", + "Physical supplier/compiler admission", + "Contracting input-size recurrence", + "Proof-assistant formalization", + "Independent human review" + ], + "hosted_ci": "Not run before submission; inspect the PR checks separately." +} diff --git a/research/observable-connector-repair/VERIFY.json b/research/observable-connector-repair/VERIFY.json new file mode 100644 index 0000000000..f4d687eecb --- /dev/null +++ b/research/observable-connector-repair/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/universal-connector-boundary/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact mask optimum, independent shortest-path duals, full dirty-state words and inverses, exhaustive small demands, literal tape invoice and semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 120, + "checks": "Five packaging tests: read-only relocation, deterministic export, false-minimum/missing-certificate and pinned-source rejection controls." + } + ] +} diff --git a/research/observable-connector-repair/model.py b/research/observable-connector-repair/model.py new file mode 100644 index 0000000000..4f6c94d1ab --- /dev/null +++ b/research/observable-connector-repair/model.py @@ -0,0 +1,230 @@ +"""Exact observable-connector model. Hanson Sun, with OpenAI Codex. Apache-2.0.""" +import hashlib +import json +import random + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def dot(a, b): + return (a & b).bit_count() % 2 + + +def matvec(rows, x): + return sum(dot(row, x) << i for i, row in enumerate(rows)) + + +def rank(rows): + pivots = {} + for row in rows: + while row: + j = row.bit_length() - 1 + if j in pivots: + row ^= pivots[j] + else: + pivots[j] = row + break + return len(pivots) + + +def selected(): + rng = random.Random(50) + # The first full-rank draw is a fixture choice, not an optimization search. + B = [3, 6, 12, 9] + draws = 0 + while rank(B) != 4: + B = [rng.randrange(1, 16) for _ in range(4)] + draws += 1 + require(draws <= 100, "fixture draw cap exceeded") + readers = rng.sample(range(1, 16), 8) + order = list(range(4)) + rng.shuffle(order) + return {"width": 4, "B": B, "readers": readers, "steps": order + order, + "seed": 50, "matrix_draws": draws} + + +def demands(spec): + d, B, readers, steps = (spec[k] for k in ("width", "B", "readers", "steps")) + require(type(d) is int and 1 <= d <= 8, "width outside bounded implementation") + require(len(B) == d and len(readers) == len(steps), "bad shape") + require(all(type(a) is int and 0 <= a < 1 << d for a in B + readers), "bad binary mask") + require(all(type(j) is int and 0 <= j < d for j in steps), "bad source step") + q, out = 0, [] + for a, j in zip(readers, steps): + q ^= 1 << j + bq = matvec(B, q) + out.append({"reader": a, "source_mask": q, "coherent_mask": bq, + "demand": dot(a, bq)}) + require(q == 0, "source tour must restore the source") + return out + + +def solve(d, conditions, weights, output_prices=None): + """Bellman recurrence over every connector correction mask; no pruning.""" + require(type(d) is int and 1 <= d <= 8, "bad width") + require(len(weights) == d and all(type(w) is int and w > 0 for w in weights), "bad weights") + require(all(type(a) is int and 0 <= a < 1 << d and type(b) is int and b in (0, 1) + for a, b in conditions), "bad conditions") + require(output_prices is None or (len(output_prices) == len(conditions) + and all(type(w) is int and w > 0 for w in output_prices)), "bad output prices") + size = 1 << d + distances = [sum(w for j, w in enumerate(weights) if mask >> j & 1) for mask in range(size)] + best = {0: (0, ())} + tables = [[0] + [None] * (size - 1)] + for i, (a, b) in enumerate(conditions): + nxt = {} + for k in range(size): + defect = b ^ dot(a, k) + if defect and output_prices is None: + continue + penalty = defect * output_prices[i] if output_prices is not None else 0 + if best: + nxt[k] = min((cost + distances[h ^ k] + penalty, path + (k,)) + for h, (cost, path) in best.items()) + best = nxt + tables.append([best[k][0] if k in best else None for k in range(size)]) + require(bool(best), "infeasible observable demands") + cost, path = min((cost + distances[k], path + (0,)) for k, (cost, path) in best.items()) + corrections = [b ^ dot(a, k) for (a, b), k in zip(conditions, path)] + return {"cost": cost, "path": list(path), "output_corrections": corrections, + "tables": tables, "weights": list(weights), "output_prices": output_prices} + + +def emit(spec, strategy, solution=None): + """Emit every scalar XOR, including source and connector restoration.""" + d, readers = spec["width"], spec["readers"] + ds = demands(spec) + u, z0, y0 = d, d + 1, 2 * d + 1 + count = y0 + len(readers) + 1 # last row is an arbitrary dirty spectator + gates, cuts = [], [] + + def gate(target, source, kind): + require(target != source, "aliasing XOR") + gates.append([target, source, kind]) + + def b_call(): + for j, row in enumerate(spec["B"]): + for h in range(d): + if row >> h & 1: + gate(z0 + j, h, "B") + + def read(i): + for j in range(d): + if readers[i] >> j & 1: + gate(y0 + i, z0 + j, "reader") + + def repair(delta): + for j in range(d): + if delta >> j & 1: + gate(z0 + j, u, "connector_repair") + + if strategy == "direct": + # Deliberately outside the fixed-query alphabet: open/fuse A_i B. + for i, j in enumerate(spec["steps"]): + gate(j, u, "source") + row = 0 + for h, brow in enumerate(spec["B"]): + if readers[i] >> h & 1: + row ^= brow + for h in range(d): + if row >> h & 1: + gate(y0 + i, h, "direct_product") + cuts.append(len(gates)) + elif strategy == "eager": + for i, j in enumerate(spec["steps"]): + gate(j, u, "source") + read(i) + b_call() + read(i) + b_call() + cuts.append(len(gates)) + else: + if strategy == "coherent": + path = [x["coherent_mask"] for x in ds] + [0] + outputs = [0] * len(readers) + elif strategy == "output_only": + path = [0] * (len(readers) + 1) + outputs = [x["demand"] for x in ds] + else: + require(strategy == "planned" and solution is not None, "unknown strategy") + path, outputs = solution["path"], solution["output_corrections"] + require(len(path) == len(readers) + 1 and path[-1] == 0, "unrestored plan") + require(len(outputs) == len(readers), "bad output correction shape") + require(all(type(k) is int and 0 <= k < 1 << d for k in path), "bad plan mask") + require(all(type(p) is int and p in (0, 1) for p in outputs), "bad output correction") + require(all(dot(x["reader"], k) ^ p == x["demand"] + for x, k, p in zip(ds, path, outputs)), "unobservable plan") + # Early prewrites are explicit; future output ports are reserved. + for i in range(len(readers)): + read(i) + b_call() + old = 0 + for i, j in enumerate(spec["steps"]): + gate(j, u, "source") + repair(old ^ path[i]) + old = path[i] + read(i) + if outputs[i]: + gate(y0 + i, u, "output_repair") + cuts.append(len(gates)) + repair(old) + b_call() + return {"registers": count, "gates": gates, "cuts": cuts} + + +def expected_rows(spec, cut=None): + d, m = spec["width"], len(spec["readers"]) + rows = [1 << j for j in range(2 * d + m + 2)] + upto = m if cut is None else cut + 1 + q = 0 + for i, step in enumerate(spec["steps"][:upto]): + q ^= 1 << step + a = spec["readers"][i] + linear = 0 + for j, brow in enumerate(spec["B"]): + if a >> j & 1: + linear ^= brow + rows[2 * d + 1 + i] ^= linear + rows[2 * d + 1 + i] ^= dot(linear, q) << d + for j in range(d): + rows[j] ^= ((q >> j) & 1) << d + return rows + + +def check_word(spec, word): + rows = [1 << j for j in range(word["registers"])] + by_cut = {n: i for i, n in enumerate(word["cuts"])} + checked = 0 + for pos, (t, s, _) in enumerate(word["gates"], 1): + rows[t] ^= rows[s] + if pos in by_cut: + i = by_cut[pos] + expected = expected_rows(spec, i) + d = spec["width"] + visible = list(range(d + 1)) + list(range(2 * d + 1, 2 * d + 2 + i)) + [len(rows) - 1] + require(all(rows[j] == expected[j] for j in visible), "incorrect observable cut") + checked += 1 + require(rows == expected_rows(spec), "incorrect final dirty-state map") + return {"basis_columns": len(rows), "observation_cuts": checked, "final_rows": rows} + + +def invoice(word): + histogram = {} + for _, _, kind in word["gates"]: + histogram[kind] = histogram.get(kind, 0) + 1 + g = len(word["gates"]) + maximum_sum = sum(max(t, s) for t, s, _ in word["gates"]) + # Row-major L-bit blocks, 1-based cells, return to origin after every XOR. + quadratic = 2 * maximum_sum + g + return {"scalar_xors": g, "by_kind": histogram, + "head_steps_L1": 2 * (maximum_sum + g), + "head_steps_polynomial": {"L2": quadratic, "L": g}, + "data_reads_per_L": 2 * g, "data_writes_per_L": g, + "xor_instructions_per_L": g, "dispatches_per_L": g, + "online_tariff_polynomial": {"L2": quadratic, "L": 6 * g}, + "data_cells_per_L": word["registers"], + "instruction_records_per_L": g, + "word_sha256": hashlib.sha256(json.dumps(word, sort_keys=True, separators=(",", ":")).encode()).hexdigest()} diff --git a/research/observable-connector-repair/oracle.py b/research/observable-connector-repair/oracle.py new file mode 100644 index 0000000000..7362cbd9c5 --- /dev/null +++ b/research/observable-connector-repair/oracle.py @@ -0,0 +1,116 @@ +"""Separate edge-by-edge oracle; no model imports. Same AI-assisted author. + +Hanson Sun, with OpenAI Codex assistance. Apache-2.0. +""" +import heapq + + +def parity(reader, mask, d): + return sum(((reader // (2 ** j)) % 2) * ((mask // (2 ** j)) % 2) + for j in range(d)) % 2 + + +def graph_edges(d, conditions, weights, output_prices, state): + stage, bits = state + for j in range(d): + yield (stage, bits ^ (2 ** j)), weights[j] + if stage < len(conditions): + a, b = conditions[stage] + defect = b ^ parity(a, bits, d) + if not defect or output_prices is not None: + yield (stage + 1, bits), defect * output_prices[stage] if defect else 0 + + +def shortest(d, conditions, weights, output_prices=None): + """Dijkstra over individual paid XOR edges and free/paid observation edges.""" + distances = {(0, 0): 0} + heap = [(0, (0, 0))] + while heap: + price, state = heapq.heappop(heap) + if distances[state] != price: + continue + for target, charge in graph_edges(d, conditions, weights, output_prices, state): + trial = price + charge + if target not in distances or trial < distances[target]: + distances[target] = trial + heapq.heappush(heap, (trial, target)) + goal = (len(conditions), 0) + if goal not in distances: + raise ValueError("unreachable observation endpoint") + dual = [[distances.get((t, k)) for k in range(2 ** d)] + for t in range(len(conditions) + 1)] + return distances[goal], dual + + +def validate_dual(d, conditions, weights, output_prices, dual, expected): + """Check a lower bound through local potential inequalities, without search.""" + if len(dual) != len(conditions) + 1 or any(len(row) != 2 ** d for row in dual): + raise ValueError("invalid dual shape") + if any(type(value) is not int for row in dual for value in row): + raise ValueError("invalid dual values") + if dual[0][0] != 0 or dual[-1][0] != expected: + raise ValueError("dual endpoint mismatch") + edges = 0 + for t, row in enumerate(dual): + for k, value in enumerate(row): + for (nt, nk), cost in graph_edges(d, conditions, weights, output_prices, (t, k)): + if dual[nt][nk] > value + cost: + raise ValueError("invalid lower-bound edge") + edges += 1 + return edges + + +def run_array(spec, word, initial, L=1, backwards=False, check_cuts=True): + """Literal Boolean array interpreter, independent of packed symbolic rows.""" + d = spec["width"] + a = [row[:] for row in initial] + if len(a) != word["registers"] or any(len(row) != L for row in a): + raise ValueError("array shape") + cut_lookup = {n: i for i, n in enumerate(word["cuts"])} + gates = list(reversed(word["gates"])) if backwards else word["gates"] + observed = 0 + for pos, (target, source, _) in enumerate(gates, 1): + for j in range(L): + a[target][j] = (a[target][j] + a[source][j]) % 2 + if check_cuts and not backwards and pos in cut_lookup: + t = cut_lookup[pos] + expected = direct(spec, initial, L, upto=t + 1) + visible = list(range(d + 1)) + list(range(2 * d + 1, 2 * d + 2 + t)) + [len(a) - 1] + if any(a[i] != expected[i] for i in visible): + raise ValueError("literal observation mismatch") + observed += 1 + return a, observed + + +def direct(spec, initial, L=1, upto=None): + """Evaluate the requested map by nested matrix sums, without any repair word.""" + d = spec["width"] + a = [row[:] for row in initial] + upto = len(spec["readers"]) if upto is None else upto + for t in range(upto): + row = spec["steps"][t] + a[row] = [(x + y) % 2 for x, y in zip(a[row], a[d])] + bx = [[sum(((spec["B"][j] // 2 ** k) % 2) * a[k][p] for k in range(d)) % 2 + for p in range(L)] for j in range(d)] + out = 2 * d + 1 + t + for p in range(L): + a[out][p] = (a[out][p] + sum(((spec["readers"][t] // 2 ** j) % 2) * bx[j][p] + for j in range(d))) % 2 + return a + + +def literal_invoice(word, L): + moves = 0 + accesses = 0 + instructions = 0 + for target, source, _ in word["gates"]: + for j in range(L): + source_cell = source * L + j + 1 + target_cell = target * L + j + 1 + cursor = 0 + for cell in (source_cell, target_cell, 0): + moves += abs(cursor - cell) + cursor = cell + accesses += 3 # two reads and one write + instructions += 2 # XOR and dispatch + return {"head_steps": moves, "online_tariff": moves + accesses + instructions} diff --git a/research/observable-connector-repair/references/PR1203-README.md b/research/observable-connector-repair/references/PR1203-README.md new file mode 100644 index 0000000000..b884fdff76 --- /dev/null +++ b/research/observable-connector-repair/references/PR1203-README.md @@ -0,0 +1,315 @@ +# Reader-compatible restoration deferral + +**Research note / exact recursive interface; no new kappa.** Nonzero reads of +borrowed workspace need not prevent deferring its restoration. The precise +condition is that each read annihilates the accumulated drift. A fully expanded +example, including cancellation of incoming dirt and both source calls, reduces +**210 to 150 two-address ADD instructions**, and **5,864 to 4,504 data-tape word +transitions**, for the same fixed borrowing interface. Preparation and control +costs are separately and explicitly charged below; these counts are not a +runtime benchmark or an optimal circuit claim. + +This refines Navinor's [PR1155](https://github.com/CrocSwap/integer-mult-bounds/pull/1155) +at `9821c6e9388f3fc097e94b72be9fa7b41a849527`. Its retained +[original note](sources/PR1155-README.md) states that read-freedom is necessary +and sufficient and uses one failing reader as evidence of necessity. That +counterexample shows that **some** readers fail, not that **every** reader fails. +The construction here has compatible readers after actual nonidentity drift. +PR1155's shared-final-target observability also admits a weaker cancellation +condition, distinguished below. No assertion is made about its executable +fixtures beyond the statement inspected in that pinned note. + +Concurrent [PR1199](https://github.com/CrocSwap/integer-mult-bounds/pull/1199) +by Sagar Thakrar at `85ac2880ea5bda44f28632b71ffa2b4e35ec6b7d` independently +corrects the same necessity claim, supplies a diagonal-sign checkpoint planner, +and states the general summed-defect identity. **No priority is claimed for +that correction or the prefix-defect identity.** This package adds separate +noncommuting-permutation evidence, distinct-output admission, an explicitly +dirt-independent shared-B wrapper, and a separately implemented symbolic +scalar/tape invoice. It does not reproduce or supersede PR1199's cut planner. +The exact concurrent source was inspected at the final submission check; +its results are credited, not silently treated as our discovery. + +## Reproduce + +Python 3.10+, standard library only, from the repository root: + +```sh +python3 -I -O -B research/invariant-reader-restoration/verify.py +``` + +Expected: + +```text +PASS_INVARIANT_READER_RESTORATION cases=5832 wrapped_adds=210->150 no_new_kappa +``` + +The command verifies retained source hashes, recomputes every certificate field, +and compares against [CERTIFICATE.json](CERTIFICATE.json). Required checks use +explicit exceptions and remain active with `-O`. The companion command +`python3 -I -O -B research/invariant-reader-restoration/test_package.py` checks +relocation, deterministic export and deliberate on-disk corruptions. Neither +command regenerates selected or upstream artifacts. `--write PATH` is explicitly +an authoring/export mode, not acceptance against the committed certificate. + +## Exact typed interface and proof + +Work over the rationals, with all arithmetic exact. Let `z` be arbitrary borrowed +workspace, `y_i` distinct arbitrary output accumulators, and `G_i` fixed invertible +linear workspace maps. A child first performs `y_i += H_i z`, then `z <- G_i z`. +All coefficients are immutable; no output aliases workspace or another output. +Readers are target-independent, and private scratch and tape positions used by +complete child operations are restored. The code specializes `G_i` to permutations +and `H_i` to rows with coefficients in `{-1,0,1}`. + +The eager contract follows each child with `G_i^-1`. The deferred contract +omits these restorations and applies `(G_r ... G_1)^-1` once at batch exit. Put +`P_0 = I`, `P_j = G_j ... G_1`. Then: + +- Eager output `i` is `y_i^0 + H_i z_0`. +- Deferred output `i` is `y_i^0 + H_i P_(i-1) z_0`. +- Both final workspaces are `z_0`. + +Consequently, equality for **all incoming dirty states** is equivalent to + +```text +H_i (P_(i-1) - I) = 0 for every i. (1) +``` + +Sufficiency follows by subtraction. For necessity, a nonzero defect matrix has +a nonzero column; the corresponding standard basis workspace is a counterexample. +This is an all-size algebraic proof, not an inference from the finite census. +For permutation prefixes, each reader row must be constant on each cycle of +that prefix. It need not be invariant under every individual `G_j`, and it need +not vanish. The condition concerns the actual chronological prefix. + +**One shared output at batch exit.** If all readers update the same accumulator, +only their summed defect must vanish: + +```text +sum_i H_i (P_(i-1) - I) = 0. (2) +``` + +For `G_1 = swap(0,1)`, `G_2 = G_3 = I`, and readers `0,e_0,e_1`, the individual +defects are `0,(-1,1),(1,-1)`. Condition (2) holds while (1) fails. If the shared +output is observable after every child, equality of consecutive partial sums +again forces each individual defect to vanish. Thus observability is a material +part of the contract; no general "one reader breaks it" theorem follows. + +## Returning arbitrary dirty workspace without exposing it + +Reading preserved input state is not by itself a catalytic scratch contract: +outputs must be independent of borrowed dirt. Supply a read-only source `x` +and a complete, exact additive call `B: z += Bx`, independent of the old target. +Its inverse is `z -= Bx`; both restore private scratch. Execute: + +1. Pre-read `y_i -= H_i z` for every output. +2. Call `B` to obtain `z_1 = z_0 + Bx`. +3. Execute either compatible reader/permutation batch above. +4. Call the complete inverse `B` after batch restoration. + +The output is `y_i^0 - H_i z_0 + H_i(z_0+Bx) = y_i^0 + H_i Bx`, and final +workspace is exactly `z_0`. Source `x` is unchanged. All `x,z,y_i` ports are +pairwise disjoint and excluded from private child scratch. The routing temporary +and source accumulator are **two admitted clean scalars**, separately charged; +no clean workspace row is assumed. Readers of other live state, nonlinear or +rounded B calls, data-dependent permutations and intermediate observation during +the pre-read/load sandwich are outside this contract. + +The same proof holds for rows of any common length `L`, with `G_i` replaced by +`G_i tensor I_L` and the corresponding block readers. It does not construct a +selected supplier or discharge the repository's physical recursive interfaces. + +## Noncommuting eight-coordinate fixture + +Use old-coordinate-to-new-coordinate cycle notation: + +```text +G_1 = (01)(23)(45)(67) +G_2 = (0123)(4567) +G_3 = (04)(15)(26)(37) +H_1 = e_0, H_2 = e_0 + e_1, H_3 = e_0 + e_2. +``` + +The first two maps do not commute. `P_2 = (02)(46)` and +`P_3 = (06)(15)(24)(37)`. Each reader satisfies (1); the latter two read +workspace that has actually drifted. Both have nonzero dependence on the +original workspace. The catalytic wrapper uses +`(Bx)_j = x_j + x_((j+1) mod 8)`; B need not be invertible or commute with G. +The certificate spells out gather permutations `new[j] = old[p[j]]`, avoiding +ambiguity between cycle and index-array conventions. + +The matrix checker uses dense exact products. The separately implemented +[backend](backend.py) instead composes index arrays, decomposes cycles, emits +scalar instructions and literally loads/unloads its clean accumulator. On every +basis of the 19 arbitrary source/workspace/output coordinates (plus a mixed +case), both complete wrapper programs implement `y_i += H_i Bx`, preserve all +source/workspace coordinates, restore the temporary, and have a working literal +reverse-inverse. This is finite evidence for the actual emitted fixture; the +universal identity is proved above. + +## Complete invoice and recurrence + +A two-address ADD `d += sign*s`, with distinct ports, expands as +`A += memory[s]; memory[d] += sign*A; A -= memory[s]`. Its source is unchanged, +so A returns to zero. It pays two source reads, one target read, one target +write and three scalar additions/subtractions. The data head traverses +`0 -> s -> d -> s -> 0`, paying `2*s + 2*abs(d-s)` word transitions. The scalar +A is separately located in a fixed arithmetic workspace; arithmetic/read/write +macro costs include their internal access and scratch restoration. + +Each permutation cycle is implemented by swaps. A swap uses an initially zero +scalar T and these **six**, fully charged, distinct-port shears: + +```text +T += a; a -= T; a += b; b -= a; b += T; T -= b. +``` + +It returns `(a,b,T)` as `(b,a,0)`. A k-cycle uses `k-1` swaps. Here the forwards +use 14 swaps, eager inverses another 14, and the composed inverse four. There +is no free array copy, hidden permutation, erased scratch or unpaid inverse. +The full wrapper has two 16-ADD B calls and ten reader ADDs. + +| Complete wrapper charge | Eager | Deferred | +|---|---:|---:| +| Forward-permutation ADDs | 84 | 84 | +| Restoration ADDs | 84 | 24 | +| Both B calls | 32 | 32 | +| Pre-reads and batch reads | 10 | 10 | +| **Two-address ADD instructions** | **210** | **150** | +| Scalar additions/subtractions | 630 | 450 | +| Source reads | 420 | 300 | +| Target reads / target writes | 210 / 210 | 150 / 150 | +| Data-tape word transitions | 5,864 | 4,504 | + +Workspace addresses are 0..7, outputs 8..10, T is 11, and immutable source +addresses are 12..19. A is outside that data tape. The instruction stream has +one fixed-width `(opcode,d,s,sign)` record per ADD; both programs use the same +address width. Each event reads one record and returns the data head. Thus +instruction reads, control dispatch and address decoding must be paid 210 and +150 times, respectively, at the same declared per-record cost. No instruction +or coefficient-access cost is claimed to be zero. + +For integer scalar inputs of magnitude less than `2^p`, every workspace value during the +wrapper has magnitude at most `3*2^p`; during swaps it is either one of these +values or zero. An intermediate output is bounded by `9*2^p`, and A loads only +workspace, source or T. Signed width `b = p+5` therefore suffices without +rounding. Allocation includes 20 data words and A, plus instruction storage, +address/control counters and the scratch required by the chosen exact scalar +arithmetic backend. This bound is about this fixture, not a floating-point +precision contract or a fixed-tape multiplication implementation. + +For event-count `K`, scalar-add count `S`, word travel `J`, and word width b, +a complete parametrized online bill is + +```text +W(program;b) = S*c_add(b) + 3K*c_read(b) + K*c_write(b) + + b*J*c_move + K*c_dispatch(b, address_width). +``` + +Here read/write costs include intra-word scans and return to a word boundary; +`c_add` includes arithmetic scratch restoration and scalar register updates; +`c_dispatch` includes instruction-record access, decoding and counter work. +No backend numerical timings are inferred. Online saving for the fixture is +`180*c_add + 180*c_read + 60*c_write + 1360*b*c_move + 60*c_dispatch`. +Startup allocation/zeroing of the two clean scalars is paid in admission `I`. + +For a general node, let `C_B^+/-` be complete recursive source-call costs, +`R_H^-/+` complete reader costs, `Q(G)` complete routing costs, `P_S` program and +coefficient preparation, and `D_S` dispatch/control not already included. With +no double counting of these terms, the recurrences are + +```text +T_E = I + P_E + C_B^+ + C_B^- + R_H^- + R_H^+ + + sum_i [Q(G_i) + Q(G_i^-1)] + D_E, +T_D = I + P_D + C_B^+ + C_B^- + R_H^- + R_H^+ + + sum_i Q(G_i) + Q(P_r^-1) + D_D. +``` + +If `C_B^sign(L) = sum_j C_child(j,sign)(L_j) + A_B^sign(L)`, substitute the +**entire** recurrence in both occurrences. All children, coefficient and source +access, frame conversions, copies, private restoration and tape return belong +in those terms. No child is eliminated by this argument. A caller requiring a +new frame or external layout conversion must add it; this fixture stays in one +fixed coordinate layout. Recursive children may not borrow the live rows. + +Preparation is not free: composing explicit n-entry permutation descriptors +uses `r*n` index lookups and stores (24 of each here), plus validation, inverse +construction, cycle extraction and instruction emission. General descriptors +are not composable in merely `O(r)` work. Budget `O(r*n*log(n+1))` bit work for +index manipulation, in addition to validation/coefficient preparation and +writing the full instruction stream. The implementation computes the product +in both modes to return admission metadata; a lean eager implementation could +omit those 24 updates. We do not use this avoidable baseline work as a saving. +For `M` invocations of a prepared fixed program, pay `I + P_S + M*W_S`. +For a single call, the extra preparation must be smaller than the displayed +online saving before claiming a total speedup. Neither M nor that tradeoff is +silently assumed. The full parametrized bill makes this boundary explicit. + +Directly computing `H_i Bx` can be cheaper than either wrapper in this toy +fixture. This is a legal replacement and correction within a fixed borrowing +interface, **not** a minimum over arbitrary circuits, a claim that a new +supplier is profitable, or a way to increase kappa from operation counts. + +## Coverage, failures and limits + +A further [separate symbolic checker](independent_check.py), included in the +one-command replay, does not import the matrix criterion or backend execution +engine. It checks all 873 permutations of widths 1 through 6 against the emitted +forward words, then reconstructs both full wrapper maps using integer coefficient +vectors. It independently derives every invoice field and bounds all intermediate +coefficient L1 norms: workspace/T/A at most 3, outputs at most 5, source at most 1. +The conservative integer-width allowance above is therefore sufficient. Its +symbolic-map digest and exact bounds are retained in the certificate. + +The finite census exhausts all `2^3 * 9^3 = 5,832` three-child instances with +2-coordinate permutations and reader coefficients in `{-1,0,1}`. Independent +literal state replay on both workspace basis vectors agrees with the matrix +criteria in every case. There are 2,592 compatible distinct-output instances, +2,772 compatible shared-final-output instances, and 180 cancellation-only cases. +This is completed finite coverage, not a new impossibility theorem. + +Controls include an incompatible nonzero reader with an explicit basis witness; +a zero-workspace input that hides that defect; omitted final restoration; +incorrect inverse order on a noncommuting example; an omitted reader; missing +catalytic pre-reads that expose dirt; an omitted inverse B that fails restoration; +and invalid/aliased instruction ports. Certificate/package mutations test +rejection of an unpaid operation, source corruption and receipt corruption. + +The exact general lemma is proved in prose. Neither the finite replay nor the +second Codex agent's algebraic review is independent human review or a formal +proof in a proof assistant. No selected cold replay was run: this isolated note +changes no supplier, selected certificate, shared generator, upstream source, +review ledger or frozen predecessor evidence. All-size compiler, common-label / +mutable-source realization, hosting, precision/tape and analytic transfer +obligations of the selected multiplication result remain open as recorded there. + +## Provenance and credit + +Base: `1b59b624d21924f8e3537cdc1ac52d3be6eda2fe`. Assignment seed **50**, generated +from OS randomness, selects recursive interfaces and the three-child/eight-entry +fixture. There is no random search. [CLAIM.md](CLAIM.md) records the three narrow +candidates and overlap decision; [SOURCE-PINS.json](SOURCE-PINS.json) identifies +exact context files and retained sources. The selected result at that base is +`836330098538459/500000000000000000`, from #1094 on #1087; complex binds in that +assembly. We do not reassign its binding supplier or modify its frontier. + +Credit Navinor / Aaron Wang with opencode assistance for PR1155's deferral +proposal and motivating reader question. Credit Sagar Thakrar's concurrent #1199 for the same applicability correction +and its distinct checkpoint planner, and his #1012 and +avirazza's #974 for the distinct hosted-assembly cost question; their reported +mass-neutrality is not contradicted by this abstract-interface correction. +Ross Richardson (CubeJerry)'s #889 supplies the shared-B, multiple-output dirty +fanout/echo construction; the pre-read/load/unload wrapper here is an instance +of that established mechanism, not a new batching claim. The additional result +is admitting nonzero readers through intervening workspace permutations using +the exact prefix condition, independently corroborating PR1199. Gareth Davidson's #1057 and woklerx's #1164 concern dirty-pool allocation and +higher-arity echoes, not the reader-defect criterion here. Ross Richardson's +universal-connector work and the repository's preceding dirty-restoration work +retain their own scopes and attribution. No priority claim is made for elementary +linear invariance or echo cancellation. + +Prepared for **mightyOil (Philipp)** with substantial **OpenAI Codex assistance** +in mathematics, implementation, verification and writing, including three scoped +Codex subagents. New files are Apache-2.0; retained source credit is in +[NOTICE.md](NOTICE.md). diff --git a/research/observable-connector-repair/references/PR1246-README.md b/research/observable-connector-repair/references/PR1246-README.md new file mode 100644 index 0000000000..e9263fffce --- /dev/null +++ b/research/observable-connector-repair/references/PR1246-README.md @@ -0,0 +1,288 @@ +# Pay for nonzero reader defects instead of restoring every child + +**Recursive-interface construction and partition planner; no new kappa.** +For the fixed five-child example below, a complete dirty-workspace echo costs +**244 scalar instructions instead of 380**. Readers do not cancel their drift +errors. The parent restores the workspace and pays for an explicit output +correction. Both source-copy passes, both directions of every child, all +private scratch and the correction are included. + +The contribution extends the zero-defect cut rule in Sagar Thakrar's +[PR1199](https://github.com/CrocSwap/integer-mult-bounds/pull/1199) and the +observer criterion independently developed by mightyOil in +[PR1203](https://github.com/CrocSwap/integer-mult-bounds/pull/1203) and Adam Gall in +[PR1205](https://github.com/CrocSwap/integer-mult-bounds/pull/1205). Their defect +identity is reused and credited, not claimed as new. The added operation is a +**paid output shear with a nonzero defect**, together with a minimum-cost +partition over a specified implementation of that operation. The selected +example uses a noncentral cyclic workspace permutation, outside the fixed +workspace-negation alphabet of Thakrar's +[PR1227](https://github.com/CrocSwap/integer-mult-bounds/pull/1227). + +This is an interface result with indivisible children. If a compiler may open +these particular leaves, their final map is just a five-ADD signed dot product; +direct evaluation is much cheaper than either echo. No supported supplier +requiring this indivisible boundary has been identified. The result supplies +a checked option for such a boundary, not an optimized matrix algorithm, +physical supplier, runtime speedup or change to the selected exponent. + +## Exact terminal repair + +Let `D` be data and `W` arbitrary dirty workspace. Fixed linear children satisfy + +``` +C_i(D,W) = (D + B_i W, G_i W), G_i invertible. +``` + +Each child's private scratch is arbitrary and restored. The matrices do not +depend on intermediate data, and there is no data-to-workspace feedback. +Eager execution follows every child by its workspace inverse. Its desired +return map is `(D + sum_i B_i W, W)`. + +Write `P_0=I`, `P_i=G_i ... G_1` and + +``` +E = sum_i B_i (P_(i-1) - I). +``` + +The cited predecessor criterion admits uncorrected deferral exactly when +`E=0`. For arbitrary `E`, the following enlarged boundary is exact: + +1. Execute each unchanged child once in its fixed order. +2. Apply `P_k^-1` to workspace. +3. Apply `D <- D - E W`, now using restored entry-coordinate workspace. + +**Proof.** Before child `i`, deferred workspace is `P_(i-1) W_entry`. The raw +data return is therefore `D_entry + (sum_i B_i + E) W_entry`. Step 2 returns +`W_entry`; step 3 subtracts exactly the unwanted term. Every private scratch +port has its original value. This proves the identity for arbitrary dirty +inputs and dimensions over any field with these exact operations. It does +not infer a universal theorem from finite samples. + +Restoration must precede the stated correction. Correcting against `P_k W` +instead would require a different matrix, `E P_k^-1`. A noncommuting example +in the controls detects this order error. An intermediate observer or adaptive +child cannot use the uncorrected output as if it were canonical. Such a point +must be a required cut, with its entire restoration and correction paid first. + +## Declared operation alphabet and partition optimum + +The executable specialization has one output coordinate, an integer row +`B_i`, and a signed permutation `G_i` on `N` workspace coordinates. There are +only two scalar instructions: `target += sign * source` for distinct ports, +where `sign` is `+1` or `-1`, and unary `NEG`. Registers are addressed exactly; +no clean scratch or implicit source copy is available. + +Canonical signed-permutation synthesis first permutes absolute indices using +`N-cycles` swaps, then negates negative coordinates. A swap uses three ADDs +and one NEG, with no temporary. Inversion has the same number of cycles and +negative coordinates. The correction repeats a unit signed ADD `|E_j|` times +for each coefficient. A coefficient of magnitude four costs four ADDs, not +one. These are implementations with a known price, not globally shortest +linear circuits. + +For a segment `[a,b)`, its boundary cost is thus + +``` +b(a,b) = 4 (N - cycles(abs(P))) + negative_signs(P) + sum_j |E_j|. +``` + +The child words are common to every partition. With `F(0)=0`, the planner uses + +``` +F(t) = min_{0 <= s < t} { F(s) + b(s,t) }, +``` + +excluding intervals that cross a required observation cut. Each chosen segment +returns the same data and workspace as eager execution, so legal segments +compose. Conversely, every partition in this alphabet has a last segment; +removing it gives the displayed recurrence. Induction proves the minimum over +these partitions. This is not an optimum over arbitrary repairs, edits inside +children, interleaved adapters, or a different operation alphabet. The +`zero_defect_only` comparison additionally requires `E=0` on every segment. + +## Seed-selected example and actual eliminated work + +OS assignment seed **58** selected recursive interfaces. It also selects +`N=3+(58 mod 4)=5`, then the following row and signs using the documented +`random.Random(58)` calls in `selected()`: + +``` +R = (1,-1,-1,1,1) +s = (1,-1,-1,1,1), sum s_i = 1 +B_i = s_i R +G(W_0,W_1,W_2,W_3,W_4) = (W_1,W_2,W_3,W_4,W_0). +``` + +Each child reader costs five ADDs. Its workspace cycle costs twelve ADDs and +four NEGs. On the full five-child batch, `P=I` and + +``` +E = (-4,-2,2,4,0). +``` + +The raw batch is wrong: on `W=e_0` it adds `-3` instead of `1`. The completed +one-block repair costs twelve ADDs. The best zero-defect partition is all five +singletons, costing **80 boundary instructions**. The repaired optimum is +the full batch at **12**, as checked against all sixteen partitions. It removes +five workspace inverses, pays twelve correction ADDs, and preserves the child +word. If every interior child boundary must be observed, the optimum returns +to 80; the observation restriction is material. + +The transparent source echo uses a separate arbitrary dirty `W` and preserved +source `X`: + +``` +W += X; B(D,W); W -= X; B^-1(D,W). +``` + +Since the completed batch is `B(D,W)=(D+R W,W)`, the two passes add +`R(W_initial+X)-R W_initial = R X`. The inverse is the literal reversed +instruction word, not a free inverse query. At depth one the complete echo is: + +| Schedule | ADD | NEG | Total | Reads | Writes | Descriptor fields | +|---|---:|---:|---:|---:|---:|---:| +| Eager / zero-defect cuts | 300 | 80 | 380 | 680 | 380 | 1,360 | +| Paid defect repair | 204 | 40 | 244 | 448 | 244 | 896 | + +## Complete recursion, storage and arithmetic scope + +`recursive_word` realizes an actual tree. A leaf adds its signed row to `D` +and applies `G` to its source. An interior reader executes the above echo using +five depth-`h-1` readers with rows `s_i R`, then applies `G` to its own source. +Because the signs sum to one, the reader at every depth returns +`(D+R X,G X)`. Negative rows use the same construction with all reader +coefficients negated. Children restore their private scratch, so siblings and +both echo passes reuse one dirty block per active level. An induction on depth +proves the stated map for all incoming values. + +Let `A_h,Q_h` count ADD and NEG instructions of an interior **reader**, including +all descendants and inverses. For this selected family the complete recurrences +are: + +``` +A_0 = 17, Q_0 = 4 +eager: A_h = 10 A_(h-1) + 142; Q_h = 10 Q_(h-1) + 44 +repair: A_h = 10 A_(h-1) + 46; Q_h = 10 Q_(h-1) + 4. +``` + +The factor ten pays both directions of all five children. The additive terms +include ten source-copy ADDs, both boundary bills, and the final source cycle. +A root echo omits that last cycle: subtract twelve ADDs and four NEGs. Thus +the depth-`h` saving is `136*(10^h-1)/9` instructions. This is tree depth at +fixed port width, not an input-size recurrence or a primitive exponent. + +| Echo depth | Eager total | Repaired total | Data registers | Eager peak | Repaired peak | +|---|---:|---:|---:|---:|---:| +| 1 | 380 | 244 | 11 | 11 | 27 | +| 2 | 4,130 | 2,634 | 16 | 26 | 52 | +| 3 | 41,630 | 26,534 | 21 | 46 | 71 | + +The data allocation is `1+(h+1)N` scalars: output, source and dirty blocks. +For `A` ADDs and `Q` NEGs, every emitted instruction incurs one dispatch, +`2A+Q` data reads, `A+Q` writes and `4A+2Q` instruction-field reads, including +signs and addresses. On the declared addressed machine, arbitrary prices for +arithmetic, these accesses and dispatch can be substituted into those counts. +All recursive calls are expanded into this instruction word; there is no +omitted runtime call dispatcher or coefficient multiplication. No frame change +is a free relabeling: each signed permutation is physically emitted. + +Program preparation is separate work. For fixed `N`, arity and bounded row, +the supplied compiler conservatively takes `O((h+1)P_h)` list work and storage, +where `P_h=A_h+Q_h`, including its repeated planning and word reversal/copying. +The materialized program contains exactly the tabulated descriptor fields. +An end-to-end bill must add this preparation to execution; the counts do not +claim faster compilation or an amortization schedule. No streaming compiler, +tape routing, address-bit cost or physical hosting theorem is supplied. + +The peaks in the table are exact maximum row one-norms over **every instruction +prefix**, on the complete original-input basis, including private dirt. If +initial integers have magnitude at most `M`, every intermediate magnitude is +at most `peak*M`. The repaired schedule therefore needs a larger magnitude +bound in these examples. The verifier uses unbounded integers and rationals; +unit instruction counts alone do not price arbitrary-precision bit arithmetic. +For general emitted words, the elementary bound `2^A M` also suffices. Neither +these bounds nor finite replay establishes a rounded or fixed-tape interface. + +## Reproduce and inspect the evidence + +Python 3.10+; standard library only. From the repository root: + +```sh +python3 -I -O -B research/paid-reader-defect-seed58/test_package.py +``` + +Expected markers: + +``` +PASS_PAID_READER_DEFECT batches=5256 seeded=160 echo=380->244 controls=9 kappa=unchanged +PASS_PAID_READER_PACKAGE relocation=1 corruptions=5 +``` + +`verify.py` checks the retained source-note SHA256 and Git blob identities, +recomputes every field of `CERTIFICATE.json`, and compares the result exactly. +`--emit` prints the recomputed certificate without changing files. Checks use +explicit exceptions and remain active with Python's `-O` flag. + +The independent oracle composes complete state matrices and exhausts all cut +sets. It does not call the production defect routine or planner to derive +its costs. The bounded domain is all 72 single children and 5,184 ordered pairs +at width two: eight signed permutations and nine rows in `{-1,0,1}^2` per +child. This covers **5,256 batches and 10,440 partitions per policy**; 1,116 +batches strictly improve over zero-defect cuts. An additional 160 deterministic +seed-58 cases have widths 3..6, arities 3..7 and row entries -2..2. All contain +noncommuting adjacent drifts; 54 impose interior observation cuts. Their 152 +improvements are finite evidence, not an impossibility or optimality theorem +outside the stated domain. The stopping rule is completion of these domains. + +The recursive census checks 120 generic reader/echo cases on all 1,044 original +basis columns, literal inverses and rational dirty probes, plus nine selected +depth/schedule cases. Every selected partition is also replayed. Nine controls +cover omitted/wrong-sign correction, wrong repair coordinates, missing cleanup, +noncommuting inverse order, omitted source uncopy, a missing second pass, +premature output observation, and nonunit coefficient cost. Eight invalid +inputs are rejected. The package test runs from outside the repository and +rejects five real file corruptions: retained source bytes, source-commit label, +certificate price, omitted correction, and treating a nonunit coefficient as a +single ADD. Source labels are recorded fetch pins; this is not a cryptographic +proof of GitHub publication or a fresh replay of predecessor packages. + +## Provenance, scope and open next questions + +Investigation base: `49b3157d1d89adcef16df8be98445451672be5ba`. The selected +certificate at that base is PR1094, conditional +`kappa=836330098538459/500000000000000000`. Its actual construction, source +manifest and review were followed; `SOURCE-PINS.json` records their hashes as +context. The source-binding baseline check passed. The selected cold replay, +native supplier admission, Linux CI, independent human review and a formal +multiplication proof were not run. Selected compiler/all-size, realization, +hosting, precision/tape, analytic and bit-interface obligations remain open. + +`CLAIM.json` records the three considered tasks, scope, seed and bounded +domain. No pinned sprint issue was present, so the donor's local-claim fallback +was used. Open PR bodies and current discussions were checked; overlap evidence +is bounded and is not proof of novelty. This package changes no predecessor, +selected record, review ledger or upstream source. + +**Open next questions.** Does a supported supplier expose indivisible drifting +readers whose defect is cheap to apply? Trace one concrete child return map and +price its composed inverse and correction before implementing this wrapper. +The blockers are a real child contract, routing and precision; transparent +leaves that can simply be rewritten do not qualify. Within the declared model, +a correction circuit with sharing could reduce the twelve-ADD bill further, +but it would need a different cost function and a newly checked partition +comparison. No global shortest-circuit claim is made here. + +Credit Aaron Wang / Navinor's PR1155 for restoration coalescing; Sagar Thakrar's +PR1199 and PR1227 for the cut and output-sign interfaces; mightyOil's PR1203 and +Adam Gall's PR1205 for independent observer/dirty-reader treatments; and Ross +Richardson / CubeJerry's PR889 for prior common-factor dirty echo work. PR1012 +and PR974 address hosted restoration mass, a different cost model. The selected +Rohan Arun / Jeremy Kothe construction and its contributor lineage are unchanged. +Three predecessor notes are retained byte-for-byte with their notices and exact +heads in `SOURCE-PINS.json`; no predecessor executable is imported. + +Prepared by **Hanson Sun (@bbMisk)** with substantial **OpenAI Codex assistance** +in algebra, implementation, verification and writing. New material is Apache-2.0 +under the retained repository license. This is a written scoped proof with exact +finite implementation evidence, not independent human or proof-assistant review. diff --git a/research/observable-connector-repair/references/PR1439-README.md b/research/observable-connector-repair/references/PR1439-README.md new file mode 100644 index 0000000000..53ef4d0d3e --- /dev/null +++ b/research/observable-connector-repair/references/PR1439-README.md @@ -0,0 +1,133 @@ +# Carry a dirty connector across a paid source mutation + +For two consecutive products A1 B x and A2 B x with the source update +x += C u between them, maintaining the coherent boundary z=z_initial+B x +requires exactly the correction z += B C u. That correction can be cheaper +than restoring and rebuilding B x. The explicit fixed three-bit pilot removes +two complete B calls and reduces **43 to 31 scalar XOR updates**, with the +two-entry correction paid. Sources, output dirt and all connector dirt are +checked exactly; the source update is part of the intended map. + +This is a typed two-call pilot, not an instantiated contracting supplier +recurrence. It changes the immutable-source premise of the inherited carried +connector model. It neither changes the selected frontier nor claims a new +kappa. The mixed-provider catalogue explicitly excludes deferred restoration +that changes its paid call contract; its dual is not contradicted here. + +## Exact contract and proof + +All five length-L F2 rows x,u,z,y1,y2 are distinct and arbitrarily dirty. +A1,A2,B,C are fixed linear maps of compatible dimensions; no commutativity, +invertibility or clean row is assumed. A complete additive call preserves +other rows and restores private scratch and heads. The two boundary types are +closed z=z_initial and open z=z_initial+B x. Outputs may be observed only +after their respective call; an open connector remains reserved and hidden. + +The requested final map is x'=x+C u, u'=u, z'=z, +y1'=y1+A1 B x and y2'=y2+A2 B(x+C u). + +Execute, in order: + + y1 += A1 z; z += B x; y1 += A1 z; + x += C u; z += B C u; + y2 += A2 z; z += B x; y2 += A2 z. + +The first paired readout cancels the old connector dirt and gives A1 B x. +After the source mutation the stored connector is initially z_initial+B x_old. +Adding B C u makes it z_initial+B x_new. The second paired readout then gives +A2 B x_new, and its intervening B call restores the connector. Linearity alone +establishes this for every L and all admissible maps, including singular maps. +The inverse is the literal reversed sequence of these self-inverse shears. + +If the adapter is restricted to a source-independent additive operation +z += D u preserving x,u, the typed boundary is valid for every input iff +D=B C. Subtract the two required expressions for z to prove necessity. Thus +omitting the correction is legal exactly when B C=0. Under the scalar rank-one +update alphabet, an adapter needs at least rank(B C) rank-one updates by +rank subadditivity. This rank bound does not price basis conversions or compute +D u for free; the literal pilot pays its two nonzero scalar entries instead. + +## Completed costs and a useful stopping rule + +Let complete fixed-port costs include arithmetic, source/coefficient access, +scratch restoration, head returns, routing/frames and per-call dispatch. With +all preparation and admission denoted I, the naive two closed echoes cost + + I + 4 c_B + 2 c_A1 + 2 c_A2 + c_C. + +The coherent pair costs + + I' + 2 c_B + 2 c_A1 + 2 c_A2 + c_C + c_BC. + +Use actual orientation/port prices if they differ. I' also includes preparing +the BC adapter and reserving z across the source mutation. The saving is real +only if c_BC+(I'-I)<2 c_B. For k calls and successive source mutations C_t u_t, +the same typed identity gives 2 c_B+2 sum_i c_Ai+sum_t(c_Ct+c_BCt), plus actual +admission, preparation and dispatch. This is a chain cost, not a new all-size +contracting recurrence. No selected owner schedule satisfying it is supplied. + +For the k-call formula, first apply y_i += A_i z_initial to every output while +the connector is closed, then open it once. Complete each output with its second +read when its source version is current, apply the coherence correction after +each source mutation, and close the connector after the final output. Thus +future outputs receive early dirty prewrites. This is permitted by the stated +observation-only contract; the formula does not apply to a stricter contract +forbidding output writes before that output's request interval. The explicit +two-call pilot above needs no early write to the second output. + +In the literal pilot (rows are binary bitmasks), +B=(3,6,7), C=(1,0,0), A1=(2,4,1), A2=(3,2,4), BC=(1,0,1). +B has rank3, C and BC rank1. Every matrix entry1 becomes one source-to-target +XOR; there are no hidden scratch or COPY operations. Baseline cost is +4*7+2*3+2*4+1=43; candidate is 2*7+2*3+2*4+1+2=31. B and C do not commute, +so replacing BC by CB fails. The fixed map constants are compiled into the +instruction list; computing arbitrary runtime BC coefficients is not included +in this fixed-map comparison and must be added for a dynamic backend. + +The data tape has 15 bits, and each XOR is implemented by visiting its source, +visiting its target and returning to origin. Its exact movement is 2 max(s,t), +plus two reads, one write and one XOR. The receipt reports both totals. +Instruction fetch/decode is charged once per scalar gate using equal record +width in both programs; the candidate has 31 versus43 records. One clean scalar +temporary may be initialized once in the common admission and restored per +gate. These are explicit macro counts, not a measured native runtime. + +## Reproduce and scope + +```sh +python -O -B research/mutable-source-persistent-connector/verify.py +python scripts/research_package.py --package research/mutable-source-persistent-connector +``` + +Python3.12+ standard library suffices. The primary engine propagates all10 +arbitrary-input columns for all65,536 quadruples of 2x2 matrices, including +singular, zero and noncommuting maps, in both orientations. An independent +literal scalar engine compares both three-bit words on all32,768 dirty inputs. +Three controls omit the adapter, reverse BC, or omit final B restoration. +[EXPECTED.json](EXPECTED.json) contains exact results; [SOURCES.json](SOURCES.json) +pins predecessor Git blobs and SHA256. No imported executable is trusted for +the identity. Selected cold replay, native compilation and a contracting +multitype supplier realization were not performed or inferred. + +Overlap search of the fully paginated863-PR/112-discussion cached snapshot +found source-mutation mentions but no coherent-connector scope. Offline +freshness and body-only search limitations remain; no absence-of-overlap proof +is claimed. Prior forty rounds, including fixed-source port borrowing and +cleanup read corridors, have different objects and hypotheses. + +## Open next questions + +Find a concrete selected-call boundary whose source mutation has a cheap BC +adapter. First extract both complete entry/exit contracts and compare the full +cost above, including reserve width and frame admissions. The blocker is a +verified hosted supplier instantiation, not the scalar identity; without one, +no contracting recurrence or exponent improvement follows. + +## Credit + +Prepared by woklerx with substantial OpenAI Codex assistance; Apache-2.0. +Ross Richardson's universal connector/PR934 work supplies the dirty-readout +contract and its predecessor attribution; Ali Romman's heterogeneous owner +assembly identifies deferred restoration as outside its frozen catalogue. +All selected supplier and dirty-commutator lineage remains credited. No +independent human peer review or full multiplication theorem is asserted. diff --git a/research/observable-connector-repair/test_package.py b/research/observable-connector-repair/test_package.py new file mode 100644 index 0000000000..eab5de735f --- /dev/null +++ b/research/observable-connector-repair/test_package.py @@ -0,0 +1,85 @@ +#!/usr/bin/env python3 +"""Packaging and corruption controls. Hanson Sun with OpenAI Codex. Apache-2.0.""" +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +class PackageTests(unittest.TestCase): + def setUp(self): + self.temp = tempfile.TemporaryDirectory(prefix='observable-connector-') + self.root = Path(self.temp.name) + self.pkg = self.root / 'research' / HERE.name + shutil.copytree(HERE, self.pkg, ignore=shutil.ignore_patterns('__pycache__')) + sources = json.loads((HERE / 'SOURCES.json').read_text()) + for row in sources['files']: + if row['usage'] == 'input': + dst = self.root / row['path'] + dst.parent.mkdir(parents=True, exist_ok=True) + shutil.copy2(ROOT / row['path'], dst) + + def tearDown(self): + for path in self.root.rglob('*'): + if path.is_dir(): + path.chmod(0o755) + else: + path.chmod(0o644) + self.temp.cleanup() + + def run_verifier(self, *args): + return subprocess.run([sys.executable, '-I', '-O', '-B', str(self.pkg / 'verify.py'), *args], + cwd=self.root, text=True, capture_output=True, timeout=40) + + def test_read_only_relocation_and_exact_export(self): + for path in self.root.rglob('*'): + path.chmod(0o555 if path.is_dir() else 0o444) + result = self.run_verifier() + self.assertEqual(result.returncode, 0, result.stdout + result.stderr) + self.assertIn('PASS_OBSERVABLE_CONNECTOR', result.stdout) + export = self.root / 'recomputed.json' + result = self.run_verifier('--write', str(export)) + self.assertEqual(result.returncode, 0, result.stdout + result.stderr) + self.assertEqual(export.read_bytes(), (self.pkg / 'CERTIFICATE.json').read_bytes()) + duplicate = self.run_verifier('--write', str(export)) + self.assertNotEqual(duplicate.returncode, 0) + self.assertIn('File exists', duplicate.stderr) + + def test_false_optimum_certificate_rejected(self): + path = self.pkg / 'CERTIFICATE.json' + doc = json.loads(path.read_text()) + doc['optimality']['mixed']['minimum'] = 2 + path.write_text(json.dumps(doc)) + result = self.run_verifier() + self.assertNotEqual(result.returncode, 0) + self.assertIn('certificate mismatch', result.stderr) + + def test_retained_source_corruption_rejected(self): + path = self.pkg / 'references' / 'PR1439-README.md' + path.write_text(path.read_text() + '\nmutated source\n') + result = self.run_verifier() + self.assertNotEqual(result.returncode, 0) + self.assertIn('predecessor SHA256 mismatch', result.stderr) + + def test_live_source_corruption_rejected(self): + path = self.root / 'research/universal-connector-boundary/README.md' + path.write_text(path.read_text() + '\nmutated source\n') + result = self.run_verifier() + self.assertNotEqual(result.returncode, 0) + self.assertIn('live source drift', result.stderr) + + def test_missing_certificate_rejected(self): + (self.pkg / 'CERTIFICATE.json').unlink() + result = self.run_verifier() + self.assertNotEqual(result.returncode, 0) + self.assertIn('CERTIFICATE.json', result.stderr) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/observable-connector-repair/verify.py b/research/observable-connector-repair/verify.py new file mode 100644 index 0000000000..527895b7ca --- /dev/null +++ b/research/observable-connector-repair/verify.py @@ -0,0 +1,224 @@ +#!/usr/bin/env python3 +"""Recompute the scoped certificate and failure controls. Apache-2.0. + +Hanson Sun, with substantial OpenAI Codex assistance. Standard library only. +""" +import argparse +import copy +import hashlib +import itertools +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import model +import oracle + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def rejected(fn): + try: + fn() + except ValueError: + return True + raise ValueError("negative control was accepted") + + +def source_pins(): + refs = json.loads((HERE / "PREDECESSORS.json").read_text()) + for r in refs["references"]: + b = (HERE / r["retained_path"]).read_bytes() + require(hashlib.sha256(b).hexdigest() == r["sha256"], "predecessor SHA256 mismatch") + require(hashlib.sha1(b"blob " + str(len(b)).encode() + b"\0" + b).hexdigest() == r["git_blob"], + "predecessor Git blob mismatch") + sources = json.loads((HERE / "SOURCES.json").read_text()) + for row in sources["files"]: + if row["usage"] == "input": + raw = (HERE.parents[1] / row["path"]).read_bytes() + require(hashlib.sha256(raw).hexdigest() == row["sha256"], "live source drift") + return {"base": sources["base_commit"], "predecessor_notes": len(refs["references"])} + + +def exhaustive_small(): + """All six scalar demands per stage, length zero through four, two tariffs.""" + options = list(itertools.product(range(1, 4), (0, 1))) + cases = 0 + digest = hashlib.sha256() + for n in range(5): + for conditions in itertools.product(options, repeat=n): + for weights in ([1, 1], [2, 5]): + for output_prices in (None, [3 + i % 2 for i in range(n)]): + plan = model.solve(2, conditions, weights, output_prices) + cost, dual = oracle.shortest(2, conditions, weights, output_prices) + require(plan["cost"] == cost, "small-instance oracle disagreement") + oracle.validate_dual(2, conditions, weights, output_prices, dual, cost) + if n <= 3: + candidates = [] + for path in itertools.product(range(4), repeat=n): + defects = [b ^ oracle.parity(a, k, 2) for (a, b), k in zip(conditions, path)] + if output_prices is None and any(defects): + continue + nodes = (0,) + path + (0,) + bill = sum(sum(weights[j] for j in range(2) if (p ^ q) & (2 ** j)) + for p, q in zip(nodes, nodes[1:])) + if output_prices is not None: + bill += sum(p * w for p, w in zip(defects, output_prices)) + candidates.append(bill) + require(min(candidates) == cost, "enumerated mask routes disagree") + digest.update(json.dumps([conditions, weights, output_prices, cost], separators=(",", ":")).encode() + b"\n") + cases += 1 + return {"demand_sequences": sum(6 ** n for n in range(5)), "tariff_mode_cases": cases, + "maximum_stages": 4, "width": 2, "result_sha256": digest.hexdigest()} + + +def array_evidence(spec, words): + cases = columns = cuts = 0 + for word in words.values(): + count = word["registers"] + for L in (1, 2, 3): + for j in range(count * L): + state = [[0] * L for _ in range(count)] + state[j // L][j % L] = 1 + expected = oracle.direct(spec, state, L) + result, observed = oracle.run_array(spec, word, state, L) + require(result == expected, "literal basis mismatch") + restored, _ = oracle.run_array(spec, word, result, L, backwards=True) + require(restored == state, "literal inverse mismatch") + columns += 1 + cuts += observed + cases += 1 + actual = oracle.literal_invoice(word, L) + bill = model.invoice(word) + for field, coefficients in (("head_steps", bill["head_steps_polynomial"]), + ("online_tariff", bill["online_tariff_polynomial"])): + require(actual[field] == coefficients["L2"] * L * L + coefficients["L"] * L, + "literal movement/access invoice disagreement") + tiny = {"width": 2, "B": [3, 2], "readers": [1, 3], "steps": [0, 0]} + dc = [(x["reader"], x["demand"]) for x in model.demands(tiny)] + plan = model.solve(2, dc, [1, 1], [1, 1]) + word = model.emit(tiny, "planned", plan) + for mask in range(2 ** word["registers"]): + state = [[(mask >> j) & 1] for j in range(word["registers"])] + out, observed = oracle.run_array(tiny, word, state) + require(out == oracle.direct(tiny, state), "small exhaustive dirty mismatch") + back, _ = oracle.run_array(tiny, word, out, backwards=True) + require(back == state, "small exhaustive inverse mismatch") + cuts += observed + cases += 1 + return {"pilot_basis_columns_forward_and_inverse": columns, + "literal_cases": cases, "tiny_all_dirty_inputs": 2 ** word["registers"], + "observation_checks": cuts, "block_lengths": [1, 2, 3]} + + +def controls(spec, plans, words, conditions, dual): + passed = [] + + def control(name, fn): + rejected(fn) + passed.append(name) + + def omitted(kind, last=False): + word = copy.deepcopy(words["mixed"]) + choices = [i for i, g in enumerate(word["gates"]) if g[2] == kind] + del word["gates"][choices[-1] if last else choices[0]] + word["cuts"] = [] + model.check_word(spec, word) + + control("omit_output_correction", lambda: omitted("output_repair")) + control("omit_terminal_connector_correction", lambda: omitted("connector_repair", True)) + control("omit_final_B_entry", lambda: omitted("B", True)) + control("omit_reader_prewrite", lambda: omitted("reader")) + control("omit_source_restoration_entry", lambda: omitted("source", True)) + bad = copy.deepcopy(plans["mixed"]) + bad["path"][0] = 1 + control("wrong_observable_coset", lambda: model.emit(spec, "planned", bad)) + bad_dual = copy.deepcopy(dual) + bad_dual[1][0] += 100 + control("corrupt_lower_bound_potential", lambda: oracle.validate_dual(4, conditions, [1] * 4, [1] * 8, bad_dual, 3)) + control("negative_gate_price", lambda: model.solve(4, conditions, [-1, 1, 1, 1])) + control("out_of_range_reader", lambda: model.solve(2, [(4, 0)], [1, 1])) + control("infeasible_zero_reader", lambda: model.solve(2, [(0, 1)], [1, 1])) + bad_spec = copy.deepcopy(spec) + bad_spec["steps"] = bad_spec["steps"][:-1] + bad_spec["readers"] = bad_spec["readers"][:-1] + control("unrestored_source_tour", lambda: model.demands(bad_spec)) + word = words["mixed"] + state = [1 << j for j in range(word["registers"])] + for t, s, kind in word["gates"]: + if kind != "reader": + break + state[t] ^= state[s] + future = 2 * spec["width"] + 1 + len(spec["readers"]) - 1 + require(state[future] != 1 << future, "early-output observation guard not witnessed") + passed.append("early_future_output_is_not_canonical") + require(plans["strict"]["path"][0] != model.demands(spec)[0]["coherent_mask"], "strong-boundary distinction lost") + require(model.invoice(words["direct"])["scalar_xors"] < model.invoice(words["mixed"])["scalar_xors"], + "alphabet restriction control lost") + passed.extend(["strong_coherence_is_not_asserted", "direct_product_fusion_is_cheaper"]) + return passed + + +def build(): + pins = source_pins() + spec = model.selected() + require(spec["B"] == [8, 13, 6, 2] and spec["readers"] == [9, 6, 4, 11, 15, 2, 3, 14] + and spec["steps"] == [3, 2, 1, 0, 3, 2, 1, 0], "seed fixture drift") + ds = model.demands(spec) + conditions = [(x["reader"], x["demand"]) for x in ds] + plans, optimality = {}, {} + for name, weights, out in ( + ("strict", [1] * 4, None), + ("mixed", [1] * 4, [1] * 8), + ("strict_quadratic", [11, 13, 15, 17], None), + ("mixed_quadratic", [11, 13, 15, 17], [19 + 2 * i for i in range(8)]), + ("mixed_tariff_L1", [17, 19, 21, 23], [25 + 2 * i for i in range(8)]), + ): + plan = model.solve(4, conditions, weights, out) + price, dual = oracle.shortest(4, conditions, weights, out) + require(plan["cost"] == price, "pilot oracle disagreement") + edges = oracle.validate_dual(4, conditions, weights, out, dual, price) + plans[name] = plan + optimality[name] = {"potential": dual, "checked_edges": edges, "minimum": price} + require(plans["strict"]["path"] == plans["strict_quadratic"]["path"], "strict all-L common witness") + require(plans["mixed"]["path"] == plans["mixed_quadratic"]["path"] + == plans["mixed_tariff_L1"]["path"], "mixed all-L common witness") + require(plans["strict"]["cost"] == 4 and plans["mixed"]["cost"] == 3, "pilot optimum drift") + words = {name: model.emit(spec, name) for name in ("eager", "coherent", "output_only", "direct")} + words.update({name: model.emit(spec, "planned", plans[name]) for name in ("strict", "mixed")}) + semantic = {name: model.check_word(spec, word) for name, word in words.items()} + return {"schema_version": 1, "status": "SCOPED_EXACT_INTERFACE_NO_NEW_KAPPA", "source_pins": pins, + "spec": spec, "demands": ds, "plans": plans, "optimality": optimality, + "words": words, "invoices": {name: model.invoice(word) for name, word in words.items()}, + "symbolic_semantics": semantic, "array_evidence": array_evidence(spec, words), + "small_exhaustion": exhaustive_small(), + "controls": controls(spec, plans, words, conditions, optimality["mixed"]["potential"])} + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument("--write", type=Path, help="authoring only: export to a new file, not certificate acceptance") + args = ap.parse_args() + result = build() + encoded = json.dumps(result, indent=2, sort_keys=True) + "\n" + if args.write: + with args.write.open("x") as out: + out.write(encoded) + print("EXPORTED_SCOPED_CERTIFICATE (not acceptance against committed certificate)") + return + expected = json.loads((HERE / "CERTIFICATE.json").read_text()) + require(result == expected, "committed certificate mismatch") + print("PASS_OBSERVABLE_CONNECTOR strict=4 mixed=3 coherent=14 " + "complete_xors=72_to_61 small_cases=6220 controls=14 no_new_kappa") + + +if __name__ == "__main__": + try: + main() + except (OSError, ValueError, KeyError, TypeError) as exc: + raise SystemExit("FAIL_OBSERVABLE_CONNECTOR: " + str(exc))