creusot_contracts/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)]
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)]
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)]
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)]
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
74pub trait LocalUpdate<R: RA>: Sized {
75    #[logic]
76    fn premise(self, from_auth: R, from_frag: R) -> bool;
77
78    #[logic]
79    fn update(self, from_auth: R, from_frag: R) -> (R, R);
80
81    #[logic]
82    #[requires(self.premise(from_auth, from_frag))]
83    #[requires(Some(from_frag).op(frame) == Some(Some(from_auth)))]
84    #[ensures({
85        let (to_auth, to_frag) = self.update(from_auth, from_frag);
86        Some(to_frag).op(frame) == Some(Some(to_auth))
87    })]
88    fn frame_preserving(self, from_auth: R, from_frag: R, frame: Option<R>);
89}
90
91impl<R: RA> LocalUpdate<R> for Snapshot<(R, R)> {
92    #[logic(open)]
93    fn premise(self, from_auth: R, from_frag: R) -> bool {
94        pearlite! {
95            forall<f: Option<R>>
96                Some(from_frag).op(f) == Some(Some(from_auth)) ==>
97                Some(self.1).op(f) == Some(Some(self.0))
98        }
99    }
100
101    #[logic(open)]
102    fn update(self, _: R, _: R) -> (R, R) {
103        *self
104    }
105
106    #[logic]
107    #[allow(unused)]
108    #[requires(LocalUpdate::premise(self, from_auth, from_frag))]
109    #[requires(Some(from_frag).op(frame) == Some(Some(from_auth)))]
110    #[ensures({
111        let (to_auth, to_frag) = LocalUpdate::update(self, from_auth, from_frag);
112        Some(to_frag).op(frame) == Some(Some(to_auth))
113    })]
114    fn frame_preserving(self, from_auth: R, from_frag: R, frame: Option<R>) {}
115}
creusot_contracts/logic/ra/update.rs

creusot_contracts/logic/ra/
update.rs
