From a86b65e648f5b004f4aa68b3ed2c7975e8ca0163 Mon Sep 17 00:00:00 2001 From: ross Date: Thu, 15 Oct 2026 05:12:25 +1100 Subject: [PATCH] Prove generic output-bank mixing query erasure --- .../CERTIFICATE.json | 2589 +++++++++++++++++ .../EXPECTED.json | 48 + .../generic-output-mixing-erasure/README.md | 213 ++ .../SOURCES.json | 60 + .../generic-output-mixing-erasure/TASK.json | 137 + .../generic-output-mixing-erasure/VERIFY.json | 47 + .../independent.py | 310 ++ .../test_verify.py | 132 + .../generic-output-mixing-erasure/verify.py | 282 ++ 9 files changed, 3818 insertions(+) create mode 100644 research/generic-output-mixing-erasure/CERTIFICATE.json create mode 100644 research/generic-output-mixing-erasure/EXPECTED.json create mode 100644 research/generic-output-mixing-erasure/README.md create mode 100644 research/generic-output-mixing-erasure/SOURCES.json create mode 100644 research/generic-output-mixing-erasure/TASK.json create mode 100644 research/generic-output-mixing-erasure/VERIFY.json create mode 100644 research/generic-output-mixing-erasure/independent.py create mode 100644 research/generic-output-mixing-erasure/test_verify.py create mode 100644 research/generic-output-mixing-erasure/verify.py diff --git a/research/generic-output-mixing-erasure/CERTIFICATE.json b/research/generic-output-mixing-erasure/CERTIFICATE.json new file mode 100644 index 0000000000..66d04e38ee --- /dev/null +++ b/research/generic-output-mixing-erasure/CERTIFICATE.json @@ -0,0 +1,2589 @@ +{ + "schema_version": 1, + "fixtures": [ + { + "name": "five_source_baseline", + "source_count": 5, + "logical_outputs": 31, + "bank_size": 33, + "masks": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31 + ], + "word": [ + [ + "A", + 0, + 0 + ], + [ + "A", + 2, + 2 + ], + [ + "A", + 5, + 5 + ], + [ + "A", + 6, + 6 + ], + [ + "A", + 11, + 11 + ], + [ + "A", + 13, + 13 + ], + [ + "A", + 15, + 15 + ], + [ + "A", + 20, + 20 + ], + [ + "A", + 23, + 23 + ], + [ + "A", + 27, + 27 + ], + [ + "B", + 0 + ], + [ + "A", + 0, + 0 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 12, + 12 + ], + [ + "A", + 14, + 14 + ], + [ + "A", + 16, + 16 + ], + [ + "A", + 20, + 20 + ], + [ + "A", + 24, + 24 + ], + [ + "A", + 28, + 28 + ], + [ + "B", + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 2, + 2 + ], + [ + "A", + 3, + 3 + ], + [ + "A", + 4, + 4 + ], + [ + "A", + 18, + 18 + ], + [ + "A", + 26, + 26 + ], + [ + "A", + 30, + 30 + ], + [ + "B", + 2 + ], + [ + "A", + 3, + 3 + ], + [ + "A", + 6, + 6 + ], + [ + "A", + 8, + 8 + ], + [ + "A", + 10, + 10 + ], + [ + "A", + 22, + 22 + ], + [ + "B", + 0 + ], + [ + "A", + 4, + 4 + ], + [ + "A", + 5, + 5 + ], + [ + "A", + 7, + 7 + ], + [ + "A", + 9, + 9 + ], + [ + "A", + 21, + 21 + ], + [ + "A", + 25, + 25 + ], + [ + "A", + 29, + 29 + ], + [ + "B", + 3 + ], + [ + "A", + 7, + 7 + ], + [ + "A", + 8, + 8 + ], + [ + "A", + 13, + 13 + ], + [ + "A", + 14, + 14 + ], + [ + "A", + 17, + 17 + ], + [ + "B", + 1 + ], + [ + "A", + 9, + 9 + ], + [ + "A", + 10, + 10 + ], + [ + "A", + 11, + 11 + ], + [ + "A", + 12, + 12 + ], + [ + "A", + 19, + 19 + ], + [ + "A", + 20, + 20 + ], + [ + "B", + 4 + ], + [ + "A", + 17, + 17 + ], + [ + "A", + 25, + 25 + ], + [ + "A", + 27, + 27 + ], + [ + "A", + 28, + 28 + ], + [ + "A", + 30, + 30 + ], + [ + "B", + 2 + ], + [ + "A", + 19, + 19 + ], + [ + "A", + 20, + 20 + ], + [ + "A", + 23, + 23 + ], + [ + "A", + 24, + 24 + ], + [ + "A", + 26, + 26 + ], + [ + "A", + 29, + 29 + ], + [ + "B", + 3 + ], + [ + "A", + 15, + 15 + ], + [ + "A", + 16, + 16 + ], + [ + "A", + 18, + 18 + ], + [ + "A", + 21, + 21 + ], + [ + "A", + 22, + 22 + ], + [ + "B", + 4 + ] + ], + "expected_erased": [ + [ + "A", + 0, + 0 + ], + [ + "A", + 2, + 2 + ], + [ + "A", + 5, + 5 + ], + [ + "A", + 6, + 6 + ], + [ + "A", + 11, + 11 + ], + [ + "A", + 13, + 13 + ], + [ + "A", + 15, + 15 + ], + [ + "A", + 20, + 20 + ], + [ + "A", + 23, + 23 + ], + [ + "A", + 27, + 27 + ], + [ + "B", + 0 + ], + [ + "A", + 0, + 0 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 12, + 12 + ], + [ + "A", + 14, + 14 + ], + [ + "A", + 16, + 16 + ], + [ + "A", + 20, + 20 + ], + [ + "A", + 24, + 24 + ], + [ + "A", + 28, + 28 + ], + [ + "B", + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 2, + 2 + ], + [ + "A", + 3, + 3 + ], + [ + "A", + 4, + 4 + ], + [ + "A", + 18, + 18 + ], + [ + "A", + 26, + 26 + ], + [ + "A", + 30, + 30 + ], + [ + "B", + 2 + ], + [ + "A", + 3, + 3 + ], + [ + "A", + 6, + 6 + ], + [ + "A", + 8, + 8 + ], + [ + "A", + 10, + 10 + ], + [ + "A", + 22, + 22 + ], + [ + "B", + 0 + ], + [ + "A", + 4, + 4 + ], + [ + "A", + 5, + 5 + ], + [ + "A", + 7, + 7 + ], + [ + "A", + 9, + 9 + ], + [ + "A", + 21, + 21 + ], + [ + "A", + 25, + 25 + ], + [ + "A", + 29, + 29 + ], + [ + "B", + 3 + ], + [ + "A", + 7, + 7 + ], + [ + "A", + 8, + 8 + ], + [ + "A", + 13, + 13 + ], + [ + "A", + 14, + 14 + ], + [ + "A", + 17, + 17 + ], + [ + "B", + 1 + ], + [ + "A", + 9, + 9 + ], + [ + "A", + 10, + 10 + ], + [ + "A", + 11, + 11 + ], + [ + "A", + 12, + 12 + ], + [ + "A", + 19, + 19 + ], + [ + "A", + 20, + 20 + ], + [ + "B", + 4 + ], + [ + "A", + 17, + 17 + ], + [ + "A", + 25, + 25 + ], + [ + "A", + 27, + 27 + ], + [ + "A", + 28, + 28 + ], + [ + "A", + 30, + 30 + ], + [ + "B", + 2 + ], + [ + "A", + 19, + 19 + ], + [ + "A", + 20, + 20 + ], + [ + "A", + 23, + 23 + ], + [ + "A", + 24, + 24 + ], + [ + "A", + 26, + 26 + ], + [ + "A", + 29, + 29 + ], + [ + "B", + 3 + ], + [ + "A", + 15, + 15 + ], + [ + "A", + 16, + 16 + ], + [ + "A", + 18, + 18 + ], + [ + "A", + 21, + 21 + ], + [ + "A", + 22, + 22 + ], + [ + "B", + 4 + ] + ] + }, + { + "name": "five_source_dirty_output_helpers", + "source_count": 5, + "logical_outputs": 31, + "bank_size": 33, + "masks": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31 + ], + "word": [ + [ + "X", + 31, + 0 + ], + [ + "A", + 0, + 31 + ], + [ + "X", + 31, + 0 + ], + [ + "A", + 0, + 31 + ], + [ + "X", + 31, + 2 + ], + [ + "A", + 2, + 31 + ], + [ + "X", + 31, + 2 + ], + [ + "A", + 2, + 31 + ], + [ + "X", + 32, + 5 + ], + [ + "A", + 5, + 32 + ], + [ + "X", + 32, + 5 + ], + [ + "A", + 5, + 32 + ], + [ + "X", + 31, + 6 + ], + [ + "A", + 6, + 31 + ], + [ + "X", + 31, + 6 + ], + [ + "A", + 6, + 31 + ], + [ + "X", + 32, + 11 + ], + [ + "A", + 11, + 32 + ], + [ + "X", + 32, + 11 + ], + [ + "A", + 11, + 32 + ], + [ + "X", + 32, + 13 + ], + [ + "A", + 13, + 32 + ], + [ + "X", + 32, + 13 + ], + [ + "A", + 13, + 32 + ], + [ + "X", + 32, + 15 + ], + [ + "A", + 15, + 32 + ], + [ + "X", + 32, + 15 + ], + [ + "A", + 15, + 32 + ], + [ + "X", + 31, + 20 + ], + [ + "A", + 20, + 31 + ], + [ + "X", + 31, + 20 + ], + [ + "A", + 20, + 31 + ], + [ + "X", + 32, + 23 + ], + [ + "A", + 23, + 32 + ], + [ + "X", + 32, + 23 + ], + [ + "A", + 23, + 32 + ], + [ + "X", + 32, + 27 + ], + [ + "A", + 27, + 32 + ], + [ + "X", + 32, + 27 + ], + [ + "A", + 27, + 32 + ], + [ + "B", + 0 + ], + [ + "X", + 31, + 0 + ], + [ + "A", + 0, + 31 + ], + [ + "X", + 31, + 0 + ], + [ + "A", + 0, + 31 + ], + [ + "X", + 32, + 1 + ], + [ + "A", + 1, + 32 + ], + [ + "X", + 32, + 1 + ], + [ + "A", + 1, + 32 + ], + [ + "X", + 31, + 12 + ], + [ + "A", + 12, + 31 + ], + [ + "X", + 31, + 12 + ], + [ + "A", + 12, + 31 + ], + [ + "X", + 31, + 14 + ], + [ + "A", + 14, + 31 + ], + [ + "X", + 31, + 14 + ], + [ + "A", + 14, + 31 + ], + [ + "X", + 31, + 16 + ], + [ + "A", + 16, + 31 + ], + [ + "X", + 31, + 16 + ], + [ + "A", + 16, + 31 + ], + [ + "X", + 31, + 20 + ], + [ + "A", + 20, + 31 + ], + [ + "X", + 31, + 20 + ], + [ + "A", + 20, + 31 + ], + [ + "X", + 31, + 24 + ], + [ + "A", + 24, + 31 + ], + [ + "X", + 31, + 24 + ], + [ + "A", + 24, + 31 + ], + [ + "X", + 31, + 28 + ], + [ + "A", + 28, + 31 + ], + [ + "X", + 31, + 28 + ], + [ + "A", + 28, + 31 + ], + [ + "B", + 1 + ], + [ + "X", + 32, + 1 + ], + [ + "A", + 1, + 32 + ], + [ + "X", + 32, + 1 + ], + [ + "A", + 1, + 32 + ], + [ + "X", + 31, + 2 + ], + [ + "A", + 2, + 31 + ], + [ + "X", + 31, + 2 + ], + [ + "A", + 2, + 31 + ], + [ + "X", + 32, + 3 + ], + [ + "A", + 3, + 32 + ], + [ + "X", + 32, + 3 + ], + [ + "A", + 3, + 32 + ], + [ + "X", + 31, + 4 + ], + [ + "A", + 4, + 31 + ], + [ + "X", + 31, + 4 + ], + [ + "A", + 4, + 31 + ], + [ + "X", + 31, + 18 + ], + [ + "A", + 18, + 31 + ], + [ + "X", + 31, + 18 + ], + [ + "A", + 18, + 31 + ], + [ + "X", + 31, + 26 + ], + [ + "A", + 26, + 31 + ], + [ + "X", + 31, + 26 + ], + [ + "A", + 26, + 31 + ], + [ + "X", + 31, + 30 + ], + [ + "A", + 30, + 31 + ], + [ + "X", + 31, + 30 + ], + [ + "A", + 30, + 31 + ], + [ + "B", + 2 + ], + [ + "X", + 32, + 3 + ], + [ + "A", + 3, + 32 + ], + [ + "X", + 32, + 3 + ], + [ + "A", + 3, + 32 + ], + [ + "X", + 31, + 6 + ], + [ + "A", + 6, + 31 + ], + [ + "X", + 31, + 6 + ], + [ + "A", + 6, + 31 + ], + [ + "X", + 31, + 8 + ], + [ + "A", + 8, + 31 + ], + [ + "X", + 31, + 8 + ], + [ + "A", + 8, + 31 + ], + [ + "X", + 31, + 10 + ], + [ + "A", + 10, + 31 + ], + [ + "X", + 31, + 10 + ], + [ + "A", + 10, + 31 + ], + [ + "X", + 31, + 22 + ], + [ + "A", + 22, + 31 + ], + [ + "X", + 31, + 22 + ], + [ + "A", + 22, + 31 + ], + [ + "B", + 0 + ], + [ + "X", + 31, + 4 + ], + [ + "A", + 4, + 31 + ], + [ + "X", + 31, + 4 + ], + [ + "A", + 4, + 31 + ], + [ + "X", + 32, + 5 + ], + [ + "A", + 5, + 32 + ], + [ + "X", + 32, + 5 + ], + [ + "A", + 5, + 32 + ], + [ + "X", + 32, + 7 + ], + [ + "A", + 7, + 32 + ], + [ + "X", + 32, + 7 + ], + [ + "A", + 7, + 32 + ], + [ + "X", + 32, + 9 + ], + [ + "A", + 9, + 32 + ], + [ + "X", + 32, + 9 + ], + [ + "A", + 9, + 32 + ], + [ + "X", + 32, + 21 + ], + [ + "A", + 21, + 32 + ], + [ + "X", + 32, + 21 + ], + [ + "A", + 21, + 32 + ], + [ + "X", + 32, + 25 + ], + [ + "A", + 25, + 32 + ], + [ + "X", + 32, + 25 + ], + [ + "A", + 25, + 32 + ], + [ + "X", + 32, + 29 + ], + [ + "A", + 29, + 32 + ], + [ + "X", + 32, + 29 + ], + [ + "A", + 29, + 32 + ], + [ + "B", + 3 + ], + [ + "X", + 32, + 7 + ], + [ + "A", + 7, + 32 + ], + [ + "X", + 32, + 7 + ], + [ + "A", + 7, + 32 + ], + [ + "X", + 31, + 8 + ], + [ + "A", + 8, + 31 + ], + [ + "X", + 31, + 8 + ], + [ + "A", + 8, + 31 + ], + [ + "X", + 32, + 13 + ], + [ + "A", + 13, + 32 + ], + [ + "X", + 32, + 13 + ], + [ + "A", + 13, + 32 + ], + [ + "X", + 31, + 14 + ], + [ + "A", + 14, + 31 + ], + [ + "X", + 31, + 14 + ], + [ + "A", + 14, + 31 + ], + [ + "X", + 32, + 17 + ], + [ + "A", + 17, + 32 + ], + [ + "X", + 32, + 17 + ], + [ + "A", + 17, + 32 + ], + [ + "B", + 1 + ], + [ + "X", + 32, + 9 + ], + [ + "A", + 9, + 32 + ], + [ + "X", + 32, + 9 + ], + [ + "A", + 9, + 32 + ], + [ + "X", + 31, + 10 + ], + [ + "A", + 10, + 31 + ], + [ + "X", + 31, + 10 + ], + [ + "A", + 10, + 31 + ], + [ + "X", + 32, + 11 + ], + [ + "A", + 11, + 32 + ], + [ + "X", + 32, + 11 + ], + [ + "A", + 11, + 32 + ], + [ + "X", + 31, + 12 + ], + [ + "A", + 12, + 31 + ], + [ + "X", + 31, + 12 + ], + [ + "A", + 12, + 31 + ], + [ + "X", + 32, + 19 + ], + [ + "A", + 19, + 32 + ], + [ + "X", + 32, + 19 + ], + [ + "A", + 19, + 32 + ], + [ + "X", + 31, + 20 + ], + [ + "A", + 20, + 31 + ], + [ + "X", + 31, + 20 + ], + [ + "A", + 20, + 31 + ], + [ + "B", + 4 + ], + [ + "X", + 32, + 17 + ], + [ + "A", + 17, + 32 + ], + [ + "X", + 32, + 17 + ], + [ + "A", + 17, + 32 + ], + [ + "X", + 32, + 25 + ], + [ + "A", + 25, + 32 + ], + [ + "X", + 32, + 25 + ], + [ + "A", + 25, + 32 + ], + [ + "X", + 32, + 27 + ], + [ + "A", + 27, + 32 + ], + [ + "X", + 32, + 27 + ], + [ + "A", + 27, + 32 + ], + [ + "X", + 31, + 28 + ], + [ + "A", + 28, + 31 + ], + [ + "X", + 31, + 28 + ], + [ + "A", + 28, + 31 + ], + [ + "X", + 31, + 30 + ], + [ + "A", + 30, + 31 + ], + [ + "X", + 31, + 30 + ], + [ + "A", + 30, + 31 + ], + [ + "B", + 2 + ], + [ + "X", + 32, + 19 + ], + [ + "A", + 19, + 32 + ], + [ + "X", + 32, + 19 + ], + [ + "A", + 19, + 32 + ], + [ + "X", + 31, + 20 + ], + [ + "A", + 20, + 31 + ], + [ + "X", + 31, + 20 + ], + [ + "A", + 20, + 31 + ], + [ + "X", + 32, + 23 + ], + [ + "A", + 23, + 32 + ], + [ + "X", + 32, + 23 + ], + [ + "A", + 23, + 32 + ], + [ + "X", + 31, + 24 + ], + [ + "A", + 24, + 31 + ], + [ + "X", + 31, + 24 + ], + [ + "A", + 24, + 31 + ], + [ + "X", + 31, + 26 + ], + [ + "A", + 26, + 31 + ], + [ + "X", + 31, + 26 + ], + [ + "A", + 26, + 31 + ], + [ + "X", + 32, + 29 + ], + [ + "A", + 29, + 32 + ], + [ + "X", + 32, + 29 + ], + [ + "A", + 29, + 32 + ], + [ + "B", + 3 + ], + [ + "X", + 32, + 15 + ], + [ + "A", + 15, + 32 + ], + [ + "X", + 32, + 15 + ], + [ + "A", + 15, + 32 + ], + [ + "X", + 31, + 16 + ], + [ + "A", + 16, + 31 + ], + [ + "X", + 31, + 16 + ], + [ + "A", + 16, + 31 + ], + [ + "X", + 31, + 18 + ], + [ + "A", + 18, + 31 + ], + [ + "X", + 31, + 18 + ], + [ + "A", + 18, + 31 + ], + [ + "X", + 32, + 21 + ], + [ + "A", + 21, + 32 + ], + [ + "X", + 32, + 21 + ], + [ + "A", + 21, + 32 + ], + [ + "X", + 31, + 22 + ], + [ + "A", + 22, + 31 + ], + [ + "X", + 31, + 22 + ], + [ + "A", + 22, + 31 + ], + [ + "B", + 4 + ] + ], + "expected_erased": [ + [ + "A", + 0, + 0 + ], + [ + "A", + 2, + 2 + ], + [ + "A", + 5, + 5 + ], + [ + "A", + 6, + 6 + ], + [ + "A", + 11, + 11 + ], + [ + "A", + 13, + 13 + ], + [ + "A", + 15, + 15 + ], + [ + "A", + 20, + 20 + ], + [ + "A", + 23, + 23 + ], + [ + "A", + 27, + 27 + ], + [ + "B", + 0 + ], + [ + "A", + 0, + 0 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 12, + 12 + ], + [ + "A", + 14, + 14 + ], + [ + "A", + 16, + 16 + ], + [ + "A", + 20, + 20 + ], + [ + "A", + 24, + 24 + ], + [ + "A", + 28, + 28 + ], + [ + "B", + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 2, + 2 + ], + [ + "A", + 3, + 3 + ], + [ + "A", + 4, + 4 + ], + [ + "A", + 18, + 18 + ], + [ + "A", + 26, + 26 + ], + [ + "A", + 30, + 30 + ], + [ + "B", + 2 + ], + [ + "A", + 3, + 3 + ], + [ + "A", + 6, + 6 + ], + [ + "A", + 8, + 8 + ], + [ + "A", + 10, + 10 + ], + [ + "A", + 22, + 22 + ], + [ + "B", + 0 + ], + [ + "A", + 4, + 4 + ], + [ + "A", + 5, + 5 + ], + [ + "A", + 7, + 7 + ], + [ + "A", + 9, + 9 + ], + [ + "A", + 21, + 21 + ], + [ + "A", + 25, + 25 + ], + [ + "A", + 29, + 29 + ], + [ + "B", + 3 + ], + [ + "A", + 7, + 7 + ], + [ + "A", + 8, + 8 + ], + [ + "A", + 13, + 13 + ], + [ + "A", + 14, + 14 + ], + [ + "A", + 17, + 17 + ], + [ + "B", + 1 + ], + [ + "A", + 9, + 9 + ], + [ + "A", + 10, + 10 + ], + [ + "A", + 11, + 11 + ], + [ + "A", + 12, + 12 + ], + [ + "A", + 19, + 19 + ], + [ + "A", + 20, + 20 + ], + [ + "B", + 4 + ], + [ + "A", + 17, + 17 + ], + [ + "A", + 25, + 25 + ], + [ + "A", + 27, + 27 + ], + [ + "A", + 28, + 28 + ], + [ + "A", + 30, + 30 + ], + [ + "B", + 2 + ], + [ + "A", + 19, + 19 + ], + [ + "A", + 20, + 20 + ], + [ + "A", + 23, + 23 + ], + [ + "A", + 24, + 24 + ], + [ + "A", + 26, + 26 + ], + [ + "A", + 29, + 29 + ], + [ + "B", + 3 + ], + [ + "A", + 15, + 15 + ], + [ + "A", + 16, + 16 + ], + [ + "A", + 18, + 18 + ], + [ + "A", + 21, + 21 + ], + [ + "A", + 22, + 22 + ], + [ + "B", + 4 + ] + ] + }, + { + "name": "odd_reader_identity", + "source_count": 1, + "logical_outputs": 1, + "bank_size": 2, + "masks": [ + 0 + ], + "word": [ + [ + "A", + 0, + 0 + ], + [ + "A", + 0, + 1 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 0, + 0 + ], + [ + "X", + 0, + 1 + ] + ], + "expected_erased": [ + [ + "A", + 0, + 0 + ], + [ + "A", + 0, + 0 + ] + ] + } + ], + "common_reader_control": { + "name": "common_reader_scope_control", + "source_count": 1, + "logical_outputs": 2, + "bank_size": 2, + "masks": [ + 1, + 1 + ], + "word": [ + [ + "X", + 0, + 1 + ], + [ + "A", + 0, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "B", + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 0, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "B", + 0 + ] + ] + } +} diff --git a/research/generic-output-mixing-erasure/EXPECTED.json b/research/generic-output-mixing-erasure/EXPECTED.json new file mode 100644 index 0000000000..1ba8dfa728 --- /dev/null +++ b/research/generic-output-mixing-erasure/EXPECTED.json @@ -0,0 +1,48 @@ +{ + "certificate_sha256": "7edebd7537a23a48b144ff60fade66e94cb0e6c1167eca44e18ad030ace7863e", + "coverage_histogram": { + "16": 42, + "19": 120, + "21": 180, + "22": 56, + "23": 45, + "24": 220, + "26": 110, + "28": 150, + "31": 22 + }, + "five_source_map_optimum": 74, + "fixtures": [ + { + "dirty_bank_rows": 33, + "erased_map_calls": 74, + "map_calls": 74, + "mixing_xors": 0, + "name": "five_source_baseline" + }, + { + "dirty_bank_rows": 33, + "erased_map_calls": 74, + "map_calls": 138, + "mixing_xors": 128, + "name": "five_source_dirty_output_helpers" + }, + { + "dirty_bank_rows": 2, + "erased_map_calls": 2, + "map_calls": 3, + "mixing_xors": 2, + "name": "odd_reader_identity" + } + ], + "frame_census": { + "frames": 168, + "input_readouts": 1728 + }, + "max_coverage": 31, + "negative_controls": 7, + "no_new_kappa": true, + "pairings": 945, + "schema_version": 1, + "weighted_fixture_optimum": 182 +} diff --git a/research/generic-output-mixing-erasure/README.md b/research/generic-output-mixing-erasure/README.md new file mode 100644 index 0000000000..cae68a4d23 --- /dev/null +++ b/research/generic-output-mixing-erasure/README.md @@ -0,0 +1,213 @@ +# Generic output mixing can be erased + +**Scoped recursive-interface theorem; no new kappa.** Reversible scalar mixing +among output rows and any finite number of dirty output-only helpers cannot +reduce any fixed additive, port-independent map-call tariff for the generic +one-connector batch. Every valid mixed word has an ordinary word with the same +B-call timeline and no more calls of any individual reader A_i. + +Consequently the five-source, all-31-mask instance still needs exactly **74 +complete A/B calls**, even granting mixing free. Its previously established +heterogeneous fixture optimum remains **182**. These numbers are inherited +corollaries; the new contribution is the all-parameter erasure theorem. + +This adds output-bank mixing to the fixed alphabet of Ross Richardson's +[PR943/934](../universal-connector-boundary/README.md). Adam Gall's +[PR1915](../connector-frame-rigidity/README.md) and Arham Garg's +[73-map exclusion](../connector-frame-73-exclusion/README.md) instead change +the connector's coordinates and explicitly exclude output mixing. We do not +claim the combined connector-frame/output-mixing alphabet is covered. + +## Contract and all-parameter proof + +Let m,n,R be nonnegative integers, R >= n, and L >= 1. There are distinct, +arbitrarily dirty L-bit source rows x_j, one connector z, and an R-row bank Y. +The first n bank rows are outputs; the rest are helpers. Fix an n-by-m binary +matrix M. All A_i and B_j range independently over exact F2-linear endomorphisms +of F2^L, including zero, singular and noncommuting maps. Independence permits +separate assignments; it does not mean the matrices must be pairwise distinct. + +The completed endpoint is + +``` +x_j' = x_j; z' = z; +y_i' = y_i + sum_j M_ij A_i B_j x_j (i < n); +y_r' = y_r (r >= n). +``` + +The operations are complete calls B_j: z += B_j x_j; reader calls +A_i@p: y_p += A_i z; and paid scalar bank transformations Y <- F Y for +F in GL_R(F2). The theorem grants arbitrary physical reader ports p as a +favorable relaxation, so it also excludes savings when each A_i is restricted +to its original port i. The mixed fixture below uses the more permissive ports. +The bank transformations act only on the row index, never on sources, z, or +coordinates inside an L-bit row. + +The word, labels, ports and F matrices are fixed independently of all map +entries and data. They may depend on M,m,n,R,L. Every child preserves its +non-target rows and restores private scratch and promised heads. Root rows +and all bank helpers are reserved against child scratch. Outputs are observed +only at completed batch exit. There is no clean full row, alias, overwrite, +source mutation, direct product call or data-dependent branch. + +Let P be the cumulative bank frame, initially I, updated by P <- F P. +Normalize U=P^-1 Y. Mixing leaves U unchanged. At a reader event e=(A_i@p), +write v_e=P_e^-1 e_p and let q_e be the parity vector of preceding B calls. +Then this event adds + +``` +v_e A_i (z_initial + sum_j q_ej B_j x_j) +``` + +to U. Neither mixing nor readers change z, so q_e depends only on the B +timeline. Setting every A_i=0 and varying all bank dirt forces P_final=I; +L>=1 is sufficient. Thus the final contribution is the sum of these terms. + +For each i, set every other A_k to zero and project to logical row i. Universal +correctness gives + +``` +sum_(e labelled A_i) (v_e)_i A_i z_e = sum_j M_ij A_i B_j x_j. +``` + +Keep an event labelled A_i exactly when (v_e)_i=1, retarget it to logical row i, +and delete all bank transformations. Preserve every B call and the relative +order of retained events. Each retained reader sees the same z_e. The displayed +identity gives its required output, while the B timeline restores z and the +unused helpers remain untouched. Each event is retained at most once and +keeps its label. This proves the componentwise bound for all stated parameters. +No commutativity or large-dimension polynomial-independence premise is needed. + +Equivalently, validity is exactly the following finite coefficient test: + +``` +P_final=I, q_final=0; +sum_(e:A_i) (v_e)_r = 0 for every i,r; +sum_(e:A_i) (v_e)_r q_ej = delta_ri M_ij for every i,r,j. +``` + +Necessity follows by independent zero/identity map specializations and varying +each initial source or connector coordinate; sufficiency follows by summing +the event formula. The checker represents these coefficients as integers of +bits and explicitly checks every helper row. Its resource limits (64 sources, +256 outputs, 512 bank rows) limit this implementation, not the written theorem. +Zero rows, zero source/output counts and R=0 obey the same proof. For L=0 the +endpoint is vacuous, but P_final=I need not follow; that convention is excluded. + +## Consequences and essential scope controls + +Erasure sends any mixed word of at most 73 map calls to an ordinary word of +at most 73 calls. The ordinary support floor is 72: twice each of five B maps +and 31 A maps. At 72, the 945 canonical paired-source words cover at most 31 +of 32 masks; none supports all 31 nonzero masks with paired readouts. Ordinary +parity excludes 73. The credited 74-call construction is allowed with every +additional helper untouched, proving exactness in the extended model. + +Ordinary parity must **not** be asserted for the mixed word. At fixed z, let +C be h += y. The word A@y, A@h, C, A@y, C is the identity for arbitrary dirt +and arbitrary A, despite using three A calls. The fixed odd-reader fixture +checks this and its erasure to two cancelling calls. + +For B prices (1,4,10,16,28) and unit A prices, every ordinary word pays at +least 180. If it has ten B calls, a missing mask needs at least two extra A +calls; if it has at least twelve B calls, it pays at least two extra units +for B. Both cases cost at least 182, attained by the inherited word. Cinna +Davis's [PR1770 weighted result](../weighted-connector-readouts-seed1275309492/README.md) +is credited. Erasure preserves this optimum; it does not solve arbitrary +unequal-price instances. + +Independent readers are essential. With one source, two outputs and A_0=A_1=A, +a paid output conjugation broadcasts one dirty-safe ABx update to both outputs, +using two A calls where an unframed implementation needs four. The certificate +has a literal eight-event witness with four charged output XORs. Exhaustive +2-by-2 matrix tests show its endpoint is correct exactly when +(A_0+A_1)B=0: 928 of 4096 triples, including all 256 equal-reader cases. +Its failure for independently chosen readers is checked explicitly. This is +a small scope witness, not a new common-reader broadcast construction; +[PR1707](../common-a-broadcast-readout-seed4a52/README.md) already supplies +that changed interface and its fully charged five-source construction. + +## Complete invoice and limits + +For nonnegative fixed **target-port-independent** complete prices a_i,b_j, + +``` +C_maps(W) = sum_i a_i N_Ai + sum_j b_j N_Bj; +C_maps(erase(W)) <= C_maps(W). +C_total(W) = I(W) + P(W) + D(W) + C_maps(W) + sum_F C_F(W). +``` + +I is admission/layout, P is coefficient/frame preparation, D is instruction +construction/access/dispatch, and each C_F includes the actual mixing +implementation, access, routing and cleanup. All complete child prices include +arithmetic, source/coefficient access, private restoration, frames and head +return. With nonnegative mixing charges the optimum additive macro tariff is +unchanged, since ordinary words are also allowed. The favorable free-mixing +relaxation already fails to improve it, so no larger mixing search is justified +under these hypotheses. + +Retargeting A calls can change port-dependent routing, instruction travel, +layout and hosting costs. Those quantities are not dominated by this proof. +The theorem does not instantiate these maps inside the selected supplier, +construct a physical child implementation, prove a recursive moment improvement, +or settle precision, common-label realization, full-row reservation, tape, +compiler, analytic transfer or intermediate delivery cuts. Non-scalar block +frames, output/connector mixing, restricted/shared readers and nonbinary or +rounded operations require separate analysis. No selected frontier changes, +full cold replay, formal-kernel proof or independent human review are claimed. + +## Reproduce and covered evidence + +From the repository root, with CPython 3.12 and no dependencies: + +``` +python3.12 -I -B scripts/research_package.py --package research/generic-output-mixing-erasure +``` + +The registered run checks source pins, the fixed CERTIFICATE.json and +EXPECTED.json, a separate independent oracle, and seven behavioral test groups. +Verification is read-only and fails on missing evidence. Explicit generation +uses verify.py --write-expected NEW_PATH and refuses to overwrite a file. + +| Evidence | Exact scope | +|---|---| +| Written theorem | Every M,L>=1 and finite R>=n in the contract above | +| Primary coefficients | All dirty rows and labelled coefficients, both orientations; 74-call baseline and 138-map/128-XOR helper decoration erase to the same 74-call word; odd-reader identity erases 3 to 2 | +| Independent algebra | Sparse noncommutative terms on every original input vector; backward suffix influence computes erasure without using forward inverses | +| Two source enumerators | Restricted-growth words versus least-unmatched endpoint pairings; all 945, identical full coverage histogram | +| Output frame census | Every one of 168 GL(3,2) frames around the stated two-source/three-output batch; 1728 total input readouts | +| Short-word census | Every one of 19531 words of length at most six in the five-letter one-source/one-reader/two-bank alphabet; 76 valid, 44 with mixing; every valid word erases correctly | +| Matrix oracle | All 256 two-by-two A/B pairs; all 4096 common-reader triples; explicit noncommuting reversed-product failure | +| Failure controls | Missing connector restoration/readout, helper-only defect with correct logical outputs, residual output frame, aliased XOR, typed index, independent-reader violation; real coefficient/frame detector deletion is detected | +| Package behavior | Normal/optimized relocated unchanged replay; missing/corrupt/typed/balanced receipt rejection; missing/duplicate fixture, erasure and source drift; generation/no-overwrite | + +Finite evidence supports the implementations; it does not replace the +all-parameter argument or constitute a proof-assistant theorem. + +## Provenance + +Base c676548106012571fefa1dce0ec16f1bcfe11dce; selector nonce +779e702f7c4ee535de2ee386c8e4f4bf; refined connector-alphabet-change card. +[TASK.json](TASK.json) records scope, overlap and exact predecessor heads; +[SOURCES.json](SOURCES.json) pins all inputs by Git blob and SHA256. The selected +record remains SHA256 10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32, +conditional kappa 0.001672660197076918, with complex side binding. Its source +bindings were checked, not its full frontier1094 cold replay. + +## Open next questions + +The useful next question is whether one selected call family has a nontrivial +known relation among its reader maps that invalidates independent isolation +and admits a fully priced shared-reader realization. First extract a pinned +family's exact reader matrices, labels and complete target-port prices; then +test a two-output identity and charge routing/restoration. The blocker is the +absence here of such a selected-supplier occurrence. Repeating universal +scalar output-mixing searches would not answer that changed question. + +Credit Ross Richardson's PR943/934 and retained dirty-commutator/fanout lineage +(including @shhxera and Chafik Boukhalfa), Adam Gall, Arham Garg, Cinna Davis, +and PR1707's 1337isnot1337. Prepared by Ross Richardson with substantial +OpenAI Codex assistance in proof, independent algebra, implementation and +writing. The recursive-interface and exact-circuit-verification specialists +performed separate AI-agent checks. New material is Apache-2.0; all predecessor +inputs and notices remain unchanged. diff --git a/research/generic-output-mixing-erasure/SOURCES.json b/research/generic-output-mixing-erasure/SOURCES.json new file mode 100644 index 0000000000..bc6c6fa54a --- /dev/null +++ b/research/generic-output-mixing-erasure/SOURCES.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "base_commit": "c676548106012571fefa1dce0ec16f1bcfe11dce", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/connector-frame-73-exclusion/README.md", + "usage": "input", + "git_blob": "101898d88778459177fcd5a5a4a45a7ba949df6b", + "sha256": "ec3cf13bb97839832e5416f437b6a8dfd622468a1864bbb5552f17f0c43a1bcf" + }, + { + "path": "research/connector-frame-rigidity/README.md", + "usage": "input", + "git_blob": "8f792e62700ec3809075b500f233cee00f3543fe", + "sha256": "d4c5aea3ecc0e988dfd01ee9e47381d813a736cf7eec96eb4f352ab4dc6f3872" + }, + { + "path": "research/universal-connector-boundary/CERTIFICATE.json", + "usage": "input", + "git_blob": "079e3e1441dc07c2f0536e9527acf290e51ea9c0", + "sha256": "e733746ba3e5151c829b4e8728bfff5ae3ed24d8d203eb77c735d20758e8266a" + }, + { + "path": "research/universal-connector-boundary/NOTICE.md", + "usage": "input", + "git_blob": "d9afdf81f656278dab69239f0fd94924f97df87b", + "sha256": "1172648a1883827399d5103a9916deaa4314e4ee2c28653c183890f6bd5a7a17" + }, + { + "path": "research/universal-connector-boundary/README.md", + "usage": "input", + "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f", + "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476" + }, + { + "path": "research/weighted-connector-readouts-seed1275309492/README.md", + "usage": "input", + "git_blob": "2cff98d7c4b8126a41738d3a89356137b43bdbdb", + "sha256": "ce3feb4bac440f3c0327fdffee93d721f1b7b9e9170e470be5a3a78c41e6fa2d" + }, + { + "path": "research/common-a-broadcast-readout-seed4a52/README.md", + "usage": "input", + "git_blob": "f421836303295327787b29e886dedc6ab0d949b7", + "sha256": "f76891c6915a55ea906b4f5f58678134fd9f7bc4d7988f45d98d8dd0f06cc541" + } + ] +} diff --git a/research/generic-output-mixing-erasure/TASK.json b/research/generic-output-mixing-erasure/TASK.json new file mode 100644 index 0000000000..aef2aca52d --- /dev/null +++ b/research/generic-output-mixing-erasure/TASK.json @@ -0,0 +1,137 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 3, + "base_commit": "c676548106012571fefa1dce0ec16f1bcfe11dce", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free.", + "first_step": { + "command": [ + "python3", + "-B", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "refined", + "actual_scope": "Prove or falsify componentwise reader-query erasure after adding arbitrary paid scalar output-bank mixing and any finite dirty output-only helper bank; allow arbitrary physical reader ports as a favorable relaxation.", + "scope_change_reason": "The inherited alphabet forbids output mixing. This result adds that operation family, with source and connector unchanged, and grants reader retargeting for a stronger obstruction. It is distinct from connector-coordinate frames and common-reader broadcast.", + "bottleneck_link": "A precise obstruction to one changed recursive interface; no selected supplier occurrence is asserted. Generic output mixing cannot improve its full fixed-port-independent map tariff, even in the favorable free-mixing relaxation.", + "budget_minutes": 60, + "stop_rule": "Stop construction searches once an all-parameter erasure proof or a smallest counterexample is independently checked; reserve final work for exact controls and handoff.", + "outcome": "negative-result", + "evidence": "README.md proof; CERTIFICATE.json and EXPECTED.json; verify.py normalized coefficients; independent.py noncommutative/suffix/matrix oracles; test_verify.py behavior controls.", + "author": "Ross Richardson with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance; math-recursive-interfaces derived/reviewed the proof, math-exact-circuit-verification implemented a separate oracle and reviewed the mathematical scope; no independent human or formal-kernel review.", + "open_questions": [ + { + "question": "Does a selected call family have known reader relations permitting a fully priced output-sharing construction?", + "why_it_matters": "Reader independence is necessary for erasure; a concrete relation changes the interface rather than repeating an excluded search.", + "first_step": "Extract exact reader matrices, labels and per-port complete prices from one pinned selected family, then check a two-output sharing identity with restoration.", + "blocked_by": "No such selected-family occurrence or physical routing tariff is supplied here." + } + ], + "selector_seed": "779e702f7c4ee535de2ee386c8e4f4bf", + "scope_key": "generic-reader-output-bank-erasure-all-finite-R", + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2043", + "predecessors": [ + { + "pr": 943, + "head": "cf360b4b09b7d0419decdd6ac85421fefed55bdd", + "credit": "Ross Richardson; universal connector and original 945-pairing boundary" + }, + { + "pr": 1915, + "head": "d30d64fea909219c364b11c2452f2207326e2b1f", + "credit": "Adam Gall; connector-coordinate frame normalization" + }, + { + "head": "aa0de6522ecb1c22cd2ee435983b24dbd2842551", + "credit": "Arham Garg; 73-map connector-frame exclusion", + "pr": 1945 + }, + { + "pr": 1770, + "head": "caae2d1a0b4497fbd5a7cd2d057d9a9b099f8873", + "credit": "Cinna Davis; weighted five-source optimum182" + }, + { + "pr": 1707, + "head": "3d2e634e046ac4fbf07ddbfb0e59da4cf9907f4e", + "credit": "1337isnot1337; common-A broadcast interface" + } + ], + "overlap": { + "entry_coverage": { + "open_prs": { + "fetched_at": "2026-10-14T17:57:03.213308+00:00", + "complete_pagination": true, + "records": 364 + }, + "discussions": { + "fetched_at": "2026-10-14T17:59:19.158000+00:00", + "complete_pagination": true, + "records": 680 + } + }, + "entry_warnings": [], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "distinction": "Output-only scalar mixing with independent generic readers; not connector frames, common-A broadcast, clean connector, source mixing or output-feedback.", + "submission_coverage": { + "open_prs": { + "fetched_at": "2026-10-14T18:08:02.884496+00:00", + "complete_pagination": true, + "records": 328 + }, + "discussions": { + "fetched_at": "2026-10-14T18:10:06.759851+00:00", + "complete_pagination": true, + "records": 691 + } + }, + "submission_warnings": [], + "submission_searched_at": "2026-10-14T18:10:06.858815+00:00" + }, + "result_summary": "All-parameter written erasure theorem with exact finite verification; no new kappa.", + "integration_base": "e112d71c8d7bb32435debcc54df932593dd8223a", + "validation": { + "environment": "CPython 3.12.12; macOS arm64; standard library only", + "registered_command": "python3.12 -I -B scripts/research_package.py --package research/generic-output-mixing-erasure", + "registered_result": "PASS_REGISTERED_RESEARCH_PACKAGE", + "independent_optimized": "Normal and -O independent receipts byte-identical", + "behavioral_tests": "Seven groups passed including real detector removal", + "source_binding_check": "make selected-record-check PASS; no complete cold replay", + "not_claimed": [ + "hosted CI success", + "selected supplier adoption", + "new kappa", + "formal-kernel or human review" + ] + } +} diff --git a/research/generic-output-mixing-erasure/VERIFY.json b/research/generic-output-mixing-erasure/VERIFY.json new file mode 100644 index 0000000000..2625928b0a --- /dev/null +++ b/research/generic-output-mixing-erasure/VERIFY.json @@ -0,0 +1,47 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/connector-frame-73-exclusion/README.md", + "research/connector-frame-rigidity/README.md", + "research/universal-connector-boundary/CERTIFICATE.json", + "research/universal-connector-boundary/NOTICE.md", + "research/universal-connector-boundary/README.md", + "research/weighted-connector-readouts-seed1275309492/README.md", + "research/common-a-broadcast-readout-seed4a52/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Fixed source-bound complete normalized coefficients, dirty restoration, both orientations, exact pairing/frame census and seven semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Independent noncommutative full-state replay, suffix erasure, matching census, all short words and dense 2x2 matrix scope controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Missing/corrupt source/certificate/receipt rejection, detector-removal sensitivity, normal/optimized unchanged relocation and no-overwrite generation." + } + ] +} diff --git a/research/generic-output-mixing-erasure/independent.py b/research/generic-output-mixing-erasure/independent.py new file mode 100644 index 0000000000..d66ab9413c --- /dev/null +++ b/research/generic-output-mixing-erasure/independent.py @@ -0,0 +1,310 @@ +#!/usr/bin/env python3 +"""Independent exact oracle: free GF(2) words, suffix routing, endpoint matchings. + +No package verifier or predecessor code is imported. Every initial register has +its own formal vector; a row is a set of (input, noncommutative operator word) +terms. Symmetric difference performs addition over GF(2). +""" +from __future__ import annotations + +import argparse +from collections import Counter +from itertools import product +import json +from pathlib import Path + + +class Rejected(ValueError): + pass + + +def require(ok, message): + if not ok: + raise Rejected(message) + + +def require_rejection(fixture, message): + try: + check_fixture(fixture) + except Rejected as error: + require(str(error) == message, "wrong rejecting check") + return + raise Rejected("invalid fixture accepted") + + +def dimensions(fixture): + s, n, r = (fixture[k] for k in + ("source_count", "logical_outputs", "bank_size")) + require(all(type(x) is int and x > 0 for x in (s, n, r)), "dimensions") + require(n <= r and len(fixture["masks"]) == n, "output dimensions") + require(all(type(m) is int and 0 <= m < 1 << s + for m in fixture["masks"]), "masks") + for op in fixture["word"]: + require(isinstance(op, list) and op, "operation") + tag, *args = op + require(all(type(x) is int for x in args), "operation indices") + legal = ((tag == "B" and len(args) == 1 and 0 <= args[0] < s) + or (tag == "A" and len(args) == 2 + and 0 <= args[0] < n and 0 <= args[1] < r) + or (tag == "X" and len(args) == 2 + and 0 <= args[0] < r and 0 <= args[1] < r + and args[0] != args[1])) + require(legal, "operation domain") + return s, n, r + + +def initial_rows(s, r): + return [{(column, ())} for column in range(s + 1 + r)] + + +def apply_symbol(symbol, row): + return {(column, (symbol,) + word) for column, word in row} + + +def execute(fixture): + s, _, r = dimensions(fixture) + rows = initial_rows(s, r) + for op in fixture["word"]: + if op[0] == "B": + rows[s] ^= apply_symbol(("B", op[1]), rows[op[1]]) + elif op[0] == "A": + rows[s + 1 + op[2]] ^= apply_symbol(("A", op[1]), rows[s]) + else: + rows[s + 1 + op[2]] ^= rows[s + 1 + op[1]] + return rows + + +def desired(fixture): + s, _, r = dimensions(fixture) + rows = initial_rows(s, r) + for i, mask in enumerate(fixture["masks"]): + rows[s + 1 + i] ^= { + (j, (("A", i), ("B", j))) + for j in range(s) if mask >> j & 1} + return rows + + +def erase(fixture): + """Trace final influences backward; no forward frame inverse is used.""" + _, _, r = dimensions(fixture) + image = [1 << p for p in range(r)] + kept = [] + for op in reversed(fixture["word"]): + if op[0] == "X": + image[op[1]] ^= image[op[2]] + elif op[0] == "B": + kept.append(op[:]) + elif image[op[2]] >> op[1] & 1: + kept.append(["A", op[1], op[1]]) + return list(reversed(kept)) + + +def query_counts(word): + return Counter((op[0], op[1]) for op in word if op[0] != "X") + + +def check_fixture(fixture): + s, _, r = dimensions(fixture) + target = desired(fixture) + require(execute(fixture) == target, "complete generic operator") + projected = erase(fixture) + require(execute(dict(fixture, word=projected)) == target, + "projected complete generic operator") + if "expected_erased" in fixture: + require(projected == fixture["expected_erased"], "fixed erased word") + before, after = query_counts(fixture["word"]), query_counts(projected) + require(all(after[k] <= before[k] for k in after), "per-query domination") + inverse = dict(fixture, word=list(reversed(fixture["word"]))) + require(execute(inverse) == target, "inverse complete generic operator") + require(execute(dict(inverse, word=erase(inverse))) == target, + "inverse projected operator") + return {"name": fixture["name"], "input_vector_columns": s + 1 + r, + "dirty_vector_columns": r + 1, "orientations": 2, + "queries_before": sum(before.values()), + "queries_after": sum(after.values()), + "mixes": len(fixture["word"]) - sum(before.values())} + + +def pairings(points): + """Pair the least unused endpoint, then recurse on the remaining endpoints.""" + if not points: + yield () + return + first, rest = points[0], points[1:] + for offset, partner in enumerate(rest): + for tail in pairings(rest[:offset] + rest[offset + 1:]): + yield ((first, partner),) + tail + + +def census(): + histogram = Counter() + for matching in pairings(tuple(range(10))): + labels = [None] * 10 + for label, (a, b) in enumerate(sorted(matching)): + labels[a] = labels[b] = label + prefixes = [0] + for label in labels: + prefixes.append(prefixes[-1] ^ (1 << label)) + differences = {a ^ b for a in prefixes for b in prefixes} + histogram[len(differences)] += 1 + require(histogram == {16: 42, 19: 120, 21: 180, 22: 56, 23: 45, + 24: 220, 26: 110, 28: 150, 31: 22}, + "complete five-source matching histogram") + return {"pairings": sum(histogram.values()), "maximum_coverage": max(histogram), + "histogram": dict(sorted(histogram.items()))} + + +def short_word_census(): + """All <=6-gate words on one source, one reader and two dirty bank rows.""" + alphabet = (["B", 0], ["A", 0, 0], ["A", 0, 1], ["X", 0, 1], ["X", 1, 0]) + fixture = {"source_count": 1, "logical_outputs": 1, "bank_size": 2, + "masks": [1], "word": []} + target = desired(fixture) + total = valid = valid_mixed = 0 + for length in range(7): + for word in product(alphabet, repeat=length): + total += 1 + trial = dict(fixture, word=list(word)) + if execute(trial) != target: + continue + valid += 1 + valid_mixed += any(op[0] == "X" for op in word) + projected = erase(trial) + require(execute(dict(trial, word=projected)) == target, + "short-word projection") + before, after = query_counts(word), query_counts(projected) + require(all(after[k] <= before[k] for k in after), "short-word price") + require(total == 19531 and valid_mixed > 0, "short-word census coverage") + return {"words": total, "maximum_length": 6, + "valid": valid, "valid_with_mixing": valid_mixed} + + +def matrix_apply(matrix, vector): + return tuple((vector[0] if row & 1 else 0) + ^ (vector[1] if row & 2 else 0) for row in matrix) + + +def numerical_rows(fixture, a_maps, b_maps, expected=False, reverse_products=False): + """Independent 2x2 block-matrix simulation on every scalar input basis.""" + s, _, r = dimensions(fixture) + rows = [(1 << (2*k), 1 << (2*k + 1)) for k in range(s + 1 + r)] + + def add(target, contribution): + rows[target] = tuple(a ^ b for a, b in zip(rows[target], contribution)) + + if expected: + for i, mask in enumerate(fixture["masks"]): + for j in range(s): + if mask >> j & 1: + outer, inner = ((b_maps[j], a_maps[i]) if reverse_products + else (a_maps[i], b_maps[j])) + add(s + 1 + i, matrix_apply(outer, matrix_apply(inner, rows[j]))) + return rows + for op in fixture["word"]: + if op[0] == "B": + add(s, matrix_apply(b_maps[op[1]], rows[op[1]])) + elif op[0] == "A": + add(s + 1 + op[2], matrix_apply(a_maps[op[1]], rows[s])) + else: + add(s + 1 + op[2], rows[s + 1 + op[1]]) + return rows + + +def matrix_controls(common): + matrices = list(product(range(4), repeat=2)) + mixed = {"source_count": 1, "logical_outputs": 1, "bank_size": 2, + "masks": [1], "word": [ + ["B", 0], ["X", 1, 0], ["A", 0, 1], ["X", 1, 0], ["A", 0, 1], + ["B", 0], ["X", 1, 0], ["A", 0, 1], ["X", 1, 0], ["A", 0, 1]]} + for a, b in product(matrices, repeat=2): + require(numerical_rows(mixed, [a], [b]) == + numerical_rows(mixed, [a], [b], expected=True), "2x2 mixed operator") + common_passes = equal_cases = 0 + for a0, a1, b in product(matrices, repeat=3): + actual = numerical_rows(common, [a0, a1], [b]) + wanted = numerical_rows(common, [a0, a1], [b], expected=True) + passes = actual == wanted + relation = matrix_apply((a0[0] ^ a1[0], a0[1] ^ a1[1]), b) == (0, 0) + require(passes == relation, "common-reader exact specialization condition") + common_passes += passes + if a0 == a1: + require(passes, "identical-reader positive control") + equal_cases += 1 + # A=E12, B=E21: AB=diag(1,0), BA=diag(0,1). + a, b = (2, 0), (0, 1) + require(numerical_rows(mixed, [a], [b]) != numerical_rows( + mixed, [a], [b], expected=True, reverse_products=True), "noncommuting control") + require(numerical_rows(common, [a, b], [b]) != numerical_rows( + common, [a, b], [b], expected=True), "independent-reader counterexample") + return {"all_2x2_single_reader_pairs": 256, "common_reader_triples": 4096, + "common_reader_triples_correct": common_passes, + "identical_reader_cases": equal_cases, + "reversed_product_rejected": True} + + +def fault_controls(fixtures, common): + require(execute(common) != desired(common), "common-reader generic rejection") + require_rejection(common, "complete generic operator") + projected = dict(common, word=erase(common)) + require(execute(projected) != desired(common), "common-reader projection scope") + mixed = next(f for f in fixtures if any(op[0] == "X" for op in f["word"])) + cut = next(i for i, op in enumerate(mixed["word"]) if op[0] == "X") + bad = dict(mixed, word=mixed["word"][:cut] + mixed["word"][cut + 1:]) + actual, target = execute(bad), desired(bad) + s = mixed["source_count"] + dirty_columns = lambda rows: [{term for term in row if term[0] >= s} + for row in rows] + require(dirty_columns(actual) != dirty_columns(target), "missing mix dirty fault") + require_rejection(bad, "complete generic operator") + fixture = fixtures[0] + cut = next(i for i, op in enumerate(fixture["word"]) if op[0] == "A") + bad = dict(fixture, word=fixture["word"][:cut] + fixture["word"][cut + 1:]) + require(any(column == fixture["source_count"] and word + for row in execute(bad) for column, word in row), + "missing read connector-dirt fault") + require(execute(bad) != desired(bad), "missing read complete rejection") + require_rejection(bad, "complete generic operator") + return ["missing_mix_dirty_columns", "missing_read_connector_dirt", + "common_reader_generic_scope", "noncommuting_product_order"] + + +def run(certificate): + require(type(certificate["schema_version"]) is int + and certificate["schema_version"] == 1, "schema") + fixtures = certificate["fixtures"] + names = [f["name"] for f in fixtures] + require(len(names) == len(set(names)), "unique fixture names") + require({"five_source_baseline", "five_source_dirty_output_helpers", + "odd_reader_identity"} == set(names), "fixed certificate fixtures") + common = certificate["common_reader_control"] + reports = [check_fixture(f) for f in fixtures] + baseline = next(f for f in fixtures if f["name"] == "five_source_baseline") + require((baseline["source_count"], baseline["logical_outputs"], + baseline["masks"]) == (5, 31, list(range(1, 32))), "all-mask instance") + counts = query_counts(baseline["word"]) + prices = [1, 4, 10, 16, 28] + bill = sum(count * (prices[index] if tag == "B" else 1) + for (tag, index), count in counts.items()) + require(sum(counts.values()) == 74 and bill == 182, "attained pinned bills") + # The written parity/path argument gives the two exhaustive source-count cases. + lower_bills = [2 * sum(prices) + 64, 2 * sum(prices) + 2 * min(prices) + 62] + require(lower_bills == [182, 182], "weighted lower-bound cases") + return {"pass": "GENERIC_OUTPUT_MIXING_INDEPENDENT", "fixtures": reports, + "matching_census": census(), "short_word_census": short_word_census(), + "matrix_controls": matrix_controls(common), + "pinned_bills": {"attained_queries": 74, "attained_weighted": bill, + "weighted_lower_cases": lower_bills}, + "rejecting_controls": fault_controls(fixtures, common)} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--certificate", type=Path, + default=Path(__file__).with_name("CERTIFICATE.json")) + args = parser.parse_args() + # Missing evidence is an error; this oracle never generates a certificate. + print(json.dumps(run(json.loads(args.certificate.read_text())), sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/generic-output-mixing-erasure/test_verify.py b/research/generic-output-mixing-erasure/test_verify.py new file mode 100644 index 0000000000..0d932190af --- /dev/null +++ b/research/generic-output-mixing-erasure/test_verify.py @@ -0,0 +1,132 @@ +#!/usr/bin/env python3 +"""Behavioral controls for complete dirt coverage and immutable evidence.""" +import copy +import hashlib +import importlib.util +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +spec = importlib.util.spec_from_file_location("mix_verify", HERE / "verify.py") +v = importlib.util.module_from_spec(spec) +spec.loader.exec_module(v) + + +class ErasureTests(unittest.TestCase): + def setUp(self): + self.temp = tempfile.TemporaryDirectory(prefix="output-mixing-") + self.addCleanup(self.temp.cleanup) + self.root = Path(self.temp.name) + self.pkg = self.root / "research/generic-output-mixing-erasure" + shutil.copytree(HERE, self.pkg, ignore=shutil.ignore_patterns("__pycache__")) + for pin in json.loads((HERE / "SOURCES.json").read_text())["files"]: + if pin["usage"] == "input": + target = self.root / pin["path"] + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / pin["path"], target) + + def command(self, *args, optimized=False): + return subprocess.run([sys.executable, "-I", "-B"] + (["-O"] if optimized else []) + + [str(self.pkg / "verify.py"), *map(str, args)], + cwd=self.root, capture_output=True, text=True) + + def expect_rejection(self, result, phrase): + self.assertNotEqual(result.returncode, 0, result.stdout) + self.assertIn(phrase, result.stderr) + + def hashes(self): + return {str(p.relative_to(self.root)): hashlib.sha256(p.read_bytes()).hexdigest() + for p in self.root.rglob("*") if p.is_file()} + + def test_relocated_read_only_normal_and_optimized(self): + before = self.hashes() + for optimized in (False, True): + result = self.command(optimized=optimized) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertIn("PASS_GENERIC_OUTPUT_MIXING_ERASURE", result.stdout) + self.assertEqual(before, self.hashes()) + + def test_missing_evidence_and_explicit_no_overwrite_generation(self): + expected = self.pkg / "EXPECTED.json" + original = expected.read_bytes() + expected.unlink() + self.expect_rejection(self.command(), "FileNotFoundError") + self.assertFalse(expected.exists()) + result = self.command("--write-expected", expected) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertEqual(expected.read_bytes(), original) + self.expect_rejection(self.command("--write-expected", expected), "FileExistsError") + self.assertEqual(expected.read_bytes(), original) + (self.pkg / "CERTIFICATE.json").unlink() + self.expect_rejection(self.command(), "FileNotFoundError") + + def test_typed_and_balanced_receipt_corruption(self): + path = self.pkg / "EXPECTED.json" + original = json.loads(path.read_text()) + mutants = [] + x = copy.deepcopy(original) + x["schema_version"] = True # Python equality would confuse this with 1. + mutants.append(x) + x = copy.deepcopy(original) + x["fixtures"][0]["map_calls"] += 1 + x["fixtures"][1]["map_calls"] -= 1 + mutants.append(x) + x = copy.deepcopy(original) + x["coverage_histogram"]["31"] -= 1 + x["coverage_histogram"]["28"] += 1 + mutants.append(x) + for x in mutants: + path.write_text(json.dumps(x)) + self.expect_rejection(self.command(), "expected receipt mismatch") + + def test_fixture_coverage_and_declared_erasure(self): + path = self.pkg / "CERTIFICATE.json" + original = json.loads(path.read_text()) + x = copy.deepcopy(original) + x["fixtures"].pop() + path.write_text(json.dumps(x)) + self.expect_rejection(self.command(), "fixture coverage") + x = copy.deepcopy(original) + x["fixtures"][1] = x["fixtures"][0] + path.write_text(json.dumps(x)) + self.expect_rejection(self.command(), "fixture identities") + x = copy.deepcopy(original) + x["fixtures"][1]["expected_erased"].pop() + path.write_text(json.dumps(x)) + self.expect_rejection(self.command(), "erasure receipt") + + def test_source_drift(self): + path = self.root / "research/universal-connector-boundary/CERTIFICATE.json" + path.write_bytes(path.read_bytes() + b"\n") + self.expect_rejection(self.command(), "source drift") + + def test_real_detector_removal_is_detected(self): + path = self.pkg / "verify.py" + source = path.read_text() + mutations = [ + ("require(coefficients[row][reader] == expected,", "require(True,", + "control unexpectedly accepted: reader coefficient"), + ('require(inv == [1 << i for i in range(r)], "output dirt frame")', + 'require(True, "output dirt frame")', "control unexpectedly accepted: output dirt frame"), + ] + for before, after, message in mutations: + self.assertEqual(source.count(before), 1) + path.write_text(source.replace(before, after)) + self.expect_rejection(self.command(), message) + + def test_empty_and_inactive_domains(self): + for f in [dict(source_count=0, logical_outputs=0, bank_size=0, masks=[], word=[]), + dict(source_count=0, logical_outputs=1, bank_size=2, masks=[0], + word=[["A", 0, 1], ["A", 0, 1]])]: + erased = v.check(f) + v.check(dict(f, word=erased)) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/generic-output-mixing-erasure/verify.py b/research/generic-output-mixing-erasure/verify.py new file mode 100644 index 0000000000..1d0af15c83 --- /dev/null +++ b/research/generic-output-mixing-erasure/verify.py @@ -0,0 +1,282 @@ +#!/usr/bin/env python3 +"""Exact normalized coefficient checker; verification never generates evidence. + +An A_i event contributes v tensor A_i (z0 + sum_j q_j B_j x_j), +where v=P^-1 e_port. All dirty columns and labelled coefficients are checked. +The all-parameter proof is in README.md. No predecessor code is imported. +""" +from __future__ import annotations + +import argparse +from collections import Counter, deque +import copy +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +class Invalid(ValueError): + pass + + +def require(ok, reason): + if not ok: + raise Invalid(reason) + + +def integer(value, lower, upper, label): + require(type(value) is int and lower <= value < upper, label) + return value + + +def validate(f): + require(isinstance(f, dict), "fixture object") + s = integer(f.get("source_count"), 0, 65, "source count") + n = integer(f.get("logical_outputs"), 0, 257, "output count") + r = integer(f.get("bank_size"), n, 513, "bank size") + masks = f.get("masks") + require(isinstance(masks, list) and len(masks) == n, "mask count") + for m in masks: + integer(m, 0, 1 << s, "mask domain") + require(isinstance(f.get("word"), list), "word array") + for e in f["word"]: + require(isinstance(e, list) and bool(e), "event array") + if e[0] == "B": + require(len(e) == 2, "B arity") + integer(e[1], 0, s, "B source") + elif e[0] == "A": + require(len(e) == 3, "A arity") + integer(e[1], 0, n, "A reader") + integer(e[2], 0, r, "A port") + elif e[0] == "X": + require(len(e) == 3, "X arity") + integer(e[1], 0, r, "X source") + integer(e[2], 0, r, "X target") + require(e[1] != e[2], "noninvertible aliased X") + else: + raise Invalid("unknown operation") + return s, n, r + + +def analyze(f): + _, n, r = validate(f) + inv = [1 << i for i in range(r)] + # Bit 0 is A_i z0; bit j+1 is A_i B_j x_j. + coefficients = [[0] * n for _ in range(r)] + q = 0 + erased = [] + for e in f["word"]: + if e[0] == "B": + q ^= 1 << e[1] + erased.append(e.copy()) + elif e[0] == "X": + _, source, target = e + # P_new=E P; inverse right multiplication adds column target to source. + inv = [row ^ (((row >> target) & 1) << source) for row in inv] + else: + _, reader, port = e + signal = 1 | (q << 1) + for row in range(r): + if (inv[row] >> port) & 1: + coefficients[row][reader] ^= signal + if (inv[reader] >> port) & 1: + erased.append(["A", reader, reader]) + return inv, q, coefficients, erased + + +def check(f): + inv, q, coefficients, erased = analyze(f) + n, r = f["logical_outputs"], f["bank_size"] + require(inv == [1 << i for i in range(r)], "output dirt frame") + require(q == 0, "connector restoration") + for row in range(r): + for reader in range(n): + expected = f["masks"][reader] << 1 if row == reader else 0 + require(coefficients[row][reader] == expected, + f"reader coefficient row={row} reader={reader}") + return erased + + +def counts(word): + return Counter((e[0], e[1]) for e in word if e[0] != "X") + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")) + + +def census(): + """Restricted-growth words, independent of the oracle's endpoint pairings.""" + hist = Counter() + + def visit(word, seen): + if len(word) == 10: + prefix, q = [0], 0 + for j in word: + q ^= 1 << j + prefix.append(q) + hist[len({a ^ b for a in prefix for b in prefix})] += 1 + return + for j, count in enumerate(seen): + if count == 1: + nxt = seen.copy() + nxt[j] = 2 + visit(word + [j], nxt) + if len(seen) < 5: + visit(word + [len(seen)], seen + [1]) + + visit([], []) + require(sum(hist.values()) == 945 and max(hist) == 31, "pairing boundary") + return {str(k): v for k, v in sorted(hist.items())} + + +def frame_census(): + """Every GL(3,2) output frame, around a generic two-source/three-row batch.""" + ident = (1, 2, 4) + paths = {ident: []} + queue = deque([ident]) + while queue: + frame = queue.popleft() + for a in range(3): + for b in range(3): + if a == b: + continue + nxt = list(frame) + nxt[b] ^= nxt[a] + nxt = tuple(nxt) + if nxt not in paths: + paths[nxt] = paths[frame] + [["X", a, b]] + queue.append(nxt) + require(len(paths) == 168, "GL3 coverage") + baseline = [["A", 0, 0], ["B", 0], ["A", 0, 0], ["B", 0], + ["A", 1, 1], ["B", 1], ["A", 1, 1], ["B", 1], + ["A", 2, 2], ["B", 0], ["B", 1], ["A", 2, 2], + ["B", 1], ["B", 0]] + total_reads = 0 + for frame, path in paths.items(): + word = copy.deepcopy(path) + for e in baseline: + if e[0] == "B": + word.append(e.copy()) + else: + for p in range(3): + if (frame[p] >> e[1]) & 1: + word.append(["A", e[1], p]) + word += list(reversed(path)) + f = dict(source_count=2, logical_outputs=3, bank_size=3, + masks=[1, 2, 3], word=word) + erased = check(f) + check({**f, "word": erased}) + require(not (counts(erased) - counts(word)), "componentwise dominance") + total_reads += sum(e[0] == "A" for e in word) + return {"frames": len(paths), "input_readouts": total_reads} + + +def rejected(f, reason): + try: + check(f) + except Invalid as exc: + require(reason in str(exc), f"wrong rejection: {exc}") + return + raise Invalid(f"control unexpectedly accepted: {reason}") + + +def controls(fixtures, common): + baseline, decorated, odd = fixtures + f = copy.deepcopy(baseline) + f["word"].pop(next(i for i, e in enumerate(f["word"]) if e[0] == "B")) + rejected(f, "connector restoration") + f = copy.deepcopy(baseline) + f["word"].pop(next(i for i, e in enumerate(f["word"]) if e[0] == "A")) + rejected(f, "reader coefficient") + f = copy.deepcopy(decorated) + f["word"].pop(3) # removes helper cancellation; all logical outputs stay right + inv, q, coeff, _ = analyze(f) + require(inv == [1 << i for i in range(33)] and q == 0, "helper control setup") + require(all(coeff[row][i] == (f['masks'][i] << 1 if row == i else 0) + for row in range(31) for i in range(31)), "helper control outputs") + rejected(f, "reader coefficient row=31") + f = copy.deepcopy(odd) + f["word"].pop() + rejected(f, "output dirt frame") + f = copy.deepcopy(odd) + f["word"][2] = ["X", 0, 0] + rejected(f, "noninvertible aliased X") + f = copy.deepcopy(baseline) + f["word"][0][2] = True + rejected(f, "A port") + rejected(common, "reader coefficient") + return 7 + + +def check_pins(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + for pin in manifest["files"]: + if pin["usage"] == "input": + data = (ROOT / pin["path"]).read_bytes() + require(hashlib.sha256(data).hexdigest() == pin["sha256"], + f"source drift: {pin['path']}") + + +def run(cert): + require(type(cert.get("schema_version")) is int and cert["schema_version"] == 1, + "certificate schema") + fixtures = cert.get("fixtures") + require(isinstance(fixtures, list) and len(fixtures) == 3, "fixture coverage") + require([f.get("name") for f in fixtures] == + ["five_source_baseline", "five_source_dirty_output_helpers", "odd_reader_identity"], + "fixture identities") + inherited = json.loads((ROOT / "research/universal-connector-boundary/CERTIFICATE.json").read_text()) + source = inherited["schedules"]["five_extra_output"] + source_word = [[op, i] if op == "B" else [op, i, i] for op, i in source["word"]] + require(fixtures[0]["word"] == source_word and fixtures[0]["masks"] == source["rows"], + "baseline source binding") + result = [] + for f in fixtures: + erased = check(f) + require(erased == f.get("expected_erased"), "erasure receipt") + check({**f, "word": erased}) + check({**f, "word": list(reversed(f["word"]))}) + require(not (counts(erased) - counts(f["word"])), "componentwise dominance") + result.append({"name": f["name"], "map_calls": sum(counts(f["word"]).values()), + "erased_map_calls": len(erased), + "mixing_xors": sum(e[0] == "X" for e in f["word"]), + "dirty_bank_rows": f["bank_size"]}) + h = census() + prices = [1, 4, 10, 16, 28] + bill = sum(prices[e[1]] if e[0] == "B" else 1 for e in source_word) + require(bill == 182, "weighted fixture bill") + return {"schema_version": 1, "fixtures": result, "pairings": 945, + "certificate_sha256": hashlib.sha256(canonical(cert).encode()).hexdigest(), + "coverage_histogram": h, "max_coverage": 31, + "five_source_map_optimum": 74, "weighted_fixture_optimum": bill, + "frame_census": frame_census(), + "negative_controls": controls(fixtures, cert["common_reader_control"]), + "no_new_kappa": True} + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--certificate", type=Path, default=HERE / "CERTIFICATE.json") + parser.add_argument("--expected", type=Path, default=HERE / "EXPECTED.json") + parser.add_argument("--write-expected", type=Path) + args = parser.parse_args() + check_pins() + receipt = run(json.loads(args.certificate.read_text())) + if args.write_expected: + with args.write_expected.open("x") as handle: + json.dump(receipt, handle, indent=2, sort_keys=True) + handle.write("\n") + print("WROTE_EXPECTED", args.write_expected) + else: + expected = json.loads(args.expected.read_text()) + require(canonical(receipt) == canonical(expected), "expected receipt mismatch") + print("PASS_GENERIC_OUTPUT_MIXING_ERASURE fixtures=3 pairings=945 frames=168 " + "map_optimum=74 weighted_optimum=182 controls=7 no_new_kappa") + + +if __name__ == "__main__": + main()