From 4d027b6ecb00c80aaa82b3f4fb77f0e0bb7bb550 Mon Sep 17 00:00:00 2001 From: Tobias Eidelpes Date: Fri, 9 Jul 2021 16:01:21 +0200 Subject: [PATCH] Final --- abstract-semantics.txt | 277 ++++++++++++++++++++++++++++++++++++++ alice.txt | 14 ++ bob.txt | 14 ++ call-contract.txt | 15 +++ call-tests.txt | 120 +++++++++++++++++ call1.txt | 33 +++++ call2.txt | 29 ++++ call3.txt | 13 ++ call4.txt | 22 +++ call5.txt | 28 ++++ counter-example1.txt | 23 ++++ counter-example3.txt | 20 +++ counter-example4.txt | 11 ++ local-contract.txt | 54 ++++++++ local-tests.txt | 289 ++++++++++++++++++++++++++++++++++++++++ queries.txt | 7 + report/report.pdf | Bin 0 -> 70736 bytes report/report.tex | 63 ++++++--- test-infrastructure.txt | 90 +++++++++++++ 19 files changed, 1106 insertions(+), 16 deletions(-) create mode 100644 abstract-semantics.txt create mode 100644 alice.txt create mode 100644 bob.txt create mode 100644 call-contract.txt create mode 100644 call-tests.txt create mode 100644 call1.txt create mode 100644 call2.txt create mode 100644 call3.txt create mode 100644 call4.txt create mode 100644 call5.txt create mode 100644 counter-example1.txt create mode 100644 counter-example3.txt create mode 100644 counter-example4.txt create mode 100644 local-contract.txt create mode 100644 local-tests.txt create mode 100644 queries.txt create mode 100644 report/report.pdf create mode 100644 test-infrastructure.txt diff --git a/abstract-semantics.txt b/abstract-semantics.txt new file mode 100644 index 0000000..ae4b6a5 --- /dev/null +++ b/abstract-semantics.txt @@ -0,0 +1,277 @@ +/* ============ Selector Functions ============ */ + +/* === General Infrastructure === */ +sel pcs: unit -> [int]; // gives all pcs of the contract +sel pcsForOpcode: int -> [int]; // gives all pcs for a certain opcode +sel argumentForPc: int -> [int]; // gives the argument for the opcode at pc (can only be invoked pcs containing a PUSH, JUMP or JUMPI) + +/* ============ Opcodes ============= */ + +const ADD := 0; +const AND := 1; +const LE := 2; +const PUSH := 3; +const POP := 4; +const MLOAD := 5; +const MSTORE := 6; +const SLOAD := 7; +const SSTORE := 8; +const TIMESTAMP := 9; +const BALANCE := 10; +const INPUT := 11; +const ADDRESS := 12; +const GAS := 13; +const JUMP := 14; +const JUMPI := 15; +const RETURN := 16; +const STOP := 17; +const FAIL := 18; +const CALL := 19; + +/* ============ Abstract Domain and abstract operations ============ */ + +eqtype AbsDom := @T | @V; /* Abstract Domain: @T represents the top element, V(v) concrete elements of value v */ + +// operation that checks whether a value is concrete (not top) +op isConcrete(a:AbsDom): bool := match a with | @T => false | _ => true; + +//operation that extracts the concrete value from an abstract value (in case of @T it defaults to 0) +op extractConcrete(a:AbsDom): int := match a with | @V(x) => x | _ => 0; + +op isAbstract(a:AbsDom): bool := ~ isConcrete(a); + +op absAdd(a:AbsDom, b:AbsDom): AbsDom := + match (a, b) with + | (@V(n), @V(m)) => @V(n+m) + | _ => @T; + +op absAnd(a:AbsDom, b:AbsDom): AbsDom := + match (a, b) with + | (@V(n), @V(m)) => (n > 0 && m > 0) ? (@V(1)) : (@V(0)) + | _ => @T; + +op absLe(a:AbsDom, b:AbsDom): AbsDom := + match (a, b) with + | (@V(n), @V(m)) => (n <= m) ? (@V(1)) : (@V(0)) + | _ => @T; + +/* ============ Predicates ============ */ + +pred ExState{int}: int * array * array * AbsDom * array * bool; // Execution State: , size, stack, memory, input, storage, cl (call level) +pred Exc{}: bool; // Exceptional Halting: cl, predicate signalizing exceptional halting +pred Halt{}: array * AbsDom * bool; // Successful Halting: storage, return value, cl + + +/* ============ Abstract Rules ============ */ + +rule exception := + for (!pc: int) in pcs() + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl) + => Exc(?cl); + +rule add := + for (!pc: int) in pcsForOpcode(ADD) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool, ?x: AbsDom, ?y: AbsDom] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size > 1, + ?x = select ?sa (?size - 1), + ?y = select ?sa (?size - 2) + => ExState{!pc+1}(?size - 1, store ?sa (?size - 2) (absAdd(?x, ?y)), ?mem, ?in, ?stor, ?cl); + +rule and := + for (!pc: int) in pcsForOpcode(AND) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool, ?x: AbsDom, ?y: AbsDom] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size > 1, + ?x = select ?sa (?size - 1), + ?y = select ?sa (?size - 2) + => ExState{!pc+1}(?size - 1, store ?sa (?size - 2) (absAnd(?x, ?y)), ?mem, ?in, ?stor, ?cl); + +rule le := + for (!pc: int) in pcsForOpcode(LE) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool, ?x: AbsDom, ?y: AbsDom] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size > 1, + ?x = select ?sa (?size - 1), + ?y = select ?sa (?size - 2) + => ExState{!pc+1}(?size - 1, store ?sa (?size - 2) (absLe(?x, ?y)), ?mem, ?in, ?stor, ?cl); + +rule push := + for (!pc: int) in pcsForOpcode(PUSH), (!v: int) in argumentForPc(!pc) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl) + => ExState{!pc+1}(?size + 1, store ?sa ?size @V(!v), ?mem, ?in, ?stor, ?cl); + +rule pop := + for (!pc: int) in pcsForOpcode(POP) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size >= 1 + => ExState{!pc+1}(?size - 1, ?sa, ?mem, ?in, ?stor, ?cl); + +rule mstore := + for (!pc: int) in pcsForOpcode(MSTORE) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool, ?p: AbsDom, ?v: AbsDom] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size >= 2, + ?p = select ?sa (?size - 1), + isConcrete(?p), + ?v = select ?sa (?size - 2) + => ExState{!pc+1}(?size - 2, ?sa, store ?mem extractConcrete(?p) ?v, ?in, ?stor, ?cl), + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool, ?p: AbsDom, ?v: AbsDom] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size >= 2, + ?p = select ?sa (?size - 1), + isAbstract(?p) + => ExState{!pc+1}(?size - 2, ?sa, [@T], ?in, ?stor, ?cl); + +rule mload := + for (!pc: int) in pcsForOpcode(MLOAD) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool, ?p: AbsDom, ?v: AbsDom] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size >= 1, + ?p = select ?sa (?size -1), + isConcrete(?p), + ?v = select ?mem (extractConcrete(?p)) + => ExState{!pc+1}(?size, store ?sa (?size - 1) ?v, ?mem, ?in, ?stor, ?cl), + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool, ?p: AbsDom, ?v: AbsDom] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size >= 1, + ?p = select ?sa (?size -1), + isAbstract(?p) + => ExState{!pc+1}(?size, store ?sa (?size - 1) @T, ?mem, ?in, ?stor, ?cl); + +rule sload := + for (!pc: int) in pcsForOpcode(SLOAD) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool, ?v: AbsDom, ?p: AbsDom] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size >= 1, + ?p = select ?sa (?size -1), + isConcrete(?p), + ?v = select ?stor extractConcrete(?p) + => ExState{!pc+1}(?size, store ?sa (?size - 1) ?v, ?mem, ?in, ?stor, ?cl), + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool, ?p: AbsDom] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size >= 1, + ?p = select ?sa (?size -1), + isAbstract(?p) + => ExState{!pc+1}(?size, store ?sa (?size - 1) @T, ?mem, ?in, ?stor, ?cl); + +rule sstore := + for (!pc: int) in pcsForOpcode(SSTORE) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool, ?p: AbsDom, ?v: AbsDom] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size >= 2, + ?p = select ?sa (?size -1), + isConcrete(?p), + ?v = select ?sa (?size -2) + => ExState{!pc+1}(?size - 2, ?sa, ?mem, ?in, store ?stor extractConcrete(?p) ?v, ?cl), + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool, ?p: AbsDom] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size >= 2, + ?p = select ?sa (?size -1), + isAbstract(?p) + => ExState{!pc+1}(?size - 2, ?sa, ?mem, ?in, [@T], ?cl); + +rule timestamp := + for (!pc: int) in pcsForOpcode(TIMESTAMP) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl) + => ExState{!pc+1}(?size + 1, store ?sa ?size @T, ?mem, ?in, ?stor, ?cl); + +rule balance := + for (!pc: int) in pcsForOpcode(BALANCE) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size >= 1 + => ExState{!pc+1}(?size, store ?sa (?size - 1) @T, ?mem, ?in, ?stor, ?cl); + +rule input := + for (!pc: int) in pcsForOpcode(INPUT) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl) + => ExState{!pc+1}(?size + 1, store ?sa ?size ?in, ?mem, ?in, ?stor, ?cl); + +rule address := + for (!pc: int) in pcsForOpcode(ADDRESS) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl) + => ExState{!pc+1}(?size + 1, store ?sa ?size @T, ?mem, ?in, ?stor, ?cl); + +rule gas := + for (!pc: int) in pcsForOpcode(GAS) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl) + => ExState{!pc+1}(?size + 1, store ?sa ?size @T, ?mem, ?in, ?stor, ?cl); + +rule jump := + for (!pc: int) in pcsForOpcode(JUMP), (!j: int) in argumentForPc(!pc) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl) + => ExState{!j}(?size, ?sa, ?mem, ?in, ?stor, ?cl); + +rule jumpi := + for (!pc: int) in pcsForOpcode(JUMPI), (!j: int) in argumentForPc(!pc) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool, ?p: AbsDom] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size >= 1, + ?p = select ?sa (?size - 1), + (isAbstract(?p) || extractConcrete(?p) != 0) + => ExState{!j}(?size-1, ?sa, ?mem, ?in, ?stor, ?cl), + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool, ?p: AbsDom] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size >= 1, + ?p = select ?sa (?size - 1), + (isAbstract(?p) || extractConcrete(?p) = 0) + => ExState{!pc+1}(?size-1, ?sa, ?mem, ?in, ?stor, ?cl); + +rule return := + for (!pc: int) in pcsForOpcode(RETURN) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool, ?p: AbsDom] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size >= 1, + ?p = select ?sa (?size -1) + => Halt{}(?stor, ?p, ?cl); + +rule stop := + for (!pc: int) in pcsForOpcode(STOP) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl) + => Halt{}(?stor, @V(0), ?cl); + +rule fail := + for (!pc: int) in pcsForOpcode(FAIL) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl) + => Exc(?cl); + +rule call1 := + for (!pc: int) in pcsForOpcode(CALL) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size > 3 + => ExState{0}(0, [@V(0)], [@V(0)], @T, ?stor, true); + +rule call2 := + for (!pc: int) in pcsForOpcode(CALL) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool, ?storInv:array, ?r: AbsDom] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size > 3, + Halt{}(?storInv, ?r, true) + => ExState{0}(0, [@V(0)], [@V(0)], @T, ?storInv, true); + +rule call3 := + for (!pc: int) in pcsForOpcode(CALL) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size > 3 + => ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, [@T], ?in, [@T], ?cl); + +/* ============ Initialization ============ */ + +rule initOp := + clause + true + => ExState{0}(0, [@V(0)], [@V(0)], @T, [@T], false); // execution starts at pc 0 in empty execution state + diff --git a/alice.txt b/alice.txt new file mode 100644 index 0000000..4a90b09 --- /dev/null +++ b/alice.txt @@ -0,0 +1,14 @@ +PUSH 4294967295; +SLOAD; +PUSH 1; +LE; +PUSH 64; +JUMPI 13; +PUSH 0; +PUSH 2; +INPUT; +CALL; +PUSH 1; +PUSH 4294967295; +SSTORE; +STOP; diff --git a/bob.txt b/bob.txt new file mode 100644 index 0000000..b980c8b --- /dev/null +++ b/bob.txt @@ -0,0 +1,14 @@ +PUSH 4294967295; +SLOAD; +PUSH 1; +LE; +JUMPI 13; +PUSH 64; +PUSH 0; +PUSH 2; +INPUT; +CALL; +PUSH 1; +PUSH 4294967295; +SSTORE; +STOP; diff --git a/call-contract.txt b/call-contract.txt new file mode 100644 index 0000000..f9658f0 --- /dev/null +++ b/call-contract.txt @@ -0,0 +1,15 @@ +// writes 10 to 3 in storage +/* 0 */ PUSH 10; +/* 1 */ PUSH 3; +/* 2 */ SSTORE; +// calls another contract +/* 3 */ PUSH 0; // oa +/* 4 */ PUSH 2; // id +/* 5 */ PUSH 3; // va +/* 6 */ PUSH 42; // to +/* 7 */ CALL; +// writes 20 to 3 in storage +/* 8 */ PUSH 20; +/* 9 */ PUSH 3; +/* 10 */ SSTORE; +/* 11 */ STOP; \ No newline at end of file diff --git a/call-tests.txt b/call-tests.txt new file mode 100644 index 0000000..993db19 --- /dev/null +++ b/call-tests.txt @@ -0,0 +1,120 @@ +/* Special tests for the Call rules. To be run with call-contract.txt */ + +// Check that the storage can have the right values before calling (at this point there is only one possible value at call level 0) +test storageSoundnesBeforeTest expect SAT + [?size: int, ?sa: array, ?mem: array,?in: AbsDom, ?stor: array, ?cl: bool] + ExState{7}(4, ?sa, ?mem, ?in, ?stor, false), + stackMoreAbstractThanForall{4}(?sa, store (store (store (store [@V(0)] 0 @V(0)) 1 @V(2)) 2 @V(3)) 3 @V(42)), + arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @V(0))), + arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(10))); + +test storagePrecisePossibleBeforeTest expect SAT + [?size: int, ?sa: array, ?mem: array,?in: AbsDom, ?stor: array, ?cl: bool] + ExState{7}(4, ?sa, ?mem, ?in, ?stor, false), + stackEqualForall{4}(?sa, store (store (store (store [@V(0)] 0 @V(0)) 1 @V(2)) 2 @V(3)) 3 @V(42)), + ?mem = [@V(0)], + (select ?stor 3) = @V(10); + +test storagePreciseUniqueBeforeTest expect UNSAT + [?size: int, ?sa: array, ?mem: array,?in: AbsDom, ?stor: array, ?cl: bool] + ExState{7}(?size, ?sa, ?mem, ?in, ?stor, false), + (?size != 4 || ?mem != [@V(0)] + || stackInequalExists{4}(?sa, store (store (store (store [@V(0)] 0 @V(0)) 1 @V(2)) 2 @V(3)) 3 @V(42)) + || (select ?stor 3) != @V(10)); + +//Check for the right storage when reentering (can be 10 or 20, but nothing else) +test storageSoundnessReenteringTest1 expect SAT + [?size: int, ?sa: array, ?mem: array,?in: AbsDom, ?stor: array, ?cl: bool] + ExState{0}(0, ?sa, ?mem, ?in, ?stor, true), + valueMoreAbstractThan(?in, @T), + arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @V(0))), + arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(10))); + +test storageSoundnessReenteringTest2 expect SAT + [?size: int, ?sa: array, ?mem: array,?in: AbsDom, ?stor: array, ?cl: bool] + ExState{0}(0, ?sa, ?mem, ?in, ?stor, true), + valueMoreAbstractThan(?in, @T), + arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @V(0))), + arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(20))); + +test storagePrecisePossibleReenteringTest1 expect SAT + [?size: int, ?sa: array, ?mem: array,?in: AbsDom, ?stor: array, ?cl: bool] + ExState{0}(0, ?sa, ?mem, ?in, ?stor, true), + ?mem = [@V(0)], + ?in = @T, + (select ?stor 3) = @V(10); + +test storagePrecisePossibleReenteringTest2 expect SAT + [?size: int, ?sa: array, ?mem: array,?in: AbsDom, ?stor: array, ?cl: bool] + ExState{0}(0, ?sa, ?mem, ?in, ?stor, true), + ?mem = [@V(0)], + ?in = @T, + (select ?stor 3) = @V(20); + +test storagePreciseUniqueReenteringTest expect UNSAT + [?size: int, ?sa: array, ?mem: array,?in: AbsDom, ?stor: array, ?cl: bool] + ExState{0}(?size, ?sa, ?mem, ?in, ?stor, true), + (?mem != [@V(0)] || ?in != @T || ?size != 0 || + (select ?stor 3) != @V(10) && (select ?stor 3) != @V(20)); + +// Check that the storage is sound after reentering (on both levels) +test storageSoundnessResumeTest1 expect SAT + [?size: int, ?sa: array, ?mem: array,?in: AbsDom, ?stor: array, ?cl: bool] + ExState{8}(1, ?sa, ?mem, ?in, ?stor, false), + stackMoreAbstractThanForall{1}(?sa, store [@V(0)] 0 @T), + arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @T)), + arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(10))); + +test storageSoundnessResumeTest2 expect SAT + [?size: int, ?sa: array, ?mem: array,?in: AbsDom, ?stor: array, ?cl: bool] + ExState{8}(1, ?sa, ?mem, ?in, ?stor, false), + stackMoreAbstractThanForall{1}(?sa, store [@V(0)] 0 @T), + arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @T)), + arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(20))); + +test storageSoundnessResumeTest3 expect SAT + [?size: int, ?sa: array, ?mem: array,?in: AbsDom, ?stor: array, ?cl: bool] + ExState{8}(1, ?sa, ?mem, ?in, ?stor, true), + stackMoreAbstractThanForall{1}(?sa, store [@V(0)] 0 @T), + arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @T)), + arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(10))); + +test storageSoundnessResumeTest4 expect SAT + [?size: int, ?sa: array, ?mem: array,?in: AbsDom, ?stor: array, ?cl: bool] + ExState{8}(1, ?sa, ?mem, ?in, ?stor, true), + stackMoreAbstractThanForall{1}(?sa, store [@V(0)] 0 @T), + arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @T)), + arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(20))); + +// Check that the storage is right when halting +test storageSoundnessHaltTest1 expect SAT + [?res: AbsDom, ?stor: array] + Halt(?stor, ?res, false), + valueMoreAbstractThan(?res, @V(0)), + arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(20))); + +test storageSoundnessHaltTest2 expect SAT + [?res: AbsDom, ?stor: array] + Halt(?stor, ?res, true), + valueMoreAbstractThan(?res, @V(0)), + arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(20))); + +test storagePrecisePossibleHaltTest1 expect SAT + [?res: AbsDom, ?stor: array] + Halt(?stor, ?res, false), + ?res = @V(0), + (select ?stor 3) = @V(20); + +test storagePrecisePossibleHaltTest2 expect SAT + [?res: AbsDom, ?stor: array] + Halt(?stor, ?res, true), + ?res = @V(0), + (select ?stor 3) = @V(20); + +test storagePreciseUniqueHaltTest expect UNSAT + [?res: AbsDom, ?stor: array, ?cl: bool] + Halt(?stor, ?res, ?cl), + (select ?stor 3) != @V(20) || (?res != @V(0)) ; + + + diff --git a/call1.txt b/call1.txt new file mode 100644 index 0000000..b9063cb --- /dev/null +++ b/call1.txt @@ -0,0 +1,33 @@ +rule rule1 := + for (!pc: int) in pcsForOpcode(CALL) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size > 3 + => ExState{0}(0, [@V(0)], [@V(0)], @T, ?stor, true); + +rule rule2 := + for (!pc: int) in pcsForOpcode(CALL) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool, ?storInv: array, ?r: AbsDom] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size > 3, + Halt{}(?storInv,?r,true) + => ExState{0}(0, [@V(0)], [@V(0)], @T, ?storInv, true); + +rule rule3 := + for (!pc: int) in pcsForOpcode(CALL) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size > 3, + isAbstract(select ?sa (?size - 4)) + => ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, [@T], ?in, [@T], ?cl); + +rule rule4 := + for (!pc: int) in pcsForOpcode(CALL) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool, ?p: AbsDom, ?storInv: array, ?r: AbsDom] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size > 3, + ?p = select ?sa (?size - 4), + isConcrete(?p), + extractConcrete(?p) >= 0, + Halt(?storInv, ?r, true) + => ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, store ?mem (extractConcrete (?p)) ?r, ?in, [@T], ?cl); diff --git a/call2.txt b/call2.txt new file mode 100644 index 0000000..f646356 --- /dev/null +++ b/call2.txt @@ -0,0 +1,29 @@ +rule rule1 := + for (!pc: int) in pcsForOpcode(CALL) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size > 3 + => ExState{0}(0, [@V(0)], [@V(0)], @T, ?stor, true); + +rule rule2 := + for (!pc: int) in pcsForOpcode(CALL) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool, ?storInv: array, ?r: AbsDom] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size > 3, + Halt{}(?storInv, ?r, true) + => ExState{0}(0, [@V(0)], [@V(0)], @T, ?storInv, true); + +rule rule3 := + for (!pc: int) in pcsForOpcode(CALL) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size > 3 + => ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, [@T], ?in, ?stor, ?cl); + +rule rule4 := + for (!pc: int) in pcsForOpcode(CALL) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool, ?storInv: array, ?r: AbsDom] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size > 3, + Halt(?storInv, ?r, true) + => ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, [@T], ?in, ?storInv, ?cl); diff --git a/call3.txt b/call3.txt new file mode 100644 index 0000000..a0c8ad7 --- /dev/null +++ b/call3.txt @@ -0,0 +1,13 @@ +rule rule1 := + for (!pc: int) in pcsForOpcode(CALL) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size > 3 + => ExState{0}(0, [@V(0)], [@V(0)], @T, ?stor, true); + +rule rule2 := + for (!pc: int) in pcsForOpcode(CALL) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size > 3 + => ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, [@T], ?in, [@T], ?cl); diff --git a/call4.txt b/call4.txt new file mode 100644 index 0000000..24f0c7e --- /dev/null +++ b/call4.txt @@ -0,0 +1,22 @@ +rule rule1 := + for (!pc: int) in pcsForOpcode(CALL) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool, ?v: AbsDom] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size > 3, + ?v = select ?sa (?size -3) + => ExState{0}(0, [@V(0)], [@V(0)], ?v, ?stor, true); + +rule rule2 := + for (!pc: int) in pcsForOpcode(CALL) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool, ?storInv: array, ?r: AbsDom] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size > 3, + Halt{}(?storInv, ?r, true) + => ExState{0}(0, [@V(0)], [@V(0)], @T, ?storInv, true); + +rule rule3 := + for (!pc: int) in pcsForOpcode(CALL) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size > 3 + => ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, [@T], ?in, [@T], ?cl); diff --git a/call5.txt b/call5.txt new file mode 100644 index 0000000..475f31a --- /dev/null +++ b/call5.txt @@ -0,0 +1,28 @@ +rule rule1 := + for (!pc: int) in pcsForOpcode(CALL) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size > 3 + => ExState{0}(0, [@V(0)], [@V(0)], @T, ?stor, true); + +rule rule2 := + for (!pc: int) in pcsForOpcode(CALL) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool, ?storInv: array, ?r: AbsDom] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size > 3, + Halt{}(?storInv, ?r, true) + => ExState{0}(0, [@V(0)], [@V(0)], @T, ?storInv, true); + +rule rule3 := + for (!pc: int) in pcsForOpcode(CALL) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size > 3 + => ExState{!pc+1}(?size-3, store ?sa (?size - 4) @V(1), [@T], ?in, [@T], ?cl); + +rule rule4 := + for (!pc: int) in pcsForOpcode(CALL) + clause [?size: int, ?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + ?size > 3 + => ExState{!pc+1}(?size-3, store ?sa (?size - 4) @V(0), ?mem, ?in, [@T], ?cl); diff --git a/counter-example1.txt b/counter-example1.txt new file mode 100644 index 0000000..fdc005c --- /dev/null +++ b/counter-example1.txt @@ -0,0 +1,23 @@ +PUSH 123; // address of sent +SLOAD; // get value of sent +PUSH 1; +LE; // check 1 <= sent (= !(sent < 1)) +JUMPI 22; +PUSH 1; +PUSH 123; +SSTORE; // sent = 1 +PUSH ~1337; // - oa +PUSH 0; // - id +PUSH 2; // - va +INPUT; // - to +CALL; // call 1 +PUSH ~1337; +MLOAD; +PUSH 123; +SSTORE; // sent = memory[oa] +PUSH ~1337; +PUSH 0; // - id +PUSH 2; // - va +INPUT; // - to +CALL; // call 2 +STOP; diff --git a/counter-example3.txt b/counter-example3.txt new file mode 100644 index 0000000..4c589f3 --- /dev/null +++ b/counter-example3.txt @@ -0,0 +1,20 @@ +INPUT; +JUMPI 16; +PUSH 2; +SLOAD; +PUSH 1; +LE; // 1 <= sent ( == !(sent < 1)) +JUMPI 19; +PUSH 1; +PUSH 2; +SSTORE; // sent := 1 +PUSH 1; +PUSH 2; +PUSH 2; +PUSH 4; +CALL; +STOP; +PUSH 0; +PUSH 2; +SSTORE; // sent := 0 +STOP; diff --git a/counter-example4.txt b/counter-example4.txt new file mode 100644 index 0000000..a80a533 --- /dev/null +++ b/counter-example4.txt @@ -0,0 +1,11 @@ +PUSH 0; +INPUT; +LE; // x <= 0 +JUMPI 10; +PUSH 123; // - oa +PUSH 0; // - id, important +PUSH 2; // - va +PUSH 1337; // - to, attacker +CALL; +STOP; +FAIL; diff --git a/local-contract.txt b/local-contract.txt new file mode 100644 index 0000000..06d3f1a --- /dev/null +++ b/local-contract.txt @@ -0,0 +1,54 @@ +/* 0 */ PUSH 1; // [1] +/* 1 */ PUSH ~2; // [~2, 1] +/* 2 */ ADD; // [~1] +/* 3 */ PUSH 1; // [1, ~1] +/* 4 */ AND; // [0] +/* 5 */ PUSH 2; // [2, 0] +/* 6 */ LE; // [0] +/* 7 */ PUSH ~1; // [~1, 0] +/* 8 */ LE; // [1] +/* 9 */ PUSH 336633572; // [336633572, 1] +/* 10 */ AND; // [1] +/* 11 */ POP; // [] +/* 12 */ PUSH 246435; // [246435] +/* 13 */ MLOAD; // [0] +/* 14 */ PUSH 2; // [2, 0] +/* 15 */ ADD; // [2] +/* 16 */ PUSH 1; // [1, 2] +/* 17 */ MSTORE; // [] [[1 -> 2]] +/* 18 */ PUSH 1; // [1] +/* 19 */ MLOAD; // [2] +/* 20 */ TIMESTAMP; // [T, 2] +/* 21 */ MLOAD; // [T, 2] +/* 22 */ MSTORE; // [] [[_ -> T]] +/* 23 */ PUSH ~42; // [~42] +/* 24 */ SLOAD; // [T] +/* 25 */ SLOAD; // [T] +/* 26 */ POP; // [] +/* 27 */ PUSH ~1337; // [~1337] +/* 28 */ PUSH ~67; // [~67, ~1337] +/* 29 */ SSTORE; // [] ((~67 -> ~1337)) +/* 30 */ PUSH ~67; // [~67] +/* 31 */ SLOAD; // [~1337] +/* 32 */ BALANCE; // [T] +/* 33 */ SLOAD; // [T] +/* 34 */ INPUT; // [T, T] +/* 35 */ SSTORE; // [] ((_ -> T)) +/* 36 */ ADDRESS; // [T] +/* 37 */ GAS; // [T, T] +/* 38 */ JUMP 40; // [T, T] +/* 39 */ RETURN; // UNREACHABLE (over-jumped) +/* 40 */ JUMPI 43; // [T] +/* 41 */ BALANCE; // [T] +/* 42 */ RETURN; // [T] +/* 43 */ JUMPI 45; // [] +/* 44 */ STOP; // [] +/* 45 */ GAS; // [T] +/* 46 */ JUMPI 48; // [] +/* 47 */ FAIL; // +/* 48 */ PUSH 1; // [1] +/* 49 */ JUMPI 51; // [] +/* 50 */ FAIL; // UNREACHABLE (over-jumped) +/* 51 */ STOP; // [] +// CALL tests are missing + diff --git a/local-tests.txt b/local-tests.txt new file mode 100644 index 0000000..e9cbe2b --- /dev/null +++ b/local-tests.txt @@ -0,0 +1,289 @@ +/* Tests for the local instructions of tinyEVM. To be run on local-contract.txt */ + +op pcToConfig(pc: int): Config := + match pc with + | 0 => @C( 0, + [@V(0)], + UPDATELISTDUMMY, + UPDATELISTDUMMY) + | 1 => @C( 1, + store [@V(0)] 0 @V(1), + UPDATELISTDUMMY, + UPDATELISTDUMMY) + | 2 => @C( 2, + store (store [@V(0)] 0 @V(1)) 1 @V(~2), + UPDATELISTDUMMY, + UPDATELISTDUMMY) + | 3 => @C( 1, + store [@V(0)] 0 @V(~1), + UPDATELISTDUMMY, + UPDATELISTDUMMY) + | 4 => @C( 2, + store (store [@V(0)] 0 @V(~1)) 1 @V(1), + UPDATELISTDUMMY, + UPDATELISTDUMMY) + | 5 => @C( 1, + store [@V(0)] 0 @V(0), + UPDATELISTDUMMY, + UPDATELISTDUMMY) + | 6 => @C( 2, + store (store [@V(0)] 0 @V(0)) 1 @V(2), + UPDATELISTDUMMY, + UPDATELISTDUMMY) + | 7 => @C( 1, + store [@V(0)] 0 @V(0), + UPDATELISTDUMMY, + UPDATELISTDUMMY) + | 8 => @C( 2, + store (store [@V(0)] 0 @V(0)) 1 @V(~1), + UPDATELISTDUMMY, + UPDATELISTDUMMY) + | 9 => @C( 1, + store [@V(0)] 0 @V(1), + UPDATELISTDUMMY, + UPDATELISTDUMMY) + | 10 => @C( 2, + store (store [@V(0)] 0 @V(1)) 1 @V(336633572), + UPDATELISTDUMMY, + UPDATELISTDUMMY) + | 11 => @C( 1, + store [@V(0)] 0 @V(1), + UPDATELISTDUMMY, + UPDATELISTDUMMY) + | 12 => @C( 0, + [@V(0)], + UPDATELISTDUMMY, + UPDATELISTDUMMY) + | 13 => @C( 1, + store [@V(0)] 0 @V(246435), + UPDATELISTDUMMY, + UPDATELISTDUMMY) + | 14 => @C( 1, + [@V(0)], + UPDATELISTDUMMY, + UPDATELISTDUMMY) + | 15 => @C( 2, + store [@V(0)] 1 @V(2), + UPDATELISTDUMMY, + UPDATELISTDUMMY) + | 16 => @C( 1, + store [@V(0)] 0 @V(2), + UPDATELISTDUMMY, + UPDATELISTDUMMY) + | 17 => @C( 2, + store (store [@V(0)] 0 @V(2)) 1 @V(1), + UPDATELISTDUMMY, + UPDATELISTDUMMY) + | 18 => @C( 0, + [@V(0)], + addUpdate(UPDATELISTDUMMY, @UP(1, @V(2))), + UPDATELISTDUMMY) + | 19 => @C( 1, + store [@V(0)] 0 @V(1), + addUpdate(UPDATELISTDUMMY, @UP(1, @V(2))), + UPDATELISTDUMMY) + | 20 => @C( 1, + store [@V(0)] 0 @V(2), + addUpdate(UPDATELISTDUMMY, @UP(1, @V(2))), + UPDATELISTDUMMY) + | 21 => @C( 2, + store (store [@V(0)] 0 @V(2)) 1 @T, + addUpdate(UPDATELISTDUMMY, @UP(1, @V(2))), + UPDATELISTDUMMY) + | 22 => @C( 2, + store (store [@V(0)] 0 @V(2)) 1 @T, + addUpdate(UPDATELISTDUMMY, @UP(1, @V(2))), + UPDATELISTDUMMY) + | 23 => @C( 0, + [@V(0)], + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + UPDATELISTDUMMY) + | 24 => @C( 1, + store [@V(0)] 0 @V(~42), + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + UPDATELISTDUMMY) + | 25 => @C( 1, + store [@V(0)] 0 @T, + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + UPDATELISTDUMMY) + | 26 => @C( 1, + store [@V(0)] 0 @T, + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + UPDATELISTDUMMY) + | 27 => @C( 0, + [@V(0)], + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + UPDATELISTDUMMY) + | 28 => @C( 1, + store [@V(0)] 0 @V(~1337), + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + UPDATELISTDUMMY) + | 29 => @C( 2, + store (store [@V(0)] 0 @V(~1337)) 1 @V(~67), + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + UPDATELISTDUMMY) + | 30 => @C( 0, + [@V(0)], + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + addUpdate(UPDATELISTDUMMY, @UP(~67, @V(~1337)))) + | 31 => @C( 1, + store [@V(0)] 0 @V(~67), + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + addUpdate(UPDATELISTDUMMY, @UP(~67, @V(~1337)))) + | 32 => @C( 1, + store [@V(0)] 0 @V(~1337), + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + addUpdate(UPDATELISTDUMMY, @UP(~67, @V(~1337)))) + | 33 => @C( 1, + store [@V(0)] 0 @T, + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + addUpdate(UPDATELISTDUMMY, @UP(~67, @V(~1337)))) + | 34 => @C( 1, + store [@V(0)] 0 @T, + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + addUpdate(UPDATELISTDUMMY, @UP(~67, @V(~1337)))) + | 35 => @C( 2, + store (store [@V(0)] 0 @T) 1 @T, + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + addUpdate(UPDATELISTDUMMY, @UP(~67, @V(~1337)))) + | 36 => @C( 0, + [@V(0)], + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + addUpdate(UPDATELISTDUMMY, @UP(~67, @T))) + | 37 => @C( 1, + store [@V(0)] 0 @T, + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + addUpdate(UPDATELISTDUMMY, @UP(~67, @T))) + | 38 => @C( 2, + store (store [@V(0)] 0 @T) 1 @T, + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + addUpdate(UPDATELISTDUMMY, @UP(~67, @T))) + | 40 => @C( 2, + store (store [@V(0)] 0 @T) 1 @T, + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + addUpdate(UPDATELISTDUMMY, @UP(~67, @T))) + | 41 => @C( 1, + store [@V(0)] 0 @T, + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + addUpdate(UPDATELISTDUMMY, @UP(~67, @T))) + | 42 => @C( 1, + store [@V(0)] 0 @T, + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + addUpdate(UPDATELISTDUMMY, @UP(~67, @T))) + | 43 => @C( 1, + store [@V(0)] 0 @T, + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + addUpdate(UPDATELISTDUMMY, @UP(~67, @T))) + | 44 => @C( 0, + [@V(0)], + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + addUpdate(UPDATELISTDUMMY, @UP(~67, @T))) + | 45 => @C( 0, + [@V(0)], + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + addUpdate(UPDATELISTDUMMY, @UP(~67, @T))) + | 46 => @C( 1, + store [@V(0)] 0 @T, + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + addUpdate(UPDATELISTDUMMY, @UP(~67, @T))) + | 47 => @C( 0, + [@V(0)], + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + addUpdate(UPDATELISTDUMMY, @UP(~67, @T))) + | 48 => @C( 0, + [@V(0)], + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + addUpdate(UPDATELISTDUMMY, @UP(~67, @T))) + | 49 => @C( 1, + store [@V(0)] 0 @V(1), + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + addUpdate(UPDATELISTDUMMY, @UP(~67, @T))) + | 51 => @C( 0, + [@V(0)], + addUpdate(UPDATELISTDUMMY, @UP(1, @T)), + addUpdate(UPDATELISTDUMMY, @UP(~67, @T))) + | _ => @C( 0, + [@V(0)], + UPDATELISTDUMMY, + UPDATELISTDUMMY); + +const INTERVALS := 3; + +test pcToStackTest expect SAT [?size: int, ?sa: array, ?mem: array,?in: AbsDom, ?stor: array, ?cl: bool] + ExState{1}(?size, ?sa, ?mem, ?in, ?stor, ?cl), + (@V(1)) = (select (getStackArray(pcToConfig(1))) 0); + + +test soundnessTest expect SAT + for (!i: int) in interval(0, INTERVALS), (!pc: int) in interval((!i = 0)? (0): ((!i = 1)?(40):(51)), (!i = 0)? (39): ((!i = 1)?(50):(52))) // ugly way to only invoke the rule on certain intervals + [?size: int, ?sa: array, ?mem: array,?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(getStackSize(pcToConfig(!pc)), ?sa, ?mem, @T, ?stor, false), + stackMoreAbstractThanForall{getStackSize(pcToConfig(!pc))}(?sa, getStackArray(pcToConfig(!pc))), + arrayMoreAbstractThan{getUpdateSize(getMemUpdateList(pcToConfig(!pc)))}(?mem, getUpdates(getMemUpdateList(pcToConfig(!pc)))), + arrayMoreAbstractThan{getUpdateSize(getStorUpdateList(pcToConfig(!pc)))}(?stor, getUpdates(getStorUpdateList(pcToConfig(!pc)))) + ; + +test precisionPossibleTest expect SAT + for (!i: int) in interval(0, INTERVALS), (!pc: int) in interval((!i = 0)? (0): ((!i = 1)?(40):(51)), (!i = 0)? (39): ((!i = 1)?(50):(52))) + [?size: int, ?sa: array, ?mem: array,?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(getStackSize(pcToConfig(!pc)), ?sa, ?mem, @T, ?stor, false), + stackEqualForall{getStackSize(pcToConfig(!pc))}(?sa, getStackArray(pcToConfig(!pc))), + arrayEqual{getUpdateSize(getMemUpdateList(pcToConfig(!pc)))}(?mem, getUpdates(getMemUpdateList(pcToConfig(!pc)))), + arrayEqual{getUpdateSize(getStorUpdateList(pcToConfig(!pc)))}(?stor, getUpdates(getStorUpdateList(pcToConfig(!pc)))) + ; + +test precisionUniqueTest expect UNSAT + for (!i: int) in interval(0, INTERVALS), (!pc: int) in interval((!i = 0)? (0): ((!i = 1)?(40):(51)), (!i = 0)? (39): ((!i = 1)?(50):(52))) + [?size: int, ?sa: array, ?mem: array,?in: AbsDom, ?stor: array, ?cl: bool] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, false), + (?size != getStackSize(pcToConfig(!pc))) + || (stackInequalExists{getStackSize(pcToConfig(!pc))}(?sa, getStackArray(pcToConfig(!pc)))) + || (arrayInequalExists{getUpdateSize(getMemUpdateList(pcToConfig(!pc)))}(?mem, getUpdates(getMemUpdateList(pcToConfig(!pc))))) + || (?in != @T) + || (arrayInequalExists{getUpdateSize(getStorUpdateList(pcToConfig(!pc)))}(?stor, getUpdates(getStorUpdateList(pcToConfig(!pc))))) + ; + + +/* Additional Tests concerning reachability, halting, etc. */ + +// pcs 39 and 50 should be unreachable because they are over-jumped +test unreachable39Test expect UNSAT + [?size: int, ?sa: array, ?mem: array,?in: AbsDom, ?stor: array, ?cl: bool] + ExState{39}(?size, ?sa, ?mem, ?in, ?stor, ?cl); + +test unreachable50Test expect UNSAT + [?size: int, ?sa: array, ?mem: array,?in: AbsDom, ?stor: array, ?cl: bool] + ExState{50}(?size, ?sa, ?mem, ?in, ?stor, ?cl); + +// Tests for correct halting +test haltSoundnessTest expect SAT + [?size: int, ?sa: array, ?mem: array,?in: AbsDom, ?stor: array, ?cl: bool, ?res: AbsDom] + Halt(?stor, ?res, false), + valueMoreAbstractThan(?res, @V(0)); + +test haltPrecisePossibleTest expect SAT + [?size: int, ?sa: array, ?mem: array,?in: AbsDom, ?stor: array, ?cl: bool, ?res: AbsDom] + Halt(?stor, @V(0), false); + +// the only possible return results are 0 and T (due to stop and RETURN) +test haltPreciionUniquenessTest expect UNSAT + [?size: int, ?sa: array, ?mem: array,?in: AbsDom, ?stor: array, ?cl: bool, ?res: AbsDom] + Halt(?stor, ?res, false), + (?res != @V(0) && ?res != @T); + +// Reaching an exceptional state should be possible +test exceptionPossibleTest expect SAT + Exc(false); + +test noCallTest2 expect UNSAT + Exc(true); + + +/* +query testQuery [?size: int, ?sa: array, ?mem: array,?in: AbsDom, ?stor: array, ?cl: bool, ?res: AbsDom, ?p: AbsDom] + ExState{13}(?size, ?sa, ?mem, ?in, ?stor, ?cl), ?size > 0, + ?p = select ?sa (?size -1), + ?res = (isConcrete(?p))? (select ?mem (extractConcrete(?p))):(@T), + ?res = @V(0); */ + + diff --git a/queries.txt b/queries.txt new file mode 100644 index 0000000..e47f784 --- /dev/null +++ b/queries.txt @@ -0,0 +1,7 @@ +/* ============ Reentrancy query ============ */ + +query reentrancyCall for (!pc:int) in pcsForOpcode(CALL) + [?sa: array, ?mem: array, ?in: AbsDom, ?stor: array, ?size:int] + ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, true); + + diff --git a/report/report.pdf b/report/report.pdf new file mode 100644 index 0000000000000000000000000000000000000000..7dbc7e07db5e986e20dd33da700caf51feb8143a GIT binary patch literal 70736 zcma&MLzE~?v~*dvZQHhO+qP}nwr!iYY}>Z&s{d=e(HnHa2 zwl^__;^TvIc5yN_w1x86?A4G?US>n+yQ{xnP#&T1`W%3*AO!`5ti+`P-`{_*ScSs# zZnQD0{QhWJZZhZbAS|p{#v^Ihs`c~d{kn(}Mfuer;Z)?2LYBlhQS|KadJ7ce=J3K) zBzmOb@){K`!64NkX{ayGuI8`f%Z--M#3QXFsg&p^4Hnas(?|kAlxJ7(=Q;Bn#+X30 zXxtd07EwYhZ8&9$X6ruJ{q{+n>bQXu?bV7_8L4;GZ*4GrnB|f}y4!+_w{ziiDbt6< z^B0s_xOR9dW6oEHjE`o@=_!xe-FBG7yk5T?Iwhq@&ZQ=Hl4=^xyngXmYV`(k_eAQa z`_$vc^?>?%OM$cv0%0I0&7r&?sp(81L8sD^7Gt6$6RdV6I_!7ZD5e8S?|0370~e$|S*%Jm_p4H-t6p?_1Ngtbx-MSvPLTazy3d*zBVo zeePNaFVYkocrJt49QT>%6-?aQ?0b|uu*7?-)n=|hCo2R(jkV@sfUQftRTEf=-)BaD zm|x!1>Uk=~O)#(LmG0P37mbJc@!*VT>DYWNm{Xx>iz~;KO9%Qos9Oc!c^0+bJXLyS zbl9lEz076a+PJ{QD^l}nj14vD^a+YL27NhlZ`Z3g0+&iC4VbqV4~kFpu)AgK57@Sh zH9U_3+ng72(gis@G4MXZ(FcRhO{v^6q#7D+6K=NdS=%8m=|ZnP=dq_Wbhf-~Xw-7?H;G9}3UaGm_<5J{&D{9h6pFfTQ zRI-=cieZ4TRTvbiq!ETf4EPP4@^}F1@b(#V1rRrot`!!PEV(#_*Po^n_En@0tRhO0 z-xY5UzHX|p_L*Us?+Rl&=Eli1sOtlFxqE@D%pmNH*E!RJ3G#{U1h|A#hS!|0rU_31 zwaM~yA+69k-1erH1Yw(+ zqDz4ng*U_IXZ4}?!IW%@mT}fv&ZTqHHoos zd%ese6=%3lpMKZ04ECH~f^8#Ou3X9oTe6J)B-ZiR;(=E|KL2A>DGcc3m|5Y`XLvG5 zX$asp%(!o_D(YM@+^&EU|F|{*L%UPyI5}XUn{o_+RK2zei|wH^x5-c+%z(r^neAR` zKn4O_-u;CTi9{^2>kEp9)GI6Dkvyp+vSfQnF_+it)$-bg?cv1k>?+JVEzqPAc#@60 zaz1NtFI3P(R|rdI=!kKmDGV{&XmV?g6F=JoC0XH>^F?rChZyqV9cnk%nEu!K9X%lX zbsdszO{wzT_VC_g!>gBZvUUOcTff)wF@Qci*Dj>nNB9RWUzvYSDHu3rPI}M6rhAS}i`3A^V|y-t;K^aZO;mps4bX>NgZAYIvIjJh$AEFV zXhoJEck5WO-mdG&9n>*$6p&*$m_Z4qG_iOG#Xl-|XIiXmpuWAcA_ngCo_QdiJpW?o zZ%Cow6A{hu*OA|D%i$n@L^3=o2_cpS*J#R~vV=+JMj>rc{#7`7S5@(4$%SP|W6rFN zeht;1n>@t{KvAA>|2!P7j0gtCH})^*4<?s;D5eg8y&I)vC(IFEJqWzNsIFQ6n02yYVG(004m?Az659zZxi|i%De}b$8SB z=V8V#?SzUR22imcJv8$^?RtD$HG93PwT7njFpHsP>lUJd7h7uES!vp|jgWeG+o5Lv zn2fn)M`wfN zKoNtgtHQo&=+yAl>-}Up({@;N6){Gsca@c}dxx7#kKY_0<=OaS?I^RL0)r7WV1GNW zS+6jiJxzyfx7c*2O~(fMIBwLo6Kb=2pEY~3bK^TypWEU;MbhPvp~f)-RVXbq-$is*b7F@(W$UJ{w(=SqU+PMffDxq`8?FtBgq`P@IPre&t5R9}}yeXTqvYtru zE}N?bs3DwxGmGaP>K^k@OWjvm{S&4Cu=i5!`33Jqd7cILQY{kdr7FxAzv$;z2vWE@ zcso84f_=q3%Qpd_fHWatT$)$vmXfMayD$5=(Gq|zPD`!_Va=Mr3p=tDq0Bptb9plx zh-UkC`SAUW%4O%5?IawM1s~TCYQ=e49|)^-2;(dHRTcPf-k2z=5rsvUQf9I8Z1e+c z|J{N7-$rC&{9i_7Bw%7-W%-}*$wa`&%*?^|KiB`#>HkOqMiw?^rvIO@H1-8l0cU#= zG)l;Uyo0%;+uOn29Spgv5MTh8EEl3QW^Gc>iuc@;Y$A z+$Wcx4Zv#u@9)>lz3bpK?zJti|I%Nd5gIKmB&n!um_O;?8YS83KH$CC;UNG+qjMwR z`Z~uu0FO=$z~0|XF%Za~Hu%+@hNd?(IKUqNN#E-QKWX<5H*m`z9R%*azcVFgj~pF@ zz?b(ttVXBCj2{2`FMs^k9^v0#*>^q7Uw!beKXsB*YwORJ{1^Pe-xz!g@Rrx_lt-?P zdiolzf{Vuv=+~e03fNC`ml0gs>E9ap6_C#ksG_&@)?XXqH4W%1KxTD-?sUyBX1f1% zmOpJ4?K)n`;Xcgol_elUV`I}V{@#^a=0*=6{%k$-M?3U$7tfz}Nl9;J@Q1$k=iR+-~pnq?1vx?<3D2coTz`%9{SA{-(vNSm;DRY zIivoFd)7Gj?1!KY8NXunshL0Mj=i7LI5zs)@Ay;txh9N%z@F-k9|)1e*b+R_|;B7w12U#KD@-Xw}WbSe780ISpS%F{#pCg zPCmGj;{KlFY*okct2FgqI{Y_G>^shX#|{mhntUGL){A#{Wal70U`^WfzbByFzltyF zUE=xot@-BmR(hR!1?2unzVdMyoL#+E4j*@ubZ&idc(bfTB+;oMf9%AI1%JGa?Qy82vm8W^{Gu zj7;SF5+;3(1fG8|XB78q+XwKR+3#Al>IQDNL**mu!^L4-LmAm*Z)n{TXu|(nzI8CD z(a|(51Z`U8DYoOleC9M|S3hJMTwI)-QSQPW3p^+{UtKh6GB43m*YDxAU#{VJVsfS>le?6n++08i3fVS-N)_O(DtmayTWKP z(=UU|j2CM^PP%Ri#ZT~wDAre=`Yy@wUd$sijUr-FsfEBeLzeGVP=NzKCJsDVKxFZ0 z=%ejaB0k73%cRZth<+IAk(lG(GSg^txgb*+o&G8!)HK;3ixLtzOsA-h=H=cOQD=GB zTo)+EVupG(IK^o)ssigdzLR_OIEEqP(fV~LEfBt(nI6>`M8h14^IYFrRd*eDg{w}R zy;r6-*ba?xO}FLlmeU5x+K`$(0Bcuc1}YbK@f78}<&npkW1SOf!C_RNUpG}x{F(V-)}*4k8aQWj zIAU#27nGu&MquenQv%p{A%qp=8G^hibESX3bi8PfX@b{|v@c$D)Fis-{K$Gc_eTcQ<8M>G;2Tpk!OVN;M}C2!mtXbe9H9kVet0C7;)n>>x3u3uQ&z{2{wVb z8A>4-`n_64hIfyRuW`QDfW6D3L5*X|%}YbiOWFob`qKN|PgNg{F=C?XS|lg{B@ng{ zvrKuH1XAvxtqf4a(}0?7QVt+h2Ft&X^dt-rzgYpdfLV+X(jsSg&in3}aV_Cf;`$qs zCCDZs*X!J`h*biHcs$SgN;9b+!eGYr2o!o~Iec0YLx426y~yA`Uv24P=Y(pc>>;(1 zJZDrTbyF{$wxpjV<6c!K$UkObIsLHc*hBfzQsA#N8TwO^cSDmr0-Gs3Ih=yu4T=0{ zWL{i{8>3hmV$iN64YF<>ou9pPMe&bYFU6a@EMc5tthS+g>o4Q++2LmNY2z<@)Go6| zFs)7eQMXI*$2#$B<@iI{g!Lwv{gC_?jQ1Hcjh?7fB6tt{f!dd|`Jek07a4EcA8pWp z8!Ik=6nYTjBu@v;X=t1@Orq;i^&fW$VVGIcqcT?#qS~S7F&D;WtU*7EA?FFg-C>-< z?VZx{H5D)v$LN58c3W%)mqS&Y7ICLulJn2xhHEIXmr&^C(+b>?ug@l7z1EgG+z_YmoxqW^ zpPuIvr)NdG>Bg^+fv61}5ir)w==}uYt`1R37~z!FR{q!b`xP@vZqnpG}D89 zn18ce+P#MaWe07!37-a0q&J&-{$YH(L}<$xnL>jzLGgJ`O}(6pgfebNBew{zFmp6T7zD4=e1b9Cs_2U7am;N+OZQDo6wP+;>K!d7j&-Y zRTUxz_4HLE6>fF6R6o(T^aRsQMbRz`k@*?_mCJ)wKS{_F2|f`8;gpN|kHC_^n-hHn z_p6I4gM^w6G{r69$tUeDLo|r1bHko@4^sQ&MFmX6D?fkiH>7VURhN?HDJjMBffF%S5b9ETC@!tn!2GxI6 z`Jh1KZ7o;+^dkMrdD{mKd9?HeQL#8MT^+n6%GTa?!;7#h`PF&Do8z(jGIUJD<@a^= z5)}%h3m%4NW&b^ZBG@!#zOq_!LX3_^3nNfE4>|V__t$;YKK&$Tw#rHGMIU6WaEO(3 zOD1$X7eWAB`U?|IKPh5>aE5@zoysAqo{X{YWIZL0;dm$aNwFfTgsO|!TCa>Ebo0yL zw3(fcK2ZEcg#&8ZF>T7mf*Lh&I~zcYl(TD=qpFN+LAo3H-*ttvx=Cx3*&GEdwl>ZI zT2?Gp=8@(xYu^PynMhanEclw$Fr7LW%@)^FHSX*uzN{Xp8PqI3l7k)VvBArS;p7e( z1fK9)kx0u>svR+E_*4hv)0*{`dYF4Yl9oNxkT zbTn+JoGOtpmE*qz!xqR;5G*o^LBC;1=Ii#-L~3@N#XeB1g!eC&i>c1WS6vigu|azy zb0;(lrwpd70^n63wGun-ZPZlO!zz-T6D4s~NbSqp?%>`71U#TE)>SSn`VH#Vdwx|a z&ic7wo}A(jcZEn$dTr5M|8f#7lkFaa+1)Pzhl6`zKGRGcGV3NNS2$Ymd6iKivfwg!NG&K(t4@=1FlT+_|WohA&cceOZ`|X0wen&zDx^RSXbnqoUb<$6fNSzzP&{EU%#t#T z_wtEE_VE}Z91PtpJe~>jZIqB)dV!{Bh{E_S6yXebd5Iy(p*qlx#4=A=8px}~+*WE7 z0L)bEU?gDVrI{PgNo(>#xGu*;jx?bl>^_VE7;qUz+2^5Rd!E#3P94%M4SV~-lF2iw@Nlip$S9&;tT*U8(YH#RoiN&&+^m@ZY6;VG}m@_ zX8nKsSle&rJd}CUOZvOdF?nHy%AD~vU#1uWfwzP9=CGE=a_NX4?sI|Hv>!xE8PwFf zg`C}6iyP4S2YV~`@W-2JdvDypZyxY{t`hCj7NQz0dXv4jQ@R%%R2a#jC@hwIk%mZ| zolGbOT^xgfsjsT#B!Hg;dp2AI^la-Li#c891^lX|9$-QexMg8AoUf~m$p)7MNiTtkV`hUCgF1WPb#A1S3{G2N7(;6_Fm?GK6-JDp__4tuH0NJCFu-tP(jET7FFQ!A%|0!t(EPBjnsV_4ho+za3O zemYDtQE0N!u_QDzX!)uV1@91bHtpXPy7Fb*C81`+LR=1(rzBQ`GMHPoVBwduLf>0z zz7r5I6g*eN%pn2&?8JD=jl77Vf%wZyGmcugtm0+pA$xr!b&U4&HG*mH^_PR&9^6R|geCcgy;0NamUv7DM*y z)01^9maOhHdT8TRM&^8`rp3GV!_n%0(%N#Z{1a3K9ozU!<;Qee#WX8?94&a@&Q)?u z8Hx;LM0pR`%s%RFY+G6Qe7L5O_;UR?%zE{!Z@Hg*Xx;{(EjKx7jQR}8jhqLt&nEDLr{96tBHe z)iTxzG&oUl__YlA`)DtBgIL>dX^YXF-VHL~x?bVAbiP7_)D)zc1qDc-OS6!wEZ8z? zLD@ChP^H-ue*olewekcqujDzzP3F*Fq|)VgRz0;RbB0H5H1@b;)b-t-vWp3Iol0kU z=iaQ`>t`$Ed+E1TUofAEjt`%9*$J6g?E8edcG{ZFb=uWh(pwTl+k~mqlF8~8L+UD) zL~9RkB>PpNMreN@lSt$72IMW))9J<3Hsh;FkO;zY9lPY4DJFevmriIan3j`?nxrR; zvf5=$%hb>@+AR0Pz+~}zeDm_A!b3-}1-ptuPOWMZT{C7^17xIph2ViF)tQRuoKjyp zyPyp{G!1Ag$;A)FgJPJ+RKvei6<3FJD=+*?W#~HJ_vLwBuD&HCsM^#W0$9LpweoqE zgHfRmZ(fm=HdFK3-4$H!POvDQA@Cj<@6HKigYkrP-#Qo*CKqu=>R0$@UA_eLyz8zd zn8&EEaUQwookS?9Y3{NV(HKCv0Ew^r8&T~%w(HkfwtkUTL5KbsQKvEAgoB=-dJVOt z2QL?bBv;19R@$y!qHu?P5VPR0OAYsnM=$UIECwhQG;D`T2-ikKNhh{zAC~(sr3ke( z*SU9y;DVAb+BSr+Hw^#NDo9-H1K9B)$u{%R(L>_Q9Az{_$K;T9>NTSIMMF=r9l$|- zaXdz(pp5Jql-$*%sPN~|xrH7={wLhJoYaPIFf>TFWq>TFtauD(O2t8z7UForOi|GN z0$JI#)FwUYU73RT#pPTd0FRg)rpU4W8gU-I`}KC$m$e^qWEd&#$7?8ZGOGW|xi-vS zv0#o*^U!CDwYBrq$5KZc<$-IrRm1i}w^_Z6I`Mcj-yw6!<;i5GmX7ao0_u2<)?ase zM(2@aU~E%R5k5=QO$POPkT`$n}&A z8<-G7+0dQCE$vOI)>bW`sf5Xco7qC?3}E534~G|GW$CY3FLu1^mrg;Zl9Dn2CJn;%E@7 zG@^b3Rt0_OJ?$RhOc*4KYgz3Gzw;<9h5MEMmi@Gae7!n0?ZNJdK(V)^Iu0Mupfo2l zvZp zHb(6z*hX7>1xeKQutwIg7?yWd&>I!#|(T-~mzcc43!G$CYiRH9_V;6L|WN=N`UK z7_ur+-NdtQ06g3u9Fu1Wi4Oczj7^s9TBo8B_(gRmnsSL0zr$fh6Ibm%PKqtS`KZTM ziK1Aq@BeB8+#QO1KF)WeSXHUY)4B)oD)9pnmMV?Pp#zy~+HO|DpB@;VQQFSYu>1c*X`ieYu? z8}ea*91HN%rfvGL*2PuAJ_0wP*y%owhg2a06_{7SbH-g?dD&>`8C?x*@XrI;cmY&?oK z2$OksC;u+5Z6>Ab%m<$YHv2v$0;)r@>O!JKedq1>;fy}pyY*P%qWyB(f&C*MqdM9d zUCpBjFmtUi(DETjVtQQ#;RW|W=H5BRx#N)FxZlX+Z9G#U7R}p3Y%oHbMKa1ZfM$G? znvidvIR;H*33#?>-6eU6vw(vr6R~V;>B=}XjymkZB5@KU zANnw2+w9WG>}vU6+~b$aKc?&`ELl*F!M7W{!5KCCj0aL@RT5F9^3WNjMX!P_U6= z+i)T|!Z@S>$cbs}gWCrL_|#|os>Vp<`X4JAh->ho(=Bk$ozomwp*hvSEu zqVM4tkCLsfk}|r>;!D15&K&M{w1$oonHbb-O#dp;pBae&8Y;3wnYsAbn;`h1ba!4Z zi`S=}c;!#Kl)@?LElRME@Rw}a($u%w$<9!S0?+b2AF7vva^Pd_3`uIuH6N^0pWh3BS7LJ)7kaykl*ZaNoEQ0EN=NDEGM2h14_l z`DNW;fE^xJ!;Y&qk5WMiX6(G({^4`2g{il`f1R|GN)seSto^92=#t<~tzS}mE0}ov z8kfh~*-pLEFdpg1%K*-q=GK0@w zBUqDY=&a#G-S%gknpF}grd=?m6a@rN`|(L~D`?NIYGXE2SM(-fu01v)X0Ny?yfhxh z*uQ<*lhua&F2vmURAwFwhEOcXbKu=d%m`F)e5qmK_sNrgIfF-{kD=jLoyl^0@-x)K zLh3OB4C<@B-3+nMq3WTq3 zCf$rabqh>pgCRz^_3e_e^p$;1dzu<74G48;f6n#|vOep)dAZ`cqo?hWzv_gvcp)1lsi8kfB|yk6FCHhFu|X6GgmTPO)gNjH~&1{YJAo!|xq;<;NYpTV$DW z7lh<+L3=&qtMi6DFmsZjQ$U&p6A_tOkB;Y}Za+Zz~3F&h602fJ@`tAnsfM`vy!d%EDIb z)A#x%s0gH6V2-kT(eVWLQO|9TXK0;Z_gRUegm%WQafRulz9LacEi7dUSrX5X9S8d>$l@!LTXI>kV~ORxm}W? zf(0kRk-I|!>L6>NL$+dJMNM@gR;k*sO`&Bv?(EP zb#fT#5A2U_63P)MPUj|i(IrtZEnIel5|_4RUG2CHFm`R1VwLEl6iZI=(-_dhJwp}< zvf{+pn>uO?rRdbavP{EHsz_6qexUr*G^oiX#ztk>Nd8*uoi6PwrkLoryBbP$ftG_ZBoCJC zQnYH{6PoF;&Oiqc7sm{x7{qK8R*T^T?rT^iEcy<_9xdAz^NqURZq@AD0^DoeDDPge zi=Qb}W{S6bzL?odu@8+`g}h*M^Ywzp71nw%%D&C}!IH@wBh;qpvWf-q`Pi3~hi$Mu z!0U2JtW%*PuKPQ-W2K}>3L6w~GRf$i@7dF!EBRoSTvA}kF5p1-!=XJTX{*02W-ID} z!N1f8yFVeWL<}|Anpfg^Fp4~FaQ^xv!8PV(6!wVI@BFx8LJ{afwBU37b8ZyRKY&2B(GOtiiS&2oKt&u&|8 zNNYcH%ou+B4_qV9i4VWjMuANI%lVtzo=VX!RV1d{bDl+YxJ<33wFluiPO30t*eH7 zl_lW<3wL$_u6X+o{lI+wN~ zrm!1OsJr?JqJF1Rq0Re9Z?9@l$>w_QR13EepDU#I z^$h~pPBlepMziag>9cQoAYiq4YTKQdPmzmz%*t!Kdw2>DXz@G&hXD|??p&VHx_v+i z8_D;;EiQS{P&CK0ORR&%>GD^4S?aQEkBMT%LsqEcpFkwyQ$gC zG;eyP2^nl1kxL|s(|ue=dqdEmY7d7mO9)Qgx{+#YI=VgMBajk-f+X;Z754>c5~R9O zKngmwsr4a2nXMNy7`#|>#Bu4-9J&xbv-?yrVW*lK0gv*=T)dq9Y}m6u(aU>(-g;WoC^0{Rqd5~}(RM0YmuwG`;wiWqo1JvH9NDzO3Cyyb$Ujt2%JJDY$L zZY4g3MUB^TWo5Zco9mr!OF&DNh5mT=uQ!u)jUD&;{<;STbf>Vq%hIkx))`y74MoF@ z*Q6YEbD1+6O+NUZ1u3n}`8x7EWDRe39A+Zyf0kpKt&ps-pMN5MA;7V#b`20ahYBK5 z`Q%ApH}x>>>-yMh_|rJX?PqRHqLOE$Zf6G_GDho#?V{d7BWf6j5T1NNY_$pa`%a?h zj(p;kgmVN&yt%5z-vh+jNo=tL_sWQ?qJ>g;B!X{NwDRq$@*zsB?Fw z6@y0?qhOt5)ZPghG%kAc1{thq9z^@moDhTbLlHwWWp9OPaPTyy$_Z+{Z{s`lS`#fD z9!PAq74pwP&N-t@eI`2MbrWkj5hbw3ZiRar@dcXQ)Uh;?4bh znVMod8elcV%4n9+aP+O?EW9X+t`&J3Ze4|;8`u2G5 z=~MqIQVZB(tDTy%||$Z2&4z= z7&|?C?S^bro8l>S215@g$H6P%gqY#8K1d^ge%ZLe9C~Q2qc{{L2H`amxuZ`L*pAr{ zQivYBv|##9lpa?k>s5c3+5q{9XPELc3%Nx*H9AykM7b-UL z_k`=>kz`%$PP5DB+9k@GZ7SZts?+OCAj~ni8dsyPFGH@Do$=lrl$0Zg9?=6w4_8^~ z^S5jV+*aJApf=Qj6veh)bT92joLHsMG{F-~NOR!-z)FQCVKkQ_d}7bg0O4mq6b%4l z9w;Z?vKTO)YkR+V`vxDvS4hd|OpRKglnW>w#crZO{_tS++$jzTX7|0kv+2eUbBjg zS2dPBD>%IG;oxg0-2O_i}ES{%}$RZhCTQRQbp5s|CY&*5D{mk_^Ee5(7Np zNFt*%-Yk<;9o4KgmgcGn!WjETk972Ml~gFe3DJXRd7ol%p!uTf{ZJw5K4V=6)myn4tgk)+aUPNB!Z+?jwV zU3no9*d|9gW@V%|t{jg4p=3~KXCAx+56)4nq^Uu2Wo6`EE!oG*hufg-lTAJ z5T9E8)Gim&L&Hd-bK}`*e&%hoC52)R;tgRM#$ofLFKPhwhW8TDISZU1hDNutOaorn zUWq+eQtxbkGD7&0Wb13pf0B%N;j4Y-FaNJ5T=cX=vxaeJwO*kI9}8W$6Aj{~$Vnff zj8H+Q=8=r^5a}?H9NF%fIgWvbUDa!&TCF^;w|NMIa$;K{_2Qqar{+_lN!8{bjUNTC zmJ%1-s8b%-8)N7fV_j2Y5!1YrLFj#P*fCqf&+emh&8ih2l}K;qH5odkPNK#>ks0lI z?z#(6HWS|ya=C2qUC3rDurI?|o0#EQ*iw~Qvaq0aJ?^p-3E%Ck;|`e#%3`Ulpu&k) z3_!}kwj1P3j`s8RGd=N7EjsP{YbB}lB83)rJ1HL)7;o*E!PrF%(~@}2u{!^B7j_5>uSp0;n+mNkghD?DB#xc6DYCBU9wR&QXK5Az=OfO1w&^1Z`lI)# zg>D{Engf${LZ(SJ!;MyAg6wqPM%2WXab#S6`~06@vvBK0q$nO~hI<0z$d2gqy)tG^ zyr8=i(y=e6_+=eMtfujyoQDOUJ$$@gW%l~?RrIShx=DJ4O2|YE{Ad!Bmd&0TNTVwl zarsqRtB_2%y=?|-boUHGp>X9EMFpB*c~*w9W0i>QN-69-L5?_$8Kw3H*9wFokIb4N zwc_OYfVm=mEBVtpG{Xm{Fscl$Dj-z<=HaYDxP%>;;Z7YJ)2?h7Ig{0uj-dFob4RnZ zqU$dWMGfkx1giA6RprfLsJ)^YIi_xwhTZ$CbMxLhY0&sV3~BtV*z156C5$N3H*x17rU^#Z!aUUc7A(De=Sgy)hh5$n?u^|(enLU81`iSNQXhn z5q{G2W`l|aWqvN2L>HxyrQst9!#L)8AGr!koUlNA-72adS51NNq;fU;HD{4I=Mf<@ zaKhY3PL;ybprMPANQ&363Se8sDJd=Zut$PWlxl8?g)c$u zh>QrjKhzoNKfN+w!-uCn3q%hJbbcmq9k>y=@qjv z>TG+8DMJoqIkT+)K2%b6>Ac&_q7#=Okn`M;)j~|WR4qB|71K$nL0E5R98t2tWJo1! z`wW**HOs8Obx&Vn=bX4xz(W)dqm^#a>R!j%+h^foV}v$u7kwc5r$ZaMI}%{FcoM;4 z#1}8FmplE))LS(p=#3DfY$&r!;C_-}K#HY>rIdF?(uZ1+s~8xz3Cn3*f*lkTnZ`x- zWIdEZg2wSqkxmaVhXiY_$7%PH`$aGULh8!Qpr`mK8Sa{=2)lNZ5}%V}8r;Ymd#)?5 z2fffWwF;0s1>SHUAyR*Re{hDuDlQpyk~g00g7GNV zla9(xPnyVNM=ILz6_ztm0M(Be^;AI1E5)rFZaSNZZ8fzsAkmXfdQU&GankUrw6Dul zlv5KR8a=6H%!l9xe8>zJ&rpy|(WJpU&F1D%nM(9VzX8^^bj?hmC$_9QMP-LGyY!>X zOrqB?^7wPHkfqWRYc5c=$TcuheG+9?q}O&=@Q-Kkg1`pqcL4g4ZPHY1CyXemWJoZx z9PDlPGM-c}*x0jmgMG`y@{b$c!sJy;07x+RxuJtX9 zPQMG(hPBAslZ3?G!(E`2Qp$JW#t;xX3S)7onXBPv}%qhaCi|l!EX}Unt^AmxnNBQq%TYazu zjJV!CO!%nn3>IegB0dInT}C=`fnts4Ay1de(DOMM{ANr{U+qmaifAwGGbO zg`!SFfGv68BFM62YgW1p&Aiqz%*5EsRd{jk`GNeD1GS?Go#onDz>QOgGY&njj)5V%A*a}<@txXs7Hds`6oyEB_VSp=S6 zI-VAE>9e=;*2rY4PUYZ}4@9S0yvDBqRv;oKmiJGR&0?2%V$tl_({^7N*zN?mO8uS8 zo#Z`NJs;(JMv?R9A#(SV8@o%HouNMYg|6Pkq+|4+gMO*+0tCF{5`=zM5>Hw#(Jd2r z%&uWly)QX)+f8d|E#rv$_Q2x}z)nHk{@JxXuC+(H8VU ztnV0Ms8??+6!r_P3fh;nqcOt7t%_QbAnnX8`xJuN3B|c$+R;wqGJ|p#EpCHCD}siAj|c&w2;GpU^`3_8Pg^ z?!A(!&Bu9JBr5m`Gr#4?fkN_itOE(MUxE{DTfW1RC8>x7tDl?g@QUBhIUa_BqhpAQhwQRQ8Dd7fPm50SVOh8o!7tuL zT>{qon@i=3#9_8#7Lgz_Z=zEg15>_27A zR7aY|Yr?swr0nVId!(IKB^nwYe@1i35cytbqs{egD6Q-E!`EL*L*BM9no~~TWqDsH0;DCTDHZ4YREv0MUGM+H*g3_B z0(5J(ZQHhO+qP{Rr|mv%+qP}nwr#ubNhULs$^6N^ue(yIhkB{1{jF8r-SlQ2FiGRC zoXt{}s#05IxB@LHDZf41DFfxCR@0MuvKY^X;;qe(YCk&ji|k&c)$F2>dxR7Thz{A7 zLCw4zuKU}uF&k`5d5vM8kAF#{p2Rd1lDKGLefp;ov@nrwpm+$4j8F{D?9Kq5y>SB)maShcqUIe8&C+ITpYPO(|X40$rQ-h zArTIJ;RAHUKAvBop#zh1b!^19CySa{YM{>lV0}$f1|=_@d+@RnMl>|>S{jyCMDN=A zl7S$3h$Z*3Y`SVl@Ql{B$N7aWOgYATgu#XZgK=j+3j$c zBnv=I5$I%?2AmvhG_M?_8xZ$d6XY74sk8z>mffG3L^()^@;Df`Z+89qBTV%10E7;u zTbUcb!I36XHhJ7Sbg_&`wDzbS-k>}qjKBrun1ZMC)6zYpoovR3*%HyH2edp{DU*8r+Z+ISC+Pq|5V@;sE%(GAR) z)v{d@-NeJv3kO z51Pd?G4cx@qnnKVANb7wUkAeY54>b${@)ZP69GFXS3mKDR!=&}IM%5)%H`@*DyScp$*q zX@UR~W)RqM--9t|W^MqoWuO?r4xh0oG6if9!9fh;~z|CP4~H(oxlh47iR*RkS+t7!Q=jH<8J|hxe4@f?iqCM z@;d#=CWXbHF$8iv(NO>ztVzS0NuZ#HvkFKRQt9Xo*(s< z!vb=11soOsp75mA{nTp)Apr2v2?F8?`T~q00ys6-?SFL#q+|l0#Uj6Le$54?h5;`D z8a&T|jX~Rhdc6%k_-Aqk0YIc7k4+x>asMD20tNs`*MR~Vz%_sg*ZqwD7=UShhv47f zgSmlXIPs3bL+pKgf4)w<2^yv-glBK^Kk=(imFHDd7FCRVxKIANNl6Oo0^(iq2mo-i z6e5u|J3Vv6bo%V|MJ-r4q0RJ$jLp=$0 z5CAOlOR*mu95#5o0sQtp|BxU3l0EKf{^Uyi-bR{aUtRsYrT-9p;rlXs*JW?+MuDGm z5#o&qV16*b#Qm0B1pZ{`n#Pf?jsNs^KR`5wImQKR@JnRij!pItf2QKXq=I$^(k%Bu zKxg)vJf`Y?zV@vL5E8Ib;Cy{Xc!nPwe9-R>CTVv0c!=%6Z+uOfg85-^4(0y+iWYLe(xDmt3~RrD%Xn0}Z|uB`bha{0 zO7=C#M8;Z6g#@Qw3B7EtSC#tWQrrEHNoo9cO9|sIgX=G{C(+7bV1gagEwoaKT_8%c z17H=jWHc2{FRb#`LWguB;_RcS>ZnZB15_>+>< zV?pXAjmhDT84Aa(56KflDzTSnRe6?ZrC{XpClz>0SDRndk4Cz{Xzvx&~rs%PcA` z%I2kp?DTTj1+y9W4YJtsGL}EQS+JYEH&T67Gdl^+U~rf;2-d!kp{IDTiSWKJcHQ231MnxCpl2e48$KB%GT=RXWH$J=Xyk(%H(Hrd7#QIafFClEitZ8 zBG^~DL{Myq<{469kLn3_pNNY^=dh8n4@qXZ6VyRieI}5{2?HwDe|@U%^d`BSEeHq? zy1w75_O)@{>t>ckahX~SK`NigYrPhl?M)9#j~DZf_7X+Mu_}d-su?E%-s|N?#BQ!w zSuJGiS*FuQ(!4PJL~3~$K~M9l@+M$e;0lLwBRUSIY0&fe(VQp~xyMy|qAHrHvjuIi z15et2PqmD}CRY3Y(3m{e-H1_|x8V=s(;1%;?~zPdwv+PiaFEByq8qf$DP~9_&QZ5B zyzl(BV>*DH=FUf?DvA|-QxEUc315%-w?ph*-!~_cprZ+t$>ADiYHU2c3K_0OQZ#{_ zFgf^2LsPKbvw+GP7L8$yF&^?zUJoAgSiOni=$`4)cF_)H%E?(dp0aT99QnD9)3o`a z)~Z|`DM!?woJRS^OG{!m5GgEIU?RrxNGHbYzA_C+Wom|?Ln?b&Z2J!`NkgJ+lh9T% zbs@9%W>|gN5D5|{O)W{a*qtaU@dXL)*}|={OD!iwln39PN08+YNa8VZ&FJQ!etd*Q zhShe??9m2Srw2{vyLmRfnsv(<9#ZHr`0x)PD^_I>*39R5@>V3%U3iCl>(lWiRK2;4 z(}r;3*?+tiKgZc}qj|Q~9efIXN-^*tg$~;0oNt#9Y zfCW3tb}G}hL4T0}ioJyBWJFs*@mEW4>w}=t$ZJ zAeu3BC-cr&%xt}*i4IGS*?P|3ah4k7raT)&3XVwEqaqzf;XjDuk2gyR&zPZ88WqQ- zQY)`9+k`A4UwVYo=$x!gKDCfBU_(O-a`cG&q zKq4o3|57D>2!gZtYzN1BO6ylE3-PF)3+1l)Ew10lmnV$mBz~D@`fm3I2}V0-Ip-ww z5-hPSUT~+rzO*U+hSx=*f&y1-!GOh{nKWqWXp}vm3;?QZXf!Z9NYAWhhPDV|rcc5g zjYue|4N&O~yWOnwVUmqLb6b`>?Ty>E39*Pxs=qD7&fRc*8#z!(*m2 zyfUs}_BLTsTKtqqXvgnbX=3c;6t!1z>-b!H&||8wP9ft+ix7PS8w2Ptm^o8_Bfm;a zzoyLsQc7r;l+!nv4k^5g#vwxzeT%)z@eX7@s0l=#csafLI6Gg@XJ>?Iqk@KQrD_>* zDkqd`;e-8kmDklh=k*zZ?6lD~8xoKcsLGeS5RHGj0kD!=}u z3Pl>w+|p($I@*zT$pP8~jCIt4i|VwIdotj;z)u<~x`Dq}I)1at3TWM{Ke}Ba_?hWC6Wq6Y zxvWKA&qlctH}$#keYFopH8SkqN@dVe-`Dyk@RJz9p2#GzS^8*Her)S(rygxoxTeK` z!h_dkZohyT)gkd%Q1a19J!^&f;t1T0_x`GV$XQb$eddx;S{*troW9`~5!CnP_jwO8UyfEpye9+JQ#|`v&88r>iHt_(`zs-z6g**o6WPir!%z$!gyki$?q5 zKcK5;LN8iuYmhy41e9Y?qk~QEIs@Ga1xm}wkL&+hp+g4E^66L6Fza(kJwGHTmZfl+M0xWk9l%3 z)I-%wgv0#CEP#B&(D0u!;dN5tPTk-j`t376;N=|$aJQ{4F?L7UeAzrHyBTkAOMLEj zwj_Gg9@goJA`PuCa``J%lVrX$PMhxVtA^9@L38$Lwy{~=Iim?f1;ksI?9yxX zb;!k~?^~^NpZgvX`!u&q%F?sJnNCbyU=$0n*K2bo{EFdy^kjo;E{A*gXDy9^=_q*{ z0c|@;T{Fi2;OItNKng**VZX@Th+#0n%_*(|Xq|Hgg;lP1@rPc0sDzskXX$CGl~=k~ zEkz3TwhShoh}ev>tDz1Bd3!q0t~ef(zCxg1o3!Xi0Pez2M^SA|#c4L-(x zLR#3i+PuJi_uFV%p zO2>&n&$JCb2gdRTp!j}VTZ|g^KeU2b)a+&fPM=QPWgR>vdM(SiFb6+YcQl|JTI{;* z#=D(`iQh4#ivu2B7|6kE(69$Il7wceU{+wq43#s~BDQ!0U`fT5G zmHpc?)+eZ4qR7_0NdilMA066)@*Ul@k+cO4C8sSFaUBIIY2)cl=mVEm^niv++@N-L zSdS+vufMaj@gIh2_B2~7VS4ts3$ejxug_J&HU{^KzB+e1DBpf6kG)n>8_x67KIk?@ znL^DTZTv^DPaSiC;K9sh7=kAK*Q*Pg((!U#m7UpohvO# zrOUyotb5m)2TJeVWf0^thGR^jCpv9=>RYL=&h6zVdE}vX{XmHWY)j+E)2SEe@~6B0 z-|K%&=Tgo+5gK0ag<0kPJ3ETEt+Wz~CLz9wAA{E{qO8%leD3du%?hju+9*}hy~b|3 zrcfi7X+xnK^eLZmoE%TRJx=B!R~mB5$wl+www-b)rSw2HUl-yq+q;U4>2rAne+Gq- z-XZI8ph$SWe0IHKbS2zhKZSh)IqnPijywjOU(tPIPG3K(=lo>u)D}tI8%Lg?RE=eV zSd_m@#RFGBuba@Y$s0IAne6i4alDj9DQ&qrJW5bAw0z1=ip2!3mY+yzPUm^tDTsF^ z859&m0tli1Xg%m}*iNbY^z5~31rNO8uu<)yMo4^{lLFMX2bEA&W$I2a#W+ma_%C4Y z+XDuZ#$8(7wHXonG@Sj)xGWn0sj})C-4&aXgSJIH=DP|_9F?uH&YF?}#LX=+iaLQh zyjv+NtkF#nmRQ>RG_|CvA~cul5wVAM9mJ7dr`t@b=N*(1$F9U|?B!iU!#vMl>;8|O z7CHv_0u4fW#9sR zc#TU>j@-I1!!QF8i^G3}1t^a{6Rz3$&~^z^f7Z21aNH#?^54jU4AZL`=~n5OAJ8wC z7RWdClW10;FMV8bQ@SJXWwl7LOGbTaV;A__TuTE*f9-x!f-aq^z zIfcYKjf}vZec4Itf(;>QU!Q8~?eA_koyRcfyg$T7Ul1+9+St~X9$2lmm0(y6S>m_u zOJX8?)&ExbK3t_oQ(tdeXr^6q-|M?rImxRo#+mSJZ}C&aNEGjq9{NJK4VY2J_R z@}DC?dC4hsA!!ke(EpM?2EO}>PrrEa`P?GN6020?tjkCGhC10DQPa6l9Tkt)npQL! zGZV}Z>h)}u=vygK_I&&W-Wp~A1#$==)#;&wT;2FW_EhYxL_J0gSVIg<{37p_u*hve zQ?f|uX8XKCK%OYu?j8bR^i=SYF!)eEw(^O*$*Rxsr~;r$8n=5NnSM-sf|z!?=;jc% zC+lx+olV3lTBn<<={qU^>G?4rufrJ0gt16CoBD}JuY8_u%j zXJ~F9pLhAaKcW^a42H7x*AX=GwCywpbi+uGU*^!`LjkvJl@X zHGpn+@T+qQcyk#=K8zfI`Dwa~_+I1o@W%Xwry^0s-g$W`J$Eau?!z3u=qT398C*Uw z%4&(n*Wg?hHM%Z{4bpuzb6qbDdOgFWmO^!Zm>ipsW`LgSr_X|KX7MWK;prhlE#v$% znx>Wl@nka&?>vX^u684SQg{%rn9UaiR+9WD;fC z8;F>CC9z=zCgW1gO)g>~Ry@)=h9kj|Tsw|$<}H{dRMUfyU(~4`flqYZrZRz>a@sh{ z#;g==Uv+mGuOF??MvK@)ow=h;`v#*t&|bDTEeY+N&-VclN9A0l3p7*YW7t>l7GFT# zdihUeD1Lq5lXJ(NIP%1oVLd_0eycr3Kaz;CuN%nicv_ULB0BCP1lP;>EnyE+5t2_p z>=0UX8nZj%=-(CvIm|Psm7E*Po@oA7u7 zBULry48vZ`T2K<;&osLsSnGd1#IWyry5W)r$P*1X_3r<+=#ACBXVRq)ZRQ0_g<0C4 zd>6@NcF zURseQhy3h2dx=#k(K8X!ZM*0p6WeCP0ew@TN>9Ks#~TYNCA} zPV0eZc2rMXJyt_;%s#w(82y7C*|7u8 zgQ;ITKJP;}AB=mR2opTHm16O|R>ibU{BZMED;+yf70;9X#zR<7OMfLry-4WG*3IA9e7+3NXLUIV*jfBke4{}TOImNC0cK}DWtT4x;Z|i2 zG8;Ud(?@#0PY%HKIymYHkbXv3L{*bWSMVk!il>W7M z`k{K5G05L*$1<}jXQ?JD_A_aqTE*A_sDhrxUQA&1p0`d5bg>$5btKzhRGyP>dqd$G z&@C*c%o?gSX(z&VMt^SE-&9Hg;yv$=pZ|0Rp9 z(y~;pgJh*-wu>*6azkew)8$Nov7$-M3;+d3NS(4Xum8g~qbC%bK6dmcTvhrkLwpdl zc3uh;r=|hA7WqoiE-Xme9YoYB^$`bFt)2E37}5$afPu$4R=!r$i)akqZQ&>>ek07! zfXZ(H5h_5`bV7SOlVjAssRxtlJ@V-ZehyO1TGJ;uXm)88Ka>42?ysk!-nwfsstEN@ z!h!_KRKJseBMFq(E$BwN%b4|DH;lcdezI!ZzPnT*)~mf?%E8FUVb%qFbO)+xc6~4scYr!bQ1vF#s_u7nZhEaxxxL_KT_vrPy;>4X? z5X~Cyh3N4s(_F;K5#uJYyiuU`lZ_phuG%rPizkjWSgas=jSNr+B&Gg^sEdhA;B=sp z1Me_1jh z?A26ry1*QYEYT^M5F$b(se%;RIJM1me7xi`jyEWQKLt`$$xjpNl{fWF zkEVm%kg(sfyG{c?*@i~!LRT}Cm|4&8F&06|+7a>PSWyibIb|%n+=Q#MJ4^byYBDzB!Sx{4Q;PwN6I3dz(UOAtc?%*Sk*dprk(ZH*WQ@kCh~3l8yDY28Uz*A> za6D8kvh1Lbr&YF3j3L)(t>Ndpo|0aPEE#+|Qc|{8V%@joyl@az8ddA)i&e8pSZTUO zq};tz1miVDbrq`jVVYkTpCRX&5 zdw+Jgtbx?4e{1`Q+V=);HUlK4UmiZ?F6Dk6IC3A9XnAawolDlpiWI(d?T`+5gUZ;S zrn!kODttr+F62lLsVF;yAz`(6ucC;$U)-&@!FcQcBGPU)T^`F<79&UtZuiH9TCy`2u(PFpS=9_CYI)ki$j1#Fo=zJWhD^_>+ z`c)6yEK$b#A)Kk3%TF4Rb!@V-O%vaCy`bX%7%D_%Hy0EfMJS*#CA@iq>QOkvblXGAUy5w4E)`PFZ{qfUGcfd)&1jv&@RvSq6NEOr!drD z36hk18WlkiLpV+ydJPk9v*c{*#D{G%f$`A%EKUt`GSjt+TTh3y;nT|QX9|no*+f5T zO^3DFK~;ai!c<+UIji##h*7a5ie51_LFP4+Up3bz(2_fLXA+CL&aC=;o^|;B7n@k^ z8&8K|K6*T?e*2TAB=1Pz<)9PAc#u3fKS- zNNy(yFV>M4(;NoQMF)XUO0olAlh|+d`nXkkVCxG1tj6dWqA$aH6*mLpw&SchU0n~x zW{-59d5+b+ka8nxr3|o)(!;k13xhp=xcp z8*hCvT_23Rzm>I^&C1!=*6dfRsvUZ}=+xOYhdUnTcDE+H1A^MuxHyXt^1sI) zAMePqt>U}87>C#^Zp{u)ul}C1m!}EJfH3@!I`Cp%3v!Z6uG>|S7#yty3&wTY`qebF zh;MD+RnHR>r_Iw~c(EPD=f{nMJDl2vHWvw_4){l+f%oCuRX2TNdhZFFi(N9iX|?|H z9YZ@JMm?MFA~241_~gK6^Kc@2$_*N}2-t)At%juXGQfuVQPKXc2uh4IfR0EvS^H>W zRrklRXXy;)N(uN)CE`LnKu?gQ$fjSQi%U@b0%5r!NqYt2tG#5AAeF$Q0Q?5 zYTiFdz9?m<3g%2Yo#FzmuR0F{-wpw_FUJlpzE(#(482IDd^#LNov;uK@9&(?`@TuX zytNYwNvEg=)05cPqYhN4J$Yr3i! zN^RT@O79)=QWb=oRcmFQnm{T#0_J9RfX#MnF?QR5zodARnPFbU(}zed%R3Gk-e&e_ zFCeLH-h41U8o6(5wpPb2S$GKUO=k0u5g^?MQsGli-kKe1f2CGH;EqojL~&kOeB-V- z(xb=|;hN%(l9gvz364a6){=e%@{XAR$CYijyL06-vZF`34UkYH(>he4b}TuLBYUle zZkA_cC1^ibhF6Sx(Zopf&VP)cQ}3>AQats(0Ou?Ci4M>8tj+bt+E*EYZVc8n~5qoAHv zVFrQdHyZxon5iyWyiAVzAkbDtEK-V(KpyKGd=Q#iJ5XciL=?d@@gtMQ>8R58p69ZB zAbc{t8wIJXaT#YK*gS!6&(>njHvvuAU`{~eFLS__L+TZf%4>Mz?5E(ewc*7zBn|m~ zK>Glo5q$iNxpU9M19-~_d#mjHM(~uNbCbH-VNAy7-=T93#d@XE z9WL^r-trJ>seBMa@_9qz`*!p#5`rmK{DfQ9WV8YezNc!?WroNtgxvf0)y?tnzG~0j z9~-Y2Z7Gc=7#&fC3rc3BO1 z-4!}6QeAtYPjTbl;Y@5aat57fVUE?>GEuGUkj2;V88j5PS~Ra!z`O6LgK&9&p@XvKhBP+v!V?!}W?~1$S0e{y7q$aTllx~DH-ZX)o`JZyfMx*w zP+{a5m_UDZGJ$bG`DcU_FYY?2axk=_9l)CBOSvrFtY>(p^zG5;9Uq!s*jbP0A741BMZ)|o z@Vsr{7*koASwVwvatr*V=4X@^&l~sNy_ORb?`Ge5ikefMn*;^XU7IO0|4mA)L{4#tvxY>|4L1Gr@!|G<G3$H9=b$GiRww9Np9eiVe3l>fBjzwO^Di%sVD7`Pu!9Wz9Q>gJ%lPNigx{TC zz|EU{;`5#YDCy<<^<41Ar&s2Viyp;)^vk9%EGwyMD1+JFMg0{gCo(#PyDKm^1)giH zV+L+(Zv)7>k^#v5HB)42_;N>+@zW_5{1xKso&#=U-mt}`mbHHFF$gUeIw&Xde-OOr(gW$`0C>5(O%dc z^OfOupP%FFomPOSURl-vzuPLFxuu2S7eDLb?C70W0Sptn$6PioE=i3JVA*7vY+0Hg zyp-PK3qRWQXi|tWlT(xT)oP$Tb2Fn4{f^gZrh4CA&a55s2Ysr&&x0>_3CFmI>~nqW zk%1XN1}7Jm2Y+KPd=fM_H-GfUPpS-{?O)bG05Pz*?8i>%y>1?S|MYC)Eq(HdemDb^ zAL%Fdf429?FTt!^;%EG!aS(%~x1cn@s02R*YJbHKc(2#Q-=H?YsK{SIom(0yzq!ub z3;ZE41C`I99cJadpVCIwpX7V`;KLRl@NalXZ>6?=gy5;Kia*AEKn5(Iz`L+h zKY+hVT0fHh&-7;>VX@!z-PwN+`OkJ_r+xu;XD9WU57TeHU+u_^{FA$R=dV()x&5#BH=n`Ft+xGZ>`iyC z04DAau;wl#j?UE%`&}ynj{RyRXF{cQX0B z!`=KJ>vUNi9Nb-f^WP4;UG{IkyWX8_fjsUx5If7AnPB#{3c9w#9x;sFXkYg%zfdD} z=H$>F>+$=}Nn#`!Bw1Ipy^h0bhlNl~UC3d07A$q;hYFGwC+lYy4`JGv?dn)D5 zYlpvy8bQdrF(H@W5QdOv%fT;Q`Z!&zKvjg={hcNhPPjU4aY+yJx7#12+n3-IYGT5t z?#ZteoF@CZlO^Yc%Y}U4D6>jOnC8>_aYEdS$i79Q-0tEz-R;?elj$DBDG{YXkDL)^ zv`-7`1`(cVk2=)~#*P;wq@&CIguz{c*x3b7NSqQW{d#v)lsfJ>vgv~#d@Yur$?GTn z8_w#2$2<3TO1TL}fniwaVTee=AJR)+nJR&{jFLbs+AHt$>8|eQ(lcttrSg%GDfW?U zSQ#z_3n1cN$)E#myMp;|yGI}uFJ$&xM_#@Qv^)}eFNw4J~ItF){ z>iQrCoKw9vdS8oNb}xy-;27c&iZ28!!PIOBBseM2hR|8ARY?5Ta#(%(66~a1a*3Vl(XlB!+$U|wC=_4LihgkBd z|L|uN%IWGSnbCZWzoiwAqrkdltMxX&!b@+ZcP>5I{*Ey1)M@2Ahr)IHNz06J`w30e zt5TIZmU?Z)6r1edF*UJgwhF}b^<;X81w^!b-5L1`Qt0#Dx9b9y96+51mZ>Qacbi~s z`fv$Ddsqe9+iS8A{hdn;{gXEEUa79YnT$jo1Y4kA>X$-x{EUsO7hLVckIKb9dQ!kb z?$U#}N|&rbHiSZ1kEYx|EFt{?ygeU$UXe3q$TY%Iu%{5{SsyRHnC_sso%AE;oKEO+ z14Ov55ifI#4C&hfM4J#=l)vVb%o@Yk;lf_i+$42p>`pC>V1Uxauee)CCo+ZP zjP9eQ{wO=1VN)EX=I46aq{@o-7vNkxV!CSAjA*n;lnXqGj%M=T-v=ggIEeK#p_L!5 zA1Sh73GATJBMQ(7*Pfd~o@j(vSp248h+Dp(E6p-8xyn{`fQJ1Rxu0Vp| z!2EBN22pDa-W!1vJw{%cGrZ%jGLz&@a(9yy6-PYO6&Qr_QhC10HpV+LayYc6)SDsS z1&1l#Pmg5W2niJIYP&$3gIZ@o%LXiFsTxaS`uJW;=Is$X0orA@R=961VALv`KUyG( zn^(B!WccT47J>cUHNleIiPPrO%W%rmnJOckB*SSMb5kh=4KyK(Gdr4`hw!|;l{?|> zcanj9-cc{=3MvdFUZO>a_ccBsNOEz3R0BnHkfx+4UO4?X0PVT2TiLXr!TuYske3BELci)ea2|_7XDRw@#BO!Q9@RAT5D^!d z>g;seINId}kNOmMU`@+*Whym=p?6g!{Z3aW>5#{h0(?%j^)3dd5j>H#(NTq=?m~i} z%$&@OooNPX{A*f9SQDmuae<-;JyCFpsn*!j%MykIP@|ve%!ZQGe#6}d+J_->o=(pv zpVNTM)a^~gM>yAcs92`{Kl8PLiXar(s||*ZrC=fD6q{g);|KY!F4-#>60>m$2ANSYF|f$ zuNB*e^J?-6R7&a|Wz80n(dj{C-%1P82w}p(xG=UAytsqa?a9${HN^2D%)VD`1piQp z{Ktji1aQ(G5v&O8-D==_%!S(wH%PE|OcMI61=$@JL$bL-N1^0AYyOUw0gh~$i9I*g z4*+mex_8MDWgPr2@D0Rt-iK`wSP}^OvyF;SL0fW2yel%8Q~w4W)+lRtw$Vm60_g?1 ztWIy26czl=hkkv~W9$y^v{tx?9{{J)%(nSJ&FiQ0STpI(e-33fwm)KrR3WX%R9#Kl z66?u&E8Dka=&51NfX9(&$V>ymmgmp7Kp(>vTQ!`_j(AOP3@QsPGqlXAJS9*j=9B@T z`p0H>uTd&n&Yu!OIkJ*Hm3={e(|6GF_C?)eA#i6K`#Y1vYSmZ>%%ZJ&SA)_FWVN14 zZ5U9ri|%q}kM#!NBejy0!Q3y>s#55_N;aYUc^ec%+gSq5_9=diYk*oW%bg#a@#UQi)&Sj=lRWWpWVSCwHwa+sdGTWiGJt6WI&&{5Ot6rYa)#8 zU~a&pq~+U#Qs9q$2UcQ4qu&PtNx+ZwR-}>0ZZ{M5nW&A zwu`D423k2+-klc8gLhwl4By2`5BJIxyyjZp>ISV&;UT?DqC*ga*iMr8&HPCzlgGfv zN3KfFl$#aHBan=h=;V%sX&YIL`*-@sV*;2YZtk6sEe&x1yTDO?JdXdf8soN*_m zkTGN<}J}$p1+t#R?LdwC*;E)H>O&9hp5$-DHduQ%q{XvGW zjg8o%aTFej`PKPx6z9KK477=^p5m8hDodk-*YTFBx>EXkrtH>=?c9_r?K=3KffYRU}Ag}%z!LEw>Y-UcM zr6E^R<_i!bYg7i`@!0Ws-f*86vWShI4(0^w1HfK|iWd})PCZ_VM9#<cc5DOnkLS?THJo}3IWHeF6E#f>TQ}LNqwCY7w!Y|sftcmbT}Z#}Atpi+QS9Fi zH@z(i^XI;k9j?E;Yi0XQ%e+zSOXV>_5X8js>YE4zyvr14`*CA9S0iJj2jR(LAoAUI zhmFWWCcgUsSWZvHBYQTE>$eZ0FUi2i8OJJ!ZGKOeVME?$1BkOT&gm--gK9*5)6`L~ z^8@OiLB43%7C$w9BqpEu_Nmh(A5)>vfPoJszIan>W4FzXxvbzM=%2Q2#X$Ctdd#QP zg;9jkee008ULAQnli^F@EiEtRpo)9=_^3(6X)D~yf(8;9A0jN@B|G|IGmRzq2tEc@zV|$3e zaQ~(u#+E4PIG#pIq+lG!=EVmecrrh3k8g^E?kv1-mXpHQO(;eBQR*rn`e#aPp{u=p zEJL@VB0pFVx=!KZ5r9lfOv)GK%e+>JHhUQ1Kybxxx}<7S34cgMRYH)8<{FXcX0E*1 z)%1Zd(yV-6vF5x@8|4H=l@g4Ly}{#T9Z?&5KW1N@J=yL5X*L{uzgp>W=BeFn9NM~) zob;@wvkKLxKA!jj*o3GX1P zXPz`d7RY|eD`AqrKKQ65^G{k$8Y~+Hr{tOlwEh{s%=8`V$J>v z;azh(Hc1yg%G=-(Lz9>n!gQ5wX3CiR8k2mRg_qPYfQ78ZYGc}+%_R0v8 z?`@Tv2$OXh&P&rQW5Me2o-}1pJh34#$o#o}$0IyTQLA1NHRa$Q9L_A$@dVPAyY{E_ z&kQu=7Sy>kZ{a1|f>LmMrJSbEm${t4QO11rJp5X#?{1pu$fT5IA-YwE)UnHA#%E!+ zh3u4lFq)5T^|X$(NV}SN=v&3FO=PpeMy338wHRy!wHuNF}pO3v3a*I<Ov{iS z-<~ip{-I`=W+)M8qcjYB4%hJW=Y{Ertv6l&ZzC&U%@{MKf0uLC82zXaPV&7GbS7WJBlS_Nt_ zsujeFlFv`jp2>uVU-SE3qJ!8eN|07mE&qb)Hhg$`t3!qXwa>`J5~b?v4JD8#5!Wmrqn^>lbm}e!*5bPbLF9_JxE+Ss#20^po{k`a;&lV|$O~ zNa2+ZYEp`)kza*34+Zfm2ov@qa{>PWR93X@hgE12B!-Vx?Rd~UjeT4^X2RjZW|8wNc%Z*fEzs=A zpqX(i$`;%jgRz2|3`TIW0LJ#KfeE@#3}-Pb(2R zuC|S7#5)k2d1{Wg$79s<8t3AcBJ@uV z??i0s3kmsjl}<*bb+1v|4?=N_qtaS1N1ft1(}_j7PnSLNkJ1}!+9CK;8DY+9XO_iW zJY+O_QBrKp%X<4miC)4o3oH9BvF!7c(IzrRjllOtr8n2)IwCw`?e`?UXY*7VboSHk zZL}Zg8BryA2_|+p%f1QjTC-5;?#)k-u}}DzG`})e)6h3;Wgc6TQ+1o2@JI`iu>dQ4 z;2c#ToorR+Q%#XnA*3DZ2SG5%DrL1nG7c&ODO6+{a?O&%kFxEn5lvrw7189-4p{gl zM*@Q<6@!F|!7F`_F=+ds2^pZ0kl_MrXi#~ze_X=o@(6Mv?hY@uzyg(KJ_a6GmW9H# zFof&(g%)+3lE)NHTRzqloN2l>VqrFZoW)J~I!0@I6eHZ+QGfn`zbEJT2*IN905Cdf83*iqL# zCN5}*0OOy5>m45>Xq>4sAbX=G=XD>zmvefUtEGm_*feG!7lwR67n^H5XCcxwYXwcl zL?Y+Xj*TH&Tzz{3YKU{#T*bl!qMi}`sNqBuv_BFov%YI?f+eZY=fDN)92*JT$& z)eJB2Cb4FANtmc_Ws42k!n=j4)&r}$?QuA*mqW~b)rKeji!R1>+bO)n_af-PhB zv=XLnMufkKd@#5MAV-&PxN&#K8xhh;fhgeroUJm?4EUwp%=%O$H35*L@3kfFP7{h* zS@f&cnU&(Bj~3631f(dWs3IC$NG4jgV#g$wi+3o#d$s-x#*LoLn^NWBx%nogCcQ@e z#^|bS+g3-b-B9K})1w89webi#BNZ@UMU;Obx4y|^a#b}tIJp&-t?Im61=j+MHC)8` z6Ytip85xJ3Xu6wk+Ws6e(*$+V$WpWflX%ue*N0%l1pZB=IamrYs(BSz7xH zTKQ4$Bh*l>qhKHPcl|GOq*aSDsGV9aUJKpLJxCem2$ok>O7Bc(JF5F^48c}l{yENX zxcHS);lL4*EI88qV}Q0aM93#f?^Z z-4GE^t;zxGml^}tqRs%0LqtWtOVBHAlKP6k$Jt^$@Vq36?WgqAEpNThaSgaci09#9 zZG5RZ53f*ofaIQmlJu9Ov5I{&g4ANEJ3tK|V6&9D5GFESe_c_dQvA9}sI?bwrARlE zxy&>$_xZmFR$6534oCpTdstD-GG|y%#8EKeKoh~q-GV_xSpwi3ZQFm%)LfJWeL0!8 zn8GU4Q3xL~&#Er^Sw#5|8&S6~Gqh>P#R$9vfa(QNIh>=9=RCXlGJiwgnA5gq_H1|GkY1YUxcY@po)LJT>0wsdjF=XG(aAlSsIG_t zXAiCv=Z?e6&5eNO@Kn0U_btYOw|F68{K=PSWPV5*?=xB;Pm8p!n+Q)=JC@-$kX^J6 zih+g%HYB%~!FV=XpI2Yn2?67dY$mbRZR)wRc>byQ6EZhf!`j9+q&-MBigC-*KPM=R zkR#9I?eeD1Um!(yJ$Ul#5NeTHcB4&V!(Q3F?SEmT7+78P4mW81qq$2208RIZn4# zA7Ybo0GfUyUL@d_?l5@E*pH~MtT9u4DhBnK_oSEES`Sw!rB4dqkCbyG)0X~X>`NvP z^E{uC&(K>znf>V+;WV^k8G$LnO?uS67-=pl*3I#mwF2w)0C&{h6!JQn+@9RvIKR?N z%Ns2AJ1jHA944(ZtSJ{d*W5a@_vWhXO?T@3Rhdp9IL9 zgh1Eg8Sk&(1R}OZrM#3i?&;VIPto%GK&^hhj7dQ>zW>*`E9m*_m<=~^Ho?{#sZ2VO z%5@E@9cHD;5h$Ot3Al0d8!J#h!7DC<*Hbg7K)KHD?O&5{yzGxs2m7;v}z+f(|)#tl#-=v z&X-3D4=e=7kt|$ixWwT8#lWv0F?C}n0r_*oM{WH}n{=kfPo%Pi_r{Nc(kdHwCP0O4tlSY- zjG<(hRZ})=bq3LJ1%}B0=oSrTwh9iunjM=n#REOhSZ&+g3M6uVl@JoS>CF(+#xQ7P z`95?=T!qjWZsRT4=2Nd1qbIWcCd!uo^4rL8jZuXK^5Br#HmN|>>`+*)PS-KwAP+&) zJptCz7iyV-@Ix2L8ySd1AvsQooe=_jyMP$Es;3jfm7uf2@T(mom}v}S$JuHgwUe{A zGhIUZOVxtjY=R}`7hOT44@awGNTe5Wzs9T7y!bvmDJeJrRoJ?bXMDWxa`1Y;tTaw% z5YRJX5bi`WEB6#TU6AY%k1a)=2%}r;!gTj}@mN2oc`29WtJ%b7zRqyVAwODhcs|jy zZ~*MXKORuJA(nsCn&HC+t;93b;gDjHJafuXtqChDoLyJK6{QQ5DL#e3%3J;B=P9BN zay-`uU!OJU*Bg_#Z%6k*(oYEKLIxQ$YZh6UPk9;dK){0g56OG7=W@S%yGO${YT3cf zGAF{w(J!Cq-|=Bx7y;+lIZ{^3? z%)!-cubz-Fj&=2%=If)_QSX^J-svt_Mqf*pl0x_C!lbY>-I9(Vs%1M6SPy;)Wa-w! zGf}OzZ$=@1^Zm>?$^23pVGDKU#l5Hj+upE^nZLc^W27=+w*Nv@(n&@QkmZ*sHJvxh z>-S;|-1+oY&yjyy<*bYTBwT)S^qsW~On*>IO2mC3>i7>+aaV)oxot2fXT3GdlaD|r z)>M7y4zfJyOEYkp0MqK~8OtpO_|!=qLi~@BSW5Ni+Q~cHJ@JyW{#eFM4^l16)6BZm z@n65Mh^nrz<;Dt`94AD70YD8nW`=nK+uJUW7SRgLAzStOFd#71cI}LP zpR4kA$AEXUjkJLeQ5+kDqOFglD*j53@F46epHc3OLw2BOyw%kLB{x^(R$Zs&K=2Lr z+&wUUuyW+&d2xMHS)BX6^O5)<-CosHKSiZIv7@oGQPGi|{9M;0ummlt1Z`RQslN_9 zeF&n^76smt&u|k$%7?bSns)L}6m6A!IBh-g;6oMSQ)#?0romzO-oS0mVVN0FF+R2+ z37z&UQWR%V&0x93#}d0b$I|>YTC^IjmpAYfe9g5ufd~T)q-AxiP38EjF2CVi!v5CM z*&Cca`1ZhPBxGl=qAxolR*^A-S_t@wJ@O_~EP^ARmqAvS*)+oOSIXu8vZq9h5sS=r z;T5>XfBkLv)!f#@!}twZt=bL(*o$oWl>*Sau{yQnmt z*kSi37$zzX4d?S;Z*>GyIgL1rV{XUogh zvZWsm=Mn0+#)Lu>Yg>+3^ECb(Va3NHSf*lLLjpQOhv1N4RV_a9j80)ZGONr5e?-!a z{1@b{ZMj9>r zWmr->m%oh(s(LNW+e$KJ#FG%$xQe+#Ig2J!2Vg*TS-c*CHdTnEFk;j zdDQV=sjfI*qI8ou5+9Q`MRpFv6>U3xc!cx^B?st!u;Ze38503*U35uk1u+P#Y}DeQ zH+p-qHGhtEo;{%W8MJ$t>jcHjsuLh;Xzt8HHU&#`b~FUWYAt5bcEYn^M92<>bZ-q4 z=@Q&EDdU7ZKh4&PcoPm~6CyRAbQ+kib_aqC9rG-A)Lv|V5RCLKc}{Ogj_B&S|= zQ&4txxeRoAZ>2O#4x_eUM^@tg++k}eR@r{A>3E)by#Y&^U5<=N=~%FHd#eo$t%m+Y zKN;RB{uQ^ET_kE^G$l=wbzCM zo^GRCNL;u4Z$U@O@^<8RGu4>GTDvC(AX*eO=R5VkxpYiN<%f=}_uP7PGso5jnYaTk ze*R5&hCQRiLc6cD$@H=n61D?(8+U(d4!^^D6sD42o6+;Kcr3{VCae}zzHyHO;GOp4 zi%HLDA)Wq{XfwmeZ^FU>)iFwRc+&fK8S5&AX08Y4N$n#Lovkq!N9yltZurT&Q)fLV zHz)CX$^E-~RZsLGgp0TzK)eQV0LG`=K7HmUpxHAZ8t6J0k9=EAz2d4aSmfJLeuV~# z8&px8H&gV8_{N4fXL=7z_cazy^>`Zz=eXzxb~WW#$E#cxGodQ4_b;TMxy31sa}awX zhf9FUM44zZun1x_>UFN|*?y>W#KT*Hk>8vYTucg2&cb2RoxOTO0mtisB=-qW_-sc% zGuiN9w@&v9^>nLi7-7#>X=@%*(%Mbx&$X!kuo`HI#$g=~ghDEJPBfm*DlqSbaJuV9 zq0Q|~SJlgiHZjKjmLY)WU%Z*8X9^sSU@Ssldmv!wXnfk<_5UEs*+WHC?S7pjpR(s* z*5#^NawtC}ME9e2JC518Qcq%18^o_bT^9*dZs9^W-g@BAfaa1KZ@{T}iakAsBy}kh zsg|PTkQeJBY%0a^Bov{0!?;jNq8?G+7TiFmN&;++^Y+zb;nkB#?>ihwh&WhtTYdNM z)2^-s2$JumxyJi2=tl$i;ffEdz!=v+7{J_m+6c>i7w;lzYhEvIoCe@}Qa&Q)I_I_q zvNRoLA;RB{lzuKQY_WsW~t3rKqaJ=#3q!klr*fW7v0) zhUpC1IUSx5tC-0iwqpHPSCfc-QH_79zh9) zhJP}-h}yyZ3?r?WoKtJFI@o>FJA>Xyrdyyxy9}))wi*)Qu`L1ixIig<1eHpg9?eO{ zWg=9VPS9Ng5BN;5DL3DX6oXeTMWqw3goAF`AFh=zr$Z?+1Q*sBp>f=QxNRF8g>oK% z2WpQSiS3hBA0nKVq(UqkW^0hnY;@~`!^D4i67{FXkaaHau2K2T1Rj6Txv+ev%h0rkCro+S*hJ(DAP?QeyR<{!< z5ku{hIgA>%jTvzGsX_~kTST|yaS-I5=>XD7uFy1429g?$4!$AP^?j-jEZ{WF>SK;SAZ0Z$cH3$qKd$cD zDhwrEJ)yo@$f#BQ`l~s`Q?%ZYnaYmWYQCnZJ7;{4FC%epD5eqGEfArCeM|Q14Xi*5 zmb_r|8i27oed#m~DWOhQI&EF$RUmahRkltasSai1NP)@I!cZ@B>UTZNh+~dzAB$ja zh#3=mF+jd2uf>9hNh60zOpm{7QJzLRk4BJOt!BTQR`5fz>aVM5x+voa7%A@%@`8yKG-S=-pqk zT*jh*KAJX3NIjQOH0~$byCI=X8=Pb?DzB@LI&37`aIwJYZk=X@^ZcSMn6KIZNc;rp zAPHfn4cU;iRg;YuoMa>bTxWv%7_H>1i+x+ffQ!lQ%_#R}^XOahYT?=I+72^MM7j25 zsqz0CDAHhJn{Hd0jpS6qqlv>ALf^wIHCZ~XEX_{`YqJNfJT2Xn$Cwi{7^ zhvl6$9h6i+#~2@uv3qGT8`;ywl)54e#PrtEw}jL9PaeW_!1nXcBCK=y`?flR#stxc znGF)l=ZRe7^P^Rr;@dY9$$JZus%&q+BWuWEtJSnQG_?3`(bbzOaUs}JtEGGyc-Y3^ zEm2V|f_C*ApXWRj9$l8x-+rKJspCj>Mm(H75+BPUP8k|O{z0c^qGG96_gRn$1cSfxScXp1i)J=_Vf!ayQ z+x~9~XQTlm8wPZ)t_s8{(8V#8gdyv)z0B4%^1rFc#9&TnA5$;$*%Tp)zAxSDHg(H= ztU!|xzZ}Kq*r@&4OU}PC?j&#(3If34>}2rMr`#K&4-|;JF;Glj>7N3 zCm*)m46}Pl*vMvaTRQlT<7q&qz_Re;M^l_tKt9TI_3XWRofA%V(=Dh&cUESv=UPgL z3FBzu_Ioqeqo!si0b1rUS5^eCl%CUuy6#eB=f(k|GW6ESc)Nglu(^HRDD_2POzsVMLg09Mq1M}>B7yKd=z-E|bAh#CNSH^Vn8ZH|! zsX}&K!a+rMojJ)zFYnyejk%lAsW#CxQ&+Wo_z`S_xvo2AaJmIi@trmR_ZxeDEt?AC zHI)|@%o&(iGGeQ&(kb6lA7LNiz>u-!zj>m(z68y62|jjk=c2R|ZAL};+Ar*z7)RpE zK=f0ZcOfHAX+Ir3haHb)PB@J2J{RT_P!x@Zh+~)GNp{GFO`s)DzdNuSt&z^xD=)E3 z=qG(_{=;h?52vf35+*A|OP^;l;BF@kv-bj?D|rDeO6r{6Xgj+ww~5NgL39|mtdLfW z;SAX~5G!bI_X>j3y=N)71^1`zP=!0;cGF7*%C9dkR;awL&|O~kspofJ_6jL{tEnEN zpMu!!zz&m5*y*j8RXCg*0nN*XI_iKF1a?3>V_j6Wy|u^8^cWs*@k-LAy?Y*I5kD;M zjyH={BQ81qeaA(!*Q>yUWm|R1p+KF}LJEyl6+Y8c4lra@+05Lc&eD@_L>&mpS`E#L zr&9}FbnOqV!dn_xB zELp&6I`?lej->XN%DkSoYGN27^o^jWLep*0*{n;>)2fZ|<*6nBminf-n!~lUCo}9X z4Z@o4TesB%a+@}fwA(kJ)_@d<%^?tx>4dK#4gy!dpnO~y-Z}SywxBPDQO=UaX4t-? z+mVS`adn`u>2E5Z@^Wm z-AiHToR0TO(EPrGQTiJ!Q)t;1*vw3=R=!{Dt1D+z(({uc`4^`J*&)Fb%||8ULcwxI zcFg~EXR7~GmCAHep7kTdJ4N0Weq+?)y(5X+(SEOEPE0XEBe?P&K>7d@I9(E}6;}6} zJnD>(Uqi2X{f_)_6}<7?seQP%`QLQ`vV4Pf1elu1ViSLf()mEv?XUv0SG!)h zw2Cr6?KV2e$11aA9K8EUqF-$hk$$!nKd{8iC#g1uj*1Uu;SFj~-h3M!JTrAZcyHS6 zydJ!`C0-Za6YRizMR|f9%lR`x^XLB9Vf!33@KmOnGH6=GJdAxWuu8g9b?zf+_#)ZI zQ0?w^|MyYq*nR;)*pzFc@_}x5wvfJqFGwB@+TUW+Crb#JsM9*=8^PT&q0l`Hv=?a`War0;~NS zHgxoIkK=tKGf@fB9obQQ;DrI$U<}OV+MPG57?lDKu;gS+mZYWLbmUPwut4+!7MnZsaNhZr+1qiQoqJH|)cVK480 zn{P(?w#RnTRzU5o(UcHmjI;kf_i9ciFD=uP-ffgNQ~+b;!3b;Z+zSC_!tdFJpTqGJ zUqYC@kH;2YYsJ37NMyZTtbzH@#wt*Hh}v?WS*x#z8oK7ck9d@^{5aVP5Z1m9AlRz2 zIcGvYqsZmlhlpML!T@sMY*I59#%crEH-9-BEVDZI*gw+} zV2Xb?YKU}g3`B~A7D)z>5f5FTFJ>-gorFc#i6sp$L-@HF2$Aw_3&x24Wfpl3tn5wy z*F0Kx`R}vAI%yW{{fZ@A!d7`g1g?l?5iGn5n>j-*_?oupQ;j!}d8H3uapL3tz)%*4 z`O(k0Q{mNP-rA*fLQlYj`B%)QJFe&jpI0C4$4i_1att|qU2c0T3>Wrf&ELg7d336sRgEy^41~K0 zDoNa(&7d|9G zi-XwTrH~f*jm3#kjsa-&xoo$6GKCsT%zbHx4b)Ew7BaUFKOT@ejR>B_HMVbAw9x0P zO?W!wwsaod@kwNhDiTotY0czsllYPP;*dCg_-QJUf|>0!v4m%l>QwXSs2SD4N;CwF zseYrJS#e70WsTVaeH**OmuhmzRKvB=uAUf`z|!IO6Bf=EKg&BJ$=2UN5%fMV{spLT zScnXD%vqVDC$hgVSM8L9K?4pkF{8;-X8^+%^t_91IP4wL&z_sN zM|%B`nNyk|s&(_q9KH2%2%N-3CZ%Hh{q{gAk=YoE9j4CZf&ynAuPzcdkW1~wvFAQ{ zv(=pw=FIXrE{rn@>DEi5Tr4zB-YxmezC+MD&uJ?~MSc;&@#1najFlr_B+~!&-T`bQ z>Dq7qFThQU)VW84=H~axo_J{6X)AKndZ+kB517`C1W~UV0SBqNBmQi1YO{zxfa}DL zZe5vg&GYT|qgw$)Whi0y<-!2SOkSN^HTzR;Jo&Wja)CTofEAz1YsTXU1`|Wx!U|a% z`l6}|H0RPx92Az<$P6VFOMcDGua~1%?zDxKIl3Zjp1~nwnUezPdp6HCoF(xP72ca6 zoG#2)L;f}uSz5cH>&Fav(QCeE62G+uLO9iQ*%p|PoxT-JX0d%blrsmzE#|#4?k8^F zI?RQQ=n+2u*Vd}PbCg}(ncbBY>)GkssvMPadlgb|oqC*Z(8)(=tcA$rIuU>=xA@?=4jJ~B5!0u(ZB@jElg$b)Xe3kk5 zcSeG-6yUc_I$0(l;mp0#g!Dg5H$7<`M7D8lJxL5#>r4^`Ry#(Mht)GKO-ryaU3GoF zMSo)B9>uXLjCmrkPFj(;^wS;AIF$_13GhJuB*)94?%<8h4t9jF z$(_Z;iU$oYIQMW_j7IWy#x)*t{bp9L;dD)(#kB=8s2~BdY*{l^yg&M>Y{`lOnf~O zRV`i#W(rFOh#`y1u1z3!l#c=^6Z|bn>HZ_+kPB<=4j~Q*&E1jZpm?88=eak_q`5Kz zCECXgX3L3aYAz7X+i2EGb!kQ%v4oMFp3y3@-9?(dl*42MSOjs-v%iX`!Q-7ukB?Ke z0F}y7)%%@{w(7N_dfFDSjCFR{fagDd3i=0O!W0(pV<>G?wem`Wu$zVnKTWTSFcj?T zTZBrDEg>&}P>9s7CqB-F5*?&BpsjM4#`PiBw#-LpeBjyP#}H}K+Vzzg)dOqpJ_3^= zSJJRQWos|MeLI`~NkQh;HZ61<<)iEF&B5ZMA`tVnlnhb&{zdQ^DR6JpeZeDZaUWhP+9-H__n|l-X?Ntaa>ur>I8Qh= zUX~xL)L{#YZRF?E(xoD^Ry{9A+uys3(H;$eg|x&#o*xma9bOYtIZ$lsw(dbT5Pyc; zV6_WtWca6QVU(%npU{|Z?s*eH6zHKzWFHj+)JPHv1?tG?v216BW|1+H*)E z+!Te?QO+F+cmBZ$t18yt$%re)j|Y8dBVCKP8%{C56W2awXJL-tU8o&T!AC_fG9r`PYnfl>|^s8*n%eA7wh-W)RVYg|+{7uB$a2LwDKL zI)FTSibZN}XNlqQJN1Jr>a74gpxl2v?wr>_eF}(gd_JItl%H15l}2e?yK^aELbee2 zE8jmrAw?g;;a?G#O*T$mA~?=KLyD@4*%Owz3M^NfgPg&0G8lswG78m78I%e3RGK%f zec1x(`KS>b4Gtv<2+-PVrN6kVtyWQYYf8?6hgT;es_-IG%2?fQ%U19PD7;FhH@37C z38jpSec~Vp=}0Gume0<7@&P+p9jFAavh_`T1pI;c=;3J%5{D1FuopZao`9U^N!Lg{ zdr`3PlJBS0Cy6T8;ydHDH|)E;46GH~DlMhZe_1^9Cok=gft}kGY0!lvR6*-83D`SC zqpX>nN`DBrMgh(Z>|0g}RrpTAr|&;9=~@=+MO!%AUEJ58qt0iBIC+&y_2XqpJ;Qbq zJ?NGQKVfGhJ$I)c%9ug89l)6zn6hmli}W}`y*=s-j-ewlqK(QX>T7m~Cm}-usC*I! zr~H`L9_JR+-vG3#;|BHV5X7@FQ*;#z82H|opx^2MR zV^R;_mfB%2epR!6m#14v^zs6mP`6qy$;N@V)28e2`b?j45p+h%uNQUw1VT|9Rq$2U zOnc#%M0#evgfcqmYap`z<{sYCShP5c+Q!3oQkq4kMG6UW25dL{;Jl z&Gv~FT!2fE(0+9d6#dygNM`5i$N)dI7S;s`rKl&D37;NtBY^|1b3}X7eZ~3xb_4Xv zD^I!1X4Qly#VK>UOSJf9EOU2&o4`)OWn-IE=#`@)z859m{bvqE+BJuXP(@$>^*#>w z2JH2{RNo@u40OPNONS$=?bFmUaA!+VV*b3s>>;H8moaOyqn6nnMWw#@1`UUS2h6}2 zB5EQQna6+nb--(#u7Tl+oCl5YLHJ}LuQCj5w)1M-^o(FOl~<8@(IkHvp1eRR;AJ+S zjCtNgA84BO0THJsR@2qS_)-Iuudn?rHBfK+N#sP9F3wH<@#lw#R6t2yO z6!%%)jk36Vpb_U7lJO`8E*l6sufTEy%dDj0p`U;rz-jFdc6Y5=TRVSFz+XS5oAhGP zph0G*0;!TTv^I#a2`g<(qjj(sQ(TFDJz3^MIqmoY*ilYl z7=VZe@$?MD2kH|6yzuq8$!?*-}V-Bw_=&Yf_ zc%H#5Dt`tG_ujf&u-!!K!j(E z0|5$sUU2_zL&| zsED$B1c3MJr+RK{mSG%3hm8CF!~S>;h1sE@6`A0-`H4R#DoR2hfZy+-Bmh52Mgjo| z2?-biIyxwbZ*x3g?~8oCUt%?6I6(lCKP&WJdH?pCmvCSme~=;AcXK*kkgQGvfc5^! zUjzy$kV1N)Kl83XxR1ZaZ}qgl)Qi8}#4K`{*X{Wi^n<_0?QTKCK7Ry@Gq0irss+)4 zR)9bI3eI=>%c~&V!aTdb+f|Xx;?)8OcOm91{fj<;hhKd+3MJSpU^kY4B7r&o#xwfv zOZwiy0*3}bAjqGW5J7Rkz`s-BXqb~IzbJymmG4`iV%F#Rt||wFp~v)%5YbV9S3JDe zzW0k}v3e1}Um*)st{`8(WK04I0P%taLV)L(Kmdp#;J@`jAiy9yg%0xn_Hq93GX?YT z@GLTa$^g1<_OJJ|z=C}T2);)-K_s|#PE9?=O>>EQ+5gHJb5>jHGDxO>Efi74znT5b zad&K9F2$wX;#gUTaG%iOe7Sv(LCl;) z7C2=i_+vK-c%|4(NZOi*+Kyyc^Sk2^?h!Y=9y{O5pgUg#oZt_@D0s;YCkw>-IaytfnfMh!qt|E$m&bkd#6Ij0whqreEf6Ix;MYnoe zjaU;;T2TD7Xg-K3gIiK2JGE#fVBkm>olm2lNz}HG+9l#pX}BL#@0mq`>yyAmd9rh! zQ-trX`0;FCZ3H6bCePk#au_!3&N6(ENlGkbBOTAGy{F1X^sXZu`Eoo}sDY?2M$3$V z4p>}h|5kDZQ&ROct_6{&x>Pn;lYqFnDpiE-rStZ>_046baRdIleuB4rD2=G(g&)tkVUss z`C$~sGPGbfu3d6kk364agtF%Q5Fs>mCHD7W{$uUzmbjh%^gbjcK?THSIuQsdn-q(& zX9zFjWf5%AN`&53gJKr^nkfIHW$6MAVJye?Lnf{16;W?B8+k2bNo_ln-1+(LP2UCf z^yUdFSTDf42B;uali%-53I6>S7lih0XzPoLxc?j;_tIKFi9b^ncG+?)roE|8%Moi! zM$;ghi$~MIsKmS4g|OR%Zr`o7s1mR&{XB+N_?B5xhPiQebMsgN>k&fG&)3hqWMIZN zsV>V&!8dIonKR7yIhWX)3}vkPDe=NA5stDrp?M9Kq}@N1wwMtmutSMe_*lYH&}!Zt z4ndng1kDf)c@QGAbar`z&%g$vGkAg_%uBIc8^+2eD886qOSMnPCb=&(IowM96kdX$ z&2~G|o9p@Q7kyZXd=8_r8q?*j@_v#!FDM6I>ybv8x5W6I)m=90`~}3;>%#)yit<&a z4mT`y%aQstR9`wqmn%|YokgAUvR*I2(ny<8C-Xz3ZiiD2%^<+ar}u6>y(yn~V=ZNr zE<0VDitkN7hQiyVsJil+)PAnzuQ>9pwMr`FolZw1-1DYpVdOB>geZB)~tDwpW0fN z!q>!&?(yPfz=%%?bEv}iqN`cojO)YrBs7RMLXxNjUykfQf+_a(k>>XN;;Zhfc@>PW z3guiDkn-=1p${GmVwIeFC100u-}Dh7@|bt1Ny}((v%kX%Q-34RGr|Maig|u*2=VRm zc_d2(C@rsJGsxx`0^XlEqovPoICs|QUnTuU-UEtr?WcodlVL1X$#O=k0+%EA&(<>7 zFb9~v;xmb~jAWWi=LB?Lj%ib%dUC1;|KcDPqpPBz9c={j7(U7cJ})ani2_6N;8zGC zwv@|t*?(Z=9UQ*ao<+_F$F;s>g*sxCY! zTyTC@6A!hw1;D#-B>S|R?^uS$w?t&(AlvqN8e3(4?tMo%7qZGdtxY457q6yun`*0!HhGEPne#Ue9Y`0$pnX=i+o&6zp~$m$-L~RMDYHD0azt zMrbG6?U1NcO60t7)5owIRL5I4&Dg$7S=D-bu*mSLU<=vHAG9AS8h8_a>gKNIH9h@F zmW0q1rdDN_v-R*jMXt%;`wBf5?X}9^1U&?_W2R`!0>8dT_SXWc!0%=oUEpKtwd7I3 z*Ndtii?H|V7U^23?8;huFGU8suEtsIplTUpgnSZ?yF_CU!5DdB=LZg=MwBEh(ZkxW zl~7=pOT!S_IrKbwy<`b*Ae>c(FPgP;rTe!8eEq(PhED zA4W9CCCkZWN>0zI;xPR6B^;0{>I8a7;KWy5^p?jd>PI0$V*aj8r8?R0H>}*fb2iF| zJ@JUQ7|-muMf#4{zww?J)R@$OIT9sq)Zf}(JQMEmri)L6?(6MpZ_n6n`35?U6 zJ#KF2uczCEpfG$n3R$~F`2wyfb(g54w$a0A7r+R*WZ%`#e<5dtIXWg%W)$@Sp&3SM zz$_cncl7(1Q7}>R3{dd8qb$);IMr5R#kzhVsHldB!-Ib+s#ol@m2 z4Bw&i2^YUK*$x(E)K!RslwLyLTzk<4@H*3%?NhzzF&bw~@vgcTQr_LQTJfl!>R+of z^~Ui$o8ych9zArAmMm)^OfuwYefmOI*6V8jr_FCF@fcHc#URWydQ9m}qQHHjpj+yR z`A?}2RB-PkOGi=4^}25HbQ7X&@n%e$&F1(;!^?@IVy1W855Uip-?7bPxs)Wnnvv38 z$J8TP-s0xoY*YwL+t*0NmnJZI-fM??YxF79WQgg4o*0Z6*(xiKjv)~Q;s&xhb$J=SB^DrxNm0Dh`l=xVs0L=w5Xg*c%bqCs!2EEQ zll?VWsD@IcSXk%BOMFs(`&f76k|43!MR+RLj+DH)Y20Qkxmx5_MS`yRO}_Ropz4;# z|9-o*ZKQ|@ozyB^j(HdM?J1?HjotYbb-H?DjSIgwhXaq$OwYHM$+aJnJ&m%8!}6cP zMJQm%*>3KYav$gMFHmE1Y}_`?JWtegO%i|4W7C(!!lKF_Z{BAO_r$qS?yWhXugBzF zh=76N_WSN)OPbTw8?vsIv8H7~*XPZNf@W40I|AC3_6!ekZYmH*koF#jFQXXJtqxRl zw0zSKgkWthRIe9KmYw_)KTmqIf#-D^+%HoN16(l?)88bQZCOpDZzlQUT&fq_M_bIj zX_UOs;c5LS5&svTM|dbX2->o{B(?{2ePgO z51gFZ5sf%!ye!bM0n<6F1Yod7?pao`DTRQUYfu0Cr6~F`%B~>p=KSuc)E*0hqO3!+ z%%QQqT)S_HOxmSfLvpD-NXE~palLL0_T)i15t@@$ zsNcV6D)7N3uXMzAF5H8Vn8)Av3S64b6Ag4ykG6al*x1gruP7a&HDh|lJ>VdDV-_|q z2xQfs^=-P^=wL{$%Vdf-ocxdKG6lHwXTC=`%@W;dB2 z{p!*YJ}^No=z1$jJxb$jbBdgp96$6)ZvU$}80H$^G^=+`YOrm?+8m{YpJ%n@OJ=a- z6>(iFWu%QZelt`_<*q~TldyXSf3!|Z@^|NV$>|xl^W%_?TpJC+QE~DLtT(58|HG5Q zE>9Cg8z*SLprpe5SZ7|uk>q*=x8l<|{LFxy)>XWc`dW0|&%NWVidJL&fAuBgl*X3~ zCR3;&P6X<{TXO{3QmQ?x&3N*0D(dky3d+)QpIb1GVe^}H8+ubp3%)S9^Qrr;DhPm% z$r{lrOQs07b4)Wv4Nn(fRt(Qernf04($w61`qMqUCx?5I+Tk9{(7>ag_p_YFIM`p^spNGmhs|Z|I}P% zwA}(nCr<-abuQ066vVwgZF0pd$<=ix*-doPvc4r98M@K+;Y)ALDBJm{<&G>RSo=KM z%qj;j2vW9Mex-~T`d7Ja7AD4=sIt={;QuhQwLZFGU{gntnYldQkahMe%WYA>sBf&A z>V>?)z*CAG=FsP%S6k6xaX&M!Q~aA4<(ox*JW=Odx~8tg)1y zLTkuG6$1jfYbU6DX`Gj>Wz!ESnUvEQ`S0{fBHH@kV&5RvL?=C^*2bP}LO3dnU3u9E zZ$w^|t3OxJhd8q7zowVz=kIxWxHT#;j1(XTb)u_TBuo*;2_YKic~^Z&T66E}bLB>v zC)quonC)67^m*CmarlxH728BA${%w8T_I(689(Bc z`zzG%=p;<|cS&n#L>FJbSf);gVyU9FH9`@5Gbw`nIVBkL+U?p$a9YVB7xpK}px=s- zAiVJup1sE)qveREeCC zjU|NQIfdxEOin=Q$fWjeJry`F1v!FMx;;xJ$3UWuJqwV`(`><?967X%ie8=A6HBgLe&TQhuGtNbAj6 z*G^jy63*|SK|<;&%v_CgpcxQprYW#H(2$A_>eH+E74I9t4lGJ|#`h}UG2pp`R*C#z zq*xzJR@lRVPVA>_egbKdA*}VHLz~KOj5OMPpZnT3 z%KAY(HA>WBw@Ughs|L)wU2AU4VyGC?MLopGOdP}350;nN%SCue16~o=0O_q<)z@(b z5ElA`Rn0{ti%Ih4|T(Wkh4->Ebj}6r+jKa09|Harj1c?%DS+s1tvR~P@ZQHhO+qP}n zwr$(CtNKlTL`U==^z7bA4l)NBarRkzB{*gV-qBmWl~`14sTuJ#HsP??^ZKv4zDS-F zYamqu&tbQ$+8Sl=};s(RhluLA1?HS2OQb4le=jON=!G1cvQIr{=FTBEcf2j zZ@^bUzOU$EY^%vVWY(UXqw<=J1lYa3NEE-EScb5>2M!+We$3KTVfX1lB5$->)62gw zUR9qjjS-3XbkX`ofcg<{X!V{x?uad9J+4WxZ1qCndHuCw)b1Sk{Fca974-OXlxt6Q zSb2n}18BH^CvL^tQ!R(^d_#s4yIcRqvwhLg@fBZW7X8F@WhxI^W_EBNKmxVhIR3V8 z#O-1y=9Hz8cEPO8wDIj*^9gD5;_38X5n|MYCuX?!j?L{py(repVYWLZyEI9y>lXTM z*Tk%Tc5Tox8+PuecJV{YSc(2T7GH8qhoK9ggLQAH2Xb)zzUC?xno>n)n-`WIOam0|r7Q}%hmol@mioZQpbrjp8mjo{;pss0D6ZfU~p` zPKVz@1r>XZ>MkvnR2=Ee?Zi!ZVzK&y5p#}i5BJWoB62XiWlhC!3G~T?ZtRFjHG;+_ zAt>gvTZ>Lc6DvRoQKC-_^W-h0hX+uJ) z;Jl&cPUCej@5yJdzZdmljH~Iq)?fc?G90bvfc$hq+(YYRgB+9EY)bR*V~nlUP14X8 zx~g8mrcT-(r;y)m&iDy}gSjqnby+&Dv2UZM21-KNjDbx1 zQuVLf_=GOwH9ck;&XC44SQqF8bJ=jgB8O?q?j_fek6lMz<1oCQZEN|0OnK|8KDw8zbF+f-(j?dIma1#{XRZ zcWy?{NYDEJ?X-`60hPmETLFavcZIEq7PNDPxVfo;Wm<@qoYU*q2104&@lafQ6O zx%n8I+Tv{A{Z;K&RpPJhUTtw);emw>t^jLHBObygg9YqlXl$&51RzRcI$mQ3u(Hac zva-S+V`9p{Q}x{Qy&7ZM;4?-0144BNE;xW;cJg76$mHmaPr=^@;Lhp^z)9+tE$Wx8 z>K6^$*FQ4yi%T%14uEHV0@naSRu6E5ua^hS5DhXkKZ#*vefXhp%8Lv5gbD-T;^U)J z(mMcX0LNz<7mR_PXLMo#{10g`(>H;i^HcNltI_#Q4A2=HSzea+OI{uv3>=>74+cH3 zq8{i2xdUk509f*;;WKs3Bi?%*12AR;{}-6m<1GR(S@Y5Oax&qm)ciG>;p>a+|7!#Y z(%BW%=1=WEB zPY17#xev++9;8f+vZ2kRg8^`=FQqr!-+OLekQD+@~5tQwfCvFCQVsbK~+~e^*%TL z_YxT`)D5UBo!uQ^3VZ7cz{Q0{27s0otMAqKu`I*?=RELwSBP^zOI#0^nCin>denYbtXz8+9b`8V=Sw;}C2 zQYY=?w;(kO^;cL+i}uXe|JV38Cu8{mehf|z^aqd~pi1R;0IhTx_pTM`3H-g-@RD~= zl0MT{((zxyFPfQ}daXMWc|H4<%6|3ZM;o~I3#dzC|5lis+Vd;++{rwKdsoan>TCJf zm4`Mj_=BGGUCeptN%`>Hvdj4Tt93fsT(@J{l5sI!I_PZlalYNsJ&#T zyl=Ip7!Xe&8hEoZ{8S);)|7#nHWR~P+-a<#>}_)$vjjAMoLPz>wp*8hh=Xiq*&7K> zhc-xB32asCUfH2?EU%sJ*RG;cy%z{T?@TH)_o}8=)4fFMgKuB7k+<1ekTo=)rP=#a zR@_FNFS`Gt*^;8)rDw^o`g-pqBNS9qcGJ|ei{w?Z>+%0H0mlg8?HwKp1;g2(er{<| z=-{)^uM>z~JG{8O(Zwryys}hV`UQGcd)9|?D53#+!c_&ad)>*=7q>*cX&`m8Wi*zALfMahG=Q!6;hGn8ZNn9m=8qr&vm5_ zZP=MW3u3e$2LJhdqh`rgH8^%l=|LRcc_+P0R2_y=JZ8Bw&$WDA)pAMSVLa}M&#r`4 zIU)a8!uFc3(CQ`P=r-Er#Gst>p?JA!anri2lZ;L3_}eqO`T;yj0DUX*AQu?AzZ}Y7 zex}%?5=h(6mqTUQv~vHIi>#h-4!9YA4hBSS*Q-%*y3cf-&cI4PRG95hq{>22cf})t zXEd2?78SYS<>W6-DI?zF-D}9$#Yq~Lq+CtD>6I6dH;q!i$Gv}-LSRdx$rI!u3j-iq zP6I?u-qsA)+zeb8oW`1R7W*BDn1k4<|ePXtDEdc&In?=X!IU8MlKb*06M{tWApghAwEO*T7k@dZ5T${R}v-8VP4-N zsLMm9$vtsUk!>`5RZ&4{&KxAHgO^rA=M3kZJM>^_E-F{?VEVT%zwqaQWf+e-@T!xw zMeXYJtH^oM`GVV96h7d*P^j7DJqCY9WPi(g(ke+EqtG&$&2g3+CMX!FF6$(lWVCTX zS7t90;e`+)lkjQqcE_3=g)fI6?8Rmu@hW>oTXQ8zX@X)W%<(UWrMQ;cQ}cx5aJ^rh zEWC0LJ-vDlAg%=HCr>GIjmchwk0-9YBqVE}6u-kpJ;|?g6GcEBeDd-Ysz>HQNXr~y zJ{QVS6riH-Z9?%iO0$YQ9=D0VP0Ss5fd__3zPPX<8i3@@z*)!{M=~SHm}IIMP%WYM zH}menaVFU4l|FV-W3|UKHl#r-7sn>b{5)v;QeXsb!ktMWq~;$+;Ed~R+OCq%qNqHv zHPH2FL*9&>f<% z^biY0i^>+Jyuv&{p1l>g3!acM%YMV1NEHJx9*z4$F<^IbvogYX)Qq}3QTR|`&%yo^ zG9dCx(&20%Ao87!I@ezilR{br1sZ6lg zlQy{@liiAW?o3-b;iK!8Nmg?yBWR|iKVj1@ab6)+VIzN| zeXXtPt$R^WymYBwad;J_O7Lu?Wt)}x0b6N(U)p;dMZczojR^ImLVK031k;H^vz8wE z3ulr897Kk(Wa7}HE%op`@S&(A?7c~$hmf3`6Dv|tB?|jR9#D?m>04bP(#kj=D)6#I z<}!uV@Vr{4R>i33S=?T0T7;m3JP5z`FX%&s_r5ohLOHkY8R4Ot=05GT?yfmva?4(Z z$PD{*bk&qDUfFxzA|0HQoK4RfUg2nF@{-hQ`ciEFz-qG$0^1;%k9maLIU`bD7=_2~-sxLQQ@Gtb>*jPN^SO7G0rH-}RTM zv#c0(k=_oW^)Zw$2cBYs{0)x-BLD8|^9WdWelWrw;(YJ-;Y(IcNz9V0T>}iEe>*lH zO>rwFz1R|j9UxWdT|QZ?3s|^tn5$tz;lG{$gaVq09fwsW+|S#AnL?ENZCQng*L2TU zz0=q<<0_c*^o#I`wu89?2a&BLT#amV(Bpmfx8k&$TjV>_!|%lII@S5oI&Rpoy#bVC zdS9CJep!neiX`BE+NVb(ip{T6G&)6sA)UmYd0ee};uUx;+C-vL;kQ^44Pm&$DO&vxdx-?xpC`pS6;&pn2Kgprgjai$faF`;(nbNnwk8^)yUL=fPIV zP>4mdUEv<)@;<&AGGFXq^}s?P33G12pLh&*FOq~p*Zo??Xn$trcqj3W z$WL@cc&Ra*Z)K$g z@ZK{aL>|t%0&kn6quS15EQNK_=u=00vf)?-S!zi+igjStKIPU&{7+Qyn)BAYH*KA& z*~8P5X7Bn}Kn?@YW`@I9F{B`dqz3A+$fmt-k>T^|n6ehn^RZ7{N9Y(E%rHiUMmvyiEHop={b zXOW~VyYLX4wd6SSRU%E!2iWdI(|t|-rk+f<8;W%f^bA>$R2vf+vcA8*=mZm`yPMwG zrHhk)4tDUDa}A1`A0O%FnW}2VHl12b1>r)91FHa+($;tP=atr}Sz_i>b5sK!Bg;wA zciw;7 z=7URlTSnjzQ6AWNne(V2q*wwm>(er~8o#PRe9`rU|TYJ3nY%$Y#d9MrOR zuNB625EMUUEwkxCcO;JYuVse+Mcj0`%U%(^R!AaYL+T6*@*gW{OYYY-n69jh+qQsz zm57wUhv~;YNdC#4vdl`MR9Jx^+eu-_B7lk+NP zJO5tVfJ_s!d2F!9@-n$IBU&^D!y`T8dU8jMvw;D8>8Y4Kjs8Lw4j^G($^E5rN?{5N zHSCsra*n9Pu*$kB?o$WF%xzf&SmW$OrQpJJ1fd9Dc^sPKx*@RK6^;~LzQRf^<}`Cw zII%are-#fy2|rolS=CG&mF#i4|YxwM|ML{bAFe z1g3I!dlrc>g%_Bl_A;07&d@HNY+W#up$x2DZLm*i6vm=rqch-BTg5am#4k-4gZS>9 zr2g<2Diva}Xy5OCi-pqKE^Wi~G*V-JjCc3d&N_XRjp)Z@t~a+UHp=5=(0{w;p*ZQA z$N2FEF?s&F8N}G!#f69n_hAD3IRXvTs3LEpvi3G;z~2TZ4_xfTr^~=MqaZa?lCS%= zRTCClH0G}67c2+P^vmIGgD7w*B+%oz2zOr@;+q5kSwoEmJiQSaH03kqqy?#nc#uWi zf-2?by$Ht1Hr8l?L?8wi)Tld|12I1aP_nM;~|03dAcK-;mg|UKTlf4WoTS zYp30X$8@hbH-v1m0r*?HKEdav7}Wi)!(mahWEx=&bLylvcINb95gOM{4=-FbKrFB# z*3t+D1au}B&tQiBZ(hLF($Et-qmTj?w~UXvgf4S4U6>|;QZv1Z9|xJgVegC+hJ#uU zXecXR=RhqJ{2nN-*M)a5fZymBUI1S(kh2*eKr&ad=PqrJbVH2qp^uLq??Zj$$cskx zGhbeO4|JQ{FG9I)$*|(LaA+>jW-6)I1wfg>7uq7>EB8-EGF{8q zME%{KNV46dYR}&C0(S7Rz=;8uRrh&rucJPR;4*RK64WL-n)j{U`mLg->-VGO4j3I> z8$*iCvrS6y#M249+Zx(IBNX;G%azV6*Ru%WmI~And$?S~`!mnNDE#o8`!3V16dh!t z`FP$i-0QGI+UcApwBSUzm^l@7DbU}oZ0H$|H|x^7$v<4CXXhk;+NB#1g=a;yfqnXr zM^-tFw>#lp*fPjVF3P!c&;_5^+Ti{~jYqQ&Ug7tDKl}~oD>R`!9+*amJ883-`+!|O zNc-r+t|8NKE~}tq2yGlbPWjaf_kNg5{g?`OPasz)%bf>@wx>wzrOLS7IisXD8 z`q<93X5jK$Mh`-il@;|GXzM5m%r_s z!Z3*UOJ}1^2C^OEBSv)tzVM(;cgU@!$aD4MKD?X>1vPQIl{$V-Wb8^(;8&Gws$exq zk{`XL`_f%^NF(3pDX&td>x-mRXwF;7_ZXbrjIbPub5MD(9QN9wwYRQ&?@v#Wzk3!s`sE@-_gq+uoe}z~S+bNUEz;cV3@n{e=E=B* zLwkFAz>$3Q(2@_%zepVFpG6?^6?Y5K^077GXSZ_KkGnlOHVWoAYJAeR9$LIq;PHAf z@7;U>iC!;))*$Eqp1$Uq%tx50eSC1? zbxsqc)rrxgKh7bw?iY~PmEEDnb`Rc@s(!mRD5TTL3kC~OK_DJsI9`h?Vrm^?@BVB) z^#}l^#K`R;inejR`X~zV5%J#?Eoh;&iRIs2noVvaZy@?(^yo9+J#=34tzlE1*(Uuk z4O}bJ{{{B?>H5yF?r2IA%vdTjn;90;(RBm24o620GvR`PUOQp@8bUi%#4h55@!=j?R(k{sI*uGj}fbJjp zi0UMbd8F|+Rd>%*&Y*nl)g8`LwVh-XZ7op*MLh3v?Er9A#8kjy8fV{^)=J%8G*^&k zsOKy#cG^j*S>0G;vWph1zzh63Grss7m zW%jGZ@COU!k56&e)1X3X`9@~irS+d`6?{p3c+MK`Yt>~F(4_bBTZMud)>z{N?FodE;m zb~OaxdY6+YqNdzfkFc(u%4l}G0mt(Sb@e=k$Bkf#9!emb89RIxHa9W}u#~wAepnfY z?ro#kbFLS+#o~u1x}A;SKBBF@wV?L7gOy*M%jb!!YIzrs&}dJhl-#&t<(R4oQw#RO z6wv6{#0e&v5$>}a58e*r-d6{%NiLgT;}h)zfBrj zAcKcqAYBCaHqoo2V;$wf=hyL$@S1_N|)uc-B($w&z67!ODB zd`D`wZXv^`n_hHod3tb}MoXU8Qt&^FkyScY4%)5;KwWBS>GDtLWM-u=b_6!6%wlGE z!@Zl7Eh!B1iZ}2-8=}shu)R=5=03^?y9~0Q*xx!rwrWVgODWto2T^t)A@1J>W-!r_-nUHYzgZ~;W;YmK^8G$$U% z2oFLc~~d-9fG!pV5dFwMd7@JGUV7F z;%HEfc<*2FAf`(@`N4NgD|3t8nqclj*8?rYpY$#onVMzwdKa2w)E?2+TkL?w$tm|9 z!+Zr^rjhL8*}FTcdPTBj9y}6-9;F7op=5@o6^Z9;_g%-9u1ZaWKet9Cyvz(d)>ALA z!fw{y0cIO3U?ZQrZl~NzZxM$NN^?t$)5E z&F7ELjVM~atq3%oe2SV z5N#$4tXkyJ5_{+|G5!id!Tn>_P&oY=cMRRpR!{FsID|D#&>L)UcGidbW0+9KFARmj z)y1@*?$VSBb0kM7rkPIFE^61tqr;o1xq(m+MW6bJJE?Nbo?4oMu?(zk;!DIQl39cG zZFEVFjycO~pky$4{_>k3KfZ8^r^~uj+>;)A-k|}eDdKceVLIA1%WG$nzODVWX8lt- z@tI}>D@$fwGOEOZZ2;XjwwPpYsZV@X6F%(sd|64XTvi^fdn4au$YN{0F_Djv%g%>V zrDSb8n`eUvYAFF{7q&Ifw6d@k?SptW8q0&aK!*)>EoQ zUq$iLx;Q$SOXev3J_jVq+{2NbA+@!lSh$GUI)His_|`aip{q{7m5%^ROAd+24Khbg z7t7EgbCrLzO>xtWD|k)v-b|+!-Rt9YYogcx>f)bpkpQ18IZH+HF=NM$?rk!9uY7lP zNjwF9ua6qgkbCK#Zy<~WPMlEnLC@tMp@KL%TvWv36!~v}%3~4Mn(?nt^*GB%yx&!w zAW;|X92z6=yJ#(w`M{gf;}c?~&#lYo&TIK9Md^uSLa~!AB5P&1C1eS9xhphbI@zox zH&nE`;nMf7nMQD4z}^{bqMXr|R%!eGGl-3flnHq)))ksH0iwlA1aFO`)0QeztDK+5i2?!o;x||LNRdFQhP4(x9WN9}d!KJDA2CviHR?s14Zac0z)PQpfVw0u@{wX=>Aa@cUsp#gj@#+Th>^~9@$ucGy zC2cF#2i$BiJg#{1;dlMLS2~HXQxFH?mFq%V)+NSepRh>S7 z*kGDJ?N8@wZ%WU4_?;=t)G>Bk#=ie$c+<5jo6XDAc-8g(sK+i!X8(jQXL8rG(* zJ(soowU3@qT{Y8;j7P5#c~bj?Tyz8sjJ=~uCP4??|Jc;Jjhbi}7UTHi6t{f)n)7!kS00E$0iWY->Rv6d;LJ5X3^Rt>IF0?4N=a^$%v^l{igONbXe zAC!&aTDVTP{ha>td^t;QR@Kk()@<2uAn+2nXVYQUHbxCn8(}#NJ?_1+p?E(_s6D)x z1<4&5waI5nySN^6-(950LYr4D)mJ3RY+8uNV-tto<%WWv#&vojRR6?c+V;!RbUvQr z_FJVcCE`wRiOBW=gR-l11j}&7GuzF52h25Lml@QRYs>?tko%y{IZjp z>etMS{HN@BSB~USl(6f9rpU1B@gs|8AB#2b@>#F;`GLs!sRlcsL2yL6k{wM7lA;PR zBryI}c5k7Ft0+ENe3%ZHsbzAC+Z&G-;8qXhiy)qPBkxg|`huK?n+ErKEN@LYougEe z^j}B5s;tVM#G`dBKqXzuBhV8`xjN4l2m&y97Vd&qn$2O-eYoh1C~nQSzY%6tUsb!R zKK<85y!+I<&?=>98^#5TXZUjc>GJu|^~>e-X(ZfKK^1NzClavc0982Z)8Y50b(BL{6!u}~f+>c~fcWB&2 z&gvdd2D|dvu$m^jVfGsshzqXnWkIUUA#nvm9Ho=PZR8#<3DI$TOXl zIV%!q0M6#r-9h+ca2UF-H(@M1HtPt`bZ@bJ^H&05&pe=LFLh<#`r7*ANHK87&#HR> z1l2HgYj+feO9i<8P4U{|A_Qe^a}zgl&$z@4yexM&gFw10Kq60z7#z(!YpyVe4yl}l zw*hsurBh)l)e9;bhPxyG9hrZtL6}9j@hbD2WK3q|H};!N;GYW_hAI@?7MO{KmbzJi zhe}h|G|Y>8uS@u%3a3_n*CK>q=3}E{l=0d5^x=t>4T8Gd*VlBpxb|% zBdKQBSf+#-99^eGy8^KZ=+;EdX&2)XJo=(i^JKQ0-Im@8lRC>Bj~$TRg%$S<;#IlY zt1>cUD;`A7Hak4{xY6We+2=ML-R9Ig)xHGoyH*Fp#0K?1WKHp#L0Be>HU+rE1O0rD z{N|b^#0O_jbgQ&7$TjJ`vTfpJUO3yg`0q8~&Au7UWA;yc+JILo~lvF-b{wm^u%Dup}(!fwP|i)&~(DP`30W zsEzgXKYV~VIzGY7i$;q&7f8X<_np3XmEe9k7eQT%s+mD6@p`gZQX)*eB)n#Mç znZ9d;B&=@GFVU`=Arl-vanR6kd_m;7?ALkZOB02uRv@D(hq@iq7YRMj^CJ~aA?%E6qFkDBpC_#V#CKc>>XzFxJkr$u7`kf<;!*|S*#LOFQ$~4_ClOZhK&0lwpsr2g zmz^@WAS==-V;Cl%%J|B&8Ql_$x6{Hp5uMP12&>b!>7Os=@j#OX#tD_qx^9a5R)KU+ zn}^Q+d2%imMM`pjpco`5?Xd*1%x(-B;tzK<)e0O-u;h3rWO0p`8GZa$;TcxdV)7`< z$#REK{<`G^=mt-f45 zopZ0k3}h5H(U?Im90Hsu;u#e85;lZ|h`_sFHqgye?HX$eJ48A38hrf(_yzi~YwpTZ z+`l{@Yz7mUnbL(Ex(HOUlij%kiUH|org3yq;DYU<2C=6-#Br`ye-_~ z&j;E!6A_Y4dVP~SkZYy=$iXDl`gF-I6n@iry%Z;(r` zHL2v0aT*ptG;}bsxBBXRu#A@`J0o*)Hckrs8VI~;V5u6IFCcHr9twcRoP16pM}S?! zw*N6ptn_!oS(wy*Bwxbm>z5MJizOuRfjk>ftZEa`eESt3oX7i=>7-;`xj~1s#{0tP zr$-4SJhmB<80twnM_~J%2FJIJoY7xgo*TQ;sF8FGjbO0as);?@uCKu>KFXc`&02h; zgr{M}rjA;U$L95`8m90CT5z1pSqA!BCio;;d$>70WVyAp?T zku{Qxu8@P8deKMebVjJ2s{s+Q!Lj;07OZ4a(PsM?D54%Bgkh;S9xAE1+TqXn=8k4RIF{sE}^)>hXS_c+z2JAai5Z+oCbtb z!Lkh$Y^Z4dI;4hsl>)jCnHN4vgi2@)4C5Ex=J&sql+y6{plw=nB(y-27Endv3}bC zX(>lrJ%DBT5Dr({4gyUug+}KT>tfX^;c{E_Fh~Iv6(C9Y_fN4eA^8a1iiN@m7bp4) zeq1YL_idpdad8@9n+=D>JTHd z$rDM7TOaN(^`MlfBN=3^VxPylL5!Q$>_!Y%bw4vt2OYC$hhBy z(K}7sqFwG=R%lAO3Q;yb%+WQ>JANm&*5x|C`_5l&V!vmqwiZbTJdi@S7I&GP|MtG2GX%%D67p!MyGx97{g z*i?+<(W&$C7;j@Ux0i<#d8n$WDmC**Duy_l)XVK^i$u=vMN6S_;weK?L~iDkXM}L` zc>n2{NT7%cIn86HiysG7Pj$g)MpNGpJ){KN}-dfz{Donbr7PhzLR?0VD%CmQ|fGNG6r#!l5 z$0?xHEU$HKg<3{g1Z_iJVljftT3oJzj#u9fiy_&65%JSp%X1dL373lqP`R-fYjgPk z?4YH=M-ZzsgxBk@-ehdx$Hm|s!6D}n{NsDFDa_=pTUO;F)KL*t<>dUox`iQ+klsAR z0&=@1i8{OZT?Vl~=eHljq&OMtkOy2e1tXb(y9@?(iqJ%n-SB#>4^-LDkQ4^;PsTCl zOu%ktgQPcNhv)9e>j(RpWbFQ?GPJM*R({OEhNzq%&!S47!R@H|IN@)$w>2!wV-7%8 z-dm{Jav{b@WAI+}M)XSxpr2 zcvB8V=vNs&B;lWD-MaaP$-DYZfR<=L-X)Wd-nfYn?FHIR8a-+127EEEiQWa~clYMM zg-fY94DD%A$pYO);2C7~6wrdFI(3Lw>FkGRZxz(=AsRj&S zv`%K9B+zT?iSUjArq=6CEmmoG|4bhpP4mLL*a1^mig0U?Ud^Jj0Ssh;=%rjTmmRjF zBo)ytC}kb6wO}YNDc}vGQt#xrJO;82PK0_S<$)AKIxOUSI;(Ecan!>-BcagEH?bAD9ygUA$T!Q`)b;us z6D{A78-(!dAm*fOf*i(^Fn*S;ei*xW{>?c;3$KAxF4?#REzjeZE3+d8LOu%(z%#-f zk3nU71q6!_7VoFqeI?+CYTB{-G5Yi2#EuOob`!`>t&&2(j&QUutOAmo&!>VogACZPb5o6K%(H|1a{xNdMoEA7)n8|1drb zc#QPy^#8g2Z{mmPKfn(j6s?H4m6Ndp9<7L#zLT+#v7xPzF%%CEl%tb_vA#8w+eWk! zBwLd8E1J8ZL_?{9EPiR1(h2aTC4jrQj{R&e`m=5*IRX9tqQbS_%YEQ9M zITb##xcb8D+|SSN>a+K%*6P&P%zL(DuH(&ad$DVV=D0ZmxlG>Q;HkL5vBG5l93)Fi z7*xJOl%shwDgliROoKLm-YbZ6LcC}=`7w)LdM7iy9KcPddzdsc0es*PDOP|&06jYk zbYo^F%)Wy83f?f}49vX9*Pt-Ja4tPD{6MFmCb-}W>A);)^gDLmA0V-TzW{|56;z#= zaAxg+OksYcz$9)V&}VSDVtt)}D#$<}3|+rs{z|U;bY&J~$dSVdqn(S#f)o<@ME zLw0~v{2XGBAmM!ylYZnoIA1#%TmqPNF8*h`*eb|~fx)Hz09JN^5P0cup>*RyabSI= zz$#!Pei$f3zJyr5gkwOvp}=}a^t_ASu{z=)@v4FMAV9;}5u~1iMy7rs?f!o0IrUtF zk@(Pi<3lI}JJB-!hxa*dW3aa%NGg(}z#bZ?0Do`pJbj&jU<(+|9-PLki$#|tFx{p? z$AoYqIyuEm<`5{K&jpy`0A{zbp1&Qm$C3YiC2#_MBLeecSc1fe27JN4QgeK-oZu|@ zKI>WhV0l3zh04gt0CT_q-4HZo$-q_J<$D!KjRql}cdx|?WdM*iz)zuKcwd2c#fRMd ze*A_3KRvyiKSB^NV0Z!`V0$1Of<{BNS9KUf-h+4Fi+Hqse_{ zqzV8kb|ZpIp9=M6Z=v{nbYr>ua@(cI>umS|-X%}q%!ru)e+Is04Rm4Of0=p`j(aD* zc2Umhx3^Tj$83Xs4@Wx%ZFY7s>TJ?s+`y&C?nvT(rJF%}scRs`g3@k&Uoh$J?r6;7 zv$uWV5DPB(b@1k~4gP4UG~Z8KH8z;q{J~%}NU;yV6&>;_lBZ9spPU4s3)2-XG-s(i1R#+krQe4Su$9frS1|X7 zQZ+&mNKS*Y#8wQ0@BB+>f(^j<3#oj7=Zm%oC@;$gUl~C7Eu5}SPJYk!4-fDM>_EOv zFCG|d-dHa`Tgn3x#Q?FKe!5&(Fa4g=(=MKr{#Sq+TlOl&m!S*@Ni-NQYNbL*=o@ft z&p*KyDB_=OZRCNUJw^9^;#|k(mWHE{%=!qgX2$(St`@=2A?{r@kc+ZeU%58ad#%a> zMDpMW*oXpcS(rENa5t-m2+q7S?hJ?xk^gS(b4xZkw)=D@B>jwd(9|pO@Fxa z{0YHKG+F{+Q^|mJF;b7h_hG4FYNE?@QCr4zlZ1XNjeet@x&4$X&b9uRz{Zsnq=|md z>}y)s$;Vf8%SR)$?h^e+cbW`B$)(tF94Jff>g%j+rc`&kRr(H-4FB8t2lMpnY3*4n zjd)MwFM2C{;#Kj<(jXlDx#r2mM#b~?E&Ws7X)3N)%{GZ;DVC+)Twb-=UqGFe^jOAD ziVNLh>K?up&+Zc!4%AqZ?oIpsv(l%ho=URL?slZrSRT8xGcip1s(k>zs5@tCYa-}>PP`RO7#JV!Ca8=P3o(w|6re6D|*V2cZa6B@Nz!!$$GInNyVNKB~f7I?qoLZ zP8PD<90u$&11f^}>HSmMh~6eH;wDU~qK)UkGe!#jll)rhl-A?8EWuhX4}o+=ZaTE* zQ?;ixdGbxGksswGy&sfkv`zeI zJ8kcy`|Q2Xn4kX$Wv^kN6|S!Z#uBcaSzxzN!su(l(LmgYUFm+Bab*$GKHgg+(fEIt zo!SOdorbv|3z7*_429Mq4n`HTWcbDm@kAOMl^{ON(htINqNIy#mcJKJ;0od*`bVaKshavjEpi- zF!Y+8h$bMf;GpPqM6^mkXpbp<8Y)hdB&nq;xH#$gfLUyD+d@<)Dz83{n;X~4R6cbd zL%FC`P2}YLcF5e%>TcN$fcqgYR%}q=>YB@}IqL=O8BJJ0_vYO$d-rh=Fp0_m& z!JLL2+ve9GP8z=?jTFl{0Zw`>GmN=3N;2Tq)HUxFbkwE2B)?y5-7p>6M_ihWux>SI z@I(ZsEiCrV4wmd%=?c$J)5!91R#{4}dG@o+_ryyf-y7%6v|Jiwl+QQIrY3jQ-`6l5 zgruiBRMCLdQ+EUZ4KeX841O#}+le6{S{eSUhYm|BY~^l|*!m5%BIf%)ja_$86U??( zP?WCpD#1dP5+D>qkqAM0l@Efl!2?ASluaAe~5+jue4_3QAQzYLFh9AOZq{ zR4Kmr-u-6o%=>2Uo!LM3?4H^E&Ccwc-QU?g2W~){!Ew4v(EUg{SvTgqViCoxf(%yE=tGi&D|^3)x;t7v*R^$_p}VTdYT->=s3=qk?7D5{0p?Y_O5kh z=WF%YK84dGgqwmbp0^-Vs-3n1IvWMtbKMtdy(}n&{>72yV)PM<;VEs7i{eIbamU@1 zM@o@>fT@mS(^)R{d!#pa>&i?!(%j6G*CT#RqSO(qx7*Se+p$x{E2i;ZZ_hJ}5Y)s4 zzJLcdSh@8TcxGea%{>9N$3mlQX(R5&Ht6ts?uw}s=pjD8S8JX#!jXqN<&xHmuC1!os zh415C3*kix_#YFc5nUNzA^YiCAvc6B<#cL8R_(4uJ~-#~sgTvS-PZiG-Z3!<`UbjL z&0n!Kt)8=`@?KQ6p#H34x8uE&9Z+#h?}Qux`N?;r@BDI_g5hAm|cK1r6*G#s0#YMO3!eANy2$|W@B9rr$(V^_pi$@i_b z@uN!d?8ZUY*B}K-M&8w(t78ppt~E}Z;j!K=nf5WWo@^kfrL1%LOks~f*}(;n^8C-y zI*_t)l@Dnd)=|W{p!>YVW4h$)0C3eqt?1em6q(F4fodqB2Bz)Q>6&za$awifx^&-) zkZe4QztHO+mT}ymDE*XEV^Jy9NE-I^aV_1OfohV&O0xUeh~PX2R6$a_pJvi(B1|;j zw8_&*#1b#_m%_Le%SD|K@mjd#eki=hYGSADLPXmA41b6qce_-;Y+;esF#j+#1A2|W z+!{7O#vbpNHPJ8+M8T6C*cEp3-B0Z4C8|M{Eoh1kez_%wc>o5b(W?>mUG|#H>XzIm zQgYkX($asf2$M4F0%xo?+GZ)6Fby}$S5-ooAwj60M6)aD-jwGBLI^6qN)QFW=Doff zluYh54DAe}d>vV`Ggq8&n*EwIxbkk}RtVF$xdnptDXgI+^r#q!kjI zu}f*ptBTAsHP1aB&9yqaIX271@esZYvx}zYuXrQ$J`9gtOh?$AjslbXG`nl{qc0e8 zu<0AUzEG-+JCq0O6}mhyiZD1*=KICXDr&MC#CfMY?n`e>fZpM|w?o+T-LU8QJn z?J_A=MPr!8#?AUAIwua6k@KFgmx#67O{UY0-e&)}U-5J>)$7~+Z?w<7N7cy1?x)s3 z0~1!Tig~TiG5Nu17ua!Es$fDC5s2i^A~oG2q#A1B>K2ajQQf8?$(MEc^{Uis)FUi4 zcC{W=M@4m%s$jFTkz5mX{9}*W(SI!z2>jARs545nGLxA;B)^fY%N!ZT!dy+WxRjO% zF)Yg1(NI!uNZ*S^C$qAY>?Job-xWRlQF*#~H^I5IG4op7bp3h03PRO)=gD8II3y1> z5u6tDWu#x+wtSdn9y+ofOA4@Jf+Bim206%r!K15_dBbcSXqNA60!K*q06W#lOSY-l zw=ZOjI_dWf+-^3nnG=nfx-wPO z`&*ya>$c7+RGoe;xti^vvuAb`oa={dcSWO@4#vkCDj(Zj3^wycm6ru{b0U064oYRx+)lD*6;d6M{{ocNTo@xq52@2wis zq}IK*xxSd#k-VRcclKYnKCPW`9Wu4= z`^j|qDCB3<4$|Ip%I@YRj^XE)pv|;oH_{8+=ERq{@yKK4y>U4iUknW!FU8Yc=xREs zwL{D@%l;h3j!~x+U%Tinplg6>*?pAP`n_D$c)a9Gyzymbp(|YT@+}%bg)O1JMKh*< zU@{c`jma>}R7OI~+r`xaVJ!ueR*;pZKEh{^xkIHS{4mrWYV+SB3ge|kB`yGB zTDRn6<$$tEvMN9jNI?N4DJv%`D=SLXGsL+3Clw2wI)zr$O|A)@IXl-DD4^ zm&xeK*h!Z&uo;Lzd~)mq7RavH0G_u+&?OWS<)y?k{78;w@~LRm8eP5%Dv5ctA{pB} zk{|0$;!(w^j}Mf*kBpo{lwyI0)2}%icAD+J#o*d5|$!cM4xf8z{Bj>B01|DR2 zU9j*YSHk?FMaFPQ%6ge#VP&y9%aZSReY|*!eX<4KomYcwHEJTcPPc)Zc*(mx{3LyT zkqDK7_Ddnl6AdlwI7ub;S2Ib`;2Mb^x%bsO;AMm~|L3&`qh;d(1Uq+Tk1tp#eU4ke zzHs&OGu@SvQdd4ygOQZ|qHKH@$FC;m{?yU3>xraiRbvFwGb8+nj`q3R1zah;W%k-) z5{5E2*cp4vX4Vo@i@Ju^dSc3$if~Dc#;j*;5J3_M_KsNYqOOjdZ<+etHD2Bd*Z(T5 zh8?Kk#cLdGc5ZjJa|QE>ItbRzOKQ}>Qnkgk$G?Co+XRJU_=SSLIZIc_i(S3i82^ET z_syuyhXQd_HI1dXU_X2Q+s{cd9Xz%+gwn=${hTW(Xu(R-P)$f`b;Nq|-Y@XOB{~NjKNu+-knYFPSvC>f^xEaU~tzkxa({f8#`rBzIU|Q?4+6+G>_Q^4U`wfr1zbHPmvzqPzFLA(GRdSrUfB5KkJLW)2X#27d zGh=A?=C@l9%K_ZpMRXnWFw2;3=N*xTC_XB8 z;0iHYI~Y;N?>3yUQT=i&1S47cncuNGhXDt5osDOc&k@w#IfO5!6QM8O2n7TSMWYOY zbYB))U0jXx!nDxq2)R-C!-v@Ku4+v0#t1L$<((VxKBL-antEm@>0x$Uu{OaNnaM$X zg_3J}7*RezZ`TO^S#q-JX(EZW2E3BzR_$gg_S+vpl=L{mo;m#J$ zS2NWB<)zOj;Rb%>}c5AoisJn!ObsV#LXJMV@H>DFFbFaDmS94m-M*_CBLKX9^ zAKmAQ@9XUjHLd&9I^R%|dbFD=L#({9l+aeZ9=`o#**N9auV}@*0i=9M_>R@%UV3nX z+={%&6@4OQ5}w^Pgp*va(8xMr#4oW3{e#s9{Xa8jZH91VkkR#WK?DL|ved8Ya0VH3 z)B^;y#vo$_fB^yW03fx^41@6l$WuKU0JA^pt{8y)pCiN{K??v=1wyqHyEy3(`~v{AU&FEPvZp;J-}kf8i_<{M5@FexE~YUcMwsgC@F~ zlb`<;eaoveWiNyoYc7pR!!JSdGg=O@*kzhyIWd<@3Qhjh9DKfnPbyF9Y|;%DXPegh z-rwx|wCL)|PwS0X8ZXy0lXT(yqyF~Aem+9;DD$_X9-Id29?+$5QCz<{s6r8W0 YBi1hvOI=ANS$QQ{h8s7ujiC(x15D<=YybcN literal 0 HcmV?d00001 diff --git a/report/report.tex b/report/report.tex index 5c0ca34..bb31522 100644 --- a/report/report.tex +++ b/report/report.tex @@ -17,9 +17,9 @@ % please enter your group number your names and matriculation numbers here %TODO -\newcommand{\groupnumber}{Our group number} -\newcommand{\name}{Our names} -\newcommand{\matriculation}{Our matriculations, same order as the names} +\newcommand{\groupnumber}{5} +\newcommand{\name}{Tobias Eidelpes} +\newcommand{\matriculation}{01527193} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % End of customization % @@ -31,7 +31,7 @@ \setlength{\headsep}{20pt} \setlength{\textheight}{680pt} \pagestyle{fancy} -\fancyhf{} +\fancyhf{} \fancyhead[L]{Formal Methods for Security and Privacy \projnumber\ - minnieThor} \fancyhead[C]{} \fancyhead[R]{Group \groupnumber} @@ -43,7 +43,7 @@ \thispagestyle{empty} \noindent\framebox[\linewidth]{% \begin{minipage}{\linewidth}% - \hspace*{5pt} \textbf{Formal Methods for Security and Privacy (SS2020)} \hfill Prof.~Matteo Maffei \hspace*{5pt}\\ + \hspace*{5pt} \textbf{Formal Methods for Security and Privacy (SS2021)} \hfill Prof.~Matteo Maffei \hspace*{5pt}\\ \begin{center} {\bf\Large Project \projnumber~-- \Title} @@ -65,21 +65,52 @@ Our group consists of the following members: \end{center} \section{Abstract Semantics} -\emph{Nothing to fill in here, unless you feel that there is something about the implementation that we should consider when grading.} +\emph{Nothing to fill in here, unless you feel that there is something about the +implementation that we should consider when grading.} \section{Fixing reentrancy} -\paragraph{Justification for the soundness of \texttt{alice.txt}:} +\subsubsection*{Justification for the soundness of \texttt{alice.txt}:} - %TODO - - \section{Soundness of the \texttt{CALL} rules} - - \paragraph{Soundness classification of \texttt{CALL} rule sets:} - - \paragraph{Intuition for the sound rule sets:} - - \paragraph{Attack descriptions for the counter examples to the unsound rule sets:} +By switching the order of line 5 and line 6 in \texttt{alice.txt}, the contract +\texttt{bob.txt} has been fixed. This works because \texttt{sent} is set to 1 +\emph{before} the call instruction is executed and therefore reentering the +function is possible but will not execute another call instruction because +\texttt{sent} has already been set to 1. The contract now follows the +\emph{Check-Effects-Interactions Pattern}, which requires that checks and state +changes have to occur before calls to other contracts. + +\section{Soundness of the \texttt{CALL} rules} + +\subsubsection*{Soundness classification of \texttt{CALL} rule sets:} + +\textbf{Call 1}: Unsound \\ +\textbf{Call 2}: Sound \\ +\textbf{Call 3}: Unsound \\ +\textbf{Call 4}: Unsound \\ +\textbf{Call 5}: Sound + +\subsubsection*{Intuition for the sound rule sets:} + +\paragraph{Call 2:} + +The first two rules are the same rules as presented in the lecture. The third rule +models the case where the contract resumes execution after a call with the same +storage as before the call. This rule applies when the contract was not called +and produced a successful halting state before the contract resumes the +execution after the call. + +The fourth rule, however, models the case where the contract resumes execution +after it was left by another call from a contract that resulted in a halting +state. + +\paragraph{Call 5:} + +As for Call 2, the first two rules are the same as presented in the lecture. The +third rule is correct because in case of $sa[size - 4] = 1$, the local memory +and the persistent storage are correctly over-approximated. The other case is +where $sa[size - 4] = 0$. In this case the caller's memory may not be +manipulated, as formalized by the small-step semantics. \end{document} diff --git a/test-infrastructure.txt b/test-infrastructure.txt new file mode 100644 index 0000000..2cf5b9e --- /dev/null +++ b/test-infrastructure.txt @@ -0,0 +1,90 @@ +/* Testing infrastructure */ + +sel interval: int * int -> [int]; // interval function: interval (m, n) provides the numbers m, ..., n-1 + +op valueMoreAbstractThan (a: AbsDom, b:AbsDom): bool := + match (a, b) with + | (@T, _) => true + | (@V(x), @V(y)) => x = y + | _ => false; + +// Checks whether there exists a position where the two stacks disagree +op stackInequalExists{!size: int}(sa: array, sb: array): bool := + for (!i: int) in interval(0,!size): || ((select sa !i) != (select sb !i)); + +// Checks whether the stacks agree at all positions +op stackEqualForall{!size: int}(sa: array, sb: array): bool := + for (!i: int) in interval(0,!size): && ((select sa !i) = (select sb !i)); + +// Checks that the first stack is more abstract than the second one at all positions +op stackMoreAbstractThanForall{!size: int}(sa: array, sb: array): bool := + for (!i: int) in interval(0,!size): && (valueMoreAbstractThan(select sa !i, select sb !i)); + +// Update representation for AbsDom arrays. Used for easily checking against a sequence of probing points in memory or storage +datatype Update := @UP; +datatype UpdateList := @UPLIST>; + +const UPDATEDUMMY := @UP(0, @T); +const UPDATELISTDUMMY := @UPLIST(0, [UPDATEDUMMY]); + +op addUpdate(updates: UpdateList, up: Update): UpdateList := + match updates with + | @UPLIST(size, ups) => @UPLIST(size + 1, store ups size up) + | _ => UPDATELISTDUMMY; + +// Checks whether the array sa agrees with all updates of the Update array sb +op arrayEqual{!size:int} (sa: array, sb: array): bool := + for (!i:int) in interval(0, !size): && + (match (select sb !i) with + | @UP(p, v) => (select sa p) = v + | _ => false) + ; + +// Checks whether the array sa is at all update points more concrete than the updates in sb +op arrayMoreAbstractThan{!size:int} (sa: array, sb: array): bool := + for (!i:int) in interval(0, !size): && + (match (select sb !i) with + | @UP(p, v) => valueMoreAbstractThan(select sa p, v) + | _ => false) + ; + +// Checks whether array sa disagrees on one of the update points with the updates in sb +op arrayInequalExists{!size:int} (sa: array, sb: array): bool := + for (!i:int) in interval(0, !size): || + (match (select sb !i) with + | @UP(p, v) => (select sa p) != v + | _ => false) + ; + +// Configurations that we use for testing. Consist of the stack size, the stack array, and update lists for memory and storage (to probe at the specified points) +datatype Config := @C*UpdateList*UpdateList>; + +op getStackSize(conf: Config): int := + match conf with + | @C(size, sa, mem, stor) => size + | _ => 0; + +op getStackArray(conf: Config): array := + match conf with + | @C(size, sa, mem, stor) => sa + | _ => [@T]; + +op getMemUpdateList(conf: Config): UpdateList := + match conf with + | @C(size, sa, mem, stor) => mem + | _ => UPDATELISTDUMMY; + +op getStorUpdateList(conf: Config): UpdateList := + match conf with + | @C(size, sa, mem, stor) => stor + | _ => UPDATELISTDUMMY; + +op getUpdateSize(ul: UpdateList): int := + match ul with + | @UPLIST(s, ua) => s + | _ => 0; + +op getUpdates(ul: UpdateList): array := + match ul with + | @UPLIST(s, ua) => ua + | _ => [UPDATEDUMMY]; \ No newline at end of file