creusot_std/logic/ra/
option.rs

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

creusot_std/logic/ra/
option.rs
