1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
//! Some useful logical items

use crate::*;

/// A wrapper around `T` that makes it safe.
///
/// This type is indented to be used in logic code.
pub type SizedW<T> = Box<T>;

/// Helper trait to turn a `T` into a [`SizedW<T>`]
pub trait MakeSized {
    /// Turn a `T` into a [`SizedW<T>`]
    #[logic]
    #[why3::attr = "inline:trivial"]
    fn make_sized(&self) -> SizedW<Self>;
}

impl<T: ?Sized> MakeSized for T {
    #[trusted]
    #[logic]
    #[ensures(*result == *self)]
    fn make_sized(&self) -> SizedW<Self> {
        dead
    }
}

/// Creates a logical value satisfying the property given by `p`.
///
/// This is also called the "epsilon operator": its goal is not extract from `∃x. P(x)`
/// a `x` satisfying `P`.
#[trusted]
#[logic]
#[requires(exists<x: T> p[x])]
#[ensures(p[result])]
pub fn such_that<T>(p: crate::logic::Mapping<T, bool>) -> T {
    dead
}

/// Indicates unreachable code.
///
/// This function indicates a logical branch that should be impossible to reach.
#[trusted]
#[allow(unconditional_recursion)]
#[logic]
#[requires(false)]
#[ensures(false)]
#[variant(0)]
pub fn unreachable<T>() -> T {
    unreachable()
}

/// Returns the inner value of an [`Option`], given that it is not `None`
#[logic]
#[open(self)]
#[requires(op != None)]
#[ensures(Some(result) == op)]
pub fn unwrap<T>(op: Option<T>) -> T {
    match op {
        Some(t) => t,
        None => unreachable(),
    }
}