From e7f53756b33f2f0f01f2fb89ab1fa27a42f8e4be Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 1 Apr 2025 09:29:49 +0200 Subject: [PATCH] vault backup: 2025-04-01 09:29:49 --- .obsidian/workspace.json | 2 +- .../notes/10 - Consensus Implementation.md | 23 ++++++++++++++++++ Pasted image 20250401092557.png | Bin 0 -> 22117 bytes 3 files changed, 24 insertions(+), 1 deletion(-) create mode 100644 Pasted image 20250401092557.png diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 192a8a8..356ff48 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -215,6 +215,7 @@ "lastOpenFiles": [ "Concurrent Systems/slides/class 10.pdf", "Concurrent Systems/notes/10 - Consensus Implementation.md", + "Pasted image 20250401092557.png", "Pasted image 20250401083747.png", "Concurrent Systems/notes/3a - Hardware primitives & Lamport Bakery algorithm.md", "Concurrent Systems/notes/3b - Aravind's algorithm and improvements.md", @@ -249,7 +250,6 @@ "Concurrent Systems/notes/Untitled.pdf", "Concurrent Systems/notes/images/Pasted image 20250318090909.png", "Concurrent Systems/notes/images/Pasted image 20250318090733.png", - "Pasted image 20250318090909.png", "HCIW/notes/2 - Interface and Interaction for IoT.md", "HCIW/notes/3 - Beacons.md", "Concurrent Systems/notes/1 - CS Basics2.md", diff --git a/Concurrent Systems/notes/10 - Consensus Implementation.md b/Concurrent Systems/notes/10 - Consensus Implementation.md index 04e5346..1963ff4 100644 --- a/Concurrent Systems/notes/10 - Consensus Implementation.md +++ b/Concurrent Systems/notes/10 - Consensus Implementation.md @@ -106,3 +106,26 @@ Let S’ be a schedule of operations only from r that leads p(q(C’)) to a deci - Since r cannot see any difference between p(q(C’)) and q(p(C’)), if we run S’ from q(p(C’)) we must decide 1 as well - in contradiction with q(p(C')) be 0-val +### CN(Swap) = CN(Fetch&add) = 2 +``` +... +``` + +### CN(Compare&swap) = ∞ + +Let us consider a verison of the compare&swap where, instead of returning a boolean, it always returns the previous value of the object, i.e.: + +![[Pasted image 20250401092557.png]] + +``` +CS a compare&swap object init at ⊥ + +propose(v) := + tmp <- CS.compare&swap(⊥, v) + if tmp = ⊥ then + return v + else + return tmp +``` + +Exercise: devise a consensus object with `CN = ∞` by using the compare&swap \ No newline at end of file diff --git a/Pasted image 20250401092557.png b/Pasted image 20250401092557.png new file mode 100644 index 0000000000000000000000000000000000000000..63aa10fea839de24f84ae7cd148e548503feb00a GIT binary patch literal 22117 zcmce;Wo%qc6sBp%F*7qWGcz+&%&{FaGgHjWY{v|3W`>xVnVF%@4C{P5BaK$8{k1bC zb=Og~RJU$-)u~hOd2WX*DM-S@;J|=@fWS*jiK&2qeCzzO`=P#lz2n~@RDV^__EK6- zARq|+|6ZWUv4ga5E4tosopV0vB4ECR~`mGK0Kf?xe3>@{Y?Y7SL2|E^?M-{~NgrEw zDeCA^#y!su;R|#+KU+stAD^oE4DLeS&R}J8vd==(j+rV!K-eHMq{tFp6uySrAvxnl zgRf`ZwRmlT*p3_1UfK~oco(sYcY6Cl*?#e<+8m8tCrJNhOjzai@y*BeignNSt=ia6 zw(ms&3dFnj0YZ4ROn49RP(#VjXsh9V6{l%Byp#l1bm+Z_p;k%kJ~X4rKHJS2*w5jT zzyM;7geD#Xl%KX&nIsCT>)xt=gqt2F{-6y1 zb{fGMt5B7`J~gvgS8(fp4f^^?kGAL*frHUX%d^X`xkk=8(CAIxa~)sUNqktKaC<2w z7}dZz@A?~;;&%|Zjf1>t^G^4R0u0DJm-)N!{bP6EY5UM9m&SFXG%DLkL6WT|M+-Vc%>^^L=(5 zL~m!~Chc5n*yj7=$%cSvrl0ZmGxqn`ORU`@`plL$VIN8e5P=nsc>0PB4LrCuJ8lNu zC?kcT+mB;f#owFt$3Dzc$VM$yf;GPDv2ES%CKmd>zRV>Z(AkEj7AA$1?G_I3*jIH# z^({e<->_NI2Tds^8e5Wb>1gSL^`46WK8muIpPJ_lN!A~{A?XG5vcNq%300C?*k|25 zrQb7JHkA|D@`C4lb}~0Cx3>nl8YxXFl{IB zNHB?Ya`Z9}x%}>lXnysD^fhyDO?S@~N7EhgjgKBBX&R+D$kNI>fzg0Yoh-8JJq9Ad z$}T^X58zd`NUQo#jE$CQROO4!>=ePG(jv25XT7dHt`ewC8e*ngdB|_hz-wouE&7t2 z1!!_xV1vK8L6~ZA(1})BQVUCKX!t_s&`LnSUBtc!X-DVqTMm>?V@iWYA}YW=hRnch z-{vb+;%1@l`4LrFo)Ky)*m(I`R&X2gx^Ta#EiLT{@YGuCJ}#yi!5jTtJZL6w-(~pj zDjv4em5jrnoPQ%dUZvH&TrS7OS&PeMHbhR2>m`0818IdyF&8$%#^QpojJ$10VqC9_0sX$6eVfCoe^TT1G!Bq|4GOf@OfH>3 zjtYs3^l2}*AlSbmZ!HTJ3Ozu5!=EUX^!JOBlWVVN(aOt+LRIByiofV%Gs5Am*1$t^ zcXb(qi$xfufoB?Qz-vB9Se*#3etKl)B$+a1V%d)uBk@2%t+W3vX(r1`T8una7Pz*Y zu2W#yCi%PY^=vu=AgXJlWhybA zf}ybip@6_=Um#R5=K!OB=RHI?JpQ&hYGsgjCGEZ)reH8;H#6*Tx7og6f+*$x!4?&%G%BV@=-($iZ{Vdb zRIi`5`qnsY)?K%EFOC*2hWrvzQ!5831!HMT1Al?#P`H%ik|o@XC9e5N&%3hjUS}}a zElC*#^$tHKXrSjjBozh4u#~s0$#ICEqMM8NARD~e9VD}ijeZq1eO1!uocgf{ zu8COSN|kUweuj;2#e2aRv?DXc)VSl@fYmHn4s+kD8=IyxTTMdak9DTqZ!%H5B^haw z3PL}x zUBFz5ac?+UM{Iwa9wdcWYd*p^xIo8xb%jnHcWdHf^l9?5uy`xzCtYgQdPq{`6OT<&`T<01!2?O z@OMMPZ0Oqp%~&a|S*B+wJA~XI8s%pDq3!mgb!ypznYlb|Xb;^?AJ*W$yt8AV2r*WL zr|NFlz6_e#F&oXXK#5{xEW-98XEw1S&)gI&R=S;tgn{>dl}FQ&_x6b0VddLM=D4Wp zuL63EK2D16q_CC|zm;9LN+2>>t*&;Q5gYCEk+gUo2CuyX0zWJ%%?#+cA`9f z^rnSVo8j(Q&S^Q-|aL3Y~8n37g5m5N4Ea*FHGOR|upck1FTg7tIo zu~8RdWY29#1N+R^qk-+OG%A9(@9V>Ag#08sO?4kDYU2Afaw0d z^@;pu#+1duVzbO2e7x`@w85u$-2kJ`L0N9Dg$zqIG@XjN_5EaoUz-du?TN08z+kC9 zE!s%dSzF5B7-E7QfBBIC82*|0q6g0w32f{dK_1x*8DRyHpM)Y^KQ9(b8}QH>>s1Rd zmyrk3EcK502PgGAeGIO;@XHU~xf_cuJ$%~J7ovvb!4|S=trcbl=Zr7TM{XS@2)<3OoeC~Q}97n_U-mf7gm&x8l>_x-SE(=g^H>55A zc1O69{J%A4G3SOKmmAkC5Yfi`-!@yHA62RivSP4%#8n^AiZ=8qvj-FxJu-=Ft zE-}yAGU}Qk+t!TKDEP2ZBkw@tMU&mMo57ezZ*CfhV0C(Xje-&Pm7j)sY z^p^-=5f*3n6=G;ls$l%i=*p{H$!=O~idsg+wJXkUf#HieTHdKj&r^XNNgrlqC`jK0 z7^&)$f1CTW4%$rY(_l-rz8UTA!<6VSq&8Z(ujRZwH5(!s`hn&#TRbxeY^Yn%} zwU=S1WXfRVIY3n+-#lyuO-&lBsr7Tzz2ivR+nq1E5fX$=ZNq;pniH{5mEJAX258u` z2&3$ni@x%vxiVCQ!-}J-%&A0QWn^6KyM4W5>7xX&O+#he0osA_qfdYNFRNko7NluYm1u6FydK*maV$XTLHH3cGT19 z{d(kt*rQOOxJ=0~8j5tK95|T&W3KP6T=&7gqx-(5{$(_7@SM(>qllyH_yXPTSlUTn z*;Rl!hx=J=v_XY5kP8rMt)r}B%|kFc*zdIZ*RG7mt-hy=R3{sO21Otul3sVZYV=p) za|E;ezUl?jxmD2U%x6DIP?y?f`pF6Bh{)UzmddmI^gzxSSV^iE5$l7WiUYzgyH=2H z7hEXVUPqg(RpTWy!>c`ade@jx;o$OOr4S((GV5BR+Zk?4)p|Xw;AfT#Z??J>gFYXR zll^$a2qNTevn{28vrtwJ{S_a9kNc=w0|T1xl(xqX1BA`!uq+z)C+*BZq8`<~m&E zA=9h~qCXU`^8so2eWBaf3}O6!@QC{R0=o45j#{fb`0X(v16#x69@Ow=K|aQY8^S>9 zkCGo$@LI(ozB%B&_-t(>4HM(aO&7P22eK7i!4*( z)W0j9R_oL50g*i;z8}bFcA!2YLMj$F@{@9MFi7q__lGQog!Q4{+OAJX`h@jx48?=# zTq1gU-g{>a51}%mCzMl?Jh@9%v`Z>(Wi}!)^6e&-hoiff@#g{G#ZTO?)f=?n(eYK9Hc zftk=I$)o?#nM`f#G)T#RqE@MTXfQ5ni16w4gF4A3%~Gnp=?37DaSk6J)Y&skDYrhF-m}GjEl^-WJ60P;>Lh;|b1^0BpznihgW#c5!jFS4to=wpiduc41Q~P+kWh zS%gocMJbghad3Yz2q{;1{(w+!2ZR1H4a4y(xcxTIRRhvkJNAd;d0vLz%Z#PB5RQ}X zXv(8OcP$YN7CVfPb~1CDZ*2nI@a)p{SV)G^%Y#}@^oDadYTL{ z9(01!@`XaFQ4e7gGzt7V%4jBdy@$tIPBpyq*abA-=vB$12Z)K_6t<$D7`SK`Fte!& zyjZj!s`$FO#ZYRxnPFQM)Ub?v^Fp{z z@81MFs0Xg(3|>c8e7kVKw$Fa?Y-3Hg4;c3EU8Q+>YB#6z@SY3Mei`3IrNV+lwA^TU z&F|7G!w;Zpb>F{zWbB;$BCfZD^5CX4gU9xh>I(ZiM2rR-#x}k7;8+v?Y-KKzZ@2Ed zt|UIz6X};y)vf@iXdTIO{O)tfsik+cwXJXPaYhmf*)6v1V~#pyW9SEf53OH z|D5zGsb24RxB@6uq~-38*PwTk7xQ;xpOj!lbzBg|Rz;%Nl}HTn>2N%I+1@>ii2*r3 ztE=BAvZFeYG@r-(8C9ytw&{Z~SAa>Bvu5@`Q6TdUJKw&geh5sCs9ZiyO?9Afd2gqL zF5FjGNC6`=A|jA1PCubN_B|}p^c%?)sPq!biZ_YL8}(^TmtIMcP!#dhQ)!|!fRU?E z*W0u$Wb9{$>j3pe?m*@We&0lXXZ}>-z9_`(oqqk!=LbwPX_;SiA{@pko>^HnB=>UT z^+LD6*4mkor$UTJQ1&YH8+lflPR*MU-ExBrsLYN~bSW~l4sj@vXi%V{-dRXKzdoxX zpJ-Yma1+0;>lNh!A;;0|>d#vtJL>0Ya!Xe?M_%$%miNb!M8%=HHhB7=T(9+?q{P@b z6;fqQ}xT+t}s^BIwY0b6*8n>35(V^_2_}CN!V=^ z#dtXgO&kI$IIgNN63xf`o`|r*@=WQ2P#b-aCz#@0M>0|!Es>ZGuRMLmG{`fefenF(=FVH5m3QPlZB%`4FQu()*+F}yL?ShE*b<%i3!Qcs#}q&)9DiX znC;<1z1~}9%rz8M1?ye>sH0u>my@1HZb#R`>4um3@9wyo*4=&|MmzI8oO`>$P-lxd z89I9SB0)c9gxSHko1Sr#zY zosFo6gAPchY@b4LsLJGxSa**Cf_(XX@9=?UL6{nT9ZY-EKQe(>mE&^o8Sm3akHaMy zZuOUYA&TcHH!%d^<%j4rQk_V*NOsFq+T0IKe?QG~5W>qHE&sNchxT6082p+a14UG> zM(y{I6zOfvK*h$v6ZfulvdyZ8 zoFYI^)s%Uww!6YFQkdv`_%nDU6>)n>CO7~O)MvoyH(1Q*qEByXk&Y0n1_T6v_T{$5 zuf!r;sx}AH9ZOxN6sc&BL%;6`P7 zxec_bWMzg7K@ZY}AZVh)fA={5v@|D@C3V9iB?!eq-{}br%m2;uIIX4zccKRN_h@(T zOx<{^newuVy2Ir>=bXlEl;4MqK(VaLnDH&ZhfAKvnZg>_F>Gwc)*ah>+(*eiMX40x zW`d$u9gcS9(H2c-yONAWi9#`;_TFSU_;;cJQ6Gv?&m#%jg&}b8&bjHe*EUy2Hpo`D zMK{Tr9fGhPizF6Snf*Yw%pGeQy$^7lbu@GPT9<*{z+tt}TQiZS*KDBKYIaK~Cr{t- zR3mqiW0ah#C;H2E(a;-8?;9Q)S&ZVPb1>ruC2@iee89 zV(|JIRgN!7W|Pn_j0I+ehjV z8{I(QCePeCteT2zM^?VR)YKPDA3+bZ9NYq_NY=;a9zRw6ny8SrZGj89PTALK)egHJP~799>nF7?&k}7V*YEpm)1pQtjP}-P)eyB+o#o*Xcq)7qy54B{Of?|hC&is zoq0&XN(r|NIQG}Xn$K1fr`U5VO^XOGak)0NIu$8d_cy}h|n z9kJIjm}*T5{gn2#S5%0Wk2zjcp;^w4FV8WeqvJDj-n~|zgZLo3XpQ34%ww*~PhKi+ z@vaiOVq>S<#!P1gGvyGajz~)Q8Vvm;yef3gcqie$a`YqqL3S+lI7yO%+dv79dD_V! zJg#_A(N+i-3kw@^i1}HRub49n3TnWw^RgHX^fpf`1BB4sVMMPuOfnZq^=0)3&b3RyR$5+xy}7!JXMH=RJ~9K} zG3>S&4;UgCBj7LbFSrrd-Rv&>nLp!~)pD|b|3>mh=!x&~GPv^gb(jROCr~B1GN2v; zsuVRftaRn2Ci&MV15Id9D+8rZW7I6(|C21F6t6}ja?dGg%xTBf>~ygG$vR?8(_1HJ z6K0LiDvY1~q2v%o7X0n+l?rk8xQ;^{R8yG6qgWEZg}S$xi(J_}woc{~Jjhk}aR_C5 z;S5gUFt6e4$%G>lo8o0~wbY=I5uWha=&{xvk7n=*%8N58YO%^sKUzkL&UN=Z6jW*E>t9fyqpex~SyPNMKYmuEIF9D@I(%%3tEY)G z!{?QcqEMxaPpcX1R58_mSYaSq7RM0)(8VkR0UaDH8`{YPiR!qLH+5o zuZvi}MKJKg%%zf8=K5V`ZnpM`OD)Dh%?tpi5V+m=II$@rHO8i z#r*Qj^UaZ&kzX1;L2_%P_6MqiOhd-cYSUM0u3hqE0n26g=TDgdc~Nz*B&9q?sYCV7 z7l@;6sbnqr7Z&3`Y?mo`$@Yxv{oVUrOl%<*B?JgDdUOY%OVlS$LiA6W^9$n2BymQ+ z;~0HU4HwJ81M{tw=lJ;==}2rWK(46ILd+=l9Z~_FGK(|SQdt)H`*}irfp}H|h>V6C zjI+r&@aGcv<I(VYTTGHoF$yvfZnpr|2qRGE zg&hwGY}a*vHQ3J2xC>9xaG3${E+rbiYC<#s!b9yQu^YOBCljG~Hbz35BbV zk7h7MlDWcBeGq-%$d6DpTc(XSw{;I{4-A2NQgSOb#KK*T^n3fWye3P`eCG3Yu*uDG z%SOfkw!3N(S-Rr>pyD)<{k<-9wgLT(8ZWeJg?yVM1%QjF#de3BE z$J;w%{z~m#69~7+fm^cuNm&~`zjDMyvhMb*v9pc?4JvFp$?AJ$oU!_+QRmj}atPW_ zSW7MKlm@eqIYb%8fB=^qZb;kPWC^&;hmB-?J!|G5IKCz|RP#tofjRAGdDiQsOU0yL z2jV9XfM7mPSC7i-IYdi+g(n*G0t~{Itb*1Gr9me0%px^8a~#kL2Dz4$SHJJ>Ps*01 z->kTQx+L$hfGAP2^)!kW?4t9srY`M!(Uw~-dM?&9xhP08cipkh%??&|hP%?rr#j6h z0`33Yw#vi7V~s25@tpYf?0SJ_^D-z7=q?F#PGCz&*sQJ9TRsFJAC%~M#WCh$``H;UwH}UR@=3RRw75*^(|J#Ef~RY7KjZnD zfJfW@GSc3A89r!61h&46dfyR>?mv&T`SX*_ zTUqRYVRegjDhFJPWRi0N=``KQ7ZN&>4=+;pp)JNg%m@wcrq4T+)IAPUIXy}g?N$~i zH|s37@?%51UGWTANl8`57#8Sjs)DZG8Z-jk5}ka^`ZcYeTOU-UZi>lR?|n6-sr41$ zu;gTM%W*K0Fpu;%J?OFp?CUfoTYYE+jgD$1Cm^2O-O99Vq!kc3ulf3V=rK;#!L?s) ze3(Qg`zlI+$EJ(g9S$H$?eo!mplk)^b|5(D5f34Vq4kk0!kYMl?aCyX>qLakPyKNU zuO{v^bn0LrIp8j*q0k`yDB}Roxp0T9NUz5oWO@PQ8x&MPJN5;zgh%N~I?j)Y>-UfB z{aEruc1e9uf5orF^L=QXrjm%~C9LcX;nC6l9-%AqI$JbDf1JSvuHE;k-i$erK-!763YA7R=y2}1D<{dzjL0*`^S&I6GOO@ z;@?G{&_Fh(TMX-0uCK3S2?b+fVEAYuXcUf2d>kAcEUZ#{pmi z1y-ju40M4;e7auTTXBX8&?p`AJE5XMSK#Fibmpu1O85&**zaiHHny{|V}AKb z{89+eoVnuh49ScJSm?0c7_Tfi?dhG^S?EYO*CxF8pH7>t7S*-MV1D5e8h^RKi9!v2 z^bb%f{W9$q!p_R+!lvnk#3;7^}qw@t}Mm$`O=yS|#}!p(6&`~gK3p}0=Jxq$cy z4FZxI0P+AK1dsgk3t%_nkHqqNyL;j1eKAt5{e0dL@3E^XgMA#$o$W$v-9>s0+2>-> zKk-_>x?pqqHEc@|XRut@{*IxgYW=X*Kguf98)WV&DQLK;nHjez>_|BN=0prO)~udW zBmM*-P@AR^snGCZ zMBIHx-krqwdG-9QcJ~syN0crqeQ;3DxY%M!Ywd%;!g$#6d~asyx}?c9Fh&sBqb$HO^W&T)_&T*SZchz%YOF;a<=lho$@7nQXH$#?Wo6~ySjV+izQKm?zc1dmP=zI z77)-k^GzF|>}-#Qp)a-I3^{wT(tPtH>w+yXtM`TW)L!`G`tV`_Pz$m`88;I3e9&Fr zpWN76ceUhW5Bf^*%>!3xKBwVa62Fi69PAWCdih2=GvHh$@*-ReSU!A|JdX}L?Yt1% zxFk{p!610J;S*~Aj_W(ktc7j&iLYI_FG+`na?wJ;Y+gUH($o6_UxZ4e{0Bptn>ix~ zW>-$W5>cPo7~liLK6){|${p*W(mE0xl)gq>3X$$Vh*9{UbA;j7NP{3My40wWu2h=d zMBY|RTzFi54UC=7AA`H5d22980GVAMPA^`6KVJM`9~uL&n`ACEXQn@?Kyp&KBdu#1 zaN0#KB>boq3r&)Yu~6I>I`c?H`AP=bt^ajd@zK-&T3S7mBE2CNMmt@;u`ngn_&%N`##yVWz9iXLMus9&p$_=`m<1;-k^$wM5E zLn8eaATs<7=3M~xO-&3;yqp?Vl7X-zlePmJeJGm`ruoOQ5>E{&r>pSZQWYB2hV$3UTSx?Z)_b;dX{lD&JU}8hm{=}yjeH3gGbKh*waRk~y9k;P(-gm#UA|3L=K9nKPI0PfZ$q(v1L_T4*wv8M= zc)O}37q<45fCB8NX3;r`3tzI*M6@pl)d6{rFZ9hE$swmujVw_aHk=A!LOyK}B7zu` z$>)e%xd{-2$s01mQM|h=Z#RacKwn>VA za}(qo-k-!Xdud&6nXAi;wnOKwt|qOIavXwgsAoe|>%LviB1+OAt>i7Eoeuh5EWoR_^ch z&=cOS9t;!+@tg7_jmos zw|IcaRj}aTdg?j*`IhMkNA<6@2dt4@Nl|F#3l}sG`r7or+CV`54?vDT9f<#3zKUA5 zJ>#h%;q9XcP>^YI`=WsSKPXIpo}#;k)VUT?Z1jFYy|;pVh?%u!jQR1Lo zE(TxG&Tfw!QIFVsM%|}J2~%I@&`%ZrnnQ`jjaS7#%)3L10&@bGqo|MLo6a96xWV#i zhFkvIC-|G6$hRnq6DtXKa#C+I^M7Z|*785@O{yk&*zBHLqn26@-p&|4+Ecl(7ga?B zY=qdnVWdDRhoLX!_fxwhm8AJ82iDdy2aFa@$*ZDBWg!<0*XAC%&XtelyyRt)zTn2v zxw~t}xl44-q&^Y4(`au6#~X40VxNn`c~e7= zPPy`qH^2$KV*R+@MPV2`Gv^!XujdQQ;P++=eq&_KdWf9nEX}ZnykWC079I2o(PMkF%-E(?@*`iAoUJK1xy2X?PDmFL{)U$y4=iK(5zE zA}VI`M{uQA_0-SR>igZb=e`?*<8&PzZ@>XDu*w!;P#kQ|1vo*wS!u=WV1y7F_?bD$ zAS(6Ph^vHphtNmi7WWbVZ1fm<1`*Wdc9nJPuk`WBu<+Y<8xz9;S>$~Dym@#(GUH*< zZp+T-wF+JGo8m#j9z_m{B9Khi>#s%&qi=6tU2FE$l4RU}vG5;dv;oRXj5A$MfAgm# z^W$5RE&ZIM&WNosX$|=W!nD@8X~WJR@-s&u(UWzx_08s0?_un(lkgp5*>FD|qu8U@K72V})q%|ArF&K{Asr0Bdek~1_{ z_sa=a*L05WsHdZBB!Jvn_T6K@ao7Jv=O65q?dP1Gp9h43$w5=1I4u{)EU`dA!kH@? zO8Nr-&&j{zqah}x>I39dBcr2?J5B?`{(0}pIXL%Db9OLQ+58yE!@kea$wy>_B^=lh@fl|_eT zJ5gR-fL{4OHDIxi_e(^ZyuG|b-+UjAS$E?)6>e=^8|M~Xm3l-y{O~$9-`_|L>3hR` zumE_6bkO}ir{MogThzOyvogG_yv3|8<{RJRd`_`=zqLz*)Y)CKl>2po&FwhRsPfF` z;Q$*u;m~7T<~8EcjA$L}{-okReJj>GtL4pZz5_cz_fi)89=GLp_R`3pLWOZN7Azm+ zO*|8bmU8=CB$H0p!_?Mg{Sr=OqMmcze(Pbh{^J+7i7n8|YEh4#Os>(n9(xESm6?Px zHp4^PGO6i)#gD_CM2jFoaT4d)uMVm^swH@+xPQA=-iZ+s_(VyaHL^9HZTg*)E>fdZ(QI z63^)FUi>v%g&Wx3>$|U$w$kJ2JstRw7#s0;&4b*pqBa*0{_S^01oKo}cA-bzHXDUp;p3T|UikOu(PM3=uP+XGB zu3~*Z(xDkz*YnKvTA6rF?~Co?=ru%1nK7_{0Ih1|xlipoFN1V^p3mtgLs?^){l?=| zx!5A)oU0ujl#nWq*Us__D`S+SXtcT$oBm&4esBb9r@oc=l070dsTx zAL&e@Ei5+!r_Q< zOaNjz|Ne|6eR1|rhEM|^?^Bj&Nn5$SbT>2x!l)Nq)BN-s+G9IMK7{?NhWVs?Whf3)J9^Of2x3i`;o{- zaH_!xMG%Bw7cRHXxgOsM_mv{U4tZJ=cjGBuZ;L|&ane&Q^~6zrIlLAm`L*Ar>q`(G zRBxrk8iaMJeMPPODK8Nxss)(GIWcv+KJ0rw3+JBkPtGUymZVpS;5P@7Awz z7r+fRS-Kc){!DtDlfac3kC6w>di?(L_0Azr`TE&B;;o6VN-CZ~R7LKjM?BQ~5_v)|qFOVR@2Z{&jbszn+qETa z)9~orxJB&jeYV?K-GPew9rho00WMAw&LqzKA%<VIGNJj-ZEPLvi!K*H}zy0Ohbi$TdQ8q+s=9J z8cASE9x=y|k+*!}s>lquJD~p`s7l05JvMw+(=bORiU(AjfMs^PgKbqNa+^L7;9=gH zNPCjrn&iABZ@o`$2w}eAcfD|34K&INnGb9EzhPCy2D-&fvlT|M1PL+x(|^2d4G@`P z${-<0Fq(Z(d>D%Clr&VH#^;SQJrlC&uNB)ARB~^UD6|=QxzG+Vi~q^)-A%dgyDx8C zwBS7qjX=-vo^DSde_tp=TR`)R-BfgsfiGBf-)P(G2Eef857P~_DmBR0e5$-=7_NJT zxhXn-a_>M4omqNYa^K^WVu2PFiEa}P_!2>`V8V7#HN0Yg-vV;wi1x*&dZT@RdY;(a+3~?aYP^gtHSMvV7v57Qv^ly-IAYku zOzq%q&h}0sUoJ;C5>c^FzKb&}kaXmdZOkdN`0#e3V1u+Y!})15A$AcSFq?J0>!wkJ zOGFd#+=nvf@&*B_tOgUD{_$VH!O z4rV}Mn_~YI)$H9`AO~VUp%C}wl4QSFTf}yv$Q7$Zmjj2d)rz-_ zhLT;MkWit)^+&rUdJRTf04{UJFu9NB#DH{C{Xmh%u7I-1jnAox45v99(A6ZNmBNc` z;Wlq&LaOStLd_-wZr?aprVZ2yPD#@a;N(yaGBK%$S*C_AJla+@>*{gmke$iKCJpIX zg3TM7#pm<#E(raMl6?x%20={nk7RA`{~}ozXzWPCi?ff5)La(P%0QSpjW(&!(S4?V zrt|D%6OI4;Q8MufX!2o2lPio4YRkY($7gdnfUk;Qiuc$^qWptqVxqp?>BNcYC_yIP z^Bi^-l->}V0BO33(cSoX1!KOEZ=iNW8S(7hRkpU!?l(0QX8)QX-3zGx=E@!KgkNV| zWl9{hg7|v5Kls~%H#Cl8C937v2%Z|bL~L+psy#C^au+@F;fX#>eAx0P1)9b-^l%Sh zP<02x3X}shQoUQb28a6>U?`2^Mj9OJ;VT1k>}P~5GD=KqE~nTnjge8TG2O z>#z@hV);9yXbhQTdinTTV^V8|CIU6jDY)!PwAVpxv_6WJr`wN86YMtJ^5<{Qr&(k3 z;lSXoOE5&n$23Y_Nh#m0E5=PcFN+j&%~}43NHY_M1Qi%Gv>>^jsz%bI?#sKv?0af~ zvB{K>|_-mcAiz&Ts$e#a@?qgnO-=tB%KEl5EFF!+zl^%`hu0Y)GL1+nkz)DRZ>Ss>A3*!9BD>N?omPPDWV)4~ zC$Rel{yWYr8=E4037aw;6fwi7mx%WWH(w)gCu5RUZ4r-#QbRgWzf!!Io`>D#>W_EO zkHy0&R;T)==%+6wTd+Vt7srws|4CX{6f(E|o&mqc^pufTzOh?~Xn2b91G6~z?GQz! z&m!1+rEkE~9$l{E$mTDBAx&ZS8++V9L(MN)YnxSTMXUkm|ntw$abUhx69MK#Fj*q4dY{w zdzfRrS@iV=|C&pFYiepDg;pF{9uV#~X8B?W_gd!Wt3+598eLboI37u8qbXFG0rdgO zC{+CHfLOiO2fG6EK`7q-LGj}&U!E|Be$#qUQBn1#nicB-Mlw1KS|%nYBBJd*Mi}#G zeHR2THt3MJnz9EWo$n%f0=AdaFmIMpl-|mseL*LMo=8w5sWsTlkIJkKmcCZoP}0>u zf9)=J%Z{D$#ISW9(k)T*D|IHe8?PtXd(&)<_c{1Bzqn-k1$sHImg@5-6fY|DbLjE} z<$vtqCOA){5R>SU-%qr0yIHDVocaGpnKrU`G6aTT6Y}(hcY5AlFis{U4gUzT9;CbH z;x-gNO;0lmINWkFF1Wrdk8H1iw-lQXw%rcNkwPQ>wetZhP%Z@e@rWWGWm^dunwfX#E4-u-UZ3%4vFOR2ss<|}U|m6ea{r$1mdUDFB{*6@dQHG9 zGWe%HWOR}=EIMXLbykO)y!2RPoZs8a0CV6vAvFB@sqyZDmloc_nyYg*7K=H|ewZH7*rpU6fXyt?9}W>0=ZNOJ8M*dx71!p<76a~y!O z#!yB9FD@?j_rE4FrCi$f`MI^FWt;U1 z%U!xC)&mXTnXWO43n(Ska+vq{dwQE{H!?eLP7(oej)^n{00_n)TpWV*u{>DLOdB5- zz(>(EK{|BPL<~kQW+>1{AS92~adsu+g**D>e%Ib3=!gu3nyI!bjoRItdAEese*IGz zeDe@Ir>HDi!sjp&bP%2lb+3nis95D?d)atK$hRx*F}v#EC*E1nD7!aHoRmQ!EfuV(Z!TvES*=?b=?P2#-QdyrpP&ir)s zh~%LgHYkRF3}LGeecjy^V3erau;n&Ein1>0IZf{*I=jVlE3C1O)x_-~R$EoA;(M{~Wgm&vvIg zB=L1jxrwULVP@7{w?8_3gGX_?Trb%qkUmega)-7jgJ9gJ&O2}R{(zOgpE+A59TG4P zCrJ6GprEk%otT)|!NH+04GJ3C!O;;04(_d@2y9|{8N@G{aARtAIt#NzpQq-18a`V? zTCxOw)mPDFltj>>bEyG}z;HT)NdhyZq^-|$9oTZ4#s$2}5@hV0Zjf~7&*FZ)QnB9V zSv%X)2+ebOz_EzY>^krJ!`cgro_~Q174Z<8?Si%d;TfgjuBZGbK70*dz512xVfdj_ znVXRJu;7R-CXLU4fZJ;3pttOSMgiVH@aWOs=~2zDn_)*Uof{)Z({{g$-My(}sUNS^ zc!uqKsCr9)QLzb)%%I5|;`oX&=^GW2S3OwO?KSW5B7W`PTc8>NC-YQf&6o>|0DMAyd!~OpZ)UO(-CF zP(Xk2HE&IgkLL?`tat>UhI+Flc{Oy22=&$F-(6MS^6@I|q*-ew23OW`ai+m-Ghgdg z{a?MDbx<5npNAJuNC@sOi)-*77F-q!kl>Ku1Piu6(BKj*xLa@wB)A244?)7>yEuz` z;D)?+b#GnO-Jkc@R84hFPfhpCRQKokKAa#3(`wk@;lemVJ1mMjfsdXFDuKZMdCTjZ z7M_OlKe^Ei@&3Lt~me(?6gKWe5+(bG3#o@Y}XV;jx>&?cZtXOalyAAg;qf!49tI9oF zF88B`qvMMmDGQ{38NL)|g=G8AtfVUugTi4~aVmin9~Dc;;=rmhlVxlFJ&g(fufext z`qAxoI0nK42j3NR)=Hh9#Z*j6I&FYG%zhDj%Z3lDYFH@>VSc44RZ!O&2YIVoBI5*Jkof!BRlbXNz zmr2!(f*b{4%WI;Qy`+`f&M1AMwL>OyCu!JOxe)O5aWx_P=RwbKxii>eu&sUW){DSx zF`kIeBx8|`7OmJAA0RlfE?tAbzcHImNt3wCF&C8(~ zJUVD-taQ8jFWc`T*(#Yuf`v*X1Sw#G!DaFgATPyf=4?6AQ23{0R_D5EDj;uaF2H4L zXp*8a!e4ZVh9vs!LTOl#IVq&DR<7V)4=-2sAq18 zuQZ_M4e?3%!Y)i{g(Ea4+=F6U45i8eMXgz1IKgf{-m<>@!X2-EH#qA3Q%^ZOG-Jn4 zBc;AQ zy^bWSBf(rYr%=1_>%&RJM>m%!PHsVAGc8ILA3bG4)osjta_?jppR@+=SRozA8;b>p zty4jKTuS2~B*XyKHbOb|x}7=Xdon*YqT?jAZ-Hv|K=4L?1@^j5L{!5pun$`JVQEV7 ze0l=hPxG3+GP>)yOi~8!-PP9S?4v}taSSvrqIOfHF% z$YVJ*l046WJoF zeYQQ^Omh~V7oeOqsqO7ix=eG9NUw)@X~!kI3Fol@QPTk2E7lI9=cUt7!eo9>l& z7gZAv0WZ(}0~MM~CFuP2eYZ5$wEdTLdVSq5Xc{cmsw?<0K*(JsS|4rVOgE%qnh&~v66?-C&v~b;hx>|?=TH(hmdjZm9 z6f3EwuF1#7KL!t^5i{M`zEJAKK!(zi0HUGX{&tBy|mjW$k1u{{9E<5Z)o!xyx<#_z;Sr!4%O6{Q)j^A5+ zQu>~;5kJFaWm}O%1RNWmeSDa$6qyJ#u>t5D&E@bNF%%p=VRRX3-(rBVc|j-;ZHV$B zMo&*GHAPpGVX~qAo8VOWhkoD|()P?uyb_8q`yA{!4Yvyv0^<6uHc3gJbUb%(8h>Zf zJqFJV)4!7MvQluU{7oq+kMl%Y|Fr>j%P~azCOi3ObgNl$p~cBE-w2h1{*1T?Fdi2# zPz8iq+uHOwlexzSqOy^fXw%`!exLNJh7SmTV~D2cdR^Ev@^Gm+_?&N+P;(Dlc?|!Q zOkOsN#CY;AFN zh#r@(&d6E&QXIZ=x`Z%=Tog`@VseQZvQC2KvJ?O8I>qKJJ6f$llEhcBi7u*?Ot$GD zd9FWVK)QsschjR*M(k^ad*qJX{tSS$W`0Uml*MYHf!VbnBzpX<BDZarcHF1^h|EPcop1d-zjT;V3%kO~iBN0F za&ye`7=Qgp-}4V6KYe&3_@Zi`oYUzWHG--!GiW$?h$RB6*nqN(Ej5;oWllayymLgn z%c2=YgZ{6=gxyQ3I%1dv?;TQc`|jVenziTZrrG=tX^r}2eX(Qo;=Fs{eVIe&&AF5D z>b;$?xfb8lR+bQlxESyf0uLyDVFHIJ|FBf9qoGuCiO3x%oI|tz3X&L#%U*Rw;5|Kp zN$pp$YTp`+(Kt#??>h^!#0Pjwbj!f5+=C5~Uio%SP3Aa%bQKaW_wt}x$2b=|#~XGx zH2EpF{K6jIr}UxgNNdZ`8}=pyL@+1j_no$*q-&rzq14&ZsZu^;xHvw{Aaax3s)4sj z3#{?8&+$<41rRmRq>#It*zbmJvPW;@GgFVQ+Pg5)OwWmg$WBK*!6%;@yD+MENsiJA zVr4|PYFLS>I=}-49ObYWB%sMA;0p6Td7YauNcw8Lz?Y`^OjGpEa&9NCrcyAoH+QxS z+(RdGH6sxQ)awVnB`b>EUd0iS5qLW76uE7FjN8;!kB5z8l+xdGK$g$zT=1cy=w6~S z>$p|s1f~1YWJ1cllCJs}x$KEA4R_CORKOaiWobS3W=xb(e7Bvbv}T=q#<2E0p*mjS zSw*Fh)pt*8W;{+pvVyo0zhznppKR4MHGah_s)SL+v&nwWjIBo>gYF!IZMIjG~%e9WpmR z2k*JiyO4Vpd(XSi8)DH98V2V7)-WVGW%iw(W?1AwJuZ2SNk^$#osC3fCP~dWu)Ku? zF7QF1oyQY60TcosZq(Ufb~uM8uIz{RAq^>KELij9vaA&^N~E_iM=HMU--Kg!G32*b zK2{5)n9MMqiBkVoU;SKoD<*5?r6>2=COnZrZh-0UwEBU?Ktw3vK+)#FgGCv%^Pzyi zcl~@lH2tUX6lj04-0?Dqxf73oArDWO6Cev$fZv5A9`iI=p7*1-Fj9G%ofCW(g7u>C z3ps5u<~t^e1|ED#F=->+6hiAF3;HjJZ_0E7BSYOMiGB9HCFQ5UL|*ym75@Wks;A0> zv~`tDlFD_ryYI3zn>%NGratY9m1?r&X6Zfiz=yaf3aOu|k4#Uf6tWn{#0a!{zxV&w z28_1aM*$Sjr4N9L`>?)dY#S&+>x>d!^40ED4-DLDgCIs=Zu?2sP7mw(FGMwbhVOp9c!tt8-rZ*Z&E7O z75~R!;@rDzC^n~Y$<6?sdwdJV{K>X_`Uxs%q6F{>u0)>>2d)u7{Ulpb_pVPMIUDQ# zYdNi5X6m+uMFk@)75WS1Y%;gykQ>}o=R>P_nHH|04yf4~GRVH&=}#1LXw?6{NmxBd zt*gpfqcvL9kn-!*a>*ULB19f_RQ zfq++?CKL>Is6a7@)-noHz=zly9Zw|^;u>}v)$wp)3S2*$1M~YzH(}p(+7=O!(=7|D zFCy}^c1y#^lIt=O5#qro3(AaI<`3km$_WSG1GqXQT>x&iVV42dphb5IFty>>o*w-1 z9zav4^ukEMN)FMO5%;VHb!$uL=p3UKl@azLk94+*FSk7xmF4yPNZlGzWxX~w&Zlk* z_)_~mRVP-%+t(Bd#kZ1Wpn1J=kKXtG_)W;OYD)sg}t>65KI zfiAMo&iew@Ew(_hL@s&OBxbo^Ag4lcy0su#P@vP7Oe0wZX70_~6rVrW(Jfx!;P@Xs zRn^F{33RA)*RN$ALj!`gF*`?Qd#c!ePm(95BqXkva>Z$I5l;%gm2Y$KKRSV0l#LGU zZZ3XOE;uZCjo(uZVXDe>Kv{gQ#@Ts=Mq_!aTvH~*)I-31M z;%H!VU7CCcsA|<&lJSwyto?1Bu67|hM!P>7bEenfhPFn%aFxO@2XHt*3!c~3k!9u;a zGAGYO%+91W!D;4fTf#7vjmc)Pqyk19c!jRRV}d-IQgAQYkr%L=Tj=gt80A%%j;`5- zIlwnH^RsJI-AwO-X}iz4j3rzhj?OcZRNgQg7G?yWHER06Xo!V8_x77S?8h?9DSpvM9T3q+>)W z6z~;hqsGy?$kIIZ$ELTpr^@uttYeuHa1hFv-lYSH(gQ}-nu;iNkl7#(=mlpJ3Md@> zaB2e+M3=k>2w^`{KJs ATmS$7 literal 0 HcmV?d00001