From 3882e396954d25146a265376d36ecce45f89ad9d Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Mon, 24 Jun 2024 13:47:55 +0100 Subject: [PATCH 1/9] fix --- ...neration-chess-puzzles-with-dafny.markdown | 34 +++++-------------- 1 file changed, 9 insertions(+), 25 deletions(-) diff --git a/_posts/2023-12-06-automated-test-generation-chess-puzzles-with-dafny.markdown b/_posts/2023-12-06-automated-test-generation-chess-puzzles-with-dafny.markdown index 3084887..661e0b9 100644 --- a/_posts/2023-12-06-automated-test-generation-chess-puzzles-with-dafny.markdown +++ b/_posts/2023-12-06-automated-test-generation-chess-puzzles-with-dafny.markdown @@ -27,8 +27,7 @@ Now that we have definitions for all relevant chess rules, let us generate some Let us first define the method we want to test, called `Describe`, which prints whether or not a check or a checkmate has occurred. I annotate this method with the `{:testEntry}` attribute to mark it as an entry point for the generated tests. This method receives as input an arbitrary configuration of pieces on the board. In order to satisfy the chosen coverage criterion, Dafny will have to come up with such configurations of pieces when generating tests. -
-``` +```dafny // {:testEntry} tells Dafny to use this method as an entry point method {:testEntry} Describe(board: ValidBoard) { var whiteKing := board.pieces[0]; @@ -45,7 +44,6 @@ method {:testEntry} Describe(board: ValidBoard) { } } ``` -
Note that I also added an `expect` statement in the code. An `expect` statement is checked to be true at runtime and triggers a runtime exception if the check fails. In our case, the `expect` statement is trivially true (a checkmate always implies a check) and every test we generate passes it. In fact, if you were to turn this `expect` statement into an assertion, Dafny would prove it. Not every `expect` statement can be proven, however, especially in the presence of external libraries. You can read more about `expect` statements here. @@ -59,8 +57,7 @@ The `Block` keyword in the command tells Dafny to generate tests that together c In particular, running the command above results in the following two Dafny tests (formatted manually for this blog post). Don’t read too closely into the code just yet, we will visualize these tests soon. My point here is that Dafny produces tests written in Dafny itself and they can be translated to any of the languages the Dafny compiler supports. -
-``` +```dafny include "chess.dfy" module Tests { import opened Chess @@ -82,7 +79,6 @@ module Tests { } } ``` -
Note also that Dafny annotates the two test methods with the `{:test}` attribute. This means that after saving the tests to a file (`tests.dfy`), you can then use the `dafny test tests.dfy` command to compile and execute them. The default compilation target is C# but you can pick a different one using the `--target` option - read more about the `dafny-test` command [here](https://dafny.org/dafny/DafnyRef/DafnyRef#sec-dafny-test). @@ -115,14 +111,12 @@ The first two tests are essentially equivalent to the ones we got before. Only t
By default, Dafny test generation only guarantees coverage of statements or paths **within** the method annotated with `{:testEntry}` attribute. This means, in our case, that test generation would not differentiate between a check delivered by a pawn and one delivered by a knight, since the distinction between the two cases is hidden inside the `CheckedByPlayer` function. In order to cover these additional cases that are hidden within the callees of the test entry method, you need to *inline* them using the `{:testInline}` attribute as in the code snippet below. -
-``` +```dafny predicate {:testInline} CheckedByPlayer(board: ValidBoard, king: Piece, byPlayer: Color) { || CheckedByPiece(board, king, Knight(byPlayer)) || CheckedByPiece(board, king, Pawn(byPlayer)) } ``` -
Adding this annotation and running test generation while targeting path coverage wins us two more tests on top of the three we already had. We now have two checkmates, one for each piece leading the attack, and two checks. @@ -160,8 +154,7 @@ Large Dafny programs often make use of quantifiers, recursion, or loops. These c To illustrate these rules, let us condense a part of the Dafny chess model by making use of quantifiers. As a reminder, here is the unnecessarily verbose definition of the `ValidBoard` predicate we have been using so far to specify what kind of chess boards we are interested in: -
-``` +```dafny datatype Board = Board(pieces: seq) predicate BoardIsValid(board: Board) { // See Section 4 for how we can simplify this // We want boards with specific pieces on it: @@ -176,12 +169,10 @@ predicate BoardIsValid(board: Board) { // See Section 4 for how we can simplify && board.pieces[3].at != board.pieces[4].at } ``` -
There is a lot of repetition in the code above. In order to forbid two pieces from sharing the same square, we enumerate all 15 pairs of pieces! Worse, if we wanted to change the number of pieces on the board, we would have to rewrite the `BoardIsValid` predicate from scratch. A much more intuitive approach would be to use a universal quantifier over all pairs of pieces: -
-``` +```dafny datatype Board = Board(pieces: seq) predicate BoardIsValid(board: Board) { // No two pieces on a single square forall i: nat, j: nat :: @@ -190,12 +181,10 @@ predicate BoardIsValid(board: Board) { // No two pieces on a single square } type ValidBoard = board: Board | BoardIsValid(board) witness Board([]) ``` -
Similarly, we can use an existential quantifier within the body of the CheckedByPiece predicate, which returns true if the king is checked by a piece of a certain kind: -
-``` +```dafny predicate CheckedByPiece(board: ValidBoard, king: Piece, byPiece: Kind) { exists i: int :: && 0 <= i < |board.pieces| @@ -203,12 +192,10 @@ predicate CheckedByPiece(board: ValidBoard, king: Piece, byPiece: Kind) { && board.pieces[i].Threatens(king.at) } ``` -
If we want to require our board to have a king, two knights, and two pawns, like we did before, we can now separate this constraint into a separate predicate `BoardPreset` and require it to be true at the entry to the `Describe` method: -
-``` +```dafny predicate BoardPreset(board: Board) { && |board.pieces| == 5 && board.pieces[0].kind == King(White) @@ -216,14 +203,12 @@ predicate BoardPreset(board: Board) { && board.pieces[3].kind == Pawn(Black) && board.pieces[4].kind == Pawn(Black) } ``` -
This definition plays one crucial role that might be not immediately apparent. It explicitly enumerates all elements within the pieces sequence thereby *triggering* the quantifiers in `BoardIsValid` and `CheckedByPiece` predicates above. In other words, we tell Dafny that we know for a fact there are elements with indices `0`, `1`, etc. in this sequence and force the verifier to substitute these elements in the quantified axioms. The full theory of triggers and quantifiers is beyond the scope of this post, but if you want to combine test generation and quantifiers in your code, you must understand this point. I recommend reading [this part of the Dafny reference manual](https://dafny.org/dafny/DafnyRef/DafnyRef#sec-trigger) and/or [this FAQ](https://github.com/dafny-lang/dafny/wiki/FAQ#how-does-dafny-handle-quantifiers-ive-heard-about-triggers-what-are-those) that discusses the trigger selection process in Dafny. While Dafny can compile a subset of quantified expressions, it does not currently support inlining of such expressions for test generation purposes. This presents a challenge, as it means that we cannot immediately inline the `CheckedByPiece` predicate above. In order to inline such functions, we have to provide them with an alternative implementation, e.g. by turning the function into a [function-by-method](https://dafny.org/dafny/DafnyRef/DafnyRef#sec-function-by-method) and using a loop, like so: -
-``` +```dafny predicate CheckedByPiece(board: ValidBoard, king: Piece, byPiece: Kind) { exists i: int :: && 0 <= i < |board.pieces| @@ -241,7 +226,6 @@ predicate CheckedByPiece(board: ValidBoard, king: Piece, byPiece: Kind) { return false; } ``` -
Alternatively, we could have rewritten `CheckedByPiece` as a recursive function and put a `{:testInline 6}` annotation on it to unroll the recursion 6 times (6 is the maximum recursion depth for our example because it is one more than the number of pieces on the board). The test generation engine will then perform bounded model checking to produce system level tests. In general, reasoning about recursion and loops in bounded model checking context is known to be difficult, and so, while you have access to these "control knobs" that let you unroll the recursion in this manner (or unroll loops via the `-—loop-unroll` command line option), I would be cautious when combining these features with test generation. You can read [the paper](https://link.springer.com/chapter/10.1007/978-3-031-33170-1_24) on the test generation toolkit to get an idea about some of the challenges. Another consideration in deciding whether or not to unroll recursion and loops is your time budget. Unrolling increases the number of paths through the program and gives you better coverage but it also increases the time it takes to generate any given test. In the end, you will likely need to experiment with these settings to figure out what works best.

@@ -285,4 +269,4 @@ Thank you to the Dafny and Boogie developers for their invaluable feedback on th Thank you to the users of Dafny and the test generation tool in particular, who are a key motivation behind this project: Ryan Emery, Tony Knapp, Cody Roux, Horacio Mijail Anton Quiles, William Schultz, and Serdar Tasiran. - + \ No newline at end of file From 29e04266adae6b44b83a46791c6689cde317a1a1 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Mon, 24 Jun 2024 15:18:54 +0200 Subject: [PATCH 2/9] use correct z3 --- .github/workflows/main.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 560fc9b..cb9958b 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -27,7 +27,7 @@ jobs: - name: "Install Dafny" run: | git clone https://github.com/dafny-lang/dafny.git - cd dafny && make z3-mac && make exe + cd dafny && make z3-mac-arm && make exe - name: "Test Blogposts" run: | From f2bd9d3a9151f68f96103cb8ff378cd4ebbcd289 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Mon, 24 Jun 2024 15:28:58 +0200 Subject: [PATCH 3/9] some dotnet --- .github/workflows/main.yml | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index cb9958b..24c9d60 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -19,6 +19,14 @@ jobs: fetch-depth: 0 submodules: 'true' + - name: Setup dotnet + uses: actions/setup-dotnet@v4 + with: + dotnet-version: 6.0.x + + - name: Restore tools + run: dotnet tool restore + - name: "Install Node.js" uses: actions/setup-node@v3 with: From a6797198388c1500ff7f1cb777ae2742e21bb15a Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Mon, 24 Jun 2024 15:32:56 +0200 Subject: [PATCH 4/9] expect --- assets/src/brittleness/RationalAdd.dfy.expect | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/assets/src/brittleness/RationalAdd.dfy.expect b/assets/src/brittleness/RationalAdd.dfy.expect index bfc885e..3e45191 100644 --- a/assets/src/brittleness/RationalAdd.dfy.expect +++ b/assets/src/brittleness/RationalAdd.dfy.expect @@ -1,4 +1,4 @@ -RationalAdd.dfy(4,4): Warning: /!\ No terms found to trigger on. +RationalAdd.dfy(4,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. | 4 | exists n: int, m: int :: m > 0 && x == (n as real) / (m as real) | ^^^^^^ @@ -16,12 +16,12 @@ RationalAdd.dfy(17,12): Related location: this is the postcondition that could n RationalAdd.dfy(42,11): Error: assertion might not hold | 42 | assert (x1 as real) / (x2 as real) == ((x1 * y2) as real) / ((x2 * y2) as real); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ RationalAdd.dfy(43,11): Error: assertion might not hold | 43 | assert r == (((x1 * y2) + (y1 * x2)) as real) / (final_d as real); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Dafny program verifier finished with 9 verified, 3 errors From f0d49ebe4371f09c2db907c7fe943f375ee8ac74 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Mon, 24 Jun 2024 15:37:20 +0200 Subject: [PATCH 5/9] expect --- assets/src/brittleness/RationalAdd.dfy.expect | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/assets/src/brittleness/RationalAdd.dfy.expect b/assets/src/brittleness/RationalAdd.dfy.expect index 3e45191..52fc742 100644 --- a/assets/src/brittleness/RationalAdd.dfy.expect +++ b/assets/src/brittleness/RationalAdd.dfy.expect @@ -16,12 +16,12 @@ RationalAdd.dfy(17,12): Related location: this is the postcondition that could n RationalAdd.dfy(42,11): Error: assertion might not hold | 42 | assert (x1 as real) / (x2 as real) == ((x1 * y2) as real) / ((x2 * y2) as real); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ RationalAdd.dfy(43,11): Error: assertion might not hold | 43 | assert r == (((x1 * y2) + (y1 * x2)) as real) / (final_d as real); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Dafny program verifier finished with 9 verified, 3 errors From a5c5a964708c99d9fe910223df95694d45e3e656 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Mon, 24 Jun 2024 15:41:19 +0200 Subject: [PATCH 6/9] expect --- assets/src/brittleness/RationalAdd.dfy.expect | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/assets/src/brittleness/RationalAdd.dfy.expect b/assets/src/brittleness/RationalAdd.dfy.expect index 52fc742..3e45191 100644 --- a/assets/src/brittleness/RationalAdd.dfy.expect +++ b/assets/src/brittleness/RationalAdd.dfy.expect @@ -16,12 +16,12 @@ RationalAdd.dfy(17,12): Related location: this is the postcondition that could n RationalAdd.dfy(42,11): Error: assertion might not hold | 42 | assert (x1 as real) / (x2 as real) == ((x1 * y2) as real) / ((x2 * y2) as real); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ RationalAdd.dfy(43,11): Error: assertion might not hold | 43 | assert r == (((x1 * y2) + (y1 * x2)) as real) / (final_d as real); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Dafny program verifier finished with 9 verified, 3 errors From c1033aabfa8a4d71da4b0e8d21b30846eb622f9c Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Mon, 24 Jun 2024 15:58:21 +0200 Subject: [PATCH 7/9] ignore warnings --- assets/src/brittleness/verify.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/assets/src/brittleness/verify.sh b/assets/src/brittleness/verify.sh index cf5dbf7..2758b98 100755 --- a/assets/src/brittleness/verify.sh +++ b/assets/src/brittleness/verify.sh @@ -16,4 +16,4 @@ cd "$(dirname "$0")" (dafny verify RationalAdd.dfy > RationalAdd.dfy.out) || true diff -w --unified=3 --strip-trailing-cr RationalAdd.dfy.out RationalAdd.dfy.expect rm -f RationalAdd.dfy.out -dafny verify TriangleSum.dfy +dafny verify --allow-warnings TriangleSum.dfy From 690f5d0e5f47151f04695a404fd82001b43b9204 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 27 Jun 2024 16:14:23 +0200 Subject: [PATCH 8/9] ignore warnings and disable tests --- Makefile | 3 ++- assets/src/insertion-sort/verify.sh | 2 +- assets/src/proof-dependencies/verify.sh | 2 +- assets/src/semantics-of-regular-expressions/Languages.dfy | 4 ++-- assets/src/semantics-of-regular-expressions/verify.sh | 2 +- 5 files changed, 7 insertions(+), 6 deletions(-) diff --git a/Makefile b/Makefile index b0b5097..2327724 100644 --- a/Makefile +++ b/Makefile @@ -11,7 +11,8 @@ default: check check: node builders/verification-compelling-verify.js _includes/verification-compelling-intro.html assets/src/brittleness/verify.sh - assets/src/test-generation/verify.sh +# Doesn't terminate +# assets/src/test-generation/verify.sh assets/src/insertion-sort/verify.sh assets/src/proof-dependencies/verify.sh assets/src/brittleness/verify.sh diff --git a/assets/src/insertion-sort/verify.sh b/assets/src/insertion-sort/verify.sh index 731aac4..2a8e757 100755 --- a/assets/src/insertion-sort/verify.sh +++ b/assets/src/insertion-sort/verify.sh @@ -16,5 +16,5 @@ cd "$(dirname "$0")" for file in `ls *.dfy` do echo "Verifying $file..." - dafny verify $file + dafny verify --allow-warnings $file done \ No newline at end of file diff --git a/assets/src/proof-dependencies/verify.sh b/assets/src/proof-dependencies/verify.sh index da7f702..b40dae4 100755 --- a/assets/src/proof-dependencies/verify.sh +++ b/assets/src/proof-dependencies/verify.sh @@ -16,5 +16,5 @@ cd "$(dirname "$0")" for file in `ls *.dfy` do echo "Verifying $file..." - dafny verify $file + dafny verify --allow-warnings $file done diff --git a/assets/src/semantics-of-regular-expressions/Languages.dfy b/assets/src/semantics-of-regular-expressions/Languages.dfy index 0275910..826b9cf 100644 --- a/assets/src/semantics-of-regular-expressions/Languages.dfy +++ b/assets/src/semantics-of-regular-expressions/Languages.dfy @@ -139,7 +139,7 @@ module Languages5WithProof refines Languages5 { } } - lemma PlusCongruenceAlternative(k: nat, L1a: Lang, L1b: Lang, L2a: Lang, L2b: Lang) + lemma PlusCongruenceAlternative(k: nat, L1a: Lang, L1b: Lang, L2a: Lang, L2b: Lang) requires Bisimilar#[k](L1a, L1b) requires Bisimilar#[k](L2a, L2b) ensures Bisimilar#[k](Plus(L1a, L2a), Plus(L1b, L2b)) @@ -182,7 +182,7 @@ module Languages6 { import opened Languages4 import opened Languages5WithProof - greatest lemma BisimilarityIsTransitive[nat](L1: Lang, L2: Lang, L3: Lang) + greatest lemma BisimilarityIsTransitive[nat](L1: Lang, L2: Lang, L3: Lang) requires Bisimilar(L1, L2) && Bisimilar(L2, L3) ensures Bisimilar(L1, L3) {} diff --git a/assets/src/semantics-of-regular-expressions/verify.sh b/assets/src/semantics-of-regular-expressions/verify.sh index cb64eb9..fbeb1f7 100755 --- a/assets/src/semantics-of-regular-expressions/verify.sh +++ b/assets/src/semantics-of-regular-expressions/verify.sh @@ -16,5 +16,5 @@ cd "$(dirname "$0")" for file in `ls *.dfy` do echo "Verifying $file..." - dafny verify $file + dafny verify --allow-warnings $file done \ No newline at end of file From bd104f6c056120b055c6673f26b588425aafb7f5 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 27 Jun 2024 16:24:19 +0200 Subject: [PATCH 9/9] add asset --- .../semantics-of-regular-expressions/Archive.zip | Bin 0 -> 3665 bytes 1 file changed, 0 insertions(+), 0 deletions(-) create mode 100644 assets/src/semantics-of-regular-expressions/Archive.zip diff --git a/assets/src/semantics-of-regular-expressions/Archive.zip b/assets/src/semantics-of-regular-expressions/Archive.zip new file mode 100644 index 0000000000000000000000000000000000000000..cacbfa2d8dd1690028575780d95a04e5cb8d732c GIT binary patch literal 3665 zcmb7HXHXN`woa&0L+@1x5K52^QUo#5F?6IOy(WOvBS>%3d-2c(L=@7;TR_s5+%Yt5du_m911@Ab`m-&$}TLLvshjVqsThM5EY&&~({01$u& z01HC;I{EpzA-w&dj?Td*##8`OWtVQJJ6G#E`Ug<}fJAs80C1HA0Pr&CPK;8ee0wV5 zE3Ds;b!=Y4<2BZSZh4z5TUL@H&$r#U^B00nOwmHw_23|*Q;FS=-936MaHhN|+fD4; zTNV(Gj5}r82!;A{S0t9DhM)9EkVwZ==QKZRfEbY za_g*B%Ns0O`3!Jv@?8fO2!fou0kh<7+vdy7{HsaHxyl9|aF#{lQ`;G3G%LuVuR&VC zQ^Y&B7#%}(e!M>z2Nuhf1l4QGhAt8~6VrLd&-~*F&m0>j3-kWwXWlT;4o^ggIJKK>H2A=3ol8ZKjK|?9w6zQ zQ>S2YMK4V-DZr_BZsb7f`Kx59nZ8UiQsSU&H@4r^_D{aJSn z(>LJ*-2m)_B0dvJpOdB4Pabrtr3-CTG|V_ao2;6-yoTu7<#_LEskZdpSQXU~$EH+* zS-UA!bh8&d*%EQXoR&A_@o{Uc#gv%zCu4y`mqzkB8B9k61V9>$qi{^rt*v1bZFHhy>{4OFOF!b9sn{Vmkj&PSLc=dYtLl zv3f&p14T1G#@Dn!JQC*~?R6(r#rG65L7z*E3^_lRp^wHDUI8gWSg2*7Wx8_uPUTcaN>T7 z$`Qn=jhT{E+?~$ATb#pkAxnawNg3FdxPL|MEKX^cYN_@9>Qeb6A>pN>U@f-kbHs;F z8EYJqi$p$*+|~h}Y=f?}P$_}9N4)D9nH%vo+Eic`kl5A>=KBeRX=NqBbN8b0@WJpI z$GRFTiRn)R-5bAV2ep$YS?y5^zGu78jolVmGusmoo>9-~k5e=ZvG_qvHb(HE}Lkl6Hpv9XoML&t?Hi-X&Z@KRvZAD#SG{O0;qP-A^?DRZ_bYR}9D_5JX+@8>Y1Suooif>V z?KJsQ>Y2Xjn~{@=Z?2n*`M!$qqMm;-iNiMaZzOrj!MT;|?rZ0F#mc^C+(8MLDX8i4 zJilamyorbz(!TJta9dko8_>b>tHgcG#G4V5OdpfED;`qlwMc`e*Zt{+ zLZ_VTWEcp~VhnbcKOSX$Xbs~&w%2Un&C}eaV9|SLBZ;zEpWecMJpqPcV6lIG zVPY-3Bi19M5W0YKuReWA9V{qHs0i&lYsatm8?i((W@FHyjs;$v2Nj7T5P4}%JF;nD zylnFyVdJ}T`VP;WqJQm4v>SwB_(;<;;gY$IruhV35S)T|I=>&gMbm!iNqJ`o4`(2# zVopXUuat^D@LjJSOI8%&Iu`3&0)8-*I84;^xiw0l2h&_n_C>{xP4if+t4J*{Gs-5q z1s>KuCZ!=D!nLkF&q(%GY$ovWU&$L&q17_m9-VR&onmR|ds6_eC}HXW&d~B!`PUW{ z5)my-oGYfusfrJtmY_DvHa~ge%ZdOR!6w{xmfnnY-**K)_kSHkY;uh%FD}WiBhBPc zmT|{fe#`dDyH8imm%opwZg-4I-w)nf{BqZpBY)cUnMzMKv2!lC6r5=xSqfI)Bx19x zWwmog6_)21O$E9{=f%bD`|NRFlPo^>F()}O0B}vEf0OL*a%U*;za(qq3O!1s$c@8Ek zq~N&*5#Z*<{6pwcb`*0`M@KatJ{NwOTkD1;dn6jY$M8KS= zg!KGk2k1oY3(M<>kCuQM-bI9ri~Hm&27L#ffbpBLW|5I?T=9Zk!>{!+%L`2X9bj9i z5@9%x7HNR+guVHLWDgZ?AK497YS$5oEqsvbhd90_Q1+A>g}K=(@|$r^tLjnFym4Aj zo1Qg8Tu>pedCMU?C=qru!b8L<2D_Sw7ieR9$=;=plMiv!Zi(AxXdQau2uABJu zArV6#_JoyAprED{!$7!wLwLA$Kys>rXfAx~Gc{I8mGUT8C^bWNhC}kGKx?!()0Dd zZCQ6PCF&4$yD3toc%;$jnOsJKT45OA$sPik!Gp3v4U#1eFa*350C&Q5$+PU=+3FPZ z;Aj&Wnnxs@tiaalvd&6a5M8KPg9$2#rY5Sykgwd6@9g$B$#F8u&loo9%uYwUMtLPDw6`LdecpY65)HCQGGVQukc`>(_TF z_!L*LD(jbn3rc8{TrAZ4E{Q*vnU=4Ni*D;oz?Zk*^A$kr?*aGF=E4JkC##> z-pJV;Fy6hH;n7~AA}S4vN}7q=tZtJ=9L2vC;If^2#D>%-aP)kzAHtVYT33KeJzIQeYa3YO|vph_q6(P4Ea50G}`hAj*Z$$@BmTXhr5e6NU$tuJkUQ**`spA z-BN;4%y4+vg4!lp?6p2JaBLY_+rB8^_Y9J)ChxjP4j~jzEcre#g2V1JVl-z?R=&1Q zJ$tBm$eCW-zXZ`jro$A8T`nzIUU8i~3H9je8kt%Dk(j!Perc$wERAJ}k_z?Q?FD{N z^?axad5~q@2x~;*Ym#W|ckY~ArbZb**|xoD{IOh8Q+&)ovT)O+5Wgj;^kZ++w8nB2wpc)Yy$>_xMUcXMI-n%jx^wQxuV zSb~?YgyUKs;5tA82ExB5rQbXE>q+TfRuOT%`-gMW@5!&5|KAnsy7~W?RYW8L0sm|i n_&xQt