From 38fc3f253c0713c4ab13fea83388ab89494719b4 Mon Sep 17 00:00:00 2001 From: Anna Shaleva Date: Wed, 15 Feb 2023 20:18:12 +0300 Subject: [PATCH] models: add original dBFT 2.0 specifications --- .gitignore | 3 + README.md | 6 +- formal-models/.github/dbft.png | Bin 0 -> 94064 bytes formal-models/README.md | 141 ++++++ formal-models/dbft/dbft.tla | 379 ++++++++++++++ formal-models/dbft/dbft___AllGoodModel.launch | 42 ++ formal-models/dbftMultipool/dbftMultipool.tla | 466 ++++++++++++++++++ .../dbftMultipool___AllGoodModel.launch | 44 ++ 8 files changed, 1080 insertions(+), 1 deletion(-) create mode 100644 formal-models/.github/dbft.png create mode 100644 formal-models/README.md create mode 100644 formal-models/dbft/dbft.tla create mode 100644 formal-models/dbft/dbft___AllGoodModel.launch create mode 100644 formal-models/dbftMultipool/dbftMultipool.tla create mode 100644 formal-models/dbftMultipool/dbftMultipool___AllGoodModel.launch diff --git a/.gitignore b/.gitignore index 61ead866..2247a5f8 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,4 @@ /vendor + +# TLC Model Checker files +formal-models/*/*.toolbox/ diff --git a/README.md b/README.md index 902ae367..cf4411a5 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,8 @@ [![Report](https://goreportcard.com/badge/github.com/nspcc-dev/dbft)](https://goreportcard.com/report/github.com/nspcc-dev/dbft) # DBFT -This repo contains Go implementation of the dBFT 2.0 consensus algorithm. +This repo contains Go implementation of the dBFT 2.0 consensus algorithm and its models +written in [TLA⁺](https://lamport.azurewebsites.net/tla/tla.html) language. ## Design and structure 1. All control flow is done in main package. Most of the code which communicates with external @@ -23,6 +24,9 @@ own payloads in order to sign and verify messages. 5. `timer` contains default time provider. It should make it easier to write tests concerning dBFT's time depending behaviour. 6. `simulation` contains an example of dBFT's usage with 6-node consensus. +7. `formal-models` contains the set of dBFT's models written in [TLA⁺](https://lamport.azurewebsites.net/tla/tla.html) + language and instructions on how to run and check them. Please, refer to the [README](./formal-models/README.md) + for more details. ## Usage A client of the library must implement its own event loop. diff --git a/formal-models/.github/dbft.png b/formal-models/.github/dbft.png new file mode 100644 index 0000000000000000000000000000000000000000..5d9f94e0a1bc76f78ddfa3d7f337e397266786ba GIT binary patch literal 94064 zcmeFZ^;?u(+cwM)BPk#VLn94>bhm&YEg&JykkSoO14v4DrwB+(N%zp8bazQJbj~|o zdfngsyzejHAMkA3`P0mtYaMH?BlrDS6Q-&xi-SpuiG+lN^IA??4G9Sq1qlh|79EKA zNGwEK;Ni6Kpi6YF;UV-o#QHnGZYSlspFp%s!=+ ze^ULa9G3o+fQ0brP~J{jHBE`!V;YVI_+^5=l#+_O%BbR~V#tx0is+)gYgfZj*p(1;-|f%<5&ydp|I?)YS0ny^YDBJAj{S10#iPKE;p*z@qf`-3*f)(v z-kY;u&X&}80_drQis^g@T^e!v-~M0E#3KSAL3ue8EwC0^uUd3DIxsK?0Jl%$h!fV@ z2?-D!o4J~vG|p-7JXvdC+Qs>UD<#6O9>zR7|xt1 zDCFV(mY%r7e0tu;dCZWIiR?FUwd zOXFXZGjBXZ%)pzHuWyB?slJIsSQ|oJ-|6q24bYzQ_1*atwb7oyzKgtZEy;GJRbMtW&4j(RIgAUq4|%huzpFo5C5(BS=dlsS zI0^xvI8B%7@<-n^Igp2~u5TVYE#OKCUXmP)gcgoSZ~a=89n zwhMBDnuDHrJ=sPU*?@OiGe$XP2#ZgtuDezWR*#+zkLNTu--#r2J)+%IaR(z|`=Ln6 z8Z66VEY&ww$c|=-&huK0ZD^5^4&0CILCG;Vf!g!>O>V=pANI-y*H89~l&8?AQ6el} zfb|J|hxK{|FHy)3KXw(=7Bwl$Si(731Y8g1YRfo*rC-&}m^Hpv-RO^A>R?7fq@Vs* zv@XI$<^p~!n(78gEaj_m8Gg%SGGERsqUvXb^Tz^1XP5R16q4(X6Bq}g3ijzY^r1J$ zkE;mf?ZY4qebr(uQZ?tle%WC|Chy6KL54}DE~$dfU-smw*gCGBfTA~V=w=Q^ZihXx zIlvM=-uUaq1O+bC*N5-vz!F4y#2w#kgGo@hYL`zI;s$8{D@%y!L^Z`O%H>4r5ylPL z5mx80JrM74FAggac+tD4eG6AEn(aDyobvSGLGs!w+uCb<1bc3WfXz@p62Rn1VF?yC z&tIg+?vHCu0ra_1a8Y2LE_#Y%6Y+P);oF^lZ+-MC4e-4-oxkT*u^l!#+q0C{;*I>l zoDi>4M%FSP#`p+8>fDj(HBJoq|4>j_go2WiqNwty6ofV?q-(Y7Fnw9K77(e^FcLH4 z+YW8iXiq}V8G0aB5q9MTQjZ#1ZFApnXYy6l7=`fetGAe5qTw|^ZP5IP%1R0Nx>bv()4Fn>ug6a-Ema8vI?+OcLNmfFVSw*kO zJa3&{Hh0?bH?-S11Fh>7ETS^;Y$E zi?Da~cD9sUMAY9Dn0B_Jo3lR>4~6Pfo0mmtW}gEtl7o|0Trm30%nZ9#IiYPIb7i9` z%bc8@#j!|^zKmbs$Ls;ACdPSv zz`yAN6C>IaJDmi#(HG7f;cdI+mu=O34!$%uB9|0h{@@wADNrtMk=@`YER88GuTSvZ z+q-CJ#Cuc>H#t=VzPd0=?%ZHkrI_&F=Bbu|Fwb27PwuHmxLxe3-IV*u>s!kh{P4B3 zC{fpl&qH`oMG9zr;Au8PPE6%nZR?u7_t-m=C0epmGi{Q(^G+!NH+1r=t{}9n=^Fd6 zp`%l5&>J;1Cr0^2c#-%ZGK+F5mzmw?x)nFF?TQr-JhM#^vGhD^=4XSbYn;FzQ^;4D z0WSrg>gc|TBPci^NvI|0s*vFX4t>tbWC9Dn-B8`ajlwh&+z@n97TGU`+rkdEHw#Kh zm|#BH#8rggqhv$hS#4cvs6lfIvZW{MML$I4mcx<0yd zi!6ZfknC4h2t3K5_JFv)>f6NT06rJPj4pV2yv?Rpyy=K}{=tpY!=(_nLWe?6Jk`;Y z1^>RzC|W}>K{^}%O_nc)v4GU}|vH@>5I?l}{D!TF3rt%Ib zG;y77&Lx@qgu=edeL*C3|7Q8hE@jOycIfoua%w^A?YTT`f${~bp6^PAZG|AYvX&PA zR^yBRHtS}DS))fPHA9hLIvm33No0zxvlUY+20AZvN=~C4`2s` z4SP^R9r^d!qma6%+~E;-=}rgK5xhq^db5g61wd}#N5YB3zAAG1Q=!M)HG~~jj~-(Q zc^b)m@jU~7ZKH~f04%wd`}EzGPZ;hY1srqQeUXT=2);_}k7r~Dn>UhhkMq&mRFPm7 z!SOxj_w8l!^u%wtXO$=1QXv)ggH~M;q+K4FA9F28f+n(8m1L&~g6|w^ME&zBT8WVd$^coX^i474lLt zozHfNz+AVyMWSsOh347)W6!rKy+O=nj70inE< zj~^a**N8aFz4bD25vl_ps}bCvy&hqmv_d{lu!yY}oF{&BWf*Y}y;mG0E+M3H;GO zen)nmUIEiVw7QLTXFW2b?O)Re8BH1WgWr4I^G4{y_UkR$^V;x}nJPDoy$JUzN|g+} zJm+6SxqzyLY)2ejF`m-opOS|@`KC$@GPSN}9K2IAHp;1>?Xw3ajsAjUXRE-yjD23;+HhJ_gpi+;nBV%;!)wGr z?7B%8Twr0xpLsG{GI@0Wnpeyg>R2b}N1g4wZR&yWr;t?Nh~(kQRIZChPzcdUl%WU| z(uFJDOu(H|XO>wo=#f(wdR{AEa5@0-tk69MSMpVXFaqYV0G)pyP3M2R;Q!orEtycc$i9omzXx(~K- zTYx#JY+W7oqmrR4lMN{8&X3u+IpQ_F8f!+5am3zyB+H_bHM=30BJx(` zebFu6NE;~^5qYoZ8Nt!E6HjhAOZlm$pZ@Iuw~@>OK58l}Xsaz|j~`nr-LvVF1{nK$ zG*?{{RQ3*-YMdjVw`hE}_hDBbr-aXx375?$#W-Bdk!0@1opCj-hjj*%;n6WgQ~agA zryq@Bm4)|ZHZi*q(Lvg_g$WpUv%pVOZP>khWx$&J7O`Sx zqRC!1yE(+VG^{)L#C37if?qejkoKE{o?7; zTZ3k#a+wImm80YcK3nqoNDYUxs$bDuVz&&0WE@1o68l$2#(D|wT5t}~5A8p?&!}{r)5wdX*#C!fazu{KW zv$`(hHo%czrj%x~o|BqT?$Bmq&+3vA{9Y1}9*k@1LyBTq60WviYu|AfbKrVAB-}`~q`_`e{BO)v#*2^WcTxUBZsU?+l@_M6X z%4WYHCk1AUlQ#p`zHhs+R!*}voHwJAOtC|)E!EiK(W3X899BE+)s!6ipa1JU@KPlP zNKicbYUCcGPmbqUp*ar&f%~ZDTnizK9%>?ks4sCx2CbTK&SfKjR4Td#l%p~!qfZsk zn(2`lA+{5?L*D6j|nI6WYZVR4=LYKP&&6?ww$_UaM0g9J2X3` z3r*SGB{53Oo1v1tL&qYt8WJAQ@~liTp>)OZ;{hYRfmi!Ta@sD0uU#FwUe;lJTyN{M zS0G?X0#WxiMclUbxdFb38VO_lfI7iuG=pxP4t)k1biW2iuo4+n3OzW67O+OXhUBCl zTxY%yl6+4K_2YhwHS!*+IS=GD`L>J+%M6z^G64^i*U9{gb3T!xE{FhtknL6_>DJsd zMLx4`r8TUG^#_KNi8e751EG*#&w4zb;m)K_ZsvkEZDa`_*cFv`MLtRxReSE#iSFYT zg;hQK2}M%>?x`w*kvfFF(qnW5xvc+bfu*TgRi-Be#5;q=S2a@UJOJ`Zm{@#X>e4<$ zk8U#QXEx88lA!Q;qkszQzFeh0LsC9kee1|&@KpS|jn+3vcs2sS)Vm0pcUN3G);UY_ z9z76#6c{Z4d$~DalPLoHd`UAIj}C?`hJ0U!%cmb$uA8(<9UhWRh%Ps$Tf#Bts8;R8 zlPr)nZG`3G+n|mLJMf3Qt!A?}-EJI9byd|Esaqmky7uegD;y_q-Vf-f8b==c#TjC6 z-~=f{ zUR;K{q*}E#e>1V(r>JBlQ<-8@MN{n{2NI`yrj%gF5()10nMKRE7L|Y%oM6ml-VT z!dTZ+?K(^wTdVd%0I`AC#6u%8v(D2c)xkc`*GPtNsT5mLWI3k}ThICt>iFo$G-Lgp z7{O9ojGA5bikDh1xxw(kEHaVrqx3}%nztvNuRn6OZ{%bNTaC7A*`MeO;hFidN02$g z??{-J1D0bA?_iqMiYvM>x7F|2jW0_3?NxS!jkBH(H{jmTNGU9(Cy$Ek&W)E0HW{vL z02`!z**)_2L{;PY68T**R)Ws?Z|}EfgkG|jw^OV3hbA_PCT{%eEK^a{IzjEM=P&9; z_`O3tR5PQvJUYLb4Vt`~kG8N}=LOEBSySfNCb4H<__b%c@%!b}dd$JLa~G|P_ZUV} z`2!n{<^r!t6RO-M_MnVKFD55Jcyot`<{KP6eR_emTYfZ{V-Dt+O2$?RgjT5%axoH2 zDYKfPA27BbC}BoLg!p1Ok$^gLU;8N1=l;iyu}(xa_D|&v_vBD8kJ48>%Ji}Lfez8< ztG+4b(^n%prNQ#L$34!0-QgiCiP3e6?d9rAb%XPD3tXOG=DkEUnj71vH;I082YpAg1(mG>5w=XzTUq+dZ`VmyhR5KYN28jnx;C2pL=H9d zShDTyB4vDh>||nwD)0kJM}qYqB(uJ&Oq-W>WY~|kdhpuwKVwN!Jk@U%>a%ibQA+1y zyUv<{(agiD)z%(nVmCbwr&8qq0}&LW6-aV20C8%;y1#|oH6)bH zV0075jM*58rsVn!8(J_qm}lM`Om1U=K78@y?)X{vTI7>&1n!Y6D;P3bY1Cu4+4MoF znVgl%hg5n#-)jD9_AztQNvj%C*AI_bJI1>CfF8c@8JAd=&)@%;O6$vME|x`N_iws7 z0D%~;89g5DCw*v%?f%cUy`ugViExP{+mbvBY_3GO)SQJgv(6ph4(SQjkH}d%QW8kA^$-+gfh+@Fad~`=XEIQ57+2ZELim8hS zdV@^1_ruMZh}?;g+^Mg+coX9iyONDTx8ANLVUOs$Gi3#%G2T_yhxyai(2L=75%aGl zoRE{D!ip~`M+0wcxK2gAfLlcDoePU>u=}h&XOX**uI0tNA0|dM_RGF@a=&=%-9LRX z#77!!8WpIAI0>sCx>wMK?bO>Zh_X{R$=V1{ocAsHj(vXpRwUhI(L$4o6+Zl_2_?)^ z{@97i)kjB9FQaQFEx>*m7Ylg#^qx05KYU|;%0U9I6k7FDfr1x;mId>!{ph!p*REe&)+QC;as`cSwapjEJpeZXyMWRM%r2 z;&pAYU{4e}azno114+L8b=x|Laim2px147R3OUhhF!tnyG~+bj;U_-*|1d8gEH zjcH%6r;bN9uZ6{fJ?5`OWpo*3ccl;&_NS{+(5w^SQ!@VZ#gP^tGi{)*Ie1Wn4`WgG zlBQQ?HSx*}eN%Y0{*#<*eR_G}Gyh0A)XY2fOZ}je(Az78<}()0!vf>!$$wc>IR)g` zw%F}#CwP=u&l?W7FlDEE>s}#%We;~LOU-*lv3VkIUD#Z3*VICK-ZcuY5>dmv`9xmh zVtQPAX%^XRrV#YB-A7aDuuhQ|c(st}7d)%^?C|N12?+|57ao|Kv0LO2;u47{fpr|W zmx+QFFFuO%@Q}5J`ihVZ&TKR#D`GT5oVL)aP&O4)4coW-hnSYRtfxvR9a6il18GQ5 zO0!hk`%am`fc@~kThXJ@vx}-|*JXxIkkNSv^xS1m)IWMF&t_Rrcg;liBGrEftz2{z z+Yi6_Vx{Tax6g>5P&uEbU#?AgwSMd5$GvI~cj1fsi~2_>+}f#H5HzQK1!`IT$5I|& zM?fo^jLXJnqj`5nqk`N|%p7Mf3Jo3XSf(jY-KLN0I|Rg~vf5?^o1cB~G$4Esd4^j= zzfoPL5!j8jqnfUbUv-F~uON!-@d!~68Y|4PJgM)M1fl9xF#WsJc>WX5VkV$SltK$^ z8zLE7Bf}^m%sv<@wY)$&y_k0zDF~nOE+@1JeccD+a!UKKxRy!rfJP=Rx{1q-5P_Nd zW7D+zReOHFf`2;dkfWkhp$-f!D)~3OrlH0yg78|USG*$thZmM%%3MIYG)t%HUhD&~ zoX2~*`s0lxy|FL^r!BGmq}}@HrHIwx`RfyAghp-V{(p7+OVqe2&<{jd<{M7uH$1fH zPun6=NPbakgb)-lBDs~C){cx@ugndS-sffI_r~=9;52mj{v(;fy55myzOl!IGaJ)} zer0FbnbI^0gb2G$FU?f=w-?|aGxkUSJqw<({+eH^XJzQ^c^m?7CoX-h!yF8m66tH) z`>G?=>a2#zockM8r4GY5rn2o&gzpkm8LVB?aUzE?{H+|ARj92Z0jpl5+<{(~c`~0~ zl(VmK0VjxcCjZnHF?OgzuDdQ&K8@{r#K0+GZ74s};!W|xUus`Mh(PWgSmMeT3PO1Z z<}`XKgd2SG@7To>NZ|I@eb=8yK^!<>iDiu#eXjp-Z+EY$QxVw&#mo|d$|{?*Q%GXH zmPTRxx1jm)9hGCoeN+5KDx2`AGGVmtyT+4$Sr0jUeB+5)iPu`vDpvp>TdACeP)L1}WiZcN($UGgzLwdQC+_jW_Rf6hWXtj!o_A}J03 z-#rbLkbojB68$HtKh6Ryo?v^lJX1|bNZ4<6`85XTlh%DN^)L5H&4n1=#p16TK+wOV z9zXWLID+Kg37|jTaVXdPNRzm^ART~1sb7NmR_;Hq8Kb_xJj$xv%Gdgg6o7-IqxA0x z(GWB|o4J}_-paLK897Q2JYW4Li<;eNq#O=kRyQd8zMtZ}kvER4aS8(%gsJoT89 ze_Ht0MU?mQiofOH3X)iE^|AOdZ9wj>k|}h)rufU9<(vTAEb#ulH!D`DC z)A_l68vvn!)g^tNqnnEGG;D&21pm%St=jv~oPf*F#*|jn_tx0$_dd6XyuN}aMrX9)Dbrg+ zm{5LE(GJ|e=X`Q=_1YwX{mcIQ1Wol3gXhf5o;#b#h7X1;QAl-=%UCb_8}27)r!eR~ z$~Tc$w}olgAip%FED=wA@IbtcZC7uS(_Ki_yY4D8AHkP# z8pz}*okN7W+X2FR(c=^WEX>tYx-<+m#xBxWGM^N5d@*pQUb|zE|I~jkifPgCW5N-I zYHOPvkFh1lY#JM|F1Xaqy%GaWpeLC>oUOK~&dA81@0&{SI^57`S~lTK?WXM%t%B9py7}l-{k_!uhjBWt#Vg+=6 z!XN^Y%<1TK-2Mm%RNGGu`Kk`wr~4wUVy@`#!X__>Se zEAC$_`GJJ0{emMsBsUPu+tYQOvFv+W=7kcP&+yw|QY8=wo1zP0Y4VklVEA(6G6&G* zYZxcB#!`BjzO?831KTh43WJuq9;r29f&|~As0Fyvhg|v`f_E%NKqPL1bBl#9pHYZN zP{xc2Cm;QFaF$4j)WN1-F-!D&UHI6-dvirM-5SfEcR)N@rBDeq{Py8SPlR!@zbwiZ ztlPE>&uc>MStVX-8`-OVqc@9EIx7~mXAx`9KfuGknQ~bz@G8f}n{4UlQi~T=OlIai z!?nSx&Y^W5?Z3ibt& zN>?L(rU%oe{Qe&17iG#3IMZ+7kqlJa8-iIGCrPpw*1xuu&bZM-7-DZ;>!;H;q3!Gq zS6PJ)Tij`i&LLp>5JtrmRicAe0jI`&?ikaTynHpaKhjK!yUHq>VFNFr!@jugWf)|p z4`k;eQlc`Sh}rEp?U$P4?Msgbu7u{{ZW3c%7;5PBL zbC17SY>2mMG=Rvb&FA)l*y)f*3?4+AzAo$`-eB4vC!BYFdEAA2^f7irWB2g&Lz~(W zbfRi$cRQtBJJPH)yz7>fVOiL`J#V2+pfT2+HtJ`BIAqk#Z&X^j376&zUOw6eFU9ps z*wWD`dLjGw8rt(kU|~t#WW4;g8Ma)(&$!Y*+7&6E<8i#wqMh*`)6t6(I4A5cahtPV zvp(t)|D)@zmq9w;*O>E#D_TRpgN3`;5;Bd~(}z_d&Qlj(PzqeXG0oSZ&Af#A>QIC9 zhI}doR1I2FLb`kWOG~MoWuqdnnaZk6-L_K>4nk>8frNMA3Ct@xVqDoddiz_9W_vY= zPMZtzZJTsK_O}V^?q6co=_1g#vh-p_z(|ZlIiXpd_G21{;_4eEbOYjnYfdJgt(nyL z9Uctd4BRWvwy9sDHW?5E)dL6aIMh{@IA1}%Ria1}_&41^n|_7fPig4~bnVNG>Q#qbYXZt1vML zCy2_;{w-nk$tI-`{X)^I`ti}rR!5MV`A@q?hFj;8-q`_1)N$5tp!SJEQ zZn5zhh|SHn0W4dB?^cu2wHkn#9rRclO&COK&ukG%0ZdpZFinq>1ZI2vr^k~D9 z5sS5bXA`bxK()@%6_?Ir0nIQONi{J9hK&5IbNtw4wm~M9`UK`mQ@Q@FvaVU5_)EtK zJTr1)F+qS4EFq5_|M7Q14#2m>M(%hfl~xt~wgM)RL#6V<=X%^`8stQ$o6b0#wmGD4 z;-AR>xn;iAIcxVP?X0vdp{GZT-cSqIQ#J>u!!%y@N6^S|KK)3pCpgng^4(ob_|@3 z`4D<4Hj1SFRWoih4`$eF3=E@z9kp|2Ts{gW-3x(n@hVnTQTq}ckUO;v4;mT3b@lWX zMELoq3H8#n)%tU+2 z6Xe9=(}ek8Nbb22JIsNUfu3D8#Xln6={YY{PLpetmbcyL?|hE~dt3m|2BqKKd6UJ@ z3%+xxDQ6~wP91QcKZLlAp45{u1Tweqm9)k+6VaWJVk>huWNXfrig3;D*H>|qRD5|s zb`-vGik;HkZ`)VRcHMg-6nXpkBg{_~TE`zT2$HDVOyE5VC1Zl~Y-$}h(qqhU}jocoFjyn{ues z-hgILC8W_;r)f&ibgdh+4V-@CeP5KHp_I<65OPRghdboqgxeCe-JZ~FbX?F*;eMAk z1Juyv!jlN&(0X{mgio9+y+9VNn83L?85w6^ou>Xp(etO_E2m@FAz3K&pBpqB7%Z?w1FSE&w`c~zQYeIsCu9aLrMTRX-~QJ)e=l^Ily|0=)kv% zz!qELr*Mj!Vg7sFKp&KaU{6>N7+a#%CuTSTG#mT8M0)HUV#Zvpl zvHSFiZr(m)#(d9B8v>weS@OBmPcJB!V;!6cHzUb*&VvR&fi9XZ;iiHc)4Z|(!CALP z702`pC_wB!^Do{E(@OmYD1(n5IL}B>_9?5(&{~SXQEgPM4<82EOxOrG%)F^x7uGAf znoYjLeR*W&M`XDaXP%Hkjl`1qw{CnQ&c$i_@ejy-IB5gftcsp6jnyl*&piMhKjKb$ z>ub@nh*SiAv5cn6rOG_3Mi#*)J|6X}moawx*RjY#^;QsgkW164MM>!<6R!ueF6rEe(6Esxy2e(#xJw z80`6JZ$$C8$9g$x$&h+CaWzXwV=duOePGl`E$x!;HanXh{JIsUmL%7mm*XRZz4qpX(g%OFb=ujIQ<^5s1 zt2+91V($QVTRmCdy$Gh2K}*KkJq zMq~n+qZ|8%bpsw$ieglWtlyFnOFyswPGtX6c67eyAZ;1c-YeDc@PRI8qxt~JVusgr zpUZh`=;;31yZXUzMy=gpUAu^F6x?m1ryUV4KS+@mX~vbE%t@UpEBoy?Y5_r?5C)v0 z8f9LV@wmJfi8QmVO(dAHq-FepjQdlwY+)L5ITuIY+-g2L!APcA zRp&C9ypmrH$hI)%qly|&JJ>Fh)9?9REZJjAygu@uKQDBZDw59Qh<>RFPawFi* zD9k^;Gb~!Vn9%iH91ZqfQnZXDT;ebjV?l}kv<}j~Ul}D-@f=uff9e5EGW%$M3gpMC zxzuACg)-Sa&p&n)6%t?(VO%pq(Y+mYNcNfNRt>O$a|Z%@Mr6w!IS+9W&162`qpF$& zUy12X+i@Ru^}E+5kNT-}T5^MQs0TxtDZxl+7PLptVp)#O7h_jZOlO4Uv#QSKr;geb zL~mtUm}&Hm&kJaFa+8NGun~~3Eo*)OE9}LJiNywaa0U^3KFv>PQ(ry%H0Ao-uQ!Lp z@$(|WL!nbF6m`T2oH-2cd9XkD$7dY>6|>}8o$O2>3c$*X&|1QFLO5%{n%PlhV0AniFmB>DWj^{wZ3u$bs%RuUB74SjB7(&P zLko}VdFDW1n?7b49Kf3q4f5b<&P-!!o@6?$13sYa`h{EGs7Qyupo->%z@%b*H0Ugu z&XU3Vp+b9<20%{($f_ewM=+;OpU=-&zR@qkvUxa-_NncHXQ$#nVQ-f8cDbiZ;k3)C z24dOBEg7do8+`A>$3e%a=h8fBv?UEA*`3C@%nJg*)i4o0O`_yApBsJp_MAw;%Nd=s zO$nHd)RJa1Zhg5dFHm*Mb62!A&G&KP$n$=6t6{&HC;m%k9Z7~7uN}TEim^Tp>KY4u z{1X`;8ux6rydO~*($aYTK~8oPC61d<(}?OUjSmX~IgvGd&_@QGzSYfi_P@O5N0G=0 z6u)w63I8%M9wTvFzs!P-vMCO?8Gjx7!HOs__S(!0d`wtW!zYLn``I;F_2s3k&i8<> zg|Nj;R8=(_KDaz#B4f))$ds4Yo1gF%?>FQ|jrpHbK6%oEB}#RcEulyo%_L^mq^7qx z4Xg~3-O{a#dyTa@Y#0*#w@8A6;o;#^Mxd$(sA81~@JAtW@pzrRo{|3(+6HH@d)jE9 z)vvrY9RO^<5#TgG*#?~Sx;}qcvc^-E2d~u(`Ass5whk;+*Zb1JOdu(MYROy#inJR| zdi;YM7-K=>^R22l4gn%t!dX&ME(3d_D{VQ&(S7Wjm%GX{sxt);Uzq?+v3=}Wi#Db& zvb>z^McxlFnSsSpy!s=ae&XD9jjCHTWg6+RdEOP5{AIO@?rT#;{7GX3pkII`?)5)q zW{v?m;bV$MrOIY+qE`?$THctJy>jLFhkN~cKYDyQ9{-hrMCJYjX65U`>{sPNpt~&k z=PjqQQKcJPnU;bYhW7*#4OJ^%a0&nGM-_F`4J2qR4Gi(U36$yA&DiwI$g@3}cY~j+_RG|%YWj>iIS&lYw zG*)VSrv*kD7)|Y4Yb>gc$mOj*FQKVbY4zQ34m_HaUX8TihiKoIm5c1#lr%n9WR~)u z7xYe*)-DYy;>6E8YY4!Zo|pc_{{vCtgKaz|m1e2u2RTHWg?h&86<0J(zcXM~Af3-n z#hG`MC$PU2L5Uf!BNQRI_QNi_u2>U8!#d5W{7xFi0o48>%Uyma@0DI9ZKQ5b3}~yD zDD?`g(j5>@Cep0YbJJ-NFf5@e}m95t#M*299k? zkBLL)!2={EBv;W&^`HHUI+abCcHz*5^1uYqz|aVLYO4uF(I?bd?XRSb4V4LW9z>_! z1W-z22tDdqBd!abXHnDhw=|(|2UT+0Hoah}@e>IjK8>A&4fio5a<y<69CUcew6ltc6gy z1rVuFv!1kjx_1PiC8IGYGFcO@PFO0TYkNaN0nbuAZF+~+^I}XsaL9k$JNKulCpJKF zmWu37yDy`WMReM0=GMDq)>GwbyJIbLjYNPl_}%ZKlG+$B?OnNVC;cM}MPS)MHn_U_ zu?cR3eaw2_W^g{uh8eTlGY0R@)$JwRhbJEhZgm*7Iq*G;j;^p=&ZH>EAlr4b_;T&b zzG`4er9_#{37NFryse(-)Q?-C|0L|M)%(29A(SmdyTQp!7EXFW$OTmVtRm~=J)(F& zvMRFjBhb0x=VHtEaC+D@l4xnIb-y0 z4J~P+VoCojo+-()9*sE?gZcf#%-WbeB8;YZ89t`{x+qY?}rJOJQA+8!6X)*&aw4!H(u{51uvqOJKEYr?e6pi;P?kT z+vohS#qO(S?CGb?^*c9pJqwb}Ss&F}gtJJ3vJ^dtG9+3H54b%Q@m=dJx{G46)6>1E zH$&#NVY|TGvM|ned(^zUFH7HI9Vih&qDN0x%1g^cBkgXlqOE-AM{Xb*b&bw@er>8F z_U#AIuL|0r2mng#ZMmv=@Oba4^e@9M(MpVUR~Db@_JBIV&N{GSD59%DU1E_+?MQh- zw|&nL^y$cCF_}Z(2ACt)3{F(ovPSS)r#o_de<+Q2_~?(xXTEW;ABkel2f7p_I8VG$ zz5rZgl+Ypf%jE12^Jm7rj{k}&Q(1Gjwr1zwbX4boEdN>#iQZUDJ^&5Jg&Cj!m8zPh+Liy zD0~G)BK#>bKr-(gPTBjt(eY7d{3yss0n?7!ue;3l`vu{ksxnqIB%1{aL7*j1YwQ+p zC~hp8&^-F<7S9$gzBuA85n@iI;DM1`ErMFB(}PGe1_kyB&V%nxh3n~q8?#w)VJ=-o z7Na2MY*TEx>t`B&@4?=ozEnUlSl2U)hBS*XhL{0n^&8Ps(COIxza6zY%R{3XS<{q& zH)I};NVD3oh9+SzZla@L!BL|f6n{>^^YtEy^v z1Pca_Y}^seso07Mca)*vm$e{==eDj}%}u=eN;4l*R94PCq6*)+w2NY4 zW%U+D&|WM{=^|UPm08m&0+iAhj5LWVPr;D>DF4s&>&_JR(FH1Baw_tpmpS;Nf41Fn zr15qboj%$Y3rdcZkuixFD%s>1c-vHKq}`x<$`94k)-!}H zGweGnlO{#KhY}QGO8)dOXs>FGycdk!kS<>T>Fz1&yLvaL5#iDPIl8S4)v|dFNqjjv ze;B<&MqCJ`lg;y&ew~;OTH|l>^X$A5w%;2qj=unf$|) z{s={#;azDqqE@vM-)e`F340P74vAzUqw%f%DEgK5M7wEE7hNOAvHbdZ;A_I<7`&@4cm$VUn~qG!I=QSm7UZtDbB@rYF1O3$wuzbP$ADStsc z(#c*D$)dB~y;S)oxhzEzDLPeU3@tnY@QW*MH{_q#BjA4?_(+$!Xqv^As&5Rkpzy-+ z+g#nSgV3%o%M&KU#tG)uQ{`Ufuc7=F52a>943rZtLn-cRRVr~hsAEAA`VjyqlGy|@ zPuiYeqU*7nJ`{4(r2eu4gZRfwKwIJD2ZO6RfDambWY#&OPS-RmSfYzt>(d|50D}SY ztbJ<7H~d+9KC?+&2 zbJ-!T=y!jBxIdyju2v8b!v$Cn>OAZp^TY+HQxj9%Ed}kn7&KU!mJ4 z+S1jVk@(xvrpnla`pmBVj3kJCfnZNuNM4`+LvV5>NLXTZc)GNynYL$uqa43oR!fY_ z)5Of74lI2bWKOlzbwr%Qm8~yzrL56J5sP)CdQ*Lz0jgS{1R}0ZDeMX)7Xa50o%r2| ztfY`7U<^@^e7{8+*`mA>9`G(f&`Ex<2SZKa1$M|SO4Ykghhx-WNPNFD{~(68bBX~% zlrvJ5^H;yKNUo^%n`cso`QyY_!dWfbS;`~B3H-_b_5xtk5vsmM9SfA`|A?VHyU>s* z)D^hDs3aS$+!Qi?2I4%YS^UjL;eA5fiwSEAG!hJ&vzd+v?>^c-1t9}dl&Brq3JjDG zxZ6_7Ym-0T8_)kd*`To?KJ&gsTv@_suWWG>;Lkdrs_@S|mCXyxt#DsP0l(HZsh*C~ zQromB(22r_GqslA%^3)Ob~oZ_^)0HQqq1r6a+2xHSVTw~ueICsM+|}iwL;=^+TsYn zdDq+8KXot<62JsaB0ntV=hyZN&{@ zDcL~0yAi>O(q(_pjL#?t3i>|;P@e>{j8yPlVozfBb<@&DWmg763-}N(!TJF1 z6|Tq)4d*}7z7qOxP~+*fEisddEjW6dKe4Nb52bL>aFSzU{!?qJ1tF;7VlK5f^*_~7 zKzn1Z)Fm!zp#6312Dwj7d<*;mapl8G<=-gCa?ULbS`c7qxh#!GvQ1EA1C89VLlNyLa#!3RcPr>SN9K{E`dUTxY+FPUn2NN zyheO#hZV93ha4@15e!B|QJ`50D$?C#VMAt?&apYvD>Uu=i1Xx8U`4gY$`8WbfWLQN zEv0`8L*vcM_D2|Q?;eX2n6asus-5FdVTwYJ>KC544P}L_4Rx zXUg%kQAPS@=X&p<5hNo8-CP1YIe{6D>rncd+OaXUZPX-L@6%!a5yUm0{r#59CEoJ3 z)(!54r4M^-+uZ~zE_Z{|1kao!g>`z7brH~=x}M%X;u1M@Gc%&t1!h`!hNCN}9!trL zFp_=KgtuIOjD(IDVI*sJADP-V*{X4o2{`1Oc4D!A z|K$vNNN)QZm*!GKqtf{`KFS(-mLXAIfI<> zXe*r}35U+?GRyD5bDG;I+vmbD%j>Y=-;F8fmy!rs?V((pUkm~l(#-2%d46p8XD2p=+#W2Ib5w2xd{~5hpECJ&YDq;ReAp$ zsg*q9?k^98wyVN#!yJp0SdDqM&AoRGnXV|MaCdPU6?$IWq@%69v$4HB{VBqRcDu21 zdvo(`F}%1i%PAO}WbJNS9PSti{Hf;CM?4HN;_8lTFrc2S8q+`&!^EFRwqX@*OF!me zur}fdl2ZqYri!({Gb{g|naarZA5dT{2uT;yK+4eW;%59GAH_+y=<>_m_Qr8Ua9d!! zP^DrDq?+DX@|*xsL+j6)Hf13)&M~X;jIn9MiuRD7`|?Sc3t2WI^wEEg(+Tl60n`mp zsj)w8G}6x`njux)Sl_#wGMqPJl`s4sg=>KTx-^vt`d!ek@<7iu3vdoV^q}12kT#8s z2|8ztF{`t1ojCBb_)Qe$;;@Ik`@_r0(IX7(^O)sp&ELA*XN0^@cPt=`k)dXcEpTnh z=ykampVT)~1Y^n z)B!=rZSE^C+XTbgnSjy5eDg!h?CkD`je9S)zpqC*v%Z7d)-P^BF}2%#eWYJ>1>-o6 zh+gVlzGJ=Kzd^L7Eg*$DtMar#(R?-s5)b1-Z0lyBzn0tDp6lA#*(JIm;H*xw3(WMp zqn7$-RclII6N9%XM83Up_y`Gr}-_=_{-<{4>xkZl637HM?|W>8W5LjSLjqjS63&?EF3MDucyj%wZfT= z98r~pe$myZYQydk2T;!0X@cp|j}3Sjy*+HII34016;Mj!DW-F?jR1V98I{V7Oi)a6 z-J5Di?sPZ1T82Mt+g)Ftj*82&&KIjQZd)aoavOatoHp6)CmJDB13 zM}ERsM67Zjz!KM5hJrmdoWB&*XALS1$9x6p5S5Ief2+@}U1TV?Kw~%FIc36!Q_bg> z+b0o#JEG;cn*WErul%d3>!Kx&2apbt=76MhBY6}M>F(|>={|r+my|RTf`FuShjdGK zcXx9)kMH~5`zPEF&o_T^_TFo)J=dIbjXB5Is@%-{{GRyD^rT+yx;b-Y5|Pjq6J)?= zu^VTO4~$U^14<4q0@`}r zuh;{Q`pyqH>|Z)GY2?$)T7)03h#WcWNj$c`F$XEh369s^U!eCbMc_6k7W=it-KW^r^=wc4Bp!SPKZ(2A%TVI< z!hKd|8R&E>HpaW&uU?!ZB?wmm*tm1$3z29UUMC?OmSc2g2XnQ>n*o)vdq8(#IHj0d zup0`svF)Fc>`RHU#v%_X1~Kk-m=U5Gw`3zAN8`*pl26e|KEivGwunkKFuE)WiD2CP|Ga60aP1 zmhcFUyXSmSW1;)f{2wUZk z1Z4`C8jQFoVY8Gnz3ajl|8a;ML2pH4-=$bbHeE3saaI~=EAw-m25O$+&%{U?k+=A0 zRc=_`aD)Milf<>KWAhwqNp21ML4T0*l06*$Me8UIJpg`(qLjERkvCGa-s}xQ7z|KYau5;> z?mJI43+)f#n%Q86JciQ2cZl(l@>EtcI6&C22~s7MQbD*2>E9eOK_z<^+4@EMnx6k{ z+7~v+TZoEGHa4qK3&~vV@v1E+VSyDdnGwt#@eXM3!A3mRxaU5#l>!a&?J~Ne*9!xr zzn0yU-~3EQa5>M~4iiHz8>M6$|VIwc}AAT-ouPGno1jFvcPAU4kJimXih-&TC!T#c#Soz=S=`InvjCBv5&GL^Yr0 z%M_%NCJ9DRPe3|CDr57-!t7wc+#RcGvl(X`#Sb^dE$U%dWzvfE0@|NHC7jR@`~74C zp_Q8;)Z`&?FYr!x6h_mM8A0n^_EV#Tt8#zD#PU?wz=N2gGlc;TX^ZJR6Et(*p4Iok zt83yg<+ee1Jdv$MX@zIrNy*h6dWC_|S)|u|wYqBaYvlbP5FnRBA6k*fc>%xl>vjQ+ zFkOLS6xl627HC1IN@$mIV++4K^i9iP%b}zG3>aj{@>j{qQjn!y_^;yi=;K91F`*qy zPRU2)aQLdgO*w%Qjh44O*WvJeZ<-}upX-&Il0ErQyZ-T2Fl9?dE5ZYn>XCS{Lj^I09)5yuM-M~e^`e%4d-2gAr^#}**tSw38AgqWI{G_YY03- zVAA}Re}s0FSXo86&$$#Y7yt8FAKL`pqGw6-tX)M4RK;H6)+R=uGMWU$3MT12>?x!{ z=ZCkBYCTFZ|8ksaHv0@?^@crtddB10s~+X9<0^0F|^9Avr zA|2DK_$rDRwXDXKd5?)J*?tfV{{C7FVuDhd(t>(tLAvS;c|y>Onjg3t|UrJ-1=DRt3>i9{aVCBp+V>ofs4x4 zVe@~OqA0Yi1mzI&q zM2J4Q;ej0oL2UY#|D8+`IeSOjgx-=fB#7y-d|HxOL#coW(OT*)>T~nmJs`o`53V@C zFFpJgL?&6o)}lqGe{fyWbYmI64!@v|yF9-=b1t{}Lw)z*)jaW|5pk3E<@{tL9>W66 zH>}fG52#(KhElUMsgLNyMSD(b9%UKd+kRli{-BBwMCvlt=>}!uxK^jJr|bizhtMz# zdEnN%82|bT4?w@WbW+U1fVnvd2SX81&VVLWVy*u0++N{qr9kQj0@YRaDuo=YxcSI( zJ;$Hn!kOH6@M3f1z5cV&hwK8FH_@)Bku)UD@|O%GMs$}V2=zGyq7VyYeYDcx{&oSs zdz0+d1r*abTo1HewS;EbAd2N&m)z~?ABNx_Phjf& zjBY1W7-;x?EkL~RnV?FdZS9R`cm*~++c{>T{orB*rC-3#wT@Ab@o(J)(z#+1hjJQN zoEnJzE8IewqkHE}m|20iyD9%Goaa?!HoX-yl*LK2V>11VcYS?%CJ2OHr#bqQK+{X> z+t}_NDVQ+K;La~K;L}guZ4@GdUH7$=kUaNiUtOW)-vKQO0?eUC@8Qh1gG;Re zuP8%lGWNCg4^FFe7yK^+X`8>K(iy>g-Jv=9Au)VFSM02T-=fTBSr?h3D|s-_G+*Mhwi+_tO31)dFI@-D}V6HYi z3olPY_RyDi6EuNI$YTcwKu4BZ#T_fuuHI=iz=aV<7yST=u|TJj{X(nrT-H_;G0&iL z7*Dk;KcCCq7G)SshCAX@V6{yTW3KBa1P-u&8r&Vbs!ly0t~cjf{8dYA8WaCnAs8Vf zncGHlzcd*MRN*)XDD!NWqK2JD`QEjk!Otsa^jYCdRX60r=8Ft$Nr>w28>HiE> zd)05;ppU|~;rM-*06HVqw{h1Y!AstXuNKuFOmgMKh@s@}9rWV1EYEuTZa1R{IdV0F zdjYLX`9QeljOpEppPoUe8|$^H5($N@&!wr(pK?5d}yW z%0EPbBcd`9Q%^EG$kG4}`Dn8&SUAz;Zu`v8^l|-YP;rwXb+nNBipAU2yG$^mBq zR~|SiZcp1o7USDmtK#d^TCQZT?{~?H`!>JL+-+XM^V@9?i(oo414#;x9A!AX@ZC{> zdY%6v1k+}__|nY4-S>{>UuMytKnHcDrC+Pwx}@)gGQIWHi?)F z#(tIhQrE3@J`ge;0Ut=fF?Cy(MSh)|n}%T2^^g$0hzh{)KcKM1>We#W>9uM|R-S1- z<|?bUF0Vn`CwAYb3P~V#Like%b7BdG3S#B|V1wP^ea}{wnp)R0P`3y@y3@g&`ALUm z4PaO_i9cI;2!-y?lqRwCIX0@STMQA@L#Y>u@TBS^6-G2_?7!{G+G!n;0(IEp6PxEw ziOf2wfFEo%*!?LDlvpUaI+3fC>_c7bfyG-GSEN{=+H9I%LG0Lw1 zyfN*lpr=DmozL*uh)hCI5SlpNON7M>T4J^0~gm+_O79(lN0!e^8fQ ziQ1Atgb`cK0s=|(F}AO$XLPY|+Uv+BxxR4awc$x|U)j)gj*lJxF7x~Y z3$_@f4CD`TW&}W9z3rX5je%LvXY>ka`G1+>Sh0ZXt9vV&NrpVuLC})?Yu@4h5m~G` z7!F2UHZY!{Q0IkW)Jjc&+WFBE{kcz{I%Vvn3&~XM%^IORrcvQ*;*6HM)_{ynvXUt! z)*z_MG!og=mA?c6wz)n+E|8eyDsfvAwcsS9bf8{oA%=b1_z$-Hq=-h(XOF{Qivm0s zb|QrQyEDsr;QdHcjRN<1(#mPWc`_4-zcdy$MEeUT3`%F(@;+6iAGX#cL#4w6^rEn@ z9pe3*5)lk*aj6vzRKxL;ekJd9*eH8_cTHTUqwAyE`ju^!BO>7DFZEBJAAo?yB2y$o zpwb9*SJl}|dV_m+YBlF-qC!#1$m{dpoo_l77d(NkhtLmGQr)pqX=X~BuVQv~03Akn z0@S(6tdRr~^DR+;W(7jRT*zU?Dh(d=rK$4kqqc>r24VbI;Ob#PaKNQ|JXg#6N=kl5 zFHCC|+j6wrw^}Sp_?ME!o(#;IQ1EWY%NrZo+U#Fvx2pa!^r4wqQR}G-Ru@Rep95U~ z8(*w+c!dBVh0Th!G6FbZ{1-3w*`7GC4}8;LhCGoV41D!{I5e=ZKI;|gVWsV_Ca}gi z_v;+SW=#qN^GRY!xR{nnwT|8<4C=SI) z?U1!aa08Qk@)z#P5oIIS17M6AlfHz)rxVOi)4|m1?7W=I-AOyU;^v{vb3k}tK3MQq zSoV2%Lt4`QqrZoi!iG{LgX71K3z~IK7WAG*hppEsyco+~(UU?1_@*>G)DpA^m9+A_ z=EHja8X9^EA_;0z2h(Q!8hf54R0!L$nRj6oQ1724Vxxke$BX<6j5JzbbjqJhjH(5wwn^5$QPTU<3-=I%rATqW#6z0pH zU}SKY0Wz;%&0i}O&7=YLWj+ei`U^iItSx{%b80$}JTDq!q%dm3-=ad2QDy{X35U;B zebIX_9e0_o-Aq*dAbBeyW)(V*G^5x_cEgyzG|@1$e*SXDEsz?;C{H@+LBM}))`ba$jaiGd;8UCUlMgs%ozGvUe5^FU(OS+ zm@BJ=6#s`Y2?q>q*am_SA=)x=RSl5yse8RR<{s;1GKB6M-{Xi4ghG39=tuUr|0jwvPHuq*ufA0Z-i_2jR8X?`vxi2+Nx2Wr(jl9h5!T&g;?(0o>Pftd`q8 zdiOQ#ygLTecx=hmrNis#=@jt$aP?ROo#^1du2teakR(tMV}-=N0oh+RV*ruIy(MK3 z$L|$;-sa8^WU2%>epKz&jHLYqg_z{Ct!2*bafUMVAKchLtt9tP9)E7h^k+67EvWqm z08kR=$x^q}{M)7$_(Xzi3!oiQN`X5@&_xw{Y$h>k=^i_X$a(44`3j4KyQt@e%W7fc z_E)uDXlksSOS$V}<1t97k1`s9U_$P@7bkFS>}F%P$z$guuRq0VLy-a*Ecjc#i~zQ8 z68FlEog!8X0|fK8$qR9zba+n#v@2G6P%IW@bQZ`z0LiZH^^V-NtVZdeFmC1P;1m=GeB9!`g3kG(ICJM&JF0v`KV7-p$iU5cK4SNRVk*iZ9GELU|(`7g~B zG7S_ONb9sT+^;>YdA_PqXub7|b=}UD&6G(o##K8BhE{_78B}@2jJi}Y2nf)Mhk6GO zl6ee2vA97iRptj8MLEm0m`9c@o-X7C2gk>KSfjJ0I=F}chTSZr_#EW?31uD zE}gT$`y}z>9l`7kE-F0~pr~UfO%?Mu6atkM48o7ZauRCF?8v`t_t#P#BV)&lbx18$ z6|l_-5Z0v~H#18mN2Zu_;-<=jA{dcp@&0Vq~Taz*JcWV&5s`EvBvXXWSTuNIaxX}$?Yez{IKyyObS?|&38Oe07vtVIgqsR5x_18uRO zHf5E+%iALc=`QNMVX7kN%g~8;4uP*C=@;B(q#Z8O_=v(}!5#{=-`C8WT0y*1bpD7! zzUBGc=iz#^1yHsod?uD=n3!T zw=0@)Y!C-VmDs;~>I;s#u=#KjBcWSxb~ytaKN{zoGx@xphg*KxSQ?4fjUAFw2-MWF z+gf&Sasi4kdS~4ca{_yshwW1m^{4!BM|l)CpT!8~Od__Us4JaRK7GG0|GnuP)?tK( z{LI0zdLrjenC|f~2T4;3-oQk)ZIC3<08Kw*q@c$PjWL){cKJVFx zb{{>}V|R+sogk8-V!h^vN`M2c)p02q^6@tI&`_4Fd$)6~^5fz0wQU?;yrYW!stv8fF$ywQ191q*=bc66p)NqkxviE ze;oL5EeLd$llB~Q^J8k;)MG@uIvT4F-O9Zo6Fs2Ksx)ip?d^T&bY_^0&qfS-X0H8@ zG&A;_$7=KS+Lx$6dC5^|GODu4@mHoy?EFDj5`YNQBW`q#b_#FUBCs})*FL_T;5ysX zUvrt1Qy6rS}`v-qS-O1&L&3^(faMw+EIJj zUa}rvU^Y)Z_%1b5RYm3=r?j%2Wwaxv z$+Xw~@bQ@LJ@%XzAXAjCxM`X@*DNpaIS|i{|Ap>>3tl)w`|nFU;obwO>0|8@9IEkN z`+H)%QtwyvjdbkZbhilNJ|F>_pr5kXb1(D_3uw6(Nci4jsuHo_l-;z-y+SY%iC#6yMvwCu{A=q3ftAOC z_}qD!Mi(Q1Y3KP?kjEa6hGcUBHjJF#~lw~Jt%RblS;oP~t ziH?|&MJ~`-P5?8L;A6#M;6VAO>zn({Q`h&*p}A>fv_~2S$Ujj>RsL(dGog2_f1U`c zqzV_8-GT8F8L07(tZagfSa;PYNlJMm1Zzz7hy7~V>6d!ECVI=`(m7Q%cdGoOK=&|&_cF52?UAvfxi4wNChViJWZl4*glsyrlgmy9GfA>d zam52>(=J~@psK^qhARMi*6x!beJp_Z`&7YKBV(mHb>)pVapx`--hfGMZEecwbw*q@ zp{7(eD;?T-BIeI&o|m`yB+VbS`=zh@67t+nH#|o-&;d#}UziMG5vCE`J-Kv-xW=Qz z{`RV(TqjVdq08`Wan%hTiHWO*mf2<<2&_GPH9`{dk@02zrdI)AEnWJ+i4No2{OudN z_mL&ME_v25@kaes{*41GDSpekc#9)+O~Oigjyp5S*({rw(6@V=YFOUs@EapW>3Hou zw^aMdJbnYkDgL%bmP3vlgi$rsNaqeWex7t$SvKXj2PmfktWv8lehJ6=lrS?g&JpE$ zunwe z7xY_FQL|}issY-6kstjiO)EXvT-Zm#?Ir14onBev7`3O4plok7V=y zCh!Wl*likhAAR4-4o3Jbw-<_{yj)+Sfqi7hKp9$h!!Xf@3XCR~hqf8m_NQc8&jo%l zwta}lk?aiPZtp+OP!Os{Q4+GLee3eUfDaUCA?xP8mfZR#?A_z5kF^!6x+}?ISJg?6 zhHFz?0#{^O)9Wh=`cldlrR*Wx;NfbFvwe{QZk~fTXU+9`O}ydo@F&t}^aiL3qSgLU zghq2~N|}>cOZ!+tu>`D9T>P^{Jw*l)-Q(U`Rr8vd^xZV=o0MX{|q0}>Zr1wBfS=mg0yFA^GDRFmT1?O zuL70DdLc5xciz7=4k_YvK9P{N-?%WHFBt1oOuIBEiley~GUDoM-#7{9PlsGRDa zs){<|s`rwn2!SF&w(TOVHg`W}(LS7qWCm2FLWaLb#F~^Wv~IR^?tP_Z@!ui*{xP!c z9c_(aATBV-6}sxnZ;sgh@b7o`D`YLUUpzDF8k933Nn+&hZBh5(kxqI<$aTVORwRl* zHF&2Iyx$y5;Th82 znP1cTqi2#ZnYbysAZ(I>3-n0+Lpr~Xs3f!ulhdyltHN&%cKlA@yJWULt9gWOnlNvJ zXrO;1Db=eX{W;9N^5?UG-V2_%(wA+$z81RhW5Qses3_L@GX6Q(Y`+=Ln4kju~&xM-BF-@QsGp)0;2vbycbz7Yecw1|tb zn=k@c2)oPH_%RhkUck*>?YqjsdXz&36_z+<4vSxP(oG$e>zVoFfCjxYN+ueKdBrSu zU;i!=$t3%qt-3jJskqt{tE%yBS~|k-bE*|kIcTRZdv$}&aLcb492lZb5 z5a{h+4qof^qikgB{Pg02EYRK&Plt!>*?Btj+U!+4CKI*&WnIxvw#;M&ozEnB?Y$F8 zYLX8&h}q+Q(#`g0XC?EP=XSU|&WR+SO7<@&*H5?dk5ZpR^a>jq1eC1Hw)pVxjy)o~ z8caYV#z4?x3z!)x*_1)aOLrx_46VE_<5j4x{|Wgh@LN5NL47oe%6WU4x77(xZA-Jw|g3fo6dh;xg=cOu#aa zx|olb;Ze$Sx*bKD6d|r{FHE4j6qb`3JUBdcrZA>&2i|SemghsIh1;MyTDPunYx&o1%Ex{*_(GlrsPiJ z;!5mfMgAFElmC%xdPZu|uE?v?s4fTO00 z5+}!JaWy)jx?2;aBL3SYw8|o#3i(X3B@!v_t5cpROe>|b&t<#e)Y_3vQ5I$D;N0V* zhri(O$;aSt_}|fO&rb1}$a!b^owWnPgU+sHZ+wy#806GFrFvZp!2ZIgXwcVke&;tI z<+?J?DZzU`b`Q3X4%=T}E(%U3WW0^SZ;)@&qhwwObZi>)@_G(?6ZQuet#&Mi;Iwv2 z{Ob0(fcj|3!1F5w=eIp>whJiEz=o^>s+z)rLFqn;5b(q4C@p3wDTrkcST5W#Ua^pSKW;u4hB}Ks?SG3=-OVlopUV#`FYRDz;VH9 zq!#ycA4z#ESV#Y`ISJOSBoPjivt>G(!n~#wcRTkbya%X+6Y1or@=(q?Ypc;gg2Yu! z!`mq2#X{dpjP|czsWx5tNPA`M*riz}-oejA_!fOaDwLYdZuydiRoa+#x0JApjp$PX zzx>jpJkKlkeEt)k890^2lZO4gM)=e8DTh|a$+*YNPfwQ|^g9{k=(H}XPhMpn_@7*d z^{By43v%a27pxT?H)*=Q)qkk_#ji(JeZbDa@KubaHNAowmo4rKe8>H6*9mIIg~dGU z9Lo}BXqOF6t@9kBE(fX_RR(4>xQ0-gLiD^-NjNr0373>M77Pvqk;g;ej*f%Vm-Cm~ z4ZcPtqI+mET2g)E2Sp6tsdR&dScjGqS=)6_Yo?C4fbzKimt92390A9!YR>PouOJ)~^6__6N@&6-?+ z^l(gRy4N+fsbb){=fGy;LIuq|;q+WqV)?uvqQ{(g*6Koq38qV^*e0Lb?+bMF4u(D% z&QpVVO=8*tSq$Yp9!;_mf~EO@cY4#Nk$>(>&spnrCY2+Pch!X|qP#q{N|-oLv&+rI zUSPUn2HNJy*Ie)Miq5}6T`$>R9myuhyldP~(Wh1IKm1BRVkGq2A-=b4o%qj-uFboS z^iF|bc#EPJUauM9J78_9f_@@!2v{)aAhLO>ev0Uf#}+ErSN_(vKTEq(L|)VH%@erC zA#E1~M``}S@TQ`ZYTWPt6qd(&GPSGxX;uO@%$2ahVHK!#l$O)HXwPqn=KA4_&jNH& zhhf9z^*cI=fOdK!l1Q~$UzOTf_q|%Bg~WVawGwBv`AGf)Ubl{5Y)7X7$+`za9XqRm zTj|i;j|Bn6?sAh~;S?RG12!!#y?f369M)4akxsu`ui>EPbM2n26qYxg4gTnN5VTxb ztg>fT+m@h)wv~^WLVXP1=rMm+QV>~3$~09*xLna|CPhaU&4MqU=(fHqcQ##p?xC@0 zr{1Tgb&}~(nhh`0y<=kvjjCX3Af~w}!_KuSsHxZ+6QKMx^juZ~+yRSI2H8SekRf1u za_G}C!GYLCGQWAWC~|F;oi6bF*_B4uwH{t~LPOK5ej5eGzTB;})8n5|i=RFeL@Xk4 zC9Oke9pFJHW5`2wQh68ub+ z<-{BKYF6G*{g25yJf6$1&CFfh?s*M;gAxUsr-l3O;JJ&l`&EydhkWu3W5-wMZF+m% zv)T4**ujh&`!6bF91g!IPmn85n4RC(&vY4tGiYv|I^4{;oVzxp$ke^GGHPY(ef)J2 z{%fe3TZPSzWu9NW#(|js#TMk-laA2;I%EX%mh(J^Fhtj~N z>f4qSqPR`n>#`K@sUQOR38-)0PTlbRcs{{l8N1Ux|LNus`RP`66!Q-SJ@k`HQg0#Y z5~H;~6Rs2El~)}wX=Pkl{6IKEsDfoOF9jStG8D24;!9V?7==6ZKqn#F=2;pcWN{+i?olx*;M_y(z*}y&<4~{0-r)9Vxt(XyY~%8we9_Q-lm<+IDtJ%I zV9Miqbem3~v%)@#6J*NdP|C4lqj~?aktXc1((p$3x1rqReh$nAZ;@ifyVw&ir}tMQ znf1UUSMO~mxQ}Lv*K@C|%aZTok<`tIDHv_|mKXi*d+mjQA#9pR-(<&mJjJf*dL~~X z`~7Z(-FBUl^-P^lmBsPxxWi%!s}bU0yz<8K$@z}vq=zYZDg>Qd?1AdH{VdRSwn!%E zaaO0Ace7VW+E6FJG}(Bi;C(4AURxcuTg~Lc1W!Pja!VlWV5OK|$tYJzFxzn}lQRasHID?s{g@@L+V^+pg1 z4-4IptFvVnZu!V-Ev=n^d#t*8&=On(#HCSCEncb%p>@nHv zqJ-Xl;dE{8ZHA~n>n^0y2h#QxBxY;MZk-DPmew@ovz`R0C(>LNxu@W5qfxYG(woea zNacRDI+HDaT#=b`jrH#CNT=Do=?ct;+r>xQMU^jR`c_?Q`}t8W#TrSGr*dqII*1-x z)rb5)?s|(aJah_fx9TgI_iAV*iQ*12;dg8fl@FP~ zgJ8#cHWOD8Y!7)pdbOHpTl&?x3;W&DxS%>}&$i;*np3Lug$_7e3cRk^*H*7yoQ0yF zs8q+_Gw^u{iX77Lj!Bn0hc=bI!o=JYLF1kIgt}fx@@hLVK4r+UnGq*;nUATxBTSkG z*fy%fvYYY1w$ZgpsDb>mZR|jtnRu;`28XqMPzv*q$@1rhQwPPU`33!%U$VH#e=v=(tp69mp zR4+m0()aGKNQJ~3LW3T;y}e;x4-w!Lz2lGNG9+9__n}Sv(iyY*&YyI-^;3Q(%9uQ6 zH`OobWR-2EdlqLA;)+|aHkJrg=aN>H_(#Mp#6|dSRV?;?wn3O)kHZ>jxu9gy<9*wQ z{~+g%G08=|+t|9JD6Dr0e3VLV-=NOD#23E+iGO1_Qo&2)aun%&!DbPzp4NC%uc{~0 zraYflR<-G#|A3x&O8DpGkY}=nzC%H{9m9~qjXUl%2XV>nrPkTn{hsGx<0a|!ai-8> zZUTWmywlNb@zpeB?g1Z6-;BcfxTk-~&od0Xn7&t9vs?Qy7-c)vp|^c1zKB(+O9YKo z3e$yji&`GO(uRGx9`7D$A^!J&T#5PZe z9Na%U>M0VvYdMX(eMy8j6MH@!yGieqXoN1pqYOj1?=RX$4KQV%62eN9K>k`dO-nvj zjymfLsX$?aRHy{4x>LajqPsMyY5sewlMfIKwiZY21w(Y`Wa5^-6zPY12$nKh=^rqk zY(=RFWL{QaD@ZCt&z~UL?ZpxtNEHi;wq*O1T|Jp29KtjND~Ld!YL4sn=2%=a(%zbT zD`%)L(-2ngkSUs^f%A-ew9_wa^reY683lN(D{KxcI1VuA95;HB|Ev)_@~8I@W;T7` zFAGK>gB?tn)nl9uJ`24?h2NE}Yz}Sq-CXU`zKmAOr5(NI| zjr_g8pE5QS?SqQ*lJv-vP2OWbeE$2+pC;8I0t}06P~8v40^GWZH3sE>qo#Tfd(br8 zVk2P(h7|3mNCNW5%5*?^7iINN;C@;d=ox6ML~Muv^%$^*;2;iF$WjP;-vH$-D z7=oSIoIv1#79{%^n|xS7rPf<}!0@6vEG|GPAR zMgF@q|NmLdTdJ3u|Lq0%cXR#gcm8$B|3<5Sqt#Px@o%*H|1Vno8=?M#DcCan zO+?GsKC%PGWyldu0YJ|92xpUqt>G~Qz{$S@ju02?ND9{Zn}z=5Eu{JB1X?l+aAYqb zD6DGR&QajQAn-YGbftS+90aWcMj+*Szm(<+oR%LnVsH^+a5Ei3NZ7!TXb*(@7l@sa zr2ILRmFH4K!(^F|>S3!mpDGuhCS8{8^UbQNDyu_4e#A@>lfo3Kl5>@Z-MuDhJUskc za!eU-Fsj8%M7%@m-#jzo;l5vZ%k!eVjQybBkbyZXJ8$x-cfhpOSXxaYfH_ZCqWMx_ z3Hdz)!+Vr_2Y22JPgp6FlT|Y5HQk9^&N&VdFMFoX<8bkEQ!Kr1e8_4&v>lJxx)rI6 zYPYNgR$T60G=yL&2*(`~tplt@xt6Qj0st?q9WK(GYf$L501f z?Wl&Rs+IS^-?&(OIeF$@xG*_!J9yI%3JBtyx_|fXTkcE|_-FtSb!ZvYlnp)JHN32v zve~8$Mhk&Ye4XCs87jdcfp0<6Q|Mzzg9!>11rF*lmi&ull;E{`pAcpv01;qUHK;-L zLq;BZ1*SXnBg$Erq5$31H#XkGp)cqbtxo{-<{4h#BPa2kOFCG7v$af$;li&wtA4F) zH-y0B1j|lZ2a#`7ogkwjU;~H)KDK&jL>hnz?RB#u`=z4{*VwxPDS^*#I3{$0oVPnt z9^Uc+b?%hawP2Sj{8T(jcqVLKt>0-l)dZP0^J?7WO{d`1+ZowadDsTOm0Gh-*@>b|l!p(Jnnw&HC5N3UZfy8ihs?|oC{LW*-ElS<7p zfPnFkC{dv|@uFG*=SDBl;9^|^{eK}{z?=TbH{D|F!-XG+BF>Th> z+1Y7v<4~_z#&F2rTW|UEuuYvNv*r=ry9iMq-Nm&a~Vq> z(whV3Qm91P%lb4IHL_w62o(bG8{fDdpnf8Sc#SEYA>{4ut3BLeFR0_1r%QbC@ji-k z>M^~^?sCHcX@{ujK@(9;D_vi1#40zB8hMY^X=@nueBIT9K)bnsYe#F*c~ZxY);wDY zP2M^d?~lTX$&1F%(>`c7jY>sZScu$(FQh&g!uFpTC|wcDD39!-p&&H>EDrFQa9`(y zHwB*skxfEd9JWdvUambAj&v=*@P2#?*yzjg4_E-I)>1-{=~cn0t}W7OI}C`q-LusJ zVm0VCmX;ohleXqk=*kNg9`AgE(u13`?~%BNZ>#yi9o)A|w;nh`KPI3$83U7-g|83C z>ud{p-NYt~x%69LtLO9Bq>}>QF8AXOX&N)?-HumYrlh2Z@6t7A^PA#+1^Tj9Kjm1v znSpDBJ}@Q~WzcTDxJ`!#L_nIy`;y9SQiQm-&gJfX$_eIYGHxz9J`rGnAd~p%aQBsM ziwL#w0QQvFRcw>6X3bc&q&fg)Kwd4>|9PI^_B z#VZ>_Sl@^9Um;#8Ig6MtXm{)H#VY7z$4q0QCUmyzAVnq!mKFUE82871R*+~2JTA*i z;EU#%Iyu5WCeM7TKlP`W4yD`NmYgMRm7IqJqY(l{py-&;wgE$6uJrE(X|dP4V_xwL zE6tP?{HbW(vrGSk`K*etj^OBroHrmsgM{&`@*<(r0%l`1yDLkC*OV1Dq0)8r9KEes zp%6yuI_Gc%)bVWa+g^`XAQpgk`18ZN3j5^KE37;Hyo(1f$dY$_^dbZv^8|!PH~U`n zK@Kk+Wtn!I8>a)prJJv7?0)IMr%kKlcMgzle1sck&Titt=XrC0oSfs`98xjCu$pcN55J_j zTTvoBHV5L3fA?h)b>^e1Z^CKfP%_u<&JJX&#H32op&=CT{?-5U{xJ?}zwq=q&|7T( z^d-PYf1$>zBhc@9Zh6!&)>gi~N|fo_ynv)=_lt_MI)jm4SF}raHH|= z<6|N1W!17iwR`%^(AcKcc%8a?k=&gc#Pyu|mVT{UQ z%^!FJ%mr-65KiJ2m#>czU=$HghtBU`7mHelGR|%?zKb#sw;ZL_I&R*0lz(-Le&f7+52kL=q`y=uVT&}5jXVaq|msqnP3rf*Z(M24%2Q(@nipByGuUxa*>5C>xp zF4OZa=F{^%PihRIQR2tf*ocbxRY~whU6DFED+6pR22u>~Ls~!H-w_Yg@vZ{e zVn6!Nwip5{&7gWNS7ZnlRIHX``6D;Pnqn1J)_?wB?oPE|&s^Dw~CHJ3VIgR+4AgM~gx8ULDM$=X?6_Q#6~J`TsT`SqIvB4=}5I-Eqt z-_(rMVU1O~`|0t8FAnP#8h89oO7@@%D7yNwANW<3piLVEU#jF;Im_b_x3v|*UH-FR49N2yKFK+=tOfvLk?(F9Gn&)vsU2zX2+tU-*L z)vzNt9tj{6ragc!55nLLp?aULgnk0K>8K{hmC6So`3x+&koTV`g83G-kFI;U5c8V9 zTtoRrkQqINeDwmcpJH85p(a)6VZpO3s zou1Iyg`go6%R^g>6Cs(}KIGvdYM;rr1C}-a;yUCd8${Syg6a(f@caRi(hv{|ytvh{ zytnFA<4&sAYv8Gb(NICdmZy9!fBtfRs=18R)W)m^WFwoi+vf?z{2JGGnkMlo_*3N!O$if9sswS(AM9mW3KDptm2I{tk2WQg3Wi zd~4oijI4N4ppk6E+AqV>v319@NKsUw0}lNl$RhbcQ9gG+Ofu0gDg{if`iCB6nt9~LJ-~O3B07laY=bBdrsm*f`QIk2d?KGaJG>}PwlLh z1Iw<=K+s+**L;O4nesJ)fZKXXOBZow-#Zteu8cc3Xd7cF+BYM!a%AdFDLP{tLJJBI z%^+Areq58Dzj3HEQ8?_4e?}-he zt#+SMKLMQxv7uDqUO>6GTU@a7Mc_f=OB1VCfJUs=tOxK_s%ty#i!#LjTukH#h=kfs zjg6hz@!0+!!rnS63a)ztg&8E25|orskrWW=9zg^|y1N^syGv9Q5D95iy1P?J=^PrA zkQzX`2JRWu?|t9jTKC?6SgaX1vClsHoU`|{_Y;eA1A*VEUJsrdx$>X7_`o>cs2lWb zuCKP<5>6&tN*L|W>rdh@>t2O$)CKeZ9zU!Q=M4q7)t)~()XXc$Bpz0nCj@V~jk#Fs ziNj_Mw4zkaxa*`F8Fk+;|2K&77j}Ndm{w4QWWSLa=8dAwT`~?M7`1iG2PFxxnU1yf??OH9M#r?8od3M>L@?}QU; z$~{vl8K~?2@?cLr)=BLXWJO%emU@E3wt~LLF*U>i{O8LsF4wElFv+HZ&rj}!b5CCz z>GZ~Zl%`QdZUie?OSJfncB6n;$-Aj_`Mt{AW6Ox$pJKy?a74BT|1bECyqm^7(;v)dqs(p!@qvmLx(mf2c-VUq zXdG$mV%`J+Xc%0a2I{@I)uOQLjqJ9TmdE3OSTtqF2c4W#9_ZMvsubEKLLd?XaS*9j z^h4~f73n4h7CWFr@Qu)T(J}7Or(rHX$?3)N>>cOeI?30Mwbsq+e;)PiR@kQ*_N*F4 zBCs9b8D#thcrntV3paa+6WF&up3onT>eJL3Iu3yRxVIQhv@&Nw_rhRhu^qTtN(hVb zFhX(3cXHnp5WQ=0BLNiNeUOZo-?GM|iRLd%p0Z$8{RUe&VF>ULo)rPkf`=kQL5Vw2 z_hiOY-4GQ$EiK=tiC!+65d@JWPd{K(dZLBB;#-+@!25Wyzh#nTzWwF5%<&tBXx6>2vhv=o&q`!rY zcVE$#eRg6w;??Vt>d=yM={2jULB?>NE5 zI{r)OAx&YkSOA#v_75=Sbx1Hy(HjH7C(X)2hgciqtsnpJo)D?gcEN5H+kGU=m$$bm|*P{uCdu zMw-1#d2yBEX_C0D#|p1VN*t-84vKq!KqJ2h6%qyYW7QB}Cj)tB-HqLas12_`TEIzw zVJ?LOTnDf+=-A+ff0jxov+#|*@UawIey@WKbtw6dAJbq%ck0Fvfp`bxlaRHsZt48`7Gf^D_CO(_W@#x4d2<#M=cH~2m~ zI~B716iI_yG`yhOv$l zJ;FDG_%jX;_^mX4MpIDek-L8nsX)*8f;342Se_SxYN!>s@eU2i-ElmYda*IhY5b&j z?P5d=*ZybQUo3z%zvzrTuy9^6sw>q~V0yn*|{$|-yfD?5%JTL(&(et2gG!?JwL z*L)=r3#6M3a1W!+X*RP;O73sRGbvtAYz2syWEc}Zdo5LBcGQ^8e+hAmV{4kGNEc&h z^%qkYZ9&;00OCScOuAPkiOgt@4-GAK$0Q^qW#J2R4V`p8{SI7$zJhTd*InM6BuJd3IuH>*C{5tgHZTPiIT};CSs2-m=5`6>_UxgQ9$%fO>WR8@S6$@E00_QV=t>rOJ;j;;U4<@i~I6bZ%#P4yX`{nMptbeg~ zc90Qwix|>a{ryGXVbu%|^;hz$PvrExT;)}%BSJ1~O`OzEbvN%~j)a8uTx#_I6!g14 zLvcFonYTMsx3zYxHZfrlqnadmIM>t&xtdUyjjZ5O=QV;QSTlTWj4#c1nf=Ka{1q8I zSiD&)XE~~xJoJ>slCnXSdF$Sx&r%GPIUzC5nSGBU;#YO0=2G9&c)(bu$z6c&Q;oFnzR43%8H?4lvty^) z;chG!Pf8))eB;cN5*ph<;K1 z>$slMGA0^tmLA;1h3Hi^0_I~xXj)R zJ8!pyBd}nBun`O!{eW1?=l0J+Hepfg3h@1Pt9$I$ zzeF{A`?A@kM%Ls9-!%|dJ>LcUx3d*m?KWll9J)|cO_;TnurNhjIdl|*)tywXK7J7^ zxM`mx5mt+-%2s7LHTM})KG{=M?vo24bVuoZD>}Gg(F%Z(e=?ToLeeP|pKFOSwK;;D z#{Cbwrs+bKN?(U0!U`2s^b5lC%V$0Nn(v0&KNWwm$YSxS>qfxNkG8%Y{qrHFDPM@H zbO)NQz|lUuBPLVcu3JTcJ4xby=UKoCh(3gcv)&68Ph&(@*jq>_Up0bp={RXy9S0Mu zX-&@hhC$9uTq1dh4Zwp=Kr1zQ>Imn)AjUUaTe|t zdmGcFYI7R}`h-QJ(1YNi^Oa5^_+0Bl{TH@t9JDr{_}PlQH%eI8skl}+LaL=*KFDHG zuW)VFJB5E{D9qjr+lU$Taub&XXCr04h6>8gon;OepR8TE^C(;M-hhZ(;jm-d&2TE)1z9C@Hu8ra zJBOuYq((3jYrNFUb|pc(&NfW^)DVx2qBikDKQ-V0>nKoAwvCXEOB9#wBjg!IzF;ASiOwu*HveSCZrn=J#blt6uNXw-d(h znq=Co7W~;5%jH`$n|P+251kCh9ZZv)%I%w|1$0I&U`K4!``eLO=UNXjkeU*>+Z{QP zH6z9O1n z&@O^I*zXa};>RYE=tt4;yWqLa`_+^^p6?ffNg6R_{hGook&~6mB#28Z{f$ z@Q=IfgQDzG1x1#H^PWE1JPto3C#imFZn;1Y#=nvm_lxY4Ncdu#ynw9(ik^bQxvl*w z-7*6n+s64o(&1YesEK3Eq0Xeoe>J)RqjXYVhF!5k8iA&rJRJ`?L?_jgk?H;bp5MK4 zoIOHEnHA<$OyTlw?GN3HIakU7??rQf2X+J*t-^blM;DR#M9oiu@Y$L42I%v#S#+#S za$xHI-?|yR5rz&JB#+H=R3>|dIp&-}{rLVYass9fjxCPO;Wo{yS&KEIV=Ce$+yy-xz#uM#8{d93#z`2&GP6P*`Uj^bhjUFp^X2 zSCI9u?pAGRE{=%nGaB%VgM)*+=KU$iJg%=jrFPxzZ%-|}j2Ad($rA8Ir!A+A!tRHL zY!POM!KU8J3$VgPy!%}HK?IQ`ezYiaJ##3R`Okthx@G_-S z_ORJY$*5V)@16h)TIlCX)po79?R)Wr#4uu_*XaV5s5Ug>5^hsQ~ZRNc92@k z#a_B0DyCx>WxDsCKfi7Goxa!JlUqu2*7`d1%N=Qcl+`GG1gt2}8V>ts20{rxR?nhg z^V^_XtGt5B<+MjZYC)HPd7D_TRr{bhB42$gMxkW5%NvI(mw$vqO78d{rU+4IlOfV9xoBiA!ex=A2{_ym%cC_Ev|deiVn{VK2S{mu8_+`Vx$L zgl2xM+3cE)A{9pdk4BXO;3E!4k=Ha%F>ig$vTEvkxXpFa=zeze)j9KIOLy+6aXVj7 zyO+8}`k=LUATYnNvMC$UKYLcW1{9d79Z&Si zx*rYvvbe9KuVV$s`<)Eyt9hMU_lA2MfW(_QA^gN~f7mQI>btey63Ht-4ENxHCz1Q> z%B+~#pRJ)IUxgy|N0b8Imf;KAo?9a)inv+ky9@Q9u2a3_+pF?fy|QNkFdGalyP7sj zWLZJd>N9ox6rp2l-&@(>`m|QNwSF;9Cu+JMgLUbgNF{*~L2X|2yaOJ*cVycQ&Q>G7zi=V|Hd!&&By+Qy;tEvCL24oOUeNnbfSbi7(sv#v*84)KIxw z65-P`0dk9ylig+~>Lz)Sk3tp={Z6fK$M;KcOJ&gJqEk_5QULhPPRvY+ZQNx?!C&}_mv`)x!hJSv# ze*piqbGLgbQxA9GeP#c(?XCLA(d#u{z+`%vlY47<>kByi81!75n8>jncUCr^S8qxn zIoyUqUR~EX57XyEu-6xV@%1`|W639+fk8d%+hjID2;1 zu%?W;QaW01U5}!Hb(-4e)=ltt1Q0?E)OP)~`JxHX$@B$)Yo3OvSQZig+}Sd3a)j^R z=f0;b1&bE3<-7fU=fgFCl`2_X&!f#_r;CBgb|`^Ds;J>0VfR;r-}LbbylL}n9!vD) z2zwK@w~%S*I5QsF9MFY|`OZ9DjB3(jqdIscYT@#$2vY8Uxd82NIA$*A=3AYt-(EGFfv(|4w zee(QYJf)+|w zI%Bz$0KruWP|1C`(iQrUJ`)LC4c*-F-B}kz`w-8aA>07s{e__$rMAS-*%=JA=3QZ~_={%0-UShCSB{lIi#Q9UXTUyE>+@lvW}J6tjl+jN{%z1kTx2 z3x6ezXd>v1V9_@vC*EBjAU-csJ!0}4Wx?zj;T{W{(Kl+geaA1=LfFXx?ic)p)6`<8 z!6yp`BNvh4_zrB1M?ZSdG#b5YcH7u}2R-%%B^RzkJ;8GiQ!6msObqvd$Y;rj*#>~x zlIPZFxUV>`@e1Nb-^o#yS;2|0zI#t#qEr9d`MeF-WGhUd%3PpVd8Lw zTNRFEIPWaM4%j1nnb*W)JIVDEu%tP+zoq>7EQznA)N-c3;^QW`coLWoev%lYDax0< z*mP^s-j%M{m%tY}GU&i89h20obu@3^Kli=DwTk<1%nRaidu=G z)<-;F)(G41s;$OTwaj+7=Ne*i0uVYRgQg?;Ky}469naN_zEl^Y0pPr4hTBxlxW=r5 zA5+vULz$Cv?h9{Y0`ew&LCPF+;;zr)T^a{`(KCB

#6B1A!%a^hlE63Nwf1Lz?@T zVZBC;Yq@zz0B50`!uGf(s^b9d2;OwAS^_wTvae6RWkbJ~=o=?r4FY7q8-RxV45Z$Z?M(Ji{rNhU4`CdP}(j)qHceCUK zm0^9vZRJ&HXuQ=v98*5t(c}Zqj*gmHD_S0gY($9!L)M|f?TGc%4oxkAX5~M|Sd~w|0DZl(s68I3@+5{>Y$uK;-0EzZg1M|0{2@?0dKVd8rdXKdC-OPrNgx zeDZ~~QNi-ab=)xYskqG52-xXvzhF0aZ?CL!isxEQs?cGQ@Jv2GWm;T3+Nj)Z%wTod z=o?UUR)PoDdsL(oLj|4%?UEox;M_B}F>TbkZ|a`1E;T%x6aE-}eo(QK{k5q`U=*%7 zAsk$$gE)oLVe3$dSAXz_G2^t3>N{Zt@}yOv|I#!c)q5vsGydRbRTI*-DxgwOs_N~6 zO(Zgd-6!Ya2j};Abg6*cu5a$*u<3#yP-U>S3%`^TthJwLGu%UWY#~B zp`zbUp(lP9hkh~jJVDJA$!jKS8-VvrGyahQ-n*(tVRZh1H?`ETOegNe@o}n%GOWC6 zSx9KRt|W$wjYHSgDg*1r$VXJxu%%{AK({WSdvsHwFrf7w`EjS^ zJIR^kkcb@4*}{I2%v6Te-Q@k!_t*!~X~jl&Biz4sP+$<+XRthmp!+w zTLpKscn97M^JF&wt|n&r98xx&mHft&wHPd-S%$++TAzwhwLBs6s(|_izfGr9rwz_T z-Qv)LtWp!f#i{o{01rjY!||#|r=a|WhNjtJ=iLYu%0pC3?hv-6j883lRXWW0o$sEf-&t2z?I$dL)YN7U9f6iV8^hdkEf9Vyx)iOP)O5DQ z9y3Sddt~@ioaRI!?!>Llf6M!)U?1ur{Z@Eqmg|jAK+ROSyD7zn`S2Zn9stfM4MlvZ|z3%rNzsV}U40MK; zinsdJx#BnuRQpE3mrt+VgpqftngAixqd5J|Xr)RVX%&tR&CMTeVJvvj+$m#>lkLo7 z&3n=LEi*d%hGH#%lTj;POfA`WKTltkg5^~5Y(!b!MNx0z4Qo;5HzMuKHR-Qh+-3-> zwFcfXiY$!9n^zoe1~n_LjUzu*DV*NMjOH3oEjaLuZar?;H@Vnc+fiK>KCzKU3O8gY z7gwS19;BYTD0VmK{>3nL7Q)7Zj?v~*>YQJaTFf5Cpm0SR8TXUu5W3>bOn7SJ{#f5R z*miVCZZ}#Bd)tIYS%M-t9tHTE*^)7(KTQ^v^z$A3Aq3}oRy6@{ZufDH(F1gY?fI6Q zVCM%3C4MQo_c*3Im&Vf_G467(IE^_zYZBy0OuaFaIX&e+Z3oWxD&}t7d{Ng~kDsb$ zHlFWUFvrd5EzUN~Mf2{T=F3%bjqqtbjNR;iE|S<=JS-=uDu;E{V=khsxi&95c2T#Q znaE5tq3o(1X4mL05v0WdmaqZq8Fuw@f_3e_rmPJIdRr92+@K7*o=J@ZhO99CnNs(~ zyXNe5ERM6j+xM!SYq9L_jr_GGD__M4kTa}SIJB&>M%nX5(r){o|B9ucyvx+o8FK!e zz|X$%u;K8~vV7kS?1|^8eEAN^B0ip`2`M>kqg@nu+D+W98yX$wtMA3=Y4^QYna;Q+ zsct8J;=@k&hpia-W1i3`>hw>RLV5=%3mLq&JQhYS3JIj?vhP=qo_-f*g(~pVsK7?IP7el;_x$)FqBpknYveC1Ton(kT<|L};S{qqvyk`UuWQfjl}{F^ za5PC{{kSc1zjPv%o^ZT77>9QPS2>Y;zOOX9k}A01kh&UBUNRd=fd6E*arH;A7@S^n zS57kW&t&0~kr(W>_Wc-(ldq9T*sX8s`ql&lb4p}x@U^rwe6*^;f=C2byJ=jcKl@6vladTT*yJvm39GsN!uEA09D(u}pua)5ArrR7OwS88It>vQ08{ib}T)rGmslU-%9 zG)_BVSK5HPfgaBKo^Rm|XRXfiYxK&;!)B~|(Ka>BVeF0L>&_m#bD7_@PuBG>w498e zAYQ3m7xz7^n^QFtsP0Ocp7Mq2y}Qe(eMntgTVYC4VJ7qe2_+CJE`8j5P+MwRIC~?H zEbV+!srS=<`XL?WUOCp=xi$7@jXE#UXD5}+4H$$C#}%n?y`l`X^9Y9fStjcADopFX zsJQh9Jf}0=<&%{WgPGo;`&&srpm!*>9E#6T9dNDE7rZ+y(Mj)Xeg!A5s zv+=Lb!jY(H zHp&atP{YLU6F5?_^$twBM`2nG*S?@W|2U@0N9s(3;zMS( zD$2>uoIjBr>l}Y4bPzF{xlkibW&G2!_eXX{`w45JcLT8noI|4fUibuNV8^;;E3pl2 zC#$kO#ATCwAnihVm&>2#wxJV&i^^7Bd)5v!1BRu)sCM!cN5gkjy(vC>^@j7bc=RoH zHTp+sFpM8-MK#ctHHKfK*$AeFI=N}Vl|%d?FVAnbrXJ>^lPagP2a2U>aSc#6%CspxOt;zN^RC4M`!+M?aZI1h_x6+@rj(CBH4)0_skCafhl(vT?gL|| zr~G)$u`vg9Y3{b;(9eKSwW-wO<2~*6c{WMBZ(|Ku8#ka+G@r7fNjRDjMIL9~8b)Yk zZ9eCIk8!tgn2RRL1ranZ#J4uuc@@m#c`V)vFzG;eX6DZM;a-ioZk~yGBvbK~m1;dv zV|{9Up7%oJ({!z`#aSn(CiZ#lbea2}pY6Jydlbn(@NxfQ2@#=vch3i7?K-qvdaPrl z<{}jHq`Mq_K9`77{k|&#Th=Imbt^GbpVZ2KZv8}Vse%}*aurm?I(hm1I>wi~zi&X{ zxA;p-`5olD!t0$PqSr0WV0J;yiF(for0!2NN>yeyrYzp1%8gU<>@HzIQo7uVMc&a0GZS4Z}*w=wvN}EbMV6B|`>yM?pnSI*&oY4Vq}% zTHnsaE?qY+TuSfoZ{oO}ilzq)HLT<33A8N#} zF`W74tJoPBb6(5;UbXprMtKsR~ z{yao)g5VLa=~Nwck>Fn}KzLsX=5V+(C@}bm^Z9hOJyk}z9HhWgX)u>5FgZs@L|1ZD z#kF&AaxrMnHAauy9B0pAgVqS`P?H|V!r!kE6Psb>+*fb-gcrezjW=sIdU(1zx-hRR z_LDh*M^N1ZGqttw~dZn!AV zAnCTc&|P~XsP0+h=qa{DuPQ15$E+lz@ z!_h3t;+Xl;U%<`PH5xHgUTu7M(N-}%e7x{BA>p+0oX2MEf-Ql3VBrRRj7Rd$I5k?) zeeFsc7S>SD4(-g8TRf|+v{QBl<~W!aiso*2kv%CXOttLx_W-PHA6{?N{Jaja4E$kD zt7G~lR0lI}k5K&1KgW#`^O1+j!bbi$XqDk}C*o!u8^^MGf|cpt0h67x%@(>{>Hc}$ zW^JCa&x1sMgCIvUG5zvh z0xyBmfp5j}l$DC9OM=TEjFXgw1=p|)DPNGyKTm4-iZ93q*Vm6nBhg&TYa)sNo^)fw zjw|ZD0nTT^08?W6TO)eRE`1@DNQliGn$i)*#>?bg0aw8aCqsm{M&jDVX5E$mc<$7G z=B#GP!pgoo(_5X_JT=HahNdMlg^ayH6|f{wTB7?CS(`I5D^lsPrs6d@ac|!^79bX# zN1t?ECyI=$2@^mNB;ern6b&tF5Uc5VEV=E8+UOP>`$*8JW3Eo#_7?Q9dpb#En^3U^ z-0pFQi?KU}Ia$sZN;P>a3FdnO(pjH{xIi|U+N!Pg>TcQIq-<*3eq&K^NZlRWcb{%Y zYN3Qb9gvo+WFiQ+zKHlnJBHbR5IyZ$P_@4`=2kMZY)e>p0ZpC;7R096nt(4wS=;&` zU*Dt*W28_GbIqy3p~yBizv=Wf!K^WQgX@N69qU)2myU{S$3?{M(EYuS}-RVU8Z`vJ}<-xOB1<`R=nwikU1u&Y}e+<;r@Ih2Ww2+A?el zd%w)KGV9mqMeXZ|F|2a3>Gz*)ECbrCgDeGKeUl?21MGCBW&yg!fjz);y8Bf4gMmTf zv#I6K-&>^l!2H9*HnrFMfPFq`n2CB~2zTnkgPz5zCX&ovp_mY|$gIf?$@@zV3u8Ky z<9wfYm5}0gA`MeG3P{FynOvOl^77%fvA$Obrv37k9+2P#H=NRLMgnvsRf+=cG%H>|ZD z)@(jIu2MHg(l62Ic6&`&3?9xYX*Rv#5qKI3^Zes<5wyz8wp}xa_Gy72jbR^f2@cn6 z&h;uskQu*w|#u6mPMPxS3LZ4%LTgSpW_JIRAVDWT>Xy78p@FdkG_SV@O z%vIN0^N@y=(UZxBdzdPoKPaZ>GVo9IPR?)0t{+wy$EJvck8n$B*LW6WrDCo5y!civ znY?GYCe#?M#mI*l@BzDZ5armS#~5e3IA}e2+8bTAe{fJfn<6(w+n+Kr1uGW-{^Rj| zo|jbtJF>hpDig(aErC~J0%~M0sv09$i^}5;EkufvQ7n-0{7z;|&S-*H`%ly=O`6Sc zyicd*Ht990MW*hfd3o9nRdtqYTbJ zq#1G=z5V=(jpu!d*t>uhYT7=GlA5ONtA!VFSvnWqd>m+=-`avusuz;2`wL9 zzzw38pD(WiQbLKZQ^po=LT!{yy|TrasRL+{6+Z@ZsW<>MGO*0#>}bZB=h@HBtaK`Q zthY1-#`lc5W?!c>V4cYm zK<}IGCHkBHypZsG%{`sWIAP z6@h1Pld8wMhsa&hs5zDhs)u*iyVW0sv;BajSm3rvk1QqK}N4LkweN zK%}?%6ywuo(QQooEYlF!4P-@rD|Kcn2)z#V*lWtr%bnFuZwZMv7$WzR0|b7AfW-yz zss$QBL{Vey9UIwo8UW{0wOj;%{dO&;LivQ752VDJAq@%KoCew;q|d^JcPA9a^}CD5 z%68EdBB&7dmk5!1A`ojfj$e)XMogdISgw))Cl7XIq007wQjAC58{U7tyMNsR{=Bt2 zOLpB+(MfrDEyJlF;mITC)Al5ml7seP`6afVHs*KR>7|nnxvybkC)SpQuuFJLPa|sz z->)Y#gjls^@l=FPR}9!3Al(4q!~{HqSu|RA>>B_#VN|uTFdrEGSV9Z??@;^8(xw+= zgt`rij_w$xWBS+FceZ7KJ2chOOh!k*_w32iix)p{!h$GUn~QvUEeA9+>97}*VRe1K zbbUuvS-#wlo7(F>5m4H$C~pt{ce}qs_;R8F_YXh_|0V}*Z^e6mI{+Oz3Q=bE>E+hd z@^LYr|J5Ow@j}jr7QN^JPJjhY^wd=H5~kEuvDpH+1vV;)tEC5+r4pd~8Pnc0tKIfNaQJYmWbbZBo%hLY(3o z{|I-5w9;F@-1$rJwQm_izmgRJ9X+nV(v2)GdxJ(OL#-GQBfIX}eZil%Iy6gLDKBbJ zh?#o`*#9SD2G|lHj!3)T5Q4Nvm0^?2h1c+CklCEuEc()&cLB_Y0z~6_ENgb2W+6SM zm_Of*>E7bu>j8NY3NlC7 z|3UfOj@&=j@|1Et#JC)Dn%$E0d(8Wq)!W~da>|q8Z!p z#p@Gt9Eh=i_+SnM8o}Rgso{lqBN=)sL5~7{_U)vewK_PzhJhg71$=s}(!+AH{EDVw z5LskQ!Wa2}!$;&|VR|RlT}m4>0+*nwD~+t8=SQqllT$Rq4naWzGvq?!tJk z;!t0?ivqAcAR5$r3+6Yc6MYG~c#4PDbcm^p((r+j4uQVN+chuW(OwlZ_+?~{3Oy`U z&8`vIi`RIsq%kRd(A-J`|Mdgt`3_NWi#$wGA02=oP+}O9Xq?^nZw?zSPML;2AWJm-PAT zx-!v`2FmdUjDgpNmR&}DV13~DtX-WTcKo@esKHgo z@?@_vzYJsm{7LKh-{}7j4ECDhTGX$Fh>@rOmc2EBn=l4k+;JZ_^JY0g{yu;75Q9gN zOt%Myew2&sMGl`dL&HBOTjVL_4bPsxZBfqBiy^Xu)&-CelHI-nz*2;rs3Mp(ML#yK zXaG2G0?TjPf<71f>_f3kjY_Q|@6h)1&BFT9;qsp;atp3g{P;3h4;2#0T}ujjExq;> zvz8i9ZYiMa&sODd0Z z+}r?7ZN-^9atP(f>%#QA*jV0c%5n>1+JbW8;^%0DijEkQQ^}Q0$X?5apVV3P29E&I z+7jtrn}`7Se8u9ex9ty6z+k3JSSU5XpmZA-n9*eh9>RxoKsumhVKVNq8a40p?V%Sh z92}1yzk;y9oqfh1WI4Q-O=|DuaiZ8@6r+-n3WUvII13q^HeDdfL6A^x3Pg0n53sW1 z0o2-sJq0dgGcJ)K{XTZgmH|o%%ATf0*^tx>-cO#RHboc*QEQY z-aA$@vFxJCykk{dgw|_=PKbL0#VwdO4bvQkWvL`(u1XQEylV!uL83?SJmgXwmE>@b z=d&fpu-HN!p6Z-cEO31Lu=J|{5$e>nq6(}2!Ch;wM4_kh_ zMW8jVW72sbmN@#!8+(e48K2d|A*(!&ux8R$Tyw2jaFQb{Q9FEh^tq^;x0*3$b4p-C zpQWv^!*;o4k=chAsN@Fk&v)(u%|^!_p@sRqo%+NEjP2T&m=J(3)6CAmJ*@`WCI#9u z88quprbNCPwl1Gg6*X->^I496-S7*5qc=`J6115KF1(*Zx~{lethhAhyBH zzD64VJ8c3B)n*;{b1ww9`D9tY8k@l8XBwA-;lW8deT=IU`nwYJAD_KM#|dChm;euZ zn@Kh1x2!SUrz{6lbySiXT(rWib%zC20_@hWV>0l{oqrS}@knzh0~~8)4+ripIUcJe zTYIbn+nB;~2OyH~j0tdD=8S}c%oRTy(Twv+7Aj=L{)m2E=((1y{T}>mMgeCTM0N;$ z6=mao^N)=A+`Q1hTRs?63RDgI_DNuKzo;g&Tk_)g2kE2XNB?3Y!NRTn>^$q?s$=kx z*a-G9FLnMBRs9s8a{Ap@i}rh7oNJ}~#eO6Omkl+mQW-FO$tEG2f*Q&`J3p@IE^FfRCyHp3TRE3uys= zhOwYto>!y)T5X{fg-`|1W?I;3;tQ?j&Hz0m~&ii&L+Y(*7 zY|bPEG^b{DRrC~E^%rDRz|$`hmtyXuLZ6(QR<$&Qis3Q>LAg_a8b9eJYD4S9hcce)nEjU$ z2KAgQ{C2ggB*Jhx(k!^;>T~E}3sGxp(#cNK>^XTvw=S!(1waVXkgTwKq;!v4{ZV2v z3j&2Dc-EL$^&FehGw1={4TUWQWs44~q$-lPG=MeGZF(HX0R~2%R~$UEGDKg`2_OVl3? z!F~wS1FEx_LI3J5DaJ_keKp#k8G~8(1-$boPKsrN7>c9hnx9ThrMO}lQI;OHUg&Wk z_wP_l5BtHupYF3A;&Wgk^O(a!Ll4bn>pjYxuHSkT{M2Bv^PM#ycIe%?!OS}UmRp=# z%iRo_Omh-X4_>cSStGoBktdkfIS#6jY|2p9VOBr0j}#qQoL6!==4ifM1 z*k-`TAR+?l{Dgus1mYlR`g(!t<&73tTbO@5`ZUx7RkkKBfi7H!P+`Hb3_`w+ISg$3 zB482liwT>@zM}%M&M#@dj)#Y*?s2t2q8kGrdlWn5Z?W)!w?HJk68{n<$i;nahWX|Y z!zmuqy<_nXUm$jj|7J|;njZh8^2&`F7UF+P<8rM~?#}0Vz(pVhllLMR9G+dJo=Y7; zv&*~R9@sxfG@$${%hb>b{`w&9C_fhGj6*9g8vjxOflN7})mS^IOmcQ^>033l#ghR4 z%x^J}Mm}pmhmRW%WE-V}Aw_6--9k+=y<7OBCIppxy<1R>tAKyGSAj990Ev?J=8ONU zxg-u7Zqgra-V}cho8+CxMo@0APh&{Y2H<29?{MGTxmHCB=$MMkuH=(e8(jUZ8Q8Ei zR4sI$J9osN0JSnn|72grhcVK8rZ-5v{OU-8_2zgrAI8gac1W$Ho=VDFK+rTw1jXN4 z7idI1Fi^`ui%Jxq$7Q-r1&qOvB7r-4fE>iiz((>Yv0iF&auWXor+FW%L7=}`xc3uI z$-={^fsJ=aF0Vz`6_hbXjRRB{Z}ndxH@-~`#`4R){VK-Voiy~hGKy`V)&{BJW_|5a zldf14di!Nh&7B9{N873iiHWJd*zOKC{9^CDx>B$1c=JKapXQXLfLKFf0%iWm9=5>A zes^4d|E$kiBB-&Bdu2*ct2;Wy3{uO!`OeQvZH6>-rE%qIEHb zp$ZA;`2#OZ_Qx9aLd16$`QeuS0q5;9rL~98C8S`7UkOysR#oXY;l4z5k`}R_E>CVS zvut2Qn_2(aF;wW>TzS?!&AYB9NxXbMuCG!sQnUMGm)R^Jxf0Fc*ONZ6hv(E1EU%1r z_43I@CSv{(4#-jVclR)66#&8k?-dhl4EhJ2dn+@Pl#~}LpVQ**UA@JkIN#U&gpsxa zL*?Q$@0>j-&g}URqi~Jud4N zaay6vt%f0slR7Q)YM0yHTW9V<7TU(Z^)hLAay_zUS>s!27+!q;SB0p_qX%=s|rR)CHba4^;^z z_;JAdy-7a3ZVj10f7?4ba1Sk#?RB~hLxX(kjjq;y~txt$%*G zqVMm25A95|Nah~o>?7KDqC0=Ig%kYKLuFOINi1;9czzvw(cgb8)lX-=Pn6BjKr*B( zR`2WH?$d)p`1Y;f4;_Rysi7fPZ4^7!{Z5dIh}+xQ2OjQp5$MFkf0{#`t2+u|tp=#E z5d2xazn1t2Fhk6PYl;%8NWi{oaM0f`E+q!j0{a+sBHm>L5=g_Sq5f-oFV7-IT=3}^ z6_-sY$RYH(Nlg2@$G;nq1bka8r6e~5I*uwt-?%Jh@Moi=LE=$HH$L~vpa|&0KJ4!b zp{xLCU|SkEVi_1qGg5$ET+748`nwS>O-(>KIQ^t#WalLnfF3`>aTNYf&kAJV(~z9C zX{^^|k*Cb`u-_-=pRQ@|gKtqq@zR0v{Y?!0(=BNIA&Me_Q#ItX59ni_1XNb|x5(z- zqZ#?jE11Zjtjvh|b^OaK*8l#-5;dvVgyx7eFy}y`MbH2Aob~{GdR2L}hTsMV?V;*3 z|NjbG1AL20Y>@_>2U4||#lJ5YfB(h=MR{SCdsXrjl-g-#MLqBS2pTo^W}w(;scD_D zo?vo0MR#rm|8GpF28K|l11om`%_CGk{JqZozpegWW<#(9H!^dbXn^ZsGw%c1e}!EP zz73X$a*P7nAL)!|K=U6Z=tL<&kIK#P1Hg#kuZ{7aFaO7m!MYD7r=%~zhjLT>GwyWM zd81_o5e)>E5&LQ6`hR==0+xXBnd(mwg;xJ*bq@6Z3fmAE4eT(wB|2F!xmAj0k^ihz zBsq{od=B$1L=ZThtFZs`B^vslk_XyrKp^RjukBHZegB9|3Uvo7AHnd&09KALnil?F z-Tgy$)aR21E`3EtkpBw%3$WFMB+}oc6Tsw#xczEkfznBOfw*P_f&k|=-Y;Ix;{k!5d;ZGng#hZLU>`AZI3}UaBu2W)6H=D*s%Y=e;# zbnVFAjCAb-+ z3>?0}6c=n;`1R;2bau1#H)2QkF?A`&A+Cd=fx!hbxbo~J^oREtEyFaNV1YR%DcbYa+5`E z`Xs{dY$5EKDx4L^X&*%KM68GA!d%Yo_bRySiQ1XfRyKwASIGU^Gfozoa=VPd zrI{DSJWg|(r)r6~Ir;#0QFxJiE;#Ke?lX}MZzkt7>p2`2e8{g;cJDl)a;rZ}KJ}bb zv;(t-zz`OB68-jn>#N`h0m7K9JiZo!DGF~kelkTci38O_WIhVZ;-zOIBvW+!AW>+K z7387s^W)InrAsM!8)LtVO5(Xu9H~0KA&m2f9amaYJ3;n&vfQxmDKX~Jpb^c#^zW$( zZQKLc9N&3$PR{BTYe!R4Q+Xe!`hZ4hAq79`qW)Yi_x$1h0kTyU`2~3j?_2L1<(Y8@%$tVINvni?0SMVA zH!siJig3r4vehEB!bU;qYNk~pUZ$IM;rg7)Vbb~oUc~w`;4;QsOYpq&&)%O`Pm474kIC7c$wO})SZ+CM-t#oM22F^# zhzYMke>05cri>SkXxtyLvpU>T-O|^V;LfJWv>SNONmFY3Fh1W$>7#TOrmipMF4ev? zL%95`U!h2HUZgRsk|$>9=kW{lwZn7AiN{E!$%n~gEzagZ-qH1rwI!jqb`-DohLeeL=iCY~>s!jS_{W zsZ3;|hRq@%-N*@S-eK1_m=C<3CGsF%RTfjU7Jg1MD4(5^EUMTqog&hMqbR7rN=_=Edc@nQA9wBgdPGYC^djW=z(|ReU9dT&iVAtoOj;m znfrsIGfwtzm$lbkkIYe5Bm({GOaH(k4&_u zk_ya=Y~;y!fAtGtVy_*0i5-0Bf5_9ewCgyAzl%U8gVqXLP}bkuJE{Jeg^7KeHfOD? zYzGCw1-6%#-{qF>h;cx++6p6Q$0KYiq#G&v)`Sq z40(^+`gQy{NxJ7jgWX3%P}Y>`5mR^Owll0GFo*;eo!h}Cs{RgY z7NqwzH%@JR@PjZesdsAtPI&<;F zsT>2`RsXgM135NzOO$6`yJ=CMCv6LtW1JQGie#wgw^8TRh7(t$ra2z$oDE(Dbe%iDfg;|_VpA;%^Z@9{#0vlEw}=W6E^ zLGxXz){RJb-xX)Tp*g=7Sw#$a6*!NjHS1B5Z2I%7?eTGl$J+TbLDt@{TL=oRfO#Z}Hj9te-Y*d;QuH zvP<9PZw(u$YflxV1*uAsRORpI>kbTj3#?jx@F?}IBZ6{QaY<&$jNQ-uF05CE4?F(yWE|HKv?Gp2WoZ$^JN#;Zbqp*T_Y2R|D&fU;!pL&v)$5e?{vS z$x||2?V38}wYPc>;o;N-heD&xMA$h}-Scu;iLtR`#!YT@9n=li^Yb@_htkNyfdELT z^SlDE$otKZa78RPoGeB&s%wh+5?v>(2L==8ClK!$l+%at#?;jZp|$$k3bU359@X5{ zd0{eAlh1?hu-d~2s`WqrT8eCuRv4H)np{V_lN5B1K&vUJMXIBKZhfPNqe9IF<(x$d zkO~w+sBQA}qCXd7{EB0ql?bQJ>%P6Ib^gJUI$=*WoZd4$za85ioC_*&wK=9M-^dx( zw3##2iG4uiIu5%!ZRexDNpf~p8N5g=xMSE|I%f|(87RZEkevWLO za?^S%km8pN`l%OfyLDWdNXuFD$m>A%gf?Muw&r&sIcJicr2B*T^57DfnKNUr?}cuV zJ3E~eQ8 z2Cf9#PFVS6;^qtI=~eSkwn6w=35w13(bQl!ve<$vX)yze2pTbS?>Ki{f+olnAonAv zUhMh{g2U$iTE*gs@UIENytOydCwQQ5%^YyD_56>N`{Eu9Zap5Xc|plLFaCC&JTY;O zB#Dwu*G=~+zlEOmjcX5l9KEJ-&+p0Qupf%oKKi~CAzfM=sKb_IDdoUA7LA;zLCQnLGk0OXcP-~ zA(7TMG@pBGFOJ;iswSpKe);M`o&PMBm}vR6?mg;k6a<^8vAso`n5^&Vipc7ge<|j$ z2f8|C|KGPp&Tv>O?rLymS)0cx&f@TU(9q?ORSn@2s(J6aP9j)Ub0@B^ZyKStGSuct ziKWC_&=XyX>CIUzHwNV@$r?=WCn#n68yN6MzGnVdRD0#M{K-ta0&f;mj&g`7`+-s< z-lm|4bzM`NCm29^%=z;+w?saz>u>ZDYIBy?mM)Wm22?3Q9gN|`rNQF0MQvZ}*?5BC z4NJj=0f!>NgQo)mo_cJBzapnO(q?2=CWrcNa{9f+H_*k&C(u;UG&b$6-Zlj}HJm-0LvO2Ifs8H^6qv#0AG9#&|%pMKxotb>O zn<5sVY%@|impuT<(V9JDbJTUwWqq{e$8L3_+Fs&3fv{HLSbc`mc`m-&oi*5G_{a1< zc-*U-tyup4%PM!J!(~F{bPwWH`xotW|8m>){3kWH zpxMJHzS(}n?&W^M`0Tz!)y(r&nL&e&G_%1wY)rh>vv2EL@6;TnDGO&yI`_{e-p-vd zp%#%ZJsx@~)H%%8vO#zIFJ6>5VUND;ig8*ooi7T1pt|M0Pd~=ynM1F{Ed*D-nyZax zp)r$U>I(jR$Bf@euCCo~NQmNft5=J0SlW3JX#eT+TQ;KV{jxqgx?|U5Y|NiZ`0`WwP1f{H z`*zecsnrMH`q`Z_o7-`ge6-WbOb?5#%u=m*pY~%R=7$ic`Zed%M@+>V(1p`N?R369 zOozFF7n*%?gugXR?p%pBlTF?`8!rt)cLF=d(uxXKIj#q`;aKb_{ITpC|fP5S|qkdz^XLx%uVt&$>FndxD z4>ht!gHGLVNv2P6zHb$R%U_Fyuil@oxkolC_59iZ`E86Ww=^qq>agfbw@&*8FH#r? zNUC#@%^G1uL$K48i>t>Ut#mA8CVi`4rvV)jj2@%6s;gix8yMagp^iGE&uG>uxD?|G z2t6nzt!$S~5w}r?2*d`|@6j?|XG0|)X)iFj(zAp03NxpvXfid(5Lp$4mqZI`Pl;_6 z9f#I$V?zmrhOe;I)jb~f`9o_gb6TYWQ5~ALg*9Cy75XpaOcy&k z-HGiEjM)RtK9TH&JidrLlpaTwS;cfqFPX(zZCt$Cmv}E_zBh1tt@FZenc`C3g#4`H zaXnh-YgB7t2kwhgvzBNwD&8J#Lk*Joa?;7n%eRtWQQnfmwT8BJmv7Sf7Z~RF^g%^ZuN7RHrH*)RP7Vj&q@ybybp8 z)A4Re1qR z2CjdLNL+4Jk7*ZwN5zxe%xBCTy}{(OInY6c%AE|caDh`l$8*IQs%i=;&q~^n_ z0YbsD>A)HCG0K-a+O9mo!3550Tui@wk2Q|P$NjXs@b`^ifP{g7-N-o?yUK`LB8LUu z9={26)O-=a&-3V!9(>)kgxMCn)e`Ik*DRCj>7~;&7*05Kf(jUJO`1v)l+O> ziYwO)k}tNH(V10!+EbfU1SEaavq=E zhHCWVK6?lRqS=R!uMI4@{>Ys_^0pIFTjiAi6{L+GuLQtaPy*L9=!A`jEe8D3BIr)g zIFPf)MG{Si{zl=@umLs@f!8|V8Li7qzkfUn$AC=lizaJ=NHfp+$=7%2j2a0Ze(=lUC1&a;b1<&0#v?j2 zk0HDiY`Ii&;iHfXyO<7+G|K(sz}b(0V7Aod_I>4GQJt!=HTrQ4&wv9zLNqmz150Lj z!A8G-5~Idw*?LJ{e3T9N=92YA7W&%+vVoBh`>9>iPl~{}ggg7==(pkKA@ETJYtgm4 zd!ZKzF)kAH1M^-1qGI?oMbdfa(gmY`(T|I{0S^31W?r^4STe)OJ@oqrtIuMvM;l1_ zanyouPU7#g|3f}4z%LuR_H`e!1>=UWD2dVUZ_AE+x>uk7#dU=9euw}OMnACBGcew( z!%7C7U{M+?4B!88;LSS+u4jJj%g&Om4$|)*$kTyYrW?-k2Z3*P`tRZUhkO=;Uq)s~ zW@{6`FW1<;ROq(>MCk2d13tdvB3A@?)=p-I(+_O8qmVQ&d!=E(CB8EUY5B*2KixU- z#KPCFuY)C5UZhupAVUYfrS_^{W(oZLYW|?~KjhOM{F3eeRZa?H2*!(gIDfOH{K(FMpRv}`Dg#UQeDH6D^nZjxVl%-MVF5ho)z5$sRdGHc;;nRSSdmZk#e+Xz z4TpFEEZA~9SGeJh6u%b9W~P^3<^!E|VcS$*#t_5EQh{T<{ZC;Swl3bUx{C8K zuQ7R9b_gCVPw?YQbr5(v@OU{!oA5VEbiM*gN8ley=UD;z7Id~S5fUfBgn9MKzIAPJ zqR!}HsT5PVJCMJD$kqMyxB8$AW&pC{>Q~>nbSWrpV#($zrQIig7>{gEQDXh>qsgs_ z;b8W{SK~1UQ})vT5QO0C`FUoCYd7vm;|&C!Z+|bn+1d+#TM*OU;j(9PM^|PwpQC$g zAk43iVzi-yxaAd}Yk2NnOUR1fmntP0MkVkDjeq#4L4SLBV~4y#03HKASDf zSg@nvB>th{!nv72=vlRmJ3tG+jR(mJ-BfE)1>s9Q4nSlUijiE2>z zPb`4zasQ#rWc~~>2!E;G%?_d)c71E{amELKd+;H#VxJ^o-*>+RBNBMUb8y+m={A97Z*d|+b;pKL>YS8%*2AJY zLJXBM<4_yqB2=r^oL~sgZp`#%8wWh;GWt_ZQ9Sg=<+j=O?-$ z3*mK{fx~ST4?YBb=3Qv&c^XUJD;?iG%lDNS*yzn*eWKs5NDnDAe>J1#?J}Tb# zI)E<%T2)Da`1kZ2aNE_h>p2Wnt6Q^C=+>nf^8hz|1qu~)_pRP4EXc{NKJ2&lo#R5! zqcgdj_Ant|1^vGsgOn{~{=+_eA9Y&(3gaO@#>u=*1-Q!Gx0%A3Z^D~!2A-Lbx{wm* zz+uMW6eXE=Fo)g~6MJ)>^IN74?v1!zp|8JB-q_BP%|C^?9@kLH3BxW;OKZT9eb=9-(WR>yw8Idw(TZOl5S%^50sQRQaLYR3wb0sC)rKgAN)08L7Zf`*uHkg)paZ9HEV?o z!FAHmykxN*(j9$p&!h!rYAVb6J)n=QiJz#w4!5myoK13bSA}31!4dEZJ|og8d!9(x zVgV#BXSVk&qpPdca}SQ}{(v!wT&+a5)xFL^E7pCofu-J5YQf4%O_Q6XUcWJuxlGtQ zGo2j^(ADcC-F`9dwNP;FmS2zCFeb*t6_iHjo&R}Jz!pVCyK0rNtqSObEGN2EP91fM zJE%AEjM0jW+FTu3SKk-B4$QuVHy;3G@Xxy(X#q3fI`<`}ajR3B%>p5BzL-36u1Pce zz?@Pp_Gx`rhDW1(-?{miQ3C@Nl4w*_oSN==3q0rrp}7C-~fhST1kGa7&J???JlL1sIy1h1XvZ^a z{4*s9H0%Mp6q|*)X_&qSY#zDAq5dP+;CyqV;!yELxK_m;&%&wN6|48Limn-GWCD99 zlEX1J7VeuYH+A9RFW||28hL#7?+PUheZqfevk|iIzzaAnd>7soeq&Xa3PMTofQuxj zy7rX>ue~88d(Kgp?i^nkBAU*X8GM=13}@rj#rzCswHh0X%My6e zdE#Z8YtthdvSga4!i$aRb?=*U);||cq6^H#u3EU#R`(Fz*IRxfZN{Oe=ZS}6>~SOn zx#orYR@$0E?C8#{V4CY2gj{HaA6@C)2OalldO|0Myry;oQ(5!8i#1MN90lhmCCp2R zSG5XQqYi+JLnIpD?{3T^O?{#!5az1(4ICQXS>3INIi;v#Z@2!Aa`RBJdv~_LlK2AY zt?+*MO+Ir_;dMgTLctsssMzi1>P59wu7_7Hh_H18=aM3K;h*F5JPIT^Keffap_65) z-1_LR?-dP9OllHroO`ZmS4GQUrCe2|IKw4al59c;Nc4o5d8P&55bi_3y>l2$H{=IxU=Ds_bNmg;&P{j*-K{ z=5H?nrMfH0f$pR}0jc@)WYPCt{dCS)-ftZ-DAh;2Z6&aaQ$*o2jW!=374J4Tuyj*Z_ z>M$(?ki2JZ9YoM#>pwF7;ZJ$8MdYUsqhcX?dhpd?lfrI zAF$Y_XbrlSn|&)0g80R}+gw|WpC~r8dtvQ&8uzh_2Zg}t)VjF=Y z|L_Cg&WFObp=&ok${x_E26&QI&`+Qrky)H;VGkQ)+FkjvNgU~d)hs*fn^(`LasHXn z00<>_!@K$Z=qb!BbGc3Z;R1mLlF9o#Zk0~cNs1g_+U?=aBf0S9Qb2=r6=wX=tflA*XUx28Dt+P9;O`6ujQ=vCgoAWJk% z0it?&^ir}*I7sy>1x@1s*^uv996_62m;{a3X&HTR4iD$`xsVXI9?>1nemJgimF}J0p z1^!4JUs?tKR8>N4?XbJf6xD_P+7B9_-^G8uD>4L#^ybyJHy6hhznc~9(8M=uEf0Fc zAJz97`xxu(lydu$S9+6J@QJE#b>ufls!cGZB0lEVfXSAaYS7``VUw@!4UIR)$8Yo> z45e+X7=&&hW*99}2ah|FefxX?-KW*BF(vOGm7qfET-lNe%0Jb<%qzb=D?PLt4`iME zQ3RP%!zb~gt)*CtbG~M={p}N~MqMcFDK;y`E1Kl_p3D3^0=_*^=7a}Cs3)rk?}n

=|?KRbOa3GMc+oYw{Xf}CGmYanLGHrIm%MbW|drSs$-H($QSv^ zAeRA^`Cbperv|7pA6Sfj;57Buip`?D&zPu46nm_=MBDai{~c-nva@L;arF;1Vm zljOmFX(())HmAP57AFF@>)o84EnLJ!DhFZxjQ5uSx~CuA3;kej^(0WCO5Yn7wQ#cc zU@UIPOZOwz!qYBpj}@S|Ka=o84BC$g1(kjtjnRC~utqGvNExrSD_$r84Hw>{;HdR` z>YE3q9McE%?&vYCJUT!8`Krp#591PQ6$4d92OY{AhrkA7^3(<6l^ zC3?}QeYg-g`-aFHX!{w_eqZD3*9WAfN@OMa><*E%(mD%vQ5A8P2kolGP6fcQW2>A0 z&D7UC@%t&Iic{bjxfXAb8ID08tjs-jnk0C2B9iqH>f?_u41rdoPei{;a3J}`2A_!|gnl&mYyyX5&Zia18zW z-WtF1gESlYd#BeZX&XCSw9WO7slL6JLxYh_L&uCW5AR+B9V*f{Gf9It&a${0dLXtJ zLHob0{>^jBXV3SUl^KwXZoa(-$%&(=1#u|3yUi;=HZBd{GU)E>lO#EPg=Jpnrci4K zEP1-hoI1wcBSC{=i8Va+#X$eJ2(0X@wu}8zlrPVwwy+GCsQn7M_JFS3v!|!0x#_SC z;Gu8s{HQQvkbK|?;re}hs?3ih$Z(T5o-aw`=^$^==UFxThGojyLg?>}XZxeEA*C|%YtEs$Wv~cO-5lJAbGugAZ9?k~Y*(IFSqZaL9aex_j}Q>paJThaEBU0_8SG9f zzZuSJ1b4-Fgw5kdLS-V>yC=Y;hJ)u*Q!J4rK&6*Z6Q)iR2?^f54_cxbs8UTn=4|fZ z97FMK4R?4*`R;jns-~D)_z5E_Zg~*FjV1dK^=0a^)NqeKwA;s>D3|z!n?@=%sg)15W9b9WwPIAMOn^67&^zKy_oe&6h+0ofD8=m+l}y0}5NO zUYM)yZl+lUbOF{i(fvzl9E&i&d;hJG;vEfk{JA}j+d{|4)bx1@^)Z3(AZPL7fDGFY zJEoQHTV?wIg|F@5SQ#G|{B^XQ#+|mq#mKF*2n95bB6$U)^=*-B<>fW-m36l!p!`4*fA=e3zr?8Cc68j?|pjn%98v{OY zV}_4X-ZL%Y7YoJb$6^gf0H8O$2B|`o3D%ApK+DS)V_DXgN5Z!K`~d;XSUgjYIOzBx zWBdy-vGgum#=?07h9kS@R-@p^WUiow~B>W|ACAM#*F~JDgm|eDH{ysUnAl zyLw(S*XOf{l_75fuRWJYvo0(-ED}UofgaplmY5LafNtB=v3*g$%ypQvlfvse(I2k} z$7ZlI1>MS5K^7hcKA{#}-3#nK3oo=LYq~-YRrm$Y6U%@8c@`>C+o!LudWttWHBt5x^ZPp7z)F}%CA-)E**CNMoDQ-(Gi#=$o$w%Kj= zNmioPU8HiS|BXRmj9qdRuLAx6&5tu#>9Na~#^v>fc6m@eJl-_5<;QU`m_s1*7XQl< za?29}%N}TeZOB(Mxe@*@s~0PLQ1@q)r0c5JcA$=|EcMn&CZ?-GIi|4c7JZiCg$ThrMeRE+vRFvy5#XI@62h$Zerag`A@n9G0 zo2e0tEP*sJXt}`o)m=gm6YY*yd<)TL862CpK~YWpfnkNs|2X0o7F?c6o zOPZd>oEf}j1{#_KT?OFq&4GR5?z*<)ooNi7O``sl5GLs1KF3exFo$54^`AILg1B8esm6EB#fMW zP10q3kt?TVFdsm^I!)p0m>&Kp-GY>nYk~2S27VLHrYr2KzdYBMri74uI$ZoRRsqWc zPVl+gxW#p$hY3M~3thUWst#PZdsrw-FY#%L=oi0a)nLC?_U*(P8J&_u0c0&Tf#lUH zLoRnATKWZle{OD>HZBXAfcR(fCoSREe&W1+0Sr7Zcm;9v0U2vIqtSoxp>?giGdUtN zj5d?(pfb-K1yS_%t-7Y9ZVxjFdg}N0VYp~y*ZAoP>k)^NgsM)g4Z1+2(=>S^a1Jzz z&NfdQqnrI))s%5w^89(Tse9I1()4o@q9RW0{?Oz^EWm(Fma=u7FNexEV4Y zmn`p=fd8HV9|GP-QodJacy9VT=Ny27>e}}2@mILe&}&)@m!4JI1{o zsRZ_YC2EDNs1)M>nn_*d&IQlTHyhxv_!IRNkBG-OC$}*cH^DNIptiyf^rV6Rl9}0! z?|HxesTW=Bl|MhL5DWSU_QwjIe*N80eQN;V?_xba9k_S6V=X>?^YEG+`^+}5f269U zGSY>Prq*W8_*x$s4k`OyY;o}PTfc7~kb9rDrxkx*1{Fj9teML=GRh@RFtgTbl$5FH zWyo9hubb(*)PJ7AFRYFnKRn#)rxhmRK6qNe8G$T&{BF((C&WCJ{I69{MNFBHWZX*@ zj!*?Z?D%7Csmi$bgbL(vTPJh~p$La{ip4q`uunRd!8P2EYP&9urQ2-l#qpPS$jAkO z{Wh1brW_LF@cr5A@+11`(*$CVf&%wL&`>4Ia3XF!5X6#(-!XdcECsw%T#~2V z%DLN};+GUtP+|50+e)C|re;^1!xe%Z&?sfZ$U5oJ>};~zM(==_;|oH8MajXcI#H+N zf1_H{poFN#aW7aNpj6x!g5kV zg#I8dh4&4FYqm83w||v{FK55!0)aWDef451=R8O2xi_|^veK`%?*|XP`=g5opUmQS zI)YKECeoTUHgfX{Ef-|#JsgX(L{%2*ndX4suG`L8>^E>oM7iv4csd7ZW7QG&Z8{I` z*Ha)@GA&ccj1prOFrVv4!_k+UybOQ`NL zQ%!4yP5t%n(@%8qyO_MLjS2p-2q4VSQpF)3?yLF`eOo_CX7Y`>b61hAy?4B2 zI(YNDTz~T6XN}%=9fO81u*pqd7Kn9;Gwqg(uSuL;fciF?F@KIOjLgk&7 zc5B(!>N=HWIt=5Gm9O%)dW!5cf&V^TRNH$*ZF3>nPjYXQZ}K^y+%?7r>>AK25GA^V zaJU0oz#;8I8-bWMcW%r%vp5*3`>XK{O&dA8S8x`VCO*@>!ePdJo}8E3^65UTUkXg&flxN#|`J91@oJ@03 zulsqR71Wt{Ox5?polCQ2g~i=yO`L~pN`R)CsLU( z@~0<`wHC8W31@T+*&KKHGjWKzv*19|LHu9>uf$b zu(5|ig+EK0ET6wZ+nIpq{81m5cQ-w~Kuz@IjikT07(ji3{QR=zyKaJtNK7ME7irzo z5&Ak6xAJWdA;8X1F$h@6}=EUwjtW&jpq1t`n%AT6t$1Rp*P7cI}&MSy|e@4d6-)=1hO| z1_R@s-!Vq7j;gbkER1>i-*Q9ObOq-7PBF^7-F59xE^0!?svn#4V)FEziA%M#Mh_tC zC5^}aYJP_BlRSnzJb5BYUez7~{kWc~ygciklBVkDSjD+JMoLE*qxR5e$qXg~cl##G z+NU=>Yq)M173KNYBmns%Ip!Ms_d$K8=G(gA^_d8`iPDYxc|*Q^&T`MpE?&X>Y?ibh zD|b1LYhE1AwV2LnQM+-Lib1oAb!qX77$ z=WV)q@|=du7r&QID8kPjrZsKlAd>lshgkFCl-nDFmhM~Rxm-QAD?s-}br4*9G~U20 z7wZwYhQeJhyBedP*ky7BAzcAbw$Ci%uG!K}H-sH@R{v%}KI0j0Q;@|txr^z!`sS;= zAs5LB>Eo!hSTc_k8g?PVE#!w#-|B~b?NiMV1oqMkos>?*w-3!MQV)!8fGpuZpqmm6 zjIG*_hI(Qe=X%0ci%N~o2Cw*;MzG?eDOm4EaMpt%e32Lzef`3zwF&F@j&Vw$P0ep! z#W`;lJ5c!*)h?=3dhc@gC0b*fUBWme?AA<^0Liy|%*p zXMmFNmt{?k!+Q&-K%3IoIF)ZTS}|wR$&16itQ(U#kTP~_l?gXn0HDlcqPuu!coy#N zo;MSS+ih;#VJOw9>=+-s?6Z^ckDd={YNT9?3_5W@gfW%Ba}2U?zGf_GIN-fJuur`$ z#U;jm1jhKv*w~QDCZ3m^cAP$M&CNOvV3Usp#999;QVBy##^LKu1=t$GRtOh!Xhyh& zDZZl5lJRG(!WAeJUozrHipMd#3mEJ0#+W*>&6(!`^Qsd*a2P&$LVmLM`3&CF)LIZf zTYAcn3xE+N1pTkj-Af6>--&*fhopJjKyY5KAvE- zy?>;}*gAC)Jj=rkQ8Go5wBb#gyNwJax7iUZ$1x%DQT_GeNcn@;d_f@8=TI!Yp`rL2 z2IKLtv9PD!Zeyt3&_-K7UA|R6h(^8f#()&!jjI#u`Se3~bb!5M13``4b!vSuIkg(V zw=t~`j{Q;JFoy62j(kBSud+-Fcb(6R+=d8$tEtNjOJpTk3Ub_E#(AcDVZi03T*^ zX)=_dyAur(7>Ld1SmBCG7fxXP8WwxIU`PZDvzt-}99|c;NUXB4&qkW}y?Xc_eWa9j zvB;ojB|Upyy{BG%?QEJ(h!J00*!0J^^dd;+Ng=EefC)%N*}Q&4=YsB-72!;*SmD|B zG}YwOrcyz7ulSguIdEkTv;P1{-ULu$L#(xU)!lv2i-o!_Jah|Z^Vz|!n>Tw6JM6#* z;3>c89$gsb1_%>e!Omm{0Ll=Cle_4a$MbJQ?7ze^{NIS!9eMgUME|$p^lym%?_2S2 zi2iSB_%}rVUr){d{~-F{l?y+(^Wq7me4~HycBGf>e=4Bav1X!AfQR&kXY}6`@4svu z31@(p`>)j`J0nSzg2(mAyJK{2+Hbot{C_H~*!dsKClF}Xf@Yoj$4d)_`X39Q{?`{F zg|6S)m=CL&2%Ir7G1&~A?#@XU7=4!VdX@1fNVd<{Se#hy0o|LL1nL5=oR9>&;5CgH z{2R^SxennvnEpk=D=R=nO~<~T^aSA?DT3XY!<#QpetDyzpOPhu35!g=Le!K1RSS2n zV%X^noPU)-*-gZafPT2UjTp{eFVdC^P|sgE;&VK(H!9WB)>z4 zrLzK9jtnnj`O?fC;&L5!O_5mX|WwOqmhmwAWTtGDQRAw|*mGIuG>cNVldIaJqFYP+$M77(SI z@DTx}B*zYA-)eoN24L`asyM}f0* z%gObzZ(_w|CNsPNjhhw%Q+Jx8U7}f;tNZr`^9!oHc{jJm-XqM=m&ia^21uIhRujTQ z^`~UU0n~^Atwn;<;_Xb1+0lyisv^y&tYuYFhEYixRTs zPicEtD}vGX)7a@+cT^N<{Ao?&>)N)4Cv#+cN5YseJH#E@S_FbV{w4dMyzNiV(go&t zUZO{2VK`{Fvmv$6W~8g$l_0&Tin^ezSRAcgZijkzJb%o$u-vrWmTYb9nGAJyXF>OFMT=zOk zcjp-QEr>wnMkYKsMg}O5reka`Q`|BT(KUoB)$2{-ulpppdV{7XLQ+?*(?TN%YbX_B zm1&O)?X(JM@a(ZJ0iNsS3obBO<_x(BpaJQ#7+%r~=i-3)m{60B)JbwtG9b8}w4A7?tYZ))Q$ zbXvHdc9}^9ulkOl)lpuX3$tUDQBb@po|fdonmTqtm0~w@Pb|n;1AVjngliTy_F8gi zPW954ysUyIOdY%-`iJbOa^j#7Mz+59PNl^}k>T~SrSk?%b9LpE2&;9KKF6;2Xci8B zA6o!VIhy;Z&WL#OZHb z4<;cCsk28fCp&VK!2IbajKAmHt8o zj-9QmsHkw87WomMj15&N$NWnlC!n%m%C~JdAHYsJS`}?i z&X?VgD|oYIma5)2k+)WRwA*RKsB_^mmPUNfAWGEsT}xYEbHO8EB+JBGe$J(zc1@3o zRCGAzuB26aoGP7pC@YbS-R{`MvajwD|B*mc*Q-|f8RkT^H z^TP+&xjM050=J0EhjTml*4@jwRzcl|Cs5xC@+wss`d@M3n`Gfx(ZL_9FP8%^H)WZ9 z4b!>VU%Ozl9y&O2fKv9N{by$Tmub?nL&6@cti;W?p~7#gW50~t8`vLA3$ZMdYVUM- z(&03{s3hm=m$*PhYZIq)v$ zE88@Sk$2#2+|FkWM>Hl@%}L&G3A?Z>RK%~eb?BhkD`bUBy6wznU0*WQRabxg9=Kci z_OO-_|3m7Q2R56?vURWEvLMIz+cOY72hg8P za)!y|kVhAMAK^*L_ge5xP>gVZS|Kg;<=`nq8yc#=F<*#`Mm%4`GSO_O`e!KmWVOz- z#N0(;39+{tbE??5UiIwDw%eFbH_P*d9=l$AjN4V-Cq9iY==K+wUZhc7yJpO|upPa2 z!8T4s5$&@hR|REtCUoxZsW!E9ELdBxNg@ZX(-^H4{U@u}5^D_vJB4nCZR~}vdOMt= zQ+1j$VE2og*j*Q_oVZG+#)O@%I|nXJ?N^@M-|X^Z{bT5H6yDv9^~R7%R*7&YiMB01 zNwS4|%2s8d+_rOuZIy}d2AlXFZoHYUGNG1d@#dGiq%)Owm}~%6Mt|e%$L{cwR<@1L zXrIa-k}#`yOQJ?P%?bs80Dc1r#{hlHAw1uWR>0-O`?lsyhhi_aBE7Ik2z$yN_7#6m z7PF9<^0&+abdliz(1IjZJ6mT4Y%bK!-}Nz#*luPLQ7SIYxq44DYokN4hc>Y+hklqm z?L%l0ezRM>5A7Y>ebr@TuxKeZXizOj7DLwlxwebxe07tGjHgt9kbSZc2C_CSY?Xd+ zH@@O^ddduSBVB&xTMa;%9#$fb{l}w5m_O~1DI}VBGLpLiy(hPoS#&Y2FmBxVSdw_# zYD#Eo7TSqoA_Rn-_96)tHX@ozGnu7>k}xo8>;f!sFJD3W)p94?x#|fS=>=jNFABCS zb3!?|4%(K`ov+f3%(RsIIKm zQNFmW2_n}2E(!9PQ|CRAcdG^9HRUD?0)^Q~W8&V!H|k=z#g1$oSUwD)Sz+pmzPLZi z;~VXtKaObRX3A%jUfe?yboV7z?|vgEQqP}iRe|WdDEN3WqjN4CC8;meMM2Cv>hSc7nEbG$)=iTzgYMDw-HH76OU6YZ zD=za2;XmBITJ%u)dw!m!shG~w^y`Y2vVW7j*nb}bRtd62h(6s|4Ga=YAcJ25)aHeP z`7b3d0{0hm4|I;8z;({x%cH*O%1bC>4Js4PViaLd>3h4;rPvEwis)``J;3?+i;(O5 z_aGVKvrYNTtEtr|L_7`v>XhLOg6hSawRu}Yd5O@lD`72~*z-P(6QWTNRSRA)aK5pY3*@BR-L#OEkyanv_CQIgn(;@hg%3TH?8QSnG)tooNx z`9jEG(t1hB^1$_Z8hm8d_KE8=(IO!h>?e{Rumi^0yS7%SQ$(jH!y|?fRmQ$4EKsa< zu4Bh#)?@c%VTd79sDUN^`|0ayhk{q;Xy3mz#`Kv7{8F#2?Xu*GVq=nX-b!tu6+wyq zH>KZ93S_d+N^usif11A9vnJVQmUioOe%`|5*wPM52Vnvf^ZeIsg*i1apU_y8mZo$iI?Mk0XFf%NFie&A(!B+`uhU!rcBxb@$HKGj{y`5p zbjjTv_Z^0LwiExZTFF-a=VTcel|W(oIQruOI;|yPn8wJ&%DvPDR|{Tt|7h|(@Yu7E zyedy!0*A{#7Rw6?)iD-b&xk!>p4Kv-*XXAsu|tdTWU8eU$p$DIY#ABoa(8GnpqF5% zGny6f14}Pn;i1w;BEma&isdtpXX~VaAp#k_&e2aAa3 z@#St0Vx3q0g+G|1f&%N1_Y5-DPibt zq&r2CMvxGs6%ZIgxXB8$*AL zpk8%PL3lna6G0SvY}bQQrQ076xDRoF)TCo`Z7U$;mE8YW;OKGCVbCHFPtoOWi0P=F z$9Dq|v)%i0E@AO(=`;j*uw>?WG}K>tm*_`JWj-@LgOJ`7erbg@IU&8gREo0z#OqO{ z)Yni_XMWH@$X?wg>m$QOTB=4g5WRm(Pb&zuOT@6MXI;<%AH$;8wiOiXverLjLfPK> zL7!sbdDWm*Tnj8s{Tc@nN!nPb-Q)*Ngl0`(3FEgQFoikV&Rc=RkhT25;{SMv94x$7 zf19Wd`ugdz#^T?gVK$Jx+RKNm%=q5{RDn>g3j9}|P-0Q(k5!lJZblmq>O&B_``@;` zM4oi$k@s8B|Ggw34t14+`eT8x%h&o5ZA0s_MV06!Sqkftb>&6(3=_3$FGcVaZg+2n zZVo>uclK zBV_aBz|oa}mLL*BM%IHU;}zYS99(0Pr;V6$%f!O@U*!!UY(>^UYuIX3{Q40V+O46@ zEIV(j5KSMp4+ou~fIkwsC>^&hY3wN8;~CSGM!O?VkBfw8%;4*#J1&~t20kO@z$T8 za1B=!h90baG5LMM=-c)}9LS3b-UdT_Zp*u*l5>2ja4X)AyJtTgugC0Ly_7ngAfmhvxfU?6qbry5qY! zE|o$sf#UCz{AYD7b7xC=g0>++0mVTD|3!C-E?i+CGU{XFa=EIhfTsP1tSO0mKjwb# zrh2E*#1Ckzo8;xJBfV5m9$?5 z=2PPkO2Pvgh!qz}S)48D*I<@-ofuSbtI>EBl^mdr60caI!!*)Nv%aXO1 zExxlU^3M}nqNG@#reTAC^nVe~FC+ik>A{ z5K{m64*$IyJ5M6F)Z(8isD-*(O;{%3K64*6P&zV;C&J;p4)+@wT)4GWi(u0Ad8k5@ znjhXC)Y29)#78hzEeSRQ9I6jdQ@iLmZq08G3i7`G$qu0%EI-aof2`B`Q{>t+ju5Fd zBmb=IRF~^VGZz<|Q}~}gsGYU%?*G^z*9Zx%=fAh7WofBPLe5m^F01llFZ!eFz(TJH zMXP*gL+I?cZaV3~A0%b@QeF6#U)-?-xGmze{P5nzkw{{ACMPfZ))S=|xFn2y)Onli zZ7Q~WFo*T6_fhY5ZSS#%y-)AMhLT zfAF=$u%2QssKj`ptQ^ni{j;j8KOWK@#WRXe0|WY?=awE!K&zdW<8}|D3cp4CxUqD` zBd`B?U}ujhdcpQc-+jR&5qlFZ3`U?+fO(Z5=IU{x+ok1}E6;Zjmg;E;)z7g!2d$V!Zm7*x{&zXIJApA4IlziLB6aGcI~G zx)&9S3F3V9Q-lzdr8iiTqMr$!;?MArXUZgXM2NgC)d&ptqz{(M|O0D=>|IWsT!6?3{=l78I*jlcAz1WX;lSVPbS`nMvIV6*@>(8 ztbLX47Z(ON((&aVJT$%HGq}yR6bWO6#r-#1(riM22`Ki@m!SGuXqx+EWpARnlf6SS znq3f0z$Usb;|srcZj2a7GL4b#iW7=LRKA_j3)f2jyzhuOTU(E}OUaIF(~-sg(Dnc! z|BpHO-z6z3!`S*3?1v!LVdvnB)zG!5O-#JI#-t;mU+350QD#whsAXhWY#c3;OMR<8 z{CO`hqu-Me$|x~R-#P}|*;(%$^?t>|wRjr)KsJ%31l`Ct*Y5VgFp7g{d5hcWlzp@( z3j)UAx%KC%b>xqWMT3l?#o?@HR|x@D;IlYpB_^8YNs{vm1YVu{J{pFdO$oq6W_`flmVvlc_ifq#c$Pd2MN$^RBQIZ{y~o{v9U&D&v_15|jS}Mx z@rv7t1;XdzESZ+(;Ova!7PTI$)FT65=1#w&Nc!EYY}JP_sEW=M{vq8CvWn0X6FVV9 zHiq@qOWqm3fvudGeuHuAO*G%3-0Q^k7pl%i^YQYqEVDWmsy;p;F;p6JAzo<&U4zV{ zTiybH(ihEAEHXSdhw|)q?nCg{`gZrav(5@?gx?SsmtnH6ug|a=Ya4h8cKY3qxW$9= zD4+a9B^tTVcQ&$C4|=G1TT~;cH5>??DE)`m3;53Wu4m(okE1)6yFeLur%36k`b4=4 zP!}9}jPh5rDu+!$l|k{T9=X9=@uNJ?q7vL#|8~c@J3`Ft=UW-%`MgVB(dzP?jY&@K>vjdF8A3$OeUf;f|wc&qFVS{b+lWge(F!!HRweQJCrep#1*lmFNs!Q&Y zndicF3|w&tTy*j%MaQLF#)FNaMC~UZ%~E(WpM>LydB?*QE*7~Rd3A``gu2@uWU*T) zxcF_v&n)Kt)bnth2=H6iX=1PsBt;Xj4)}k8T}|%RJALXJLix=J%OrJd+(NP9C+~|V zu)&;r^{zdV&Tgw7xiyPmNp_0dw5_U52di@U@=?^Y{NZj3X^)a-v|>`paup-y z>B}Fby3VmYG=~=vk+8v|qdaqKFAK*ub%i5ls%HwBvU*pJGDIouOMz`EAc~Z%zcj9x zQfPg+Y`n=b0U00_5E4ofJ(}cu`IZ*=6=~@=?x57~M;riP43&;@9}gA!n5?a>{Q#&9 zKF1$C?PU2i;JeARlfwDVBYmyk@zIJGdYt@DrMR~fC7NIi?Z6Iub>$1?P3$Rrzw@e>SK;6_s=-3^BV zq@oK^`RSF$jbO+u3hK&{`W>uT4plZLu~+8Yy!M*lOopo{YL3!057 zj63*9JY-U^aU+#k!pgL#nRkdhwzk`^H%na{g#?EIz2HKU+CNK4O?z&ftzw|MyT=?B z_AF*@FixH~?aPoC*fonM;smztaK>0zs{ z=ecTm3SiUzItKskb?TcfOG-Q)E{TnxlF^K-{&;TIUD$b+VEw~5C{VA{pW8|odG zHTVS2`LnY>0M)d$t?RaonIhY@dWRFLZ}WAb z1b`nI&j%HOmFhE8;T1j?lgnZhj7-(Sicq0#w^b&@`FcxmQXApM=1_RJnHh}~7Y^hp z_Kq~lb~23!f7AxUx9FF5>zkJbEG9QRYjw+)n1d*EoZkOg*SoOfA5$FR-%aE*Q@S6l zY&#Z>E+5Y&aLHHcnXqd}=K0`gZS(rF+MYQ&Yt%qRMdkh!T~K;$^ABgvtL^ zbuYcHZc5?PgZ?mTA+AkPPy!;XqNhivpq1Qy!)2mXe4~CJ6e>aTuz1V1+VYScPdNDE z?rBCJmdoMQ8ncvk#&|NJm1^tBLIi9~p6z`vdrc%ZI_WZDBXO6Zs%m$*Mfd2qneKPl zSmmnulklV2rgft1mnEi(Q6KvFrUAHQb{nu*i5cm&RcQPdY{&rGK z@|fR%dvBjfXQeRIFg!dQ?vqu2-f^@2v{Tu~@bYdd0V-nO`Rj+Ejbu zKN2jLG1Z+bS3$hejG^f4%su8?x;-zMUrMTD*AbO}qoy-``owiKWIb^s*WtW;!q%#k zQM-FifJgmK9jMBFNJPDwEED9u{@ufX7)x z!x>wF9Dq(cv*P#?OF}&1d%mAa@1BlZJ?F@&!aKX|dr|WT@RexuHP)eaMJVRj>`w2*xNYD91G?DWs&}*1fH8=nKXx5tHcA z{Z}ff%!-L*3JcD+nl7;>O0rmRhrW`7d#zu3tBq&`mU5@kwv$7I*B*|kV;>8$^@GBV zVB68aw*9kP)Ila^sju-dE=S_V{~QT${}8VT;-nP6cz`y0$+;LZp|i{!bYiC%CGcFy zrof~2{2Wa3>v85a!)m;Zbp|7!6}vaf0!7O#xa;Gp*Wne+V~?XrC_9hpyAEYYH?28! zc%d;r3&(EZX<7OJhl6GJ0RflntJCw^ZJq6SRK}9x_I(2oGn!Hl;*frrggEExZ;~MF9c8W(ASiA{? zJ((jb)Qvv5PP^j-&iMC%`nF~KagEXgR zmIhD4%hUxvOw98P^$yPC$0i8>3M38NN(c74^D8Jz;NhQnq}`Ye1~s=#2fJP(MHB&R zkA3#Yl{3C`qo~tQPz1^0`b&MhVpKO#bpGp?M#u1;6ID(?? zYYL%?_ZiCsT#}#{*2AY>b!eSv^{DiP-v;O~K7IIgJA4YmSnqjTGY?G$mzc+j9}e0? zR8;y!6)z*FhFRAUUM9@aLhTs!GMH^utJguEUXPm{6J@EZ4%TL=@>JOkh9{6W1ZBN? z^1mG|xTw-9mWUqh`1OB9AAEO{Z8+!td^GP@|6tcCibiqyzABLzP3ln zzJNM{AGdE+<>BBjs)Lwv6DS_pA1oFA4u86mo66p@Tux96csEO+mfm>0Ta6Ej8#UPS zhT87zRH)&PVw+6WJZ3D!VS?Yuo~zT3Xfx?p^l+4+(p3Y7t6Cw^NkuL@m`f}`F73o| zqf|!%H^E5}hWlGbwL6iZsPp|zkrY{*WJT=3g+1@NTVUp0L!EgD3_+@*QS5}5C)yTA z#-41g=L61-iiBz``osB}RLGUM{dLYd60`ynIqa3|)kz%|8HJthSy@88iN_Y=_0wcE zS&N$<^2sMIHF^H8I?;f)$AD&2=2*P(w?uauik=Z%hkLFKxYWVbd87pDT1O^M7lx{NS?Z%B8m8#k_)<%kX(*_&Re_vhtkfwaOSmJL8 z`oGqWA}=S_Stv>ExmA*M+og;VCS;H7P?MP692%Z6lf(XzDlYzV37#c7zslZLGdnN^ zlb@Wr;RCGB=9!In{8BW!hi74Mo|PQI3fw~j2Kh~(Hro4ztvC(x+6owcHuXx6H`kM` zhud>H?b6>?9`{*~qWTyMFu{JC)8p`Z;o>bFwSii4&N?|vz!V;vF zQBd*oqgIws>qqc>i1ot~GtYJSEeQLA_-fwS62Xt@Mrep+y;L@(c!IuOwW4P%l-l}{ znuEroWz!OSqNT=q@^c4S596~sD^F5tJ<@7+nH#Wr%RRogE+`4~L9|%doGPk}q2;^k z_7db;8=YN#3wOh+4!aK+#-s$ORcr33ICAiOgA=@)(4w@VDyZs%dnp{@|W6YCDMk$MDzl*^xS1V#~y*PYLe4QCd_g`=9=Y4tNU0FSaKvXxRw)s z5%cmkwtu_6s58GKvHN?Y8x=~hNeIlCXLJpXJGq3)1cMurH!8$C$_D&4|5= z+}zx7v5bnfT&_Y~A4}&y1xloSJU)p zB%HEu?Dtq)(z@en#LdBp^XHjQunus*H7n+qs46NZ{OF`O#9w~cw}85u^No^T!AQWS zD>{&X(F-!^l546KOSfi^mXv|pQn~F*jj}T7YpR2&?ZQjId*ft?GW?_$K zc@S+x?_^wL0rN?75Rs7l#-7(uc%So>MK1UIt(rKm$c0S^h$(qsC3j6DSrzzaE>c9b zUNzsqox&}E6f#jg3wW&*f3-9E&d~QlLuj1Kw|-1IUkzQ0CJN4!DpJTWtNrC?H6=pFUs+ub+vJe8gW`1|O`NZo`lj&ObU{Z7slEQUg zO-;>LC;rU8#>O?xlF1qQOW9`uXmdKJ&p;zpnRfe79Jg`@NWD>awFbc99pzeSeB+?2b~VBVjhj{)!9 z{MOCYB*Vvq`J0c4cXB~P2I8|UGJ`AT7%Tc(w>U>XU7g<8N{cNWjuCRl9sjZNTx_vA zQ;w;BIlp-TJh+7UyReut2M7P^(86dL;9hdPvbMCuQ-5GC{f6W=J8O>7S*e0v9{r%6 zO~X^&&0lRbwY86OGU;7u8gg(e%Aw|STX=-*TxYJ92zKm;tM0;rFD4jDL!b@iQ!W#; z4siOu@}Lnt->DVNZ^Nz<0yl>Xbf|x8c&kJ|^hI{7r+y7&JohUoE~DGHq)~M2$~6 z*ptU~4@QR$I)nePTsEVN+!A;{2=i9^JOehRuUmr3SU2x*mDTY?%(PyNLsCfd`DS{c3t9s>brljvj?Zu2;+7C-^a-98_bkp!? zI!n31mEQ5;^jP`=HnwzQ*}YZLRYSE52IoaT^+&A!X@Sy~i2V;~1MGy!l2M#geHk`{ zR>O$9xkxlL!V+022~|d074lH;t|Xp$y{a(2ktl*$5mc^qDn(H{e!Z!gX-yTBW3y$r z#O}Dp5(GQAFhIS0-Y;19e3NDQm#%X^O)c zitQ_Ok`d$5uDt&eD{YfO>rHw~=*btUx9X;qn-CCIpSn)-z-47P#(%fw9WwgYIZzoD zXmU4p{aZL{j}8;kPfXqzth%oTef9=of%5=8p5VcJ7+;trCYfjG7&&%vq!m8I`{3+r zxo+cP>-4tQVWcrsOrVP5AFqLiktC7k{yngHqiyX#ZOD3m<9t&NSswQmYRNlWicsPU z4-c0nLX7w6dwFU-&TyZ8w`PGz;W~*}E`H63x%aLUjuHZn-o`jz=zJenW+ndZX!`q9 z!}pt;p`-J^&2gSK!a*syv7cQiTlu&ane1kRnt%XiU1!X^7d60jQ$^K~YoKJ$pWXM* z8XvE6x$vA*XmY5T5%=i0gB2Qd?TFL=g&cOv1{)a9obtd+cIjl0>u+IX0?3L94i6Zq087ee=7Hx!KC8Jr!x5 z;Pj??xpnAjON2uv)mR9pnVfUyAR($y+vBjF^6L&m$ z+T!BtIyM#cL->tVWPcRF3erd_5Tzx^Wp?0b+_y1x<-tpuMv7+K4|2R|&PxjO+^{%G zw;E~vf~mW&@MZ$H@WC(FQ>CJ&Xy`FGNtrk1WbWFH2FYlnkuRrM-L2WuigE)9>pC`K z-%SC8py%ORnG>I&vq+lF_W|;rd=ZB3H#_|dsbo*C&PJb+VDyxgiSwnn7OdwBxfOj) zc+l_mUdktp@%D7iaM4L7Xx4{9Y9)s=eqm(uw;# zmFKS>70c-o%|Bg;QT*+PDTpj_N5gnSvH~)Nr8Ay(d-JedEtvRx&!?*Nh$ra*_^Xbx z*nv*7I9CB&niH0mrPaE3Z&CvBs3E?JdnAylUHl4Vg!i=HZ^!un7(LJ`=NGe3bmv1lB2E~4DQI8oBsn`!|{_!F>k_7mf`t78{ z30uBhAyxMI`6VQsnsnxb`@w+~97oI4$u>WW?Q4(O{I-$H^sO%wAEZjnKT41u~Z=)lwb`l?Qp@=}-Y>)RH zg)zwO>$KMF?O{AwdJQj3(q|0F%q@B0BYJkHu^b}Obh~HIW5dIb0*mFn1x&$2bvAy7 zda;WwPU+x~;z4*-zKW!NBbtiO`5)$Q2g6g9r15v3QTiWWqf0o1*$IFg?pO5FQCbE! zHG>TH>1=RNFkSq`?CKSn81+ffb>(d~U%S*a7AIHhJU8g-6`PQ9ovsSxU$Gp82;b!7 z-7GPqMhp)>beg$%434UJ4Azw?=fHG+`~2>ce=GqV;_&~@cy`T_h>yM27EM?_>32N| z>-fc`9RS_NYf14MXj$r+I8MJjo_5^7zuiVXa%d~{WtTr1{R_{}-&a={q)9_D({Us3v*vr`e&A!qskX z97k(L%diTcJf)B)9M3oMN~up)=LZ`aMFSCT7lv!u9j1|Tmecp&L;uQ(e(#wQf5&%H=J=WvZSI?>rUP3Ly;FI}fj!mQl-R}hO@)vj{> z<0YWMxR)o^JEGgVNTLgLYUes%UlpH)_srE7=WRvKX)X0sb(2#OgoxdZlB~1h_At$o z-7epnTTmGsuQI*I%_ViWH9N&3jG>)`qBK{sU{-SUBw|WSGt48#u6{DXcRU1~45; z7#+RM{#oRPtGy+d#}|MhS>c3y=%pV6vh3C*baW_Zj`Z3X=Zo<~mbO+k<4TZvBNoF& zs?3Tq$X$_5GDhr-noZNNsTa`4^qGw^bnw*E3BBFc(D3333|_$*y9$_wZ7vu0g};zV zmz*j-1C%%I{??-_bq<<;0A8uWr%Izow5eV- z;W$VV>`HTTwq5Kzo-fpjJtiMX6+f@xZ$;yCKC~qb)lnBUYKtbeB9mTW#0)W{Tt&V7 zOqA3-4?ZQd&m5XAkj5gE*lmh|*d!B~KJVv&mLe|e+&BTPrQzd(?5~@WAbd>B4T!;-@o%2uZv?c*3UnKh36ppz z@yDe%0XIiP5#Thl-eCA=cKo*#(wz*%Ju(WmDCgsUKY>yL0}3?w@D8O0?Qf(0kMN=h zIvAKMP~PsZDv+K4L@(d(%e7n~-u^WXP})m@%Z(TqiooUXC&btwac)4#WO#Lu{I7ne zj|5HqTUht^6P(vTb8$b6ga;)|``c8M3~0)|WkLPQ4gc$>KnXu%DCLu2$}3OvuUN4o z^HRZM=)i&EZU27qogVZdL8cUHS=Qg>X5l$#ik7E}{NMZV|AyoLhU32-#{X}2To8Ti WzbN;dAWlRBe`KYVqzWYU1O5xO4e5FS literal 0 HcmV?d00001 diff --git a/formal-models/README.md b/formal-models/README.md new file mode 100644 index 00000000..9c700e0d --- /dev/null +++ b/formal-models/README.md @@ -0,0 +1,141 @@ +## dBFT formal models + +This section contains a set of dBFT's formal specifications written in +[TLA⁺](https://lamport.azurewebsites.net/tla/tla.html) language. The models +describe the core algorithm logic represented in a high-level way and can be used +to illustrate some basic dBFT concepts and to validate the algorithm in terms of +liveness and fairness. It should be noted that presented models do not precisely +follow the dBFT implementation presented in the repository and may omit some +implementation details in favor of the specification simplicity and the +fundamental philosophy of the TLA⁺. However, the presented models directly +reflect some liveness problems dBFT 2.0 has; the models can and are aimed to be +used for the dBFT 2.0 liveness evaluation and further algorithm improvements. + +Any contributions, questions and discussions on the presented models are highly +appreciated. + +## Models + +### Basic dBFT 2.0 model + +This specification is a basis that was taken for the further algorithm +investigation. We recommend to begin acquaintance with the dBFT models from this +one. + +The specification describes the process of a single block acceptance: the set of +resource managers `RM` (which is effectively a set of consensus nodes) +communicating via the shared consensus message pool `msgs` and taking the +decision in a few consensus rounds (views). Each consensus node has its own state +at each step of the behaviour. Consensus node may send a consensus message by +adding it to the `msgs` pool. To perform the transition between states the +consensus node must send a consensus message or there must be a particular set of +consensus messages in the shared message pool required for a particular +transition. + +Here's the scheme of transitions between consensus node states: + +![Basic dBFT model transitions scheme](./.github/dbft.png) + +The specification also describes two kinds of malicious nodes behaviour that can +be combined, i.e. enabled or disabled independently for each particular node: + +1. "Dead" nodes. "Dead" node is completely excluded from the consensus process + and not able to send the consensus messages and to perform state transitions. + The node may become "dead" at any step in the middle of the consensus process. + Once the node becomes "dead" there's no way for it to rejoin the consensus + process. +2. "Faulty" nodes. "Faulty" node is allowed to send consensus messages of *any* + type at *any* step and to change its view without regarding the dBFT view + changing rules. The node may become "faulty" at any step in the middle of the + consensus process. Once the node becomes "faulty" there's no way for it to + become "good" again. + +The specification contains several invariants and liveness properties that must +be checked by the TLC Model Checker. These formulas mostly describe two basic +concepts that dBFT algorithm expected to guarantee: + +1. No fork must happen. There must be no situation such that two different + blocks are accepted at two different consensus rounds (views). +2. The block must always be accepted. There must be no situation such that nodes + are stuck in the middle of consensus process and can't take any further steps. + +The specification is written and working under several assumptions: + +1. All consensus messages are valid. In real life it is guaranteed by verifiable + message signatures. In case if malicious or corrupted message is received it + won't be handled by the node. +2. The exact timeouts (e.g. t/o on waiting a particular consensus message, etc.) + are not included into the model. However, the model covers timeouts in + general, i.e. the timeout is just the possibility to perform a particular + state transition. +3. All consensus messages must eventually be delivered to all nodes, but the + exact order of delivering isn't guaranteed. +4. The maximum number of consensus rounds (views) is restricted. This constraint + was introduced to reduce the number of possible model states to be checked. + The threshold may be specified via model configuration, and it is highly + recommended to keep this setting less or equal to the number of consensus + nodes. + +Here you can find the specification file and the TLC Model Checker launch +configuration: + +* [TLA⁺ specification](./dbft/dbft.tla) +* [TLC Model Checker configuration](./dbft/dbft___AllGoodModel.launch) + +### Extended dBFT 2.0 model + +This is an experimental dBFT 2.0 specification that extends the +[basic model](#basic-dbft-20-model) in the following way: besides the shared pool +of consensus messages `msgs` each consensus node has its own local pool of +received and handled messages. Decisions on transmission between the node states +are taken by the node based on the state of the local message pool. This approach +allows to create more accurate low-leveled model which is extremely close to the +dBFT implementation presented in this repository. At the same time such approach +*significantly* increases the number of considered model states which leads to +abnormally long TLC Model Checker runs. Thus, we do not recommend to use this +model in development and place it here as an example of alternative (and more +detailed) dBFT specification. These two models are expected to be equivalent in +terms of the liveness locks that can be discovered by both of them, and, speaking +the TLA⁺ language, the Extended dBFT specification implements the +[basic one](#basic-dbft-20-model) (which can be proven and written in TLA⁺, but +stays out of the task scope). + +Except for this remark and a couple of minor differences all the +[basic model](#basic-dbft-20-model) description, constraints and assumptions are +valid for the Extended specification as far. Thus, we highly recommend to +consider the [basic model](#basic-dbft-20-model) before going to the Extended +one. + +Here you can find the specification file and the TLC Model Checker launch +configuration: + +* [TLA⁺ specification](./dbftMultipool/dbftMultipool.tla) +* [TLC Model Checker configuration](./dbftMultipool/dbftMultipool___AllGoodModel.launch) + +## How to run/check the TLA⁺ specification + +### Prerequirements + +1. Download and install the TLA⁺ Toolbox following the + [official guide](http://lamport.azurewebsites.net/tla/toolbox.html). +2. Read the brief introduction to the TLA⁺ language and TLC Model Checker at the + [official site](http://lamport.azurewebsites.net/tla/high-level-view.html). +3. Download and take a look at the + [TLA⁺ cheat sheet](https://lamport.azurewebsites.net/tla/summary-standalone.pdf). +4. For a proficient learning watch the + [TLA⁺ Video Course](https://lamport.azurewebsites.net/video/videos.html) and + read the [Specifying Systems book](http://lamport.azurewebsites.net/tla/book.html?back-link=tools.html#documentation). + +### Running the TLC model checker + +1. Clone the [repository](https://github.com/nspcc-dev/dbft.git). +2. Open the TLA⁺ Toolbox, open new specification and provide path to the desired + `*.tla` file that contains the specification description. +3. Create the model named `AllGoodModel` in the TLA⁺ Toolbox. +4. Copy the corresponding `*___AllGoodModel.launch` file to the `*.toolbox` + folder. +5. Open the `Model Overview` window in the TLA⁺ Toolbox and check that behaviour + specification, declared constants, invariants and properties of the model are + filled in with some values. +6. Press `Run TLC on the model` bottom to start the model checking process and + explore the progress in the `Model Checkng Results` window. \ No newline at end of file diff --git a/formal-models/dbft/dbft.tla b/formal-models/dbft/dbft.tla new file mode 100644 index 00000000..e291ebcf --- /dev/null +++ b/formal-models/dbft/dbft.tla @@ -0,0 +1,379 @@ +-------------------------------- MODULE dbft -------------------------------- + +EXTENDS + Integers, + FiniteSets + +CONSTANTS + \* RM is the set of consensus node indexes starting from 0. + \* Example: {0, 1, 2, 3} + RM, + + \* RMFault is a set of consensus node indexes that are allowed to become + \* FAULT in the middle of every considered behavior and to send any + \* consensus message afterwards. RMFault must be a subset of RM. An empty + \* set means that all nodes are good in every possible behaviour. + \* Examples: {0} + \* {1, 3} + \* {} + RMFault, + + \* RMDead is a set of consensus node indexes that are allowed to die in the + \* middle of every behaviour and do not send any message afterwards. RMDead + \* must be a subset of RM. An empty set means that all nodes are alive and + \* responding in in every possible behaviour. RMDead may intersect the + \* RMFault set which means that node which is in both RMDead and RMFault + \* may become FAULT and send any message starting from some step of the + \* particular behaviour and may also die in the same behaviour which will + \* prevent it from sending any message. + \* Examples: {0} + \* {3, 2} + \* {} + RMDead, + + \* MaxView is the maximum allowed view to be considered (starting from 0, + \* including the MaxView itself). This constraint was introduced to reduce + \* the number of possible model states to be checked. It is recommended to + \* keep this setting not too high (< N is highly recommended). + \* Example: 2 + MaxView + +VARIABLES + \* rmState is a set of consensus node states. It is represented by the + \* mapping (function) with domain RM and range RMStates. I.e. rmState[r] is + \* the state of the r-th consensus node at the current step. + rmState, + + \* msgs is the shared pool of messages sent to the network by consensus nodes. + \* It is represented by a subset of Messages set. + msgs + +\* vars is a tuple of all variables used in the specification. It is needed to +\* simplify fairness conditions definition. +vars == <> + +\* N is the number of validators. +N == Cardinality(RM) + +\* F is the number of validators that are allowed to be malicious. +F == (N - 1) \div 3 + +\* M is the number of validators that must function correctly. +M == N - F + +\* These assumptions are checked by the TLC model checker once at the start of +\* the model checking process. All the input data (declared constants) specified +\* in the "Model Overview" section must satisfy these constraints. +ASSUME + /\ RM \subseteq Nat + /\ N >= 4 + /\ 0 \in RM + /\ RMFault \subseteq RM + /\ RMDead \subseteq RM + /\ Cardinality(RMFault) <= F + /\ Cardinality(RMDead) <= F + /\ Cardinality(RMFault \cup RMDead) <= F + /\ MaxView \in Nat + /\ MaxView <= 2 + +\* RMStates is a set of records where each record holds the node state and +\* the node current view. +RMStates == [ + type: {"initialized", "prepareSent", "commitSent", "cv", "blockAccepted", "bad", "dead"}, + view : Nat + ] + +\* Messages is a set of records where each record holds the message type, +\* the message sender and sender's view by the moment when message was sent. +Messages == [type : {"PrepareRequest", "PrepareResponse", "Commit", "ChangeView"}, rm : RM, view : Nat] + +\* -------------- Useful operators -------------- + +\* IsPrimary is an operator defining whether provided node r is primary +\* for the current round from the r's point of view. It is a mapping +\* from RM to the set of {TRUE, FALSE}. +IsPrimary(r) == rmState[r].view % N = r + +\* GetPrimary is an operator defining mapping from round index to the RM that +\* is primary in this round. +GetPrimary(view) == CHOOSE r \in RM : view % N = r + +\* GetNewView returns new view number based on the previous node view value. +\* Current specifications only allows to increment view. +GetNewView(oldView) == oldView + 1 + +\* CountCommitted returns the number of nodes that have sent the Commit message +\* in the current round (as the node r sees it). +CountCommitted(r) == Cardinality({rm \in RM : Cardinality({msg \in msgs : msg.rm = rm /\ msg.type = "Commit" /\ msg.view = rmState[r].view}) /= 0}) + +\* MoreThanFNodesCommitted returns whether more than F nodes have been committed +\* in the current round (as the node r sees it). +MoreThanFNodesCommitted(r) == CountCommitted(r) > F + +\* PrepareRequestSentOrReceived denotes whether there's a PrepareRequest +\* message received from the current round's speaker (as the node r sees it). +PrepareRequestSentOrReceived(r) == [type |-> "PrepareRequest", rm |-> GetPrimary(rmState[r].view), view |-> rmState[r].view] \in msgs + +\* -------------- Safety temporal formula -------------- + +\* Init is the initial predicate initializing values at the start of every +\* behaviour. +Init == + /\ rmState = [r \in RM |-> [type |-> "initialized", view |-> 0]] + /\ msgs = {} + +\* RMSendPrepareRequest describes the primary node r broadcasting PrepareRequest. +RMSendPrepareRequest(r) == + /\ rmState[r].type = "initialized" + /\ IsPrimary(r) + /\ rmState' = [rmState EXCEPT ![r].type = "prepareSent"] + /\ msgs' = msgs \cup {[type |-> "PrepareRequest", rm |-> r, view |-> rmState[r].view]} + /\ UNCHANGED <<>> + +\* RMSendPrepareResponse describes non-primary node r receiving PrepareRequest from +\* the primary node of the current round (view) and broadcasting PrepareResponse. +\* This step assumes that PrepareRequest always contains valid transactions and +\* signatures. +RMSendPrepareResponse(r) == + /\ \/ rmState[r].type = "initialized" + \* We do allow the transition from the "cv" state to the "prepareSent" or "commitSent" stage + \* as it is done in the code-level dBFT implementation by checking the NotAcceptingPayloadsDueToViewChanging + \* condition (see + \* https://github.com/nspcc-dev/dbft/blob/31c1bbdc74f2faa32ec9025062e3a4e2ccfd4214/dbft.go#L419 + \* and + \* https://github.com/neo-project/neo-modules/blob/d00d90b9c27b3d0c3c57e9ca1f560a09975df241/src/DBFTPlugin/Consensus/ConsensusService.OnMessage.cs#L79). + \* However, we can't easily count the number of "lost" nodes in this specification to match precisely + \* the implementation. Moreover, we don't need it to be counted as the RMSendPrepareResponse enabling + \* condition specifies only the thing that may happen given some particular set of enabling conditions. + \* Thus, we've extended the NotAcceptingPayloadsDueToViewChanging condition to consider only MoreThanFNodesCommitted. + \* It should be noted that the logic of MoreThanFNodesCommittedOrLost can't be reliable in detecting lost nodes + \* (even with neo-project/neo#2057), because real nodes can go down at any time. + \/ /\ rmState[r].type = "cv" + /\ MoreThanFNodesCommitted(r) + /\ \neg IsPrimary(r) + /\ PrepareRequestSentOrReceived(r) + /\ rmState' = [rmState EXCEPT ![r].type = "prepareSent"] + /\ msgs' = msgs \cup {[type |-> "PrepareResponse", rm |-> r, view |-> rmState[r].view]} + /\ UNCHANGED <<>> + +\* RMSendCommit describes node r sending Commit if there's enough PrepareResponse +\* messages. +RMSendCommit(r) == + /\ \/ rmState[r].type = "prepareSent" + \* We do allow the transition from the "cv" state to the "prepareSent" or "commitSent" stage, + \* see the related comment inside the RMSendPrepareResponse definition. + \/ /\ rmState[r].type = "cv" + /\ MoreThanFNodesCommitted(r) + /\ Cardinality({ + msg \in msgs : /\ (msg.type = "PrepareResponse" \/ msg.type = "PrepareRequest") + /\ msg.view = rmState[r].view + }) >= M + /\ PrepareRequestSentOrReceived(r) + /\ rmState' = [rmState EXCEPT ![r].type = "commitSent"] + /\ msgs' = msgs \cup {[type |-> "Commit", rm |-> r, view |-> rmState[r].view]} + /\ UNCHANGED <<>> + +\* RMAcceptBlock describes node r collecting enough Commit messages and accepting +\* the block. +RMAcceptBlock(r) == + /\ rmState[r].type /= "bad" + /\ rmState[r].type /= "dead" + /\ PrepareRequestSentOrReceived(r) + /\ Cardinality({msg \in msgs : msg.type = "Commit" /\ msg.view = rmState[r].view}) >= M + /\ rmState' = [rmState EXCEPT ![r].type = "blockAccepted"] + /\ UNCHANGED <> + +\* RMSendChangeView describes node r sending ChangeView message on timeout. +RMSendChangeView(r) == + /\ \/ rmState[r].type = "initialized" + \/ rmState[r].type = "prepareSent" + /\ LET cv == [type |-> "ChangeView", rm |-> r, view |-> rmState[r].view] + IN /\ cv \notin msgs + /\ rmState' = [rmState EXCEPT ![r].type = "cv"] + /\ msgs' = msgs \cup {[type |-> "ChangeView", rm |-> r, view |-> rmState[r].view]} + +\* RMReceiveChangeView describes node r receiving enough ChangeView messages for +\* view changing. +RMReceiveChangeView(r) == + /\ rmState[r].type /= "bad" + /\ rmState[r].type /= "dead" + /\ rmState[r].type /= "blockAccepted" + /\ rmState[r].type /= "commitSent" + /\ Cardinality({ + rm \in RM : Cardinality({ + msg \in msgs : /\ msg.type = "ChangeView" + /\ msg.rm = rm + /\ GetNewView(msg.view) >= GetNewView(rmState[r].view) + }) /= 0 + }) >= M + /\ rmState' = [rmState EXCEPT ![r].type = "initialized", ![r].view = GetNewView(rmState[r].view)] + /\ UNCHANGED <> + +\* RMBeBad describes the faulty node r that will send any kind of consensus message starting +\* from the step it's gone wild. This step is enabled only when RMFault is non-empty set. +RMBeBad(r) == + /\ r \in RMFault + /\ Cardinality({rm \in RM : rmState[rm].type = "bad"}) < F + /\ rmState' = [rmState EXCEPT ![r].type = "bad"] + /\ UNCHANGED <> + +\* RMFaultySendCV describes sending CV message by the faulty node r. +RMFaultySendCV(r) == + /\ rmState[r].type = "bad" + /\ LET cv == [type |-> "ChangeView", rm |-> r, view |-> rmState[r].view] + IN /\ cv \notin msgs + /\ msgs' = msgs \cup {cv} + /\ UNCHANGED <> + +\* RMFaultyDoCV describes view changing by the faulty node r. +RMFaultyDoCV(r) == + /\ rmState[r].type = "bad" + /\ rmState' = [rmState EXCEPT ![r].view = GetNewView(rmState[r].view)] + /\ UNCHANGED <> + +\* RMFaultySendPReq describes sending PrepareRequest message by the primary faulty node r. +RMFaultySendPReq(r) == + /\ rmState[r].type = "bad" + /\ IsPrimary(r) + /\ LET pReq == [type |-> "PrepareRequest", rm |-> r, view |-> rmState[r].view] + IN /\ pReq \notin msgs + /\ msgs' = msgs \cup {pReq} + /\ UNCHANGED <> + +\* RMFaultySendPResp describes sending PrepareResponse message by the non-primary faulty node r. +RMFaultySendPResp(r) == + /\ rmState[r].type = "bad" + /\ \neg IsPrimary(r) + /\ LET pResp == [type |-> "PrepareResponse", rm |-> r, view |-> rmState[r].view] + IN /\ pResp \notin msgs + /\ msgs' = msgs \cup {pResp} + /\ UNCHANGED <> + +\* RMFaultySendCommit describes sending Commit message by the faulty node r. +RMFaultySendCommit(r) == + /\ rmState[r].type = "bad" + /\ LET commit == [type |-> "Commit", rm |-> r, view |-> rmState[r].view] + IN /\ commit \notin msgs + /\ msgs' = msgs \cup {commit} + /\ UNCHANGED <> + +\* RMDie describes node r that was removed from the network at the particular step +\* of the behaviour. After this node r can't change its state and accept/send messages. +RMDie(r) == + /\ r \in RMDead + /\ Cardinality({rm \in RM : rmState[rm].type = "dead"}) < F + /\ rmState' = [rmState EXCEPT ![r].type = "dead"] + /\ UNCHANGED <> + +\* Terminating is an action that allows infinite stuttering to prevent deadlock on +\* behaviour termination. We consider termination to be valid if at least M nodes +\* has the block being accepted. +Terminating == + /\ Cardinality({rm \in RM : rmState[rm].type = "blockAccepted"}) >= M + /\ UNCHANGED <> + +\* Next is the next-state action describing the transition from the current state +\* to the next state of the behaviour. +Next == + \/ Terminating + \/ \E r \in RM: + RMSendPrepareRequest(r) \/ RMSendPrepareResponse(r) \/ RMSendCommit(r) + \/ RMAcceptBlock(r) \/ RMSendChangeView(r) \/ RMReceiveChangeView(r) + \/ RMDie(r) \/ RMBeBad(r) + \/ RMFaultySendCV(r) \/ RMFaultyDoCV(r) \/ RMFaultySendCommit(r) \/ RMFaultySendPReq(r) \/ RMFaultySendPResp(r) + +\* Safety is a temporal formula that describes the whole set of allowed +\* behaviours. It specifies only what the system MAY do (i.e. the set of +\* possible allowed behaviours for the system). It asserts only what may +\* happen; any behaviour that violates it does so at some point and +\* nothing past that point makes difference. +\* +\* E.g. this safety formula (applied standalone) allows the behaviour to end +\* with an infinite set of stuttering steps (those steps that DO NOT change +\* neither msgs nor rmState) and never reach the state where at least one +\* node is committed or accepted the block. +\* +\* To forbid such behaviours we must specify what the system MUST +\* do. It will be specified below with the help of fairness conditions in +\* the Fairness formula. +Safety == Init /\ [][Next]_vars + +\* -------------- Fairness temporal formula -------------- + +\* Fairness is a temporal assumptions under which the model is working. +\* Usually it specifies different kind of assumptions for each/some +\* subactions of the Next's state action, but the only think that bothers +\* us is preventing infinite stuttering at those steps where some of Next's +\* subactions are enabled. Thus, the only thing that we require from the +\* system is to keep take the steps until it's impossible to take them. +\* That's exactly how the weak fairness condition works: if some action +\* remains continuously enabled, it must eventually happen. +Fairness == WF_vars(Next) + +\* -------------- Specification -------------- + +\* The complete specification of the protocol written as a temporal formula. +Spec == Safety /\ Fairness + +\* -------------- Liveness temporal formula -------------- + +\* For every possible behaviour it's true that eventually (i.e. at least once +\* through the behaviour) block will be accepted. It is something that dBFT +\* must guarantee (an in practice this condition is violated). +TerminationRequirement == <>(Cardinality({r \in RM : rmState[r].type = "blockAccepted"}) >= M) + +\* A liveness temporal formula asserts only what must happen (i.e. specifies +\* what the system MUST do). Any behaviour can NOT violate it at ANY point; +\* there's always the rest of the behaviour that can always make the liveness +\* formula true; if there's no such behaviour than the liveness formula is +\* violated. The liveness formula is supposed to be checked as a property +\* by the TLC model checker. +Liveness == TerminationRequirement + +\* -------------- ModelConstraints -------------- + +\* MaxViewConstraint is a state predicate restricting the number of possible +\* behaviour states. It is needed to reduce model checking time and prevent +\* the model graph size explosion. This formulae must be specified at the +\* "State constraint" section of the "Additional Spec Options" section inside +\* the model overview. +MaxViewConstraint == /\ \A r \in RM : rmState[r].view <= MaxView + /\ \A msg \in msgs : msg.view <= MaxView + +\* -------------- Invariants of the specification -------------- + +\* Model invariant is a state predicate (statement) that must be true for +\* every step of every reachable behaviour. Model invariant is supposed to +\* be checked as an Invariant by the TLC Model Checker. + +\* TypeOK is a type-correctness invariant. It states that all elements of +\* specification variables must have the proper type throughout the behaviour. +TypeOK == + /\ rmState \in [RM -> RMStates] + /\ msgs \subseteq Messages + +\* InvTwoBlocksAccepted states that there can't be two different blocks accepted in +\* the two different views, i.e. dBFT must not allow forks. +InvTwoBlocksAccepted == \A r1 \in RM: + \A r2 \in RM \ {r1}: + \/ rmState[r1].type /= "blockAccepted" + \/ rmState[r2].type /= "blockAccepted" + \/ rmState[r1].view = rmState[r2].view + +\* InvFaultNodesCount states that there can be F faulty or dead nodes at max. +InvFaultNodesCount == Cardinality({ + r \in RM : rmState[r].type = "bad" \/ rmState[r].type = "dead" + }) <= F + +\* This theorem asserts the truth of the temporal formula whose meaning is that +\* the state predicates TypeOK, InvTwoBlocksAccepted and InvFaultNodesCount are +\* the invariants of the specification Spec. This theorem is not supposed to be +\* checked by the TLC model checker, it's here for the reader's understanding of +\* the purpose of TypeOK, InvTwoBlocksAccepted and InvFaultNodesCount. +THEOREM Spec => [](TypeOK /\ InvTwoBlocksAccepted /\ InvFaultNodesCount) + +============================================================================= +\* Modification History +\* Last modified Fri Feb 17 15:47:41 MSK 2023 by anna +\* Last modified Sat Jan 21 01:26:16 MSK 2023 by rik +\* Created Thu Dec 15 16:06:17 MSK 2022 by anna diff --git a/formal-models/dbft/dbft___AllGoodModel.launch b/formal-models/dbft/dbft___AllGoodModel.launch new file mode 100644 index 00000000..eb14599a --- /dev/null +++ b/formal-models/dbft/dbft___AllGoodModel.launch @@ -0,0 +1,42 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/formal-models/dbftMultipool/dbftMultipool.tla b/formal-models/dbftMultipool/dbftMultipool.tla new file mode 100644 index 00000000..3eb395ec --- /dev/null +++ b/formal-models/dbftMultipool/dbftMultipool.tla @@ -0,0 +1,466 @@ +---------------------------- MODULE dbftMultipool ---------------------------- + +EXTENDS + Integers, + FiniteSets + +CONSTANTS + \* RM is the set of consensus node indexes starting from 0. + \* Example: {0, 1, 2, 3} + RM, + + \* RMFault is a set of consensus node indexes that are allowed to become + \* FAULT in the middle of every considered behavior and to send any + \* consensus message afterwards. RMFault must be a subset of RM. An empty + \* set means that all nodes are good in every possible behaviour. + \* Examples: {0} + \* {1, 3} + \* {} + RMFault, + + \* RMDead is a set of consensus node indexes that are allowed to die in the + \* middle of every behaviour and do not send any message afterwards. RMDead + \* must be a subset of RM. An empty set means that all nodes are alive and + \* responding in in every possible behaviour. RMDead may intersect the + \* RMFault set which means that node which is in both RMDead and RMFault + \* may become FAULT and send any message starting from some step of the + \* particular behaviour and may also die in the same behaviour which will + \* prevent it from sending any message. + \* Examples: {0} + \* {3, 2} + \* {} + RMDead, + + \* MaxView is the maximum allowed view to be considered (starting from 0, + \* including the MaxView itself). This constraint was introduced to reduce + \* the number of possible model states to be checked. It is recommended to + \* keep this setting not too high (< N is highly recommended). + \* Example: 2 + MaxView, + + \* MaxUndeliveredMessages is the maximum number of messages in the common + \* messages pool (msgs) that were not received and handled by all consensus + \* nodes. It must not be too small (>= 3) in order to allow model taking + \* at least any steps. At the same time it must not be too high (<= 6 is + \* recommended) in order to avoid states graph size explosion. + MaxUndeliveredMessages + +VARIABLES + \* rmState is a set of consensus node states. It is represented by the + \* mapping (function) with domain RM and range RMStates. I.e. rmState[r] is + \* the state of the r-th consensus node at the current step. + rmState, + + \* msgs is the shared pool of messages sent to the network by consensus nodes. + \* It is represented by a subset of Messages set. + msgs + +\* vars is a tuple of all variables used in the specification. It is needed to +\* simplify fairness conditions definition. +vars == <> + +\* N is the number of validators. +N == Cardinality(RM) + +\* F is the number of validators that are allowed to be malicious. +F == (N - 1) \div 3 + +\* M is the number of validators that must function correctly. +M == N - F + +\* These assumptions are checked by the TLC model checker once at the start of +\* the model checking process. All the input data (declared constants) specified +\* in the "Model Overview" section must satisfy these constraints. +ASSUME + /\ RM \subseteq Nat + /\ N >= 4 + /\ 0 \in RM + /\ RMFault \subseteq RM + /\ RMDead \subseteq RM + /\ Cardinality(RMFault) <= F + /\ Cardinality(RMDead) <= F + /\ Cardinality(RMFault \cup RMDead) <= F + /\ MaxView \in Nat + /\ MaxView <= 2 + /\ MaxUndeliveredMessages \in Nat + /\ MaxUndeliveredMessages >= 3 \* First value when block can be accepted in some behaviours. + +\* Messages is a set of records where each record holds the message type, +\* the message sender and sender's view by the moment when message was sent. +Messages == [type : {"PrepareRequest", "PrepareResponse", "Commit", "ChangeView"}, rm : RM, view : Nat] + +\* RMStates is a set of records where each record holds the node state, the node current view +\* and the pool of messages the nde has been sent or received and handled. +RMStates == [ + type: {"initialized", "prepareSent", "commitSent", "blockAccepted", "bad", "dead"}, + view : Nat, + pool : SUBSET Messages + ] + +\* -------------- Useful operators -------------- + +\* IsPrimary is an operator defining whether provided node r is primary +\* for the current round from the r's point of view. It is a mapping +\* from RM to the set of {TRUE, FALSE}. +IsPrimary(r) == rmState[r].view % N = r + +\* GetPrimary is an operator defining mapping from round index to the RM that +\* is primary in this round. +GetPrimary(view) == CHOOSE r \in RM : view % N = r + +\* GetNewView returns new view number based on the previous node view value. +\* Current specifications only allows to increment view. +GetNewView(oldView) == oldView + 1 + +\* IsViewChanging denotes whether node r have sent ChangeView message for the +\* current (or later) round. +IsViewChanging(r) == Cardinality({msg \in rmState[r].pool : msg.type = "ChangeView" /\ msg.view >= rmState[r].view /\ msg.rm = r}) /= 0 + +\* CountCommitted returns the number of nodes that have sent the Commit message +\* in the current round (as the node r sees it). +CountCommitted(r) == Cardinality({rm \in RM : Cardinality({msg \in rmState[r].pool : msg.rm = rm /\ msg.type = "Commit"}) /= 0}) + +\* CountFailed returns the number of nodes that haven't sent any message since +\* the last round (as the node r sees it from the point of its pool). +CountFailed(r) == Cardinality({rm \in RM : Cardinality({msg \in rmState[r].pool : msg.rm = rm /\ msg.view >= rmState[r].view}) = 0 }) + +\* MoreThanFNodesCommittedOrLost denotes whether more than F nodes committed or +\* failed to communicate in the current round. +MoreThanFNodesCommittedOrLost(r) == CountCommitted(r) + CountFailed(r) > F + +\* NotAcceptingPayloadsDueToViewChanging returns whether the node doesn't accept +\* payloads in the current step. +NotAcceptingPayloadsDueToViewChanging(r) == + /\ IsViewChanging(r) + /\ \neg MoreThanFNodesCommittedOrLost(r) + +\* PrepareRequestSentOrReceived denotes whether there's a PrepareRequest +\* message received from the current round's speaker (as the node r sees it). +PrepareRequestSentOrReceived(r) == [type |-> "PrepareRequest", rm |-> GetPrimary(rmState[r].view), view |-> rmState[r].view] \in rmState[r].pool + +\* CommitSent returns whether the node has its commit sent for the current block. +CommitSent(r) == Cardinality({msg \in rmState[r].pool : msg.rm = r /\ msg.type = "Commit"}) > 0 + +\* -------------- Safety temporal formula -------------- + +\* Init is the initial predicate initializing values at the start of every +\* behaviour. +Init == + /\ rmState = [r \in RM |-> [type |-> "initialized", view |-> 1, pool |-> {}]] + /\ msgs = {} + +\* RMSendPrepareRequest describes the primary node r broadcasting PrepareRequest. +RMSendPrepareRequest(r) == + /\ rmState[r].type = "initialized" + /\ IsPrimary(r) + /\ LET pReq == [type |-> "PrepareRequest", rm |-> r, view |-> rmState[r].view] + commit == [type |-> "Commit", rm |-> r, view |-> rmState[r].view] + IN /\ pReq \notin msgs + /\ IF Cardinality({m \in rmState[r].pool : m.type = "PrepareResponse" /\ m.view = rmState[r].view}) < M - 1 \* -1 is for the current PrepareRequest. + THEN /\ rmState' = [rmState EXCEPT ![r].type = "prepareSent", ![r].pool = rmState[r].pool \cup {pReq}] + /\ msgs' = msgs \cup {pReq} + ELSE /\ msgs' = msgs \cup {pReq, commit} + /\ IF Cardinality({m \in rmState[r].pool : m.type = "Commit" /\ m.view = rmState[r].view}) < M-1 \* -1 is for the current Commit + THEN rmState' = [rmState EXCEPT ![r].type = "commitSent", ![r].pool = rmState[r].pool \cup {pReq, commit}] + ELSE rmState' = [rmState EXCEPT ![r].type = "blockAccepted", ![r].pool = rmState[r].pool \cup {pReq, commit}] + /\ UNCHANGED <<>> + +\* RMSendChangeView describes node r sending ChangeView message on timeout. +RMSendChangeView(r) == + /\ rmState[r].type /= "bad" + /\ rmState[r].type /= "dead" + /\ rmState[r].type /= "blockAccepted" + /\ \/ (IsPrimary(r) /\ PrepareRequestSentOrReceived(r)) + \/ (\neg IsPrimary(r) /\ \neg CommitSent(r)) + /\ LET msg == [type |-> "ChangeView", rm |-> r, view |-> rmState[r].view] + IN /\ msg \notin msgs + /\ msgs' = msgs \cup {msg} + /\ IF Cardinality({m \in rmState[r].pool : m.type = "ChangeView" /\ GetNewView(m.view) >= GetNewView(msg.view)}) >= M-1 \* -1 is for the currently sent CV + THEN rmState' = [rmState EXCEPT ![r].type = "initialized", ![r].view = GetNewView(msg.view), ![r].pool = rmState[r].pool \cup {msg}] + ELSE rmState' = [rmState EXCEPT ![r].pool = rmState[r].pool \cup {msg}] + +\* OnTimeout describes two actions the node can take on timeout for waiting any event. +OnTimeout(r) == + \/ RMSendPrepareRequest(r) + \/ RMSendChangeView(r) + +\* RMOnPrepareRequest describes non-primary node r receiving PrepareRequest from the +\* primary node of the current round (view) and broadcasts PrepareResponse. +\* This step assumes that PrepareRequest always contains valid transactions and +\* signatures. +RMOnPrepareRequest(r) == + /\ rmState[r].type = "initialized" + /\ \E msg \in msgs \ rmState[r].pool: + /\ msg.rm /= r + /\ msg.type = "PrepareRequest" + /\ msg.view = rmState[r].view + /\ \neg IsPrimary(r) + /\ \neg NotAcceptingPayloadsDueToViewChanging(r) \* dbft.go -L296, in C# node, but not in ours + /\ LET pResp == [type |-> "PrepareResponse", rm |-> r, view |-> rmState[r].view] + commit == [type |-> "Commit", rm |-> r, view |-> rmState[r].view] + IN IF Cardinality({m \in rmState[r].pool : m.type = "PrepareResponse" /\ m.view = rmState[r].view}) < M - 1 - 1 \* -1 is for reveived PrepareRequest; -1 is for current PrepareResponse + THEN /\ rmState' = [rmState EXCEPT ![r].type = "prepareSent", ![r].pool = rmState[r].pool \cup {msg, pResp}] + /\ msgs' = msgs \cup {pResp} + ELSE /\ msgs' = msgs \cup {msg, pResp, commit} + /\ IF Cardinality({m \in rmState[r].pool : m.type = "Commit" /\ m.view = rmState[r].view}) < M-1 \* -1 is for the current Commit + THEN rmState' = [rmState EXCEPT ![r].type = "commitSent", ![r].pool = rmState[r].pool \cup {msg, pResp, commit}] + ELSE rmState' = [rmState EXCEPT ![r].type = "blockAccepted", ![r].pool = rmState[r].pool \cup {msg, pResp, commit}] + /\ UNCHANGED <<>> + +\* RMOnPrepareResponse describes node r accepting PrepareResponse message and handling it. +\* If there's enough PrepareResponses collected it will send the Commit; in case if there's +\* enough Commits it will accept the block. +RMOnPrepareResponse(r) == + /\ rmState[r].type /= "bad" + /\ rmState[r].type /= "dead" + /\ rmState[r].type /= "blockAccepted" + /\ \E msg \in msgs \ rmState[r].pool: + /\ msg.rm /= r + /\ msg.type = "PrepareResponse" + /\ msg.view = rmState[r].view + /\ \neg NotAcceptingPayloadsDueToViewChanging(r) + /\ IF \/ Cardinality({m \in rmState[r].pool : (m.type = "PrepareRequest" \/ m.type = "PrepareResponse") /\ m.view = rmState[r].view}) < M - 1 \* -1 is for the currently received PrepareResponse. + \/ CommitSent(r) + \/ \neg PrepareRequestSentOrReceived(r) + THEN /\ rmState' = [rmState EXCEPT ![r].pool = rmState[r].pool \cup {msg}] + /\ UNCHANGED <> + ELSE LET commit == [type |-> "Commit", rm |-> r, view |-> rmState[r].view] + IN /\ msgs' = msgs \cup {msg, commit} + /\ IF Cardinality({m \in rmState[r].pool : m.type = "Commit" /\ m.view = rmState[r].view}) < M-1 \* -1 is for the current Commit + THEN rmState' = [rmState EXCEPT ![r].type = "commitSent", ![r].pool = rmState[r].pool \cup {msg, commit}] + ELSE rmState' = [rmState EXCEPT ![r].type = "blockAccepted", ![r].pool = rmState[r].pool \cup {msg, commit}] + +\* RMOnCommit describes node r accepting Commit message and (in case if there's enough Commits) +\* accepting the block. +RMOnCommit(r) == + /\ rmState[r].type /= "bad" + /\ rmState[r].type /= "dead" + /\ rmState[r].type /= "blockAccepted" + /\ \E msg \in msgs \ rmState[r].pool: + /\ msg.rm /= r + /\ msg.type = "Commit" + /\ msg.view = rmState[r].view + /\ IF Cardinality({m \in rmState[r].pool : m.type = "Commit" /\ m.view = rmState[r].view}) < M-1 \* -1 is for the currently accepting commit + THEN rmState' = [rmState EXCEPT ![r].pool = rmState[r].pool \cup {msg}] + ELSE rmState' = [rmState EXCEPT ![r].type = "blockAccepted", ![r].pool = rmState[r].pool \cup {msg}] + /\ UNCHANGED <> + +\* RMOnChangeView describes node r receiving ChangeView message and (in case if enough ChangeViews +\* is collected) changing its view. +RMOnChangeView(r) == + /\ rmState[r].type /= "bad" + /\ rmState[r].type /= "dead" + /\ rmState[r].type /= "blockAccepted" + /\ \E msg \in msgs \ rmState[r].pool: + /\ msg.rm /= r + /\ msg.type = "ChangeView" + /\ msg.view = rmState[r].view + /\ \neg CommitSent(r) + /\ Cardinality({m \in rmState[r].pool : m.type = "ChangeView" /\ m.rm = msg.rm /\ m.view > msg.view}) = 0 + /\ IF Cardinality({m \in rmState[r].pool : m.type = "ChangeView" /\ GetNewView(m.view) >= GetNewView(msg.view)}) < M-1 \* -1 is for the currently accepting CV + THEN rmState' = [rmState EXCEPT ![r].pool = rmState[r].pool \cup {msg}] + ELSE rmState' = [rmState EXCEPT ![r].type = "initialized", ![r].view = GetNewView(msg.view), ![r].pool = rmState[r].pool \cup {msg}] + /\ UNCHANGED <> + +\* RMBeBad describes the faulty node r that will send any kind of consensus message starting +\* from the step it's gone wild. This step is enabled only when RMFault is non-empty set. +RMBeBad(r) == + /\ r \in RMFault + /\ Cardinality({rm \in RM : rmState[rm].type = "bad"}) < F + /\ rmState' = [rmState EXCEPT ![r].type = "bad"] + /\ UNCHANGED <> + +\* RMFaultySendCV describes sending CV message by the faulty node r. +RMFaultySendCV(r) == + /\ rmState[r].type = "bad" + /\ LET cv == [type |-> "ChangeView", rm |-> r, view |-> rmState[r].view] + IN /\ cv \notin msgs + /\ msgs' = msgs \cup {cv} + /\ UNCHANGED <> + +\* RMFaultyDoCV describes view changing by the faulty node r. +RMFaultyDoCV(r) == + /\ rmState[r].type = "bad" + /\ rmState' = [rmState EXCEPT ![r].view = GetNewView(rmState[r].view)] + /\ UNCHANGED <> + +\* RMFaultySendPReq describes sending PrepareRequest message by the primary faulty node r. +RMFaultySendPReq(r) == + /\ rmState[r].type = "bad" + /\ IsPrimary(r) + /\ LET pReq == [type |-> "PrepareRequest", rm |-> r, view |-> rmState[r].view] + IN /\ pReq \notin msgs + /\ msgs' = msgs \cup {pReq} + /\ UNCHANGED <> + +\* RMFaultySendPResp describes sending PrepareResponse message by the non-primary faulty node r. +RMFaultySendPResp(r) == + /\ rmState[r].type = "bad" + /\ \neg IsPrimary(r) + /\ LET pResp == [type |-> "PrepareResponse", rm |-> r, view |-> rmState[r].view] + IN /\ pResp \notin msgs + /\ msgs' = msgs \cup {pResp} + /\ UNCHANGED <> + +\* RMFaultySendCommit describes sending Commit message by the faulty node r. +RMFaultySendCommit(r) == + /\ rmState[r].type = "bad" + /\ LET commit == [type |-> "Commit", rm |-> r, view |-> rmState[r].view] + IN /\ commit \notin msgs + /\ msgs' = msgs \cup {commit} + /\ UNCHANGED <> + +\* RMDie describes node r that was removed from the network at the particular step +\* of the behaviour. After this node r can't change its state and accept/send messages. +RMDie(r) == + /\ r \in RMDead + /\ Cardinality({rm \in RM : rmState[rm].type = "dead"}) < F + /\ rmState' = [rmState EXCEPT ![r].type = "dead"] + /\ UNCHANGED <> + +\* Terminating is an action that allows infinite stuttering to prevent deadlock on +\* behaviour termination. We consider termination to be valid if at least M nodes +\* has the block being accepted. +Terminating == + /\ Cardinality({rm \in RM : rmState[rm].type = "blockAccepted"}) >=1 + /\ UNCHANGED <> + +\* Next is the next-state action describing the transition from the current state +\* to the next state of the behaviour. +Next == + \/ Terminating + \/ \E r \in RM : + \/ OnTimeout(r) + \/ RMOnPrepareRequest(r) \/ RMOnPrepareResponse(r) \/ RMOnCommit(r) \/ RMOnChangeView(r) + \/ RMDie(r) \/ RMBeBad(r) + \/ RMFaultySendCV(r) \/ RMFaultyDoCV(r) \/ RMFaultySendCommit(r) \/ RMFaultySendPReq(r) \/ RMFaultySendPResp(r) + +\* Safety is a temporal formula that describes the whole set of allowed +\* behaviours. It specifies only what the system MAY do (i.e. the set of +\* possible allowed behaviours for the system). It asserts only what may +\* happen; any behaviour that violates it does so at some point and +\* nothing past that point makes difference. +\* +\* E.g. this safety formula (applied standalone) allows the behaviour to end +\* with an infinite set of stuttering steps (those steps that DO NOT change +\* neither msgs nor rmState) and never reach the state where at least one +\* node is committed or accepted the block. +\* +\* To forbid such behaviours we must specify what the system MUST +\* do. It will be specified below with the help of fairness conditions in +\* the Fairness formula. +Safety == Init /\ [][Next]_vars + +\* -------------- Fairness temporal formula -------------- + +\* Fairness is a temporal assumptions under which the model is working. +\* Usually it specifies different kind of assumptions for each/some +\* subactions of the Next's state action, but the only think that bothers +\* us is preventing infinite stuttering at those steps where some of Next's +\* subactions are enabled. Thus, the only thing that we require from the +\* system is to keep take the steps until it's impossible to take them. +\* That's exactly how the weak fairness condition works: if some action +\* remains continuously enabled, it must eventually happen. +Fairness == WF_vars(Next) + +\* -------------- Specification -------------- + +\* The complete specification of the protocol written as a temporal formula. +Spec == Safety /\ Fairness + +\* -------------- Liveness temporal formula -------------- + +\* For every possible behaviour it's true that there's at least one PrepareRequest +\* message from the speaker, there's at lest one PrepareResponse message and at +\* least one Commit message. +PrepareRequestSentRequirement == <>(\E msg \in msgs : msg.type = "PrepareRequest") +PrepareResponseSentRequirement == <>(\E msg \in msgs : msg.type = "PrepareResponse") +CommitSentRequirement == <>(\E msg \in msgs : msg.type = "Commit") + +\* For every possible behaviour it's true that eventually (i.e. at least once +\* through the behaviour) block will be accepted. It is something that dBFT +\* must guarantee (an in practice this condition is violated). +TerminationRequirement == <>(Cardinality({r \in RM : rmState[r].type = "blockAccepted"}) >= M) + +\* A liveness temporal formula asserts only what must happen (i.e. specifies +\* what the system MUST do). Any behaviour can NOT violate it at ANY point; +\* there's always the rest of the behaviour that can always make the liveness +\* formula true; if there's no such behaviour than the liveness formula is +\* violated. The liveness formula is supposed to be checked as a property +\* by the TLC model checker. +Liveness == /\ PrepareRequestSentRequirement + /\ PrepareResponseSentRequirement + /\ CommitSentRequirement + /\ TerminationRequirement + +\* -------------- Model constraints -------------- + +\* Model constraints are a set of state predicates restricting the number of possible +\* behaviour states. It is needed to reduce model checking time and prevent +\* the model graph size explosion. These formulaes must be specified at the +\* "State constraint" section of the "Additional Spec Options" section inside +\* the model overview. + +\* MaxViewConstraint is a state predicate restricting the maximum view of messages +\* and consensus nodes state. +MaxViewConstraint == /\ \A r \in RM : rmState[r].view <= MaxView + /\ \A msg \in msgs : msg.view <= MaxView + +\* MaxUndeliveredMessageConstraint is a state predicate restricting the maximum +\* number of messages undelivered to any of the consensus nodes. +MaxUndeliveredMessageConstraint == Cardinality({msg \in msgs : \E rm \in RM : msg \notin rmState[rm].pool}) <= MaxUndeliveredMessages + +\* ModelConstraint is overall model constraint rule. +ModelConstraint == MaxViewConstraint /\ MaxUndeliveredMessageConstraint + +\* -------------- Invariants of the specification -------------- + +\* Model invariant is a state predicate (statement) that must be true for +\* every step of every reachable behaviour. Model invariant is supposed to +\* be checked as an Invariant by the TLC Model Checker. + +\* TypeOK is a type-correctness invariant. It states that all elements of +\* specification variables must have the proper type throughout the behaviour. +TypeOK == + /\ rmState \in [RM -> RMStates] + /\ msgs \subseteq Messages + +\* InvTwoBlocksAccepted states that there can't be two different blocks accepted in +\* the two different views, i.e. dBFT must not allow forks. +InvTwoBlocksAccepted == \A r1 \in RM: + \A r2 \in RM \ {r1}: + \/ rmState[r1].type /= "blockAccepted" + \/ rmState[r2].type /= "blockAccepted" + \/ rmState[r1].view = rmState[r2].view + +\* InvDeadlock is a deadlock invariant, it states that the following situation expected +\* never to happen: one node is committed in a single view, two others are committed in +\* a larger view, and the last one has its view changing. +InvDeadlock == \A r1 \in RM : + \A r2 \in RM \ {r1} : + \A r3 \in RM \ {r1, r2} : + \A r4 \in RM \ {r1, r2, r3} : + \/ rmState[r1].type /= "commitSent" + \/ rmState[r2].type /= "commitSent" + \/ rmState[r3].type /= "commitSent" + \/ \neg IsViewChanging(r4) + \/ rmState[r1].view >= rmState[r2].view + \/ rmState[r2].view /= rmState[r3].view + \/ rmState[r3].view /= rmState[r4].view + +\* InvFaultNodesCount states that there can be F faulty or dead nodes at max. +InvFaultNodesCount == Cardinality({ + r \in RM : rmState[r].type = "bad" \/ rmState[r].type = "dead" + }) <= F + +\* This theorem asserts the truth of the temporal formula whose meaning is that +\* the state predicates TypeOK, InvTwoBlocksAccepted, InvDeadlock and InvFaultNodesCount are +\* the invariants of the specification Spec. This theorem is not supposed to be +\* checked by the TLC model checker, it's here for the reader's understanding of +\* the purpose of TypeOK, InvTwoBlocksAccepted, InvDeadlock and InvFaultNodesCount. +THEOREM Spec => [](TypeOK /\ InvTwoBlocksAccepted /\ InvDeadlock /\ InvFaultNodesCount) + +============================================================================= +\* Modification History +\* Last modified Fri Feb 17 15:51:19 MSK 2023 by anna +\* Created Tue Jan 10 12:28:45 MSK 2023 by anna diff --git a/formal-models/dbftMultipool/dbftMultipool___AllGoodModel.launch b/formal-models/dbftMultipool/dbftMultipool___AllGoodModel.launch new file mode 100644 index 00000000..e522df66 --- /dev/null +++ b/formal-models/dbftMultipool/dbftMultipool___AllGoodModel.launch @@ -0,0 +1,44 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +