creusot_std/logic/
ra.rs

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

creusot_std/logic/
ra.rs
