From acb33e2f41b87837e69fba4822e5e032a3f52081 Mon Sep 17 00:00:00 2001 From: German Nikolishin Date: Tue, 30 Apr 2024 16:11:50 +0100 Subject: [PATCH] fix func return type and pipe --- crates/semantics/src/expression/complex.rs | 58 +++++++++++++++++++-- reports/main.pdf | Bin 1016330 -> 1016321 bytes reports/main.typ | 8 +-- 3 files changed, 58 insertions(+), 8 deletions(-) diff --git a/crates/semantics/src/expression/complex.rs b/crates/semantics/src/expression/complex.rs index 5e46a0f..eda7cac 100644 --- a/crates/semantics/src/expression/complex.rs +++ b/crates/semantics/src/expression/complex.rs @@ -254,7 +254,7 @@ pub fn resolve_func_call( ExpectedType::Concrete(ty) => { let mut error_return_ty = false; - if check_func_return_type(ty, func.return_ty.ty()) { + if !check_func_return_type(ty, func.return_ty.ty()) { contract.diagnostics.push(Report::type_error( loc.clone(), String::from("Functional's return type mismatched the expected one."), @@ -811,16 +811,66 @@ fn parse_args( fn check_func_return_type(ty: &TypeVariant, return_ty: &TypeVariant) -> bool { if let TypeVariant::List(l_ty) = return_ty { match l_ty.as_ref() { - TypeVariant::Generic(allowed_tys) => allowed_tys.contains(ty), + TypeVariant::Generic(allowed_tys) => { + for at in allowed_tys { + if check_func_return_type(ty, at) { + return true; + } + } + false + } a_ty => check_func_return_type(ty, a_ty), } } else if let TypeVariant::Set(l_ty) = return_ty { match l_ty.as_ref() { - TypeVariant::Generic(allowed_tys) => allowed_tys.contains(ty), + TypeVariant::Generic(allowed_tys) => { + for at in allowed_tys { + if check_func_return_type(ty, at) { + return true; + } + } + false + } a_ty => check_func_return_type(ty, a_ty), } } else if let TypeVariant::Generic(allowed_tys) = return_ty { - allowed_tys.contains(ty) + for at in allowed_tys { + if check_func_return_type(ty, at) { + return true; + } + } + false + } else if let TypeVariant::List(l_ty) = ty { + match l_ty.as_ref() { + TypeVariant::Generic(allowed_tys) => { + for at in allowed_tys { + if check_func_return_type(at, return_ty) { + return true; + } + } + false + } + a_ty => check_func_return_type(a_ty, return_ty), + } + } else if let TypeVariant::Set(l_ty) = ty { + match l_ty.as_ref() { + TypeVariant::Generic(allowed_tys) => { + for at in allowed_tys { + if check_func_return_type(at, return_ty) { + return true; + } + } + false + } + a_ty => check_func_return_type(a_ty, return_ty), + } + } else if let TypeVariant::Generic(allowed_tys) = ty { + for at in allowed_tys { + if check_func_return_type(at, return_ty) { + return true; + } + } + false } else { ty == return_ty } diff --git a/reports/main.pdf b/reports/main.pdf index 2993fc3fac8abc6581d6a45599c71949a77d3065..c4e39d0881abe818bf1844cebf30329fda3ac181 100644 GIT binary patch delta 19288 zcmZ|01yogi(>^THjR;61NcZ71rKCtGUDDm15{K?aID&+02!NN}r zI8ucalNE`1OhAQL8^-}Zr6^h_XH+Kh<0c=vix{bpvhZMl=98wR==cb%0xgGQ9#H?< zk@Q-vTdE*4`nn-bcUiTuzkI>;ZrY;b-D|^XBO*mB&6`1-WWK8R_L@^^Uzv~zuGTRi zMeXj`l(M#wwv(w_PK<-@f~!Vhon=8fI6%@u0*k0pcfo4}N0;_Wn2P8XIq67{4wh?h zMc+3>yJ6lbm&02phq;^HZEHx0NbudJjV|5dG^eC{{vVbMPSe!N!XJf4Rdm8_5ut4}s6i;5S)N)F#LSd)2S8ynK&X$*g4<&7EfbnUAky=D+#S^HG=i!Zo&uJkl5_mHeIep*<`Q& z*J_TfS-b%%{=THFt1<&P9<{SAY zrS)fLN8AVv>v0MC1L^yX&NIRleJVXY=T!8Z*zqR4Cpo3*L%nv|(S8t{C=Ehx%OHn_Y0YX}^QS|)xb~`7 zb3W-3M{@yAQsV;GnHNj_n(VhndO3|DoXM7NYmIk*rd?ZIVaID3(IUt4i76UZP6=>4 zut5AkK*O#*VH6=YT##P~f>eG%*n~{*A|z;d_<}H#02{&&27wxuLkM5t-v+^ccK{pm zO&lRLg1q}_RQ-PUXfAe`dq--x@r{3Yoy@kRTFl@hMnMV{yVRF*ev450bSE^M9Rusl1`cW@2yj`gPg2_L=Bj2-QwyvQ{ON)8U@6%e$-u8`v^I zvE-c(b-YuH9887|g1vN#>nBhy&&5wuo>P}`k%%+C!cddY)}8^q;lcG@y{U~FCwtEg zAt>_smxAX0Oxp@w{{^w+XAdcN&emKQ^a%L4$aCtAR(h|Rb{t+Pu*&PWSGG4FQMNRH zJ_G-}q7xrl-fZZ9tor?#;Ezus_XtmYT`Ldn4hV7s?tNcB?YF5RdirdMTm_p`hJ%{^ z30@FlD@;~XP>@!erSq#%X~I`NK_^EN1~PBf6VZ^XBldJ#+ycuW>`Mz><@)uH`hJ(f zkK&Fub_l=t?x)||pU7;V4nH5-V9-2ERX9Cvy)c{IpU-ERP$P7~ePo??t{S>vzqUGksD67v3M8 zB0N*?f62PDZ!)GY^Ce%N)r&fHVj26fK4ppfT$QE8$2 zT?n0tH1(m8!bj{i4Aut`!c@K+SUoN)xrXuY#c@(+y!(*Uhq9ElU3(1gRx629ZlA!*B@%C&7$duyHSbZr<)>bvZZbsrP6)*k z4jJe-jz-`!fk~=)TY+zUm7}-<66Vdvskc+o%Dzwld+Q8nI+2oG`7gaqJB)_CR(27G zy@Ac&&RxR4j~^Qn9Zh{uue550OC3jT04!tcKJ?vcFl4;M(@LdFPfjGOct_=A!~al* zgI__~jGNY|#Crf7(^<2n5>QQ~!-O@jYxf2AAhASq?c2s_GwpR0NhDqgl#EA|K7iX|>Sfbf2!xaAd*7L2Zj5meP{SAAXMd@t$Hj z&{}Ud7C7jG^nH2wM~tbV5c+s}P+8yj26-xF^;Ld?P?3hd%~=xemhi6c;)OC|!1Cjf z{*x1vH<%j<)Fo!PgZ1-v14{v+(zNkKXS{lJJ=l3w<~c$VZ4a%oz|Ibj``Z+!D6yW! zkUoWMFknpYMmg{M*dl&3!vnqaQ@i-HSo>ut@wC{6)zru6i<20cl)NHg>uFZxW%-we zkDuY#B0ni7alL)2kP0z~l+yTw2y?5v4QW5_n{rwuAEM69p%>sCBZAC%XQhWvMhJNm zdGQA)!jmaN!bqcMf+CY}KT(t!hwNQVT^Z;v(vZZ?O2@W~?bX9(I=!0^0PJKG!-cQJ@6a3jvqLkuJmW(@?h@Pp8@}<5= zMve|uIBVvM)IRQ!dA#g_ggk7Kns}vyCc#9&d zsDwEosb8GD1R=k1n5dle(oCAEzjhPAhbQv7)fRWe9C!G6_-R01;2fAQPt%^~u4 zs^&JMzo_qvvf8ab#TTg>LagBO!AkxJV_rX&pcrg#d zjEGY7Aeq5L3%8Nt&084HzDf}mFByOMq5e51BiqSpd8_IHV7DX13e4(_xYI==EKJz$uP&@8ci6VxEJ?Y^?#>r%|wN)T;HBGL4m$HAu zX*{-N@u1=h1MOT`gb*S4gyH$^*SyJGxAAdPxCv!q@a_mR%9s?TumMLHx)Q7-m@jr* zUk`8PUqHeRXGkHlY>||r7>OEL1X=hJXAv6=B7)qZ?{FXDus=NFDdamR??{mvPA`pp zvoKkc^)0<)K-D;C=G~OHQBahK=7TQvPii;V6zre&k<9owl;OuIgs5+#hT|0CO-&3K zvRZ|R4S9QymsTgcKqVoyX4bkArID$zrjzA3Yh zeRKlgm{Nai4X=@yHBX# z)hTtRz7xTddg7;uiIZTtTeGPW-djBmlwL%SUJHK_eIPL8cU$A_gpoK+2|=)V zGYMNnecVI#kbCJr859_^yXP9s)PbSX*qIK=gBLAt3WTQW0=&S?vM-Elu&tT8J{SZF zw2Izrw>Y%+rcABmC&)I4sJ)5W)nyx)CGaZZ>YY`@sw!}WA{22O6d&j+M z1(|Zs9Y;EPBZl>Ajpy_Bh&y37b#CnU_wC8o`z+4f>vpUp3RJH-S5x%w>BfhTXzkr= zIJ@o$O84c1^I=1UPiF#YIi=O`O znN5=3uVn24k=X~t{D`|F2jow_{U8zXS`LPdC`tqmf0St7;@SJw^g*7l>5VQ`+aw$& zXtZFSeY2ihx1FdrZRg%dD&`8ajscFk#mBOkx6~^blLE`1Mou}zOR}XHm`+?sh~O&~ zh`kGi4K0^9fEX>pd~DV7>DQ|e{uB0Ma zv05QKd!7UkMOXR)#njLA&=gq)4KuM;M^GZq=|7wI;UTdz2I7%%*aG92uU=gs>GS2~ zJMuIN3-4L3Je)_vU({kBYi6jJ$7Yqc(e@?b!bznUjsxTl=KF$Fl&(A6>8>9}EmO+1 za8aBE2;AmOrFGHbWM+3P-bYZi=8DA5({eXXu~oBZ;=SfHbwgYX*#Opc+;w%rbtktEGcRV(sKUh)5;$4c=K?$6o!^ng_m(KXf1apD zc&TDDRQ_mu2KsIjQ5?*rvx*Gd_Y!6-%GT(7Y_|%st>9eMAWW6XTC>Ypl824p8>G8( zo0`&Ky9qA#5PtQ1aNebA;X&h1c&A{AR4XqKnFmRjZ$wb{`?4ir4yUTa0Gi(Old!yU zlGL4E-B!G>tGqfmN?dPW78c@V8`(cK$<=ukI4fnYV`w7oO*UcujIuv4LZoD}yU2;~ zLPIcHN)h%!J^m;85ra|cz4vs$S8PQka|Q!_zXnaMh6x4(mAOj5mBrY;llNe<27HRJ z=sv%@%Nqy`9VMl&sm7u*x|^lnd{R~N^p*M!6xcD^d|qHq_lT$C7AH?S%v)uh*%|h( zp3@&;ZwmVQ3VD1PS9Ut^oKc6EDA5}ygjN}`x#y;O`F!O11v73D$VxZ(kk;K5BQVxG z%TC}0*#l|iuu|p<(R~_`2)#o=ZI?8zYOA;G*C~p~&S~-*Fw${Q_Xg|dW*rfcmU6k$ zowUwjeZ8LMpl6|p6nWe-=XGjOtqBcOt7e9?D5hI7g%U9OuW0oM`XdB^q8whr-W3J*@)uwj;KFDQ_sob#wqW7i^d?~2G(nEo!Nwsu$Gm>0 zx>ggB7vA+ko0U}C)ClqIGv*WbBaN~*a$nUaMz3RqI@9#lFmQOXtz_klkxH}n&!J~G z6K<~}M#l#%?J0S*HyhmbZT6Oop7BY7#|Sd=%<%}d&zh@)DE*7Jn;V|BF`2Hz|jIn)25P@pl^3Bc4tuDO&@{9THD$#ANPbcS7Z=h1RKK6Q~LD971qh%w{^N`~0t|Fon@|^GZn;eNh-5;?1n!;s% z5+O7{AG4k~A98)z-EeDRP9<{mIKWq(>uc7-&y?(;e3w^B<9aet*4a^ZZCSby_lk72 z89dv1OvD6Tl}4`1+J%27q6Oc6jk5v z2<3l{C1MKjC8a1*_(^M_eZdm;Gs*{Hd{Ac0U~#~?PMFr*cEP(elayk=eruSjO+lNi zMyV=I(TP&9dev)EHMV`^JKL_Wi5r72a!uxhcn&dV`7ViLH})W6mYSh8RFvEnHf!f$ zz&1+yrYprh>3k+G*`9gi4g)>Q~d>WJ#AZC>Rue zz{`i2Ag{rwred?DO%AX9EFvthD4M#@wHsC#zd33*FUrj^gz?U~^ec|r&J~=5-HWYv zzu4id+Np5So`uEDUjFVFGwB@_5*A0b=0Uq>Ew^Om!lNM12_ID4Lh^)|4t{q(&ClNa z+B{O`*89HO-hxtsKSD&DP|LOV?o7EwwlCH_M3RPSo_uo_QOwfa=~x<3Q`why$S$Pc z-EJs|jy)*OqGF5Pzmt`xb*%|s^KKJn#3xa4?Ts2wx#l*lYuZb@^QzgR-lKG(2^Fir!m}b=B9O?K8S2jem|uQap4`IH>J9r|l%C}k z(LvVO{L|dYj0VM>3V?(bw0^5`Yy5rQ-M%Z%4^IYeJ_ktMAgg&vD3I2)Bt;lNq(mkm z8zNIvDSk$fto1_c*J#NQhAD@$U4^gNJzYEyzJkt)a`j9~iE8nuobC3?%nq3I9!Rn@ zGsMf{a%1QSw_E*+_?3{5g>)SC`Y$iZcCu1gYKxcT#S4>t%dTC9i)~k(eZbsbzL$|< z))6`p(f2?tB5Ic}WLHFmVKmt^hpK55C@Mmeqa0N z3&|_Qf*>JWCx!ZD?JAx6) zQxuBzPk0zRtTt|ou7o@pNS>*jv>+iuinnt$nu#MRbk*za*R723{pYn?_<5*@Zu^$k zhonsj>Jtb%6?l(Y5PB&|lPGf}OujT@mlt_5U;kj^mi=u1;nxz|#pxLE_c7&1uYYwt z0<)YD*uEqK5X4qdl{@&*Vu7>_8Hv0Qd0_;Tg*i&yKfzMR>!ph$PFeLm<({#O1=R_6 zn9WW7aFN)qnYNb94LrrmZE0~If~1rB6lZ4iwa2UI=RY0aRRq%4$}DH0=!8*#vSrMJ8juTr>(d?&pcgtxwX9RXK3<8`O^?3Z=hl@!j^Dx zzp~S0+Eb=R?ydPEEVWnm_8Yb@`(H#ADTB9PtuSjumaw+y%ab^2a;QE3p_!#G@@z|P zCnmbydy}Ef56aa7@6%M_X9C)3FZi@7bgX2Le&%d%aQ(m=rB5o3>*tele20k?ADMc> z-!H}THYWFJf;|)TN1#<)_GF~~JmQ7^qmzQt&{}c%r&u(Ry(!b~4@E!+ zu#MXnBYdj@jJLL5{14n4m>5ZRKnT}a2wB^XR#o||YsJHun#WKRDROAH=ey`R3q~)1Mfd%!*I{>B zF%&9xzDqWD3l45ak0-gU>N!($NWRd-uE~;K;O)AvOZn-s_twM3fe5Slf!)+cY%*L$ z77Dk5l{A&ieKf@i1D(69*bwy_S|r-+0RmrJhV_VGlquNGdT~mxx9-#wMm+!ManIDE zC~0r@m8|+JnA67esBniU?)?d09sl}^ot>5@%!PT*XpLUCmS}T85cP>lN|5~*Z+i8x zwC^$%U4ar#pga?Lz>~MQJDpmMr)~@fm-NpS2%LpF2Fl*NyL628d5w)I9qsLJ?)_C3 z_{KCn-smN@bMdqNXw{J7?+@2|Qox3JPgRNV zUrDJb&0_!Z|}#0j!~A7%BD+ zt)utNvv^#wxhevCcsz zqS846iVChqV;X}!m!WHZ)E_(<-_LV&b>i<*R4jZc61QfLIs2easyNXbbbrUYtf1IW z56T+s@$2o`x6dwXQQ3&)Biz_x&n1FX4aKjMY(YRaTnFN4+E5jrntBTSi;!(}ci% z6&Eft<5=sO>k_3jTEf>2F+$fRu_l3U#gfzwnrJF1EdW~29Ivq**I!}(Lt%qjB$gNm zO;6MQTe?cT@P;*~O_HH!$zyYP5>t50oSl+9G#_hN6*ry@i)KrXvzv+s|mNqC|$gSII&mxZl&*5Phka1{?dlg7s^dF|`4O!`cJ`VaDZWaKDAF%w*!4FM+u2aXm3y|*45;gfh(_$POb3%&@26*#<)TG^R=NbUjsg+7l?@*uppde zsW654&EJizyaVxRKwCzuXz%XRW(eK8!oBH>}^jcrM8`v@au#C07C- zUQ=VqC;e7&cxS0P0BX47CyJM=BwBLlie+Eekx!s@V5FySmdAoO#0e=CQ=2{HuDm4D zWvFjf=?}I^thH^I!eW0-D28LT(+rBzn}iXzU>71E6|Up>QRL97(Nc0X7uX_VYQN-| zb*P=}*O3w!1hze{K6eQ!j#Bw@cG_QKnttN$#SXLJwXysqy+~UDRohgz*5=SKOepB$ zwK?QMc*VDcjd+;4Rh$ZN%SUj!78ALq+8pj~(AqERHCHyNhItQUbsJ>=-iX+{viSKlfHIb?Y8tM{$6YoJn~_aABzQ2|CfWEo_VzY2W{)SY zyWD|}i&1|Co8$6?P9NVle;z4cOZutCXT*-}yb5;(>px^p8l*%oYX3+^u-R!S+P2EO zzDm*E*vYsH#AG|k`NHq}f(t2g{Y*-$@))C0D{$1-sG2m0DMZ=hF=cYZn9%3f2a>bM ztd%$Qx=(T{DZ z%YCZFp-J;VQywr71}^`${mPRxi( z!!PDwawfvQoac;CxGA5T&5QR>zb3rhUk|MpJ;0O3(;FLUlz?#^nZLKCU>nr;N>KLV z|HZL*YsOBj>i3iXyU1;Ql41<-|NQp|Vn|!z86AME?V$2|j?7+8FJpTpGgkT!D@NA) zT{*WYi@8%~=u56I;*f&xNiZzCSy(>U)fkNU07k`~4ESs&?M5crt&Y z?9V5gTjgkJ@-ZFS%XYl^dfY;0=YLiDbq^!CqjxcSKDf!K;V2hqu*>UCJJjphgIEtw zBU|yK05Z>CX?*mWk6dAm@~5zjpW@H`HmVlP8JG9Xuf=55zxtsp*$NGrE{8!yR#WFGX^o88{BLw(qB`@a zg}t~VqOj+V%_zih^D>H;;&Wl~CJ6E#Bxf9_=!6W}=PQlKf$o%T2^Y5QZ5=M5_b)dF zV~GWM$r(QTrtagmyKaM|r%olLA)9gLvn3nIM24(l+#bzjP`ygI?JYl5 zMDg)QqC{`AjD=47VQ0YbH_s@#fI{3=KIm|TvtTyY65EG~n1uj(4M$2Fu0X`|c5m{4 zewtg|nKl{Ns^0rSSo0or1)Vl!i!n3fHg-4*TS}{YE;t#hognrGq9j7&&Nl05jGU&o z5-?W#=}cYcfPA|)yl<_2+NczO&0i&QhENk zZhgRsyVcD`$^kcHZ2S=$iPMR2Do+xcDYq*O7ayvZUv46){LDsi;+U6GdU(jIbm7{J zRPYJq8;VRH`J`d1)W&6}Km1F$(Bf%n2F9+7_>;U?zbWlADc$q%kkWz9sOB9UiPDZ9 zSDi2AB3E%i>KglbljknPMfR329h1YHCvh6TKe^F$S2q7KY=O1n6v}6e7=Iup&+MsI zSwayd;>uaRtO`~#-V;TNr;TKNqhuhzsLi+Hqg;LJO6p2oogElfz7f&sfXlqqWbd56 z?U2bvX#%!4bOpzpT*yZ7qU8O$*;59?-)CBS+uG1xF~>e*K~ zFiLG+lD(Syo2n!f!}L@3&piQEuum|nYU-cX-tx=M_eq~VIc;w3T7j+kN(pQGzFtmo zY1S7n+j~yJ*tRK0H%`MB@REDx!MS$Mu(4L`2aB~gyGQim2?&+0($J*)N>o&?P$ zZnM+Y$v@4;Z1QijArDMQC=qgxxJJXUZnMyHD<`6EOZ`{DgE&G8rE_^FY%p>#PXM=uvT6UONnGbrVAe<>|q{5;c~n@j4u z=!#M!k*0aE^}*B_!$M`{;Gn09Iv;ENhLDI>WjyH~7ZLfWS6Ov@UX!s9iRH^Q*uD(V z?1(EpIf^e!c*Ayc*EAl{ROzu?vz5dt1ePIW4oZ~;Gi!EMe*N5M)tpj`F9kCod%|p5 z-pK%1k{Kn1k8l{ilCUiUJ(a?&c&liUc09h_o69fNXwN=oJYjCOnekai*nD0QsLa5% z5IR2<10~0R6sC<3?Wc2ic%8t8*1Vn+U~!DSPf1Z7_lCTt9I!!bnSZw?9uLhgq(8DS zSfhGSk2kB`tjfqS*po3xs%zk>qtopUFRPutVtWjOq}13o$? zPnX<39?qRr!*2>w<>5~50fg-KgE=L(!FpE^d7I5yN1J#lkBztk@>#qoxqy7Zk(Ba& zO&-lS=SLhlPgE5UiG1ulxLqmZk8+QPwh3;_-A#X8^{$La?A{yjLV0oN1Clv;tuR{g zRDUgV^KYG9#w-{0At|OjxWSCHEi<}JLX!t#IPH-x=EaDVs=~MD)|1;a?gOWk&vYd9 zsgzR}>M95oRtJ^=1?o@IO3uD*PO->Qg6zs0wZm0kD@{_V+iFUt)wQRXDKCm`f&`Fr zE|Ui7`g|O6t#c(OFZAS;`62F3(f+nFSjCumQ&sp^FF7;A-I=^+T5~NZH`Egt$=wfL zex!HzU^2khOBLNd?R+&=i8=cMUgXczbwU!ECu=Z6N!q_8knZt%?Vk>~F(;Wq98@}y zmd{Axw(qq{;zi(CF_M*pNMUoUYH-)X)vrz&9BWpOla@kwHC|31zwo>~dtHRR`s;#I z*^93O8ARuS!auh(_`$0sdeMdD?qDBVMt{WBr+q4H%joynJragO%+qVnotvN;zB&gJAg$VGeEp*e!bw zu_V4*KC-jNF3HV$;q%yZZsFIr+$E#0Of3()Z%$1-qG=BZhlZ`0=W;MV zF%t5v+oT9ytHeYv-zCYMlg>3^^RG{oAsy$mWVw_g?~~BO0hGuw=dSQ%Bdp)8{CLS; z5&Q~gEbsjU8_$5W=9Fa8Z3;)p?c^*4^3S)SSa)x1n5<~zYg6ky;5Nf!PY4#SofXuC%XdpEW##9zf%mbJU|#Cv~Yj<%MnRv`wT; z#mk+N^;dPLoKBwL*Qq%2$hA)X7Ku{wsus7tQV2OrSH3+p*xL5dTbw1EPe4`olpmr6 zWiGWI`rMuTvqaux3!ch|h?y^QT?My_UsuGxb+sa`?(v>JEpwU%xhVUxw`sR@97Ho>%fLS>hBc_oW9w9O-Q4n@Uzz%+UvO6pIurg3l@V*q5 zdC#%_acj^E+>kGIqbb33mW~MDbGC}j6!N1T$IqRQ2uDqRGzr79c$`HlUnKX~gWrHn zT(tDtGPn>0SsXyMr2{Q&Yrn)n9ieWsg@<1+UMa@6gXK3sX`Q7!02<9J{6u9sIcnu` zFH0aluwdQq(hUfOii?)MtXtu@dYIoX@Ohn*c|lz^qvk=>r~=16ciwTA!ue%A ztyZ3B;Li&=92M#2^)U*ZV!ju%PVI6Q>4Wg1T{A=?R1YguN!eBcET?Wi>KWtta?ts) zD2SZl8`Tmljdbu-NyzaGtBB{9#g?T4qE`Wv&vArc(Ni6hzYbH}#O7W`hj7ZoZT0+# zt|8}>9Zn1SZ}^T-W}Z)>^Q$HgEvr=gU55q_>+^h}Ih5L%R$G#qkNr-(`gy}*bmTD^ z-u)DAM8@34*?M3#QQjNP{M^RE;(}IS1uiuN@T#>7T184!LPAPKLypMh>&D+qFgz<)Pkb8$ za^7*_rNl^D&CmICf-lZ zR$_*`&xfU)gxut$XcE*#U`02&2axB%ez>_y*zatL$)cIcbW>6 zLOF}xR)WLw9akC=hZ2%_?=5Ry0myaiuLGN(kDD+6-4}~x6V%cw6kGEC9F885Lp~2Qx=Yyco^y- zTC)_m3{x%mQ!aq=8gZ5KuBz$I*5YMD`l%LVH(;(IXKRv0z3Ayi>fu)*z9Au+| z%R)%2oiPyX)Ay4i`USU}`~;&9&#uKb4v;I`>319n`Qq{(#Ek}0o`%YnwZ8mf7;O#E z`IOTgo+QWeU5(UY43pNSFbAQWeq<$!0Jz^%5~NG4!z|Z*G%@ZQ^XNbxSVj)4Tw*!* zZWUCIXXpQPpZ~KC*6Vyytx3BU&xGMrE1H>9?Fpx{}h?N1o z53K5Qq^qqG`BfXQ)c3xw(9ujlSlDuq382w_Nt^HI zalp-uE5B!8|FRUqia$^R4&DKU)Y3<>KT_9Uoa2R?V$9A79XPzhv%A$bT%W?@`V()> z*(YndF&IPX9i~Yf%M(&zkdsoz1R`Rg?xjj!s?6ICE0=eR>m1`oK|2DKAENA)R12?8 z98B!pe=IgQm=JsPioCZqdO@?a{mOMPX)ifMXovT?rkSJtb1RR<;A(o@-Ev7#w4)P3 zWgd*3@QZ0upAKv5E(-e6R^EH#&QC&|jzq@?TJ)RZ%F7tdg?qj0yEqz*ClFHsxtd*u zW(~)TFHf)N?*!eR6q65L_9McHJ~^ECsjY*D%{558_NY>-Y>T*~rQA(VvGZnq5Ue~T zZk-XNdCG4}^)xSD_W`F*gmJ&~^;u@C_PD5u5AKh;Zlw8>onlSCXsuBKkw~vRdbnHa zTe86u%V>M&R?Om7*JlS`lNYgqt#L8_X@^;7k_&uH!24xojMe#L86OvS{SuCN zeP32$Fl*2cKlk1uEv_@eho!x!XOGJsvOQP>%2Kn1I$P1b<7Hd&FLOHC*MIu4wSS#B zx$DP6H?iDB&v)8)R>Xjp!rUwf(#%I~#yCbrY;!k8cOeesa*Gd$Yz#(|@+e+lXo@_a zz7~&=Av=)%1zxP0<3eKKF_gtvxTicCq!=7R;5PuPd?%pLky8$cX$4h z_R0)?ELFdqX>D0Q9S`@~ls3+>@RxB;v+u6x2qjl#G14*_jKm5ANt(27xQlOQDwibU zUs?5W6OY#Re~Dg0Mu)?PWC?G54m!{~50t^Ea6NCz*WaBfnCfp;l(mX8x-0s&)^kbh z^-{4~UTo;-C@1cWtzg4IFk+O^u7P$S^pP5Ay{w4hc(FdY27sIHlDBAbl*EiKZBl9E zN8NsLajS^;wRlb@)$ofit@{Z2Al^X zeR7{NZqM*`cEIiG>lh@*zIx97Y}T86JA!XI;_|U}@@1lxnA@X|6E}m$=e|G&Iry60nep$#+B)H6Eh?K6-X1KvrS+=|e?NCWxwJdX&M#$zF4tG{g~>m&P8pb`vgHE46ez~YfV zAZ%*b-s`z3zGI8~+m5Phj?)X5EA=8vlS4_kpECWEkWMeZ0{XEo1^?@UUK=-#@W52I zv2E7UR0{yD30>p-HLUv!5eJR9`B#UPH1iCLuRN&t3wl0!`#vv>M-b32wvAe>E|ine z63&-rP=xn|cC@x>xj^$mqnrg4&%V|#?C(j1%?E}BgB5?8;qQuTi9U9O{i@i>Bp-h( z3h7khDNLG-@GBu(IHeKUwrHTb%RJW9Z?*Eux zyDW3;mE6)TA5QN$L6n>m;EYvN20AdkU#!6nZkv)3zeiGJYY~~3%c0mJ_!pO zj|ZEPY))@;o_WKI$IfSmR{uImY=tfk{@2a$v^P+aTJDss5%9a=}}k zVBGN*Ot-=Iw|ohO^e`O5L~@dpq-03Sw|@7veA5D>aKhs44g@=1AZZ77=_5?^?d>lOFg4h2%=%}_KVMkVYli(p<-BSS#4qw&$sOuOn3)+|Is1l`) zV3k#LV~V+10M4H%&SLka_I$Xt=q8+bptqri^OX8>*ZEcv%smUJRB=#qKqH_DtG2*rM1+%D(H}|VXRi*ZY*rd7G2HP!;>}K5VUy3hDJQ20? z9t~Ahv2GkyIlI$!aSQ0C7Ds4_F^oySqGmvgD9h_SC8$fXQ9)`c(?3wRWL0>)Z8Aqp zZBQ!_aCOTE!(dq*n;K`dv17$zMvtqID%(J-k5cwtz?UGKt8?!FB!=`^y5nvMyI|A| za>t2t@~71YGS9tbkWEt=OaIE0)v-8^(|Qg=K6UQOMP!~+n2qhW{xUmk>?am#yGT)3xB0`?W6TD*^7;=V3m3{tba>meAcD-Cx?0MMf z+>@X>Wm}TJwG&Oz8j@AmI-f3JA~h$0Es&0po;QxOXkXWxZU?W@mr%+?~S>an7;1fn%! z7oPPQ{-U7DDCR)+ZAX|kFAs!`D!tUv;|u?0Vm>t88uC38L%4 zgusGAX!hWOUM3c>^-0N`ITI7krr){c||0Yi%&27o~T zfBF)H2>}2wv}C}9Kw$Lb!i1m@pdgxiAV3g`ek~9Lg#Dw3__u;EAQTKkOArhMKsiS< z2!esZ=uW^waP;KDz)-jlx;+R0D)dJ%2th#@1Oi9Pt{@DG5~Djo#V3dc6Brc!7sOyN zAnMF$L8A1UJ^J;0zo?oTnH5m8jj#XAR+KyGO!R@W^e^jJp~1z z-mY~dy(@-(AfOQVuLA+WFgO}M;XoJ|^@48BZxiUDfdF6-8iL>;A&3yVD-aOXPRK)) z3G|Y{L14&VDFi_vAhf1}gP>q2da6M%6x7j52ZDnE=$S_KJn%nZlKhui;9wvK06``? z{U0%*_y8Rya4-su=tqSJ0{)Ugg@lCASO*RR3xd$00|)CG!p{Tt4H5_0Ns1UjnxDW)0mKi7<21COvic*0fL9}ea1fi&z_eZ4>D1Ju48_ggL z07i|1KNL}VzuO8;CIkTfb*&Hx0!IrPMY?b}8th;|fDizVKr@I+v=F*uAd0}y4Wfu0 zfF2AAvwsDMqG149`eCT%{CC(O{xh3l5a8dV0s;l2*BAyx(Fl5gP%x_h&<=v4VRSx3 zk?vo#fPlfEpuZR!#eP6E%);OxIP}ljq1YJ(5Ok6d{Jr1&84QYaQO$!U1E2r`zfb-L zv%>*GU0z(eek1*6$U}84+@O{ zLG%*}L11VpMsY5xh0)RkLXCX%08xVk z_Lm-Nl>eDx0YNwj0)?T~48_3EzmkSp7hpn2fY1L$qJlsudYq^{q7QyJ7{zkvF@d3| z35<3gFdS7#G#LaH)PKVK-=x6+kiQC!sxBBk7&wZe{;UiDwKo9a=(vQVYW-(|1mSR0 zY5vR);!%><1O9n%u0F+}vL7_jZ^;-r&+d_WJP$2um-ftOd4*$tVzlErT z{iO&++lYVbp>{cRJpelQp!ELg?B6orza7i`4We_0{(%A1WnEd_-_Fvrp zXY`X%YA>M79547o*1gUozAlip=rl=Pko1Z2|NUS>OpNP3=l}B~eFAZD0#`R<7dI~# Ua|;3#HKB$llz@#*=9%pO2Yp8TxBvhE delta 19411 zcmZ{L1yq!4*ES*DB@Lp4q)g9%fFNB;NC^l?mxQFi&`5VTNOyOK3KD{JcMD1?ApiKD z_nhxL*!MfPbz4yK2+Iv51jgP-*h`*?}Kc+vHKeqoZe;j{Ye>{JDe}Y=V#goLR zWY`>u*r$ZIk?aa#&N5i;EHA*Mx7%@(G;eB&gZN=U3#by==)GhP(+DOlUN`{iLI}C$X#4w@G@+ z@uXv};`1dIOdSqmMZP?}n>x|f6|C!MSoTE`{*g$`$gbl3CvK=jmRj#;=~fodPW|8u zBQXEbxa%ezW;)vk!f4fpp|6+3v@D0*@Fdf#_3qAMH(7cTQ*xSg1z=U+5_IO(NG2&A zdp@4NFO9@FBBzsk zAF=2*-k(2BFg%f;G)xPubMZUC^1xQtZ`Ae4U4BitOgJ&UUsoGq^iEmsngih!Q@l&8 zkku=*Ys-t2vOMqGNg^N=mD~x~#Feml-77%8>hMX~`Sd46Uq@t_=+%81>*l-HcZQ61 zELZ;;T-~&y?83146;fixdrUZGWFl}$lwf=%#FqCa+_XJ0cf35OVf>^k<^4E^Cx+N( zen?dBsm8~i;4d+Z+1U00tCTs4EZM{PRpU1&GJ6kvJq+j)*$8l{8rIGU@tkh~1q2Zd zUu}p&h;ZRh0T>9FsNzo4lxPq_M9?7SPLx520}_BCpovuhM74jRnE^y|_?VEyY*SK> z#HwCKO%`=q*Rs3> z`8?9r+ynh_<_Q%v1@x6lr^IG%+SehK}z#(Eb`Y+%J=6 zGro0CaV}CwR!JJ(Eop1U+N-EUk;vS;u5}k_8%*ESvMe!8-Oy?cFdrn}wP-S@h&2eT z&DT!m{^j?{W6yTv#%5JEIW|DuqF0NDq{#HGO1xj7zo6tT5mgpSS04F;HMWg~hsN+; zVTCBG5qy`*ZGqf3svMLLDefyp8EDT3e0!Kew*5ehn5$o<=z{H+5iOVe6~(q%TBt);B{nvoxqRXHa7_U4_K_vYN4eSzTF`}DV@B~3Q4 z=B#>Jd<=J5f97n4Zl(LI8%=q>5Q=!FRzCkW5_|B`)r@~lV?zP?i}5xQ{^;TL0|i+` z5Ibokg$!Zp`IfP=Agky%{q^A$HwuZWcBJLb(-%zyAeRWPl_y!cQ9BWj3D`jhQbMwy z=HE2wb{t+!YLE4NBa@-olM~e{puljaS(cR1z0bz<{R>mqwDHH|tmoayM|RsGbj{?y zlGK-I77Wsshaa}()^F>-32LXJXu@rG5}u6?!{AhaLcmgeM-f~wdzMw znMJ}#zi1052>a98{wjS@%PHNKv$ILOOEdIxn86}A64SOrgRH1g(EBF%o$7LbmNWX0o4doCc{!0WAZbI=8q;v z*qWZq#E>;}x-2OPf&!k$w2rZ7DnTkk%5e66Y?3m8rpin81E`=#pw9iH-)m-4Wc#5f z&j#=Mjz&z|HoZ53I*w^iFu=avFzIFKChpxKFkT(l#M^RFz;6A9_SK$<48Ba*vJH3;_Cm&`G~kpY*c89zlaW6$=p8i+sZ>VO zQIYtDT@oaBsX5bqp3TbpDO;=``v;`_CP7S=oIKDVYJG+%nHm52!eYGNRyEGn{K`VE zlT6tCRNc@N=~oG@@jUk=){rl~kD^-Rg`Z6O+E60LWA1J8c$dEyP(Ls!?$KopinW8x zzocc};n3`dof8;|-J*(O78&kSs}aan zJV#U*Ubl_C7Rg5UI7Q(U7Wz3TA4kB$c^s4FVb4iEQK8LUwQ(uNbHp82c3hTT%Cetv zhYuu{4e|O-=A0%&91o2cFLYYG#=-ODX|Z>tVij-+pBnGJ6Sv{RE2K9jEVMjkxEU80 zA@KS6DR(2ZRph4nh&dW*`jdbnuEv@|ebw-;IfqAoRD#yMPj5~YU*Kjt8|b<&FT%~P z7RjKqX?3Q}Hx2&URw+tN`VHoSWE3Wp4Eyf(1lHAx`S|Kg>ZZ{?h4vEuq%zUdmjf}$ zduN6p;Jr}>GA%3no!41`y{-#E~6gaP2@Ttc_`{70rMs7&U+`VlQgy8^8l}Z+J|64 zq$$IL-6?)(@4nC$;+gy@_d1p8?RVEr<_XQ(&O@q@LA9EB7d|>N%*5OS5*Or(@oZPp zE8h@W@JQ%9(FND?6{CNmqYjr}LfoLP{Y2H9NWKoK-Frve(+1dH4%`5-4J*nUvpZv& z2rN;BjnyQ9al^9cbG@|5kAk+(Je5_$I6hzn+>w|GBDSyW%}V!kp_NmO6xzhQ!@8jF zhc9gBbxvsb^AI4^vP>Og$(V-BKfsH|sOR_lJ{G#bb3~^#?CFdNb1HX})=#;-Rs6J| z%LAxRgFE<|S)SaA8L5c>0E}?rbMqi|T#Hc|qBf;{-K+#WJoZf(&>F{Do$#mI3HW&X zohLrk8=Ur&?^h+q&8G~SI-&Y(;kGXMk7#D<j+E8H8j|r16t--UNu;*%`27?l5(pJN}09QwXzKK0pGKJQAUpSMMz zmW3>{V)lXU@wE>QJl-?xamLzTMlbCo&B7n@;atUUC?H0t`dL*7^mY*eVww|?=#&fXU)GN>5 zl%;dK{R;vvXs~FKd9#sID|DhPSVnrDZARMG564zIpT4i!|Gb6zOmKWR&ivr)zPjoT z1lq=08#}5#`||nQai&G(g#MmScCTzK;|@wzCC>1R9N!+tCVED;H9BNhBTSJry`f}` z-1A4PL7T)^(V`cUm%B-ZaXEPaS_WLUbgQHmK|9UtQP((z*w#un<1Ya*_ueUghsf4o z(kHaNR&3-c`a+q|xmM(cD@r!PS_dNuL}(>|Y5CIqhzrJ_ncMNzYEHJ=AEglOT~!Nm zifA+`kXyKM9=eA3rlciO4mu(6Oe~2ypp^h@vf92MdUhK*7T<^SqFbJ7?5FM8b&D!( z$7H&B_SlR7Nx0cv=Own??@VUw4erljr-aLVgNA$35;n>|Zq|<&z8t}>&ZakEkk(@& zc!uL4d;~YDbqvCn=F2!!cqsH`__5*7t&c>ToOW?8FQ%gjBV7wp$L7kAZQKis7^Aw86mh_Fw5Xb6EoBLZx%UntJPB z?1sM}=)1>uOvBn->%QzicI0HP!~0SP3tZMZ5-)xjnO6V$bImb^K^ukL>Nqq9-5S#5$R7 z!^%xAoxV?Rszfx|#a(ZsA~u%*N~7-yyT8mn^EQu9mu34}=~40;1ylwDrOz9dS~&~v z(*#`wKB_ArGFchW0D!0mzp}#U)gVC69h}B4m0DYQ4u4P z-7)nsUx+YY25~(b{l*h{DT!SXm?V@G1M#BYjwo2O|EW#m(F;|s*$e^d*BNN9%MITq zEcZW7Th2oi0HFygkMNH5TD?7CIS=?uOcPfc$W;h`*+Cdw5ti69;i1UrPnvfT%hqxM zR4?PFl)^!?y9Q0Rr4ymvBEvBzqjA3S7M3AL1e2TWoGAhHjUws^ryQHHc!2aX^=PKI zjk)q79)t~*FK~_#z5b6CPh}qfmM~4-s#*Yk+78772YDW0BM$>NOFNnH<8yS5Q*=6I zJbhlSPjvg&xX!~UY*~;|6JPvo==;^)Ikktho6$pNCthE*8&fW~6u_eN_H*5$gyaq; z!#9&h&P*Pbj{siSk@mdjdg;PXf^+Uwpk#7yvX=r^8=pu+mCG`?At=o^lB)l5wP;5w z4Z-*6g3_kdCdb=sT-lLEUX_ifrs|4Gole}Ri<6tbuAgR+_R}$vJ|(n(IAKFNUUQsd z7cp{FnF4GuTpCpJKFIX!W{Zh#bc`z*s=i3Yc(_4piYY)}aFkACDiiD?_|kH7zEfba z+aUk0TP+6f58=6;o}5v+`5oFf*>0UZciWA}iZ%VHYRLLMqsZ!w)OT%CJy~)^af81s z=Wjykbu?O7gsmV*_xq(mQs2EHxMxB7B2ntF7kz{w{z?#%gQfdaX&C6IkgTU%|+$wc=7-9$FIG zASyC;e&4E5`BNqD@_@TUhP~R96gd=Aeq&!+DJS!jU|oGBQXncXFKps$v1jTc*6=gX&Mgl{k94LlL+S?@mIMdbs^8>Tyw;84r;<>s?() zK`q6kC0;%ZX;31$@nI-HLfZmTbF&vKv&iQP9=Vw9jaAT06D5hKw{9L1-8eG-%x$o8 z&sesEkzN$z2g`ls#BIo@$}=hA9h&oB-HX~iLZ22@255m!p6A+~bsW5N1DI+29*LEA zj8hFj$;&(jM(@8B<}n~MR}`jy^ll4X2z(6PXKZX5L0WS>nPyy~XaESg6S=WZ+SSkO zx5{U+J__KSV?V89=9-hpxF-acyeN50xldYa=$MYJqsPOUs*xLW&A9%lim?!(`OIkO zZJ@GC)>@1NAEnP#&@Ap7%eIksz~WW25eYotzD#c%eY+IY12m=oD%amwUkV)EDxd5m zt)-LCfi%W8;+LNUbCQ{rxV+YHcjH@7nX^0Qk_cfMZm=?>99F>grm{7#`OtAPv;=h<-w3i>`VhM69P(W^*5+NYW! zoKFydwimeT#DSY-TqE>LU?PgOiW{Hz0V>~o^`$31)_4-#$9 z7YVugC3rWVrpbgRC)H``tt%f-QP3{?U|q#`QF&PwCchtI4|DXTv3|ZymanMy`Vbc^ zt6`cXNo7KZH&kd-+h6W{%tc9axS{4aE9t!iHtxC)0h#q^i3{JO<+1(Ql3W0Ki+la5 zP?Ptfpe-r?%|lsIQVjE?eFnU|W={dF19BlkU5^f!7O zR~)Kfo_mz5Ai{@-LZMgJ*fi!=d8K3)L(ZSxX8JSiYS2`e)2&p|PEmh)_mP^+fZgm~ znq9XMa-e6nBE}SRUPGXRzHwb3kvJunp}xMh9IL~NPdO11ws~*!&%QI7U6PwU>Mcgssqa%9|| ztRAiW8CPrb!<6}Z6ycs7w8m5K zNvro>eogDQ`%L3&8!x)KIc#vA?`79tdYYpIgm(9pL6TtiUrr0yHryn>tm)f++1bvj z<-4FM)?*K)b|W3Kj}?NHTt2B#_|RTmXD2H8(NHp`(8;8JVI<-}IHJAtm*e0CkvYju z>VI;)fsuuD4~%@Z1|@I5)GV}_?GFNa#5Pk07z#V5On>W-G}hF6CmStd;{z@Db*Wkl zWCPl`X_?k>m-!?2E_RAMT~FOC`gaMQWZ ztO5SXpJ;NVS-TkQTa5fPqM!OSR(x-1)!rC-wzwa`YY=mO-0JormEhCt`cODC4ml$$ zZoe!SJBO^CKpYMbhFv@KH0|BnJeHh_V^h6Vx>N+ATydr8M>jI{1K$QW#~D#k3)Y`r zX}5H2y(^QECN^nLJ(;}b%Kf*7v@aVsya;5S4?u^VV@elJM46MMW2Dk4bxK{Op0Vpp z3ENpVRPHN;CqioF2Favbi$T$i)|pK>P9<-bxRwj(&0(ps5?9b5jt$woFMTGl6jYUs zx(umx$&{w!nU5O}41a<9rKLRZYIHb1b)G#dv?E$Yx@0qMGSAvRUfs*6_~a6*ep2zX z&roXN*64_kY18!*_0=4%L(AlR(46U+r7MePG{zboMVX$rQqS8(Zw{D~E8Bu0o$0BP zg;!^kBGL*FEw-|h$z!I5m*a-+{-xZjx2r|^k`P74mwvIUt2WkLJHK{SC<1st?q0mZQi5fkk;Lez09FD z!?RLMiXA^&)>6Y>hMYQKG?T6Sye^5% zE7^C*Nfc_Re(0TxxH{`!dmBUN>KLwxdG@M1++2*=NGA!Z$t2+>jAJ%j$X9EsQd1k? zjpVk@trK(JzT-mQA9Zg>sCP7o+b~2>pJPB0Ibk;0x{t_Lc2FC)*ifl2P1ds<$*`hW zL*R)be3__1okd>xG)j%c4_?z)HzU`M*yOX-iRIX=9+{*HKLE=nZw=^*hlo}t^_8Ex zSy(FOepmaRqHs241K4S$U)G0)#VdbRM$UVZjwla& zzl+6}4VThzxKDcb#O2R1t|5OwX40;Y#jF;&u}DQ7xGr)p(0G)T74o7@r(E}&Fw)~! z7T{Dsx2rycAhlW2E`Pl<*H9%_(DIdPWbo=f-Rm~a>aF6>)?JFH_r^vzxuprdrg9{6 zkG;b$X-|4vBpx^FmDDPr0#v)djUlo0(2c+u`7xGjD3(ttI$^9rLNxmqY$ENZ5_(x- zEO&f?pJ!MEy|3bsa91(@!uq?h_5iFy^ofHw#pJ~I6J*r=ChE79{a|h6M80Bpz|eDP zdgO$3)uS)^ay%9DVN--PNhJj^B=+I=B#yr*?1Lt$875NK#r$J92evt+YJGm<>wNYP z3t$Q(+Xn`=TO3;E9N5|k{vWSCCU2<~p4*y!No{M9#ZTB4JNB~lLUJ~^1g>pKW;xP* zFfXi5kHGBF~aNHF1Y$7 zwWF%(7KSLYW_>zlX>dN>DL=u(+y3_G7kUNp8NpJB*!wjh+7jK@s{#7)X#xA8t7^;j z7_dg4Dgp7zwd&CoEmq;9Wh_UjWWG!3#hL>*8p2b|0Zykng5!)<7MZo+;>YUQRaqS3 zVotSFObQy4r4esHripjT@72VJx*bEH%hje9Bf~97*|ccYfIJO=w2%*=BITrw*hWh| zQan{^NH~;?`uoe)N_{IbwIbehNlCL}24NY@q-64*%iO6`YoAx)&%p*$GtJMO@E5J0 zWsXz>GnieU4phqfRW@^T+WP8xUz>Vz7*g)t7jMoN+2Ed}H^~tjy!}QfK3@=^>xWq@ z=EoU|)L^`6t|lTlkSaMAhb1~r9X7N-m9Ke2L4g@#84mgphrff}Y~^vwm2Y`y%AJ+W z*PJTS@`_13m0Pf=`-?E0Chbfiz62;_$a3V1bL#-Fn4gABnXUTwES>fJ*+X)lkDC&a zn6u3S;df~v!&t9;b~vIen#5V93j5=vr9y0XkPK`4PWS1L;@X4{{CqXD4pmCq(+rA@ zzBv8ztlm$`_hil>h@cOhr5F9&5V$w=1@VkwQf`9QxJWQm$76tXF}Gr+W`Qn!?>aPu z^6r2xPfuE&&cl`_={Z>9SF7?k!;I>!N=>fzhPQ+K7PZ+4La-^j(!9{=b!Avw;OHJ;Y+X?Fkc=o_;F^VpjNCar3#kIye&PudeT zFAb0{(FZ}ks`bo07#zE$$ZyY8r@65TOSnQB6FjFG*Qpp|GR;f)A+*)|=~1xfb{$cs z{(wpJ&G_hql_$p6XLn8*wD$d$@z~-PRQlMBY86j6TSm|F3gG5tlb>cW73$-JF)mpu z8$b5EQxVSDCO>rfdF@v(XZudxW~Ft`3uC7(b!(Z2(H0r-k;vFS*vHAhg@bj@DUfOk z2?Zs~8x7o3XY8r;vf$mVuVPY<9AM4FUoL3J*rpx_PlSIAkz0dcN{0!K`Kn6H$rARjiw_;YKg$h;tcTP;nxw%sBy6TBJ55IeM_ zQSqu@S2C_f;{MvIeM9E4*T4xC9_w1LHuNW)A5rq8ev`Y*v|J9=zM_#cX(w6c7mJeF zy7r^7!!W*e@kIP>Xk{>7NlYPQVEtgEwEd40c%G*1{WZrg{9Yfjdf#{3ZzsH08s?`< zPgyLdg0dICaWmu}5yqmx(mVm#k}D5*%zR~#B5h458y zh!^$NX`McGqRQ*-B5`W2jolzC=vP|2m$%q5FthWPXSHJuk_jq9OG-~3HaCb#oJ(I8 z1S|($ca3;n-RSG;<@V1>)KCHaS%hq7JhL%xYpkBL_7&1y(LTm|f}>L9-I5WOvtKFrJ(wun zDE+mvJ@)8{LF-2U41{!(3a8cIHQ_U3RPJt>1V56)ZV&bZOAvu=(5Mz(^N43eFDh#; zq8_XjewwQCTqk^}Q@G8dRd3ka@nKT`dV;tE8{agHU-%A~7J@JHj=x2XmozGFh!)fH zNNZ!7q~F2L4XO=PUlc7(8>FxF;g!7@^kc`c#t!$hZr=5b-_cf}5@1(S(Z za2w$Qk5q72F0?b?$k%-Lfhx#Zw zxDf7wzFXm4VRn;PCxrK!8NQMgR{Ow;#G9>IjxKo_{DEawO}*XQe^nc^5ozIHyZo*Z zDGf5lTQ!S>;Fcs@J?rkXJk`|46CH=HjHXi-g|XH-(oy!+RwJ!$UKukJ5}%iZl{mHd z9~aStTo$ap$u1Gran156XA*^bTz%U~Y|NyQ|MazkCdiYVq4&bk-u0o{s=dbR{$rE) z$F)XR>htZ%JbC(3pl7o;^zjjEd*;Kr^pcLqnbxVuP0ke35e8{TjRns)T>XAIFi!Ga z);pydW9~r&2}M{i*6g$6w8hVF#~7K@Y2|Y+=R@*!@=nT?H!I-)bA zedoMpi`~R)IqKw;oIG-Ih1?YKlI5xWT~Bb^z)T!l8ej0csH(~32>K)7w%+jZ46W%X z18?~Fs5dW9thQ-eZF5!Od-AU-a<8XP=w@)toHCSWz~jW~G9fO89gwwfN$)a?&3k?= zE5XbeB61*vwhDKb+=;DCUfk=9A?E;OwZ1#OhmPNCwjyq>*5t&dK3V>5XhM1Xdv3?7 zJIA&>Z6*ECPPYSX({+9iGPx@WjC zJ)OWG9TyPbs)>&Ido@>_=EG8xVlh1vlKns-5x3vW1pGU*FJH@5^7SWYhu z6!)fl^xD$YI>-!Nf_hc%Jvc}SGQMEMzn6CFuL}5KLOOxG)NBmOIUDVI^`?RxD+eUiT`rD} zx@O+Lc=7A#5{Jse{>G2_j3zPUNqcqAc))TbkuzA^Q+u~I@JYt>{(>(4H)u#xlo!&C z2B=S#(-^k;Fl292S1e>ih3WJ2p8Em=Gv_WI4#Ucv_!1AXyJa!^g;NcZi8eGe_4bPD zT^{xyghxI|#u!AdT_b*VRLwA3dKd)07?o&zOco&q$o*m&5C1jXZ+$@)q;GRqK-MRimnvk?ts9!rs!v+^~Vi*rFls}c#e#VnSw@bnYK2OoZM&*LD3WU za@jbdc}m5rJy%Ti%@Cz@R zXE=DVTO+h3&p=hfpHi+~ZI@_^G>jYis-2YSE8=daiz- zaSYscA~avp;Mc~v@#BGpeZP=&ZX}q!+ZEbylh@vGK4@0=^{l5Syz_WF3rSvA(G);L zFaXwLRoNQV;TtHnE2an(!E%q~%&}0WO)ywU57OeRmEKqRTth@h(*N`3@b08grE0N= zh-5?as54An&)lm0d!cip{Fq1+F@-iyY`;$ z<;tROJi%#HWAJ;LMf|Ccw>c^!3fyv?A}ql+h-Y1Xf?bzeBPyOc??eF)o>#7~gRh9f z=2p-CsuxU4(h=l~SCr!9$c`sfqUI-E2gAd^Jo84O=2rK$Eah1h8B^)3avsukwAE-P zwQ$63kXtbr+@5Y(x@!9|J}SI2wr$nkaa*{kZtGTd5e#jhnLQ=q&r$U$~f!mFO*J7pCya0R2J z-uGvVDwLTq+uxq$vMcW`z^06VrMOf;2^+y~?-*3k%mCG9`8CFu`4)tkV&AOw)X2;6 zdVM};^K949obq>lPH#UD^5OA=^u~&?Nh1E8^9D=Z@b4I7m(ln+Z(k4QvJtC3KdG;} zz8h>oxy4i+iDVqvLfWN(&|rH2Ht-CzBHbP@>vw8tzJal-AAj!R--M-8aX^&lm|1@ zKGLDKR27KSZ`-E5)xo_U`gKPPGVh6(YU9csZ@I@U21fYszh{Hf3;Aag%a$^yjo*~I zFs@D&X0|#q8m%OaAH5*epZkdnRVgm5h?$VGDofxomh3nlHAsv1zAPbM^YbTnjx+`s zNmkEZ;W;<-_6eEpx2uKU2?D-I49wE+=qTl0bm8qtyi^e3dEv&YvF{VJ239c$dh9DD z#8G(tskRq7HZ7v+mxt)b+8#Q76FZ&bBRN03SNBQKB*>~ze8)}-Oh+y{mn#qAWCrb0 z@a|OoAOq2ERD($oM*UYi^MPiH1o6{=6z8Wz+B{g4to;|p?+t{;G^qI1(#%1B3n^+r zsmGV1H=Ftf>&O_j~@+<`qZj? zSzG^m?XCiA-(=29!)#I~(T_)>IS zoWJdO5jw~#-O61H4+)umjHfYA!%#J;DvIRg?7Pq>W)`KEr1a4gp_3vr|B&2&b*-8v z1we*nr$UBHrN&5WEiskk?OA+8)ozw^c)FV0bO7i+8C+?kn-RDg}naD>hum;eci(uAA=SQECWykzTNp#n?*pWFf zev|1c6AB)|l(YlbwIqY0-F07lQdODUK<(0^(x)=zUpJFVpSp%!%^I8(A291OJBB1z zds05F7qa39RX5Ztf#)*2k|MCrG}ux;!WxkuzNTQwdf+-w;fnwCUufW=&=GBUt;-rH=oukqD!X)yPCGPxMm%->|T)rhvJD@1$+QB~ZY~_5a!=ue4=GBzgOdm!gmgsfAK;ZL_to5a^ z1%6)4vXya?=dIfE+%Isd;s!(_R0F;_k;BBpe3K@&aK$|ca%h(r@a*-5+x5Qfyge;2 z_V?(<&wVFIYSWXDcWXY9W_Yn}ke~_H)M}`z^(*MB%xh1xP#U&HP)|iJ^6vLhf^|ky z3}>D0V=}1W8mG^RNO#sI4nIOZo7SMNCjQ{iPwN&SGEPsbeKWdZMBF3n-4N^bgymL4 z$(3j!ZQN*exy$YN#HTJQGGc!I)EFmbK0I%E^j1!CE~tBLsAKUJSmuZeRqu?#;O(LH z3($i+g+u&L-8wv+YS`(LNSML}8QvPziW4ad$waYBe)@!|*yeINRX{+>51KxcdXg3_ zT6x)EZ@pju7v-%n{NU4+sUK-B5=GLSC%Mce;73n5Up$C;A;7W;X5`0ECu(=x!Mlyq zIJ~nJ<6LExsKYe^q|Zk9Djj7FFZ!HY`xYpNLvKqw&Sf&M=$hvtLrT1jfpxd} ztk1){N%i}aI$goN40`xK!U&;qea$`b%)ElhHx&}!WN}h^((mkQ$}KxmGZIOt8Ypf} z#;bX2+}B%kB42x!hkTXXa?BKSEaA3PDGL zpr7g4P;$n8$w9C+7R$8%V?hDeuLmZ$>$ES;59R|KAPGnP&w~hw_mB=952l_txpUrr z5I2t37cEH_Hl>OBa7yd?)(gv0X%`1Nb8X5pSlasr6Xegr&Tj`qHqfsNgxOW23j=cYuDba1dv7>gKstqV=iPCUdV2?p zqQ=wA=5VbZ$tMY&Umg1#PXhf8n-{s+!UtYb&DR?7$c0ZA5UzM;R^{3{TLIW&zEx>P z`T0p0QSCd@P`h*S^W!!+Nc~9ZBUfA%$W$60`Dw}*S3a>@N`SPkD6TLdKlsV8eO7hJ z|6Fj}N^jk9#je@Z^n>$uGA;HsSu2tmW z3JZm-S;%h^N=B1HJr?0Sg;lT8(-gwMNnV-q(SK17*&iUwFZuk_Yw*@DB|9YVa#VQPJUwkL4=*%qcw^yEqndrd98os1f{}D zhbv;{_&gWDT@pV3-JL#B`m?3xU`w!YxO8120_PZ+j?&@LJ-7kv7 zD=fuuu>}H0h0JRJ{7se@a{~3!Q-nsRRfHzC#*VKYObl%j2kl7-6Q^AN=au4w=JO|C z9#MN8R&0mfXE5FJ(st7^u+R`cziXhyLM%ynkF%MqA9Aur za%R?@%2D$4C6kzA`H)QH(B@3-&Z7&@PQSY@l^f!;gmV6-x;Ps$_=h5&kfTaC0%>mW zbGx@sq)aLaahG^U@pD}HD&E1R3rA$tBh)t<_da*zW0PI7oIPyqE;%DJYS}^)$t1znDw#`}Uv{JkC-GZ1lF}%#NW}cQV@8&Z^R# z)vx7jlvI^i<=b_yik4E`XXH0+f4}q|XFd=Jim+u90${({?c z<&YOzMoeqf72fLafH)iS(mx|V1Ju&WsqXZ>LK`P|{kE_$=SlAjg|woa*NqTunbShb)LwP`P%TF$Wb32(hANVLSbNG?4XN-7 zL6N{U@2+0WuVU*nC~mBNZ*ao}zviOHQ0?%$-&zV=Ua6WS;ldOxw>zeY5~2q3!auOl zk5C_sUHd2x(mrP%F4uuiu%HJqTF2+m&$&&tuDDS>8b>$#wayG*{D7UR)+V=fN1I0V zRN)bCHA&CoUgrMniDcw7!l>@+61(cDB2bx$Y#%3M0^y!lYY=uQUDz3@#mCFZaXY2N z%6Up)EBf73h~T#ylPGY4pw*iO+USS2+Y!39#@o-v{k46iROA}>=3cJdaDOc@3w-;v zDUOg3r|kJyJAg|oghl9`dVbBKh0FcMEnvSe6&GYO;yyDs(|)FIZc@~h)cdiVtOBdI zn_PsH=H0VL2QAOl8WWGD?OrvkTMoaix@ldvY}C+V`}tyZuO!DjlDo@}-+U50DpbT@ z>&3N}b+~W|Iq}-cxbw7>Oplf^Z-JfPkPK3j{-;X!n5wQQ8I3S z{f%Zd3<3wBI~=9s4==z$ARzj)sM8?-QjF4zK*bPs|KI8RKVCou2L1;Ihk&5}mO}^v zzz{S!RF*)&Xg5X(q6|bc8UX;HGWoCb{>ftm02LCnG(i9$0Q3|?08oKKR{}&CgLXRv z5DY|5MFbFnlKj_2kf`{=U_i7Oqv{Ot$HO2X1ca8X2oMAzi2f`H4uSlEArR;lj&d{v z3`PFS8bJigXdwDcz$g#?fq|i5bYoBj0YR%A1Q-fMryv9v_CM8({4akYz;G}aJ;q=J z730`t9Hl!9QG$(gFcB zP}`FU;~@VXYZOTX!RR>#1ETo&4>=h0?*#paXTd-q49!lIA3^BU27>|s!2d?(pX5f- z66|m0{^vj#018FR6BrDPVu*h`1BT*q=pQ5vg`wx-Z!xsaf|L2!J4p*3jet!2jWlzbONNDke0=D8@z=#ox~&|C)_Zl#Tc&CVxK+ zM70@oz5#;4=w3ikHs}vh1Hw=}^KT{p)d57AjcyDQ1VjxuXo4W9Ai4_?AUG6(ejr#7 z@Q2Z00QA3e!#@oZ#n>paK+^&KJxkmX{Ez?tP7qXP!TxAwU-YH0jTi=gg`eCf$GcX35-DXQFO(ql>Sc={`UVr?nfX{ z-3MJU0*=N3D8+(;pnvDgZw!D&t-mo4>h#~@f9v>-fr0D&k@ed^^ra{NRC=>s{07&S+83}bD7=*_CzcJM8^~b~ihi6dy z@uy-GccDLv+TZ><@1Nxcr38Z7m;Mk0p$#Cv<-mWIA_RiQj=$y52aw+w0`#wtAb-0b zDu~A4zcJLdjBX4RgtofENTn=qnh9l zv=Be|{qXR5$-$p|G)pzBNP=SbbM{-@Y>bE#FP+# Q3Os6SA>`nYdLsS*09~92<^TWy diff --git a/reports/main.typ b/reports/main.typ index a4b2640..bf4fa00 100644 --- a/reports/main.typ +++ b/reports/main.typ @@ -53,7 +53,7 @@ name: "Dr. Indu Bodala", email: "i.p.bodala@soton.ac.uk" ), - date: "April 20, 2024", + date: "April 29, 2024", program: "BSc Computer Science", is_progress_report: false, abstract_text: abstract, @@ -1272,7 +1272,7 @@ An example of a failed formal verification report is shown in @Figure:ariadne. ) #pagebreak() -= Testing strategies += Testing Strategies During the development test-driven development and extreme programming techniques were applied. Each crate was extensively tested using unit tests. An output is displayed in @Listing:TestCases. @@ -1373,7 +1373,7 @@ Project development did not see any major deviation from the original plan. This However, the development of the semantics crate took slightly more time than expected due to the realisation of the importance of the functional correctness of the crate in the scope of other crates. Therefore, more time was dedicated to testing and development which shifted the deadline for the rest of the planned work. @Appendix:ActualGannt illustrates the actual time it took to complete the project and the updated objectives. -= Final words += Final Words This paper's goal was to prove that formal verification techniques can be integrated into the development and compilation process as first-class citizens. It addresses numerous problems associated with the security and safety of typical SCs and provides theoretical and practical proof of how they can be addressed at the language level. @@ -1549,7 +1549,7 @@ Due to limited time, this project will only focus on a single-contract execution caption: [`Cargo.toml` file] ) -= Emit example += Emit Example An example of a Folidty SC that represents counter application with some additional function to demonstrate other statements and expressions used and the compiled teal approval program.