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