creusot_contracts/cell/
predcell.rs

1//! Cell over predicates
2//!
3//! This module provides [PredCell], a wrapper around `std::cell::Cell` that allows predicates to be used to specify the contents of the cell.
4
5use crate::{logic::Mapping, prelude::*};
6
7/// Cell over predicates
8///
9/// A wrapper around `std::cell::Cell` that allows predicates to be used to specify the contents of the cell.
10#[opaque]
11#[repr(transparent)]
12pub struct PredCell<T: ?Sized>(std::cell::Cell<T>);
13
14impl<T: ?Sized> View for PredCell<T> {
15    type ViewTy = Mapping<T, bool>;
16
17    #[logic(opaque)]
18    fn view(self) -> Self::ViewTy {
19        dead
20    }
21}
22
23impl<T> PredCell<T> {
24    /// See the method [`Cell::new`](https://doc.rust-lang.org/std/cell/struct.Cell.html#method.new) documentation.
25    #[trusted]
26    #[requires(_pred[v])]
27    #[ensures(result@ == *_pred)]
28    pub const fn new(v: T, _pred: Snapshot<Mapping<T, bool>>) -> Self {
29        Self(std::cell::Cell::new(v))
30    }
31
32    /// See the method [`Cell::set`](https://doc.rust-lang.org/std/cell/struct.Cell.html#method.set) documentation.
33    #[trusted]
34    #[requires(self@[v])]
35    pub fn set(&self, v: T) {
36        self.0.set(v)
37    }
38
39    /// See the method [`Cell::swap`](https://doc.rust-lang.org/std/cell/struct.Cell.html#method.swap) documentation.
40    #[trusted]
41    #[requires(forall<x: T> self@[x] == other@[x])]
42    pub fn swap(&self, other: &PredCell<T>) {
43        self.0.swap(&other.0)
44    }
45
46    /// See the method [`Cell::replace`](https://doc.rust-lang.org/std/cell/struct.Cell.html#method.replace) documentation.
47    #[trusted]
48    #[requires(self@[v])]
49    #[ensures(self@[result])]
50    pub const fn replace(&self, v: T) -> T {
51        self.0.replace(v)
52    }
53
54    /// See the method [`Cell::into_inner`](https://doc.rust-lang.org/std/cell/struct.Cell.html#method.into_inner) documentation.
55    #[trusted]
56    #[ensures(self@[result])]
57    pub fn into_inner(self) -> T {
58        self.0.into_inner()
59    }
60}
61
62impl<T: Copy> PredCell<T> {
63    /// See the method [`Cell::get`](https://doc.rust-lang.org/std/cell/struct.Cell.html#method.get) documentation.
64    #[trusted]
65    #[ensures(self@[result])]
66    pub const fn get(&self) -> T {
67        self.0.get()
68    }
69
70    /// See the method [`Cell::update`](https://doc.rust-lang.org/std/cell/struct.Cell.html#method.update) documentation.
71    #[trusted]
72    #[requires(forall<x: T> self@[x] ==> f.precondition((x,)))]
73    #[requires(forall<x: T, res: T> self@[x] && f.postcondition_once((x,), res) ==> self@[res])]
74    #[ensures(exists<x: T, res: T> self@[x] && f.postcondition_once((x,), res))]
75    pub fn update(&self, f: impl FnOnce(T) -> T) {
76        self.0.update(f);
77    }
78}
79
80impl<T: ?Sized> PredCell<T> {
81    /// See the method [`Cell::from_mut`](https://doc.rust-lang.org/std/cell/struct.Cell.html#method.from_mut) documentation.
82    #[trusted]
83    #[requires(_pred[*t])]
84    #[ensures(_pred[^t])]
85    #[ensures(result@ == *_pred)]
86    pub const fn from_mut(t: &mut T, _pred: Snapshot<Mapping<T, bool>>) -> &PredCell<T> {
87        unsafe { std::mem::transmute(std::cell::Cell::from_mut(t)) }
88    }
89
90    // TODO: Find a way to write the `get_mut` function
91}
92
93impl<T: Default> PredCell<T> {
94    /// See the method [`Cell::take`](https://doc.rust-lang.org/std/cell/struct.Cell.html#method.take) documentation.
95    #[trusted]
96    #[requires(forall<x: T> T::default.postcondition((), x) ==> self@[x])]
97    #[ensures(self@[result])]
98    pub fn take(&self) -> T {
99        self.0.take()
100    }
101}
102
103impl<T> PredCell<[T]> {
104    /// See the method [`Cell::as_slice_of_cells`](https://doc.rust-lang.org/std/cell/struct.Cell.html#method.as_slice_of_cells) documentation.
105    #[trusted]
106    #[requires(forall<s: [T]> self@[s] == (_pred.len() == s@.len() && forall<i: Int> 0 <= i && i < s@.len() ==> _pred[i][s[i]]))]
107    #[ensures(forall<i: Int> 0 <= i && i < _pred.len() ==> result[i]@ == _pred[i])]
108    #[ensures(result@.len() == _pred.len())]
109    pub const fn as_slice_of_cells(
110        &self,
111        _pred: Snapshot<Seq<Mapping<T, bool>>>,
112    ) -> &[PredCell<T>] {
113        unsafe { std::mem::transmute(self.0.as_slice_of_cells()) }
114    }
115}
creusot_contracts/cell/predcell.rs

creusot_contracts/cell/
predcell.rs
