creusot_std/logic/ra/
option.rs

1#[cfg(creusot)]
2use crate::logic::such_that;
3use crate::{
4    logic::ra::{
5        RA, UnitRA,
6        update::{LocalUpdate, Update},
7    },
8    prelude::*,
9};
10
11impl<T: RA> RA for Option<T> {
12    #[logic(open)]
13    fn op(self, other: Self) -> Option<Self> {
14        match (self, other) {
15            (None, _) => Some(other),
16            (_, None) => Some(self),
17            (Some(x), Some(y)) => x.op(y).map_logic(|z| Some(z)),
18        }
19    }
20
21    #[logic(open)]
22    #[ensures(match result {
23        Some(c) => factor.op(c) == Some(self),
24        None => forall<c: Self> factor.op(c) != Some(self),
25    })]
26    fn factor(self, factor: Self) -> Option<Self> {
27        match (self, factor) {
28            (x, None) => Some(x),
29            (None, _) => None,
30            (Some(x), Some(y)) => match x.factor(y) {
31                Some(z) => Some(Some(z)),
32                None => {
33                    if x == y {
34                        Some(None)
35                    } else {
36                        None
37                    }
38                }
39            },
40        }
41    }
42
43    #[logic(open, inline)]
44    #[ensures(#[trigger(self == other)] result == (self == other))]
45    fn eq(self, other: Self) -> bool {
46        match (self, other) {
47            (Some(s), Some(o)) => s.eq(o),
48            (None, None) => true,
49            _ => false,
50        }
51    }
52
53    #[logic(law)]
54    #[ensures(a.op(b) == b.op(a))]
55    fn commutative(a: Self, b: Self) {
56        let _ = <T as RA>::commutative;
57    }
58
59    #[logic]
60    #[ensures(a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc)))]
61    fn associative(a: Self, b: Self, c: Self) {}
62
63    #[logic(open)]
64    fn core(self) -> Option<Self> {
65        match self {
66            None => Some(None),
67            Some(x) => Some(x.core()),
68        }
69    }
70
71    #[logic]
72    #[requires(self.core() != None)]
73    #[ensures({
74        let c = self.core().unwrap_logic();
75        c.op(c) == Some(c)
76    })]
77    #[ensures(self.core().unwrap_logic().op(self) == Some(self))]
78    fn core_idemp(self) {
79        self.core_total_idemp()
80    }
81
82    #[logic]
83    #[requires(i.op(i) == Some(i))]
84    #[requires(i.op(self) == Some(self))]
85    #[ensures(match self.core() {
86        Some(c) => i.incl(c),
87        None => false,
88    })]
89    fn core_is_maximal_idemp(self, i: Self) {
90        match (self, i) {
91            (Some(x), Some(i)) => x.core_is_maximal_idemp(i),
92            _ => (),
93        }
94    }
95
96    #[logic(open)]
97    #[ensures(result == (forall<x, y> self.op(x) != None ==>
98        self.op(x) == self.op(y) ==> x == y))]
99    fn cancelable(self) -> bool {
100        match self {
101            None => true,
102            Some(this) => {
103                proof_assert! {
104                    let _ = T::core_is_maximal_idemp;
105                    let _ = T::core_idemp;
106                    ((forall<x, y> self.op(x) != None ==> self.op(x) == self.op(y) ==> x == y) ==>
107                        self.op(this.core()) == self.op(None)) &&
108                    this.cancelable() ==> this.core() == None ==>
109                        forall<x, y> self.op(x) != None ==> self.op(x) == self.op(y) ==>
110                        match (x, y) {
111                            (Some(x), Some(y)) => this.op(x) != None && this.op(x) == this.op(y),
112                            (Some(x), None) | (None, Some(x)) => this.op(x) == Some(this),
113                            (None, None) => true,
114                        }
115                };
116                this.cancelable() && this.core() == None
117            }
118        }
119    }
120}
121
122impl<T: RA> UnitRA for Option<T> {
123    #[logic(open)]
124    #[ensures(forall<x: Self> #[trigger(x.op(result))] x.op(result) == Some(x))]
125    fn unit() -> Self {
126        None
127    }
128
129    #[logic(open)]
130    #[ensures(self.core() == Some(result))]
131    fn core_total(self) -> Self {
132        match self {
133            None => None,
134            Some(x) => x.core(),
135        }
136    }
137
138    #[logic]
139    #[ensures(self.core_total().op(self.core_total()) == Some(self.core_total()))]
140    #[ensures(self.core_total().op(self) == Some(self))]
141    fn core_total_idemp(self) {
142        let _ = T::core_idemp;
143    }
144}
145
146/// Apply an [update](Update) to the inner value of an [`Option`] resource.
147///
148/// This requires the resource to be in the `Some` state.
149///
150/// # Example
151///
152/// ```
153/// use creusot_std::{
154///     ghost::resource::Resource,
155///     logic::ra::{
156///         excl::{Excl, ExclUpdate},
157///         option::OptionUpdate,
158///     },
159///     prelude::*,
160/// };
161///
162/// let mut res = Resource::alloc(snapshot!(Some(Excl(1))));
163/// ghost! { res.update(OptionUpdate(ExclUpdate(snapshot!(2)))) };
164/// proof_assert!(res@ == Some(Excl(2)));
165/// ```
166pub struct OptionUpdate<U>(pub U);
167
168impl<R: RA, U: Update<R>> Update<Option<R>> for OptionUpdate<U> {
169    type Choice = U::Choice;
170
171    #[logic(open, inline)]
172    fn premise(self, from: Option<R>) -> bool {
173        match from {
174            Some(from) => self.0.premise(from),
175            None => false,
176        }
177    }
178
179    #[logic(open, inline)]
180    #[requires(self.premise(from))]
181    fn update(self, from: Option<R>, ch: U::Choice) -> Option<R> {
182        match from {
183            Some(from) => Some(self.0.update(from, ch)),
184            None => None, /* Dummy */
185        }
186    }
187
188    #[logic]
189    #[requires(self.premise(from))]
190    #[requires(from.op(frame) != None)]
191    #[ensures(self.update(from, result).op(frame) != None)]
192    fn frame_preserving(self, from: Option<R>, frame: Option<R>) -> U::Choice {
193        match frame {
194            Some(frame) => self.0.frame_preserving(from.unwrap_logic(), frame),
195            None => such_that(|_| true),
196        }
197    }
198}
199
200/// Apply an [update](LocalUpdate) to the inner value of an authority/fragment
201/// pair of [`Option`]s.
202///
203/// This requires that both the authority and the fragment are not `None`.
204pub struct OptionLocalUpdate<U>(pub U);
205
206impl<R: RA, U: LocalUpdate<R>> LocalUpdate<Option<R>> for OptionLocalUpdate<U> {
207    #[logic(open, inline)]
208    fn premise(self, from_auth: Option<R>, from_frag: Option<R>) -> bool {
209        match (from_auth, from_frag) {
210            (Some(from_auth), Some(from_frag)) => self.0.premise(from_auth, from_frag),
211            _ => false,
212        }
213    }
214
215    #[logic(open, inline)]
216    fn update(self, from_auth: Option<R>, from_frag: Option<R>) -> (Option<R>, Option<R>) {
217        match (from_auth, from_frag) {
218            (Some(from_auth), Some(from_frag)) => {
219                let (to_auth, to_frag) = self.0.update(from_auth, from_frag);
220                (Some(to_auth), Some(to_frag))
221            }
222            _ => (None, None), // Dummy
223        }
224    }
225
226    #[logic]
227    #[requires(self.premise(from_auth, from_frag))]
228    #[requires(Some(from_frag).op(frame) == Some(Some(from_auth)))]
229    #[ensures({
230        let (to_auth, to_frag) = self.update(from_auth, from_frag);
231        Some(to_frag).op(frame) == Some(Some(to_auth))
232    })]
233    fn frame_preserving(
234        self,
235        from_auth: Option<R>,
236        from_frag: Option<R>,
237        frame: Option<Option<R>>,
238    ) {
239        let frame = match frame {
240            None => None,
241            Some(f) => f,
242        };
243        self.0.frame_preserving(from_auth.unwrap_logic(), from_frag.unwrap_logic(), frame)
244    }
245}
creusot_std/logic/ra/option.rs

creusot_std/logic/ra/
option.rs
