creusot_contracts/
resolve.rs

1//! Resolve mutable borrows
2use crate::prelude::*;
3
4/// This logical function is assumed as soon as a value leaves its scope. It states that the
5/// propheties of every mutable borrow appearing in it parameter is eaqual to its current value.
6///
7/// Its body is opaque, but Creusot automatically generates an axiom stating relevant properties
8/// depending on the definition of `T`.
9#[logic(prophetic, inline, open)]
10#[intrinsic("resolve")]
11pub fn resolve<T: ?Sized>(_: T) -> bool {
12    dead
13}
14
15/// The trait `Resolve` makes it possible to expose to clients a custom resolve assertion for
16/// opaque types.
17///
18/// For example, if a library defines a notion of finite mapping, it does not exposes the internal
19/// representation of the finite mapping data structure. Hence, the `resolve` predicate above wil be
20/// completely opaque for clients. This library should implement the `Resolve` trait in order to
21/// provide to the client a definition it can use. E.g., `Resolve::resolve` states that any element
22/// of the mapping is resolved.
23pub trait Resolve {
24    #[logic(prophetic)]
25    #[intrinsic("resolve_method")]
26    fn resolve(self) -> bool;
27
28    #[logic(prophetic)]
29    #[requires(inv(self))]
30    #[requires(structural_resolve(self))]
31    #[ensures(self.resolve())]
32    fn resolve_coherence(self);
33}
34
35#[logic(open, prophetic)]
36#[intrinsic("structural_resolve")]
37pub fn structural_resolve<T: ?Sized>(_: T) -> bool {
38    dead
39}
40
41// Instances for fundamental types, which make impossible
42
43impl<'a, T: ?Sized> Resolve for &'a T {
44    #[logic(open)]
45    #[creusot::trusted_trivial_if_param_trivial]
46    fn resolve(self) -> bool {
47        true
48    }
49
50    #[logic]
51    #[ensures(self.resolve())]
52    fn resolve_coherence(self) {}
53}
54
55impl<'a, T: ?Sized> Resolve for &'a mut T {
56    #[logic(open)]
57    fn resolve(self) -> bool {
58        true
59    }
60
61    #[logic]
62    #[ensures(self.resolve())]
63    fn resolve_coherence(self) {}
64}
creusot_contracts/resolve.rs

creusot_contracts/
resolve.rs
