From f1cd70173074e02a1cdca5c0cdafc468737b7d0e Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sun, 16 Aug 2026 20:04:20 +0200 Subject: [PATCH] =?UTF-8?q?ch01:=20unified=20leaf-index=20numbering=20?= =?UTF-8?q?=E2=80=94=20Leaf=2018,=20matching=20the=20estate-wide=200-based?= =?UTF-8?q?=20convention?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- chapters/ch01-why-verify.tex | 2 +- main.pdf | Bin 704401 -> 704400 bytes 2 files changed, 1 insertion(+), 1 deletion(-) diff --git a/chapters/ch01-why-verify.tex b/chapters/ch01-why-verify.tex index c796c1e..527d3d1 100644 --- a/chapters/ch01-why-verify.tex +++ b/chapters/ch01-why-verify.tex @@ -169,7 +169,7 @@ Before you read another word, go and touch the thing this book is about. Open append-only log of machine-checked proofs --- 19 entries, each one a claim of the form ``this exact version of this software was verified, resting on exactly these assumptions.'' Entries 13--16 are the four Ed25519 libraries -whose pyramid you see above. Entry~18 is the first \emph{post-quantum} entry +whose pyramid you see above. Leaf~18 is the first \emph{post-quantum} entry in the log. You cannot read the proofs yet --- that is what the next thirteen chapters are for --- but you can already see that they are real, public, and checkable by a stranger with a stock laptop. That stranger is who you are diff --git a/main.pdf b/main.pdf index a5a968b8c91099b6d2cd022f1b25a3f4e3190f4c..2834b4035dd37156b9b60f96f5af9c89a290e883 100644 GIT binary patch delta 10357 zcmajk(_5wu*9P!3*^_O%$#vJ%WKFgw+q}Cb+qP}nQ%$z*nrzqme1E~W@!LDM*2X&4 zajv*ehS*PrTF(d|VSUJP>z46B#lOOVe4LO{Ei)CBe(j(ftEi$-xtOuf=*TW^fJGf* zad@sq@$n9sq(d{fP_fYwZwz6i5J;otC8*P?Bs}}7l++Hq!=U#?+n06fQg*GT(@<`LPX%)>wYRDlbjjs;X z%BF49iO@fbF@N4TCh8UvppPQ(L6>I6f*>HbRyu&Ar>Vapx<^<`D#vUs&Ztbai0F3a zDiMDmtPNs14COOebl+&a9}#pMubXV{Ul&L}VNy^!pPAoKR)2AAtXuE6N9rDMn@Z5( zW6k5*Sl6h=>eZImz@9-h^%qJU!Z&E^WF2aAoMVqYE^Krk$5h?^+pcKwDvwy?_|i>) zbZZ2ZDQgpcPG(H>_a|SHA z=9O=_(}DgW<70lAy(bKmK*wdp=_>j;TA9xYA1TL=I|p8U0uPF!0^BY3c69^c;yvo zAaiaHBYQ@FD%UX?XuYh5lWDett?HX>h>1?ti{$@FxF>rFv)Oa zAYSQSh6?e}+hL*4AEc^x$!(#`r?~{c!C;>kQxYQ4?R1wtXz0>{A3y$yr)v)y9Z2#8 zb{PwA&FYKx_v&%R(_fwcV1NvvHUhzUw{<{QEg(NNFR^R}zx+jdNdtp9gC09ZEjW*oAJ1_XPLKUp^yQ6Wsj6K6-Y=@$ zTG&p)^ay{C@!tV(eHbeKqF=6nCklPO!7-|r5Ij2t{+_9Nn>a)(iTB~NsnYRmb2QGV zdW)YAj$aFcUw7r-(!!{P42qF5x~knQ9PHXPe*GTJw`G)c-?q$O;9CT{mR8gsSC|P? zMfa-$kc@EAFkeSIYlAWbU>iLK%~YPnZz422aYboN8wBR7-C^Fn+Y{x1wf6eYFD$g* zdfzAJk#wef32}~Dc;lySR->$O)j%-Q9OmkiqMZqOzecf4>SSY&7j2^tSXE=4k+}J% z{xsBdE*K&uF5U*Y3lm9Vd$(_o7Pi%j2vnIpdd+lu%`sQvoxNc)TybEr4F)P~>DA7+ zi8?EQKO8aQ>``aNg~t5>>K^^ouhw9h1NA9;Cv?xmjT)bFo=w#s(`f-)ioLv2#8B<6C z?VRH}1G1|z>L{c;*R<Zv<#SRM+LbFN+( zJ6IdOrI+f}2p;+HK zi1mpf(D!8r>LLf`;j1thzL!`Ecxn;Ic_P8X4r9>N`XR?~`tOC_W8s|;z>FMZ=8gwCY{XWoWsqH8Lw41I6eKjQ zfgg46g4elS1`d(%z`72K37YE2lU5A|0 zZUvxot96aRcD3VRf5*!Q;kGRoIgA>_lZ!Gw@;d5KkP!9itj13!E}ivugl%K{3kyUa z3tsNA3*GhRR|>>?aVQ$w@leq?VC45wCEE4jJ~aajge8b}77mlEJN%cm&No)QUpG&9 zzLtYg$yNwU_unN2S>&PhGw; zJB2?>`yHz@Z9DJP011ZIeVjV|SIkV2Ea z?^ifSz^`qwT?9MX;&|cK-Q@P#%k1i63W?koDKYfUE!Ravq6ybk1h6TNHHI48r&GR7omHK{KCbU>Px^oE zH?7bQ5bf@8AVO;VE`ev8LjNrY6N+deVsZ&W&MiOBTAL#t5qCT`g8quRntcV|4B`TY z^6a7^M_S#kVC7gS^hlwNJ!SSCy>)v zgYr>(%YrbU^IxcR%(Q0jZR>i(&ZB!n%C|5($wZdE?gdO<*AjTl5E)`OVR>ZN$LLYg z_>kg9X)NE|dF;cXlF+zQ)bVU$w$=kHeo`fhX?ahLPn0xtAUjZ>tr)Jh7DsN3)Hk%` zNqE)cc@gT6CBw_e)a8!Mvn-6S1xQjPa1=ws z(0;AnrCbe!B;urOFnWZC>bQ-LvH8g&4I|7<2S0l9-eK>-=Lf`#1`M@UkG=pzJJK2{ zvh~W@*y25EQb%KLKv!WOG;50k7_S|a-*okgz=pnsE=LcbFPIt3ZODDpeVI}7N_?Lg_LXTJw4=Sbl zyvva}0@V7=$W-FTP$kcT9`+l7fd=G2?=4-s-#)_=c}VkWn}+ObK1Rw2 z?KlMMV|u&=Fqs)CKapRL;g1mS#7gnc0gTJ?sN1s!k95=1WS%T;`XeVgaT}uL0Sc^g zo8)zp#{;TsaQ#>2Y%#Tf17AQKdibCrpx5=e>$N{>S&n9%=_Ijp*`- zEhfT7vbk`@ry`iA1eYui52aVi)<|k|ub;YCOIU%vv*jMYAORoQt7VzX=5wAg0dWz{ znm{6O=M2id*cU~Kuwx&T;R=7sV_NTZrOULI;iHCUQcO0HX_PPU5DAjJ-_b~nnB4X~ ztvKw?5x&N#oePiQl@l7eH;cF2ci>m4%jcWH-V|_QNkm#37F$E`$SH@!{p*9G^l)-o z6DIeMf@e?f+XrBaIrWu-3#^YVWBEKHjhvrae@r(D8?*M!+~{JVJG(yW(H(kxVv6it z3<$6mSf~{t8??f^{VRr|((Iy}n7(6S7DRBv9$pP;R}${mow-2ZML-mXUv=<^H11al zWwl{;*kSTbcvSc?4IA|uc?CxZlRVLtl@;Q>mBmd@f*s*0SCoJh?XWD8O*K;2M zCTr#?WmnrxUUfbZm19-Ex_8;oV-a5QO&LZ|z)zTCszh!`If-Swk*r2c8o!ClnY(_4HpFL7xtdU%ssaP@$FX!Jv9L*% zm2b5h{~nQ9B?n2&V)%hql6)GDjed2$Aoo+)f*x;g`}uOghD5RY~p2O94~;meSoZ$sr@glO}_f3OmNMj~wd)REVe-w&s^M(jrJH>(gL*pQ?;?SMXeY#Gx zRWrF(!|^>6&9JQmwlM``O+-!(&O(A(Awas=G}U9-1oQ`PKASzAg2e;NO2#*vD8ULV z=+!nkhyux_Luk?USS-v3=7O;OC63?9zG7ksPDG2OjoXdM7^jxuU(xZoDv9&P?8pPYncNbe5O7OlIp}VGY@7gV5M*blewWt{?EOjGMiDkN_jW zZmJ`^6Y=s{`4I3jcT)!uIN(C^0df_cKV`7aIT0Kglx9<^msw(hrx-N(Lyj;YdU;QS zy|E&>1%nrdsl}~5>WwUqLJnHRL{r3KODT#G`aX~vSJ73@(}Ag7gpHI6?lB-M6EcW! zmw6`-%dW}&-bAXOZh3WRcX+WO9Jmgd<@@Z*QW_zrInr*Y4T6dqiRR`%@#R%6L(cvq z6A*LveN9Q>c*dMTUa->YZY2&PCgjC!J_(bVfUX~ng~4ED5JR+Il6s^0T88^Br_f!s z-j;&YVcLwH6TJR}FrI)ehW$a>FBuZhU2+L8;zmCc$%lf~({$cA%bVq(v$P#)qtz-gjyQeWkJ*IB_I|h*)PUJ z^mgDOD%kex{~}Ca-DFTeqw~J_ z)3$y17A6CbMw}R*T%LSlkf*Q;qfB{b6WG?hRM;jvRpYgZMZT+ka!+*hyc)cCaeF2} z>U|AB%nCuwg8UEEf1v*Z^PeyOf&CBMf8bjXvk)9FAlX}dA`r{q0As7rVZ$$Ic&}(r zmrEkKxJ!dRk5~eqB!W9TF7Ig`j-9-WH!T&rgA-odS^gm|M?4x8TliQC zHvwC|d!~?ovxReX{Xkb1vNukG#l8V9=q1)hn3S{7%HYE0_FugS{#s#+H8emmp1_rcZr7>G7et0y_=5r2dWH7c|u7VYbQy@grIl%$AefQ%PgN z3RWmnDV%xXg(i-OwPgNOyc+#>WR&6}BBm*Un1d+3;v^PB01c<&!7`F$!IRTMFS}ri zwaz&kFsYN1$}Yiov&NQ4VMr-4GcalwdW^O1Q7&;>(F;P-Hl;&|IYp}??;%wW+DgSN z$W~)a=T7uOsFwP}v1n~aVU9e4l08?7D4b|0xKa`J1EhGmt^Su}WLwZb>1!A%s%x^9 zXcv_MK1iz}=p~p#f&W2~ijAVp=1M_*fK<#IupKebs`o+vnU{dXo%09nRr>3hMd%lF z90pt)6=Uzpg1S5#YOgyHKX`)>zCI!4kSB|Lq;SkUt#B$74F->=b|(72rQSa ziQtLSlY{Es^cu3_y|p z+qNh3l?%WS&lX2QcE&pANy7RSjt}c8L7Ty1J7NSaXOY(n={-X-@2_SYc@}Bbs$aw= zsFbS)fswDN;l(ZM=XK?-n_%Zy35iTKF>Fbi+k%Rtb?~fJ;%@J3Apq$2(}BHCW?J-2 z5EQ>H&F}eU)X$$=WpGn2<9@k@2Bxz>_}P<1&#>_Y9bgH5Nsn|CxEK&+3bcFiLZ0$Oc-lSgA25~YyU^F6TY3M_)BW;;uX0oM{@BH4OD z^~lY_z+af7ut7<8SffSY8fMwrXo;l)W6}^E?OGt`dOxFCOX;wk>SFl)tB5|vugA$k z$ zX1v9&(-~SfsoO%X2wSDwKvR=yYg`@7*kTy|M1bpmXQkH3wExJL85uSdMzEAs?ENdM zdNB@YH zt4-!zwp#{hRc^m2zx@JHI6!IY`fh)IjqUDk$a`Da6%z75HBq2)08mSg-RL|>j-@gGL% zx6rA1GuRX4Q5pWgGR-4clf?<>dJe-=e*1FN8oHF+J6i$Rb7n2^H)KyC#t9sHhvAEQ z`*!By8o_4*kO%{Pat9eL1OVOP^ByVdgpr)=5zA5J|^yvv};P+C4KzFXsU z$GS-{CBrDkfPy~ljFMo1_2Cy`jYl$6+*?;)r(4q~G|hqA$GL|41BOn0tjXh)iu;d) zUkGavZ!1*EK->27!1Kwj4Sx@O%gKog_}UE=GzwMGPo3X2Ql6`oEw~B3IoSX}0=`|X z>En;ION^5woh&SNW(m|)d%2ofEG0{)gB+bGbDf#9XK@2h!-IFbPEkk4&lmr&Y62~) zoz4PGlZCYu&F1Ddo(C&`mn674-m^G^gfrz?)X^t_ew;y!d7;jUYX}1lZxPnNy*T)2 zD=X$!LYb3@KJMegvd+KXr0YJYh4pmxD4_3$+spR zZ{FX?fK<}Mn496}gf}`Mne=Gt7WaAV&DA%)XJqT(@;2s~>N7s)(A+aF=Lq-N6g2Vq z*Zdh!15M#RyLOLjJoERAe2(@UZr$_%MW#DlA>ZShrIyBitr>Ih&?gKg%Wb~i?QdL{ zIEmM$_XeVVqzhavJ*D@c@d_3)`9j1oBuM;Fu>Q(tt2JtRPLWbnpn>TcF;+ctAZ(9w zx_dTeqn=q)5kg(f$XY!~Q!)1TCMcY9c+>z)6QoyP2VNPxLLT1*DEeS#YG)t!9?V=&u|Y7mdZfvb3T@ z8_A*%hYK0QH92asbEN_h_)L=L@l#d~GI6-IP}H2_BK%}5lCbj(nSQ&jT6Lm{^&aI>I>ZQ53@e8bZ1S{X#7>yH3PNz z&suQ^cPu!^Q+$xNO_iX)y_D~Wiv4lp6owX5z#XF?6Rr5{W~)}z915={b*j^excIo( z87VQJnHSO-aB7Ec`3 zmFA5;lV5IMfUWKOYd0J9i}FZ#9*USq(DUg7Ora{IoA`(mJ@C;J5EbqAKmd&R_dBla z7Ch;{st{y;!a=@pOB5z-nTXdAqdBFGk_b}OA1wr*4eqN_dxuD}<^b7(qzCWgiU;o= zj5Kdf(Ecq7rRyOpnxZYx-|bY0mvsI;jk()z3JNe3%#w4gc}H{#j8yVTY{J@beL$e| zFf(M>5uh3EuqfL179cN;K4DeQAy8Hf3@#l zno_T=mvOcdpG!JoqN72(#x$p6WO2~(toR*A^TkGbW%6N!D+MO zr(;u<^?z#H-Es%$;xXb8K1#3m($lXq&i;LUmP(sV2nlXTXJ6p;0j8vPHf2^j{=dg$2DGb*qO^ z;QiWJ$!m+}r~&15#w$21TS?!ajk}wqBhNS`F|T}j#o9Q}OMwGI--ySy-5gf7Yb>r> zuqC^}4IQ6vdW{^kfB{%*Ts)EgJ$4S&o0;7Y^3o%4?b zDF4BuRh%qfNq=kW)@SJs;y?3pb@obAOdcCtif!ptMy9WQGOdfAs2H4hssBwKH0%VY z4x%#IF5^05gx5xm{)Z^9dD3#@>G-{-7*5fZt4+TO7rpcMyeM7BN&X2UKxGupsHZEZ zNZasi44^_=9=01ssfOWdl9CVJBq9kbHX=<#xw1bJh4A}{NAOE(1arsV%5txP1Z0nnvWDW z&vH7gY;a+*es4WyPlPKNRPSb^0On>UQ#7WhXABp!1eSq9%d_@&RijaAZBRA^t(Jk6#j>ACE>ZifIW9py^Ibqr_s+YB%Q-+IEWMGFp~Bt(|pUd z`oOSJ`;h^2Rs%t=r*hp0{O!C}RuVUoU5o0t5SD_ioAd2F+Z%M=_@AwC6?Ir{0U=jw zJPpnoC~aZewoh&hFuQM z#pU?GQyT>&95MTCR+8`_zNITOS=NV-f$NKg$MZssqqg+@f08*BO+I+$&0}G4{&`;q zm|laws#K9tzLW=UzVk-M%=O!6(db&3L)c*Q2cT=fd^j|I63HE3kLa6c4z;ufSN6~< zdqdP+L5mA}pjkiW%MUI#f1q~)A0>goDBp%;%1LTJwe8ZrtbyxWK6f3OsUOYrk$u zePNeCVOLoxm0-aLXBYc?FiwefMu&%W$tn890p^GW<}dwPm!D z98DLgr)X}Da(%l0qTs}hVJ?d$#zoHhoKdf^<2=uW9Fd|vO02IW?jE%_ zlnwTBt-N@UlY5hvo16eFaLo;~_MX_Lm&YTwDVGv-!P~+~#--5{XW_Fe0;kxDTaYIb z4or2ffN}!L!MB*~OHyIq6}c0XKlq~SCJJ+pU;0TtKUL`Z7Q=AB@{$UiLN^4W_Dr_t zB2q0)kShY7UQai_{`jiA>AuRJw~Mv=@#dN;da;p?eGztek4um+`imq$Jkv z@nT>Ti}>!d?y?kgB{15nZ+I)OR{f)01*_giMXi2>U_RA1Q0Wo3fKKvgWZd&_%d6MJ56_JP=537w+ruH+f4p@jp8cjAf);F;n%&ku~~TzQ7XYx<_+doHP~4 z9lv>nr@ZYpad*+NAvjhoFz0qEmu4r||SUMud&d=?J8 ze5k9s4PsbLX*A9_uU0o&&N%bhSyoLf^f#NP3XePOav)F32_Ms3s$?HM81p_ig+3m1 zyzWWT7CON(7(9CY6W{{RT>Z!hBi*Dt4Vl_3&{(y7SG z>T+^(y7+zr>2h#=)8*u3v-H;e?^B`6$Dhrsj0;kB@q7y*d;R# delta 10356 zcmajjV?&;g!^ZKr>{_;MTg$d>+nw3ATV6JoZLDQn8OwJ4fA=f6AAFu2Z{T|*ebFU< z(KYzQX2z#~g8?4ZAT%9Gr}4=(h=h(66X-SSQnh8u{Oh2Gkvm}!K3kn9z zu>Csu)yOc`nxaI_<`)+iuSRVjhGJ^jo+E1!jc_g1V!!m#e`{p0MF6E=xyRL4y@HXg zUe`>YZx;|@L@hfL`P-|yT1VoqQ(MMb*}C?GpY@4eJmcW1`ZnqJ-W92KD-TOT0RfZ#$kPzN{X-aD$Hy|q z9#5MIGBDQ6`a4cwqG?yXs4rLEWAf75wSoQ7=&?=U|DdVlu%KJsuVrQ;%%CA_w-54Z z23|6+0LTc5sDm+jM|7u@VqPEa%bN+zcY|l@yxHUG3>Jcl!$0P)Q&{(iu_l!h43PCH z6}nO%0+Gc`xCKYqOXSWDP}637M!2bX`{`~_Hd$C6Zb5W7&SlcPQZ!1OS`FI`5fJcU z?voo0E^>={oAoVd=76NI<1f6%wM`z)ljKr1}x`S zrP^!+D8D6!*e+|)IoD)Nhb1Skx_a3z5U2Cu1eG=8F*Q%;D27<$!>`XbN?U4Y=s3=# z_)lb}>x@_X!|tds3wRwcSLh7pP@YM>=Ld+6M`M;4eI2e4@Na`th+#3R!7|?pfLUW> zd~$)nW8oyI7Gm1GWi~J9A!=utOBz6JGdCiyI@nqvlqhnFOZdsZvaU$g zVNhO`J$g2N${p?)5TmNMVF^*=q1+D zQOdxj!3#c2`+P|ILy37z&zKZOGdEse(Z9RJuF1f{SasVmA2u~tHJKrL4v>PA!h~e0 z^d(XC)#~@?Ja+$#7&wl>FgJ#U)@mTAeB59`NeN6XjuWp5{fDxUu-su<75)tr?uHUt zlvR{gxqzGVI`LNvjWHJ&D^Vk&jGRx~g$+iW)jXl_7R6d!esJHC;%CFRV*K^k5dUeB zAead>wGdV4sAn=m-jOMaQ6MtQQIV=|uE{fceDlq=v?9CcVtZ{L#dm4!AGDlZQKeam zrV;o%e2hgRwd}dlg((2f7I z_tTIIM`Hy{oqP@gLd&9!XFc{uwb#~Q%)lITQ3#DVxSD*{{T8%RKE3-f$MF?5+RJXz z%;pf2_H8buOjyugJYaT>B!&kDLKjv)YzcEiw+u%EN6uYZ4H{L!sLn>; zxMnJ@{;D!>qK{9LRC2HDm$_87hfF^zv

!6vx*SH-s>wQM5&6&w%#^)$112^aj?%%YgG`~K@n>vM zMgB1)i`$?1w2YSzy4Ctfv5uR>FD$W)=2z5lp~wc-Rv>C{uBW$&&gRB0E{|G6NwP?) z=8J^SGTdDbqSw4ltG!xaYh$P&Gw5cF}Ng6zq#3-1$f6@2CG50%! zWP^aSbQUA=4OJw?uT|8JRc=(dHurtGt0XtkDku{N*Og&j6IT!cEf-R|9yZJ;e=f_p zwR@;^3J}qB?-w#+CF$*bzF6IQK=v{;0I47MVdaW23(*0l$P_l`VN@Z!<+SOL&ULZn zdgCnE8}^{j5;2T!gg^i7@xaWYdtqYqLpvQ=T1A!m%LlqRK5md2x(VfY1xdwU$q17) zLP-DAm1p~}#!HNlARV%caIQylJu!L0wXK`n3Sc05Ui0X9Q4&CWpDQzuLP4&~V40}pjajr?_wv||y!q4AGM$U}(=-8># zr~v7>@q{bIZ#NExuFDR7W3II_E%^g!;orJ;)v4U%04xl~HLAY7ce4l7qrAvC<0=U`fFaE5Mll!*D6Sbbx66sA^}(-M?2(^X<3K4!vbc z2UVoe@W{+!e`wh%K}G_aB$}fF%Y-V5!S5ETqs-UF@{d-J%j(mDa~XI zA#~mXl0j%vn0YXwf5&rs-dKXF+Ps*O6xUSPB97CArk(iqk->GDWUzBd7qxvpE)+_z9EexO zW`@((wpCD3ywr~Pk`tUE>d&+2n}J(zZKQ5%Wak)N`1h)&L^X0Me`4HtEmVJBfm=vy zlwAG=J#;56E`H_nd)hP1!i?}?Heh5dp9abaN19&F@g6PuXaIy8Y?=Sf`rkEPcL5qk zeP-$kyXl@U_=LE|%3@_gzk3LgmiWp}iHSsUWCa#A(sOw4XO-KtC#j zy@uuC{`PA|QGN91iLNZ{u zxD&jh*CB+cM!c}+;{$;>%nhZsORV0yhTZy93r3I?%`Hl33^lFK5e9)+G>?Ors<6Q^ zRgThEryi$dH_iqn5!LIE;I$z=IJA7xN3{V>#Hb;FFmn)noya=oG_jpT&h0%x4G)De z7y;h>U?sjCRNxQ{5rc9|3VhOtaOc{Jdp(Wwty~%q?%_aW)?M_(GR6u)aqXJ_kQlAu zUNXQc#=r9DXT27vawO@5Ul=c{^}Jk4@khEX*MGd(v{^!o^5&5=5P1ePgF? zQH&7?NFt2wH-`>-+ys+*Z}QjfgO6hyaX#(}Jwx(jNeP7N$6JB%P_gAu$1R?fXxfTL zij3ILsMfKF7rM{@*Gb}=;b;5lHEAO>*=djB9q|~UhxiparLn~S>MDXwPsRrkuQW+l z))xG>?dDeK-b&h|gKA1k%`u#{g6l{O7Q>^Gb;C?!Pz*ZQyn@i^{pC4rTw6Tfzt zol$)&Nm1`}1uv~1Io3lr)*L@0F%ePS#qlBfg~;-XBcoW_1a1X5aoZomqQ|Npg=cYm z33j~NB-;$6;yaa9tlZM2@X6Fo`!+hs7 zRLL)~JF%Guc)jB$+@7OlV8ev>m`Uev^)ZutJe~}!PoJOBMM~~>^H)@eC8w_Wu?G}~ z)Ptbvv0HH?gi6Dy2kQ59-{uAXNoCQm3xZQu7Qt5HGbMJ)Ka&*0vsYrD5l51P{p8L^ z@T2Ti(V{b_DEfj|KaWJ?Z1#jk+*Q)>%%t9GSvq0@IC@Np8NTuTJ$UL~?Ub+?IR^)$Yw z#N?DMpl$Ge2s(DJaUVVTuLs6#!Qa2C%pN3kc~9A&QIt(#UU2y}@9OO;_-9SV==N_Q z^%^%@n`jq9W^y&vXCinSyATRl&AJ|eVzmd>{m(&)6S0ba2mTFk*}Ev+D{N!+#T3JY zL!>g%MjQ`^>50Z~U_8qSWG0A8H?oIZ1Y6Glamb5+kj>>Hf+PXCsw10?_>X%_h5(aM zJ?;@p!Weu>xn2J{Gugt(N%cCjUU{3x2*by0Ffy0$xp3F_?^t?-8mGOZ5vs`1x~C^H zE=3G|Kj1Z z$~0)Ek&Jp~P;rrtha}{AvOD_KfFUXm)(lD^jXdnw!D2Irj1g5{kxE1iMaa&~=*Ca5 zePq9H&Lmg$?+~n+!Q7Ba>>kM#`nK0$+b(LNgl?9Ff@-7JeXf|>Fm~+U^;wQ@cx#4@ z(pjbyUA1M|+1S(YoCRphEwsH?%>;)5>c0i7Ic!Ycn0#`9g#@v-Y2kjXp*Du_#_Jc2 zbwdPn2jtG6`K9{53*LGTTteWJx8toYrfAhc8Y;{dPQsmSrzCG24CaNa#qonQjey%G zMnmFD$yLZrlKn0iloO4vCkTvTx%8T}+~KV5m3Es5(y&G|(TOx}Ec1YXyhj@7={jvf z*(mqSY<6n+7#9-3S3Pdx@l2>nY-CME>WRH`Mcl8P&yKP%Ye4gRcR-X`YQhmU9&oj* zFg?JA3oy~m`ZfeU_?+OYkDEnp-`QPkiBCv5R*pb%C+en5bbcVG+(EjHPDHn>>8B+e zK^6zGz@?ezzPuUvhxekk_%7okMY%zB3y$sZoqlmF z9@O6r%X+`}#q@sf-0*a72QhCz$6=-bx#V=!#q_QUWxb8%!65m!r4t>n=_U@;W~=S- zx~lj0kfQ$bm1D*V!&&A*HFoXNzICocHur(7OO>QW(eB456eBz+$HDV+=Jwa_^BN-J zd}+C1H+w4TCzkh*hpM_!+c#M9I3NtyTH`Nn{`XC>t?_xUXYZcfVlKY}8*{d>^5Lm5 zkE!jm;8XbU_7F7eR#1WWL+||4Hn%K~{>Lt=neYlwbhHI}$30!+Zc7C>zzBuUkA%+$ z{}04}ApZmPAL##l`wz^2VB6vI;ao1kS=#+$;VWSPGMBpaojq`~FYvDqJlOlauB@v9 z(_>I5wLo5-Fa~o1ww2_kr$%>&&Rn^hF_NZGu0O3MJ|m4EeMw+v)M$}O-d_q1{yy>gwtF2!sQnltg4-al3d;E5flIr>fE$})h?4dwDujuQ z(3X;sI*n5$cI3)Im|WmBPCwzghHQ{!k5h_+(XzEhTwO-22I-b0Kj9ai2{`%n5Dg4R z!3bK`yqFF=4~+LA!8W<4i;xCJJ85bQ-Mr>&bs<@LRTn044HlkN2q9S$^F04R!44c? zxS%8Zk92Bb^d||exT?Iis<3fWM38~nJQ42ngrFwksJ&ZBxhZ{RWJ=p>jol3kU7B+x z=n0qfj}=AHfrR>M%ek@QI;4!gvL+6AX(lpOG8#g@*l8QZ1g43IJ={n9(yut3f|fI_SK{n+aXfVtF%IMVkGIY%z;@^P@@vzg=rgqdGjEh+|KOYQj;#=L~~= zltwBLKSCACewfBrdkqOKKLlTC$vOaQ)k?G)k#g7Nqlok1X{hQNU(NJyv#sP}gevm@ zRYS?+09VVtg6DV%mex%YP&XN zkn*U^*k?4<4~k5r?FrjwGwXVQ@r7P40|kQ4-F4t7_1Q$&CWH{F5o}QGFvLODKGB1N zE3H-{k%$I$_l$+QL+T$Yv4Xp(3K@r7a_O!tG>TCsB{Z%_qI9t`y=@p|FgbhGc2VU0 z34AHFx5RY|Cj)QV5cN#ldYER};ySlG&Eqe>%(9lUHNR#fkp71tx0E9QN_i*k#e5B) zl`TBoc)0NW+OXEXCu^ z*1;wT#UJG!G?0vT@1z3y3S#m=Vyf=gd`E+Frh2gs@ggwO6T9grQ4=j3q8l$Zry+w2&2qmOcYH=Wcn zx(pl^Eur3uNdm!uu0`sh#ZC^8h^u@1ob)lQQuFT40%YwwDq}YlE>j=3JMFZ5ipo=^ zTvrhqYfZ3V8XcoUVqGg`aR$P&b@RkY-7y70ndt)o!l{-LK5YY>4aBi+WI;r$#ajok zoU8XJ4{rD#$7+JwJ~O9^s~V0TJs^vjNal$-bFGtu-C6=%wuG9=WQ@fu>`^ zNGTBOY`JQ+fLmTT@l`+Hca}qVykal#U*w{n)XyCL=l~$b=|j%9v(@dDxh@f(zc=d* zV()vF5IkzrFcmmB9KN-HR0P(VMJT0QkeK1ll5+nX>?4*qFdf$V+e{&jwIKVl%MoF8 zS1|43V|4><8Sva}8OCdTtR+4Tir}$K^n|)Bog}(&qS*)?yJ%R5}#Kr*1DgE=uLn z5;%&N4mMDyd62Kv>SbTeQ~Q_a48ay?keU4WmEH!x51Zm!f@^GA;D@Ls?#t&UVMUST z!ja;VktKr7pYr=$de`2=L~>>zxG_8L*00K+~m^Il@iBTfD~o*o1m* zFRRh&8OS#NYbnOmB~c(d@uPS90def(T+uJ45&zNQQB%Cy;;Bo`mYTve#u)OrH{TrK zE6oRZP8G}I!nxxp&kh`;=O$zGo($rsg; ziDbb#+cci;@)6PeW^Zt;u(XSHh@RH#F!r;DvO21ewBD+0jSTv7)!SzbGmuy}*aC4e5FZly$^dDCSPm2@pXRsN~CVkXz(+0wi` zt&GSm^tCf^l`4^0ARrTNX>H^Pc8WyQdsV;0nz2n|79v)UjNh zIHTZ;v2vg3-Z}n9G`wrtJFDc_TXO?$=lvPz+t#Zez7ji#`{CNU-IvE;;+HI(`(Mvv z3jjRA26+m{*t=YU`E|_OvlYrZ#u^an#_Up^0fN7h1D zMn-1rn@T+hFsm02?|pl;Bic=JGSzYfU2(oTvJCa>ZU_WH2KjsGs52S~0S(i))Mpd+ zzFqu%Syj+`aR2{i61**+=%n|y8LqE7Ht z!i%>Ja*{CZa^FEkY<0Cv;LFp41?!yFh|#rAR~F;ZOCk3Nd_B*>?-#?~LgE9IyPrF9do}Jy{x?JeLmHYHt^Cx1j`(X^T};a6DD&Ht%h2djyZH9uhF z2J?w$boT@v8JRYMLZWK%Cu-crfvkd2uCvDApvnDSw%E~SjkELpc*fKqFCcp+=Fa1x zVc6qvWNFRZBfGHh_;~T%|2v>7zR0<)TuiDCpN-^X9JP!b1LUk0XE(!;v?uQIPw6^Khai+%cBiPwhsDAe3{{=mi4?6*|8l<`mt8 zD_S?uUX-otfv;zC)!(M)J4-e>*zM4LZQu4#ZV~dv7JIpnDrPE4YWUbxZK$);jYJ+ z+ngf{bYl4D9+@(dCAW(rX5VBTn`NiCX%}gD{0t2mXSyNYWG!C z9sVMJdTH4eG2+y>j#_m*vI-hIHPwNVuzmnxk3PUnX)ip8GkMxAY=Hy?UhWxkx~%N9 z6}?EbdemIK>;PoGt(p~ zHx_)k6Hk(HhpK&FIYQv&awgYG%0it_!qU$v*^4@xb8LJgsCJYXY_D9>VzG8#lzFPc zKhW&~+Wz+5w4jjDGHT_q5o-Q>jux;9D6`UQRyR2O>YkCNpO0e`IyA~iT@;StEV_k` zF$r%3+9b~0`2_Qsl$`1!1XpUmhwXfKsk87d=0z{MLTheh>qFD2HthS(9*DHDm&^9$ z{q0KUJ&v_S>_jU9z+4y-2D65AE1!ZLR+`qmeKD`1VxLV)9;t4$)vPC0B_ zCLx$Xn~{IfysC<`l_#SQB(avL!j0ZxkNvJUigV^mnJAn*jnX`UH<7nFd3}-sIW>gT zR@whGT)Zq@F2_ucolGn3{3XJTE2h+^$i8x%J0i=?a5s^e@ZYhJKHK)j+nqe03j1O; zj}ES?nPb;%l^ffms5B6SahTPSp5gbz0u zJf_0P!UGSWYZ&>)Js86oxANfXt5Mn+O$vdSDx7|EP0z$BwO3zENtbGiSdV*sa(c60 z((@%Cv?h2|6S`9}SGMYKVCmqLJPby1{!Cw?|ED~w72PO>yRsW1w}%1Hj9t4&oLY>v zr4I7+Z)9M6Kecdql_HX7(0w}jhW?McftdDuH_`?DkL;44J-_MVC^tu1H->kKS zg(xht=QqXWz3g))nqe!}XT_u+JKXz*SdgI9CO}gZV8ve_gm({Q)phqo(N)~IAjI*N}F#89@Umvf_yZZVr(}4t@QY4B*4@kl zCR({9Tq?B8?Wx-p=>zcFJ@lUpL~z(Z`Ss;XZdKPeP?d^L=K%Z-+4LHI?nrKsd2_E7MTk^!&R??b!WQT(~8@A_U`tvDT2dc@2W z=2zk#3|qiqzo+IaV}0>Cp`g#_?H23^>U)JM;!J(FG*H>xaCC!Zr({e6@a%9%I1Cu};Nddg?H*cX_=~nQGn`;R>yZy;kJk%lE2vyz zrUL|gfa_h7+mGFL4{)?&)9c5$2I2RX(nWDqzJl51g$C`7rkx)T1jvEeh7`Y3{=wxw z;wkvqVBFgw{r-g#^K@*&(4JU;{0$`6E+YFW3113t5+{3pzpRku$6stlIvp3h z-{HyFzR2nyKgvGLpt`+2*l}+6jNj^%-o3g?=(`}}j+%s=E`aE~p}w`C@8HD0!Wqex z>1Yg{(YGbwMIiah=%G=y1qC8XNn74v1b;|aX3 zw3$LodvCU&Uy55Nly)DA|FGD|Wq5;mb0QLo$Il~;0d0Jnt@=dLe-TpkgR~k6lEF=d zlry6LSK6;_*gD6Hl^qMp&h+9pAOPy6J@bPbZlNS@kg=@8k^E@$ zVUqCWF4}}2+O8BptjG@&u}?~c1OVt0fk<_-@CI8T%z=0LzHIw8eYC-Aa^Lo>+yqp<>U%>tI?CmwX_f_FDG^X30-6kj516kSlck8-3u7Wjg zTXQrK1Z?uxWd5Pwdo75MKK<@;JoO%N!Pn%kD%9U)(0M2?mR3aLX3~% z|H^K_XC5%??GoY|!iQPn-!E*}mxrrVgjkHt-j#iB>kopwpH&$Z?D0&4%QsTGNiphP zj=+|D0|`&I*mZ}5t;u(x0U;Z>{!g&1@m>gRhB;v9j{H#$Kr2yLeV2Y>ed*HE*-hE> zK}^6m!{2Wi0aWTMl75IYQ@=ty@_A4v5t!jKKaN zk!>u8wsg8Po&o(?)k}^ldM}tbML|sV0|l?@Rp$Th2z(b{1Ak79LAWQ&S68GYei8q5pr;o>B=vjRiLoy7L824!fzJY1Ic$3d;pgNhzuH G1O9(AG*S5g