creusot_std/logic/
mapping.rs

1use crate::{logic::ops::IndexLogic, prelude::*};
2use core::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_std::{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")]
20#[trusted(positive(B))]
21pub struct Mapping<A: ?Sized, B>(PhantomData<fn(&A) -> B>);
22
23impl<A: ?Sized, B> Mapping<A, B> {
24    /// Get the value associated with `a` in the map.
25    #[logic]
26    #[builtin("map.Map.get")]
27    #[allow(unused_variables)]
28    pub fn get(self, a: A) -> B {
29        dead
30    }
31
32    /// Returns a new mapping, where `a` is now mapped to `b`.
33    #[logic]
34    #[builtin("map.Map.set")]
35    #[allow(unused_variables)]
36    pub fn set(self, a: A, b: B) -> Self {
37        dead
38    }
39
40    /// Create a mapping, where every value of type `a` is mapped to `b`.
41    #[logic]
42    #[builtin("map.Const.const")]
43    #[allow(unused_variables)]
44    pub fn cst(b: B) -> Self {
45        dead
46    }
47
48    /// Extensional equality.
49    ///
50    /// Returns `true` if `self` and `other` contain exactly the same key-value pairs.
51    ///
52    /// This is in fact equivalent with normal equality.
53    #[logic]
54    #[builtin("map.MapExt.(==)")]
55    #[allow(unused_variables)]
56    pub fn ext_eq(self, x: Self) -> bool {
57        dead
58    }
59}
60
61impl<A: ?Sized, B> IndexLogic<A> for Mapping<A, B> {
62    type Item = B;
63
64    #[logic(open, inline)]
65    fn index_logic(self, a: A) -> B {
66        self.get(a)
67    }
68}
creusot_std/logic/mapping.rs

creusot_std/logic/
mapping.rs
