creusot_contracts/logic/
mapping.rs

1use crate::{logic::ops::IndexLogic, prelude::*};
2use std::marker::PhantomData;
3
4/// A mapping: map every value of type `A` to a value of type `B`.
5///
6/// # Pearlite syntax
7///
8/// Mappings have special support in pearlite code: you may write a closure to create a
9/// mapping.
10///
11/// ## Example
12///
13/// ```
14/// # use creusot_contracts::{logic::Mapping, prelude::*};
15/// let value = snapshot!(4);
16/// let map: Snapshot<Mapping<Int, Int>> = snapshot!(|n| if n % 2 == 0 { 0 } else { *value });
17/// proof_assert!(map.get(1) == 4);
18/// ```
19#[builtin("map.Map.map")]
20pub struct Mapping<A: ?Sized, B>(PhantomData<A>, PhantomData<B>);
21
22impl<A: ?Sized, B> Mapping<A, B> {
23    /// Get the value associated with `a` in the map.
24    #[logic]
25    #[builtin("map.Map.get")]
26    #[allow(unused_variables)]
27    pub fn get(self, a: A) -> B {
28        dead
29    }
30
31    /// Returns a new mapping, where `a` is now mapped to `b`.
32    #[logic]
33    #[builtin("map.Map.set")]
34    #[allow(unused_variables)]
35    pub fn set(self, a: A, b: B) -> Self {
36        dead
37    }
38
39    /// Create a mapping, where every value of type `a` is mapped to `b`.
40    #[logic]
41    #[builtin("map.Const.const")]
42    #[allow(unused_variables)]
43    pub fn cst(b: B) -> Self {
44        dead
45    }
46
47    /// Extensional equality.
48    ///
49    /// Returns `true` if `self` and `other` contain exactly the same key-value pairs.
50    ///
51    /// This is in fact equivalent with normal equality.
52    #[logic]
53    #[builtin("map.MapExt.(==)")]
54    #[allow(unused_variables)]
55    pub fn ext_eq(self, x: Self) -> bool {
56        dead
57    }
58}
59
60impl<A: ?Sized, B> IndexLogic<A> for Mapping<A, B> {
61    type Item = B;
62
63    #[logic(open, inline)]
64    fn index_logic(self, a: A) -> B {
65        self.get(a)
66    }
67}
creusot_contracts/logic/mapping.rs

creusot_contracts/logic/
mapping.rs
