From 9c5b8476eadd082c44ef82e243964178ffb3db6c Mon Sep 17 00:00:00 2001 From: Zilin Chen Date: Fri, 14 Aug 2026 16:45:25 +0800 Subject: [PATCH 1/2] fix wrong fix in #2212 ported from wasm 2.0 @maximelegoupil: Frame_ok implies that C'.RETURN = eps --- .../7.1-soundness.configurations.spectec | 3 +- .../7.1-soundness.configurations.spectec | 3 +- spectec/doc/example/output/NanoWasm.html | 4 +- spectec/doc/example/output/NanoWasm.pdf | Bin 245110 -> 243776 bytes spectec/test-frontend/TEST.md | 31 +++--- spectec/test-latex/TEST.md | 4 +- spectec/test-middlend/TEST.md | 93 +++++++++--------- spectec/test-prose/TEST.md | 6 -- 8 files changed, 65 insertions(+), 79 deletions(-) diff --git a/specification/wasm-3.0/7.1-soundness.configurations.spectec b/specification/wasm-3.0/7.1-soundness.configurations.spectec index 5befd6375b..e17614b240 100644 --- a/specification/wasm-3.0/7.1-soundness.configurations.spectec +++ b/specification/wasm-3.0/7.1-soundness.configurations.spectec @@ -37,8 +37,7 @@ rule Instr_ok2/label: rule Instr_ok2/frame: s; C |- FRAME_ n `{f} instr* : eps -> t^n -- Frame_ok: s |- f : C' - -- if C'.RETURN = t^n - -- Expr_ok2: s; C' |- instr* : t^n + -- Expr_ok2: s; {RETURN t^n} ++ C' |- instr* : t^n -- Resulttype_ok: {} |- t^n : OK rule Instr_ok2/handler: diff --git a/specification/wasm-latest/7.1-soundness.configurations.spectec b/specification/wasm-latest/7.1-soundness.configurations.spectec index 5befd6375b..e17614b240 100644 --- a/specification/wasm-latest/7.1-soundness.configurations.spectec +++ b/specification/wasm-latest/7.1-soundness.configurations.spectec @@ -37,8 +37,7 @@ rule Instr_ok2/label: rule Instr_ok2/frame: s; C |- FRAME_ n `{f} instr* : eps -> t^n -- Frame_ok: s |- f : C' - -- if C'.RETURN = t^n - -- Expr_ok2: s; C' |- instr* : t^n + -- Expr_ok2: s; {RETURN t^n} ++ C' |- instr* : t^n -- Resulttype_ok: {} |- t^n : OK rule Instr_ok2/handler: diff --git a/spectec/doc/example/output/NanoWasm.html b/spectec/doc/example/output/NanoWasm.html index f7edd685ea..63786e0d49 100644 --- a/spectec/doc/example/output/NanoWasm.html +++ b/spectec/doc/example/output/NanoWasm.html @@ -7,7 +7,7 @@ NanoWasm — NanoWasm documentation - + @@ -378,7 +378,7 @@

Binary FormatSphinx 8.2.3 + Powered by Sphinx 8.1.3 & Alabaster 1.0.0 | diff --git a/spectec/doc/example/output/NanoWasm.pdf b/spectec/doc/example/output/NanoWasm.pdf index 525ff3f867e6321e90bb2a0323854a0cdaeac592..a9f146cc4f2767a50032cef30dd5aa3b2c73549d 100644 GIT binary patch delta 17058 zcmZ6yQ;;rAw07IJ-M!kjZQHhOd-dD4ZQHhO+qTWs=iB@Lmaz-(5?W>63beE;iTq{lX&DGy7= zOnTKk1~1g1Fyg9+q%jSaUB&($M`n)K!~}r~%$dZ3YLvu;iq_Nv8VUl!#nL1Op$H1hl{5#B-c$um z0tUjx)-(^V2$qzLiVnuk!aWn`IwZG?`s3(f@V43hTxP(W#XnvdOulplls)hv^ zM9Uam!v;1&rH?6raWdSvwRyn!Elb%K&n1!obIOZda}*jf(nq1`@+ zO$_Cqj&;)K{glHJZuGy{P#N?r7By*%Hv}oQ5RdRy36U~3t4SiNloz)^hmDj7%8QAC z+Yu%a2^JqELss^gR3c_&rnhFfLVTMa_hcxjZH=FDpWN(xKE3l-6B(Ei))?kdiEcXv zx>4;cV;qT8yy(8rdtC(B3=^m%|5m=Cr8?r(3z(!@{)XIB(ISiYJ@J{r>L@Q6+tF5S zzMC^oohqD!LF`}wVLn;4@@kWA^;G4sej+n*l!Oz_AWIIWhzD6M1M)4;<@aiSnjn5Q zq2v<4#M{;FbBpw!Kjt*B0DKVg(260X6wwchm&Nuk92$ICEig%m7^;9Sm_bD((XXFK zD!HcH+P4EcaFXIATTEp#N??`Z$G4u+`g-mm$8=;~qV|MuCz2X8%0?oH)?}s{*66^F zRlHz@ljt}48Yra==gNMT^PRif%V%JRYFrT* zGka4PS7$RLyZ?D|NXo|mPqM~D|8EKTV{!pzLtE6esYEKNQ@M+=X$jGwq3A@F`u@U` zDksb5_hu49xO{8=Dr|P2ABJL_V`Y(zT$6 zu28AU649kibl?jxGjj7M8@P{zobA?_ZygB6`O#Y*Z z=`%pHi#}AYBnzepeRez2_%nx6ymf)(#R$={lr%w`@Fv@L&)^B0lz@Snw1wpk+>oS< z9SoM|Ax84QQ#aV?po~l`NdusifF2Dwmo0Xro-2)f4#!f_2lz#noY*8M0cXjr^f32r zT+77948>wh-d3sPOCl$4rlV96`t*U@v`~xODR6E;7?1TrTFYB$2664Fv1Z?DLh$BM>Ph{3f%Prj^Odw>Ub)AB__eXT@kl(O zHX_V@5Tr0FC^K3tKpk(GcLjqU-6;Fb2VJ#)<6Ak%kFtsYiD=hcZ(}(K%=O|7Xf*O* z&*VTQw9yX>ktaPxgIaL0JU|vkAFQ%Cyb7D0D$T_J$cqg+{=)$Cmq}1ZRcy5f z_fYJRai(@hm>-05Yi-8&SA=Vp=Bn{MfBc|-SWEk(9gpZ$5w{H7zn{kCPzeI=%s?J# z`4@iRbp%YIktdJ8D(P4I^0n}*Z^_y~!iK!dvG+xT+ed7%h(?dHxgN(czfb>Ecp3>90`Ek49Y!fOZQPE=ggfkxHrgZj$Ovaim z&klorwEP1OJTb+;_j9fS2&!!bhZbD?xJ6w+&9fv2s9}`w(5SnRObzG3`0F@qjS+kB z>ZTga2X=_Ar5U=k9XF9hhIOe~E5%ZMFKng3x#@Bc93UJ&gLd}U%l zZizKRcCj?`l+dTNQgkbGQkj}r?(;uJ2t^eWZZ57{Ek=owXQ-`K;d-5pWOoO=T@^k^c~f=-x&d%dbLraSladv2J!;aQzsC6sxnP>`d6(t zwDMIgk9lui+zM!AYhEu;7QNw|%yQ^$&qLk`4neb@7QI?&9dU;$T78st76(@9Xj4_A z;0~o;+pGu-sZZTlkZZP6nMnPf5Na*ObA^aLxmZFyT&!vl<+VY97NN0Y3WJ4Lbj|>I zhMbWPx)Kz1}<=Wkh#`TcwH+JWoQqJ1emk9Mf3>z7#Xm-Ziv@THEX2 z9&eubp39`oW#6@_hob$pyG#qKe!&1d`J3*g6$3DJ9Ctk4K2|5;lo1oqOrbkIigoi^ z%aQ5FvpV20fR?5fk)O14MU}Y7?5dN(BMHs#cG^0U_;Sp-4u4Ab7}w{l@^piZ2)Ckq z+rBcXAZQUJ?AVrd2U}{Fwix)YSahwnI=5<$PFM4W-dd}{2B75G^E;(v8Am`Db@@+= z6R*xbf`tqS?zpW9<18Eqj|qe!(z+1ls-U(LcfAK2C(OnP0KrCo#9(NXyoQRz@6A6Cud}(8zemlX} za~#YkCd?D8*_RQ;DC@y$r~#XzUI*nuf(RMmKrBzhI!}bqlm!$AUj~?NYytX19gqz4 zq$$?}|L}sSA%QdtFaW{FkA*%9g*u}>vc3nhcC{MARsZ!%j$%3+m;`)q4y_M0z?-Ht z;BQSA)!V(PsY60^HOUCrXx}OP>U@IWrK8f1^;qxA zu6O#^%NCJ=VN9tS?suSd8w})1iHuUG~Y$3T6HOQ{E{REdnPDgRGgog{vhY69?=6!BUTwoWqtl zQqPmdG*btyhll$sC?m*mkv(j)AQGgQ&KRTwhH_CY+BkFk_g8NLB{#E~QmZAwFj>XH zbr#3a!E`N!Ov1V{@fi%4485V_ahA&CKoaUBQ_@uY(2Vf(`yQ%9Ew4&FQWP3zq5@i? zhFf4(e4=FpsMLU50aiY-3ShcjixOO7J{LtJfJ%f`bP`#l@K6mL{ed)AdXf})-(L!h zBo_^+F`@v+5||aF47MRsb{5nr8moY6kkLH>C7$I}0l^&DH?S9|1p0IMi2oTnnfyE| z8wyJ=x@2-b&G7H2%LWMHvzcZ}K_6?9NWLI7rXz^qNTP)$-M*x40RTkX7>W_(*;FS* zwiiedI1b~L%W;yviVI=dy9L!2eENVksC7|OHoN;%qTg_t$8funhnCX=m&StST(+`a z5vtueAC|lk1)Q))RC`Hc%5UIikK#V6R%GslYl+i2g^J5Ix6Q z36pyTWKXnC8wrU?Gvxs-JcfMbxh zV#(0u(XjynWXN7KN%Mr1NV&QyHnyC<;PdQbjBDlYeB?Oq2~an6G1#8=e5v+wh*}nI z@ClaIy*gyUr+Z~o5f*|!`@(o}`?qo6(z7t^&O6=hm#uJ5f0w7`PT@=9Z94^@{>5=& zN5}o`bVl~?%G%PzqccB?U)FzR%tT#R?l#C(Aq(K$=~iG@k@KcHb62@tM(La;b9>Y8 zDpQZUxbCQO3Ba^Lx^;da1L;_{`>xot_H`lmx5t1z1>nbf{!MwplTat(6}1GgE(9#? zaUez+`?;b$87WPhh%q@t9rlpikAXeet&utla^CVu@v^eND)vIcL* z(c}4aKX!+^p}fJ`Vrnt5A5+h>dFe>$<$+@rtol4YeQNCZcjNr(pw^ecKwla)s_diw ztNg3o$LBT^;>-e^Gl30DnwW%4_d}W){HZ6+4mbxRe9d&%kSZz+pQyH$wunrPqsl}w zrGOE@kEAU%bVoMDU63!rvddFE&D?JbY}e6`fe{fw83-cYhT>*MPR1^P+xG;b_y0Tj!~k3b{mSXjfP)tnVMIR}J*jVB>^ z381F8VlgvT*A@D}?nfRQOXz9P|8wiF8mZo#-zY2MTm0ZeY7@`1z=318C(@d45gyCy zjQ|URrL|>X!<#un2$h8Eaa#Xikm{eda?sU0YeXcPRJ1h#As~bTi!W4AC1-~M>*-~O z?a$`!f(gY~ZqImvTqB6>L4~kov*b@zWLX*{)?MdlS;TMc;-w<7{We@Qiu^xFNy| ze%huv`Z1!5r^iHSWHClP_Pxv^gv>;GbGZ-Q7QwBiS+M;=@S}y?_8=iR7xy#gaNdjg zCgkWu@?pQekidUE!eDY5SM=%dc|!lU@Ro_v;gd&%aox(H=V1}36Lk^TXJBCIHF*WQ zQw)7%7N+RU4}Bq+7yRArME3U&;8=-$yH@pFUAjq;@Fp;*85UuYo-;hU!(TCxO1+CI zs#cbxC^CUmZVd~fs}PyykHt$?1c=I%T^Wx-DJh+Al++xI2pmY589WI#1Y9gs@nIfv z7-mpxhOhCkj8&)TPTVu4S7WdR*dQgY8=#et(6)&nD%QXI#0N9|cA(%+qwM&{`80I< zhwCXeec0C3!d;Tyv>BBQaZ1a{s@74P;1R0Q{)9r3K}*L^J~s_PcDAT0fr+iK^%-M-vw2()SkUB< z#Rvl1e)iv0sgJ{#bc_ChVaG-{iE0LXrdj$6gd(eWdiH!{z(j^siD5aJJfvkkSh~xH z;KCnmJaTuR=YijS0S4y$1N0)(+ejjuA!0BF_5%xLECoc8p)3~ua$5%!8wdY^zjJve zdqz$Dp;s8Ga?*u4dsn>|CZddNCk%BW0DN<)EpIK1D1qMX)b_xt zUEZ$9Px@*|Na!kk$G;?7_ybOPNcYm2bv|UF%GiabB;QljeF&>!fK1u%G{%kWW-QXk z2pea=w0u{vO!0f^UMPVM%iUuGL2^{gGgZ=`saF_F8N;oJ2egLaoQN5qEt<6lA~iJe z?hHXMLYb>=0Bx1ve-(8WKSA_ZOW6@Z1`!oW*2f;0O!isNg*H zAyIe~u~`z-^3W~E#|x?K!BxC(oqs8dhxV@SC5L$704621-td|k5Fk>gxNL`6sN?dJ zN~`3WO!VNW@r2SHx&_lsl*_KY-wR4Pr3xw(tztQmxp}H*7d9HDEt9TD6gqQ4IVn~S z-8WaSZIz2p7Hd)oo-@SO>k3g_zCMg#D5m+36F5krl4bFPnP$V^rR4B(aP^9+Sm+*` zN-c>{00(j%KV4hQ;UA$q%)syn({sqn*+ zXjVOzq_z{OmV;jITF-T2-Vu8LIh(kIuT0Dr&Y@SdVQ?j*pw&ozhCu^P4|axJ;yu(D z%0fB^;Xl&pGv;Ef!oykQX zAj)MCtPaU%h@@297O^)V#S`&b63@evlfJ*`p%jU!6dQ4Ql5lO6Nio)cUbi3x18b3l z7$AlX1mG!kp$jEhiqQuGrC7BPMlr$U4nAl^9W$w)J8)V=g_Wn91HZsOZSK$Z+ZOiM z_CiFdd3maYU#?O@~1t2a3=_yjzos>qn zWy{df`n^0nO(KvMMX`yZCL`~9$+p#$o{=R&(oWOLZO0n|7IXjbe;!U-*5cWsrP~+X zeTmstNB_KVn=?x0r4Q`@OjTx|Qhd5||3*?pus^+2J1Q`H zP_aKTf7PdV7%XjY9T>CiL7%4i>B^d^nwJoy*OcCxC)QPuubAg(6%;J#SA@Q*`lqmh z`%__5aByVFui4W&XmiU`l9A&e*9?0)}2YjZfqGhJ80-taC;jttE& zTI`wv^j<)#Xu8DqQ)f$G$QqnB6fd|orO#-HVM7EIH-ZoqtAd`$SZWKaU zGP~Pv71SmSR)kj6gmG?Xp+VDHlg&XN1gwaO4UM)}#jl_RiVng+r)YvCRV8q26wV#^ zT2vW-wStUUXM?a0bf2u*z*0FTiO9-c|D_8Apaf+w+Nnh{8}I}$zJCh!?*Y#b<_c~S zRSxR!p!m2!`AjlWG|F{MO>WzI^+7N=j{}ouZjV@2k=`(A<1>FcrBfjJ%T&eIf>deb z7+$x)hmKznu?UoK0Dqih(*kRs%)UEq{_=p8h8Ai#%!VEav4jXMYKOzf(3nq)r=P9y*>*szqE zu=!-m{c}$%DRpXD3{NAxIztR7e_up6sv>GM#8jMb#uUh#3fCjnO6*FRh1I@ zS+aU2?Jl2!jWFGs#2iQHOu*x&i4KwuY3V2rm*2$o_;|%vTJE8|bP!g88mEF(qzxUr znyBgLIgTwk+M(xhH@%Yy!-u@(T`wQXvMF0)Unn;p-3L=KYXZXX#pGpfnV^dS1nz*T ztxLw@pa{V5eZP=%f)>+^p;2QAj3@g{!5pDV)@z*gQ6&;lo#X$>VE+q6l?RGaz*LaK z?8_WSTjL`I)`9ccke4QsN=e~j`JFFy5GF5+ej`s_98Dj~-LbQ(XwUQa@^wIb)ehbj z@#)cIN7eMCDCp0J*Mfb3uR|g_pa5e$7peWQkt>9}>H=7*Qv7DRsS3}*Tn93Z`!7p}OS_>9UwhsRpg{SCGA z2Vp(}CkVRfYXvQ6YR6VT!4ZiM#tyIg3~-SaV6MBD#E_pvwtj2fu|rS+*d)0Y;$_y` zYm>>v7^${yEpmqPai1+Z%j(Q{+wH87Z^L-9a;ttWcQZfPTOoFnTqbI~nV$OY{2RV< zvq8ah4fXG;+|mavMrAe!oYrzcr%IUb$9*%$SfXvHFiW2E`ttEaiLcATW>eLIiSE=M zQ|T*ed6qX~_0ne{vlL7jaExE~5p>^~PG_FA@2y|fQ3cllXdzfJtA-?_Yz3sOhsF=V=fi;G|FWBz^FL|H&iY?_lo}xQpBq5? zPg%-3h!AE^_i~;WM4_@$Mm8hQ2PFmxFSIIZxyn&9eP4aGZybAyDurB+`y+-PW6y5w zz4anfaZ8}}WPS7Iboz&a2g zdPD!@{BRNe(`7lwzuPePpV=1_A3)(~i3wHx+!C?GppkxXusFHAYAd|jr9F*2EZ%7N z!Mm5?;L%HA`8K&>t>G{OJgKQp(9$oyNbMoaMu43en}?&y@dD0-bOdZ4qj;EJ(&~`I z+UwY@YE-Wv^?h^daBQ#_hp`>Y;NpoFxfEdt8doPk+=qZ;xaZI^$^_yF??!kdI7fax z#mAzh9HrQ5AGCwvJKZ}cmrSCfD%~Cn+RGQ59-_nP3SxtZ<*F^IS#42JgR2xvy&u12 zV^T&yORlFrMFDCm%bfjI#!_3`!Gj~CQ(gDBV` z#$M=`)}`?Oh%~8JGUx_OQ#Ji7^yI+w2nT{@Ri;3LVy%SA42-9tj3-@b3P}MK4Hh~k zaY^lH)dLmAW-*y>geCx%*160zSVCdvE=I1!<_yF2}FSYnzggTPp!dlAP(85M^ z7}<;)`FVtm48MSLroyVS(HFIdN(c%&Q@9(xCG#zw$hjrrci$B;4k4Kz%g0FmVaC90 zt3Sk?-hK*gn5%Z-P=a7&{}R2Ah&Pfel;64aFnfTNi*vO%3BrBXD+@Z#Hpr4GZ(yE< z-Kr-;=m0KGdlmXmJK_z=@9>I3<>VYi?Sk^3~ z4nacQh%@TtPgj4@+H(+9_iIV71N1saYUeY63s4zyfdriV`-if|(P>Hu8IX)1&~O$Rg8 zvI30v5s(@Y-!WQ@)4T+qiFWm#G6~4oHPmV`kcaxIGN)ZnWTczT=DUGZXOzb4oCV`j zMg|@!>uRM7XCo3kd5o!{1dJc^{b|cVw`vf_Kb3$!d{h2<71ZzL4X%257S!bs7vM;1 z#NiVRJ-0+M08JM)uBG!G3UWgHv##Pyf z>hF)YleL~FKTrxbQI`d93o~UYGO1|jW{hARj++g{v;-K1J#pa>fH)IJgv8@(*%D=e z(O%J6ioXfbyK}y#5NzMY4*(rrBBA)emN_HEq?h2V?Us!f3;yiFHFFm8c7?I4 zRQR;lpaEy!JiE;0JtVh>@!) z90CotAj_o<52Aw#e}Spd`w2TX@ZrLl$cCUbKm=x_hLi>so=$<&ihrwWxEV{^fMTYTqUge$IeYX#0iPZOCn=h}b8vtb3uYqF%>80rj1KJa@6#VD_kv zU^IJJ2(JB}K3Boa1N_-Dtz2wXgkMp{_s)q0QEQXV7X0>@yA52K!QL*CPsJX7vG#!= z3uZtb(GP(xRlIkKrbBkzk!7%r>nxR>Su}>tYd|?zo7FO0_J4Vn>Z4$>!`Y8U1yWN8 zP&z}y!pjCJnx$ggqyoQG$9-}bgD#Y~4v zdIUPmse0*nb>OBl%$z-4(cLdWarafxa)>#1yv`DpJG@e>^RgGA#BH>;acx6i{YWsX z0S~AUzY9F?nhh7nDqPpjrs+hKtBXan9#Q2R2_cu=@(xuXh%_O{%p7kZ0lEfgmKcz1 zr|?d4C$+_P1LPAA9MKH8fB|KWJQ+LJ*+rU8G_Q{9Ejxl&a&5bf#_BC_?*$?`#iEir zCz2$%Vzjz%wPR$(Fi~_}?Q;^GR|2w;pygX<$xEl}$viCkC9O}JwyT(->9D2fp4-|L zqj0Rt;O1M@Y^g%v=BBP*1T9=DMT=Kp-?4SiqcXnFfOtd%YT?Y*Tn5dx2kjC2=;GsqpLD19SJw6d#^rH~Z&Cg(iOy6GTw_F$A^EOZf$Son*M`FD>Z{`@+eG+C&>JoX z2BI&^YNE4IRT%b=n}&X5`co;WpnSgruq*6cfVtRJ$i`8?)ZoV1)YPHLBXR7Yj0?-2 zwj-1AHqb9-!}wfsa$E)4My}8Ya%GxnHlF)JBdpNLZzYD$&g5OwhqNDVSnMjkc`CgB6IRfoKa>Ui&CPaU8VpF z4zgqa-p?6hB(`xd!ha{Lyc}$@n*Ko=oXKG%9q^$BiK-zL8KO$s)nXTRw*6a-%8rH~2nI()1qxDiw{#xA6`Oc82>;e9#| znO;6or{zfQP?ls}5q=HUO zR$N*)-vf9L;e(not%iGKYBIDy=6#(ZINVa|eLMiM9k6;~vb#dSRCz=CVBvz+y)9Za z={!_2328eB`?-~fi7EFgGPj^A*tu-Oi)3QIap-b06qSK?-D|R$Oyhpwas`%R*?77n z{<%V>VMC;_f(biNK`y%}Nx6h}3HGM-G}(=%gt}yC4bgrssk|F$5QPexAq30#b2?(9 zML8fOZ-PEzGroeGSzL}qQX+ACQdGgmaC=ePbX=XQ>upKF=VT+VO--p6TVKuRAKzO|FE$i%>2Aa#0Qk?1;DC2vLJ-p2Tm2%O3=%HVIhjVu1DY063EK-TuLW6F|Te#sWW}naF4G?CGk(f-_dJQ6n zs8M8v9ZOsY(YWV73+{s3)a_}ycRvf_lZZT#*Tb$<5vg(RbQ@tFLEfwMX2>zf(*VJG zczLTPTdcf^?RkIs9lt~pczuxgB?ExZR))|P3RIvTkZByqmXKEiY1>l}Rz;!RXmVUZ zt6G;T@*$v(btba^5WYK*si5TBmWjmT^9D~(1&DlaN?RNp8F!(De+J#eOF~1sZ*`Ew zycFo%ap4Vl#6At<%w4pLj=6O5pKzTlJMf-mvf*F0`+M`|!T61o1^#65qXV{wd@DuT zHp)ItS4qfhDOijR+f=AX+1qkBj`FuqMY$St$*0$cn#JK0T+E$d|k3pve#W)m| zZgKIr?f2lJa!9wJiDk}iLjaNTaP1TThj2;(Eb3&(A4MU^Y&_wR#6nE!@@0Tz`T1fE zB08cXC^IekEf4rbEKc*m(g?RN2Q{V2<6p zsinGwzpL#Tw?6cjd+R{_ibvKZH~hSXDq5ufsyWf-_0)WkII&f*CmLH_*|2qCKD=Q5 zgb21}AKUg|9u@-`rW+&#m9I&1~c9{P!_UG8zgtj7fiy; zKP#>*!B-a+*TYcW6rk@46%m1AV-qE^Xu+LK=`OqM?knk>)0<+-iU02?rZkt31d4Mi z=>r0*$~=k$6gn~4j`hYES=jJ7Qx;U4p^(VsK45w;tKXcy;*Kt(*r+TZLx^4Bi}M)w z3Vbzo@_sY2J-`&joK|vG(BX;wQxus zwH&_)B_j^M%$gWV`r8;gj~HA!Fx$(Ru*!TrIa)vM+C5|>h#Gf|1fjg&EF(rGu2=(V zvq{5+T3{-*T3tu{l%sg&6e7Z_T`j?bYG5@yRN}_MQKV2KP6jH>YfcdHXOJs*>Z>+vRMVeK&u+qk#9%OX`ZZvBQ2 ziN%>=AyJUZANS&eXjKB#QBxPD;L~5YT}@#3suOEEJZ14YPjcl>M+Mk4mj(kfXd`0O z-*yHc447O!m~7~pAJc__bIW4NaDSp~xmc68k)!+(VlEnWNj7_hGgB|4Z4%tY5ZRPot6&t9*h6-c%Mvn&6YE%M z6*6EEtuRv|-djTRVQ+rUH4=p*A3J2nE|6C??Xx`|J%G5X}sF&b~uGrZzA=S8VlcpZAqLzC)r-Bt7A7{i?Vvq*N z%6|^xZyd+6<4(Wgf}Hh6!F zOav6CwKjpVvzq=o%hTsw@!!p{iaQ2O+G#TZs_X_yYTOCR5UsA*n%HkrmWq)p<0xtB z7f3VcLa=My5(B&{5m9mwr2Yg0PaNc9F3T|KP>n$48r%s&mq_ANdPpX3kB)ax{c*yL z132rts5)mXLS00^tn#mTwwZk3;>cyn;8fC4427%}Da5zbT3;>9*nYB$Kq3oI2b%(* zz`oxoP6+U!ED`i(w_XoDOV;-mPoM-=_*L@gGa>s9-^!ORBi*F7wv!+`UNbH%x4C;= z!>3tx;D7AuPOAv4m!ZEiejV?|Llv>PJF z)oO2Y1-dQ)*sB+AAwqn(fhVsdcc=uHDEG_290TKvQDE|q4ie-~?Q^1*s=%zx08-=j zLo0vK{u8o6Jl*NMNoIpeYZ3@A?5p}E@4P^woQY(nBoY?F!Sb-#>hHk`Wj)LEN=(_x zw5Ng;kyn7)T{;b-(T!JJ^YTY?K5Ke|b03|;qCPFi+L?hWB;U||lFoTu4bH`?lBb9R z5$~LB-Ye!3UaJjhQk}T{^Oz+Fzy|u1QN|QEs@V@M>O=YAp@vg6bA__hi?i;mu5y|B zpIOmp!z6b-Zms29aK6VCPc&mG8|>qd-7t2LW_*c0y!r^gHOoa$(wYU`V=JYVh5iru zV9P>bRJn1LElQ=gjjF73C5cR4m;v`q{uq|M7TxEg5cOBuNY*#r$>#1gz~4Uc+t4xG zB-%@)N1kEbSb`ZbCXFcdNp<40q-HjWW}nCX{yXi9znY6H;U`zcL!zyg2ubjbe_U&1 z7+2nWyK_|DM0Ol@+gvE`&F?xH*(!qJf@;;JcAKkMA@ZF`$R2{M#3>LwWW(Trx!ORKPraFsEe7I`fB^L zq6b&vsk)PuY8?7XEw0+rr^nLlU*6YJov^wjs%H@m95 zf#2tep+G?)dp_|WfNHW2scQC4xHR3?Tdk}&W=3pYjxVq01oOuWF&oN490I;XAt8tK zGY)rFT-ei9t)x2zTaRDU?=zpMciV(}jAb+F;a-ANGk4@4GMqu>zUffRy-Kmht>rvq zx-3T7wr<+0#?KpjPWryXy=QxM{gfkTZFvgx48|Y42nrVlfLssW-prJj8;dl}bk!bB zbJ1P>)5uG8<>Uy#(qrv+Ri<2*=BHjgua}$W;{&!)#{jpY_VQ`La*^N#hsZ=w^n`=Q zO17VgY81Ru7xSo|sW0IB@OmH5l$USEl(E)55NksJ(46Svfk-%1R?_72)p-CSz)?Nc z5CUzilrab!0NKzLTWnqi^m_PyeDhB!(NzS<1$UJSPgxZaV4(a4BsHU3}H z>KF?>VCvtsq@72k^;n)C-`|(SlHJteAT_rTVM*6Hb3ySnlvrGiqIAVhRQk^&5ZU|Eqn6k5iWRk5smF?#Y$^Wg}E z2Aji>?5W-I!iZ1vIqNd*gl4%#AkAUYo{!Z?RZQ6c zpemBi(J9nv5CwTfBQ#H4FKmTqB2(2d+@xCN2mE_pnq%-`?5V1~9Ua<$D0U?EEqoV% zg#NTjn3=9m(i}!1Yk($B$V<72{2{v{+46z!;tA?`;5xSFtxYY9b@iQ{uCwviunpYv z?$z7cbI{5Djzjm{kr(Y{fmc z*4)VAqo}M-=wmFM*bm4cKC?1*+!>K?VjK^&c4UHTad>Xd`}2Fn>j#ELpP{ zByGU0UQX)0@@e0%&Yhk3&VHFjn=O_M$T{T=)Wx>rEALFof8EOG;xAZCMZ$<0OeOhY zM0yl>{`%?W5x_Ld_?gbe`J(v)I`_;zzk|_3E)WFxRnjk?in4cd3U0?@@C7b78o2~i zN7}wQa|Te=_m#R_mVV(D&MZdqi}u3f0C1t72C$!S8FX+Ra0O#VyI48c6SC8@(le*IHG>L)F#jJZGoz`eaQvUxpR2n+YFx2Dyqc4= zB*oAcl?kAyt%>v;M?eg@-^a41wzlr^ECVhfg=ER_?u;T+RE+?dv$49Vdg*K;n(q5Gih!?hBNJ;7*PN~ z{_FGe@!Ql>!sgt|(N*OpIoOaU(tH0%Zuc_mQGEknQ&b;R<-#{k@BAPKnYg0uKW{6yl$1t$+Mb=l^8-+}8n+})uboS5?8#$QV zed`|ap_k8B$g(WQZH$e_WS_hr@6Zd7U^DA^_*=@3;jGg*8pj=Uyl55`H zc&_m&FIo4T6!obh}Mzk=61b6Zj`q-XAv@prr zK6SQp($E#}mNfm_!EbJK#CH!qdE8viu z<(|woyc1XA#zBe)Myg#g9@ z6SGAEB5DvKgbIKn8k5z=zzt4srevNPMj5C1Lqk|)OY5KA=;X(2Jr8r7lp-ZGP#P>V zRd!iY({`svl<{95 zD88sN9LQO942Y|83W^XQF*97pZ$OZQaXcOOl(vjd4ua#XG6F=jAGN+R)w)r=*EN}s z8=#t_DrJ_=8Jku9^u{lI_Ti5uBwaR^Z*#*G9vVAL99|lT7i3wTo{bBN7qrip=p->L zilc`qrqB>jWRPM1$VtD-w!~jQi++uyMeJUjGBwG{{cSH~^O{x)NIG zoY&CfI+)l7G8&jEGNvjT2a>6hmYSdz7`L&7u~BtQPKcA0oNP1&6S=i)^)+ow%s~3O zayk}|PR?D~$K#xU$8Fc!?Az${bzWAA_9!h=TPcGyD)!T$c482mW_}eB86hO?qFR!( z5WZ$%74bcMWhy>wcA z18Ah%N2hJ=0ek88(`n~TpqZ|lPDip2w18Hy-z|BiSJB3}HOA@0J3zZz&PUyU?E(it zw_9#q`Udkqq$tX!DDBsfgWwQ2432;va1_z?ZlIu5n`soOi2O(cnQa3NE-+wx}BhBRnh3E`c$(s;9bp5ln&0Zq-{yGS2ij z!8}+5OJEsXXUHV;$;m5V+O7V7kDi?YTG}j_1I&`}SjhG@aMi7$Tu*2-3t*N>kv~{z zDB*adhuu-Y;K=dh**7KRimcm#PrBqK#|l7|z^g#Gz|N4sXdBWNSwpgRf-1M3x0(ez zLw4e1$Vp5L)C;MHaDibV!%!+vDkM@n=x{snQ1jtNbh-8Y)+HjvDwtz`tNfhIIVYk2El}6la)|E!x`}BTe%zeIC>7x7HTS}MQpS)DM?EZOKY21C&lqNh= zdrxW7Gk1O}O?hTxQ)${flcBBk&3N+oxq0$tB1PPm?fD=J>OeivH=+SFf;~Xrh$hes s^m%9jt)LC)^U&_e>j&xd@4woAe`1&CmrcC`9t$!!IW`IR delta 18384 zcmYJaV{j(W(zYAhwr$(CZEIrti9NB6C$?=*oJ?%n*5uoJzjf;TSkJJP76J$5Nf~6qXeNZGfB@s+Xck9S z`A_6Z$;J@^SkAKk8Wur--1`n3#lM9zrhK1mS`|~9P@&;H+p}V6OToDSk_LZ$^WCdd zPzwr>zySU=J@*uxJ!QzLTI{+guP9<$NGcXln+4KH5n{T}j5$0?dC2VeR~4 zW4;uKgs3lNTO=a8Ag50qWyh2uwEMhai*Mu26E;*5Y3qzDzyLkb)uRmu#6 za!Lw1CO9_>TM8*X9UxoYX+s2M{PrJ)Ukh^n)#rk~x+su9tyQPDkbs~NW>N%RgL1d; zaIGg72Aou&s<**Jiv938;eMJ}eUUnK3$n$)DP^yW7Qz%Q>~AiGaCGY1j&m^~v=y#w z7mzS8TI21R)K-8(wPr}`DRT=NgQqpDxN$_=mNTnxNgKL<7hnog8UP9mOs$uI=5xsuuPb$5$ z2E#%8SU=Z872s{OIoVsQly$Flcl33R)bxCV~YcRNlSK1?^iutx79~ zh51#9{hDm^P--lv`bki1>3Mm3Zt%hsRq<}l@|MNbA3%=v-Xh8(QXC7Vm~U{R5UtqK zHOz5yloe4?N+J-M8rDzk+s=ZumEyViekljT1y*mJFJ?MEJjyol@9sJicEPh)%gA^> zLP6#DsqcLyoE%ntuVoHhJdI}Vm;f5bmB+uoF+3;W5(F+3sN*Hx@txZQ9*)>XBlj#d zCU<1Bnt+|=X_qmt-T{$(bN_liRg&!{&TJ=#I0&7KAGJ4{uB$ivL}4ky)B0~mhlVZ?hs~w#!uFIN#<6WnMUoH| zE#z^Rq=soSe{GBLq_XcA+lt$#GL~m+KmA=8J$Hu(4VQ0%09>&z=q&HCM+`R+NIL<% zw9Ap5CgA0U!-;(AA~}R}HB}a)5)$ zB?ZlkVLWfHid3lZc|2^Ne|`DQfzhGdN!$>2`u)W-BZ{Phctw(uA+m$yitmW$=m10F zFb$T-_9)jbgPe&-hx{YOaXr-&h`w>Ou2aD0>F(F$c9bH+%p?+$=Z-MGCbpA2tSYj9 z>W5-5j%sjH3&28C=mEpiUlf`~B(9cngMb z-U!Aoj=8Wn48nipj&HSna7#K;?e1R&5{0N8GkCB_P!-Eh2XT(Hel{}N6@&u^e1`t_ zQkgiOperfJxM2|4|0D_jm#V_W1ZU-DO&J8I0gUP>x@~fy^j>Nga=VsE+#`yy=f$VE z2)oK`WJY=}64)d+t;+!ER6QSVyGcl*fu{OZ>?yG_s#5`|VyNG`T+at!I-4rC7t8 z0FY>UW?)!)D&FdaH4?|0pOuOU6&D`Jg8YcfK4Yw-4X-jEL3Ggp=ykB1y z^=6rxW#c5wN8f&;T|g$(gVSV^)CkxQQJ9SkN7?@D7>^i8)i?8)^8KzeBQ5FQv2vj+ zi4_jGvJm0kPkpXKt87#f+`VdZZIeT?2LzYN@{TNT9<6R>CRc2ZC`kD%fEH3LyvQ#d z7l4bP(1POpxOO|AY-f11dbGFppZx2Jf{flcZffqJ z%q7K#8VDjT{RBCAB<^MBY6*6SYi;L!!v&=pkPyj2r)$KR&e}PaFGQ2a(*(5<1q{>* zKzF@h5zyLmDEq-rBflR`4h(7n4=Et>9{>}Mhn0E&N@E&0m)vfXOy!LUy&hl-l8#5-SvXkL42`+InSSNC8@wdSV7y1>DQl&{Cszz%P+ypeE-Y{&h^9BR;c?;Xm34>$D$F{c!gxN5_bSyc|uL z4jLGyg+%Q-)<;`L`vwr4MP?*0x+POCbUB!4nL@*XbX0a-5pt&zNC|Kzz(;qAV1u;4 zT_v;-8_GDzsfe_#m+FGRTJ(sC(zEyAN@A@djo~M$Z_^3aHQxZ4ODtVcTh{Sm42PcI z@yX@;hSpTo+3b^N1RVnXf#$wSvdEtXtw<_{_*y=rza;eIi^@5^BchuN-i~r6wUi9M zWBhUVL=deE1ja>g5gn_T03AH0W0#;rDm1x!%g3iEsIU?`7ts|?A{O{mU^!AubEISl zRC@5|36ri<*P*u+%c0lo(a(PnF6aYC?c`E6E30rm$Sor>`)30R{^?c{i+9SbC z)!+sUi{JCm7hGb+v`RCibxo}~F7OL2+l+Bdx8RPJaGy4hD(6yx0Nks+7pfe)<+(Bb z&qnA8d_PRp?m8|X^{&WR#co%xyhA#&aSrCIqi+nj$f2PniSWO!1gKYA)1+4(*8(3l z8)L)kZn6mgr%;FQdZw}3XShSWw%^W)_#WE2wbf-;*23B>FO0ml#ajW8SqztbGT%$x z{{~vNG;=rn*AM+GnvLTF359)93gQc})x*Fl5h8e>>{`sl zQ}-l!&2y1et#4hA)~i`8?<}@p)Adm;$Z zlB&(%0Bzuu_B6XSjvT%kzio36S5hm-b2Z}|9UyytY5DaTe6#A-q2J4jg*RTikhV=G zYvCGIJ)z$qdea+X8V@j)s$aTpz@9eY;S>>qIqDw<%8XUcFaOIREn>Y1-$miYD){KNt6!78mD(bg&q&Ei<)q#C{81&g7}>Bc7a2&rNU`LJM0wRC*1u&; zn+`+ph~fV*V>i=OU5qQo&PalB0~NBl^OZXqqPu(&dj?;m(m z0rCqf#jpk0>WE&Dn!c+rbmw`fLMux&g&XM)5zhN|_q&GKdnRqaJ_SYbpyT)c@E^x& zNOZg`N>y@%rrRl}Bk~0I>Pj^<{W@Y=3k9y`qpML~t5^Jb+3Rhx_6(p2pn$nPkR`M! z0x=y8y)R!U;EHa7`pN_Z3&1G(l+oyK0M3mb=9z3An0@Hc3W{hc?ha8 z9NiP=$tvi_PU1uVCVa7PDUVuEY7R8|ne z6uTzi@PHe<+)TDIO8Qf|Z#yc-0~93v9s)u}z}f=~fM?)cX7?y+g~6AEjPtKmkfTXk z5#&CdN>e3`Q2yL`jhwQE{=%kh3{px**DKT=HbnH7u{3Z+CGg-j00$PO#MCt2 z*yN3B71ztVhyFAQO+X4>gLVAdv;!e=wA$=&;&S(Jkf!!G#C>J;_Jol&s;h@=7gZy_ zx*~4bY%4XnDT4hUYU$XEcn=S)-LcuJjAny{)rY1xHb@Wfimz+DlXzHi+F;NOpyT3> z58iPf$402f2}e}(6jAAfyqv*bR^9GekaCGc9eMeHwhKY*dDY$L0t7n!GZA=z_4uQc z=$avD1hhSF*U$FCKHSL5@~VH->`g}G zZA2xGOVe&1&f*^CRyLrm3&-e>H&T|OE{`G;AyG7QrOd@*@)k)jbETba+I?tjT7Npc zs3)-GGGu;i^c3>@vGrvAAz3g`;C@^NjDPt*I6ir@eF&&sX~SuLu$qLTV^1xtcVcAt z|KueG4aPEuFRS5Hi|`-J!QTfyeadLLaB8a%q(dln1SF?+95Z`5{#&prMkpjTEH@)0 z>0-k~)EIfclT=bNYzgr!Of{tr{~5K5RrF*vw9hcr$6ZGYQ_1P8Vjy#Z5xv*|mdf#xkQ7XUv#Q&RD_NzZ&LZrF`#kbTG6ulInMU; zV(pJBtm*q=+ufoVI*o5>l5JE1B=TVq^^|Vxm1BTmwKzViGi4Pxh-Mr2USMu^IyR=c zqA2Vk`;T^Q=uHO3nqZU_mF@4`ag|v}ra{Da&_WK3M2Z?BG z?&HclwrQ?62s|mA!GjWQ`T}}kO1&MLjGSS7_jJ+K=j7tdvv~n2)?yA3RJ7 zArVEpt@1I|Y2&+IB;#Xs$lK)E;xH$vD*DlF9Bn6rDD`$7skZeg9eGX!*hgwm&#AN0 zz(<9eg=`YX)l6%mPb)0}FY`n-h^;2h33NDh*wuhVGf-V#AFmF*j-3*$sMnAYImU|N zWijrdj^BtX@}hqF7kt}lSPE0ja|X06ZbEkFAZw0?{G%awW~OD-x5(*m23fUD-e0Ub zFH*_f>jfnNTi5*w3M9HPC&X|CezFig2RAFRgHC8*GB-&Ioqu z8zqhiLj<&Dh!j-g^MIZfzybNxE1kxidPnqZ{;B{ER{wVp%*Ku5`4FRH-~!r*394#2 z0YG(O9YFkC(%%dC@ZqKAmH0p)NX;BxMs^K(Lqw7@`a2i*3dp879XMG^iAR2G1fvfQBS%NnJY zAMki^BJ7kNa(*OUIA#S)M{9Q*5>{?buK&@ZS9jOxKdo5ctMTCYOE{TN4>>FZNxa{L39BCre;xB z&a(bRpq42FRQ08x{~WAixCEUe#J_#1)|e*=aRfEB6foNRDoMjLO?ZED(N+=?3cfU0 zsmv#&!EHD&WRi{`991&N{i8uMS6&Z>7w4llp@G%fo3z>ApH= z`wGY@FFV-SdGX`EZ$**1pT>;7j~|1!;$9oV8>dXq&P9=rFFQ@W-1XKMRejk?>DZ51 zh@1A=t;&JB&qr7~r?v0j3F@!+*+aI!mY>px3}ei+7mik5^jEJI2Mq}U8MX0~RO?#E zyLv(V&wtFHjjqeNJ)Q$MHU2%H7e1z>-b(Z#9WyHZRL1{P1Q-i5#hg#7Dnv@MB4UoV zFvh&b4|KzxSglg{i}2hCMib!W_|2svA^y$JT2bvD<-Xn6%WYL>*x2e@;dKoD`}6IU zQ^cQ=R|w;Bl2SQ_J*A!pxH+@Y2>5p&U{{r3y<1jt@$KK1JDaXelcV9R5s+;(Q;(f; zp0+~&oVQzkifw&+!hIs)QIy$0S~MNAbK=Suk`IZIX<&D56~oW|^S-+K#+FS1`C#Q4 z;N#Pkj%VY$7z_|MGR{hbDsT^M}?*^7iJXZE0(5svMQdxTkPz7v-8gDJ_?}9h@ z+0_!>&eU=)98%Zs%v!n82rS5{bkewR-q|HCCu$AH)Ts&UWdv0(aGTpm*^RBmZN)9d zRpPp_bA9-i%+)__n-@ayRmIo$GhJTpGFkn^S9v{-zPqdHUno@@R~c8oQup<#I8qg| z`&z5_Zj$dP@vQf`G9h8#4F_{?o|4=uK-^T4xrb>6hOHGx z3=<8Q5WlaEbB=9P64So>VrNfH_REd1>2V9NvusblOC=Yt`xP#=Q^sK5g+!+Wm~ z)*#*!yQuDhsU`xEb`t&KLOp1+4OR!0kAu1#f#BOR%vVwuT}ed8QpBa^!})>0Kw(Ez z^8|#}jBak@{qDZiRGI6~8b4{r&78VT_J#UUiC41~Y&|M&AFCRDRaT@7LbLNXiZbv3 zv`4_y7^auQ9`(9&w_1@O?XwstH$2i71CMj_-hjXnn3!xE&-EBV7u)u4x^(naL-VWa z7^oWio+T$LI0eS`UdMp-DVf*sZaPasGE!o0T`?A%90vsterI!(*9>q4EG z3reY5%%>sCh~q-Ma8cWfPEsPy*rx^bl}^B$8NC}vqW+Yw>c*S-nB5oB`57PGU-GhE zd&qKW$^4aSNAnu%HJx%Pc*jb1U&OWAu>SvRlLwgoJIndc(CR9XGcCqXoDyHZKq z2lAwdXLrcD$t-E)xsSaBCs|0>Qt*)-^ZfL|qxlDgFiy7S9qpk~GGoPl_XUU!El7ry zXp>(V2`9kx97IXPNXeOvR7O!vEllFZm)*VRz>u3;Je4NvNg1F>q=lVIKAoN=EHED~ z%=NQj;aX4t(iYwX4&+D>&|=VaCQI%)_@a#|Dx-{r0o+1?1-ZX>HRNHWG8whBpp)Ob;G!;>xnE;F=;h63B}&y``vNoe|SGHpZeCMH-vPS zYP# z%S$@|yfZ|+H5Kqj2yg2nR08R$56Ll7>(Ve-iPkV^k_MFLF3WrvG-dACb$`uNQ2tpx+?LNmWUgq_kwwab{f`h=~xZE+aYO zxn|Q~R`)UMf}OF2`Xo0H>USg}%(ayDO_Bou?3dgyhxZ}=%3F96mqSe_Z8$C29hpJL z<5hWh2nf*7y_~gEE8A4M&?vILaLKItOH9x@aUPimMV3o~)yTL3t70*Qo9N6QL{>4> z;UVe=pX1;5xKELk|9ZR3lf;u3?|D&eykNU$D3wFo?r(yoHn{MYNIPiM)LtwA z?Zdm`5JUarAtVHPq-0P&r4?+xiP<_?*C<`Mv71ph4?-`3E69?-xUW<@1?mf7ZE`JEU>ryfZ7##@4R0dISFVNeeBE z?T4~yC#G_h-JFC?!_B%qnmvBSq%f|D^Z?eladn11Y%^2LQI;1H zUSv)Azm4EEB%p*rAqU%3n(KW?6=XQ5a)OqXL2Jsf0{%&PwRr*3h6 z$=AOFE^nS>6gX!)M2qOUkuFP0bREUN?uyR*3|g6ZL#X2i97?4ld?G-BZ9naTqYDZA zm8ecz#~F$mbyt_QO}&uABd8Xc-7g-qWQkvI<13N3#tw!=W;`I0WtGVY zsK)n%Tq-+I^TFtgL#=-R%%LBVN|2CfPo)_4>NoMpBu=*OV7;vI#wV=_T0ZZvR&W@F zR10{fcI86g3@iDR;t#MAx;Yd15M}0>`_B0K!r?m52`w2_QC-v(Ree%}94Tym;w1PZ zXQ5Ws|=^MaIGL>hxj@{`b zTmMsiUS!G%MKJHnZg4aT3PgmIb3lM1zQ7>=FR_w7%}v}k!S!JniszT_#8WXFZA|Lz z8Ogpa+gB6pVN|OTYTxb*V)Pv&#ED@Wkdkis+FM3E2nE$tslmnO(H$qnnQZ zN(Hbms1L9E1hNw=CL2&v_^`j7yWd@Ko<>7fXUZutqtBo@AUY4HEX5u%d^=>SX2n}Q z3Pvv1%n}d_*d$*vHy%a@hM4*co7XIu!pAyON zJ^#2!2Wn;eQq{Pl6EQNi-h8tCalV8|S`9~<6Wp)Z!NQKB)4ik5|41Pozt1R6>QceV z0(#xGjeD&OUvVHS8DrA8}BZ4HR1ywK@mVoNOarXi_XRLXSO0q*a}Em}4)s6rcAW6HTqkrh3>!e2iF3iaib=ZS*Epa%dW| za~5Tg6b{yHsw$3bMle&gWu>iHk*8@QbVy>>=qp%^%Iw`nZO#+eO$T{^%OaYN$hnkmD^cpT^w zOY|98#sU6vR*2LSzgeiR4gN^m0o^qTtBbNQrE$d|j(ZDM9WEL| zV|-|N9deg6=3>1DFi2-dk&D03EW@A_p$aVhAVZUMbID4butU)0H3h-$6r z1*d}z1k8pZmcAKtSUYb9NBdTTls4#BQ1;!GMwK6BZKZg1F22hnr#`@M8c6fB4DG{* zu8_2bf@rO35KA%Oc!wFip(V{Ar@WuFc@Kg!j}krs&24o!P~Rm z?=Kru;`FH!$@IeB;)fv$)(QvJ<^8RoOBn~Pyke}eapWZRcNF=~3OFUT$yU(!EgggwhOx%aa4?*MWsS|P z9p*V#!L=Sy(L;m)--G$tTuB&JkGaWHcGVa}^l%d0RzD?-aD~`qbVEo1elXczS z^e`udHruomW{h3-E>xbtc=E_ji}N&Pjd5-JCN>{(bB=C>vTlX+>O`^QD$EtRi8C_`?w?)~=E_`G4;?;F2^d zVUggHf)^ry&g|K_!(m{H7;!|w*>_p=mwBdSyw77aml z*AOXuyO;dx-bvYZP;sP6;Q6jxc%cR}UonxCv_U107+S4>RB%PPjN}kDCs0IX_fqipnICxw z=?nMIffqE{AN+a7%rAezEeaaV3Q&7^nlZdbmvnXb{e4$OR zxi(;KeEDe!>8{XL>$s+=loeR~Qu3P%)$w|RPqI$7;cz%j5LAsZ$yp-nQ7 zEE!$MY3INj{?q2N8n`k%|W_M3p?+a)BU?&ojEIM z7KNndlyGx_nOy`X%bER-ZovxU7rs9C!WP6V=(&N#{Mos5Gk2q?2k@Nh;vu^}wY2Q@ zq4=9u)SD1;8Q<>#=3oWtZ3M1m@t98^Ev+8689HCu_lInH@R+cMmp69tl$k0MW&as; zaXNF#N6^2?9`XasIXiU~S5hbl%bG0@ZW+t}`7RvN5m8O;vb7995AF8qGRD5IQ0RlB zELlhJ6k3eGA|wt_2AmY&F{1wfGJ(7!`*v!BEV!Te%>)yGSL^a)55K)wQ{SsB_O_AS zCJA2nKx>JOEpTnG^AY4@%VbDOtcudW`TKjf5rQz}3}60;zH$z3;8ZAvi-tY)cUl4s zbOU*Eml;)|B0gZ@p4BW-cc`@r2fp2)n1XIr&w6q9!Z!ECbbHAcR{I)htZ+Bwm9flKZc+ zFOpCOgcZoEXZezUBBHvb*&)f8D!JMsjcgV05E=yl@LhqaX5E1-Ur?62?UFa6zZcHI z(`KSvR=XUK@qGIn^S`Sus1mu!L;mEYkyVBrxOP{tmWtF-z)dySl(#MzVF%R&fPlFw z7z*VQ-+_e&Xktenx<#qYUQSpHl(8&Nz+xz8{t}}SmI>j|$^2V4G?0Ez;ult!V}We1 zTdL9v02=H|(3Snf{&iirg#UF=fA5Um{l*q19;s5M0mUS>(iQc;5W7e$2~rHhfVocM4yFfBnv6vryu4a=l!zET9U ztOi+PJCL5{)(FKU-U+PWlFY2=#y{Q$LW9B(uumBaBOxlo-U&M95o_Qlo27@egvT7V z0Q#01)&JB=I!2nhV$dWmQv*+n)XheMV99eW6R}kHe<7U>0iQkHgXa%7&elnQF7gQK z?zTb|;S2>X&i3>b9b2-bqW~9w*dZJK z;Nhoo`AxlvORIcTc(;sHWN=$9a1=4bbV#?Qk$Zr_x)L#I$*H?LyEL2YYV+FrEA}2P z*wJF6`0k2_PmF(li6s~&6MCImT%9g;UT9hbpsTGcn24E>o4=0Q&s~)J>Q7R&ldvA=Ice26EhfV>ST^3@D}D*Uo}*u>I%8q zs{D?=R1+`tzT09Lo>eSbUE`3H(!&u}Uf25$dv5NWpERSAMl3MBJl7-@-?zosa_5@C zKI+OfzwAF32l`F!oM0UR(xtDs+`63cSetQT{iHrR4xcm5T!9I;NP0#Kbl1gN1GNu9 zJ=Mc0cGMe$-u>fENXdmPN=^NpUR zsIYgm#e(016zLO$e}Tmz3>;cmd(RN`_M*&-Sr;GTeXSHB%_}Yg>(n!^c&GRs7Yfw6I0<@lu z3Ba>oR8R!h$pEPAf{J67=>rVCi9ufzBF^*_8lcy&g>kwC^=W{XFh^BzK@|vrzOcBX zA)*mtsSWI|q}VrUd^j%)YFYR~S5M2s93G;G>|?t9Ht>L60f6Qtt(~S6*-P?suuwk(L80K+lnD59ERxq! zCLw)P?8mUk#Jm|WM$Ji%yY}ZGi$AyySnR)HPxG1>QKVn%Mv#Zm$3en z+?tsJ8CvM#MkDDJFv3y8mnE*?F7MAZ_kWL+(}pZSLlKK&Q(>sm#&wbL>FNO7!%65E zm@@?m(Hqj~fvKqA9YD!YQG`7gkgUah5vXY`4p4Y`Mpkl^a*pLtDd||$tu>e-lqeSg z z1`y-`U+W_=OpuM!5dM-aMc~1r>5KClC$WeHj!R{}ZXpwn3jQ!mDw08L>aY>g99r&t z2+C?x%wj{VbI3=Y(Aaw>4@BNC8*(y)a$N!ycu!#w3@TGR`PBlc6AcjC0LMub7))A| zY{3%1*OVZ(8A;R*qPH{=6s=`D!j2F~Ol1*APv%PrxGzKK~(*InaP+|( zRf&|SmPSQ=0)IRPUzw#-ZlRAC+&wjCgy2Ui-_-Kct&i`mC%K`IyDwZ-{Ub=gT^a2; zL7H_|5yGf*Dubh-+#^Sog)xtPRD}wR6k;E2?-O{f;>%J%tpNX;-(LHX?_P1@!bBy$ zcxa&`$flx$LkV*i!Oe$$D9Hm+ID%CPB)oY*%uG;&=f6naI*`eg8?zsEz716a-`*-g zZXoudiRySei4*$mf#7^yJRn&1UcN>~hkU`N80@59iC1gLXz zj*iZyC~uXxj{qOeqaV>H6*AmMEls+Lyf3%DoO0-0efya#{@{UsxSP+9eIUQFk8{eY zC4E%Cbuf&(r~=q~>X81JHyA2nxq;bbD@Eie-&$uZ=N9Ef8fj{m>@Pe?50f(RsELn{tsZsPi8OvOzqu*(XcFHSXw1F|T$JD)&6$E0MNO5-(D86Gj^I zrlW$ll>nuQ|F%4La#Lh7_~%J`?RxY0BNJWq97~%~y_vr}`RJhnq1kX7Yd4jsp9Z?G zFW6Uxur^0IRovDr1u?)E9Wz2rmVfo;&7K9vY`#kF^C$9m1jisBr_ZZHLgscEOh9qUct`e zanA}VR>)tZz%8W$bRG*F8o(QfmPxQGZz-zW39`vrk^16NGzc=maATxY#QY*y;DeVs z2=_)931%P-B&UJqIK^2=iwa~25h3tTB0f7T2QGyl-FGy;swsY9zxD+iB0t@4hM;S2 zSpYLWWX0o9(vl!Xpv}J{q!2_iA{qXMST}@&)9OHAc|*cc z+ZcccHnPoHQm~Au8y7O+?ETc&VsnHa3SihF^2*sgq9T@F&U)ibj<*gJMJb)!LH-G6 zRW)-U_*kF=lSWeb>*=5BnkS@Gf8<0{BLE=56%A z+k4730M}wJCiS`t-rCI>aAc~yW$Xm*7Y65uaw&iEP!L{@1{pEq80n*OCn^m6hMdGZ zv)z#*wxxDN%*8a2;pqYvvdJaG!+WaB3*?B<G^P?Nvj*tUA*ttuTYo#c`e|s;|xJjU%PQbr7aOR!yJBU=8;r4WVHz9qf0W#X8 zvN;@fC;1r-0rr8(x7z`WSsR3pA%HLLR%C@mx~BEsaZo7H6JC{yR=OWVcoAH7N zF?6=5sQ=2wOt;l4>n2_2(C6NisMxzsMw2|+EhhsV(tC61um`Oi2j|#cR#@B4)#wd? znw3zh9{PR=64l_`(Z@V95CFRTT*^TjUZ1j(Do9z96!bABGJdf7lre9|-Y!oA_$0H- zX9u-%jH>M&F4HEAmfb0hf!O7hiI1#j?-q0QR)Z3*@M|?{xS1?PX(MLbuzc6DJ%Z_f z1YoEA5|jkiGJ$j{zANpb<#9A`hEy0-y0lv>7^I^J2XTiYtk$;B76AL%7h0Z9|GLi} z;U%0wNV<00(XYxjSz_DPNS^J|+STce7Hy>zsS2UungOL0i#7;$gG&nNM-5^MKEh;9 z8EA^gP(u~wQTx&`RDu4TU^KZT294W9n$F)zZt7eII0>%3Cwh~Xa^x25ZTf!Nm)(R@ zr}H*V22Cp0yje!xf&fbW*yWv)ob_4OSr?M*#4lu#fnCG}?2zsdkeQ+>pG~7U?U+MG z!}zE24Zn*e$;UH%Lf?44+B%(#mKp09lGPn{!r%Ji8AwS!Wy<2a-OK)*0*gd5)=c=% z=XPTOg6-tSQP&?ccq8Ni2gQHT7L<*_T}yFjA@QX9#GZ-GMgaWrwuY-~Pm1-GmFMzC z^rYR&oVBM*keXRfY(c>ZJ@bp|&?Y5mgu<3xQR| zgB8CWlkr)&ez7=IRPZmiJ35F0(zhrkj#bR~E4y=lv$sSeYVNr<1zKgj7qrP8a-3e5 z4U&E{UIsT^>*AUMOEMx&gD<)REsdYT<9552IbGkAMYWw2WR!C(UAU)xy9#k{CzDd|~v7G1Olg)mPps{HKZ} zDrwR;rOk4elkRl*q@Gkk@uU-W>8$kEuG`g#?YqoN3UR{4FQUw;w*`Z+PQ4bjHZ zU@dR)Hb5N$I&ekqb~w3iMW;`RPr)Mg#I8xyQ*^ZpSoXnA>~#9~Tje$9^qK%{=So*w zQIU>xys(-xnfsdVH+aRCtn8P`M&pXjbFPDSwQtRW!8G)uQAu8FRsH)}d85`d@FKe| zPy5w8&o%qL?nJSAa;))D*|1!$%T-tRab7Z~7;qW;oHAn`nDOzR+6b^!OyY;G+@#+Z>m!b7aL+ z0>~Kqp-GrpJ$B~G`RBr(7f7tVi*@`TBWq9Y&JNPlg`*IjGIi6JmeE|*esOl%p`8%3 z)0C`__Ks%r!c$dlM(o4ugY^3@fQnX0YE9oZt3PYEEbTF)Adr_&K~ELGg$%!z=2b?| z#j`}qZavW5a`AJ*{p0HDa6vwOvL3rK2@n|dPCdiZ|Vv8Ha?veWCZ%R3@q z=~LIoFn-FGH&5ee=t&Sw`NSyOm%FbZ36h&e-T}J5hT+I!j?#TAWA_5q zfL(6wgshwl#0QyXtx@Nr&_D(l1Jv3>fk#(aafYz3A+uK*Liy%HSrTW2>12j{y>XH z;p(dG8oCa*z;;qH&J7H6#?G1I+B|6WsR5%D$o#@%`Q*||ur^5lUQgP%3AZaR2owZ7 zCztM|15-EEs?k_(wW_-q0b*`ow{or6$$~#~llQQgIoR0vQ#dk`)G$DIY(uKlRKlXO zHcUC%RsgD-4p9*VKu?HXxr#k{{{O zeQa#OZoiYepX!WbHFO$2L8^TJ!|IUQ$>cAnp+v>R;*qjAI**%Z$5C|I##0ruljz!& zl{5RwDn`2v_+JIW0KmujX@($YZ*|@6`0zTE;=atA1mp_Fcguv8@}9%NX=`Ru)4?XAGvHI>?C>MPNaUAQG6wcWu1VC^cSv7K^Jp9Q{?$_?1r z7Qx>2J9m(T|CKz@JbChre>$z zeVn1WI`OX-5Do(eW}AXMO@A#yp42SgC-cl|FNLee=9wJ! zz@w5omL=i6XIwoOYjiGJnYx3bH+U+)J&k2+$I

sT22WZ$;37ANwuycFo-%kO*)= ziFVT}a0PHsj`q4*a0gHt4iXv-OC1sgTTe?8HWoHET9RMRrtUUwmZl`0macBLPL3p8 zOzcb?8RGTeqTuW-|F=3iqob;P^dHmjT>agl%d+7?BOyPUUUVqdf?6T8bTt`~t2{(f zx?u}`)lUCy+;xZ20fSwsT!2V?e_a3j$zx5*K&KVt;TB6B_Acl<6|m8)2V|6E352&> zFxa5RN+A#4mW4DK7*dZ?fPc#3713i|z-4xLnB_O$UK*DFuvvFme*OBjvr__jmVc^u z4c%e+@sBr`x3}NjG{2pG+cr1N_PN=8__SF)WOnIEvs-T4mu|B~=L_7n&xp6%U3dIc zZ_&#vKd=3S0}}t*K6Fnzw4`#e->;XOhj#slh;+!!=F7T8uwmQ+i+{yGP@PE@}Js=9lJBOJ6UCm#-l*E5x|e78-<AQLnD)YsnD%ReWdGy7+BSdCIU4VnTPnj+K3FPMw9?ZIR~G$B-wElJ zesaPCwYlaKar1r9qg=syF|q@Z9^!lmU?{n9nt z_qLU|-wO{CCWi>tW`+nFAxA-&uW!m1e9f@bF!3tR+{aDiS)4Xe$cT{47bXJ8QB_0$ zIa5njhz{s6BK9wB)9W0YbnRv1^uHyIH@tl|eNEsXD2W z$}n*pH&N&BeFW$EfEYnaSB^p3+G7w69f?H{O$9Rs(O5A#IR-ig!Fwd*j);jmtXPiJ z3EP)u3}SH##vm4_$}xz=mBqYdeJ~83l`P1SQh$!=(UEeZ4oUT_O_pd79CG@1c=r-( z{{`Si@T2gf^rPB$h>x4PC-*P={-6YRuG#++ywQY7t^OnfcYw`lNiyJ4qO2 z$2ET9ZXPrDF72saoSt4#T3XjuRquLJExpo-p&uX-BL;>{2oo{z4M@ZUKS3hK5>q)?VwZ=WH{xziw7x8MDOP3SX6`Gv;M`Ne(h#g>DZi0YzYyZZ~NQ$bvPx zI#Mwx0qbUi9NL#@+aE)#ksT^!i5k+)6xvT({bX(}Ex!eJ&=(2RAL^l`_ zWpsK(lk&FMO2;gT7Q{-UoKDkgGwd=d=~zLcA7UR}1D%#u4;tv2=(PGAXrybU)3)}5 zCb|NhcHRtH=nm28Cus!-K;A8Rksd{MC`IYR6y+avC`Z$vX_0s1@~0C~^`^m%Ca h_%%`_instrtype(`%`_resulttype(t'^n{t' <- `t'*`},), x'*{x' <- `x'*`}, `%`_resulttype(t*{t <- `t*`},))) -- Instrs_ok2: `%;%|-%:%`(s, {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [`%`_resulttype(t'^n{t' <- `t'*`},)], RETURN ?(), REFS [], RECS []} +++ C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype([],), x*{x <- `x*`}, `%`_resulttype(t*{t <- `t*`},))) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:37.1-42.35 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:37.1-41.35 rule frame{s : store, C : context, n : n, f : frame, `instr*` : instr*, `t*` : valtype*, C' : context}: `%;%|-%:%`(s, C, `FRAME_%{%}%`_instr(n, f, instr*{instr <- `instr*`}), `%->_%%`_instrtype(`%`_resulttype([],), [], `%`_resulttype(t^n{t <- `t*`},))) -- Frame_ok: `%|-%:%`(s, f, C') - -- if (C'.RETURN_context = ?(`%`_resulttype(t^n{t <- `t*`},))) - -- Expr_ok2: `%;%|-%:%`(s, C', instr*{instr <- `instr*`}, `%`_resulttype(t^n{t <- `t*`},)) + -- Expr_ok2: `%;%|-%:%`(s, {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(`%`_resulttype(t^n{t <- `t*`},)), REFS [], RECS []} +++ C', instr*{instr <- `instr*`}, `%`_resulttype(t^n{t <- `t*`},)) -- Resulttype_ok: `%|-%:OK`({TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS [], RECS []}, `%`_resulttype(t^n{t <- `t*`},)) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:44.1-47.49 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:43.1-46.49 rule handler{s : store, C : context, n : n, `catch*` : catch*, `instr*` : instr*, `t*` : valtype*, `x*` : idx*}: `%;%|-%:%`(s, C, `HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, instr*{instr <- `instr*`}), `%->_%%`_instrtype(`%`_resulttype([],), [], `%`_resulttype(t*{t <- `t*`},))) -- (Catch_ok: `%|-%:OK`(C, catch))*{catch <- `catch*`} -- Instrs_ok2: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype([],), x*{x <- `x*`}, `%`_resulttype(t*{t <- `t*`},))) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:49.1-51.42 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:48.1-50.42 rule trap{s : store, C : context, `t_1*` : valtype*, `t_2*` : valtype*}: `%;%|-%:%`(s, C, TRAP_instr, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), [], `%`_resulttype(t_2*{t_2 <- `t_2*`},))) -- Instrtype_ok: `%|-%:OK`(C, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), [], `%`_resulttype(t_2*{t_2 <- `t_2*`},))) ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:5.1-6.36 relation Instrs_ok2: `%;%|-%:%`(store, context, instr*, instrtype) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:54.1-55.27 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:53.1-54.27 rule empty{s : store, C : context}: `%;%|-%:%`(s, C, [], `%->_%%`_instrtype(`%`_resulttype([],), [], `%`_resulttype([],))) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:57.1-61.86 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:56.1-60.86 rule seq{s : store, C : context, instr_1 : instr, `instr_2*` : instr*, `t_1*` : valtype*, `x_1*` : idx*, `x_2*` : idx*, `t_3*` : valtype*, `t_2*` : valtype*, `init*` : init*, `t*` : valtype*}: `%;%|-%:%`(s, C, [instr_1] ++ instr_2*{instr_2 <- `instr_2*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x_1*{x_1 <- `x_1*`} ++ x_2*{x_2 <- `x_2*`}, `%`_resulttype(t_3*{t_3 <- `t_3*`},))) -- Instr_ok2: `%;%|-%:%`(s, C, instr_1, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x_1*{x_1 <- `x_1*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},))) -- (if (C.LOCALS_context[x_1!`%`_idx.0] = `%%`_localtype(init, t)))*{init <- `init*`, t <- `t*`, x_1 <- `x_1*`} -- Instrs_ok2: `%;%|-%:%`(s, $with_locals(C, x_1*{x_1 <- `x_1*`}, `%%`_localtype(SET_init, t)*{t <- `t*`}), instr_2*{instr_2 <- `instr_2*`}, `%->_%%`_instrtype(`%`_resulttype(t_2*{t_2 <- `t_2*`},), x_2*{x_2 <- `x_2*`}, `%`_resulttype(t_3*{t_3 <- `t_3*`},))) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:63.1-67.33 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:62.1-66.33 rule sub{s : store, C : context, `instr*` : instr*, it' : instrtype, it : instrtype}: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, it') -- Instrs_ok2: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, it) -- Instrtype_sub: `%|-%<:%`(C, it, it') -- Instrtype_ok: `%|-%:OK`(C, it') - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:70.1-73.33 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:69.1-72.33 rule frame{s : store, C : context, `instr*` : instr*, `t*` : valtype*, `t_1*` : valtype*, `x*` : idx*, `t_2*` : valtype*}: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t*{t <- `t*`} ++ t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t*{t <- `t*`} ++ t_2*{t_2 <- `t_2*`},))) -- Instrs_ok2: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},))) @@ -8333,7 +8332,7 @@ relation Instrs_ok2: `%;%|-%:%`(store, context, instr*, instrtype) ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:7.1-8.36 relation Expr_ok2: `%;%|-%:%`(store, context, expr, resulttype) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:76.1-78.44 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:75.1-77.44 rule _{s : store, C : context, `instr*` : instr*, `t*` : valtype*}: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%`_resulttype(t*{t <- `t*`},)) -- Instrs_ok2: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype([],), [], `%`_resulttype(t*{t <- `t*`},))) @@ -8409,30 +8408,30 @@ relation Exninst_ok: `%|-%:OK`(store, exninst) ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec rec { -;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:226.1-227.50 +;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:225.1-226.50 relation ImmutReachable: `%>>_%%`(fieldval, store, fieldval) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:240.1-243.35 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:239.1-242.35 rule trans{fv_1 : fieldval, s : store, fv_2 : fieldval, fv' : fieldval}: `%>>_%%`(fv_1, s, fv_2) -- ImmutReachable: `%>>_%%`(fv_1, s, fv') -- ImmutReachable: `%>>_%%`(fv', s, fv_2) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:245.1-248.20 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:244.1-247.20 rule `ref.struct`{a : addr, s : store, i : nat, `ft*` : fieldtype*, zt : storagetype}: `%>>_%%`(`REF.STRUCT_ADDR`_fieldval(a), s, s.STRUCTS_store[a].FIELDS_structinst[i]) -- Expand: `%~~%`(s.STRUCTS_store[a].TYPE_structinst, STRUCT_comptype(`%`_list(ft*{ft <- `ft*`},))) -- if (ft*{ft <- `ft*`}[i] = `%%`_fieldtype(?(), zt)) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:250.1-252.42 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:249.1-251.42 rule `ref.array`{a : addr, s : store, i : nat, zt : storagetype}: `%>>_%%`(`REF.ARRAY_ADDR`_fieldval(a), s, s.ARRAYS_store[a].FIELDS_arrayinst[i]) -- Expand: `%~~%`(s.ARRAYS_store[a].TYPE_arrayinst, ARRAY_comptype(`%%`_fieldtype(?(), zt))) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:254.1-255.44 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:253.1-254.44 rule `ref.exn`{a : addr, s : store, i : nat}: `%>>_%%`(`REF.EXN_ADDR`_fieldval(a), s, (s.EXNS_store[a].FIELDS_exninst[i] : val <: fieldval)) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:257.1-258.28 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:256.1-257.28 rule `ref.extern`{ref : ref, s : store}: `%>>_%%`(`REF.EXTERN`_fieldval(ref), s, (ref : ref <: fieldval)) } diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index 2380d7f35c..7daad7f869 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md @@ -14239,9 +14239,7 @@ $$ \frac{ s \vdash f : {C'} \qquad -{C'}{.}\mathsf{return} = {t^{n}} - \qquad -s ; {C'} \vdash {{\mathit{instr}}^\ast} : {t^{n}} +s ; \{ \mathsf{return}~{t^{n}} \} \oplus {C'} \vdash {{\mathit{instr}}^\ast} : {t^{n}} \qquad \{ \} \vdash {t^{n}} : \mathsf{ok} }{ diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md index 758438c24a..d3377103db 100644 --- a/spectec/test-middlend/TEST.md +++ b/spectec/test-middlend/TEST.md @@ -7809,46 +7809,45 @@ relation Instr_ok2: `%;%|-%:%`(store, context, instr, instrtype) -- Instrs_ok2: `%;%|-%:%`(s, C, instr'*{instr' <- `instr'*`}, `%->_%%`_instrtype(`%`_resulttype(t'^n{t' <- `t'*`},), x'*{x' <- `x'*`}, `%`_resulttype(t*{t <- `t*`},))) -- Instrs_ok2: `%;%|-%:%`(s, {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [`%`_resulttype(t'^n{t' <- `t'*`},)], RETURN ?(), REFS [], RECS []} +++ C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype([],), x*{x <- `x*`}, `%`_resulttype(t*{t <- `t*`},))) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:37.1-42.35 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:37.1-41.35 rule frame{s : store, C : context, n : n, f : frame, `instr*` : instr*, `t*` : valtype*, C' : context}: `%;%|-%:%`(s, C, `FRAME_%{%}%`_instr(n, f, instr*{instr <- `instr*`}), `%->_%%`_instrtype(`%`_resulttype([],), [], `%`_resulttype(t^n{t <- `t*`},))) -- Frame_ok: `%|-%:%`(s, f, C') - -- if (C'.RETURN_context = ?(`%`_resulttype(t^n{t <- `t*`},))) - -- Expr_ok2: `%;%|-%:%`(s, C', instr*{instr <- `instr*`}, `%`_resulttype(t^n{t <- `t*`},)) + -- Expr_ok2: `%;%|-%:%`(s, {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(`%`_resulttype(t^n{t <- `t*`},)), REFS [], RECS []} +++ C', instr*{instr <- `instr*`}, `%`_resulttype(t^n{t <- `t*`},)) -- Resulttype_ok: `%|-%:OK`({TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS [], RECS []}, `%`_resulttype(t^n{t <- `t*`},)) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:44.1-47.49 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:43.1-46.49 rule handler{s : store, C : context, n : n, `catch*` : catch*, `instr*` : instr*, `t*` : valtype*, `x*` : idx*}: `%;%|-%:%`(s, C, `HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, instr*{instr <- `instr*`}), `%->_%%`_instrtype(`%`_resulttype([],), [], `%`_resulttype(t*{t <- `t*`},))) -- (Catch_ok: `%|-%:OK`(C, catch))*{catch <- `catch*`} -- Instrs_ok2: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype([],), x*{x <- `x*`}, `%`_resulttype(t*{t <- `t*`},))) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:49.1-51.42 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:48.1-50.42 rule trap{s : store, C : context, `t_1*` : valtype*, `t_2*` : valtype*}: `%;%|-%:%`(s, C, TRAP_instr, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), [], `%`_resulttype(t_2*{t_2 <- `t_2*`},))) -- Instrtype_ok: `%|-%:OK`(C, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), [], `%`_resulttype(t_2*{t_2 <- `t_2*`},))) ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:5.1-6.36 relation Instrs_ok2: `%;%|-%:%`(store, context, instr*, instrtype) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:54.1-55.27 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:53.1-54.27 rule empty{s : store, C : context}: `%;%|-%:%`(s, C, [], `%->_%%`_instrtype(`%`_resulttype([],), [], `%`_resulttype([],))) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:57.1-61.86 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:56.1-60.86 rule seq{s : store, C : context, instr_1 : instr, `instr_2*` : instr*, `t_1*` : valtype*, `x_1*` : idx*, `x_2*` : idx*, `t_3*` : valtype*, `t_2*` : valtype*, `init*` : init*, `t*` : valtype*}: `%;%|-%:%`(s, C, [instr_1] ++ instr_2*{instr_2 <- `instr_2*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x_1*{x_1 <- `x_1*`} ++ x_2*{x_2 <- `x_2*`}, `%`_resulttype(t_3*{t_3 <- `t_3*`},))) -- Instr_ok2: `%;%|-%:%`(s, C, instr_1, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x_1*{x_1 <- `x_1*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},))) -- (if (C.LOCALS_context[x_1!`%`_idx.0] = `%%`_localtype(init, t)))*{init <- `init*`, t <- `t*`, x_1 <- `x_1*`} -- Instrs_ok2: `%;%|-%:%`(s, $with_locals(C, x_1*{x_1 <- `x_1*`}, `%%`_localtype(SET_init, t)*{t <- `t*`}), instr_2*{instr_2 <- `instr_2*`}, `%->_%%`_instrtype(`%`_resulttype(t_2*{t_2 <- `t_2*`},), x_2*{x_2 <- `x_2*`}, `%`_resulttype(t_3*{t_3 <- `t_3*`},))) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:63.1-67.33 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:62.1-66.33 rule sub{s : store, C : context, `instr*` : instr*, it' : instrtype, it : instrtype}: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, it') -- Instrs_ok2: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, it) -- Instrtype_sub: `%|-%<:%`(C, it, it') -- Instrtype_ok: `%|-%:OK`(C, it') - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:70.1-73.33 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:69.1-72.33 rule frame{s : store, C : context, `instr*` : instr*, `t*` : valtype*, `t_1*` : valtype*, `x*` : idx*, `t_2*` : valtype*}: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t*{t <- `t*`} ++ t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t*{t <- `t*`} ++ t_2*{t_2 <- `t_2*`},))) -- Instrs_ok2: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},))) @@ -7856,7 +7855,7 @@ relation Instrs_ok2: `%;%|-%:%`(store, context, instr*, instrtype) ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:7.1-8.36 relation Expr_ok2: `%;%|-%:%`(store, context, expr, resulttype) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:76.1-78.44 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:75.1-77.44 rule _{s : store, C : context, `instr*` : instr*, `t*` : valtype*}: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%`_resulttype(t*{t <- `t*`},)) -- Instrs_ok2: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype([],), [], `%`_resulttype(t*{t <- `t*`},))) @@ -7932,30 +7931,30 @@ relation Exninst_ok: `%|-%:OK`(store, exninst) ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec rec { -;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:226.1-227.50 +;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:225.1-226.50 relation ImmutReachable: `%>>_%%`(fieldval, store, fieldval) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:240.1-243.35 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:239.1-242.35 rule trans{fv_1 : fieldval, s : store, fv_2 : fieldval, fv' : fieldval}: `%>>_%%`(fv_1, s, fv_2) -- ImmutReachable: `%>>_%%`(fv_1, s, fv') -- ImmutReachable: `%>>_%%`(fv', s, fv_2) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:245.1-248.20 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:244.1-247.20 rule `ref.struct`{a : addr, s : store, i : nat, `ft*` : fieldtype*, zt : storagetype}: `%>>_%%`(`REF.STRUCT_ADDR`_fieldval(a), s, s.STRUCTS_store[a].FIELDS_structinst[i]) -- Expand: `%~~%`(s.STRUCTS_store[a].TYPE_structinst, STRUCT_comptype(`%`_list(ft*{ft <- `ft*`},))) -- if (ft*{ft <- `ft*`}[i] = `%%`_fieldtype(?(), zt)) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:250.1-252.42 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:249.1-251.42 rule `ref.array`{a : addr, s : store, i : nat, zt : storagetype}: `%>>_%%`(`REF.ARRAY_ADDR`_fieldval(a), s, s.ARRAYS_store[a].FIELDS_arrayinst[i]) -- Expand: `%~~%`(s.ARRAYS_store[a].TYPE_arrayinst, ARRAY_comptype(`%%`_fieldtype(?(), zt))) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:254.1-255.44 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:253.1-254.44 rule `ref.exn`{a : addr, s : store, i : nat}: `%>>_%%`(`REF.EXN_ADDR`_fieldval(a), s, (s.EXNS_store[a].FIELDS_exninst[i] : val <: fieldval)) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:257.1-258.28 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:256.1-257.28 rule `ref.extern`{ref : ref, s : store}: `%>>_%%`(`REF.EXTERN`_fieldval(ref), s, (ref : ref <: fieldval)) } @@ -19720,46 +19719,45 @@ relation Instr_ok2: `%;%|-%:%`(store, context, instr, instrtype) -- Instrs_ok2: `%;%|-%:%`(s, C, instr'*{instr' <- `instr'*`}, `%->_%%`_instrtype(`%`_resulttype(t'^n{t' <- `t'*`},), x'*{x' <- `x'*`}, `%`_resulttype(t*{t <- `t*`},))) -- Instrs_ok2: `%;%|-%:%`(s, {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [`%`_resulttype(t'^n{t' <- `t'*`},)], RETURN ?(), REFS [], RECS []} +++ C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype([],), x*{x <- `x*`}, `%`_resulttype(t*{t <- `t*`},))) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:37.1-42.35 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:37.1-41.35 rule frame{s : store, C : context, n : n, f : frame, `instr*` : instr*, `t*` : valtype*, C' : context}: `%;%|-%:%`(s, C, `FRAME_%{%}%`_instr(n, f, instr*{instr <- `instr*`}), `%->_%%`_instrtype(`%`_resulttype([],), [], `%`_resulttype(t^n{t <- `t*`},))) -- Frame_ok: `%|-%:%`(s, f, C') - -- if (C'.RETURN_context = ?(`%`_resulttype(t^n{t <- `t*`},))) - -- Expr_ok2: `%;%|-%:%`(s, C', instr*{instr <- `instr*`}, `%`_resulttype(t^n{t <- `t*`},)) + -- Expr_ok2: `%;%|-%:%`(s, {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(`%`_resulttype(t^n{t <- `t*`},)), REFS [], RECS []} +++ C', instr*{instr <- `instr*`}, `%`_resulttype(t^n{t <- `t*`},)) -- Resulttype_ok: `%|-%:OK`({TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS [], RECS []}, `%`_resulttype(t^n{t <- `t*`},)) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:44.1-47.49 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:43.1-46.49 rule handler{s : store, C : context, n : n, `catch*` : catch*, `instr*` : instr*, `t*` : valtype*, `x*` : idx*}: `%;%|-%:%`(s, C, `HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, instr*{instr <- `instr*`}), `%->_%%`_instrtype(`%`_resulttype([],), [], `%`_resulttype(t*{t <- `t*`},))) -- (Catch_ok: `%|-%:OK`(C, catch))*{catch <- `catch*`} -- Instrs_ok2: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype([],), x*{x <- `x*`}, `%`_resulttype(t*{t <- `t*`},))) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:49.1-51.42 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:48.1-50.42 rule trap{s : store, C : context, `t_1*` : valtype*, `t_2*` : valtype*}: `%;%|-%:%`(s, C, TRAP_instr, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), [], `%`_resulttype(t_2*{t_2 <- `t_2*`},))) -- Instrtype_ok: `%|-%:OK`(C, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), [], `%`_resulttype(t_2*{t_2 <- `t_2*`},))) ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:5.1-6.36 relation Instrs_ok2: `%;%|-%:%`(store, context, instr*, instrtype) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:54.1-55.27 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:53.1-54.27 rule empty{s : store, C : context}: `%;%|-%:%`(s, C, [], `%->_%%`_instrtype(`%`_resulttype([],), [], `%`_resulttype([],))) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:57.1-61.86 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:56.1-60.86 rule seq{s : store, C : context, instr_1 : instr, `instr_2*` : instr*, `t_1*` : valtype*, `x_1*` : idx*, `x_2*` : idx*, `t_3*` : valtype*, `t_2*` : valtype*, `init*` : init*, `t*` : valtype*}: `%;%|-%:%`(s, C, [instr_1] ++ instr_2*{instr_2 <- `instr_2*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x_1*{x_1 <- `x_1*`} ++ x_2*{x_2 <- `x_2*`}, `%`_resulttype(t_3*{t_3 <- `t_3*`},))) -- Instr_ok2: `%;%|-%:%`(s, C, instr_1, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x_1*{x_1 <- `x_1*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},))) -- (if (C.LOCALS_context[x_1!`%`_idx.0] = `%%`_localtype(init, t)))*{init <- `init*`, t <- `t*`, x_1 <- `x_1*`} -- Instrs_ok2: `%;%|-%:%`(s, $with_locals(C, x_1*{x_1 <- `x_1*`}, `%%`_localtype(SET_init, t)*{t <- `t*`}), instr_2*{instr_2 <- `instr_2*`}, `%->_%%`_instrtype(`%`_resulttype(t_2*{t_2 <- `t_2*`},), x_2*{x_2 <- `x_2*`}, `%`_resulttype(t_3*{t_3 <- `t_3*`},))) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:63.1-67.33 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:62.1-66.33 rule sub{s : store, C : context, `instr*` : instr*, it' : instrtype, it : instrtype}: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, it') -- Instrs_ok2: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, it) -- Instrtype_sub: `%|-%<:%`(C, it, it') -- Instrtype_ok: `%|-%:OK`(C, it') - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:70.1-73.33 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:69.1-72.33 rule frame{s : store, C : context, `instr*` : instr*, `t*` : valtype*, `t_1*` : valtype*, `x*` : idx*, `t_2*` : valtype*}: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t*{t <- `t*`} ++ t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t*{t <- `t*`} ++ t_2*{t_2 <- `t_2*`},))) -- Instrs_ok2: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},))) @@ -19767,7 +19765,7 @@ relation Instrs_ok2: `%;%|-%:%`(store, context, instr*, instrtype) ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:7.1-8.36 relation Expr_ok2: `%;%|-%:%`(store, context, expr, resulttype) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:76.1-78.44 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:75.1-77.44 rule _{s : store, C : context, `instr*` : instr*, `t*` : valtype*}: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%`_resulttype(t*{t <- `t*`},)) -- Instrs_ok2: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype([],), [], `%`_resulttype(t*{t <- `t*`},))) @@ -19843,30 +19841,30 @@ relation Exninst_ok: `%|-%:OK`(store, exninst) ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec rec { -;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:226.1-227.50 +;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:225.1-226.50 relation ImmutReachable: `%>>_%%`(fieldval, store, fieldval) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:240.1-243.35 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:239.1-242.35 rule trans{fv_1 : fieldval, s : store, fv_2 : fieldval, fv' : fieldval}: `%>>_%%`(fv_1, s, fv_2) -- ImmutReachable: `%>>_%%`(fv_1, s, fv') -- ImmutReachable: `%>>_%%`(fv', s, fv_2) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:245.1-248.20 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:244.1-247.20 rule `ref.struct`{a : addr, s : store, i : nat, `ft*` : fieldtype*, zt : storagetype}: `%>>_%%`(`REF.STRUCT_ADDR`_fieldval(a), s, s.STRUCTS_store[a].FIELDS_structinst[i]) -- Expand: `%~~%`(s.STRUCTS_store[a].TYPE_structinst, STRUCT_comptype(`%`_list(ft*{ft <- `ft*`},))) -- if (ft*{ft <- `ft*`}[i] = `%%`_fieldtype(?(), zt)) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:250.1-252.42 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:249.1-251.42 rule `ref.array`{a : addr, s : store, i : nat, zt : storagetype}: `%>>_%%`(`REF.ARRAY_ADDR`_fieldval(a), s, s.ARRAYS_store[a].FIELDS_arrayinst[i]) -- Expand: `%~~%`(s.ARRAYS_store[a].TYPE_arrayinst, ARRAY_comptype(`%%`_fieldtype(?(), zt))) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:254.1-255.44 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:253.1-254.44 rule `ref.exn`{a : addr, s : store, i : nat}: `%>>_%%`(`REF.EXN_ADDR`_fieldval(a), s, (s.EXNS_store[a].FIELDS_exninst[i] : val <: fieldval)) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:257.1-258.28 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:256.1-257.28 rule `ref.extern`{ref : ref, s : store}: `%>>_%%`(`REF.EXTERN`_fieldval(ref), s, (ref : ref <: fieldval)) } @@ -31830,32 +31828,31 @@ relation Instr_ok2: `%;%|-%:%`(store, context, instr, instrtype) -- Instrs_ok2: `%;%|-%:%`(s, C, instr'*{instr' <- `instr'*`}, `%->_%%`_instrtype(`%`_resulttype(t'^n{t' <- `t'*`},), x'*{x' <- `x'*`}, `%`_resulttype(t*{t <- `t*`},))) -- Instrs_ok2: `%;%|-%:%`(s, {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [`%`_resulttype(t'^n{t' <- `t'*`},)], RETURN ?(), REFS [], RECS []} +++ C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype([],), x*{x <- `x*`}, `%`_resulttype(t*{t <- `t*`},))) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:37.1-42.35 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:37.1-41.35 rule frame{s : store, C : context, n : n, f : frame, `instr*` : instr*, `t*` : valtype*, C' : context}: `%;%|-%:%`(s, C, `FRAME_%{%}%`_instr(n, f, instr*{instr <- `instr*`}), `%->_%%`_instrtype(`%`_resulttype([],), [], `%`_resulttype(t^n{t <- `t*`},))) -- Frame_ok: `%|-%:%`(s, f, C') - -- if (C'.RETURN_context = ?(`%`_resulttype(t^n{t <- `t*`},))) - -- Expr_ok2: `%;%|-%:%`(s, C', instr*{instr <- `instr*`}, `%`_resulttype(t^n{t <- `t*`},)) + -- Expr_ok2: `%;%|-%:%`(s, {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(`%`_resulttype(t^n{t <- `t*`},)), REFS [], RECS []} +++ C', instr*{instr <- `instr*`}, `%`_resulttype(t^n{t <- `t*`},)) -- Resulttype_ok: `%|-%:OK`({TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS [], RECS []}, `%`_resulttype(t^n{t <- `t*`},)) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:44.1-47.49 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:43.1-46.49 rule handler{s : store, C : context, n : n, `catch*` : catch*, `instr*` : instr*, `t*` : valtype*, `x*` : idx*}: `%;%|-%:%`(s, C, `HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, instr*{instr <- `instr*`}), `%->_%%`_instrtype(`%`_resulttype([],), [], `%`_resulttype(t*{t <- `t*`},))) -- (Catch_ok: `%|-%:OK`(C, catch))*{catch <- `catch*`} -- Instrs_ok2: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype([],), x*{x <- `x*`}, `%`_resulttype(t*{t <- `t*`},))) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:49.1-51.42 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:48.1-50.42 rule trap{s : store, C : context, `t_1*` : valtype*, `t_2*` : valtype*}: `%;%|-%:%`(s, C, TRAP_instr, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), [], `%`_resulttype(t_2*{t_2 <- `t_2*`},))) -- Instrtype_ok: `%|-%:OK`(C, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), [], `%`_resulttype(t_2*{t_2 <- `t_2*`},))) ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:5.1-6.36 relation Instrs_ok2: `%;%|-%:%`(store, context, instr*, instrtype) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:54.1-55.27 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:53.1-54.27 rule empty{s : store, C : context}: `%;%|-%:%`(s, C, [], `%->_%%`_instrtype(`%`_resulttype([],), [], `%`_resulttype([],))) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:57.1-61.86 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:56.1-60.86 rule seq{s : store, C : context, instr_1 : instr, `instr_2*` : instr*, `t_1*` : valtype*, `x_1*` : idx*, `x_2*` : idx*, `t_3*` : valtype*, `t_2*` : valtype*, `init*` : init*, `t*` : valtype*}: `%;%|-%:%`(s, C, [instr_1] ++ instr_2*{instr_2 <- `instr_2*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x_1*{x_1 <- `x_1*`} ++ x_2*{x_2 <- `x_2*`}, `%`_resulttype(t_3*{t_3 <- `t_3*`},))) -- Instr_ok2: `%;%|-%:%`(s, C, instr_1, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x_1*{x_1 <- `x_1*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},))) @@ -31865,14 +31862,14 @@ relation Instrs_ok2: `%;%|-%:%`(store, context, instr*, instrtype) -- (if (C.LOCALS_context[x_1!`%`_idx.0] = `%%`_localtype(init, t)))*{init <- `init*`, t <- `t*`, x_1 <- `x_1*`} -- Instrs_ok2: `%;%|-%:%`(s, $with_locals(C, x_1*{x_1 <- `x_1*`}, `%%`_localtype(SET_init, t)*{t <- `t*`}), instr_2*{instr_2 <- `instr_2*`}, `%->_%%`_instrtype(`%`_resulttype(t_2*{t_2 <- `t_2*`},), x_2*{x_2 <- `x_2*`}, `%`_resulttype(t_3*{t_3 <- `t_3*`},))) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:63.1-67.33 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:62.1-66.33 rule sub{s : store, C : context, `instr*` : instr*, it' : instrtype, it : instrtype}: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, it') -- Instrs_ok2: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, it) -- Instrtype_sub: `%|-%<:%`(C, it, it') -- Instrtype_ok: `%|-%:OK`(C, it') - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:70.1-73.33 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:69.1-72.33 rule frame{s : store, C : context, `instr*` : instr*, `t*` : valtype*, `t_1*` : valtype*, `x*` : idx*, `t_2*` : valtype*}: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t*{t <- `t*`} ++ t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t*{t <- `t*`} ++ t_2*{t_2 <- `t_2*`},))) -- Instrs_ok2: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},))) @@ -31880,7 +31877,7 @@ relation Instrs_ok2: `%;%|-%:%`(store, context, instr*, instrtype) ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:7.1-8.36 relation Expr_ok2: `%;%|-%:%`(store, context, expr, resulttype) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:76.1-78.44 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:75.1-77.44 rule _{s : store, C : context, `instr*` : instr*, `t*` : valtype*}: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%`_resulttype(t*{t <- `t*`},)) -- Instrs_ok2: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype([],), [], `%`_resulttype(t*{t <- `t*`},))) @@ -31959,15 +31956,15 @@ relation Exninst_ok: `%|-%:OK`(store, exninst) ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec rec { -;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:226.1-227.50 +;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:225.1-226.50 relation ImmutReachable: `%>>_%%`(fieldval, store, fieldval) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:240.1-243.35 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:239.1-242.35 rule trans{fv_1 : fieldval, s : store, fv_2 : fieldval, fv' : fieldval}: `%>>_%%`(fv_1, s, fv_2) -- ImmutReachable: `%>>_%%`(fv_1, s, fv') -- ImmutReachable: `%>>_%%`(fv', s, fv_2) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:245.1-248.20 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:244.1-247.20 rule `ref.struct`{a : addr, s : store, i : nat, `ft*` : fieldtype*, zt : storagetype}: `%>>_%%`(`REF.STRUCT_ADDR`_fieldval(a), s, s.STRUCTS_store[a].FIELDS_structinst[i]) -- if (i < |s.STRUCTS_store[a].FIELDS_structinst|) @@ -31976,20 +31973,20 @@ relation ImmutReachable: `%>>_%%`(fieldval, store, fieldval) -- if (i < |ft*{ft <- `ft*`}|) -- if (ft*{ft <- `ft*`}[i] = `%%`_fieldtype(?(), zt)) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:250.1-252.42 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:249.1-251.42 rule `ref.array`{a : addr, s : store, i : nat, zt : storagetype}: `%>>_%%`(`REF.ARRAY_ADDR`_fieldval(a), s, s.ARRAYS_store[a].FIELDS_arrayinst[i]) -- if (i < |s.ARRAYS_store[a].FIELDS_arrayinst|) -- if (a < |s.ARRAYS_store|) -- Expand: `%~~%`(s.ARRAYS_store[a].TYPE_arrayinst, ARRAY_comptype(`%%`_fieldtype(?(), zt))) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:254.1-255.44 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:253.1-254.44 rule `ref.exn`{a : addr, s : store, i : nat}: `%>>_%%`(`REF.EXN_ADDR`_fieldval(a), s, (s.EXNS_store[a].FIELDS_exninst[i] : val <: fieldval)) -- if (i < |s.EXNS_store[a].FIELDS_exninst|) -- if (a < |s.EXNS_store|) - ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:257.1-258.28 + ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:256.1-257.28 rule `ref.extern`{ref : ref, s : store}: `%>>_%%`(`REF.EXTERN`_fieldval(ref), s, (ref : ref <: fieldval)) } diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index 5f28a90733..c5f9f478ef 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md @@ -18076,8 +18076,6 @@ The frame :math:`\{ \mathsf{locals}~{({{\mathit{val}}^?})^\ast},\;\allowbreak \m * The frame :math:`f` is :ref:`valid ` with the context :math:`{C'}`. - * The result type :math:`{C'}{.}\mathsf{return}` is of the form :math:`{{\mathit{valtype}'}^{n}}`. - * :math:`{{\mathit{instr}''}^\ast}` is valid with :math:`{{\mathit{valtype}'}^{n}}`. * Under the context :math:`\{ \mathsf{return}~\epsilon \}`, the result type :math:`{{\mathit{valtype}'}^{n}}` is :ref:`valid `. @@ -18162,8 +18160,6 @@ The frame :math:`\{ \mathsf{locals}~{({{\mathit{val}}^?})^\ast},\;\allowbreak \m * The frame :math:`f` is :ref:`valid ` with the context :math:`{C'}`. - * The result type :math:`{C'}{.}\mathsf{return}` is of the form :math:`{t^{n}}`. - * :math:`{{\mathit{instr}}^\ast}` is valid with :math:`{t^{n}}`. * Under the context :math:`\{ \mathsf{return}~\epsilon \}`, the result type :math:`{t^{n}}` is :ref:`valid `. @@ -30011,7 +30007,6 @@ Instr_ok2 - valtype* is []. - localidx* is []. - the frame f is valid with the context C'. - - the result type C'.RETURN is ?(valtype'^n). - instr''* is valid with valtype'^n. - Under the context { RETURN: ?() }, the result type valtype'^n is valid. - Or: @@ -30055,7 +30050,6 @@ Instr_ok2/label Instr_ok2/frame - (FRAME_ n { f } instr*) is valid with [] -> t^n if: - the frame f is valid with the context C'. - - the result type C'.RETURN is ?(t^n). - instr* is valid with t^n. - Under the context { RETURN: ?() }, the result type t^n is valid. From c37b5aaa9ae4ae569df9a73f04cee9fb03b11b70 Mon Sep 17 00:00:00 2001 From: Zilin Chen Date: Fri, 14 Aug 2026 17:27:59 +0800 Subject: [PATCH 2/2] discard nano wasm changes --- spectec/doc/example/output/NanoWasm.html | 4 ++-- spectec/doc/example/output/NanoWasm.pdf | Bin 243776 -> 245110 bytes 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/spectec/doc/example/output/NanoWasm.html b/spectec/doc/example/output/NanoWasm.html index 63786e0d49..f7edd685ea 100644 --- a/spectec/doc/example/output/NanoWasm.html +++ b/spectec/doc/example/output/NanoWasm.html @@ -7,7 +7,7 @@ NanoWasm — NanoWasm documentation - + @@ -378,7 +378,7 @@

Binary FormatSphinx 8.1.3 + Powered by Sphinx 8.2.3 & Alabaster 1.0.0 | diff --git a/spectec/doc/example/output/NanoWasm.pdf b/spectec/doc/example/output/NanoWasm.pdf index a9f146cc4f2767a50032cef30dd5aa3b2c73549d..525ff3f867e6321e90bb2a0323854a0cdaeac592 100644 GIT binary patch delta 18384 zcmYJaV{j(W(zYAhwr$(CZEIrti9NB6C$?=*oJ?%n*5uoJzjf;TSkJJP76J$5Nf~6qXeNZGfB@s+Xck9S z`A_6Z$;J@^SkAKk8Wur--1`n3#lM9zrhK1mS`|~9P@&;H+p}V6OToDSk_LZ$^WCdd zPzwr>zySU=J@*uxJ!QzLTI{+guP9<$NGcXln+4KH5n{T}j5$0?dC2VeR~4 zW4;uKgs3lNTO=a8Ag50qWyh2uwEMhai*Mu26E;*5Y3qzDzyLkb)uRmu#6 za!Lw1CO9_>TM8*X9UxoYX+s2M{PrJ)Ukh^n)#rk~x+su9tyQPDkbs~NW>N%RgL1d; zaIGg72Aou&s<**Jiv938;eMJ}eUUnK3$n$)DP^yW7Qz%Q>~AiGaCGY1j&m^~v=y#w z7mzS8TI21R)K-8(wPr}`DRT=NgQqpDxN$_=mNTnxNgKL<7hnog8UP9mOs$uI=5xsuuPb$5$ z2E#%8SU=Z872s{OIoVsQly$Flcl33R)bxCV~YcRNlSK1?^iutx79~ zh51#9{hDm^P--lv`bki1>3Mm3Zt%hsRq<}l@|MNbA3%=v-Xh8(QXC7Vm~U{R5UtqK zHOz5yloe4?N+J-M8rDzk+s=ZumEyViekljT1y*mJFJ?MEJjyol@9sJicEPh)%gA^> zLP6#DsqcLyoE%ntuVoHhJdI}Vm;f5bmB+uoF+3;W5(F+3sN*Hx@txZQ9*)>XBlj#d zCU<1Bnt+|=X_qmt-T{$(bN_liRg&!{&TJ=#I0&7KAGJ4{uB$ivL}4ky)B0~mhlVZ?hs~w#!uFIN#<6WnMUoH| zE#z^Rq=soSe{GBLq_XcA+lt$#GL~m+KmA=8J$Hu(4VQ0%09>&z=q&HCM+`R+NIL<% zw9Ap5CgA0U!-;(AA~}R}HB}a)5)$ zB?ZlkVLWfHid3lZc|2^Ne|`DQfzhGdN!$>2`u)W-BZ{Phctw(uA+m$yitmW$=m10F zFb$T-_9)jbgPe&-hx{YOaXr-&h`w>Ou2aD0>F(F$c9bH+%p?+$=Z-MGCbpA2tSYj9 z>W5-5j%sjH3&28C=mEpiUlf`~B(9cngMb z-U!Aoj=8Wn48nipj&HSna7#K;?e1R&5{0N8GkCB_P!-Eh2XT(Hel{}N6@&u^e1`t_ zQkgiOperfJxM2|4|0D_jm#V_W1ZU-DO&J8I0gUP>x@~fy^j>Nga=VsE+#`yy=f$VE z2)oK`WJY=}64)d+t;+!ER6QSVyGcl*fu{OZ>?yG_s#5`|VyNG`T+at!I-4rC7t8 z0FY>UW?)!)D&FdaH4?|0pOuOU6&D`Jg8YcfK4Yw-4X-jEL3Ggp=ykB1y z^=6rxW#c5wN8f&;T|g$(gVSV^)CkxQQJ9SkN7?@D7>^i8)i?8)^8KzeBQ5FQv2vj+ zi4_jGvJm0kPkpXKt87#f+`VdZZIeT?2LzYN@{TNT9<6R>CRc2ZC`kD%fEH3LyvQ#d z7l4bP(1POpxOO|AY-f11dbGFppZx2Jf{flcZffqJ z%q7K#8VDjT{RBCAB<^MBY6*6SYi;L!!v&=pkPyj2r)$KR&e}PaFGQ2a(*(5<1q{>* zKzF@h5zyLmDEq-rBflR`4h(7n4=Et>9{>}Mhn0E&N@E&0m)vfXOy!LUy&hl-l8#5-SvXkL42`+InSSNC8@wdSV7y1>DQl&{Cszz%P+ypeE-Y{&h^9BR;c?;Xm34>$D$F{c!gxN5_bSyc|uL z4jLGyg+%Q-)<;`L`vwr4MP?*0x+POCbUB!4nL@*XbX0a-5pt&zNC|Kzz(;qAV1u;4 zT_v;-8_GDzsfe_#m+FGRTJ(sC(zEyAN@A@djo~M$Z_^3aHQxZ4ODtVcTh{Sm42PcI z@yX@;hSpTo+3b^N1RVnXf#$wSvdEtXtw<_{_*y=rza;eIi^@5^BchuN-i~r6wUi9M zWBhUVL=deE1ja>g5gn_T03AH0W0#;rDm1x!%g3iEsIU?`7ts|?A{O{mU^!AubEISl zRC@5|36ri<*P*u+%c0lo(a(PnF6aYC?c`E6E30rm$Sor>`)30R{^?c{i+9SbC z)!+sUi{JCm7hGb+v`RCibxo}~F7OL2+l+Bdx8RPJaGy4hD(6yx0Nks+7pfe)<+(Bb z&qnA8d_PRp?m8|X^{&WR#co%xyhA#&aSrCIqi+nj$f2PniSWO!1gKYA)1+4(*8(3l z8)L)kZn6mgr%;FQdZw}3XShSWw%^W)_#WE2wbf-;*23B>FO0ml#ajW8SqztbGT%$x z{{~vNG;=rn*AM+GnvLTF359)93gQc})x*Fl5h8e>>{`sl zQ}-l!&2y1et#4hA)~i`8?<}@p)Adm;$Z zlB&(%0Bzuu_B6XSjvT%kzio36S5hm-b2Z}|9UyytY5DaTe6#A-q2J4jg*RTikhV=G zYvCGIJ)z$qdea+X8V@j)s$aTpz@9eY;S>>qIqDw<%8XUcFaOIREn>Y1-$miYD){KNt6!78mD(bg&q&Ei<)q#C{81&g7}>Bc7a2&rNU`LJM0wRC*1u&; zn+`+ph~fV*V>i=OU5qQo&PalB0~NBl^OZXqqPu(&dj?;m(m z0rCqf#jpk0>WE&Dn!c+rbmw`fLMux&g&XM)5zhN|_q&GKdnRqaJ_SYbpyT)c@E^x& zNOZg`N>y@%rrRl}Bk~0I>Pj^<{W@Y=3k9y`qpML~t5^Jb+3Rhx_6(p2pn$nPkR`M! z0x=y8y)R!U;EHa7`pN_Z3&1G(l+oyK0M3mb=9z3An0@Hc3W{hc?ha8 z9NiP=$tvi_PU1uVCVa7PDUVuEY7R8|ne z6uTzi@PHe<+)TDIO8Qf|Z#yc-0~93v9s)u}z}f=~fM?)cX7?y+g~6AEjPtKmkfTXk z5#&CdN>e3`Q2yL`jhwQE{=%kh3{px**DKT=HbnH7u{3Z+CGg-j00$PO#MCt2 z*yN3B71ztVhyFAQO+X4>gLVAdv;!e=wA$=&;&S(Jkf!!G#C>J;_Jol&s;h@=7gZy_ zx*~4bY%4XnDT4hUYU$XEcn=S)-LcuJjAny{)rY1xHb@Wfimz+DlXzHi+F;NOpyT3> z58iPf$402f2}e}(6jAAfyqv*bR^9GekaCGc9eMeHwhKY*dDY$L0t7n!GZA=z_4uQc z=$avD1hhSF*U$FCKHSL5@~VH->`g}G zZA2xGOVe&1&f*^CRyLrm3&-e>H&T|OE{`G;AyG7QrOd@*@)k)jbETba+I?tjT7Npc zs3)-GGGu;i^c3>@vGrvAAz3g`;C@^NjDPt*I6ir@eF&&sX~SuLu$qLTV^1xtcVcAt z|KueG4aPEuFRS5Hi|`-J!QTfyeadLLaB8a%q(dln1SF?+95Z`5{#&prMkpjTEH@)0 z>0-k~)EIfclT=bNYzgr!Of{tr{~5K5RrF*vw9hcr$6ZGYQ_1P8Vjy#Z5xv*|mdf#xkQ7XUv#Q&RD_NzZ&LZrF`#kbTG6ulInMU; zV(pJBtm*q=+ufoVI*o5>l5JE1B=TVq^^|Vxm1BTmwKzViGi4Pxh-Mr2USMu^IyR=c zqA2Vk`;T^Q=uHO3nqZU_mF@4`ag|v}ra{Da&_WK3M2Z?BG z?&HclwrQ?62s|mA!GjWQ`T}}kO1&MLjGSS7_jJ+K=j7tdvv~n2)?yA3RJ7 zArVEpt@1I|Y2&+IB;#Xs$lK)E;xH$vD*DlF9Bn6rDD`$7skZeg9eGX!*hgwm&#AN0 zz(<9eg=`YX)l6%mPb)0}FY`n-h^;2h33NDh*wuhVGf-V#AFmF*j-3*$sMnAYImU|N zWijrdj^BtX@}hqF7kt}lSPE0ja|X06ZbEkFAZw0?{G%awW~OD-x5(*m23fUD-e0Ub zFH*_f>jfnNTi5*w3M9HPC&X|CezFig2RAFRgHC8*GB-&Ioqu z8zqhiLj<&Dh!j-g^MIZfzybNxE1kxidPnqZ{;B{ER{wVp%*Ku5`4FRH-~!r*394#2 z0YG(O9YFkC(%%dC@ZqKAmH0p)NX;BxMs^K(Lqw7@`a2i*3dp879XMG^iAR2G1fvfQBS%NnJY zAMki^BJ7kNa(*OUIA#S)M{9Q*5>{?buK&@ZS9jOxKdo5ctMTCYOE{TN4>>FZNxa{L39BCre;xB z&a(bRpq42FRQ08x{~WAixCEUe#J_#1)|e*=aRfEB6foNRDoMjLO?ZED(N+=?3cfU0 zsmv#&!EHD&WRi{`991&N{i8uMS6&Z>7w4llp@G%fo3z>ApH= z`wGY@FFV-SdGX`EZ$**1pT>;7j~|1!;$9oV8>dXq&P9=rFFQ@W-1XKMRejk?>DZ51 zh@1A=t;&JB&qr7~r?v0j3F@!+*+aI!mY>px3}ei+7mik5^jEJI2Mq}U8MX0~RO?#E zyLv(V&wtFHjjqeNJ)Q$MHU2%H7e1z>-b(Z#9WyHZRL1{P1Q-i5#hg#7Dnv@MB4UoV zFvh&b4|KzxSglg{i}2hCMib!W_|2svA^y$JT2bvD<-Xn6%WYL>*x2e@;dKoD`}6IU zQ^cQ=R|w;Bl2SQ_J*A!pxH+@Y2>5p&U{{r3y<1jt@$KK1JDaXelcV9R5s+;(Q;(f; zp0+~&oVQzkifw&+!hIs)QIy$0S~MNAbK=Suk`IZIX<&D56~oW|^S-+K#+FS1`C#Q4 z;N#Pkj%VY$7z_|MGR{hbDsT^M}?*^7iJXZE0(5svMQdxTkPz7v-8gDJ_?}9h@ z+0_!>&eU=)98%Zs%v!n82rS5{bkewR-q|HCCu$AH)Ts&UWdv0(aGTpm*^RBmZN)9d zRpPp_bA9-i%+)__n-@ayRmIo$GhJTpGFkn^S9v{-zPqdHUno@@R~c8oQup<#I8qg| z`&z5_Zj$dP@vQf`G9h8#4F_{?o|4=uK-^T4xrb>6hOHGx z3=<8Q5WlaEbB=9P64So>VrNfH_REd1>2V9NvusblOC=Yt`xP#=Q^sK5g+!+Wm~ z)*#*!yQuDhsU`xEb`t&KLOp1+4OR!0kAu1#f#BOR%vVwuT}ed8QpBa^!})>0Kw(Ez z^8|#}jBak@{qDZiRGI6~8b4{r&78VT_J#UUiC41~Y&|M&AFCRDRaT@7LbLNXiZbv3 zv`4_y7^auQ9`(9&w_1@O?XwstH$2i71CMj_-hjXnn3!xE&-EBV7u)u4x^(naL-VWa z7^oWio+T$LI0eS`UdMp-DVf*sZaPasGE!o0T`?A%90vsterI!(*9>q4EG z3reY5%%>sCh~q-Ma8cWfPEsPy*rx^bl}^B$8NC}vqW+Yw>c*S-nB5oB`57PGU-GhE zd&qKW$^4aSNAnu%HJx%Pc*jb1U&OWAu>SvRlLwgoJIndc(CR9XGcCqXoDyHZKq z2lAwdXLrcD$t-E)xsSaBCs|0>Qt*)-^ZfL|qxlDgFiy7S9qpk~GGoPl_XUU!El7ry zXp>(V2`9kx97IXPNXeOvR7O!vEllFZm)*VRz>u3;Je4NvNg1F>q=lVIKAoN=EHED~ z%=NQj;aX4t(iYwX4&+D>&|=VaCQI%)_@a#|Dx-{r0o+1?1-ZX>HRNHWG8whBpp)Ob;G!;>xnE;F=;h63B}&y``vNoe|SGHpZeCMH-vPS zYP# z%S$@|yfZ|+H5Kqj2yg2nR08R$56Ll7>(Ve-iPkV^k_MFLF3WrvG-dACb$`uNQ2tpx+?LNmWUgq_kwwab{f`h=~xZE+aYO zxn|Q~R`)UMf}OF2`Xo0H>USg}%(ayDO_Bou?3dgyhxZ}=%3F96mqSe_Z8$C29hpJL z<5hWh2nf*7y_~gEE8A4M&?vILaLKItOH9x@aUPimMV3o~)yTL3t70*Qo9N6QL{>4> z;UVe=pX1;5xKELk|9ZR3lf;u3?|D&eykNU$D3wFo?r(yoHn{MYNIPiM)LtwA z?Zdm`5JUarAtVHPq-0P&r4?+xiP<_?*C<`Mv71ph4?-`3E69?-xUW<@1?mf7ZE`JEU>ryfZ7##@4R0dISFVNeeBE z?T4~yC#G_h-JFC?!_B%qnmvBSq%f|D^Z?eladn11Y%^2LQI;1H zUSv)Azm4EEB%p*rAqU%3n(KW?6=XQ5a)OqXL2Jsf0{%&PwRr*3h6 z$=AOFE^nS>6gX!)M2qOUkuFP0bREUN?uyR*3|g6ZL#X2i97?4ld?G-BZ9naTqYDZA zm8ecz#~F$mbyt_QO}&uABd8Xc-7g-qWQkvI<13N3#tw!=W;`I0WtGVY zsK)n%Tq-+I^TFtgL#=-R%%LBVN|2CfPo)_4>NoMpBu=*OV7;vI#wV=_T0ZZvR&W@F zR10{fcI86g3@iDR;t#MAx;Yd15M}0>`_B0K!r?m52`w2_QC-v(Ree%}94Tym;w1PZ zXQ5Ws|=^MaIGL>hxj@{`b zTmMsiUS!G%MKJHnZg4aT3PgmIb3lM1zQ7>=FR_w7%}v}k!S!JniszT_#8WXFZA|Lz z8Ogpa+gB6pVN|OTYTxb*V)Pv&#ED@Wkdkis+FM3E2nE$tslmnO(H$qnnQZ zN(Hbms1L9E1hNw=CL2&v_^`j7yWd@Ko<>7fXUZutqtBo@AUY4HEX5u%d^=>SX2n}Q z3Pvv1%n}d_*d$*vHy%a@hM4*co7XIu!pAyON zJ^#2!2Wn;eQq{Pl6EQNi-h8tCalV8|S`9~<6Wp)Z!NQKB)4ik5|41Pozt1R6>QceV z0(#xGjeD&OUvVHS8DrA8}BZ4HR1ywK@mVoNOarXi_XRLXSO0q*a}Em}4)s6rcAW6HTqkrh3>!e2iF3iaib=ZS*Epa%dW| za~5Tg6b{yHsw$3bMle&gWu>iHk*8@QbVy>>=qp%^%Iw`nZO#+eO$T{^%OaYN$hnkmD^cpT^w zOY|98#sU6vR*2LSzgeiR4gN^m0o^qTtBbNQrE$d|j(ZDM9WEL| zV|-|N9deg6=3>1DFi2-dk&D03EW@A_p$aVhAVZUMbID4butU)0H3h-$6r z1*d}z1k8pZmcAKtSUYb9NBdTTls4#BQ1;!GMwK6BZKZg1F22hnr#`@M8c6fB4DG{* zu8_2bf@rO35KA%Oc!wFip(V{Ar@WuFc@Kg!j}krs&24o!P~Rm z?=Kru;`FH!$@IeB;)fv$)(QvJ<^8RoOBn~Pyke}eapWZRcNF=~3OFUT$yU(!EgggwhOx%aa4?*MWsS|P z9p*V#!L=Sy(L;m)--G$tTuB&JkGaWHcGVa}^l%d0RzD?-aD~`qbVEo1elXczS z^e`udHruomW{h3-E>xbtc=E_ji}N&Pjd5-JCN>{(bB=C>vTlX+>O`^QD$EtRi8C_`?w?)~=E_`G4;?;F2^d zVUggHf)^ry&g|K_!(m{H7;!|w*>_p=mwBdSyw77aml z*AOXuyO;dx-bvYZP;sP6;Q6jxc%cR}UonxCv_U107+S4>RB%PPjN}kDCs0IX_fqipnICxw z=?nMIffqE{AN+a7%rAezEeaaV3Q&7^nlZdbmvnXb{e4$OR zxi(;KeEDe!>8{XL>$s+=loeR~Qu3P%)$w|RPqI$7;cz%j5LAsZ$yp-nQ7 zEE!$MY3INj{?q2N8n`k%|W_M3p?+a)BU?&ojEIM z7KNndlyGx_nOy`X%bER-ZovxU7rs9C!WP6V=(&N#{Mos5Gk2q?2k@Nh;vu^}wY2Q@ zq4=9u)SD1;8Q<>#=3oWtZ3M1m@t98^Ev+8689HCu_lInH@R+cMmp69tl$k0MW&as; zaXNF#N6^2?9`XasIXiU~S5hbl%bG0@ZW+t}`7RvN5m8O;vb7995AF8qGRD5IQ0RlB zELlhJ6k3eGA|wt_2AmY&F{1wfGJ(7!`*v!BEV!Te%>)yGSL^a)55K)wQ{SsB_O_AS zCJA2nKx>JOEpTnG^AY4@%VbDOtcudW`TKjf5rQz}3}60;zH$z3;8ZAvi-tY)cUl4s zbOU*Eml;)|B0gZ@p4BW-cc`@r2fp2)n1XIr&w6q9!Z!ECbbHAcR{I)htZ+Bwm9flKZc+ zFOpCOgcZoEXZezUBBHvb*&)f8D!JMsjcgV05E=yl@LhqaX5E1-Ur?62?UFa6zZcHI z(`KSvR=XUK@qGIn^S`Sus1mu!L;mEYkyVBrxOP{tmWtF-z)dySl(#MzVF%R&fPlFw z7z*VQ-+_e&Xktenx<#qYUQSpHl(8&Nz+xz8{t}}SmI>j|$^2V4G?0Ez;ult!V}We1 zTdL9v02=H|(3Snf{&iirg#UF=fA5Um{l*q19;s5M0mUS>(iQc;5W7e$2~rHhfVocM4yFfBnv6vryu4a=l!zET9U ztOi+PJCL5{)(FKU-U+PWlFY2=#y{Q$LW9B(uumBaBOxlo-U&M95o_Qlo27@egvT7V z0Q#01)&JB=I!2nhV$dWmQv*+n)XheMV99eW6R}kHe<7U>0iQkHgXa%7&elnQF7gQK z?zTb|;S2>X&i3>b9b2-bqW~9w*dZJK z;Nhoo`AxlvORIcTc(;sHWN=$9a1=4bbV#?Qk$Zr_x)L#I$*H?LyEL2YYV+FrEA}2P z*wJF6`0k2_PmF(li6s~&6MCImT%9g;UT9hbpsTGcn24E>o4=0Q&s~)J>Q7R&ldvA=Ice26EhfV>ST^3@D}D*Uo}*u>I%8q zs{D?=R1+`tzT09Lo>eSbUE`3H(!&u}Uf25$dv5NWpERSAMl3MBJl7-@-?zosa_5@C zKI+OfzwAF32l`F!oM0UR(xtDs+`63cSetQT{iHrR4xcm5T!9I;NP0#Kbl1gN1GNu9 zJ=Mc0cGMe$-u>fENXdmPN=^NpUR zsIYgm#e(016zLO$e}Tmz3>;cmd(RN`_M*&-Sr;GTeXSHB%_}Yg>(n!^c&GRs7Yfw6I0<@lu z3Ba>oR8R!h$pEPAf{J67=>rVCi9ufzBF^*_8lcy&g>kwC^=W{XFh^BzK@|vrzOcBX zA)*mtsSWI|q}VrUd^j%)YFYR~S5M2s93G;G>|?t9Ht>L60f6Qtt(~S6*-P?suuwk(L80K+lnD59ERxq! zCLw)P?8mUk#Jm|WM$Ji%yY}ZGi$AyySnR)HPxG1>QKVn%Mv#Zm$3en z+?tsJ8CvM#MkDDJFv3y8mnE*?F7MAZ_kWL+(}pZSLlKK&Q(>sm#&wbL>FNO7!%65E zm@@?m(Hqj~fvKqA9YD!YQG`7gkgUah5vXY`4p4Y`Mpkl^a*pLtDd||$tu>e-lqeSg z z1`y-`U+W_=OpuM!5dM-aMc~1r>5KClC$WeHj!R{}ZXpwn3jQ!mDw08L>aY>g99r&t z2+C?x%wj{VbI3=Y(Aaw>4@BNC8*(y)a$N!ycu!#w3@TGR`PBlc6AcjC0LMub7))A| zY{3%1*OVZ(8A;R*qPH{=6s=`D!j2F~Ol1*APv%PrxGzKK~(*InaP+|( zRf&|SmPSQ=0)IRPUzw#-ZlRAC+&wjCgy2Ui-_-Kct&i`mC%K`IyDwZ-{Ub=gT^a2; zL7H_|5yGf*Dubh-+#^Sog)xtPRD}wR6k;E2?-O{f;>%J%tpNX;-(LHX?_P1@!bBy$ zcxa&`$flx$LkV*i!Oe$$D9Hm+ID%CPB)oY*%uG;&=f6naI*`eg8?zsEz716a-`*-g zZXoudiRySei4*$mf#7^yJRn&1UcN>~hkU`N80@59iC1gLXz zj*iZyC~uXxj{qOeqaV>H6*AmMEls+Lyf3%DoO0-0efya#{@{UsxSP+9eIUQFk8{eY zC4E%Cbuf&(r~=q~>X81JHyA2nxq;bbD@Eie-&$uZ=N9Ef8fj{m>@Pe?50f(RsELn{tsZsPi8OvOzqu*(XcFHSXw1F|T$JD)&6$E0MNO5-(D86Gj^I zrlW$ll>nuQ|F%4La#Lh7_~%J`?RxY0BNJWq97~%~y_vr}`RJhnq1kX7Yd4jsp9Z?G zFW6Uxur^0IRovDr1u?)E9Wz2rmVfo;&7K9vY`#kF^C$9m1jisBr_ZZHLgscEOh9qUct`e zanA}VR>)tZz%8W$bRG*F8o(QfmPxQGZz-zW39`vrk^16NGzc=maATxY#QY*y;DeVs z2=_)931%P-B&UJqIK^2=iwa~25h3tTB0f7T2QGyl-FGy;swsY9zxD+iB0t@4hM;S2 zSpYLWWX0o9(vl!Xpv}J{q!2_iA{qXMST}@&)9OHAc|*cc z+ZcccHnPoHQm~Au8y7O+?ETc&VsnHa3SihF^2*sgq9T@F&U)ibj<*gJMJb)!LH-G6 zRW)-U_*kF=lSWeb>*=5BnkS@Gf8<0{BLE=56%A z+k4730M}wJCiS`t-rCI>aAc~yW$Xm*7Y65uaw&iEP!L{@1{pEq80n*OCn^m6hMdGZ zv)z#*wxxDN%*8a2;pqYvvdJaG!+WaB3*?B<G^P?Nvj*tUA*ttuTYo#c`e|s;|xJjU%PQbr7aOR!yJBU=8;r4WVHz9qf0W#X8 zvN;@fC;1r-0rr8(x7z`WSsR3pA%HLLR%C@mx~BEsaZo7H6JC{yR=OWVcoAH7N zF?6=5sQ=2wOt;l4>n2_2(C6NisMxzsMw2|+EhhsV(tC61um`Oi2j|#cR#@B4)#wd? znw3zh9{PR=64l_`(Z@V95CFRTT*^TjUZ1j(Do9z96!bABGJdf7lre9|-Y!oA_$0H- zX9u-%jH>M&F4HEAmfb0hf!O7hiI1#j?-q0QR)Z3*@M|?{xS1?PX(MLbuzc6DJ%Z_f z1YoEA5|jkiGJ$j{zANpb<#9A`hEy0-y0lv>7^I^J2XTiYtk$;B76AL%7h0Z9|GLi} z;U%0wNV<00(XYxjSz_DPNS^J|+STce7Hy>zsS2UungOL0i#7;$gG&nNM-5^MKEh;9 z8EA^gP(u~wQTx&`RDu4TU^KZT294W9n$F)zZt7eII0>%3Cwh~Xa^x25ZTf!Nm)(R@ zr}H*V22Cp0yje!xf&fbW*yWv)ob_4OSr?M*#4lu#fnCG}?2zsdkeQ+>pG~7U?U+MG z!}zE24Zn*e$;UH%Lf?44+B%(#mKp09lGPn{!r%Ji8AwS!Wy<2a-OK)*0*gd5)=c=% z=XPTOg6-tSQP&?ccq8Ni2gQHT7L<*_T}yFjA@QX9#GZ-GMgaWrwuY-~Pm1-GmFMzC z^rYR&oVBM*keXRfY(c>ZJ@bp|&?Y5mgu<3xQR| zgB8CWlkr)&ez7=IRPZmiJ35F0(zhrkj#bR~E4y=lv$sSeYVNr<1zKgj7qrP8a-3e5 z4U&E{UIsT^>*AUMOEMx&gD<)REsdYT<9552IbGkAMYWw2WR!C(UAU)xy9#k{CzDd|~v7G1Olg)mPps{HKZ} zDrwR;rOk4elkRl*q@Gkk@uU-W>8$kEuG`g#?YqoN3UR{4FQUw;w*`Z+PQ4bjHZ zU@dR)Hb5N$I&ekqb~w3iMW;`RPr)Mg#I8xyQ*^ZpSoXnA>~#9~Tje$9^qK%{=So*w zQIU>xys(-xnfsdVH+aRCtn8P`M&pXjbFPDSwQtRW!8G)uQAu8FRsH)}d85`d@FKe| zPy5w8&o%qL?nJSAa;))D*|1!$%T-tRab7Z~7;qW;oHAn`nDOzR+6b^!OyY;G+@#+Z>m!b7aL+ z0>~Kqp-GrpJ$B~G`RBr(7f7tVi*@`TBWq9Y&JNPlg`*IjGIi6JmeE|*esOl%p`8%3 z)0C`__Ks%r!c$dlM(o4ugY^3@fQnX0YE9oZt3PYEEbTF)Adr_&K~ELGg$%!z=2b?| z#j`}qZavW5a`AJ*{p0HDa6vwOvL3rK2@n|dPCdiZ|Vv8Ha?veWCZ%R3@q z=~LIoFn-FGH&5ee=t&Sw`NSyOm%FbZ36h&e-T}J5hT+I!j?#TAWA_5q zfL(6wgshwl#0QyXtx@Nr&_D(l1Jv3>fk#(aafYz3A+uK*Liy%HSrTW2>12j{y>XH z;p(dG8oCa*z;;qH&J7H6#?G1I+B|6WsR5%D$o#@%`Q*||ur^5lUQgP%3AZaR2owZ7 zCztM|15-EEs?k_(wW_-q0b*`ow{or6$$~#~llQQgIoR0vQ#dk`)G$DIY(uKlRKlXO zHcUC%RsgD-4p9*VKu?HXxr#k{{{O zeQa#OZoiYepX!WbHFO$2L8^TJ!|IUQ$>cAnp+v>R;*qjAI**%Z$5C|I##0ruljz!& zl{5RwDn`2v_+JIW0KmujX@($YZ*|@6`0zTE;=atA1mp_Fcguv8@}9%NX=`Ru)4?XAGvHI>?C>MPNaUAQG6wcWu1VC^cSv7K^Jp9Q{?$_?1r z7Qx>2J9m(T|CKz@JbChre>$z zeVn1WI`OX-5Do(eW}AXMO@A#yp42SgC-cl|FNLee=9wJ! zz@w5omL=i6XIwoOYjiGJnYx3bH+U+)J&k2+$I

sT22WZ$;37ANwuycFo-%kO*)= ziFVT}a0PHsj`q4*a0gHt4iXv-OC1sgTTe?8HWoHET9RMRrtUUwmZl`0macBLPL3p8 zOzcb?8RGTeqTuW-|F=3iqob;P^dHmjT>agl%d+7?BOyPUUUVqdf?6T8bTt`~t2{(f zx?u}`)lUCy+;xZ20fSwsT!2V?e_a3j$zx5*K&KVt;TB6B_Acl<6|m8)2V|6E352&> zFxa5RN+A#4mW4DK7*dZ?fPc#3713i|z-4xLnB_O$UK*DFuvvFme*OBjvr__jmVc^u z4c%e+@sBr`x3}NjG{2pG+cr1N_PN=8__SF)WOnIEvs-T4mu|B~=L_7n&xp6%U3dIc zZ_&#vKd=3S0}}t*K6Fnzw4`#e->;XOhj#slh;+!!=F7T8uwmQ+i+{yGP@PE@}Js=9lJBOJ6UCm#-l*E5x|e78-<AQLnD)YsnD%ReWdGy7+BSdCIU4VnTPnj+K3FPMw9?ZIR~G$B-wElJ zesaPCwYlaKar1r9qg=syF|q@Z9^!lmU?{n9nt z_qLU|-wO{CCWi>tW`+nFAxA-&uW!m1e9f@bF!3tR+{aDiS)4Xe$cT{47bXJ8QB_0$ zIa5njhz{s6BK9wB)9W0YbnRv1^uHyIH@tl|eNEsXD2W z$}n*pH&N&BeFW$EfEYnaSB^p3+G7w69f?H{O$9Rs(O5A#IR-ig!Fwd*j);jmtXPiJ z3EP)u3}SH##vm4_$}xz=mBqYdeJ~83l`P1SQh$!=(UEeZ4oUT_O_pd79CG@1c=r-( z{{`Si@T2gf^rPB$h>x4PC-*P={-6YRuG#++ywQY7t^OnfcYw`lNiyJ4qO2 z$2ET9ZXPrDF72saoSt4#T3XjuRquLJExpo-p&uX-BL;>{2oo{z4M@ZUKS3hK5>q)?VwZ=WH{xziw7x8MDOP3SX6`Gv;M`Ne(h#g>DZi0YzYyZZ~NQ$bvPx zI#Mwx0qbUi9NL#@+aE)#ksT^!i5k+)6xvT({bX(}Ex!eJ&=(2RAL^l`_ zWpsK(lk&FMO2;gT7Q{-UoKDkgGwd=d=~zLcA7UR}1D%#u4;tv2=(PGAXrybU)3)}5 zCb|NhcHRtH=nm28Cus!-K;A8Rksd{MC`IYR6y+avC`Z$vX_0s1@~0C~^`^m%Ca hmaz-(5?W>63beE;iTq{lX&DGy7= zOnTKk1~1g1Fyg9+q%jSaUB&($M`n)K!~}r~%$dZ3YLvu;iq_Nv8VUl!#nL1Op$H1hl{5#B-c$um z0tUjx)-(^V2$qzLiVnuk!aWn`IwZG?`s3(f@V43hTxP(W#XnvdOulplls)hv^ zM9Uam!v;1&rH?6raWdSvwRyn!Elb%K&n1!obIOZda}*jf(nq1`@+ zO$_Cqj&;)K{glHJZuGy{P#N?r7By*%Hv}oQ5RdRy36U~3t4SiNloz)^hmDj7%8QAC z+Yu%a2^JqELss^gR3c_&rnhFfLVTMa_hcxjZH=FDpWN(xKE3l-6B(Ei))?kdiEcXv zx>4;cV;qT8yy(8rdtC(B3=^m%|5m=Cr8?r(3z(!@{)XIB(ISiYJ@J{r>L@Q6+tF5S zzMC^oohqD!LF`}wVLn;4@@kWA^;G4sej+n*l!Oz_AWIIWhzD6M1M)4;<@aiSnjn5Q zq2v<4#M{;FbBpw!Kjt*B0DKVg(260X6wwchm&Nuk92$ICEig%m7^;9Sm_bD((XXFK zD!HcH+P4EcaFXIATTEp#N??`Z$G4u+`g-mm$8=;~qV|MuCz2X8%0?oH)?}s{*66^F zRlHz@ljt}48Yra==gNMT^PRif%V%JRYFrT* zGka4PS7$RLyZ?D|NXo|mPqM~D|8EKTV{!pzLtE6esYEKNQ@M+=X$jGwq3A@F`u@U` zDksb5_hu49xO{8=Dr|P2ABJL_V`Y(zT$6 zu28AU649kibl?jxGjj7M8@P{zobA?_ZygB6`O#Y*Z z=`%pHi#}AYBnzepeRez2_%nx6ymf)(#R$={lr%w`@Fv@L&)^B0lz@Snw1wpk+>oS< z9SoM|Ax84QQ#aV?po~l`NdusifF2Dwmo0Xro-2)f4#!f_2lz#noY*8M0cXjr^f32r zT+77948>wh-d3sPOCl$4rlV96`t*U@v`~xODR6E;7?1TrTFYB$2664Fv1Z?DLh$BM>Ph{3f%Prj^Odw>Ub)AB__eXT@kl(O zHX_V@5Tr0FC^K3tKpk(GcLjqU-6;Fb2VJ#)<6Ak%kFtsYiD=hcZ(}(K%=O|7Xf*O* z&*VTQw9yX>ktaPxgIaL0JU|vkAFQ%Cyb7D0D$T_J$cqg+{=)$Cmq}1ZRcy5f z_fYJRai(@hm>-05Yi-8&SA=Vp=Bn{MfBc|-SWEk(9gpZ$5w{H7zn{kCPzeI=%s?J# z`4@iRbp%YIktdJ8D(P4I^0n}*Z^_y~!iK!dvG+xT+ed7%h(?dHxgN(czfb>Ecp3>90`Ek49Y!fOZQPE=ggfkxHrgZj$Ovaim z&klorwEP1OJTb+;_j9fS2&!!bhZbD?xJ6w+&9fv2s9}`w(5SnRObzG3`0F@qjS+kB z>ZTga2X=_Ar5U=k9XF9hhIOe~E5%ZMFKng3x#@Bc93UJ&gLd}U%l zZizKRcCj?`l+dTNQgkbGQkj}r?(;uJ2t^eWZZ57{Ek=owXQ-`K;d-5pWOoO=T@^k^c~f=-x&d%dbLraSladv2J!;aQzsC6sxnP>`d6(t zwDMIgk9lui+zM!AYhEu;7QNw|%yQ^$&qLk`4neb@7QI?&9dU;$T78st76(@9Xj4_A z;0~o;+pGu-sZZTlkZZP6nMnPf5Na*ObA^aLxmZFyT&!vl<+VY97NN0Y3WJ4Lbj|>I zhMbWPx)Kz1}<=Wkh#`TcwH+JWoQqJ1emk9Mf3>z7#Xm-Ziv@THEX2 z9&eubp39`oW#6@_hob$pyG#qKe!&1d`J3*g6$3DJ9Ctk4K2|5;lo1oqOrbkIigoi^ z%aQ5FvpV20fR?5fk)O14MU}Y7?5dN(BMHs#cG^0U_;Sp-4u4Ab7}w{l@^piZ2)Ckq z+rBcXAZQUJ?AVrd2U}{Fwix)YSahwnI=5<$PFM4W-dd}{2B75G^E;(v8Am`Db@@+= z6R*xbf`tqS?zpW9<18Eqj|qe!(z+1ls-U(LcfAK2C(OnP0KrCo#9(NXyoQRz@6A6Cud}(8zemlX} za~#YkCd?D8*_RQ;DC@y$r~#XzUI*nuf(RMmKrBzhI!}bqlm!$AUj~?NYytX19gqz4 zq$$?}|L}sSA%QdtFaW{FkA*%9g*u}>vc3nhcC{MARsZ!%j$%3+m;`)q4y_M0z?-Ht z;BQSA)!V(PsY60^HOUCrXx}OP>U@IWrK8f1^;qxA zu6O#^%NCJ=VN9tS?suSd8w})1iHuUG~Y$3T6HOQ{E{REdnPDgRGgog{vhY69?=6!BUTwoWqtl zQqPmdG*btyhll$sC?m*mkv(j)AQGgQ&KRTwhH_CY+BkFk_g8NLB{#E~QmZAwFj>XH zbr#3a!E`N!Ov1V{@fi%4485V_ahA&CKoaUBQ_@uY(2Vf(`yQ%9Ew4&FQWP3zq5@i? zhFf4(e4=FpsMLU50aiY-3ShcjixOO7J{LtJfJ%f`bP`#l@K6mL{ed)AdXf})-(L!h zBo_^+F`@v+5||aF47MRsb{5nr8moY6kkLH>C7$I}0l^&DH?S9|1p0IMi2oTnnfyE| z8wyJ=x@2-b&G7H2%LWMHvzcZ}K_6?9NWLI7rXz^qNTP)$-M*x40RTkX7>W_(*;FS* zwiiedI1b~L%W;yviVI=dy9L!2eENVksC7|OHoN;%qTg_t$8funhnCX=m&StST(+`a z5vtueAC|lk1)Q))RC`Hc%5UIikK#V6R%GslYl+i2g^J5Ix6Q z36pyTWKXnC8wrU?Gvxs-JcfMbxh zV#(0u(XjynWXN7KN%Mr1NV&QyHnyC<;PdQbjBDlYeB?Oq2~an6G1#8=e5v+wh*}nI z@ClaIy*gyUr+Z~o5f*|!`@(o}`?qo6(z7t^&O6=hm#uJ5f0w7`PT@=9Z94^@{>5=& zN5}o`bVl~?%G%PzqccB?U)FzR%tT#R?l#C(Aq(K$=~iG@k@KcHb62@tM(La;b9>Y8 zDpQZUxbCQO3Ba^Lx^;da1L;_{`>xot_H`lmx5t1z1>nbf{!MwplTat(6}1GgE(9#? zaUez+`?;b$87WPhh%q@t9rlpikAXeet&utla^CVu@v^eND)vIcL* z(c}4aKX!+^p}fJ`Vrnt5A5+h>dFe>$<$+@rtol4YeQNCZcjNr(pw^ecKwla)s_diw ztNg3o$LBT^;>-e^Gl30DnwW%4_d}W){HZ6+4mbxRe9d&%kSZz+pQyH$wunrPqsl}w zrGOE@kEAU%bVoMDU63!rvddFE&D?JbY}e6`fe{fw83-cYhT>*MPR1^P+xG;b_y0Tj!~k3b{mSXjfP)tnVMIR}J*jVB>^ z381F8VlgvT*A@D}?nfRQOXz9P|8wiF8mZo#-zY2MTm0ZeY7@`1z=318C(@d45gyCy zjQ|URrL|>X!<#un2$h8Eaa#Xikm{eda?sU0YeXcPRJ1h#As~bTi!W4AC1-~M>*-~O z?a$`!f(gY~ZqImvTqB6>L4~kov*b@zWLX*{)?MdlS;TMc;-w<7{We@Qiu^xFNy| ze%huv`Z1!5r^iHSWHClP_Pxv^gv>;GbGZ-Q7QwBiS+M;=@S}y?_8=iR7xy#gaNdjg zCgkWu@?pQekidUE!eDY5SM=%dc|!lU@Ro_v;gd&%aox(H=V1}36Lk^TXJBCIHF*WQ zQw)7%7N+RU4}Bq+7yRArME3U&;8=-$yH@pFUAjq;@Fp;*85UuYo-;hU!(TCxO1+CI zs#cbxC^CUmZVd~fs}PyykHt$?1c=I%T^Wx-DJh+Al++xI2pmY589WI#1Y9gs@nIfv z7-mpxhOhCkj8&)TPTVu4S7WdR*dQgY8=#et(6)&nD%QXI#0N9|cA(%+qwM&{`80I< zhwCXeec0C3!d;Tyv>BBQaZ1a{s@74P;1R0Q{)9r3K}*L^J~s_PcDAT0fr+iK^%-M-vw2()SkUB< z#Rvl1e)iv0sgJ{#bc_ChVaG-{iE0LXrdj$6gd(eWdiH!{z(j^siD5aJJfvkkSh~xH z;KCnmJaTuR=YijS0S4y$1N0)(+ejjuA!0BF_5%xLECoc8p)3~ua$5%!8wdY^zjJve zdqz$Dp;s8Ga?*u4dsn>|CZddNCk%BW0DN<)EpIK1D1qMX)b_xt zUEZ$9Px@*|Na!kk$G;?7_ybOPNcYm2bv|UF%GiabB;QljeF&>!fK1u%G{%kWW-QXk z2pea=w0u{vO!0f^UMPVM%iUuGL2^{gGgZ=`saF_F8N;oJ2egLaoQN5qEt<6lA~iJe z?hHXMLYb>=0Bx1ve-(8WKSA_ZOW6@Z1`!oW*2f;0O!isNg*H zAyIe~u~`z-^3W~E#|x?K!BxC(oqs8dhxV@SC5L$704621-td|k5Fk>gxNL`6sN?dJ zN~`3WO!VNW@r2SHx&_lsl*_KY-wR4Pr3xw(tztQmxp}H*7d9HDEt9TD6gqQ4IVn~S z-8WaSZIz2p7Hd)oo-@SO>k3g_zCMg#D5m+36F5krl4bFPnP$V^rR4B(aP^9+Sm+*` zN-c>{00(j%KV4hQ;UA$q%)syn({sqn*+ zXjVOzq_z{OmV;jITF-T2-Vu8LIh(kIuT0Dr&Y@SdVQ?j*pw&ozhCu^P4|axJ;yu(D z%0fB^;Xl&pGv;Ef!oykQX zAj)MCtPaU%h@@297O^)V#S`&b63@evlfJ*`p%jU!6dQ4Ql5lO6Nio)cUbi3x18b3l z7$AlX1mG!kp$jEhiqQuGrC7BPMlr$U4nAl^9W$w)J8)V=g_Wn91HZsOZSK$Z+ZOiM z_CiFdd3maYU#?O@~1t2a3=_yjzos>qn zWy{df`n^0nO(KvMMX`yZCL`~9$+p#$o{=R&(oWOLZO0n|7IXjbe;!U-*5cWsrP~+X zeTmstNB_KVn=?x0r4Q`@OjTx|Qhd5||3*?pus^+2J1Q`H zP_aKTf7PdV7%XjY9T>CiL7%4i>B^d^nwJoy*OcCxC)QPuubAg(6%;J#SA@Q*`lqmh z`%__5aByVFui4W&XmiU`l9A&e*9?0)}2YjZfqGhJ80-taC;jttE& zTI`wv^j<)#Xu8DqQ)f$G$QqnB6fd|orO#-HVM7EIH-ZoqtAd`$SZWKaU zGP~Pv71SmSR)kj6gmG?Xp+VDHlg&XN1gwaO4UM)}#jl_RiVng+r)YvCRV8q26wV#^ zT2vW-wStUUXM?a0bf2u*z*0FTiO9-c|D_8Apaf+w+Nnh{8}I}$zJCh!?*Y#b<_c~S zRSxR!p!m2!`AjlWG|F{MO>WzI^+7N=j{}ouZjV@2k=`(A<1>FcrBfjJ%T&eIf>deb z7+$x)hmKznu?UoK0Dqih(*kRs%)UEq{_=p8h8Ai#%!VEav4jXMYKOzf(3nq)r=P9y*>*szqE zu=!-m{c}$%DRpXD3{NAxIztR7e_up6sv>GM#8jMb#uUh#3fCjnO6*FRh1I@ zS+aU2?Jl2!jWFGs#2iQHOu*x&i4KwuY3V2rm*2$o_;|%vTJE8|bP!g88mEF(qzxUr znyBgLIgTwk+M(xhH@%Yy!-u@(T`wQXvMF0)Unn;p-3L=KYXZXX#pGpfnV^dS1nz*T ztxLw@pa{V5eZP=%f)>+^p;2QAj3@g{!5pDV)@z*gQ6&;lo#X$>VE+q6l?RGaz*LaK z?8_WSTjL`I)`9ccke4QsN=e~j`JFFy5GF5+ej`s_98Dj~-LbQ(XwUQa@^wIb)ehbj z@#)cIN7eMCDCp0J*Mfb3uR|g_pa5e$7peWQkt>9}>H=7*Qv7DRsS3}*Tn93Z`!7p}OS_>9UwhsRpg{SCGA z2Vp(}CkVRfYXvQ6YR6VT!4ZiM#tyIg3~-SaV6MBD#E_pvwtj2fu|rS+*d)0Y;$_y` zYm>>v7^${yEpmqPai1+Z%j(Q{+wH87Z^L-9a;ttWcQZfPTOoFnTqbI~nV$OY{2RV< zvq8ah4fXG;+|mavMrAe!oYrzcr%IUb$9*%$SfXvHFiW2E`ttEaiLcATW>eLIiSE=M zQ|T*ed6qX~_0ne{vlL7jaExE~5p>^~PG_FA@2y|fQ3cllXdzfJtA-?_Yz3sOhsF=V=fi;G|FWBz^FL|H&iY?_lo}xQpBq5? zPg%-3h!AE^_i~;WM4_@$Mm8hQ2PFmxFSIIZxyn&9eP4aGZybAyDurB+`y+-PW6y5w zz4anfaZ8}}WPS7Iboz&a2g zdPD!@{BRNe(`7lwzuPePpV=1_A3)(~i3wHx+!C?GppkxXusFHAYAd|jr9F*2EZ%7N z!Mm5?;L%HA`8K&>t>G{OJgKQp(9$oyNbMoaMu43en}?&y@dD0-bOdZ4qj;EJ(&~`I z+UwY@YE-Wv^?h^daBQ#_hp`>Y;NpoFxfEdt8doPk+=qZ;xaZI^$^_yF??!kdI7fax z#mAzh9HrQ5AGCwvJKZ}cmrSCfD%~Cn+RGQ59-_nP3SxtZ<*F^IS#42JgR2xvy&u12 zV^T&yORlFrMFDCm%bfjI#!_3`!Gj~CQ(gDBV` z#$M=`)}`?Oh%~8JGUx_OQ#Ji7^yI+w2nT{@Ri;3LVy%SA42-9tj3-@b3P}MK4Hh~k zaY^lH)dLmAW-*y>geCx%*160zSVCdvE=I1!<_yF2}FSYnzggTPp!dlAP(85M^ z7}<;)`FVtm48MSLroyVS(HFIdN(c%&Q@9(xCG#zw$hjrrci$B;4k4Kz%g0FmVaC90 zt3Sk?-hK*gn5%Z-P=a7&{}R2Ah&Pfel;64aFnfTNi*vO%3BrBXD+@Z#Hpr4GZ(yE< z-Kr-;=m0KGdlmXmJK_z=@9>I3<>VYi?Sk^3~ z4nacQh%@TtPgj4@+H(+9_iIV71N1saYUeY63s4zyfdriV`-if|(P>Hu8IX)1&~O$Rg8 zvI30v5s(@Y-!WQ@)4T+qiFWm#G6~4oHPmV`kcaxIGN)ZnWTczT=DUGZXOzb4oCV`j zMg|@!>uRM7XCo3kd5o!{1dJc^{b|cVw`vf_Kb3$!d{h2<71ZzL4X%257S!bs7vM;1 z#NiVRJ-0+M08JM)uBG!G3UWgHv##Pyf z>hF)YleL~FKTrxbQI`d93o~UYGO1|jW{hARj++g{v;-K1J#pa>fH)IJgv8@(*%D=e z(O%J6ioXfbyK}y#5NzMY4*(rrBBA)emN_HEq?h2V?Us!f3;yiFHFFm8c7?I4 zRQR;lpaEy!JiE;0JtVh>@!) z90CotAj_o<52Aw#e}Spd`w2TX@ZrLl$cCUbKm=x_hLi>so=$<&ihrwWxEV{^fMTYTqUge$IeYX#0iPZOCn=h}b8vtb3uYqF%>80rj1KJa@6#VD_kv zU^IJJ2(JB}K3Boa1N_-Dtz2wXgkMp{_s)q0QEQXV7X0>@yA52K!QL*CPsJX7vG#!= z3uZtb(GP(xRlIkKrbBkzk!7%r>nxR>Su}>tYd|?zo7FO0_J4Vn>Z4$>!`Y8U1yWN8 zP&z}y!pjCJnx$ggqyoQG$9-}bgD#Y~4v zdIUPmse0*nb>OBl%$z-4(cLdWarafxa)>#1yv`DpJG@e>^RgGA#BH>;acx6i{YWsX z0S~AUzY9F?nhh7nDqPpjrs+hKtBXan9#Q2R2_cu=@(xuXh%_O{%p7kZ0lEfgmKcz1 zr|?d4C$+_P1LPAA9MKH8fB|KWJQ+LJ*+rU8G_Q{9Ejxl&a&5bf#_BC_?*$?`#iEir zCz2$%Vzjz%wPR$(Fi~_}?Q;^GR|2w;pygX<$xEl}$viCkC9O}JwyT(->9D2fp4-|L zqj0Rt;O1M@Y^g%v=BBP*1T9=DMT=Kp-?4SiqcXnFfOtd%YT?Y*Tn5dx2kjC2=;GsqpLD19SJw6d#^rH~Z&Cg(iOy6GTw_F$A^EOZf$Son*M`FD>Z{`@+eG+C&>JoX z2BI&^YNE4IRT%b=n}&X5`co;WpnSgruq*6cfVtRJ$i`8?)ZoV1)YPHLBXR7Yj0?-2 zwj-1AHqb9-!}wfsa$E)4My}8Ya%GxnHlF)JBdpNLZzYD$&g5OwhqNDVSnMjkc`CgB6IRfoKa>Ui&CPaU8VpF z4zgqa-p?6hB(`xd!ha{Lyc}$@n*Ko=oXKG%9q^$BiK-zL8KO$s)nXTRw*6a-%8rH~2nI()1qxDiw{#xA6`Oc82>;e9#| znO;6or{zfQP?ls}5q=HUO zR$N*)-vf9L;e(not%iGKYBIDy=6#(ZINVa|eLMiM9k6;~vb#dSRCz=CVBvz+y)9Za z={!_2328eB`?-~fi7EFgGPj^A*tu-Oi)3QIap-b06qSK?-D|R$Oyhpwas`%R*?77n z{<%V>VMC;_f(biNK`y%}Nx6h}3HGM-G}(=%gt}yC4bgrssk|F$5QPexAq30#b2?(9 zML8fOZ-PEzGroeGSzL}qQX+ACQdGgmaC=ePbX=XQ>upKF=VT+VO--p6TVKuRAKzO|FE$i%>2Aa#0Qk?1;DC2vLJ-p2Tm2%O3=%HVIhjVu1DY063EK-TuLW6F|Te#sWW}naF4G?CGk(f-_dJQ6n zs8M8v9ZOsY(YWV73+{s3)a_}ycRvf_lZZT#*Tb$<5vg(RbQ@tFLEfwMX2>zf(*VJG zczLTPTdcf^?RkIs9lt~pczuxgB?ExZR))|P3RIvTkZByqmXKEiY1>l}Rz;!RXmVUZ zt6G;T@*$v(btba^5WYK*si5TBmWjmT^9D~(1&DlaN?RNp8F!(De+J#eOF~1sZ*`Ew zycFo%ap4Vl#6At<%w4pLj=6O5pKzTlJMf-mvf*F0`+M`|!T61o1^#65qXV{wd@DuT zHp)ItS4qfhDOijR+f=AX+1qkBj`FuqMY$St$*0$cn#JK0T+E$d|k3pve#W)m| zZgKIr?f2lJa!9wJiDk}iLjaNTaP1TThj2;(Eb3&(A4MU^Y&_wR#6nE!@@0Tz`T1fE zB08cXC^IekEf4rbEKc*m(g?RN2Q{V2<6p zsinGwzpL#Tw?6cjd+R{_ibvKZH~hSXDq5ufsyWf-_0)WkII&f*CmLH_*|2qCKD=Q5 zgb21}AKUg|9u@-`rW+&#m9I&1~c9{P!_UG8zgtj7fiy; zKP#>*!B-a+*TYcW6rk@46%m1AV-qE^Xu+LK=`OqM?knk>)0<+-iU02?rZkt31d4Mi z=>r0*$~=k$6gn~4j`hYES=jJ7Qx;U4p^(VsK45w;tKXcy;*Kt(*r+TZLx^4Bi}M)w z3Vbzo@_sY2J-`&joK|vG(BX;wQxus zwH&_)B_j^M%$gWV`r8;gj~HA!Fx$(Ru*!TrIa)vM+C5|>h#Gf|1fjg&EF(rGu2=(V zvq{5+T3{-*T3tu{l%sg&6e7Z_T`j?bYG5@yRN}_MQKV2KP6jH>YfcdHXOJs*>Z>+vRMVeK&u+qk#9%OX`ZZvBQ2 ziN%>=AyJUZANS&eXjKB#QBxPD;L~5YT}@#3suOEEJZ14YPjcl>M+Mk4mj(kfXd`0O z-*yHc447O!m~7~pAJc__bIW4NaDSp~xmc68k)!+(VlEnWNj7_hGgB|4Z4%tY5ZRPot6&t9*h6-c%Mvn&6YE%M z6*6EEtuRv|-djTRVQ+rUH4=p*A3J2nE|6C??Xx`|J%G5X}sF&b~uGrZzA=S8VlcpZAqLzC)r-Bt7A7{i?Vvq*N z%6|^xZyd+6<4(Wgf}Hh6!F zOav6CwKjpVvzq=o%hTsw@!!p{iaQ2O+G#TZs_X_yYTOCR5UsA*n%HkrmWq)p<0xtB z7f3VcLa=My5(B&{5m9mwr2Yg0PaNc9F3T|KP>n$48r%s&mq_ANdPpX3kB)ax{c*yL z132rts5)mXLS00^tn#mTwwZk3;>cyn;8fC4427%}Da5zbT3;>9*nYB$Kq3oI2b%(* zz`oxoP6+U!ED`i(w_XoDOV;-mPoM-=_*L@gGa>s9-^!ORBi*F7wv!+`UNbH%x4C;= z!>3tx;D7AuPOAv4m!ZEiejV?|Llv>PJF z)oO2Y1-dQ)*sB+AAwqn(fhVsdcc=uHDEG_290TKvQDE|q4ie-~?Q^1*s=%zx08-=j zLo0vK{u8o6Jl*NMNoIpeYZ3@A?5p}E@4P^woQY(nBoY?F!Sb-#>hHk`Wj)LEN=(_x zw5Ng;kyn7)T{;b-(T!JJ^YTY?K5Ke|b03|;qCPFi+L?hWB;U||lFoTu4bH`?lBb9R z5$~LB-Ye!3UaJjhQk}T{^Oz+Fzy|u1QN|QEs@V@M>O=YAp@vg6bA__hi?i;mu5y|B zpIOmp!z6b-Zms29aK6VCPc&mG8|>qd-7t2LW_*c0y!r^gHOoa$(wYU`V=JYVh5iru zV9P>bRJn1LElQ=gjjF73C5cR4m;v`q{uq|M7TxEg5cOBuNY*#r$>#1gz~4Uc+t4xG zB-%@)N1kEbSb`ZbCXFcdNp<40q-HjWW}nCX{yXi9znY6H;U`zcL!zyg2ubjbe_U&1 z7+2nWyK_|DM0Ol@+gvE`&F?xH*(!qJf@;;JcAKkMA@ZF`$R2{M#3>LwWW(Trx!ORKPraFsEe7I`fB^L zq6b&vsk)PuY8?7XEw0+rr^nLlU*6YJov^wjs%H@m95 zf#2tep+G?)dp_|WfNHW2scQC4xHR3?Tdk}&W=3pYjxVq01oOuWF&oN490I;XAt8tK zGY)rFT-ei9t)x2zTaRDU?=zpMciV(}jAb+F;a-ANGk4@4GMqu>zUffRy-Kmht>rvq zx-3T7wr<+0#?KpjPWryXy=QxM{gfkTZFvgx48|Y42nrVlfLssW-prJj8;dl}bk!bB zbJ1P>)5uG8<>Uy#(qrv+Ri<2*=BHjgua}$W;{&!)#{jpY_VQ`La*^N#hsZ=w^n`=Q zO17VgY81Ru7xSo|sW0IB@OmH5l$USEl(E)55NksJ(46Svfk-%1R?_72)p-CSz)?Nc z5CUzilrab!0NKzLTWnqi^m_PyeDhB!(NzS<1$UJSPgxZaV4(a4BsHU3}H z>KF?>VCvtsq@72k^;n)C-`|(SlHJteAT_rTVM*6Hb3ySnlvrGiqIAVhRQk^&5ZU|Eqn6k5iWRk5smF?#Y$^Wg}E z2Aji>?5W-I!iZ1vIqNd*gl4%#AkAUYo{!Z?RZQ6c zpemBi(J9nv5CwTfBQ#H4FKmTqB2(2d+@xCN2mE_pnq%-`?5V1~9Ua<$D0U?EEqoV% zg#NTjn3=9m(i}!1Yk($B$V<72{2{v{+46z!;tA?`;5xSFtxYY9b@iQ{uCwviunpYv z?$z7cbI{5Djzjm{kr(Y{fmc z*4)VAqo}M-=wmFM*bm4cKC?1*+!>K?VjK^&c4UHTad>Xd`}2Fn>j#ELpP{ zByGU0UQX)0@@e0%&Yhk3&VHFjn=O_M$T{T=)Wx>rEALFof8EOG;xAZCMZ$<0OeOhY zM0yl>{`%?W5x_Ld_?gbe`J(v)I`_;zzk|_3E)WFxRnjk?in4cd3U0?@@C7b78o2~i zN7}wQa|Te=_m#R_mVV(D&MZdqi}u3f0C1t72C$!S8FX+Ra0O#VyI48c6SC8@(le*IHG>L)F#jJZGoz`eaQvUxpR2n+YFx2Dyqc4= zB*oAcl?kAyt%>v;M?eg@-^a41wzlr^ECVhfg=ER_?u;T+RE+?dv$49Vdg*K;n(q5Gih!?hBNJ;7*PN~ z{_FGe@!Ql>!sgt|(N*OpIoOaU(tH0%Zuc_mQGEknQ&b;R<-#{k@BAPKnYg0uKW{6yl$1t$+Mb=l^8-+}8n+})uboS5?8#$QV zed`|ap_k8B$g(WQZH$e_WS_hr@6Zd7U^DA^_*=@3;jGg*8pj=Uyl55`H zc&_m&FIo4T6!obh}Mzk=61b6Zj`q-XAv@prr zK6SQp($E#}mNfm_!EbJK#CH!qdE8viu z<(|woyc1XA#zBe)Myg#g9@ z6SGAEB5DvKgbIKn8k5z=zzt4srevNPMj5C1Lqk|)OY5KA=;X(2Jr8r7lp-ZGP#P>V zRd!iY({`svl<{95 zD88sN9LQO942Y|83W^XQF*97pZ$OZQaXcOOl(vjd4ua#XG6F=jAGN+R)w)r=*EN}s z8=#t_DrJ_=8Jku9^u{lI_Ti5uBwaR^Z*#*G9vVAL99|lT7i3wTo{bBN7qrip=p->L zilc`qrqB>jWRPM1$VtD-w!~jQi++uyMeJUjGBwG{{cSH~^O{x)NIG zoY&CfI+)l7G8&jEGNvjT2a>6hmYSdz7`L&7u~BtQPKcA0oNP1&6S=i)^)+ow%s~3O zayk}|PR?D~$K#xU$8Fc!?Az${bzWAA_9!h=TPcGyD)!T$c482mW_}eB86hO?qFR!( z5WZ$%74bcMWhy>wcA z18Ah%N2hJ=0ek88(`n~TpqZ|lPDip2w18Hy-z|BiSJB3}HOA@0J3zZz&PUyU?E(it zw_9#q`Udkqq$tX!DDBsfgWwQ2432;va1_z?ZlIu5n`soOi2O(cnQa3NE-+wx}BhBRnh3E`c$(s;9bp5ln&0Zq-{yGS2ij z!8}+5OJEsXXUHV;$;m5V+O7V7kDi?YTG}j_1I&`}SjhG@aMi7$Tu*2-3t*N>kv~{z zDB*adhuu-Y;K=dh**7KRimcm#PrBqK#|l7|z^g#Gz|N4sXdBWNSwpgRf-1M3x0(ez zLw4e1$Vp5L)C;MHaDibV!%!+vDkM@n=x{snQ1jtNbh-8Y)+HjvDwtz`tNfhIIVYk2El}6la)|E!x`}BTe%zeIC>7x7HTS}MQpS)DM?EZOKY21C&lqNh= zdrxW7Gk1O}O?hTxQ)${flcBBk&3N+oxq0$tB1PPm?fD=J>OeivH=+SFf;~Xrh$hes s^m%9jt)LC)^U&_e>j&xd@4woAe`1&CmrcC`9t$!!IW`IR