From 43f2c40cacdad6894d077987d7c8d874cbd25545 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sat, 11 Jul 2026 20:23:49 +0200 Subject: [PATCH] =?UTF-8?q?S6:=20Proposition=201=20(pin-store=20safety)=20?= =?UTF-8?q?=E2=80=94=20the=20last=20theorem,=20Merkle-layer=20share?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The consumer pin store (§5.4) as a transition predicate; the paper's Prop 1(1) fully mechanized: - pinAccept: same-size ⇒ root match; smaller ⇒ reject (rollback); larger ⇒ consistency proof verifies. Mirrors sthstore.py. - pinAccept_monotone: an accepted step never shrinks the pin (definitional). - pin_prefix_correct: an honest advance where D is NOT the prefix of D' makes pinExtract output a genuine collision — same-size routes to extractMTH (whole-tree Lemma 2), grow routes to extractCons (Theorem 3). Explicit named-extractor form ⇒ non-vacuous (pin_prefix_nonvacuous pinned). - fork_distinct: the Merkle share of Prop 1(2) — different roots at equal size commit to different content. EUF-CMA transferable-evidence is signature-layer, OUT OF SCOPE and documented in the file header (not smuggled). Cones: single hash axiom (pin_prefix_correct adds Classical.choice via functional induction downstream). 33 certs green. Fable statement-audit: matches paper Prop 1(1); Prop 1(2) scope-bounded honestly. LTL untouched. Every §6 statement is now kernel-checked: Lemma 1, Theorems 1-3, whole-tree Lemma 2, Proposition 1. Remaining: S7 fidelity, S8 freeze. Co-Authored-By: Claude Fable 5 --- verification/Proofs/AxiomCheck.lean | 5 ++ verification/Proofs/AxiomCheck.olean | Bin 2080 -> 2192 bytes verification/Proofs/PinStore.lean | 93 +++++++++++++++++++++++++++ verification/Proofs/PinStore.olean | Bin 0 -> 106984 bytes verification/check.sh | 6 +- 5 files changed, 103 insertions(+), 1 deletion(-) create mode 100644 verification/Proofs/PinStore.lean create mode 100644 verification/Proofs/PinStore.olean diff --git a/verification/Proofs/AxiomCheck.lean b/verification/Proofs/AxiomCheck.lean index b587815..baa0878 100644 --- a/verification/Proofs/AxiomCheck.lean +++ b/verification/Proofs/AxiomCheck.lean @@ -7,6 +7,7 @@ import Proofs.Consistency import Proofs.Binding3 import Proofs.Refactor import Proofs.Theorem3 +import Proofs.PinStore #print axioms LTLAcc.domsep #print axioms LTLAcc.kbelow_pos #print axioms LTLAcc.kbelow_lt @@ -36,3 +37,7 @@ import Proofs.Theorem3 #print axioms LTLAcc.extractCons #print axioms LTLAcc.extractCons_correct #print axioms LTLAcc.extractCons_nonvacuous +#print axioms LTLAcc.pinAccept_monotone +#print axioms LTLAcc.pin_prefix_correct +#print axioms LTLAcc.fork_distinct +#print axioms LTLAcc.pin_prefix_nonvacuous diff --git a/verification/Proofs/AxiomCheck.olean b/verification/Proofs/AxiomCheck.olean index 08b26f10d2f1584d624c77da920fff9d95f0b884..bb38c86919756d5f2a4b0ceb948d9a4fdcdba865 100644 GIT binary patch delta 337 zcmZ1=FhOua1XBdZ#;C8%lk1r!IRY~Cf=lv?QYSB9maz0-Y4D$xz`)=cz!CK}u-b|N z2qYL787iRSKqedjncujfJnqSnEa8kZCa+|PXR=_O%*ATQnZXJ%s$+5>t2^fgDDT4L zg{e%<6Re(Aeoz_5757GkwD-KgA delta 271 zcmbOrxIkb+1k(%ljZt5jxxR5RKmga|gDl~b6<8yfPOwa_VzuM^!P4MAErEeSV)8*& zcTNXZ2rpr>Ae+0=1SoF}MdO6d0J894-Hqu4+vF;CGtM7y9Xr|G83QIWa)@&_u)|DI=ZCu6cX#wC@#% z(o+C(q#^jbi!Cm3SX_eU@smsGGX&^y2m^g};>6Egoo< z0ZpQu#`iq`+I4ByT#bghq<=2RH_cZv-{ulc?<-vCDWU$OU8KeJKMhIoLo_{cNyGaj zBo0X&o;V~9fJT(w9NH78`#Z99#<$M1^$#g7rMD2+NekldK1pf-`qb}J9}OB&`pnQ{ z1zk3HUuM~vk83Ng=jqezY;7MtEGE{MO?mB0hrX%tLyzVAr0qiLqdlY?U!UKK5tsDW z1AVo|rT2g3Ol6mqi<6$$Awgk5B0_-4jUHtEdSG>*VJIs?3n@ky;eOhp1$!B1wr}mh8_>-sPLKx zcQ;)-mUb3_zoakV@BWFy2KDI|pFBK%h|feBPm59ad(_4vOEc$JyG?zp7o@BkaYLVE zj@K@XhZB07mHO5ybGqL&rAOh+E85-NVXL1wZF@iBDSm#P>hWvb{!xwo2RrUCe@Pwa z&kY(5dGWTHqtZs_^!^jX_$FZ}d5`Y{^v>GrX|S89|mLsL{g)Jsachtwcf zUV9^$dRh;Cx;@#@Gpkyhr@)=v zXBC%Lr+x9=Tx>%RWuV?37+}huHy)~8i=)v4JrTe!%sKX{S4hW$Eoct|-@b(f)9H&^ z7x@4G9lc%B5UNXRdV_6{bAVQz_H~g!;7X2h@87Kc1kDidrR37Up9#9~oi7Fl0oVF^ zW}e09DyYX72M_ezjfx%pPNjo`6@${l{z*CheImUoy#J^?3k%WX775y*=&}}{jDPf4 zF(^H(!=$Xoed31|i4R=lA``p z{ZKC{$G=13)9Z`5pdOd)g$_0@n>qE8(xcg7j7Gbr(|cV#eC>7o*V_;Ek}|*AwI-MD z59QOK&pmJ3j@`4}-lbOAOL}JKDqyPUcW)cKF626?)E($@sd#24`WP|7fTGpUqvt zDW$m+l-~q9lECK%t@5~|J0I*}ycB;1>b4to&;$OFSs6w1hmljKir)r)j(7MAdb~OZ zclsnG^uPQrtiR;9g1_*?en!?HN`+}vpZgH{=K#OrQE_D4NI6g2X}5h(^gM~98}epbpq%j}iZ!*L*`zK#iT17e^^jfbI#?q3+_&~~5QJ=|-ihkCewB4wR#nW!cBuo$h% z(<(i`Ezn~FEtl!M{@td%`>2nb5Kmjj_)gHxvt*{ zy)Mwc)m!#9?YrpRzH0s$J!ofq$1dA5offM2vW}2)?j#H%SKfZiMfLb}negbK>5-+1 z;!^!Yqn-Vnu>Ek18dN__T2hWf$E4x$i5N*aAJU+&&tG5f3Od*GfzqY)aNJ0l56OuM zaqLg&$%1??X!p6{jZfeDv!&uu_J)S)ez4AsoY=@Wa;hKdC1rfx76UBpje@?{%k*6| zVtnfu_G3r8rqg@P{B2$}{8!l#90A-3>arc&MqZ6RvyOD^|D={mJKWGS<>r@z|8akJ zTlMukJ&AsL48@TDpn-#5tK6@C1Gmzn;$}fR;}-GuHm0n?gKfa+&z+TRCTRV8uTaer z#!)qB^|?Sg_>0fKTukTk_7m(ty9@N=i)BtSHYMqg>Q95OOZa`o8Ru2zU zUvO& zTMAD>o~8kR@tYSGGRIZi*q5?N#VrSX9mX`9B<*C}ZUC>cY}0tgP4yFrcH*ZS4jM<@ z3J)ov#~~c_LVUdoPxHe9`~!3JUg<|B^xJ^{*lhT>oa;)z34S_&m$!a+l{G=L;~vii zNSPE`8SEDq8{aRkk9OxgeAo!zWY?V6^!nD(Ea*Kj>l54R%5Qqhs)id4CG(DNe`C`X zjGOA0u_mQYEfN!bTXxw`B=r5S_I|f(&w-6fm+Hsn*H1CiWu~aYefLie@NEh$|C-jn z_fmH7yn)oa5zx@5tpUm&*8eQ%>p#&kaYSa)U8PXjunxbq`cBY|S)9JmU z&%e19|5bRf6?i7-&)GA>Ip-A~20L?rm)~(Hfq_?cmV`1=ovw!V7^D&DhX;Djc9_|a){`zaHW{OSeV~&xsGkucl%9P!ykk0@Ojc)#x^E2Za z#i8tWqg~VKz4~05DCcXi2RQR0^_9~X=z}I7Y%=M7GrkG)n>S>974FM_@Xc_2`4#7+ z!mViM_;tJc))mfOg-4=)JNU|N`+lu=bEa9V;=p-B%K4)mwMst%crN3D9!tJKTMT1M z?Nm-{{TOr5&U2f9Vogta1ES->hBBDvm?wX|aee_~rtAy@PCqKGI*?DU8&2qt1mE99 zzInSSI#BX%8Q&owB!3x0j%xMi$go@$W{2^n~#~$^Y5-d{#Y4& zf0E*Po}O53e=hapLO$drJuZFMG(FpK(sb|h4HeG_v~xZ{EvsuuKtzxxregT?Pq6fxe2|c zogP0sJ9VGbN!pnT+*DSN!yCp86Pb%@+=!cjw`_T`Dd(!f(-221@b%_Ljk$I!KRLfi zDcdqJuD^VK#rq^D^kfw_|B@DVYOeC-d3qB2KgkdkuT042fQI(H`_-K7OMU0SA?0*G z8H3|4_iDyV^+VrDIXRmD}BBSE%FNsfta*jp=CT zc*b??&eGtW2h2-S=BM^hE{b-qA{VV>Zm4+i|D;T+4sio~fztH&>PT26Js$5H69z|iS~yuTJx|XN zKRp)6+d$)AYIFMEYvZpWp2k$PGyjJ4{mwfUz=Jb@GygLCKIqE)d*1ka>toyiUu}fG z06Xr#Z$R&^wYO*2ieHGyZQ4o_LzE z&NDvXdnfAb7MVY3Xg8tW#C5Xd$sYsy&jer7*9ZJ5^Ct)Skpn!s^Y|;A6RLkh72QAD zSAF2a>zq4Y9QxV+fr{_``!xF^p(nY-pL=9}hoLw$A9RD3+>$3zdG#QInoa|aL$v)H-ZY%XEjea2BaMGcJV{vVurO;)spH| zp8M*gshS?2C6i7R-)Sj5S}`eo^n;W!iyQgm(WX}qCtdwD%v%j z-m7L%@_79Bx&2r=kLXK2)eq&fp>OoWI>&}wy>eOcJkMU6pB@k7P1SY3|9tq<^7Qs) zUsHPI^D@>e|MqCesdnXGB>uL879UZdlET!baEqV+L*IYvM;-Oz!KskT0NwH0zk4)) zyq6{)ob88C{OWphS&we`;eS;bvWqoe)AP)Ii>jY8#;QXZ=ZG45e8T?dRba{%w$B z|7neHosj)IfV1vYdEY)u=nqZ@9*O$(WymHAYlyPX0z3=!w{pi`WULg<`!&iZ4LIIQ z%2R(xP2K-}w^Kfr^109(4tz+fRwFqkN`D6O)&l(WvYPkhKE#H0*2T=K88-_?>Jd=# z9@Hxb_wdR!{zxUQ$2l7~^QiNQe0O9XG0!N!ep3Hpl-K%s&izB;uzvAFVur`* zeW5>J-HE8J$8S}w&fTk(f3OC)F&gdkq5b*x+`_1M_@0aLxp;xexANq58szz0#xk$v zi_9BkFV7T7xt^=~=zZSxafHv%~A zIbC_yZ<-z6OZk%ty;0yRQa)uyo_Pj533%$mwGEj|-tk2pNd>;mR{Jh<&Wod+b>vo+ zuG2yypY)%O{LThn>$q!Ux&Kn~j3=MhT|B$63FE2o2*?qSYVq18>0fAFJw6ejU1uM? z@-+XVfZu#vZp+jBO9FnZ%Y_Tlzf`o-zlT}2m!y9;U|$CKY7J|9N7m6$#5WuG&Km1G z$o#*7cFvDJ?Y7?+b-=gJ<8$lrGxLAi-IV2BDzrE}^SnQKMBhHzS?Yjc`cN<*0wU_^ z@rnYSaJ=Ns{a+<|&s?>58&lBE7$+9a$n$(B4LIxGt2Htn^ZZDSS0-?dcjFSZO>(?* zfU_>fzh8K&jF%xow~z7MA5r)v886lw>Tedgw6WA533=Mrqw|qc)UV>j$wSJs?bt-t zlRj#T+$X{>ZrsnLK>yV8A5KoZ-D!?uQ*m>lopJkf{=bE&LdC`HXIJmV*B;8ad4Ti$ z>$MfT56JZ*8n~&x9v^$lvTJ2r!hoBB_enkXy~rb9on~AM7`9iFakE2?<8rdNW7Pjo z-0IV5Jubd_?1KLNjmj5ja%s*(#irtR1MQ4k{fKjys6xdpw1Ms~$Mf$ujeBI=B7oEG zpRZJ@862r=Q1Vg0dB6P2|FU<Jy`sm1`SQxRV_o5nk`Imq&Um&d`(B)kXEboe zW6GlB8ZsU!z!~pl+2tz9cx1z_H1HkxU$Y%DAF>gTOyC37x0zowQn%0>FYJeMfH(N- zez8!2hXXgfs{2{)M%}f=fU9`2ZjrKndE+^>&zQJjiRx9fxS@KN-hWkG?V-B9Na#J& z{pO~KuaDkS3>t2h%}Ac4DKS33CW7wPeZtSe!_vw#;E_u)Uqg?tk3uX2Ik z`Sw)L5&}=dePu{v-OqNF))goTT*Z^)Ps%*d&f(r366b#sXYgJsu6z&00==C}7D#)g z=>F4+LBowHXxIAiUfW#xKE;0(9-Ia|1?QIoF7{t6_e+_;qhbGBU-wIv^DhTD=T~3P zRuk))@{5~s(jw@5aGXkO{a+@x@`rYYne{kL|LgLSnMLBuDlz3x6xw;-ad&N%I?|sc z;Jm;2`L#n`d^$CMQ-Sk7tVPY_Xt{r6{bkq=rm2cY#f9>u)MNA0V``$u!3_HGy5!%!d0_TFpH=aQMmx{DQf3D-g;czPQ-Cub z`+q;vLdGM_4|fcGB`Oe(DEUl3yh2i??c9$mKMH`Cl(pA;o+W%yY??k_Tnw-2eqHQz zz4F1^RVM>CMxdSJJN%9BYoQCTKT*Kx&$-7_cG4eZ5Bn!&t}1(IjVD(1vN_U@B;an)qTg({$hhSoZXV#XekeJOW31w8YO4G1tH1ZRY?0>; zX5f5o(5?C3Ief2N$!8<4tl<0o+AFW;kJK$xcm{Ag@GTWq`{t#>Eq>=st_De)88d}D zfV2Ng)s}oI?RP^j&%0L5OkX6=yIjCMpjR%RZ_ga@+Q)O>W_ldPG)df85CK-W8SShq z|2*(ilKU(t^jg8!>D0Cqxlf@kQueL#pk3=ckEv8%`SQUDec#Ud^dH;o(>Ik#8g9%& zJM&>lD_3`ztMFhu@LbSZU#v>yK0=eZ$9hg03SqU*YtN9i$9Q@@q)tVpUE#0mar&uU zjJ;ylUOj*tqtQ;gzI!hwi#n8DDZp9JuHQ;oX^hl46rKj$ig@;@+a!m1^gO#``t|Fh zJ^DrkAN-%^?VMjZ&_8g{&{2onIJQm#At{$%iQZ?s{xiZk~oPUt;Tv(WwYeMP)y=^Ad#^0Rl+zUghHy}7`- zKj~8UdJ(xl33*fZm-~}ne%ZY?FjCi`;>`0UQtqpCOVy_mo_q#D+3R}`26}hYjEp(7 zWukWqD|_u|XMBr4`0hPvuhY+-)ZtwV2EZOoKG+4E{zP5+-}yj+yMgm_h4Z>B{31x; z;lMqh`MS5;F7wXLctz@QnK#eVHJ^~rMBbQz|Mp4aB_RS2Vcr5y>VE9Jyiemfq#b$P zZ_=h)Ql9HP@1H%9qg%@R08+Zu;YkM*A2sPVNn&pUroQZ_s?;8Oa{!0n*dCRCXw?K7d> z37T7C@+-2wyU@=2t{&gioW`}(>p$Yk`|t_h#0GIM35=?>qob;ua9B9 zRyfbaSYMV7KJvEAUpM5LKWAoMvdH}LP(R}I_*|bG(tcA*-ES-SLhfE&CG9r@=Q+iw z!6}cV{mgIH?OWwi!}5#!Art!Lx!S7_woH}wG5#E%$`cyc@~q$JpYdNCSErqvKThCo z(6RYzFO~k;(e43lklApK^v~2Pum4l$E{UXn+B|sXIjCB9o_7vvh29Zgb}#bi;ZE0 zpYKbjgKu-UJsYL{hBCVS?EkmWgm$w3T)+Oi|1h_S>^}>5NE=vSlj2G~bGM9?U zb1^IDKk(B-7jF%X)Pth>ccJc?EV}<)rUVY=xtPLzM-|hX@i@>$dKj-uRe6<;TLtbeAnhEQi0hi+U|9rI-{C{ZN&6&{e|M_Yc^_Tf}oA+=^bfMl`^8b9bg4O4)T`%bV=0e`oR{vY! z+UE@eBgEg@-1ogB!@V2pK}#ioOB)a0xk@zTM|NwGUD*^jMX_kOk)LPaxk^g@o0TZ9 z`r+PWAMql!boYsj;r|+61@nKIsP9X=l>5GTzU2z>eT_;Gykwzn4^u z>`7i_2mK@^)`~`GRQekQJy$DaxIakwd!S-ddbpP%rC%*Z506WRF6oaGdaf+*Tstd1 zzxNDH#Vr%MJg#hxU_le6;T)>qkv8E;i^HJ!-`-r$>GWQUizj!$f0Z4+xS2ZW{xLF_8QY zDfA;rB@~hF0(^ z9KUdb^T~h|>L!0zEzStNuX(4@J8TG~P9I zPcU%he+gaHf4-+qod^0pOWAs;c$>%Tk8fV4LvN9p|1)I|=)Fg&Q}M__yVi&Iy4Wh& zh5vfvVd$jWO@A9cDi;|LsdFg5!hqASZ>De04itVlpg$6P*WX_jmQVOq2%V7@#NToH zm)f=OVnKsOwElecI|cgw=WPE=`x@W;rnr4Zc!5{T?AG$KVKc7EQ(6?ks zz9W4*?3k#Sls_qGr$6Z%x6Gmf;@Pw}r~k>HDadH3hsuhSpJ?_bBF!N0Qd z;;{uI$f;As?_bAK!QUf1pi!Z)|ML6Su}ttUsIuN#IP|~#{&nmI`0stZA&Y07l+wfl zIZsua+DG}mzw^k2UdHcZxwY~Z2Ybie9d zN&l1Ul(Nr~UvFo8i+%H8sPr!ia;!I*$stE%eN6(+^=3`r{^LQB`Uooh5x`SH!y7I- zF4q(02q|-{T^C)4`d8EAn-|&8^VZ*sTyIRN;8D0{?=$Cxd{U(Jcpz`G>V7x+`+foA zJ55%gA7doidEfF{&d%=@rY_}AG;qG(``g!hCTjhAFJ%YULsIT9yw3r<&*VP{Az3KL(0KWm6yyo>2jG?kOw7c#n^C$73{kr@- zZv=4W=e>6WrT@DJnLo;3&M8vPN$vX`+Tn4R*H1n_N`;;_!}oNm**jBo#|iyz2&kVN?&dOT*g`J*uNP{qlNc6VVN zuW`2V2<{WqIPi0}%!>sZ&m5BW@&1AH=&Rhym+6br?}UEhB?m5dp7(g@;umz_(cL=w7F9x_lK(g4AjqP z;Fae(VhTj*_C0NXmjb>~AAH@qAnee&)xIhypa1?L4g8<3JKv)a);Y=VzkkRE|GK}= ze^oe)oH|wd{r3-s_w~3;`*YvNFNFS=-+%uQ0sa-$2JSDCm))R=2TB!c|LDJ;P$Fvo z7=?8>8v0T}(?FRcieK#?U1(Q-YuGdQk2b}COB)~Gdg6h6#+F0v_jPMETCr%j(cix5 z54Y|Y^1+dP^!RXoPoA*$yV^6F0?HmeD}Y0e$+VU0O$C8Kga!V zaI`{oJObwz%!3ju1A~L26{_QgzPg`bp!ug&XqqqD3w!m4VZTlJhB?(^0|g!lxoFT~ zi9h7a4_w88p(ZV=t2XoEH3KBkqZCS4DZb^@m#Q@^ZnGf?0*%J#{jwnaH{eqCMu0CId|ej2I5|J!r1bH57w3%?d_$J) zni3LCO*&QjQjkA(@XgtgImfl z&*VB2(qGrlyjfLgRh-Q4T-X&3zA0PE*JoT*|GeLze&g7QNpc;u`RQMDclZpMcNX9d z&|CWweqlV-{NbLHlzTwi;3u)v?C`DUSqaV{R?y9U? z;g$ED*U-*tJrBMZ7_DPxo^UHS@(0GHw=8Y zKiR({pRhj^_sO(Bxn{A-LBjrM$T2=I%yXPK3VFsS1$;$b_&!Y9&v`}t=dA6Q$oORX z=}+%lyQqv$8t@#@bwkIVl=d42>i+XSzHa4T+vXScMdSXF_7@GdNso4AT8)ez=?+?Sk*YT~%Gi6=PLBEl}U+Xz^fQ(-l@Mz${^=AwV5%G=0 zxTFBD_geLS1q2?3{7VCV{qBrH1qGgoc8*{7!=thb3EW*(_mAhXMZY@pO@Kka)ci0E z)^Y0Jll|owsXq)j?K>7fp{3Lx37q|Z*}CSm!suV?=b4|I(zdzkJwff|tD$}Ri|_td zmT7kR>UawD8>`rUil4Uj6mX*p?R?HTwDy%Y3R9Qz%MF}_<>YbCxh*qEYosCb18fxr26 z`r`TA)4>9_Lp~gQ8&3^bD)S_o@do};_{sY(Kwh)ynV+wac_6S$`XC92bde@;abt%7cfHM#7e$e%I%^vTia6_W*Zwkh-K%wCN!6{GhFyO48 zFBYtSR*rKdaOVHvm*Ypu`5z5D8uPUO7u!a1{%dwT^Bhuso41TZ8uT?d{g?9RO{Lck>?gMjy)6Y*2ovkJP3`x@C!2R)Gsm1Nm&lJdqgU|4m=|$$VildEj z1|I0Tc&~_vV-Ebc0dKha(T<`5cc9%=Shu6zs?x4dfxEDONeACoT{@g823+m8Z(zR{ z4w?nNms@Y%QC#ea4BDmaO$T2t_&N^HT%dnTsgCnLhx*RERcV~8`@G-d{_KzD6`RO- zX5&7J>*m_&gNw*@(>_%9lk4W%l0(0j>!uaB6ZE5E{|*u3;rsob-O3^D`t_qzXX<@? zxwrbi@{jh@zNny6PGO&szfTsR1hnhx2kTt=|Md4fis6rlb%RP7QuRNSUehq$ZZqhn zPlhZH5O@^Yx!ztjbqEL)coJ~lr#Z*2{4q%2slb_s4;PMg8iA{Eb|W4h&L(p*=@OJV=z_djQg0{^UO3qLO#`d@zk zbG8)lkKFg^<8pb~z3(6RpR*|zb^d0@xmO0{b3hfY-sAL$zqL8=%+Jfeo!l~U@Zk7l z-;c3)^*?zo6h1=t|4O;owX@q=@+QepjzLPXahYbCne4Vn= z<9oj1guXSkue^45#Ut-)5UQU{wDb8&v)YILg(@W4 z_ExV!v_GwulG{*#jZn3Nm66f!-5MLK|Z7*>x zPkiT9N}+asRUmSd-runjV?Ne<@s4+J7}}#i%M^JuPsBNZ?_2VBRtA>dUApJ1ZGS;E!`QeHDTLDgU$3PCW9DaSQn_fx^Qep9{VkAI$oP?;I%Hj(HL?TKBW#OT#ohm3o{hX)z> z`==bc2=FPE=fx=@>B*a0Do#9?N`m~Hgi_&chTiw4jEa*J?L3#7SLoj?n4#hr>>>_Y zY+BLqB0f8xyl2F^^uucjsd@4pa>UEGDBV%!b7++Azv%;=_MP4(moIDvV(8fhKdt7 z-_-bWzB+-QJrX}v<|*f^3;2Y8{>gokr`mH61{g|75U{x{+NLuYW;2iw=>Fq3+|(N-}%>QYb@uC!tIdb{Q338p7mt^PTFouuQ<6{B+`unPp3R9QzGaBu7tiOjHA61ZfmO}Zix}H6oianBf zmIj>lEa&01?lO-vfpeVmZ~Of_j6Ldcp=T17ocb~oe`_2F5jT&shaCp~2`bx^! zbP+$%rs?tJogMvjC^g`tkuU6Ap@OdA#x%5Z92V`o{k=XS`uyTLl?lGtgKWOvU(jTp zef}yxS0Rnk`}Nsnn5g?-=lVC1Y3|`K(k?UFX;-}qG2ZVy0Un$Kd#vD#_;|AKhqF}t z>}couG<( ztCf`ZK+g1$?*I4?s?Cx4!}(|ier4f;kL3DbrT@TRZ5(-w_1SA5^2-crsavKd^GD%M z$XP+>6pwEp<$d)Z_=VKtJ&PkTlzg;bT|NI*{v?i-!ab1V`m{Rvct_Sog_|bnew$!l z^@*?iCjB!5r~i8jE=`g4TY)o9%j!4yfcC4rMu z$D3!$I7Jgj9)~Y;RgrN@0dB&0^r^nOKjS3Fk@o}VT7UQ(?N@Q+|4BK<-WS-O62~0$ zXKCEHz^u0~%~vei`jJ26V?7S+hw(`M^RqXp8|n#@a8KHAG9Q*TZ*`U~9W8AGS)ao{+7 zdS-JQISvuP`FVzMn|BuG*eW}tfOB8eDBw`HJmZ9ZlfW0-=I{hj4+2~vdjHu4blPS| z!CxNME;(JJjeOokiBI&&T1c- z4V-xrI!(7@)%K6VINmZIso;+Q-^IZre05&g!}?Es6&7E;LfaKidze>$H!T0^)9gus z{xr~90}DU-!eD1pT3Q|CVxHG-Dpz0B)F(Rz1(Y4s{`Py6$&yw}ykghje=U zgVRv=B7k2Xm0hWn=%00i`~5EU>U<~jI0KlaRwT-kpV@Kn&dhnp5HE%e*5o@D@E z^7gtN-c1?ob7LLJ2LAH5_ph6zJn$R9%T&#YEhBKAt60Go+i37;=BGAp&-~rO!Er+d z47cfuv~lqLK4a7jJ&rH;DL-I;NXI`EhlU&NXy^IPOh81C}^=*9Bh<#j#RsSx?5nu7z zsz2oV%kyadPC>CVpY4_MJWnQm{>yJ$%lLYr-}H%YN7j!^E=&D9Pc{Spcf$SItTURP zXYTK8aWVZ`JsC$|p4g%1pYF+%uHT^d#!sdl6ex1cH$rQ z`1gA`&Q8dufbZ6tLan(jsyK4YNI6D>7zB-Kaq_Kena~sS%DjK(#I{_n*pwcwhosya z4C)&=;$i;rpJ0=k+5$a4-G!K;PZq*o5tI z^}V{3zhSfWIMANHXHUJPY*3f#hkH&^`ZYXeP@K-Cj}O1!B^vsEF4N+#KQ~nPL-DA7 z9B5~rhb=fZSI7sa181I(Idp3bZPMg}vw-t_DgTe23H-2)!gGOh9+)QFITC`xuJB0U zA#-$pD^|YHynw*@9%VT27gwdW;pZfjyanyVn_KgLR!GRZ5nmhl66SP^;pfqx7sr0X z5|cz6eDxw7dIsJZcrT}Gt2vBgHrg4-rYp;L74pG1fHRJ-?>@Fx#xe9$-G9dM_wWq| zWgH`bGmc;6esJw+af|}r_G7tmPm5y`@WswL6J;Dz(N26z_T%d^jt zveY?l1G`m$I9CFjDTB^4Q&asQfx4uidO?SF75ad}L#aOva>SR1mg_6^rvT3c-Mnu1n?=REyMa8&0siBPHrGN$KCu3h za-Hemt6q7>KWx4pucdd}v>7@3?_R#~M?3GE%2ZByS;o-@oZsJ*ee2wL_T?Ra;30@} zwSuXw<-AGv!-vm-=~6aT~vNs zfwRv3z4i~^dlhOt7z0wquP=k=XNME|>Xp8I`P}N8-aVk~$J9Z$vsCor80u2}@ZOA+ zaqz1f^6Rq-}d@LEH2jhb=z;(ayfYhc=F<>B_Dg*lPt}=8i3G>8rx+Y)5`v ztY4);P?)Yk;ZEROhxSg27-s~o?$a~<;_Cu`nclrC@wpT2QT$;zSKxTK!T)H>>`3kf z$?vrf`a>4!{@Xkmqq%ofxEbxt+aT=TsXq$!Gsx!YAoZI+ z)8j(iICo%usowmYToc3iIih+X`Yl6hrPO{$5$uJi}iR+ zt#UbSuls)$RW3bGkIhd{G~`o2x5PBesPa+pWu-^!$C!?G{*J~t@R$RUB38Opuhgmh4!mS zlP3W;rl6g5)coz5rV3M+@+-~Hu8x~qccEV@zP#5Y<-Mt@Z+_+|eZKv34)hjjuwZqY z4L7sVpE2}vJr1o4L62;fq0-!pIyCphr-mQ{EY<8yxCiQ?F>0S{6DE?oA(+Fs)+O_ z1^Q;Ri=1B7y!#4p-+370e!Od!jnt*=$buZ#i(~7)?Je(HY_LBUe4F?GIX(#WM!o0Q zT-c-Da|}<@{VudTn#UE&PT%iGnt?B0{=yRartpY5m`A{iZPX+yK@4_>DPeQF@>3;Ff0H4bmw1Igv$^iA`E<+JM1{h{gssG{(SxRA3Rb%5^~X?e}1?qUf%bZP?u7Gw?B9Lpj_v8 zzLW+$c2K^4a-GUVJMqvGtq03>#)AhSXeoKl&GUE4+pVWYOL;fsJfJZ@?%X2J!TH?6v|NwF^3G*0bAzkw zkHGn{8Tbb;4O>+fiRblitS-lMbca#<2^)z+j`Fup)ovo?`F!6AzAx&oy~+3AmHxDG zx_&;#Szg(2nzdiyZpc~T-_Y?9xAMe)qAt&RF{1F`P`*#3$Hxl1(Y8wKW!`gqDBo}PCvEe{L(U2Md#9=o^uy1wJ>#aCqyQ2l4W-->?C{hi6V=FOMkVdKn2ME}ee z8~9Fro!o%qpyZh^4&X5p?;e)(h517HnO_FIAm!5`mj&8-LeI{;*H`+PFS)?i%>Ot< zJ{Jr}d&nx?kAoGjZzjw(LJ-weG(!Ph&eCl>PJl3O>hv`IQdKx!>^S zKjeu=_pDGr?lWw_S&!RPdU2er#}44Ex9)>86GZ(9P6y8U*SE*6@1=iPe)2QUZA_8= z<+6X&{h__u&~M_-+`R&``#Y&wKg2HMGHmpQL;)4iJuIc@xeLSD1ysd_(lpNpib$VQg zpS^piu+(n>&ipC8>5V|SuebT(d;ad@k?{)w?f`u>-jgin51%VCzE@X|h?Vku{*?v! zKy$ff(!X4^bNvnIwsCBp^_S<%U+I3fTKZGpJnJvoLqNlNuc##VTa2#-c%8ew(s@s= z#y5rMxWKnxEmK75clhbAboZsNrGB3Crh_lwK=eVW-^}wa;2#d$yk6?h_0wY4U3`ul-z>;+d`rh%(|>GF+k<%LFZOS_;M?%V=PRUrAsckRiO(3m z`I59R9dhB|OS(91be{bO^2-AJy~9m5%l(V*`6}Y`sL7^pW&Z}=pFw`opoE*Uf8K|t z1Aq9@`_tt3Q$OvG>)AEnY5H>^f4#)rp;CVq+Cwt*IP5s#2$bW``_ypY)n7gkE61Pr zsTSb%#_ujD$Ipg#;?CAPK9ljYp??SXYWMGaU+&-1QMb~8f0nfBxZJ;Gp}uDUxBt9v zwp>4R(a!ohvCgIrdDhP}0&a)>Uu4wrNdIzy+hBjz)KA9B z{ecDXqkp}vZQIHE8?sUNKOD4fwSN8O{(aa)%_UXE2MrK^t4KwGmLp6 z@0TpV9iTTuu8ffT5$qry~xw-cY|-t#pINy+3x|qY0Hl@r2VGNy5Gd(D=(=k?RP@X48Dis8u9qRTW`5v zwgNBH=u^W7Srkh(y z`?(%dzVUcVp7)haTXg@4Fa79mUp}kx<9cic--U=N9i)D)$CO`Fd{CaxAKLx&N46{X zyR_d5+zD#v`D0(1A0GJS0^W9ar=xPc;d;#ehq=b@lJWES^>4qJyIJ<{CcagV!`_wQ zUF7&tzZ>I|wC&6tsox4Y;)V&X{ZhXfxE=I(`?pre@pr;MC-4g$cdgO}d&-#@`Iw4%(o} zt-ob_sGs9Aw*85QQojpw#8*8UQc>!60(XNBU)E)fjIRgr@c_4Psh=pt;NSr-u1!(oa^F|y*uBR{zgpI`{nn9OdL@!&+nUNLEeG+ z5YYCO&T_p>2c8SM{euNpWxPCySIADipTZT>F39;t{khQJBKwU%sXrWY7Et?xHE+xL zXoh|p@IwKMFU$QC*Go6%Timq6U&?$=r+(Z&EDNoXBIBC{+=RMOseP}RGM{p37x3Y= zx}KKt4cVpp?ZAD`!`nxbWPHMbhr|E)Yv<}SpHw}z0OxvC{zQj%GJZD7Lx1qHt<7Y7 zxc{`kzh*_sR+jr22jtU16YA9YTh=q~KWYEELFIcz2&-EZ`yE z=y6&8;gHR;K5+j@ePd3{J;DA|JZKN&Rj0-N5yYiER_M2b#?*Lw_0#Mz19yVHJ8Q+~ ztVdEG_fuKm3v=8b&peacOY&uYLOd8QMXf=g>c{FK@Xs{$##Md(7YJ z@w0;VZ8@e0^G@1h0&WMrccHECha#jtH}~z}Yux9{Lp*1e`dr}40$<5dHP6fQ_7L0; zd4RWhXViQ?57Fx1Gv6Pu_laOPs&4t-Lon~w{rsua&4K$8`$Q=w4L9=p$~B$dYfs^x zf8f6g4^Dwx2MWH7pRA4qNI#PeE&X4 ziOISu>2C(~-0J8!e82ajfr>-L-Hmp>k9w(l_hGuUejelj&bY5z(6tQvQsZL!PWO}F zTl;bIcw_!ZU4z2;{eP67xMt!mDQ|_m4ddF~@j)T_q{#!1*~r_ntp8m;Pcj0}pfqe^V*fuKuQNH*z0* ze z-gfX?!B=ra%1C+sY6k8AeyZEjjs+rh4a%N$wDbERf8M(FbU}e<0q6G$wrl)xp+W-B z1x|ndXqw%#FmUBhD)NEyA$xTHUn_cd+zU^pyw@PbZvj8`g@eEHu6{*}gn8L~|0w=k z&U46F!GB`xwN`vzg93^_8vJRX4)CAPIR75&EcsP@T)>&HThey*EEcJAC_EQ9<9F&x zvB|{+9Wm;R@hI=-NUz{7#l->Y@rZ(S1j)8c0V|Bi3JX;bR|A$~USH??o5UpmZ? z=XzTFoZ#=?qJ6U${Q~l|_+^1V!FDo->n1x<@$mrXeC<1bes!*!3J>3>$A{0S?i?$! zQm&U4;5`4DR6S!DCzO)60q6PMn3t>k!gWjGCXO@s&NQER%=;3hW~A~b8~b1GpVPtD zWY5{p!srO7(&ylLDEOA&T5`3Lz&&W^=Vbf5vvFW$frqcw{Wa~^>4N+lPgW6l7M`b? zf%kd&><3i^ZUb%wo-cOWl4=4Efqp*MKl#7(w`IJYkYoQP=daoz`?mvkf!4MeGph^z zxp*G#2EMCcqktL$cL4VQ-#Msghj4+112-Me{h#P+cAzG3t!6&+b6>XD#KB-wb=0>m zTcM}Jzc23pv}MstisyNH2FLXuF7>!lbvx3ar|^UGovqu$=PDkpA7d8UHJ#q8W9H_w z_^-l)ZS!?`zNgq@!r?sc?S*9NIG?|FOR4b{rkMHw`4(RzHf88&tzBIt=i-sFB&`v*7*R=6f7iC8_ zaQe}DYO7Jw51!lJ0AIQH8())tP@aAoy1cej%7^}-$0-6d8I-72E9?h11()o z%lo7xw6l(O%-PbWBsx%W;xkQB?zxBc_obB@PhVbTKwtY>58rxy(pNWBBvqW;Xy^W? z=O=GkWIlL+Gaqi0e0{&XpEv!OHy`5OtiM;rA(isr>%KW@Rw*#3dX<8F$o*2+V+G%| z@25B5eVeq$41PQKUMl&yZ~HiVoKR9i;T#?U3XC_Vx!evZH6t@!oVO+zFif+pzKDrVO1G>#d0z9_RvI0u!ahxikNB zOxrpD`hDLIK>w!%Prn-|{5M7GetDp0;^Yr+7^9W6*FN9-Vy2&UzR*gAdIU#%VYMFT zcSFt$++A4b>wac_PCoGI-1_(H@cYTFkh4Or)&7@b@*{4N--+?_fI7h6e$2+pA(7Cp3jd$|BO-d>K z{@>$l0sqNg-^%#!`9_c-+^Fl*=8*TYgJ1oj@;UV-9nY++(|2}F7{s+i;f6|jdluvx z*8VL--d|8Y7kKRVEt2K)@w76!e8?f47Jd7JbF!{;K5{<9IRdPKPx3uDvb-*5f&Bf_ zSHgk>o&@`Cz{9rwcvsFR%JX~EU!D8eu%IM87Ro=$r$c_z)@2)w0;heP&*gvoBP=lT zi9Ge^LViPZ?s_@jsXruJ_oGgHp}&kzk>~f-@1E)C6%_qMKjkfuFLGg9e>tCQXg8JB z_1|;0uF3hN{0j%}09~5Ub^+&+!n0s^I`Erk2UX24{C5D)0zP#^n;9Vj4=<E-ryYzbZ2%fJh|J=Z--%+e? zevX;KJ-|8Mu~#D+zaZ?7sG7I`M-e}7k^P&GB0lhc#Ov)dpXPr^O`Y%lf%odm@kGqk9=`^8H)_oaYGuj!yU!zBc6&CUHAbwWxeKmSiqKt2PEnRO2=A--N4PAmG^#oJn z4P-sA19ySm9rHtxBBFmc_5Al~t# zPXc8e(jk`xnlNI1&!@#97kIB$IftJXhmezc9R9qUlXFaHaQ=xh`$Z^xymo^m-*yCJM-=L!$}KdKBv{w?c#jNHDr7u*XJzAa~#^fvGp#; zLD`=Robze-JJU8w`$F8hehc_M{BguFX&>hc^^gAaa#g9{0(siEHKofT>et5UncqVj zo0vGPU;L05?dQPaw9jVt@!kL+F*LgaET}^c=%0C}Y5k=sUEWqK8g9%)J9DAV`wQJN zuX2Ffu#U}I`%WFX?=qay{Z0pdt^4bjf<=CZ0jFON&sX^*pTHx5J5Z-)e>v3myOk>L zHuN72zJ8Z7uFANE15W||(D3=^a@-krj?2oQN;8Y@{^Ti*H?F?8 z8-CT}Q>p*MxnsA~_>plpqn&Xd(Ct;LjJp*$} zZoMkw?gCD~&p$qBl>0$9aPBvqMMDS6{a_B_<^kWVjNwz|xTFC${ige$^v=V{a{Wlh zJTU{G)@Vc5P>~lLH{X1Ix9oDMpLLh(d;k9bhRXHX3B9a0SC4vn$a=%N>jK}UmUTMH zyr6!r?@2TNjF9WQ$4`IRlP4NTc{gy=@4Ek<`87%~uT);!ft!KfY!I6+^EUDoU5@^B zoY&)h>7Si?vH$qw(*vcYeNN!?|6=)`pG*6!z+IqgqY6jK@v*`_H}C~pwwx*^#>b3$ z>;WF1yDy%<6Q=z0VBI&J*8OPz_~rL`KcH~ut9m>0GpqQmDY710A;U75Ff8Uk$!;Sv!h(o^J|J0QGZx?VY*p#^V1GI_DpY6p8Q8UNEemmr8-@0o3L!|!D273QCtPf3hZ(Ahy zPcA?CTHoynmig%>j(zE*9~yO#^VbR71G@Y2nmy8fE80yLbUR+G+bL4UpZUr9F#k-= zrujvEWqs!Tg0tGeYSMpKOIcY$tgw5YeV-;H*T z&p#JGw@CZ7ubuJ!E+XsK%_9k|W&JW;)N$JXt)qIZwBHPz>q}^>hGX*B2b}ibnOOEm zX`h|)*k?XI7Q9;8=V-0>Px*HmWi^-m^Yi2`=$Z9S(p1^M8|@)&bUj-RC!CV~JAr#Z z-;3I?OU@q;;%B;~%a`msv)$A7w~X(Gs7|e=evZEj`>>HO49l}WwL>rcv)=A;McQvA z4*J4(KLpA6Sl>c?u>O|q+Npu8Uv9{;ep$Nq93< z*JOOmz|Fu5^$)L+XMc(KS%J5kT0L6sFWsm=cHnadP7Rm)OV$t8x56v_Pi0>M-((T= zo!)6V8p;*!aECh_N;nM^Fr1b#KP0q=CS$j;ZdZp<$M z;0dR$_2BDUH}byrqSSNs^i9rPBI_#*Yzny}hrW<bscBZWqI0G5QmSaFXEEdseDt}4|0H`a3gv{pfe?NF+IwJ()I5ks zX@8geq>sPesdvJxl0w*H1WxwUocr`z(pTUX;B=nysQ&vE{Qjc=?K?o%v-uMZE3Hq_ ze{SGUUA`9J@m&PG2zciFw7q#cr-&5pas{ zx7X~cwEpq|C;jXFu{)LP7XYrs`sDA^ww_!+?Gbh-vPV`W$O)#R&)Jm|Bdq7yMG@! z%=23Se3ajw|6t#6e*dN|llD{oieGg68rRPUek14xeYUU#x8DNX0{nXIM&0@P$cOlG z03X%=_94DLaw9*wfrm9|8qL>7M&L!j$9BwnkWFfYf0Be$ODuw1byiF9wX>mx?2C$IEg4_DdpbkUm2+tVAhG zp%3L52lz@rf2MJl!|J=x2QXeNpjX|H_SVjiYad%Rk5xH$XaN0z`k9Z$nX2j&nwPAg zPdw8+uUgeS7NZ|8+o%4{2mPJL?=PvYt190=t}?wB^t+nxs8yqC9;dkyl{pWqu!V!HUtSptGOIt{us6dfy3+8~wqa z&BC0j;3e#$_VocN|Ap6Y+~niRjCyK+&(4<1BJwNv)xd2idu6nk5ap@B>HUhN-+Z0- zC$3*X2>+Z%m#pLbv>#Rsx-L)dh>2$M>Gx16j*1%j7Kh2^gZ@?Dly=eg;BWlWCMlfZ zdf?>$&r%mY$^B~vu1EW$8!UBl{mFmyyuoxjem_6Y?Fx~9a&qh#k}uW^^gdJ4zX0?@ z+c-Rt@H5m6+G7J=jPjv7V@5@JB!%eD{0`Dyl6U4z*J|7!+J7WY_PjiI`}e%Rjljtt zEvEIUPx=b^7T`25`Rkv!!~GF}UJlT`+~re0@2^t$(G9%&%UyQGF#TP?i-5n_%(qp| zaEf;u=nA)6>X4s=eiZLCPN!e1;o|qBX7FimNk8l#xM?DvCjw~K2z*(WKaNGQc&B)# z_WKO(d6Kv903Y$cZnGqEeu`%|=!PA$kBesV_3$5!H-Ed5CVag4z^6r-wEKpMw@>yH ze`HC!-C;~V#jEyTY5##Ox+&odH=>^6dHM6+5^Dc$@oEA6%oM#V(y6L+iT(&cPY39> zJ!0C+{h@`w$)5A?FYC?kw~N6?_FQosevkAK@=Jl!^YV?R9#gnK3V^F`OMCloZ=mP? zE`ok~;1{Y*7#PF+VF7Li?m19xw3^`*k4Df9Z1PuA@`KQ?+~2^j|8k@Ox32(l$^MJK zpW78-mu?jNF5tx|hpoui6y>bIDITf)tsP(7%-dK0C+#NwCr&MVjPp}G>Oq&V^s{H8 znS9Ex^gB21n2(q7{AmLp<=3?by4H@6>ZyYI1E=|?qx(uU*RKFLjn~(@O>kDyZ-vyK z;&I2J-HtGgY=HZ>6mn)Zeeq+Sf7N#+zaHcM)t}CFr}56?ne5Ype&avq>P4a-U{27U zVzL)>yLJpr=KgY^p7b5+pSv{1S)s2P{BF>F{Mh6RYKE7hpNoM1TzAK3u?(m8wNid} zoqw}lm=qt>F91G@C*Pw5i9FtXgsWnM&&m4Md9_O%lW#-&M&Os$tHxJj@$SQTwE%B; zarMX5JyHSDA9Ua40N$l`tsyml3xDgT%Kpg5dc_U8IUS$Lsfl)^H2MA5&~6gUAk^5>{iLyd|=(^hs`iFZgdL-d4 z^r7o+2k8Gg|8{BZq^j~m_X7$*pKtr|L>*IA`p|W^5A=UGHm2Y0``MxEZgse{_p+;Z zySsfqJ9OP`1by$VUyZ4+sj5%t{(%kj&u^VJE%f`@V*em?-7O>rzn@3(0sdl?0vG!S ze)d_!of-G_^gZrC->cQ>o>t(dIWq3(zP{GM)w9Fke}Nk!q#tNq^U&$E!{H210#5VH z{FL3xA{cH5PVs+r)Cxb}H^>K0dEw_ret0;F@oRt=qFn#;rfJa(FG0O&th8h3x7Lkx z-=@TImHV|a&^tbz`^^94eoYf8?SEnHzlZL2zvdb)+ck`kr3v&`pX>6@-R{>y_nqvZ zFR9ae(+e-_-g1Zue{6ko&a~(98I#cux=cv#)pD_vBA8?nB3!E=t-TrF!PM z7?Y4vaS8g+ab^O2zpp>7rZ!a2ihl|EP=DEp-a9EVR#%li)L$OZKQrFgB2H74K6IRw zfW9E@_wBUbOI%`{h5AciVw|bKr;3*L8&C>dj59O)tjsg_-lxmWOSKComg?=OCTf|ak+z2KwqIx+Ca8+;z~lU}&rUUVsb0be(%Vk(d4 z#Yux2(0ne&yAC*w=QZsI7DT}Sf!mNz=zFBUZn^e%1o~OvR`AohX2s-TrIAiyUC{n0 z+J7Va&L`}&bNxtu>2W!pW`AUUBf=D97yeV`QK>(zdz&@zz7m;Vfzvvl{8RK+PIsQq zXx*t&OF52&mmdyKs^Hh5p7j6c!`Mt(7m0qR+({*^>1-f~8U#Yx;OY#*!UNOo^4V$!z@&;jr>wnU( zeA}^-eyUjMhcjz?sQ0%x`Z%>i`-0?$1M#t)$qzz5dUwT|z2iSumB{vmUGyGW8{}S} zJ8W7w!=0$7{=YN%y*&{OHv{*e+_f>ReI#(vF1=%9V50YNmA|50n#cU$TeINtPs11< zKt1Wz=1SDR;SATtNk7p2{qFmQT!~<~5je%&)IR!2kqoy0Cx1(XR@ zEc~m&CFos1n;_$9Q&t{)ykL z<7nMXTtYsrM?Ih~0R4bAs^c~CiLyc;T3R;L)Wjx zpx?E7`_|fqs`R1j*8u28>@s(&qpM0EIuGk>NdKJp{iOiC2ZOkTy`l541@w=s>|m_= zK8y&JFGA))C5Hts7wE+Ykyrf55~sNBKRy1RSbvZ-h||15D2Ab&jfp9?tYxBJ^y2J!gP11~_ie|hKiyniXaih(!U*`+VM}A!+&Prd;46PT%F;x|48xo$i;nA zxO^A*h<{p}4R<&{?LQWP?xT^1UZ}z3)9>Ng5Z`aqtaYBpM=AKozWYp*wp05`elCB$ zLi+**i)4QTiC8hHXbQn-H`uC#K|2|45xS{ z{vW@KdVup6fzO9>_4=9Hq8Yyf^#PQ}8f?45ZO*TF z`}BKkrSSizzR!Qk<5ycx+UEv;)P++kxqe3A)K4!a&2GT;qu*nr@wWBD(@ki+iSgqA zKlNXoqz^ym?Yn_foctXz-~?}<-kWPi-kCY5-)M?|G0(SD$?MUm(%)3Nu;7Q_JVN*D zke~ABg_v;Qg0D6B=CAm@Ood<67JQoe(jNwtcJIaT2!@yI1N{4p8?7UO3%MO2xA^iW zcU0D@`nbUN{*K$N!+{IFPT)(LUUQAgUcu)9y%**22j(4!U^uB@q-wKTY%F(=VNPkPEa%40o;ZDn5bzr zEEc%P$D!|Ib%TCFQrYS__y?|03Hs3Yu@-^;!neIO)sm#&IDP2*SW7|w_FuPOs&1-E zPw!*3!Ef3I(mxL!KkBbxs7x>7#SEPMyQ0Rr`87cojDO(dzw@u{QpGde4V?TpXl~O? z4a19olmB|f7JXj}_}%>H1HDi4!f zTYd@o-!!5v#z*P^v^lBr92ata)z&pOatWINw zQ+}g)%>3ZIO8LzVK59R(YE66Iz5{p>%H{_r#Wi8_9hCoppDy^x(v;y^-~r&def>k5 z0atqO-sk=*j#;Xdek$MBGd7lf+8R+Sb8oH2!B?q^ex!4jv`%TfEyv8)-E`mK1ph08 zcG@C5G7>mH<)N@4PfZNZufRRv^P)Vn>34r5=btCnVSeCUe%YB4#c*n$*7XsYm+SC# zn68Pmi{v{KtJmb~FcokU%AMUe{m9pyw2q+mKfb(p6K~%c!hdl6eac~CRqzt_(>lTf zy57dY%lLf>J$I+y@BV8>heJyLmGk?-N6+1RPiwJ`KbKcEmG(K|pD$V;Y{mVr15W;V z>xtb>Xr2}Nd62(}f9$)TdWm0*dpfs7`dJ~b`U{IzN1`90u85~76X}DpqsI0EU$+*b zp7u*$dw9u*++SYUTLQY@yPS&V_eoaZWx#7pDf)%4OK9C{0$uVOqos->LWm60U+g~o|NC+&Np%Za7o3^${m=A)NZ zT~3Suez!QVfqsv9NNuv8$AO0AQF}4Na=9OhP*2Y_PL|z@dbhx2)yP#h$IZs@Pm5=l?t4~hdC7lZFysdRs4Y%cv|LAl*O`4z4|#R18GE#bkn zT)sPmKjpz86FEP{K@sT2zIg0CZa>8V_4B{KEd7q}?*+g|`nT!kT*2GdwvhU};2-0R zU88vWM#3@vo3z@{ins40{Xy69daswc{~f>`z`rkgq0)X8onN86(P~)KUY^&Az(@MO zIKO)i&)aU`K9v9Yk3Go8xfbmQfP0@aY5Dz!2K}yWDg6*NXGQt^tmtv?=bJg%+4My; zB~HrcM+@Yr&-LFs_KgY4MXU$&9nLM$eSYIY^Y*YpIT8d;&*wbgKXE}fGo0b{e2?bW zp(`G3&iB2%;PazA6xKLCg7H(Ft6E7rcfR&}zet8t`xHkzcN|&G_XSPhBl&%I9nIr$ zrUPz88QZc;27eAjOBj&J^84o`R#PH^>J>GA9fak?vLN z++GvvX3-uPfZ)?F9XUa{(iG9*Pr^6Rb2_ox8pr~b?b-M}9= z{KoC4{-k*8H(_dTT5kyZO29|@zfx=GsK}BE|4=+r-e|UU@?M@dG;O7QG>@fiY`lr) z_q+AC0rVM{2K-BQ%GTugE`vTvplkM&{}{K|iF%sHVh0r7;r14S-vc`L_>+fX{LCKU zUf?BPhMm7#e;Yv8tni!nNl)P~>Tinw^nd;y%lliUm;TV9{QP9+0bGCTZ<2p(!20W4 zzBPpZ4^Ltd=coR5f^ONdPtI`rslTZ|XHA&iF@p7{7ks4u*t+@CdHa6gzY=nm(6~I%wS@{9~UW?;mvSq#w?{G&v`dt$XOX2E|j#&bsr%$}0ND3OKtm6J@iUcRf)Ir+6j%$LyQcGMw8FKC-{Zr(X}}{pTSZWrK0sJ47@2bnb%m zuRF4XkK$eEr)!V#j&(qd$NoOa?I-`3K-Xw!*~eUeAI^1<{ER<-X~+HJ43TfG)%Ohd zj}^EFWu5mvv2gvpsP|Qu{gl?Jd)pXhpLMdVC;vBClYAkJ;i?YOKGN^-?IyQ*`#Rus zzGP|Mz-Bx?Ou)T$Wjj0Sy?BWG#|oVKr^cI;Zgc+x9+rGg&^;NQ_+};h9+5clpM7fc zU%Y?4;G_7+JeiZgPj`wzGY z_}r8xw_+Ktvq}A}z#lo2cQ%gUPSpDmpIH}I_o&A4Pb9w%_?h*iw{!oN-PbB7*6}STHs&*7&bqW;nXhezv{Za z*f88K<%@Q^pxtX(iwacEigqoK=Rmo#OYx})hSR=nKJf24_Ip2);f1KDeMQIGTIo>? zF9A;L!I@3gbdF|t8F1QnJpBE+>oE-1be8_0eaA14ZCj~kxB)oLkISm3HjM=?=Eu-| z+a%C``Oj`!9Q*^hD4(yb*|jylpR$85A7$?5!QGlMem~ZEg}@6| z3~Q}pcp29HCBWzShWeTVSG;)dech~7N|nOT<@c?cZqg6muYcx`RZZ-lQa{jnNSYU4 z?N-`3!Yfc!u%9g8qx;&{4YKz|dV_Efr|-!U|D|uHkKp|75dOa&8@&5&{50=%+hsn- z*M)TMGJt*h;$tV~hwBs%D3^$%0OV8q>#lm6M=;z6T-#mRKkm%xfsqWS`zRyu-_65g zn0yz$Uqt>}aV^Ti?~}AWq}}A7BaYrjqu9EW`j7IM=b&MBgr=f@$^Z1c^wDN@meIT{ z{O^E#YQO*CH_Q0*R10u7$~(X3d_d1rMINJlW%@o=5$K+r-tv3$lhj5P>~AA*AIkN$ z{%gklrM^$vOZM1W)sEu+3c!zg&v_pDQ>P|p zWRxqT{6pyD50mRJ&Hd6p$3`yFeO>pYNzf^HqzUzk?BKOJyvBI^Q{Yin;H1yal%W}6 zUP%$O2RMz>*~W~&_&BBKN5t>wcINSL#&5&^qZe{&HvM@u&m;a2`PCanPUQZgajfbo z?Ys8VX*c;x%sb6tOwG%$#j7ws3caaa6Zjf6yzLBUxCQlO*X`^FHt_tS1MVQY!EgP+ zvx56gYn1*V`x5JR z(nm7;=(!J#?@y0Dl1}57k5AgawLsoZ=Y3}KKU^D(6C-d3%4^NPn#b)eKs}u&f1yS3 zTio6N>?{V|x(h1@1u{=|Q*0xAK>2 zz?Im)sXQzRUQ{9#sWo=i52QjuFe-ffUOul=$qi3^{9OW=x( za$I~?zMrG=fX<5&^$$Px zir(h;=T`93ywd*lnVs1EdAWa_pwldfTR`{cd>qj{=K5ft z&3EQ<@{CiGpj+qQ5C5!#Qau<(v0{m1bteUwgajw<1%y{*g#)G z@;i5aqXx#W(2Mq8)%~R17u%d1R};AC2l_s85!Quz&~io2{2tlFXk%g$I7U!jG-44+L zk17F9{=NS8g6;fVei?9@Pxmd`IiBw)YWhq2>HfA};cYMP9|LfTpRuj4zQx9SR1$Ey z|K0XM*IXL!qW_HWp97^C`q;sDa9`q=8pWSvpRi5vIr02Th36Axbe{yiiDwUd*Fxb6 z<+C=H_V`g6A*UF8PfXhPYs<1=pOG7be$;|q^?>B>l%J8(N}&^%@Ux|ktTzJR*W`w$ zHE?ekKeYPaycx;#&*O;S(V2Yo!|&(@L5-csnL2i;dGPyfxIm(o5j z$@h(EQyj+hw}r^h`6XddIFoM%?m}5#GjKaU?`gvK#b_V*l>5`SskeoHibLc-yGEm& zbCJ;?@KWFu_XkwAT)vO19w671$=bV&t~7or(X z=VWcb$Bc8Ij$wHDIWXXtN0dzA{4UfNpnP@AN7wm2tYwB=rxyeN_?52L_&%%?`y#YY zzHma;F22vI%BZ|g>vH8k!uM(Q1Eqgx-=$8^!+SZu892#LTf5s^o!J+FeA>s||K{0U z+`lgH)4q{+@<S>&Vu4~cqV+qJJL1B6Yx8=2MwOKx*d`t3vzmS$11zgeU-seANOhlAMv7Dq576(r&q4e(2TJ_w|kqgUik{=)gmJRfKul=hR~A3ierJw9HH zz{$R{Ifr)h@nQi^`7%TQp^=XlM+pDIhOq&jPu#%CKeP&Ri15?e_sU z!p`|$PrAbMQ2@9e<96tTr(fdZmCgmwdf=P?y2kM5!scz#zecn4Q|%Kc(rCRP#$(B| z5-0yzKsU$ynTPIgcsyx=J5cT#{XzoI4>TT0-jh#n`IYx4t#4?3F!PT=OZog>3c0kO z@y+QCqxpUYjWhL7Y0pP>?>iQSb-joeTHlcTOSQBe`TD~QK9cW^|MmmEAEXCvLwV}l zp0a2r--UXzuU4Y^{TPPRb8M1-{0r^pVGJ(@Kk0X8*7~Eo{ZeW_R@&F2&457>j9)!W z*3)zB2PS(XxqtM)DIP{!+eC8z&~t1v=w4Z8-^lIr;yE<&&w0LEa~@AF@X`9w)M~qc^c=eYbWc{-s3;!`+=lvMl=X{}HQav%u)h>|$vf}WQ#1Q%{i7Z({jg?L%h|CE zw_qGm|6H6id3_`TShQ~jAIW#EU7g6~>w())y1sp*PaKo)3gPcpyd$L=!zo{>VMlXw zWH;{rV(^oG>pqOH#{FL!f{#vH|19^9dW5u_^w%7XYgN$ z&L3Wb$)|iq_PxBg)vq+q-YuW$M@oOac3;E2H1F|zrUq_C`SPWQrq^Wc(Ril);h0&^ zJsGBx8BN5K8+m_ z^;PjPOn>UHBH(SBzWuWrIPb4w^F9-Y)0A1{*mEY37j_^kT#*h9X z>5oRO-)JTFDa57xz2|e4^t7pIl~-RXl_IZv{bhr^DUR-Su1(l=zmTWkk#5u*@O)#Y zbKOyaiA(5H1f144C;Hz$uILfG1nvV)<7xGlgI`lT3p@av;{8IJ`VPghz_m%0^TD-$ z-+zzi12f47o#w-ZHEY2ick{mmbR8C~&rA>=W0z>JfaZVDEl5r)s|~uKJ;=WWz(>#8 zGK;=v#_gf?*terwjOXjkQt;7w>ejZ!pY!!*F>v*0X}8ugZv>rh5b`}(@9KfSy1UjZ z{9J<>^>qKzFFa>IKi5F}7c`#Fob`3$^S2B9G@fQP>$rr^-vz*FU$2|z>l8kJ7XzpL zjk=DH-{SLkDRA1~c>J>q=Xw65{R{ONY5!l>lvjGOd`0^gdf@HCuG;zhLHifPU$D>m zD(5$Y&xZ2m!p)zucq-oqcL5*h%4tC3RQR8sLlgi%x8I}T^9z0dg#5d?em_0;551qF z6#SpPfAKQ6pU!cT|C@aO>??eIrync*Lh>V;d;aD9qXuq9dFTG*TikwnKLz#Al?-ny z{v6Z=KI)(Qs{OOH(sNGW1yt5n?d1Na_fwF5+Zuo0m&aEr_$Yp!>i^hBmGmDc?IZoN z_IO5e|LK8~e!9+{>*qh#G7GEFGb0~_xm}`Ik z%=I&akNDr~Jz^i{r{_>M(4BkhPyt^L(EBUY(4$Y+b|xM_1>ht5M|4`*g4thgAHBC? z-uU~J_>f6fEDIVW{e`Owzw<6#akG}7Y*XQHe2;7Hq#{(@2 zSv*9!U|#_E?Wban^7&p5Tsu+PKfKy+f6{!<^N|{Kmc+1yyuT^l&4{rkbm?Z656a`g2mFOo5q0@^w4gqK@?u!8S9m;9 zypw&a-Wl13+h?>$zYzb0;@t~5KgGKRblQvCALag~_g@siKi=xGgLwbA!RLm41-@x@ z_;@V>UJU;B`?g%<`uTttfxo%`$S$rQz5l`m{!`8V@$mT8PLlRHz<>K`Z8F!-Nce2I z&v7X2>l0i*djEwD@;@J!HHwYbCz?by&_Tufkfm0lf9$W1uZ=cR5(|opc#gSQj zeAuvVr1Q<`56*i%+$7gs;#^BR4E6=CZqrpsvR=e>0PSiYmiBMa``(IRIJIj4{>93j z)gyr`Qf|gTE|t;vtgM5xQfJ5yN;~E2UpwSX>5%^C< z^7A)zj(YMi@8oc&qJeS=`?`X7lIcj1Dqq$MJ|E-;P>wIU-XMbEMX1+ImiGVguda0@ z!wsmXb0Uq?k|stmJPA1ErQWe=s%VDWfot)7g@Nsd-XFv8eBg8+yZny(Q#Hd2fzv+y z{h3E%V}Xl2AA0_}1oR7L*617u|G+hOJ%3#W`i`?M9H?fOe&h6^=ZAHVNIyOBoT^uK zYgKwWKb!==CV~Fa+p*u*NUBUP`o{^J{98O|c$b=>6L=wT@?YtwE&bvdUILu_*Xf&~ zr!@>O15WP8hTEOq-Kh2}kzNI_IDDN4ptgoOCJ%4Qg{ipsjU(_~Kr4RL=74)sX zUh`EQT~&JWpAX|QAM|mWS;~6`E7J@Ac!8U-9$R1^(zhPy1YQQ5)&b7?>HpSexMqs9 zm)4nyZSvpNGTZ>1@|Iyn`ZEm}UIaapK~^4A%lT z0AGA{_Xo{@E4^{=bDs2Ln#y2O`k^BKK~DT9KbT@>Ts$Sln&_uMH94=)`f6H9(M7&K zqH~dyXNLB?e+K_va1rGCP+o7Eyo%2cWz(em0Pqid+4u4FMM+BK_Gd0MKFZg3MyvD> z$yXmcUC8y*0=J;t@oK&Oe0@Xv`P9CnL)~Xt`;no)7x(g;n-^0a68f#L zeE-Y`ocy;X@Vb`op9O%^`m^4z*5Q2rOq(q2qxEO(zs9C~|I7%S&LcM4KXG{!#;?%N z0-W;HvMYc7%=gb6z$p)%t(X2d?Qe;^Lcc%ghMsQF9|@n@m)3FI9}dtJf$qD_eb&=@ zL&Rkih^eH#Yg=+k3X@YFm+EQK{w+K9pXhi_?G`k`F4~u*bEBAq^y^@gMFYCrh*>`Qu$+i$`CCh5Qb>Jii3 z_GLBGrJXHzUtYkUdzL}20k|_f@=LCNA@C&NCm%X@Dvs$-_Z4Jc>dT+$E7=D=;{WT$ zgy%Rv-B%QXE-kK}gU;a!|Izn_see1XZu*q>ZyET=f8D=WxRTpX`|@@ae8^$5mqM?LL}kDU8(!$^kb1E=w^WaVo;q8MHX zobtx;jPIS%3@?v=&@CE!>b)3-Q~VQu*pw7k1ojDp|1@b*fAU|czW(96#kT=;KaI5Z ztrXvAHwk!?^#^=vv@h}+?L*M}66~NmdE~3NDGualk@-dgdHJBb*4gc2dM?&`tk&aevY?IGz#jZj7sA zhQ`PFcrZb(73HpJJNIz?X*`hpXUdBAa`~PR{@P0?bm06n9=xE7>er(wx1YuXjrRvL zm+s-`{8ct-H^t*5(^H4|b61Ktnn#Omw~OxVU#Cz$^?>e%tK>blPKdIi-ixwh(w(9IQ@r^>_r=*aR*;{0yy<|e(xqP;Qgehh_^!U6(Qcf z9=3Nj*N@_f_}^<(8prv|Lij(LtzE$RDV{WsN&64%+3n``8A9^URLziM;Vi!-fsf+p z-LJ>%D&;@ml;0M%UGzew{0E%k<=lIXkMaCR`K=Ii&y7lM&g0RE{-gZ9q2_n3?iNpF z;J>qRWTkT+C8*cTl=k=Qci|<9XP&?4do2dgeOw$DM&q8x6Me5G33QVqUigFehZFU* zj*J>w_a)vR2I%7f-NA!j26#M`pg+AN=am7ycs%)0Pxr&$ynEwmI@d1ZDIff*3~8@< zV$7@YEI;ZHhdSW>Y=!S=fQxly9T-a`okPPp_r&b1+$sm%m3G7Edu3M0Ju>=O^sS$= zlaQAq-KdwDTBTYMvx6Q_s)XJ}z-gX-tnbdZ_&n_cPI2gX=*!wXP6NPcotpMrmna^m z+Dz#Wn&$^3{IQD1sS!BcfAy)hq9%`13*oqrs&#nP86Kw&;M6bPH8uB9oC*8f!0C6H z&&^ylhVoj_e&CchCpqh<#bO+a^YR9)6KS1gg1tWQ{Wu`=NG+uw$-lzyg3pcnLAoz1 z#r;G8e74ulw@lDf<`eoPfzOa7{dT?dvE4d_4*eNr#6GGG`29P|3Y!BDp6?$l`RMtq z4bLlGpkH2p_JJ0Pwp?E^9_iet5&Q+9PpG^0k~r7TFQKOvbbio%@!+EFtw1N_(YgKN z2c$llY+3$(=Iq0*{al(V7>5O*Gk{KWvHd_j=z{qoR`PpMT0vK@2XQUAH_t%;c*`cs1edzCu_(6YG-RYH%o~rbrzcZq-OZ_rF z9+uoGzbbv`?~Is0e{j|4MxC8i=|g{K#18tx75>~V_Nw%uzcbv5-dXtZeVVHDp}#ZY1^r*I_IWONxP-BY-}?&voe=?x-}@@6A?+>$ zzb;397P$DmFC+Ub#uc5vqr*kVU?>yv-uIlF)$_oXMSB&y%eEWVekSnF*ci8cL9h%nzpkMp- zV-KpU`nk&Qx#)AHe?IE0yvdscqZI!1hx`tm1@wX>n9nuRK4%MAj!Re+OM5i}x9Vhl z0r+~Y*fW5htpxL0yu^!v@4YcQkDkErp2u>;ztlek}n0#-%^Mr0*IB z`BCpj{8-P{*V1hku@;3NH;&Hk|m zZ@;|j)`INUEp`MllacGF*m9)ya0GiWdnX^dB(3= z;9}huI={IZwzU0KMDGhZ*DN8{gx{mOH{`{%0b~U0z!{mpq zBh>Sxe_qNO)}wJ{@#4J%VWIPzAQAJP3wg^3ej7@Gi*&^5@B7y6 zH;1!qrT~bLGCaYA1OrD5)5Av z<2k9bloR211x{vD1aoqxGzcWG7)p>ZtR<554 zxC!M42{&4E{V4BQfv-Jxq$&50OE2Zpx@W{&@elC!J>Vn%{<64hU*3LUYsv2gU9BeL zd-C@EsMo>%)|@b;a+RZmDe=MB{xc>m~7PkHyp={wr-bp_>J^54f3TeRo;TfuKa zJIjxExS#81>|fdc{pN4)%K1IuC;4TEf3DB%F9kpK|6j)o{k;GE;3xdt=bQ7neD?#g zeZn{7uF-RT-9qUX!Vmn=OnHB$yn^uuoYwuzKmTl9H1dhSRluz%8+=rjOy?2>?uC9% z;Qr{(YS4OH;7;Hk;9s?D@MkQOZvyTGetkrT{Avuh4VLy<;s2)x2ma;#uUaJSQ$bGq zTPHg4{-<@F4s@;V#NXomUm7BR=Z9^Fa``6kSy5`geXcoQclx2X6ZpawmS2^xHU+Ps ze-O7G;8Q<5daMS+oxr`opKRAQzb3;?!2Q5qbDg%=0WRi+(0r?MN`F*;>XdXAn)qHpM+B2BG22{XNC6$`GCqK{BC%`I4Qq$iY&D_UuQikKYOpr zQWYWfv_;F(g8MZO^l*i=C-ext6g_Uz8lFm8^G{Dr$rzKIH6wMfgI?#Z*cl$Cswvyo zEtc&@=l*c9U6vy_rHJ?Qj71}g?D9+0ufnHA<+Uo6UKOdbLk`iq@R`#I{>k8@HNW`C z>+cJZTMRiw@5g6OC-^<651=Huv@f7rBJHI5mS~6crFweb=|te75cVa3pXhD)%;|(4 z?Z8K4PkiL{^gG9*UdSzg9HRH)Gp7^$PSpEQl3YE0Usd&FW&7R~1j&zw&14+mds#?R|}v3eob2029U#Ai+? z_)VyHqZDF9y)PX3Af&!K+97?3J`wfxQHnz7Q3igZS3f1~<#eJw8aLD*f}htDPIAqV zL-baB=5&Hzhk6G}l52#0o{;)=fK)h*bFz9x#~ZY^q0)$Pt3@0KQ2Nks zMX<-sJ$NM4$F8aX)J}XMngW9FCeBRAY8Jm}ro;9OF4VBP?=3O`B{80F> z{pTSsJVWy8Ljfx5;B))-Nja%$>5fj>Inz^xT%A5MJ1aXcJ1bpzC*RzTx|Hm!ywt3` zcJ15u)}^QE@@%O(dwP~GdHS5>td!JTU0P0drY<=v&X%2(nwzJyr6y0;WvA(^gRHu| zYz5F&0oq!1(`M%dDbjOwqaGS3g$C7#3$iK{N|~OQt5beWZAPB0qoByrS(Szrv&H+t z6oT1#_Sp(WvTjCd*6j4GR7KN_jP%^}?5xgl`oRwQQbAo>c21`5>@zEMS=m{g<|L=g z&YqpyM-ivAto#?WCfS~v(>7O^l#^}Ob=7xm*SVcecun>X&GV%p{j*n+sHohH&*P+j zI_2hN=cMYC!-J{zJe@r!b$WV=GJ16S18?5fxktO+x?Clmbh+vCQiIBgAH~sS&Q|=F znVgqm>l2rosl016HAjM}k14M~)9G^*`=%wQ%xu?3myw(^18B17q1^ObrIS+TDlKIz zo(uMgVq2Wzu&mVSvQvWM=O}%gHn+2GWO`0cc22G?H_sN-w6k5QgbBg8r1{_YoQ!LM zDIs(7Ll9B<0X`?C=42*kDS=Y%XeD}dkEiD;QK1A$c8-V|C5ebwqX*u-b=gWFQG~>a z9#RNrDoUl=b^1ZNp<`KOv-rwB2NZ@=tU)5b;)rR-LD&;s|2R#TjAwSK`*CI zS9B994bt_~4Qi|WnLN4YqmNb?t=J*PBdrSz%PQNQ20N*wyi~cr%XO&Gv$yVXTXsfj zr@WlhRNeH{+!W!Xoe? z%iA9!x-@%QZfcG)e<-6-j=4z%kiqD(ZMo04r$rNkioK=ZTtg-ZQUWq#IS{AdwR z8u+acr2+iL7c1ll`NhaLNvvLsKUz;viCb0WJ*ruX`AS9<=CQd!bOWCs3L)>+2i^ZY z^iB8X0$1c#nWreu1TOR`1)q9(g`Ps6C_$iHRMOta_`LKCiOBY8-Zp{1W1WrtJxy!B zBxr;jns2G3c`s2(dP?>i;7HHT%!NQP9I~NA) zA37Y|f>-=>gW9Lk4gC$EFD%A=5OZf+$?>xGgdQ&3=QtR@s4t(VLh9)`Lnu9cUnI2Ni~9_&U(kNE8(L5KKeV3mVQ4+= zhw*lWA8B8UN-gZLqV%9FLRo^c6s2mF^rsf30i_wG6{T>puqO%q?qKzb9{0T8NmP<) zy0QY3y(IsNc%wX~S}of*U;m}?_Ow&M<9$LNjYleJT#n41o-~s$+7*#Po&j=_P!2!V zsOkB)HeL`dDtNdP^@{A^b-(t}>~SMz3=tm$zXv$wv8gj=@3DVdCrjW8&pq|YyoWws z$n&Gz`Ap3>PgJ`(7V@gh6Qq~Gg`YKRq+bju!FSJn#NaANagJEB30iRpyXbz#208Q2 z93AInN;TTb!(;l)h{}KDxE&Phma-Yn^8})MOldt`=(u*eo;K7XT5g>F8G{x z;rpNT8mHVGrKd<&a`{D&bIJYV{qIcpzB9@9-$Opl!&K6IO#W47zMNzsM7el7+I7uBu8X>>n|5N^; zL%#=VZM%5zVIfoaq3|B<&^$^d z`FmipvRZ&b+>TPnskve4p;eRSwk7$R_0kVu2^NYSH)wx?N;TrjhSEcE2LDpM4WElq z5}gh0m!PD218ZO88#l(Snbixwk{_w0JTW~rEp^s_ygZ)Rh24~Ie2}v+)i?OxX`6%j zLD;AKPqqe2nm5G?!4$ z9ln1|a!o|{(%tPfS^od*EyMFZ(#Hz9)E@bVKI`y1$^Tb-&9y4WLq6nt@1cJH=Rf~9 z`J|5v`q1allJuu|vCplnkM3pZ$0U?QPjY`^k$j9BJF6FYgzTV_@>;I4^ErBU>Zt52Qbf)Z zlt&66CvjY#KW80k-$hVSE>fw=9uS{JyL7)3VC{-}y3Yuy57WIW?V@%dCrpicBTAA_ z_YI+PZ2yZKCzB)e{^>_?-7eRg?mG$@ouYS`_bzgI{-J#310BT`l|pYpPw`Iq&<*;s z5I(Y#^a-^y$y3!|Tpt?0HqenCREFw9`5{z)C-{k;;)U{I67<%Au8`5+Ek6AW55@`N zL$j%JTvI$!8NhQTC-$-2*gw)^f20)mVM&<3y_k2+i2r=FV_@wVmELgS`H2qaEZk11 OhZ@hb%#2?6;Qs-d`WWm0 literal 0 HcmV?d00001 diff --git a/verification/check.sh b/verification/check.sh index 06f318e..0563d19 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 Refactor Theorem3 ) +PROOFS=( Basic Completeness Extract Descent Consistency Binding3 Refactor Theorem3 PinStore ) # Certificates and their exact expected cones (observed at first green # compile, 2026-07-10; any drift in EITHER direction is a failure). @@ -51,6 +51,10 @@ declare -A CONES=( [LTLAcc.extractCons]="propext, LTLAcc.sha256, Quot.sound" [LTLAcc.extractCons_correct]="propext, Classical.choice, LTLAcc.sha256, Quot.sound" [LTLAcc.extractCons_nonvacuous]="propext, LTLAcc.sha256, Quot.sound" + [LTLAcc.pinAccept_monotone]="propext, LTLAcc.sha256, Quot.sound" + [LTLAcc.pin_prefix_correct]="propext, Classical.choice, LTLAcc.sha256, Quot.sound" + [LTLAcc.fork_distinct]="propext, LTLAcc.sha256, Quot.sound" + [LTLAcc.pin_prefix_nonvacuous]="propext, LTLAcc.sha256, Quot.sound" ) free -m | awk '/Mem:/{if($7<2048){print "FATAL: <2GB RAM available — refusing to compile"; exit 1}}'