From d0c5bae1a2aacce7a3c3ea08193f642f2ae96fae Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Sat, 20 Jan 2024 11:51:42 +0000 Subject: [PATCH] Add tests for final borrows --- creusot/tests/should_fail/bug/869.mlcfg | 74 + creusot/tests/should_fail/bug/869.rs | 21 + .../tests/should_fail/bug/869/why3session.xml | 48 + .../tests/should_fail/bug/869/why3shapes.gz | Bin 0 -> 790 bytes creusot/tests/should_fail/final_borrows.mlcfg | 394 +++++ creusot/tests/should_fail/final_borrows.rs | 39 + .../should_fail/final_borrows/why3session.xml | 143 ++ .../should_fail/final_borrows/why3shapes.gz | Bin 0 -> 2168 bytes .../should_succeed/bug/final_borrows.mlcfg | 1505 +++++++++++++++++ .../tests/should_succeed/bug/final_borrows.rs | 179 ++ .../bug/final_borrows/why3session.xml | 116 ++ .../bug/final_borrows/why3shapes.gz | Bin 0 -> 2800 bytes 12 files changed, 2519 insertions(+) create mode 100644 creusot/tests/should_fail/bug/869.mlcfg create mode 100644 creusot/tests/should_fail/bug/869.rs create mode 100644 creusot/tests/should_fail/bug/869/why3session.xml create mode 100644 creusot/tests/should_fail/bug/869/why3shapes.gz create mode 100644 creusot/tests/should_fail/final_borrows.mlcfg create mode 100644 creusot/tests/should_fail/final_borrows.rs create mode 100644 creusot/tests/should_fail/final_borrows/why3session.xml create mode 100644 creusot/tests/should_fail/final_borrows/why3shapes.gz create mode 100644 creusot/tests/should_succeed/bug/final_borrows.mlcfg create mode 100644 creusot/tests/should_succeed/bug/final_borrows.rs create mode 100644 creusot/tests/should_succeed/bug/final_borrows/why3session.xml create mode 100644 creusot/tests/should_succeed/bug/final_borrows/why3shapes.gz diff --git a/creusot/tests/should_fail/bug/869.mlcfg b/creusot/tests/should_fail/bug/869.mlcfg new file mode 100644 index 0000000000..f4bf3a9e22 --- /dev/null +++ b/creusot/tests/should_fail/bug/869.mlcfg @@ -0,0 +1,74 @@ + +module C869_Unsound + use prelude.Ghost + use prelude.Borrow + use prelude.Ghost + use prelude.Ghost + use prelude.Ghost + predicate resolve0 (self : borrowed (Ghost.ghost_ty bool)) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve0 (self : borrowed (Ghost.ghost_ty bool)) : bool + ensures { result = resolve0 self } + + use prelude.Ghost + let rec cfg unsound [#"../869.rs" 4 0 4 16] [@cfg:stackify] [@cfg:subregion_analysis] (_1 : ()) : () + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : (); + var x : Ghost.ghost_ty bool; + var xm : borrowed (Ghost.ghost_ty bool); + var _4 : borrowed (Ghost.ghost_ty bool); + var b : borrowed (Ghost.ghost_ty bool); + var _6 : borrowed (Ghost.ghost_ty bool); + var bg : Ghost.ghost_ty (borrowed (Ghost.ghost_ty bool)); + var evil : borrowed (Ghost.ghost_ty bool); + var _12 : borrowed (Ghost.ghost_ty bool); + var _15 : Ghost.ghost_ty bool; + { + goto BB0 + } + BB0 { + [#"../869.rs" 5 29 5 41] x <- ([#"../869.rs" 5 29 5 41] Ghost.new true); + goto BB1 + } + BB1 { + [#"../869.rs" 7 31 7 37] _4 <- Borrow.borrow_mut x; + [#"../869.rs" 7 31 7 37] x <- ^ _4; + [#"../869.rs" 7 31 7 37] xm <- Borrow.borrow_final ( * _4) (Borrow.get_id _4); + [#"../869.rs" 7 31 7 37] _4 <- { _4 with current = ( ^ xm) ; }; + assume { resolve0 _4 }; + [#"../869.rs" 9 30 9 38] _6 <- Borrow.borrow_mut ( * xm); + [#"../869.rs" 9 30 9 38] xm <- { xm with current = ( ^ _6) ; }; + [#"../869.rs" 9 30 9 38] b <- Borrow.borrow_final ( * _6) (Borrow.get_id _6); + [#"../869.rs" 9 30 9 38] _6 <- { _6 with current = ( ^ b) ; }; + assume { resolve0 b }; + assume { resolve0 _6 }; + [#"../869.rs" 10 38 10 47] bg <- ([#"../869.rs" 10 38 10 47] Ghost.new b); + goto BB2 + } + BB2 { + assert { [@expl:assertion] [#"../869.rs" 11 20 11 50] Ghost.inner ( * Ghost.inner bg) = true /\ Ghost.inner ( ^ Ghost.inner bg) = true }; + [#"../869.rs" 13 33 13 41] _12 <- Borrow.borrow_final ( * xm) (Borrow.get_id xm); + [#"../869.rs" 13 33 13 41] xm <- { xm with current = ( ^ _12) ; }; + [#"../869.rs" 13 33 13 41] evil <- Borrow.borrow_final ( * _12) (Borrow.get_id _12); + [#"../869.rs" 13 33 13 41] _12 <- { _12 with current = ( ^ evil) ; }; + assume { resolve0 _12 }; + assert { [@expl:assertion] [#"../869.rs" 17 20 17 53] (evil = Ghost.inner bg) = (Ghost.inner ( ^ evil) = true) }; + [#"../869.rs" 18 12 18 58] _15 <- ([#"../869.rs" 18 12 18 58] Ghost.new (if evil = Ghost.inner bg then + false + else + true + )); + goto BB3 + } + BB3 { + [#"../869.rs" 18 4 18 58] evil <- { evil with current = ([#"../869.rs" 18 4 18 58] _15) ; }; + [#"../869.rs" 18 4 18 58] _15 <- any Ghost.ghost_ty bool; + assume { resolve0 evil }; + assume { resolve0 xm }; + assert { [@expl:assertion] [#"../869.rs" 19 20 19 37] Ghost.inner ( * evil) = (not Ghost.inner ( ^ evil)) }; + assert { [@expl:assertion] [#"../869.rs" 20 20 20 37] Ghost.inner ( * evil) = (not Ghost.inner ( * evil)) }; + [#"../869.rs" 4 17 21 1] _0 <- ([#"../869.rs" 4 17 21 1] ()); + return _0 + } + +end diff --git a/creusot/tests/should_fail/bug/869.rs b/creusot/tests/should_fail/bug/869.rs new file mode 100644 index 0000000000..333f9a7f61 --- /dev/null +++ b/creusot/tests/should_fail/bug/869.rs @@ -0,0 +1,21 @@ +extern crate creusot_contracts; +use creusot_contracts::*; + +pub fn unsound() { + let mut x: Ghost = gh! { true }; + // id(xm) = i1 + let xm: &mut Ghost = &mut x; + // Not final: id(b) = i2 + let b: &mut Ghost = &mut *xm; + let bg: Ghost<&mut Ghost> = gh! { b }; + proof_assert! { ***bg == true && *^*bg == true }; + // Final: id(evil) = i1 + let evil: &mut Ghost = &mut *xm; + // This proof_assert does not pass ! + // Indeed evil != *bg (because the id do not match), which causes the next line to put `true` inside `*evil`. + // And thus *^evil == true, disproving the assertion. + proof_assert! { (evil == *bg) == (*^evil == true) }; + *evil = gh! { if evil == *bg { false } else { true } }; + proof_assert! { **evil == !*^evil }; + proof_assert! { **evil == !**evil }; +} \ No newline at end of file diff --git a/creusot/tests/should_fail/bug/869/why3session.xml b/creusot/tests/should_fail/bug/869/why3session.xml new file mode 100644 index 0000000000..792fb12aa4 --- /dev/null +++ b/creusot/tests/should_fail/bug/869/why3session.xml @@ -0,0 +1,48 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/creusot/tests/should_fail/bug/869/why3shapes.gz b/creusot/tests/should_fail/bug/869/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..54a393a5e36e281af460e1920b05eecd0a501b00 GIT binary patch literal 790 zcmV+x1L^!9iwFP!00000|E*QYZrd;rz3VG{YpWAyxT-)7K>>rg^i=RzgOteBXkxc^ z7Jq)ZNl}!fNtc6d&CHuOZyss;eY-k-vp@WCb>|Pq?SA)hC06Z+#-7=e-T8a_<#6j$ z)Y=WRr}A{V&S46+Ly9i_%_csT)P{j|`@>;>?}vBS-|g3g2-}^#N)#1#@W=htohJ!h z=|yJFldqQyu~--)RUTP-T<)tn+$1AsHeyNQMis(V)TF}A6^X3KUFQ8=X5a1nAu^QD zSV^v&Plfhzp|QuKKiot!o0lOkkXA1Mvl&oVOL1MUCQsM6v?yXmkH9`4TkG$(SB13F z<-}-K$;OYRT^Us!i`*mj!Kc`gS~G53V!l`|EVrGKKc8#e08g%OGs3Rz)zLo(ONqyF zQ)AIuz-7sq+T1dWqk+xmg)W$cjfeJ-oq^jw0vjYt zX9+a(%RpD`G9aT_@qL{@G5f^*j7XCVU;<4_V!kSwL(X4C%yp_fRXx6W30%doERGd% z(ts!mVouZx9II($n=`oUw+H4yK1P7$W~6SG&#@jOG2OUWH|{0NUR`_@)YA3Q^z3=@QJP|SYm&Kau8pVq z(&o|S^lM@AZ86MD9#0lyk&+xPAT&_tfFU_Urazx`V?M3I{;;~;9rw4pp=m5qbb=G1 z+|Y@k^CFPG;}SUr#X7R0TvOHzD7{nzL8UmiC`CXuFdxvxYu-z>06f`9oJB{jJd<)cbC6R)s);rmU;K^W-^s>j$ U_4#xu{f`5G0ooIJ>M98U02$SS ([#"../../../../creusot-contracts/src/std/slice.rs" 19 4 19 50] inv5 (shallow_model1 self)) && ([#"../../../../creusot-contracts/src/std/slice.rs" 18 14 18 41] shallow_model1 self = Slice.id self) && ([#"../../../../creusot-contracts/src/std/slice.rs" 17 14 17 41] Seq.length (shallow_model1 self) <= UIntSize.to_int max0) + function index_logic1 [@inline:trivial] (self : slice t) (ix : int) : t = + [#"../../../../creusot-contracts/src/logic/ops.rs" 43 8 43 31] Seq.get (shallow_model1 self) ix + val index_logic1 [@inline:trivial] (self : slice t) (ix : int) : t + ensures { result = index_logic1 self ix } + + function shallow_model0 (self : borrowed (slice t)) : Seq.seq t = + [#"../../../../creusot-contracts/src/model.rs" 101 8 101 31] shallow_model1 ( * self) + val shallow_model0 (self : borrowed (slice t)) : Seq.seq t + ensures { result = shallow_model0 self } + + use seq.Seq + function to_mut_seq0 (self : borrowed (slice t)) : Seq.seq (borrowed t) + val to_mut_seq0 (self : borrowed (slice t)) : Seq.seq (borrowed t) + requires {[#"../../../../creusot-contracts/src/std/slice.rs" 82 23 82 27] inv2 self} + ensures { result = to_mut_seq0 self } + + axiom to_mut_seq0_spec : forall self : borrowed (slice t) . ([#"../../../../creusot-contracts/src/std/slice.rs" 82 23 82 27] inv2 self) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 82 4 82 43] inv3 (to_mut_seq0 self)) && ([#"../../../../creusot-contracts/src/std/slice.rs" 81 4 81 85] forall i : int . 0 <= i /\ i < Seq.length (to_mut_seq0 self) -> ^ Seq.get (to_mut_seq0 self) i = index_logic1 ( ^ self) i) && ([#"../../../../creusot-contracts/src/std/slice.rs" 80 4 80 82] forall i : int . 0 <= i /\ i < Seq.length (to_mut_seq0 self) -> * Seq.get (to_mut_seq0 self) i = index_logic1 ( * self) i) && ([#"../../../../creusot-contracts/src/std/slice.rs" 79 14 79 41] Seq.length (to_mut_seq0 self) = Seq.length (shallow_model0 self)) + predicate resolve1 (self : borrowed (slice t)) = + [#"../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve1 (self : borrowed (slice t)) : bool + ensures { result = resolve1 self } + + predicate resolve0 (self : borrowed t) = + [#"../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve0 (self : borrowed t) : bool + ensures { result = resolve0 self } + + let rec cfg indexing [#"../final_borrows.rs" 37 0 37 41] [@cfg:stackify] [@cfg:subregion_analysis] (x : borrowed (slice t)) : borrowed t + requires {[#"../final_borrows.rs" 35 11 35 24] Seq.length (shallow_model0 x) >= 1} + requires {[#"../final_borrows.rs" 37 19 37 20] inv2 x} + ensures { [#"../final_borrows.rs" 36 10 36 37] result = Seq.get (to_mut_seq0 x) 0 } + ensures { [#"../final_borrows.rs" 37 35 37 41] inv1 result } + + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : borrowed t; + var x : borrowed (slice t) = x; + var _2 : borrowed t; + var _5 : borrowed t; + var _6 : usize; + var _8 : bool; + { + goto BB0 + } + BB0 { + [#"../final_borrows.rs" 38 11 38 12] _6 <- ([#"../final_borrows.rs" 38 11 38 12] [#"../final_borrows.rs" 38 11 38 12] (0 : usize)); + [#"../final_borrows.rs" 38 9 38 13] _8 <- ([#"../final_borrows.rs" 38 9 38 13] _6 < ([#"../final_borrows.rs" 38 9 38 13] Slice.length ( * x))); + assert { [@expl:index in bounds] [#"../final_borrows.rs" 38 9 38 13] _8 }; + goto BB1 + } + BB1 { + [#"../final_borrows.rs" 38 4 38 13] _5 <- Borrow.borrow_mut (Slice.get ( * x) _6); + [#"../final_borrows.rs" 38 4 38 13] x <- { x with current = Slice.set ( * x) _6 ( ^ _5) ; }; + assume { inv0 ( ^ _5) }; + [#"../final_borrows.rs" 38 4 38 13] _2 <- Borrow.borrow_final ( * _5) (Borrow.get_id _5); + [#"../final_borrows.rs" 38 4 38 13] _5 <- { _5 with current = ( ^ _2) ; }; + assume { inv0 ( ^ _2) }; + [#"../final_borrows.rs" 38 4 38 13] _0 <- Borrow.borrow_final ( * _2) (Borrow.get_id _2); + [#"../final_borrows.rs" 38 4 38 13] _2 <- { _2 with current = ( ^ _0) ; }; + assume { inv0 ( ^ _0) }; + assert { [@expl:type invariant] inv1 _5 }; + assume { resolve0 _5 }; + assert { [@expl:type invariant] inv1 _2 }; + assume { resolve0 _2 }; + assert { [@expl:type invariant] inv2 x }; + assume { resolve1 x }; + return _0 + } + +end diff --git a/creusot/tests/should_fail/final_borrows.rs b/creusot/tests/should_fail/final_borrows.rs new file mode 100644 index 0000000000..e563342697 --- /dev/null +++ b/creusot/tests/should_fail/final_borrows.rs @@ -0,0 +1,39 @@ +extern crate creusot_contracts; +use creusot_contracts::*; + +// Since we reborrow `bor` after `b1`, its prophecy depends on `b2` and not `b1` +pub fn not_final_borrow(bor: &mut T) { + let b1 = &mut *bor; + proof_assert!(b1 == bor); + let _b2 = &mut *bor; +} + +pub fn store_changes_prophecy(bor: &mut T, x: T) { + let b1 = &mut *bor; + // The prophecy of `bor` changed here after the reborrow + *bor = x; + proof_assert!(b1 == bor); +} + +pub fn call_changes_prophecy(bor: &mut i32) { + fn inner() -> i32 { + 2 + } + let b1 = &mut *bor; + // The prophecy of `bor` changed here after the reborrow + *bor = inner(); + proof_assert!(b1 == bor); +} + +// When unnesting, we can't statically track the prophecy in the inner borrow +#[ensures(result == &mut (**x).0)] +pub fn unnesting_fails<'a: 'b, 'b, T>(x: &'a mut &'b mut (T, T)) -> &'b mut T { + &mut (**x).0 +} + +// Right now, we don't reason about the indices when tracking reborrows +#[requires(x@.len() >= 1)] +#[ensures(result == x.to_mut_seq()[0])] +pub fn indexing(x: &mut [T]) -> &mut T { + &mut x[0] +} diff --git a/creusot/tests/should_fail/final_borrows/why3session.xml b/creusot/tests/should_fail/final_borrows/why3session.xml new file mode 100644 index 0000000000..42ce63e43a --- /dev/null +++ b/creusot/tests/should_fail/final_borrows/why3session.xml @@ -0,0 +1,143 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/creusot/tests/should_fail/final_borrows/why3shapes.gz b/creusot/tests/should_fail/final_borrows/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..f162bf2718cdcc54d9ef352c5e91f642a8fe255c GIT binary patch literal 2168 zcmV-;2#5C{iwFP!00000|GigPj~lrWe%G(i+a~kGD&7k_z`($O0|a?m^rHomP1-_a zX)I~H+JB$o(XC^~$8O@lW2w7X{Hj>TSJdC`mWPl2DIJzy(*CgCZGT;=<=x*G$IpJf z{Q?7f=#OlGheeh7u-h;ETYu*Rl#ljCUv*`_`#p`neEPS4UzYQF>o-O0*JINxP<3qr zgT?WWr?jLOzhC?9apCvru-kk|tSY@NFa>JRTosl|er?slM;uj~%o;y&cT8BZF>k43c~p z)>gDT%ep!!h;d0$RT?{{5ER8jf5ur0c6(QS*_wkUh#jcw6wV=;vtmRH+%1E>E* zR)O$gF}z#m-F~^<9anYNs$unzoqF^sOXuLf8vE1N<9^qp+Rp>G0@h!rVknP;EOGr- z^v`H>F7Em|YcdM?rHgd*78g}h@NfYyJG|`hat^R8FzP12@@0VKAg1JsDY@8^E6x#T z1HZqG{NcFUr&avuw;$4B^|aqTeN6F>S7W^5uLk+;fP=a?je6np>@hD6^4a6d7+?|d zo0Il#8d%xK>OLf@=qH_uVqop0B^T^rK3Vje&C7!|!of55K;fQ=hOp5Pw#vJse<%Oj z^V233I#>yRf*0}={qZ6_i7W3fpS$Y&3Nb}-^?6yDg}$2LR9;VKwh*0*n(c{*W*%yy zmAGZb)x<$$tgB6k*b!NUoe>V4;PgVs<%6+`|06wnNQ18 zvvx`01E_=mw~PQ&gF)p4XrusgfSDFx<^|})0EHP~qK1M}dk}7$5b&0`NQusL?!&ne zRYxwJsLsHZ5rBQSJq9({Zc7(neN7uvCWe-rf0mERHEnp6Ax5Nflfs?~KGVYUcAE~z z_4dOm`}O9~TVI|DL7WMJ7ebgAgP$2goEbwBW4w9mH);Ff_|emKXS1P#`m`I<1}I|3 z-DG`-iq|Y>zUNy?f5GqYhDY;gsOTv0P zrcAzwhk9Cmz1Wka>8SsBJ(jGt zbzun=S^YL^|KK-=5gG;9BP*w^eQT!YnCFOV{YczVc$VG}yeWFwVbP z(_L*M7mDmv$7rFJ+Uc79cNfzMF2|F+98ajE+?wald&+0a~g=f82tjit;}VTST~&2ViDDrlwKcOWC6+neq(^Br6Pn751uYS*ut*iBsPY2yXOmd6(yT16pClfxy}Z(1r`{B94R`2!0A&tL1z(8a3|0S zaDq8*9XE~>o^o8CQH_x~gpg7gwLqaL-wcI-Xi#AEoKPim!u}QPfRYL}OQlhvRw+_m zgUyky?0U396>M}8{<;M%DJH{p&{3+Gb5@dEq&jBS5H~_;DC;YlbXxoAgSmXFUb#qDpi(t)Wio~v7CuuT37ymocRx#B8nA07ytmSVl>qN literal 0 HcmV?d00001 diff --git a/creusot/tests/should_succeed/bug/final_borrows.mlcfg b/creusot/tests/should_succeed/bug/final_borrows.mlcfg new file mode 100644 index 0000000000..9c48ff2c95 --- /dev/null +++ b/creusot/tests/should_succeed/bug/final_borrows.mlcfg @@ -0,0 +1,1505 @@ + +module FinalBorrows_ReborrowId + type t + use prelude.Borrow + predicate invariant1 (self : borrowed t) + val invariant1 (self : borrowed t) : bool + ensures { result = invariant1 self } + + predicate inv1 (_x : borrowed t) + val inv1 (_x : borrowed t) : bool + ensures { result = inv1 _x } + + axiom inv1 : forall x : borrowed t . inv1 x = true + predicate invariant0 (self : t) + val invariant0 (self : t) : bool + ensures { result = invariant0 self } + + predicate inv0 (_x : t) + val inv0 (_x : t) : bool + ensures { result = inv0 _x } + + axiom inv0 : forall x : t . inv0 x = true + predicate resolve0 (self : borrowed t) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve0 (self : borrowed t) : bool + ensures { result = resolve0 self } + + let rec cfg reborrow_id [#"../final_borrows.rs" 5 0 5 42] [@cfg:stackify] [@cfg:subregion_analysis] (r : borrowed t) : borrowed t + requires {[#"../final_borrows.rs" 5 22 5 23] inv1 r} + ensures { [#"../final_borrows.rs" 4 10 4 21] result = r } + ensures { [#"../final_borrows.rs" 5 36 5 42] inv1 result } + + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : borrowed t; + var r : borrowed t = r; + var _2 : borrowed t; + { + goto BB0 + } + BB0 { + [#"../final_borrows.rs" 6 4 6 5] _2 <- Borrow.borrow_final ( * r) (Borrow.get_id r); + [#"../final_borrows.rs" 6 4 6 5] r <- { r with current = ( ^ _2) ; }; + assume { inv0 ( ^ _2) }; + [#"../final_borrows.rs" 6 4 6 5] _0 <- Borrow.borrow_final ( * _2) (Borrow.get_id _2); + [#"../final_borrows.rs" 6 4 6 5] _2 <- { _2 with current = ( ^ _0) ; }; + assume { inv0 ( ^ _0) }; + assert { [@expl:type invariant] inv1 _2 }; + assume { resolve0 _2 }; + assert { [@expl:type invariant] inv1 r }; + assume { resolve0 r }; + return _0 + } + +end +module FinalBorrows_Select + type t + predicate invariant1 (self : t) + val invariant1 (self : t) : bool + ensures { result = invariant1 self } + + predicate inv1 (_x : t) + val inv1 (_x : t) : bool + ensures { result = inv1 _x } + + axiom inv1 : forall x : t . inv1 x = true + use prelude.Borrow + predicate invariant0 (self : borrowed t) + val invariant0 (self : borrowed t) : bool + ensures { result = invariant0 self } + + predicate inv0 (_x : borrowed t) + val inv0 (_x : borrowed t) : bool + ensures { result = inv0 _x } + + axiom inv0 : forall x : borrowed t . inv0 x = true + predicate resolve0 (self : borrowed t) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve0 (self : borrowed t) : bool + ensures { result = resolve0 self } + + let rec cfg select [#"../final_borrows.rs" 10 0 10 72] [@cfg:stackify] [@cfg:subregion_analysis] (b : bool) (r1 : borrowed t) (r2 : borrowed t) : borrowed t + requires {[#"../final_borrows.rs" 10 30 10 32] inv0 r1} + requires {[#"../final_borrows.rs" 10 45 10 47] inv0 r2} + ensures { [#"../final_borrows.rs" 9 0 9 55] if b then result = r1 else result = r2 } + ensures { [#"../final_borrows.rs" 10 63 10 72] inv0 result } + + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : borrowed t; + var b : bool = b; + var r1 : borrowed t = r1; + var r2 : borrowed t = r2; + var _4 : borrowed t; + var _6 : borrowed t; + var _8 : borrowed t; + { + goto BB0 + } + BB0 { + switch ([#"../final_borrows.rs" 11 7 11 8] b) + | False -> goto BB2 + | True -> goto BB1 + end + } + BB1 { + assert { [@expl:type invariant] inv0 r2 }; + assume { resolve0 r2 }; + [#"../final_borrows.rs" 12 8 12 10] _8 <- Borrow.borrow_final ( * r1) (Borrow.get_id r1); + [#"../final_borrows.rs" 12 8 12 10] r1 <- { r1 with current = ( ^ _8) ; }; + assume { inv1 ( ^ _8) }; + [#"../final_borrows.rs" 12 8 12 10] _6 <- Borrow.borrow_final ( * _8) (Borrow.get_id _8); + [#"../final_borrows.rs" 12 8 12 10] _8 <- { _8 with current = ( ^ _6) ; }; + assume { inv1 ( ^ _6) }; + assert { [@expl:type invariant] inv0 _8 }; + assume { resolve0 _8 }; + goto BB3 + } + BB2 { + assert { [@expl:type invariant] inv0 r1 }; + assume { resolve0 r1 }; + [#"../final_borrows.rs" 14 8 14 10] _6 <- Borrow.borrow_final ( * r2) (Borrow.get_id r2); + [#"../final_borrows.rs" 14 8 14 10] r2 <- { r2 with current = ( ^ _6) ; }; + assume { inv1 ( ^ _6) }; + goto BB3 + } + BB3 { + [#"../final_borrows.rs" 11 4 15 5] _4 <- Borrow.borrow_final ( * _6) (Borrow.get_id _6); + [#"../final_borrows.rs" 11 4 15 5] _6 <- { _6 with current = ( ^ _4) ; }; + assume { inv1 ( ^ _4) }; + [#"../final_borrows.rs" 11 4 15 5] _0 <- Borrow.borrow_final ( * _4) (Borrow.get_id _4); + [#"../final_borrows.rs" 11 4 15 5] _4 <- { _4 with current = ( ^ _0) ; }; + assume { inv1 ( ^ _0) }; + assert { [@expl:type invariant] inv0 _6 }; + assume { resolve0 _6 }; + assert { [@expl:type invariant] inv0 _4 }; + assume { resolve0 _4 }; + assert { [@expl:type invariant] inv0 r2 }; + assume { resolve0 r2 }; + assert { [@expl:type invariant] inv0 r1 }; + assume { resolve0 r1 }; + return _0 + } + +end +module FinalBorrows_ReborrowField + type t + use prelude.Borrow + predicate invariant2 (self : borrowed (t, t)) + val invariant2 (self : borrowed (t, t)) : bool + ensures { result = invariant2 self } + + predicate inv2 (_x : borrowed (t, t)) + val inv2 (_x : borrowed (t, t)) : bool + ensures { result = inv2 _x } + + axiom inv2 : forall x : borrowed (t, t) . inv2 x = true + predicate invariant1 (self : borrowed t) + val invariant1 (self : borrowed t) : bool + ensures { result = invariant1 self } + + predicate inv1 (_x : borrowed t) + val inv1 (_x : borrowed t) : bool + ensures { result = inv1 _x } + + axiom inv1 : forall x : borrowed t . inv1 x = true + predicate invariant0 (self : t) + val invariant0 (self : t) : bool + ensures { result = invariant0 self } + + predicate inv0 (_x : t) + val inv0 (_x : t) : bool + ensures { result = inv0 _x } + + axiom inv0 : forall x : t . inv0 x = true + predicate resolve1 (self : borrowed (t, t)) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve1 (self : borrowed (t, t)) : bool + ensures { result = resolve1 self } + + predicate resolve0 (self : borrowed t) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve0 (self : borrowed t) : bool + ensures { result = resolve0 self } + + let rec cfg reborrow_field [#"../final_borrows.rs" 19 0 19 50] [@cfg:stackify] [@cfg:subregion_analysis] (r : borrowed (t, t)) : borrowed t + requires {[#"../final_borrows.rs" 19 25 19 26] inv2 r} + ensures { [#"../final_borrows.rs" 18 10 18 28] result = Borrow.borrow_logic (let (a, _) = * r in a) (let (a, _) = ^ r in a) (Borrow.inherit_id (Borrow.get_id r) 1) } + ensures { [#"../final_borrows.rs" 19 44 19 50] inv1 result } + + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : borrowed t; + var r : borrowed (t, t) = r; + var _2 : borrowed t; + var _4 : borrowed t; + { + goto BB0 + } + BB0 { + [#"../final_borrows.rs" 20 4 20 12] _4 <- Borrow.borrow_final (let (a, _) = * r in a) (Borrow.inherit_id (Borrow.get_id r) 1); + [#"../final_borrows.rs" 20 4 20 12] r <- { r with current = (let (x0, x1) = * r in ( ^ _4, x1)) ; }; + assume { inv0 ( ^ _4) }; + [#"../final_borrows.rs" 20 4 20 12] _2 <- Borrow.borrow_final ( * _4) (Borrow.get_id _4); + [#"../final_borrows.rs" 20 4 20 12] _4 <- { _4 with current = ( ^ _2) ; }; + assume { inv0 ( ^ _2) }; + [#"../final_borrows.rs" 20 4 20 12] _0 <- Borrow.borrow_final ( * _2) (Borrow.get_id _2); + [#"../final_borrows.rs" 20 4 20 12] _2 <- { _2 with current = ( ^ _0) ; }; + assume { inv0 ( ^ _0) }; + assert { [@expl:type invariant] inv1 _4 }; + assume { resolve0 _4 }; + assert { [@expl:type invariant] inv1 _2 }; + assume { resolve0 _2 }; + assert { [@expl:type invariant] inv2 r }; + assume { resolve1 r }; + return _0 + } + +end +module FinalBorrows_NestedFields + type t + use prelude.Borrow + predicate invariant4 (self : borrowed ((t, t), t)) + val invariant4 (self : borrowed ((t, t), t)) : bool + ensures { result = invariant4 self } + + predicate inv4 (_x : borrowed ((t, t), t)) + val inv4 (_x : borrowed ((t, t), t)) : bool + ensures { result = inv4 _x } + + axiom inv4 : forall x : borrowed ((t, t), t) . inv4 x = true + predicate invariant3 (self : borrowed t) + val invariant3 (self : borrowed t) : bool + ensures { result = invariant3 self } + + predicate inv3 (_x : borrowed t) + val inv3 (_x : borrowed t) : bool + ensures { result = inv3 _x } + + axiom inv3 : forall x : borrowed t . inv3 x = true + predicate invariant2 (self : borrowed (t, t)) + val invariant2 (self : borrowed (t, t)) : bool + ensures { result = invariant2 self } + + predicate inv2 (_x : borrowed (t, t)) + val inv2 (_x : borrowed (t, t)) : bool + ensures { result = inv2 _x } + + axiom inv2 : forall x : borrowed (t, t) . inv2 x = true + predicate invariant1 (self : t) + val invariant1 (self : t) : bool + ensures { result = invariant1 self } + + predicate inv1 (_x : t) + val inv1 (_x : t) : bool + ensures { result = inv1 _x } + + axiom inv1 : forall x : t . inv1 x = true + predicate invariant0 (self : (t, t)) + val invariant0 (self : (t, t)) : bool + ensures { result = invariant0 self } + + predicate inv0 (_x : (t, t)) + val inv0 (_x : (t, t)) : bool + ensures { result = inv0 _x } + + axiom inv0 : forall x : (t, t) . inv0 x = true + predicate resolve2 (self : borrowed ((t, t), t)) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve2 (self : borrowed ((t, t), t)) : bool + ensures { result = resolve2 self } + + predicate resolve1 (self : borrowed t) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve1 (self : borrowed t) : bool + ensures { result = resolve1 self } + + predicate resolve0 (self : borrowed (t, t)) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve0 (self : borrowed (t, t)) : bool + ensures { result = resolve0 self } + + let rec cfg nested_fields [#"../final_borrows.rs" 24 0 24 54] [@cfg:stackify] [@cfg:subregion_analysis] (r : borrowed ((t, t), t)) : borrowed t + requires {[#"../final_borrows.rs" 24 24 24 25] inv4 r} + ensures { [#"../final_borrows.rs" 23 0 23 32] result = Borrow.borrow_logic (let (_, a) = let (a, _) = * r in a in a) (let (_, a) = let (a, _) = ^ r in a in a) (Borrow.inherit_id (Borrow.inherit_id (Borrow.get_id r) 1) 2) } + ensures { [#"../final_borrows.rs" 24 48 24 54] inv3 result } + + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : borrowed t; + var r : borrowed ((t, t), t) = r; + var _2 : borrowed t; + var borrow1 : borrowed (t, t); + var _5 : borrowed t; + { + goto BB0 + } + BB0 { + [#"../final_borrows.rs" 25 18 25 26] borrow1 <- Borrow.borrow_final (let (a, _) = * r in a) (Borrow.inherit_id (Borrow.get_id r) 1); + [#"../final_borrows.rs" 25 18 25 26] r <- { r with current = (let (x0, x1) = * r in ( ^ borrow1, x1)) ; }; + assume { inv0 ( ^ borrow1) }; + [#"../final_borrows.rs" 26 4 26 18] _5 <- Borrow.borrow_final (let (_, a) = * borrow1 in a) (Borrow.inherit_id (Borrow.get_id borrow1) 2); + [#"../final_borrows.rs" 26 4 26 18] borrow1 <- { borrow1 with current = (let (x0, x1) = * borrow1 in (x0, ^ _5)) ; }; + assume { inv1 ( ^ _5) }; + [#"../final_borrows.rs" 26 4 26 18] _2 <- Borrow.borrow_final ( * _5) (Borrow.get_id _5); + [#"../final_borrows.rs" 26 4 26 18] _5 <- { _5 with current = ( ^ _2) ; }; + assume { inv1 ( ^ _2) }; + assert { [@expl:type invariant] inv2 borrow1 }; + assume { resolve0 borrow1 }; + [#"../final_borrows.rs" 26 4 26 18] _0 <- Borrow.borrow_final ( * _2) (Borrow.get_id _2); + [#"../final_borrows.rs" 26 4 26 18] _2 <- { _2 with current = ( ^ _0) ; }; + assume { inv1 ( ^ _0) }; + assert { [@expl:type invariant] inv3 _5 }; + assume { resolve1 _5 }; + assert { [@expl:type invariant] inv3 _2 }; + assume { resolve1 _2 }; + assert { [@expl:type invariant] inv4 r }; + assume { resolve2 r }; + return _0 + } + +end +module FinalBorrows_ReallyNestedFields + type t + use prelude.Borrow + predicate invariant2 (self : (borrowed (t, t), t)) + val invariant2 (self : (borrowed (t, t), t)) : bool + ensures { result = invariant2 self } + + predicate inv2 (_x : (borrowed (t, t), t)) + val inv2 (_x : (borrowed (t, t), t)) : bool + ensures { result = inv2 _x } + + axiom inv2 : forall x : (borrowed (t, t), t) . inv2 x = true + predicate invariant1 (self : borrowed t) + val invariant1 (self : borrowed t) : bool + ensures { result = invariant1 self } + + predicate inv1 (_x : borrowed t) + val inv1 (_x : borrowed t) : bool + ensures { result = inv1 _x } + + axiom inv1 : forall x : borrowed t . inv1 x = true + predicate invariant0 (self : t) + val invariant0 (self : t) : bool + ensures { result = invariant0 self } + + predicate inv0 (_x : t) + val inv0 (_x : t) : bool + ensures { result = inv0 _x } + + axiom inv0 : forall x : t . inv0 x = true + predicate resolve3 (self : t) + val resolve3 (self : t) : bool + ensures { result = resolve3 self } + + predicate resolve2 (self : borrowed (t, t)) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve2 (self : borrowed (t, t)) : bool + ensures { result = resolve2 self } + + predicate resolve1 (self : (borrowed (t, t), t)) = + [#"../../../../../creusot-contracts/src/resolve.rs" 16 8 16 60] resolve2 (let (a, _) = self in a) /\ resolve3 (let (_, a) = self in a) + val resolve1 (self : (borrowed (t, t), t)) : bool + ensures { result = resolve1 self } + + predicate resolve0 (self : borrowed t) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve0 (self : borrowed t) : bool + ensures { result = resolve0 self } + + let rec cfg really_nested_fields [#"../final_borrows.rs" 30 0 30 61] [@cfg:stackify] [@cfg:subregion_analysis] (x : (borrowed (t, t), t)) : borrowed t + requires {[#"../final_borrows.rs" 30 31 30 32] inv2 x} + ensures { [#"../final_borrows.rs" 29 10 29 33] result = Borrow.borrow_logic (let (_, a) = * (let (a, _) = x in a) in a) (let (_, a) = ^ (let (a, _) = x in a) in a) (Borrow.inherit_id (Borrow.get_id (let (a, _) = x in a)) 2) } + ensures { [#"../final_borrows.rs" 30 55 30 61] inv1 result } + + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : borrowed t; + var x : (borrowed (t, t), t) = x; + var _2 : borrowed t; + var borrow : borrowed t; + { + goto BB0 + } + BB0 { + goto BB1 + } + BB1 { + [#"../final_borrows.rs" 31 17 31 30] borrow <- Borrow.borrow_final (let (_, a) = * (let (a, _) = x in a) in a) (Borrow.inherit_id (Borrow.get_id (let (a, _) = x in a)) 2); + [#"../final_borrows.rs" 31 17 31 30] x <- (let (x0, x1) = x in ({ (let (a, _) = x in a) with current = (let (x0, x1) = * (let (a, _) = x in a) in (x0, ^ borrow)) ; }, x1)); + assume { inv0 ( ^ borrow) }; + [#"../final_borrows.rs" 32 4 32 10] _2 <- Borrow.borrow_final ( * borrow) (Borrow.get_id borrow); + [#"../final_borrows.rs" 32 4 32 10] borrow <- { borrow with current = ( ^ _2) ; }; + assume { inv0 ( ^ _2) }; + assert { [@expl:type invariant] inv1 borrow }; + assume { resolve0 borrow }; + [#"../final_borrows.rs" 32 4 32 10] _0 <- Borrow.borrow_final ( * _2) (Borrow.get_id _2); + [#"../final_borrows.rs" 32 4 32 10] _2 <- { _2 with current = ( ^ _0) ; }; + assume { inv0 ( ^ _0) }; + assert { [@expl:type invariant] inv1 _2 }; + assume { resolve0 _2 }; + goto BB2 + } + BB2 { + assert { [@expl:type invariant] inv2 x }; + assume { resolve1 x }; + return _0 + } + +end +module Core_Option_Option_Type + type t_option 't = + | C_None + | C_Some 't + + let function some_0 (self : t_option 't) : 't = [@vc:do_not_keep_trace] [@vc:sp] + match self with + | C_None -> any 't + | C_Some a -> a + end +end +module FinalBorrows_SelectField + type t + use Core_Option_Option_Type as Core_Option_Option_Type + use prelude.Borrow + predicate invariant4 (self : borrowed (Core_Option_Option_Type.t_option t, t)) + val invariant4 (self : borrowed (Core_Option_Option_Type.t_option t, t)) : bool + ensures { result = invariant4 self } + + predicate inv4 (_x : borrowed (Core_Option_Option_Type.t_option t, t)) + val inv4 (_x : borrowed (Core_Option_Option_Type.t_option t, t)) : bool + ensures { result = inv4 _x } + + axiom inv4 : forall x : borrowed (Core_Option_Option_Type.t_option t, t) . inv4 x = true + predicate invariant3 (self : borrowed t) + val invariant3 (self : borrowed t) : bool + ensures { result = invariant3 self } + + predicate inv3 (_x : borrowed t) + val inv3 (_x : borrowed t) : bool + ensures { result = inv3 _x } + + axiom inv3 : forall x : borrowed t . inv3 x = true + predicate invariant2 (self : t) + val invariant2 (self : t) : bool + ensures { result = invariant2 self } + + predicate inv2 (_x : t) + val inv2 (_x : t) : bool + ensures { result = inv2 _x } + + axiom inv2 : forall x : t . inv2 x = true + predicate invariant1 (self : borrowed (Core_Option_Option_Type.t_option t)) + val invariant1 (self : borrowed (Core_Option_Option_Type.t_option t)) : bool + ensures { result = invariant1 self } + + predicate inv1 (_x : borrowed (Core_Option_Option_Type.t_option t)) + val inv1 (_x : borrowed (Core_Option_Option_Type.t_option t)) : bool + ensures { result = inv1 _x } + + axiom inv1 : forall x : borrowed (Core_Option_Option_Type.t_option t) . inv1 x = true + predicate invariant0 (self : Core_Option_Option_Type.t_option t) + val invariant0 (self : Core_Option_Option_Type.t_option t) : bool + ensures { result = invariant0 self } + + predicate inv0 (_x : Core_Option_Option_Type.t_option t) + val inv0 (_x : Core_Option_Option_Type.t_option t) : bool + ensures { result = inv0 _x } + + axiom inv0 : forall x : Core_Option_Option_Type.t_option t . inv0 x = true + predicate resolve2 (self : borrowed (Core_Option_Option_Type.t_option t, t)) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve2 (self : borrowed (Core_Option_Option_Type.t_option t, t)) : bool + ensures { result = resolve2 self } + + predicate resolve1 (self : borrowed t) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve1 (self : borrowed t) : bool + ensures { result = resolve1 self } + + predicate resolve0 (self : borrowed (Core_Option_Option_Type.t_option t)) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve0 (self : borrowed (Core_Option_Option_Type.t_option t)) : bool + ensures { result = resolve0 self } + + let rec cfg select_field [#"../final_borrows.rs" 39 0 39 56] [@cfg:stackify] [@cfg:subregion_analysis] (x : borrowed (Core_Option_Option_Type.t_option t, t)) : borrowed t + requires {[#"../final_borrows.rs" 39 23 39 24] inv4 x} + ensures { [#"../final_borrows.rs" 35 10 38 1] match let (a, _) = * x in a with + | Core_Option_Option_Type.C_None -> result = Borrow.borrow_logic (let (_, a) = * x in a) (let (_, a) = ^ x in a) (Borrow.inherit_id (Borrow.get_id x) 2) + | Core_Option_Option_Type.C_Some _ -> exists r : borrowed t . inv3 r /\ result = r /\ (let (a, _) = * x in a) = Core_Option_Option_Type.C_Some ( * r) /\ (let (a, _) = ^ x in a) = Core_Option_Option_Type.C_Some ( ^ r) + end } + ensures { [#"../final_borrows.rs" 39 50 39 56] inv3 result } + + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : borrowed t; + var x : borrowed (Core_Option_Option_Type.t_option t, t) = x; + var _4 : borrowed (Core_Option_Option_Type.t_option t); + var r : borrowed t; + var _8 : borrowed t; + { + goto BB0 + } + BB0 { + [#"../final_borrows.rs" 40 10 40 18] _4 <- Borrow.borrow_final (let (a, _) = * x in a) (Borrow.inherit_id (Borrow.get_id x) 1); + [#"../final_borrows.rs" 40 10 40 18] x <- { x with current = (let (x0, x1) = * x in ( ^ _4, x1)) ; }; + assume { inv0 ( ^ _4) }; + switch ( * _4) + | Core_Option_Option_Type.C_None -> goto BB1 + | Core_Option_Option_Type.C_Some _ -> goto BB2 + end + } + BB1 { + goto BB4 + } + BB2 { + [#"../final_borrows.rs" 42 13 42 14] r <- Borrow.borrow_final (Core_Option_Option_Type.some_0 ( * _4)) (Borrow.inherit_id (Borrow.get_id _4) 1); + [#"../final_borrows.rs" 42 13 42 14] _4 <- { _4 with current = (let Core_Option_Option_Type.C_Some x0 = * _4 in Core_Option_Option_Type.C_Some ( ^ r)) ; }; + assume { inv2 ( ^ r) }; + [#"../final_borrows.rs" 42 26 42 27] _0 <- Borrow.borrow_final ( * r) (Borrow.get_id r); + [#"../final_borrows.rs" 42 26 42 27] r <- { r with current = ( ^ _0) ; }; + assume { inv2 ( ^ _0) }; + assert { [@expl:type invariant] inv3 r }; + assume { resolve1 r }; + assert { [@expl:type invariant] inv1 _4 }; + assume { resolve0 _4 }; + goto BB5 + } + BB3 { + assert { [@expl:type invariant] inv1 _4 }; + assume { resolve0 _4 }; + assert { [@expl:type invariant] inv4 x }; + assume { resolve2 x }; + assert { [#"../final_borrows.rs" 40 10 40 18] false }; + absurd + } + BB4 { + assert { [@expl:type invariant] inv1 _4 }; + assume { resolve0 _4 }; + [#"../final_borrows.rs" 44 4 44 12] _8 <- Borrow.borrow_final (let (_, a) = * x in a) (Borrow.inherit_id (Borrow.get_id x) 2); + [#"../final_borrows.rs" 44 4 44 12] x <- { x with current = (let (x0, x1) = * x in (x0, ^ _8)) ; }; + assume { inv2 ( ^ _8) }; + [#"../final_borrows.rs" 44 4 44 12] _0 <- Borrow.borrow_final ( * _8) (Borrow.get_id _8); + [#"../final_borrows.rs" 44 4 44 12] _8 <- { _8 with current = ( ^ _0) ; }; + assume { inv2 ( ^ _0) }; + assert { [@expl:type invariant] inv3 _8 }; + assume { resolve1 _8 }; + goto BB5 + } + BB5 { + assert { [@expl:type invariant] inv4 x }; + assume { resolve2 x }; + return _0 + } + +end +module FinalBorrows_Set7 + use prelude.Int32 + use prelude.Borrow + use prelude.Int32 + predicate resolve0 (self : borrowed int32) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve0 (self : borrowed int32) : bool + ensures { result = resolve0 self } + + use prelude.Int + let rec cfg set_7 [#"../final_borrows.rs" 48 0 48 21] [@cfg:stackify] [@cfg:subregion_analysis] (r : borrowed int32) : () + ensures { [#"../final_borrows.rs" 47 10 47 20] Int32.to_int ( ^ r) = 7 } + + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : (); + var r : borrowed int32 = r; + { + goto BB0 + } + BB0 { + [#"../final_borrows.rs" 49 4 49 10] r <- { r with current = ([#"../final_borrows.rs" 49 4 49 10] [#"../final_borrows.rs" 49 9 49 10] (7 : int32)) ; }; + assume { resolve0 r }; + [#"../final_borrows.rs" 48 22 50 1] _0 <- ([#"../final_borrows.rs" 48 22 50 1] ()); + return _0 + } + +end +module FinalBorrows_NotFinalBorrowWorks + use prelude.Int32 + use prelude.Borrow + use prelude.Int32 + predicate resolve0 (self : borrowed int32) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve0 (self : borrowed int32) : bool + ensures { result = resolve0 self } + + use prelude.Int + val set_70 [#"../final_borrows.rs" 48 0 48 21] (r : borrowed int32) : () + ensures { [#"../final_borrows.rs" 47 10 47 20] Int32.to_int ( ^ r) = 7 } + + let rec cfg not_final_borrow_works [#"../final_borrows.rs" 53 0 53 38] [@cfg:stackify] [@cfg:subregion_analysis] (_1 : ()) : int32 + ensures { [#"../final_borrows.rs" 52 10 52 22] Int32.to_int result = 9 } + + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : int32; + var x : int32; + var r : borrowed int32; + var r1 : borrowed int32; + var _6 : (); + var _7 : borrowed int32; + var y : int32; + { + goto BB0 + } + BB0 { + [#"../final_borrows.rs" 54 16 54 20] x <- ([#"../final_borrows.rs" 54 16 54 20] [#"../final_borrows.rs" 54 16 54 20] (1 : int32)); + [#"../final_borrows.rs" 55 12 55 18] r <- Borrow.borrow_mut x; + [#"../final_borrows.rs" 55 12 55 18] x <- ^ r; + [#"../final_borrows.rs" 56 13 56 20] r1 <- Borrow.borrow_final ( * r) (Borrow.get_id r); + [#"../final_borrows.rs" 56 13 56 20] r <- { r with current = ( ^ r1) ; }; + [#"../final_borrows.rs" 57 10 57 12] _7 <- Borrow.borrow_final ( * r1) (Borrow.get_id r1); + [#"../final_borrows.rs" 57 10 57 12] r1 <- { r1 with current = ( ^ _7) ; }; + [#"../final_borrows.rs" 57 4 57 13] _6 <- ([#"../final_borrows.rs" 57 4 57 13] set_70 _7); + _7 <- any borrowed int32; + goto BB1 + } + BB1 { + assume { resolve0 r1 }; + [#"../final_borrows.rs" 58 12 58 14] y <- ([#"../final_borrows.rs" 58 12 58 14] * r); + [#"../final_borrows.rs" 59 4 59 10] r <- { r with current = ([#"../final_borrows.rs" 59 4 59 10] [#"../final_borrows.rs" 59 9 59 10] (2 : int32)) ; }; + assume { resolve0 r }; + [#"../final_borrows.rs" 60 11 60 16] _0 <- ([#"../final_borrows.rs" 60 11 60 16] ([#"../final_borrows.rs" 60 11 60 12] x) + ([#"../final_borrows.rs" 60 15 60 16] y)); + return _0 + } + +end +module FinalBorrows_Branching + use prelude.Int32 + use prelude.Borrow + use prelude.Int32 + predicate resolve0 (self : borrowed int32) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve0 (self : borrowed int32) : bool + ensures { result = resolve0 self } + + use prelude.Int + let rec cfg branching [#"../final_borrows.rs" 64 0 64 32] [@cfg:stackify] [@cfg:subregion_analysis] (b : bool) : int32 + ensures { [#"../final_borrows.rs" 63 10 63 22] Int32.to_int result = 3 } + + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : int32; + var b : bool = b; + var x : int32; + var y : int32; + var r1 : borrowed int32; + var r2 : borrowed int32; + var _8 : (); + var _10 : borrowed int32; + var _11 : borrowed int32; + var r21 : borrowed int32; + { + goto BB0 + } + BB0 { + [#"../final_borrows.rs" 65 16 65 17] x <- ([#"../final_borrows.rs" 65 16 65 17] [#"../final_borrows.rs" 65 16 65 17] (3 : int32)); + [#"../final_borrows.rs" 67 17 67 23] r1 <- Borrow.borrow_mut x; + [#"../final_borrows.rs" 67 17 67 23] x <- ^ r1; + [#"../final_borrows.rs" 69 13 69 21] r2 <- Borrow.borrow_mut ( * r1); + [#"../final_borrows.rs" 69 13 69 21] r1 <- { r1 with current = ( ^ r2) ; }; + assume { resolve0 r2 }; + [#"../final_borrows.rs" 70 4 70 11] y <- ([#"../final_borrows.rs" 70 8 70 11] * r2); + switch ([#"../final_borrows.rs" 71 7 71 8] b) + | False -> goto BB2 + | True -> goto BB1 + end + } + BB1 { + assume { resolve0 r1 }; + [#"../final_borrows.rs" 73 13 73 19] _11 <- Borrow.borrow_mut y; + [#"../final_borrows.rs" 73 13 73 19] y <- ^ _11; + [#"../final_borrows.rs" 73 13 73 19] _10 <- Borrow.borrow_final ( * _11) (Borrow.get_id _11); + [#"../final_borrows.rs" 73 13 73 19] _11 <- { _11 with current = ( ^ _10) ; }; + [#"../final_borrows.rs" 73 8 73 19] r1 <- ([#"../final_borrows.rs" 73 8 73 19] _10); + [#"../final_borrows.rs" 73 8 73 19] _10 <- any borrowed int32; + assume { resolve0 _11 }; + assume { resolve0 r1 }; + [#"../final_borrows.rs" 74 8 74 15] y <- ([#"../final_borrows.rs" 74 12 74 15] * r1); + [#"../final_borrows.rs" 71 9 75 5] _8 <- ([#"../final_borrows.rs" 71 9 75 5] ()); + goto BB3 + } + BB2 { + [#"../final_borrows.rs" 77 17 77 25] r21 <- Borrow.borrow_final ( * r1) (Borrow.get_id r1); + [#"../final_borrows.rs" 77 17 77 25] r1 <- { r1 with current = ( ^ r21) ; }; + assume { resolve0 r21 }; + [#"../final_borrows.rs" 78 8 78 15] y <- ([#"../final_borrows.rs" 78 12 78 15] * r21); + assume { resolve0 r1 }; + [#"../final_borrows.rs" 75 11 79 5] _8 <- ([#"../final_borrows.rs" 75 11 79 5] ()); + goto BB3 + } + BB3 { + [#"../final_borrows.rs" 80 4 80 5] _0 <- ([#"../final_borrows.rs" 80 4 80 5] y); + return _0 + } + +end +module FinalBorrows_UnnestingNonExtensional + type t + use prelude.Borrow + predicate invariant2 (self : borrowed (borrowed t)) + val invariant2 (self : borrowed (borrowed t)) : bool + ensures { result = invariant2 self } + + predicate inv2 (_x : borrowed (borrowed t)) + val inv2 (_x : borrowed (borrowed t)) : bool + ensures { result = inv2 _x } + + axiom inv2 : forall x : borrowed (borrowed t) . inv2 x = true + predicate invariant1 (self : borrowed t) + val invariant1 (self : borrowed t) : bool + ensures { result = invariant1 self } + + predicate inv1 (_x : borrowed t) + val inv1 (_x : borrowed t) : bool + ensures { result = inv1 _x } + + axiom inv1 : forall x : borrowed t . inv1 x = true + predicate invariant0 (self : t) + val invariant0 (self : t) : bool + ensures { result = invariant0 self } + + predicate inv0 (_x : t) + val inv0 (_x : t) : bool + ensures { result = inv0 _x } + + axiom inv0 : forall x : t . inv0 x = true + predicate resolve1 (self : borrowed (borrowed t)) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve1 (self : borrowed (borrowed t)) : bool + ensures { result = resolve1 self } + + predicate resolve0 (self : borrowed t) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve0 (self : borrowed t) : bool + ensures { result = resolve0 self } + + let rec cfg unnesting_non_extensional [#"../final_borrows.rs" 85 0 85 82] [@cfg:stackify] [@cfg:subregion_analysis] (x : borrowed (borrowed t)) : borrowed t + requires {[#"../final_borrows.rs" 85 48 85 49] inv2 x} + ensures { [#"../final_borrows.rs" 83 10 83 24] * result = * * x } + ensures { [#"../final_borrows.rs" 84 10 84 24] ^ result = * ^ x } + ensures { [#"../final_borrows.rs" 85 73 85 82] inv1 result } + + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : borrowed t; + var x : borrowed (borrowed t) = x; + var _2 : borrowed t; + var _5 : borrowed t; + { + goto BB0 + } + BB0 { + [#"../final_borrows.rs" 86 4 86 12] _5 <- Borrow.borrow_mut ( * * x); + [#"../final_borrows.rs" 86 4 86 12] x <- { x with current = { ( * x) with current = ( ^ _5) ; } ; }; + assume { inv0 ( ^ _5) }; + [#"../final_borrows.rs" 86 4 86 12] _2 <- Borrow.borrow_final ( * _5) (Borrow.get_id _5); + [#"../final_borrows.rs" 86 4 86 12] _5 <- { _5 with current = ( ^ _2) ; }; + assume { inv0 ( ^ _2) }; + [#"../final_borrows.rs" 86 4 86 12] _0 <- Borrow.borrow_final ( * _2) (Borrow.get_id _2); + [#"../final_borrows.rs" 86 4 86 12] _2 <- { _2 with current = ( ^ _0) ; }; + assume { inv0 ( ^ _0) }; + assert { [@expl:type invariant] inv1 _5 }; + assume { resolve0 _5 }; + assert { [@expl:type invariant] inv1 _2 }; + assume { resolve0 _2 }; + assert { [@expl:type invariant] inv2 x }; + assume { resolve1 x }; + return _0 + } + +end +module Core_Ptr_NonNull_NonNull_Type + use prelude.Opaque + type t_nonnull 't = + | C_NonNull opaque_ptr + +end +module Core_Marker_PhantomData_Type + type t_phantomdata 't = + | C_PhantomData + +end +module Core_Ptr_Unique_Unique_Type + use Core_Marker_PhantomData_Type as Core_Marker_PhantomData_Type + use Core_Ptr_NonNull_NonNull_Type as Core_Ptr_NonNull_NonNull_Type + type t_unique 't = + | C_Unique (Core_Ptr_NonNull_NonNull_Type.t_nonnull 't) (Core_Marker_PhantomData_Type.t_phantomdata 't) + +end +module Alloc_Boxed_Box_Type + use Core_Ptr_Unique_Unique_Type as Core_Ptr_Unique_Unique_Type + type t_box 't 'a = + | C_Box (Core_Ptr_Unique_Unique_Type.t_unique 't) 'a + +end +module Alloc_Alloc_Global_Type + type t_global = + | C_Global + +end +module FinalBorrows_BoxDeref + type t + predicate invariant1 (self : t) + val invariant1 (self : t) : bool + ensures { result = invariant1 self } + + predicate inv1 (_x : t) + val inv1 (_x : t) : bool + ensures { result = inv1 _x } + + axiom inv1 : forall x : t . inv1 x = true + predicate invariant0 (self : t) + val invariant0 (self : t) : bool + ensures { result = invariant0 self } + + predicate inv0 (_x : t) + val inv0 (_x : t) : bool + ensures { result = inv0 _x } + + use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type + axiom inv0 : forall x : t . inv0 x = true + predicate resolve1 (self : t) + val resolve1 (self : t) : bool + ensures { result = resolve1 self } + + predicate resolve0 (self : t) = + [#"../../../../../creusot-contracts/src/resolve.rs" 34 8 34 31] resolve1 self + val resolve0 (self : t) : bool + ensures { result = resolve0 self } + + let rec cfg box_deref [#"../final_borrows.rs" 94 0 94 35] [@cfg:stackify] [@cfg:subregion_analysis] (x : t) : t + requires {[#"../final_borrows.rs" 94 20 94 21] inv0 x} + ensures { [#"../final_borrows.rs" 93 10 93 22] result = x } + ensures { [#"../final_borrows.rs" 94 34 94 35] inv1 result } + + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : t; + var x : t = x; + { + goto BB0 + } + BB0 { + goto BB1 + } + BB1 { + [#"../final_borrows.rs" 95 4 95 6] _0 <- ([#"../final_borrows.rs" 95 4 95 6] x); + [#"../final_borrows.rs" 95 4 95 6] x <- any t; + assert { [@expl:type invariant] inv0 x }; + assume { resolve0 x }; + goto BB2 + } + BB2 { + return _0 + } + +end +module FinalBorrows_BoxReborrowDirect + type t + predicate invariant2 (self : t) + val invariant2 (self : t) : bool + ensures { result = invariant2 self } + + predicate inv2 (_x : t) + val inv2 (_x : t) : bool + ensures { result = inv2 _x } + + use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type + axiom inv2 : forall x : t . inv2 x = true + use prelude.Borrow + predicate invariant1 (self : borrowed t) + val invariant1 (self : borrowed t) : bool + ensures { result = invariant1 self } + + predicate inv1 (_x : borrowed t) + val inv1 (_x : borrowed t) : bool + ensures { result = inv1 _x } + + axiom inv1 : forall x : borrowed t . inv1 x = true + predicate invariant0 (self : t) + val invariant0 (self : t) : bool + ensures { result = invariant0 self } + + predicate inv0 (_x : t) + val inv0 (_x : t) : bool + ensures { result = inv0 _x } + + axiom inv0 : forall x : t . inv0 x = true + predicate resolve2 (self : t) + val resolve2 (self : t) : bool + ensures { result = resolve2 self } + + predicate resolve1 (self : t) = + [#"../../../../../creusot-contracts/src/resolve.rs" 34 8 34 31] resolve2 self + val resolve1 (self : t) : bool + ensures { result = resolve1 self } + + predicate resolve0 (self : borrowed t) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve0 (self : borrowed t) : bool + ensures { result = resolve0 self } + + let rec cfg box_reborrow_direct [#"../final_borrows.rs" 99 0 99 44] [@cfg:stackify] [@cfg:subregion_analysis] (x : t) : () + requires {[#"../final_borrows.rs" 99 34 99 35] inv2 x} + ensures { [#"../final_borrows.rs" 98 10 98 14] true } + + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : (); + var x : t = x; + var borrow : borrowed t; + var _4 : borrowed t; + { + goto BB0 + } + BB0 { + [#"../final_borrows.rs" 100 25 100 32] _4 <- Borrow.borrow_mut x; + [#"../final_borrows.rs" 100 25 100 32] x <- ^ _4; + assume { inv0 ( ^ _4) }; + [#"../final_borrows.rs" 100 25 100 32] borrow <- Borrow.borrow_final ( * _4) (Borrow.get_id _4); + [#"../final_borrows.rs" 100 25 100 32] _4 <- { _4 with current = ( ^ borrow) ; }; + assume { inv0 ( ^ borrow) }; + assert { [@expl:type invariant] inv1 borrow }; + assume { resolve0 borrow }; + assert { [@expl:type invariant] inv1 _4 }; + assume { resolve0 _4 }; + assert { [@expl:type invariant] inv2 x }; + assume { resolve1 x }; + assert { [@expl:assertion] [#"../final_borrows.rs" 102 8 102 21] * borrow = x }; + goto BB1 + } + BB1 { + [#"../final_borrows.rs" 101 4 103 5] _0 <- ([#"../final_borrows.rs" 101 4 103 5] ()); + goto BB2 + } + BB2 { + return _0 + } + +end +module FinalBorrows_BoxReborrowIndirect + type t + use prelude.Borrow + predicate invariant2 (self : borrowed t) + val invariant2 (self : borrowed t) : bool + ensures { result = invariant2 self } + + predicate inv2 (_x : borrowed t) + val inv2 (_x : borrowed t) : bool + ensures { result = inv2 _x } + + axiom inv2 : forall x : borrowed t . inv2 x = true + predicate invariant1 (self : borrowed t) + val invariant1 (self : borrowed t) : bool + ensures { result = invariant1 self } + + predicate inv1 (_x : borrowed t) + val inv1 (_x : borrowed t) : bool + ensures { result = inv1 _x } + + axiom inv1 : forall x : borrowed t . inv1 x = true + predicate invariant0 (self : t) + val invariant0 (self : t) : bool + ensures { result = invariant0 self } + + predicate inv0 (_x : t) + val inv0 (_x : t) : bool + ensures { result = inv0 _x } + + axiom inv0 : forall x : t . inv0 x = true + predicate resolve1 (self : borrowed t) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve1 (self : borrowed t) : bool + ensures { result = resolve1 self } + + predicate resolve0 (self : borrowed t) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve0 (self : borrowed t) : bool + ensures { result = resolve0 self } + + let rec cfg box_reborrow_indirect [#"../final_borrows.rs" 107 0 107 58] [@cfg:stackify] [@cfg:subregion_analysis] (x : borrowed t) : t + requires {[#"../final_borrows.rs" 107 38 107 39] inv2 x} + ensures { [#"../final_borrows.rs" 106 10 106 25] result = * x } + ensures { [#"../final_borrows.rs" 107 57 107 58] inv0 result } + + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : t; + var x : borrowed t = x; + var borrow : borrowed t; + var _4 : borrowed t; + { + goto BB0 + } + BB0 { + [#"../final_borrows.rs" 108 25 108 33] _4 <- Borrow.borrow_mut ( * x); + [#"../final_borrows.rs" 108 25 108 33] x <- { x with current = ( ^ _4) ; }; + assume { inv0 ( ^ _4) }; + [#"../final_borrows.rs" 108 25 108 33] borrow <- Borrow.borrow_final ( * _4) (Borrow.get_id _4); + [#"../final_borrows.rs" 108 25 108 33] _4 <- { _4 with current = ( ^ borrow) ; }; + assume { inv0 ( ^ borrow) }; + assert { [@expl:type invariant] inv1 _4 }; + assume { resolve0 _4 }; + [#"../final_borrows.rs" 109 4 109 11] _0 <- ([#"../final_borrows.rs" 109 4 109 11] * borrow); + assert { [@expl:type invariant] inv1 borrow }; + assume { resolve0 borrow }; + assert { [@expl:type invariant] inv2 x }; + assume { resolve1 x }; + return _0 + } + +end +module FinalBorrows_BoxReborrowInStruct + use prelude.Int32 + use prelude.Borrow + use prelude.Int32 + use prelude.Int + predicate resolve1 (self : borrowed (int32, borrowed int32)) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve1 (self : borrowed (int32, borrowed int32)) : bool + ensures { result = resolve1 self } + + predicate resolve0 (self : borrowed int32) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve0 (self : borrowed int32) : bool + ensures { result = resolve0 self } + + let rec cfg box_reborrow_in_struct [#"../final_borrows.rs" 114 0 114 66] [@cfg:stackify] [@cfg:subregion_analysis] (x : borrowed (int32, borrowed int32)) : int32 + requires {[#"../final_borrows.rs" 112 11 112 29] Int32.to_int ( * (let (_, a) = * x in a)) = 3} + ensures { [#"../final_borrows.rs" 113 10 113 22] Int32.to_int result = 3 } + + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : int32; + var x : borrowed (int32, borrowed int32) = x; + var borrow : borrowed int32; + var _5 : borrowed int32; + { + goto BB0 + } + BB0 { + [#"../final_borrows.rs" 115 27 115 37] _5 <- Borrow.borrow_mut ( * (let (_, a) = * x in a)); + [#"../final_borrows.rs" 115 27 115 37] x <- { x with current = (let (x0, x1) = * x in (x0, { (let (_, a) = * x in a) with current = ( ^ _5) ; })) ; }; + [#"../final_borrows.rs" 115 27 115 37] borrow <- Borrow.borrow_final ( * _5) (Borrow.get_id _5); + [#"../final_borrows.rs" 115 27 115 37] _5 <- { _5 with current = ( ^ borrow) ; }; + assume { resolve0 _5 }; + [#"../final_borrows.rs" 116 4 116 11] _0 <- ([#"../final_borrows.rs" 116 4 116 11] * borrow); + assume { resolve0 borrow }; + assume { resolve1 x }; + return _0 + } + +end +module FinalBorrows_BorrowInBox + type t + use prelude.Borrow + predicate invariant2 (self : borrowed t) + val invariant2 (self : borrowed t) : bool + ensures { result = invariant2 self } + + predicate inv2 (_x : borrowed t) + val inv2 (_x : borrowed t) : bool + ensures { result = inv2 _x } + + use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type + axiom inv2 : forall x : borrowed t . inv2 x = true + predicate invariant1 (self : borrowed t) + val invariant1 (self : borrowed t) : bool + ensures { result = invariant1 self } + + predicate inv1 (_x : borrowed t) + val inv1 (_x : borrowed t) : bool + ensures { result = inv1 _x } + + axiom inv1 : forall x : borrowed t . inv1 x = true + predicate invariant0 (self : t) + val invariant0 (self : t) : bool + ensures { result = invariant0 self } + + predicate inv0 (_x : t) + val inv0 (_x : t) : bool + ensures { result = inv0 _x } + + axiom inv0 : forall x : t . inv0 x = true + predicate resolve0 (self : borrowed t) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve0 (self : borrowed t) : bool + ensures { result = resolve0 self } + + predicate resolve1 (self : borrowed t) = + [#"../../../../../creusot-contracts/src/resolve.rs" 34 8 34 31] resolve0 self + val resolve1 (self : borrowed t) : bool + ensures { result = resolve1 self } + + let rec cfg borrow_in_box [#"../final_borrows.rs" 120 0 120 49] [@cfg:stackify] [@cfg:subregion_analysis] (x : borrowed t) : borrowed t + requires {[#"../final_borrows.rs" 120 24 120 25] inv2 x} + ensures { [#"../final_borrows.rs" 119 10 119 22] result = x } + ensures { [#"../final_borrows.rs" 120 43 120 49] inv1 result } + + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : borrowed t; + var x : borrowed t = x; + var _2 : borrowed t; + var _4 : borrowed t; + { + goto BB0 + } + BB0 { + [#"../final_borrows.rs" 121 4 121 12] _4 <- Borrow.borrow_final ( * x) (Borrow.get_id x); + [#"../final_borrows.rs" 121 4 121 12] x <- { x with current = ( ^ _4) ; }; + assume { inv0 ( ^ _4) }; + [#"../final_borrows.rs" 121 4 121 12] _2 <- Borrow.borrow_final ( * _4) (Borrow.get_id _4); + [#"../final_borrows.rs" 121 4 121 12] _4 <- { _4 with current = ( ^ _2) ; }; + assume { inv0 ( ^ _2) }; + [#"../final_borrows.rs" 121 4 121 12] _0 <- Borrow.borrow_final ( * _2) (Borrow.get_id _2); + [#"../final_borrows.rs" 121 4 121 12] _2 <- { _2 with current = ( ^ _0) ; }; + assume { inv0 ( ^ _0) }; + assert { [@expl:type invariant] inv1 _4 }; + assume { resolve0 _4 }; + assert { [@expl:type invariant] inv1 _2 }; + assume { resolve0 _2 }; + goto BB1 + } + BB1 { + assert { [@expl:type invariant] inv2 x }; + assume { resolve1 x }; + return _0 + } + +end +module FinalBorrows_BorrowInBoxTuple1 + use prelude.Int32 + use prelude.Borrow + use prelude.Int32 + use prelude.Int + predicate resolve0 (self : borrowed int32) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve0 (self : borrowed int32) : bool + ensures { result = resolve0 self } + + predicate resolve3 (self : int32) = + [#"../../../../../creusot-contracts/src/resolve.rs" 45 8 45 12] true + val resolve3 (self : int32) : bool + ensures { result = resolve3 self } + + predicate resolve2 (self : (int32, borrowed int32)) = + [#"../../../../../creusot-contracts/src/resolve.rs" 16 8 16 60] resolve3 (let (a, _) = self in a) /\ resolve0 (let (_, a) = self in a) + val resolve2 (self : (int32, borrowed int32)) : bool + ensures { result = resolve2 self } + + predicate resolve1 (self : (int32, borrowed int32)) = + [#"../../../../../creusot-contracts/src/resolve.rs" 34 8 34 31] resolve2 self + val resolve1 (self : (int32, borrowed int32)) : bool + ensures { result = resolve1 self } + + let rec cfg borrow_in_box_tuple_1 [#"../final_borrows.rs" 126 0 126 60] [@cfg:stackify] [@cfg:subregion_analysis] (x : (int32, borrowed int32)) : int32 + requires {[#"../final_borrows.rs" 124 11 124 26] Int32.to_int ( * (let (_, a) = x in a)) = 2} + ensures { [#"../final_borrows.rs" 125 10 125 22] Int32.to_int result = 2 } + + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : int32; + var x : (int32, borrowed int32) = x; + var borrow : borrowed int32; + var _5 : borrowed int32; + { + goto BB0 + } + BB0 { + goto BB1 + } + BB1 { + [#"../final_borrows.rs" 127 27 127 39] _5 <- Borrow.borrow_final ( * (let (_, a) = x in a)) (Borrow.get_id (let (_, a) = x in a)); + [#"../final_borrows.rs" 127 27 127 39] x <- (let (x0, x1) = x in (x0, { (let (_, a) = x in a) with current = ( ^ _5) ; })); + [#"../final_borrows.rs" 127 27 127 39] borrow <- Borrow.borrow_final ( * _5) (Borrow.get_id _5); + [#"../final_borrows.rs" 127 27 127 39] _5 <- { _5 with current = ( ^ borrow) ; }; + assume { resolve0 _5 }; + [#"../final_borrows.rs" 128 4 128 11] _0 <- ([#"../final_borrows.rs" 128 4 128 11] * borrow); + assume { resolve0 borrow }; + assume { resolve1 x }; + goto BB2 + } + BB2 { + return _0 + } + +end +module FinalBorrows_BorrowInBoxTuple2 + use prelude.Int32 + use prelude.Borrow + use prelude.Int32 + use prelude.Int + predicate resolve0 (self : borrowed int32) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve0 (self : borrowed int32) : bool + ensures { result = resolve0 self } + + predicate resolve3 (self : borrowed int32) = + [#"../../../../../creusot-contracts/src/resolve.rs" 34 8 34 31] resolve0 self + val resolve3 (self : borrowed int32) : bool + ensures { result = resolve3 self } + + predicate resolve2 (self : int32) = + [#"../../../../../creusot-contracts/src/resolve.rs" 45 8 45 12] true + val resolve2 (self : int32) : bool + ensures { result = resolve2 self } + + predicate resolve1 (self : (int32, borrowed int32)) = + [#"../../../../../creusot-contracts/src/resolve.rs" 16 8 16 60] resolve2 (let (a, _) = self in a) /\ resolve3 (let (_, a) = self in a) + val resolve1 (self : (int32, borrowed int32)) : bool + ensures { result = resolve1 self } + + let rec cfg borrow_in_box_tuple_2 [#"../final_borrows.rs" 133 0 133 60] [@cfg:stackify] [@cfg:subregion_analysis] (x : (int32, borrowed int32)) : int32 + requires {[#"../final_borrows.rs" 131 11 131 26] Int32.to_int ( * (let (_, a) = x in a)) = 2} + ensures { [#"../final_borrows.rs" 132 10 132 22] Int32.to_int result = 2 } + + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : int32; + var x : (int32, borrowed int32) = x; + var borrow : borrowed int32; + var _5 : borrowed int32; + { + goto BB0 + } + BB0 { + goto BB1 + } + BB1 { + [#"../final_borrows.rs" 134 27 134 39] _5 <- Borrow.borrow_final ( * (let (_, a) = x in a)) (Borrow.get_id (let (_, a) = x in a)); + [#"../final_borrows.rs" 134 27 134 39] x <- (let (x0, x1) = x in (x0, { (let (_, a) = x in a) with current = ( ^ _5) ; })); + [#"../final_borrows.rs" 134 27 134 39] borrow <- Borrow.borrow_final ( * _5) (Borrow.get_id _5); + [#"../final_borrows.rs" 134 27 134 39] _5 <- { _5 with current = ( ^ borrow) ; }; + assume { resolve0 _5 }; + [#"../final_borrows.rs" 135 4 135 11] _0 <- ([#"../final_borrows.rs" 135 4 135 11] * borrow); + assume { resolve0 borrow }; + assume { resolve1 x }; + goto BB2 + } + BB2 { + return _0 + } + +end +module FinalBorrows_SharedBorrowNoGen + type t + use prelude.Borrow + predicate invariant2 (self : borrowed t) + val invariant2 (self : borrowed t) : bool + ensures { result = invariant2 self } + + predicate inv2 (_x : borrowed t) + val inv2 (_x : borrowed t) : bool + ensures { result = inv2 _x } + + axiom inv2 : forall x : borrowed t . inv2 x = true + predicate invariant1 (self : borrowed t) + val invariant1 (self : borrowed t) : bool + ensures { result = invariant1 self } + + predicate inv1 (_x : borrowed t) + val inv1 (_x : borrowed t) : bool + ensures { result = inv1 _x } + + axiom inv1 : forall x : borrowed t . inv1 x = true + predicate invariant0 (self : t) + val invariant0 (self : t) : bool + ensures { result = invariant0 self } + + predicate inv0 (_x : t) + val inv0 (_x : t) : bool + ensures { result = inv0 _x } + + axiom inv0 : forall x : t . inv0 x = true + predicate resolve1 (self : borrowed t) + val resolve1 (self : borrowed t) : bool + ensures { result = resolve1 self } + + predicate resolve0 (self : borrowed t) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve0 (self : borrowed t) : bool + ensures { result = resolve0 self } + + let rec cfg shared_borrow_no_gen [#"../final_borrows.rs" 149 0 149 43] [@cfg:stackify] [@cfg:subregion_analysis] (bor : borrowed t) : () + requires {[#"../final_borrows.rs" 149 31 149 34] inv1 bor} + + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : (); + var bor : borrowed t = bor; + var b1 : borrowed t; + var _shared : borrowed t; + { + goto BB0 + } + BB0 { + [#"../final_borrows.rs" 150 13 150 22] b1 <- Borrow.borrow_final ( * bor) (Borrow.get_id bor); + [#"../final_borrows.rs" 150 13 150 22] bor <- { bor with current = ( ^ b1) ; }; + assume { inv0 ( ^ b1) }; + assert { [@expl:type invariant] inv1 b1 }; + assume { resolve0 b1 }; + [#"../final_borrows.rs" 151 18 151 22] _shared <- ([#"../final_borrows.rs" 151 18 151 22] bor); + assert { [@expl:type invariant] inv2 _shared }; + assume { resolve1 _shared }; + assert { [@expl:type invariant] inv1 bor }; + assume { resolve0 bor }; + assert { [@expl:assertion] [#"../final_borrows.rs" 152 18 152 27] b1 = bor }; + [#"../final_borrows.rs" 149 44 153 1] _0 <- ([#"../final_borrows.rs" 149 44 153 1] ()); + return _0 + } + +end +module FinalBorrows_InspectNoGen + type t + use Core_Option_Option_Type as Core_Option_Option_Type + use prelude.Borrow + predicate invariant1 (self : borrowed (Core_Option_Option_Type.t_option t)) + val invariant1 (self : borrowed (Core_Option_Option_Type.t_option t)) : bool + ensures { result = invariant1 self } + + predicate inv1 (_x : borrowed (Core_Option_Option_Type.t_option t)) + val inv1 (_x : borrowed (Core_Option_Option_Type.t_option t)) : bool + ensures { result = inv1 _x } + + axiom inv1 : forall x : borrowed (Core_Option_Option_Type.t_option t) . inv1 x = true + predicate invariant0 (self : Core_Option_Option_Type.t_option t) + val invariant0 (self : Core_Option_Option_Type.t_option t) : bool + ensures { result = invariant0 self } + + predicate inv0 (_x : Core_Option_Option_Type.t_option t) + val inv0 (_x : Core_Option_Option_Type.t_option t) : bool + ensures { result = inv0 _x } + + axiom inv0 : forall x : Core_Option_Option_Type.t_option t . inv0 x = true + predicate resolve0 (self : borrowed (Core_Option_Option_Type.t_option t)) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve0 (self : borrowed (Core_Option_Option_Type.t_option t)) : bool + ensures { result = resolve0 self } + + let rec cfg inspect_no_gen [#"../final_borrows.rs" 155 0 155 43] [@cfg:stackify] [@cfg:subregion_analysis] (x : borrowed (Core_Option_Option_Type.t_option t)) : () + requires {[#"../final_borrows.rs" 155 25 155 26] inv1 x} + + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : (); + var x : borrowed (Core_Option_Option_Type.t_option t) = x; + var r : borrowed (Core_Option_Option_Type.t_option t); + var _4 : bool; + { + goto BB0 + } + BB0 { + [#"../final_borrows.rs" 156 12 156 19] r <- Borrow.borrow_final ( * x) (Borrow.get_id x); + [#"../final_borrows.rs" 156 12 156 19] x <- { x with current = ( ^ r) ; }; + assume { inv0 ( ^ r) }; + assert { [@expl:type invariant] inv1 r }; + assume { resolve0 r }; + assert { [@expl:type invariant] inv1 x }; + assume { resolve0 x }; + switch ( * x) + | Core_Option_Option_Type.C_Some _ -> goto BB2 + | _ -> goto BB1 + end + } + BB1 { + _4 <- false; + goto BB4 + } + BB2 { + goto BB3 + } + BB3 { + _4 <- true; + goto BB4 + } + BB4 { + switch (_4) + | False -> goto BB6 + | True -> goto BB5 + end + } + BB5 { + [#"../final_borrows.rs" 159 8 159 14] _0 <- ([#"../final_borrows.rs" 159 8 159 14] ()); + goto BB7 + } + BB6 { + assert { [@expl:assertion] [#"../final_borrows.rs" 161 18 161 24] r = x }; + [#"../final_borrows.rs" 155 44 162 1] _0 <- ([#"../final_borrows.rs" 155 44 162 1] ()); + goto BB7 + } + BB7 { + return _0 + } + +end +module FinalBorrows_PlaceMentionNoGen + type t + use Core_Option_Option_Type as Core_Option_Option_Type + use prelude.Borrow + predicate invariant1 (self : borrowed (Core_Option_Option_Type.t_option t)) + val invariant1 (self : borrowed (Core_Option_Option_Type.t_option t)) : bool + ensures { result = invariant1 self } + + predicate inv1 (_x : borrowed (Core_Option_Option_Type.t_option t)) + val inv1 (_x : borrowed (Core_Option_Option_Type.t_option t)) : bool + ensures { result = inv1 _x } + + axiom inv1 : forall x : borrowed (Core_Option_Option_Type.t_option t) . inv1 x = true + predicate invariant0 (self : Core_Option_Option_Type.t_option t) + val invariant0 (self : Core_Option_Option_Type.t_option t) : bool + ensures { result = invariant0 self } + + predicate inv0 (_x : Core_Option_Option_Type.t_option t) + val inv0 (_x : Core_Option_Option_Type.t_option t) : bool + ensures { result = inv0 _x } + + axiom inv0 : forall x : Core_Option_Option_Type.t_option t . inv0 x = true + predicate resolve0 (self : borrowed (Core_Option_Option_Type.t_option t)) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve0 (self : borrowed (Core_Option_Option_Type.t_option t)) : bool + ensures { result = resolve0 self } + + let rec cfg place_mention_no_gen [#"../final_borrows.rs" 164 0 164 49] [@cfg:stackify] [@cfg:subregion_analysis] (x : borrowed (Core_Option_Option_Type.t_option t)) : () + requires {[#"../final_borrows.rs" 164 31 164 32] inv1 x} + + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : (); + var x : borrowed (Core_Option_Option_Type.t_option t) = x; + var _r : borrowed (Core_Option_Option_Type.t_option t); + { + goto BB0 + } + BB0 { + [#"../final_borrows.rs" 165 13 165 20] _r <- Borrow.borrow_final ( * x) (Borrow.get_id x); + [#"../final_borrows.rs" 165 13 165 20] x <- { x with current = ( ^ _r) ; }; + assume { inv0 ( ^ _r) }; + assert { [@expl:type invariant] inv1 _r }; + assume { resolve0 _r }; + assert { [@expl:type invariant] inv1 x }; + assume { resolve0 x }; + assert { [@expl:assertion] [#"../final_borrows.rs" 167 18 167 25] _r = x }; + [#"../final_borrows.rs" 164 50 168 1] _0 <- ([#"../final_borrows.rs" 164 50 168 1] ()); + return _0 + } + +end +module FinalBorrows_ShallowBorrowNoGen + use prelude.Borrow + use prelude.Int32 + use prelude.Int + use Core_Option_Option_Type as Core_Option_Option_Type + predicate resolve0 (self : borrowed (Core_Option_Option_Type.t_option int32)) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve0 (self : borrowed (Core_Option_Option_Type.t_option int32)) : bool + ensures { result = resolve0 self } + + let rec cfg shallow_borrow_no_gen [#"../final_borrows.rs" 170 0 170 49] [@cfg:stackify] [@cfg:subregion_analysis] (x : borrowed (Core_Option_Option_Type.t_option int32)) : () + + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : (); + var x : borrowed (Core_Option_Option_Type.t_option int32) = x; + var _r : borrowed (Core_Option_Option_Type.t_option int32); + var inner : int32; + var inner1 : int32; + { + goto BB0 + } + BB0 { + [#"../final_borrows.rs" 171 13 171 20] _r <- Borrow.borrow_final ( * x) (Borrow.get_id x); + [#"../final_borrows.rs" 171 13 171 20] x <- { x with current = ( ^ _r) ; }; + assume { resolve0 _r }; + switch ( * x) + | Core_Option_Option_Type.C_Some _ -> goto BB2 + | _ -> goto BB7 + end + } + BB1 { + [#"../final_borrows.rs" 177 13 177 15] _0 <- ([#"../final_borrows.rs" 177 13 177 15] ()); + goto BB6 + } + BB2 { + goto BB3 + } + BB3 { + [#"../final_borrows.rs" 174 13 174 22] inner <- ([#"../final_borrows.rs" 174 13 174 22] Core_Option_Option_Type.some_0 ( * x)); + [#"../final_borrows.rs" 174 13 174 22] inner1 <- ([#"../final_borrows.rs" 174 13 174 22] inner); + switch ([#"../final_borrows.rs" 174 27 174 38] ([#"../final_borrows.rs" 174 27 174 33] inner1) = ([#"../final_borrows.rs" 174 37 174 38] [#"../final_borrows.rs" 174 37 174 38] (2 : int32))) + | False -> goto BB5 + | True -> goto BB4 + end + } + BB4 { + assume { resolve0 x }; + assert { [@expl:assertion] [#"../final_borrows.rs" 175 26 175 33] _r = x }; + [#"../final_borrows.rs" 174 42 176 9] _0 <- ([#"../final_borrows.rs" 174 42 176 9] ()); + goto BB6 + } + BB5 { + assume { resolve0 x }; + goto BB1 + } + BB6 { + return _0 + } + BB7 { + assume { resolve0 x }; + goto BB1 + } + BB8 { + assume { resolve0 x }; + goto BB1 + } + +end diff --git a/creusot/tests/should_succeed/bug/final_borrows.rs b/creusot/tests/should_succeed/bug/final_borrows.rs new file mode 100644 index 0000000000..a3246db288 --- /dev/null +++ b/creusot/tests/should_succeed/bug/final_borrows.rs @@ -0,0 +1,179 @@ +extern crate creusot_contracts; +use creusot_contracts::*; + +#[ensures(result == r)] +pub fn reborrow_id(r: &mut T) -> &mut T { + r +} + +#[ensures(if b { result == r1 } else { result == r2 })] +pub fn select<'a, T>(b: bool, r1: &'a mut T, r2: &'a mut T) -> &'a mut T { + if b { + r1 + } else { + r2 + } +} + +#[ensures(result == &mut r.0)] +pub fn reborrow_field(r: &mut (T, T)) -> &mut T { + &mut r.0 +} + +#[ensures(result == &mut r.0.1)] +pub fn nested_fields(r: &mut ((T, T), T)) -> &mut T { + let borrow1 = &mut r.0; + &mut borrow1.1 +} + +#[ensures(result == &mut (*x.0).1)] +pub fn really_nested_fields(x: (&mut (T, T), T)) -> &mut T { + let borrow = &mut (*x.0).1; + borrow +} + +#[ensures(match x.0 { + None => result == &mut x.1, + Some(_) => exists result == r && (*x).0 == Some(*r) && (^x).0 == Some(^r) +})] +pub fn select_field(x: &mut (Option, T)) -> &mut T { + match &mut x.0 { + None => {} + Some(r) => return r, + } + &mut x.1 +} + +#[ensures((^r)@ == 7)] +fn set_7(r: &mut i32) { + *r = 7; +} + +#[ensures(result@ == 9)] +pub fn not_final_borrow_works() -> i32 { + let mut x = 1i32; + let r = &mut x; + let r1 = &mut *r; + set_7(r1); + let y = *r; + *r = 2; + return x + y; +} + +#[ensures(result@ == 3)] +pub fn branching(b: bool) -> i32 { + let mut x = 3; + let mut y; + let mut r1 = &mut x; + // r2 is not a final reborrow + let r2 = &mut *r1; + y = *r2; + if b { + // kill r1 + r1 = &mut y; + y = *r1; + } else { + // gen r1 + let r2 = &mut *r1; + y = *r2; + } + y +} + +#[ensures(*result == **x)] +#[ensures(^result == *^x)] +pub fn unnesting_non_extensional<'a: 'b, 'b, T>(x: &'a mut &'b mut T) -> &'b mut T { + &mut **x +} + +//============================= +//=========== BOXES =========== +//============================= + +#[ensures(result == *x)] +pub fn box_deref(x: Box) -> T { + *x +} + +#[ensures(true)] +pub fn box_reborrow_direct(mut x: Box) { + let borrow: &mut T = &mut *x; + proof_assert! { + *borrow == *x + } +} + +#[ensures(result == (**x))] +pub fn box_reborrow_indirect(x: &mut Box) -> T { + let borrow: &mut T = &mut **x; + *borrow +} + +#[requires((**((*x).1))@ == 3)] +#[ensures(result@ == 3)] +pub fn box_reborrow_in_struct(x: &mut (i32, &mut Box)) -> i32 { + let borrow: &mut i32 = &mut **x.1; + *borrow +} + +#[ensures(result == *x)] +pub fn borrow_in_box(x: Box<&mut T>) -> &mut T { + &mut **x +} + +#[requires((*(*x).1)@ == 2)] +#[ensures(result@ == 2)] +pub fn borrow_in_box_tuple_1(x: Box<(i32, &mut i32)>) -> i32 { + let borrow: &mut i32 = &mut *(*x).1; + *borrow +} + +#[requires((*(*x.1))@ == 2)] +#[ensures(result@ == 2)] +pub fn borrow_in_box_tuple_2(x: (i32, Box<&mut i32>)) -> i32 { + let borrow: &mut i32 = &mut *(*x.1); + *borrow +} + +//========================================= +//=========== NON-MUTATING USES =========== +//========================================= + +// This checks that various mir non-mutating instructions preserve the final borrow property + +// Non-mutating uses not featured here: +// - 'Copy': cannot be emitted for a mutable borrow +// - 'Projection': cannot appear in the analysis +// - 'AddressOf': not supported by Creusot + +pub fn shared_borrow_no_gen(bor: &mut T) { + let b1 = &mut *bor; + let _shared = &bor; + proof_assert!(b1 == bor); +} + +pub fn inspect_no_gen(x: &mut Option) { + let r = &mut *x; + + if matches!(x, Some(_)) { + return; + } + proof_assert!(r == x); +} + +pub fn place_mention_no_gen(x: &mut Option) { + let _r = &mut *x; + let _ = x; + proof_assert!(_r == x); +} + +pub fn shallow_borrow_no_gen(x: &mut Option) { + let _r = &mut *x; + // x / *x is shallow borrowed here + match x { + Some(ref inner) if *inner == 2 => { + proof_assert!(_r == x); + } + _ => {} + } +} diff --git a/creusot/tests/should_succeed/bug/final_borrows/why3session.xml b/creusot/tests/should_succeed/bug/final_borrows/why3session.xml new file mode 100644 index 0000000000..bc6dc1e435 --- /dev/null +++ b/creusot/tests/should_succeed/bug/final_borrows/why3session.xml @@ -0,0 +1,116 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/creusot/tests/should_succeed/bug/final_borrows/why3shapes.gz b/creusot/tests/should_succeed/bug/final_borrows/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..024f5e0e696ca63262372a6cca160309fc077eb7 GIT binary patch literal 2800 zcmV)kiwFP!00000|K(Xrk0ZGazWZ1Bwn^tAQttqJFbo^jK#)rUAIGSNYQ|Wv zJ+VF8n|~kbRi!Fd_s(HA2#^7KT$W^tB0qklSbut1-@nvf-F^LwyWLOM%U{=O{qpD4 z<6rgZ@(Uc;K0UGn>{oG2Z|WZp`hc(X&E2o(UmQEg*El6N>9d$KY0jj%_?^|C4*Hb@ znYy{&Zr3;0{qXZoez5LOm->7V^{G3E{cG4u`Ad)?R^fRPH{X*Yg!lEQm_~mjY zQ6!1z1z?aU4m?ZbSt3S>oc?g1bjJPauwD1p+xq6BP+GZ4_Q1`FL;=zU;e*o$*8jYH zb5E9G$uewW8I|T#np4Fb@H7d0lOM`ymZw>sjw3(^2J~kHKC=U0GKBT#w!sjjHb6E7 zK(>XAwxEHRurLX>;U{b+*Cw&r%g{lrJ(w)iWSKh3H1tP{w%$>Pcs4IOfJ%Lcg$O$c zp7+{{85U@Oz_8nlR?4R1^}aseo!`MP9<6Ay@yt{acn_7J!q#e+l+jrkos|KVw9)=Q zzc72nPdtH>1V+g`fH7>Y4j^|~u*`yak}Ew(%TtPU2obPHnB8or#|~dm3~og3eS~7B z3i2E%EJO+mu0(!7%+5p{qJ>3uXyhd>&B9su70iXR$vLBFGQ1tYXXgjC{-FB;^dez? ze&E?KAA`_#HHz`=HjM_1K{m|seEocCx86tp{Py+i@bKnU+Irs( z1E2hfE??a3=4l-04g%l76Q(lbQT&Fm zj-f7y5(aAzv-ITDyB>QS%?3^5TKt?B28 zA0{}-hCX=9zlI2wc_+DS__(X2yfATF@&SLQ^#0_|UBZJHQNl-*phro@4j-{2Ja!^_ ze3*FjAkNT3aTe8hJJ1(d>Lh7Em9rCEO^)|`QrSW~=3or|3J35WO%DYIF&co>jI7AR z$T-dNG|SUtLP3m7Fpue+P{76rj!{j<8d3@lDFsqaK?t#3#x>~V8&9X{VN7N=QpFsG zIqQIk$shvJ5_Jzi98wSD3}Hf=7|ALHkX`_z533@SOvq&uIGUxXdiIlPF-I6h(|&Mw zl#pT~%7W#fFg}E$8ZzL1qJ|7rR7|`f121DG>flSM2?7&l9POMin#D zoEc4d9M6n)9C(izN6^AxYnI`QlcCM?&@*lz;|B6bpf9!H+9KZqj~dIM~1!mbEOnPk$1*fu>=^arAft1Y#Z|wTY{}As+IRRbW%_+ zx+qoGBh=mwBZp>r-1FZ+ruF&!@8c9bkx0~LThw+LIuqm&5l(=!#O$)gdVBo)^+I*r z*2l_(D!0dfTz_`n$i6VyddrnC&+{*Fo=ygt=YZ|f?AzA6Xc`>@z3LPxI+3e>-3IC( z8B}HBR0+19LI(5{KgB_YAjTUB?xIF0Q_Y7105LfNWhk|FgW#BJ7I}+kdV!it3)39Fx`3!(cT&FFXdT z1u909ti~Z7fe)z$O}fhYR1+3vtC=8q8aD%S(9DbcGCL z`c6MTvUn57C`+;io(i%2PCev_$xOI^H{t%J`@#qG50Y4EH-R|a7RC}rq)hB@&4E9~ zoIgc&g9x>yh_$7ld)2_7Vu0_o4o`I!EqYv!r^|z+u~xr6N>&a0R&Lp5E(>=Owl8Y? z$5D^MC~{jnBh<@-;}2mD>%SCVc{#=Q-WA8@`t8!)KUh|33D4QO#f7ps7rw(Uy@uoI zO{8?GBAiNNN=`$nw5Lez)*#(?_&!cp%Qul}HCm1bO~Qx_mo#Z#rJLZum(#zHba`*LwN)PuIX$D4Sa z4f)C6eRVk*+7j<|B@#2lo`l+st+6;JLsuj?Idl%l#Vy~Bq14>!OZ(+?`Meshnm@*d z(TlI*##$uS00VjFx;>Ze`niDxxq$_X4J^oc7>1VCAJxEOzuCYl0&b~+CC3Jq97Trm zd&-i_VHk;FTABSVS7bRbLmZ~Q$LzZL?c$3o^3w5gy&T=I4|nkm+xncm7J5f~p)EUU zKE|zLoaa6#EBc(x_19zPZmwTF(s7HnB&3!lrj{j6T9!6>)Fy}8?`i^@-;V-Ik0}4J zpP6>atp315C!jmse8XsLttJxZ-)Vw{Vj~yyaU|W)!l^mSZrSc)0cBYDY7Y$ zT7vTcEiPN&`0yt^!aJ6L|2s?ID!{4?IF%wQUwPHX^-w zay@=_m(?~{ExjXp#M)EF_j2LOa9#BSVNqzKKfPXq$yn}&iQ$49dR6mMZu(9(I#6w9 zFu)N8xZD4JRYh?jS|TAFNoe6k@ab~@>Myg&ia~Svv43YTuwXROf8oXT*K^&vJXWDCjvvMCH;-y?_#LO|w!CEeK+Q)=FBg5e zP+s}J)aNq+c#7i{=d8ho0rb6ALMcn^&~^rxl)?z9*Sx|CDz@sBQVrICJ)jY)#m*Y; z6hKqgqU-HiRw68HdLi4c6-)?FBvbSq=dJCaWvCm6YhabFOrbb1B<_37*^v)S( zt>vuktZSjsvR#9&Kvf_sAmO|M(gjw$0mKG7jjp${cb)2ZQ+GW>RXf|eHP{MF-a-SH z3=NQA&9wldr2^WBJ8MwD8lgfq-=c1fWNqufI940iD`7g8#XljkdykF3rdhLevg)LkAQ}^Immi3n3KibhGAAaTYv67H+jO zwbFEaCcJinoQ7RfOQ41r#U4+d>l8-jW* zRn490(U8JjCzMg(3^!{5m0)Cgu&7ZrOwf|vpww+c`;aZHGEK7^lbhYHdnwmfZYeBfp$6?$E`d5>+w9-B(nhtxeMBUkjFtirB5-Ql#lCz`}2tuIr z2N7LEkZfGt3CV!1g{_1MOEr*oh=PG24UzQa+BOso40?`?A_pqTR{sGt3JTy(Bme+{ CRc;9Y literal 0 HcmV?d00001