From c1b27a13ae2525785746ac6a05bb263a95afccf7 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 1 Dec 2024 22:16:02 -0800 Subject: [PATCH] Add a draft post on forward analysis Signed-off-by: Danila Fedorin --- content/blog/00_spa_agda_intro.md | 3 +- content/blog/01_spa_agda_lattices.md | 1 + content/blog/08_spa_agda_forward/index.md | 424 ++++++++++++++++++ .../blog/08_spa_agda_forward/plusminus.png | Bin 0 -> 42474 bytes 4 files changed, 427 insertions(+), 1 deletion(-) create mode 100644 content/blog/08_spa_agda_forward/index.md create mode 100644 content/blog/08_spa_agda_forward/plusminus.png diff --git a/content/blog/00_spa_agda_intro.md b/content/blog/00_spa_agda_intro.md index 601710f..cb9890c 100644 --- a/content/blog/00_spa_agda_intro.md +++ b/content/blog/00_spa_agda_intro.md @@ -106,4 +106,5 @@ Here are the posts that I’ve written so far for this series: * {{< draftlink "Our Programming Language" "05_spa_agda_semantics" >}} * {{< draftlink "Control Flow Graphs" "06_spa_agda_cfg" >}} * {{< draftlink "Connecting Semantics and Control Flow Graphs" "07_spa_agda_semantics_and_cfg" >}} -* {{< draftlink "A Verified Forward Analysis" "08_spa_forward" >}} +* {{< draftlink "Forward Analysis" "08_spa_forward" >}} +* {{< draftlink "Verifying the Forward Analysis" "09_spa_verified_forward" >}} diff --git a/content/blog/01_spa_agda_lattices.md b/content/blog/01_spa_agda_lattices.md index 69ebbb7..6fc1b88 100644 --- a/content/blog/01_spa_agda_lattices.md +++ b/content/blog/01_spa_agda_lattices.md @@ -79,6 +79,7 @@ a less specific output! The more you know going in, the more you should know coming out. Similarly, when given less specific / vaguer information, the analysis shouldn't produce a more specific answer -- how could it do that? This leads us to come up with the following rule: +{#define-monotonicity} {{< latex >}} \textbf{if}\ \text{input}_1 \le \text{input}_2, diff --git a/content/blog/08_spa_agda_forward/index.md b/content/blog/08_spa_agda_forward/index.md new file mode 100644 index 0000000..f9bbaf1 --- /dev/null +++ b/content/blog/08_spa_agda_forward/index.md @@ -0,0 +1,424 @@ +--- +title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 8: Forward Analysis" +series: "Static Program Analysis in Agda" +description: "In this post, I use the monotone lattice framework and verified CFGs to define a sign analysis" +date: 2024-12-01T15:09:07-08:00 +tags: ["Agda", "Programming Languages"] +draft: true +--- + +In the previous post, I showed that the Control Flow graphs we built of our +programs match how they are really executed. This means that we can rely +on these graphs to compute program information. In this post, we finally +get to compute that information. Let's jump right into it! + +### Choosing a Lattice +A lot of this time, we have been [talking about lattices]({{< relref "01_spa_agda_lattices" >}}), +particularly [lattices of finite height]({{< relref "03_spa_agda_fixed_height" >}}). +These structures represent things we know about the program, and provide operators +like \((\sqcup)\) and \((\sqcap)\) that help us combine such knowledge. + +The forward analysis code I present here will work with any finite-height +lattice, with the additional constraint that equivalence of lattices +is decidable, which comes from [the implementation of the fixed-point algorithm]({{< relref "04_spa_agda_fixedpoint" >}}), +in which we routinely check if a function's output is the same as its input. + +{{< codelines "agda" "agda-spa/Analysis/Forward.agda" 4 8 >}} + +The finite-height lattice `L` is intended to describe the state of a single +variable. +One example of a lattice that can be used as `L` is our +sign lattice. We've been using the sign lattice in our examples [from the very beginning]({{< relref "01_spa_agda_lattices#lattices" >}}), +and we will stick with it for the purposes of this explanation. However, this +lattice alone does not describe our program, since it only talks about a single +sign; programs have lots of variables, all of which can have different signs! +So, we might go one step further and define a map lattice from variables to +their signs: + +{{< latex >}} +\text{Variable} \to \text{Sign} +{{< /latex >}} + +We [have seen]({{< relref "02_spa_agda_combining_lattices#the-map-lattice" >}}) +that we can turn any lattice \(L\) into a map lattice \(A \to L\), for any +type of keys \(A\). In this case, we will define \(A \triangleq \text{Variable}\), +and \(L \triangleq \text{Sign}\). The +[sign lattice has a finite height]({{< relref "02_spa_agda_combining_lattices#the-map-lattice" >}}), +and I've proven that, as long as we pick a finite set of keys, [map lattices +\(A \to L\) have a finite height if \(L\) has a finite height]({{< relref "03_spa_agda_fixed_height#fixed-height-of-the-map-lattice" >}}). +Since a program's text is finite, \(\text{Variable}\) is a finite set, and +we have ourselves a finite-height lattice \(\text{Variable} \to \text{Sign}\). + +We're on the right track, but even the lattice we have so far is not sufficient. +That's because variables have different signs at different points in the program! +You might initialize a variable with `x = 1`, making it positive, and then +go on to compute some arbitrary function using loops and conditionals. For +each variable, we need to keep track of its sign at various points in the code. +When we [defined Control Flow Graphs]({{< relref "06_spa_agda_cfg" >}}), we +split our programs into sequences of statements that are guaranteed to execute +together --- basic blocks. For our analysis, we'll keep per-variable for +each basic block in the program. Since basic blocks are nodes in the Control Flow +Graph of our program, our whole lattice will be as follows: + +{{< latex >}} +\text{Info} \triangleq \text{NodeId} \to (\text{Variable} \to \text{Sign}) +{{< /latex >}} + +We follow the same logic we just did for the variable-sign lattice; since +\(\text{Variable} \to \text{Sign}\) is a lattice of finite height, and since +\(\text{NodeId}\) is a finite set, the whole \(\text{Info}\) map will be +a lattice with a finite height. + +Notice that both the sets of \(\text{Variable}\) and \(\text{NodeId}\) depend +on the program in question. The lattice we use is slightly different for +each input program! We can use Agda's parameterized modules to automaitcally +parameterize all our functions over programs: + +{{< codelines "agda" "agda-spa/Analysis/Forward.agda" 36 37 >}} + +Now, let's make the informal descriptions above into code, by instantiating +our map lattice modules. First, I invoked the code for the smaller variable-sign +lattice. This ended up being quite long, so that I could rename variables I +brought into scope. I will collapse the relevant code block; suffice to say +that I used the suffix `v` (e.g., renaming `_⊔_` to `_⊔ᵛ_`) for properties +and operators to do with variable-sign maps (in Agda: `VariableValuesFiniteMap`). + +{{< codelines "agda" "agda-spa/Analysis/Forward.agda" 41 82 "" "**(Click here to expand the module uses for variable-sign maps)**" >}} + +I then used this lattice as an argument to the map module again, to +construct the top-level \(\text{Info}\) lattice (in Agda: `StateVariablesFiniteMap`). +This also required a fair bit of code, most of it to do with renaming. + +{{< codelines "agda" "agda-spa/Analysis/Forward.agda" 85 112 "" "**(Click here to expand the module uses for the top-level lattice)**" >}} + +### Constructing a Monotone Function + +We now have a lattice in hand; the next step is to define a function over +this lattice. For us to be able to use the fixed-point algorithm on this +function, it will need to be [monotonic]({{< relref "01_spa_agda_lattices#define-monotonicity" >}}). + +Our goal with static analysis is to compute information about our program; that's +what we want the function to do. When the lattice we're using is the sign lattice, +we're trying to determine the signs of each of the variables in various parts +of the program. How do we go about this? + +Each piece of code in the program might change a variable's sign. For instance, +if `x` has sign \(0\), and we run the statement `x = x - 1`, the sign of +`x` will be \(-\). If we have an expression `y + z`, we can use the signs of +`y` and `z` to compute the sign of the whole thing. This is a form +of [abstract interpretation](https://en.wikipedia.org/wiki/Abstract_interpretation), +in which we almost-run the program, but forget some details (e.g., the +exact values of `x`, `y`, and `z`, leaving only their signs). The exact details +of how this partial evaluation is done are analysis-specific; in general, we +simply require an analysis to provide an evaluator. We will define +[an evaluator for the sign lattice below](#instantiating-with-the-sign-lattice). + +{{< codelines "agda" "agda-spa/Analysis/Forward.agda" 166 167 >}} + +From this, we know how each statement and basic block will change variables +in the function. But we have described them process as "if a variable has +sign X, it becomes sign Y" -- how do we know what sign a variable has _before_ +the code runs? Fortunately, the Control Flow Graph tells us exactly +what code could be executed before any given basic block. Recall that edges +in the graph describe all possible jumps that could occur; thus, for any +node, the incoming edges describe all possible blocks that can precede it. +This is why we spent all that time [defining the `predecessors` function]({{< relref "06_spa_agda_cfg#additional-functions" >}}). + +We proceed as follows: for any given node, find its predecessors. By accessing +our \(\text{Info}\) map for each predecessor, we can determine our current +best guess of variable signs at that point, in the form of a \(\text{Variable} \to \text{Sign}\) +map (more generally, \(\text{Variable} \to L\) map in an arbitrary analysis). +We know that any of these predecessors could've been the previous point of +execution; if a variable `x` has sign \(+\) in one predecessor and \(-\) +in another, it can be either one or the other when we start executing the +current block. Early on, we saw that [the \((\sqcup)\) operator models disjunction +("A or B")]({{< relref "01_spa_agda_lattices#lub-glub-or-and" >}}). So, we apply +\((\sqcup)\) to the variable-sign maps of all predecessors. The +[reference _Static Program Analysis_ text](https://cs.au.dk/~amoeller/spa/) +calls this operation \(\text{JOIN}\): + +{{< latex >}} +\textit{JOIN}(v) = \bigsqcup_{w \in \textit{pred}(v)} \llbracket w \rrbracket +{{< /latex >}} + +The Agda implementation uses a `foldr`: + +{{< codelines "agda" "agda-spa/Analysis/Forward.agda" 139 140 >}} + +Computing the "combined incoming states" for any node is a monotonic function. +This follows from the monotonicity of \((\sqcup)\) --- in both arguments --- +and the definition of `foldr`. + +{{< codelines "agda" "agda-spa/Lattice.agda" 143 151 "" "**(Click here to expand the general proof)**" >}} + +From this, we can formally state that \(\text{JOIN}\) is monotonic. Note that +the input and output lattices are different: the input lattice is the lattice +of variable states at each block, and the output lattice is a single variable-sign +map, representing the combined preceding state at a given node. + +{{< codelines "agda" "agda-spa/Analysis/Forward.agda" 145 149 >}} + +Above, the `m₁≼m₂⇒m₁[ks]≼m₂[ks]` lemma states that for two maps with the same +keys, where one map is less than another, all the values for any subset of keys +`ks` are pairwise less than each other (i.e. `m₁[k]≼m₂[k]`, and `m₁[l]≼m₂[l]`, etc.). +This follows from the definition of "less than" for maps. +{#less-than-lemma} + +So those are the two pieces: first, join all the preceding states, then use +the abstract interpretation function. I opted to do both of these in bulk: + +1. Take an initial \(\text{Info}\) map, and update every basic block's entry + to be the join of its predecessors. +2. In the new joined map, each key now contains the variable state at + the beginning of the block; so, apply the abstract interpretation function + via `eval` to each key, computing the state at the end of the block. + +I chose to do these in bulk because this way, after each application of +the function, we have updated each block with exactly one round of information. +The alternative --- which is specified in the reference text --- is to update +one key at a time. The difference there is that updates to later keys might be +"tainted" by updates to keys that came before them. This is probably fine +(and perhaps more efficient, in that it "moves faster"), but it's harder to +reason about. + +#### Generalized Update + +To implement bulk assignment, I needed to implement the source text's +Exercise 4.26: + +> __Exercise 4.26__: Recall that \(f[a \leftarrow x]\) denotes the function that is identical to +> \(f\) except that it maps \(a\) to \(x\). Assume \(f : L_1 \to (A \to L_2)\) +> and \(g : L_1 \to L_2\) are monotone functions where \(L_1\) and \(L_2\) are +> lattices and \(A\) is a set, and let \(a \in A\). (Note that the codomain of +> \(f\) is a map lattice.) +> +> Show that the function \(h : L_1 \to (A \to L_2)\) +> defined by \(h(x) = f(x)[a \leftarrow g(x)]\) is monotone. + +In fact, I generalized this statement to update several keys at once, as follows: + +{{< latex >}} +h(x) = f(x)[a_1 \leftarrow g(a_1, x),\ ...,\ a_n \leftarrow g(a_n, x)] +{{< /latex >}} + +I called this operation "generalized update". + +At first, the exercise may not obviously correspond to the bulk operation +I've described. Particularly confusing is the fact that it has two lattices, +\(L_1\) and \(L_2\). In fact, the exercise results in a very general theorem; +we can exploit a more concrete version of the theorem by setting +\(L_1 \triangleq A \to L_2\), resulting in an overal signature for \(f\) and \(h\): + +{{< latex >}} +f : (A \to L_2) \to (A \to L_2) +{{< /latex >}} + +In other words, if we give the entire operation in Exercise 4.26 a type, +it would look like this: + +{{< latex >}} +\text{ex}_{4.26} : \underbrace{K}_{\text{value of}\ a} \to \underbrace{(\text{Map} \to V)}_{\text{updater}} \to \underbrace{\text{Map} \to \text{Map}}_{f} \to \underbrace{\text{Map} \to \text{Map}}_{h} +{{< /latex >}} + +That's still more general than we need it. This here allows us to modify +any map-to-map function by updating a certain key in that function. If we +_just_ want to update keys (as we do for the purposes of static analysis), +we can recover a simpler version by setting \(f \triangleq id\), which +results in an updater \(h(x) = x[a \leftarrow g(x)]\), and a signature for +the exercise: + +{{< latex >}} +\text{ex}_{4.26} : \underbrace{K}_{\text{value of}\ a} \to \underbrace{(\text{Map} \to V)}_{\text{updater}\ g} \to \underbrace{\text{Map}}_{\text{old map}} \to \underbrace{\text{Map}}_{\text{updated map}} +{{< /latex >}} + +This looks just like Haskell's [`Data.Map.adjust` function](https://hackage.haskell.org/package/containers-0.4.0.0/docs/src/Data-Map.html#adjust), except that it +can take the entire map into consideration when updating a key. + +My generalized version takes in a list of keys to update, and makes the updater +accept a key so that its behavior can be specialized for each entry it changes. +The sketch of the implementation is in the `_updating_via_` function from +the `Map` module, and its helper `transform`. Here, I collapse its definition, +since it's not particularly important. + +{{< codelines "agda" "agda-spa/Lattice/Map.agda" 926 931 "" "**(Click here to see the definition of `transform`)**" >}} + +The proof of monotonicity --- which is the solution to the exercise --- is +actually quite complicated. I will omit its description, and show it here +in another collapsed block. + +{{< codelines "agda" "agda-spa/Lattice/Map.agda" 1042 1105 "" "**(Click here to see the proof of monotonicity of \(h\))**" >}} + +Given a proof of the exercise, all that's left is to instantiate the theorem +with the argument I described. Specifically: + +* \(L_1 \triangleq \text{Info} \triangleq \text{NodeId} \to (\text{Variable} \to \text{Sign})\) +* \(L_2 \triangleq \text{Variable} \to \text{Sign} \) +* \(A \triangleq \text{NodeId}\) +* \(f \triangleq \text{id} \triangleq x \mapsto x\) +* \(g(k, m) = \text{JOIN}(k, m)\) + +In the equation for \(g\), I explicitly insert the map \(m\) instead of leaving +it implicit as the textbook does. In Agda, this instantiation for joining +all predecessor looks like this (using `states` as the list of keys to update, +indicating that we should update _every_ key): + +{{< codelines "agda" "agda-spa/Analysis/Forward.agda" 152 157 >}} + +And the one for evaluating all programs looks like this: + +{{< codelines "agda" "agda-spa/Analysis/Forward.agda" 215 220 >}} + +Actually, we haven't yet seen that `updateVariablesFromStmt`. This is +a function that we can define using the user-provided abtract interpretation +`eval`. Specifically, it handles the job of updating the sign of a variable +once it has been assigned to (or doing nothing if the statement is a no-op). + +{{< codelines "agda" "agda-spa/Analysis/Forward.agda" 191 193 >}} + +The `updateVariablesFromExpression` is now new, and it is yet another map update, +which changes the sign of a variable `k` to be the one we get from running +`eval` on it. Map updates are instances of the generalized update; this +time, the updater \(g\) is `eval`. The exercise requires the updater to be +monotonic, which constrains the user-provided evaluation function to be +monotonic too. + +{{< codelines "agda" "agda-spa/Analysis/Forward.agda" 173 181 >}} + +We finally write the `analyze` function as the composition of the two bulk updates: + +{{< codelines "agda" "agda-spa/Analysis/Forward.agda" 226 232 >}} + +### Instantiating with the Sign Lattice +Thus far, I've been talking about the sign lattice throughout, but implementing +the Agda code in terms of a general lattice `L` and evaluation function `eval`. +In order to actually run the Agda code, we do need to provide an `eval` function, +which implements the logic we used above, in which a zero-sign variable \(x\) +minus one was determined to be negative. For binary operators specifically, +I've used the table provided in the textbook; here they are: + +{{< figure src="plusminus.png" caption="Cayley tables for abstract interpretation of plus and minus" >}} + +These are pretty much common sense: +* A positive plus a positive is still positive, so \(+\ \hat{+}\ + = +\) +* A positive plus any sign could be any sign still, so \(+\ \hat{+}\ \top = \top\) +* Any sign plus "impossible" is impossible, so \(\top\ \hat{+} \bot = \bot\). +* etc. + +The Agda encoding for the plus function is as follows, and the one for minus +is similar. + +{{< codelines "agda" "agda-spa/Analysis/Sign.agda" 76 94 >}} + +As the comment in the block says, it would be incredibly tedious to verify +the monotonicity of these tables, since you would have to consider roughly +125 cases _per argument_: for each (fixed) sign \(s\) and two other signs +\(s_1 \le s_2\), we'd need to show that \(s\ \hat{+}\ s_1 \le s\ \hat{+}\ s_2\). +I therefore commit the _faux pas_ of using `postulate`. Fortunately, the proof +of monotonicity is not used for the execution of the program, so we will +get away with this, barring any meddling kids. + +From this, all that's left is to show that for any expression `e`, the +evaluation function: + +{{< latex >}} +\text{eval} : \text{Expr} \to (\text{Variable} \to \text{Sign}) \to \text{Sign} +{{< /latex >}} + +is monotonic. It's defined straightforwardly and very much like an evaluator / +interpreter, suggesting that "abstract interpretation" is the correct term here. + +{{< codelines "agda" "agda-spa/Analysis/Sign.agda" 176 184 >}} + +Thought it won't happen, it was easier to just handle the case where there's +an undefined variable; I give it "any sign". Otherwise, the function simply +consults the sign tables for `+` or `-`, as well as the known signs of the +variables. For natural number literals, it assigns `0` the "zero" sign, and +any other natural number the "\(+\)". + +To prove monotonicity, we need to consider two variable maps (one less than +the other), and show that the abstract interpretation respects that ordering. +This boils down to the fact that the `plus` and `minus` tables are monotonic +in both arguments (thus, if their sub-expressions are evaluated monotonically +given an environment, then so is the whole addition or subtraction), and +to the fact that for two maps `m₁ ≼ m₂`, the values at corresponding keys +are similarly ordered: `m₁[k] ≼ m₂[k]`. We [saw that above](#less-than-lemma). + +{{< codelines "agda" "agda-spa/Analysis/Sign.agda" 186 223 "" "**(Click to expand the proof that the evaluation function for signs is monotonic)**" >}} + +That's all we need. With this, I just instantiate the `Forward` module we have +been working with, and make use of the `result`. I also used a `show` +function (which I defined) to stringify that output. + +{{< codelines "agda" "agda-spa/Analysis/Sign.agda" 225 229 >}} + +But wait, `result`? We haven't seen a result just yet. That's the last piece, +and it involves finally making use of the fixed-point algorithm. + +### Invoking the Fixed Point Algorithm +Our \(\text{Info}\) lattice is of finite height, and the function we have defined +is monotonic (by virtue of being constructed only from map updates, which +are monotonic by Exercise 4.26, and from function composition, which preserves +monotonicity). We can therefore apply the fixed-point-algorithm, and compute +the least fixed point: + +{{< codelines "agda" "agda-spa/Analysis/Forward.agda" 235 238 >}} + +With this, `analyze` is the result of our forward analysis! + +In a `Main.agda` file, I invoked this analysis on a sample program: + +```Agda +testCode : Stmt +testCode = + ⟨ "zero" ← (# 0) ⟩ then + ⟨ "pos" ← ((` "zero") Expr.+ (# 1)) ⟩ then + ⟨ "neg" ← ((` "zero") Expr.- (# 1)) ⟩ then + ⟨ "unknown" ← ((` "pos") Expr.+ (` "neg")) ⟩ + +testProgram : Program +testProgram = record + { rootStmt = testCode + } + +open WithProg testProgram using (output; analyze-correct) + +main = run {0ℓ} (putStrLn output) +``` + +The result is verbose, since it shows variable signs for each statement +in the program. However, the key is the last basic block, which shows +the variables at the end of the program. It reads: + +``` +{"neg" ↦ -, "pos" ↦ +, "unknown" ↦ ⊤, "zero" ↦ 0, } +``` + +### Verifying the Analysis +We now have a general framework for running forward analyses: you provide +an abstract interpretation function for expressions, as well as a proof +that this function is monotonic, and you get an Agda function that takes +a program and tells you the variable states at every point. If your abstract +interpretation function is for determining the signs of expressions, the +final result is an analysis that determines all possible signs for all variables, +anywhere in the code. It's pretty easy to instantiate this framework with +another type of forward analysis --- in fact, by switching the +`plus` function to one that uses `AboveBelow ℤ`, rather than `AboveBelow Sign`: + +```Agda +plus : ConstLattice → ConstLattice → ConstLattice +plus ⊥ᶜ _ = ⊥ᶜ +plus _ ⊥ᶜ = ⊥ᶜ +plus ⊤ᶜ _ = ⊤ᶜ +plus _ ⊤ᶜ = ⊤ᶜ +plus [ z₁ ]ᶜ [ z₂ ]ᶜ = [ z₁ Int.+ z₂ ]ᶜ +``` + +we can defined a constant-propagation analysis. + +However, we haven't proved our analysis correct, and we haven't yet made use of +the CFG-semantics equivalence that we +[proved in the previous section]({{< relref "07_spa_agda_semantics_and_cfg" >}}). +I was hoping to get to it in this post, but there was just too much to +cover. So, I will get to that in the next post, where we will make use +of the remaining machinery to demonstrate that the output of our analyzer +matches reality. diff --git a/content/blog/08_spa_agda_forward/plusminus.png b/content/blog/08_spa_agda_forward/plusminus.png new file mode 100644 index 0000000000000000000000000000000000000000..cecf094dbea118f4b9ba840d514bc2c58b1c59b7 GIT binary patch literal 42474 zcmeFZ1yodR8!n6rQc8z3GBgO%Ff>S)q=1A-ca74ZFo;M=OFJSWEiEmfGzyhwlnP6``PzXcV5>Hzpklt5sw-V0|Votit;rb3=B*d z2F96(IOo9`MyqO142%oX_VV)ARpjLvuY0)K*gIKcU?_(t-oQ50?WD-O8TVMm4xxtI zfXk$FRv8x&I!^2aXO>~-J0JXr&Q#Cs8`D`~nEth9yoYq!+}w{Ecqzyd?v&oTG5-8s z@nP34>%`dpW`D|Qx|r8WhB(H{jG2em#9l%%YFhl=onA=?n0Vl2d^~q`FZ+z=)Aq@^ z@FxQUlNd>eoz>Yd7w;*L77*wZ1?`*;J!_txcRwTZ?6T(cth?uBDI5&5x8&iQXBbs| zHtqMBI3AGOgmAXXeVB`7w|RURH=EjxyHFAgsZ(uX0l%|Ek%HFn`8VuY|X z{xKWT*{6zOpV>sb@Cc{$9y&jb!nvI%1^I@Z5!qz_;-aI6C{?SW6s3_i9??v=hp50w zKkR5VE)7DpVS!bk`a+c10BZZB`sT21%X34lDJctME3&p!q9CF*s~w{31a%eV;4ylk znYq$iefJ33G$k};F10-%!p8MvY9;qKu4R09k_axSZRY(AKaaPA{}1tIqi3bgTmC?Rdg zl?;hs=)gIn9kG{Zt!{9<|zFZ zhwJ%LH8a`t+uWH?2q~YNFlbTEDz$e{x8awIA_g|R*T@-ZU&&xRJ%?Lpe+#eUY;bhr zJE=XbaZ*fCnG5_F45I8$5X35F^q1@3-IrTqyXOB`M551pup1le@hP;YtAv2jbnqr4 zP3*-?xpe#%8G<9;*eDVLKQ&A(M#x^67eS%PC0ByN_a{O9gryTytX3`LkyafLQ|FGj zOUf4*9}tB+ta^QBCB$!Xa%~a2K%no9ZppXd1*`Ae@J2@XlmDbYKQxHTHJN=hHv9zPDCcWMo+YNN2kekHt2c9&lK zk>s|}4LhOaBF5eCV78Kibfx3-J6F_nwZz{8S(D*#uVk(K%Vtlt@)+ULaOok0z=Bd zuz@Y1W@{eOod`xE^>!b6@o;^Jh{CT&EUMx$_p( zh$q(-KWmC!6FrxeX=L+TPE{e5(ZLiW#%}k&deE& zM@;U@`_FH`_kHj39``-Dj>tktTv=RrT)EC;okwxk^OW<{?UUcT=Wwa^CrHJA>P)iI z@*qo5%9J(J99MKPp*NpzkT3kwOgkV?(V$$Z@sv2CmA)k zU^Wm?A|ltX6;pEK*^Lq})75w>Q|ar{H-mBlvrhufjlJn(e0M9gSusT5d;p|E(L3sE zG&@ykP#c~6M`YjCLAMu^2Ca8n&p<4*Z$V-Qe6v3&2E2p53w&qv&M`8EW;Ye7?yru? z>Zq>yL?YMmL&_GduUJFkxT}L5^=(eRFSkc54u*S1xSI<*3dffl#one{WV$rItAATR z(bC4$ayv<(=q;UE8A~hw2agQvv{^qc#{%X81%oI9$wA*irzN>1<0U^~JsR`0JmF8m zLr&pU7e<{%FIFXgyDomCPQ6aGPHpF9Lt4X|z>t7>Sy5-tT5)4f7z*`lpf}rGd{oRcgDayX3K5M< zE#Rg8;mHl29UlMWD4uE)`(ona2$P#8O|><3;a?WVe7{^7)BRE~=E`4jX&^Eu(vu#O zFes*mUP)5Qx7KIQZ)NwWyStfd)G_%+zu{8pQR(PAsU6|XId9kXl?}w<^8=@yg$<$Y z**$|psSSbM>3!#2zjqbZHhf+J<_F^Y5yyo4O}0K|HszY!tVN8)h_mJeDA*s-ixe$$wSK?Pz5E z3#kbknbvE*0pF>u@Od^W^{y0{Q`v}B-^{r@_{ZlTP4mn}wbLE?WT?f9IE%8nr;4W= zzwWOOuKDhdAL$?2E{rb}y!Yd;7cj8hvN^CxvfjZp4906ND12O~VYFJFUFKy)ILAEu zah`Mb#T-3_173M(k#1zJde(c6GD`A@+84f>rs9?6w5;QqVKW*%j$K2+3>)7_XgYc0 z!my;U60sOwuxN^3HMOjD^F6#!N2O*X!F7T2$eC3tUcB5oX`yhxoW9SdZ=4@HC0;n! zx_Eyq)U$3LtAA81i(lIBWK}^^q2SRtkFqhc9%(mO9~u*cdy-RSSZQeD?-@JvOe13b zZ7^8K@3@VcW^Uq^%*f^G+8Zq-=Zxi02GSin?w5pgzfZoy?RB%!9m_q`?QK+IBbQh4 zdqe%#i|dOIKV5W0IjRoUn~M8<+viU%(^z6(VqU84YVA%Nyjf^odZMOa^LAVHwCjMg zHJ?R)Rb)-rWEfRl>JmTj;=M+eFuw4_2uXboVkE!TiOb!wc`$dBq`LC>-CmJRUGvWS zZ{}V&Ua)VGUxtmR&2-DV-G(-dD-3i->-<_)y8X`X2!0a#=$to{$NL3;M|DSPBDr?; z-N~!tE7+H?7YU5%3!&G<_1@nT?6E_+_Bbs&sJbjl(E7g487|mI61PLdqf_aNBwhqK z?YnoahqhyDk!4;I<$w-*aZZ1nPU^hkr4=I{P$cxCa$5a!il=QzU#5#?Rfgz%zzWKz ze>05tDvzKUtnM>%Wh4;gH8eqZ=k*;y6OX2ku;FPB&-u@N(>MG}(rc;RwwHx=DkFv< zC0^souicmC;Ay7S-qpS?^J9T`a=-S?*KMv4uOyD$Xfoe@Wucj+?{i|wHsG!gLvFoMZbl>ONX5|K4 z4&XR-IIP^i`MKIJq$VVUDf$WIknGJZg%2OjcsHEGaNx%f^p?twOwKyB!ivo@vc@@L zI}{A-xbfWW1Rbb{wxMYm^}vOk83o+C;H!GaG>w`?ekpR0}O2N7YR7LpPv1B zH74xoxu4(9JOsaC$m+_gsDMvhOAl*n7f(A^*as-B0XTu{rfdWP9SRooaYjXlc@4Bb zWUprkGt^LrTDm&(SXjBj=LU!ARC7L4A`PA;BMZ%L-_S3tpc^l4ru z#_yNF93`0yHLf$tyLwnN3iDj$xymGk$H>Si;bCP1)w!nl<96_uB$FKs<_6{E_44xK z@e<&1^|0mT6B85Ty~@wa&wmA6amCZe1!m!W#l;iyTO&W)xn}KY>0$2%vv+l2M7L{k z+w~4il8FiZpx^)fCa1Nx{U1+q@%+&(&_Q1GFT8v_S9yPL8{8^^J`25W?``d5bj{uw zj2U=_lzTXDZC`i7pY(#Y3;9R>48tM%D(?=1OKyw1N{jO ztwa1%<8}-T84Q(cvU=WUmNW2Qk-e?CM?*fqem3|K^)-cuaZj1p8z0^#^0$yBOT;7g z)P@)<;xXLPJBzD|9J}Rz{u!Jk3X{CVjzs<%DK~>G)5|?MUS>sw>sKccL<2RO{k<*^ zT6cysGJ|aWcKmg7dKMO%s^^!+GlpILYSXYLZ9X$%oWYU7I7@U71M`=!9`aAA&y$WEgWZPR~fl<^)CLHPG)F=E_LCze6Y6gI!)`BjFW z;>e(o*gwDj`b?QV97dSO;4MAMze6HNgFE2_0snLwXC@Luj?MO> z;+=mQdJMTRsehOe3``G23`BhS`Rv+%>NJ=xhF^#7cWM7SUB3*=f2ZsBbwPCR|G&FS zrZ=>2Z+*IV;$){f-Qtf8^O{KXWN*5+WAVe5dBnn8;W0B@OcGwU#NH9tSs6#ZS=1h4mv$9 zY8U&tb7caE_l{SCTo1OF=HIG((nCdF;%kvOKxNN)H63Qy50~Xo%4`^iZ!Zm{#cM)4 zX}!kW=MI)iczvj~B-Y_nA};AvlD-vGS8vI5N-!H}-kRx%wV7-Qomjjq;IGp+Ty27aip z8)z8=V&0^KT&B8@g->y5Uw`Rv;yE=6tJ88Wra^j+lG9Gy5BTrTV85h`*WH}`LSaPdXZ>B-!Z`Dty<4T98c7xgL8#25c_K zT4hPV6}zEgQ|pw@Pwe-lPxt$^Cujw1)U)?R4XN(02JY4o_vff38&F)IHF?oBD`G4m zm#ZxiPQU~snbhfwL~1u*A`eCmSaPsjhQWN8U|ZhcFdVd0!O3vCNsh?wrU3^jBD)=Z z=%~t}+Q0?3uj;HY!F0~TaFkG@GUaea822sOcw%VuS8fX&I{ZsvR`BR^6|7{z$j+)# zVrXqWI3$RnzUYHHhZ(LJX=?`86qVL^W&h!YVej#%0?KNF6^Bl84jf53Byvj0Y;sC5 z=)?Mb++eY3njrJ$5s)Yr0)#{#KLu3ZU2%_!qJn{Qhc>`H)+b@$D{-xf> zbNRy2FuHAue{MU6B{bgR{KUavb?{)(O{LSulY^zi2R506i1;fW@Ms=aaA?7!>CuN8 z2QGqidZ7Thzx6>Y#4Ys6Q?+Cs+1I|>f(xm4SloXR|MJgb^S43umrYmYFQ35jEth%b2J@;E^|Jv4^$q?#dTKgJ^x3r(pltw9|PBPCA?? zpV7=xkkYlnwb<_&f9;;lZT7ekNx}k`)_Jn_V0i5As52{VxG_^$;CrxfvaRE+?HAoD zFCJ6AlntLGlm=3FN$k(W3wduBnd_`z2cB$ZrDYv2+s=g$N?q+u6A=N6!N20d9>d96 zm|f>;ztkbO!)7c*DRu4L#|o!mkELLT$0R3DY#tCYxPXCtHhV`+-(u}+^IS7FgWx3R zjTg?NRo_Q}cb9+C(wmjc|NA44)>?(;lXmgcGbM)MB%k1rgWh{*&V5%zLDeo_p7p;X zlshT!Sx6*d{Q=UBG(~l8Iqe_QFvF(q#QT_vu z@uytsz8TOwC9lt4l~ZcOX#|Twkq2J4To$n~Qt8Ni%qd#gQ_cv3ecxh(awxQh9Eib5 z#LIBA%EMK%x+Wd1cfjH`>Rc`4(aLQuH&X3dg5Rq{E!Tcl@v;$f%kl1n>x|8DQT6yE zsohqV#@>g-5cL>($wwux>;{-T(N-di-nXNJ@}R_jmTL}e4#buU%N4>){b=g>Hspu{~WmkI22%9-z zId`RO#Ge$Z5jeadGVTo#-5v7`SsNOmM$gpq|D^3cj$ZA z%raTIG_}+Faf?npgaluIk9D|QuC?`fwr;g?)b6E39C`E%KHB!MYp&S05K9PsliuFw z&^KGL_79xljM?Rv@c4vM(wqvB@JPIrBE$$D)Y;HYe#3+quJsLbl9XuBbA9rjYmAAI z5dzX5t(F_h+u*m_;6-!-CFeG8l+b2~ji!`(PXsr(`q@4=BN)kyJxR3BNZXbEk~XRb zhwkE|&aO3W6kPr!vq~?a@Bx>sGOuQCBOM84sE1|SR>M8F+j9Q#DZ2&DUVl8$<`6w*gJMMl}u*tBjk%$`)jUvZAgsM14UdQH3gXc)4w1F&Rp7 zZ0WhIk2lK4iJ-$IyV|IkeXt0#M}z)sudak@7E<3SjX-ubQU#DeH!j^0_3?7IipI$x z)fBbBH{$S_Ij8(!rrVt=lUIHv;4=}lw&>n3TAzbO-|@M1W!Dw29h?jgI4tIn6}Az` z8-g78mIaJc<`2Wi_Kp-m8WQV4iHIk8D*swbPH9dH=LW~{)Ih%5?T@I~H+y-Z@r2kw zr5iHCTEcTfXk6?00$vUE=8tE;zrL z=RZueWD*=0dVMe~+iu@`)bvvdV9Ni}BVM`rZ`BjgbA7Qj?x`ZK^l-HWEU+W|1dVfn zUAtdcMLc0e((5L+hkC7!$5W8{(N`XYs*<6H_eJnFUg}7<hVNZU5960v~ zZBS!??^5Qhp9R;H90ThNb_km7bFThE0bBgYaY@+8kTK@MK`roaZk`7wJRBL`tXva; zRKZ1F9-~BTqOxPoi?7yuGTQ+?NU7oA^InBbAsaTs$4%8jJ7EDO&U4Q0Fl4wp@TP7(A5%a*$3zjWL?CN``;i?HjzeuU>@Zwr-3)Xob<|+2Qpt=w zTjN1zZdM?5`rQ%xw@MXOLh-<=_1wQ_1}5XL{>9&hgBM(b_NCB%Ncj4-UmqHRB-Zvk z*`HVPP=srim^B3J7Z@nSyn-!%=A#bv{CXeze0MT0ZziJc0)tfjr4MyptG7T@@OHZL zvn&dwql7|jTtlHilc>_d_BgPCs`7c|a)Ay5%m0}2PhKM!h(gmk;nzTwhX7kVc%GP%ZvaVzn%{_%;aigoB-}CollPVa9>aw}=Q9&43*3@( zDSmB37ZLFR-Fu9%=U)!D7Iev=Y+3#u?mEJ;qD-DMrChP%Og>hm2+uEfhR8#sBWGee zaU5&FLR$FM2mRqJf1*U_0*3*I?#oHU4_6QERNn?pFW)5&FJdUi87Taa5oSR@HErdJEWn$_-KUb~#n}F&F6T_%eZK9GL(HI01vMC4dOZ5On13Hs;BFiR%`d&qQ z{C^fS3m!douB##A8?}>K$@ar$(Y-+Hc|GdK1RZtzbDS?f5nsQuIVarHxW^>XH7&Ug8B)9w!F>HCbe~QVc4% z@o=RMyI*qGL@=xm_*0Mg!WaU*UwO=S$ti1`fZ4wNpX|T`W>}k5_bV|UE0&XqaJI}# z%e70z1KDTz4=x9)@61M&s;8SQq4xtm*bmgvRcOC(txtTF%%UyEweDM0Ge~uWXru{a zg8)yXQiX9Bviseg_M=A$PxxVEHYV zD!sbZe3r}BKEl`)hpvG_2CU|aMCMg0pEd)jQJV2`!K0h>-P`u^VEa;o?Yr0TDAK!Q zsUZ?rK;JmGO4AVM1t}9x{MEByygufX9yX($`+x?y+8};+mTcP!N3qnE!O$1)Yz_pW#@cm zIwt7Il9?rEg8t4&?SV%Ip%$3-$wH58e$ z)ouyU=yT4)jwKCD2uOEAKS){Nzh%JUdxLzeo&|ZfTxU1_trnO{BTOEyr zT-0c@46giNbsCiN1A$9_zD%$tvQ`ZBG$h!%JIUEyaYI?nf=tVzqoE@MxCh=``{fF^ z6obICWdBJ)gLP_~x%)p=l_XGp;xcaHD{+d7Q<1b{{HaH;-Hd63op3azkGD|XK=D~s z^h<22UslsVYuu@S+JmlgY^(oMTfhu^egG0b=EySZZo7oOXz`UxCU-vRH-oIeGl84c zE~bLiO02RJz%=?4H|!YmD$Xlo5ks{F@{S1+*$?ZXw7 zaal-=-Yh|5X|SmGscZ<-iyTfq&pCCVricXYEb5UK-_z!d@Ew_Y8`0YoGx2#Z4!^_7>Mv>TgP0ymK5K{T|%X`CkXkl)SIpipWtUZ z_O}JkwVKbWi)xos2|GPWkqW4_8PF&zbf12g;uh{J5Om@X92Hkyst#NEy$+a2dCy4Ad~vUEj9~P%Qa-qAhMq+ z>bqq}`sf%XZ~`aQTq{l0&fuv9p!V`&-C7-P|kmB_um7 zd8T!Dn=gut5p_TerJN&?1I|$r;D5>K#iXP#VyIdYH!gwH-q)|ibu0NikqJ2hAh37? zCEUFO*K8Q?-V>Ems`WNowZ4SNK0K2MZm6|2X?VYJRZgkzgtBQ*0mi$zSWsd>_&^S1 zB*VoDLEGW_LrbRSN+|D(SFC6KX%M8+bW~B0CW@xD7W@GeJ5@NO3D&_o&7ay?9R=FE z68BrHU(l`Q)?#j{+5*q7+n2j@h#0!vVcgf*P7HM)^r=g>fNR!ozh9jPp9keVFW}%= zoe$uB1y|+RY~F&K*$hleyaMPD(?S&qiJQP#@6ydT5(VmHKme#OTY5zlD${*i71;6Z z&x7)vjnT+F?5do;X7HSx#ndoC@Ou>r1mscYtl`n)R5z-b(Lz1Z~LZ_+)wILzvY964c_9X|6Jw&UK@7l*AwepEf5_TgTj z7VL-we!okf$JQlCv5wDB(=b*W2n`BIxG5rs~Y-!KpOMC<+azGC2IYc-`?>r-!SKnml9R+iKY zqjH-CJjbbl4g6i;(L3&pd1`qgWwC|asTZ`&8*g<5G4%j9ETi!as~MPgbjgDjgpAD8;c*!hUM*=lsReOVfj!6+ zb;cW&S%ssM@(W+;M0TTDaP>0{I~y!#b7D6^_v(C>imH1+3Bn1)UD%HkFwsSXlkJkA zPra2)EYW(Cjzh&l_>???bmDgfGoW`=^(mU)p~G}^xx!}bwY$xbsaKI?+|vi6B2D|f zjLbxE5pSVFg@F1k>67)ChqJ(uD`bO#p;hvEp_$>(+j_qX*MFL3;-PmS$N(i`$CfkS zZ#w?wO56>S<%trSxB1UXgK8#ICSpc|LU|<)v+-z_7aMpMJU)?aR+ug370(*Q+^5>C z?$ggF9X`3f>}S$?r1x#5ZZ-O#9mH3KiBg+A0@)G_0b8-?x+!F>Kj=i@wwT-3H(h5t zK(#XKWGk1rU(9n(Ff}G5k$7)psF4DGyRfWh#v$PisC&-8bd9DGcroBlTNwEUl(WA) zwB57Rv_7NXXPs{nnEe(4qkbEYVw7Ve=1Bw@ZSqL%%Rkbne~&Z%UQhdLAP!2Ff@(OR zobis23Nek-NAdt!de2>15mY!GLNWiR3Fc2fto8 zIuIa~W7AsQmH>5~df*pT?iY5boxTK3B==X>gOetHn~boH_ad|L{NPI7tRf#`sE6gFN^BQ5ErrgQhUd3`_m00iAWv_T>$?ybbm)ZF$AVyHE>z$9?Dchof z>Ky;dk>vpB0y0Kc_Opn141*LP9{)WO`aZRZgb#8kW~VX5GN1+SPrKoO=0G{=_sl*m zVj82DBpAJg)xj1HE{9)6gB0S3p#(@W;O^oPk&?wG^Y()3+EZ<=j;{Z$-3G1w@0BtV zse*h-Ze@UMegk2!R#L%cW?xLVdAS?e%l^`1Fe$NJ1 z79Cr#g2mKq)PfEd2tc@iZHEUQh4m2kQAc;OjUtNK?jv3qzg#Y$SC)Z--y6<&a)j>r z>n*K7!mDu23yNK)a81>F1e54nlZeofh9!tJh|^gvpre?_Ad0#7f+!fNeecOr9JuCL zLu+(v=x%NTZBYRh6-{;QGERo#S5aC}Jb4P1`o9B35ex;7I@^Y+Ff*$r0D+MRI$#-5 zA#~3?$29tFojyWxoMT6?(F>P;EsXsOO{|L}i(;2izm6%#cBYUY-5R=^J_~6c#yA=9 zs8Qv+a7~CCEdh`a`Je8cjg6d?AGCPhDWDS0B&>lD_56kZwapXxy_=Ku zTN+|l;F>M(oSDVta*0I=!hnQ!|LG#~*?->yjU!f|wn4>+`8@<2kt|8NmKtoOIKfoldU7BO-` zKj?)|4L{kPo*T0?g;J-Lx1Hx#Mz`St%34a~%A zo=Sy?|9??kc8DN8sP{F0wELO31dh8S8u!GX_x5M*5tP%M8~3In%1ZW!ZL?BB@hKJe zf%9MwipyrgXb=CpdkkQWFZ^~_tT!F4aDuG)if&d5hn&Co=t&YMfYPPdbUeOnv-mM@ zE*PJOJyAij$jk@-Wn;i$s?X+J%9>59Q+coO;xaV_`|&oY$OyzpY&;wWu%*12BCge< zCg2s@G#&2zw%a#E2X!qbEjSUDp%*xD0!a*^v zbiY$8@OBcn(QRSZaTD!z5J(B>4AD#a>a{6K;Tr>d(D!`v7^g3BsQUD~D1qtr7?I8S zevt;hT?6(~f8y;UvsEM_WZ1o(E~+Ak;-+NN(0pHpbdKhMMI4oPeAF-M(&KY)X|#!Z*fe#i5Lo20G?vxCE{fePwIbb0`Z~<7FQU5w@ZpPhw0KsR$Ri1Df zEKC7qE49vPfYX;+oQ7w7o@1>6JYX8g zs-*#aeAQW7L+S)whwDzdA^=bTX~UK=lBp6g6&L_25#YJjjGfla+cZ`IWOjDXn+6%t z=Q{wN_Qa^dPJ59Qf$=lVcf{s48A_Q7Fs^&%19*vT!G{R2=`b1mN0Gc@fU*Phg4m$Xd)zcPE z+S?He=>;GRJ$}OQMAFv)-wL7HubVjLIoNL8Q1%dJX3SRU15gUjsc<&Ms=7({6HUdh z<9@3`8xvZA8>EVlS>$i`q? zDA}3Z!kzUYlq$gmr8L3p88_;;7P_ecI z0F0KH)J6+UjN{CT5rcIJsK$ke!QzmdS;^?X@&%Q=&oRgNU{A*2CqD4b(&_`~ZK?4g z0YY*s0)YGv7Xu)BfiM7np93&}PTKFd{fRjwUu|x3A#lR^&7x)%QG$xO&~{MPGWmh) z{{t-#DsQ-mc;^D9f5hwmn@;>790cma!or~LCh`k(;O{WDe-)r=uww#2EYWy?Uoio{ z5eNQ1AxI-`Mk>!uo^B^lH5WIID+aZWPbNJDE8PUVT`vHz$_DvVmiU7Xo5U{_c-Q2J zFBSH>70;c^ZF+m)xTHN`&zdjl)hjQJR+prJG}!(Tplk|{I!!BN0R9g^*s>Y#xPk(R z&B4}!kK{$y#Vcwrq8X&6j7O@yR>#Lba+Q!T{O~4wftC>v!`fGm%}JRR@B_YQnYXOI znHSjo5lNLz->OD?%>2ITCl1*eqM0okrzgi6uepn0bT{;XythVyK~c|}`{$y#YkHHS z-~7eVd{3@eu>eZt`@mK00Z=HMsNb^We?aZ4ZokFzT*ygIO*Ri4b{em*;pF8QnxMF1 z{KT_QtQ`$+<1Eq6M@I0}cBrTDv()k~gAU|zr@Xifqi#NaOKJWD083JuK-ztPaz`@* zx?eiz9}XS*CoKJx)3Ne~DXN3A8B`dAYKc|=SLp@F(Z_CWhKwgw%AlM&A>Yh#GAb~u zBTGV&H487&dVnv>Nde6YJjnA|ZP<-G64hBq9s@{K;aZC%-pk)ct0y*|7i>|=<*MGI z;Skmu3PxuTYmz%dke#{!Ya+NII|DLZ=**T5J_5q8i8;?zQm<1AK%5LxcW$@D4xq^% zuhM&i;_&6>3(NcXfoR)71bROGB8b+qSr)}xMdnRXd&B*K6tIQ&EI3ML9a`A~L6g0% zNDx(g&GcKrZ80}jy*9{`XGULxH*q8j)?^5h348LQ_P2WmYh8^}9^|SWcI>xAZ*$>D zqaGcL&{`0|A+Lki7$998QknA;&WSh-L6edaeN3>4*mO>}dZ9G`cYQyaQNg{61jV zpY`A}=;HE#c=IbFj2^FLzA^;ZerY=pc?eF)KJNo2sDUak1Q~v(F!C;dOic>pH=n_# zCF-Q5N+Ff{Kn0j;9NvI|5c~tQj$@UO@{leT3L;8n#phj37vyp!vYEw*pelBW{Siox z{+I7*aWYg@YUaB)D=`q$<10L|Qg|5>yXNp{HQtJLM%c1b96iVfvJ83$f`UejE8uo) zby;$R#$G_9s@KLm``cZ(Eq1I!qD7f-=EpkdO~P+nLnYjcV**lF% z*!UhY?-e4k43uj(#sP3%m2Pw5E#nU^*>9Q_K-wf6ST?80tfG&&0G+Q>q1szeVXkj~ ze7BJ@YATlZEkNhvx2VkCw$)DqNy42m04L|i%f0Gbhzx5D*ACg=oOeCLn(i+u3Zgy$ zd&}-|sb7D0C3#%$miQ`lLC$&ugfNwYjX6TUfcSIB#1-%8Jn;mH_ zsC2iy<)2W_U@ZuQHb5g=*aO{-o6b~m#&s%B^azD^kCHjP!;nuDEHp* z|EPLU+M$?&JWO>g9+p$a%W)H%nPSh#j*;>$ILVOgWCQ@mKf$A&40R+;@QI)oZ&ua@ z9Wuif5#NR4`m<09D1Tt%o2whQi>4^2+{6~20^K|?vEiLqNKZ0hbuC(=j|t4MAV8G* z7V!429~mt}U}aD1XC3#LVB>*@-|SXs7h;&yKbf3hU=Y@!-vz+bnzI!g?3O^@YE>Dv zw*#yK_N2#}_Gx1K`O~#9={CY4D*&O6kOZ|2p#CoSZlQ>20Sc-4FChEjSI>Q4Qvh6O zmBXFW9e{6_KkWrt=|d$zdGDS82;6sYGGAsR4xP`~;$wLN4!l%cQdZ2<I#U_e;q zSghN)lyt!&+7(n&AJW&6oMDb3?`rF;1Z<7kE03`eo6F_>=ii%;R=YBETzt__Bd1hy z2Y4jhG)a1dLuUcV*Pv)+LJBv-7u5u+IzF{KfH^pR`lC$9_U;1!ZST3o^S-`fT!FLF zbb9hNC)o@SIPI$_wKD&w9b=I7Z@{v~G+t2a0jVFF`t8A+>#ZrP5E#D_Js5L`GEstBADNGyk4epOZ9jLzmygYf+(Dm zt%&rwjIRHFao8BX!f(5VEys4Q}0yr2&&51{1!JY;(hMi1wj%Df0ICbnFu$t zrPTNcRL3%F3FVa9ra5xcNw(#Qq5ReH5+~IF&i55eZuCL%RzHYis&SO*sp5-fE;)kAS4n4?vy;HJacphEpZ%^*R_of zR=Ig}P_pAg)d>k`NCK-dS?U+h)w=$kSWqM#SEDnTSJ|Vt5xMFW*|CNf}mJ zU$7D7z#;ky=z>5@pudECO|IK@SQ_vjC?25D(W!}w@OCB^{+^Y(k7-D~LpFZdTe@Bv^?K&6i+2_wv10On2o zp~+{fz>JK$BOGy1{@7)}OwX2ICx(_$5Ap`>cmIZ5w~7H`ZUX-R8&E<`v{4TeBwW-2m__Y$H0eyaNY0hQUf4}!aZr?W~`mcDMN2l26!}% zJ8`J+1O9yNIc`VbP+kR|vSZ_3M@P%P^)VU=3jl~Q|1kIf^ek!Who*BKYc(>Atk|pO zbO$`|aa?ExYs(o67*w#Pm6F(#wT1cPEC5uO5MVN{7tW%?YFb|uVt_AJlDB?M4yK;; zAc+@30@+;d=rXJv15wL|U4RqDdSTuasDSuT?K*J_6s#34fn;-dl3;RsF-X!f(2*hp zfNS)uEukH6I-Zp>L|_aM3Iu7JnOE0UPvZYZOPI2?WjS*4iT(>Ef!|E00c}~<4T?@0 z(d?Up5<xv%Gy^#kg?jL zfN31AIH_!&&|YGN@~}7rj(IS!P1gc$TFs)V(7gzO+ieeT_e_Q{&=;E2lo9E~qgT*p zaG=TH=!1Kj34=V{e zUK$|j|B$Q2tNL`WUi>De%^pyF@}ExwIl$z$4hRF_>P28xGMFOw+==5r3O&Zakw(JX z4PdXe+ULJ;oVTf;jz`AoQo4AAaL6Zf9cyhImH{3J9&8e8hEvfl3-d+5{f=M4>3;}-R#ecg+>g^{IrByq7%BkwhoGXA17C|{`o z&0e_n0pM!w$U^)VuJj1$ymYWA6W-t8iZPM|oaX!f7M$vwqkzGl8sjE|A~WWy3j#{V zqYA8)hxCW>X?qVmWjfud+zp<*IeeKN{m7sK3X&w*Cp-arfT$43a}rl=kOs0<2DBAs zLzIXQpZ6sIt0)#3tMq9`%ri>_9&NS+JTpUK?mT+5LVr+X{G|!aO-R~C27%A0?Nk7b z0IqA4`}XlAz+ejn%HX?Izk4IekHP|S+Sz4rG06FJASRHkw;W=A4`e3FZh;W>?a{=3 zpI22EgLtnxpueZw8lO_|2g=+vB9eskCru&3x63L7P0#*lKD+)#eC0LdaZZ=>el<=X z3hl<({p!X&VENPv*2RZc`UQv8T5`Gc2VlKcH~pFV4+d0k;T?_Z1*=NV{Wz|8#%`;Q zb&YYH4ZC}^$-Mm_WWBkLU)s~G`-9oS1Or74nsne_C^UP6K+%Qe5}QUU8LkR(l4&iB zBN`POK!q>>7iW*2{f~__*l_?f!}1xh?U_^{o2U-{+I0;B0?x=O;ym5GRj@e-&`cEX z!Bn){)($9tu>wtiKOf-zWi&C%DsKTD zNge$NB94QFe9j{kc`9_&jdrh@9*Y5rxyIh5L}I~7 zc3RTDWJ@$eFU8HnXcL`1xIXvf`q7iMXO=BW#ncqq@lCA}Ww1heY&vu$*=OBF)=5bluuflnB z5Y40joW<_Bp)MjkX#v-93DPbp(nlmkw==qN**1jH5Wil4XLS{J8N1|;%cdgSqIj?Z z*o-9G3vQS(R8ZK<8sNKXu-{8J*AlpTq~8Z86-om@zm$a!xsDWHn7gULyI^pWU;ZpH z?!?{q7ly|TCIq{hk(^skU%n+xT+IW_UDKa6!(=vW5I=!%M%+5-gAo7ibM56q$UaG;k-M4A~rl zorcZekM!RfP#V}S(xd-Y;oFdmJ72^%NtkE@-h46#tjFNHIX$z?!@rgu)BBo6WPw+I zcWJN}E}fo+egngZ;bP;_uXV?R*PUL=1KCPx*O!&D*4fhCf@3~KF2V*BC>3^#JB2ROgaK5aOtgOMz1jeCd8kTUs{v4YJN0DIndBkP|}$1wV}@*P7IwC>28^u#>tTT(nj(i z=4MK6rf*jV>dZd554uD>=^)3N4qnFGn-+woI9z-@8v&t^g=lzM4!45E2l6pFgiR#RqH>UEC#!xplyl zNVgn6a0LX3w*7;~el*Lk3kcazUKFSTa27`VfX&gC|0E5~>X9wTdXVQek0nDX$ULL`=$}6i~OnK@^#Ml6la3*Zsx0Xb27!{=up>PdIp1taPZ8D zIFyFF@AFNh?@MiDeD<_i3FrrP`HaIzxc|}kW}|1n=Sok*=5mdIj{WrXP|)!Z7n4p6 zDBjTQ{*U&)JRZvZ?O#%8Q=#PuA;uEgWiO?okUe{aWDmoTt)#RaVNlYLY-Q}(*ES6^ z#UT5ZWipl_#9%DXb?bDN?|Gi**Ez56?|Jq5zRn->Qq0^l_dTEc`druhdcWV-lf5ys z<-i8D-wC|WP20#_3$(7rS%iGtb#-yBW-&F(wAjP3 zgT_+7VLD!UHvXp?q2s{`ClfGc%*qSB%H{(!T3YeXXXTg|KXWXemOl`5<3^qEr-JEW~NSNR`?Q zi=i17Lo?{%zdi{u4q_F`hGoU_^u%$h=;IYS>*bd1BEpJimkPN-X1}5xxIu2!MPYR) z+~ix>cuhd?V-my0D~~)P(>JORVB;D)d-T8txlktV0jSP$4y{r_F&*1_j4JwaMICaq z+ixFCLxl1sb4R_+o zZ8VVajJL0d<7A3oBZLnB$ZU%oO%;xI#o!4S$d<4_le0j!lm(@I7F>WV%K>o#v;tfc zj$@$4=VU(}8cfzcv^rrsn)z%v#L|tX+ksBX6wiiyHuZ3@o$|=uAeUDHk6*tgGvUBs zxF)?XZ#oE~1(%7}As7BCyc^TqJz#?susT5ij>ZK?V>Z48UsH?b0Tn`|3_RfEgONuf zJ{-~miidjZ7f+z-_d#Pa1dGyAH#9Vio`Rd9Q6rwwfAGc`k%9WH`?9xIIL3hJyy_FX z{IrqNa|iUC$LG)QgH~#pBm^gW2X>k`#-=^T%SPf2Ga?6B`J+HHdwk6lNUX;PwEQ3T zzCL>ZTY?cDu*{T56mtRm`9@Q4;<9tQP6ul&ziED}O`))Q>al2azL6^~jb%E0AHfZ{ zKiO7Q8>?QAwHU-rKxP7& zG@3S2E50{4!vF4k$#Pvr?$VaM4xRCU9blx-IhubmR z%a=&{KN-JgxFY{k^M?QF=un0Ul7=nS^6;ARPmvNPG3~C_1guFqvdF!PDa5FnJjL~L z9w5^5*oid&da-ar3BO9RZ2Ug>we7|IqoDn+7PaLF)I^RI1gos`|Hmo|B#*(Jr?4ed zBT#e4Aywd$FOv)jK!U{$fYvWvh4w4cT|rp0ha|Ki7_?O(Vdn=7Jwy;557k6UTa=kj zjdn@jm$rz6!Z&HoSE`7?l7h01g1i!(t5V;7=<+Cr_LGxQ>E&G5KFk_3Ed1pk;TMZy zKY()p!A@DV2)c4Ub6loZ$N?)>_W@R!8>__&E_aVNckf_)V0dT<8yXs_xkb~2kZDO+X9U`z;nv)fjj2Yu7zIDW^JS&evMlX zWPnb&i=jXt4P`2YaLxMqam%{638-|;+N(bJR;DbBJsA*v^u=p_vdMltuZa0r*ooRU zm40aYrutrSn%!}Xw^aZQ_=#=Ha~rMmaT9={laNBgf1BE@0A{#3t4HcVM^Fe55VzFY znXZhhf1uTp?*TMyV(uCh!W4JYy14qPe)GWKjxl)SUaLo(k21<;?as&brVHRPxSPdN zk04;`GUZ>dh6`v7=c~amaj%RfciWI04bSGL87H^9>idov0=rZ9nQ@=`WWZBL1+2pE zd{g1L@Kg@?(Hov)xWTDVyw1LqE#I^hD5MdC;_ubn8%`z`y+RGdg?TAE6%x03#l>Xm z!qbQh9*7%d3b!GYXa{S^?1kWg@!8ZJDS@Gl1Es?t1w+$Ik*FD7*%g39lT~r`0cuXi z)ezVi0?Iois33dLuiGL?GZk!;JPiKZ5Q3Ffo%(0n|3S9>|CE6IL*#;D08Wx<;W-0Y zP(-wp`ozJ##g#ExfF=DPI~` zX!zY}^ljio71@9{Bu&xUtf6x}S(KybG14w;1ZWD9;l%hac!4p*y(#n#Z=Ca>8^ZHWa%C9tl9fx!_08b=YnBY3$OMQ?-Z zN3ufT?x;S;1x}bDot@@Lrq=Vwz`Z@k77Gj$qu_0_f)k(K+c(r7ZIG<9_l1a4*U=#v zA0Mx6>16GyA6^MLOG0_M1tOo!pH~#y*9ayQRj_kdU%Yr?B`fQZj#b>FgM(pZWlCGO zZnb6jZJsy%*X`qeKbV7Bfr!*~tVeZVVBlF>a>vUjCFN#?uBswhF*|`g9TG#kwj?*sQ+qIX`wP!{x0KJcg~Wj*1KK7Nlc0^pCv z>f({PXhKl&r_RiC*Yqm|zui0@PisLyd$>I^> zv9lkNAGNDbjzS`QadR2}Wpe}S-1^{C3n(oKbP9jF1Y+x#Vwo@gUL3JY5lMZhs1{>D z)mvd!k#_0Xsti2^n|BYiy$~DZwfnKORB~3uyH!y7z&|XFGIVNdR-}@j$>7uOP#mvo z*50!)pf>a2y^P~@zgS|q|I0=3w`6lp{H z;`H<(>|zJsW65H(Sx~?z zLIKBDQ^L;c+_b9cDAh{Y+KW@Jg)`IpE&Q%HG&dP4y-4|QheJW`X(f;M;sQg$Oy2{r zXCN3KctxYA)=~IXQ1Z&HZj|JOX!1V`!D(dw2^%ZCzq??UAtAwL{W?s zE~aY*^q&1mlgD!Zn4?-`-0>QYFfg#^dA9E8o4kc>rt zLc6=GX=wq+r&7oj%)Iu|oEy%)3|Qeh{rTLpg*UlCjC-5nAU5>qj}a&`>?-B4jAQGL zXc^~7fJrLBcz5T?=mt4ZO+efF%-f%NP^=t$;gD8EH{?m}gP!NW$Vg;ut@cpeg~^mB zM-9@9g*gb?n%&)h^KJDdhs-B2vlR!falfvaY);CAJ2pi6)he7I&f6%?5^}q9*MoUzU<_bV94YHHp3w2pT^}$};avGSD7ran5VuO}|3IrhvF34@Ty&Y|Q@FC zAujBIVvJ`GyBA0i`Zxe&PAo1iUJCWzwATGzb7O?W*-xnQ`L=R1%<07`=S2|!y!|CP zl%^m1jALU{+k(!zGK2GKDv3z4p_;6fJ2?>X0i#nu#LSSIvQ{%xr zz&6*bybxdDk3?Y~>JfhR`=>_f>$m*$Qy7q&s=)cGg6<#`68wTneddc~d9PV=PlxjVxh#fC^^=U<#A42={N2fH-w1wC9C z^wQ&<_yelgb`*M?GPq?P{6eN|Y^@hKdr&Zb{g}RZ{&~^Ug6s|*Mf#mS6YpF5qbqe1 zwfv!g2baQ`+XWL1p!PU@nJ`q&Oy!eA4QJCE+6a^`pg2;1OBM{o6k2CzXLj#RzH$@X!~(tC0u-5Qkjmdm-)#1x!?huu zwJXl@c+4p5B2hUTyW+6ndJ}#=L7E7d`I&bKehC`S9Gzn6TC-q2^Og{ZvW8qg=8+NCqbn~C?!~fiU zfZ&lcX#-Zs7E%oQXvX}Py~=4k^lR1)*ldsyr~>uVz|uIQb)=)%dUCKK+n3>ixYCwN zIo>ObMfogYn9IwoNt>d;?(_F0DG9n`_R6-~29KA>Ue!(3tO9|674(a<0oeP*zETk> zK9QF8Hf2B4cCGxpp4x^6VNR50IM_5-_1;tNyq)~i#0?ti*}yh!)p}VIEt7!+0d}w# z)GaD5wnn4(dFdS0qQ{JX(AB!-T~h`f0LECrO}p+75P}-~_$~vYxpDRu^-`V_38cVQ zF#BcCzI{8cUAtB!C`)q9aHDg!3JD3xwmt8mRR{CRTS0M|4Fp{fR%>)DOFfgN0u?xF zv$Xj;LQO?u3+ag|$@Gsk>4&ZCar;>EoI1ppFJJEZ`Qu@vr8kFwT&sbH$Wh_6 z8VAl$M2I~87fmDr5E=JTrb4Vn&BaT7jfxe+(DB1k-+C5en zw57NcB@G)k`&+};8Ihuzt|xu7_3hp&PB)VNM)j&$uI@53n&;&7w zQ7xdPi1v310`{2zpP<9_IyuXC)YfD_ppZyg;~y0AZ#N%R*UNRyeUgz-UYt<2n0bRz z(gyFVz25ygc4u*jF z2%jfAc+qb>WOw-flSjbYlzcF^QuvM_`nK!bCXllXv_qHabB{(LC@nUg!Ga4U$LS4$ z)hDG(^`Z_q8e78x34vSakta&Zo0Q;qL_J4S|}W)i8u(rF3U_H24}_ z-9Hda9%F)*>v!~^_MQ+UvYrnNerc5~3I-m_Bn}&b56B6zqU~s%7j|{rarG>xiSOYo zz=!5LddT~(aRml1d&4DM9iwOhZsMBOz$l6U+k@oFcX<+j>d1b7mc19c-dhfx(gq(P zW`lrqRarlqxHYiJ>`bPRJZc;_>T|qoaelPPcfr|r z$Ygw`#^3yHFt3FF*k*qLaPY!eA1`}7)my*}R7cw1U|Z@+PnedERrt4o(M zjp!;4zr$SH7CeZBX9>Z)*-jmDExGphVINMCs^OL}_|SPx+Pp+mQBl#Ikt2U5+&&7D z`%2IyT7woF8OxP-ZYaDL^A-Qtj^HuECnIyN+n{jXFwa6#Usimxls!6(Thb==K)Aj@QnuY8#Bc(QFG?dUGkVs?xZ8YlR#?wwXOBFf`507>{6^- zYMq1(T`5{D8~fQ=557NxXPsd>&!i0TkT)0oMDqc1Q-b?6j{p-rf_b!2CHX}z+tJ%rM1uv|4a-t-+$E_))DO`ujTPg9 z=yo>w?r9Jux$KmuKoE6#ZaZ;^+I*?RY(<<~^wG(3Fq!L=DovgNulI()YCzq@k$~Ry zTv2)%Y>#_Gfh~QpPjyD{aG++q(W!DtV2#zrY^Ibp{JaeQB2w>&;LO$y#iISdA#J#e z!edeJ`+IlbVuCdDyitN1@`_VQZ8ykj1iTSYV2*=U^E>z^4-czrE3FqouMv?~Wkn(axVFKZ%`uS7hy*A51)NkG-9 zzkfU~%JSV3Uq2r#LO7-bvX%TXHeCSxYRz|^?IVAW5DmmygxmUl8cSTJ;MCyr3l69>l>P zIaqTxu#uz}dZZf{yg?cBpfO(@v^`=``|TrPdWr$GxNP+sbAsjl zWE`5eH*jprcJ5M&QuZ&i^(CE0PynbWNHAT+s}>Zp1*aZF7)P0>2V8Z zgO+pYK~WZ2m9;z>o!y1}nxhCBuTFqGtcb~OHND#-0-G>aeZrKt7b0df#D;#FpVjy0(L}<`4qlrL# z+_mGZ36i(|5h9L1(bO_OKfho4WBO`uZ|}BydlN(U(98q5<&u^=oy#goC%1sjJI$sG zzqv$nTV7u*-i%u=0uuO~kk8&HH=ny+?M;`94HZl!yY$8QPPGtW*p?Ym)GHlcC@&QU zq}O!0Pg6BFJnPn z>)(xh231))0ualuyyJ?)<#Wr`Rd3z}Sg)V?_23S+381`L%AiyssM7sW6f&l$) z$WQ-CCE49UKF-w~!f$4p%t}xoiO+)0q9)z^0_0((^VOEAqAI9+!-F(V6+(Q#KkUCB zhW+>bx#o|}%laW`06zpJG;t}N)`fIhdA?q`D$lX459Zy3XIT>RY^CLTZJj%cgrSc= zE~GpzG!AoJGe;gH5ze_}>;_a^N0LrO>Ev^~>|0`>buBK?DK>teY{Hh<&O=QZB$&@4 zfK=87#9C$E(Q|NQYsGlLs*V6V*Bj^jlWX7(@L4K{o zoEvHU>0YRx?||zq zd+rs>446$%jcCmIt1}~eHSQYdW<+7P5qmz-GJk}B_B74?lfmF;xL9=mMfy0we~vH? zPTy4^-!jZUGZ|Ue>eXZ>|EXI#-W`*@{c!&I5kvn;LkbATBS3VMz1(iL>qoJ`pHTOBTu`L9{#$u`T;k_k;(zdG-0Nt3(} ze&Pi*dG6+AGWjE(MP3t0P|b*tNm9cx{a^vMQRW^@gm$yI=w#TA-v`5ZpT!)tS1yGG zi}5lsZc=a`41f1<|49UeEx+!x>)`)lM>tuc@e_6?gOE=Olo_&JOjtjlv79&z?QB zj!!`pX3taw+5mKnl-o$)0(O(tt88qS$uC$kH>T4)R_nPZdfdJgSXhwT+c#Y=EiEi-Xj`|s3$~Km^0$gsV}a?~ zd=0Og#j8Rv+flGO1Mv*XBD;+8G&Eewr3WC$^wuhlpx+_Wo|dZ@Gk8^!b-PSD_T?U- zq6h7H<2V;zVff|bCa0-fak>CTc(CC#mFRi!*YQGtu#qRX383Nn$AIBaO=PjV?pnTv zYgv0>vruoaGe|*ES1Ps@KSKzutDI%p052W{*&-mzPWmaw%5>(}lRK~FynMbHXsv`% zu;fV7qnt^c-JG>D-gYr*307{pjF4uD_BfOD)`^AF;l1%+*|8=|T-w5X;L>tan$e@- zOIY-18uH^r#^e$fZR_f&A1{{VY5=))C)Ri|~p^<3uM)_r$gwZ%c9&%6H5t*wXZY`A?n zJq#dP!{|@trvK?+OAsB9%Kmqe&3n+SSTgPYTBBFx2jD3f%Z zQ+5IAOU#(R4{`>OcVBt%1Wc}xy4>h1mizDegxqpsBKr>;0%_+;_}?%6e~0Q~;cS;s z(kI)ZozB4EOKjU?Ft}c}twIF8khOmen^2u0zgval!ajT~A@T13V-Rc{U||F5zGdOA zZU}>XC(M?rawLPfHB<0;DE7d={(Gce-&WzRCq5T1T-Us39}o?BELjec1TdWph+pY2R}dR7HXa6)I?!5FIp3H$dJ( zC7Jzkcr;KVcm16k1(_$ywyP@-8paA-iEoBf036}J4>9_>Y@UenKQxNN zp4Z_-TVMZobS=Ju^>DTbVkbq+8n^+r+p>jgi(pE@3vCA|y}%9ruV8rE;T-Sb9^Uv!?5H7rDlK^FiNeDHw< z0tA*x=eE?>w*X8OR{CBQ0{FoHm36&@fNH?mE-jKfz*{~ifY#A;`up*fi*jVI1p5Cj z94-NkYyRA%0hQobeT+OtbCb0BPLQl%5kL%51s+t6E$GU3?y)9v8Ra<`{cKy>(Ol}C zpK4xeoafvn1+`>GQ-#757<^Rjtx*uVFJ%@65~2NR{`0f$vL3@{(z;-ppw-;;n1)+X zQBeXEa(rHW8(=Q4_rt0D!Edb^J?R5hP_`OaYYgcrD^wwQ9hlgKK|0yzp{(^s5tYW) zGu&>3Q80e!!&}U!47cTLA#SGnttHie%mHJ(eD4IPdO5pW;(p5kE664~@uC@%f8@EF zyb>IGGP3PMQxggp1xCv5J^cUnf_wJ_OB)#s29&D>9*7RA&F|4FG3!Vj z!1TZjH%(9Y1Z8jR%&CgpiP=iP{}8wJrOt)rU!sfHM8PXKRa0hDtK-l<|B!^sUn_oYgNERUz1wq^0Y! z#MRrajGVl)9lev#Mg*sEgE~n+TFEM04>nCX;0YUU);qTRB0!M~Pp{LT!qH0TGp#yY zaad`)?$X0lPlxY|U;n6y|DS5&zf`$Kyk1kz#I&*&vGn_aHJ|@ri@&%6{9EPb1;E<+ zGC5fV<#=ljD{e9;KRFwZ$B(>la>no+@f{S|n0oT#0j)EQ6>{f6RSE*E#8 zayrh+sOvMwc+~qwC*mu|w$@C-v0JnHn(x{Sh!(3=xysU=jb$N z|F->J-vB{!H%kiM4H0GX?j_1}dLHqkHTk7kzI}b@+d#jIr_KWJELZu{zLALcjd`na z4mYZve|z~ib}2GU@oKfe74pENLaQC$Ou~Qntnff4mE;|q?{^9O{v}_h4^p?m_{8d{ zlgGYIBm8AFBNL2aJfz099j(5nb`9q*GZ}vwSoqHyvi);O|5-Hum$$_nze1K}gXfto Sao~8vq^7EQG+pIvz<&X