From 3dcb316a5ce97048073988b4bf4cb7ce3c486303 Mon Sep 17 00:00:00 2001 From: Andrey Kuprianov Date: Wed, 2 Sep 2020 12:31:15 +0200 Subject: [PATCH 01/10] #414: testgen tester -- utilities to run multiple tests with logs and reports --- testgen/Cargo.toml | 1 + testgen/src/tester.rs | 414 +++++++++++++++++++++++++++++++----------- 2 files changed, 307 insertions(+), 108 deletions(-) diff --git a/testgen/Cargo.toml b/testgen/Cargo.toml index 42855ed5e..5e1d2b5b6 100644 --- a/testgen/Cargo.toml +++ b/testgen/Cargo.toml @@ -11,6 +11,7 @@ serde_json = "1" ed25519-dalek = "1" gumdrop = "0.8.0" simple-error = "0.2.1" +tempfile = "3.1.0" [[bin]] name = "tendermint-testgen" diff --git a/testgen/src/tester.rs b/testgen/src/tester.rs index d905125c4..2b2c3902f 100644 --- a/testgen/src/tester.rs +++ b/testgen/src/tester.rs @@ -1,39 +1,115 @@ use crate::helpers::*; use crate::tester::TestResult::{Failure, ParseError, ReadError, Success}; use serde::de::DeserializeOwned; -use std::panic::UnwindSafe; -use std::{fs, path::PathBuf}; use std::{ - panic, + fs, + io::Write, + panic::{self, UnwindSafe}, + path::{Path, PathBuf}, sync::{Arc, Mutex}, }; +use tempfile::TempDir; +/// A test environment, which is essentially a wrapper around some directory, +/// with some utility functions operating relative to that directory. #[derive(Debug, Clone)] pub struct TestEnv { - root_dir: String, - logs: Vec, + /// Directory where the test is being executed + current_dir: String, } impl TestEnv { - pub fn add_log(&mut self, log: &str) { - self.logs.push(log.to_string()); + pub fn new(current_dir: &str) -> Option { + fs::create_dir_all(current_dir).ok().map(|_| TestEnv { + current_dir: current_dir.to_string(), + }) } - /// Read a file from a path relative to the environment root into a string - pub fn read_file(&mut self, path: &str) -> Option { - match self.full_path(path) { - None => None, - Some(full_path) => match fs::read_to_string(&full_path) { - Ok(file) => Some(file), - Err(_) => None, - }, + pub fn cleanup(&self) -> Option<()> { + fs::remove_dir_all(&self.current_dir) + .ok() + .and(fs::create_dir_all(&self.current_dir).ok()) + } + + pub fn push(&self, child: &str) -> Option { + let mut path = PathBuf::from(&self.current_dir); + path.push(child); + path.to_str().and_then(|path| TestEnv::new(path)) + } + + pub fn current_dir(&self) -> &str { + &self.current_dir + } + + pub fn logln(&self, msg: &str) -> Option<()> { + println!("{}", msg); + self.full_path("_log").and_then(|full_path| { + fs::OpenOptions::new() + .create(true) + .append(true) + .open(full_path) + .ok() + .and_then(|mut file| file.write_all((String::from(msg) + "\n").as_bytes()).ok()) + }) + } + + pub fn logln_to(&self, msg: &str, rel_path: &str) -> Option<()> { + println!("{}", msg); + self.full_path(rel_path).and_then(|full_path| { + fs::OpenOptions::new() + .create(true) + .append(true) + .open(full_path) + .ok() + .and_then(|mut file| file.write_all((String::from(msg) + "\n").as_bytes()).ok()) + }) + } + + /// Read a file from a path relative to the environment current dir into a string + pub fn read_file(&self, rel_path: &str) -> Option { + self.full_path(rel_path) + .and_then(|full_path| fs::read_to_string(&full_path).ok()) + } + + /// Write a file to a path relative to the environment current dir + pub fn write_file(&self, rel_path: &str, contents: &str) -> Option<()> { + self.full_path(rel_path) + .and_then(|full_path| fs::write(full_path, contents).ok()) + } + + /// Parse a file from a path relative to the environment current dir as the given type + pub fn parse_file_as(&self, rel_path: &str) -> Option { + self.read_file(rel_path) + .and_then(|input| serde_json::from_str(&input).ok()) + } + + /// Copy a file from the path outside environment into the environment current dir + /// Returns the relative path of the file, or None if copying was not successful + pub fn copy_file_from(&self, path: &str) -> Option { + let path = Path::new(path); + if !path.is_file() { + return None; } + path.file_name().and_then(|name| { + name.to_str().and_then(|name| { + self.full_path(name) + .and_then(|dest| fs::copy(path, dest).ok().map(|_| name.to_string())) + }) + }) + } + + /// Copy a file from the path relative to the other environment into the environment current dir + /// Returns the relative path of the file, or None if copying was not successful + pub fn copy_file_from_env(&self, other: &TestEnv, path: &str) -> Option { + other + .full_path(path) + .and_then(|full_path| self.copy_file_from(&full_path)) } /// Convert a relative path to the full path from the test root /// Return None if the full path can't be formed pub fn full_path(&self, rel_path: &str) -> Option { - let full_path = PathBuf::from(&self.root_dir).join(rel_path); + let full_path = PathBuf::from(&self.current_dir).join(rel_path); match full_path.to_str() { None => None, Some(full_path) => Some(full_path.to_string()), @@ -41,9 +117,9 @@ impl TestEnv { } /// Convert a full path to the path relative to the test root - /// Return None if the full path doesn't contain test root as prefix + /// Returns None if the full path doesn't contain test root as prefix pub fn rel_path(&self, full_path: &str) -> Option { - match PathBuf::from(full_path).strip_prefix(&self.root_dir) { + match PathBuf::from(full_path).strip_prefix(&self.current_dir) { Err(_) => None, Ok(rel_path) => match rel_path.to_str() { None => None, @@ -51,28 +127,71 @@ impl TestEnv { }, } } -} -type TestFn = Box TestResult>; - -pub struct Tester { - root_dir: String, - tests: Vec<(String, TestFn)>, - results: std::collections::BTreeMap>, + /// Convert a relative path to the full path from the test root, canonicalized + /// Returns None the full path can't be formed + pub fn full_canonical_path(&self, rel_path: &str) -> Option { + let full_path = PathBuf::from(&self.current_dir).join(rel_path); + full_path + .canonicalize() + .ok() + .and_then(|p| p.to_str().map(|x| x.to_string())) + } } #[derive(Debug, Clone)] pub enum TestResult { ReadError, ParseError, - Success(TestEnv), + Success, Failure { message: String, location: String }, } +/// A function that takes as input the test file path and its content, +/// and returns the result of running the test on it +type TestFn = Box TestResult>; + +/// A function that takes as input the batch file path and its content, +/// and returns the vector of test names/contents for tests in the batch, +/// or None if the batch could not be parsed +type BatchFn = Box Option>>; + +pub struct Test { + /// test name + pub name: String, + /// test function + pub test: TestFn, +} + +/// Tester allows you to easily run some test functions over a set of test files. +/// You create a Tester instance with the reference to some specific directory, containing your test files. +/// After a creation, you can add several types of tests there: +/// * add_test() adds a simple test function, which can run on some test, deserilizable from a file. +/// * add_test_with_env() allows your test function to receive several test environments, +/// so that it can easily perform some operations on files when necessary +/// * add_test_batch() adds a batch of test: a function that accepts a ceserializable batch description, +/// and produces a set of test from it +/// +/// After you have added all your test functions, you run Tester either on individual files +/// using run_for_file(), or for whole directories, using run_foreach_in_dir(); +/// the directories will be traversed recursively top-down. +/// +/// The last step involves calling the finalize() function, which will produce the test report +/// and panic in case there was at least one failing test. +/// When there are files in the directories you run Tester on, that could not be read/parsed, +/// it is also considered an error, and leads to panic. +pub struct Tester { + name: String, + root_dir: String, + tests: Vec, + batches: Vec, + results: std::collections::BTreeMap>, +} + impl TestResult { pub fn is_success(&self) -> bool { match self { - TestResult::Success(_) => true, + TestResult::Success => true, _ => false, } } @@ -100,24 +219,29 @@ impl TestResult { } impl Tester { - pub fn new(root_dir: &str) -> Tester { + pub fn new(name: &str, root_dir: &str) -> Tester { Tester { + name: name.to_string(), root_dir: root_dir.to_string(), tests: vec![], + batches: vec![], results: Default::default(), } } - pub fn env(&self) -> TestEnv { - TestEnv { - root_dir: self.root_dir.clone(), - logs: vec![], - } + pub fn env(&self) -> Option { + TestEnv::new(&self.root_dir) } - fn capture_test(env: TestEnv, test: F) -> TestResult + pub fn output_env(&self) -> Option { + fs::create_dir_all(self.root_dir.clone() + "/_" + &self.name) + .ok() + .and(TestEnv::new(&(self.root_dir.clone() + "/_" + &self.name))) + } + + fn capture_test(test: F) -> TestResult where - F: FnOnce(TestEnv) -> TestEnv + UnwindSafe, + F: FnOnce() + UnwindSafe, { let test_result = Arc::new(Mutex::new(ParseError)); let old_hook = panic::take_hook(); @@ -139,11 +263,10 @@ impl Tester { *result = Failure { message, location }; }) }); - let test_fun = || test(env.clone()); - let result = panic::catch_unwind(test_fun); + let result = panic::catch_unwind(|| test()); panic::set_hook(old_hook); match result { - Ok(res) => Success(res), + Ok(_) => Success, Err(_) => (*test_result.lock().unwrap()).clone(), } } @@ -152,60 +275,79 @@ impl Tester { where T: 'static + DeserializeOwned + UnwindSafe, { - let test_env = self.env(); - let test_fn = move |input: &str| match parse_as::(&input) { - Ok(test_case) => Tester::capture_test(test_env.clone(), |env| { + let test_fn = move |_path: &str, input: &str| match parse_as::(&input) { + Ok(test_case) => Tester::capture_test(|| { test(test_case); - env }), Err(_) => ParseError, }; - self.tests.push((name.to_string(), Box::new(test_fn))); + self.tests.push(Test { + name: name.to_string(), + test: Box::new(test_fn), + }); } - pub fn add_test_with_env(&mut self, name: &str, test: fn(T, &mut TestEnv)) + pub fn add_test_with_env(&mut self, name: &str, test: fn(T, &TestEnv, &TestEnv, &TestEnv)) where T: 'static + DeserializeOwned + UnwindSafe, { - let test_env = self.env(); - let test_fn = move |input: &str| match parse_as::(&input) { - Ok(test_case) => Tester::capture_test(test_env.clone(), |env| { - let mut env = env; - test(test_case, &mut env); - env + let test_env = self.env().unwrap(); + let output_env = self.output_env().unwrap(); + let test_fn = move |path: &str, input: &str| match parse_as::(&input) { + Ok(test_case) => Tester::capture_test(|| { + // It is OK to unwrap() here: in case of unwrapping failure, the test will fail. + let dir = TempDir::new().unwrap(); + let env = TestEnv::new(dir.path().to_str().unwrap()).unwrap(); + let output_dir = output_env.full_path(path).unwrap(); + let output_env = TestEnv::new(&output_dir).unwrap(); + output_env.cleanup(); + test(test_case, &env, &test_env, &output_env); }), Err(_) => ParseError, }; - self.tests.push((name.to_string(), Box::new(test_fn))); + self.tests.push(Test { + name: name.to_string(), + test: Box::new(test_fn), + }); + } + + pub fn add_test_batch(&mut self, batch: fn(T) -> Vec<(String, String)>) + where + T: 'static + DeserializeOwned, + { + let batch_fn = move |_path: &str, input: &str| match parse_as::(&input) { + Ok(test_batch) => Some(batch(test_batch)), + Err(_) => None, + }; + self.batches.push(Box::new(batch_fn)); } - fn add_result(&mut self, name: &str, path: &str, result: TestResult) { + fn results_for(&mut self, name: &str) -> &mut Vec<(String, TestResult)> { self.results .entry(name.to_string()) .or_insert_with(Vec::new) - .push((path.to_string(), result)) + } + + fn add_result(&mut self, name: &str, path: &str, result: TestResult) { + self.results_for(name).push((path.to_string(), result)); } fn read_error(&mut self, path: &str) { - self.results - .entry("".to_string()) - .or_insert_with(Vec::new) + self.results_for("") .push((path.to_string(), TestResult::ReadError)) } fn parse_error(&mut self, path: &str) { - self.results - .entry("".to_string()) - .or_insert_with(Vec::new) + self.results_for("") .push((path.to_string(), TestResult::ParseError)) } - pub fn successful_tests(&self, test: &str) -> Vec<(String, TestEnv)> { + pub fn successful_tests(&self, test: &str) -> Vec { let mut tests = Vec::new(); if let Some(results) = self.results.get(test) { for (path, res) in results { - if let Success(env) = res { - tests.push((path.clone(), env.clone())) + if let Success = res { + tests.push(path.clone()) } } } @@ -248,63 +390,47 @@ impl Tester { tests } - pub fn print_results(&mut self) { - let tests = self.unreadable_tests(); - if !tests.is_empty() { - println!("Unreadable tests: "); - for path in tests { - println!(" > {}", path) + fn run_for_input(&mut self, path: &str, input: &str) { + let mut results = Vec::new(); + for Test { name, test } in &self.tests { + match test(path, input) { + TestResult::ParseError => continue, + res => results.push((name.to_string(), path, res)), } - panic!("Some tests could not be read"); } - let tests = self.unparseable_tests(); - if !tests.is_empty() { - println!("Unparseable tests: "); - for path in tests { - println!(" > {}", path) + if !results.is_empty() { + for (name, path, res) in results { + self.add_result(&name, path, res) } - panic!("Some tests could not be parsed"); - } - - for name in self.results.keys() { - println!("Results for '{}'", name); - let tests = self.successful_tests(name); - if !tests.is_empty() { - println!(" Successful tests: "); - for (path, _) in tests { - println!(" > {}", path) + } else { + // parsing as a test failed; try parse as a batch + let mut res_tests = Vec::new(); + for batch in &self.batches { + match batch(path, input) { + None => continue, + Some(tests) => { + for (name, input) in tests { + let test_path = path.to_string() + "/" + &name; + res_tests.push((test_path, input)); + } + } } } - let tests = self.failed_tests(name); - if !tests.is_empty() { - println!(" Failed tests: "); - for (path, message, location) in tests { - println!(" > {}, '{}', {}", path, message, location) + if !res_tests.is_empty() { + for (path, input) in res_tests { + self.run_for_input(&path, &input); } - panic!("Some tests failed"); + } else { + // parsing both as a test and as a batch failed + self.parse_error(path); } } } pub fn run_for_file(&mut self, path: &str) { - match self.env().read_file(path) { + match self.env().unwrap().read_file(path) { None => self.read_error(path), - Some(input) => { - let mut results = Vec::new(); - for (name, test) in &self.tests { - match test(&input) { - TestResult::ParseError => continue, - res => results.push((name.to_string(), path, res)), - } - } - if results.is_empty() { - self.parse_error(path); - } else { - for (name, path, res) in results { - self.add_result(&name, path, res) - } - } - } + Some(input) => self.run_for_input(path, &input), } } @@ -317,9 +443,17 @@ impl Tester { Ok(paths) => { for path in paths { if let Ok(entry) = path { + // ignore path components starting with '_' + if let Some(last) = entry.path().iter().rev().next() { + if let Some(last) = last.to_str() { + if last.starts_with('_') { + continue; + } + } + } if let Ok(kind) = entry.file_type() { let path = format!("{}", entry.path().display()); - let rel_path = self.env().rel_path(&path).unwrap(); + let rel_path = self.env().unwrap().rel_path(&path).unwrap(); if kind.is_file() || kind.is_symlink() { if !rel_path.ends_with(".json") { continue; @@ -336,4 +470,68 @@ impl Tester { }, } } + + pub fn finalize(&mut self) { + let env = self.output_env().unwrap(); + env.write_file("_report", ""); + let print = |msg: &str| { + env.logln_to(msg, "_report"); + }; + let mut do_panic = false; + + print(&format!( + "\n====== Report for '{}' tester run ======", + &self.name + )); + for name in self.results.keys() { + if name.is_empty() { + continue; + } + print(&format!("\nResults for '{}'", name)); + let tests = self.successful_tests(name); + if !tests.is_empty() { + print(" Successful tests: "); + for path in tests { + print(&format!(" {}", path)); + if let Some(logs) = env.read_file(&(path + "/_log")) { + print(&logs) + } + } + } + let tests = self.failed_tests(name); + if !tests.is_empty() { + do_panic = true; + print(" Failed tests: "); + for (path, message, location) in tests { + print(&format!(" {}, '{}', {}", path, message, location)); + if let Some(logs) = env.read_file(&(path + "/_log")) { + print(&logs) + } + } + } + } + let tests = self.unreadable_tests(); + if !tests.is_empty() { + do_panic = true; + print("\nUnreadable tests: "); + for path in tests { + print(&format!(" {}", path)) + } + } + let tests = self.unparseable_tests(); + if !tests.is_empty() { + do_panic = true; + print("\nUnparseable tests: "); + for path in tests { + print(&format!(" {}", path)) + } + } + print(&format!( + "\n====== End of report for '{}' tester run ======\n", + &self.name + )); + if do_panic { + panic!("Some tests failed or could not be read/parsed"); + } + } } From b5853cab3585e1ec714c98c907cca50177e00cc4 Mon Sep 17 00:00:00 2001 From: Andrey Kuprianov Date: Wed, 2 Sep 2020 13:32:14 +0200 Subject: [PATCH 02/10] 14: add testgen commands, in particular to call apalache and jsonatr --- testgen/jsonatr-lib/apalache-tendermint.json | 150 ++++++++++++++++++ .../jsonatr-lib/apalache_to_lite_test.json | 42 +++++ testgen/jsonatr-lib/tendermint.json | 31 ++++ testgen/jsonatr-lib/unix.json | 29 ++++ testgen/src/apalache.rs | 122 ++++++++++++++ testgen/src/command.rs | 82 ++++++++++ testgen/src/jsonatr.rs | 36 +++++ testgen/src/lib.rs | 16 +- 8 files changed, 505 insertions(+), 3 deletions(-) create mode 100644 testgen/jsonatr-lib/apalache-tendermint.json create mode 100644 testgen/jsonatr-lib/apalache_to_lite_test.json create mode 100644 testgen/jsonatr-lib/tendermint.json create mode 100644 testgen/jsonatr-lib/unix.json create mode 100644 testgen/src/apalache.rs create mode 100644 testgen/src/command.rs create mode 100644 testgen/src/jsonatr.rs diff --git a/testgen/jsonatr-lib/apalache-tendermint.json b/testgen/jsonatr-lib/apalache-tendermint.json new file mode 100644 index 000000000..d56efc334 --- /dev/null +++ b/testgen/jsonatr-lib/apalache-tendermint.json @@ -0,0 +1,150 @@ +{ + "description": "Transformers for Apalache counterexamples (CEs) with Tendermint blockchains", + "use": [ + "tendermint.json" + ], + "input": [ + { + "name": "first_state", + "description": "extract the first state from Apalache CE", + "kind": "INLINE", + "source": "$.declarations[1].body.and | unwrap" + }, + { + "name": "last_state", + "description": "extract the last state from Apalache CE", + "kind": "INLINE", + "source": "$.declarations[-2].body.and | unwrap" + }, + { + "name": "history", + "description": "extract the history from the last state of Apalache CE", + "kind": "INLINE", + "source": "$last_state..[?(@.eq == 'history')].arg.atat..arg.record" + }, + { + "name": "states", + "description": "extract all state from Apalache CE", + "kind": "INLINE", + "source": "$.declarations[1:-1].body.and" + }, + { + "name": "lightblock_commits", + "description": "extract commits from a LightClient block of Apalache CE", + "kind": "INLINE", + "source": "$..[?(@.key.str == 'Commits')].value..str" + }, + { + "name": "block_validators", + "description": "extract validators from a block of Apalache CE", + "kind": "INLINE", + "source": "$..[?(@.key.str == 'VS')].value..str" + }, + { + "name": "block_next_validators", + "description": "extract next validators from a block of Apalache CE", + "kind": "INLINE", + "source": "$..[?(@.key.str == 'NextVS')].value..str" + }, + { + "name": "block_height", + "description": "extract height from a block of Apalache CE", + "kind": "INLINE", + "source": "$..[?(@.key.str == 'height')].value | unwrap" + }, + { + "name": "block_time", + "description": "extract time from a block of Apalache CE", + "kind": "INLINE", + "source": "$..[?(@.key.str == 'time')].value | unwrap" + }, + { + "name": "id_to_validator", + "description": "transform an identifier into a validator expected by `tendermint-testgen validator`", + "kind": "INLINE", + "source": { + "id": "$", + "voting_power": 50 + } + }, + { + "name": "id_to_vote", + "description": "transform an identifier into a vote expected by `tendermint-testgen vote`", + "kind": "INLINE", + "source": { + "validator": "$ | id_to_validator", + "header": "$header" + } + }, + { + "name": "block_to_header", + "description": "transform a block from Apalache CE into a header expected by `tendermint-testgen header`", + "kind": "INLINE", + "source": { + "validators": "$ | block_validators | map(id_to_validator)", + "next_validators": "$ | block_next_validators | map(id_to_validator)", + "height": "$ | block_height", + "time": "$ | block_time" + } + }, + { + "name": "block_to_commit", + "description": "transform a block from Apalache CE into a commit expected by `tendermint-testgen commit`", + "kind": "INLINE", + "let": { + "header": "$ | block_to_header" + }, + "source": { + "header": "$header", + "votes": "$ | lightblock_commits | map(id_to_vote)" + } + }, + { + "name": "ids_to_validators", + "description": "transform a non-empty array of identifiers into Tendermint validators", + "kind": "INLINE", + "source": "$ | map(id_to_validator) | map(tendermint_validator)" + }, + { + "name": "empty_array", + "description": "just an empty array", + "kind": "INLINE", + "source": [] + }, + { + "name": "first_validator", + "description": "extract first validator from a non-empty array of identifiers", + "kind": "INLINE", + "source": "$[0] | unwrap | id_to_validator | tendermint_validator" + }, + { + "name": "const_id", + "description": "constant identifier", + "kind": "INLINE", + "source": "a" + }, { + "name": "fixed_validator", + "description": "extract first validator from a non-empty array of identifiers", + "kind": "INLINE", + "source": "$const_id | id_to_validator | tendermint_validator" + }, + { + "name": "ids_to_validator_set", + "description": "transform an array of identifiers into a JSON-encoded Tendermint validator set", + "kind": "INLINE", + "source": { + "validators": "$ | ifelse(ids_to_validators,empty_array)", + "proposer": "$ | ifelse(first_validator,fixed_validator)" + } + }, + { + "name": "block_to_signed_header", + "description": "transform a block from Apalache CE into a JSON-encoded Tendermint signed header", + "kind": "INLINE", + "source": { + "header": "$ | block_to_header | tendermint_header", + "commit": "$ | block_to_commit | tendermint_commit" + } + } + ] +} \ No newline at end of file diff --git a/testgen/jsonatr-lib/apalache_to_lite_test.json b/testgen/jsonatr-lib/apalache_to_lite_test.json new file mode 100644 index 000000000..0df1663f0 --- /dev/null +++ b/testgen/jsonatr-lib/apalache_to_lite_test.json @@ -0,0 +1,42 @@ +{ + "description": "Transform an Apalache counterexample into a Tendermint LightClient test", + "use": [ + "unix.json", + "apalache-tendermint.json" + ], + "input": [ + { + "name": "block_to_initial_block", + "description": "transforms a block from Apalache CE into a JSON-encoded Tendermint initial light block", + "kind": "INLINE", + "source": { + "signed_header": "$ | block_to_signed_header", + "next_validator_set": "$ | block_next_validators | ids_to_validator_set", + "trusting_period": "1400000000000", + "now": "$utc_timestamp" + } + }, + { + "name": "state_to_lite_block_verdict", + "description": "transforms a block from Apalache CE into a JSON-encoded Tendermint light block", + "kind": "INLINE", + "let": { + "block": "$..[?(@.key.str == 'current')].value" + }, + "source": { + "block": { + "signed_header": "$block | block_to_signed_header", + "validator_set": "$block | block_validators | ids_to_validator_set", + "next_validator_set": "$block | block_next_validators | ids_to_validator_set" + }, + "now": "$..[?(@.key.str == 'now')].value | unwrap | tendermint_time", + "verdict": "$..[?(@.key.str == 'verdict')].value.str | unwrap" + } + } + ], + "output": { + "description": "auto-generated from Apalache counterexample", + "initial": "$history[0]..[?(@.key.str == 'current')].value | block_to_initial_block", + "input": "$history[1:] | map(state_to_lite_block_verdict)" + } +} diff --git a/testgen/jsonatr-lib/tendermint.json b/testgen/jsonatr-lib/tendermint.json new file mode 100644 index 000000000..ba119bd81 --- /dev/null +++ b/testgen/jsonatr-lib/tendermint.json @@ -0,0 +1,31 @@ +{ + "description": "Transformers for generating Tendermint datastructures", + "prerequisites": "add tendermint-testgen to your $PATH", + "input": [ + { + "name": "tendermint_validator", + "kind": "COMMAND", + "source": "tendermint-testgen --stdin validator" + }, + { + "name": "tendermint_header", + "kind": "COMMAND", + "source": "tendermint-testgen --stdin header" + }, + { + "name": "tendermint_commit", + "kind": "COMMAND", + "source": "tendermint-testgen --stdin commit" + }, + { + "name": "tendermint_vote", + "kind": "COMMAND", + "source": "tendermint-testgen --stdin vote" + }, + { + "name": "tendermint_time", + "kind": "COMMAND", + "source": "tendermint-testgen --stdin time" + } + ] +} diff --git a/testgen/jsonatr-lib/unix.json b/testgen/jsonatr-lib/unix.json new file mode 100644 index 000000000..ee31c113b --- /dev/null +++ b/testgen/jsonatr-lib/unix.json @@ -0,0 +1,29 @@ +{ + "description": "Useful external commands", + "input": [ + { + "name": "date", + "kind": "COMMAND", + "source": "date -I", + "stdin": false + }, + { + "name": "utc_timestamp", + "kind": "COMMAND", + "source": "date --utc +%FT%H:%M:%S.%NZ", + "stdin": false + }, + { + "name": "utc_timestamp_hour_ago", + "kind": "COMMAND", + "source": "date --utc +%FT%H:%M:%S.%NZ --date '-1 hour'", + "stdin": false + }, + { + "name": "utc_timestamp_2hours_ago", + "kind": "COMMAND", + "source": "date --utc +%FT%H:%M:%S.%NZ --date '-2 hour'", + "stdin": false + } + ] +} \ No newline at end of file diff --git a/testgen/src/apalache.rs b/testgen/src/apalache.rs new file mode 100644 index 000000000..1c0ce83aa --- /dev/null +++ b/testgen/src/apalache.rs @@ -0,0 +1,122 @@ +use crate::{command::*, tester::TestEnv}; +use serde::{Deserialize, Serialize}; +use std::io; + +#[derive(Deserialize, Clone, Debug)] +pub struct ApalacheTestBatch { + pub description: String, + pub model: String, + pub length: Option, + pub timeout: Option, + pub tests: Vec, +} + +#[derive(Serialize, Deserialize, Clone, Debug)] +pub struct ApalacheTestCase { + pub model: String, + pub test: String, + pub length: Option, + pub timeout: Option, +} + +pub enum ApalacheRun { + /// Apalache has found a counterexample + Counterexample(CommandRun), + /// Apalache has not found a counterexample up to specified length bound + NoCounterexample(CommandRun), + /// Apalache has found a deadlock + Deadlock(CommandRun), + /// Apalache model checking run failed (e.g. a parsing error) + ModelError(CommandRun), + /// Apalache returned an unknown error code + Unknown(CommandRun), + /// The tool has reached the specified timeout without producing an answer + Timeout(CommandRun), +} + +impl ApalacheRun { + pub fn message(&self) -> &str { + match self { + ApalacheRun::Counterexample(_) => "Apalache has generated a counterexample", + ApalacheRun::NoCounterexample(_) => "Apalache failed to generate a counterexample; consider increasing the length bound, or changing your test", + ApalacheRun::Deadlock(_) => "Apalache has found a deadlock; please inspect your model and test", + ApalacheRun::ModelError(_) => "Apalache failed to process the model; please check it", + ApalacheRun::Unknown(_) => "Apalache has generated an unknown outcome; please contact Apalache developers", + ApalacheRun::Timeout(_) => "Apalache failed to generate a counterexample within given time; consider increasing the timeout, or changing your test", + } + } +} + +pub fn run_apalache_test(dir: &str, test: ApalacheTestCase) -> io::Result { + let inv = test.test.clone() + "Inv"; + + // Mutate the model: negate the test assertion to get the invariant to check + let mutation_failed = || { + io::Error::new( + io::ErrorKind::InvalidInput, + "failed to mutate the model and add invariant", + ) + }; + let env = TestEnv::new(dir).ok_or_else(mutation_failed)?; + let model = env.read_file(&test.model).unwrap(); + let mut new_model = String::new(); + for line in model.lines() { + if line.starts_with(&inv) { + // invariant already present; skip mutation + new_model.clear(); + break; + } + if line.starts_with("======") { + new_model += &(inv.clone() + " == ~" + &test.test + "\n") + } + new_model += line; + new_model += "\n"; + } + if !new_model.is_empty() { + env.write_file(&test.model, &new_model) + .ok_or_else(mutation_failed)?; + } + + // Run Apalache, and process the result + let mut cmd = Command::new(); + if let Some(timeout) = test.timeout { + cmd.program("timeout"); + cmd.arg(&timeout.to_string()); + cmd.arg("apalache-mc"); + } else { + cmd.program("apalache-mc"); + } + cmd.arg("check"); + cmd.arg_from_parts(vec!["--inv=", &inv]); + if let Some(length) = test.length { + cmd.arg_from_parts(vec!["--length=", &length.to_string()]); + } + cmd.arg(&test.model); + if !dir.is_empty() { + cmd.current_dir(dir); + } + match cmd.spawn() { + Ok(run) => { + if run.status.success() { + if run.stdout.contains("The outcome is: NoError") { + Ok(ApalacheRun::NoCounterexample(run)) + } else if run.stdout.contains("The outcome is: Error") { + Ok(ApalacheRun::Counterexample(run)) + } else if run.stdout.contains("The outcome is: Deadlock") { + Ok(ApalacheRun::Deadlock(run)) + } else { + Ok(ApalacheRun::Unknown(run)) + } + } else if let Some(code) = run.status.code() { + match code { + 99 => Ok(ApalacheRun::ModelError(run)), + 124 => Ok(ApalacheRun::Timeout(run)), + _ => Ok(ApalacheRun::Unknown(run)), + } + } else { + Ok(ApalacheRun::Timeout(run)) + } + } + Err(e) => Err(e), + } +} diff --git a/testgen/src/command.rs b/testgen/src/command.rs new file mode 100644 index 000000000..c6aca4576 --- /dev/null +++ b/testgen/src/command.rs @@ -0,0 +1,82 @@ +use std::io::Read; +use std::{io, process}; + +/// A thin wrapper around process::Command to facilitate running external commands. +pub struct Command { + program: Option, + args: Vec, + dir: Option, +} + +/// The result of a command execution if the child process managed to execute +pub struct CommandRun { + pub status: process::ExitStatus, + pub stdout: String, + pub stderr: String, +} + +impl Command { + /// Check whether the given program can be executed + pub fn exists_program(program: &str) -> bool { + Command::new().program(program).spawn().is_ok() + } + /// Construct a new Command + pub fn new() -> Command { + Command { + program: None, + args: vec![], + dir: None, + } + } + /// Set the program to run + pub fn program(&mut self, program: &str) -> &mut Self { + self.program = Some(program.to_owned()); + self + } + /// Add a new program argument + pub fn arg(&mut self, arg: &str) -> &mut Self { + self.args.push(arg.to_owned()); + self + } + /// Add a new program argument, concatenated from several parts + pub fn arg_from_parts(&mut self, parts: Vec<&str>) -> &mut Self { + let mut arg: String = String::new(); + for part in parts { + arg += part; + } + self.args.push(arg); + self + } + /// Set the working directory for the child process + pub fn current_dir(&mut self, dir: &str) -> &mut Self { + self.dir = Some(dir.to_owned()); + self + } + /// Execute the command as a child process, and extract its status, stdout, stderr. + pub fn spawn(&mut self) -> io::Result { + match &self.program { + None => Err(io::Error::new(io::ErrorKind::InvalidInput, "")), + Some(program) => { + let mut command = process::Command::new(program); + command + .args(&self.args) + .stdout(process::Stdio::piped()) + .stderr(process::Stdio::piped()); + if let Some(dir) = &self.dir { + command.current_dir(dir); + } + let mut process = command.spawn()?; + let status = process.wait()?; + let mut stdout = String::new(); + process.stdout.unwrap().read_to_string(&mut stdout)?; + let mut stderr = String::new(); + process.stderr.unwrap().read_to_string(&mut stderr)?; + Ok(CommandRun { + status, + stdout, + stderr, + }) + } + } + } +} diff --git a/testgen/src/jsonatr.rs b/testgen/src/jsonatr.rs new file mode 100644 index 000000000..028065417 --- /dev/null +++ b/testgen/src/jsonatr.rs @@ -0,0 +1,36 @@ +use crate::command::*; +use serde::Deserialize; +use std::io; + +#[derive(Deserialize, Clone, Debug)] +pub struct JsonatrTransform { + pub input: String, + pub include: Vec, + pub output: String, +} + +pub fn run_jsonatr_transform(dir: &str, transform: JsonatrTransform) -> io::Result { + let mut cmd = Command::new(); + cmd.program("jsonatr"); + cmd.arg("--in"); + cmd.arg(&transform.input); + cmd.arg("--out"); + cmd.arg(&transform.output); + for include in transform.include { + cmd.arg("--use"); + cmd.arg(&include); + } + if !dir.is_empty() { + cmd.current_dir(dir); + } + match cmd.spawn() { + Ok(run) => { + if run.status.success() { + Ok(run) + } else { + Err(io::Error::new(io::ErrorKind::Interrupted, run.stderr)) + } + } + Err(e) => Err(e), + } +} diff --git a/testgen/src/lib.rs b/testgen/src/lib.rs index 861714dfd..8e6606a99 100644 --- a/testgen/src/lib.rs +++ b/testgen/src/lib.rs @@ -1,18 +1,28 @@ #[macro_use] pub mod helpers; +/// Helper types for generating Tendermint datastructures pub mod commit; pub mod consensus; pub mod generator; pub mod header; -pub mod tester; +pub mod time; pub mod validator; pub mod vote; pub use commit::Commit; pub use generator::Generator; pub use header::Header; -pub use tester::TestEnv; -pub use tester::Tester; +pub use time::Time; pub use validator::Validator; pub use vote::Vote; + +/// Helpers for organizing and running the tests +pub mod apalache; +pub mod command; +pub mod jsonatr; +pub mod tester; + +pub use command::Command; +pub use tester::TestEnv; +pub use tester::Tester; From d9167e1487614c44f738b40319d7ece1c4c612b6 Mon Sep 17 00:00:00 2001 From: Andrey Kuprianov Date: Wed, 2 Sep 2020 13:48:22 +0200 Subject: [PATCH 03/10] #414: add model-based test driver to LightClient tests --- light-client/src/tests.rs | 46 +++++ light-client/tests/light_client.rs | 53 +----- light-client/tests/model_based.rs | 176 ++++++++++++++++++ light-client/tests/supervisor.rs | 4 +- .../support/model_based/Blockchain_A_1.tla | 1 + .../tests/support/model_based/LightTests.tla | 40 ++++ .../support/model_based/Lightclient_A_1.tla | 1 + .../support/model_based/MC4_4_faulty.json | 11 ++ .../support/model_based/MC4_4_faulty.tla | 16 ++ .../tests/support/model_based/README.md | 66 +++++++ .../tests/support/model_based/_jsonatr-lib | 1 + 11 files changed, 366 insertions(+), 49 deletions(-) create mode 100644 light-client/tests/model_based.rs create mode 120000 light-client/tests/support/model_based/Blockchain_A_1.tla create mode 100644 light-client/tests/support/model_based/LightTests.tla create mode 120000 light-client/tests/support/model_based/Lightclient_A_1.tla create mode 100644 light-client/tests/support/model_based/MC4_4_faulty.json create mode 100644 light-client/tests/support/model_based/MC4_4_faulty.tla create mode 100644 light-client/tests/support/model_based/README.md create mode 120000 light-client/tests/support/model_based/_jsonatr-lib diff --git a/light-client/src/tests.rs b/light-client/src/tests.rs index dcc407bcb..6ad1a400e 100644 --- a/light-client/src/tests.rs +++ b/light-client/src/tests.rs @@ -8,9 +8,14 @@ use tendermint_rpc as rpc; use crate::components::clock::Clock; use crate::components::io::{AtHeight, Io, IoError}; +use crate::components::verifier::{ProdVerifier, Verdict, Verifier}; +use crate::errors::Error; use crate::evidence::EvidenceReporter; +use crate::light_client::{LightClient, Options}; +use crate::state::State; use contracts::contract_trait; use std::collections::HashMap; +use std::time::Duration; use tendermint::block::Height as HeightStr; use tendermint::evidence::{Duration as DurationStr, Evidence}; @@ -148,6 +153,47 @@ impl MockEvidenceReporter { } } +pub fn verify_single( + trusted_state: Trusted, + input: LightBlock, + trust_threshold: TrustThreshold, + trusting_period: Duration, + clock_drift: Duration, + now: Time, +) -> Result { + let verifier = ProdVerifier::default(); + + let trusted_state = LightBlock::new( + trusted_state.signed_header, + trusted_state.next_validators.clone(), + trusted_state.next_validators, + default_peer_id(), + ); + + let options = Options { + trust_threshold, + trusting_period, + clock_drift, + }; + + let result = verifier.verify(&input, &trusted_state, &options, now); + + match result { + Verdict::Success => Ok(input), + error => Err(error), + } +} + +pub fn verify_bisection( + untrusted_height: Height, + light_client: &mut LightClient, + state: &mut State, +) -> Result, Error> { + light_client + .verify_to_target(untrusted_height, state) + .map(|_| state.get_trace(untrusted_height)) +} + // ----------------------------------------------------------------------------- // Everything below is a temporary workaround for the lack of `provider` field // in the light blocks serialized in the JSON fixtures. diff --git a/light-client/tests/light_client.rs b/light-client/tests/light_client.rs index 8c6d1146c..d618d2350 100644 --- a/light-client/tests/light_client.rs +++ b/light-client/tests/light_client.rs @@ -5,14 +5,14 @@ use tendermint_light_client::{ components::{ io::{AtHeight, Io}, scheduler, - verifier::{ProdVerifier, Verdict, Verifier}, + verifier::ProdVerifier, }, errors::{Error, ErrorKind}, light_client::{LightClient, Options}, state::State, store::{memory::MemoryStore, LightStore}, tests::{Trusted, *}, - types::{Height, LightBlock, Status, Time, TrustThreshold}, + types::{LightBlock, Status, TrustThreshold}, }; use tendermint_testgen::Tester; @@ -21,47 +21,6 @@ use tendermint_testgen::Tester; // https://github.com/informalsystems/conformance-tests const TEST_FILES_PATH: &str = "./tests/support/"; -fn verify_single( - trusted_state: Trusted, - input: LightBlock, - trust_threshold: TrustThreshold, - trusting_period: Duration, - clock_drift: Duration, - now: Time, -) -> Result { - let verifier = ProdVerifier::default(); - - let trusted_state = LightBlock::new( - trusted_state.signed_header, - trusted_state.next_validators.clone(), - trusted_state.next_validators, - default_peer_id(), - ); - - let options = Options { - trust_threshold, - trusting_period, - clock_drift, - }; - - let result = verifier.verify(&input, &trusted_state, &options, now); - - match result { - Verdict::Success => Ok(input), - error => Err(error), - } -} - -fn verify_bisection( - untrusted_height: Height, - light_client: &mut LightClient, - state: &mut State, -) -> Result, Error> { - light_client - .verify_to_target(untrusted_height, state) - .map(|_| state.get_trace(untrusted_height)) -} - struct BisectionTestResult { untrusted_light_block: LightBlock, new_states: Result, Error>, @@ -229,17 +188,17 @@ fn bisection_lower_test(tc: TestBisection) { #[test] fn run_single_step_tests() { - let mut tester = Tester::new(TEST_FILES_PATH); + let mut tester = Tester::new("single_step", TEST_FILES_PATH); tester.add_test("single-step test", single_step_test); tester.run_foreach_in_dir("single_step"); - tester.print_results(); + tester.finalize(); } #[test] fn run_bisection_tests() { - let mut tester = Tester::new(TEST_FILES_PATH); + let mut tester = Tester::new("bisection", TEST_FILES_PATH); tester.add_test("bisection test", bisection_test); tester.add_test("bisection lower test", bisection_lower_test); tester.run_foreach_in_dir("bisection/single_peer"); - tester.print_results(); + tester.finalize(); } diff --git a/light-client/tests/model_based.rs b/light-client/tests/model_based.rs new file mode 100644 index 000000000..026e1a996 --- /dev/null +++ b/light-client/tests/model_based.rs @@ -0,0 +1,176 @@ +use serde::Deserialize; +use std::time::Duration; +use tendermint_light_client::components::verifier::Verdict; +use tendermint_light_client::{ + tests::{Trusted, *}, + types::{LightBlock, Time, TrustThreshold}, +}; +use tendermint_testgen::{apalache::*, jsonatr::*, Command, TestEnv, Tester}; + +#[derive(Deserialize, Clone, Debug, PartialEq)] +pub enum LiteTestKind { + SingleStep, + Bisection, +} + +/// An abstraction of the LightClient verification verdict +#[derive(Deserialize, Clone, Debug, PartialEq)] +pub enum LiteVerdict { + /// verified successfully + #[serde(rename = "SUCCESS")] + Success, + /// outside of trusting period + #[serde(rename = "FAILED_TRUSTING_PERIOD")] + FailedTrustingPeriod, + /// block verification based on the header and commit structure failed + #[serde(rename = "INVALID")] + Invalid, + /// passed block verification, but the validator set is too different to verify it + #[serde(rename = "NOT_ENOUGH_TRUST")] + NotEnoughTrust, +} + +/// A single-step test case is a test for `Verifier::verify()` function. +/// It contains an initial trusted block, plus a sequence of input blocks, +/// each with the expected verdict. +/// The trusted state is to be updated only if the verdict is "Success" +#[derive(Deserialize, Clone, Debug)] +pub struct SingleStepTestCase { + description: String, + initial: Initial, + input: Vec, +} + +/// A LiteBlock together with the time when it's being checked, and the expected verdict +#[derive(Deserialize, Clone, Debug)] +pub struct BlockVerdict { + block: AnonLightBlock, + now: Time, + verdict: LiteVerdict, +} + +fn single_step_test( + tc: SingleStepTestCase, + _env: &TestEnv, + _root_env: &TestEnv, + output_env: &TestEnv, +) { + let mut latest_trusted = Trusted::new( + tc.initial.signed_header.clone(), + tc.initial.next_validator_set.clone(), + ); + let clock_drift = Duration::from_secs(1); + let trusting_period: Duration = tc.initial.trusting_period.into(); + for (i, input) in tc.input.iter().enumerate() { + output_env.logln(&format!(" > step {}, expecting {:?}", i, input.verdict)); + let now = input.now; + match verify_single( + latest_trusted.clone(), + input.block.clone().into(), + TrustThreshold::default(), + trusting_period, + clock_drift, + now, + ) { + Ok(new_state) => { + assert_eq!(input.verdict, LiteVerdict::Success); + let expected_state: LightBlock = input.block.clone().into(); + assert_eq!(new_state, expected_state); + latest_trusted = Trusted::new(new_state.signed_header, new_state.next_validators); + } + Err(e) => { + output_env.logln(&format!(" > lite: {:?}", e)); + match e { + Verdict::Invalid(_) => assert_eq!(input.verdict, LiteVerdict::Invalid), + Verdict::NotEnoughTrust(_) => { + assert_eq!(input.verdict, LiteVerdict::NotEnoughTrust) + } + Verdict::Success => { + panic!("verify_single() returned error with Verdict::Success") + } + } + } + } + } +} + +fn model_based_test( + test: ApalacheTestCase, + env: &TestEnv, + root_env: &TestEnv, + output_env: &TestEnv, +) { + println!(" Running model-based single-step test case: {}", test.test); + let check_program = |program| { + if !Command::exists_program(program) { + output_env.logln(&format!(" > {} not found", program)); + return false; + } + true + }; + if !check_program("tendermint-testgen") + || !check_program("apalache-mc") + || !check_program("jsonatr") + { + output_env.logln(" failed to find necessary programs; consider adding them to your PATH. skipping the test"); + return; + } + env.copy_file_from_env(root_env, "Lightclient_A_1.tla"); + env.copy_file_from_env(root_env, "Blockchain_A_1.tla"); + env.copy_file_from_env(root_env, "LightTests.tla"); + env.copy_file_from_env(root_env, &test.model); + + println!(" > running Apalache..."); + match run_apalache_test(env.current_dir(), test) { + Ok(run) => match run { + ApalacheRun::Counterexample(_) => (), + run => panic!(run.message().to_string()), + }, + Err(e) => panic!("failed to run Apalache; reason: {}", e), + } + + let transform_spec = root_env + .full_canonical_path("_jsonatr-lib/apalache_to_lite_test.json") + .unwrap(); + let transform = JsonatrTransform { + input: "counterexample.json".to_string(), + include: vec![transform_spec], + output: "test.json".to_string(), + }; + assert!(run_jsonatr_transform(env.current_dir(), transform).is_ok()); + output_env.copy_file_from_env(env, "test.json"); + + let tc = env + .parse_file_as::("test.json") + .unwrap(); + println!(" > running auto-generated test..."); + single_step_test(tc, env, root_env, output_env); + output_env.copy_file_from_env(env, "counterexample.tla"); + output_env.copy_file_from_env(env, "counterexample.json"); +} + +fn model_based_test_batch(batch: ApalacheTestBatch) -> Vec<(String, String)> { + let mut res = Vec::new(); + for test in batch.tests { + let tc = ApalacheTestCase { + model: batch.model.clone(), + test: test.clone(), + length: batch.length, + timeout: batch.timeout, + }; + res.push((test.clone(), serde_json::to_string(&tc).unwrap())); + } + res +} + +const TEST_DIR: &str = "./tests/support/model_based"; + +#[test] +fn run_model_based_single_step_tests() { + let mut tester = Tester::new("single_step", TEST_DIR); + tester.add_test_with_env("static model-based single-step test", single_step_test); + tester.add_test_with_env("full model-based single-step test", model_based_test); + tester.add_test_batch(model_based_test_batch); + tester.run_foreach_in_dir(""); + tester.finalize(); +} diff --git a/light-client/tests/supervisor.rs b/light-client/tests/supervisor.rs index ce8098d2a..a5867ff3c 100644 --- a/light-client/tests/supervisor.rs +++ b/light-client/tests/supervisor.rs @@ -121,8 +121,8 @@ fn run_multipeer_test(tc: TestBisection) { #[test] fn run_multipeer_tests() { - let mut tester = Tester::new(TEST_FILES_PATH); + let mut tester = Tester::new("bisection_multi_peer", TEST_FILES_PATH); tester.add_test("multipeer test", run_multipeer_test); tester.run_foreach_in_dir("bisection/multi_peer"); - tester.print_results(); + tester.finalize(); } diff --git a/light-client/tests/support/model_based/Blockchain_A_1.tla b/light-client/tests/support/model_based/Blockchain_A_1.tla new file mode 120000 index 000000000..6b0a7e4b0 --- /dev/null +++ b/light-client/tests/support/model_based/Blockchain_A_1.tla @@ -0,0 +1 @@ +../../../../docs/spec/lightclient/verification/Blockchain_A_1.tla \ No newline at end of file diff --git a/light-client/tests/support/model_based/LightTests.tla b/light-client/tests/support/model_based/LightTests.tla new file mode 100644 index 000000000..c761a39ba --- /dev/null +++ b/light-client/tests/support/model_based/LightTests.tla @@ -0,0 +1,40 @@ +------------------------- MODULE LightTests --------------------------- + +EXTENDS Lightclient_A_1 + +TestFailure == + /\ state = "finishedFailure" + /\ Cardinality(DOMAIN fetchedLightBlocks) = TARGET_HEIGHT + +TestSuccess == + /\ state = "finishedSuccess" + /\ Cardinality(DOMAIN fetchedLightBlocks) = TARGET_HEIGHT + +\* This test never produces a counterexample; so the model should be corrected +TestFailedTrustingPeriod == + \E s \in DOMAIN history : + history[s].verdict = "FAILED_TRUSTING_PERIOD" + +Test2NotEnoughTrustSuccess == + /\ state = "finishedSuccess" + /\ \E s1, s2 \in DOMAIN history : + /\ s1 /= s2 + /\ history[s1].verdict = "NOT_ENOUGH_TRUST" + /\ history[s2].verdict = "NOT_ENOUGH_TRUST" + +Test2NotEnoughTrustFailure == + /\ state = "finishedFailure" + /\ \E s1, s2 \in DOMAIN history : + /\ s1 /= s2 + /\ history[s1].verdict = "NOT_ENOUGH_TRUST" + /\ history[s2].verdict = "NOT_ENOUGH_TRUST" + +Test3NotEnoughTrustSuccess == + /\ state = "finishedSuccess" + /\ \E s1, s2, s3 \in DOMAIN history : + /\ s1 /= s2 /\ s2 /= s3 /\ s1 /= s3 + /\ history[s1].verdict = "NOT_ENOUGH_TRUST" + /\ history[s2].verdict = "NOT_ENOUGH_TRUST" + /\ history[s3].verdict = "NOT_ENOUGH_TRUST" + +============================================================================ diff --git a/light-client/tests/support/model_based/Lightclient_A_1.tla b/light-client/tests/support/model_based/Lightclient_A_1.tla new file mode 120000 index 000000000..e2bdf7956 --- /dev/null +++ b/light-client/tests/support/model_based/Lightclient_A_1.tla @@ -0,0 +1 @@ +../../../../docs/spec/lightclient/verification/Lightclient_A_1.tla \ No newline at end of file diff --git a/light-client/tests/support/model_based/MC4_4_faulty.json b/light-client/tests/support/model_based/MC4_4_faulty.json new file mode 100644 index 000000000..1d43ae8e4 --- /dev/null +++ b/light-client/tests/support/model_based/MC4_4_faulty.json @@ -0,0 +1,11 @@ +{ + "description": "Tests for 4 validators, target height 4, with faulty primary", + "model": "MC4_4_faulty.tla", + "timeout": 60, + "tests": [ + "TestSuccess", + "TestFailure", + "Test2NotEnoughTrustSuccess", + "Test2NotEnoughTrustFailure" + ] +} diff --git a/light-client/tests/support/model_based/MC4_4_faulty.tla b/light-client/tests/support/model_based/MC4_4_faulty.tla new file mode 100644 index 000000000..a1542f5e9 --- /dev/null +++ b/light-client/tests/support/model_based/MC4_4_faulty.tla @@ -0,0 +1,16 @@ +------------------------- MODULE MC4_4_faulty --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 4 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +IS_PRIMARY_CORRECT == FALSE + +VARIABLES + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + history, nprobes, + now, blockchain, Faulty + +INSTANCE LightTests + +============================================================================ diff --git a/light-client/tests/support/model_based/README.md b/light-client/tests/support/model_based/README.md new file mode 100644 index 000000000..bf26cc512 --- /dev/null +++ b/light-client/tests/support/model_based/README.md @@ -0,0 +1,66 @@ +## Light Client model-based testing guide + +In this directory you will find the model-based tests for the light client. +They are "model-based" because they are based on the formal `TLA+` model of the Light Client: see [Lightclient_A_1.tla](../../../../docs/spec/lightclient/verification/Lightclient_A_1.tla). +The tests themselves are simple `TLA+` assertions, that describe the desired shape of the Light Client execution; +see [LightTests.tla](LightTests.tla) for some examples. +To be able to specify test assertions we have extended the Light Client model with `history` variable, +which records the whole execution history. +So, by way of referring to `history` you simply specify declaratively what execution history you want to see. + +After you have specified your `TLA+` test, list among tests of a _test batch_, such as [MC4_4_faulty.json](MC4_4_faulty.json). +Such test batches are then executed automatically when you run `cargo test`. + +When you run `cargo test` some machinery will run under the hood, namely: +* [Apalache model checker](https://github.com/informalsystems/apalache) + will execute your `TLA+` test, and will try to find an execution you've described. +* The model execution (or _counterexample_ in model checking terms) + will be translated into the format that is understood by the Light Client implementation. + For that translation two other components are necessary: + * [Jsonatr (JSON Arrifact Translator)](https://github.com/informalsystems/jsonatr) + performs the translation by executing this [transformation spec](_jsonatr-lib/apalache_to_lite_test.json); + * [Tendermint Testgen](https://github.com/informalsystems/tendermint-rs/tree/master/testgen) + takes care of translating abstract values from the model into the concrete implementation values. + +So, for the model-based test to run, the programs `apalache-mc`, `jsonatr`, and `tendermint-testgen` +should be present in your `PATH`. The easiest way to run Apalache is by [using a Docker image](https://github.com/informalsystems/apalache/blob/unstable/docs/manual.md#useDocker); +to run the latter two you need to locally clone the repositories, and then, +after building them, just add their `target/debug` directories into your `PATH`. +If any of the programs is not found, execution of a model-based test will be skipped. + +After you run your model-based tests with `cargo test`, the results will be printed to screen, +and also saved to disk in the [_single_step](_single_step) directory. +Results include: +* [Report](_single_step/_report) on which tests were run, and what is the outcome +* For each test, it's relevant files are also saved in a subdirectory of [_single_step](_single_step). + E.g. For the test `TestSuccess`, which is referenced in [MC4_4_faulty.json](MC4_4_faulty.json), + the results of it's execution will be saved into [_single_step/MC4_4_faulty.json/TestSuccess](_single_step/MC4_4_faulty.json/TestSuccess). + These results include, for a successful test: + * [log file](_single_step/MC4_4_faulty.json/TestSuccess/_log), where test logs are stored + * [counterexample.tla](_single_step/MC4_4_faulty.json/TestSuccess/counterexample.tla), + the counterexample produced by Apalache in `TLA+` format + * [counterexample.json](_single_step/MC4_4_faulty.json/TestSuccess/counterexample.json), + the counterexample produced by Apalache in `JSON` format + * [test.json](_single_step/MC4_4_faulty.json/TestSuccess/test.json), + the actual static Light Client test, generated by Jsonatr from the counterexample. + +One important feature of the model-based testing is that each time you run a model-based test, +a different static test could be produced. This happens due to the fact that the test you describe +is very abstract, and it's requirements can be fulfilled by a multitude of concrete tests. +To see what peculiarities a particular test has, please inspect the test report or logs. + +We suggest the following workflow for running model-based tests: + +1. Experiment with your model-based test, by trying different scenarios. +For that you might want to run your test in isolation, +as counterexample generation by Apalache may take a significant time. +In order to run only your test, just create a new test batch with your test, +and temporarily remove/rename other test batches (files or diretories starting with `_` are ignored). +2. After running your model-based test, inspect its report/logs. +3. If you find the test details interesting, simply copy the generated `test.json` file +into [single_step](single_step) directory, and rename it to reflect the model and model-based test you used to generate it. +For example, [single_step/MC4_4_faulty_TestSuccess.json](single_step/MC4_4_faulty_TestSuccess.json) +was auto-generated from the model [MC4_4_faulty.tla](MC4_4_faulty.tla) and the test `TestSuccess`. +4. Next time you run `cargo test` this static test will be picked up and executed automatically. + + \ No newline at end of file diff --git a/light-client/tests/support/model_based/_jsonatr-lib b/light-client/tests/support/model_based/_jsonatr-lib new file mode 120000 index 000000000..f2ef6f0a5 --- /dev/null +++ b/light-client/tests/support/model_based/_jsonatr-lib @@ -0,0 +1 @@ +../../../../testgen/jsonatr-lib \ No newline at end of file From e03c10f0f21f55e63ef733a2c82a36ffe9c246d5 Mon Sep 17 00:00:00 2001 From: Andrey Kuprianov Date: Wed, 2 Sep 2020 14:42:39 +0200 Subject: [PATCH 04/10] add talk abstract --- .../tests/support/model_based/Abstract.md | 50 ++++++++++++++++++ .../support/model_based/LightClientMBT.png | Bin 0 -> 94990 bytes 2 files changed, 50 insertions(+) create mode 100644 light-client/tests/support/model_based/Abstract.md create mode 100644 light-client/tests/support/model_based/LightClientMBT.png diff --git a/light-client/tests/support/model_based/Abstract.md b/light-client/tests/support/model_based/Abstract.md new file mode 100644 index 000000000..5a1da00ea --- /dev/null +++ b/light-client/tests/support/model_based/Abstract.md @@ -0,0 +1,50 @@ +# Model-based testing with TLA+ and Apalache + +In this talk we present our instantiation of model-based testing (MBT) using the TLA+ modeling language and the Apalache model checker. In our work we have created the infrastructure that facilitates model-based testing, and makes it appealing and beneficial for software developers to apply in their everyday development practice -- much more so than the standard integration testing with manually written tests that we've employed previously. + +Our model-based testing procedure finds its rightful place in the verification-driven development process (VDD) we apply at Informal Systems. More concretely, we use it as an alternative approach to integration testing of the implementation in the Rust programming language of the fault-tolerant distributed consensus protocol named Tendermint. In the VDD process, we start with the semi-formal English language description of the protocol, which is then formally specified in TLA+, and verified by our Apalache model checker. The TLA+ specification is used as a reference model for clarifying misunderstanding both at the English language level, and at the level of the concrete implementation in Rust. Model-based tests are expressed in pure TLA+, and respresent simple assertions on the computation history the user wants to examine. Consider the model-based test below: + +```tla+ +Test2NoSuccess == + /\ state = "finishedSuccess" + /\ \E s1, s2 \in DOMAIN history: + /\ s1 /= s2 + /\ history[s1].verdict /= "SUCCESS" + /\ history[s2].verdict /= "SUCCESS" + +``` + +This is the model-based test of the Tendermint LightClient sub-protocol, which is used to establish a trust in a blockchain block retrieved from an untrusted source. The test describes a computation history in which the protocol execution, despite passing through two distinct intermediate states with unsuccessful block verification, still finishes successfully. This model-based test is then used to automatically generate and execute the complete integration test for the Tendermint LightClient protocol: e.g., in a Tendermint network with 4 validators these 6 lines of TLA+ are translated to more than 500 lines of the JSON integration test with all necessary details: private and public keys, signatures, timestamps, etc. + +In our presentation we would like to convey three main messages on model-based testing, which we describe below. + +## Model-based testing with TLA+ is easy to understand, and can be sucessfully appllied in the industry to provide correctness guarantees for real-world software. + +In our initial experience of implementing and applying MBT, we find quite appealing its simplicity for the end user, being it a researcher or a developer. The model-based tests are quite abstract and concise; they can precisely describe what behavior needs to be tested. At the same time, in sharp contrast to standard integration tests, they leave a lot of details unspecified. An important feature of MBT is that these missing details will be instantiated in different ways with each run of the model-based test; moreover, this behavior can be easily employed to _exhaustively_ test all scenarios falling under the abstract test. In the above example, the intermediate results are only restricted to be unsuccessful, but concrete verification errors are left open. And the model checker will indeed instantiate for each run different combinations of failures: due to the blockchain block falling out of the trusting period, not enough trust in the validator set, signature validation errors, etc. + +One of the main reasons for the Tendermint modeling and model-based testing being successfully implemented and accepted within our teams is the rich syntax and sematics of the TLA+ language. TLA+ allowed us to concisely model the complex aspects of the Tendermint protocol, as well as to express correctness properties and tests about it. In particular, even for developers without a prior exposure to TLA+, following the models written by our researchers has helped to clarify the protocol abstractions before diving into the implementation, thus avoiding the painful experience and countless hours of correcting them when the implementation is already done. + + +## Substantial infrastructure is necessary for model-based testing, but the complexity is reasonable. + +Some infrastructure naturally needs to be implemented in order to apply MBT. The good news is that a lot of that infrastructure is reusable: some for different components of the same product, some for different products or even different companies. Within our first MBT project we have implemented the following infrastructure components, highlighed in the figure: + +* Apalache model checker extension for providing JSON input/output (reusable globally); +* JSON Artifact Translator (Jsonatr), which, with the help of a transformation specification, maps an abstract counterexample produced by the model checker, into the concrete integration test (the tool reusable globally, the transformation spec -- for a specific product); +* Test generator (Testgen), which plays the role of a _concretization function_, mapping abstract model states into concrete implementation states (reusable for multiple products sharing the same data structures); +* Model-based test driver, which orchestrates the above infrastructure components to run them within the standard continuous integration (CI) framework; for Rust this is done via the standard `cargo test` command (used only for a specific product/component, but quite minimalistic). + +Implementation of the above infrastructure took us about 3 person-months of work, which is quite a reasonable cost taking into account the reusability of most of the components. + +![Model-based testing of the Tendermint Light Client](LightClientMBT.png) + + +## MBT can serve as a "missing link" to synchronize formal specification and concrete implementation, and to connect academia and industry. + + +The original VDD process, while being highly successful as acknowledged both by our research and development teams, still lacks some necessary feedback loops. We have observed that after some time the English specification, the TLA+ model, and the concrete implementation start to diverge. Our initial experience with MBT suggests that it can successfully play the role of the missing link, providing feedback loops between the three levels of abstraction. In particular, in this talk we will demonstrate on concrete examples how MBT has helped us to eliminate the growing divergence between the abstraction levels with the help of simple model-based tests. + +Another aspect that can be observed on the figure, is that MBT brings a research engineer in the process, as _some_ research experience is necessary for implementing the models and tests concisely and efficiently. What we have observed quite frequently is that while academic researchers often excel in devising new verification approaches, they struggle to find real-world applications for their methods. The developers in the industry, on the other hand, desperately need _some_ level of formal reasoning to be applied to their products, in order to provide reasonable correctness guarantees within the time and budget bounds. Our experience demonstrates that the advantages of MBT can be made so convincing as to justify for commercial companies hiring researches as staff or contractors in order to apply MBT to their products, and, thus, to establish the long-needed dialog between academia and industry. + + + diff --git a/light-client/tests/support/model_based/LightClientMBT.png b/light-client/tests/support/model_based/LightClientMBT.png new file mode 100644 index 0000000000000000000000000000000000000000..a5233ccb8387bb48cb48525111a433226a3ff058 GIT binary patch literal 94990 zcmc$`cR1C5{6Bo8A|py7TZ(K+*@RG8W$%?u_TJ?nWK~E)cIL^-Jjh7MPWH;)m>|){jDjs{Pd;A zz>k~uq(sw1&S96&Q1d5FGIqP)BW8H@<3`iM@p3+jFY%{X*rkO#-P^v5Aq!r(R>8sa zv|xzzzmJH@s2CqyD-nqM?f<7wvuMHFr=Mw#-2a_ow25sE8$XLc@Vdl~DQq5Ifo~gF z(gMyPJ~8rjUBjJ&KxC3sQT_k&Ns-4Le@d5L%rj<2Ncy3xtE;{~T@#)=aAb z4;8c7{Le)G#8sPU-&T4LS2s6vb91Fc{$O)nkBHg7K6RUo#KFPA9ur;*?QxuQ&Q5jC z3D!+7@CgZ&cf8KPz+PLEsy0#0ounf`SabIBPsSaZBPy5=s* zJUboA=)XUgKuL6Nyw0NYL&b!5eoajhd0$V@C)M1d-5)g`8}<$k0e`~SJX7l9#g$n5 ziwtVsym@0qNY!FKvf0jw@;zLuNC>YxK3pVZ7WG)?;^O)!;djs}ILY<4jqYMAoSvX#C)E_;16rT?q}<%& zvwu&BF6z-+*51~#jX`vD#bh$NHH!XlhViu0r0M*@Olh~oVKarw4>Nw(-81)%e78FV zm2+JFG>1)3PfO3wdYvRW)J+T7pB(LLiJfV6a&vQQ3MHfZ`tIF3N4kV}?|%6hD?2$k z85oRb`A42&awK=Qww79JJ{J}~x3<1OOx$lJK+=SnX)#Bn}US3{bU!Qe< zb}^TpnwpxrdZucw-95eNmG=&H``MM1?`JCCzke?qaWxo;tR#z^`1(Al#WXBDy!vpx z#wRtapuleBccF65om;o8_W#bUqt+rmeE2Y4WmEnrWpTHTj+vd^`e<*9q^W1}^Tp7NFJJfs1Y8@D7tk)etxjoaX_(t< zhi)4)YaW&kE-o%6CeyWE+dLyT5Qspjpa9Psf4U_t%LRpXW1(R!k$cE_^o<_sNmh!8=9Pqp? z;%RKx5|;jCOZ+ z#_RkJ)l|ea3=GzstF+_&rd|-ZuMRymFhD!ae6REUh2VS8bD}5xP*qh`K_OzmCNd&| zn20F-_RikcOk*j=$-|?fV~&HJJ?!=CO!_a4X=9=>lKZo7*VorGGc!MbzEvHq&*LFP z2cv0iYrDO*^^_y7Q4L96Gd|JN1H+u5&cVXM($v&MNhB*HBje}ir=~{H>O@LP+S%DD zeaGspc04ybyHk}un8>9|m*C5_wKbYZxk621ZtLf`V{LKqNv?WvadDZItf!}E^mlv& zLjTgTutM{nmWVm${djIYtL)B>4i}MR*NiXSyaD?ieuukDuGPnf*o1@xly-4?ZthY= z{qb{na`(3F?}FUCyuVvp!!;hLVLJ=z@91dPZ6ECVb2~fV*;x4xNl9QZ z<|CoQR4aq1fX#0Nr^g!sC`0sznaYnJKc=T&Pw3czyB1bgd+%*dXJuu<{Jm*2t8rgT zcgQR&!}O%dFf%j5_ex4iMt(bS9didT@k^O=Y$=}UB_;fK@0Nf4x;s?-4BP-?z>$-b z6ke;-M*Zo@w;%%OmgMQaO6jne|B)v%zER=o>groI6&{1?vaes=`?Hl;wF^t7}!U>Yx9zJz(~G+ITpAJUrlO?O(9o#TFM>P1ZF^wZOsI4n zdFAR=266AQtgPTVn~e!HOi0!f+b`MK77Ja;av57S8+C`fqYh*YVtX3_r%4Q!n-Zo7 zL=4faVHn|s3spP6^`aRi4K*~}*2k*EeRhAQN>2J|QqwY-L_v_>55g z0HgpZfq{Wu+w*tt-J74A+dn)^h>N2ac1F%rf+yj*al>qNs2E%W88ech^wXz?X-6*I zGOOvv;M=!vJJcV$pIT&>mzCKKmt@t{9G)C*Fy6Bp0+%}9nKanjyESZ?3a)v1*(PN{ z@cBp?c*h?OEA;a@;8yhY#1WTI~YlHI{ z92&9`ph;FET9S~dDdVV_MHFjw(33%9 zaQLoc&Yqro=Kkyk;lp+k9_t^KbM(N$HU<;pu**Hy%0U0;OB3MLF1_$h1z{p)4NoO6{vH#av&++);WhgnHc5l`AN#3d_R zTeVzuXorfD654V4Wv7MA;yFa%iPU-=VTg&Un%cFH;rf68L&KD&>BZh*Jp%)!nn%!+ z=xDMgJ`)p@u&^+QR$=8Z6LVe?H*W?@h&sy7V!=dPrg&L2zq<78+qeDw z{YH&m=sUFcA)(jNR;!G(G%k!%8Tt0wS8R(-j*L9+_JLSJ@b9R{^eL1P#6|sasnUnr zV$gg0`;oMQMbR_G;{yW&y@DwpK8QdDVbT=lAi4zx;y<;6Cy2@Q8w6cDZM_R4hZxV!PwEtR5`=t;EjRnctZgq5l}N zTreQhXU~?70w9rtOqW5Hv`m-#nEnT!qPqGojYx`YonLd#k+8}K2L(Ae!cUg-KYyO` zszalb$xVy3ZES7v&z!ON`M%h5>rbv)j!pT<;-Zzw`?AeSLC9}lML^^FKfEkEPEJnV z+1cSqP=FMsd}O*Qv_|VbB*B%s?J3AX?kX+sl@K#L&Bx`&Hju9ge$01{!^diajkbaGReGY5l+4tAigq>%LpS2<_VbLv7;%X4cOE?lb zAVIOJH&;}I%mXahy#`%Y=DO6Eg^YppbwW#7BzYZMe~Lz-P+x)#?W#6Poo3{w+ZEHE z5MKCFP@wo@qH*TK2O3?h5GSWC_#&dJ%!qcT!{w)03JED< zUe1$sez4RqYt$s?O>WUMBh7Uf8B=j)aGevwT~=P++ZCRF{Lp$j9;PIUQPO|7#C-il zY8~qH=g;yCUbAVT3^sOlM{rj|$lg>Wk1?kw8>a{Fea^Yw_zVEZX#MrqTrrFZ}B(G;u)!_Mvyy3i@qmmdLS=i zsr20kcUJeTH41{4GEaiTNEtf>A?U%H!C?F3q|q@x7Fp{sS%>z)!btibd+R=0`K{*w z?q#<#Ma1nfPeT3Pp9n}c;5L{{M*lq%ZSA3qXo>a`E>g%%drTY}M|Eo43p*_!HPtOP zZ7H+vzvnQq>MF9tK@ax9$;0DbrQa=i>U$b4P0A?Y3-id;VLx1gOOE5>;uPY!67M~y zp|AH_NcNa;Y$D}FW8Oes7#8+OQPE7t9b7Y}k6S?CoymJr+I#O35{zz_SMv%|l9Myl zmg7oaXp8sp&R|ebkP{^#UnVj*xR^`fP(3&jBQFwb*5l9CgU1f#2qZ^p*^0fV#(!tq zxH?L>^3^$7!PP-D72T+H>C1d1){ULR8ak|_hrv=Yc*oe6M_;P@5NI|8g4#L8=jL3z zo_%b`oLF~GcJ}W3OYJ4A%LDoHuc@D^s|$Ez7NPvXPWW_BPM(ql?8%s!-Du*A7W@0q z%E}6gcCZ0g*D}XqS)a#RMfwn)+9AV-8o&=+tF^WD#n73pR>ln<^yj7ioSdwz-a$yH z#@z-D)N+&|LC(0gfipvC85u~Nj$r0FuY^OPC%HTHjDl5>kd*XzZzj5_u`xX(gH7>$ z&+xF&UD#y9-2&`9W8vSa`Ql`leuh#sRr zbwMzx6HIHQK0p$EM+gc9|0C(`ogH)P@Aegff`Uc^h4&>TB}KSCS65dTf{B$vN;lKN zTQ88P$dh0TSsCp;yIUL_%aF5k#5IMGW~jZg=F0JqR7sT>PcSkqOF45hp<}6DiA^Pi zi<1+Vw}uJtLMNR& zxcL(mS>K|!yF@);D#8Ej>FI%Ygk`wi-2A|MZEhlDf?L1NcmEx`ntk)6IDS+og=~unkees(5_8+jf@e=chf4G7!*dUbZYEXu$s`3OB??Gn` zp^8Q4<2(tJC2(d3WYX#!8mg*&_+(=D6A~03KNf*00%LkD$I|K~2-(}~Yj=<%+z@Fm zT)5yQM3*5KnVvzO>NS7u;L)x`Y^R0K!BUQJREFMFUPCBid^e}Qf!CXzovq`&dJggC zwrTUL@bGZ>3YSUDw!KA?rz{xo41Ru^vAFmqU)&fVF&J1MpTpmUdT#-2a(K>YloS)w zGd5;dteuyie}S2<6?(7qK_JY0xa}<)WdDNz^l)-;q?ft~Mw^Rto6l?)l&fvk*O8KsBvGK-jG48_E6!oPO$Sqjk?(gkE)v_(d`{1rL zp@CnlzvYj`pqzE2AU}s z&0wIa`e)*X_w}^nGM=E0x%8ZQue$vF{NmzXi&EJK4;<+#o{!$k>94ZtP47?-Wgv1) zK9A@j`+-I3pgIG~=t$r_-E1No=aj?`oUPL5Nt3u!*tF{J z5;?JxA-FSE(Id{g!{wIPWrz*J*pv9>wRViBE^kR6T=9Dp&APJ}dx}^1Uc<=92s$%7 zocQr0S3-xajSYmHHYYk~-lBd4;s9^vBc51So<_cis3@cZ{jeN+dFC|oHPHaR5~2|@ zopYhrvHrWNoZolmthC0~_<1*G)WqFaww^^di~%O0tNVCR5ejt(G-*w>D4Q)4urH!x zG$Q54v?G`caq=Ca;4|k85XKJymVnH0Zf>sZFJt#Mxc2w_=IsMKSJ=cWmGKda1Q_fY z&+FK%Xgov+ldb?KJNu(bsqPXkB02!WPnodb)B@R-pK_5S5T7PDy8$}I9S^TTw*CM6 zC(jCz8nsncgeP82|4nxaTzej{P}Sfev~s%E#rj;Q6%=a9gIvhaPag|2n?3r-|Crq< zT`hd@J|f!KqxyqL)#Ienrlk^5FOwS8E^=vC8^)}Uy}5qPwoGuRhAFA_a~n*}<19*4 zJmvVzv&j?-OQ#9V?2HN|G{0EScp{kB@3}c84834OzAG15Jaw~4Z8iy)dVU>u@h6$} zbG%P1J+dhUcKsf@B#-ZRg>7$q6gnNMWXd$67FktJ=p9*_sPV}<-Y?OV*U4vbdVgjK z#~9oo+4lL?k5+T{Khd;3o!_c+`E%s=Jp|9;av%YRt(#r$`l8R`+SZ7#?Lwd+ZaNxd zn6NM9eR5XC=&Q#Z! zUB#RW9)M5@86%cyY1n1Je>i~q314}hnKj&e;zo}@7D1WSY%{WHn7RPn$}rDC8XZb8&{7FZl?LO9g-fjjtPwn-%O=FO z3V6aJ15TP2ql0 zK~dZEEKEwlwO#4z;dFKp&Ol2o->FJ)|MUn`4lC~DJA3n@+Tt(gh|b}mw!2`X!)ol7 zjYsApab(}`!Jr4uGGkv3zEW)mQ}%v+c3?Q!jlPQ|l4@DxBQi#$=52ia2Zs3^jdpSm zlUHi(!~YuFyzV+&v!Bh=weEUJdUd?EFO(UHJZw8N%k_r`nngkn!>D7GofTcU+p(i5 z%RYCSyGyq_8L25+(Pm%2c%nNOfchI7`E9gUQGwAz$lza_-Z@`mMppW*h<@aWSo?z_ ziaGT-AuhQM_j`!%%*OdJom8s_0 zlEled(s7pX09ma$#f~%I9%)|Y*@ykXO7Rg`5`52+rbw#u+?dPKAF72S3VnK%3E*r; zaWIRVO5gIlm1#${L8jD8QzHg-x&u2sLW`Eb?IEbOAxiu^n9TpbK25Qolu`ry5U<+x z3P%hAH5h~|YH^1u*!=%~ip`qp1yg%R{*at#0f>C>ZcrmZj`*Yqz2N{(A7rkH0~{nt4y# z3()YEZ-4gKJw(cq>5dXIpZorD%pdB+qnMX@nahY0VdKwy(`^@QxZQN7!wmXVGIqzIZMaF#VlWC<%^`~*-%>yB-v2Fq;+802}DfL zMQf`{kR-aM&0fY&y2H=Eh@Y18Vcv`RLQTDrnK6^S5#t<;lUXu1ctBW>NAuJxY1B~fjQm5U$B*^>QGBxulE?-_O#SKXcqKfJu%P)b&f{=GG}htqVUznXW zgWkHe@am#b&KI7TyZbCZtO8$Nzt2S&$zm3VDX_V=177L$~eq!4hW<|$mw zH_L==oP#I#bNY{<+$R07CeKIf$j|VhjhI|duOE9yOw8<)o|l1^uZ@Q0%d#Ex#dcei zUTaE$rDGgZY$}Kld)H!`2!*V-cXf+t+s~f`1qDBU{HQES)1qaHP;K`)@;Fu&6yoRS zhY}7BFh>46cdmuBwYM+N@E0->LDN%G7yv3tNr7g61}n^Ig7>>P<`kn( zo9%za^~QE{Y8C)N@g0@HHP0BA^24cxpFb5<_Kc;Nes*RDB?3Y$7_~6@q<3OtP?>CdAlGkI zS!*Nb-Cw*qnQ(6{#Ne4hYrxzB$B0jFp1srksP!>E_^zKaU;{J5f}|!1K_Zb-qP&4;r$k6W>=5HKEm=}pT3S*<$jlJu$<97!*#6An zHVM7Bh-cPT&XjCb0=a4F@N2nez{7_d;OSH9=inhQ`19DtfSkXVrC~g7I__-jTTSN! zN2ANfB_YA^)}J7fFGx^SbkvxyXQ^gygiNAbHyMDvm>6UJM8JT!++ARNa5|09>Vg6; znrf>pj(4^UiXzE8P}SeL({Ebb+}hfI;$G=GoES=UV57q^my%mF1C!%sF=1dpln9)&YidJN9kQ_fu-79AQ&in zu>EO(4J#m0uAdVhy5H7p|3mi1jT>BswbZ@11g?m2c7i!P>Up+8hqs&H#^vO{Fjc1l z-0G_#`V=Co!jh7yCsm(jJU;a_bCS#$0oN8o-&dfv557N%VLi>`6~NVzbyZbWrWNPl zb~gyCJZ_~wOS)jO?M)r@?TL<#H6Jw?8uX0Y-KBO^mI8&nYQsQeg()AlTik(50`Wq} zM9T=DC0RHBov=5|O@Gz}U5}Jw`7VZ~y^Kn@?Cp2S4`=1Z%-D;}(u-M?e$Dn5_1`#Z zoq3jmiuZAHzG3Kq{FgWm;yZ6Vk=jOZKZ_{tOo?_s0uN#G(}l5jRAjxSE!Go#B^_4> zkO)-`kp_OdFT=}xHvg+fA5%H0xre^p!9hrHtwzIRdmAUiS@7VJYJqA~lz>}Hv zt?ZZz;v#V^gEI=#TW(@~%FK%KPJaFRHMr60WiER?jNHZ&1gM~I_Z=u+jbEpx_C`UwzIKThLKc z04yxce2vwwa6zDl%z7L@(y*;($yGXw^MR4{t6nQtqd=NxNm=d2e4huFA(|D_f?GsP zkXC7xkbB>h%jxfR>XH#V=(9HzF`_4aqL89nsQl>BxAZzV%P}&>C+k9*)|*Af#V1j9 zuJ=$qoe>+mPnh0$+)GsaZxU-Mol$3d?E-r^HDvA_RCmuC)VOn3dxc(s@#wWuWTjv| zfCu90t;dmH%q~fzkfh~{3iSiv#LJSXWD7%?(!R$Hk>a8{3OUBfUN+0SZ!)e`oP2P+I!T|8o}dpBq$EP>@-qSGAJ= z%$KXjkMuwu3iZg?*l=iKaJH8pJjQuW8gBtiAbk8PwVl8L5aDePj7+3?zu#+;HIef5O`N00`5?+kwD-5 zkYg)5R^0ioUy~q_X|J!|>G=5*GeM&zO_>kwZ>;%6NB_!>s}4(2C#$<2oZmpqg!L9Q z(RI+({V?<#FV<_PUCwpr3{k1nWN+Ti#NKnTzrb&yV=FCug;d_3CeNa1*A(m9Fsv7) zc`>nH3Sx)tuGVnFji#1nAs`&^vay98k-LRd-pUet9LBpHV58reA}%T}KCV|sExlw> zO;u%D>_&C1G3i+%7QM7ljUm{6_Y zX|KA4>;UyGP?h!3EQ;#Z3vzRJ>ir=lp%GDtzvu%k&5mzF=Tx7^WP8>ATd0sz34e@u}H-2AZ05*@(ub zrfYIP?LUKhsAAIpP+syNRyvKm_!|Co7M7rit6Q6Ien>BNc6VcE-CwdnfRCW!?ds^b zlc)%hesvxbR{vPsdY;>~qA|j4XcScoHFv{lz1QP^7XInORl>Nhg0Z9k02h$xkPerlTTLVx{-3v_!GYrT!InSCvrw%)8+yo z%}9tM1`P~gkcS{vz;P0i@B`38C1qv*nMgsT@{~;IMfB0%4$zOe3(+;^FMbCk^WNRN z7x2mp3RdC4lV#R#55GguAd}cL2GvX`8Dq8%V7+S%FYrN~5pa4q*=cd7)d`dtqZJMT zplMo)Zq&I56#U-~USeL1p-6I6k@alifc+(J6XUGx?7aV%S70Ej8a(veAhg5-z`vv2 z42Q@jbhJh@0&2pX339D(FVEEoq^}9gFW%PLkXe2I6U**x?TaY{*wkUl*UhM`r zD*&!y-8l3I_y$YBoeT{PA3uKVeR(8NkPCJe{wbH`?)Q;Qpa&qdGm_5?f z)dgr+My3g1*oB{o+dG3spb+6TsCEUKN?@+;jfPTL4abxVeQL-8M*q zMN?f6+hTgDhWivh4I9qE!9he!91Yq9psm~6+g}`WtdEqhEcRwh_*>>wfD=yYwBS!{ zw#Sv7p4WeF?C?YMlgsGMmqCe+P}JCuR|8_Te{fI)x`Lu2dw_R=B@^prV`E#GpPvXg zJ-&JKCUD1q-25{621gw5M$(Y~xZ^EEVf*=WQWf~woXa>#&i0GxIC1{Rm#hm0Au?{oFupL+npyhQ7EvP{(=Ly3H z&rRev57(DK)E67@By`NZ>HF*tbqMQ?8}I+`sMDpnp@!)=n+5j}QBH(3ykUt;+vrHzo8CYK*0K^QijKB`bL?{5#2}ESn zjD6*F2qVyVa7qIx)s~~__+}P;m`w4O>%>wP|g$1^^Z45xJNfSQ*i6hv_$?yB5WyKOL zT3L!r4O7Uq^n2T#9Y{hU7xpi)$N`sF$|dUccQz#CyojN}tGdX@NX`7aTwID7y4IRL7a$k)&E8+vfJL|bw9BWh-UQ%B#$&Ad_4<|2ioNm-9wE(aj zjQJUmHV{nUkxWce;66}AMedW^A++|dqM|^|*3sU60L+ADkv^cabaZsJz)wm)G&N1v z=ZTJtjB7K)F$Tf;F3kQ|Pp)faUtPStz0J+DD!J1f^qG8rsq zWh(djY7M2~Pkm=afK3sBIWp@zG-artJ{>w$pcjz%cYtWC+hcWTYd*=L$Pf*zGAw9d zSoc7VLkglgpAs$wR3?san(IhN74@(OcL$3*30NyYyaCg0Y;0UiA!+);b@+{d@#tW% z-hVMI^vszv$jreRT`^(dss=fUlRe@=y^u?IX< zyIBc7!A0PN$rvSSGc#{UNcaPh+t>vj#B~8EePAXI_V!-w?Gr+xo;;lz6EkIyksRxT zl2wwe8d3shslxW{B2O;3)V?LxKXM6pttG1~sQNk_4UYB#rLE5{$dN3`TAeiW-GEwi zbr_&(~ETjzLI2L%`PB-fi(*JVYq z#U3DLfIxtS=}n?*2%I1M{?o$6)^>%Mw{{bZ28e)&oeLyqyiqsq+)-;jqXm*5*XHu( zx`rURN)MOaRUJ@;Qm`q5LhULgWii+2#6*!g$1_vY0!_|VCr}D-b@Val1_T5|w5Y19 ztAnQ*9=0wW9y{gv_3Iae?<)N+K9XeGVQ>e|RfNnS>T<1loCVDl>mK~|Ysl^^sFT4O z{{D5&=^q{$S*|OkPHk^l+VPH*dz+BJ<}L$c)erR12Dbvu(I`PJ-0xWDgj}O)}eL_lwkU$7D~W2b61S<108)+ zAsz%rejp15u@S5aoPq=ABt0hA78bCecmrL6xP-*X8YDm~g%#@%QgA8_&@zM7xpwg} zo52*Zv$NOlweV)Eq%vH+x|?rw{5V&=x`IPQ1gEWFaAOaMv@*yCZ~wFlN_%TTUTKGV zi1K~IOQ8G|>+Ww<7weXnm$xm~O;iNd_gS&FP*i?VQB*_(R6YVIBJiE^kuUTMxmCFx0Vq;h zc|kVvD7a@un3&y*ST{YAw-o^FA_lwxEQL|~8l~Fkh4%jngT#b{3LyPa zdei4iH4f9z=yAJyH4aa6)hkz^FaTnNmno~uko>8foSe7!fpL6w7E6Ay`o;jwJv(iP z{7Oos%nx$aqkzR9t8^+0(#lfpOqHy!tlR@qo|J?H_-Ru|N4~Z9pvW|P`m`4^yI?&@ z&>BjDvINBVyg+Wg%Y&OybJvPF{dpk$1M&u-d4XA-?@CtakfM+V&F5E#$q7g>C@Ez- z(uhT2AAnW)2t-=;D@1^7fxa*rtzyPU?d;+LMfo7NgPPjYsJO_37d+UTo7Hh2@eoth zrrs#E_M?pOdP(JXzwbL-jkpPM2I|tL2h$@ht*vCb8@8ZuhsxbXX9qu7MuD+karD_4 zZth#M{@Uw5{CuLh8`F?$jnU%D4`ys3@daIH0=J$V)uEfD?nd&`HSv4c%hCm!wjh!; zL=6J002v-mEaVugv+aMwPWX#0Co|PBKh!NjlVWYRL@MRKT}IW+^~(P*0qQN{y4#4L zDdRCR8RqtNJ4};zUt3dsT8iDB2z5T)Qe{goT{-OIP`QXklK)S^{#MZa_}ncGQ$d)h z`yyfoZ_Xk4yQo=-@LzUauAc}_e%jIQ!yeZjM#1(t_q~^mO&%CFfB}Lya-bQi*xp6E zEYLoxtcC=-nwgnVM}B9Zm_DzmtQ^&1`mM~+0d{h*Dt(xpnPG94Ij;(J0U&5NsHNda z$k<91*Hr~LQ{eY1TG`NNt^7Y7CU^=5XLOBk@PPLgdPgWszfC!qHWU&z@30ey{pw?nyW6McPle)$1v)Ge{6E4}^)6&q0 zd-qN#SvlU^S|=HzJ}d+{S zQ2x~n+sz9pBcq>v>EW3Kxd)zP$rs1oK*noRG`*8qgKkJkXr3q6tRb1Ks1IPQfX2DK zOH9Oxl{BCjotsli5v%(01ytUkgZa1T0n{U)5WtlX<4_`i+=m4z26A)I{h7JB?ck*M zP}bnW2NjP#PNdq(7%(<45EmP}_47`*7-aHriO=aVHdssizv7KeT=stpHy9jHR~>_j zu#H^wz9;0?4?Dg*Iy4W?WkE#;dI4N2W{X09-}ZHK zD(LEL)^soV)jLK5K?P_$j6rhcE2k^%x8 zC^TVybNYoL_!2Ps0*?LIA^aKHwQJV^Z-SHqe?ZW-SbLH1oa^q(RuF^$iU&n==R6X5 z762^hWe`EtAVu$7gsVt0vST_vE)L2xKiK&NpglcvW?I@e)8d}q7TD~9!D18I%s`~h z)d6RfS5&O*9DoagfOGlsoA>XBo+ZbDVouKieV2*pKI_|Yh(@ISCE#HlOg2S|sxu3BrA!4@CbJyMn*KLbU;XV`lM1@dKS ztFt#Hf5pvt)m2xI%sF3h61aEoYhB$0e3VyERD>xL8h>$ORH!-l`?s?_t{kM~)Py8P zLrbg1Apmx}K)hJ|kOcy00TQxvt^!i-?z`oT;qj%?q?VgRxw*Mz-znQgVJJ!H7dLhu z$fTtYR65N-$(Z83oV&T{SRHIaP2=(WUeY0Eq@ke!-1qaLFH)cHxu#5I)N>N5S4u)(*w|tBX0Tcqd1fI&|c6l*TGf@hBslp25MIv@cG06A$mxijoufs`IL6XXYZnQoVTkL$GP z=o>WE(QeRLKDUkuqyAci3p>^Iy3Fx<{xPcoioBc3NLv zCL$rhZS4Z@We#aN$@zVD?I0P~(P4L&DH2Vixx%rp9 zJm#C?;^LyBHIpm%u0?)_`UGWAqd8)0|3Y1-@ON#k8073A+ZVDNtMw{vlC|hOjQuj# zP*jN2HzC$9#IO0vq0MgevPu{Cp*9>&Q;_>I`M8~sRHjnTwJ$1 zVhh8t2vWgRuumwqxD2X)b$3Ub>wItvCTPqbQvs#?h*m z`1ttj{v{$JqJu465kYE}kKgi{afmy~xz7u$IzUg{Flws`FykMVArpTn7M zPjX&H^6KAmZLYoQmjXSDNr1B@CDnLtnU?EvyGMYT8waMf{tP0CecW{{M{tL@-^t_? z#(~)g{M@^qMcdNhFGUct18*>6y~!h5q(koCwA>VMy^x+yzx=w(Foqh`o(bEsIM_Uf z0Rq@dCOp$LndHMd$+gu^AR6tt&yeF8j6KZgot>LAn5q5^Pn>!RwhM#>?2t39I1`ed zU%335zl%x3rd;IiT@BP=Qs+D%C$2}(H;_=Ea=w69ia1Aa#T1^Ox2(vPK2t+9 zsq|qZEE!;+#m{N-opI_t8Rd);{q&7mqt#@w$EKW2^5}~pN-$B8(RcHkY(FpQci`9n zpV`zKBI8!F)TJrliL%W@*-AW{6Ji_xSJ84uT8fN3@3NOyn7M{k9PM+>F0X29snPw= zwON~AGwPK6UDdy~vdekIDJ>#ff1>5Cptdb%d%jBQ>gpns*kqq4oFC>Gd5hGu&yH*zs zST#)~>sxkaW+~KQ#K5mQp~1c}tHPZfPB!F6$KBE8?bWZpOE0#b z3r1~J#b-}nibcjAFKBcsecdj!r0u@td#t|9)L-Xt9LJ$y?D$;Ps|DMdGtNI~lq-T+ z69fRu(^Ff^GPFF;x$mc*4W~+ZvcvP|HfH7}#L3AwC)bGk9~^RO+@+kW?iFl~q-pw6 zd5#Q$7^HVb$$#2GKKXgASvF@6B)+?bm3Q(gPZWclI~@+-EDpU@8ciSz48h zwG%h#be+^^@d#TT{q;rA)uUz zzR!lej(u4PZU@J4mzMHsl!m+SroXvEV!pnlMc9D$*zUm`HhnVJWUc8LxOSQ08{cbG zYQRI!2RY-)CmwZcb2TR2_wJqz4M{%mU_ZXCNb6RV6}GVdYH_Hqi6GsTMg4_TFN<7< z*{Mt7ZSSK@2Z_UXY_%MGLPBPh{MTbldWJza6ohv=;dwTqr#_59|27x(}yT z&0!m}uvd!ZHO)O0dV$v_KNg!aZ&R?AS0wWa`x>7{iFFN+&jbtdD8_YA4&-zmy4w|T zNP6wN#eqjSPjukZBCoaHlE*i70Z5t_QxNt*p>8EGzpy}NAAt~~A#DJ*&hN7e*}7kS z(D2uWsTh~e$lmHp{K8G!nf(*~*?R>|q1aiTkHo{y-nmQqZI66G?Rg|rRXocmdR(X7XF-x#V=eF3>yk8lY z*|9;Rr!&VG?M(iA|sDlzgYQ}df#-}Az2rq?& zhbKzkbV~fZFup#n?qfzqx&O8j5SRlNN+B|Ufv$HeW7gSAW4|q^regormE}(+6qaMu zm#=~WLckm^bybNs_q#$Q{eJoqjYzF9hy4Qsjh41I&-zv8`>$)iv&WEjS{5knxWVr# zkL#+If3~0UCk`+>J&q=rah=J^S`V9Q@u6Km>4NE&S`fl;ohoQX``HO?d5L=$@yy8b{ zkNO7cz{3RE1|Jsu0XMj~dagUIf5|)HYkJ(r+r;!!>5vGg@G zE-Z4?iQh9-hp(YL!ukC_bRwNL9_CJ4O$NdQ}>*19t>(_D_o76Y| zNnsoEnX%!k>A@~|4}SSv=6#IYK8y&|l3Aw&;j`x_hO9!q|6cD=OXH0C!T0>KSd4NG z#XQ#ZKUuV==&a%Gs)UPYHtC>ldp{Y`_D@PUwFWbcgjTenGw(b`;R@@(3J|ykMr2e` zz5VwFl7>-u@C9+}sl-JORqD{_|FnaKAVg5SHBXWf=Fbhn`zOC}?^;3Jfc`3i?6TPE zk)@&(PD+8eaDSbWVp%w-)wvs8i7N;Yh=12Y4#4v8+nwGq(8Fc*Fa7t96I>_HG|2Xh zaTfd`M&M^Hq&PaZ(4JHCf7a)=uj>o3Rn5a=l@E4#aY-FybD31B+R&BlDQ3kwmyxe(HX%z&Y< z_jfJLKzd0b?J6=pQf_;jpK(eTR2RT%LtGG`AzK~!z-LnOKR4v-^7>+sC%_}p-$0=+ z@%uXF49P1HA;F79v?1A1Al9Q<{-*;8#DJFNE7)L!eLWP!=PQ^IR8EOEBY1WO&IO+I zuI%6hR`~<}0GRs+F+Q?AHMUwg{b_8ZVp6)gBeJ0ki>@MLAMmIhaSA-uuyNc7FTs3E zZM=#|5!j@oI=+`)gp=$3v!+WJ>c@HgOFVZfuNcReo0(ypSP&$H1$F@MIHF+&KgkEs zoEHwtS=tJ2*19rv04kKMb4BhBy3rVL>W;}w*zhKC*-!9vrRdyR>QFLAgWfY*QZH;i z_=}D{H?085^}Y=l3-c@yCi4Y>Gg|P>Tu^+0V$z*4<@6M0e8LG1-RbwvQ420okRmuQ#(!(jjs%^hza2d`erNu7z%L; zJM2s5ho)}_CA2xC5IJnPMy z=bGfdy@jr;YiPh|1v1M+^*T7XF;V6ZiGwtYfT>`Pq}5nq?k!aAEvkFqx;}&h;PAo! zSYx?o^9Oh)UcW)eXWMSP@d4y;NU73BB)KRruYE-~YB=S1#x0=dtkF|M?0=#&fFz;B z2$8d5?W}Ey5RnyKUAvppIo~HO{R)&g4{-+*5*P^+#-vWU)5(bmWkw2s1UZ?T^>x8c zNuK1T!~P<~dC*2RZ-TI{|9`gODAfa*Ho8*Og?{(V_(yj)RSo3?fl;qi5bD;$kbfx{ zG6s3!ZL8wP>+UW*q2I?x!v9|MsnIP2f2>;=&pMG0`nI1IP=?hx(FEeFFGDJWS{5R3 zf3ET6#@)L+HndZewOb;jATz(bv~d%u_`yrzpuZj-a~a#07usU~lB!9|m3)emNEMj6 z|IPgJ3U5U-+#bR2cL+s~>pK@@r|TDL%FA0HQhA&M^F$3&NMpRw@ZuB{DhF>!-+Y6Jl#2q%1W79T~vJdkdG#EzOQj4+?gy9 zGiu`CVEq{;2!2x02!G+^vo41a2@)-9wl8gFdAYX)6X=qJPw(;4?7_Q|7^GEkUhls5 zFB><2G>7f((L_R5DLsZ~B;o~>|ZMGP{9uLvb1YQbO z9Z2VfZOX60i&5yup798~Cu<&GLq4iKo;kVTIb)*&K5OrvTdRe_(4g4#9JhxZf8u%f z;n9he%U)9-?l-apKB|YcC;Ly#JrVx<9nrt{cVxw-7TreFsQk&2`LJXv4O&|YZ*QNb zOd|whk@%l%+TlM18_-c8qqFXPW-_ct6L_p)BmEG!EYvSapHa7|?)6i5423P^&biE; zupRs#z_nsfQ8nqUa&QxQ>x}sAEPOq0i#nlMee~RR41MS`T^TzoDj|p>g zZ`ChKoq5MWcrDZHh4iISbK z%!XY5q#s7b;92BZP_6Wfaiu!6Xs|lrk=U-Pla|3as)*H~8=$0KO4&AbDRTCANt#S* zL}=a*DZ&>10lvnspR;Evi99;+mhjvow6>UkyZNY-bEEqOF81L4Yw-2gx56z-b;!>i zXhpR29o~M7&|G(_8OPLvfTsPq^s9fcJ8ZjF&lgZhJHwLvCi&%_pcBe$j$_JXCtzT+>FZ~E8Q8;3cq3wI3RJuoWvJ*7|JP3E_qpg`S9{Z(X;p2XXjeiy4JNld>3Y*7uMiK z_i6um3@Pno78&jw=j~h^jDh;b@W_VRUq>;?MX}4_w-i&gCxqVfZqP?EAx*x%9g5vq zx!cgkB16aVi&^H(PKeUqfqIuNsCTP<0+S2^;%^e2au0;# zqx6yQktP&K6LP8j^Dfl4tNFWR^%X4-lYcz=!zYBnWqv=P#k3?S_1}Vb(hA@U1f*cH zsD(X+MtnmLF$CwsQ}ecc;tEobF)zSt)BIi&iL$;vo5X`&&M%@AHV1Qv z-pu;Vx-I(gt%lvTsalVRih9`AgoM-Wx(jQEjE+)?Fm&z5b{FB{ll}hP_5hY0QHk!i z-1%L^FCJ#a#3XKJ^}9nzP4)^?yodU>S8-enrGvXW5Jy&>{!qd23u`FMzydb+`Eq`B4h`rteC3b4z> zHX8q#;*^bEU;WPM6BYHCGg3?&tN(Qp6LIO(TE^EQQGe8Y$E-(0h?)0zi!6D7B~$ny zx$jE*&?jE(`rppM<=pnQOH0H~Qk~s12k6T{z^%_50xUs~>#V+qc`(HCbf5;>0QqrO zZ3|n1uwYck_$rlvwszsbRknVz5yJe$={dE~(~dzOJ@5RSlFL1Hv6HTbtMhX+YH8ho z>8lkU(Siz3mtX9sK1aXB^sYAJbN6bwdr!rVSL&xq4wjRruK$GCiXQDmRCra1pX};3 z^kuHAAXr)C2HTXxsQB#ny?n0D8KGC_skD=o+llIRdVMR`UR^t=M3<$f8wUl`2kn_; zl$>X_1J{~K9wyU9j9vCS)-K<-PxGWg?i69b0;OhXT<)6{#Xvw@KW}scEL8ukV6YD~ zf%W-Zw7_h;s;kSzR%~6c)N(^z4q6ZU{!QCUVzOZ&e&D-tyF#~_hI41G8+$v_3VwEZ z#Td}}SSF6!lBUby07)JlJQnG@6m+IMHKl8NweYJa*{9oKl26}r8+AVH;SIUWe%i`- zw~NRrP1Jp8Z+wQ9Hu1Y|eNAamxmH@(K-+K8qxc${nvHT@ecOw-W?mEb&?R>>BUa6e0IsTp=v6_bTUrny3gxeRFv|(&Mg|_W{*KVg(Y^GtBS-+x8 zG`Eg#h0=jD3YYw*9VkNxw?)n0sP%iwDNG zZ8$U>rYk&T*CL7?4~&eAH?p6KOz9>_F(P+jm_Dp`SFv{~CW+Sks#jy5DR>lJJAC?U zQS4ciX4-JIw)Ws)31?kOVR})0RSKu^rmLdwy+?>Q$0x$p^76Xxmfrd05Idzg+fF3J z_^7?Lh@06-=5lJ29K9&)@wzBMO?$2^tx#Fg)SMS(uA=z$3ZxhI3>Nf1_AA4ni9MDT z6CnLwYeNpi%|Mh8ob6c-PN2V=#OwI@HIN5zCn6Y9-(fgEFP=29;`5LlV0GJQiakB8 z9tNyNcs}vFQ?ses5YOW^?c8*u%sW1n_PN~CzCN2B_8Gi1#-WeVyG}ci zn37Wxt~F_?j+nNaEVGc*JyK@qV(%)VlE%5$0C`U3kt)3w6-5xEJGAXAcIJ2xP|$Gk z4{GDJ-;`Xz%ja`7Q?Y$H*EyQxk!ocoQ!_C&{+Hi2=+jc=-)9t*VaLN}SNrQcKFY}V zw?EPmNft?i$j7em4qPz6Q8MQx2rbYf46=AYni}a}58pI{UjswKGVdKu6)LvJtJk77 ze13l@Wp97T{>;MI2$x>0dP6*U^t|lg>rvTtZ=&!~zVt}9kc&W{8QykozH5aad6yrd&g>yq*7!Ey{Ro+A_HLLrTbfLb!4urR?g9@A7lR?!N$G z9OQokZ8EJb|Ijy)Cj!7|b|PN^CM`q{a0K=AXy_$c_qs0|-vC-jApeaOHwXLPFUPXC zFI?apa`sZ)3D8j0YUt4}4oG+f1xY28*`Gdrd(3vPuU~HM=qx+?Y1xf?`$l6F?5{7q z=Bk2+f4v8jFDAzL0~@H9Bnxe9X368$0hIazgna*u$8c}ZVX_BPdOTZ z^;;ItLkACr`U~F1c=@xDA5B+rVkLG5Sw+9M8q!BMhHXGyjW1KCL0f*@GFdat8K$&P ziAhM9&v6DX!}zZ@gUSKiy3ceHzn`jkrK)&7`wJ9A8E&D0gvLT5tWS!oWfNNuDBU|c zp40<#%K}Xym_58P%l!XChK2ip%FyeXyEru`w?IQcHYsq$?{^~fzIH4+RJkUp*GRtd zdje7wAWv?J!8q+6veiuGJ3D^%Roru`nfkBJ=Ys8=ph{^#WQRL=(H;1`8foq&etQ?&Hu+i*Yhm^;)y<*6Bs$h5mo_ zgb}#|+Gof6w>1Lv((MAqGN6-j9AjtDqf7NkjxPeypVLT+{5!ovHHfw5fO=KNS#LN!u?!x1O_Mvmh)uxR-xQp}sDkq3T z%IaX$j8b3!Lf?m)9tbFWdRhNP@0LLjS65X4zSrlQ#%)SEZtH?|*8cQ<*FH+L zzTsf71e`=ql2P9T=GNWZ5~;UDw!d9mZRe{nw}?!X>j-#wnn|D6Q)?G!^QV`TEXc=? z_jTMZO6YaoIpibylxBU8;jnVG;d-ZlFfO0M;L%G-&^V8B zYqy2d7X>2cCpmo=V|#y%!C(0=9dnx>6K+0A7{cC}CQHv7KW<$a{Mhgt6UPyleO9~& z!nCb&d?*=;mE4;td`8?;HG0}4G%PKlc{Xi^I>@g)ZqBiteXa!yWS0|79^E+r>4%spDW;Vb-^bp>hPrHiy zHqv`Uw;mhB`lZU1P-PBSywI{X*6oS!6MIbj{VLkz`!sbdgh7VI9V!ydBvWvG8Kj%>d0n2j@32j%3ixNpPi>+@6{c>?t zR#4|Taf!^Ntp>K+TKAomVk;kg?OY#JSitq(nKc{f@##=wh%C!SKr#D^kzwz>2B7Hq zJR+I@bP|scT z*$2b*%LC)to!hT`(7Z)*0ub0TBu;l#9sV%<1rMvHC+)wucMukuC&c81lbsq=&=rYF>{=Na=e zQ{KKB<@(5AaJ5Ql6W4h}2fsyq=C{vwdE0b;LLx8#|ip5k-(ytQg0;G5?Owky1f-c%Z;fNda}?ygatz zUR`5*(E-&&dMu}S`0VX|mE)}cyil3Rf!aD*4>{aSpkbM*avECh6ZQ7Cw%2lJrtjAG zL3I)AG`w@|v&E$c8y=zPDa^|AVv(YRR_n6m{CXetXuEO(Y*Mm`c}m6Xc|NF~gM5wF z52fmpp66a-I%AU>$!P1idp5~?RuW}30o$?4%Bw%R3P9>QJZ}Gx(WAX#p&mjBpnb*a>&p>tKVSG<2(y&?+vcE9$xEN0ttRq5Q>({VUL4cf42VJ*Lz;D}5Q zRTQ)Ay-=EVvj#TdioTauN6e!^?qZwM)&e5kWITPrf#Pfo|ZYE3@P!Q5w|R!R_5Cw>Yo) zEU(!ehGQE23hRO714s8Kb$a@`x_LJ?%Nfsnn*bZRzcThiw%gIaBraWoRAatTopk6W zf0HMd(p+xeK^@f*5w<{Jt7k7kB7JXaI+?!5&>QacGnW|yf$f-4eTS{FuijifMqt99 z7hDWYP%n!ADG);~?$|Umf&NZ%l*OpwuiY&7U{vfwPCHwbN`eQDO$nh6Z=o9d&G+(pORE6i9*TzpmLF+WQ&u zX)5p6Zi7F8c$t8jz3aRt54r!T!_>IUkm>RCW7a2+Unq-N3|osSP(?F!Ik>22sy!O= z*~&>42=i{RZMnO1F?n_pY-yXy^1-DdU+as0xkr2Mose^#DOu#w*H1bb&|58B_+7Hz z4NP*fw|49Yz*6R{+9n+mX;{+8-*Uwx{<2Fik5wm!dSWRI5_`%jE>&HMZ(BasLM{kS zO!USH`GDQNLd?MHB-4+!;i#ZwIVmrpb7O79yo}Aqbz_Nd%GrEoJ6WfyHlx_+;^!05 zWc8L0XSG=x<=4AcA_d+>mhx)lGb=lrtBs3#I6kF=ayS&q=Qn#uDcGsG**(m!x2fZU z<#=%qBNkCSKys1&)t{&kHShgi%ZD>GS;C&XKDL72bp14tjEfQjGHzU%1Mt!+A)#^H zNa$G;;q}4bjAg_-HJY>IssLKyQlAR;F81~Z%@F?-zTO(6=<}1k>-zoFb5}VPudPcy z-TDug!3@os|Cb9O?cI=UsOb)KKPHxb0CI-9oRO}I$_-Os`G@mXaH~c`qOxeqPExzB zP^OW68(Rlo%10K2czu+MW$3sCN^Mc$3a#*&(Wx2FvMVv${(+yJk`(?aa{>a^@~stj z$EWhZvqf871ngZjPSnjK+;fZ)x@U`H4I5wZ!q}K(+^?g_rrNbBH!QXr*7lEf>eg&N z)Xyc9@cPu}gB{!0`UO3chbK)JcY@l2&4**S)8$5i&smFZ#XH&uLgSM?VMjnmea*NX z(9GH#EyLeYAx*w7)Yq_fIUo!VJ37F=oR;rP@M4&@{))ScyR7}Gh_3F_+DeSuYO1PC zIG?9%q*v1mlYrNVXfW@sJ1tq>K64)uf{L6UhbRq+i5Bo#dQNM2-)bow&8xRuPdJ5M zjT!muN2bTEJbD>f1N7L!Np&mI)iaw=ywcnk;U_x4U~S1_#}Hasgh8>$nl-;^4f z$AikrQtKA}{$rmY`sDlc>%S3aEnT+io*uL1A*2`E#~Ulqnpt3E%<*&jj7%1}5w9sq zcKYJdtH{Lp5ZjTt$JK`R9x$=3TK?C^W?X&JM3LkCtp3lW*3j_y_k*miSs^< z-%z`r2R`m`lFghsIWPVC;Gy&b|oWDc!8YZG~_FNXT#D^|JH3)aVF*CWo;ri&n`h>gc=(2B9q0uKGm_7iKD ziq7KN)r$~fMZHpkAbJ5O`1H56ii`OsGi$<0m!YL1`#l%2v(et;a-YjBrBx?L`D(r- zU_5}F@f&J2d6p=4F*j8GPsMWfV4OIJRdY-Y&P-pupADdztjMV;G2RcYVsE!OTYPmM zCw;v)7h}JNn_{{6p`-Zkil`KRSCYlF@eCeGV(tv~lx~h1Q+si2A1{vYYO2{&{F=kv zS7d%)h$Npup?wBiKO*h`Idkx%S?69hPC)U5Vb75g*ALQPFQxUL~6_PKS2s6biYY7M~O>QMR$e>5(wu}Ne_#(R)aLeDOF!gaOzWW2Ap2sOwOePm|!(z4C7@}~8x^IUNGc+6_i zmA$&Z$-d|25sstK*ZcjsHL3VEwPACi+-(WsfR;}m&>`>#7K_Vzus@-vA*S8>Kb_g? zc><3o?b@g4E$}5$?KZ%Bee>t6xX6Ll$vB#L{*lK&iVir!AO2bKCanNZa2%Zj50nPb zKJID+YcOzeK&ChW@CrZT-1z+cwCrZ!{~-UxxD{ncB*h_b*1*36n%_VMnG$BlssGUK z65`6XdOiM%InDWbpdGr@(qdn1E~sj8u#pua|Z;SdH~K z2|2MfvTxPm%FK%*M2L`n9y_ z@?x)mndWlko@1XT?@EG6%aAZR9bEY{=e@{R5G+8Eab{z91@tA=)Q~qVUsd|Hs8=&( z!y8X+Ny9dEu>>Z!#MUy_-5w&^hD(dJWhf3kT!=t$jJ@!lI7`X{7|1Zj66fFT0WTz_ zUVP?I-0QsO#Amj&sOLGw(Q<`9E3}%5rAxvPF!%v{8J!?kF*~YuW9i=MNFY_XdC3^a z=`dB?E=YE#PnDB-5&aOnCD^#f7=VCHxrK#xvqRmhEagCI9To_J0dx=;x1$5JetTI? zZHoI_QHD#NRwPxIU}CR$vLWIXS$e-DeK+oB5c5t{WLZYt{|%DIBBP`IMlJqHY_B}W zz<4P64hT2~rkeA{-x05L9p-58UcXZo@7M-9Zqt%R8+FX)`-kWfA_=4g1*q;jaO>jR zlybmY`%^-WadkM8h_Rao)og-6B-eA22VfN#k$n$7lRLori8#wUanHp zRZQgF=;|p#1s$REfEcAE^mOW?^=L)DtibL0WU8csiJwyrHSbIR-erdOa|gVwCO3>u%58yJrqwr~O{zh|l+5exV@ zATt2c2$mea%V*5l;(B={D4GGcvqmlNCAM#qMH#le|Kbn8Qqj_Q^-kg8YHFq*=e-s}pt=Yakj&wVUbb|p zMiQ}D!a!=@i%%d6K2MEps_8LR|ESse&)VH&d&=m3NhLg85<2{WQ(*BcZux^oAF_-e zKcmD^CJ6}+zTp;Kxc2HE${z1e?3jz4#dy_u4oy$)pift;@i zV9|_QQ#?t%0$ck_*3jRRa!&?6+mOaZfA!dNs=(U2c&^AlA}pnd+;>-s_^B;1zUBPR zRPp%Lm@zL83u;uUjtea6LvKXz9Las%zgE0LRN>PNk5vOWDf0l;>10cVAlTh(myiD{fXcy(+$#Q;qpQ?-#F9LZoOxj*H+%Lcwv7 zRpp-PBl@5Jdl~q9kP_j+Rp_M9h16fL20t25JUQ@Ck{sjo>&+1^GVT;mSwp6nReLIe z06zTTyx`}AFZEPT}5rJ4g>+V zk_Q7W|3Y`s9p;;+T!U#CfE+b{3c(Wp1rJJP4K`BuTKYAj1BA~l%951l)4_EpEpvrq zR)+B&YxCNjMzA0GhTEwC$fXLWFXKP#m&E)F8+DXIUj@JwFgZc%+hmu`E~|d7I&wiZ zUz`k9iTQKT4dTC-4MA=xn8094{Co^JotygE8$)5h~YV&dA6g^{eLq95#^c&$JB)U%(Ovc>Tez^6Z|G|{2q zR-Zq0bDtI8kYHh=^^F+rB;KH}%U?WN0=dUeRX2z*@f$!wL`t8*U34{X9yr*#rqobS zgh^FXJ@~l3%YhFxpU^&YAkLpU!vMv@7a)GchxIWql@$lZUr>gP0jN}P3v?>o?DN7T z$A2lrUVst=RCxpwE%@$AJr~^mQCRo}tihM$;Mx;l_|PL(kIu@=c`GIqu4Tb6c6Rpm zs+EDr5r)^xIzFl=C7wlX53{;VOZJ4(s1p|WZx9*)Kb%l#=0bv;;@cW9P#9jXwh2^7 zLt5W+1AWT4^<(x0)^k~bKE)D$xq9cL_aXVZ z&YL$s)a1Z>6!Fkc6h8u05C*gu0#Y?Iv0CY^kKS0l%iuj40{~KQrf{%*|MJjp?$d)_ z46c`-j;2Lps(_7xL;I)h!R-Mum;y;F*rJkFK-w0tvp(8oj&4Lxg%+j)f*V3$ar!mv zHf~rwZ@j|R@=MhRl7QqpDC++r0n>oa{5zR1*hT3sKK!-8NB~;DAZ!f?L#)B%q4&ha z(fUs*WDHaKdaez9=d>DLOI#K2nf~Icz>NM3*yIViHqH;ApwsZ<#$S-bbXI?SUuZ25%>fqNkxNg)3 z8y~srezu=GTvWyd??B|8=U3Y`WkeOX-cjk)c{kxqJHpbYYk%cQ=}$%`pCaw0duHvf zMU?#2MuR^Ll6rAiQsCU)-qs%wh6P5Id=WitgjIZ>K}0BN6@$E1xF#o}^++!-ZK(=-V`}Oz!5S!bK zO&%K!a~j8|0k$jr$1(L?r243S@K05j)d%6jymg1|LZ*umsPju`?P*m`@pjB|mv_x_ zPl=g=&Redd)(TN2g^{|G09qdW5~r0W>8mSR_i{e5@r%E>qX-knlV$TE3=9GT7xTycG8a!l&tP6uPZJLg0ddm>J!B8N*+N8 z%>l~KU0co-Rq;+id$+}YR+noQgb1a*qWg=z7x6Z%;voXx!S;6=qw1RZJ8{USvyfB{ zOzazXK`{?24l|mJ3h}2*GNj}6t`37ZNEIAs?pWh%I(}RwT7c@? zV@o#hO;5!}M;d7ei@+5=^OPNbC4&9=ekJ6eE5J2KkCMU-X)Oj9GYBqI7-B0*l1P?} zvEzJhGH7J3uojeP>SH+ioNOKU{ z4E^$vyP)Ge$a^NoC49vcoJxm-_yUv+mUtyS$k2w&rs)kgMHbKN?NeeeJ%|)Maz6(!zHwY*%T~aYX2K*msw#H;GB6xNj#}^aDU{O;nA( z=LAEzS8{7v^tEb!{j}0?j$4=_?z4vnU+o{@iNbA?g%TqoLfpWt%GuCL@;Ny^*(u1B zym2v`aUE<)Knp?UCA^#GsRtufXDx(8mO~wapm{QCz!fW>0R&fuCbC}?>9Zl81;3SRr_h(n)aTRH2~9PV$5 z@~Y6SzwRFZ16)v-wvoYx>{kKc)XKT7`)<%^LG{AkZ$#xO53_LLS#agQSVZMN8Zzqi zmNP-npL4gW_yqTacO0tB=SJu3e(Va}qTg$V48Uv*BxBSpTf~;$66V(LCuyq>PG}Lh zsL!RlOuDA@?L-Wi^MkoD$A7%c7L#B7K5}$rMMEuTjz9b{Liq5&(o3{Kt;Kr6>rbWm znXgzqKt?;)rC_g}-S5%A=T1HnHZ^6pg#p;v=%0 zu#l~)e$`Ml;kElx**ROd<^PC-hf6myw2 zmYKXvEdXIa{$Zjbliq5;pkXfB9B{6owg)f3kh%{(F!;U)cs~N7bs>HhM$(zJ-1s}> zVf>sbxWjGd78IKY3}9p6=SiVd;IRQt(}ozlhOs&X7m-PG;2P;7BGc|UJfYX1cJTJk}3x4)!E!IWgrfUEYpp@q;_bxwZZ^z;)ob`bhg=^zf!!!Y1f zV``0U0~!9TsVvq^CO!POewc5aS>9sb`O$)Y%OPmZCGO<*YfTxAEh)*A#=3VviV^!) z^Ght7*-&v{1OxZDKWhpj5Ce1rptG|;2H$eM)qE3}s-db1l(gKEKn^3=C0xO>Ukz9L zOxJIlQCQ3eioLvkv*Y*aEwZ-Rv_U-OuPgQafR6VLf{7=*n2I^5MpFd3>pl*_w*7d9 zJWBL`&hSWvICbK@i*t?Cn=M^cS5(W1_E!GTi-6<|2Sa7ikM!a=K=I#3^mtSFi=S=XO{Ape7k=0(NKPkMuBmx|FM@UlX65No z&0h{*H)LHN(*-jq)B=s&ATsPv;Sb*U|4!=$KpX}aa0?(<|LfLo#S~D5S~$;pCOv+} z&VQ!g+|WJZf2)e@v;VfO1X(O~$C|oKEodnOrcVqMksV6tQdy1Ti_Fnu*w_z7=*s|s zB*1upFql5ts890`DsIQ0iWpskGwe0fVTD^ueMgU%!Ri+edM1#{2Cj`*i`gDy#Q8iP zb}wZ*eh*A#t2R7ew4CX0qar$VGz0?+uw4)kg$8(KL2+DBr}e$^>7Y@Y3dX(WSuDlX z*4OA(el!?BkDGU?l_U$>;Iqa7<<`_7uv7M*c7ySXMc}@AP^lR?Zms-v_o!aDrO$l^ zN|VEaI6O@Y9O*kCiWp9=fzK79lRxP0fnMVRk^-Qdq$EI@qmfdKe3!wguaj|zpjdu` zX{pQFDdHi&T~vU;!e>rzxKw8&p@2h{tiaD?otiIS?5hM`+0cPD0TpDf)CuZ`q@-~@ zrg7ek_OAdofB-00cjUGTCPw$syhvdOs??1rmph}G7-kDrWu>}4A z1{TnFB)5U57}rcGj_w5gs0%mu1^X5KZ(t*`lOpuU8I(!ZMqlFGq&TGj-Sc&>@AAd$ zLlNh54dW%nuFy9{1MKhG+VDP14yQ#4O57r$RU=?6A z+JQ-32+=r6CpI5`Sjh&(=6z*He=~6SJRq<|CW}6?vb0aqH`EOcco4UA>nPA0Acg@y zm@uxOqZKn%^3s!{xxtWIlo^4FV~R~4{IBljt2&7De-kCX1^|SBAG%TvKm0|9qoG3v z!@3EVVPxGp(!-G!X%i-FdAR0Rn1+uC|L-zC;1Q$e4%DRE@pb0;U=d(Ee)qS2PlR)) z`X!}5ANm8c!1QjWq&|?x0b6cLV11{jT(vom=>d$jpZ-v|k8t9L7kCN-2Q10CaHJt1 znDwVYbwxr*=im7GLQA{=qdRg52DP*wD8vqns@?rxVT8tl@i+X`vvWL`%Ix_%_6^8(gyg?kq{V5zuJbv`o zA#Q^QgkNbc2j?3}-j>w~+ZCmDkQ zG8On30{>rWzz(Dz2c>~(qp{%%u!p1LZYzg`v;RM(2mH6ye|GPuW0Ef<&{qN*E4~MQ zo8!N^hmi?-TNzkD02~J_%Yo2vJ1Ml!k3q*khk}u$Y99@*hPXqq5{nZao}o9Eml8mB zo>k(u4A4BK|CyTl89esJPyirL7$5(D!5`=Vp`9!q#OIbd2o~nea-~B*1HVVL9%=-| z3MqDZpesrM9>3vBO0bw@IYtnKVfe!!Sjr?t2{-R}FTU-U<(JY6(fL<{Heu*sXyoE$ z7Q24^B(Pzp@tQs_<0U5@L0_Tfo}u}z7NAtj|L)kpVwPPmE(CtJHLkooe;U=7lq9r@YG!#Pn`5cX$=%!8D^JhFpV*L*zx0(L z-B^l6*YnB>DSijf;0L;g(XiJo-R|!Y2Ao^;OyHJC5=o#4si6^QM2-I$?3FtVhqO4f z()ZQ*{_;MkTDkn1L2zYUJ+p#x^D3U)`1uMF1BvH*%tHSx|5|Em()~wTo@0vP{o-d? z^AoRz-@WLmn|V``5k`CXsBi$t5SO9-Ku4y*T^%JG3Y*y053Koid!S#_>enI+S^Lp~@lY@3W4* zpgsIo-wvJ+)1usKDU787JENWDH&OFn8p}YXz#ej;@s$Hwr(yF_o%_ihT%o*DJj^`r za)#M8yMZ-Ahan>&uG&w0JQmt^hFoVXE7~hkIO6!Q*71pU6_8Ub<+MFvR%RY9(jF`# zE6PO~X?Z}q_+7!{T!jkNaQ)xc-6~+3LalvYfb*(`8w^77HZ{Y|o zYieCPXB8~P2|9bzj4QF62c?cv3&9MhGN%Od+{h%fo! z+n*ova67h9IlYV7A#LBMaC#RurAy;a@21kG5YPABBsMJB#?raNSSRmM^p6Cw zU18B=pX1NJI^9k#ii}PNz75Fi?GeSk$7Sz*$0zo30|YH6z0@Z4nd(QQXt z%My@MNx=D)4DKW3^lmh0>LT=?I4ohF;zzLNWEp3BI1 z8C$|UZ;kH@7Z@gw4MKo_L>a-o#n5m8~e$0jF{{G#i zG`pz2C>k=@zo^G=`&LEnJhNAK%~%SoVJi2N&9$nUW17A5$Nuz=rprBv9X=OszuFfz zHut?RPVWy9_%}Wyp()q_%l;@V4|mUA$hoRiOF`QsX3c+zz3bcd138xvs&)(G=hW0w zUs>LB>hVXn3gM;RkrI7bx@I;;53DIFt<6>g%s>*43ZI+-i{3heq`5&!z#cue5o7I= zh6C=}6WkH0tuD?t=;-!q z6R>Wdh^GvXh>xxN!!=l+cLS{EC7yGe6<3>Ge6BQ}VZFkPxCz{Cf zme=L_u9`aUP_-ksNli|FyLA%2OKz}gbCb*9!CyEyZ)H4M;fVK+G(<9WO}JDoch45o zTYX~hIwUG)Kd<+AB_o>5MDy#qX$em~KbECqKMDO=Gw>}Uq{&b_(-eGbkj6I4H$QIt zY-G~jIA61B_Et-`noDNi3Japt3BL7jDL80A$7yX$Orwg9g{|zu;Har(*kLDf1|t&p zNG}iu3E*3-x?^)yktQlbUmsb-om;(kcec=h>3ACHShzbF zTl3IMqzyx0H0)8LmC5Dw!5`gP>1J%09oZ!@gI*iFy zcCXU3kxLi2npzw&qJmF&M1qpaGs;_`GGF((f$*xPf1;?nNaWU6Fid1m3 zlmtDHVJ#VR&s_`^@8#kLpZ7k}q}u;}BvTMQleN6V`l@ng=_{lmg+CXIv5}=*JX6== zVxywJq0y~nRHwv<#fw8><5PLq`{Yq29}?mm6OEiNxmk^Btwapq*=q2qQc0B=0**BALn z^Inr#f|)y#Ne217`*88_nT+hHspfc}QY~3r+{7yC1&aqG@gqkg?*e%odWTT81r*36 zm0#p}538*ww$1v-&!JFtSb+cPnhWveFA4Q|or^WCqVPv9{Gs+o*?D<6?_)yhQ`$ml zhNre3OJqpSHV#!!2%2cRNg?W|#>cDQGoTLiumkCUWt#}JqsFZ6*WOJb!^UjY3*_Gm zvd1@k{w%Iz$PH;&tCy^nW2gZbx$W0`FDSz~`Ie5(R^3YysizK!tEF;MXr0#F1O=<- ziRZs*ex|>qO5kNajk1gxn8@|F%(kRw`6|%*;osT;GZ07(KkfzA6=Oh7W>2C7IP9?C zLH0lwh`c9(Lb!!nFGA^2nxQ81GKp;#d7eLHUO?cuzAh~Udw`q+V9w;QzM<*q=veah zBFq`8#OD5Ur?%Li+WFes6vjwh@HX89G326Q=O3xY%?mPmnJ%Q z<8seQHCXXc&Qwj^MV3a|5DVPNxvWM=@q$$|CN61Gb=1N9Ix?1A;Z#pK`CH{5epD&J z8;fS&S(^`JT@j|shZPczJw^UeVKqY~L;L&fPR{Vt+ACmP7Ot}+0u{;lyf;@F+bLz8 zX+}2Y)H>MM=MCE2@>`pS@NX0IOv5Z`tO! z4-==9cD1y;jI56R)#eayBM*X46`W*O#l{PcQX5WtorzToQak^)o=!13!<|P*Xi=w+ z-F?)gf;pdU|HyIvn}w((-wK~fRcld*kMfnlg1jiqe<;BL(3Z(IIx})Ct<5d7^yeSB zo;{U}K_+=RR6gVJn9~GPn4nC-q~?BRxJ*(5oV1JUSY+AV!K%q<)VIB zRapHiGShZ*S6fez9OC*z@j1{`bvz8@$qAUPYn}=KOZl-7p;-n?a)T#xS7A}ncV&TS*pkF#;Bwe5k)k>;bYjHa6yTD`kD^JmP%@ z3seZjjx=-%vj4s&)9Gep^qgX?Z_a%f6BfQ! z$0u^&;OA+X|1=L1hjU3z7VKgb6T{Z{5>x>5=8XrS7l0s*|Np_9CJWygXh(6bKviBO zdsh_PC<)pE4m=9~NE6L{IsC4{qRvkNucO#yh$3+lk!&(V?TNyOqyUJ&fIZEb!SSNo z>Id8wJ1RMxz4HqMxFYwC9>eZ4k^4Jo6d(nQtuJ4?>oz4jaWkuuU0}gnn^MICSnuJ? zGZv4@-D_`h+~lE=d|kPp`CaNH_!nRPZy<{bQ4y^l^KsH^nCZg&55IOup!Qq&-|?%YvI3QKztn$n zee!6Eo`AQD_?!NSRv`GupTCm%&foCcrMCxFb1{CG1E$ZV4cXB2%G%y+Qs&mie@znW z;U9i{=En5$jh$7*+!y?IZV~_2+z4EpwizLWi3acNfm5TsS3;(={eS*O>^I-_-hIs`hKOeZ^>1NvM?D97$#gs*TPXpAQ* zg6AD@c_;DAWC2MA0uy8rF6@@`DH)h?y@@6a_I%xaL2Fnn;i<`>F+SI;Q2#H;5MyX z0n;yq`zE%WfqLWJT7V*ftVtt}8^A%=bxF^}prpy5aAJ$q9-mOuEc9R)Go5*%hZpt- zgBIV{S*n1?iwjFxS@{7+UG@b2xIY*cpm4++4{nlHwIu?zyhPkfLx0tPITPXsfWj>R zc9oAw!#q<1qHN%*d)CgOApc#%QEa7DEk& zu>tl-+YaW(YE}J#Y#*Rp550SHHyB25VCR9ynztl;@2!(INGnw@)w*G&3Op8^;sYFH zD_+1#EJMrpLf!+0Vs>`$G+@GZ`e6FM?wOQB6G5W&Fy15eOJyA_%WbwUfq;k;VElqR#J2nsFl(m5gX%%t;?_|t%94xRoCwfc3bM0P z@61I-5ygFqX2NGo5Uh&fq)`Dh;?7}A4EG;hi~$G1YIOrI@&Ux%GKVwqA`1+aKW0xO z&>4V-KIgavh_!K_?uh?bQ>PFoVEl5gDu&bp1cus{F<-|101@9w=;O1HzosQO`L(Qv z?jm88r6fAw(jf5j_H8Q3rw1RU=^i>j^KuLjJQ#?e*HnwStnBOnq0^WJl%O9<&u@d9 zBIz(9>^8adl}K6vR7>K4N#{xO@L}ZZM~k@tvxheKL) zcfxWLVHkAl1JDHq_wOQt)(Ay<@Xa4F-#%>=>1?p5z=IiSI6^NygO1cO=sf!$<}sY1 zh%UJSy%un%1Mz3J9}0~Nnw)yLAa@>ixzsGuppxQ7H-w&!eA}^)-m!mIoh?EGt@8m$ zomGV#(qu`>?hzp*$$9(Xly#!WHv1Ig_CH7Lom&y3F0XT+Ofe$29}resR4diziH^Og zHvX>&SN#1M+Uo=`p}=PXv2KH1$3u$kNjU~*B5DkY$KsGw16Mmk!xYxwLl^d!*PYJP zHZCqi`*jh$V+%tijyyQ@VNM*{2|`T28VE=7IIMdK`9R)8H_%mRP<6|4UtpQgikk#p zr2g?45C2g4FqI{%*w+LM2y^)kysZ4lQ(NJWLh_gRCa#|u`6g5TZ)K2Y z0HDwV(dM#!Ft>OtaeVr?L7xH9ofs{xoYMWx5w|)Tu z(%RtK#C>SSl~l4};*7SAjyz7#=ZIJg2sM^?VEDtkt2^)Tvp#+L!lcP8B8FMQ{_6ew z!I?$)h>MeJ+&a*D_)6iwX1-$q%yS7v>aSGEaq+)&i<`lmB1exDE8}ZT;w3h8X{3XENMFe}VIla4-n~@-D3=&ypcIWwf=z3I0xXL@r84WhN>*>EaR_He-IuCnl!<{VYB@ z8i+-%k~TrA{5`w@%m(QE5M}_prx~|?Vs*XuBR?%aPF6jveL-k?@z}MN;Dy3rFLcyv zXwt4WeV}ekQ_Hbb54n_<)w})=PgemIRTr%hP(W$`r5h2Y8>AZ~rF)QWNvWZv6#)?e zX_1odE&<7*yHmQm;hph+@BPcQeik#Fd+#~t?){y;zy0m9+3B76o6AUhqrG>6^Ye47 zmq#)76!sKg0>PCi_WDDnEykee{)?|R@`N|?HuuhWxhvh=uk&mY%@fF<*os_u=o|Xj z`j~Fl4JfqtcqMe98S-GY^?nyn&L47QzP_KTKfcJ$tH51cpHFgClHW{qRrrwo#x0=0 zL|qEcz8$+VQeL&w+@M3-a#Ypw#U2-HMn-Rq1j&1(mI$ps50lEeNY4t5tsmPD$HlR} zp5cZ!?o*)^m9oTU^<7>2USufkIpaHz2zjO+lSi75Mc9m$QvxlXLC$Lj1w##83eow%vl?tFips6Q=eclMR%O3SvsecCwBzD!53 zw^FI=B9-Vow;Aa4ZVqRGhGJc}S3FT`FqDi`2okc4f8$F)V)KNdFBW@1sRJOCc!UI^ z{_B@CZJJnZI}1+yE&~_!ZxYeB#ufHI-0->`XIn z^kra3b}3fOkIyr8@7(2OzEVTt;XGDWdfsYSG?}GEwN=?Pk}3FvV0b=iE#ybhq|H!Q+yQ;T`Z5d?9uA359#v3oCXCZ%KI zJ^E{@rhru{es+I2OTn7X${`AqHAr>^3fyU?)EiIR?&@8Nl%OxNYyF?FaOs0?YMl0q z0%bx+c$`kYSg(Z2XEonG7V^ln7@uP^w|Jp-vwii%2!3HdtDqf`D=lE zm}%el^e+4y%42_0o7^a???#n+d?30GO*p4pMbrCme*xh?r zEYcK%W*G7@W2A*0OA@_}lX-p9gxmkF4H9CE-Uf*?E!eF(!-0kNHSI5AAet~cSlcrM zL1>e;6>T`v0NHuUeFGJM&LEtm#;T?S==Yw?59GiiNJwT?DKoSUmUEGZ!?#-B7kkT` zY)1(Zoe!rnefXyLVd3OTmY#0Rx>I@d_AU-??OkJj9z7w-XkGrE6?Q!2!dy)Pc?!Hw zwfiJ2cc8RthS{ECeYhNWH@#_l<(zGkPd)~$^V9FPD+JMPLT+?_KY67Nx;i?sour>t z;gGH#v8F<3qaC@i$?!`gH=BuKEA=-CH> znw3EjP5j)TY-96iW4F-l*{C*5sl|sm;W_bxzm_)3x=O0flqJHhT~WN{H}wsF8U?oa zpZea0gS8K^=ojzUbIem)p0F3xft9_o@c(R{PzZ}O5b)hNCp!z`e#}z=99f5K&J)>%gTBdaV>0;liY1O8lIK{$2Q;oV{T=r}d9XuPy)d ztI?O+-#+TjMG?@h4y&1H<{p|HK7@1H*AxgzeD-}WKoQ~V;_UoQKC8O(VRK)``+i7J zGHWVPP#W((S#qk5=17TWeELT8tL-X^%=4mK&wWWuLLP425X;8Hx5Vl z*{+@L^qKSuK;I}f57=t!&w7WxB#HgJf+D}Scd~tj_L!oVd$`qxm!UJ3({^X|X};$< zO4l7&>J&wJhP4*(YqlE^dBRe#AOj7hH@~9^@FU9w4OQm&u1h^9YSPTX;Do+MhC_6G zef6r>`}em8%gxPQ{fZdTj{4{1KHF2R`p4OJ3oyHu8K(Q2Yg?n+w_^vrPj>&<{b_9S zXJvqDX#Cy%aFT!&zLajHn^?%)`RRj|;tkR{EX56wY>dB~X)X^*YGyECVPeEm&O6wZ zyM0b%*C3_sCNCOxm@TF(`lR&vdC+JAX%s~Psi3Dv)cZt|tx;37DBRB!5E{&40R#IY zkyomMYj!A@QCQ{N`VW^H7;_(Zx8_>pUr%hm#%Qi9*x*~lYQyT5n{_|LJxWp5*3-+=%16oeX7*1Xr@D%7TOt=V z8H`_WD4!y)W4Q({>d&N=lT)~#-<6M&&q$7gP}x=^gNVmrQ(Nqsy9jh-+<0PNaN1_q zV>fq(uh4^r|i^VLtNW)~jM5Y_FyI#(R2F;>@KV0SrRMzwJ1(I@HN z+ptmxr=@GvDx6Ct=6kzzQ{QxRp5~Cs<7vIw;g)3B>QtqCU4+shT`W|x7@fpHH7Pqd zYDKO2BQqx_hAWl_sWI#|@f-cQx09fDZJqd*0sR>*C$kXeXUNyD(NgFyuR&o0W?N@& zTdO3Wce795`Zi0Sy)GSEDJUQB{gIw)%3wJ$o;=&+yI=JlmZV%|;5_xqLz=mbT@}R~ zFWNW=au`|=O>)?ybKBvw;8)tzKl`1BGtfAUTT0@%+f{D4gG4uX*PhqQtyowbX`St* z@o%u?6tKvT_a5S3q(i!C+t4LL%%0&%h_Fqy9^XhQSx8A)b(7xaFin6+a0FQvBG+K? zXK*z6<&@?a!$i@{x#?x{s;S>C9pVXS=7i4Omw#cwNUvqg9HfnR)cs`#$WChNvhC358bOH0!3z)a? zJx8T_v&otJ+p~?sx`?Y!Oso_Xgl+;ey1=Zc8bw10czE@n(qpCxY4thn;F6tB?nZtx zwa9_T({I`iVPbF<-Cs)yiOJDp zh|SbWFP(pwJ1pRTOSd+Dp>xL_;3>p0V`Ku&>-Bfedy}jj^l;9X zB##j->!QmJ6f7fi_(DQnmv>q`Hbtd{gwUJdTE>|ZJmGM{7&_s{lGKUIGJ0bX)n`T= zVoZF97Ghc^V`he<{Si%h!Ity?xB$k)&l&Z2J+E{Q1>ZQWY!F{&X#)kj&{Q1%CdaW= z!+c_$5DLy0AJKzoJ{wT_?kZx_Aj8X+jE6B+LJT-%AYs2bnL9rQ_t=%uK7Yw^bt1(c zvef^?T#=YBhz9)01xg#|ij2i)k|O-D-|SeOr9tc*DCXs?RBfC&#p+HgH9DSm3FWXo z5{&1DJ*j{-TQXei(E1SR7QW=FOeXqmWwMOrdcr}J`}*i`DLp4}K%GS^6wV_?DZU+G zl3~saALps4@mSIbk6jO*{J(FsK-ZprfldS-feE2a>h@B6<8C7=TDrx_kTMkl+X z2MDj(pGMyMRw~EhH#eNDm-Sum;H>8of_$30Kr&9~$UApVtmDO9F0!OTwU0qS$v{rt zDhyS;IO>OVKS*KDQ=@jn0bYg&-K`Kyv?Kn@PN!rT8Dog?pOu=0 zb|+@x$O{yjpj|ge-8Gw}KzZr))PtL_pq08Cx}Xv)1yL^cpr(?|_zSGgGJFh%SUIZ( zMoQ4R2BY)!i%0_a*H>pJPJgJ-X?79f@D@5BOO|(=b(bZK~*_T&|T+yk@-g~lZqoeCHyy|R@ttS6$=b-o7 zN_I%k*41d{MX| z*~@izFpF&Wx&HI;)XPQscWDW!f1HvT>F*-9SuwGrDfxIZpS4%a?2vbAB`6Q$-EGE3 zCFxDC&1Gga6aH0VX;2kh>0e*aKg)0%cJ%7ln(jbzNF(86x9Pkyl^l+FBqPnst6%Et zUo4&^4B{;t`ha_#{w8cLb!fk5VzHe6giSvu(0sDNpzmro6mWS+@hE9K5>YbD&WQ|+ z?W-GWJx=|a4bFGS;LP?_q6;x>;pk*M+=jGEsXnHjheWFm%vT|-$cpGMyOKx=@sDm= z2LMW}sW4mlTsxqh`fD9#Ga`Ci#u2YVqFQCWKxOp8*LaC2e|$^jI~gp2o!93m>`m_9 z1im<*isc+X*1NS~{d=t&X-_GguG@#&u5JR9%z7taP*FYAD$j`}4QcXQ5lzM=u!-lj z9ow^0LKiOg0g~M0sa?@yrttfIKa`U{J^{*q7VM)gr%A5)!nq0Q3v00;{21!TlvE`~vEXvFuo$XDwu4 zFK->CP!(NRJL)YfL=hPjQV`L`3b|hQ+QTBZs&*#qUwa%L>Kok+02MH0iLO&^=&)nn z=}Pg$!kOQFq7bjk-svm4^5JLXg5X-};XG1T3Z79xrba$Tk#BNc!8OTFpSoBmd2JpB zywK&RF&o~XQOlJgr5f?9{~t$sZHiMNHvg(rQtb;o0yr$ zMka?%?h|vEh*Zu94JZIb^1u6`!HD_zF$nnqxc%f$<6u-=AP5N3>Z z#K+)sa$O_Bq>7hU8SvFT=uEo58jJ{_F2SOUb>yavi28VCvb3U1#1>sbqt@NyPMOhZ zOuUw=&zc64j0`8@k6hK^m14Xc`#5Ws`G?JG^#P#agMtlKZmAyjztOejlnp-F9&S#Z zMUKF zWvdPik&~!z#38AkhZ{zMXBmFSqB6_pC@QD(>)RJ2=_DGpkJs4Eo_{H2Cs%1|s4}lf z>g}+g+E8dDErRm6;lO>Upf8-Hn0<5O?GW|im$5G>2PFb!k7~IM!XPY)gzjyUZ&^Oo z;JT>>0dpl8TsaT=V=%Su!g-w2u2`z;MuzcCt41G2SjQ?{-@FK zd)un7T(3~3ubhDfG=X^g;a``CMLMA1e% z72brPm=0)&jA)9AgW<)EyT8)^cO4PT{OdEOe_sW4-2XibTgHgb&}N<}HMqs!q5s_? z5zv*K+QG^wVE z{rf)Czgb%79vINhAJbX*rGgk7>3;{$0nb0qw?%+>n%~C%Chvj`%=DNIV4X`Wgns~w zfNbFD`HBYhJ%U8Mm@{fqSyNG5-ML&0IS+`+18{n6*`aD*c+0hpbq8IN)i1ND^t8dP zcDK~8P`7$!$q_n9(!w{?-3TrLG9iATQ75P+MKswtZv}Tkb!u_QN9BDsB1q*o@vhux z60cyFR~*uB8;_GTx9Oa+AhL)HL2%3cnQyU1tF5BW+tSAr6Wd6? zkRr*Q!i_)K$h-M;E=zRdoPt2TWvns>)S922pErx>`(AWLz>Ka-{;m{{f0WHYyYX#H zJ&(Kfn6z>`Y^XVmo0Em!|2hHKewLtF-<`_yHe(pL@M!EaHY*#%%0EC!-+u`9Q`5#Z zHVlMxTo|yMkA_u&9Tya!2>OB|o9E!YajJiJFzvpFrxuuli*4aYGqdj-} z(|4itEV6$=^!UzY-+O+1Xw$c1LHO*f+=11>uF5xK=G9@gC1d_J2;CJ4zdsdbi@&L8 zT>fs|Pj~+Wp45EdyR9v1XJ1*haNG;KXNJzbE3eiQJo3Fix4f_2(Fi|1jgq$%J$2q;`jUSraz#j?*~VFz>tuHFRa>Cs@IfaWkdRUNUoD{4zx>7pm1IHA+*I6s& zdx>1aLK?uj<&VD`fKyDES;Hz05|fG&i75#Mcm-E#-L*tG-L=d-etA@=>RS8NF|gUb z;cWY&;BYy!W*8bnV44cET>VvWa)~<-EgRxfa+7mZh{jrPMoa^`T#CG3c&}O(cJck! z*lNA6-|?!^T}fqGop0aI90HRJ4`@xn+qkpX7Qq1MY;Kh%CiIZ($?h?9whQ;3^e z%1ddFUovZI$yJG*$E@{NOSo2CW9cu~zAMA0u@>>+?xKrxd@7;_n%DiEw(|xJb!`?4 zmi$YuNBQpsb5uwv=`nG!qvy5RS1x58;-rJ{B#OQZ$g?7T`I#hpx@tXaZgW=ONr>a! z@1L>e00gY{Esp_+GM4OG%UUu+=s|36v%33F6ySuOV_RQO&xSLhL6}_BzlO-WUzW)? zPk4&^?keYJXJ0sp-}%tWdwBC@ZN>;5efV3F=Sn1meUWF2mfF(vY z1Wwo18AUE+=XeBOr*gsMAR4BoIgN$MX%p*vE9t54cA8-tUm=1&0Lm}jIrEVLmNK zqKL#-aWp{*E~kGZt|XJ(NpwPzg~kK`P(7y-S(?8m@g_{v1NKntZ47+X%H=&PFl-J} z`c60Lf)+B}t?l|cap?rEo5<1=P!ZpG_4`yWxRGY}p~^hW-ppgtR%NcqdVR@QTe#{V zW?$52B|6Dc$@lMNJ4@Udm@v7l+2s7^tBS;Kmnj2=x);lG@2AuDYpe3IjW79t#f$D5s)uMbkRr9(n3a9@A?7&j!a{z6yE%_2{#)gtqc-_=!Hxc1i9=L_z) zRM7hEY=cVqmeLxx8!=DMTKOyqbwv39`rBoL1(1t%h-!CF?NncNwjGBIxO7(n`?H6pium`Z=gdG494Gt{)*{aq+}4p$y+6|@QgwH9f3G&o6>32fZ+s& zP^0xVy@7`g`mX#_+Sue*-)gd?6#ten)A80X^YaQZOHq1WQKx!wE}Cq*3OqwNKWgH^ z!3jHFy6qXdzp$1xA?NjiuCT#{d7Q=Gzw@A9Rk(7_@fidi(aEWzg16MzkPP*t zNN-NHr=VX&hO1NuNv#=BZ>U3`#PIe)^AfuNiL|Qm&N)v#OEB??me5CIU73bZ}ixr@`e11o>c1Dm+Al% z|J=J)^2r0F58YPWv{PhQ6$Is=5^#nIyi1Mtkl$WDJ9*zc>O(t6WS8;LQcs(NJ88|9 zz$apLBE3*5n3UOfh7MF;g@n;ICRsuf->QEX2%mq-4ght#2~foWERT#K4;a751D`@9 zYIcAv0aW>sHD>elaWJ&_eB9gGC=h|62yB2CMxy?{y1vfzbzNc` zObB%M0KM;Dy;4^KWm?68B|8GZ{@?Ea|Fl*JkU>mJ0X@J2#ypPz!N{N$nq(QmPx?cC zYA}N6NUwzpduS5^&;55ZNIyWJT`M2Rz<_-9jOif`0&)5e_5$H^q~9rs21H~364_ux zC~!?k$k>UX)f^I%t1Qv!*ru!ay8LweC72WT zuGJ&ZZ2YbM6guKc)ZoxHhd6Ot9NGYZD&G|l4~FgS#&$+dV5}2fb*R+T+a2GPw|D#b z-ETL*pibbN7WAb?!D}X8#cojh&*$cR*jvD68ceAvQ$46~mqE;7yA}7(1g;Y+-OUcm z1sx0a#CFKU>T=rcdRhGZZI6!6*ZDt~0dq^P{DylRjBM!K+RW$@t{Tsbec!|4BVbFe zbvtf3;rH~1Oh6|R2mqugPZUd-CkF31XTaM>$mS$nQ`a~B2Ub3UiKCXv)c|LNMkv)Y z0w4N$O0c*K@b2!zGsthERmHBmzuTt+qF$JtAoVyGcguldw%mx5vt2TDv(nM%tb0LE zhh_=lDfHxQ=%JD0cJuFR#-^R%V=A+vP0vQGk5g?|Bh1&@|V3+3oQLvm4k6)oU&51)C|w=RW^w>~nEQ(~a*8Hf~ct`{(pw zq5Hz8x5B~10C3{6L}P|fYIlJ%m6$k}<%V=3?YlR6%l#;^F&$znM6jk%VIfVWE zem77>+g|6OD>=u==;}}7goyXLCON$6B#rI#I?8j?6Id%h`gl078^Fqg!}Zbeaiegu z@4q+v(~y;vI@3lw#f0Hm+P#lo_pcUkIB2%JDFKmZuj~0wDR0?rbK4ow%>Ye% zu|i6si|5q}F@Q^%jLXX3$sW?0VXNs)+ZFrPd@|SlK(tXX$1OcepAj;9)0N~>l*;Y- z`Dz;8DH{}QH>(QZvWMSP6oRCZXG;cRY7fQv-`NmHC-ksm(U|2~ytoC9cd-FDrhoB+ zQ?EvujKed>E6lBAuyd*Rg69o0D6Urqu6NulyH&0h`kKC(E8kO8RJr3z{K3)ee$9c^ zrjbO(GLBQ~uWR>0Q+)!otmfBZT+LKtWtF+x3FLE}W%E;OzInHu6t3M2cA}CXwrkE_ zWAWYfYTfqzL0(oLul-HQ$zOgB3l`7)kFuD>B5n^i_@YFNi-SjXjvoG%2^4LVR>dX>q@ zmEIisR~B+EvH$Zg-h}eR%{lyik{fAU^XZGeJ$#95n=*;auNj(^Z6TTLK|7O1-A;Ci zobT+adURZdH=RqF=|Xo|ZT6GDDn6TsRlOvBv%iYNBI2;Wgo^U+ zCx#uo5r+uaok4Pg%oDypC<{>s1+yL!k(9;s=st}R?uX!Da;>Q*4nd6{p^siBAQE%1 zDu$i&sUdVGmE#o{TUJ*vOrr8ZSg6)u511U`hR*?Wo=Sll=Ffj|UfaL8mCP9d2KWAP zQ2(~4mihCGiHvOrnT%2Z-DWb7jQ*5i0jk3nTQ(40FuFUgw`I$sDgk0BSjOlHFv)&f zs#w;G6>^Nu#^xO$p`>D}%WEldCaltY-PX})8j_o8bm8f$f$Czh!bcc;cbrg*g4T6c zdqJi?m+Ss%&w?bx9QKQMjo)qPQ<-hW3V)=J`zG#5*CB`MSYgGZ(8cjaYn9pQD53=4P9voP{|U{4)p@QmYOvlsm8u5M^lv(FVI^rI0EM!xF`6Eb?c9dX0naCbe3+cE2py*;z8)f zKY1g(hHtVjP1Nu1=5n4=TC}IHk3Q&IY^*1YdJ&@{!Ntp~t{M%w$?7Jog=2_QqHAor zR9lhaedi9`s?5FPTXgA=vqTq&3=7>}4cqQ{N>h^f=04xfy)KS%+yUP`e%E^o2Ztul zrEZudE;)om@Zh8a;lXWv@8w-=X9|)_i*Gi0F*ilSvIn4ipvz71p#Z1T6 zRqjd|^lHQ&Kho#wZrjLnKObvXk}D_T?mPeyjY;!5^l-xeErGi zsA*Oidq0 ztOk6cMu$~V%6H3sQX=-q&PotN{V<5T`YxPn1m79K!x?M@dr;5US}NoeESyDOt{AFLb(?_=c6II%|uVDpbVh-6Y0ym=-y zqRq*65Fkbz5(dNvEly71z@cEx*}n0T$m6WKo}ptqkfOF^rAoco+QLJp(KZy(qHaxK z+KGpUCf6p`MJ@G?(S3P`VYZPnxgwu4@(>#S1_AB(t!Bef`A@nU&n{LbDDnNEr}G3S zp%0G2f~DQhYfR7UR>9Bllx!ZGhsft-m`B+lhqCL7>h(#msJ{2M18-|o1?s1BqbW2x zX*Y&aZ8)`xZpcg6xp*gLF+jXU&C*4jRb67qV23-o|z=W!;7RdIm-%kx)tcmo#&jv$nNsW(Yr9SXJ3CObuF=6ITdVmC#KI%#~5eTPd= ze}-&3$?cuMpmjMPUlnMTt2_pJjaSuBDM5mKW|$N;Pmu?zdG$S0bDSJZeOx4cM&@^) z_F)%-0p8cQ(n;n=j%rZw4xOfXichLl)n`qaY?qw#hp?E}3kvR3@-UE?<^Q%Mf2B1u zJFKO>;9Qno+1S=}6`C@ZEfZ&oL&a5mXKV=zO@XLg%|*^#e=aPfsC?hIN`~t?NzOo~ zm!v;!vz?^ETTw@)MBUm^_%v4YG=Q2rwd^QBEazf;oF~aPiT523H@6--jqUi}S9mKf zsSOTAQM%w!K#9d}QMSeQR0sHhRX-;qukOR@LGV!U4`D}+(0_CHIY}tlc=G$jM(+~i@y8e%n&BaWP;-kMmElNZ;tuZyz(a($M-7_ckO_Ot zj^g!H1fB8DeA#gY)q@0&EO4}IbD&9N`nGvnthIKTUS=U)H9Z=d>&{0fMOEWx7_TxI zl&IR0bHlZ==~I7kV>F1N=koEeW4%_TPf!_kCz0I!=%r_BFQgX3Wot6th4l>9B5Rd{ z!w~e0UM7kpT|i5dija`g{-{KCYLhD`3NOsDAP=x-mkndsRHLZ4Vp;AxxIOYhRwsbszNGA+lHc|Aof$bALuQ^S2omtxrB(x;{#K}bF-;7olm5VNP~dT~&n}_KBOE!xCFHBsj#CN-}i! zWR=V93GIA1t?~(W=2M^O{a~?>9itLNI%U0ob=gz=?W?#|9Y#jI4t6PFS~}am)V2yU zsrI3~-pzBXt|`0dIHBsxRju+mI_Q4SjmIe9rJIspl{DWAv3<{1d7l53*a_?1UBKa3{)KBhsZ{r4I(aIB*;;O1#dgkOKSID#P%TR4-s8L(ar8^!te~R{xmMy?%?E5 ze;NE@bX)np_5!efC`sI^8h@*P<7_Ex8glAle zF$A0yhhnWabElJQmQmcwn@KDYB?v0*A1SzErIM$1q^a&1@F(cXIZVPl(Ac=aQ9Hv@ zn`2c|!!@?}sNXe)Vkkdpr>6xyKUk8)5nWux6dD^3LzM+}Vk`F6QHE6UoOM0aB)Dn* zo)B9^nv%p7oxsyCJ=1x<&x( z8uih`g(rBF&UsVQqqA{w`0iz;r;AIZp(ECLwpU)D@JP-@VWty4k+7Xeu520F*I#Dm zZSZ6+zc#Bdx3=&04LCWdy>#!@0kuUDohmX?CkCuEP?6UdLm-%L+HnQg$D1s!Se>6w zU9qUxjNEUe0 zP|ktBa|c3m=MeCF3g!5=&7a1&bGG1wADQ~;ZHjU{h-TDzNXX^PiC5>`?*R5->%_iD zOKAbTy&g@~HLyHFe712U(*N?O8J3bgdzwJWao6vfjnbI%Z5z_2Ym?hMiqNOl7+8{j zQD}M8WywWt^z_SeO$JI^B-K}kqOsb-V71MR&+y*`$r!%Rtn=>URj`G*Dn2ocieJ^~ zPG}%#W5@WU!=aL#n$UafJq@A1wW3Ud2%C71A7*6lix@TgbuKx@l*fWgwEbZ+(S0Hm zxKAR&Tv@j^s&yNk8MHB*+m^4Kd}G!gVlNnprACi0@d)ROQW`HH7Os^S^X^Zozw+`R zP0423TlIbMF(}FT*Rx-_77Tq$bEH#>IBB2rw zHiPegWyH5H;60)lGj1>ZBZa#mH*2>u?OcnT3tL|4JLqv@@HyH1yPN(xV9VHUflaYK z_R3WKN$Khg4v6Ah*zDH4*T?;}k+w@Y9D|kIvIWz{M*0k&Y8xsVA z)>9ts{#i;%Ib$5@&gk48Wt2|jOx?R}>ktNf2tkhePL7)rCl#wOM6QxQ@^(9r?`QIU zKyGM$m*dmhSFeOQUI~}NAAK72khbw=gVid$`SbjR32cg=mqvhhDZZ+LuG8}Ulum3y zL672|^GfC{2kP(h&lJ((GRb$IUl^l9>i0CPF}N>;W}tg&-%4M;GiI6V@L9rJuQ$_KhJ5M-LKTmMztbeXu&T&7no$+#qxxUTw#2j z4w$#qXJ*G|!ksvjg;O=RgX6-oezE1Nm-n#4W~K?dD#2tJQ>0*Wk#fBxwOK~fPw(v( zStFe?pM6zvNKxbc*tg6{T+!>zwgKOtSw6}{qStrY?o2^$Pv2br=FL}&YmjV)H zU%EleP9@#?StE3R_k#hTd_ep^%dCK?_?I1QUQqA=!nDcF(rgQCOEusSlG@;KHX-^h zJR>y=*ZnTfJ#CSHEquS~2-#t~qWS9Y?trkD!l5W-!&1*j21RVYJ0FqGvUnxp zv%fy&b7Tiw=M?&fyV-zCa&>|-A?mrm^K{|eR>{<+p=_RwsL{m*AC(Y&+`$~b%QAye zaZXH7vwn5>%H+&Zj_;}D1c&!&8!vPbgNBOPsQ&brDDAcl+v*bV7APg-c{r2$d>em) zs6GwSkeP$7ZUQ*5Q3hM|J09|GFg^cFdbEX>zfnA4)oDNFb3tRghOMo9BRM47Tz@v) zV*SzGfUnP|ubcHuEBVdyjxa;bjwtdS#~O5S_^8D0(O%ySM#?h=guWFj~6D_ zmjEsEpVei1H(3x=9l(qO-BR~z zrnow&_|=4;-+x?PxDh(PA`dan#E)Em70Cl-Y_rw(>mJB!fm^G%?gZn^|q324ScPDXQ%egWt`TWP4hC)c4bz z_4&&ikUliWRW>G;nN=`wjfddlQC>}}yL;Cx=XATI7XIS4mNApd!k3T>)4+GizSC_* zL^7Z z8YD@p(VXW2!wyLm6bI7H|085EFFw@ygU;F!bKdWJG(UB+4oDWRz^l~RvBNqpz)m_Z zi?3(Oj%+a5>Vop7=5_0V6a2Cv$cS3TN9@;nUV)tYzVph&{@rCY6$Z#Ih#rsFSpJ34 zK%Nj0nd&)wK_rd9+xMVidJ3Ur{M;dGRR}O`ni(E7#>U3ZQ(}5x6Ye88EeBW;GIa6q z+x%&e;<=~>^Gm()5EQ$BkB}(8#l(Pa2cRnec!VO5oo)tu$%KvxwGojd0;wZYkXF(w zJj<}L1h6(9v>pbn5U{<5x)3}sq~C3z?FyBqAl=@>dvybY$ib`NVcft`WhEAM8pv?)A_IX__UKd!^8f&|Kdx#K&Fq?XhM( zJ>MW?gMO~kbUXw@5W3+gcWlMfv7mW1<*z-X$@GT%4n%e_pl+EuIFuuD&))Hsfgo-J z>nW!@iqkn?r|F^;JmIj_56!Jwhv&tETN3qLVW5p&6#`875&~%CzBY(+L{_p;zBUhTiQ?9^9Tm zdHE~WiKkq8O;-*{yLIeG}lXKnywW`#k+WAUbrdPIf{g2`b8U5~B>FORL)1_{5sbnfNOYxw2&0A~rDm(;dh@2WAOySgU$^=%VteXEb-5iUIFkCp zU?{luj?(H)O$YWA;10RCTR_&{>a~li>dN`OL0ts``NEbvv;)9LKNdMr`)fbrza4Ss*MgSYICf8s&$jF3%gD7D2fMy>B z1yY(^9{5VRG!;nq!P>>m1fm0)8X6w%¥hZZBxDjC_>&dxD_k z+||_u5scT;(qe@+Ov+{#N|uOEB8e=UtZe{UYorS~Wt87+K)SS4OXB7M@>h^0&|!ua zhqc^5`Elon=vz4(7T<3?LKW$1)O^|$k6~BA6m^l`^7bIu+73yiA4qXe$X>KM%MbdE z+Ps&R4hAx|`D0M>M@Nm0%2oj&Qb&XVJ>YRoXLg7}_J>qE7(>n7fKCD#e=oAH4wi4`SWL4SsB3G8J15kNCCOT z-Swm4X7T3cCX@urL*^UK>PNB+%%}VA$+sHr%?9~@Lyx!!XjRsFVtByzi|!$n zcnq;2=^f1i+3z|A*sAj@8mZ?oK&kkO3#kUQ-I34wT4b|w*N3-u{s`k=0#E6A%(^pVt;S{KmFC|C>ezG5HlPPicWr`oPB5#Vii?pHtL9YL@=x;I#y@ z;H>ecwQN6xl8@T28Xp7@@@~5d{09?o^^uTLM@<8W(slz7MuZs4qFk3X9tLAZY6^yu z0#^g7X)YitMPTa{FA$70ENehffkUKROI_SmJN9O^nz2+o#6|+JI{l4@uc15=l_fjz zn?0Q@2acF;U+k)EruQX%#4!INNMH2^iyJD}a)Q3=57i1)(T!3OB`Z1iz_(9RvR0rkh<*pT{8@FjpBV&A0b@8CkL=UwPH zZ@5y@VLBDk?|N2e=VJ6@7|J8Vq$e+p(47gxgU`xZE1(;I*z^4MKJ{bG#K7Q>cnGK8 zop&Y>cW+R}a@~Y+Mi{ow?!Ri~`~D%6*G;B}D1Z>#>tAL(eF62sNkClp$u_NH80;1y z7MwB&dJ={_7C?H|`J2cU!xi)fdT}LA6_G;2PqPtxEPWqxwheo}3~dGwSIA*r2$ZbH zenOfZdiWNpAxq(hf=ly;?&Cj!O7ai99|u5d*tu6{{5oZ4x2a|Wp$<_1hWaj1Za@$I zLY>|@E<|ECC;(4whggyiKZsa${1ETWHgGX?0Z{*P@kJpDF<^iez>POxE&lauBPx&%)Vu8Yk;XIY{v6p{ z8%T?ak^-d#G6nn_`Lyex15gtQ$pwC`LD4^=ecW-dzuCVRQ8@?jLBR%guAQBsL%tvP zqj*5?<11Ao$K9f@qw_sA6%+^~1exf=k-VN2QLU^xiIwP;ynR3;l|NR;aB>idJ(oMS z_36`NAWs(44Ip}TD9WIv)nGVA<6!8h4UdoN>193rQDalre|7{(Cuf93rv&Mk_yLml zC!H}Nuu+B!Tb_y$?ZE|6P#*#LCqP{0O~N~oSon!adg`f<3JR4YJARXpkhl^84%r1V z>FOuVzKSm0-diXVSo~ss6k?VKpam0vFyO55yZxs%bh`a9fmiy#khVsedn;n?H5i}T ztRvO^h@nwk$4a&2CT$msui>ew^N-Ym2z`?`zwgsWIUt^{PAD4GfAhv4+&q<4Pqjl7 z*w47XH1hrhm!2R5aN@`NO!kP3-bm~NL;0`5MS27CE-c$~sG3AbtWYba2|9@GR6MYm z+5nK=ADb^=5i%5Hna*d~#P$K%1@9_A^k=zeJ2#s^g?KXnTRu%c0FlioXUxWW-vsMSDrz%IBoYaIj1xFFb_XC`r1O^P9*9$!0eJ2m`h6$MNZzgc7CD(N zOD!Qj-V)68Rloo~X404q&v3)yQ=gf+$4SPg4C~-)q#Z zH|0M{aICXbY{`wV$Xoo8oPx`YP>h#mWDBT*Wc=#|2 zbR>Brh7LRlKwtBeIH<@#9dcxIR#4lzQV+FpQP!%Mr+mtr1MLv*4eFm-Q4WwedY;BK z8ag-MI(6LfGhYyaP)mF~h|Gd)Yw1rc1NOv4&{)M48ypNJwIxr_YLHli3|O1H)WB&T zX|Z$To1DKdB8>E}c!*Jj-^z=8#_E1A6{df=z(gLrtoOBPa*i*aSBSnP86rxpM{#mr zGlE))N9evl)-$mlWy9PpeSffiFkp^5KThSb`(x1a&6mnDd+1t<41@6dunuP z)Zz^I>>+%0vk{dAmJF*z7IyQAiv3b>@eBYg6(lYuU_fPqV!5_d9iGgcD@gG;Mm)Qy zsHovz{qOgY-sI;)yjh;7TfcqlZ&xby;NFR_D{@lT3PHC6M8%D(2|Ow8m@yL;L$Tm3 z+O9!CE@X1E{=_`|1?tq4Mea&0tF@@KCeRH`!bb?q&2d&$b<$8@9Lz9Bki@>$zJ1## zujf7AwUBxgZuVAVgq>5xr!W+Ko zoAe54Lr$H13JWW%rTTr?4;uVjdPVZ`R4@$EVDKnd_w8p+9QrS41Ytgw1!+(r(MQ zVN+V9F#JHA{END056Gkv4Dg$5?MMy&y{ayK`)GMhH0DDg%be_j87EHs%0AAg3enGm zpXI@0PY|Y^O>XT{<>Ol2keVP6%<^bt!K&)Vl5_#}c86lg(^|5!l$c?7TSZxxYq~rXTn? z-Yu(4PT%ggE$3tPdENTw3%uUB^K$q-!^F?w^K);+{?_QAv3tY0o1R(tZknaqzU^cM zxx&qDF0m(YRDdn|H{oD@@l>7XbX7Wz-HDR9E+kMF zapkhEMN%`P*=smK3pFH13#8oo=N@CqtLw(AGb)U;4R{}1^aNQdDs0D>?O*xbT*?_4 z+S`x6UT<-MH{z93iE%(eyW&?&d$3wLznIQaPW#un>#cZ9)?mH1zrUCkk&%|>@b@#W zEsI~%F03wA@c~HKA$!XB>_l%R*`bfA?_xzh3cd2THhb9UtAug^^NNMmD_CO;d(+9M z9@@CLh~?W;x4~SI@_XC+Xrs-)Mu%xf?Ho5YN^(c%Eh@q<*0=$OWoo+hq`kw+{qODi zKCg-UN#r~4i)&sxv zT>JIAAEwoEzgc*7YmW5V@9GuEa(E}EllGR*|Gnj?xH6WJ@Lh~C@_%i-^RctQU~I|P z&Ec+bPE&64W=)n6f8Tpj1**n+9=wxGdyP`qK@8~?mV4xjK9O&3W@ct?{z%l%PuNN)(2E2Yj-HMS zX7iPnmV!{$WF*21HC1tH#l4+^@IoEB$f5RBRL;A{ld{k%t-vbz%=Y$3Ag#b*z>k)h z{xy~7zrf=0bQ02Nawe)6B}HOX2zO`X->+LIhx2g%JguyTd3e^ai_d;zHFcOIYqF}S zl%#Z+BsIdRq-Tv^!yM6nICMwe?y&&(oqwIs6W*1hw<(n9CgoKj>}xk=%DT(n;&7q$ zM}wiXz46-+l0dyIHTC`J$eJm=^3_&ZdsdZ(aQo_QgC81oH@Q%T6od=4R>pKs}zUBmC)?I5k3{jv*HQbu{H(B@A`LH=`1 zXEH1Z*?{3C#dyg0GYK{5m48J;8%2zO)q9du!PK8M?v!c9e97iS(jKLUpZSKe=y>(n z84h3WM>qG`e8v`E{CZJkh#T}{(i+tyi0e;l5!=sUmzdR7rZ|AX%pV4OsiOuxWpV{@ z1i8oZu9Fjo()gE<76qiKU8G`^^@>+otYIIbsX31giYqYg=(4 z9?{jw zHbBm{SYLhE1AdIxV%0SY^9)B#ExrAI`A0rShM!g2<(Q z@(=B+v4mG+ODgwk`#A?w6<%lESWDVI!>0a8l9EjZLmZm-yY&(%C3g5=4g}OeMft5G ztDbtxT9u29wXOEuO-HtA`Q2QDJT0z)|E@uY0e7c9|H|BDVBWrn@BKb%XCoKS?h<0U zmdoDLes<@)Z4MO~b#@cF_GFy{OhhcQq#y7C;2TKupX7I>$|@)zL2#{5R<>2OVB;`; zzV>`ZRG-&$9lIo`o(js!1aF#ZcRvZ)`*J{DKI7WHCT5wkBNJLlv-aNDjJl6dNo3P) zavm*VAqrN@!!o+-zBoQzIbijK|B7a-U*f$FN}?QjhDVHl+ZDgjXBAF)hu8+j8rU$8 zu1P%8yw(rF#60$#I?@O+;VC|+ByH^>>0YIVzcv-y}`eGQxT%%a4{Yd#*J432DY zUPRn4ot{}vFMiz39cDvYQ2`Sj9v6BFRl6%#;y$H;2Fqr_A|szw&t{~j&sXv|Fe=76 z0>R;!(}%i4o+bX%R#Z01U?Po;fI1k587_94xxiP|2C%k|-7$=M_PxVWoJ6hsk3Dz+uv?@ zL{T9Ccmp`miTh8Afe+k3HU_8`6nC6civekO0w@%`Kp##-H}2n5MkqQ+i$_0vKF=!} zusU)9)BgsBhfyF4!v!qIa)-=G@;6k}6X9UW7x1=AA95I``0=<0W4Frp-Ct4T&|Kf* zH;;6nzo6c^NU%!7Y0G2m_s$>)0XMJajur9(SD{5uUXGfYBLnT16G?65)|2tyD97G9VE?s0~q+8OPi-m@I2D~u33*oyOZC121No;Y( zL?1Uc_2PHJGN1kJkn1_c$)&9`<+2`zmhGL84at7i($1CD<*s+Hq!t%SR-{LQIR7r% zkLds(gsVV1$6)mAjP>DDWJ49)*l^!y#ra0Q2yHFJKIS+O9@ah~3kKDxFpoz86I^S@ z27z-5;IZ=6(+8)@MJOY^y&0>Th_cHub~Ds0QN=iJDnD^;o99pON=y!bpNi9=nlOI& z2-(lm7S(9!xW=Cevxj2)%=Q-tQP&IsM^Y%leS{^jVFmjXeH>$@Iv4)PCbKi7bA^$e zogU3_ArY0zpQ@QSZU|=QgZifxl`7B+JL}jY>pSmyGl98<1*jXaT8jF8;u)q26e__+ zXUtcZt7GqJAfyV!KHdOqzwYlTwo4JJ_24Id!>XBZ44p(7MFE16eWJf!3h@)oz<4RQo#h{t*MVmMB*9?-)f6!E ziwurl%`dcWW@?>->%oIHHE)?(43S=Do25qf#Fh1{vCi7i|235EnR> zGEJlacS4rzTKvG@!mVXopjuNE{aB{Rlb-ZbO)Hi4@H*JC*%#>5&8R_SvxA{G#)jwX z|29BVBO4prSCtTOe$e~yOt_HaNAW)!W=ABs+mtvy_j(<3kN%c=!M*7P0<|a)V~ge05`dO!3~B4#AIT!npJs>+6AD z)Y)QVElb3Un;2frk|P*1bLhx~#hy#T zaRK>(O2Oy{uT9)#g?!KEksi~>bxi}Fdsw1-bW2L36Ro!u&D_f~y;hPa2T%4TZ zLQH`p=3v4g%;}`44Q25#1bxiPwlh2;4FIPxd2LxdHWTd?jc*fnk^qQ4p;E>-+4e$f{!_WTT8 zEeo#OD(HqblQ7lqiclq_OOoGrLzt^z*e)or|1p(e3B*PRw;u3frppaTcfy{a>r?>{ zvK1q}wH}85+1MB*w>)%DJ}7^Pk+wy^z_oouD-;~+=ARsDdav)n(lZ=ic+Vy}ykA?Y zwV6&+EGS1*=FU6v@CcPOu2pNWd_H6hRP6AhRn- zaWVZzV}+9V_!sbULiSpE%5FS7t*3{J`@T?dMjrrPRrRNwzJfoM)u>kK+BKM2umgwa z=LB&O!S+WfaU-C&xwHKdUAhHCvvyW?_(g4+d4-|+>{wY?lw>{R0{SLGUJY7VZ6JDP zCo`M<(p;AepXK+MDT>oliHtj6)jl6tG6+9ic{OGzI6OU>DPmxrz!Ea~@E2EVVX?Z- zQ;D|{w@=Pa@2VbY;BR=>BWQC9iLj~w*#{9xo@T3XUJ60u&OmAZC3Xto~yHVeX| zLX|lMw}+V4W7%B9o~akXF&GN)1Nbf2DI!oj23EFY(rsI4UDi@k{f%UFtiNWUy^8Q{ z2{(z-!SPD(}$}PE<5D4 z_Vv4qT1GXANsl2tPTutdZTDE@!%mw>-b)^vNBA6UKLpQr&$D>h)3|csH~ii~XCM0f zKt55~NoSv8GdTuJVfQ#xJnPFkY0L0GS+~}s+jVldIbOrkYN^}1LT*onyEkVHWZsH6 zD~m0qL~Q=$GZ&!>3%x%6a_>`T%@2|^^0z7l6wmPnq_r z((J-*YVFQ%QRd!flcPfTXk%pjv#lS*Zy4BAS;snxCEJ#wpUzA4%y>*Z z0YEKNrho7&%5RGswDf&UB^FoP%_!Lx+a2aDdK#-8HaEw)$7fV8PFw5u7-#rA=l;4_ zD!Z_vK%k;#A8Y2fA46h#Zs+6TEmJC#<>hQjD-b7asUhck4_QjrdgAC>MJngXYrRIg z`?sCxS({kIPWc0~HP>e;F3URSGXoU@>1l5Gw>8WajCJl=x%nu5LkMRL!#Gxr6-0Y`(&+>Fh{yx$zi9Rv+skq%?|UYw=!E>Unfg%8ZG^ZC2YtB{UW zknOs?VKWaAW_m-!mQ=tPT}3Y^ce!V}h97ay*=n z@b+Nsg3{NR$&+b;J;iA@K7Dh+|G+5oalo#{LXP+P61bjB(sLL9b&)6eT9A2G$W^F3 zl-V9@F4Vy?Gcj^_Dzg0W6g~SUI_K$FS}Ll`MB$Y5;zebk{HJ3ZpO7%F@wkHkuZ1~@ zSwKLqAyh%!BpdP-`r3UuvIvy*Nur*9p_;%G6Ec|YzrJ37aFKOo;zizgx_Y(8J@ESm zUIqr4ifJ&>>~PjK)^v7km3%w5=UhoPhf$t&yZQ7B2ju-)lggixLI6ZPf{5-l{3Z2c z6MDIQo&H1R9coN|K$GK_9K^uWJjSO0MsZRDK%JkEkK^BUCa4nEGl}t<4cTICfGb_W zg!B~2hIx4=vP$@oA>2xZm~sc{v0as=8?tg)ZMWgCeE@vY;}nJIS_>Oeg(iI!JPe~_ zS@PZQF8C9?(YX975*1S3epXJ7EaFq?MK@5z!%#v78&VUMLv&$M3J90`KOS~!MVzmB zW-4y~=z9zLli!+4{#_@vDb7or$fZNH7=?q!I0~zBJ!nOSfU?TpZEFRc?cNfG zIJ^(x1YwfgQW12xe|812<%yUN)p5u{O@n+bqA^N55t#E~gv0a!tL9Ef~T^p%u2gt-gn3{zc)k&3@0 znQ@khJfVWpqobpP>b-6mI|!HRv5(YO>`$IJ>;i}UstV`5va+(urG?rhp7`?2%*@M$ zon-C`YD%B#s;Umh;D@+(rF_uBX5&Z3@~R=#*5vNlil(Z}=*KyH3AWA7bucc)ozPCc zos-5@w&`qDEOV_thJu*Whg)hKoVZ@GXj6sodW$wch#hetXSFvwpLgE7zlS9oVUhbd zbZYASSlD;=JsI`xz%w{UZ19)QX>N}X$$w3#abMu!9m?Qy4R%zdZTnmCXrKz989K*z zFjIOZV zM!3Jdp%oIDe(AiB2VPU~r)h*X>mvXP%2l%%D@t9XLSB%klalUKWH{O#wA~6{PcPT{ z`yS~J7T>e_o%f?n4}BGiS!)1J>rsHkR~80+mN-cta}Ue&8)TTZa_eosOG0_ORlicb zPn)%r*}K!dD-4Dr2Or?-)--re6%w6*3FUwEZ(e_`l7`L~!BBgIIBQsJJYe-cv|3Dk z%Mj6~Ct|ZC(P2OxcUi!HQRaPLb~4W0 zQXA0R3@dn36@MS_F|NDzVP-WJzx(m`uVR+tGy~RxAlib<2ktZwe46wV2E{mH_{w!* zK!}d0ClUz*QGHB{*yP#%D0YJR1m^4_GUu`ANN305>+ zL^uFLSX>SN>O5WsENCM1K>M&iJw6n*(fP8aC+qqu-E}r1GYi~^CK*^*H?GDMxxe?C z!P;@Y&63B)+_sK$RS32es9Z$#eswgKe|8cwZ^|I(RuW#YeY8XB(CjZf?D8czT2@vW zM}c-0BMSivHvU&}-b3%SqFTJhZY&7_wC*H>1xE_NA;x=(Ntz0LXg2Y~dn;1V#Yx_5 zY)rS`{1eH#gGCkBFPtq@P2P_Qo&6?_p!C_!6KKx7A7fO5x4 zei*7N8t`FUT!1Ia3=I!pkHEjn(0leVj9^WBMQxp2l<#fsD7Y{o`|TWJ-^aHBL8rh+ z?NYV)9hiy*?wAW~2y=zo2R+@1i9=jS$Jx1R*49417Jt%*jit6A!~aDYTP}tY&liHz zcp~qOrYLZStqx2*qg@&^$Oguq(cnh(p=&3b3$Zi&hnjWcrWr#5Om$Mm`;N#uLm%o3 z4-j0m=_31dH@)^hH-2JiNv>zRM-BSQ=r1_mY<9eLBt!lM(6+EA5J3vwVJ8#0z+rC2 zaBA40;DPgNfJybr8?5-$&u=(2_o+sPItdtXOK?%+>>kCA`V_3&T0p zk1=zyNYhd?G#e;~7s!b)*AH}i2?`F6M#{3r#m-r+JmI8_UZbX_(TNEmGZUf!|9z4n z%SsSN$8L$IG~U5G>4vDoXKS(X(wicVzn0F%#T7wNQ$nSJEI-M8#nY8={Wp11KJ=o# z?;Z?plLKuCY|@R6m656MIO{!TBPO`Kvz7(177_p%C82M^1c5d&UUTcBD>`di2SAck z#n&Kik5&8*Nbu0t33nP)sYoDi0yFOt`ncV}h^p>Z^1chNdZM_24TFtb2B~rJP{#K} z!C~R&{IXn%Am+Q^2lUOzi_W0f7@V*iNy2p5+Eb`-SxkDCgj(VS&WcZ^wzzz0SZEOj zY$P6ot<^LY5a-d=#O)y>+9>1`>fznN)Ar&^bo>9|m5&@UKj>^9e>vMroV zeFLNT4C9OG85jIUNMgP+@NiJo(`aRn>;=5ej1_@Q_65v#Tg5;F(NsjusC` z4Mh7FixU3)+IS1RHE>1Rtl62U==m>;T?p1UHfHzFUz|1^+s{S*_mTjG;7r|9SCbyN zGAz^FJs}R#A7UU}JCb+d%l+`i_KTrE)!A^K>f3D9_lI9pL#|jEU)+-P8sr&MK>*2Y zU}_3|z_-s;y@BYc?lO{g%8rgLl0AsKfx7t>$T3h2urnyMo`=wgh*18t;u0^))s6NJ zn$%pEK)c$K7_+&2g&c%-Ag%-k2bm9}x~l8yrpf0YM{5OXYKRYM^650NeXMCp9AH0{ zvSWBB09#-GcP0#_&r`PoQ5xXaI5{~5P^*tgL`=M9N$M9BL>4b11-K?a;?*ze$S&en zEwflI@+z@sWgexx&vq15*8oWfB{edkYH~&_RT2nuPmT*Z z8dL@Uxc1nmT3)RbydDxOH2nNJ#qU4^!GIZOyOsckZ+c}NG1bJI;&*`a$KmQ=<6G7X z!_OMT7g$C?M*dV%yuBfFK+NUTzZe6K->TM$^8a!HQYq?p$Lmwb*=8^Ly|a)l?fqbj zSyN`5#;b(cbstPE{XkP!^=3E14XlGB_C5S_!T0Z?MQ(pm$b--TMp!?8tGCa}x&`Jt z1gh$xmX+zYNKdu-4T*b2u_En$I?D%j$%8el3?-$MC73CyiOfKO**I{+VuY)NXMZ_iz1W`ID^erFkq9Vv{^Ad z&-XgA#S53X@T$`@^Zr&2-*2W^|OD*XJoJ@^nqz@VB;7t;wvNY#fy+kOifqDt_+*FBoh4HJj!}v}<2{{O!T!yC*Xiy+r5yPZ}gQ;rncNwi6UNvUz`wbg2E4ZL`YrTD< zKq%-@aJ@e4X*AUC=?wTGXAQi5S4SZ%hI;2WpN$kQnhl1`hwmu)3tt=zNV!;KRAt3V zO8Q>?_7~Qx&468j^tJ8q-ySH&gTvgJR3UW#%U0_x2>0@_2ES@oc?;}1`M1M!{e@3b zw6Z+5PUYqa56bm#JkI-5GHL6L{GEk|on+4OMT8EL@j2L;1%AT*mD{N-@GPpk$$F53 zvsKmZv0}grU(|hPS8_RjTMzTC`hy5E5rR{;-FzG*1?pb}cG~w{2IIq-<#mbVx{k0K zkTU)RpvOvjkh>Bu<$~7#{GxB2b$1X$tNYX#1BIZmkXzO9B>+X<%`<JJt=Mg~<*6XFs6e|Q+Y53n4;v?y)sbSzY6z$74 z=xJ$9uReIY>yhn`03#Onwc?u)JQ4Ko@cP@ZI$0}%e-R$xU|Xbjld_kaj{s%$JwEsI z!3Cc*3lh?u%(jbUa%55lm2^+|U#sX1NWkOJ$Y?hK1IWLl27dwd58kS}a+x)UW$ndz_5lP|=is-B&kW8Ii;;dJVyFr^Vmae}VHMe3nbbSV3!onA&@VkD_7DnO zlsw^+Kl6Y{;>4d$1{=0VSV>$bnJy|9=I@O#NTKBBk3qX*!ItUXE+#+Gk-y%m1TfZ1 zh$GpqQ}d*byW-b3og22gN2@vazBhNd9ISL4LGv4&?0U}Q8Hj`1fwvIH#Ynx6F$)4` z$s(WB< z>D~YR+g!~bZLTxC7eW|G;ji@8R6_13dSArff1o8q{N%)5`tsX5MyU3aP;9ZOUu)&l zi)d)RuXZCk5@+ku749kemX5OtWAznQ|AIJ?xw$q*`7@C_2aG5Bm;9`kGiNqgV-oYP{ArP zg>N<#0qC}!LYU9u82V7l&9<6z&U?q24CW}FWU|pm!_rB1K-T&gl2$MtoOhulyQ)3q zoRZe4V4~+*!ymvbbg=|jks`%qS3Lef+qubG)6V0C10v}skm+Tw>FCdtZQ8Bz z=Cf%D8qqE=#_xH)tHCkkl+z-gU=2&Yh$BIjf{&ByOk_Rr#hla@$5C7$TpfJ}I4`5| zzDpe4nQR4@lCw=0OOGKbhs4rJnQ^xRcT9Ii0e(zJ6&l z^Bky+WfO-tVRuPON~=LN>`JyK3lD<07{7mL`f<#szfj+YBBd6F^i&R=vku83~eRAsy8ooC9d2KbT{XknQV1Z;_WET&z>NxC;IR zl9r9qi!$3EbEYB>AFmL3z>~9D5SuM3Q>RL@Bwpsy?UKa9PTWc?V=}1As8{yAi67FA zGFihiIEKa%^D8<)M`vimxk+Cc(twByy2aJItPjKqD;T;S7ZKLQf;envrU3xiASk^z zqEp|8J5yyY6s24(Ems+;x;ZsA`dhA zfQ6dbcY7%9${3GCVDAVPzw;_?m=?J*d}QT@f9#9Ql&0KlQq=A9)u*p&51ym6t!0t- zT&~_wu-8TZYLrGIIHur3Q@bsMzt_oD?#RtJzz@&^04TrvWgO9NG5ETycW=f zRFsPa-A=2j(NXenKYbL!OrZ7&{2Zwt`fM2frPrue-R|!-KuOMz?X>z+J~})FwO;W@ zYxO=A0g{B)wQmB6U#AtIU{TT$M2Psi(=nYIRQ>x@5d2hQ>YE;~uNH7eJyi&I+gXFt z@w58D0;@N!vR;1WpVk`w2OPm54qVe7+mk1H8z=l2BHOe1C-@qG9`nr(?J;*}?s3}s zTHf#j6``h;h?s!WIAP~(+)DtG$kXB&5ie1}Zq~L%2z@W2diJkrc)1d5APgzgkTkqF$Exp1Hs58J! zPPN`o&5loUD>>-iUoFGiqjEk>t`hXD@uuhmO5u%6j%W*^S-+>?iM0@wZzvS3dy-enh0 z#HR?CcUAd5IP?Rl?fL!l=N0JEsM!O@{-7)V=@&8fl#uhRCD5YNUE+eZcVj-3mu=K` zf6(4`uDKcjZFJtkV3{uUG(9R+L%Ku!Zg=?)`5+9Va~HYpatL`oM8fkPz!ig@X4!(i zd~ylTo2|)+qYA7*IVr6`iu!2K-SU9>+G;c-JtxOBx#eQkAq49~`LKsG{O`nXtp#p` za9R%DTlMjBA}?c-(N|_9?osWleT`fw&q+8p3iND-zp*hbRsKujrNhB--Z=D(5ji{I z-BpK5Yzo~)!bd$%9GVKUhmPubm+%#60r(*`*Bq0v2L`N?U4dyuFjNgkk74(XE zHg1rtzLBM{avytR;dAcwyOQ=Ora8|h{67F0RpLqiZ*UAV8T|t*RjAa^is#aXZM>vp zY*JIl6|km&D3ncvv*yBjCk_(czdGR01v& zAAv`v1(Ea5s|XrFt=)4w7G00&Q^2D7mqLcJ<&GQlq%r){{BWK4OciP~?*%t495aL> zfl>74n4b+*kv?J8HdDaeewSR6{JD(1eYtvZSFJ2+Hkjx%@Fl|g$JODy(s2kmV86bH15FkU_p%{XwjVlMRGQs^vr|<>`8%XB}2t@k6CN zDRG7fBj`*jCHW|DTvy0+kG=Jn4p4y8a$>dGR`eY1x9ottNS2jVgu6WMaoYUi?T&9x zBIxt+;PLxvFXJp|8@#9YiQ`>)hhWb{FEYqkudgq+3=YVyW>#o3HcAw78)B zVw}5{8Bjw8y80W6Id+mu|KmG+CtPW3V_etWw%>5%100=vb*A$wKva?WwYCHRbjYs} z!XW%HZ44HOT0M~60MvuZ4&q0_ZH&)=gdD+|Ve=x~k?&^*F%^{iQH(brzC0yjd`A52 zY4!@6_~KK!bFh+6h^})+sCoWA59vgF?_2>Kf9;h>Z1jSFp4I>+BWQAOLEEJcwkua& z6qo0;ROrYD?)81;Y}J3)&!J{{6SMa9-juBD?8)-^>+FF45dFTZHLsBIiaS{K0gMFt z@MfGVC}I;rsC|ZiFQ_TaXm|nHrVLZ{P%dBnU`i8wtLmLHJCcG}F>CxVYAl+>BVpf8P|GLMuKLvf3qfhYUIHGGbdid4H+2!SMb?@Ma z&s<+>YPcakb<3O^TTXKK7d5#p#uA5O#s}YNBx-3SYiT4NEY=Z2elQONHOH%uu`dvP zWhP6^&!fXs?9>{2{}K@L$}~aeAU4>~2_}G~&Wxhhf{tpSg76@CZ;gS0(P#Jt6EW^(3Bp<;mLj!u^dHl(b<(j(> zLP6QnnU5@mnE_3GK>^5SxCz4n_QlW75BjfH490=IJO-e&9Mbp=_iy&xA2~jqO)=+o z^NJ=0&itYk)0P$%bwZO8^3=dg{I>u+?0U=#Nr~~V!Mf&sDt;j8b=`Dg>R`<-5n>}} zO6S%Ny$$GI05+Q!`&K+B7nh!XO6YzB8aQo_o>|jWEr2mwpjo%oFh(m{ zRkY8HGo({2zO~_D(^OM*mr3*5G$G&Bi*M#-fhsg;6>Bwg(68g>qU--@8%BwO#X`H_ zYd3lW9;@wq{l?{d&8xNT`}bcam9ce-cV5)EXuBVqfY5X%tZ#snDW{i3&~kOe{)QSU zK)JA!+_y7BI@ih%x$Fu*BQp$Y|Gtf|mYgY@dXoKeD&+B?eSN~aXMjQYz=GqftgK{P zB5i2^rU(ymGtZO4x`UUq3@7}mp^-?M%$CY!wbjvFKsj5Ry7znQ!tp{qFr_}^$*+bo zwUm(?UP>AvhxKm+*{`Vq{-{R@hetdPfj+eLvpP$o2FV|;8d767ccZS%j!=ceac<)s z-N6xnDUw)U@8CsA1HA^I7g3~Xe3k(rs^>xXA6$FG>P&x_Lf}f|8G-^CTj7`(7h6nT zv~Pb$@f5I%Vr&!KiX&`(M|dNBOQ0ew1LN-ki~fQY8(D2oDEh&8e-{xW+hC(#cbakA zfDI3pBQ8{dEZDJgd(e=213eN|l_#}-3nz#pGLUKE-Fv({M8^({Q-Zkq1Rn1&reC&Ux7sJghtL@DDf7v%ye+Rkm^*OjZTu}8PgNm#!}<^_8{X6I?ePoIlg z1{i{Md7n9JQ!a64Fy~=roO*F@^f(AhtUtLIa}n^cL}H54Ql5mGvztQ}SL9%_Z;5hZ2z?x;-A?<|N`#3J~Pomd?yP!YbFec1sog?oOdp83_ z>f%7~a6_pey{A?3Yo33n|CK#M97*HDejEU1wDA^cW^b0F7E^?15es#M4g{~g*I!r1 z9Z(9tNxpt%4Zb-h)Ejwlyj}e5>aXr!22NM@mLJo%v_Oy~Knf6=UP30?{6~M4`aqQ4O^TiSWwC2dCyG*4I{W}{-8b30={SorMRu^#HY(P)T zK=R`Nr`fT*#G1TMR-nB?MmhOEqe@es&|=T41?-;jq70(WZmGU3)Q5X`Xb7Hz;Vuxy ziVL`?;NCXaZeJMr2m+g;s`A4Zl+=4=gpR#Gcc1`nBr>Ml%>$>gVwyDSPx*Y*V?arC z2mVmEy+Qg&@WA^6pq2lk`_l9re3W% zKcUByvnrEs@=t%Pnm}!W~cjcP?YkAw(BB6gf+s->l6_(r3JQm;bHo2nj;ELKz{U z1fytbiubbgRN-i6+yd|_r83Cc(ra8{uT{$tW$LU{-Qk=NDnLxvECJo$v&%&#Be%;2 zc41YD0?&(K8#PB}6UO^q-}?H*zT%7TOR-}DF9C}Cz{IN;%d$LynyFQe_3maU-ub^{_Xd33JRJNv+ze3HI4Ft@bCxGkTn#Ub3uD@$*q!3ID1yDTpow|nt!Pno>GK$Wlv4MT zJMxisvgaY7%&ahi(a=Vi{T!gcU>D0Y-5aAq!6xv@&Q`nETY`A~fsu-BO?ht-b30^T zj|2g}4>|VtdkAFjVMWTYn}m=8G)uaZwE)>y^^9Vu9qCUffm z<(stIn$XII9=p8Q=b)XPPqy<$Cc2=Wa019cwki+}g^0*9 zLSbPR)s^45xYua0%tUe`lrPLE_*fu*Z?M1L8X@s;cGhHTfjrz`U*GQ-d+-hfO9Hnh zr=+TYt#zuV6$G|zrp-?3VcYg!xB2Hys=-pSJ6>-Ajup_ru``-gcn|ig5bPJwX#!CE zJP9z4q;bhw^a*IW%K_mki9ufI2HNjfHTiPc<>(?fXGsP4d%iMiQOZ zI>%jURwvFb{|w~^~2M^L6o2<2N0Ie4g2P`nzP!o#+Y4-+vE+z-KMV}$KBY+yF zgYn=NijZ1zjj9%Lq}#!75x=7LvanV}F_|X9$(N5thkXZ>NxA&7=kIjD!HT5>(LGqy z>0Kv1aHDpJaBtC@b4^bpfNSHXR_5g5X<`$zjSK}x930HQicw)`YpoG~EkLKi@ZZ0C zzf3zXn#GH305Kip7S^>S5BGEDB@iNbjR=Yu$2-Yxm8PzHr#3NLJO|O9hiex+Z zc$bGa3ira&I#~HZI;(kC;(kIqMK{WEr9#01r|g4>?#7han@QZV-5IVdEV*eu-h)NP zF2|ndJrJEV*P`3NugifxYA}mxeH~<}Rin48_qF49RW>Q#b#K41}>Sw^c4({%}7Ept?q=`P>2iwaI}F3NaC zjV|2$v-w0sMg`TSy-+~6mL0aVr4Gdwmjo<*NYTZiW=PMDBMNN$3GEhg0EoehYu1`0 zjN1sQM1VpT$ZY^s5-?11M+3dyP?_FTSe?K-2V+Dow(R`;*^@WO&Z01t$~A}jIA&ai zbNnaaT-Ud=IO1ZUT?yp8Kz^pL59b^)I5du-e%_PVnBT`_O7k#XLJxIEwpX-s7#1TQNu^AD!XOO~y^B zl61yW|Bd|><^72e@6$^uan#xveRe?P1ri^iui!f3ELu zAJ>BluAWIC1#r`c`&^ywQr=e~4ik?$l?3Fo?oalu`fllm{faj;Opj+yweC)g&H{0k z+wNH*iqovf0f3>*?PtE~seOGut=H~B$J4mXaF5uCOIad)!`N8Q?bYXh=e>)$CT!65 z3*i|vuMFO1ds^hqQxA>!{7Pi`?$VbFu5-#U9zFI*&UaXVWS8{YLEG_RYrTH+z3i0| zR?C}%sa@ea3$B49V4t9wKuYp|=odLg&Up+eGcQ08yte$E(9xGe{1b@y9W8S=GuYiF z5=wR^8W)Y)&wCfg(cLL1xL+DyVa$4#+`A!aj!6Ay+dVIEARj(B^Kdto$1-RfcpUVh zSj_zx_N!?_g+$)-O!9Ky9xPfOYu@kQPE(M_Cx2WT{U_9R5%88Fdf{^54#~Wy-49kA zW?Bvj__1G-<+YW3@6+P6#<5wUZvMYq00g16{Ssnu`J&Xn)!|?UV5=*hGDtl~;2c)? z&0O8t#N1tv_s6yfqk`=&zuYX!Atu%?lzP;-%BJUm^W6#c5`Ux z#OL_Msjsc{&<32RRY-{O$Wt?jcrCPbU6uClXg16OjlZBQxQ=%{3iJJf=y(zM=CfqG z;BbOcOyD0aFlDccO9Ge+Kj7jT8nm~T7E+}(g~9D%43OPYz{MfD#?^YRgcNY+>pcpU zQk(G3y8n24Tk+M6!ntXIwFi+wj}rk2Fa~(6ciVHw-PK;pbXHrT1Ld}JXT1wyS<7vu zKNz#&6?4COJZyh|BGMN?)`J8Y{(^<8%kq@|F+@tusnrxTUa|`d03Kd&HY2lW1w@*ss;sX-if=xO%F>&%{**ryduOaABJ0t3JLrXAm!42!A5Y-sD7FJUA@JuA@%G_j z{)!vXVozDqUEUO=cn;Ad;@#5ptIThB25IBjKhmjEh@BdwvA-_aS;{yQfiL*yE%@z# zu?9?XM@xl$xT}!&U}twU{lxwpQ5+6)w1a~l2fOzXfUx?)N>on#JkPVT-~#%7c7H}# zLJFRq>q(&^M_}Jx=lO$-xu|f8=N*}VuFDw3j*jT;Zy`PZo7WT7qNvEpsx!8))8*25 zvH!<?!Z>+_81~4sr?Ox`+m*^Cuie zUx*mrzzBTQhgUZLb5Y&Nd7(%Qm>%0a$(9e>AtLtthrNruK1Wk{+)CatU$A$c`i!-U zACzRC3ojVrx2LLT)e~G$2&n72IjRI?`tHUo|6ikdkg> zOG-;h3eqXvpi(Lb0!oL3AT1r65RvX~kZv~JaR<(K?_Y4&;i+mP+UH z-V-F9By2pt%0eL3Xwe=r6u%sA4Y`bCJE2jQ&0{YIM4vNP90Wq?m5~T(=Xl~Lfud9z zd;L`RAH1O2^z8liOo{uR?kkgf2)~>6*H1HpUDdR=#@od7sZMNXR9m(KpHeGU!I;qfjD}q#Gw^T%^&|FER67Jh`UQOLN{4 zb#Ivr%-D=iw!tId#=1xJ&@#)ZS9zpPUutzITE}Jsq2N}W3f3(UR|qLSx}!VzHz#l0 z=Fs4qI+fIOsm%0ZKrw);dqy10=|2jP*)qng_TqU4tMY0YJ3vrH8|n{RQ|3}CcUPkJ z|EBC;xyvglo++rLq@>;VILG?MbB#B;_kI3+)nd5zHZCoe{5~aRD5bYLIZQ&hXaN{? z*^Heu^MD`pucZXiLWXZI(pT0kM$U6m-)8{wDYI{B#}&xc&Rvv?SDyKZuAKZ(|NB8K zaGgfB=ZRvqZfIb6>9Vzt&#sWfAZ}#p&qmBAzbWdEYq26o@DUZk>^S6Y$DV3iHo(IW zyjNchhs?nvFz>fx%|ljSxTU71I7`^eSmaiDn0Lg|0}|zMWR9b^FHTsAfSkbXbR`Og z=tteiD$y*)bzPfNnKm#_qqryT5IxN1HJwl?H2wGeG2(khQpMC@*ULR2Oaw@T75whr z64?fp6t2TAoN!1v?0qDuhBl|2y!}2)QgH4b53yTCEFVWj>v$XjfMq~=2yh^aj;P|( zee$UKyxJc$C?|t)chb8|LW+0D2}p@ZQBLNHfVP0>6y~P%%p0B+M^u{;1|*FV%@|A2 zWkt5l<>#}ZPD1;rX3)N|4*_q)7FE4FXNe6b!y8=QHIN`G)x0XXVfWMcJlFSw{2}mT z>LW%!LC(-Ldv5TjkjuYQcM{-D!mg!?HT1aOrJy*zS|C)GvcPeB!Qf(c#ZLjO*HY;Qod0{-tg9 z(OCX85p;Qdn$7xwu9e1_OI=`p2jXYOuWL+eM1QmkhGc@SP-^-rIB&|0yHe2B zF!9p)pb!tfJqN=Te7#;HoVs^F)%m^^Po{+JMWc-!tgzs@oemNNH!%@`G?;-Of<6j* z~VB00DSAGHdqJ4)Jug>>lNn)rbe|wK|iOC(Nq!4YbXFjm=xH z?_GZSEG~K1qV30=f{NabXEz)r{SL7ya=o=iMg>O2e$o;=kJhXx$;xWwKau{U9VK(8 z@JcS;`2geQkN%fp1IZyW$6%HJER4UjHfjDg`L(`gSxI7*9Ci5mn?&+w$`*`LuwnL{ z2q7&P5gh&elE-8T&Xj93SG!?qSI7s{sKXIttG~DZhQ4By+hA_Dm?e9$8mRDQ=VnuZ zPI1az#M06d;wfYm)6)7s6S;Ce7&xYzv2k&qKf>YQ#&w}fzdG*yYi(`4@BFTN)zQt1 z{?1vVlm)u93XnvL$@PZ<3__IYiB&->Y)+?8+ScS}=0ls@kyWb7TwtpqT8iyR5bS9t zbKU!Fy?rCaJFB#G|HUGswIfPUSXdZyOQcaV*WBtyvi|#nz?%|r>Gp1#&+i+sy;QHf zI7oj0_f9|^^7#s|oG;fofIEdYjT|!Cc{Fg|HrW7)C zb+pY%`ufrVCBco63yvrV^L>*4f_smTN=V8PmQnRzYQ#?-N5YER1x3bYlFi%;s;=1*NOFh%q#7nbXAn0tr3h15N0@4>fvvrv7{4L&!`a_B`6bEomz=8g2vm zwa_@@Mc|ORUwzpx&Gs8|5h1R*n4FuD!AQH)0b2tS;og@*Pg6J2a&sjFSB5mfJX%ftq4dM0dXwZ726rl_@FS0=;plAjo-uLLfHND6>3?_5T%HOp*c*3l$-A=SwsuJ61FABJ&1(VPJWKt*1Pr= z_QJ5VHVaPypw;L!VPFtvu-CZL8=oEWBPC>^WG+S9-bP6m-8DsE2wNnxJ3UUQkXe@6 z`0~C3H^-eH8GUW^Dt` zSuNn`tdpBY_dHQy2CzY~;z<*C&~P{>R6yR2oOgj`Hl-7K9b!~BeBW2_g5YKL4e#nf zyh_t$1g$a3JkT#Yp#r9g&B{X6s+hOmRX5GCrvz-jx8^%Knw$UJF!rgy@_LXM-$-#j z?L1UWxs46<2z()|D49p-o{OVUC)JZTA|jVQz5}NVkR7(nLQ2<453^4Vgp-8OlM%@A z5tKcGEP*b@y|xW^CkTjTKI9R^a91tKNd`U6I^28U6J5(^?DI!$E1Oe80QYeM_=U*! zv-aV<{3tBFqC(3gVAkUi{pV|MA&R$YxOJ&%gg+!aT>KiE!L_a~j1y=U2ydQyO|Tza zdINZ1)y&FXULlI$_q>9H4>YoiS8-oU@ftp^ro>Fdhrn(M`<;W(QLER7#LUdp?M+Q^ zaAj2>_;43Cq&+{dT(!kDkq;m-rby$-+UkARMrL}<9sG#rOE)Sord8YDz4MGEgkUh? z`65}9lzVFt-_>lIQWa!DKeS7B`GzrHT+S+XJuowa`A&jE!t}6L49a5OnV9z__iiG6 zZzJpSh1L)Mh9&x8EXLRB;0h_!e4^uDi1zv*a7;>`3tSB_-`2K+)kjw?##kRemM7OvQlkZ7Hec1Jbsw476)D! z$upq;&gmN=0FTjQNsKdQ;eEU&)`P%=nyHqpNC@cnE~w zRx3G16mRQ9P|1p3anoMW=_Py}_%Z%p-B;B1_`6ss<}&!N8ueBBa%v38>)R~he}4^< ze)`D~qV1{_auWrySz(>Hl}r5y?EMpgy_vg4#^ZZ&HPe$VBkmYDVh1;VFz7YgBPIWS za2`v=Rr%p6>-=@d;CW=|Pe)rypRa^u)|OV!BLylmwjXlKTXVA{yifM0(x0xC2&D4q zRXM;ivXjuv{H#rpGlcPGtox@6QZiF21C5_G7Jgc*fx3hk;4HT#iYtnVj?NfZW;xmO zWbA{|4;Z6S!)8$NDSM27g;cYIxT`o2+yJYimo4|fs^BGZm^ zD_s~2Y3{yV6jmVriWSN7l%k7=uHJPpa7Xziit^;fNhLz{8OjBVGCe(AJqBuZ_+2X) zqQ3Q!5{FWh>Ne%ynxQEC+fUePy6TEjD+=lMe#L1B8m@iTw(4!K{!!kl5bAYo^1AlJ z69NpR-;USxrB^?ZYgd0==8NIx@~{j#^mWp7B?33|=DR-#BdVKoL=Gp{o}jo93XWq;kXXxp>wl6KN+Ly7i;co*vz zNS_FlQvJ2D@`T;gvsEEv^M=2-#B zC&{^MwFuKIjw!V1Z)s?PhB(mc^ZR7Q;WPAnGqf%aiL#gQrU zgdWqu8DD3xh^JR_MBoukOJJqZ>1uXM3St)&Zj0vQ|0;Sot3sVMXtJU{kW4_!OJxZ_~-8fWg zalGH`wH~~sQ{i=sQbtR;bIHrALre!OVimwQ0=11XoGeQ*3jG4bTZTs)SS9L8Bi z6c@Eo4zX-mo_c*xkQ*PX%FQqn&xxA^q~3lc7hx?@1|$ znWbLrX+QA+pnWt<2Q? zuz&u;2~M&Vw}$js%(!2Cv8%#~ry zg;rwN&pL4-Ehc~9)5#gD9lL`4oFPEk{P0Zbyo0}&zPMdFyn#g1FqY{}S#CWN$mg35 z>AM@8Q=zBt&O9{cQ6t<=<0G(}cA!)*I(Bk={h^if@w|4~ zSww!fqNN086dPZD-fYRJTh^~Y{LT8F7TZnSTLt&W%eNN%b4TsAvYup~RldWwMRyN@ ze4YK4UfdSX6ktOfkjiUZb@pNTYup)|6gwtNcpJDB` zR&oo|e=79x64;U`ctGbY_e0tJbk5t}&$=0-gQBt1s=$jP{4_jVB zkaWTvy5g<^1-}7Aq&e=HbHlpI!G=HATvBqsgkZi}M*Mvs<;Rb^IDWv;?E?iQpv2QV z4EU|nIrWu+0W}Q`Fk_pS0IzlqKWI#BJ3LJk5%ij{zv%M9ReK+HMtjny(+vdx; z#VeO4Eh}4B2ro{8Y0`jBm5s?7!-tNqxb(*xXN`S2Wq)IrTl0#JuHWtY6;Rxr6t=r- z4}5USN2Li^Qg<#Re!oRJaj|{sx4Mo{@4$WMNPN^7Z_J|gdP27?uj*Y45S))+60!Cw z=o`*{d%E5^#oKT7M=D zbwsBxnbo^{on^$YekUbHyt=qX(yR#B!(5N*9bgreyBw&acn5xF7yUR^?usgpW-scC zsOo0BHZshA#mDa<9>!Z5*aXb;99K1Dmaih-UXlh|u5W2&Wks<1m{3T+_uuePBimZ{ zlM#T8)YOPvfYP9(svY}@wX}4Ay9{2lwA^jvry%mY0;hGnyMB<4N@&aSTc!45(DoND zt9hH~PB2%ZAWE0n=jZS5R2`bCdpNNc9TNk!mY~7{TpNP%3l-7vZ*|Wv5yA@Rv@gOG zq@3_%gZC0zD`)b+uGVV z5Z8Th0%BN;O3W_p$3be{q6kz!qcoUl3}N{8316Qp2KeYZVtJ<*7D({%pUU4x0-A}G zl$7X(Z*Fex=g+d*+S-JTn;B$6%HvDgPHWMX?k60)*Qqsi* z2!1YIy0k4onNnQ5yS>;0*{5U;0H`O1v`|}<2y38vhdaJ{_1#@v zvvzdcd8_o8=3ACKv^2NmRnpYfu?=nicM?Zl5h0fOzz24a&UX{DG_=>p3XMy1?CtH3 zH(OX3zBLaGm3{yIfScQ?KJac(P>^Pcm8H4)*501Ag+*&eM*^q0s->mnvuDp_WpO*U z;^X6O*97esI@6WXfU3#E;{*Umb8Rv6b91UMUc69Kqy3Z=5Fl-6XsD+*xiVA$Zd$oC zez)B$s74$w=*AOd=iu-;AOPwgBu>ZTk@HbY-G*Y2%*=oq1fqW6%I=7Vgnx~?cNo`= zS|cat=K4E3e>p6x%FD~s($dDsK>=h!3JR74!Yei45$@``1p@W28I(YeYglM#*4Q1` zwaoQ)q^j*D?Zldziu>=B2^UY8MX)zhd%8H817#OpiBi-Gh5fR+4>v1S3 zD8db)2lmJN8y^X1ZzJ2|1yOG%k))(Cz+aC`$^|1_SX>_x1LcqEHmVp0S>b%gccErjY`W>~N8}8q`4n=$^Cle%+&OE)I@$ z0bNB!MJ1(Yn5O3DVG=xUE-qatGBPp}KT{JE078RkadC0^;Qx5BxU@9fx}OemFoq7VXvESskBI z>^Cm93;*rg_ZCug`Bq#yScG>Lqvg+aOfY%kvuHPu+h|Upd)WMqt|=WMz_Emw%1x&5 zj?U@*{eAFq!p8KvAqaA{$KKT9ZdT|@1JPjkSjO(|E-Wk#yKc91e+FD~Y4 zVb96Q(N>LBr6Zhgj|-!gs%nLWG(H|bT^b&Kr-c_AIu3JWkF?&)I3fUno9!~K1jQQJ z4~q5KM}d_xmOFxLLLW|~EtJ|2z@E1oDAUpF^53yZ9Z{;#bj9FFvzBO^z>=}NZmElo`D#k$z`cGZPCwt%JL zp+ry$c^w-I3yYJ}USwqCyJCEMYi0*rR%&<^IAp^1ey-CI3x*sa%<8{hftts{!jcPG zN_s6(Y^_z|FM_uTK+=a+33^x*nj z%4(dLsIEFM34#4yK~1d$(9|$?K$PLJ*+dJa{*vfGc%Fxfs!78>G6xoWw7+YCc85QsX)W?Dggcc+L*g9GqTU}jTfLR6j zIKhRV`JKkc&o5rUC3N@NK!1OZZgmxiAX=yQ8>u=y*(>ms#ujN7DIe?&i;m+vHKgqL{E$H4+B)(*P$6OYX*W1CTVkp0^r-z+`<179j*1*cj$_JR?*Eh8buV~Z} z>$=x$xto}nsH>9*LSagj<7yI$N;X~qSOGM~4Vj)X?VTRh9!77zkh+bE)wS)Ytw44y z_bp;?>3A5Z_*U%~tKc!a{ln5pT-jk@p4(6K=r~y{MvETh{a-AA-jj#A2MeULXF<$w z$MsoBZW9n(M{B4y$)9LWqq~TSYdLG(uDyMi>xSSeDIxq8yRxAl?P*EgYfE7&ydvG} z#OUNk<+H#4-~@RFTIk!}CXJ8iMYAt^M0eg6y18H6ym|BE$B)`_etv%4>e6lTf-(3& zNCb=nup=#gn6(@!c5!uO!+EG{>Js2SP?zz*M-=LNiHSMz(og)?$>XsIaHxnWF4&%i zfAd-k7(JRrnaj;m98EuyH=k#jDi!jIa!?_1I@9akIy>g^4DBClnXjL9Dswx^tLRe| zBi-!o?#86_wkgs1EN-WgoL{8TA!LqyJeM)fUPX_1kf*w_FX9*o&G zDOr>wDADY`f8+YRt3x0s3*g0IgEF0=DGLh=aL3`{VOSk_g+pc46AEtey-vaeSKdi> zV`o|kSI{nxc-L_`?)rR*wtXh86!u79^Iy=a)&22@^)e>b=3}`ds!FOESixl69?aSk zE26ueiiCa*!7YcTua#hbv}Se^2fW9> zMVhP3fK^+_#SQZvL_SJDc;^H3g=+h^Rg&ENww zWN%RWMp$9-?oCFw(?f!xBS_7=c_RQbC~#vJ&w#m5BB!Ok-ShChX4%<^#AsK)8P7|F zNVmZj7FG-Ate7e$; zcXH1X-hkNOdh4^(<&JR|k0lDL=Hrc#pQT+4q$9m<5wh{@!ft9twTrHPhHIthJaWyd zTsrzkKBJ}XePbQReS1i?O2>s-y*y|8(cMBwXwWIahfn>aM)poa_3X zg>Ufa^Tmlu_W5%teg{_7a{tbk^-Dk39)|fxicHWu`O3uA2L=d18ooz8S?ah(% zE=*2)q3u|zH#fLHV&5SjE7@9jr=9e`-m%cBxa8>CRj0~$ip?`TqF0RZQ=1AoB#`ROP9&B{`$`ee{4t9+&067*A41pa=*?{c%nF{PB47`vLPkzM(_a>gb??U5oVrT93ck5Go(5|*7w_xR*cOQi(ja0WWx+4B~ zVGC_J+{D`2Z!JvR`p9Dv%TLcr!=^)XnM=Of#%AMVa@mp7M5sGO+>hg_YPPlGt!c6b z2ggFv&v8DIx|Mr#dERaj<9m&oy4D9463ihfCGl>9y+iaj^o=EsLInBy-HQ$av>Pgq zF>a#!IXSr+mqQ1Xzpjl{8P>!-R`V)l_BcumAxO12Jya@aV!VMgc5~A-->R-2sN8LG zy77a}d`rBBab>)i-gu(DF7v+gL2~ZdVS8fd)a>a;=Jn$Lh{RskWt>qXoJVawPRmd{oQLz74QIQY>`3JTYPcD}(pSxRr!S}tU zH&L;%+IPdhxqTyg-Upp+HB$OBBg%i>L3z}~O(HE;kl!TF=gX5Gqx!$WNF5SvVtLw`F{S@zMx&RhA)ki{!Yf^{Dl&U3b&C-;-5FRH{fyO zry}3{ZhO>VsX58}O=D8(R9#|TyFX!Ap{A-uh|gzn+C9^yWZdZMFIo?Mp01bQ!0P-; z82giviPvWT?T`VX*aj+aPfU@+!Ex=xupj_sETtEZijZF^l`3}JwRW$P!oRAi$^Y0& z`oyjCYU~p^l5^k4tHx5DL$_yC{_Kp)GfRMzt7VND@HpHj-@;oP9Pb)`B%y?qloaKt z&9{Hc++geTWv<>Xlsem$VJF^L73Jz`-RNw+gVEG6R+KU+;}LNxqev*=al)%3f~ogX zb#;OI(`Cx}+)19GNp;>EK_u)UYIN#B4}CT^v1gp)^|*xcXWKCZXkjy?~*)x07JG=F*SGDJKLzGlu-roq_4=F>?21?4r~ zJKTLdGjUdVT$ASE{eG5*A@>$d*auNeMLLzRdB%Os`jUzH@ZbcYv<3C{^orM^`@$%i zA>N@u~=>p}} z5p*A}+Y3wleI%J;&KM{~(qTI)$SotJq2Y2K1(_1EE>VVgp@Tb%pMrp!ApHmf zSxegypPOGqbd}QTkFv|yTtdHx{%hj_=Uo|XmAWiVE2oWhGJeas5{i@MvA&Mzz&J~$ zHr*=JTnEds@6BSHcKaQpEJJV}A`q;9 zafU`SKYmzSFnP@)$|J9P7WrfvqE&?$j=-RWDw=NlHyp zW@pSONRAsf%ylFaautYMIUF6K@Yq0ep1Cj;6{Xv#%Z&Dz3t?j3t!K?LWa6eBdo0ym zrCXBavRku$D>;YmUj=u)^Q zFrJTnXH0&;Yd<&i{dC#&T}b~=Nt%|}vz%C&oaT1xBDduQ-R-fP9qhTkQVSM>-~)rf zDb$+o=|83Cq@)@VTAWO}p5T}NwQ%e4eNQgCo{}@yMS3-PG?)-h!Y68ck0bFzj|aE- zOOC(nOrVj;;#ux1V!kgpZAWL^;t!UKadoSXHVbT~(-=#)z6n;#QCrts>rU;~Zv zqZ)!I9$v>wQ`0*=uCH^QuA*Q?klBA!3?cCCCACl>+7$fzh6 z--nU}1Oy!ppTLc|Gn~PGmtRaoc_@COztMsV>rnynN6Nz}*a#gRC6gLADv*gBcRz$D71{DURq_G6boiXB(R8o46$(>fR26`1PqcBB6(V%(Wcy0&B=&S4Sm&X!C$QKI2y-frfgl<7v+&AArsp4r&J%?{3wjw| zly_puZ{#AZsoL~X=OOx9D{IyZ!)K>yjqzrRbmi6>Bb8=l>iT(;zYI;G-R z8QjVvrk%@63x6;>IGC>blJW*kmkSRcEGcu@CLA0zEH2(PofHHErwMgO?~?JkaJ;2l zbbUE+Bj;uk1X{_+i57A;+SKJ7Pe zSVf?)1hi7C2YY`UsF|2#$MZ4&cTc`|qu2viAs!JP9v&SX{q<|g0Nn86RdOiQ2X6QY zxgf30%*@UY>foY3Z|6~Q*1zW)B330mJv}B=iiS2oxxM%2iy0i9g8^LE@EI9O#N|e?EcZ1+WN=nMtuY}b9#V3}@Y*}z_ zg@24#Q%>nK%O0bsoNKk<*#bDA$&@U351&8JcLYu*Xs^CMUGuH^ii!Zeqj$*@{ly0^)dU0zw_EBQh}{V&+jDau1|tM*;T zu)G2{0$p{7qaWT2YUs*u1y25Sm}-5$?xUmGtS3MD$4`Fyl*s_F2Wa0XaDr^wLBkQx z&$>Dv1xd#yJ38u-i0eigo1=fT%FG2XV?3(`GfzYuFxlRz-h$v3jh@ zH!@6(1cPhQa7TrRpUaDa+6^tIdCyRlPBJsrn<}V4bZZoYPU}Yx|+^ z3F?D(jn&3?n?`cG+Xr*U-IgijCvkd1Iwuw=8iz5OP#5qv0T=!iwYr0BTp=g^)x_slsYU>Xrn&VZ$l zr{j^A{o|nE?C9tyR{*yA;I#=uuJfNN+D2bQ^W5@i4jMY*(piLT3gH|w{A(bgH2Bf6 zaTu}6LI91_;lk&Lapxr#OD0*dhTxoN?!<~20~?*3S#4X>>eFAR-fFs_t&Z4B1WQd+ zEe&0MB+ew(6*yUpL#dY2R!h8bz9ZsU%htiS8Ge! z9<%UDdFl@EUChSsI-K{XI>y{3v^r-IUT;V!XA(7y(H)~)#$Dv8a<3t@u*bDpXs0ky zIJIV|^jdzFB7lsyydhvVNmN9AM|rq4#%iAEhJ5wgGta2J?Qw|~=}n=N`3a$Y(-Qw+ zFX`zrH41H&7jKYXMLlXhO6Z;#E2#TWOF7Bh^E~bx-AiFseC1|7^nsz9JA-Vzfa)D!5y!;cRGTXtCOsd z!MyP=>4BqTA%WCzLYb`Y*MyB0N;tJ`mHF|f{%x#{iMiLFTD2FI9rtXdw25WBlH(w6 zo_J#CH?4JLxpN=Jt{LqvvZ3gQ>6Z2Qaa-C)Y%AHwthNr`uR9aC)*c0IJp;O-f4!>K z2Xlq9s<&8zK}x2(-6*0C{bSUFNaI-{GXW&6IOi;Oyl$iVq~KPoQCMCW{^F6m5J_g7 zLqh_E5}nHHB6b%YIG20rNOz6D*`lCu)ksvX3%q}JIK9VI`ufKMOygzqHF+1y*1{;9 zmUx~*>$6-3-F%@ z{}27w=IQHuSN+8Hulsi`7S-J9YPh+&gL}j3XD+`}x#zRPYAnjnxW+BgpWIfIXncN= zHLyYMOzeAM;P?I&$)jmKy6bA~od59fc7lnU zUu3612gu@P3$|NQFX+Dc=n>wa8BkiF@ma5UZ>SzW@1hgp_Nt`2-VuVt6-W`x^mN8d zhMoyebZv5)%-KI{7S#ySse1V+4s(bd;IuS5?WnJej)YeqHZpw6UQKzq<^3=T++U0> zs`uow-H)%5YVwCq-+n|>%n|>Xo+nX(;iIUyY-~n;9*qwV4=*<-m)2zFe?wcUf#DHr z2X?=%Rqy@IlNExWAIYNreRm9{mZJJAx4K}bca6T5m8^x6J3cd;5xt@R@-T)a*Ygbx zB{db74#9n?527CoUK=-TR%m@~t`9flMPkZYZHtG`TCA>^KW-6IBowPLS>d?H4~_vV z)R737Ix9*XoLs*cAIlf*?BZo)W|VH;my;r#4e#{-COqXFuVoay{^P^@rymU1?k*CD z1>a-$n9L^YfYP(ldudhU!@Y%bL;k95G2qAC&!_k3ULif*sC#r>BJEt5wCx(uqld{4 zFhi-EHezOZKH@712s6f3t`p+uVe+~Cr{z0vwok`Bs;xq(HzU3dtdNrdDPx!g7A0j! zZSdL%y?_G1i-AYqxpe`Hu^~t{mYmnNkW7@Qxn+JFP9DYCXULpCZ`dZ1)tu3W(vENJt4_uxOa>lP`sm#qPUbgU`y*9grGBuF-H}`FakMw#Bi^7> zP8T%&a9SKM;G-r46yQi^)I&@G$LWD~k+I=XnTR?oODn3-nZ@Oa-Z#Z+_wX*J_zlf9 zSFhZdGs$)h6jh9^db0sA2_{{y=3jw%1=H!m@oxFNcfqV*QGKTwtYk8pMOPBk;*Wp=P{zyi4Wk%ZZ4 z$&Bh;l6~~nJP&E`bk8KL&uXXgYUO6&Qn`!!5#J4Aomun3P)) zkJ3in=EJRph+60FXG&^0FMCzDI&Tg6Tdb~vS29bLXb zrzWeKxvjw)+Bu(<_)*{sC(2c5bcza$tD_B4{q{}09__DI?E+2gCr2^1Bbou`sYWoaUIAUaQYP)aMfjet@pJl?W$6`ebWCEx5{OFjz;NEqg zB{k&JJWe7kbAp@>^D2_lq^`QAhw`7** zgkpa9@Nr5f{CxBZm(CpwZfbKA{Z?2lfj33Nro7g{h>zSSFQ z2yb^%&4W<2+NL!IqP(TCQBqE>e|hKL=XwZ(y%p+}s7||tz_G;e@MNJBO;molw)f2c zdXLyoLWXZsUKj?!#4YMU1$l#ZlBTciP6b*rn8{j<)dOs2*zWo*z7W$^fqyQ0!W1Td zk^wwxxw68d>RZK{3jpDxsv@vSx?~#j83ljYDO87Tiavca_-EG15|Wa^8$W0h26rA! zm8??t#EP&Yu}&*huPv{pgITbp;Pk)%p@vO&=O(5;NpXX1J9nz|J7@rNK>N;u z^L}(Bc`~^n;Qgzz{Jf%G)o=(cNb97k&n-=^{#$VWNGiPxVh6m)!JEvej^5HFcmiJx|qq^FiceYXEos^`vl+2->*d;cA;etoKmc9RH-6UEeH z$rrQqx_4ig*>+}OZT^~1S;03K@S z@F8%`tQuY7^##svqdxRP^LSr;F8ccF4QXi^;Dn_z`v6 zkzYJ#Chaq`j%N25E;QB1-o4Qh!v5>xTn^bLP#grlzj@X6_9Gu^;X`*8plUsDPlZWJ z%OdcTx=aA4q?)BpnKn_1rIhe;t7a$G6F}3S#l!wPq~CMRO?+C$%|lP$v?+l58_43q zrFh_$5NEKn);veeoj32gx9ye65!)yOc1(N&d&IS-QmiWbs+RJYy98 z!BVmlG1+L;*RNlrqS6PJ0rGXk3@F#rJDuq3fo|Lg#BHRMsE9JsK>ba9bVP*A2Q4-s zHjg$l7o8^;Px}3q4fD{AX=iXR=6J#GnZ*IkFbZ`L(_s<`Kv4jZsBxN?$akTU&!68| zy_A~#oxSnk{;T(%|o~_})gbc1|4jQlap|yiP_*vyme;oTp_iujcIf4B>(Htai_zH^0TL z)CNwN!`05^o$Zk)Z4-{2P;&aby;`{Yw@fXy&kVZi7He;|nyTI0`2jTsyz2)eBGtr_ z)&G4>>>1_Wi^8Lbxq5IDk;W%#2jMZr7tAipXOERn;PjP__|EbfZ0b_|+68bbwC(D| zFgHW(aPsyc)O4Q&y7(}T%* zVlsPUix0lb(4-h2D*lXLb*O!WbWF}l4bUs*->OZ6>NQ&S+c$`x{TI*g9UTmRn^ zgA-%j3~kqv%x?nuT_7h50dk?AAKcD>^4zw%CO*1)>x3B)wE!11%yPNgB6Q(1dn#PY zY?~{S+1G98k41Um@%k1X-c7>jbhU>>CU@^#^g1g;Dwu*;QX5K9`gPzv>PhS1ECpaL zH1JKeY@4q_Q8sA5zc_fz>PX-F{D_|ZBR*BbKcEi1jhq?(C;k0yq}GQT=m;lKb+%ey zsT<8ge#iWE;ary}eA_rDzyDr^qRi9In%JI^qYU4h-n*uAwi=voW5S$kcI`xj?lfB*AP18eJC)y(X%@XSuYxUK&aQ6w~Ok8RqjJV4QS zP!b>YwzLH3MNa5S1Ng?lp@>?la@-R^!n1z1DxHXRhqpMlOPDW9J@3yjE_CEqYPMzx z)Om*jVf*{e;g!d!q`)AywzeiDBvg6(Ea#J9AAlYKj$~ADaQp7gFqxohVSfImejT%J zl~$sH*0Ve!A|iPF#`^mARpKj&`T5;rV<&r@cM#V&z(q*6z6V=aX*<^YR}d0atOyN& z1V%gxAuDAS-4oJsMtjRY6IFVsX_$_1(ldsPE2bl2U+mX8`8oL`hTS^H+9*2z~ z57~{|Q*?vKc-bC3f~cGQ?qwXk{c3K+Z-oaPe_+E-gwab$5hbjHjvO8yMn~V13OznK zSxkf8z}rKDUur6(>C!SXwsv)e;CFX+DyXVHk_vs1j)R2-yoVv!Uxhcfx0N&dAg%CD zd;SW5F9DM)C@5%YVbR>uG8?2Y%rg9=P$^9=PQax*-z?m4Hnn-IH=Jo>Z!fLwp-*pr ze}8Z9;Lwn-pWi(kKX@9%CM7?(zx(mBz^JJq!SgV^$>1KZZAwA{g=~dD2hhoZqZhvB zi`28WX7LimGzI7@KwMc^0P4C2=rDL2hHphhMSXpJJ3Bk?AHWmhg*;pVOxqAlL44&M zKAY`~WVj*JhZR$_x3k;Y+~o5(vPQ-TEmr^WvM*K1j?UcGv>hfecl#UUUfQc+NN@M&s& zvi4;-6Eky8Ru&9$dPatswKWBd0CaD>(hZVBXWQrDksS%b69AAcEiFw-`jc-KG;N|} zY6?isj(9;3Q7f!k*4Ooci3tE9gNy&x)=sxZu>*v!@EE!@VcWt4$T@8tG6)Ms|<8ZSc{PnJi3W?d056H@`xwbHBddS*#%mAbrJ`(KQ zDBx#*k{W($MGMHANFMV|0Qi>CbiQsQ;ZUSl^ zc3`3#S8;Qa=-MNn)V8&K){Ff2?;oraz^1AxD+5vLZR8zhty1@c&5(x@j`sE-b;^Wd z$z7#hXQu$>fyBbP0OF2l&dijQzXohgWnWd5RaNJvrq~>olmRrW5#3}E&F{3fIopDP zfnjR;{=wgd2B&ll=6B)Y2?@F{ULY}}K&s%+4S{#TGXqFq0C-YMf!_h&2hg4XlwRyf zlaJ*ALFw;T)zWhJ#i%d@Tg@*6#_H``gr8n}9KX{{<1OR| zYAFDJ+xLQ>J{hE|V++ux?;l*bejQa>x-J0Y;k7cD*WLX>kr0-YwD(KkkO7LU%s#-# z)5^szgtEKD%ge}su;J87h866grbOXVcXxMbY3#Cf?|Rl~v! z!M{?O<%553a^|;qftG}XKeZGf!Lzagyi1|fMa9M4&leLgNc=XoxBtfKycJ2Twqw~fxr$hD*p~k!A|ldng^Ab};suy& zMvFKj9$qkW3qR13z|O=h*0s^Ct?oBDIywr=C*1HM71hFnrKu@>fcnq26$k#c)k1HS zAcyqRQ)cM`Lo0 z0f-qX2{Q$FW>6u9O&s849f2{H5EqBd0O0wMA{i^-vU!7Byx8D?`?5>dBIrB-M2BFb z9&0~4y7WC^XQEtn2B~``i3RZ#4KREvA212cxvwA&zf|z$(Ub=gfbWzsP%jd&nm{EQ zZisuWc0R!?9+*i=W)vB|`QSt95WKOLmIWLlDnAf16@Ze|i#$AZO=ogGa) zd0pQbl{ewB7dK>)s-%;dnOS|fl=fqL#0dCtn#_ znt_k0W&8fv+3sH)xcB~k_rdpdKcDX%!2IxWaTXfE)TG(z#J(6v50Ee~1x`a);`TAp zKnE0Hib%G7>2)T4erjN7Xz1JBA8ZiCUEX7l_0($a&!*F0hEI<*LJk4TwCLc4HqbJ5 z?(S@yIgiK7jCeaa85I>p3%d5W8xY|j6SH3!gIOcP!$4=!M+O0YobVVh(;kkFWeSC& zq-38g1PlgMZLKcF26#Oa6G~CvRs#Jw@T}eqv zojX<%owb=68J8pha*(UohdOCzW?yeFDC&El*1-h3e?RxZqrSd^RK`teL#T3~scEPa zqKgFWk7j0Opz1=w-{EjtjOy#xkAje--nKgr%|M%!HZ&B+6^~9%PL7Y$FZi#g!erh% zEHkIX^Z63vIT#=(?`}rd<hi>0j$E9Jyp4a*91EoUkVr4+4DRb9?x zs;+I}(MeUF31YK4x6Y~}gFDST_1Q>Q$5EBKnZ!$6@DBl1!Dc_GsS$qVQ~Y`X%!8X} zmpQoez*AXRT8bKS60DFnE+qr+24L0T?Ou7=jv%Q%=}o?8CBqjSH8@@L>QNH0Y^h+1 zQn|Dnf2=!H7UI8u|IKesAFSxPBH0_$x`|5_p1ZGYAvv7>G}BqbdmcQaj}#vpo^$$8 zs*M(>PJ;wM|5o0)d$Z&+*;?98u#u~32#Dpa51m$Ok9J0~Zt?>K@quD2b%QBV*I zFk_9t{nW%WwOS3d8lY1I;t#*SqJP$ie+lrFey$ zKsMzojK(ZwT(qcc1(Jz1rA?jQC)bJiNr@FISdMY|DG-_vS1;D}!Z_7XWnnE_*IuEpy^vv0lJBaqXcID13nm`?v zDC0C-bNk`-aXvfrA$sUNScbj$f{6h`qouX=PGfIG2E@XcFb@eEG=O$7fm8(Y-G}%P zt^_SQn*<>m81;Aqf}F?w4@W61WSpgPQT{DFwHZe`stLB{>4t;9}2UWzUGf|tTbq^Lt@4+bVUheW z1pw+uG#~=X0Q;h^^e>?^7~IN8i(wKnbNtrFVoQX)ZRSRDc_$uy$699y z{|V&J_f6U2A)3_`4rF5qK!wJ;93V+S@YM3JNgBkcF<2r4NvfKcg literal 0 HcmV?d00001 From 29807a49255a749400f419576690bda7a5f6da32 Mon Sep 17 00:00:00 2001 From: Andrey Kuprianov Date: Fri, 4 Sep 2020 11:04:20 +0200 Subject: [PATCH 05/10] #547 add missing file updates from #529 --- light-client/src/tests.rs | 46 ++++++++++++++++++++++++++ light-client/tests/light_client.rs | 53 ++++-------------------------- light-client/tests/supervisor.rs | 4 +-- 3 files changed, 54 insertions(+), 49 deletions(-) diff --git a/light-client/src/tests.rs b/light-client/src/tests.rs index dcc407bcb..6ad1a400e 100644 --- a/light-client/src/tests.rs +++ b/light-client/src/tests.rs @@ -8,9 +8,14 @@ use tendermint_rpc as rpc; use crate::components::clock::Clock; use crate::components::io::{AtHeight, Io, IoError}; +use crate::components::verifier::{ProdVerifier, Verdict, Verifier}; +use crate::errors::Error; use crate::evidence::EvidenceReporter; +use crate::light_client::{LightClient, Options}; +use crate::state::State; use contracts::contract_trait; use std::collections::HashMap; +use std::time::Duration; use tendermint::block::Height as HeightStr; use tendermint::evidence::{Duration as DurationStr, Evidence}; @@ -148,6 +153,47 @@ impl MockEvidenceReporter { } } +pub fn verify_single( + trusted_state: Trusted, + input: LightBlock, + trust_threshold: TrustThreshold, + trusting_period: Duration, + clock_drift: Duration, + now: Time, +) -> Result { + let verifier = ProdVerifier::default(); + + let trusted_state = LightBlock::new( + trusted_state.signed_header, + trusted_state.next_validators.clone(), + trusted_state.next_validators, + default_peer_id(), + ); + + let options = Options { + trust_threshold, + trusting_period, + clock_drift, + }; + + let result = verifier.verify(&input, &trusted_state, &options, now); + + match result { + Verdict::Success => Ok(input), + error => Err(error), + } +} + +pub fn verify_bisection( + untrusted_height: Height, + light_client: &mut LightClient, + state: &mut State, +) -> Result, Error> { + light_client + .verify_to_target(untrusted_height, state) + .map(|_| state.get_trace(untrusted_height)) +} + // ----------------------------------------------------------------------------- // Everything below is a temporary workaround for the lack of `provider` field // in the light blocks serialized in the JSON fixtures. diff --git a/light-client/tests/light_client.rs b/light-client/tests/light_client.rs index 8c6d1146c..d618d2350 100644 --- a/light-client/tests/light_client.rs +++ b/light-client/tests/light_client.rs @@ -5,14 +5,14 @@ use tendermint_light_client::{ components::{ io::{AtHeight, Io}, scheduler, - verifier::{ProdVerifier, Verdict, Verifier}, + verifier::ProdVerifier, }, errors::{Error, ErrorKind}, light_client::{LightClient, Options}, state::State, store::{memory::MemoryStore, LightStore}, tests::{Trusted, *}, - types::{Height, LightBlock, Status, Time, TrustThreshold}, + types::{LightBlock, Status, TrustThreshold}, }; use tendermint_testgen::Tester; @@ -21,47 +21,6 @@ use tendermint_testgen::Tester; // https://github.com/informalsystems/conformance-tests const TEST_FILES_PATH: &str = "./tests/support/"; -fn verify_single( - trusted_state: Trusted, - input: LightBlock, - trust_threshold: TrustThreshold, - trusting_period: Duration, - clock_drift: Duration, - now: Time, -) -> Result { - let verifier = ProdVerifier::default(); - - let trusted_state = LightBlock::new( - trusted_state.signed_header, - trusted_state.next_validators.clone(), - trusted_state.next_validators, - default_peer_id(), - ); - - let options = Options { - trust_threshold, - trusting_period, - clock_drift, - }; - - let result = verifier.verify(&input, &trusted_state, &options, now); - - match result { - Verdict::Success => Ok(input), - error => Err(error), - } -} - -fn verify_bisection( - untrusted_height: Height, - light_client: &mut LightClient, - state: &mut State, -) -> Result, Error> { - light_client - .verify_to_target(untrusted_height, state) - .map(|_| state.get_trace(untrusted_height)) -} - struct BisectionTestResult { untrusted_light_block: LightBlock, new_states: Result, Error>, @@ -229,17 +188,17 @@ fn bisection_lower_test(tc: TestBisection) { #[test] fn run_single_step_tests() { - let mut tester = Tester::new(TEST_FILES_PATH); + let mut tester = Tester::new("single_step", TEST_FILES_PATH); tester.add_test("single-step test", single_step_test); tester.run_foreach_in_dir("single_step"); - tester.print_results(); + tester.finalize(); } #[test] fn run_bisection_tests() { - let mut tester = Tester::new(TEST_FILES_PATH); + let mut tester = Tester::new("bisection", TEST_FILES_PATH); tester.add_test("bisection test", bisection_test); tester.add_test("bisection lower test", bisection_lower_test); tester.run_foreach_in_dir("bisection/single_peer"); - tester.print_results(); + tester.finalize(); } diff --git a/light-client/tests/supervisor.rs b/light-client/tests/supervisor.rs index ce8098d2a..a5867ff3c 100644 --- a/light-client/tests/supervisor.rs +++ b/light-client/tests/supervisor.rs @@ -121,8 +121,8 @@ fn run_multipeer_test(tc: TestBisection) { #[test] fn run_multipeer_tests() { - let mut tester = Tester::new(TEST_FILES_PATH); + let mut tester = Tester::new("bisection_multi_peer", TEST_FILES_PATH); tester.add_test("multipeer test", run_multipeer_test); tester.run_foreach_in_dir("bisection/multi_peer"); - tester.print_results(); + tester.finalize(); } From f95a8c9a3795aed9ea85dddfccf75955a9df448a Mon Sep 17 00:00:00 2001 From: Andrey Kuprianov Date: Fri, 4 Sep 2020 11:18:31 +0200 Subject: [PATCH 06/10] fix merge typo --- testgen/src/tester.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/testgen/src/tester.rs b/testgen/src/tester.rs index 92131c906..909b1095a 100644 --- a/testgen/src/tester.rs +++ b/testgen/src/tester.rs @@ -190,7 +190,7 @@ pub struct Tester { impl TestResult { pub fn is_success(&self) -> bool { - matches!(self, TestResult::Success(_)) + matches!(self, TestResult::Success) } pub fn is_failure(&self) -> bool { matches!(self, TestResult::Failure { From 9d4531a45603e0f4f86a3b98a7725088ba85fde1 Mon Sep 17 00:00:00 2001 From: Andrey Kuprianov Date: Fri, 4 Sep 2020 11:58:33 +0200 Subject: [PATCH 07/10] remove ref to time: it's in another PR --- testgen/src/lib.rs | 2 -- 1 file changed, 2 deletions(-) diff --git a/testgen/src/lib.rs b/testgen/src/lib.rs index 8e6606a99..58c875e94 100644 --- a/testgen/src/lib.rs +++ b/testgen/src/lib.rs @@ -6,14 +6,12 @@ pub mod commit; pub mod consensus; pub mod generator; pub mod header; -pub mod time; pub mod validator; pub mod vote; pub use commit::Commit; pub use generator::Generator; pub use header::Header; -pub use time::Time; pub use validator::Validator; pub use vote::Vote; From 4df1e28be19ac158e828909ee4602211c702fc7d Mon Sep 17 00:00:00 2001 From: Andrey Kuprianov Date: Fri, 4 Sep 2020 12:03:14 +0200 Subject: [PATCH 08/10] fix clippy warning --- testgen/src/command.rs | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/testgen/src/command.rs b/testgen/src/command.rs index c6aca4576..b75339cf8 100644 --- a/testgen/src/command.rs +++ b/testgen/src/command.rs @@ -80,3 +80,9 @@ impl Command { } } } + +impl Default for Command { + fn default() -> Self { + Self::new() + } +} From f032a208f86f7a0b8dbbfd45536899b7f55a9e52 Mon Sep 17 00:00:00 2001 From: Andrey Kuprianov Date: Fri, 11 Sep 2020 14:17:30 +0200 Subject: [PATCH 09/10] fix merging typo --- light-client/tests/model_based.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/light-client/tests/model_based.rs b/light-client/tests/model_based.rs index 026e1a996..ec6e626ce 100644 --- a/light-client/tests/model_based.rs +++ b/light-client/tests/model_based.rs @@ -140,8 +140,8 @@ fn model_based_test( assert!(run_jsonatr_transform(env.current_dir(), transform).is_ok()); output_env.copy_file_from_env(env, "test.json"); - let tc = env - .parse_file_as::("test.json") + let tc: SingleStepTestCase = env + .parse_file("test.json") .unwrap(); println!(" > running auto-generated test..."); single_step_test(tc, env, root_env, output_env); From 6af3bd0b89d0ef8150ac4ab9dcf48a1d6e32d026 Mon Sep 17 00:00:00 2001 From: Andrey Kuprianov Date: Fri, 11 Sep 2020 14:23:18 +0200 Subject: [PATCH 10/10] cargo fmt --- light-client/tests/model_based.rs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/light-client/tests/model_based.rs b/light-client/tests/model_based.rs index ec6e626ce..6bf80ed4f 100644 --- a/light-client/tests/model_based.rs +++ b/light-client/tests/model_based.rs @@ -140,9 +140,7 @@ fn model_based_test( assert!(run_jsonatr_transform(env.current_dir(), transform).is_ok()); output_env.copy_file_from_env(env, "test.json"); - let tc: SingleStepTestCase = env - .parse_file("test.json") - .unwrap(); + let tc: SingleStepTestCase = env.parse_file("test.json").unwrap(); println!(" > running auto-generated test..."); single_step_test(tc, env, root_env, output_env); output_env.copy_file_from_env(env, "counterexample.tla");