From 406750887f66d184a201f1ae92e17d3dba6cbf9f Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sat, 11 Jul 2026 19:25:04 +0200 Subject: [PATCH] S5.3 Fable re-audit: machine-verify the ConsRec base refactor (permanent artifact) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Re-derived S5.3 (all done under an Opus switch) from zero. consRecBinding STATEMENT re-confirmed faithful to paper Thm 3 steps 1-2 (y=MTH D₁ = the hash-fold condition; some=>collision / none=>x=MTH(D₁.take n₀) = the two Lemma-2 outcomes); non-vacuous (some-branch is a SPECIFIC-pair IsCollision, not pigeonhole-provable; none-branch a real equality needing hcons). FINDING + FIX: Opus changed ConsRec's base definition (list-match → decidable if) with only 'recompiled clean' as evidence — a definition that mirrors the deployed verifier. Now machine-checked: consRec_base_ false_eq / consRec_base_true_eq prove the decidable-if base EQUALS the exact list-match forms it replaced. Kept as PERMANENT cone-audited theorems (F1 discipline: keep the evidence), not a throwaway probe. QUEUED for S5.4: extractCons_correct (Theorem 3 endpoint) MUST carry a permanent non-vacuity witness like extractIncl_nonvacuous/extractMTH_ nonvacuous. S7 must re-confirm the NEW ConsRec base vs Python. 26 certs green. LTL untouched. Co-Authored-By: Claude Fable 5 --- verification/Proofs/AxiomCheck.lean | 3 +++ verification/Proofs/AxiomCheck.olean | Bin 1856 -> 1968 bytes verification/Proofs/ProbeRefactor.olean | Bin 0 -> 42456 bytes verification/Proofs/Refactor.lean | 27 ++++++++++++++++++++++++ verification/Proofs/Refactor.olean | Bin 0 -> 42872 bytes verification/check.sh | 4 +++- 6 files changed, 33 insertions(+), 1 deletion(-) create mode 100644 verification/Proofs/ProbeRefactor.olean create mode 100644 verification/Proofs/Refactor.lean create mode 100644 verification/Proofs/Refactor.olean diff --git a/verification/Proofs/AxiomCheck.lean b/verification/Proofs/AxiomCheck.lean index 59b0fbd..3d27b90 100644 --- a/verification/Proofs/AxiomCheck.lean +++ b/verification/Proofs/AxiomCheck.lean @@ -5,6 +5,7 @@ import Proofs.Extract import Proofs.Descent import Proofs.Consistency import Proofs.Binding3 +import Proofs.Refactor #print axioms LTLAcc.domsep #print axioms LTLAcc.kbelow_pos #print axioms LTLAcc.kbelow_lt @@ -29,3 +30,5 @@ import Proofs.Binding3 #print axioms LTLAcc.extractConsNode #print axioms LTLAcc.take_all #print axioms LTLAcc.consRecBinding +#print axioms LTLAcc.consRec_base_false_eq +#print axioms LTLAcc.consRec_base_true_eq diff --git a/verification/Proofs/AxiomCheck.olean b/verification/Proofs/AxiomCheck.olean index 245dfdefad9ade550ca43fb2171eea3f7f8ae272..f2afdfaee821d063eb1aa938bd0c5319ac76ec33 100644 GIT binary patch delta 354 zcmX@Ww}F2`1Y^a?nfL8)np$tC$k3`jtMfr*iUvB7^@0s}(@GlcHU(wO~N zynP!;nFIqP!wRT4kO>Ds<~L3#k8^S-vpeI7$tRiPnIc#wYq8jIcCbK_Ig`zu@xkPcY~q{(>@as+WRnkYfT}nFr4696 YAe${1SQ#EbJ?a2;FFNgkq#mRP0O{CQivR!s delta 269 zcmdnMe}Hd71S7}BNHu1zZyXE|z%ltFv-@NRmI$U7%#&xa*l|j*H26=9AtIpbb#^_CJVBe zb4`HqHn2_(Vsm49!8&;sn;EAB8%)PdHh0E?$%^daoD1M$j_mRQ7ohqgprQw$G{|NP U23Cd&W{3$FaL_l9)PwW@0NLF~%>V!Z diff --git a/verification/Proofs/ProbeRefactor.olean b/verification/Proofs/ProbeRefactor.olean new file mode 100644 index 0000000000000000000000000000000000000000..2ad15d2eef3e95e3801b930580be0f0e4a51c472 GIT binary patch literal 42456 zcmcJ2cVJXi)BdJx3U%pGP?n+uL<~Kk$O4K1DWORKm4p!3P?9ADgD5T{5EUVSKtM`V zz$nEas1Za0C*BuW0DW z993y!{_*?omBtW5Q##s3DX;SFWq|SOdLWoc1MogFDKT+WvU;QUTL}GmH)=P%GVYBX z!XbJnM@m1s#w5oZPMeqLvG^#z?VyvZmxQcu`%^<<5IZB#uG??uzvib@SV*&J2dI;B z2H(H=)oWm{E;0&o>3-!v{?UM%0h?+(dQ))GQ$=1F7inen)-oa{Id1rCc6B_E-Pr^)ty-PyYO4RI|bB1rIU$aiX2_Y`3F59aP#4p6j%ilydtv2#31#esdu|Dx_}Y z(G|Joa2fN`pZ(U1zqN!u80|h5tFrTnUL$52v)jCkcE1p`=f{0|g~=oKFn>rnKI0Qp z;wQ%4ZchaCOs%l+Y)s#c=Y>P`&<0Zal7)+xmSF$ zN0qLp5PGhDdGh2c>&@3hkBkfBKs%(}kn^_$sQB1H!#W*$j`5IsNB$cJuhg`l7#MQa zaPUWgrlwZf?Gqwe%{uAN@&4q^L0uRFiF*e4KUp{FEc*$w_yy*|ZWr)u(D!H0XzvTX zO1rAV%$HG*wVY}=VqUskC6K>b_1J8mP=y=5+;ts`O-#UQQhr=Q166!h-uLOa&X)0A zMbp3OamK}rRK1ngo-Zo;GPgEJ6jdqS-asB-Fd^J2D zIP-2@&jvnz8cu(T!I$6RdR2eml4qreQyB1|VC8>QWZjci_z%;K;qVL01b;4QDEKeN zZ~HJHoScgO+qlIUD>1qCaZ883?`Jg~GbX9)KH(8P%x_Z8q2Uf{QRANj`2tW|(v&7g zYTfgaa7jOK4#3W%hF3}fKLB%T^ z^!XvKCfCkXcpJE{6YX`^?)<>eZ|N2H;L4A;9+@Gy^v89Yl=(T_Icapalr&*8`$>nM zY|x$GH2S+y{dI=~7d@Oeq^yggM|k8CdkY|60(xrbjH&CY^_dIYH>9HSXR;|_vAFl| zysxn8r8V+a`eEEjjW+Xgf(p^cGYa~0KHcB@o54>^5?u7qK2nZrpBPUWFQ+F9dfqwl zi?d_pz00Ymg1j&;QqD7HOmd&Zl&)o)af3(f%7>m}(A3n~Z~kn1z?=~V?jKS~`ES^0 zULRkmy9+Oka$i=Tq|KPu!BODfm3fp)qx549N4pdB`p?e~rA~w1b=)PrdW+JY;YOSzAnyb{`dQSo{?Mbi6@NJR)4lj# zKXxnlPW31fbtnq+Iu~;G5zF5T^r}btx*7zzV(_p3JAZsoC@oP`_+40s^RRw~R8jFd zSroG*IK<3lkC5;eVLuiIxd`yLYIwMEg`o2McH{1d``j$ZrGa0RN}h0jkaC_R#l?F1 zHO9%aKIKDx;KLnC<`g!J7AD#6WWavriL^`plz`t>Rr&R2)P+(#e?rmDaUS9vUZCd> z^NZ`(sb4>NOkcm8kmvfe#J#SwzJ4*k(!m#zm6oNiU)0O|Ji9e!l@HcWi8u2r8}j*} zM^0FGaGeuh(%{z+4xBuS?>#=Kl5$Cpb!>OzeaCfdII?A{LeV4jg8h(6 zyZB+Rq2lEL4eRl_8B4*Xf3ClzM#(d;5s67ji7&)?VkV8cKWWf+^5V3ftN(n=IB~Pc z?Ulz4d2iTd$p&9ODB67r@!s2Bjz8PmG`a5{k&(;jzd{M*f@&(i8b5NlBY6$n8U;KQ z_(}Wrqul$*et`8@^vQm}3BKwJ&+*7e`msi!Jq`3f4@WkptkK_f?lVbw-V&dXoMPrc zSsI8wPh4`K?`Y84<{ST>KOBDf7onZL1f8>R%9!?8YAJtdPh{7Q8_6s7Wa+mapa8y_#eB6yw999^jxnfh8Pzq_h-q@_)#hS<3~Hows~TYXP&yD?}ePgzgiC3 z(phvExPK1XX=AG&M>G~pF0rQoIQLt{7k+%1yfRLFE&MW0w%W@7J}*A@nzYF!dP< z{UW&N;aHP0H38??c<>wB&k2y;Ad=v-|){r z9qoCJNU0o9s%h^S}rOYDRvao)Jg0FPT_v0$w zVgHkceMbcNQs20?yb}1Nzi{kBxo_w{@rOUSZ;-e#S4lZ{K9#qMwS( zK0mX5;_Fj|!N@C5-RZEbu)QVP6q9&+?uRV*Du37AoR;sS)S7q*+8LL%X$61#YB=|+ z;o#fzSN$4(8cx03uLccR_?i#;*Y`b9kWT|0So+&If9O%xmfx>tdhs8;Fm{gBi(mZa z`tj$1@ii^3+x;$up7!5u4EISZ!(BN4A^x8i7R}Z1u(~Qn zH`7nUZNOci{R(^r`D-}ingM)I&&cam;Nn+R1jRkRRUM1_cDoB87u>w|XFlm=crn_! zAN^q9cddOjJg8oIzc#-5@jyQfXFNi|cOZXhJAdH%c;=v=2ueR^V&84|``|x#rt!Y2;pO`ie%`6H41%wT0f!?|r`?bieYy zc8>=xR0}cJ7>|${U$6W9aPT)fRym@2P!cqZuddFB<_s2t-kX2%aXb`eampq zx!^R|UHjSj)eps8Y={0m=Uv>lOxqhig*SLVX~fZUAD;m}C-}mH zhb;HL9~Ayb@a1^%J3F`@yVE&Q3E~w7{vyzen}_8D+@3d{&tI4~HoJ;TLWPZu0&mZo z+s=s`;P=}wbx6?dd2`!2kqi7?|IA$w?3FiiPQ=eac}|oCe#YMgf6{UOuzBy)T0BS5 z<68nbo|9ZJ{4D2A=Om1;t%35J{P|~NR{d|zNgR-ScYoJD|8`E|0^h}$8asGSqUVbp z`;G-uA3S-de9416&ksgj3w-+y`4T{Xionl&j~V^f1@C;3{pCpa_-x zx_#lOs})ymYQcSg9`9(#r-3hi^7CEpw9eB$w-X!t(z*W0|as&drr`n}gp7x@4FW_<+L zJ4%WF4%m?ezTyAfmRnWJ#{#r7uUAi-*VzVK?DMXFCE#zku)(rwx7WYh)=k?3%Kyo^ zyEj!2rDckWe(!bD0sfa}+&Wa__WBp#eNOHI|Bu%$?W`Ge`?|^c$DEX&W!)@5JaT(*{S$7=|Dm@bicP(fb5;s#=1b3pH zpGQ7b=h%LG-DBqMvf$~!`FZ5Ul}{dOsaQ$IJc<@O9lgtF_fmOB6Nw z{g?4+E@)QXw-fZp}nH=h@p&t{m&5;XFU!IE>m^GM?uL zh93cu9B0(ILg?GmFaNr)L#!yfq`zF?rJ(CuJBM_u)Q< zdB5Y{^9xqj`{kPSBDfRs%=>juk9|Ms(GiP?rvqo+zclj4^w#eMoAuL>_ss^*yszES zr^OTV|2$0jeBjLc4O?9o8;`Aio_H~E=6#Q!oBp)C*P;i3`v$d8{+WqxG>-Q3t#Wl; zZ{9cilm;rC{=MFELzkJy!?^zXL_nVY9Xs;WzEj64&tv~i;PkJ~{4HZPwtwUV`%ec> z|0Z4k_{GcbBz#KwY~b|o{F%Zvzt!kahj>14`nND+Vx`Va{(h1Ai-Er)4aU{;{n_cY z#@#qAuZ{Tnb6>@LT$*v?Lp>iuAA$eKr^PRveN4|st}D!sds@}F%K2{Sw>lxud@asR z7{~c7IM3J8!I#!$)&YN)SZCIW+wwUZd>KPVzi*8;**t$lUj*=c(DC23zaHRJEM|Xb zr#%--yLAuLaMn5QqsN|Goy0mP@*!a=9^s&Q-vuAwIhuj{@OcF0%ZBMC5A1LM&K|Kq z@HEIVU*`QZ@9SQdlFVaU!8579g6ijyZ;Nv)w^@G>^1ivinJ*KnHy%58;2Z6!zYsX{ zW!~f#0Wa06WFDW2{!-w~m&YI4u&(-*E=Q?9q^0V2x-=Nq##0Xu`l;xHKjgI`?|I&c zb?vhj9sG&1m6d3`}tG}rzS;(-+Nz>3;q?q zuS%;LdON@OeLykzm(96nx-H~(e(!xjNE;QWO3m{lss)wjH}5C?6waI%4!KW_#`+oo zc|VAz;l0i;_o*3Z7d9hq{`?%3pL?F3cW6FTSPa>_KBwQ;l@gzrpg0XZp8aqM^bbG3 z;Y+_?huva7A#IiYoZpK+`FX$I5AWkhc|T`7A3KtKdOuOnH|d3y`%X*@GoM$LIMHAB z!~Wgi&jKy5DP`kR;%KI&od3{M)pyagPWR>g?eP=s9M1z=x|yH(0=H(df6&!E zc2{Sgx}AKE;G4x2vKa@llV@wB0kCddT*By-vh~jMoSCJ)^7o8V4`Ed!m8U-ZoE8i`DIQ1LwThvvJE;oEKs*A2uPS-8~YVF(Zs(Gm@Pd)acKXuX)hB zGU}Nz+tM3+A#9?L{*tmTj5NN|kUCBcx#%f@yzNot_xjA_v8%&VOfduZ4@W!e)}NzW zy-icZ?(CtbCUIO~$fVcNBSHYx$~*L*Jg1Pjah{WMz9%Fm+;P4aK+l4thNqw2IcFN< zREl=y?dLylXr{+0q?7WW^ZnKnd#iG8i=8=;4+me|57}*lw0azldK?9O?)TdhgUfJ# zo|`a#wk3W?GeO$$Zct*dDrTVyYTqD5ObJpy29Cz`@`&`orz76$uT;`gr`x68_9kfIL z*$bHmqR;!BjpLBNZgIOi#U~ef3PD>W^efiKD-H1p>a6^nv7w}s_PJT06X#nc*l&e` zZ?k3b?|ini%zi%$zn{x_7y*9akvwMoA!QwkRbQkwRT<;vslSIS;0Q!CG4iyjHr@ubw z;YRH(^|ljt0Oz?*{%3wg6Myp!1@0RSocHPd_cl8*c-A8$Denf(`}AeM*3H}A;WzWS zNbx@lIPcT{@*llp*u@S!7xK*mK35bP*TijePb@x@c3NIb-g6(zaeLzR;?;V+vvg7Z z@&4|M%YVM+XBTNDZwJo24?3CT=WjP*Q@<1Y6Q27#v1rlf`h6w$bCbP_2>D_`cc;1dYPWOFtSedI z>oeBpkZzwH?RlX0#%~J_)a)-pJL^OHkM{ZoX*lb&rJM49(Ak-<2WvR%CjIa8*{2`t z{W~DXI+b0$O|jm8G;r3P%Nw12_5SU^-Jro07k*Fy{Tp@8^E{9PRCHzVN&eZNP;p`YZ=L+WgH_6K&$$b4 z!lzq#v}5m$Vuya8&Gi=c`4@vf=t(8N?^5+Hg2`q2k9O9Ni3|O6^!nid zPW$60PT9+Sf~-^jw{^qVFGHUjw87ugPV+kuVh^9U=6;~TjH6$2y%U`Ei1rK!I9y4$ zm-VOw`j<~>QJwaRysf*61M5-kOIuyKe%7Nf@I4>a$&X_q@~lVH|98E2`s?~#Uiv>v zn0`Rl9|=4I^!?ABt2p+epY@3T9emkdZafMg$9j|$=##Ja&w5k>KHn)hMSB0XrWwjGw}_UF>(Eo%QI8AKR*%3glY>#w7!M*U!H4 zB=31dJ_mRX@DNL^=Q}fk7oeT%*5Rxa2AFsH~y!Xr}TZD?o@dX)= z_I~ajo{#&7qn-09#g;4&|xG4HcLOTjnl>o;rJ?ocNk;0x)Y>>VEV z@junTCv}Rxks5906$2{7u*-9Q>V%#@BV#A^Z1A1=oeTr_)YDav`((n251ySHRSJ1e zJ>_~-^V^NP%B{Dd$X~?u%AnE@eCs$NCrvzBUbC|5CTF z0R6jw4@j8YJ6N+n1MRGj9e12euAt%EujPPm@{WfqRn&0q*XaMt{-^8c_Lo48`?bOE zI`eh=ZM~J>+^?nWJN8I9`yn3&zPf={-%99T->>B$zaqic@?i8Il^rS%`B&;t2KZPf zUEu%w{ILsF!pNzpWr}@z3w8g3ruK0asM5WQdztoNURb{FWyQ@%MJoT32S**h)BK|Uw{CTwtJ@z5InJ-H=My{W z_Pc;{epL$z9#GDH;2EGdr?d;w=9lMrT+Wvq@NN5a&MxoyCG&y%=>qU|ojWL|ilb~k zaXsOBF>U9rgT5MW@2BFx`4D!0(i?sn&i%FneE09G)!1LdneWlS4<#*~WYust+L`aK zwf^MZ01aopXMykA^F{H28qR#D{*)tcUeNUydFdZHc+ISG`hi>eD?cl~lh!>*)6aZ& zfN%MrW>(!l2jrOVmp@-pyAwaTLviqKYwZOjEWj=f!}uExf8zlxT=Ob*dD0l zGaE-1+cZ24`%3QD{NMNOuJ6~}kY|4F9BYsDFRRzqEa0rSH!|WMw`zDa@I25jPkq&~ z8v2*@#fCZ+23iEZZ+Fiws17|ATryuuuzpwuDu3#|wrWug@cI19K6eC_7}U_?+2=+= z&m*<3ocr~|KV}P?fqT}WoscW7^xE5z%}%+2d-l1Ums9d8eXGyATK|w6U|*N&O#Cc`JmcCuy>fFu4d=WL8KmMc)W4v*zlL*OhXXIVx?r+Z!=up7 zdF@y`zGHxfb6%%`@6*NScL!=X=QZ^^9^34r>(BMlAH8<^Q@Z|4;-Dq2TJ9iCKj(D_ z@MDvoy{`Kg@{IDE^Llv0b5r&HIj_UP*LK~dC3^o+XeS;u<7!XcKhEnk@HGfe_tWhw zg)4>dRr{8+AN@vw@581R|4Qgz<|WVFxsIiQFR{na&6T57p7O8cYb5eK z6MXH97uBi)KAD&N41%-*gpD7CF@6w6eyEh%%FoYY=-X8IRhyRg@Bc)&jQ;#XqLlxJ zZu8o^^*C?Y1ou2g&+mDs)`_a-8?AT+kAgh!6E_VzJi%YXIlt1tSEcmAUaN+4eq{oW zfA5ov0UDl5{k4^yfAw>O25LCxS0VUby?5!UAPwjIqW<6q>+jO_hYV4AIe(vfdg4Z1 ze<}2agRlRJ^b5h7e$KBn@Xb!FyjAxv4RV}c-F9v-(EI27$^>6gooXNG{pX^c`0@R@ zF5N%QuR`!GS+uF5ZeJAIOF?}G^m(;{W`D>~5cU_p-1X zxPKAac}~?fssB8vGR}p4{FvWMkJP=ucCpVgO!;pIt-9{#t>iWBM?39rxp>Si+Hd0R z%Ezzr)tff@Ab1+&8Q+&CHob?w3LXVK6ZFEuhVfOSm4${Kcl{iEpf=MDJ)U*A5PJI5 z8a-`dg|zw`=X!xHT7YcJO7TJ|Aw2Rvcmn>kKK+DvjSw9i7xY zHK7TW8C16?8v1_ved$jVzqpVmY;sP|-#g)WNxRsY0sb7&fE6zu7fdb#x8|dr=i(z8 zb^6#}!6se|oa6cS))hbN;}P_niUadDbzpUWJzqnCry(8_+6C9-c>5S}px>nYT-S_4 zm!#1!#Uy$hoY4Dawc3~W4O`P#7{uR9wA0@WI~qGoVTD_Bfz#hVmK@!n`RkK`b3A^o z+p6k&U1z`Y_dlXT?B#fo((d8$2`O<&2{Gn@Bsvs(OWEJ^Do!_!{j#M-QNq*0B6tMa z`8jR(%@y|j)x74Lzi{GM&}3!>7WwGj4X zL++W*A&=_gS%~&<%>Noa7M<7YQz`LI@TbPvM*4V%3|H-}bF&M6o2`#GpW7kzJin6? zH{2NWk$3nRHZxB2KMMN&8#(vJzp=)1uAYH*=KqA|7rX0z=KyD%T6TyGV0Otgf(aLYG3m(cb&1bRn&;9s(gy=W? z^e+OxB}Vz{p6kn@6x|9rIbd8U-dcQiANRr1ziFMF<@9sd{o z5qm0vnUr-w>@h-q*XKe*N2vInUitAor&oRaIqiu;JNwA0duf7hPZ01l&^gOmmy2H- z?9BweGotEYJXaM`|K<6`22&v&C~76gkSvqwulAY>gf4tsipiPexl)=pEy=#e4saEq~fb`pL-VbSMWmM z;lNkFl5<-3KNolu@F_nG*;fhnOTGnI)J4kL-Ch1Q1+a2?4?U+|%-PWDPYfO!zkMo$6#tcu6AMeus??fczU7+tC_-*;awSOrQbHuMqv>Q6jYu|Sh#^R;m z)?DBm|Cjbms;-ZJA#mnrrQwYm>f>VpUJ5#7#*MmF?5YRR&-~-~jUO=fALg(4$+<|% z+~`vFbD(0Ur*1`!Qt@he{Ls=DkF=jDJ&B)gv>Q6j>xKI1<(~g%o^u}Gv#H8yKfB@; zJM$pVJRI2b`%V5Do&~%J^xWy*P4zn9(U1AEr{nkx`Xu`8qm|v%KeF0KHJPh|TYx)2 z0~W(E3J}+$X%74o54l1px=Y0TzLCRb(_xZpi&Wv9q^o95T;g!?Z zhP@{&2JWARcJA-LZ1;-!89#7qCUEY9-%E%spiYTXt`~l&(TF79vi_}wz%7V(vxjH> zrpKWaIOEmnhx^XyaSj=y;^2UM*Jt((*5ecooN+4s>7O2qlW8CJ=d}OSxa>CMWDVKt8x5@v^3&zf902J%>J{`?#kEmq8K>yX8*ypMS47f#wvfA zU-8e?s=;^|_T2URGwORpvfD2=6;0C(yFJhEMnJ#oeAj?)w^g`^arSYu9d)=x*O+RH zv!3n)+&>FA_jN@%ndR<#^MDsLQTA``RX3jTleiTD=RWCp>+^5u`=n6dmT^jc_)|%x z`Zz}+Zg$`;mburneo0)oZjy5SOiqoB9d7(6b#mOeQQA0q>QglI+0JCl*>_*HE{sP8 z+F76aTxj)NLeqi#p1XezaQgVzn&6i-{ni5Dtk-R)rS{kBxdV6!=r3XK|H67J@e0Gd zu#H#o2!H)QzN}B;Zv}Kl8jSbG&tQB1?6yV5pLRw<-{Ba`h=Ay3yWy|D8|~zK%Kg!6 zx<6UKnYVlY8PY}1>oDMXpwVNjW4ON&e==APfe#qduerX?hhV-~5|qCQr-yx1)vhcM z`AFO+*@18Tx|5UVKZ1wje$oN_L>Hf4)uPMfBTxsTf&clX-_+_F?nXQBC)aP}mLJKPXZ8&-?EA zKX2*|Rf1bXf%Cq5@|@a#>3J0aoPNC8?!wnx8$>=2{W`%{^m68&TG6Tp!837Akq&&5 zdv0QF4bR6peKznuH%`XZ(Q&l%xhVgmuJs`r&d(u3;F84-S%3Z?G|J%jS zN7BLn%2!K*>N?7?TZEtM3F}}k`1jjfFV+hy&oA)~gB``-JO53CRri5Ua6V_t{#U(` z+gV?4!Y8PBv97+hu+|rTcGZu_hX9WPZSrW~UP z`>Kv;3f%KO60RfLgAWelIwJklfIddy$;cI>W5(GRCbWVj=f&=Vj@Ux|bdu_o`YiHq+adSg2zyI`E!v)3H-rhW%couM;tG`jRPj-jm3hBUo z^MLo32IGp}He&gVA-7t~YsuRp%3~gJ{kq%t2&2JonW*B@w8gYF`Z^Ydc8*8Xv%d}Jw!Eu)Htn$Tb5{B@b>~NI{OpQD^27duiUaWs+bc!>8qUvI9pI}vZ`B)| zR}%kB^lt$k4Z8W`~I`wXW}KmnNKU`KVG@q1@)wKBh(D*l84=eo#w zbGPqZ=Agew$hoSF?xN2x2lCAg{Na{+3wVEF^cPr+ddB*Y1->E9E9)zI#ZUOX>vSIY zM_+omJ?~AFXA&d(!ehkK^ZiA}J9K~D=*;k2W_Tptj!7zBjQ5Dq<5A7MUb<+sPvrNQ9U=nVZ!3SXMXVcwc{IJ{Y8I% z%>g;$vpOAU;~!Qg&-oDzz8kwnZLw;&9qn$=U#FDR57he4LOb(p#kaw!K^o5boCm&y zX@}+qYdGr_{eSAY)w}QHAMx&s4%P9~5^oD|H>l484=mH;k;8tFr)N8_NY>*~gg6v{Z$^WLFIRv+GC%mcTshdc zm4NTf&;L16(aRpOKa2T`^~3g(ibvz2D-QF%xSahCg*(94Z||^S`u(U2?X0Kn%is8D z_oJTQ_2PVcXUnY91AbWim-Hd?EeGZbz9sY0kZ@bs;`zFAB zOMt&34aQZ{bMw-j6^=e5uO~tJuUJ1_ckFx$v3+*)84;lo|qrFX)-C=8fFXUdq#8DrMz&HP9#pB#l z2+r}O{v+RCp3J?r+5am_uN`#HS3i{dzMli_T-Q&Azvs}_Yil%cj%U&SFLvqcAD=&V zgRgK$$LL_h$+Qo4X91tTbjcBYKINgE^|$IzO&0KbBO+e}oX-dUxgquueqTh!%f|8S zqx`hE6@7oie^P9)g99e|GBAJa;43QVc7L@pdp+}OE`*Y=PM!YD>7pz0R^++g;yFZ> zHxJCx&ml6Pm-yESk=^|xl`@fMz0CpNuting)z2YZ@TUOyn1!z`4%FmJ(9ZGLz4!yC z{`~{aFWXcVhhDG0^J}m!-vM#DSJA@Md!F};F0(HZa(piGv28QP_-i=rcY!bUtHKZ~ za2XHp{bC0A5|&=E2EY#08{!FnbHF!X?Bj3f{uZH~`>(y9RGX*!8wT9+s`4k~%@M2l zeULlNXFK>7&ApaT(LqZTmGR+ost)iinEAz)O5hWm^O@%o*H`uZRNpUTK#ueAz(?a- z>-z=P=N$0;-8=hXuA`!#^O^ehKJi5#U4H@ON*E8oc9#zP^S5 zXa3}mdN5w!Z*V?Gg3sFcnRZ-%#XcAMbpby$Ahd2}Ej}4&Xa0ZR=dItXX!(}|oabzt zzG}6&DsUMu7xJ6uYz5%&{nX`_HuR%LOWhxOpUaehfAJIV-mDfzPDMq(_qmMyH5ISa zoUa;Gx0mNP^8xlmf^YL@ai7%ypWtq^N8x;?{YT9g)C4a5-M0S+f3+8bD%Y}=@9$3e zng{-MgBxemF3)bB(|GUyg~j|`WA1w(Z=bIG6kN_}!nOBCzk%NO+5h&t>f$%+HS@ey zy_atAcQr(xk8~s#?w>Nz-@JVLHr}5q26G$(z3`k=BS8~nl{@#XK| z^7ot~o-c&YRCWyBe0fK7rDK7x!#^7B z9M4JbZv07kf%+YweRn>SxZ3vuV74llf8vy_R%^^LI;s?^fwm)=k~sJn-AWKk>((?&bfr5q!mhTfB3tl%qti8b9%gcEhw~%S6-R+dYxxwfxl75qR-|3Q0tfQ z^LI;`R|VjI`e;-|`9IY9CC>{ouQ*#G z#zk6mztR)(prUzg6wSeTM-=CQmma01{9i-=U7sf$?n;WE7^D3try*+OjpzKW82U#a zc{;M;uI-COv*_a|OMPyrJw42OU~{%B$6nterzWJaZwf2;nZNY5n73 zQ(LD;j#-pqHO|wjlhgA~U@u-*eDz*l1qQ4}PJbPG$QJc_a1|0H-}4%zZOy z=A^*cf{S0(^Mx~X5^dNM6VajCzew*-1^Z(_V|O-h|HX2o{lF!WyI zJp(C!-=4oKE__CQSt20s1eJEtZ|E>D+TDHofGOv?6|9m*1H0?z>?7l1$Mug%7#*kC zEc&vcKOZz8`S`h}32D_upV+~1V83kVk4?6e23(;={)fy`ev>~8?{z+1FXJmJ^!A6S z)S#l*1wG_X$9tX6j2qgsK&h9Xv*dfV*GE6Jm;6o9ZXO8Wwb)S#dGg!dQvT|EVh8oo zUg~8#^-H_xjf5WZJMmuU6TP8mcY{(d_b1s}yJ6#P`Bnt`^E5uuTZ-{7)Y=XCyFSOz zCuV${F&ARv!~k59Pn?$_vsGL=L~dG>b)>Ty9s~D{Ks)1CZ`tyWg`;Yj(_ZAAz?t8j z>b(8j_I*EYlrF@cD(H)}GTtZ9p5(Fw7k%l_mkoO0!|A>MZvN>F=)1=HOv*fAJo!7C z!Y^?ugq~7R=(%gXNQxVo8XG?%eq4OYq;82xdbliNALHPdqvADuPqTuy&98pQ{#YN# z$9C2Wz1?_y+jwU}Zw@Hs)9^lDYd7TYx;}JE9Pf%B7gtt<4Mk!<>qk(Avj2&l5f#U$ z&zUIwh(6YHQr46BgmLi+aa~eUl9GkhyhL9(^hAMft=BJe$-zCXghAqer*&7_`8%0L zpPtKjeOo-Tp*Igym_PpR3}~yyiQPXWd_8spuCy z%vVz8ZMVd6V938YqBqxsnoHaab-z5ABYar{dLiVaxkp_G_|Mcn$0taZ(rf1lRK*!>gV1#k-yJ z#k-w(qqiG<-nH&^8yAzD93Okz_nv5{ZNBm+^y2Zp55D#8Lilsn-xrT{CdRXfn&S@n zXwY8QmR#RH;->lkD#R}4Au02*UuvRfFQUgc8+wMlaw8=%HY=a@aDPckeaVTbo+q=- z@rHZ}=s*9QeKNG~?t0L3Tm5ulJkr4*^0tbH@XNTdzJ`0Xv)+1*!)^QF9O%ynEdnhC zbwaP(OMfWvOs!q~ZkuPcOK=&lLdcbZLhi14*gGyIMtJ0s_;P&+Td3l(qt%$@ zO&=S5L~!wk`A5n;>>ZO5>l7yA5PI(LU9Sno`2~e z?54gf=*a^ezkBG)uCDD(1^+jFMh&~8z7puMEmD5=e5%*y?nAe3p+Dm!LS2UL+b*N+ zwsk5RdPqe`?iY3WFpKpzy~NocsmL4WAwGPc3;pC5+<1MB_c^4*i@o^S{{NebU6O~i zJ1DcPo`f5B$?TuF8+K-cGHlYkcCD1Ab>|?S>C`y)QKKIVr{{W`mOBxc#u`^R@_jUi|f2mveQ- zA=q=*ePW-)l$f&rpd#Focg8;4qT&>`L{WF%6^*0JG|F1q8?edUzr1H>ZRVF9J^c4)-g*u)KY@cLW#v zEbk~edCyDi<35L!`<;O?u_^JfDx|vq;m~tF^F+J#&-~OvbeaC&ML+k;q^xfPjIW9H ziW@&Z#xrW=M`eTW~7lVz!j$LYb9{9;zD+e7`K zXqWfA^!R60RC0qSAFk0N;f8s}DR?yG>^=$)k8iT)+?1*}MTf-4eHXoyqdg-IJ8!&y zzP)+>A#%BQk)t2%uga3wcFi9$sR{clxr3ZB-q*OUkh+mKcEr^US_~QiJz1cIptfbo zPx7mNeJwWV3k5FiW_)n2#C7!kuO~()o^1G~;F5>DuOKbEzc9X-o0MuKV`91A!^ndE zJkX-ChtBtG89(@c(lG1JJveH~~wY&Eav9?W(3 zvj6ylyfOU)&V5gD-(k=EyyjgG?gmc(8xMG-%}4+JWt7N^|Fz_WagmxEIOBb}^ST}h zqY||(oAjFny?LO4zrEMD3i4Lncd6Zum3U#PW9T)7V*tty5Ym+?EmBNE4T zPl}t68kZ0|$!wE&8Zzb;lBN8w(4h5a-#+0q>#)9G;X224+nb6K;b&a=e^k8roal%A z#QA?aD9?6M@)OVKpzP&)^5uK!=lBMB@n?ds)Qg{b`1udtdsAMZK%+<9qV+ zJ@+$w?@h_iy5;CtUSB%&=Yo=-^T|8UL%~<<#m|22HOlK}J1O-u-u!<@d{4fJ_mm#; zvz_yV@4cxvzq_5%_bvLc=f;65=Q`|5PA^BBim f#NW26EUw{36?FTk_c?xwrsMOt0?<&6Uwrs~7(07x literal 0 HcmV?d00001 diff --git a/verification/Proofs/Refactor.lean b/verification/Proofs/Refactor.lean new file mode 100644 index 0000000..90bd5a7 --- /dev/null +++ b/verification/Proofs/Refactor.lean @@ -0,0 +1,27 @@ +/- S5.3 Fable re-audit artifact (permanent, not a throwaway probe): the + S5.3 change of ConsRec's base from list-match to decidable `if` must be + SEMANTICS-PRESERVING — Opus's only evidence was "the chain recompiled". + These two theorems machine-check the equivalence against the exact + list-match forms that were replaced, so the refactor's faithfulness is + a permanent, cone-audited guarantee. -/ +import Proofs.Basic + +namespace LTLAcc + +/-- b=false base: decidable-if form = the original `[s]` list-match. -/ +theorem consRec_base_false_eq (C : List Hash) : + (if C.length = 1 then some ((C.getLastD default, C.getLastD default) : Hash × Hash) else none) + = (match C with | [s] => some (s, s) | _ => none) := by + cases C with + | nil => rfl + | cons a t => cases t with | nil => rfl | cons b u => simp + +/-- b=true base: decidable-if form = the original `[]` list-match. -/ +theorem consRec_base_true_eq (C : List Hash) (r : Hash) : + (if C = [] then some ((r, r) : Hash × Hash) else none) + = (match C with | [] => some (r, r) | _ => none) := by + cases C with + | nil => rfl + | cons a t => rfl + +end LTLAcc diff --git a/verification/Proofs/Refactor.olean b/verification/Proofs/Refactor.olean new file mode 100644 index 0000000000000000000000000000000000000000..3dcdd5db6de09428a369bd35887d6e64f86ef1ca GIT binary patch literal 42872 zcmcJ&c|cU<_dh-?!y+!@PPsHLC6)Oex5O<`%g|iLEh#HNLSa zOO0F#mx>k>trW|Y+#=J&7Q>}?q@}o2-+S)!dJPXF^m+gO_}xD^bD!5a=Q-y*=Q+=F z@140MPmYgG^7ZM`p|hidABW2m7i3+2ICrKbCr?OKCwjjn&|i49$?bnk zetws5h#tz3(vNKEnuC*|TosnqQ?Kkva@>41-qlFfUSeL7X28BM@JE8u{#=|pzz027I4?<=kLegQ;S+m|KFuS@ zU)huLZR??HPrbH78bf7V(M~>TH$K-m9}|<)5~jurS5^Hk=$Tn-$?4c(Th9tEdVJ-B zagef~{;JvhtJ|3mJyXZ@D{dVcKUWw;5B(#hzUT;3h51MHlt8`$^!}#D4%nL=Gs7gf z-Kyfi`f+~EeaB`@{qYG=ApHbG9VzFWb@L^#v zaNlgS*SS2owfO!_hm@N-|8^x(aOscwNjd+bUDGD^Ps0{PVzH1ezK6dn?8H@BK%{rn<-{ezLAu z0+pYG+HGvTA+h9R_7jG7_V0fGCNl?sTT9V@B=}a|5;2y%#`@sTd9&q((S4bVM!R1Y z__u7DcG`kLby)lYW1!CkJQp;i;qpg(IrwnE=%>c{&6*55J#j39zJ=#kP3zw;`Txv| z(KW2+jvy7U)1xMx9eXgt)Fa~(g?7eZ^O=uU!(4N{WZtD*Sh&>UP{_aek(4l*;uaY% zj(a}(d3ed3DGP7gWUhbGe+k-|7jeyJK1u}!Zmj^$@jAHR^K-OS@EqWw!OFkJ&7ZpJ z3p-_e$eRJaaPTcEvhVP-vnNIW%`ca>6p3Hdn+1K>zdRY*!Fs}6uS5@Xhm`zk=Bxg6 zJ;l&-G5*~TQ&MJa7Y@NI(9XIy=dYrAdSkv9CXRzROEMEQO0 zzv(ePkdyH)0nYgt2EHfTbRNvSP`#M(_2^?B4H)u3vaT;5@sEU_4A7p=Hs}42XVfSC z+mL5bkjnx8k;}`s`P<2eZBx+GcQH>HF>8|z;I>Ouwh-HV%q1$fmPyRn<) zKEw&Ru-YnaqEqU17W8obNxKnef9_i{z#sO-=q;>!G7i~j=e#_!v2g<*^e^Meb@rB4 zJ72LlMXQQ;G2}RY6Fx0Z^Z{=87r=by_?3Zw@9?54z7e9O@(?@nfd|!5e)*ky?wVhu z;t@O??Hu1e_pMIz2QGGU-!Y+A$C-xX=3(Ssjq7f@SAC7bcxR)ZF&|#s6;u0|nbs1= z0<<%qr>)-lo$5u!BLjE|Xv5CEYx~$0hu9y5_6ktzm*=vruwU$CeIaE(E_Py2LyxCk zh1XSa%76F3kk7~5J5AUGk3l=@%;wqUw;t&B>R#fRz*%P&eYfbd!532M5YGk9I@5p3 z=#h)c+FtS# znU^Jo{l0eKQ$(S0EDGuR!iD6EXXLZQiTfr}j{DG9&-SKDoMNEw)e|ROJ?iZ9TtCzj zg~mb3Ja@&W4oyz$S9vjQ@JL**T(jNyXq3Im z{FF8$UxPz!Dh>^noZ%&m=&@EnPZ;o7`{HU*r$KAnkILS6;P}e@DA(&4=xM*_@h2Aj z)bt1GU+m37JL|=J9VX8dOb)Rl4>;?>m#q^!82y`v;6=bWAK!fI`$X1d!6Sf|fi9SH zI)imqaLyO51Ao*#RY$AW0TGBpP<<7rFwo!n*M8RDt6qz~P~=@C_&VM7;(Gy@Us8{5 zsQ=(=vT|5%U^pBD5&j$MKltCw{$_Ac*p2+&`^O^icMoV&5gd9W{|)sY{F${Tj;Iw> zm0#*R>p#apI2;y#OBCv6SOXO&&W9+R>-F3A+(wE+t&)rdS%QbfA-rb z;repcPNUt&4gPxvkDF`UO)?Lo-7gF6Me*Gj-97v0bGD z@t6J5A89w@=ecgOG*W&zdLMq2{hRrVcCM%C>9zOxAa7*9P>TM-!N=>9H|Edj=IfPT zx<1acKkFTv?}NOpGM-rX&j0sZ*KUXEKSg^>&`x`MI1AS3_7=eo&i{UwlXv=H9!dY~ zw+wtAmp8lS3tZyO>k(4c^LXP9l-MALZf96y6}PWmynWK7lz#h(JJHVd&XzKx-O`1w%?JMF<*mPoOuJKiQ>I;i=>+AA zfpfjvxA50bJIszOBVG=i>s^K=!>=&u*G9m7ZB3M4v!uZ|g5w)>xc9>9^YYp7-&3bK z4tIUEu7N%dPRO&4zWVyU`+Xus+LX7tfpa_>yl8ACHJo)i8+~TiXO8zjc1r*(mVGfZuQP%!h)Ed1K_F=Mejym}j}5+2HSYx!{%HpsM_`FX#T+ z2L3|ui&DvR<~1qnT}phMr(el)uGh9u<^QO=x|c5~X&oa>QdhXYXC6qqj>uO>Fu#=wd)8^{@HF)adCiNDS0p7A9|EERrAm3#b0zfcCGbB z{s87vKJ3ec-0B1UhI0Qv{YJd4+2G3u-}%^vy8^ZO#Jb3MmNY$CM~|l)@wD8m{ORXB zHlVusXb1kv%-c?JK1%=8&$wj{OB$(<2m6hId_;EYQI3Z`pCf>0f=;*;_;NM#Ie_yy z7knJ2*ol9g^PbOQUn$~J4E|Tv{X8)U@sat!dQZxE;fjwPuf^H3?%SKGIJLWae%}N0 zSDV*d|E4D`w(`c6VUI_T3wpvoTyr+-cK?530e96&u>qiH&YmleTOB)ie4<1J>%B* zJUQ&S7tDLb2JY`hJL~2!>)>d;K4t@_9lt)YbRq4K_~!%XK4;2qUk%R!PQSK3`_3po4Yxsm9{3Ixt+?ACxSlr-;6KQ{v17FP{E<=?$$!svcjzrDJ~>CS=e_vffuX`>;Qmgu z8-19^kKLD&E(jmD)olf_u0_*@#U$XE(jTEZp);f0LSVB1EP?CBW%VNyznihuUF{f;{qPqM#UxW^?}zpmqgwTf5Uc#-}muGrV%Vdk0);`pl89Y z@fE?Bc9{21MGwc2lw+O}KVh;KZy$SG%zx0xfXCmpJl*&s;W5??Pe0r0zw@vKfiSNl zz>g+VrD2!93+=hY>-YSI{r#I={gRWb*hRf1&~vr@?vjE}_iPbe(vRiVs`I~o=ozM_ z;MM}j*}-@Ao*$P|r$KA1kNVOfab`a;(38G&^(V={ete8}WO>=~{=AB*^jGYN0GJX|G9v)T1KIi!&pB(`|2{Rn?bj!xU6f}G(N;@ z{S^KR>?=#L?+OF|toDmH*LEqr{44y~;Lit*0{@jRudb~VMNUP9KN5W0FJyuL@6X?k ztQ%RCU;MLxzW{vE|J_kg4}5}`p`H7pb+Z=ru>qI(0(h}Zp9 z_4r%Las6KadDf6Joa_8@Kh_ea{1!WmxOu*h!uw5=qstE`bY3?IxK9N5dB3U6=E2K` zAAfT+@fhH|-_-v(=a0viq|BxMOyEPL!8lI5@>j=uHtp#rpN%*K<^tz)JKkrk>3a~I z6QuOdvq?Af8h&}|Q91N~d9Gtf+4J-0muH{O{YutXD}NQ6H&lw~xp=f9S1vu}w@5Rnm zyJ@E9kI|p!c|6B)S=FjC*9Dy8_;1h8g`dwyvLN@rJ|8bZ910-k9JG5wfZa6H z^QXGJDg*!2(Z_ZNVjL(S{G7jq%;!5*yxy6X`C*VTAN51-!$tZj-06=z0l)AW@$%>Q z^!OaS-`|c&`gLFq_&L6Tml~b$K|hAPwE#GuPY;Y3b6meKQv#fM^w)z;7V&tWzbkom&%(W)yu&os48r~U%qPfLSw*!(Q*$KIq0 zwfM*NhWFv;b==%{?s12?=M}sH^7QZ6(fjxRc&yGM(It53UCMv@w;?%p;;YLqX94#O z2TuP|9=I)R!;)5>=gv{U>EB=fZF@cK*a5EhJ{iF2-=q8c-x4}L>K*FO0sf3M7)Oim zg8wr#9o zD&?~vp9eas?LR$(D&;-j1K@a^y?xUceYb8pA{t~o%OJ<`xV2|cR=tp>eTfJCNBPI` z`23NNT4dcb_D|rxVZdiggK^Z}+{Jx(|3=OS&+}*c_xiDvxq7|leH9n<%y2#(r`LOq z7yWmQTy#_)FUBVi@^=m&w97xjG{xL6M4~+lvFI`B*Md9Q13 z@bz!fq+8u;_L+R{&vh*u{GW_^Kcik4dsbBRd+(PD!G9(5=5(8}&(sg$_g>e^!Ed|s z_}ThFI=6Wr#fR$}V<;T*+&=^3Y44=s$bF_0=Q_XaGhJvGd1D;>dHu-iy`L5xUM!d# zhHQ=BFCXSkOGr*qe1;y+zOD%Rqt9;s*zbq2*M&p+DMvf^bxXH=Z~k^baOsD6Mat`4 z<98+Fg+~s(A4g~9@3be@>_0KpaaeHKj~lwogZ;>f^dANO4A5dr{ymD*#I4zA=RDd} z*7^)}8S>VAFTByDl?%Do72HO>pey|B-*PMj&x8Nvz(a?*o~DmRKQ%rdOh}8Tnc|1X zKSvkke?8x&mwLA-{M+Lv+Bu#FKk9F;eZZ|5z-h<2fqNRz4&6@PKlyxFtvtp-?Bu-` zQcn8G@ktZYT*_3jGcQ2dSAzcTjBYV;chIm?wA0d6;T)%zvVyxPX*C{p;2e)_*K?cE z4zV)=IP3nvo~K*sb-w`p#(?jxIT^F`x}S-5-p8r`+SC+({W^eg1mBXQ5g+jTn-YhH zFqV`z_2fR`z437g<73B7j=yh;cDJx<{+2>--IuP07EgTiQ^qCqZWR~$`t!Z11$tb< zfzz*-+W(ZJ`xOP8esz3n!b;t*LiC#fzW5#|!UEv8_{I50%G^jzPV^+Aj4$VN0rWid za#*($7k=qaKT6Tg@tykY-JUy*GJckB%FklVhvCZ)_ThXHJNTKDb1m_4MnlDu^Ev|h z(x=@z-PL^iL$t$%cFy~}&V$Xh47fE5IP+}unz!C&?8VMJFZ}$3RL}Q|#7^GpA!X^F z7@syc)<}g)Yn8p67iG|UvGxN8M-AWj8tn}YuR1U4%w78ib%;ITz-e!n`)0-I_C^8c zyx6<-qfa<5#9rQHBc$0zWQzdvz9|3e4c-ZwsbP@eQHcIBa+eLc3~bg^!i6L=BmeIsAq%Ul(^ zGw3()@(GSA_Zy0k2SGiQ|0Q)#{I1W}Ftiiz)oOop)*;bvXMTdOTzz1omsT6r;0=T*Lhuow0dkqJ$3+J_|?wj;7Z(|`y=MhfPd1=HBoG+Zhyx0Z=c_x zx%64L*NuL%K@SayDQ1ks-a@o4@&39eonymX%3VUO~_s9>&mog7TpZ9$t8~BShExWtA_+&#* zKInoo1sC=4azefoc(1J5?`ZeE150rK!xgCFVCk*s`mQb3@L5%*{eBky&XV)c4u0X0 zJZAkNWgUuBKRh*68RO>Jm$)GxbTp$yyU%}LBMb)apM!R;7uzyk>}3io+*$yfb!c^P zPtW(VML+LP^Zv(UyS`aJW9IBPq2H$h^1S~sZ`xgLx>=gkJtgXz=l)I&C>!_6HzAn5E;xs#Q5U(3We-zre|0z7ZtvRn31F4@P|315SOM&iRXoT{s z4C}>AyY&UVf7X?7@J;^Ka*N)76xxZOUpBu&_m6cY1AIdt_c^TFR{^_ofZv?3BREjA zzX0v558c-9^9|B)*69-PjXphhUa*F`(k>&~&f zKX2FjuRy<1;2Tiumy%lO->7q*?-7Q=&kXSO9Wu`rf;?2&rq+!Dy_{Ox zM$XFoEW!LP0$;=Wiwo<3&&+?cGyf-*He6D-68GGH;YIkOesuzWJeJj0dJuWeFUohn z(y^<)u0-`y@#FK2Mf-m-Hdo3%AEQokZ6M{EmNdTdo2W)Vp6ALr(3iUA+85vU7_wC~ z>DSp@Z>8Ok^DhK{Dd_$S4NTjCTPx7ccurm7pRd=C(Ee5JPnbGmANL8ePW^vdH;nx< z^hJSooL@1J-|3Ke@;Nj21FhzK`!Ux$!C8+O&yfK~YU}p09u-0Vsu>*`&|Z-*Lp$qH zlMCD3x_;K9pnH|yk2!k#aZE&>^@#faZvN^BU4JCxsQz ztVi_k(9`xR1u*dK{@)}s%;>8dU&R6bhs5Pui=uAF}6K3?;Pd=~I5;6+DMy70R{ zg6E-~>)A^;k7-!fF4_F=_pMT=B_=8^b6$AnQyKIfe0 zw(KhV4hL|~n>1V3Qaulyz-edj@_Hlv?8*Z1!wsC{{A|x3?$FoWY~ZXb2Znvs#j42{ z!R~zU{W{w{s~&Kfm*JS#8KA}BYc~F+HnwW&WGMK`!S``@XIXu%PSH0~qjs4`ET|B} zFVFR9#QiFMmz{Cb2DSRq{4R=td+O<0$i*KW)VOy+!$y$z)KjiUjlS5rTVHRZ@LZE| z{bO{+o4$6XOyXLEei^smy=TtqanA!@270O8&qww3n)NOZ&jV8Z%0JWbut?<>>z7}P zw-(oSc>4G3*USf4M)Q5MFBY}!+qtfAh<)sz_TB#3xP!WW`p54*U)#H}ov+iQ-@XhYTrdACP8mRnZ{rWj5^`8I@XMGF<-m&8ozwh=}b^R_c{npFl7VG*WfoFlvOj-CtkfxvYk^bHP?b;08zaq%7J}$X0 zsaWry^|1_mdlw$PU++I?kn*2+#3zI2>i)4lhJmk3>v03V$nm;z*H5<((d{n-&i&fL>EEYS zu^)KQ11b)`-dQ-gHu~51Ygx#jF!1>o{@S!ogvwL?l{(}CAM0c!_)iu8HMOpToQlf) z;C?Lwe9K&8y43@pIe*a3`CqoK>keBb?x`=Eq5AUc!;=2~v17TMiaf7(Sa%yd>w7`3 zyLqse^YcRc{4c7TUtxn)d&jVft`d;Yj-TL@*euV+w-KO@)y!fc@ALmyV@W5a17@*r1g!VkpMnCTEuFtO` zv~zxa(CM`m)y=Om@THE4I$quUqW^!DwZ5d=A2w9^&-wMufvZVIuCq1nl&6-H$o-9;9O6*Ud;M*_aR>m zuYerqgQI22^L`r6^(1td^1J2!#%=vIocSIO{BX*OX;ux7LOb*Qxz1Z|4$yGsdj|Nv zI9r+!sNu|a>Q6iR!Z}@kftUXAV>Y~4ML+No(2!R%1_WvPneU;%SB<{Is{0q}teWo^ z-(Pv3-aprqaPT=gO+BIaABA?}&0l({mhK<(Jp+6z&tLgmx320d3husaq=VM%tbAL-}w3){^P$7mM&ptP7go@99n*4F*hqr#8 z58Sg3eG0i-Uijj!?~@YS0Qc;3IWK1v*8W1DciGU(eX4)UvfX-Ka$fWMOaHhk#`wBb zXX0luaL#Kd z_}*Q1c2A&&b6!(_M6VBhbp6?0`eQcEzF*hx2A&UE?rxkJr0M6prhmt#KXOI)uN-pR zCq}nEGgI%M^V&8_`QLTZh2?tx4zv@Gn)Bx%-9OH2C-_>0XZh*&6{CMQ@XdF*#s_Qm zXH!4!+n2BCH@}vKbDx+GzPXVrGD0+*`$YQRy~EHYy8Y#l<2rV3|9uy9`)#9@-(1K3 z82$4PRqThn1AOPsKlN2@^e^+0_uaXUIl(t=YP~Wm3-2rW6J|ugv-GF%h7J=HjjPVkMojEaL>BQ z-)W{djjHb(qj&{(JgDNs>%?tik4*8`aLz9$`07@i+h^5q&M!Ccgx9y6576*zv~zy_ zH9R6LP{TRD^1=7)%`1Kk(s0f%>JPr{mfgDkaxeXlJ}`BwuD=+#ZH)4B#A{jSf;Ih| zUrzANPp-3F_sB!*-vw;~>%fOg)e>Y6fQ5md?d z0sWZYD~>ih$9A!=1acLi^)`LKoxG;~4=KNCf5&B$uG4-K@1k(}U+2$jHu@mA6Y|8L zntJ<9^i^;Na5w0=C9MG=A?qF=aq{QadU$sBTaA!zw=C{kGz} zsUMsx6gK^LUK}rJ7du_x&jJm2?aAYU$zkBuT(tAP__#K`-|<(li5CLrc)q;-weR)u zCqa~M-Mp)9gek0WYc_ED`}^{5H*5a-xN!fD&viT1d%fTMXa4?2bcnqiFH+ha zosg6kpOO@7-jGCxVsA0~1HF3ehIBJ+^lT{er0UXU&HlnUH(1PiRklJoC|R!~AVHaOqjS zJ{1%1sqDVm@N^q}yvvDW9?viSWxhV%{N4_!>4;&V@s*@#W6Z}_^RsX>PW0dLsOs0h zjcZ@R^BX+()m><3{!eLtet_6Xb6qfetFbOc_8mW7^TSh@BBAfZZ~ysh z{kopn!t-x>TwZ$Ikk1C4voZC%?bpN2?_%lC{rLR|(Qo+aUjY6R(9DIt97@5ho5OkI~%xvF53BhrnGx@-2rn~-H>w?&0guKS@g<4`% z9DZ8!&P_k9edm4J<3Kz6$Zd9Eif&IS>~Vr`!OG56;^zeJ2L5Sey(4;_bN|TuoO>hE z@6exfWJ4|=^tbN{ldX1Tfs9`<+PQzc)_d;S01c;nIrtj?Q!+YG!)>w3Z^}RP>L(>Z z8qWQz1AH^qx>(G?u5;OAsSBov~TgDUl!3m`P~EKZZQt| z-9s_-41KcKbJ8Y<#37@N@}m@ZUqrH`x8IWdck+pE%FtR3mvEQ)NPUZBJ*7E zeBj~0*FBT}lOCsR;8DP5eErb=+IG`C@u9}&{{!Te|B6lg@XU`K==t%<{LP)-$*CQ6jWB->^9>+() ztp&iDCr|C2)_{2;cnNUkaqZ}~t@ZJ-0IvXjXwKDUb?vGLk!PNA{1Qh#{txq9{N$V^ zWp4DXe2t0N=^4MM@hV;&j~`y~$KIC9BHs1UMh^F<)=mR`(}A zyW$l)3n3ql@f|hjE6@9o166IY%`p;uMkT~0vtHy7h)KL!<`T1mgN^*3< zgb8M=VXr4Y3!!(>s3WyM&#ik}7z8gzJM(VMma>snax+cVVkJ@r~ICvih6q92Ot=v%mwp$0GQ#2 zC-0rm7e3<9hX}~`dvO04Jx<}k8K;Wx{u#(PiG93| zq5VH@3Ut$cxh`-(uN z;Fd{BKKlNY3VocT5H~yU4l6U?X8n@5)G*LQipF3j|ob~>T&NUUXC zK+GL`;IDrs+R1l+=KAM!e{z8{Z}Q-Y(uJ65NLC$_U^m`uYs6A5$rB$Mt*+@XH_j z&1|6InP}&A=iBe?xV52%hvNQCF8G>v4Vl~sxQqw)S)_rgYl|@8Z!1&{O*I zxRSqrtMity8@PW^qVk{D=ZnAJHUO#ww}t`d_4)J#P5#pJDiS#Tc=qmdpK)yv`9k#T z0$=IVIeQz&s2&7&<9=krS9 zr$6l2O81M}qIGZWo+4p?`TU;zqsC z2X%pOzw@^vH#;p=4&mo}wD}w*3;gqH9lxzvL=|?6@N+$39V`IsWEC&g)#sKp{=mehxoS$~sQvkl=BX!T-3O*T+a4&!TJAPo*zpq{fxu7Y^uRVI~n5BmMDx;ic$@?-Ba;y{Jd{J{+i) zIuck2K1-_7NB()ot_N4=Pa)!)4LJwo?BiCwUd{h;@Vqyl?+uFq|J#2TC06r)96awG z;`_q0!GEeWcDei?2Ok=5P_f_py+QeJ{qY+2LV}k9=X(MF z4FBv4?pX!rythnM{?2|axI-ZQ~BOS_?rvP9bwKB5eWpK_ z3?xJ*N9-`h5!v@B+{UwVnwMuvf~L zpgp3OvTx~*+j<0Qcm;4?ukAlkXG)NU^LsF%)0O(IwNj*l-8Hi}_uG1&hl#$DT1pSE(>R_ry)U2;dP+gRTe18R zecZ#*pY3U-_wI`5<-Ffz^cPr)dB(hTfUlol|MMYU_6xuFb%PW9Q~PY&$$Mp${`y(? zf15dencx>5V|+ZnyXXJA`y!%S$KM}o`4w=VV({~K_n((GJ@M_ufu+RDf%E$u@w-Ot z?YQ8R!@zxQGnC(auj1C8#}YTSDgO?*HG71@`Mu`)x1XA?Ustl;IH4ybb!wu1U73S< z$Mxl!>&{ue5u#m{ZFWxmDuS2zF4!I!qMC@}zWu;7q-kPY0H zsp9c=TZ~OpUiOIn z4vY`ydoK8c!w(PTeOldq{;sMRe8=j3b6vkbYMH70Vm+Iz|z`H%lK9ALcuMZ<@8c(_*VlSzzK^XF^mzFFtayhp&dmp#MzJ4f9@I#yTkSxoEc` zj>XsgM+71+f)^6+sr28vZP(ZOdkC11rQmDw`?qWK_aHDIc^z=A^{Ebe|Mq8vu_i}FXmx;UL{ zuIP6_&I!8rldr4%j@*rQu6w7#UysoDCE37PUrG;ruv=fB_`8;T@RjW95u@!(ti|xJ z82F#r$yM^b9PO-+H}!k-7=Mo__S>FQe&-BV^y`YmME(v@#w!AO#QmfL{QKTMmt(VY zq!bl>cJMpF7yZ;zztsnyfqUlHLWp*J`Ru&T?|lEfoQgd6BfQS4`@+E&{hW$f@IvS% z{#lZ9fWL;b9+rY{?9#fc_50Sju+K7E`8#RJbISsCd9-sp_AGnTrT?yt^D6>;gXg{a zL$D@K`}uwPlJuJ%^NXppKNE7qd+nGr$zQ{1e=hjaKPd^d0+;dd-cJ>RFKNXe)&SU{ zdQo$KiB!MjfA>t76T=14Xa3)LXm5+UTK<&+=X04mMyxtt54en1F6ITF%UH6M zJvR+lYO|pqHCpPrhS%R*f9>FRKDOk8`VMj`D*ChiT5{Hs6cG06NU(3*%` z?|bjh1(y4$`Pf(6=c)KPK?Rrl`Y!F<$6~n@Ab@d@<~C4rjxa@YIw_iu`y+X{?#S}e zqqJ20Yv`}>d#KUwl!U3V+RI!GQ6sLN`v?`#Kk?`T&epqkE)&h7k82<)*UZ83u}SP* z^n^XH?2ZI|xWSBP8ywxZfO>e%LmC3%zUdhw;^Wd&Qj;t1aELxP^kjoxy#JBn@J~vo zh?s%<7NXs-(L5d-^F(peI`&<1BJ!ocY0sMrUr3odEpWcz;#Yn7U>u}OkyLkVN@{$6 z_13ogGSU>6`YU=ZFDO6lpoQ0`rO%o4+D_px^j_kgfRz8AgZGPs&&VfB6y!5NrCszJ zI?RK157;?!#+m-bYo*b^YW&{C`1rWVBVv;##%nfwF>~h4y?< zk(YMP&l0cprovzxv{yb0e;fH=9Mcpr|B4+!FIDx=j&q$)I5k za7aFJUWUzAaq8~ewjuXuA9MH(+&2pCjCb>ut9q17XlzbvBf|V^vGf5Q*IRzuX&+}4 zpdNN(QmYp^-<2@IJ|Q_J(cash=8Cr`8(&XOFn-fxj~V-DjD2!KYT8|iv1xIx4t7(E z_(4B&z5M8hen|Uz`ZfP^)&JgcYIQv;WqQ7bW><;h4f$#To~iMPd?xJ9(b^?HIDbf4 zw^QQBr^h9XOPHLHHm!ehik`OSco?$gQ38F@d+#Xj+WybCq*3}~ohBdKS-16eZphcTPWMkvbSF%XuUrfbMS4EvLeIUQMusG2EinIAnCRoWO3L*$ zA!%|#QheXEw3Jja$vi|~G4zy!Zf`z3XZfMMorFQ+!S~r3x;=-q^ZvKqZhXEW9ubRF zJfc8FiOAb=?$+AHe(o}LJRhkW}+uilf}vf&ERFM3!vNLfGnCr_Rn zAD7lQBOy7Fkq~_)&{F~WMz_D({AXXg??s=1`-Ux6ei*vVBWZfd_^tNT9&#e`k-%Bc zmJWaG*oTv*?-5+=F&A3nGb!^nKEs`yV!ZBJ8Ke~t=ygGF7HHwxqL0!_dw)i~LGr;k zNCVZW#hsGuj>on|?4#YK(9?BE$Cgj~wc9A{26l-!Y0%4+^HrZ0VP5Ub5ASx?9q)GL zjoxnbS>yWCe{yVUYC_x%zgwi8d9Ww!{PAJ8y|j7>{HgK(1H`$K6S$a};|}=>(7~6M zU)eeCS~u!p9+EO2ho>id_Jn$TBVJK)8~e=FwB)$lBI@BjpOpGilhZxFm=HZK$Y+86 z^Uvw~!iMc>4m~%lV?nUn4*q;l;g@ma`c~}K&U)rG4mVtvL_&WIXa;CDsAY-rHx!ip z79!6aTD$nidCU40`R9+#H%|Db5&Ww$4~8U>Gs1I7Cl5&yzoV;dZUdHlNFiKF%*v zuJ=Qe(_$)S}<=bMA$ z6BA=Sqo({|KaQ2k&pUhfslWcrXAiTV7_`#|q2dSaCS^U=`_SW*13f>DsqGj0+NQnK zUs#QPJ^nHElwD({A8FVj=_;S&`&2;A?xXPVgm!z+%&2#bdP7&Kb~)!EdMQVH#vO58 zedBC5^ZG;L>a0PI8`xLIDEkBzYlYFZ6$08@=$Lk8x%Igc`hxIAxMlvQ>d7n-A zYbu^mprwx=K0Bym!kGU{-$?yFq%a$Y*p~%8d7!=KAL`O9{~eCQKB z`t?e&)?S@{cZ>f`zio9TpXlfQ*`c+IeqS-bI7ln#uf`|x*=Tob?S_1fzxOrX<2^2U z@_>~1De3V^aq2Fl#M6*5k9_E<)vEJ*U)<|5>#)9G;r}(_y6sIxiO$deqr*7Y#82GS zO~r@jw=#Cqk8^6 zW%nKb5uDco7E8H#J6QVVb$o%=uhH&Pgmcybkr#g6fAQw8sD@w9Bj%lLo${OGMJoD* zpX0=NPzt@|3xmAyR~OeP4HtWJAfKhRiyYTg(p)^hvf=)GIPMP@;(l%x?qlZQK3)dz r58!$>2J5{Y>t7DW(~17`wEn{lFEf2q918su&B620QqV$;Uwr+4=UC`S literal 0 HcmV?d00001 diff --git a/verification/check.sh b/verification/check.sh index b188c4a..6654bd4 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -17,7 +17,7 @@ export LEAN_MEM_MB="${LEAN_MEM_MB:-4096}" CORES="${LEAN_MAX_CORES:-0-3}" GEN_MODULES=( LTLAcc/HashExternal ) -PROOFS=( Basic Completeness Extract Descent Consistency Binding3 ) +PROOFS=( Basic Completeness Extract Descent Consistency Binding3 Refactor ) # Certificates and their exact expected cones (observed at first green # compile, 2026-07-10; any drift in EITHER direction is a failure). @@ -46,6 +46,8 @@ declare -A CONES=( [LTLAcc.extractConsNode]="propext, LTLAcc.sha256, Quot.sound" [LTLAcc.take_all]="propext, Quot.sound" [LTLAcc.consRecBinding]="propext, Classical.choice, LTLAcc.sha256, Quot.sound" + [LTLAcc.consRec_base_false_eq]="propext, Quot.sound" + [LTLAcc.consRec_base_true_eq]="propext, Quot.sound" ) free -m | awk '/Mem:/{if($7<2048){print "FATAL: <2GB RAM available — refusing to compile"; exit 1}}'