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
8pub mod 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, Positive},
26    mapping::Mapping,
27    ord::{OrdLogic, PartialOrdLogic},
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: Mapping<T, bool>) -> T {
42    dead
43}
44
45/// A variant of `such_that` that returns an `Option<T>`, returning `None` if no value satisfies
46/// the property.
47#[logic]
48#[ensures(match result {
49    Some(v) => p[v],
50    None => forall<x: T> !p[x],
51})]
52pub fn try_such_that<T>(p: Mapping<T, bool>) -> Option<T> {
53    pearlite! {
54        if exists<x: T> p[x] {
55            Some(such_that(p))
56        } else {
57            None
58        }
59    }
60}
61
62/// Return a logical value of type `T` without any constraints.
63#[logic]
64pub fn any<T>() -> T {
65    such_that(|_| true)
66}
creusot_std/logic.rs

creusot_std/
logic.rs
