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(),
}
}