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

creusot_std/
logic.rs
