Fix Seq::get_mut_ghost (#1402)

creusot-rs · Mar 3, 2025 · 8b949c1 · 8b949c1
2 parents b4bedbe + f62ae77
commit 8b949c1
Show file tree

Hide file tree

Showing 6 changed files with 589 additions and 698 deletions.
diff --git a/creusot-contracts/src/logic/seq.rs b/creusot-contracts/src/logic/seq.rs
@@ -548,7 +548,7 @@ impl<T> Seq<T> {
         None => self.get(index) == None && *self == ^self,
         Some(r) => self.get(index) == Some(*r) && ^r == (^self)[index],
     })]
-    #[ensures(forall<i: Int> i != index ==> (*self).get(index) == (^self).get(index))]
+    #[ensures(forall<i: Int> i != index ==> (*self).get(i) == (^self).get(i))]
     #[ensures((*self).len() == (^self).len())]
     pub fn get_mut_ghost(&mut self, index: Int) -> Option<&mut T> {
         let _ = index;

diff --git a/tests/should_succeed/ghost/ghost_vec.coma b/tests/should_succeed/ghost/ghost_vec.coma
@@ -53,7 +53,7 @@ module M_ghost_vec__ghost_vec [#"ghost_vec.rs" 4 0 4 18]
   let%span sseq51 = "../../../creusot-contracts/src/logic/seq.rs" 553 30 553 34
   let%span sseq52 = "../../../creusot-contracts/src/logic/seq.rs" 553 4 553 65
   let%span sseq53 = "../../../creusot-contracts/src/logic/seq.rs" 547 14 550 5
-  let%span sseq54 = "../../../creusot-contracts/src/logic/seq.rs" 551 14 551 84
+  let%span sseq54 = "../../../creusot-contracts/src/logic/seq.rs" 551 14 551 76
   let%span sseq55 = "../../../creusot-contracts/src/logic/seq.rs" 552 14 552 44
   let%span sseq56 = "../../../creusot-contracts/src/logic/seq.rs" 580 31 580 35
   let%span sseq57 = "../../../creusot-contracts/src/logic/seq.rs" 580 4 580 49
@@ -219,7 +219,7 @@ module M_ghost_vec__ghost_vec [#"ghost_vec.rs" 4 0 4 18]
         | C_None'2 -> get'0 self.current index = C_None'0 /\ self.current = self.final
         | C_Some'1 r -> get'0 self.current index = C_Some'2 (r.current) /\ r.final = Seq.get self.final index
         end}
-      {[%#sseq54] forall i : int . i <> index  -> get'0 self.current index = get'0 self.final index}
+      {[%#sseq54] forall i : int . i <> index  -> get'0 self.current i = get'0 self.final i}
       {[%#sseq55] Seq.length self.current = Seq.length self.final}
       (! return' {result}) ]
 

diff --git a/tests/should_succeed/ghost/ghost_vec/proof.json b/tests/should_succeed/ghost/ghost_vec/proof.json
@@ -9,14 +9,97 @@
     "M_ghost_vec__ghost_vec": {
       "vc_deref'0": { "prover": "[email protected]", "time": 0.03 },
       "vc_deref_mut'0": { "prover": "[email protected]", "time": 0.017 },
-      "vc_get_ghost'0": { "prover": "[email protected]", "time": 0.04 },
+      "vc_get_ghost'0": { "prover": "[email protected]", "time": 0.018 },
       "vc_get_mut_ghost'0": { "prover": "[email protected]", "time": 0.03 },
-      "vc_ghost_vec'0": { "prover": "[email protected]", "time": 0.273 },
+      "vc_ghost_vec'0": {
+        "tactic": "split_vc",
+        "children": [
+          { "prover": "[email protected]", "time": 0.026 },
+          { "prover": "[email protected]", "time": 0.026 },
+          { "prover": "[email protected]", "time": 0.028 },
+          { "prover": "[email protected]", "time": 0.027 },
+          { "prover": "[email protected]", "time": 0.031 },
+          { "prover": "[email protected]", "time": 0.038 },
+          { "prover": "[email protected]", "time": 0.036 },
+          { "prover": "[email protected]", "time": 0.03 },
+          { "prover": "[email protected]", "time": 0.031 },
+          { "prover": "[email protected]", "time": 0.031 },
+          { "prover": "[email protected]", "time": 0.04 },
+          { "prover": "[email protected]", "time": 0.032 },
+          { "prover": "[email protected]", "time": 0.05 },
+          { "prover": "[email protected]", "time": 0.024 },
+          { "prover": "[email protected]", "time": 0.04 },
+          { "prover": "[email protected]", "time": 0.061 },
+          { "prover": "[email protected]", "time": 0.034 },
+          { "prover": "[email protected]", "time": 0.033 },
+          { "prover": "[email protected]", "time": 0.043 },
+          { "prover": "[email protected]", "time": 0.035 },
+          { "prover": "[email protected]", "time": 0.035 },
+          { "prover": "[email protected]", "time": 0.027 },
+          { "prover": "[email protected]", "time": 0.043 },
+          { "prover": "[email protected]", "time": 0.043 },
+          { "prover": "[email protected]", "time": 0.032 },
+          { "prover": "[email protected]", "time": 0.052 },
+          { "prover": "[email protected]", "time": 0.036 },
+          { "prover": "[email protected]", "time": 0.031 },
+          { "prover": "[email protected]", "time": 0.052 },
+          { "prover": "[email protected]", "time": 0.047 },
+          { "prover": "[email protected]", "time": 0.036 },
+          { "prover": "[email protected]", "time": 0.05 },
+          { "prover": "[email protected]", "time": 0.059 },
+          { "prover": "[email protected]", "time": 0.035 },
+          { "prover": "[email protected]", "time": 0.041 },
+          { "prover": "[email protected]", "time": 0.05 },
+          { "prover": "[email protected]", "time": 0.06 },
+          { "prover": "[email protected]", "time": 0.039 },
+          { "prover": "[email protected]", "time": 0.058 },
+          { "prover": "[email protected]", "time": 0.078 },
+          { "prover": "[email protected]", "time": 0.155 },
+          { "prover": "[email protected]", "time": 0.089 },
+          { "prover": "[email protected]", "time": 0.124 },
+          { "prover": "[email protected]", "time": 0.072 },
+          { "prover": "[email protected]", "time": 0.039 },
+          { "prover": "[email protected]", "time": 0.043 },
+          { "prover": "[email protected]", "time": 0.041 },
+          { "prover": "[email protected]", "time": 0.038 },
+          { "prover": "[email protected]", "time": 0.035 },
+          { "prover": "[email protected]", "time": 0.042 },
+          { "prover": "[email protected]", "time": 0.036 },
+          { "prover": "[email protected]", "time": 0.04 },
+          { "prover": "[email protected]", "time": 0.052 },
+          { "prover": "[email protected]", "time": 0.044 },
+          { "prover": "[email protected]", "time": 0.044 },
+          { "prover": "[email protected]", "time": 0.039 },
+          { "prover": "[email protected]", "time": 0.041 },
+          { "prover": "[email protected]", "time": 0.041 },
+          { "prover": "[email protected]", "time": 0.065 },
+          { "prover": "[email protected]", "time": 0.044 },
+          { "prover": "[email protected]", "time": 0.062 },
+          { "prover": "[email protected]", "time": 0.037 },
+          { "prover": "[email protected]", "time": 0.077 },
+          {
+            "tactic": "split_vc",
+            "children": [
+              { "prover": "[email protected]", "time": 0.036 },
+              { "prover": "[email protected]", "time": 1.1 }
+            ]
+          },
+          {
+            "tactic": "split_vc",
+            "children": [
+              { "prover": "[email protected]", "time": 0.037 },
+              { "prover": "[email protected]", "time": 0.854 }
+            ]
+          },
+          { "prover": "[email protected]", "time": 0.108 },
+          { "prover": "[email protected]", "time": 0.036 }
+        ]
+      },
       "vc_into_inner'0": { "prover": "[email protected]", "time": 0.018 },
       "vc_len_ghost'0": { "prover": "[email protected]", "time": 0.014 },
       "vc_new'0": { "prover": "[email protected]", "time": 0.012 },
       "vc_new'1": { "prover": "[email protected]", "time": 0.023 },
-      "vc_new'2": { "prover": "[email protected]", "time": 0.043 },
+      "vc_new'2": { "prover": "[email protected]", "time": 0.02 },
       "vc_pop_back_ghost'0": { "prover": "[email protected]", "time": 0.027 },
       "vc_pop_front_ghost'0": { "prover": "[email protected]", "time": 0.027 },
       "vc_push_back_ghost'0": { "prover": "[email protected]", "time": 0.014 },