creusot_std/logic/ra.rs
1//! Definitions of Resource Algebras
2
3pub mod agree;
4pub mod auth;
5pub mod excl;
6pub mod fmap;
7mod int;
8pub mod lattice;
9mod nat;
10pub mod option;
11mod positive;
12mod positive_real;
13pub mod prod;
14pub mod sum;
15pub mod update;
16pub mod view;
17
18#[cfg(creusot)]
19use crate::logic::such_that;
20use crate::{logic::Set, prelude::*};
21
22/// Define a _Resource Algebra_.
23///
24/// Resource algebras are a concept inspired by [Iris](https://iris-project.org/). Used in
25/// conjunction with [`Resource`](crate::ghost::resource::Resource)s, they unlock new reasonings.
26///
27/// # Notes on the definition of resource algebras
28///
29/// Our definition of resource algebras differs from the one in Iris in that it
30/// does not require RAs to define a "core" function. Instead, we follow "Idempotent
31/// Resources in Separation Logic --- The Heart of core in Iris" by Gratzer, Møller &
32/// Birkedal (GMB), and require RAs to satisfy a "maximal idempotent" axiom.
33pub trait RA: Sized {
34 /// The operation of this resource algebra.
35 ///
36 /// This is the core of the trait. This operation will be used to [`join`](crate::Resource::join)
37 /// and [`split`](crate::ghost::Resource::split) resources.
38 ///
39 /// It must be [associative](Self::associative) and [commutative](Self::commutative)
40 /// (among others).
41 #[logic]
42 fn op(self, other: Self) -> Option<Self>;
43
44 // Derived notions: `factor`, `incl`, `idemp`.
45 // We allow the implementor to give a custom definition, that is possibly
46 // simpler than the generic one. The custom definition is the one that
47 // will be used to prove the RA laws.
48
49 #[logic(open, inline)]
50 #[ensures(result == (self == other))]
51 fn eq(self, other: Self) -> bool {
52 self == other
53 }
54
55 /// Inclusion of RA.
56 ///
57 /// This asserts that `other` is, in a sense, 'bigger' than `self`.
58 ///
59 /// # Notes on reflexivity
60 ///
61 /// Following Iris, our definition of `incl` is not reflexive.
62 /// We could define it to be `self == other || ...`, but doing that
63 /// loses the following desirable property for the product RA:
64 ///
65 /// ```text
66 /// (x, y).incl((x', y')) == x.incl(x') && y.incl(y').
67 /// ```
68 ///
69 /// If you need the reflexive closure of the inclusion relation, then
70 /// you can use `Some(x).incl(Some(y))`. Indeed, `incl` on the Option RA
71 /// has the following property:
72 ///
73 /// ```text
74 /// Some(x).incl(Some(y)) == (x == y || x.incl(y))
75 /// ```
76 ///
77 /// Note that the paper on the maximal idempotent axiom (GMB) uses the
78 /// reflexive definition of `incl` on paper, but not in its accompanying
79 /// Iris formalization, where it uses the non-reflexive definition (as
80 /// we do here).
81 #[logic]
82 #[ensures(result == (exists<factor> self.op(factor) == Some(other)))]
83 fn incl(self, other: Self) -> bool;
84
85 #[logic(law)]
86 #[requires(self.op(other) == Some(comb))]
87 #[ensures(self.incl(comb))]
88 fn incl_op(self, other: Self, comb: Self) {}
89
90 #[logic(open, sealed)]
91 fn incl_eq(self, other: Self) -> bool {
92 self.eq(other) || self.incl(other)
93 }
94
95 #[logic(open, sealed)]
96 fn incl_eq_op(a: Self, b: Self, x: Self) -> bool {
97 match a.op(b) {
98 None => false,
99 Some(ab) => ab.incl_eq(x),
100 }
101 }
102
103 /// Factorizing elements of the RA
104 ///
105 /// Given `a` and `c`, this returns an element `b` such that `a = b.c`,
106 /// or returns `None` if there does not exists such an element.
107 #[logic]
108 #[requires(factor.incl(self))]
109 #[ensures(factor.op(result) == Some(self))]
110 fn factor(self, factor: Self) -> Self {
111 such_that(|r| factor.op(r) == Some(self))
112 }
113
114 /// Ensures that we can go from `self` to `x` without making composition with the frame invalid.
115 ///
116 /// This is used in [`Resource::update`](crate::resource::Resource::update).
117 #[logic(open, sealed)]
118 fn update(self, x: Self) -> bool {
119 pearlite! {
120 forall<y: Self> self.op(y) != None ==> x.op(y) != None
121 }
122 }
123
124 /// This is used in [`Resource::update_nondet`](crate::resource::Resource::update_nondet).
125 #[logic(open, sealed)]
126 fn update_nondet(self, s: Set<Self>) -> bool {
127 pearlite! {
128 forall<y: Self> self.op(y) != None ==>
129 exists<x: Self> s.contains(x) && x.op(y) != None
130 }
131 }
132
133 // Laws
134
135 /// [`Self::op`] is commutative.
136 #[logic(law)]
137 #[ensures(a.op(b) == b.op(a))]
138 fn commutative(a: Self, b: Self);
139
140 /// [`Self::op`] is associative.
141 ///
142 /// This version uses `and_then_logic` for brevity, but is not easily used by provers.
143 /// Thus, we have [`Self::associative_none`] and [`Self::associative_some`] as laws,
144 /// which are more friendly to provers.
145 #[logic]
146 #[ensures(a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc)))]
147 fn associative(a: Self, b: Self, c: Self);
148
149 /// Specialized version of [`Self::associative`], in the case where `a.op(b) == None`.
150 ///
151 /// By commutativity, it also covers the case where `b.op(c) == None`.
152 #[logic(law)]
153 #[requires(a.op(b) == None)]
154 #[requires(b.op(c) == Some(bc))]
155 #[ensures(a.op(bc) == None)]
156 fn associative_none(a: Self, b: Self, c: Self, bc: Self) {
157 Self::associative(a, b, c);
158 }
159
160 /// Specialized version of [`Self::associative`], in the case where `a.op(b)` and `b.op(c)`
161 /// are both valid.
162 ///
163 /// By commutativity, it also covers the case where `b.op(c) == None`.
164 #[logic(law)]
165 #[requires(a.op(b) == Some(ab))]
166 #[requires(b.op(c) == Some(bc))]
167 #[ensures(a.op(bc) == ab.op(c))]
168 fn associative_some(a: Self, b: Self, c: Self, ab: Self, bc: Self) {
169 Self::associative(a, b, c);
170 }
171
172 /// [`RA::incl`] is transitive.
173 #[logic(law)]
174 #[requires(a.incl(b))]
175 #[requires(b.incl(c))]
176 #[ensures(a.incl(c))]
177 fn incl_transitive(a: Self, b: Self, c: Self) {
178 let _ = Self::associative;
179 }
180
181 /// The core of an element, when it exists, is included in that element,
182 /// and idempotent. Note that the statement `c.op(self) == Some(self)` is
183 /// equivalent to `c.incl(self)` for idempotent elements.
184 ///
185 /// The specification of this function is not part of an ensures clause,
186 /// because it has a tendency to make the provers loop.
187 #[logic]
188 fn core(self) -> Option<Self>;
189
190 /// The specification of [`core`].
191 #[logic]
192 #[requires(self.core() != None)]
193 #[ensures({
194 let c = self.core().unwrap_logic();
195 c.op(c) == Some(c)
196 })]
197 #[ensures(self.core().unwrap_logic().op(self) == Some(self))]
198 fn core_idemp(self);
199
200 /// The core maximal among idempotent elements included in self
201 #[logic]
202 #[requires(i.op(i) == Some(i))]
203 #[requires(i.op(self) == Some(self))]
204 #[ensures(match self.core() {
205 Some(c) => i.incl(c),
206 None => false,
207 })]
208 fn core_is_maximal_idemp(self, i: Self);
209
210 /// Cancelation of resource algebra elements.
211 ///
212 /// An element `e` is said to be _cancelable_ if it can be removed from a
213 /// composition: `∀ x y , e · x = e · y → x = y`.
214 #[logic]
215 #[ensures(result == (forall<x, y> self.op(x) != None ==>
216 self.op(x) == self.op(y) ==> x == y))]
217 fn cancelable(self) -> bool {
218 pearlite! { forall<x, y> self.op(x) != None ==>
219 self.op(x) == self.op(y) ==> x == y
220 }
221 }
222}
223
224/// Unitary RAs are RA with a neutral element.
225pub trait UnitRA: RA {
226 /// The unit element
227 #[logic]
228 #[ensures(forall<x: Self> #[trigger(x.op(result))] x.op(result) == Some(x))]
229 fn unit() -> Self;
230
231 /// In unitary RAs, the inclusion relation is reflexive
232 #[logic(law)]
233 #[ensures(forall<x: Self> x.incl(x))]
234 fn incl_refl() {
235 let _ = Self::unit();
236 }
237
238 /// In unitary RAs, the core is a total function. For better automation, it
239 /// is given a simpler, total definition.
240 #[logic(open)]
241 #[ensures(self.core() == Some(result))]
242 fn core_total(self) -> Self {
243 self.core_is_maximal_idemp(Self::unit());
244 self.core().unwrap_logic()
245 }
246
247 /// The specification of [`core_total`]
248 #[logic]
249 #[ensures(self.core_total().op(self.core_total()) == Some(self.core_total()))]
250 #[ensures(self.core_total().op(self) == Some(self))]
251 fn core_total_idemp(self);
252
253 /// The unit is its own core
254 #[logic(law)]
255 #[ensures(Self::unit().core_total() == Self::unit())]
256 fn unit_core() {
257 Self::unit().core_idemp()
258 }
259}