From 743475296e3ea35461aeed1ec25d0e5d7c6ad070 Mon Sep 17 00:00:00 2001 From: ross Date: Sun, 18 Oct 2026 18:10:23 +1100 Subject: [PATCH 1/2] Prove direct584 commuting-retiming obstruction --- .../CONTROL-native-entry-base.json | 108 +++++++ .../CONTROL-native-entry-extra.json | 108 +++++++ .../PATHS-base.json.gz | Bin 0 -> 15345 bytes .../PATHS-extra.json.gz | Bin 0 -> 15345 bytes .../PROOF.md | 164 ++++++++++ .../README.md | 97 ++++++ .../SOURCES.json | 48 +++ .../TASK.json | 66 ++++ .../VALIDATION.json | 205 ++++++++++++ .../VERIFY.json | 24 ++ .../exact_algebra.py | 153 +++++++++ .../verify.py | 291 ++++++++++++++++++ 12 files changed, 1264 insertions(+) create mode 100644 research/direct584-commuting-retiming-cover/CONTROL-native-entry-base.json create mode 100644 research/direct584-commuting-retiming-cover/CONTROL-native-entry-extra.json create mode 100644 research/direct584-commuting-retiming-cover/PATHS-base.json.gz create mode 100644 research/direct584-commuting-retiming-cover/PATHS-extra.json.gz create mode 100644 research/direct584-commuting-retiming-cover/PROOF.md create mode 100644 research/direct584-commuting-retiming-cover/README.md create mode 100644 research/direct584-commuting-retiming-cover/SOURCES.json create mode 100644 research/direct584-commuting-retiming-cover/TASK.json create mode 100644 research/direct584-commuting-retiming-cover/VALIDATION.json create mode 100644 research/direct584-commuting-retiming-cover/VERIFY.json create mode 100644 research/direct584-commuting-retiming-cover/exact_algebra.py create mode 100644 research/direct584-commuting-retiming-cover/verify.py diff --git a/research/direct584-commuting-retiming-cover/CONTROL-native-entry-base.json b/research/direct584-commuting-retiming-cover/CONTROL-native-entry-base.json new file mode 100644 index 0000000000..cbba0b74d9 --- /dev/null +++ b/research/direct584-commuting-retiming-cover/CONTROL-native-entry-base.json @@ -0,0 +1,108 @@ +{ + "class": 0, + "direction": 268, + "events": [ + { + "registers": [ + 47 + ], + "section": "start", + "index": 47 + }, + { + "registers": [ + 436, + 47 + ], + "section": "A", + "index": 3857 + }, + { + "registers": [ + 437, + 47 + ], + "section": "A", + "index": 3858 + }, + { + "registers": [ + 437, + 446 + ], + "section": "A", + "index": 3899 + }, + { + "registers": [ + 446, + 437 + ], + "section": "A", + "index": 3900 + }, + { + "registers": [ + 439, + 437 + ], + "section": "A", + "index": 3909 + }, + { + "registers": [ + 168, + 439 + ], + "section": "B", + "index": 0 + }, + { + "registers": [ + 150, + 439 + ], + "section": "B", + "index": 1 + }, + { + "registers": [ + 150, + 554 + ], + "section": "B", + "index": 12 + }, + { + "registers": [ + 150, + 56 + ], + "section": "B", + "index": 288 + }, + { + "registers": [ + 56, + 285 + ], + "section": "B", + "index": 544 + }, + { + "registers": [ + 282, + 285 + ], + "section": "B", + "index": 545 + }, + { + "registers": [ + 285 + ], + "section": "warp-B-entry", + "index": 7 + } + ] +} diff --git a/research/direct584-commuting-retiming-cover/CONTROL-native-entry-extra.json b/research/direct584-commuting-retiming-cover/CONTROL-native-entry-extra.json new file mode 100644 index 0000000000..cbba0b74d9 --- /dev/null +++ b/research/direct584-commuting-retiming-cover/CONTROL-native-entry-extra.json @@ -0,0 +1,108 @@ +{ + "class": 0, + "direction": 268, + "events": [ + { + "registers": [ + 47 + ], + "section": "start", + "index": 47 + }, + { + "registers": [ + 436, + 47 + ], + "section": "A", + "index": 3857 + }, + { + "registers": [ + 437, + 47 + ], + "section": "A", + "index": 3858 + }, + { + "registers": [ + 437, + 446 + ], + "section": "A", + "index": 3899 + }, + { + "registers": [ + 446, + 437 + ], + "section": "A", + "index": 3900 + }, + { + "registers": [ + 439, + 437 + ], + "section": "A", + "index": 3909 + }, + { + "registers": [ + 168, + 439 + ], + "section": "B", + "index": 0 + }, + { + "registers": [ + 150, + 439 + ], + "section": "B", + "index": 1 + }, + { + "registers": [ + 150, + 554 + ], + "section": "B", + "index": 12 + }, + { + "registers": [ + 150, + 56 + ], + "section": "B", + "index": 288 + }, + { + "registers": [ + 56, + 285 + ], + "section": "B", + "index": 544 + }, + { + "registers": [ + 282, + 285 + ], + "section": "B", + "index": 545 + }, + { + "registers": [ + 285 + ], + "section": "warp-B-entry", + "index": 7 + } + ] +} diff --git a/research/direct584-commuting-retiming-cover/PATHS-base.json.gz b/research/direct584-commuting-retiming-cover/PATHS-base.json.gz new file mode 100644 index 0000000000000000000000000000000000000000..8d33a0ac7060bbd79c520d28d607bc67aa83a24c GIT binary patch literal 15345 zcmb7rWmud|vNrDS1a}GU5@ZM#+@0VS+$G2`XmE!R2=4A4Tml5w;1XPe`x(gl?(R9e z=Um^%k9qp3mTJ0t?y9=0hb$Zc;`tBi=`ejMYLhQ6ZzZq%LF}Gx-|mVV&WAmPh3S>n zIh1~6FI0f%m6@r$MP9h1s><&e*@)xnYEz162SGQq$dEq2yHSJ34Zo+m%& zHxC(4kI{aQ;1TTop7!mZj*|_1ZY%otJn_j&Ql3t?&sg9oD0eZnBTlNwRAjK%_xqh5 z8WPN`R#bSzQX5ikLrRSlDW1+oW43Tmet@ihxXk|U zC7whncYG6Pawhv`4}Dj7#drE*H{=j5Wi_>;)BF&ZJNtpMbOoVGY+!Pu{o$cP1V-!0 z!0#sX+TQ!si6^4>o(JcuEmo`c$t8ow0%VUm_F@XzVo=jsa2{!up6f@dyqdX5f3mEG_L-aSV6bb+($0Pvqx=2)!)Obf88~ z%#cnvg~gCDzKAgxF?aIwd83WCeac!G)GV4(kr3INs<0dOGTU&g%jkYh>cs`iJgrbL(eAzTbI~zVQv;zdTrm$cBKtA{g^l^l);s}x-HC2WG z(v@Gin_v?bz4OX?zK}zc(99q|Sg!lqb!bWe(y9UsF%RXI9%LpogmDyFDptWkB4$_% zd|;To4u%(IAcrS>U{{vr*X3wrgy(`JeY}?_J+YTr;QBAfEQg&$%t2E!45Se7YVvs; zt)f>dM1-@pL|me}n-ZgU~=;o&(hR1_)gIy_vN>Ccv+UJ%U&6~ZxK z{;;cLaHHx$ra(Fh^XVh`Mx26a-pavgyx9cLd22-GMR=Lj5D}NA!>i+`tdGo4!AAR$ zqU*D-IGSx>5rvL;38L6IRW?CYim&vrSSYAP>8oSN6TJDR_-x{5cIWJHZ2jR^O^-KB zA?OG!L9(pFdA|O#Ybpv-qXXYa;l~p!SScn;;&y8&3TJjmmm|V>v(!xQ*p{g46bfH>Yb1jk?{B4fLVTrBY^BFU)LJaAl_6*BZ!m@D5#JQR!1&h* zziO>&XVRCPtul8ojjR1#hA9KzRO?5lOUhkn@I8z#rRcE*%Q&}TinR#cny3fkI5CDY z&@yqg>C*u_>C!q5kD8Y{Yp=3n`lStgnqJMLN{~B#AOuX6N}$vi-t>KwCxU+5Xx2bDXt2XS+Q?khhfafe9rVZRQWF1SMx- z-^OLD(f-Rt8U2AvKx_n=UPr-H5|nDVUq+?%(I=T+Mhn=q81)P0@pE)`m=#22joM{o zios7XHS4PRLhO^E&v*r+wFr}OPieHB?Y0;+9+Q#?5R;5hFEY6DP4v9W|y=zp9f+7LhT*a8pO%5>?@heZSvTpjCKl+QUS569X$kF1Q9Q zjz^9h1N+ew&}A9QB#JjokIYmJp$!BV4`N}_UJ7#b$Z!5BOCgVi9RLxU0sizH00~t? zgj0g+*>adVoSw%ZM|S%T#S}6CW!f27O>V;f4;6hc)nFBk7kH+AOIBM`ATn!6RZMNl zH12d_RKNOQ3l>T_ks)sKW_xs?gg{BOF<};+M(l*^6<=)$K<;wiu1wcGvYoT;2<2 zTlGVy3oOW2?E*F+z;*-~;z$*u z02(2Z4;4rW0VN7yDFVcTXtvmPG*Rba!eYi~qZjAIXnRWr(<2|y2(^9$Y&0VLAiBtn zX^{jwkoDH6SJnh48A%LhARUQck8X^Tpp8fJv`92u^hj;MNX;LwbEl3ytN~UB#;HII zjTfaBL9!xJ8HIO@GDZ;BiNG?mH=Q7|n?T;s1zi%^WRmd9G9l<2H;<1;SfUxs?Gffq zpW!s1vn$G?I)}ZI>HtA-*`LJmpmHuyp+df3aU3?C(WMwgC{Z#6O;L0?H4g!jjKZ)L zz@)e~sd~fJQEwpA+ zFg_&1m8m!Gu=W8U!W0%Dh0&8nf&l}HB1ga;;l8D~xIqg0c3>^IitGGA+?gilyF@gC zlemfU+FeIJ!vI1r#M-%F<^R<5t;quR9dy=D} zrHQ0h+qIem@ogAuaw3!=JY7>5%-PHeSv#1@5n6I0)aDf8kRRw@XL8uVXF^R8LEwt~ z5NsCwjrTU&u{l^hJ0q<7^n9 zIA)Jo8W$V$o2U2LZ2hKJIc|VrlZK57Twjh0db`i7i-i{D_6H6WyYAx4R&`rYkdcv= zhXP*T6xVjIzh08hy!v5HdQs9Y>3T#MUzX0Z?c=IbpvQZ*eM==P|7QEF5$|xY-V$M* zqfZO`6!`$8OxRZxG|-N=f44h?ScIxig`=3c*5u}}>pjR^t69^Al}627=eGz6DpT zSz}ikE^U5574)tPCie>9W{b^c$NnS5st@15 zg6e$1_d9;nQF--h6VzNpqLK9{q zJO^iZq6*)oNAff#5T(5IkdzH}A-s~X&uO$*b~Z|P2v z9!{~hqejLs(P6@ecHnx_>`gcN+O4)7mw!`6=7Y^8XP;XYiMoxHKUK2Sfx*5}dWVN( zvllBs6h(6|W zl3wBOBoM16bd3+%X_^$I)x>gFBmjCkR4o2{7`&kw5We3w;PGD>yCe|_iCg;Vv+DqP z#vZGAT`D;qvIyp2RSA1nkyjf1xjc&Dfh@`4wj)geY}UI;W`O zWnY%TnOX>ouy8W0OK-o6rl9*wwPl?8gu*{AFC@n zGg~3jGTEwW2Qv>=c|sHiVu^Ij$Pm&6cw{^;Ni)*V%|wMWJgqGUmuRm6Iiv9O^jb&sem77$qdt#X1TM zBW{?kSHRognQ$hfEY%&gd{r9`@Tl-0<946<5g{IRq$12iHRI%qP;#kr3*NeT(B35a z$~NwTT}(g0Md%i9g`$YJ+GC^a7oDm%rPVph3fIL0lgqJzthsZM7_5QxhRklT8u_h@ zdCWK=gdC`xroj}WhSCwN?vVNfaQeh>`cN(wK(y_l+BU61$5#pK<$!3Y=6FB|1-wug zsSu$Hfzw!y(#EuMSOB~b(#{BMdUs3!sYLWw6oFyx9p%E)J^Eg~08&^Nx&X9z6fYbh zFOD6y@0n6reI+?Kny6klW9cZ(18U;=lpLJbaGYo)Gq2Q`0=-4 zjfIk^1$vki6}MIpp1RskSnsWck_xN}YTwRHVz>oYQrI96b=8x~;`ZzEFMF{(1;aiD z`K=jT&%&W-fg6A1c+$DXe-RNm7<9Iu9DlzLH$r|Etmq(pMb#yfn=FGJ%Ek*wYOwho z?K-8}SASIn4wZJFLnZ8$J;AOM^(#jPy!3rB3AB`;<3Rd|y*7+&VoJ7>5^reD0t%DZD!QS$zzB&x zN^p_v7s|_2RBsv_n7*2v%GtGaQe1^@AQs)rGcG6>*}&&H5lCKgFeRd@cs8g-1*?cM zG|DrKxx(xp#D~MjSH|4?AzX7Y-JFrDX;Y`QN;}X)Cv>uyiHi7eeBFi;z1=;Z96c=P z2R2ITahkg+IR1!X>ER~v=y7F+y`G_mt#Mg}C8<(=LrnoVz205#JYWm!Zwc$~W28>x z&=X2p+w(u?QxZa&4%l;ix9cCn*MLKPl$g6Px65Nk%2-s zab#~ns~7le4VGW5K|lH*Yk&=xf&d2S0EQrcsTVv)2+;ov?*j;f0Dmz4Sq33U{cJSy z*apCc01{lRlqE3Kc&-QA48j+<2eQr4pm6+~H2|x4wgF%jknS^3hZTbLX~rjNC@Bd8 zjBBOrn=im$g9QeDxY+JR#W7!=J3^C|xhTf^oQ~Kbs>=dLT{^a}%2YqYdrZ6)BmBh*%f1(~~^!r_HX@h>H(4O@PHxxr{K# ze2%bAeA3d$XWUPE#(h&I9`Pp_+y14b45x;?uYoyU8V7U?Z4EP{gz{5Rfwq^?){N7k z!@Ws@EcHx_w0HcWlbE%@Oe+i=(J>mn65$F8O9Cgj0exI2%okXv-NXW;zvz+NfEgJ5 zfs3DGUW3sevgwR`8yo>W13&F13b@4z1WpJ=GH{V}fL-vD>UbOHh;Bi4$U{*Q_DG8& zUkfZc5;%JKIvBP19zl@tpm45&hV$aYD1up)&f6!{)h#)5zJHzb&({&( z--kNnlf}LzGWrmTH!hQ?bRJ4C$&^oq6{LOilRi{QL$nU!0u`0O2p>W$NC{W0m&F+~ z&DW6r@~lN7unJ6MDbTrTKLEXEU(`DuzzFMB(2W*=R*a+WC2&x=kSUYZzrTUg zf?A9-myRYF!C9!Hw!2%|%@@EJL|PH8n#NN&K~-sDx6U$0vqj6n8(Y-Hn*y?AU&u7g zn%YG zgZ);JqGV4udpAQA0UQgk6<>*kI;C}#vOHYqRRqUK418rVJTL0VpgwCXL!Z4Wdbg_Gt0!m= zaM751E-Ia-hty~lXJ=Bd(CFAPg-Xgs5?n;qwl<0o@_s{7JU6|mJ)Q6rlakt;-!FvC z1H{83@&~{b2@I*80X!cE4)VnsJO=^+p??Pgi2sm5{~ZWq{v8OA8pW`^rUbkHoJawI zf4lwv0`xCN0Bj?`Dqi9Qu!==J2?TgcIS%DqByLLNTpdnu{nmsYDg0oib|_oJFX+``Db>*U1nNbnjRVZPgPGzn*tQdh_Sx-u#Q%dV5UiQ zk=z&R`Uc;Z<6pr)wF&=!0sp9f0sqlMF!;CpPw=lOlIzCTHD{?`bgVMl5}qFgq(x=I z!pH|?B7j&rwJ$tT0o^g2qDRFsvM&hFNs;XT$MY|Tc=r4i0`;{23I#@91S5fIuwctT z1YBnW8;J#IeselU#%A|E&waJ?N|9-&F3%^#Z4f-HTOf&|nUo!CAPKIU+QDqxXRm9v zzN8{-VWF;qYm?>90`s}4PbJQzV!hU(Onv)E}%bUVBd0p5HS&bmq->4aKe|~Z0kF_Vw6?MYzEpkDjYfv9oG$B zYArGsqP$ooE+Pb^vFp?9GdLOpvF8lkwx>G4|Z^KxD} z5XpM!9Oz367WVT0i#HzW;1%Z3eeAGt?9e5c(BF0*TimxF(xdV83yjPJG!!kqL-7MH zP|ggHfYq!`oGqj>mbnijQ3}HGKbyF_7zCOg1m}Mj0>XB1k6}um$^!{@nJ;AbHk$Qm zypjJVb_R=a3@@_23}v6ugpZ(zy0yab-EbMJ)V7XS*~|k{R*MR1eYL)s#iHbaU&WfksQPL zd_M6phpP54tm8QD3C$XI7W>UWqn8|+tK0LP{P4Hm3RzmcuJ3;r2=OTC;id+$0Dyc! zW@N(vh-FqFNghze;fqStSPUgN`T+ewAj^&E zn^6e|m+!lA?YXjFV}_;8`?5zEJ`;)rndVnSnU?24L=)y2CVgwpq~Zw+p{AxM714bI zbyoAAC>pkZrDzU=|4=mD>2@a$+s_nDnUf@+!>bpH=HYM{$csV2KE%%-*oj^1ctr6` zv;_EcL0FUj@wP+%>1|WLp!PFu^G}&!$X_0~Bj7LZU8sxP_{A*;L+*dzUj74Z(@|C> zdbf{8RY33t7n+u)T87WMk&olig>bY~ywNx5be-)AyEfy8Z{HkCeNNaRy~F13&*SsnAQtW5zenX^Y~Qv;|EwGkw+!-(i%Cg_N#wcTU|RAHh9aaxfq)dAEU5fe_=p zD&T)%V<=dd$*8m zaEj9%s;Gr<@hF4AI~kcIja9!@?MkQO9n?m{9;oxKW^Va&KIs4}e~`-0P*vlMFQv0I z1uf+~#vGj;YHDVbPv@hmVvgS%F) zgQGy4(SJP~jMhM5(1 z#;MwvKqoB@eYpR^=zQQPPuFhd$L^KIM50!S+jhF53bUe2o1Ag&tIa5u-}o*O)6iKQvxy(_L5rY9Ocsv34MIBQEd-XR7i5fs z_t*lA=dmcMLagpNPZ^1RgSM6vPwDzQPpR-;9ZnP>Wa%URUiN>ZN6Txa*|+xf9aM>`(X=6_r{X9z z%3D^bwx-Mw_Fs%+cQfS&XbV*n<69EZl};@xpB$XTkECk*hec!t)^867=jval&wS)M zG;j~I%j+Bzi-$$~2pO^_2PqA)3oF{iBi4Ym*#_;|D0wtq<`Uj&r>Y?hc;CQ)8LK|$ zS;F>)>evd11LVSwIf?jdVuV@go!NV^;fze=5QyX?@NvBv00WHYG3Ge!Ch*U@HANHG zUS~252%>v7axPDdU@(DI&4_lTL&iW%AOiyhH&_l)`m^^2MUnKnhqznyRQw)fT?2a4 z*=@Hm<661i(Mn^*1yUc2#t}$v=@U#C@yDJarNM7s@GIH|McEN<^+r_Xj@bs$_-xz?G_qiI*f`x)VIgGdW&gyO=5RXqTmtoyD?dKLdQ@zsAnt~=HYFxhhCq?mI@RonOEGn zeY81($6SgvGEt|ATP*f_-XHtu^T-^29(8*x6B@g`ep@pphap+(6X;P9h(jU%8rC{5 zq8C0KU3LVYi61%*si3RK;e&%#=yH`PHyrY~Cfyng;@jtVi>51Fs7qsV~~ z+!8K2%W7G6*=X%`O(kz78xsn0cUR|zpRpNo!8f346`=FEnNGWsjndgNJPNWwY7o0Z zXBW7kUb|9+YN^fI6utwaFg+ixLXhe{ei-^5OY-K;n(Xhc6B$uhq8c#n6L^7P0 zNwo)`90c4NM*o!y(KG#%3#r$~pZ<&c+D!pp6S$tfP@O@F$2~`><&RVW=R=N@9e$ow zkzA?b7lQ5VSy;=kT-l?~VEK2t^6fGX<6cB<^%X36zf0MZbPO|;AaDf4G0eQD~Rp$Mv*UleInRrc_n$~vV z-qu5-QEpbq73uz-MH^gUi#RaTdVIBc?0fTt0X6}&kN~AGRp}<&2SvsIEhze|{ck~$W2TpQG5qvK+ypd*qZ5O)3(+pmAUHdsjA-Ye)&(}bhBSo~ zMx{SP>ws=sqYa#naL+Lj)k{qDP3Uh@i#o#pIn@!-MNar4dSSIv)Iz{vksJdGG1x5s zl}4GP_`_-eo)ag}W*bbB)lmL1+a2D2!l+9`=;4s(;S#za{*5D(G>Ty-dk&&rEdHO2 zNgmt()s+r~?WKb%(w||$X_t(@I)LYfGzRz6;Ii2{tTVbdlc^L-izdy*ho9rohR^^- z4}DhA$)A7t0p`%6CWE~`{IJki5Q(_yjqwwn{XR?|=Z8T1Z$T-fyn z@Dh})r|!O`lh}SjHCXxo2(kF!{|>RD$n-2j$F*7D@v|OWd+Dz(z=r(eJn!qt0%KrN zgz-rb>#^jkH|hc6+?lWBoCtZr^xC0Ce9A*3OGAKdg>lOg(q*}?^TVYonwaA9JYs`}SW$c0RT;VG%Q_+!&#**MkEtCkts?I3-n@zDhECM1 z+no2Xw>Me$^SpC4sUGe_MIk1X^useKarNBbu4@Ere6Vw!chOc8u;rYlebSN=n)aTo zmrFL&kIA5HRf`3CwpCh};opAjq6vPf<0{6~2vdScP`T4hVGJ?Wkj@KDD7!{ai=lqL zh7*a|=`Mz&<^j$(u!QJj`ie{F;d$(+dPr|4!oL3;sJU*uit7RUUOTI+>vgi$iZ{9X zTA~pp2gbPirvZRC2BvteSWrkPIc4aM93>L?6$Z0R36p{{6oFD8J`@Z53J`y-W+(&< zCC^sg>iY%-vCjt|9%Bo{l zm}LUU649Z?J;t{b$^@2$yG@ld&R>mEQ6>)}`W9d1^S_zt;2?0mG90$7bm!W{I%aD& zk%fQdvIW%;=pFj>`KWT3&XlW)`dmOpik9W;!Y z)(2-sSmTcxM%tJ9sWB6d^=YW}Uf@CI{bM9lV%5*%`kxEH0aJ1MxKp5M4-v>zoTHq^ z1f*#<-b$e9LR#^V$UEp@Bq}vFo*IQjf+9fR!bW>w$j8F(DFxq+Vt^SkktS;;phrY6 zpRgtKTxhWL)gg!mD#G7J=35wr_ExTR6jRT$sF{X^H%D+nuH%J2Y<;PlFfo|^yRuK8$aZL zZ}i!Evi!NwN0!L_`^2Y1>SX*C?zQla&)8i`^_BnehEQ8H$SF;he|=q)Kbv^AP?}yU zVMB_Ut$T1B?X^^h(;H=e^GwuQ1K2~%9=}D7~v@B-v%gt0BiXmKCqZzeXSS zvZ$Y2Spzt}{;Xkoj*Kpw9j{1fm!4|FWu2D^U~qA|?)(_rKqZ(=?a?@Q?QM5K`&q%ydZ~pbPj-`VqfSDFZi~#dc+2Zb&AGLyiiH!S zThx-SNi;;Kt>X^L=y5Lc3w3Fd6}Ry$X4@8s!;B!euF4u_dEW0dsNIw`>Wv2cw87=x zk`vVwzGY1Pv|_UmYNg7Z7h)mSB6;@*xxEmbP^lWTBs1N^WROL*&G~^mv&iFn&FM}( z0-`0>k4&Sc{ADakRbsGIw3e<*%vNVzP^qw7W##)7AvKUiVD%JgQRi{RLiFTPH9rOddKpXSNdNnzWs8FD0=5JHWNv6 zpp>qMQu#>Vn=&MP#9B)b%CSI}DwKv&QIunz6ADCmeL^8G_#2Y13OqOh7P-_P)Z^b92yoJATD4Xw`JEsv4KXGg3E^b~y2o zF^QQNfWN&SO0tMQ2HX3znEQiZn{DKfeZ;r`H}G55baf6b(;Lq#t(M$f*-+1JWb#;!D7Y#^aCpOlbpL2x^pT~E@(=SoExMT zGk8!7j(xzFF23y?)V4+(Dg6o}DTeNa_=3>8ntLPTsU2K}I!@NX(}(rEiTe`}*&+=D z9;NiWgm2B}=Wo8&YAM^r)duH2e68h^HBV2Mw0h(matvcbgM2<_d@xG>lsY*ePh?&~ zEHQ>BPAf;zF`>hAF>v0_4r8$|LA2zz;BPj1V5=s@@ie^gyt)U7@e1Z%ZF>(nEn7_B z@e>lyG6h@i2GKP=6FK@O1<5gl`sHP8lyrZh3kn`oKu1iJ{VEmwZ&A{TQ#7SsGk+Ix zf$}`6ZfLxHIT)zh)B{>xf?P9lF3m+|sufB|prxg%(UVPxF`DzsS#*423$QUoZvo_YPedTacA!?}Eh6yz&DD5ey z3b{zf?UUQ`Q~Mp7Aubu3mJgYR_DApl$kvMH-PM=gk`i6&&WdU_Wj}Y;(!!~{`K0^x zCt@WQ*!7bgrk__Jnr5y*EK$}vDqOz)$vi&lT9dpo*_DL%W}sVYCANP6F9!ZOcxGZH zKlVw&zkLm@)Y}22Rn1FvaG<*RG;sRLNWH)=^qQcNQ6sVUJU2>De4bFRS zCY;8G46zXm(-%aLo+WA(N=^xkiEO`ClJT4>6kdekDPv_XqNiB@=gp_U+zGV9{OPQv zI8k~866iEo2Y86&SRd?VvO&I8GH2qe0U>Aads2D4w<6(Tt*g9Qy4O+-Y;CI=a?PIj zdt1L?MFt!PbH2FSLe-oj?cjQU;EmSkjP`I|MQtTXr+IK)+lV!F`AM5>nu1_{Q2WkR zPb!E!?Hd~-Wnm)(BTqf7Dg!G)dpj(0aQP!5a{hb03?}-Aey6k|e4A>+@8;MRv$Sa6 zV43FQv2#0vAi%4Ru}KQzY9uBfm`98&!vC|Vl+yX{MZxP%t;$ONycLTQF$5YfElRBZ z7Nod53$WtRUiPj9;km@m573bl_%jBDbojgfw~gt^g?^a_3+TBtq7VZf`Y)}|O1>jb z7)|&;9{?wGfB<-S@Co_u16VZZI$Xj3M%nAwje+p%@)#SkKV5wB9aqaiw-C67DR`!^ z!(OZ*W}%(#aBB^I?ecgYk!kXEre??CNGb;33)?|ej3tmIFtw~=xgS8@eRC3w#9(rx{$3i4J>$PC^+h0?F@6M@eYlLEP`ehfD@+uPn;?- zB=@7k^Kv8AG#s8$oF1zV`uW48GM$x`N@iIy*dO{5E!Yf+Y$gMw~%T0kurexb$5BZsd)w-Rg9wyNGxz}_?GC*mho z!2WPayzRgzU&vdKX_hr8mPk7l@p^QpgJ&)uQG#J0mf0s&$zCJ%pm8#=S$D)K>@)4u z0sjcQ6j-1}jfXF!x(E=l?RVVdiIeNo=u_^x)51Ku(vZUFZw_mC#nKmjk8M%;T4pmgmuX zPjdyC0NY9-y80#uVw<74WgVQ;8yA>!*F( zT^ih?GHE)fm1Rn(<%~2Ka0N+FHm@_*J4r9CeAn6-Y+mQCepIbo6}ySR=~4gvnLoT_ z^A&$dg)MtI@sQINeCt|7CgVr z8#UW}&g<%m9QS|v=2a6^qSm`><9}}C)@CrYzOI}w&ACc>{s5mD+lA3#?RwkjhO(4K*F$29 zg{0>r5QE*or1p7`b9*rUtOk5&MnBn>JHs!?EoS3PsdOA3CxEnR?S7fndTa)*SG9W( z$kF3O4=F4T4sqzAYN-v^Te?tH#**m}`vIrII{KMUFn%ULy?GpOl z?ew*aJggk9utsY_$Oy^c{`*_y&Eo|-ptzgB9}4wv^W_~E{r@Q*AXIzFr!R5j;u zpqnzQ_G@EIwl?=8B{QrWCT>k9jG32w-I{*rq55*nRgpjHG`gmnstMlzf{#}3msqWt zk&W?sxGIh+yDrd5LF%cRoMK;=d{Q;9u%i!VCtFiRhWG{K&z`@WHatH{?#!64Bx}g? zJzb-5S?~n|UfK&*wkV$MxvjHT8YrH9cx2j^=KWCu{;olhdFWb1?G zyi6Mlww9RRI#%kZ6CCI!0vp$A6T+FOA-3jSA2KmsY$(wy^&--BVHn#8?1kBxcERsK z!Nb>f$FurHvgu@;Yy`sT&jP zwsmedYK*1T{?t z;B~_s^N}wOX+#$zY8f~^OeKk;;r*t+F<*Z3wQf#g;3s%LE~ED|+`0zcxrW$*dK5z< zNj= literal 0 HcmV?d00001 diff --git a/research/direct584-commuting-retiming-cover/PATHS-extra.json.gz b/research/direct584-commuting-retiming-cover/PATHS-extra.json.gz new file mode 100644 index 0000000000000000000000000000000000000000..8d33a0ac7060bbd79c520d28d607bc67aa83a24c GIT binary patch literal 15345 zcmb7rWmud|vNrDS1a}GU5@ZM#+@0VS+$G2`XmE!R2=4A4Tml5w;1XPe`x(gl?(R9e z=Um^%k9qp3mTJ0t?y9=0hb$Zc;`tBi=`ejMYLhQ6ZzZq%LF}Gx-|mVV&WAmPh3S>n zIh1~6FI0f%m6@r$MP9h1s><&e*@)xnYEz162SGQq$dEq2yHSJ34Zo+m%& zHxC(4kI{aQ;1TTop7!mZj*|_1ZY%otJn_j&Ql3t?&sg9oD0eZnBTlNwRAjK%_xqh5 z8WPN`R#bSzQX5ikLrRSlDW1+oW43Tmet@ihxXk|U zC7whncYG6Pawhv`4}Dj7#drE*H{=j5Wi_>;)BF&ZJNtpMbOoVGY+!Pu{o$cP1V-!0 z!0#sX+TQ!si6^4>o(JcuEmo`c$t8ow0%VUm_F@XzVo=jsa2{!up6f@dyqdX5f3mEG_L-aSV6bb+($0Pvqx=2)!)Obf88~ z%#cnvg~gCDzKAgxF?aIwd83WCeac!G)GV4(kr3INs<0dOGTU&g%jkYh>cs`iJgrbL(eAzTbI~zVQv;zdTrm$cBKtA{g^l^l);s}x-HC2WG z(v@Gin_v?bz4OX?zK}zc(99q|Sg!lqb!bWe(y9UsF%RXI9%LpogmDyFDptWkB4$_% zd|;To4u%(IAcrS>U{{vr*X3wrgy(`JeY}?_J+YTr;QBAfEQg&$%t2E!45Se7YVvs; zt)f>dM1-@pL|me}n-ZgU~=;o&(hR1_)gIy_vN>Ccv+UJ%U&6~ZxK z{;;cLaHHx$ra(Fh^XVh`Mx26a-pavgyx9cLd22-GMR=Lj5D}NA!>i+`tdGo4!AAR$ zqU*D-IGSx>5rvL;38L6IRW?CYim&vrSSYAP>8oSN6TJDR_-x{5cIWJHZ2jR^O^-KB zA?OG!L9(pFdA|O#Ybpv-qXXYa;l~p!SScn;;&y8&3TJjmmm|V>v(!xQ*p{g46bfH>Yb1jk?{B4fLVTrBY^BFU)LJaAl_6*BZ!m@D5#JQR!1&h* zziO>&XVRCPtul8ojjR1#hA9KzRO?5lOUhkn@I8z#rRcE*%Q&}TinR#cny3fkI5CDY z&@yqg>C*u_>C!q5kD8Y{Yp=3n`lStgnqJMLN{~B#AOuX6N}$vi-t>KwCxU+5Xx2bDXt2XS+Q?khhfafe9rVZRQWF1SMx- z-^OLD(f-Rt8U2AvKx_n=UPr-H5|nDVUq+?%(I=T+Mhn=q81)P0@pE)`m=#22joM{o zios7XHS4PRLhO^E&v*r+wFr}OPieHB?Y0;+9+Q#?5R;5hFEY6DP4v9W|y=zp9f+7LhT*a8pO%5>?@heZSvTpjCKl+QUS569X$kF1Q9Q zjz^9h1N+ew&}A9QB#JjokIYmJp$!BV4`N}_UJ7#b$Z!5BOCgVi9RLxU0sizH00~t? zgj0g+*>adVoSw%ZM|S%T#S}6CW!f27O>V;f4;6hc)nFBk7kH+AOIBM`ATn!6RZMNl zH12d_RKNOQ3l>T_ks)sKW_xs?gg{BOF<};+M(l*^6<=)$K<;wiu1wcGvYoT;2<2 zTlGVy3oOW2?E*F+z;*-~;z$*u z02(2Z4;4rW0VN7yDFVcTXtvmPG*Rba!eYi~qZjAIXnRWr(<2|y2(^9$Y&0VLAiBtn zX^{jwkoDH6SJnh48A%LhARUQck8X^Tpp8fJv`92u^hj;MNX;LwbEl3ytN~UB#;HII zjTfaBL9!xJ8HIO@GDZ;BiNG?mH=Q7|n?T;s1zi%^WRmd9G9l<2H;<1;SfUxs?Gffq zpW!s1vn$G?I)}ZI>HtA-*`LJmpmHuyp+df3aU3?C(WMwgC{Z#6O;L0?H4g!jjKZ)L zz@)e~sd~fJQEwpA+ zFg_&1m8m!Gu=W8U!W0%Dh0&8nf&l}HB1ga;;l8D~xIqg0c3>^IitGGA+?gilyF@gC zlemfU+FeIJ!vI1r#M-%F<^R<5t;quR9dy=D} zrHQ0h+qIem@ogAuaw3!=JY7>5%-PHeSv#1@5n6I0)aDf8kRRw@XL8uVXF^R8LEwt~ z5NsCwjrTU&u{l^hJ0q<7^n9 zIA)Jo8W$V$o2U2LZ2hKJIc|VrlZK57Twjh0db`i7i-i{D_6H6WyYAx4R&`rYkdcv= zhXP*T6xVjIzh08hy!v5HdQs9Y>3T#MUzX0Z?c=IbpvQZ*eM==P|7QEF5$|xY-V$M* zqfZO`6!`$8OxRZxG|-N=f44h?ScIxig`=3c*5u}}>pjR^t69^Al}627=eGz6DpT zSz}ikE^U5574)tPCie>9W{b^c$NnS5st@15 zg6e$1_d9;nQF--h6VzNpqLK9{q zJO^iZq6*)oNAff#5T(5IkdzH}A-s~X&uO$*b~Z|P2v z9!{~hqejLs(P6@ecHnx_>`gcN+O4)7mw!`6=7Y^8XP;XYiMoxHKUK2Sfx*5}dWVN( zvllBs6h(6|W zl3wBOBoM16bd3+%X_^$I)x>gFBmjCkR4o2{7`&kw5We3w;PGD>yCe|_iCg;Vv+DqP z#vZGAT`D;qvIyp2RSA1nkyjf1xjc&Dfh@`4wj)geY}UI;W`O zWnY%TnOX>ouy8W0OK-o6rl9*wwPl?8gu*{AFC@n zGg~3jGTEwW2Qv>=c|sHiVu^Ij$Pm&6cw{^;Ni)*V%|wMWJgqGUmuRm6Iiv9O^jb&sem77$qdt#X1TM zBW{?kSHRognQ$hfEY%&gd{r9`@Tl-0<946<5g{IRq$12iHRI%qP;#kr3*NeT(B35a z$~NwTT}(g0Md%i9g`$YJ+GC^a7oDm%rPVph3fIL0lgqJzthsZM7_5QxhRklT8u_h@ zdCWK=gdC`xroj}WhSCwN?vVNfaQeh>`cN(wK(y_l+BU61$5#pK<$!3Y=6FB|1-wug zsSu$Hfzw!y(#EuMSOB~b(#{BMdUs3!sYLWw6oFyx9p%E)J^Eg~08&^Nx&X9z6fYbh zFOD6y@0n6reI+?Kny6klW9cZ(18U;=lpLJbaGYo)Gq2Q`0=-4 zjfIk^1$vki6}MIpp1RskSnsWck_xN}YTwRHVz>oYQrI96b=8x~;`ZzEFMF{(1;aiD z`K=jT&%&W-fg6A1c+$DXe-RNm7<9Iu9DlzLH$r|Etmq(pMb#yfn=FGJ%Ek*wYOwho z?K-8}SASIn4wZJFLnZ8$J;AOM^(#jPy!3rB3AB`;<3Rd|y*7+&VoJ7>5^reD0t%DZD!QS$zzB&x zN^p_v7s|_2RBsv_n7*2v%GtGaQe1^@AQs)rGcG6>*}&&H5lCKgFeRd@cs8g-1*?cM zG|DrKxx(xp#D~MjSH|4?AzX7Y-JFrDX;Y`QN;}X)Cv>uyiHi7eeBFi;z1=;Z96c=P z2R2ITahkg+IR1!X>ER~v=y7F+y`G_mt#Mg}C8<(=LrnoVz205#JYWm!Zwc$~W28>x z&=X2p+w(u?QxZa&4%l;ix9cCn*MLKPl$g6Px65Nk%2-s zab#~ns~7le4VGW5K|lH*Yk&=xf&d2S0EQrcsTVv)2+;ov?*j;f0Dmz4Sq33U{cJSy z*apCc01{lRlqE3Kc&-QA48j+<2eQr4pm6+~H2|x4wgF%jknS^3hZTbLX~rjNC@Bd8 zjBBOrn=im$g9QeDxY+JR#W7!=J3^C|xhTf^oQ~Kbs>=dLT{^a}%2YqYdrZ6)BmBh*%f1(~~^!r_HX@h>H(4O@PHxxr{K# ze2%bAeA3d$XWUPE#(h&I9`Pp_+y14b45x;?uYoyU8V7U?Z4EP{gz{5Rfwq^?){N7k z!@Ws@EcHx_w0HcWlbE%@Oe+i=(J>mn65$F8O9Cgj0exI2%okXv-NXW;zvz+NfEgJ5 zfs3DGUW3sevgwR`8yo>W13&F13b@4z1WpJ=GH{V}fL-vD>UbOHh;Bi4$U{*Q_DG8& zUkfZc5;%JKIvBP19zl@tpm45&hV$aYD1up)&f6!{)h#)5zJHzb&({&( z--kNnlf}LzGWrmTH!hQ?bRJ4C$&^oq6{LOilRi{QL$nU!0u`0O2p>W$NC{W0m&F+~ z&DW6r@~lN7unJ6MDbTrTKLEXEU(`DuzzFMB(2W*=R*a+WC2&x=kSUYZzrTUg zf?A9-myRYF!C9!Hw!2%|%@@EJL|PH8n#NN&K~-sDx6U$0vqj6n8(Y-Hn*y?AU&u7g zn%YG zgZ);JqGV4udpAQA0UQgk6<>*kI;C}#vOHYqRRqUK418rVJTL0VpgwCXL!Z4Wdbg_Gt0!m= zaM751E-Ia-hty~lXJ=Bd(CFAPg-Xgs5?n;qwl<0o@_s{7JU6|mJ)Q6rlakt;-!FvC z1H{83@&~{b2@I*80X!cE4)VnsJO=^+p??Pgi2sm5{~ZWq{v8OA8pW`^rUbkHoJawI zf4lwv0`xCN0Bj?`Dqi9Qu!==J2?TgcIS%DqByLLNTpdnu{nmsYDg0oib|_oJFX+``Db>*U1nNbnjRVZPgPGzn*tQdh_Sx-u#Q%dV5UiQ zk=z&R`Uc;Z<6pr)wF&=!0sp9f0sqlMF!;CpPw=lOlIzCTHD{?`bgVMl5}qFgq(x=I z!pH|?B7j&rwJ$tT0o^g2qDRFsvM&hFNs;XT$MY|Tc=r4i0`;{23I#@91S5fIuwctT z1YBnW8;J#IeselU#%A|E&waJ?N|9-&F3%^#Z4f-HTOf&|nUo!CAPKIU+QDqxXRm9v zzN8{-VWF;qYm?>90`s}4PbJQzV!hU(Onv)E}%bUVBd0p5HS&bmq->4aKe|~Z0kF_Vw6?MYzEpkDjYfv9oG$B zYArGsqP$ooE+Pb^vFp?9GdLOpvF8lkwx>G4|Z^KxD} z5XpM!9Oz367WVT0i#HzW;1%Z3eeAGt?9e5c(BF0*TimxF(xdV83yjPJG!!kqL-7MH zP|ggHfYq!`oGqj>mbnijQ3}HGKbyF_7zCOg1m}Mj0>XB1k6}um$^!{@nJ;AbHk$Qm zypjJVb_R=a3@@_23}v6ugpZ(zy0yab-EbMJ)V7XS*~|k{R*MR1eYL)s#iHbaU&WfksQPL zd_M6phpP54tm8QD3C$XI7W>UWqn8|+tK0LP{P4Hm3RzmcuJ3;r2=OTC;id+$0Dyc! zW@N(vh-FqFNghze;fqStSPUgN`T+ewAj^&E zn^6e|m+!lA?YXjFV}_;8`?5zEJ`;)rndVnSnU?24L=)y2CVgwpq~Zw+p{AxM714bI zbyoAAC>pkZrDzU=|4=mD>2@a$+s_nDnUf@+!>bpH=HYM{$csV2KE%%-*oj^1ctr6` zv;_EcL0FUj@wP+%>1|WLp!PFu^G}&!$X_0~Bj7LZU8sxP_{A*;L+*dzUj74Z(@|C> zdbf{8RY33t7n+u)T87WMk&olig>bY~ywNx5be-)AyEfy8Z{HkCeNNaRy~F13&*SsnAQtW5zenX^Y~Qv;|EwGkw+!-(i%Cg_N#wcTU|RAHh9aaxfq)dAEU5fe_=p zD&T)%V<=dd$*8m zaEj9%s;Gr<@hF4AI~kcIja9!@?MkQO9n?m{9;oxKW^Va&KIs4}e~`-0P*vlMFQv0I z1uf+~#vGj;YHDVbPv@hmVvgS%F) zgQGy4(SJP~jMhM5(1 z#;MwvKqoB@eYpR^=zQQPPuFhd$L^KIM50!S+jhF53bUe2o1Ag&tIa5u-}o*O)6iKQvxy(_L5rY9Ocsv34MIBQEd-XR7i5fs z_t*lA=dmcMLagpNPZ^1RgSM6vPwDzQPpR-;9ZnP>Wa%URUiN>ZN6Txa*|+xf9aM>`(X=6_r{X9z z%3D^bwx-Mw_Fs%+cQfS&XbV*n<69EZl};@xpB$XTkECk*hec!t)^867=jval&wS)M zG;j~I%j+Bzi-$$~2pO^_2PqA)3oF{iBi4Ym*#_;|D0wtq<`Uj&r>Y?hc;CQ)8LK|$ zS;F>)>evd11LVSwIf?jdVuV@go!NV^;fze=5QyX?@NvBv00WHYG3Ge!Ch*U@HANHG zUS~252%>v7axPDdU@(DI&4_lTL&iW%AOiyhH&_l)`m^^2MUnKnhqznyRQw)fT?2a4 z*=@Hm<661i(Mn^*1yUc2#t}$v=@U#C@yDJarNM7s@GIH|McEN<^+r_Xj@bs$_-xz?G_qiI*f`x)VIgGdW&gyO=5RXqTmtoyD?dKLdQ@zsAnt~=HYFxhhCq?mI@RonOEGn zeY81($6SgvGEt|ATP*f_-XHtu^T-^29(8*x6B@g`ep@pphap+(6X;P9h(jU%8rC{5 zq8C0KU3LVYi61%*si3RK;e&%#=yH`PHyrY~Cfyng;@jtVi>51Fs7qsV~~ z+!8K2%W7G6*=X%`O(kz78xsn0cUR|zpRpNo!8f346`=FEnNGWsjndgNJPNWwY7o0Z zXBW7kUb|9+YN^fI6utwaFg+ixLXhe{ei-^5OY-K;n(Xhc6B$uhq8c#n6L^7P0 zNwo)`90c4NM*o!y(KG#%3#r$~pZ<&c+D!pp6S$tfP@O@F$2~`><&RVW=R=N@9e$ow zkzA?b7lQ5VSy;=kT-l?~VEK2t^6fGX<6cB<^%X36zf0MZbPO|;AaDf4G0eQD~Rp$Mv*UleInRrc_n$~vV z-qu5-QEpbq73uz-MH^gUi#RaTdVIBc?0fTt0X6}&kN~AGRp}<&2SvsIEhze|{ck~$W2TpQG5qvK+ypd*qZ5O)3(+pmAUHdsjA-Ye)&(}bhBSo~ zMx{SP>ws=sqYa#naL+Lj)k{qDP3Uh@i#o#pIn@!-MNar4dSSIv)Iz{vksJdGG1x5s zl}4GP_`_-eo)ag}W*bbB)lmL1+a2D2!l+9`=;4s(;S#za{*5D(G>Ty-dk&&rEdHO2 zNgmt()s+r~?WKb%(w||$X_t(@I)LYfGzRz6;Ii2{tTVbdlc^L-izdy*ho9rohR^^- z4}DhA$)A7t0p`%6CWE~`{IJki5Q(_yjqwwn{XR?|=Z8T1Z$T-fyn z@Dh})r|!O`lh}SjHCXxo2(kF!{|>RD$n-2j$F*7D@v|OWd+Dz(z=r(eJn!qt0%KrN zgz-rb>#^jkH|hc6+?lWBoCtZr^xC0Ce9A*3OGAKdg>lOg(q*}?^TVYonwaA9JYs`}SW$c0RT;VG%Q_+!&#**MkEtCkts?I3-n@zDhECM1 z+no2Xw>Me$^SpC4sUGe_MIk1X^useKarNBbu4@Ere6Vw!chOc8u;rYlebSN=n)aTo zmrFL&kIA5HRf`3CwpCh};opAjq6vPf<0{6~2vdScP`T4hVGJ?Wkj@KDD7!{ai=lqL zh7*a|=`Mz&<^j$(u!QJj`ie{F;d$(+dPr|4!oL3;sJU*uit7RUUOTI+>vgi$iZ{9X zTA~pp2gbPirvZRC2BvteSWrkPIc4aM93>L?6$Z0R36p{{6oFD8J`@Z53J`y-W+(&< zCC^sg>iY%-vCjt|9%Bo{l zm}LUU649Z?J;t{b$^@2$yG@ld&R>mEQ6>)}`W9d1^S_zt;2?0mG90$7bm!W{I%aD& zk%fQdvIW%;=pFj>`KWT3&XlW)`dmOpik9W;!Y z)(2-sSmTcxM%tJ9sWB6d^=YW}Uf@CI{bM9lV%5*%`kxEH0aJ1MxKp5M4-v>zoTHq^ z1f*#<-b$e9LR#^V$UEp@Bq}vFo*IQjf+9fR!bW>w$j8F(DFxq+Vt^SkktS;;phrY6 zpRgtKTxhWL)gg!mD#G7J=35wr_ExTR6jRT$sF{X^H%D+nuH%J2Y<;PlFfo|^yRuK8$aZL zZ}i!Evi!NwN0!L_`^2Y1>SX*C?zQla&)8i`^_BnehEQ8H$SF;he|=q)Kbv^AP?}yU zVMB_Ut$T1B?X^^h(;H=e^GwuQ1K2~%9=}D7~v@B-v%gt0BiXmKCqZzeXSS zvZ$Y2Spzt}{;Xkoj*Kpw9j{1fm!4|FWu2D^U~qA|?)(_rKqZ(=?a?@Q?QM5K`&q%ydZ~pbPj-`VqfSDFZi~#dc+2Zb&AGLyiiH!S zThx-SNi;;Kt>X^L=y5Lc3w3Fd6}Ry$X4@8s!;B!euF4u_dEW0dsNIw`>Wv2cw87=x zk`vVwzGY1Pv|_UmYNg7Z7h)mSB6;@*xxEmbP^lWTBs1N^WROL*&G~^mv&iFn&FM}( z0-`0>k4&Sc{ADakRbsGIw3e<*%vNVzP^qw7W##)7AvKUiVD%JgQRi{RLiFTPH9rOddKpXSNdNnzWs8FD0=5JHWNv6 zpp>qMQu#>Vn=&MP#9B)b%CSI}DwKv&QIunz6ADCmeL^8G_#2Y13OqOh7P-_P)Z^b92yoJATD4Xw`JEsv4KXGg3E^b~y2o zF^QQNfWN&SO0tMQ2HX3znEQiZn{DKfeZ;r`H}G55baf6b(;Lq#t(M$f*-+1JWb#;!D7Y#^aCpOlbpL2x^pT~E@(=SoExMT zGk8!7j(xzFF23y?)V4+(Dg6o}DTeNa_=3>8ntLPTsU2K}I!@NX(}(rEiTe`}*&+=D z9;NiWgm2B}=Wo8&YAM^r)duH2e68h^HBV2Mw0h(matvcbgM2<_d@xG>lsY*ePh?&~ zEHQ>BPAf;zF`>hAF>v0_4r8$|LA2zz;BPj1V5=s@@ie^gyt)U7@e1Z%ZF>(nEn7_B z@e>lyG6h@i2GKP=6FK@O1<5gl`sHP8lyrZh3kn`oKu1iJ{VEmwZ&A{TQ#7SsGk+Ix zf$}`6ZfLxHIT)zh)B{>xf?P9lF3m+|sufB|prxg%(UVPxF`DzsS#*423$QUoZvo_YPedTacA!?}Eh6yz&DD5ey z3b{zf?UUQ`Q~Mp7Aubu3mJgYR_DApl$kvMH-PM=gk`i6&&WdU_Wj}Y;(!!~{`K0^x zCt@WQ*!7bgrk__Jnr5y*EK$}vDqOz)$vi&lT9dpo*_DL%W}sVYCANP6F9!ZOcxGZH zKlVw&zkLm@)Y}22Rn1FvaG<*RG;sRLNWH)=^qQcNQ6sVUJU2>De4bFRS zCY;8G46zXm(-%aLo+WA(N=^xkiEO`ClJT4>6kdekDPv_XqNiB@=gp_U+zGV9{OPQv zI8k~866iEo2Y86&SRd?VvO&I8GH2qe0U>Aads2D4w<6(Tt*g9Qy4O+-Y;CI=a?PIj zdt1L?MFt!PbH2FSLe-oj?cjQU;EmSkjP`I|MQtTXr+IK)+lV!F`AM5>nu1_{Q2WkR zPb!E!?Hd~-Wnm)(BTqf7Dg!G)dpj(0aQP!5a{hb03?}-Aey6k|e4A>+@8;MRv$Sa6 zV43FQv2#0vAi%4Ru}KQzY9uBfm`98&!vC|Vl+yX{MZxP%t;$ONycLTQF$5YfElRBZ z7Nod53$WtRUiPj9;km@m573bl_%jBDbojgfw~gt^g?^a_3+TBtq7VZf`Y)}|O1>jb z7)|&;9{?wGfB<-S@Co_u16VZZI$Xj3M%nAwje+p%@)#SkKV5wB9aqaiw-C67DR`!^ z!(OZ*W}%(#aBB^I?ecgYk!kXEre??CNGb;33)?|ej3tmIFtw~=xgS8@eRC3w#9(rx{$3i4J>$PC^+h0?F@6M@eYlLEP`ehfD@+uPn;?- zB=@7k^Kv8AG#s8$oF1zV`uW48GM$x`N@iIy*dO{5E!Yf+Y$gMw~%T0kurexb$5BZsd)w-Rg9wyNGxz}_?GC*mho z!2WPayzRgzU&vdKX_hr8mPk7l@p^QpgJ&)uQG#J0mf0s&$zCJ%pm8#=S$D)K>@)4u z0sjcQ6j-1}jfXF!x(E=l?RVVdiIeNo=u_^x)51Ku(vZUFZw_mC#nKmjk8M%;T4pmgmuX zPjdyC0NY9-y80#uVw<74WgVQ;8yA>!*F( zT^ih?GHE)fm1Rn(<%~2Ka0N+FHm@_*J4r9CeAn6-Y+mQCepIbo6}ySR=~4gvnLoT_ z^A&$dg)MtI@sQINeCt|7CgVr z8#UW}&g<%m9QS|v=2a6^qSm`><9}}C)@CrYzOI}w&ACc>{s5mD+lA3#?RwkjhO(4K*F$29 zg{0>r5QE*or1p7`b9*rUtOk5&MnBn>JHs!?EoS3PsdOA3CxEnR?S7fndTa)*SG9W( z$kF3O4=F4T4sqzAYN-v^Te?tH#**m}`vIrII{KMUFn%ULy?GpOl z?ew*aJggk9utsY_$Oy^c{`*_y&Eo|-ptzgB9}4wv^W_~E{r@Q*AXIzFr!R5j;u zpqnzQ_G@EIwl?=8B{QrWCT>k9jG32w-I{*rq55*nRgpjHG`gmnstMlzf{#}3msqWt zk&W?sxGIh+yDrd5LF%cRoMK;=d{Q;9u%i!VCtFiRhWG{K&z`@WHatH{?#!64Bx}g? zJzb-5S?~n|UfK&*wkV$MxvjHT8YrH9cx2j^=KWCu{;olhdFWb1?G zyi6Mlww9RRI#%kZ6CCI!0vp$A6T+FOA-3jSA2KmsY$(wy^&--BVHn#8?1kBxcERsK z!Nb>f$FurHvgu@;Yy`sT&jP zwsmedYK*1T{?t z;B~_s^N}wOX+#$zY8f~^OeKk;;r*t+F<*Z3wQf#g;3s%LE~ED|+`0zcxrW$*dK5z< zNj= literal 0 HcmV?d00001 diff --git a/research/direct584-commuting-retiming-cover/PROOF.md b/research/direct584-commuting-retiming-cover/PROOF.md new file mode 100644 index 0000000000..1cdcc54f8c --- /dev/null +++ b/research/direct584-commuting-retiming-cover/PROOF.md @@ -0,0 +1,164 @@ +# Complete direct 584 commuting-retiming cover + +All addresses are zero-based positions in the two pinned PR 3133 words. This is +a finite statement at binary address dimension nine. It is not a theorem about +all supplier words, all helper eliminations, or all dimensions. + +## Changed word and exact algebra + +The original word contains + +``` +B48: 168 += 584/2 +B753: 584 += 439 +B1196: 168 -= 584/2 +R82: 584 -= 439 +``` + +The last two operations occur in B and restore respectively. The helper has +arbitrary initial dirt. Remove B48 and B753, replace B1196 by `168 -= 439/2`, +and remove R82. Remove helper584 from the live/helper inventory and regenerate +the inverse-reverse cleanup after every retiming. In the full fixed word the +two helper reads contribute `p/2 - (p+q)/2 = -q/2`, and the restoration returns +the helper. The exact interpreter checks this assertion against the complete +word, including all surrounding operators; it does not assume isolated scalar +cancellation is sufficient. + +The original-cut word and the first and last contact-class representatives +are replayed in both orientations over the rational free group algebra. Each +live input and arbitrary dirty helper is an independent column; native warp +symbols are independent noncommuting invertible operators. Forward endpoints +are `y += x`; the same-order inverse-transpose endpoints are `x -= y`. All +other live rows are identities and all ninety private cleanup rows are zero. +The supplied cleanup is executed literally and compared to an independent +inverse-reverse derivation. These finite symbolic identities imply equality +under every substitution of invertible operators, but do not admit the frames. + +## Exact family + +Only four additions with common source 439 may move: + +| Destination | Original B address | Addition | +|---|---:|---| +| 168 | 1196 | `168 -= 439/2` (the new direct read) | +| 150 | 772 | `150 -= 439/2` | +| 56 | 802 | `56 -= 439/2` | +| 115 | 1244 | `115 -= 439/2` | + +All other scalar instructions remain in their original relative order. No +read crosses a B boundary, no correction gates are added, and every native +slot retains its physical register and position. Native operators, phases, +entrance/exit frames, and all helper entrance/terminal frames may change freely. +Non-native scalar frames may be chosen arbitrarily subject to the inherited +common-frame and monotone consecutive-contact inclusions. This is a generous +feasibility relaxation: a contradiction already rules out a paid realization. + +For two nonzero transvections `d += a*s` and `e += b*t` on distinct endpoints, +the matrices commute precisely when `s != e` and `t != d`. A nonidentity +scale commutes with the selected transvection precisely when it touches +neither endpoint. These criteria follow by multiplying their elementary +matrices. The four movable reads commute pairwise. No native slot touches +their source or destinations, and no remaining fixed B gate touches source 439. +The verifier checks these premises on both pinned words. + +Remove the four movable reads and the two deleted gates to obtain a fixed +sequence. Each selected read can cross precisely the contiguous interval of +fixed gates commuting with it around its original cut. It cannot cross the +first noncommuting gate on either side by the allowed adjacent swaps. The +maximal original-address insertion windows are + +``` +168: [0,1301] 150: [0,1292] 56: [560,1245] 115: [0,1373]. +``` + +An insertion at address j is immediately before original B gate j. The fixed +sequence's integer cuts omit the removed gates; the verifier derives those +cuts directly rather than treating the displayed addresses as an input. + +## Finite quotient and completeness + +For each read, partition its legal cut interval at every fixed contact of its +destination. A slot is the closed integer interval after one contact and before +the next. The four slot counts are respectively `8,4,1,8`. The carrier has no +fixed contact in B, so a contact class is exactly: + +1. one slot for each movable destination; and +2. one of the 24 orders of the four reads on carrier 439. + +For a chosen order with slot intervals `[l_i,u_i]`, feasible nondecreasing cuts +exist iff the greedy recurrence `c_i=max(l_i,c_(i-1))`, starting at zero, never +exceeds `u_i`. Necessity follows inductively: every feasible cut is at least +its greedy counterpart. Sufficiency is the produced cut sequence. Equal cuts +are allowed, with the specified carrier order fixing the order at that cut. +Of `8*4*1*8*24 = 6144` choices, exactly 1002 are feasible for each provider. + +Every allowed adjacent-commutation placement has one of these slot/order +descriptions, hence a generated representative. Conversely each generated +representative lies in all four maximal windows, so commuting each read to +its chosen cut yields an allowed placement. Within one class, every physical +register has the same ordered contact list. Changing cuts inside a slot only +crosses gates disjoint from that destination, and the carrier order is fixed. +Thus all common-frame/monotone inclusion constraints are the same up to event +renaming. One infeasibility witness per class covers every allowed placement. + +## Independent physical path certificates + +For each representative, the retained certificate identifies a nonzero vector +v and a sequence of literal physical events. The checker reconstructs events +from the changed word itself, with native warp entrance/exit events separated. +Input r has frame span(port[r]); target r+112 has terminal frame port[r]^perp +in F2^9. These actual source/target contracts remain fixed. +It requires that: + +* v belongs to the exact fixed source frame; +* the sequence is strictly chronological; +* each adjacent pair consists of consecutive touches on a common physical + register (no intervening read, write, scale or native warp is omitted); +* no interior event is a native warp boundary; and +* v does not belong to the exact fixed endpoint frame. + +Monotone inclusion along each consecutive-register edge propagates v. A common +scalar event uses one frame for its involved registers. Therefore propagation +forces v into the endpoint frame, contradicting the last check. This argument +uses only necessary frame inclusions and not a floating objective, graph +optimizer, heuristic failure, or a claimed native phase calculation. + +All 2004 final certificates pass this literal checker. Every path starts at an +original input port and ends at a target output; none uses a native boundary or +a helper entrance/terminal boundary. Each is therefore independent of every +native operator, phase, native entrance/exit rank, and helper entrance/terminal +frame at the existing positions. These boundaries can all be relaxed at once. + +For discovery, 660 classes per provider first had port-to-target certificates, +and 342 had certificates ending at native slots on registers 285/381. The latter +were insufficient for this stronger statement. They were replaced by new paths +after relaxing all native boundaries and every helper terminal boundary. The +additional discovery paths end at targets 124 (206 cases), 159 (67), 215 (30), +192 (19), 212 (12), and 129 (8). The final verifier consumes only the complete +2004 port-to-target certificate set; it does not rerun that discovery search. + +The checker expressly rejects a valid fixed-native-boundary certificate when +it is offered for the stronger port-to-target contract. It also checks that an +actual inserted native reset breaks a formerly consecutive scalar path. Thus +neither a fixed-slot obstruction nor a path jumping across a new reset can be +used to exclude a larger model silently. + +No invertibility, equal native entry/exit dimensions, phase realization or cost +is needed for this necessary-condition obstruction. Free changes at existing +native slots and helper boundaries still cannot repair it. Changing the scalar +network, adding or moving native slots, changing input ports or target output +contracts, or crossing a noncommuting gate with corrections remains outside +this result. No claim is made about those larger models. + +## Meaning of the result + +The direct helper elimination is an exact arbitrary-dirty algebraic identity, +but none of the complete commuting-retiming family has legal monotone frames +even with the stated native/helper boundary relaxation. There is consequently +no cost gain or +conditional κ to claim from this family. A changed scalar-network/consumer contract +requires a new exact word, native operator/phase proof and complete cost invoice. + +This is a written finite coverage argument plus exact executable evidence. +There is no Lean/kernel proof, all-parameter supplier theorem, new selected +frontier, or global no-go theorem. diff --git a/research/direct584-commuting-retiming-cover/README.md b/research/direct584-commuting-retiming-cover/README.md new file mode 100644 index 0000000000..c070870a49 --- /dev/null +++ b/research/direct584-commuting-retiming-cover/README.md @@ -0,0 +1,97 @@ +# Complete direct 584 commuting-retiming obstruction + +Deleting helper 584 through direct carrier 439 delivery is an exact dirty-state +identity on the two pinned PR 3133 provider words, but **every allowed placement +of its four commuting reads fails the native frame contract**. The cover has +1,002 contact-order classes per provider. It remains impossible even if every +existing native slot and every helper entrance/terminal frame can change freely +together. + +This closes the gap between a few nominated placements and the complete stated +retiming family. It directs the next attempt toward a changed consumer network +or an additional/moved native slot. It does not supply a cheaper +construction, a larger conditional κ, or a global barrier. + +## Exact scope and evidence + +Only the common-carrier reads to 168,150,56,115 may move by adjacent commuting +swaps inside B. Every other scalar gate retains its order. All native operators, +phases and entrance/exit frames may vary at their existing positions; helper +entrance/terminal frames may vary too. Scalar frames may be refitted subject to +the common-frame requirement at each scalar gate and monotone consecutive-contact +inclusions. [PROOF.md](PROOF.md) gives the algebraic edit, +maximal windows, exact slot/order quotient and path argument. + +The checker derives all 6,144 slot/order choices, retains exactly 1,002 realizable +classes per provider, reconstructs their literal words, and checks the fixed +certificates against consecutive physical touches. It does not import the +search graph or an optimizer. All 2,004 final paths run from original input ports +to target output frames, +without any interior native boundary. Every class is rejected, independently +of the native and helper boundary choices. + +The original-cut word and both extreme class representatives pass complete +forward and same-order inverse-transpose replay over the rational free group +algebra: 631 independent inputs, 90 private cleanup buffers, all dirty columns, +and literal inverse cleanup. A written commutation argument covers the other +representatives; the package does not claim 2,004 full algebra executions. +Twenty controls reject wrong direct sign, stale cleanup, crossing the actual +noncommutation barrier, zero direction, incorrect physical register, reversed +path order, a fixed-slot certificate offered for the stronger contract, omitted +contacts, an actual inserted native reset, and a target frame accepting the +claimed obstruction direction. + +## Sources, attribution and limits + +Base: `20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority revision 6. +The two live words are byte-exact from dcharb78's +[PR 3133](https://github.com/CrocSwap/integer-mult-bounds/pull/3133), head +`51eb9c4ee9e4722010d308aa3309e039d3940cc2`. Their Git blobs and hashes, and the +historical catalogue/selected record, are in [SOURCES.json](SOURCES.json). +The selected record at this base is κ=0.001672660197076918. No source supplier +admission or selected cold replay is claimed here. + +Credit stays with dcharb78 for the coupled 586/588 folds and final source words; +Marius-Paul Dumitrean for PR 2979's joint frames/extractions; Jeremy Kothe for +PR 3015 and the preceding mutable-carrier/scalar rewrite lineage; Mason Hale, +Jeremy Diviney, Yiyang Lu, Tekalign, icekylinx and the complete source lineage. +The source [CREDITS.md](../rank7-coupled-586-588-carrier-fold/CREDITS.md) and +[NOTICE](../rank7-coupled-586-588-carrier-fold/NOTICE) are authenticated live +inputs. Gareth Davidson's PR 1995/2013 fixed-word bounds and the retained +[normal 45 A-retiming boundary](../normal45-a-retiming-boundary/README.md) concern +different fixed words/retiming domains; this package does not repeat or extend +their conclusions beyond their premises. + +New work: the direct 584 elimination, complete four-read contact cover, physical +certificates and simultaneous relaxation of all existing native/helper boundaries, with a separate exact interpreter/path +checker and publication review. Prepared by Ross Richardson with substantial +OpenAI Codex assistance. Separate AI agents are not independent human review. +Apache-2.0. This is finite executable evidence plus a written coverage proof, +not a formal-kernel proof or an all-parameter multiplication theorem. + +## Reproduce + +Python 3.12, standard library only; the direct verifier needs neither Git nor +network. From the repository root: + +```sh +python3.12 -B research/direct584-commuting-retiming-cover/verify.py +python3.12 scripts/research_package.py --package research/direct584-commuting-retiming-cover +``` + +The registered command has a 600-second bound. The initial fixed-frame replay +took 165 seconds; final scoped validation is recorded in [VALIDATION.json](VALIDATION.json). +A missing certificate is an error; the verifier never regenerates it. Exact +source-container hashes bind immutable inputs, while regenerated certificate +containers are compared by decompressed JSON rather than gzip-header bytes. + +## Open next questions + +Can a changed scalar consumer network or an additional/moved native slot remove +the obstruction without repaying the saving? Begin with one explicit changed +contact and one literal previously rejected class. Derive the resulting frame +path or an exact legal construction before a broad search. A survivor still +needs arbitrary-dirty word/cleanup equality, native operator and phase equality, +and the complete local, idle, owner, precision and outer invoice. Changing only +existing native frames or helper boundaries is closed here, not an open question. +Structured scope and next steps are in [TASK.json](TASK.json). diff --git a/research/direct584-commuting-retiming-cover/SOURCES.json b/research/direct584-commuting-retiming-cover/SOURCES.json new file mode 100644 index 0000000000..f01ec2e46c --- /dev/null +++ b/research/direct584-commuting-retiming-cover/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "LICENSE", + "usage": "input", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "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/rank7-coupled-586-588-carrier-fold/CREDITS.md", + "usage": "input", + "git_blob": "24f00912d4ec829c3c8d2a8d086aa135664a124c", + "sha256": "1d9d8f56d8899f55878e4cb2c4e052b22506444016a51c2e678773505f5189e6" + }, + { + "path": "research/rank7-coupled-586-588-carrier-fold/NOTICE", + "usage": "input", + "git_blob": "89c20926ea7f803718f751d95989d5a269908efd", + "sha256": "c9731c9cca25ede32c2a1b3aef6d5b249973cb2ed5fb2494407bdca598763661" + }, + { + "path": "research/rank7-coupled-586-588-carrier-fold/edits/FINAL-WORD-base.json.gz", + "usage": "input", + "git_blob": "cb4cc24a4545944627ad595c0c5080196952b9f0", + "sha256": "300a9b8ad1d554f0e6f84f43f3f5fd870a5b4e5f81ad856900b6e8999684892e" + }, + { + "path": "research/rank7-coupled-586-588-carrier-fold/edits/FINAL-WORD-extra.json.gz", + "usage": "input", + "git_blob": "decc8f26d8aab108baf75f0d8b2d1012eb06d076", + "sha256": "495d030f1e03b90e954dad3043994f03293d41b9ed220a3beaef849df435d3f0" + } + ] +} diff --git a/research/direct584-commuting-retiming-cover/TASK.json b/research/direct584-commuting-retiming-cover/TASK.json new file mode 100644 index 0000000000..4439f254e2 --- /dev/null +++ b/research/direct584-commuting-retiming-cover/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json", + "research/rank7-joint-endframes/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering" + ] + }, + "scope_status": "changed", + "actual_scope": "Complete finite commuting-retiming cover for direct helper584 deletion on both pinned PR3133 provider words. All2004 paths are original-input to target-output, excluding arbitrary native changes at existing slots and helper boundary changes. Exact dirty-state identity is checked separately.", + "scope_change_reason": "Explicit donor task seeks a valid conditional kappa above0.00173. This standalone result closes the missing coverage between a few nominated direct-fold placements and the entire four-read adjacent-commutation family; it changes the next research decision to a joint warp/consumer change.", + "bottleneck_link": "Helper deletion appears favorable before frame admission. A complete physical path cover prevents counting that apparent saving or repeating equivalent retimings.", + "budget_minutes": 240, + "stop_rule": "Complete the four-read class cover and independently checked literal witnesses; stop before treating changed native boundaries or other scalar networks as excluded.", + "outcome": "completed", + "evidence": "PROOF.md; source-bound verify.py and exact_algebra.py; PATHS-base.json.gz and PATHS-extra.json.gz. No new kappa.", + "author": "Ross Richardson", + "ai_assistance": "Substantial OpenAI Codex assistance, including separate construction, exact interpretation, physical-path review and publication agents. Independent human review is not claimed.", + "open_questions": [ + { + "question": "Can a changed scalar consumer network or an added/moved native slot repair direct584 elimination without repaying the saving?", + "why_it_matters": "All1002 commuting classes remain excluded even with every existing native boundary and every helper boundary relaxed. A different contact network is required within this source contract.", + "first_step": "Pick one literal rejected class and one explicit changed scalar/native contact, then derive a new necessary path or an exact native realization before broadening the search.", + "blocked_by": "A survivor requires full dirty-state/cleanup and native-phase equality plus the complete local, idle, owner, precision and outer invoice." + } + ] +} diff --git a/research/direct584-commuting-retiming-cover/VALIDATION.json b/research/direct584-commuting-retiming-cover/VALIDATION.json new file mode 100644 index 0000000000..d2c0397d86 --- /dev/null +++ b/research/direct584-commuting-retiming-cover/VALIDATION.json @@ -0,0 +1,205 @@ +{ + "status": "LOCAL_REGISTERED_REPLAY_PASS", + "command": [ + "python3.12", + "-B", + "scripts/research_package.py", + "--package", + "research/direct584-commuting-retiming-cover" + ], + "runtime_seconds": 154.48935966699992, + "result": { + "status": "PASS_DIRECT584_COMPLETE_COMMUTING_COVER", + "providers": [ + { + "provider": "base", + "classes": 1002, + "endpoint_kinds": { + "start -> end": 1002 + }, + "exact_algebra": [ + { + "case": "anchor", + "pass": true, + "orientation": "forward", + "independent_inputs": 631, + "private_buffers": 90, + "cleanup_matches_independent_derivation": true, + "precleanup_helper_rows_and_isolation": true, + "bad_endpoint_rows": [], + "nonzero_private_buffers": [], + "undefined_cleanup_registers": [] + }, + { + "case": "anchor", + "pass": true, + "orientation": "dual", + "independent_inputs": 631, + "private_buffers": 90, + "cleanup_matches_independent_derivation": true, + "precleanup_helper_rows_and_isolation": null, + "bad_endpoint_rows": [], + "nonzero_private_buffers": [], + "undefined_cleanup_registers": [] + }, + { + "case": "first-class", + "pass": true, + "orientation": "forward", + "independent_inputs": 631, + "private_buffers": 90, + "cleanup_matches_independent_derivation": true, + "precleanup_helper_rows_and_isolation": true, + "bad_endpoint_rows": [], + "nonzero_private_buffers": [], + "undefined_cleanup_registers": [] + }, + { + "case": "first-class", + "pass": true, + "orientation": "dual", + "independent_inputs": 631, + "private_buffers": 90, + "cleanup_matches_independent_derivation": true, + "precleanup_helper_rows_and_isolation": null, + "bad_endpoint_rows": [], + "nonzero_private_buffers": [], + "undefined_cleanup_registers": [] + }, + { + "case": "last-class", + "pass": true, + "orientation": "forward", + "independent_inputs": 631, + "private_buffers": 90, + "cleanup_matches_independent_derivation": true, + "precleanup_helper_rows_and_isolation": true, + "bad_endpoint_rows": [], + "nonzero_private_buffers": [], + "undefined_cleanup_registers": [] + }, + { + "case": "last-class", + "pass": true, + "orientation": "dual", + "independent_inputs": 631, + "private_buffers": 90, + "cleanup_matches_independent_derivation": true, + "precleanup_helper_rows_and_isolation": null, + "bad_endpoint_rows": [], + "nonzero_private_buffers": [], + "undefined_cleanup_registers": [] + } + ], + "rejected_controls": 10 + }, + { + "provider": "extra", + "classes": 1002, + "endpoint_kinds": { + "start -> end": 1002 + }, + "exact_algebra": [ + { + "case": "anchor", + "pass": true, + "orientation": "forward", + "independent_inputs": 631, + "private_buffers": 90, + "cleanup_matches_independent_derivation": true, + "precleanup_helper_rows_and_isolation": true, + "bad_endpoint_rows": [], + "nonzero_private_buffers": [], + "undefined_cleanup_registers": [] + }, + { + "case": "anchor", + "pass": true, + "orientation": "dual", + "independent_inputs": 631, + "private_buffers": 90, + "cleanup_matches_independent_derivation": true, + "precleanup_helper_rows_and_isolation": null, + "bad_endpoint_rows": [], + "nonzero_private_buffers": [], + "undefined_cleanup_registers": [] + }, + { + "case": "first-class", + "pass": true, + "orientation": "forward", + "independent_inputs": 631, + "private_buffers": 90, + "cleanup_matches_independent_derivation": true, + "precleanup_helper_rows_and_isolation": true, + "bad_endpoint_rows": [], + "nonzero_private_buffers": [], + "undefined_cleanup_registers": [] + }, + { + "case": "first-class", + "pass": true, + "orientation": "dual", + "independent_inputs": 631, + "private_buffers": 90, + "cleanup_matches_independent_derivation": true, + "precleanup_helper_rows_and_isolation": null, + "bad_endpoint_rows": [], + "nonzero_private_buffers": [], + "undefined_cleanup_registers": [] + }, + { + "case": "last-class", + "pass": true, + "orientation": "forward", + "independent_inputs": 631, + "private_buffers": 90, + "cleanup_matches_independent_derivation": true, + "precleanup_helper_rows_and_isolation": true, + "bad_endpoint_rows": [], + "nonzero_private_buffers": [], + "undefined_cleanup_registers": [] + }, + { + "case": "last-class", + "pass": true, + "orientation": "dual", + "independent_inputs": 631, + "private_buffers": 90, + "cleanup_matches_independent_derivation": true, + "precleanup_helper_rows_and_isolation": null, + "bad_endpoint_rows": [], + "nonzero_private_buffers": [], + "undefined_cleanup_registers": [] + } + ], + "rejected_controls": 10 + } + ], + "literal_path_checks": 2004, + "seconds": 154.48935966699992, + "scope": "Four B reads, finite h=9 providers; arbitrary existing native boundaries and helper entrance/end frames; no new kappa." + }, + "environment": { + "python": "Python 3.12.12", + "platform": "macOS-26.5.2-arm64-arm-64bit-Mach-O", + "dependencies": "Python standard library only" + }, + "mathematical_files_sha256": { + "verify.py": "62b150488560a36088a418be52133298b050026481451a46968fa6cb97ce2248", + "exact_algebra.py": "6fa6b1995fdc67c7b6bcfe75440b7225868d988574aeb468b907eebf8a06770d", + "PATHS-base.json.gz": "61659e1a46c441edb89d8292152091f1043f322bbfc2166c6e59ea49416a6446", + "PATHS-extra.json.gz": "61659e1a46c441edb89d8292152091f1043f322bbfc2166c6e59ea49416a6446", + "CONTROL-native-entry-base.json": "8f13d77119409c4470da5de97621b06eedd914e5c3736d67e2660d1a9f06559a", + "CONTROL-native-entry-extra.json": "8f13d77119409c4470da5de97621b06eedd914e5c3736d67e2660d1a9f06559a" + }, + "other_checks": { + "independent_cover_review": "PASS; rational matrix commutation and pairwise interval-feasibility review; final source binding pending", + "publication_bytes": "pending exact local publication commit", + "source_history": "pending exact local publication commit", + "git_free_export": "pending exact local publication commit", + "hosted_ci": "not submitted" + }, + "scope": "Finite h=9 words and declared contact model; no new conditional kappa, supplier admission or formal-kernel proof.", + "source_note": "The recorded registered execution preceded only a trailing-blank-line removal in exact_algebra.py and addition of the unchanged root LICENSE live input; the exact publication export is replayed separately." +} diff --git a/research/direct584-commuting-retiming-cover/VERIFY.json b/research/direct584-commuting-retiming-cover/VERIFY.json new file mode 100644 index 0000000000..a7b6951211 --- /dev/null +++ b/research/direct584-commuting-retiming-cover/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "LICENSE", + "research/rank7-coupled-586-588-carrier-fold/CREDITS.md", + "research/rank7-coupled-586-588-carrier-fold/NOTICE", + "research/rank7-coupled-586-588-carrier-fold/edits/FINAL-WORD-base.json.gz", + "research/rank7-coupled-586-588-carrier-fold/edits/FINAL-WORD-extra.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "All1002 contact classes on each of two exact provider words;2004 literal input-port to target-output paths, independent of all existing native and helper boundaries; arbitrary dirty free-operator forward/dual identities for original-cut and both extreme representatives; literal cleanup;20 semantic rejection controls. No supplier or kappa admission." + } + ] +} diff --git a/research/direct584-commuting-retiming-cover/exact_algebra.py b/research/direct584-commuting-retiming-cover/exact_algebra.py new file mode 100644 index 0000000000..01ad1580e5 --- /dev/null +++ b/research/direct584-commuting-retiming-cover/exact_algebra.py @@ -0,0 +1,153 @@ +"""Exact rational free-operator interpreter, including literal cleanup. + +Ross Richardson, with substantial OpenAI Codex assistance. Apache-2.0. +Developed independently of the PR3133 auditor; source JSON is the sole input. +All initially dirty registers are independent columns. No finite matrix fixture +is substituted for a noncommutative warp symbol. +""" +from fractions import Fraction as Q + +def plus(a, b, coefficient): + for k, v in b.items(): + x = a.get(k, 0) + coefficient*v + if x: + a[k] = x + elif k in a: + del a[k] + + +def left_op(row, op): + out = {} + for (variable, word), value in row.items(): + nextword = word[1:] if word and word[0] == -op else (op,)+word + out[variable, nextword] = value + return out + + +def scalar_inverse(g): + if g[0] == 'warp': + return ['warp', g[1], -g[2]] + if g[0] == 'add': + return ['add', g[1], g[2], -g[3], g[4]] + assert g[0] == 'scale' + return ['scale', g[1], g[3], g[2]] + + +def programs(w): + a = w['A'][w['prelude_events']:] + fw = list(a) + at = {} + for i, (pos, reg, G, U, E) in enumerate(w['warps'], 1): + at.setdefault(pos, []).append(['warp', reg, i]) + for i in range(len(w['B'])+1): + fw.extend(at.get(i, [])) + if i < len(w['B']): + fw.append(w['B'][i]) + fw += w['restore'] + restored = set(map(int, w['helper_final'])) + cleanup = [] + for g in reversed(fw): + if g[0] != 'warp' and 112 <= g[1] < 224: + continue + g = scalar_inverse(g) + g[1] += 704 if g[1] in restored else 0 + if g[0] == 'add': + g[2] += 704 if g[2] in restored else 0 + cleanup.append(g) + corrections = [['corr', c['target'], c['source'], c['operator_word'], Q(c['coefficient'])] + for c in w['initial_corrections']] + forward = (corrections + w['precondition'] + w['compensation'] + w['A'] + + w['cut'] + fw[len(a):]) + return forward, cleanup + + +def apply(g, rows, dual): + kind = g[0] + if kind == 'corr': + _, dst, src, ops, q = g + if dual: + dst, src, q = src, dst, -q + ops = [-(1000+abs(o))*(1 if o > 0 else -1) for o in ops] + else: + ops = list(reversed(ops)) + v = rows[src] + for op in ops: + v = left_op(v, op) + plus(rows[dst], v, q) + elif kind == 'warp': + op = g[2] + if dual: + op = (1000+abs(op))*(1 if op > 0 else -1) + rows[g[1]] = left_op(rows[g[1]], op) + elif kind == 'add': + dst, src, q = g[1], g[2], Q(g[3], g[4]) + if dual: + dst, src, q = src, dst, -q + assert dst != src + plus(rows[dst], rows[src], q) + else: + assert kind == 'scale' + q = Q(g[2], g[3]) + if dual: + q = 1/q + rows[g[1]] = {k: q*v for k, v in rows[g[1]].items()} + + + +def canonical_gate(g): + if g[0]=='warp': + return tuple(g[:3]) + if g[0]=='add': + return g[0],g[1],g[2],Q(g[3],g[4]) + return g[0],g[1],Q(g[2],g[3]) + + +def literal_replay(w,dual,aliases=None): + """Execute the supplied cleanup itself; never replace it by derivation.""" + forward,derived=programs(w) + aliases=aliases or {} + def execute(g): + if g[0]=='warp': + g=list(g) + op=g[2] + g[2]=(1 if op>0 else -1)*aliases.get(abs(op),abs(op)) + elif g[0]=='corr' and aliases: + g=list(g) + g[3]=[(1 if op>0 else -1)*aliases.get(abs(op),abs(op)) for op in g[3]] + apply(g,rows,dual) + live=set(range(704))-set(w['removed']) + restored=set(map(int,w['helper_final'])) + rows={r:{(r,()):Q(1)} for r in live} + rows.update({r+704:{} for r in restored}) + cleanup=[g[:3] if g[0]=='warp' else g[:5] if g[0]=='add' else g[:4] + for g in w['cleanup']] + used={r for g in cleanup for r in (g[1:3] if g[0]=='add' else g[1:2])} + undefined=sorted(used-set(rows)) + binding=list(map(canonical_gate,cleanup))==list(map(canonical_gate,derived)) + if undefined: + return {'pass':False,'orientation':'dual' if dual else 'forward', + 'undefined_cleanup_registers':undefined, + 'cleanup_matches_independent_derivation':binding} + for g in forward: + execute(g) + pre=True + if not dual: + pre=all(rows[h]=={(h,()):Q(1)} for h in restored) + pre &= all(not any(v==h for v,word in rows[r]) + for h in restored for r in live if r!=h) + for g in cleanup: + execute(g) + bad=[] + for r in live: + want={(r,()):Q(1)} + if dual and r<112:want[r+112,()]=Q(-1) + if not dual and 112<=r<224:want[r-112,()]=Q(1) + if rows[r]!=want:bad.append(r) + buffers=[h for h in restored if rows[h+704]] + return {'pass':pre and not bad and not buffers, + 'orientation':'dual' if dual else 'forward', + 'independent_inputs':len(live),'private_buffers':len(restored), + 'cleanup_matches_independent_derivation':binding, + 'precleanup_helper_rows_and_isolation':None if dual else pre, + 'bad_endpoint_rows':bad,'nonzero_private_buffers':buffers, + 'undefined_cleanup_registers':undefined} diff --git a/research/direct584-commuting-retiming-cover/verify.py b/research/direct584-commuting-retiming-cover/verify.py new file mode 100644 index 0000000000..e7cd0bf253 --- /dev/null +++ b/research/direct584-commuting-retiming-cover/verify.py @@ -0,0 +1,291 @@ +#!/usr/bin/env python3 +"""Finite contact-class cover, without graph/optimizer/predecessor-auditor imports. + +Ross Richardson, with substantial OpenAI Codex assistance. Apache-2.0. +""" +import copy +import gzip +import hashlib +import itertools +import json +import math +from pathlib import Path +import time +from exact_algebra import literal_replay, programs + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = ROOT / 'research/rank7-coupled-586-588-carrier-fold' +MOVABLE = {168: 1196, 150: 772, 56: 802, 115: 1244} +DELETED = {48, 753} +FULL = [256, 128, 64, 32, 16, 8, 4, 2, 1] + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def span(vectors): + result = {0} + for v in vectors: + require(isinstance(v, int) and 0 <= v < 512, 'invalid F2^9 vector') + result |= {x ^ v for x in tuple(result)} + return result + + +def regs(gate): + require(gate[0] in ('add', 'scale'), 'unexpected scalar gate') + return gate[1:3] if gate[0] == 'add' else gate[1:2] + + +def commutes(a, b): + require(a[0] == 'add' and a[3] != 0, 'expected nonzero movable read') + d, s = a[1:3] + if b[0] == 'add': + e, t = b[1:3] + require(b[3] != 0 and e != t, 'expected nonzero source transvection') + return s != e and t != d + require(b[0] == 'scale', 'unexpected scalar gate') + return b[1] not in (d, s) or b[2] == b[3] + + +def classify(w): + gone = set(MOVABLE.values()) | DELETED + fixed = [(i, g) for i, g in enumerate(w['B']) if i not in gone] + gates = {r: ['add', r, 439, -1, 2, []] for r in MOVABLE} + require(all(commutes(a, b) for a, b in itertools.combinations(gates.values(), 2)), + 'movable reads must commute pairwise') + require(not any(z[1] in set(MOVABLE) | {439} for z in w['warps']), + 'a native warp touches a movable endpoint') + require(not any(439 in regs(g) for _, g in fixed), 'unaccounted fixed carrier contact') + slots, intervals = {}, {} + for r, at in MOVABLE.items(): + low = high = sum(old < at for old, _ in fixed) + while low > 0 and commutes(gates[r], fixed[low - 1][1]): + low -= 1 + while high < len(fixed) and commutes(gates[r], fixed[high][1]): + high += 1 + contacts = [j for j in range(low, high) if r in regs(fixed[j][1])] + slots[r] = list(zip([low] + [j + 1 for j in contacts], contacts + [high])) + intervals[r] = (low, high) + reps = [] + for choice in itertools.product(*(range(len(slots[r])) for r in MOVABLE)): + selected = dict(zip(MOVABLE, choice)) + for order in itertools.permutations(MOVABLE): + previous, cuts = 0, {} + for r in order: + lo, hi = slots[r][selected[r]] + cut = max(previous, lo) + if cut > hi: + break + cuts[r] = previous = cut + else: + reps.append({'order': order, 'cuts': cuts, 'slots': selected}) + require([len(slots[r]) for r in MOVABLE] == [8, 4, 1, 8], 'contact-slot census') + require(24 * math.prod(map(len, slots.values())) == 6144, 'Cartesian cover') + require(len(reps) == 1002, 'feasible contact-class census') + keys = {(tuple(x['slots'].items()), x['order']) for x in reps} + require(len(keys) == len(reps), 'duplicate contact classes') + return fixed, gates, intervals, reps + + +def make_word(original, fixed, gates, rep): + inserted = {} + for r in rep['order']: + j = rep['cuts'][r] + old = fixed[j][0] if j < len(fixed) else len(original['B']) + inserted.setdefault(old, []).append(r) + gone = set(MOVABLE.values()) | DELETED + w = copy.deepcopy(original) + b, mapping, chosen = [], {}, {} + for old in range(len(original['B']) + 1): + for r in inserted.get(old, []): + chosen[r] = len(b) + b.append(copy.deepcopy(gates[r])) + mapping[old] = len(b) + if old < len(original['B']) and old not in gone: + b.append(copy.deepcopy(original['B'][old])) + w['B'] = b + for wr in w['warps']: + wr[0] = mapping[wr[0]] + require(original['restore'][82][1] == 584, 'restore edit preimage') + del w['restore'][82] + w['removed'] = sorted(w['removed'] + [584]) + del w['start_extra']['584'] + del w['helper_final']['584'] + _, cleanup = programs(w) + w['cleanup'] = [list(g) + [FULL] for g in cleanup] + return w, chosen + + +def literal_events(w): + """Physical events and consecutive-touch edges, without virtual registers.""" + events, refs = [], {} + + def emit(rs, section, index, fixed=None): + require((section, index) not in refs, 'duplicate literal event reference') + refs[section, index] = len(events) + events.append({'registers': rs, 'section': section, 'index': index, 'fixed': fixed}) + + for r in range(704): + frame = [w['ports'][r]] if r < 112 else w.get('start_extra', {}).get(str(r), []) + emit([r], 'start', r, frame) + scalar_index = 0 + for i, g in enumerate(w['A']): + if g[0] == 'warp': + emit([g[1]], 'warp-A-entry', i, g[3]) + emit([g[1]], 'warp-A-exit', i, g[4]) + else: + emit(regs(g), 'A', scalar_index) + scalar_index += 1 + for r, frame in zip(w['centers'], w['center_frames']): + emit([r], 'cut', r, frame) + for t in range(112): + emit([112 + t], 'cut', 112 + t, w.get('target_levels', {}).get(str(t), [])) + bypos = {} + for op, rec in enumerate(w['warps']): + bypos.setdefault(rec[0], []).append((op, rec)) + for i in range(len(w['B']) + 1): + for op, (_, r, _, u, e) in bypos.get(i, []): + emit([r], 'warp-B-entry', op, u) + emit([r], 'warp-B-exit', op, e) + if i < len(w['B']): + emit(regs(w['B'][i]), 'B', i) + for i, g in enumerate(w['restore']): + emit(regs(g), 'restore', i) + for r in range(704): + frame = w.get('helper_final', {}).get(str(r), FULL) + if 112 <= r < 224: + p = w['ports'][r - 112] + frame = [v for v in range(512) if (v & p).bit_count() % 2 == 0] + emit([r], 'end', r, frame) + next_touch, last = {}, {} + for i, event in enumerate(events): + for r in event['registers']: + if r in last: + next_touch[last[r], r] = i + last[r] = i + return events, refs, next_touch + + +def check_path(stream, certificate, port_to_target=True): + events, refs, next_touch = stream + ids = [] + for supplied in certificate['events']: + key = supplied['section'], supplied['index'] + require(key in refs, 'path references missing physical event') + i = refs[key] + require(events[i]['registers'] == supplied['registers'], 'physical register mismatch') + ids.append(i) + require(len(ids) >= 2 and ids == sorted(set(ids)), 'path chronology') + v = certificate['direction'] + require(v != 0, 'zero obstruction direction') + first, last = events[ids[0]], events[ids[-1]] + if port_to_target: + require(first['section'] == 'start' and first['registers'][0] < 112 + and last['section'] == 'end' and 112 <= last['registers'][0] < 224, + 'path is not input-port to target-output') + require(first['fixed'] is not None and last['fixed'] is not None, 'unfixed path boundary') + require(v in span(first['fixed']), 'direction absent at source boundary') + require(v not in span(last['fixed']), 'direction accepted at endpoint') + require(all(not events[i]['section'].startswith('warp') for i in ids[1:-1]), + 'path crosses a native warp') + for a, b in zip(ids, ids[1:]): + common = set(events[a]['registers']) & set(events[b]['registers']) + require(any(next_touch.get((a, r)) == b for r in common), 'nonconsecutive physical touches') + return first['section'], last['section'] + + +def reject(action, expected): + try: + action() + except ValueError as exc: + require(expected in str(exc), 'control rejected for unintended reason: ' + str(exc)) + else: + raise ValueError('defective control was accepted: ' + expected) + + +def main(): + started = time.monotonic() + pins = json.loads((HERE / 'SOURCES.json').read_text()) + for row in pins['files']: + if row['usage'] == 'input': + require(hashlib.sha256((ROOT / row['path']).read_bytes()).hexdigest() == row['sha256'], + 'live source hash mismatch: ' + row['path']) + reports = [] + for provider in ('base', 'extra'): + original = json.loads(gzip.decompress((SOURCE / f'edits/FINAL-WORD-{provider}.json.gz').read_bytes())) + fixed, gates, intervals, reps = classify(original) + certificates = json.loads(gzip.decompress((HERE / f'PATHS-{provider}.json.gz').read_bytes())) + require([x['class'] for x in certificates] == list(range(len(reps))), 'certificate coverage/order') + endpoint_counts = {} + for i, (rep, cert) in enumerate(zip(reps, certificates)): + word, _ = make_word(original, fixed, gates, rep) + stream = literal_events(word) + label = ' -> '.join(check_path(stream, cert)) + endpoint_counts[label] = endpoint_counts.get(label, 0) + 1 + if i == 0: + bad = copy.deepcopy(cert) + bad['direction'] = 0 + reject(lambda: check_path(stream, bad), 'zero obstruction') + bad = copy.deepcopy(cert) + bad['events'][1]['registers'] = [703] + reject(lambda: check_path(stream, bad), 'physical register mismatch') + bad = copy.deepcopy(cert) + bad['events'][1], bad['events'][2] = bad['events'][2], bad['events'][1] + reject(lambda: check_path(stream, bad), 'path chronology') + old = json.loads((HERE / f'CONTROL-native-entry-{provider}.json').read_text()) + check_path(stream, old, port_to_target=False) + reject(lambda: check_path(stream, old), 'path is not input-port to target-output') + bad = copy.deepcopy(cert) + del bad['events'][1] + reject(lambda: check_path(stream, bad), 'nonconsecutive physical touches') + # An actual added reset between two witnessed B contacts must + # invalidate the old path, even when its scalar indices stay put. + a, b = next((a, b) for a, b in zip(cert['events'], cert['events'][1:]) + if a['section'] == b['section'] == 'B' + and a['index'] < b['index']) + r = min(set(a['registers']) & set(b['registers'])) + reset_word = copy.deepcopy(word) + reset_word['warps'].append([b['index'], r, [1 << j for j in range(9)], FULL, []]) + reject(lambda: check_path(literal_events(reset_word), cert), + 'nonconsecutive physical touches') + accept_word = copy.deepcopy(word) + accept_word['ports'][cert['events'][-1]['registers'][0] - 112] = 0 + reject(lambda: check_path(literal_events(accept_word), cert), + 'direction accepted at endpoint') + cuts = {r: sum(old < at for old, _ in fixed) for r, at in MOVABLE.items()} + anchor_rep = {'order': sorted(cuts, key=cuts.get), 'cuts': cuts} + anchor, chosen = make_word(original, fixed, gates, anchor_rep) + algebra = [] + for label, rep in [('anchor', anchor_rep), ('first-class', reps[0]), ('last-class', reps[-1])]: + word, _ = make_word(original, fixed, gates, rep) + for dual in (False, True): + result = literal_replay(word, dual) + require(result['pass'] and result['cleanup_matches_independent_derivation'], + 'exact operator or literal cleanup failed: ' + str(result)) + algebra.append({'case': label, **result}) + bad = copy.deepcopy(anchor) + bad['B'][chosen[168]][3] *= -1 + require(not literal_replay(bad, False)['pass'], 'wrong-sign control accepted') + bad = copy.deepcopy(anchor) + bad['cleanup'] = copy.deepcopy(original['cleanup']) + result = literal_replay(bad, False) + require(not result['pass'] and not result['cleanup_matches_independent_derivation'], + 'stale-cleanup control accepted') + illegal = copy.deepcopy(anchor_rep) + illegal['cuts'][56] = intervals[56][0] - 1 + illegal['order'] = sorted(illegal['cuts'], key=illegal['cuts'].get) + bad, _ = make_word(original, fixed, gates, illegal) + require(not literal_replay(bad, False)['pass'], 'noncommuting-boundary control accepted') + reports.append({'provider': provider, 'classes': len(reps), 'endpoint_kinds': endpoint_counts, + 'exact_algebra': algebra, 'rejected_controls': 10}) + print(json.dumps({'status': 'PASS_DIRECT584_COMPLETE_COMMUTING_COVER', 'providers': reports, + 'literal_path_checks': sum(r['classes'] for r in reports), + 'seconds': time.monotonic() - started, + 'scope': 'Four B reads, finite h=9 providers; arbitrary existing native boundaries and helper entrance/end frames; no new kappa.'}, indent=2)) + + +if __name__ == '__main__': + main() From e3dc9c1660bfec0501dd7522f44a21746f9b89e2 Mon Sep 17 00:00:00 2001 From: ross Date: Sun, 18 Oct 2026 18:13:52 +1100 Subject: [PATCH 2/2] Record exact publication and Git-free validation --- .../VALIDATION.json | 43 ++++++++++++++++--- 1 file changed, 36 insertions(+), 7 deletions(-) diff --git a/research/direct584-commuting-retiming-cover/VALIDATION.json b/research/direct584-commuting-retiming-cover/VALIDATION.json index d2c0397d86..e302d90103 100644 --- a/research/direct584-commuting-retiming-cover/VALIDATION.json +++ b/research/direct584-commuting-retiming-cover/VALIDATION.json @@ -1,5 +1,5 @@ { - "status": "LOCAL_REGISTERED_REPLAY_PASS", + "status": "LOCAL_REGISTERED_AND_GIT_FREE_OPTIMIZED_REPLAY_PASS", "command": [ "python3.12", "-B", @@ -194,12 +194,41 @@ "CONTROL-native-entry-extra.json": "8f13d77119409c4470da5de97621b06eedd914e5c3736d67e2660d1a9f06559a" }, "other_checks": { - "independent_cover_review": "PASS; rational matrix commutation and pairwise interval-feasibility review; final source binding pending", - "publication_bytes": "pending exact local publication commit", - "source_history": "pending exact local publication commit", - "git_free_export": "pending exact local publication commit", - "hosted_ci": "not submitted" + "independent_ai_review": { + "status": "PASS", + "scope": "Separate agent reviewed the proof and exact interpreter. A separate local checker reconstructs both1002-class covers using rational elementary-matrix multiplication and pairwise interval-order feasibility, instead of the producer commutation predicate and greedy recurrence.", + "reviewed_verifier_sha256": "62b150488560a36088a418be52133298b050026481451a46968fa6cb97ce2248", + "availability": "Review script/receipt retained locally, not part of the public replay. Independent human review not claimed." + }, + "publication_bytes": { + "status": "PASS", + "scientific_commit": "743475296e3ea35461aeed1ec25d0e5d7c6ad070", + "files": 17 + }, + "source_history": { + "status": "PASS", + "ancestor_pins": [ + "20ecf2891d80b5acf18d980b2164fb44ea7faa90" + ] + }, + "git_free_export": { + "status": "PASS", + "commit": "743475296e3ea35461aeed1ec25d0e5d7c6ad070", + "export_files": 17, + "command": [ + "python3.12", + "-B", + "-O", + "research/direct584-commuting-retiming-cover/verify.py" + ], + "runtime_seconds": 170.7573594999999, + "literal_paths": 2004, + "rejected_controls": 20, + "math_source_hashes_match": true + }, + "hosted_ci": "not submitted; report separately on the PR" }, "scope": "Finite h=9 words and declared contact model; no new conditional kappa, supplier admission or formal-kernel proof.", - "source_note": "The recorded registered execution preceded only a trailing-blank-line removal in exact_algebra.py and addition of the unchanged root LICENSE live input; the exact publication export is replayed separately." + "source_note": "The exact committed scientific export passed the optimized Git-free replay, including the final mathematical files and unchanged root LICENSE. Subsequent validation-only commits retain these six mathematical file hashes.", + "scientific_commit": "743475296e3ea35461aeed1ec25d0e5d7c6ad070" }