From e2318c8bb4605873d6bb50922c17ed88061e5ad3 Mon Sep 17 00:00:00 2001 From: clabby Date: Sat, 9 Sep 2023 18:04:32 -0400 Subject: [PATCH] =?UTF-8?q?=F0=9F=93=9D=20`Rule`=20Docs?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- README.md | 21 +++++++++++++++++- assets/rules.png | Bin 0 -> 57986 bytes crates/fault/README.md | 34 ++++++++++++++++++++++++++++++ crates/fault/src/solvers/alpha.rs | 20 ++++++++++++++++++ crates/primitives/src/lib.rs | 1 - crates/primitives/src/rule.rs | 7 +++++- 6 files changed, 80 insertions(+), 3 deletions(-) create mode 100644 assets/rules.png create mode 100644 crates/fault/README.md diff --git a/README.md b/README.md index eabbc67..d4cd7e2 100644 --- a/README.md +++ b/README.md @@ -4,6 +4,9 @@ A framework for building solvers for the [OP Stack][op-stack]'s dispute protocol. +> **Note** +> WIP + ## Overview * [`durin-primitives`](./crates/primitives) - Contains primitive types and traits used by other solvers within `durin` as well as agents utilizing the solvers. @@ -26,8 +29,24 @@ implementations of this primitive. The `durin` framework allows developers to cr implementation of a `Dispute Game` and use them within simulations, challenge agents, testing, and more. ## Creating a Solver +1. Create a new crate for your solver under the `crates` directory. +2. Add `durin-primitives` as a dependency to your crate. + 1. Implement the `DisputeGame` trait to model the state of your dispute. + 1. Implement the `DisputeSolver` trait on your solver struct. + 1. Create `Rule`s for your solver. + +### What's a `Rule`? + +A `Rule` is an isolated invariant check on a `DisputeGame`'s state that can be used to determine if a solver's suggested +state transitions hold the state's invariants. The `durin-primitives` trait exports the `Rule` type as well as the `chain_rules` +macro, which can be used to apply multiple rules on top of each other when asserting pre or post conditions for the game's +state transitions. + +As the solvers within `durin` are meant to be consumed by agents who act on their suggestions, it is critical that the +state invariants of the respective games are upheld. `Rule`s allow developers to easily check these invariants and +assert that their solver's suggestions are valid with respect to the state's invariants. -*todo* +![rules](./assets/rules.png) [op-stack]: https://github.com/ethereum-optimism/optimism diff --git a/assets/rules.png b/assets/rules.png new file mode 100644 index 0000000000000000000000000000000000000000..87d05ca60284de05a0fc9ccb4fcba39edd31c5a3 GIT binary patch literal 57986 zcmeFZX;_k57%q%vgH5(|+oWley3^9MoHC`k%&AnI70oH9G|edltTd}_TA5Rt)Gjqq zK~pd%uq<(=R762Vb09^;2@nuCukG`l^XEH1&vkv*^=*FWy5MEK>s{+v&$^%cejXlQ zv%S1+^WM!M5NMm_l?(PD&_jRix7G|rjr+6oK~cr_htK>XVR?K}_K^lx*^L6F?(qXYk)y@!!GtAE@{jBmLhy7@rw$1^If#2kn+D5!D__7pHwz!pU2kjSKdG za&CXiOBs754cd*7mNw6)DQs)zL&0kUYMPv{<9Hkgy-b2jCF%;z&R}y;1PFYGdVFY^ zxJ7o&ftf_go*9J|2%Vef)z#y0LWRT!B7(8!CK=AYhs1f}wzX~|9OV+5N((;iScT8s zlSw=uvBW^)_Wp*2X-%w+iH;I^DQG*HDG?lBWlCXdUrBtoAC%Oq3zLX1kEu7kwJMCZ zh+4bd=reiHST*dYw3?~jbbY0tnli?aj{o+g+w(v>Y^xmqS^YuU2uf>p2D7tu*Sa#f zBYVcAi?Euv4s>}IEH3@`;*7P60}&yh(MRHiz%^tJGO=E}&}+qR?LrmuZ$KQ8BbONQ zYA|K<=r6Ic%>K2@Qmp>NvHw5Eu_MO;JJ9-~gKaQ4Ene&mlA?)jNwL8AkM%>Xt=s&I3$nz1TunGRXVBwii05ZHKk#l)C@Zd(}tzj z9MzGf0{$joV{MSx4+5!%l&rvJN{XE_@3 zvb5Y;f!6A}#0P?A@M`nes$glY$HTvS)Ktpit$oynw33c0NW6jl@l+1zF(UQ7kYfcE z_5kA>0v?=`9Sllzu>AdKtB9 zcLAI?NHM&GS*l}UR7S*eu~^~whxhyZkNB24K2o)+Hv-lTCYK0!;m0o`eht+|WhZd( z^jj)(4NKi)?_m?qFY7+EQ(tM?_^_Ts5d9>pAy*gv{_G;@B+^kRNBQ>_f;PMDD9Lhh zppHtfdJO|1dM@WA@78hIV)6OKWIwyp3t#8IpI0cCNX8V9ag<`BI9N&N&UJZuVDG!7&H}l@SGx9z>Z9=w|pVESr}Md z)TNZyjMSl5tw33<)6<#mxc5OSs~UaQh0x@@c$>Kpcfrc&1BLB@aQXKM zuiyKgLr$1F@%MI+Qrt10Hu4L9FnwO{UO?7+)uqRF2{*XH*4?d)?1~B2woi-`V*^~FAI)aDn=!ymC@ zUB-;lz_2^s{~osfM`sVqxaa=*4*Pb>XDaR>NW~nK`6bzBfhc$kmwzI#yX;Hx6@Q-* z=z$xuEqS-*Bk_8CE|48?PIZ}<~WWXE+&L6JfMay4Mi=TMjR(PXySpLtN zZL&(As`=iYIXRX61VouQzU#b#`AOPFL&;Q&wU-0`FKkESFTRsCqp;j?P6>fi&W;Zg zhN3@yq}?W)^UFr+%T;UUE_dho7CsdZw8!`K=W9`)^Cw(qM4BWkB1Waz6wxxT>wAC` zh8%li5neQL;ys&KDavFTut&IF;gL3#ZA;q#3wQl(;eXI(URj4aXIi=IzqDKk%a(b) zS$b7-i1g)23Dq_k$z4h^$DxJ^leFIcl4ozjNVQQ+FNep@idVxTyW~$tHqvL#zn44I ztmatH{PO%ty>Vl4Ibn0zz6=NEkv&-W{*2r6mFe(Mb|dXhXWvTRDX(*H>o5sPR!$a#}2<6jeh?ih9lt`2hQ#@hMbWvvY*U&yySLHKlmKnbG_U8 zUAPNA$)F$ym5Re}%u)-5_TMOanJyF?T&LfcVUpyS#2VZh(#JT(;u)~o|>g4X} zyt;yAXj<-4C>lG|iQ+Sm(g^-=EN4hdxu9Ccisty){n!r|Hl|{BcCbnXg2aIEZo>s3A^DA$E7clX#jm$#qmCItpZ7`oWq$}#T`mH<7(G)Ny}E+ii}bv}pLe8$Mr zt9skBe~85p!&h+i(l6-y*np$Xqbl1u8lg z51kt<5@#_BClX?Zqp9DJ&d+l2T5q0iE{k#9TumED?@}eU__xKkcxAJ~NnHa2tn*#V zVQlUm!<_~#ifBl^Fz^5q4XWTdsIsVpQ?=&Q0fW!#g4WBr@kpToGg#-Sh@6sNFV=YE z7>W0})t!edhDX~#{(yhixGMuP`PYN0!osfn(3QFh{m<067FB3VixB;`1z2~@O5Xh5 zUQT^h492}ZT!oGBm)~DR`%zN~hb~+FY0Ey8MX>z7{39K4hs(rA4kg`jfME;ov(&}! zkky+nDpqtJ3(P@r$C!QQUAUU@VxlBk*f?60^)Qs)t0zC`Wk&$lq~Bnt?20GXH8N<_ z@PF9U5{pvvNqa%Is4-;4nY33WPuVuxqj`YUB8zuw38(Yp!$d+S0s|4VEDFFAuRP;u z`Kh0PyjF#q45T16sCl=)t5u0rS=gu3weyo_VZ^x3SC z_-=g`t+u3gz5;vlwSn=Ju)QOi(gbg%g14}lT?2Zc39bXB?T2LX9C0-mo3-y48@CJx z*JzCms3if1n?)9AJpj~j7W2Ee)My_r`L2<9I`1g!lco0ye_3~2=g%CAUwc9V*;Hk^ zoL!V~eEHs}qq}ye^$u6+OI8>%YjTUyjlP0N(MZj4^wrY)RYOaa6*yXt-t9pzmM*`# zQDWn_6%X6b>p05$Y@>b!&({GniWKkYCXQ&N+R%d^w^!>ZXV;SUbkxf|VX4MkbWd?$RtA}xf0Q5npS)t_$=`);>DB?UZ6qdj{g=*;hMNi`&l zVx#^BM|&*X+|-{8$+ON$KX%=;#_^{nsgy@fHl@c2CbRVfv03CH$gztqqDL3crKTfS z$9G9RVU-$j1A%88eO%WE)TYS0(Dbi~c(@J?y!aE#eE5?3-omG08iRFDDELOUBqDDB zU(R|z95x9(R_sQ-_SR{RTeq1y{)UaRAqBwnL=u~UJeVUaKr{aqQvPlEJWEszb`ot3 z`$w8^r7%>M#`BuY-WR-wo}fFa!(ZOtQ7sFq*eZKw4Mfjm+jl0#W!)dTpgE)P&aGU5 zzWoMNW|WZTpx9K%QIt)C9HmH-aVCQW{%fiwQXvT<1gV$ zI#tZP%(s|24VPAzD9n_iqv&KHNX+^zA*s46S6t8>GM3**n>0M3Z?UT>RB=bc%Fn;E zS7DfKd9xZ+jufu||0{QVjx``wiEdHwX!C>x|hmV1t!@sD@-eC$u+WSl0FG03JSHDm?vxC$MrC znTzfU;)zr*tmh)mb3?VKB&w|E1Rr01vQaow%8$WD4W(jZQYlfcRENwuQc!{nDB_M> zB7li2Us}!@eXxw~sng&EKmPtIf@~ijmBGlHRUWWi4D5mHj&_7Fvl7a#R(`aaKdBiO z{NSP7pD8$1pYDt^$F1JtVXw-!xVy_g)4q0V7T>A+`GG%I6(F{&pO|D7pweUr)d^B2G1~iFhUt6%}ztu9}r!N_zBsOf(OSy`)LY ztRZ(Yt>^h?AvzS(a=2}04fXY#8*_D0p7Qc)3G<&R+!|~baY-y^5e1KWHvh44j#d@= zns6+P0&ThEUW=P6z-Jcb9UV3)+%~7USnXqfA5}7rKX45a)YaD5-jlZn95o)|ZtBE~ z?_8iKVzUWhSbql0cFqC9%B-#2;ra#N3Gv0Fz|%FnrIPzK`taltk2p87|1gV(iw_?z zJ&kgR*;XY3a#54n51igdahb97q?7Cm@cU0AhK+>kV*)gEhrimi%nbYvrNNPcH;nm>szQ!u9cJ^y2-)mHPN5v@R4OhQdKY$ zwYeh_ORuc&DoD;g53}nHpKkWzvWtA*?u(*?`(wZc{dAZ)*8`9GBO2@O`sC9b#Jt8= z2s45F*z~{9XN-Z&i0zB;s!*?bsB`DB${cxdgD&Ju?lmmB{8du;ta7=Bq;_a)iQ-q6QC?e=7*Glpl{Nf!Br z)=8m#+#2QQwHpP&>u}XI3RaN?YeAwRsZ$)JbDUK$WiesyOD*85R&PE*QZF5Kj~zN% zntS{M?~N6hDuG=;;6NW4N`X5)<%xD{-f3q<*|^>?>}V(=(^zJ=U^~++cjpIp2FD63 zvy#gLKXT|EQSKMbG_lh<$3^IIucuU@|NT0usgwF&JhG#T>Qrs$Izdu)ZHtFPK}RKw zlBNZm$?CtCcXk;9qubu75k*r7FkcynnJIXuQKof2Bbw^jd`h`!GC%B_8?rkIEGm=e z$Xi5~L)JTvjXS#cj94^Wf!3V8(Ru7guJ=LF3AO5S|68V=%Y%*#2obOBB#uOtCn58O zdZQ!7@+zX^LBnF3m5j>l{lz0@HL5pCOeA$mUkde4xE6D*Oz<0HoNpx?|(rH;4zNUH*9x( zf!&7qm^9}2%~P|TTwrcicM_^OyhMnJZ;LjtL_L;NR=mBR*u3?cqUzz7S5&6Hy!W6w zR=i?$=_}fH?K^a@Ra2(b!(Hi&rrd1llG`*k>0l7mqtM4ImI3FNpL>U(dlE`;H9 zY#nWbexB}gSBQ5M73IsMQ6a@_ZFtrKis_FgM?S5kvV>9-OEV>>Dbsv6FC#dLMXL^H zdDW1=7E#(Djk$R1_0L%?0kpi3S1NkZ*ckaqV8dlm;mrFoCa={H98i;g1fRJvXYtp& z^zEvcBsW7D)MK9YhiuxGV@j;tP-x9WAluG4vg}m@_Q{t7NJK>6m?h>N=1B14-Z0vA zQY#8#8Sg^v;UOnfDN~;5&XmxN=Ka?{1XE_19Y02RYVWt1N{vKjYR-laS@8`+zHf=t z`qK_1pN9Oyu|u~>z{Y>|VND@i!PuN5+V~%oMB24DS47mNSC+teQXf@L#l93V&DISS zHuK4|*J2JQ76W9&lJGaV3j(=pU9+yW*Z(VjwD=IXZuHOE>7u-cA(+~L-=Y52jnBsu zR+`lb6Aa*c5w-FFdzI)gIh7ag1!td^CDOx*aNvW)@vn++fd9bj{~lYvLuUWl4gL?q z|37A9m{hJ2YNwYvPps?hxeQ(TvTFlR3oiV!MX!vo7;EG#F5-Yd+o>u5-JR%LrVxiA zN`zzRQq11{GGBn>!^w97;IQ`0HS$L&s06Z--D&;P%iquM68!?gy#my__D`_UdmEjQ zEkJ-DdsJ9`4tE8%=o+s&xwQIuqq>J!Jj_AxXKL4jyrqt7iVn$5Hq{zW&3^JnyB1i` z_V@UK&!q8muth|PUBXYL?B(kPTH7_pG57Jn)QSg^x`UkIwib)6hnjCkFLfDX?-Q^1 zqnSHFqY=MN!P~cFBuHzP1JGX`PU60edQ{KY;if_%EDG>^+qFJ7D}WOgIKK%om0O>D zOtveo!iBvkFR?j14`10RSByIvc5a4Gl!~<-WI#OY_4|SORk1R3m3=0x%U8~=8M({S zPPE*SbLQ;sCAYOLho))6Usf1VoVCuHwV-KpCRZ{&Eun6aF~)l`AnS9;J0OW5kf?Yq zE>BcCqI_QdQ;rktP-H|H7y3T<>97Wx6&8hB1#v%r##iMB?9*dk#W{>Xm1Cl%qRHJ$Vp=_`GxtPBN5s@8Q)s>4FT8JI zHvWCN2KD>gAt(M{AHm+-5Jpym7JGNSl>I4O6x3_vubS=&^~yF1HQR1n8!nKT^M{sR zQAr+|l(Q|-^(O=17JW<`n4}iwg|ca^F4-6BK&?m*gxS)r7o|}d(%=y8dC$uQrOWI( z{nN3twbWZTW=#jCP8^-GAoX01Vt1G>Lf|jPH$i|UyS#>ai!aOp_Odz^m zzsp|u!LwBN!`6rE$4W(_tQ~)mLb8kU@4~I0cI?eyS*Z75^x38{;)E+JRJGy>1dd;Z zWE8>c<^~Hg$mu*c#fYcVBtP0K0vlV}GWdI*qJ3}Ax%I<$-dYrx8wbop9VO+8{L@kw z?s`S0ADi9+nA=+1nCP%SV?6f`DsL#=`m3g#n-(ee)sSB9hg;d5EPvU%7#q`=?n+Eo zUTacp8t&HP+We(8n%S|cx*u2D=?SChD@$G-LGLSZ3c)G6_zJZvjUvzsxHgm7=7A%%;SOVrqD4W4ZeLm|y&>lH zUercG!a!dU`HN=QD~HVYh1zeZZE<_H80ux;)ueKrY5A3>3^gNDqkT2uVt}3QN+aXd zN!qD^sPKC88NjiBvOZIzRFNBDfOl(t@%_pZ)zPh>EG#h_h9+=0xj6nEP$z z-2G~$_H7IF9c5Vt)_G`c&Ci!49=o#29el15Q+*+5ib1k`$_zsQgTiyD%amJ`bkl%+ z@4ht4C5!D-#P;z)=Y?7%^yDs9-60<djvwdAbBGFyqJm7 ztb?86E{4wWw%bKnGVIc?!jS28?7b<|=?O&bsu{!DaKOPbj%#2`@l<$6rB}kjHy;Oh zVh+nD+Kp?6Dc(no4|_Uz1m_nh5?n)_V6Sk%>Wh4InH4nCQH^&t)RHcoJlk8$&3%b? zMBQ3EYCWC(Y3L-VY#vJlZ*;ATa#n8TqLR7RJk-A0snm4B%n5AJx~~mHiwFN;g*H;E z>0Q@XHJRGqJxfo@fIhuklZtj?P($R2ShGL!+WM`BMvzkRF0Igz7s#uc4^R9km>hO9 zY;*UqXDd)PYKkN8`C2XcD(Z90r|6-XCMzKa;;s14dg=hmyBPyOk>7?wUHYRgAf>YB_et z^l5yUsIIz}ceWJqTe&*F1*EfT2II|YjDz8H9%LEzeA3Wx`%)m+8C$-+lS~&m`JxXy zT2@f5qTWAMMoe;9bMAzmbO)Forgx($F4nuGvVfejH)GEO7Vn6vDB+5V(gqw#As#bR zKrM)9-0TBWp3fxMv2xo{kilHM%`nkaOt_!dZm!DuyW@b5*Kl(sd005x>Q#U%_ML;M zV=g{s)aR(78>RV4ObN%bKO>6B1smpF7(v zciU!_*AW!(g@_%_I9QVAz&_ew8{-+G^I)y+2|v3?2r3*m10-yVr}< zr@tsx_0`@wy)M0k)#eAoywzl#cnjV|o3Q88qa3p6_n!@3&Sk!E2ZR=5{<}? zI&zB9CURxWHn{OV-)Yw7`j~QE`o!SA420SCG3Z>l$`CHIzOmXEwU4Xn*H9yp!J`-s zzEQ(Wm$m`)<{y#)fU!t5Uy}s?Y?TYq{7kj^niZW<5q0l^%`e-a=FH7Ir_v0SUxpqc zS>`d*aJqi8%}pg1S05SddjHbxQgo*y#MAvE9>e*kaU}X}*V%LLZ5%IN$7VU4o}I^{ zSyKp$!WO$d^vlQj{hn?I%pN3o?oGEp7XN&2RQK8)yyoB|jQOMevy>lkh*~?WNzozMaFBMlT zW{N)uXP!m(+st&^JgYg|rzyG_R!8l}&j^h z^@M1!-8aUN!5gt+Wu6z*Z2QvD{z~KM-Q>$s!885(E@tyt(cQeIWzmWLC|7bHp&J*n ze)RSr86z$mn5cTUjVpwzU12zF@sFFRfhxXxkLwVMJazbRynO!6PwUTH`gsKTSuzX#aji%@3y~A z&)^l{QSNktv2Zf^om90H-7{`4BM*w$y9UsAPF11Av-5?3IR2A}0!R~x;pnlNA%loh z{^uHA?^kyaVcCkQ`@U*^UItdtRMqiZeGHOV8RPfmt|!Er*K!p)83#uOylBwukHRED z#rBU($%9pa&S1NN9`$$H`b(MAK7zj%y9=ZK7Jn7@h~OB(k!j6^hV zdxuJfn7g5p2e-^uXxGYsa@KTwmuD8MI%KePRa>rF_1AQt-JI65Howqg?yec4+*b1$ zd5Mi?58y{9$My^7u{`BYu5;nl^|D}56}X-kC;!J{CgEya=G7d8UDK*~4U(@{@`YTM zuV17Ph}Z_S#yO?kY3p|e#hz;k^GG{hDf`O94%R4k=`e3^%-u{*d*G<;^gpRU)15Jg z=fj$bwYPILl+zFT?cE|x>t!|<^|Z*@$EykT`+2_SniBNLeY#ASc7sevSHd-}s|%&f z0hPSR*8%0reRTsT`#&At(XWmxr0IU=T>l>9&%Ki`uf3&JTfT|-{{3zF=Jr~pOKjg4 zwOKnG*m$~=wA+vixgy{XeSCl$3T(qonX@HsC3{QXV7Fy0R%KMb_tBK<9Djt)Nm!G= z2epn{ZBV1`@CH~wUV+_u9c9%^$^T^6*PXa$BN9B@Q9ehubbK4^9-kMXt^9!pErPKOfJ%l@T4mc zr|In1r-OnmyJD;Zj(T*9j~HJ+aM>@E$M?~834&JL+SC4S<^clS0(AR{k$t2VlT=+GeG;4y0 zT2#VSO|h#iI|XJ*?RO1?d8rF zaSlEceTXFZdbc!V2n3KIm2CkbS#5Ih70%C(5X`~phke*XYOK@lNbG;{vGy|ilcjpN zqIW06bl>3#(?_)k?4-M1b_ss+giZ%GAhnR8RFFP+`9q)DA@TJN;@r}w=OQp~F!DR> zSv$?`K3@B8W|oYN|1F^*>Y|_%0}Z_iCiN7F=IX;gs?#`jjYZM~4p;&7FU(6+3eA}3 zkPx$^4Yt^r$oNnOuGKH1{=$e4E4#6?=aKy1cXMZN@vZ3>*-)nEt=mL>>LH1Ocv%>9HW?nb`{Um{xf_<@Y=#f&99nZm2jD zcG`&0lQP}G8z8}5dxz5TPl1PRH7JDdWC~~B_##x;12d)mR>SY!VL+iI*A~IR67T2V zdR_@d2K_}s9P*M7dT!tXSeH*x7Y90;_p%pG=n5P6)?`LiQ%d*LM2Ry4jhJlIaCMEa z0f}&rwrd|Cik9Mrun8-VV=+vtk^R-Pyg$C8tfVMBl*F@Sq(i)0njQwIEoJxVktqU`ie0QYYe* z%}p-}4M>*XuBK)1d1o)W54u3&qCJDGx?l5Nn?_B&z*lpoOL;wMa#`HEnfmI&`$-lT zI{8dA9RFNih~Hd^d6%_Z#+yo@JZ#`eL>#F2G{=rnb!b7)XV{e^&nl9DE*Qamzw@ww!xloEKkyBEQ`#2$8?sj9GW zh)Q1+@}kPVNO|TCD6m-1Y%OKw-}6lC88CsAuOaS*&*kZ_T=a79biJRu4pI02$9T*| zTfu7m&2qVO8@GW(mK+OJoggw0)S1BYt)Ef9#zOEmZ41K0{hu$M%L=xVQ` znqQa1)i{hV=9sB1?+l&!RXEW2cXjc(hNPo#?;i|?)0g~ObM5pDBNH9@GgDbf*2L<} zoaw4c<}rAd|NiuYAZu8Z9&70U6M&ShCf&^DwVVgl%+1e2LLnv;U7{=bN$HFdRb5%f9nQ3V|-Q{ zZfaB{+*~Pl*Ma|OBCs|qJz?Tdv!y=XF^IRpgI`d4+a)vX^1k~4shv;X$=TIE4A^*m z%z*)wm(sk;3K+E@yoKGOhuYyy;ow8T@}2ND!&JDg4x6^HL^orbPM6Hh#cYOS8kC@k)>kNVss8Wxb)G%vCo(>7y8sGCnAb^O8KB_wYhJYDY~&5 zZ5K5hMTKHZHMXVqu9yXjR8vHEJizKk`+T2YE7|8O@^Jc?^|5?Z?=9CS$%&ia_o6tZ zM7))TBeqzOj08umm2X4xrp)EHDD>`&9nuGsVNF>eTU9O*#{I=X`mS&pQeo(u7o(Gb z7Iy+Zjl;uLV-}3N;X%rBnR1ti%QXzb4_GgTDAFTFw(${jSYq@ipdCNpM0MvR3^ zMk7ej1Yhci9yE@v(~L)~reO9Wri-!rVxD`m$B-he=4RqjPv|3l#;&=~jM@mj7TLPx zUd(5gkTScgG`<~TTwq1uhXgWA_w1JZ#7d}?6=x5gsPbaQ+y=9KuTOYK1G1`}Z5jcPIjR5Y#R}RYDAWUTy%ue1# zaHiROGuLB#;)hX;U%2|C$8se$D7-j73Nhcv05^#1;rV!Q%z@=H>I8#0Un=E(5lB`w zm>#&LXsn7k+1V>$vPZj9{goH(ua2;^HnIAaM5RlT&J=|As>?2n&x{8YDX>c^E)e%? zuu*QbXtd4q${c@tZhhx`?kcbX#Yu1AblqiJS5FqGUZERGC?|SLDOR^YFh+AOPABDVHO1A_E z(ZLe$liIj9Xq8NeUM^ zMR~V+VuAc>pd6y&9c>AFI3l<7m(_%5qa{_?- zN}gbG)CCw+eOr6c>E#mep0sx)UAbHh<%p;QUb4N*uIuA*4KuoL2X$$i+h+^;^e*wR z(KG+SH9I&xC<>2to$Gyp0`5vyO9YwCJgBhATC#49nG0`Zzo=kSjRziJ;5J$J8rY4_ z(8$!1Cm(GN$Gvj%s?L5><{7;BsnxKWf&>e8F+TCkV?E-!q60CXR=AniFev5I-v~XD z<8Yx{<>6<^J0xq$M1_vb{-*8rpQ#&sN`BI+?;ge0kCPa878sDv#)VnQ4RM$)pCRlp zXEm{yeg2(-q?NKuYJqFGiQTqY>4I0y7~(eR`dl;iHJtPf`wm?fB03({8c&ZR){%a8 ztSim~CKq6$AM60h&c0E&Dd|q>-b!zMkw=W-z1~HfT1CWS_;BN+!P(o`=f6Cq%{vpR zQw_1hqNp^y;=+E>_BnUiA67aCrGCZm&FSY<@FTq89mX==Dn%Bn;pt3+Qq^r^04@fq zS^X8xB<`#B8H9~U;O?A#)QwJ2w8Bf!@;VsTL;h)GswY1UHlEC%;zl2ne?2wA*zi2) zy!IyPba=yY)m^Tas(8y*D}25MFLTRTRxVDYqgLoB#Zd~__Ju)#^;%L+X`6i)eG^R0PA8G?I1Tt*Ix8xdVAQ7}<^ch^d zio$q0EvR%6A_}o}qR|T!&-$&u!jY1^U9#oubMG8;C&iHU1I~XGZDaRjmgLjF1v8pU zB|{N^enfc@dU$f-C8w=7(HSX@>!n}OwoBXq)9>)$(mBP>2F|&^ zjCUTEB!>`d(miAwNV-X$v3FqWyW1)q;(2sNxsf#}Q@d`_r7AS=m_zN~ayekB1K32h zu$o_Y0{igZ^9s%n$gfz*i$>Y1(3`L>QNNy4@R^U0`u(+9z#?#d64FaIw;b9Ea@cnF z<-J4M?coN2=bG)`fI!EwS@Pvi&Yay3YRCfZ@ZN|Vqk*N3&!(oAs<8XEWGVKE_4rcc zE~&WX`IAQ8r+6{LgkR{RM3lgw3~f-VV*!xUqh~Id=Ol#NeL@Mo=Z+n=iW7`8w%L;< z?at0tK=NBWU942|gEN`)3|GFK7dgQGxgw}k7gbVFQ3poN7=rGx%gE)+8?#tHF01bY z!vDJQG_wu5#MuQtI~)n){v9q5S?M)a3)_iHOnd=SA{cW(3H!7`ol-0Jy?=rTq?U6a zvsT5l!mO^LOY7|lp&w6JIbqz5?p$3TNB`hm<~QAT1?NFe;~zWx2;C^_P8@bTHRoQR zJ&wokbI(u6{S-$s8_^dm9gSZeBqL$~ZD$4)mgl#Up$cg(E{HvsIgirSv?meHZl^w1Jra(d*>zu)Wcso{OD>6$#C1im=D(&5bGTS2_Fl+&b1_i6)kwa;Ygl0pMtq(l=F>Jet*+MO zJ*l+ecZ*b*garN0c2UhXkW#Q_tM&X#tTVqIRx1$XJsj5#E3b%*4wsCXK^-829ftU~ z(<;WBTw}xBSx1gTJE(|kWMjHRjlsIMg*@-&`WYp~g*`xcBt$(9Q! zdD8*kO~0(qKS+rtuDV0(R~na>G%0!X8Ght!^T?6ftQgmU%SaB(ox^I4+#~~V+A#Y+ za`qpGt;cMUb=bDDGM=sgq^%DDKJ2N+8JX?-J3@KNfkc8^+9JhYUFqnW2YdR^SUyg2 z*7@Sf%;FoymN|UM)zXRz1}R)69tlgmvO6=8{f35c)uJwj1R6822f|hbM8Shn5FQK_ z)_(bnO<>dCz4b<_^Cm0FP`BC|8?a${+T4gEZrkf>g&7k{&y#S;Wbs z8-ZGh>~@QL;V?Sg$?Acv7#Z2H*sjyek<4*0S?juXf%10(w9@v!4$#S~l!eW;NjAP? z&@Zo{LV7r|%OW~G+RFS^J;&=@uKn8|cmNu5I1)IQCSFc^kmSphP-_~C%1b_#XtV&oDBBc)NU(E&zqW|$PQX?lU%YuHnH~{ zfciGd%Q#eKd4~fjS4pO&=#nj;8Dwdn^!VNl=Bs9mE%7mfv3kmn%RPB%EIvwPMoJKn zo$fb41tKbWB&C(BQ7y(HSGuW3KiBEOxr~i9W&e~d*eiOwZTR!RexUxU-<=`sAH%L@ z5h)hJOZyg0Oxp4{U!RxW&85PT>zt`j87%+@^XP^#u7!t>zeYH zm}CVqkdE;U38?wpW{9(=Vbf$JX%%-a7F?oA1(W* ztZap!EFd;1UD>or#Q&y;Sh(?h&ssV|)AaKvxXVCM#!n)UZ^46%!Uq&9oRh=QAq=U6 zuK-fD=B-<`LQd<+%gC5e5+f1va-ghBYdMQw!W3lz^pvpf$uGQHk%s8Oj z#PT4k8}ipciR)czRDbo_fg5Rz!%F+}Z3SJtz=HUIxSx-;bR}7$wTbrlf68)t?NeOw z72pvY9ZAiF>*5A$qK4ypikAJM;^!Qyxmnay=lnf|1n=d9Xk>3qUfS5*o$ngc z1(G6PpEB?gEkBAL81cH&Vwfk%u8awXl~rqr8-br{sZy%FEa<#Rgz^u9J1X(j=tB7Ttwy##9_%iRXwWocWGCE$)jkP>=ev(`|=u74Dvp* zwzyj=b>$|Oug-JV%By1HOOsS$N8*`&iTxe#!_o#}K&6+H(kK21j6-|Ou-*&Q`ZQHsR7%vR0~+#lvfwcEJw5UabYt!fy_n^c>Gv$@RE zvS)Y)4tQ(J6r;t9TcQ9Fr#u|a0)ec&e_Lm++xC+gd(cwbV(Tn^Mv1S1>FeV+l~`X= zN}4`oTJoc@kMo&8riE5yc!9?_$%0qehNn&lTq2Igl-US%los+Dbf@mWYygk@3^#hj zZWF}MF&tN%4J1Zk{2V!}yar_6ZGtTZ=2@Xu%WH^HkHmN|hn99xIC-h%M<~Tn2ka+= zi*?cBXGY~PwMAFMXo5$FCc8wxemV-*7C7jbS85Z*Y+sKHCFKZACIFIpWKiKdfHIFJuL;@7mYZ@a^oZY71;+w9 z_Pn-rJy*WX3()DceGLX*J)S-a-JRRo1)I{gqFt?XWWCoulnI7RLX^e~<>9>9L8{{h z4VRl*!y!iq=z|?FC0k0;ZHV~&NA~gen>A@OZ+N20uuN;{>)j|P{{Kd-DflD znf&5^iiA3(_S@Qit*j`$DWMMkG^cdZqO?bk6C!HVoMU=9D+l>9Sz40bjqKY!Y4~9W z-vHZg)c5y}{?6T*;}fSM)6gy*CU&CIk0;3&(w<{^Ue)BQjDiMY`HoK3qHwPk<+5_x z1g>@tEo_f+7}xQwFUVVMD34>84$!E0EIB@8u(i%udFKe=P~EwKIHJOhnfUPRn`Pv* zQ{m9*0rZZO{6ceEv#goupeRPcP#)eK=&QYx-%FiF31cNA7R`+fny7THAcN4&VAaid za7_oD52oXe@ZWhpF(IL!(4zVKv0ftt;gpTY881I24mOQ{B!CCzltl3nj@`Fp#+wESDh z4#-3nJF8stv&W+ny7&e@bf>=^ujv0?sB2?|b-d7`s zlGS#2s|h!>1{I!nnm+w5sX%c0L35VWPBP<6JXNRurtpl6%VsMed_C%TA3VmG&U(zY z-mW###wgaD5DO=By?<2P>URqzbe z#lJ2)^CNE;y&O;hN~sFNFI^yaagD56)W?%Emob^4jfn8tY-=_+lYY z5ou9IIQ@t>_-eD8$l_FMWd0A`L%HKTABQ$>4L@{vv9vKY&*EnO-gofPY$mLIX!kFY z3-3y(e<&56M`P#-#p^`lsjp*08&M<=+rPRQ_ zu%rpo>w-iqzrCzkO!viSP<(xQhbk4{-0HOOVmoPX@4GGt>3^*adHJ-UWY^#ptm zP!7mH*t&ZB01|cAQ!3_-EGxUSw7=8Py@<}T6Zq52K2{HsuA5@&pAi^>8pmbPQ){({ ze>IPWeIXsSp}X-@i}vcBwI@u`4Ea?OLMqpNm{`m7r%MXVoYW2GLK4!0*5TYPMO}qz z&_=L`P_2^%Ga1p$+#V#Myq?En;v88oqt70hb=O|~sQN1h;BpY$^&qWW0N4Y$EG6v~ z3I1&zgjc?=YtMXGhG^v;#mcjc9_65a22H{thW25M33#>x?CCT%n*AExlk1=ytNf&> zCx|YJ`%dNF^DXtXH6(q|uPF(ei>g=ff4_L#$CZ5`W_L$R+BB+sC@*ZTE#Km#>#p|~ z=vsT!^LT;8hUq#cJbOowHGRYef@JDYKZS9B4XqT=V=++OI8TOClW8=Z9e7C?mB+f7 z?s_1o5sVBt(wm?sN}oFf;(!_b!%{+cB&w*O4gOSP;8K>XcrlxJdTqY30#`IBymm4R zke9V(_5%sX9-8;6PC_L^nn`=AEFXQh`-#t(WDAT7T5SHf>@noZXl5 z2P35B{)ckY>9p`r2f7m|pzUi6<6Ay)IOL-?N%8*d3BT6H)+&l~65E}J4>1Qy!JCcn z(`1Wlv~2h?OlTs0jR608f!_Fo&(tIfJU{~oqUWhtCGn>Y#kaVPe&W+-?GLT5l6TUe~;yD>Ny{12|Di!xN+^P7&%)|7Di);m5xTx;Q#1#Z`jZ#&SN^vmE*-7d;sa&8aA`xqmWRq@aRUWT`g?W5v5_fFpYG%oti zaBta-^xoy@-WQkbV{Gp&nGGxc6p|VKdw$wl!E*ox&&7R|ZdnH*t=8C3f#Sn#T_V?d zr&3gyoPxGkPO;s-5Oy6kl{k>0&t^14hezU}T@{5Q8<1tBicK}zw1u4NsX`D&Mz zCxiD;XiUQ)2H2iyOzb+B;0h^Z(bD{qQ@sxJ*E>JUb)QbfYpx6y&q}ulqjG6wBsfo0 zc-46fBUwgn9W!7-0U$5{5;IWoM6pd){q;zGAjVlWpR=2KzSQ?(4J`;3S-fOsJZnUO zY$d*2mm9b>D^khO1qS;&j2DR{VG`l&oiiZr>L5U7AMUwfEIp{ci^s2~JUax|v}(0c zQ7~3@exEM$*7vTx1M_L5h~+yolk-w>IK7h;jL#g8Voo~xaH-d#SKse~@{YqbuN2@w z04j+O_DFVopJy;K0sQS+Engh7`hLmy*jNI~6X*fQ_Duij+kF*I)oM#jURb)&H}o@R zMkKmI$pm(++wiR6Za1ZNc(j_lt4sgn;qLZwHzm>?sW`~_@?^$@@k2(g5itoX54<~lz>xEVH$1D@6Wp2*Hr=4^1 zW~WQf{Lxy{9(t=Gn*vo*52vDm*;c4hgLyi0pQ4;57(oLMJ`?$pnqBHaAQuZEeBIkcXEFK#ZeYs zc6gKYz92NETGDB{I^7LbjJ3HyQh^a8rZ3Rqq};8ghUi_Go`GynW7I4hJ@A@pO$t4q zGJoZd+c$zf_F5DU!AGL2A@Rb-NT3*4UPG({3O)!u=o;9?aHc)?&NuOM-i=Yco~*~8 z;~ZM+y%Nv0Pq?=6z(T4#7@eOrj?zA{w@;-$z$`33G=-|FeKpyzJ)QhGyv z5&^zPgN4LWUwc)A$duDz;?kDKjGg>OO~0D#PU7)0UW_YXQ6&ecSuT=?@NGmR+*Yt8 zNl91EM5Q|_;@#8pZ}3xPN`BAY1{g;5!sg4nvWVm(RilAdUC`AbDUL=}D7mN=$0oh{ zevMs=Hi0kl(EM-IPwX%3Rv_<2R+Zb2OnXU(B=z?ye(va`jJQ!%N!bTK4O2O*JZ9q~ z-qaTi%@4>|wh<>3<;q=xClq-K;CMkdw_LM7mDTG*F4uBt^_!DG(i-*0132U5Hak8S zQy5YxE3cH=jMMw+ZlM%|FJ~I~|rw?(@()FqhQ!CmPj=wGM!nqy$WrhLTCh|ebr^6o( zUd}qd>D=mGbIpw6Ar_YSmLMf3@0C)1c({)F!q^=4#%>v!5@+kZ5rf_6jBn+>o2HsE z%Vl^$?0kHC+dv8c7#2r_yqo3LJ7z}ehKZ`lIhbr(?GMRAYY*vDarGk=BhhQdOV}RA zyF+P&a`%9)h{Wfywx< zG>gDiX=1x5UAmG78QF^VLW=9h?#aZ@2KHS898Z;C z%#qp1jGhKB;dU7%wZ3{5{^ULP9NSX@^q=YPmP`DED?NYT`7)wE=fm2Sr7QW;w3NTX z*p9bBT*}xc54t1xKdmv&3||end)aG74p-S-1E;AplbT`(^8eHxMssQ zA7bthht%6kUhXT;jH}kSTs^?+tI{-~)K2?R=Yk@XilSu;^^uxMj6$>QN06aSH8&Y*X0NCIwR!SCn6FQJ@_l@H3d}XaQ zS!YVw$3&kn+`0#>I@?3Ur2PhwXx{;P^gwz|_eXqzMSaOS(RtD_d13z^tIz-wquJzw z>#PX{EE~thN$(N$C^hv*cuA%)V1rsqS|-sK_aO1xabTD-(b+)UzRoybLL z>S=cZM_|LXt8~TPuEWJyoi|;_Xud2Az?3Hf)w+&gWY%^>#d2L zzW(fH-2T=Tq}#dIbz8+;W{;V4nZGs1ys8JWyI$LNCo0pFxd)1{soJp)5XlLi7o1ZE zJ-AU9X?+#-auDXm8HfcqpK39yo0VJC_jA-2@){jO0*9EfvkVU}@L>G(jiFHLFpdv+ zeF0lP<6Ut7F;gpP3XNfNX3P#FPzr+nS~F`xahf~-0f68CW!xYr`#&a&^8-x={QY2S zlgtRXRP_JO=+?pn0Li%-ky^bdQ;;j`0pPfY81Zi4Zx58R8RJKu3Yn5YnLk6k*@rO< zU14Ctn8|f|i68ya!+6r8Y5rZ`t|MKKe7U6QYA!K&$hPKC^8S(C!3F`pjM-7A{SZGq z?Ox@4xACg7SiU`YzGmR*P0y60uA46=S;{ZJJNQV$x4&zMvdb5aeS4uv=&Om8ttR(9 zF{iU<8V*Nt-(?$ALAj?TE|*pZ1v*p*Rii@da;jy!yEW=*i@ye1Em70bOpN(m_3krw zY}-)HgibcDq+3?Fr&5A{SNrIDfQ)OM;>@Q(k=E|Xc$iHx6byiA=UdAlx>D(nyfjax z+i-by2VS00rc-yjq!?zX%*6#bJ0LIJJ*){n1<$!KHcjx)a|^K|GO#FR6%`c?Vb8=3 z)K0wB?V^s7>N80%?Nur~aO%W>k@d&>CGL}X538+p_F#*aVPdpIR82J+$AA~T*9RT@ z)uZO|^8_nn&k!4C@5!IAb>ST z{0+|~DPiikywWG_a}ksBxw?;=u+lf;cfs^l8adK>v#b3hc)0~P8y8i|LTQvCRFSNc zDuPJiWzUr^l9r#EZB%Sm%=Fi1XI-6-y7ASlNj8cHg3@&uo6+{O*124X8lFGPz$B3D znaujAsMJBPd(vKAa7u28jhi!sy+>eWlD0Wsy{X#!L$O~-!E#Z9yI&z$AmXN3>Shgj zD%o*F!p5lKyW(@+eW;Lib0#1JDn4QW2oU%A-V9~I*K$p0vCHN@i5&?EE>;#L1bO!3 zt8M~(4n?Lgt3c5gKfmU!C(9GA~6$A@0B3li>1V*xGGNw`IX{~FykkZL4#w=EG zx^vzwP|o8D+TYZbq{MRdY^%|ux*qP$q{SNv(IS~l(-$Mb5=0zlpj42Q?8;WCaqsB? zJ-OJ%kYw>h9$gm(#BUUB8WI(T$jc;D&%V`_$UfyV>Ls;)FnE)Ib~p`$k{BwMtoqZN0UX#&GQ2iiyeVaAxUnZu5gF>`a2JSH%{t#eyk) z9YwVYAm<10 z`;-U2tpzh^-=EwHV8Vh zvp??$Kv!e;50|^;?yfP>^}fm*&Q>3cc4z^qoC1|TH1-P=PHK2@M}&~+8MqM3z~P_j@kYD^Mm?XW8*GG1+a#1l?@LQBkhVM1?-Oh z65so6qmrV^J~Q=E`b5*ik8KUoO&q8IfudfQS3;U4ihWfJj~FYyhZ6|~bl@GU^L&3n zL1W#K_Y3R89)|HYfwOlGgx@@VS919sSB|G7F7w20e0>1AZd270#XBPKv+?Md6^S=u zIs*F>%Ms1_UNS#i^m~F%D>h!_B)*)GH10oMX`r%LDl0GV`_1Ji38XCge38K{!Q1 z-H;|}M}lf(Mfez3OLWt!?@AKr_~V`FxUGlPmJQEP%5CvCnf%ua2!NUME(s<9Rp>#t=f_+%vwcHX~fpw**sc3TY((rEybY?9Mce-Af+Z#9lxjnAB zPoy^oOEO7`?X30M!@no@r1H&6)d>T3QMj$+f&N1K1Q@IeJerrb=@k4r7xtfyV{nxM z!zU1MnbX@R0QhxOi@|TegM7@2-2MUGJi_1=jOV|zGAT_!G;t7e$-Ma94Q7a2j?w6W z*BQF;!cclpoFps_g04m~I=AayUNJ_) zeY(i-ji@Fx6BRB|{bOYa!d&NIU_=;35{3L{nvm_*I6}Aoi+K#F_|1034ui$^p?BG! z{YUAR&XmItxAAr-(g*h6WMM&)U(yej6-Yo*KMihxoul~*X4AA{uj0FK9UFB@7t#z0 z7&Ih+k9@X2D%{vTRWnM=w_q8m3-V)zk}Qktv?)KXsoM=2LddgV;xU+TH6}b)lJu`a z1bwU216S`o(|N||5fo9nfy0J{uy2j?w>GQ+pT?aUUv6kSZa(fVb^w#DsUia0XBkgA zH={Ym^FMNR81?@@w$%T-GR6%2x6#_w!C9`e5M`l9hLPPBT6+tzeq1=fbR>Pbonp%% zW~2=VbT>AY`in&qW&QW%HoexJg}$8&qC0XzA-;c>&oVxo5n?)W)qLR!F~0@8T^XHU zKm-39NV9_tDK)p%uVLuayuzXx-PkdtTmPEzL3%%nCby6D%ZIaQ9cXPJ113cSawMb) zV?}C)NNO61LUmrvZ7~`ybSVbg(9}qI3w_I=!$J%(Sh{cq`~?SOeWWF{X#%ye{T+WI z#FE)~c8pGj-L@!`U@FvHuCCpZG2Yz8XsiP;E}6!yJ80s&Scy8NjNdq2rw)=)AlV7f zM~M>tF{Pu^OCzak?^dDuc0ZtSO^78a9A<~@dDVOjRKbv3wvR^e>;Hyb0dkho@?98s z# zehULdrC!tR-haow4n6x*60kbeFlJF79AHuAY+OC_Ash(*K!OfpJ}uQHEG*o`$R#<1 z()8d}_CBY!J^-HuK3n?0%S_v%+S_TH69r;9(lOUL>FJ2^68mdDb=ZAq#MRT}B)%Ovmb8y zbX5Ax_sK;f&V0D7_r&-vY9TdtaXHxdz$Zw#>${U!FeXRbF_W%QbqojtDyQF^?dz@7KOz8<#VVyd?et6bi=O#_+%P(>ohp5wle-7amd$2qU0yzsAe zxb%gR!d@^=NP5{H44i&jtM!~!4MyC{;m(;S4&uu?rlpSy@CW5?nATaRb#te>WAR9YGtNxwg4$8kZD#3L%p$7p&`Mpmq>-7&kEE2O9x_-eFmly(KT5nw)JTR*!WjdWK}R#5e@7^)zMI z&XHY@N8}brx8JI553W(IOZ4E3K8cM(^YLRz+F>{28-sXZE*a8ulOz!YqVZuaxprdt zqosS5(6+Ao#1LXJOAphU@5@Wx=X2)U4Xc$<&yvNWeuIX1R$ZkbdqRLuv7|c}zbQ&& z{FdB`7RJd+7;Iht_$S7yS4RqZA11Mnj>}=+Cg<505v{atzM9T!Dy@{TGkTh*N{;(( zLiFu*s`am9q=xI6_N=Lti24H%4wQ1aFLqRKM1xNRo9`cy@HqnivY^qksXioC)j^%V zpms&4d;a8PSfX}{o7D;Vc4Jk)(8x1!Puq%Q>qo_8u|9ce3d_R@+UZ|L<#7t5(Y(j- zwN11kZEeOf*-8PK)cOdM=;J#+w=diw-3>38PM3`j+Iw9dJc1JqULlhg zVA+kyVfuLjCJmqF8Z1-|YQ~OzEitxwg?Eb3%@dv--w>>AENT>DHuBk5Sk3E{i+>5= zkYDGY`Uo)3n>(h;!2{ZOryr*0UM(Uwja>D#S)p>qn=E@pA<4ns#d_2| z+V(<#XotginW;y=#Lr35dez+n+~q3|W6!j^h$##$5USZH#%W>jm#hP>9bXlr=I%La zeRmfloEQh`xY@otYgzvY4F>*u#@?+fD<8=90gP<>KvS?{KCQ{6edN{aqw!%vMO;=s z`=r7lFW`^RzZJpu<=N*w7=y;uDP29P93M=iV{oY`w<3A5C>J}*4G9`d&X#Ogh+Ru0 zors+o zaUxU7z1$b!N}ZL6(AK%5Ha}V(UOnQf@J`W`y>gte0-vHCgDXq%>+-s=Gy``CpRbq1 zBoRqCRMno}RqCe43xt*l{n?d<72hu~8t$|P4f9WANZ>in%rcPfebOft+!to+o!Rqp zg6ic|$`kD7`<|LBG#34S*dksgbU9f(*W%#g-a4p8oKFUg@RV4!c|_oI2L^^qMk$2q z@t}0;weTNG!=LyV^=pEYbj`dWCAXkH@cd8hjaiU97QWdM<95L`|BD*Tho=q10fc7{ z3na7&xyvVi3ZG9B&mB?}jn5hs;9h_D@~2`{@PRX#>r*G8)!T)}0UxAa4EiI+@&0bV z4_nbTU0~C6-9BXRq=Mi`!&9pQl1B^m z=QIC&MUmgPtxe>#SVl^ny6;4UPp7tM+1L!pgewj;le6nh_nYU-7;-%4#a9Q^Cpm4Z z&l6X-*#yn+HnZ)hz>pR)5G0&*jt?_T^#}Pa4E$5vU92uX1alyc%1Vy0?`11;=3N90 zg*o*0%f+i5g1?nS`+3f;)%UKJy(Z;T6xsQy?D!ml()i?Q2^vEIhr}YlX`|UYc8t@n zq_K1((8s*J_NZe)S@NCmkeOwG_DQ4UMGTD!N%!#?ZLNk)@q zVEbd3jpLIeIyt3tjcNdH5{lUdU`XRgpRlQY_1#TmiMZW6egg~`l0HuZ??-w8$*YR`A zUBE=8E;oDp>l8@xQSdBg&f82Yw&^tI*QvSO0)sjZ?6JGz4JdZ+@#<~^74bSk)5)@Q z&VFOk;{0>se81tdcK{lE8t`w=b!3fp_5B^7T*b;xV*IJ}TE>6LdmrQ&HtXi4w1N$#WqAfottn%Fj)I~vWH&ebQK6% zbeTRERbjjlj*T|s@$@M7ii^%75KhE%MJ^{N{BT{Tthj`)a#GLut|(j7;Rpkf)MHIv z1waxj*K#VcH^h_iRN1IY+W-*q51|}pr~?V!U!7{pHnkf%FG)^}cWb4#5g(2h#K3>P z5w*JsKQfoGITFAjo)(mUOBB`ZpW+`;iIB9plD3t*rz*I1HGsb2ISqFwa`)a$f(-|w zVJlR%VK0Zsf`Bsx6`TyH9H>g%ck)6V$I$i=_i><%6$kP_kJdM@$pFjK4*(-S|9xY7 zHv*0J`Tzg*CCm>CfI>4G zw%V<|e`)_0Wp(4kZlH;lXd&jys0Lgahej`1u=HD>T+tXTx5r{cHtB_tR`>Gejr%ywmLa}C=B0Q9G4g)$rh8qr6- zia#E+3y1$8NG=Rl0PsbF?zIh9ar=Ufsd4JMTs3nkb?ML7jzkhhJP$+)+_7LpRRcE7 zC=hN}Bw(AnZ9sr-?qfQFOk-FJ-8#@Flv7NO;Rw$!o~?|+(04sXqY@zC$QuNLmv085 z1;$(nl2Ou8+jxcT0631zFpEYgfj9)O8goQW%W+eU_tiMnlM3K-`vkJ$3Rwb+iX`^uU*@tN+FYOeMA$pA-N7 zid1IQu3)+I@l2+WZk#u;UK}_NUcc`=ztel~VPIc1sB~AS_Uyvg1q>Gez=xXyq!YO} z1k9U@_>IHGaxQ%g)6$GQoyLZd`pX+cCZa=8Eo-CyjHxve~1 zCt5fCD%Qk0u`6*|2kb;UrO^8;7uCu8ql#iftFl6W|7zAi$OZgP#&^S_HSnw1)H+n4#7hbG)-ot zJ3I79G}=SQi5e0^hmjvJr|%yPy{Z#W3)SJTmH>z2D*GA9%nf1TE4Y(}{erOIU~j|o zx3#|V?(Nt}kYdHuvLQ9wK9YLz{LpW%7^EloV(3SaM{rO`@$wHN;=naERtcJ|+MX#z zR>%!l+uT-`QCsp%omWgl+s~c`PFzR6F8^Jp2wjF*?eUpyzvMkN*)1(4A+5v;d9Xuw z8yeFP^jU|NQ06rYvAq<8N1+J#Nbt*vO&hXJRg1qwoT|`9yCLgiV7mgQKSFzK8hM!w zscuGoAFEC@1w?%H+M!VV@EjLK#E`Wf?^%XdQz7QPG(X;%uf05f=>*>V9!@0$?H(;bSz867cM>nXl-y51-2J==m*?`T#4rM zdzg>jfS$7Zj*)?(vvH*b$ZN3zlv4r18FeRbC;1Ppq-A_=!k7umt{<=}l3z!5SZTU9hTeD*8y9+-Nh%mfe&Dec)(ws-{}?2U zqel{3ikl(-CH~B{cEeBJD=RFR2S>I|dr0N(P}x_LHn5G`IyLeA@vLg}{pe}(7xwXvD} zOcTk(a1j7|{oKpHeq;5q>xh<%C^5aKcr!lP%VSFY8Q$x3`+%EBrZfMF9od?B$NC5k zD}b3;IikS#r?>y0+5A+4BD&0Zj)hqa5HzR}(mA_Xl<-s&sV%fq;>J^rJvX#41h;io zmKm9UWjx15W1Hkz5eMRGuZ`)(NdMhTHnITo*lD@rcwk$3YBa5j6Q$?W4+}#a$Y*^d z8JxXU7x=)4nIScGfZD&IdF0CN56ko#3`td?NNq-k}Yxs`L|KzM8ZIN!m{FYICXW4CU zHhhZ7)=+!{UMc;np-6kge|=97?W?QaE@tl?XBlLp_t+@qEeb!((fKG0VQ7u&`l`={ zoMQNpK#(T=l*S!cd#4RT$`6Y*3jCuhT1U{+nWp8&8rY;k2@Z_Q8z6|1C;xRVXq;cH zXUn6HE@94b)OOF#LQzB|$)aYOeiK5MU`KnHE^hnGL7M0Va!$6!%ri3%Z_)&=03Kvi zJ%$rP-g4ZjFHl@KHm%-f^NCHk&?WqG5}T!M!_Jg<>Vicp#XqN@G?ypQUIM43zU@rx z%)5An46vG)S=KB!Q-j81)_1d9jbr4?1~NU@y4!Up*DK7&Z!PTK$o(#wN_xg3rStE@ zO#BPskKbXL-Vfl+doTn2B6ORmEbp&qUFhStodxX_XQ$gW1Lv7NEn6O$Yiq_@oSc4$j1wh;P$W-E$Pvo8YLnUCWF<1jI*=sC=T z&-(K=9u{2ZfB~N|g{#Ds%)rg?Iy&-?XK?V!@{;2`;sw(_Z=G%NV@l%N*A8?n^2{-I zDf%h(AZzAxFTpVko&<2@{$xkQ!!}L+^SkhnlebR{zeYY@*mBlEE2ne?z^+3=QVfqW z2ukIkr(3~cAf9(ClI14zPQR4TY+WL2X{I09>3QoErf!@+;#C;3s6zyEWaqFOQ^i)&3@(YA*pEj;}Y>GkL7k6rv zRjwAvaP+u7yYZeSq7aXd(b%tkftmRVun>ZZkU3!p755`_WOW#_gMN$VxC`@oXD^>_ zA#_Mm9-XI4{YO>zGJ}yOVh0Z#VBhKgx3q$x>HYU5L$5AuwXjId?5yoT#hDBmP6sMc zuJi;^G721+(>p`qcH6t8&)5+&0|Wg=fdNL$+;?{R`0>K}+7OY8&9;5q@rC`9M@&0h zNGeHSYq9bSQ)>%>5SvE-Na^4}GHv_$LQ+Ya<9ueHH+VQSbfG-}9s^^+%nYs?>yns$ zvuo(CZ`w0+pZ!<+B&JT3L8&uIG@Rb7wuUM4>kfyMQnstAFFMGUKELi>_(e)eYG(vj zzZ0&AE>^zZ649(U#ZQvi!~M^n>f>FUg5ES#cT5AmPSa;L1IR3B7n)S5Y_3OWA_fj0 z;bsVQ;IR*XnerQ^4~4)rG;QDPkWp+~nw2KHF%&5oti&XCe0vU&4;N*g?Gk%Sa3kIT z+;@jR-^^r1z(dK0#6GYh@xz>&=zrgf#%-~fxk?5%Uu@9C{d)6uycgFqGcGl3g zbCDQ*6uGst3C?|Ar6ZWR{TV%8+aVgvUzJMHjF(v)7|cmrTvs?)Y2Zr4*pyNuc1m@1 zppVb5Z?-Cjo?}{jwX-e{hN%aGoSD8)ZuskL_w(QTzpwuK0s7}wrlJ$O8oJrixpw;T zynhL;2VHULFy+*g1kyKn4rDz^z8y&9=fHHHz{v*;ra{#^{M%M>@%L-!`RIO_4)lA6 zIHZE@D3a^+UEIEel7&VOA*4IQ#}Ax65`>nA-3ZMa0FtZ#7`UU8`Z6RZp1%H4d|F+nZ`LRq2;FTYRGoizjy+<&c|9YNZcaj71qxir% zDZ_u2HG|gX#vR8t)>)+fZHOnc_PRKxPa(qZA65M$Pt~&QcsDlNiN=o0Mo0|r&IUV> zR)@O|)lQZnu0vk`sKzWRI%{o?!~uD{RJ#?;uLHQ-&IF6G(>Fhyw6)m$9`Iz_ z&sZ267nBqp0xiDT=MA(J#$-q}NR~%0-GE9T1gmDebmYLe?yTjW?=Co9sMQYloJH#7 zPK}LRF^GbFNT?*q|L4VY%$J>l$8lgTH22!^bedh{Nk90nD5)6cu*-Xa(NW)jFcAd5OFXoLdA>srncCG9jP+pPX8(ea!%@T)lxkw!D$ba)i>CGT=ktogw>6=vvwh$U700r}>QGde0pQ zZtac+YIdOT*867Q?UE98N+oWF1Bf@?xCWzjCYH*40mOvVN-i2*q> zw9w-}R!|Y?gqN@k@#r49#yojC?QLHzwa0tvVhNA;AUI*7qB2Uo1As8Zr1*8%(9o%I zj$%(nU!U!f5vIfK5juNOy0aP6^ZcY1r5NmkxmjW~K7dLd!8{mXIP)Sy!{}}7P>t>Q ztd=A2mzP;o`#bfeBK-ByOW7#j+6Se_%PzCzy_*(mFW^y8yVkZQ_^pxf+qeJG+KiD$ zYo&S`iGMlN?{R)O+k6K9bq0+a32a&iTGLk6yDf1`iS)ECK@w4<$$E8Jg#LZT8nmv2 zXTE7aYY0&q8v^17KIXvbgyDkBW%pCdGv$tHp|>d;_AOoXAewo|OV5f;Vt9;aZoSx& zeoRL|H*r}n{O)Ss_t_;6^xG-C3asXH7L(LCZkitKal(b;oFp|}O?#GI1OAA?4|}xk zQF~ze*mB=ddNa_u-*jpGHjaJ-g*S)lK~nehp!J50d2~|5vllM$VV>-hW>)MEatV?j za6i2av-J&ZsA$xibdjhHp8X8aK{gVB4hA|s{eIw2NnvK3*W{WT@KvGXahcwK$+0$p z4E@-9>W9%wvXi{racL*)esqfG@82%xg6=KzNYwmE~3<`#aWVeMOjim{s_dcT5Wb*8M{-%`U`6FCZ{1|k% zC$f*e3rf#6YnM^kuu@wCQ7{W4$qq~3D^{+gik}1qyPMPuS!=F01>jbbu*XFjd{U3a z$_||6L_&g+aVuZ;)Eca>g%3BVBh5!NB##a0X?;7EYXks|?*7I_#Ma-<_`@L`_exbA ziEGo+Wdr9e9QbLiYgl$=KlKy~J`b&5M!2E3e`Y2SGU&Bn9k_-QT{#yU%dZhZ3CZJukjP0ul zU&vhKkdT(G)sKfC*aa(8FTP15H~#YWANOCZmWfMEk)UFnX7T*iaeK7&ZZ#D>kA{_t z?%KFFu@RQqz-V3CmS;2(H~q@;lH&YQ^M;m(@xzeFUbsOs+?2ZP0jbgZcF)_G8l#8SNo$@vzWhY zwnoEMgDnX+KSz*zg{4%W%zv$W3aF2+^B-=d*5#+s{UaR>(&!yD@+eO<7p{WYc5i5v z2otzvz_y{$+tTNu1ha`k+*$-SY@_%5mOX)3Y3-9#z{yTM5nYoS=4I|i`Fl+U%}4Tx z@QJib0?|2I-wayU{Q-469OX5Phzis38znt#Nk3+He$jAQT?$VBc8Nf4-te~DO!g&J z!1AceAt+Fu#ByM{syLKy zyvTR6f+B0HXUaDk4-Q=K-nfj9@i||eC#yuV8gC~%Bu5yVi)E2#T}E$N8mxds8$8|4 zCt=yz?~hbO&gLgXoMa(stXV7$ICDCBi0`$q{8@VUo1`!k{DZh;8&Awb=?pISn)!_E zm*u#+xz_CYD>gQ=vT3;59*nTeP{8mKANtD8RlB?=g!kP=o2757QQJ8Gk+%xnx zBMT)PFxvh_T>Hc{I&kzpekLt8%CKoRW*Y4+DYXfXR_CBDV-fnpBQ3h#O{G>WUku_4 zYS*e03Cq_IDqgr6|CHK$j)y!vsTVY0utTLro>ofGRjcrjJ;~y`P7n%ytG{5skc(YU z)kq^-tP-xawsdeI%7^`=#$hE`aLB)rJF`W!z~2K2LCunmUwN9bmoF(Tg8I7|xhjHE zacpwyt1Zj=J$>HD*K^Y^guGdLq!-g`&`?-Toz>^-rj#uwL|8j^RH|RLXs8JDHD@WT z)pD-Qcd&EnbMP!7SZS+Lhnu}_TJx0-R=s*zt5|Omw5lx@uA9+VXNxl7SR5)D!ejYyN4Q++@4Ax`lp0_>b>!u{+G0Ocn>BF!A>1d7^*WY z^$fNG$l!FA2vlaTDR@UtB0Nz9mrss~4W%cG(lk!a-Fi@NFP_`tdDS(y37xZHA=lJ+ z6!x^lKsz>EYH%UI@|0mzfH|Dkm1{xZ-qaY^SI=_$YYfQ$v!Zg`OeCwC^vgcQXFf!M z#dqr(p_HbcQd3?m$bDLpJSy?6{S+)^>u_;X$jTJnh#qKqEneJXcb7f0v)zYHxlqRA>N-pp5%0Yu>}a7S&!v0K+#ez->Ty2xOwqeVkA^)n=0nP!)d}!AKIO26FysNOC#X|MBRvDX;t!IGlgSG-vQ(^wzxApQuHB%zdDcCd4G9 zhrdLhq_3{|^k&yI(MZakbIhihFAKR^kXKv7u|F>rdy+c_;{@{zRDJE#3xL3LTvv=* z1w!UH^KoUl^#xWPg6Wep$Ir&CyOwL+6C(vohY&xXG_nSQ-nrl2G?i|E3m?&SdzogzDchm$G?>WENi3eGR9IiYK%^$uFlP3uCf|$5*RZ zFt<3t?d5fMa4{t@YJ7e`llZf>N+m8)akTYpY+&Xe>FE!Fo1S8$^GpwcVB|%bm}KMD z-%8w#2@Ah|oVqcoo26@K^3mLft%KDwG8)$&l%GH*2k#m&luzAA>7CTDeAX79hT8J) z1p$=MtFn8|Z->$ld0H$HG^U_$YcNAvv;MRJaIC&Z|5N{@WYlr_(R$JBudJv~;D|Vx zWe~FYtI5y-ezYq^gBeJyk>#GEQNUa{ z8lz5{4gw-tU5f9f-B$Pg@AqkP-QDH^Z2cyofF&&kJD{nU-^lHLLx;sIna7ESx{v~@<_(LnoU{A6NealwaYxaiG8;SM5RGO zX~BLgBNJZ7T8iWi`e?~GnDo4QbV=1L#V=Dlx?Wvwk*6idee2I3Z=!uxKc7mPLgre| z@-O}V)ZXlPeibY#>^B5Tk*{gzLf?mmv`qCoxhJ!aLVTP zafN5;nN}CZBpr?FG(MDguJ-yh*U8;c-KWkROTC@=>ele}-Gnn%ACRn80Y_z~gW75Q zedY^UB^`kF>(-}@%H~tNI!0Y+{fN9e(LT~o#MBDy?dQId*#C2 zwi=VPZdXFp301joi6pCPM_qAE!9VT2XfKMhw%PCX^y6}&Y_bI#y;pSId}I3;_l0-Y zFvd|*Oimo6FeTPW7Cf`fb`ILOMnlDqN#-eg_z#cmtGsi3tM^(zAFVtdVHgJ3jQabs zZ^Mh%hc!qsMVpQ9T(Er}wZs9L(Mw(c5eT;%9(trsym^Ysbp2RDuUE+8-gWn?z&GsVg=ZP-Ul2C8 zkQr-)C%Y*+#NnlG9i^!mx~XdY3O#~^@Y@{AEkDu*&mA5*)P{#WB@~;D`sm($%m^F0 zC=PC`H~guw`CTJ+FQ30HkqWM{$WIAgX||_t(I(?VXXE$OuY)Tt#QkuzHP{HB;saYE z(G`_a^Zmu)g0z~H=#&~&n~iT=`JvC+k{YPW{q{z664*CI_wO0SbCT+c=7lvj^!Mc*9U5bSY2P-&O^i^VSoK6hkBM(acBwV1j4tZL- zkq3?2s+37zQimUg3W#eMHJWzZx;*K*K5y0WQtgFKz}IX03R8mTm^+Pztfr(z**cDk zY9_A{c7+Qm%xKWb9UAznAx7>4`~Y991o)wU3H?SLZ zhD~tqvk|E%H*3x#$XROR8)h*{rqke(VPbDVD3Rw6>~fexGMeQYZlg(|4}n5)DhsjP zD|fFYG#&f{Yai5wQM!ohugXH;t4d0^02^j*2g&KofY7)zP^(X(lt&3x`6vH*jN(%y zbZVvN`))HEW=()%xG4NdR_Nh8k@3!^;P{*Dn>sV5{mi-VpZUHmiTPX3(<)rLXquQf zEhP4(*GOrZ4R*)#;sqG_r>XogXlganMCY5Vo)Am$<`OeTo=Uy~YVC$89S7nTCe?4W z>d*7Qq08(0*EkN9f6rjK*=iuO*+LEgSDO4%=md9ygu;6Fi6y-Aoy1G2dkh?6W9m@E zN7SPYSvQCUh&rHKpct8`G)3oogL}2PtY!a_%iQkOv1>TX8GOsE&8$MRL`nw#+23zz zd?+S;?C+oNC(GaTJDhxyb7ZxeCDpU*#{bdYdp|UleE-8C6h%Z>Tx?VeARR$KK#ID; z3P|rI1d$qw^iF~byj>M^m5zXmpp+yCBy>XA6$C<1gg`?bPY+-WBTN{XOOxEWhLiCs~dczS?p)XK>DfS(#qN+>9a%L<6d9^56 zA+Vvi%H?2gJ&|f+wrtOBq6fX2XUtA+TzTW%YCe`Mv!VBRu|-grA7>8? z(U+5kRXM`)`y}Lj(jTbx_4D)oXH<0#<9B8odVtJHBJ&;uJe`n6(Gyh93X8viE~Se; z3oD(N{gu%3ez>K*8-gBTOz1Yd4;4H+CuQ{A8oQc`A5e=eWsTJJ`AHJnICYAX$!%WUs2xtE2o4-q)fNH2d6{fzqjxKnHNB1Zlyk;?L+^Gu z_CLV7=(rlyL}SlgFD`{FM&$=67!c^xL&k}sZkFBIhyQ*MliQ3J`n~&eTg=*a793AM zD8qTxL!_uXc~$mERhUR9X8TrAkcY7~^jNa_gY~V)<0vBL z(Mqq{k}R7WHWrT_HzK~P+{!hk?$*g!br__1y`8eM2#5hboNDYR;8@Vv z#JPC)WFWbK7#WSd&|r8E20(^~6-A$!z3(#p!MbMlH~Y=^T{Gq5HNM}S1hIA4gg}Dp2%R2UZdQuqbsb($tONs zHW(zEZ46u<*d7$dgBnoLCGD>?Jz(Q*cQ7tPQ@37=i@==Xv#8bG9!&8|btn3VSg$x%@)xXm&%XoezX9_;XT)EB} zz4BoyZ}-il4fb(w(^`FYjZrpfEl!W7VdvBtrWHGn`eT^T&dwIL6@`=tI8e6v`TDY{ zA1nf&{?Q-wv8X*X+l;k93Xs{54fd(MJc4n*Q(m@2a%wVbZD(9M=^Tq%pO0u=!eg1+ z#uEA=*G-0M5{BmLeM8bK?EZ>*tx2uh>cLknL>mtDZ1)_mk?UwSbE)9kH8KoaL_y-CJ4w?6VA{2 zOR>Pk$4^7r`<}@Z(q$;DnzRp%rwqppoqgQ|A7R6_4biYoY0stlSYPEI3qF3KO2%K^{$%M@LsUfPQ@ZWL zT)p*&srDTGJ1E?!zgg|zqksyrqg_LeWeS&L{bF*fI_}7%sidHYz>F`3*2S%(C zBh$YIo~fJ>Ssqox@;BMJ_R6V#U3cDv^|>bPcIh?Y z%hy>uN(V>V4$HROxi^#+c<~OYGSW3wK1UALJRCNTz2WgKe|Nc!<>y8Jp#Nw5!+jnPu6tD)q z&L*#hXZ7p*!=xeN=fm#zxLmV~IRyL14M`f#(96B6j(`0^s)dP*(!)lvZBng+-BU_Cmit%oEZrfrC^Xv|Ux1{u zOX&q&RXz5Wp?H$Zm6Z-O1VEg5?JhG;q2A~OV|LreeFEZsr4v=!?8kiury+igD5aw4 z(HnF^VE#9Td&aUm;Hzu~pb|kvhui%rH8Yesz-kxR`Qb=r@|o$Olvoxeb_!b(1e%7B zQN-z(C#j^qk7rYaT}7vLt>Wd{YaSTo?VwPH4Ij#|XM!#loM`#L8j_OzQP)F~ z-b>u^39YYC-_gHFsq0>h&q1gx1l*|QFI z>U}8#Jt(sNLkDHUw$epEWH=cI=Y>f+c+;0DsZ&a2cS*TAQbpo0!ki6f>Mx zMvSOoMWUH**Kyky|58E|$yqk7+iO&c(AIiypQVHx8?|&qv(&5dC5J z`6YpmjTSe@8KuPEb79l^f9eyrLvdREgN>lT@#tlY{?mqh-zNZ~{BbKVa@&k-JsHSJ zclRF3tuoqIb+>oo&>t}M$yaa}2X)tg=0Q@Fcz4E%zSnZzLDKpl2+ukItG=NZN0U}= zMK6$!BuK54An@#_G_WR0iTde`D0Fq-Ty==^w*n1->0dVFIKQx?g zYHTV!{kj)dQjzH6T!)>J zjW8Dg9VrAdZ6m6QsEj)LCy}>|()?t)!woMHS7ih5ZxOC~7hdJ--SJ6hP1Z-qmFB0h zFrv%roJ;g;dWlP8ekM0zZnmr^il}5;dS%s|@oT?tPv{3b++uw7^VEs9IBM(Q2b<=O za|C)~!;DpgJ=s2XKJ4neV#Vg)DpQ2$ShJX(Qfiyum+3=@?Bl;e45%k#jlZ-TVIOEN z5z_Q4I*VZ{3^YANnrwzm>26Vl$3JQZQLQ14Fwz|SI*f$^S&X3R! zbYEgTBfY;s^x<>`!dWFF#0*O4v(c+(fMX^=)S?BjDU^u{p<2d98gGbwkm~xpfiESN zB1ezAazqkvkCX!-4^}gUHYQLT3tp8(#kt*!d{?4zyep^_Qu85QyJ@`Hn5GFUf zy8E+8PTv6-WYRYVok@&LFM9Mm+4Kk5P8)Afh=f@1N=<*L8w{@( zNv6}93)x0v*lk}XCOz165U-=WkOyeobc+55nD5)5j~^P;V6d?(&n6%QBuzXh{5bs0 zOc{<) zhFi!&*!qW3Ugx8l?46Ky4NKOWf1Z2sCk4p$teFQ0u@s#r(GQx&h_Bw8X-gZ#Bhj-B zQ6kE$H}F_9-8{Tn#rBRdcXo)d(f!76`GTeIAe!iLnmk%HW1xqlx%TBFP`+P3$R|R) z(K%&L5;_MiAx&ZRp#I!RYIYC)?#q5ZG&_P2}L8=`X<=gb^+p*zK{todpn} zY;K(}LMKO#T}{VP^k<@&+p8D~l(Z6bXoVT`aLQbiY2PP-9VGK9EOI8YL=H#P0(4_!G%Mvhm9kw zK*wrx!$lBAYnSNooVRJzl-iTf&a7zX?u6{GuGJ=Icj{vf#mt8#$qbBnb4*J%Y`P=K z&*9p;W~E6rwb)Sj^8q}tGiX2W*RzSSa>Kz1)v3d! z5_RjsMTY#zc|pxE|M1PvZxT%IhKz_W&z@ZfuO?jx`~68}m3y`On?FlGSIwp^G~7KM zzp(42OED_GpW*r_ekb($3`)6PcSF>p>0vaHKAd5;*(ZT&jb1&PJ6Sip8Z}-fUa~7T=l%nw2vJ&eo>yP75#jYz#3WQDV61(56f=HtEQ8usUXkG+ zDh@rYw%pyEA6wQ~H!|!8&)yV4VXYhstvr^-ri&`??yvLQ>AI zY#skG|B7+Xk$5~j@0?{sRvAo@^L3-xt=0Ssus%KtIMMRZzv6oMd6qt}ToY7gRr{%K z(Qjv})J_dZ*7;8>oRhP>Sh0IU|F;Z$R;LSitm;|af`73ot-}3RsA~ES^!b&93dk_G z5Sfl&x_7$z;*TY#HC*g6e1#j?5+Td%a$-N|`TSmFhOlH#zEFO#&T-IT*`qE8-og$s z4h$?asc<)--^)KYpBT(b7k_W|CW90}9(^6GVYE-B4BPZ@sltpMUS+yZ1Cs| z0+RM>O*na58blRPEmI=Z@?@MMT#+I50mB~HW~A@4yc3YXg;Jz#SX9;6*B2P7+DejP zDt86rFld5g`gxyn6Qy9KR%@3oiqus7X#M$@P<%rLklblVVVl{BH`vuO+oP@b7uNo~H`DWdEMD%?{2mH8M4c z#YtfK_4lQ&?IzFErN1-_zM>O1xKVLd!hHRHlV@k5X=fSd_A|kXC-nJkjMdbejD;sK zj`?!?@+{9kxc%clgQ&==is-?~f^$>5H&bUK(F?A?7`$dN$g%piOxcIJ=Jeg5@R>J{ zt;)SBUd9qgM(fASw%=Afm5EBe#Y&y5id|_LaWngS!5y*unV<_g;sdS{)0UIHp>$z; z?5On?NoB+$xVz~oe5+iyfWTdQQ%Ni2y~F@$B)nUyiRsBNt|LWqc-!U|cbR_aaS=P$ zqc&S*1m8FYJ~$3@j`bV3sfCN4ASG>QWunul6V%fH$|`wZlwKdrMgnP?n>_#Vbufw!PDP9x#FTY|Q9vKEXUvUaO+VZ8vd8jfo4K7Z^G3AK zE$(ZX@`auBj6&*zy5wA~3%s^`;+ov%j?kZ?tC2f9R|Ki5OTT*){4;M*nne&5o%G)q z+5@xG*!@na2?9|6?sZ?-;$-6itWcon()@PtQdZEDN6=_DPWcPjE0kSBGlSx#w+2nf zvWkFgm-Cd1!Sc;;&=D)OCr>1bUeN@yuO|5iHpz|>}@$A974i= z({6bVIL&I`ZR;(*`%A2(+J%fvfS#RA}w}Po8FC-GN`hTcox4aom(xoJ@=FWU>W8h+2sE1M^=!B}r-&?7= zi?H0_*{QO48M@+Y>`nvWn$397h0P|LsSLZoGax1!g*?iKi%6{Z(TvW4_t_@{54svni(9&)w9%lw?kEoy$8rPe*VQ8kY=IDd z8umJ9vk;^ap~?(tt+qw{$d)jbgD4GIfB8{?KGsw2OG>bdnQM1xRO;I9Bs{&hJzuDN zG+R6@->aTCmhsPoIo0PuGeane{!RP2AA1gl?%U8l zE;|bLc0_tQXC%H=D!drr?K#K*Ebp{M2(~!lrB@?%b9K`4Jb8s=oY1=&B*m4hI*?qR z_ML5IAY@9%K7AKXo=IRvSPe7$5*gbBcivcNfUBf(((G_Yv_cPiUVQK|Hb2U2x^vmT zzrpKWL8JO)7(QV1+>bdz{06cs2sugN=0CdSQIAJqvc~VNVKyClM9A|GmfNeuuiHd z69vG_1-pDydNood$6ZbafFE2JdbRxLW#+$Si}MO1KF}XFMM0ARu%v~O>&q1eak0x& z`JhJYO8vKC&GZ;xN-$otDw^eeagWqUneM)wk@8BFvQrtcE}<+^10-#!J^?LKw0pVZ zzB}a{O|r(gdDug0jrAw(<<_jW0ZNmC06gl|HDF0--}wRD=KDdb`uChtn2iw)z%sL} z{hQ|g)!_O>xNwKB)SJopqp=r5-_2;Z(UkfYMowInGlEyS{4zzYj%i#oxwNJ+b{bUr zL~%`yku(@~pTPHd)zeK%{pT_T_qh?j*r*fO9q?}1i%GXICv?aoUU0lxzfjK1{D>cS z{V`TpBTuCwt!Wm(MoWjAPhu-fT%M0UVWjcCvlvzpeMV7h?TJgq8AowpN%aGU3TfP7 zTDcd`==oF^w%#`D1_>5fU7~d|bjq?pYAXH9vzG_ceW%!+JLA`6)Ho#RC)aDw?tCIn zaZhbck>PIhv0vY287<~%Lu&yGKis*#7Unn?q1--sPQPZPVfBT=86l6xxCo2f4< z+&Z$+(}jijBGUkx})jfl~U^bR!6?x>3Nf{m85 zWZ*sU2j4U@ozue;lb(W_W>7!Gc?su;jpPYqiK-STePcUXO^3l*Bhl8|-~xg!AW#t1 z9nNwe=}G5I!2w%fbF0dZ7|ao$HGrHd#6@rQCMe^jeJj3OXDkd5UYHI-H@GO-&&j2(6ua> zh|azv+Vy@-Pt)!wQZA4bmGPZjft0s@A^oL2Snk-deoS=?dge&H9(t}JL7(#YmpYLd zk-^;Kv{mC+`VzEVVR*O7t?h2@hzQO8W=K2xnDXMn%X!Ef zH=TG zi&AmE8(%95Qr*CH622K>#ffycO8%~Fy+kbWVf>*S%yQYykk+%V1<$B?TF|ds=S4ge z@s;!IQryhdBBFJ zwOW+6EOlQK_T#$o|7^U+FNRh7^f#CCwtwH6jgUZ_Q)64@JVm7|ytM#TGI0JO`M~+b zu!-~P=6M&x@VNH4GV=~ZAYhaAP~1pQR61+2onA+gl4prMm--*;z&~6fuB>8QRrB}e z1iz`N`z_#Z#;~rl=Y)1%&1n1^x9aVf*@Ws^7u#1}^?Dm!jlh}MnCaK4$WzPrI>nk} z)6|c3Q0FTWJ8r1cc+20t)&2cqk-ZHPMUQT6pn?mN3u2!<`cY>N;m~G0i^u({Kwiz0HY1X6zfgn9X*5)chV<* zfFS{MC~X>lg)@BjslM&VX2~V8#!b6Jyty}4;J!4ZF5_kR$u?N|U_(~hjD-OQ_w7Aq za70TL0Nc9IBJix;Wl(=EmJ!oHbi31{CLJ9r-LcjFI@^v)nLlkX=Uy72{-;oJ0Ym?=&l2PxEU{k5G^fP<3$#?3q`i_ zwkFJ9p3vz7Y>y*^8uy;&2gn)9`RCLiLV!4L{naE8@7ySvu%an41s%GEmJPkYAu*(iT%4N!zrDCp@!$^<$2-CX2m}W5!bLWyqt_12e zaiQ^RV!2;AUF_{lY7aEn|4lAu893J^YbzhP9E zJ~aPh#Oyas0jS;(KDk!&QckFOVwwJ7fVF~hCki6v&)0*14p<8OrTTytU6nbsQPuWR z+C>g$ksnrD2XoV@$^Y8;k;$I~Cs(hNClWk}_O~a40vBX}dAdL~KtB(fJgL{h`D?Es zq9dfmca4%dn#vPi&BtXi>ZBm#%z-!vhUg;O>U53LNBhA4cuQP2iP z&m-5UN+;FR8Rg|G#vtE+eFQR5DpB6JNNxGsRtbuZUyDg&_=xtDoLrRgOW#@PK-{mH zI}lei>U?`ZE&qdSu&H2JN^^mUR1!Pvn%d%#6?3g?9%P3olU1Qw1R7Cio{v?XT9qDIVEW4$(V9(gJpgLn{Hl)^2vP1yg}oHO2U?QajQ(m)QaA zT3PQd@+BTRVLTs1Z=H{G^8BrKrE@#c&QJWSWj+XnxdDq5X|Sq4kb^u7n8mD)^g0r@snWt8)(YkxUyANJq(VG~$Ey54447*z51BtC zmj5~P)~G=mA_ISE>E|17l30u#+mo%dcje!&`1I2c6v z3TU(LW{E8+=btY&hF!wGz0VC_&h8%(L-5uG;(ou~-4R2}mD0By`}ICl=~-VNYR@Z>ix;9_Y63XWX3zq9R_+3>QF;|-0a88* z$7fL+_-)qz^}-d7|ZK?7lfFwdHR#sL|T{!Or8 zLV)`UKy6j(xPmEsn0mnbY0?R_;aDlgCDTj@0T4i=WB1V7pa*Y*&yMHtp<_Xa8BbrF zwX|Yyji;6Lu{~tP-f+)-l2E1{mjxcr`&o(<`wG-}t?p%}fDi(B3^ZC`Pzmf938T;U z9k4J5TkvT?_A(BLccDDdga1N4f}rg8B5{MF!iZm9m55~T0XyoXh6;Ajy1>1XwMA3h z!^if39edNJQ?Cj@|99BW50w4OUfUHCo}tCh_A1uy*o@pnoD@RvUoo1~A~46K2_wuJ zcK1E_eJ=;VPEyZQ0x11if~UZ-tiASbJzhB?tpy@HHF(P(6U(0s>bb~^7e*8~Yiojl zOzr=6ksn)DEs)>HswT^odtPS*tA6&KUrbdh0euvdYy91BYhXXr`DY6%sP%CI9<7W& zz>UYj7C@Uo6vEp5DS6O{Rz;SH#IFea&o8ZD*Ch#@Re{|*7+(IfRWDYAJrcGK&H|ko zUhtC^PYM)dquy6_`FCpvb2% z?WGkPHC%WChXIWP_zgYx3V14W#T*J2LIA%(8X~R;3t}x-Q2DpLPX6Q|yg$zMw)rHy z_wF7)d&t&-GEv4`QUK}ipCk=F>Dsr%VI^Ux)6bd;Tm;s3>EQ9>p}V!)5=DvviXh;+ zPyNx_>3JybirEM-0-z`Sz!-izx<8&4hAvibOF;XD5C8?FQ8RZGX$m?rc@OQryU+IL z0RI#JapOR5zwtouF&#Ou1;5}CB8q8k#A*UJ-g4Rs)^vti3nBP)4eTyMi$BCr|1+D- zYz3XGU<*F|2swAIdKG9{qmC38_|lr6?DWZGmtM^mE2G^lT6P?Jgz8>zkBe(>{w`3I zO5F(+C^8UG?0?VoM$8C1iu1}3cUsQVgA;jfNmT`*As^3{;a@`y2Bu`1iYUR9>sE7K%+7Oiu?ygYUkS) zqAv>^8)+wUu7IIhd$Q025;~XoCRMDrMsCw|Q9-9w2*EF{(F#P4&j3>8*v!1TjnQs| zFch-)0F>8hW3=@rSm#4+Au=t<#}h;;{`dPqpGG(Gn`k@Wad(mkwHXW@+j~GUVO4AS zD$#pF?2BfFIDhy(guoX3m%Ne!m#211N=~1x5H*uQ2=C$1B5G2q;Cy~#HCt@%(>Nxe z$S>QnY{|QiItuP@8VT+N{^1IUS^e9)pzc*;^i#cgZ-i0-0g-kD^nXwMXr?--@_DYn zVV<*f5aeM2wg4&u9s6zn{t;>~LzIWeQvP?^ApE6-R=fWK*+3cj)%;Fw91=qCi|YKb z%QynQOjOz-!vh68;=mSs>al!DNdTRCU))eE5aa`t>bQ$ANhpljP>`-X-8A-6pNBZ) zxR;u$G=7^*1PemH11~$okMIJnrB|7K=3GZrds7#LaP!h#r?DjTH;FH2_(7^bWhkM2 z+8r61zXRTd`DX172=JagSqH-2ASPFr@d~R~FFGKEA8oAMNBN~Pz;S!*2g0gl_O}zo z1pMbGH|l^2F9;~|E41xTX}pyoKzS7A3%$3;B2XtOjj~oL9X_v8hTax>pbvYf5r7>c zu&2HGY^x`~(mzp^_v1BqbQ&1^8UCj$gDv>Ci?Vka5HSG;w+cLJQMWsm6s4MaNE#7X zC482D+jit@l=iZcUnAvMcxx9G64(7r!ov$}!M|5jBlHUu;>Ty%M)8Dai9bveAp#z5 zKW}31BB;B8sxKjK2-V@#)h_$`4&j1w{eM?}XlEJFCg=?~&?flP^$%Bsiyk#>v~K+2 zWC!;aun<<{S09dU5KH3v)j8b0_BK_Op}MHhYb>yLr**RT(}dUUez#@QGYxZF=KS#kP^-wMJHhwz&aX|&>%Fk|_lHzuM7K2G& zw}2<-b$v<6H0qTETL5)|ijHy?x{nAQFoXi}>X5iyQmPQ*xe$VXOUK?tu;20}1Ut2^ zhcp*B_All5FZ$!v(X`*Z9XeF}7cv*TVOw9fMW&mm|K@OoMz0#RxGBYN zmN;ds7lXwZA4aTa;MISaBSe2P<9%gmr{LX1ulm0MK*QC+rW26W%uf036# zh^zUE-^$E2m${|Z?bLwki_wXh?S(W0WH_+W>qvtwfNunO#D$8LOdDyFZQD zCLaJzDD6!y)GM0cJaBY{`x&<%Tr45Vwd;=4+?-fB{C^_9(&jxRnlDuXl@4A^!&^&k z7K8OpZVDC^2Lnf6foylFQbOgdoa(O6V%247*D@oVz0-R>^B`hXS#S^;Fbnew`6}ixb>VDM`a7?BLYnaZ$xGsssH+So;w{TC+@Td2m z4p%-ALNxx(?rwP6$wLA4j%_Q50e#ZbAbs|rkI!Xu#8~Q-Ir?m`Q_9Zosyu4cuORF@ zZ(cZ3SPxhp-#bg>uTStgq=YgsPxtZ2B*G}%kQ=Yg;B3=Y}sHuVc-v)~J;@X;? zs^tC(stKWfuil~P^Lw$tqfWs2c+r8rK{s$8(1S&lErHkL7ru+`Kv2UH(6^$X%=L$* z)?1}8F_80*;lzUVrYpk0suHG{^jTd^$WVQ8p0CoZ6$)p7egF!RTRQy-Oai3LxNT#T zyj2YpJ*Ir}V-?W*r{QSp#!%uGV6;2^%_IodD}l%qLiBdHfHPRmKv=u2H7NtK>6Qiye%-qyRd68YGlrEty0t zwBF+Kyob9J>wwgzK^yZ0#>Rk~+@CyNeB`3ia{J+3?8c6{~{$F5d|F_4;AdvB%nhVh6{y$Lp|Ed#0 z038Bc|MlH}jPmbV_}?V^Pon%MKL1-Q{ **Note** +> WIP + +This crate contains an implementation of a solver for [Optimism][optimism]'s `FaultDisputeGame`. This implementation is currently +generic over the `TraceProvider`, `ClaimSolver`, and local resolution algorithm. This allows for expanding the solver to support multiple +backends, such as [Asterisc][asterisc] or [Cannon][cannon], as well as multiple local resolution algorithms, such as @inphi's +new sub-game resolution mechanism. + +## Solvers +* [`AlphaClaimSolver`](./src/solvers/alpha.rs) - The first iteration of the Fault dispute game solver used in the alpha release of the Fault proof system on Optimism. + +### Rules + +`Rules` (see: [Rules](../../README.md)) in `durin-fault` are defined within the `solvers` module. These rules are used to describe the +expected behavior of all possible state transitions that the solver can suggest to the game's state. + +## Trace Providers +* [`AlphabetTraceProvider`](./src/providers/alphabet.rs) - A mock trace provider for the `AlphabetVM` used for testing. + +## Resolution Functions +* *todo* +* [`(Planned) Sweep`] - "Sweep" resolution is the first implementation of a global resolution algorithm for the fault dispute game. In reverse + chronological order, the algorithm looks for the left-most uncountered instruction in the game DAG and compares its + agreement with the root claim to determine the outcome of the game. +* [`(Planned) @inphi's Sub-Game Resolution`] - @inphi's sub-game resolution algorithm is a new resolution algorithm that allows for + the resolution of a game to be split into multiple sub-games. This allows for the solver to reduce the amount of + moves necessary to resolve a game as well as enforce incentive compatibility in bond payouts. + + +[op-stack]: https://github.com/ethereum-optimism/optimism +[cannon]: https://github.com/ethereum-optimism/optimism/tree/develop/cannon +[asterisc]: https://github.com/protolambda/asterisc diff --git a/crates/fault/src/solvers/alpha.rs b/crates/fault/src/solvers/alpha.rs index 7ddad78..c239bcf 100644 --- a/crates/fault/src/solvers/alpha.rs +++ b/crates/fault/src/solvers/alpha.rs @@ -189,6 +189,26 @@ where } } +/// The rules module contains implementations of the [Rule] type for the +/// alpha solver. +/// +/// These rules define the conditions of the game state that must be met before +/// and after state transitions and are used to test the validity of the solving +/// algorithm with various resolution methods. +pub mod rules { + use crate::FaultDisputeState; + use durin_primitives::rule::Rule; + use std::sync::Arc; + + fn pre_move_rules() -> &'static [Rule>] { + &[] + } + + fn post_move_rules() -> &'static [Rule>] { + &[] + } +} + // TODO: prop tests for solving claims. #[cfg(test)] mod test { diff --git a/crates/primitives/src/lib.rs b/crates/primitives/src/lib.rs index 1c98113..21f63ed 100644 --- a/crates/primitives/src/lib.rs +++ b/crates/primitives/src/lib.rs @@ -12,5 +12,4 @@ pub use dispute_game::{Claim, GameStatus, GameType}; mod traits; pub use traits::{DisputeGame, DisputeSolver}; -#[cfg(test)] pub mod rule; diff --git a/crates/primitives/src/rule.rs b/crates/primitives/src/rule.rs index 7ed0e47..ea4ad9b 100644 --- a/crates/primitives/src/rule.rs +++ b/crates/primitives/src/rule.rs @@ -1,7 +1,11 @@ //! This module contains the [Rule] type as well as several helper macros for applying //! rules on top of one another. +//! +//! [Rule]s are functions that take a state, run validation for an invariant, and return +//! the state back if successful or an error if not. They are used to validate state +//! transitions in tests where the various solvers in durin suggest a state transition. -type Rule = Box anyhow::Result>; +pub type Rule = Box anyhow::Result>; #[macro_export] macro_rules! chain_rules { @@ -19,6 +23,7 @@ macro_rules! chain_rules { }}; } +#[cfg(test)] mod test { use super::*;