creusot_contracts/ghost/resource/
fmap_view.rs

1//! A resource wrapping a [`FMap`] in a [`View`]
2//!
3//! This module defines a specialization of [`Resource`] for the case where you want:
4//! - A single, authoritative version of a [`FMap`]
5//! - Multiple fragments of such a map, that each assert that some key-value is in the
6//!   map.
7//!
8//! These are the [`Authority`] and [`Fragment`] types respectively.
9
10use super::Resource;
11#[cfg(creusot)]
12use crate::logic::Id;
13use crate::{
14    logic::{
15        FMap,
16        ra::{
17            agree::Ag,
18            auth::{Auth, AuthUpdate},
19            fmap::FMapInsertLocalUpdate,
20        },
21    },
22    prelude::*,
23};
24
25/// Inner value for [`Resource`] and [`Fragment`].
26type FMapAuth<K, V> = Resource<Auth<FMap<K, Ag<V>>>>;
27
28/// Wrapper around a [`Resource`], that allows to agree on the values of a [`FMap`].
29///
30/// This is the authoritative version
31pub struct Authority<K, V>(FMapAuth<K, V>);
32
33/// Wrapper around a [`Resource`], that allows to agree on the values of a [`FMap`].
34///
35/// This is the fragment version
36pub struct Fragment<K, V>(FMapAuth<K, V>, Snapshot<K>, Snapshot<V>);
37
38impl<K, V> Invariant for Authority<K, V> {
39    #[logic]
40    fn invariant(self) -> bool {
41        self.0.view().auth() != None
42    }
43}
44impl<K, V> Invariant for Fragment<K, V> {
45    #[logic]
46    fn invariant(self) -> bool {
47        pearlite! { self.0@.frag().get(*self.1) == Some(Ag(*self.2)) }
48    }
49}
50
51impl<K, V> View for Authority<K, V> {
52    type ViewTy = FMap<K, V>;
53
54    /// Get the authoritative version of the map.
55    #[logic]
56    fn view(self) -> FMap<K, V> {
57        self.0.view().auth().unwrap_logic().map(|(_, x): (K, Ag<V>)| x.0)
58    }
59}
60impl<K, V> View for Fragment<K, V> {
61    type ViewTy = (K, V);
62
63    /// Get the fragment of the map represented by this resource.
64    #[logic]
65    fn view(self) -> (K, V) {
66        (*self.1, *self.2)
67    }
68}
69
70impl<K, V> Authority<K, V> {
71    /// Id of the underlying [`Resource`].
72    #[logic]
73    pub fn id(self) -> Id {
74        self.0.id()
75    }
76
77    /// Create a new, empty authoritative map.
78    #[check(ghost)]
79    #[ensures(result@ == FMap::empty())]
80    pub fn new() -> Ghost<Self> {
81        let r =
82            ghost!(Self(Resource::alloc(snapshot!(Auth::new_auth(FMap::empty()))).into_inner()));
83        proof_assert!(r@.ext_eq(FMap::empty()));
84        r
85    }
86
87    /// Insert a new element in the authoritative map and return the corresponding
88    /// fragment.
89    #[requires(!self@.contains(*k))]
90    #[ensures((^self)@ == self@.insert(*k, *v))]
91    #[ensures((^self).id() == self.id())]
92    #[ensures(result@ == (*k, *v))]
93    #[ensures(result.id() == self.id())]
94    #[check(ghost)]
95    #[allow(unused_variables)]
96    pub fn insert(&mut self, k: Snapshot<K>, v: Snapshot<V>) -> Fragment<K, V> {
97        let s = snapshot!(*self);
98        self.0.update(AuthUpdate(FMapInsertLocalUpdate(k, snapshot!(Ag(*v)))));
99        proof_assert!(self@.ext_eq(s@.insert(*k, *v)));
100        Fragment(self.0.core(), k, v)
101    }
102
103    /// Asserts that the fragment represented by `frag` is contained in `self`.
104    #[requires(self.id() == frag.id())]
105    #[ensures(self@.get(frag@.0) == Some(frag@.1))]
106    #[check(ghost)]
107    #[allow(unused_variables)]
108    pub fn contains(&self, frag: &Fragment<K, V>) {
109        let new_resource = self.0.join_shared(&frag.0);
110        proof_assert!(new_resource@.frag().get(frag@.0) == Some(Ag(frag@.1)));
111    }
112}
113impl<K, V> Fragment<K, V> {
114    /// Id of the underlying [`Resource`].
115    #[logic]
116    pub fn id(self) -> Id {
117        self.0.id()
118    }
119}
120
121impl<K, V> Clone for Fragment<K, V> {
122    #[check(ghost)]
123    #[ensures(result@ == self@)]
124    #[ensures(result.id() == self.id())]
125    fn clone(&self) -> Self {
126        Self(self.0.core(), self.1, self.2)
127    }
128}
creusot_contracts/ghost/resource/fmap_view.rs

creusot_contracts/ghost/resource/
fmap_view.rs
