creusot_std/ghost/
lifetime_logic.rs

1//! Encoding of Rustbelt's _lifetime logic_ in Creusot.
2//!
3//! The main types are [`FullBorrow`] and [`LifetimeToken`]; the first is
4//! a mutable borrow whose lifetime is tracked by Creusot rather than by the
5//! compiler. This lifetime is represented by a `LifetimeToken` object.
6
7#[cfg(creusot)]
8use crate::{ghost::Objective, resolve::structural_resolve};
9use crate::{
10    ghost::{FnGhost, NotObjective, Plain, resource::Resource},
11    invariant::{Guard, GuardRef, Guarded},
12    logic::{Id, ops::Fin, real::PositiveReal},
13    prelude::*,
14};
15use core::marker::PhantomData;
16
17/// Abstract representation of a lifetime.
18///
19/// Used to identify a lifetime in [`LifetimeToken`] and [`LifetimeDead`].
20///
21/// To differentiate this from a normal Rust lifetime (e.g. `'a`), we call the
22/// former a _syntactic_ lifetime, while this is a _synthetic_ lifetime.
23#[derive(Copy)]
24pub struct Lifetime(Id);
25
26impl Clone for Lifetime {
27    #[check(ghost)]
28    #[ensures(result == *self)]
29    fn clone(&self) -> Self {
30        *self
31    }
32}
33
34impl Plain for Lifetime {
35    #[check(ghost)]
36    #[ensures(*result == *snap)]
37    #[allow(unused_variables)]
38    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> {
39        let s: Snapshot<Id> = snapshot!(snap.0);
40        ghost!(Self(s.into_ghost().into_inner()))
41    }
42}
43
44/// A token signaling that the corresponding lifetime is still active.
45///
46/// This token is not duplicable, but it may be [split](Self::split) into
47/// multiple other tokens. Each token has an associated [fraction](Self::frac);
48/// if it is `1`, the lifetime may be [killed](LifetimeDead) to end borrows made
49/// at this lifetime.
50///
51/// This type is purely ghost, and all operations on its values compile to no-ops.
52// FIXME: do not wrap this in `Ghost`
53pub struct LifetimeToken(Ghost<Resource<PositiveReal>>);
54
55impl LifetimeToken {
56    /// The fraction owned by this particular token.
57    ///
58    /// If the token owns the full fraction (`1`), it can be used to end the
59    /// lifetime.
60    #[logic]
61    pub fn frac(self) -> PositiveReal {
62        self.0.val()
63    }
64
65    /// The lifetime identifier associated with this particular token.
66    ///
67    /// Only tokens with the same lifetime can be combined.
68    #[logic]
69    pub fn lft(self) -> Lifetime {
70        Lifetime(self.0.id())
71    }
72
73    /// Get a full lifetime token for a fresh lifetime.
74    #[check(ghost)]
75    #[ensures(result.frac() == PositiveReal::from_int(1))]
76    pub fn new() -> Self {
77        Self(Resource::alloc(snapshot!(PositiveReal::from_int(1))))
78    }
79
80    /// Split a lifetime token into two tokens, by dividing its fraction by 2.
81    #[check(ghost)]
82    #[ensures(result.0.lft() == self.lft() && result.1.lft() == self.lft())]
83    #[ensures(result.0.frac() + result.1.frac() == self.frac())]
84    #[ensures(result.0.frac() == self.frac() / PositiveReal::from_int(2)
85           && result.1.frac() == self.frac() / PositiveReal::from_int(2))]
86    pub fn split(self) -> (Self, Self) {
87        let (r1, r2) = ghost! {
88            let q = snapshot!(self.frac() / PositiveReal::from_int(2));
89            self.0.into_inner().split(q, q)
90        }
91        .split();
92        (Self(r1), Self(r2))
93    }
94
95    /// Split a lifetime token from this token, by removing half of the token's
96    /// fraction and giving it to the result.
97    #[check(ghost)]
98    #[ensures(result.lft() == self.lft() && (^self).lft() == (*self).lft())]
99    #[ensures(result.frac() + (^self).frac() == self.frac())]
100    #[ensures(result.frac() == self.frac() / PositiveReal::from_int(2) && (^self).frac() == self.frac() / PositiveReal::from_int(2))]
101    pub fn split_off(&mut self) -> Self {
102        Self(ghost! {
103            let half = snapshot!(self.frac() / PositiveReal::from_int(2));
104            self.0.split_off(half, half)
105        })
106    }
107
108    /// Combine two lifetime tokens together, adding their fractions.
109    #[check(ghost)]
110    #[requires(self.lft() == other.lft())]
111    #[ensures(result.lft() == self.lft())]
112    #[ensures(result.frac() == self.frac() + other.frac())]
113    pub fn join(self, other: Self) -> Self {
114        Self(ghost!(self.0.into_inner().join(other.0.into_inner())))
115    }
116
117    /// Same as [Self::join], but with a mutable borrow.
118    #[check(ghost)]
119    #[requires(self.lft() == other.lft())]
120    #[ensures((^self).lft() == self.lft())]
121    #[ensures((^self).frac() == self.frac() + other.frac())]
122    pub fn join_in(&mut self, other: Self) {
123        ghost! { self.0.join_in(other.0.into_inner()) };
124    }
125
126    /// Terminates the lifetime, giving back a 'dead' token.
127    #[check(ghost)]
128    #[requires(self.frac() == PositiveReal::from_int(1))]
129    #[ensures(result.lft() == self.lft())]
130    pub fn end(self) -> LifetimeDead {
131        LifetimeDead(snapshot!(self.lft()))
132    }
133}
134
135impl Default for LifetimeToken {
136    #[check(ghost)]
137    #[ensures(result.frac() == PositiveReal::from_int(1))]
138    fn default() -> Self {
139        Self::new()
140    }
141}
142
143/// A [lifetime](LifetimeToken) that has expired.
144///
145/// This token is freely duplicable.
146///
147/// It may be used to [get back](EndBorrow::get) the value that was originally
148/// borrowed.
149#[derive(Copy)]
150pub struct LifetimeDead(Snapshot<Lifetime>);
151
152impl Clone for LifetimeDead {
153    #[ensures(result == *self)]
154    fn clone(&self) -> Self {
155        *self
156    }
157}
158
159impl LifetimeDead {
160    /// The lifetime associated with this particular token.
161    #[logic]
162    pub fn lft(self) -> Lifetime {
163        *self.0
164    }
165}
166
167/// A mutable borrow, with a synthetic lifetime.
168///
169/// Correct usage of this borrow (e.g. non-aliasing) is checked by respecting
170/// the contracts of the associated functions.
171///
172/// Objects of this type may only be [constructed in ghost](FullBorrow::new).
173#[opaque]
174pub struct FullBorrow<T>(PhantomData<(*mut T, NotObjective)>);
175
176#[trusted]
177unsafe impl<T: Send> Send for FullBorrow<T> {}
178#[trusted]
179unsafe impl<T: Sync> Sync for FullBorrow<T> {}
180
181#[cfg(creusot)]
182#[trusted]
183impl<T: Objective> Objective for FullBorrow<T> {}
184
185/// Container for the final value of a [`FullBorrow`].
186///
187/// Can be used to get back the original value once the lifetime of the borrow
188/// is finished, by using [`EndBorrow::get`].
189#[opaque]
190pub struct EndBorrow<T>(PhantomData<(*mut T, NotObjective)>);
191
192#[trusted]
193unsafe impl<T: Send> Send for EndBorrow<T> {}
194#[trusted]
195unsafe impl<T: Sync> Sync for EndBorrow<T> {}
196
197#[cfg(creusot)]
198#[trusted]
199impl<T: Objective> Objective for EndBorrow<T> {}
200
201impl<T> Fin for FullBorrow<T> {
202    type Target = T;
203
204    #[logic(opaque, prophetic)]
205    fn fin<'a>(self) -> &'a T {
206        dead
207    }
208}
209
210impl<T> Resolve for FullBorrow<T> {
211    #[logic(open, prophetic)]
212    fn resolve(self) -> bool {
213        pearlite! { self.cur() == ^self }
214    }
215
216    #[trusted]
217    #[logic(prophetic)]
218    #[requires(inv(self))]
219    #[requires(structural_resolve(self))]
220    #[ensures(self.resolve())]
221    fn resolve_coherence(self) {}
222}
223
224impl<T> Invariant for FullBorrow<T> {
225    #[logic(open, prophetic, inline)]
226    #[creusot::trusted_trivial_if_param_trivial]
227    fn invariant(self) -> bool {
228        pearlite! { inv(self.cur()) && inv(^self) }
229    }
230}
231
232impl<G: GuardRef<T>, T> Guard<FullBorrow<T>> for G {
233    #[logic(open, prophetic, inline)]
234    fn guards(self, initial: FullBorrow<T>, current: FullBorrow<T>) -> bool {
235        pearlite! { self.guards_ref(current.cur()) && ^initial == ^current }
236    }
237}
238
239impl<T> FullBorrow<T> {
240    /// The lifetime of this borrow
241    #[logic(opaque)]
242    pub fn lft(self) -> Lifetime {
243        dead
244    }
245
246    /// The current value of this borrow.
247    #[logic(opaque)]
248    pub fn cur(self) -> T {
249        dead
250    }
251
252    /// The final value of this borrow.
253    ///
254    /// Also accessible with the final operator `^`.
255    #[logic(open, prophetic)]
256    pub fn fin(self) -> T {
257        pearlite! { ^self }
258    }
259
260    /// Create a new full borrow of the value `x`.
261    ///
262    /// Note that it also gives back a value of type [`EndBorrow`], that
263    /// can be used to get back the original value once the lifetime of the
264    /// borrow has ended.
265    ///
266    /// # in Rustbelt
267    ///
268    /// This is the 'LftL-borrow' rule.
269    #[trusted]
270    #[check(ghost)]
271    #[ensures(result.0.cur() == *x)]
272    #[ensures(result.0.lft() == *lft && result.1.lft() == *lft)]
273    #[ensures(^result.0 == ^result.1)]
274    #[allow(unused_variables)]
275    pub fn new(x: Ghost<T>, lft: Snapshot<Lifetime>) -> (Ghost<Self>, Ghost<EndBorrow<T>>) {
276        (Ghost::conjure(), Ghost::conjure())
277    }
278
279    /// Adds a guard to a mutable borrow.
280    /// This is analoguous to `Guarded::<&mut T>::new`, but for `FullBorrow`.
281    #[trusted]
282    #[check(ghost)]
283    #[requires((*guard).guards_ref(self.cur()))]
284    #[ensures(result.inner == self)]
285    #[ensures(result.guard() == *guard)]
286    #[ensures((*guard).guards_ref(^self))]
287    #[allow(unused_variables)]
288    pub fn add_guard<G: GuardRef<T>>(self, guard: Snapshot<G>) -> Guarded<Self, G> {
289        unreachable!("ghost code only")
290    }
291
292    /// Get an immutable borrow to read the value.
293    ///
294    /// The `token` object ensures that the lifetime of the `FullBorrow` has not
295    /// expired yet.
296    #[trusted]
297    #[check(ghost)]
298    #[requires(self.lft() == token.lft())]
299    #[ensures(*result == self.cur())]
300    #[allow(unused_variables)]
301    pub fn borrow<'a>(&'a self, token: &'a LifetimeToken) -> &'a T {
302        unreachable!("ghost code only")
303    }
304
305    /// Get a mutable borrow to write into the value.
306    ///
307    /// The `token` object ensures that the lifetime of the `FullBorrow` has not
308    /// expired yet.
309    ///
310    /// Functionally equivalent to a reborrow.
311    ///
312    /// # In Rustbelt
313    ///
314    /// This is the rule 'LftL-bor-unnest' (but mixed between syntactic and
315    /// synthetic lifetimes).
316    #[trusted]
317    #[check(ghost)]
318    #[requires(self.lft() == token.lft())]
319    #[ensures((^self).lft() == self.lft())]
320    #[ensures(^^self == ^*self)]
321    #[ensures((*self).cur() == *result && (^self).cur() == ^result)]
322    #[allow(unused_variables)]
323    pub fn borrow_mut<'a>(&'a mut self, token: &'a LifetimeToken) -> &'a mut T {
324        unreachable!("ghost code only")
325    }
326
327    /// Change the type of a full borrow.
328    ///
329    /// This is similar to [`std::cell::RefMut::map`].
330    #[trusted]
331    #[check(ghost)]
332    #[requires(self.lft() == token.lft())]
333    #[requires(forall<b: &mut T> *b == self.cur() && ^b == ^self ==>
334        f.precondition((b,)))]
335    #[ensures(exists<b: &mut T, res: &mut U>
336        *b == self.cur() && ^b == ^self && *res == result.cur() && ^res == ^result &&
337        f.postcondition_once((b,), res)
338    )]
339    #[ensures(result.lft() == self.lft())]
340    #[allow(unused_variables)]
341    pub fn map<U, F>(self, f: F, token: &LifetimeToken) -> FullBorrow<U>
342    where
343        F: for<'a> FnOnce(&'a mut T) -> &'a mut U + FnGhost,
344    {
345        unreachable!("ghost code only")
346    }
347}
348
349macro_rules! tuple_split {
350    ( $map_split:ident $( ($name:ident, $idx:tt) )+ ) => {
351        impl<$($name),+> FullBorrow<($($name,)+)> {
352            // FIXME: docs
353            #[trusted]
354            #[check(ghost)]
355            $(
356                #[ensures(result.$idx.lft() == self.lft())]
357                #[ensures(result.$idx.cur() == self.cur().$idx && ^result.$idx == (^self).$idx)]
358            )+
359            pub fn split(self) -> ($(FullBorrow<$name>,)+){
360                unreachable!("ghost code only")
361            }
362        }
363
364        impl<T0> FullBorrow<T0> {
365            #[trusted]
366            #[check(ghost)]
367            #[requires(self.lft() == token.lft())]
368            #[requires(forall<b: &mut T0> *b == self.cur() && ^b == ^self ==>
369                f.precondition((b,)))]
370            #[ensures(exists<b: &mut T0, res: ($(&mut $name,)+)>
371                *b == self.cur() && ^b == ^self &&
372                $(*res.$idx == result.$idx.cur() && ^res.$idx == ^result.$idx &&)+
373                f.postcondition_once((b,), res)
374            )]
375            $(
376                #[ensures(result.$idx.lft() == self.lft())]
377            )+
378            #[allow(unused_variables)]
379            pub fn $map_split<$($name,)+ F>(self, f: F, token: &LifetimeToken) -> ($(FullBorrow<$name>,)+)
380            where
381                F: for<'a> FnOnce(&'a mut T0) -> ($(&'a mut $name,)+) + FnGhost,
382            {
383                unreachable!("ghost code only")
384            }
385        }
386    };
387}
388
389tuple_split! { map_split_1  (T,0) }
390tuple_split! { map_split_2  (U,0) (T,1) }
391tuple_split! { map_split_3  (V,0) (U,1) (T,2) }
392tuple_split! { map_split_4  (W,0) (V,1) (U,2) (T,3) }
393tuple_split! { map_split_5  (X,0) (W,1) (V,2) (U,3) (T,4) }
394tuple_split! { map_split_6  (Y,0) (X,1) (W,2) (V,3) (U,4) (T,5) }
395tuple_split! { map_split_7  (Z,0) (Y,1) (X,2) (W,3) (V,4) (U,5) (T,6) }
396tuple_split! { map_split_8  (A,0) (Z,1) (Y,2) (X,3) (W,4) (V,5) (U,6) (T,7) }
397tuple_split! { map_split_9  (B,0) (A,1) (Z,2) (Y,3) (X,4) (W,5) (V,6) (U,7) (T,8) }
398tuple_split! { map_split_10 (C,0) (B,1) (A,2) (Z,3) (Y,4) (X,5) (W,6) (V,7) (U,8) (T,9) }
399tuple_split! { map_split_11 (D,0) (C,1) (B,2) (A,3) (Z,4) (Y,5) (X,6) (W,7) (V,8) (U,9) (T,10) }
400tuple_split! { map_split_12 (E,0) (D,1) (C,2) (B,3) (A,4) (Z,5) (Y,6) (X,7) (W,8) (V,9) (U,10) (T,11) }
401
402impl<T> Fin for EndBorrow<T> {
403    type Target = T;
404    #[logic(opaque, prophetic)]
405    fn fin<'a>(self) -> &'a T {
406        dead
407    }
408}
409
410impl<T> EndBorrow<T> {
411    /// Lifetime associated with the corresponding borrow.
412    #[logic(opaque)]
413    pub fn lft(self) -> Lifetime {
414        dead
415    }
416
417    /// Get back the original value used to create the corresponding borrow.
418    #[trusted]
419    #[check(ghost)]
420    #[requires(self.lft() == lft_dead.lft())]
421    #[ensures(result == ^self)]
422    #[allow(unused_variables)]
423    pub fn get(self, lft_dead: LifetimeDead) -> T {
424        unreachable!("ghost code only")
425    }
426}
creusot_std/ghost/lifetime_logic.rs

creusot_std/ghost/
lifetime_logic.rs
