diff --git a/research/fstar-cert-census-seed298df375/CENSUS-RECORDS.json b/research/fstar-cert-census-seed298df375/CENSUS-RECORDS.json new file mode 100644 index 0000000000..49871f8d4a --- /dev/null +++ b/research/fstar-cert-census-seed298df375/CENSUS-RECORDS.json @@ -0,0 +1,2746 @@ +[ + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 7, + "resolved": true, + "seed": 20261083, + "threshold": 2, + "tied_lines": 2, + "v": 4, + "witness": 4, + "zero_pairs": 2 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 10, + "resolved": true, + "seed": 20261084, + "threshold": 2, + "tied_lines": 1, + "v": 4, + "witness": 4, + "zero_pairs": 0 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 8, + "resolved": true, + "seed": 20261085, + "threshold": 2, + "tied_lines": 1, + "v": 4, + "witness": 4, + "zero_pairs": 2 + }, + { + "evals": 42, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 5, + "resolved": true, + "seed": 20261086, + "threshold": 2, + "tied_lines": 0, + "v": 4, + "witness": 4, + "zero_pairs": 2 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 7, + "resolved": true, + "seed": 20261087, + "threshold": 2, + "tied_lines": 0, + "v": 4, + "witness": 4, + "zero_pairs": 2 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 7, + "resolved": true, + "seed": 20261088, + "threshold": 2, + "tied_lines": 1, + "v": 4, + "witness": 4, + "zero_pairs": 1 + }, + { + "evals": 49, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 6, + "resolved": true, + "seed": 20261089, + "threshold": 2, + "tied_lines": 0, + "v": 4, + "witness": 4, + "zero_pairs": 3 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 9, + "resolved": true, + "seed": 20261090, + "threshold": 2, + "tied_lines": 0, + "v": 4, + "witness": 4, + "zero_pairs": 2 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 9, + "resolved": true, + "seed": 20261091, + "threshold": 2, + "tied_lines": 1, + "v": 4, + "witness": 4, + "zero_pairs": 3 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 6, + "resolved": true, + "seed": 20261092, + "threshold": 2, + "tied_lines": 0, + "v": 4, + "witness": 4, + "zero_pairs": 0 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 12, + "resolved": true, + "seed": 20261100, + "threshold": 3, + "tied_lines": 2, + "v": 5, + "witness": 5, + "zero_pairs": 2 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 11, + "resolved": true, + "seed": 20261101, + "threshold": 3, + "tied_lines": 1, + "v": 5, + "witness": 5, + "zero_pairs": 1 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 10, + "resolved": true, + "seed": 20261102, + "threshold": 3, + "tied_lines": 0, + "v": 5, + "witness": 5, + "zero_pairs": 2 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 10, + "resolved": true, + "seed": 20261103, + "threshold": 3, + "tied_lines": 0, + "v": 5, + "witness": 5, + "zero_pairs": 3 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 12, + "resolved": true, + "seed": 20261104, + "threshold": 3, + "tied_lines": 0, + "v": 5, + "witness": 5, + "zero_pairs": 3 + }, + { + "evals": 19, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 9, + "resolved": true, + "seed": 20261105, + "threshold": 3, + "tied_lines": 0, + "v": 5, + "witness": 5, + "zero_pairs": 2 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 10, + "resolved": true, + "seed": 20261106, + "threshold": 3, + "tied_lines": 0, + "v": 5, + "witness": 5, + "zero_pairs": 3 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 9, + "resolved": true, + "seed": 20261107, + "threshold": 3, + "tied_lines": 1, + "v": 5, + "witness": 5, + "zero_pairs": 5 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 8, + "resolved": true, + "seed": 20261108, + "threshold": 3, + "tied_lines": 1, + "v": 5, + "witness": 5, + "zero_pairs": 4 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 13, + "resolved": true, + "seed": 20261109, + "threshold": 3, + "tied_lines": 2, + "v": 5, + "witness": 5, + "zero_pairs": 1 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 11, + "resolved": true, + "seed": 20261117, + "threshold": 4, + "tied_lines": 3, + "v": 6, + "witness": 6, + "zero_pairs": 5 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 14, + "resolved": true, + "seed": 20261118, + "threshold": 4, + "tied_lines": 1, + "v": 6, + "witness": 6, + "zero_pairs": 1 + }, + { + "evals": 84, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 10, + "resolved": true, + "seed": 20261119, + "threshold": 4, + "tied_lines": 3, + "v": 6, + "witness": 6, + "zero_pairs": 5 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 12, + "resolved": true, + "seed": 20261120, + "threshold": 4, + "tied_lines": 1, + "v": 6, + "witness": 6, + "zero_pairs": 3 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 13, + "resolved": true, + "seed": 20261121, + "threshold": 4, + "tied_lines": 1, + "v": 6, + "witness": 6, + "zero_pairs": 1 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 12, + "resolved": true, + "seed": 20261122, + "threshold": 4, + "tied_lines": 1, + "v": 6, + "witness": 6, + "zero_pairs": 5 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 12, + "resolved": true, + "seed": 20261123, + "threshold": 4, + "tied_lines": 2, + "v": 6, + "witness": 6, + "zero_pairs": 3 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 10, + "resolved": true, + "seed": 20261124, + "threshold": 4, + "tied_lines": 1, + "v": 6, + "witness": 6, + "zero_pairs": 3 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 11, + "resolved": true, + "seed": 20261125, + "threshold": 4, + "tied_lines": 2, + "v": 6, + "witness": 6, + "zero_pairs": 1 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 8, + "resolved": true, + "seed": 20261126, + "threshold": 4, + "tied_lines": 0, + "v": 6, + "witness": 6, + "zero_pairs": 2 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": false, + "min_cost_upper": 13, + "resolved": true, + "seed": 20261134, + "threshold": 4, + "tied_lines": 1, + "v": 7, + "witness": 7, + "zero_pairs": 12 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 11, + "resolved": true, + "seed": 20261135, + "threshold": 4, + "tied_lines": 0, + "v": 7, + "witness": 7, + "zero_pairs": 6 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 13, + "resolved": true, + "seed": 20261136, + "threshold": 4, + "tied_lines": 1, + "v": 7, + "witness": 7, + "zero_pairs": 4 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 12, + "resolved": true, + "seed": 20261137, + "threshold": 4, + "tied_lines": 0, + "v": 7, + "witness": 7, + "zero_pairs": 8 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 13, + "resolved": true, + "seed": 20261138, + "threshold": 4, + "tied_lines": 2, + "v": 7, + "witness": 7, + "zero_pairs": 3 + }, + { + "evals": 82, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 15, + "resolved": true, + "seed": 20261139, + "threshold": 4, + "tied_lines": 3, + "v": 7, + "witness": 7, + "zero_pairs": 6 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 13, + "resolved": true, + "seed": 20261140, + "threshold": 4, + "tied_lines": 1, + "v": 7, + "witness": 7, + "zero_pairs": 6 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 15, + "resolved": true, + "seed": 20261141, + "threshold": 4, + "tied_lines": 2, + "v": 7, + "witness": 7, + "zero_pairs": 7 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 14, + "resolved": true, + "seed": 20261142, + "threshold": 4, + "tied_lines": 1, + "v": 7, + "witness": 7, + "zero_pairs": 5 + }, + { + "evals": 19, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 12, + "resolved": true, + "seed": 20261143, + "threshold": 4, + "tied_lines": 1, + "v": 7, + "witness": 7, + "zero_pairs": 7 + }, + { + "evals": 105, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 17, + "resolved": true, + "seed": 20261151, + "threshold": 5, + "tied_lines": 1, + "v": 8, + "witness": 8, + "zero_pairs": 8 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 12, + "resolved": true, + "seed": 20261152, + "threshold": 5, + "tied_lines": 1, + "v": 8, + "witness": 8, + "zero_pairs": 5 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": false, + "min_cost_upper": 14, + "resolved": true, + "seed": 20261153, + "threshold": 5, + "tied_lines": 2, + "v": 8, + "witness": 8, + "zero_pairs": 12 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 11, + "resolved": true, + "seed": 20261154, + "threshold": 5, + "tied_lines": 0, + "v": 8, + "witness": 8, + "zero_pairs": 9 + }, + { + "evals": 84, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 15, + "resolved": true, + "seed": 20261155, + "threshold": 5, + "tied_lines": 4, + "v": 8, + "witness": 8, + "zero_pairs": 8 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 15, + "resolved": true, + "seed": 20261156, + "threshold": 5, + "tied_lines": 2, + "v": 8, + "witness": 8, + "zero_pairs": 7 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": false, + "min_cost_upper": 15, + "resolved": true, + "seed": 20261157, + "threshold": 5, + "tied_lines": 1, + "v": 8, + "witness": 8, + "zero_pairs": 11 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 13, + "resolved": true, + "seed": 20261158, + "threshold": 5, + "tied_lines": 1, + "v": 8, + "witness": 8, + "zero_pairs": 7 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 18, + "resolved": true, + "seed": 20261159, + "threshold": 5, + "tied_lines": 2, + "v": 8, + "witness": 8, + "zero_pairs": 7 + }, + { + "evals": 11, + "falsifier": false, + "family": "dense", + "min_cost_exact": false, + "min_cost_upper": 14, + "resolved": true, + "seed": 20261160, + "threshold": 5, + "tied_lines": 2, + "v": 8, + "witness": 8, + "zero_pairs": 11 + }, + { + "evals": 150, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 17, + "resolved": true, + "seed": 20261168, + "threshold": 6, + "tied_lines": 2, + "v": 9, + "witness": 8, + "zero_pairs": 10 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 21, + "resolved": true, + "seed": 20261169, + "threshold": 6, + "tied_lines": 3, + "v": 9, + "witness": 9, + "zero_pairs": 10 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 19, + "resolved": true, + "seed": 20261170, + "threshold": 6, + "tied_lines": 1, + "v": 9, + "witness": 9, + "zero_pairs": 4 + }, + { + "evals": 19, + "falsifier": false, + "family": "dense", + "min_cost_exact": false, + "min_cost_upper": 19, + "resolved": true, + "seed": 20261171, + "threshold": 6, + "tied_lines": 0, + "v": 9, + "witness": 9, + "zero_pairs": 13 + }, + { + "evals": 128, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 18, + "resolved": true, + "seed": 20261172, + "threshold": 6, + "tied_lines": 2, + "v": 9, + "witness": 9, + "zero_pairs": 9 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 22, + "resolved": true, + "seed": 20261185, + "threshold": 6, + "tied_lines": 2, + "v": 10, + "witness": 10, + "zero_pairs": 7 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": false, + "min_cost_upper": 18, + "resolved": true, + "seed": 20261186, + "threshold": 6, + "tied_lines": 2, + "v": 10, + "witness": 10, + "zero_pairs": 11 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": false, + "min_cost_upper": 17, + "resolved": true, + "seed": 20261187, + "threshold": 6, + "tied_lines": 0, + "v": 10, + "witness": 10, + "zero_pairs": 15 + }, + { + "evals": 34, + "falsifier": false, + "family": "dense", + "min_cost_exact": false, + "min_cost_upper": 21, + "resolved": true, + "seed": 20261188, + "threshold": 6, + "tied_lines": 1, + "v": 10, + "witness": 10, + "zero_pairs": 11 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 16, + "resolved": true, + "seed": 20261189, + "threshold": 6, + "tied_lines": 2, + "v": 10, + "witness": 10, + "zero_pairs": 10 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 22, + "resolved": true, + "seed": 20261202, + "threshold": 7, + "tied_lines": 2, + "v": 11, + "witness": 11, + "zero_pairs": 9 + }, + { + "evals": 19, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 21, + "resolved": true, + "seed": 20261203, + "threshold": 7, + "tied_lines": 4, + "v": 11, + "witness": 11, + "zero_pairs": 9 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": false, + "min_cost_upper": 23, + "resolved": true, + "seed": 20261204, + "threshold": 7, + "tied_lines": 4, + "v": 11, + "witness": 11, + "zero_pairs": 16 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": false, + "min_cost_upper": 28, + "resolved": true, + "seed": 20261205, + "threshold": 7, + "tied_lines": 5, + "v": 11, + "witness": 11, + "zero_pairs": 12 + }, + { + "evals": 150, + "falsifier": false, + "family": "dense", + "min_cost_exact": false, + "min_cost_upper": 24, + "resolved": true, + "seed": 20261206, + "threshold": 7, + "tied_lines": 4, + "v": 11, + "witness": 10, + "zero_pairs": 19 + }, + { + "evals": 150, + "falsifier": false, + "family": "dense", + "min_cost_exact": false, + "min_cost_upper": 23, + "resolved": true, + "seed": 20261219, + "threshold": 8, + "tied_lines": 3, + "v": 12, + "witness": 11, + "zero_pairs": 19 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 29, + "resolved": true, + "seed": 20261220, + "threshold": 8, + "tied_lines": 4, + "v": 12, + "witness": 12, + "zero_pairs": 8 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": true, + "min_cost_upper": 28, + "resolved": true, + "seed": 20261221, + "threshold": 8, + "tied_lines": 4, + "v": 12, + "witness": 12, + "zero_pairs": 10 + }, + { + "evals": 150, + "falsifier": false, + "family": "dense", + "min_cost_exact": false, + "min_cost_upper": 26, + "resolved": true, + "seed": 20261222, + "threshold": 8, + "tied_lines": 2, + "v": 12, + "witness": 11, + "zero_pairs": 11 + }, + { + "evals": 1, + "falsifier": false, + "family": "dense", + "min_cost_exact": false, + "min_cost_upper": 27, + "resolved": true, + "seed": 20261223, + "threshold": 8, + "tied_lines": 5, + "v": 12, + "witness": 12, + "zero_pairs": 12 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 8, + "resolved": true, + "seed": 20262083, + "threshold": 2, + "tied_lines": 2, + "v": 4, + "witness": 4, + "zero_pairs": 3 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 5, + "resolved": true, + "seed": 20262084, + "threshold": 2, + "tied_lines": 1, + "v": 4, + "witness": 4, + "zero_pairs": 5 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 4, + "resolved": true, + "seed": 20262085, + "threshold": 2, + "tied_lines": 0, + "v": 4, + "witness": 4, + "zero_pairs": 4 + }, + { + "evals": 50, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 7, + "resolved": true, + "seed": 20262086, + "threshold": 2, + "tied_lines": 3, + "v": 4, + "witness": 4, + "zero_pairs": 4 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 4, + "resolved": true, + "seed": 20262087, + "threshold": 2, + "tied_lines": 0, + "v": 4, + "witness": 4, + "zero_pairs": 3 + }, + { + "evals": 11, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 5, + "resolved": true, + "seed": 20262088, + "threshold": 2, + "tied_lines": 3, + "v": 4, + "witness": 4, + "zero_pairs": 6 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 7, + "resolved": true, + "seed": 20262089, + "threshold": 2, + "tied_lines": 2, + "v": 4, + "witness": 4, + "zero_pairs": 1 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 7, + "resolved": true, + "seed": 20262090, + "threshold": 2, + "tied_lines": 3, + "v": 4, + "witness": 4, + "zero_pairs": 1 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 6, + "resolved": true, + "seed": 20262091, + "threshold": 2, + "tied_lines": 2, + "v": 4, + "witness": 4, + "zero_pairs": 2 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 5, + "resolved": true, + "seed": 20262092, + "threshold": 2, + "tied_lines": 1, + "v": 4, + "witness": 4, + "zero_pairs": 2 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 7, + "resolved": true, + "seed": 20262100, + "threshold": 3, + "tied_lines": 1, + "v": 5, + "witness": 5, + "zero_pairs": 4 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 7, + "resolved": true, + "seed": 20262101, + "threshold": 3, + "tied_lines": 2, + "v": 5, + "witness": 5, + "zero_pairs": 8 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 6, + "resolved": true, + "seed": 20262102, + "threshold": 3, + "tied_lines": 1, + "v": 5, + "witness": 5, + "zero_pairs": 4 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 8, + "resolved": true, + "seed": 20262103, + "threshold": 3, + "tied_lines": 3, + "v": 5, + "witness": 5, + "zero_pairs": 7 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 10, + "resolved": true, + "seed": 20262104, + "threshold": 3, + "tied_lines": 3, + "v": 5, + "witness": 5, + "zero_pairs": 2 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 6, + "resolved": true, + "seed": 20262105, + "threshold": 3, + "tied_lines": 1, + "v": 5, + "witness": 5, + "zero_pairs": 7 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 9, + "resolved": true, + "seed": 20262106, + "threshold": 3, + "tied_lines": 3, + "v": 5, + "witness": 5, + "zero_pairs": 1 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 9, + "resolved": true, + "seed": 20262107, + "threshold": 3, + "tied_lines": 3, + "v": 5, + "witness": 5, + "zero_pairs": 3 + }, + { + "evals": 34, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 7, + "resolved": true, + "seed": 20262108, + "threshold": 3, + "tied_lines": 3, + "v": 5, + "witness": 5, + "zero_pairs": 5 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 9, + "resolved": true, + "seed": 20262109, + "threshold": 3, + "tied_lines": 3, + "v": 5, + "witness": 5, + "zero_pairs": 3 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 11, + "resolved": true, + "seed": 20262117, + "threshold": 4, + "tied_lines": 3, + "v": 6, + "witness": 6, + "zero_pairs": 2 + }, + { + "evals": 26, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 9, + "resolved": true, + "seed": 20262118, + "threshold": 4, + "tied_lines": 3, + "v": 6, + "witness": 6, + "zero_pairs": 7 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 8, + "resolved": true, + "seed": 20262119, + "threshold": 4, + "tied_lines": 2, + "v": 6, + "witness": 6, + "zero_pairs": 8 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 10, + "resolved": true, + "seed": 20262120, + "threshold": 4, + "tied_lines": 2, + "v": 6, + "witness": 6, + "zero_pairs": 7 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 9, + "resolved": true, + "seed": 20262121, + "threshold": 4, + "tied_lines": 2, + "v": 6, + "witness": 6, + "zero_pairs": 4 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 10, + "resolved": true, + "seed": 20262122, + "threshold": 4, + "tied_lines": 2, + "v": 6, + "witness": 6, + "zero_pairs": 7 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 8, + "resolved": true, + "seed": 20262123, + "threshold": 4, + "tied_lines": 1, + "v": 6, + "witness": 6, + "zero_pairs": 6 + }, + { + "evals": 26, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 9, + "resolved": true, + "seed": 20262124, + "threshold": 4, + "tied_lines": 2, + "v": 6, + "witness": 6, + "zero_pairs": 9 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 7, + "resolved": true, + "seed": 20262125, + "threshold": 4, + "tied_lines": 1, + "v": 6, + "witness": 6, + "zero_pairs": 7 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 10, + "resolved": true, + "seed": 20262126, + "threshold": 4, + "tied_lines": 2, + "v": 6, + "witness": 6, + "zero_pairs": 6 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 8, + "resolved": true, + "seed": 20262134, + "threshold": 4, + "tied_lines": 1, + "v": 7, + "witness": 7, + "zero_pairs": 9 + }, + { + "evals": 34, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 9, + "resolved": true, + "seed": 20262135, + "threshold": 4, + "tied_lines": 2, + "v": 7, + "witness": 7, + "zero_pairs": 10 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 8, + "resolved": true, + "seed": 20262136, + "threshold": 4, + "tied_lines": 1, + "v": 7, + "witness": 7, + "zero_pairs": 13 + }, + { + "evals": 19, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 12, + "resolved": true, + "seed": 20262137, + "threshold": 4, + "tied_lines": 3, + "v": 7, + "witness": 7, + "zero_pairs": 12 + }, + { + "evals": 150, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 12, + "resolved": true, + "seed": 20262138, + "threshold": 4, + "tied_lines": 4, + "v": 7, + "witness": 6, + "zero_pairs": 10 + }, + { + "evals": 64, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 10, + "resolved": true, + "seed": 20262139, + "threshold": 4, + "tied_lines": 2, + "v": 7, + "witness": 7, + "zero_pairs": 13 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 8, + "resolved": true, + "seed": 20262140, + "threshold": 4, + "tied_lines": 1, + "v": 7, + "witness": 7, + "zero_pairs": 12 + }, + { + "evals": 11, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 13, + "resolved": true, + "seed": 20262141, + "threshold": 4, + "tied_lines": 5, + "v": 7, + "witness": 7, + "zero_pairs": 9 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 11, + "resolved": true, + "seed": 20262142, + "threshold": 4, + "tied_lines": 3, + "v": 7, + "witness": 7, + "zero_pairs": 8 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 11, + "resolved": true, + "seed": 20262143, + "threshold": 4, + "tied_lines": 4, + "v": 7, + "witness": 7, + "zero_pairs": 9 + }, + { + "evals": 150, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 13, + "resolved": true, + "seed": 20262151, + "threshold": 5, + "tied_lines": 4, + "v": 8, + "witness": 7, + "zero_pairs": 17 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 8, + "resolved": true, + "seed": 20262152, + "threshold": 5, + "tied_lines": 0, + "v": 8, + "witness": 8, + "zero_pairs": 22 + }, + { + "evals": 36, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 14, + "resolved": true, + "seed": 20262153, + "threshold": 5, + "tied_lines": 4, + "v": 8, + "witness": 8, + "zero_pairs": 15 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 10, + "resolved": true, + "seed": 20262154, + "threshold": 5, + "tied_lines": 1, + "v": 8, + "witness": 8, + "zero_pairs": 12 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 17, + "resolved": true, + "seed": 20262155, + "threshold": 5, + "tied_lines": 5, + "v": 8, + "witness": 8, + "zero_pairs": 10 + }, + { + "evals": 37, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 13, + "resolved": true, + "seed": 20262156, + "threshold": 5, + "tied_lines": 4, + "v": 8, + "witness": 8, + "zero_pairs": 17 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 13, + "resolved": true, + "seed": 20262157, + "threshold": 5, + "tied_lines": 4, + "v": 8, + "witness": 8, + "zero_pairs": 8 + }, + { + "evals": 42, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 13, + "resolved": true, + "seed": 20262158, + "threshold": 5, + "tied_lines": 4, + "v": 8, + "witness": 8, + "zero_pairs": 17 + }, + { + "evals": 88, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 12, + "resolved": true, + "seed": 20262159, + "threshold": 5, + "tied_lines": 3, + "v": 8, + "witness": 8, + "zero_pairs": 25 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 17, + "resolved": true, + "seed": 20262160, + "threshold": 5, + "tied_lines": 6, + "v": 8, + "witness": 8, + "zero_pairs": 11 + }, + { + "evals": 150, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 9, + "resolved": true, + "seed": 20262168, + "threshold": 6, + "tied_lines": 0, + "v": 9, + "witness": 8, + "zero_pairs": 18 + }, + { + "evals": 11, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 16, + "resolved": true, + "seed": 20262169, + "threshold": 6, + "tied_lines": 5, + "v": 9, + "witness": 9, + "zero_pairs": 16 + }, + { + "evals": 11, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 14, + "resolved": true, + "seed": 20262170, + "threshold": 6, + "tied_lines": 4, + "v": 9, + "witness": 9, + "zero_pairs": 22 + }, + { + "evals": 19, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 12, + "resolved": true, + "seed": 20262171, + "threshold": 6, + "tied_lines": 3, + "v": 9, + "witness": 9, + "zero_pairs": 20 + }, + { + "evals": 150, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 15, + "resolved": true, + "seed": 20262172, + "threshold": 6, + "tied_lines": 5, + "v": 9, + "witness": 8, + "zero_pairs": 20 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 17, + "resolved": true, + "seed": 20262185, + "threshold": 6, + "tied_lines": 5, + "v": 10, + "witness": 10, + "zero_pairs": 22 + }, + { + "evals": 150, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 12, + "resolved": true, + "seed": 20262186, + "threshold": 6, + "tied_lines": 2, + "v": 10, + "witness": 9, + "zero_pairs": 19 + }, + { + "evals": 26, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 17, + "resolved": true, + "seed": 20262187, + "threshold": 6, + "tied_lines": 5, + "v": 10, + "witness": 10, + "zero_pairs": 32 + }, + { + "evals": 29, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 18, + "resolved": true, + "seed": 20262188, + "threshold": 6, + "tied_lines": 4, + "v": 10, + "witness": 10, + "zero_pairs": 24 + }, + { + "evals": 104, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 18, + "resolved": true, + "seed": 20262189, + "threshold": 6, + "tied_lines": 6, + "v": 10, + "witness": 10, + "zero_pairs": 26 + }, + { + "evals": 150, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 18, + "resolved": true, + "seed": 20262202, + "threshold": 7, + "tied_lines": 5, + "v": 11, + "witness": 10, + "zero_pairs": 27 + }, + { + "evals": 150, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 14, + "resolved": true, + "seed": 20262203, + "threshold": 7, + "tied_lines": 2, + "v": 11, + "witness": 10, + "zero_pairs": 31 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 12, + "resolved": true, + "seed": 20262204, + "threshold": 7, + "tied_lines": 1, + "v": 11, + "witness": 11, + "zero_pairs": 30 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 18, + "resolved": true, + "seed": 20262205, + "threshold": 7, + "tied_lines": 5, + "v": 11, + "witness": 11, + "zero_pairs": 26 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 19, + "resolved": true, + "seed": 20262206, + "threshold": 7, + "tied_lines": 7, + "v": 11, + "witness": 11, + "zero_pairs": 19 + }, + { + "evals": 67, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 16, + "resolved": true, + "seed": 20262219, + "threshold": 8, + "tied_lines": 3, + "v": 12, + "witness": 12, + "zero_pairs": 41 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 17, + "resolved": true, + "seed": 20262220, + "threshold": 8, + "tied_lines": 3, + "v": 12, + "witness": 12, + "zero_pairs": 30 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 19, + "resolved": true, + "seed": 20262221, + "threshold": 8, + "tied_lines": 5, + "v": 12, + "witness": 12, + "zero_pairs": 34 + }, + { + "evals": 150, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 19, + "resolved": true, + "seed": 20262222, + "threshold": 8, + "tied_lines": 5, + "v": 12, + "witness": 11, + "zero_pairs": 39 + }, + { + "evals": 1, + "falsifier": false, + "family": "config", + "min_cost_exact": false, + "min_cost_upper": 16, + "resolved": true, + "seed": 20262223, + "threshold": 8, + "tied_lines": 3, + "v": 12, + "witness": 12, + "zero_pairs": 28 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 12, + "resolved": true, + "seed": 20263083, + "threshold": 2, + "tied_lines": 3, + "v": 4, + "witness": 4, + "zero_pairs": 0 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 12, + "resolved": true, + "seed": 20263084, + "threshold": 2, + "tied_lines": 2, + "v": 4, + "witness": 4, + "zero_pairs": 0 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 12, + "resolved": true, + "seed": 20263085, + "threshold": 2, + "tied_lines": 2, + "v": 4, + "witness": 4, + "zero_pairs": 0 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 12, + "resolved": true, + "seed": 20263086, + "threshold": 2, + "tied_lines": 2, + "v": 4, + "witness": 4, + "zero_pairs": 0 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 12, + "resolved": true, + "seed": 20263087, + "threshold": 2, + "tied_lines": 2, + "v": 4, + "witness": 4, + "zero_pairs": 1 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 12, + "resolved": true, + "seed": 20263088, + "threshold": 2, + "tied_lines": 2, + "v": 4, + "witness": 4, + "zero_pairs": 0 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 12, + "resolved": true, + "seed": 20263089, + "threshold": 2, + "tied_lines": 2, + "v": 4, + "witness": 4, + "zero_pairs": 1 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 12, + "resolved": true, + "seed": 20263090, + "threshold": 2, + "tied_lines": 2, + "v": 4, + "witness": 4, + "zero_pairs": 1 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 15, + "resolved": true, + "seed": 20263100, + "threshold": 3, + "tied_lines": 3, + "v": 5, + "witness": 5, + "zero_pairs": 2 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 15, + "resolved": true, + "seed": 20263101, + "threshold": 3, + "tied_lines": 3, + "v": 5, + "witness": 5, + "zero_pairs": 2 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 15, + "resolved": true, + "seed": 20263102, + "threshold": 3, + "tied_lines": 3, + "v": 5, + "witness": 5, + "zero_pairs": 1 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 15, + "resolved": true, + "seed": 20263103, + "threshold": 3, + "tied_lines": 3, + "v": 5, + "witness": 5, + "zero_pairs": 1 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 15, + "resolved": true, + "seed": 20263104, + "threshold": 3, + "tied_lines": 3, + "v": 5, + "witness": 5, + "zero_pairs": 0 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 15, + "resolved": true, + "seed": 20263105, + "threshold": 3, + "tied_lines": 3, + "v": 5, + "witness": 5, + "zero_pairs": 0 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 15, + "resolved": true, + "seed": 20263106, + "threshold": 3, + "tied_lines": 3, + "v": 5, + "witness": 5, + "zero_pairs": 0 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 15, + "resolved": true, + "seed": 20263107, + "threshold": 3, + "tied_lines": 3, + "v": 5, + "witness": 5, + "zero_pairs": 1 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 18, + "resolved": true, + "seed": 20263117, + "threshold": 4, + "tied_lines": 3, + "v": 6, + "witness": 6, + "zero_pairs": 0 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 18, + "resolved": true, + "seed": 20263118, + "threshold": 4, + "tied_lines": 4, + "v": 6, + "witness": 6, + "zero_pairs": 2 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 18, + "resolved": true, + "seed": 20263119, + "threshold": 4, + "tied_lines": 4, + "v": 6, + "witness": 6, + "zero_pairs": 2 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 18, + "resolved": true, + "seed": 20263120, + "threshold": 4, + "tied_lines": 3, + "v": 6, + "witness": 6, + "zero_pairs": 0 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 18, + "resolved": true, + "seed": 20263121, + "threshold": 4, + "tied_lines": 5, + "v": 6, + "witness": 6, + "zero_pairs": 1 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 18, + "resolved": true, + "seed": 20263122, + "threshold": 4, + "tied_lines": 3, + "v": 6, + "witness": 6, + "zero_pairs": 2 + }, + { + "evals": 145, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 15, + "resolved": true, + "seed": 20263123, + "threshold": 4, + "tied_lines": 4, + "v": 6, + "witness": 6, + "zero_pairs": 4 + }, + { + "evals": 82, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 15, + "resolved": true, + "seed": 20263124, + "threshold": 4, + "tied_lines": 3, + "v": 6, + "witness": 6, + "zero_pairs": 8 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 21, + "resolved": true, + "seed": 20263134, + "threshold": 4, + "tied_lines": 4, + "v": 7, + "witness": 7, + "zero_pairs": 2 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 21, + "resolved": true, + "seed": 20263135, + "threshold": 4, + "tied_lines": 4, + "v": 7, + "witness": 7, + "zero_pairs": 3 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 21, + "resolved": true, + "seed": 20263136, + "threshold": 4, + "tied_lines": 5, + "v": 7, + "witness": 7, + "zero_pairs": 3 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 21, + "resolved": true, + "seed": 20263137, + "threshold": 4, + "tied_lines": 7, + "v": 7, + "witness": 7, + "zero_pairs": 2 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 21, + "resolved": true, + "seed": 20263138, + "threshold": 4, + "tied_lines": 4, + "v": 7, + "witness": 7, + "zero_pairs": 2 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 21, + "resolved": true, + "seed": 20263139, + "threshold": 4, + "tied_lines": 4, + "v": 7, + "witness": 7, + "zero_pairs": 5 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 21, + "resolved": true, + "seed": 20263140, + "threshold": 4, + "tied_lines": 4, + "v": 7, + "witness": 7, + "zero_pairs": 0 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 21, + "resolved": true, + "seed": 20263141, + "threshold": 4, + "tied_lines": 5, + "v": 7, + "witness": 7, + "zero_pairs": 4 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 24, + "resolved": true, + "seed": 20263151, + "threshold": 5, + "tied_lines": 4, + "v": 8, + "witness": 8, + "zero_pairs": 3 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 24, + "resolved": true, + "seed": 20263152, + "threshold": 5, + "tied_lines": 4, + "v": 8, + "witness": 8, + "zero_pairs": 0 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 24, + "resolved": true, + "seed": 20263153, + "threshold": 5, + "tied_lines": 4, + "v": 8, + "witness": 8, + "zero_pairs": 2 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 24, + "resolved": true, + "seed": 20263154, + "threshold": 5, + "tied_lines": 5, + "v": 8, + "witness": 8, + "zero_pairs": 5 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 24, + "resolved": true, + "seed": 20263155, + "threshold": 5, + "tied_lines": 4, + "v": 8, + "witness": 8, + "zero_pairs": 3 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 24, + "resolved": true, + "seed": 20263156, + "threshold": 5, + "tied_lines": 7, + "v": 8, + "witness": 8, + "zero_pairs": 1 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 24, + "resolved": true, + "seed": 20263157, + "threshold": 5, + "tied_lines": 4, + "v": 8, + "witness": 8, + "zero_pairs": 2 + }, + { + "evals": 150, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 21, + "resolved": true, + "seed": 20263158, + "threshold": 5, + "tied_lines": 6, + "v": 8, + "witness": 7, + "zero_pairs": 5 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 27, + "resolved": true, + "seed": 20263168, + "threshold": 6, + "tied_lines": 5, + "v": 9, + "witness": 9, + "zero_pairs": 0 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 27, + "resolved": true, + "seed": 20263169, + "threshold": 6, + "tied_lines": 5, + "v": 9, + "witness": 9, + "zero_pairs": 2 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 27, + "resolved": true, + "seed": 20263170, + "threshold": 6, + "tied_lines": 5, + "v": 9, + "witness": 9, + "zero_pairs": 1 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 27, + "resolved": true, + "seed": 20263171, + "threshold": 6, + "tied_lines": 5, + "v": 9, + "witness": 9, + "zero_pairs": 4 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 30, + "resolved": true, + "seed": 20263185, + "threshold": 6, + "tied_lines": 5, + "v": 10, + "witness": 10, + "zero_pairs": 6 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 30, + "resolved": true, + "seed": 20263186, + "threshold": 6, + "tied_lines": 5, + "v": 10, + "witness": 10, + "zero_pairs": 3 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 30, + "resolved": true, + "seed": 20263187, + "threshold": 6, + "tied_lines": 5, + "v": 10, + "witness": 10, + "zero_pairs": 6 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 30, + "resolved": true, + "seed": 20263188, + "threshold": 6, + "tied_lines": 6, + "v": 10, + "witness": 10, + "zero_pairs": 5 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 33, + "resolved": true, + "seed": 20263202, + "threshold": 7, + "tied_lines": 8, + "v": 11, + "witness": 11, + "zero_pairs": 6 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 33, + "resolved": true, + "seed": 20263203, + "threshold": 7, + "tied_lines": 6, + "v": 11, + "witness": 11, + "zero_pairs": 3 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 33, + "resolved": true, + "seed": 20263204, + "threshold": 7, + "tied_lines": 6, + "v": 11, + "witness": 11, + "zero_pairs": 5 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 33, + "resolved": true, + "seed": 20263205, + "threshold": 7, + "tied_lines": 6, + "v": 11, + "witness": 11, + "zero_pairs": 3 + }, + { + "evals": 150, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 33, + "resolved": true, + "seed": 20263219, + "threshold": 8, + "tied_lines": 6, + "v": 12, + "witness": 11, + "zero_pairs": 9 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 36, + "resolved": true, + "seed": 20263220, + "threshold": 8, + "tied_lines": 7, + "v": 12, + "witness": 12, + "zero_pairs": 8 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 36, + "resolved": true, + "seed": 20263221, + "threshold": 8, + "tied_lines": 7, + "v": 12, + "witness": 12, + "zero_pairs": 3 + }, + { + "evals": 1, + "falsifier": false, + "family": "tied", + "min_cost_exact": true, + "min_cost_upper": 36, + "resolved": true, + "seed": 20263222, + "threshold": 8, + "tied_lines": 8, + "v": 12, + "witness": 12, + "zero_pairs": 2 + } +] diff --git a/research/fstar-cert-census-seed298df375/CERTIFICATE.json b/research/fstar-cert-census-seed298df375/CERTIFICATE.json new file mode 100644 index 0000000000..fc6c87255e --- /dev/null +++ b/research/fstar-cert-census-seed298df375/CERTIFICATE.json @@ -0,0 +1,99 @@ +{ + "by_family": { + "config": { + "instances": 70, + "max_tied_lines": 7, + "min_witness_ratio": 0.8571428571428571, + "resolved": 70 + }, + "dense": { + "instances": 70, + "max_tied_lines": 5, + "min_witness_ratio": 0.8888888888888888, + "resolved": 70 + }, + "tied": { + "instances": 56, + "max_tied_lines": 8, + "min_witness_ratio": 0.875, + "resolved": 56 + } + }, + "census_digest": "3237519deb9ec377f5a8a86b7b4b1e8197074ee8d0dd0e653cfcea1104c9e6e8", + "claim": "F-star: cert(M) >= floor(2v/3) for exact 3-total rational decoders", + "controls": { + "binding_pair_order_rejected": true, + "bruteforce_crosscheck": [ + { + "brute": 3, + "family": "dense", + "search": 3, + "v": 3 + }, + { + "brute": 3, + "family": "config", + "search": 3, + "v": 3 + }, + { + "brute": 3, + "family": "tied", + "search": 3, + "v": 3 + } + ], + "chain_control": { + "brute_cert": 4, + "min_cost": 7, + "min_cost_exact": true + }, + "corrupted_witness_rejected": true, + "diagonal_control_cert": 3, + "threshold_table": { + "4": 2, + "5": 3, + "6": 4, + "7": 4, + "8": 5, + "9": 6, + "10": 6, + "11": 7, + "12": 8 + } + }, + "domain": { + "factor_entries": "-2..2", + "families": [ + "dense", + "config", + "tied" + ], + "seeds": "20261015 + 1000*family_index + 17*v + i", + "totals": 3, + "v": "4..12" + }, + "falsifiers": 0, + "instances": 196, + "min_witness_ratio": 0.8571428571428571, + "no_new_kappa": true, + "outcome": "SCOPED_NEGATIVE_NO_FALSIFIER", + "resolved_witness": 196, + "schema_version": 1, + "source": "research/root-unit-decoder-lemmas/README.md section 7 (OPEN)", + "unresolved": 0, + "worst_instance": { + "evals": 150, + "falsifier": false, + "family": "config", + "min_cost_exact": true, + "min_cost_upper": 12, + "resolved": true, + "seed": 20262138, + "threshold": 4, + "tied_lines": 4, + "v": 7, + "witness": 6, + "zero_pairs": 10 + } +} diff --git a/research/fstar-cert-census-seed298df375/README.md b/research/fstar-cert-census-seed298df375/README.md new file mode 100644 index 0000000000..6864337d61 --- /dev/null +++ b/research/fstar-cert-census-seed298df375/README.md @@ -0,0 +1,151 @@ +# fstar-cert-census-seed298df375 + +**Scoped negative result (no new kappa, no frontier change).** An exact falsifier +census for open problem **F-star** of `research/root-unit-decoder-lemmas` +(section 7, OPEN): over 196 declared exact 3-total rational decoders on +v = 4..12 lines, every instance carries a machine-checked labelling/order +witness with `|S| >= floor(2v/3)`, and no falsifier was found. This is evidence +for F-star over the declared domain, not a proof of the statement. + +## Scope and question + +For a rational 3-total decoder `M = sum_{j=1..3} p_j q_j^T` on v lines with +`M_tt != 0` on every line, the source package defines an **L8 labelling**: +F2 vectors `a(t)` supported in `Omega(t) = {j : p_j(t) != 0}` and `b(s)` +supported in `Psi(s) = {j : q_j(s) != 0}`, with `K_ts = a(t) dot b(s) mod 2`. +`cert(M)` is the largest `|S|` admitting an order with `K_tt = 1` on S and +`K_ts = 0` at every incidence `M_ts = 0` with t before s. F-star states +`cert(M) >= floor(2v/3)` for every exact 3-total decoder. The source package's +proven consequence: F-star closes every open T = 3 window at once. The source +states F-star as OPEN with about 90 sampled configurations at `cert = v` +(RECORDED, not reproduced there). + +Both bounds in this package are reading-independent: `cert(M)` does not depend +on any pairing B, and the witnesses prove `cert(M) >= |S|` for the sampled +decoders under any reading of "exact decoder on a root unit". A found falsifier +would have been a falsifier under the universal reading (any 0/1 unit-diagonal +B with ones only where M vanishes); the unit-attached reading needs unit Gram +tables and remains open question 2 in TASK.json. + +## Method + +Two exact sides, stdlib only, deterministic (fixed seeds `20261015 + 1000*family +index + 17*v + i`): + +- **Side B (lower bound on `cert`).** Deterministic local search over labellings; + each labelling is scored by the exact maximum acyclic subset of the incidence + digraph (subset DP), and the maximizing subset and sink-peeling order are + stored and replayed by an independent witness checker. +- **Side A (upper bound on `cert`, falsifier hunt).** The source package's + proven chain `cert(M) <= sum_j rank_F2 B[R_j, A_j]` for every admissible B + (0/1, unit diagonal, `B_ts = 1` only where `M_ts = 0`, s != t; the chain's + proof uses only these two properties, so asymmetric B are included). The cost + is minimized by exhaustive enumeration when the admissible pair count is at + most 10 (always at v <= 5) and by deterministic single-bit local search + otherwise. Any instance with minimum cost below `floor(2v/3)` would falsify + F-star. + +Domain: v in 4..12, exactly 3 totals, factor entries in `{-2,-1,0,1,2}` with +nonzero diagonal; three families: **dense** (random factors), **config** +(`M = P Q^T` with `P,Q` over `{-1,0,1}`, the rank-3 configuration model of +https://github.com/CrocSwap/integer-mult-bounds/pull/2111), **tied** (a +2-adic-weighted alphabet, retained only when tied minimal valuations cover at +least half the lines: the obstruction named in the source section 7). + +## Evidence + +`python3 -B research/fstar-cert-census-seed298df375/verify.py` recomputes +everything and writes `CERTIFICATE.json` and `CENSUS-RECORDS.json` +(census digest `3237519deb9ec377f5a8a86b7b4b1e8197074ee8d0dd0e653cfcea1104c9e6e8`). + +| family | instances | resolved with witness | falsifiers | min witness ratio | +|---|---:|---:|---:|---:| +| dense | 70 | 70 | 0 | 8/9 = 0.889 | +| config | 70 | 70 | 0 | 6/7 = 0.857 | +| tied | 56 | 56 | 0 | 7/8 = 0.875 | + +All 196 instances resolved: `cert(M) >= witness >= floor(2v/3)`. No falsifier +and no unresolved instance. The worst instance (lowest witness ratio) is the +config instance at `v = 7`, seed `20262138`: witness 6 against threshold 4, so +`cert(M) in [6, 12]` there (12 is its exact admissible-B cost minimum). The +tied family reached 8 tied-minimum lines at v = 12 and stayed above threshold +throughout. + +Controls (all in `verify.py`, all required to pass): + +1. Three tiny-domain instances (v = 3) are certified by exhaustive enumeration + of every labelling; the search engine must reproduce those exact values + (3/3 agree). +2. A corrupted witness (one `K_tt` broken) and a wrong order at a binding pair + are both rejected by the independent witness checker. +3. The `floor(2v/3)` threshold table is checked against hand values for + v = 4..12. +4. A hand-checkable diagonal decoder (`p_j = q_j = e_j`) gives `cert = 3`. +5. The proven chain `cert(M) <= cost(B)` is rechecked on every census instance, + and an exact-chain control pins `brute_cert = 4 <= min_cost = 7`. + +## What is not claimed + +F-star is **not** proved: witnesses are lower bounds on `cert(M)`, and only the +recorded 196 instances are covered. The census is not exhaustive over decoders; +it is exhaustive over labellings only for the tiny controls. `cert(M)` values +are not pinned exactly above v = 3 (the worst instance above has `cert` in +[6, 7]). Nothing here changes kappa, any supplier, the selected record, or any +window; the T = 3 window closure remains conditional on F-star. The universal +versus unit-attached readings of the quantifier are not separated. + +## Reproduce + +From the repository root, Python 3.10+ standard library only: + +```sh +python3 -B research/fstar-cert-census-seed298df375/verify.py +python3 scripts/research_package.py --package research/fstar-cert-census-seed298df375 --check-only +python3.12 scripts/research_package.py --package research/fstar-cert-census-seed298df375 +``` + +Expected markers: + +```text +PASS_FSTAR_CERT_CENSUS instances=196 resolved=196 falsifiers=0 unresolved=0 min_ratio=0.8571 digest=3237519deb9ec377 +PASS_FSTAR_CERT_CONTROLS bruteforce=3 diagonal_cert=3 chain_cert=4 +``` + +The registered CPython 3.12 replay prints `PASS_REGISTERED_RESEARCH_PACKAGE +research/fstar-cert-census-seed298df375 outcome=completed`. `make` is not +installed on the authoring host; the scripts above are the underlying commands. + +## Open next questions + +1. **Exact `cert(M)` for the worst instance** (config, v = 7, seed 20262138, + `cert` in [6, 7]). Why it matters: it is the smallest witness ratio seen and + the natural place to look for sub-v certificates, which would sharpen what + F-star can promise. First step: branch-and-bound over labellings at v = 7 + with the maximum-acyclic-subset bound, or a larger deterministic search + budget. Blocker: none structural; needs a longer exact run. +2. **Universal versus unit-attached readings.** Why it matters: a separation + decides whether a future falsifier refutes the lemma as stated or only its + universal reading. First step: wire A3/A4/D4 Gram tables into `min_cost_pairing` + and compare admissible-B minima on the same decoders. Blocker: unit tables + are not in this package. +3. **Tied-minima family at v = 13..18** (see TASK.json). The named obstruction + accumulates with v; the census stops at v = 12. + +## Credit and provenance + +F-star, the `cert(M)` definition, L8 labellings and the proven chain +`cost >= sum_j r_j >= cert(M)` are from the merged package +`research/root-unit-decoder-lemmas` (root units, Lemmas A and B, the L8 lemma; +[PR 1590](https://github.com/CrocSwap/integer-mult-bounds/pull/1590) by +DreamingOfClouds, with Claude Opus 5.5 (Anthropic) via Claude Code +assistance). The rank-3 configuration +model, the `tied_min` / `cex_min_1` examples and their certificate limits are +DreamingOfClouds' work in https://github.com/CrocSwap/integer-mult-bounds/pull/2111 +and https://github.com/CrocSwap/integer-mult-bounds/pull/2162 (one-copy +certificates stopping at 11 and 18 there; this package does not restate those +examples). The adjacent independent CR2/B2 audit is +https://github.com/CrocSwap/integer-mult-bounds/pull/2293 (Aaron Wang). The +source README is pinned as an input in SOURCES.json. + +Prepared by **Aaron Wang** with help from opencode (substantial AI assistance; +no independent human review claimed). New work in this package is Apache-2.0. diff --git a/research/fstar-cert-census-seed298df375/SOURCES.json b/research/fstar-cert-census-seed298df375/SOURCES.json new file mode 100644 index 0000000000..afe8ee671f --- /dev/null +++ b/research/fstar-cert-census-seed298df375/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/root-unit-decoder-lemmas/README.md", + "usage": "input", + "git_blob": "de305484c78226a3f8da5f3277ced78974116fbb", + "sha256": "e3c856bc361a57cc2424c829001dba94e8f3a1bc8f6616f9c2f740e9665506a9" + } + ] +} diff --git a/research/fstar-cert-census-seed298df375/TASK.json b/research/fstar-cert-census-seed298df375/TASK.json new file mode 100644 index 0000000000..5410b7bed9 --- /dev/null +++ b/research/fstar-cert-census-seed298df375/TASK.json @@ -0,0 +1,75 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?", + "starting_points": [ + "certificates/selected-result.json", + "docs/audit.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected review scope and choose one exact all-size or precision implication.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write its quantified inputs and conclusion; find a missing hypothesis or construct a minimal exact adversarial instance.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "Choose one tape, precision, hosting or restoration lemma." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision" + ] + }, + "scope_status": "changed", + "actual_scope": "F-star falsifier census: for exact 3-total rational decoders M = sum_j p_j q_j^T on v lines (M_tt nonzero), test the open problem F* of research/root-unit-decoder-lemmas section 7, cert(M) >= floor(2v/3), where cert(M) is maximized over L8 labellings of the largest ordered subset S with K_tt = 1 on S and K_ts = 0 at every incidence M_ts = 0 with t before s. Two exact sides: (A) falsifier hunt via the proven chain cert(M) <= sum_j rank_F2 B[R_j, A_j] over every admissible pairing B (0/1, unit diagonal, ones only where M vanishes); (B) witness side exhibiting a labelling and order with |S| >= floor(2v/3).", + "scope_change_reason": "Pair-collision rule and drawn-card saturation. The OS draw (nonce 298df3754c1488b77620ddda3eb48b27, track adversarial-audit) offered, in order, uniform-transfer-audit, supplier-boundary-audit and selected-stock-envelope. uniform-transfer-audit was completed today on its hosting-implication refinement (https://github.com/CrocSwap/integer-mult-bounds/pull/2273, comment https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18939459); supplier-boundary-audit was completed today on its owner-map binding refinement (https://github.com/CrocSwap/integer-mult-bounds/pull/2301, comment https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18940382); selected-stock-envelope is covered by a live claim (https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18932014) and the PR2084/PR2120 first-stage coefficient work. All three first-choice objects are recent claimed or completed objects, so this session takes the explicit open-problem route instead: open problem F* of the merged research/root-unit-decoder-lemmas package (section 7, OPEN), which the handoffs thread's T=3 open-core request (https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18932893 item 4) invites independent eyes on. This keeps the adversarial-audit method of the drawn card (exact counterexample search at a claimed implication) while changing the object to an unclaimed named lemma.", + "existing_restriction_being_changed": "Nothing is relaxed: F* is tested as stated (all exact 3-total rational decoders, all v). Two readings of the quantifier are audited separately: the universal reading (any 0/1 unit-diagonal pairing B with ones only where M vanishes) and the unit-attached reading (B admissible for a concrete root unit, zero on non-orthogonal pairs).", + "method": "Exact stdlib-only arithmetic. Zero patterns of M and of the factor supports drive cert; F2 ranks use Gaussian elimination mod 2. Side A: for each sampled decoder compute the minimum of sum_j rank_F2 B[R_j, A_j] over pairings B (exhaustive for v <= 5, deterministic local search plus B = I baseline for larger v) and compare with floor(2v/3). Side B: search L8 labellings by backtracking and score each by the exact maximum acyclic subset of the incidence digraph (subset DP), then exhibit the maximizing labelling, subset and order as a machine-checked witness. Controls: hand-checkable tiny decoders with brute-force-over-all-labellings cross-check, a deliberately corrupted witness must be rejected, and the proven inequality cert(M) <= sum_j rank_F2 B[R_j, A_j] is rechecked on every instance that has an exhibited witness and a computed pairing cost.", + "parameter_ranges": "v in 4..12; T = 3 totals exactly; factor entries in {-2,-1,0,1,2} with M_tt nonzero on every line; three families: (i) dense random factors, (ii) configuration-style M = P Q^T with P,Q in {-1,0,1}^{v x 3} (many orthogonal pairs, the rank-3 configuration model of https://github.com/CrocSwap/integer-mult-bounds/pull/2111), (iii) tied-minima 2-adic constructions whose products p_k(t) q_k(t) attain their minimum 2-adic valuation twice or more, the obstruction named in research/root-unit-decoder-lemmas section 7.", + "nearest_overlapping_prs": "https://github.com/CrocSwap/integer-mult-bounds/pull/2111 (DreamingOfClouds: reductions and certificate limits on tied_min and cex_min_1; records one-copy certificates stopping at 11 and 18, does not search for F* falsifiers and states no F* census); https://github.com/CrocSwap/integer-mult-bounds/pull/2162 and https://github.com/CrocSwap/integer-mult-bounds/pull/2277 (char-2 jets CR2/B2 and dense-pairing overcomplete floors; different statements); the source package research/root-unit-decoder-lemmas (merged) states F* as OPEN with about 90 sampled configurations at cert = v. Overlap helper run on refined terms 'cert(M)', 'L8 labelling', '2-adic certificate', 'tied minima', '2v/3' returned only these two predecessors (2026-10-15 05:24 UTC, complete pagination 539 open PRs / 1038 discussions).", + "optimistic_full_cost_budget": "No kappa, supplier, word or moment budget is in play; this is a missing-lemma audit. The whole-construction price is the exact census itself: all counts, ranks and witnesses are recomputed by the verifier in one bounded run (no sampling left implicit).", + "bottleneck_link": "F-star is the named route to closing every open T = 3 window at once (research/root-unit-decoder-lemmas section 7 consequence, PROVEN given F*): it would give cost >= floor(2v/3) >= N(h) for all open T = 3 windows. A falsifier would redirect the T = 3 decoder route; certified evidence widens the domain where the closure argument can be trusted. Finite supplier improvements matter only under the retained transfer obligations, and this audit addresses one such inherited implication without touching kappa.", + "stop_rule": "Stop at the first exact falsifier (an instance with min_B sum_j rank_F2 B[R_j, A_j] < floor(2v/3), fully recorded), or, absent one, at the declared-domain census with machine-checked witnesses for every sampled instance and the exact obstruction recorded for any instance where no witness reaches the threshold. Time cap: about 40 minutes of computation, one bounded pivot maximum.", + "success_evidence": "A falsifier instance with exact pairing-cost minimization and the failing threshold recorded, or a scoped census: exact counts per family and v, the minimum achieved witness ratio |S|/v, every witness replayed by verify.py, the proven-chain inequality checked per instance, and the tiny-domain brute-force cross-check agreeing with the search engine.", + "falsification_test": "Side A is itself the falsifier test for F*; its negative control is a constructed instance where the pairing cost is forced below threshold by hand (if such exists in the domain). Side B witnesses are rejected if any K_tt = 1 or any before-pair constraint fails; a corrupted copy of a stored witness must fail verification.", + "time_compute_cap": "One session; compute capped at about 40 minutes single-process stdlib Python; no SAT solver, no third-party packages, no large downloads.", + "predecessor_authors": "F* and the cert(M) definition: the research/root-unit-decoder-lemmas package (merged, Douglas Colkitt with OpenAI Codex assistance lineage; Lemmas A and B and the L8 lemma are its PROVEN results). Rank-3 configuration model, tied_min and cex_min_1 examples and certificate limits: DreamingOfClouds, https://github.com/CrocSwap/integer-mult-bounds/pull/2111 and https://github.com/CrocSwap/integer-mult-bounds/pull/2162. Independent CR2/B2 audit: Aaron Wang, https://github.com/CrocSwap/integer-mult-bounds/pull/2293. This package does not claim their results; it adds a declared-domain F* falsifier census and machine-checked witnesses.", + "intended_artifact": "research/fstar-cert-census-seed298df375/ with TASK.json, SOURCES.json pins, verify.py, CERTIFICATE.json, RESULT.json, README.md; reproduction: python3 -B research/fstar-cert-census-seed298df375/verify.py then python3 scripts/research_package.py --package research/fstar-cert-census-seed298df375 --check-only.", + "outcome": "completed", + "evidence": "SCOPED NEGATIVE over the declared domain: 196/196 instances carry machine-checked witnesses |S| >= floor(2v/3) (70 dense, 70 config, 56 tied; v = 4..12); zero falsifiers, zero unresolved; minimum achieved witness ratio 6/7 = 0.857 (config family, v = 7, seed 20262138; its admissible-B upper bound is 12). Controls pass: three tiny-domain brute-force cross-checks agree with the search engine exactly, corrupted and wrong-order witnesses are rejected, the diagonal control gives cert = 3, and the proven chain cert(M) <= cost(B) is rechecked per instance. Recorded in CERTIFICATE.json (census digest 3237519deb9ec377f5a8a86b7b4b1e8197074ee8d0dd0e653cfcea1104c9e6e8) and CENSUS-RECORDS.json. This is evidence for F*, not a proof: witnesses are lower bounds on cert(M), and only the recorded instances are covered.", + "author": "Aaron Wang (with help from opencode)", + "ai_assistance": "Substantial AI assistance: this package was produced by Aaron Wang with help from opencode (opencode agent harness). No independent human review claimed. No model is cited per orchestrator attribution rules.", + "open_questions": [ + { + "question": "Does F-star hold for tied-minima 2-adic decoders at larger v (beyond the declared v <= 12 domain), where the named obstruction (isotropic lines with tied minimal valuations) accumulates?", + "why_it_matters": "F-star would close every open T = 3 window; the tied-minima family is the only obstruction the source package could not order.", + "first_step": "Extend the census family (iii) to v = 13..18 with the same witness engine and record the minimum achieved |S|/v as a function of the tied-minima count.", + "blocked_by": "Nothing structural; needs a longer deterministic run than one session allows." + }, + { + "question": "Is the universal reading of F-star (any 0/1 unit-diagonal pairing with ones only where M vanishes) equivalent to the unit-attached reading (B admissible for a concrete root unit)?", + "why_it_matters": "A falsifier for the universal reading would refute the lemma as stated in section 7; a separation would pin which reading the window-closure consequence needs.", + "first_step": "Enumerate small units (A3, A4, D4) with their orthogonality patterns and compare min_B pairing costs inside and outside the admissible family on the same decoders.", + "blocked_by": "Needs the unit Gram tables wired into the search; the current census keeps the two readings separate by construction." + } + ] +} diff --git a/research/fstar-cert-census-seed298df375/VERIFY.json b/research/fstar-cert-census-seed298df375/VERIFY.json new file mode 100644 index 0000000000..577a4ec5d7 --- /dev/null +++ b/research/fstar-cert-census-seed298df375/VERIFY.json @@ -0,0 +1,16 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/root-unit-decoder-lemmas/README.md" + ], + "commands": [ + { + "argv": ["{python}", "-B", "{package}/verify.py"], + "timeout_seconds": 600, + "checks": "F-star census over 196 declared instances (v = 4..12, three families) with machine-checked labelling/order witnesses and per-instance admissible-B costs; controls: three tiny-domain brute-force cross-checks of the search engine, a corrupted witness and a wrong-order witness must be rejected, the floor(2v/3) threshold table, a hand-checkable diagonal decoder, and the proven chain cert(M) <= cost(B) rechecked on every instance; prints PASS_FSTAR_CERT_CENSUS and PASS_FSTAR_CERT_CONTROLS" + } + ] +} diff --git a/research/fstar-cert-census-seed298df375/verify.py b/research/fstar-cert-census-seed298df375/verify.py new file mode 100644 index 0000000000..e6c17946e8 --- /dev/null +++ b/research/fstar-cert-census-seed298df375/verify.py @@ -0,0 +1,518 @@ +#!/usr/bin/env python3 +"""F-star falsifier census for exact 3-total rational decoders (stdlib only). + +Object: open problem F* of research/root-unit-decoder-lemmas section 7. For a +rational 3-total decoder M = sum_j p_j q_j^T on v lines with M_tt != 0, an L8 +labelling chooses a(t) supported in Omega(t) = {j : p_j(t) != 0} and b(s) +supported in Psi(s) = {j : q_j(s) != 0}, K_ts = a(t).b(s) mod 2. cert(M) is the +largest |S| admitting an order with K_tt = 1 on S and K_ts = 0 at every +incidence M_ts = 0 with t before s. F* states cert(M) >= floor(2v/3). + +Two exact sides: + Side B (lower bound on cert): exhibit a labelling, subset and order witness. + Side A (upper bound on cert, falsifier hunt): the proven chain of the source + package gives cert(M) <= sum_j rank_F2 B[R_j, A_j] for every 0/1 unit-diagonal + pairing B with ones only where M vanishes. Any instance whose minimum such + cost falls below floor(2v/3) is a falsifier of F* (universal reading). + +Everything is deterministic: the only randomness comes from fixed seeds. +Aaron Wang, with help from opencode. Apache-2.0. +""" +import hashlib +import json +import random +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +T = 3 + + +# ---------------------------------------------------------------- F2 linear algebra + +def f2_rank(rows, ncols): + """Rank over F2 of a matrix given as a list of bitmasks (bit c = column c).""" + basis = {} + for r in rows: + x = r + while x: + c = x.bit_length() - 1 + if c in basis: + x ^= basis[c] + else: + basis[c] = x + break + return len(basis) + + +# ---------------------------------------------------------------- instance model + +class Decoder: + """M = sum_{j> j) & 1 and j not in self.omega[t] for j in range(T)): + continue + for bmask in range(1 << T): + if any((bmask >> j) & 1 and j not in self.psi[t] for j in range(T)): + continue + opts.append((amask, bmask)) + return opts + + +def threshold(v): + return (2 * v) // 3 + + +def kval(a, b): + return bin(a & b).count("1") & 1 + + +# ---------------------------------------------------------------- Side B: witnesses + +def cert_witness(dec, labels): + """MAS of the incidence digraph on valid lines, with order. labels[t] = (a, b).""" + v = dec.v + valid = [t for t in range(v) if kval(labels[t][0], labels[t][1]) == 1] + if not valid: + return 0, [], [] + index = {t: i for i, t in enumerate(valid)} + n = len(valid) + outmask = [0] * n + for ti in valid: + for s in valid: + if s != ti and dec.zero[ti][s] and kval(labels[ti][0], labels[s][1]) == 1: + outmask[index[ti]] |= 1 << index[s] + full = (1 << n) - 1 + dp = bytearray(1 << n) + dp[0] = 1 + best = 0 + bestmask = 0 + for mask in range(1, 1 << n): + m = mask + while m: + bit = m & -m + u = bit.bit_length() - 1 + if dp[mask ^ bit] and (outmask[u] & (mask ^ bit)) == 0: + dp[mask] = 1 + if mask.bit_count() > best: + best = mask.bit_count() + bestmask = mask + break + m ^= bit + subset = [valid[i] for i in range(n) if (bestmask >> i) & 1] + # Sink-peeling order: sinks first. Edge u->w requires w before u. + order = [] + remaining = set(subset) + while remaining: + sinks = sorted(t for t in remaining + if not any(s in remaining and s != t and dec.zero[t][s] + and kval(labels[t][0], labels[s][1]) == 1 for s in remaining)) + assert sinks, "MAS subset must be acyclic" + order.extend(sinks) + remaining -= set(sinks) + return best, subset, order + + +def witness_ok(dec, labels, subset, order): + """Independent replay of the witness conditions.""" + pos = {t: i for i, t in enumerate(order)} + if sorted(order) != sorted(subset) or len(set(order)) != len(order): + return False + for t in subset: + if kval(labels[t][0], labels[t][1]) != 1: + return False + for t in subset: + for s in subset: + # t before s at an incidence M_ts = 0 requires K_ts == 0. + if s != t and dec.zero[t][s] and pos[t] < pos[s]: + if kval(labels[t][0], labels[s][1]) != 0: + return False + return True + + +def search_labels(dec, budget=150, seed=0): + """Deterministic local search over labellings maximising the witness size.""" + v = dec.v + rng = random.Random(seed) + options = [dec.label_options(t) for t in range(v)] + base = [] + for t in range(v): + common = sorted(dec.omega[t] & dec.psi[t]) + j = common[0] + base.append((1 << j, 1 << j)) + best_labels = list(base) + best_size, best_subset, best_order = cert_witness(dec, best_labels) + evals = 1 + improved = True + while improved and evals < budget and best_size < v: + improved = False + for t in range(v): + for opt in options[t]: + if opt == best_labels[t]: + continue + trial = list(best_labels) + trial[t] = opt + size, subset, order = cert_witness(dec, trial) + evals += 1 + if size > best_size: + best_size, best_subset, best_order = size, subset, order + best_labels = trial + improved = True + if evals >= budget or best_size == v: + break + if evals >= budget or best_size == v: + break + if best_size < v and evals < budget: + for _restart in range(3): + if evals >= budget or best_size == v: + break + trial = list(best_labels) + for t in rng.sample(range(v), k=max(1, v // 3)): + trial[t] = rng.choice(options[t]) + for t in range(v): + for opt in options[t]: + if opt == trial[t]: + continue + cand = list(trial) + cand[t] = opt + size, subset, order = cert_witness(dec, cand) + evals += 1 + if size > best_size: + best_size, best_subset, best_order = size, subset, order + best_labels = cand + if evals >= budget or best_size == v: + break + if evals >= budget or best_size == v: + break + return best_size, best_labels, best_subset, best_order, evals + + +def brute_cert(dec): + """Exact cert by enumerating every labelling (tiny v only).""" + v = dec.v + options = [dec.label_options(t) for t in range(v)] + best = 0 + labels = [None] * v + + def rec(t): + nonlocal best + if t == v: + size, _, _ = cert_witness(dec, labels) + if size > best: + best = size + return + for opt in options[t]: + labels[t] = opt + rec(t + 1) + + rec(0) + return best + + +# ---------------------------------------------------------------- Side A: pairing cost + +def cost_B(dec, B): + """sum_j rank_F2 B[R_j, A_j]. B is a list of row bitmasks over columns.""" + total = 0 + for j in range(T): + rows = [] + A_list = sorted(dec.A[j]) + colbit = {s: 1 << i for i, s in enumerate(A_list)} + for t in sorted(dec.R[j]): + row = 0 + for s in A_list: + if (B[t] >> s) & 1: + row |= colbit[s] + rows.append(row) + total += f2_rank(rows, len(A_list)) + return total + + +def pairing_ok(dec, B): + for t in range(dec.v): + if ((B[t] >> t) & 1) != 1: + return False + for s in range(dec.v): + if s != t and ((B[t] >> s) & 1) and not dec.zero[t][s]: + return False + return True + + +def min_cost_pairing(dec, exhaustive_limit=10, budget=300, seed=0): + """Minimum cost over admissible B: 0/1, unit diagonal, ones only at incidences. + + Exhaustive over all such B when the admissible pair count is small; + deterministic single-bit local search otherwise. Returns + (min_cost, B, exact) where exact says the exhaustive minimum was proved. + """ + v = dec.v + # Admissible B: 0/1, unit diagonal, B_ts = 1 only where M_ts = 0 (s != t). + # The source lemma's chain cert(M) <= sum_j rank_F2 B[R_j, A_j] uses only + # these two properties, so asymmetric B are included (stronger upper bound). + pairs = [(t, s) for t in range(v) for s in range(v) + if s != t and dec.zero[t][s]] + base = [1 << t for t in range(v)] # B = identity + + def apply(mask): + B = list(base) + for i, (t, s) in enumerate(pairs): + if (mask >> i) & 1: + B[t] |= 1 << s + return B + + if len(pairs) <= exhaustive_limit: + best = None + bestB = None + for mask in range(1 << len(pairs)): + B = apply(mask) + c = cost_B(dec, B) + if best is None or c < best: + best, bestB = c, B + return best, bestB, True + + rng = random.Random(seed) + best = cost_B(dec, base) + bestB = list(base) + bestmask = 0 + evals = 1 + improved = True + while improved and evals < budget: + improved = False + for i in range(len(pairs)): + cand = bestmask ^ (1 << i) + B = apply(cand) + c = cost_B(dec, B) + evals += 1 + if c < best: + best, bestB, bestmask = c, B, cand + improved = True + for _ in range(2): + if evals >= budget: + break + cand = bestmask ^ (1 << rng.randrange(len(pairs))) + B = apply(cand) + c = cost_B(dec, B) + evals += 1 + if c < best: + best, bestB, bestmask = c, B, cand + return best, bestB, False + + +# ---------------------------------------------------------------- families + +def draw_entries(rng, v, alphabet): + P = [[rng.choice(alphabet) for _ in range(v)] for _ in range(T)] + Q = [[rng.choice(alphabet) for _ in range(v)] for _ in range(T)] + return P, Q + + +def make_instance(family, v, seed): + """Build a decoder with M_tt != 0 on every line; deterministic in seed.""" + rng = random.Random(seed) + for _attempt in range(2000): + if family == "dense": + P, Q = draw_entries(rng, v, [-2, -1, 0, 1, 2]) + elif family == "config": + P, Q = draw_entries(rng, v, [-1, 0, 1]) + elif family == "tied": + # Products p_j(t) q_j(t) from a 2-adic-weighted alphabet; retained + # only when tied minimal valuations cover at least half the lines, + # the obstruction named in the source package's section 7. + P, Q = draw_entries(rng, v, [-2, -1, 1, 2, 4]) + else: + raise ValueError(family) + dec = Decoder(v, P, Q) + if dec.diag_ok and (family != "tied" or tied_score(dec) >= (v + 1) // 2): + return dec + raise RuntimeError("no instance with nonzero diagonal") + + +def tied_score(dec): + """Number of lines whose minimal 2-adic valuation among products is attained twice or more.""" + def v2(x): + if x == 0: + return 99 + k = 0 + while x % 2 == 0: + x //= 2 + k += 1 + return k + + count = 0 + for t in range(dec.v): + vals = [v2(dec.P[j][t] * dec.Q[j][t]) for j in range(T)] + m = min(vals) + if vals.count(m) >= 2: + count += 1 + return count + + +# ---------------------------------------------------------------- census + +FAMILIES = ("dense", "config", "tied") + + +def run_census(): + records = [] + for family in FAMILIES: + for v in range(4, 13): + n = 10 if v <= 8 else 5 + if family == "tied": + n = 8 if v <= 8 else 4 + for i in range(n): + seed = 20261015 + 1000 * FAMILIES.index(family) + 17 * v + i + dec = make_instance(family, v, seed) + thr = threshold(v) + size, labels, subset, order, evals = search_labels( + dec, budget=150, seed=seed + 1) + assert witness_ok(dec, labels, subset, order), "search produced an invalid witness" + minc, B, exact = min_cost_pairing( + dec, exhaustive_limit=10, budget=300, seed=seed + 2) + assert pairing_ok(dec, B) + # Proven chain: witness size <= cost(B) for every admissible B. + assert size <= cost_B(dec, B), "proven chain violated" + if exact: + assert size <= minc, "proven chain violated" + records.append({ + "family": family, "v": v, "seed": seed, "threshold": thr, + "witness": size, "min_cost_upper": minc, "min_cost_exact": exact, + "tied_lines": tied_score(dec), + "zero_pairs": sum(dec.zero[t][s] for t in range(v) for s in range(v) if s != t), + "evals": evals, + "falsifier": minc < thr, "resolved": size >= thr, + }) + return records + + +def run_controls(): + out = {} + # C1: tiny-domain brute force cross-checks the search engine exactly. + brute_cases = [] + for k, (family, v) in enumerate((("dense", 3), ("config", 3), ("tied", 3))): + dec = make_instance(family, v, 777 + k) + exact = brute_cert(dec) + size, labels, subset, order, _ = search_labels(dec, budget=200, seed=900 + k) + assert witness_ok(dec, labels, subset, order) + brute_cases.append({"family": family, "v": v, "brute": exact, "search": size}) + assert size == exact, "search engine missed the exact cert on a tiny instance" + out["bruteforce_crosscheck"] = brute_cases + + # C2: a corrupted witness must be rejected. + dec = make_instance("config", 5, 4242) + size, labels, subset, order, _ = search_labels(dec, budget=150, seed=1) + assert witness_ok(dec, labels, subset, order) + bad = list(labels) + t0 = order[0] + bad[t0] = (0, 0) # breaks K_tt = 1 + assert not witness_ok(dec, bad, subset, order), "corrupted witness was accepted" + # A binding pair (K_ts = 1 at an incidence) must reject any order with t before s. + binding = None + for t in subset: + for s in subset: + if s != t and dec.zero[t][s] and kval(labels[t][0], labels[s][1]) == 1: + binding = (t, s) + break + if binding: + break + order_rejected = False + if binding: + t, s = binding + flipped = [t] + [x for x in order if x not in (t, s)] + [s] # forces t before s at a binding pair + if not witness_ok(dec, labels, subset, flipped): + order_rejected = True + out["corrupted_witness_rejected"] = True + out["binding_pair_order_rejected"] = order_rejected + + # C3: threshold table by hand for v = 4..12 (floor(2v/3)). + table = {v: (2 * v) // 3 for v in range(4, 13)} + assert table == {4: 2, 5: 3, 6: 4, 7: 4, 8: 5, 9: 6, 10: 6, 11: 7, 12: 8} + out["threshold_table"] = table + + # C4: hand-checkable diagonal decoder: p_j = q_j = e_j on three lines. + P = [[1, 0, 0], [0, 1, 0], [0, 0, 1]] + dec = Decoder(3, P, [list(r) for r in P]) + assert dec.diag_ok and all(dec.M[t][s] == (1 if t == s else 0) for t in range(3) for s in range(3)) + exact = brute_cert(dec) + assert exact == 3 + out["diagonal_control_cert"] = exact + + # C5: the proven chain cert <= cost(B) on a known instance, both sides exact. + dec = make_instance("dense", 4, 31337) + exact = brute_cert(dec) + minc, B, is_exact = min_cost_pairing(dec, exhaustive_limit=6) + assert pairing_ok(dec, B) + assert exact <= minc + out["chain_control"] = {"brute_cert": exact, "min_cost": minc, "min_cost_exact": is_exact} + return out + + +def main(): + sys.stdout.reconfigure(encoding="utf-8") + controls = run_controls() + records = run_census() + total = len(records) + falsifiers = [r for r in records if r["falsifier"]] + unresolved = [r for r in records if not r["resolved"] and not r["falsifier"]] + resolved = [r for r in records if r["resolved"]] + min_ratio = min(r["witness"] / r["v"] for r in records) + worst = min(records, key=lambda r: (r["witness"] / r["v"], r["v"])) + by_family = {} + for fam in FAMILIES: + rows = [r for r in records if r["family"] == fam] + by_family[fam] = { + "instances": len(rows), + "resolved": sum(1 for r in rows if r["resolved"]), + "min_witness_ratio": min(r["witness"] / r["v"] for r in rows), + "max_tied_lines": max(r["tied_lines"] for r in rows), + } + cert = { + "schema_version": 1, + "claim": "F-star: cert(M) >= floor(2v/3) for exact 3-total rational decoders", + "source": "research/root-unit-decoder-lemmas/README.md section 7 (OPEN)", + "domain": {"v": "4..12", "totals": 3, "factor_entries": "-2..2", + "families": list(FAMILIES), "seeds": "20261015 + 1000*family_index + 17*v + i"}, + "instances": total, + "resolved_witness": len(resolved), + "falsifiers": len(falsifiers), + "unresolved": len(unresolved), + "min_witness_ratio": min_ratio, + "worst_instance": worst, + "by_family": by_family, + "controls": controls, + "outcome": "SCOPED_NEGATIVE_NO_FALSIFIER" if not falsifiers and not unresolved + else ("FALSIFIER_FOUND" if falsifiers else "UNRESOLVED_INSTANCES"), + "no_new_kappa": True, + } + digest = hashlib.sha256(json.dumps(records, sort_keys=True).encode()).hexdigest() + cert["census_digest"] = digest + (HERE / "CERTIFICATE.json").write_text(json.dumps(cert, indent=2, sort_keys=True) + "\n", + encoding="utf-8") + (HERE / "CENSUS-RECORDS.json").write_text(json.dumps(records, indent=2, sort_keys=True) + "\n", + encoding="utf-8") + print("PASS_FSTAR_CERT_CENSUS instances=%d resolved=%d falsifiers=%d unresolved=%d " + "min_ratio=%.4f digest=%s" % (total, len(resolved), len(falsifiers), len(unresolved), + min_ratio, digest[:16])) + print("PASS_FSTAR_CERT_CONTROLS bruteforce=%d diagonal_cert=%d chain_cert=%d" + % (len(controls["bruteforce_crosscheck"]), controls["diagonal_control_cert"], + controls["chain_control"]["brute_cert"])) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main())