From d8c13a065a942018e41721f859dc97da5249a2e1 Mon Sep 17 00:00:00 2001 From: Yuzhou Wang Date: Tue, 13 Oct 2026 13:35:37 +0800 Subject: [PATCH 1/2] Research: certify exact R420 block-7 factor schedules --- .../CERTIFICATE.json | 8407 +++++++++++++++++ research/r420-block7-exact-schedule/CLAIM.md | 31 + .../r420-block7-exact-schedule/EXPECTED.json | 86 + .../r420-block7-exact-schedule/NATIVE.json | 51 + research/r420-block7-exact-schedule/README.md | 226 + .../r420-block7-exact-schedule/SOURCES.json | 27 + .../r420-block7-exact-schedule/VALIDATION.md | 77 + research/r420-block7-exact-schedule/native.py | 88 + .../r420-block7-exact-schedule/nominate.py | 85 + research/r420-block7-exact-schedule/verify.py | 327 + 10 files changed, 9405 insertions(+) create mode 100644 research/r420-block7-exact-schedule/CERTIFICATE.json create mode 100644 research/r420-block7-exact-schedule/CLAIM.md create mode 100644 research/r420-block7-exact-schedule/EXPECTED.json create mode 100644 research/r420-block7-exact-schedule/NATIVE.json create mode 100644 research/r420-block7-exact-schedule/README.md create mode 100644 research/r420-block7-exact-schedule/SOURCES.json create mode 100644 research/r420-block7-exact-schedule/VALIDATION.md create mode 100644 research/r420-block7-exact-schedule/native.py create mode 100644 research/r420-block7-exact-schedule/nominate.py create mode 100644 research/r420-block7-exact-schedule/verify.py diff --git a/research/r420-block7-exact-schedule/CERTIFICATE.json b/research/r420-block7-exact-schedule/CERTIFICATE.json new file mode 100644 index 0000000000..3b1ae51ab3 --- /dev/null +++ b/research/r420-block7-exact-schedule/CERTIFICATE.json @@ -0,0 +1,8407 @@ +{ + "block": 7, + "factors": [ + { + "batches": [ + [ + 11, + [ + 0 + ] + ], + [ + 0, + [ + 1 + ] + ], + [ + 1, + [ + 2, + 9 + ] + ], + [ + 2, + [] + ], + [ + 3, + [ + 8 + ] + ], + [ + 4, + [] + ], + [ + 5, + [] + ], + [ + 7, + [ + 1, + 3, + 4, + 5, + 6, + 10 + ] + ], + [ + 6, + [ + 2, + 5 + ] + ], + [ + 8, + [ + 4 + ] + ], + [ + 9, + [] + ], + [ + 10, + [] + ] + ], + "feasible_state_destination_pairs": 20992, + "minimum": 14, + "original_gates": 17, + "potentials": [ + 0, + 1, + 2, + 3, + 0, + 1, + 2, + 3, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 0, + 1, + 2, + 3, + 0, + 1, + 2, + 3, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 0, + 1, + 2, + 3, + 0, + 1, + 2, + 3, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 0, + 1, + 2, + 3, + 0, + 1, + 2, + 3, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 0, + 1, + 2, + 3, + 0, + 1, + 2, + 3, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 0, + 1, + 2, + 3, + 0, + 1, + 2, + 3, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 0, + 1, + 2, + 3, + 0, + 1, + 2, + 3, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 0, + 1, + 2, + 3, + 0, + 1, + 2, + 3, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 0, + 1, + 2, + 3, + 0, + 1, + 2, + 3, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 0, + 1, + 2, + 3, + 0, + 1, + 2, + 3, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 0, + 1, + 2, + 3, + 0, + 1, + 2, + 3, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 0, + 1, + 2, + 3, + 0, + 1, + 2, + 3, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 0, + 1, + 2, + 3, + 0, + 1, + 2, + 3, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 0, + 1, + 2, + 3, + 0, + 1, + 2, + 3, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 0, + 1, + 2, + 3, + 0, + 1, + 2, + 3, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 0, + 1, + 2, + 3, + 0, + 1, + 2, + 3, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 9, + 10, + 9, + 10, + 9, + 10, + 9, + 10, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 5, + 6, + 7, + 8, + 5, + 6, + 7, + 8, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 5, + 6, + 7, + 8, + 5, + 6, + 7, + 8, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 5, + 6, + 7, + 8, + 5, + 6, + 7, + 8, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 5, + 6, + 7, + 8, + 5, + 6, + 7, + 8, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 11, + 12, + 11, + 12, + 11, + 12, + 11, + 12, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 11, + 12, + 11, + 12, + 11, + 12, + 11, + 12, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 11, + 12, + 11, + 12, + 11, + 12, + 11, + 12, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 11, + 12, + 11, + 12, + 11, + 12, + 11, + 12, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 11, + 12, + 13, + 14, + 11, + 12, + 13, + 14, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 11, + 12, + 13, + 14, + 11, + 12, + 13, + 14, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 11, + 12, + 13, + 14, + 11, + 12, + 13, + 14, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 11, + 12, + 13, + 14, + 11, + 12, + 13, + 14, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 5, + 6, + 7, + 8, + 5, + 6, + 7, + 8, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 5, + 6, + 7, + 8, + 5, + 6, + 7, + 8, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 5, + 6, + 7, + 8, + 5, + 6, + 7, + 8, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 5, + 6, + 7, + 8, + 5, + 6, + 7, + 8, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 11, + 12, + 11, + 12, + 11, + 12, + 11, + 12, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 11, + 12, + 11, + 12, + 11, + 12, + 11, + 12, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 11, + 12, + 11, + 12, + 11, + 12, + 11, + 12, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 11, + 12, + 11, + 12, + 11, + 12, + 11, + 12, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 11, + 12, + 13, + 14, + 11, + 12, + 13, + 14, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 11, + 12, + 13, + 14, + 11, + 12, + 13, + 14, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 11, + 12, + 13, + 14, + 11, + 12, + 13, + 14, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 11, + 12, + 13, + 14, + 11, + 12, + 13, + 14, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 5, + 6, + 7, + 8, + 5, + 6, + 7, + 8, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 5, + 6, + 7, + 8, + 5, + 6, + 7, + 8, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 5, + 6, + 7, + 8, + 5, + 6, + 7, + 8, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 5, + 6, + 7, + 8, + 5, + 6, + 7, + 8, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 11, + 12, + 11, + 12, + 11, + 12, + 11, + 12, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 11, + 12, + 11, + 12, + 11, + 12, + 11, + 12, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 11, + 12, + 11, + 12, + 11, + 12, + 11, + 12, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 11, + 12, + 11, + 12, + 11, + 12, + 11, + 12, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 11, + 12, + 13, + 14, + 11, + 12, + 13, + 14, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 11, + 12, + 13, + 14, + 11, + 12, + 13, + 14, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 11, + 12, + 13, + 14, + 11, + 12, + 13, + 14, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 11, + 12, + 13, + 14, + 11, + 12, + 13, + 14, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 1, + 2, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 3, + 4, + 5, + 6, + 3, + 4, + 5, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 5, + 6, + 7, + 8, + 5, + 6, + 7, + 8, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 5, + 6, + 7, + 8, + 5, + 6, + 7, + 8, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 5, + 6, + 7, + 8, + 5, + 6, + 7, + 8, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 5, + 6, + 7, + 8, + 5, + 6, + 7, + 8, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 11, + 12, + 11, + 12, + 11, + 12, + 11, + 12, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 11, + 12, + 11, + 12, + 11, + 12, + 11, + 12, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 11, + 12, + 11, + 12, + 11, + 12, + 11, + 12, + 10, + 11, + 10, + 11, + 10, + 11, + 10, + 11, + 11, + 12, + 11, + 12, + 11, + 12, + 11, + 12, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 11, + 12, + 13, + 14, + 11, + 12, + 13, + 14, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 11, + 12, + 13, + 14, + 11, + 12, + 13, + 14, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 11, + 12, + 13, + 14, + 11, + 12, + 13, + 14, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 11, + 12, + 13, + 14, + 11, + 12, + 13, + 14 + ], + "rows": [ + 3, + 518, + 4, + 264, + 16, + 32, + 100, + 2046, + 272, + 512, + 1024, + 2049 + ] + }, + { + "batches": [ + [ + 0, + [ + 7 + ] + ], + [ + 10, + [ + 0, + 11 + ] + ], + [ + 11, + [ + 7 + ] + ], + [ + 1, + [ + 11 + ] + ], + [ + 2, + [ + 11 + ] + ], + [ + 3, + [ + 11 + ] + ], + [ + 4, + [ + 11 + ] + ], + [ + 9, + [ + 5, + 11 + ] + ], + [ + 5, + [ + 3, + 8 + ] + ], + [ + 6, + [ + 11 + ] + ], + [ + 7, + [] + ], + [ + 8, + [ + 11 + ] + ] + ], + "feasible_state_destination_pairs": 22528, + "minimum": 14, + "original_gates": 24, + "potentials": [ + 0, + 1, + 2, + 3, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 4, + 5, + 6, + 7, + 2, + 3, + 4, + 5, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 6, + 7, + 8, + 9, + 4, + 5, + 6, + 7, + 6, + 7, + 8, + 9, + 4, + 5, + 6, + 7, + 6, + 7, + 8, + 9, + 6, + 7, + 8, + 9, + 8, + 9, + 10, + 11, + 6, + 7, + 8, + 9, + 8, + 9, + 10, + 11, + 2, + 3, + 4, + 5, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 6, + 7, + 8, + 9, + 4, + 5, + 6, + 7, + 6, + 7, + 8, + 9, + 6, + 7, + 8, + 9, + 8, + 9, + 10, + 11, + 6, + 7, + 8, + 9, + 8, + 9, + 10, + 11, + 6, + 7, + 8, + 9, + 8, + 9, + 10, + 11, + 8, + 9, + 10, + 11, + 10, + 11, + 12, + 13, + 8, + 9, + 10, + 11, + 10, + 11, + 12, + 13, + 0, + 1, + 2, + 3, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 4, + 5, + 6, + 7, + 2, + 3, + 4, + 5, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 6, + 7, + 8, + 9, + 4, + 5, + 6, + 7, + 6, + 7, + 8, + 9, + 4, + 5, + 6, + 7, + 6, + 7, + 8, + 9, + 6, + 7, + 8, + 9, + 8, + 9, + 10, + 11, + 6, + 7, + 8, + 9, + 8, + 9, + 10, + 11, + 2, + 3, + 4, + 5, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 6, + 7, + 8, + 9, + 4, + 5, + 6, + 7, + 6, + 7, + 8, + 9, + 6, + 7, + 8, + 9, + 8, + 9, + 10, + 11, + 6, + 7, + 8, + 9, + 8, + 9, + 10, + 11, + 6, + 7, + 8, + 9, + 8, + 9, + 10, + 11, + 8, + 9, + 10, + 11, + 10, + 11, + 12, + 13, + 8, + 9, + 10, + 11, + 10, + 11, + 12, + 13, + 2, + 3, + 4, + 5, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 6, + 7, + 8, + 9, + 4, + 5, + 6, + 7, + 6, + 7, + 8, + 9, + 6, + 7, + 8, + 9, + 8, + 9, + 10, + 11, + 4, + 5, + 6, + 7, + 6, + 7, + 8, + 9, + 6, + 7, + 8, + 9, + 8, + 9, + 10, + 11, + 6, + 7, + 8, + 9, + 8, + 9, + 10, + 11, + 8, + 9, + 10, + 11, + 10, + 11, + 12, + 13, + 4, + 5, + 6, + 7, + 6, + 7, + 8, + 9, + 6, + 7, + 8, + 9, + 8, + 9, + 10, + 11, + 6, + 7, + 8, + 9, + 8, + 9, + 10, + 11, + 8, + 9, + 10, + 11, + 10, + 11, + 12, + 13, + 6, + 7, + 8, + 9, + 8, + 9, + 10, + 11, + 8, + 9, + 10, + 11, + 10, + 11, + 12, + 13, + 8, + 9, + 10, + 11, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 12, + 13, + 14, + 15, + 2, + 3, + 4, + 5, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 6, + 7, + 8, + 9, + 4, + 5, + 6, + 7, + 6, + 7, + 8, + 9, + 6, + 7, + 8, + 9, + 8, + 9, + 10, + 11, + 4, + 5, + 6, + 7, + 6, + 7, + 8, + 9, + 6, + 7, + 8, + 9, + 8, + 9, + 10, + 11, + 6, + 7, + 8, + 9, + 8, + 9, + 10, + 11, + 8, + 9, + 10, + 11, + 10, + 11, + 12, + 13, + 4, + 5, + 6, + 7, + 6, + 7, + 8, + 9, + 6, + 7, + 8, + 9, + 8, + 9, + 10, + 11, + 6, + 7, + 8, + 9, + 8, + 9, + 10, + 11, + 8, + 9, + 10, + 11, + 10, + 11, + 12, + 13, + 6, + 7, + 8, + 9, + 8, + 9, + 10, + 11, + 8, + 9, + 10, + 11, + 10, + 11, + 12, + 13, + 8, + 9, + 10, + 11, + 10, + 11, + 12, + 13, + 10, + 11, + 12, + 13, + 12, + 13, + 14, + 15, + 3, + 4, + 5, + 6, + 5, + 6, + 7, + 8, + 5, + 6, + 7, + 8, + 7, + 8, + 9, + 10, + 5, + 6, + 7, + 8, + 7, + 8, + 9, + 10, + 7, + 8, + 9, + 10, + 9, + 10, + 11, + 12, + 7, + 8, + 9, + 10, + 9, + 10, + 11, + 12, + 7, + 8, + 9, + 10, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 11, + 12, + 13, + 14, + 9, + 10, + 11, + 12, + 11, + 12, + 13, + 14, + 5, + 6, + 7, + 8, + 7, + 8, + 9, + 10, + 7, + 8, + 9, + 10, + 9, + 10, + 11, + 12, + 7, + 8, + 9, + 10, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 11, + 12, + 13, + 14, + 9, + 10, + 11, + 12, + 11, + 12, + 13, + 14, + 9, + 10, + 11, + 12, + 11, + 12, + 13, + 14, + 11, + 12, + 13, + 14, + 13, + 14, + 15, + 16, + 11, + 12, + 13, + 14, + 13, + 14, + 15, + 16, + 3, + 4, + 5, + 6, + 5, + 6, + 7, + 8, + 5, + 6, + 7, + 8, + 7, + 8, + 9, + 10, + 5, + 6, + 7, + 8, + 7, + 8, + 9, + 10, + 7, + 8, + 9, + 10, + 9, + 10, + 11, + 12, + 7, + 8, + 9, + 10, + 9, + 10, + 11, + 12, + 7, + 8, + 9, + 10, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 11, + 12, + 13, + 14, + 9, + 10, + 11, + 12, + 11, + 12, + 13, + 14, + 5, + 6, + 7, + 8, + 7, + 8, + 9, + 10, + 7, + 8, + 9, + 10, + 9, + 10, + 11, + 12, + 7, + 8, + 9, + 10, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 11, + 12, + 13, + 14, + 9, + 10, + 11, + 12, + 11, + 12, + 13, + 14, + 9, + 10, + 11, + 12, + 11, + 12, + 13, + 14, + 11, + 12, + 13, + 14, + 13, + 14, + 15, + 16, + 11, + 12, + 13, + 14, + 13, + 14, + 15, + 16, + 5, + 6, + 7, + 8, + 7, + 8, + 9, + 10, + 7, + 8, + 9, + 10, + 9, + 10, + 11, + 12, + 7, + 8, + 9, + 10, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 11, + 12, + 13, + 14, + 7, + 8, + 9, + 10, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 11, + 12, + 13, + 14, + 9, + 10, + 11, + 12, + 11, + 12, + 13, + 14, + 11, + 12, + 13, + 14, + 13, + 14, + 15, + 16, + 7, + 8, + 9, + 10, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 11, + 12, + 13, + 14, + 9, + 10, + 11, + 12, + 11, + 12, + 13, + 14, + 11, + 12, + 13, + 14, + 13, + 14, + 15, + 16, + 9, + 10, + 11, + 12, + 11, + 12, + 13, + 14, + 11, + 12, + 13, + 14, + 13, + 14, + 15, + 16, + 11, + 12, + 13, + 14, + 13, + 14, + 15, + 16, + 13, + 14, + 15, + 16, + 15, + 16, + 17, + 18, + 5, + 6, + 7, + 8, + 7, + 8, + 9, + 10, + 7, + 8, + 9, + 10, + 9, + 10, + 11, + 12, + 7, + 8, + 9, + 10, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 11, + 12, + 13, + 14, + 7, + 8, + 9, + 10, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 11, + 12, + 13, + 14, + 9, + 10, + 11, + 12, + 11, + 12, + 13, + 14, + 11, + 12, + 13, + 14, + 13, + 14, + 15, + 16, + 7, + 8, + 9, + 10, + 9, + 10, + 11, + 12, + 9, + 10, + 11, + 12, + 11, + 12, + 13, + 14, + 9, + 10, + 11, + 12, + 11, + 12, + 13, + 14, + 11, + 12, + 13, + 14, + 13, + 14, + 15, + 16, + 9, + 10, + 11, + 12, + 11, + 12, + 13, + 14, + 11, + 12, + 13, + 14, + 13, + 14, + 15, + 16, + 11, + 12, + 13, + 14, + 13, + 14, + 15, + 16, + 13, + 14, + 15, + 16, + 15, + 16, + 17, + 18, + 3, + 3, + 5, + 5, + 5, + 5, + 7, + 7, + 5, + 5, + 7, + 7, + 7, + 7, + 9, + 9, + 5, + 5, + 7, + 7, + 7, + 7, + 9, + 9, + 7, + 7, + 9, + 9, + 9, + 9, + 11, + 11, + 7, + 7, + 9, + 9, + 9, + 9, + 11, + 11, + 7, + 7, + 9, + 9, + 9, + 9, + 11, + 11, + 9, + 9, + 11, + 11, + 11, + 11, + 13, + 13, + 9, + 9, + 11, + 11, + 11, + 11, + 13, + 13, + 5, + 5, + 7, + 7, + 7, + 7, + 9, + 9, + 7, + 7, + 9, + 9, + 9, + 9, + 11, + 11, + 7, + 7, + 9, + 9, + 9, + 9, + 11, + 11, + 9, + 9, + 11, + 11, + 11, + 11, + 13, + 13, + 9, + 9, + 11, + 11, + 11, + 11, + 13, + 13, + 9, + 9, + 11, + 11, + 11, + 11, + 13, + 13, + 11, + 11, + 13, + 13, + 13, + 13, + 15, + 15, + 11, + 11, + 13, + 13, + 13, + 13, + 15, + 15, + 3, + 3, + 5, + 5, + 5, + 5, + 7, + 7, + 5, + 5, + 7, + 7, + 7, + 7, + 9, + 9, + 5, + 5, + 7, + 7, + 7, + 7, + 9, + 9, + 7, + 7, + 9, + 9, + 9, + 9, + 11, + 11, + 7, + 7, + 9, + 9, + 9, + 9, + 11, + 11, + 7, + 7, + 9, + 9, + 9, + 9, + 11, + 11, + 9, + 9, + 11, + 11, + 11, + 11, + 13, + 13, + 9, + 9, + 11, + 11, + 11, + 11, + 13, + 13, + 5, + 5, + 7, + 7, + 7, + 7, + 9, + 9, + 7, + 7, + 9, + 9, + 9, + 9, + 11, + 11, + 7, + 7, + 9, + 9, + 9, + 9, + 11, + 11, + 9, + 9, + 11, + 11, + 11, + 11, + 13, + 13, + 9, + 9, + 11, + 11, + 11, + 11, + 13, + 13, + 9, + 9, + 11, + 11, + 11, + 11, + 13, + 13, + 11, + 11, + 13, + 13, + 13, + 13, + 15, + 15, + 11, + 11, + 13, + 13, + 13, + 13, + 15, + 15, + 5, + 5, + 7, + 7, + 7, + 7, + 9, + 9, + 7, + 7, + 9, + 9, + 9, + 9, + 11, + 11, + 7, + 7, + 9, + 9, + 9, + 9, + 11, + 11, + 9, + 9, + 11, + 11, + 11, + 11, + 13, + 13, + 7, + 7, + 9, + 9, + 9, + 9, + 11, + 11, + 9, + 9, + 11, + 11, + 11, + 11, + 13, + 13, + 9, + 9, + 11, + 11, + 11, + 11, + 13, + 13, + 11, + 11, + 13, + 13, + 13, + 13, + 15, + 15, + 7, + 7, + 9, + 9, + 9, + 9, + 11, + 11, + 9, + 9, + 11, + 11, + 11, + 11, + 13, + 13, + 9, + 9, + 11, + 11, + 11, + 11, + 13, + 13, + 11, + 11, + 13, + 13, + 13, + 13, + 15, + 15, + 9, + 9, + 11, + 11, + 11, + 11, + 13, + 13, + 11, + 11, + 13, + 13, + 13, + 13, + 15, + 15, + 11, + 11, + 13, + 13, + 13, + 13, + 15, + 15, + 13, + 13, + 15, + 15, + 15, + 15, + 17, + 17, + 5, + 5, + 7, + 7, + 7, + 7, + 9, + 9, + 7, + 7, + 9, + 9, + 9, + 9, + 11, + 11, + 7, + 7, + 9, + 9, + 9, + 9, + 11, + 11, + 9, + 9, + 11, + 11, + 11, + 11, + 13, + 13, + 7, + 7, + 9, + 9, + 9, + 9, + 11, + 11, + 9, + 9, + 11, + 11, + 11, + 11, + 13, + 13, + 9, + 9, + 11, + 11, + 11, + 11, + 13, + 13, + 11, + 11, + 13, + 13, + 13, + 13, + 15, + 15, + 7, + 7, + 9, + 9, + 9, + 9, + 11, + 11, + 9, + 9, + 11, + 11, + 11, + 11, + 13, + 13, + 9, + 9, + 11, + 11, + 11, + 11, + 13, + 13, + 11, + 11, + 13, + 13, + 13, + 13, + 15, + 15, + 9, + 9, + 11, + 11, + 11, + 11, + 13, + 13, + 11, + 11, + 13, + 13, + 13, + 13, + 15, + 15, + 11, + 11, + 13, + 13, + 13, + 13, + 15, + 15, + 13, + 13, + 15, + 15, + 15, + 15, + 17, + 17, + 6, + 6, + 8, + 8, + 8, + 8, + 10, + 10, + 8, + 8, + 10, + 10, + 10, + 10, + 12, + 12, + 8, + 8, + 10, + 10, + 10, + 10, + 12, + 12, + 10, + 10, + 12, + 12, + 12, + 12, + 14, + 14, + 10, + 10, + 12, + 12, + 12, + 12, + 14, + 14, + 10, + 10, + 12, + 12, + 12, + 12, + 14, + 14, + 12, + 12, + 14, + 14, + 14, + 14, + 16, + 16, + 12, + 12, + 14, + 14, + 14, + 14, + 16, + 16, + 8, + 8, + 10, + 10, + 10, + 10, + 12, + 12, + 10, + 10, + 12, + 12, + 12, + 12, + 14, + 14, + 10, + 10, + 12, + 12, + 12, + 12, + 14, + 14, + 12, + 12, + 14, + 14, + 14, + 14, + 16, + 16, + 12, + 12, + 14, + 14, + 14, + 14, + 16, + 16, + 12, + 12, + 14, + 14, + 14, + 14, + 16, + 16, + 14, + 14, + 16, + 16, + 16, + 16, + 18, + 18, + 14, + 14, + 16, + 16, + 16, + 16, + 18, + 18, + 6, + 6, + 8, + 8, + 8, + 8, + 10, + 10, + 8, + 8, + 10, + 10, + 10, + 10, + 12, + 12, + 8, + 8, + 10, + 10, + 10, + 10, + 12, + 12, + 10, + 10, + 12, + 12, + 12, + 12, + 14, + 14, + 10, + 10, + 12, + 12, + 12, + 12, + 14, + 14, + 10, + 10, + 12, + 12, + 12, + 12, + 14, + 14, + 12, + 12, + 14, + 14, + 14, + 14, + 16, + 16, + 12, + 12, + 14, + 14, + 14, + 14, + 16, + 16, + 8, + 8, + 10, + 10, + 10, + 10, + 12, + 12, + 10, + 10, + 12, + 12, + 12, + 12, + 14, + 14, + 10, + 10, + 12, + 12, + 12, + 12, + 14, + 14, + 12, + 12, + 14, + 14, + 14, + 14, + 16, + 16, + 12, + 12, + 14, + 14, + 14, + 14, + 16, + 16, + 12, + 12, + 14, + 14, + 14, + 14, + 16, + 16, + 14, + 14, + 16, + 16, + 16, + 16, + 18, + 18, + 14, + 14, + 16, + 16, + 16, + 16, + 18, + 18, + 8, + 8, + 10, + 10, + 10, + 10, + 12, + 12, + 10, + 10, + 12, + 12, + 12, + 12, + 14, + 14, + 10, + 10, + 12, + 12, + 12, + 12, + 14, + 14, + 12, + 12, + 14, + 14, + 14, + 14, + 16, + 16, + 10, + 10, + 12, + 12, + 12, + 12, + 14, + 14, + 12, + 12, + 14, + 14, + 14, + 14, + 16, + 16, + 12, + 12, + 14, + 14, + 14, + 14, + 16, + 16, + 14, + 14, + 16, + 16, + 16, + 16, + 18, + 18, + 10, + 10, + 12, + 12, + 12, + 12, + 14, + 14, + 12, + 12, + 14, + 14, + 14, + 14, + 16, + 16, + 12, + 12, + 14, + 14, + 14, + 14, + 16, + 16, + 14, + 14, + 16, + 16, + 16, + 16, + 18, + 18, + 12, + 12, + 14, + 14, + 14, + 14, + 16, + 16, + 14, + 14, + 16, + 16, + 16, + 16, + 18, + 18, + 14, + 14, + 16, + 16, + 16, + 16, + 18, + 18, + 16, + 16, + 18, + 18, + 18, + 18, + 20, + 20, + 8, + 8, + 10, + 10, + 10, + 10, + 12, + 12, + 10, + 10, + 12, + 12, + 12, + 12, + 14, + 14, + 10, + 10, + 12, + 12, + 12, + 12, + 14, + 14, + 12, + 12, + 14, + 14, + 14, + 14, + 16, + 16, + 10, + 10, + 12, + 12, + 12, + 12, + 14, + 14, + 12, + 12, + 14, + 14, + 14, + 14, + 16, + 16, + 12, + 12, + 14, + 14, + 14, + 14, + 16, + 16, + 14, + 14, + 16, + 16, + 16, + 16, + 18, + 18, + 10, + 10, + 12, + 12, + 12, + 12, + 14, + 14, + 12, + 12, + 14, + 14, + 14, + 14, + 16, + 16, + 12, + 12, + 14, + 14, + 14, + 14, + 16, + 16, + 14, + 14, + 16, + 16, + 16, + 16, + 18, + 18, + 12, + 12, + 14, + 14, + 14, + 14, + 16, + 16, + 14, + 14, + 16, + 16, + 16, + 16, + 18, + 18, + 14, + 14, + 16, + 16, + 16, + 16, + 18, + 18, + 16, + 16, + 18, + 18, + 18, + 18, + 20, + 20, + 1, + 2, + 2, + 3, + 2, + 3, + 3, + 4, + 2, + 3, + 3, + 4, + 3, + 4, + 4, + 5, + 2, + 3, + 3, + 4, + 3, + 4, + 4, + 5, + 3, + 4, + 4, + 5, + 4, + 5, + 5, + 6, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 2, + 3, + 3, + 4, + 3, + 4, + 4, + 5, + 3, + 4, + 4, + 5, + 4, + 5, + 5, + 6, + 3, + 4, + 4, + 5, + 4, + 5, + 5, + 6, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 1, + 2, + 2, + 3, + 2, + 3, + 3, + 4, + 2, + 3, + 3, + 4, + 3, + 4, + 4, + 5, + 2, + 3, + 3, + 4, + 3, + 4, + 4, + 5, + 3, + 4, + 4, + 5, + 4, + 5, + 5, + 6, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 2, + 3, + 3, + 4, + 3, + 4, + 4, + 5, + 3, + 4, + 4, + 5, + 4, + 5, + 5, + 6, + 3, + 4, + 4, + 5, + 4, + 5, + 5, + 6, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 2, + 3, + 3, + 4, + 3, + 4, + 4, + 5, + 3, + 4, + 4, + 5, + 4, + 5, + 5, + 6, + 3, + 4, + 4, + 5, + 4, + 5, + 5, + 6, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 3, + 4, + 4, + 5, + 4, + 5, + 5, + 6, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 2, + 3, + 3, + 4, + 3, + 4, + 4, + 5, + 3, + 4, + 4, + 5, + 4, + 5, + 5, + 6, + 3, + 4, + 4, + 5, + 4, + 5, + 5, + 6, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 3, + 4, + 4, + 5, + 4, + 5, + 5, + 6, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 3, + 4, + 4, + 5, + 4, + 5, + 5, + 6, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 3, + 4, + 4, + 5, + 4, + 5, + 5, + 6, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 9, + 10, + 10, + 11, + 10, + 11, + 11, + 12, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 9, + 10, + 10, + 11, + 10, + 11, + 11, + 12, + 3, + 4, + 4, + 5, + 4, + 5, + 5, + 6, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 3, + 4, + 4, + 5, + 4, + 5, + 5, + 6, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 9, + 10, + 10, + 11, + 10, + 11, + 11, + 12, + 4, + 5, + 5, + 6, + 5, + 6, + 6, + 7, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 9, + 10, + 10, + 11, + 10, + 11, + 11, + 12, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 9, + 10, + 10, + 11, + 10, + 11, + 11, + 12, + 9, + 10, + 10, + 11, + 10, + 11, + 11, + 12, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 9, + 10, + 10, + 11, + 10, + 11, + 11, + 12, + 9, + 10, + 10, + 11, + 10, + 11, + 11, + 12, + 10, + 11, + 11, + 12, + 11, + 12, + 12, + 13, + 10, + 11, + 11, + 12, + 11, + 12, + 12, + 13, + 5, + 6, + 6, + 7, + 6, + 7, + 7, + 8, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 9, + 10, + 10, + 11, + 10, + 11, + 11, + 12, + 9, + 10, + 10, + 11, + 10, + 11, + 11, + 12, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 9, + 10, + 10, + 11, + 10, + 11, + 11, + 12, + 9, + 10, + 10, + 11, + 10, + 11, + 11, + 12, + 10, + 11, + 11, + 12, + 11, + 12, + 12, + 13, + 10, + 11, + 11, + 12, + 11, + 12, + 12, + 13, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 9, + 10, + 10, + 11, + 10, + 11, + 11, + 12, + 9, + 10, + 10, + 11, + 10, + 11, + 11, + 12, + 10, + 11, + 11, + 12, + 11, + 12, + 12, + 13, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 9, + 10, + 10, + 11, + 10, + 11, + 11, + 12, + 9, + 10, + 10, + 11, + 10, + 11, + 11, + 12, + 10, + 11, + 11, + 12, + 11, + 12, + 12, + 13, + 10, + 11, + 11, + 12, + 11, + 12, + 12, + 13, + 11, + 12, + 12, + 13, + 12, + 13, + 13, + 14, + 6, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 9, + 10, + 10, + 11, + 10, + 11, + 11, + 12, + 9, + 10, + 10, + 11, + 10, + 11, + 11, + 12, + 10, + 11, + 11, + 12, + 11, + 12, + 12, + 13, + 7, + 8, + 8, + 9, + 8, + 9, + 9, + 10, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 8, + 9, + 9, + 10, + 9, + 10, + 10, + 11, + 9, + 10, + 10, + 11, + 10, + 11, + 11, + 12, + 9, + 10, + 10, + 11, + 10, + 11, + 11, + 12, + 10, + 11, + 11, + 12, + 11, + 12, + 12, + 13, + 10, + 11, + 11, + 12, + 11, + 12, + 12, + 13, + 11, + 12, + 12, + 13, + 12, + 13, + 13, + 14 + ], + "rows": [ + 129, + 2178, + 2180, + 2184, + 2192, + 2472, + 2240, + 128, + 2432, + 2720, + 3201, + 2176 + ] + } + ], + "frame": 549, + "registers": [ + 1, + 7, + 26, + 27, + 30, + 31, + 106, + 107, + 108, + 109, + 115, + 117 + ], + "schema": 1, + "seed": 17, + "slice": [ + 471, + 512 + ], + "split": 17 +} diff --git a/research/r420-block7-exact-schedule/CLAIM.md b/research/r420-block7-exact-schedule/CLAIM.md new file mode 100644 index 0000000000..daad72df14 --- /dev/null +++ b/research/r420-block7-exact-schedule/CLAIM.md @@ -0,0 +1,31 @@ +# Local sprint claim + +- Track: bit supplier; OS-random assignment seed **17** (`secrets.randbelow(100)`). +- Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +- Claimed: 2026-10-13 05:23:34 UTC; expected finish: 05:58 UTC (13:58 Hong Kong). +- Object: PR543 R420 phase-B block **7 = 17 mod 10**, frame 549, + original B[471:512], on the unchanged selected supplier word. +- Method: split the original 41-XOR block into its upper/lower triangular + factors and use an exact subset-state dynamic program to minimize each + factor among schedules that finish each destination in one contiguous + batch, using only positive additions from the current other wires. + Check integer transfer equality, both positive envelopes, literal reverse + cleanup, all arbitrary-input columns, frames and complete native bill. +- Deliverable: frozen circuit, finite-class optimality certificate, verifier, + source pins and a scoped research note; no new kappa assumed. +- Three candidates considered: (1) block-7 factor scheduling; (2) punctured + R439 mini-node basis changes (close overlap with #728); (3) full-frame + decoder resynthesis (close overlap with #708/#748/#753). Selected (1). +- Distinct coverage: #670 and #674 optimize blocks 3 and 5, respectively; + #691 changes quad 13; #754 synthesizes cleanup windows on at most four + wires. This experiment checks all subset states for two twelve-wire + factors with a precisely stated schedule class, not another stochastic + rewrite seed or a claim of unrestricted XOR optimality. #681 integrates + the earlier circuits but does not change block 7. +- Coordination: browser inspection of the issue listing and API inspection + found only issue #650 (request for Discussions), no pinned sprint issue. + No reservation issue was created. Initial metadata covered 586 open PRs + through #767. The repository review ledger ends at #626; later proposals + are not treated as accepted frontiers. +- Contributor: Yuzhou Wang / @yzhouwang, with substantial OpenAI Codex + assistance. Apache-2.0. No delegated workers or independent human review. diff --git a/research/r420-block7-exact-schedule/EXPECTED.json b/research/r420-block7-exact-schedule/EXPECTED.json new file mode 100644 index 0000000000..13056dd05d --- /dev/null +++ b/research/r420-block7-exact-schedule/EXPECTED.json @@ -0,0 +1,86 @@ +{ + "columns": 660, + "controls": [ + "omitted local XOR", + "F2-neutral positive inflation", + "omitted cleanup", + "stale scalar-valid cleanup", + "omitted dirty compensation", + "illegal frame descent", + "inflated lower-bound certificate", + "unpaid witness gate" + ], + "factor_audits": [ + { + "feasible_pairs": 20992, + "new": 14, + "old": 17, + "state_destination_pairs": 24576, + "states": 4096, + "valid_donor_subsets": 20992 + }, + { + "feasible_pairs": 22528, + "new": 14, + "old": 24, + "state_destination_pairs": 24576, + "states": 4096, + "valid_donor_subsets": 22528 + } + ], + "kappa": "unchanged", + "labels": { + "frames": 672, + "gram_det": 1, + "labels": 120, + "lattice_rank": 8 + }, + "local": { + "boolean_inputs": 4096, + "integer_columns_each_orientation": 12, + "reverse_strictly_smaller_entries": 25 + }, + "native": [ + { + "adds": 26916, + "copies": 9, + "erasures": 9, + "forward_prefix": 144651, + "paid_histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "payload": "998206739997057013039187410944", + "payload_bits": 100, + "rank_mass": 5112, + "records": 29874, + "reverse_prefix": 2270064 + }, + { + "adds": 26890, + "copies": 9, + "erasures": 9, + "forward_prefix": 144651, + "paid_histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "payload": "942069190649173878911112170496", + "payload_bits": 100, + "rank_mass": 5112, + "records": 29848, + "reverse_prefix": 2205308 + } + ], + "status": "PASS_R420_BLOCK7_EXACT_SCHEDULE", + "word_sha256": [ + "e597e3885c0a8daa262afa5985ee2930443329126aece76d33159d81882bdcc2", + "d8faa85175256c99afbd8f8ac8639c0de9be2e5ff3ad7f64012fe506f58dd43a" + ] +} diff --git a/research/r420-block7-exact-schedule/NATIVE.json b/research/r420-block7-exact-schedule/NATIVE.json new file mode 100644 index 0000000000..d010852ff5 --- /dev/null +++ b/research/r420-block7-exact-schedule/NATIVE.json @@ -0,0 +1,51 @@ +{ + "status": "PASS_R420_BLOCK7_NATIVE", + "words": [ + { + "adds": 26916, + "payload_bits": 100, + "rank_mass": 5112, + "stages": [ + { + "bridge_controls": 6, + "columns": 900, + "stages": 5 + }, + { + "bridge_controls": 18, + "columns": 1380, + "stages": 9 + }, + { + "bridge_controls": 24, + "columns": 1620, + "stages": 11 + } + ], + "word": "original" + }, + { + "adds": 26890, + "payload_bits": 100, + "rank_mass": 5112, + "stages": [ + { + "bridge_controls": 6, + "columns": 900, + "stages": 5 + }, + { + "bridge_controls": 18, + "columns": 1380, + "stages": 9 + }, + { + "bridge_controls": 24, + "columns": 1620, + "stages": 11 + } + ], + "word": "replacement" + } + ] +} diff --git a/research/r420-block7-exact-schedule/README.md b/research/r420-block7-exact-schedule/README.md new file mode 100644 index 0000000000..76fb31fc5b --- /dev/null +++ b/research/r420-block7-exact-schedule/README.md @@ -0,0 +1,226 @@ +# Exact factor schedules for R420 block 7 + +**Finite bit-circuit construction and finite-class optimality certificate; no +new κ.** The phase-B block at `B[471:512]` (frame 549) in eumemic's selected +PR543 R420 word falls from **41 to 28 binary XOR additions**. Its literal +reverse cleanup saves thirteen more, so the complete native word falls from +**26,916 to 26,890 ADDs**. No temporary register is introduced. + +The exact forward **integer** transfer matrix is unchanged, not merely its +reduction modulo two. The reverse cancellation-free transfer matrix is +entrywise no larger (25 entries strictly decrease). The replacement retains +all 660 dirty-input columns, the original per-register frame paths, all +420 helpers, nine retained copies and paid rank mass 5,112. This is a scalar +instruction reduction, not a recursive-profile or practical runtime result. + +| Local native bill | Original | Replacement | +|---|---:|---:| +| First factor | 17 | **14** | +| Second factor | 24 | **14** | +| Block plus its reverse cleanup | 82 | **56** | +| All ADDs, including D and scatter | 26,916 | **26,890** | +| All native records | 29,874 | **29,848** | +| Forward positive prefix | 144,651 | 144,651 | +| Reverse positive prefix | 2,270,064 | **2,205,308** | +| Local payload allowance | 100 bits | 100 bits | + +## Reproduce + +From the repository root, Python 3.9+ and the standard library suffice: + +```sh +python3 -I -B research/r420-block7-exact-schedule/verify.py +``` + +Expected final line: + +```text +PASS_R420_BLOCK7_EXACT_SCHEDULE factors=17+24->14+14 ADDs=26916->26890 states=8192 columns=660 controls=8 kappa=unchanged +``` + +The default command writes only into an automatically removed temporary +directory. `--out /path/to/new-directory` retains both complete words, the +original exporter's binary records, frame files, and exact receipt. An +existing output path is rejected. Nothing under `upstream/`, the original +supplier, or the selected frontier is edited. + +For unchanged C++17/Boost native legality and five-, nine-, eleven-stage +column checkers: + +```sh +python3 -I -B research/r420-block7-exact-schedule/native.py --out /tmp/block7-native-new +``` + +Expected: `PASS_R420_BLOCK7_NATIVE words=2 stages=5,9,11 bridge_controls=96`. +Set `CXX` to the compiler executable and `BOOST_INCLUDE` to the Boost include +directory if needed. Defaults are `c++` and `/opt/homebrew/include` on macOS, +`/usr/include` elsewhere. The C++ inputs and portable headers are source-pinned; +the external compiler and Boost version are environment dependencies. + +Reproduce the complete nomination, without a stochastic search or a solver: + +```sh +python3 -I -B research/r420-block7-exact-schedule/nominate.py > /tmp/block7-certificate.json +cmp /tmp/block7-certificate.json research/r420-block7-exact-schedule/CERTIFICATE.json +``` + +Expected: `cmp` exits zero. Both factor searches complete all 4,096 states; +there is no timeout, sample, truncated search, or claim of unrestricted +circuit optimality. The OS assignment seed is **17**; `17 mod 10` selects +block 7. No other object was optimized. + +## Exact object and schedule class + +Base commit: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +Selected bit source #543: `2065fe4f72a914d907f1046603f5a36f17018535`. +Selected #626 source: `660de893d27bb7abd1d5b01b1640207528a5c851`. +`SOURCES.json` pins every consumed repository source, including the unchanged +checker/exporter and optional native dependencies. `CERTIFICATE.json` contains +the complete integer distance potentials and explicit replacement batches; +`EXPECTED.json` contains the exact regenerated evidence. + +Use local wire order + +``` +[1, 7, 26, 27, 30, 31, 106, 107, 108, 109, 115, 117]. +``` + +The original 41-gate block has a fixed cut after gate 17: its first and second +factors are the original upper/lower elimination factors. We retain these two +**integer** matrices separately. Each is a binary matrix with diagonal one. + +Within each factor a schedule finishes every destination exactly once, in +any order. Finishing row `d` means one contiguous batch of operations +`wire[d] += wire[s]`, using distinct other wires; no extra scratch, scaling, +subtraction, or later revisit of the destination is allowed. Empty batches +are allowed for unchanged rows. Sources may be read before or after they +are finished. The output is on the same named wires, with no free permutation. +All additions have coefficient +1. The same circuit is then interpreted +as XORs over F2 in the bit word. + +The original two factors belong to this class. The certified minima are +14 and 14, respectively. The combined 28 is optimal only among independent +schedules of these **fixed two factors**. A circuit that crosses the cut, +changes the intermediate matrix, revisits a destination, uses cancellation, +borrows wires, changes frames or chooses another block is outside this claim. + +## Proof of the finite-class minimum + +Let `M` be one factor and `e_s` the original unit row on wire `s`. At the +boundary after finishing precisely the set `S`, the row on wire `s` is +`M_s` for `s in S` and `e_s` otherwise. This follows directly by induction on +the batches and does not depend on their earlier order. + +To finish an unfinished destination `d`, choose a subset `Q` of the other +wires such that, over the nonnegative integers, + +``` +M_d = e_d + sum(current_row(s, S) for s in Q). +``` + +This is necessary and sufficient; its exact cost is `|Q|`. Since the target +row is binary, selected donor supports must partition `M_d - e_d`. A donor +with a coordinate outside that support cannot occur, and a donor cannot +occur twice. The empty set is handled explicitly. This proves that the +state graph enumerates the entire stated class, with transitions +`S -> S union {d}`. Marking an unchanged row as finished is a harmless +zero-cost transition: its row stays the same. + +`nominate.py` minimizes over this acyclic graph using a recursive exact-cover +oracle. Its path is a construction, not the sole evidence for the minimum. +`verify.py` does **not import the nominator**. It reconstructs each matrix +with twelve separately replayed integer input columns and independently +enumerates all eligible donor subsets using ordinary integer addition in +base 16. Each sum contains at most eleven binary vectors, so no carry can +hide an overlap or a missing coordinate. + +For every valid donor subset the verifier checks the certificate potential +inequality + +``` +p(S union {d}) <= p(S) + |Q|, p(empty) = 0. +``` + +Telescoping along any schedule gives `p(full) <= cost(schedule)`. Separately, +the explicit batch witness realizes `M` at cost `p(full) = 14`. Thus the +lower and upper bounds coincide. This is checked for **49,152** possible +state/destination pairs across the factors; **43,520** are feasible. Every +potential and witness is in the committed certificate. This is a finite +mathematical certificate with a written completeness argument, not a +proof-assistant formalization. + +## Full word, growth and accounting + +The changed block occurs at one closed D4 frame, after the initial target +single reads and before all later needer writes and target reads. Its same +named-wire integer map therefore preserves all source and helper components +of every later read, including arbitrary initial dirt. Nothing in D, A, +scatter, or the remaining B gates changes. C is regenerated as the literal +reverse of **all** z-destination gates in A and B, at the full frame. This +retains the original H1–H5 interface; no checker guard is patched or relaxed. + +All twelve changed wires already have the same legal climb to frame 549. +Every wire's ordered frame path is checked equal to the original. Reordering +first accesses inside the block can reorder MOVE events globally, but cannot +remove or discount any individual climb. Native legality checks common-frame +access and the actual emitted chronological stream. The complete rank +histogram remains `{1:1320, 2:1440, 4:60, 5:120, 8:9}`. + +The first factor saves 3 ADDs, the second saves 10, and their full reverse +saves another 13. There are no new helper, source-copy, preparation, +restoration, frame-change, or recursive-child charges. The recursive paid +profile and retained-copy cost are unchanged. The selected assembly remains +complex-bound and unchanged; **no larger bit exponent or κ is inferred**. + +The verifier compares exact integer matrices for the complete block and +compares the reversed positive matrices entry by entry. Because positive +updates only increase each row, every intermediate norm within a block is +bounded by its final row norm. Equality of forward matrices and domination +of reverse matrices therefore preserve the relevant prefix envelope for any +nonnegative starting-bound vector. The native exporter and independent C++ +checker also recompute the actual prefix numbers shown above. The inherited +payload formula `64 * forward^3 * reverse^2` stays below `2^104`. + +The primary checker replays all 4,096 Boolean block inputs and all 660 full +word columns with a separate set-valued interpreter. The unchanged PR543 +checker verifies exact rational E8 geometry, all 672 closed frames, the +complete word, and each H1–H5 hypothesis and conclusion. Geometry is computed +once and reused only because the entire frame/label data is unchanged. + +Eight negative controls reject omitted local work, F2-neutral positive-cost +inflation, missing cleanup, scalar-valid but nonliteral stale cleanup, +missing dirt compensation, illegal frame descent, an inflated lower-bound +potential, and an unpaid witness gate. The stale-cleanup control explicitly +passes the endpoint map before failing literal H4; endpoint equality alone +is not passed off as interface compliance. + +## Scope, related work and credit + +The selected conditional result remains +`51110230636731/31250000000000000 = 0.001635527380375392`. +All-size compilation, common-label/mutable-basis realization, physical +hosting, normalized residuals, precision/tape/exact recovery and analytic +transfer remain inherited obligations. The hosted-parent/invoice/outer +assembly was not regenerated for this local circuit. Finite stage checks +are not a full multiplication theorem, a speed benchmark or independent +human peer review. + +Credit eumemic's #543/#493 construction and interface; Dylan Crow's #370 +format, exporter and checker lineage; DreamingOfClouds' retained-total and +pricing work; Zhihao Chen's scalar interface; chafreaky/DaysSky and the +cumulative stage, realization and hosting lineage in the original +[NOTICE](../e8-bit-r420/NOTICE.md). Those source notices remain unchanged. + +Concurrent #670 (yongjae321) and #674 (x0hu) shorten **blocks 3 and 5**; +#691 (mtpsl) changes phase-A quad 13. #681 (Alluri) integrates those and other +circuits; #754 (Jeffrey Cox / namredips) gives exact synthesis of cleanup +windows on at most four wires. They are credited as related predecessors, +not imported or asserted composable. This contribution supplies an unchanged +literal-H4 circuit at **block 7**, and a complete twelve-wire factor-schedule +lower-bound certificate. The elementary dynamic-programming technique itself +is not claimed as new. See `CLAIM.md` and `VALIDATION.md` for overlap checks +and exact execution limits. + +Prepared by **Yuzhou Wang (@yzhouwang)** with substantial **OpenAI Codex +assistance** in task selection, mathematical derivation, implementation, +verification and writing. Apache-2.0. No delegated workers were used. diff --git a/research/r420-block7-exact-schedule/SOURCES.json b/research/r420-block7-exact-schedule/SOURCES.json new file mode 100644 index 0000000000..119298b52a --- /dev/null +++ b/research/r420-block7-exact-schedule/SOURCES.json @@ -0,0 +1,27 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "files": { + "certificates/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "docs/research/community-k492-review.md": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47", + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp": "1c344d18fcd494eeca93e259f10cafae7705780e6592f6dcb35b34752dab9bc2", + "research/e8-bit-carrier-skeleton/code/bit/checkers/json.hpp": "aaf127c04cb31c406e5b04a63f1ae89369fccde6d8fa7cdda1ed4f32dfc5de63", + "research/e8-bit-carrier-skeleton/code/bit/checkers/legality_h.cpp": "6c1ef2b24e57781d6951c172a1024fc4300e6fd392c9d6672079a7806ab663b3", + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3", + "research/e8-bit-carrier-skeleton/code/bit/regression/stage_cohort.py": "6c288f6f234b528c1a7c0a4adfb724e91e0fe6b18c8dffad96af3f973de1829a", + "research/e8-bit-carrier-skeleton/portable-include/bits/stdc++.h": "420094be2af295eed03a983dd66debbbe9cfb78d8252859f4498a615a0074b99", + "research/e8-bit-r420/NOTICE.md": "12ba6e0845f222e9940b00f6c60d261db104246a8d3143da267682973479f811", + "research/e8-bit-r420/README.md": "9807be57c6adf26b30e4f54e2f8160075bbc05091f1a6d157e43d2a4620c1c9f", + "research/e8-bit-r420/code/xcheck.py": "5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424", + "research/e8-bit-r420/data/bitE8mut-r420.json.gz": "9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784" + }, + "pr543_head": "2065fe4f72a914d907f1046603f5a36f17018535", + "pr626_head": "660de893d27bb7abd1d5b01b1640207528a5c851", + "related_not_imported": { + "670": "2e31fcad7f9ecc8b97039ecb2333e581fd725fa1", + "674": "1b01fd8b135fb2c458554fbbbab4338336bf366d", + "681": "e536f6fc8aad65adef8ac4682d13625598a5c3f9", + "691": "ee6b9175fe006c11871802866c487b5ecc1a93a4", + "754": "47ebba87e064cc69d9b4834081fc74080762a74f" + }, + "source_word_git_blob": "0c63ca62759dc63d302be6552aeeee1ede70350f" +} diff --git a/research/r420-block7-exact-schedule/VALIDATION.md b/research/r420-block7-exact-schedule/VALIDATION.md new file mode 100644 index 0000000000..efc841c89c --- /dev/null +++ b/research/r420-block7-exact-schedule/VALIDATION.md @@ -0,0 +1,77 @@ +# Validation and handoff + +Local execution on 2026-10-13, macOS arm64. Base: +`66849e1475c930fd7732b1a0067ffee7e1e95f60`. + +## Completed evidence + +- `python3 -I -B research/r420-block7-exact-schedule/native.py --out /private/tmp/r420-block7-native-v1`: + PASS on CPython **3.14.5**, Apple Clang **17.0.0**, Boost **1.90**. + The source-pinned, unchanged native code was freshly compiled for this run. + Both original/replacement words passed chronological legality and all + 900 / 1,380 / 1,620 physical columns at five / nine / eleven stages. + All 6 / 18 / 24 bridge-omission controls per word rejected: **96 total**. + Native counts and exact positive-prefix payloads matched the independent + Python recount. The two native summaries are retained in `NATIVE.json`. +- The primary verifier passed on CPython **3.14.5** with isolated optimized + execution (`-I -O -B`), and system CPython **3.9.6** (`-I -B`). + All eight semantic/accounting controls rejected for their named reasons. +- Fresh nomination reproduced `CERTIFICATE.json` byte for byte. The verifier + does not import the nomination code and checks every lower-bound edge using + a different donor-subset enumeration and integer-column interpreter. +- A minimal export containing only this package and `SOURCES.json` inputs + passed from outside the repository, in a path containing spaces, under + isolated optimized Python. Corrupt-source, inflated-potential, + changed-expected-receipt and existing-output controls all rejected. + The existing-output sentinel remained unchanged. +- Git verified that the original word has the same blob + `0c63ca62759dc63d302be6552aeeee1ede70350f` at both the exact main base and + the fetched PR543 head `2065fe4f72a914d907f1046603f5a36f17018535`. +- `make selected-record-check` passed. Its first invocation failed because + certificate bootstrapping (without `-B`) created an untracked xcheck cache + in an immutable supplier package. Only that new cache was removed; the + contribution now suppresses bytecode before importing repository modules. + No selected source bytes or inventory were changed. + +The execution path above identifies the local run; it is not a portability +dependency. Use a fresh output directory for reproduction. `NATIVE.json` +records a completed local run, not hosted CI status. `native.py` recomputes +and checks native status/counts/coverage against the exact Python receipt. + +## Deliberately outside this contribution + +No full repository-wide `make verify`, selected supplier cold replay, +hosted-parent invoice, outer assembly, remote Linux CI, proof-assistant +build, or runtime benchmark is claimed. This addition changes only the new +research package, not a selected generator. Full native stage replay was +chosen because a local circuit changed. The selected bit source, frontier, +and `upstream/` remain untouched. + +All-size compiler/common-label/mutable-basis, physical hosting, residual, +precision/tape/exact recovery and analytic assumptions remain. A potential +certificate proves the stated finite schedule-class minimum; finite scalar +replays do not prove the integer multiplication theorem. + +## Review focus + +1. Check the fixed 17/24 cut and row-batch class in README; the minimum 28 + does not claim unrestricted XOR optimality. +2. Check the independent base-16 subset enumeration and potential + inequalities, including empty batches and arbitrary completion order. +3. Check the complete integer map, reverse positive domination, unchanged + register frame paths and literal cleanup. All restoration work is priced. +4. Check `EXPECTED.json`, `NATIVE.json`, source pins and predecessor credit. + +Contributor: Yuzhou Wang / @yzhouwang, substantial OpenAI Codex assistance. +No delegated workers or independent human peer review. Apache-2.0. + +## Publication overlap refresh + +The initial snapshot covered 586 open PRs through #767. The submission +refresh inspected the 100 most recently updated open PRs, including all new +arrivals #768–#786. Main remained at the exact base. No block-7 or fixed +two-factor row-batch certificate appeared. New #774 concerns target +compensation forests; #782 concerns intrinsic lattice parity. Neither +changes this block or supplies the finite schedule-class certificate. +The inspected #681/#691/#754 heads remain those in `SOURCES.json`. +No pending implementation was imported and no additive composition claimed. diff --git a/research/r420-block7-exact-schedule/native.py b/research/r420-block7-exact-schedule/native.py new file mode 100644 index 0000000000..22c15adbb0 --- /dev/null +++ b/research/r420-block7-exact-schedule/native.py @@ -0,0 +1,88 @@ +#!/usr/bin/env python3 +"""Compile unchanged native checkers and check both words, with 5/9/11 stages. +Yuzhou Wang + OpenAI Codex, Apache-2.0. C++17 and Boost headers required. +""" +import argparse +import importlib.util +import json +import os +from pathlib import Path +import subprocess +import sys +import tempfile + +sys.dont_write_bytecode = True + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location('block7_verify', HERE / 'verify.py') +v = importlib.util.module_from_spec(spec) +spec.loader.exec_module(v) +ROOT = v.ROOT +BASE = ROOT / 'research/e8-bit-carrier-skeleton' +CK = BASE / 'code/bit/checkers' + + +def command(args, log): + with log.open('w') as out: + subprocess.run(list(map(str, args)), check=True, stdout=out, stderr=subprocess.STDOUT) + + +def replay(out): + # run() performs source pins, both complete finite words and all package controls. + receipt = v.run(out) + bindir = out / 'bin' + bindir.mkdir() + boost = os.environ.get('BOOST_INCLUDE', '/opt/homebrew/include' if sys.platform == 'darwin' else '/usr/include') + common = [os.environ.get('CXX', 'c++'), '-O2', '-std=c++17', '-DHDIM=8', '-DNCOPY=9', + '-DVPORTS=120', '-DRHELP=420', '-I' + str(BASE / 'portable-include'), '-I' + str(CK), '-I' + boost] + command(common + [CK / 'legality_h.cpp', '-o', bindir / 'legality'], out / 'compile-legality.log') + for k in (2, 4, 5): + command(common + ['-DKPAIRS=' + str(k), CK / 'columns_k.cpp', '-o', bindir / ('columns' + str(k))], + out / ('compile-columns' + str(k) + '.log')) + summary = [] + for index, name in enumerate(('original', 'replacement')): + wd = out / name + expected = receipt['native'][index] + command([sys.executable, '-I', '-B', BASE / 'code/bit/regression/stage_cohort.py', + wd / 'records', wd / 'records', wd / 'cin', wd / 'cout'], wd / 'stage.log') + command([bindir / 'legality', wd / 'cin', wd / 'cout', wd / 'legality.json'], wd / 'legality.log') + legality = json.loads((wd / 'legality.json').read_text()) + v.need(legality['status'] == 'PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE', 'native legality status') + v.need(legality['common_frame_ADDs'] == expected['adds'] and legality['rank_mass'] == 5112 and + legality['copies'] == legality['erasures'] == 9, 'native legality bill') + stages = [] + for k in (2, 4, 5): + result = wd / ('columns' + str(k) + '.json') + command([bindir / ('columns' + str(k)), wd / 'cout/COHORT249-RECORDS.bin', result], + wd / ('columns' + str(k) + '.log')) + checked = json.loads(result.read_text()) + status = ('PASS_NEW_COHORT249_ALL_FIVE_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL' if k == 2 else + 'PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL') + v.need(checked['status'] == status, 'native column status') + v.need(checked['formal_columns_checked'] == 2 * k * 120 + 420, 'native column coverage') + v.need(checked['local_scalar_additions'] == expected['adds'], 'native scalar count') + v.need(checked['payload_prefix_upper'] == expected['payload'], 'independent prefix bill') + v.need(len(checked['negative_controls']) == 6 * (k - 1) and + all(c['rejected'] for c in checked['negative_controls']), 'native bridge controls') + stages.append({'stages': 2 * k + 1, 'columns': checked['formal_columns_checked'], + 'bridge_controls': len(checked['negative_controls'])}) + summary.append({'word': name, 'adds': expected['adds'], 'rank_mass': 5112, + 'payload_bits': expected['payload_bits'], 'stages': stages}) + evidence = {'status': 'PASS_R420_BLOCK7_NATIVE', 'words': summary} + (out / 'native-receipt.json').write_text(json.dumps(evidence, sort_keys=True, indent=2) + '\n') + print('PASS_R420_BLOCK7_NATIVE words=2 stages=5,9,11 bridge_controls=96') + return evidence + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--out', type=Path, help='fresh directory for binaries, words and all logs') + args = parser.parse_args() + if args.out: + destination = args.out.resolve() + v.need(destination != HERE and HERE not in destination.parents, 'output inside package') + destination.mkdir(parents=True, exist_ok=False) + replay(destination) + else: + with tempfile.TemporaryDirectory(prefix='r420-block7-native-') as tmp: + replay(Path(tmp)) diff --git a/research/r420-block7-exact-schedule/nominate.py b/research/r420-block7-exact-schedule/nominate.py new file mode 100644 index 0000000000..66831a31b8 --- /dev/null +++ b/research/r420-block7-exact-schedule/nominate.py @@ -0,0 +1,85 @@ +#!/usr/bin/env python3 +"""Exact finite schedule nomination. Yuzhou Wang + OpenAI Codex, Apache-2.0.""" +import functools +import gzip +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +N = 12 + + +def matrix(ops): + rows = [[int(i == j) for j in range(N)] for i in range(N)] + for d, s in ops: + rows[d] = [a + b for a, b in zip(rows[d], rows[s])] + return rows + + +def solve(ops): + m = matrix(ops) + if any(x not in (0, 1) for row in m for x in row) or any(m[i][i] != 1 for i in range(N)): + raise ValueError('nomination class requires binary integer matrix with diagonal one') + rows = [sum(x << i for i, x in enumerate(row)) for row in m] + dp = [10**9] * (1 << N) + dp[0] = 0 + previous = {} + feasible = 0 + for state in range(1 << N): + for d in range(N): + if state >> d & 1: + continue + wanted = rows[d] ^ (1 << d) + donors = [(s, rows[s] if state >> s & 1 else 1 << s) + for s in range(N) if s != d] + donors = [(s, row) for s, row in donors if row & ~wanted == 0] + + @functools.lru_cache(None) + def cover(remaining): + if not remaining: + return () + bit = remaining & -remaining + best = None + for s, row in donors: + if row & bit and row & remaining == row: + tail = cover(remaining ^ row) + if tail is not None: + choice = tuple(sorted((s,) + tail)) + if best is None or (len(choice), choice) < (len(best), best): + best = choice + return best + + sources = cover(wanted) + if sources is None: + continue + feasible += 1 + following = state | (1 << d) + if dp[state] + len(sources) < dp[following]: + dp[following] = dp[state] + len(sources) + previous[following] = (state, d, sources) + if any(d == 10**9 for d in dp): + raise ValueError('unexpected unreachable state') + batches = [] + state = (1 << N) - 1 + while state: + state, d, sources = previous[state] + batches.append([d, list(sources)]) + batches.reverse() + return {'original_gates': len(ops), 'rows': rows, 'potentials': dp, + 'minimum': dp[-1], 'feasible_state_destination_pairs': feasible, + 'batches': batches} + + +def nominate(): + word = json.loads(gzip.decompress((ROOT / 'research/e8-bit-r420/data/bitE8mut-r420.json.gz').read_bytes())) + block = word['B'][471:512] + registers = sorted({r for _, d, ss in block for r in [d] + ss}) + ix = {r: i for i, r in enumerate(registers)} + ops = [(ix[d], ix[s]) for _, d, ss in block for s in ss] + return {'schema': 1, 'seed': 17, 'block': 7, 'frame': 549, 'slice': [471, 512], + 'split': 17, 'registers': registers, 'factors': [solve(ops[:17]), solve(ops[17:])]} + + +if __name__ == '__main__': + print(json.dumps(nominate(), indent=2, sort_keys=True)) diff --git a/research/r420-block7-exact-schedule/verify.py b/research/r420-block7-exact-schedule/verify.py new file mode 100644 index 0000000000..089a787bf8 --- /dev/null +++ b/research/r420-block7-exact-schedule/verify.py @@ -0,0 +1,327 @@ +#!/usr/bin/env python3 +"""Finite circuit + independent lower-bound certificate replay; stdlib only. +Yuzhou Wang / yzhouwang, substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +import copy +import gzip +import hashlib +import importlib.util +import json +import struct +import subprocess +import sys +import tempfile +from collections import Counter +from pathlib import Path + +sys.dont_write_bytecode = True # Do not add caches to immutable supplier inventories. + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +N = 12 +WORD = 'research/e8-bit-r420/data/bitE8mut-r420.json.gz' +XCHECK = 'research/e8-bit-r420/code/xcheck.py' +EXPORTER = 'research/e8-bit-carrier-skeleton/code/bit/export_records.py' + + +class Reject(Exception): + pass + + +def need(condition, message): + if not condition: + raise Reject(message) + + +def digest(data): + return hashlib.sha256(data).hexdigest() + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':')).encode() + + +def source_check(): + pins = json.loads((HERE / 'SOURCES.json').read_text()) + for path, expected in pins['files'].items(): + need(digest((ROOT / path).read_bytes()) == expected, 'source hash: ' + path) + selected = json.loads((ROOT / 'certificates/selected-result.json').read_text()) + need(selected['reviewed_dependency_heads']['543'] == pins['pr543_head'], 'selected supplier binding') + need(selected['audited_source_head'] == pins['pr626_head'], 'selected construction binding') + return pins + + +def integer_columns(ops): + """Column-vector implementation, independent of nomination's row updates.""" + columns = [] + for j in range(N): + col = [int(i == j) for i in range(N)] + for d, s in ops: + need(0 <= d < N and 0 <= s < N and d != s, 'bad local gate') + col[d] += col[s] + columns.append(col) + return columns + + +def factor_audit(original, cert): + columns = integer_columns(original) + m = list(map(list, zip(*columns))) + need(all(x in (0, 1) for row in m for x in row), 'binary factor') + need(all(m[i][i] == 1 for i in range(N)), 'diagonal factor') + rows = [sum(x << j for j, x in enumerate(row)) for row in m] + need(cert['rows'] == rows and cert['original_gates'] == len(original), 'factor binding') + p = cert['potentials'] + need(len(p) == 1 << N and all(type(x) is int and x >= 0 for x in p) and p[0] == 0, 'potential admission') + # A different oracle from nomination: enumerate donor subsets as base-16 + # integers, using ordinary addition. At most 11 binary vectors are summed, + # so no digit carries can conceal repeated or missing coordinates. + encode = lambda mask: sum(((mask >> j) & 1) << (4 * j) for j in range(N)) + packed = [encode(row) for row in rows] + feasible = 0 + covers = 0 + transitions = 0 + for state in range(1 << N): + for d in range(N): + if state >> d & 1: + continue + transitions += 1 + wanted_mask = rows[d] ^ (1 << d) + wanted = encode(wanted_mask) + available = [] + for s in range(N): + if s == d: + continue + mask = rows[s] if state >> s & 1 else 1 << s + if mask & ~wanted_mask == 0: + available.append(packed[s] if state >> s & 1 else 1 << (4 * s)) + sums = [0] + counts = [0] + for value in available: + sums += [x + value for x in sums] + counts += [x + 1 for x in counts] + found = False + for total, count in zip(sums, counts): + if total == wanted: + covers += 1 + found = True + need(p[state | (1 << d)] <= p[state] + count, 'Bellman lower bound') + feasible += int(found) + need(feasible == cert['feasible_state_destination_pairs'], 'transition coverage') + need(len(cert['batches']) == N, 'batch count') + state = 0 + witness = [] + for d, ss in cert['batches']: + need(type(d) is int and 0 <= d < N and not (state >> d & 1), 'destination once') + need(all(type(s) is int and 0 <= s < N and s != d for s in ss) and len(set(ss)) == len(ss), 'donor admission') + total = 1 << (4 * d) + for s in ss: + total += packed[s] if state >> s & 1 else 1 << (4 * s) + need(total == packed[d], 'batch exact integer sum') + witness += [(d, s) for s in ss] + state |= 1 << d + need(len(witness) == p[-1] == cert['minimum'], 'optimal witness length') + need(integer_columns(witness) == columns, 'factor integer map') + return witness, {'states': 1 << N, 'state_destination_pairs': transitions, + 'feasible_pairs': feasible, 'valid_donor_subsets': covers, + 'old': len(original), 'new': len(witness)} + + +def local_check(original, replacement): + need(integer_columns(original) == integer_columns(replacement), 'local integer map') + old_rev = integer_columns(list(reversed(original))) + new_rev = integer_columns(list(reversed(replacement))) + need(all(b <= a for aa, bb in zip(old_rev, new_rev) for a, b in zip(aa, bb)), 'reverse positive envelope') + for value in range(1 << N): + a = [(value >> i) & 1 for i in range(N)] + b = a[:] + for d, s in original: + a[d] ^= a[s] + for d, s in replacement: + b[d] ^= b[s] + need(a == b, 'local truth table') + return {'boolean_inputs': 1 << N, 'integer_columns_each_orientation': N, + 'reverse_strictly_smaller_entries': sum(b < a for aa, bb in zip(old_rev, new_rev) for a, b in zip(aa, bb))} + + +def scalar(word): + """Independent set-valued interpretation including arbitrary helper dirt.""" + n = 2 * word['v'] + word['R'] + values = [{r} for r in range(n)] + for section in ('D', 'A', 'scatter', 'B', 'C'): + if section == 'scatter': + saved = [values[r].copy() for r in word['ret']] + for t, row in enumerate(word['scatter']): + for k in row: + values[word['v'] + t] ^= saved[k] + else: + for _, d, ss in word[section]: + for s in ss: + values[d] ^= values[s] + for r, value in enumerate(values): + expected = {r} + if word['v'] <= r < 2 * word['v']: + expected.add(r - word['v']) + need(value == expected, 'dirty-column endpoint') + return n + + +def paths(word): + current = list(word['start']) + result = [[f] for f in current] + frames = list(map(set, word['frames'])) + def move(r, f): + if current[r] != f: + need(frames[current[r]] < frames[f], 'frame descent') + result[r].append(f) + current[r] = f + for section in ('D', 'A', 'B', 'C'): + for f, d, ss in word[section]: + for r in [d] + ss: + move(r, f) + for r, f in enumerate(word['final']): + move(r, f) + return result + + +def literal(word): + need(word['C'] == [[1, d, ss] for sec in ('B', 'A') for _, d, ss in reversed(word[sec]) + if not word['v'] <= d < 2 * word['v']], 'literal cleanup') + + +def prefix(records, reverse=False): + norms = [1] * 661 + maximum = 1 + opened = False + for op, a, b, c, f, ph in (reversed(records) if reverse else records): + if op == 1: + norms[a] += abs(c) * norms[b] + maximum = max(maximum, norms[a]) + elif op in (2, 3): + if (op == 2) != reverse: + need(not opened, 'copy nesting') + norms[b] = norms[a] + opened = True + else: + need(opened, 'copy close') + norms[b] = 0 + opened = False + need(not opened, 'copy lifecycle') + return maximum + + +def export(word, out): + path = out / 'word.json' + path.write_bytes(canonical(word)) + subprocess.run([sys.executable, '-I', '-B', str(ROOT / EXPORTER), str(path), str(out / 'records')], + check=True, stdout=subprocess.DEVNULL) + raw = (out / 'records/249-records.bin').read_bytes() + records = list(struct.iter_unpack('<6i', raw)) + counts = Counter(r[0] for r in records) + hist = Counter(r[4] for r in records if r[0] == 0) + hist.update(r[5] for r in records if r[0] == 2) + # Record MOVE/COPY ranks, not scalar gate fan-in, determine this bill. + forward, backward = prefix(records), prefix(records, True) + payload = 64 * forward**3 * backward**2 + return records, {'records': len(records), 'adds': counts[1], 'copies': counts[2], 'erasures': counts[3], + 'paid_histogram': {str(k): v for k, v in sorted(hist.items())}, + 'rank_mass': sum(k * v for k, v in hist.items()), + 'forward_prefix': forward, 'reverse_prefix': backward, + 'payload_bits': payload.bit_length(), 'payload': str(payload)} + + +def rejected(label, fn, message): + try: + fn() + except Reject as exc: + need(message in str(exc), 'wrong rejection for ' + label + ': ' + str(exc)) + return label + raise Reject('negative control accepted: ' + label) + + +def run(out): + source_check() + old = json.loads(gzip.decompress((ROOT / WORD).read_bytes())) + cert = json.loads((HERE / 'CERTIFICATE.json').read_text()) + need({k: cert[k] for k in ('schema', 'seed', 'block', 'frame', 'slice', 'split')} == + dict(schema=1, seed=17, block=7, frame=549, slice=[471, 512], split=17), 'object binding') + block = old['B'][471:512] + regs = sorted({r for _, d, ss in block for r in [d] + ss}) + need(cert['registers'] == regs and len(regs) == N and all(f == 549 and len(ss) == 1 for f, _, ss in block), 'register binding') + ix = {r: i for i, r in enumerate(regs)} + original = [(ix[d], ix[ss[0]]) for _, d, ss in block] + first, a = factor_audit(original[:17], cert['factors'][0]) + second, b = factor_audit(original[17:], cert['factors'][1]) + replacement = first + second + local = local_check(original, replacement) + new = copy.deepcopy(old) + new['B'][471:512] = [[549, regs[d], [regs[s]]] for d, s in replacement] + new['C'] = [[1, d, ss] for sec in ('B', 'A') for _, d, ss in reversed(new[sec]) if not 120 <= d < 240] + need(all(new[k] == old[k] for k in old if k not in ('B', 'C')), 'unrelated word edit') + for word in (old, new): + literal(word) + scalar(word) + need(paths(old) == paths(new), 'per-register frame paths') + spec = importlib.util.spec_from_file_location('pr543_xcheck', ROOT / XCHECK) + xc = importlib.util.module_from_spec(spec) + spec.loader.exec_module(xc) + audit = xc.Word(old) + labels = audit.labels() + for word in (old, new): + audit.w = word # Geometry unchanged and hash-pinned; retain exact rational geometry. + audit.full() + h, c, _ = audit.interface() + need(all(h.values()) and all(c.values()), 'predecessor interface') + receipts = [] + for name, word in (('original', old), ('replacement', new)): + directory = out / name + directory.mkdir() + records, receipt = export(word, directory) + receipts.append(receipt) + need(receipt['rank_mass'] == 5112 and receipt['copies'] == receipt['erasures'] == 9, 'paid profile') + need(int(receipt['payload']) < 2**104, 'payload cap') + need(receipts[0]['adds'] - receipts[1]['adds'] == 2 * (len(original) - len(replacement)), 'complete scalar bill') + need(receipts[0]['paid_histogram'] == receipts[1]['paid_histogram'], 'paid histogram changed') + controls = [] + controls.append(rejected('omitted local XOR', lambda: local_check(original, replacement[:-1]), 'local integer map')) + controls.append(rejected('F2-neutral positive inflation', lambda: local_check(original, replacement + [(0, 1), (0, 1)]), 'local integer map')) + mutant = copy.deepcopy(new); mutant['C'].pop() + controls.append(rejected('omitted cleanup', lambda: scalar(mutant), 'dirty-column endpoint')) + mutant = copy.deepcopy(new); mutant['C'] = old['C'] + scalar(mutant) # Same F2 inverse, but intentionally outside literal-H4 contract. + controls.append(rejected('stale scalar-valid cleanup', lambda: literal(mutant), 'literal cleanup')) + mutant = copy.deepcopy(new); mutant['D'].pop() + controls.append(rejected('omitted dirty compensation', lambda: scalar(mutant), 'dirty-column endpoint')) + mutant = copy.deepcopy(new); mutant['B'][471][0] = 0 + controls.append(rejected('illegal frame descent', lambda: paths(mutant), 'frame descent')) + bad = copy.deepcopy(cert['factors'][0]); bad['potentials'][-1] += 1 + controls.append(rejected('inflated lower-bound certificate', lambda: factor_audit(original[:17], bad), 'Bellman lower bound')) + bad = copy.deepcopy(cert['factors'][0]); bad['batches'][0][1] = [] + controls.append(rejected('unpaid witness gate', lambda: factor_audit(original[:17], bad), 'batch exact integer sum')) + receipt = {'status': 'PASS_R420_BLOCK7_EXACT_SCHEDULE', 'factor_audits': [a, b], 'local': local, + 'native': receipts, 'columns': 660, 'labels': labels, 'controls': controls, + 'word_sha256': [digest(canonical(old)), digest(canonical(new))], 'kappa': 'unchanged'} + expected = json.loads((HERE / 'EXPECTED.json').read_text()) + need(receipt == expected, 'expected receipt mismatch') + (out / 'receipt.json').write_text(json.dumps(receipt, indent=2, sort_keys=True) + '\n') + print('PASS_R420_BLOCK7_EXACT_SCHEDULE factors=17+24->14+14 ADDs=26916->26890 states=8192 columns=660 controls=8 kappa=unchanged') + return receipt + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--out', type=Path, help='new directory for both words, native records and receipt') + args = parser.parse_args() + try: + if args.out: + # Never overwrite an existing path or place artifacts inside this package. + destination = args.out.resolve() + need(destination != HERE and HERE not in destination.parents, 'output inside package') + destination.mkdir(parents=True, exist_ok=False) + run(destination) + else: + with tempfile.TemporaryDirectory(prefix='r420-block7-') as tmp: + run(Path(tmp)) + except (Reject, OSError, ValueError, KeyError, subprocess.CalledProcessError) as exc: + print('REJECT_R420_BLOCK7_EXACT_SCHEDULE:', exc, file=sys.stderr) + sys.exit(1) From d1634f3b316f2c3a1bb5f93a6117c8ebab9ab011 Mon Sep 17 00:00:00 2001 From: Yuzhou Wang Date: Tue, 13 Oct 2026 13:38:46 +0800 Subject: [PATCH 2/2] Record block-7 sprint result and PR handoff --- research/r420-block7-exact-schedule/CLAIM.md | 13 +++++++++++++ research/r420-block7-exact-schedule/VALIDATION.md | 8 ++++++++ 2 files changed, 21 insertions(+) diff --git a/research/r420-block7-exact-schedule/CLAIM.md b/research/r420-block7-exact-schedule/CLAIM.md index daad72df14..bf9f2ef21c 100644 --- a/research/r420-block7-exact-schedule/CLAIM.md +++ b/research/r420-block7-exact-schedule/CLAIM.md @@ -29,3 +29,16 @@ are not treated as accepted frontiers. - Contributor: Yuzhou Wang / @yzhouwang, with substantial OpenAI Codex assistance. Apache-2.0. No delegated workers or independent human review. + +## Result update (once) + +Completed 2026-10-13 05:39 UTC. Submitted +[PR #789](https://github.com/CrocSwap/integer-mult-bounds/pull/789). +The 41-XOR block is replaced by 28 XORs, with exact fixed-factor minima +14 + 14. Charging the literal reverse cleanup saves 26 native ADDs overall: +26,916 → 26,890. No new κ. All 660 dirty columns and frame paths pass; +fresh 5/9/11-stage native checks pass with 96 bridge-omission controls. +Python 3.9/3.14, optimized/relocated/committed-source replay, source and +certificate controls and selected-record integrity pass. Scope, source pins, +proof, inherited obligations and full validation are in README/VALIDATION. +Final overlap refresh through #786 found no block-7 factor-schedule duplicate. diff --git a/research/r420-block7-exact-schedule/VALIDATION.md b/research/r420-block7-exact-schedule/VALIDATION.md index efc841c89c..4b2ff40d0e 100644 --- a/research/r420-block7-exact-schedule/VALIDATION.md +++ b/research/r420-block7-exact-schedule/VALIDATION.md @@ -75,3 +75,11 @@ compensation forests; #782 concerns intrinsic lattice parity. Neither changes this block or supplies the finite schedule-class certificate. The inspected #681/#691/#754 heads remain those in `SOURCES.json`. No pending implementation was imported and no additive composition claimed. + +Final committed-files-only replay at construction commit +`d8c13a065a942018e41721f859dc97da5249a2e1` passed from a minimal export. +The complete patch applied cleanly to an empty target for these additions; +staged whitespace checks passed. The submission is +[PR #789](https://github.com/CrocSwap/integer-mult-bounds/pull/789). +The subsequent handoff commit changes only this validation record and the +one-time claim result update, with no code or certificate changes.