diff --git a/research/dirty-fanout-cut-certificate/BENCHMARK.json b/research/dirty-fanout-cut-certificate/BENCHMARK.json new file mode 100644 index 0000000000..be253cf32a --- /dev/null +++ b/research/dirty-fanout-cut-certificate/BENCHMARK.json @@ -0,0 +1,26 @@ +{ + "enumerated_forests": 16807, + "median_seconds": { + "compiler_and_checker": 0.0006839910056442022, + "enumeration": 0.049754062994907144 + }, + "optimum": "49", + "platform": "Linux-7.2.8-200.fc44.x86_64-x86_64-with-glibc2.43", + "python": "3.12.14", + "rows": 6, + "scope": "New exhaustive forest baseline versus new compiler plus full certificate checker; not physical runtime.", + "seconds": { + "compiler_and_checker": [ + 0.0009310570021625608, + 0.0006776990048820153, + 0.0006839910056442022 + ], + "enumeration": [ + 0.04990035000082571, + 0.049754062994907144, + 0.048841502000868786 + ] + }, + "seed": 19, + "tariffs_sha256": "fc81a077041b75d182d3374eb979bc8b83c5070f103d2553d044ce84ceb10a02" +} diff --git a/research/dirty-fanout-cut-certificate/CERTIFICATES.json b/research/dirty-fanout-cut-certificate/CERTIFICATES.json new file mode 100644 index 0000000000..51338ef4c4 --- /dev/null +++ b/research/dirty-fanout-cut-certificate/CERTIFICATES.json @@ -0,0 +1 @@ +{"chain":{"cost":"5","cuts":[{"price":"1","rows":[0]},{"price":"2","rows":[1]},{"price":"2","rows":[2]}],"parents":[null,0,1],"q":3,"schema_version":1,"word":[["ADD",2,1],["ADD",1,0],["P",0],["ADD",1,0],["ADD",2,1]]},"cheap_cycle":{"cost":"103","cuts":[{"price":"1","rows":[0]},{"price":"2","rows":[1]},{"price":"2","rows":[2]},{"price":"98","rows":[1,2]}],"parents":[null,null,1],"q":3,"schema_version":1,"word":[["ADD",2,1],["P",0],["P",1],["ADD",2,1]]},"hierarchy_112":{"cost":"1539","cuts":[{"price":"1","rows":[0]},{"price":"8","rows":[1]},{"price":"4","rows":[2]},{"price":"4","rows":[3]},{"price":"6","rows":[2,3]},{"price":"6","rows":[4]},{"price":"6","rows":[5]},{"price":"4","rows":[4,5]},{"price":"8","rows":[6]},{"price":"8","rows":[7]},{"price":"2","rows":[6,7]},{"price":"10","rows":[4,5,6,7]},{"price":"4","rows":[8]},{"price":"4","rows":[9]},{"price":"6","rows":[8,9]},{"price":"6","rows":[10]},{"price":"6","rows":[11]},{"price":"4","rows":[10,11]},{"price":"10","rows":[8,9,10,11]},{"price":"8","rows":[12]},{"price":"8","rows":[13]},{"price":"2","rows":[12,13]},{"price":"4","rows":[14]},{"price":"4","rows":[15]},{"price":"6","rows":[14,15]},{"price":"10","rows":[12,13,14,15]},{"price":"14","rows":[8,9,10,11,12,13,14,15]},{"price":"6","rows":[16]},{"price":"6","rows":[17]},{"price":"4","rows":[16,17]},{"price":"8","rows":[18]},{"price":"8","rows":[19]},{"price":"2","rows":[18,19]},{"price":"10","rows":[16,17,18,19]},{"price":"4","rows":[20]},{"price":"4","rows":[21]},{"price":"6","rows":[20,21]},{"price":"6","rows":[22]},{"price":"6","rows":[23]},{"price":"4","rows":[22,23]},{"price":"10","rows":[20,21,22,23]},{"price":"14","rows":[16,17,18,19,20,21,22,23]},{"price":"8","rows":[24]},{"price":"8","rows":[25]},{"price":"2","rows":[24,25]},{"price":"4","rows":[26]},{"price":"4","rows":[27]},{"price":"6","rows":[26,27]},{"price":"10","rows":[24,25,26,27]},{"price":"6","rows":[28]},{"price":"6","rows":[29]},{"price":"4","rows":[28,29]},{"price":"8","rows":[30]},{"price":"8","rows":[31]},{"price":"2","rows":[30,31]},{"price":"10","rows":[28,29,30,31]},{"price":"14","rows":[24,25,26,27,28,29,30,31]},{"price":"18","rows":[16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31]},{"price":"4","rows":[32]},{"price":"4","rows":[33]},{"price":"6","rows":[32,33]},{"price":"6","rows":[34]},{"price":"6","rows":[35]},{"price":"4","rows":[34,35]},{"price":"10","rows":[32,33,34,35]},{"price":"8","rows":[36]},{"price":"8","rows":[37]},{"price":"2","rows":[36,37]},{"price":"4","rows":[38]},{"price":"4","rows":[39]},{"price":"6","rows":[38,39]},{"price":"10","rows":[36,37,38,39]},{"price":"14","rows":[32,33,34,35,36,37,38,39]},{"price":"6","rows":[40]},{"price":"6","rows":[41]},{"price":"4","rows":[40,41]},{"price":"8","rows":[42]},{"price":"8","rows":[43]},{"price":"2","rows":[42,43]},{"price":"10","rows":[40,41,42,43]},{"price":"4","rows":[44]},{"price":"4","rows":[45]},{"price":"6","rows":[44,45]},{"price":"6","rows":[46]},{"price":"6","rows":[47]},{"price":"4","rows":[46,47]},{"price":"10","rows":[44,45,46,47]},{"price":"14","rows":[40,41,42,43,44,45,46,47]},{"price":"18","rows":[32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47]},{"price":"8","rows":[48]},{"price":"8","rows":[49]},{"price":"2","rows":[48,49]},{"price":"4","rows":[50]},{"price":"4","rows":[51]},{"price":"6","rows":[50,51]},{"price":"10","rows":[48,49,50,51]},{"price":"6","rows":[52]},{"price":"6","rows":[53]},{"price":"4","rows":[52,53]},{"price":"8","rows":[54]},{"price":"8","rows":[55]},{"price":"2","rows":[54,55]},{"price":"10","rows":[52,53,54,55]},{"price":"14","rows":[48,49,50,51,52,53,54,55]},{"price":"4","rows":[56]},{"price":"4","rows":[57]},{"price":"6","rows":[56,57]},{"price":"6","rows":[58]},{"price":"6","rows":[59]},{"price":"4","rows":[58,59]},{"price":"10","rows":[56,57,58,59]},{"price":"8","rows":[60]},{"price":"8","rows":[61]},{"price":"2","rows":[60,61]},{"price":"4","rows":[62]},{"price":"4","rows":[63]},{"price":"6","rows":[62,63]},{"price":"10","rows":[60,61,62,63]},{"price":"14","rows":[56,57,58,59,60,61,62,63]},{"price":"18","rows":[48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63]},{"price":"22","rows":[32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63]},{"price":"6","rows":[64]},{"price":"6","rows":[65]},{"price":"4","rows":[64,65]},{"price":"8","rows":[66]},{"price":"8","rows":[67]},{"price":"2","rows":[66,67]},{"price":"10","rows":[64,65,66,67]},{"price":"4","rows":[68]},{"price":"4","rows":[69]},{"price":"6","rows":[68,69]},{"price":"6","rows":[70]},{"price":"6","rows":[71]},{"price":"4","rows":[70,71]},{"price":"10","rows":[68,69,70,71]},{"price":"14","rows":[64,65,66,67,68,69,70,71]},{"price":"8","rows":[72]},{"price":"8","rows":[73]},{"price":"2","rows":[72,73]},{"price":"4","rows":[74]},{"price":"4","rows":[75]},{"price":"6","rows":[74,75]},{"price":"10","rows":[72,73,74,75]},{"price":"6","rows":[76]},{"price":"6","rows":[77]},{"price":"4","rows":[76,77]},{"price":"8","rows":[78]},{"price":"8","rows":[79]},{"price":"2","rows":[78,79]},{"price":"10","rows":[76,77,78,79]},{"price":"14","rows":[72,73,74,75,76,77,78,79]},{"price":"18","rows":[64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79]},{"price":"4","rows":[80]},{"price":"4","rows":[81]},{"price":"6","rows":[80,81]},{"price":"6","rows":[82]},{"price":"6","rows":[83]},{"price":"4","rows":[82,83]},{"price":"10","rows":[80,81,82,83]},{"price":"8","rows":[84]},{"price":"8","rows":[85]},{"price":"2","rows":[84,85]},{"price":"4","rows":[86]},{"price":"4","rows":[87]},{"price":"6","rows":[86,87]},{"price":"10","rows":[84,85,86,87]},{"price":"14","rows":[80,81,82,83,84,85,86,87]},{"price":"6","rows":[88]},{"price":"6","rows":[89]},{"price":"4","rows":[88,89]},{"price":"8","rows":[90]},{"price":"8","rows":[91]},{"price":"2","rows":[90,91]},{"price":"10","rows":[88,89,90,91]},{"price":"4","rows":[92]},{"price":"4","rows":[93]},{"price":"6","rows":[92,93]},{"price":"6","rows":[94]},{"price":"6","rows":[95]},{"price":"4","rows":[94,95]},{"price":"10","rows":[92,93,94,95]},{"price":"14","rows":[88,89,90,91,92,93,94,95]},{"price":"18","rows":[80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95]},{"price":"22","rows":[64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95]},{"price":"8","rows":[96]},{"price":"8","rows":[97]},{"price":"2","rows":[96,97]},{"price":"4","rows":[98]},{"price":"4","rows":[99]},{"price":"6","rows":[98,99]},{"price":"10","rows":[96,97,98,99]},{"price":"6","rows":[100]},{"price":"6","rows":[101]},{"price":"4","rows":[100,101]},{"price":"8","rows":[102]},{"price":"8","rows":[103]},{"price":"2","rows":[102,103]},{"price":"10","rows":[100,101,102,103]},{"price":"14","rows":[96,97,98,99,100,101,102,103]},{"price":"4","rows":[104]},{"price":"4","rows":[105]},{"price":"6","rows":[104,105]},{"price":"6","rows":[106]},{"price":"6","rows":[107]},{"price":"4","rows":[106,107]},{"price":"10","rows":[104,105,106,107]},{"price":"8","rows":[108]},{"price":"8","rows":[109]},{"price":"2","rows":[108,109]},{"price":"4","rows":[110]},{"price":"4","rows":[111]},{"price":"6","rows":[110,111]},{"price":"10","rows":[108,109,110,111]},{"price":"14","rows":[104,105,106,107,108,109,110,111]},{"price":"40","rows":[96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111]},{"price":"26","rows":[64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111]}],"parents":[null,0,0,2,5,0,7,4,0,8,11,9,8,12,12,14,17,0,19,16,21,23,16,22,25,16,24,26,29,24,31,28,0,32,35,33,32,36,36,38,41,42,32,42,45,47,40,46,32,48,48,50,53,48,55,52,48,56,59,57,56,60,60,62,65,0,67,64,69,71,64,70,73,64,72,74,77,72,79,76,81,83,64,82,80,84,84,86,89,90,80,90,93,95,88,94,97,64,96,98,101,96,103,100,96,104,107,105,104,108,108,110],"q":112,"schema_version":1,"word":[["ADD",1,0],["ADD",3,2],["ADD",2,0],["ADD",6,7],["ADD",7,4],["ADD",4,5],["ADD",5,0],["ADD",10,11],["ADD",11,9],["ADD",9,8],["ADD",13,12],["ADD",15,14],["ADD",14,12],["ADD",12,8],["ADD",8,0],["ADD",18,19],["ADD",19,16],["ADD",20,21],["ADD",21,23],["ADD",23,22],["ADD",22,16],["ADD",27,26],["ADD",26,24],["ADD",30,31],["ADD",31,28],["ADD",28,29],["ADD",29,24],["ADD",24,25],["ADD",25,16],["ADD",16,17],["ADD",17,0],["ADD",34,35],["ADD",35,33],["ADD",33,32],["ADD",37,36],["ADD",39,38],["ADD",38,36],["ADD",36,32],["ADD",44,45],["ADD",45,47],["ADD",47,46],["ADD",46,40],["ADD",40,41],["ADD",41,42],["ADD",43,42],["ADD",42,32],["ADD",49,48],["ADD",51,50],["ADD",50,48],["ADD",54,55],["ADD",55,52],["ADD",52,53],["ADD",53,48],["ADD",58,59],["ADD",59,57],["ADD",57,56],["ADD",61,60],["ADD",63,62],["ADD",62,60],["ADD",60,56],["ADD",56,48],["ADD",48,32],["ADD",32,0],["ADD",66,67],["ADD",67,64],["ADD",68,69],["ADD",69,71],["ADD",71,70],["ADD",70,64],["ADD",75,74],["ADD",74,72],["ADD",78,79],["ADD",79,76],["ADD",76,77],["ADD",77,72],["ADD",72,73],["ADD",73,64],["ADD",85,84],["ADD",87,86],["ADD",86,84],["ADD",84,80],["ADD",92,93],["ADD",93,95],["ADD",95,94],["ADD",94,88],["ADD",88,89],["ADD",89,90],["ADD",91,90],["ADD",90,80],["ADD",80,81],["ADD",81,83],["ADD",83,82],["ADD",82,64],["ADD",99,98],["ADD",98,96],["ADD",102,103],["ADD",103,100],["ADD",100,101],["ADD",101,96],["ADD",106,107],["ADD",107,105],["ADD",105,104],["ADD",109,108],["ADD",111,110],["ADD",110,108],["ADD",108,104],["ADD",104,96],["ADD",96,97],["ADD",97,64],["ADD",64,65],["ADD",65,0],["P",0],["ADD",65,0],["ADD",64,65],["ADD",97,64],["ADD",96,97],["ADD",104,96],["ADD",108,104],["ADD",110,108],["ADD",111,110],["ADD",109,108],["ADD",105,104],["ADD",107,105],["ADD",106,107],["ADD",101,96],["ADD",100,101],["ADD",103,100],["ADD",102,103],["ADD",98,96],["ADD",99,98],["ADD",82,64],["ADD",83,82],["ADD",81,83],["ADD",80,81],["ADD",90,80],["ADD",91,90],["ADD",89,90],["ADD",88,89],["ADD",94,88],["ADD",95,94],["ADD",93,95],["ADD",92,93],["ADD",84,80],["ADD",86,84],["ADD",87,86],["ADD",85,84],["ADD",73,64],["ADD",72,73],["ADD",77,72],["ADD",76,77],["ADD",79,76],["ADD",78,79],["ADD",74,72],["ADD",75,74],["ADD",70,64],["ADD",71,70],["ADD",69,71],["ADD",68,69],["ADD",67,64],["ADD",66,67],["ADD",32,0],["ADD",48,32],["ADD",56,48],["ADD",60,56],["ADD",62,60],["ADD",63,62],["ADD",61,60],["ADD",57,56],["ADD",59,57],["ADD",58,59],["ADD",53,48],["ADD",52,53],["ADD",55,52],["ADD",54,55],["ADD",50,48],["ADD",51,50],["ADD",49,48],["ADD",42,32],["ADD",43,42],["ADD",41,42],["ADD",40,41],["ADD",46,40],["ADD",47,46],["ADD",45,47],["ADD",44,45],["ADD",36,32],["ADD",38,36],["ADD",39,38],["ADD",37,36],["ADD",33,32],["ADD",35,33],["ADD",34,35],["ADD",17,0],["ADD",16,17],["ADD",25,16],["ADD",24,25],["ADD",29,24],["ADD",28,29],["ADD",31,28],["ADD",30,31],["ADD",26,24],["ADD",27,26],["ADD",22,16],["ADD",23,22],["ADD",21,23],["ADD",20,21],["ADD",19,16],["ADD",18,19],["ADD",8,0],["ADD",12,8],["ADD",14,12],["ADD",15,14],["ADD",13,12],["ADD",9,8],["ADD",11,9],["ADD",10,11],["ADD",5,0],["ADD",4,5],["ADD",7,4],["ADD",6,7],["ADD",2,0],["ADD",3,2],["ADD",1,0]]},"hierarchy_16":{"cost":"163","cuts":[{"price":"1","rows":[0]},{"price":"8","rows":[1]},{"price":"4","rows":[2]},{"price":"4","rows":[3]},{"price":"6","rows":[2,3]},{"price":"6","rows":[4]},{"price":"6","rows":[5]},{"price":"4","rows":[4,5]},{"price":"8","rows":[6]},{"price":"8","rows":[7]},{"price":"2","rows":[6,7]},{"price":"10","rows":[4,5,6,7]},{"price":"4","rows":[8]},{"price":"4","rows":[9]},{"price":"6","rows":[8,9]},{"price":"6","rows":[10]},{"price":"6","rows":[11]},{"price":"4","rows":[10,11]},{"price":"10","rows":[8,9,10,11]},{"price":"8","rows":[12]},{"price":"8","rows":[13]},{"price":"2","rows":[12,13]},{"price":"4","rows":[14]},{"price":"4","rows":[15]},{"price":"6","rows":[14,15]},{"price":"10","rows":[12,13,14,15]},{"price":"14","rows":[8,9,10,11,12,13,14,15]}],"parents":[null,0,0,2,5,0,7,4,0,8,11,9,8,12,12,14],"q":16,"schema_version":1,"word":[["ADD",1,0],["ADD",3,2],["ADD",2,0],["ADD",6,7],["ADD",7,4],["ADD",4,5],["ADD",5,0],["ADD",10,11],["ADD",11,9],["ADD",9,8],["ADD",13,12],["ADD",15,14],["ADD",14,12],["ADD",12,8],["ADD",8,0],["P",0],["ADD",8,0],["ADD",12,8],["ADD",14,12],["ADD",15,14],["ADD",13,12],["ADD",9,8],["ADD",11,9],["ADD",10,11],["ADD",5,0],["ADD",4,5],["ADD",7,4],["ADD",6,7],["ADD",2,0],["ADD",3,2],["ADD",1,0]]},"hierarchy_31":{"cost":"371","cuts":[{"price":"1","rows":[0]},{"price":"8","rows":[1]},{"price":"4","rows":[2]},{"price":"4","rows":[3]},{"price":"6","rows":[2,3]},{"price":"6","rows":[4]},{"price":"6","rows":[5]},{"price":"4","rows":[4,5]},{"price":"8","rows":[6]},{"price":"8","rows":[7]},{"price":"2","rows":[6,7]},{"price":"10","rows":[4,5,6,7]},{"price":"4","rows":[8]},{"price":"4","rows":[9]},{"price":"6","rows":[8,9]},{"price":"6","rows":[10]},{"price":"6","rows":[11]},{"price":"4","rows":[10,11]},{"price":"10","rows":[8,9,10,11]},{"price":"8","rows":[12]},{"price":"8","rows":[13]},{"price":"2","rows":[12,13]},{"price":"4","rows":[14]},{"price":"4","rows":[15]},{"price":"6","rows":[14,15]},{"price":"10","rows":[12,13,14,15]},{"price":"14","rows":[8,9,10,11,12,13,14,15]},{"price":"6","rows":[16]},{"price":"6","rows":[17]},{"price":"4","rows":[16,17]},{"price":"8","rows":[18]},{"price":"8","rows":[19]},{"price":"2","rows":[18,19]},{"price":"10","rows":[16,17,18,19]},{"price":"4","rows":[20]},{"price":"4","rows":[21]},{"price":"6","rows":[20,21]},{"price":"6","rows":[22]},{"price":"6","rows":[23]},{"price":"4","rows":[22,23]},{"price":"10","rows":[20,21,22,23]},{"price":"14","rows":[16,17,18,19,20,21,22,23]},{"price":"8","rows":[24]},{"price":"8","rows":[25]},{"price":"2","rows":[24,25]},{"price":"4","rows":[26]},{"price":"4","rows":[27]},{"price":"6","rows":[26,27]},{"price":"10","rows":[24,25,26,27]},{"price":"6","rows":[28]},{"price":"6","rows":[29]},{"price":"4","rows":[28,29]},{"price":"10","rows":[30]},{"price":"10","rows":[28,29,30]},{"price":"14","rows":[24,25,26,27,28,29,30]},{"price":"18","rows":[16,17,18,19,20,21,22,23,24,25,26,27,28,29,30]}],"parents":[null,0,0,2,5,0,7,4,0,8,11,9,8,12,12,14,17,0,19,16,21,23,16,22,25,16,24,26,29,24,29],"q":31,"schema_version":1,"word":[["ADD",1,0],["ADD",3,2],["ADD",2,0],["ADD",6,7],["ADD",7,4],["ADD",4,5],["ADD",5,0],["ADD",10,11],["ADD",11,9],["ADD",9,8],["ADD",13,12],["ADD",15,14],["ADD",14,12],["ADD",12,8],["ADD",8,0],["ADD",18,19],["ADD",19,16],["ADD",20,21],["ADD",21,23],["ADD",23,22],["ADD",22,16],["ADD",27,26],["ADD",26,24],["ADD",28,29],["ADD",30,29],["ADD",29,24],["ADD",24,25],["ADD",25,16],["ADD",16,17],["ADD",17,0],["P",0],["ADD",17,0],["ADD",16,17],["ADD",25,16],["ADD",24,25],["ADD",29,24],["ADD",30,29],["ADD",28,29],["ADD",26,24],["ADD",27,26],["ADD",22,16],["ADD",23,22],["ADD",21,23],["ADD",20,21],["ADD",19,16],["ADD",18,19],["ADD",8,0],["ADD",12,8],["ADD",14,12],["ADD",15,14],["ADD",13,12],["ADD",9,8],["ADD",11,9],["ADD",10,11],["ADD",5,0],["ADD",4,5],["ADD",7,4],["ADD",6,7],["ADD",2,0],["ADD",3,2],["ADD",1,0]]},"hierarchy_64":{"cost":"827","cuts":[{"price":"1","rows":[0]},{"price":"8","rows":[1]},{"price":"4","rows":[2]},{"price":"4","rows":[3]},{"price":"6","rows":[2,3]},{"price":"6","rows":[4]},{"price":"6","rows":[5]},{"price":"4","rows":[4,5]},{"price":"8","rows":[6]},{"price":"8","rows":[7]},{"price":"2","rows":[6,7]},{"price":"10","rows":[4,5,6,7]},{"price":"4","rows":[8]},{"price":"4","rows":[9]},{"price":"6","rows":[8,9]},{"price":"6","rows":[10]},{"price":"6","rows":[11]},{"price":"4","rows":[10,11]},{"price":"10","rows":[8,9,10,11]},{"price":"8","rows":[12]},{"price":"8","rows":[13]},{"price":"2","rows":[12,13]},{"price":"4","rows":[14]},{"price":"4","rows":[15]},{"price":"6","rows":[14,15]},{"price":"10","rows":[12,13,14,15]},{"price":"14","rows":[8,9,10,11,12,13,14,15]},{"price":"6","rows":[16]},{"price":"6","rows":[17]},{"price":"4","rows":[16,17]},{"price":"8","rows":[18]},{"price":"8","rows":[19]},{"price":"2","rows":[18,19]},{"price":"10","rows":[16,17,18,19]},{"price":"4","rows":[20]},{"price":"4","rows":[21]},{"price":"6","rows":[20,21]},{"price":"6","rows":[22]},{"price":"6","rows":[23]},{"price":"4","rows":[22,23]},{"price":"10","rows":[20,21,22,23]},{"price":"14","rows":[16,17,18,19,20,21,22,23]},{"price":"8","rows":[24]},{"price":"8","rows":[25]},{"price":"2","rows":[24,25]},{"price":"4","rows":[26]},{"price":"4","rows":[27]},{"price":"6","rows":[26,27]},{"price":"10","rows":[24,25,26,27]},{"price":"6","rows":[28]},{"price":"6","rows":[29]},{"price":"4","rows":[28,29]},{"price":"8","rows":[30]},{"price":"8","rows":[31]},{"price":"2","rows":[30,31]},{"price":"10","rows":[28,29,30,31]},{"price":"14","rows":[24,25,26,27,28,29,30,31]},{"price":"18","rows":[16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31]},{"price":"4","rows":[32]},{"price":"4","rows":[33]},{"price":"6","rows":[32,33]},{"price":"6","rows":[34]},{"price":"6","rows":[35]},{"price":"4","rows":[34,35]},{"price":"10","rows":[32,33,34,35]},{"price":"8","rows":[36]},{"price":"8","rows":[37]},{"price":"2","rows":[36,37]},{"price":"4","rows":[38]},{"price":"4","rows":[39]},{"price":"6","rows":[38,39]},{"price":"10","rows":[36,37,38,39]},{"price":"14","rows":[32,33,34,35,36,37,38,39]},{"price":"6","rows":[40]},{"price":"6","rows":[41]},{"price":"4","rows":[40,41]},{"price":"8","rows":[42]},{"price":"8","rows":[43]},{"price":"2","rows":[42,43]},{"price":"10","rows":[40,41,42,43]},{"price":"4","rows":[44]},{"price":"4","rows":[45]},{"price":"6","rows":[44,45]},{"price":"6","rows":[46]},{"price":"6","rows":[47]},{"price":"4","rows":[46,47]},{"price":"10","rows":[44,45,46,47]},{"price":"14","rows":[40,41,42,43,44,45,46,47]},{"price":"18","rows":[32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47]},{"price":"8","rows":[48]},{"price":"8","rows":[49]},{"price":"2","rows":[48,49]},{"price":"4","rows":[50]},{"price":"4","rows":[51]},{"price":"6","rows":[50,51]},{"price":"10","rows":[48,49,50,51]},{"price":"6","rows":[52]},{"price":"6","rows":[53]},{"price":"4","rows":[52,53]},{"price":"8","rows":[54]},{"price":"8","rows":[55]},{"price":"2","rows":[54,55]},{"price":"10","rows":[52,53,54,55]},{"price":"14","rows":[48,49,50,51,52,53,54,55]},{"price":"4","rows":[56]},{"price":"4","rows":[57]},{"price":"6","rows":[56,57]},{"price":"6","rows":[58]},{"price":"6","rows":[59]},{"price":"4","rows":[58,59]},{"price":"10","rows":[56,57,58,59]},{"price":"8","rows":[60]},{"price":"8","rows":[61]},{"price":"2","rows":[60,61]},{"price":"4","rows":[62]},{"price":"4","rows":[63]},{"price":"6","rows":[62,63]},{"price":"10","rows":[60,61,62,63]},{"price":"14","rows":[56,57,58,59,60,61,62,63]},{"price":"18","rows":[48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63]},{"price":"22","rows":[32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63]}],"parents":[null,0,0,2,5,0,7,4,0,8,11,9,8,12,12,14,17,0,19,16,21,23,16,22,25,16,24,26,29,24,31,28,0,32,35,33,32,36,36,38,41,42,32,42,45,47,40,46,32,48,48,50,53,48,55,52,48,56,59,57,56,60,60,62],"q":64,"schema_version":1,"word":[["ADD",1,0],["ADD",3,2],["ADD",2,0],["ADD",6,7],["ADD",7,4],["ADD",4,5],["ADD",5,0],["ADD",10,11],["ADD",11,9],["ADD",9,8],["ADD",13,12],["ADD",15,14],["ADD",14,12],["ADD",12,8],["ADD",8,0],["ADD",18,19],["ADD",19,16],["ADD",20,21],["ADD",21,23],["ADD",23,22],["ADD",22,16],["ADD",27,26],["ADD",26,24],["ADD",30,31],["ADD",31,28],["ADD",28,29],["ADD",29,24],["ADD",24,25],["ADD",25,16],["ADD",16,17],["ADD",17,0],["ADD",34,35],["ADD",35,33],["ADD",33,32],["ADD",37,36],["ADD",39,38],["ADD",38,36],["ADD",36,32],["ADD",44,45],["ADD",45,47],["ADD",47,46],["ADD",46,40],["ADD",40,41],["ADD",41,42],["ADD",43,42],["ADD",42,32],["ADD",49,48],["ADD",51,50],["ADD",50,48],["ADD",54,55],["ADD",55,52],["ADD",52,53],["ADD",53,48],["ADD",58,59],["ADD",59,57],["ADD",57,56],["ADD",61,60],["ADD",63,62],["ADD",62,60],["ADD",60,56],["ADD",56,48],["ADD",48,32],["ADD",32,0],["P",0],["ADD",32,0],["ADD",48,32],["ADD",56,48],["ADD",60,56],["ADD",62,60],["ADD",63,62],["ADD",61,60],["ADD",57,56],["ADD",59,57],["ADD",58,59],["ADD",53,48],["ADD",52,53],["ADD",55,52],["ADD",54,55],["ADD",50,48],["ADD",51,50],["ADD",49,48],["ADD",42,32],["ADD",43,42],["ADD",41,42],["ADD",40,41],["ADD",46,40],["ADD",47,46],["ADD",45,47],["ADD",44,45],["ADD",36,32],["ADD",38,36],["ADD",39,38],["ADD",37,36],["ADD",33,32],["ADD",35,33],["ADD",34,35],["ADD",17,0],["ADD",16,17],["ADD",25,16],["ADD",24,25],["ADD",29,24],["ADD",28,29],["ADD",31,28],["ADD",30,31],["ADD",26,24],["ADD",27,26],["ADD",22,16],["ADD",23,22],["ADD",21,23],["ADD",20,21],["ADD",19,16],["ADD",18,19],["ADD",8,0],["ADD",12,8],["ADD",14,12],["ADD",15,14],["ADD",13,12],["ADD",9,8],["ADD",11,9],["ADD",10,11],["ADD",5,0],["ADD",4,5],["ADD",7,4],["ADD",6,7],["ADD",2,0],["ADD",3,2],["ADD",1,0]]},"hierarchy_8":{"cost":"67","cuts":[{"price":"1","rows":[0]},{"price":"8","rows":[1]},{"price":"4","rows":[2]},{"price":"4","rows":[3]},{"price":"6","rows":[2,3]},{"price":"6","rows":[4]},{"price":"6","rows":[5]},{"price":"4","rows":[4,5]},{"price":"8","rows":[6]},{"price":"8","rows":[7]},{"price":"2","rows":[6,7]},{"price":"10","rows":[4,5,6,7]}],"parents":[null,0,0,2,5,0,7,4],"q":8,"schema_version":1,"word":[["ADD",1,0],["ADD",3,2],["ADD",2,0],["ADD",6,7],["ADD",7,4],["ADD",4,5],["ADD",5,0],["P",0],["ADD",5,0],["ADD",4,5],["ADD",7,4],["ADD",6,7],["ADD",2,0],["ADD",3,2],["ADD",1,0]]}} diff --git a/research/dirty-fanout-cut-certificate/PROOF.md b/research/dirty-fanout-cut-certificate/PROOF.md new file mode 100644 index 0000000000..6bedd70383 --- /dev/null +++ b/research/dirty-fanout-cut-certificate/PROOF.md @@ -0,0 +1,233 @@ +# Cut certificates for exact dirty-output synthesis + +Tekalign, with substantial OpenAI Codex assistance. Apache-2.0. +This is a self-contained written argument and executable certificate checker, +not independent human review or formal-kernel verification. The graph algorithm +and dirty-output mechanisms are credited prior work. + +## 1. Contract and delta + +Retain Ross Richardson's PR3121 contract. There are q>=1 required rows +A_i in F2^w, w>=1, with independent arbitrary initial dirt a_i. A complete +oracle P_i performs A_i ^= p for the same arbitrary p on every invocation. +Its read-only inputs are disjoint from the A rows and preserved. ADD(i,j) +performs A_i ^= A_j for i != j. Required endpoint: A_i=a_i+p for every i. +Words are finite, fixed and straight-line. Every gate is paid; arbitrary +interleavings and repetitions are permitted. No other helper, COPY, CLEAR, +free basis change, adaptive branch or intermediate observation is admitted. + +Let mu_i>0 be the complete stationary P_i price and c_ij>0 the complete +stationary ADD(i,j) price. **The directed edge is j -> i.** A physical caller +must supply these prices, including source access, routing, frame adapters, +precision, scratch restoration and head return. No physical tariff or selected +supplier placement is constructed here. The implementation accepts exact +positive rational prices; the certificate soundness argument also applies to +real prices whenever the displayed inequalities are established exactly. + +PR3121 proves the optimum is a directed rooted-forest bill using Edmonds' +disjoint-branching theorem. Its executable uses bounded enumeration. This +package supplies a polynomial arithmetic-operation compiler and a small +independent checker. The checker proves a concrete all-word optimum by adding +weighted cut inequalities. It neither calls the optimizer nor invokes the +branching theorem. This does not claim a new graph optimization algorithm, +new forest synthesis identity, replacement of the physical H1-H5 interface, +or a new multiplication kappa. + +## 2. The word inequality + +For a successful word, let o_i be its number of P_i calls and k_ij its number +of ADD(i,j) gates. For any nonempty row subset S, define + + o(S) = sum_{i in S} o_i, + k(in S) = sum_{i in S, j not in S} k_ij. + +Then + + o(S) + k(in S)/2 >= 1. (1) + +If o(S)>=1 this is immediate. Otherwise the predecessor's dirty-span lemma +requires at least two incoming ADD occurrences. For completeness: + +* With zero incoming ADDs, the coefficient of p in S remains zero, so it + cannot become one in every required row. Here p must be arbitrary. +* With exactly one incoming ADD, specialize p=0 and retain all q independent + dirt columns. Every prefix matrix on dirt is invertible. Before that gate, + the span of the S rows is the coordinate space W_S; internal ADDs preserve + it and outgoing ADDs leave those rows unchanged. The incoming source row + lies outside their span, because all q rows form a basis. Replacing one S + row by its sum with that source changes the S-row span. With no further + incoming gate, internal ADDs preserve this changed span. It cannot return + to W_S at the identity dirt endpoint. Outgoing feedback does not alter the + argument: prefix invertibility still keeps an outside row independent. + +This is PR3121's oracle-free subset argument, itself extending PR3063's +one-row invariant. The new use is the combined inequality (1), which handles +unknown oracle destinations in a single certificate. It does not restrict a +competing word to the compiler's forest shape. + +## 3. A directly checkable lower bound + +Supply a finite collection of nonempty subsets S and rational prices y_S>=0. +Require + + sum_{S containing i} y_S <= mu_i, for every i, + sum_{S: i in S, j not in S} y_S <= 2 c_ij, for every i!=j. (2) + +Multiply (1) by y_S and sum. Nonnegativity of all gate counts and (2) give + + sum_S y_S + <= sum_i o_i sum_{S containing i} y_S + + (1/2) sum_{i!=j} k_ij sum_{S: i in S,j not in S} y_S + <= sum_i mu_i o_i + sum_{i!=j} c_ij k_ij. (3) + +Thus sum y_S lower-bounds **every successful word**, including repetitions, +feedback and interleaved oracle calls. No linear-programming duality theorem, +integrality theorem or graph theorem is needed for this certificate's validity; +(3) is just a nonnegative weighted sum of proved inequalities. + +`check.py` separately verifies all q root capacities and q(q-1) ADD capacities, +positive cut prices, the complete emitted word's symbolic dirt/p endpoint, +literal inverse, actual gate bill, and equality of that bill to sum y_S. Equality +proves the word optimal in this exact contract. Every physical bit position +obeys the same XOR identity, so checking the q dirt symbols and p certifies the +finite word for all widths and arbitrary data, not merely sampled one-bit data. + +The parent array is checked as an additional forest/invoice witness; the actual +emitted gates establish the upper bound. The checker does not trust the parent +array instead of replaying those gates. Nor does it require laminar cuts. A +positive control supplies two crossing cuts plus singleton cuts, independent of +the compiler's output, and obtains the same cost-8 valid endpoint. + +## 4. Constructing certificates without enumerating forests + +Use the classical Chu-Liu/Edmonds minimum-arborescence contraction algorithm. +Add a **graph-only** root s, root edges s->i of weight mu_i, and ordinary edges +j->i of weight 2c_ij. This root is not a physical helper or free oracle. +Deleting s from an outward arborescence gives a directed rooted forest. + +The implementation maintains disjoint clusters of original rows and residual +weights. Initially clusters are singletons. At each level: + +1. For every nonroot cluster V, choose its cheapest incoming edge, with an + explicit deterministic tie rule. Subtract its residual weight delta_V + from every edge entering V, and add delta_V to the certificate price y_V. +2. If chosen edges are acyclic, they form a rooted spanning arborescence; + every nonroot has one parent, and following parents must reach s. +3. Otherwise contract one chosen-edge cycle to its union cluster, remove + self edges and continue. Keep original edge identities and each cycle's + chosen edges for expansion. There are at most q-1 contractions. +4. Expand in reverse. A contracted cluster has exactly one entering selected + edge. Keep its actual entry vertex, and add the saved cycle edges into all + other cycle vertices. This breaks the cycle, spans the cluster and leaves + a rooted tree with exactly one entering edge for every recorded cluster. + +Root reachability is guaranteed by the finite root edge to every original +row. The root is never on a selected-parent cycle. All residuals are nonnegative +because delta_V is the cheapest incoming residual; all emitted prices are +nonnegative. The compiler drops zero-price cuts. + +For any original edge e, its residual is + + w_e - sum_{recorded S entered by e} y_S. (4) + +While its endpoints are in different clusters, step 1 updates exactly the +relevant term in (4). Once its endpoints coalesce, no later cluster separates +them, so removed internal edges need no later updates. This proves every +original edge capacity in (2), not merely capacities of the final graph. + +Every saved cycle edge is tight when chosen. After its endpoints coalesce, +its residual stays zero. Final acyclic chosen edges are also tight. Expansion +selects only such edges and gives exactly one selected edge entering every +cluster whose price was raised. Summing their original weights via (4) gives + + selected graph weight = sum_S y_S. (5) + +This proves the constructive certificate property. It is also the standard +primal/dual explanation of contraction, included to make the implementation +reviewable; no priority for that method is claimed. Even a bug in this compiler +cannot establish a false result unless the separate checker also accepts a +false capacity, endpoint or equality. Source/code authentication and ordinary +software correctness remain part of the trusted verification boundary. + +The cluster family is laminar: any two are disjoint or one contains the other. +There are at most 2q-1 distinct nonempty clusters (q leaves and at most q-1 +unions). The explicit implementation retains at most q^2 original arcs and +uses O(q^3) rational arithmetic operations. Its naive certificate checker also +uses O(q^3) arithmetic operations for these certificates. This is an arithmetic- +operation count, not a uniform unit-cost bit-time or physical tape bound. Exact +rational bit lengths and input/output storage are real costs. The complete +q-by-q tariff matrix must already have been supplied by the caller. + +## 5. The restored word and complete price + +For each forest edge parent(i)->i, execute ADD(i,parent(i)) in child-before- +parent order. Call P once on each forest root. Execute the preparation ADDs +in literal reverse order. During preparation each parent still has its original +dirt when read. Each nonroot therefore holds a_i+a_parent. On the return pass, +parents have already become a_parent+p, so that row becomes a_i+p. Roots get +that endpoint from their P calls. No extra row or oracle uncompute is hidden. + +The complete price is exactly + + sum_roots mu_i + 2 sum_edges c_ij. (6) + +Together, (3), (5) and the executed endpoint prove optimality. The exact inverse +reverses all gates and has the same bill; a caller needing it as another stage +must pay again. An arbitrary path-dependent or time-dependent tariff cannot +be substituted into (6). The package does not price independent private oracles; +their fixed additive bill is handled separately by the credited predecessor. + +The chain fixture from PR3121 has cost 5. A constructed cheap-cycle control +has mu=(1,100,100), c_12=c_21=1, c_10=c_20=50 and c_01=c_02=100. +Choosing each row's cheapest incoming augmented edge gives 1+2+2=5 but has +an unrooted cycle. The certificate assigns y_{0}=1, y_{1}=y_{2}=2 and +**y_{1,2}=98**, proving 103. Two roots and one twice-paid edge attain 103. +The extra cut records the missing root connection instead of trusting a +cycle-free label or enumerating all competing words. + +## 6. Coverage and remaining obligations + +`RESULT.json` records complete q<=3 tariff cubes with every mu_i,c_ij in +{1,5}: 530 cases compared to unrestricted shortest paths on exact affine +states, with 394 strict sharing wins and 240 mixed-root certificates. These +comparisons optimize over arbitrary gate interleavings at the stated tiny +sizes, not over a full physical model. +The separate parent-function implementation checks 48 seeded positive rational +instances through q=6 (145,984 forests across those repetitions). Larger +constructed instances have q=8,16,31,64,112. These domains are corroboration; +the word inequality and certificate argument supply the all-word conclusion. + +The q=112 example is an explicitly **synthetic** stationary tariff matrix. +It has a 223-gate word (one oracle, 222 ADDs), 216 positive cuts, and 12,544 +capacity inequalities. Its exact declared optimum is 1,539. This is a compiler +stress case with nested cycles, not a selected supplier invoice or a claimed +physical saving. All named certificates are committed in compact JSON. + +Negative controls cover missing restoration/oracle calls, wrong edge direction, +undercharged edge capacity, inflated/negative/duplicate cuts, cyclic parents, +typed values, wrong cost, source/receipt corruption, duplicate input keys and +operation under `-O`. An export executes the checker after physically removing +the compiler file. A nonlaminar positive certificate tests acceptance beyond +what the contraction generator emits. + +An actual physical caller with legal unobserved target lifetimes and complete +stationary prices remains missing. The contribution removes an exhaustive +synthesis/certificate-checking obstacle; it does not solve the predecessor's +physical caller, frame, clean/dirty hosting, precision or complete supplier +recurrence obligations. No selected record, upstream source or kappa changes. + +## Credit + +Ross Richardson's PR3121 (`eea0861aff47df568be4bb4a4db43c2da390d351`) supplies +the subset dirty-span lemma, exact edge-price theorem and forest tariff model; +PR3063 (`3f384b8b7daccb2c8e12013fd81a738202ce0f8d`) supplies the destination +tradeoff. Cinna Davis/PR1944 supplies the original dirty echo; PR1968's multiple +common-term accumulation is separate. Anthony/PR774, Oscar Fennell/PR759 and +the retained synthesis literature keep their forest-construction credit. + +Credit Y. J. Chu and T. H. Liu, *On the shortest arborescence of a directed +graph*, Scientia Sinica 14 (1965), 1396-1400, and Jack Edmonds, *Optimum +branchings*, J. Res. NBS 71B (1967), 233-240, DOI 10.6028/jres.071B.032. +The code is newly written; no third-party implementation is copied. The general +contraction and primal/dual method are classical. This result is their explicit +word-level certificate application and reusable scoped implementation. diff --git a/research/dirty-fanout-cut-certificate/README.md b/research/dirty-fanout-cut-certificate/README.md new file mode 100644 index 0000000000..a8c115df29 --- /dev/null +++ b/research/dirty-fanout-cut-certificate/README.md @@ -0,0 +1,140 @@ +# Exact dirty-output circuits with small cut certificates + +**Scoped proof simplification and synthesis tool.** A supplied complete directed +tariff matrix now produces a restored-XOR circuit and an independently checkable +optimality certificate. The checker uses a weighted sum of elementary dirty-data +cut inequalities; it does not import the optimizer or invoke the external +branching theorem used by PR3121. No physical supplier or new kappa is claimed. + +## What changes + +Ross Richardson's [PR3121](https://github.com/CrocSwap/integer-mult-bounds/pull/3121) +proved the exact stationary dirty-output fanout tariff. Its executable enumerates +small forests. This package supplies the classical Chu-Liu/Edmonds contraction +algorithm, emits the actual preparation/oracle/restoration word, and verifies a +matching lower bound for **all permitted interleaved words**, not only forests. + +The reusable observation is simple. For any nonempty set S of output rows, +a successful word must either invoke the shared-value oracle inside S or pay +at least two incoming ADDs to deliver the value and restore arbitrary dirt: + +``` +oracle_calls(S) + incoming_ADDs(S)/2 >= 1. +``` + +Price several such cuts. If their combined load is at most mu_i on every oracle +and 2c_ij on every ADD edge, their total price lower-bounds every successful +word. When the emitted circuit costs exactly that total, optimality follows. +[PROOF.md](PROOF.md) gives the self-contained argument, credited subset lemma, +contraction invariant, complete word and scope. This is an explicit application +of classical graph optimization, not a new general optimization theorem. + +A useful failure control is the cheap directed cycle: per-row cheapest choices +suggest cost 5 but cannot reach a root. The certificate adds the missing +joint-cut price 98, proving the correct optimum **103**. This catches the +structural error with inequalities, without enumerating competing circuits. + +## Executed evidence + +- All **530** tariff matrices through three rows with every positive price in + `{1,5}` match unrestricted exact shortest paths on affine maps: **394** strict + sharing wins and **240** mixed-root certificates. +- **48** seeded rational instances through six rows match a separate exhaustive + parent-function implementation, checking **145,984** forests across those cases. +- Nested-cycle examples through **112 rows** compile and pass the separate checker. + The 112-row fixture has **216 cut prices**, **12,544 capacity inequalities**, + one oracle and 222 ADDs. Its declared optimum is **1,539**. +- Eleven semantic/certificate mutation controls, four invalid-price cases, + source/receipt/cost corruption, duplicate input keys and optimized read-only + Git-free replay pass. A valid certificate with crossing cuts is accepted even + though the compiler only emits laminar cuts. The exported CLI checker runs + after the compiler file is removed. + +[RESULT.json](RESULT.json) records complete deterministic receipts. +[CERTIFICATES.json](CERTIFICATES.json) contains the exact named certificates in +compact JSON. The large matrices are **synthetic stationary tariffs**, defined +exactly by `hierarchical_prices` with seed 19; they are not prices of the selected +supplier. The finite searches corroborate the proof and implementation, rather +than prove a full physical multiplication theorem. + +The implementation uses O(q^3) rational arithmetic operations, and its certificates +have at most 2q-1 cuts. Bit lengths and the complete input matrix are real costs; +no unit-cost physical-tape claim is made. On the same six-row instance, three +alternating CPython 3.12.14 runs gave median **49.75 ms** for exhaustive enumeration +and **0.684 ms** for compilation plus the full checker (about 73x). Both returned +exactly 49. [BENCHMARK.json](BENCHMARK.json) records every timing, input digest and +environment. This compares the new exhaustive reference with the new compiler, +not two versions of a production physical routine. Timing is descriptive, never +a mathematical acceptance threshold. + +## Use and reproduce + +Python 3.12 standard library, from the repository root: + +```sh +python3.12 scripts/research_package.py --package research/dirty-fanout-cut-certificate +``` + +Expected markers: `PASS_DIRTY_FANOUT_CUT_SYNTHESIS`, +`PASS_DIRTY_FANOUT_CUT_EXPORT_CONTROLS`, and `PASS_REGISTERED_RESEARCH_PACKAGE`. +Direct `verify.py --suite small`, `examples` or `controls` runs a bounded subset. +`verify.py --emit` prints a fresh receipt and writes the named certificates. +`benchmark.py` reruns the same-input timing comparison without a speed threshold. + +For a user-supplied tariff matrix, `mu[i]` prices a complete P_i call and +`add[i][j]` prices ADD(i,j), directed **j -> i**. Diagonals must be null; all other +prices are positive integers or exact rational strings. No float prices: + +```sh +python3.12 research/dirty-fanout-cut-certificate/synthesize.py \ + research/dirty-fanout-cut-certificate/examples/chain.json > /tmp/fanout-certificate.json +python3.12 research/dirty-fanout-cut-certificate/check.py \ + research/dirty-fanout-cut-certificate/examples/chain.json /tmp/fanout-certificate.json +``` + +Expected: `PASS_DIRTY_FANOUT_CUT_CERTIFICATE`, cost `5`, one oracle and four ADDs. +The checker can be distributed separately with the tariff and certificate files. +It contains no solver dependency. Direct execution requires no Git, network, +third-party libraries or predecessor executable. + +Exact scientific base: **`997e6a9ca7b4f95d50e366f61412fd640d72a88a`**. +[SOURCES.json](SOURCES.json) pins live predecessor documents and records exact +PR3121 reference hashes/head. The subset argument is rederived in the local +proof; no pending predecessor code or graph theorem is imported at runtime. +[TASK.json](TASK.json) records the changed card scope, seed, candidate selection, +completed domains and stopping rule. [Coordination claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/3061#discussioncomment-18989707). + +## Open next questions + +The model requires arbitrary independent dirty output rows, the same arbitrary +common value from disjoint preserved sources, stationary complete positive +prices and unobserved intermediate rows. There are no extra helpers or free +COPY/CLEAR/basis changes. A separately required inverse has the same bill and +must be paid again. Path-, state- or frame-dependent prices require a new model. + +The next physical task remains to name one operand-compatible caller, prove its +target lifetimes, and price every oracle/ADD route including access, frame +adapters, precision, restoration, ownership and head return. Those obligations +block supplier admission; this tool does not remove them. Once that matrix is +available, synthesis and a directly inspectable optimum certificate are ready. + +A separate optional formalization can encode the dirty-span lemma and weighted +inequality, then the finite checker. This would shrink the trusted software +boundary further; no proof-assistant or independent human verification is claimed. +The selected frontier, frozen packages and `upstream/` are unchanged. + +## Credit + +Prepared by **Tekalign**, with substantial **OpenAI Codex** assistance in +mathematics, coding, verification and writing; Apache-2.0. Credit Ross Richardson's +PR3121 at `eea0861aff47df568be4bb4a4db43c2da390d351` for the subset lemma, edge-price +optimum and chain example; PR3063 at `3f384b8b7daccb2c8e12013fd81a738202ce0f8d` for +the destination tradeoff; Cinna Davis/PR1944 for the original dirty echo; PR1968's +separate multiple-term accumulation; Anthony/PR774, Oscar Fennell/PR759 and the +retained forest-synthesis lineage. Their discoveries are not claimed anew. + +Credit Chu and Liu (1965) and Edmonds (1967), +[Optimum branchings](https://doi.org/10.6028/jres.071B.032), for the classical +contraction/optimization method. The code is newly written without copying a +third-party implementation. The contribution is the explicit cut-certificate +application, compiler and separate checker for this dirty-output contract. diff --git a/research/dirty-fanout-cut-certificate/RESULT.json b/research/dirty-fanout-cut-certificate/RESULT.json new file mode 100644 index 0000000000..22c9101634 --- /dev/null +++ b/research/dirty-fanout-cut-certificate/RESULT.json @@ -0,0 +1,121 @@ +{ + "controls": { + "invalid_price_types": 4, + "nonlaminar_certificate": true, + "rejected_mutations": [ + "missing_restore", + "missing_root", + "wrong_add_direction", + "inflated_cut", + "negative_cut", + "duplicate_row", + "typed_cost", + "typed_row", + "parent_cycle", + "unpaid_cut", + "forgot_half_ADD_coefficient" + ] + }, + "examples": [ + { + "adds": 4, + "certificate_sha256": "f2e213c4d562cd2eceb3113a60783433e04b6d674eb7e40adf045d47270affe1", + "cost": "5", + "cuts": 3, + "direct_cost": "201", + "inequalities": 9, + "largest_cut": 1, + "name": "chain", + "oracles": 1, + "rows": 3, + "tariffs_sha256": "6c9ad4d935287ab95fde7e671490ab7abad058ad53936158c560901ddba09a7c" + }, + { + "adds": 2, + "certificate_sha256": "65853cb9d8ad69dbf65d81adfbb6249045fd55ca25ccd65f9459e803922aaa54", + "cost": "103", + "cuts": 4, + "direct_cost": "201", + "inequalities": 9, + "largest_cut": 2, + "name": "cheap_cycle", + "oracles": 2, + "rows": 3, + "tariffs_sha256": "a62853ab9d5e9ef2c3c0f2503a53b86539592d8c685eb6de351202d94d91f315" + }, + { + "adds": 14, + "certificate_sha256": "60d49b0f538e6464e57d395332a9f1728ec9bda95fc209f0aa51485720a29c24", + "cost": "67", + "cuts": 12, + "direct_cost": "70096", + "inequalities": 64, + "largest_cut": 4, + "name": "hierarchy_8", + "oracles": 1, + "rows": 8, + "tariffs_sha256": "6581c619294a0de583081c6b102dd77e0f40e0e94b8f3f9d122780c8b81f3e29" + }, + { + "adds": 30, + "certificate_sha256": "c06c0ba3a775aa37dc507009e132aa9bc0876cdf8e0c7dba06aa76d3e95b9a34", + "cost": "163", + "cuts": 27, + "direct_cost": "150188", + "inequalities": 256, + "largest_cut": 8, + "name": "hierarchy_16", + "oracles": 1, + "rows": 16, + "tariffs_sha256": "17c22d10053d24863922fd2ce890ba8a7a73b420a22775dab5a66768540eacac" + }, + { + "adds": 60, + "certificate_sha256": "a698df4d687821d6c30178c41faf90a127e714fcb872ffef5275478d7c025625", + "cost": "371", + "cuts": 56, + "direct_cost": "300349", + "inequalities": 961, + "largest_cut": 15, + "name": "hierarchy_31", + "oracles": 1, + "rows": 31, + "tariffs_sha256": "34b3fccc303f6456883370f2bd5f6b7f7806208ddbf86079e8280df8ecdc6bf8" + }, + { + "adds": 126, + "certificate_sha256": "a8a320b587457880b5c403a994792f67c464bf964507712cc130c024b96a6358", + "cost": "827", + "cuts": 121, + "direct_cost": "630700", + "inequalities": 4096, + "largest_cut": 32, + "name": "hierarchy_64", + "oracles": 1, + "rows": 64, + "tariffs_sha256": "b122dfe62eb12ab8f7c2a10725f54ea0b2863d113b1b0fd85920ccf5434fee02" + }, + { + "adds": 222, + "certificate_sha256": "bfd8b0acc5b7f217b4e9887c28c0bfd765e0f38a97e11795b54ff45ff5246b55", + "cost": "1539", + "cuts": 216, + "direct_cost": "1111242", + "inequalities": 12544, + "largest_cut": 48, + "name": "hierarchy_112", + "oracles": 1, + "rows": 112, + "tariffs_sha256": "91d09b7a0c17ee611bf5510ea58c1b27201ba1d5ef2f6c3f126add15ca6f67de" + } + ], + "small": { + "affine_settled_states": 84227, + "affine_tariff_instances": 530, + "enumerated_forests": 145984, + "mixed_root_certificates": 240, + "rational_forest_instances": 48, + "receipt_sha256": "ec0c90c396fa41b7749ca5bc45d4781d581f32a4588c0597c0ebc443beea4b78", + "strict_sharing_wins": 394 + } +} diff --git a/research/dirty-fanout-cut-certificate/SOURCES.json b/research/dirty-fanout-cut-certificate/SOURCES.json new file mode 100644 index 0000000000..ebf2553681 --- /dev/null +++ b/research/dirty-fanout-cut-certificate/SOURCES.json @@ -0,0 +1,63 @@ +{ + "schema_version": 1, + "base_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/dirty-anchor-tradeoff/PROOF.md", + "usage": "input", + "git_blob": "3a097f2d7d9257adde19b2a4fb559b3a5fa2e6ac", + "sha256": "ba2fd83c22f57bd7658550067c9da4331fa84c22f8fa611eb0717bceac03f764" + }, + { + "path": "research/dirty-anchor-tradeoff/README.md", + "usage": "input", + "git_blob": "34835986c889dab2ab51218963778b80fc29c01d", + "sha256": "5e0da575c58ee15f99672128aa74aa7ecac4a8b6e60703e1ad73cd5ed68508a7" + } + ], + "references": [ + { + "pr": 3121, + "head": "eea0861aff47df568be4bb4a4db43c2da390d351", + "path": "research/dirty-anchor-edge-tariffs/PROOF.md", + "author": "Ross Richardson, with substantial OpenAI Codex assistance", + "git_blob": "7643ababf0f003eaf699edb4910ce9693025b5cd", + "sha256": "1c73b56222dbd63a2230a23c00ce4b822eaa3aa7cdd4c5d6ba9975b98857b289", + "use": "Read-only mathematical predecessor; its subset lemma is rederived with credit. No executable imports or runtime dependence." + }, + { + "pr": 3121, + "head": "eea0861aff47df568be4bb4a4db43c2da390d351", + "path": "research/dirty-anchor-edge-tariffs/README.md", + "author": "Ross Richardson, with substantial OpenAI Codex assistance", + "git_blob": "16aa73e36b791fd4c025011123b8101dd4a1c2d6", + "sha256": "dae5277016949f17bc55191e34a5f9470475b94ed679c843217973711ce2a341", + "use": "Read-only mathematical predecessor; its subset lemma is rederived with credit. No executable imports or runtime dependence." + } + ], + "algorithm_credit": [ + { + "authors": "Y. J. Chu and T. H. Liu", + "title": "On the shortest arborescence of a directed graph", + "year": 1965 + }, + { + "author": "Jack Edmonds", + "title": "Optimum branchings", + "year": 1967, + "doi": "10.6028/jres.071B.032" + } + ] +} diff --git a/research/dirty-fanout-cut-certificate/TASK.json b/research/dirty-fanout-cut-certificate/TASK.json new file mode 100644 index 0000000000..00c76da8bc --- /dev/null +++ b/research/dirty-fanout-cut-certificate/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 6, + "base_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "changed", + "actual_scope": "Compile an exact stationary dirty-output fanout word and certify its unrestricted all-word optimum with elementary weighted-cut inequalities.", + "scope_change_reason": "The bit-track helper-contract reading led to PR3121. This contributes exact synthesis and a smaller trusted certificate boundary, not another R439 helper-star rewrite or another abstract fanout census. It does not claim H1-H5 replacement or a physical caller.", + "bottleneck_link": "A supplied complete directed tariff matrix can now be turned into an optimal restored-XOR word and a small independent lower-bound certificate without exhaustive forest enumeration; physical tariff derivation remains the bottleneck.", + "budget_minutes": 60, + "stop_rule": "One compiler/certificate implication. Reject the approach if cuts do not cover arbitrary gate interleavings, expansion fails to return dirty state, or exact tiny searches disagree. Stop after the fixed declared domains and reserve the final quarter for verification and publication.", + "outcome": "completed", + "evidence": "Self-contained cut lower-bound and contraction certificate proof; exact emitted word/cut certificates through 112 rows; 530 unrestricted affine optima, 48 rational forest cases, mutation/export controls and same-input benchmark.", + "author": "Tekalign", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematics, implementation, verification and writing. No independent human or formal-kernel review claimed.", + "open_questions": [ + { + "question": "Bind an actual physical caller to complete stationary directed prices.", + "why_it_matters": "Abstract optimality does not supply physical access, frames, ownership or recursive costs.", + "first_step": "Identify one named shared-value group, prove unobserved target lifetimes and price all oracle/ADD routes before invoking the compiler.", + "blocked_by": "Operand compatibility, source/target placement, physical restoration, price stationarity and full supplier bill." + }, + { + "question": "Formalize the small certificate soundness theorem, if a proof-kernel consumer is needed.", + "why_it_matters": "The certificate removes the optimizer from the trusted mathematical path, but the Python checker and written cut proof are still unformalized.", + "first_step": "Encode independent dirt rows and prove equation (1), then the nonnegative weighted sum (3).", + "blocked_by": "No current proof-assistant integration is claimed or required by this package." + } + ], + "assignment_seed": 19, + "assignment_randomness": "Python secrets.randbelow(100), operating-system randomness", + "track": "bit supplier / helper contract", + "candidate_tasks": [ + "R439 disjoint-helper pairing after PR3117", + "Larger-register identities beyond the scoped three-register obstruction", + "Exact cut-certified dirty-output fanout synthesis after PR3121 (selected)" + ], + "seed_use": "Random(19) for 48 rational tariff instances; seed19 also specifies the deterministic larger asymmetric nested-cycle tariff family. Exhaustive {1,5} cubes are not random.", + "overlap_coverage": "Main refreshed to the exact base; all 255 open PR metadata records, latest 100 updated PRs with recent comments/reviews, open issues, handoffs and claims, and current Discussion3061 read. This is not a review of every diff or unpublished work.", + "expansion_decision": { + "proved_or_inherited": "Credited dirty-span cut lemma, stated stationary common-oracle contract and forest echo.", + "new_evidence": "Exact cut-weight inequality directly certifies arbitrary-interleaving optimality; constructed compiler emits valid matching certificates and complete XOR words.", + "unknown": "An actual physical operand-compatible caller and complete stationary tariff matrix, routing/frames/hosting/precision and supplier admission.", + "decision": "Proceed with one bounded proof/tool simplification. Do not expand physical supplier construction or claim a new exponent." + } +} diff --git a/research/dirty-fanout-cut-certificate/VERIFY.json b/research/dirty-fanout-cut-certificate/VERIFY.json new file mode 100644 index 0000000000..e01184310f --- /dev/null +++ b/research/dirty-fanout-cut-certificate/VERIFY.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/dirty-anchor-tradeoff/PROOF.md", + "research/dirty-anchor-tradeoff/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Exact contraction/cut certificates; unrestricted affine searches and independent parent enumeration; complete symbolic dirty endpoints/inverse; semantic and price mutation controls." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/check_export.py" + ], + "timeout_seconds": 300, + "checks": "Optimized read-only Git-free replay; standalone checker with compiler removed; source, word, cost, receipt and input-key corruption controls." + } + ] +} diff --git a/research/dirty-fanout-cut-certificate/benchmark.py b/research/dirty-fanout-cut-certificate/benchmark.py new file mode 100644 index 0000000000..405ba124e5 --- /dev/null +++ b/research/dirty-fanout-cut-certificate/benchmark.py @@ -0,0 +1,35 @@ +#!/usr/bin/env python3 +"""Same-input exact enumeration versus compiler+checker; timing is descriptive.""" +import gc +import json +import platform +from statistics import median +from time import perf_counter +from pathlib import Path +import types + +HERE = Path(__file__).resolve().parent +v = types.ModuleType('benchmark_verifier') +v.__file__ = str(HERE/'verify.py') +exec(compile((HERE/'verify.py').read_bytes(),v.__file__,'exec'),v.__dict__) +v.sources() +mu,add = v.hierarchical_prices(6) +times = {'enumeration':[],'compiler_and_checker':[]} +answers = set() +for repeat in range(3): + for name in (list(times) if repeat % 2 == 0 else list(reversed(times))): + gc.collect() + start = perf_counter() + if name == 'enumeration': + optimum,forests = v.forest_min(mu,add) + else: + certificate = v.solver.synthesize(mu,add) + optimum = v.Fraction(v.checker.check(mu,add,certificate)['cost']) + times[name].append(perf_counter()-start) + answers.add(str(optimum)) +v.need(len(answers) == 1,'same exact optimum') +print(json.dumps(dict(python=platform.python_version(),platform=platform.platform(), + rows=6,seed=19,tariffs_sha256=v.digest([mu,add]), + optimum=next(iter(answers)),enumerated_forests=forests, + seconds=times,median_seconds={k:median(t) for k,t in times.items()}, + scope='New exhaustive forest baseline versus new compiler plus full certificate checker; not physical runtime.'),indent=2,sort_keys=True)) diff --git a/research/dirty-fanout-cut-certificate/check.py b/research/dirty-fanout-cut-certificate/check.py new file mode 100644 index 0000000000..a246cd1753 --- /dev/null +++ b/research/dirty-fanout-cut-certificate/check.py @@ -0,0 +1,117 @@ +"""Small certificate checker: no optimizer, graph solver or predecessor import. + +Proves a concrete optimum from restored-XOR semantics, cut-price feasibility, +and equality. The all-word cut inequality is justified in PROOF.md. +""" +from fractions import Fraction + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def rational(text): + need(type(text) is str, 'canonical rational string') + value = Fraction(text) + need(str(value) == text, 'canonical rational string') + return value + + +def check(mu, add, certificate): + n = len(mu) + need(n >= 1 and len(add) == n and all(len(row) == n for row in add), 'tariff shape') + need(all(type(v) in (int,Fraction) and v > 0 for v in mu), 'positive exact tariff') + need(all(add[i][i] is None for i in range(n)), 'no self ADD tariff') + need(all(type(add[i][j]) in (int,Fraction) and add[i][j] > 0 + for i in range(n) for j in range(n) if i != j), 'positive exact tariff') + need(set(certificate) == {'schema_version','q','parents','cuts','cost','word'}, 'certificate fields') + need(type(certificate['schema_version']) is int and certificate['schema_version'] == 1, + 'schema version') + need(type(certificate['q']) is int and certificate['q'] == n, 'row count') + parents = certificate['parents'] + need(type(parents) is list and len(parents) == n, 'parent list') + need(all(j is None or (type(j) is int and 0 <= j < n and j != i) + for i,j in enumerate(parents)), 'parent domain') + for i in range(n): + seen, j = set(), i + while j is not None: + need(j not in seen, 'parent cycle') + seen.add(j) + j = parents[j] + cut_masks, weights = [], [] + need(type(certificate['cuts']) is list, 'cut list') + for cut in certificate['cuts']: + need(type(cut) is dict and set(cut) == {'rows','price'}, 'cut fields') + rows = cut['rows'] + need(type(rows) is list and rows and all(type(i) is int and 0 <= i < n for i in rows) + and rows == sorted(set(rows)), 'cut rows') + mask = sum(1 << i for i in rows) + need(mask not in cut_masks, 'duplicate cut') + value = rational(cut['price']) + need(value > 0, 'positive cut price') + cut_masks.append(mask) + weights.append(value) + for i in range(n): + root_load = sum(w for s,w in zip(cut_masks,weights) if s & (1 << i)) + need(root_load <= mu[i], 'root dual capacity') + for j in range(n): + if i != j: + load = sum(w for s,w in zip(cut_masks,weights) + if s & (1 << i) and not s & (1 << j)) + need(load <= 2*add[i][j], 'ADD dual capacity') + # Actual emitted gates, not the parent vector, establish the upper bound. + state = [1 << i for i in range(n)] + common = 1 << n + bill = Fraction(0) + word = certificate['word'] + need(type(word) is list and word, 'nonempty word') + for gate in word: + need(type(gate) is list and gate and gate[0] in ('P','ADD'), 'gate opcode') + need(len(gate) == (2 if gate[0] == 'P' else 3) and + all(type(i) is int and 0 <= i < n for i in gate[1:]), 'gate operands') + i = gate[1] + if gate[0] == 'P': + state[i] ^= common + bill += mu[i] + else: + j = gate[2] + need(i != j, 'self ADD') + state[i] ^= state[j] + bill += add[i][j] + need(state == [(1 << i) ^ common for i in range(n)], 'arbitrary-dirt endpoint') + for gate in reversed(word): + state[gate[1]] ^= common if gate[0] == 'P' else state[gate[2]] + need(state == [1 << i for i in range(n)], 'literal inverse') + forest_bill = sum(mu[i] if j is None else 2*add[i][j] for i,j in enumerate(parents)) + cost = rational(certificate['cost']) + need(bill == forest_bill == cost == sum(weights), 'primal dual equality') + # Laminarity is an optimizer property, deliberately not a validity premise. + return dict(cost=str(cost), rows=n, cuts=len(weights), + oracles=sum(g[0] == 'P' for g in word), + adds=sum(g[0] == 'ADD' for g in word), inequalities=n*n) + + +if __name__ == '__main__': + import argparse + import json + from pathlib import Path + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('tariffs', type=Path) + parser.add_argument('certificate', type=Path) + args = parser.parse_args() + def unique(pairs): + result = {} + for key,value in pairs: + need(key not in result, 'duplicate JSON key') + result[key] = value + return result + data = json.loads(args.tariffs.read_bytes(), object_pairs_hook=unique) + need(set(data) == {'mu','add'}, 'tariff fields') + def parse(v): + need(type(v) in (int,str), 'exact JSON tariff') + return Fraction(v) + mu = list(map(parse, data['mu'])) + add = [[None if v is None else parse(v) for v in row] for row in data['add']] + result = check(mu, add, json.loads(args.certificate.read_bytes(),object_pairs_hook=unique)) + print('PASS_DIRTY_FANOUT_CUT_CERTIFICATE', json.dumps(result,sort_keys=True)) diff --git a/research/dirty-fanout-cut-certificate/check_export.py b/research/dirty-fanout-cut-certificate/check_export.py new file mode 100644 index 0000000000..f5265bee3b --- /dev/null +++ b/research/dirty-fanout-cut-certificate/check_export.py @@ -0,0 +1,100 @@ +#!/usr/bin/env python3 +"""Optimized read-only export; independent CLI and disk-corruption controls.""" +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def main(): + with tempfile.TemporaryDirectory(prefix='fanout-cut-export-') as temp: + root = Path(temp) + package = root/'research'/HERE.name + shutil.copytree(HERE,package,ignore=shutil.ignore_patterns('__pycache__','*.pyc')) + for name in json.loads((HERE/'VERIFY.json').read_bytes())['inputs']: + to = root/name + to.parent.mkdir(parents=True,exist_ok=True) + shutil.copyfile(ROOT/name,to) + def run(script,*args): + return subprocess.run([sys.executable,'-O','-B',str(package/script),*map(str,args)], + cwd=root,capture_output=True,text=True,timeout=240) + files = [p for p in root.rglob('*') if p.is_file()] + dirs = sorted([p for p in root.rglob('*') if p.is_dir()],key=lambda p:len(p.parts),reverse=True) + for p in files: + p.chmod(0o444) + for p in (*dirs,root): + p.chmod(0o555) + try: + completed = run('verify.py') + finally: + for p in (root,*reversed(dirs)): + p.chmod(0o755) + for p in files: + p.chmod(0o644) + need(completed.returncode == 0 and 'PASS_DIRTY_FANOUT_CUT_SYNTHESIS' in completed.stdout, + 'optimized read-only Git-free replay: '+completed.stderr) + # Generate a real CLI certificate, then remove the compiler completely. + tariffs = package/'examples/chain.json' + generated = run('synthesize.py',tariffs) + need(generated.returncode == 0,'compiler CLI: '+generated.stderr) + cert = package/'cli-certificate.json' + cert.write_text(generated.stdout) + compiler = package/'synthesize.py' + compiler.rename(package/'compiler-unavailable.txt') + checked = run('check.py',tariffs,cert) + need(checked.returncode == 0 and 'PASS_DIRTY_FANOUT_CUT_CERTIFICATE' in checked.stdout, + 'independent CLI without compiler: '+checked.stderr) + changed = json.loads(generated.stdout) + changed['word'].pop() + cert.write_text(json.dumps(changed)) + rejected = run('check.py',tariffs,cert) + need(rejected.returncode != 0 and 'arbitrary-dirt endpoint' in rejected.stderr, + 'disk word corruption rejected') + (package/'compiler-unavailable.txt').rename(compiler) + receipt = package/'RESULT.json' + raw = receipt.read_bytes() + changed = json.loads(raw) + changed['controls']['nonlaminar_certificate'] = 1 + receipt.write_text(json.dumps(changed)) + rejected = run('verify.py','--suite','controls') + need(rejected.returncode != 0 and 'complete typed receipt' in rejected.stderr, + 'typed receipt corruption rejected') + receipt.write_bytes(raw) + source = root/'research/dirty-anchor-tradeoff/PROOF.md' + raw = source.read_bytes() + source.write_bytes(raw+b'\nchanged\n') + rejected = run('verify.py','--suite','controls') + need(rejected.returncode != 0 and 'live source SHA256' in rejected.stderr, + 'live source drift rejected') + source.write_bytes(raw) + certificates = package/'CERTIFICATES.json' + raw = certificates.read_bytes() + changed = json.loads(raw) + changed['chain']['cost'] = '6' + certificates.write_text(json.dumps(changed)) + # Only this single certificate is needed to detect its corruption. + cert.write_text(json.dumps(changed['chain'])) + rejected = run('check.py',tariffs,cert) + need(rejected.returncode != 0 and 'primal dual equality' in rejected.stderr, + 'certificate cost corruption rejected') + certificates.write_bytes(raw) + bad_input = package/'duplicate-tariffs.json' + bad_input.write_text('{"mu":[1],"mu":[2],"add":[[null]]}') + rejected = run('synthesize.py',bad_input) + need(rejected.returncode != 0 and 'duplicate JSON key' in rejected.stderr, + 'duplicate input key rejected') + print('PASS_DIRTY_FANOUT_CUT_EXPORT_CONTROLS') + + +if __name__ == '__main__': + main() diff --git a/research/dirty-fanout-cut-certificate/examples/chain.json b/research/dirty-fanout-cut-certificate/examples/chain.json new file mode 100644 index 0000000000..22622e86e0 --- /dev/null +++ b/research/dirty-fanout-cut-certificate/examples/chain.json @@ -0,0 +1,4 @@ +{ + "mu": [1, 100, 100], + "add": [[null, 100, 100], [1, null, 100], [100, 1, null]] +} diff --git a/research/dirty-fanout-cut-certificate/synthesize.py b/research/dirty-fanout-cut-certificate/synthesize.py new file mode 100644 index 0000000000..ed16f0c1b0 --- /dev/null +++ b/research/dirty-fanout-cut-certificate/synthesize.py @@ -0,0 +1,137 @@ +"""Exact directed contraction compiler; no third-party implementation copied. + +Tekalign, substantial OpenAI Codex assistance. Apache-2.0. +Uses the classical Chu-Liu/Edmonds minimum-arborescence method. The emitted +cut/word certificate is checked without importing this implementation. +""" +from fractions import Fraction + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def prices(mu, add): + q = len(mu) + require(q >= 1 and len(add) == q and all(len(row) == q for row in add), 'tariff shape') + def exact(x): + require(type(x) in (int, Fraction) and x > 0, 'positive exact tariff') + return Fraction(x) + roots = [exact(x) for x in mu] + edges = [[None if i == j else exact(add[i][j]) for j in range(q)] for i in range(q)] + require(all(add[i][i] is None for i in range(q)), 'no self ADD tariff') + return roots, edges + + +def compile_word(parents): + q = len(parents) + children = [[] for _ in parents] + roots = [] + for i, j in enumerate(parents): + (roots if j is None else children[j]).append(i) + # Iterative postorder; the graph root is not a physical row. + prep = [] + todo = [(i, False) for i in reversed(roots)] + while todo: + i, returned = todo.pop() + if returned: + if parents[i] is not None: + prep.append(['ADD', i, parents[i]]) + else: + todo.append((i, True)) + todo.extend((j, False) for j in reversed(children[i])) + require(len(prep)+len(roots) == q, 'spanning forest') + return prep+[['P', i] for i in roots]+list(reversed(prep)) + + +def synthesize(mu, add): + mu, add = prices(mu, add) + q = len(mu) + # Vertices are disjoint bit masks; 0 is a graph-only root. + nodes = [0]+[1 << i for i in range(q)] + # Edges: source cluster, destination cluster, residual cost, original key. + edges = [(0, 1 << i, mu[i], (None, i)) for i in range(q)] + edges += [(1 << j, 1 << i, 2*add[i][j], (j, i)) + for i in range(q) for j in range(q) if i != j] + dual, stages = {}, [] + while True: + incoming = {} + for edge in edges: + u, v, weight, key = edge + tie = (weight, -1 if key[0] is None else key[0], key[1]) + if v not in incoming or tie < incoming[v][0]: + incoming[v] = (tie, edge) + require(all(v in incoming for v in nodes if v), 'root reachability') + chosen = {v:incoming[v][1] for v in nodes if v} + for v, edge in chosen.items(): + dual[v] = dual.get(v, Fraction(0))+edge[2] + reduced = [(u,v,w-chosen[v][2],key) for u,v,w,key in edges] + # Follow chosen parents to find one cycle, deterministically. + cycle = None + done = {0} + for start in nodes: + path, index, v = [], {}, start + while v not in done and v not in index: + index[v] = len(path) + path.append(v) + v = chosen[v][0] + if v in index: + cycle = set(path[index[v]:]) + break + done.update(path) + if cycle is None: + selected = [edge[3] for edge in chosen.values()] + break + merged = 0 + for v in cycle: + merged |= v + stages.append((cycle, merged, chosen)) + nodes = [v for v in nodes if v not in cycle]+[merged] + edges = [] + for u,v,w,key in reduced: + u = merged if u in cycle else u + v = merged if v in cycle else v + if u != v: + edges.append((u,v,w,key)) + for cycle, merged, chosen in reversed(stages): + # Exactly one selected original arc enters the contracted cluster. + entering = [(j,i) for j,i in selected + if merged & (1 << i) and (j is None or not merged & (1 << j))] + require(len(entering) == 1, 'unique contracted entry') + destination = entering[0][1] + for v in cycle: + if not v & (1 << destination): + selected.append(chosen[v][3]) + require(len(selected) == q, 'one parent per row') + parents = [None]*q + for j,i in selected: + parents[i] = j + cost = sum(mu[i] if j is None else 2*add[i][j] for i,j in enumerate(parents)) + cuts = [{'rows':[i for i in range(q) if mask & (1 << i)], 'price':str(value)} + for mask,value in sorted(dual.items()) if value] + return dict(schema_version=1, q=q, parents=parents, cuts=cuts, cost=str(cost), + word=compile_word(parents)) + + +if __name__ == '__main__': + import argparse + import json + from pathlib import Path + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('tariffs', type=Path) + args = parser.parse_args() + def unique(pairs): + result = {} + for k,v in pairs: + require(k not in result, 'duplicate JSON key') + result[k] = v + return result + data = json.loads(args.tariffs.read_bytes(), object_pairs_hook=unique) + require(set(data) == {'mu','add'}, 'tariff fields') + def parse(v): + require(type(v) in (int,str), 'exact JSON tariff') + return Fraction(v) + mu = [parse(v) for v in data['mu']] + add = [[None if v is None else parse(v) for v in row] for row in data['add']] + print(json.dumps(synthesize(mu,add), sort_keys=True, indent=2)) diff --git a/research/dirty-fanout-cut-certificate/verify.py b/research/dirty-fanout-cut-certificate/verify.py new file mode 100644 index 0000000000..5224da5c39 --- /dev/null +++ b/research/dirty-fanout-cut-certificate/verify.py @@ -0,0 +1,251 @@ +#!/usr/bin/env python3 +"""Exact compiler certificates, complete tiny searches and adversarial controls.""" +import argparse +from copy import deepcopy +from fractions import Fraction +from hashlib import sha256, sha1 +from heapq import heappush, heappop +from itertools import product +import json +from pathlib import Path +from random import Random +import sys +import types + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def loads(raw): + def unique(pairs): + d = {} + for k,v in pairs: + need(k not in d, 'duplicate JSON key') + d[k] = v + return d + return json.loads(raw, object_pairs_hook=unique) + + +def local(name): + module = types.ModuleType(name) + module.__file__ = str(HERE/(name+'.py')) + sys.modules[name] = module + exec(compile((HERE/(name+'.py')).read_bytes(),module.__file__,'exec'),module.__dict__) + return module + + +solver, checker = local('synthesize'), local('check') + + +def sources(): + source = loads((HERE/'SOURCES.json').read_bytes()) + declared = loads((HERE/'VERIFY.json').read_bytes())['inputs'] + live = [p for p in source['files'] if p['usage'] == 'input'] + need(set(declared) == {p['path'] for p in live}, 'declared live inputs') + for pin in live: + raw = (ROOT/pin['path']).read_bytes() + need(sha256(raw).hexdigest() == pin['sha256'], 'live source SHA256') + need(sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest() + == pin['git_blob'], 'live source blob') + + +def canonical(value): + return json.dumps(value,sort_keys=True,separators=(',',':'),allow_nan=False) + + +def digest(value): + return sha256(canonical(value).encode()).hexdigest() + + +def forest_min(mu, add): + """Independent exhaustive parent functions; does not use compiler helpers.""" + n, best, count = len(mu), sum(mu), 0 + for parent in product(*[[None]+[j for j in range(len(mu)) if j != i] for i in range(len(mu))]): + for origin in range(n): + seen, v = set(), origin + while v is not None and v not in seen: + seen.add(v) + v = parent[v] + if v is not None: + break + else: + count += 1 + best = min(best,sum(mu[i] if j is None else 2*add[i][j] for i,j in enumerate(parent))) + return best,count + + +def unrestricted_min(mu, add): + """Dijkstra on actual affine maps, permitting every gate interleaving.""" + n = len(mu) + initial = tuple(1 << i for i in range(n)) + target = tuple(v | (1 << n) for v in initial) + queue, dist, visited = [(0,initial)], {initial:0}, 0 + while queue: + price,state = heappop(queue) + if price != dist[state]: + continue + visited += 1 + if state == target: + return price, visited + for i in range(n): + for j in range(-1,n): + if j == i: + continue + out = list(state) + out[i] ^= (1 << n) if j < 0 else state[j] + out = tuple(out) + cost = price+(mu[i] if j < 0 else add[i][j]) + if out not in dist or cost < dist[out]: + dist[out] = cost + heappush(queue,(cost,out)) + raise ValueError('unreachable endpoint') + + +def small(): + rng, rows, forests, states, sharing, mixed = Random(19), [], 0, 0, 0, 0 + # Complete positive {1,5} price cubes through q=3; 2^(q^2) matrices. + # Unlike {1,2}, these include strictly profitable sharing, not only ties. + for n in (1,2,3): + for values in product((1,5), repeat=n*n): + mu, it = list(values[:n]),iter(values[n:]) + add = [[None if i == j else next(it) for j in range(n)] for i in range(n)] + cert = solver.synthesize(mu,add) + answer = checker.check(mu,add,cert) + want, visited = unrestricted_min(mu,add) + need(Fraction(answer['cost']) == want, 'unrestricted affine optimum') + sharing += want < sum(mu) + mixed += 1 < answer['oracles'] < n + states += visited + rows.append((n,values,answer['cost'],digest(cert))) + # Larger exact parent enumerations and fractional, asymmetric prices. + for n in range(1,7): + for case in range(8): + mu = [Fraction(rng.randrange(1,41),rng.randrange(1,5)) for _ in range(n)] + add = [[None if i == j else Fraction(rng.randrange(1,31),rng.randrange(1,5)) + for j in range(n)] for i in range(n)] + cert = solver.synthesize(mu,add) + answer = checker.check(mu,add,cert) + want, count = forest_min(mu,add) + need(Fraction(answer['cost']) == want, 'independent forest optimum') + forests += count + rows.append((n,case,answer['cost'],digest(cert))) + need(sharing > 0 and mixed > 0, 'nontrivial sharing and mixed-root coverage') + return dict(affine_tariff_instances=530, affine_settled_states=states, + strict_sharing_wins=sharing, mixed_root_certificates=mixed, + rational_forest_instances=48, enumerated_forests=forests, + receipt_sha256=digest(rows)) + + +def hierarchical_prices(n): + mu = [1 if i == 0 else 10000+(19*i)%23 for i in range(n)] + add = [[None if i == j else 1+(i^j).bit_length()**2+(19*(i+1)+j)%3 + for j in range(n)] for i in range(n)] + return mu,add + + +def examples(): + rows, certs = [], {} + chain = loads((HERE/'examples/chain.json').read_bytes()) + cycle_mu = [1,100,100] + cycle_add = [[None,100,100],[50,None,1],[50,1,None]] + cases = [('chain',chain['mu'],chain['add']), ('cheap_cycle',cycle_mu,cycle_add)] + cases += [('hierarchy_'+str(n),*hierarchical_prices(n)) for n in (8,16,31,64,112)] + for name,mu,add in cases: + cert = solver.synthesize(mu,add) + answer = checker.check(mu,add,cert) + masks = [sum(1 << i for i in c['rows']) for c in cert['cuts']] + need(all((a & b) in (0,a,b) for a in masks for b in masks), 'compiler laminar cuts') + need(len(masks) <= 2*len(mu)-1, 'compact dual support') + rows.append(dict(name=name,**answer,tariffs_sha256=digest([mu,add]), + certificate_sha256=digest(cert), direct_cost=str(sum(mu)), + largest_cut=max(len(c['rows']) for c in cert['cuts']))) + certs[name] = cert + need(rows[0]['cost'] == '5' and rows[1]['cost'] == '103', 'credited chain/cycle controls') + need(any(len(c['rows']) > 1 for c in certs['cheap_cycle']['cuts']), 'cycle needs joint cut') + return rows,certs + + +def rejection(action, message): + try: + action() + except ValueError as error: + need(message in str(error), 'intended control: '+message+'; got '+str(error)) + else: + raise ValueError('control accepted: '+message) + + +def controls(): + mu,add = hierarchical_prices(8) + original = solver.synthesize(mu,add) + cases = [] + def mutate(name, edit, error): + c = deepcopy(original) + edit(c) + rejection(lambda: checker.check(mu,add,c),error) + cases.append(name) + mutate('missing_restore',lambda c:c['word'].pop(), 'arbitrary-dirt endpoint') + mutate('missing_root',lambda c:c['word'].__setitem__(slice(None),[g for g in c['word'] if g[0]!='P']), + 'arbitrary-dirt endpoint') + mutate('wrong_add_direction',lambda c:c['word'][0].__setitem__(slice(1,None),list(reversed(c['word'][0][1:]))), + 'arbitrary-dirt endpoint') + mutate('inflated_cut',lambda c:c['cuts'][0].__setitem__('price','100000000'), 'root dual capacity') + mutate('negative_cut',lambda c:c['cuts'][0].__setitem__('price','-1'), 'positive cut price') + mutate('duplicate_row',lambda c:c['cuts'][0]['rows'].append(c['cuts'][0]['rows'][0]),'cut rows') + mutate('typed_cost',lambda c:c.__setitem__('cost',True), 'canonical rational string') + mutate('typed_row',lambda c:c['word'][0].__setitem__(1,False), 'gate operands') + mutate('parent_cycle',lambda c:(c['parents'].__setitem__(0,1),c['parents'].__setitem__(1,0)), 'parent cycle') + mutate('unpaid_cut',lambda c:c['cuts'].pop(), 'primal dual equality') + c = dict(schema_version=1,q=2,parents=[None,0], + cuts=[dict(rows=[0],price='10'),dict(rows=[1],price='10')], + cost='20',word=[['ADD',1,0],['P',0],['ADD',1,0]]) + rejection(lambda:checker.check([10,10],[[None,1],[1,None]],c),'ADD dual capacity') + cases.append('forgot_half_ADD_coefficient') + for bad in (True,0,-1,0.5): + rejection(lambda bad=bad:solver.synthesize([bad],[[None]]),'positive exact tariff') + rejection(lambda bad=bad:checker.check([bad],[[None]],{}),'positive exact tariff') + # Independently supplied crossing cuts: acceptance does not require the + # compiler's laminar form or reconstruct the compiler's chosen certificate. + c = dict(schema_version=1,q=3,parents=[None,0,1],cost='8', + cuts=[dict(rows=[i],price='2') for i in range(3)] + +[dict(rows=[0,1],price='1'),dict(rows=[1,2],price='1')], + word=[['ADD',2,1],['ADD',1,0],['P',0],['ADD',1,0],['ADD',2,1]]) + need(checker.check([3,4,3],[[None,10,10],[Fraction(3,2),None,10],[10,1,None]],c)['cost']=='8', + 'valid nonlaminar certificate accepted') + return dict(rejected_mutations=cases,invalid_price_types=4,nonlaminar_certificate=True) + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--emit',action='store_true') + parser.add_argument('--suite',choices=('small','examples','controls','all'),default='all') + args = parser.parse_args() + sources() + result = {} + if args.suite in ('small','all'): + result['small'] = small() + if args.suite in ('examples','all'): + result['examples'], certificates = examples() + if args.emit: + (HERE/'CERTIFICATES.json').write_text(canonical(certificates)+'\n') + else: + need(canonical(certificates) == canonical(loads((HERE/'CERTIFICATES.json').read_bytes())), + 'complete typed certificates') + if args.suite in ('controls','all'): + result['controls'] = controls() + if not args.emit: + expected = loads((HERE/'RESULT.json').read_bytes()) + if args.suite != 'all': + expected = {args.suite:expected[args.suite]} + need(canonical(result) == canonical(expected), 'complete typed receipt') + print(json.dumps(result,sort_keys=True,indent=2)) + if not args.emit: + print('PASS_DIRTY_FANOUT_CUT_SYNTHESIS') + + +if __name__ == '__main__': + main()