prusti-dev icon indicating copy to clipboard operation
prusti-dev copied to clipboard

Published 20 hours ago • verified publisher icon viperproject

Cannot use PartialOrd in specifications despite marking them as #[pure] using external spec feature

Open Ramla-I opened this issue 1 year ago • 3 comments

I'm trying to use the basic comparison operators for a type in my specifications, and following advice I found from other issues, I've marked the Ord and PartialOrd required methods as pure using the external spec feature. This still leads to a Prusti error: [Prusti: invalid specification] use of impure function "std::cmp::PartialOrd::ge" in pure code is not allowed

When I add the ge() method to my external spec and mark it as pure, I get an unexpected error. I'm wondering if I'm missing something when trying to use external spec for trait methods, or if this actually is an issue for now.

This is the code:

#[derive(PartialEq, Eq, Copy, Clone, PartialOrd, Ord)]
struct Frame {
    number: usize
}

#[extern_spec]
impl Ord for Frame {
    #[pure]
    fn cmp(&self, other: &Frame) -> core::cmp::Ordering;
}

#[extern_spec]
impl PartialOrd for Frame {
    #[pure]
    fn partial_cmp(&self, other: &Frame) -> Option<core::cmp::Ordering>;

    // #[pure]
    // fn ge(&self, other: &Self) -> bool;
}

impl Frame {
    #[ensures(result >= *a && result >= *b)]
    fn max(a: &Frame, b: &Frame) -> Frame {
        if a > b {
            *a
        } else {
            *b
        }
    }
}

This is the Prusti assistant output when I try to set the ge() method as pure:

Run verification on /home/ramla/Desktop/prusti_test_trait_purity/src/main.rs...
Preparing verification run #6.
Killing 0 processes.
Run command '/home/ramla/.config/Code/User/globalStorage/viper-admin.prusti-assistant/prustiTools/Latest/prusti/cargo-prusti --message-format=json'
Spawned PID: 22981
Output from '/home/ramla/.config/Code/User/globalStorage/viper-admin.prusti-assistant/prustiTools/Latest/prusti/cargo-prusti --message-format=json' (0.5s):
┌──── Begin stdout ────┐
{"reason":"compiler-artifact","package_id":"libc 0.2.147 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/libc-0.2.147/Cargo.toml","target":{"kind":["custom-build"],"crate_types":["bin"],"name":"build-script-build","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/libc-0.2.147/build.rs","edition":"2015","doc":false,"doctest":false,"test":false},"profile":{"opt_level":"0","debuginfo":null,"debug_assertions":true,"overflow_checks":true,"test":false},"features":[],"filenames":["/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/build/libc-1bba9bf9745c12fc/build-script-build"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"proc-macro2 1.0.66 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/proc-macro2-1.0.66/Cargo.toml","target":{"kind":["custom-build"],"crate_types":["bin"],"name":"build-script-build","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/proc-macro2-1.0.66/build.rs","edition":"2021","doc":false,"doctest":false,"test":false},"profile":{"opt_level":"0","debuginfo":null,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","proc-macro"],"filenames":["/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/build/proc-macro2-884f532ba632d096/build-script-build"],"executable":null,"fresh":true}
{"reason":"build-script-executed","package_id":"libc 0.2.147 (registry+https://github.com/rust-lang/crates.io-index)","linked_libs":[],"linked_paths":[],"cfgs":["freebsd11","libc_priv_mod_use","libc_union","libc_const_size_of","libc_align","libc_int128","libc_core_cvoid","libc_packedN","libc_cfg_target_vendor","libc_non_exhaustive","libc_long_array","libc_ptr_addr_of","libc_underscore_const_names","libc_const_extern_fn"],"env":[],"out_dir":"/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/build/libc-a9bc53cd384d4f74/out"}
{"reason":"compiler-artifact","package_id":"unicode-ident 1.0.11 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/unicode-ident-1.0.11/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"unicode-ident","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/unicode-ident-1.0.11/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":null,"debug_assertions":true,"overflow_checks":true,"test":false},"features":[],"filenames":["/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/libunicode_ident-813befa82c16f6ea.rlib","/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/libunicode_ident-813befa82c16f6ea.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"syn 1.0.109 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/syn-1.0.109/Cargo.toml","target":{"kind":["custom-build"],"crate_types":["bin"],"name":"build-script-build","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/syn-1.0.109/build.rs","edition":"2018","doc":false,"doctest":false,"test":false},"profile":{"opt_level":"0","debuginfo":null,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["clone-impls","default","derive","extra-traits","full","parsing","printing","proc-macro","quote","visit","visit-mut"],"filenames":["/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/build/syn-a91da4f44256a695/build-script-build"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"cfg-if 1.0.0 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/cfg-if-1.0.0/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"cfg-if","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/cfg-if-1.0.0/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":null,"debug_assertions":true,"overflow_checks":true,"test":false},"features":[],"filenames":["/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/libcfg_if-e51f42a584a012d8.rlib","/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/libcfg_if-e51f42a584a012d8.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"either 1.9.0 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/either-1.9.0/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"either","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/either-1.9.0/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":null,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["use_std"],"filenames":["/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/libeither-52acbece5203d46b.rlib","/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/libeither-52acbece5203d46b.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"rustc-hash 1.1.0 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/rustc-hash-1.1.0/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"rustc-hash","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/rustc-hash-1.1.0/src/lib.rs","edition":"2015","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":null,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","std"],"filenames":["/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/librustc_hash-988d62c3b13c8cfc.rlib","/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/librustc_hash-988d62c3b13c8cfc.rmeta"],"executable":null,"fresh":true}
{"reason":"build-script-executed","package_id":"proc-macro2 1.0.66 (registry+https://github.com/rust-lang/crates.io-index)","linked_libs":[],"linked_paths":[],"cfgs":["wrap_proc_macro","proc_macro_span"],"env":[],"out_dir":"/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/build/proc-macro2-edde9dcc03cb5007/out"}
{"reason":"compiler-artifact","package_id":"libc 0.2.147 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/libc-0.2.147/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"libc","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/libc-0.2.147/src/lib.rs","edition":"2015","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":null,"debug_assertions":true,"overflow_checks":true,"test":false},"features":[],"filenames":["/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/liblibc-0369cb00fbe7ea23.rlib","/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/liblibc-0369cb00fbe7ea23.rmeta"],"executable":null,"fresh":true}
{"reason":"build-script-executed","package_id":"syn 1.0.109 (registry+https://github.com/rust-lang/crates.io-index)","linked_libs":[],"linked_paths":[],"cfgs":[],"env":[],"out_dir":"/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/build/syn-2537434c1202bea7/out"}
{"reason":"compiler-artifact","package_id":"itertools 0.11.0 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/itertools-0.11.0/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"itertools","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/itertools-0.11.0/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":false},"profile":{"opt_level":"0","debuginfo":null,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","use_alloc","use_std"],"filenames":["/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/libitertools-2274e33e23a19fb5.rlib","/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/libitertools-2274e33e23a19fb5.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"proc-macro2 1.0.66 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/proc-macro2-1.0.66/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"proc-macro2","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/proc-macro2-1.0.66/src/lib.rs","edition":"2021","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":null,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","proc-macro"],"filenames":["/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/libproc_macro2-8b2d0be68bc2247f.rlib","/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/libproc_macro2-8b2d0be68bc2247f.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"getrandom 0.2.10 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/getrandom-0.2.10/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"getrandom","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/getrandom-0.2.10/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":null,"debug_assertions":true,"overflow_checks":true,"test":false},"features":[],"filenames":["/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/libgetrandom-443bc38aa7720c10.rlib","/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/libgetrandom-443bc38aa7720c10.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"quote 1.0.32 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/quote-1.0.32/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"quote","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/quote-1.0.32/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":null,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","proc-macro"],"filenames":["/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/libquote-deecc67d8e984fcb.rlib","/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/libquote-deecc67d8e984fcb.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"uuid 1.4.1 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/uuid-1.4.1/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"uuid","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/uuid-1.4.1/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":null,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","getrandom","rng","std","v4"],"filenames":["/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/libuuid-61e0b72238ee0d67.rlib","/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/libuuid-61e0b72238ee0d67.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"syn 1.0.109 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/syn-1.0.109/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"syn","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/syn-1.0.109/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":null,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["clone-impls","default","derive","extra-traits","full","parsing","printing","proc-macro","quote","visit","visit-mut"],"filenames":["/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/libsyn-fa84a753388845a1.rlib","/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/libsyn-fa84a753388845a1.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"prusti-specs 0.1.9 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/prusti-specs-0.1.9/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"prusti-specs","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/prusti-specs-0.1.9/src/lib.rs","edition":"2021","doc":true,"doctest":false,"test":true},"profile":{"opt_level":"0","debuginfo":null,"debug_assertions":true,"overflow_checks":true,"test":false},"features":[],"filenames":["/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/libprusti_specs-06d8df31967b48e7.rlib","/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/libprusti_specs-06d8df31967b48e7.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"prusti-contracts-proc-macros 0.1.9 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/prusti-contracts-proc-macros-0.1.9/Cargo.toml","target":{"kind":["proc-macro"],"crate_types":["proc-macro"],"name":"prusti-contracts-proc-macros","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/prusti-contracts-proc-macros-0.1.9/src/lib.rs","edition":"2021","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":null,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["prusti"],"filenames":["/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/libprusti_contracts_proc_macros-b4ab3b3ae82eed94.so"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"prusti-contracts 0.1.4 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/prusti-contracts-0.1.4/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"prusti-contracts","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/prusti-contracts-0.1.4/src/lib.rs","edition":"2021","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["prusti"],"filenames":["/home/ramla/Desktop/prusti_test_trait_purity/target/verify/debug/deps/libprusti_contracts-734cb4485d0b5aac.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-message","package_id":"prusti_test_trait_purity 0.1.0 (path+file:///home/ramla/Desktop/prusti_test_trait_purity)","manifest_path":"/home/ramla/Desktop/prusti_test_trait_purity/Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"prusti_test_trait_purity","src_path":"/home/ramla/Desktop/prusti_test_trait_purity/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"warning: unused `#[macro_use]` import\n --> src/main.rs:1:1\n  |\n1 | #[macro_use] extern crate prusti_contracts;\n  | ^^^^^^^^^^^^\n  |\n  = note: `#[warn(unused_imports)]` on by default\n\n","children":[{"children":[],"code":null,"level":"note","message":"`#[warn(unused_imports)]` on by default","rendered":null,"spans":[]}],"code":{"code":"unused_imports","explanation":null},"level":"warning","message":"unused `#[macro_use]` import","spans":[{"byte_end":12,"byte_start":0,"column_end":13,"column_start":1,"expansion":null,"file_name":"src/main.rs","is_primary":true,"label":null,"line_end":1,"line_start":1,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":13,"highlight_start":1,"text":"#[macro_use] extern crate prusti_contracts;"}]}]}}
{"reason":"compiler-message","package_id":"prusti_test_trait_purity 0.1.0 (path+file:///home/ramla/Desktop/prusti_test_trait_purity)","manifest_path":"/home/ramla/Desktop/prusti_test_trait_purity/Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"prusti_test_trait_purity","src_path":"/home/ramla/Desktop/prusti_test_trait_purity/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"warning: associated function `max` is never used\n  --> src/main.rs:30:8\n   |\n30 |     fn max(a: Frame, b: Frame) -> Frame {\n   |        ^^^\n   |\n   = note: `#[warn(dead_code)]` on by default\n\n","children":[{"children":[],"code":null,"level":"note","message":"`#[warn(dead_code)]` on by default","rendered":null,"spans":[]}],"code":{"code":"dead_code","explanation":null},"level":"warning","message":"associated function `max` is never used","spans":[{"byte_end":535,"byte_start":532,"column_end":11,"column_start":8,"expansion":null,"file_name":"src/main.rs","is_primary":true,"label":null,"line_end":30,"line_start":30,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":11,"highlight_start":8,"text":"    fn max(a: Frame, b: Frame) -> Frame {"}]}]}}
{"reason":"compiler-message","package_id":"prusti_test_trait_purity 0.1.0 (path+file:///home/ramla/Desktop/prusti_test_trait_purity)","manifest_path":"/home/ramla/Desktop/prusti_test_trait_purity/Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"prusti_test_trait_purity","src_path":"/home/ramla/Desktop/prusti_test_trait_purity/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"warning: 2 warnings emitted\n\n","children":[],"code":null,"level":"warning","message":"2 warnings emitted","spans":[]}}
{"reason":"build-finished","success":false}

└──── End stdout ──────┘
┌──── Begin stderr ────┐
    Checking prusti_test_trait_purity v0.1.0 (/home/ramla/Desktop/prusti_test_trait_purity)
thread 'rustc' panicked at 'internal error: entered unreachable code', prusti-interface/src/environment/query.rs:313:21
stack backtrace:
   0: rust_begin_unwind
             at /rustc/5e1d3299a290026b85787bc9c7e72bcc53ac283f/library/std/src/panicking.rs:577:5
   1: core::panicking::panic_fmt
             at /rustc/5e1d3299a290026b85787bc9c7e72bcc53ac283f/library/core/src/panicking.rs:67:14
   2: core::panicking::panic
             at /rustc/5e1d3299a290026b85787bc9c7e72bcc53ac283f/library/core/src/panicking.rs:117:5
   3: prusti_interface::environment::query::EnvQuery::find_impl_of_trait_method_call
   4: prusti_interface::specs::external::ExternSpecDeclaration::from_method_call
   5: prusti_interface::specs::external::ExternSpecResolver::add_extern_fn
   6: <prusti_interface::specs::SpecCollector as rustc_hir::intravisit::Visitor>::visit_fn
   7: rustc_hir::intravisit::walk_impl_item
   8: rustc_hir::intravisit::Visitor::visit_impl_item
   9: rustc_hir::intravisit::Visitor::visit_nested_impl_item
  10: rustc_hir::intravisit::walk_impl_item_ref
  11: rustc_hir::intravisit::Visitor::visit_impl_item_ref
  12: rustc_hir::intravisit::walk_item
  13: rustc_hir::intravisit::Visitor::visit_item
  14: rustc_hir::intravisit::Visitor::visit_nested_item
  15: rustc_hir::intravisit::walk_mod
  16: rustc_hir::intravisit::Visitor::visit_mod
  17: rustc_middle::hir::map::Map::walk_toplevel_module
  18: prusti_interface::specs::SpecCollector::collect_specs
  19: <prusti_driver::callbacks::PrustiCompilerCalls as rustc_driver_impl::Callbacks>::after_analysis::{{closure}}
  20: rustc_middle::ty::context::GlobalCtxt::enter::{{closure}}
  21: rustc_middle::ty::context::tls::enter_context::{{closure}}
  22: std::thread::local::LocalKey<T>::try_with
  23: std::thread::local::LocalKey<T>::with
  24: rustc_middle::ty::context::GlobalCtxt::enter
  25: rustc_interface::queries::QueryResult<&rustc_middle::ty::context::GlobalCtxt>::enter
  26: <prusti_driver::callbacks::PrustiCompilerCalls as rustc_driver_impl::Callbacks>::after_analysis
  27: <rustc_interface::interface::Compiler>::enter::<rustc_driver_impl::run_compiler::{closure#1}::{closure#2}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_span::ErrorGuaranteed>>
  28: rustc_span::set_source_map::<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_interface::interface::run_compiler<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_driver_impl::run_compiler::{closure#1}>::{closure#0}::{closure#0}>
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

error: internal compiler error: unexpected panic

note: Prusti or the compiler unexpectedly panicked. This is a bug.

note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new

note: Prusti version: 0.2.2, commit 2c2145c 2023-06-30 08:49:14 UTC, built on 2023-06-30 09:00:22 UTC

query stack during panic:
end of query stack
error: could not compile `prusti_test_trait_purity` (bin "prusti_test_trait_purity"); 3 warnings emitted

└──── End stderr ──────┘
Exit code 101, signal null.
Ignored diagnostic message: '2 warnings emitted'
Prusti encountered an unexpected error.
Prusti encountered an unexpected error. If the issue persists, please open a [bug report](https://github.com/viperproject/prusti-dev/issues/new). See [the logs](command:prusti-assistant.openLogs) for more details.
Rendering 2 diagnostics at file:///home/ramla/Desktop/prusti_test_trait_purity/src/main.rs

Ramla-I avatar Aug 09 '23 15:08 Ramla-I

Thank you for the bug report. The panic is due to an unreachable!() in find_impl_of_trait_method_call: https://github.com/viperproject/prusti-dev/blob/863cd59705a43863eaba75c0dad1f4521de05aff/prusti-interface/src/environment/query.rs#L273-L320

In other words, Prusti fails to find the method that implements the declared #[pure] fn ge(..) -> ..;. I suspect that this is because #[extern_spec] is usually used to attach specifications to items defined in external crates, while the #[derive(PartialOrd)] is actually in the current crate (@Aurel300 is this correct?).

As a workaround, I'd try to define and use in the specifications a method like

impl Frame {
    #[pure]
    #[trusted]
    #[ensures(result == (self.number >= other.number))] // i.e. the implementation of `#[derive(PartialOrd)]`
    pub fn ge(&self, other: &Self) -> bool { *self >= *other }
}

fpoli avatar Aug 10 '23 07:08 fpoli

Sorry for the delay in responding! There is no core limitation here, just various bits and pieces that are not done "yet". I'll start with providing the modified file that does verify, then comment on some parts of it:

use prusti_contracts::*;

#[derive(PartialEq, Eq, Copy, Clone, PartialOrd, Ord)]
struct Frame {
    number: usize
}

// (1)
#[extern_spec]
trait PartialOrd<Rhs> {
    #[pure]
    fn partial_cmp(&self, other: &Rhs) -> Option<core::cmp::Ordering>;

    #[pure]
    #[ensures(result == matches!(self.partial_cmp(other), Some(core::cmp::Ordering::Greater)))]
    fn gt(&self, other: &Rhs) -> bool;

    #[pure]
    #[ensures(result == matches!(self.partial_cmp(other), Some(core::cmp::Ordering::Greater | core::cmp::Ordering::Equal)))]
    fn ge(&self, other: &Rhs) -> bool;
}

#[extern_spec]
impl PartialOrd<usize> for usize {
    #[pure]
    #[ensures(if *self > *other {
        result === Some(core::cmp::Ordering::Greater)
    } else if *self < *other {
        result === Some(core::cmp::Ordering::Less)
    } else {
        result === Some(core::cmp::Ordering::Equal)
    })]
    fn partial_cmp(&self, other: &usize) -> Option<core::cmp::Ordering>;
}

// (2)
#[extern_spec]
impl PartialOrd for Frame {
    #[pure]
    #[ensures(result == self.number.partial_cmp(&other.number))]
    fn partial_cmp(&self, other: &Frame) -> Option<core::cmp::Ordering>;
}

impl Frame {
    #[ensures(result >= *a && result >= *b)]
    fn max(a: &Frame, b: &Frame) -> Frame {
        assert!(matches!( // (4)
            a.partial_cmp(a),
            Some(core::cmp::Ordering::Greater | core::cmp::Ordering::Equal)
        ));
        if *a > *b { // (3)
            *a
        } else {
            *b
        }
    }
}

#[trusted]
fn main() {}

(1) First, there is a couple of extern_specs for trait PartialOrd and the implementation of that trait by usize. These specs belong to prusti-contracts and will hopefully be added to Prusti with #1249, which I've been working on recently (again). Note that the lt and le methods should also be specified, but are not needed for this program.

(2) Next, the extern_spec for the Frame implementation of PartialOrd. Some things to note:

  • partial_cmp needs a postcondition. This is because an extern_spec implies the specification is trusted. In general, it is not actually a problem if you extern_spec methods which are implemented in the local crate, but this is something to keep in mind. Because the method is considered trusted, the implementation coming from the derive(PartialOrd) is ignored, and we must repeat it in a postcondition.
  • gt/ge/... are not specified. This is what was causing the crash in your original program. The problem is that an extern_spec should always correspond to a method that actually exists. This is an extern_spec for impl PartialOrd for Frame: there is no gt method in it, because derive(PartialOrd) only generates a partial_cmp implementation. gt etc are provided by the trait as default methods.

(3) Skipping the assert! for now, the condition was changed to *a > *b instead of a > b. The reason is that the latter would actually call a different method, using the implementation of PartialOrd in &Frame instead of Frame. In Rust you can typically ignore the distinction, because of the blanket implementation impl<A: PartialOrd<B>, B> PartialOrd<&B> for &A. Nevertheless, this is a separate method that needs its own specification. In #1249 we will also provide specifications for such blanket implementations. We already have some cases of this for some arithmetic binary operators, e.g. forwarding i32 addition to &i32 here.

(4) Finally, once Prusti is happy with purity, specs, etc, the max implementation still does not pass. Debugging a bit we can find that assert!(*a >= *a); (needed for the first conjunct of the postcondition) does not hold in the first branch. IIUC, adding this assertion forces the partial_cmp function to be unfolded, thus showing the required property.

Aurel300 avatar Sep 11 '23 17:09 Aurel300

Thanks @Aurel300, the explanation was very helpful. The example verifies for me too.

Ramla-I avatar Sep 11 '23 21:09 Ramla-I