move external body stuff back to map.rs

verus-lang · Jul 28, 2023 · a882d52 · a882d52
1 parent a43b385
commit a882d52
Show file tree

Hide file tree

Showing 2 changed files with 78 additions and 78 deletions.
diff --git a/source/pervasive/map.rs b/source/pervasive/map.rs
@@ -115,6 +115,84 @@ impl<K, V> Map<K, V> {
     pub open spec fn ext_equal(self, m2: Map<K, V>) -> bool {
         self =~= m2
     }
+
+    #[verifier(external_body)]
+    pub proof fn tracked_empty() -> (tracked out_v: Self)
+        ensures
+            out_v == Map::<K, V>::empty(),
+    {
+        unimplemented!();
+    }
+
+    #[verifier(external_body)]
+    pub proof fn tracked_insert(tracked &mut self, key: K, tracked value: V)
+        ensures
+            *self == Map::insert(*old(self), key, value),
+    {
+        unimplemented!();
+    }
+
+    /// todo fill in documentation
+
+    #[verifier(external_body)]
+    pub proof fn tracked_remove(tracked &mut self, key: K) -> (tracked v: V)
+        requires
+            old(self).dom().contains(key),
+        ensures
+            *self == Map::remove(*old(self), key),
+            v == old(self)[key],
+    {
+        unimplemented!();
+    }
+
+    #[verifier(external_body)]
+    pub proof fn tracked_borrow(tracked &self, key: K) -> (tracked v: &V)
+        requires
+            self.dom().contains(key),
+        ensures
+            *v === self.index(key),
+    {
+        unimplemented!();
+    }
+
+    #[verifier(external_body)]
+    pub proof fn tracked_map_keys<J>(
+        tracked old_map: Map<K, V>,
+        key_map: Map<J, K>
+    ) -> (tracked new_map: Map<J, V>)
+        requires
+            forall |j| #![auto] key_map.dom().contains(j) ==> old_map.dom().contains(key_map.index(j)),
+            forall |j1, j2| #![auto]
+                !equal(j1, j2) && key_map.dom().contains(j1) && key_map.dom().contains(j2)
+                ==> !equal(key_map.index(j1), key_map.index(j2))
+        ensures
+            forall |j| #[trigger] new_map.dom().contains(j) <==> key_map.dom().contains(j),
+            forall |j| key_map.dom().contains(j) ==>
+                new_map.dom().contains(j) &&
+                #[trigger] new_map.index(j) == old_map.index(key_map.index(j)),
+    {
+        unimplemented!();
+    }
+
+    #[verifier(external_body)]
+    pub proof fn tracked_remove_keys(tracked &mut self, keys: Set<K>)
+        -> (tracked out_map: Map<K, V>)
+        requires
+            keys.subset_of(old(self).dom())
+        ensures
+            self == old(self).remove_keys(keys),
+            out_map == old(self).restrict(keys),
+    {
+        unimplemented!();
+    }
+
+    #[verifier(external_body)]
+    pub proof fn tracked_union_prefer_right(tracked &mut self, right: Self)
+        ensures
+            *self == old(self).union_prefer_right(right),
+    {
+        unimplemented!();
+    }
 }
 
 // Trusted axioms

diff --git a/source/pervasive/map_lib.rs b/source/pervasive/map_lib.rs
@@ -150,84 +150,6 @@ impl<K, V> Map<K, V> {
         )
     }
 
-    #[verifier(external_body)]
-    pub proof fn tracked_empty() -> (tracked out_v: Self)
-        ensures
-            out_v == Map::<K, V>::empty(),
-    {
-        unimplemented!();
-    }
-
-    #[verifier(external_body)]
-    pub proof fn tracked_insert(tracked &mut self, key: K, tracked value: V)
-        ensures
-            *self == Map::insert(*old(self), key, value),
-    {
-        unimplemented!();
-    }
-
-    /// todo fill in documentation
-
-    #[verifier(external_body)]
-    pub proof fn tracked_remove(tracked &mut self, key: K) -> (tracked v: V)
-        requires
-            old(self).dom().contains(key),
-        ensures
-            *self == Map::remove(*old(self), key),
-            v == old(self)[key],
-    {
-        unimplemented!();
-    }
-
-    #[verifier(external_body)]
-    pub proof fn tracked_borrow(tracked &self, key: K) -> (tracked v: &V)
-        requires
-            self.dom().contains(key),
-        ensures
-            *v === self.index(key),
-    {
-        unimplemented!();
-    }
-
-    #[verifier(external_body)]
-    pub proof fn tracked_map_keys<J>(
-        tracked old_map: Map<K, V>,
-        key_map: Map<J, K>
-    ) -> (tracked new_map: Map<J, V>)
-        requires
-            forall |j| #![auto] key_map.dom().contains(j) ==> old_map.dom().contains(key_map.index(j)),
-            forall |j1, j2| #![auto]
-                !equal(j1, j2) && key_map.dom().contains(j1) && key_map.dom().contains(j2)
-                ==> !equal(key_map.index(j1), key_map.index(j2))
-        ensures
-            forall |j| #[trigger] new_map.dom().contains(j) <==> key_map.dom().contains(j),
-            forall |j| key_map.dom().contains(j) ==>
-                new_map.dom().contains(j) &&
-                #[trigger] new_map.index(j) == old_map.index(key_map.index(j)),
-    {
-        unimplemented!();
-    }
-
-    #[verifier(external_body)]
-    pub proof fn tracked_remove_keys(tracked &mut self, keys: Set<K>)
-        -> (tracked out_map: Map<K, V>)
-        requires
-            keys.subset_of(old(self).dom())
-        ensures
-            self == old(self).remove_keys(keys),
-            out_map == old(self).restrict(keys),
-    {
-        unimplemented!();
-    }
-
-    #[verifier(external_body)]
-    pub proof fn tracked_union_prefer_right(tracked &mut self, right: Self)
-        ensures
-            *self == old(self).union_prefer_right(right),
-    {
-        unimplemented!();
-    }
-
     // Proven lemmas
 
     /// Removing a key from a map that previously contained that key results