Indexing of FMap in logic

creusot-contracts/src/logic/fmap.rs

@@ -1,4 +1,8 @@
-use crate::{logic::Mapping, util::*, *};
+use crate::{
+    logic::{ops::IndexLogic, Mapping},
+    util::*,
+    *,
+};
 
 #[cfg_attr(not(creusot), allow(dead_code))]
 type PMap<K, V> = Mapping<K, Option<SizedW<V>>>;
@@ -26,6 +30,15 @@ pub struct FMap<K, V: ?Sized>(std::marker::PhantomData<K>, std::marker::PhantomD
 
 /// Logical definitions
 impl<K, V: ?Sized> FMap<K, V> {
+    /// Returns the empty map.
+    #[trusted]
+    #[logic]
+    #[ensures(result.len() == 0)]
+    #[ensures(result.view() == Mapping::cst(None))]
+    pub fn empty() -> Self {
+        dead
+    }
+
     #[trusted]
     #[logic]
     #[ensures(result >= 0)]
@@ -107,14 +120,6 @@ impl<K, V: ?Sized> FMap<K, V> {
         self.get_unsized(k) != None
     }
 
-    #[trusted]
-    #[logic]
-    #[ensures(result.len() == 0)]
-    #[ensures(result.view() == Mapping::cst(None))]
-    pub fn empty() -> Self {
-        dead
-    }
-
     #[logic]
     #[open]
     pub fn is_empty(self) -> bool {
@@ -184,6 +189,17 @@ impl<K, V: ?Sized> FMap<K, V> {
     }
 }
 
+impl<K, V> IndexLogic<K> for FMap<K, V> {
+    type Item = V;
+
+    #[logic]
+    #[open]
+    #[why3::attr = "inline:trivial"]
+    fn index_logic(self, key: K) -> Self::Item {
+        self.lookup(key)
+    }
+}
+
 /// Ghost definitions
 impl<K, V: ?Sized> FMap<K, V> {
     /// Create a new, empty map on the ghost heap.

creusot-contracts/src/logic/fset.rs

@@ -28,6 +28,13 @@ impl<T: ?Sized> FSet<T> {
     #[creusot::builtins = "set.Fset.empty"]
     pub const EMPTY: Self = { FSet(std::marker::PhantomData) };
 
+    /// Returns the empty set.
+    #[logic]
+    #[open]
+    pub fn empty() -> Self {
+        Self::EMPTY
+    }
+
     #[open]
     #[predicate]
     #[why3::attr = "inline:trivial"]
@@ -141,7 +148,7 @@ impl<T: ?Sized> FSet<T> {
     #[ensures(result.is_empty())]
     #[allow(unreachable_code)]
     pub fn new() -> GhostBox<Self> {
-        ghost!(loop {})
+        ghost!(panic!())
     }
 
     /// Returns the number of elements in the set.

creusot-contracts/src/logic/seq.rs

@@ -47,6 +47,13 @@ impl<T: ?Sized> Seq<T> {
     #[creusot::builtins = "seq.Seq.empty"]
     pub const EMPTY: Self = { Seq(std::marker::PhantomData) };
 
+    /// Returns the empty sequence.
+    #[logic]
+    #[open]
+    pub fn empty() -> Self {
+        Self::EMPTY
+    }
+
     /// Create a new sequence in pearlite.
     ///
     /// The new sequence will be of length `n`, and will contain `mapping[i]` at index `i`.
@@ -252,7 +259,7 @@ impl<T> Seq<T> {
     #[ensures(*result == Self::EMPTY)]
     #[allow(unreachable_code)]
     pub fn new() -> GhostBox<Self> {
-        ghost!(loop {})
+        ghost!(panic!())
     }
 
     /// Returns the number of elements in the sequence, also referred to as its 'length'.

creusot/tests/should_succeed/fmap_indexing.rs

@@ -0,0 +1,12 @@
+extern crate creusot_contracts;
+use creusot_contracts::{logic::FMap, *};
+
+pub fn foo() {
+    let mut map = snapshot!(FMap::empty());
+    map = snapshot!(map.insert(1, 3));
+    proof_assert!(map[1] == 3);
+    map = snapshot!(map.insert(2, 42));
+    proof_assert!(map[1] == 3 && map[2] == 42);
+    map = snapshot!(map.insert(1, 4));
+    proof_assert!(map[1] == 4 && map[2] == 42);
+}