diff --git a/research/r439-block1-schedule/CANDIDATE.json b/research/r439-block1-schedule/CANDIDATE.json new file mode 100644 index 0000000000..de2944f738 --- /dev/null +++ b/research/r439-block1-schedule/CANDIDATE.json @@ -0,0 +1,2602 @@ +{ + "block": 1, + "phase": "B", + "start": 128, + "stop": 163, + "frame": 507, + "registers": [ + 0, + 3, + 11, + 61, + 62, + 63, + 68, + 69, + 72, + 465 + ], + "split": 14, + "original": [ + [ + 6, + 2 + ], + [ + 6, + 5 + ], + [ + 6, + 8 + ], + [ + 6, + 0 + ], + [ + 6, + 3 + ], + [ + 1, + 4 + ], + [ + 9, + 7 + ], + [ + 9, + 5 + ], + [ + 9, + 0 + ], + [ + 7, + 2 + ], + [ + 7, + 4 + ], + [ + 5, + 8 + ], + [ + 5, + 4 + ], + [ + 5, + 0 + ], + [ + 3, + 1 + ], + [ + 3, + 7 + ], + [ + 3, + 8 + ], + [ + 3, + 4 + ], + [ + 3, + 0 + ], + [ + 0, + 6 + ], + [ + 0, + 7 + ], + [ + 4, + 6 + ], + [ + 4, + 1 + ], + [ + 4, + 7 + ], + [ + 8, + 6 + ], + [ + 8, + 1 + ], + [ + 5, + 1 + ], + [ + 5, + 7 + ], + [ + 2, + 6 + ], + [ + 2, + 1 + ], + [ + 2, + 7 + ], + [ + 7, + 6 + ], + [ + 9, + 6 + ], + [ + 9, + 1 + ], + [ + 1, + 6 + ] + ], + "replacement": [ + [ + 1, + 4 + ], + [ + 6, + 0 + ], + [ + 6, + 2 + ], + [ + 6, + 3 + ], + [ + 6, + 5 + ], + [ + 6, + 8 + ], + [ + 9, + 0 + ], + [ + 9, + 5 + ], + [ + 9, + 7 + ], + [ + 5, + 0 + ], + [ + 5, + 4 + ], + [ + 5, + 8 + ], + [ + 7, + 2 + ], + [ + 7, + 4 + ], + [ + 3, + 0 + ], + [ + 3, + 1 + ], + [ + 3, + 4 + ], + [ + 3, + 7 + ], + [ + 3, + 8 + ], + [ + 5, + 1 + ], + [ + 5, + 7 + ], + [ + 7, + 6 + ], + [ + 0, + 7 + ], + [ + 2, + 1 + ], + [ + 2, + 7 + ], + [ + 4, + 1 + ], + [ + 4, + 7 + ], + [ + 1, + 6 + ], + [ + 8, + 1 + ], + [ + 9, + 1 + ] + ], + "factors": [ + { + "minimum": 14, + "reachable_states": 1024, + "reachable_edges": 4480, + "batches": [ + [ + 0, + [] + ], + [ + 1, + [ + 4 + ] + ], + [ + 2, + [] + ], + [ + 3, + [] + ], + [ + 4, + [] + ], + [ + 6, + [ + 0, + 2, + 3, + 5, + 8 + ] + ], + [ + 9, + [ + 0, + 5, + 7 + ] + ], + [ + 5, + [ + 0, + 4, + 8 + ] + ], + [ + 7, + [ + 2, + 4 + ] + ], + [ + 8, + [] + ] + ], + "gates": [ + [ + 1, + 4 + ], + [ + 6, + 0 + ], + [ + 6, + 2 + ], + [ + 6, + 3 + ], + [ + 6, + 5 + ], + [ + 6, + 8 + ], + [ + 9, + 0 + ], + [ + 9, + 5 + ], + [ + 9, + 7 + ], + [ + 5, + 0 + ], + [ + 5, + 4 + ], + [ + 5, + 8 + ], + [ + 7, + 2 + ], + [ + 7, + 4 + ] + ], + "distance": [ + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 1, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 2, + 2, + 3, + 3, + 2, + 2, + 3, + 3, + 2, + 2, + 3, + 3, + 2, + 2, + 3, + 3, + 2, + 2, + 3, + 3, + 2, + 2, + 3, + 3, + 2, + 2, + 3, + 3, + 2, + 2, + 3, + 3, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 7, + 7, + 8, + 8, + 7, + 7, + 8, + 8, + 7, + 7, + 8, + 8, + 7, + 7, + 8, + 8, + 7, + 7, + 8, + 8, + 7, + 7, + 8, + 8, + 7, + 7, + 8, + 8, + 7, + 7, + 8, + 8, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 1, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 2, + 2, + 3, + 3, + 2, + 2, + 3, + 3, + 2, + 2, + 3, + 3, + 2, + 2, + 3, + 3, + 2, + 2, + 3, + 3, + 2, + 2, + 3, + 3, + 2, + 2, + 3, + 3, + 2, + 2, + 3, + 3, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 7, + 7, + 8, + 8, + 7, + 7, + 8, + 8, + 7, + 7, + 8, + 8, + 7, + 7, + 8, + 8, + 7, + 7, + 8, + 8, + 7, + 7, + 8, + 8, + 7, + 7, + 8, + 8, + 7, + 7, + 8, + 8, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 6, + 6, + 7, + 7, + 6, + 6, + 7, + 7, + 6, + 6, + 7, + 7, + 6, + 6, + 7, + 7, + 6, + 6, + 7, + 7, + 6, + 6, + 7, + 7, + 6, + 6, + 7, + 7, + 6, + 6, + 7, + 7, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 11, + 11, + 12, + 12, + 11, + 11, + 12, + 12, + 11, + 11, + 12, + 12, + 11, + 11, + 12, + 12, + 11, + 11, + 12, + 12, + 11, + 11, + 12, + 12, + 11, + 11, + 12, + 12, + 11, + 11, + 12, + 12, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 13, + 13, + 14, + 14, + 13, + 13, + 14, + 14, + 13, + 13, + 14, + 14, + 13, + 13, + 14, + 14, + 13, + 13, + 14, + 14, + 13, + 13, + 14, + 14, + 13, + 13, + 14, + 14, + 13, + 13, + 14, + 14, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 3, + 3, + 4, + 4, + 6, + 6, + 7, + 7, + 6, + 6, + 7, + 7, + 6, + 6, + 7, + 7, + 6, + 6, + 7, + 7, + 6, + 6, + 7, + 7, + 6, + 6, + 7, + 7, + 6, + 6, + 7, + 7, + 6, + 6, + 7, + 7, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 11, + 11, + 12, + 12, + 11, + 11, + 12, + 12, + 11, + 11, + 12, + 12, + 11, + 11, + 12, + 12, + 11, + 11, + 12, + 12, + 11, + 11, + 12, + 12, + 11, + 11, + 12, + 12, + 11, + 11, + 12, + 12, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 5, + 5, + 6, + 6, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 8, + 8, + 9, + 9, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 10, + 10, + 11, + 11, + 13, + 13, + 14, + 14, + 13, + 13, + 14, + 14, + 13, + 13, + 14, + 14, + 13, + 13, + 14, + 14, + 13, + 13, + 14, + 14, + 13, + 13, + 14, + 14, + 13, + 13, + 14, + 14, + 13, + 13, + 14, + 14 + ] + }, + { + "minimum": 16, + "reachable_states": 1024, + "reachable_edges": 3984, + "batches": [ + [ + 3, + [ + 0, + 1, + 4, + 7, + 8 + ] + ], + [ + 5, + [ + 1, + 7 + ] + ], + [ + 7, + [ + 6 + ] + ], + [ + 0, + [ + 7 + ] + ], + [ + 2, + [ + 1, + 7 + ] + ], + [ + 4, + [ + 1, + 7 + ] + ], + [ + 1, + [ + 6 + ] + ], + [ + 6, + [] + ], + [ + 8, + [ + 1 + ] + ], + [ + 9, + [ + 1 + ] + ] + ], + "gates": [ + [ + 3, + 0 + ], + [ + 3, + 1 + ], + [ + 3, + 4 + ], + [ + 3, + 7 + ], + [ + 3, + 8 + ], + [ + 5, + 1 + ], + [ + 5, + 7 + ], + [ + 7, + 6 + ], + [ + 0, + 7 + ], + [ + 2, + 1 + ], + [ + 2, + 7 + ], + [ + 4, + 1 + ], + [ + 4, + 7 + ], + [ + 1, + 6 + ], + [ + 8, + 1 + ], + [ + 9, + 1 + ] + ], + "distance": [ + 0, + 2, + 1, + 3, + 3, + 5, + 3, + 5, + 5, + 7, + 6, + 8, + 8, + 10, + 8, + 10, + 3, + 5, + 3, + 5, + 6, + 8, + 5, + 7, + 8, + 10, + 8, + 10, + 11, + 13, + 10, + 12, + 2, + 4, + 3, + 5, + 5, + 7, + 5, + 7, + 7, + 9, + 8, + 10, + 10, + 12, + 10, + 12, + 5, + 7, + 5, + 7, + 8, + 10, + 7, + 9, + 10, + 12, + 10, + 12, + 13, + 15, + 12, + 14, + 0, + 2, + 1, + 3, + 3, + 5, + 3, + 5, + 5, + 7, + 6, + 8, + 8, + 10, + 8, + 10, + 3, + 5, + 3, + 5, + 6, + 8, + 5, + 7, + 8, + 10, + 8, + 10, + 11, + 13, + 10, + 12, + 2, + 4, + 3, + 5, + 5, + 7, + 5, + 7, + 7, + 9, + 8, + 10, + 10, + 12, + 10, + 12, + 5, + 7, + 5, + 7, + 8, + 10, + 7, + 9, + 10, + 12, + 10, + 12, + 13, + 15, + 12, + 14, + 1, + 2, + 2, + 3, + 3, + 4, + 4, + 5, + 6, + 7, + 7, + 8, + 8, + 9, + 9, + 10, + 3, + 4, + 4, + 5, + 5, + 6, + 6, + 7, + 8, + 9, + 9, + 10, + 10, + 11, + 11, + 12, + 3, + 4, + 4, + 5, + 5, + 6, + 6, + 7, + 8, + 9, + 9, + 10, + 10, + 11, + 11, + 12, + 5, + 6, + 6, + 7, + 7, + 8, + 8, + 9, + 10, + 11, + 11, + 12, + 12, + 13, + 13, + 14, + 1, + 2, + 2, + 3, + 3, + 4, + 4, + 5, + 6, + 7, + 7, + 8, + 8, + 9, + 9, + 10, + 3, + 4, + 4, + 5, + 5, + 6, + 6, + 7, + 8, + 9, + 9, + 10, + 10, + 11, + 11, + 12, + 3, + 4, + 4, + 5, + 5, + 6, + 6, + 7, + 8, + 9, + 9, + 10, + 10, + 11, + 11, + 12, + 5, + 6, + 6, + 7, + 7, + 8, + 8, + 9, + 10, + 11, + 11, + 12, + 12, + 13, + 13, + 14, + 2, + 4, + 2, + 4, + 5, + 7, + 4, + 6, + 7, + 9, + 7, + 9, + 10, + 12, + 9, + 11, + 5, + 7, + 4, + 6, + 8, + 10, + 6, + 8, + 10, + 12, + 9, + 11, + 13, + 15, + 11, + 13, + 4, + 6, + 4, + 6, + 7, + 9, + 6, + 8, + 9, + 11, + 9, + 11, + 12, + 14, + 11, + 13, + 7, + 9, + 6, + 8, + 10, + 12, + 8, + 10, + 12, + 14, + 11, + 13, + 15, + 17, + 13, + 15, + 2, + 4, + 2, + 4, + 5, + 7, + 4, + 6, + 7, + 9, + 7, + 9, + 10, + 12, + 9, + 11, + 5, + 7, + 4, + 6, + 8, + 10, + 6, + 8, + 10, + 12, + 9, + 11, + 13, + 15, + 11, + 13, + 4, + 6, + 4, + 6, + 7, + 9, + 6, + 8, + 9, + 11, + 9, + 11, + 12, + 14, + 11, + 13, + 7, + 9, + 6, + 8, + 10, + 12, + 8, + 10, + 12, + 14, + 11, + 13, + 15, + 17, + 13, + 15, + 3, + 4, + 3, + 4, + 5, + 6, + 5, + 6, + 8, + 9, + 8, + 9, + 10, + 11, + 10, + 11, + 5, + 6, + 5, + 6, + 7, + 8, + 7, + 8, + 10, + 11, + 10, + 11, + 12, + 13, + 12, + 13, + 5, + 6, + 5, + 6, + 7, + 8, + 7, + 8, + 10, + 11, + 10, + 11, + 12, + 13, + 12, + 13, + 7, + 8, + 7, + 8, + 9, + 10, + 9, + 10, + 12, + 13, + 12, + 13, + 14, + 15, + 14, + 15, + 3, + 4, + 3, + 4, + 5, + 6, + 5, + 6, + 8, + 9, + 8, + 9, + 10, + 11, + 10, + 11, + 5, + 6, + 5, + 6, + 7, + 8, + 7, + 8, + 10, + 11, + 10, + 11, + 12, + 13, + 12, + 13, + 5, + 6, + 5, + 6, + 7, + 8, + 7, + 8, + 10, + 11, + 10, + 11, + 12, + 13, + 12, + 13, + 7, + 8, + 7, + 8, + 9, + 10, + 9, + 10, + 12, + 13, + 12, + 13, + 14, + 15, + 14, + 15, + 2, + 4, + 2, + 4, + 5, + 7, + 4, + 6, + 7, + 9, + 7, + 9, + 10, + 12, + 9, + 11, + 5, + 7, + 4, + 6, + 8, + 10, + 6, + 8, + 10, + 12, + 9, + 11, + 13, + 15, + 11, + 13, + 4, + 6, + 4, + 6, + 7, + 9, + 6, + 8, + 9, + 11, + 9, + 11, + 12, + 14, + 11, + 13, + 7, + 9, + 6, + 8, + 10, + 12, + 8, + 10, + 12, + 14, + 11, + 13, + 15, + 17, + 13, + 15, + 2, + 4, + 2, + 4, + 5, + 7, + 4, + 6, + 7, + 9, + 7, + 9, + 10, + 12, + 9, + 11, + 5, + 7, + 4, + 6, + 8, + 10, + 6, + 8, + 10, + 12, + 9, + 11, + 13, + 15, + 11, + 13, + 4, + 6, + 4, + 6, + 7, + 9, + 6, + 8, + 9, + 11, + 9, + 11, + 12, + 14, + 11, + 13, + 7, + 9, + 6, + 8, + 10, + 12, + 8, + 10, + 12, + 14, + 11, + 13, + 15, + 17, + 13, + 15, + 3, + 4, + 3, + 4, + 5, + 6, + 5, + 6, + 8, + 9, + 8, + 9, + 10, + 11, + 10, + 11, + 5, + 6, + 5, + 6, + 7, + 8, + 7, + 8, + 10, + 11, + 10, + 11, + 12, + 13, + 12, + 13, + 5, + 6, + 5, + 6, + 7, + 8, + 7, + 8, + 10, + 11, + 10, + 11, + 12, + 13, + 12, + 13, + 7, + 8, + 7, + 8, + 9, + 10, + 9, + 10, + 12, + 13, + 12, + 13, + 14, + 15, + 14, + 15, + 3, + 4, + 3, + 4, + 5, + 6, + 5, + 6, + 8, + 9, + 8, + 9, + 10, + 11, + 10, + 11, + 5, + 6, + 5, + 6, + 7, + 8, + 7, + 8, + 10, + 11, + 10, + 11, + 12, + 13, + 12, + 13, + 5, + 6, + 5, + 6, + 7, + 8, + 7, + 8, + 10, + 11, + 10, + 11, + 12, + 13, + 12, + 13, + 7, + 8, + 7, + 8, + 9, + 10, + 9, + 10, + 12, + 13, + 12, + 13, + 14, + 15, + 14, + 15, + 4, + 6, + 3, + 5, + 7, + 9, + 5, + 7, + 9, + 11, + 8, + 10, + 12, + 14, + 10, + 12, + 7, + 9, + 5, + 7, + 10, + 12, + 7, + 9, + 12, + 14, + 10, + 12, + 15, + 17, + 12, + 14, + 6, + 8, + 5, + 7, + 9, + 11, + 7, + 9, + 11, + 13, + 10, + 12, + 14, + 16, + 12, + 14, + 9, + 11, + 7, + 9, + 12, + 14, + 9, + 11, + 14, + 16, + 12, + 14, + 17, + 19, + 14, + 16, + 4, + 6, + 3, + 5, + 7, + 9, + 5, + 7, + 9, + 11, + 8, + 10, + 12, + 14, + 10, + 12, + 7, + 9, + 5, + 7, + 10, + 12, + 7, + 9, + 12, + 14, + 10, + 12, + 15, + 17, + 12, + 14, + 6, + 8, + 5, + 7, + 9, + 11, + 7, + 9, + 11, + 13, + 10, + 12, + 14, + 16, + 12, + 14, + 9, + 11, + 7, + 9, + 12, + 14, + 9, + 11, + 14, + 16, + 12, + 14, + 17, + 19, + 14, + 16, + 5, + 6, + 4, + 5, + 7, + 8, + 6, + 7, + 10, + 11, + 9, + 10, + 12, + 13, + 11, + 12, + 7, + 8, + 6, + 7, + 9, + 10, + 8, + 9, + 12, + 13, + 11, + 12, + 14, + 15, + 13, + 14, + 7, + 8, + 6, + 7, + 9, + 10, + 8, + 9, + 12, + 13, + 11, + 12, + 14, + 15, + 13, + 14, + 9, + 10, + 8, + 9, + 11, + 12, + 10, + 11, + 14, + 15, + 13, + 14, + 16, + 17, + 15, + 16, + 5, + 6, + 4, + 5, + 7, + 8, + 6, + 7, + 10, + 11, + 9, + 10, + 12, + 13, + 11, + 12, + 7, + 8, + 6, + 7, + 9, + 10, + 8, + 9, + 12, + 13, + 11, + 12, + 14, + 15, + 13, + 14, + 7, + 8, + 6, + 7, + 9, + 10, + 8, + 9, + 12, + 13, + 11, + 12, + 14, + 15, + 13, + 14, + 9, + 10, + 8, + 9, + 11, + 12, + 10, + 11, + 14, + 15, + 13, + 14, + 16, + 17, + 15, + 16 + ] + } + ], + "reverse_dominated": true, + "source_sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" +} diff --git a/research/r439-block1-schedule/CERTIFICATE.json b/research/r439-block1-schedule/CERTIFICATE.json new file mode 100644 index 0000000000..bb62cc8b15 --- /dev/null +++ b/research/r439-block1-schedule/CERTIFICATE.json @@ -0,0 +1,728 @@ +{ + "F2_matrix": [ + [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 1, + 0 + ], + [ + 1, + 1, + 1, + 1, + 0, + 1, + 1, + 1, + 1, + 0 + ], + [ + 1, + 1, + 1, + 1, + 1, + 0, + 0, + 1, + 1, + 0 + ], + [ + 1, + 1, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 1, + 1, + 1, + 0, + 1, + 1, + 0, + 1, + 1, + 0 + ], + [ + 1, + 0, + 1, + 1, + 0, + 1, + 1, + 0, + 1, + 0 + ], + [ + 1, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + 0 + ], + [ + 0, + 1, + 1, + 1, + 1, + 0, + 1, + 1, + 1, + 1 + ] + ], + "block": 1, + "boolean_inputs": 1024, + "columns": 661, + "controls_rejected": [ + "understated factor minimum", + "altered distance potential", + "missing factor", + "self addition", + "boolean register index", + "drop circuit gate", + "reverse circuit operand", + "F2-neutral positive-cost inflation", + "dropped cleanup", + "nonliteral original cleanup", + "illegal lower frame", + "missing dirty compensation", + "dropped exported block ADD" + ], + "factor_optimality": [ + { + "distance_sha256": "0fbd8783c3b20dbc065121243b07f988d06d2875162835df62177c5c16cabb35", + "feasible_edges": 4480, + "minimum": 14, + "state_destination_checks": 5120, + "states": 1024 + }, + { + "distance_sha256": "f7b0793f5633c2361bc53598867914597d1c9f780db61a04106828503ae56be4", + "feasible_edges": 3984, + "minimum": 16, + "state_destination_checks": 5120, + "states": 1024 + } + ], + "kappa_claim": "none; unchanged paid rank profile, no hosted replay", + "labels": { + "frames": 636, + "gram_det": 1, + "labels": 111, + "lattice_rank": 8, + "punctured": 9, + "root_lines": 120 + }, + "native_records": { + "original": { + "adds": 24305, + "copies": 9, + "erasures": 9, + "moves": 2911, + "paid_histogram": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "payload_prefix_bits": 93, + "payload_prefix_upper": "9528119495320518471870892800", + "positive_prefix": [ + 49347, + 1113070 + ], + "rank_mass": 5129, + "records": 27234, + "records_sha256": "ea44aa047a2a9cf034de8b56b2166c49cf2dbdf9cd9ed6a20299a4f2b05ef09a" + }, + "replacement": { + "adds": 24295, + "copies": 9, + "erasures": 9, + "moves": 2911, + "paid_histogram": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "payload_prefix_bits": 93, + "payload_prefix_upper": "9257646390457307514450801408", + "positive_prefix": [ + 49347, + 1097158 + ], + "rank_mass": 5129, + "records": 27224, + "records_sha256": "6e9bd3b124c3eb0794637aa33ed297421a4c74e3e7cbc748650d0beb8f923587" + } + }, + "new_gates": 30, + "new_phase_gates": { + "A": 2075, + "B": 707, + "C": 2569, + "D": 111 + }, + "old_gates": 35, + "old_phase_gates": { + "A": 2075, + "B": 712, + "C": 2574, + "D": 111 + }, + "positive_matrices": { + "forward": { + "original": [ + [ + 2, + 0, + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 1, + 0 + ], + [ + 1, + 1, + 3, + 1, + 2, + 1, + 1, + 1, + 1, + 0 + ], + [ + 1, + 1, + 1, + 1, + 3, + 0, + 0, + 1, + 1, + 0 + ], + [ + 1, + 1, + 2, + 1, + 3, + 1, + 1, + 1, + 1, + 0 + ], + [ + 1, + 1, + 1, + 0, + 3, + 1, + 0, + 1, + 1, + 0 + ], + [ + 1, + 0, + 1, + 1, + 0, + 1, + 1, + 0, + 1, + 0 + ], + [ + 1, + 0, + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 2, + 0 + ], + [ + 2, + 1, + 1, + 1, + 1, + 2, + 1, + 1, + 1, + 1 + ] + ], + "replacement": [ + [ + 2, + 0, + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 1, + 0 + ], + [ + 1, + 1, + 3, + 1, + 2, + 1, + 1, + 1, + 1, + 0 + ], + [ + 1, + 1, + 1, + 1, + 3, + 0, + 0, + 1, + 1, + 0 + ], + [ + 1, + 1, + 2, + 1, + 3, + 1, + 1, + 1, + 1, + 0 + ], + [ + 1, + 1, + 1, + 0, + 3, + 1, + 0, + 1, + 1, + 0 + ], + [ + 1, + 0, + 1, + 1, + 0, + 1, + 1, + 0, + 1, + 0 + ], + [ + 1, + 0, + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 2, + 0 + ], + [ + 2, + 1, + 1, + 1, + 1, + 2, + 1, + 1, + 1, + 1 + ] + ] + }, + "reverse": { + "original": [ + [ + 1, + 0, + 0, + 0, + 0, + 0, + 2, + 1, + 0, + 0 + ], + [ + 0, + 2, + 0, + 0, + 1, + 0, + 4, + 1, + 0, + 0 + ], + [ + 0, + 1, + 1, + 0, + 0, + 0, + 3, + 1, + 0, + 0 + ], + [ + 1, + 3, + 0, + 1, + 1, + 0, + 9, + 3, + 1, + 0 + ], + [ + 0, + 1, + 0, + 0, + 1, + 0, + 3, + 1, + 0, + 0 + ], + [ + 1, + 3, + 0, + 0, + 1, + 1, + 9, + 3, + 1, + 0 + ], + [ + 3, + 8, + 1, + 1, + 2, + 1, + 26, + 8, + 3, + 0 + ], + [ + 0, + 2, + 1, + 0, + 1, + 0, + 7, + 3, + 0, + 0 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0, + 2, + 0, + 1, + 0 + ], + [ + 2, + 6, + 1, + 0, + 2, + 1, + 20, + 7, + 1, + 1 + ] + ], + "replacement": [ + [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 0 + ], + [ + 0, + 2, + 0, + 0, + 1, + 0, + 2, + 1, + 0, + 0 + ], + [ + 0, + 1, + 1, + 0, + 0, + 0, + 1, + 1, + 0, + 0 + ], + [ + 1, + 3, + 0, + 1, + 1, + 0, + 3, + 3, + 1, + 0 + ], + [ + 0, + 1, + 0, + 0, + 1, + 0, + 1, + 1, + 0, + 0 + ], + [ + 1, + 3, + 0, + 0, + 1, + 1, + 3, + 3, + 1, + 0 + ], + [ + 3, + 8, + 1, + 1, + 2, + 1, + 8, + 8, + 3, + 0 + ], + [ + 0, + 2, + 1, + 0, + 1, + 0, + 3, + 3, + 0, + 0 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0 + ], + [ + 2, + 6, + 1, + 0, + 2, + 1, + 6, + 7, + 1, + 1 + ] + ] + } + }, + "reconstructed_word_sha256": "0f35e69cb568e780e83d8bec32cfa98c36bfe2cfb42d1adb9f53d6babddb485b", + "saved_with_cleanup": 10, + "status": "PASS_R439_BLOCK1_SCHEDULE" +} diff --git a/research/r439-block1-schedule/CLAIM.md b/research/r439-block1-schedule/CLAIM.md new file mode 100644 index 0000000000..a7d556aa13 --- /dev/null +++ b/research/r439-block1-schedule/CLAIM.md @@ -0,0 +1,73 @@ +# Local sprint claim + +- Track: bit supplier. OS assignment seed **8**, drawn with Python + `secrets.randbelow(100)` on 2026-10-13 at approximately 08:37 UTC. +- Base: `f567884aeb8851b6e794af1184119a3bfbe1e631`. +- Scope: selected PR589 R439 phase-B block **1**, `B[128:163]`, frame 507, + ordered registers `[0,3,11,61,62,63,68,69,72,465]`. This punctured ten-wire + block includes arbitrary dirty helper 465, unlike the twelve-source blocks. +- Hypothesis: exact positive-integer rescheduling of the two existing factors + (first 14 gates, last 21 gates) reduces the scalar additions while preserving + the physical output assignment and not increasing positive reverse bounds. +- Method: complete subset-state dynamic programming in each factor's + destination-once positive-addition class. No helper, output permutation, + repeated destination batch, frame change, or additional copied total. +- Deliverable: literal circuit, finite search certificate, full local arbitrary + input replay, exact complete cost, native checks if available, source pins, + negative controls and a scoped research note. No kappa claim. +- Timebox: 40 minutes from 08:37 to 09:17 UTC; orientation ends by 08:45; + reserve 09:07 onward for verification and handoff. +- Claim recorded: 2026-10-13 approximately 08:43 UTC. No pinned issue exists + (GitHub GraphQL `pinnedIssues(first:10)` returned an empty list immediately + before this claim); no separate issue opened. + +## Candidate selection and overlap + +Three candidates: (1) a fixed-frame rewrite of a punctured phase-B block; +(2) an A-stage single-summand transport at frame 509; (3) smaller cleanup frames +for the fixed decoder. Candidate 2 overlaps PR589's fixed-point transport and +PR843's new source sum; candidate 3 is excluded in the stated fixed-prefix model +by PR827 and has the restored-sharing obstruction in PR848. Choose candidate 1. + +Diversification: apply `random.Random(8).sample([0,1,3,5],4)` to the four +punctured blocks, obtaining `[1,5,3,0]`; take block 1. This selects a different +matrix and dirty-helper interface, not merely a new seed for an old search. +The completed greedy transport search in PR589 does not search this class. +PR844 changes block 4 and PR857 changes block 8. PR728/792 change A mini-nodes. +Historical R420 block work (PR789/790/810) supplies related scheduling ideas, +but no pending code or savings are imported. PR661 fixes the gate word and +PR827 excludes smaller cleanup frames; neither excludes a scalar rewrite. + +Read the contribution rules, selected certificate, current review and status, +central review ledger and contribution-review index. Current conditional +kappa is 0.001661634653669567 (PR799/589), not a historical PR title. +Initial live overlap check: recent 100 open PRs through #867, all R420/R439 +search results; exact R439 search returned 11 open/closed PRs and no block-1 +claim. Source PR589 head is `a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46`. + +Contributor: @Deftsalt-debug, with substantial OpenAI Codex assistance. + +## Result and handoff — 2026-10-13, approximately 09:02 UTC + +Completed: [construction, proof and replay](README.md). Block 1 falls 35 -> 30 +ADDs and complete native ADDs fall 24,305 -> 24,295. Both fixed-factor optima +(14 + 16) are checked over all 2,048 states by two different implementations. +All 661 dirty-input columns, thirteen controls, identical frame paths/profile +and the reduced positive prefix pass. Both words also pass unchanged native +legality and 5/9/11-stage checks with 96 bridge controls; minimal relocated +optimized replay passes. No new kappa, unrestricted optimum or hosted invoice. + +Final overlap refresh through #874 found navinor's #873 at +`117c48527dd4f066dad103121761154cf1bb39cd`, a distinct whole-block rescheduling of +frame 508. It is credited in the README; no priority or composition is claimed. +PR844 and PR857 still concern frames 520 and 523. Main remains the exact base. + +Initial GitHub fork creation returned HTTP 403, `Resource not accessible by +integration`, so the first handoff was a local commit and verified patch. +After the contributor created the fork, the finished branch was successfully +[pushed to Deftsalt-debug/integer-mult-bounds](https://github.com/Deftsalt-debug/integer-mult-bounds/tree/research/r439-block1-schedule-seed8). +A publication-time overlap refresh through PR876 found no matching block-1 +contribution; main remained the exact base. Both CLI and connected-app attempts +to create the upstream PR returned HTTP 403. No PR was created. The contributor +can [open the prepared comparison](https://github.com/CrocSwap/integer-mult-bounds/compare/main...Deftsalt-debug:research/r439-block1-schedule-seed8?expand=1). +Validation details are in [VALIDATION.md](VALIDATION.md). diff --git a/research/r439-block1-schedule/NATIVE.json b/research/r439-block1-schedule/NATIVE.json new file mode 100644 index 0000000000..2bb6f527eb --- /dev/null +++ b/research/r439-block1-schedule/NATIVE.json @@ -0,0 +1,1202 @@ +{ + "original": { + "legality": { + "all_final_frames_pass": true, + "common_frame_ADDs": 24305, + "containment_pairs_checked": 2386, + "copies": 9, + "donor_intersections": 0, + "erasures": 9, + "max_inherited_integer_abs": 2, + "nested_MOVEs": 2911, + "new_frame_ids_collision": false, + "nondegeneracy_checked_by_separate_exact_bank_audit": true, + "old_max_frame_id": 635, + "paid_histogram": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "rank_mass": 5129, + "records": 27234, + "scope": "Independent chronological geometry/copy/source-owner audit. F2 all-column replay is in the separately freshly compiled transform receipt; address transform theorem and bank completion remain separate.", + "selected_helpers": 0, + "selected_pairs": 0, + "source_owner_intersections": 0, + "status": "PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE" + }, + "stages": { + "11": { + "bridge_additions": 2664, + "copied_center_original_source_immutable": true, + "formal_columns_checked": 1549, + "fresh_center_copies": 99, + "global_live_registers": 1549, + "independent_dirty_registers": 439, + "local_odd_scalar_additions": 24305, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "local_registers": 661, + "local_scalar_additions": 24305, + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + }, + { + "omit_bridge": 6, + "rejected": true + }, + { + "omit_bridge": 7, + "rejected": true + }, + { + "omit_bridge": 8, + "rejected": true + }, + { + "omit_bridge": 9, + "rejected": true + }, + { + "omit_bridge": 10, + "rejected": true + }, + { + "omit_bridge": 11, + "rejected": true + }, + { + "omit_bridge": 12, + "rejected": true + }, + { + "omit_bridge": 13, + "rejected": true + }, + { + "omit_bridge": 14, + "rejected": true + }, + { + "omit_bridge": 15, + "rejected": true + }, + { + "omit_bridge": 16, + "rejected": true + }, + { + "omit_bridge": 17, + "rejected": true + }, + { + "omit_bridge": 18, + "rejected": true + }, + { + "omit_bridge": 19, + "rejected": true + }, + { + "omit_bridge": 20, + "rejected": true + }, + { + "omit_bridge": 21, + "rejected": true + }, + { + "omit_bridge": 22, + "rejected": true + }, + { + "omit_bridge": 23, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 93, + "payload_prefix_upper": "9528119495320518471870892800", + "reverse_fresh_center_copies": 45, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 21, + "cancellation_free_signed_row_l1_upper": "1113070", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stage_additions": 267355, + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 8 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 9 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 10 + } + ], + "status": "PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + }, + "5": { + "bridge_additions": 666, + "copied_center_original_source_immutable": true, + "five_stage_additions": 121525, + "formal_columns_checked": 883, + "fresh_center_copies": 45, + "global_live_registers": 883, + "independent_dirty_registers": 439, + "local_odd_scalar_additions": 24305, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "local_registers": 661, + "local_scalar_additions": 24305, + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 93, + "payload_prefix_upper": "9528119495320518471870892800", + "reverse_fresh_center_copies": 18, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 21, + "cancellation_free_signed_row_l1_upper": "1113070", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 4 + } + ], + "status": "PASS_NEW_COHORT249_ALL_FIVE_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + }, + "9": { + "bridge_additions": 1998, + "copied_center_original_source_immutable": true, + "formal_columns_checked": 1327, + "fresh_center_copies": 81, + "global_live_registers": 1327, + "independent_dirty_registers": 439, + "local_odd_scalar_additions": 24305, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "local_registers": 661, + "local_scalar_additions": 24305, + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + }, + { + "omit_bridge": 6, + "rejected": true + }, + { + "omit_bridge": 7, + "rejected": true + }, + { + "omit_bridge": 8, + "rejected": true + }, + { + "omit_bridge": 9, + "rejected": true + }, + { + "omit_bridge": 10, + "rejected": true + }, + { + "omit_bridge": 11, + "rejected": true + }, + { + "omit_bridge": 12, + "rejected": true + }, + { + "omit_bridge": 13, + "rejected": true + }, + { + "omit_bridge": 14, + "rejected": true + }, + { + "omit_bridge": 15, + "rejected": true + }, + { + "omit_bridge": 16, + "rejected": true + }, + { + "omit_bridge": 17, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 93, + "payload_prefix_upper": "9528119495320518471870892800", + "reverse_fresh_center_copies": 36, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 21, + "cancellation_free_signed_row_l1_upper": "1113070", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stage_additions": 218745, + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 8 + } + ], + "status": "PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + } + } + }, + "replacement": { + "legality": { + "all_final_frames_pass": true, + "common_frame_ADDs": 24295, + "containment_pairs_checked": 2386, + "copies": 9, + "donor_intersections": 0, + "erasures": 9, + "max_inherited_integer_abs": 2, + "nested_MOVEs": 2911, + "new_frame_ids_collision": false, + "nondegeneracy_checked_by_separate_exact_bank_audit": true, + "old_max_frame_id": 635, + "paid_histogram": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "rank_mass": 5129, + "records": 27224, + "scope": "Independent chronological geometry/copy/source-owner audit. F2 all-column replay is in the separately freshly compiled transform receipt; address transform theorem and bank completion remain separate.", + "selected_helpers": 0, + "selected_pairs": 0, + "source_owner_intersections": 0, + "status": "PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE" + }, + "stages": { + "11": { + "bridge_additions": 2664, + "copied_center_original_source_immutable": true, + "formal_columns_checked": 1549, + "fresh_center_copies": 99, + "global_live_registers": 1549, + "independent_dirty_registers": 439, + "local_odd_scalar_additions": 24295, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "local_registers": 661, + "local_scalar_additions": 24295, + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + }, + { + "omit_bridge": 6, + "rejected": true + }, + { + "omit_bridge": 7, + "rejected": true + }, + { + "omit_bridge": 8, + "rejected": true + }, + { + "omit_bridge": 9, + "rejected": true + }, + { + "omit_bridge": 10, + "rejected": true + }, + { + "omit_bridge": 11, + "rejected": true + }, + { + "omit_bridge": 12, + "rejected": true + }, + { + "omit_bridge": 13, + "rejected": true + }, + { + "omit_bridge": 14, + "rejected": true + }, + { + "omit_bridge": 15, + "rejected": true + }, + { + "omit_bridge": 16, + "rejected": true + }, + { + "omit_bridge": 17, + "rejected": true + }, + { + "omit_bridge": 18, + "rejected": true + }, + { + "omit_bridge": 19, + "rejected": true + }, + { + "omit_bridge": 20, + "rejected": true + }, + { + "omit_bridge": 21, + "rejected": true + }, + { + "omit_bridge": 22, + "rejected": true + }, + { + "omit_bridge": 23, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 93, + "payload_prefix_upper": "9257646390457307514450801408", + "reverse_fresh_center_copies": 45, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 21, + "cancellation_free_signed_row_l1_upper": "1097158", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stage_additions": 267245, + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": false, + "stage": 8 + }, + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": true, + "stage": 9 + }, + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": false, + "stage": 10 + } + ], + "status": "PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + }, + "5": { + "bridge_additions": 666, + "copied_center_original_source_immutable": true, + "five_stage_additions": 121475, + "formal_columns_checked": 883, + "fresh_center_copies": 45, + "global_live_registers": 883, + "independent_dirty_registers": 439, + "local_odd_scalar_additions": 24295, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "local_registers": 661, + "local_scalar_additions": 24295, + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 93, + "payload_prefix_upper": "9257646390457307514450801408", + "reverse_fresh_center_copies": 18, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 21, + "cancellation_free_signed_row_l1_upper": "1097158", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": false, + "stage": 4 + } + ], + "status": "PASS_NEW_COHORT249_ALL_FIVE_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + }, + "9": { + "bridge_additions": 1998, + "copied_center_original_source_immutable": true, + "formal_columns_checked": 1327, + "fresh_center_copies": 81, + "global_live_registers": 1327, + "independent_dirty_registers": 439, + "local_odd_scalar_additions": 24295, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "local_registers": 661, + "local_scalar_additions": 24295, + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + }, + { + "omit_bridge": 6, + "rejected": true + }, + { + "omit_bridge": 7, + "rejected": true + }, + { + "omit_bridge": 8, + "rejected": true + }, + { + "omit_bridge": 9, + "rejected": true + }, + { + "omit_bridge": 10, + "rejected": true + }, + { + "omit_bridge": 11, + "rejected": true + }, + { + "omit_bridge": 12, + "rejected": true + }, + { + "omit_bridge": 13, + "rejected": true + }, + { + "omit_bridge": 14, + "rejected": true + }, + { + "omit_bridge": 15, + "rejected": true + }, + { + "omit_bridge": 16, + "rejected": true + }, + { + "omit_bridge": 17, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 93, + "payload_prefix_upper": "9257646390457307514450801408", + "reverse_fresh_center_copies": 36, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 21, + "cancellation_free_signed_row_l1_upper": "1097158", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stage_additions": 218655, + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 24295, + "signed_inverse": false, + "stage": 8 + } + ], + "status": "PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + } + } + } +} diff --git a/research/r439-block1-schedule/README.md b/research/r439-block1-schedule/README.md new file mode 100644 index 0000000000..749826d207 --- /dev/null +++ b/research/r439-block1-schedule/README.md @@ -0,0 +1,214 @@ +# R439 punctured block 1: 35 additions become 30 + +**Finite bit-supplier construction, with a scoped finite-class optimum. No new +kappa.** PR589's phase-B block 1 can use **30 instead of 35 additions**, with +the same positive integer map on all ten arbitrary inputs. Rebuilding the +required literal reverse cleanup saves five more: the complete local word goes +from **24,305 to 24,295 native ADDs**. Only this research directory is added. + +The block includes dirty helper register 465. Its input is never assumed zero. +Every one of the 661 physical registers retains its frame path; all 439 helpers, +nine retained copies, source accesses, restoration and recursive charges remain +accounted for. The positive reverse matrix decreases entrywise. The complete +native payload allowance remains **93 bits**, below the unchanged 104-bit cap. + +| Complete local quantity | Original | Replacement | +|---|---:|---:| +| Phase-B block additions | 35 | 30 | +| Corresponding literal cleanup additions | 35 | 30 | +| Native scalar additions, including scatter | 24,305 | 24,295 | +| Native records | 27,234 | 27,224 | +| Frame climbs | 2,911 | 2,911 | +| Positive forward prefix bound | 49,347 | 49,347 | +| Positive reverse prefix bound | 1,113,070 | 1,097,158 | +| Paid rank mass | 5,129 | 5,129 | + +The paid histogram is unchanged: +`{1:1323, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:19}`. +This is a circuit count, not a runtime benchmark or an exponent improvement. + +## Reproduce + +Python 3.10+ with its standard library suffices: + +```sh +python3 -I -B research/r439-block1-schedule/verify.py +``` + +Expected final line: + +```text +PASS_R439_BLOCK1_SCHEDULE gates=35->30 native_adds=24305->24295 columns=661 rank_mass=5129 controls=13 +``` + +This checks the source pins, the exact factor minima, all 1,024 local Boolean +inputs, the unchanged owning E8/frame/interface checker, all 661 dirty-input +columns, actual exported record semantics and COPY/ERASE lifecycle, complete +positive bounds, the paid profile, and thirteen negative controls. It compares +the complete deterministic report with `CERTIFICATE.json`. + +`--output /absolute/new/directory` retains the reconstructed words and native +records; an existing destination is refused. `--write-certificate` explicitly +regenerates only this package's report. Ordinary verification changes no source +or committed artifact. + +The exhaustive nomination can also be reproduced, independently of the checker: + +```sh +python3 -I -B research/r439-block1-schedule/search.py +``` + +Expected: `PASS_R439_BLOCK1_SEARCH gates=35->30 minima=14+16 reverse_dominated=True`. +`--write` explicitly regenerates `CANDIDATE.json`. + +`python3 -I -B research/r439-block1-schedule/check_package.py` checks isolated, +optimized execution from a minimal source tree with spaces in its path, five +source/receipt/candidate corruptions, and preservation of an existing output +directory. Its expected marker is `PASS_R439_BLOCK1_PACKAGE`. + +For the unchanged C++17/Boost legality and five/nine/eleven-stage checkers: + +```sh +python3 -I -B research/r439-block1-schedule/native.py +``` + +Expected: `PASS_R439_BLOCK1_NATIVE words=2 stages=5,9,11 columns=883,1327,1549 bridge_controls=96`. +Set `BOOST_INCLUDE` to the include directory when Boost is installed outside +the default compiler path. `CXX` selects the compiler. `--output` retains logs +in a fresh directory; `--write-receipt` explicitly regenerates `NATIVE.json`. +Only time and the temporary stream pathname are excluded from native receipt +comparison. All proof-relevant receipt fields are compared. + +## Circuit and complete cost + +The exact object is `B[128:163]` in +`research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz`, at frame **507**. +The ordered physical registers are +`[0,3,11,61,62,63,68,69,72,465]`. +The two fixed positive factors are the first **14** and final **21** gates. +The replacement retains their integer maps and uses **14 + 16** gates. + +The saving comes from using two existing destinations as accumulated donors. +In the second factor, first perform the original updates to registers 61 and +63. Then update `69 += 68`, allowing registers 0, 11 and 62 to read that sum +directly. Next update `3 += 68`, allowing registers 72 and 465 to read that +sum directly. These five shared pair reads each save one addition. The full +literal schedule and its physical binding are in `CANDIDATE.json`. + +There is no new preparation, scratch, source read, COPY, frame or child cost. +Every addition in the substitute and in its regenerated reverse is counted. +The native multistage checks include their bridge additions and arbitrary +helper restoration. The unchanged global supplier is complex-bound; in any +case, an unchanged bit moment supplies no larger kappa. A new globally hosted +invoice is not inferred from these local counts. + +## Exactness and scope of the optimum + +For each fixed factor, consider only positive-addition schedules in which each +physical destination is finished in one contiguous batch and never changed +again. A batch may be empty. There are no additional wires, permutations, +negative additions, or changes to the boundary between factors. Donors can be +any other current registers. This is a restriction on schedules, not a lower +bound on unrestricted XOR circuits. + +At state `S`, a finished row is its prescribed target row and an unfinished row +is its input unit vector. Finalizing destination `r` means adding other current +rows to make exactly `target[r] - e_r`. All target entries are zero or one and +each current row has a diagonal one, so no donor can appear twice. Thus every +possible batch is represented by a donor subset. The cost is its cardinality. +Donors are unchanged within the batch, making their order immaterial. + +The state graph is acyclic: an edge adds one destination to `S`. The Bellman +recurrence from the empty state therefore gives exact minimum path costs. +Both graphs have all **1,024** states reachable. Their complete edge counts are +**4,480** and **3,984**; each implementation examines **5,120** state/destination +pairs per factor. Minima **14 and 16** are attained by the recorded schedules. +The stopping rule is exhaustion of these two graphs. No random circuit trials +or time cutoffs are used, and no unrestricted minimum is claimed. + +The nomination encodes positive rows as base-11 integers and enumerates every +donor subset, with no carries possible. The verifier instead solves donor +equations by exact elimination over F2, then checks each candidate sum over Z. +Each reachable current matrix is invertible because it comes from elementary +row additions, so its F2 donor representation is unique. Consequently the +verifier cannot miss a positive integer batch. It compares all **2,048** stored +distances, not just the two final minima. These are different implementations +written by the same AI agent, not independent human review. + +For circuit correctness, columnwise integer replay proves equality of both +factor matrices, hence of the complete ordered block map over every commutative +ring. The signed inverses also agree. The whole supplier's claimed restored +endpoint is checked over F2, not asserted over Z. + +The reversed positive block matrix falls in 10 entries, its entry sum +**174 -> 116**. Inside an addition-only block, positive row bounds never +decrease, so the endpoint dominates every internal prefix. Substitution into +the unchanged positive exterior therefore cannot increase the complete forward +or reverse bound: the forward block matrix is equal, and its positive reverse +is dominated. Actual native prefix replay independently checks this argument. +The payload formula `64 * forward^3 * reverse^2` remains below `2^104`. + +## Provenance, overlap and limitations + +Base: **`f567884aeb8851b6e794af1184119a3bfbe1e631`**. +Selected conditional kappa there is **0.001661634653669567**, from PR799/589. +The reviewed PR589 supplier head is +**`a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46`**. `SOURCES.json` pins execution, +native and contextual inputs by SHA256 and base Git blob, plus the original +PR589 paths/blobs for the word, checker and generator. Those original paths +used `e8-bit-p111/`; integration renamed the retained package to +`e8-bit-p111-tuned/`. All four checked original objects match byte for byte. + +The OS assignment seed was **8**. `CLAIM.md` records the three alternatives, +seed-based selection among punctured blocks, scope, timebox and coordination +checks. No pinned sprint issue existed, so the claim is local. + +PR589's closed transport/Steinberg search does not cover this factor-scheduling +class. PR661's fixed-word frame result and PR827's fixed-prefix cleanup-frame +obstruction do not exclude a scalar rewrite. Related scheduling work is +credited: Yuzhou Wang's [PR789](https://github.com/CrocSwap/integer-mult-bounds/pull/789), +commdata2338's [PR790](https://github.com/CrocSwap/integer-mult-bounds/pull/790), +Jerry Lin's [PR810](https://github.com/CrocSwap/integer-mult-bounds/pull/810), +and Gautam Gupta's [PR844](https://github.com/CrocSwap/integer-mult-bounds/pull/844). +The latter changes R439 block 4; zeusinsight's +[PR857](https://github.com/CrocSwap/integer-mult-bounds/pull/857) changes block 8. +This contribution covers the different ten-wire, dirty-helper block 1. +Sagar Thakrar's PR728 and Ryan Haines' PR792 change phase-A mini-nodes; +PR843 changes the frame-509 source sum. No pending implementation or saving +is imported, and composition with those PRs is not certified. + +The final refresh through PR874 found concurrent **navinor's +[PR873](https://github.com/CrocSwap/integer-mult-bounds/pull/873)** at +`117c48527dd4f066dad103121761154cf1bb39cd`. It independently uses a whole-block +single-write class on the neighboring **eleven-wire frame-508 block** +`B[205:242]`. That related contribution is credited; no scheduling-mechanism +priority is claimed. This package changes **ten-wire frame 507** `B[128:163]`, +certifies two fixed factors and supplies fresh native 5/9/11-stage evidence. +It imports none of PR873's code. Main still had the pinned base at refresh. + +The complete local word and native multistage checks are covered. Fresh +globally hosted owner programs, invoices, moment/outer assembly, cold supplier +regeneration, repository-wide `make verify`, Lean and remote CI are not claimed. +This isolated addition does not change a selected input or generator, so the +affected checks are the package checks and selected-record integrity; the broad +regenerating suite is not needed to test an unchanged selected construction. +Inherited all-size/compiler, common-label/mutable-basis realization, whole-call +hosting, signed decoder, precision/tape/exact-recovery and analytic assumptions +remain. Finite certificates are not a formal multiplication theorem. + +## Credit and license + +Prepared for **Krishnendu Purohit (@Deftsalt-debug)** with substantial **OpenAI +Codex assistance** in task selection, circuit derivation, implementation, +verification and writing. No independent human review or delegated-agent review +is claimed. New files are Apache-2.0 under the repository license. + +Construction credit remains with **eumemic** (PR543/555 and scalar interface), +**DreamingOfClouds** (PR545/589 puncturing/transports and PR503/510 pricing), +**Dylan Crow** (format and exporter), **Zhihao Chen**, **DaysSky** and the full +lineage in [`NOTICE.md`](../e8-bit-p111-tuned/NOTICE.md), including Jacob +Sussman's E8 unit. The verifier structure adapts **mtpsl's PR691** +[`verify.py`](../r420-quad13/verify.py); the native harness adapts **Ali Romman's +PR688** [`native.py`](../r420-two-block-composition/native.py). Original notices +and assistance disclosures are retained. The new nomination and independently +implemented optimality check import no pending PR implementation. diff --git a/research/r439-block1-schedule/SOURCES.json b/research/r439-block1-schedule/SOURCES.json new file mode 100644 index 0000000000..d381a336c4 --- /dev/null +++ b/research/r439-block1-schedule/SOURCES.json @@ -0,0 +1,90 @@ +{ + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "supplier_head": "a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46", + "execution_inputs": [ + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "research/e8-bit-p111-tuned/code/xcheck_p.py", + "research/e8-bit-carrier-skeleton/code/bit/export_records.py" + ], + "native_inputs": [ + "research/e8-bit-carrier-skeleton/code/bit/regression/stage_cohort.py", + "research/e8-bit-carrier-skeleton/code/bit/checkers/legality_h.cpp", + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp", + "research/e8-bit-carrier-skeleton/code/bit/checkers/json.hpp", + "research/e8-bit-carrier-skeleton/portable-include/bits/stdc++.h" + ], + "context_inputs": [ + "research/e8-bit-p111-tuned/code/nodeopt.py", + "research/e8-bit-p111-tuned/code/gen_p3.py", + "research/e8-bit-p111-tuned/tune/README.md", + "research/e8-bit-p111-tuned/NOTICE.md", + "research/r420-quad13/verify.py", + "research/r420-two-block-composition/native.py" + ], + "files": { + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz": { + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f", + "base_git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "supplier_path": "research/e8-bit-p111/tune/bitE8mut-p111-tuned.json.gz", + "supplier_git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a" + }, + "research/e8-bit-p111-tuned/code/xcheck_p.py": { + "sha256": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e", + "base_git_blob": "184f5dcf94a486cc7db91ca4db5865916bf26009", + "supplier_path": "research/e8-bit-p111/code/xcheck_p.py", + "supplier_git_blob": "184f5dcf94a486cc7db91ca4db5865916bf26009" + }, + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": { + "sha256": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3", + "base_git_blob": "3632d370486a02f5456f7643ced03f8c925b2350" + }, + "research/e8-bit-p111-tuned/code/nodeopt.py": { + "sha256": "6a5896f60b1fe05c41ab28ce822dff782c635e12d0c74fad20b5ce2a4010fa3f", + "base_git_blob": "dd30a2e4e6e33ba60669d7b421229a2f6e53d6ad", + "supplier_path": "research/e8-bit-p111/code/nodeopt.py", + "supplier_git_blob": "dd30a2e4e6e33ba60669d7b421229a2f6e53d6ad" + }, + "research/e8-bit-p111-tuned/code/gen_p3.py": { + "sha256": "438b83f10d70ceca7cf78049420204b7de2dc61682f913c50a62596106ad84cd", + "base_git_blob": "ab21c9c19fc2386f273cd568b46282efcdd77fff", + "supplier_path": "research/e8-bit-p111/code/gen_p3.py", + "supplier_git_blob": "ab21c9c19fc2386f273cd568b46282efcdd77fff" + }, + "research/e8-bit-p111-tuned/tune/README.md": { + "sha256": "46c7917fb252949f38b7bcd88cf568efc282e3ea065b61d11e457e41673d0b2d", + "base_git_blob": "5b1554369682c8344d4f0767111d9b2b35eecbec" + }, + "research/e8-bit-p111-tuned/NOTICE.md": { + "sha256": "5b88eb2b7de76aa2a3288ee3c7a08d18a5eadfa82f5e7a99e207d232aed71221", + "base_git_blob": "b589500c8ae02a0a4c476e61dfdd1b79dcbf7cad" + }, + "research/r420-quad13/verify.py": { + "sha256": "cf46b382822c1323ac0d96561599b442d13f261c91c2d1c67245bf5c7aac8fe8", + "base_git_blob": "6721f8b461e68c2c51ca19c0861e6ae4b5b61d45" + }, + "research/r420-two-block-composition/native.py": { + "sha256": "2b7d0c5451c55dea8524a2bad04d347db2eb17fe7a8402f6814bb41206a4e0cb", + "base_git_blob": "84afab02a9f97e72b531d207241ee57f5c1ae525" + }, + "research/e8-bit-carrier-skeleton/code/bit/regression/stage_cohort.py": { + "sha256": "6c288f6f234b528c1a7c0a4adfb724e91e0fe6b18c8dffad96af3f973de1829a", + "base_git_blob": "f6d7afe3e623208c4207b6a683a1e3e49249e31c" + }, + "research/e8-bit-carrier-skeleton/code/bit/checkers/legality_h.cpp": { + "sha256": "6c1ef2b24e57781d6951c172a1024fc4300e6fd392c9d6672079a7806ab663b3", + "base_git_blob": "cb1233c7e96b1aa8bbf4d2e4165d75ab0dca64b9" + }, + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp": { + "sha256": "1c344d18fcd494eeca93e259f10cafae7705780e6592f6dcb35b34752dab9bc2", + "base_git_blob": "42bb232fbec4de703e70cc13dc2f39a3b43a3a01" + }, + "research/e8-bit-carrier-skeleton/code/bit/checkers/json.hpp": { + "sha256": "aaf127c04cb31c406e5b04a63f1ae89369fccde6d8fa7cdda1ed4f32dfc5de63", + "base_git_blob": "82d69f7c5d044c9887c96b90c97f5639083ecd14" + }, + "research/e8-bit-carrier-skeleton/portable-include/bits/stdc++.h": { + "sha256": "420094be2af295eed03a983dd66debbbe9cfb78d8252859f4498a615a0074b99", + "base_git_blob": "fc5664e929d9a81d9b4926bee049a93330be86ec" + } + } +} diff --git a/research/r439-block1-schedule/VALIDATION.md b/research/r439-block1-schedule/VALIDATION.md new file mode 100644 index 0000000000..c725579905 --- /dev/null +++ b/research/r439-block1-schedule/VALIDATION.md @@ -0,0 +1,73 @@ +# Executed validation + +Date: 2026-10-13. Base: +`f567884aeb8851b6e794af1184119a3bfbe1e631`. +Environment: Debian 13 x86_64, CPython **3.12.14**, GCC **14.2.0**. +All verification was performed by the same OpenAI Codex agent; no separate +human or delegated-agent review is claimed. + +## Completed + +- `python3 -I -B research/r439-block1-schedule/search.py` reproduces the entire + candidate and every distance: minima 14 + 16, 2,048 states, 10,240 + state/destination checks, 8,464 feasible edges. This is exhaustive only + in the two defined fixed-factor scheduling classes. +- `python3 -I -B research/r439-block1-schedule/verify.py` passes with 13 controls. + The same report also passes under `-O`. The verifier uses F2 donor elimination + and entrywise integer lifting; the nomination uses packed subset sums. + Integer matrices, all 1,024 local Boolean inputs, all 661 arbitrary columns, + E8 geometry, H1-H5 and the decomposed conclusion, actual record semantics, + frame paths, copied-centre lifecycle, complete costs and prefix bounds pass. +- `python3 -I -B research/r439-block1-schedule/check_package.py` passes from a + minimal relocated source tree without repository metadata, under `-I -B -O` + and with spaces in its path. Altered immutable source bytes, missing source + coverage, wrong physical wire binding, understated minimum and false receipt + saving are rejected at their expected checks. Existing output is preserved. +- `BOOST_INCLUDE=/tmp/r439-boost/usr/include python3 -I -B + research/r439-block1-schedule/native.py --write-receipt + --output /tmp/r439-block1-native-first` completed fresh native checking on + both words. The retained `NATIVE.json` records legality and all 5/9/11-stage + fields, except timing and temporary stream path. Both words cover + **883 / 1,327 / 1,549** formal columns and reject **6 / 18 / 24** omitted + bridges per stage configuration: **96** bridge controls in total. +- A second native run from a minimal source closure at a path containing spaces, + invoked outside the original checkout under `-I -B -O`, exactly matched the + retained receipt. Python and C++ positive prefixes and scalar counts agree. +- `make selected-record-check` passes at the exact base. The selected + certificate, all pre-existing tracked files and `upstream/` are unchanged. +- The four word/checker/generator files annotated in `SOURCES.json` were + compared directly to their original PR589 Git objects; all bytes agree. + +The native Boost dependency was absent initially. The Debian header package +`libboost1.83-dev_1.83.0-4.2_amd64.deb` was downloaded from +`https://deb.debian.org/debian/pool/main/b/boost1.83/` and extracted into `/tmp`, +without changing system packages. Download SHA256: +`1f11fc6fb2ffe9378a0f0ebc8f2fd9223fb958b4a40bb9381c67a8857d947ca3`. +This is an environment dependency, not a mathematical source certificate. + +## Corrections during development + +The initial exploratory split guessed 19 + 16 gates. Checking the actual +positive factor maps exposed entries greater than one in that first prefix. +The generator's true upper/lower boundary is 14 + 21; both factor maps are +binary with unit diagonal there. All published nomination and verification +use that fixed boundary. This was corrected before any candidate was accepted; +no failed search or optimum is inferred from the rejected exploratory split. + +## Limits + +No repository-wide regenerating `make verify`, cold reconstruction of the +supplier, new hosted-parent program/invoice, outer assembly, Lean proof or +remote CI run is claimed. Those constructions and generators were not changed. +The native checkers' signed lift and finite F2 endpoints do not discharge the +inherited signed decoder, all-size, realization, hosting, precision/tape and +analytic obligations. No unrestricted circuit minimum or improved kappa. + +Metadata was refreshed through PR874, including concurrent PR873's distinct +frame-508 block. Main was still the exact base. GitHub denied fork creation +with HTTP 403 `Resource not accessible by integration`; the first handoff was +a local commit and patch. The contributor subsequently created the fork, and +the verified branch was pushed successfully. Upstream PR creation through both +the CLI and connected app still returned HTTP 403; no PR or hosted-CI success +is claimed. Publication-time overlap was refreshed through PR876 without a +matching block-1 contribution; main remained the exact base. diff --git a/research/r439-block1-schedule/check_package.py b/research/r439-block1-schedule/check_package.py new file mode 100644 index 0000000000..b94262da5a --- /dev/null +++ b/research/r439-block1-schedule/check_package.py @@ -0,0 +1,78 @@ +"""Minimal-source relocation and corruption controls for this finite proof. + +Prepared for Krishnendu Purohit (@Deftsalt-debug) with substantial OpenAI Codex +assistance. Apache-2.0. No source tree mutations or third-party dependencies. +""" +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +RELATIVE = HERE.relative_to(ROOT) + + +def run(): + with tempfile.TemporaryDirectory(prefix="r439 package with spaces ") as tmp: + root = Path(tmp) / "checkout" + package = root / RELATIVE + shutil.copytree(HERE, package, ignore=shutil.ignore_patterns("__pycache__")) + pins = json.loads((HERE / "SOURCES.json").read_text()) + for name in pins["files"]: + path = root / name + path.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / name, path) + command = [sys.executable, "-I", "-B", "-O", str(package / "verify.py")] + + def call(extra=(), reason=None): + proc = subprocess.run(command + list(extra), cwd=tmp, text=True, capture_output=True) + output = proc.stdout + proc.stderr + if reason is None: + if proc.returncode or "PASS_R439_BLOCK1_SCHEDULE" not in output: + raise RuntimeError("relocated verifier failed: " + output) + elif not proc.returncode or reason not in output: + raise RuntimeError("wrong corruption outcome for " + reason + ": " + output) + + def corrupt(path, change, reason): + saved = path.read_bytes() + try: + change(path) + call(reason=reason) + finally: + path.write_bytes(saved) + + def change_json(path, change): + value = json.loads(path.read_text()) + change(value) + path.write_text(json.dumps(value) + "\n") + + call() + corrupt(root / pins["execution_inputs"][0], + lambda p: p.write_bytes(p.read_bytes() + b"\n"), "source hash mismatch") + corrupt(package / "SOURCES.json", + lambda p: change_json(p, lambda d: d.update(execution_inputs=[])), + "source pin coverage mismatch") + corrupt(package / "CANDIDATE.json", + lambda p: change_json(p, lambda d: d["registers"].reverse()), + "unexpected circuit registers") + corrupt(package / "CANDIDATE.json", + lambda p: change_json(p, lambda d: d["factors"][1].update(minimum=15)), + "minimum certificate mismatch") + corrupt(package / "CERTIFICATE.json", + lambda p: change_json(p, lambda d: d.update(saved_with_cleanup=11)), + "certificate mismatch") + occupied = root / "occupied" + occupied.mkdir() + sentinel = occupied / "sentinel" + sentinel.write_text("preserve me\n") + call(["--output", str(occupied)], "FileExistsError") + if sentinel.read_text() != "preserve me\n" or list(occupied.iterdir()) != [sentinel]: + raise RuntimeError("existing output was modified") + print("PASS_R439_BLOCK1_PACKAGE minimal_relocation=1 corruption_controls=5 output_preservation=1 optimized=1") + + +if __name__ == "__main__": + run() diff --git a/research/r439-block1-schedule/native.py b/research/r439-block1-schedule/native.py new file mode 100644 index 0000000000..43bbf5ebb5 --- /dev/null +++ b/research/r439-block1-schedule/native.py @@ -0,0 +1,124 @@ +"""Fresh unchanged native legality and 5/9/11-stage checks for both words. + +Adapted from Ali Romman / PR688's r420-two-block-composition/native.py, +originally prepared with substantial OpenAI Codex assistance. +Prepared for Krishnendu Purohit (@Deftsalt-debug) with substantial OpenAI Codex +assistance. Apache-2.0. Needs C++17 and Boost headers (BOOST_INCLUDE). +""" +import argparse +import importlib.util +import json +import os +from pathlib import Path +import shlex +import subprocess +import sys +import tempfile + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("block_verifier", HERE / "verify.py") +verify = importlib.util.module_from_spec(spec) +spec.loader.exec_module(verify) + + +def run(out, write): + pins = json.loads((HERE / "SOURCES.json").read_text()) + package = verify.ROOT / "research/e8-bit-carrier-skeleton" + bit = package / "code/bit" + checkers = bit / "checkers" + required = [str(p.relative_to(verify.ROOT)) for p in + (bit / "regression/stage_cohort.py", checkers / "legality_h.cpp", + checkers / "columns_k.cpp", checkers / "json.hpp", + package / "portable-include/bits/stdc++.h")] + verify.need(pins["native_inputs"] == required, "native input coverage mismatch") + for path in required: + verify.need(verify.sha((verify.ROOT / path).read_bytes()) == pins["files"][path]["sha256"], + "native source hash mismatch: " + path) + local = out / "local" + local.mkdir() + verify.run(local, False) + compiler = shlex.split(os.environ.get("CXX", "c++")) + include = os.environ.get("BOOST_INCLUDE", "/usr/include") + flags = ["-O2", "-std=c++17", "-DHDIM=8", "-DNCOPY=9", "-DVPORTS=111", "-DRHELP=439", + "-I" + str(package / "portable-include"), "-I" + str(checkers), "-I" + include] + bindir = out / "bin" + bindir.mkdir() + + def call(name, command): + with (out / (name + ".log")).open("w") as log: + subprocess.run(list(map(str, command)), check=True, stdout=log, stderr=subprocess.STDOUT) + + def receipt(path): + data = json.loads(path.read_text()) + # Only execution time and the temporary absolute stream pathname vary. + data.pop("seconds", None) + data.pop("local_scalar_stream", None) + return data + + call("compile-legality", compiler + flags + ["-o", bindir / "legality", checkers / "legality_h.cpp"]) + for pairs in (2, 4, 5): + call("compile-columns" + str(pairs), compiler + flags + ["-DKPAIRS=" + str(pairs), "-o", + bindir / ("columns" + str(pairs)), checkers / "columns_k.cpp"]) + results = {} + for name in ("original", "replacement"): + records = local / name + base = out / name + cin, cout = base / "cin", base / "cout" + call(name + "-cohort", [sys.executable, "-I", "-B", bit / "regression/stage_cohort.py", + records, records, cin, cout]) + call(name + "-legality", [bindir / "legality", cin, cout, cout / "legality.json"]) + legality = receipt(cout / "legality.json") + verify.need(legality["status"] == "PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE", + "native legality did not pass") + verify.need(legality["rank_mass"] == 5129 and legality["copies"] == legality["erasures"] == 9, + "native legality price mismatch") + results[name] = {"legality": legality, "stages": {}} + for pairs in (2, 4, 5): + path = cout / ("columns" + str(pairs) + ".json") + call(name + "-columns" + str(pairs), [bindir / ("columns" + str(pairs)), + cout / "COHORT249-RECORDS.bin", path]) + data = receipt(path) + status = ("PASS_NEW_COHORT249_ALL_FIVE_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" if pairs == 2 else + "PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL") + verify.need(data["status"] == status, "native columns did not pass") + verify.need(data["formal_columns_checked"] == 222 * pairs + 439, "column coverage mismatch") + controls = data["negative_controls"] + verify.need(len(controls) == 6 * (pairs - 1) and all(c["rejected"] for c in controls), + "native bridge control failed") + expected = json.loads((HERE / "CERTIFICATE.json").read_text())["native_records"][name] + verify.need(data["local_scalar_additions"] == expected["adds"] and + data["payload_prefix_upper"] == expected["payload_prefix_upper"] and + [int(x["cancellation_free_signed_row_l1_upper"]) for x in data["signed_lift_prefix"]] + == expected["positive_prefix"], "native/Python prefix or count mismatch") + results[name]["stages"][str(2 * pairs + 1)] = data + for stages in ("5", "9", "11"): + old, new = (results[name]["stages"][stages] for name in ("original", "replacement")) + verify.need(old["local_raw_H"] == new["local_raw_H"] and + old["local_scalar_additions"] - new["local_scalar_additions"] == 10, + "native paid profile or saving mismatch") + verify.need(int(new["payload_prefix_upper"]) <= int(old["payload_prefix_upper"]), + "native prefix increased") + path = HERE / "NATIVE.json" + if write: + path.write_text(json.dumps(results, indent=2, sort_keys=True) + "\n") + else: + verify.need(results == json.loads(path.read_text()), "native receipt mismatch") + print("PASS_R439_BLOCK1_NATIVE words=2 stages=5,9,11 columns=883,1327,1549 bridge_controls=96") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="fresh directory for logs and execution artifacts") + parser.add_argument("--write-receipt", action="store_true") + args = parser.parse_args() + if args.output: + args.output.mkdir(parents=True, exist_ok=False) + run(args.output.resolve(), args.write_receipt) + else: + with tempfile.TemporaryDirectory(prefix="r439-block1-native-") as temporary: + run(Path(temporary), args.write_receipt) + + +if __name__ == "__main__": + main() diff --git a/research/r439-block1-schedule/search.py b/research/r439-block1-schedule/search.py new file mode 100644 index 0000000000..481cbdac81 --- /dev/null +++ b/research/r439-block1-schedule/search.py @@ -0,0 +1,120 @@ +"""Exact nomination in two destination-once positive-addition classes. + +Prepared for @Deftsalt-debug with substantial OpenAI Codex assistance. +Apache-2.0. Related fixed-factor scheduling: PR789 and PR844; no code imported. +""" +import argparse +import gzip +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WORD = ROOT / "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz" +REGS = [0, 3, 11, 61, 62, 63, 68, 69, 72, 465] +N = len(REGS) + + +def matrix(gates): + rows = [[int(i == j) for j in range(N)] for i in range(N)] + for d, s in gates: + rows[d] = [a + b for a, b in zip(rows[d], rows[s])] + return rows + + +def solve(target): + """State S: rows in S are final; every other row is its input unit. + + An edge finalizes r by adding a subset of the other current rows. Positive + coefficients and a diagonal of one prohibit repeated donors: each current + row has its own diagonal one, and all targets here are zero/one matrices. + """ + if any(x not in (0, 1) for row in target for x in row): + raise ValueError("this search class requires binary positive targets") + if any(target[i][i] != 1 for i in range(N)): + raise ValueError("non-unit diagonal") + base = N + 1 # no carry even for the sum of all N binary rows + unit = [base ** i for i in range(N)] + packed = [sum(x * b for x, b in zip(row, unit)) for row in target] + distance = [10**9] * (1 << N) + parent = [None] * (1 << N) + distance[0] = 0 + edges = 0 + reachable = 0 + for state in range(1 << N): + if distance[state] == 10**9: + continue + reachable += 1 + current = [packed[i] if state >> i & 1 else unit[i] for i in range(N)] + sums = [0] * (1 << N) + by_sum = {} + for donors in range(1 << N): + if donors: + bit = donors & -donors + sums[donors] = sums[donors ^ bit] + current[bit.bit_length() - 1] + by_sum.setdefault(sums[donors], []).append(donors) + for r in range(N): + if state >> r & 1: + continue + choices = [d for d in by_sum.get(packed[r] - unit[r], []) if not d >> r & 1] + if not choices: + continue + donors = min(choices, key=lambda d: (d.bit_count(), d)) + edges += 1 + nxt = state | (1 << r) + cost = distance[state] + donors.bit_count() + if cost < distance[nxt]: + distance[nxt] = cost + parent[nxt] = (state, r, donors) + if parent[-1] is None: + raise ValueError("no schedule in the nominated class") + batches = [] + state = (1 << N) - 1 + while state: + prev, r, donors = parent[state] + batches.append((r, [s for s in range(N) if donors >> s & 1])) + state = prev + batches.reverse() + gates = [[r, s] for r, donors in batches for s in donors] + if matrix(gates) != target: + raise ValueError("nomination endpoint failed") + return {"minimum": distance[-1], "reachable_states": reachable, + "reachable_edges": edges, "batches": batches, "gates": gates, + "distance": [None if d == 10**9 else d for d in distance]} + + +def nominate(): + word = json.loads(gzip.decompress(WORD.read_bytes())) + original = [[REGS.index(d), REGS.index(ss[0])] for f, d, ss in word["B"][128:163] + if f == 507 and len(ss) == 1] + if len(original) != 35: + raise ValueError("wrong block") + factors = [solve(matrix(original[:14])), solve(matrix(original[14:]))] + new = [g for factor in factors for g in factor["gates"]] + reverse_old = matrix(original[::-1]) + reverse_new = matrix(new[::-1]) + dominated = all(b <= a for x, y in zip(reverse_old, reverse_new) for a, b in zip(x, y)) + return {"block": 1, "phase": "B", "start": 128, "stop": 163, "frame": 507, + "registers": REGS, "split": 14, "original": original, "replacement": new, + "factors": factors, "reverse_dominated": dominated, + "source_sha256": hashlib.sha256(WORD.read_bytes()).hexdigest()} + + +def main(): + p = argparse.ArgumentParser(description=__doc__) + p.add_argument("--write", action="store_true") + args = p.parse_args() + result = nominate() + path = HERE / "CANDIDATE.json" + if args.write: + path.write_text(json.dumps(result, indent=2) + "\n") + elif json.loads(path.read_text()) != json.loads(json.dumps(result)): + raise ValueError("candidate does not match exhaustive nomination") + print("PASS_R439_BLOCK1_SEARCH", "gates=35->" + str(len(result["replacement"])), + "minima=" + "+".join(str(f["minimum"]) for f in result["factors"]), + "reverse_dominated=" + str(result["reverse_dominated"])) + + +if __name__ == "__main__": + main() diff --git a/research/r439-block1-schedule/verify.py b/research/r439-block1-schedule/verify.py new file mode 100644 index 0000000000..1ef1dad266 --- /dev/null +++ b/research/r439-block1-schedule/verify.py @@ -0,0 +1,406 @@ +"""Exact finite punctured-block replacement and native-word checks; no new rate claim. + +Adapted from mtpsl / PR691 verifier structure, originally prepared with +substantial OpenAI Codex assistance, Apache-2.0. +Prepared for Krishnendu Purohit (@Deftsalt-debug) with substantial OpenAI Codex assistance. +Python 3.10+, standard library only. No assertions are used for acceptance. +""" +import argparse +from collections import Counter +import copy +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path +import struct +import subprocess +import sys +import tempfile + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WORD = "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz" +AUDITOR = "research/e8-bit-p111-tuned/code/xcheck_p.py" +EXPORTER = "research/e8-bit-carrier-skeleton/code/bit/export_records.py" +EXECUTION_INPUTS = [WORD, AUDITOR, EXPORTER] + + +class Reject(Exception): + pass + + +def need(condition, reason): + if not condition: + raise Reject(reason) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def matrix(ops, positive=False): + # Each column is evolved separately; search.py evolves whole rows. + cols = [] + for j in range(10): + values = [int(i == j) for i in range(10)] + for d, s in ops: + need(type(d) is int and type(s) is int and 0 <= d < 10 and + 0 <= s < 10 and d != s, "invalid circuit gate") + values[d] = values[d] + values[s] if positive else values[d] ^ values[s] + cols.append(values) + return [list(r) for r in zip(*cols)] + + +def circuit_check(old, new): + need(matrix(old) == matrix(new), "circuit F2 map changed") + positive = {} + for direction, a, b in (("forward", old, new), ("reverse", old[::-1], new[::-1])): + before, after = matrix(a, True), matrix(b, True) + need(all(y <= x for rr, ss in zip(before, after) for x, y in zip(rr, ss)), + direction + " positive matrix increased") + positive[direction] = {"original": before, "replacement": after} + return positive + + +def optimality(recipe): + """Independent of nomination: solve each donor equation by F2 elimination, + then check its lift entry by entry over Z. No packed subset sums imported. + + Every reachable current matrix is invertible, since its path consists of + elementary row additions. Thus the F2 donor subset is unique. The positive + binary target and unit diagonal forbid repeated donors in any exact Z sum. + """ + need(recipe["split"] == 14, "wrong factor boundary") + need(len(recipe["factors"]) == 2, "wrong factor coverage") + results, combined = [], [] + for old, recorded in zip((recipe["original"][:14], recipe["original"][14:]), recipe["factors"]): + target = matrix(old, True) + need(all(x in (0, 1) for row in target for x in row) and + all(target[i][i] == 1 for i in range(10)), "factor outside binary unit-diagonal class") + rows = [sum(x << j for j, x in enumerate(row)) for row in target] + distance = [None] * 1024 + distance[0] = 0 + edges = 0 + attempts = 0 + for state in range(1024): + if distance[state] is None: + continue + current = [rows[i] if state >> i & 1 else 1 << i for i in range(10)] + basis = {} + for i, value in enumerate(current): + expression = 1 << i + while value: + p = value.bit_length() - 1 + if p not in basis: + basis[p] = (value, expression) + break + v, e = basis[p] + value ^= v + expression ^= e + need(value != 0, "reachable donor matrix is singular") + for r in range(10): + if state >> r & 1: + continue + attempts += 1 + value = rows[r] ^ (1 << r) + donors = 0 + while value: + p = value.bit_length() - 1 + v, e = basis[p] + value ^= v + donors ^= e + if donors >> r & 1: + continue + actual = [sum((current[s] >> j) & 1 for s in range(10) if donors >> s & 1) + for j in range(10)] + if actual != [target[r][j] - int(j == r) for j in range(10)]: + continue + edges += 1 + nxt = state | (1 << r) + candidate = distance[state] + donors.bit_count() + if distance[nxt] is None or candidate < distance[nxt]: + distance[nxt] = candidate + need(distance == recorded["distance"], "distance certificate mismatch") + need(distance[-1] == recorded["minimum"], "minimum certificate mismatch") + need(sum(d is not None for d in distance) == recorded["reachable_states"] and + edges == recorded["reachable_edges"], "state/edge coverage mismatch") + batches = recorded["batches"] + need(len(batches) == 10 and sorted(r for r, _ in batches) == list(range(10)), + "not a destination-once schedule") + gates = [[r, s] for r, donors in batches for s in donors] + need(gates == recorded["gates"] and len(gates) == distance[-1] and + matrix(gates, True) == target, "schedule fails to attain minimum") + combined.extend(gates) + results.append({"minimum": distance[-1], "states": sum(d is not None for d in distance), + "state_destination_checks": attempts, "feasible_edges": edges, + "distance_sha256": sha(canonical(distance))}) + need(combined == recipe["replacement"], "replacement differs from factor schedules") + return results + + +def cleanup(w): + return [[1, d, list(ss)] for _, d, ss in reversed(w["A"] + w["B"]) + if not 111 <= d < 222] + + +def build(base, recipe): + need((recipe["phase"], recipe["start"], recipe["stop"], recipe["frame"], recipe["block"]) + == ("B", 128, 163, 507, 1), "unexpected circuit location") + regs = recipe["registers"] + need(regs == [0, 3, 11, 61, 62, 63, 68, 69, 72, 465], "unexpected circuit registers") + original = [[507, regs[d], [regs[s]]] for d, s in recipe["original"]] + need(base["B"][128:163] == original, "original gate slice mismatch") + circuit_check(recipe["original"], recipe["replacement"]) + out = copy.deepcopy(base) + out["B"][128:163] = [[507, regs[d], [regs[s]]] for d, s in recipe["replacement"]] + out["C"] = cleanup(out) + return out + + +def paths(w): + result = [[f] for f in w["start"]] + for sec in ("D", "A", "B", "C"): + for f, d, ss in w[sec]: + for r in [d] + ss: + if result[r][-1] != f: + result[r].append(f) + for r, f in enumerate(w["final"]): + if result[r][-1] != f: + result[r].append(f) + return result + + +def audit(w, module, geometry): + # Geometry is unchanged; reuse the baseline's already checked exact spaces. + obj = copy.copy(geometry) + obj.w = w + result = obj.full() + h, c, _ = obj.interface() + need(all(h.values()) and all(c.values()), "interface H1-H5 or decomposition failed") + return result + + +def records_check(directory, word): + """Independent set-valued interpreter of the actual exported instructions. + + This checks the scalar projection and literal MOVE/COPY/ERASE lifecycle, + not the multistage formal-column or hosted-recursion contracts. + """ + raw = (directory / "249-records.bin").read_bytes() + need(len(raw) % 24 == 0, "truncated record") + records = list(struct.iter_unpack("<6i", raw)) + dim = {int(k): v["dim"] for k, v in + json.loads((directory / "frames.json").read_text())["frames"].items()} + frames = list(word["start"]) + [None] + values = [{i} for i in range(661)] + [set()] + pths = [[f] for f in frames[:661]] + hist, counts = Counter(), Counter() + for op, a, b, c, d, e in records: + counts[op] += 1 + if op == 0: + need(a < 661 and frames[a] == b and dim[c] - dim[b] == d and d > 0, + "bad MOVE") + need(set(word["frames"][b]) <= set(word["frames"][c]), "MOVE not nested") + frames[a] = c + pths[a].append(c) + hist[d] += 1 + elif op == 1: + need(a != b and c == 1 and frames[a] == frames[b] == d, "bad ADD frame") + values[a] = values[a].symmetric_difference(values[b]) + elif op == 2: + need(b == 661 and not values[b] and frames[b] is None and frames[a] == c, + "COPY lifecycle") + need(d == 0 and e == dim[c], "COPY rank") + values[b] = set(values[a]) + frames[b] = d + hist[e] += 1 + elif op == 3: + need(b == 661 and frames[a] == c and frames[b] == d == 0 + and values[b] == values[a], "ERASE lifecycle") + values[b] = set() + frames[b] = None + else: + raise Reject("unknown record opcode") + expected = [{i} if not 111 <= i < 222 else {i, i - 111} for i in range(661)] + need(values[:661] == expected and not values[661], "record dirty-column endpoint") + need(frames[:661] == word["final"] and frames[661] is None, "record frame endpoint") + need(pths == paths(word), "record frame paths differ") + prefix = [] + for reverse in (False, True): + norms = [1] * 661 + [0] + maximum = 1 + opened = False + for op, a, b, c, d, e in (reversed(records) if reverse else records): + if reverse and op in (2, 3): + op = 5 - op + if op == 1: + norms[a] += abs(c) * norms[b] + maximum = max(maximum, norms[a]) + elif op == 2: + need(not opened, "prefix COPY lifecycle") + norms[b], opened = norms[a], True + elif op == 3: + need(opened, "prefix ERASE lifecycle") + norms[b], opened = 0, False + need(not opened, "prefix open copy") + prefix.append(maximum) + payload = 64 * prefix[0] ** 3 * prefix[1] ** 2 + need(payload < 2**104, "native payload cap exceeded") + return {"records": len(records), "adds": counts[1], "moves": counts[0], + "copies": counts[2], "erasures": counts[3], + "paid_histogram": dict(sorted(hist.items())), + "rank_mass": sum(k * v for k, v in hist.items()), + "records_sha256": sha(raw), "positive_prefix": prefix, + "payload_prefix_upper": str(payload), "payload_prefix_bits": payload.bit_length()} + + +def rejected(label, fn, exceptions): + try: + fn() + except exceptions: + return label + raise Reject("negative control accepted: " + label) + + +def run(output, write_certificate): + pins = json.loads((HERE / "SOURCES.json").read_text()) + need(pins["execution_inputs"] == EXECUTION_INPUTS, "source pin coverage mismatch") + for path in pins["execution_inputs"]: + pin = pins["files"][path] + need(sha((ROOT / path).read_bytes()) == pin["sha256"], "source hash mismatch: " + path) + base = json.loads(gzip.decompress((ROOT / WORD).read_bytes())) + recipe = json.loads((HERE / "CANDIDATE.json").read_text()) + need(recipe["source_sha256"] == sha((ROOT / WORD).read_bytes()), "candidate source mismatch") + need(recipe["reverse_dominated"] is True, "candidate dominance claim mismatch") + factor_report = optimality(recipe) + revised = build(base, recipe) + positive = circuit_check(recipe["original"], recipe["replacement"]) + need(positive["forward"]["original"] == positive["forward"]["replacement"], + "integer forward map changed") + need(paths(base) == paths(revised), "physical frame path changed") + + spec = importlib.util.spec_from_file_location("predecessor_xcheck_p", ROOT / AUDITOR) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + geometry, labels, baseline, h, c, _ = module.check(base) + need(all(h.values()) and all(c.values()), "baseline interface failed") + revised_audit = audit(revised, module, geometry) + + # Independent exhaustive evaluation of the ten-register Boolean map. + for bits in range(1024): + endings = [] + for gates in (recipe["original"], recipe["replacement"]): + value = bits + for d, s in gates: + value ^= ((value >> s) & 1) << d + endings.append(value) + need(endings[0] == endings[1], "exhaustive ten-bit map differs") + + evidence = {} + for name, word in (("original", base), ("replacement", revised)): + path = output / (name + ".json") + path.write_text(json.dumps(word, separators=(",", ":")) + "\n") + directory = output / name + subprocess.run([sys.executable, "-B", str(ROOT / EXPORTER), str(path), str(directory)], + check=True, capture_output=True, text=True) + evidence[name] = records_check(directory, word) + a, b = evidence["original"], evidence["replacement"] + need(a["adds"] == 24305 and b["adds"] == 24295, "unexpected native ADD count") + for key in ("moves", "copies", "erasures", "paid_histogram", "rank_mass"): + need(a[key] == b[key], "native cost changed: " + key) + need(b["rank_mass"] == 5129 and b["copies"] == 9, "incorrect native cost") + need(all(y <= x for x, y in zip(a["positive_prefix"], b["positive_prefix"])), + "complete positive prefix increased") + + controls = [] + fail = (Reject, module.Reject) + for label, mutate in ( + ("understated factor minimum", lambda r: r["factors"][1].update(minimum=15)), + ("altered distance potential", lambda r: r["factors"][0]["distance"].__setitem__(1, 1)), + ("missing factor", lambda r: r["factors"].pop()), + ): + wrong = copy.deepcopy(recipe) + mutate(wrong) + controls.append(rejected(label, lambda: optimality(wrong), fail)) + controls.append(rejected("self addition", lambda: matrix([[0, 0]]), fail)) + controls.append(rejected("boolean register index", lambda: matrix([[True, 0]]), fail)) + controls.append(rejected("drop circuit gate", lambda: circuit_check( + recipe["original"], recipe["replacement"][1:]), fail)) + wrong = copy.deepcopy(recipe["replacement"]) + wrong[0].reverse() + controls.append(rejected("reverse circuit operand", lambda: circuit_check( + recipe["original"], wrong), fail)) + inflated = recipe["replacement"] + [[0, 1], [0, 1]] + need(matrix(inflated) == matrix(recipe["replacement"]), "inflation control is not F2-neutral") + controls.append(rejected("F2-neutral positive-cost inflation", lambda: circuit_check( + recipe["original"], inflated), fail)) + bad = copy.deepcopy(revised) + bad["C"].pop() + controls.append(rejected("dropped cleanup", lambda: audit(bad, module, geometry), fail)) + bad = copy.deepcopy(revised) + bad["C"] = copy.deepcopy(base["C"]) + # Same endpoint but not the literal reverse required by H4. + obj = copy.copy(geometry) + obj.w = bad + obj.full() + controls.append(rejected("nonliteral original cleanup", lambda: audit(bad, module, geometry), fail)) + bad = copy.deepcopy(revised) + bad["B"][128][0] = 0 + controls.append(rejected("illegal lower frame", lambda: audit(bad, module, geometry), fail)) + bad = copy.deepcopy(revised) + bad["D"][0][2].pop() + controls.append(rejected("missing dirty compensation", lambda: audit(bad, module, geometry), fail)) + + # The record endpoint checker must see literal instruction corruption too. + directory = output / "replacement" + rawpath = directory / "249-records.bin" + raw = rawpath.read_bytes() + recs = list(struct.iter_unpack("<6i", raw)) + for i, rec in enumerate(recs): + if rec[0] == 1 and rec[5] == 4 and rec[4] == 507: + rawpath.write_bytes(raw[:24*i] + raw[24*(i+1):]) + break + else: + raise Reject("negative control has no exported block ADD to remove") + try: + controls.append(rejected("dropped exported block ADD", lambda: records_check(directory, revised), fail)) + finally: + rawpath.write_bytes(raw) + + cert = {"status": "PASS_R439_BLOCK1_SCHEDULE", "block": 1, "old_gates": 35, "new_gates": 30, + "saved_with_cleanup": 10, "labels": labels, "columns": revised_audit["columns"], + "old_phase_gates": baseline["gates"], "new_phase_gates": revised_audit["gates"], + "boolean_inputs": 1024, "F2_matrix": matrix(recipe["replacement"]), + "positive_matrices": positive, "native_records": evidence, + "factor_optimality": factor_report, + "reconstructed_word_sha256": sha(canonical(revised)), "controls_rejected": controls, + "kappa_claim": "none; unchanged paid rank profile, no hosted replay"} + path = HERE / "CERTIFICATE.json" + if write_certificate: + path.write_text(json.dumps(cert, indent=2, sort_keys=True) + "\n") + else: + need(canonical(cert) == canonical(json.loads(path.read_text())), "certificate mismatch") + print("PASS_R439_BLOCK1_SCHEDULE gates=35->30 native_adds=24305->24295 columns=661 rank_mass=5129 controls=" + str(len(controls))) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="new directory for reconstructed word and records") + parser.add_argument("--write-certificate", action="store_true", help="regenerate this package's certificate") + args = parser.parse_args() + if args.output: + args.output.mkdir(parents=True, exist_ok=False) + run(args.output.resolve(), args.write_certificate) + else: + with tempfile.TemporaryDirectory(prefix="r439-block1-") as temporary: + run(Path(temporary), args.write_certificate) + + +if __name__ == "__main__": + main()