1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
use crate::{logic::ops::IndexLogic, *};

/// A mapping: map every value of type `A` to a value of type `B`.
///
/// # Pearlite syntax
///
/// Mappings have special support in pearlite code: you may write a closure to create a
/// mapping.
///
/// ## Example
///
/// ```
/// # use creusot_contracts::{logic::Mapping, *};
/// let value = snapshot!(4);
/// let map: Snapshot<Mapping<Int, Int>> = snapshot!(|n| if n % 2 == 0 { 0 } else { *value });
/// proof_assert!(map.get(1) == 4);
/// ```
#[trusted]
#[cfg_attr(creusot, creusot::builtins = "map.Map.map")]
pub struct Mapping<A: ?Sized, B: ?Sized>(std::marker::PhantomData<A>, std::marker::PhantomData<B>);

impl<A: ?Sized, B: ?Sized> Mapping<A, B> {
    /// Get the value associated with `a` in the map.
    #[trusted]
    #[logic]
    #[creusot::builtins = "map.Map.get"]
    #[allow(unused_variables)]
    pub fn get(self, a: A) -> B
    where
        B: Sized, // TODO : don't require this (problem: return type needs to be sized)
    {
        dead
    }

    /// Returns a new mapping, where `a` is now mapped to `b`.
    #[trusted]
    #[logic]
    #[creusot::builtins = "map.Map.set"]
    #[allow(unused_variables)]
    pub fn set(self, a: A, b: B) -> Self {
        dead
    }

    /// Create a mapping, where every value of type `a` is mapped to `b`.
    #[trusted]
    #[logic]
    #[creusot::builtins = "map.Const.const"]
    #[allow(unused_variables)]
    pub fn cst(b: B) -> Self {
        dead
    }
}

impl<A: ?Sized, B> IndexLogic<A> for Mapping<A, B> {
    type Item = B;

    #[logic]
    #[open]
    fn index_logic(self, a: A) -> B {
        self.get(a)
    }
}