From 71edada2132205bb5de4fa965c4c65ba1dd6ac68 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 14 Dec 2023 16:34:33 +0100 Subject: [PATCH] Solve various issues --- .../DafnyRuntimeCSharp/Concurrent.cs | 7 +- .../input/Std_Concurrent/Std_Concurrent.go | 2 +- .../output/Std_Concurrent/Std_Concurrent.go | 2 +- .../main/java/Std/Concurrent/AtomicBox.java | 11 +- .../DafnyRuntimeJs/Concurrent.dfy | 188 ++++++++++++++---- .../DafnyRuntimeJs/output/runtime.js | 102 +++++----- .../binaries/DafnyStandardLibraries.doo | Bin 57547 -> 57513 bytes .../src/Shared/Std/Concurrent.dfy | 40 +--- 8 files changed, 221 insertions(+), 131 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeCSharp/Concurrent.cs b/Source/DafnyRuntime/DafnyRuntimeCSharp/Concurrent.cs index b0b2101a14..e81405974b 100644 --- a/Source/DafnyRuntime/DafnyRuntimeCSharp/Concurrent.cs +++ b/Source/DafnyRuntime/DafnyRuntimeCSharp/Concurrent.cs @@ -62,13 +62,12 @@ public class AtomicBox { private T val; private Lock l; - public AtomicBox(T t) { - val = t; + public AtomicBox() { l = new Lock(); } - public void __ctor() { - + public void __ctor(T t) { + val = t; } public void Put(T t) { diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/input/Std_Concurrent/Std_Concurrent.go b/Source/DafnyRuntime/DafnyRuntimeGo/input/Std_Concurrent/Std_Concurrent.go index 2a9f3bbf3a..4fe317dba8 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/input/Std_Concurrent/Std_Concurrent.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo/input/Std_Concurrent/Std_Concurrent.go @@ -188,7 +188,7 @@ func (_this *AtomicBox) ParentTraits_() []*_dafny.TraitID { } var _ _dafny.TraitOffspring = &AtomicBox{} -func (_this *AtomicBox) Ctor__(inv func (interface{}) bool, t interface{}) { +func (_this *AtomicBox) Ctor__(t interface{}) { { _this.mu.Lock() _this.Boxed = t diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/output/Std_Concurrent/Std_Concurrent.go b/Source/DafnyRuntime/DafnyRuntimeGo/output/Std_Concurrent/Std_Concurrent.go index 2a9f3bbf3a..4fe317dba8 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/output/Std_Concurrent/Std_Concurrent.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo/output/Std_Concurrent/Std_Concurrent.go @@ -188,7 +188,7 @@ func (_this *AtomicBox) ParentTraits_() []*_dafny.TraitID { } var _ _dafny.TraitOffspring = &AtomicBox{} -func (_this *AtomicBox) Ctor__(inv func (interface{}) bool, t interface{}) { +func (_this *AtomicBox) Ctor__(t interface{}) { { _this.mu.Lock() _this.Boxed = t diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/Std/Concurrent/AtomicBox.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/Std/Concurrent/AtomicBox.java index 1ee61f07a8..2ec231f4ae 100644 --- a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/Std/Concurrent/AtomicBox.java +++ b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/Std/Concurrent/AtomicBox.java @@ -6,14 +6,15 @@ public class AtomicBox { private volatile T val; - public void __ctor() {} - - public AtomicBox(T t) { + public void __ctor(T t) { val = t; } + + public AtomicBox() { + } - public AtomicBox(dafny.TypeDescriptor td, T t) { - this(t); + public AtomicBox(dafny.TypeDescriptor td) { + this(); } public void Put(T t) { diff --git a/Source/DafnyRuntime/DafnyRuntimeJs/Concurrent.dfy b/Source/DafnyRuntime/DafnyRuntimeJs/Concurrent.dfy index d96f778dbb..735c85be69 100644 --- a/Source/DafnyRuntime/DafnyRuntimeJs/Concurrent.dfy +++ b/Source/DafnyRuntime/DafnyRuntimeJs/Concurrent.dfy @@ -1,66 +1,86 @@ - /** -Dafny-native implementation, possible because JavaScript is single threadded +This module is marked as an extern, but its implementation is also written in Dafny, +in the module InternalGenerateJavaScriptConcurrent. +By not compiling this module, and mapping the Compilename of InternalGenerateJavaScriptConcurrent +to the CompileName of this module, we can let the later implement the behavior of the former. + +The reason for this indirection is to circumvent some of Dafny's rules, +which has the potential to be unsound, +but much less so than an actually external implementation in JavaScript would be. + +The reason we need to circumvent some Dafny rules is to allow us to +add requires and reads clauses to the definitions from Concurrent, which we need to write the implementation. +Adding such clauses inside the module that actually replaces Concurrent is not allowed. */ -module Std.JavaScriptConcurrent replaces Concurrent { +module {:extern} {:compile false} Std.JavaScriptConcurrent replaces Concurrent { - class Lock ... { + class {:extern} MutableMap ... { - constructor() { - isLocked := false; - } + constructor {:extern} {:axiom} (ghost inv: (K, V) -> bool) - method Lock() + ghost predicate Valid() { - // Written this way so that we don't get a warning about - // "requires !isLocked" being an unnecessary precondition. - isLocked := !isLocked; + true } - method Unlock() - { - // Written this way so that we don't get a warning about - // "requires isLocked" being an unnecessary precondition. - isLocked := !isLocked; - } + method {:extern} {:axiom} Keys() returns (keys: set) + + method {:extern} {:axiom} HasKey(k: K) returns (used: bool) + + method {:extern} {:axiom} Values() returns (values: set) + + method {:extern} {:axiom} Items() returns (items: set<(K,V)>) + + method {:extern} {:axiom} Put(k: K, v: V) + + method {:extern} {:axiom} Get(k: K) returns (r: Option) + + method {:extern} {:axiom} Remove(k: K) + + method {:extern} {:axiom} Size() returns (c: nat) } - class AtomicBox ... { + class {:extern} AtomicBox ... { - var boxed: T + constructor {:extern} {:axiom} (ghost inv: T -> bool, t: T) - ghost predicate Valid() - { - this.inv(boxed) - } + ghost predicate Valid() { true } - constructor (ghost inv: T -> bool, t: T) - { - boxed := t; - this.inv := inv; - } + method {:extern} {:axiom} Get() returns (t: T) - method Get() returns (t: T) - { - t := boxed; - } + method {:extern} {:axiom} Put(t: T) - method Put(t: T) - { - boxed := t; - } + } + + class {:extern} Lock ... { + + constructor {:extern} {:axiom} () + + method {:extern} {:axiom} Lock() + + method {:extern} {:axiom} Unlock() } +} + +/** +Dafny-native implementation, used to generate the extern implementation +possible because JavaScript is single threadded +*/ +module {:extern "Std_Concurrent"} Std.InternalGenerateJavaScriptConcurrent { + + import opened Wrappers - class MutableMap ... { + class MutableMap { + ghost const inv: (K, V) -> bool ghost var knownKeys: set ghost var knownValues: set var internal: map - constructor (ghost inv: (K, V) -> bool) + constructor (inv: (K, V) -> bool) ensures Valid() ensures this.inv == inv { @@ -77,39 +97,55 @@ module Std.JavaScriptConcurrent replaces Concurrent { } ghost predicate Valid() + reads this { forall k :: k in internal.Keys ==> inv(k, internal[k]) && Contained() } method Keys() returns (keys: set) + requires Valid() + ensures forall k :: k in keys ==> exists v :: v in knownValues && inv(k,v) { reveal Contained(); keys := internal.Keys; } method HasKey(k: K) returns (used: bool) + requires Valid() + ensures used ==> exists v :: v in knownValues && inv(k,v) { reveal Contained(); used := k in internal.Keys; } method Values() returns (values: set) + requires Valid() + ensures forall v :: v in values ==> exists k :: k in knownKeys && inv(k,v) { reveal Contained(); values := internal.Values; } method Items() returns (items: set<(K,V)>) + requires Valid() + ensures forall t :: t in items ==> inv(t.0, t.1) { items := internal.Items; } method Get(k: K) returns (r: Option) + requires Valid() + ensures r.Some? ==> inv(k, r.value) { r := if k in internal.Keys then Some(internal[k]) else None; } method Put(k: K, v: V) + requires Valid() + requires inv(k, v) + modifies this + ensures Valid() + { internal := internal[k := v]; knownKeys := knownKeys + {k}; @@ -118,6 +154,10 @@ module Std.JavaScriptConcurrent replaces Concurrent { } method Remove(k: K) + requires Valid() + requires exists v :: inv(k,v) + modifies this + ensures Valid() { // only here to mollify the auditor assert exists v :: inv(k,v); @@ -127,6 +167,7 @@ module Std.JavaScriptConcurrent replaces Concurrent { } method Size() returns (c: nat) + requires Valid() { // only here to mollify the auditor reveal Contained(); @@ -136,4 +177,73 @@ module Std.JavaScriptConcurrent replaces Concurrent { } } -} \ No newline at end of file + + class AtomicBox { + + ghost const inv: T -> bool + + var boxed: T + + constructor (inv: T -> bool, t: T) + requires inv(t) + ensures Valid() + ensures this.inv == inv + { + boxed := t; + this.inv := inv; + } + + ghost predicate Valid() + reads this + { + inv(boxed) + } + + method Get() returns (t: T) + requires Valid() + ensures inv(t) + { + t := boxed; + } + + method Put(t: T) + requires inv(t) + modifies this + ensures Valid() + { + boxed := t; + } + + } + + class Lock { + + ghost var isLocked: bool + + constructor() { + isLocked := false; + } + + method Lock() + requires !isLocked + modifies this + ensures isLocked + { + // Written this way so that we don't get a warning about + // "requires !isLocked" being an unnecessary precondition. + isLocked := !isLocked; + } + + method Unlock() + requires isLocked + modifies this + ensures !isLocked + { + // Written this way so that we don't get a warning about + // "requires isLocked" being an unnecessary precondition. + isLocked := !isLocked; + } + + } + +} diff --git a/Source/DafnyRuntime/DafnyRuntimeJs/output/runtime.js b/Source/DafnyRuntime/DafnyRuntimeJs/output/runtime.js index 7ac8b228c0..ae059a2f7a 100644 --- a/Source/DafnyRuntime/DafnyRuntimeJs/output/runtime.js +++ b/Source/DafnyRuntime/DafnyRuntimeJs/output/runtime.js @@ -403,66 +403,19 @@ let Std_Wrappers = (function() { } return $module; })(); // end of module Std_Wrappers -let Std_Concurrent = (function() { - let $module = {}; - - - $module.Lock = class Lock { - constructor () { - this._tname = "Std.JavaScriptConcurrent.Lock"; - } - _parentTraits() { - return []; - } - __ctor() { - let _this = this; - return; - } - __Lock() { - let _this = this; - return; - } - Unlock() { - let _this = this; - return; - } - }; +(function() { + let $module = Std_Concurrent; - $module.AtomicBox = class AtomicBox { - constructor () { - this._tname = "Std.JavaScriptConcurrent.AtomicBox"; - this.boxed = undefined; - } - _parentTraits() { - return []; - } - __ctor(t) { - let _this = this; - (_this).boxed = t; - return; - } - Get() { - let _this = this; - let t = undefined; - t = _this.boxed; - return t; - } - Put(t) { - let _this = this; - (_this).boxed = t; - return; - } - }; $module.MutableMap = class MutableMap { constructor () { - this._tname = "Std.JavaScriptConcurrent.MutableMap"; + this._tname = "Std.InternalGenerateJavaScriptConcurrent.MutableMap"; this.internal = _dafny.Map.Empty; } _parentTraits() { return []; } - __ctor() { + __ctor(inv) { let _this = this; (_this).internal = _dafny.Map.Empty.slice(); return; @@ -514,6 +467,53 @@ let Std_Concurrent = (function() { return c; } }; + + $module.AtomicBox = class AtomicBox { + constructor () { + this._tname = "Std.InternalGenerateJavaScriptConcurrent.AtomicBox"; + this.boxed = undefined; + } + _parentTraits() { + return []; + } + __ctor(inv, t) { + let _this = this; + (_this).boxed = t; + return; + } + Get() { + let _this = this; + let t = undefined; + t = _this.boxed; + return t; + } + Put(t) { + let _this = this; + (_this).boxed = t; + return; + } + }; + + $module.Lock = class Lock { + constructor () { + this._tname = "Std.InternalGenerateJavaScriptConcurrent.Lock"; + } + _parentTraits() { + return []; + } + __ctor() { + let _this = this; + return; + } + __Lock() { + let _this = this; + return; + } + Unlock() { + let _this = this; + return; + } + }; return $module; })(); // end of module Std_Concurrent (function() { diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo index ad4b26df8c956fc3cc0b6570fe39d73cf229f6b2..0ced8600d82eb60e79295bf101beeeb6cb1478cf 100644 GIT binary patch delta 25235 zcmV()K;OU1!2_wm0}N100|XQR000O8O@EOL(GE?2j#rD{7^W-V008rYvFkf{f3~fu zWLX&g?yp$-VUvs@Hvwc6gt<_0HhZgh1oxchVYobbS!gsQn6*F{@&4^kS5?1Mzpa-f z=*)BGzRw;>ukPxq>gww1>gwuHKX1pQU{CXO#IeLdB6jWOle1y}$>a(mJUQEtJqgAm z>(>VYjHAkSwN{erY3IZV=PsiGf77=3f{8lDmlhj-g}0Z?Y_@>{={oY1#~h0;IFQ#D zd7~U129Gi4%{-+{|mx4rmb&MJ_B0t5u-p|uBtLGsUP{%Z06?@l@a3BEHVGhrMyNM9@hetaUag` z?Xv_!&U~~(L7rWYyFz8{e@>^}>(GiI9VPqYJh0&KK$P?fzDVN$t|4Rzhm9Z3r<2R! zK+wmawybJx9Ac-e-#zd4hxxTr{3bo0Iz>X-hl5|7!c6eSDca4Q0wFeDN%kR7^t_vS zH7DnR(mfOhqy6~D$GbcJqN*kbTr+XL0i`r=COtTY+R?@j(1t^;e@hgz?9xFu?`|et z+4&s?-^3CS^BT6$fa+`^0$8j}CMZA~i@pQ+Z{{Ko{A|C_?`Tnc>+_^E|NfSU`Jkb?Iu!{O8(rhZXM-ck9aznBOPeGNJOqeDT|M}1Ws$Ezb z_W(SLqhBr5H+k-Gf5bIqxc}&DN=!nAxVhh|ND6Z>QYX0h0`12L`ov-i4kIi7<|%c9cq>^9+SKajzL^t5|1%F%cTak+?-)i^i%e$y3=@)OqS{mx9-{oQlX*=cWqn^Dq z!=@BB{<~}vU^p|;1`(Qu%Csob$c2pdxHH3?oKdSK_ZP@+Ow=FOeYnmCRG&2v_hSRW zVaG7Ax?*M5#AhU>d4u`l+1## z`ty{J*-QKn2$cATR)6?WZ3ww+vrdBp4Nz?s!#X1d;2HKU{@^;F5OS9tyVMwftnZVg z@hlRdUUu~H&Bs~NKZDRIX?t{V#&*R*9Pynq+B56wM2@QhTz;D230=J}+GRv1jm@T+@YnM0Z32jF&q{#0J28 ztI+1Qiu6D$S|v@Cy9=Vus7A*wSC~*qD7wgYf5JQ$hUNYN!ZU(AcygVm84MJBZk%`F z1#NmYgFB|cmG{PE%k5o0gk=BbaSd}&GR*d-(}|Gc9sq_O#7+uIUS{tBYrHlpi zf0i`t?P%hWFDW2r2@o9NN26KBi5lbwF_M_f#e_!FP+xk_D~P1ye$!qyZ^T+2Ut6q` z_@Pm-S1zt4LZanXD*@#ZCO&P-gAOeZW@ybA86bgvYsyOr9)6e3d{t*~$OAvcjtmu# z#H`0cZzBQdc9=N{v1-$4C0DELg3f85i*aC2B6#PbX(*7kL-) zK2mtUWkJQ}i1=-U0=S;z5CIo!oJ_CRa7bE#HVMs8hOm$}1tLhuZkA2@LyHgxfAx4hU2t5-4#p92O%26{x>t{V2L@* zAvGU7{01C`w^_zwR1a~b$l9;F)2?VW9rjrz;2)iA_dj%}MFf;Qv?zg+M<*uU=_&A7a6cPnIXr9`jG5~To4yZ+ z%5p?D%`e3Zq2Tf3F)KXopXj$zzTOF%ZI0mO*XJpsBqSEF4XJX7$`R@$J-i<0-K#d_ zwn6B69{*>UerdpocGiYJ#eeKYlg3OM`9_o%EZcZq{25)(QlWDjANz9GG<7chpPz|jqm4eYq;B!mO5a5g0gI}BpLAy9T9bT#S7NeB3#d!1> z#}1i%zBzVthNE*PvjJQaTzs0Fco98LzdCKz9w`7rmc&J{?pUoC)`+Q72m`*8*EuP)Ad z=~VSF#$N@UoDIhpnGY5p_Yiu6N`UkhGQ;^G2xtL8L2ai-L4TkjcaU*3MxSjQ#F`AN zmV?2mw$5iIWK2+H8)v8xhO`4sCAl4R|fRar)o6pi9n=P58WrCwi z!-{|V9YEli0uLt}KJ#XUe1PFIjY;pL08Ozp9&oK$pjsSqsfL+2E-wf2iZm*h$=47|te^PZIkP%G zNxp4GiIA*`5+Q{xN`z{!1g|O)_DESjIT4*oM9`2$X&~v3k|0~#GohRUOM3V(j{j;1 zfAdN?ZGYr96X`~ZS?TDH(6m{5eqkRcZ}Z`ZR+>y~c_=!v#-{yOv9mtwPAhJpUQb1{ zX$~Hjke60#-ghr2)AJ9*?CjkeITF&)?5P@+tj+VmO5D_h&z%BGRI{?-n4cO4<}DOG zaXVC}ajMp~6Kq?pThRjKO8_DJmkGJg&L6@>Hh-N82G}5lJtACtF#-WV@0-s&_tM4ayy|3a04-lF$~@m`?@(C4=!lV=h?R)0`B(nJYTW) zpHR}VccfKzp#qGz4J~cbsoz8kao%xvyT~wmUy9_J@%BIJp^kEK#eE6WX6p-dHWE`; z41ZVitixGckDn_BOhJap-Lo4+0e&`!DykmP2R>F^m9G_5M@KO8| zyu~N0YP`^IBYvsp%-~P?xQ6)Z%D?hN3p~Hys>NO0w!aT8R9J9j>-I;PV;HYOIcxvN zOnLucEWfHIM{nNlwKRa|yDtv+WbBS;uz#C3NUoQ1?ML;N{kLN9&(ASg>0Z|Fo~NCS zMt?F$NiyMdqq70KOXm;)o$DG&4@d*fhTk4N?`%B%kis20gxPHWn&t=7#=WPLi_u`b zltV@nQJ#pJ%bksTX4gYb>woV3_q(IrColHibvD2O{1&mXeDiJQx3%axn!M_Y%70+P zZw4D4s!co5XiuIS(F_xItOqBRb}Wl(+O5p7<->Pz21gIwtKsDA8&CKcLJF~_L@TiQ zpo;jO?;yqiY{F_wf%yPy{KkU^Ya3$R^#qcyhrFJAX|UOmKy4u)niC~CwF}?Md^=7_ z1d#Jgh#*j-JEh1YdEh{=-dnZk)_;UAaO@0I)}&pM$%#W_woJWnor49KNeOEN9#JMd zq&AefsYTsmY>8(9OTYiVWLRW97y{-zErX4c7KniTFgRgQE@Xp&n#**;1skM3ZGhI+Vc#SEYnX@S zk5-{v{MRji2;~pm;?4@z?|Ah)ofZ7B;(x%NJ8S-j4eZ)2clOH+AP$Bmm0g@#Dd)Qx zV>Z64Cu%6d9AD)e*B$%Mjemz*cX(?vmjaK;F*ByRp-Ob+Sr)#Tl zbS)R3hidH+YoYSEs#UZp^d5uO z%}v#rsN^lCx<$?Y?B(^@{;&H-hcH>ZBX4V2RrO!)zj}++mzK2}dVlCFy23tcfGZ!o z;^LoHGA1{DbSNPomo<)*U@VLkt#xBPh_r+$Esmk>@5gO8i2bD@kd*I2FONyg$G+@I zf0ZSB`cR=TZsJ+mhpZ7c?*EeT@Yq4nesR`H=yUf?;KaTG?; z;CPsRZollF!^;g)aSZr5gjmuAes~R4jGJcDpq)2c>Pzep#6ne_g~T!C0Z23AR|z?P zpo<5Y<8{YAjQE&IhmSgjkm9~3#GU!=9cjgyGR{AIHsLhD@3Ina7d)-NE8sjGwm?SDW+y~MtH(3F>-LkpgE;7u5S#=d&c)He<-bQ*#yFaR?jJy`NnU^;2{ zwh{vA=B^z2R~g9>_U z>ter!P^;jdCUVk*M&nvf5QAAxd-Uo2^L_9#1 z;syhI^6CMD(U3v1`E^L1{<&)ZT(f_!+dm)JKR4{3KifYa+CLxJKfCtNp8d0L{~Xvq zQ~T$s{d3p;`NaPD)c*O*{<&xWe9nHJINS{fKbrmGio6Xg3LSBf&2)`pFQ0Usva_Y>nUV z9Xy8wf8!ipH$NRszKCCM(r*8QfQp}VO;{5fDgMHgSQxw9+Y~hA@8Cz1SKb|8TlL>% zpIM;0*UsMds@oZ6mnzMnrXml&D<3JDdMqIvS|mZPu}F=3yaJ$xHSXCU0vv8SKy;Oa zwtx5<)Mj!I-VDp993&qT4u{H7fV+ZU!f?vP6c{9vQ%SLf7#~XxMHZc1P|~)%E2c;n zp2X{lg2^~d1~4gXP+Sl!jMRrje6gBvVc{+I$LAN&8D1Y9OyK_aBu`F3`W| zdQE!jXfk=xoxV>SLrMiNN=ZAwhY9SNxDLDp#lkV-$WImL9bN!@Q#b zg*SImP@x5LC$wJ6%>=viv-k4#(SQE~(+74Cg2m*aJVtl7^tK+neez=Ozuq1k?fLbV ze!pif?U**N_ulLuJPTBBhiZr5rlE>Y4_+L+3RK<W)ACqJnTuoCAinu79nT#QWH+q$43`5Lo2~A{(32hmOznI_36kzu2NAE{zIY)6 z4rvcO=GWOS_>WQehq>qm5q}XDtem%)MggY*SQt-X0XyYQx>3Zk8064+T#QD6u{L81 z(Yb;_QE8b>irYiH2*rs|e24;MK;YgcAjkZMAU<9q{=@F%#V|r}v&yf+B`&`gX93W< zPaW=f_fpDV43Jm_gM5?6M=MKBn5zxy53hn>%8;77+nhD7Gq8$3u7AMkgbUZlK5ZK% zdWhML=wF|k==T@D4D)fCWv@63_MTJqHxS0amnMY!D|q0-SS$CHPEykL7Zg)8DE{|v?`kR(~|bz zoc3>=_9GeR8HaEj!hb-lg$@pdFit{PSTOL2E)HN>ji#Q51{f~31`?b{RsbY_-!A}+ zhL{1|!?n}{t(RDvM9+A$_7mnV6|Yi&jL7<}xObkp~efr3l z9s%WFa+f^%yniW|q*kKhbLcju7PgdS*Z{YC{YvhJTQ4u&Im$4BwCeKz1t#X@3!oAX){~W=e4?CTb|sY%HCW zcBIXwT#8sbin~$D5Ru%$C>&iR{@$^nE4iWzhMS~fno=KtbxZ-;+CxMR@{h(lWNyEi zyUC(BbR$(1`!`4R0DzOhT3~1dg1(5uqVV#bd}~7DuB}{arlQ*rU5236$Ulf%g}`-W z2tXqvRDZt|PWKm5pu_jYh@KBFav?WjMGE*<6h5*}`&B9y3D_e(PL6&%cy}cJ@1J|` z)>aXI{2DepsL+|=K8At>dlV@FHxucHhNjhb&rY4O$^7Jv|o3# zj50pxPy`cTK-j6@%$RQ31JKKwCWxO^Q}LN9w10Eb#;j!lK8Q(UUgo695FP8WV6Jo# zTh0yY>)1qSR*MqM?syIq2GzdwJt}0cfJnx# z3W0Q#H2@Th1TYZXXCj{!A7yJ68IDU!iC1(>KC+=#AB!}Iblj>y7)C^za3nh(Gqs{H zS+!8SD7K@3(Li2?Pj;>!cton{B>T~W#((xFxGNGCP>c3Q&J@SZamZ!@R`4#hF2feh za7g8+OPbqW6e5!^RXH9z`RTH~;>S*k(hlRFLdW#oB4WZJm4cMuKBF;^3)!#gRJCE3RDPZ)G_t8w-q4kX34SM0S+=5UoYjS>E-1K*41JvlYeP6 z;f&Ddl4zp%!UFs~A$s|8*A*f#7Yl?)w6KMUn@aI$RwhX1u^g8Al@h`)2VzMt*;Ra4 zPGo)$EkBoHA-01Q&ED0bfm}MGc7R**eIp{TWz$ZsoMv$%5jQ%P(Tj%S%;d@(BZgKx zh_Z;*fA1a5NG-IC<}>lrS4v8)SbyEJI9xxHRy9Xk-gf|0ipEti78s7JKrSdA*HF2T zfLsM`ArZL>ScQ<>LIJR2aB)58j(9XZ>(dfGQO$I!vrraC*}|G$Bd&M8pxkIY*Y}HX zEs9UZov3wW9y*slGHwGpC)?JyIUhQo)>a`sV#ZUl-9Rjfx7*XrNc&^E%zp~0xJd$= z#Nh7OOS4G(J{g7pIkhM>uW8*vwd5^3%<+K)6+rRN^vc>|z@4N%7?hAwUtUQ9RZOm( z55sf$^!z@giic_6r>lLCIbSE+Pdcj)Ti6vdrqRsaJ$$;qFRz<5SOs~}7a6ggtn+KW z@{>XezQa}E2V3^{7nAo52!EW_$U{X{hz*(?Y9ilJpS<7C@C{(GQ1Irejhm#x=}iKL zBXS$Myqpa6yl0BwzYsYD(MjvV4iZ$i+{=>fBK+hfvGq7U11*{Dh(>mc7AX z>$Z`Fhe8zYp(Lo5_kR=btCN=qojeEQ(KS|7{v6At1VB&_##2 zm>?JYogEKPEUj&?6+z(mIRaSf1chm|59>{xp`Aj-Nt2>pzz_?SzVv`|5M5~DWehIz zlXK0)a7x7;Zm^$`)hWI^x*8Ja$Dv7IO*8 ze3|AhG0zv~2(=PfhAKI>Kx9MSsblF_wWK&j5qDsu#aC4=zl!5f3Cz4t>2<`Ng2x=< z6WZU7M+I6rGj0=cy|gmE85@2w95=G`d{ZTcVsG49xa~xdg$x$*={z^Ru)^xt&pLok z#Njl{(JhEi@PDmP!U_hgV><}3K64L>`G(CE5fXb$A;fq>-GJ?JF8&LRinESdjtkdg z5g4hn;b1UIH6j-CTle6B8wkl3pdlpN4af#10-r25hA4pP){LpxuQ;T#UuU?#-79xa zI9`dFX%YZqG{GmJ358VrD5U4OfS!{OJ#MnYFdRqo$b-fsuC zxwN-`dNIx1dt`Orcy|~J`}v}@XfLirg%{}+1kz&-9wSU4)L;zq2|I+9~;yh|1bjLZY)GXJ(WgdyDJa!f;H!wk6KVvT_=ojh}@jDsRtr*GkOyTfOx?;|=HocIDzje$c))7m0 z3+~p!|C#s(CIA*h1Mtbg^Ge{fu+ev%){iOb?0-AnH#`tpoceBH9K;(X*8bI?bNCE{ zrZ-QOZwmc=pY5-ApUsvGi_CK>iq18)6reE6A8PV*X@9e`6PO9_V6~+=lWF6;m%b-| zCq&eo3&SioKhyC*{jilX9q-W$r*I;4nc$6p^u6AuZWBQE8!nuhUm=GrvI)V%d`z=Y)!4uQZID-%xwtg$a2gqfucT~z;pkdAR8WTf;>eA8V#r@G6Ik5UQK9P_GCFJ?FPt^T3#ZcfwBgM zEuL@6tqnbBR%tF|=X`%aFRklE3RC3iq=v5g6R6!aE8h-+^4VPnoEwvvh#jfon|A`wzrLm4g=#+&%KtnG`i2+aT( zw9j(l>30oyW{?i1bml?y2iMJFLF6|GZ6-pB03Y7hA{~M~;IZ~E4Y7o7TK0;ff*FbT zaV6FV8^%Bka%?xZfNrWwr*R_fQiGVYte_o)xD=W}2!vQtMx$l=)}xX-n17d67fqL9 zLeQt#OsF*dgz9a|wzicdYKrmXIK{oWEp~9I0IYP_%N+%QC%@KwSi!8I3I~p?8JZW9 z$tT!E<`BSvJGH9zs4iup7po68Je!kL)*dag7IND%Y(rzGh$R;4?;#4zsDB!s!x@(z z?}qV$R3yNWxp8pk<zBYzg4?HpHd=3_8*c660?*nBja-d;wfg{@Yr`^h-0z2A;A zm;TZPo0S%9JC`*d%F$bnq4#T=i(R#H<-pjSYx78M#NSk0_eIOL^!L+>3k7(VR++WI zIi#)xIR1rZcxKUg1Ik<{vY_tbi7hPhK)Ol=0JP6cxRb z`U6z%mtb|MQ*_{1J_)y;o7S@n8FN;W#6v4IRX73x_b>EKvTOiHB^TqhbDlhf>& z`fs;SBp?$n7PYA8QhyNPz3nnLEO{2H?z<7^7-M6Er=ih0(TOUyK%+DHLWh&YLB>zT z6ayS(AN#IMl zrT$4_MakbkZOHHqJWHbMqPNKlF=5Xe%%W=E5_fKHlDkev3x8qQZy$!E^tDd{1M!0GtNlXL3Hm~ntzxKtR)yRUV`Ndtup+%#lC~_sy>Rp)u%52 zTQ#O#6$%p8lNx$SlP>5Q3t+>pU=9FqLxXm#!6gU*RF&G+aLoyeGe()*KDYRr zfQCczFQJ^>pnvLVnqN%E>g0f!AU!9>OSaU~Y}C&^MdTUJ@E`BC5~1X?90Iyn3B=28 zCc6tY2P>@hmE>2&Qm5wv@0PUe6a

5xt)0*89GJ6;);q#W)xDsIJ7?#-^{k(|p(+ zH8MLJV^CEyOYz{j5m{?q1!fkG2#yX6NYz##N=7~@Y zeZvKm->;i^f1F;Z`xclqTIZ{HuQQmL zTdaZ?V-5dL&wrPtr7i12kqSp>mO7{7|7ctn#aB^Sm#l$zy1tS!j|X!VCkkgV1K5L( zJyUs`qzv4!0m9gp8^&9es7i(|(4uiygJ_7qOr*^6j@8obbZOh!&c4%n7<_;eQ-%@@B`iscUIaSuxu#zY$(F?QEhC9G-e?~P4$KRv8-FpWuL<~ckxq@yC@89lS)7?B)SYs;aBO8F&jGFIr=ih%;Xn6A-9;T>Yim0?2QLDg4Wo` z*kIAW8h`sJEkzRK(4qy&CTBKTGO+i?gD8KZy!;kYK`M;2+Up6yIlfIVAmv3SpK}(>nSN55m2*P$?`t_=kj7fe<`wPP}4Epeqx|)EiqE zShm#A_*wCN3Yh6Z4$tY>Vm7R{oR%Zn$_jQ#3=4qWOn91V=4WBJKy_Q0TM5KR z=GT4b-Q0uF2sfl#V5-Ak%e642O%#Zk+@R`Gz-8!80LF2t<- zBw2?0%Fts-kVLepOk#`#sLtwPkg|*t)gj6Y4*|M`5a22i&bAa*J4XykV=uFiLVuQG z?6WxmD-415kySeob|*c^5~bPb5KAW*r1XN`k(A~dTp`F}Hx)CyIv{U6aIs2fk(G}hHc}=;Xe*2mr7%}fO9coO zhbnP&e`)k9$=UzEqV*OWxn?rS^Mf(c=@p{a3ggzK>^z;EUmud9YgA{zmmd;XHL-ti zCo_=`rOYU?T7R1k^K_xtfZdzDLWvE>?A-$V-4L4QayWq;vG}`{=m2u(GNiGC#@)Qi zoLdP^In`a81u$Q_FUtot##4ARaAA|bq8gnSk`q~A zOHWH~gs5gP-iaE}ErrV^lNh5$2wyhk-)ax|C6i{OF&kkO-j1^_B$mw60alX_liuA< z-tNCTT3dbha+9*7D1R5LvZ$MY+HrSohl-`UgTdRi)kfEhagUjjY`e^6Ko=$=qi|WK zQ_=F=71~Kh5pxB?MvNindeZ}{ajIp!qJ{aTZOIMVnnGc+`;Qg@Bd$>xkUEN2in_~M z0^Q=hH|0!fYf2+Q%145$=w6l+>i_O2E~uhv<|=n&^4J@=JAW^~ia!Doou^|~IHRhs zXj1d>a=*>J0?;6oEdo@_T?ce&Xs%frn`+t-Uy@r#6UxxjlsnjrruahGq$3u=Weg7) zIOV{TY6++oPI%lbF4Vk7-F(iy#h%>1$0GT#3H7gKz8oeeg52o%=C6gKOsoJ z;kAer?fztssej{Fu_ozy2uQ4tofVmJkk^+_xM0Gl8~ZU9=K-1U`!OmHo%4Q7D7TpX zmW;{I72?YOn@%Ud!uIa#{ou)_eoh9{WAP-+YB>mHCDN%;oD;Y33zu!rrv7u z14j8-zhu)sO0ROL#BZ=tln9BjuDUxKP5M5nwseOuW`7dz;cN#gDsgV>6nOEvs+JOT zi(*YMi8>>fGacnRNUMwy0zMpZdpZ}Xl)Y*1(ZC{xEFdE z*MZTdIQ4b=AZv$XfQI>kN^dD2Wkgn)nOj^C#PshQ-#M>>v;#St(Y*lR|_oh;_T z=oAG_Pk#fLD=<>w2dJ&o<~G_NJ%Mt0WyDaat;`@VW;K6FM&T`Y^L~bKOpgs|*~Wb# zHR<8?IPYGyoh;{uIjoR(yD&e4%*s}zw|Kvyh&WslDV|ACp-ye^=z{zs7=wTer9?5! zu<`e6n!C{p@{udRN4;%@;m~-rD2EmwZryQLzJJmiE!JshOQY`JU+d#FpMKT`{8B67 zzDhynT$y(X`|Z$+%CM3e$j2%@8te=PK9*L^zPi5;UjDv+52Q~SzElo^Kr#Wpk<1;y z+pyYBz5t#FO^4dk+t^LTCgM`ixsQp+1*f#xVTV-r3?k)69Kyp7A zj(^;*5?EasipMKF$_VgKb~MkOg+4|N_nnww;-4O)ts+sb{_GXLd}TkKjJEP*&PN__=@B3wS1%&SlmRH2q*$e zz(pO=x2&*i@W*q+YyQTG{XINxD?#W8potK|yG>{0z9mP~YX+=Pd-3Oo zCg=H11vM7us8(X4wfTyPfOE%X@AdAR-J^py@>(%GquMghsIrQ3QF=O>WbnRaAO6*GsJNMx zH3E$e&cP+{5fBeI3CWmx@{P-y==sPgw_>i;x?#0xV;W{$C!WH8(}2=sPuueOL4VCM zClcyuI+AoDzel<#*fI8E9<>#p$IjQCI1;dGb!EbZDrmS?E{s{o z=<&9mFscjNdP1)S+fSBa0rXb=Z77OwC9+V!7e*KMTa7T(z4a;6LI<70<(MoGj6T7M z7_wQ#7{aOa2%ph^pb9~O6P5a;0(>aMvK`wrHWS8I;QArK$0~}gm~Ume=%#n-yQYY_S)pGH^=oZISRa{Nhn)?$wH;t-)Z-Nz}l?k*=3|R{e4fU)$j#$p$ zbQdF=H!Tk%^(yTXH7@s)V+HU8=L9!H)JwAVn>ul|wM2T0py(#nGp`cl*Ui&O|04TV z9kyId_?A*39@$yy&+2{q64dI`OC8UFQYl8W;uJR_7|f9A5GO_|g;IziTcj2bY{OcP7XGF{4gPnk;vJo^ROUkED$jniXgnr*?JFgO|jCaWSrSL1A zhn8*)%xtLpdMXUVX+BId?kRfrVmMB_Qw6AH>FAIJ7o3cq|4D<37=d1cvToV@_Ihzv zmNKlrdBWwGp0gMS&N^1lI0&v=x(QtI4GesZ3wE9}1DiM!YmIv?UiB1({pwmSBy_P65T1=<(A=w|t!V@G8CiGS~i z{&G8_uv2%*cy+(~?x%po2&yuZEANVEOH_L|BnN%o?T~8}hm`Zewj70>*>*ZEVy5+f z9Ohkhbmr#Q-=^FDF4N6lT1WT(MfNj8NE{(i#s)k? zt%Dj_8nsw3e;>1u&(l4Nnahl9vLhyk&gesVeaD0K4d` z=6jh{lZtg+4x)R+Y%XJH?%(1qYbt)PZFO&k)pUMW1{YKY z)O8`w2+>A#CUCJZh4ef!K59*f;vo&%t;jdm7!AYIt?u$AE;fn3@j{O`T#qW{=leL}`7a;LDO_lvgcU2C>H6OP~$q zFTVU$B<8Qb^i>~wZ`tz%xzdssZxx;$vn+LN2kR|$aB48eBKP;&_V?QM=ULmnIi7lU zFjl^9MbAx(B{V!Gg5Jx2a#1G&dTKKbGz2aP;KIt5)Fp=m-M->>-CSDGE#)dLwMuu| z%_n#vT$|stNj}Fy?;+dW@ipFwAa&X@ARuIHr3p`qPJLe(>UO+wA+z$k9$5PtVFRnW zcQx#k?#_g*1;7^Lc$RzXxif>Ty0YS=y65G^Iqq$=bPs%HL1MpuKsUkD>>2y@&oV*~ z7eS$Yu)*V(Vh0AZ_#;hx^NiOT3w(xlOu~XLG?rW-!OMA@%jD1Ue4_}#k@^Ev9E$gN zbIYg>b*rOjIk$HRhp#cgy=+J>G6luFaqnCCXw0Jy!6&vW%uJ2sd0>wE%ERbWy7U-g z5}8IuF`qMC7*xD}mfn@2{Y|MX*~TZd@9`BL-4wpEZYR3F`u0fgT=43g_kHT@Y@7<- zasE{svW`XKpwCa?S&UOyY^fe*ra1LuoltUhdC1Y|N$S-oSC>h}fFoi2eEkY?TFd*X z_HklB#Ht z%WR}cAg5536`7`}vvRO3xivKzWqPWRz=5Zeno~9X$4EjX2~0~S1me@UFSBpS6My*y zQmEr|s9y_SSCv{|()$RrcnP%trQ^-oGA%D4$99+)oJ1R{OXyc+0We8?RWyRie-m&? zp!J-L->_voFxw<7d^a>iszQca$N z@p}r0G{mx8bTXB7vjXuh^Q>dNe>tJ5nO*SkrG7fBuq*$9%*_1+ZbFjc4D?P*xlZao zXEzM+>~OhA#Mwe!@kE8DQPHqD?c4*fa85~ktiqz6mrHs-%Z;Qzg(O*BvCOyCUx?(< zo40#Gna6bQ0>Ug35B;Bl=5gM9hR(JM=S2NpXPgmkN8fWk=)M;_8_>E2f3S;!DqyiU zmKFjMBw$gnP8Z71nzC`Kfd_86M0>-xQTpx$$M_BXC3t(MpT(mC0?RJ6()gd%pYP@b>kZdafRO`&+U7Z&qw50)K0^zcpJ_vyB&{*>6+dgCi=%eTIC^o8ZBG7o{>ny*SDRoI>oi8!kymW%OLMNS!Pzn<@FwxfF- zAG003bIw9{BEI7l&v$%2#n^?$xf3OZuLy}ko+%-axdqpbaRh>ne=-uCz-NR>$`yVo z7+%hNWac?M`fxh-9pm;%hV&V~Glvm4deJJ)iAJ9>a(U42l{sy23}tTcJnq{*Y8Rmz{8 z>EreC9NOPS8frcUe_~66oJbK_ps!CRgKKt}ug0Bzv13pfV^MWXb_bW;ai5~r%)?lU z`}}pL7wHwe{A&5_0jU;45bGSmi}R%qU@@xf#3@<7drq;;r(Ln&v7oNNBUwp4N$6E4 zy)gbc-nfc$OA<)dC?8rsuneQSuj#=C{-Bq!a>OP_T@6uZe=zD&)Lq3%ZZFAKveb;J z@>&+ZBBOU!rqka|r@SLJj0zDCPNcpy?7kru_&pM<<4S=*W`;&1F0k7uxPYJ$$ z|4UUd?^?+MfBmGDsyPjI6R@TKC0T@cY4Fp}fk(m?7Hzp0v*E>4T?@5IJkCR{A5Qg< zeOCYFsett&jl9Tu^=$Zlh+)k|4?zyFQtgKzLkm*_J9M9349_1Gog2r|n>S)JbBn5h zHeVVY9zlXxfn+SP<+M_&kA)GcKrE;&_f^4NW5u13e_#_lin{L`pg|T5BkwlJfPS$v zUs|!8aJRxvZ){6mzJY(bqnE?+MVYXkL7jPJb^o-1xAMp-xomQ9RFPYS?cwl!@Vy>} zY$mGQ7Os$piOTNR!~bYHJUc^$SzDlPYt98pUGd4PG9%f1$+#VLrj$md{#x)SmG>nzR;w$7lARN;xEeBW!YQXy0(B4(yj!g zuq9y2y8%eGWQr#?yRsH91YKPpRe5!byQ3qk1>aFf-!!oy$MJ)I5V0KbqE`T}!mnL; zf5%Z09;_~yp!BNreT&$cmPARX?8HJuPZt@ctEYa5?e=%1f$_2gtvZM)=?T5ZAfdQb zY*?Be5~>0?b_ETkfCW;x3Sc@l9H6Cq;}FYVo3eP<@_5j4D4Yj+KxA6Q>}t8ZSaA1c z65A?be9Pf`L86yxXG_*;RoT;1`T(xdfA*4V>bcx9F%^bP<`#_F^jMx(fe9>;%v4wN zP+B^uyhROM8%gri^=_exAseGGX{1cBb=6%K0bPWQ;!9G5!}SB)_H!NL;2D;@SvyTn zhhs5rC2ug})4Ru^r+4YfJA6JdpKXUG&ov!-kC_iU3#KT(YNax0F67x})jMAPe?J|& zd+?yws(d)Dmyg9*Ax@#O@P|Q-K!xLLnZOT#{1H4WdroJ`L@ z470O$Z&Ws@Shotk(ZHoZE5p*!e;xLVrd1iTRoEhgHoxg(;V{c?UR^PoW#*A!ey6M= z>~2xeK3=vGrRXHQb)R+g=OEg|(SVL%j)QHkmmMuZkq9%W?61Wt`&&$9Kb?#w)gIXH zL(T7f2DLfE5!AoaYZT3*eeNgYjigg2IC~jQf?2tVa8ct@eU+Cw?H#S^f7X}yPnD0V z_%wlDLk&O8_zufu5DV-je8seUTk1U|Q@AZv3=$ONlHKsfB^vUV)pnv9hT4l>&ae}e z2X3DtugogMG%K~~k3CX?f%W!HjL5)?!XDBs z524xnt2CZ1m)e#^>^wWMf6&@(@5E*|mbL5`+slOu`mGq#Fxx+s+?oAUnuSYOta52G zo@on4n~ilK$(B0o7Zn3Zw4{Dz=?6V$zwa)_zPYR)t8)Kox)9 z7jOf6UHf?*;}~5X|m* z>4#z$Q{-(5;;K8axD<64qo|B3uIl(-8eZ|*5Wv!D8CYmy2r^YfdF9AtFTu3hGG<1P z#Pt)#pZj(r@bZ&fp2Ql#Owmu5RpX5-ISjP%7~Bpl%4=YoAZ_ z3q4DZ!Aw@c1B&IMiOus<7;}Kc6KO?j>w3rS_KBN|3)<3%z<7L_4rRbK=GOYCOed9` zi@vwtjw3361{NPkfg2`0nz`+P=Jo=Cglw(PLcjBRY)D5i>4hxSanu)Ds zkY-|2!5GE(I>Oh-0)Kp^H`pXg#YhfM;YJI9ve-6)r^Gnhpa9vXUPE}ijjiO3pyI|* zQLtOX2=cwGy>2bXZ891(ybnGg8K_8rgnIeV9luYh<*kgiQ+hCvfYqRRhG?qQkaETQJJCom)e18&(sykpT{Y5b~)sc~; zn!BxG?24QSs|_0n=+$;FJ%xRtE@Fn|M>^{k|8!4TGkc6ERewW6YPOF)q+`*Ox#so} zV>7-?n@v_5K}MNaAt&ACroKoi^HJKYo|m<<7iws35?;2Fb`ioL%A#@!Wh~D9_cU+;#|XIZ3>E z8PBP1nCJ3a0nZ~n&Bt?QM~8TBJ};E#DlK9=1h||e-ekOt=TtY$bNQ`+=aHV~u+P$8~eezTRsQZ|H}HnarN3<`QeiKBLr<>5;7<9fn%~6 zjFZ)q*1jS^ce2L9n^wiOznWUK*2!BV?Ryz7f0nViU8XL^+HkhOB~F>Kx`x)#OPnbwWQA}CqNO!{HV zULf+qwfg?nkAG?Xczp7wRffkWvueIr%kP7DNe}Un`s?V@xwYbgl;SPuw^{c2f9t@% zj1KfQSv3tflWlpMCgJhPBKTiQ!uPZ+7r?H05cu1~`SX|;cDn@#2ATvm)Onna-hYA- zJNT{Oh%9!<&3P)!gwi<`M$t2;!W0hB2?RS`#5}lLtl=s&Ec85eYP+|Uf2hMdT4Nmr z9Fqc*xsM)HzpK1oV$2#9SsKBQiU|0`X@u7Nh=H{Vjn|;{ccs~2c)Q)YuE5m_+*oDY zxFu1mLjHm=SU4*?3x>F8dOdW@M?=2D^jt;lH1|mU=?|HIP?*M#kCT`wbitRdS8k}1 zXOJyIg8nitzsR9Xb*#VtA=a&NbY@l*OWEpokTUNOt>RhR{FA4^9|2pF$G{~^&QB#n zwaU%j!h5~u%5CgEui3!NdzZK9vTX>D3YTnWyvJH?g8YTaYJHgqDvs764-K*i` z>>Gd3%vw$N&(25QeZe5Jw0PgvBrX%v(9|}3LiCVJ_`v{}i%SRGB88NMgF1-`=OEeFR)(G({39wmy?si!byMc zUJS=+cWOEbLD^!;ndZ{@G#v~Dj8rGWg8Ir_A{Wr(qaDbBAafspxhE&qk(g4MsJ@vT zCCfXMWU&RQZAM~d$?8WfHNTQ&QHTC^XCgt}gv!wg2{n@8nEE%uFFG^X{4NO)N{f2x z8){e|Y}sLQ1Ee&DQuS5l(d~1`7~g+VDJfEfZnC%nYDpQ4(a}`A$Ot>aNOj5B6w$fG zJ}lPjci>Br{thvqko5T$PzE-T$D`A7#r9N=SVfJk47VbpKy%|CN^b{f^pZci67_X6 zpAO%@Pp4HRs6vlSpuV}{>NE%GU3jP5a{Uw0s$K1RL%wJXJg2@Ka0{y~_v?TBYQsJu zFbN^4B0l8IJEn(Ac{tXX6N=ivonZRsYC@q z&qPG5fp%zEMz&v3^}T39X6b+15La&UhkL(u0%4a|hY&t}PzO|pIU~XrDx@pj{g3T# zQT`0$a$$BWI=UC&M396DYlkRB2ZHEs5%y=X_hxQ0H0U@8i=RJ=Tb=|IxeKiED0UV= zRjRdcR{^rJ)KP%7Zplrs&pgH@2+ZdqKp5OXpgecZ{d~uf8F%EG?5KZnFC`30C6BA` z2)koq6ighjIR#K&De+0cbG+%nzKs`b<-}Rp#AHr}0B zN1fwOs4U-H2%MEtia@Ay$-dWFK{-x=z$XFIAj=){g&gV?kJ z$Z$z#d+pQYtes)P{ zCEE$~DeR^6@Oqqgui8-RR5DwFaCP&YH4Hz*9Djz#dF(Pb{fvE$Mkxws))pmxwY}+d z5^B!gaCUnHW||kAVa&6(EcL7Z$E}IaI@=FxyzJ&5aFaF1BNS^6;8xNPb$}SO@SmQj z(ro&$x>u8I#~6RYaa;BnNXXfP^(GzR6C3nolY2({COsXcS7OpVK5E<@izR)hF_jI3 zt~+WaM@>9-oJ>aE!Ri$|K~;?!SFPkKdLq0(oi3=qyVW{8ygn0qtm&{nOLwj0Izr)f zQ&`sUT#G8ZE<$2g*a)|Wh&;GY9AqFfwl)&3KzmE@=Q zBn!)7GJZe0ULba}qH;9tjDu*U!9ji4otu|Xg9^O@-giv9v9sX@W(X}aJM2q6~jy(sz+84mu&-6d!h(>jIkZu;A$uVPL!gT3>p|T z@gtl)X9@*vR@{jH;RmA+SU(MHS!mW|!t5NLbw_`t7@kqR7>@FD36}r(hlSpi2HT7f zAU_wA@T=H(iv3nOm*2~ZF(TCWnRtC=;1{vGdsU6yR4>YI`dp9QvJu)?Q5s~WxK0&2 zu5|F^x|9Or@AcyvTjr=#dVA5?8^elx(N}PU+I02_UpEKCtlJxz7#u9 z0jJ&TW@#%KgZrRkwUdpIDe;{-8}8wKlzRc_By3`yihq6R$Ndx4 zrmAmDNNGAv;NdBymD*V3*Axn-ivpP{hZ6KHn(c~VIw;+wN**%(36k7ViUORB#cF`+YLg)bF#XIv!0ZD*?hV$sahe=Wa6)g2HRk*=G;SpW zDA>6plOD?|0c4X&%QqSu>gvWqR?HhJ_9KLZ*sCyRHifjGotho5V3V55H8LwU@22Tx zD(p1qik+)TqE=3VoW;`xc!FAx^dcRv!qc9HKk|bpY{n$hT16Ba(AK`llL5?0e_9@g z=_!nrVfNEu(0(enpaLvq!U>fEb9*H!fG;mbufS399#6J*FY-x4M&tEC#lyJLOtNDB zY$Ub}T@Ws!t2dLMXsx)P*vgqRPQ58J91kvtgSc!|jSzI0O5POc_H^ zTAq%b8DX_K?3Q`}n#NDWF~(l(e~G@biDG)*Vx_!B65_o*Jkd0+wT8!rX{9YKg@X)( z!U8hvakU|BSv8e_?vGR0ArA9vDW4HC8_tj+BJ>}Pp+Yc@pYB!g87#xz1)CX>o`W6# zRH3twz_@6@Ir2r`t&K&~?%K^7YpX4`(FrXipo`hA$KUrz_2_=BqNT-Le^SczF=`xJ zcP%%J*pazF&%p<^w7NT>=O(RY_=8q8(BKLbQ(TrZkDL8Tl3$;v$dktQc9Rtm*MwCM zwjF%maq83gxiqRxCBpkg8Ph_QDGTMxFc;Q(mi(l4BkmT!82M^Md>+<{VDWQX^p=i$sewz#dV7REdxW`wKXM`a7Vg842arEt|_2oA@Xe~7x8MlumrdTQ#d z?V1Aa^pI6GG5QaTN3#a5aOIChy%ne)T{XZ4$zc~eHwK|KVDkFYpE-(e`KkHe|5xPtN7Qd_-hUSS`&Y*<6rCIuLtN0#R%zfIk8NOJ z9CITG&kpi>J0A8Y1JIDc^7fOiRG(5+?Em`DcZYA^ygB%F_h|3k%l%hE>x+7?C&KVU zjz3s^v=Obo``>Q$jkV4rUH!$uZ^ghj)>cudT1?+PjB``@g>0d-m@2i``dy zhqQk6E+3+he|}xTTYEy7gcQMa22Ie};Gw_V!LvW!%^+=YI(R+mj?>1F^=zl`JBRO> z!f%-D2#a9@jbza+EgAG#2#tfC8h9E&P1H8r+~{4du47|!f(JUPvo8Lp+x&C*{=?zL zbUJx2Fy;Wx8LASBKc)cj9RA~vAGT2ju-{T6@M7|%e`^2UsO#>%5w?2w+Ud>@#ZJCE z#kk*amkj|vM7P+KoD0LwCmVch)XK+JHu8{dYJ8NmlrX{2G@9xmU|x$@nrJ>!)kH>O1Rir#a_BojG(BoTE-e{&vw>9 zkB?KhY6`WK;qx13tNwg#B{yds{O{_`9dMFf+zqJC(O_F_HwZw)d%m5U$Rkyer=i&B*VJkIV1nnFXn;xK zOGFf-n7r{eX^QKq(=*sFo2~enZS&BTUaVs-7%>%t_a^K1nAz8heC_7v1*)iQ=ql~m z&53sbu}nc)2%)sum%3$p_Mx7j!=>S~f0hJe?tW_xhVh~B7i)wxJ^hgOKc$1{vM1VQ zCN4zm)(TfXXX!H_*t!C@vYwB+x!5nUJ`Ar=ShB#X&NM^d@S8kX(j0ISWT??uu5S&< zgET=+j(7r)a%LW@r3`%C%DYBI;6T#Q!Z}$Pfl5y4=DjA;6+Z#+VwBT%x^RF%e?rwW zc8V@MBc!4)ABMtAyn)gib|7ai#g~)bltYd7M`?BFsmV-|+4|zy9f-R9;78fU1bvHs_=- zO6Aa5RG3OY2wDdao2!he)*pfOe^R$!hzVz*UW(e8S^SRAPR#PRh=rWp+QtLvZF3+k zS6d}Gvn<=k1&O`Rv|ydt9_<;r@^kewIx6sYi<2yPT!Ol)fg1MAOJt=-%3x(rjQuPq z78Q2G)rDCpL|2e22?@jRa3+~9r0~oU;hJ;HXc|60NuU=oJJEWbn?^KRf9I!jQL{V? za!qQ?Dj>7QS$(Zs$Rf*%%bJE+xNlP~kFTL!7c7|{((VAQWeBa?VjuGEa3nwQBewbk z1E3~{d@5QWN$4DVt72_&1VUOGwyQMQXi*M=5~O3Y+e-5Jr8cgX(gB0%!KGItuyO_yN8V1_;e=-@VgkFQp0pmbDyBoW!+qg zc|DkX8RwJ0)_`>&la|IgaXf^Lkq07E4Hb@+1+FK6|6dH$zZ(oqJv6j^xlw3~t3*Ae1nlILYq<2@9&)Jp|Jjag=i1HPr@iCT)x-rSO6vE79 zg~Yfn8YuLA5MBc&w#PagR@QABF2&w5y6vPOHaA(I(S9JJvf1g@g%}jkMDE6g+A-}dP&rtC&te{qmq^(J)u(kIWO7LIDNW%{>a{y~;tu#~=z8J__vyszL&5rEpyR9j}M zs{5_h!pjflyV;W=EiHYD7Fu23QiUeg2P0B&c+@A;xGT6JWfRp^j)b|M4?f8lACISvq!q@S{ii z_HgY}z*%-FsoT=u)d1}yCown7WY3K4bw zRvNglTO_+ae>CQCxmWfK5EE$bqkvk(2NWEhO%>rtSQLz{L_;$b{^8MFy+@ z1Tg=aS%E`+z5IA2tNN{^$H}|MPuEuQu7um5c=Kj4OQEE~mid5%#k55otCM2cHk8St zmTln48Ebkwf+jj}B(1Y?i=qY=h1+i(VXI+tf7BH>hwcjU=Ct^c0w--GwGWa%-8o@@ zveAzjQ*J$NK)wAQ;i%?>f(|IGTUpk*nLuF__khUTUlPhHhl201V2*wU?%Cv`7X+tv z!gB4UAlZdQ#wzGuep!rC^Cm?V1{4ST>aBp{uQhE>htn+oZ8Akat2y^Uv&VdUOcw(l ze^|DU^?BpLgS7{R*vI%?5BpV1fzsIAt->V1{mx0V3hnSI6BB(rFyA`z8`)|eZ_q50 zSsc(L!+n~8@z~sEuo?7sAoQOz5V|5gGPKXtVmqM45K2|K^jxY&UTxL31FFpd9h+GK z#A*cesvnc5T(gUh+GgCriE$a$Czo1}e{hsN42Y31ts0je5ngTLjj3Hi9tS=Pp^4*p zDJ9jOjAvRyhmQ~t@Cr5zb4Nbnf@)TgeYLo#HQFj<{ zwTf4^E|Y&Got4!!d1tG$V)Xk}N7vX`f6!UQ%Uvt7;s&z?b+y%%wa!Lo!@33bf524y zf)y_)K?Qzf{u66JsXM2pM~P+Bm&E!N5(>f63R!9q`b z!>)SgY)YPa^Ih6#N^Z7lz-5Ac=4*!8@SE+PiLr4)^M3|CQmixS>Pl2$oLPntF01A{ zO{5LWIaSo#6|~?4v*<+kn>PmLUrD`Hcu{Y*pMRPT#d?a{^xXuXX!s9*LbY{Jw>1P3@MEQ^RTpEC zB~)KG$u0jOou=Q=lMvb!f0OQqgFD&i#`t^hWdEA`Z-(_+Db`2R;rX8p>-AEs|LdYV zm|pxj5dZP+4)8zPTYkBlbX*@;4;1|B&p*hsp?0}*c{qG>&9Y*?sb!_}Xx(GL>gt-} z4xArr--c$;qfQ}%Vw0vGgVyGA{djyV-Zsz6M~s{PFr2batMXH$e_`Okz^|?YZk>&l zAZPJul*a1n1AkbA5dsY(LqZMhuGW5zw|MYKcD42}(AA^Du9}W~7|JV%M}c;#Cn4+K zRYJV#F)R+j_^Bfc3Sy!nVF1Z?V2sDl^V! zMqosyevmWuFYNkbf1uY~(8bam1icmpz3zf8nD7G1dIb9V5As=FN*kbpR}!R?dnI-A z)s^+)_B4>u_T_F-8ZH+=thOEj)1Z=Pl&UYxGfI}#!X2Pj#{IYYv)q{e?6~8Uro4(d z(4azP|7e6Sp`;C(4N|XZ`LH<=G72kgpCX*ln|IDz*gI zMJ`HRRgia6%-$AjQi0W6#OtwIu-EW9;CBxhn3Z;YGckL8Wo?x+n^pS5fDlVG`dvD! z5r?v3G}wPSgS|<>ztfD#6=sa9|up(R91LCzej>dg1B)%A@Rz+IaSE>q5B$29A8j%jRNv4E2r zf^)kkHLhJ#Y%WHQ1Jp!_9mwE!ZrhX|sLUoMw{e0}e`xy@8^^V{W$Q2d@Z{Q@bYO*l zBx|8lj4O7;BI|hvCyi@!ep~%it0RDDYluwGLH9Cf%DDX=Z28BRCd?d1261>0IU z(+)3Ye+zLz`8jlax#|nbI+{)Ef!crgl?$Y=P^ygZF)C(|z6&}}eb|&{nK@~#Czt-= z=)($Uqlf(u=~-%@fF7pPVRtnA1HEg}2!G?uh4}8Cpq_cs{Lt+l*?OV1KhynLz-SXu z*uU3b5Blqs-Ao9jveHCzd@A(M-xoCv84H_Me=Y#lt=1oFs6P-32IDZy6{|~A$KoP& z+0)#?+sj|29T#mw^0>XN>xGA~CaYs$D>OHK_KKkdD)i{L&H_<-Z;@YEyi@reWGHkW zCt?pB=p1SrFWfj&QXyhbz*lKHc)YjM04+77_q*vq;dDBkOgED~m>ViJ;lV}TpPZ#{ zfAFVhW$j-y1im47EmYEyYu-Qa4o6E3>_AVCK{xLrHPVfK|7b_h1P)uFhv?=wXrN7a z^q9Kj8QKA&kkW>oV8p~EyRXc=o=(oYkgHraeEfE&VeX5(Rj&c*h0j3Zu!Ep=9I-&v z1!JO>6&RC@(1r7BnjcIXgY>kEtUuE5e^k@6Zr=X@E1r6LvJbiYiB)1!nwJGH`FFs( zVSSce1d%wJ=&^1vfslnqtz>U!Hk=MG`u#M^lG1~EZHsHbjmlF-me!gzjj5K1w;&PTlRy?wrza$~UBE;(pWb-$iD;j3O1;q_OJqZG zII{-ds-hWQV`h;wFtzihlAs2Wp+m1`IZ7nN#q+39d-4Qva_3JNA(}(g=8qJzHy~s+ zrjQ3ziSMiQ%N{`g4WaJ=NGNLZf1a?;?Bk+Kt8oHK2_Nw>rUKO1(EJBB%PBwOe6Kdy z15)8kaeEqS2E`;_$UAC|niBx&bwz*b@wblLtI^i@a6y{|B{}M)SQ$a6wti^#FGBi{ zq;PBSdIGc(%j__#ebvbjV~7M>l`WE*)P8z7gC{uqwgp?ue0{8zC`ClfIC!;mnDro^ zzw$>Wsame}R9%vDb!o=Qx>Rdv=F74>WlKzez`{(=N&SCNO928D0~7!N00;n0f0I+- eISx&Kj#rD{7^W-V008rYlbYZw1|#4A0002pF%vxi delta 25242 zcmV(%K;plt!2`>|0}N100|XQR000O8BY2Sv(GDYcj#p_K5>idy005YUvFkf{f33Z# zV_6h^=T{7Pn3jUjwroR)jh)YcNjxWD7Bm+j)wgkx zWJu1+-fIS{M|X8qb#--hb#-;9pEu)Cu%|^j;#lG!5xaKt$=R^~cyb95o}6vSo&@8O z_3Hz-*mrZH^ILZ`957@xQa+ohf2j?$mE?MoI#I>BJ1hXUExuq{kMV``RUyJz`3tE3l8pzWC@3jAEvX(#c&`HWKdgHwKj^IQ`YZJyZvE) zvMK1OJENUKwZK9BCErBC35H5d?&30$qPkS5N0gupGe!b z+-OAT+saqW3zQyY`1;v1yOR7UzX_uaf1r@ zqe(n~(Udes*~IE>xst`$%t37hSW9XOBDB-l1z1(c;6ZxYJs;(0`h>V##K~$LoP#%W zje#P}QZx6Ac<_z7m{?EP#8cH3d+9Qr2DoF@zsDtx->~DAb_`Hi)0{y%oj;`!cxg%- ztcI6Da(HTYe`IJiJ-il+ve>RR_~5pZI8r6LV zCtTh|MM*zP9M;lMPyH?zJIJjnS0D8@sTnqmT5@-Z?8es=;<^vl`GD%P2I6jPAUN#UDAX8%fA7lTDy$0($WCZLv}tmxyN>G* zshJd?JXPe1ax=u~kS@aO{Y)Jd>}>+GAgum8w=WoL(NeLr-FvB|a ze?qA-pLK^L*j}h^WDa$e>{laV!h0nBzt6;yhP@q4Jn|(43--#zwM0m?+-fDD+}6aWO?keg<-rWC z86yKE&~Ht7DZ#_<(wVR7pcHxF=RuP3Q2ddL1+n<($Snc;E&vI!YSU>Ymuu`6)oJ6B z-Yyq^tl4>vF7bVp%QYoxF4j*bXJ_Ym7x6w)c)wwh-{u_uO@sotL*)h4RVHn1mNaY0>Qap zOSE~1dRTNi5tGq>FdJN0GV5zn-Dq2;m(?Ld01wk4u>`~nDXuI$1(O_rI)7zzFw9`x zdpQ}8hU2t5+Z9X7dm$Rb{#P^SV2L@*A%7yg&IcTZ2Xw|_R1a~b$l9;Ev#w}08}?Zx z;2)j)_uqGC)bkMx&Liboh@o{$rj0*x*0z^B)iRk01Guhy2G+`p1cd)6wMV z@ZB({IH4&=4$mMg456fBp??V_YZk6hvTh*^B^wsjP;%cw9ZDWp_(RE$770K%Tr70)AM#SCn2T<7Y( zJklsh%vE|4O`)n+@^*r5D};s-1cj8r<@Cs>{PC>Y|0w3h;L+1oa;S#ZluE&9CGfeW zW(e>_?7`2^grJ?Do(?Zndy7#@+G0F{kmQrZ%u__-ye6{M; zRFh_>A&9kwCZJ?f&gQc;$Yx7sX_?^Y(y-#+eg_cUroh9=hR?itAs=A)Ok>jfAV5;?wna2pCn(mqC`m6M2V2X79~QpSAtiS2z#WgpPYzJ zB_e3ZqBM~7M@f*a?U_(cfh9fs7sr1sgui)8o_{v-n~8KI#jJGnM`+rtJ-@JzlQ;Qr zL@P}uwmcLaS!2`wi`ZG8b!QbfP_Jg9*(?W-OUO&BHSgOOliBqBFgttuT8@M?G<&K> zC2Mm!SdE*S@VQf9iE36h9P?A-z`TW`CvJ!8TwB%Jc7koIbt_tcd+4)_# z$bY6&!2lbiut$VzFGe6hZL>Jr^^plhH9BTMod=AIpsI61bF9cV5Sj?nN^U1K0d62h zF^0kGd|x()dq-Mj7b?Jb+tAV`o%&6*5a%6tw~Gw3 z_oYal8E^li9_lC;SKa4IZMHr~XCpCn)qij`&pMpN_4v6;q}E|hC(@*VH>>bUYt{ku zVjNnfk9R}gsNpT!i?AAg;pO;*`ht(*pWszXSykhOejD*iy*USe$`???S6BX(CtBe7 z?N%-B;@J-{1az)zBt0MvI2(R* z^sMvX$@>&8IwH(w``0)t5D?9YlEmkQ51PIirz8T%c_u^h__ox@HbFcu@U15#DOV@;l)P^#FxTt%KE%7X1<&QsB42!H+y-p=u zQHy%IYiHO`baV*Kjop0j;7~`5@yIv4+k+vls&9aGvV~D}h{d^!gz5f~>HdKol)}3u z@~|VAcurqyNxN;JP{;CGn}0b=!FC|?w;iFkdyOfUCc}ZGT1{2_x@8Ga%V49V1tMVI z4^9}AbJ<{^<}#gd!3L>M8=&Z5PCu%6d9AD!c*MA-RZ^DOLcX(?v zm&~iEt}oSE3AINxq6H}8>lQz??q+ZD)Acntx|WO2L$&sZwNQCn)hgN)dXs=PLMvN) ze|!N!pKr!PDV4GdDPQ-5&|1rz?0qh5uO%}v#rsN^lCx<$?Y?B(_8{xADShcH>Z zBX4V2RrO!&zkGw$SAXtlHT2L~bcKD?09QVE#l=6ZWK3@Q=ukq^G;16w3tSj0TIGh1KNzB#6It7ZRlg~iYHk8VsU}4OX z8Y7w!g)mEEs3bq2Ez<#80^sAhH8EUtc25=-9Jg5`&ko(fW8YB0hCIH>7J-i#>7!Iy z`=cDs3n*4ywtp`eNpw#hEPnF`ut2ij0Pu_Jg)-8b}1{L(y*2R7cp;ptGT^ox6m{U}o|3O+E@;l6E zSt28)3?Vr2$&&T%9C-%>$_Rl^0=QH;6 z#Nlo@_|fbaR~=s40g$F_&EdKo1Zm1P9RAyZkbkDk9SJ)a(v&@P#smW*oq<7|SDoR( z!j3aYSh(g46&9{L1BQhg&ah$OeP{4=?~g;hKMD2zG}QZEsP|`H?ako+XpscD#v(QD@Ctw$*0^JX2ynRR0DsX{658TxP@Bmec-SqUagcmWI29s2+*yGEIqrdC0!G8B6O^H^;SO}N6(V1@TD6PB0>R^;i_0s4kj8ia}C@;2}EDNfEuy z%(dkKKPj`(nPd8tPpiMfkn%e?&wme2U!-S~*%j%jqsioXclIuA3@Kl~C?)LxA11J8 z;yUmK6br|QlPk)BYiIbyoiHBOHly+sGWX|`Niu?3q&k!_dT@c0s{{W@0rYZUf>_KpJekE77T^-n_ewR_vC ze2-VYmGJnoQFr|DXBC8N;(r`4taW`2-hRbDf6{+-R?VO5O6I+=H2|Caj4^~VI@`Km z+DoqKHA#IVh=p(|oT7JUUrvr@-J#gWzM~+kM~6c2<;#4Z9@&9cJ6_+g09;#ZL3Yi0 z&u}@AvDxZA486ND!2H|SlpyJrbrA9L&GY9n;E?vfV}70Ooc|bwe}9;ZZV(Y+!OD4y zSrl*@fQ9iC7O+#^q#H#ni$M;J$N6X!7;7`O5S=R+6qT0Aq_{oAi%^^h#fKi62;vJf;y>(8UJN4yH?RCET;lS3eii_&`_$o%w=bmp#Q=#_FvvG~e6+gKgt^+F z{_raJg$${=z0FzUI)4MJ_~QzkPPlM==+m}QqKBAWi~jYwiGC#W^DrN$S>`IOo};t~ z>ZkKbo(8~5lEos_w1BcT%K)LPKyfH-2M8@FTIk?V2;(G# zg#`nT=;8qGsnOK)&;Y~5)8u0-TZ=d_3=eXE(V900FbH&Xfr)`ht4|*p(<7k#TYv77N1rz3lGI96d=A~F6a%ln zIZ)J*w1A^er$6dDm;gwu3zpQ-Qn5ps>vg7gf<_1GTtpv9?cOq7wd8uyQkvUrFzJ{( z&|ds4kKo5k#wi+Ds`<#Y7E7nvJEC(vGy*luHq7M{zew86uK97=@#Y#NRtM zbR}1G!ElpQOjGIuu#PD}TYHGeLH@ybhs^Cab2nKOhi;^bV*lo-9sqDMSPKk|K+qR) zSQK8~lTT4xxS`=Xfh-9O=}N9@^uP@f)xYT(BZ2>NX34@H8oFawk7r~CO;@D z+&Mc|5sHqe$gQr9U2$Z=i?A&n|H6QL>wjj_R~Fc#lV8bjIyQGmdD&dBR4qO$3sNWG zv^i6>@`H&6?0wPA-?w*rnXK6~v3|C828d+*st`y=Spz`9NB{%DeJ1i*@lm#Bk>R+s zlz2tAoRQ742M*Hyr8-5MIkczQkCPelOHeItA6aH zDD5!*DRfNVEg~iyQYlCY?lT$#xsW~GG219>1LfUaX~y;}NDRA_GRR8qq(FsmMjcac zds_jrZk8PD9pE67@%2)EnqFR>V1HdLrZSmE6V3>IE{P_JFD$^{6QUO{c3mL?bFn~( zL}V2)DCb< zzHdb2wQSnSmD4OvB;rQLGJ4TaoSR&kW5m#E2T>N$`k%d{IjMz~(R?O;`hQAEsTHeR z7KiIc(yHcY%li(1O3}Cq#uCGE704yU;~FZL5|FFFEhQpX0jm&_TPOf_3@)w*-4Tzb zXMI}2C#soFbr#CvC|g+5YsB>~7L*%}=lXULu0`?5xD&OG%tPn$N5*YH=VaUZHs?d< z)A|~uN6dIiwrhwb@pgN<8GmViY?oOf71v2%lNj6`dubMF-zUQmAg30E<~6NbsFu8C zhdDlwpaLjgO0f;U%f+$0rFZxS#Zk=xMaOMQmA$)5k``DyUZCoJve{-y8U3g7nBcRjZi6$oG51$FMQ zn%?{ypH+G!+V#Cr=ZjgmU38d>339>T+41ni(%SY~5d@B(BY>q& zP?$#hu-?=e+9_0=G%4x@46#t@OAj~)(S;UX#^549IoC`Kr&QeG2KyOVo#Jal*#B@y z>$Nl}G=QXlR)6>0aYqv})3sO5&O=thV^WU!D==eg;H6;{W7)&X=P4u5A^j&4DGf^U@)Rxn^4+d+u+ znR`&oH*Btmkl14iA;uHx25gV1_%Adn&N^y2E?kdAV5H85gTW}(h*->T-GK*gAS7FW zhLCJGARCkje6rjaq5!5_Gp1s{;E>9Go#Fm^r`$Q=cqQhhNdSz|1fPH=6jJe{ke=fL zdQL+0xPQqG!-Q0IHdy_^q2ZlM{snXHW&wbO=uR`BG%$D2ol*}3D=cv?u)-3*ft$26 z>JqRLme$#MFSKFy_UWY?^Vk;qhVHCZxqn-Eza7}-(%$~b`7Cqqk=1?U-C->3=Zn&! zJ--wco~M@(NRKsm$P%1KDN?~AnV1l}S#$Hg+FXp*D&)aF+ZrC&rnFnYgaK(7Qb>Vz;H9tN< z0Cn)I%X2qiuI_6_eF9tbT?eK#-;;22yZ0c5}7!m0Tca@Zo95Pv+(cK}N;wh=V@yyt!vut{xZ@Sa_t8RDn< z9UXc^hv^z?j!EWRv;|)-+M+x5kAQCJX1@~^tf2x}{C;>g$&imbfD6QrkaEKo(w8a5 zgX3ZXyl5@s?sV_nTdSAs7{;sJ2IieqS$cK{7u|6`9nkVH0Z~?(T0K4h!DR(q8-Kq> z4-@{=>7l;G@F+o`ZM!(w5>ST+U9mp=_}9Nsz;qe?*s(7vK}9{yNq9Cl!6~)P_H}k6aFgVeG$(qj4`Yk8W9MSDj3TO<_8VT!D$UlSU%wp2z;?J z@g%?+`|?59sWJwIz7=&!hq$~gr;RrmXp$MfE=miB?1~KYhc*obW?6^=s~keb0M4Z{Q0nA{9z=g|-7FSF zeuL0vBBTiL;e9F6A=m>RYyaF3OX#L$uP7>*k$4wZVtue-48$PEc5@5prn+<*C(bSWkTeVWaLO4E<1-ezoTTS=m37*CE< z+?(5C2Zsv4N{4-~qag6)*P0Kjm=#pvz>zgW^L#S-2%E?p0yuD|R@ENWr7ZMf?fwJL z<|LK1M~ke5+_ntc(AX(riG})mhypX}ABR&o~ZFkX;~1UND`4u9^v9Jx%2XXxWzjep+#%0MF7Yvo<(~)Rh3ozt9ZNEIMyMnd?Lr)LlHW zg+(4nSE&Gi_PI%SD1X1LwL`p)R8+V(>y^~4%}9);yhH(@sk&u24CT-#pSU*1gIsht ztuyZ19=H~OkMP}lT)_-Ph9hCTHWTWPjqtq81fh3L?C>UFL=* z&qCFGH)4u0Hb!_F8m$wZsA3B=I+HJSI7u92{8UUaz_AvHV}I4GxAO~Le|0Xos5;RZ z7pNy=%!JlqtXO9W)`(^mM3roaipyzr(ealAzLZ<)pA=S<{Qc904Bx=BB)Tqole`cU zcG_STRr7|pbANrE+;%!z3d4SXKOCjsjAxcVlk|}BXl8Bg)SQa$r6==yaI4KYBUuO0 zy=Q6ueloC@V8nO@mM^r*@aGo$4#uncDE?NTJ_Bskn08etNLWv5=oL-6pld9E4ZDIl z02FHNLN*Q!+OY;#AOuiVYFop#AS})pWpex6;%@>P4u8qNgmQL+s%L3_J{zl(17d>o zoER_JN=vg*Klc=oXFS7ywA)IAlFxDo=wc-hFT0uSF4Y{Yu-aFWUlmK8P6ggAY1t_V z6sID3o#xj2zJV20W)8(T7x$>H#M;KDue!5**c~-8I~!wARWnQR;F%FwYhDFr7LEvx z4h%@uS(BBW4}Z;xW%FevFv~)mvn6bv{zKk3I|etMoU&<5=a%*PJUrUUS}{fw^#))#v1;go_{YZD_howA{CC%EOk!D|IxTE zim#%uE?EQbbbTRZ9uMX!P87~!2CxSmd#3U>Ng23i1B9_H*NnF+QI!l`phe@h2GJ0I znMj#?J62Ceu(sTii;^ZCBkHWz5vc6(WN?M859#iPUrKWahu>Z1bX|1psOREBAX;eF zF(>Gzg@1Fn$?F~0rox%b9u5pU6%-$DtJ@vS!m^>U23EJa+Y7k3m8YqkmxcjgiFw4$+ zaDQ&CDg^O^IzEcJO(PJ4*-9E-L@xy4fEYx+1&LepiCanlv%LFU6v8Z{rgiik9)x>q zp;B0Q@DB;E0wH+VoOs2SKvyP^sn@nJuxzQJ@w4Ll6fo0+9G=s$#cWt@IW0%DlcQ5k zFM2oGe&R7ioN`KSZ^D(8NKHH8xD;Rkt7>vvkV)lGa7+ICE zibRrhlk3 z*@;rf85RJ$nea5#%+JDbf$Fw0w-Sht%&)u9ySWFU5pGDgz)Xj~mTO^3n`r=+B}%i=A(l=sNa+Q= zBPq=_xI&P{ZYpMYbwJ*D#+%y!a!X(0_70!CNX*f&pF#lL#R_Mz_U5gS(qJL5qDV$I zdjYVbOnfbienllr;a~G~ydCPea=#{Gur|Sdx7#6l?R#WDLy%BeJd+NqHAG^1+?P`% z;9`}|A}b$1Y@|$x&{h~BN@1>|mI@Fm4prjl{@mzSlC%GRMe8j&a?NCt=Lch?(pQ0WC z2$Q~|7bA+*0Ye+1V7!Oksfdlr#flSIU`tO+ZiJ|2Fy4t8&@F|F6_fa)MhKrb<=<)# z_&JkCqcIz172b@qE+m%B(*ahK50l>BPTuUlJX&9S`(l%lqbPrutFow@fZB0)ZikAc zyMw`-^|eOVjB$^dl5D%oWJ7Qr6>^+V_kK3G@A5% zRBh=FVa$Id-ox1rR8->J)+zAfbyY1T=oZDAU=npkE@wK*b&ysey%UerR^rZIL%Wzm zVd7~$m2_*hCEc=$HqqK94hkrFpm8tsGOh!oO>ye$_CeMZx7KZ$R&h&x%#gV8Apnx20KFjrut!Vgeesm*P)KX?M=^2&&z zQd^lpUd(F#l8nMz?&kdr;g}v9(z1>FLTb{(t8w1FY&%)b4Rcr_?{;Z^2AP$uNN@3e zLlJSfBvL$+phBJ6;L!#7M=%Bf8A^#_nqlMbmo#^y7vv*XfRB3H3d5oCXi*L=KHR$F zu6%!`H(IRI(3VEszrWVUYd-y~4fv&2!hMy3%(*h}688I{7nNZpHIR>0dNkM>416rD zntgSDAH4j1{~k!6GJL5V1c77%ej}MXfVW|_oqPd251J0Or?;`2icQ3&pmQG+kqb^~ zv%?Ol?#Hh!^ebFikZ*MNE8JV?n}FngFdTomUnQ`*G8B(jc$5*~q3mdpI}3e`8tywW z!^A&5Mq5RqT>aTAeEG_LI?0>dQ;ZN$!8)Q!XntETd|O#ZPT-9k1k|>pHx^Y5S+4aL zd+P$Me%T!cQuvDF@RfX|7FgUwmk1~VOTa}P(YLH{&)|>sR1JL7)&*j0xL5p*6Z<`R z+*X3n5kM0mgm;_H$bC(YW>*YYq4wg>4^5`|P6ag<=crb2OJJv-Ms(ZImhYsHxw1+< z*81Kg>mcwvlW?bq0$uZy`llcQ;TDq|s2&OJy=156@>R9xlS8N>e~`hW$&BRC+NXf~ z%U(F!EC6jUzTz)oS+*Ya91 zJfqq&DBa#4CRnq=_4Wgq_4aj3YNl{Es54yND|_yCB9n}lRcJ^99EP4s-^lv^=Z zYTdBfv@s1ct`kq-e`!EzvZrnN{Gh*PnG*^1G#yF0kl!O+6zmv#F%R11uwU`%DC*Lw zp6Qg9j{x%fFw-Q+> z;7g+m`>jS8>fZX4X`zG8;c`qC2u7daL=4%iVhrI_dW6qte^7;>z==wIQUN{`V%d&u z8k-5@D{%dg;N)o59gc?McWQ0|9_`#~0C>h&-4EH*eb1cc=j_-EPaX;2`~GCf_$pwQ zA0Rh`4Z*F26W=F<$+J|EFG<-H6{<1TjS@ntayhv02O*v})nClo?{`Oiw!JpF>&|9|cgHR~)PAMb$i;e-^Ek6nFs7r^xk2t(2?I28GJK zZA!(35-RCsP?f_QL_xn1JzI^dCqiE-1|M0?D(#8lDZ6{kD2|+zlNden*}zDdvZhFUjtHrC$GRR|#HwHJ*_K z^`=qve@(C=v@(H~i6LvDp`o62#}UiQJa;yNJ;GE!Qh7Qp`tHYLy3ExsG#3MUP{aL+lUxHeFda2_DP%6b} zUYz141cMne9pc1DrBDhnWQ)||fepEM#V=mXePWASEI!nJ+v@^EC^jD#~2z4B!IiM_MAOfm`*-y?>b%os*JaHFWLKj24NJI&8 z(N@Pk)&5!>yg>V+=iMy-YwU=OKk=U((cf-I6n5&a7_aU(-~AM@7(rELa^+nSZHa2{ zhUB0xx*c+j;*fG)+LoiRGuuwbMa;Bbf55z}j?TjT`p0zp-(|Y_OX~=qKynw<-QMIp zFAf!R)Q~x@!JrMdt&DlgR`E{uw4ICpFCUIb8Vw!83W>92Y$`pDwThfo=lNEuJ-q&f zy%sngsk^OsU@UgiSY|(Sgv1dNWo*DR)H zLQpSNFoCeVhS5vNGSiIC%5Z&|T|0t&nH}p2?Y60WH|gMQiDOpb2RkWDe~0T}J}a#iW-wR>`F_PM=L;qDVWD4<8XDW+ca_0N*E(@)Wyk6-mhlI2p~zB``rsr2 z$+KVs0EGfV6Vn44G3kP=_RZ3-HHon?s!h;5;EURxoVethb)lgfwmAHNfB!`NTh>*5 zIXH0^)9}=AA$ci~%3H?govH#a53q~AYQC3QHK|zF9FcCQ%I+g@lk6+6c1_8ZbiPi z#%LIxZgrb4aj{AKl@D62e^q|VmQU_uR#WGzadyDm@Io%iroomm@X#=zYS2nnZt4`{ zF?+n$B1-EU1z(mdqr7U-GKe)6UIJ|>fAi(9A~AperLX$fd&{0D$d#77c&qU2m}jYD zJ6Lb2gHwYA7P)`cwtv>Pzs}nB)$!D`gR$~;D|&8PETQ2k5%gY`e~UU1&{LafpdoNU z02fxaq^>w5==K%2>*mseZYfu3sa3kOZa%>a;oAJBP4W~Ay@zaf$5(hKg4AitfPj#( z)h0YGI`e&DsN3dK0f>YkSu z=eW1g(mn8*1&RFvf87L6v*+yBKg$R~Tn2^q!3K|CiX9ltC$6}Nn{!s#XM!YFsOJff4wV1`h}fFoi2eEkw~TFd*X_v!P%g00 z36ZeAJ%@x&kZI(MF{4L@HTS#X*Hxt!nDjotEM7q^KH_*zSpZBDUlom@ z@_z(e5NJIo<2P&>56m_R3*U@SC!+y=k{w;x-cn9PA$V#ow_0)7wU9Mh#pF;@M@BRT z$K_+toz2V`V7}w5O=*uSj)2aQyyO8e9M&inwnseV=(r3f94{pMm&@bACy^zSvz#%R zl2nuDVEm2(A`P)D7oALH-K;>o%RK8?Z+}6kYGxNae5s!fE9}a@ATxJAft!$|I0L=Y zQm&KwFW3zOJU?765^=UrS3FUnX;d_9PCNGiESyu)9;>jZ=jD>#&vGN_PasKFS1j{w z^%o*}^!m+SQ06h6yMQo{#6$n5pn04(pP{p@!Z}gD*Ewf|+tIh254!K=&IYuu0e|eW zpbA**jisf41PNFctkb13w5DvFYT$ueF45lbZIr%y!7+YAe+Ay&>1XlifB>w;DJq(e zu{ISHn*%GX)=rnB)}HM?KfHOprk<Sg+OZbxzTBJAe9?dQJEJzfZ4$1T0^zErX#oW#jLq*6LAIG#?jG zYYr@~)?CdsK0h;>i{ALk+VZV09erWBs?0-RH|DF-NENmxL?X^AiRE&iLeRGmKqmOr0n(d__nU@=OVV%q_Tfj3W?qlz)-v1U@57 zQm*hz!SHhCBQvM)=)>vQcZ}O78PbPml}Qn_%A`}I^veM*PmnM&b zRw;jWrjOUlb7+4PX{h-ah<_~&aw0`!fxbST46fK=z8ZJ>#g0K`j78Nk*&SST$9;-g zGY?}a?(^4~o~M`a@~h>y2c%jIL9BBKFV2@ffW@e?6Q^YT?v!GgPrG8lV?kYkN3xQ9 zlF+M8dSU!)ym1xhmL!m@Q9iVOU>QbtU(tgN{6Q~c<%ms=x*DR+V1Lx5sN0H@++LEe zWT_cb<+Ut+MMm$eOs9XCPI*Uc7!@KOoJf6Z*nLAzlECkBZ}I7_=gohePx5N70DOX) z-{N6CQebdFy8**hKmWfQ;-inx%8AUd>T=G?<>87)sIdJ;pL9rz8USf$_9x>U0$$DW zpAvli{+Fs^-nEhi`hQ6)RdW{XCSXhdTe1l8(%@&G0*{0(E!uK9X2bI*x)y4ac$|k? zKb-0z`>g)UQvvHm8hMfR>gn*^5W|{_9)cWTrP>cch8Cs;5!G9)r6m{P>K!YqAM&50b z0sUfUzOrgL;ckST-q@DBd;|Yi%g1Z{?9w@}9}TQAKVQwui%a z!S{L?vYDuIQ@BDRCMvsI5C5at@azl~W^IAGsW}%Ub=4=U%8X?5CF8DudFEc7hey9c z*l`t(zUW@{(tk%E#HOiEAg|3((OBOqMR>3WlLmo6Bm9u1dBZZu?=&D-7mhJOSa_fp86D)b zqNL*J(86o(fB7$S;X>jpD+pef4KY)HZJ zNV^h{!j^z7?*<^%k}00p?9y7i5Oj5YROQtz?v9SE7JNq`ebdB-9LEp-LBw*zi(Ub^ z48L~a9e+njc(A%)g3`;<_bp;)S`sClvJ(ptJzZp&uAcfKw%gy42FA-0wCW(Hq$l(q zgM{K%v0-U?NT>?n*cCLC0v1T&DuC(KaDbNbjYBMdZOYPrC0g-7Hv#aIu zV#(c?No=c#@hyk%1&Lm&oh@0XRb@|4=>xb*+kZ>0sTXp~#8enEnOiVw(_?vF1tzdW zGE-g6Luu)t@)k94Z6wK4*Sm!(hHQ+&q>(bg)>U^|1auKHiZ4kK4%c^Z+b?v8gJ)Rs zX6-CJ9gfAgmAt`>PwyUwp5CP^@9_D=e6}5$JlAySJ!U@aESRGBs+G#1xs+#{RquHD z|9^Ds?!kjztMcKrUOpCMg*b)A!XE}T0u|Ed>Wj5U6MdUwGx^ZP8x_v%MDCj05O_DE zFb%f3AL32U*?tbWOt+K9Ky)`0KiKK*AbFICR@%;ix{ZNrQ`APssf#FtEe-p4)iiwj zVltb)A7*E7U#o0Tv2GQ7qk&6-R)(dcJAdpKO{+3wtFT1~ZGO|o!eO4>yt-mE&&(si z{6<+t*xjO_eSFVKl%kXH)_vB|pMz)iB_8Pw(+M^OJsuTV6L_PHO8H^;KT#w0E?sTYq2T zKUO}f;?o3r4K@5Y=Q}JHK`gMB@D|RNIMa7-}zi zF~?3+9=LssyfUj0)2!5{KlXf4)^YW&KNj!gK8Ch&WtgfFEr9D*abjBo1lHR(F(Lym z3VTSmJcQ=&uhMw7Txweuv5V})LVs(wy%U??Sk|&%Y%dos=r>|a!)*Upa%c8qX%;SB zvC5^%c&05FZ8p|{BwOmRUsMbv(USU=r5`NO#8uwQ*z%@c6;{Yiib-dxTKh4rSQR2E z16BNaU(~tX1dBD}Zkf3d`~FqM^WHOiEQJ!w=uvek@(8_%y?j?dcS(1MXMZ-0y&D){ zK`^`Lg&&GtOp&)Kh^y|v;!@OIjG{8CxT@oSX?VqJLjX&sWniI+A;?q_<&`6oy#&*0 z%a|EG64#Fyf9~6jz{`(vc@k>`GetjMRE;;TOLsP%Bd?6i8~OM4}2c~M67Gmhh-O) z`Y7ta^KPRQ`YWPLiux-oRynnJc9?}-7H$BdPE<3O4})gOw{&700evEZ-LQH24ZIkV zJ#)D+xU&Kkm#D4-#s`?fstr*mPbSl=_Myy*CG-K1C1b92so>!zrWk9=_}PCfY0MzI z)?px<7J8N*ftjp=2NcUi6PxF!Fy;V>C(?@6*7c6t?GrZ_7qq1jf${h}8_Ixd%&ql7 znNBJ>7kzKP8E0Lv2nDl$ZY2lj`N64}1e2M{frAm$c=RC~D94ig?!-g)s2f@%92Oo; zG!t9NAkD<4f-#Emb%d{v1^9nTZ?H+0ijf?i!i^RHWwC7pPl<81K>@N&y@v2;8(Ya6 zLB)-sqF}d%5#)PWd)-=&+hjCocprQ~GEk8K3H9>6JARi^%NrSOr}_xl6J}bdxoigW zNenh(8I%$Wyb+jSl0iN1g!=m|)Zg#e)@Ie`SuA^?;Swtdb|$|o`6Pc7Rd>Kx`io*} zsv{#wHFsOX*cCYu)*3bt(5vlUdJ6kOUBnE_4|LWo{^_2wX7(6Ss{V$C)NCKUPsgGs zbIt7o#%6q;HJhw9f{Ze;LQcAiO?{D4=A*P(y(nvCFVxW7B)n)P8=Bjc9QEQB84?-9 zV~<9SG0P)LbBd`w$pL?3;eVc)=6H*~SD|??*qkSW3V<-56|c-~W7`Tc{3+b@z#wa| z7wr&WzGn&ZnKv)n2~ypkw+g}RGzC#x$O|( za*}xSGM-c2Fwf<;0-i^DT8!t+jt=qMd|oQgRa(S$2yi(`ym@08*h=ki+t&m%o8 z#&dJp8e+Nrx>SzKJc;cP+;VzY>oR_0)iAs1QvtWb-PC3_SLeYc(P;0@L>}fXd&y(# zhqLOTYG2jsp1l}}kL}T?CjY7KcUgtAPkOzt;Ljn=@oSS1zFu+M#8~eezTfP9-|IYfrarN3<`R+HkhOB~F>K%wGALQf zO!{uiULf+qwfg?ikAG|Zczp7gRffkW^J>0W%Ws2tNe}Un`uph8g|*_6l;REOw|VyY z|LDNKjSloRSv3tfmu-2ICgJhPGWcIg!nd?6m%y$?5ctQ$`RkY$cDp4A2ATvm)J2?* z-hYA-JNT{Oh%9!|H>KHNc(dKQuE4bl z+*o7WxFJ!iLjIC5SUM{^ONO{?dOdW@M?=2D^jt;lwD3s&RhR;**KM9|0SaslX*m zE>0ywwaU%j!h5~u%5CgEui3yXdY8B8vTX>D3YTo>yvJH^W8YTaYJHgrWvs764 z-OJ(R>??oJ%vw$N&!!{qzF?49TD)&+5|@c-XlffiA$rIq{9phq#3h7^JaTX1A&)5Q zq$^Kqte9U+ku9BVCRzIFk+iHUZJ*3*1`{zcN6CleI$4E00w2V(b}hkPC!3q9i{lR` zWTr2~e+jHyP&=BoTP$K!7SUl8e>{VFCe+L`8JHpCJb&JW{m@AK7g(?8X}1lT_mY#O z!byK`pAW}rcV;>XLD^!;ndZ`TmJWsjMyeBGL49Q|kqhY2(GKK5khu@Q+>;aQNKC0r zRNqXFl6yOpWU&RQZAM~d$?8WfHNTR3q7MD-&P0N`36-N05^5yFG4*eRUvy@&`CSko zlos{WH`K5`*s{aq21scPrRuB9qnqcBF}{DLQc|P{-DGhE)RHn7qob*Kkr8%;k?NAM zDWY?WeORp5Z@`x#{T*UJA?b@PpbTsvk4LBFitVW!v5Fd78E!>Hf#$|Pl->@|=p}!2 zCF;v&J{!J!m(Hq4P=y|uKz((^)oBjWyYx=E<@y(*RlC~thJ4u=cusve;1*U}?$>|C z)rNgSU=l)7MSRGacT!7wwE+;+`oci50LUJFnO}&=@?NUV)-Zv$ys@(Tb4HG{7eh_h zS{FmKsufkJ;taL(MVC}U)RLs6Qk&B5=O2^mqjJ-t=Evn=dB~EnK@^P&&CcybW@iws zQi%$Jo{NZB1MSeTjBLN6>U-IQ%+r6jA+Fry5BGlK1i~(_4k3K{pbn@Gb54XUR7h94 z`ybogqWl@g<-+V%baXGli699R)(%mM4g}HNGVIS{@6EzyXwY#G7C(O!w>$|bau-60 zN*-6=5q8VOD3~~4a|)omQsR?>=XleDeH$;>>WQ##en z0C{*~Q|6eBtfG*-&Iz^vkQ{;uNpam}suuNPdFH(iG!Yzr4L126S}imMUV?q@iBJH; zELV%hQ2ZY>4cG;?dL@W)!E#mtgM}6kI;YkcfRE^sxrK(C$+#;t$p`$`bpVQG@&l}* z*O!ukN)Rrg(+`I7OCtLgi|+{^MagHZoU;QRi&JZ@Kb!LyKw{#p*f@XB+$#?(x$0Rv zZ-0y)jylJmP+7jY5I8HP6oF9Zf_<;Ef^wV!fmiZ?lVM>FIaO_jMAO<$&v#U7(1{(l z2C-=ckl~Wf_S&b(Sv$jo{cStwkfI8`5s-EB+AKzl^ixIrncOE6!4`TnKzCsAE`X#_ z1X!T9d;8hz;k)at6&|BHz>nc;I`X>dA9; zZdVr7N_;8kr`i!aDr?ee*5Z0519fVvw0Slrh(ve`5>jZI0a0!C?dDp;p8hvF_6rTX zdLKu$OSTi}Q`k%C;ng_rUbdmssbsbU;p*l)YZ!irIsOcf^Vl+P`U(3QjZzfOtSw6X zYJ0QUB-EU};q3MZ%rq}J!;gI@=Fxyy)idag!IvBNXcn;8xNPb$}SO z@SmQj(ro&$x|fqq#~6Rgal7X+kdU(n>vcN9CpPHGCijf?b$U8VFU6#Lbkw*#7EAh0 zVCNS=fT#Q;mi+AC&oG3*v z88k3x;zu}p&J+sTthg5c!w*IuuzniYve2x_gxNVf>yCd)F+8JsF&yRR5-k7qFAKd( z4YnB}Kz=SJ;TN&-6#K1mF29o%V??O$bMgApz%OEV_p%zhsa}-b^tm3pWh1n)qBO`# zah)o5T9UzW9ZeFvv6yLn?w?q`8JzJWqdpxAcNwJ5v>8}#|)UE^um2i^$% zeIa(B0#3Wv&C*sf2KPb7Y9}e}3o`pS82JpS!@qqn{r6oK=`K?O5jmOwhP;1!fz3GN-j8r5gy7TRyJ7xB@TSqX zsTm7_c{TYQ9S|I~B4Q9-bayn&(_N8j>h&6zU|@$&FbsrEFc2v0*gN;`*yW24iN+x^ zD0^AIJ5B%Vd;;Dm8&!v-dcUa^5FZ&OPG{bl8kJ1e4xKUP-0!asimdU`WX<9!`W zabbU^-#gJh6%0vGu%ClddeCl@R&tMy;i>Hexs%V%Q{p>wHr&DcD0c$TN!Y|Z761Cs zkNYR8O;z8RkkWLPz{68YE48u6uPGEv7c1GdbunvUK0{%*C(!Kn^Q4kW#5ZTrvN3|B zAIawZ4)c7J?u`e-?pRC$6$LmMi`4+t)g~bgVET!DfY}Fr+-t0H?KC->;Dp{3Ys~Z! zG;SpWDA>6rlFKRqc#|v3HyUf|>e@n9%o{59BZP$5t1xCZg|wfYnjNoVlYGlHGOIT4 zX6Z#L>@?_#ovTTrR!@SQ#nT0Nf?AODJRPsW)1HPu@`EUB#w62PMHCy*);`aZgaoLu<(#D%B2AWOS!H%YI4)z(D zGKQeEJRLhT!fJEaE%g92jh~2PjJ?=@6MbP5#q_+zN_mYW#Cv;qqG?=f4UY}eN?TeA z2N?#11!UOcYD3zxYAONUAE&TG9OhS2J|ko{oFPL*=sy}mg%-K*d;ScbiGHZvkU z2Rr_uLT4d?anXQt7qeZDzweRi(fwLQON+UGq?GF; z)Ht^8y4NsbN9F=O2OreZ>h6G^o3xtY4_ehggDX%>aaqbdZuTchel<;zCynjxCMzPY z39BA#JNUli)Ti@vX;hm^g!i>FriCg~7Ru*gF0Az|`9bYQ+%14H^40E2IbiIqp);)K zSx)8Ta6&X%Nh*uva388YQI+L?MHI8akQJo`VY+k7P3o|fm|-#4;^=Tx6@KBRc@7Y+ z{PS(8;g!P_xy3!yTihzlIh>rOM#4N6i56*qJ)#1s5+M)v7mB3GN6F?r3+v-GBv=x; zMg1acI>?%Q)YLF6_9cn10MZa+BOP^O9j#g&l`ZfJ=G%~z!c~tUI2>btBI;@y$wXM` zsj0KJYYMp2Lsr$q=sz$X%^JAEl|L5sR-k%x)c_kLhh6O4Ft}yvDi!cu#kufndKvI4 z1YHi?pYZG6f4_aY|I7Z-A?ZI*cspQZ-dXLet#90a@Z-aub{{`^y7%l3YbAI7+pM|s zRe1s+>qU2Zyt0bdQde7l$w~+R>WIJA@UJ!T*E;^SF84((02(q_-hSMb>QkzU{a=24d-&${>w{l*kM`ca*ncUszNq(V zA`Cy|`2Dq?9z?6}{UH$pN@5R6$tgo%cYWuK%T;EvNwRaB>_kVf0_w?EP9Bg zRsOp-7XKA$;Mrt$W*@xjfP>%D(Fi^hQledcc;3t8B?Z`0>f-bhY%P9dl;g2 zjhmxY;E+0hU?$nb!{uu_SH4}fXS`D6#?oY60ke6xU=rKidS4UX7IhPT zq&3#m-Md8T0%s#&drh^j71E-uY$wRaOK7sfNo@Ro6@WQ}fDbv!bjoHnWIbX(aZopt zqA|1q3PVSHs)SD&T+y|Ij5QPi)NvnkW&%jjsU*OO4$H(k{p5(V*h_bc5fnAn%2;FV z+0HuX@o@^*Ore%Ce179>&7ZHWsSSdItMtvlTzHZ63PPi*?KeBc@{T-elb#Gy8gxuigB-Koyk@ zU8Oy{KJhLfmMKUJA(S@zQnzf+KGYL*xHNo!){RSWyAWcw{Bc1@HoSDaJDFa`(@~%-4IFK~7a86c6ppsL%d9R6d#ZLe{ALX>2E*v0# zkWlrEouUiR2&w4v`=Kxsuc7ps9mttW@#Um99$B8m+ySK?ygg;2Nj7$Y*93@s%ytct3Ta~b3EAT^4CabhUly5$NJmDkZ2pemxa z&6M;-sT?|s3R4LPLF)iwbCogG`XjJ^Uh4KsG2txKOHn&Bi{J6tiCO-Zv5>P{+jtiiLCTU8LaGy zv7ZISqQY*tx-ct+=n8TrAz}C(&Lz`@6rMRETyt(2O~dCW3G^~%Ct9xy(}+fY>*91S zYnEq0u1Sqq1!UGZtFM&{S!7vpS<^5J_if7M@g=nDf+h2P+8v;^454*f>_grij^qb^ z#8#hR0Mz7=Petn^37unaRje(JKuAl&c9jMjEy_Vqf^mSRA+Fm>-d~uu{{Ki z6fE~F_XE~HDz2Zq^$)Ru?CP$6gh6$5h6Xtp#3Zr-4qLJ+pGvhvK=vLmZn&F8BYq*L z2=l(|$e@`h>)ov^5cHxuZFqj1R&tTeO^DvoI( z*7b#$*MrIDaXtxb4Oj;?P|?U>+9&ux(Kx-#ix&fbKsw-2gG)+! z#&fiRXn+a^0xO?eIRGrBz4g#Qp>cTl_60c`Ygyev$+Z+iMBp7eTTj{Q8sWkc`|6HT zIk_X&t4`bN?+l`L9U)#Od0s{}-a~Oq-89BbYge9C9M}>E%x|{$g^zHZjr zH%1){{KmX5z`&RU+Wp;suF|1(03rHOXCB&CCzSN(yzH=A`XdNru#VK#aw3DR zWXX=M6JC6_9Y;FSb6qC!SWBJa9-rtw3fH-4R~4O{R;NFBw3nTKCGW~_^7mor9`DiQ z&C#=mOxt;v4h3t^hvWR=&W@d~=`Mbfer;Kvq2g~?{bl&E_|jQ> zsMV1Y+r9yYE&5hWQJn`-PIVpxStVM0 zM_zRv6fw(?%(*3hFb=Y--h_@{`s8`k!ck4OO#eR2-^&sVmeSWT<1;{o_Z3_z0#N&z zYRgPjb-&eGc=^G6H+wv!rKL~NLTejas?fyxU_=TIkNSi*}KmGV4FM#Di!Qd;9IyVgxgtF zA)?OTN&^>mi)7d5kH$PM_sX6DVgk*56i|!!fP%xbsUjQ+i-NJ0XlSOwKRnuUzSWIO zhttrwe)-scs&&}15o3%u8%}EcCO>^>0e}J?_SFvBVXRjR945@G~Spm2evrZ{93sDU?*$G9R$8n6{{6by6(b zhB8^yvJE^rV@+>H&_oB0q;($Lps0aG;r3fc*lO5+9CgLbp}T^-IW4}Yz)2fP?Ste` zcTU)!Z1iKslv__5P;b6PII20JpaTl)R+e>cCQul~Js|S-mxQv$q2PNgn4_P8dpbGq z1;MGEuv~j7NOozFu?o7EUlya(yh%}o0mZ?-dMlv#YfYQe;VjF4pUlwDYR-Mo>@nXS z(Zzs&`|^|{hy9wRKxu4lS7DOie&?iFg?9LqiHSZQm~S2VjchfK zH)xj0EDmUr;Xcj4cw}xf*bMq75c;nf2wjmL8QSM+u^rH22&JlAdM;HXueNI20oCS! zj?F9qVl4uC&5y}buG!^BZ8PrR#JC9SlMAhXM>xtJ2E<61R*egf2(LEr#?&q$j{~2F z(8Te)l#*&s#xt#k2339N`RHkRw3w15LiV@)TgeT9g41 zQFj<{xrSG^E|PyGoz=B((v=0C9pL~i$!#%De<$)iV!0DBFXc?0IJNVLdY1EmGS+hVQ!p}y%0 z6fE?_H|(l+&Zgv$&BgHzCuC7EC#+hXZ z;j(JJ(?oh;Ij4$xyMz{;U>2R|e)Gm*z&xq91~2N(H?+$c5?dpcE3)EssMZMB6aP$` zqD;}TDwf9MK3u8sOh-cVh3b9ws{Qm}6|~-iKxI;opYc^R|LcX+i9)q?P`5P%67XZS zsZ|$aktI}LHpwmjKAojs(Ub7m6@QEFhl4xW=*IY4?_~d;`)`KzdMVaNv*GlwhV@1% z*8g?h9n8-E8i;>?cL(?%?Jd9DO**a*tOp8y?Z@xr*-*ROg*+TSxn@~0-_)|w`Dw#r zz}nin;trf2Yu|=u&`+I02E`^#JqE2W=KAsYSiEgsl#duU{eC!OpVs83Mt{S=gMnY$ z0NgqcR)d_yr%@VfYxn(O5k?3!j0_1iw7XjWG2Y_-PqM4^hk>qsD(tH1$cLf4f_M~Y zr+N~y@l7Sfs~!_`QGNYJ1qvZf&S&|1^KCsMY#W&9p+ozJn6Pbhd!mW|d}ahjWa>LPQ~$=UKYs>#-347N%|X!XVbB{c=z<9^pln2-Z+s`8<%P5XDtIM9 zI=NR;H(y)bC~i*!8Es$g7Ny~G0mN$S5ikuZc}A)F(mbPNSuNcGdTHE$Yd^}3>5q;( zPHD=^m;((eRQ8WX_!3ImpxGexnwAfn6CtCp()KCB3BB28-pwn+r+=RwZtzY1{Rp=@ zKdp%^!BvrqQdbq^T^F;r#hO%LH5c)EtQPDwybk!?Lk4E0UEf^H-dJ5<pOoCh34cnV?Ne+V*W#9~zwE=4 zD|6C;75SWej)ASv-1ONih7zdIqu)9UMCrXneqr%e z<$I8!(0!bUJ#?URsBOG(<4j3~h&=&crs?3(-cAFw)R5lqrU!-7*=#b~O!i=IsMLf9 z=Xrl}mVds+pQ4quf6);5hTxS@Nh_{-|ExP4tu(L$Jv|29yo=OGH~QV99YGT~Y=s`8 zo8zE?HsR4@>XK(@2Z%yS8+L*b6O-(|GV^LSnRX#pxor68%}&GI7kQ&z1JVnhfy7}4 zLF+hTfvO9}L@O&WCK;g%=a)1;m^B9JX%|_4q<`V5rf1!}{~lI6_4Z^Ra`zLf#H2JY z3tsT=fOo_CEV~FIaWv6m-CzPC3y)gK-p+hD9iI35X_hJ9a}+r>uv%C`I7+c}kTj+9 zp$MW|j$9FDLTfyF_GCv)pU-0MY4H-0eQzgu_C($AJ{CX z{G9W>+GGz%g)_zNX{Z?#lYAlXs5xp*0HoIy{h7z#I&!Z@TjRq8Z61{5sFz}81fkmc zq1nF-=|7Uft-smICqs-O5^PnrNNQ61>E#Tb;OyHLY%TNkky@e@5jrvB z)zV?sgM9wVADN_Txz bool - ghost predicate Valid() - reads this - constructor (ghost inv: T -> bool, t: T) requires inv(t) ensures this.inv == inv - ensures Valid() method Get() returns (t: T) - reads this - requires Valid() + reads {} ensures inv(t) method Put(t: T) reads {} - modifies this requires inv(t) - ensures Valid() } /** @@ -79,53 +72,40 @@ replaceable module Std.Concurrent { // Invariant on key-value pairs this map may hold ghost const inv: (K, V) -> bool - ghost predicate Valid() - reads this - - constructor(ghost inv: (K, V) -> bool) + constructor (ghost inv: (K, V) -> bool) ensures this.inv == inv method Keys() returns (keys: set) - reads this - requires Valid() + reads {} ensures forall k <- keys :: exists v :: inv(k, v) method HasKey(k: K) returns (used: bool) - reads this - requires Valid() + reads {} ensures used ==> exists v :: inv(k, v) method Values() returns (values: set) - reads this - requires Valid() + reads {} ensures forall v <- values :: exists k :: inv(k,v) method Items() returns (items: set<(K,V)>) - reads this - requires Valid() + reads {} ensures forall t <- items :: inv(t.0, t.1) method Put(k: K, v: V) - reads this - modifies this - requires Valid() + reads {} requires inv(k, v) method Get(k: K) returns (r: Option) - reads this - requires Valid() + reads {} ensures r.Some? ==> inv(k, r.value) method Remove(k: K) - reads this - modifies this - requires Valid() + reads {} // TODO: this isn't really necessary, if it's not true // then Remove(k) will just never have any effect requires exists v :: inv(k, v) method Size() returns (c: nat) - reads this - requires Valid() + reads {} } } \ No newline at end of file