From 0095b948df53837f653a241545ffa31c09a7de7b 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 --- formal-models/.github/dbft3.0.drawio | 111 +++++ formal-models/.github/dbft3.0.png | Bin 0 -> 69526 bytes formal-models/README.md | 60 +++ formal-models/dbft3.0/dbft.tla | 430 ++++++++++++++++++ .../dbft3.0/dbft___AllGoodModel.launch | 42 ++ 5 files changed, 643 insertions(+) create mode 100644 formal-models/.github/dbft3.0.drawio create mode 100644 formal-models/.github/dbft3.0.png create mode 100644 formal-models/dbft3.0/dbft.tla create mode 100644 formal-models/dbft3.0/dbft___AllGoodModel.launch diff --git a/formal-models/.github/dbft3.0.drawio b/formal-models/.github/dbft3.0.drawio new file mode 100644 index 00000000..8382b326 --- /dev/null +++ b/formal-models/.github/dbft3.0.drawio @@ -0,0 +1,111 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/formal-models/.github/dbft3.0.png b/formal-models/.github/dbft3.0.png new file mode 100644 index 0000000000000000000000000000000000000000..c54ba856ad50554ebc7f88006077183e72f126c4 GIT binary patch literal 69526 zcmeEu2RzmL|NrM42glwd>zLVlrgH3z$|_`UvNt7;QD!Ja2o+kAC{e}{GBZk<emNb!);+IjCkpch6%8Sb@NFLql zZ|CCVMHuja_i;B54?BKoEje*XFqEJf{v9>&>9BpES3uy_XMH!Xz!1#~OZ*Lb5r>$0h2Rrcb z8+pLAczW1-`#C!KZ8d>SN%PBS@=L0M2lyWubpipw7cVif~Q$Mg)*_OtVGJ>c!=mZ33PLG^8aps0p8vo0d79uH#&HGc{w={j+HQ?ou8j~ z@b}%Ey*&uqBlPhBJO6HUe1q{1G{v`?x;X~8ZuM1^BPqdb@ag*?DOG+^Xj19q8rwP1y00dMwb>hrl$7;Ooz?=zDwn09t?R;}j4OO6X)4 z7~l>1xdwQ85T5!6_<6hkbhd!K)ttS(0<`Qr-8}F-tM2XT<^YInZ0F?K-d3}ADA15!z?H&#ucK-fu z4koT{K=|yaoH!jB-i@p(4yEB~SRiJ>?dO|BfkT)WPC_7T%`K z|4ej3?{E6!_j>-IW`6VNr3ke9PPXMe0Jo?)x&;B+{Ve11zJYk{_D#&h{J$xDym69} z^#SJsxNrM8_~e4`2Y!DW2QQZY&_Mn`XutplMozxqm!J<|dpo~SV7|A;2L#-j;`?bq z^S2#*-})c3DWG)z((C{EQ2c%Hr($pC;2!An)1lboxAz?z{J~?w%j?fPCym!h`gZmJ zoqVVK?L6FE@JP!6s7$;9R0H5EzztY`Rl);LH%CXjZBp}d0<3Ch|IJR}wWJSTmweMm za%%i?8lVNwJOrKmlU4X#GxA$z<3|Pj+agCWrv&6fSQ~hmpi}T$aU!U?zgH0xUY8V? zQXmNUwyxY-5Er~l zAnxqp9qix=fRH$lFi$rxy8t{+QVVu<3ve>_*;;Tg=t+>EpCksDGCvnLyWbG3t?7Ru zIhv~SYVvp>_M_wwEc`!F7682ajvJ*2UxR=44y0rVZLYuY47NRnZLa+#jQJzb;-7D` zx8>+pYVyy8-`}vR8BoFh4CwkJW8$UhCzkqA8ot-svIJ)P1#A8JSpIMF@D?21g08=5 z5D4)5cVW81))aptO#e6W_iy-{3IHc>BfxEShvynEm+$bxw*JJkkC-#T7sR7fFYf?v z8$TzPKo2{-76UB~TaF+8p`VMrAl^>m=lJ=z&{n^1L;V8oO8OAMEddVygmW~d`4tuU zRq+FEuMpU(?L}^ZA%J1O!6p80`{BpGqQtKXrj|Ug{f@tnofr82vvB`A_w=)2*;>{% zr2Ca&`IAxFw!HtYg7__k@S~jmrciDx**^iLiAjn}6Ih;rl(s{9e-2Fhes0Ar0&SbS zzamH@DAZqoG#@`Fd|<>FA0+!0YyDZgq<=I%{~w_uIlQvMOY^TI8-GDqMDTQeakO~7 z^j}!?TUzi>3vvFaZVAx-cVQ6$?))w+A}Fl?`>^OowYCK#06g||1A0yJH&Mm^2d0`J z_sX#@>H@*0aBj0NH2LRgNkthCNMUwEr$e$xy+h5GT z4|Dx*lCt0Ddw-n`{#6$IM^EHCnD%|1`P-vkWSYTD+X-nx${Mu%B4Pda12LtoSAQ3X z5n|(iA`ttZbD((FX8Y$ilDg8rN{uKIV8pg*{p;p*34r7~!TTrWVgbz50tHilBlG(2 z#hTkC9skO((6&_%~(w zcSC`H6oLL{%RGSRcK9mEZSzVfMFQsPkK@=aK>G*Ktn_xd!ym1z`3Wk655Fpsv_P;=?4naR4%pcw0|Bq_5q_?xb z+q!=H7TSMwt(LuUke9xrf~SI(n}(W?mx+nAzTMV0$uQu*y`B-@kz72>GB zDW<;>J@|%2R2|#_*7!|a@|O<@{9*X;y=43*{rujYfN56J~lJc7)K25ZCY0@UH- zHfFnL%iC032FSSi9=5&V50$9?c=AJs*W#^%K6}OJ_VgZX2I#GKByOoNHi=Te%Ryo8XZkhTyicXoV)MWituvQ{Uxmin+uKk0+eED26RptA5axV4{!XjU|M`u>pPuSToNcyW z5Rwq%w65~u-uq?1!Q`63C4HCR&+iU@9o^i}CL*CsH6!Jbf*}#@mLz~;Q|BPd`tXa# zm*x(HeteUWZ(iY?A$HGqTx+MSEA8`J7MaJt%nD_wq`O=_cyVgbCBL>vPQvN|--io( zPgD*c`Jw&|4(9t{g#DP;i4dN87Z7+jI#p*xudk$Bgu@0SNI$GgOrKzd8axO!lTWuve z=J3rUV$W6@(&Sva*pCg}72@aPbKK44&FKioQ5_AF09$ZmhFQ^LmR_AW)WydlVXc4m z?AiN$@1tqcuC?11>x=v?R$ToiY zO^&zgMC(}-Kw^ug$VZ)Lc}Xv-M7(l`rw(cbhbNO^j_f~{M#BJk`b=2vfN7ylA_BA_ z$?;<^N>~Bm^|}NuGNgZ97;m{AF#UA#YKDmE(?XpzWZ_t{@?6;{bDT+Xd6rkZh6lO^ z*keQ z7FwvE)v3B_Yd-WK@MgLg504tXVfv{J;nJssu2g;CYr)+AtN6QID7&bWXC{zHw zeUh`wffOS(l==Vf5Om9+OED=4ouet@RQt6-1q{fN!*>B~@fk#5F0U8cY&dZjoAgO-x+!#x)r zPUq1=Evr%=iO39Ma82CX6uGzH4W5HSHfKn=jR!TrI3YPN-92&LbchbHS5* zoy!ai4DTzB7lp~FL#ZiOh!K&#WjwaU`K<8Nyj+7XKqSsDa0o|Uvn4t6HZ^?xv#HWB z>FF{?tT1k>bRh;RIM}`CBjp(mhJC4EyNhMQ2D#=aA|rNo@Id%_riUWgHc=h0)XBGh=B zCw+GWIFn(>XFvAAG3Sjp0y}p|`OiEpN@TaR`*KhsR1fOPRpLGH5(O>Ckg>GW+@v4j z*M#zpzY}ufJRQo~fXU*obnR8^%DX23k(0K@u*!CRY2W#p0=7K&@WWI^_rA3AB!VrC zu{6dPcL&av?(`Oe<|Z^oBh{Xy?MeyIxrUguC^3^_)w@K`IDLOKT;#ws(lJ0Eka>hg zEwU~OGS-~i9X#jJ-F_B=^s-h}C)f`xq391}%bxWjFT9!`o_+Mb*8wUv`Sg{>Tg0zp z_sw@m)YFQZE+6EDD;otB|8342z>l+qjal@0~OWR3T<5S$iV}goaKWeR zS#@D7_B3UEv@$Bo>3ieJgZZFThMP<{IQrEwl527>pWK&?TvW|TS+K%Rddz_wdAiOQ zD0-Cnejhiq4(~yDn*|(q@SrAi^xm<+M4i#YC&HJUSVl(eS7>deK%cDv_Lzw!=oXaH!H#kC>d%XHZjS431qyIAuhi zDm`1(mp#D$+B-|1+Ue82`47Ot(^?}PH6UgR#e%i8=2L@BA&17=L}BQS`6Bz`YS-S& z!$)9fb2U}$?1wB|%KG}!Xb}y&-aA~y6a0>85lEg(VH*Zv$xXah))pS}!myjj-O
m6n#~#BtGq4Yg!ybCUn1h;RdOs)WrxWf+!|=;g!U%nskuHx@wo?c+1`?7c9$p zh*p6A{=Dd)dypmKxJmrNXS8p@2q^sPW{_v{r6$>2m z#FrM8DPk(l+IhM_M(`xULY0mi*%A6B2I)gt7D8h9BCkZfI}XA=^;ub*47f?9`Bt~> zdTcHk)Hz^4Jt7Md@|KE|%h zYh_ilv;lh9+wy4BGBMK7?}s@Do3&3Kb5U4JhH-T?vAdj^j?bloVd(X|3$$L%uL=`S zSu)3wr|%_+5S5u3x;Nwb8hr$@j|WSu%aVZ9TeM9+y%>D|?AfCvaTnh2T^iwa!X`23 zt(CFU-=ruT=Sk;G-vxhX%VXLB`E~;t7R|iTaQlpFxS&XhA6hcUKk8AlHHCYBY0=us z$Br{+aP+FOdw3Qyy4l%2pim45$`_DJ{T};0(&vn;z3Y}=Q^ZFb-9T1q)DXv=Hd@ZQ z=g=nD+R+eA>cka!f#Y*@JqLmkcByP9cK3vM!*N(=&s$8iE{gUV&Fj7BAq?wR0iLxx zVf3ou$UPb=hBvwUDo}z83kyMeR1FH&Wc;{X9bpFcpL9+{&@uQl1~1v!$)g`cLIr+|eR;J)6hnzwe@aOCr1$4iM2VuTJ; zart~)O#3eJ%$YTHa^g}-UfLm~Z9azK^`qoSh2SIP?|1vZ$74St&>6BA@@IX|fQ4k> zNf;?wT=3A2_f1C9a2RkZ(Aa`EQ9B|Fc(4f6wR!)sB+Le_Exe#!-Y$LzECPi^V7adO z1^S)xW^8?tS|}C0Y_{WCc;Zgjg*8TV~@PqEe+SuhpJeBOM?{yZ8+)%WDF@> zA9{49K-bVk5ID+Y>sqA3N}LIeMY?r6M|BO**2eEhJ(k2(pxpBt>YFgs185jhftoq1h< zwfVWBCEL^R23D?$=FfMk9!px|^=ut}nWL3&vt#$cgA;`}W{R_mnwON-x!|STzy?(T zIzUTQTBy5pSZ=f;WvkRhy3M9jLHDYIz}u;GV42ctaS<+vq%+V6bmig=N!7K{mVxK? z)2uKptSKT3T24TzbR(zOV3Q>Kne2}~)o}V)UpJgos+zX7g0)Ap z5wXoKXA5*2PvMV498c{;XIt(auzDWc6p8J}dYemcI$2@kc-kv^HlLG*U(m$*%0W4s zGKoAYEy$Q1U_ELjs@1!bFl-1M33j#A5=P00#}G>3$)g$~pU>;D*s)Tpah_Xk8J*1j znm3=EN6TB3v^gd)?fRIY7nUt}g#9U-i1j10I|pnEH~F};YkU(sH=YYKt(#Ns&`P+b zcW#+ir%z0$@33VtU(SKBY<(T)wCO^*=MVUs+3!`)f0~XDXF4t8g4hum02l+y5kuDl zMH=tj%~)2HC49E+h>l>Lt{T}9dI?i9s&eWwKfYeCr(#8uoU;eZ+P^2{8eKkpxTeVTe#Aj zo_+j8k!R%@cn4GefxDM+ca`RXq+}KMi|)gF*;&xk6%I4F8*|V>K)DGnHvT|H%~X8@;uTuym8q*N5Q(j(maIN=p64XdcZ^F?4Yci-B7NR z9R;;%E?v(KASgSD+6PZD!>>LF@NkqF{F-odZ%lT)d4z70RZ+4=e+Xa1`S!!*2@+~I zA05Ab=80B+rAP6ESdP(cuR%xpIk?7TKRWR;>R+{B%$un{9nIbtBEWuD=O?^qK&-gUQ#*XSVhuBk%L~1 znf6zaHjpzj(Lzn(HNtU*GUzxOjaWIuJhODiWuNAG!D@xKn?o<%x-MGKT)so;MO&7) zSDi)0>R`XT*Zzl%vb*iR&cY~n09gw;4K!A_&+CV3jFC-q@5!$oeUkNA0nKz}rtf81 zZQC<`^}7$a&Bg4<3iL!wuRXX`nRV;^cyU)FKqh##%mKL0X9;P6I2hn%+TbY98z-8t zw0mZ7_STSqi;xYs%>djUm$2)@z(E!kv6{T>0C}}p(U3>ykKM}jep7Rcq?A6f3%Sez zI3PSWi=u}YuB{x<>K44W>-3$H`Jy))Yro|%7BrFRk^j=+^xD{bn z{pL%$qs5ab|2Mf`=6&nV&>@w`tZA+>z0vigJ63 z&>gI>Flntkf*^T8aWUKXzz&!vkoy9$yxbfZt>WOl#xQPY_d8q>_H&VqemVY=Mme23 z(8rmjco8LU&ms9xpZkPH9-!>L=E}3~ZLF7pkKt9jkH=@p(h7r(D;l3kvqaxa4D^4s zPOiFArI?**e2v>@9S74rexl}pD61@4(3113X@8Q_M>(qZC1GxZ)0<~f4SywxWS@C; zJ-hjs6-}i7y_pdC8}?4tZ(Xupe6%)bg6HPQsPD@Lp`>sT#ru$UBEkcb2(CpH1 zrKQX+MAOmD!}hl#8cUWA59eG799Cv6=+VZ#UUUkWRKDZxqtP@J(pn#c zbZZTi=q)D>Bv+O zo4P&gKy|53^WLugvQx~uChK6{9v$VN*@CAOE)1BiVT3LMC$-S?sTE$8h!o;?LH5Rpk? z7B#bt_yS^DML?@Qlj$D0@i0tiruuE(72t7?szF*QoCiMCE^)4dpbjG|<|7S=`rtjg zPs*?|0e-{R1>yAFGeRc%vs6AkGpEN$cSO=^07!w97dD+f0$AH^GiqSRo9MX9!R(zc z??)I$ysmJ2CU9)HQtaf~LQBBgi?3o?@4ELVFTQ!A=kPe`PT~qaWVx}n;*^)%mRW8| zhXLWBr(n}=PqO74@0hKTrFAMBARwoUIdT`zZN3strmL*Y@_sy`8Gf6c1&iDP0V0#Q z@-g=+APxq)sXTL*4s8F@lol^V#n!xX-U62&qz#3gZDNAW^VfIoVcQS4RgpjmzpIV8 zf3-H3HFSkl3)Kh6NPA4I{c|-{r18t$UbHgx!guzrCZuiD4irced!=<^GPRtc9-Nk!PeCf$m@-Nh>2e`PeJ|g187banog3XQ96cEDEjHTfc zSe~)d#ME=jEba+iY&|g=zUuh^gyB4$#_j`mAYR~L?tW70{VB1?@RWjmC%=xo+2RW_%ip{Dm%3WpABO}z}v2iSFRghHM;Nh(vfw3>(+fpuP3;fK z`I6P?S3TR8q~Mp5fOr~sS(WB!;57QFNj0=3vR#&Q9NWfih#*Ej#$q0brD@|+EH%ev zurEUpRh%x$w7v{H=U!5-F!cE2Ggm;!H-j^5UiE~Ys*c)16m)H(3y!m7p8L>yCHB)O zulLxOf{V(*^m#Vrj%3fT8@J?L6`{bg*o1Lsl=H$MJ62iO)G%=+r3-WQo8fBJ7L^{C zJO;~qfxmFwzB!?<#9YSQg^xDJspEVvh&GFjv!Fxk5b@5=X zTCu44nsB^GQAyp2FM}>c^coMs*B|haN0ZVN!-%{%?LLUW6vNl5?xHlbwTEX0%boO; zW{xqfS8yT!E}g zeuaE!5Gzfca9mqn2&%S~!xW)tnW3Dr;@r8<zb;^J9x9i zA=|NbVa$h1d+yBA_`-!(bRo`@pA418t?wPnu>6qHSA2lYt-Ph^oB{&UfG?1NpnZBp zL<F0Rj7<`2@^{r4XU9g5(Agsj?5sqkT3UO3aaB~sx8tM zU?HEMn-+E36os#UZL@7gS3!N!*f=Hxl-CV<$&QPQXkCqe-Aq8&)T+pk2@VWI(_t({E$d-hLKi>R{g?FuH z#Ky|iq<6vM6p`T|*>QV~bKfeDW+$?X1|Ml8 z3OdG%((4-Gc&(LEd&e>|jgD?v7x@xxiOik0Ya*Z0aTb7%AEVlAjoOX_YzV21R+AhP z!JVRDX}=cUnQF(}Qm&lUJ+^sd)Q%P9To+do+r|kCFem_urFL!PVeoCsaT?=&&b?JM z;QtkuQ$76zZhCViPpy~jyag4oZp(o8x){nI?Rug zIo$6{G76jQ*P7>*SpL93Pw!=Z7|M?TN|GOjj?#pSAmlv;&>)!M7mBi^jq^6pc~4a4 z+RIbT1LG?I=H=63hlE}=KHU_bs6y{eJWFE|ect7;;bOj9k;A%&nYqk8t&3!s7jf?- z>gm+@5M7ik{ZHmS*W0E|Rs;rV7fHgZd_uMX>*?D6e^Q5;|C{!yceqtQc zcx9I&C#gq#V#IE*MsXyUSKo{9XYF);-uyY| z5?{aBK-$aQCG-~cvPq?fW6Kr1FZs^pUgV^!stRMZTJhpAe?5M`g^KO)!4&CoeQVzN zm=L&LR)5?~aemv3$1)y3jgpq#WDZ(x92!cseEY$TfpZJ~Wz0PH3!G9jWSaZ@$*`^) zgXHsGPwaYfftz1}Nz_C+9M|)K(u|6EB?wX0&|Lre(JTJ@rFu?xYt%p}!PJL!(bvRUjV9exVFTe1u5Q39bgWrTfT9RU)=kcNB2Hv|I*aGaMced zpGhp5ck}B^<_jO$t-&b1=$^L`?Y>-u>XOYu&Q}$~zUo7=kl|bN`NY?kBM%07Zr+nj z=sP1C%F_I0>efdA$AubIs9nXW+e>;E-)xt103X--3{}YE>dY27s-Xlj3<>Jp9*S^7 zOWD)`Hq>qYbK$fSX!9ocgzF0Z1&*%T{?MHA5OLbFge#d6qM`Y?RfWm+(A|@tR-}pF zb}BuwJ;ev#Q|i`J^7AT+BMB}Fg&s61lXxpg6@Ixr{duT=c}OYk{#SRbgd=V$QuVT@ zi7D||=${#|yCN@nlsgehao;H`#sE>F`$C!5E*CyS$G;qAI(X0gP5k@m32xXR+{YTz zwVF8AWW2hj?xUwxckzvg5S3pFYsIJ!lU-!3DyBuwyT{L8;-@h}deHV)u?q1X>%Q*i zg%1mzNPFYhb+ILS*UEWYZri;l&WneCm9iQRak$K7UelB?QfpHmI$~Rf822NJ#4o3y z6M-h84a_617vz*rMN)>H);}NI>iop3{oE=0cYRl;c7JZ;J5T9XbLNB9b}hhD8o0c# zz@v;nn`gi|1xL?M`##NH$lA{!&(wzEVRY%IXTq?|7(jfK3%mdpx4S#ahEZbYlu7@W zB7`kNGdV2Ou|!eDIu&y~igI~rhn<85<&1>{MRSCvVE9eN1==>FvL5l_YP|!C$!zy| zOCrhY+dozntLDhSdLWI9E)5d80z0QPGO0f|b^4*K4uxvaM~+k%X`4;d3HuE`hS!L4lNwdT<@S%& z@SRwF5Y~8bY5Bg#xs8(uExbFjFZsh-_%sfjUA)I`5uTCaQummRBTfkZ@c(A zncZdD&rS0C_IVI1v&JP~isR8N`|L4vIGu-_xvy-Zr{mq%UfzK9`Aa$dm((2}`VCqe z-XR~y@So`1)kd0p;E96&o4Ou#jQa!;VD1$t@8pPI8fo-RSk>;fsNtuFsC@5Q#6G2y zKc;ooP)vw_h4Zbw{#nByBMkp35MlzzI8o$HWqq6dLRvbkOI|LcBvV39)9az%WM%y= zm+ldRWrHt5ZTHD``RsP?$_`w4KCXS0C0CwwSDmjt2n1utvq{#Y#Gsv+Yad0IHObIK z7vJ?>!iY7S#Oqh;zA2HS87{fLM9vVj0Wo?G@aRiPxgdnTn&ui;@B3`>diQp$jM9Re zc~9y$6*2UaaMBl&>>j!2ZdoW-eQwac)U_k~URJY5e1&=Ef@6_c&Xa75CI&|q4Q}P4 zLXE_W$S11w#>4gp1a2xGTe+bmy_oRCUdg-Mtjt=%u<1~)Oi>~G{cQbRntYonLT|1; zId%2Wp}xxbp0+0fMpJ#K-7k}Z;*^)pMFG4!M5y-O&61b)u{ajZ`}PqM1nvc(A+?iV zKe@H%DBP~R@J?1CIM4}R@QmbRg_%CIMk(pijdVSOE<<7g!rY&K^2-G?A39YE7V!Y{ zTlgY_D&KKrerOZ-(duSSRw4UfEz7`}7ey@AA*wNV&0Ilw!Y6>}=@^aL&ha~0XKIEa z!`+|XV0vC^W#K+x`DO_uCwksJzv4`71mrAW3>NYReZ>}E-UuxTxk9YE>KxIUEzbC-{vhFWLv-h3cogr>Dbo*BLL@V99 z;rkL#E-Gi*YtWW5PXq7y>Z4N>#zngJT(lR90Uk;zwXW3#?oXv&D*}D>%%sa55JP6Q z?aHI;*$LyNhioCI6QJfM8&oA&zF)zqTW!LH`Ag-~!%HG}N5MDiAJz!M;B7*$0W^POo%=YTA!;Msv* zuc2lSM$;f)=jOmW7WSaTXS#uuD?O?Yl!t_?^>Qi)CDmP%kXZ5pz?|yn`l=@MQ!|Uretycd zJ!P7@`uc^eGR{4~dv>%ktQWU>Ffd#M3P(Qm+eGx9Tza|dW7Hm(X88eprH3d3+31y5 z0NL(3a6$T1X`Iu2z`N%|P=Oy_UE~a%pgY!k`P5oI8P?N^PqYq15tyHJW>E4Y(2!(e z^trFNXqrNJeO#B^QA%4Fs=;8-K`N4IHmQ&Ts=0;c14<)tpqj#L|;O97=mx=J8I zrJ@7MO+vUpxruT-cGKq+dQic0C>_+6sezi24085_oo>JfKPQS+gOzM9kJDVpzacTF zsx%t*kxI_{l_mX!=0ui`Ad=I1nc_t$`@Zf!C(rjO9^ijHR+F7F&Pg7tV~w#Lx3i$C zSpn`%eg;gcw|%MYHEsy*vpjF-_8@%b*8SNH=jFi#jfdI@s9i~1{9qSu%mI`= z)tR&(Yi314NHS51>-K4awA7uCRi)G2c9QQ%pl?6?#9B(-yQd)1q_vfy>8kz(X}{Aq z>EF>L#(^}Wts*TOq6sFE0V-{FiHht;@uf24Un50A&a;WkVwa=rwGRnebq?9VKt|El z{JQDwyiS_#-SlE+ROmVr(I&Y&Pvk@ymHZ~kI*7|*mwmeTDtuv7S1Rkm9)s<%gTcG7 zBo)Wa*ljZ~lcX_3d|2NiE_+dQlz{{Q#qw$))?5Nmo;gZN8Nq^&z zvRB~BY=u*Y024i9VZtL*HT4V3B1iOvjrnMytb~l)92K8Hl&J^E^sb0lHBFO!j48TV zQW0OLuX55sEhw}pR>=agtvhX`U5z5&zq$4?MRuvNq?A#*F7}b<)53U4VFVdgpIw|f z!xn~38sLB}f1SDQ_Gzm3+$Tk0Ehj5;htJ=b+tJ zFR91ss+|ft&5vv{Ahy17V$4W&ugM+~3n*aW7^x*v0D{HlQh+3(I#vofkBuZkI8`2d zE_}U2N?A!h9mP8D7tuB0by%XL5lqx@myEiMPf*1uH30(hzxCFlFnz5jDTX` zfm$o>FG|jeaNDY?MqS`?Bza$i#PIg|q!S%sGgH8kU^Gb)y4A*gCtKM{DJFw#;kaRC zx4x?vpdI%n&F0E9Aq1rAW%jr@okzdj;EU(b-LoBU2(%AiPgSMjR8dxo-NH7sX|!YqHo!j5`F! zpz6a`76-);sZ^dMlpyAV(liT?FF-dPycU9JVIk3=@FHqrMFHEW=+ z{uK%ALDcYbVQ3_F2Qe*s*7dV!4cZ;CPoikph5<{i^r-|v6sD5H5cir1XW0VllXx3(rARu17RGe-@!Nv z>=KgC31p`mu-d&Bpk*XVr3;DJ33GyBqOeJS^XZc?P=vF&*STbWj)M331U9FJV5@t_4qvCdG(hJ{DigZ;<^B7P z*X)@vp39q;VmU8g(N58woKA)c*q2|^HNBnUBE5il9m7xj0+yNw$}30fDCYq@O4XyL ziy@;xI1lLxsr!NirHngbruOT*o6_x^FGvtB_ByD%*xOtok1j{HhG~yT@sbu}X}j%= zx$lz7+p6gkO{nEK#PhVns-y2U4K}5GjmBM~_EAt25WN@n=7Ni(&($IL1u-ZxJn^$3 zCj)fyE|FdXG9(EtsQ_OzYekJBn{xnvD=peIK z#vL<^C&QezQ2tmh18dzAw8qCv%ZT^)DIe}aK-H*ux+C;vM5#&oP+0(N6LCYnk0FlX z{LU5x1!9B(wXdvD64qKJacYqRJC`7$nD`!kXHU*m!$bsufO;)o(AiM%L00w!`ztS;8OP+$y?np-GcfLs%Iy?wl$ z6jPif2NpQ$K_&79%F&Wv3%!JNU9q02D;KpzkvSwt3b=ZT0JFxX0t%*UV( z0Nt^aZRm`^fc4PMk{+dI1S>3y_Q{}($DIFgj~ixtNe*9q@FtZ+MO}=PTmWkDK6D;K z2f>fl^(P7PVwo|t?}>H@`UuEZMw<*r>^5amj=t{6`z$(=3>_ClUwVEF%xhaE@T?Z= z0qZ%*5GsKpA)h^V$~fO=f1Lj#`Ao$eHVZ#{1t|gOl|$ztNqD3dh75ZvZv4}pS;jcI z^#M(q7Fvg!7A29UyWWqH%~E0HHi3}euc1-q_j?feZP{e3bdZNm{22*L4xwpEQj6^! zfQJ@2R2I|r!e)v|}ToZDKdw7&f zO$IhkdPB9#I9JG%XuMgKdmwQq*@*+=RR(;s;iniHad0$Th9vDVYhQ?4nL;ptd6RX| z^`WSdEXzH-sUS;=$+1$s$c(oO9Tl{xlHqcmLnfRwNirnBP%b<~!S^dhqqw;vS50<; z7^qsANTCZ13)>l@BXB5Blx9US@Ll?zb@Hp)W0F+t;!zh1-@Ujca_F%=I9raGn~wVd z+l_cs0!*fz=YwR~Mg7E(jC71q$VemEB>}Q6G2X?!vwUn_P?iBwiDD}$dBzKc`1&{& zm(lNEn1_!Ah-W=9d8A{cxI#Yckie^bpy38-W(TOuR{+^f94ic~6AEgM?=oPfpItQu zNWWU78Wf_SkwJ-{kWg3RNXzG`G5&0UAF;#HyRi2?OEw=snbnAaBr`3Sos&T}96D zRPNVdM7+2N{16FJQBd&Qh*0zeI>hpGQ=2w3fww5M00i8t&7gPJ5R{A|WVS=G@mw8F zsgfUCt{aM&mZo>urOqomuVuZz*(45e$O$AqLKcF2Jnls)u8NXY50War?t}pdFs);= zOc#pm0SLJu=>3qdjh`Au4B{T(mo%`wHKWaSQUmyE=_QIbbz$fD$1SI%93Bt2--?1_ zDOuH?-!#os#e~Guns=yTxCfM~bWdvn8L`Vbcs~k6F+86+T1!$gf(%vKTRUwnEuPdv z;zaDA_V{p#nPDm1M;{=>G(MOJf>tT(3#BewYHZrE)qGKk_9zJ^9NR(6^7n34gg z5ePp~jsU6Ep2b>cjhDPWTQ075t7=S@B>TqcD#;8GEVYz5VZv=OWL5Kcl(%YGKnt~u zM1Wwp5XZsco8}b)pJxZ3@gvP5Qkb+?mp)_;Cpsv-0xK)J917~#r+c-zGP>;&7eGC3 z$KF*6CSktlq7xA_lUCd`Y6L2P*5tI4+UQF zB7^2uKyCX3iGzVN0Dt!xIW6MH3+v(;cC|CCq@Jec&;?GI?D0>oD=IG*c_TawlWX-Z zU%3+f;*)kV`z26O-Hvt()Zcw@M-!*e2B`WMZ6`KdQ~>3wcuV-XQ9zeD@l*;C^-*sM zuLhtD5>+z0kRfL* zfpuAvtlQHV;L^1qurv21WjVo7?R?*Q56O$@V;-FWDHa*0*}+Jvhmu*mMTLbu1RvAy zaq_x~k3A=K3lLX|+Al-yi*p;q$ z#W>kvm&b7EnGzBWvZL2dEX_$rm?Cf>Z=ODSC`bMba7uQ4XuMNvT&&MsV*N<}u!oK~ zlPPd9CqAI4vNA-1)u*2pk?n$Ao@+0Bb<Tj-&ZWfLRD{)p+Tb4;# z+&psYTFAod`{q#3K5$(}=4I&Hi+*okfDlP9xCc-eHqg!yYPafOW@YQ7I*d(-IsrT| z9xI8mYdFP_*_9|ic7~x~P|mw(77_%D>4jb!92S7a2Inl@iFi?r^;E^fD<9wLOk+8&7jn)UkNmaJ}$SS^A?K;7^Y5 zus6YmW7G}%O09-PSfIG3C}Il7L4#R?o>C;lD1b!T!wkgVopJ$pl_c6o(^)oRJ8&SO zZ^SGp&;B*KhE4^u2b4>TFhzi?9<$`1fm4~8Ku1p3-Ox?FC+6wHTP(8!chu>VKw_6R zE=3nhTct*)&fH2SP4pT;kLi0D?ES9qIzxu2xzRbvwaxiPnrHY(NJQ{HKMn+RmC4>% zp51a{7LJYdOdaf{k1WR>g~8B|SdoIpbWm9A?(og^C3=y&Qb?J}ij1RTE0c`7VkLI5cVPtXCHgUo&XPV{!hP zb=_Vd84c3fG`dd7e$Q9<6dMtRQ2T+E*LN(0TFIT)4ayCYQ>~hr(bW#!5wu)I26sLR zF>*hRBqE)dD;^->Xu>L8(ifZrmxkK+n80CZcA|Y5VTyXhg(Uf@G|SD+&4c->=m`Md zxNni|FHN=tjPQ_8x=cWk9wX=eqP0L>v(=;+RJZ3wLW3qz7DPuVQbjV-JBS0BG{)uS zC&Z<5GqfaM9p6lE^PJ|gR5I1VdLxni-qH4tJGpc@-$bzcMVrg$*GVol#@=FNLPYvS zC1MvsEVXS`YeGLxR2cYWxkU@2S8(AOJ_q-Ec$8=(fM*6uv%18g+{5MgG#8W75n9w( zL}wp|DY5OYXLz`052?W>sh=rZl4QMnam%8Aj?;jgso{hV2a0x(s$>`t)ur_r-Wc=Hl92+ezREH=jgpAQ54gk`)#fs+P8vuK@F_R35U-) zQVh^~C6yk)h#HU-v;#NR9s4M%T-c(rB&j@>j17V9O_|G$_k$^Nrce+^4t@p~s%8<; zhF1%R`nnEOFd&tqy*K?e9EMqi0`(>Aj-;FbQ}gT4IuDiYc03IM%mcCdYC~lnG;=WA zsm5oi1!i{EE&i`)p(-Nut9en;y*@725RYJLg_cme)7UJ0J_f?Vp>wd=0XS`5G!+A8 z-Xpm5UL+muJ}b7U&$Q^%F}9M+A(vcjqqIQf{T;jFoAgoZwskG~O1yB4%a-$KK+aI; zxbV8!C{o0!CSclVrCwKZMIB}@Ps4v3PC~~9O;RwZlyF?|g<&(`GthiHxF1s6nPdrN zt@BpVm*2ei*$0N*eF=%V$=g3xj%mh$7-CH`G1N~T#X8o7Id_DNkJ9h+RIhsYXCRey zb^ahmQ3avchRDPzlVOtc7+mxeNP9ymTuz9nNK6*%FfCJxtsI|5jrv$)6NQaz)blEWkDcTKha-*~fn%uR@L}K&s!2pquO%yjm=JMQ@Kn+!Bno>7 zT%svE$c1QBLeh#*;>06I;+)V{k`}T036LUJH8ngsNIeymY#U4s*T8TM?SLiuET9?= z!;5IbxK-qZ)v)<8F!YIr4=Dr4R7$f`xzW%a8YoKhtO^6hwx+E?B8?0^KaAnGMbxOF z1xZ*DajX*QJJYGwKAU|#g=mJ?%ceul=Ohz(vpK_$by9-cEyan0{LZ%w3bPh&6uBD+ zCwD-0QKxxe)6gJ#1O`W5WVqa(DP|$yz(9+LL#YXJyhXSZ?1D#3 zB+=A}N0B|YWIQ0Rt%{Lu+%=)Pmo5Z(nP`QMrWX`)m=_vdLm^UUz)ep-R#dw95&0@T z6j{|FVw}<(0y&v{TSrh=Rm6$ z(!j#!=v%o*nBrD2{E@&BJ!+D$*@#>nxk%&r{rFbuYB(Yxr<)B!1M2O|bo#n$^pr(?LM7*d# zn+VG0;nut$gVdiY1#)-NjZO^`31itw#Ll3wmXa2qE)##myq#m6s);n)11<>6?}Tyo z*PKoQIVZGp705YBS*G2=f=YHQGqkw`tAv)h#%(h}RqlWob`oEM{^DC&>GDr$rC%*e zItb)=N0OokQ1EfeB-{w!6Ji%qgI3t40f?g>Q2^uwY11S;ax3o3h_gR1&;VMuFWt34E4~7DeE-z>q-{ zJ}Y3$1#x-xr)YvOt z%HWp2yvpmlK4n16*)QvQ2$Z33B{zFRiSC3v(8dXIkL~x(=&vojB!&|(tUdKQTT~q1 z)BRUHH4EZWJxZ#M7VA`*hlPum?se<8UI;b1|CG(Nj9u;18nvm@La>N0lm5-8(hGw; z@4bU}cUIk_DVP8fh73wg08s!wT(wyvZ`uE2@2#V%`ucv+wKp3iq)X{kx;r-^C?Kgw zgNO(s(kaNMq(h~VQUnC0rMnvhr3EAe6r{WETt3h5+~~-hPnXwb+_jXiMNCR+PT-v<64SGzV2t~w)Tb=g*XaPQOqbl%i=XN$a zh5bxF69gHu6)ultTO#L_c7PliArmMA1aC})?UuiA5XvWm)YLxboANHh)JV5r33Gs= z)aw9}FFI?+1q|{7D$AqY7fra#LrhMD)MMK9c%9qYeEtexHko~f1pf$reMY1K?anCj zWXzBlu%Ns(O+sb-%pF=vWXQnq7Foglufx?fq$xx3ZT@^dU*W9lb$Ws}6#AW96AI1B zvXc)R#5txgZqx-+lf%>@%f$Ej zAAaAhw2gckM-uyv3{{xgV2Su3&WnJHo+ul__5&u|H+8U&huY%mnm%3j%Q?24t6Pl= zd`370WD&jpnz|AGl6t|};kkX9T5s#$H1^*4`C}hAg@^2&st_vDcO3!_8?{#SlkGZi zZGf`|x^1zmeytdiNIfPkH|*zsAMBX}K%`3lcv>iO;+6hwv5SzW&s_S;;rIl1gU4yF zxy4~4O_&flMg#dMwsTZkV4-#1;my+y*fBN?gL@6ny0Dqe_C-hqo5O}GtB&J=q5k=l z3PCsBcj(Fa7*c0|l@6eInH&1{k1cyF`ky|C@rhF*LCeIC1U1if(%HP4C zHU)Yyr{q^p#I|gO*pqMPydJ&tJAuOG>(7>v-0L_dXuep|O&C_;D;^%H67yQ1;`~u? zm&FN%m1- zcHXEhAcenarc#)GeKgB8C@Li^*;iPw_S5{E;O-~41Uox3qIit@th>#bM&HOjqtbH~ zNq+mFi;kRC&f)wv)n`S1@_?1qmtXIcnl)%ta90&h?|VF+UyX|cd|iU~sg20{oEbCQ zRQq>L&h2jGpExA!qians@7;Nj!0t+ltBwR~Py`YE`~nT|>Rl=!2Q)mB%VQS~-}?i8 zP3KAN&J(X zPNJ-;mpr6nKq@6iX?m7br$fp0@LM54u!H7*v-UU?{{B4ioTbe6aZ9;mZwobjp%?J@ zd4anyvha?Zfm`zFaq|a0dfEw%iiY{+5XXq5yvU#Q190_-c*ei)6D(D^9d`lsE7=ylO4yvpx?BPD8&SD%~YEWuJ6!k(RLcp zn`0%*v1qrVsVBa{&x-;x`V8N_e*61tEmI*&4(^O2S8P$t`mtNhac_+4!~S23Uw4*) zWxG!GcU$M7kMK_)`kRJTABz>47IDFfeZ1P}O*57RW$#7knNB5=Ih-jAj``^h9J0RS zQyD8vOZucUVtKqO^@F?nzgvBz9EuKCT|9#MxlCN-nMs7;o+Q6V5>-mL584(jve;di zmd;!{KN`~&7ZZYKNTz`MDiM1pT%PlJAUhbM3x8aBh$%q zbd3hnvm!G1a_wlvvzaYu(gb|>F#^GX1)pS*FRp_xv7O~SO?x2F@wu2C`j@ILMeujx zBX!lW54G2yz0OrXu6-%#w@yNm0M(Q`2lqIBZhvCWDDK9fDZAK)dl-PZj|Up7L8MkL zop7;=Dgia8yzEY?VJ#fcwVnK~EWLjw-`+W4n{s>g-H{=_1FW)3FU;Wnyy}Z2u;LDl}(%GxdpJcY+fQPR; zVNvIsQ^~?$LIeqaH^-MMEDb6b=QTTDe${Cm6T1Fh&aWg@&o?3VdfAz438P7<+GoNW zyOLN+pQ23|8(A%`z+Wk^|e)(Dez zsr0CPgXFQJBTViL;|-psYDwYjqz~3RXV^Id$4VPQWj-~EO(bwMDD?E;?B?inc;hLBBs7cPESvHAofk z!s*0X$-I4;Er1ywDLB7$Xu|UM;EUs-+OD9u$L&;K^m0w1`=?c6G+~$3iQ3vP55cFq zL2Ef5eLT&zX;_+qCkxHq3%BCD+MB;YN^bKwN#Mc$FDSy|aK5diPmT1rp3idcMY`tL zuq@~d{TrsbiP$!>h1JhiRYE6;$;KR=2*0tDG2pwE+I7BH#F8Q3F{oFXND*7k^CNa5 z2%h3AGP{x3V8BV`o0Q0|k;-22?B^m_`JuJ}GO61#g{$TFkxU5*3n{fkGe%z@G*pR& z6{tbK786<8Cdc2BzI26>JEQ2-e;P!e><|n|^?yx?Qw|F}zO`DIt1Va}-lUKgp08d4 z96g_mD~ADzzXIeWj+`#QumT75ya&AJc!5+2c9TmLI0?~ldw7^N_#^|%l5zw!e-4|V zW)nn7O|1&^6I8rLLvR|zGiE;LVxvzYK8KFpz)kc4m`{?qlzN?bWnV;m|JoB#P*m0N zNNt!&-u12e3AJ+Ta}u51=)mfeeSR7%r>a9HCda3vu4?Dc3M5p<_bnT)x=>>)pjxR` z!=XCh*MS9RUm~xH2k_93V3#n%u;Oiy9fa53*5-NF0UR+~+ZR%n4XSH*KIEpq1^iQp z+{LL23<%ZPgTR~8iy4Pq}B-GBskRsrpKH zzOrLph;3r;Qp*e(#-ZWpMZ@W~x;GHR)KP`tVU}aJs(wo97ybbTBR1d~(%K&x1CdV& z#-QPpK`hi4S;VHLi8}SiNFNifDUi8+9>D=Xi($ge4NOJ6gn%G@<4y;oNy7GCfeqdej(IDndKC6>r|A%9oH2$_9F!)SrFHN&?T!s-17tV1t+u-u_Pm zfQnxJ-kj*P4k+}*1?0>#4*52(mdnroOiOyNm2_r5%)R-NHcJ--M!j!qQ|7vp7t7`j z8>&D6h)%df!ZSdB-KlZ4J(|eXVw6l(X?fz^5`=drN8{>|y!E8~+3stRGQWfG9x#$W z!9VoK%RAEPM$tN=q)_XePUJ-AG&ikIop)5*lwho<1ZBWwwd~rK3f< z@A=X4lDaGqPNoPw45$0}Qb6Edp0)zf92ciK-)T)&itZrWa5D3J_FNuM7@mVxKliV& zrBB6A6}AE)iEA8wv5+Pb;lKl}xPV6enF#!eGsh60xlEX0`k3a4_I+ z)%oi-TkH>o5Sw+qwt|KJyMb}{hcWKWLC}NHcFQb~WEMN|B%y?XRV6a^K?le^(Smh$ z_#|p)iRRB=K1~OiPP#zRX7k5{?xULS5Ac2sE-wwmSZlzC0a0ZRu%N{PMvOn6J5;5} ztbVaxpq3SeAyYcDJ}QvGBnt?t0(q2QN8Bt!XBeu1f&h!-A_h$ z_fP(9fn)l;4WQ|s8dlpSq@!S=*Ni{ipT1Bi&sfkRnj&!rll(yuYj4OunqRNn;-%Mh zO=i6W9)B*exg|{4y9WWc@`Dm-)y(_XNIiv|7jH^=@8((U-#nC$Xu{@^zVjM*MWw#~ zrc@J6{)nB^k8{7iH>)tQeYVHY_r|I3EfWJ|4qriP<5q3$EM4Q+yd3ZL=A9hl9x}E1 z2$x1jYAnoEreks(JGRT4R}KYm^UHmXoV}ORJhEpg!#f1S{I4otUx_J}tz38{(9n8* z{pL6^`*>;Qsj+}Ss>aU+)5#N&LVw62=VCd-Z!#5;pb!hGzQ6oF#_;H8f9m^ERmGF$ zl)#D8XB+j`KjGnKDz$v14QCw8l4k-^lCbaxn>I^5@tl&9hOe;M`uYUbL$LMUC-55g z;1Pb*;(C9bJQUx0hE{xLaVx1>{K6R)^EYt#8Wdwt;Bx8A{k3vV;1$=nV zrjbVZkh-r|UWOgwGX6-!vFf@iRxU?}3nfXLS)t;XirY*B3_k(3O=x>B{+`9wHQO94 z?hXr*{9E-LVr7z|vtJEoL%p|i&UST&%uT{e-=pLRAypczv- zQ(-^FD{o=a9E4hr$_4~lT`B(Dvq-~{T&=`2obc_wWZ_pLXq~{DnHT75Rg~w43qP&X z|5!PTQ>9BdDMmXLYMg7&C4C9}Y7wdIYtgT*pAXplTf_L06y5%7#Wr(tT}0}kERdsL zQ)w1ihlzoP#Z{%@6ex)&A?}b<7)u2T7+ux^VZNtsZoW!{W zX+WY_)o)hbcig{MZfBw6Xr3YzA4Zrt(4qC_mFl#iwn=|GcI7Bx?Q}m%n)Q@QA?Og$hxevPh@^I_-(RMS>}u_fsVZ;wDhfY&c=R zU2&3TH5}~IS?hkNm2}I;*}$(TzGnQYFEnUEDwQHY!xJ5C8%#$sF?#>;VC1YkY!}+`&ZJ* zUkz}p;~LFnvE=2fmp8xEsxj39NA4%rOHFSPLXbN25ecg(p7M4E86ZrGBhlU5NJtkN z&Lq338;C<_^#%eRtEs)}XQ|m$-_=jpOz%!z_iFi@g=+F|O0{r|Mlewvo{p$rsrx~F z0;Yp(cF0aA{-U2_Z%<#7lIOudy070%i36pFcSF!2qZOoX`h)rh6Z#Uyq#Z(gwU!f; z%i{>M^#xd5Ye(ZHl94^{yiDS&`TnvA#7qHtk~;X z43Yu`K}{4W6aU)_;%q3(AMGLLgb1Em_w`o_vRQAwIw$|*D~u{O9mBid%Y-FPm-xm6 z2hn1=3v>@(fW-J=wy?GLijw^4W-D*mEkMT@n(h7i_Hecp6O+kFgxvk)0#=CobWI;e zb-V(b?sxpA!vfJdO_!r*1s=G+nOKl6Zw!yThk_oE`fPDYc0g;hAf_-o4G%&dlEiO> zVM9kPXBhA14G^IfqH4hqSCbOVYW_Lk#`ju_W~8lK6C0kwh$C?m3sR`yqj44WQ{pOq zZE-d&Jm@12u4^0W@}UJK_O$tx*7{p!k#?)rw8JR0eG=*2n!fiY-@T^|Tu1}(0)@;> ziti;=>+0#TM}!O#(vJ&%wx3FvD{8m+*r&^k8&s&Oi{{K^;_x&sL$9NgcJd}tqC z05PGx`5+lA_UNm^KC_z>;E|g0)wT{Rex}W4fpFgj^3(lc>^m*Ftn-p^_a&H$?{VqI z-f9z72xGM&Aw2E*}}?O#ckIgtIb$!W+X!m5Vn-Z8UrFufZVx{;A+SY~Xc}A3KWu)* z@Np{m!>^aB3@_<5K8fB^Oz2q5b2;z z+Wc{#e+#I04Ny!A~40y_MwjfDG%sS+RwJr1gEV^p_fN1SuT> z>FK55s5+A0ne+G*oS1ejFXm{3TU&k7&HJldqsIj(JFZ_r@lYr)wAKC?LAe)0M90AYdZ8paq3SSq;YExQ1B2*T zVFHlEeo}jYoTGpBOJc4MhIHy$jrl$7WDA335V880r}X+^*eZnY?7n5K^&79e=QSjf zXK{2o5~|t$E>+sr=@3IJmj8w^0)OITGPH6aVPOtqP8~k>pBctl0-%2fY{c8${kOwX z)cSYXR|e+Tx;=g=@#PL%x150B$DPD<$7!m>+qWZ|2vM%}m$gN8tvf_J%b>ZU5c6p# zar7r?%z`0=Td35;q0j8J&4BO&@PYya?X4EltAv><^U=H4CnCv-9a=Xen~z{ z6;;S6gTD3pTI}s7f?U!5W+}O|(CnKL?~iP~iw>yE3J^FddWa8couAW;0Vpn$vwc5# zr(M-f-DKwLc)BmoPm`MO?FRC)gXmWV|MFapGO7OKxx8}Ihw838?v=j~UWVoZ|1B7B zphQ${m6l%^U3u|aC7~|D^4aeGy;P?L1@wP0U1slmX;g>}jS%5LzF>h-rSe2Cjtcos z7<{oLv^P^{J7eN9qbh+UjT)4#OBi0ib|NhfcdMaJsMFefne4nIljeNvlMF|&h&_!m z*k)q2kbnWd*k_T9;lyoKRPHEf-Sw?YE&jDKLjxp7hT)T&2r`npIUgBQV#{{Lk=@c2 z>Prrk*Ta$@l(MT@MSLKYe)1K^FR}M1LzjSAl4^pzB1O54rP|yu$U9JDy>rzvvYqfF(8toDH~p>m!V((u1$`mz-Y0B%CvN2;YKVbB%V>P&$?l08%`X8vVL=nw! zm3ttDnk_S(2`lSaWU-SO>HR;{;TPfBr}|DtS6;oh$TF>PNlaO!7k?V^@>g>y4HAY0 z(J7sxz6X^SF@NFE&M-duUt!5h=$iEHP&Q<>i+TillqM$j)*ECyrz7rop?PjW<0(hH zeBT4ztk(Fcy#rYt1RD0EgI=qAUhnw_GfmREN#ImK!d2pM~8KYr}y#{HjWOQSm7|8BOV zzU0_=RowH?gtzC1%oPMN39cbB^Vh&a%B6aApz*F8xYo_$ms+lWOj@3lh`r-6G$T_L z(l37Pzj7s?jTYUDWOyGvf#4SVu zMal!qE(&_y!lbG5YZ2_^WGkEhVgYz4tJiztr_L+VWnGkhC{5(D&FUlkM+99)KlTet51B~BP)#Mbyi8oaG%NX-fO&Bt(>-4`1X)3$$1XI%m0Z>#^Q0_i zhFfF&$hS`{n^C;I?G0)6in-I|@$px^u-_UlEBd!y|D+>WRdZR23_=@_L7h1BPW>l; z9=AC~;b9Ke-~1pCsdbNvD8F`3$heQv-mr|SEQ!}iEJ8B6I zO$m9HWb5T9$G~nYN>yHSQB@VQ5<{Nl+f)RjzuChN!(4LW;uiElv|8xmh2THYYAShT zy;mx5gJcno-?qU}o`Kng-A)OHKE=kU>KBtNO&gIFp2w_}_gO}==Dn3n4pa560ZJ+s zZ|L$qF0nO^odA{i3ht&f`R=tYZRi?wRWWXh5QNxubgg)7T3GK=Ssh_TL5;%xD$^(1 zNswpEguT{3=HS3&n6w|EN1hI>6yADD9tu3=_JB?N>zpRGhKYDB5AfaZYOmc#&c(q0 z5Z~F0zfNp@{FpdF>6~AzH9EaZIM&7Z(+L|1McD2fwcm%8B+O&4z*#+As^&(5LQrA z^?aoIBM$>B$rBU<1@e@ukkEGHcJb1WZBtf28waL0|Lc*rTQZxgJAEb_JCREK#+QDZ z?Oj)obB#(9+bcwg*R8HPZ4<_vdU2eOiUy&;ULR;JHcybR@VS*Mg7j@gV4J9kiBgoV z%QZ;Fmh-@wCJw4&ek`JF!rCr6e)x%`R20yt3M2oPi+nNa5;r$VZM%D8xpcDKMHNa1 zSXheS0~|_TBa!d%bAesp=R&7k!KmXAJz%m`2F3W=0lDewn zaJxFhBD*BGQjY6D(`?Vi$- z{@aYQ-Xd^pd>#r-IaB5Iz#Cw3t8jMxjdUQh)&(eml0P(ec7?mpem*}l_q@4u8jhYL zl){F`i3plX3-9W^aBf2r(e}OCnTG>Bh$_b)0e5tP&GbFM&!=_!K@^n^fXlKUq8(68 zcc0nZg3#V-iF~&K5Yy{AQp*YfxSOAn-|S7PRkySH3{Dv&!xVI(V4^esn5S@1h>$}5 z3N9)MvcU-b{f#%NVAL3D=y&o?kS;^bz1EV;;?&C-0upIX;HRp*3qa4PI}JWw;o&V3 zT5xjsFbIX_iofUVEL6YQLU5-HXis$j;I_DYaeg2#<-CY{286qJ-YVnS8jjbvaf1LS z_4Anq-)E13)$+9VKh3z0{t!^{WYS4GcU^S`xavy3_$*uBKJc8V7d0H``&a|GZg9h9Sr~7zaJivYi2dCjFGra>|U-?_J`@l7x2Yd_V zAY%R3cnK?rj(+(E1hO4ToQJ#(Os4Ir^1C><5=(t=mj!aIVDez7cB6s2|DeZ1-sPvp zF;Hdafv$2VSCf8~5yUnz!lvzPfQcHu3cF|Kb)$xpBnA^C^f&$;0`XtmjU&TI%qgE) z-Ay>A7ku;!kPYX7B=u5_SV}ER7R4aQBJCn=o-5g1lq_TOh*ja}fP5?~@|fs?!4>ra z4-d?oDK59d)h*cY7C+U#PVGvl^Ear7raAJ1JPuD?Q{M(uOXHyPz zGM>fds7QK(Lf1fO8YtCYK}^2jv>!CF3lKxTPdM87Q8c2jMls;ljAyWrkaLz58qKoZ z%+sj*p0*|jh<2T+3Qt%4nV@K!zjot9An#2meKg3&d!^VlI}r^H@rAFApssj3V;A7fGl z7W{x;gPj@k9)VXFfKSPFGXm1h#DjX2HQG`{?Xrv4+A|8OwM;j7)YzG#$v>4zpDX zLfS^8q@=nw0MRL%2YsRYnShHb5IqsRL_?Wf)VxMkMH0A>{*^l)oFBxq<2C^j;QDuh zn*jFmCShdcZ^S~Nd5{5=FOjz(if6V) z((8^VU@|~KTUepCXlM@DSvUb%#MivfhD%bw8g~IZ#^L%S-4w#J9Y zOu+hR2$)SEmPc8#$YcN}pcF8U*yv>L3~81P(t1A-IM`z-OLn@8+m$VqhOjCD%>ooQ zJGl;2MG-O}I`>=S!wuMks}>~w1`L&k5k)cUEbyf)MbejG;cjDH^_TJZ?nVt`K2%y$R+v_3Gjj1W3_ljPtO@YXX%w9H#O*NA!UwB7^M)5Vfxm zQwOjKvycKcB*py(esXZ(T_~G@n7@0n0mWx1A9iR`J$sf;wgf^cc>~)aTJ}i~2ue}V z`Z&Cal$UN- zs{!&VzV`M!d8aY(eHlMpjU-ssu-L%m@oyhU0$Tl4lLn(wHutk@EiViY327g|K^|jh z$=(?II=Eg-;%E0?UvKdhxdpca5^c%Xpmge!v3QYI<5wCA9z;iunU-wuf*7@=iA%wFnEmx8Ng*IpWt}5O0(j&uW(Vgs6A_qM-oq7Yo;Q*2 zzi#@FXzsfgZ_4+?BTDI`Bl02e@A$qNn7rb3gGLmE!+?_a&qE|uLiC4QnnuMQV51^QmWCMDEJ{PEZv5^fV zkkzH$W>8z_y|c3O4M;$`qr+fa%$VMNsi;H3=MWrxRAzEwwavU6IlWA}V{TWXU5i_D zC+m8@J&k9Q7{5b6>v~_Q*y4R8F3<@`pa~L^`>v5-U|J9ufmjC*A-QPV$#PqiE^28I z#Z<9=x!5wAjqaKX)_sDK8=?)pP%DN z8U#)XF29f?darqjHIr)R?oSmU<81K^=5nX6j@)fY7`+irk#&A{GQ02M-S}P=(!N$v z#USTXH7!ZrO^HYXl%Yt}!lJsHB71u94OGwQo8UbT_;#@hfvSQ<I?`e=ps7kg0~Mb z{HoF{KV)LT0@g!+`*!q{W&n3>bK^2&HpiT^$K_&RYX_7rU7Kao4q#0x$F513gqW|-1 z6a@)h);`tt+-Nu{oaURNL^SEoF$oltxNgjt&IGzBSZra)+Fnj~5g0Vn1n@Tg(1(bM z(=kjI+-qP5I?+ub;CZrMxrCQBUO^j9>9ydh)fw3SrlczrntT5B(t5~_23i-Lg2r(K zbw>D<2mpkXbhMyd4va2S-Sj3%CLAU&FxT(0xCs7zn4S@sN`UNNExU2~kHmwwAh%DK zv*0Q(F4Wg3aYlCT@&*?#7UogL!c)_LA%|y_3dF#To$}I z7X%3lkSNVLATt*)c>y25&^Yjq84pxpu+jGsy=|a^%;J}+JP^CjuU#1Gr;S%;P4}`M zlv}ao#cX$OfCi1PJOwQKz69P4XfsS$IToGG#3<+ASg?qPaP%Q^3wjey(&R^MNBC=n z55UQ~FCZOI#fKMj^&xQsg z(m@BzUMX7w0XO56v<+Gs8gV}zlDZU-B*K`9_iEZ=xGg*42uC7I*Sq&rsUZpuO_Z$j zVrV%T6At17s4i3PvaAWS;j#pDGr>u?22von=bBSDSdlVP{*d;h zUzDdjiU~qQA*GOz2i0`)j-k*j0cN?>3m+r>8w|EZMqYFC0i{zq{JJ#coUol)Y=_IL z%)O`fAfKmt&A_Wa;B&0jLujt_kPFcumL9U_r52P6{Z+Dnszy5n^T9sTa%Kfhi8|Zw z3O}i@z_rb;YI^db%r#evI3Y7s*Vu}&%Xyug|JeOFYi>G7qRsK}2Pw<%Z8Qoq96DbQ zx1$Kb3NGYxb9!srM6&2~Ichny^2r2?14G-R2${$}?t`O^YCWDh+}L|PJ1PF)Fq!6t z&m=6YH=y8RN+;xbn6~`wr~y@%gQ2ERUni4wP=yYYDxQAll6Eg#_*GDp5CM68^$%I| z^2`|A2WDJ$X&(m5Ws9cuMPJVaFVEjEG@i8JthL?Kbd=1eLTq~zn8kWlMCA&8bh~t; zzQ_@pJJ{sFiD5E0Py>6~)0nH@6d)uCM-=)N5*pMQOcD$P_C$|rDAwGk+xSPB%Ab!7 z$G^C}%;9_AIT)P~BbMBmmYt=HUXC~-6G`v<8J$MmwDlFrkTlwv#OB9ZlqLqcpU>qE zvvQJcJ{6*n&zekb|D)MDfhg(P*jN&;PAP`FbHUHr?SrQVM@WLHTPQ2?%p1>bM+oWU z4u9b=w9l12A(Etf?5V)!k>^v<-#N&NTI+s?U3U$`>vbEtFa^d`D{@I_^R0pzrt2N6 zOxwVt^#(JXE>_}ELvJUlI;y~!_jys$?hV!CG1i+m+rjx~z?0Ves9BH3#|?Ffe;PMW zOU{X;5lpkch}T<-40pp6qy#{{6bS=nb8wO8yF}pYeHbA+Ohzkf)okZN;z| zwsuNsy)Qo!Q|UZTj3mKeGEhA(&?b3ug(WFeuJeus{=(%9v>_f;*A$&g>Y0yOPL8M< zG50#&Jq*WdAYjpYv?+pB6fZIL{Q{psS_SGEaX?06|NE=dpv{pViM`;vdX_rF0|Owq zqxT~hZul;={l2<2zft1Fj1h&*GVfEvzlfyxE`&fMq&V}@d|_Wgk*@{-IN{@+`#z-59sEWjoK6UqXb4Hu0rfWU1( zMM2o197xc@5ULy>yk$=1f8O%n+U1l_K<%qzi02-4(ZIZ@S>3Dlf_Tq*Rx`b`nE+>f z1QIQIf_9RCTd?OtQ~P|?b6K}1jG;xQ_;in0x6T}vcB{_Z4RE37?`|~ztJ4|GVL133 zw39>HG9FNjxtLLeK#pcUeG)g}KDwlc$wlN)NWHo`KiJya{>4@f7X|gt;gB|woH88}j1&Kz zo0)SW(2EP-!#QBFZfY(3*QJ6|C) ze8n8it3+q~LPCE_NJvA^M>O(s$o*{Z>GUW*)thRcva?+q#cw)c<3iyII&|=bmh#1l z@nqGk3K_-TuOOi}C-{O_L6UYOu=Kgf`IAP0N#;mhWrLf{BR2&D`s1o5x=+pwbBi9b zLWf+TXUw2u$6@)GXJPS+fjPJ>+1JC#y|;2q)?S!SGm(|=kE3H+O-`B79*3%xRURpW zriv#@l7*#h%&*~ku3NC#)exuJ?$_}*ti>8j2M=e`o)0Y@?+nr%%$~G#ugmRZ-gXHr zHhKAID4b^J^{3h^IG6E}=q4Wu8(erMsz+YJA$l_B_|r}N_Pg4=qhF_!X#+fue7>=Lelm2j`6e{cqmHB15)5CkYw; zaFW))V_M~?%0$P2L^Ju|+hD=JBMSK;klZ^w>#X^0&+qfq-9TqW8gVs(#-EepvDUmT zB4WAI`th|7$(OR9boJgMEkhPgXCg1vm}yY<#bjjE^$i39GqWC}n-Z8Fhd5%z^8Bbr z1XM%0ik3jW+6V5HmWXqF2N%=NLkXW++K5Fee#+$ch;Tl7fWP$g^oy_MLd=UKKF2pw z$NYpLg1k>>ET31s+$YSaaCg3g3r{IUXm87l)NKuypq1Gvm;UJD&B)Dt`slEG_N;kx zVIOAP(_%g+dwIFe`~Bv8wwG^m@P*Ym9K9I$dA@fypWxNliiiR<^dYJSo}g?fZmO?& zyfjFY(|hyVBjM3$Gjs9}@#$EzEcMD7npFS%aMCWL+LTiLq8{>y%UbURT;8w5F~+DH zZPyZspdk95JS;FQFxLKG+YlaPUJ0R(xnH)vq@SrUH42`p`6d|9+s=NRB6@Z&ZPi&v z?2^Bh{8Yzx*Wm{7CR66a_4XeFY#q);DR%-f3WlIIiFD zhX?B}0o|4H%H$u8n=GaI(VNAsFAwD3&`y>c-aX@0h-$!Je0mlvWPak2F1_FwdnH%i zqDGcJpU>xhSJ3?l;lnWHBV9>Rte=8B3Rg_B0ZE{0Mi>_(4eA8!^%&{1+feu|y1 z$2lkI9vNM~1)lg!TcX|he2?hV=uJ(zyiy_*6raLD05=68@eT4k%#!#%HvhMmvPQII)y$=~fWhz$IE&KPEQ zCLL`0p< z7Lcd%*z1i<7GfR7ZEZdA5#=Q~NxiN)l(qGs`*kwsD2gU+o|?yONxc@##a~(*;K%!f z^BnJfZ6iR#NNS~5??4P-Xqv`-Pw&AE|DDG<^MLM1QPpY2b%PT5y>H%`@h z@Pi5siSU`DXEDo7-X7@Wc>zj(yW-o}de>XFo-^Ar&&Xmg^KaPdW;+!!|9K_DID5u6 zG#wcHN_Wkem9Oj_FRr0n;~x<~pblmh0e@XAsPKC^i+UWSPx3$hnny}c?lHSFmLmi$ zf{G(-i|-GYm*p4jQ%Rw^c;HO<*JGibzPRM{bBya(3F-VTzXslOkWMlShuX%ydZqYf z-qzpe=QIGqXh3@BT^Tp-9|0Rq5_DfP6|jJ6TkU-FnBHSr0Z#uT10MA>y5|>bWrJ2B zHQ@Z7ua`>%*J*_*g|2~vU~02ir9X9B+A?G9#(%I>MtQ@F04Qi|G{u1x{yg=NOBpMaDxoPht{L^Id zF0&;Fo%@e2!gg(q?80g6gV22;$pTM#sL5rH*QlK7PZKqd0eZUH5A+jfn^R!#cn@NO zO$J`?Jga)Arl$64BU#FgOLnJEc(?K5EC$pP=9I30Q6i%DojPga+Rly+-Nxrfa4kJ^4S1rC$UkT?f%!CE#hZ>A zRm{f$|EX$ia9 z)tuB7Py^_7TJ2ss?70BqcAnXmh&4EQjru!Wxo7(kki}+$tlX}$1E9q|DoZr;4rB0M zVNMZ#L?pZ2#R|F&qesIfBD&1O!^06NC%LI*Z0|a!>w~O>GBm&&(5<=vD*Hx&`?)S{ zX~%48iv?XGB4Vz?K}WvT2K3>>+Unb<^`D&%=LSHL=-EU+2m5=bZt+zp`J08*bN%@j zAl~KGk05a(VmdXr@NM->)8ri-NH3C$&c`H4imvd`D?)Lbn{!DV7kZCsor3pkc=I-6K( zyzOFHevxt&2*h6T4emxvt>HtXENE4$#ewl<>u(499;ApSW68BkV1w6$ ziho~oBM48KU2gHDl;!WJ-RhuSqJhlp2koGbZpbX?y7b_Yj--2Y@19 zGRJPZduf;gstm!xXQbx0UaUR@g;V}Ie6XO9tAFM`sgoWFDVkMv-ILq=h6mQA_}_$w zJy;D-Hb4Ms{EuazSa8;1nH3zWX)6*zV5n)Ful(>ne4z}NEvXxBPVKKDjV;r4RqTsf zPVm&j*$Dj4Nub9VvGaLj)E7Ejiz}K~9_UW#Ty8C!DRWv-sh*2jZa9*I0Hyq1#@j5r zb8LUdkk>pN7@sw~JY*Z5#N0a>%hOS6xByXM+hmI8hCs2sgzuI9V7V7Z(q_|Ax*;x_ zU%d__s4V6CJtg;8^jVkBc)2rpDD}Kyx>zZM$hm7~GLf3vhHH7pKI9)=_2#LTFhe$#m(SSkmN{F(@G2`bb0c^65s z(sk#KB`lmw>&{>UNY&x6V#7VioK$D}Vd$fi&n=%Y_J^t=T<`>d3digTWa6heLG+jmmo`@`MF0^Zf2OW=ioQrz(T5-TO~gH`B*o@ebo#YAhZanIz$^RK4f z{(Vcm949-U7b7E1*sV{q)z!>fR-b|D-TyvFjx!bebzw#|W0s8zYn)q{@NM0b2|uCZ zYf#SO4sThz39Q^yqEf`$qUaB*i`@R-1L!!Lqk!Q3S0Of$Rez%1GSX`*xM?;zMcwXK z{2Y$G?Y{9gazeO^B7&;@LFR0}kaOR6u6*?W+Odwa#ik?`-?{U>^D6o8XzwRgBRWSJ zC&yD?+3pl*H@UDWxt~AX8hW2;^tmx#==j6ygS-00;E3>VJZp^t>>(>vE?=IdnBG(j zr`ZomyRGm&9J^}A!+usJ`tZ=cWZ|0k*~;wOlwc_HuvO6sZc$f)&}Ud}Qh~N%xzqMPGAg&5W8khyW%B9g%~+IVhyS9+PrDi!B#g?Lp^ZC#iAA&iU`-SGAALfO(e$4n_JjHB3Fh6QgaLrj+ViLy?56Ca{bp8S+`%B zevk#IeVfnmck3I4oY(Y!9oF|{I%r5gQO|0OVKH?7_(O>pL-XH^+Hrk(E|9FJPN z$20&_C84t|^%ah4MP0 zG`5~#);`;D*sVVna&bP~agzKk?o-+`q?&tF8;=W}Q>h&N-6E3xJ*nOj(KBIYV!X^QR1wGotR3<)5U8t{~7MLchR6 zV6u4E+D;}*Ki^D)Iab>HjJ(T8>sIF-FYu34CmS5ZQez2PFs@E@bP-Ill|H}KPl@%0a zyMNHBJUtNA7xqj;+w8nnV9Mr9=gyp8=>A^1YSr1er7GFzU_UTEo<>0-BKh+Jp8B1y z3-%zheWvHWJbeCpXac&4KOvo_mIprJIxmCh6p#GnAXRPc^+})K6M98b6nEaKT$MMv z5R-S9HIJ+G7?dxPeb&`C&{K5BB)FtEH1tqwCjD$DpUf~c-qac#545CRKurx8D zQTx}fb)cR(8%w;2{%LJsV4B-{^??+<(_$9K$gXn49_l3vhw`glO1?kJE4Z=NC!?2J zH$zo$I*e{@xpIKMrGk(YsgKDWKb~cE0xyj5f{22_uUTT|h7)l36O-eA~G{r!f5a|u@PH=|QM*tjn8W+MR(Lurc z23(uJZvlay|MQmrX_x<_I)gu&LZF>0bX_quoLZnQr&rbZMhy|}-rs)SbPIvPlpdsF zAnkoQ;qoi+>eGbh2#q)RN=IE04AB2*;552lZNdkRnODya8ZX#GS``>#LKKyhRwwO> z-qSv<@&_TVWR9KU?rR2*C(Aj%!?APrA3l75jdMC1Gxgo8uIZoaK}aRr=cnIOp4P65 zHPVf3FZJ32Strbb*MOaJ*l+H~aQ({FvO&3b5qveF44!j{nx83l-y7WQ(=7Rr~wr6>;4iBG!$QeB*DtKdZz)XOFVDZcMUF^=t0we;G6}Z zmDPlI-Ea6p!@@YfJ?cly#osf_0@1r)fLc-==pe;_V5mnZnqFE(CfKQ$w{i%iOoTw% zT!wX5|31k9F6~zkuz1SVfZew(D174zlqeYmGHN$(X7=*cMuPBT9;~J~PQ4XydJq9s zGpilk-7D6=cf|=$-=6CS|9y+eeL#Jkgj}K4mmbs zQ+Gj4v>CiRp@_kq9m}@9J`GqqNJm%&u&vK1Ou&_C9T(hUBq9d0>6F1MVu+Yq&CN() zUINYi4lbdCbDhC-jx++!f<>TL9c1xg3HGVA`#tA8&-Falxy~QwoJZHyKQ?RcwXDzj-0%DKe&6p(MtlUSg;Mz+OS+vc zvhTm)3rV=o#--dHgKEqKfCD@0f)Q~8%V@401JIe<|~>0lT}YYwU7$MtV}P+UTS zGEgjAsi8{#H0kOfM2*o_ll&yqRqSBQtO}H=$P;B6c9YO~%ckR!(KX5PSrD4mTwOh4 z0l(cikKD2i&Usg^uHl523UzaUK@qP%K#{~i$XQ5bPxk0RpJ0@J8i74Fop=B)Zq~9E`>}_b zmAk)A$pJYV<$KJ+1XCj8Ad{k149|sPXBVy{>xzN$y}-}|I%E|&wWc5b6k*lFnq;UZ zlikqJ(AwiioVH2L7~3&Y=%62fzEfn1VA{($7DT#obsL)Q_i^tO9VBDI;pF|9hHFncD-Px&EmDN(Ar$X_>G_?XlYs{ z2E&B%w2TDf3h)e!1CCu;xfx&gzW&B$kYg37dj!~}qQu-29SqQd)TtrzE+OxpW8el& zXC+5M^oO^(Ae!4m>8$&f&ClUS9xpEz!a~l)0kmY$)*;;IM@fRM9sG|s>#)@2CcGc) z&2BFr#uy(Te>?s(r5FtZ!{8sVzN z2Y`_+8W*yoJC8dss2k=l#zA8qkD#tlJbEjhfk6g@=3Aqrpe4zH&lfma%)WEgbVEY{ zhB}C1(TukS0PgrEuTXf@nkEVS7#@D1Hg$-RDl4d+u zaW|5Q=}g?^S=zLIR`nD&r1d&R<+YP;WNBO!Fp06Kd}Bu->_)( zV#bf0RXZ=Kf|O;wSfV~B8hY2-5WSQlJLzECo}R(di~7dE-~_aX67(<5z8JRV;oUEr^dAnKN)NSPV zhIj?{p4wR|JuM>Z{+{A$the~+dP4jMPGKIEPZXuD!4#~sJ{R=P%lrGUT$H9}N7QKe z^-#hatxVKF`oXPh^{kw4Dj(%ASig9eeoS~rpz^avucC1=1)Y4?_ou7b{J#a9ieVyH#b!eWNhN5L!hg%30Y5;vczWd=ZLdBTj$69Yp`wtY#3RR&C@J#l+9kW4JgM&K z40|eqw6`0N%gSUfIqOD|uSIGatrQ>H${JoIz*dK7%l-aM77s@0-?zjrJ<+VCJawQw zS6js-k&$_+grGN3wZ?6W#;U3!#Z_$2*;d?A9rJbK!b`r)!X*`mH}~WSH8|f$6!BNw zTJH3Q#MawtZt)A1`_~7#D@MMYMyhvExu{g5@XgA$Bu}8_XW;zc%ljP}_w@Ur z;1|LnW*1AGEJOJ^Z+Ff?g~z-qm~@i`S|-|_o?;=KpHkMv`R#hu+%eO>6B*RaAGWq5 z8-AsJ9HoIOOX^eMGhKKr%Gh`3wmoy6S2(NHT{%pu#lGu0iC*SpiJ{|4glf1UXv#HYa}3xF9_vVVaYN$#U{OG*%4 zpKA9=n^zdCN%!B3h*|1QmsU(IrJ=V-Um?L7Y{mSf`<1KxveomTQD=yz8MTt zMR^Umklq5!NTKVr`m{qlTQ2&(Q$9NEE0`K$gCDB}2NexrH%w42lXn2g?_x_i<>sw+ zFZ)ZzeE*f1=y7^}?<67r(14_DhECE+mZ#~JZ4ZgCJw3W_jEeXH=N`!p`1kGsJkV9X zusBt^j1Xb>W{B_KucSZR+rw4vqrkcQ_ZW-~!GlpSHb{1Np1fNU&3WmC*X;)^Y1D&s$jyq+IKq9pyijRP9ZwtHYl6+ zs$lo!9`MVioDEPs7c+^~%Ic6O?>N3%Qc|yyr+69iuEBzJtMsB>iSvyi>XHfRN^VA1nR>*&Qnh7-Y znLcj+NIojfKcEl6Pkw=uGeJ{36Zkc`6ew)-|7@QkON54A#E60KDMfeXD88EE9p*xtFSQL3I_MNg$w~f?05=h48?(`W0M! zKh>GeC7`B^-r+d_x=`B}qQ!K{YtA!l92{w8a+;+0UD%!uDMy8W@q*tnBEE{&bWYn{$l`2tvI zAa(N45_q$iuY=SgfT+Rj=QFJ$cNg*Ar?ApJYisUO{(GgY3}e-k9osPS#4hVY-+q@E zTKq2U@$@5^+gT>9ie`C=!skU7Eo8R zU8mcut)|zBO~f=w;kd3)1Uvbdb|5?!8z3gW0|%A*STkU{koFdUoO#E(%pE9M#9jc+ ztIdNT@Z=v5g8uS`7d7`k8$V)XL~UF(fW6Y9S_%O3vbQNzKWFdU9Cfaz+~$V9T~>Bkf7A<^3lg|1t1d?Q zIqLg41yKIE@U&DP$8RjsyL5jRQ=`md{|5_DICdv-Xxoj9_auZ?HV3n-;NJ##1+ta^ zYX{7Xe5%~oZOjOTFhL5iwoAoAA`9eJMHUwQcP>r9chB+Kqq@93j#{=7^p=BTv z&~@$_4+4MGosT9QPG=|~3^%fh8j7{SClbOgK5lm4r~c45T7LX|wof#5j*R5Nloh3^ zJ*W--GAMYG-xMdHxYx6Vp02IeFpa-k-^9l0^@0`JqQXdfF2or?&RI^^5zYmrs{wN_ zlcw|_nTAe-V?!WP*0m~iW-1bRkBU33R)SEe6k}Jnz}57coNQmW{q~k`b9x+8MN4z| zgo(+u`O`cdI>3~-#Xtb>PE-=^B>gF{4zLM88JQoisgER1^IeoIlf%Y72R3)H7CJ+5 z0$2SAjj$&xLnoYAK*+&A5hYam5XEC@P1E7Sw8K3$&wQCv@DZs#0Ef=XwPb@aH|q}T z4pv4qv0T~}d0;bMYvHzFsQAwAzjeF+%4z`wKm-3#5Jw5~R;~)1X}?y7H@Ci4!#qlv zU)3&$SzwLQo{4zpw*2-~{6*fIEM_ljGHEMS1N%-m4_6{xfNr`XSc#2mpWbE0D=HjR zfPvR-w1ibZ()zdxfj&pVG*aqFC4vcoa0qs*vCY{LX94r!iR{0+%r~hC-*jzzM$DqG zLPf`~FP8xB0BMaWamb5_6C) zM1@yy->rKwT~!DnYM5jfVDY8qY+z39c+o;^zy}(VVJD~svf1d zxKuYprMZXy3nuWtjThWBRQnQ3m6a})HM-UG>h5!+Mgs2&FYTrU<~u)rM0A#p80)FV zlo_iqfIT9;HVM2(Oa^;I0O7vbm9VrJ){dq0lHynE?>V76PmSn&aJ+xJqWddvw*IfY zH&Om?qTl!cdiP2O>(Sne{KeS~V{VdACkjV2rwXNS-7EccqX07JnWcfMXx8QBL5t?= zYdc@6Rf;GPH5_Rt+wOy^FI^io#De_Bd~LoVVD>s%5Y=e*JQorGFSAx~zH1>_u8{G$-$QLej$wtApezag` z9l5Y4JMrUkOc+I(0t458a&+2Su&|W{5vqv&2z91G{RXa+JD3`NZB9|H34GtH#6lT- zBG=z9u69!XD_Fn^sX}|tBQ758`*@Ly^t`E+mN7rh-Y+gs;i}j`sulKWMi(t#?nrwh zJ7GxtWT{F?l0_qRmbA|)pKB*vTXv5R3yo>sN`T9_nzM-a=kXdBQ-mMRg^MaG@n!gt zQaA;OFi$*Gun*)mFE>f}=t*gnd+YiubXDLM#-wA1GVSffwJ-M$9MAk+-Xs%!J+XW1 z&WX?T24pR2O%XHAku+Tj_Yu47-1c-TDE;I!QU~^5mVFz76VYzpvbQU|r_g=h?{ydd zv^h_JrLyXQeNQ#2frP;)q{2kn-zUtJYmfxa+DLNIeET7Fu|a1ge~#|_@8T~~GL|m+oj@eb^b3KO4M_>Vj*acPm+LB^NdR9aJD#H-P;vU$%r+2j* z-N@cjCn+bY#z;*(Xpv;m;kE9LO%SMZC5vMVxb{iIx-mOkyI!qoHp!<`n^(?3x<{Mm zsAeH<2)^(0uwF81XwmNNUA$Ca*AJdx)MXtR15{&ke1%naYfQjotgHX%K+5~~(tNx& zuAg-19%W}Y4_^Fxf7n)96BtOyB9W51NPlX;SjM*4(ElV^Yp*8bC!!J(L{9{?|YUf1S=uOHc#0cvOj!%@2g-E+ZJN@1#d}Vh?$O7=!@T;RPbO(6%;Z2HSc zZb12>zH74zI4ZUbo;1uu$I9iV?l|vPQ_pei86dI!YZS8xoNRM@KhU?{L(o2AffUD66QNC7sNb`#G`LdNZ zf$1F3$$Pmm4V?!-Hwa+3%^Ktq6fZT0@hSVu;b0>6RIKsT~d5JqCt zmcX|LPINb*4|u`XVJXw6P&r0HO)Z}#ONu>0^TEa#7%3>Or^($~tZ&Y@ z?d6C0fY%0jrex4eLIVrD!lIC4#OibqJp0+QDe5^eYqZ69f>tvq{grLIUq#DkP?2KJ zcC7AJUhWtu)tT-{6t^S79)c+oQ+q2NBzg}aE$4vLJkXr?^+$pnuN>A8iN10|0qCt^ zfhtJ~JUZepNFx3idvI_tEktl2eu@&_zCnQ}$P+}N7q4Emb@+CqNPaMhZB~K>BH)pT zYKrAZ3wR}i#+w`Ent?%ul_AjIqC`_l(%J8=6Xg& zMP-@;p0CR*A`*YFns%rK@CH_X;VaM>r_Z96_iUQlaZp#d>AwOp6EL|5R@cw)g#lUQ zF+7kW3lb_F3p(L<9H98()j$eyCBn9ktskrWP74~wQUB-{69+yd!NOog*%G+&KR6hv zb5}DYQYV*sUh5pt*MMo9niWwoedO*7-?c;U2Sq|)5QR<|304h(&i+`M3p(ja$^dkj zsyt*cFi`-y5AUUbS|~0tQ3c2+36bO=!R3x2@IIVvq=KK5NSbVzhrtA=z-eKrMWB9} zoKBv>+xm~7X_0Bst7+bx>}HfTO0z?)tNL3PQB`l_nDEPmf%W6O4_||$;kG+H4J?I{ z30wMM3}Lj{VWyoR*EtBH$*yj+VLH0C5{$-75XduURNjSpRSdiL-STQ}KYSbA8MR%$ zm8lln#_6>PhPslRWMovWM8`2vfeRgf0480x4FmMYryQ7Ermu&pwhPTf3FAM;l1=nxqrIcz@CB; z1>p|}!G9xEzQ5aKp9uh78UUo;k-^)VN9z(6rA_eTHHQUTGIcda&FViJYJ%XE6yIqf zdSnLK(F?oyu~0ge1$242BH#-FA#&lDl>YZi{`j!j-=#N9h0gIce z30ZKXx;rb}@~BbmPaG4blzhgtGc1V#YKmOqpv!BU-pt?kx&vtQ0+rUIH6vZa{59{J zShNE}UK4SIpCRTDTW;Ht_K*hZNb5YM2FE?5pF8Hx5PhggOWJjPZ(;ZY#@w?AghBj; zia-P}86@~Uvu~R7ByGvPC=40f=K)YWJ{f-608m@S{Iw0QCgIJ&nTceUHuXuu+-IQK zxe=Z&dvtuQ6znC+nn3h)e!`-cL&}1PC8-|N*5JdrgBX&H1qaWB|i5eE+!*r1TuY1}j zHm7KXmwVHBU3^n{zr0osC*N_sASxWwcqZn|QO*G9Yrmbay7TzemhDMqs`|_8rLruy zV&W2vu3VY3`n3rm(%<@7*c@?5^2c6KUd?tak7B&@SWvmSPtiR{P}%xRO=s_;xrvZ3 zRJRkj>J%xSs7BD*ziRlbF~ZS88uB;KjfzJNbOkacdoQw2e5$IDsBq9LHL4$Xmz#D38dTM<9&V98wZZ1X4{tT!SFBJ`R_LdG$wYG7IB%8sNqK5pe>;ATN z%^awch{>jg`4kML~K-|w_B@s%8FhJu_MxZ?i{V0sBIdF^UmgkIFY=Hd#8pQ zX>UCX(ABVhBvSSB0WdiPDGHV5M-+HESZhT;ot{kJcc=H>-OwHx8J;M@nMixGdMzCa zeE-zShmOz4YfNaRh#h>N@v|;Odaozy216uZ7KM(OMN~i2Www+qo#Vf#8P!~e<)8U$ zXZ&W${Mhrmpx7cEgZ5b z9D{c;Hnf*nda5JuJ?2)n>T?a5i0WZ*A6E$oDJgqrWYeyHdxF$xz-2_w;%P#`g%DTq zgIT%v%W6v3m?SiqG4~{*?zyZo2AJc>|5gs73FgB0o!Ue`(`E!Xb@oct)rr&%dP$r$ zEs9PL;(2w7#UoYU>c{k#@Wb4!h29+3VYS#6K7t3--y(#&bA&FNX2ugEP+4L}x<xI3Yv&PqNZLc>38?MdG7t0I91q|N9fzvj7%GKqDc5;JuC zWrXgvE=hIKK<>PmRPc=hJKRabSf8t@7O&QVM|0rufJR*nEu?ruoPQCH5hL$b2 zj3N7-C_!pHj(2ru-D|}A!|w&bA1C+1NwB23)_R|< zEF73x2H5-8V?q%FCZaiHhzloB&7;P*_doMz)prZu9XaN^9~c6SQR^j;!}ntW&{O=9 znW;#HxpIDzQA@LWAJ&&Wzn-kuJ9Jz(3k92c61E4bSBIE!!3`4oi0)r=S{~!ak{Rgz zi~wl%Mn#()ex!aT*aZagv)V$9J={oxVZpa0?O@!ksqCBDZUS1*)DfNUE!`KQ4S2m) z&sLeNG8w$?TA8s)u^4;N~WFMKy0a?AHGA=<>(HvJ(KV5r& zwriHY+I*ScYyhx0k?b2GV6S5yjIy;jEK#O*wg%?44c*yqO7C_$TU(#Qo8_+!7VkkN z_Z6mW?c2-$O{bghIL*s@I7)Yf*)+hVvq2vb4$YnDoC7{{ncUBYIdU130;64yA)1~nOT^hGq&)odMV%4tW0HAUW38AG5n=f3a zB%IS%AoIY4LN;Oqi@4*bzRGUl>b;EN-a!gkcIxYo&j&h|O*7gKmlu_Q@V-$!gIg*9 zdY0yf&=)WA?zcWz+4mNDBd|!BKRBrVXJ<&_eD>(ajCjnYY>kh@U$|BK_=fI3^sEeI zgwPEWhX+fCyqYpXN!8V$YINul^h+EX0dayaVK5vZ=~vBA7kufNpsinOjAyhLHIo}H z?|b&?1;nyP6}!)q=$00_`6y=zU6?)t;cehyd9&}E*)u_D z(H%t0V^B%Db5{*&2{1)nZn?VL*%{Dc%>AcZ{wvAmp+d@bQG}2Eee~DSCy|G_wAc%l zOCI^`KP{<;Y_C?B0O$uHlC)~0pK~6oLG1KZADoF@1uf?@?^dgJ7c;@+!uI0j3;49dqZYZ& z1&n>=GMOrzRAAhpAM4?4(g8wW)!~90Zh5}ac%~lDqbcM{f$|rUK1c_Xw_3=kM;XN} zJ5)vvPW^cSoRJr9CvC-6Xe5%yw;E1IA)x-{6@qHe#ctP#Dgjt+i$;|6V<``fj#Kmu zkZROPPHCCNIH8YgHwG%a@=W49L2J0%*eTotXE7;adH@zUQ0%tE#40si>N8OS3XO#9 zas!V;#elB zyAi$kJyX+$mgyD!hnvpQWho$OyZS>4JbSaK&r~3osB>nuNuM*7{h?f@t%*q zUO&6Ds6keT{Agw=ANFBSy(d7!9~?V)2#QIYlVbKKfvsFW^l2T~lHJ&R?k=@fh`!-` z*~VuNp!Fa3FDd^)gMbXabITlF=!H*Zcj%>*e*AF$%@zQ4K=-9OLw{W`DRo=STeE8a zZ8n2(0Lse>OHCG-%MlhAPfgvCJni(k-3`}}NdU*Tdo1v#Nu4VJ&E!Y?5u`LOGgd|Q zMo}%#k+uB`e}IF$^0CLccyW`iP21_cLeGl@XT=@B1k$wPR!BCMF-M1?$Dzi z1ThD?G3c9V20lLJdzBJH;A&pGVBv~iR=a%MtaM^VkYahG4|K=>wypzR0GLKv3kHH% z(!Q+buLH$sD)tyD7GyOf!nqA_MhCcWihOp|rX4hxrbBdQzd zd`d7@Fy^~hhJ$kty`NZ&M@!2so|Zg)b5NvHhMSPsD+4%j;^m76HbK6t7D%IrNZ6c~ zm6@nN=#+K|I;oK*;JBzr1hE{jWvIhX_W@${i^N(zR#=&oN{2x)?^lMp&|_KO;uPEg zkomF!oUz?ppM5;55sl>&)9B?F(i8Z(HXOWe5pQ{9C z<$7v34u_jLWJuFnt&}=si@l83H`%3lWbky;IiI(*2|GW-8it(^D> zI`g;|X2W!d4BPw2t(T68i3gYvPG^pJ7U%o{1EjM4ShlDq`-k}udyC+VA<@kqGD!H* zWZ8;aG(;~~FXTvs#l6nuoX7Dt>cD(oD^?Ir!Ga{{LTkWgq_*%e?8_& zZK(1Sg2<$D(7xtry%1e){fK{F%amI#+1{^p>pg&9}~XI=gLSu_pwS1 zY}QHi$mjqtWlc}W$x%6`F+inNK#vqU^pjDqTQ{_WwkQZd&ZPAo?8C@p!<<3ndGKD5 zRmnxbvBi2|tmgMi&^IfrLa!a>=5*`wvwyPy)Rfa|UCwN37NBPLTq!RgVDYNNeDenQ z%uF8t44^H(SDgk)2zzqWYO7tc!l$Pg4l(3r0K+JqoZMc4y&JCHH&d8?EmwMIBe24+ zC$+w!QFp)H1hpreh0skSPSU!?Og20kv?%xm28j7r!WW z*{7!d+g4>?Q*oo-Cj-D-TGztBU`i)&!vh0|QmW#(k2l2>xHmeT=&F;XeN1_36atw< zU6V^Kg|End(}P&!7==t8FV(4HylOKT5k`Mf3;)W5@Gk1tge=u|My{iaWYU&brtLAI zwzmY#@P-h^5ZPJeM%twGWv?n@kxalHDZHr}ETz-kGbeZ{N-7@rk z<;gj-(L)fQ{spMzT)1`M;1Fb@S+POc+rO1znW-)jqe5cDIyM_;e9D5S+lh`93-j_` zPW4{(kCoxlZ%7+ZUt#wb@cKD4zS1w1M{LewI@@9Z0WE+Pvn3&^>(b9Ewl#1NG*5~) z!Up3!zIE>2v^xdXy1vHdb`bsQj{h0J{scW9!ZcL~<J^&h-Or^p4HT25#eNf2I6nfCXnl>ASiqpD{}T5+xmCs ztV~zkbWzG*TF5cUhn&&@C8bG9TDb#edd&N}EX0ketXH)3Xxd;&215A4SZyxt;j_Oo z6+Bn&VZOJ4tg-{Z)V9!aR110zDd%zQ8z+zuptiTzYGJKo<~_Dl9QBWoHM|iv;-gP| zW?0tZvu0(h#V*56ovZ4WLiYX!f!%L+PKqMxUop@@TFF&x_xr-EYWd zKcEN7Y?e?P?D8~^$KE`N=3(w&YF$%4HDS6*`%792y_?)hlXTqT7%M_YM&W|*uTyOx zzVA~C>%o5!eh3ud;I`MH>zubOP;O2Wl=9cS`^w$r$*b^?Y22gPh6<`_vr_l=J%7`#Y$`*uza1bjgq;X z%_Eso-}0-f$(AIKj?BUTBH4Y>MmJ(zj7*ua*t3N#@dMtO&D_t-EEVxVL1&v~F5M1~ z@Tn9e{O7hNJqn}(!v2Q2IgRJfKQ?CGO`gUD;>jr9+)8$m_5G=b3$pFuom872{W0@v zH*#fTaeJo7n)*q<;dWv~&UsH}TH3?b!GZwO-jHKnTP2sy2(Tg2?`WXmPaNnfnD6AQ zn2C%p*Kxiq>^f~~v}GPW7PqHWlSD7Y#RazDOnG4vjRJ$dHWvmHA~@GM4RMJwT+Pe!9p&}CYBuGVP^CNC~`qRRz-cA>Y?4VjNL zC4zzru4k=gkGrp|`^;JFH_+Bk?+jX=d~I>&&?kxe^h^C4H_Dw7=SFuA5sSAiKHoUF RH3)&PD=Hew?-b30{s%uERS*CG literal 0 HcmV?d00001 diff --git a/formal-models/README.md b/formal-models/README.md index 7f476875..ffddcc5b 100644 --- a/formal-models/README.md +++ b/formal-models/README.md @@ -356,6 +356,66 @@ configuration: * [TLA⁺ specification](./dbft2.1_centralizedCV/dbftCentralizedCV.tla) * [TLC Model Checker configuration](./dbft2.1_centralizedCV/dbftCentralizedCV___AllGoodModel.launch) +## dBFT 3.0 (MEV-resistant) models + +The [Neo X chain](https://docs.banelabs.org/) uses dBFT 2.0 algorithm as a consensus engine. As a part of +the Neo X anti-MEV feature implementation, the dBFT 2.0 extension was designed to +provide a single-block finality for the encrypted transactions (a.k.a. envelope +transactions). Compared to the dBFT 2.0, MEV-resistant dBFT algorithm includes an +additional `post-Commit` phase that is required to be passed through by the consensus +nodes before the block acceptance. This phase allows consensus nodes to exchange some +additional data related to the encrypted transactions and to the final state of the +accepting block using the new type of consensus messages. The improved protocol +based on the dBFT 2.0 with an additional phase will be referred below as dBFT 3.0. + +We've checked dBFT 3.0 model with the TLC Model Checker against the same +set of launch configurations that was used to reveal the liveness problems of the +[basic dBFT 2.0 model](#basic-dbft-20-model). The extended 3.0 model brings no extra +problems to the protocol, but it has been proved that this model has exactly the same +[liveness bug](https://github.com/neo-project/neo-modules/issues/792) that the +original dBFT 2.0 model has which is expected. + +### Basic dBFT 3.0 (MEV-resistant) model + +This specification is an extension of the +[basic dBFT 2.0 model](#basic-dbft-20-model). Compared to the base model, dBFT 3.0 +specification additionally includes: + +1. New message type `Ack` aimed to reflect the additional `Acknowledgement` protocol + message that should be sent by resource manager if at least `M` `Commit` + messages were collected by the node. +2. New resource manager state `ackSent` aimed to reflect the `post-Commit` phase of + the protocol, i.e. a consensus node state when it has sent the `Acknowledgement` + message but has not accepted the block yet. +3. New specification step `RMSendAck` describing the transition between `Commit` and + `post-Commit` phases of the protocol, or, which is the same, the transition from + `commitSent` to `ackSent` resource managers state. This step allows the resource + manager to send `Ack` message if at least `M` valid `Commit` messages are + collected. +4. Adjusted behaviour of `RMAcceptBlock` step: block acceptance is possible iff the + node has sent the `Acknowledgement` message and there are at least `M` `Ack` + messages collected by the node. +5. Adjusted behaviour of "faulty" resource managers: allow malicious nodes to send an + `Ack` message via `RMFaultySendAck` step. + +It should be noted that, in comparison with the dBFT 2.0 protocol where the node is +being locked in the `Commit` phase until the block acceptance, the extended dBFT 3.0 +does not allow to accept the block in the `Commit` phase. However, it allows the node +to move from `Commit` phase further to the `post-Commit` phase and locks the node at +this state until the block acceptance. No view change may be initiated or accepted by +a node entered the `post-Commit` phase. + +Here's the scheme of transitions between consensus node states for the dBFT 3.0 +algorithm: + +![Basic dBFT 3.0 (MEV-resistant) model transitions scheme](./.github/dbft3.0.png) + +Here you can find the specification file and the basic dBFT 3.0 TLC Model Checker +launch configuration for the four "honest" consensus nodes scenario: + +* [TLA⁺ specification](./dbft3.0/dbft.tla) +* [TLC Model Checker configuration](./dbft3.0/dbft___AllGoodModel.launch) + ## How to run/check the TLA⁺ specification ### Prerequirements diff --git a/formal-models/dbft3.0/dbft.tla b/formal-models/dbft3.0/dbft.tla new file mode 100644 index 00000000..50439c4f --- /dev/null +++ b/formal-models/dbft3.0/dbft.tla @@ -0,0 +1,430 @@ +-------------------------------- 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", "ackSent", "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", "Ack", "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 <<>> + +\* RMSendAck describes node r collecting enough Commit messages and sending +\* the Ack message. +RMSendAck(r) == + /\ rmState[r].type /= "bad" + /\ rmState[r].type /= "dead" + /\ rmState[r].type /= "ackSent" + /\ rmState[r].type /= "blockAccepted" + /\ PrepareRequestSentOrReceived(r) + /\ Cardinality({msg \in msgs : msg.type = "Commit" /\ msg.view = rmState[r].view}) >= M + /\ rmState' = [rmState EXCEPT ![r].type = "ackSent"] + /\ msgs' = msgs \cup {[type |-> "Ack", rm |-> r, view |-> rmState[r].view]} + /\ UNCHANGED <<>> + +\* RMAcceptBlock describes node r collecting enough Ack messages and accepting +\* the block. +RMAcceptBlock(r) == + /\ rmState[r].type = "ackSent" + /\ Cardinality({msg \in msgs : msg.type = "Ack" /\ 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 /= "ackSent" + /\ 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 <> + +\* RMFaultySendAck describes sending Ack message by the faulty node r. +RMFaultySendAck(r) == + /\ rmState[r].type = "bad" + /\ LET ack == [type |-> "Ack", 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) \/ RMSendAck(r) + \/ RMAcceptBlock(r) \/ RMSendChangeView(r) \/ RMReceiveChangeView(r) + \/ RMDie(r) \/ RMBeBad(r) + \/ RMFaultySendCV(r) \/ RMFaultyDoCV(r) \/ RMFaultySendCommit(r) \/ RMFaultySendAck(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/dbft3.0/dbft___AllGoodModel.launch b/formal-models/dbft3.0/dbft___AllGoodModel.launch new file mode 100644 index 00000000..52b9984e --- /dev/null +++ b/formal-models/dbft3.0/dbft___AllGoodModel.launch @@ -0,0 +1,42 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +