From d41f576a577faed5688d3752421242b915955e5c Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Wed, 28 Feb 2024 11:22:18 +0100 Subject: [PATCH] rename ghost, logic and predicate functions `#[ghost]` -> `#[logic]` `#[logic]` -> `#[logic(prophetic)]` `#[predicate]` -> `#[predicate]` and `#[predicate(prophetic)]` --- ARCHITECTURE.md | 2 +- README.md | 7 +- creusot-contracts-dummy/src/lib.rs | 5 -- .../src/derive/deep_model.rs | 2 +- creusot-contracts-proc/src/derive/resolve.rs | 2 +- creusot-contracts-proc/src/lib.rs | 84 ++++++++----------- creusot-contracts/src/ghost_ptr.rs | 16 ++-- creusot-contracts/src/invariant.rs | 2 +- creusot-contracts/src/lib.rs | 82 +++++++++++++----- creusot-contracts/src/logic/fmap.rs | 36 ++++---- creusot-contracts/src/logic/fset.rs | 16 ++-- creusot-contracts/src/logic/int.rs | 12 +-- creusot-contracts/src/logic/mapping.rs | 6 +- creusot-contracts/src/logic/ops.rs | 16 ++-- creusot-contracts/src/logic/ord.rs | 34 ++++---- creusot-contracts/src/logic/seq.rs | 22 ++--- creusot-contracts/src/logic/set.rs | 12 +-- creusot-contracts/src/model.rs | 22 ++--- creusot-contracts/src/num_rational.rs | 16 ++-- creusot-contracts/src/resolve.rs | 8 +- creusot-contracts/src/snapshot.rs | 8 +- creusot-contracts/src/std/array.rs | 4 +- creusot-contracts/src/std/boxed.rs | 4 +- creusot-contracts/src/std/cmp.rs | 4 +- creusot-contracts/src/std/default.rs | 2 +- creusot-contracts/src/std/deque.rs | 12 +-- creusot-contracts/src/std/iter.rs | 6 +- creusot-contracts/src/std/iter/cloned.rs | 10 +-- creusot-contracts/src/std/iter/copied.rs | 10 +-- creusot-contracts/src/std/iter/empty.rs | 2 +- creusot-contracts/src/std/iter/enumerate.rs | 16 ++-- creusot-contracts/src/std/iter/fuse.rs | 6 +- creusot-contracts/src/std/iter/map_inv.rs | 20 ++--- creusot-contracts/src/std/iter/once.rs | 4 +- creusot-contracts/src/std/iter/range.rs | 6 +- creusot-contracts/src/std/iter/repeat.rs | 2 +- creusot-contracts/src/std/iter/skip.rs | 14 ++-- creusot-contracts/src/std/iter/take.rs | 18 ++-- creusot-contracts/src/std/iter/zip.rs | 12 +-- creusot-contracts/src/std/num.rs | 4 +- creusot-contracts/src/std/ops.rs | 12 +-- creusot-contracts/src/std/option.rs | 16 ++-- creusot-contracts/src/std/result.rs | 2 +- creusot-contracts/src/std/slice.rs | 28 +++---- creusot-contracts/src/std/time.rs | 16 ++-- creusot-contracts/src/std/tuples.rs | 6 +- creusot-contracts/src/std/vec.rs | 12 +-- creusot-contracts/src/util.rs | 8 +- creusot/src/backend.rs | 9 +- creusot/src/backend/logic.rs | 4 +- creusot/src/backend/ty.rs | 2 +- creusot/src/ctx.rs | 2 +- creusot/src/translation.rs | 1 - creusot/src/translation/pearlite.rs | 2 +- creusot/src/translation/specification.rs | 44 ++++++---- creusot/src/util.rs | 53 ++++++------ creusot/src/validate.rs | 11 +-- 57 files changed, 416 insertions(+), 378 deletions(-) diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md index eafaf886d0..b23aa48468 100644 --- a/ARCHITECTURE.md +++ b/ARCHITECTURE.md @@ -151,7 +151,7 @@ Instead, we replace the `discriminant` / `switchInt` pair with a match directly ## Logical functions -Logical functions are created by `#[ghost]`, `#[logic]`, or `#[predicate]`. +Logical functions are created by `#[logic]` or `#[predicate]`. ## Specifications diff --git a/README.md b/README.md index 097641ed0a..657c4eaab8 100644 --- a/README.md +++ b/README.md @@ -152,15 +152,14 @@ Contracts and logic functions are written in Pearlite, a specification language - Logical Expressions: quantifiers (`forall` and `exists`), logical implication `==>`, *logical* equality `a == b`, labels - Rust specific logical expressions: access to the **final** value of a mutable reference `^`, access to the *model* of an object `@` -We also provide three new attributes on Rust functions: `ghost`, `logic` and `predicate`. - -A ghost function is marked with `#[ghost]`. It can be used in ghost code, to assign ghost -variables of the `Snapshot` type. +We also provide two new attributes on Rust functions: `logic` and `predicate`. Marked `#[logic]` or `#[predicate]`, a function can be used in specs and other logical conditions (`requires`/`ensures` and `invariant`). They can use ghost functions. The two attributes have the following difference. - A `logic` function can freely have logical, non-executable operations, such as quantifiers, logic equalities, etc. Instead, this function can't be called in normal Rust code (the function body of a `logic` function is replaced with a panic). You can use pearlite syntax for any part in the logic function by marking that part with the `pearlite! { ... }` macro. + + If you need to use the prophecy operator `^` on a mutable reference, you need to mark the function `#[logic(prophetic)]`. - A `predicate` is a logical function which returns a proposition (in practice, returns a boolean value). When you write *recursive* `ghost`, `logic` or `predicate` functions, you have to show that the function terminates. diff --git a/creusot-contracts-dummy/src/lib.rs b/creusot-contracts-dummy/src/lib.rs index c7a952d901..9e1f60b1dd 100644 --- a/creusot-contracts-dummy/src/lib.rs +++ b/creusot-contracts-dummy/src/lib.rs @@ -43,11 +43,6 @@ pub fn pearlite(_: TS1) -> TS1 { TS1::new() } -#[proc_macro_attribute] -pub fn ghost(_: TS1, _: TS1) -> TS1 { - TS1::new() -} - #[proc_macro_attribute] pub fn predicate(_: TS1, _: TS1) -> TS1 { TS1::new() diff --git a/creusot-contracts-proc/src/derive/deep_model.rs b/creusot-contracts-proc/src/derive/deep_model.rs index 6dd6807924..7171b82fd9 100644 --- a/creusot-contracts-proc/src/derive/deep_model.rs +++ b/creusot-contracts-proc/src/derive/deep_model.rs @@ -47,7 +47,7 @@ pub fn derive_deep_model(input: proc_macro::TokenStream) -> proc_macro::TokenStr impl #impl_generics ::creusot_contracts::DeepModel for #name #ty_generics #where_clause { type DeepModelTy = #deep_model_ty_name #ty_generics; - #[ghost] + #[logic] #open fn deep_model(self) -> Self::DeepModelTy { #eq diff --git a/creusot-contracts-proc/src/derive/resolve.rs b/creusot-contracts-proc/src/derive/resolve.rs index 1b081e2daf..3888b8ebc6 100644 --- a/creusot-contracts-proc/src/derive/resolve.rs +++ b/creusot-contracts-proc/src/derive/resolve.rs @@ -14,7 +14,7 @@ pub fn derive_resolve(input: proc_macro::TokenStream) -> proc_macro::TokenStream let expanded = quote! { #[::creusot_contracts::trusted] impl #impl_generics ::creusot_contracts::Resolve for #name #ty_generics #where_clause { - #[::creusot_contracts::predicate] + #[::creusot_contracts::predicate(prophetic)] #[::creusot_contracts::open] fn resolve(self) -> bool { use ::creusot_contracts::Resolve; diff --git a/creusot-contracts-proc/src/lib.rs b/creusot-contracts-proc/src/lib.rs index bf4a3cf717..6209c692da 100644 --- a/creusot-contracts-proc/src/lib.rs +++ b/creusot-contracts-proc/src/lib.rs @@ -467,59 +467,35 @@ impl Parse for LogicInput { } #[proc_macro_attribute] -pub fn ghost(_: TS1, tokens: TS1) -> TS1 { - let log = parse_macro_input!(tokens as LogicInput); - match log { - LogicInput::Item(log) => ghost_item(log), - LogicInput::Sig(sig) => ghost_sig(sig), - } -} - -fn ghost_sig(sig: TraitItemSignature) -> TS1 { - let span = sig.span(); - TS1::from(quote_spanned! {span=> - #[creusot::decl::ghost] - #sig - }) -} - -fn ghost_item(log: LogicItem) -> TS1 { - let span = log.sig.span(); - - let term = log.body; - let vis = log.vis; - let def = log.defaultness; - let sig = log.sig; - let attrs = log.attrs; - let req_body = pretyping::encode_block(&term.stmts).unwrap(); - - TS1::from(quote_spanned! {span=> - #[creusot::decl::ghost] - #(#attrs)* - #vis #def #sig { - #req_body +pub fn logic(prophetic: TS1, tokens: TS1) -> TS1 { + let prophetic = if prophetic.is_empty() { + None + } else { + let t = parse_macro_input!(prophetic as Ident); + if t.to_string() == "prophetic" { + Some(quote!(#[creusot::decl::logic::prophetic])) + } else { + None } - }) -} - -#[proc_macro_attribute] -pub fn logic(_: TS1, tokens: TS1) -> TS1 { + }; let log = parse_macro_input!(tokens as LogicInput); match log { - LogicInput::Item(log) => logic_item(log), - LogicInput::Sig(sig) => logic_sig(sig), + LogicInput::Item(log) => logic_item(log, prophetic), + LogicInput::Sig(sig) => logic_sig(sig, prophetic), } } -fn logic_sig(sig: TraitItemSignature) -> TS1 { +fn logic_sig(sig: TraitItemSignature, prophetic: Option) -> TS1 { let span = sig.span(); - TS1::from(quote_spanned! {span=> + + TS1::from(quote_spanned! {span => #[creusot::decl::logic] + #prophetic #sig }) } -fn logic_item(log: LogicItem) -> TS1 { +fn logic_item(log: LogicItem, prophetic: Option) -> TS1 { let span = log.sig.span(); let term = log.body; @@ -529,8 +505,9 @@ fn logic_item(log: LogicItem) -> TS1 { let attrs = log.attrs; let req_body = pretyping::encode_block(&term.stmts).unwrap(); - TS1::from(quote_spanned! {span=> + TS1::from(quote_spanned! {span => #[creusot::decl::logic] + #prophetic #(#attrs)* #vis #def #sig { #req_body @@ -550,7 +527,18 @@ pub fn law(_: TS1, tokens: TS1) -> TS1 { } #[proc_macro_attribute] -pub fn predicate(_: TS1, tokens: TS1) -> TS1 { +pub fn predicate(prophetic: TS1, tokens: TS1) -> TS1 { + let prophetic = if prophetic.is_empty() { + None + } else { + let t = parse_macro_input!(prophetic as Ident); + if t.to_string() == "prophetic" { + Some(quote!(#[creusot::decl::logic::prophetic])) + } else { + None + } + }; + let pred = parse_macro_input!(tokens as LogicInput); let sig = match &pred { @@ -573,20 +561,21 @@ pub fn predicate(_: TS1, tokens: TS1) -> TS1 { }; match pred { - LogicInput::Item(log) => predicate_item(log), - LogicInput::Sig(sig) => predicate_sig(sig), + LogicInput::Item(log) => predicate_item(log, prophetic), + LogicInput::Sig(sig) => predicate_sig(sig, prophetic), } } -fn predicate_sig(sig: TraitItemSignature) -> TS1 { +fn predicate_sig(sig: TraitItemSignature, prophetic: Option) -> TS1 { let span = sig.span(); TS1::from(quote_spanned! {span=> #[creusot::decl::predicate] + #prophetic #sig }) } -fn predicate_item(log: LogicItem) -> TS1 { +fn predicate_item(log: LogicItem, prophetic: Option) -> TS1 { let span = log.sig.span(); let term = log.body; let vis = log.vis; @@ -598,6 +587,7 @@ fn predicate_item(log: LogicItem) -> TS1 { TS1::from(quote_spanned! {span=> #[creusot::decl::predicate] + #prophetic #(#attrs)* #vis #def #sig { #req_body diff --git a/creusot-contracts/src/ghost_ptr.rs b/creusot-contracts/src/ghost_ptr.rs index 44f2158ed0..64041cec16 100644 --- a/creusot-contracts/src/ghost_ptr.rs +++ b/creusot-contracts/src/ghost_ptr.rs @@ -29,7 +29,7 @@ impl ShallowModel for GhostPtrToken { type ShallowModelTy = FMap, T>; #[trusted] - #[ghost] + #[logic] #[open(self)] fn shallow_model(self) -> Self::ShallowModelTy { absurd @@ -131,7 +131,7 @@ impl GhostPtrToken { impl GhostPtrExt for GhostPtr { #[trusted] #[open(self)] - #[ghost] + #[logic] #[ensures(forall> !t@.contains(result))] #[ensures(result.addr_logic() == 0)] #[ensures(forall> ptr.addr_logic() == result.addr_logic() ==> ptr == result)] @@ -140,7 +140,7 @@ impl GhostPtrExt for GhostPtr { } #[trusted] - #[ghost] + #[logic] #[open(self)] fn addr_logic(self) -> Int { absurd @@ -151,7 +151,7 @@ impl<'a, T: ?Sized> ShallowModel for GhostPtrTokenRef<'a, T> { type ShallowModelTy = FMap, T>; #[trusted] - #[ghost] + #[logic] #[open(self)] fn shallow_model(self) -> Self::ShallowModelTy { absurd @@ -174,14 +174,14 @@ impl<'a, T: ?Sized> GhostPtrTokenRef<'a, T> { #[requires(new_model.subset(self@))] #[ensures(result@ == *new_model)] #[allow(unused_variables)] - pub fn shrink_token_ref(self, new_model: Ghost>) -> Self { + pub fn shrink_token_ref(self, new_model: Snapshot>) -> Self { self } } impl<'a, T: ?Sized> GhostPtrTokenMut<'a, T> { #[trusted] - #[ghost] + #[logic] #[open(self)] pub fn cur(self) -> FMap, T> { absurd @@ -265,9 +265,9 @@ impl<'a, T> Resolve for GhostPtrTokenMut<'a, T> { } pub trait GhostPtrExt: Sized { - #[ghost] + #[logic] fn null_logic() -> Self; - #[ghost] + #[logic] fn addr_logic(self) -> Int; } diff --git a/creusot-contracts/src/invariant.rs b/creusot-contracts/src/invariant.rs index ff9fdae4c4..51aa0d047a 100644 --- a/creusot-contracts/src/invariant.rs +++ b/creusot-contracts/src/invariant.rs @@ -1,7 +1,7 @@ use crate::*; pub trait Invariant { - #[predicate] + #[predicate(prophetic)] #[open] #[rustc_diagnostic_item = "creusot_invariant_user"] fn invariant(self) -> bool { diff --git a/creusot-contracts/src/lib.rs b/creusot-contracts/src/lib.rs index 5ef8b382e1..fd324b72dc 100644 --- a/creusot-contracts/src/lib.rs +++ b/creusot-contracts/src/lib.rs @@ -32,20 +32,41 @@ mod macros { pub use creusot_contracts_proc::law; /// Declare a function as being a logical function, this declaration must be pure and - /// total. It cannot be called from Rust programs as it is *ghost*, in exchange it can - /// use logical operations and syntax with the help of the [pearlite] macro. + /// total. It cannot be called from Rust programs, but in exchange it can use logical + /// operations and syntax with the help of the [`pearlite!`] macro. + /// + /// # `prophetic` + /// + /// If you wish to use the `^` operator on mutable borrows to get the final value, you need to + /// specify that the function is _prophetic_, like so: + /// ```ignore + /// #[logic(prophetic)] + /// fn uses_prophecies(x: &mut Int) -> Int { + /// pearlite! { if ^x == 0 { 0 } else { 1 } } + /// } + /// ``` + /// Such a logic function cannot be used in [`snapshot!`] anymore, and cannot be + /// called from a regular [`logic`] or [`predicate`] function. pub use creusot_contracts_proc::logic; - /// Declare a function as being a ghost function, this declaration must be pure and - /// total. It cannot be called from Rust programs as it is *ghost*, in exchange it can - /// use logical operations and syntax with the help of the [pearlite] macro. - /// Unlike functions marked with the `[logic]` attribute, `[ghost]` functions cannot - /// use the final value operator (^), nor call other `[predicate]` or `[logic]` functions. - pub use creusot_contracts_proc::ghost; - /// Declare a function as being a logical function, this declaration must be pure and /// total. It cannot be called from Rust programs as it is *ghost*, in exchange it can - /// use logical operations and syntax with the help of the [pearlite] macro. + /// use logical operations and syntax with the help of the [`pearlite!`] macro. + /// + /// It **must** return a boolean. + /// + /// # `prophetic` + /// + /// If you wish to use the `^` operator on mutable borrows to get the final value, you need to + /// specify that the function is _prophetic_, like so: + /// ```ignore + /// #[predicate(prophetic)] + /// fn uses_prophecies(x: &mut Int) -> bool { + /// pearlite! { ^x == 0 } + /// } + /// ``` + /// Such a predicate function cannot be used in [`snapshot!`] anymore, and cannot be + /// called from a regular [`logic`] or [`predicate`] function. pub use creusot_contracts_proc::predicate; /// Inserts a *logical* assertion into the code. This assertion will not be checked at runtime @@ -109,20 +130,41 @@ mod macros { pub use creusot_contracts_dummy::law; /// Declare a function as being a logical function, this declaration must be pure and - /// total. It cannot be called from Rust programs as it is *ghost*, in exchange it can - /// use logical operations and syntax with the help of the [pearlite] macro. + /// total. It cannot be called from Rust programs, but in exchange it can use logical + /// operations and syntax with the help of the [`pearlite!`] macro. + /// + /// # `prophetic` + /// + /// If you wish to use the `^` operator on mutable borrows to get the final value, you need to + /// specify that the function is _prophetic_, like so: + /// ```ignore + /// #[logic(prophetic)] + /// fn uses_prophecies(x: &mut Int) -> Int { + /// pearlite! { if ^x == 0 { 0 } else { 1 } } + /// } + /// ``` + /// Such a logic function cannot be used in [`snapshot!`] anymore, and cannot be + /// called from a regular [`logic`] or [`predicate`] function. pub use creusot_contracts_dummy::logic; - /// Declare a function as being a ghost function, this declaration must be pure and - /// total. It cannot be called from Rust programs as it is *ghost*, in exchange it can - /// use logical operations and syntax with the help of the [pearlite] macro. - /// Unlike functions marked with the `[logic]` attribute, `[ghost]` functions cannot - /// use the final value operator (^), nor call other `[predicate]` or `[logic]` functions. - pub use creusot_contracts_dummy::ghost; - /// Declare a function as being a logical function, this declaration must be pure and /// total. It cannot be called from Rust programs as it is *ghost*, in exchange it can - /// use logical operations and syntax with the help of the [pearlite] macro. + /// use logical operations and syntax with the help of the [`pearlite!`] macro. + /// + /// It **must** return a boolean. + /// + /// # `prophetic` + /// + /// If you wish to use the `^` operator on mutable borrows to get the final value, you need to + /// specify that the function is _prophetic_, like so: + /// ```ignore + /// #[predicate(prophetic)] + /// fn uses_prophecies(x: &mut Int) -> bool { + /// pearlite! { ^x == 0 } + /// } + /// ``` + /// Such a predicate function cannot be used in [`snapshot!`] anymore, and cannot be + /// called from a regular [`logic`] or [`predicate`] function. pub use creusot_contracts_dummy::predicate; /// Inserts a *logical* assertion into the code. This assertion will not be checked at runtime diff --git a/creusot-contracts/src/logic/fmap.rs b/creusot-contracts/src/logic/fmap.rs index 796190aac6..04357dd532 100644 --- a/creusot-contracts/src/logic/fmap.rs +++ b/creusot-contracts/src/logic/fmap.rs @@ -7,7 +7,7 @@ pub struct FMap(PMap); impl FMap { #[trusted] - #[ghost] + #[logic] #[open(self)] #[ensures(result >= 0)] pub fn len(self) -> Int { @@ -15,7 +15,7 @@ impl FMap { } #[trusted] - #[ghost] + #[logic] #[open(self)] pub fn mk(_m: PMap) -> Self { absurd @@ -23,7 +23,7 @@ impl FMap { #[trusted] #[open(self)] - #[ghost] + #[logic] #[ensures(Self::mk(result) == self)] // injectivity pub fn view(self) -> PMap { absurd @@ -31,7 +31,7 @@ impl FMap { #[trusted] #[open(self)] - #[ghost] + #[logic] #[ensures(result.view() == self.view().set(k, Some(v.make_sized())))] #[ensures(self.contains(k) ==> result.len() == self.len())] #[ensures(!self.contains(k) ==> result.len() == self.len() + 1)] @@ -41,28 +41,28 @@ impl FMap { #[trusted] #[open(self)] - #[ghost] + #[logic] #[ensures(result.view() == self.view().set(k, None))] #[ensures(result.len() == if self.contains(k) {self.len() - 1} else {self.len()})] pub fn remove(self, k: K) -> Self { absurd } - #[ghost] + #[logic] #[open] #[why3::attr = "inline:trivial"] pub fn get(self, k: K) -> Option> { self.view().get(k) } - #[ghost] + #[logic] #[open] #[why3::attr = "inline:trivial"] pub fn lookup_unsized(self, k: K) -> SizedW { unwrap(self.get(k)) } - #[ghost] + #[logic] #[open] #[why3::attr = "inline:trivial"] pub fn lookup(self, k: K) -> V @@ -72,7 +72,7 @@ impl FMap { *self.lookup_unsized(k) } - #[ghost] + #[logic] #[open] #[why3::attr = "inline:trivial"] pub fn contains(self, k: K) -> bool { @@ -80,7 +80,7 @@ impl FMap { } #[trusted] - #[ghost] + #[logic] #[open(self)] #[ensures(result.len() == 0)] #[ensures(result.view() == Mapping::cst(None))] @@ -88,26 +88,26 @@ impl FMap { absurd } - #[ghost] + #[logic] #[open] pub fn is_empty(self) -> bool { self.ext_eq(FMap::empty()) } - #[ghost] + #[logic] #[open] pub fn disjoint(self, other: Self) -> bool { pearlite! {forall !self.contains(k) || !other.contains(k)} } - #[ghost] + #[logic] #[open] pub fn subset(self, other: Self) -> bool { pearlite! {forall self.contains(k) ==> other.get(k) == self.get(k)} } #[trusted] - #[ghost] + #[logic] #[open(self)] #[requires(self.disjoint(other))] #[ensures(forall result.get(k) == if self.contains(k) { @@ -123,15 +123,15 @@ impl FMap { } #[trusted] - #[ghost] + #[logic] #[open(self)] #[ensures(forall result.get(k) == if other.contains(k) {None} else {self.get(k)})] pub fn subtract_keys(self, other: Self) -> Self { absurd } - #[ghost] - #[open(self)] + #[logic] + #[open] #[requires(other.subset(self))] #[ensures(result.disjoint(other))] #[ensures(other.union(result).ext_eq(self))] @@ -140,7 +140,7 @@ impl FMap { self.subtract_keys(other) } - #[ghost] + #[logic] #[open] #[ensures(result ==> self == other)] #[ensures((forall self.get(k) == other.get(k)) ==> result)] diff --git a/creusot-contracts/src/logic/fset.rs b/creusot-contracts/src/logic/fset.rs index c500edcde6..7b3dfb65b4 100644 --- a/creusot-contracts/src/logic/fset.rs +++ b/creusot-contracts/src/logic/fset.rs @@ -17,7 +17,7 @@ impl FSet { } #[doc(hidden)] - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "set.Fset.mem"] pub fn mem(_: T, _: Self) -> bool { @@ -25,14 +25,14 @@ impl FSet { } #[open] - #[ghost] + #[logic] #[why3::attr = "inline:trivial"] pub fn insert(self, e: T) -> Self { Self::add(e, self) } #[doc(hidden)] - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "set.Fset.add"] pub fn add(_: T, _: Self) -> Self { @@ -47,21 +47,21 @@ impl FSet { } #[open] - #[ghost] + #[logic] #[why3::attr = "inline:trivial"] pub fn remove(self, a: T) -> Self { Self::rem(a, self) } #[doc(hidden)] - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "set.Fset.remove"] pub fn rem(_: T, _: Self) -> Self { pearlite! { absurd } } - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "set.Fset.union"] pub fn union(self, _: Self) -> Self { @@ -82,14 +82,14 @@ impl FSet { Self::is_subset(other, self) } - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "set.Fset.cardinal"] pub fn len(self) -> Int { pearlite! { absurd } } - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "set.Fset.pick"] pub fn peek(self) -> T diff --git a/creusot-contracts/src/logic/int.rs b/creusot-contracts/src/logic/int.rs index 7fb8a8de44..1a7725f5f7 100644 --- a/creusot-contracts/src/logic/int.rs +++ b/creusot-contracts/src/logic/int.rs @@ -8,7 +8,7 @@ pub struct Int(*mut ()); impl Int { #[trusted] - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "int.Power.power"] pub fn pow(self, _: Int) -> Int { @@ -16,7 +16,7 @@ impl Int { } #[trusted] - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "int.MinMax.max"] pub fn max(self, _: Int) -> Int { @@ -24,7 +24,7 @@ impl Int { } #[trusted] - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "int.MinMax.min"] pub fn min(self, _: Int) -> Int { @@ -32,7 +32,7 @@ impl Int { } #[trusted] - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "int.EuclideanDivision.div"] pub fn div_euclid(self, _: Int) -> Int { @@ -40,14 +40,14 @@ impl Int { } #[trusted] - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "int.EuclideanDivision.mod"] pub fn rem_euclid(self, _: Int) -> Int { absurd } - #[ghost] + #[logic] #[open] pub fn abs_diff(self, other: Int) -> Int { if self < other { diff --git a/creusot-contracts/src/logic/mapping.rs b/creusot-contracts/src/logic/mapping.rs index 7fb7be6089..b53c838370 100644 --- a/creusot-contracts/src/logic/mapping.rs +++ b/creusot-contracts/src/logic/mapping.rs @@ -5,7 +5,7 @@ pub struct Mapping(std::marker::PhantomData<(A, B)>); impl Mapping { #[trusted] - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "map.Map.get"] pub fn get(self, _: A) -> B { @@ -13,7 +13,7 @@ impl Mapping { } #[trusted] - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "map.Map.set"] pub fn set(self, _: A, _: B) -> Self { @@ -21,7 +21,7 @@ impl Mapping { } #[trusted] - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "map.Const.const"] pub fn cst(_: B) -> Self { diff --git a/creusot-contracts/src/logic/ops.rs b/creusot-contracts/src/logic/ops.rs index 80339c0be6..3deff865dd 100644 --- a/creusot-contracts/src/logic/ops.rs +++ b/creusot-contracts/src/logic/ops.rs @@ -5,7 +5,7 @@ use crate::*; pub trait IndexLogic { type Item; - #[ghost] + #[logic] #[rustc_diagnostic_item = "index_logic_method"] fn index_logic(self, idx: I) -> Self::Item; } @@ -13,7 +13,7 @@ pub trait IndexLogic { impl IndexLogic for Vec { type Item = T; - #[ghost] + #[logic] #[open] #[why3::attr = "inline:trivial"] fn index_logic(self, ix: Int) -> Self::Item { @@ -24,7 +24,7 @@ impl IndexLogic for Vec { impl IndexLogic for Vec { type Item = T; - #[ghost] + #[logic] #[open] #[why3::attr = "inline:trivial"] fn index_logic(self, ix: usize) -> Self::Item { @@ -35,7 +35,7 @@ impl IndexLogic for Vec { impl IndexLogic for [T] { type Item = T; - #[ghost] + #[logic] #[open] #[why3::attr = "inline:trivial"] #[rustc_diagnostic_item = "slice_index_logic"] @@ -47,7 +47,7 @@ impl IndexLogic for [T] { impl IndexLogic for [T] { type Item = T; - #[ghost] + #[logic] #[open] #[why3::attr = "inline:trivial"] fn index_logic(self, ix: usize) -> Self::Item { @@ -58,7 +58,7 @@ impl IndexLogic for [T] { impl IndexLogic for [T; N] { type Item = T; - #[ghost] + #[logic] #[open] #[why3::attr = "inline:trivial"] fn index_logic(self, ix: Int) -> Self::Item { @@ -69,7 +69,7 @@ impl IndexLogic for [T; N] { impl IndexLogic for [T; N] { type Item = T; - #[ghost] + #[logic] #[open] #[why3::attr = "inline:trivial"] fn index_logic(self, ix: usize) -> Self::Item { @@ -80,7 +80,7 @@ impl IndexLogic for [T; N] { impl IndexLogic for Snapshot> { type Item = T; - #[ghost] + #[logic] #[open] #[why3::attr = "inline:trivial"] fn index_logic(self, ix: Int) -> Self::Item { diff --git a/creusot-contracts/src/logic/ord.rs b/creusot-contracts/src/logic/ord.rs index e5f9177019..76bda7b493 100644 --- a/creusot-contracts/src/logic/ord.rs +++ b/creusot-contracts/src/logic/ord.rs @@ -2,10 +2,10 @@ use crate::{std::cmp::Ordering, *}; #[allow(unused)] pub trait OrdLogic { - #[ghost] + #[logic] fn cmp_log(self, _: Self) -> Ordering; - #[ghost] + #[logic] #[open] fn le_log(self, o: Self) -> bool { pearlite! { self.cmp_log(o) != Ordering::Greater } @@ -15,7 +15,7 @@ pub trait OrdLogic { #[ensures(x.le_log(y) == (x.cmp_log(y) != Ordering::Greater))] fn cmp_le_log(x: Self, y: Self); - #[ghost] + #[logic] #[open] fn lt_log(self, o: Self) -> bool { pearlite! { self.cmp_log(o) == Ordering::Less } @@ -25,7 +25,7 @@ pub trait OrdLogic { #[ensures(x.lt_log(y) == (x.cmp_log(y) == Ordering::Less))] fn cmp_lt_log(x: Self, y: Self); - #[ghost] + #[logic] #[open] fn ge_log(self, o: Self) -> bool { pearlite! { self.cmp_log(o) != Ordering::Less } @@ -35,7 +35,7 @@ pub trait OrdLogic { #[ensures(x.ge_log(y) == (x.cmp_log(y) != Ordering::Less))] fn cmp_ge_log(x: Self, y: Self); - #[ghost] + #[logic] #[open] fn gt_log(self, o: Self) -> bool { pearlite! { self.cmp_log(o) == Ordering::Greater } @@ -134,7 +134,7 @@ pub use ord_laws_impl; macro_rules! ord_logic_impl { ($t:ty) => { impl OrdLogic for $t { - #[ghost] + #[logic] #[open] fn cmp_log(self, o: Self) -> Ordering { if self < o { @@ -148,7 +148,7 @@ macro_rules! ord_logic_impl { #[trusted] #[open] - #[ghost] + #[logic] #[creusot::builtins = "int.Int.(<=)"] fn le_log(self, _: Self) -> bool { true @@ -156,7 +156,7 @@ macro_rules! ord_logic_impl { #[trusted] #[open] - #[ghost] + #[logic] #[creusot::builtins = "int.Int.(<)"] fn lt_log(self, _: Self) -> bool { true @@ -164,7 +164,7 @@ macro_rules! ord_logic_impl { #[trusted] #[open] - #[ghost] + #[logic] #[creusot::builtins = "int.Int.(>=)"] fn ge_log(self, _: Self) -> bool { true @@ -172,7 +172,7 @@ macro_rules! ord_logic_impl { #[trusted] #[open] - #[ghost] + #[logic] #[creusot::builtins = "int.Int.(>)"] fn gt_log(self, _: Self) -> bool { true @@ -201,7 +201,7 @@ ord_logic_impl!(isize); impl OrdLogic for bool { #[open] - #[ghost] + #[logic] fn cmp_log(self, o: Self) -> Ordering { match (self, o) { (false, false) => Ordering::Equal, @@ -215,7 +215,7 @@ impl OrdLogic for bool { } impl OrdLogic for (A, B) { - #[ghost] + #[logic] #[open] fn cmp_log(self, o: Self) -> Ordering { pearlite! { { @@ -228,25 +228,25 @@ impl OrdLogic for (A, B) { } } } - #[ghost] + #[logic] #[open] fn le_log(self, o: Self) -> bool { pearlite! { (self.0 == o.0 && self.1 <= o.1) || self.0 <= o.0 } } - #[ghost] + #[logic] #[open] fn lt_log(self, o: Self) -> bool { pearlite! { (self.0 == o.0 && self.1 < o.1) || self.0 < o.0 } } - #[ghost] + #[logic] #[open] fn ge_log(self, o: Self) -> bool { pearlite! { (self.0 == o.0 && self.1 >= o.1) || self.0 >= o.0 } } - #[ghost] + #[logic] #[open] fn gt_log(self, o: Self) -> bool { pearlite! { (self.0 == o.0 && self.1 > o.1) || self.0 > o.0 } @@ -256,7 +256,7 @@ impl OrdLogic for (A, B) { } impl OrdLogic for Option { - #[ghost] + #[logic] #[open] fn cmp_log(self, o: Self) -> Ordering { match (self, o) { diff --git a/creusot-contracts/src/logic/seq.rs b/creusot-contracts/src/logic/seq.rs index 31f3860705..cbeba88a70 100644 --- a/creusot-contracts/src/logic/seq.rs +++ b/creusot-contracts/src/logic/seq.rs @@ -13,14 +13,14 @@ impl Seq { pub const EMPTY: Self = { Seq(std::marker::PhantomData) }; #[trusted] - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "seq.Seq.create"] pub fn new(_: Int, _: Mapping) -> Self { absurd } - #[ghost] + #[logic] #[open] pub fn get(self, ix: Int) -> Option { if 0 <= ix && ix < self.len() { @@ -31,7 +31,7 @@ impl Seq { } #[trusted] - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "seq_ext.SeqExt.subsequence"] pub fn subsequence(self, _: Int, _: Int) -> Self { @@ -39,21 +39,21 @@ impl Seq { } #[trusted] - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "seq.Seq.singleton"] pub fn singleton(_: T) -> Self { absurd } - #[ghost] + #[logic] #[open] pub fn tail(self) -> Self { self.subsequence(1, self.len()) } #[trusted] - #[ghost] + #[logic] #[open(self)] #[rustc_diagnostic_item = "seq_len"] #[creusot::builtins = "seq.Seq.length"] @@ -62,7 +62,7 @@ impl Seq { } #[trusted] - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "seq.Seq.set"] pub fn set(self, _: Int, _: T) -> Self { @@ -78,7 +78,7 @@ impl Seq { } #[trusted] - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "seq.Seq.snoc"] pub fn push(self, _: T) -> Self { @@ -86,7 +86,7 @@ impl Seq { } #[trusted] - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "seq.Seq.(++)"] pub fn concat(self, _: Self) -> Self { @@ -94,7 +94,7 @@ impl Seq { } #[trusted] - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "seq.Reverse.reverse"] pub fn reverse(self) -> Self { @@ -163,7 +163,7 @@ impl Seq<&T> { impl IndexLogic for Seq { type Item = T; - #[ghost] + #[logic] #[trusted] #[open(self)] #[rustc_diagnostic_item = "seq_index"] diff --git a/creusot-contracts/src/logic/set.rs b/creusot-contracts/src/logic/set.rs index ec36252a28..f4bc35d3ea 100644 --- a/creusot-contracts/src/logic/set.rs +++ b/creusot-contracts/src/logic/set.rs @@ -17,7 +17,7 @@ impl Set { } #[doc(hidden)] - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "set.Set.mem"] pub fn mem(_: T, _: Self) -> bool { @@ -25,14 +25,14 @@ impl Set { } #[open] - #[ghost] + #[logic] #[why3::attr = "inline:trivial"] pub fn insert(self, e: T) -> Self { Self::add(e, self) } #[doc(hidden)] - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "set.Set.add"] pub fn add(_: T, _: Self) -> Self { @@ -47,14 +47,14 @@ impl Set { } #[open] - #[ghost] + #[logic] #[why3::attr = "inline:trivial"] pub fn remove(self, a: T) -> Self { Self::rem(a, self) } #[doc(hidden)] - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "set.Set.remove"] pub fn rem(_: T, _: Self) -> Self { @@ -62,7 +62,7 @@ impl Set { } #[open(self)] - #[ghost] + #[logic] #[creusot::builtins = "set.Set.union"] pub fn union(self, _: Self) -> Self { pearlite! { absurd} diff --git a/creusot-contracts/src/model.rs b/creusot-contracts/src/model.rs index 91835cf59a..eea2b3cba6 100644 --- a/creusot-contracts/src/model.rs +++ b/creusot-contracts/src/model.rs @@ -8,7 +8,7 @@ use crate::*; /// Models of inner types are typically not involved. pub trait ShallowModel { type ShallowModelTy; - #[ghost] + #[logic] fn shallow_model(self) -> Self::ShallowModelTy; } @@ -24,13 +24,13 @@ pub use creusot_contracts_dummy::DeepModel; /// Typically, such a model recursively calls deep models of inner types. pub trait DeepModel { type DeepModelTy; - #[ghost] + #[logic] fn deep_model(self) -> Self::DeepModelTy; } impl DeepModel for Rc { type DeepModelTy = T::DeepModelTy; - #[ghost] + #[logic] #[open] fn deep_model(self) -> Self::DeepModelTy { pearlite! { self.shallow_model().deep_model() } @@ -39,7 +39,7 @@ impl DeepModel for Rc { impl ShallowModel for Rc { type ShallowModelTy = T; - #[ghost] + #[logic] #[open] #[trusted] fn shallow_model(self) -> Self::ShallowModelTy { @@ -49,7 +49,7 @@ impl ShallowModel for Rc { impl DeepModel for Arc { type DeepModelTy = T::DeepModelTy; - #[ghost] + #[logic] #[open] fn deep_model(self) -> Self::DeepModelTy { pearlite! { self@.deep_model() } @@ -58,7 +58,7 @@ impl DeepModel for Arc { impl ShallowModel for Arc { type ShallowModelTy = T; - #[ghost] + #[logic] #[open] #[trusted] fn shallow_model(self) -> Self::ShallowModelTy { @@ -68,7 +68,7 @@ impl ShallowModel for Arc { impl DeepModel for &T { type DeepModelTy = T::DeepModelTy; - #[ghost] + #[logic] #[open] fn deep_model(self) -> Self::DeepModelTy { (*self).deep_model() @@ -77,7 +77,7 @@ impl DeepModel for &T { impl ShallowModel for &T { type ShallowModelTy = T::ShallowModelTy; - #[ghost] + #[logic] #[open] fn shallow_model(self) -> Self::ShallowModelTy { (*self).shallow_model() @@ -86,7 +86,7 @@ impl ShallowModel for &T { impl DeepModel for &mut T { type DeepModelTy = T::DeepModelTy; - #[ghost] + #[logic] #[open] fn deep_model(self) -> Self::DeepModelTy { (*self).deep_model() @@ -95,7 +95,7 @@ impl DeepModel for &mut T { impl ShallowModel for &mut T { type ShallowModelTy = T::ShallowModelTy; - #[ghost] + #[logic] #[open] fn shallow_model(self) -> Self::ShallowModelTy { (*self).shallow_model() @@ -105,7 +105,7 @@ impl ShallowModel for &mut T { impl DeepModel for bool { type DeepModelTy = bool; - #[ghost] + #[logic] #[open] fn deep_model(self) -> Self::DeepModelTy { self diff --git a/creusot-contracts/src/num_rational.rs b/creusot-contracts/src/num_rational.rs index be700d066e..95cf6e595f 100644 --- a/creusot-contracts/src/num_rational.rs +++ b/creusot-contracts/src/num_rational.rs @@ -1,6 +1,6 @@ use std::marker::PhantomData; -use crate::{ghost, open, pearlite, trusted, DeepModel, Int, OrdLogic}; +use crate::{logic, open, pearlite, trusted, DeepModel, Int, OrdLogic}; use num_rational::BigRational; use std::cmp::Ordering; @@ -12,7 +12,7 @@ pub struct Real(PhantomData<*mut ()>); impl DeepModel for BigRational { type DeepModelTy = Real; - #[ghost] + #[logic] #[open(self)] #[trusted] fn deep_model(self) -> Self::DeepModelTy { @@ -21,7 +21,7 @@ impl DeepModel for BigRational { } impl Real { - #[ghost] + #[logic] #[trusted] #[open(self)] pub fn from_int(_: Int) -> Self { @@ -30,7 +30,7 @@ impl Real { } impl OrdLogic for Real { - #[ghost] + #[logic] #[open] fn cmp_log(self, o: Self) -> Ordering { if self < o { @@ -44,7 +44,7 @@ impl OrdLogic for Real { #[trusted] #[open] - #[ghost] + #[logic] #[creusot::builtins = "prelude.Real.(<=)"] fn le_log(self, _: Self) -> bool { true @@ -52,7 +52,7 @@ impl OrdLogic for Real { #[trusted] #[open] - #[ghost] + #[logic] #[creusot::builtins = "prelude.Real.(<)"] fn lt_log(self, _: Self) -> bool { true @@ -60,7 +60,7 @@ impl OrdLogic for Real { #[trusted] #[open] - #[ghost] + #[logic] #[creusot::builtins = "prelude.Real.(>=)"] fn ge_log(self, _: Self) -> bool { true @@ -68,7 +68,7 @@ impl OrdLogic for Real { #[trusted] #[open] - #[ghost] + #[logic] #[creusot::builtins = "prelude.Real.(>)"] fn gt_log(self, _: Self) -> bool { true diff --git a/creusot-contracts/src/resolve.rs b/creusot-contracts/src/resolve.rs index f2dc879bcc..ed297eb976 100644 --- a/creusot-contracts/src/resolve.rs +++ b/creusot-contracts/src/resolve.rs @@ -3,14 +3,14 @@ use crate::*; #[cfg_attr(creusot, rustc_diagnostic_item = "creusot_resolve")] #[trusted] pub trait Resolve { - #[predicate] + #[predicate(prophetic)] #[rustc_diagnostic_item = "creusot_resolve_method"] fn resolve(self) -> bool; } #[trusted] impl Resolve for (T1, T2) { - #[predicate] + #[predicate(prophetic)] #[open] fn resolve(self) -> bool { Resolve::resolve(self.0) && Resolve::resolve(self.1) @@ -19,7 +19,7 @@ impl Resolve for (T1, T2) { #[trusted] impl Resolve for &mut T { - #[predicate] + #[predicate(prophetic)] #[open] fn resolve(self) -> bool { pearlite! { ^self == *self } @@ -28,7 +28,7 @@ impl Resolve for &mut T { #[trusted] impl Resolve for Box { - #[predicate] + #[predicate(prophetic)] #[open] fn resolve(self) -> bool { Resolve::resolve(*self) diff --git a/creusot-contracts/src/snapshot.rs b/creusot-contracts/src/snapshot.rs index b0da99475c..4ba6827948 100644 --- a/creusot-contracts/src/snapshot.rs +++ b/creusot-contracts/src/snapshot.rs @@ -9,7 +9,7 @@ impl Deref for Snapshot { type Target = T; #[trusted] - #[ghost] + #[logic] #[open(self)] #[rustc_diagnostic_item = "snapshot_deref"] #[creusot::builtins = "prelude.Snapshot.inner"] @@ -21,7 +21,7 @@ impl Deref for Snapshot { impl ShallowModel for Snapshot { type ShallowModelTy = T::ShallowModelTy; - #[ghost] + #[logic] #[open] fn shallow_model(self) -> Self::ShallowModelTy { pearlite! { self.deref().shallow_model() } @@ -38,7 +38,7 @@ impl Copy for Snapshot {} impl Snapshot { #[trusted] - #[ghost] + #[logic] #[open(self)] #[creusot::builtins = "prelude.Snapshot.new"] pub fn new(_: T) -> Snapshot { @@ -46,7 +46,7 @@ impl Snapshot { } #[trusted] - #[ghost] + #[logic] #[open(self)] #[rustc_diagnostic_item = "snapshot_inner"] #[creusot::builtins = "prelude.Snapshot.inner"] diff --git a/creusot-contracts/src/std/array.rs b/creusot-contracts/src/std/array.rs index dc2f2d2501..d4badf497c 100644 --- a/creusot-contracts/src/std/array.rs +++ b/creusot-contracts/src/std/array.rs @@ -3,7 +3,7 @@ use crate::*; impl ShallowModel for [T; N] { type ShallowModelTy = Seq; - #[ghost] + #[logic] #[trusted] #[open] #[creusot::builtins = "prelude.Slice.id"] @@ -18,7 +18,7 @@ impl ShallowModel for [T; N] { impl DeepModel for [T; N] { type DeepModelTy = Seq; - #[ghost] + #[logic] #[trusted] #[open(self)] // TODO diff --git a/creusot-contracts/src/std/boxed.rs b/creusot-contracts/src/std/boxed.rs index 2e65842d17..cd686e68f5 100644 --- a/creusot-contracts/src/std/boxed.rs +++ b/creusot-contracts/src/std/boxed.rs @@ -4,7 +4,7 @@ pub use ::std::boxed::*; #[cfg(creusot)] impl DeepModel for Box { type DeepModelTy = Box; - #[ghost] + #[logic] #[open] fn deep_model(self) -> Self::DeepModelTy { Box::new((*self).deep_model()) @@ -14,7 +14,7 @@ impl DeepModel for Box { #[cfg(creusot)] impl ShallowModel for Box { type ShallowModelTy = T::ShallowModelTy; - #[ghost] + #[logic] #[open] fn shallow_model(self) -> Self::ShallowModelTy { (*self).shallow_model() diff --git a/creusot-contracts/src/std/cmp.rs b/creusot-contracts/src/std/cmp.rs index ea8c76d6ea..9db3799cce 100644 --- a/creusot-contracts/src/std/cmp.rs +++ b/creusot-contracts/src/std/cmp.rs @@ -64,7 +64,7 @@ extern_spec! { impl DeepModel for Reverse { type DeepModelTy = Reverse; - #[ghost] + #[logic] #[open] fn deep_model(self) -> Self::DeepModelTy { pearlite! { Reverse(self.0.deep_model()) } @@ -72,7 +72,7 @@ impl DeepModel for Reverse { } impl OrdLogic for Reverse { - #[ghost] + #[logic] #[open] fn cmp_log(self, o: Self) -> Ordering { match self.0.cmp_log(o.0) { diff --git a/creusot-contracts/src/std/default.rs b/creusot-contracts/src/std/default.rs index e95565db1e..b1770f27ab 100644 --- a/creusot-contracts/src/std/default.rs +++ b/creusot-contracts/src/std/default.rs @@ -2,7 +2,7 @@ use crate::*; pub use ::std::default::*; pub trait Default: ::std::default::Default { - #[predicate] + #[predicate(prophetic)] fn is_default(self) -> bool; } diff --git a/creusot-contracts/src/std/deque.rs b/creusot-contracts/src/std/deque.rs index 8dace155aa..3d06232b86 100644 --- a/creusot-contracts/src/std/deque.rs +++ b/creusot-contracts/src/std/deque.rs @@ -5,7 +5,7 @@ pub use ::std::collections::VecDeque; impl ShallowModel for VecDeque { type ShallowModelTy = Seq; - #[ghost] + #[logic] #[trusted] #[open(self)] #[ensures(result.len() <= usize::MAX@)] @@ -17,7 +17,7 @@ impl ShallowModel for VecDeque { impl DeepModel for VecDeque { type DeepModelTy = Seq; - #[ghost] + #[logic] #[trusted] #[open(self)] #[ensures(self.shallow_model().len() == result.len())] @@ -31,7 +31,7 @@ impl DeepModel for VecDeque { impl IndexLogic for VecDeque { type Item = T; - #[ghost] + #[logic] #[open] #[why3::attr = "inline:trivial"] fn index_logic(self, ix: Int) -> Self::Item { @@ -42,7 +42,7 @@ impl IndexLogic for VecDeque { impl IndexLogic for VecDeque { type Item = T; - #[ghost] + #[logic] #[open] #[why3::attr = "inline:trivial"] fn index_logic(self, ix: usize) -> Self::Item { @@ -115,7 +115,7 @@ impl IntoIterator for &VecDeque { impl<'a, T> ShallowModel for Iter<'a, T> { type ShallowModelTy = &'a [T]; - #[ghost] + #[logic] #[open(self)] #[trusted] fn shallow_model(self) -> Self::ShallowModelTy { @@ -126,7 +126,7 @@ impl<'a, T> ShallowModel for Iter<'a, T> { impl<'a, T> Invariant for Iter<'a, T> {} impl<'a, T> Iterator for Iter<'a, T> { - #[predicate] + #[predicate(prophetic)] #[open] fn completed(&mut self) -> bool { pearlite! { self.resolve() && (*self@)@ == Seq::EMPTY } diff --git a/creusot-contracts/src/std/iter.rs b/creusot-contracts/src/std/iter.rs index e2618d2bfb..e7d6544f14 100644 --- a/creusot-contracts/src/std/iter.rs +++ b/creusot-contracts/src/std/iter.rs @@ -24,10 +24,10 @@ pub use take::TakeExt; pub use zip::ZipExt; pub trait Iterator: ::std::iter::Iterator { - #[predicate] + #[predicate(prophetic)] fn produces(self, visited: Seq, o: Self) -> bool; - #[predicate] + #[predicate(prophetic)] fn completed(&mut self) -> bool; #[law] @@ -63,7 +63,7 @@ where pearlite! { true } } - #[predicate] + #[predicate(prophetic)] fn into_iter_post(self, res: Self::IntoIter) -> bool; } diff --git a/creusot-contracts/src/std/iter/cloned.rs b/creusot-contracts/src/std/iter/cloned.rs index 514b3abe13..09cef10136 100644 --- a/creusot-contracts/src/std/iter/cloned.rs +++ b/creusot-contracts/src/std/iter/cloned.rs @@ -1,13 +1,13 @@ use crate::{std::iter::Cloned, *}; pub trait ClonedExt { - #[ghost] + #[logic] fn iter(self) -> I; } impl ClonedExt for Cloned { #[open(self)] - #[ghost] + #[logic] #[trusted] fn iter(self) -> I { pearlite! { absurd } @@ -17,7 +17,7 @@ impl ClonedExt for Cloned { #[trusted] impl Resolve for Cloned { #[open] - #[predicate] + #[predicate(prophetic)] fn resolve(self) -> bool { pearlite! { self.iter().resolve() @@ -31,13 +31,13 @@ where T: Clone, { #[open] - #[predicate] + #[predicate(prophetic)] fn completed(&mut self) -> bool { pearlite! { exists *inner == self.iter() && ^inner == (^self).iter() && inner.completed() } } #[open] - #[predicate] + #[predicate(prophetic)] fn produces(self, visited: Seq, o: Self) -> bool { pearlite! { exists> self.iter().produces(s, o.iter()) diff --git a/creusot-contracts/src/std/iter/copied.rs b/creusot-contracts/src/std/iter/copied.rs index 0460d5178c..9944f4b4b6 100644 --- a/creusot-contracts/src/std/iter/copied.rs +++ b/creusot-contracts/src/std/iter/copied.rs @@ -1,13 +1,13 @@ use crate::{std::iter::Copied, *}; pub trait CopiedExt { - #[ghost] + #[logic] fn iter(self) -> I; } impl CopiedExt for Copied { #[open] - #[ghost] + #[logic] #[trusted] fn iter(self) -> I { pearlite! { absurd } @@ -17,7 +17,7 @@ impl CopiedExt for Copied { #[trusted] impl Resolve for Copied { #[open] - #[predicate] + #[predicate(prophetic)] fn resolve(self) -> bool { pearlite! { self.iter().resolve() @@ -31,13 +31,13 @@ where T: Copy, { #[open] - #[predicate] + #[predicate(prophetic)] fn completed(&mut self) -> bool { pearlite! { exists *inner == self.iter() && ^inner == (^self).iter() && inner.completed() } } #[open] - #[predicate] + #[predicate(prophetic)] fn produces(self, visited: Seq, o: Self) -> bool { pearlite! { exists> self.iter().produces(s, o.iter()) diff --git a/creusot-contracts/src/std/iter/empty.rs b/creusot-contracts/src/std/iter/empty.rs index 9fdc551ec7..52def108b0 100644 --- a/creusot-contracts/src/std/iter/empty.rs +++ b/creusot-contracts/src/std/iter/empty.rs @@ -2,7 +2,7 @@ use crate::{std::iter::Empty, *}; impl Iterator for Empty { #[open] - #[predicate] + #[predicate(prophetic)] fn completed(&mut self) -> bool { pearlite! { self.resolve() } } diff --git a/creusot-contracts/src/std/iter/enumerate.rs b/creusot-contracts/src/std/iter/enumerate.rs index f2d0172950..662f3cc642 100644 --- a/creusot-contracts/src/std/iter/enumerate.rs +++ b/creusot-contracts/src/std/iter/enumerate.rs @@ -1,23 +1,23 @@ use crate::{invariant::Invariant, std::iter::Enumerate, *}; pub trait EnumerateExt { - #[ghost] + #[logic] fn iter(self) -> I; - #[ghost] + #[logic] fn n(self) -> Int; } impl EnumerateExt for Enumerate { #[trusted] - #[ghost] + #[logic] #[open(self)] fn iter(self) -> I { absurd } #[trusted] - #[ghost] + #[logic] #[open(self)] fn n(self) -> Int { absurd @@ -27,7 +27,7 @@ impl EnumerateExt for Enumerate { #[trusted] impl Resolve for Enumerate { #[open] - #[predicate] + #[predicate(prophetic)] fn resolve(self) -> bool { pearlite! { self.iter().resolve() @@ -37,7 +37,7 @@ impl Resolve for Enumerate { impl Invariant for Enumerate { #[open(self)] - #[predicate] + #[predicate(prophetic)] fn invariant(self) -> bool { pearlite! { (forall, i: I> self.iter().produces(s, i) ==> self.n() + s.len() < std::usize::MAX@) @@ -51,13 +51,13 @@ where I: Iterator, { #[open] - #[predicate] + #[predicate(prophetic)] fn completed(&mut self) -> bool { pearlite! { exists *inner == self.iter() && ^inner == (^self).iter() && inner.completed() } } #[open] - #[predicate] + #[predicate(prophetic)] fn produces(self, visited: Seq, o: Self) -> bool { pearlite! { visited.len() == o.n() - self.n() diff --git a/creusot-contracts/src/std/iter/fuse.rs b/creusot-contracts/src/std/iter/fuse.rs index 1893a0a124..2ac534497a 100644 --- a/creusot-contracts/src/std/iter/fuse.rs +++ b/creusot-contracts/src/std/iter/fuse.rs @@ -3,7 +3,7 @@ use crate::{std::iter::Fuse, *}; impl ShallowModel for Fuse { type ShallowModelTy = Option; - #[ghost] + #[logic] #[open(self)] #[trusted] fn shallow_model(self) -> Option { @@ -13,7 +13,7 @@ impl ShallowModel for Fuse { impl Iterator for Fuse { #[open] - #[predicate] + #[predicate(prophetic)] fn completed(&mut self) -> bool { pearlite! { (self@ == None || exists it.completed() && self@ == Some(*it)) && @@ -22,7 +22,7 @@ impl Iterator for Fuse { } #[open] - #[predicate] + #[predicate(prophetic)] fn produces(self, prod: Seq, other: Self) -> bool { pearlite! { match self@ { diff --git a/creusot-contracts/src/std/iter/map_inv.rs b/creusot-contracts/src/std/iter/map_inv.rs index 406f74abf7..d71b1cc7e9 100644 --- a/creusot-contracts/src/std/iter/map_inv.rs +++ b/creusot-contracts/src/std/iter/map_inv.rs @@ -10,7 +10,7 @@ impl>) -> B> Iterator for MapInv { #[open] - #[predicate] + #[predicate(prophetic)] fn completed(&mut self) -> bool { pearlite! { *(^self).produced == Seq::EMPTY && @@ -31,7 +31,7 @@ impl>) -> B> Iterator fn produces_trans(a: Self, ab: Seq, b: Self, bc: Seq, c: Self) {} #[open] - #[predicate] + #[predicate(prophetic)] #[why3::attr = "inline:trivial"] fn produces(self, visited: Seq, succ: Self) -> bool { pearlite! { @@ -53,7 +53,7 @@ impl>) -> B> Iterator #[trusted] impl Resolve for MapInv { #[open] - #[predicate] + #[predicate(prophetic)] fn resolve(self) -> bool { self.iter.resolve() && self.func.resolve() } @@ -64,7 +64,7 @@ impl>) -> B> Invariant { // Should not quantify over self or the `invariant` cannot be made into a type invariant #[open(self)] - #[predicate] + #[predicate(prophetic)] fn invariant(self) -> bool { pearlite! { Self::reinitialize() && @@ -107,7 +107,7 @@ impl>) -> B> ::std::iter impl>) -> B> MapInv { #[open] - #[predicate] + #[predicate(prophetic)] pub fn next_precondition(iter: I, func: F, produced: Seq) -> bool { pearlite! { forall @@ -116,7 +116,7 @@ impl>) -> B> MapInv result == Self::preservation(iter, func))] fn preservation_inv(iter: I, func: F, produced: Seq) -> bool { pearlite! { @@ -130,7 +130,7 @@ impl>) -> B> MapInv bool { pearlite! { forall, e1: I::Item, e2: I::Item, f: &mut F, b: B, i: I> @@ -143,7 +143,7 @@ impl>) -> B> MapInv bool { pearlite! { forall @@ -153,7 +153,7 @@ impl>) -> B> MapInv>) -> B> MapInv bool { pearlite! { diff --git a/creusot-contracts/src/std/iter/once.rs b/creusot-contracts/src/std/iter/once.rs index ad96988263..000d18ca89 100644 --- a/creusot-contracts/src/std/iter/once.rs +++ b/creusot-contracts/src/std/iter/once.rs @@ -3,7 +3,7 @@ use crate::{std::iter::Once, *}; impl ShallowModel for Once { type ShallowModelTy = Option; - #[ghost] + #[logic] #[trusted] #[open(self)] fn shallow_model(self) -> Option { @@ -13,7 +13,7 @@ impl ShallowModel for Once { impl Iterator for Once { #[open] - #[predicate] + #[predicate(prophetic)] fn completed(&mut self) -> bool { pearlite! { (*self)@ == None && self.resolve() } } diff --git a/creusot-contracts/src/std/iter/range.rs b/creusot-contracts/src/std/iter/range.rs index db68337ff0..2a21d42f9e 100644 --- a/creusot-contracts/src/std/iter/range.rs +++ b/creusot-contracts/src/std/iter/range.rs @@ -7,7 +7,7 @@ use crate::{ }; impl + Step> Iterator for Range { - #[predicate] + #[predicate(prophetic)] #[open] fn completed(&mut self) -> bool { pearlite! { @@ -40,7 +40,7 @@ impl + Step> Iterator for Range { fn produces_trans(a: Self, ab: Seq, b: Self, bc: Seq, c: Self) {} } -#[ghost] +#[logic] #[open] #[ensures(r.is_empty_log() == (result == 0))] pub fn range_inclusive_len>(r: RangeInclusive) -> Int { @@ -51,7 +51,7 @@ pub fn range_inclusive_len>(r: RangeInclusive< } impl + Step> Iterator for RangeInclusive { - #[predicate] + #[predicate(prophetic)] #[open] fn completed(&mut self) -> bool { pearlite! { diff --git a/creusot-contracts/src/std/iter/repeat.rs b/creusot-contracts/src/std/iter/repeat.rs index 2dd172cec5..156c00b34c 100644 --- a/creusot-contracts/src/std/iter/repeat.rs +++ b/creusot-contracts/src/std/iter/repeat.rs @@ -3,7 +3,7 @@ use crate::{std::iter::Repeat, *}; impl ShallowModel for Repeat { type ShallowModelTy = T; - #[ghost] + #[logic] #[trusted] #[open(self)] fn shallow_model(self) -> T { diff --git a/creusot-contracts/src/std/iter/skip.rs b/creusot-contracts/src/std/iter/skip.rs index 830306e384..0c3acd035d 100644 --- a/creusot-contracts/src/std/iter/skip.rs +++ b/creusot-contracts/src/std/iter/skip.rs @@ -1,22 +1,22 @@ use crate::{std::iter::Skip, *}; pub trait SkipExt { - #[ghost] + #[logic] fn iter(self) -> I; - #[ghost] + #[logic] fn n(self) -> Int; } impl SkipExt for Skip { - #[ghost] + #[logic] #[open(self)] #[trusted] fn iter(self) -> I { pearlite! { absurd } } - #[ghost] + #[logic] #[open(self)] #[trusted] #[ensures(result >= 0 && result <= usize::MAX@)] @@ -28,7 +28,7 @@ impl SkipExt for Skip { #[trusted] impl Resolve for Skip { #[open] - #[predicate] + #[predicate(prophetic)] fn resolve(self) -> bool { pearlite! { self.iter().resolve() @@ -38,7 +38,7 @@ impl Resolve for Skip { impl Iterator for Skip { #[open] - #[predicate] + #[predicate(prophetic)] fn completed(&mut self) -> bool { pearlite! { (^self).n() == 0 && @@ -52,7 +52,7 @@ impl Iterator for Skip { } #[open] - #[predicate] + #[predicate(prophetic)] fn produces(self, visited: Seq, o: Self) -> bool { pearlite! { visited == Seq::EMPTY && self == o || diff --git a/creusot-contracts/src/std/iter/take.rs b/creusot-contracts/src/std/iter/take.rs index f4d7b57185..25d76f10b9 100644 --- a/creusot-contracts/src/std/iter/take.rs +++ b/creusot-contracts/src/std/iter/take.rs @@ -1,25 +1,25 @@ use crate::{std::iter::Take, *}; pub trait TakeExt { - #[ghost] + #[logic] fn iter(self) -> I; - #[ghost] + #[logic] fn iter_mut(&mut self) -> &mut I; - #[ghost] + #[logic] fn n(self) -> Int; } impl TakeExt for Take { - #[ghost] + #[logic] #[trusted] #[open(self)] fn iter(self) -> I { pearlite! { absurd } } - #[ghost] + #[logic] #[trusted] #[open(self)] #[ensures((*self).iter() == *result && (^self).iter() == ^result)] @@ -27,7 +27,7 @@ impl TakeExt for Take { pearlite! { absurd } } - #[ghost] + #[logic] #[trusted] #[open(self)] #[ensures(result >= 0 && result <= usize::MAX@)] @@ -39,7 +39,7 @@ impl TakeExt for Take { #[trusted] impl Resolve for Take { #[open] - #[predicate] + #[predicate(prophetic)] fn resolve(self) -> bool { pearlite! { self.iter().resolve() @@ -49,7 +49,7 @@ impl Resolve for Take { impl Iterator for Take { #[open] - #[predicate] + #[predicate(prophetic)] fn completed(&mut self) -> bool { pearlite! { self.n() == 0 && self.resolve() || @@ -58,7 +58,7 @@ impl Iterator for Take { } #[open] - #[predicate] + #[predicate(prophetic)] fn produces(self, visited: Seq, o: Self) -> bool { pearlite! { self.n() == o.n() + visited.len() && self.iter().produces(visited, o.iter()) diff --git a/creusot-contracts/src/std/iter/zip.rs b/creusot-contracts/src/std/iter/zip.rs index 409f2fa485..a5f1069ad2 100644 --- a/creusot-contracts/src/std/iter/zip.rs +++ b/creusot-contracts/src/std/iter/zip.rs @@ -1,22 +1,22 @@ use crate::{std::iter::Zip, *}; pub trait ZipExt { - #[ghost] + #[logic] fn itera(self) -> A; - #[ghost] + #[logic] fn iterb(self) -> B; } impl ZipExt for Zip { - #[ghost] + #[logic] #[open(self)] #[trusted] fn itera(self) -> A { pearlite! { absurd } } - #[ghost] + #[logic] #[open(self)] #[trusted] fn iterb(self) -> B { @@ -26,7 +26,7 @@ impl ZipExt for Zip { impl Iterator for Zip { #[open] - #[predicate] + #[predicate(prophetic)] fn completed(&mut self) -> bool { pearlite! { exists @@ -39,7 +39,7 @@ impl Iterator for Zip { } #[open] - #[predicate] + #[predicate(prophetic)] fn produces(self, visited: Seq, o: Self) -> bool { pearlite! { // Using an `unzip` definition doesn't work well because of issues related to datatypes and `match` diff --git a/creusot-contracts/src/std/num.rs b/creusot-contracts/src/std/num.rs index 6ea805cfae..5eadb2b86d 100644 --- a/creusot-contracts/src/std/num.rs +++ b/creusot-contracts/src/std/num.rs @@ -5,7 +5,7 @@ macro_rules! mach_int { ($t:ty, $ty_nm:expr, $zero:expr) => { impl ShallowModel for $t { type ShallowModelTy = Int; - #[ghost] + #[logic] #[open] #[trusted] #[creusot::builtins = concat!($ty_nm, ".to_int")] @@ -16,7 +16,7 @@ macro_rules! mach_int { impl DeepModel for $t { type DeepModelTy = Int; - #[ghost] + #[logic] #[open] fn deep_model(self) -> Self::DeepModelTy { pearlite! { self@ } diff --git a/creusot-contracts/src/std/ops.rs b/creusot-contracts/src/std/ops.rs index e07157388d..d4c0912267 100644 --- a/creusot-contracts/src/std/ops.rs +++ b/creusot-contracts/src/std/ops.rs @@ -172,13 +172,13 @@ extern_spec! { } pub trait RangeInclusiveExt { - #[ghost] + #[logic] fn start_log(self) -> Idx; - #[ghost] + #[logic] fn end_log(self) -> Idx; - #[ghost] + #[logic] fn is_empty_log(self) -> bool where Idx: DeepModel, @@ -187,21 +187,21 @@ pub trait RangeInclusiveExt { impl RangeInclusiveExt for RangeInclusive { #[open(self)] - #[ghost] + #[logic] #[trusted] fn start_log(self) -> Idx { pearlite! { absurd } } #[open(self)] - #[ghost] + #[logic] #[trusted] fn end_log(self) -> Idx { pearlite! { absurd } } #[open(self)] - #[ghost] + #[logic] #[trusted] #[ensures(!result ==> self.start_log().deep_model() <= self.end_log().deep_model())] fn is_empty_log(self) -> bool diff --git a/creusot-contracts/src/std/option.rs b/creusot-contracts/src/std/option.rs index 3470d856f4..accd4a752f 100644 --- a/creusot-contracts/src/std/option.rs +++ b/creusot-contracts/src/std/option.rs @@ -4,7 +4,7 @@ pub use ::std::option::*; impl DeepModel for Option { type DeepModelTy = Option; - #[ghost] + #[logic] #[open] fn deep_model(self) -> Self::DeepModelTy { match self { @@ -137,7 +137,7 @@ impl ShallowModel for IntoIter { type ShallowModelTy = Option; #[open(self)] - #[ghost] + #[logic] #[trusted] fn shallow_model(self) -> Option { pearlite! { absurd } @@ -145,7 +145,7 @@ impl ShallowModel for IntoIter { } impl Iterator for IntoIter { - #[predicate] + #[predicate(prophetic)] #[open] fn completed(&mut self) -> bool { pearlite! { (*self)@ == None && self.resolve() } @@ -191,7 +191,7 @@ impl<'a, T> ShallowModel for Iter<'a, T> { type ShallowModelTy = Option<&'a T>; #[open(self)] - #[ghost] + #[logic] #[trusted] fn shallow_model(self) -> Option<&'a T> { pearlite! { absurd } @@ -199,7 +199,7 @@ impl<'a, T> ShallowModel for Iter<'a, T> { } impl<'a, T> Iterator for Iter<'a, T> { - #[predicate] + #[predicate(prophetic)] #[open] fn completed(&mut self) -> bool { pearlite! { (*self)@ == None && self.resolve() } @@ -247,7 +247,7 @@ impl<'a, T> IntoIterator for &'a Option { impl<'a, T> ShallowModel for IterMut<'a, T> { type ShallowModelTy = Option<&'a mut T>; - #[ghost] + #[logic] #[open(self)] #[trusted] fn shallow_model(self) -> Option<&'a mut T> { @@ -256,7 +256,7 @@ impl<'a, T> ShallowModel for IterMut<'a, T> { } impl<'a, T> Iterator for IterMut<'a, T> { - #[predicate] + #[predicate(prophetic)] #[open] fn completed(&mut self) -> bool { pearlite! { (*self)@ == None && self.resolve() } @@ -291,7 +291,7 @@ impl<'a, T> IntoIterator for &'a mut Option { pearlite! { true } } - #[predicate] + #[predicate(prophetic)] #[open] fn into_iter_post(self, res: Self::IntoIter) -> bool { pearlite! { diff --git a/creusot-contracts/src/std/result.rs b/creusot-contracts/src/std/result.rs index 9fd665d826..0a746d8f4b 100644 --- a/creusot-contracts/src/std/result.rs +++ b/creusot-contracts/src/std/result.rs @@ -5,7 +5,7 @@ use ::std::fmt::Debug; impl DeepModel for Result { type DeepModelTy = Result; - #[ghost] + #[logic] #[open] fn deep_model(self) -> Self::DeepModelTy { match self { diff --git a/creusot-contracts/src/std/slice.rs b/creusot-contracts/src/std/slice.rs index 96ecb87765..a1d67f0e7b 100644 --- a/creusot-contracts/src/std/slice.rs +++ b/creusot-contracts/src/std/slice.rs @@ -11,7 +11,7 @@ impl ShallowModel for [T] { type ShallowModelTy = Seq; // We define this as trusted because builtins and ensures are incompatible - #[ghost] + #[logic] #[open(self)] #[trusted] #[ensures(result.len() <= usize::MAX@)] @@ -24,7 +24,7 @@ impl ShallowModel for [T] { impl DeepModel for [T] { type DeepModelTy = Seq; - #[ghost] + #[logic] #[open(self)] #[trusted] #[ensures((&self)@.len() == result.len())] @@ -34,14 +34,14 @@ impl DeepModel for [T] { } } -#[ghost] +#[logic] #[trusted] #[creusot::builtins = "prelude.Slice.id"] fn slice_model(_: &[T]) -> Seq { pearlite! { absurd } } -#[ghost] +#[logic] #[open] #[rustc_diagnostic_item = "slice_len_logic"] pub fn slice_len(x: [T]) -> Int { @@ -50,7 +50,7 @@ pub fn slice_len(x: [T]) -> Int { impl Default for &mut [T] { #[open] - #[predicate] + #[predicate(prophetic)] fn is_default(self) -> bool { pearlite! { self@ == Seq::EMPTY && (^self)@ == Seq::EMPTY } } @@ -65,15 +65,15 @@ impl Default for &[T] { } pub trait SliceExt { - #[ghost] + #[logic] fn to_mut_seq(&mut self) -> Seq<&mut T>; - #[ghost] + #[logic] fn to_ref_seq(&self) -> Seq<&T>; } impl SliceExt for [T] { - #[ghost] + #[logic] #[trusted] #[open(self)] #[ensures(result.len() == self@.len())] @@ -83,7 +83,7 @@ impl SliceExt for [T] { pearlite! { absurd } } - #[ghost] + #[logic] #[open(self)] #[trusted] #[ensures(result.len() == self@.len())] @@ -364,7 +364,7 @@ impl IntoIterator for &mut [T] { impl<'a, T> ShallowModel for Iter<'a, T> { type ShallowModelTy = &'a [T]; - #[ghost] + #[logic] #[open(self)] #[trusted] fn shallow_model(self) -> Self::ShallowModelTy { @@ -373,7 +373,7 @@ impl<'a, T> ShallowModel for Iter<'a, T> { } impl<'a, T> Iterator for Iter<'a, T> { - #[predicate] + #[predicate(prophetic)] #[open] fn completed(&mut self) -> bool { pearlite! { self.resolve() && (*self@)@ == Seq::EMPTY } @@ -403,7 +403,7 @@ impl<'a, T> Iterator for Iter<'a, T> { impl<'a, T> ShallowModel for IterMut<'a, T> { type ShallowModelTy = &'a mut [T]; - #[ghost] + #[logic] #[open(self)] #[trusted] #[ensures((^result)@.len() == (*result)@.len())] @@ -414,7 +414,7 @@ impl<'a, T> ShallowModel for IterMut<'a, T> { #[trusted] impl<'a, T> Resolve for IterMut<'a, T> { - #[predicate] + #[predicate(prophetic)] #[open] fn resolve(self) -> bool { pearlite! { *self@ == ^self@ } @@ -422,7 +422,7 @@ impl<'a, T> Resolve for IterMut<'a, T> { } impl<'a, T> Iterator for IterMut<'a, T> { - #[predicate] + #[predicate(prophetic)] #[open] fn completed(&mut self) -> bool { pearlite! { self.resolve() && (*self@)@ == Seq::EMPTY } diff --git a/creusot-contracts/src/std/time.rs b/creusot-contracts/src/std/time.rs index 3178c16e9c..6b087f06b6 100644 --- a/creusot-contracts/src/std/time.rs +++ b/creusot-contracts/src/std/time.rs @@ -7,7 +7,7 @@ pub use ::std::{ impl ShallowModel for Duration { type ShallowModelTy = Int; - #[ghost] + #[logic] #[open(self)] #[trusted] #[ensures(result >= 0 && result <= secs_to_nanos(u64::MAX@) + 999_999_999)] @@ -19,7 +19,7 @@ impl ShallowModel for Duration { impl DeepModel for Duration { type DeepModelTy = Int; - #[ghost] + #[logic] #[open(self)] #[trusted] #[ensures(result >= 0 && result <= secs_to_nanos(u64::MAX@) + 999_999_999)] @@ -29,21 +29,21 @@ impl DeepModel for Duration { } } -#[ghost] +#[logic] fn nanos_to_micros(nanos: Int) -> Int { nanos / 1_000 } -#[ghost] +#[logic] fn nanos_to_millis(nanos: Int) -> Int { nanos / 1_000_000 } -#[ghost] +#[logic] fn nanos_to_secs(nanos: Int) -> Int { nanos / 1_000_000_000 } -#[ghost] +#[logic] fn secs_to_nanos(secs: Int) -> Int { secs * 1_000_000_000 } @@ -51,7 +51,7 @@ fn secs_to_nanos(secs: Int) -> Int { impl ShallowModel for Instant { type ShallowModelTy = Int; - #[ghost] + #[logic] #[open(self)] #[trusted] #[ensures(result >= 0)] @@ -63,7 +63,7 @@ impl ShallowModel for Instant { impl DeepModel for Instant { type DeepModelTy = Int; - #[ghost] + #[logic] #[open(self)] #[trusted] #[ensures(result >= 0)] diff --git a/creusot-contracts/src/std/tuples.rs b/creusot-contracts/src/std/tuples.rs index 74d29bdf97..0aa1ed6c60 100644 --- a/creusot-contracts/src/std/tuples.rs +++ b/creusot-contracts/src/std/tuples.rs @@ -3,7 +3,7 @@ use crate::{Default, *}; impl DeepModel for () { type DeepModelTy = (); - #[ghost] + #[logic] #[open] fn deep_model(self) -> Self::DeepModelTy { pearlite! { () } @@ -23,7 +23,7 @@ macro_rules! tuple_impls { impl<$($name: DeepModel),+> DeepModel for ($($name,)+) { type DeepModelTy = ($($name::DeepModelTy,)+); - #[ghost] + #[logic] #[open] fn deep_model(self) -> Self::DeepModelTy { pearlite! { ($(self.$idx.deep_model(),)+) } @@ -31,7 +31,7 @@ macro_rules! tuple_impls { } impl<$($name: Default),+> Default for ($($name,)+) { - #[predicate] + #[predicate(prophetic)] #[open] fn is_default(self) -> bool { pearlite! { $(self.$idx.is_default())&&+ } diff --git a/creusot-contracts/src/std/vec.rs b/creusot-contracts/src/std/vec.rs index b2251ecaa4..efacdeaa04 100644 --- a/creusot-contracts/src/std/vec.rs +++ b/creusot-contracts/src/std/vec.rs @@ -13,7 +13,7 @@ impl ShallowModel for Vec { type ShallowModelTy = Seq; #[open(self)] - #[ghost] + #[logic] #[trusted] #[ensures(result.len() <= usize::MAX@)] fn shallow_model(self) -> Seq { @@ -24,7 +24,7 @@ impl ShallowModel for Vec { impl DeepModel for Vec { type DeepModelTy = Seq; - #[ghost] + #[logic] #[open(self)] #[trusted] #[ensures(self.shallow_model().len() == result.len())] @@ -45,7 +45,7 @@ impl Default for Vec { #[trusted] impl Resolve for Vec { - #[predicate] + #[predicate(prophetic)] #[open] fn resolve(self) -> bool { pearlite! { forall 0 <= i && i < self@.len() ==> self[i].resolve() } @@ -207,7 +207,7 @@ impl ShallowModel for std::vec::IntoIter { type ShallowModelTy = Seq; #[open(self)] - #[ghost] + #[logic] #[trusted] fn shallow_model(self) -> Self::ShallowModelTy { absurd @@ -216,7 +216,7 @@ impl ShallowModel for std::vec::IntoIter { #[trusted] impl Resolve for std::vec::IntoIter { - #[predicate] + #[predicate(prophetic)] #[open] fn resolve(self) -> bool { pearlite! { forall 0 <= i && i < self@.len() ==> self@[i].resolve() } @@ -224,7 +224,7 @@ impl Resolve for std::vec::IntoIter { } impl Iterator for std::vec::IntoIter { - #[predicate] + #[predicate(prophetic)] #[open] fn completed(&mut self) -> bool { pearlite! { self.resolve() && self@ == Seq::EMPTY } diff --git a/creusot-contracts/src/util.rs b/creusot-contracts/src/util.rs index a719a9cb15..da7ea0126d 100644 --- a/creusot-contracts/src/util.rs +++ b/creusot-contracts/src/util.rs @@ -3,14 +3,14 @@ use crate::*; pub type SizedW = Box; pub trait MakeSized { - #[ghost] + #[logic] #[why3::attr = "inline:trivial"] fn make_sized(&self) -> SizedW; } impl MakeSized for T { #[trusted] - #[ghost] + #[logic] #[open(self)] #[ensures(*result == *self)] fn make_sized(&self) -> SizedW { @@ -19,7 +19,7 @@ impl MakeSized for T { } #[allow(unconditional_recursion)] -#[ghost] +#[logic] #[open(self)] #[requires(false)] #[ensures(false)] @@ -28,7 +28,7 @@ pub fn unreachable() -> T { unreachable() } -#[ghost] +#[logic] #[open(self)] #[requires(op != None)] #[ensures(Some(result) == op)] diff --git a/creusot/src/backend.rs b/creusot/src/backend.rs index 71ffbf4434..f04ad83442 100644 --- a/creusot/src/backend.rs +++ b/creusot/src/backend.rs @@ -140,9 +140,8 @@ impl<'tcx> Why3Generator<'tcx> { self.finish(def_id); } } - ItemType::Ghost - | ItemType::Logic - | ItemType::Predicate + ItemType::Logic { .. } + | ItemType::Predicate { .. } | ItemType::Program | ItemType::Closure => { self.start(def_id); @@ -200,7 +199,7 @@ impl<'tcx> Why3Generator<'tcx> { } let translated = match util::item_type(self.tcx, def_id) { - ItemType::Ghost | ItemType::Logic | ItemType::Predicate => { + ItemType::Logic { .. } | ItemType::Predicate { .. } => { debug!("translating {:?} as logical", def_id); let (proof_modl, deps) = logic::translate_logic_or_predicate(self, def_id); self.dependencies.insert(def_id.into(), deps); @@ -340,7 +339,7 @@ impl<'tcx> Why3Generator<'tcx> { fn is_logical(&self, item: DefId) -> bool { matches!( util::item_type(self.tcx, item), - ItemType::Logic | ItemType::Predicate | ItemType::Ghost + ItemType::Logic { .. } | ItemType::Predicate { .. } ) } diff --git a/creusot/src/backend/logic.rs b/creusot/src/backend/logic.rs index 54149df259..f12938d782 100644 --- a/creusot/src/backend/logic.rs +++ b/creusot/src/backend/logic.rs @@ -334,11 +334,11 @@ fn proof_module(ctx: &mut Why3Generator, def_id: DefId) -> Option { decls.extend(clones); let kind = match util::item_type(ctx.tcx, def_id) { - ItemType::Predicate => { + ItemType::Predicate { .. } => { sig.retty = None; Some(LetKind::Predicate) } - ItemType::Ghost | ItemType::Logic => Some(LetKind::Function), + ItemType::Logic { .. } => Some(LetKind::Function), _ => unreachable!(), }; diff --git a/creusot/src/backend/ty.rs b/creusot/src/backend/ty.rs index ae04467845..3d981be8b3 100644 --- a/creusot/src/backend/ty.rs +++ b/creusot/src/backend/ty.rs @@ -156,7 +156,7 @@ fn translate_ty_inner<'tcx, N: Namer<'tcx>>( Closure(id, subst) => { ctx.translate(*id); - if util::is_ghost(ctx.tcx, *id) { + if util::is_logic(ctx.tcx, *id) { return MlT::Tuple(Vec::new()); } diff --git a/creusot/src/ctx.rs b/creusot/src/ctx.rs index b38cb6749e..69832951a8 100644 --- a/creusot/src/ctx.rs +++ b/creusot/src/ctx.rs @@ -318,7 +318,7 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> { fn mk_opacity(&self, item: DefId) -> Opacity { if !matches!( util::item_type(self.tcx, item), - ItemType::Predicate | ItemType::Logic | ItemType::Ghost + ItemType::Predicate { .. } | ItemType::Logic { .. } ) { return Opacity(Visibility::Public); }; diff --git a/creusot/src/translation.rs b/creusot/src/translation.rs index 2c5c35eb61..eb7886735a 100644 --- a/creusot/src/translation.rs +++ b/creusot/src/translation.rs @@ -34,7 +34,6 @@ pub(crate) fn before_analysis(ctx: &mut TranslationCtx) -> Result<(), Box bool { #[derive(Clone, Copy, PartialEq, Eq, Debug)] pub(crate) enum Purity { Program, - Ghost, - Logic, + Logic { prophetic: bool }, } impl Purity { pub(crate) fn of_def_id<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId) -> Self { let is_snapshot = util::is_snapshot_closure(tcx, def_id); - if util::is_predicate(tcx, def_id) - || util::is_logic(tcx, def_id) + if (util::is_predicate(tcx, def_id) && util::is_prophetic(tcx, def_id)) + || (util::is_logic(tcx, def_id) && util::is_prophetic(tcx, def_id)) || (util::is_spec(tcx, def_id) && !is_snapshot) { - Purity::Logic - } else if util::is_ghost(tcx, def_id) || is_snapshot { - Purity::Ghost + Purity::Logic { prophetic: true } + } else if util::is_predicate(tcx, def_id) || util::is_logic(tcx, def_id) || is_snapshot { + Purity::Logic { prophetic: false } } else { Purity::Program } @@ -329,12 +328,22 @@ impl Purity { fn can_call(self, other: Purity) -> bool { match (self, other) { - (Purity::Logic, Purity::Ghost) => true, + (Purity::Logic { prophetic: true }, Purity::Logic { prophetic: false }) => true, (ctx, call) => ctx == call, } } } +impl std::fmt::Display for Purity { + fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { + f.write_str(match self { + Purity::Program => "program", + Purity::Logic { prophetic: false } => "logic", + Purity::Logic { prophetic: true } => "prophetic logic", + }) + } +} + pub(crate) struct PurityVisitor<'a, 'tcx> { pub(crate) tcx: TyCtxt<'tcx>, pub(crate) thir: &'a Thir<'tcx>, @@ -346,15 +355,16 @@ impl<'a, 'tcx> PurityVisitor<'a, 'tcx> { let stub = pearlite_stub(self.tcx, self.thir[fun].ty); if matches!(stub, Some(Stub::Fin)) - || util::is_predicate(self.tcx, func_did) - || util::is_logic(self.tcx, func_did) + || (util::is_predicate(self.tcx, func_did) && util::is_prophetic(self.tcx, func_did)) + || (util::is_logic(self.tcx, func_did) && util::is_prophetic(self.tcx, func_did)) { - Purity::Logic - } else if util::is_ghost(self.tcx, func_did) + Purity::Logic { prophetic: true } + } else if util::is_predicate(self.tcx, func_did) + || util::is_logic(self.tcx, func_did) || util::get_builtin(self.tcx, func_did).is_some() || stub.is_some() { - Purity::Ghost + Purity::Logic { prophetic: false } } else { Purity::Program } @@ -373,11 +383,13 @@ impl<'a, 'tcx> thir::visit::Visitor<'a, 'tcx> for PurityVisitor<'a, 'tcx> { let fn_purity = self.purity(fun, func_did); if !self.context.can_call(fn_purity) && !is_overloaded_item(self.tcx, func_did) { - let msg = - format!("called {fn_purity:?} function in {:?} context", self.context); self.tcx.sess.span_err_with_code( self.thir[fun].span, - format!("{} {:?}", msg, self.tcx.def_path_str(func_did)), + format!( + "called {fn_purity} function {:?} in {} context", + self.tcx.def_path_str(func_did), + self.context, + ), rustc_errors::DiagnosticId::Error(String::from("creusot")), ); } diff --git a/creusot/src/util.rs b/creusot/src/util.rs index dc81964b52..808a5dad66 100644 --- a/creusot/src/util.rs +++ b/creusot/src/util.rs @@ -35,10 +35,7 @@ use why3::{ }; pub(crate) fn no_mir(tcx: TyCtxt, def_id: DefId) -> bool { - crate::util::is_no_translate(tcx, def_id) - || crate::util::is_ghost(tcx, def_id) - || crate::util::is_predicate(tcx, def_id) - || crate::util::is_logic(tcx, def_id) + is_no_translate(tcx, def_id) || is_predicate(tcx, def_id) || is_logic(tcx, def_id) } pub(crate) fn is_no_translate(tcx: TyCtxt, def_id: DefId) -> bool { @@ -90,12 +87,12 @@ pub(crate) fn is_logic(tcx: TyCtxt, def_id: DefId) -> bool { get_attr(tcx.get_attrs_unchecked(def_id), &["creusot", "decl", "logic"]).is_some() } -pub(crate) fn is_predicate(tcx: TyCtxt, def_id: DefId) -> bool { - get_attr(tcx.get_attrs_unchecked(def_id), &["creusot", "decl", "predicate"]).is_some() +pub(crate) fn is_prophetic(tcx: TyCtxt, def_id: DefId) -> bool { + get_attr(tcx.get_attrs_unchecked(def_id), &["creusot", "decl", "logic", "prophetic"]).is_some() } -pub(crate) fn is_ghost(tcx: TyCtxt, def_id: DefId) -> bool { - get_attr(tcx.get_attrs_unchecked(def_id), &["creusot", "decl", "ghost"]).is_some() +pub(crate) fn is_predicate(tcx: TyCtxt, def_id: DefId) -> bool { + get_attr(tcx.get_attrs_unchecked(def_id), &["creusot", "decl", "predicate"]).is_some() } pub(crate) fn is_trusted(tcx: TyCtxt, def_id: DefId) -> bool { @@ -180,7 +177,7 @@ pub(crate) fn has_body(ctx: &mut TranslationCtx, def_id: DefId) -> bool { ctx.tcx.hir().maybe_body_owned_by(local_id).is_some() } else { match item_type(ctx.tcx, def_id) { - ItemType::Ghost | ItemType::Logic | ItemType::Predicate => ctx.term(def_id).is_some(), + ItemType::Logic { .. } | ItemType::Predicate { .. } => ctx.term(def_id).is_some(), _ => false, } } @@ -296,9 +293,8 @@ fn ident_path(tcx: TyCtxt, def_id: DefId) -> Ident { #[derive(Clone, Copy, Debug, PartialEq, Eq)] pub enum ItemType { - Logic, - Predicate, - Ghost, + Logic { prophetic: bool }, + Predicate { prophetic: bool }, Program, Closure, Trait, @@ -312,8 +308,8 @@ pub enum ItemType { impl ItemType { pub(crate) fn let_kind(&self) -> Option { match self { - ItemType::Logic | ItemType::Ghost => Some(LetKind::Function), - ItemType::Predicate => Some(LetKind::Predicate), + ItemType::Logic { .. } => Some(LetKind::Function), + ItemType::Predicate { .. } => Some(LetKind::Predicate), ItemType::Program | ItemType::Closure => None, ItemType::Constant => Some(LetKind::Constant), _ => None, @@ -322,10 +318,10 @@ impl ItemType { pub(crate) fn val(&self, mut sig: Signature) -> ValDecl { match self { - ItemType::Logic | ItemType::Ghost => { + ItemType::Logic { .. } => { ValDecl { sig, ghost: false, val: false, kind: Some(LetKind::Function) } } - ItemType::Predicate => { + ItemType::Predicate { .. } => { sig.retty = None; ValDecl { sig, ghost: false, val: false, kind: Some(LetKind::Predicate) } } @@ -341,9 +337,10 @@ impl ItemType { pub(crate) fn to_str(&self) -> &str { match self { - ItemType::Logic => "logic function", - ItemType::Predicate => "predicate", - ItemType::Ghost => "ghost function", + ItemType::Logic { prophetic: false } => "logic function", + ItemType::Logic { prophetic: true } => "prophetic logic function", + ItemType::Predicate { prophetic: false } => "predicate", + ItemType::Predicate { prophetic: true } => "prophetic predicate", ItemType::Program => "program function", ItemType::Closure => "closure", ItemType::Trait => "trait declaration", @@ -354,6 +351,16 @@ impl ItemType { ItemType::Unsupported(_) => "[OTHER]", } } + + pub(crate) fn can_implement(self, trait_type: Self) -> bool { + match (self, trait_type) { + (ItemType::Logic { prophetic: false }, ItemType::Logic { prophetic: true }) => true, + (ItemType::Predicate { prophetic: false }, ItemType::Predicate { prophetic: true }) => { + true + } + _ => self == trait_type, + } + } } pub(crate) fn item_type(tcx: TyCtxt<'_>, def_id: DefId) -> ItemType { @@ -362,11 +369,9 @@ pub(crate) fn item_type(tcx: TyCtxt<'_>, def_id: DefId) -> ItemType { DefKind::Impl { .. } => ItemType::Impl, DefKind::Fn | DefKind::AssocFn => { if is_predicate(tcx, def_id) { - ItemType::Predicate - } else if is_ghost(tcx, def_id) { - ItemType::Ghost + ItemType::Predicate { prophetic: is_prophetic(tcx, def_id) } } else if is_logic(tcx, def_id) { - ItemType::Logic + ItemType::Logic { prophetic: is_prophetic(tcx, def_id) } } else { ItemType::Program } @@ -522,7 +527,7 @@ fn elaborate_type_invariants<'tcx>( ) { if is_user_tyinv(ctx.tcx, def_id) || is_inv_internal(ctx.tcx, def_id) - || (is_predicate(ctx.tcx, def_id) || is_ghost(ctx.tcx, def_id) || is_logic(ctx.tcx, def_id)) + || (is_predicate(ctx.tcx, def_id) || is_logic(ctx.tcx, def_id)) && pre_sig.contract.ensures.is_empty() { return; diff --git a/creusot/src/validate.rs b/creusot/src/validate.rs index d57a5e7a47..895efe5283 100644 --- a/creusot/src/validate.rs +++ b/creusot/src/validate.rs @@ -132,18 +132,15 @@ pub(crate) fn validate_impls(ctx: &TranslationCtx) { continue; }; - if util::item_type(ctx.tcx, *trait_item) != util::item_type(ctx.tcx, *impl_item) { - eprintln!( - "{:?} != {:?}", - util::item_type(ctx.tcx, *trait_item), - util::item_type(ctx.tcx, *impl_item) - ); + let item_type = util::item_type(ctx.tcx, *impl_item); + let trait_type = util::item_type(ctx.tcx, *trait_item); + if !item_type.can_implement(trait_type) { ctx.error( ctx.def_span(impl_item), &format!( "Expected `{}` to be a {} as specified by the trait declaration", ctx.item_name(*impl_item), - util::item_type(ctx.tcx, *impl_item).to_str() + trait_type.to_str() ), ) .emit();