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

creusot_std/logic/ra/
option.rs
