From 551a6ed6220f6da1ca792672234c0f35b34f4adc Mon Sep 17 00:00:00 2001 From: Xavier Denis Date: Sat, 18 May 2024 14:50:38 +0200 Subject: [PATCH] Update tests --- creusot/tests/should_fail/cycle.stderr | 2 +- creusot/tests/should_succeed/100doors.mlcfg | 4 +- creusot/tests/should_succeed/hillel.mlcfg | 14 +- .../should_succeed/iterators/01_range.mlcfg | 86 ++++---- .../iterators/01_range/why3session.xml | 8 +- .../iterators/01_range/why3shapes.gz | Bin 961 -> 961 bytes .../iterators/02_iter_mut.mlcfg | 114 +++++----- .../iterators/02_iter_mut/why3session.xml | 6 +- .../iterators/02_iter_mut/why3shapes.gz | Bin 3539 -> 3555 bytes .../iterators/03_std_iterators.mlcfg | 14 +- .../should_succeed/iterators/04_skip.mlcfg | 90 ++++---- .../iterators/04_skip/why3session.xml | 6 +- .../iterators/04_skip/why3shapes.gz | Bin 1067 -> 1069 bytes .../should_succeed/iterators/05_map.mlcfg | 186 ++++++++-------- .../iterators/05_map/why3session.xml | 6 +- .../iterators/05_map/why3shapes.gz | Bin 5478 -> 5484 bytes .../iterators/06_map_precond.mlcfg | 202 +++++++++--------- .../iterators/06_map_precond/why3session.xml | 8 +- .../iterators/06_map_precond/why3shapes.gz | Bin 8880 -> 8887 bytes .../should_succeed/iterators/07_fuse.mlcfg | 100 ++++----- .../iterators/07_fuse/why3session.xml | 6 +- .../iterators/07_fuse/why3shapes.gz | Bin 1320 -> 1322 bytes .../iterators/08_collect_extend.mlcfg | 8 +- .../should_succeed/iterators/09_empty.mlcfg | 58 ++--- .../iterators/09_empty/why3session.xml | 6 +- .../iterators/09_empty/why3shapes.gz | Bin 446 -> 449 bytes .../should_succeed/iterators/10_once.mlcfg | 66 +++--- .../iterators/10_once/why3session.xml | 6 +- .../iterators/10_once/why3shapes.gz | Bin 624 -> 628 bytes .../should_succeed/iterators/11_repeat.mlcfg | 86 ++++---- .../iterators/11_repeat/why3session.xml | 6 +- .../iterators/11_repeat/why3shapes.gz | Bin 494 -> 489 bytes .../should_succeed/iterators/12_zip.mlcfg | 4 +- .../should_succeed/iterators/13_cloned.mlcfg | 94 ++++---- .../iterators/13_cloned/why3session.xml | 4 +- .../iterators/13_cloned/why3shapes.gz | Bin 788 -> 792 bytes .../should_succeed/iterators/14_copied.mlcfg | 94 ++++---- .../iterators/14_copied/why3session.xml | 8 +- .../iterators/14_copied/why3shapes.gz | Bin 789 -> 791 bytes .../iterators/15_enumerate.mlcfg | 6 +- .../should_succeed/iterators/16_take.mlcfg | 114 +++++----- .../iterators/16_take/why3session.xml | 8 +- .../iterators/16_take/why3shapes.gz | Bin 944 -> 946 bytes .../tests/should_succeed/knapsack_full.mlcfg | 8 +- .../rusthorn/inc_max_repeat.mlcfg | 2 +- .../selection_sort_generic.mlcfg | 8 +- creusot/tests/should_succeed/sum.mlcfg | 4 +- .../tests/should_succeed/sum_of_odds.mlcfg | 4 +- creusot/tests/should_succeed/vector/01.mlcfg | 4 +- .../vector/03_knuth_shuffle.mlcfg | 4 +- .../vector/06_knights_tour.mlcfg | 16 +- .../should_succeed/vector/08_haystack.mlcfg | 8 +- 52 files changed, 739 insertions(+), 739 deletions(-) diff --git a/creusot/tests/should_fail/cycle.stderr b/creusot/tests/should_fail/cycle.stderr index 20c60aff7d..0b6cae6b1f 100644 --- a/creusot/tests/should_fail/cycle.stderr +++ b/creusot/tests/should_fail/cycle.stderr @@ -6,7 +6,7 @@ warning: unused import: `creusot_contracts::*` | = note: `#[warn(unused_imports)]` on by default -error: encountered a cycle during translation: [{Item(DefId(0:5 ~ cycle[f39e]::f))}, {Item(DefId(0:6 ~ cycle[f39e]::g))}, {Item(DefId(0:5 ~ cycle[f39e]::f))}] +error: encountered a cycle during translation: [{Item(DefId(0:5 ~ cycle[b375]::f))}, {Item(DefId(0:6 ~ cycle[b375]::g))}, {Item(DefId(0:5 ~ cycle[b375]::f))}] --> cycle.rs:4:1 | 4 | pub fn f() { diff --git a/creusot/tests/should_succeed/100doors.mlcfg b/creusot/tests/should_succeed/100doors.mlcfg index f5d6f08362..015a0bdeaf 100644 --- a/creusot/tests/should_succeed/100doors.mlcfg +++ b/creusot/tests/should_succeed/100doors.mlcfg @@ -470,14 +470,14 @@ module C100doors_F goto BB21 } BB12 { - [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _12; + [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _12; [#"../100doors.rs" 20 4 20 41] _17 <- ([#"../100doors.rs" 20 4 20 41] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem))); goto BB13 } BB13 { [#"../100doors.rs" 20 4 20 41] produced <- _17; _17 <- any Snapshot.snap_ty (Seq.seq usize); - [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] pass <- __creusot_proc_iter_elem; + [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] pass <- __creusot_proc_iter_elem; [#"../100doors.rs" 22 30 22 34] door <- pass; goto BB14 } diff --git a/creusot/tests/should_succeed/hillel.mlcfg b/creusot/tests/should_succeed/hillel.mlcfg index a56725f8b4..25476f66ec 100644 --- a/creusot/tests/should_succeed/hillel.mlcfg +++ b/creusot/tests/should_succeed/hillel.mlcfg @@ -1149,7 +1149,7 @@ module Hillel_InsertUnique goto BB24 } BB18 { - [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _28; + [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _28; assert { [@expl:type invariant] inv4 _28 }; assume { resolve6 _28 }; [#"../hillel.rs" 84 4 84 111] _33 <- ([#"../hillel.rs" 84 4 84 111] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem))); @@ -1160,7 +1160,7 @@ module Hillel_InsertUnique _33 <- any Snapshot.snap_ty (Seq.seq t); assert { [@expl:type invariant] inv2 produced }; assume { resolve4 produced }; - [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] e <- __creusot_proc_iter_elem; + [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] e <- __creusot_proc_iter_elem; assert { [@expl:type invariant] inv5 __creusot_proc_iter_elem }; assume { resolve7 __creusot_proc_iter_elem }; assert { [@expl:assertion] [#"../hillel.rs" 86 24 86 57] e @@ -1717,14 +1717,14 @@ module Hillel_Unique goto BB21 } BB16 { - [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _23; + [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _23; [#"../hillel.rs" 104 4 104 48] _28 <- ([#"../hillel.rs" 104 4 104 48] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem))); goto BB17 } BB17 { [#"../hillel.rs" 104 4 104 48] produced <- _28; _28 <- any Snapshot.snap_ty (Seq.seq usize); - [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] i <- __creusot_proc_iter_elem; + [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] i <- __creusot_proc_iter_elem; [#"../hillel.rs" 108 26 108 27] _32 <- i; [#"../hillel.rs" 108 22 108 28] _33 <- Slice.length str; [#"../hillel.rs" 108 22 108 28] _34 <- _32 < _33; @@ -2366,7 +2366,7 @@ module Hillel_Fulcrum goto BB12 } BB10 { - [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _19; + [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _19; [#"../hillel.rs" 159 4 159 60] _24 <- ([#"../hillel.rs" 159 4 159 60] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem))); goto BB11 } @@ -2438,14 +2438,14 @@ module Hillel_Fulcrum return _0 } BB22 { - [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem1 <- Core_Option_Option_Type.some_0 _50; + [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem1 <- Core_Option_Option_Type.some_0 _50; [#"../hillel.rs" 171 4 171 58] _55 <- ([#"../hillel.rs" 171 4 171 58] Snapshot.new (Seq.(++) (Snapshot.inner produced1) (Seq.singleton __creusot_proc_iter_elem1))); goto BB23 } BB23 { [#"../hillel.rs" 171 4 171 58] produced1 <- _55; _55 <- any Snapshot.snap_ty (Seq.seq usize); - [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] i <- __creusot_proc_iter_elem1; + [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] i <- __creusot_proc_iter_elem1; [#"../hillel.rs" 177 32 177 43] _60 <- total - sum; [#"../hillel.rs" 177 19 177 44] dist <- ([#"../hillel.rs" 177 19 177 44] abs_diff0 sum _60); _60 <- any uint32; diff --git a/creusot/tests/should_succeed/iterators/01_range.mlcfg b/creusot/tests/should_succeed/iterators/01_range.mlcfg index 8fe7262935..fdeaad2c29 100644 --- a/creusot/tests/should_succeed/iterators/01_range.mlcfg +++ b/creusot/tests/should_succeed/iterators/01_range.mlcfg @@ -339,57 +339,68 @@ module C01Range_SumRange end module C01Range_Impl0 use prelude.IntSize - use seq.Seq - predicate invariant3 (self : Seq.seq isize) = + use Core_Option_Option_Type as Core_Option_Option_Type + predicate invariant3 (self : Core_Option_Option_Type.t_option isize) = [#"../../../../../creusot-contracts/src/invariant.rs" 8 8 8 12] true - val invariant3 (self : Seq.seq isize) : bool + val invariant3 (self : Core_Option_Option_Type.t_option isize) : bool ensures { result = invariant3 self } - predicate inv3 (_x : Seq.seq isize) - val inv3 (_x : Seq.seq isize) : bool + predicate inv3 (_x : Core_Option_Option_Type.t_option isize) + val inv3 (_x : Core_Option_Option_Type.t_option isize) : bool ensures { result = inv3 _x } - axiom inv3 : forall x : Seq.seq isize . inv3 x = true + axiom inv3 : forall x : Core_Option_Option_Type.t_option isize . inv3 x = true use C01Range_Range_Type as C01Range_Range_Type - predicate invariant2 (self : C01Range_Range_Type.t_range) = + use prelude.Borrow + predicate invariant2 (self : borrowed (C01Range_Range_Type.t_range)) = [#"../../../../../creusot-contracts/src/invariant.rs" 8 8 8 12] true - val invariant2 (self : C01Range_Range_Type.t_range) : bool + val invariant2 (self : borrowed (C01Range_Range_Type.t_range)) : bool ensures { result = invariant2 self } - predicate inv2 (_x : C01Range_Range_Type.t_range) - val inv2 (_x : C01Range_Range_Type.t_range) : bool + predicate inv2 (_x : borrowed (C01Range_Range_Type.t_range)) + val inv2 (_x : borrowed (C01Range_Range_Type.t_range)) : bool ensures { result = inv2 _x } - axiom inv2 : forall x : C01Range_Range_Type.t_range . inv2 x = true - use Core_Option_Option_Type as Core_Option_Option_Type - predicate invariant1 (self : Core_Option_Option_Type.t_option isize) = + axiom inv2 : forall x : borrowed (C01Range_Range_Type.t_range) . inv2 x = true + use seq.Seq + predicate invariant1 (self : Seq.seq isize) = [#"../../../../../creusot-contracts/src/invariant.rs" 8 8 8 12] true - val invariant1 (self : Core_Option_Option_Type.t_option isize) : bool + val invariant1 (self : Seq.seq isize) : bool ensures { result = invariant1 self } - predicate inv1 (_x : Core_Option_Option_Type.t_option isize) - val inv1 (_x : Core_Option_Option_Type.t_option isize) : bool + predicate inv1 (_x : Seq.seq isize) + val inv1 (_x : Seq.seq isize) : bool ensures { result = inv1 _x } - axiom inv1 : forall x : Core_Option_Option_Type.t_option isize . inv1 x = true - use prelude.Borrow - predicate invariant0 (self : borrowed (C01Range_Range_Type.t_range)) = + axiom inv1 : forall x : Seq.seq isize . inv1 x = true + predicate invariant0 (self : C01Range_Range_Type.t_range) = [#"../../../../../creusot-contracts/src/invariant.rs" 8 8 8 12] true - val invariant0 (self : borrowed (C01Range_Range_Type.t_range)) : bool + val invariant0 (self : C01Range_Range_Type.t_range) : bool ensures { result = invariant0 self } - predicate inv0 (_x : borrowed (C01Range_Range_Type.t_range)) - val inv0 (_x : borrowed (C01Range_Range_Type.t_range)) : bool + predicate inv0 (_x : C01Range_Range_Type.t_range) + val inv0 (_x : C01Range_Range_Type.t_range) : bool ensures { result = inv0 _x } - axiom inv0 : forall x : borrowed (C01Range_Range_Type.t_range) . inv0 x = true + axiom inv0 : forall x : C01Range_Range_Type.t_range . inv0 x = true use seq.Seq + use prelude.Int + predicate resolve0 (self : borrowed (C01Range_Range_Type.t_range)) = + [#"../../../../../creusot-contracts/src/resolve.rs" 26 20 26 34] ^ self = * self + val resolve0 (self : borrowed (C01Range_Range_Type.t_range)) : bool + ensures { result = resolve0 self } + + predicate completed0 [#"../01_range.rs" 23 4 23 35] (self : borrowed (C01Range_Range_Type.t_range)) = + [#"../01_range.rs" 25 12 25 52] resolve0 self + /\ C01Range_Range_Type.range_start ( * self) >= C01Range_Range_Type.range_end ( * self) + val completed0 [#"../01_range.rs" 23 4 23 35] (self : borrowed (C01Range_Range_Type.t_range)) : bool + ensures { result = completed0 self } + use seq.Seq use seq.Seq use seq.Seq use prelude.IntSize use seq.Seq - use prelude.Int predicate produces0 [#"../01_range.rs" 31 4 31 64] (self : C01Range_Range_Type.t_range) (visited : Seq.seq isize) (o : C01Range_Range_Type.t_range) = @@ -404,31 +415,20 @@ module C01Range_Impl0 ensures { result = produces0 self visited o } use seq.Seq - predicate resolve0 (self : borrowed (C01Range_Range_Type.t_range)) = - [#"../../../../../creusot-contracts/src/resolve.rs" 26 20 26 34] ^ self = * self - val resolve0 (self : borrowed (C01Range_Range_Type.t_range)) : bool - ensures { result = resolve0 self } - - predicate completed0 [#"../01_range.rs" 23 4 23 35] (self : borrowed (C01Range_Range_Type.t_range)) = - [#"../01_range.rs" 25 12 25 52] resolve0 self - /\ C01Range_Range_Type.range_start ( * self) >= C01Range_Range_Type.range_end ( * self) - val completed0 [#"../01_range.rs" 23 4 23 35] (self : borrowed (C01Range_Range_Type.t_range)) : bool - ensures { result = completed0 self } - - goal next_refn : [#"../01_range.rs" 57 4 57 39] forall self : borrowed (C01Range_Range_Type.t_range) . inv0 self + goal produces_refl_refn : [#"../01_range.rs" 44 4 44 26] forall self : C01Range_Range_Type.t_range . inv0 self + -> (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) + goal produces_trans_refn : [#"../01_range.rs" 51 4 51 90] forall a : C01Range_Range_Type.t_range . forall ab : Seq.seq isize . forall b : C01Range_Range_Type.t_range . forall bc : Seq.seq isize . forall c : C01Range_Range_Type.t_range . inv0 c + /\ inv1 bc /\ inv0 b /\ inv1 ab /\ inv0 a /\ produces0 b bc c /\ produces0 a ab b + -> produces0 b bc c + /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c -> produces0 a (Seq.(++) ab bc) c) + goal next_refn : [#"../01_range.rs" 57 4 57 39] forall self : borrowed (C01Range_Range_Type.t_range) . inv2 self -> (forall result : Core_Option_Option_Type.t_option isize . match result with | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self) end - -> inv1 result + -> inv3 result /\ match result with | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self) end) - goal produces_trans_refn : [#"../01_range.rs" 51 4 51 90] forall a : C01Range_Range_Type.t_range . forall ab : Seq.seq isize . forall b : C01Range_Range_Type.t_range . forall bc : Seq.seq isize . forall c : C01Range_Range_Type.t_range . inv2 c - /\ inv3 bc /\ inv2 b /\ inv3 ab /\ inv2 a /\ produces0 b bc c /\ produces0 a ab b - -> produces0 b bc c - /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c -> produces0 a (Seq.(++) ab bc) c) - goal produces_refl_refn : [#"../01_range.rs" 44 4 44 26] forall self : C01Range_Range_Type.t_range . inv2 self - -> (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) end diff --git a/creusot/tests/should_succeed/iterators/01_range/why3session.xml b/creusot/tests/should_succeed/iterators/01_range/why3session.xml index d2c28d597a..21451b408c 100644 --- a/creusot/tests/should_succeed/iterators/01_range/why3session.xml +++ b/creusot/tests/should_succeed/iterators/01_range/why3session.xml @@ -31,14 +31,14 @@ - - + + - - + + diff --git a/creusot/tests/should_succeed/iterators/01_range/why3shapes.gz b/creusot/tests/should_succeed/iterators/01_range/why3shapes.gz index b7932098428ae2556df75c6e69d78d5cd1b65b10..f987f5878ae5f6bf2182cece7d2ae4363bdfbf9b 100644 GIT binary patch literal 961 zcmV;y13vs8iwFP!00000|D{$-Z{s!)zUx=`wrzp}9KKoXE?^iDWMI)lTku$eBB`uV zTS_G-+y46wDcO;{PJp65Si_lb9vpr{>4&@3@YOxVVf7OGVc)esujK0P$HG1JU3m6! zAa00<#>L~)>7OhXS=?o>In25Hd*^Cbd*`_s`L?Pj4sw&Jx>@QEX8DXgmR>6eVrV&c z6eC@&D2vlySlA1(vMdr|C|I=}pTNp9=RVF!K+T*Hi6E)8(Qt_EDVw#lBTYRu|S3~ zD4mDEJ$;!EInDc`Zor}5A()iYgyS|dYbdtUl-tGK0qWM}f!f!=EL|TNH{Bm5cMx<| zk20QE?rZXu7C6caVgP%C7-(1!1H?PT0D+;;#Ng$6nM1#kLSJQ|?`5Dk+vg19sL@1} zaVW;ULS_z-aYgLd4s*UG@SMh`XrCaTFLfwfpJ#S>KJN0UPeaCVpeGS4IE#5U&r`@2 zW6Gy7T}<;uiFvaRzw$wH3B1Vl_NKO6&()}tbA|lQ@g`zw-gr!4#k7{wT1{(Rrr+{C z#&1!P&zLBYas0x=F*LJc``@CdWt6d3H1(=zf^4`KCN|JWWuOs;HnOQj023N+R#1@w z6+w`iND59%9<>Km8xTzTplcNnL#P0{)C}w;umV8xLXWg-D4aU&+$0y`tIk2T-^OwxyNH4o_rjL z8{$5>cz8VhQ^cx>+u}8aIk#Lo*Sgj_znST?a;h0I)!O;~@VJks7>Ffqz5S){;skbw z%3;?%AfoRqb$=AlZ~Y-!3!C-YeX?*-@Rd8pq2E78V)Y6w+O_@h*nf-R!{JXv{pz}h zXqA;N?K-!|P`hBsJwn~CJ4yZl|6ApjFDG}*F53ZxQ?A9s{WXrwikybOM%}yG?T2`- zEq64jjJV&APtmgM$#!RCR=Llg-cJ0TC3c~ts#iFKUAJxfr!EZd*FGC1GB82CrB19QutE`c(${UIvQ0eaSGc8qGu* zmtyP{3Uh#rCt}BOn9D1H_cRVg`waPftwZ7Yva`d}VOv)Hykra)`Yd7v7qRT-WeZt7 zfA#sTi{q1flXyS;dTU}eMiiU>7DdgYU`M4IK6^BHrmeuA2)((ftyfbu>f}@*zjM5a zSdG&e3Bb+`(F`nSbw2Al|IMo#pESO?r5rn=xuYrtnYb4wCP-2lNW#!0Q!4_Pkhobu zLn>4RL0TdyI4yb99#m^UFzJJCRX`A}q=_`hHh>@`Y7Ls}K!r&VyzqjC1#eg-g?7aF zsM;hX7pg>7W79m_|3M5?sW{ zyyuig#oN#(l{6tzgG^3qkF|kpKs3M`U=7fU83-<75tQ-}A`8MNVuBRlbL%mCsF_Fd jJjSS83V}ut-Y3T>&LJtUJW!QA^vvU5Z6v&LDG2}o#7*8= diff --git a/creusot/tests/should_succeed/iterators/02_iter_mut.mlcfg b/creusot/tests/should_succeed/iterators/02_iter_mut.mlcfg index eef1cb9f30..d3cd06f184 100644 --- a/creusot/tests/should_succeed/iterators/02_iter_mut.mlcfg +++ b/creusot/tests/should_succeed/iterators/02_iter_mut.mlcfg @@ -1227,6 +1227,30 @@ module C02IterMut_Impl1 ensures { result = inv3 _x } axiom inv3 : forall x : Seq.seq (borrowed t) . inv3 x = true + use Core_Option_Option_Type as Core_Option_Option_Type + predicate invariant2 (self : Core_Option_Option_Type.t_option (borrowed t)) + val invariant2 (self : Core_Option_Option_Type.t_option (borrowed t)) : bool + ensures { result = invariant2 self } + + predicate inv2 (_x : Core_Option_Option_Type.t_option (borrowed t)) + val inv2 (_x : Core_Option_Option_Type.t_option (borrowed t)) : bool + ensures { result = inv2 _x } + + axiom inv2 : forall x : Core_Option_Option_Type.t_option (borrowed t) . inv2 x = true + use C02IterMut_IterMut_Type as C02IterMut_IterMut_Type + predicate invariant1 (self : borrowed (C02IterMut_IterMut_Type.t_itermut t)) + val invariant1 (self : borrowed (C02IterMut_IterMut_Type.t_itermut t)) : bool + ensures { result = invariant1 self } + + predicate inv0 (_x : C02IterMut_IterMut_Type.t_itermut t) + val inv0 (_x : C02IterMut_IterMut_Type.t_itermut t) : bool + ensures { result = inv0 _x } + + predicate inv1 (_x : borrowed (C02IterMut_IterMut_Type.t_itermut t)) + val inv1 (_x : borrowed (C02IterMut_IterMut_Type.t_itermut t)) : bool + ensures { result = inv1 _x } + + axiom inv1 : forall x : borrowed (C02IterMut_IterMut_Type.t_itermut t) . inv1 x = (inv0 ( * x) /\ inv0 ( ^ x)) use seq.Seq use prelude.UIntSize use prelude.Slice @@ -1244,43 +1268,37 @@ module C02IterMut_Impl1 && ([#"../../../../../creusot-contracts/src/std/slice.rs" 18 14 18 42] 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) - use C02IterMut_IterMut_Type as C02IterMut_IterMut_Type - predicate invariant2 [#"../02_iter_mut.rs" 20 4 20 30] (self : C02IterMut_IterMut_Type.t_itermut t) = + predicate invariant0 [#"../02_iter_mut.rs" 20 4 20 30] (self : C02IterMut_IterMut_Type.t_itermut t) = [#"../02_iter_mut.rs" 22 20 22 64] Seq.length (shallow_model1 ( ^ C02IterMut_IterMut_Type.itermut_inner self)) = Seq.length (shallow_model1 ( * C02IterMut_IterMut_Type.itermut_inner self)) - val invariant2 [#"../02_iter_mut.rs" 20 4 20 30] (self : C02IterMut_IterMut_Type.t_itermut t) : bool - ensures { result = invariant2 self } - - predicate inv2 (_x : C02IterMut_IterMut_Type.t_itermut t) - val inv2 (_x : C02IterMut_IterMut_Type.t_itermut t) : bool - ensures { result = inv2 _x } + val invariant0 [#"../02_iter_mut.rs" 20 4 20 30] (self : C02IterMut_IterMut_Type.t_itermut t) : bool + ensures { result = invariant0 self } - axiom inv2 : forall x : C02IterMut_IterMut_Type.t_itermut t . inv2 x - = (invariant2 x + axiom inv0 : forall x : C02IterMut_IterMut_Type.t_itermut t . inv0 x + = (invariant0 x /\ match x with | C02IterMut_IterMut_Type.C_IterMut inner -> true end) - use Core_Option_Option_Type as Core_Option_Option_Type - predicate invariant1 (self : Core_Option_Option_Type.t_option (borrowed t)) - val invariant1 (self : Core_Option_Option_Type.t_option (borrowed t)) : bool - ensures { result = invariant1 self } - - predicate inv1 (_x : Core_Option_Option_Type.t_option (borrowed t)) - val inv1 (_x : Core_Option_Option_Type.t_option (borrowed t)) : bool - ensures { result = inv1 _x } + use seq.Seq + use seq.Seq + use seq.Seq + use seq.Seq + function shallow_model0 (self : borrowed (slice t)) : Seq.seq t = + [#"../../../../../creusot-contracts/src/model.rs" 108 8 108 31] shallow_model1 ( * self) + val shallow_model0 (self : borrowed (slice t)) : Seq.seq t + ensures { result = shallow_model0 self } - axiom inv1 : forall x : Core_Option_Option_Type.t_option (borrowed t) . inv1 x = true - predicate invariant0 (self : borrowed (C02IterMut_IterMut_Type.t_itermut t)) - val invariant0 (self : borrowed (C02IterMut_IterMut_Type.t_itermut t)) : bool - ensures { result = invariant0 self } + predicate resolve0 (self : borrowed (slice t)) = + [#"../../../../../creusot-contracts/src/resolve.rs" 26 20 26 34] ^ self = * self + val resolve0 (self : borrowed (slice t)) : bool + ensures { result = resolve0 self } - predicate inv0 (_x : borrowed (C02IterMut_IterMut_Type.t_itermut t)) - val inv0 (_x : borrowed (C02IterMut_IterMut_Type.t_itermut t)) : bool - ensures { result = inv0 _x } + predicate completed0 [#"../02_iter_mut.rs" 31 4 31 35] (self : borrowed (C02IterMut_IterMut_Type.t_itermut t)) = + [#"../02_iter_mut.rs" 32 8 32 76] resolve0 (C02IterMut_IterMut_Type.itermut_inner ( * self)) + /\ Seq.(==) (shallow_model0 (C02IterMut_IterMut_Type.itermut_inner ( * self))) (Seq.empty ) + val completed0 [#"../02_iter_mut.rs" 31 4 31 35] (self : borrowed (C02IterMut_IterMut_Type.t_itermut t)) : bool + ensures { result = completed0 self } - axiom inv0 : forall x : borrowed (C02IterMut_IterMut_Type.t_itermut t) . inv0 x = (inv2 ( * x) /\ inv2 ( ^ x)) - use seq.Seq - use seq.Seq use seq.Seq use seq.Seq use seq.Seq @@ -1289,11 +1307,6 @@ module C02IterMut_Impl1 val index_logic0 [@inline:trivial] (self : slice t) (ix : int) : t ensures { result = index_logic0 self ix } - function shallow_model0 (self : borrowed (slice t)) : Seq.seq t = - [#"../../../../../creusot-contracts/src/model.rs" 108 8 108 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) @@ -1322,40 +1335,27 @@ module C02IterMut_Impl1 ensures { result = produces0 self visited tl } use seq.Seq - use seq.Seq - use seq.Seq - predicate resolve0 (self : borrowed (slice t)) = - [#"../../../../../creusot-contracts/src/resolve.rs" 26 20 26 34] ^ self = * self - val resolve0 (self : borrowed (slice t)) : bool - ensures { result = resolve0 self } - - predicate completed0 [#"../02_iter_mut.rs" 31 4 31 35] (self : borrowed (C02IterMut_IterMut_Type.t_itermut t)) = - [#"../02_iter_mut.rs" 32 8 32 76] resolve0 (C02IterMut_IterMut_Type.itermut_inner ( * self)) - /\ Seq.(==) (shallow_model0 (C02IterMut_IterMut_Type.itermut_inner ( * self))) (Seq.empty ) - val completed0 [#"../02_iter_mut.rs" 31 4 31 35] (self : borrowed (C02IterMut_IterMut_Type.t_itermut t)) : bool - ensures { result = completed0 self } - - goal next_refn : [#"../02_iter_mut.rs" 63 4 63 44] forall self : borrowed (C02IterMut_IterMut_Type.t_itermut t) . inv0 self - -> inv0 self - /\ (forall result : Core_Option_Option_Type.t_option (borrowed t) . inv1 result + goal produces_refl_refn : [#"../02_iter_mut.rs" 50 4 50 26] forall self : C02IterMut_IterMut_Type.t_itermut t . inv0 self + -> inv0 self /\ (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) + goal next_refn : [#"../02_iter_mut.rs" 63 4 63 44] forall self : borrowed (C02IterMut_IterMut_Type.t_itermut t) . inv1 self + -> inv1 self + /\ (forall result : Core_Option_Option_Type.t_option (borrowed t) . inv2 result /\ match result with | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self) end - -> inv1 result + -> inv2 result /\ match result with | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self) end) - goal produces_trans_refn : [#"../02_iter_mut.rs" 57 4 57 90] forall a : C02IterMut_IterMut_Type.t_itermut t . forall ab : Seq.seq (borrowed t) . forall b : C02IterMut_IterMut_Type.t_itermut t . forall bc : Seq.seq (borrowed t) . forall c : C02IterMut_IterMut_Type.t_itermut t . inv2 c - /\ inv3 bc /\ inv2 b /\ inv3 ab /\ inv2 a /\ produces0 b bc c /\ produces0 a ab b - -> inv2 c + goal produces_trans_refn : [#"../02_iter_mut.rs" 57 4 57 90] forall a : C02IterMut_IterMut_Type.t_itermut t . forall ab : Seq.seq (borrowed t) . forall b : C02IterMut_IterMut_Type.t_itermut t . forall bc : Seq.seq (borrowed t) . forall c : C02IterMut_IterMut_Type.t_itermut t . inv0 c + /\ inv3 bc /\ inv0 b /\ inv3 ab /\ inv0 a /\ produces0 b bc c /\ produces0 a ab b + -> inv0 c /\ inv3 bc - /\ inv2 b + /\ inv0 b /\ inv3 ab - /\ inv2 a + /\ inv0 a /\ produces0 b bc c /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c -> produces0 a (Seq.(++) ab bc) c) - goal produces_refl_refn : [#"../02_iter_mut.rs" 50 4 50 26] forall self : C02IterMut_IterMut_Type.t_itermut t . inv2 self - -> inv2 self /\ (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) end diff --git a/creusot/tests/should_succeed/iterators/02_iter_mut/why3session.xml b/creusot/tests/should_succeed/iterators/02_iter_mut/why3session.xml index 427502c37f..e4cf9c256a 100644 --- a/creusot/tests/should_succeed/iterators/02_iter_mut/why3session.xml +++ b/creusot/tests/should_succeed/iterators/02_iter_mut/why3session.xml @@ -113,12 +113,12 @@ - - - + + + diff --git a/creusot/tests/should_succeed/iterators/02_iter_mut/why3shapes.gz b/creusot/tests/should_succeed/iterators/02_iter_mut/why3shapes.gz index a8943ec22988bc33a672128210e016862555c65c..178a861ce55889e2c0b66151547b704b78d95f83 100644 GIT binary patch literal 3555 zcmV<94IJ_xiwFP!00000|J_Tb=d0Me){Mh{L}i`KR)eG$G@!Q`sPoo z^G|MneC7qY&qG!~JER3|hfuKlmHXknJNV;=^GAnRhr{X1?$fFE2Pn8ZpLYA>*?n?f z$*p@oUEkLQzm23OYnw!t->>e@?ryg^`^Ue3J{N_E``zQ-9nYi?kq`VtJ~}p#>Zi}= z-IM=`6l#_?oDclmxDWn3-d<<~to_&B;q+l&5qA@&Htq+UpF_XJ+gGH}_W^D@182r? z+b|X2%r!W3A1_JAi<=~Jg;#xeJk_5o|3uuAKQzvNdN}_l4&$CQyNa{BsNYqm&Q6(~ zDtkq~poggfMNpu~JH$0pkV8|*2V^4IsxsY=#QVhoiv2x`z1O|@+er61^FERiBy@^{ z$njJs00q!Xt;ETo7hIZA3_#Wl(EAo2BL38b0L9BMjVMk=d_IfMT72H&vn7)Tv0&36 z+Os0d&{bJPWtAt&Jdp>)xuG?cxG|jRXYfxM_RcGoxIOA7aJD}l{UdIE*Y11w&Lz0l zoU3L!XkjF(l)O!)B+B$Vd(_a0yR(b)n~BqJCV?Sm7q@9+NS-J+ZIs!xVJ8&`DyE!; ztblU3S|EgV%r6k_MNHNEhkhTzVxb zy+)ckFcSF1Q3gv?zsCJOAeev%Q`(i zp1%0{51;-$*su+d&Hm^P>1ZI52u3Rm%cJHnma9=}Z1 z!tJIOiqp%7Zt|hOE;wugt;q6@n{LPZpt*~xVmny9nbsV66~*TCx|S+F|)=fST#pIx~}|8zP$dydw&aGSd-k<;Hc4pBd9 zDR2dp7`TGYF>Hl$e-t=zA|i;?61-2F_%wjx#tPaHa92=z33K1t4mK3U-MTqFu8;of zxl4ScPkhif_VilbW-sLJaHWDJsZ7?gxw6Z=%}320&pDR2olL(ol($%F%1!#X-&}5x z-9?c{WE7|Ky<~q|5u4zJD`I1O^@?E~uSj!saJjbWWH`Pe8(fhWEEgfHFG57G3)$;J zEi=lnb{{c1<%fkDKQ+{CkKeOI*-|0OVy$qsju~G&_%fTrm@$ycjSvfq9Pc37e)1^R zx)vLRLrSv^(WC$xXZmPq+K6aw+d;4u$}pT{Z-{{>PSTN!#(0z+QzxGb0T%b6I!Wh< z7_D3H(>YMZh^~8h&?!P+z$0pgmkC}*c+eOudOuekyv(kx!e4o>3=MwQ>R(kLT~Z)Q zE(>hu4^Lk(s07JPo_`Qv2K3e;;O^NSKF=J=bhnYUEBhjNh_)$whCtUUJF0b8o<1Mz zr}=|Fq7DDk9Y6T{&xgb2+{axSCB!bJPFtyyBw&&x8J}@FsY56Awx)tuhTpf=NczBn z{u8R=?4!DmE2@v8qpsu1ODVa0DV^(gcSEeadpsFju2nSVt+C zIYwBKyi2~h`=PJze&~1Ue(2BWe)L@Tqf+Enco4pv#^PwLAJRgI)V` zSj@6bi&3@{INW$RogVr|1xMj=em6-r|s+b4)ffE%5Z`P<$>&5_B^I>H0sO})}%2D z(}PAT1NLnhi1rZxq9Nc%*G;x12O9h}Lw;VcAX~FrD_{#3jVQL;a(&eud#_b?)POgxC2isv?7b3+ANW;hy?Ab&WkBSpiREn!#AqLiP zsC)nT%4YnVUWTCu-0vTsU3vg{rSH=V%;i8tUychjnsc-Ie0=n-`sm7oUq77iKzwJL zb%9V&Go6A7(+gE9ZEb?-D-Y(|K{T2G47v)+H|Om5cS~0)xG1JWV>kT*kruM>SAbvd1g$vx$jo`;n1O*rzB~dV%7=)lg zGlamH_2VFD<4tq8ZoU*OzHQ-DiiG(6KCgCbs$jCM%9$KLwlO~U*oLz`IT4H|?n{qt z2$nlV#=BM`4BwCR7AK_?=?iKVZ`5`T;C**1Dd2v@?Mdf}8y>jKJrDp$~Isqr!M0je9Y-aU!4_Bn@b-i##{vF_U^_4e5=@H)O$Xzo~Q&o+xIL&u3P3oO294CZ*+ z*vY1Q+iGXJ2N2QDT+sW4K<~q!)e2PU8dBAcF)g4ZjnLYcl2y7NEBTQIEM~6Ih#!2rSCq|Y?!c@+w62QBNhReF7tPxD}8cJ=bQUQs*3dw+iiaWw<+E7Oo zQG!ZJya#C-0UVL2nMa~vDY0NIXbZ}Mv>+^S3(Nw7g9T!-(i2YAnhC;a4NB>{77dfM z5}FXDwF#_}Zy|u!_uN!9>W=UR5qVP)R$_`ME6^^=0=|VnsVgHIt_3Aj6YxPom1rEQ zSu~9kYbmWnnc{!ka%MTT94sf68OxBkvP`a+5~VlPRYpthsDZ|5)EgIyvxe7vEtnOk z8nA*`ZY5z`R24DAkQLr2)-!S+0e$0!>#~!QTvCvT#!=O4TS* zikgtRDl1l(re>akTuZPLVfD`^fu<(VBP!_$0aBJI3|cp`lwP`~sv(jfR+w+1Vt|L= z&e5!aO05|~+t$RF1Z6~dLn9StCH*EUO)Vr9HTM`0eA#ed6t5(jQpj2fLIM>;{zi#8 zQE|g7=LNhfvyItiB-lbjC#r{X_c^wub|PM)xN11Cj`&A3fmn5wF9k{Z{!+~dqDP$ zu!dX1tfAI`HN+#M*R`+8T6rNj5fv~ZouLd^qbtB<#4~O4z34O67}*fK zrx2y4CJ0zzFjho>s_QDzkD(N4U@-lTybx7#ytWIMH$*5!wIalLEb)~V#zmEfP#PR2UAHZ?|eFb^PeOMO&76!k;UGOMnrY5H0USj5>HCB%d zlV4qVREA7<;qZI84_08x8B=L5YbG4Uuv_VhV5wkga23neMP*(ln{Cwjvayntc3x~4#2tt zLOjHZ6R-dQ5ww94#u_AL`>Fy@Fok)60Ucy0UR~vCFEQ0nS(^wXUjZa5#|5niwFP!00000|J_H4;<#7!b~vbN4-#og-m;BPnULwNf8r$bfAwBJ8%{qDdjnfRbj;$vWgsDAu( z*gS_HS)~_wqxs0swf_(f^X-)(z&3o@JnTPg8}Qe0YVE(H`6culx_!eca~I+67vSt1 z?mkXMIC}}s-la?8d~uycuIZ|ePy6;$6P}rW4iB9VA0H3@NyD@!&#uz!Ch2!IsB=)} zpvqB^ujt`afifykmL2kvDX6I_lmjZ0>{XfX$I|`MfW-cu#6IfY{%xjvQ+S_A2{Jm; zAaQ)E6MzcvSSx8V>V=jT6a!E+19;ctL&85bAt3RJVM~IV%=@V|)wD658E5EE9rrFPmiaB|CUUmj?ZOjne%J4N_s(ay zx14JhMR^QffhwB_e84|{prHdv=IU+C_c~C^mb1jp{jbK(|5DMQLp=1}o?qf)qsMmdzS@&Tl7YI6~ zoHJR0gPLhPGF!7Ap7P1mn^?>laWYvKEEDOi3C?(E1i(4!eV)9K>DZX* z(%tn^dSyAiCZ(rZBi(AlZz*j}bU}0d>b3=1rxQPfr!5(28@Y`iaYF+cAQdyiasMTi z95hFkwSRire-7;*KK^^M;XXok+ns;NMC4GlyxpmV()9U5*X7V(&p2!bZP@u8*TatYQFG!*my^}&lhyt#iR)kckD)qy z;Z!CrUhVqQ^8MxI>j^lq@Q?j2_zlZdXFtfwg4N+akKtSTdLg0{qteeYri*M*?)m)uq)>Eyxo1E^ZOkw6ORew_87J2`26Wuh28gi zvw-PVx268FH&e*$6vu#Zc7(&^o4f}ji1i?c3i{d~^i4mA#WC0l%uq0zn`Ntxte&%K zT3c4$*+bXm&;_fe^;fLA?1)y4aAMWN>h;NLfA*qPN8T@3^`+(e%gfgj@S@VFft%7* z$&&u=(~$I|&jqfCk^)!MIfboQ?#}`zO(X=FTY~p_lQ<2aw6TFc1l(4L$1r!j?NCEe z-ClM3r>kA~au^aH8xtRljXhq<+x(Th9j{dJER~bBVy^r+Z;M%TCrXYLeJ3;SjO8tr znrfXt?$*Z})NoPakr<`vaxXRBR;DKS%oV9IzIesBPFKWI9UQN%2N}+<$R}466)!~y zABzw<>OzgW(B~QDRJ+d@J>`eT8b3GGeUCq~g#26~%2Tayv5uKvJNhzT!dNhns z23Xoh>STi>Qnc>9&y+xwBDxvj!Q=>i1W%|1US)Wd;K5L^82wxi@T$1Bj(?TCDmM5- ztA9~}cus*NxgxMlczFIyK_yD=)20d8LW!>5Hqh3_hiHW^t%t??$g7=`Y^^_OcLV9QpaBEEDM-rNv3C7+3TdMQ2^d*SwUT_B;JUoEQV*eU*!WXn1<;Tn=NOa*m#$ z4*gPei|Zr>yTpj7vUjPk?tb{&yC3n3bU)%JbU$XP`_Z}k8EUy`Z|~lbohH}p-!aR; zq*tFjBl{WA&+zpWM)m+x=!7fh^h_>6Qjp0&<~Y}s;MeC$%Z-N!wpa0l!h_o(3TwTFkEH*iqQn$Tw^g5%$F`%fC;#yAIt4Mmvj20OT82(^#T$ijGs&ALSIEDEZK$q`k>VAkX=I7^Y?F#- z#R(}Y$JH;80&6@pynlS*3;vDAVd#*d3?ukH7C{k) zMp+abGlLLSXr~Yqv%a4MZMta**WKrer?)Md%8`)1-<8#2O;=p?RXJDl$2KmO9@}Vk zBqw9_oc86%HUcZ1A{Rp|5r^+*dP|c@1Dv|{EPXm(Zm9pl_IPH{^PB`w+fnzJlg8_l2 z6;=r&EH|e1wY5P6Y-`=p5iT9a*`a{mdKJ7E%&MA5*v5NZ0|ehT6b9oV;m|nL4wXac zkiODsJVt6Q)>gJ{&FZcbs;!ZCk{i)NZ7gaXk@%aCENEziXQIUpJ!+;UDr6ymvYiA$ zNNAUl5F9cG)`4-L9ViFVfpEYb5I8tsj>DwVBn$W!0<~$Z?1YiX&@c#5LXGS^sabZNmsd(TMKY!T zgcIBebOM}Uj$6lxxOQBvxR!OW=o@R4@Mxj)hV&++7Q7R!xRTsSQVlrCoUl$9C$tml z71%CtW4&z!2jD>ycZjA_wzgonsp~7Log~whPKvJvuX((wlC|zMt7Xer+tdwjYuoaG zpso}+MX=_llOR)*s-PDZLV!8I%^SVY;iSyQl@!H5X0GT2*Tbaoib=mw2V&n!XN9xeS#%bhWzN`g z4`ZCs&M0T3Gh)Rp1`VPm%R*tu{V}qJUkX*iQNYM!|)VY#4VD-uZ^@msXT`I80%xOkI_Dc`xx(I!2kJK zl9ZCEE)dWmLSq$U9S^JnsRSs|r1%Mxi~wW4AyOE>vtN_N21$2{>F5=Pq6uX>%P39? zuQhME$Se|Blv#nlExR=bqo`Q&7HVlY6AA^iZL19hSQ0V?A>xO^B~ZKs3Yfr&2dcz? z$E;5Dsr&&d2gp~5ciKmF0Z?J^8{CDCBDXEGod}9DAGTCIa!P(}6G#~<-$lUhV;~f@-<+NMW}z4Wm-Qw%{9H?n870W?T9l-HizyOJb&!H&g?1@1br2MLY6uW+>2! zSU8H}7rz;wQW>mkDr|^TNwTw@QjMmPI2QEY2dagEY7U68kg82e^g#6o$fyhwFqI%V z*@u=2i>|{UmDk8PqjFVoDpTuVD1eECBVWgW@Ggri=^ N`5%2E7#Ni^003Xs3G4s> diff --git a/creusot/tests/should_succeed/iterators/03_std_iterators.mlcfg b/creusot/tests/should_succeed/iterators/03_std_iterators.mlcfg index 3d75fae7ef..4077e52c51 100644 --- a/creusot/tests/should_succeed/iterators/03_std_iterators.mlcfg +++ b/creusot/tests/should_succeed/iterators/03_std_iterators.mlcfg @@ -348,7 +348,7 @@ module C03StdIterators_SliceIter return _0 } BB11 { - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _17; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _17; assert { [@expl:type invariant] inv3 _17 }; assume { resolve4 _17 }; [#"../03_std_iterators.rs" 8 4 8 38] _22 <- ([#"../03_std_iterators.rs" 8 4 8 38] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem))); @@ -745,7 +745,7 @@ module C03StdIterators_VecIter return _0 } BB10 { - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _16; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _16; assert { [@expl:type invariant] inv3 _16 }; assume { resolve4 _16 }; [#"../03_std_iterators.rs" 19 4 19 38] _21 <- ([#"../03_std_iterators.rs" 19 4 19 38] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem))); @@ -1148,7 +1148,7 @@ module C03StdIterators_AllZero return _0 } BB12 { - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _17; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _17; _17 <- (let Core_Option_Option_Type.C_Some x0 = _17 in Core_Option_Option_Type.C_Some (any borrowed usize)); [#"../03_std_iterators.rs" 29 4 29 87] _22 <- ([#"../03_std_iterators.rs" 29 4 29 87] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem))); goto BB13 @@ -1156,7 +1156,7 @@ module C03StdIterators_AllZero BB13 { [#"../03_std_iterators.rs" 29 4 29 87] produced <- _22; _22 <- any Snapshot.snap_ty (Seq.seq (borrowed usize)); - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] x <- __creusot_proc_iter_elem; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] x <- __creusot_proc_iter_elem; __creusot_proc_iter_elem <- any borrowed usize; [#"../03_std_iterators.rs" 31 8 31 14] x <- { x with current = ([#"../03_std_iterators.rs" 31 13 31 14] (0 : usize)) ; }; assume { resolve2 x }; @@ -2462,7 +2462,7 @@ module C03StdIterators_SumRange return _0 } BB10 { - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _17; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _17; [#"../03_std_iterators.rs" 65 4 65 48] _22 <- ([#"../03_std_iterators.rs" 65 4 65 48] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem))); goto BB11 } @@ -2859,7 +2859,7 @@ module C03StdIterators_EnumerateRange return _0 } BB11 { - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _12; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _12; [#"../03_std_iterators.rs" 73 4 73 96] _17 <- ([#"../03_std_iterators.rs" 73 4 73 96] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem))); goto BB12 } @@ -3433,7 +3433,7 @@ module C03StdIterators_MyReverse return _0 } BB15 { - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _28; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _28; [#"../03_std_iterators.rs" 97 4 97 36] _33 <- ([#"../03_std_iterators.rs" 97 4 97 36] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem))); goto BB16 } diff --git a/creusot/tests/should_succeed/iterators/04_skip.mlcfg b/creusot/tests/should_succeed/iterators/04_skip.mlcfg index dd6b61cf78..344f5ba626 100644 --- a/creusot/tests/should_succeed/iterators/04_skip.mlcfg +++ b/creusot/tests/should_succeed/iterators/04_skip.mlcfg @@ -589,41 +589,38 @@ module C04Skip_Impl0 ensures { result = inv3 _x } axiom inv3 : forall x : Seq.seq item0 . inv3 x = true - use Core_Option_Option_Type as Core_Option_Option_Type - predicate invariant2 (self : Core_Option_Option_Type.t_option item0) - val invariant2 (self : Core_Option_Option_Type.t_option item0) : bool + use C04Skip_Skip_Type as C04Skip_Skip_Type + predicate invariant2 (self : C04Skip_Skip_Type.t_skip i) + val invariant2 (self : C04Skip_Skip_Type.t_skip i) : bool ensures { result = invariant2 self } - predicate inv2 (_x : Core_Option_Option_Type.t_option item0) - val inv2 (_x : Core_Option_Option_Type.t_option item0) : bool + predicate inv2 (_x : C04Skip_Skip_Type.t_skip i) + val inv2 (_x : C04Skip_Skip_Type.t_skip i) : bool ensures { result = inv2 _x } - axiom inv2 : forall x : Core_Option_Option_Type.t_option item0 . inv2 x = true - use C04Skip_Skip_Type as C04Skip_Skip_Type - predicate invariant1 (self : borrowed (C04Skip_Skip_Type.t_skip i)) - val invariant1 (self : borrowed (C04Skip_Skip_Type.t_skip i)) : bool + axiom inv2 : forall x : C04Skip_Skip_Type.t_skip i . inv2 x = true + use Core_Option_Option_Type as Core_Option_Option_Type + predicate invariant1 (self : Core_Option_Option_Type.t_option item0) + val invariant1 (self : Core_Option_Option_Type.t_option item0) : bool ensures { result = invariant1 self } - predicate inv1 (_x : borrowed (C04Skip_Skip_Type.t_skip i)) - val inv1 (_x : borrowed (C04Skip_Skip_Type.t_skip i)) : bool + predicate inv1 (_x : Core_Option_Option_Type.t_option item0) + val inv1 (_x : Core_Option_Option_Type.t_option item0) : bool ensures { result = inv1 _x } - axiom inv1 : forall x : borrowed (C04Skip_Skip_Type.t_skip i) . inv1 x = true - predicate invariant0 (self : C04Skip_Skip_Type.t_skip i) - val invariant0 (self : C04Skip_Skip_Type.t_skip i) : bool + axiom inv1 : forall x : Core_Option_Option_Type.t_option item0 . inv1 x = true + predicate invariant0 (self : borrowed (C04Skip_Skip_Type.t_skip i)) + val invariant0 (self : borrowed (C04Skip_Skip_Type.t_skip i)) : bool ensures { result = invariant0 self } - predicate inv0 (_x : C04Skip_Skip_Type.t_skip i) - val inv0 (_x : C04Skip_Skip_Type.t_skip i) : bool + predicate inv0 (_x : borrowed (C04Skip_Skip_Type.t_skip i)) + val inv0 (_x : borrowed (C04Skip_Skip_Type.t_skip i)) : bool ensures { result = inv0 _x } - axiom inv0 : forall x : C04Skip_Skip_Type.t_skip i . inv0 x = true + axiom inv0 : forall x : borrowed (C04Skip_Skip_Type.t_skip i) . inv0 x = true + use seq.Seq use seq.Seq use seq.Seq - predicate completed1 [#"../common.rs" 11 4 11 36] (self : borrowed i) - val completed1 [#"../common.rs" 11 4 11 36] (self : borrowed i) : bool - ensures { result = completed1 self } - predicate resolve0 (self : item0) val resolve0 (self : item0) : bool ensures { result = resolve0 self } @@ -636,19 +633,6 @@ module C04Skip_Impl0 use prelude.Int use seq.Seq use prelude.UIntSize - predicate completed0 [#"../04_skip.rs" 22 4 22 35] (self : borrowed (C04Skip_Skip_Type.t_skip i)) = - [#"../04_skip.rs" 23 8 31 9] UIntSize.to_int (C04Skip_Skip_Type.skip_n ( ^ self)) = 0 - /\ (exists i : borrowed i . exists s : Seq.seq item0 . inv4 i - /\ inv3 s - /\ Seq.length s <= UIntSize.to_int (C04Skip_Skip_Type.skip_n ( * self)) - /\ produces1 (C04Skip_Skip_Type.skip_iter ( * self)) s ( * i) - /\ (forall i : int . 0 <= i /\ i < Seq.length s -> resolve0 (Seq.get s i)) - /\ completed1 i /\ ^ i = C04Skip_Skip_Type.skip_iter ( ^ self)) - val completed0 [#"../04_skip.rs" 22 4 22 35] (self : borrowed (C04Skip_Skip_Type.t_skip i)) : bool - ensures { result = completed0 self } - - use seq.Seq - use seq.Seq predicate produces0 [#"../04_skip.rs" 36 4 36 64] (self : C04Skip_Skip_Type.t_skip i) (visited : Seq.seq item0) (o : C04Skip_Skip_Type.t_skip i) = @@ -662,27 +646,43 @@ module C04Skip_Impl0 val produces0 [#"../04_skip.rs" 36 4 36 64] (self : C04Skip_Skip_Type.t_skip i) (visited : Seq.seq item0) (o : C04Skip_Skip_Type.t_skip i) : bool ensures { result = produces0 self visited o } - goal produces_refl_refn : [#"../04_skip.rs" 50 4 50 26] forall self : C04Skip_Skip_Type.t_skip i . inv0 self - -> inv0 self /\ (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) - goal next_refn : [#"../04_skip.rs" 63 4 63 41] forall self : borrowed (C04Skip_Skip_Type.t_skip i) . inv1 self - -> inv1 self - /\ (forall result : Core_Option_Option_Type.t_option item0 . inv2 result + use seq.Seq + predicate completed1 [#"../common.rs" 11 4 11 36] (self : borrowed i) + val completed1 [#"../common.rs" 11 4 11 36] (self : borrowed i) : bool + ensures { result = completed1 self } + + predicate completed0 [#"../04_skip.rs" 22 4 22 35] (self : borrowed (C04Skip_Skip_Type.t_skip i)) = + [#"../04_skip.rs" 23 8 31 9] UIntSize.to_int (C04Skip_Skip_Type.skip_n ( ^ self)) = 0 + /\ (exists i : borrowed i . exists s : Seq.seq item0 . inv4 i + /\ inv3 s + /\ Seq.length s <= UIntSize.to_int (C04Skip_Skip_Type.skip_n ( * self)) + /\ produces1 (C04Skip_Skip_Type.skip_iter ( * self)) s ( * i) + /\ (forall i : int . 0 <= i /\ i < Seq.length s -> resolve0 (Seq.get s i)) + /\ completed1 i /\ ^ i = C04Skip_Skip_Type.skip_iter ( ^ self)) + val completed0 [#"../04_skip.rs" 22 4 22 35] (self : borrowed (C04Skip_Skip_Type.t_skip i)) : bool + ensures { result = completed0 self } + + goal next_refn : [#"../04_skip.rs" 63 4 63 41] forall self : borrowed (C04Skip_Skip_Type.t_skip i) . inv0 self + -> inv0 self + /\ (forall result : Core_Option_Option_Type.t_option item0 . inv1 result /\ match result with | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self) end - -> inv2 result + -> inv1 result /\ match result with | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self) end) - goal produces_trans_refn : [#"../04_skip.rs" 57 4 57 90] forall a : C04Skip_Skip_Type.t_skip i . forall ab : Seq.seq item0 . forall b : C04Skip_Skip_Type.t_skip i . forall bc : Seq.seq item0 . forall c : C04Skip_Skip_Type.t_skip i . inv0 c - /\ inv3 bc /\ inv0 b /\ inv3 ab /\ inv0 a /\ produces0 b bc c /\ produces0 a ab b - -> inv0 c + goal produces_refl_refn : [#"../04_skip.rs" 50 4 50 26] forall self : C04Skip_Skip_Type.t_skip i . inv2 self + -> inv2 self /\ (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) + goal produces_trans_refn : [#"../04_skip.rs" 57 4 57 90] forall a : C04Skip_Skip_Type.t_skip i . forall ab : Seq.seq item0 . forall b : C04Skip_Skip_Type.t_skip i . forall bc : Seq.seq item0 . forall c : C04Skip_Skip_Type.t_skip i . inv2 c + /\ inv3 bc /\ inv2 b /\ inv3 ab /\ inv2 a /\ produces0 b bc c /\ produces0 a ab b + -> inv2 c /\ inv3 bc - /\ inv0 b + /\ inv2 b /\ inv3 ab - /\ inv0 a + /\ inv2 a /\ produces0 b bc c /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c -> produces0 a (Seq.(++) ab bc) c) end diff --git a/creusot/tests/should_succeed/iterators/04_skip/why3session.xml b/creusot/tests/should_succeed/iterators/04_skip/why3session.xml index 99ce13df07..0c1f8d3819 100644 --- a/creusot/tests/should_succeed/iterators/04_skip/why3session.xml +++ b/creusot/tests/should_succeed/iterators/04_skip/why3session.xml @@ -26,12 +26,12 @@ - - - + + + diff --git a/creusot/tests/should_succeed/iterators/04_skip/why3shapes.gz b/creusot/tests/should_succeed/iterators/04_skip/why3shapes.gz index fc2bfb948a0ada86938598bc97679c7707304cff..4137c8e3fe8f267cf6e7e752ca8f2ec33900e5ea 100644 GIT binary patch literal 1069 zcmV+|1k(E-iwFP!00000|D{z+Z{s!)zWZ1Bwr%#p;hV+gAOtaJpy;Iqk2NTYN{n@+ z)ONDlf8XIlmh24*6m!q@uzs`3pXz_y`Za%?s9-j*O0W+B%=BjRV%N1R`;~-VJVdr!-cz~{z|*7 z+Aq18v#74LdsO0m>)YVN_6kqn5}7zTIA8SnM9Dx~fp%hqdZC#ss8a>YQaL&;Ws+W& zB2}O)F~VudX7%)1z0)a=#sQ|FWQt9T1WpL4h^c^HgoUS*`ND1TNv>`JRx=80a?2K- z$>-hx6kdV>)jaqxzPujdId*s={lo6JafoxF{9Qs%`{4;W^fx^58-F;(f9Lr>j&IR%XpqKXUriE-0Hc9CHg&P} z_x^1^oF)H+-xOlrWiDhKcPdZo?!PCZcngoMM=nSHhf}u?*+SwQtAcar_p$ zPcL5+@$3FIpE{;|zaRX;G4T5izaQ(dbLpNORig0}MMAhg;puLFj>k;Mc(zR6l&9^* zV_77yBrCb|=W&PO7dJ!p5$4n~WOniU?l3;>111KaC-%q}{Pu@9Je{BMe27OpX#AIZ zWN@}=mg8d2S(sNpwy;qK=BG1XTE^c;4mHQY}R8 zE>!+O6F8chhfbBk$AZ=%ubKdgAPjVRcG^vTLSto!k}9^&`&WvY>Rs=++f=sZf;JV|hg>5@qt=)E|txS9L#)zUvGAm#0notX7=_5@aj7E=Cao1EN|2T_8CJ~18w2m{axLj~7DP}zB@K+%pV zb;}3SdLvZd^|I$GNa=ahs*5Tzl%?dFa!XMRwG=ER7K{aLL0LdY!UDIzETC3c$w+jd z!~|m^?*J8aJ%rE++IEI3gI6kA@KR$YTGgv)2-QmT99V#^4>?FiZ;k!|uX*8=I0^s&LUfxcZ{M1DhQRUj=OBU#dYhT~KLl0wvg}3K^X<%9X2Y2~@+B7+7>qBkm%oB3 z_GVPVf}If=p5t+!xx;dxXLL27yCJ~2Ye?F85>b4sqE(i?D0^P^FqbN_;mlo9ztFCW z_G@mYESiOOBqfM7)(tk>1)jh;GIECCFzdra8GyO~^~h+-g>I^#O%=>b6Zp8)NqSzY zRDryt2*;(E)bpkKU{fAl07^m5lo%HY91&I!R{%Q;i%v)LncL)(Ep7r)G74gJD`uT3 zr``Y(o`V5XJz&$nydL8vwsfNLVfS0##i>wum(cT}dm>KX1+e%v^M3DNVjvgW2m0F= z;5*(E6eO$g6wm$fJ*psVReHvLrxV=Z@f`o1hku;jVvtY~O~Rp=B#;2X8}?Y0#TM`J z?a*Dc{6xP4G#IfU++&r)6mA|SwWqoblTnz2PGL$;VGg_;=IBfe@Nl`sx<8%z@3H;# z@+}d+9bSjiAPnvg9Ug-KJhb%tSdK$T_Y6@bnoLn7MBX8DcWvC`+wsDv99;iOy0{*wW>Kfvd3uT;Wr^?1s}^Ekf?D zRQW*@1fH6QkCmdwLe`)cO#oRC1;MU2F^b_io(}1@@lwzYFW0iEy5#Jd2YR)xDi7Nw zr&JqCSK@4{^fVvJfEEAflT~oj$@AENWul0MtP z%mI@qWAs(|V3fTndt3I)3;vgG zgJ&zDm^8{c1(qqJnSr*kf;DKUp9Qap4vhHDTW^TZ96|%i0o2NIC9P6ix2O#m-U?%G z`QU1F%Iw>{-b>SHjWSx(MiT|eGJ4IW=Ol)E4xTd)&V%(}Jdh*hL3$7#NGq(cw#k}v z9qT%Zy_2l9Y+tv|A&E{>1@qi_Zap`iYtPlHj*{**NC{w)yS>yLRn1uIFxFhBbO^XL l5*llP0$LMm5-OX%MX>2$O005))7XknP diff --git a/creusot/tests/should_succeed/iterators/05_map.mlcfg b/creusot/tests/should_succeed/iterators/05_map.mlcfg index f3b7edb3cd..24b119c79b 100644 --- a/creusot/tests/should_succeed/iterators/05_map.mlcfg +++ b/creusot/tests/should_succeed/iterators/05_map.mlcfg @@ -1935,86 +1935,62 @@ module C05Map_Impl0 ensures { result = inv9 _x } axiom inv9 : forall x : i . inv9 x = true - type item0 - predicate invariant8 (self : item0) - val invariant8 (self : item0) : bool + use seq.Seq + predicate invariant8 (self : Seq.seq (borrowed f)) + val invariant8 (self : Seq.seq (borrowed f)) : bool ensures { result = invariant8 self } - predicate inv8 (_x : item0) - val inv8 (_x : item0) : bool + predicate inv8 (_x : Seq.seq (borrowed f)) + val inv8 (_x : Seq.seq (borrowed f)) : bool ensures { result = inv8 _x } - axiom inv8 : forall x : item0 . inv8 x = true - predicate invariant7 (self : borrowed f) - val invariant7 (self : borrowed f) : bool + axiom inv8 : forall x : Seq.seq (borrowed f) . inv8 x = true + type item0 + predicate invariant7 (self : Seq.seq item0) + val invariant7 (self : Seq.seq item0) : bool ensures { result = invariant7 self } - predicate inv7 (_x : borrowed f) - val inv7 (_x : borrowed f) : bool + predicate inv7 (_x : Seq.seq item0) + val inv7 (_x : Seq.seq item0) : bool ensures { result = inv7 _x } - axiom inv7 : forall x : borrowed f . inv7 x = true - predicate invariant6 (self : b) - val invariant6 (self : b) : bool + axiom inv7 : forall x : Seq.seq item0 . inv7 x = true + predicate invariant6 (self : item0) + val invariant6 (self : item0) : bool ensures { result = invariant6 self } - predicate inv6 (_x : b) - val inv6 (_x : b) : bool + predicate inv6 (_x : item0) + val inv6 (_x : item0) : bool ensures { result = inv6 _x } - axiom inv6 : forall x : b . inv6 x = true - use seq.Seq - predicate invariant5 (self : Seq.seq (borrowed f)) - val invariant5 (self : Seq.seq (borrowed f)) : bool + axiom inv6 : forall x : item0 . inv6 x = true + predicate invariant5 (self : borrowed f) + val invariant5 (self : borrowed f) : bool ensures { result = invariant5 self } - predicate inv5 (_x : Seq.seq (borrowed f)) - val inv5 (_x : Seq.seq (borrowed f)) : bool + predicate inv5 (_x : borrowed f) + val inv5 (_x : borrowed f) : bool ensures { result = inv5 _x } - axiom inv5 : forall x : Seq.seq (borrowed f) . inv5 x = true - predicate invariant4 (self : Seq.seq item0) - val invariant4 (self : Seq.seq item0) : bool + axiom inv5 : forall x : borrowed f . inv5 x = true + predicate invariant4 (self : b) + val invariant4 (self : b) : bool ensures { result = invariant4 self } - predicate inv4 (_x : Seq.seq item0) - val inv4 (_x : Seq.seq item0) : bool + predicate inv4 (_x : b) + val inv4 (_x : b) : bool ensures { result = inv4 _x } - axiom inv4 : forall x : Seq.seq item0 . inv4 x = true - use Core_Option_Option_Type as Core_Option_Option_Type - predicate invariant3 (self : Core_Option_Option_Type.t_option b) - val invariant3 (self : Core_Option_Option_Type.t_option b) : bool + axiom inv4 : forall x : b . inv4 x = true + predicate invariant3 (self : Seq.seq b) + val invariant3 (self : Seq.seq b) : bool ensures { result = invariant3 self } - predicate inv3 (_x : Core_Option_Option_Type.t_option b) - val inv3 (_x : Core_Option_Option_Type.t_option b) : bool + predicate inv3 (_x : Seq.seq b) + val inv3 (_x : Seq.seq b) : bool ensures { result = inv3 _x } - axiom inv3 : forall x : Core_Option_Option_Type.t_option b . inv3 x = true - use C05Map_Map_Type as C05Map_Map_Type - predicate invariant2 (self : borrowed (C05Map_Map_Type.t_map i b f)) - val invariant2 (self : borrowed (C05Map_Map_Type.t_map i b f)) : bool - ensures { result = invariant2 self } - - predicate inv0 (_x : C05Map_Map_Type.t_map i b f) - val inv0 (_x : C05Map_Map_Type.t_map i b f) : bool - ensures { result = inv0 _x } - - predicate inv2 (_x : borrowed (C05Map_Map_Type.t_map i b f)) - val inv2 (_x : borrowed (C05Map_Map_Type.t_map i b f)) : bool - ensures { result = inv2 _x } - - axiom inv2 : forall x : borrowed (C05Map_Map_Type.t_map i b f) . inv2 x = (inv0 ( * x) /\ inv0 ( ^ x)) - predicate invariant1 (self : Seq.seq b) - val invariant1 (self : Seq.seq b) : bool - ensures { result = invariant1 self } - - predicate inv1 (_x : Seq.seq b) - val inv1 (_x : Seq.seq b) : bool - ensures { result = inv1 _x } - - axiom inv1 : forall x : Seq.seq b . inv1 x = true + axiom inv3 : forall x : Seq.seq b . inv3 x = true predicate precondition0 (self : f) (_2 : item0) val precondition0 (self : f) (_2 : item0) : bool ensures { result = precondition0 self _2 } @@ -2026,7 +2002,7 @@ module C05Map_Impl0 use seq.Seq predicate next_precondition0 [#"../05_map.rs" 74 4 74 50] (iter : i) (func : f) = [#"../05_map.rs" 75 8 77 9] forall i : i . forall e : item0 . inv9 i - -> inv8 e -> produces1 iter (Seq.singleton e) i -> precondition0 func (e) + -> inv6 e -> produces1 iter (Seq.singleton e) i -> precondition0 func (e) val next_precondition0 [#"../05_map.rs" 74 4 74 50] (iter : i) (func : f) : bool ensures { result = next_precondition0 iter func } @@ -2041,17 +2017,18 @@ module C05Map_Impl0 predicate preservation0 [#"../05_map.rs" 81 4 81 45] (iter : i) (func : f) = [#"../05_map.rs" 82 8 89 9] forall i : i . forall b : b . forall f : borrowed f . forall e2 : item0 . forall e1 : item0 . forall s : Seq.seq item0 . inv9 i - -> inv6 b - -> inv7 f - -> inv8 e2 - -> inv8 e1 - -> inv4 s + -> inv4 b + -> inv5 f + -> inv6 e2 + -> inv6 e1 + -> inv7 s -> unnest0 func ( * f) -> produces1 iter (Seq.snoc (Seq.snoc s e1) e2) i -> precondition0 ( * f) (e1) -> postcondition_mut0 f (e1) b -> precondition0 ( ^ f) (e2) val preservation0 [#"../05_map.rs" 81 4 81 45] (iter : i) (func : f) : bool ensures { result = preservation0 iter func } + use C05Map_Map_Type as C05Map_Map_Type predicate completed1 [#"../common.rs" 11 4 11 36] (self : borrowed i) val completed1 [#"../common.rs" 11 4 11 36] (self : borrowed i) : bool ensures { result = completed1 self } @@ -2062,18 +2039,41 @@ module C05Map_Impl0 val reinitialize0 [#"../05_map.rs" 93 4 93 29] (_1 : ()) : bool ensures { result = reinitialize0 _1 } - predicate invariant0 [#"../05_map.rs" 131 4 131 30] (self : C05Map_Map_Type.t_map i b f) = + predicate invariant2 [#"../05_map.rs" 131 4 131 30] (self : C05Map_Map_Type.t_map i b f) = [#"../05_map.rs" 133 12 135 57] reinitialize0 () /\ preservation0 (C05Map_Map_Type.map_iter self) (C05Map_Map_Type.map_func self) /\ next_precondition0 (C05Map_Map_Type.map_iter self) (C05Map_Map_Type.map_func self) - val invariant0 [#"../05_map.rs" 131 4 131 30] (self : C05Map_Map_Type.t_map i b f) : bool - ensures { result = invariant0 self } + val invariant2 [#"../05_map.rs" 131 4 131 30] (self : C05Map_Map_Type.t_map i b f) : bool + ensures { result = invariant2 self } - axiom inv0 : forall x : C05Map_Map_Type.t_map i b f . inv0 x - = (invariant0 x + predicate inv2 (_x : C05Map_Map_Type.t_map i b f) + val inv2 (_x : C05Map_Map_Type.t_map i b f) : bool + ensures { result = inv2 _x } + + axiom inv2 : forall x : C05Map_Map_Type.t_map i b f . inv2 x + = (invariant2 x /\ match x with | C05Map_Map_Type.C_Map iter func -> true end) + use Core_Option_Option_Type as Core_Option_Option_Type + predicate invariant1 (self : Core_Option_Option_Type.t_option b) + val invariant1 (self : Core_Option_Option_Type.t_option b) : bool + ensures { result = invariant1 self } + + predicate inv1 (_x : Core_Option_Option_Type.t_option b) + val inv1 (_x : Core_Option_Option_Type.t_option b) : bool + ensures { result = inv1 _x } + + axiom inv1 : forall x : Core_Option_Option_Type.t_option b . inv1 x = true + predicate invariant0 (self : borrowed (C05Map_Map_Type.t_map i b f)) + val invariant0 (self : borrowed (C05Map_Map_Type.t_map i b f)) : bool + ensures { result = invariant0 self } + + predicate inv0 (_x : borrowed (C05Map_Map_Type.t_map i b f)) + val inv0 (_x : borrowed (C05Map_Map_Type.t_map i b f)) : bool + ensures { result = inv0 _x } + + axiom inv0 : forall x : borrowed (C05Map_Map_Type.t_map i b f) . inv0 x = (inv2 ( * x) /\ inv2 ( ^ x)) use seq.Seq use seq.Seq use seq.Seq @@ -2088,10 +2088,10 @@ module C05Map_Impl0 = [#"../05_map.rs" 42 8 53 9] unnest0 (C05Map_Map_Type.map_func self) (C05Map_Map_Type.map_func succ) - /\ (exists s : Seq.seq item0 . inv4 s + /\ (exists s : Seq.seq item0 . inv7 s /\ Seq.length s = Seq.length visited /\ produces1 (C05Map_Map_Type.map_iter self) s (C05Map_Map_Type.map_iter succ) - /\ (exists fs : Seq.seq (borrowed f) . inv5 fs + /\ (exists fs : Seq.seq (borrowed f) . inv8 fs /\ Seq.length fs = Seq.length visited /\ (forall i : int . 1 <= i /\ i < Seq.length fs -> ^ Seq.get fs (i - 1) = * Seq.get fs i) /\ (if Seq.length visited = 0 then @@ -2107,24 +2107,25 @@ module C05Map_Impl0 val produces0 [@inline:trivial] [#"../05_map.rs" 41 4 41 67] (self : C05Map_Map_Type.t_map i b f) (visited : Seq.seq b) (succ : C05Map_Map_Type.t_map i b f) : bool ensures { result = produces0 self visited succ } + use seq.Seq predicate produces_one0 [#"../05_map.rs" 117 4 117 57] (self : C05Map_Map_Type.t_map i b f) (visited : b) (succ : C05Map_Map_Type.t_map i b f) = - [#"../05_map.rs" 118 8 123 9] exists f : borrowed f . inv7 f + [#"../05_map.rs" 118 8 123 9] exists f : borrowed f . inv5 f /\ * f = C05Map_Map_Type.map_func self /\ ^ f = C05Map_Map_Type.map_func succ - /\ (exists e : item0 . inv8 e + /\ (exists e : item0 . inv6 e /\ produces1 (C05Map_Map_Type.map_iter self) (Seq.singleton e) (C05Map_Map_Type.map_iter succ) /\ precondition0 ( * f) (e) /\ postcondition_mut0 f (e) visited) val produces_one0 [#"../05_map.rs" 117 4 117 57] (self : C05Map_Map_Type.t_map i b f) (visited : b) (succ : C05Map_Map_Type.t_map i b f) : bool - requires {[#"../05_map.rs" 117 20 117 24] inv0 self} - requires {[#"../05_map.rs" 117 26 117 33] inv6 visited} - requires {[#"../05_map.rs" 117 38 117 42] inv0 succ} + requires {[#"../05_map.rs" 117 20 117 24] inv2 self} + requires {[#"../05_map.rs" 117 26 117 33] inv4 visited} + requires {[#"../05_map.rs" 117 38 117 42] inv2 succ} ensures { result = produces_one0 self visited succ } - axiom produces_one0_spec : forall self : C05Map_Map_Type.t_map i b f, visited : b, succ : C05Map_Map_Type.t_map i b f . ([#"../05_map.rs" 117 20 117 24] inv0 self) - -> ([#"../05_map.rs" 117 26 117 33] inv6 visited) - -> ([#"../05_map.rs" 117 38 117 42] inv0 succ) + axiom produces_one0_spec : forall self : C05Map_Map_Type.t_map i b f, visited : b, succ : C05Map_Map_Type.t_map i b f . ([#"../05_map.rs" 117 20 117 24] inv2 self) + -> ([#"../05_map.rs" 117 26 117 33] inv4 visited) + -> ([#"../05_map.rs" 117 38 117 42] inv2 succ) -> ([#"../05_map.rs" 116 14 116 68] produces_one0 self visited succ = produces0 self (Seq.singleton visited) succ) predicate completed0 [#"../05_map.rs" 22 4 22 35] (self : borrowed (C05Map_Map_Type.t_map i b f)) = [#"../05_map.rs" 23 8 23 75] completed1 (Borrow.borrow_logic (C05Map_Map_Type.map_iter ( * self)) (C05Map_Map_Type.map_iter ( ^ self)) (Borrow.inherit_id (Borrow.get_id self) 1)) @@ -2132,30 +2133,29 @@ module C05Map_Impl0 val completed0 [#"../05_map.rs" 22 4 22 35] (self : borrowed (C05Map_Map_Type.t_map i b f)) : bool ensures { result = completed0 self } - use seq.Seq - goal produces_trans_refn : [#"../05_map.rs" 36 4 36 90] forall a : C05Map_Map_Type.t_map i b f . forall ab : Seq.seq b . forall b : C05Map_Map_Type.t_map i b f . forall bc : Seq.seq b . forall c : C05Map_Map_Type.t_map i b f . inv0 c - /\ inv1 bc /\ inv0 b /\ inv1 ab /\ inv0 a /\ produces0 b bc c /\ produces0 a ab b - -> inv0 c - /\ inv1 bc - /\ inv0 b - /\ inv1 ab - /\ inv0 a - /\ produces0 b bc c - /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c -> produces0 a (Seq.(++) ab bc) c) - goal next_refn : [#"../05_map.rs" 60 4 60 44] forall self : borrowed (C05Map_Map_Type.t_map i b f) . inv2 self - -> inv2 self - /\ (forall result : Core_Option_Option_Type.t_option b . inv3 result + goal next_refn : [#"../05_map.rs" 60 4 60 44] forall self : borrowed (C05Map_Map_Type.t_map i b f) . inv0 self + -> inv0 self + /\ (forall result : Core_Option_Option_Type.t_option b . inv1 result /\ match result with | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces_one0 ( * self) v ( ^ self) end - -> inv3 result + -> inv1 result /\ match result with | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self) end) - goal produces_refl_refn : [#"../05_map.rs" 29 4 29 26] forall self : C05Map_Map_Type.t_map i b f . inv0 self - -> inv0 self /\ (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) + goal produces_trans_refn : [#"../05_map.rs" 36 4 36 90] forall a : C05Map_Map_Type.t_map i b f . forall ab : Seq.seq b . forall b : C05Map_Map_Type.t_map i b f . forall bc : Seq.seq b . forall c : C05Map_Map_Type.t_map i b f . inv2 c + /\ inv3 bc /\ inv2 b /\ inv3 ab /\ inv2 a /\ produces0 b bc c /\ produces0 a ab b + -> inv2 c + /\ inv3 bc + /\ inv2 b + /\ inv3 ab + /\ inv2 a + /\ produces0 b bc c + /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c -> produces0 a (Seq.(++) ab bc) c) + goal produces_refl_refn : [#"../05_map.rs" 29 4 29 26] forall self : C05Map_Map_Type.t_map i b f . inv2 self + -> inv2 self /\ (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) end module C05Map_Impl2 type i diff --git a/creusot/tests/should_succeed/iterators/05_map/why3session.xml b/creusot/tests/should_succeed/iterators/05_map/why3session.xml index 055719b646..e10768d0fe 100644 --- a/creusot/tests/should_succeed/iterators/05_map/why3session.xml +++ b/creusot/tests/should_succeed/iterators/05_map/why3session.xml @@ -185,12 +185,12 @@ - - - + + + diff --git a/creusot/tests/should_succeed/iterators/05_map/why3shapes.gz b/creusot/tests/should_succeed/iterators/05_map/why3shapes.gz index 0b8348001668ce3510d5e7c73e63cec90370aece..dc7f2848d69103941ba97982f12c3f68b1a9358b 100644 GIT binary patch delta 5374 zcmV*9_$5)-Qrq2e#u;D($W2jX zvB;`AtSa*6U%z{E|Fi!X?%#Y4clXz~H~;=dzxnRpF8uY)XLn*(sbEi(3+BXgL7zk} zsFTbEc~ZF`PC6I($>ai^ED9g*ZpTkUxTllz-+zB1b|QWvaevHxN`X*WYpB++Qsa&d z5u)0^A)KhvYA}*M{POYP?k5?fBWHcVE)Gw*@ORhd;c)p-i+4|Sc3Pze0l&K z%vztw9Q<4VU3yc8JY%w#$Fm-{H$y-dmAf4CT9pE7^f50H#WmXO=}w%TIHue%#`z{= zoaeTgF}#s0jDK-{S%&6RhUTme?J)GGo11VSNr)3y<-<~twSYyPTjmCBN7)j>2z7E? zFCQXfCQhNQ1$UJpdo0YF^F_?FLtBgHS#|u~wZB2F$kT|0`~f9Q@h$%Pcklnxe>@3( z65{f(>QuCr`TOu;T6p`#e|$fEx*1aS`t2g=%KKyz=YNul?D?O53$RKaP!l{&zbtc|L}Ietn}648lwNPH1>a4wHjzmG-*j` zI-C#q_DgGluPegrup0Fw48~emHi>0Z`k*TDOQ^a!%%oz^^_&t=2z7Z_Y&NlR{SfXF z8(6Y+MSn|8KBk5d<>kf0uQP(>V#2UoOemI%3CD6VAz3aaEX&1&X1SQ~EEhAP{Z0(| z^><)MwZDiPRPAprEH>X*Zibh(BWn#Apu%f^zBXhL4Ovt}R@IPYHDs}E$RdNs)y2Dq zVxuQu#L7as{xutO!j3(2i9+?7%_H`+0`b$^d1%q>I753$RZxzWnp*z?Vey_~tR zXl{HlH?YMM%Y3#3R?UsC%#CfD8~cK}akp!3__See++FUi@ETj^Au}LnB2RrfHV9sf zk1ba17OS?4Rhz}C^!;{vVvKFT zMt>KR-oY5v6j*KgEf}M|gfX^ajHwu-pT?Mq%MnOgyfJIMF%@r2bq$8>qWXR)6@95F z1?K&R=g=?3+>iVFi^YQPYavqIFti>m=9f%B_^G8Ztwuo8?6-fvu=4>rN}|juq$N9qShKUI~pBsbQ9l)cRIx zG^}R(c6;gzuORg$v4IVdB{7$LkJ6st*6lY$=T}YB+{MC6m7RD(cGb|n|2~SNHGh^; z)4XD~JErI7){hJjAL5EnXQXr8W8zU@{u=-K>qo5@1y~6D#b3`_u+(0!2TQc0bhd>! zT>N#f`5EDrN^G-pPKH)%9fk6EdS&jrB3?~wOI?}<^*u@BdRHNLd(^kY({l*Kc%h-t zye1NO-&XN25cq<&x4n|i%ky=tntv}F7xUQ?Iy@osJq_B@pTpMZF<^Y8uc%COQIAx< zBA9CY&wcYbJTkdG?_b8jR*SCAq^5SFfQ_E};>yh*&21$owF(8~a|MK^zh5$GJOuws z5FpRf1W6sU5cJh%l)PU36e$1yy1&Z0Z^mC+d(+{`ZSHWkEq+DTYLVqPCx5Q|e%9(- zjJt`er^KjULX0nvvN{*zPS(n=QdYy$8o|G8iP0@w;{Mr@<~t%=H{bW9bIY|Sx(JJ} zghfwB4`}oa(ZgXi2Ase}K#zRI6c=OxiIsp>fj|}wZHuOlk&2blRpOXEvg8!#v|9=A5doKGO1oqEB z;B(n;;_#mA{Sp%H)*l~f#_^H%l*F??)^uR0=#MpFc$_ncZI+g8XKC5Vo?OY%vXeQ~ zobgVI*2L!J06hQePPSx4O`Dvhnvyn6f!9Ktjm=r;wj*x|$(ngKIrF?EXGz6*sd^l5 z3OglR%+sf>DVHqsI)BY=Q&K&qlxs3rHz!XU$JX`y%eEQxlxa@=TGDgIxoId$TD>Hf zV=8$`{d2kG{<&&8#uKT?XgrN}?dfyPP`gr7j1OFXydh&NftGYW=bArUs_b!kCjd6=yQ~2kKj6g-aYeL z28u*h6RBusE)!Ztw`;XV*`imq>C7wxm%e=FoX$buPd%sRNba~&v15~f2PA(#nU~vm zEHfY$M2^RJWm!n>otjZ|5;zxhi?%JEsz-?p!P~nJ+3>uB%~^y$`uHg`$Fd!$me@QO{J;8Y$~C0 zCMSK=)OyHLVC$}c**=KewWe6M4^uO388gP2Ca(p`ciK`GWu}$s+}sZ351OG%&TsFG zH#d$+nP%|c(Kq>IEN&*;9(TE0x61Za@6nabi|Xbj;}(SfF8odS?cx0zUJ}_KeL9&B z_u=l7dk7zY&z3>PJ7)Or_-w5?Zf%@f2A0+FF-nGG(dA>&?PH_v1>*Pum=SNTmOBr8 zx$_{FI}dV!*Y!=C_M(kG>4Lj@0mpdaPTMyOBh0achzT6|DPJ&z%g1-HvD|2=7YfQ+ z&v!RLp+z)Ny-D5_WP_`%Q`#b>Sh=PNIcFzyefyAq;_bubhJ%|KvekRtzJ5q1`;p83 z#M!bz@p7Y3m)n`C81GoME3zSgW&lSpCMrj2v^hp^c#I%XHf&c>QMJhJqdhic}EuI1vXnBC&< z{QD;T^xa&4J;o2$H$R8F>xcJvL*N|$iQfmxJrj;3i}b(w-%@3)LhyKdcX#`@F#gLg z|5LvI7^(e6e!9N#A9BY+ta$XXLD`;AXxHz5;+-FEe*v(<1*1sj-TS{nOwDxD9F}>? zObzY+>-Lv$^6y320At}T{uT-s4}bp{-pnx4_*JDxUL~44MRNW(9^XIvd%V17EzSJ7 zyi={Xod>7Y2y`Aq%)t9yS;fy6{vH~Z)*#Y!(5=6fJ!U2a!mh}X_#+xslK8YON*efo zB1@{mgs4=NCf|@I8vK}uF5;vrPbw}=YLNIQ5vOt<;J#CI^fAe z*twMD#4o0cPd9hL4?p|Ogi`Tw^dRod^Jw!HBJ;- z89fe9fLY8NKL)e2wQr$|)dnl3(uPx7pCpri3mF(Bp;@^_A|CVKQLW=l&aDHilz1@~ zs^m_SunQFeoivlj3nG8lBmQ14(n!;I8_6qmnau#D$7XZqHWff;)@#KtFBkn!%Z<;h7y#bu*ZNJmleCvrD0XE65hWg*K&)L% zKu0%O%0(p#F_x;+2xiLw@G+WCS#Orso2}NHrOs$2>UvADwcdYhD1JCTFK$Src6ESq zCH>KM`QgyX)Hu(uLoF=InA%$we>-DQ;8(@PvfH76F(*s0*`YYlmP#yO%;S_)YMn@9 zP`Wx+%`_%evJK5NHhnKErEOdYZLgY@ij#XANgI82%qwN|#!6{hHPbAqtBcdSH`DFi zo9J||@iL|MYkmtu&5vQI`85o!LrZF7ON3;)L_gI0 zRAz~wsEMGSlXaSdo%y#WtY)1|%{sA{$~rAK!A1HB#oK=vDdl;V!0No_s%G0VcE@P# za2DyLb`j04Z?N+I!}b3{<2K!ZbT+V_iEZN%-lQ$~ax8FlRn;15zGMqnlP#bnTfmoW zfmq}&7qP2F>Ut5nS(34KC4SdPAA$X^bAVsvP31?T(eg=@?Fk`yJ*9|h)=ZgNyiM89 z^Kdhz0os31za9=P$%CtvClSN{4P-}cGg3;Pni<*27PKULe1cYW83+o=cBxzy1)-{H zw2sNqD;|Z}`m>3>FIR`vr<|Wy)w%kE(7YJcGby~xKM;jAuu^kA-U|`E%K60AOv$vN?6~MSzfcsU?>*;YG^3G%t7)R%_LH()`Y7bdq<`E$V201YP0wb#41T!%mG_!*k zhspKYsL=~Kkd!>c5sm8%L~S~wJEJ-yJ0m*7J42meopznJorWgpPGb>dr$wj18@+!3 zdz=^xB(?L(x)9B4^gsZxrUuVs5dpm#e}2+Km^2#|8)a{J?*};rQm7APL=hN!HU7ll zJWW!L9A+(~5zrdVb#ErAN6{zo+Sg-GYp;mND`Bu~1E)YF!{oV^u2&{OynQ|CnqeIK zAXPsqFD&bo=T5m{ghybR>nX9vUyXk~30^2zMgz71E|gaqt0+aUwKAqp8-sg2+trGb z9`z`#f_&X1dVvLv86nbY7?SNe`+CA9YeyRZ>lUlVhH3Ivc^wqi&J200vf|a)8=MQh zvJBA?HyoY{8~7-c8oBmX`^=tvHTJMG5lxfsVGP*d$w)XPaMoBaxRrept~Gz1)tyzZ z#^f|8h|~?rhavQ%?gt^A9w)AbX&i_rCgH}so)UVlWN=bU+K+MPknk;xl_Dq+{16g8 zJL=pkLbRHk)>3okl(KLOV8<3KXokrOMLu!JUz0=l)?D(w$5z6$b}UFf86|oy;5to| z_F$(vCp-6w=Ir4*4#L8@!|s1E1wV1G$05Lzv~J42q|>j=By%)su!FdZYZrp^3}S~? zde52Ec_qy&Gua0gIYgW?^boUw&3FU`&_-u%U^&DPF-}3063a0*ieXHQV`3l^BbgY= z#8@T;GiZl!X4^g)qEx3w_?r$ON8{v~mqQO<4-q40c`y(_{6+}i2oZlAA%w&F;lV(N z;^Npm^21+-C%`Qt0&cL2T1(b=JvcUb4X+(=$8_e2XTDx|?4IBXky8i~yms7%-jjtF z0+@v;RQMyuo&?M}AOM!*G%(2(*A`<9hJr%8nF4Hrt`YQypg;&4@Wik+)?ok;BTyq5 zc?2T@?P91OqjJRL2v&bDxOI@OU}CTXAudMf9)bxDP&dNEw=Xfq&@0w+6^yY=B8nY? zfZ3VJ;g2X82!fpu4257R1XCduBXIPGwIscQ$;5Sp*%0i8U^oQJ`8{kYF+r|Y2e{(! zJq*|A*^|TyU`O&5pVXjLLAt`G|oH;?DqQ7Qrc`!QFp=7$$2N;N%~`iuSyB zgQQ+yb77>hqc}N9C%7|k&mgFnvWXTCABSwT^vDAU+o=5@jL4Zx%%FfUkdgqE@RabN z9ncbhf+x-g?SPo1W2y!1w7LjZh+a8~I71;uf)7Z81MH1b0DKVn5-^ys^Ah|6!uAV0 z#1ol`*(?2rFy()2-~!mgoSXXKpss?O-~o%$3>xtoVS4~P;L+t@`443fxDfMuCRp#i zaE^w^rN+K6_BJS97(_=z9`c-cK3Fj#xQ3@b#{b7mnV9*f zoSZjC^?^?#%mSiQQfVVY&$$Ew%f3#|{?ks-_0l`9p^`Czf=6SqqevPMsKmSyWy6QR z#8U#^{nLLZbO(Om^TreHtjcBGR?wavfgD2>HRY`c^Z3ytBM-;rp7ONqg zL79H+6(Nv_2Ql#^COPqc@WzFm-g0cK3eL0)GzAlnj;0WTRNPc%%s-4F1273(57LOi zPlm8NX$>!1J4D&NaBsMbXH?KRcvFBRJP;+kDL8*gc%YZ?rZ~JQ4sVK!c$kHD2n{$w z10KUAcvzMNKKj5}Z@ioMgs4t17bF|P7y-TAntc=PK?Ekfm0HncdCw*| ciNqF16No_;ln>7|eG~2f13zfP5RO>@03Usd2LJ#7 delta 5368 zcmVDDlxWWcWif0W`F%2eo555Qrq2e#u;D($W2jX zvB;`AtSa*6U%z|v@U#CI9^QNo_YXIBxBvb|zxnRpF8s~yXLn>*sbG(k3+BjkK_5jf zsH4mUc~rR|jyf0k(c}UhEeap+@5WCcRSuZVhP^=^63$D zFl&7zbMSBdcj-+X@{Gw|UZ3>1yBz|$sNCf`uT?3aMqlS8qPRwzJ>8MBBgd2*#yH<( zjPu+!Gln;Eg?};5FU!!J%FvwEp&f?)bbA{fA_;Nis(e@qvKFwYbIaVI?I>G97@*Yga%)}|wwcxHYWUmXe=5!JB?9kStc~%{Nf8%daEAljAA%8##Q+$iR{@wfk^dFCc zABDI)tU48~W&R<2m=@lC@gLt$pKga#y?(n$y7E4m#DA%zB76R)@OTvJD0D8#QYtzo zG$eK(<~~@5tsaLRR+`4w{)gD*L%99v@#jqa;D2~KU{?C-a0Ai*SQ`7ktXd7UCYrRQ zG#yR{eEX%fz}FRFc36#i6b550ESto#DSc3t_$5?b9cEIo=Xy>FD1^E^EH<0ixOois zi482-x__djCeNv1M0t7f`0I>dxtK647ZZx*V#2XpOh}fC3CnUZp;;~_Jj=z5XulIf ze*GO7QtdC|237l;3yaM+mYdW<`c8gWp#j4F>)q1gNwOF-WtXeEq&7bsBWG(ROr^xE3@am_?m+@2N@AXskGcm?C zV1J{FN$+5cY6`42{T7T-U&0t$F~(Gk(NAMc#pMVjE#8KM;eQg8*dA^t<}zB(g?`w>?330TfYP@O*Ld9z z3s`Rm%Qr--u&9;ROelWe5SRBW;mz`*mB3b1mUX8UcE^fS@Q!s0dar~=i_|d7MrwU4 zH5yj4eY-vNg;$XJlGwn8$dZ^#zDH?KaO?IPqVub!Y3^d-rOHk`A-ig5-+v#)(SI6C zscBv@+a1&MbL%q$#D}=z(+TNZcTPMC%-`T&e{#tRLF z<~5PP`?iXIfxs8Ez3r8BUY@RF)qi~1xR}qD(BTQ0?`hDM{v5VOj{)PEzM?YCMV+a9 zMKIO)pZn%>I5W9D?_b8jR*SAqq^5SFfQ_E};>yj>=C+cPT7?4gxdKAd-!GXo9)kZR z2#}{~f~1aF2>NO>N?xyi3Y7nU-Ct$hH{-9Zz3K4eHg`DL7QZ5EwaD_D6Mt8JKWlX= z#@)o#Q({yvA;uR-S)Gb;Cu`+bDXZaWjo@Fl#OM|-asTW{^Bs|`o9}zlx#ijuU4+F~ z!lI|62Q>PI=;5#$15V%~pfg`F#RXYFVkMweAdp2v+oI`Xq_iy>c0#12NuCJ(zQWkz z;D3afEgtl)f$hZ(&or%*(0}1&jViM973S1$no}XdGqgSt0q)7n9c3xmQd$5~vK`5- zJAFxVv1MEv$#wuzvX%VY^8wPm1VCcEqohTa;5WtDlIHbxMV69QvUGa@>2@V*cdXFv z0i=CGu0xwcOaZ~F#wTiDg|W-#_{~V`_mTE=bKJ$-r)2-E;QuMvzkdMsp2~g)f&DWO z_*C|rIJ_r&zl4Ol_19;baebyeCGqU9YdWx0^w%|Ecs*wj+bk{H&eF1@J-U*kWk++U zIpduat%=Rc0eJq`9c{^qnl?F0H6?AD0R_~_wPRkeNo&U}TYJzgN?Kcp`NaFvP&3<~ZysQ4W67RPIc!&Sb~Y2CpslR^v3{F* zv~*1KaC7_9hwylJ>qGM;bv*^l$!{O1qkiG=

NjUs_b!=gKB@^f^kiGq}#5ch9_* zfg+LBL@Jt@%Y>HE?OLr-w&+!DIy1|_r7xd3r&AF4Q_rb6lDl51*maYD2PA(znU~vm zEHfY$M2^RJWm!n>otjZ|5;zxhi?%JEs{`PgdU}J8db8GSkX*ZtsTj2hGqW=eKvp zn;XZZOf&fJ=$m{p7B>@auXnjyx61Za@6nabi|Xbj;}(SfF8poy?eYB@UJ}_KeL9&B z58?ikdk7zYPnJQ(J7)Or`q^4@y|r;}8CX`wbCe9%MVGIOZeKU*ULcMyfEn@TYPs{k zmpcz)x$__wcwOJLX)oI7qb|6s7jTRx?zDZwFv1*5h?u~UAM*u6xO{vE8_SJ`dZD1K z^?Y{|6k0?R)tlr^K{mMBI;AaAij`}ckaKoI*S8OUDc(L@ZaBD^AzQuI?dykRvLCtZ zPn<0q6fZXlb-A6Hit!F+^(T4bPm1PN!U^`Ngta<*ht+Q^JkCBPtI$ZS0x?TK+=6H& z(Gt%N=Gwbt)w^sjQa)Cy3**21 z@;~MKkCEDMoQ#EM5B8@w4KNno;%}jF@%ZMx2i^Kx*<)r>Anb}9iJ#G^lEkNNQPRMF z7gt^C(g9B% z!p@~ECw?(qe7e04e)!qUWhephYRyv0&w9;`QlZ5)7 z=!6t+Nby6OHu<|lX7p}rADSn0cc`msbZD0Du)qFC`K9%*dt?=Arq2CcDxuXK?JGmh zyxq~6CLLOZJDjTHY4~=o%d6F;d3iH;jkWMqQ#NgVgW}b6E)db zz~#OPpfe`YETbw)n+l*a>$T#Smy78iyIQDT^*oY zNq@9memHbAHO@2aPz#GPruLS_-_BSR_*HSS>~<(%%+XS8b|?|raGmS}=Y(q1RP2bB(X&V{a}d7wRahBhBmY&Mt3S2O!VdLa5CNt z5xq*8x|J(~xoqrSsBKm=C5X+udzB$XOoKc@tGY#)0cX2ZuIf2vMK&_0k|@7wG1uGG zSMxGdS%Sia@0B1mk~G?A=E7*mhH>Np-Zg2)-f(}`3EK(P3E2tJ3Em0nh;^BE?)nvTAju(L)>a>07Td0-Tb z9tPo<9mOLeDn^&N4;MW85Vh%y?u_b;?2PCP?+kT@b=q~>b{d+XJB>wq0cI(E|a%ni@QlMFjL}{P{@_VbW|=Y?Qs>y&vQhNTEKE5k+9^)%X*G^E630 za+tM{MnG#c*S(pf9z~zTYhRB&t-T^5uY|#}4V(gz43pjuBXHve>L_bc%gq_84cJ5xKLhctfCaX*2Y!y<#kY4J2T|1%8FNGZ*VU3$}&Vp z+;Dg*Y~Z6%YUJ8m?K6Aw)!4(%L^MshhcRG-CnMpIz*%Fx;8ylYxYl%5cUFJB8k5tY zAW}CdABND6x*vpedYrf#rg0#in1mbidP?ZIlEFzaX+OrDL&CQ(R*IlR@Iy%W?5K0E z2+?YCT1(BDQ_8|EfE`<`pcy7B6#2v0O z$Pa%Ro&dLq2)My6YAspg_2Ag#HN1Af9n+a7p80y=v3r6mL{1?{@Y-=3dQTQ!2w)bX zP~ndpdlE3`fB;yI)4(KGTw9Da7zzsUW(u$gx<=3+f&w9Iz!SsPScd^Xj6jWK zhd-iZAP9CsFcgBN5KM(sjKI+!){^uJCKJ~YW<#(Wg5eM>=l8Is#00ro9pH+?_b^pdT(jyNbY@_yrFd}C%F@plaKuQ8s!c)S7c0fx2 z3Z6J0v;$(2j;R*3)9NBvA$sK`;tYit2|geV4zM>$0q{ZOOTb{l&P(tQ2-`305Km+# zX0P-g!j!Xt3t)c_b8hN`gSrZCf(I;0GibzXgzW+FfJc{qZJe7|yuGV)kNC*j1D%jAGNpBk*uMgonKfvrLFF zc*Gu9Sq;RUz^l>#Nv`Y!sDMpIW;Gu5r(s(2USqcac#(eyj>G420o$`>8k#`fB?Cf) ziU&+%6XF!#!8A4@j!g(!j>rD#CI)9Wr~ns|uro<(_+Z6|;2NI#82=wLWn$)^a&q1n z)dxO}FbjxINu`YpJ?9b#Ec-e+`%gPT*GuobhDyc=3LcHcjv{G5pc3;+lno#L5>E+u z_fI!L9&>+VPP5T!H;MSyaKUtlH=>!QxNF8^4W6L)RVCqtw;{lj9#QZXTdam~24(uO zSA;+!9>m0xnB>I&!5bHLddsn`Dmc?J&=gEOI+{WVQgKt6G5;`z48SCCJxC)4KN-UA zq&2*3?GR=6!oA@#o>4*P;7tLN@IaLCrr;#ufnI;Yo8s`MIJ_w?;$arrAvE9!4R{Qf z;9*4r2%^`M<7zZk7{hzG;A4Ob*H3+Ng*n_{>@#>kPsO7#(1X**;qV~_zyo^l_Bgyf z4sVac+v8GSI5mI`A*7YYPjVP&mbrh9SpWe30+E0K diff --git a/creusot/tests/should_succeed/iterators/06_map_precond.mlcfg b/creusot/tests/should_succeed/iterators/06_map_precond.mlcfg index 519ff46029..2dbea35128 100644 --- a/creusot/tests/should_succeed/iterators/06_map_precond.mlcfg +++ b/creusot/tests/should_succeed/iterators/06_map_precond.mlcfg @@ -3568,84 +3568,60 @@ module C06MapPrecond_Impl0 ensures { result = inv9 _x } axiom inv9 : forall x : i . inv9 x = true - predicate invariant8 (self : item0) - val invariant8 (self : item0) : bool + predicate invariant8 (self : Seq.seq (borrowed f)) + val invariant8 (self : Seq.seq (borrowed f)) : bool ensures { result = invariant8 self } - predicate inv8 (_x : item0) - val inv8 (_x : item0) : bool + predicate inv8 (_x : Seq.seq (borrowed f)) + val inv8 (_x : Seq.seq (borrowed f)) : bool ensures { result = inv8 _x } - axiom inv8 : forall x : item0 . inv8 x = true - predicate invariant7 (self : borrowed f) - val invariant7 (self : borrowed f) : bool + axiom inv8 : forall x : Seq.seq (borrowed f) . inv8 x = true + predicate invariant7 (self : Seq.seq item0) + val invariant7 (self : Seq.seq item0) : bool ensures { result = invariant7 self } - predicate inv7 (_x : borrowed f) - val inv7 (_x : borrowed f) : bool + predicate inv7 (_x : Seq.seq item0) + val inv7 (_x : Seq.seq item0) : bool ensures { result = inv7 _x } - axiom inv7 : forall x : borrowed f . inv7 x = true - predicate invariant6 (self : b) - val invariant6 (self : b) : bool + axiom inv7 : forall x : Seq.seq item0 . inv7 x = true + predicate invariant6 (self : item0) + val invariant6 (self : item0) : bool ensures { result = invariant6 self } - predicate inv6 (_x : b) - val inv6 (_x : b) : bool + predicate inv6 (_x : item0) + val inv6 (_x : item0) : bool ensures { result = inv6 _x } - axiom inv6 : forall x : b . inv6 x = true - predicate invariant5 (self : Seq.seq (borrowed f)) - val invariant5 (self : Seq.seq (borrowed f)) : bool + axiom inv6 : forall x : item0 . inv6 x = true + predicate invariant5 (self : borrowed f) + val invariant5 (self : borrowed f) : bool ensures { result = invariant5 self } - predicate inv5 (_x : Seq.seq (borrowed f)) - val inv5 (_x : Seq.seq (borrowed f)) : bool + predicate inv5 (_x : borrowed f) + val inv5 (_x : borrowed f) : bool ensures { result = inv5 _x } - axiom inv5 : forall x : Seq.seq (borrowed f) . inv5 x = true - predicate invariant4 (self : Seq.seq item0) - val invariant4 (self : Seq.seq item0) : bool + axiom inv5 : forall x : borrowed f . inv5 x = true + predicate invariant4 (self : b) + val invariant4 (self : b) : bool ensures { result = invariant4 self } - predicate inv4 (_x : Seq.seq item0) - val inv4 (_x : Seq.seq item0) : bool + predicate inv4 (_x : b) + val inv4 (_x : b) : bool ensures { result = inv4 _x } - axiom inv4 : forall x : Seq.seq item0 . inv4 x = true - use Core_Option_Option_Type as Core_Option_Option_Type - predicate invariant3 (self : Core_Option_Option_Type.t_option b) - val invariant3 (self : Core_Option_Option_Type.t_option b) : bool + axiom inv4 : forall x : b . inv4 x = true + predicate invariant3 (self : Seq.seq b) + val invariant3 (self : Seq.seq b) : bool ensures { result = invariant3 self } - predicate inv3 (_x : Core_Option_Option_Type.t_option b) - val inv3 (_x : Core_Option_Option_Type.t_option b) : bool + predicate inv3 (_x : Seq.seq b) + val inv3 (_x : Seq.seq b) : bool ensures { result = inv3 _x } - axiom inv3 : forall x : Core_Option_Option_Type.t_option b . inv3 x = true - use C06MapPrecond_Map_Type as C06MapPrecond_Map_Type - predicate invariant2 (self : borrowed (C06MapPrecond_Map_Type.t_map i b f item0)) - val invariant2 (self : borrowed (C06MapPrecond_Map_Type.t_map i b f item0)) : bool - ensures { result = invariant2 self } - - predicate inv0 (_x : C06MapPrecond_Map_Type.t_map i b f item0) - val inv0 (_x : C06MapPrecond_Map_Type.t_map i b f item0) : bool - ensures { result = inv0 _x } - - predicate inv2 (_x : borrowed (C06MapPrecond_Map_Type.t_map i b f item0)) - val inv2 (_x : borrowed (C06MapPrecond_Map_Type.t_map i b f item0)) : bool - ensures { result = inv2 _x } - - axiom inv2 : forall x : borrowed (C06MapPrecond_Map_Type.t_map i b f item0) . inv2 x = (inv0 ( * x) /\ inv0 ( ^ x)) - predicate invariant1 (self : Seq.seq b) - val invariant1 (self : Seq.seq b) : bool - ensures { result = invariant1 self } - - predicate inv1 (_x : Seq.seq b) - val inv1 (_x : Seq.seq b) : bool - ensures { result = inv1 _x } - - axiom inv1 : forall x : Seq.seq b . inv1 x = true + axiom inv3 : forall x : Seq.seq b . inv3 x = true predicate precondition0 (self : f) (_2 : (item0, Snapshot.snap_ty (Seq.seq item0))) val precondition0 (self : f) (_2 : (item0, Snapshot.snap_ty (Seq.seq item0))) : bool ensures { result = precondition0 self _2 } @@ -3658,7 +3634,7 @@ module C06MapPrecond_Impl0 use seq.Seq predicate next_precondition0 [#"../06_map_precond.rs" 83 4 83 74] (iter : i) (func : f) (produced : Seq.seq item0) = [#"../06_map_precond.rs" 84 8 88 9] forall i : i . forall e : item0 . inv9 i - -> inv8 e -> produces1 iter (Seq.singleton e) i -> precondition0 func (e, Snapshot.new produced) + -> inv6 e -> produces1 iter (Seq.singleton e) i -> precondition0 func (e, Snapshot.new produced) val next_precondition0 [#"../06_map_precond.rs" 83 4 83 74] (iter : i) (func : f) (produced : Seq.seq item0) : bool ensures { result = next_precondition0 iter func produced } @@ -3674,11 +3650,11 @@ module C06MapPrecond_Impl0 predicate preservation0 [#"../06_map_precond.rs" 105 4 105 45] (iter : i) (func : f) = [#"../06_map_precond.rs" 106 8 113 9] forall i : i . forall b : b . forall f : borrowed f . forall e2 : item0 . forall e1 : item0 . forall s : Seq.seq item0 . inv9 i - -> inv6 b - -> inv7 f - -> inv8 e2 - -> inv8 e1 - -> inv4 s + -> inv4 b + -> inv5 f + -> inv6 e2 + -> inv6 e1 + -> inv7 s -> unnest0 func ( * f) -> produces1 iter (Seq.snoc (Seq.snoc s e1) e2) i -> precondition0 ( * f) (e1, Snapshot.new s) @@ -3689,11 +3665,11 @@ module C06MapPrecond_Impl0 use seq.Seq predicate preservation_inv0 [#"../06_map_precond.rs" 93 4 93 73] (iter : i) (func : f) (produced : Seq.seq item0) = [#"../06_map_precond.rs" 94 8 101 9] forall i : i . forall b : b . forall f : borrowed f . forall e2 : item0 . forall e1 : item0 . forall s : Seq.seq item0 . inv9 i - -> inv6 b - -> inv7 f - -> inv8 e2 - -> inv8 e1 - -> inv4 s + -> inv4 b + -> inv5 f + -> inv6 e2 + -> inv6 e1 + -> inv7 s -> unnest0 func ( * f) -> produces1 iter (Seq.snoc (Seq.snoc s e1) e2) i -> precondition0 ( * f) (e1, Snapshot.new (Seq.(++) produced s)) @@ -3702,15 +3678,16 @@ module C06MapPrecond_Impl0 val preservation_inv0 [#"../06_map_precond.rs" 93 4 93 73] (iter : i) (func : f) (produced : Seq.seq item0) : bool requires {[#"../06_map_precond.rs" 93 24 93 28] inv9 iter} requires {[#"../06_map_precond.rs" 93 33 93 37] inv10 func} - requires {[#"../06_map_precond.rs" 93 42 93 50] inv4 produced} + requires {[#"../06_map_precond.rs" 93 42 93 50] inv7 produced} ensures { result = preservation_inv0 iter func produced } axiom preservation_inv0_spec : forall iter : i, func : f, produced : Seq.seq item0 . ([#"../06_map_precond.rs" 93 24 93 28] inv9 iter) -> ([#"../06_map_precond.rs" 93 33 93 37] inv10 func) - -> ([#"../06_map_precond.rs" 93 42 93 50] inv4 produced) + -> ([#"../06_map_precond.rs" 93 42 93 50] inv7 produced) -> ([#"../06_map_precond.rs" 92 4 92 83] produced = Seq.empty -> preservation_inv0 iter func produced = preservation0 iter func) use prelude.Snapshot + use C06MapPrecond_Map_Type as C06MapPrecond_Map_Type predicate completed1 [#"../common.rs" 11 4 11 36] (self : borrowed i) val completed1 [#"../common.rs" 11 4 11 36] (self : borrowed i) : bool ensures { result = completed1 self } @@ -3722,38 +3699,63 @@ module C06MapPrecond_Impl0 val reinitialize0 [#"../06_map_precond.rs" 117 4 117 29] (_1 : ()) : bool ensures { result = reinitialize0 _1 } - predicate invariant0 [#"../06_map_precond.rs" 157 4 157 30] (self : C06MapPrecond_Map_Type.t_map i b f item0) = + predicate invariant2 [#"../06_map_precond.rs" 157 4 157 30] (self : C06MapPrecond_Map_Type.t_map i b f item0) = [#"../06_map_precond.rs" 159 12 161 73] reinitialize0 () /\ preservation_inv0 (C06MapPrecond_Map_Type.map_iter self) (C06MapPrecond_Map_Type.map_func self) (Snapshot.inner (C06MapPrecond_Map_Type.map_produced self)) /\ next_precondition0 (C06MapPrecond_Map_Type.map_iter self) (C06MapPrecond_Map_Type.map_func self) (Snapshot.inner (C06MapPrecond_Map_Type.map_produced self)) - val invariant0 [#"../06_map_precond.rs" 157 4 157 30] (self : C06MapPrecond_Map_Type.t_map i b f item0) : bool - ensures { result = invariant0 self } + val invariant2 [#"../06_map_precond.rs" 157 4 157 30] (self : C06MapPrecond_Map_Type.t_map i b f item0) : bool + ensures { result = invariant2 self } - axiom inv0 : forall x : C06MapPrecond_Map_Type.t_map i b f item0 . inv0 x - = (invariant0 x + predicate inv2 (_x : C06MapPrecond_Map_Type.t_map i b f item0) + val inv2 (_x : C06MapPrecond_Map_Type.t_map i b f item0) : bool + ensures { result = inv2 _x } + + axiom inv2 : forall x : C06MapPrecond_Map_Type.t_map i b f item0 . inv2 x + = (invariant2 x /\ match x with | C06MapPrecond_Map_Type.C_Map iter func produced -> true end) + use Core_Option_Option_Type as Core_Option_Option_Type + predicate invariant1 (self : Core_Option_Option_Type.t_option b) + val invariant1 (self : Core_Option_Option_Type.t_option b) : bool + ensures { result = invariant1 self } + + predicate inv1 (_x : Core_Option_Option_Type.t_option b) + val inv1 (_x : Core_Option_Option_Type.t_option b) : bool + ensures { result = inv1 _x } + + axiom inv1 : forall x : Core_Option_Option_Type.t_option b . inv1 x = true + predicate invariant0 (self : borrowed (C06MapPrecond_Map_Type.t_map i b f item0)) + val invariant0 (self : borrowed (C06MapPrecond_Map_Type.t_map i b f item0)) : bool + ensures { result = invariant0 self } + + predicate inv0 (_x : borrowed (C06MapPrecond_Map_Type.t_map i b f item0)) + val inv0 (_x : borrowed (C06MapPrecond_Map_Type.t_map i b f item0)) : bool + ensures { result = inv0 _x } + + axiom inv0 : forall x : borrowed (C06MapPrecond_Map_Type.t_map i b f item0) . inv0 x = (inv2 ( * x) /\ inv2 ( ^ x)) + use seq.Seq + use seq.Seq use seq.Seq - use prelude.Snapshot use seq.Seq use seq_ext.SeqExt use seq.Seq use seq.Seq use prelude.Int use seq.Seq + use prelude.Snapshot use seq.Seq use seq.Seq predicate produces0 [@inline:trivial] [#"../06_map_precond.rs" 43 4 43 67] (self : C06MapPrecond_Map_Type.t_map i b f item0) (visited : Seq.seq b) (succ : C06MapPrecond_Map_Type.t_map i b f item0) = [#"../06_map_precond.rs" 44 8 56 9] unnest0 (C06MapPrecond_Map_Type.map_func self) (C06MapPrecond_Map_Type.map_func succ) - /\ (exists s : Seq.seq item0 . inv4 s + /\ (exists s : Seq.seq item0 . inv7 s /\ Seq.length s = Seq.length visited /\ produces1 (C06MapPrecond_Map_Type.map_iter self) s (C06MapPrecond_Map_Type.map_iter succ) /\ Snapshot.inner (C06MapPrecond_Map_Type.map_produced succ) = Seq.(++) (Snapshot.inner (C06MapPrecond_Map_Type.map_produced self)) s - /\ (exists fs : Seq.seq (borrowed f) . inv5 fs + /\ (exists fs : Seq.seq (borrowed f) . inv8 fs /\ Seq.length fs = Seq.length visited /\ (forall i : int . 1 <= i /\ i < Seq.length fs -> ^ Seq.get fs (i - 1) = * Seq.get fs i) /\ (if Seq.length visited = 0 then @@ -3769,27 +3771,28 @@ module C06MapPrecond_Impl0 val produces0 [@inline:trivial] [#"../06_map_precond.rs" 43 4 43 67] (self : C06MapPrecond_Map_Type.t_map i b f item0) (visited : Seq.seq b) (succ : C06MapPrecond_Map_Type.t_map i b f item0) : bool ensures { result = produces0 self visited succ } + use seq.Seq predicate produces_one0 [#"../06_map_precond.rs" 142 4 142 57] (self : C06MapPrecond_Map_Type.t_map i b f item0) (visited : b) (succ : C06MapPrecond_Map_Type.t_map i b f item0) = - [#"../06_map_precond.rs" 143 8 149 9] exists f : borrowed f . inv7 f + [#"../06_map_precond.rs" 143 8 149 9] exists f : borrowed f . inv5 f /\ * f = C06MapPrecond_Map_Type.map_func self /\ ^ f = C06MapPrecond_Map_Type.map_func succ - /\ (exists e : item0 . inv8 e + /\ (exists e : item0 . inv6 e /\ produces1 (C06MapPrecond_Map_Type.map_iter self) (Seq.singleton e) (C06MapPrecond_Map_Type.map_iter succ) /\ Snapshot.inner (C06MapPrecond_Map_Type.map_produced succ) = Seq.snoc (Snapshot.inner (C06MapPrecond_Map_Type.map_produced self)) e /\ precondition0 ( * f) (e, C06MapPrecond_Map_Type.map_produced self) /\ postcondition_mut0 f (e, C06MapPrecond_Map_Type.map_produced self) visited) val produces_one0 [#"../06_map_precond.rs" 142 4 142 57] (self : C06MapPrecond_Map_Type.t_map i b f item0) (visited : b) (succ : C06MapPrecond_Map_Type.t_map i b f item0) : bool - requires {[#"../06_map_precond.rs" 142 20 142 24] inv0 self} - requires {[#"../06_map_precond.rs" 142 26 142 33] inv6 visited} - requires {[#"../06_map_precond.rs" 142 38 142 42] inv0 succ} + requires {[#"../06_map_precond.rs" 142 20 142 24] inv2 self} + requires {[#"../06_map_precond.rs" 142 26 142 33] inv4 visited} + requires {[#"../06_map_precond.rs" 142 38 142 42] inv2 succ} ensures { result = produces_one0 self visited succ } - axiom produces_one0_spec : forall self : C06MapPrecond_Map_Type.t_map i b f item0, visited : b, succ : C06MapPrecond_Map_Type.t_map i b f item0 . ([#"../06_map_precond.rs" 142 20 142 24] inv0 self) - -> ([#"../06_map_precond.rs" 142 26 142 33] inv6 visited) - -> ([#"../06_map_precond.rs" 142 38 142 42] inv0 succ) + axiom produces_one0_spec : forall self : C06MapPrecond_Map_Type.t_map i b f item0, visited : b, succ : C06MapPrecond_Map_Type.t_map i b f item0 . ([#"../06_map_precond.rs" 142 20 142 24] inv2 self) + -> ([#"../06_map_precond.rs" 142 26 142 33] inv4 visited) + -> ([#"../06_map_precond.rs" 142 38 142 42] inv2 succ) -> ([#"../06_map_precond.rs" 141 14 141 68] produces_one0 self visited succ = produces0 self (Seq.singleton visited) succ) predicate completed0 [#"../06_map_precond.rs" 21 4 21 35] (self : borrowed (C06MapPrecond_Map_Type.t_map i b f item0)) @@ -3800,32 +3803,29 @@ module C06MapPrecond_Impl0 val completed0 [#"../06_map_precond.rs" 21 4 21 35] (self : borrowed (C06MapPrecond_Map_Type.t_map i b f item0)) : bool ensures { result = completed0 self } - use seq.Seq - use seq.Seq - use seq.Seq - goal produces_trans_refn : [#"../06_map_precond.rs" 38 4 38 90] forall a : C06MapPrecond_Map_Type.t_map i b f item0 . forall ab : Seq.seq b . forall b : C06MapPrecond_Map_Type.t_map i b f item0 . forall bc : Seq.seq b . forall c : C06MapPrecond_Map_Type.t_map i b f item0 . inv0 c - /\ inv1 bc /\ inv0 b /\ inv1 ab /\ inv0 a /\ produces0 b bc c /\ produces0 a ab b - -> inv0 c - /\ inv1 bc - /\ inv0 b - /\ inv1 ab - /\ inv0 a - /\ produces0 b bc c - /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c -> produces0 a (Seq.(++) ab bc) c) - goal produces_refl_refn : [#"../06_map_precond.rs" 31 4 31 26] forall self : C06MapPrecond_Map_Type.t_map i b f item0 . inv0 self - -> inv0 self /\ (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) - goal next_refn : [#"../06_map_precond.rs" 63 4 63 44] forall self : borrowed (C06MapPrecond_Map_Type.t_map i b f item0) . inv2 self - -> inv2 self - /\ (forall result : Core_Option_Option_Type.t_option b . inv3 result + goal next_refn : [#"../06_map_precond.rs" 63 4 63 44] forall self : borrowed (C06MapPrecond_Map_Type.t_map i b f item0) . inv0 self + -> inv0 self + /\ (forall result : Core_Option_Option_Type.t_option b . inv1 result /\ match result with | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces_one0 ( * self) v ( ^ self) end - -> inv3 result + -> inv1 result /\ match result with | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self) end) + goal produces_trans_refn : [#"../06_map_precond.rs" 38 4 38 90] forall a : C06MapPrecond_Map_Type.t_map i b f item0 . forall ab : Seq.seq b . forall b : C06MapPrecond_Map_Type.t_map i b f item0 . forall bc : Seq.seq b . forall c : C06MapPrecond_Map_Type.t_map i b f item0 . inv2 c + /\ inv3 bc /\ inv2 b /\ inv3 ab /\ inv2 a /\ produces0 b bc c /\ produces0 a ab b + -> inv2 c + /\ inv3 bc + /\ inv2 b + /\ inv3 ab + /\ inv2 a + /\ produces0 b bc c + /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c -> produces0 a (Seq.(++) ab bc) c) + goal produces_refl_refn : [#"../06_map_precond.rs" 31 4 31 26] forall self : C06MapPrecond_Map_Type.t_map i b f item0 . inv2 self + -> inv2 self /\ (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) end module C06MapPrecond_Impl2 type i diff --git a/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml b/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml index 3b39a35c25..53cb19a983 100644 --- a/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml +++ b/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml @@ -378,14 +378,14 @@ - - + + - - + + diff --git a/creusot/tests/should_succeed/iterators/06_map_precond/why3shapes.gz b/creusot/tests/should_succeed/iterators/06_map_precond/why3shapes.gz index c178f20207625e2e24bd40031134377c4fd71d23..92c89e3b8cc6b9aa6e4954c365c8808da28b6846 100644 GIT binary patch delta 3387 zcmV-B4aD-WMYlz;o)v$KQ=>Oq_NxRq-Qs>Z+4ePlCF;f(Uaz6xM^-OytzII~UuH_3 z*uhrI@~6DFI6wZ7!)c>GaBRaj^iys1b~91km{r%kZp;-E!_&6th4Cy_cA!vc(^K9y zET&AzXwTCPAJ>n-s`(U=z2hw?SG(%4PoDcSfG2VQPnK=S*PDNDu6B!8P*|?Lr zvb(5}09i{^Ety2ZQGd?_^r~!_U5sSB1Vvo07hg>s)YZi-UG&C^UPYs&=b__HNT*aE zdLL{*STEmjwdZor#h&v$XM4YQd%HJ#y;pm=N9mqjBxyRj8UnS6#gf? zdkPG}x+o-9z36{a^g>44hh(gku49I$3`3f|6nn|{lI?}x3%3_`FU(%(y-<4rP+~9m zUa&p)d+zq!?z!1>ec`llDTdDLz@0Ki^-A{1m`-DuTJsEC@1^`&_}!oe6EFwEpbRKA z3|)wW>9tW>bvDCSUk|_UdmzhfG|9(a7;l5_V@H##!%%-F_?zGd76qoc56<))v#q%^ zvX|Cz$IOuN=gjT3-fOkja<9c+^Sx$!<@d_%mE9||S6ENAS8}h!Uh%zRd+GPm?WMio zf%(3(l7rTi4MucI+TIU}8yN>zD1_Os??CG4edO9D3%EuB=}u`-FjqjF1?s@@y<>ap z_ZH-5_tt;xt=?O;w{maA-txU=d*k=U?G32Y?2X^grD9Mfvh%4lzu_QpY2SPc^?qbgqo zs>1Xv3B{dLyys3k&zQMp6keee9e9Rmflq!eW2#Ux)3YC5x7E4kg>en*=3bj%DD*L5(?VVNhcvYPe!wO|Y5IAG1KG=q@Bd(k`Bg@M5f zvjZ~)TetUi?_Y;l5UO{E!zPe}4I!lnB%{P{VaQ_}y$1e@FqRDB%9)@s!A`*A>4$$F zZlQrC7UB1>31k0?knZ~A{1ByND#DG51L!1pA7Ddx_?faI%^7=LhzH&cuxgx&I{D7% zZZJ+K0Y8wuV&1)4#2FNbl}W|E)6&C6*9j!9=$=DuWKklViC2WNhq&;)^-2YzX{LI3 z5w5pMupkT%6UMJ;noTFI7z|_^)Chkpp^hiXyaCnl4i4Ld^sA!}`WNTO)%2cs)@xXA z6m5{nh9P)}l~;?nwFc%q)JZRt&^E!n51fN=jF2FiV#}igF2I!(CZaeI1&SzAM4=+C z@j)Gm=H+l6>T%R#{)|^9S?Hm2y&gKv205^4+o`?nW17^!1PYKRWlcH9qI6#XqmwA8#*Rb=(G?+ zaEwc9iv<9^{8F=*diXY}56XM#Rq$N(v5)W>I;n=fum)^~mqM?TK}zpn{c$VF{J^XY z7S36628MQ7T=QZ&cL*RY&Z71PXj*9B-fG60mWd9Yb~1rUtKebv z0e%TM#*J>3q{Vd<Fl+X#zVZ2?$r^t6_(fP5RK%0D25B#Kw7^PirQ(&<0Lzu z7_@LN-C%W$0e@g!g|g0Q2~+T;P!yOoCYa`dRGeTcs!n0$m30ojT`DN5mqgJqs1a{E zXS>11p^NZ`obPzY9dwB(dJb+0hhO4fjHh`Q+@N7)K__dUQnG(N<`olbJnS1$^a=c@ zm&H;txRb&vWwI|%H@sLad^gAd4}VCn1Ixe?OhF|ulS9W%AoUz$O1#q@sC2~Ay)c&0 z&Bnk{ha8VQXcIiVI?p|0u*ytSuLDc^x3L7r^jYvW+;Q7eFcp?8Q_`kkbOCgBLBE%z zrZ72tHiix8I1d$>-eFTip14LE-ea2((`z_Gp%pLKcKExNVn z)>4sr7W9II@&orOHwdZ0%%A}?7#GPj1KI^Wz;ovJKu1`cH0!%g4@Ps9x~>!OkYQ(g z!>lVtHCZ&jA4<&k3}VM6tVESulW~b~M0l)%)@g5(J4}OEv1#|dVd<;Gs zABB&^2lam#?ZKi=Sm?;3BM*c~1bHCjfshA69te3L100+0v*Az z7m}XQkrXeAbn1FoxI-s}k|e;<7EZpTJ*3V+Zod)GVghPRz$1KZ$kWsg-rGJot6;N% z^8J4hImq9E>UAuVLj$PBw?gMIhy)Bw0fSvA+BS;Lp|S;Zwt&(W(Auwcuw6eeW1Z+V zoJ`iMXnVLu34$A3-*=;!)Zz~_VC$_I2E$-tSTFiMK=VPoQFhgIuxQ2s%Rkhh^$?}v zOu$$T0xmoEoefGVvKqYa((ZD2P*In;n|cy z8(M924BJI$`-htZ26Gh-=70tFgB^O9K)s0p*0k`wwrZRN0EQv=N1qJ%6%cQOOMPI% z3>;>FgS0pBXdwrJc_R!>hAc||6(9^btleNJ2a>Q*o#VV`6#Uh2brlaln9eGoBcp$R zKbsIr5LOf@C~48dF6rXH2c;R8DKaZYq}=b1m=mFgkzt)u(Iqcwmr{%l{YBGvkaF;U z1bL3Ml<*z}yhj1=QNVi?@E!$xBVp+P2oQo(1ltiG)Pqwb;1mgRibf~L1?H3Ya4~%B zOcJ!+49_OI;IL%F8vzUjFciR007HM_(Sf4_Ce%3qI2io2!H(yBD2_u`DLwSba44tH zzmb?0iD{9T7Kv$*m==j?k&Mo&&|wt-!?d7le1NUj7ekUsxL$Q;(9m*N8PzjTjyF(o zE)r0W#_odgu1_(*B&HO!5`GXmXbv?YSkm0Tk%~^o(AgOJpjWVfgld#`ro~1(>T&I-eU9vI^ijLHD%2S4+ z(<#Pb>`**wr<#HEIDA^xCoO+fV!AU{4c=PEA?MjRz2@0Fmag+qq89d|4g(#%=^&d1 z&=-SD^?Dqw{63xgm~`rU53khraD-r`2Pu2V|3^P9wUZj zM2gmT27^vKM%rDNof+^AK4?G@I{Hm9I;gwo0s`-s*8l;-i|^iK<3T^6$9SBtN9)tR2W>SG8L zT$5#s@b%`KtKH&NxgBItHtsT>`m4^ltR*#AJhCf0>F=3<=6`=sW|54dv7GMHq0(kO z^5$wW<%`BH@^0)$VAZUX$T5U1C|6ZTRqv8k;-WWJ^eP%HJr5msLOP}T(EDKf!Fu_I zt38){F7}-7Iotca+uOa_>%H2`JxcfNB1zM+E@`bI6Iv-3WsFLtr0_rC-BVx))P4TT7c$yDBx8TAbR9E1Wf;=zrPxcpmuxTmUbwxmdtvrM?}ge6fD(Jb_k!)Y-*dO; zcF)b8>kFraOEGj_2kw+Hs#mg4#&jCP)S74DdN1YI!tVw(n1DGL24%1YVdz2}Os|d7 zs7dm~G9Sk-fBzJ7$KA zKWA>Q^?4NOwwug1G|XEKmoI?;YD)zqcSiySHX< z_1>zzm3x0H_LlE0+Z(?(Zf`)HW^eS~sJ)SUBld>x4clwK*O&$1X}%s+4>!PjkhSey z&x0AbHa>}N2s~QV=`t7QRp2VQ^<45^2xpWMF~#1*L7Of`o;owGn|>9zcH9g}#}NJC zq)46Tg2YhteHt+5nTVZu6{tF|W!H(|m{x;UMtgs&v^NgI!fKdE8CCfzP!*ntA_gLkW?v5;Hb4^qD(R1?H=f+}}1(5^_!4NIidEsG4;`yv8f2L*s0!A`Ohn#aVf z?!bRnjAFN3nWTJIaD5$&)k7`yjA`4;sK8>p<4_D*L#j&cJCRA?b!Y+DV+wjeFb}yk zB#}I$3ymQOdSwS$WPp7Ys5&ty!G#*EiCiWJBeaKrl?KL4Cqzcov%P}}>RtuHk|nEq zpq-#yHFMG$?qlZ^s6qx?5Egs?I&2p$S+swQb12y!-Xtgib1VZ-){CK+nZZ2%|2kMq z4XIb4+OD^lf}44yTLe}1pGkq zih1{H5ob^!RwfnuPD>9PT_=#ZqI(XtkwuAcCSDQ79^%6H)+-f=rkU#DMY!H3!GbV6 zOc=kWX*Qj-Vla?xP$RH}I-Vr+22_8;J2-3;(yxv_=wF;8SJQjmS+8NeQM5rO8;0N^ zR$eXQ)*6`eP$#`mLfZuQK5!1gF+zf5iY<>0xBypDn26#;6eyxd5rvAl#s_sMnwP_Q zsK-%{`7>UbWTA)7^?K+u8|1*c&asZuT|qjT(kBH70ZRgwK%WAA3iK%m7xaHAa&QX{ zJwD=p7J4zlJRFoZni=Nc$vV>u-VZQnY&W7OUkW`gVvNR1BYa@7H$iYc4Dh&wkkLy~ zBERCL(6gZO-f3+O<2nT8JdhkZW3BKp=pteCi=oH0kJb;prZ9!!nmfjNZvjFw;q8bX ze<}1JgP}p7v!euKq>d%2Av%9x+i^c=QS`TbG1?nK8X`-brho)kI7zS3rQnKj%SsT9 z%NOHZisU2<73W|@MBc-QVAAnkvaXL~%s!*@LW}Eqqxfzg@J}B>{SHW}D$3DVm=%gC@!Wys{UJAWV1}VLR^~bFw^8>RsSU6|N85r7S zam|bA+#!IpIE&gFplP9fd#f3b1DVuAEa=&nLNBI1StdGo+Q|eat%8Tu2lyr67&p3A zk`~udkn5$Sv)57@5AlCOx>rZoR#;xELo|~2p%^Y`18MzIC~Bu6kCW_tV$j09bc59~ z2K<3_70NoJB}~DWLQ!DWm|&U*QgMQ*s5*s}SJpZBcB!DKUJ^yephmpuob3i1hc3b& za=zmochDuG=sCD09Da#^F`njKaD#@G1)Z#YO3C(^S4^z&uy21v(I@bqUKUHq;7$sw zl*zt4-SA?y@ZBH-Jp3WO4lDypFa?#sOb#74fz)%1De+Espwbab_rh30HyZ;-9dbPK zpiS`b>OA+1!74LRy$&qt-^LOg(`UikaK~*=!BkkXOi7!D(FM@i1^r%bg$ALx!F04YRHo)nw89 zekd{DGl*el1Q%Gi;5){ofa$NHnVqt41ON*F#(R7?KKKnv7tG;f@iF*ld=x$sAJk*C z2a7ggp(B5fjyw<|5#)i82SOeQc_8G0kY^VblEF(WVTF>S4ZVZWLc5)um(KY9jQ|@8 zPDr3ru%Q4O3a}w8LVV8awxT=f5;FvG~6SXWOO5<=#=)&(Z+u{+BrvC=UxHwk!jlr3#4hE5Ui@u zDbQ)sE_Q)|H8S#0VS={)z1l%Y8JUm+T=;=AHfX^@Ox_p_rjz|R2y_I;UPyXIM^d~f z(y8lV;SQY?N|FFaTR8cW_K-RQx&1~!iwUSP0gv#tAx~2~cyIgUtb)x3%J)O$Ab$s{ z*Rg*{4h^6h-wK_>AQCVz1q^nfXxk_{hsqYv*#b&iKx@C&!FK(?jCG>da57o1qV3@t zB?xYCecz2@Qj0&#fUUP;7z~4nVZG@40L=&SM%h)Dv1 z?H_Iu7|c~Tm;)Bv4|eEb0`(>aSkuDy+NyC902qecAAK_5S3tZCF7<&4GjNyz4$|Jh zqlFv@=8Z5k8L}w-SAa0&uy%u?97w`Kb&m6%QSev8)m1zIVLGdTj*R~OY(gkOSW$nV zprl0)yQGT)ACzWXrpT-qk#fI3Vorn}Muv4tMVGv!T}m-J^cPLvLCV4Z5#%}2Qo?%_ z@E!%cM*;6qzV`5~@+cWr72M53mC(NGyM@q?0sQ zT*>Jm4eD`r(bJwmtS%QeCh!$x4!46<3ML>N2buM(gwZX>xRJ~sI;;eM6g&FLj)$P7 zfW!+?I@$o{VDrn^TX@LEB~{EfN#}hedzKDmaGg?;cge~yC^}NpDNh-OPNx`$u|x5! zooWWsCRX+cx!(hhn#2Q^qObySh~(biCWl;It+C5rh{x6Kwk_p)$4Jz z^80k|W74VbJ-kxe!x4g&9;}E7Zk`ogafT$Fc*_UV)U$L7jnSbGc#Ig95h+^V84Nn{ z7-@H5c4ojg_@Dtr=;$}a=%50h8yOacWGwinXP_<82zG!++e1SoSap9L_!fhpKC}3nr7#R{qhJ=wJAxI^R3<)DcYQlkz6Uqx|2L%Pw zITJ}pK?Xr~^WK22{lF}|E`9iK>Lc{rngBteyTECayTOoRANo!>n2R}RCN2A>KK?(Z K91xLHqyPXdM@7W| diff --git a/creusot/tests/should_succeed/iterators/07_fuse.mlcfg b/creusot/tests/should_succeed/iterators/07_fuse.mlcfg index e55c589402..4ed32bfa49 100644 --- a/creusot/tests/should_succeed/iterators/07_fuse.mlcfg +++ b/creusot/tests/should_succeed/iterators/07_fuse.mlcfg @@ -637,47 +637,60 @@ module C07Fuse_Impl0 axiom inv4 : forall x : borrowed i . inv4 x = true type item0 - use seq.Seq - predicate invariant3 (self : Seq.seq item0) - val invariant3 (self : Seq.seq item0) : bool + use Core_Option_Option_Type as Core_Option_Option_Type + predicate invariant3 (self : Core_Option_Option_Type.t_option item0) + val invariant3 (self : Core_Option_Option_Type.t_option item0) : bool ensures { result = invariant3 self } - predicate inv3 (_x : Seq.seq item0) - val inv3 (_x : Seq.seq item0) : bool + predicate inv3 (_x : Core_Option_Option_Type.t_option item0) + val inv3 (_x : Core_Option_Option_Type.t_option item0) : bool ensures { result = inv3 _x } - axiom inv3 : forall x : Seq.seq item0 . inv3 x = true + axiom inv3 : forall x : Core_Option_Option_Type.t_option item0 . inv3 x = true use C07Fuse_Fuse_Type as C07Fuse_Fuse_Type - predicate invariant2 (self : C07Fuse_Fuse_Type.t_fuse i) - val invariant2 (self : C07Fuse_Fuse_Type.t_fuse i) : bool + predicate invariant2 (self : borrowed (C07Fuse_Fuse_Type.t_fuse i)) + val invariant2 (self : borrowed (C07Fuse_Fuse_Type.t_fuse i)) : bool ensures { result = invariant2 self } - predicate inv2 (_x : C07Fuse_Fuse_Type.t_fuse i) - val inv2 (_x : C07Fuse_Fuse_Type.t_fuse i) : bool + predicate inv2 (_x : borrowed (C07Fuse_Fuse_Type.t_fuse i)) + val inv2 (_x : borrowed (C07Fuse_Fuse_Type.t_fuse i)) : bool ensures { result = inv2 _x } - axiom inv2 : forall x : C07Fuse_Fuse_Type.t_fuse i . inv2 x = true - use Core_Option_Option_Type as Core_Option_Option_Type - predicate invariant1 (self : Core_Option_Option_Type.t_option item0) - val invariant1 (self : Core_Option_Option_Type.t_option item0) : bool + axiom inv2 : forall x : borrowed (C07Fuse_Fuse_Type.t_fuse i) . inv2 x = true + use seq.Seq + predicate invariant1 (self : Seq.seq item0) + val invariant1 (self : Seq.seq item0) : bool ensures { result = invariant1 self } - predicate inv1 (_x : Core_Option_Option_Type.t_option item0) - val inv1 (_x : Core_Option_Option_Type.t_option item0) : bool + predicate inv1 (_x : Seq.seq item0) + val inv1 (_x : Seq.seq item0) : bool ensures { result = inv1 _x } - axiom inv1 : forall x : Core_Option_Option_Type.t_option item0 . inv1 x = true - predicate invariant0 (self : borrowed (C07Fuse_Fuse_Type.t_fuse i)) - val invariant0 (self : borrowed (C07Fuse_Fuse_Type.t_fuse i)) : bool + axiom inv1 : forall x : Seq.seq item0 . inv1 x = true + predicate invariant0 (self : C07Fuse_Fuse_Type.t_fuse i) + val invariant0 (self : C07Fuse_Fuse_Type.t_fuse i) : bool ensures { result = invariant0 self } - predicate inv0 (_x : borrowed (C07Fuse_Fuse_Type.t_fuse i)) - val inv0 (_x : borrowed (C07Fuse_Fuse_Type.t_fuse i)) : bool + predicate inv0 (_x : C07Fuse_Fuse_Type.t_fuse i) + val inv0 (_x : C07Fuse_Fuse_Type.t_fuse i) : bool ensures { result = inv0 _x } - axiom inv0 : forall x : borrowed (C07Fuse_Fuse_Type.t_fuse i) . inv0 x = true + axiom inv0 : forall x : C07Fuse_Fuse_Type.t_fuse i . inv0 x = true use seq.Seq use seq.Seq + use seq.Seq + predicate completed1 [#"../common.rs" 11 4 11 36] (self : borrowed i) + val completed1 [#"../common.rs" 11 4 11 36] (self : borrowed i) : bool + ensures { result = completed1 self } + + predicate completed0 [#"../07_fuse.rs" 16 4 16 35] (self : borrowed (C07Fuse_Fuse_Type.t_fuse i)) = + [#"../07_fuse.rs" 18 12 19 32] (C07Fuse_Fuse_Type.fuse_iter ( * self) = Core_Option_Option_Type.C_None + \/ (exists it : borrowed i . inv4 it + /\ completed1 it /\ C07Fuse_Fuse_Type.fuse_iter ( * self) = Core_Option_Option_Type.C_Some ( * it))) + /\ C07Fuse_Fuse_Type.fuse_iter ( ^ self) = Core_Option_Option_Type.C_None + val completed0 [#"../07_fuse.rs" 16 4 16 35] (self : borrowed (C07Fuse_Fuse_Type.t_fuse i)) : bool + ensures { result = completed0 self } + use seq.Seq predicate produces1 [#"../common.rs" 8 4 8 65] (self : i) (visited : Seq.seq item0) (o : i) val produces1 [#"../common.rs" 8 4 8 65] (self : i) (visited : Seq.seq item0) (o : i) : bool @@ -697,42 +710,29 @@ module C07Fuse_Impl0 val produces0 [#"../07_fuse.rs" 25 4 25 65] (self : C07Fuse_Fuse_Type.t_fuse i) (prod : Seq.seq item0) (other : C07Fuse_Fuse_Type.t_fuse i) : bool ensures { result = produces0 self prod other } - use seq.Seq - predicate completed1 [#"../common.rs" 11 4 11 36] (self : borrowed i) - val completed1 [#"../common.rs" 11 4 11 36] (self : borrowed i) : bool - ensures { result = completed1 self } - - predicate completed0 [#"../07_fuse.rs" 16 4 16 35] (self : borrowed (C07Fuse_Fuse_Type.t_fuse i)) = - [#"../07_fuse.rs" 18 12 19 32] (C07Fuse_Fuse_Type.fuse_iter ( * self) = Core_Option_Option_Type.C_None - \/ (exists it : borrowed i . inv4 it - /\ completed1 it /\ C07Fuse_Fuse_Type.fuse_iter ( * self) = Core_Option_Option_Type.C_Some ( * it))) - /\ C07Fuse_Fuse_Type.fuse_iter ( ^ self) = Core_Option_Option_Type.C_None - val completed0 [#"../07_fuse.rs" 16 4 16 35] (self : borrowed (C07Fuse_Fuse_Type.t_fuse i)) : bool - ensures { result = completed0 self } - - goal next_refn : [#"../07_fuse.rs" 39 4 39 44] forall self : borrowed (C07Fuse_Fuse_Type.t_fuse i) . inv0 self - -> inv0 self - /\ (forall result : Core_Option_Option_Type.t_option item0 . inv1 result + goal produces_trans_refn : [#"../07_fuse.rs" 62 4 62 90] forall a : C07Fuse_Fuse_Type.t_fuse i . forall ab : Seq.seq item0 . forall b : C07Fuse_Fuse_Type.t_fuse i . forall bc : Seq.seq item0 . forall c : C07Fuse_Fuse_Type.t_fuse i . inv0 c + /\ inv1 bc /\ inv0 b /\ inv1 ab /\ inv0 a /\ produces0 b bc c /\ produces0 a ab b + -> inv0 c + /\ inv1 bc + /\ inv0 b + /\ inv1 ab + /\ inv0 a + /\ produces0 b bc c + /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c -> produces0 a (Seq.(++) ab bc) c) + goal next_refn : [#"../07_fuse.rs" 39 4 39 44] forall self : borrowed (C07Fuse_Fuse_Type.t_fuse i) . inv2 self + -> inv2 self + /\ (forall result : Core_Option_Option_Type.t_option item0 . inv3 result /\ match result with | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self) end - -> inv1 result + -> inv3 result /\ match result with | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self) end) - goal produces_refl_refn : [#"../07_fuse.rs" 55 4 55 26] forall self : C07Fuse_Fuse_Type.t_fuse i . inv2 self - -> inv2 self /\ (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) - goal produces_trans_refn : [#"../07_fuse.rs" 62 4 62 90] forall a : C07Fuse_Fuse_Type.t_fuse i . forall ab : Seq.seq item0 . forall b : C07Fuse_Fuse_Type.t_fuse i . forall bc : Seq.seq item0 . forall c : C07Fuse_Fuse_Type.t_fuse i . inv2 c - /\ inv3 bc /\ inv2 b /\ inv3 ab /\ inv2 a /\ produces0 b bc c /\ produces0 a ab b - -> inv2 c - /\ inv3 bc - /\ inv2 b - /\ inv3 ab - /\ inv2 a - /\ produces0 b bc c - /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c -> produces0 a (Seq.(++) ab bc) c) + goal produces_refl_refn : [#"../07_fuse.rs" 55 4 55 26] forall self : C07Fuse_Fuse_Type.t_fuse i . inv0 self + -> inv0 self /\ (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) end module C07Fuse_Impl1 type i diff --git a/creusot/tests/should_succeed/iterators/07_fuse/why3session.xml b/creusot/tests/should_succeed/iterators/07_fuse/why3session.xml index ca2f81f559..a8bfaf6eef 100644 --- a/creusot/tests/should_succeed/iterators/07_fuse/why3session.xml +++ b/creusot/tests/should_succeed/iterators/07_fuse/why3session.xml @@ -43,15 +43,15 @@ + + + - - - diff --git a/creusot/tests/should_succeed/iterators/07_fuse/why3shapes.gz b/creusot/tests/should_succeed/iterators/07_fuse/why3shapes.gz index a74736381c0038189595e49da6bdbff76e91f8fa..f273287c4eaac3963e5d3de4bca12e7bd3ee1993 100644 GIT binary patch literal 1322 zcmV+_1=ac=iwFP!00000|Fu_3a~n4dzUx=$*4Dld1fQMBL8GyUdub1y;V~ZWE;rHC zmR!kk+J9g0rCr%>(k4?KBof32fZ#`f`tfRg`WPPLY5g3Jr`=)y^IEO1ep)^K5qA4$ z<=Jf=N)K%)JilFq$KzrAG{h5l4A<9Qc;$7Mma+aSuj*XZxu|pO7HC<33v*;kUN|rz zK0H4C!4iC|jiEg`{Dr~#mhIb^Y(@i+W)8YO((jH(_f=Yub6 zq9;F9hmjaxh~Lq7=nu!^;d2~+c=)|7a~r1JKHPh-VK>tE%>oEE0ZFAqb8~i#o|{d{ z05@&NDQ=G<`=SFiH;d?#rIJ$nIb-Vz^BgxN!D&#X+;g?5yihp=P($=5e6!s&BLzs_LVAv?QdWcgz}?vmT)9rV!rvv4B#T_)YxTCNAg~ zQUn{ zz01XWX&O@OJO%Ofn9Ci1ReP6$9Q{S?s>a@OqUJ2>QfOHi@-LOJp$hscr~?+la+f_R zCd@3M4+&RPUc*FZez$vy$1p6$Asy@Wbtu@9p<0v|vD&i=b%*n9Z3Sp)xvnieT*hK%*lxK0+fTG)BUik_%3zF5L_)O=r7!>90`}8aIK+Nj!O9?oqn@ zi8iOF_;@O+-Qqb=Z`gcf6;{*}cyayedF8d@EL_wUJ|_t01c{4yWlE3o#@p^q>Fs7I zPS2#JKqr+_OueinSJk<$^IB|QIQTA0x9PLGct*YI=&7MC8@i@?KDYB?8i{@X&5C*3 z%I#)Z=lI3bFu~|~A z+{4yXYqDhxOLgB0OlPz*Xoqo4Zba9XPh? zt(bb`Q_m(Cg{1ciNNu9l3@l1v*PtCJ2hxFXfDQ--E2RXd_pKNNS`>`@L_P-I_j;NX zeG&>;LUH=G4$QZsWN%=QLqDi6S_Rk(jdrAZ1I*e1Lqc)uIDIR}2`e0@-Eqg^|1>q> z6a|c`kFmG?WPy#QHzU&`4rs<~%KR%+{WKWMxg5EjqC{(YtAnAZz{GU07LzH#99oCQ zA*Dz;ln&_((IIyTE1^anC(5kR0VdspGALQpIMBbT-sHpz;RHItoq&oWaxg=PKyO`Y zQwYNdhR1kbKgZMg?s)ilt=3mRt)Bh}cZX-? z*-afv4{azszgdOH({cFJ$1`{g*VkTn<@G)-WBpfN)w!&5QRlc{Sj%F#a7Vu6MF11x z!{gIm-c)_BX`p+7!6-p8jn&D#QfW}7V(XEU>dmKf z^c1J+FcRYn@jLp4?sz&KKgZ#Rhu_;Ww_&_HgnJJ*+zs^IEeydXLsBW(?54ozx!Dv1 zxM@31d3zK&79FVBEwWFZ3Z(XPwyi77bKDew)1XSZ=W0`Vp>hhwbG>U3^%8S3lrJ#{ z%AKS$=9nJ3i?4O3;> zm*w)$YaxSL$apGb1wa%YGoFR#E*DC7TrAD7wpn-m8G}2 zcrRT;%AKbqzMgZrRY4uF5SF{_NHN*W z68e#FMddY&bmq5rPw^D`#W0T-997Wm8({l}VC%JPZgyW}shHR*>s-`1*7^6bRLm^pa|edG1GC(L z=PgqcP8kAEody~mq45zKA)zr6CQ2?inYwgyuymdM;$^%>O=#Q%A}8_WeYr>J@+aDy zpW@@WsO}fffqKK{BdcabJsB^qUp=q9R)U3#+QMgma0ZC*y?B7U>V>HlEL)+bN;o${ zwQ1$(zj-lld$}p4xblTvJi3zC0_FwolkjGJ2b!dko2nTgU0E94A}hIPH!*4*#dC5yvQC zP+g3j?M4f1Fr68g7O_V&WLM^2x$4H=SkC3Z?HDCm(^(x1Jq1RlgSD7k3Fgo`G!6+O zd epiMvGfRHnk;3RXxI$@m9tG@xKsx9`e4gdfk^o|Yy diff --git a/creusot/tests/should_succeed/iterators/08_collect_extend.mlcfg b/creusot/tests/should_succeed/iterators/08_collect_extend.mlcfg index 30ab6a127b..676c2bdb7f 100644 --- a/creusot/tests/should_succeed/iterators/08_collect_extend.mlcfg +++ b/creusot/tests/should_succeed/iterators/08_collect_extend.mlcfg @@ -410,7 +410,7 @@ module C08CollectExtend_Extend goto BB20 } BB14 { - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _17; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _17; _17 <- (let Core_Option_Option_Type.C_Some x0 = _17 in Core_Option_Option_Type.C_Some (any t)); assert { [@expl:type invariant] inv5 _17 }; assume { resolve4 _17 }; @@ -422,7 +422,7 @@ module C08CollectExtend_Extend _22 <- any Snapshot.snap_ty (Seq.seq t); assert { [@expl:type invariant] inv2 produced }; assume { resolve2 produced }; - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] x <- __creusot_proc_iter_elem; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] x <- __creusot_proc_iter_elem; __creusot_proc_iter_elem <- any t; [#"../08_collect_extend.rs" 30 8 30 11] _26 <- Borrow.borrow_mut ( * vec); [#"../08_collect_extend.rs" 30 8 30 11] vec <- { vec with current = ( ^ _26) ; }; @@ -791,7 +791,7 @@ module C08CollectExtend_Collect goto BB21 } BB15 { - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _15; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _15; _15 <- (let Core_Option_Option_Type.C_Some x0 = _15 in Core_Option_Option_Type.C_Some (any item0)); assert { [@expl:type invariant] inv4 _15 }; assume { resolve3 _15 }; @@ -803,7 +803,7 @@ module C08CollectExtend_Collect _20 <- any Snapshot.snap_ty (Seq.seq item0); assert { [@expl:type invariant] inv1 produced }; assume { resolve1 produced }; - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] x <- __creusot_proc_iter_elem; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] x <- __creusot_proc_iter_elem; __creusot_proc_iter_elem <- any item0; [#"../08_collect_extend.rs" 47 8 47 11] _24 <- Borrow.borrow_mut res; [#"../08_collect_extend.rs" 47 8 47 11] res <- ^ _24; diff --git a/creusot/tests/should_succeed/iterators/09_empty.mlcfg b/creusot/tests/should_succeed/iterators/09_empty.mlcfg index 766c95ebb3..f405891957 100644 --- a/creusot/tests/should_succeed/iterators/09_empty.mlcfg +++ b/creusot/tests/should_succeed/iterators/09_empty.mlcfg @@ -123,37 +123,37 @@ module C09Empty_Impl0_Next end module C09Empty_Impl0 type t - use Core_Option_Option_Type as Core_Option_Option_Type - predicate invariant3 (self : Core_Option_Option_Type.t_option t) - val invariant3 (self : Core_Option_Option_Type.t_option t) : bool + use seq.Seq + predicate invariant3 (self : Seq.seq t) + val invariant3 (self : Seq.seq t) : bool ensures { result = invariant3 self } - predicate inv3 (_x : Core_Option_Option_Type.t_option t) - val inv3 (_x : Core_Option_Option_Type.t_option t) : bool + predicate inv3 (_x : Seq.seq t) + val inv3 (_x : Seq.seq t) : bool ensures { result = inv3 _x } - axiom inv3 : forall x : Core_Option_Option_Type.t_option t . inv3 x = true - use C09Empty_Empty_Type as C09Empty_Empty_Type - use prelude.Borrow - predicate invariant2 (self : borrowed (C09Empty_Empty_Type.t_empty t)) - val invariant2 (self : borrowed (C09Empty_Empty_Type.t_empty t)) : bool + axiom inv3 : forall x : Seq.seq t . inv3 x = true + use Core_Option_Option_Type as Core_Option_Option_Type + predicate invariant2 (self : Core_Option_Option_Type.t_option t) + val invariant2 (self : Core_Option_Option_Type.t_option t) : bool ensures { result = invariant2 self } - predicate inv2 (_x : borrowed (C09Empty_Empty_Type.t_empty t)) - val inv2 (_x : borrowed (C09Empty_Empty_Type.t_empty t)) : bool + predicate inv2 (_x : Core_Option_Option_Type.t_option t) + val inv2 (_x : Core_Option_Option_Type.t_option t) : bool ensures { result = inv2 _x } - axiom inv2 : forall x : borrowed (C09Empty_Empty_Type.t_empty t) . inv2 x = true - use seq.Seq - predicate invariant1 (self : Seq.seq t) - val invariant1 (self : Seq.seq t) : bool + axiom inv2 : forall x : Core_Option_Option_Type.t_option t . inv2 x = true + use C09Empty_Empty_Type as C09Empty_Empty_Type + use prelude.Borrow + predicate invariant1 (self : borrowed (C09Empty_Empty_Type.t_empty t)) + val invariant1 (self : borrowed (C09Empty_Empty_Type.t_empty t)) : bool ensures { result = invariant1 self } - predicate inv1 (_x : Seq.seq t) - val inv1 (_x : Seq.seq t) : bool + predicate inv1 (_x : borrowed (C09Empty_Empty_Type.t_empty t)) + val inv1 (_x : borrowed (C09Empty_Empty_Type.t_empty t)) : bool ensures { result = inv1 _x } - axiom inv1 : forall x : Seq.seq t . inv1 x = true + axiom inv1 : forall x : borrowed (C09Empty_Empty_Type.t_empty t) . inv1 x = true predicate invariant0 (self : C09Empty_Empty_Type.t_empty t) val invariant0 (self : C09Empty_Empty_Type.t_empty t) : bool ensures { result = invariant0 self } @@ -164,6 +164,7 @@ module C09Empty_Impl0 axiom inv0 : forall x : C09Empty_Empty_Type.t_empty t . inv0 x = true use seq.Seq + use seq.Seq predicate resolve0 (self : borrowed (C09Empty_Empty_Type.t_empty t)) = [#"../../../../../creusot-contracts/src/resolve.rs" 26 20 26 34] ^ self = * self val resolve0 (self : borrowed (C09Empty_Empty_Type.t_empty t)) : bool @@ -174,7 +175,6 @@ module C09Empty_Impl0 val completed0 [#"../09_empty.rs" 15 4 15 35] (self : borrowed (C09Empty_Empty_Type.t_empty t)) : bool ensures { result = completed0 self } - use seq.Seq use seq.Seq use seq.Seq predicate produces0 [#"../09_empty.rs" 21 4 21 64] (self : C09Empty_Empty_Type.t_empty t) (visited : Seq.seq t) (o : C09Empty_Empty_Type.t_empty t) @@ -186,21 +186,21 @@ module C09Empty_Impl0 goal produces_refl_refn : [#"../09_empty.rs" 28 4 28 26] forall self : C09Empty_Empty_Type.t_empty t . inv0 self -> (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) - goal produces_trans_refn : [#"../09_empty.rs" 35 4 35 90] forall a : C09Empty_Empty_Type.t_empty t . forall ab : Seq.seq t . forall b : C09Empty_Empty_Type.t_empty t . forall bc : Seq.seq t . forall c : C09Empty_Empty_Type.t_empty t . inv0 c - /\ inv1 bc /\ inv0 b /\ inv1 ab /\ inv0 a /\ produces0 b bc c /\ produces0 a ab b - -> inv1 bc - /\ inv1 ab - /\ produces0 b bc c - /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c -> produces0 a (Seq.(++) ab bc) c) - goal next_refn : [#"../09_empty.rs" 41 4 41 35] forall self : borrowed (C09Empty_Empty_Type.t_empty t) . inv2 self - -> (forall result : Core_Option_Option_Type.t_option t . inv3 result + goal next_refn : [#"../09_empty.rs" 41 4 41 35] forall self : borrowed (C09Empty_Empty_Type.t_empty t) . inv1 self + -> (forall result : Core_Option_Option_Type.t_option t . inv2 result /\ match result with | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self) end - -> inv3 result + -> inv2 result /\ match result with | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self) end) + goal produces_trans_refn : [#"../09_empty.rs" 35 4 35 90] forall a : C09Empty_Empty_Type.t_empty t . forall ab : Seq.seq t . forall b : C09Empty_Empty_Type.t_empty t . forall bc : Seq.seq t . forall c : C09Empty_Empty_Type.t_empty t . inv0 c + /\ inv3 bc /\ inv0 b /\ inv3 ab /\ inv0 a /\ produces0 b bc c /\ produces0 a ab b + -> inv3 bc + /\ inv3 ab + /\ produces0 b bc c + /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c -> produces0 a (Seq.(++) ab bc) c) end diff --git a/creusot/tests/should_succeed/iterators/09_empty/why3session.xml b/creusot/tests/should_succeed/iterators/09_empty/why3session.xml index 712547ed18..6401fbd274 100644 --- a/creusot/tests/should_succeed/iterators/09_empty/why3session.xml +++ b/creusot/tests/should_succeed/iterators/09_empty/why3session.xml @@ -24,12 +24,12 @@ - - - + + + diff --git a/creusot/tests/should_succeed/iterators/09_empty/why3shapes.gz b/creusot/tests/should_succeed/iterators/09_empty/why3shapes.gz index ae6edce834e92658431fe7373017a05edd93114c..088a39e76a63cad321e41b348eec039a116b506c 100644 GIT binary patch literal 449 zcmV;y0Y3g8iwFP!00000|CNwIuiGFHgzx+cAKT;t3mB->LlnufFTGUa*rx^7uaOcv zjnk<8_XRtR94Uv^7q7?P3_E<-RMU4n(^TE)G9AX@Q&m@+j||V3G5w4*ah&MbBc0CI z-}A`k@ojdo>km8(H|}|}b|7xIhyg>y*gfe*Tq}Q>5`yK|JcP)WSlI0`j;HgHu9UbJ zxPSXH4zvo`WN|tS@0l0}FY((9eH~BaJ#_fl!`;(#c%f-L-YDlZ%?{Y-O{V&QoQP3iOtd_5A3OfdeuR#I@Gy?dUVjcWg*@DUy6C1vTP;F zR!>WBw_bbWZTC`bc569n^;)P4vRkfD-`}SDH%I>Y-}dQqZv}`tmZANAX-vAlMFRln*dPsLAhWpGN)w7BH4 inv0 c + /\ inv1 bc + /\ inv0 b + /\ inv1 ab + /\ inv0 a + /\ produces0 b bc c + /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c -> produces0 a (Seq.(++) ab bc) c) goal produces_refl_refn : [#"../10_once.rs" 31 4 31 26] forall self : C10Once_Once_Type.t_once t . inv0 self -> inv0 self /\ (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) - goal next_refn : [#"../10_once.rs" 44 4 44 35] forall self : borrowed (C10Once_Once_Type.t_once t) . inv1 self - -> inv1 self - /\ (forall result : Core_Option_Option_Type.t_option t . inv2 result + goal next_refn : [#"../10_once.rs" 44 4 44 35] forall self : borrowed (C10Once_Once_Type.t_once t) . inv2 self + -> inv2 self + /\ (forall result : Core_Option_Option_Type.t_option t . inv3 result /\ match result with | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self) end - -> inv2 result + -> inv3 result /\ match result with | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self) end) - goal produces_trans_refn : [#"../10_once.rs" 38 4 38 90] forall a : C10Once_Once_Type.t_once t . forall ab : Seq.seq t . forall b : C10Once_Once_Type.t_once t . forall bc : Seq.seq t . forall c : C10Once_Once_Type.t_once t . inv0 c - /\ inv3 bc /\ inv0 b /\ inv3 ab /\ inv0 a /\ produces0 b bc c /\ produces0 a ab b - -> inv0 c - /\ inv3 bc - /\ inv0 b - /\ inv3 ab - /\ inv0 a - /\ produces0 b bc c - /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c -> produces0 a (Seq.(++) ab bc) c) end diff --git a/creusot/tests/should_succeed/iterators/10_once/why3session.xml b/creusot/tests/should_succeed/iterators/10_once/why3session.xml index 04d21c9212..b93a7b390a 100644 --- a/creusot/tests/should_succeed/iterators/10_once/why3session.xml +++ b/creusot/tests/should_succeed/iterators/10_once/why3session.xml @@ -25,15 +25,15 @@ + + + - - - diff --git a/creusot/tests/should_succeed/iterators/10_once/why3shapes.gz b/creusot/tests/should_succeed/iterators/10_once/why3shapes.gz index 464974532355ea56d0430608159195c25afc1186..e771c6f69665ad8f83815a4d683bd3a57c3945db 100644 GIT binary patch literal 628 zcmV-)0*n10iwFP!00000|D{q*kJB&|yysWs2DBGHe;cWXs#26n2o6X-?&|p?yAf?t z+OojE$4*_EUG;*<#m;zU-uU^wU(}~(Jj7G|5|5{T96r{vUVNy|-?1NFz>=nHiG`-Z z!*L8hd^{06#a)MSe>nf1w%ds_ZL0}=oNSAj-h3eYTrKGd`jMOeF-Yd zEgtf2Wi`6-cpQJm@NWMt(Z38nPRgzyaF+t~!SbdY*qkw|q!p>uDj$ku_Z*M?`LPf9 z6!T)aha6yG#l`}ii<^?1Hv^-un*#sk)a38=Ev9L=VtWs4uD<1!MV_wNOo@9l zC1x|F(#wj!BXxqd8p#AxbcvcakcuwL#8>7NA%cL4*J`YiSED zshF0GaHpLUM0PR~2ObfO4^$w8H44KOFeCMxN;s9q zQ7xhjNEJ~)2tqCv9e}BUwU7cp3#2uzu26YFlmZNld(Aj8k~rpM7obzb_~Z?y1>J&b zLAD@TNL84jK?lubs?L?v9yCx!Ll+|PqRW>gZ$+*X&UZWzPywYw;XQ&*0_;*}xXB`T OEBXW7ijPEJ1pol6E-zmI literal 624 zcmV-$0+0P4iwFP!00000|D{q*kJB&^z2{ft2DBHCzm3#GRVi{M1P3G^cQuZk-HJ9T zZCT*oW2Y|3u6jZAV*6#@n>TOzeo>#F@fgqbOFW%-L;tas_2NTy`Hs8(1srM0l{jcB zJf4Q|qm5^R=eX}M9*&pa<8?dMjMr*JA4l0jrjrh2otq?mC5gCPB6{>Kw%b>D2It7F zX6%XM37AVpz!$*ZD%#SJO*ZIc1G0^qBi2-#GA>zfupJJ^eZ0g#9LLS$=b?`?8;b;< zcl}eU7~ZrUYB!=t5o4kbG7Kq8dr%fOOsDYTduE0 zWtrk3-&RheA5N#?XAJKS-%|OPzKtWZ+x56l26n;mrhIVOV`fPwQma+|D3aWBJnb%z zyMRwIAC9+>4J@44IG}TKQ=Idra+|svPIVuDT}obj3Y1NO(kW2Lf!?y^^KB;^=3rlRkwG-ZvVgd^Tewp^ybwKLnhXkyRc zgsC~8a>;G_^)*^q-m1KHdB1M(UrJ5>RTYFN!E~*cRB^2haxSz0#kvS01gM#%7A&cl zmW*((y%$7wG7=9hBA7N%mDn;BDl4t9yi%ZADJhiUk;QR2omU zh%z8mL;)cPxmol8rUqsq82}5!8mlWqO%hIm9u!h90YZ?J`;JkjB#%iOj0J5$S&$Zl z1zv&ThJ~P&LFgd1!Dy~p2;DdUc6mthmgGUkh?JTTNJj%VU7|{+SR!|^Rha~DNq+$7 K^Zh+v1pom3Bqb*R diff --git a/creusot/tests/should_succeed/iterators/11_repeat.mlcfg b/creusot/tests/should_succeed/iterators/11_repeat.mlcfg index 696ad5bbe5..6e442e5759 100644 --- a/creusot/tests/should_succeed/iterators/11_repeat.mlcfg +++ b/creusot/tests/should_succeed/iterators/11_repeat.mlcfg @@ -199,52 +199,47 @@ module C11Repeat_Impl0_Next end module C11Repeat_Impl0 type a - use Core_Option_Option_Type as Core_Option_Option_Type - predicate invariant3 (self : Core_Option_Option_Type.t_option a) - val invariant3 (self : Core_Option_Option_Type.t_option a) : bool + use seq.Seq + predicate invariant3 (self : Seq.seq a) + val invariant3 (self : Seq.seq a) : bool ensures { result = invariant3 self } - predicate inv3 (_x : Core_Option_Option_Type.t_option a) - val inv3 (_x : Core_Option_Option_Type.t_option a) : bool + predicate inv3 (_x : Seq.seq a) + val inv3 (_x : Seq.seq a) : bool ensures { result = inv3 _x } - axiom inv3 : forall x : Core_Option_Option_Type.t_option a . inv3 x = true + axiom inv3 : forall x : Seq.seq a . inv3 x = true use C11Repeat_Repeat_Type as C11Repeat_Repeat_Type - use prelude.Borrow - predicate invariant2 (self : borrowed (C11Repeat_Repeat_Type.t_repeat a)) - val invariant2 (self : borrowed (C11Repeat_Repeat_Type.t_repeat a)) : bool + predicate invariant2 (self : C11Repeat_Repeat_Type.t_repeat a) + val invariant2 (self : C11Repeat_Repeat_Type.t_repeat a) : bool ensures { result = invariant2 self } - predicate inv2 (_x : borrowed (C11Repeat_Repeat_Type.t_repeat a)) - val inv2 (_x : borrowed (C11Repeat_Repeat_Type.t_repeat a)) : bool + predicate inv2 (_x : C11Repeat_Repeat_Type.t_repeat a) + val inv2 (_x : C11Repeat_Repeat_Type.t_repeat a) : bool ensures { result = inv2 _x } - axiom inv2 : forall x : borrowed (C11Repeat_Repeat_Type.t_repeat a) . inv2 x = true - use seq.Seq - predicate invariant1 (self : Seq.seq a) - val invariant1 (self : Seq.seq a) : bool + axiom inv2 : forall x : C11Repeat_Repeat_Type.t_repeat a . inv2 x = true + use Core_Option_Option_Type as Core_Option_Option_Type + predicate invariant1 (self : Core_Option_Option_Type.t_option a) + val invariant1 (self : Core_Option_Option_Type.t_option a) : bool ensures { result = invariant1 self } - predicate inv1 (_x : Seq.seq a) - val inv1 (_x : Seq.seq a) : bool + predicate inv1 (_x : Core_Option_Option_Type.t_option a) + val inv1 (_x : Core_Option_Option_Type.t_option a) : bool ensures { result = inv1 _x } - axiom inv1 : forall x : Seq.seq a . inv1 x = true - predicate invariant0 (self : C11Repeat_Repeat_Type.t_repeat a) - val invariant0 (self : C11Repeat_Repeat_Type.t_repeat a) : bool + axiom inv1 : forall x : Core_Option_Option_Type.t_option a . inv1 x = true + use prelude.Borrow + predicate invariant0 (self : borrowed (C11Repeat_Repeat_Type.t_repeat a)) + val invariant0 (self : borrowed (C11Repeat_Repeat_Type.t_repeat a)) : bool ensures { result = invariant0 self } - predicate inv0 (_x : C11Repeat_Repeat_Type.t_repeat a) - val inv0 (_x : C11Repeat_Repeat_Type.t_repeat a) : bool + predicate inv0 (_x : borrowed (C11Repeat_Repeat_Type.t_repeat a)) + val inv0 (_x : borrowed (C11Repeat_Repeat_Type.t_repeat a)) : bool ensures { result = inv0 _x } - axiom inv0 : forall x : C11Repeat_Repeat_Type.t_repeat a . inv0 x = true + axiom inv0 : forall x : borrowed (C11Repeat_Repeat_Type.t_repeat a) . inv0 x = true use seq.Seq - predicate completed0 [#"../11_repeat.rs" 17 4 17 35] (self : borrowed (C11Repeat_Repeat_Type.t_repeat a)) = - [#"../11_repeat.rs" 18 20 18 25] false - val completed0 [#"../11_repeat.rs" 17 4 17 35] (self : borrowed (C11Repeat_Repeat_Type.t_repeat a)) : bool - ensures { result = completed0 self } - use seq.Seq use seq.Seq use seq.Seq @@ -260,27 +255,32 @@ module C11Repeat_Impl0 ensures { result = produces0 self visited o } use seq.Seq - goal produces_refl_refn : [#"../11_repeat.rs" 33 4 33 26] forall self : C11Repeat_Repeat_Type.t_repeat a . inv0 self - -> inv0 self /\ (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) - goal produces_trans_refn : [#"../11_repeat.rs" 40 4 40 90] forall a : C11Repeat_Repeat_Type.t_repeat a . forall ab : Seq.seq a . forall b : C11Repeat_Repeat_Type.t_repeat a . forall bc : Seq.seq a . forall c : C11Repeat_Repeat_Type.t_repeat a . inv0 c - /\ inv1 bc /\ inv0 b /\ inv1 ab /\ inv0 a /\ produces0 b bc c /\ produces0 a ab b - -> inv0 c - /\ inv1 bc - /\ inv0 b - /\ inv1 ab - /\ inv0 a - /\ produces0 b bc c - /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c -> produces0 a (Seq.(++) ab bc) c) - goal next_refn : [#"../11_repeat.rs" 46 4 46 35] forall self : borrowed (C11Repeat_Repeat_Type.t_repeat a) . inv2 self - -> inv2 self - /\ (forall result : Core_Option_Option_Type.t_option a . inv3 result + predicate completed0 [#"../11_repeat.rs" 17 4 17 35] (self : borrowed (C11Repeat_Repeat_Type.t_repeat a)) = + [#"../11_repeat.rs" 18 20 18 25] false + val completed0 [#"../11_repeat.rs" 17 4 17 35] (self : borrowed (C11Repeat_Repeat_Type.t_repeat a)) : bool + ensures { result = completed0 self } + + goal next_refn : [#"../11_repeat.rs" 46 4 46 35] forall self : borrowed (C11Repeat_Repeat_Type.t_repeat a) . inv0 self + -> inv0 self + /\ (forall result : Core_Option_Option_Type.t_option a . inv1 result /\ match result with | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self) end - -> inv3 result + -> inv1 result /\ match result with | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self) end) + goal produces_refl_refn : [#"../11_repeat.rs" 33 4 33 26] forall self : C11Repeat_Repeat_Type.t_repeat a . inv2 self + -> inv2 self /\ (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) + goal produces_trans_refn : [#"../11_repeat.rs" 40 4 40 90] forall a : C11Repeat_Repeat_Type.t_repeat a . forall ab : Seq.seq a . forall b : C11Repeat_Repeat_Type.t_repeat a . forall bc : Seq.seq a . forall c : C11Repeat_Repeat_Type.t_repeat a . inv2 c + /\ inv3 bc /\ inv2 b /\ inv3 ab /\ inv2 a /\ produces0 b bc c /\ produces0 a ab b + -> inv2 c + /\ inv3 bc + /\ inv2 b + /\ inv3 ab + /\ inv2 a + /\ produces0 b bc c + /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c -> produces0 a (Seq.(++) ab bc) c) end diff --git a/creusot/tests/should_succeed/iterators/11_repeat/why3session.xml b/creusot/tests/should_succeed/iterators/11_repeat/why3session.xml index d12c471928..6b6921b368 100644 --- a/creusot/tests/should_succeed/iterators/11_repeat/why3session.xml +++ b/creusot/tests/should_succeed/iterators/11_repeat/why3session.xml @@ -21,13 +21,13 @@ - + - + - + diff --git a/creusot/tests/should_succeed/iterators/11_repeat/why3shapes.gz b/creusot/tests/should_succeed/iterators/11_repeat/why3shapes.gz index c09e6ad31decfa7d45fb0fa9604c04908789cfc3..e646a003c9e6a4b100a0a09b737093c8fe10598b 100644 GIT binary patch literal 489 zcmVGg{TURBAFLWe4yBxPn)`i=a z-Eb;<`h70m)>A+9yoNES+PArw=Pvc_PD|69MH-lXhy3=5SkL#q&hmd|*K4PoakhP` zrs+F5Y5HE!8Cm={kKb9(XEUE41OCgY&QDQvWR*g&45ZY?gANra#=Q2vLS9kH8`eOf zJSr|b6M+S<1Tulj8jv3j^=;E55qfBD*XVO3(2#Np8WOhn%qjXy@{ zdw&YXs1`pPwfsWe;w23I@fMQPRLY3m{LUyCS+`R~xtsdQFMCrZhi~B=@M?10GFca9 zU&j7YcH!@JwZT+iTzDp*i1lmY;`4xQw?-Oebo*3I(iiUMyD50MsmVI6y?vXDdhSxsw>RyWXep6sN`wGq3Al<#N-bDhA*({k z8rqOTT9iygGw;%7#c?qr^ZG;pRsXaUkymG)Etqmc?2k0$Q)f7t?QLRSO;04?+LQUCw| diff --git a/creusot/tests/should_succeed/iterators/12_zip.mlcfg b/creusot/tests/should_succeed/iterators/12_zip.mlcfg index b2b9039d81..a9a64feb63 100644 --- a/creusot/tests/should_succeed/iterators/12_zip.mlcfg +++ b/creusot/tests/should_succeed/iterators/12_zip.mlcfg @@ -864,6 +864,8 @@ module C12Zip_Impl0 | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self) end) + goal produces_refl_refn : [#"../12_zip.rs" 41 4 41 26] forall self : C12Zip_Zip_Type.t_zip a b . inv2 self + -> inv2 self /\ (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) goal produces_trans_refn : [#"../12_zip.rs" 48 4 48 90] forall a : C12Zip_Zip_Type.t_zip a b . forall ab : Seq.seq (item0, item1) . forall b : C12Zip_Zip_Type.t_zip a b . forall bc : Seq.seq (item0, item1) . forall c : C12Zip_Zip_Type.t_zip a b . inv2 c /\ inv3 bc /\ inv2 b /\ inv3 ab /\ inv2 a /\ produces0 b bc c /\ produces0 a ab b -> inv2 c @@ -873,6 +875,4 @@ module C12Zip_Impl0 /\ inv2 a /\ produces0 b bc c /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c -> produces0 a (Seq.(++) ab bc) c) - goal produces_refl_refn : [#"../12_zip.rs" 41 4 41 26] forall self : C12Zip_Zip_Type.t_zip a b . inv2 self - -> inv2 self /\ (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) end diff --git a/creusot/tests/should_succeed/iterators/13_cloned.mlcfg b/creusot/tests/should_succeed/iterators/13_cloned.mlcfg index 439771a6e2..c2ca4c08cc 100644 --- a/creusot/tests/should_succeed/iterators/13_cloned.mlcfg +++ b/creusot/tests/should_succeed/iterators/13_cloned.mlcfg @@ -401,45 +401,55 @@ module C13Cloned_Impl0 ensures { result = inv4 _x } axiom inv4 : forall x : Seq.seq t . inv4 x = true - predicate invariant3 (self : Seq.seq t) - val invariant3 (self : Seq.seq t) : bool + use Core_Option_Option_Type as Core_Option_Option_Type + predicate invariant3 (self : Core_Option_Option_Type.t_option t) + val invariant3 (self : Core_Option_Option_Type.t_option t) : bool ensures { result = invariant3 self } - predicate inv3 (_x : Seq.seq t) - val inv3 (_x : Seq.seq t) : bool + predicate inv3 (_x : Core_Option_Option_Type.t_option t) + val inv3 (_x : Core_Option_Option_Type.t_option t) : bool ensures { result = inv3 _x } - axiom inv3 : forall x : Seq.seq t . inv3 x = true + axiom inv3 : forall x : Core_Option_Option_Type.t_option t . inv3 x = true use C13Cloned_Cloned_Type as C13Cloned_Cloned_Type - predicate invariant2 (self : C13Cloned_Cloned_Type.t_cloned i) - val invariant2 (self : C13Cloned_Cloned_Type.t_cloned i) : bool + use prelude.Borrow + predicate invariant2 (self : borrowed (C13Cloned_Cloned_Type.t_cloned i)) + val invariant2 (self : borrowed (C13Cloned_Cloned_Type.t_cloned i)) : bool ensures { result = invariant2 self } - predicate inv2 (_x : C13Cloned_Cloned_Type.t_cloned i) - val inv2 (_x : C13Cloned_Cloned_Type.t_cloned i) : bool + predicate inv2 (_x : borrowed (C13Cloned_Cloned_Type.t_cloned i)) + val inv2 (_x : borrowed (C13Cloned_Cloned_Type.t_cloned i)) : bool ensures { result = inv2 _x } - axiom inv2 : forall x : C13Cloned_Cloned_Type.t_cloned i . inv2 x = true - use Core_Option_Option_Type as Core_Option_Option_Type - predicate invariant1 (self : Core_Option_Option_Type.t_option t) - val invariant1 (self : Core_Option_Option_Type.t_option t) : bool + axiom inv2 : forall x : borrowed (C13Cloned_Cloned_Type.t_cloned i) . inv2 x = true + predicate invariant1 (self : Seq.seq t) + val invariant1 (self : Seq.seq t) : bool ensures { result = invariant1 self } - predicate inv1 (_x : Core_Option_Option_Type.t_option t) - val inv1 (_x : Core_Option_Option_Type.t_option t) : bool + predicate inv1 (_x : Seq.seq t) + val inv1 (_x : Seq.seq t) : bool ensures { result = inv1 _x } - axiom inv1 : forall x : Core_Option_Option_Type.t_option t . inv1 x = true - use prelude.Borrow - predicate invariant0 (self : borrowed (C13Cloned_Cloned_Type.t_cloned i)) - val invariant0 (self : borrowed (C13Cloned_Cloned_Type.t_cloned i)) : bool + axiom inv1 : forall x : Seq.seq t . inv1 x = true + predicate invariant0 (self : C13Cloned_Cloned_Type.t_cloned i) + val invariant0 (self : C13Cloned_Cloned_Type.t_cloned i) : bool ensures { result = invariant0 self } - predicate inv0 (_x : borrowed (C13Cloned_Cloned_Type.t_cloned i)) - val inv0 (_x : borrowed (C13Cloned_Cloned_Type.t_cloned i)) : bool + predicate inv0 (_x : C13Cloned_Cloned_Type.t_cloned i) + val inv0 (_x : C13Cloned_Cloned_Type.t_cloned i) : bool ensures { result = inv0 _x } - axiom inv0 : forall x : borrowed (C13Cloned_Cloned_Type.t_cloned i) . inv0 x = true + axiom inv0 : forall x : C13Cloned_Cloned_Type.t_cloned i . inv0 x = true + use seq.Seq + predicate completed1 [#"../common.rs" 11 4 11 36] (self : borrowed i) + val completed1 [#"../common.rs" 11 4 11 36] (self : borrowed i) : bool + ensures { result = completed1 self } + + predicate completed0 [#"../13_cloned.rs" 22 4 22 35] (self : borrowed (C13Cloned_Cloned_Type.t_cloned i)) = + [#"../13_cloned.rs" 23 8 23 43] completed1 (Borrow.borrow_logic (C13Cloned_Cloned_Type.cloned_iter ( * self)) (C13Cloned_Cloned_Type.cloned_iter ( ^ self)) (Borrow.inherit_id (Borrow.get_id self) 1)) + val completed0 [#"../13_cloned.rs" 22 4 22 35] (self : borrowed (C13Cloned_Cloned_Type.t_cloned i)) : bool + ensures { result = completed0 self } + use seq.Seq use seq.Seq use seq.Seq @@ -462,37 +472,27 @@ module C13Cloned_Impl0 val produces0 [#"../13_cloned.rs" 28 4 28 64] (self : C13Cloned_Cloned_Type.t_cloned i) (visited : Seq.seq t) (o : C13Cloned_Cloned_Type.t_cloned i) : bool ensures { result = produces0 self visited o } - use seq.Seq - predicate completed1 [#"../common.rs" 11 4 11 36] (self : borrowed i) - val completed1 [#"../common.rs" 11 4 11 36] (self : borrowed i) : bool - ensures { result = completed1 self } - - predicate completed0 [#"../13_cloned.rs" 22 4 22 35] (self : borrowed (C13Cloned_Cloned_Type.t_cloned i)) = - [#"../13_cloned.rs" 23 8 23 43] completed1 (Borrow.borrow_logic (C13Cloned_Cloned_Type.cloned_iter ( * self)) (C13Cloned_Cloned_Type.cloned_iter ( ^ self)) (Borrow.inherit_id (Borrow.get_id self) 1)) - val completed0 [#"../13_cloned.rs" 22 4 22 35] (self : borrowed (C13Cloned_Cloned_Type.t_cloned i)) : bool - ensures { result = completed0 self } - - goal next_refn : [#"../13_cloned.rs" 52 4 52 35] forall self : borrowed (C13Cloned_Cloned_Type.t_cloned i) . inv0 self - -> inv0 self - /\ (forall result : Core_Option_Option_Type.t_option t . inv1 result + goal produces_trans_refn : [#"../13_cloned.rs" 46 4 46 90] forall a : C13Cloned_Cloned_Type.t_cloned i . forall ab : Seq.seq t . forall b : C13Cloned_Cloned_Type.t_cloned i . forall bc : Seq.seq t . forall c : C13Cloned_Cloned_Type.t_cloned i . inv0 c + /\ inv1 bc /\ inv0 b /\ inv1 ab /\ inv0 a /\ produces0 b bc c /\ produces0 a ab b + -> inv0 c + /\ inv1 bc + /\ inv0 b + /\ inv1 ab + /\ inv0 a + /\ produces0 b bc c + /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c -> produces0 a (Seq.(++) ab bc) c) + goal produces_refl_refn : [#"../13_cloned.rs" 39 4 39 26] forall self : C13Cloned_Cloned_Type.t_cloned i . inv0 self + -> inv0 self /\ (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) + goal next_refn : [#"../13_cloned.rs" 52 4 52 35] forall self : borrowed (C13Cloned_Cloned_Type.t_cloned i) . inv2 self + -> inv2 self + /\ (forall result : Core_Option_Option_Type.t_option t . inv3 result /\ match result with | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self) end - -> inv1 result + -> inv3 result /\ match result with | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self) end) - goal produces_refl_refn : [#"../13_cloned.rs" 39 4 39 26] forall self : C13Cloned_Cloned_Type.t_cloned i . inv2 self - -> inv2 self /\ (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) - goal produces_trans_refn : [#"../13_cloned.rs" 46 4 46 90] forall a : C13Cloned_Cloned_Type.t_cloned i . forall ab : Seq.seq t . forall b : C13Cloned_Cloned_Type.t_cloned i . forall bc : Seq.seq t . forall c : C13Cloned_Cloned_Type.t_cloned i . inv2 c - /\ inv3 bc /\ inv2 b /\ inv3 ab /\ inv2 a /\ produces0 b bc c /\ produces0 a ab b - -> inv2 c - /\ inv3 bc - /\ inv2 b - /\ inv3 ab - /\ inv2 a - /\ produces0 b bc c - /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c -> produces0 a (Seq.(++) ab bc) c) end diff --git a/creusot/tests/should_succeed/iterators/13_cloned/why3session.xml b/creusot/tests/should_succeed/iterators/13_cloned/why3session.xml index afe363cead..e31fb4ea76 100644 --- a/creusot/tests/should_succeed/iterators/13_cloned/why3session.xml +++ b/creusot/tests/should_succeed/iterators/13_cloned/why3session.xml @@ -21,13 +21,13 @@ - + - + diff --git a/creusot/tests/should_succeed/iterators/13_cloned/why3shapes.gz b/creusot/tests/should_succeed/iterators/13_cloned/why3shapes.gz index d2e1f411ef7ed8d96b838d13190f8076caae12e0..6f78d5a9476be359157e8f9ab33e6be1dd5b7837 100644 GIT binary patch literal 792 zcmV+z1Lyo7iwFP!00000|D{z;kK;BBz57?>*6r*?q`nL6AqZ+Hm-bLV#~sL$yc=vL zo+jzE{r9D8Id;-Pfnsw=M2e5(qaKkDPn*lv@R~21w|u@FhSN_QwR!rnx&9swr#JMh zZNlq$NPon90T1EhM~_~3xu345U+|*ZyxLf8*ssuh0uRg@;7o{XzrJa=)3AYNbk3LI_?D?#U6%;-c0Nof4`ynH5N1u0LgXVwC=}(Iq9_#Q zjUpx6R!z$)iqGSbO6kxI=kxGqPCvYSBgF1Vsndk-52tV}vpOXDZg01KoaqQBB?;>E z(-e7Zrb#?15w%d7$38NtWE9Xv zrcBNXRo*Bkop9Wt1IHS{ZHZ(#iH;-VB1Db~G4YUs=`@7{cR<15fH~`o(@iuy3&s1C ztm#AFGqh-X&@A@cunspU98v{z2o9M8>%chB4k(*+Aex@aX=ZKAsRM<@>>=YppkEbDuN#)<-hN08MirhrN$rASmV92LJ##5t0A^ literal 788 zcmV+v1MB=BiwFP!00000|D{w-kJ~s5z57?>*6s8nQlDO+hahO6T-rkc9XpUExeYcG zPm^@o{`*q494pykfkkt0NQ#f-d#3!?!|MFSKd1BRC7sUu;rRDTtsY)Cm#=<*d_l*y zjekB3@mok|aNys(ap;7TyXkoP2PcZpi;u;JU4`ZouqsEj_)P=l)6?_ir&9&5wq+7< zdN!Fe6^8k9I`k84G)LqVZN}*1NU(tUe>37&W}^7K_*ncuW5gFmxG;juXeQU*kn=R3 z_nq&854)Rq4%U%5XJqfE_uzBN80bo%n=?XbsInlFDILtFaJaoH#+Q-BGP1m*NjhrR zI$%?S*-)-60aJWkd{ql)3bd+7<;?B7f}$nB+yfTffF|CQcLnQ>55v>*Azf0WBknhk z?}uZm&vX?3|opx3i8p&XcL7($quBBjWCijXPFnxe=Q<&`28 zTbG@dWhp+5CbiPO8&0R;dy21~{vpKXK&9h^@ApT4$Xe|qJ-63WH)=Yjxkb6^wBXe@r3y}1Tt2>cSh|5K zU!>h{qlB))`Fhm>om1xeWi3?kb@5H{ZyWqkrEUH-P2@p|poP*r^npnwgMcnDWl~b8 z(n?urh2<74Sk?&M=1i8N=r}SieBh`MBlpppPE$H?3zQ5Nm~E}Gx(S9Sp?Du-YkJ@J z3|nk_&@A-aunt!!EK&!w2o{-z)`GF1El@RSK{TCVEdO0rd|O-jc;gkDD9o7SU(E*i`rxCeRGB^s0`Bc-B7ZS0xqw8tJI S^l9vb_n=>;!;nnN2LJ#y0g|Es diff --git a/creusot/tests/should_succeed/iterators/14_copied.mlcfg b/creusot/tests/should_succeed/iterators/14_copied.mlcfg index fb32bbe697..413f29e8d6 100644 --- a/creusot/tests/should_succeed/iterators/14_copied.mlcfg +++ b/creusot/tests/should_succeed/iterators/14_copied.mlcfg @@ -401,47 +401,57 @@ module C14Copied_Impl0 ensures { result = inv4 _x } axiom inv4 : forall x : Seq.seq t . inv4 x = true - predicate invariant3 (self : Seq.seq t) - val invariant3 (self : Seq.seq t) : bool + use Core_Option_Option_Type as Core_Option_Option_Type + predicate invariant3 (self : Core_Option_Option_Type.t_option t) + val invariant3 (self : Core_Option_Option_Type.t_option t) : bool ensures { result = invariant3 self } - predicate inv3 (_x : Seq.seq t) - val inv3 (_x : Seq.seq t) : bool + predicate inv3 (_x : Core_Option_Option_Type.t_option t) + val inv3 (_x : Core_Option_Option_Type.t_option t) : bool ensures { result = inv3 _x } - axiom inv3 : forall x : Seq.seq t . inv3 x = true + axiom inv3 : forall x : Core_Option_Option_Type.t_option t . inv3 x = true use C14Copied_Copied_Type as C14Copied_Copied_Type - predicate invariant2 (self : C14Copied_Copied_Type.t_copied i) - val invariant2 (self : C14Copied_Copied_Type.t_copied i) : bool + use prelude.Borrow + predicate invariant2 (self : borrowed (C14Copied_Copied_Type.t_copied i)) + val invariant2 (self : borrowed (C14Copied_Copied_Type.t_copied i)) : bool ensures { result = invariant2 self } - predicate inv2 (_x : C14Copied_Copied_Type.t_copied i) - val inv2 (_x : C14Copied_Copied_Type.t_copied i) : bool + predicate inv2 (_x : borrowed (C14Copied_Copied_Type.t_copied i)) + val inv2 (_x : borrowed (C14Copied_Copied_Type.t_copied i)) : bool ensures { result = inv2 _x } - axiom inv2 : forall x : C14Copied_Copied_Type.t_copied i . inv2 x = true - use Core_Option_Option_Type as Core_Option_Option_Type - predicate invariant1 (self : Core_Option_Option_Type.t_option t) - val invariant1 (self : Core_Option_Option_Type.t_option t) : bool + axiom inv2 : forall x : borrowed (C14Copied_Copied_Type.t_copied i) . inv2 x = true + predicate invariant1 (self : Seq.seq t) + val invariant1 (self : Seq.seq t) : bool ensures { result = invariant1 self } - predicate inv1 (_x : Core_Option_Option_Type.t_option t) - val inv1 (_x : Core_Option_Option_Type.t_option t) : bool + predicate inv1 (_x : Seq.seq t) + val inv1 (_x : Seq.seq t) : bool ensures { result = inv1 _x } - axiom inv1 : forall x : Core_Option_Option_Type.t_option t . inv1 x = true - use prelude.Borrow - predicate invariant0 (self : borrowed (C14Copied_Copied_Type.t_copied i)) - val invariant0 (self : borrowed (C14Copied_Copied_Type.t_copied i)) : bool + axiom inv1 : forall x : Seq.seq t . inv1 x = true + predicate invariant0 (self : C14Copied_Copied_Type.t_copied i) + val invariant0 (self : C14Copied_Copied_Type.t_copied i) : bool ensures { result = invariant0 self } - predicate inv0 (_x : borrowed (C14Copied_Copied_Type.t_copied i)) - val inv0 (_x : borrowed (C14Copied_Copied_Type.t_copied i)) : bool + predicate inv0 (_x : C14Copied_Copied_Type.t_copied i) + val inv0 (_x : C14Copied_Copied_Type.t_copied i) : bool ensures { result = inv0 _x } - axiom inv0 : forall x : borrowed (C14Copied_Copied_Type.t_copied i) . inv0 x = true + axiom inv0 : forall x : C14Copied_Copied_Type.t_copied i . inv0 x = true + use seq.Seq use seq.Seq use seq.Seq + predicate completed1 [#"../common.rs" 11 4 11 36] (self : borrowed i) + val completed1 [#"../common.rs" 11 4 11 36] (self : borrowed i) : bool + ensures { result = completed1 self } + + predicate completed0 [#"../14_copied.rs" 22 4 22 35] (self : borrowed (C14Copied_Copied_Type.t_copied i)) = + [#"../14_copied.rs" 23 8 23 43] completed1 (Borrow.borrow_logic (C14Copied_Copied_Type.copied_iter ( * self)) (C14Copied_Copied_Type.copied_iter ( ^ self)) (Borrow.inherit_id (Borrow.get_id self) 1)) + val completed0 [#"../14_copied.rs" 22 4 22 35] (self : borrowed (C14Copied_Copied_Type.t_copied i)) : bool + ensures { result = completed0 self } + use seq.Seq use seq.Seq use seq.Seq @@ -462,37 +472,27 @@ module C14Copied_Impl0 val produces0 [#"../14_copied.rs" 28 4 28 64] (self : C14Copied_Copied_Type.t_copied i) (visited : Seq.seq t) (o : C14Copied_Copied_Type.t_copied i) : bool ensures { result = produces0 self visited o } - use seq.Seq - predicate completed1 [#"../common.rs" 11 4 11 36] (self : borrowed i) - val completed1 [#"../common.rs" 11 4 11 36] (self : borrowed i) : bool - ensures { result = completed1 self } - - predicate completed0 [#"../14_copied.rs" 22 4 22 35] (self : borrowed (C14Copied_Copied_Type.t_copied i)) = - [#"../14_copied.rs" 23 8 23 43] completed1 (Borrow.borrow_logic (C14Copied_Copied_Type.copied_iter ( * self)) (C14Copied_Copied_Type.copied_iter ( ^ self)) (Borrow.inherit_id (Borrow.get_id self) 1)) - val completed0 [#"../14_copied.rs" 22 4 22 35] (self : borrowed (C14Copied_Copied_Type.t_copied i)) : bool - ensures { result = completed0 self } - - goal next_refn : [#"../14_copied.rs" 52 4 52 35] forall self : borrowed (C14Copied_Copied_Type.t_copied i) . inv0 self - -> inv0 self - /\ (forall result : Core_Option_Option_Type.t_option t . inv1 result + goal produces_trans_refn : [#"../14_copied.rs" 46 4 46 90] forall a : C14Copied_Copied_Type.t_copied i . forall ab : Seq.seq t . forall b : C14Copied_Copied_Type.t_copied i . forall bc : Seq.seq t . forall c : C14Copied_Copied_Type.t_copied i . inv0 c + /\ inv1 bc /\ inv0 b /\ inv1 ab /\ inv0 a /\ produces0 b bc c /\ produces0 a ab b + -> inv0 c + /\ inv1 bc + /\ inv0 b + /\ inv1 ab + /\ inv0 a + /\ produces0 b bc c + /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c -> produces0 a (Seq.(++) ab bc) c) + goal next_refn : [#"../14_copied.rs" 52 4 52 35] forall self : borrowed (C14Copied_Copied_Type.t_copied i) . inv2 self + -> inv2 self + /\ (forall result : Core_Option_Option_Type.t_option t . inv3 result /\ match result with | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self) end - -> inv1 result + -> inv3 result /\ match result with | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self) end) - goal produces_refl_refn : [#"../14_copied.rs" 39 4 39 26] forall self : C14Copied_Copied_Type.t_copied i . inv2 self - -> inv2 self /\ (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) - goal produces_trans_refn : [#"../14_copied.rs" 46 4 46 90] forall a : C14Copied_Copied_Type.t_copied i . forall ab : Seq.seq t . forall b : C14Copied_Copied_Type.t_copied i . forall bc : Seq.seq t . forall c : C14Copied_Copied_Type.t_copied i . inv2 c - /\ inv3 bc /\ inv2 b /\ inv3 ab /\ inv2 a /\ produces0 b bc c /\ produces0 a ab b - -> inv2 c - /\ inv3 bc - /\ inv2 b - /\ inv3 ab - /\ inv2 a - /\ produces0 b bc c - /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c -> produces0 a (Seq.(++) ab bc) c) + goal produces_refl_refn : [#"../14_copied.rs" 39 4 39 26] forall self : C14Copied_Copied_Type.t_copied i . inv0 self + -> inv0 self /\ (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) end diff --git a/creusot/tests/should_succeed/iterators/14_copied/why3session.xml b/creusot/tests/should_succeed/iterators/14_copied/why3session.xml index f3bed7e753..ad84849a1f 100644 --- a/creusot/tests/should_succeed/iterators/14_copied/why3session.xml +++ b/creusot/tests/should_succeed/iterators/14_copied/why3session.xml @@ -21,14 +21,14 @@ - - + + - - + + diff --git a/creusot/tests/should_succeed/iterators/14_copied/why3shapes.gz b/creusot/tests/should_succeed/iterators/14_copied/why3shapes.gz index dde1cfd5a1eb59bb2a87b87dbe9ade07343b4e85..dd930c6d47147a01f13f13b73ef4e6949a70bd20 100644 GIT binary patch literal 791 zcmV+y1L*u8iwFP!00000|D{z;Z`&{oz57?>wynL0)c1fMf?$Sn*$xAAY#~c>8!U~p zBVLiOS$Mp0pa5F{`A|5f){n^1gsp7 z#HtyFxMSS51FS#x$iZ9n-iMxG0n>joqGx8T*tFPK?6)zZ6C<1$L1r|P(--7i>d(2x zHQxF4g+Dvzo-w9p?}m49Iiz~?ieV!PdT4qzr{EB9pqqN!r z848RCVRdn+V#{KS`QTK6&N8NS>hi6i%o1R%0n^+db-XHX1Q)b* zyIq`(>n3}To84oI>2?;;-4AhJyXRC1SN ztDa%mSkG_jj++}5vp(@19SEW)`%=8)x(mzT#8#U39^75lQln=;k;bID>@1ipUFS&wN2 z>)Mu}M%{uWzNLyZxIktwRX~GakQmSglmTfVW#a}|)uwWiXzgQYK%motr(9G!$p~vy zlgd(JP#aVRr9okkR|r8WY-04z#SpNijE3kmX6_C VQKE06&LF%7{Q)JmqCLw8007gNhHC%- literal 789 zcmV+w1M2)AiwFP!00000|D{w-kJ~s5z57?>*6s8nQr`>o5CjdBOM57wV+XQ6+F)nm zG)brJzprG=v63woSTqNRr1(g_XUcy)tj=HDF`id1@pRq~hrd^1_3*m8e0BT73tF=6 z-0?JoZ$6&Ef_wAEqGguvrsL@!EUP}PK2{%g4Vq5Crd+N?ZyE>}pO2THR#d#$)=9w1 z*(6pq7~;5dS!3w7T&4^x^vFg+6WA*=x5nUMJ!UzhZnVh~M=kk2c z^{)5M?{4BH*hc1@k-eMVgDWXxps#^`&hWLND1uBTw=kQ`;`XW-T}Ech$o!6G)=^q* zflLi%Ls(q{s`|3}q7_b6Xj3tlQ@8I5s+ItA4_I`AJn^Q!D_C!wAD)j-@e)HmqHgo} zemKNNu7?sm?+>4I&Tz1Z?$ea_ad?h4m)N@{Y zrRx<|oLzgeT~A^|*60+^!_!O5)5>~@K(1$FLRnDLFd3m*iaCYfQ-ng1w-i~S$gdQ0 zv31>PUYFw2Xy#VZ^~32je2?MP^FJA}8IJoHCVbi-+*8qNAM$g1J+-5zBRp>s%agtx zQ&_J3C7$+|$9-_0WBJQ@9aBB>vEE1Ibm5&T$YnA zd%?}6PQAyNyAa?(+iu!$(Npey@GvwwLm8#Q%H{X;dIAL-5_}*dj z4HV@f?S320=q6mQR~wKeWv*Y>LR4Q?UseCM!5>xHmS5Ke>IL(X2}ynOgbVH&^qvS6 zqd*Z?!f?Y3HE6()j!|7QNerx~NGNljqCgDP1*dwM(}5bu$zXsOZIqFnS2Qv~QwUlm zml8pZI)NlUQAK)OAv2gepg}N53}^$&fHaV+aRaRD717{T;!Jp?fr_9aWJ?kf6-t-e zQesdWR0gF%VUTw^(ipiGLPsG(@;>q4lF|+Z^g&?(!9B>4KITDbRGf?4NQXp3FC8Wb TkmA@0??Jx+HlI}I%Lf1e92SC` diff --git a/creusot/tests/should_succeed/iterators/15_enumerate.mlcfg b/creusot/tests/should_succeed/iterators/15_enumerate.mlcfg index 203ccebd0d..06e3e4af14 100644 --- a/creusot/tests/should_succeed/iterators/15_enumerate.mlcfg +++ b/creusot/tests/should_succeed/iterators/15_enumerate.mlcfg @@ -760,7 +760,6 @@ module C15Enumerate_Impl0 use seq.Seq use seq.Seq use seq.Seq - use seq.Seq predicate produces0 [#"../15_enumerate.rs" 28 4 28 64] (self : C15Enumerate_Enumerate_Type.t_enumerate i) (visited : Seq.seq (usize, item0)) (o : C15Enumerate_Enumerate_Type.t_enumerate i) = @@ -777,6 +776,9 @@ module C15Enumerate_Impl0 val produces0 [#"../15_enumerate.rs" 28 4 28 64] (self : C15Enumerate_Enumerate_Type.t_enumerate i) (visited : Seq.seq (usize, item0)) (o : C15Enumerate_Enumerate_Type.t_enumerate i) : bool ensures { result = produces0 self visited o } + use seq.Seq + goal produces_refl_refn : [#"../15_enumerate.rs" 40 4 40 26] forall self : C15Enumerate_Enumerate_Type.t_enumerate i . inv0 self + -> inv0 self /\ (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) goal produces_trans_refn : [#"../15_enumerate.rs" 47 4 47 90] forall a : C15Enumerate_Enumerate_Type.t_enumerate i . forall ab : Seq.seq (usize, item0) . forall b : C15Enumerate_Enumerate_Type.t_enumerate i . forall bc : Seq.seq (usize, item0) . forall c : C15Enumerate_Enumerate_Type.t_enumerate i . inv0 c /\ inv1 bc /\ inv0 b /\ inv1 ab /\ inv0 a /\ produces0 b bc c /\ produces0 a ab b -> inv0 c @@ -786,8 +788,6 @@ module C15Enumerate_Impl0 /\ inv0 a /\ produces0 b bc c /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c -> produces0 a (Seq.(++) ab bc) c) - goal produces_refl_refn : [#"../15_enumerate.rs" 40 4 40 26] forall self : C15Enumerate_Enumerate_Type.t_enumerate i . inv0 self - -> inv0 self /\ (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) goal next_refn : [#"../15_enumerate.rs" 53 4 53 44] forall self : borrowed (C15Enumerate_Enumerate_Type.t_enumerate i) . inv2 self -> inv2 self /\ (forall result : Core_Option_Option_Type.t_option (usize, item0) . inv3 result diff --git a/creusot/tests/should_succeed/iterators/16_take.mlcfg b/creusot/tests/should_succeed/iterators/16_take.mlcfg index 63f28dd488..530e208ef6 100644 --- a/creusot/tests/should_succeed/iterators/16_take.mlcfg +++ b/creusot/tests/should_succeed/iterators/16_take.mlcfg @@ -369,75 +369,58 @@ end module C16Take_Impl0 type i type item0 - use seq.Seq - predicate invariant3 (self : Seq.seq item0) - val invariant3 (self : Seq.seq item0) : bool + use Core_Option_Option_Type as Core_Option_Option_Type + predicate invariant3 (self : Core_Option_Option_Type.t_option item0) + val invariant3 (self : Core_Option_Option_Type.t_option item0) : bool ensures { result = invariant3 self } - predicate inv3 (_x : Seq.seq item0) - val inv3 (_x : Seq.seq item0) : bool + predicate inv3 (_x : Core_Option_Option_Type.t_option item0) + val inv3 (_x : Core_Option_Option_Type.t_option item0) : bool ensures { result = inv3 _x } - axiom inv3 : forall x : Seq.seq item0 . inv3 x = true + axiom inv3 : forall x : Core_Option_Option_Type.t_option item0 . inv3 x = true use C16Take_Take_Type as C16Take_Take_Type - predicate invariant2 (self : C16Take_Take_Type.t_take i) - val invariant2 (self : C16Take_Take_Type.t_take i) : bool + use prelude.Borrow + predicate invariant2 (self : borrowed (C16Take_Take_Type.t_take i)) + val invariant2 (self : borrowed (C16Take_Take_Type.t_take i)) : bool ensures { result = invariant2 self } - predicate inv2 (_x : C16Take_Take_Type.t_take i) - val inv2 (_x : C16Take_Take_Type.t_take i) : bool + predicate inv2 (_x : borrowed (C16Take_Take_Type.t_take i)) + val inv2 (_x : borrowed (C16Take_Take_Type.t_take i)) : bool ensures { result = inv2 _x } - axiom inv2 : forall x : C16Take_Take_Type.t_take i . inv2 x = true - use Core_Option_Option_Type as Core_Option_Option_Type - predicate invariant1 (self : Core_Option_Option_Type.t_option item0) - val invariant1 (self : Core_Option_Option_Type.t_option item0) : bool + axiom inv2 : forall x : borrowed (C16Take_Take_Type.t_take i) . inv2 x = true + use seq.Seq + predicate invariant1 (self : Seq.seq item0) + val invariant1 (self : Seq.seq item0) : bool ensures { result = invariant1 self } - predicate inv1 (_x : Core_Option_Option_Type.t_option item0) - val inv1 (_x : Core_Option_Option_Type.t_option item0) : bool + predicate inv1 (_x : Seq.seq item0) + val inv1 (_x : Seq.seq item0) : bool ensures { result = inv1 _x } - axiom inv1 : forall x : Core_Option_Option_Type.t_option item0 . inv1 x = true - use prelude.Borrow - predicate invariant0 (self : borrowed (C16Take_Take_Type.t_take i)) - val invariant0 (self : borrowed (C16Take_Take_Type.t_take i)) : bool + axiom inv1 : forall x : Seq.seq item0 . inv1 x = true + predicate invariant0 (self : C16Take_Take_Type.t_take i) + val invariant0 (self : C16Take_Take_Type.t_take i) : bool ensures { result = invariant0 self } - predicate inv0 (_x : borrowed (C16Take_Take_Type.t_take i)) - val inv0 (_x : borrowed (C16Take_Take_Type.t_take i)) : bool + predicate inv0 (_x : C16Take_Take_Type.t_take i) + val inv0 (_x : C16Take_Take_Type.t_take i) : bool ensures { result = inv0 _x } - axiom inv0 : forall x : borrowed (C16Take_Take_Type.t_take i) . inv0 x = true - use seq.Seq - use seq.Seq - use seq.Seq - predicate produces1 [#"../common.rs" 8 4 8 65] (self : i) (visited : Seq.seq item0) (o : i) - val produces1 [#"../common.rs" 8 4 8 65] (self : i) (visited : Seq.seq item0) (o : i) : bool - ensures { result = produces1 self visited o } - - use prelude.Int - use seq.Seq - use prelude.UIntSize - predicate produces0 [#"../16_take.rs" 31 4 31 64] (self : C16Take_Take_Type.t_take i) (visited : Seq.seq item0) (o : C16Take_Take_Type.t_take i) - - = - [#"../16_take.rs" 32 8 34 9] UIntSize.to_int (C16Take_Take_Type.take_n self) - = UIntSize.to_int (C16Take_Take_Type.take_n o) + Seq.length visited - /\ produces1 (C16Take_Take_Type.take_iter self) visited (C16Take_Take_Type.take_iter o) - val produces0 [#"../16_take.rs" 31 4 31 64] (self : C16Take_Take_Type.t_take i) (visited : Seq.seq item0) (o : C16Take_Take_Type.t_take i) : bool - ensures { result = produces0 self visited o } - + axiom inv0 : forall x : C16Take_Take_Type.t_take i . inv0 x = true use seq.Seq predicate completed1 [#"../common.rs" 11 4 11 36] (self : borrowed i) val completed1 [#"../common.rs" 11 4 11 36] (self : borrowed i) : bool ensures { result = completed1 self } + use prelude.Int predicate resolve0 (self : borrowed (C16Take_Take_Type.t_take i)) = [#"../../../../../creusot-contracts/src/resolve.rs" 26 20 26 34] ^ self = * self val resolve0 (self : borrowed (C16Take_Take_Type.t_take i)) : bool ensures { result = resolve0 self } + use prelude.UIntSize predicate completed0 [#"../16_take.rs" 22 4 22 35] (self : borrowed (C16Take_Take_Type.t_take i)) = [#"../16_take.rs" 23 8 26 9] UIntSize.to_int (C16Take_Take_Type.take_n ( * self)) = 0 /\ resolve0 self \/ UIntSize.to_int (C16Take_Take_Type.take_n ( * self)) > 0 @@ -446,27 +429,44 @@ module C16Take_Impl0 val completed0 [#"../16_take.rs" 22 4 22 35] (self : borrowed (C16Take_Take_Type.t_take i)) : bool ensures { result = completed0 self } - goal next_refn : [#"../16_take.rs" 53 4 53 41] forall self : borrowed (C16Take_Take_Type.t_take i) . inv0 self - -> inv0 self - /\ (forall result : Core_Option_Option_Type.t_option item0 . inv1 result + use seq.Seq + use seq.Seq + use seq.Seq + predicate produces1 [#"../common.rs" 8 4 8 65] (self : i) (visited : Seq.seq item0) (o : i) + val produces1 [#"../common.rs" 8 4 8 65] (self : i) (visited : Seq.seq item0) (o : i) : bool + ensures { result = produces1 self visited o } + + use seq.Seq + predicate produces0 [#"../16_take.rs" 31 4 31 64] (self : C16Take_Take_Type.t_take i) (visited : Seq.seq item0) (o : C16Take_Take_Type.t_take i) + + = + [#"../16_take.rs" 32 8 34 9] UIntSize.to_int (C16Take_Take_Type.take_n self) + = UIntSize.to_int (C16Take_Take_Type.take_n o) + Seq.length visited + /\ produces1 (C16Take_Take_Type.take_iter self) visited (C16Take_Take_Type.take_iter o) + val produces0 [#"../16_take.rs" 31 4 31 64] (self : C16Take_Take_Type.t_take i) (visited : Seq.seq item0) (o : C16Take_Take_Type.t_take i) : bool + ensures { result = produces0 self visited o } + + goal produces_trans_refn : [#"../16_take.rs" 47 4 47 90] forall a : C16Take_Take_Type.t_take i . forall ab : Seq.seq item0 . forall b : C16Take_Take_Type.t_take i . forall bc : Seq.seq item0 . forall c : C16Take_Take_Type.t_take i . inv0 c + /\ inv1 bc /\ inv0 b /\ inv1 ab /\ inv0 a /\ produces0 b bc c /\ produces0 a ab b + -> inv0 c + /\ inv1 bc + /\ inv0 b + /\ inv1 ab + /\ inv0 a + /\ produces0 b bc c + /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c -> produces0 a (Seq.(++) ab bc) c) + goal produces_refl_refn : [#"../16_take.rs" 40 4 40 26] forall self : C16Take_Take_Type.t_take i . inv0 self + -> inv0 self /\ (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) + goal next_refn : [#"../16_take.rs" 53 4 53 41] forall self : borrowed (C16Take_Take_Type.t_take i) . inv2 self + -> inv2 self + /\ (forall result : Core_Option_Option_Type.t_option item0 . inv3 result /\ match result with | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self) end - -> inv1 result + -> inv3 result /\ match result with | Core_Option_Option_Type.C_None -> completed0 self | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self) end) - goal produces_refl_refn : [#"../16_take.rs" 40 4 40 26] forall self : C16Take_Take_Type.t_take i . inv2 self - -> inv2 self /\ (forall result : () . produces0 self (Seq.empty ) self -> produces0 self (Seq.empty ) self) - goal produces_trans_refn : [#"../16_take.rs" 47 4 47 90] forall a : C16Take_Take_Type.t_take i . forall ab : Seq.seq item0 . forall b : C16Take_Take_Type.t_take i . forall bc : Seq.seq item0 . forall c : C16Take_Take_Type.t_take i . inv2 c - /\ inv3 bc /\ inv2 b /\ inv3 ab /\ inv2 a /\ produces0 b bc c /\ produces0 a ab b - -> inv2 c - /\ inv3 bc - /\ inv2 b - /\ inv3 ab - /\ inv2 a - /\ produces0 b bc c - /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c -> produces0 a (Seq.(++) ab bc) c) end diff --git a/creusot/tests/should_succeed/iterators/16_take/why3session.xml b/creusot/tests/should_succeed/iterators/16_take/why3session.xml index 8b1d215963..5c62559519 100644 --- a/creusot/tests/should_succeed/iterators/16_take/why3session.xml +++ b/creusot/tests/should_succeed/iterators/16_take/why3session.xml @@ -21,14 +21,14 @@ - - + + - - + + diff --git a/creusot/tests/should_succeed/iterators/16_take/why3shapes.gz b/creusot/tests/should_succeed/iterators/16_take/why3shapes.gz index d50cd6e67e378dd357cac9db7f5393ac1763cf6e..9278d2197640be14e78bf50d25e5bde50d33d992 100644 GIT binary patch delta 935 zcmV;Y16cg92eJo{8Grny7+?>Ev4R8?y)@u4#)zU4Azo=~d$;Ys?~tM*$`Mc$^}*x} z-^@JDqsQ+b_SbLl;;;KRf4TPK@M*9155Mege?ULHF-yv{rIwaEc)5)2tMgZC8GQI) zxs_Jc)A6)2E0Zmf&6CaQELu!~Svt%mRs}Tp=a<{xR;PG9Gk+nr$bbZ{{@hL2xQ+11 zyNljaykMT12JS47_;=3Hra4tU1!n02`xSSUxX(RNOBeNuJ0KH)1{w#hUipJF_sp1h zIhgoCfJ8@=9L~I7(KEIs(&9`_$;duIO9DLT1hv2>T!&k(NgQXn4Ot|02XKyh@ zeS}9`QseFIb?Sd#-Zy6IDcDepl|W}DIHrIZf{~Z!U*Pk z3PS6uRbh@bD>aRM&O3gr~c+IF~L*3q1hl{sj{?~%hOn%#xk${a8u$P zeh0wE%$|}DQ5Z+pTq%6Mykb@vE6P5aQ}csEI5Kg;O?_7cUBBk3OBCT=y=ZfMU5{4a z#+369*?+7R<8n(e^e&2tAWg(giea+D^z-3qOvLk0iWl3`acQ|uz2iLej`K2a2j?*y zVWO-j>A2XCj`LYMJkF)Vd@%#xl8zb6*`0LdT~`tCab=@o@t&tz{B&!;O5wzOrj z{j9jtmT5;K*|51|5nQXhHSFwh-;J03;QzY)7=K)38C-Ok9Bi2!`S>MPgmEUV4&!Fa zixkmoP)cz}Tql&# z8swguiWU{s6~#zdQBhG|Q7lGx-gv`RC!4NyII#`UjuOM2H_jnvg0+~a7*b;uqZK1N z!CUGBoVx}(I1$Sa5L={yv)rW;YIOm=* zCLWFkeiTBYqe_lyjHpvVH7O{Af}^gu;44EzlrvMa4@2@Ou1>Z}ww#||4~cgjS`^4q zL$Z{gO%2H>U4MbOriSBgPj&zNa`HFd@D9-a_*;MWvyMCj@3lLB<(U5LK+=~X?)U!L zJBB#y>5(5Pb4M3{?N4t$pzTsYpn^_Uzu!-rsM2OwgnWm3mzt*MtXTG+SOK%bIV&{G z3MW>mpLT;(!5s>qqN=}K`aga1?)f_hex~m}?mCpzc7JC&ImoGN`2Q(wI~Pu$$8-)8 zjQJQMP%!p4f9Y<=uA#3!JUFfng#t4{H_kqGH-Cu$Pw|BL3IPYkK{l3$SRP`T*Y12X z>K*@wfR8hK06#}zYFKgw`h0n1R2?hoE}BF0gG1F~;KGZ;T@iNuI)^S;gnRX(E&1(w zbcz>wF@Ij`q&>wTNWH;*LddEpQLCaruus9R-n zYe{b*FCi&%L?kzIET;xXT3=p8@TBu57YFHwaC^orQ z1Xeap?xD%+Hr$XF^V&kCG~i^hUgB2y}6m_^1vUBalo HoCyE`?ZMAY diff --git a/creusot/tests/should_succeed/knapsack_full.mlcfg b/creusot/tests/should_succeed/knapsack_full.mlcfg index 776a577f26..93cd91c9da 100644 --- a/creusot/tests/should_succeed/knapsack_full.mlcfg +++ b/creusot/tests/should_succeed/knapsack_full.mlcfg @@ -1384,14 +1384,14 @@ module KnapsackFull_Knapsack01Dyn goto BB50 } BB18 { - [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _32; + [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _32; [#"../knapsack_full.rs" 88 4 88 55] _37 <- ([#"../knapsack_full.rs" 88 4 88 55] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem))); goto BB19 } BB19 { [#"../knapsack_full.rs" 88 4 88 55] produced <- _37; _37 <- any Snapshot.snap_ty (Seq.seq usize); - [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] i <- __creusot_proc_iter_elem; + [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] i <- __creusot_proc_iter_elem; [#"../knapsack_full.rs" 96 23 96 26] _41 <- ([#"../knapsack_full.rs" 96 23 96 26] index0 items i); goto BB20 } @@ -1488,14 +1488,14 @@ module KnapsackFull_Knapsack01Dyn goto BB12 } BB36 { - [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem1 <- Core_Option_Option_Type.some_0 _58; + [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem1 <- Core_Option_Option_Type.some_0 _58; [#"../knapsack_full.rs" 98 8 98 59] _63 <- ([#"../knapsack_full.rs" 98 8 98 59] Snapshot.new (Seq.(++) (Snapshot.inner produced1) (Seq.singleton __creusot_proc_iter_elem1))); goto BB37 } BB37 { [#"../knapsack_full.rs" 98 8 98 59] produced1 <- _63; _63 <- any Snapshot.snap_ty (Seq.seq usize); - [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] w <- __creusot_proc_iter_elem1; + [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] w <- __creusot_proc_iter_elem1; [#"../knapsack_full.rs" 111 38 111 51] _67 <- KnapsackFull_Item_Type.item_weight it > w; switch (_67) | False -> goto BB41 diff --git a/creusot/tests/should_succeed/rusthorn/inc_max_repeat.mlcfg b/creusot/tests/should_succeed/rusthorn/inc_max_repeat.mlcfg index a6d01b606c..3cb7bdd480 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_max_repeat.mlcfg +++ b/creusot/tests/should_succeed/rusthorn/inc_max_repeat.mlcfg @@ -332,7 +332,7 @@ module IncMaxRepeat_IncMaxRepeat end } BB10 { - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _18; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _18; [#"../inc_max_repeat.rs" 16 4 16 86] _23 <- ([#"../inc_max_repeat.rs" 16 4 16 86] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem))); goto BB11 } diff --git a/creusot/tests/should_succeed/selection_sort_generic.mlcfg b/creusot/tests/should_succeed/selection_sort_generic.mlcfg index eab4cefe59..722e0ce2c5 100644 --- a/creusot/tests/should_succeed/selection_sort_generic.mlcfg +++ b/creusot/tests/should_succeed/selection_sort_generic.mlcfg @@ -740,14 +740,14 @@ module SelectionSortGeneric_SelectionSort return _0 } BB12 { - [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _20; + [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _20; [#"../selection_sort_generic.rs" 35 4 35 43] _25 <- ([#"../selection_sort_generic.rs" 35 4 35 43] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem))); goto BB13 } BB13 { [#"../selection_sort_generic.rs" 35 4 35 43] produced <- _25; _25 <- any Snapshot.snap_ty (Seq.seq usize); - [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] i <- __creusot_proc_iter_elem; + [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] i <- __creusot_proc_iter_elem; [#"../selection_sort_generic.rs" 39 22 39 23] min <- i; [#"../selection_sort_generic.rs" 43 17 43 24] _32 <- i + ([#"../selection_sort_generic.rs" 43 22 43 23] (1 : usize)); @@ -817,14 +817,14 @@ module SelectionSortGeneric_SelectionSort goto BB32 } BB24 { - [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem1 <- Core_Option_Option_Type.some_0 _44; + [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem1 <- Core_Option_Option_Type.some_0 _44; [#"../selection_sort_generic.rs" 41 8 41 121] _49 <- ([#"../selection_sort_generic.rs" 41 8 41 121] Snapshot.new (Seq.(++) (Snapshot.inner produced1) (Seq.singleton __creusot_proc_iter_elem1))); goto BB25 } BB25 { [#"../selection_sort_generic.rs" 41 8 41 121] produced1 <- _49; _49 <- any Snapshot.snap_ty (Seq.seq usize); - [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] j <- __creusot_proc_iter_elem1; + [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] j <- __creusot_proc_iter_elem1; [#"../selection_sort_generic.rs" 44 16 44 19] _54 <- ([#"../selection_sort_generic.rs" 44 16 44 19] index0 ( * v) j); goto BB26 } diff --git a/creusot/tests/should_succeed/sum.mlcfg b/creusot/tests/should_succeed/sum.mlcfg index f9ad306608..52c11f6d80 100644 --- a/creusot/tests/should_succeed/sum.mlcfg +++ b/creusot/tests/should_succeed/sum.mlcfg @@ -292,14 +292,14 @@ module Sum_SumFirstN return _0 } BB11 { - [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _17; + [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _17; [#"../sum.rs" 8 4 8 67] _22 <- ([#"../sum.rs" 8 4 8 67] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem))); goto BB12 } BB12 { [#"../sum.rs" 8 4 8 67] produced <- _22; _22 <- any Snapshot.snap_ty (Seq.seq uint32); - [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] i <- __creusot_proc_iter_elem; + [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] i <- __creusot_proc_iter_elem; [#"../sum.rs" 10 8 10 16] sum <- sum + i; goto BB5 } diff --git a/creusot/tests/should_succeed/sum_of_odds.mlcfg b/creusot/tests/should_succeed/sum_of_odds.mlcfg index fcaf2c5f05..adc0ee4f05 100644 --- a/creusot/tests/should_succeed/sum_of_odds.mlcfg +++ b/creusot/tests/should_succeed/sum_of_odds.mlcfg @@ -299,14 +299,14 @@ module SumOfOdds_ComputeSumOfOdd return _0 } BB10 { - [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _18; + [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _18; [#"../sum_of_odds.rs" 38 4 38 50] _23 <- ([#"../sum_of_odds.rs" 38 4 38 50] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem))); goto BB11 } BB11 { [#"../sum_of_odds.rs" 38 4 38 50] produced <- _23; _23 <- any Snapshot.snap_ty (Seq.seq uint32); - [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] i <- __creusot_proc_iter_elem; + [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] i <- __creusot_proc_iter_elem; assert { [@expl:assertion] [#"../sum_of_odds.rs" 41 12 41 33] let _ = sum_of_odd_is_sqr0 (UInt32.to_int i) in true }; [#"../sum_of_odds.rs" 44 13 44 18] _29 <- ([#"../sum_of_odds.rs" 44 13 44 14] (2 : uint32)) * i; [#"../sum_of_odds.rs" 44 13 44 22] _28 <- _29 + ([#"../sum_of_odds.rs" 44 21 44 22] (1 : uint32)); diff --git a/creusot/tests/should_succeed/vector/01.mlcfg b/creusot/tests/should_succeed/vector/01.mlcfg index c0526875b5..921ebdfed4 100644 --- a/creusot/tests/should_succeed/vector/01.mlcfg +++ b/creusot/tests/should_succeed/vector/01.mlcfg @@ -456,14 +456,14 @@ module C01_AllZero return _0 } BB12 { - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _19; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _19; [#"../01.rs" 9 4 9 42] _24 <- ([#"../01.rs" 9 4 9 42] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem))); goto BB13 } BB13 { [#"../01.rs" 9 4 9 42] produced <- _24; _24 <- any Snapshot.snap_ty (Seq.seq usize); - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] i <- __creusot_proc_iter_elem; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] i <- __creusot_proc_iter_elem; [#"../01.rs" 12 8 12 9] _28 <- Borrow.borrow_mut ( * v); [#"../01.rs" 12 8 12 9] v <- { v with current = ( ^ _28) ; }; [#"../01.rs" 12 9 12 12] _27 <- ([#"../01.rs" 12 9 12 12] index_mut0 _28 i); diff --git a/creusot/tests/should_succeed/vector/03_knuth_shuffle.mlcfg b/creusot/tests/should_succeed/vector/03_knuth_shuffle.mlcfg index 4877ddda39..a7c725cd2e 100644 --- a/creusot/tests/should_succeed/vector/03_knuth_shuffle.mlcfg +++ b/creusot/tests/should_succeed/vector/03_knuth_shuffle.mlcfg @@ -480,14 +480,14 @@ module C03KnuthShuffle_KnuthShuffle return _0 } BB12 { - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _17; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _17; [#"../03_knuth_shuffle.rs" 16 4 16 43] _22 <- ([#"../03_knuth_shuffle.rs" 16 4 16 43] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem))); goto BB13 } BB13 { [#"../03_knuth_shuffle.rs" 16 4 16 43] produced <- _22; _22 <- any Snapshot.snap_ty (Seq.seq usize); - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] n <- __creusot_proc_iter_elem; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] n <- __creusot_proc_iter_elem; [#"../03_knuth_shuffle.rs" 20 20 20 27] _26 <- ([#"../03_knuth_shuffle.rs" 20 20 20 27] len0 ( * v)); goto BB14 } diff --git a/creusot/tests/should_succeed/vector/06_knights_tour.mlcfg b/creusot/tests/should_succeed/vector/06_knights_tour.mlcfg index 53246fd819..ae48c4b483 100644 --- a/creusot/tests/should_succeed/vector/06_knights_tour.mlcfg +++ b/creusot/tests/should_succeed/vector/06_knights_tour.mlcfg @@ -1575,14 +1575,14 @@ module C06KnightsTour_Impl1_CountDegree goto BB20 } BB13 { - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _17; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _17; [#"../06_knights_tour.rs" 73 8 73 46] _22 <- ([#"../06_knights_tour.rs" 73 8 73 46] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem))); goto BB14 } BB14 { [#"../06_knights_tour.rs" 73 8 73 46] produced <- _22; _22 <- any Snapshot.snap_ty (Seq.seq (isize, isize)); - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] m <- __creusot_proc_iter_elem; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] m <- __creusot_proc_iter_elem; assume { resolve1 __creusot_proc_iter_elem }; [#"../06_knights_tour.rs" 75 29 75 31] _28 <- m; [#"../06_knights_tour.rs" 75 23 75 32] next <- ([#"../06_knights_tour.rs" 75 23 75 32] mov0 p _28); @@ -2254,14 +2254,14 @@ module C06KnightsTour_Min return _0 } BB10 { - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _15; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _15; [#"../06_knights_tour.rs" 113 4 114 74] _20 <- ([#"../06_knights_tour.rs" 113 4 114 74] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem))); goto BB11 } BB11 { [#"../06_knights_tour.rs" 113 4 114 74] produced <- _20; _20 <- any Snapshot.snap_ty (Seq.seq (usize, C06KnightsTour_Point_Type.t_point)); - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] x <- __creusot_proc_iter_elem; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] x <- __creusot_proc_iter_elem; switch (min) | Core_Option_Option_Type.C_None -> goto BB13 | Core_Option_Option_Type.C_Some _ -> goto BB14 @@ -3057,14 +3057,14 @@ module C06KnightsTour_KnightsTour goto BB48 } BB15 { - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _35; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _35; [#"../06_knights_tour.rs" 142 4 142 36] _40 <- ([#"../06_knights_tour.rs" 142 4 142 36] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem))); goto BB16 } BB16 { [#"../06_knights_tour.rs" 142 4 142 36] produced <- _40; _40 <- any Snapshot.snap_ty (Seq.seq usize); - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] step <- __creusot_proc_iter_elem; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] step <- __creusot_proc_iter_elem; [#"../06_knights_tour.rs" 147 50 147 60] candidates <- ([#"../06_knights_tour.rs" 147 50 147 60] new1 ([#"../06_knights_tour.rs" 147 50 147 60] ())); goto BB17 } @@ -3134,14 +3134,14 @@ module C06KnightsTour_KnightsTour goto BB40 } BB31 { - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem1 <- Core_Option_Option_Type.some_0 _54; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem1 <- Core_Option_Option_Type.some_0 _54; [#"../06_knights_tour.rs" 148 8 149 54] _59 <- ([#"../06_knights_tour.rs" 148 8 149 54] Snapshot.new (Seq.(++) (Snapshot.inner produced1) (Seq.singleton __creusot_proc_iter_elem1))); goto BB32 } BB32 { [#"../06_knights_tour.rs" 148 8 149 54] produced1 <- _59; _59 <- any Snapshot.snap_ty (Seq.seq (isize, isize)); - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] m <- __creusot_proc_iter_elem1; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] m <- __creusot_proc_iter_elem1; assume { resolve2 __creusot_proc_iter_elem1 }; [#"../06_knights_tour.rs" 151 28 151 30] _65 <- m; [#"../06_knights_tour.rs" 151 22 151 31] adj <- ([#"../06_knights_tour.rs" 151 22 151 31] mov0 p _65); diff --git a/creusot/tests/should_succeed/vector/08_haystack.mlcfg b/creusot/tests/should_succeed/vector/08_haystack.mlcfg index 4e8104f9db..82531417bd 100644 --- a/creusot/tests/should_succeed/vector/08_haystack.mlcfg +++ b/creusot/tests/should_succeed/vector/08_haystack.mlcfg @@ -591,14 +591,14 @@ module C08Haystack_Search goto BB31 } BB13 { - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _24; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _24; [#"../08_haystack.rs" 22 4 22 112] _29 <- ([#"../08_haystack.rs" 22 4 22 112] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem))); goto BB14 } BB14 { [#"../08_haystack.rs" 22 4 22 112] produced <- _29; _29 <- any Snapshot.snap_ty (Seq.seq usize); - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] i <- __creusot_proc_iter_elem; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] i <- __creusot_proc_iter_elem; [#"../08_haystack.rs" 25 20 25 32] _36 <- ([#"../08_haystack.rs" 25 20 25 32] len0 needle); goto BB15 } @@ -654,14 +654,14 @@ module C08Haystack_Search goto BB32 } BB25 { - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem1 <- Core_Option_Option_Type.some_0 _45; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem1 <- Core_Option_Option_Type.some_0 _45; [#"../08_haystack.rs" 24 8 24 68] _50 <- ([#"../08_haystack.rs" 24 8 24 68] Snapshot.new (Seq.(++) (Snapshot.inner produced1) (Seq.singleton __creusot_proc_iter_elem1))); goto BB26 } BB26 { [#"../08_haystack.rs" 24 8 24 68] produced1 <- _50; _50 <- any Snapshot.snap_ty (Seq.seq usize); - [#"../../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] j <- __creusot_proc_iter_elem1; + [#"../../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] j <- __creusot_proc_iter_elem1; [#"../08_haystack.rs" 26 21 26 24] _55 <- ([#"../08_haystack.rs" 26 21 26 24] index0 needle j); goto BB27 }