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

creusot_std/logic/
ra.rs
