creusot_std/
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;
9mod 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
21pub use self::{
22    fmap::FMap,
23    fset::FSet,
24    id::Id,
25    int::{Int, Nat},
26    mapping::Mapping,
27    ord::OrdLogic,
28    seq::Seq,
29    set::Set,
30    well_founded::WellFounded,
31};
32
33/// Creates a logical value satisfying the property given by `p`.
34///
35/// This is also called the "epsilon operator": its goal is not extract from `∃x. P(x)`
36/// a `x` satisfying `P`.
37#[trusted]
38#[logic(opaque)]
39#[requires(exists<x: T> p[x])]
40#[ensures(p[result])]
41pub fn such_that<T>(p: crate::logic::Mapping<T, bool>) -> T {
42    dead
43}
44
45/// Indicates unreachable code in logic.
46///
47/// This function indicates a logical branch that should be impossible to reach.
48#[trusted]
49#[logic(opaque)]
50#[requires(false)]
51#[ensures(false)]
52#[variant(0)]
53#[allow(unconditional_recursion)]
54pub fn unreachable<T>() -> T {
55    unreachable()
56}
creusot_std/logic.rs

creusot_std/
logic.rs
