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

creusot_std/ghost/
lifetime_logic.rs
