creusot_std/logic/ra/
update.rs

1#[cfg(creusot)]
2use crate::logic::such_that;
3use crate::{
4    logic::{Mapping, ra::RA},
5    prelude::*,
6};
7
8pub trait Update<R: RA> {
9    type Choice;
10
11    #[logic]
12    fn premise(self, from: R) -> bool;
13
14    #[logic]
15    #[requires(self.premise(from))]
16    fn update(self, from: R, ch: Self::Choice) -> R;
17
18    #[logic]
19    #[requires(self.premise(from))]
20    #[requires(from.op(frame) != None)]
21    #[ensures(self.update(from, result).op(frame) != None)]
22    fn frame_preserving(self, from: R, frame: R) -> Self::Choice;
23}
24
25impl<R: RA> Update<R> for Snapshot<R> {
26    type Choice = ();
27
28    #[logic(open, inline)]
29    fn premise(self, from: R) -> bool {
30        pearlite! {
31            forall<y: R> from.op(y) != None ==> self.op(y) != None
32        }
33    }
34
35    #[logic(open, inline)]
36    #[requires(self.premise(from))]
37    fn update(self, from: R, _: ()) -> R {
38        *self
39    }
40
41    #[logic]
42    #[requires(self.premise(from))]
43    #[requires(from.op(frame) != None)]
44    #[ensures(self.update(from, result).op(frame) != None)]
45    fn frame_preserving(self, from: R, frame: R) {}
46}
47
48impl<R: RA, Choice> Update<R> for Snapshot<Mapping<Choice, R>> {
49    type Choice = Choice;
50
51    #[logic(open, inline)]
52    fn premise(self, from: R) -> bool {
53        pearlite! {
54            forall<y: R> from.op(y) != None ==>
55                exists<ch: Choice> self[ch].op(y) != None
56        }
57    }
58
59    #[logic(open, inline)]
60    #[requires(self.premise(from))]
61    fn update(self, from: R, ch: Choice) -> R {
62        self[ch]
63    }
64
65    #[logic]
66    #[requires(self.premise(from))]
67    #[requires(from.op(frame) != None)]
68    #[ensures(self.update(from, result).op(frame) != None)]
69    fn frame_preserving(self, from: R, frame: R) -> Choice {
70        such_that(|ch| self.update(from, ch).op(frame) != None)
71    }
72}
73
74impl<R: RA> Update<R> for () {
75    type Choice = ();
76
77    #[logic(open, inline)]
78    fn premise(self, _: R) -> bool {
79        true
80    }
81
82    #[logic(open, inline)]
83    fn update(self, from: R, _: ()) -> R {
84        from
85    }
86
87    #[logic]
88    #[requires(from.op(frame) != None)]
89    #[ensures(from.op(frame) != None)]
90    fn frame_preserving(self, from: R, frame: R) {}
91}
92
93pub trait LocalUpdate<R: RA>: Sized {
94    #[logic]
95    fn premise(self, from_auth: R, from_frag: R) -> bool;
96
97    #[logic]
98    fn update(self, from_auth: R, from_frag: R) -> (R, R);
99
100    #[logic]
101    #[requires(self.premise(from_auth, from_frag))]
102    #[requires(Some(from_frag).op(frame) == Some(Some(from_auth)))]
103    #[ensures({
104        let (to_auth, to_frag) = self.update(from_auth, from_frag);
105        Some(to_frag).op(frame) == Some(Some(to_auth))
106    })]
107    fn frame_preserving(self, from_auth: R, from_frag: R, frame: Option<R>);
108}
109
110impl<R: RA> LocalUpdate<R> for Snapshot<(R, R)> {
111    #[logic(open, inline)]
112    fn premise(self, from_auth: R, from_frag: R) -> bool {
113        pearlite! {
114            forall<f: Option<R>>
115                Some(from_frag).op(f) == Some(Some(from_auth)) ==>
116                Some(self.1).op(f) == Some(Some(self.0))
117        }
118    }
119
120    #[logic(open, inline)]
121    fn update(self, _: R, _: R) -> (R, R) {
122        *self
123    }
124
125    #[logic]
126    #[allow(unused)]
127    #[requires(LocalUpdate::premise(self, from_auth, from_frag))]
128    #[requires(Some(from_frag).op(frame) == Some(Some(from_auth)))]
129    #[ensures({
130        let (to_auth, to_frag) = LocalUpdate::update(self, from_auth, from_frag);
131        Some(to_frag).op(frame) == Some(Some(to_auth))
132    })]
133    fn frame_preserving(self, from_auth: R, from_frag: R, frame: Option<R>) {}
134}
135
136impl<R: RA> LocalUpdate<R> for () {
137    #[logic(open, inline)]
138    fn premise(self, _: R, _: R) -> bool {
139        true
140    }
141
142    #[logic(open, inline)]
143    fn update(self, from_auth: R, from_frag: R) -> (R, R) {
144        (from_auth, from_frag)
145    }
146
147    #[logic]
148    #[requires(Some(frag).op(frame) == Some(Some(auth)))]
149    #[ensures(Some(frag).op(frame) == Some(Some(auth)))]
150    fn frame_preserving(self, auth: R, frag: R, frame: Option<R>) {}
151}
creusot_std/logic/ra/update.rs

creusot_std/logic/ra/
update.rs
