creusot_contracts/
logic.rs

1//! Definitions for pearlite code
2//!
3//! This contains types and traits that are meant to be used in logical code.
4
5#![cfg_attr(not(creusot), allow(unused_imports))]
6use crate::prelude::*;
7
8mod fmap;
9pub mod fset;
10mod id;
11mod int;
12mod mapping;
13pub mod ops;
14pub mod ord;
15pub mod ra;
16pub mod real;
17pub mod seq;
18mod set;
19mod well_founded;
20
21// TODO: do not alias these names. decide either to re-export them, or use a submodule.
22pub use self::{
23    fmap::FMap, fset::FSet, id::Id, int::Int, mapping::Mapping, ord::OrdLogic, seq::Seq, set::Set,
24    well_founded::WellFounded,
25};
26
27/// Creates a logical value satisfying the property given by `p`.
28///
29/// This is also called the "epsilon operator": its goal is not extract from `∃x. P(x)`
30/// a `x` satisfying `P`.
31#[trusted]
32#[logic(opaque)]
33#[requires(exists<x: T> p[x])]
34#[ensures(p[result])]
35pub fn such_that<T>(p: crate::logic::Mapping<T, bool>) -> T {
36    dead
37}
38
39/// Indicates unreachable code in logic.
40///
41/// This function indicates a logical branch that should be impossible to reach.
42#[trusted]
43#[logic(opaque)]
44#[requires(false)]
45#[ensures(false)]
46#[variant(0)]
47#[allow(unconditional_recursion)]
48pub fn unreachable<T>() -> T {
49    unreachable()
50}
creusot_contracts/logic.rs

creusot_contracts/
logic.rs
