From de50c7bd3df96a6eba9059e1f642ba3eee203902 Mon Sep 17 00:00:00 2001 From: Anna Shaleva Date: Thu, 25 Apr 2024 20:03:58 +0300 Subject: [PATCH] formal-models: extend dBFT with additional post-commit phase Close #111. The additional step is called RMSendAck and allows to send Ack message once enough Commit messages are received. Block can be accepted only if BFT number of Ack messages are collected. Signed-off-by: Anna Shaleva --- CHANGELOG.md | 1 + formal-models/.github/dbft_antiMEV.drawio | 111 +++++ formal-models/.github/dbft_antiMEV.png | Bin 0 -> 70101 bytes formal-models/README.md | 62 +++ formal-models/dbft_antiMEV/dbft.tla | 430 ++++++++++++++++++ .../dbft_antiMEV/dbft___AllGoodModel.launch | 42 ++ 6 files changed, 646 insertions(+) create mode 100644 formal-models/.github/dbft_antiMEV.drawio create mode 100644 formal-models/.github/dbft_antiMEV.png create mode 100644 formal-models/dbft_antiMEV/dbft.tla create mode 100644 formal-models/dbft_antiMEV/dbft___AllGoodModel.launch diff --git a/CHANGELOG.md b/CHANGELOG.md index 1488390a..43020b79 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,6 +5,7 @@ This document outlines major changes between releases. ## [Unreleased] New features: + * TLA+ model for MEV-resistant dBFT extension (#116) Behaviour changes: * simplify PublicKey interface (#114) diff --git a/formal-models/.github/dbft_antiMEV.drawio b/formal-models/.github/dbft_antiMEV.drawio new file mode 100644 index 00000000..3852ba04 --- /dev/null +++ b/formal-models/.github/dbft_antiMEV.drawio @@ -0,0 +1,111 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/formal-models/.github/dbft_antiMEV.png b/formal-models/.github/dbft_antiMEV.png new file mode 100644 index 0000000000000000000000000000000000000000..a2a2b6ef4920d3649ba992a80e6f88a4a2997688 GIT binary patch literal 70101 zcmeEu2|Sc*-~T;hF!r64WvtovHI=bvD_bG^PWGJ=V<~GWL&+|U-^PJ~7@B4m|nfto0`&xe2Z~6X~TfD(REh_Szg2oV}`658WEWk6w+0DZV;*(a}`ol6TC&#TmQW8=!q7rhVQZgozl6=xCGIHRTgo2oajMUMs z{&p@-UW5Vly^p(jc-ZktY08R8fT0A;@Xx4%Z-?yzy#fNazU#Sp1%`mO5Cu6KIhn0C zzaTKIq?DYPgdn)1<>cV*4MvfYkdy#FlAuY`&Cki%8$71@t=HDnP62ilXeS)0){N2302)mIHlNFQQx)BiSJm;mk>!6 z6L~}b&;acNp<1R20d@xfp}rq&drZ#|Ek8RSSAB0sCl4^NV+dhEGSV_zYjO-Fv?wSN zcH`o=JrQAEe1oyu@$J2QTe*~kOQ4&hlmB=73-I>#2ypZHzR|(k%gf1uaIAz8?fm?_ zgTL?Q?Cn9=9-)s9*!g#(;~R{Bpeer9)Xg!#b*ry}EMa;0_5)6CF0R`%gY)0ov8Ua3 zXF`L&tDU2F@YeI+ntppMTZG&ur=Pbs81FZy_S@UrojgO-oILQ<-lijA9>8(`^=E&f zhTku;@!uKl_#rtJ8`mR_c2X{(KI(^M)l|KXh)NQ8A;``nkU;Y-QuzmjZnLnHBcMLv z(%Ub<)!W6}%g#gN*H%?O??5ldZ^Dk3)MJ63J_M#w0GGc$qUY`H18DuNk5fQED4~;G zV1PI1=NjPYLAdK5;OFiB%h>|IQ@#e}m8szlU!_5$42eAaM7)s{p@HGyI4^SKx1gOY>hQ02k_bf!vx7e}&)J zFINUmer}#l0pBzRzH#eJeC&SZ1Ojt_-M9dq`%TsS^nm5I9>t&GRkJ0oZb0z^J-)R%8F|9S2)ap{ zpqaKO^7jt(b8sR&gjcM8ELp#u9dE&YH>0c~L8u5bO3D$gx2N19@jo!7G%y~TKnriv z=KoK0Lho<-Qe?S7SUIp09McKaqZqW<3$KHfM< z%J_hD0o=EJAAEDc_XD5b#=(o_e`_FrAT(eA10yG2@FCy>*xt@B6qxU=@c{w1rucqZ z(EM!&-?#q9Yzioyzx4WlJrsW*{HfU6Ik*S<{BkJv`0ahi27l)<;pO#Lo|D4sBt1KO zfKI+s{&pU2E_kHn08}Pk0jdJ<72pP}zY5`or<pZ zBw1BHS#{8YXC8u1{>3W%p&9v^+4xZb|6Jq<=9GYZ2x|im6LboGD^3Je_m3)K!s8NR zlJW!r-`15|i~MsGwW##gY=pU`2$$PR)7#nEf7=%T-0=tCXWJZrp8rODN!Y?q)aBo; z=H!0RmlDo)4qG;JTZjILUVc!oZeDHyZa@x>15EX|G|BIT=|{-)TRi1z_svc53~|A` z1Y*t}-oXy800@Zz3G;OGvJ1fDB-LP7w*V(&pREN4gPsHl`bA=ZDf4r2v-^o)ZB73h z$AVFy`-p7XN&k zy)8$-QTk$MS!ZhqvJ97Igio zK_I~IKZNP>TT}drF#X@e-#_s;3(Ne{$!N4E$@G*AbzG0ew5Rn3gxzv{S#1{sDzjlf#nHEX*;C%=fJe@=T_Jv(6+hz zD}pqFLj4U$^YL@S2S$wXL9%bL)?dX->PO@AzX%n{;*}L%ntvbJ_zS`!f~WJFqs8l` z|AR$8(}I6mi1SBvOMv!&2#W}C=MP~KL1F#RhebcCwJjI{;IXG0&}$MuMHT-GOf^C9 z{~S{-sUS(_J-{0qif0qmY(I5E^tbLzt{&wp(`DQTFc3PT{xCSl1Nn8Kpa7=OQ(LaP^ zgb4Yc2*>{anNYlgv;Fgv)UMR;5+n))FtKf5|GJr70xbDX@cu~|SpYUQLD|&b$iM!3 z5$ASc$GT~y({oN@cEXI{(U4_iU64i zg?tj40P}zU7@l8#f|vfplD%z!@-M~v1WWSg;C-1bl5Vr;*44il>=OcxqW=T3zf%8a z_WwtfNBzBK|35qM^e;90zr2sItuwaG+&{_e|9*VYZMFYT8ec}@`vAv3IR0PFEdQ7j z`N6(!ndKw+xWvy&#_$zu_(EVjp2Yw1atgtJ1i3i{|1i|{nf=Zk`X6Shx3&MDV5&jc zmXrd)*&qnscE$UjW36QfmTr4;0&v*&EdGjtJA$(R4N`Ro`T=47=m!5Us@Rg+&H-=h z`t5ho{-Z0l?2UuG^c>|qZReiinOr-Q2x2qg~r;z?#vDW{K>lsV!;y$!ny4 zl^Ck50(kfSI~VGgGKy`@_|K1`{y3@J_RA#Oll~Rrs6Q3cpF|J7VG&Te0kFnTamoLv zkibugLMUta6JQ1?5C3=7oDre|1kZ|Ka0rNJo2~!DQN~XX@5i_J>^;04+*KSLoO}ZC z@6-K`fB#nlj$gFr_W5rsw*Lgc@y+G?8-I3VJM8-FUpV<~u=d;C?Z2tAb%XGLGx$R` zTfz9s$~rp;LP6T8#u_X&+CeNqZWQfe>cW)jntdm`X(Y+@fty+ zA|8#0&mNHrptuE?5%t!F*#)S>$8F5^%$Bt(yY!QB@jhyO!xt)E_3`9~cCW?P9T%lP zzR9av>P(7Pkc1~eJXoXzJPF;;WxHs4#*=$R*t;{64(Wu@<38oLUg-ro6wn~nMQ-eT_@)bYY^Yjt;q~MMYBh*Xi9-IZqw$ z9~IO+FY>8djmGf(;C;8|WOkX8Ujz08&F)|lG>Wl4@m}_($&GXSx~yxC_b6|!sc9rK z7qzDCHVz2*k=LyL%n zGS!TfTM~vuv{{k>icOt^EbGEA9$%W%5B>NiBj3E-IYacm@3`hp8CTjDw=FV{f0-4` zP)>KbcJSiVfJ=T&k*v7YL*5S;_MNC0I`TyxhOW;KTa4!wBBo$21piaZ1A|{Z43u&1 z*db(ml~VuWo)@<`R#x8T8;?Fd<;}I9)yd~wui(+U_QZix-SuJ=Ev>JDM?~vB@_7zb zoUsm_WI9^zOr@crv2rehze{x`I_B`LBcjh&>eFOhI@yj5-V@~G<#pV{>CNE?$59;( z69-#xWQJMMW0qc@IMm6@B5tjB_UzdQz3-!G_NPi869_K!diAj9zI&hR+;G){;n=rn z=g#q}_+(0PLnv;8{@M;_705Pz`Av?u>qN_06F_2%#>mGVXL(33Do4C_ho=r`28Sn; zVU8R)mPW$>dHPIP?tp2cP9g%dAc^r~FN;|L;dMLtFEXTmT^Mh^5itF1@mhwk>9a!Z zG-TmuveI1X2zAlRJ2rIzE}pD(n3@wy&u-nR)dAZoTK!OG)5*I}wo6zA4WUs-?pTW| zv%9S9lJh9|JkzK9aq}#XRy8+t9k9oy9-mHnf$#VeZBwFQ)PaW6R966ZJfC~@sA%B$ zJg)wnBX0A->*I+V>q|Cn83Gm+B2=9FE!!X#GUv)F|F`GG;HG4A^r@_7jwO~=s!wy| zGx>vf&0Gu~5Rp>1RKR?XFEp{-IR5$F1INku+;=cD1s|ubyo=~3M=LzEY4$IpJYQE| z;MdDSYo%}$B`^s;8}hCbommDF(_ORlT6j})s6ijGbg;r>z;Wol+w(Wf=C))Plp|`_ zs2eG}*1+k@IJGgFE1TuxG?zcrZ5CRnozfzzLiG!amj{e0}@)Am>ljq<)0sKjrw ztu=CgO(7EP;UPlBz9;>vehz=W+VSo8Gi`JdX}%`wYW=i+2nz!S~H$ ziKK)lY|5SWm0(bhV!%{tQXghfYrs{_>>4^5y%XJ;N<%-qcPb_M+&D{Ti;z*pTEM%Hrdt?U246jCKamp1m-y%~hLspLH+Wx{x^jJW=^8li zP!s)O3XMv~R(i!a2ZQF~uEX6I9Zu)bLd~m^ABo5eVsMS|3`S&EwM-acuD#dK=4#kK zNj6`qJ-J#~jhs-U#GFS!(&hpuc{`RF7#QA{A1?}%R)bPgt`H+4eM`A*ujaGDQ}c2S zz5tOpzrZdOdEJ)e%-huP_0Oh?L!_rm8L>jRsgi{lsNi7N-j9@L*p-gZ@BUajv-@dqq#*t%%=h69e*e2#&J57wH}kjSK->D+L?EsA0j7hiD8xL z_|mp>i~_bi_vph^dDs55^CSYz4Y4%F7xx6tmhAKvh2|#IMHBwSd38tE9I2gp23qZ(No1sQA1?FpXq=xRF)LAqJ1Didt_ODKB%Y?-rO z|4cpa^X>GDAyI8G?XbF5uu?5l`}mVAi<*mq$f zS`$$a7qatt`mQTGd-#1%a*4?f^$Tz8pT3C*UWFVTVOShZ+QyZX{qLkmpmI@5iJF@+ zDD<+KB+dbM>RGgXi-40lgbO}h$EpKkv8O5RrIl7*PTv<#9?T1+GTdUq!O^dekzALB z`Q*N8;G}9w%7PVk&|~y-Ish@tXg5gnX^rEe7R3bSqZM%(1 z;b4WQE-^Wy&wz&XC>*dM^`t~dz$%x7hBGT;`K##^1%8?m`$P)EN3^*qz9i3A8epwcSf^iBsEtb%!c6tXoU zeS+ON$ACi`KXUlGvHF3JHR=Yt7lpvsm-j=uw-U=BEFb2ALi%Xlz7xE5m<+69s4CEU zkreOZrjFku8djC4i;labT#$llq1&}yz$QYY@ro%lQWp8SUI&37RTT>+lMeETLpXi# z$PQ*gTrU>FQVDaS52&Eihsa)XbS%?hk;24lU-QGi-k`LPVM6w=T!2s~)Fn4kHQ}^| z?Q@VfiDWH+gT8orSZKT&{TRD4ubEZF(hBHdZ_BMk%fv`Se*oqjY}Ph;%td}J8OGV( z$mVipIzE>UhN0K>F3@~EzbZsLWyu^zp1zMHLPUCI@cxYF82SieKR1?Eha~~2yJ(wy zdNKIH*|SGU;x4@3w=~S-giT`5T`OgyzeQ0x&YjMYz8n6|mfN%)^6dgLERuP%{>~ZK zZ~@_BKeR-Sf7Ih9YYO+ilA^VhkL_p9;OJFk_Hr*|bg}LFfI=}KC|^P@b$jjiN}V&V z@~&MTqlk|-x{0h%uO^N=ZM2+q-=S5YrM*6y)QL0l0{iFaI(7sl>{97Y?4Aj+`s1*U z?zfm|9Te?#nz4Q8K@96xe(trqVe~5D$i3>yhPSwS%TWRg3kyMeRSXK&r2RNu9bpFc zpR`Xz&@uQl1UJM3tFi+YiBW=MTsK$721QERE~vDb!c#9u)tux9ipVqk=qnmw7}e#*HBr3R=GCw?2pm-;H}wd1F}{8@R-i8nOl`@9ONLOc$lV>N;;-u+=w<{;`uc)& z5=Nrk$({#8>2pGRt=7Pjjk1M333Q)DR`Ng*2}(B;C{`;s&a+l$L5?J{;iu{5DPSQ6 zxUaV==dE2f9C^Li@KPd(7^cINUp^lf)3#eIb7oDAoVbLNhjtKYn~z}_dz>68AAE%T z{T~1Kc6orX?jcPIw6yutAl84$u;nCh8s?mJ6*w*&=z7ZnN=J(EX|)@N_C2Sf-R} zT!afE=?pXsUAcHuLS=2Fx&MXzG%HLKYl_H%mJ?9QUC60jut|~wO!h~gsXKkFs~t)z zazMbNz#cHzj#CnF6%E@OftsV)h}b5VvjsX0r|`!ihNpI-vn|&SSRFTRip2I~oz0~; z9jvf%Jna=co6bqWFKA$WWucr+=|pbjW@O9`upZT7m8v~Sm|X}Q33j!_5=P00#}JC( z&f{t#pU>;D*wGTJaqio#86C|28n>RFN6T3hw>l;;?f#gc8g~Y&~t~wCO_G7Z3TG*zQ-& zf0~XDXF4tIg4hum02l+y9z)j+MH=th!&q9BC3Lp+h_*njjw;y^dT~=Ssxs;U5rpO{ zLNkZhykAf5xwCPhr~g`^VzX++V@pX*vuKF$* zyF`?*7@AXSVy}b4kT}+UcQ{-Fb=ST5VV`G3t!iDLiprbf9_^mMcUH8fbjFQO<8RoU z!gcV$D`xtp--#<}PSyS|ycODM?yfx!R<9ukG~Bmy?0+Q;XRz`ZQAQc2bm|_a(w3l(ZkMHZ(>(!Bk zrA39^Otg{r-HR(G94kpWDRR)OG1LCaQU)i z${5)=_n!RP(WhCT<IwWz_pYDTHNCcIU6YqUK(AWFX{K%r*px7 zqWj8qk+fK(nYd*Eh3@NX6SpJms@{A_ceHpK<^Lx4%e-&x89JmASWJvnn*XUtY-`E; zrj8MlzH_NQ0$r(e8apz&RZwov5IO_p7A7qfM-U`0DK2LF>hFMg0=X{`&CAV!(JBnw zZwTXZcE8IRVLuny;Fse+X_V8k1AUxXk_S=z_8gKI^|@DY_#w*fYpxvYzJ@w!_$Xer z`*?hoC@DACxT5}*UHSl?vIJ#@D%g)^RYM<0q>1MObCXf|i_LPy3Uc zKFVITKM8XOoZdW>O89FDB-_mE8`(|AtY{+r@6UwD-L!YIe(RF;@}spuBRn@pT5W&U zF}V>N+jqsv)m^9ZZ4s(0fM%D5DlDaUBN~rx9=5+7(NMf}cqr#e;E)n)LAMreY|$xT zQt7U{k9y-^Oslj42kKK!uKN@*(5=-_qPMIVklz3gH2;vPy=h&d@0Hz-@=lWtt4TxI zdAeSYj%RdI?mF-?kwrtV;D+7fq=8%eBC?S6Lhrh8;P3g&tN7pUK3_g&0odmK7iOq zA-{e$?fwr{Z#nMV_3SQyfrv~Bvxu2(#1|0LDgs*dxpdd?%|~H^GgWW%t^kjFL>1CZ z;n4q3v&69uf;x<>n2$6d>Vx;}J}JRU`S}dT3c~5TW&}<2W~qF-XHJij?uevS2ap0O zCuBN(1hBT-W>o)sIgV{P>J%})j7%O*s&VOvELiFU?LUX{|i?3r@@45FSFTQ!I z>+mG$ZsH0)WVx}n;*^)%nptK^hXLWBXJFHAPqSqm@0zWVrFAG7ARwoUIkFeeZN3&t zrmLvQ@_sU`5q^h_1&iDP0V0#Q@-p|xBMt_-DL;3X3T*q*m=-TdwX136yag^lNDB%( z+sFi)=d0`3yXyelR#_Y+^sXl6!L^!P*3cDJO;j%+BkeKKw$D{mk;bp~c+pDN3Ekbd znvk|pou6@nd>VjVHyk!H;M0`hV~?HXD{jxP8ZOPfa$+ub>AJe_#Fy?|MgKzWI)ICN z>mnjfd|?tYDcIatO#vYsjaV8^{^c1v4NM(}^y1#o#g-Ez;j5kxK^V@{Y4ibb2jck; z<{luWK9CZN3{NT8fAZ__oBclg5W7-PAviB%dwcHpuWNF2&WmVshA(rCuCh^E@Y*oe z2fXdPc;$xiHKPY!uN+zDN3T#;Qm3|^7u99p*DH{6YU`f~I*b_qJon1t>$--80f-w; z5I;Cw=K!J9+iGjlKfP3t($M;loG($8e$BIONfLf335chGmsLrQI!?Whnp9m&JlkbC z$FX(Xh6rNhWxUD_u{3Ucilt`14EALRqKeZ+nbwzq=iEce8HOHza^?yM`DSp0&8wWy zRnb;mh=Q(9bi#3#%yS=luEc&C;qe~*QgBfzm_E;@%#rNH4ddp#Yr+&*7Mn1xj4~b= zWXCGwni?jisCZ$nZZll9%A&&KlE*+<5AYXm*f%Bg7Mn|(yYSNHIJKYe0nujBan@8c zufZKA;UflsRi;72FC)fwsKOJ*1>JC=pYEXbHS#ez-w4k6&7^5GfZPg5iQHARyJ0BX zi9|uk{U7KvH!qJzCEe?Xr7j-KRlO==z9tkeTvS|p;>&Da^PB^YDF9cQD%3_L8w9HUW>DAo1&*WzZ za?eQw9x0@KEF_kbX-HP^+7)-NBz_#l_g+_O5t0H+wy*KMU;RS>D-Jhp&sku&dU;2`d6M_b?daotx*EofbSgd^+^7eZ0$rlIMfw5D_P%1-=9X!khEM?EeE3%GmOvW~&@fvW6Nf+eT43%d* zlO%8M)q|1-{a&}%nC*p6=I4H)e|4|vcz))kJfsON3a#BmTrdV_3^~ex;n7Mq011L3 zVyHe2zhY|;)ID0|SHw%3Iv_b3k+soxCsRwLQm+k;aY`yhTxUE$fgy*>xOCMjf9QXZ zuM_84p_r&Pt|SGBh~w3I7XsApySk2drtAW2<^pV*284K)3#BGUV5?~>pUziqk*%XDZe{HpGLRUh)QrI{+ab1VBYkyk! zdqi%PGA(9^gty>MrR|NFKwPylIr+7{7oZp|cWU_z>ALH58kdPaHedmLdE+QM^_lL&=`H!h7T(K9Z`t!4bY} zw~~957}9;rld_jPSjXeV%?w`BNECF82c_FN%s!@>QghcbGL4RISqJ$FZHdgCwreDx z(st&Djvu4iY>C>A18fMYj#QBx6ULpQU}?J^-jQm@++3!V)it_#WWRQ7kzOa5%r}AFngJYrhy; zOo`URERH&uqnzKG#Tyi$VcN`3lG)uKNH7YS9MGKS5nukmKu_;wei+J+07{Y%hK|yJ z3nSz_`q3bm;TMXsq>b}7(0)%;>e|Cy#SP;v0OsY>V!OC*6+Yb*pQudlO*~6u5`Es~ zu;F69Tam-Mhnczbea(wxn3r+y#Ovr(c@dqIEPYSsJ=a^OP2+p*&;xlMdXiKeOYY{m zRkgGRu`qM`#Z3)m%sW_I2j$2{%n5e(H#ik}$AG+f!Oz(MK}pBS;nYx(-*sNu)dlF3__gVGvhtt{m$ zu1us0f>9jF<<#~e{8>AkUo?Hrxy0LN)}QujPcgkkolH{6;n*^H?@PXOxfeO;Dl5ZS ztya9)&Bw+cG*j(5d@x0-OwXEUJ|+aNo7ERLb2Yzp#$y=|phiebZ!rfgHw+G@TE6|@ z#=x-!|1xG?_yta>8Zym&{$yC&g+cOquP1gsy}-pM&m>}^6priuKxszByb^>ct#7Iu zd;FU3L5Z%@y=qkuN-*_dU3B)K5o$)O>D;;7eeF@u4!$p3>?pa8Yr}UwUy8fjBqJ7C z{+tNjN5fH2sLjyA-ziSpj23_T+#4FU%~d6eL>iu9-vW=3RW+llekN_NX(8ExPAzM7u8+p*m%wgt9b!nY#Uv-*KT@1!_}v>hhA>%{$wv6u`^5 zK0_7qq$;ynmTEA83`2r?x0fQ^&{8I~e;4Ww-??yFakP0Oe8P2w{sMbvOKt%M?ODNyyWrHLwXTj-tXx4R-Iag-|&N^##QBgz0#p?gD_*De=6 zN5{V!Vmf%={7wA(=?N~_0NlqK)47^B+GxDGrskuoT6^)0uppIR3Tyd@50hPFjS8k& z*1Ox!U;LLbLb}oR*Rb;O9_zmD=Yq7BR=t`p#pOGQ$Koz^=a+~WMytL@w=`**!p zruKYp;!$+Tr{_Yj z%osp?lncB77PqG>%7#&V=afm`mm-8MLlZeH)UjAW**X<-Jc@F8X@{M-I^~RoI7L&0 zhCui&g$3GHqtb4%p(e@b5URBAFhIK>g7hUSbb@+Eqsb^AuZtU+ z=unGknc`VX#UHrOTVp2BPzBsP(X8nhzeA*>bBSx0z~=RY41xBV48g=@UIy>dDWd8* zP9`l9o1wA`CF}R&&o%8nfH7I~^<5QJwAXs_WqK*urfpL1Ocb83_ZWXUBG+#880r$U zW5uU}UK6&PybNQAGLvc*#O1b+Rq&lyJrLG-cxm~8$GMG@86u${=dQ)Y$&ZuJ`RN2*;@>Tf&wI+)$1+s;k$`SyAcE3w8UUy9?_DE;g)csQM#oVmAj zqPzXw*B+jL_4!LVeV5c6ANdVf8{Q=!$MBu#*xgE+tp8Nr|4nVT8peHs2r%~wly`F2 zFO4+%7OZklYt+!QLsY)^EMlM0$sN-?YbYwnx5Dw(Uhk}7kP(LO6bLZ^WSl7crlPLZ zejzO#)+r~OQJg8RtKs#?Z?dB9woBKr!Lq>@!PW<4yM6XJcV-8!ycpNI#*!;Xy1Ulb z9t481fSR!W#+JG26`?>Wb zC0!7LUrlq3tM-338QZfRE2FgFV&0qjO+^g;BAoPvBzuPMyIU5@R-GHLFL7CwRI@DV+-`)C@-)O4$wEJaJP@MA0xhQ~VhcMN? zds%W)J{HHKdEP!og1|jLG^l#=>nFFi9QivH7v9Op2M0RA3!amFEH~4G)+i-hx{$7C z(4|N$K$r*ePky;z=0m4K!6Fu5ej8t8Q0Y64%nxnkI$G7l!76AUtZ5lI^RkG=Iz%Pr zo|!8sPxu57JsqP_>p4Cr>r9O>WVri_n@lfCtSsF7E#EAGcxTgoc0i#I->Fx{a^Gx2+zXC!ySdO7fKtmIN!4efFd!g$yG(7+>TF!taPg2o2F< zQj|CPMPUZ2a$dt(c@Z0-#{u@AG(GWU_EL$}Bb}z@y3O@N;Y+Q%^YKpJ6sU|S>+=NI zU&j5VNcR4ddoskV2JhSspJ<_bH}pXK=|!bXdv)3p=4s$PUweFt!njDso|E?CRe*<5 zN~~*ifcsOS+k!w}J2UBW7sQZRZ9DVmx_82O=pkFk=>({`$p%#k7I2^GXMD#OTX*wm zWB9Q7(`V#g7tr(RbnA-OOmx`?WG-pkJ^bbQA!Si*OI6jVbg-+rY(W$pRLvkeERj3~ z?C=B#8%9+g#(a00(K#SXGI+MX$7`_3gV8j|*SRV1u7y1)@tLkC3 zVYZr&ooCMMv@(Y}^OX;UR9HO5wcOg;T9!-3z;96HH#za4t;z2G(Ho%D=b0?TqH+J& zi|eL$tQkemPe)aYn3baKlU#NKr#ZH<>;+(fc7>??hz;{|tB#MRTAg)0Pybl5LDoY*B3cLC+Lp#Tt2my zPlolh;uWa{Q3U3v9T}8-2s9*-7=7+5E}Etg9=TZ!YKM%>)yOtJJwGH9y6AYr(cZzq zZF6J2_mUcEww!0SRS!l4rzjvVux@xolg=3zLOqSEk3NUO-l59h8wY1(fj_C?gFxL) zDmj_6OUM4RAl1ppK4AqM5SjMqR1~OUIxI9GKN4mv)F@uJcFy*R<||N*BD9&W=zrBD z8$}!^xJ!21G1ad@JYu>wWMwjQ8gQ(U`Qtk@xv8m} zU;)$dyYo_)XNRkd&!vD;A00&yp;FccJ{1oRj1I z6c6yfF008-Y3C%5)zOC7_B&Znn}}6Ol&QyH90B7!~~{O52Ic zV3&Qm_Q`)?R8uVN#2$m~wS&Psu_Wck&Dd-+Fq5P)M7&tvB2Ie|bd-TO0L5~uA=aGy zP@Y3muoV0u8eIiFN#PXFAW47Ykg|{e%51q)J3kXWV`0K$Q&qJK%)&?Xgp7G}9)LCq+%DOS+}vaLOBq*a9?Kd`y>F-2yn zp}2%msy6nq=d;3iN+ARpR*y}LI>Q!*P3mWdEq|T4?W+dM#u%k*v>(Fu3b`#)loeabea#@Xh3Xz^Teo;%0835Bo!ZA`y zBtHa;&7}ZILN%-;avmE=gm9`j_Cn}Jv7}l`N=hbhI;~cEtTK>r15mHzHm7NnaF7lX za9Dn5Cw8PYA4C?>f(>^1FlNAqGN?0H)#2tpwGdO1OX8tbE95{6Y8Yk7}lkJ(}nf&3s z%F<$(h|P7=Cp;)lGaZw~USixKI0jW0wz4=Nib$pMB%uT`AC!h!czgl6@!<6kL^BJC zI)xWeBP$Bnj;_%dGIU6VQr{pJiGe&uYOTI{OGZc2>{5v|sGMJayhQU{+<7kREVl$T z%*H?@i%Q5iKofygM9wcSj7y=Yd*)x0z#c{oy%2(iV|NhKvSr;ki&m%I5&JY67ajY8 z=#BpxwQ`j|Ey@`y5#dl2t;7PYO`>$LNLV-^<7A{B*OSLqv<1p!(7Sl7awS{oI~8-` z?g~(a)H{g}STBu4*gO=%arhmKqrfg9d7VIZx*n_5a{*dLqLe$4h@CJe7$ypv#HvF_ zUVHH39w{M9J`u_2R%_z4`lRBZ{ss?v9Z;s3E9FXAk1+@{C_!Ft=nRoizU73OSK|qX zdS>FJ>OOWV0Wa~24ael%(1Sx_DbZa!yT*-po9K3@6E~ec2?IqqoBN!L59G*upHJB3 zR3B`0|JdOhl$ZMHTuG%vSHHY}-#*5c3FE%Jc`26T@)fNVoyqBBsDN#GjIQzR6esBg z%vcN`@k>~09w@IIsim9;@F-Q6nl6Tn0^vNUBdF#J5|q;Jh?$zN?`}!8al9l!xY%o> z@?!6BhCIF;*%GETEXhN96-(P?XUuhvRL)jak7zzj2^38-pus0W69DS}0!Y_zIk>QD-4LKN~llO>p>yaTzXbE}vqFD=S1lg1W_*)5qfYB`` z@Cw2)Q^$FBr(Oq2-tZjlTSPmVy%O%2VLTb;tcB9YGHF=L-k>#J9$H4czfbvSHv+0c z&C?yBHzP_-(t}C^Xd8*^^L-3)4Ci+?BPbBV6sY~Bg%YrqO7T;R>>!U_6Rm+!l={%5$)cYD2ETQvw0~SXVIZ5P2;Sn&A zYhrb=&V>SFc+}iN@dD(Uxclvs?WCB(EIF{iQTip5=+T?eF(^k%K27uz(sjjprnXGP z7LAYc(`FG_#GNN1X24)8*fXDiIskP0QnsNp0t41VJ4^eNTHBW-z=LJR(7q?yA>hL=R}pP86tTyYNh$h< zC(rZfNHTO>5Piw{Q82Goj%dJdX! z&?HHd07JR(2n9c&5RKyEid;3>31XnCrNV_SFf43mh&KPBJQ11|g}`^|d)LXYX^l!y zv57@pEPVI!w(y}R_TX&UV{SPf0BkqxQ2{WSR-O-%WjFOxLo(7)MnNO>WS0cUw%B+# z*UqxhbpaU$NI7a(aq)8=D8$#t@oFjkfrWYaXn5H%t;o5_@TMgJq*zJ86sAl zTn-orw@2@#UIclAmQ)BUgz7AEhNp6kg%R=KBJe{bNJc@ybHjqs7w8bnFHCJ(&G_G< z(EJc^uQr3;T}MzdhLG6~#>R8DJEcl|Y`$SAY+91uZkIZ*J29hK!9oOo25EXWH&&_1wrozeQo?yF`^JxKc9qw?d=&Y&XelE zS4%Heu&E6@$2V>{CF$^_-~DzJ6idmf`r?*prV1t`p4Plw1;f>^SgCVb1IUP7&cO#! zAd2Dn+|gQsk`ZL6(%#x>X=-w(9ugyB1GUG8i_Hv6;68c)A*S)dgb}ogi7y~v??#<4 z7rf!&=jgiGfLocZw(|?C6bxA}hC5bpKwrP;$(dcxhpYT=pd;ZNec73?)yoj_5p!?G~&{s$2GFV!>zErg~$lR(VesDsp#e$^$rroX*MQJeN`98k_ypGu7 zqkCa@sK_9S+xQw9nOK=+)?U64R=XE#oYi0P_-whj-YqIIl@e?lrz<5g zK(N$O`h*FW#h_L7lM$ZEWqwW6G7_r>OI!f;xb6E^DVT(Kqm%DmqWSWsx$TNkkq$BYgiZL0#zP&g zq#Y{wq~A&4lNwpCy-z`SxIE3)0M6;zN9Aw2@<%wETJ|2wRp62jYk1==M4d#28Ns~_ ze4+;hyxJ?m#^a*|uSY?ta9$L6#ET4?TLHE06C@4>&H(&9VC1lfA1|zpXV~4wu#$S3 znq3DtVKT=*xvnU`T;z%HFift|y?o_L^vh3L$!wQEMRgn6El_XI!5xhpf*YXfU!;xL za8VwVtKu!;=LUWq=EPGeMAS#UDZJ`|GDuX;>_mo~!Sn!BwG2wq3rm46|w{N=+WB$I~zR$YiLVfeNfk8)e*{#Q>MC8G)U7AR)s6j%w%omitH^L@)Em z3`ns^JIxM6QazH$;wdUD>?Zh_eovCum3{0vsGEVfQq+7IbYHBsYdB38v^rdKLOw&> zCXa-MLl5BW)H)TnThUm*x1IVadl%zmhFqS&q34Q7G{}x#Ke03?6=90NfxLP8$e|p$ zGr%d?{h{G*jqz1Iu43!QdWSu<#h6Tii#hQDMU|By9IQ6|tcYwk?DAY&;p8qjo5Y^Na!0e3&^p3jjpCs#_R><(!xv;;8l-V^3TAj%uJvo zr|YWkqTUgQcxhrBh>WA(J8+L(pS-9|e2A>%GB{A!2TH zPGW6yzJcaBJ`xfUyx)%<0bOIVH3dusbt5QY{o5^2k9*g5mTtt;c#&l9Gl(G`s@OK;HcT-&Oi_>NX!1MBJ(g zCFFb$wF@{jX>F|677t%HsLx|@{+e~eos>03&9q0 z=XHZJgXC1JCT4V%LstYXXOY3(kAjR`&mxIPC+4p9ldv~p6)))tOoEq&+V+~jVQ4m@ z{TX2jy2OPf`KdI^O-)S$`6}oM0N=Q7lN~5Ywgimuh*zqVUx6MY>;AH(Kux2?iuXQa0i2QsOT%gIfMN#$l}O1wV4ncnI-&1tDTtY?VDpPMm)5J5SZav9&B%m^^ovTwE`(TW*{oKFew-*b@XKG))KSnnbM4Un6~s$wU{y{ye9n<%fYvLhbOA+7 zYj^b)ebl;bZL^*t4;5j5QfW3OiK?OdGA#=}4@o!R+N|`0l_-=ypMq z6b#D6>=%4t*bMj#G~Wi^52@)$vV^kMc`E74Zr%Uv1HG~qxDvAT&E z>Z6Wg9qq)NJ3_`w>Gyf6M=ks_kV?8*e-NXngiyN%$;2p=VG{EgT=W!3dqXLlPKc;T zOcv`9EmMlEEU$XC+Gs-~g^f(qi(U_oO^4G-3@Ue}pvHOzICSdm4g}I)()o>9+goi) zv@;SKBhCwb!^)Zo@giSi&OL|i32m9!Cw!X5%I(UczKL^LQOX@x0qVv)mfPG~C$i&(t`NP)A8 z8Xg^_mWoQY4W@>xV>kzQz><6xQ1yr5MKobt%5p-g*nDXi`b7PQlzwC?rP-<6Xy`5t z6s2)inE_*4-C8f6Muwgr!tmK5s#VbfB&>)yR`K+m=~Qc<&Ay&OG{Ng+(jn(_5{W$7 z9O1`0D8bt;R}%;LoNpTxW-Z(-ayJl4ZinomPIJSip#k(T4350WaJem0)PmoEfff;m zQWao-i*P4CK-Pw)MUBDIWr^D8rNbK~(A0>>k=?dr+#s*5f{|+2J)yFXE(Cd*XoZfZ z2NZIc7aCnhAyQ|+o1T8GsC2O-a+SI$vdTlmIK?>xax(e2>II&-ZeLa$2q^Nbucz|u z-*25gSGPK+H2o6u0&)BrQucoA(AQz)3o&{+8h42n3d4S6T}KEm|?n6n#_cw%+u!aUn_-q;Lr?=QMp+97^@)O?X@Z>0*J!3v1+d-R_mMd ziUXiz;uus(iaUsX4Fgen?&1+>gL zZkq|Ja{EQGllU6+m*3J#mw!ns{cc%OK`>Y7!e|+erO8MC2^>5DJ%ZLoNc-Wqh@@yM zINrwn#N#X!02zkcNU2#ng;6;o(VCPTWTl$F$V2-ETL5j3NmX)FdJOLD0 z1g9+pW>bFoC3RSYD$ zDf=8nB)}7;6xhv^z-QTLRsdcL3>ie>vjVnUAdAmuW58=0ghcf3iDdNyk;MLwNZ*Lm zfa*Sa;OMtEGGFuUcc9{_@kP`KsP7XiVQ|Y|Ughy!pE4lk=#z0h1j^92lAArDM0Z0T zYT*RAMi2OA^wktz62Tgf z$Iu}qpoB=bAl-GJ?dSVB=XcJ!_pWvRxw)3h)UJtbyGH|^jy_R{&1Ljc)dDSz$?&GU;otD>B_HG6gIdXxGpYi z5O0AV<1b1b{^54J{l8j(4}7R{LffhB^>z^-(=S8;hMWb9gKzI6rxdq=92p_)FAW55 ztR$`XSMU%@$9;5kUS}I}E(3H(w?GMVfTGmt0Fo~%d%^__@_pL-hdV)7e71g8Clb10 z?K*&!)}sHIXO^_A5<)2YNs#I(ZiCbn_$5Xs`;KFk zxh5il?;`EwLi_NJsEr$R!PMmN^MHNy*UYrfFDq>$uZF?I?n6Um))rVI-iH_Dcit6g zL(;m>il0^s`*`RqF0S5XeEVvObNk|E!>oW2-Y3fNum4Ql2wzFPz_(#}-I`i&>e3p% z>Mu<10jF@ky;CJZS?Z31-$8@c(%odcHhdf4tbsHvcGS3wAc@o?iZa6E&PqC|=h3-Dj>iMTe8Y z<)91Tc;I;q{Wa;3^jq-1`H!o|kuM;J0n>9XTSh|#v0z0yavX88(j{-Tv68gi$Ai`T z@(zB)xRpuIf}L@#4xmYJNC$XMKOd?4+9f($jRLFkBt9eia#YDEpzU9e7#jx-xr`(bYA>ZJ?X{xJa8msgR{ArPA5_3w9eImALE6kOwk^B0G{_g~8m!XBG z!Mw|OCTM{eiVYZ65hxlMtQ7N{rM)u!=??GniI2&ZB17%hxuN7G>Zs_n|DsS(*t|o@ zp~8iDOu$k~vfPgQziZ^F9x##QU?bl{f!TSz<`V_{NfQ+!Olv=~T>~OhLX*8kglay| zqy=_9xh>S*o*Bt+)NS2q&iW%w<^`>ut7!6@2OW%59I_5)8nj;&1gZR%mR}9&mzdS7 zm-AH?jPJQWo>`8I1AJY=^Aj7ym}XksQ?Yn>hjoy$J?^k2YZ&(>O2}7vuHQF%=Y{5-*37+E}zn}DC>)1$@@0!$2}>gDw_i@}cJ zNxOMU<9AkWxkjpNJ^En6_3429nhejlYVqjOSVB)+?L)nl?^jdRn@qFz4$elc#3I8p zZyaws`Um`Ga6~C2fHu=^)Vt=O)1&Ovp|m5#`@>Ogg+HHo2fi%y&+InLdHv@1Pz`GV zdoKQjBX3M$^xBbI_0iX8*M~hTb3@yUz_MMd^1G$|z)NJoi|LkOWqy$Y>l{8zV#cq;xn{5*qf=?LFYg5l|j3NKg8#GkE`K`NlL~=l^W=x#3WFuJsuIsWLJwDPu=!e`y;y8Yafw8m8)yimysQwDUfH!ApVxk;!^rG?>)@5K>tsl zWspIa!H3vRUO7pBaINi25f}82sx3w6cj6;8mEjLHmtVZjQ#-18CF!$9PM!c&mpKP^ zIeuwUSf-$!<^Mx=w$9YNnB2<3vn3U3EQj z$^vcTfd2IYDYbqzBBYt1`T1GpiVJ}423?wpxPK7QEj7jNU-A5HZctDq!!>%hbSh0U zubG^%phOIxJ__#98qL42B%&kiEL9*NK@_w;%dJib2vGD4ir{&Zhxf?POYvV%kkx%- zJ|xcX!vqF7rnY~srme2~o;hn|K!JH}D%DN*>+P43XgQ&MtYuYCmGcJ;YlVva0G%G# z79^;)@N=Q?eMpZOS_3Pu^bb{?WSFXqY41WbH;q%yg8)e2a0xHFpWUTh$mjdto`LSQkTnUx>Ie~UK^clY6jTrd6voJ2u}>z~TS zReqPdA5}^8nq9y*F{zIz@VfkrBr3!p^_nMMJI+#;1~I1}8$43*R&*|fe%yr{$4|Re zPJNHhsjl$Vs(j~yRbmuLht;v_>WaJ2)183T+8NoQMK{3KW{%OsqG!LhGHB$fcgjRsLdO4y^o8 zOE2XO4e5gAGD{?DLc(lH4e5l@(1ZF)vCvPd(8^pQd&}6!8;V!1P;z@DquPQ&)bTb^ z|BarZlsKhO|D)T>1$o*+#o}1`^stX=#lX??*|=f=koZeLPU3jQ1sGP~pq_Vt_Z<0j zqZk+KQVC8%jC}6yX7yglz_O$iPA8blDWr*oXz1uvV19!3s!>0j2JwPTz`4liv#8gB z<8$C9`T)!)$-IhRovz9Rh5s7r3jb7C+4e|vfK|@*joLAtQu9l4ot-HEs^dMuOIA*m z2du1)Pk*?op1t@ap**s8zy6{N9j-j8nRYo0ss(->Sa9|&;-a`8Khq#?F&hjkYJlt@ zg4UK6k2?)#kZ{I= zaE@M%RyG&CJWZ~c`EKsdZC`fqv3d#;mU8c`oW6sNXflnML0|gHz{}hotChI5(92X0 zE{TN^B`}&i-5@Vo|HMSIYu5C0&`eV$R(GbNZAO@LboWBj1SQ6y{xGQiWJ~Qi5X02c z1`}WwV>T-nB<~jd0R|&Z;2P4}8yp6aPYK50!6|`QsBbcejr%5QbomipCcO0IoEAlu zZHIW?7MZf&KhNR`h1>~U8@-pdLpRoV4ulNZ;9U&>_Up=x8%EDIfIsIIjJEI^mT&@7 zQUsiI15m`beX_?9q%5-PWYQa$6Iq|L6IYN=gcZ}osH%-tB*so$QpsIf`n5^Lt=K8W zZBUuDV@`3ewo)wY(_@U%ptn#jYO0w`?kxa$`)^Vhc(yaS-#VQ1m?a5|zTm0^@c3A7 z5&`Hf(CefwbSEobdtp}Pe6t!C#Ee|+`P>Vr=*3@+iB4;PLQkAUPQ2ieYw>I%e)(ry z^7(3U``d?kw_Y)1>w>_jcP%YSy!!8BIG@3WDi8po6DE=H0?=Rj)vmUOqj_2^lBvo~ zPo6gg5a{QsUp$nv9+NxWc`aJ%v;WH-M)F4m`yZM4oVo$b`E}h)rNc~1sOuDFXDkd? znnKti!jjjMoyvM0y#Cj2e)+(+kOwl5bO5kzCDtCzl83}4?AQX*GH;@ddp9?(;VXQ5 zBTmv5!?X{?fGKa@yqS{-I{{tn_Tg%o?I27+Y^?()(I5z+uxjYbkdbm*8;d{MUl;Vz z8+ni)N%Ln37@|7Y0sZUFYf@RX$b=qGZme8zG6VeYPC)TYQyBENXXePnOFrbfrC~L-%9BG=c1?boBoglH;+#Yq=`g0@Iy;3;GzCa z5-Yynx)e7Oxe2?%V9k#rnT*m#)wAV+K)~Os3D#~j*&hfaHfq1x3KjV7_{UieV4gJw zKo3G%?`MM~vzXB*3B}AD$`LUS+Cc7!7Ob-)Bv(C6G=KT(X$Hu2(glh(n?ELu`Kr3p z;Qy=hda5hLSOY!`h$?e|1uX_JVuJB}AsQIAQj=fGQh zwQt2ql_4*uB>CCs%bV@RK0V-~;rV26ii>>H@d(6;*aFp&s8t8~YAd(ti!SqBnm1rcu3~oR6E^gJ)UyHM=0Ob+XIQ`{s%F zZ4(1zuE3|%hRvFqNydiZ8QH5_8~VA%U6iVI;Vuo1bU2uctVdLMcAUf;^at1QKbCnN zIzL}bcYixc6V@ga>U&Whmp-~kregNdwfg3>%eO|zxJF8{PK>WzOI2T(H61$^E%1db za?cktea2D|3Gy+J$~)qB(T0Z$J*n?XR1}UIQ~XCyUaZ$${!D@?yOSo#>ML?3T#ry6uRS2Q=1cUg*+-6dh_>+;C z9|fj%mnm5ZwP%WKvIG_6#cc~`zoXOXs;s&ei~0We|h7Pstv87ln?r^ZW3QQ$3yLAzk-ZIcYA4*EpY)XW4aGtW1^> zA4-xkvqHtO7PXlA8GZ(AoAB0d{5^|JZrfZOzBUW;kGJc1#7ZTvPYxMQhCJWOMKg<) zf3k-_5(l79@AZ~n3s*#bXyJEWHJ~SV;6#z#XH{bE<<|1H$C+Y7%hzf=L9B`(u5gcX6 zZ)Cns(1=JcdH)^W9zoJ?-a8*TH4Hb}a}%d#r2vUyRku-L>9}{V%+5l`(L6;sK9nS@ zw@oW8R%P5!+oY!zx8es$&3F$=isOW>w^U%!FssHeTka2$k)a=??ymfU3D!B_)SYa7 z6)r$skwHSApp&ks+vJ#n86Op*06rqMtomavjq>AktARkT_L^r0T1mIPob46Z%54XO z+9EDKaKLMMY$0|s?$S4URZ_b=>6=2;jmtcTc1=wS?}wbo;@Il-oDe|q%uAqGt4d!w zb^icJ#g;+xRf5{Og{nEQ6`rsV2;Yxreitj1JY;}h71v-cgCi$vy}0qMMwPV&IC4L` zUckOV2t#U6J`z?@JiXc;V1O_wia>YrAt7C8AdB*ru0I}$RT>037Phr=p~UQ>_wr|4 z)|?a9-5SA0;p&gKZZz@y2xp}}I2lxE7`cKcayx1tFWDJfsJ6O(&uz9Tk) zo?i-gt)t4KoxOyQDaD1H7_^@Q9kx3Vvyzm~?Ean?;(Pj9iU?36{aXD#j*Yx1@b5(Z ztsv-qagoDheT6|r8m@oI1qw%EwEn&Y4dll;yI1Zbt$iGd$zDhzSk_2}T+ zGIg%ZL~F~Dd-KAPsXFSvjxuDeE04)>VlHbjOJ4gFfTc#6_-f3GbE57~w+5S&Aoy#Z zt;NdAWTy=|C;#g!j4U!8Cb0a^AU+ zuNsR+q^%p4lR$pZkqpa@6#kTNTuJwotWr>0oKuSc%IC*-Z9x$qSkT~(o6|Sf-8PG` zTefBxK%woEDDG5uzccyueB8i=!jHgT*vzEpUQ(5=o*q|ta32ZNh|m}Np9xcitrq#+ zx@`ENb*hh>iU0K|Qhe<0+}+!zI~)Ks9Rc|hR{ z!&`O;|Bb&O;~$pplVW0>S0p>Hz*KyXS2yN%%XRrs4jXccW5D*t5Tk_s0z@51WwlC( zBZ9S8l8CP$AtIimJZF{0G_r7>vtZ(-JbJb16i5J$sfw`2Fwl52?dq$YfSEJqf|`wx zW;1U10W?HmKczA7*o4RyNv>&ZJ@c?JmO1}t;D?o0D$K8#)IVRplTIWr=pjUL8qUR+ zomMt3EE4DBd{11f7m0;J5p?xh`Ja2A%sj+oaOAaC=H7?Mg~+%N&4cSy z)|*LA4=8conH5>cOIllsWxP^{BS;yEC{8W}M%I%5&YB^lzJh7R@nnlaxV6+J-LhQf z{c-dOWyiY`5D$f1g*ICsBWO0lAO(~tv$ThHwbBN|-CO9F`ArHIY$23;2?$}P5>jI8-e+5r@V{-`KYA~TwF|B`eDMfu4Ke6}poo+8eU zKF$yz(2g`6m+`F40p7dbzwKt?LW5dLM`cW|3E=l{GahKFpvoAB6*8f>Oc$O+MQL`5 z+*jvhxxmOQ_e_FtHXoBW{v1Z>3H-T9Bh^1Ai!(jjKHnA%;z8{&&?wr;t8fsfnC7?09b z$hI^hup}tgI%4hXy4G#i+e@LT!eH}pCvo&=Da@=PgkPYD<+;n|w8f0@0q}x61nn*t zFe!(cD&d7}JnT9(VhQ7U{=1EILi~bUwhF3%MH+qkHFu206CvIxU$d0FNoX={@OeJx z*Et6iu{;Ehitgh5T4!gMh5;0pb)|JLdAn7`PR(RuXe7g%f5D{sSF3@XOdmSd;2+QB z4_1|bJ(u*iylC&p;nV+x@G>=L1#iQE0}Y~bv!v|Yh(74IazbtR{TDlX_fnne<GJLNw+8u`kZ@5RWDq-yDwQRA@|4T9!{Ez(5_>Z>&Qn%iGumQE(x_g^x|sR(YbT1L zFt=*Dgj%hQSIN%v(&^4eUdeC-i`dghgDqAL3kewTi+K^j5=PciN&5^1t+~E&sUhSp zH8eo-WEwuXg`gzAlbg?y5>vV(j_i~wSDSaBxg47OpoB}sD*OY5)RQ4RpTw_+!J^0@ z4$!2)yFSE2Ft!AlauvU*Y5E}cRk~Q~gES|raY!Z|xlv(z88(rvtD}7ZZK*dDPei{ zX6g@?+gtP)U4{Qo#3w`J%Zdbm&rpRiA zk9jQ4JiIgLzbjfGgm4@b)O1@P3E`*k5AmQS*C&gkp{Dx+fD#CY*Ui&W5hw-gkxeX_`Y;AK^l->mH9TPU>USAgl&b%y{*9;04% z{_QD~s>;awi#L_Oyp5ZCkyd)`rt;`*L;`ingZmxSOjiq%ex7lMb5T()ZT!Om@Y7VS zb;bWYE6I$tRY;@3T3B^N_si*I|HxO{6= z^fCeS;%wHlk1D~)a%w#;;Zfe?(l+TQrMVM)>LZ8V-C}Q9#9Ld^DBdoaJB=M34e5pc zR)1CAv-x^~k!V@fWj-PRZ9oaN+K|3<4Rzo-04UydIjgK+%51%~nj%r5M-OE7mUG(=Vf zjj?0bBg#FFI4UgJ2eW6ME1Ddn>Tv@~Du$q+cn_b<8qe+;t@slDh7{EfcZW8_4P8`- z+av)Yc5NL??i&`?JG54ZIFV3;h_CYa@m3P#5j|?J^{+YDKN%+N2bqv3y-NkRpHhVY zPq{r{6aPA=$*f@_UdtVPc1{hqC2}en{)=G61eqnz0Lv<1oAv*A*Ff3u|E3%Byc-ash>hXaJm1$ga;eyXl~Iarm?&&)yo1jS5^JmD=Mv0c|FnxEb> zo4K0P7s}z|8;RcqGBh}II=Y;zm9d<$h+@y%9ktpfEV*^!c=-wj zA;4bmZ!I=M^ilpxGjBM>n{xk_>n0|Ok-9G2kh1NSedkMYP%YbIQ6&?O*6Sk&pUF$E z0~%F+@IP{qZ$=&B<|e5vcWy40jJ3L`Kp6lFOA&g2M|0Ik^w-DLu`l5hKIh(WXiaV3 z<1erm_yaiI>Q^~G9QZl61Jum9z%cnuYQ0ubNJvO`0mOR@0RNkEAR&!vMF9{%3fWKA zrw0-HP7KJd{i;a>LUNUZ?$?*e=6k(A*_~`mH|zcZ;ZBpfmGT78#B0@=#~cN?V>z9Y zj{^YFOoFj$VZ~keR|^2kbnrUve~Kxttvm{|t3}Llnd4&%8_rZ`+oNHVnr>?t%|kbk zKCc94FoDKpBnX-d&?ILJ0H>)9_$6%jl#=w_Vv%_+3dhF3N1(khrRrW zO2=tGeO+KPeFyOKaorveMWqAavbPV>4k+xM7dE#c^mElj0Sy4ee03eH;eY_#El4A1 zmR4fb>8v(^R|-k92As>A=*&FkFX$5{p_Ze^MRdQ*KITr>6ZfSsSW_# z<`&P-_T_Fk&*7f};jaE0B?4Q+k!m+S5a6VCHc{{W;xVvVp49wTGw!25M6~=_jFQeB z7o7pFy3`{+$=SUJJSS>}^+zAQtN~oN^TXJIf_iypdGN!nSL`rqJ68N4*wxMIYl6nY zcMvC(sId@AWC2{j0ml}(J~N@0tqzNe4VYFuow=cV1t!^`D8lW;h)-6mNKCTa{fGTm z5<-4^_UTMZ`3GRH=?L6UAusi9kbH;)EP683lNC)(;oMvsN`ttS+PYg+x%bxeMQh&E zJ%SE?U_XO{(+HGUbAZ=Z?)Ky!aE-qQzJ)RnvA!}=%mJdKU;P1rY=;tO!EgMN8M-Qc z&d;pGQs3ESgIp_^Jm{}kujlL8?{b%OSx`R$s_gfmtLW!xGA*-!*d`X(wEY%fqK2`d z_sl$RR$n2H#smoejemzg{1;!t-~bYHB4Ac~3y$dpmwp4X;rAd(y+l2RM(aMiLI7lu zex5$VoBZrLW#+~qhy39_)o^yi5$QRzD=LV90L+{t#6UxX>c>PkGhy%_wV;;7s*G`y zbjYVL2%NX<=C$;A(K}QpYalNE%|zXcpAL-D9z|uS2qvNeSAS?6DAi*jR&Q|H4;bA6 zh@rq|JnfH>m#)YDz<^sbp1?su&e>LIH2YQ~e}nEjhU#1(+I6NaI9c{(g`#Z!+Km%| zyf>lbQJ=t7`Xbl2iD;-_AZ%%By|S`$hab9l-Pi18a32fb!;#g(MA}Y+D9ah3X}LHX z_XpU^K*O=o58N;*xF59EpESM9_p&B{{1yOi7EOE=>R?eNvv%vAyQ5p`p7fOl@m?n< zD6NO1@gZjE1i-svnZBQ(yExZVRhYZ-qf@WV`T)NM7aQgsf}p^UkcRhGIHa3J0Cg#; zx1?ORdyCY%ef!nj@SRuy$n^0Wmb64gZkJ{l(433}jz5fKI(rsQlpttOx6%3SOx^~c zC7h8v;}LR-BLr?`49h+lGT9A*-Iuc+;H(gWw2dezD0FQAqEk8p`ab!O{9eAlaYRb)EZhhI@HpimpHA^K^~P$!I_dpQb!sACK?}zlqk?I$K~*?5+IX$ zFT>s?%id>ZxQ?qMLXyUy#6-P`F&Q1yy@zk5*BMX5YJh?^aYAg-&=jzAN*?2gi%#at zlwx0}sPh4VgI$I)lqWm*EvZuO0x*Mx*ETKQy};xT`GcJMmq)fMAPk@QNAn7bf8He? zxL6IGFdn$5Q_u>n0`(0su#cq`s-KL8^FkpLSaa54XcLVQL_q_u|3ZbY5gxwYIiMAJ9ptAb0SfyzxfWDK5jG$_^H~+Z_uGK079{=#43)YO zbrHuT@TJU0FcstAZ{b|@m3IH-Mh9Fiw~Sap?F>QxWmc*`dS4;fm41+et>5VhE-99M}%gGEcfdP>Q_X-<%luzkqFA6cD!d70*a1;(_OUNt6qo zuIKp6U{TXz5@1^x`RYZiVCj;)-rqI%|MW5-OT|$1QzG0^2496G1c46`+J}E+fpUe{ zpY-duLc*F+tV#?CpIU*Cvkf*btEm)I(_GM~QU&Bye2vBoRl70peHlMpjv!i8w^+yL z_igP>0$Tl4lX{~P&S$6GO+khSBn%JWAdg|Rm6en6jQc6Y7f`JeUj=77h5*GpqFneoQ zNns#U<(Q&E0(j&OW*bj~l@!b@@8AkGFR@g6udyEz&AoTyO$DB~M=It!A|C?(j(66!0Gj(PuAC7Hvms^(A5qnX-Ud*zIMDv zQOlt0MC{HqR^$n8FN!ru#_uc8=K@tPF0!5+vbylK5!BXs=d9#>6S^kV)@CpwX3X?# zzOYTg>i`^llqYgyw9TG3T=6vNjMk_?yB0O)jn#hr{xqIdVnm;a!PQc+$l_fDKF|qB zpotQaySd3RFf9m-KpcGskZhFgSeY$K7d799VlCy_c7b)i_y-gSa{@HjJItfcd!^PZ zxuC_q%*#CLj2a~F2+Hvb+N{PEPvfP`XQud*`hb&y*C+Up$#X_x)uhU~^K&`KIGa0# zx!m!KgLj$|e%uVB&OSRmp4@YJ-tbNZ(&jF&WR~@+9G9f(q(LMB%1|_Nc23Prfh!~M zCaUYl<1bxn<(5J^4S=ydcCP4MTC(xfrt6)@jI4WW=pfzifVU6Pf+|w%)6y|u0qbJAX(cpU#l>^V6#<-$l@UEbrG=j{-IonuPra!SiP>>L@_KCK~di`<1xWG>u1orL}>$M_s z*Yye034a%Pi%kq=%d7DYB7??Depef&??R+S85mXzzE!XT9qpvP=5f4MF;9>^QqB-Y z<2mc9)$ZS#R@@N+O}!ktuok?nj@Ct|pz$0*oe=>=A^;&J9nNZ(0i(;$P9_s1D;}#S znCo}gU4;I=OpkC(1wi&Mmfj@(Bk|x3$nDd;^6BDLe5kuY;*|2tB@Le-5P44?gui$P zjg;ByT>`O^U>UQ_CDIe7X4q=k{Qj^jE*oB)KLvRm@iVI(VS*6(@jY-;*G?32lUm zD8-=Pva-nfHhh{RKsb7lx&@?#kz;+x>_}FY1OS|@8wBZqDn3^+7xRf&#UyCr2rv~6 zoRhFpJOYg&-$;Ng#KQdZ#2v1l)|!Fw|?QtH&)kBz4Fm z$we@u?^LzL@SC>95sswyUGLmep@XP-G*L3nb0KAvtaykIpt?+%%c3UChRYB!P6Q_5 z8{7cFJ={)>-7HG@z^XLz&TG4i*N>!9f2`6e#|uyR{vAJB6f}o>=m$+v1;^GM%!Dr& zj5%^b62GYJ1CKt&Qx!R$G}IkK(QiD?p|d|`HxQJ%OLyYlup@5z_%V@F$FV+ z`qhN&x7JbD42tLi8gOaIiAHGfZ{DQPslJVm!YAmQe|o-6`h=Lxckb!aeaiY{>3z^P3wz2G=roQd-R}j!wQE< z*>ju2BWLEBMeV6&YADli+fOt@ZL!MPCdyTkjEUeA$%F@6%(K z#@zs$`TkUg`ebt&!MWMJO(Wd;h*%akdou+%->Ji~$&T&7S;1TbvB8e6SDsAUUfd<9 zCCw2vo`$e&LCs{*h(Yf#cENEp+R8CLZ!?y_!i^OYd0A;!2p}@@jrO- zD)^P>yzIG*dsrYHVoTN2OvJI7L_E!nkX1xPuUFp1lu_8@Abs)sVLhrg7emLCu|_GQ zr2-u!fqenD)U$$FpY!8P6I4eIskBvJ^RZVsygMJA-X@p2fb$gCL>c;;Q^l?BQ;Atz zu6OqPs`CXuX4rVcucg#pI?}R0if6?;5C>`qRuS?*HP+rkA~CJ!Njgj@R>*e%KaLaH zVB7_#7h8}X;f!EyIEbxidK5Ws2y7?rTlG*ae$3)}PpLh#^Fq~&dOpTJx@|5S>F6FN zDM8Ha2ZXGP=;9Y5GrSIW<|l)>Bx`^TBNfWDCxKX``fRsH#Rb)8dj)uSfTA!;g~nsr z%*l9qZ(CGpI?yrj>dJ7T&zLJtFj;-IuZqwCf2tyB@Fg?yPA1+=`|Ztbe8h__8$=<2 zg_;=^)@K+*-i|7fLbWzAbgWxT_+-V~hBXz5h^-EP&jhnH+``tW2Ui}?Mx{IaY00@L ztt$kMh9VPf_g-$q;h8fvHWG;=d3zdEYw3{W7z{3wivXe(%~86uG4BEXX>D0M6}7H| ztq>HWTZn(pF6a6BBIM!bZCgHIhO3=YBI7NH#N;`Tkii#6qq z(84`hmXe1LfmI1M7YM%z@g%bFkrIM$fKdFj^p{say@b9HI-lqs97H~110tyb7l5z- zjKqfs4=5mN);IX@XOI`^LkKiN9Em|HQ6s>BhL8z_tPszXGNg?OVTW6X#_A$a5bij* zkX#1^-a7){fENR0VHm)L>|x*w!H?8%$suY-4u}V>L;<&f)#3vLKJzKKFoXyBPqS#y zkTw>Wr6G!&|1{y6o{!rszpW}5kaul7dhu*9Y+Wnse1Zia`(o+nY4Auc{Nzlzg34ZmrgJY-~x($G&f?GXZo7ETE7{3k>f+O{y8`P_Tmi#Y#N?pC?#W_YU4&ja2h_u++->K zPY1s_rJ`f^N$>hPjk(>=fiP$7D@e5D0l5=C+)sNseEkL?`m_BRe-$tS$!Zipdoh@K zByJ%dcB6sr1RpY+vb^`7PXbM-JQvPGKCx9YETl$c<@@;A$idy82(`z}sf1hYGV2;V zF>X&^Y(-Czl6#Z<;tW^)V`_Q4n<1K9O{|1vS+`{i6&SY&@WqB&iwY7eBE5D zP#Do%X)@Q_#mi6Vn_MCINXMa$!yn#U9pp9qb;q3)e;!`|a z1lB>8P!t6}$uGz&r^n*`OrF1p6@PO-J~My0Myis)QNHpDdqjft6Q~5?uFvdM(2*%W z#0nz5Csg>z&9D8sYWAW7oMW7ZeZ75^H8r(;n-9#?llk3icINNU35+k31qVY@WSPjZ zzw?uV?~w1NOiTY6T4(;tx!Vy!QeNXyUZB}8?i=q7O+o^Du2kHafBH*ZvXf!UIkq() zBO;!K^(~;%!`*(cc=_s=?I{Xqbx7sc-^r8u7DInUY4*kDoALIQMo!8r#FZOwyt6+S zex@CN^DyMVH}JD$^haUhuF*L4s#LLR%_n2;Lzj`KL*IOImdA#YJo~nrBl#ycY>hRe z2;q)xz!#IzUtyYINlbV8!nnYYjGzbK{^wbe$M+vd!i*%Np9R~+VjP0enqD~upd(QIn`8;8KBWWMHOERlFMKnfzxPsvv^B$!f1j>k%s_*?h{mudh2b3;(K*Kh zoai|`^RfJoyI18SCkW@B9!CmKdR*^|calIy4Cc`bxF3HcG9Q_-uL|4;hr_F3TYpzH z{vtV9*)fV+cC9{38cf&i?4#)==Gg1*-wZeQUC}43jAqJt;83SrWh}NmpVA=d68ZZv zCl`~x;RPf{RU-};UMBH;hXQ10y3OqtLn43a%`ZQ)``M4uU*_AFy@DqbR&6s0SvSn_E2FK*gQ0sym*~z_ zpWGkt|F|L#X>)}-|I=dD8|R^Ky1u0-_C?a)kmk!W^WL;Edor)V>aZ`+m2|y_JdyY@ z`!5-~^dwQ`Rv{33qOElCpI0Vv?Y%i)@Xu3@d&X7nlg;uy##1-s!sT%IKFxlCRAOm6 zculKcKHT*Tf4Nou5(PQn7XO{)Kw{vRv&;~?Q>h@6Z!3jib<9=RAnq*Ha9rWUtM66? zTTT6Okh0IiLdh0q5u$YtMoH_;*2(#{)Z#S5ai^+dsALQ|2ie1_tzBo{Yvm ztv|E|$B@K6*}g=x=b=r_&C9(~bt|Qv>96FMwW4Cyx?OZlog6T~GQ=(+uzHfK7yjuD zaR~1}RN_INGFh5+zg{(~d@s%>c&RrJn4D!GH_C>CRRt=i=7d9}H!FXkH?cY3$odV0 z0BYI&2Fgh|mT(6M0SD|WesP~aU7x6f^Fv@%o#%D%5AQNi3pNPA58OXj)}C4Eu+N{B z+>}-xsccyBYjyB2V*c+tP7l=tmy$wqCO5Y5zjRfde6ii555_>`qpM|#`ne5?^NwZEi01yBqauUPmi6706Hci@L zRrYxH_A#ISd)CQgpx)O8jE+_6fdq{Ch{#sSogMgJy8bxse4AKkNEV2gL4gD=TwGio zKor=FS2_&=8cbxY*M0(!Gtzj>3tG2sWdZP{bANtruH##%s1pZEaI-uJBzq;7dEJf{ z$hVtwCRrDI8+aZp=np6;o<}6hF0w}xQb@5u9=yS)@BkiRjfo|1P&;Wi&FeZ??9gf5 zMnD-j(c$47f3S4?2I%oBA7B)5wmE^z;ea!xN$>0J7nM060yb_vS=v)rX1iNtXRTsV z7a(F*?R!9>*qQB-;l60O4-l-C!Mtcj-G+q}J6M|Ue30t1;Cf>j7Nk3Swe`4}cx|@2 zw$j`Kn753QSFW_%iazYfu)$&w!lEWVr@Nx|W1`OiEVK+0m4GkkI<4{|<+X;UGSlr* zm}b0SQc_M>@a~)SKJx3-Ge=_p@VQ*%p72~`ssW#%oz(@J01 ziZFTxK&q&-{f6^-x$NWu|74%eak)PX6Yw(LK9>}S?{BAYL` z?*X(h`{ad7&C175EnEi(=Q_y2`V@feiNu#{ojj(rw}$kzI(P9Fa)lxK`})&UvrYQL z>BZZ$xbydPyBx?NRf3=jMX>!W(nH^YY(|RM0)v7E016N;!}yY{Fm|$Je&_PHt*#f$ zm-@Q8VsntzkU_&s@3Rfr%q#9o{qoNefLSTQZDUk4Q^v&;%v8&^=}X{fz6_|hM7deZ zZE`0Ee~?q$Vfk{xL?Ch13xM6Ja`xI|kOeaj*>J;V8-w%QeP9RKYG>4y$lquiB#>Tn z+?bLN3p;X%dk4rq=dx)KyfM(4-(d06^Bklfe|<$=Dt(p=j<*Yr5)T#xl%S$*7S5F* zc#eq2e7pk5{%%+;`Dz17xU`DZRqk&j%VbV(OG`!*Cm}G48oyX1<|F=@+=3 zORMxX&($tufoU)g7ZXc78~%x9Zu}4+ovL*XP8T}u7(G7vHivq)^&x`k2)AyjG_D0y zQjj%No{o3Y(V!1bpJ1nh^BB4{9zxghpcaxW()RA87tT7q7Z{WwX>_vyy!fqBYJb5m zsw_SBYriwjBk#lkoiRfR0;aq;_=P$=m78zm%{V)n_iFn=o*P^&{oo zj+9<^cq*OJ7|sTGG)^D=6bResUkFX{aRUMGJPp~x&@EdzrEOs>X63qU!PZ>m>qIV( zA~4Hff=vI;GF%oD_&n9Pb^mGsc-}j`o{hgiD(RV?df_Liaz3vhXNGN4{62nr>!Psv zQJc$-7eV@AhTlEJ2H`#^0kmL_i@kF^NDWm4;}EjY30lup9e|oC@ke`Wd^k|>#XnO$ zY7~dU3TBlZ_hdJ|69D2i{x``%7f$_?bujNHPA>wng0l|$q)>ltOQ9$NLwCuUe){=A zkP?_PN^1uiU-#5f#N_B&c@4e25-xMae_tNj&?h~XhlheZdj2!!aLj#M7V>)5HN5Jw zXw^HrJ)OKhT4wv&WTV|>(u)PdS6HjdEF(BDYj=E@pCH(mD)bmTEXB71)W-?c8Pvn{ao(SjfauuOc&h>kleI197yqM(7 zpN;@dU((9q&)0CGp7;YstAk39>-C=Vkf6t$$n!rZo>!5D<{dpf@$IglE_tWj$ziOb z%Pb$>!H9<`ROm8=8!|5Ia*7aS<>Ut__W3;DdKI5e_({>ujI zUoC{3LR@<03lFtC%%OyZjOdWz{Aj1I2V+rsW{{g3ofl&f2k%1E`%NmX3BPa6BnYgc z#3~-VHPM96OPMk9Oo|RRYSX`DYTo6iuc`ccN7rFe9#_&}q8OEwH2J1YqqcH~E3F>v zaQ}0N#E>8_;O*MYJJ$HjedKE=%gVA&9PKC6w~a^tN$7FqwDrx`{G_wpmL&9`VW%8m zKmTqVQ&FVcEn2Qrk+j2gI&=M&)Y^+X48tQs{Q92^{@Ja{q!Sn0=t$!orSozqPkw$w zh=ORscyQp|qXzN=!KRwh_c}(MZv|k#A-U6a{%d$Lmpj`i5c!AWV#&69Xs`h8(8p8L zcpa_u+QJe)lK+NGS>%EJW9Ik!7L}$J%|uu3cThbO!*%1Mo$8$gJMw`C56&Z)r5a~d z&S}5%qo7t6+OWSHoG+M4ada6+%#X11{?siaOxXSor>O}}^ygK=%2sdusJh)to8t|4 zs|Ms38*?=No&-FV{`;;z6{UN$|1@{Gnw}u*V|Ar3X)q>>Tf_b_$;Vw~R`;I{pvmE> zmzOPRoN;&qzC_WBJJpFlypKYEVeW#zeo6(o?Eie&`C=4ZOY@(3MI^7sVJ#$gqij3( z$^vk|VVH{VocEWeGqGRRI%}tc=n)%%yj^h5vB<$x>P@*QwedVvaQyo9O0Amv0Ef)W z$N7;e&S&~-w0)O4yv}91Mjf}56=$jBCx|v zJTTY*UYRX{w}5bnbqF77j^jb=_Uui38^I>bVl+khvUbQlWPslQuxOF7>?!6a1QRd zf%xapteLi1$j!W$$mFBmy@w&BX}`-Xwq^g@$gdq?Y#Ukq_mg;I#NInRaz;sW1*I2G z1vxIV3`s}%3EIgw&hXhvT;A!tU_~ESdL`Le%;BxcX1pS1^&scXnUj7*61mWmmT=h* z`;37zgXM}$ZZJMnq=S~e_5Q+g6x*D$slAy0Fab(j?jp)hpw$Ie-%Gm6SUhv}K-@lV z`*>j?B+{ zRAk8PepEz&9qDGyuKo7*-g-`L-HWpqYom(F&+fi_H^UoYYGg2SKEEb;t#G9&P|Evf zN^E=-q%C~8mI%B7bQSH0+_icqjQlU2YfAuqH`6_^_=3$k(Z(iHuUJ~X4GapqH*yi+ zJ36xYCIZfn9(G2Jcl656zSy5uye#GQXEnX*5o4+2jjZ4RewTOex}%dzH^_Vx!OUEt zgy)C$Vh&b<^ujrMLIxF^3WUZBzP6A*yPldlKm0ws^jMLd`c(7M>5{6Nc@FNS zPNCA*qz5iJ6wt}xp!`qxtsI16CjtWAqurmT{pn9-U}JM*s^;i&ToRhg#cy_03EM?Y zv-1SJ9=yo=N9q0X?b15Cpxmm~oCK{UU*FN7W+#0YiG$~LuEj5BLKa-le*Y-bFOKy| z*CSIch)+uTWBTyNdL(2~2MglhllD5QE%aA=*s#b<>*RxNG=#w7h^`{RbO<5K|03Q1 z4EX;P;{Csl=>GqO3;6%xlkuUx*0K=2rjQy&*WY3tAN`QV&<*|m0+=cwlqTr@adnd@ z6sBZ9IlC49(TOGo2OGsCWpl7G4IH;yrR9Cgu5fA7Ww3YQHXZI!Hpw&z*8QacHNkhVR<8W&_3QC)wY-(l(#w*JQKjW@C7QP&NAep0G!|aZ8kIk} z_}QS?4+uzEs=;PCsHT?{E>Il;m*cDkLGo9ngevmcGx2k@;jv22b2sZP zf>ls38ZONj78R9XuBf13l?+!HVY&y*d`rdc%-d4S;A|HHLSSz?IXRWs1Nq215DOg# zzWt`WynHzxRB!?xY(X)Jj%T&t;G+);wG58M#l|WC9SJnQurL75yjC`i_?XGllx%tU zk#uFCZ{uLWIh?;Q4U`1YAS5Q1UPA+)mYb*bS~MbSXL00i08$5egA#L`LqOMEYhxI_g+Ib}qd{H=@ zF_6aw7kHH9XJ%kf0}=iS%@egwziMTGysZpy-9|Ofu3oq4$ACJ2YH*cOpc?CJSS+>u zbIUVT=7pH|c8~a$H^_a6&!O2~=*fXINz0uVy+QEocFglvnSE8cP~|VUt|)jAX$7@g zs*F&00`?dfATt5TC3^|fc=`46cx{n4dS-TZx#X)r4y>Jlt^tAJ4WK*%PJN9(sp;ug zrLO2Tf2}DVms6 zux=;T%#Db_S@OZKEIV5C~X3fwYUHWq-=OJdx;07E$@r{OAwWWzDx*AhV$ia%{w<>wvHf znOC<%5PjR*_glKV)mK14Ohyu$q4%%25Lv8v?n8{oZZwvI)oc6_k%l$o0m_~{ymh#o zm$?K`poGRy6*`ZWnbJO40FECSM>oMsEE;Ww=TYzpB4w07!x538%FsbRsHkZkAHLe% zBR#uVdJ2k7%wK^1tfpSKSLdI5->rAF$|@7?~usQlpn2#D53o_kpJ!Y*uOBE&zAo*5ui5~w@F~b{UxX4GFmOvf!3~rt#W4NsDhKG9jL-WNCG6+K+kie02G)I7-2S8s zwRc&gmbSs!Y%zD%rmFG)1bSQw$b34Kh4@$+L|Quv5>MnhWIJ9DRR!SZF=$=&2#iru zcP$Sp#CwMHC_&zvdFSRth6OxUhY_{*2pyUgfdz`%3y>J`k%ml$vaTjFo9gj5)e@5E z!Y^WT`yQ7A<<+gqKOh=dcCgX+4B0{lqQlXPn16Et3p48n(wY=AG>k${tn>*~`8NIlcYtcLX0gX0FT+hDdHEhej;kbMu2_l6ZP4;2oh9*on0 zw+@@orRmPD8vQ5+3K<|nUP7*t`3eTkwRnW4%pL8-HeDC2QmC^41I|hx4vTsWafVPE zs$;@QJ;(yao48Mzb4)}gX0ucp%my@mu$^NqSh3#s07pjNVcTt?qxgE~b&J<=*SNvU9~fCz9`Ng(P2qIFpJtBmcB1gb8z<<@% zjvS_n;0Grq8*i%FVPpN!qB*=CGwToip&)S>=fY?M=!^V6f;RkrxSjdmNTB>TT_&8q z@vEE(%C#T-hN&$N^4!mcXR{OLbw58vbQxBZnSD}7~MZ1|f8 z)CeQr72^)096d*5q<|EX{w34+c)z87A)2c_TtIV{b8U{VWh;fDg%e6)U>Bi02|r?0 z)L1LDN>Jqe_qdHBM+awmb^-v1VUPQM5CM{2I2)m#Nq~8COL%{UlNS#iVn0Z6ybjsW z;57Qa{m}gE)iUs{yfl+V^D(4ODWkxG2S1P-*D|n|q2Qxh9B9qgG&B{!J1`F8DpX@G z0{kXI*}p(MSSx6`{?i*sk4dASAD~bR=^Wpvz=vN0o_{SVsfPdZi1_FWF*jzV3yeyS zvaDzng5ARknG~btXfkhy35VhdSjKkcQe!6RFtMDG0`e?+!Qyw;dM=%i_x@UX!l3uo zsNgnFHe0+t|HX@=a}>Aq5qM}*bvn4qmyt*QiXyDgR=iBS=ZW~2wU#h7VKrxZiuPTH zosxqOmf6Cp^d_81Cj@lJFUQ_9=Ve_rOC19XGB%&%X9&C&Q4;hJZQI?Su6iFXvS&NF z_|&e@>s!`$%4{}TC-EXRgC>o9&qr)*YNjNMob*7CRVtP;WkglsGyI>*C2AY-KGgn2-lR27KJzJMd}6woG%TARK{$+~QgTfP^)Vm`LPKJ>!><}js8A1QomT=n04RJXK# z;$G$a_^@M{=QT?u%i*7x=G=06_0{IS4@#-oT8thZ&XdC~@wL`w1q<^u5{ew_jZAB1 zx?c%Za`W%YK}ENiU5-_1bq;|SU5chIyC)n9gxFJa35m>t$K3CE26Y-N=nkIH)Ov#I zf36i@W^I;s_rCl2AVz+L?0xrNCMTEfWB@r-B{w~YgX{j@xDwh2A&ziP=xxxA*aXO~e(S`m7gLa}gjDeK1L8{WRo zR_%OCUNn#@fABWkgIc}qzbRMyplU=ieaj8Y6I}kVg1e@JmExeZ%JL2kp6MBMq+ij< zesTik=qRuC82Nsm{0uW5+VK`034C@v{o@a7ldax&hPS=_@q#m?iQWB-7_P@$E8mXP zdh-sffyVE&=6V!7X+oH$$h6p34Qm_VKG55B2-JXQ+gc<3xQA})f3UXpB@(5}e<*MF zBS+_fS91d=!}nACx+7$o*|!>e7EiN!EnI0IElCm@*#DgLKwq2t-1m%jNoq*bI`aa& zeuC1=lNWKR=f!-ffq*j zLQvN$XbxQ;iISCe{8V|Z*3oQ(M})qD;OoxS2A?y5;sljFJ(W0ZQ`$H-O)V-s^m&zd z7>8~!MSR)0Nv9Rr&*Ev@+&!U#*!mH!ykW|3hv!l4rqP;b6{Z{|YxmeFt;g^Nc69a`@9MA?5{k!`qV9a}+2YUb(%X!y z*aCy0_(Koi9nc^LN5R&Sg8stz#p%a){InLg+6YB2BeZlcL|56IGxIyQ%)~;ysbEe6bKd-lS5{$`O7{4_EX0DP#9+Y>F-WNTfYeRW{@?$*kLg|JyW9bBh^zI(dN z!RGBB-Ew2H9}6q;64JZZPO*oE%WS?b-e3qDmiDRx9V*)p>0^RNkfUIyke2#db>(CZ z>FsM#e8UTepzWz_@ZOp8(DUQj#A{t3C#?qzuvNt;I*~CrIA|KNx3!=Qa@p{f#%hzT z`*J3}SgZlm|8^YD4OKem&lE@hDSCP(kh%5>X0<{4XGY`T?9g{O=xue?{yivXey2F9 zXC&SfREjk$$Hr^)c~L{i1dzc9&XW!GHOB5a8Han%2JnCM4YNvkYqByw&nRsNrFjo` z6!I!?fUz0aH-3D50uCUAThidoZ^+9{sNM{nSp8P^pce#tS*=fhylmS1QLVUC56B3A z=R0zTs@;UPmPeE8c4nE|r%gQAAA;FZFMxod!aWvwLG{&$QF$nagn3)rpa@5CGZz>d z{?Q@hc!)|53eMWfwSSPkSrnQ2(#A5NEBAs5~{atzK= zKydCIxlm0saFv{>XBhmsG^`AcChOj0r%&BCGGg@p93cT=EsNBH!=|+U@c*3qFhBup zCKL1s+eIe2yVc+7mYp93=DtmAAk}O|0oE&Ja_t>Ra})qWUK8GG7YdF$fw07GFoSY> z8TTC{xQg5t8dj`;K2-tM$BagT8`fskiB0RFkZbY zdMe};2O{RXDdEV2D++(UVrMyh6LC@1Y6)vyU$V!2Zh{LV1rL962KUl>bkU-^he@); znOf5pvK_YNL6~tFdINBvK+r5!Lhc)CAVttp&)^ZXlr2seNf3kxbg*MF%dwzpmg&b> zZS^Acjs*)>CGFJbWFHSd!SrEcBIt0aN(oj1IOaw`eJQX|sFnNFM#`<9P;6tcYxcG{ zw3_6dt(N)M>PDg;Z^rXdNLVhU6br21bQ<$^VLU zconef?L}zG7*Un;sRC)lj+Y@bl2SRvO+B(LZ zw+?uw_9uLnHFtW%4X0Zz-qgT}mjI{H`v#=0L*a6mz`xMmBE3E&t3KkI^@0$Z*a7UJ35VE8U z5iwuBN&qn*vSzBnAGS})pWTMMJV&kzC}wX17kLNgRAxDxT&l0HAG2cBoq^CQ&`*ku zi<>Dh=RE`l>vkG~vByl0=UgCI_#7z&=!fBo-Z!Y>0Uho_(%cleEpqY;=)>=V8*nD7 z%XN`(TLd4vX{XPlq=|b5=DJjK4bakw&c@KyX~xLY2q{g|ASh{Sg3%rP;!H7#iM-iT z;&~1zVSFg+mc6C0m?3`yx8y7x`B6>fImiJ&r|F`|Y?}UQY-2DDMAcnH4u7~+6MRxc zV^)07KPqf*PY=}&mA^|RWDvu{t{~7MbL{R|#Cve7-P|K_H%to|*?CsAAw4{=tbssx zVLjN=y4no{6OrUXgZ{vRLd%`HehT&?BaJj&lc6*t7SH#kCXGQKWqj4*bpA*li9cG3L zo_C}`%Mw6N*Tz%KvFAt(-!(YRd2b@LAh1Z0|1e52s$OTVK*AJIHNKDxf8&FxjMsTzP5*-q>d7tUo+7{>otV7Tq zHIe@cfes{QCpLN$^ZdE0-ne(_^Ces$-rE6OWqaI|VDX zD&sB#2J4@;fI1&X{@J}Vsp13wL>2cWp)C-ub5oi`8D8!5(lvm`>;_V?ku!L1&w~}e zFlP?c(6j^qH%a+4p|YvS1R>UGv@zRWmG|TKR8ab7r@1cqwGow#Rz!pI6(RrW4hE0L zGe!Yz@;~*(>}mqi8LqE8&5F6{SWHIXnR!lG4FGDp{kdb8Dz|V~# zGY|%`5z@0GUGpv7?p+7#B#73S&OsbK*`9eY;Bl%td(RPv?R=`;sH~{?u_Xv31(e%} zx;PST*oR7xTY!v&z(DWgv0eHv2kK4pV!X?d3*aohDYkFgXDXwuR}m& zMcg(gR*!On4kD(k6HV`$-dR^z#z};(ZXJ!V8RExq+G08)y(5mmN$2gr?s3zNxGSIw z=jLL_(o~H%U<$0EB~fr4@0aqapeNpMI1;94%uy<=QiInb1+ z#LyiSLsNOGh~nr_{Ve=|=n;MjL1@i8O9i=9w)B^0I6i>CAYqz&Kz+q^|ET5-D>pPY zZ({W8_WM~Be!skYs#aPmODG00yvjMKZq|rFNM)KXhcd~oO)oJ^kAU6Qqb6H;x3x%j zjrH^qDP!No&ERsnv4eW4{-GhBz9l{XPiEK8?R8w44h`E8upVg+ugwQUi=N!#aiLG- zj~}>O=2$r@>-aTcidbF!U5AY&;oDMG4z~_-$yn$0I~d)F=VBm{bMJM9%bzySXY7SJ zeKV6SOYf>E#mI+fpi0 z#;v}OUYGa>fkEmw)0Hb3T$9|4{PK-Zv?iJ>IHiV^vV5JhA+_EKll}_RddMj48i0v9 z6i~%SWO(mKV)|rK9~pqOvbqbFR@!Gc~ z)LH4gtG1}1qJEkwo`UVHU!FiY{qi30h1tKx;iJByE7-Ia;BH*&J!V6=R)a2b`}mF|g&h=a9M3rmsH3Bvoa%~V;LNBc!GA_y^qpHG|J#KxYZl>=HuCHBU_yB*<}Gx)n+CsI>0skN21aoV(0dmWLoJmy}gpvU+4shB<1HA3kh0ypQg zaWl+hj=xf1WQX`l)JtrKu6hyfe44=nH`)%1gJ3y{W%Lf4Begze)Z6U+7Hz_n84YxFO+*;)H>F8(R)mrW-D-WAQ5k5gW4&zsgM{ z?n2;mpbAuubFPE5zqSwPvCt}*_xlCxp_Jerx`bX_a`JV+D*g=WPTO&(7%9Q`}N}D;*ysamiTZWRmE)X$4x{- z-{M%U6sx3jD4YlflPzlUvq`bA=Kw}sp3C@1!lt6A(ZapE^|mSRjZESRz{eYemqrpV z3fa%WOuy&B)_~RWNR=}Xs-C{pH6lc(q_B`tQVMG6k=5_K2w}@?Yr7`tx_BDsCb-i2 zLtqMm8T(QI(-T02@x>zWHjM-qgtEee+@8RD|3w_2OL)3s*}WEvdn364J`)=oYYAX~ zIFPQrvomX9edJCo z1iKL?QN_Loo>iUbg;|b<1&YbZNxsXMH&cEBrN?*2%yT+MIS16~uz#hBioFR?2jA=V zmS1`;R}mwyDY5SOzn+>}aB3Pr>J#j;0`QO4&=*Q((I-5=JVU`I3e3j|bXT*7Z#u)r zBxbj_BUS6>VA4=}I`}R7>zzbev5>mGUs~aK@jYc7;SFCzowe40tX$qn01zH#X+#+y4?er>9KmPWn6oCadTq&rR_aXaz zoWuK_+2k&duK^%ul;#V+oLuYr(J|zEoQN{^XnIQL;BVdf- zR`ZHX8!=wSbd8CjfjQ26B>y9SP7K*e&v!K^jDc!V`De<5L|^=pRdjhG(!> zt$>%DWv8dg-^dhCn_3wxzIRC10AkG4s-Hv-kU9eoOYozBa0s>%RS}_;5$-v)mHB57 zXn6&|I?dD^ozm8qJ9S=@?}}d|6rGTuDDAl!9ZpJ1OKYY>0=?#Gp@cW89N0oQpTRpY z1rC`@D`Oa|oSI3VTebEb0~AGi#74RYCz}yPgZ%u+$BjF4aGU~crxJdxi_XPWY5G9#t7Z3yedzB>5< zl!_+@c$G-@cMYX{M=Ng~WtkHHx-y-&FMu*iFHw>6t3azomW8fOsZi}?Q|Iw{G0q0q z!rbm37D?(N9YDcuP=SA(q!!_>7-*M}b3pEg2=LEu>OA^6tlZ!;pa!{i=l^E&QG+l;d^;-Ob;G%g)4R5`SFxgP&GYdGATtKx5JL^Cd% zQ}BEv`wRhkWA0sR47@?->%cQmm^vy9#h*X#`_orPM!5Q0BxIb3`~iEFK_Ctp%PA?% z3q^6az1cOtU0pql0|_U%8}O2saw>8$D-uy>TW9JgyeDgK+T!8Lw<&4y-DLv6dZFEIIexOvdqNDcXZ)J?ogL+~T$ZUyL{+P+a z-Q{?A&D*8vO-qbeOf+(R^dmYHm-8-MD%nZ!Y27Z^3{(TI(7DRPQFc|qfh6LG zr-yPnR`IiVqOA6P8oc_kn7didyNb&%klED+vd$rJ(mbLGK;HyRU*9Xec z)h;44XYATKROsK~b&jC%1ax_`$YwE}H%qqIh)AHHN0AwX@D;v5^N+9!vxk*e|4CTI z*(LFn^B4a^SVerJ*z-+xtWn6d?s?keN}R#?SI?6Be@H*{g`)%1S;W7`!Q@(3=(R2AD>r#Kq)O|I=`BS_S|ZD=~0{@=3g^f&3CW=vb_GKoG|BY zeP`32)2A?@P{vgnGjQpti|%3@GJNw{Y`3HIAI^;VP!V6T^IzD%aCjmwFLD5nMMak* z*ZKQy!q+*0-H*e&V3j-7diF+WG27oh*u;z;L4 zK}mwU;M$2-IDpRq-Q7oI9tR1Hk-egvANIdIb=yI^{!@-hZ&MjHvZhO~x1^}vVUmEA zNi29IDarIkM*l_E#tr^jD-fI|<~evA3q}Eaiaz5s(haF5VrApEUp#QD`XS598v=3# z6s$~(2SFEE6$}oNFBVt;$q1m#hy)>z3PVFfbeY1a_$*e@?j4^5U|`6EOEDPO-j}Ea zo9gT`iGMNaLd|H~4aBd(nVU}iP{W>}ZfPi(#8-%fo^hOgs4Uk2g0@$$tiUrPb(Viv z1=&_4w??twtQc`52R4ZIUenIOmAAPCnSho^rGZ8m8RHM9Np=pAykAdk6Adm|z5cUB z|J8|kr}X(VMpQYs?cAnUHC)KVUc6#0tS5xniYr0<0N+idU}Ake=$Jk17Vt?J8AGk1 zU;h?#aoq@Y(Tk1&!YwJ&pS`s#q}P1!QN&)Z;NAV;>;$eq2PKGRbX}G2-PNiryX|=w z)2T57;?gV?KpW&c=qJ4d#YIm5A+L7L-k!NK)aGZ1Qt$34em5(-_=e`s-DWHNy#fXc zUjc45X2G;gx7kTQCjw(o03Krl03Qhp>7Vb?-* znBebn{JaDl@Nh-C3!2V3fOz-jQ573==cZsoJ_98m$M_xhGnoL4-vmCHTOi9lN9UdS zCeR9I5-|%z1(lOza6Se=?!QFI9`emK1O^7)q!k>L32EZYCKs&3nW}yPG zzp)BCcE!*)r)5OP+zDO+(@TkfMJ@&@E@%M)7B^u|=3sXVCQ>%RT(VOVgdDPoseT%* zpWXml;31=kPp4wqA=6*Z|6hVCW}YCRp|y3qdVnLet39az?dp$ePo$nnx~O$B(Vc>V zsn`Xjkjv46RnsTG0a{%@+I43pu~%v()Fs4pO2qJxF(eR#A9qAX$+v=2a|4_Tap|>Y zT1BGc>2zsd3xO>Nq^#VGn<_cNO;LFQqr-QQ36cS#TiSM)Yc@8o*pAeJB3q+8ib2x+ z@z>RTL&N5_ne{ud+xAjbDInKg_vt$To?G{3MVvT^Oz&dWbFhD_^DgW11bPDmK->az zTmc$jco~fT^p2X$f>du&4PSZqO;Zqe9i(f#FlmeCgtZh#Yce6cX;lL-Qnb5wQl(L@ z@jJMy6uth|+b4l^CS{kq=NX+;_??44eV%|;0WjYS)R8wpi6{vorecd{)k&A}S(hsK z0MG+3L+4hDMsFe;TNM=*$7^FLiF1@;%7niWQ!*}hZNY%j3tDtk9Fv_LHX&7~W2F3+ zM=IlHx9P@gtCvI>uL0soPB8I$d7v^Wtd;CnJYSkZH(IpKmb)(LGCITA{rKc7da>K9 zmMy@kvEDK9B^JbK^}s5E@)h7}FsXX8bdI*YnIxrmqgRQ;|_pDwL$NKR=0dwV@hQEx{5s9rgJq5R|-tePo+!rq+Wh zO58pfgyE|I9nZ-Z!cyW2s+ZdfqZU@ayd?I)O@#D;gEz%TIXpb4Pesf+R&FD4U{znk zmI>A&3kv9Y)5MdcYHCD7uwO_HOf`e}x3fujd_OLs*whYziEAdwTmxYYvlMK*usaQ; znQ$Iex~`1fa9QY2u=oj#6R{Srk-v0V{6P8{jvSMlIs zV`6%Kr0sp@^Tv;THzZf1p2HIVT|=v}rp8Px6MjKlHl6zwK-@SHWUO8z-Wzf5y>SV( zHsl2oD$MmdwLrG)lN3B`%#(oOp#r===UY6(1X6HAY#AmD@OH_SH2yw~u?9C(b2oCX zz3U2|I_^X@$XH~{5)H`88>71vFqWCJi(;{3GWHv7v;Li%4cEMB2A~T<9dT8ChG`nFE%rwEDLx;LV%t#p)9_ zZ0sRfKFe>{L`Q4yZ=Cgpk18^1t^*8gywEXY;$T>c+2~g!gz8>JDs#d%zTpqdh41IC z(^h>B5|iPceRt0{s%kP#Y6_m8Ktw9I09=I5AhD+h1g-L}Shwk^jEMk@4GzbdR`p`@ zoio{|;Z|z(oQIm#y?nL9p;qr@3lYUy!e^omGBBK^7<+FOTRXk_X-mB&5eIc_)bIOxK#(ooXHXio7J)d!U3w) zQizypBQJgX;=pCFycL8;C4%hWdF{u{p=(4oy)>rC z_%1t+Q&5X8%HKD;J@ku(q3DDh(Dr|i(b-qzxWefhW_evmS+kUXve<;O*6~sOWr`(r z4p0hkO8F&LCd&VYKWIK6Y)NBLQP-kAE(ail7mN?*(I2H&klVO(DxQ$oxh!KdBafEy z1GR@rRK$UZ=ORHA`+;6O5guv>$J(d?7Ph(Kf0D^j8=AeGicv6I?jFTNekranMx$n5#luBzQkX}gJU@` zk%Mpj=7%~dW8!#^rpWpJ#y+Sc1u&;uZjjh|NCdfkSMz*@xfxNmcC9o0?dT)|^{>GX z%YTO-+yhL1haV&)_IJctx0q#g%vQVK)Y+cJLl*{V$iPRCOwe<3SN}fsXKHPdHs#jG zbC_`IZo^0ZBJA8Yw`sc;tlueM(gh@aK^mX4eP2%1sJLUz_07IF!+B`ncDTyua$J;Y zaG0UIy&TLXg4a_9+Bv8h&nXjJ)it{Q-2E+^=mNoswMWgg;{~)9`?+Bu2WA*{+IP|! zS6hk`LL$6}-#^95KzDS14YMpK`wRNO`B(HI;=zNx_J=c*7eD-0>_hRt*@u5UmP0VD zXyYZnfKLRy> + +\* 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", "commitAckSent", "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", "CommitAck", "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 or in some other round. +CountCommitted(r) == Cardinality({rm \in RM : Cardinality({msg \in msgs : msg.rm = rm /\ msg.type = "Commit"}) /= 0}) + +\* MoreThanFNodesCommitted returns whether more than F nodes have been committed +\* in the current round (as the node r sees it). +\* +\* IMPORTANT NOTE: we intentionally do not add the "lost" nodes calculation to the specification, and here's +\* the reason: from the node's point of view we can't reliably check that some neighbour is completely +\* out of the network. It is possible that the node doesn't receive consensus messages from some other member +\* due to network delays. On the other hand, real nodes can go down at any time. The absence of the +\* member's message doesn't mean that the member is out of the network, we never can be sure about +\* that, thus, this information is unreliable and can't be trusted during the consensus process. +\* What can be trusted is whether there's a Commit message from some member was received by the node. +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. See the comment above the MoreThanFNodesCommitted. + \/ /\ 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 <<>> + +\* RMSendCommitAck describes node r collecting enough Commit messages and sending +\* the CommitAck message. +RMSendCommitAck(r) == + /\ rmState[r].type /= "bad" + /\ rmState[r].type /= "dead" + /\ rmState[r].type /= "commitAckSent" + /\ rmState[r].type /= "blockAccepted" + /\ PrepareRequestSentOrReceived(r) + /\ Cardinality({msg \in msgs : msg.type = "Commit" /\ msg.view = rmState[r].view}) >= M + /\ rmState' = [rmState EXCEPT ![r].type = "commitAckSent"] + /\ msgs' = msgs \cup {[type |-> "CommitAck", rm |-> r, view |-> rmState[r].view]} + /\ UNCHANGED <<>> + +\* RMAcceptBlock describes node r collecting enough CommitAck messages and accepting +\* the block. +RMAcceptBlock(r) == + /\ rmState[r].type = "commitAckSent" + /\ Cardinality({msg \in msgs : msg.type = "CommitAck" /\ 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" /\ \neg IsPrimary(r)) + \/ 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" + /\ rmState[r].type /= "commitAckSent" + /\ 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 <> + +\* RMFaultySendCommitAck describes sending CommitAck message by the faulty node r. +RMFaultySendCommitAck(r) == + /\ rmState[r].type = "bad" + /\ LET ack == [type |-> "CommitAck", rm |-> r, view |-> rmState[r].view] + IN /\ ack \notin msgs + /\ msgs' = msgs \cup {ack} + /\ 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 <> + +\* TerminatingFourNodesDeadlock describes node r that is in the state where dBFT +\* stucks in a four nodes scenario with one dead node allowed. Allow infinite +\* stuttering to prevent TLC deadlock recognition. +\* Note that this step is unused in the current specification, however, it may be +\* used for further investigations of this deadlock. +TerminatingFourNodesDeadlockSameView(r) == + /\ Cardinality({rm \in RM : rmState[rm].type = "dead" /\ rmState[rm].view = rmState[r].view}) = 1 + /\ Cardinality({rm \in RM : rmState[rm].type = "cv" /\ rmState[rm].view = rmState[r].view}) = 2 + /\ Cardinality({rm \in RM : rmState[rm].type = "commitSent" /\ rmState[rm].view = rmState[r].view}) = 1 + /\ UNCHANGED <> + +\* TerminatingFourNodesDeadlock describes node r that is in the state where dBFT +\* stucks in a four nodes scenario and the same view. Allow infinite stuttering +\* to prevent TLC deadlock recognition. +\* Note that this step is unused in the current specification, however, it may be +\* used for further investigations of this deadlock. +TerminatingFourNodesDeadlock == + /\ Cardinality({rm \in RM : rmState[rm].type = "dead"}) = 1 + /\ Cardinality({rm \in RM : rmState[rm].type = "cv"}) = 2 + /\ Cardinality({rm \in RM : rmState[rm].type = "commitSent"}) = 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: + RMSendPrepareRequest(r) \/ RMSendPrepareResponse(r) \/ RMSendCommit(r) \/ RMSendCommitAck(r) + \/ RMAcceptBlock(r) \/ RMSendChangeView(r) \/ RMReceiveChangeView(r) + \/ RMDie(r) \/ RMBeBad(r) + \/ RMFaultySendCV(r) \/ RMFaultyDoCV(r) \/ RMFaultySendCommit(r) \/ RMFaultySendCommitAck(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 Wed Jun 19 17:51:15 MSK 2024 by anna +\* Last modified Mon Mar 06 15:36:57 MSK 2023 by root +\* 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_antiMEV/dbft___AllGoodModel.launch b/formal-models/dbft_antiMEV/dbft___AllGoodModel.launch new file mode 100644 index 00000000..52b9984e --- /dev/null +++ b/formal-models/dbft_antiMEV/dbft___AllGoodModel.launch @@ -0,0 +1,42 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +