From 5bfc9fdac9f985cff7fb959506877cbbf0961b82 Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Wed, 4 Dec 2024 14:16:35 +0100 Subject: [PATCH 1/4] Implement `Clone` for ghost containers (like `Seq`) --- creusot-contracts/src/logic/fmap.rs | 9 +++++++++ creusot-contracts/src/logic/fset.rs | 9 +++++++++ creusot-contracts/src/logic/seq.rs | 9 +++++++++ 3 files changed, 27 insertions(+) diff --git a/creusot-contracts/src/logic/fmap.rs b/creusot-contracts/src/logic/fmap.rs index d66e12ed1..700ac2c90 100644 --- a/creusot-contracts/src/logic/fmap.rs +++ b/creusot-contracts/src/logic/fmap.rs @@ -430,3 +430,12 @@ impl FMap { panic!() } } + +impl Clone for FMap { + #[pure] + #[ensures(result == *self)] + #[trusted] + fn clone(&self) -> Self { + Self(self.0, self.1) + } +} diff --git a/creusot-contracts/src/logic/fset.rs b/creusot-contracts/src/logic/fset.rs index 3ad96d2b4..4eedbdfce 100644 --- a/creusot-contracts/src/logic/fset.rs +++ b/creusot-contracts/src/logic/fset.rs @@ -304,3 +304,12 @@ impl FSet { panic!() } } + +impl Clone for FSet { + #[pure] + #[ensures(result == *self)] + #[trusted] + fn clone(&self) -> Self { + Self(self.0) + } +} diff --git a/creusot-contracts/src/logic/seq.rs b/creusot-contracts/src/logic/seq.rs index 89cd2c57a..23912ff08 100644 --- a/creusot-contracts/src/logic/seq.rs +++ b/creusot-contracts/src/logic/seq.rs @@ -602,6 +602,15 @@ impl Seq { } } +impl Clone for Seq { + #[pure] + #[ensures(result == *self)] + #[trusted] + fn clone(&self) -> Self { + Self(self.0) + } +} + impl Invariant for Seq { #[predicate(prophetic)] #[open] From 75868a3837efe0bb5869b2982ebf3f2bada59261 Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Thu, 5 Dec 2024 09:52:39 +0100 Subject: [PATCH 2/4] Restrict Clone to be on `Clone + Copy` types, and add Copy --- creusot-contracts/src/logic/fmap.rs | 7 +++++-- creusot-contracts/src/logic/fset.rs | 7 +++++-- creusot-contracts/src/logic/seq.rs | 7 +++++-- 3 files changed, 15 insertions(+), 6 deletions(-) diff --git a/creusot-contracts/src/logic/fmap.rs b/creusot-contracts/src/logic/fmap.rs index 700ac2c90..5688294f4 100644 --- a/creusot-contracts/src/logic/fmap.rs +++ b/creusot-contracts/src/logic/fmap.rs @@ -431,11 +431,14 @@ impl FMap { } } -impl Clone for FMap { +impl Clone for FMap { #[pure] #[ensures(result == *self)] #[trusted] fn clone(&self) -> Self { - Self(self.0, self.1) + *self } } + +// Having `Copy` guarantees that the operation is pure, even if we decide to change the definition of `Clone`. +impl Copy for FMap {} diff --git a/creusot-contracts/src/logic/fset.rs b/creusot-contracts/src/logic/fset.rs index 4eedbdfce..b5fc9377b 100644 --- a/creusot-contracts/src/logic/fset.rs +++ b/creusot-contracts/src/logic/fset.rs @@ -305,11 +305,14 @@ impl FSet { } } -impl Clone for FSet { +impl Clone for FSet { #[pure] #[ensures(result == *self)] #[trusted] fn clone(&self) -> Self { - Self(self.0) + *self } } + +// Having `Copy` guarantees that the operation is pure, even if we decide to change the definition of `Clone`. +impl Copy for FSet {} diff --git a/creusot-contracts/src/logic/seq.rs b/creusot-contracts/src/logic/seq.rs index 23912ff08..d28a4a84b 100644 --- a/creusot-contracts/src/logic/seq.rs +++ b/creusot-contracts/src/logic/seq.rs @@ -602,15 +602,18 @@ impl Seq { } } -impl Clone for Seq { +// Having `Copy` guarantees that the operation is pure, even if we decide to change the definition of `Clone`. +impl Clone for Seq { #[pure] #[ensures(result == *self)] #[trusted] fn clone(&self) -> Self { - Self(self.0) + *self } } +impl Copy for Seq {} + impl Invariant for Seq { #[predicate(prophetic)] #[open] From 3779413c9d605ee9689a4935283e005c41ccca18 Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Thu, 5 Dec 2024 09:55:47 +0100 Subject: [PATCH 3/4] Add missing implementations of `Invariant` on ghost containers --- creusot-contracts/src/logic/fmap.rs | 10 ++++++++++ creusot-contracts/src/logic/fset.rs | 10 ++++++++++ 2 files changed, 20 insertions(+) diff --git a/creusot-contracts/src/logic/fmap.rs b/creusot-contracts/src/logic/fmap.rs index 5688294f4..f93d5aa53 100644 --- a/creusot-contracts/src/logic/fmap.rs +++ b/creusot-contracts/src/logic/fmap.rs @@ -442,3 +442,13 @@ impl Clone for FMap { // Having `Copy` guarantees that the operation is pure, even if we decide to change the definition of `Clone`. impl Copy for FMap {} + +impl Invariant for FMap { + #[predicate(prophetic)] + #[open] + #[creusot::trusted_ignore_structural_inv] + #[creusot::trusted_is_tyinv_trivial_if_param_trivial] + fn invariant(self) -> bool { + pearlite! { forall self.contains(k) ==> inv(k) && inv(self.lookup_unsized(k)) } + } +} diff --git a/creusot-contracts/src/logic/fset.rs b/creusot-contracts/src/logic/fset.rs index b5fc9377b..9ebd35b76 100644 --- a/creusot-contracts/src/logic/fset.rs +++ b/creusot-contracts/src/logic/fset.rs @@ -316,3 +316,13 @@ impl Clone for FSet { // Having `Copy` guarantees that the operation is pure, even if we decide to change the definition of `Clone`. impl Copy for FSet {} + +impl Invariant for FSet { + #[predicate(prophetic)] + #[open] + #[creusot::trusted_ignore_structural_inv] + #[creusot::trusted_is_tyinv_trivial_if_param_trivial] + fn invariant(self) -> bool { + pearlite! { forall self.contains(*x) ==> inv(*x) } + } +} From 9661b163c80f632b81455343ab69a6cbec5f6113 Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Wed, 4 Dec 2024 14:19:00 +0100 Subject: [PATCH 4/4] Update tests --- .../creusot-contracts/creusot-contracts.coma | 319 +++++++++++--- .../creusot-contracts/why3session.xml | 263 ++++++------ .../creusot-contracts/why3shapes.gz | Bin 23189 -> 23384 bytes creusot/tests/should_fail/bug/878.coma | 4 +- creusot/tests/should_fail/bug/specialize.coma | 4 +- .../should_succeed/bug/final_borrows.coma | 4 +- .../tests/should_succeed/ghost/ghost_map.coma | 389 +++++++++--------- .../ghost/ghost_map/why3session.xml | 4 +- .../ghost/ghost_map/why3shapes.gz | Bin 710 -> 702 bytes .../tests/should_succeed/ghost/ghost_set.coma | 215 +++++----- .../ghost/ghost_set/why3session.xml | 4 +- .../ghost/ghost_set/why3shapes.gz | Bin 421 -> 401 bytes creusot/tests/should_succeed/hashmap.coma | 12 +- .../should_succeed/heapsort_generic.coma | 4 +- creusot/tests/should_succeed/hillel.coma | 8 +- .../should_succeed/iterators/02_iter_mut.coma | 10 +- .../iterators/03_std_iterators.coma | 6 +- .../iterators/08_collect_extend.coma | 4 +- creusot/tests/should_succeed/knapsack.coma | 2 +- .../tests/should_succeed/knapsack_full.coma | 2 +- creusot/tests/should_succeed/linked_list.coma | 6 +- .../selection_sort_generic.coma | 2 +- creusot/tests/should_succeed/slices/01.coma | 2 +- .../tests/should_succeed/sparse_array.coma | 12 +- .../tests/should_succeed/take_first_mut.coma | 2 +- .../traits/16_impl_cloning.coma | 2 +- .../type_invariants/vec_inv.coma | 2 +- .../tests/should_succeed/vector/02_gnome.coma | 2 +- .../vector/03_knuth_shuffle.coma | 2 +- .../vector/05_binary_search_generic.coma | 2 +- .../should_succeed/vector/07_read_write.coma | 2 +- .../should_succeed/vector/09_capacity.coma | 4 +- 32 files changed, 766 insertions(+), 528 deletions(-) diff --git a/creusot/tests/creusot-contracts/creusot-contracts.coma b/creusot/tests/creusot-contracts/creusot-contracts.coma index 342dc19e7..61c652f2d 100644 --- a/creusot/tests/creusot-contracts/creusot-contracts.coma +++ b/creusot/tests/creusot-contracts/creusot-contracts.coma @@ -8778,58 +8778,32 @@ module M_creusot_contracts__logic__fmap__qyi9892930999379617882__ext_eq [#"../.. && ([%#sfmap1] (forall k : t_K'0 . get_unsized'0 self k = get_unsized'0 other k) -> result)) end module M_creusot_contracts__logic__fmap__qyi9892930999379617882__contains_ghost [#"../../../creusot-contracts/src/logic/fmap.rs" 285 4 285 49] (* logic::fmap::FMap *) - let%span sfmap0 = "../../../creusot-contracts/src/logic/fmap.rs" 285 33 285 36 - let%span sfmap1 = "../../../creusot-contracts/src/logic/fmap.rs" 284 14 284 43 - let%span sfmap2 = "../../../creusot-contracts/src/logic/fmap.rs" 314 28 314 31 - let%span sfmap3 = "../../../creusot-contracts/src/logic/fmap.rs" 314 40 314 50 - let%span sfmap4 = "../../../creusot-contracts/src/logic/fmap.rs" 306 4 313 11 - let%span soption5 = "../../../creusot-contracts/src/std/option.rs" 36 26 36 51 - let%span sfmap6 = "../../../creusot-contracts/src/logic/fmap.rs" 132 8 132 35 - let%span sfmap7 = "../../../creusot-contracts/src/logic/fmap.rs" 124 8 124 35 - let%span sfmap8 = "../../../creusot-contracts/src/logic/fmap.rs" 103 8 103 26 - let%span sutil9 = "../../../creusot-contracts/src/util.rs" 43 11 43 21 - let%span sutil10 = "../../../creusot-contracts/src/util.rs" 44 10 44 28 - let%span sinvariant11 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 - let%span sfmap12 = "../../../creusot-contracts/src/logic/fmap.rs" 58 14 58 86 + let%span sfmap0 = "../../../creusot-contracts/src/logic/fmap.rs" 285 27 285 31 + let%span sfmap1 = "../../../creusot-contracts/src/logic/fmap.rs" 285 33 285 36 + let%span sfmap2 = "../../../creusot-contracts/src/logic/fmap.rs" 284 14 284 43 + let%span sfmap3 = "../../../creusot-contracts/src/logic/fmap.rs" 314 22 314 26 + let%span sfmap4 = "../../../creusot-contracts/src/logic/fmap.rs" 314 28 314 31 + let%span sfmap5 = "../../../creusot-contracts/src/logic/fmap.rs" 314 40 314 50 + let%span sfmap6 = "../../../creusot-contracts/src/logic/fmap.rs" 306 4 313 11 + let%span soption7 = "../../../creusot-contracts/src/std/option.rs" 36 26 36 51 + let%span sfmap8 = "../../../creusot-contracts/src/logic/fmap.rs" 132 8 132 35 + let%span sfmap9 = "../../../creusot-contracts/src/logic/fmap.rs" 124 8 124 35 + let%span sfmap10 = "../../../creusot-contracts/src/logic/fmap.rs" 103 8 103 26 + let%span sutil11 = "../../../creusot-contracts/src/util.rs" 43 11 43 21 + let%span sutil12 = "../../../creusot-contracts/src/util.rs" 44 10 44 28 + let%span sinvariant13 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 + let%span sfmap14 = "../../../creusot-contracts/src/logic/fmap.rs" 58 14 58 86 + let%span sfmap15 = "../../../creusot-contracts/src/logic/fmap.rs" 452 20 452 91 + let%span sboxed16 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 use prelude.prelude.Borrow - type t_K'0 - - predicate inv'4 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_K'0) - - predicate invariant'0 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_K'0) = - [%#sinvariant11] inv'4 self - - predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_K'0) + type t_FMap'0 - axiom inv_axiom'0 [@rewrite] : forall x : t_K'0 [inv'0 x] . inv'0 x = invariant'0 x + type t_K'0 type t_V'0 - type t_Option'0 = - | C_None'0 - | C_Some'0 t_V'0 - - predicate inv'5 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_V'0) - - predicate invariant'2 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_V'0) = - [%#sinvariant11] inv'5 self - - predicate inv'3 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_V'0) - - axiom inv_axiom'3 [@rewrite] : forall x : t_V'0 [inv'3 x] . inv'3 x = invariant'2 x - - predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Option'0) - - axiom inv_axiom'1 [@rewrite] : forall x : t_Option'0 [inv'1 x] . inv'1 x - = match x with - | C_None'0 -> true - | C_Some'0 a_0 -> inv'3 a_0 - end - - type t_FMap'0 - type t_Option'1 = | C_None'1 | C_Some'1 t_V'0 @@ -8839,7 +8813,7 @@ module M_creusot_contracts__logic__fmap__qyi9892930999379617882__contains_ghost function view'0 [#"../../../creusot-contracts/src/logic/fmap.rs" 59 4 59 35] (self : t_FMap'0) : Map.map t_K'0 (t_Option'1) - axiom view'0_spec : forall self : t_FMap'0 . [%#sfmap12] forall m1 : t_FMap'0, m2 : t_FMap'0 . m1 <> m2 + axiom view'0_spec : forall self : t_FMap'0 . [%#sfmap14] forall m1 : t_FMap'0, m2 : t_FMap'0 . m1 <> m2 -> view'0 m1 <> view'0 m2 use map.Map @@ -8847,27 +8821,79 @@ module M_creusot_contracts__logic__fmap__qyi9892930999379617882__contains_ghost function get_unsized'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/fmap.rs" 102 4 102 55] (self : t_FMap'0) (k : t_K'0) : t_Option'1 = - [%#sfmap8] Map.get (view'0 self) k + [%#sfmap10] Map.get (view'0 self) k function contains'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/fmap.rs" 131 4 131 39] (self : t_FMap'0) (k : t_K'0) : bool = - [%#sfmap6] get_unsized'0 self k <> C_None'1 + [%#sfmap8] get_unsized'0 self k <> C_None'1 + + predicate inv'6 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_K'0) function unwrap'0 [#"../../../creusot-contracts/src/util.rs" 45 0 45 36] (op : t_Option'1) : t_V'0 - axiom unwrap'0_spec : forall op : t_Option'1 . ([%#sutil9] op <> C_None'1) - -> ([%#sutil10] C_Some'1 (unwrap'0 op) = op) + axiom unwrap'0_spec : forall op : t_Option'1 . ([%#sutil11] op <> C_None'1) + -> ([%#sutil12] C_Some'1 (unwrap'0 op) = op) function lookup_unsized'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/fmap.rs" 123 4 123 50] (self : t_FMap'0) (k : t_K'0) : t_V'0 = - [%#sfmap7] unwrap'0 (get_unsized'0 self k) + [%#sfmap9] unwrap'0 (get_unsized'0 self k) + + predicate inv'7 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_V'0) + + predicate invariant'5 [#"../../../creusot-contracts/src/std/boxed.rs" 27 4 27 30] (self : t_V'0) = + [%#sboxed16] inv'7 self + + predicate inv'8 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_V'0) + + axiom inv_axiom'6 [@rewrite] : forall x : t_V'0 [inv'8 x] . inv'8 x = invariant'5 x - let rec get_ghost'0 (self:t_FMap'0) (key:t_K'0) (return' (ret:t_Option'0))= {[@expl:get_ghost 'key' type invariant] [%#sfmap2] inv'0 key} + predicate invariant'4 [#"../../../creusot-contracts/src/logic/fmap.rs" 451 4 451 30] (self : t_FMap'0) = + [%#sfmap15] forall k : t_K'0 . contains'0 self k -> inv'6 k /\ inv'8 (lookup_unsized'0 self k) + + predicate inv'5 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_FMap'0) + + axiom inv_axiom'5 [@rewrite] : forall x : t_FMap'0 [inv'5 x] . inv'5 x = invariant'4 x + + predicate invariant'0 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_FMap'0) = + [%#sinvariant13] inv'5 self + + predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_FMap'0) + + axiom inv_axiom'0 [@rewrite] : forall x : t_FMap'0 [inv'0 x] . inv'0 x = invariant'0 x + + predicate invariant'1 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_K'0) = + [%#sinvariant13] inv'6 self + + predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_K'0) + + axiom inv_axiom'1 [@rewrite] : forall x : t_K'0 [inv'1 x] . inv'1 x = invariant'1 x + + type t_Option'0 = + | C_None'0 + | C_Some'0 t_V'0 + + predicate invariant'3 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_V'0) = + [%#sinvariant13] inv'7 self + + predicate inv'4 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_V'0) + + axiom inv_axiom'4 [@rewrite] : forall x : t_V'0 [inv'4 x] . inv'4 x = invariant'3 x + + predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Option'0) + + axiom inv_axiom'2 [@rewrite] : forall x : t_Option'0 [inv'2 x] . inv'2 x + = match x with + | C_None'0 -> true + | C_Some'0 a_0 -> inv'4 a_0 + end + + let rec get_ghost'0 (self:t_FMap'0) (key:t_K'0) (return' (ret:t_Option'0))= {[@expl:get_ghost 'self' type invariant] [%#sfmap3] inv'0 self} + {[@expl:get_ghost 'key' type invariant] [%#sfmap4] inv'1 key} any - [ return' (result:t_Option'0)-> {[%#sfmap3] inv'1 result} - {[%#sfmap4] if contains'0 self key then + [ return' (result:t_Option'0)-> {[%#sfmap5] inv'2 result} + {[%#sfmap6] if contains'0 self key then match result with | C_None'0 -> false | C_Some'0 r -> lookup_unsized'0 self key = r @@ -8878,27 +8904,28 @@ module M_creusot_contracts__logic__fmap__qyi9892930999379617882__contains_ghost (! return' {result}) ] - predicate invariant'1 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_Option'0) = - [%#sinvariant11] inv'1 self + predicate invariant'2 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_Option'0) = + [%#sinvariant13] inv'2 self - predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Option'0) + predicate inv'3 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Option'0) - axiom inv_axiom'2 [@rewrite] : forall x : t_Option'0 [inv'2 x] . inv'2 x = invariant'1 x + axiom inv_axiom'3 [@rewrite] : forall x : t_Option'0 [inv'3 x] . inv'3 x = invariant'2 x - let rec is_some'0 (self:t_Option'0) (return' (ret:bool))= {[@expl:is_some 'self' type invariant] inv'2 self} - any [ return' (result:bool)-> {[%#soption5] result = (self <> C_None'0)} (! return' {result}) ] + let rec is_some'0 (self:t_Option'0) (return' (ret:bool))= {[@expl:is_some 'self' type invariant] inv'3 self} + any [ return' (result:bool)-> {[%#soption7] result = (self <> C_None'0)} (! return' {result}) ] use prelude.prelude.Intrinsic meta "compute_max_steps" 1000000 - let rec contains_ghost'0 (self:t_FMap'0) (key:t_K'0) (return' (ret:bool))= {[@expl:contains_ghost 'key' type invariant] [%#sfmap0] inv'0 key} + let rec contains_ghost'0 (self:t_FMap'0) (key:t_K'0) (return' (ret:bool))= {[@expl:contains_ghost 'self' type invariant] [%#sfmap0] inv'0 self} + {[@expl:contains_ghost 'key' type invariant] [%#sfmap1] inv'1 key} (! bb0 [ bb0 = s0 [ s0 = get_ghost'0 {self} {key} (fun (_ret':t_Option'0) -> [ &_5 <- _ret' ] s1) | s1 = bb1 ] | bb1 = s0 [ s0 = is_some'0 {_5} (fun (_ret':bool) -> [ &_0 <- _ret' ] s1) | s1 = bb2 ] | bb2 = return' {_0} ] ) [ & _0 : bool = any_l () | & self : t_FMap'0 = self | & key : t_K'0 = key | & _5 : t_Option'0 = any_l () ] - [ return' (result:bool)-> {[@expl:contains_ghost ensures] [%#sfmap1] result = contains'0 self key} + [ return' (result:bool)-> {[@expl:contains_ghost ensures] [%#sfmap2] result = contains'0 self key} (! return' {result}) ] end @@ -20506,7 +20533,7 @@ module M_creusot_contracts__stdqy35z1__vec__qyi6844585276173866460__resolve_cohe let%span sindex3 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span sinvariant4 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 let%span svec5 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41 - let%span sseq6 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq6 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95 let%span sboxed7 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 use prelude.prelude.Borrow @@ -20570,7 +20597,7 @@ module M_creusot_contracts__stdqy35z1__vec__qyi6844585276173866460__resolve_cohe axiom inv_axiom'3 [@rewrite] : forall x : t_T'0 [inv'3 x] . inv'3 x = invariant'3 x - predicate invariant'2 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_T'0) = + predicate invariant'2 [#"../../../creusot-contracts/src/logic/seq.rs" 622 4 622 30] (self : Seq.seq t_T'0) = [%#sseq6] forall i : int . 0 <= i /\ i < Seq.length self -> inv'3 (Seq.get self i) predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_T'0) @@ -24646,6 +24673,126 @@ module M_creusot_contracts__ghost__qyi17645547594388049322__clone__refines [#".. goal refines : [%#sghost0] forall self : t_GhostBox'0 . inv'0 self -> inv'0 self /\ (forall result : t_GhostBox'0 . result = self /\ inv'1 result -> result = self /\ inv'1 result) end +module M_creusot_contracts__logic__fmap__qyi4648834920430559677__clone__refines [#"../../../creusot-contracts/src/logic/fmap.rs" 438 4 438 27] (* as std::clone::Clone> *) + let%span sfmap0 = "../../../creusot-contracts/src/logic/fmap.rs" 438 4 438 27 + let%span sinvariant1 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 + let%span sfmap2 = "../../../creusot-contracts/src/logic/fmap.rs" 452 20 452 91 + let%span sfmap3 = "../../../creusot-contracts/src/logic/fmap.rs" 132 8 132 35 + let%span sfmap4 = "../../../creusot-contracts/src/logic/fmap.rs" 124 8 124 35 + let%span sfmap5 = "../../../creusot-contracts/src/logic/fmap.rs" 103 8 103 26 + let%span sutil6 = "../../../creusot-contracts/src/util.rs" 43 11 43 21 + let%span sutil7 = "../../../creusot-contracts/src/util.rs" 44 10 44 28 + let%span sfmap8 = "../../../creusot-contracts/src/logic/fmap.rs" 58 14 58 86 + let%span sboxed9 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 + + use prelude.prelude.Borrow + + type t_FMap'0 + + type t_K'0 + + type t_V'0 + + type t_Option'0 = + | C_None'0 + | C_Some'0 t_V'0 + + use map.Map + + function view'0 [#"../../../creusot-contracts/src/logic/fmap.rs" 59 4 59 35] (self : t_FMap'0) : Map.map t_K'0 (t_Option'0) + + + axiom view'0_spec : forall self : t_FMap'0 . [%#sfmap8] forall m1 : t_FMap'0, m2 : t_FMap'0 . m1 <> m2 + -> view'0 m1 <> view'0 m2 + + use map.Map + + function get_unsized'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/fmap.rs" 102 4 102 55] (self : t_FMap'0) (k : t_K'0) : t_Option'0 + + = + [%#sfmap5] Map.get (view'0 self) k + + function contains'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/fmap.rs" 131 4 131 39] (self : t_FMap'0) (k : t_K'0) : bool + + = + [%#sfmap3] get_unsized'0 self k <> C_None'0 + + predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_K'0) + + function unwrap'0 [#"../../../creusot-contracts/src/util.rs" 45 0 45 36] (op : t_Option'0) : t_V'0 + + axiom unwrap'0_spec : forall op : t_Option'0 . ([%#sutil6] op <> C_None'0) + -> ([%#sutil7] C_Some'0 (unwrap'0 op) = op) + + function lookup_unsized'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/fmap.rs" 123 4 123 50] (self : t_FMap'0) (k : t_K'0) : t_V'0 + + = + [%#sfmap4] unwrap'0 (get_unsized'0 self k) + + predicate inv'4 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_V'0) + + predicate invariant'2 [#"../../../creusot-contracts/src/std/boxed.rs" 27 4 27 30] (self : t_V'0) = + [%#sboxed9] inv'4 self + + predicate inv'3 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_V'0) + + axiom inv_axiom'2 [@rewrite] : forall x : t_V'0 [inv'3 x] . inv'3 x = invariant'2 x + + predicate invariant'1 [#"../../../creusot-contracts/src/logic/fmap.rs" 451 4 451 30] (self : t_FMap'0) = + [%#sfmap2] forall k : t_K'0 . contains'0 self k -> inv'2 k /\ inv'3 (lookup_unsized'0 self k) + + predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_FMap'0) + + axiom inv_axiom'1 [@rewrite] : forall x : t_FMap'0 [inv'1 x] . inv'1 x = invariant'1 x + + predicate invariant'0 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_FMap'0) = + [%#sinvariant1] inv'1 self + + predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_FMap'0) + + axiom inv_axiom'0 [@rewrite] : forall x : t_FMap'0 [inv'0 x] . inv'0 x = invariant'0 x + + goal refines : [%#sfmap0] forall self : t_FMap'0 . inv'0 self + -> inv'0 self /\ (forall result : t_FMap'0 . result = self /\ inv'1 result -> result = self /\ inv'1 result) +end +module M_creusot_contracts__logic__fset__qyi11096226875104347554__clone__refines [#"../../../creusot-contracts/src/logic/fset.rs" 312 4 312 27] (* as std::clone::Clone> *) + let%span sfset0 = "../../../creusot-contracts/src/logic/fset.rs" 312 4 312 27 + let%span sinvariant1 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 + let%span sfset2 = "../../../creusot-contracts/src/logic/fset.rs" 326 20 326 63 + let%span sfset3 = "../../../creusot-contracts/src/logic/fset.rs" 46 8 46 26 + + use prelude.prelude.Borrow + + type t_T'0 + + use set.Fset + + use set.Fset + + predicate contains'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/fset.rs" 45 4 45 39] (self : Fset.fset t_T'0) (e : t_T'0) + + = + [%#sfset3] Fset.mem e self + + predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_T'0) + + predicate invariant'1 [#"../../../creusot-contracts/src/logic/fset.rs" 325 4 325 30] (self : Fset.fset t_T'0) = + [%#sfset2] forall x : t_T'0 . contains'0 self x -> inv'2 x + + predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Fset.fset t_T'0) + + axiom inv_axiom'1 [@rewrite] : forall x : Fset.fset t_T'0 [inv'1 x] . inv'1 x = invariant'1 x + + predicate invariant'0 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : Fset.fset t_T'0) = + [%#sinvariant1] inv'1 self + + predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Fset.fset t_T'0) + + axiom inv_axiom'0 [@rewrite] : forall x : Fset.fset t_T'0 [inv'0 x] . inv'0 x = invariant'0 x + + goal refines : [%#sfset0] forall self : Fset.fset t_T'0 . inv'0 self + -> inv'0 self /\ (forall result : Fset.fset t_T'0 . result = self /\ inv'1 result -> result = self /\ inv'1 result) +end module M_creusot_contracts__logic__int__qyi3540547019284611154__clone__refines [#"../../../creusot-contracts/src/logic/int.rs" 37 4 37 27] (* *) let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 37 4 37 27 @@ -24664,6 +24811,50 @@ module M_creusot_contracts__logic__int__qyi3540547019284611154__clone__refines [ goal refines : [%#sint0] forall self : int . inv'0 self -> (forall result : int . result = self -> result = self /\ inv'1 result) end +module M_creusot_contracts__logic__seq__qyi8239750555979287100__clone__refines [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 27] (* as std::clone::Clone> *) + let%span sseq0 = "../../../creusot-contracts/src/logic/seq.rs" 610 4 610 27 + let%span sinvariant1 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 + let%span sseq2 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95 + let%span sboxed3 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 + + use prelude.prelude.Borrow + + type t_T'0 + + use seq.Seq + + use prelude.prelude.Int + + use seq.Seq + + use seq.Seq + + predicate inv'3 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_T'0) + + predicate invariant'2 [#"../../../creusot-contracts/src/std/boxed.rs" 27 4 27 30] (self : t_T'0) = + [%#sboxed3] inv'3 self + + predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_T'0) + + axiom inv_axiom'2 [@rewrite] : forall x : t_T'0 [inv'2 x] . inv'2 x = invariant'2 x + + predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 622 4 622 30] (self : Seq.seq t_T'0) = + [%#sseq2] forall i : int . 0 <= i /\ i < Seq.length self -> inv'2 (Seq.get self i) + + predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_T'0) + + axiom inv_axiom'1 [@rewrite] : forall x : Seq.seq t_T'0 [inv'1 x] . inv'1 x = invariant'1 x + + predicate invariant'0 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : Seq.seq t_T'0) = + [%#sinvariant1] inv'1 self + + predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_T'0) + + axiom inv_axiom'0 [@rewrite] : forall x : Seq.seq t_T'0 [inv'0 x] . inv'0 x = invariant'0 x + + goal refines : [%#sseq0] forall self : Seq.seq t_T'0 . inv'0 self + -> inv'0 self /\ (forall result : Seq.seq t_T'0 . result = self /\ inv'1 result -> result = self /\ inv'1 result) +end module M_creusot_contracts__snapshot__qyi5567339964777190687__clone__refines [#"../../../creusot-contracts/src/snapshot.rs" 59 4 59 27] (* as std::clone::Clone> *) let%span ssnapshot0 = "../../../creusot-contracts/src/snapshot.rs" 59 4 59 27 diff --git a/creusot/tests/creusot-contracts/creusot-contracts/why3session.xml b/creusot/tests/creusot-contracts/creusot-contracts/why3session.xml index 8ba632708..5b920d707 100644 --- a/creusot/tests/creusot-contracts/creusot-contracts/why3session.xml +++ b/creusot/tests/creusot-contracts/creusot-contracts/why3session.xml @@ -1761,12 +1761,12 @@ - + - + @@ -1776,7 +1776,7 @@ - + @@ -1786,7 +1786,7 @@ - + @@ -1796,26 +1796,26 @@ - + - + - + - + @@ -1825,7 +1825,7 @@ - + @@ -1835,7 +1835,7 @@ - + @@ -1860,7 +1860,7 @@ - + @@ -1869,17 +1869,17 @@ - + - + - + @@ -1888,37 +1888,37 @@ - + - + - + - + - + - + - + - + - + @@ -1943,37 +1943,37 @@ - + - + - + - + - + - + - + @@ -1983,7 +1983,7 @@ - + @@ -1993,7 +1993,7 @@ - + @@ -2003,7 +2003,7 @@ - + @@ -2013,7 +2013,7 @@ - + @@ -2023,7 +2023,7 @@ - + @@ -2040,10 +2040,10 @@ - + - + @@ -2054,22 +2054,22 @@ - + - + - + - + @@ -2079,7 +2079,7 @@ - + @@ -2088,19 +2088,19 @@ - + - + - + @@ -2115,21 +2115,21 @@ - + - + - + @@ -2138,14 +2138,14 @@ - + - + @@ -2154,35 +2154,35 @@ - + - + - + - + - + - + - + - + - + @@ -2193,7 +2193,7 @@ - + @@ -2216,29 +2216,29 @@ - + - + - + - + - + @@ -2251,54 +2251,54 @@ - + - + - + - + - + - + - + - + - + - + - + - + @@ -2317,7 +2317,7 @@ - + @@ -2326,7 +2326,7 @@ - + @@ -2336,7 +2336,7 @@ - + @@ -2349,12 +2349,12 @@ - + - + @@ -2365,7 +2365,7 @@ - + @@ -2375,7 +2375,7 @@ - + @@ -2390,7 +2390,7 @@ - + @@ -2400,7 +2400,7 @@ - + @@ -2410,7 +2410,7 @@ - + @@ -2420,7 +2420,7 @@ - + @@ -2430,12 +2430,12 @@ - + - + @@ -2445,26 +2445,26 @@ - + - + - + - + @@ -2474,7 +2474,7 @@ - + @@ -2484,17 +2484,17 @@ - + - + - + @@ -2507,7 +2507,7 @@ - + @@ -2575,7 +2575,7 @@ - + @@ -2585,7 +2585,7 @@ - + @@ -2596,10 +2596,10 @@ - + - + @@ -2610,7 +2610,7 @@ - + @@ -2620,7 +2620,7 @@ - + @@ -2631,10 +2631,10 @@ - + - + @@ -2645,7 +2645,7 @@ - + @@ -2655,7 +2655,7 @@ - + @@ -2666,10 +2666,10 @@ - + - + @@ -2700,17 +2700,17 @@ - + - + - + @@ -2719,7 +2719,7 @@ - + @@ -2728,21 +2728,21 @@ - + - + - + @@ -2752,7 +2752,7 @@ - + @@ -2762,7 +2762,7 @@ - + @@ -2772,7 +2772,7 @@ - + @@ -2807,7 +2807,12 @@ - + + + + + + @@ -2827,12 +2832,22 @@ - + + + + + + + + + + + - + diff --git a/creusot/tests/creusot-contracts/creusot-contracts/why3shapes.gz b/creusot/tests/creusot-contracts/creusot-contracts/why3shapes.gz index dc51f2921829b41a6d0bc7e94a9a4ed81b43830e..18053c4dee2ac7150a649008034eefc06144e4ee 100644 GIT binary patch delta 22567 zcmV)bK&ii#wE@_+0e>Hh2mk;800030?7i8N966F8`0ihkZ?)T$5`i9204vFs;pQ^N zLnOQBVOm^9_JxA8D!N!ClM&3Wny+6`yWGs&%)^68)*PD;%=Eya0Q7=FRRQ}y{^^Iu zKgUn?@rPgQ=f{VSAO5c&psKFD(pWglF&ow^P&wnthe)h!k+GSTh*$L>XpPc+DEL*$F zB00HJSoH*R0&`x@x)x4=^BMgTU&lW^b+u-w{kP9w>fPaAm;LAjJWaOiRL4$TRo`jZ z$DTkIecn$4b$?Zx1Gy9U^#tG7MeSujbAoU}v(s;^)qeM1*X{1^?oj{w>FMw9I(AwP z9{(2qz6YbLQwTTW2EGzEW`Uc{HEz-2jF*>pQJid`;j+&e2RAYmESPGWVq2W}9F?#3 z(dBHB^|I3*O|QrnEM)6>7W~t#6nd`L4v{vyZLX^W27lqKQ7+~&ue==XZ|BO(b;Akq za$Q<__vUiBC&Xo`7HxyrZ+o|ak^de)-d`YTRrGglby$P!*1oCUH>$VRw7ILS>((>= zdxzESVHaGxJ>RVXmvuWc-C5{G_4a%>hFx>xwq(q9=B{Xa^mVHp&ObNPf|YXVErFSE z{MZ=-_ary9+EXBlhPMqGpFX~O`0#Wx9SVUL#GjkKXy9!xdzXeqd$Lkn)e!z4W;|C=FiUHQq|rr-@69>6`sSdExc=uowYzTf z{2B9~_muCV%}x6EdXHPCa#bp>a~&?Y?)gpiPq*sE=XyO)ty#Bg8uEINjbY5*$$wFG zw-)zXOisLFa^f>4Ctf!>@tVnrn*qj(H=Gv962Ja;9#IPz2J0PyKy_^V~ zuK7@wm6tf#@!QO6E><3Tdh85&QN4wWone=C+biAlYt3pl*SIs+Rps7FH>bL&+galt ziq_TJYIx}#*_!#vf3m@&6qe1pqV3tNTPe7wU*f}uUv<2@@yCBby*uyghd(|2IsW=k z|3lF~?s>ny`*L4wzgBet-p~KIdlMg@K7YwiUp~k8?-s3k__)`gTU$3E zo=kiwC-Y`K6P&i}*-TW|J!$dh+TK0ZUwV;_4LyW>K#G zu0@Hx?7Q9OuGciPdBynZRg5X79P|CMLQ5A#eXEILZ~~o_UvyJOb&OEo-{5hw?wy&ks-U9*Tm0_fYzM@W&I)n0q$j!2Yyi|5=Nb6ylQo zd0=$D-z>dbw|@2NWYzV0zg@g!aaML+l*nb@?KT68-$uvt9YM)9-mO?s=el-ouAq`s2UVRvoExt({~IVZsO)&dtB2J{=ovacUx*)K&o48`Gov-ED=`qis0 zl%lSn``wzQ_=m0>7G<4_=>o=;hP@(KFvQ1C4_6stL4b|MO9ITsG{fr6{buP3C#GAu zqWph;yLgF>&X8G@;AP+KHkUYf`{B!9>*x4Xhn4A+uL}l^Yo~GTv=R&+LGVH_>|8MH zo?zIKbM0P(C0A}D4=zvwJxZ2+?LZI(xey;2Cn0Ak^jp|+Zx*<5BW~P?8@He|j4S|4 z&X|?2cmw+N4c^gpr&-mKM_}OlWg%`txzc}f*gR)O(wq3{&SL`|_bXLQL!lBhyT54-?mbEcpyvM=9SYk}Q9? za!5E?6>7BR1YrpUabOZ$nO-;^GH|I4XXP)V;u^mzDsEPCPsQ^XZhH*w%sY8|Nz>`i zu>8|^k@)FPWmZ@eV9(MUgNtT`6lROeQ_ z=9ObHoJgIAOUuA)6r%4Mo0YXOoqlOXv0-NY5qS3de!isfRD4O*MfX3|r_NC+i&Awy z_WsW&IFUV(JCVH6vyU6C&Td}gna92D4o0J?d!o^hCh3ktYT6GA@xzd3*uH=3>o)=G zG3LjqDVya0XBc7DrtdqeQ}|QYGyL9LIF1zN`hVQVI&A1oU7;D>FytAw>-uie58WBf+B7T&I9K>tn>m`hx(1ejC|6nzJO6qOY5b9wvrkuf zC|xp8x`lgEehKTOd;{N{L4F6O>4D$EF=@sw`RxTR*JzIu+Lle@RkX)mSD6#xxoD{y zRY#u)JKZ?BHDVgI3iXN+C%rZ48=TM{)1VGdWX@2z>&TZNd8QI!u5*9QOeL!3o3&Y} zM6Fw>>j8MDEM*+VZlXQv97htoy};$_&s{3y8_>Ss_IL}oPdK`X+m(f$<@Phk@4)Q? z+Hc_YIOFzb(4G#Z_Q$>-K7Fo#eR!;gE%Awulk^<=b;YJJ+hJ;t0)7u1z^ z%i*=~($rARs=>1dopyiec``nZ5bT0XGu>h@%;Zab2=P&gzoicqwmV^GvTUlZoBmgXOZd26hnl>XpuX!EB0-ht8q=5dVK&vH9dlqfyc@>)R={R}R9(&h$rV7d(zkd0%D>U1<_J`5E9i$U z_i#u5$-Db7{rxz|wrKoqC~zWrjs*8>cGg)<7#c0Avu1x$H^Gi-(UghVWW$xo1|2ml zCfiwOXCK6Rrjw1<55{<6IuFLQKNyqx2xvYS!^VPV!1=^8CBave1gnzZg_7Xe?#6Or zH-qG^KynJnEvNZrwOg`3@eId&1;?y7=CGVu=PrRQ9QVmp1Gd?0o2naI{tGyrH#xoA zDs1odnW=xCVm0lY1-`;@g9+f*-<}UfLJ62s;dynPma78rXe_s`-{uqb2Rf@aDVL8lH?$0ge zXywtL7`D;sr}n*bar1~vFT*H$wZ=CwIyivMn}vVbd^V`z?ZTEnp+DR5Z|0`}9EX~~ z;{BeHKH*QB@e=e@PUjXg{B<>3o`>F8o9q0|Q>wpmO1*(K)ziGgn$pqEz1bC+j-qcD ztktvf#8eloIeCqzA;LcIj85Vo$HtS69EO?7&AG*#HRZSKR-Nh#ShLe2Vb68dCE<3` zF!O(ouU5?F?E)h`1twhd*3^VhhGEq62(Z86Jfr~scy3M0Va^peYqM}>Y2E!|?_MGm zrw%8^J*2u9A@${ssnx1)a!*Z2ecnm62LBygRSTrP&|#G~T={2D;7Uzw#vyO!~Lar~05cl$%* zo7v*bbu9e0{d zdWt{2``3>j6y!L&pWgk~kAKxQT+Q<95-q+wj=5c%381h01l-qS{x*+4RKN9k7h}zo z;JM6+5DneBA<1Q)U3pp5=PxfaiC|0=Tirf@F*ykEey4n$S%zIw67_dz*PUincblnU z%R=6Sa;4?K%>#urYsQ?(1a~`0h<|_RSon4KW=K!tv3^X{8nbfo)Md}m87RLU+m0zR zny~cxWEW(YDNVIj#zA1FUvRe~_8x^` z3*m6i+FK`|4IJRQ$jszF?@G@ziE%>e;ar%f+MSm3k^I^0gK$3wawe@NP%VD|jTOGX zW;pB853%3;r>$wexme-^>8A_ij+33SNjs~L%h^w(+$>4g1Y;$SD?0VJ0J@~XH{BK3 zGr@MM?%u@w@vooW*C$O>K7pT0-nrB84${p{`x|Eq#RsF}gSFy=rQ#dr+ULG}sDFD> z@;pA(PmkkjX44pUhxJ7I&V7F;1+lgNJiYsu_-RUE-q|<)F#4g#BxC4OP0w53B7sr% zGL+BB!FvtP8K}=paVvv=nBw`q(qf9wq*d&Sv{Oyq;%w zT#DU~`IN>AJ;iprSe+S8SAbleW71{ot>gnekn#qZ&c~nynPv{TIh|I;^A&+o%3e?k zE>aoV5E_RrmtjpSI1?+TGqKVou^`VD@%nN-=V`}u8@2RxrykSYuf?>+D$R|NX9%{0 zvvu^mY=6I(uQR_Y_UeCChoQ3+og>)Kt#0Z%cul6b0=n5kw_1(9maB`t0{*%6&$~YB zy;-u$86SUK_qihHQ?Kg`loxpKf$E;PJ^l&(iuY&h>Rm?uf{dda?0AYUq8M)$Q|hXI z3nL63bA4N4n+N=g2mGx(FoXO8@?WB9L4N-~HTlCn`NM_Ba7lmu?F8$nl5k1+4f%Nc zT<_nx;&-mN*84YXEFC#R|4W_UXGEN9X1o%v@yZ(3GfdJq-}lBVcZ3yp==xv47AJJS zl^?nhPh^&ipmSekD|TCDM|#?eah-#R3({Z6#t!MXdtWln4Me9QW3^B7pRabTnGxMy zC;AfBvqYy0i*kQWbbCQ`dKuB_w-cRI`ejXYT3dQ!fJ;rlJ)-j_*)Ecjc8I>+`ywXz zOeE@CXaO~yzqkCK4d<(pf9+`Ttjw=Y7XJWgPn*&n({pm3Hs$=;aM%X1m+qwTx;`wQ z$(WU|9m3t6zw^`TyHzWP@Zcs|UL!J_P_DFGUpVUACHH?Hetq|DqUc3YUL+3G@9 z2j?np#tnbi*LkzMlX1zh&oF0tX4P>_;a&TD%$ComQ+8<1{5ko2%=12<%LQ+He>QNn z!J=CT{3_oNEO@0Wc%E50yy<=fYkv|~IcNBf8}G9AaFY*f$wlW2R5!8G z(ENWkPWa|SZYqO^#Yz1|^U^nCE+?j?FPoY6*mN`EVs71slWub}ezSSqF7@-#yS)?F zT6Ww)@n!DH=Z*F2yTGkG&I{d|>xk@Z{j0$2g{b|MibSwM+#@T!o(_a#O!SsLhzXj9tKGUy4?iWnYznSR={da}mRq0$~ z^$n%;yr=hfHvgT?|JP^pZxrd$cheSJ*L}<3Hm;*C0cY+g#xbww%=}j~fxgA~H*GHJ{_R}c4YqVeuDRH(xfuLcaxwVt%*8sh6T*s% zb&X4hU6*s)b20pOF7CbP*SHwMbuNaB@cf*M;WB)Eoxqo{xuFale%!>FN@N5!!4gFiM@MlwNHK@kZL=PuD^J0 zg-mEwKl}WW5e}D#Nab+)wR#KQPIrN(TOnwduQhh}db(hD7e$^|`K`j?dr^O@Z-|W7 zduaV}5sZ%yAO7^dK7IVq-(~-0s(#nqR_MR+r1v>Du0WB@?m&?p^W(`*S7PjRf5yN0 zX>m88`_$6_ZI+rpe!hU*d}c$KukSPs=zIY7Zg4J?N@)hE}VTXK+}J!?OXu; zyVM(V!v4d-)Mve~#J_uqbW{A#ubIBqjEO<~ySpLpmP)?6Y29-U#K(URAM+JmKBlv5 z4ESOwSNFQ^`)xfzG3)`E2J95a>v`Yx_R?iv&Lnfa%`3FChz@UWEYzF7c((b~tMN6J z)n_5>Rw4Coj;)~h>CNO-MVL*edp6=ymyI7nn=aBYkFw5msnmJ(mOBrZH=%nr;rw%X zzm(;d@vh+T2)O>5X$ODk3jK-ws2<>SVmEFW?Cz#thkw;@;G{$>oh;nV|9-Ql-#DDC zjNg0-Z-$FX(|C4%DQWngOf7%->t9w_u;yfKXR$oPp^Jfe8dyJhGY*gcfN@sX=;0{X zC0@SC;M?MOX`)VjM)|b-JapTUsAm-0=LatA%x^MGPZ#&n4zhnq$c>pOS}#5}bd?LP zuIrh}t(YO>bRF+}oA3(w?}Os|h5WM0Z+AU-c75F9>WbxDUVDwP-p0Btzbm-VcN zZ*`qF19Rr=SFc6^DdU!VZAUo+IVVTW`cFd*8F^dhpyyyLwwP{F-9+_2lRe&T^oyj$ z8T9Vn?+CEp8g740KfIbvxce=PyLm1~yJV97!GZDYzSZDMekSpyznMC2X0dLx=wMtu z-D{I)^;!SDz}*0N8xOB_zx#E!(=8AtRQ>w!`0!NAwFH!|{SHdccNHhpwacPukd5Z` zYV+rief>gpzulnYSD6$?lR+_Taq)nIm~VLJ@eAj>bc4-@ zzRe%DG2`W}>eX1AbAIl&^>?4|HDBH}zPyOWTr6!bEb|-1Y#o!lLCRmIWv=R&H~TBO zyluWf*XnWx;>6-SuAr#AtK#x^@D4Hgc=)#xB@dUG%rJv+Z6{nFoJwd3v7ZQpT=6?edN0@)FVNhumY4 zl|;!!LJt3SLFyF3KURLadFwS?xIo47g_!YkO3=UT`)!28-XbLSc_G=?fN#Immh`)D z{4N~-e-(~r8Ra>j>&08&K$e8Kp4l6)VMY&@3Q_557pQ;n}qvscLbPwU``9%6TU@I)tw z-Ba=U-o**-exBXI>j7jKzQ=R2r~Ydmm#?szxBq26psWXUCqEA8PtpzOHA?zVlaV{q*jyA4`3&bbgATpWeOy_$TeS ztg0W%SaGirfQQF-9gwNDzIWf>;(rzYxYIX&-W@M~&XCP77m(xU4sv{*&DHAd^80H` zT+e1U&5b1v5S1jK9^D)~%Bu z8#8~GH~&p}^q+@{Y-W$st{`qbr#?jEhfJcqN6oD+Ui1y~MPiVG7V}=cOgufUvYhzz?8+y6?wON~smE>t(?T}q9=o|rE7@tI z`7a2IWnR1i7N?c~3!Ghk2Wfrdz3(x*Lf;Q|%jNXNEtFx77p)g<`q`~JZ7*EM{w6D? zofXshI_R@^HLqQyy0XR-;@iE|(Q|*R8xgRxtmQ?K@s`Ob?9W`ryLN4CYq2M!-G#vO z3o*BHWT%;iU+^LxoC)XFLe6jL>Bj=M7s6**+*=5pMSAw3t5pnT`AFq5#Bo*}_HNUA zv3!V+&JDJwoyJ#M_wlccU!Xb7?svRa!(o1ZW4!$27O9u+M0fYg zZ$1q+=l$}7F81!((ZhUnHD$JjzsRkepu`Vj2}0- zfYi5NH=BA77ik77%bwup(e8h{N@qLA-1u!H7{6_#-_Kd6z4OV=v)-pv`6*L=#Tnrw zGtLNaewuwrWfQ+{w54Bnb~U}7O;E-}^l1j24Y~uSw@~{@16-0vn+!ymewh{9f$6^e z^ZGQqD&_Cq%<$N@=hvg`e))}#^9UWhfr@jYTu#x>;oqM@4BslcTi$<3Gvh5KGu~1% zBTL}Vqafob$asRYI-rqF=z>jVL^l)BVI(>{PxPl7h(56R5}hkjjA`Jr!dvK1CxD+P zk=tbh{0(fdI}6%fSKo2Is8OtcGt=-bOrv6Po0{M)HG!j=z!R?M@0B&qf4%vs|H74h z23yie{2Wu0mfxkb3?F|;8=GB;35x(%FKQ3k!C>HLWeq znT-m!Y(5uM>@3MM%v;RQEjr(5YvOmbHLn;Mv*mqHYxFk5Vs32GX?j3mGB$aXLEbPn z&6ctGl_!i|YH@w{ePMNKU~2z}G01gy-Tw2Jx}e4xo1K5}f0s6Q@%`h@7?&2`nLDO| zyZ+zyoU^gtJ;!^qDPDYV`8*kZ$!ga-%x^gqOH_5?0IUOte^Z&}+r0M6+p^NKTX zo^Rp1jTZsB!<*f>B;Hlmn(Bh8Ou&Km0zk2@j=CedkqjsTDyUoc7CE^qy)k0h~@f^$~>Lvf8TKv2FbA+gAUv_Q8!IWAf0#Xn7&D(JS*6o%rM@ z4=7L1pN&e*oRyl{S8AGi5li{38F3G}PYQqgMbSN^=v}Mr^Hb*aT{3E)YPV6`Wuy&} z%03zLA~$XI657^bGR_}#+wu!6bRJF5+fA?AO%E>iS-T&;#P{$2{{MXbIA%|6nU7<_ zmA*lA|KaK5eU}0^C0lLA&=%@EjOkcmOveg`#qn=>7~K2Z{M_fg+vIMRn%boyzj}Yw z=Qzy^muR}SW=%-@&wu{-`1F5&{M)eRty9zRLk-H4Jsaoa-*+>k|6xiS+<2UC5t3L; zax0EC(vmJGxkZzw^NT{u)^_xx+R^Vbl$gt=V_qL$LCs>4TgQe)9Bue9ooTyJ(HZo+ zccy<+a6;lZx$a590nu0Hy9NI=z6XEROX+&JNz>blnqD<;yb*P>8Fr^Q(HX{b6O893 zm=L;8#%IrA3tv%uy?U=|XKkmj{k+v)bN{mD?q$to8>QccP8<8=|Ke!cvq07yC1=Ex zN!(x1W6uH!|6`WDW$^qDn#vw#{C8aHHthM{$_r20_Rb2kZE0s;ZT-g1(9L@N@GOicNElC$qh^++ zW`?# zc4arH$BwMwyp}RLId;|KMvs5p1De^J+2)aLxAh|FW6jqqT#RkQtxa*1i48HDZZ6Q> z4Yu*d#hD4hCFr~E<+kBa1mh3Xt4=5AZyo(}cXra@vl%Z2{K3R89|m8!-n$uE@bG^- zq?x|^^5OB}zjt>RXU$LY@No7fEShyH_;t)5KRm^U55t4jeavjxj@N(fcxcx>@K_!m z|NY}b{|N8Nj+d=oM}3>Q{?f%c{B+J-0(OJRaW3&46}w2v{T7V7!^L7Bzoe(nF+aWg zOa1%f_&ogy@L>hIix$rP3hc1A# zN$GwJUKRGB`xN=bY6dVrKMVoK;ez4(v^)Ind(6bjjz6RmD?LultKIm+ch&uu4_eFcMOK*RHj5VX!lJwpSde9e*84^ z&n~9_xyJnGnBMDOLv;G%r~CG1hUAZ*IvMC-^hFmQ!SmhO4`1HDKNpW$cf%jIXA(~S zxMeEHXdGT{rdx;|T|VQziPMfT{5t*`-}f3^;|%fB)8~IdpHJBkotJ&T**QA&^Yk3@ z<>n2e&jZJ>xan?0Zn{n{&}gopkw-N04jLC(ZKF-HkH$-%lNlC2^4R!i?;q+>F(qsG z`+4cauRmXm=cY`IEe~Or)JCT+z@c895ofsV4_x>p`qf1f`RGBf5b z=C%BL>VtptnJ%xcpJ4eX{xaY3)Py@1Obdny@ZB(pZeH5%RcH0x(D0A9HvFes89hvoGZg6gPcQ|AsLPKO+$fm@E+$>u*HVHN~@&lM-IQpYI%F!PANJl)v z(Hyuo3l1ewu2z!s7BD*R5_xi5gZ2a1=!iukd2W9sz>*VWsyU*=L>Vg?({}m$+y4uaI#yeAe4j83HA>Y6Tj1`zoHBwyH)oE9Egk{%i zZO)beIhaPCN~_jX#AaJaHTkZq-|QM9MKr+ZBV?vbHs)N2vLzo)&Ds@B-&KwfW?fxE zq1G&bux2L|B1evBT+PTS+S+x6&91p73k;B;2uG7Wr6OP{>IWaHO#D|u+>v)rY1(DS#e2n ztKz(AHD|*P`Z39Dj%m4;RICACGv-iZb+sB(LTx^@*!6_1o)Mx$N*Tly&(W3Kd<>bL zvk|Mq$p^AX7~=jli{7JjCj~5#odf3R2IH zWDi`Fpao-gnUM&5@W~VtjT4{A575N5P@-jWLdgeLe_aYtq(SwmQ7^@04`{MU=o2Q> ztoRtP#tbbYgp4>eNR^ul;GH2Vg_Da$GG}Lr8V}HNXeFEKqe+g9$=)?XuAr&R041OC#)V={rbs21 zs1$Tue_Lkfn-}~pcx%j6ns4k=^io20u~HVcwFC@k252RO;v>425e-+OKpAsmaoL8F zN1EnZ0bM5KH%S|Mwx-@wQojI)@n3&xYf z3Ry}>nMDA_a17l_Egvl%Egmf#tvPZyvOlsrf3h6e9+{6!N5&(=krq@ zD=~wKh9M@59KA%g7Ep+=z#ySt2ON=-w>g6sNR^;@6d^1^sgmcBMk;V%Es_ta5Rnj5 z^(KcTnSzruZ+i)ms^P*cwvbO8asy?7(prZHd$0%%l4~6!Q>n3HOD4CFptQ=^ujpVb ze=&#!Z=^X%6sUSH&Sx(m)T=b&LrRuR$|3lIiE1{O5>=)gQ!B=|VQ#wFVO06CXbl-- zLBPf;)v@I`^0v!4i_4h7R_h!YYs~AHdoFiyVR1m-8N-KZ4Ajs zKH3m5Kr9VRiY(qZ12%Um#<~L;+ajQ@Q>{go>QgXTe5jru5(0!!g4B0iVKMqFW# zoOS)J4A4?`ShKaMd4wEVgg{W4t5=DN{h4A9s~pcc`lgn&fiQqC@gQd1*m(g3X_%k0sqma-)`+Z;=# zYz%pHr4G<4Sq3BCv`p9x$E0>_%$#B|&hr3`ISI9(4A)vPs=B;u(L(hMG1vi`Z=o=% zaZsHJh^7RWJsL)90qQunW}Fd}e;P7iLkzVB&(3%Zg)^}X&?JGR>XW!&0{WVjcZ;*S zwCs9i`pxl15^5=hePm~Y;S?$oQwXePvd!a4ODf8}Aw}JMs`1vd4<>jnp-CH{>Bs#r z_|}-Mw@_0l&I`9dECq0!TdPGNME2FDl5B)v#b&B4#~QfW5pRjuH`S@Zf7KWvQE*TL zx0;+I?$}c3D0mduRTCd;8KKprs=gRTEM!NDQ!L_xt)_}ARxp%ERlB$nbm#%v zx79E;r5Z}kSR!Wh6$2FDqC`hBrd~O&wn}1{jkiUruxrd&DAvMie=JwIa$HSfqxCJe zQq@365=sS8nkJX1H;2U@h$TTIJy#lvn359CxdN?)z@?K1P^r}yue&*vSUdcRJ8)^W zhTKAqgchyCfDm1we-XnDAw7M#ZxViof<=6lI2iZtT|K~ph3XuTSHDs{RJsF zPd2++k&{pTCM5oVDI_1zBjpsTbs4<3hE%Cm!k7kVwzU{DC8zuld;$)^rwT=RKK7QW z_yYu~5{e$6Qmlbe$zF<2t$6eX+yE_-B;zeh@fOH4gceOJe*v;I$5zI_ z;tr{_<_#u6SB1&@Y9b;Tgjxgj=L7MFlu~o0Dhsim%PWd&;!{LV5;6|ZOiV^{C}^5< zu{g^yv{0dXf3@$OAD~eV=%Tlc6G=+?#T<-WYfPzd<&G^~r(_);9UUERC|L(bXO0ps z%w!P@Y;7cVfJo|3vdqauFRk@z5&TyI2gH`VP$2-DOF$D;EhSq@NG6#94-Q+h**8pq z*yKXu^yI|e#44^oNh=;aq+(ku!2n5>Mg~!Bk?3*_f6~#&$$^O+iP{l0ICjN`piGn; z2A9P33d_9Nj+M@RA`>Ax&E5xP>TymLM6k_ln}^Ru2ya9 zo?7luOCU~MY;84HHbl{)6&A1NW$H$7{*XQ8WZ4UOYl63_cyu7%MNr>l8lmaoqXb)P z%Lu_>^VwNzd}(dg#tf(FobrI0f}9WR{Hmp~Rbm zb*|c!*qSKGl<3v*DXtYLDM#Z5Xf>Mzp0aNevNVKT)#;d%`Y#jSt#Dn z7qF#BqvC4;%t9DrjWr2*qVIw?=P8#EAW(){xU@o?OmbAI2JXe)g+qdfvG``Cv`p%( z%8qjNMo+1&KcRbb$f0lp2`v#gC{=BB{v0Pkq1kFa2++VLP8f>!!4q@H*`i}k zmIoRAI^fW1p{njuB{8Z0K(eonC53v%DqxDy#-b-GhaiDDkfjuImRg1dngiuze}J4} z&Io!|a^2QPR9kBmy91D?gPwlKa*1qeX|@#4RZpWPCUsl&3JVUcc~6zp?Vdu$L`X3( zxf-*_Y)AeHWUZ&zT1GL|c{Cx^)ItkZEsv3Z4BPBY^qgDOO&*vsV68TZi@sli@;0;* zO#qLgjA;yTYoyNlSR-*7SNcsge@s!)Z=TdNU^E4Dw$*kgZc=0Ehuts=7F$i?5NbvB zStKbX7?Xo3mVEBRKAT|_iNw_!#Kf(}tTs$dF(=hGJVbrGdL>ilhM7gJdMg6eyWE7i zJ74y}Avz#rYg;o_P&8fu7)!xSqW=Gq+5pX(=&PD=AtB|=4r*c~u~{&Oe>g%@H<(W# zwZ$S7flYLJzNv(Y>=9a4Pg#V}g1EpTCWD5d88$Xl7jS^qFj#buUMQ%MpAXjT{1IQwFQOHIcq$%Ph^QM}s$TB^>rl&sSO zbjs1IBfN+b)lnNFV|2(?e}qL{w=L#YlaZEUOMnDfeU0PXqBGWJjqo`RAVrjORkvAo z-V9_uxPr};f|N@}mlH^1Yn@HX`Hgsl*0KqqkTEHi6eNL5U_wnADl8Db3*InRiPWMm zIVTs2trV~&w45X6-qqsyKp~@vy6?MWp@bmh8nPf(V=A=)8c-mCf6Cw?ay1ZRWiTdi z^&n0B08OGEA8oNVVfH0C&S0R$+N@2ncjO}-RAmK3Na_l!fo);{6i7ydO0SRt9|Ii& z9s?YMIr?z){^;G&%h7Mf3^mMCtK$@#_}D1;1_afX*b)lxAet`&$}W0C8t_7EB2a4N zTMkzBGjVjIWUy}VB~87{WLtIKR`O1;84<^Jlnf40fP5hnVkrPAVAQ~*S4-E#k;0Q6 zH8~im*p4*O6Hw8#0MC$3jnPUm;sP3W&A~X6Z#6@Iq&zltS+H(y#!~cq9Q)HX+5?8-S}C5KZv}j))u=_~G1(@icghBP0MSj; znB2%{JeaK%ORl6)3Z>o(MSD=^0FZ8%)mH$G!UGpWxw;B9j?jEDfT;v7j<_<0=3*`} zL@8c>pf?ZD9z>6*5WKAzO^Jrp#7wppbyG`Et6&c$l5LS{tK4!7=t`j&DX{wOu-O4x zgWv)-PU0;i+7f)0fMUI1XxWd@nlwbBsPUDmmZgoRWC3W-Wk2Kw9Fk+gR&5ZX=&?GY zhJi|B7re7^fR>@ElJ!MDQbnSHC&R&6^*54#H!whhg0UG^$F8P_M3mGrYPJY-Y{`x^ zwH{iuC31ygipJAz@WomE3`t7v``|5tQFpnuB?q5Em8u-))q5Grgg576AOfKpo1&LZ zb^uvCsuk0_Y0w_5cw+=~_lUmQT-ED>7NAv|T^ymY%id6Au+YRdiP?tKN+F_XQW#f% z8Yxub=D=7WJscaW1O=PP@NfVL@>12xMjf}zz>QQ}`^MR-chWiUFb$&lGN1rfOf)&G z%2t=E$zV$GRb7{u#yH9;0fNgpalzD`AGr?D2pt5>Xs{R!#hV;ksN6XDtfs{P zP2I}5i8m0lZUbyxM4uIIin$Me(4aej3&6@qwh%(nR4S9OaP(CpHD!R-pjs#hQls}m zm{Kk=dx}*cj~dn;usVrgU0|`G_LD&56isE))0_;@7+OrC32#zOmKG>@f^1c6U5Y%e zw1g-w5w_s5m}Ww?*0T7Hv3lb)sE0B;@<`QXYpp9Fl3D_iQZl5$B6bIV^}VHFP)L1+ zxpr1lCU2d|CR-S3N;Lw2wVFsJ;&Q9einkJ-k0{>if`in$m(`yd9xgNI7$VahjKqV=b9$^<>buSS(_%ul);EYouD3s3p!QE$G6dB{nYC zSf!6mqI)4w8%i*(dQ2RQBU_W@%3eV8K@mp^qkt)=zppRpJbG%Uvu_|AH?rb(#3^p2dkCzmO7G3AVG3V=yoT+R|KXHG`rD$IF8V-(Wx3OS82N~)$f zj*d&F0?iN5Ft)~e2y7fPIEf+=IkybSdFl6BRRW9{OLNAgQY~<;)X2Fa1)U3hKs?Qz2@4QYJznmiGKkoG)+|o4cu6( z0Yv8-1g_yPdFA7YPbr z>~XZ6H|_&CJ@sVCs&Y(rg;?`;eak7u(laR>LP3tq9AXVdWj80Zp%tSs+3Nba!J$?4 z_ONdP(Fbq5O@UmcRDW!#Lk6*exEoq zOA&(xooEQkD!7E?y2L{z0T+^7qvn!=9=&6~BN7~JqL^4S&qO&9g&0Gstu#x)_h{;7 zXKlzBqgUHgvc$$wycdhc7}pCp!6AAF#UoHiPaGsfM=8bxM%k3qrbr{WLV6fHR~T@$>75%r7r_ovNghj)YLlSU^z(hNq?OOU_!rVbzEb-v$f@{8%8!z zt@XM$E62q$q_V@IU^GC;g==drRZXMO8)DXF&ygoYiZswmxniLA^i<&|RgeiG$ZfoLswXq)-Cb zL6_Pi7(Rlb11N8q(yUJ@>k-{Z)l}CIjf({a1Hm7`xFZ-j1Th+RDVouh07~bB5ucKk zfQ|>Q3{!hFH5r>zGtL@@QgfE5H;}kS47sk`XMYx_5vV==CZN|5XFxEcGX5p;cq z_QvGuuoe+35WpvmSI49WdJDZ02Y{)4f)X^A&@Mv-UOya0N6!qDYS5U2T^2h!<1fI9%!EBWU(NV8?S9RXzHY zt!ns^OcHUyY0_%W6o=a+{s@|_3UUOn2Y*W%>~Rp78JcZ1s^P_1o!`M{JK<^G$E(3@ zT=GryTwh!vNg?T-20LUdt@~ua;xtyJ`CynZK?89a*jdT3&p`lK_7N+gde+dEU~C$) zSCj;oNW_^lj%R(?YXUZsKqRawCozR12#VDUEML;xSiRZM*g0c`^**u2FFcj# zu#Nl7p=9jRR%(NiQ)$K_H&3LO|Hw${k3qnAFqi-xTH`cJRS29^tEp{4QvuNzF6h}P z5A&0jLN5Vblg2_e0k)I~N3iw?mXBcRAT|)UrZ>WyYsq*n#aL5=X6(%El7BEPh_;mqwOCMlGKZ|k9}W0% z%Gl@Sg7Y`QiU~~wuZen^a-rS`iNHdJY96wEz{wGuJ%ZySI68vEBRGFJf>T`ToOLX{ z#UV!!dj#Pl2pxj3DG^eIq<(=Wnu3i9po$uqy?i?NRj_?w zxMAM6;Zvg=$PjIGz?cwI3sG}ZH6Ozb&p9Zs-Ga}oS^0sYab$u-^)Do{7-9h*xp!mf zK6V4F!oGx%ny(Rz`dEKL$SpVUzJhCg2nh7_qxYC%8Rq)+@Uy;kAyK$g2xx&NwW=Phrb@7wAHe$~csC3n!vMDd7p@vwiwqf@ z7hq?q<{?;T*q|S>BDsT&I7~k1KR7~A#D$y3(s;Hg*qBM0x;=l;P;^y6iO|qTxhM zCed3NzK;y6mGzCsEnsuaHgMwRie3)T?L<;cK+Wc1z2=*btM}#DR&{Nu>rXT~Sj12a z0b6nX2`{*BKCVxZN-TobBohqk5j`bi^u|w4zSml4;D|=Y4@U_8+s~nt1mM)1U`Jq* zl}*VR6_PP`CxL35^JfxY9J1hA7bE!zUz~8MK^!L0~&WkBj05% zB&LD7$MwAns~N_%))I<$>gx%^Edm(k^L^&PPMt~tyzx@OQgJrqP)#AO&G`5O0``-b z5c7Q|QuWlDAb@LGth#zdlC#|*#Yn6_AjmKg`o0r!lEm2JlkKjAYaq2&q+BxvO#$gA zVvh*!`%k8HKJ6sjM2vsFa+8TQ@QAtO+~$+v?>-qaR&Pd;-VpT&#uv?I<|b6F=1l&8 z5RM4`AA%VZD}iUA?4W79uxaLm(|kILhWjK(bO%SpCM*`axTcSqrU4ZUQ}F;pA_w|I z0&g_bP(b71u0*iS2l647Na*_bA%=s|R}ErLnQN{owqi+x#NB_fKwRtdAjlkA1ISGu zGvKCgaOj&SrWBIcnUsCZPo2IK1E za!NJEs+o8aoSR$<%tut0hc6-9CeBim?16F)uIXC|g*1ZP!{vib9;2;>tR^ydw-|~A zbs%VhaW$ix8A*SRNcIqer3heKL5zW;@t}7<69moW8t2Ozz}J_^Vjp+1RpSa=Y)+{F z5c)M-Fr*ngnkW*RbtG(%b9PN178{P$3RgpY6)VO@F;mct_mZ$;fvO3tGPx;9+y8&P zok^D6II=|NZ#97Tz5{Fn?f#eWkCA*KePu{l8I@534MKnC5d^^ofVz6a40|ei_m$mG4dGmDOa^*34?;>=(89TY9zIh;FxU0ah>BTQ5{w4S&Jm< zn8gax|27R^fcG}@vt!rTHcLJ8Ot0j12;(V*A^@@Q2c5>B9$Va|mr;%*=+7Gx%sz*W zbUlaZy@h}J?AR>4df3z%UV$Pjt|C0o9P}1-{2aFYtc}r;{TVf{vbA1&*69ZQR$On- z)pzwjw$ZcHnhQnoCMX&#xptmBJ5ZK(zfa0P+E8kwwUJ_6Fs9K+ypdQV(MBS#gYwF% zgU&%=?BZ%PK^Pn}xjbSvd`JF4o88L*1joto!i#?_GZf?js&}56b;9@QAGEplSw4{> zT5E(ekF1_v09l*stvs-Q)TZ$u%e0Qz7FS!$LndliiK#x)L_@pTNaNFcLNhLX#ZbW2 z1Rp45-FMfrIzN&yqrbLc^`i|G<4Fw@sz@&n?m9;0VJPG{_xn$#jSyORLSVevO zE{cB+fD)w9?HE9fRmWY%_m@!8PoWC3Xk^~V>{Wt9cWx9B*gkZsr1wMCOGUB%r{SO9 zw1w1zDKhRR3t56NU3v^zv2ynLH1zSCw&;vi0g9T-hCpYxw4c)_InsQ%U1|fe2eMS6gQK;h}qnmE!yh9%pC<)9)2zMnn za&P3;$hDD6Bgg;IHJ_8$Mvi;^pN$O=B3hteFy11TMYk@l$Y`R}=Dwcq?L*P*0mbq# zlzgtj3KiWdGky6T;wD5mzOfG*CCA8dE|j?E=~3(Kw%5ui``M&N{oX!!#8y=Ecus%3 z(A#u58`A+6;;H%MZ|%can?xl~ooBBO72C2TwK%p*e~_E>t$ol1&AI5<6nyCvg-~Bw z-JJTfHVpsxKK~_jJfYYWUnM7YHszcHx@(@*L1+C~AN=O{wKzgbXTyH6@-9$zE=}lq zb^6~PPZ+S7zA0#ottTB>7_%MjyFgOD|@1VqV*Qw~E7W8)a22lkO_|K0IP zWoJNSsH^m?rH+yTEt3!5{O~yGx5qmjsQF6{q_sK(D$@HLSl7=-9>t|L#)dt!QAVTm zMrl8ugVaVTjqq$FHOks3%a3Ovem{OWO?!!RN=I3+(?r$qDb$q?-x3a{?>m2giHpRwzMajfxe=U*kwXwvL51tnEu^inFUMYc~!R8%WV5(q|J?H1| zd;bty8236K-+NjhG^{R${nouM;v(O7|4q26?%_&aD&k_{t^=v#>NkU&i#IOTxaha_ z!=pmwiH#MimwVkg)^yP9wv=0m!v*i*_dSbaqPD?SSqx4zKwX=m#XWz^-X+&uYvcNT z-$Qqr`=tA%3fv0;b$1FK6Xckm?*V;lAI4tOO6u5Q9f2Fog?&g78*UGC_=>^Zf%NZt zH%d3ulOZWAj5ya82q%oCu7})>AmumrqsU|jciuSV0Kh1IfLk=9Qf2mt^*aR)$! zQQmPCa>Xr_Wwn2gxYS>gU3;JkKWcaO-piTF-Bt-1ah@`zKOKLOL>wYlOWc|rh=1$p zlp=9Mm^r+$Mq~Z`eh{)V9Tgd_-YeC*iTm8by2kc>ujfM>n>03VY}D9lV?+P)Z`+?_ zG$x~}@9Z-nygw`jKq070?r{qFa{C@JN0&=DUGyT5pfrC2GCw_Z176s^-hYsgKzAnD z<=CFf^O#TqBX{2SIrz)%L$tbj>>|eO1lEoPxYspeuE*yf=*#VcUQ_!8#g)1%>6qzr zNk7@8KI=uZFSkE>p>EZNR@*caPJN-EZ-mBI`qSk4K&{KF`Pci;1_ulkFLiYqgc27S)(d3(H<#yb z?`!R2BA+hHKJ{HG;VNik?1sDg&eRz%@6AQ;V@?P(M z@jNw-6d!9AR7VD1*i{`>pugPB7#Lx{zqOwK{kWxWqSb4!QahG9J=ffUb@XwfRNYjL3vmnD-e{|chPwz z!X{+;wd+J$eNjo7Pre3a^9MHp;82~It5!&oIsmw_P?7dazWD`I^47JF#TiBG;>=T| z&U0B9-E$o3MxNi3Q7L2sH8y9TRurJE$bxTaeeO&CXy0|)7y=yTF$gIO6IU;SDARup z@Z$KXKX97Lbn>=B_mIA2W-lTl1BVyhVM5+h4#PxX07I1PeLrTAC>w?UrNDK8)&Oco zX>OJAAz^y4^SW&Rj{ET9L2K1PWsZMUsy%Z|a^s{I>af7jEy>np187}Q+%Ht6$|LGc zZJcubehmO9=f%&gc#tnd?y9kh_`2gn$XC37Kg5?qr{VMT6OgrCa4bF1$9~ouX&=95 z_yk2S2DqUPxC?=rKfuK)<9Rj_1A2ZB8NdcuwNsAR!#lWbymRc*=To*W^>u$}V;i=% zjw0QbYrnKnh;p0d59vuARpBNEN3E@1jyNQO)u1i83-@p@6r#?p9EgXEF{WWymKaO= zqx;9b*d}0$ECMTPU=inKcrAN#!KJ;90_eRgbI)tfA}?wPQ$!yFP$P?}1= zd1q4O^YiMoFkcBONj=Ia{h&*9t6R=Ty~=0DPH;pQt?8F{)j5Z}Ze-Lp>GbiZWB=*+ zO3~MjIHK1^gn7ZrkdVLXu#!7ZJn7f*6~tdLMxeFhJvHhw&R|p^VGDoG)H8xU8{hY_ z$^$A-CNHz^DIs+yz`(V*pBwJ`>-fHpEz;Ge3^=vyq5zCVKrxC^L7DQ|7=84)(n=Z@ zFk=D%pf9`~+cejCJoBVVlgdphyklyUt1q~YXj1$&=bERx%c1DqqC3Y1n``OJ^0PIN;HfdtydB*mr-_T8vW6Y}9r4L;u(YkcT~I_jCFhuv0S49f1GqH2=s~{;3W4 zFiq@!N*%rw7!VMw=NTUOOkDk-KVQp2q484d05eQf5h|>mu$#5I?wUQJXhPbAqzS>6 zhnf)3;J8k-A5E$^srJWnjRiq|7@P}BXB~Z20$>pCMCGo_6Y_t5&DlHW( zN3?^0!ncfE*qX35VR+f`D{JR0S}uoFPVaJt?Vx$iwlnTyV3s5}Hk)uXLG2z04r5xM zSlCP`pt4U)i_Cv9SKh}-6WA>Yy<`n+NM=7kn_lxa=KaW+08sS%_t6BHcyQuHUzRK8 zSe?N7nX7bV!V-778QJ|#i`FLac>-jf;pAhIW0X9z8{{SCnjVGb;pq3;LzM69QM&r3 zC_GwWT5JHevb<-qS_SHT+&K+VZ=&GWYZH}g3_4)DTAeM3I$Pzl7Dv6g-l~N6=)ne~&@=Hn` zdeRI?(gf~#D6E$@5n!zR>-yLfuyzq_6o+#$KO37L_0Z(UUGt~)F?@Zyo5v|-n+-Xa z@BvUIXTAj}Kd+C0W$Jdo0<5vJqK0^c2h0TBZcl%VpVzws&aoKUj4pccK?kNw2t(@PY5TV)pbg7gR<ZIMo}WwkG1xzZa#k?aDj%skPwip1Ky9KwF>=;L3kAaff6j? zMCNYdiBVv^vB~r`ejQ(k#Hb^B-^biKU6K=LN0Cy(*d_yUhuXmhQOO=OMX9cYv8 zx>9c}!_VV8v3*uL-41UV@PZYcEL?Y=dD|?D6P$|6=!eS$&#N>1D|+uT;K5h!eYSr% z|Lg4?+hElI8AA6u&!j39?jT{w{5d})?oHg9xHfTlVb3!bCt>3P8!nFldY@8I=UXZ- z@F)qKE1P({7H}+!ykGfbM@ZFSsW9Qqd-lisT%_-_*Fdgn7orGg61FP5Sop{D23v!( z*6IuHT!*gR3#`y9fJOInBtb6_*>Hbl*s_v)ucOTADET>{0FL+X3Kr;Pds#$6m=jOd zQY(w)h%?{M@4+&b2mFyiNg1>662`S>!XRdU?7>7PARHUc-0Hv%07d47bDqbu@%m1m z7&a>J^a?(0#)U#)P^z}xwb2sKJ|gfB&jO21cA}gpE)-9 zFUQqwb9K=B^YCR>Nid2!eZiCTUN=k1Uyh5@OQs7%6L3K^T?Uu}AB1Y6+{Z<^8byc(571ZaA3fa;BEu-CqU_?&|Qn9MVc0F zTBvEc`>N&cD|ob!eZs64?%)G|@CFxj&y?Gzwq(;1O^aWB)?!V|-RD@PKpxXk0lAJ_ z0*Fb2_~7exTR2|#Q?513cHlArcaM1z*k^(%>nt)bx!lIB6<*8r`u%^5ggeW{mZWlg^F59fP05>*H6?9I(v)BgO--pbrE;|e1QA%uu(N|`%4fjn0TBAN zA6Tw3-N!QArP21?53ql3#ux=9^=qCo`(V$WgGYH|kd$F}%`XuA#b7utr=F<;1TfvS zgkctW-#fwYvnfYY_NHu2vDUZx^2_#W&w>!!hQAe7g*CSLob@@EXj42d!cC#~!SPaG zVoURn$~>E3??aFlP|kpiQEv5;&k zaBFlJwxR0%6!?P|u>BP_2xHH;<8}SeOd)~YV;`iubf*uB)sy$~wViJ;+0T6ntV}em zmpLG8lrdz?3Bq}`aqsa}Z?u!F-Rq{D9)~CVSE}afbOI2FJI1BZ<)B@LNm2~ILQk-v z=&&z|5d;ds?GtFM^8B_4?ZTJ@5p_-OknZI$@M_-IsMl{DJn9^0+8*M*08~qd7WYykkvNzX0- delta 22326 zcmV)JK)b)#wgHv30e>Hh2mk;800030?7iEP967Ea_#R(TZ@qhDZAM%Ol53^5(bg&_ z(yUI;!yF46+ZP$H-FaFqsg$WY-ShQp@LRZhxJO2+q@K(6gQ_BV0YLx+K>(!xAOG^h zgV5?RX=;;dF`?*pX>y5)lW|T6qc>s zWs#iRDXe;eIe|G(XI%>?z&S?0#MkjpPhG7UYX9x?mwI>jyk&T)$mXS%$+i_&C+43~Y*G`LZyU?Ei79NUt_=eT^e zk4|Tct(TqlczR`R!D4MaFM@x%l|#?<+F{aWx6OHVz<(f|HOd7Z^UBN7{&udsoHv{h zFXyGDcW*AIdqP~6YSA``{kC@-6#4J*Rx^9i} z-#e;q54(`sZG5)|T-NPix--#>>TP^ChFweJ_R5&;%w5s;=<8NHl7DWd1uNy!TLQDi z@ndHU+$7)BYEOYI8s0W&eERtA;ltC(j6ZHb;j+(d2=%Sw-^L$*pHq_{0x^FpWZ4Yy zgs^AjYV{R67x{#=Z|NePkoRm|v?p{Y^s6qiS!%lqzXlOb7{zPHdAna>5%%NMmUFeTXwKMCdbsK}- z(q*lxhfX66f9!Pda}Ay`M}L3pH19Pa8%p8>)DRZ!pxlP&G zlJB#;y}ZjaA~5SS$=S=A?+NqR1O47wa;_HI_q>*?OtiWv*3SbwEn}M+FiGK z{*3vDJ>|P-bCdqP-s2WjuC9vfQiltvdwx^>)2+Jkxn9q6Yu4?WhP>WmV;Hk{@?TWl zt(W^PCMRAoIq?~j6R(?`c+KR*O_LKhO-|f4Iq|B=iC<}Q;#ZiQ_%*5vf6Mmo_atIf zc_~YHqO}a+iB`@AbAo>pt^5yLJ-1t3xOWsQHYbJ)T)WcM;N6NlF|10%4u~slFA;&$ zH6O~d@{%Syew%sC#mqy`kDVbes<&vdGwiZ%d#0Oyty#_H9CvVCRqoAn6V*lC&K&nh zw65M(!%OeT7UnDe$%c$lST^g5wy{~aQgBbd#D@>R>UekKkAr`Dciz_ze|q|J{Pm&! zhmwEX^L~BzuW$Zar?o!U$B*xSt?B~2pZ{_9CO$rW{*s@*e2(wmEn4;Paj!u)w{Ac@ znfOpn=FJ)toVM&4CaUY6wD@yv?;h(f{gRFkA4>h3Qs5!?CHL{i6OQ1P&2^yMBma84 z#R3iJTv?w!e=L7ra(z?^$1cdD%4VzdZqYhE*7vQi>VB>uy?S+Gbwb^57vH^El&imM zQDQIqZnwGXHO&mK7+<}LF~yW)zF$^o>7uA_HE|41pd5n>j=`4fteV93@FBh*Wer!A z`OD|eRl5(>3)!Q&?9ra=(I|Vg*Whk8lO5TEZP~jr6S#jq6PU~HU%xyJqNcvj^zrlO zkN?pN?^2LQAYHR%O*i&X{^$Dn;pyE&QSk2`O1}^Oc%qqb&qf@?pH|{OYq45|xD2pF>)ctbJi{>K`TnoHWSqgeFGD< z*%lM~@-=@G`DB%eb`vokm}pmvdR(X%%USWBLm0#|#+bWZE516()<|Q!T;uEbpOnlG zal1kM{mGx?tW{1v{-`B)KaX(7ntfbey*ewU%|UiG*x{#c(W5G$cR#)V_@S2Hncw~O zFQ=2~_dFQ)JkUMw;lr=-^F#dbq~bnqia2hHc<6tD#fNS?A2kYe{6Fgvo~t9?Q%5|i zBi?IpHy{tY$S*hSuI-51d8eIA0&H(BaIs-PzhNx<`e7~ms{*lLz((UG17>5IVfN;Jvvfrh)6HB- ze!qWRyrf2F$Sg|mvhQ}AOB%fW@a3=db9}19%oOG83xmeF(>QlpEesw(@M2-u`NFV! z3&W0*Yxf!~rE-&aa6uC2NwVx~2Zkuf#qyC62|2GqzeO$gWr8 z3E%#*s{QyO*HIep4)M!}5B2e>+ZyHm{Fhz))$5(&!~2fCJ?nJJbKb$E@nKT=fTLivFCV%i#3Y_D3e6<;Fi8!_QqI72obr7l$wGfB zhlG<=p+;*?5SCC72O+_g>4oDV1DD!xR{kO`uIant;$|iHTs)8Aw#VSkypy+=Je~dw z%RhY=iJ$&dVTDBj_9DG8*eJ#mv(C((^J@Ba7^Owsc*?b<%=A2&I!fB1! zyh<#F6RGoXX&IP}LiAl@v$8g((=W|9Hel8tfoH$(=TjO_#g|-NbpKO*>Kv7_C{^cU z@Be&)6WJ5F6UiGr`?%5S?C=`TJnn6GFd9wW6OD#6Np~Dl(|(wUABH@`_FaEpzX@26 zF+WaC*(?V*!w9oBecxG~!k@aH;rHIcailQU|KmQ^QA3fP{rUE5$*fLsyH92nOX;Nd z#}mpHHBdS-<9K#CA&oV5MP_uvkZ0Jg>$}N6bZ0Va)36-iT;XSJ=49^bI{4v|%$;bD zBl&$YBQ41M=Ii8rp}lnp_GEu`YsEgRTJHQ^?4sktywGk!xzcjj`PXwuZrlRZvkTQ-eX$sT)MWln_WqNQ$B z9epC~bmQdKh-uU+)GJ1u^wy+ra3Xt5gE~BsIYZ^HBVU5#nM#DY&NY8Cm8hC;)@Gp+ zwQixV2jHEulyMllN%p8Xjx2b4LCe*jyIjaOkbNQT@fK;HXmpdbs|YjYU4yZkjlZtI1Pgi}OP*>hf zhu4djriN-(4W2#dv`c?4lkstcU>9tf=@xroCSU49h>yzrEq$o4-3dFBWm9$a@*#`q z=E1_-Ab)&3Q*I&`%vkvdXM({X1bvG+$>2s2m}sV|!3=YS5eAuV^_ol7V6Iawj*v6} zzO}GA=y)P{Ggn%(0kBtRu$;Emzz*SFy;95U z@T(81t^ksizP;;b{*92D6HuwGpdYr} z!yW%8@9x9&_v5f8zZJO`qYoGK6EkGP6=Z{s8WzZQ z*4fzyvBq?=(fYv{PfX{*nDz%_QXc`$2V>Zn@C-Pgc%~%yijrVe61-3nJlow^PV8oo z+!aVpA-N@*Z&te{`xDP-%vWg4N@EU7%sO`oY|*$+t{SM#X4_QV*z#W>>AWfF-Bw|H zug^@~uK9m&-`=k!c`m8EC8=^Dsoh|*JRz+|l2OvS#(qaqx=MF$cIH%HvvhndD6Jkh zKbPxUDE;;ZQun0Xp)z;LhuyL2%G`S@Plqd_iT?YlK=sEs#I38iYaEutOy&OEVop{b z{fS|ltbS_WI~O;Pxb!lLqE~BtlcIwI*t}Vo&1Zju8s08!`4jrHE&pbI3czuw2`t|4 z8R--Kv>7i!PvvxOF{58sv*mf{jkUSX-#n%IE2q>OL{mM@JEAEa@7$Z+CDU>A?LxGA zQJ#eALNq6@@iau(mz~i`{Nvbo(vib3Q@J^}n2VN z@zsBf*}Pp)r02jyi{6@=2+A;wdL9AxXPk!=;2+PeX*tZf0%vU&&Md9FU+mpWqTiayEL%*Uw8X)|1LT7O64*fq!)M=pv|iG za^TsYF#8KuO;>fR^b_8n06&v{vPeGK2VE2C8sWL@OB!%r0d=O(D-IH zIdh!~zpei)e~eBzW!J=i`||01#nVn+RkY>%8Gn?RUCkgR)od|!w?%oXPc|6vSiCSY;E}pvV89D>yw`1EeMMe{r zUZ3oO?J}k5*pcmaOww^9R$f87ML+*`mhra`gfIf^9u(BoR8$sW*>z6Igm4JHGygYXsmzm{WZf` zmwt%-=09zr`Q~DZ6QrLmh&v)X6O(pUAD7rqqujibt}Tq!dR+0TzXi}G4Zi8Fz@8bl zQ+4+y=8u2<^u9i6qVfs+eC3@x4eub`+_b-OworU9Dn3{%K3FQg0oOkF}4pQ zlY{pfoHJ0LL2)aCe?akkUul8jGijAOdv}+ec{QD9cGsmno(;@d@v5|EO&5)LjK4o2 z<@4pHzI2SR(;0AQr9u~1f4G2ghM%XnNA9j%F2Lp)_Lsqmd`39sY_@;T!)rXd<5KK? z%uyOE^c36eVs&OXT>)}=j!BoTw~`O^K*}3zIv;};Y??Xb=6qTe&u0Y6DSN>wxJYGa zLueejT!uBT;LNO;&df@e%z`|d#OurXoY9WyHg4(bPCcc&UkkLxD$R|NXBf7Gvvu^m zY=6I(uQR_Y_Uctfq4R$#I!Cado88oP@S03<1$48CZnYYHEmtRf1^jdKpLc!Md$Sam zGd+I4?sH|GPra@SP+riz2daDG_V_3CE7_mTt9Kds3pS4HV8>H*5yg13K&h+xErKw3 z%=K-FZ5i+@8SuBtzzp&W*ndf;1^fN~)a(!Y><*2E&-MPN zRQyvauJ!&68%xK|(En2B_n8pqnwhMGYqGM2^^B18&G)_WDji`Z9XkIPh{XxrZ{w5GF|KnEal!hFwXwtc?cSGya|6?9$XM;u{O7YBYi3Nh*O|VA z^(@or!lGO=-Cln%onFRt`t3|7UH!6VI;}0eF~FrJ;2zU?lWiACNjps6?tKvxd?ph0 zEwq4|&fk0epAF}$EC1Tj;@LI7I$8V!R(sl9?J+&K&eP^Pe>NPp!R)0wX}qov%V#oX z{f}qK6(4i=KK#P70%7#5z*TMY+sA!#RirM4>R7hA(AB}Y zDw}Zw_H}>R?CxY-O6)VjnVy+-98-ALJ|DB?^XZfwnzMXPJ|FYE&*yT&+uolIT5X8v z76HG?Hv|h==?b0~mX2<^AHmw61k23N^sdD9CG^{debM@f5BGCH8duM4^qJq8(A1(C z&a0|hH>y>)m1Qum>bK2h;WKpo-sqE%6BK_bMdu4tH;K~F{5DDW=0k2OgNMaQ{Y7}` zn=zM&Y3a)_(;k~{MqJ?5eK_ehH{&-JSYAHCZYu6*8DzrG9Hy5qdi zt+|fK&gQ=g%wD)P`%6*ZV%vW6)rP}2j-${_;JUZN=_Xk_A$AwRx5b}U;!n4V|8IZ9 z=BtGMlIaVfr~fU4p7(`*6>`52dj8EqKj^2lix{qtNZqUDy_Yn!F;b7zkP=A^A9oeFH?V__4s3+ zDIB&lg}YCip8Q^>@ObCsd-ShmAKRW6aGwCb^+4;89^dD@fBIY> z>*rtNa5Je37yhy+eK*|lnUdJM$5#8~_kpOk)9Ct(=T^u>R`s*bFB#!*iHLL^PQO-f z!Q1IB&~z&V?eew8?p{w9?CyV}$nz?{RXBVvYV{3~@p=!fKQ4mt@!`Xt-q)v(ANsrO zzf9Hdy4wo;& z`JZ1ieXSW2!}9O$hP;1UD*5iFbuT#(A3uD|S9JN9&ayG!i=kZI>$>l^^$f+Z2V@$s zQyj17eb?Jdmwh=~nd@y{p`DlL@b<<+z4?o0n_s;eUsG9q7Q${7Qvc@I3W}fJOkP!l z89Lpw5tq7b{1Do7k%oC(>r9tQomX$U^Kf|+x@Qy4KbQAQS$=;R?+Ol&fa|ZBc7U$X zpV*J;0Zu1&D*9v!X^1N5L-X@=XTcUXGV0>eOdkpO&A8 zZaWtBf@1spz=eOE`AvrD`Ql#MK{gq=fr*m!;$uTsrQqtkol~Ec<0-MSHOQC z65lV@FYEg4t_RPqk6T<_v7E2hUSq7cu`bK6OWXTpjrH)YuJdMK&XWD=)wn>)xaD5k zQO-cl$x*ZZ(@;Z3-qtzjIT(vArkhlUsQzcN$GeSwk+gp}gWlcy9Rc=R!>#FuSF;Is zzlCu(&&6n$Lef7tFrMAF8hpvmB);@FQ^(CL){Pb&jH{=6ZSt%>>%SMc8vt+P;kE8} zzwUOr1;RwCUmqSHo@%+4fYP9gp|E>iZ_@5o`ME;ED*>oQ z%SF1&Onz=j&ggKM_qr`Dca~tWBJsyKVj5 z@xA8DyC#iw^8josHTuw98+EwJ_Vvj2S- zm|R<6t0xOK7MOga1vV({>+4EY<1@?Yn)bXQ73QDI=%35zpUdc(Wwg0@T|0q28@bhY zV;6totSV8u0D6+LHdcIR3df{{Ol-o)whme6APA zvC*wDw7cdL=gF~dugLV^8t1bp?)k@Wf_Hxl4{!1H-o(XuSoaD)rzt+STDIHh*Gz9^ z$>s~j|76McVadj0sa?;{H9pn&>NI$ZTFqOQtPL8fBjhMd*$;}{QUIp{l`CP$7NOhP{xXTjQ~76zUzQY zt@XY8{uckM`1_r{@$>F@@pFc3ez|}gKX;Jh>uj!8Z6!WARrhYp)X`@gw95;gdMPhDrr17<@P1JxTZQA}@k=OS96PL5 z>L^*b%Dp|8uh+KevUs7-NnCfDRjtuJM_yn(LmL)&uU;meo>o~R zK0Ukg37>oBWCQisAuvs36ZhERGRee;Wy~ zGp*%Ck@1$vxY(b$jCbwY*w$oENV^k(=Oyr4Zq+;GB{hDTN63IrKcYY+@1)Z z*W%tp=)9z7AG%t_P?nEWE<+q=#bNI@y%)=e_~_hV8|^f{(z;K7eTDpz{@rW53$$hN z>hAI--NhTaTMq>;seOL3(!D)Ae~pRCX3SH*y!wD!S07+BJm3VY#AZ3sEUj7I{Iv7I zfqsJKG`rvNS`CN!{f+VRlUt--x)a^qFTeRT*qryv54za9XGah7(bbgM8vY`;a)J^+ z{Qceg3D)>wnQ)QgyJ|Y-gkF}-CNX~8Y}GrxU=>(~{d21N;qQu!{xl&a3Y@pVYXlf3wi=EkdKq z;x;wGTWSJFHGwBw@!zXxod0_BQ~!l4`wX?DTk&&BOrsI!4 z`cHh##g*??9|G*b>8FiOGg`VEST3r+?A9FYc?_7i-hXY3Z(^)0K1p>}`xA%l^p&%L z!!qOW;;!S@OvuQ^;p=bG_HBlDFrHUR;u#pfBu@(Vfy=v%Xvd z8&-$iv_xbsq;5`}+48;r>2iQc%WcUntaq~MQ(My&T^VK9US3tU&zhs-EpL_B|MD08 zCfj-6di(kFtpdDns|=s$+urQE5y5P28P`<#vl8Ua-0kcke;n+gtCmMUU08qA^9*w- zH#nI{xM3pQY{9Pgr%Om@3sx>H*!kA9wm4@tD%`U9TyU|oB+oE!F+aEXe50+2-_h2* zVr0yw_dTuA+YF1ju}P=t0foufIh{X%rhXip`}}OW)VYF*6&V^>)mb?LW%xG3WgTLND}xz^(od{0I0y)~Dfx z6ik-y>>ZD_WWd&WhsG_3PU{x~Myx2oL(}oILqew7QWkf5uiJ~*^Nu$T?Ow|&|U>zUOhj# zJln)*aTEQFFix}69)qQSQ`?zlTB2jW;RH5G_bmt5odtg*WWNH=xI$sN%0F#dDjbW# z9qj34e@N~(pN6F^TyRnNda)4BD{`)r{iwzK{q_u>K9FKCh&La=>C{snLFg^3t-2lC z#^1he^&e{=+!!(@4=s$A7eX7oGGEb&Pk!=%^7Q=KsMO3^shNGHrl}XPl+T(G_mKOf zf3RPa+(U}qwc0*EWnSMUqxPwG8^v8l+7PMilOZp1(^fB`Z5<}#{6V)ZzraH0(e%9C z^t#>j;9{S(`{7G`|Nig)&*zV0_SBa7I3`@_8$|aXo<81pDR5J=)n*KBq0YmYjupmq ztZ-Ny|CWcrz0b|hecroG?q;c}T^jPMe^-5u)4Xs=rfYN7gtY(s=Z}w1|M$ng4RhW) zH4Q)1pgh^LaX$WiH#7PlrnJG0$N3f^i3O5dajcP-bcy5^PoB;%3N2gP(T{3Jzt2!& zE}M>deSC#93naIW4U0J1@MAjDcA=s(=y&f-|EAzX#1XmfNx^~8SMc3}e;VI|f9hB1 zdbml`+l!iBHE+BTb+Q?DQJnY;CGVNI)Yl)IGVal}JU(jRE0tx?ProCnG{0~B9k23x{PIVjh zd~fB2CvAIYh1s^Wv#;`w+K0K?f8VoIXw*`6)KYd(`;!{8qZ+fL8ne?D>@L-!jN6Ee z+lY+$-Rrh~V`u2FUOzkw;|UVR6Xd9wWvQ8Au9+9n&qdPR$|ZMd~5j%#9L8BI4A=ivhng@ymz7SFZPNh88^h-wtV}@4kF^eE9F(-Njk+lRP|}y$OqEoeF*( z^T!WQ@!`YppmiTJTejnMe>)!9bq_q2hsS^a_|QMXd$QwYtJhKAX0E?2u6a@BUK%{y08Qe*%11f$pM(b3gfPLcMqMeB532 z)ayPE>tXeNDDXDG`0?q_^|MxYFyG9kGBRguLjCEj_uVY03Dmdgf9if-&$I8=HMk(` zm9{6a+cUA(XJXF`fBcdj>(f|uM*q+Sa5g#JkHM?L9(11~znIMc=I4hY;5b|`oS$}w z-+hnSva;h3>6Voqr{>je{NcN5x7r=e?v1MT!De9tTt*+COTE30aVLXgL@9px@E@P! zr*09r9_uOmbhorFfBY|#ej9%rdN=M&*1Md#KQ0m{dUp?w!ul|#L_928Eu!!7{l|}g z`SNMDO!|vs^O*xImsyvO-3!RzP&l6?7m0p{cHdP0&b?Xj~_W0@P^PtkEgn-V`yx;5`Ao+QE5%_ZdnwW)S zWY~0<0yn*f7i2V7$jBoZd54UP#IA8$-Y4Uw+r(O^FG)S+;C!5^QMX z2QbHQ^hbA;qdoGGj(CKlIdE+j97>{Gtt96yV07LkfAZwG2JHv1(GiP8^4v&(B`3&K zb3})UGFCFC>&Qo-BjBoQ3Z^)5PB6Pb6mp{CeF_5E)eO*ewVPdycc%IrFiML;zJU!G zD=?dCq`0oD)2{9a%dXYhoGk%zFpWHwR;{Us&9;zg@?BTI*)>FpXn@g2$V{1R%()O{ zOFo*KIkhXAzN;J|%(}XSLahN|%}yvpjvUdrnvqkqwd)F-U2{zq7$89rjwX9bMZi+j zF9}qex~@2Oo#T^aC@KPuNRyB#ECJ1vy(kv}Nt4wmEq}TNgJG+u)J#o`NVDRSzxxe*430vQZ)fCa49LcPAw1~ytoEZ z*q9co7=Ig>jU?-;VIr!X3LrW#`{Y~8+#DBU*jHbX0%t?kipK$(B%RQIbn&WAX``n37dpnbxz8_&}zbXc~cQv3Q8pdn3dN4HTqa9?2fK zC_@Xz>@p(}_~4T%CK@L`lOLdoYoSETlJT1GTni2`NJjm2dfN*;Nd zYXx+fkdu>Csc#+{dR4OTe37}hN#LUqmL}-PqrG5h=doa#owk{Y?4l86S zA!QZ;6vHueGqrrQbhLQ1aJ1&g;mH2T?tjQ~WP4;jG94L@3`aIc3P*?i2{M%$E4E~E3kgcAjQxxb#(xrn zSnx)glSF~4_u_o^0z$n?BR-^L$)p^DFPNxigDFvE$}zQKd>e4n%?_ikAB)zIF%|@D ztWq6Yj-zb5oU^!$8Em!A0fdOfdkQgHtbUy7x79FEz0^c4m<*{Du$8&^LJp;1ZFI%N z@}4{yN-a{fvH9ZI+Z7SNEVSmJ1aEWYT(V0odE0GMR@BCjjO3#Y z5d*~1z@*6HjWb|#r(&!-kg+WS>O9q2WT`#{lf{SX2~!!MC1tP_t|H=dX>7z52FY3H z-^u_jWrsCeo0><+p+yJ;mAQIdQL!J?ABtcg*Ak{|!3V4oT?I;oswC61!GDHBC{)O2 zjH+^_CCI>@L$i$~5rqL7I|=$&`&D zkFL}KS|!V1#G950o8g$$j*Xd9EXH{rpfM+*7F6I`3r1C!cP(0|o*@Q1K=UmWMl}wq zGXc?*;Ic=bZX}_WQrJg!HW*H!A~A))Y9`w}&a|YW(i>9L&8He~J^NsS=MtK<0h)d_4ufxv z*?J2#mEyc`3&c_YN8DO10wJ=mHkD)}1S>XEZ8_G!)sA#a#J;Ic4S%l22#JD&8o1Tu z9C0U>LPx=)z_yYVv#VsS^_8HOoOS;zlCsOeKyXwoB#grv{W{>T+NKs(YPNV2z^HKx zkt%t?V#+{=$ofnjRSz|{VoOxpN&-;JPC!OFN0WQjPBxCB8<7%rUhS_*qqzb#noP}a7tbfLGl`F^9BsN;#Vk=b* zge0L<5anrdiF$Kb?15MkG}3dWp@=Cd>l$`r>srhZ1W?UvUR6t=5oR z$dS;Zbr=w$D}U62Mbqyt;t$0-Te5hn1+r6P2u!jZN{cmzN&_?qSbb~ADXG681?S0T zS1WSzso#XeA25aF1A3&KLbWb~_tuaq)k+xC0L``*W2WR(9)eH6A^23GsLaRSG8KP- zAXP%q15}DNP%7C=@u?M$-hdmRMUrH^WhveQd4|xUX@4a^mgd;Xh?`fNvpH8dSB7lW zhHMS8m|SxlXIc=F1IvICg($axl~Oj&$$w5xF$YD^duqU0L{c?B!_~gITwqw z9778gs()Ae-uVF<<$x}F+c=S=q@QBJ$hF3l3RmvL(sfGK@zK%I;f9iRaCGJ<;lfN7 zvB1_wVh4z%{v^wsO!U%PuNJ|7C2&A&$qN+%u(<>@LDf>SrG#XX8R+1!C7XT26o^eO zBu-CG>`koV`jfQM!9yyxwGs@FRB2=o)fR~^*MA@#kDMHs$dRZWQG;VwYzQhu$zgCw zT(7YFA&97UVdh3$eD*0f>#*c#L(XAhl-61AY{(ElTtJ> zP=BguokM%Y^_P?PDOK>+InN@^I7;f#3Z_Eybj|hGJcn9bND?X;cBX_t#&Wf4Tld^@ zhgt%0;$my7xw0XO7Ok*&H7`>)g7b&$DJRQb$XgS$(><=a09ISKI zro`4nNv1@vj!$u|KuI|oH$bb|B=D4dlaQq$|Hn{h!~4+R!YmH&Z_Jv zS8w!`+WHf^H-{VwH;~X0frC;d7=K~R$ep`|d4QH%HHKm#WD?88MMuzVw9UH0W}K;b zFs^Wm>L%vY)Td02LWq>vg-#E89F(kuqlaxJ%ebLr^@sosY~qBWcpp45hny`s=45$T zqhALcS}j!7U8*c5^&d#~)v=^d&r}6WG1^%4MCA}9FbA@fLe5glFhO&moPP|EGt3!5 z&q}V_`iN?4tzvfo@^sMC4_PjeO)brq;<@T+)WoE2t6pKjp*8QRlDgef$e0Kz1}0Zy z_L%J`KY^_E6kE$EraF%%gqm7t!K&pk%8y~2y@{T4tGdYpQwFTnCUMdCQ&8E4R-y^u zQB*LE0d9@dSs!a8PUB3!segtky7ZeTH4PX|!JKWi-HDsjSo&c%jDp2hlQ@K0QGFIk zN(si~V2UN5`>@Yu7)2s+wFWV9t1+t$Q&Y@I^$ibEAFp1?l(}JMQLEmHK=m#+VeZbC zeQ<~l2-(`!OcfN37XZdmFq5eNzoa%mvnKkgCR|8JIkSVB7)fjv%zq({(9{j)6G&~b z2t{BMot|$hp%Qz9meo@hA+#VaaEQsEVQ7Yp4b=r4pfya^q+BZpV?2oqHC0S5*=)&L z9H2Qwssyn{L~m*f!A5bJCDl}tgaMk>Nj1*C*x*vraY}Nb#blK3c7T?uvn?g-^Z=c5 z^y&yNqD*zvhR7HlvVRp}QP*vYxz%K(rPvZ6K~`Vmh+A~V+N=>i#{r~>O0McQ%g&pD z%?DSonNpB)$>?$dX>6^tNhQA#kI-5+Arvwu#gc*~a0yJPNkfGN!grw?#ww9o^d;xy zLa~(swuF{*#N4}DJRc}zG*S0`mn@VJgj_=w#A-~XHb4UkB!5sDJVdSrVyq0t1g;*W zi65Xz)Z?Qq)+WrpB*z&Hv{;+9DfW(hq=TxgfCx!lVKuN#41fa3h*0SjQs85tW58p8 zV=zY_j@}==J9;_#&6uHvd1`f>ViO-51>b<6+7eqr0Unm-%Yd?r-jD{o(3%L88u^xk zRsBpH-MBJXHzxR|-et0_I&Uj^C)kXLV>_-44pD%7AroRL04ZS9z@%48*Tj*-la4hx z80oSdd7>wvqG0S&S&ljOr)#ta48^rlJUQPA_)x1+i^^lNO-k>S4fX({o2D_j zk1!z`C%sD(oY&fJns%`s-1qIicy$*A`k z+XyXXQ)}_9S*E5|JVFT+sRY7k>VGJGEoUQ5N-NkHsV0-y6jPC#k-@#7@}dDn3eG2C zuUVL$rF7uV&OJrU?>je9%e-A5E^cs0~Wq zix1yLqfo)*8cTo@a{`T7QH`2y6>1wZoHo;UVhHLUGI~@{nglG>I`4eQIe%w+C4DEd zdY`?i>U&}*C8!=xa5*O~n7Z>L*8v)#gMb+g7NenflVb~&8z-ODv>2eN zTRAuJ24dE2fUS$@v%*a=_kRHzbO&$&SOv)zLP(lQWfB&SzG|eV4A2@>3k5-H^j-*4 z$|Yt`u?pl-!@2`jClRa*EEd#$5{R6lsZ4sBlK~n-i%B%$O{&S#0tHWytu9-aB9AjI zA&N_cEqE-ZnNY2@EWQ)0-Z%~Fq0EjvQgzu{>k5dZmVl&`3~8{4-G4!SZz&iQQeR=N zoz;}dTW7M#7Dk>@jR0V+CQ^yG+-kJqtwiS|%J-pLLCwPxL!o(ZG{Bl%Qtb~_Q?o{S zQ=+o^J~W-CG-1)GdriKWR47j~)lg0^`VUI^5N5=^Te69?nS)?~S|7tnlA#F4`&;EGKRLJSb9uHaykdPoWe+s1iU-3y!Z zUN||!$e2Ay;))p5#Wp}Qv6Lve8cQBR=RMKrh-M8Y@skcL0?umA zWX(LTld3wB0nw8^J3_NR1;aIV4}8k7Ivxx={_Ws$78XY&KX7HX3!0mlTKObd{4-JSi2rxm>$MuL8~# zQ`9HJ1`0XH)ioIDlaf3`f8#=9${E=d0F%79oF!P!oQ%d*nDa!&D5T*PavEclR84Ul z9hXc6njfHHY>o90*f?fz5=A0%ZW)sE((kpZ1Q;=v=8Q?DTHso#k#j`~Iv4tYcnF6m zSgf>IG*D=wAt6n%sY>lI$dw9A&@@_0KE-6cW$z(-&9ybv1nWi?e*;ixnyL&MxUp6P zh|V<#TvOsA-$kY5;);fftTh~@)R1$FQK}l9Bz?NoPTqLZ5O+-AOiCtqJ7KFX5){DL z(`Y+y+y`)a>dBH-<(TXWvF7dimQ#wQ7g9Kcf*hGS#2SpQ-JH;dR*c4EtLt%tL#yiT zVc!Iz58im20=Y`5f7nuo3}OYxS-tg5vJ}(|UF$J;j3sMOyGk0s=^?1|%|xu$3%Sge zA_fgQ(GZkXa0$tEiHFJpE+n}|%_RjrddGf8BskbaF|lTziAo|0F@{uIX_kWT$<$$I zZO9m-SKCvv#Kuv)7mLOi*Dr8_L-Y=cN5tU4LaN3Bw}N1>f0SbSJO>3ws6hhVnL!st zMHdVkrchk;5QnV(LpI)tiIluBp(cQs6heU{38Nh@+88)s!G>aE5%qj@R-u$!vT-dW zF5_gSs>eh;agY!lr5F0!|6G$UneAahX%Gm~&C6L#O2cDhWsgxE}U zkc~;s6lRwUe*l(LChYW-p}r22Y$%kycP^rJK{La_=Qe;df`pQdQ;Uxr8oegvv5_tV z8z$Q2U~I58h(}c8#CvW{O{eHqY_tq~Tarq&S$%R!n?f9gB{6Z$=?lN#fltu1HWFtUMa zt=GL-B`%gBl^qTRqX9xLTw8OgY8s8+5VJ0Ojyw@kq=6;_MccG-irfOGY`g~LMMgFQ zu_l&yb&EukTg}87GH41o=iX!0388mI?VW%m!BEziW)b3Su&CWVN=-=|7}=LIG7O?kY`99K0stuAh9l^*Uh|#c1(TuJHP&yxs_>`;! zbUa99nA)SM$=IBlan>-DnzKZ`fy6ap$aUR5f3rA^UD^{vN%;;%$gS8F6fgq+7naM6&N&Yx$0IAfdMl6 ze|*v22MRext64KFsxpI(&RQ@~T<>U})5m1*P11xMi!PLud}vf5Yh)agqxF1^4NyzU znk`O{J?iDd)LM?#3J!bmti6o^Tmj9GD3T+1SDR%$;>8p=4p%z)2%7y5*vTA5RgXSp zs~Wx}lSEu_nzWiT#o;!IKZ0hff*b+tf5DOldmIF2hGtuhYIt#0=XdbgPIQ|0@oI1z zmwXdF*B4hvQb>BI!44Tq>pmH37@LOd zl_bF>5^?5C<5?f}nt+WY5D9C_Nlf7gf@1Z8OHTtm8EXtlBT%!xddvt-qsCx;UX_;7 zMqO3WqdIr`@zj^O(O0KpY&F3|3L%(eYA!jr=!>c2y_b1k%{kDFh3@tS90ARtRvT(& zP4g)vRaZ4MAA+agYM=pkxe9}V(`$$}hs4%#u|+h&Pp{}$=doXtC_+4c*Vw9`Nv=2y z#cafuiiLhL;RK>ng1cq}pc;=EoouBJ7kL4xi|V)gymqmzeKzZcVlzLF+v zzK$krzK$krzK$lWSDKxb?p`T)lS-mm9TrZ_AtDXiBf}vYuzIthv2(@>>wRL4UwA6f zVH@|EL&?~st<(l3r_zieZ=Ogm|B;c@AA^ALU@!qXw8m+cst`D-R#V%8rm|5U@RI~X zF9DsCG($E4x07o_Eq_Zq_2#!GajWWadYn!L9ie6(i@;zu3LZh=2%=*v&i)A29l^>G ztUZF|BUn0!4aBYKjqv7LGM-B@*3_UGJ9E3_9}EkkZKXmj7Sx{1A?xu+1Ad$`_IbJB z{7tZ8LKDGjqMoK)s5e3)u#lmehio5kas+1q@)iy0kKp(Sj*j5)2o8Ua;FOk%vyP>= zIOGUok05*mp+gWhB|@r@)GyFPQ?M}sR8b?dU!Tr>6>MMF_-xq)4JT*{Le^U!wJ;ke zZovCCdTNvd8KR927!zV@A!=@_=3}_wIR}-sTj-fJD?d;)j!clK{)I#qLoDDU_iilR z$8LaC*q0De^EHA|A4`7-x#b4lS8%Nl0fC;LJRiZ+5j-Bj!x6l>3BIOABB;yV6cMHt zZH&NV^d3_z1Fl~WKkHi;5`{~JfEHL%tLnjOssxMq0lYtgcf$ZO3~(E8;i{pv$dJK# z0d}Tp9)fj-4f-J~k~`Rl1M)%t!4ZNIF5Enp#XaSTPD_^@ipf{0$sHYmAd&H3mjh5a}|bMEaCg8u$(6O4NELQt5|Wv>Ad4JT?c ziQdZaePmdztZzJS0h?>KffF}Z^m2f1Cz4_UYBmq^HQ#((y)VbMs%uMKf1=UBB8FlJ z*ox~INqI70B>9*0sAfKzjV9f3)b zV<;RvxJE;&B^vy$I26OFgzRnd!Q>Vt)>3`dKpZ4L#J~-GSCivKH-Do88h1n^-vt*E z(?H$h`rd`r4C7jB3B^10^@QOT0Sx$j9~{`JQz?KqUMg5B&W0SSDa5rIAAdl=9*K!C z-v^PZr`7}kT+3qB)hm*m?G7nMV*LR@21MxlBH|>8vBf9bT?yAfYOP4QW(t}D(j#Jz z2=4nMQ#zk^5^f?!Uw^sD#2R?STyk!6Wca%yL&oaODAF6E9>Msc+05L8s@0sy9}vP3 z!T&=jV`3%n43r%-jTbh}oN$^?N6~Pf0<`m z^bHPu^Td=w5<8Q!kNK$++Uwz6?@nq~xCc@Xco9=fGN}xCaQgI-K9=CYu|d5cm`hHn z##l8IPl9ukOM&@_>hkafD;B7lz$%lQlC-@$=(P|V z`|GyNQuC=f6LN{3^*NL?zUn%U;8SQq)J&HxX}stSntx^oV~p{L3`b<`6OKr}8>356 zO~BAf!T+zfGs&_WN0#XPtp@PkcYtl6-TxB)F_JH&uM8CLl{pf6ak2ZKj<|6^xWb$y^L}kL4V$mVD>p| zr0Y3M?|&`SXXj?&)x)OF@Cp=JaTVct=AgHz9h6sA z9dr%~V;5JW3Bur*$>kBV;XCpV+U#BiAUIBr7k^%4nV}#LP`&fitP{RZ|Desa&+>^B z(OM&%d1UqU0?682Z{>mgqc)8PS*CTwwz%429x_qGN=)^UCK}q!MjD^q6Pj`9D~1BD zCip-h>%O~|)%lTx8U3{ls~>Hk7*A@LP(^xqaMv*^4?`ixx!->>ZG_Om6DlL)R}a+Q zbAM5E0F)q&ZpQ#>tUB&8zQ2T$ehO8PMI-Y@X0H+?x^tt5!1ke2CA}ZAUMh<9KMnu< zrY)o%Op$RnS;!KE>C$7!ij}j^r=gGEv_)sE3Q*KsHUv7mrTv^f$)T>4PeUKSX$#XY zWI(!Wonu8GIv4i;TTvr=&x2wAS-;A*GJgm$=qut^i$Wa-8QpX%=NKuKUWLbxlr zk$WSzMy`!q8ae)tuKAq2HgeqS|7>i45YYk!gYg!zEV^}ZMMe{)HuvxO-aZt~9#AX~ zL&@hVtWeRdGSipeA#Os1;~V?1QF4qN=R%2lo*uQ%ZhNhavY$wMkU+)Oq&mP_ZpbQj24|^ar^~-`WRV(432oO~IE=Q3&;= z)y=6tYs2u5@AF?m#}kT8@l|qSXH(8Opu6T-9dy=@^}%n>UyCE8bT;f4EAIkj=hB3( zSEv8&`Gf(R>6?Pa*m}~Dg)!UVK7Z~?yNKVOKL}alN0etW*tfttVMKw7Iqpd!7`fpz_SMHISyBa^Byf@47xCCAwIuXA-K^ zKub&;Q3}A(PsL1r+x6!>BeEw=lQY2dT(g=k@H2LOFpf38?fR>v8BLm9rl6#1jGn4{ z#Y!)$e)sj$DGIB{NvQxaF@J)1pn6z8ezS47(6?QGKre5V*efLvG}ydD3rrO(vgi8z zeeWM)3*%nr<9kmFgof3{u;04ZMO@_j?!O6F)jeFvOGR8P+;t#zT>WN{bMeN-8W;Vx zet1-VK}$C?hB-Ij7Iak$_;{Jv*#Ow=~mDvQC12B>Q@w12o~*}LSLYi(S= z?|bM@bDwmdRDpXTpzcngV}cy>^F5$%?Zen>T1g!{tRrxvxv&o@V#DoW4qq|2JCOc; z??&l{dNL%1g%Ri40^x+Q)b)_N5v2U)eiWJP;LaPT8~_-_4{(cSRI1H)KNx}1Z|=+V z7~$4O&XuOnL?ecKcz>d1I>wK_=>McY1&hrN{M*Sof$7-LA%?oj%!gKtnC*9uOZABf z!w#KMQLmE`S|>L9k!tUL{4d5N2=J?&o#X)gnge2;4hVP_t@}q`{x|n1hYVl~ut*o0 z)+>X9UZe6ALVlMOF-c=kY5;jRfu#lF8K_y*F&Tl|QmoH+Tz@kltl)7ni)a{7t=LBG z-cwI~WFTyfSsSx7W^T;Xm}_Ikx-uJ6G$wCMxW0ar{X`^$_;d=VmMqHq6!N(O0$IAt zwpAOeG*)h`)L3g{1O1>P2=5O|0Z<6)l6#y&zTCb?%+ci%P8YohB!4K)fXq)1-GCRiulFA$B+#8n zb~(1^@;oM#z{s8VeGdL|`w*?J9=nJ!JAt)h0q%8;nCtO52>NpSpx4xXL2;$-N;+ox zT+&Z=sn2@R?91(sUZ`8Oq1AS*9qWiiLR=ei?zjwNKla7;k&=qFX{9hj36^uhFr`F< z=uKwjD1TqSzu~g$j8Np7GWm>Aw%S6~%er$@Z2tBBv%vvF#YFd4G2^=o#_*RW5eeGLCd@S`1<>0y^qClU>KAjMghhFavz?f$Hc;Mjl9?U zU%XC@BgMy>1=W$k7j{)gRVWx9Nd!AJ_OFlC%6}e9EdfZL(Tz)i1Z!d1ADy0SNMrx{ z`&<)1wEJ#zi8t`SldpgrP*rU`g`4{XZ`Ao9lw#J#cK`R*@| zSLft@7Dd_`*&TSJ)Zuf2#P$4^_^+>XhLBTs5L$~W@ z5@8cE{n~XRt-h$F%qL%iviXCX0C1>I%vCESNgV*(Sg1(*CExr4DtYVL$Ks5lb#dk? zQs=oWjP5xObtBL5WK;^7K#k4WrxgWgE3)8QTA%xpKiYTQHiiI)c??3z!o<~!Ab-kq z1H3qX>JOZzGM#*!Lb2un@jL>kgfVZl38RMPIlid*Q7HQtyt*oiPZ)yugH!s4+ySzI zB8a4^lh(DmFpcgA@*dK+%|^J50!X%3+uY3}A?Iz3;~?5@nBF^ zD9x=hJ|s*pc3zk5-*F#aJZP;tsDI3{O0{Q>Np76c<0!q&!=o%>VNCd#x`ti z9Ywk=*M4cE5al+@AJUULs=`eSj#^v29C1hlt3g|G7w+L+C`6rGIS>ySV@$)aEHRe! zNB56=u}#1hSp-(pz#`7e@LKlff}i%@`@Qqz4BSoMURQ+zHTw!F6A53}IcKiC=R7Ig zq)?LrqYsQB#ynmd-2OuaPk-?$s|I)9j5l0Pt@}ex_u08|Rd2G?x@W@14s%F2L1`-e z=AB8A&#$Y~!h9vDB=snx^n)(Zt!_CV^(vp8JHZiMw5DI)Rp%V?x{*=aq|?Wr&i$w3 zD@9*B;)q@w5#|LeLqh(l!%FTv@uXkJR}g>27=hM~_tdD%ID=7vgnunKQ_l$cY<%D6 zDi5eUnY_%tr-am<00YEn5fWGi{Y|~ul@ywGdO)593@Q$fXuD;-RM3dsLIoCYhT@FR>7Tq~E*j!6zmd6zo z$N!;?shahrzk9bk@;VB>)EDPE_u?JbxkoSFYs(7{K6-Ql-8q zMmk?~W$>}2-q*5!ZbpSS!Gipwd#o zazr}_D16Jvg{=u|6NZ-^zp{4DqUCZ(<@7FR*bbWKY&+vV2WClvbF&FY6V&d3;4r53 ziG|IC0xJ8&w13DPbLD-WG=bfc&`Z|9hGg~wwCOc(W8RO92>?aEkB=t6#Dfzr`m$Ux z$La*u&s?P|6PCEs&B*R|TC_HS&l4c?3@0Cx9HZo!-5@V9*Yqef4@bY(9-@5z9;K^q zio&B6ro{$eE6aN(t5u-h$DPv<^(G2_y*5#~#-IbXJAclasu7S+1N4jH43{lE?%xE* zDa|IZj!F_nG+K-e_NzK7Ml#H5LF6Qd?pU&==cyst<=zOJ2MaVFfO z4v2WJbAi?Oa`zK(eTycrxG5EY{xfr_VC_J)?4y|Pvd1Imm-?Dq21F@FusGTd6zZ(t z&KT@<;(xsc*yDmxCHD{e9a%z$Qzh{-s#2;!wOZ``O@2wK zLr&P=uuR(SdJ&0|>O9hp#lRws2K-2P223!jZ z-D2Kl9WAVukEaaAcL2$~x%XjfL%IpyV77tz0fxZ8j&IS`830?WM^dX&CzL|f?A{-I z#edJ^%L^~DD9sw^CxSu%->Plu{M2atG`@q&Ny5UnZzm1$u^?j{M`In;U&nV1cwUym zM=>29njryOo2(2wuJ`yBmAVCG&bT;Gf)h$M7u2Hn`mvvwe0qt3Z>!7#UyvT*gWRgp zIOSsv8y!yo(wo5l0Vjdf+9*n-`mxr2)ql+g1TN697ZL)Jb-?>kv{s>CF$k{$AW(uO zoXFfwJTVHaH#V8R#;@ZGkr;JE@B5fr=Q%YD5J=v{^yD#q8eiZM3vI5|v5BlPyaR30 zU03RjW%zk~C$`T@r`zEz175JAlZETU>M( z1s)}VYh@FU*8+}Zk@qW~>?hRo$JuGdw~^t1+eITjwI*>B7Ylx8MdtC-s>oHI!b;HD1hUAT)_gpY%hyQ2y^1e zT54sn9C7CR`8`<1@_;`wC@Ew1UBbBbOc=!Mk3E>k1cYP5nOhy$0iejdaL)61HeTQ9 z6T?R3onFDG&A3nq3`*73yEaFpqnw;J8CW0iP*dw<^dE}}_z zldxBXLpiXFGUiq5Ru<>Q8P2mGSe+!?!RmdzELWcF0=!jS8=hwCB;2uv7C~UN^kyoF+gu&={ycn{RT7M%PG9gOz1Pi>@|W}C^pfcU(F9x&O_u?tzz3n4DEE2MB)v&m zlhkWY_OR6wrd zmH=YXAU^nd-4>45{gi9XvK_cgz};h>1ooL=$~ub-OfI)^YlYWxy?>6Mk#Hwlh8(R@ zz?+~P(CvcjxbL0TXj;7~92~1Qt#BEFbgdgzhL(9&Fc4SpE_p`nbDtYQq&2T&9eR;C z$RdkDuj1n@SO_dCBj|SeBx_3Al%y%a5}KM)ZA#?@M$H(bpcH=1Q)VCR*>mtHZ+wwb zGzC?8gP{SVa5?o%9e*Hq>82$NlgE3^8J5=El&LAhfg0!MH70)9Rqa_28r$%t!fLL@ z7N4^|*Wzr-(UiUEr75ze@C`R60i?YX7daqm0Z8Z|!_t1PEw!nX3u%O;aF2bELeiZ+ zC{|D2%hz_kVP8KVADHbmt(Q3<7L+k$%n53EwQ=v8Rc>68tbg6>rkoy!Cp=B6=IV3; zV1+wwq{4T*4CA2~euZ;j?a*Nf5+ex8{@Z(3IMqG{tsh?IgKA`0RRYUXm|hs diff --git a/creusot/tests/should_fail/bug/878.coma b/creusot/tests/should_fail/bug/878.coma index c1fae20a9..eba933955 100644 --- a/creusot/tests/should_fail/bug/878.coma +++ b/creusot/tests/should_fail/bug/878.coma @@ -112,7 +112,7 @@ module M_878__test2 [#"878.rs" 19 0 19 14] let%span sboxed7 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 let%span svec8 = "../../../../creusot-contracts/src/std/vec.rs" 65 20 65 41 let%span sslice9 = "../../../../creusot-contracts/src/std/slice.rs" 18 20 18 30 - let%span sseq10 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq10 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95 let%span s87811 = "878.rs" 15 8 15 22 use prelude.prelude.UInt32 @@ -254,7 +254,7 @@ module M_878__test3 [#"878.rs" 25 0 25 14] let%span sboxed7 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 let%span svec8 = "../../../../creusot-contracts/src/std/vec.rs" 65 20 65 41 let%span sslice9 = "../../../../creusot-contracts/src/std/slice.rs" 18 20 18 30 - let%span sseq10 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq10 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95 let%span s87811 = "878.rs" 15 8 15 22 use prelude.prelude.UInt32 diff --git a/creusot/tests/should_fail/bug/specialize.coma b/creusot/tests/should_fail/bug/specialize.coma index ab52d8f60..d6c798deb 100644 --- a/creusot/tests/should_fail/bug/specialize.coma +++ b/creusot/tests/should_fail/bug/specialize.coma @@ -43,7 +43,7 @@ module M_specialize__g [#"specialize.rs" 27 0 27 18] let%span sspecialize2 = "specialize.rs" 6 9 6 13 let%span svec3 = "../../../../creusot-contracts/src/std/vec.rs" 65 20 65 41 let%span svec4 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span sseq5 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq5 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95 let%span sboxed6 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 use prelude.prelude.Opaque @@ -169,7 +169,7 @@ module M_specialize__qyi2463200954251793265__x__refines [#"specialize.rs" 12 4 1 let%span sspecialize0 = "specialize.rs" 12 4 12 22 let%span svec1 = "../../../../creusot-contracts/src/std/vec.rs" 65 20 65 41 let%span svec2 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span sseq3 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq3 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95 let%span sboxed4 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 use prelude.prelude.Opaque diff --git a/creusot/tests/should_succeed/bug/final_borrows.coma b/creusot/tests/should_succeed/bug/final_borrows.coma index 4073975ab..b58b79456 100644 --- a/creusot/tests/should_succeed/bug/final_borrows.coma +++ b/creusot/tests/should_succeed/bug/final_borrows.coma @@ -1943,7 +1943,7 @@ module M_final_borrows__index_mut_slice [#"final_borrows.rs" 208 0 208 48] let%span sslice10 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 let%span sinvariant11 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sslice12 = "../../../../creusot-contracts/src/std/slice.rs" 18 20 18 30 - let%span sseq13 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq13 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95 let%span sboxed14 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 use prelude.prelude.UIntSize @@ -2104,7 +2104,7 @@ module M_final_borrows__index_mut_array [#"final_borrows.rs" 214 0 214 52] let%span sresolve8 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span sinvariant9 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sarray10 = "../../../../creusot-contracts/src/std/array.rs" 9 20 9 30 - let%span sseq11 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq11 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95 let%span sboxed12 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 use prelude.prelude.UIntSize diff --git a/creusot/tests/should_succeed/ghost/ghost_map.coma b/creusot/tests/should_succeed/ghost/ghost_map.coma index ec4d8ae07..2570c6600 100644 --- a/creusot/tests/should_succeed/ghost/ghost_map.coma +++ b/creusot/tests/should_succeed/ghost/ghost_map.coma @@ -1,101 +1,112 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18] let%span sghost_map0 = "ghost_map.rs" 5 18 5 41 - let%span sfmap1 = "../../../../creusot-contracts/src/logic/fmap.rs" 237 14 237 31 - let%span sghost_map2 = "ghost_map.rs" 7 22 7 53 - let%span sghost_map3 = "ghost_map.rs" 8 25 8 26 - let%span sghost_map4 = "ghost_map.rs" 8 28 8 30 - let%span sghost_map5 = "ghost_map.rs" 10 22 10 47 - let%span sghost_map6 = "ghost_map.rs" 11 22 11 34 - let%span sghost_map7 = "ghost_map.rs" 12 28 12 29 - let%span sghost_map8 = "ghost_map.rs" 12 31 12 32 - let%span sghost_map9 = "ghost_map.rs" 12 34 12 35 - let%span sghost_map10 = "ghost_map.rs" 14 17 14 19 - let%span sghost_map11 = "ghost_map.rs" 16 22 16 47 - let%span sghost_map12 = "ghost_map.rs" 18 45 18 46 - let%span sghost_map13 = "ghost_map.rs" 18 48 18 50 - let%span sghost_map14 = "ghost_map.rs" 19 45 19 46 - let%span sghost_map15 = "ghost_map.rs" 19 48 19 51 - let%span sghost_map16 = "ghost_map.rs" 21 22 21 43 - let%span sghost_map17 = "ghost_map.rs" 22 22 22 50 - let%span sghost_map18 = "ghost_map.rs" 23 22 23 34 - let%span sghost_map19 = "ghost_map.rs" 24 22 24 48 - let%span sghost_map20 = "ghost_map.rs" 25 22 25 47 - let%span sghost_map21 = "ghost_map.rs" 30 22 30 42 - let%span sghost_map22 = "ghost_map.rs" 31 22 31 49 - let%span sghost_map23 = "ghost_map.rs" 32 22 32 42 - let%span sghost_map24 = "ghost_map.rs" 33 22 33 43 - let%span sghost_map25 = "ghost_map.rs" 38 22 38 31 - let%span sghost_map26 = "ghost_map.rs" 39 22 39 32 - let%span sghost_map27 = "ghost_map.rs" 40 22 40 32 - let%span sghost_map28 = "ghost_map.rs" 45 22 45 42 - let%span sghost_map29 = "ghost_map.rs" 46 22 46 34 - let%span sghost_map30 = "ghost_map.rs" 47 22 47 34 - let%span sghost31 = "../../../../creusot-contracts/src/ghost.rs" 217 9 217 15 - let%span sfmap32 = "../../../../creusot-contracts/src/logic/fmap.rs" 139 8 139 34 - let%span sfmap33 = "../../../../creusot-contracts/src/logic/fmap.rs" 132 8 132 35 - let%span sghost34 = "../../../../creusot-contracts/src/ghost.rs" 85 22 85 26 - let%span sghost35 = "../../../../creusot-contracts/src/ghost.rs" 85 4 85 48 - let%span sghost36 = "../../../../creusot-contracts/src/ghost.rs" 84 14 84 36 - let%span sfmap37 = "../../../../creusot-contracts/src/logic/fmap.rs" 376 35 376 38 - let%span sfmap38 = "../../../../creusot-contracts/src/logic/fmap.rs" 376 43 376 48 - let%span sfmap39 = "../../../../creusot-contracts/src/logic/fmap.rs" 376 4 378 17 - let%span sfmap40 = "../../../../creusot-contracts/src/logic/fmap.rs" 374 14 374 49 - let%span sfmap41 = "../../../../creusot-contracts/src/logic/fmap.rs" 375 14 375 40 - let%span sghost42 = "../../../../creusot-contracts/src/ghost.rs" 69 14 69 18 - let%span sghost43 = "../../../../creusot-contracts/src/ghost.rs" 69 4 69 36 - let%span sghost44 = "../../../../creusot-contracts/src/ghost.rs" 68 14 68 35 - let%span sfmap45 = "../../../../creusot-contracts/src/logic/fmap.rs" 264 14 264 34 - let%span sfmap46 = "../../../../creusot-contracts/src/logic/fmap.rs" 116 9 116 31 - let%span sfmap47 = "../../../../creusot-contracts/src/logic/fmap.rs" 348 36 348 39 - let%span sfmap48 = "../../../../creusot-contracts/src/logic/fmap.rs" 348 4 348 62 - let%span sfmap49 = "../../../../creusot-contracts/src/logic/fmap.rs" 336 4 345 11 - let%span sfmap50 = "../../../../creusot-contracts/src/logic/fmap.rs" 346 14 346 89 - let%span sfmap51 = "../../../../creusot-contracts/src/logic/fmap.rs" 347 14 347 44 - let%span sfmap52 = "../../../../creusot-contracts/src/logic/fmap.rs" 415 35 415 38 - let%span sfmap53 = "../../../../creusot-contracts/src/logic/fmap.rs" 415 4 417 17 - let%span sfmap54 = "../../../../creusot-contracts/src/logic/fmap.rs" 413 14 413 43 - let%span sfmap55 = "../../../../creusot-contracts/src/logic/fmap.rs" 414 14 414 41 - let%span sfmap56 = "../../../../creusot-contracts/src/logic/fmap.rs" 92 8 95 9 - let%span sfmap57 = "../../../../creusot-contracts/src/logic/fmap.rs" 285 33 285 36 - let%span sfmap58 = "../../../../creusot-contracts/src/logic/fmap.rs" 284 14 284 43 - let%span sfmap59 = "../../../../creusot-contracts/src/logic/fmap.rs" 314 28 314 31 - let%span sfmap60 = "../../../../creusot-contracts/src/logic/fmap.rs" 314 4 314 50 - let%span sfmap61 = "../../../../creusot-contracts/src/logic/fmap.rs" 306 4 313 11 - let%span sghost62 = "../../../../creusot-contracts/src/ghost.rs" 181 15 181 16 - let%span sghost63 = "../../../../creusot-contracts/src/ghost.rs" 181 4 181 28 - let%span sghost64 = "../../../../creusot-contracts/src/ghost.rs" 179 14 179 28 - let%span sfmap65 = "../../../../creusot-contracts/src/logic/fmap.rs" 39 14 39 31 - let%span sfmap66 = "../../../../creusot-contracts/src/logic/fmap.rs" 40 14 40 49 - let%span sfmap67 = "../../../../creusot-contracts/src/logic/fmap.rs" 214 14 214 38 - let%span sfmap68 = "../../../../creusot-contracts/src/logic/fmap.rs" 215 14 215 83 - let%span sfmap69 = "../../../../creusot-contracts/src/logic/fmap.rs" 217 8 217 35 - let%span sfmap70 = "../../../../creusot-contracts/src/logic/fmap.rs" 103 8 103 26 - let%span sfmap71 = "../../../../creusot-contracts/src/logic/fmap.rs" 66 14 66 71 - let%span sfmap72 = "../../../../creusot-contracts/src/logic/fmap.rs" 67 14 67 61 - let%span sfmap73 = "../../../../creusot-contracts/src/logic/fmap.rs" 68 14 68 66 - let%span sresolve74 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span sfmap75 = "../../../../creusot-contracts/src/logic/fmap.rs" 48 14 48 25 - let%span sfmap76 = "../../../../creusot-contracts/src/logic/fmap.rs" 124 8 124 35 - let%span sfmap77 = "../../../../creusot-contracts/src/logic/fmap.rs" 76 14 76 55 - let%span sfmap78 = "../../../../creusot-contracts/src/logic/fmap.rs" 77 14 77 84 - let%span sfmap79 = "../../../../creusot-contracts/src/logic/fmap.rs" 58 14 58 86 - let%span sutil80 = "../../../../creusot-contracts/src/util.rs" 21 14 21 30 - let%span sutil81 = "../../../../creusot-contracts/src/util.rs" 43 11 43 21 - let%span sutil82 = "../../../../creusot-contracts/src/util.rs" 44 10 44 28 + let%span sfmap1 = "../../../../creusot-contracts/src/logic/fmap.rs" 239 4 239 34 + let%span sfmap2 = "../../../../creusot-contracts/src/logic/fmap.rs" 237 14 237 31 + let%span sghost_map3 = "ghost_map.rs" 7 22 7 53 + let%span sghost_map4 = "ghost_map.rs" 8 25 8 26 + let%span sghost_map5 = "ghost_map.rs" 8 28 8 30 + let%span sghost_map6 = "ghost_map.rs" 10 22 10 47 + let%span sghost_map7 = "ghost_map.rs" 11 22 11 34 + let%span sghost_map8 = "ghost_map.rs" 12 28 12 29 + let%span sghost_map9 = "ghost_map.rs" 12 31 12 32 + let%span sghost_map10 = "ghost_map.rs" 12 34 12 35 + let%span sghost_map11 = "ghost_map.rs" 14 17 14 19 + let%span sghost_map12 = "ghost_map.rs" 16 22 16 47 + let%span sghost_map13 = "ghost_map.rs" 18 45 18 46 + let%span sghost_map14 = "ghost_map.rs" 18 48 18 50 + let%span sghost_map15 = "ghost_map.rs" 19 45 19 46 + let%span sghost_map16 = "ghost_map.rs" 19 48 19 51 + let%span sghost_map17 = "ghost_map.rs" 21 22 21 43 + let%span sghost_map18 = "ghost_map.rs" 22 22 22 50 + let%span sghost_map19 = "ghost_map.rs" 23 22 23 34 + let%span sghost_map20 = "ghost_map.rs" 24 22 24 48 + let%span sghost_map21 = "ghost_map.rs" 25 22 25 47 + let%span sghost_map22 = "ghost_map.rs" 30 22 30 42 + let%span sghost_map23 = "ghost_map.rs" 31 22 31 49 + let%span sghost_map24 = "ghost_map.rs" 32 22 32 42 + let%span sghost_map25 = "ghost_map.rs" 33 22 33 43 + let%span sghost_map26 = "ghost_map.rs" 38 22 38 31 + let%span sghost_map27 = "ghost_map.rs" 39 22 39 32 + let%span sghost_map28 = "ghost_map.rs" 40 22 40 32 + let%span sghost_map29 = "ghost_map.rs" 45 22 45 42 + let%span sghost_map30 = "ghost_map.rs" 46 22 46 34 + let%span sghost_map31 = "ghost_map.rs" 47 22 47 34 + let%span sghost32 = "../../../../creusot-contracts/src/ghost.rs" 217 9 217 15 + let%span sfmap33 = "../../../../creusot-contracts/src/logic/fmap.rs" 139 8 139 34 + let%span sfmap34 = "../../../../creusot-contracts/src/logic/fmap.rs" 132 8 132 35 + let%span sghost35 = "../../../../creusot-contracts/src/ghost.rs" 85 22 85 26 + let%span sghost36 = "../../../../creusot-contracts/src/ghost.rs" 85 4 85 48 + let%span sghost37 = "../../../../creusot-contracts/src/ghost.rs" 84 14 84 36 + let%span sfmap38 = "../../../../creusot-contracts/src/logic/fmap.rs" 376 29 376 33 + let%span sfmap39 = "../../../../creusot-contracts/src/logic/fmap.rs" 376 35 376 38 + let%span sfmap40 = "../../../../creusot-contracts/src/logic/fmap.rs" 376 43 376 48 + let%span sfmap41 = "../../../../creusot-contracts/src/logic/fmap.rs" 376 4 378 17 + let%span sfmap42 = "../../../../creusot-contracts/src/logic/fmap.rs" 374 14 374 49 + let%span sfmap43 = "../../../../creusot-contracts/src/logic/fmap.rs" 375 14 375 40 + let%span sghost44 = "../../../../creusot-contracts/src/ghost.rs" 69 14 69 18 + let%span sghost45 = "../../../../creusot-contracts/src/ghost.rs" 69 4 69 36 + let%span sghost46 = "../../../../creusot-contracts/src/ghost.rs" 68 14 68 35 + let%span sfmap47 = "../../../../creusot-contracts/src/logic/fmap.rs" 265 22 265 26 + let%span sfmap48 = "../../../../creusot-contracts/src/logic/fmap.rs" 264 14 264 34 + let%span sfmap49 = "../../../../creusot-contracts/src/logic/fmap.rs" 116 9 116 31 + let%span sfmap50 = "../../../../creusot-contracts/src/logic/fmap.rs" 348 30 348 34 + let%span sfmap51 = "../../../../creusot-contracts/src/logic/fmap.rs" 348 36 348 39 + let%span sfmap52 = "../../../../creusot-contracts/src/logic/fmap.rs" 348 4 348 62 + let%span sfmap53 = "../../../../creusot-contracts/src/logic/fmap.rs" 336 4 345 11 + let%span sfmap54 = "../../../../creusot-contracts/src/logic/fmap.rs" 346 14 346 89 + let%span sfmap55 = "../../../../creusot-contracts/src/logic/fmap.rs" 347 14 347 44 + let%span sfmap56 = "../../../../creusot-contracts/src/logic/fmap.rs" 415 29 415 33 + let%span sfmap57 = "../../../../creusot-contracts/src/logic/fmap.rs" 415 35 415 38 + let%span sfmap58 = "../../../../creusot-contracts/src/logic/fmap.rs" 415 4 417 17 + let%span sfmap59 = "../../../../creusot-contracts/src/logic/fmap.rs" 413 14 413 43 + let%span sfmap60 = "../../../../creusot-contracts/src/logic/fmap.rs" 414 14 414 41 + let%span sfmap61 = "../../../../creusot-contracts/src/logic/fmap.rs" 92 8 95 9 + let%span sfmap62 = "../../../../creusot-contracts/src/logic/fmap.rs" 285 27 285 31 + let%span sfmap63 = "../../../../creusot-contracts/src/logic/fmap.rs" 285 33 285 36 + let%span sfmap64 = "../../../../creusot-contracts/src/logic/fmap.rs" 284 14 284 43 + let%span sfmap65 = "../../../../creusot-contracts/src/logic/fmap.rs" 314 22 314 26 + let%span sfmap66 = "../../../../creusot-contracts/src/logic/fmap.rs" 314 28 314 31 + let%span sfmap67 = "../../../../creusot-contracts/src/logic/fmap.rs" 314 4 314 50 + let%span sfmap68 = "../../../../creusot-contracts/src/logic/fmap.rs" 306 4 313 11 + let%span sghost69 = "../../../../creusot-contracts/src/ghost.rs" 181 15 181 16 + let%span sghost70 = "../../../../creusot-contracts/src/ghost.rs" 181 4 181 28 + let%span sghost71 = "../../../../creusot-contracts/src/ghost.rs" 179 14 179 28 + let%span sfmap72 = "../../../../creusot-contracts/src/logic/fmap.rs" 39 14 39 31 + let%span sfmap73 = "../../../../creusot-contracts/src/logic/fmap.rs" 40 14 40 49 + let%span sfmap74 = "../../../../creusot-contracts/src/logic/fmap.rs" 214 14 214 38 + let%span sfmap75 = "../../../../creusot-contracts/src/logic/fmap.rs" 215 14 215 83 + let%span sfmap76 = "../../../../creusot-contracts/src/logic/fmap.rs" 217 8 217 35 + let%span sfmap77 = "../../../../creusot-contracts/src/logic/fmap.rs" 103 8 103 26 + let%span sfmap78 = "../../../../creusot-contracts/src/logic/fmap.rs" 66 14 66 71 + let%span sfmap79 = "../../../../creusot-contracts/src/logic/fmap.rs" 67 14 67 61 + let%span sfmap80 = "../../../../creusot-contracts/src/logic/fmap.rs" 68 14 68 66 + let%span sresolve81 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 + let%span sfmap82 = "../../../../creusot-contracts/src/logic/fmap.rs" 48 14 48 25 + let%span sfmap83 = "../../../../creusot-contracts/src/logic/fmap.rs" 124 8 124 35 + let%span sfmap84 = "../../../../creusot-contracts/src/logic/fmap.rs" 76 14 76 55 + let%span sfmap85 = "../../../../creusot-contracts/src/logic/fmap.rs" 77 14 77 84 + let%span sfmap86 = "../../../../creusot-contracts/src/logic/fmap.rs" 58 14 58 86 + let%span sutil87 = "../../../../creusot-contracts/src/util.rs" 21 14 21 30 + let%span sutil88 = "../../../../creusot-contracts/src/util.rs" 43 11 43 21 + let%span sutil89 = "../../../../creusot-contracts/src/util.rs" 44 10 44 28 type t_FMap'0 type t_GhostBox'0 = { t_GhostBox__0'0: t_FMap'0 } + predicate inv'0 (_1 : t_GhostBox'0) + + axiom inv_axiom'0 [@rewrite] : forall x : t_GhostBox'0 [inv'0 x] . inv'0 x = true + function inner_logic'0 (self : t_GhostBox'0) : t_FMap'0 = - [%#sghost31] self.t_GhostBox__0'0 + [%#sghost32] self.t_GhostBox__0'0 use prelude.prelude.Int function len'0 (self : t_FMap'0) : int - axiom len'0_spec : forall self : t_FMap'0 . [%#sfmap75] len'0 self >= 0 + axiom len'0_spec : forall self : t_FMap'0 . [%#sfmap82] len'0 self >= 0 use prelude.prelude.Int32 @@ -107,147 +118,150 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18] function view'0 (self : t_FMap'0) : Map.map int32 (t_Option'3) - axiom view'0_spec : forall self : t_FMap'0 . [%#sfmap79] forall m1 : t_FMap'0, m2 : t_FMap'0 . m1 <> m2 + axiom view'0_spec : forall self : t_FMap'0 . [%#sfmap86] forall m1 : t_FMap'0, m2 : t_FMap'0 . m1 <> m2 -> view'0 m1 <> view'0 m2 use map.Const function empty'0 (_1 : ()) : t_FMap'0 - axiom empty'0_spec : forall _1 : () . ([%#sfmap65] len'0 (empty'0 _1) = 0) - && ([%#sfmap66] view'0 (empty'0 _1) = Const.const (C_None'3)) + axiom empty'0_spec : forall _1 : () . ([%#sfmap72] len'0 (empty'0 _1) = 0) + && ([%#sfmap73] view'0 (empty'0 _1) = Const.const (C_None'3)) use map.Map function get_unsized'0 [@inline:trivial] (self : t_FMap'0) (k : int32) : t_Option'3 = - [%#sfmap70] Map.get (view'0 self) k + [%#sfmap77] Map.get (view'0 self) k function ext_eq'0 (self : t_FMap'0) (other : t_FMap'0) : bool = - [%#sfmap69] view'0 self = view'0 other + [%#sfmap76] view'0 self = view'0 other - axiom ext_eq'0_spec : forall self : t_FMap'0, other : t_FMap'0 . ([%#sfmap67] ext_eq'0 self other -> self = other) - && ([%#sfmap68] (forall k : int32 . get_unsized'0 self k = get_unsized'0 other k) -> ext_eq'0 self other) + axiom ext_eq'0_spec : forall self : t_FMap'0, other : t_FMap'0 . ([%#sfmap74] ext_eq'0 self other -> self = other) + && ([%#sfmap75] (forall k : int32 . get_unsized'0 self k = get_unsized'0 other k) -> ext_eq'0 self other) function is_empty'0 (self : t_FMap'0) : bool = - [%#sfmap32] ext_eq'0 self (empty'0 ()) + [%#sfmap33] ext_eq'0 self (empty'0 ()) let rec new'0 (_1:()) (return' (ret:t_GhostBox'0))= any - [ return' (result:t_GhostBox'0)-> {[%#sfmap1] is_empty'0 (inner_logic'0 result)} (! return' {result}) ] + [ return' (result:t_GhostBox'0)-> {[%#sfmap1] inv'0 result} + {[%#sfmap2] is_empty'0 (inner_logic'0 result)} + (! return' {result}) ] use prelude.prelude.Borrow function contains'0 [@inline:trivial] (self : t_FMap'0) (k : int32) : bool = - [%#sfmap33] get_unsized'0 self k <> C_None'3 + [%#sfmap34] get_unsized'0 self k <> C_None'3 - predicate inv'0 (_1 : borrowed (t_GhostBox'0)) + predicate inv'1 (_1 : borrowed (t_GhostBox'0)) - axiom inv_axiom'0 [@rewrite] : forall x : borrowed (t_GhostBox'0) [inv'0 x] . inv'0 x = true + axiom inv_axiom'1 [@rewrite] : forall x : borrowed (t_GhostBox'0) [inv'1 x] . inv'1 x = true - predicate inv'1 (_1 : borrowed (t_FMap'0)) + predicate inv'2 (_1 : borrowed (t_FMap'0)) - axiom inv_axiom'1 [@rewrite] : forall x : borrowed (t_FMap'0) [inv'1 x] . inv'1 x = true + axiom inv_axiom'2 [@rewrite] : forall x : borrowed (t_FMap'0) [inv'2 x] . inv'2 x = true - let rec deref_mut'0 (self:borrowed (t_GhostBox'0)) (return' (ret:borrowed (t_FMap'0)))= {[@expl:deref_mut 'self' type invariant] [%#sghost34] inv'0 self} + let rec deref_mut'0 (self:borrowed (t_GhostBox'0)) (return' (ret:borrowed (t_FMap'0)))= {[@expl:deref_mut 'self' type invariant] [%#sghost35] inv'1 self} any - [ return' (result:borrowed (t_FMap'0))-> {[%#sghost35] inv'1 result} - {[%#sghost36] result + [ return' (result:borrowed (t_FMap'0))-> {[%#sghost36] inv'2 result} + {[%#sghost37] result = Borrow.borrow_logic (self.current).t_GhostBox__0'0 (self.final).t_GhostBox__0'0 (Borrow.inherit_id (Borrow.get_id self) 1)} (! return' {result}) ] - predicate inv'2 (_1 : int32) + predicate inv'3 (_1 : int32) - axiom inv_axiom'2 [@rewrite] : forall x : int32 [inv'2 x] . inv'2 x = true + axiom inv_axiom'3 [@rewrite] : forall x : int32 [inv'3 x] . inv'3 x = true type t_Option'0 = | C_None'1 | C_Some'1 int32 - predicate inv'3 (_1 : t_Option'0) + predicate inv'4 (_1 : t_Option'0) - axiom inv_axiom'3 [@rewrite] : forall x : t_Option'0 [inv'3 x] . inv'3 x = true + axiom inv_axiom'4 [@rewrite] : forall x : t_Option'0 [inv'4 x] . inv'4 x = true function make_sized'0 (self : int32) : int32 - axiom make_sized'0_spec : forall self : int32 . [%#sutil80] make_sized'0 self = self + axiom make_sized'0_spec : forall self : int32 . [%#sutil87] make_sized'0 self = self use map.Map function insert'0 (self : t_FMap'0) (k : int32) (v : int32) : t_FMap'0 - axiom insert'0_spec : forall self : t_FMap'0, k : int32, v : int32 . ([%#sfmap71] view'0 (insert'0 self k v) + axiom insert'0_spec : forall self : t_FMap'0, k : int32, v : int32 . ([%#sfmap78] view'0 (insert'0 self k v) = Map.set (view'0 self) k (C_Some'3 (make_sized'0 v))) - && ([%#sfmap72] contains'0 self k -> len'0 (insert'0 self k v) = len'0 self) - && ([%#sfmap73] not contains'0 self k -> len'0 (insert'0 self k v) = len'0 self + 1) + && ([%#sfmap79] contains'0 self k -> len'0 (insert'0 self k v) = len'0 self) + && ([%#sfmap80] not contains'0 self k -> len'0 (insert'0 self k v) = len'0 self + 1) function get'0 [@inline:trivial] (self : t_FMap'0) (k : int32) : t_Option'0 = - [%#sfmap56] match get_unsized'0 self k with + [%#sfmap61] match get_unsized'0 self k with | C_None'3 -> C_None'1 | C_Some'3 x -> C_Some'1 x end - let rec insert_ghost'0 (self:borrowed (t_FMap'0)) (key:int32) (value:int32) (return' (ret:t_Option'0))= {[@expl:insert_ghost 'key' type invariant] [%#sfmap37] inv'2 key} - {[@expl:insert_ghost 'value' type invariant] [%#sfmap38] inv'2 value} + let rec insert_ghost'0 (self:borrowed (t_FMap'0)) (key:int32) (value:int32) (return' (ret:t_Option'0))= {[@expl:insert_ghost 'self' type invariant] [%#sfmap38] inv'2 self} + {[@expl:insert_ghost 'key' type invariant] [%#sfmap39] inv'3 key} + {[@expl:insert_ghost 'value' type invariant] [%#sfmap40] inv'3 value} any - [ return' (result:t_Option'0)-> {[%#sfmap39] inv'3 result} - {[%#sfmap40] self.final = insert'0 self.current key value} - {[%#sfmap41] result = get'0 self.current key} + [ return' (result:t_Option'0)-> {[%#sfmap41] inv'4 result} + {[%#sfmap42] self.final = insert'0 self.current key value} + {[%#sfmap43] result = get'0 self.current key} (! return' {result}) ] predicate resolve'3 (self : borrowed (t_FMap'0)) = - [%#sresolve74] self.final = self.current + [%#sresolve81] self.final = self.current predicate resolve'0 (_1 : borrowed (t_FMap'0)) = resolve'3 _1 - predicate inv'4 (_1 : t_GhostBox'0) + predicate inv'5 (_1 : t_GhostBox'0) - axiom inv_axiom'4 [@rewrite] : forall x : t_GhostBox'0 [inv'4 x] . inv'4 x = true + axiom inv_axiom'5 [@rewrite] : forall x : t_GhostBox'0 [inv'5 x] . inv'5 x = true - predicate inv'5 (_1 : t_FMap'0) + predicate inv'6 (_1 : t_FMap'0) - axiom inv_axiom'5 [@rewrite] : forall x : t_FMap'0 [inv'5 x] . inv'5 x = true + axiom inv_axiom'6 [@rewrite] : forall x : t_FMap'0 [inv'6 x] . inv'6 x = true - let rec deref'0 (self:t_GhostBox'0) (return' (ret:t_FMap'0))= {[@expl:deref 'self' type invariant] [%#sghost42] inv'4 self} + let rec deref'0 (self:t_GhostBox'0) (return' (ret:t_FMap'0))= {[@expl:deref 'self' type invariant] [%#sghost44] inv'5 self} any - [ return' (result:t_FMap'0)-> {[%#sghost43] inv'5 result} - {[%#sghost44] self.t_GhostBox__0'0 = result} + [ return' (result:t_FMap'0)-> {[%#sghost45] inv'6 result} + {[%#sghost46] self.t_GhostBox__0'0 = result} (! return' {result}) ] - let rec len_ghost'0 (self:t_FMap'0) (return' (ret:int))= any - [ return' (result:int)-> {[%#sfmap45] result = len'0 self} (! return' {result}) ] - + let rec len_ghost'0 (self:t_FMap'0) (return' (ret:int))= {[@expl:len_ghost 'self' type invariant] [%#sfmap47] inv'6 self} + any [ return' (result:int)-> {[%#sfmap48] result = len'0 self} (! return' {result}) ] function unwrap'0 (op : t_Option'3) : int32 - axiom unwrap'0_spec : forall op : t_Option'3 . ([%#sutil81] op <> C_None'3) - -> ([%#sutil82] C_Some'3 (unwrap'0 op) = op) + axiom unwrap'0_spec : forall op : t_Option'3 . ([%#sutil88] op <> C_None'3) + -> ([%#sutil89] C_Some'3 (unwrap'0 op) = op) function lookup_unsized'0 [@inline:trivial] (self : t_FMap'0) (k : int32) : int32 = - [%#sfmap76] unwrap'0 (get_unsized'0 self k) + [%#sfmap83] unwrap'0 (get_unsized'0 self k) function lookup'0 [@inline:trivial] (self : t_FMap'0) (k : int32) : int32 = - [%#sfmap46] lookup_unsized'0 self k + [%#sfmap49] lookup_unsized'0 self k - predicate inv'6 (_1 : int32) + predicate inv'7 (_1 : int32) - axiom inv_axiom'6 [@rewrite] : forall x : int32 [inv'6 x] . inv'6 x = true + axiom inv_axiom'7 [@rewrite] : forall x : int32 [inv'7 x] . inv'7 x = true type t_Option'1 = | C_None'0 | C_Some'0 (borrowed int32) - predicate inv'7 (_1 : t_Option'1) + predicate inv'8 (_1 : t_Option'1) - axiom inv_axiom'7 [@rewrite] : forall x : t_Option'1 [inv'7 x] . inv'7 x = true + axiom inv_axiom'8 [@rewrite] : forall x : t_Option'1 [inv'8 x] . inv'8 x = true - let rec get_mut_ghost'0 (self:borrowed (t_FMap'0)) (key:int32) (return' (ret:t_Option'1))= {[@expl:get_mut_ghost 'key' type invariant] [%#sfmap47] inv'6 key} + let rec get_mut_ghost'0 (self:borrowed (t_FMap'0)) (key:int32) (return' (ret:t_Option'1))= {[@expl:get_mut_ghost 'self' type invariant] [%#sfmap50] inv'2 self} + {[@expl:get_mut_ghost 'key' type invariant] [%#sfmap51] inv'7 key} any - [ return' (result:t_Option'1)-> {[%#sfmap48] inv'7 result} - {[%#sfmap49] if contains'0 self.current key then + [ return' (result:t_Option'1)-> {[%#sfmap52] inv'8 result} + {[%#sfmap53] if contains'0 self.current key then match result with | C_None'0 -> false | C_Some'0 r -> contains'0 self.final key @@ -256,13 +270,13 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18] else result = C_None'0 /\ self.current = self.final } - {[%#sfmap50] forall k : int32 . k <> key -> get_unsized'0 self.current k = get_unsized'0 self.final k} - {[%#sfmap51] len'0 self.current = len'0 self.final} + {[%#sfmap54] forall k : int32 . k <> key -> get_unsized'0 self.current k = get_unsized'0 self.final k} + {[%#sfmap55] len'0 self.current = len'0 self.final} (! return' {result}) ] predicate resolve'4 (self : borrowed int32) = - [%#sresolve74] self.final = self.current + [%#sresolve81] self.final = self.current predicate resolve'1 (_1 : borrowed int32) = resolve'4 _1 @@ -276,33 +290,36 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18] function remove'0 (self : t_FMap'0) (k : int32) : t_FMap'0 - axiom remove'0_spec : forall self : t_FMap'0, k : int32 . ([%#sfmap77] view'0 (remove'0 self k) + axiom remove'0_spec : forall self : t_FMap'0, k : int32 . ([%#sfmap84] view'0 (remove'0 self k) = Map.set (view'0 self) k (C_None'3)) - && ([%#sfmap78] len'0 (remove'0 self k) = (if contains'0 self k then len'0 self - 1 else len'0 self)) + && ([%#sfmap85] len'0 (remove'0 self k) = (if contains'0 self k then len'0 self - 1 else len'0 self)) - let rec remove_ghost'0 (self:borrowed (t_FMap'0)) (key:int32) (return' (ret:t_Option'0))= {[@expl:remove_ghost 'key' type invariant] [%#sfmap52] inv'6 key} + let rec remove_ghost'0 (self:borrowed (t_FMap'0)) (key:int32) (return' (ret:t_Option'0))= {[@expl:remove_ghost 'self' type invariant] [%#sfmap56] inv'2 self} + {[@expl:remove_ghost 'key' type invariant] [%#sfmap57] inv'7 key} any - [ return' (result:t_Option'0)-> {[%#sfmap53] inv'3 result} - {[%#sfmap54] self.final = remove'0 self.current key} - {[%#sfmap55] result = get'0 self.current key} + [ return' (result:t_Option'0)-> {[%#sfmap58] inv'4 result} + {[%#sfmap59] self.final = remove'0 self.current key} + {[%#sfmap60] result = get'0 self.current key} (! return' {result}) ] - let rec contains_ghost'0 (self:t_FMap'0) (key:int32) (return' (ret:bool))= {[@expl:contains_ghost 'key' type invariant] [%#sfmap57] inv'6 key} - any [ return' (result:bool)-> {[%#sfmap58] result = contains'0 self key} (! return' {result}) ] + let rec contains_ghost'0 (self:t_FMap'0) (key:int32) (return' (ret:bool))= {[@expl:contains_ghost 'self' type invariant] [%#sfmap62] inv'6 self} + {[@expl:contains_ghost 'key' type invariant] [%#sfmap63] inv'7 key} + any [ return' (result:bool)-> {[%#sfmap64] result = contains'0 self key} (! return' {result}) ] type t_Option'2 = | C_None'2 | C_Some'2 int32 - predicate inv'8 (_1 : t_Option'2) + predicate inv'9 (_1 : t_Option'2) - axiom inv_axiom'8 [@rewrite] : forall x : t_Option'2 [inv'8 x] . inv'8 x = true + axiom inv_axiom'9 [@rewrite] : forall x : t_Option'2 [inv'9 x] . inv'9 x = true - let rec get_ghost'0 (self:t_FMap'0) (key:int32) (return' (ret:t_Option'2))= {[@expl:get_ghost 'key' type invariant] [%#sfmap59] inv'6 key} + let rec get_ghost'0 (self:t_FMap'0) (key:int32) (return' (ret:t_Option'2))= {[@expl:get_ghost 'self' type invariant] [%#sfmap65] inv'6 self} + {[@expl:get_ghost 'key' type invariant] [%#sfmap66] inv'7 key} any - [ return' (result:t_Option'2)-> {[%#sfmap60] inv'8 result} - {[%#sfmap61] if contains'0 self key then + [ return' (result:t_Option'2)-> {[%#sfmap67] inv'9 result} + {[%#sfmap68] if contains'0 self key then match result with | C_None'2 -> false | C_Some'2 r -> lookup_unsized'0 self key = r @@ -317,7 +334,7 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18] { field_0'0: borrowed (t_GhostBox'0) } predicate resolve'6 (self : borrowed (t_GhostBox'0)) = - [%#sresolve74] self.final = self.current + [%#sresolve81] self.final = self.current predicate resolve'5 (_1 : borrowed (t_GhostBox'0)) = resolve'6 _1 @@ -325,21 +342,21 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18] predicate resolve'2 (_1 : closure0'1) = resolve'5 _1.field_0'0 - predicate inv'9 (_1 : ()) + predicate inv'10 (_1 : ()) - axiom inv_axiom'9 [@rewrite] : forall x : () [inv'9 x] . inv'9 x = true + axiom inv_axiom'10 [@rewrite] : forall x : () [inv'10 x] . inv'10 x = true type t_GhostBox'1 = { t_GhostBox__0'1: () } - predicate inv'10 (_1 : t_GhostBox'1) + predicate inv'11 (_1 : t_GhostBox'1) - axiom inv_axiom'10 [@rewrite] : forall x : t_GhostBox'1 [inv'10 x] . inv'10 x = true + axiom inv_axiom'11 [@rewrite] : forall x : t_GhostBox'1 [inv'11 x] . inv'11 x = true - let rec new'1 (x:()) (return' (ret:t_GhostBox'1))= {[@expl:new 'x' type invariant] [%#sghost62] inv'9 x} + let rec new'1 (x:()) (return' (ret:t_GhostBox'1))= {[@expl:new 'x' type invariant] [%#sghost69] inv'10 x} any - [ return' (result:t_GhostBox'1)-> {[%#sghost63] inv'10 result} - {[%#sghost64] result.t_GhostBox__0'1 = x} + [ return' (result:t_GhostBox'1)-> {[%#sghost70] inv'11 result} + {[%#sghost71] result.t_GhostBox__0'1 = x} (! return' {result}) ] @@ -347,7 +364,7 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18] let rec closure0'0 (_1:closure0'1) (return' (ret:t_GhostBox'1))= bb0 [ bb0 = s0 - [ s0 = {[@expl:assertion] [%#sghost_map2] forall k : int32 . not contains'0 (inner_logic'0 (_1.field_0'0).current) k} + [ s0 = {[@expl:assertion] [%#sghost_map3] forall k : int32 . not contains'0 (inner_logic'0 (_1.field_0'0).current) k} s1 | s1 = Borrow.borrow_mut {(_1.field_0'0).current} (fun (_ret':borrowed (t_GhostBox'0)) -> @@ -360,7 +377,7 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18] | bb1 = s0 [ s0 = Borrow.borrow_final {_7.current} {Borrow.get_id _7} (fun (_ret':borrowed (t_FMap'0)) -> [ &_6 <- _ret' ] [ &_7 <- { _7 with current = _ret'.final } ] s1) - | s1 = insert_ghost'0 {_6} {[%#sghost_map3] (1 : int32)} {[%#sghost_map4] (21 : int32)} + | s1 = insert_ghost'0 {_6} {[%#sghost_map4] (1 : int32)} {[%#sghost_map5] (21 : int32)} (fun (_ret':t_Option'0) -> [ &_5 <- _ret' ] s2) | s2 = bb2 ] @@ -371,11 +388,13 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18] | bb3 = s0 [ s0 = len_ghost'0 {_11} (fun (_ret':int) -> [ &length1 <- _ret' ] s1) | s1 = bb4 ] | bb4 = s0 - [ s0 = {[@expl:assertion] [%#sghost_map5] lookup'0 (inner_logic'0 (_1.field_0'0).current) (1 : int32) + [ s0 = {[@expl:assertion] [%#sghost_map6] lookup'0 (inner_logic'0 (_1.field_0'0).current) (1 : int32) = (21 : int32)} s1 - | s1 = {[@expl:assertion] [%#sghost_map6] length1 = 1} s2 - | s2 = [ &_20 <- (([%#sghost_map7] (1 : int32)), ([%#sghost_map8] (2 : int32)), ([%#sghost_map9] (3 : int32))) ] + | s1 = {[@expl:assertion] [%#sghost_map7] length1 = 1} s2 + | s2 = + [ &_20 <- (([%#sghost_map8] (1 : int32)), ([%#sghost_map9] (2 : int32)), ([%#sghost_map10] (3 : int32))) ] + s3 | s3 = [ &x1 <- let (r'0, _, _) = _20 in r'0 ] s4 | s4 = [ &x2 <- let (_, r'1, _) = _20 in r'1 ] s5 @@ -408,13 +427,13 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18] | bb7 = bb8 | bb8 = s0 [ s0 = v_Some'0 {_22} (fun (r0'0:borrowed int32) -> [ &x <- r0'0 ] s1) - | s1 = [ &x <- { x with current = ([%#sghost_map10] (42 : int32)) } ] s2 + | s1 = [ &x <- { x with current = ([%#sghost_map11] (42 : int32)) } ] s2 | s2 = -{resolve'1 x}- s3 | s3 = -{resolve'0 _24}- s4 | s4 = bb10 ] | bb10 = s0 - [ s0 = {[@expl:assertion] [%#sghost_map11] lookup'0 (inner_logic'0 (_1.field_0'0).current) (1 : int32) + [ s0 = {[@expl:assertion] [%#sghost_map12] lookup'0 (inner_logic'0 (_1.field_0'0).current) (1 : int32) = (42 : int32)} s1 | s1 = Borrow.borrow_mut {(_1.field_0'0).current} @@ -428,7 +447,7 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18] | bb11 = s0 [ s0 = Borrow.borrow_final {_34.current} {Borrow.get_id _34} (fun (_ret':borrowed (t_FMap'0)) -> [ &_33 <- _ret' ] [ &_34 <- { _34 with current = _ret'.final } ] s1) - | s1 = insert_ghost'0 {_33} {[%#sghost_map12] (2 : int32)} {[%#sghost_map13] (50 : int32)} + | s1 = insert_ghost'0 {_33} {[%#sghost_map13] (2 : int32)} {[%#sghost_map14] (50 : int32)} (fun (_ret':t_Option'0) -> [ &inserted_none <- _ret' ] s2) | s2 = bb12 ] @@ -445,7 +464,7 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18] | bb13 = s0 [ s0 = Borrow.borrow_final {_38.current} {Borrow.get_id _38} (fun (_ret':borrowed (t_FMap'0)) -> [ &_37 <- _ret' ] [ &_38 <- { _38 with current = _ret'.final } ] s1) - | s1 = insert_ghost'0 {_37} {[%#sghost_map14] (2 : int32)} {[%#sghost_map15] (100 : int32)} + | s1 = insert_ghost'0 {_37} {[%#sghost_map15] (2 : int32)} {[%#sghost_map16] (100 : int32)} (fun (_ret':t_Option'0) -> [ &inserted_some <- _ret' ] s2) | s2 = bb14 ] @@ -456,13 +475,13 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18] | bb15 = s0 [ s0 = len_ghost'0 {_42} (fun (_ret':int) -> [ &length2 <- _ret' ] s1) | s1 = bb16 ] | bb16 = s0 - [ s0 = {[@expl:assertion] [%#sghost_map16] inserted_none = C_None'1} s1 - | s1 = {[@expl:assertion] [%#sghost_map17] inserted_some = C_Some'1 (50 : int32)} s2 - | s2 = {[@expl:assertion] [%#sghost_map18] length2 = 2} s3 - | s3 = {[@expl:assertion] [%#sghost_map19] lookup'0 (inner_logic'0 (_1.field_0'0).current) (2 : int32) + [ s0 = {[@expl:assertion] [%#sghost_map17] inserted_none = C_None'1} s1 + | s1 = {[@expl:assertion] [%#sghost_map18] inserted_some = C_Some'1 (50 : int32)} s2 + | s2 = {[@expl:assertion] [%#sghost_map19] length2 = 2} s3 + | s3 = {[@expl:assertion] [%#sghost_map20] lookup'0 (inner_logic'0 (_1.field_0'0).current) (2 : int32) = (100 : int32)} s4 - | s4 = {[@expl:assertion] [%#sghost_map20] lookup'0 (inner_logic'0 (_1.field_0'0).current) (1 : int32) + | s4 = {[@expl:assertion] [%#sghost_map21] lookup'0 (inner_logic'0 (_1.field_0'0).current) (1 : int32) = (42 : int32)} s5 | s5 = Borrow.borrow_mut {(_1.field_0'0).current} @@ -516,10 +535,10 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18] | bb22 = s0 [ s0 = -{resolve'0 _68}- s1 - | s1 = {[@expl:assertion] [%#sghost_map21] remove_none1 = C_None'1} s2 - | s2 = {[@expl:assertion] [%#sghost_map22] remove_some = C_Some'1 (100 : int32)} s3 - | s3 = {[@expl:assertion] [%#sghost_map23] remove_none2 = C_None'1} s4 - | s4 = {[@expl:assertion] [%#sghost_map24] get'0 (inner_logic'0 (_1.field_0'0).current) (2 : int32) = C_None'1} s5 + | s1 = {[@expl:assertion] [%#sghost_map22] remove_none1 = C_None'1} s2 + | s2 = {[@expl:assertion] [%#sghost_map23] remove_some = C_Some'1 (100 : int32)} s3 + | s3 = {[@expl:assertion] [%#sghost_map24] remove_none2 = C_None'1} s4 + | s4 = {[@expl:assertion] [%#sghost_map25] get'0 (inner_logic'0 (_1.field_0'0).current) (2 : int32) = C_None'1} s5 | s5 = deref'0 {(_1.field_0'0).current} (fun (_ret':t_FMap'0) -> [ &_82 <- _ret' ] s6) | s6 = bb23 ] @@ -541,9 +560,9 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18] | s2 = bb28 ] | bb28 = s0 - [ s0 = {[@expl:assertion] [%#sghost_map25] contains1} s1 - | s1 = {[@expl:assertion] [%#sghost_map26] not contains2} s2 - | s2 = {[@expl:assertion] [%#sghost_map27] not contains3} s3 + [ s0 = {[@expl:assertion] [%#sghost_map26] contains1} s1 + | s1 = {[@expl:assertion] [%#sghost_map27] not contains2} s2 + | s2 = {[@expl:assertion] [%#sghost_map28] not contains3} s3 | s3 = deref'0 {(_1.field_0'0).current} (fun (_ret':t_FMap'0) -> [ &_106 <- _ret' ] s4) | s4 = bb29 ] @@ -566,9 +585,9 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18] | bb34 = s0 [ s0 = -{resolve'2 _1}- s1 - | s1 = {[@expl:assertion] [%#sghost_map28] get1 = C_Some'2 (42 : int32)} s2 - | s2 = {[@expl:assertion] [%#sghost_map29] get2 = C_None'2} s3 - | s3 = {[@expl:assertion] [%#sghost_map30] get3 = C_None'2} s4 + | s1 = {[@expl:assertion] [%#sghost_map29] get1 = C_Some'2 (42 : int32)} s2 + | s2 = {[@expl:assertion] [%#sghost_map30] get2 = C_None'2} s3 + | s3 = {[@expl:assertion] [%#sghost_map31] get3 = C_None'2} s4 | s4 = new'1 {_2} (fun (_ret':t_GhostBox'1) -> [ &_0 <- _ret' ] s5) | s5 = bb35 ] diff --git a/creusot/tests/should_succeed/ghost/ghost_map/why3session.xml b/creusot/tests/should_succeed/ghost/ghost_map/why3session.xml index 0c98bfe61..fb4e30b79 100644 --- a/creusot/tests/should_succeed/ghost/ghost_map/why3session.xml +++ b/creusot/tests/should_succeed/ghost/ghost_map/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/ghost/ghost_map/why3shapes.gz b/creusot/tests/should_succeed/ghost/ghost_map/why3shapes.gz index d2efb203a4e7c926c7f5466f9073c6ca2e6bc9c5..1a76a6eab40de853e81895879a85fba614376365 100644 GIT binary patch delta 688 zcmV;h0#E(M1-=E48h;xDl~O5M2|1TsTFn*B5@#1Bfh>@0w_jhGU?*hL-R$i#o_X`; zd4Ml>llF;rrkxy2)0TDhW1=Q^UxV(M%IXj@WSIj2{hZRqR3SqsSQad3N{7ZPHbB}oy|ek~yNH}834n9Jwe57dWTy9u_cmq|dx`WXyAJ$1(6mW{O;99{D|D$fN88eH@Uh z>;!`$g{XSXH}reI+ZbjyHRi4r?;m0O$ef+LkbF*!X@Bd@!GxTOP2KJr!$JtRYkH`g zrhYNYaJxp8(5kFxgMw4JM8W6fxX=B{Lu+eYulKw2w<<;n7z^JSZSly_K4o|*kB-DV zn+0^-LSX$rhY67R035@ zW%Xp5vdhb5|7|aq&$tD~$XDJ#|4T*+WgVGRbkQ#&rt^qVKo$5r# WTIonjEi~7lS?~|LosrGW2LJ$7x>5uH delta 696 zcmV;p0!RJ61;z!C8h?X%hm!P!MgAPXeh?blZ(*a=BC+1?)GnK#eR zWBlb|(!S7Ex0AhY+On>GOyuO@t4BYlwAPi+kmW4(7Br=Oso#8t+yXIQ&=fg}H1*sv z>CLu#_ZbG1*HzomW45R(?TZ-=gvSg+OjFW-x=g?N3`3OkyMNi~IZf$VciFCL%fGtl zSE93s#3-H7)YQzcaim`NN@cb88OEsvHU^la7T6d^V5vhkDi9!b$f(`WN@rFDa0K3O z;;^-{YIW0@1%VJCg!FB25kwBgFXKvQ@@!JCc6Nio*3WMh59VK1x4N_Eb*OmEe$^Z8 zi?fY{&aePMrhg9EXowJ{4w)T0qFwdY(AJQ|2ys6Y5W91Cyb@t>-5?u{kPo&Sbab-O zn|iO!xB+rr4lZz@?+)fLcBIcdcVx_SYR4gPAu~oUQip6bK^~+IxjACU!}JKfLk3ax zo~`NkZoAgZ3~2M(}llT zp^Ru*R;UXJ@bE*&(U*7a()J-t2>1BMZIozWDJ?Cev9`*^S;f^;?}Bivxy(^=l#?zg9(jOae1|-ghCfVlFb8T? zA1^KQ`sXd{A63s=auI7Giy#V?QnM&7L>MoZnlbU@=?P>$;Y>lIAXX45kP1QtfdZj` eD*y#dB`Q{tk}6bz5{fHO%=-rydlV$K2LJ% {[%#sfset1] Fset.is_empty (inner_logic'0 result)} (! return' {result}) ] + [ return' (result:t_GhostBox'0)-> {[%#sfset1] inv'0 result} + {[%#sfset2] Fset.is_empty (inner_logic'0 result)} + (! return' {result}) ] use prelude.prelude.Borrow @@ -64,58 +75,59 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18] use set.Fset predicate contains'0 [@inline:trivial] (self : Fset.fset int32) (e : int32) = - [%#sfset21] Fset.mem e self + [%#sfset22] Fset.mem e self - predicate inv'0 (_1 : borrowed (t_GhostBox'0)) + predicate inv'1 (_1 : borrowed (t_GhostBox'0)) - axiom inv_axiom'0 [@rewrite] : forall x : borrowed (t_GhostBox'0) [inv'0 x] . inv'0 x = true + axiom inv_axiom'1 [@rewrite] : forall x : borrowed (t_GhostBox'0) [inv'1 x] . inv'1 x = true - predicate inv'1 (_1 : borrowed (Fset.fset int32)) + predicate inv'2 (_1 : borrowed (Fset.fset int32)) - axiom inv_axiom'1 [@rewrite] : forall x : borrowed (Fset.fset int32) [inv'1 x] . inv'1 x = true + axiom inv_axiom'2 [@rewrite] : forall x : borrowed (Fset.fset int32) [inv'2 x] . inv'2 x = true - let rec deref_mut'0 (self:borrowed (t_GhostBox'0)) (return' (ret:borrowed (Fset.fset int32)))= {[@expl:deref_mut 'self' type invariant] [%#sghost22] inv'0 self} + let rec deref_mut'0 (self:borrowed (t_GhostBox'0)) (return' (ret:borrowed (Fset.fset int32)))= {[@expl:deref_mut 'self' type invariant] [%#sghost23] inv'1 self} any - [ return' (result:borrowed (Fset.fset int32))-> {[%#sghost23] inv'1 result} - {[%#sghost24] result + [ return' (result:borrowed (Fset.fset int32))-> {[%#sghost24] inv'2 result} + {[%#sghost25] result = Borrow.borrow_logic (self.current).t_GhostBox__0'0 (self.final).t_GhostBox__0'0 (Borrow.inherit_id (Borrow.get_id self) 1)} (! return' {result}) ] - predicate inv'2 (_1 : int32) + predicate inv'3 (_1 : int32) - axiom inv_axiom'2 [@rewrite] : forall x : int32 [inv'2 x] . inv'2 x = true + axiom inv_axiom'3 [@rewrite] : forall x : int32 [inv'3 x] . inv'3 x = true use set.Fset function insert'0 [@inline:trivial] (self : Fset.fset int32) (e : int32) : Fset.fset int32 = - [%#sfset40] Fset.add e self + [%#sfset45] Fset.add e self - let rec insert_ghost'0 (self:borrowed (Fset.fset int32)) (value:int32) (return' (ret:bool))= {[@expl:insert_ghost 'value' type invariant] [%#sfset25] inv'2 value} + let rec insert_ghost'0 (self:borrowed (Fset.fset int32)) (value:int32) (return' (ret:bool))= {[@expl:insert_ghost 'self' type invariant] [%#sfset26] inv'2 self} + {[@expl:insert_ghost 'value' type invariant] [%#sfset27] inv'3 value} any - [ return' (result:bool)-> {[%#sfset26] self.final = insert'0 self.current value} - {[%#sfset27] result = (not contains'0 self.current value)} + [ return' (result:bool)-> {[%#sfset28] self.final = insert'0 self.current value} + {[%#sfset29] result = (not contains'0 self.current value)} (! return' {result}) ] predicate resolve'2 (self : borrowed (Fset.fset int32)) = - [%#sresolve41] self.final = self.current + [%#sresolve46] self.final = self.current predicate resolve'0 (_1 : borrowed (Fset.fset int32)) = resolve'2 _1 - predicate inv'3 (_1 : t_GhostBox'0) + predicate inv'4 (_1 : t_GhostBox'0) - axiom inv_axiom'3 [@rewrite] : forall x : t_GhostBox'0 [inv'3 x] . inv'3 x = true + axiom inv_axiom'4 [@rewrite] : forall x : t_GhostBox'0 [inv'4 x] . inv'4 x = true - predicate inv'4 (_1 : Fset.fset int32) + predicate inv'5 (_1 : Fset.fset int32) - axiom inv_axiom'4 [@rewrite] : forall x : Fset.fset int32 [inv'4 x] . inv'4 x = true + axiom inv_axiom'5 [@rewrite] : forall x : Fset.fset int32 [inv'5 x] . inv'5 x = true - let rec deref'0 (self:t_GhostBox'0) (return' (ret:Fset.fset int32))= {[@expl:deref 'self' type invariant] [%#sghost28] inv'3 self} + let rec deref'0 (self:t_GhostBox'0) (return' (ret:Fset.fset int32))= {[@expl:deref 'self' type invariant] [%#sghost30] inv'4 self} any - [ return' (result:Fset.fset int32)-> {[%#sghost29] inv'4 result} - {[%#sghost30] self.t_GhostBox__0'0 = result} + [ return' (result:Fset.fset int32)-> {[%#sghost31] inv'5 result} + {[%#sghost32] self.t_GhostBox__0'0 = result} (! return' {result}) ] @@ -123,34 +135,35 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18] use prelude.prelude.Int - let rec len_ghost'0 (self:Fset.fset int32) (return' (ret:int))= any - [ return' (result:int)-> {[%#sfset31] result = Fset.cardinal self} (! return' {result}) ] - + let rec len_ghost'0 (self:Fset.fset int32) (return' (ret:int))= {[@expl:len_ghost 'self' type invariant] [%#sfset33] inv'5 self} + any [ return' (result:int)-> {[%#sfset34] result = Fset.cardinal self} (! return' {result}) ] - predicate inv'5 (_1 : int32) + predicate inv'6 (_1 : int32) - axiom inv_axiom'5 [@rewrite] : forall x : int32 [inv'5 x] . inv'5 x = true + axiom inv_axiom'6 [@rewrite] : forall x : int32 [inv'6 x] . inv'6 x = true use set.Fset function remove'0 [@inline:trivial] (self : Fset.fset int32) (e : int32) : Fset.fset int32 = - [%#sfset42] Fset.remove e self + [%#sfset47] Fset.remove e self - let rec remove_ghost'0 (self:borrowed (Fset.fset int32)) (value:int32) (return' (ret:bool))= {[@expl:remove_ghost 'value' type invariant] [%#sfset32] inv'5 value} + let rec remove_ghost'0 (self:borrowed (Fset.fset int32)) (value:int32) (return' (ret:bool))= {[@expl:remove_ghost 'self' type invariant] [%#sfset35] inv'2 self} + {[@expl:remove_ghost 'value' type invariant] [%#sfset36] inv'6 value} any - [ return' (result:bool)-> {[%#sfset33] self.final = remove'0 self.current value} - {[%#sfset34] result = contains'0 self.current value} + [ return' (result:bool)-> {[%#sfset37] self.final = remove'0 self.current value} + {[%#sfset38] result = contains'0 self.current value} (! return' {result}) ] - let rec contains_ghost'0 (self:Fset.fset int32) (value:int32) (return' (ret:bool))= {[@expl:contains_ghost 'value' type invariant] [%#sfset35] inv'5 value} - any [ return' (result:bool)-> {[%#sfset36] result = contains'0 self value} (! return' {result}) ] + let rec contains_ghost'0 (self:Fset.fset int32) (value:int32) (return' (ret:bool))= {[@expl:contains_ghost 'self' type invariant] [%#sfset39] inv'5 self} + {[@expl:contains_ghost 'value' type invariant] [%#sfset40] inv'6 value} + any [ return' (result:bool)-> {[%#sfset41] result = contains'0 self value} (! return' {result}) ] type closure0'1 = { field_0'0: borrowed (t_GhostBox'0) } predicate resolve'4 (self : borrowed (t_GhostBox'0)) = - [%#sresolve41] self.final = self.current + [%#sresolve46] self.final = self.current predicate resolve'3 (_1 : borrowed (t_GhostBox'0)) = resolve'4 _1 @@ -158,21 +171,21 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18] predicate resolve'1 (_1 : closure0'1) = resolve'3 _1.field_0'0 - predicate inv'6 (_1 : ()) + predicate inv'7 (_1 : ()) - axiom inv_axiom'6 [@rewrite] : forall x : () [inv'6 x] . inv'6 x = true + axiom inv_axiom'7 [@rewrite] : forall x : () [inv'7 x] . inv'7 x = true type t_GhostBox'1 = { t_GhostBox__0'1: () } - predicate inv'7 (_1 : t_GhostBox'1) + predicate inv'8 (_1 : t_GhostBox'1) - axiom inv_axiom'7 [@rewrite] : forall x : t_GhostBox'1 [inv'7 x] . inv'7 x = true + axiom inv_axiom'8 [@rewrite] : forall x : t_GhostBox'1 [inv'8 x] . inv'8 x = true - let rec new'1 (x:()) (return' (ret:t_GhostBox'1))= {[@expl:new 'x' type invariant] [%#sghost37] inv'6 x} + let rec new'1 (x:()) (return' (ret:t_GhostBox'1))= {[@expl:new 'x' type invariant] [%#sghost42] inv'7 x} any - [ return' (result:t_GhostBox'1)-> {[%#sghost38] inv'7 result} - {[%#sghost39] result.t_GhostBox__0'1 = x} + [ return' (result:t_GhostBox'1)-> {[%#sghost43] inv'8 result} + {[%#sghost44] result.t_GhostBox__0'1 = x} (! return' {result}) ] @@ -180,7 +193,7 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18] let rec closure0'0 (_1:closure0'1) (return' (ret:t_GhostBox'1))= bb0 [ bb0 = s0 - [ s0 = {[@expl:assertion] [%#sghost_set2] forall k : int32 . not contains'0 (inner_logic'0 (_1.field_0'0).current) k} + [ s0 = {[@expl:assertion] [%#sghost_set3] forall k : int32 . not contains'0 (inner_logic'0 (_1.field_0'0).current) k} s1 | s1 = Borrow.borrow_mut {(_1.field_0'0).current} (fun (_ret':borrowed (t_GhostBox'0)) -> @@ -193,7 +206,7 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18] | bb1 = s0 [ s0 = Borrow.borrow_final {_7.current} {Borrow.get_id _7} (fun (_ret':borrowed (Fset.fset int32)) -> [ &_6 <- _ret' ] [ &_7 <- { _7 with current = _ret'.final } ] s1) - | s1 = insert_ghost'0 {_6} {[%#sghost_set3] (1 : int32)} (fun (_ret':bool) -> [ &_5 <- _ret' ] s2) + | s1 = insert_ghost'0 {_6} {[%#sghost_set4] (1 : int32)} (fun (_ret':bool) -> [ &_5 <- _ret' ] s2) | s2 = bb2 ] | bb2 = s0 @@ -203,11 +216,11 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18] | bb3 = s0 [ s0 = len_ghost'0 {_11} (fun (_ret':int) -> [ &length1 <- _ret' ] s1) | s1 = bb4 ] | bb4 = s0 - [ s0 = {[@expl:assertion] [%#sghost_set4] contains'0 (inner_logic'0 (_1.field_0'0).current) (1 : int32) + [ s0 = {[@expl:assertion] [%#sghost_set5] contains'0 (inner_logic'0 (_1.field_0'0).current) (1 : int32) /\ not contains'0 (inner_logic'0 (_1.field_0'0).current) (2 : int32)} s1 - | s1 = {[@expl:assertion] [%#sghost_set5] length1 = 1} s2 - | s2 = [ &_20 <- (([%#sghost_set6] (1 : int32)), ([%#sghost_set7] (2 : int32)), ([%#sghost_set8] (3 : int32))) ] + | s1 = {[@expl:assertion] [%#sghost_set6] length1 = 1} s2 + | s2 = [ &_20 <- (([%#sghost_set7] (1 : int32)), ([%#sghost_set8] (2 : int32)), ([%#sghost_set9] (3 : int32))) ] s3 | s3 = [ &x1 <- let (r'0, _, _) = _20 in r'0 ] s4 | s4 = [ &x2 <- let (_, r'1, _) = _20 in r'1 ] s5 @@ -226,7 +239,7 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18] [ &_22 <- _ret' ] [ &_23 <- { _23 with current = _ret'.final } ] s1) - | s1 = insert_ghost'0 {_22} {[%#sghost_set9] (2 : int32)} (fun (_ret':bool) -> [ &inserted_true <- _ret' ] s2) + | s1 = insert_ghost'0 {_22} {[%#sghost_set10] (2 : int32)} (fun (_ret':bool) -> [ &inserted_true <- _ret' ] s2) | s2 = bb6 ] | bb6 = s0 @@ -245,7 +258,7 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18] [ &_26 <- _ret' ] [ &_27 <- { _27 with current = _ret'.final } ] s1) - | s1 = insert_ghost'0 {_26} {[%#sghost_set10] (2 : int32)} (fun (_ret':bool) -> [ &inserted_false <- _ret' ] s2) + | s1 = insert_ghost'0 {_26} {[%#sghost_set11] (2 : int32)} (fun (_ret':bool) -> [ &inserted_false <- _ret' ] s2) | s2 = bb8 ] | bb8 = s0 @@ -255,9 +268,9 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18] | bb9 = s0 [ s0 = len_ghost'0 {_31} (fun (_ret':int) -> [ &length2 <- _ret' ] s1) | s1 = bb10 ] | bb10 = s0 - [ s0 = {[@expl:assertion] [%#sghost_set11] inserted_true /\ not inserted_false} s1 - | s1 = {[@expl:assertion] [%#sghost_set12] length2 = 2} s2 - | s2 = {[@expl:assertion] [%#sghost_set13] contains'0 (inner_logic'0 (_1.field_0'0).current) (1 : int32) + [ s0 = {[@expl:assertion] [%#sghost_set12] inserted_true /\ not inserted_false} s1 + | s1 = {[@expl:assertion] [%#sghost_set13] length2 = 2} s2 + | s2 = {[@expl:assertion] [%#sghost_set14] contains'0 (inner_logic'0 (_1.field_0'0).current) (1 : int32) /\ contains'0 (inner_logic'0 (_1.field_0'0).current) (2 : int32)} s3 | s3 = Borrow.borrow_mut {(_1.field_0'0).current} @@ -320,9 +333,9 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18] | bb16 = s0 [ s0 = -{resolve'0 _53}- s1 - | s1 = {[@expl:assertion] [%#sghost_set14] not remove_false1 /\ remove_true /\ not remove_false2} s2 - | s2 = {[@expl:assertion] [%#sghost_set15] not contains'0 (inner_logic'0 (_1.field_0'0).current) (2 : int32)} s3 - | s3 = {[@expl:assertion] [%#sghost_set16] Fset.cardinal (inner_logic'0 (_1.field_0'0).current) = 1} s4 + | s1 = {[@expl:assertion] [%#sghost_set15] not remove_false1 /\ remove_true /\ not remove_false2} s2 + | s2 = {[@expl:assertion] [%#sghost_set16] not contains'0 (inner_logic'0 (_1.field_0'0).current) (2 : int32)} s3 + | s3 = {[@expl:assertion] [%#sghost_set17] Fset.cardinal (inner_logic'0 (_1.field_0'0).current) = 1} s4 | s4 = deref'0 {(_1.field_0'0).current} (fun (_ret':Fset.fset int32) -> [ &_65 <- _ret' ] s5) | s5 = bb17 ] @@ -349,9 +362,9 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18] | bb22 = s0 [ s0 = -{resolve'1 _1}- s1 - | s1 = {[@expl:assertion] [%#sghost_set17] contains1} s2 - | s2 = {[@expl:assertion] [%#sghost_set18] not contains2} s3 - | s3 = {[@expl:assertion] [%#sghost_set19] not contains3} s4 + | s1 = {[@expl:assertion] [%#sghost_set18] contains1} s2 + | s2 = {[@expl:assertion] [%#sghost_set19] not contains2} s3 + | s3 = {[@expl:assertion] [%#sghost_set20] not contains3} s4 | s4 = new'1 {_2} (fun (_ret':t_GhostBox'1) -> [ &_0 <- _ret' ] s5) | s5 = bb23 ] diff --git a/creusot/tests/should_succeed/ghost/ghost_set/why3session.xml b/creusot/tests/should_succeed/ghost/ghost_set/why3session.xml index cbca4290d..f7c485e07 100644 --- a/creusot/tests/should_succeed/ghost/ghost_set/why3session.xml +++ b/creusot/tests/should_succeed/ghost/ghost_set/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/ghost/ghost_set/why3shapes.gz b/creusot/tests/should_succeed/ghost/ghost_set/why3shapes.gz index ee3c4c000c2114287bc62048a5a8332da9073cfa..55a9638a9f0b5869423f3e759e92edf529670832 100644 GIT binary patch literal 401 zcmV;C0dD>uiwFP!00000|Fx7qZ-X!p#dkgh8*L~5gWyUTSS)AB6x|wKjnkqMNDN8U zZ(jv+B#qQcm70m4-kEoI&xnVoxO>B$@8Y8mUDY|}A?N9x5y1?|mlJ;eSp*yJJp=E3)ujV2HNyGMa@bQsF2!Fup0mba6QnTaVg znO~xmxB0Q}iE-SVoX_IAZeJ@0Qi0T1HE%vt{kkgg)en#BH)RHj{ZJS#!Eu}_|Lc1l zE4o7nzUlAM=zQto9O3*FSMb|*i1EISZ$B|{ee$loPfLC~@W1wv-|qU)_3%H7BIK!d vI?uI!DYX`2vnjKULWL@miU}EWX0^@j%w{&V%1SFNw=DVs)$^9{5(NMNmy^XH literal 421 zcmV;W0b2eaiwFP!00000|Fx7)Z=)~}#qWFyZnQnw41Y|e9N2@`kybrbb43%!X;2AH z3`w`&z6!*ljZ&#AZBG33M$a>T9&z^&c5B+2E<705)wX>Mv+&_Q=yz1NhlnAQ9=yhp zOAlU)F_s>@1_;uF*Ah&m2d|}=N)KMkFq0mZ{*t+x5Tf--rzrA-~%& z$gXWzED+$z_<`AM`}b=2cLf2@g@&ZyB1?0C#Zs(zRxENbg(=v|h_FyX