From 65d290556f4852dc5149ae2407e1fd7d700aefb2 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 28 Nov 2024 20:33:08 -0800 Subject: [PATCH] Write a new post about proving the connection between semantics and CFGs Signed-off-by: Danila Fedorin --- content/blog/06_spa_agda_cfg/index.md | 1 + .../07_spa_agda_semantics_and_cfg/index.md | 376 ++++++++++++++++++ .../while-cfg.dot | 15 + .../while-cfg.png | Bin 0 -> 14727 bytes 4 files changed, 392 insertions(+) create mode 100644 content/blog/07_spa_agda_semantics_and_cfg/index.md create mode 100644 content/blog/07_spa_agda_semantics_and_cfg/while-cfg.dot create mode 100644 content/blog/07_spa_agda_semantics_and_cfg/while-cfg.png diff --git a/content/blog/06_spa_agda_cfg/index.md b/content/blog/06_spa_agda_cfg/index.md index 915c93d..256f615 100644 --- a/content/blog/06_spa_agda_cfg/index.md +++ b/content/blog/06_spa_agda_cfg/index.md @@ -190,6 +190,7 @@ some of the indices of the elements within. For instance, in the lists concatenated list `[x, y]`, the index of `x` is still `0`, but the index of `y` is `1`. More generally, when we concatenate two lists `l1` and `l2`, the indices into `l1` remain unchanged, whereas the indices `l2` are shifted by `length l1`. +{#fin-reindexing} Actually, that's not all there is to it. The _values_ of the indices into the left list don't change, but their types do! They start as `Fin (length l1)`, diff --git a/content/blog/07_spa_agda_semantics_and_cfg/index.md b/content/blog/07_spa_agda_semantics_and_cfg/index.md new file mode 100644 index 0000000..5659105 --- /dev/null +++ b/content/blog/07_spa_agda_semantics_and_cfg/index.md @@ -0,0 +1,376 @@ +--- +title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 7: Connecting Semantics and Control Flow Graphs" +series: "Static Program Analysis in Agda" +description: "In this post, I prove that the Control Flow Graphs from the previous sections are sound according to our language's semantics" +date: 2024-11-28T20:32:00-07:00 +tags: ["Agda", "Programming Languages"] +--- + +In the previous two posts, I covered two ways of looking at programs in +my little toy language: + +* [In part 5]({{< relref "05_spa_agda_semantics" >}}), I covered the + __formal semantics__ of the programming language. These are precise rules + that describe how programs are executed. These serve as the source of truth + for what each statement and expression does. + + Because they are the source of truth, they capture all information about + how programs are executed. To determine that a program starts in one + environment and ends in another (getting a judgement \(\rho_1, s \Rightarrow \rho_2\)), + we need to actually run the program. In fact, our Agda definitions + encoding the semantics actually produce proof trees, which contain every + single step of the program's execution. +* [In part 6]({{< relref "06_spa_agda_cfg" >}}), I covered + __Control Flow Graphs__ (CFGs), which in short arranged code into a structure + that represents how execution moves from one statement or expression to the + next. + + Unlike the semantics, CFGs do not capture a program's entire execution; + they merely contain the possible orders in which statements can be evaluated. + Instead of capturing the exact number of iterations performed by a `while` + loop, they encode repetition as cycles in the graph. Because they are + missing some information, they're more of an approximation of a program's + behavior. + +Our analyses operate on CFGs, but it is our semantics that actually determine +how a program behaves. In order for our analyses to be able to produce correct +results, we need to make sure that there isn't a disconnect between the +approximation and the truth. In the previous post, I stated the property I will +use to establish the connection between the two perspectives: + +> For each possible execution of a program according to its semantics, +> there exists a corresponding path through the graph. + +By ensuring this property, we will guarantee that our Control Flow Graphs +account for anything that might happen. Thus, a correct analysis built on top +of the graphs will produce results that match reality. + +### Traces: Paths Through a Graph +A CFG contains each "basic" statement in our program, by definition; when we're +executing the program, we are therefore running code in one of the CFG's nodes. +When we switch from one node to another, there ought to be an edge between the +two, since edges in the CFG encode possible control flow. We keep doing this +until the program terminates (if ever). + +Now, I said that there "ought to be edges" in the graph that correspond to +our program's execution. Moreover, the endpoints of these edges have to line +up, since we can only switch which basic block / node we're executing by following +an edge. As a result, if our CFG is correct, then for every program execution, +there is a path between the CFG's nodes that matches the statements that we +were executing. + +Take the following program and CFG from the previous post as an example. + +{{< sidebyside >}} +{{% sidebysideitem weight="0.55" %}} +``` +x = 2; +while x { + x = x - 1; +} +y = x; +``` +{{% /sidebysideitem %}} +{{< sidebysideitem weight="0.5" >}} +{{< figure src="while-cfg.png" label="CFG for simple `while` code." class="small" >}} +{{< /sidebysideitem >}} +{{< /sidebyside >}} + +We start by executing `x = 2`, which is the top node in the CFG. Then, we execute +the condition of the loop, `x`. This condition is in the second node from +the top; fortunately, there exists an edge between `x = 2` and `x` that +allows for this possibility. Once we computed `x`, we know that it's nonzero, +and therefore we proceed to the loop body. This is the statement `x = x - 1`, +contained in the bottom left node in the CFG. There is once again an edge +between `x` and that node; so far, so good. Once we're done executing the +statement, we go back to the top of the loop again, following the edge back to +the middle node. We then execute the condition, loop body, and condition again. +At that point we have reduced `x` to zero, so the condition produces a falsey +value. We exit the loop and execute `y = x`, which is allowed by the edge from +the middle node to the bottom right node. + +We will want to show that every possible execution of the program (e.g., +with different variable assignments) corresponds to a path in the CFG. If one +doesn't, then our program can do something that our CFG doesn't account for, +which means that our analyses will not be correct. + +I will define a `Trace` datatype, which will be an embellished +path through the graph. At its core, a path is simply a list of indices +together with edges that connect them. Viewed another way, it's a list of edges, +where each edge's endpoint is the next edge's starting point. We want to make +illegal states unrepresentable, and therefore use the type system to assert +that the edges are compatible. The easiest way to do this is by making +our `Trace` indexed by its start and end points. An empty trace, containing +no edges, will start and end in the same node; the `::` equivalent for the trace +will allow prepending one edge, starting at node `i1` and ending in `i2`, to +another trace which starts in `i2` and ends in some arbitrary `i3`. Here's +an initial stab at that: + +```Agda +module _ {g : Graph} where + open Graph g using (Index; edges; inputs; outputs) + + data Trace : Index → Index → Set where + Trace-single : ∀ {idx : Index} → Trace idx idx + Trace-edge : ∀ {idx₁ idx₂ idx₃ : Index} → + (idx₁ , idx₂) ∈ edges → + Trace idx₂ idx₃ → Trace idx₁ idx₃ +``` + +This isn't enough, though. Suppose you had a function that takes an evaluation +judgement and produces a trace, resulting in a signature like this: + +```Agda +buildCfg-sufficient : ∀ {s : Stmt} {ρ₁ ρ₂ : Env} → ρ₁ , s ⇒ˢ ρ₂ → + let g = buildCfg s + in Σ (Index g × Index g) (λ (idx₁ , idx₂) → Trace {g} idx₁ idx₂) +``` + +What's stopping this function from returning _any_ trace through the graph, +including one that doesn't even include the statements in our program `s`? +We need to narrow the type somewhat to require that the nodes it visits have +some relation to the program execution in question. + +We could do this by indexing the `Trace` data type by a list of statements +that we expect it to match, and requiring that for each constructor, the +statements of the starting node be at the front of that list. We could compute +the list of executed statements in order using +{{< sidenote "right" "full-execution=note" "a recursive function on the `_,_⇒ˢ_` data type." >}} +I mentioned earlier that our encoding of the semantics is actually defining +a proof tree, which includes every step of the computation. That's why we can +write a function that takes the proof tree and extracts the executed statements. +{{< /sidenote >}} + +That would work, but it loses a bit of information. The execution judgement +contains not only each statement that was evaluated, but also the environments +before and after evaluating it. Keeping those around will be useful: eventually, +we'd like to state the invariant that at every CFG node, the results of our +analysis match the current program environment. Thus, instead of indexing simply +by the statements of code, I chose to index my `Trace` by the +starting and ending environment, and to require it to contain evaluation judgements +for each node's code. The judgements include the statements that were evaluated, +which we can match against the code in the CFG node. However, they also assert +that the environments before and after are connected by that code in the +language's formal semantics. The resulting definition is as follows: + +{{< codelines "Agda" "agda-spa/Language/Traces.agda" 10 18 >}} + +The `g [ idx ]` and `g [ idx₁ ]` represent accessing the basic block code at +indices `idx` and `idx₁` in graph `g`. + +### Trace Preservation by Graph Operations + +Our proofs of trace existence will have the same "shape" as the functions that +build the graph. To prove the trace property, we'll assume that evaluations of +sub-statements correspond to traces in the sub-graphs, and use that to prove +that the full statements have corresponding traces in the full graph. We built +up graphs by combining sub-graphs for sub-statements, using `_∙_` (overlaying +two graphs), `_↦_` (sequencing two graphs) and `loop` (creating a zero-or-more +loop in the graph). Thus, to make the jump from sub-graphs to full graphs, +we'll need to prove that traces persist through overlaying, sequencing, +and looping. + +Take `_∙_`, for instance; we want to show that if a trace exists in the left +operand of overlaying, it also exists in the final graph. This leads to +the following statement and proof: + +{{< codelines "Agda" "agda-spa/Language/Properties.agda" 88 97 >}} + +There are some details there to discuss. +* First, we have to change the + indices of the returned `Trace`. That's because they start out as indices + into the graph `g₁`, but become indices into the graph `g₁ ∙ g₂`. To take + care of this re-indexing, we have to make use of the `↑ˡ` operators, + which I described in [this section of the previous post]({{< relref "06_spa_agda_cfg#fin-reindexing" >}}). +* Next, in either case, we need to show that the new index acquired via `↑ˡ` + returns the same basic block in the new graph as the old index returned in + the original graph. Fortunately, the Agda standard library provides a proof + of this, `lookup-++ˡ`. The resulting equality is the following: + + ```Agda + g₁ [ idx₁ ] ≡ (g₁ ∙ g₂) [ idx₁ ↑ˡ Graph.size g₂ ] + ``` + + This allows us to use the evaluation judgement in each constructor for + traces in the output of the function. +* Lastly, in the `Trace-edge` case, we have to additionally return a proof that the + edge used by the trace still exists in the output graph. This follows + from the fact that we include the edges from `g₁` after re-indexing them. + + ```Agda + ; edges = (Graph.edges g₁ ↑ˡᵉ Graph.size g₂) List.++ + (Graph.size g₁ ↑ʳᵉ Graph.edges g₂) + + ``` + + The `↑ˡᵉ` function is just a list `map` with `↑ˡ`. Thus, if a pair of edges + is in the original list (`Graph.edges g₁`), as is evidenced by `idx₁→idx`, + then its re-indexing is in the mapped list. To show this, I use the utility + lemma `x∈xs⇒fx∈fxs`. The mapped list is the left-hand-side of a `List.++` + operator, so I additionally use the lemma `∈-++⁺ˡ` that shows membership is + preserved by list concatenation. + +The proof of `Trace-∙ʳ`, the same property but for the right-hand operand `g₂`, +is very similar, as are the proofs for sequencing. I give their statements, +but not their proofs, below. + +{{< codelines "Agda" "agda-spa/Language/Properties.agda" 99 101 >}} +{{< codelines "Agda" "agda-spa/Language/Properties.agda" 139 141 >}} +{{< codelines "Agda" "agda-spa/Language/Properties.agda" 150 152 >}} +{{< codelines "Agda" "agda-spa/Language/Properties.agda" 175 176 >}} + +Preserving traces is unfortunately not quite enough. The thing that we're missing +is looping: the same sub-graph can be re-traversed several times as part of +execution, which suggests that we ought to be able to combine multiple traces +through a loop graph into one. Using our earlier concrete example, we might +have traces for evaluating `x` then `x = x -1` with the variable `x` being +mapped first to `2` and then to `1`. These traces occur back-to-back, so we +will put them together into a single trace. To prove some properties about this, +I'll define a more precise type of trace. + +### End-To-End Traces +The key way that traces through a loop graph are combined is through the +back-edges. Specifically, our `loop` graphs have edges from each of the `output` +nodes to each of the `input` nodes. Thus, if we have two paths, both +starting at the beginning of the graph and ending at the end, we know that +the first path's end has an edge to the second path's beginning. This is +enough to combine them. + +This logic doesn't work if one of the paths ends in the middle of the graph, +and not on one of the `output`s. That's because there is no guarantee that there +is a connecting edge. + +To make things easier, I defined a new data type of "end-to-end" traces, whose +first nodes are one of the graph's `input`s, and whose last nodes are one +of the graph's `output`s. + +{{< codelines "Agda" "agda-spa/Language/Traces.agda" 27 36 >}} + +We can trivially lift the proofs from the previous section to end-to-end traces. +For example, here's the lifted version of the first property we proved: + +{{< codelines "Agda" "agda-spa/Language/Properties.agda" 110 121 >}} + +The other lifted properties are similar. + +For looping, the proofs get far more tedious, because of just how many +sources of edges there are in the output graph --- they span four lines: + +{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 84 94 "hl_lines=5-8" >}} + +I therefore made use of two helper lemmas. The first is about list membership +under concatenation. Simply put, if you concatenate a bunch of lists, and +one of them (`l`) contains some element `x`, then the concatenation contains +`x` too. + +{{< codelines "Agda" "agda-spa/Utils.agda" 82 85 >}} + +I then specialized this lemma for concatenated groups of edges. + +{{< codelines "Agda" "agda-spa/Language/Properties.agda" 162 172 "hl_lines=9-11" >}} + +Now we can finally prove end-to-end properties of loop graphs. The simplest one is +that they allow the code within them to be entirely bypassed +(as when the loop body is evaluated zero times). I called this +`EndToEndTrace-loop⁰`. The "input" node of the loop graph is index `zero`, +while the "output" node of the loop graph is index `suc zero`. Thus, the key +step is to show that an edge between these two indices exists: + +{{< codelines "Agda" "agda-spa/Language/Properties.agda" 227 240 "hl_lines=5-6" >}} + +The only remaining novelty is the `trace` field of the returned `EndToEndTrace`. +It uses the trace concatenation operation `++⟨_⟩`. This operator allows concatenating +two traces, which start and end at distinct nodes, as long as there's an edge +that connects them: + +{{< codelines "Agda" "agda-spa/Language/Traces.agda" 21 25 >}} + +The expression on line 239 of `Properties.agda` is simply the single-edge trace +constructed from the edge `0 -> 1` that connects the start and end nodes of the +loop graph. Both of those nodes is empty, so no code is evaluated in that case. + +The proof for combining several traces through a loop follows a very similar +pattern. However, instead of constructing a single-edge trace as we did above, +it concatenates two traces from its arguments. Also, instead of using +the edge from the first node to the last, it instead uses an edge from the +last to the first, as I described at the very beginning of this section. + +{{< codelines "Agda" "agda-spa/Language/Properties.agda" 209 225 "hl_lines=8-9" >}} + +### Proof of Sufficiency + +We now have all the pieces to show each execution of our program has a corresponding +trace through a graph. Here is the whole proof: + +{{< codelines "Agda" "agda-spa/Language/Properties.agda" 281 296 >}} + +We proceed by +{{< sidenote "right" "derivation-note" "checking what inference rule was used to execute a particular statement," >}} +Precisely, we proceed by induction on the derivation of \(\rho_1, s \Rightarrow \rho_2\). +{{< /sidenote >}} +because that's what tells us what the program did in that particular moment. + +* When executing a basic statement, we know that we constructed a singleton + graph that contains one node with that statement. Thus, we can trivially + construct a single-step trace without any edges. +* When executing a sequence of statements, we have two induction hypotheses. + These state that the sub-graphs we construct for the first and second statement + have the trace property. We also have two evaluation judgements (one for each + statement), which means that we can apply that property to get traces. The + `buildCfg` function sequences the two graphs, and we can sequence + the two traces through them, resulting in a trace through the final output. +* For both the `then` and `else` cases of evaluating an `if` statement, + we observe that `buildCfg` overlays the sub-graphs of the two branches using + `_∙_`. We also know that the two sub-graphs have the trace property. + * In the `then` case, since we have an evaluation judgement for + `s₁` (in variable `ρ₁,s₁⇒ρ₂`), we conclude that there's a correct trace + through the `then` sub-graph. Since that graph is the left operand of + `_∙_`, we use `EndToEndTrace-∙ˡ` to show that the trace is preserved in the full graph. + * In the `else` case things are symmetric. We are evaluating `s₂`, with + a judgement given by `ρ₁,s₂⇒ρ₂`. We use that to conclude that there's a + trace through the graph built from `s₂`. Since this sub-graph is the right + operand of `_∙_`, we use `EndToEndTrace-∙ʳ` to show that it's preserved in + the full graph. +* For the `true` case of `while`, we have two evaluation judgements: one + for the body and one for the loop again, this time + in a new environment. They are stored in `ρ₁,s⇒ρ₂` and `ρ₂,ws⇒ρ₃`, respectively. + The statement being evaluated by `ρ₂,ws⇒ρ₃` is actually the exact same statement + that's being evaluated at the top level of the proof. Thus, we can use + `EndToEndTrace-loop²`, which sequences two traces through the same graph. + + We also use `EndToEndTrace-loop` to lift the trace through `buildCfg s` into + a trace through `buildCfg (while e s)`. +* For the `false` case of the `while`, we don't execute any instructions, + and finish evaluating right away. This corresponds to the do-nothing trace, + which we have established exists using `EndToEndTrace-loop⁰`. + +That's it! We have now validated that the Control Flow Graphs we construct +match the semantics of the programming language, which makes them a good +input to our static program analyses. We can finally start writing those! + +### Defining and Verifying Static Program Analyses + +We have all the pieces we need to define a formally-verified forward analysis: + +* We have used the framework of lattices to encode the precision of program + analysis outputs. Smaller elements in a lattice are more specific, + meaning more useful information. +* We have [implemented fixed-point algorithm]({{< relref "04_spa_agda_fixedpoint" >}}), + which finds the smallest solutions to equations in the form \(f(x) = x\) + for monotonic functions over lattices. By defining our analysis as such a function, + we can apply the algorithm to find the most precise steady-state description + of our program. +* We have defined how our programs are executed, which is crucial for defining + "correctness". + +Here's how these pieces will fit together. We will construct a +finite-height lattice. Every single element of this lattice will contain +information about each variable at each node in the Control Flow Graph. We will +then define a monotonic function that updates this information using the +structure encoded in the CFG's edges and nodes. Then, using the fixed-point algorithm, +we will find the least element of the lattice, which will give us a precise +description of all program variables at all points in the program. Because +we have just validated our CFGs to be faithful to the language's semantics, +we'll be able to prove that our algorithm produces accurate results. + +The next post or two will be the last stretch; I hope to see you there! diff --git a/content/blog/07_spa_agda_semantics_and_cfg/while-cfg.dot b/content/blog/07_spa_agda_semantics_and_cfg/while-cfg.dot new file mode 100644 index 0000000..293696f --- /dev/null +++ b/content/blog/07_spa_agda_semantics_and_cfg/while-cfg.dot @@ -0,0 +1,15 @@ +digraph G { + graph[dpi=300 fontsize=14 fontname="Courier New"]; + node[shape=rectangle style="filled" fillcolor="#fafafa" penwidth=0.5 color="#aaaaaa"]; + edge[arrowsize=0.3 color="#444444"] + + node_begin [label="x = 2;\l"] + node_cond [label="x\l"] + node_body [label="x = x - 1\l"] + node_end [label="y = x\l"] + + node_begin -> node_cond + node_cond -> node_body + node_cond -> node_end + node_body -> node_cond +} diff --git a/content/blog/07_spa_agda_semantics_and_cfg/while-cfg.png b/content/blog/07_spa_agda_semantics_and_cfg/while-cfg.png new file mode 100644 index 0000000000000000000000000000000000000000..f196a6c422db15fd099926e0102e57235a65c5ff GIT binary patch literal 14727 zcmeAS@N?(olHy`uVBq!ia0y~yV2WU1VCLswVqjos`(abSz`($k|H*Y zfkA=6)5S5QV$R#U^)Vr(`+j^h{xjh|lh%XxDci%kE^!&&nw^+eadw?#+*#e*m#)6a zD)WsBKP!^stIK-!%8T~4?A0@O-Ff|N)4fyQ9-h@XD>C&{xZ4b+SxQYDJO=mepVg(G z?`!xo!*c(<_0Qvt+nGPtEjV|&_}Q8C9KLpEMg|8h`MvB63=aM+0t^aLiYyErZXApZ ziv*n*8Zw9%nl*nKe^^vhR9M)ur^-xg1?1%9BqdjV7hy12l*!>g*Q)f(i$Gm@!Hm{> zd#i<=9Qb^lUx>)a$cTw8`}>&bdT3l+Tx29z`BG<&-KDR^+0{%zrSzqJz>U%>w-=izrVkq zZ(aUwU+wR@UoX|aew$}oeXsDitfZvm$B!SY&ayGwJGL_LqL#LH`q^1uPsjf&`u*)~ zo@j{3(iJOS?En9JKS=+?iGi`PYfrZ@JjiVcSa*53|NX+_vNLDSEG;edeUrBRwzy8j zh4u0K^Y{I9+kBJ3!MG(rqy4a9-Jc)t_y3REd-44Gi@{Ib`{iV9t4dN+mwtC=X7Cks zS{PUV_p7XRnMFRotX0YBX}YYetkd=5^)xk4o<3dua_Mxdk{1uY>ALsJ{k{9XZu!q8 z3=d*k0v0K|_wD)dsJm;?owD1x*5&X1tpEROed6J^yCs)>>+0$zPMo;^*VXlD=jQzU zdOeHC$>=dO+3{>s3Rp@LU&%8R?@_t&mk)z#nsfByfU^Or1H!uI{;t*x)` z|NFN6xLoy_+~3jpd!PPgWOT4@30Tx`_iKfFzg%TyrL1*XPLjF2{QNa*)~r~e@%32k z?{AfrRty(J6h)rDxw*NWUw)o(y5IA2bJy=KZs(H~(~nzoujt{S)K7u}nio3BRm$yhvS-O1n}-x4rq#flZ%?^T_?e}DhX-?wwN z?bu=Qby`CMgZ>#-hF=MtriE<$a(6D}?|eEfdf&fa+1KyRv#qWwQDV3-nbkRC`)&QW zJr#HFE?T@e*KGD8jndN6>+AHMi3kV?2ns%Y_|s=a_4jw{Zrj<}`L=9Ww@y!6`}N=N z_t&ppEp3=|YO<>ckg<6dpkQhiMVQNX}!9;yS(`~ zkF;6N>1n!ar62Epzi;*W_4#+do9P-DY;fE%_-~0D$c7ENTkM8&K7!N$qkvO#b{l4E14mQiz|M?jI@6&XD`@dgq$r>3M)&0JG z-%5LhhF4C`n~llG#dIPjOrHGsR{D<*5BqICotU8L9A)eF|KH!!r%y-!ee3Jt<8xL^@-?Q-Eq{)*vSA2Z*;X{EwA3H;C^4adxM~@yY z^O?D+_V>5+`L);HdfVCAU0&u}T>ac(ecWC(-&s#~{XV6=KIhh!%quGbePw=~2#k*Y z{d9V~RepO*%aUcw%(kVwx*pvs9~2lB_3G$Dh6QJJDqL1fn>n-c-JPAi(&oFiUAcb! z`O~Mp5{8Fz&wqV=-8x?hX>9qw|9n2LAG_Uv?nnf*s!KDD@0dEC+Bb*@2hNa|G8GC)!%Zi$L_vsSNEr4 z_uY9jX6z_>>Sdc|vW{C^Z%3R}?4F9kgoK34zmFe3{`~p#{M*}dUte3>&L{io{{H>f z-B}v8ZLH%Eb$xkzd%l}nTa|ZN*|&FhchB8^`SN9cIhz|BlaKdGn|}%`G+!OIc308U zu0?|R8>+ctu6svi*MN@vhee7Ha+Z-%XpTU)nXM#R;!`rDgNPfv@wa&mK5zukKMiyS+{9w#r3+M1ec zYa$od#co)zAOVy-j`bE>$Xs6LD{WP>qVKWf?)Pn|lIV|IJ@`+c`>MC&phc(bG> zAaF|D-m28Jv{l5+eLSIT}{o-{{HyQX}s_284_|IIY|f$Po6sU>k(o99ox># zG*(wtJ^DER_iXF(cUw=dsc^ZzE_Uz7*@-spB7M8_is<-=aM<66t?Bw{&vRrJPRx9(`V1Vy}a!HzL3Fzdy~_S`v3o4 zUS57XXWN`PbFQuqUmgGV)R{9^ekjZKJUgwwU&c7C=WJT^{<^)tY^O6Md-X}Hh6N=y5+^nvze|~i{V}qGXOTqnpwZ>^@3ig@YSn4hQ zb-IwSaQc}U3-1|aURp9~l29)Dm9wBc`Ty^CadGkUvrMy}otb&|&pPLJK3-X?FURHU zzr4y}Sit+b{llSF?#1r?>sGGx^!E1l^xRq2esgpB>iaGg|Ni{s6jrm4;p0ue(!RMV z{oEW+Z}049uABMVA5ZqTlQheTC@uYZVxsc;y9@X1sW~}G)!*)CN>$Y_@%WmDFDEh{ z_^k8K?$EAXy9|?$iHM4ReS3TR#^+V__5aQ9RU|(+(D?Q1*K@kJx97)iN;&!E@3 zA=&Nx@^V%sFK%v5pFC+28;`_-xH7-94-0O*E!%xJE-dWZ<9_?RdwYKV`1lx-w6E8N z{GDl>{%+@Ux$6@jEpqJ!WgPMNnu%L886;*Nb+*X9wno;vOrvX4($Oxpd;0UIOfe~X za)RIP$APV?wzhxc|2>Vb`*}J(%W&zlZ*OiI=iJzE=~9qu;JzP^y02WhGVNc>aryc` zw|X-(GhcmP%Gdswzy62w_jh-X_ex)%mdSWv^_rTjl81*{Pfybg7CCzTy1A9ru9tIv ze|^1tUvzZz>{+v_9vooQKev4H{{Mg9JGb!^hHWUdDtlv*a$-XE_T6@`BXZx}*_m{I z3ey3RHIj#7cbENrX1?Fk-@p9c+SRM8Kb=%J&%bx)!Er|sQPI6WpUw83u2*_HE-Gr) zq)DK7=C}W|Vbi8dubs1#Zg0!wxBU_zZ7-Jmy^GLz5mCfZct<7XXWcWxrzsk>GNy1?bz|-mj2YKQ`g4rtvb>n zc=P7Xds5-ir>E(zUbQOgF@NTVJu4Pz2&?&I6#U+peEimr4u%J|Vl}-61_m3JEnD{U zx44K%MZU!1pDz~o@A-ase&w^7A3hX3KmLemw49-7juk`l{sVsj1OhMd zE!%5;y*F+h3S_KXz-?4in!Qj()os6E$;A!+D`eAjq?4LY6J-xfDYfF91gI#*@`__Et zVA!(EnZw%)1h&-2bgx{y_U`ul`LFYwoSNp(=c}K^kWe+j z>d&8=>vyM2neyO4g6#8+lQwKH*z3-)K-Sk;LK*~CKUI#3h>V>1D=#Q0sG?#=++l`> z%EFC23=Sqv91H@z0!$1p$}J2G7daG1g+@by@-*@Jay5fVcw}T`UERLdd8w&Of34nK z{+^GIuk7yI+uQRiDt43|W^Bm3DZ|%(&v-%Ps#UApdZj``Lrd@4GBYum<=zqz5m|CD zgdw49j+ANdfddD2zuUFivRX}5HPDeEL(M5e?fc#G_~J5YlZ*-5)fpL1E3~9t+F$?w z!i5XVzH{>O`ug}>Nt0vPz~Gdj_V3?6W;ULTs`-q}Y(IYg&Nk*}h+t4OnfZF2?9)9O z3|lx9O=jNC-@i9_xnFPXR_AuU+FxHT7RfOfSUY7HnazHCuljxNo7K$hd|y63JTJl! z)u8VCIrGsQjpwe63zl*${CVW)(bCt~-rjl(s$h=l*Dd^O!;p~Ga$yP^pG?KuV~)*i zH*?I+rZX}WE4M8BvO50nt6RM%PoBKx&%}`C&f&Y#yZJ)E z!wd;U6YcHZX;L z7cXA?b&i=q&6UIVOsU9;hYAc^q!djyK6#R2Z*LzTfB*HmBfJb5J;w$#UX zcXf0Gh^Q(kIJ|e%S+r-*o=uyA-fJ>sc(n_Zy}ov~bf>F;P)*37oQM(V}~MtIc60fF3TGiO>>eaZMb?bokgd-m+f{vNZx zZtv$~kB)XP_np1$XaNHQ^M(ozQP;?=Syy|_@2$9JRQu~oR~OgUX@CCw30)ng+4bp& zu)oh-tI*3o85nkLs^d6(=#W{?jSK5yt*=iDUha2xp6%_@>v`MzZNFuZ{GTZN^hUfl``2rx)LH>dFNF-w`g z%*)GoWvxPve`H{&nkeMt8d&x9)zq0YSKga6b!uo#%$zAxOzQvD>|Msh@WMNQL)2B$ zJnv33zuk&^kDfo@o_E*E-ky8i24;o~zDUIo5mjsJ-NDQK*6oJ$HLcDuGhCRyL*Uqv zBPpq=E4QDSX}o;F0*CdL3=F?8x`?x8N$q{c$ne4=hGX;Q&F1;{WJE=;Zcg{Ve(cYm zKb4=Ky|fTzaL~u>^jX{YU(hr*F224l*6JJ^!-dub0@J2Wwf*&C@ztwWjnmKhczSyJ z`OPy*?RvfX>({T3kM(Nn>t8Q)Vrck=y-WAc?~yc~qt9FR@{;S{rALk&ku*+QvE65u$;u^5Ty8T$VpujPJeIi$(uB3l3Sn5%6pUM z&HMNB`TXiyJBEgPYh(_!a*OLlZ}SNhiI2bk;>C+)s2E&`yLB< zh64;ZyC*S$frW3+xw^XM@B8`e(o*lc+on&Owrt4~pIIg^5A)lvS+nNLuL}$ewl}uy z(R%XWV6%I_+}@YVW?vCsUJ(--8v6U&Tj@VRZf?i8_4hp3W@u;k@5jf-zW>j-c8h%! zbLQmY;_8#Pzqh;myiUtG2S(jnb;3l@v zP78{UU;mwhVa+lB-|c&9eij7=PW;x-z4`XG+~~x_hr#}~SJ%Z_>)RfAdV2caFOwN1 zrtvB2XoA4Se}%k{9vp0ber_%|A0Hnt@7p^&i%Uwj+!OvgzpJb3!i9jn%QLP_RCX_W zcW0%>sXsqIxARB}Nl2{t?!utsbXfr2t~XgQ*SdV3P35IZYfHJ3DrJ z{{Fw;7@65#SoEB}x;k83C!*lzr>9r0gzQbvbO;Fv0ngUV{0zz&<~cVu6g)g6XIu5c zT7rT5L6YR!*gX{&ORbHJf{uG$;gh$EiH_c#dV1QfT~;97F)=Y|X=x!LQ?k81Jx^X) z8O+VaRWgUG!BoI$?bK=0cIB17xZrr)^U9~spG93kL(Fpve^F9CH;zM4mSD+g&K1q;}-Ukv-pTWqKSnkei@4e`#{6X|2`b%uj0Kdvv1$N z%*@Pwn@=58$$5G29v$t@&d&Zii>tv?(8+hDbH;?vi@IL1I;poG-k5q?Y;Rkp+U&F6 zt_1u0&a=6hwt1&n-It5*pP!u#-p|F&aNU)|H1&W$+|Ht>M>>V`r0xIxNd6ibbJ)w* zcdlLSuKD-v@A3UUDjxsmUHSgxr6vq#-9hTj1wn&6x2CRnTlV|f+UU}m%a;ZP1zoy) z`Re*@a+XCZy1H-w{QPX?$9lkpW8pHM3YQmUaaU4bUt1d*8Y;zq*~-(?(|ei@CqI9A z?$3wq^2>Z@m%X~8DZ890L98Vpm~BtQvA155(?5OswEyqhd@26RSvt1N3$Ai3T-H;T zwPn$wLtB}CY~|VgD5^Q4ip}A*fRk_Ru9B0b)=ElF$35rp$=TdE;trbiD7(HcHtO7E zH;`^oj)i6G;`U~3za3lND{$yooI;7=kJ+!+AH8JE5Y;7+wS3Q>nA+S(`1>`J? zo?KYye2eF?CP=F*$HFo#Ev=aCwKX+O&CR7UZh=!yPuDm9$h5HgB_EgQw0Vpdgjxcu zUkS9ew5*u!a`EUw=k{5}Enkj`$Itj!%KnytuJ3*~R6^x3{;w zy}ahcSADygE?@ORvG(}qDO09Q*|1^5&(F_y^RdkJKCctABjE2oXNDv}r?)HmIeH70 z`nb8Z{mOH6Y}9TsH8r*3d188QX*y_>ZPO;B=VH$<8FP#4h3tPX(BLyi>gu_v+Tk(V zdkb7%sHvzNDUG&WWxC-DPs1?*r?(PsJ1+F@I(vc2b`Z|XA%pV9Yv}y@o zAD8>6m`hhpRaMp2)>c8`z}BNXznuB``FZIau7)&@g>LKO_O9Bu`nS7(jCXC;m4^i( zVPUT^b8f;nul$UWVtTH(HerfVcNe2<96@p(w7q{^){M8Xq z!~sei>(n=Y#VHxRtP#}#Oc^FM@TDP>9A^H zt1;gzyxdLt@FnAhRzauU8IL+9bf?bpW7BnDV30Hbtpzx6$+#gDB&F0cM=Dp!`#i%m z7Y@^;E`g$~FS|g7$~mnNyxclL`OvWqUw9G>K~CHe(H6Y;?2${x4O0c2dROdTWcR^H z#IM&(9;Dlm!*tQVimKq23Cf3FC%u$BAjPrJ?M>P4*V}$2|L1A#Pt0PSHjnX4pFoyN z?XENT@5dkaoOK|(Wi7~!D+Qf;S2$TY57O+S(ho#aNooVwJdpZTO4(hnK>~VXMt7FS7A)t7rDYB1)b0HhZ8Y!n0t-pR% zeT_ZbHX(TNt%R472Ld=2ik|SlJE6%#I8l;KCX$5m> zj)J83c?LHJj;#ky>X|eyO=qYTbaJTIv1NYIA&})*>yq)|^CC5=t4VXb&u_`Ue{U9EdktWwx(H&0(JYBrZc=(Z27_7$I;ufG@U_Tu_Y=%K5C|hnT((m zulIR|dk!317yLVL``53k!`m)wXg&yXY`=0#R6zW*1s@u>XGl+*$7s_H_SXuHuEhH+ z&%!dcZ%mZYv1P6Rh3IX;g^A8D%x2uaVE~G1n^sVuFL&cyxO2l7o(F<00o*czhrA=I z*fOl0R@vDOsjTe@H?9g;tA=t;U zP!ePeDAC;&J=_*xE1_s&I&B`~tbS0EReaKM!3(5T&1r>T@Eob99T$>7Ts{ytMrUzd z(UT;}?1Yz+4|ajd48@Y_`@0HPIG>o!v9@JtdV?Cs*6Dv%tXz4qaFSYqOGcuOEwf3R zK$gp2mXfcpLS@x6nZ!>=NPC}W;8kjo;sg~!W^b~MUkMbsWO(Y>GRJg-T@fO`ij9@^ zr3L4n_ND0z=Ae=*cyVZGsFmL(mahq~iVlMu6`%|*@kHEPS}xp*sA4NnY>^5qZ&h}Z zVDvuE;0G!kDtadfc!4sr6NhQ?uIn5-BiuNq&12+P=;kBt)W_kP_)^lt4U`*$7su!* zOM0Jo&;fhY^pxPj0v%iCnIM(rS2flPo;q^LSfE27tK~XJqL_{?b0$dUqm-gzi?H{3 zaN+oPzEr7&%qu5hr-u<$Y(=1u*c}ucoP2*tc(AivXx)!L8hKD^OlU%BE%E!iBH?|6}IzK7U{r$HFomxkH~m6kQVBz$_wfftepC1nM>&NaY`S|Fl_jJ9L z|I1^dqJG`0e!ugb-G>9rRXjiZD|!WTr%ak8BqnB7|F7nHd?})FU?An!TNRj-^XA^( z>ivJe-JUdQ(z5e{U*Fyi-@H=lNrA-`{pcc>j%%6!E*T#^dQ{ph=R%p)g2a{!-HR42 znlyRx?9I#HDeftH+V#uG-l-!j``jht)YR0?>F57Fmj7Sz?2M#s8p}UU#V_ju7rVul z&(FKNtMt_s&*sEg55AT0`SmW+ofTKLY}2NqYilBx`^{aocJ0}dCokrDJ@~KOa_{Ts z`TuPc6&Jp&EwPsg`S;UH(%#;JxvH#Rcrled3&=g0T`|L>McU*J~! zvg@^+h?HW>biLT3yU(QTD_okr&+EkQD*6BK?>gOc<_}&Q%6{N)x$s&@NC-4ys#f;m z^78()!zRnNY`Idp+qs?3%8yB#lZR)HdH%fxj?J@fr2qf-H@^1k)HG$r>q;$AKfc%h z|9))WmA%#FcjFa8M4mo6+P&`f#EBEF{Fu5we*Qe$vUu6;OU8Nk>VD@=OKI-oSSZHE zCnF&%d-uWgy#0U6dfPK6{OXt>aAFBBOSulQwUt(t$|UiV#Ai@Bdgp$kX;i;Ihoe?D)2 z|IGg9)Ai%;?I>Kl-JNNjE63K$D}$H+ez)6y?@@*4uG!hySN{t?H+8D$TEG5%10(Y^ zoybjTXJ=ixa^1yS=65g$0j}j)_UhlM@pyEiKpY`E+XU_j|7&Uq0~p{I|Eaxw*Mb<#`tgI<4Iq z7Gr$k;ew*G+%2!pOS0RXOWS<6^7-82XJ-oM>6iZQ53jBLJIgft%Pd|aL8rAKDf7D} zlan3@yt3eQd3kN^?9VkX>;FBkzgKXWcimgiut&*@34P6uv!>NL)w;SK^|$}~WNF}& z9pCR&`_Hiul$6Yz5bU7tKd3Q<%>TuhC$@#nAZo8eg z`|XiVVbD^je}8|!e*HSW{_oew&1r>2OlvP+s&Cfie&}!icT4&Edt!Yod z-;EnL-mBJ$i17Z;yG^IXkCBm4P*8B~54RmX5{8E?*rlvjLKPM+A2L}apb$9<<-7zie?*4<!jc_bdZ%tupC?^?AC!?GvKzcV;wi-?Ks z`}Jyd{h!D3*;!d%=CL;H6m*(#rc+p5OgCyv-QQogZbj`)XG~yi5m@%|?e_b6F*^z_ zFY_%eEv-7wbik^jSKwJdXsBt@k&YKHUfj8JC-?TYyY>J7R{66WP_j^Jv1DOmtNZ4uU+>sf`SOr07U8fv=N zKO-Zgw_3+b>-TdT!sgXc5Y6#HB9D zeZSxB{`KouSk2>7RyMY8FD@;IN^AA2C_z}MXN;oa`{b`>8UfEJca-~Z?7Wq;4NJJ9bRY zx-92l6RV}A<+|E7e))eVl>2!kjh2)ee|dj@|DHX2O7Gv^a^%R7*xhAYA4&Iq$Y$J= z`}EXQW_G@qjY&t%@7Fy3w)De?4@LHc ze2ebZKAjqFmV3)2>&l7^8w_-hUFF&@77hY}dE_`{i=K{lAK2 z(GZcNX`5Z$-R=K=xqNQ-!Gi}u^(knXuB7D4qn)Nlj2p})zH|iW8XJGUv$I&*Jg+2o z<@)vKPoI`HOlrA3@AdWd<@X}?RD8U$GWhn79oFUVzFc~A?%=_Lx&IZb{zft6y12RJ z-P)q5sOb3DGkUI7Y1X;#Vj?0I`91RX`>tvWeB@DR=X6@3acWiQ>Thpvmp?kfd41Z; z%gg!YY%EMnu54Acx39mtDzs~n&Br6caz79E_4nuh=KrV_Tc_KQR`vazZSAiw)8p%I zZcTlDZti*8?{`Y~7oMMI+qLLMj@j3P0p1|<3;lanwYIkA-q_&ym+ckq*__e?>shCn zCm-us7rT4cyJt_I&b2Ilw(I`Z#KUZ^fo!}|C69Z}s|qdle&l(e`HW-XB8}SL-_D*m z5s-iK+_`&utG9nHtE&2Su$kSu?9GnC$Hy8P7-XMa=G-q95uK2b5EV7+bzW@j-7Zn> zS^uWZwJw*ltqKVgxvt$RcFefJeTG^~*P+^`?t1cXJ=*A)YcyFmtTLis;7O|9bIQHFy*F>(yxf2OyKS=%Kdg8@w_LueJJ$v@d?D?WsVwyTSUoPzuI$NV3;+^?9yD(})!om6f zzAR6BSM%!1${8~x@_QI9m-)@zm2{Nry49lfd%xY9q8Z%O)O6){&8L&<>i+XWL{c9e z>CCNn0cFQjj^w1IO`A5&t9ZnDeVS$Qvn5NGRD7$oFMfV*?Yec}9`Kh0#`C>%y!9uF zA@<0TBR#U#X4clXE5F~_S-d)Yec1l86&k0a^Y<&*D zo&E7Fn72;1A#Ps%zn|szDwl8DcCFIf*tq!7kD@Ih(N0%uRjwW9xxic{?7q#sB|xeckTm{`2Fu=goZ$nzoIOj=sGvcK62Q zfG+}l4lbeEqwbLQIGmwAj*|D(dz#Z>OQ zIV(a*GGpTX|Np+f+JAffzF(_~Eie4~_3P^DaP6*1vt~(&iY~of^Xp;fMqMAVLz^~j za+j~&vTIk>vokX_H8oG3Jo!qT^VRFu$9tupFTK9K*XMVu7TIq#lHU5wQ=jm>_!bvPR{T5>-WEYH&NMr zntuGe>C=~MoC@~0U3x!e*F(t#Z+(OhfeMEihKDQJ_IOX%d!?_crnc*^df}xdo@eWK zZ(r&8Z|jxo*H^!Y#`JS@BID!bWn}*Rc-;TmbW)s(J#)nbOQ(v5hgvT# zcE5h*%95o^O@Ht$1TXy5E=FGX+4v#8`*!u7EAscbvc3KM{Jgx1?w0ZXUw-N3W%V+XHbRy4GF6!Lgs-~*iD`Oe77qme0^LhL4ziO-=UN8FfCG+du zXEkx!I>|3CEZly#Y&K}YnUj-KQ{U%|{&WU@qbd$@y_g+2H;r5aYieuP|1JZyT~@xo zcJ11-Wy|C&3J!FCe%TU#`sL;2`~Q6M{yOdJ>+7G57Rs2-_N@)jcv~BGyV4eDxRL2ns;}XtBXs<{})mkT3V}Ctax#0 zX}4fpZ+CZh_5Z)$y}iAam6YyPK9}A6$23p*F5ET)zqx}8788c?= ze!p+`Q{in6_$OFr{+(-bs9v{QOt)yS@2g#qeHeSJ&TlPye=jyDXwr-sH&%!1_sT~} z|Np)JfAzOFH?80A3EtZ=Jx+$ty{6_*r?C3G%4ai|dQX34+b7my&urrU`X8@U$;Gz^ z4jd4RWr+v~c(6CI$N9(l)MsaA8mFJTQq3iCv`^OBZ;r)64=a7GKavNkd;Uo&GMKzL zYkogO1e9aU@7HX;xB0*w4n>B~g|#mx%{lB?!LP`YV0VsRt*5Wg&)4^Awb%?fMV163 zQBhIt@O2>~sc&vcSj?UZLlqU5zlqKcs|B4Hj(vT*{r;}K?0Mhc z-L3y|SYE_+rd4Uy^K)}cXK_zUy0G1!K|oJkJ^f%4Yinz3U0q%Ioxq)6>(^)!CL8g62rECRkK|ds7&;!SVETeR+cd9ECc5`HNuDSm!^(cJ93Qd{!x?^_wX{FSNbny%{{j1m`}`E5f20>Hi8 zD=UNdR(}W2(=&50@+-A4@T~Hlu6N$%bI-lt1HUXxxrXSH$v;saZNt~c>1t_x`k~Qq zGj?xP=zGB}1rHCg?saF7y0)vnc`fI|r>Cdy|M%;4SdB6R_m79|@^wERvhQ8aV6!Y$ zk%x=x)t#N2r@Jw(QPj}zcrUnTsdGDDRX;;ay!U_JTQYp@)7=;u4*b{=!A8NBL-2B` cZ~qz2bi6ZcdT?qU0|Nttr>mdKI;Vst0D!PzoB#j- literal 0 HcmV?d00001