Java binding type failure when trying to add specifications to `PartialOrd::partial_cmp`

[paaassscccaaalll]

The Problem

When adding these postconditions to fn partial_cmp() I get a Java binding type failure.

#[ensures(matches!(result, Some(core::cmp::Ordering::Less)) ==> other.partial_cmp(self) === Some(core::cmp::Ordering::Greater))]
#[ensures(matches!(result, Some(core::cmp::Ordering::Greater)) ==> other.partial_cmp(self) === Some(core::cmp::Ordering::Less))]
#[ensures(matches!(result, Some(core::cmp::Ordering::Equal)) ==> other.partial_cmp(self) === Some(core::cmp::Ordering::Equal))]
#[ensures(result === None ==> other.partial_cmp(self) === None)]

The Backtrace

Verification of 2 items...
thread 'rustc' panicked at viper-sys/src/../gen/scala/Some_wrapper.rs:53:5:
Java binding type failure. Expected object of class scala/Some, but got scala/None$ instead
stack backtrace:
   0:     0x7ad4c0b96aaa - <std::sys::backtrace::BacktraceLock::print::DisplayBacktrace as core::fmt::Display>::fmt::h57c8c3925ce49724
   1:     0x7ad4c1413d26 - core::fmt::write::hd591db34e8fefc49
   2:     0x7ad4c24132d1 - std::io::Write::write_fmt::hafb13061963e9b6c
   3:     0x7ad4c0b96902 - std::sys::backtrace::BacktraceLock::print::hd6817bcf0b2f34da
   4:     0x7ad4c0b98dfa - std::panicking::default_hook::{{closure}}::h63ea7ef0f18efe7e
   5:     0x7ad4c0b98c43 - std::panicking::default_hook::h2cff96b5f1f11a61
   6:     0x7ad4bfcf0138 - std[1b8edffc354b3989]::panicking::update_hook::<alloc[b79a629e2207f6f2]::boxed::Box<rustc_driver_impl[9fa7216c7b2fdf15]::install_ice_hook::{closure#0}>>::{closure#0}
   7:     0x7ad4c0b995b8 - std::panicking::rust_panic_with_hook::h7fa9a8f224b9d5b8
   8:     0x7ad4c0b992aa - std::panicking::begin_panic_handler::{{closure}}::h3d3287d2b656a3fc
   9:     0x7ad4c0b96f59 - std::sys::backtrace::__rust_end_short_backtrace::hc4e874dc2f50ca08
  10:     0x7ad4c0b98f6d - rust_begin_unwind
  11:     0x7ad4bd7cde00 - core::panicking::panic_fmt::hac5ac125fcb13ef7
  12:     0x55be8d406222 - viper_sys::wrappers::scala::Some_wrapper::Some::call_get::he0398fd987792f24
                               at /home/saentis/repos/prusti-dev/viper-sys/src/../gen/scala/Some_wrapper.rs:53:5
  13:     0x55be8d2a5062 - viper::verifier::Verifier::verify::{{closure}}::h84c2c56864fcdaaa
                               at /home/saentis/repos/prusti-dev/viper/src/verifier.rs:237:59
  14:     0x55be8d2d96cc - viper::ast_utils::AstUtils::with_local_frame::h8e1f8f54df9b70c5
                               at /home/saentis/repos/prusti-dev/viper/src/ast_utils.rs:58:22
  15:     0x55be8d2d8bc9 - viper::verifier::Verifier::verify::h1f43f6a3e5f42ccf
                               at /home/saentis/repos/prusti-dev/viper/src/verifier.rs:188:9
  16:     0x55be8cc9060d - prusti_server::backend::Backend::verify::{{closure}}::hb32e1054c12f80f0
                               at /home/saentis/repos/prusti-dev/prusti-server/src/backend.rs:36:21
  17:     0x55be8cc904bd - viper::ast_utils::AstUtils::with_local_frame::h3890999bd45230b2
                               at /home/saentis/repos/prusti-dev/viper/src/ast_utils.rs:58:22
  18:     0x55be8cc903b9 - prusti_server::backend::Backend::verify::h793ce5d6d07295b2
                               at /home/saentis/repos/prusti-dev/prusti-server/src/backend.rs:18:17
  19:     0x55be8cc8dd40 - prusti_server::process_verification::process_verification_request::ha33d0379e84416d2
                               at /home/saentis/repos/prusti-dev/prusti-server/src/process_verification.rs:119:18
  20:     0x55be8cd55ba9 - prusti_server::verify_programs::{{closure}}::hff76c2968bfae845
                               at /home/saentis/repos/prusti-dev/prusti-server/src/lib.rs:82:30
  21:     0x55be8cdd89bb - core::iter::adapters::map::map_fold::{{closure}}::h38b3200f479ecb16
                               at /home/saentis/.rustup/toolchains/nightly-2024-12-15-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/map.rs:88:28
  22:     0x55be8cdd8bb6 - core::iter::adapters::map::map_fold::{{closure}}::ha233ecadccf62392
                               at /home/saentis/.rustup/toolchains/nightly-2024-12-15-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/map.rs:88:21
  23:     0x55be8cc9f24b - <alloc::vec::into_iter::IntoIter<T,A> as core::iter::traits::iterator::Iterator>::fold::h0301882458619006
                               at /home/saentis/.rustup/toolchains/nightly-2024-12-15-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/into_iter.rs:318:25
  24:     0x55be8cdd33e3 - <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::fold::h559e794fe4b0d907
                               at /home/saentis/.rustup/toolchains/nightly-2024-12-15-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/map.rs:128:9
  25:     0x55be8cdd34c0 - <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::fold::h9756674444405816
                               at /home/saentis/.rustup/toolchains/nightly-2024-12-15-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/map.rs:128:9
  26:     0x55be8cdd4776 - core::iter::traits::iterator::Iterator::for_each::hbf50602254b9a307
                               at /home/saentis/.rustup/toolchains/nightly-2024-12-15-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/traits/iterator.rs:800:9
  27:     0x55be8cd999c6 - alloc::vec::Vec<T,A>::extend_trusted::h2edc631ec5ed9dd8
                               at /home/saentis/.rustup/toolchains/nightly-2024-12-15-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/mod.rs:3556:17
  28:     0x55be8cd9e4e7 - <alloc::vec::Vec<T,A> as alloc::vec::spec_extend::SpecExtend<T,I>>::spec_extend::ha3d4a5e8d6f4b621
                               at /home/saentis/.rustup/toolchains/nightly-2024-12-15-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/spec_extend.rs:29:9
  29:     0x55be8cd98da0 - <alloc::vec::Vec<T> as alloc::vec::spec_from_iter_nested::SpecFromIterNested<T,I>>::from_iter::h16e656a7d4452b3b
                               at /home/saentis/.rustup/toolchains/nightly-2024-12-15-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/spec_from_iter_nested.rs:62:9
  30:     0x55be8cd6e3e5 - <alloc::vec::Vec<T> as alloc::vec::spec_from_iter_nested::SpecFromIterNested<T,I>>::from_iter{{reify.shim}}::hdac8a50c979005c8
                               at /home/saentis/.rustup/toolchains/nightly-2024-12-15-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/spec_from_iter_nested.rs:52:5
  31:     0x55be8cd9b52e - alloc::vec::in_place_collect::<impl alloc::vec::spec_from_iter::SpecFromIter<T,I> for alloc::vec::Vec<T>>::from_iter::hae9b7fbdbba5252c
                               at /home/saentis/.rustup/toolchains/nightly-2024-12-15-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/in_place_collect.rs:246:9
  32:     0x55be8cd9d8b1 - <alloc::vec::Vec<T> as core::iter::traits::collect::FromIterator<T>>::from_iter::h50cb92f3b4b01af2
                               at /home/saentis/.rustup/toolchains/nightly-2024-12-15-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/mod.rs:3415:9
  33:     0x55be8cdd4585 - core::iter::traits::iterator::Iterator::collect::hbe6c62bb5c71f6ec
                               at /home/saentis/.rustup/toolchains/nightly-2024-12-15-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/traits/iterator.rs:1971:9
  34:     0x55be8cb8b2ca - prusti_server::verify_programs::hb4af89715840df22
                               at /home/saentis/repos/prusti-dev/prusti-server/src/lib.rs:80:9
  35:     0x55be8cb54393 - prusti_driver::verifier::verify::ha3abcab32e7dfd3f
                               at /home/saentis/repos/prusti-dev/prusti/src/verifier.rs:47:27
  36:     0x55be8cb630cb - <prusti_driver::callbacks::PrustiCompilerCalls as rustc_driver_impl::Callbacks>::after_analysis::h1d38e7f512e368bc
                               at /home/saentis/repos/prusti-dev/prusti/src/callbacks.rs:162:13
  37:     0x7ad4c24a3cc2 - rustc_interface[685a71190dde8c4]::interface::run_compiler::<(), rustc_driver_impl[9fa7216c7b2fdf15]::run_compiler::{closure#0}>::{closure#1}
  38:     0x7ad4c232ca11 - std[1b8edffc354b3989]::sys::backtrace::__rust_begin_short_backtrace::<rustc_interface[685a71190dde8c4]::util::run_in_thread_with_globals<rustc_interface[685a71190dde8c4]::util::run_in_thread_pool_with_globals<rustc_interface[685a71190dde8c4]::interface::run_compiler<(), rustc_driver_impl[9fa7216c7b2fdf15]::run_compiler::{closure#0}>::{closure#1}, ()>::{closure#0}, ()>::{closure#0}::{closure#0}, ()>
  39:     0x7ad4c232d448 - <<std[1b8edffc354b3989]::thread::Builder>::spawn_unchecked_<rustc_interface[685a71190dde8c4]::util::run_in_thread_with_globals<rustc_interface[685a71190dde8c4]::util::run_in_thread_pool_with_globals<rustc_interface[685a71190dde8c4]::interface::run_compiler<(), rustc_driver_impl[9fa7216c7b2fdf15]::run_compiler::{closure#0}>::{closure#1}, ()>::{closure#0}, ()>::{closure#0}::{closure#0}, ()>::{closure#1} as core[83eb7458e699dd0c]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  40:     0x7ad4c232ea01 - std::sys::pal::unix::thread::Thread::new::thread_start::hcf95b8a74a5f5cfe
  41:     0x7ad4bac9caa4 - <unknown>
  42:     0x7ad4bad29c3c - <unknown>
  43:                0x0 - <unknown>

error: the compiler unexpectedly panicked. this is a bug.

The File

use prusti_contracts::*;
use std::cmp::{PartialOrd, Ordering};

#[extern_spec]
trait PartialEq<Rhs>
where
    Rhs: ?Sized,
{
    #[pure]
    fn eq(&self, other: &Rhs) -> bool;

    #[pure]
    fn ne(&self, other: &Rhs) -> bool;
}

#[extern_spec]
trait PartialOrd<Rhs>: PartialEq<Rhs>
where
    Rhs: PartialOrd<Self>,
{
    #[pure]
    #[ensures(matches!(result, Some(core::cmp::Ordering::Less)) ==> other.partial_cmp(self) === Some(core::cmp::Ordering::Greater))]
    #[ensures(matches!(result, Some(core::cmp::Ordering::Greater)) ==> other.partial_cmp(self) === Some(core::cmp::Ordering::Less))]
    #[ensures(matches!(result, Some(core::cmp::Ordering::Equal)) ==> other.partial_cmp(self) === Some(core::cmp::Ordering::Equal))]
    #[ensures(result === None ==> other.partial_cmp(self) === None)]
    fn partial_cmp(&self, other: &Rhs) -> Option<Ordering>;

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

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

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

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


#[pure]
#[requires(min <= max)]
#[ensures(result >= min && result <= max)]
fn generic_clamp<T>(value: T, min: T, max: T) -> T
where
    T: PartialOrd,
{
    if value < min {
        min
    } else if value > max {
        max
    } else {
        value
    }
}

#[trusted]
fn main() {
    let value = 5;
    let min = 1;
    let max = 10;
    let clamped_value = generic_clamp(value, min, max);
}

The run command

I ran it using this command:

./x.py build && \
    PRUSTI_DUMP_DEBUG_INFO=true PRUSTI_CHECK_OVERFLOWS=false PRUSTI_PRINT_DESUGARED_SPECS=true PRUSTI_DUMP_VIPER_PROGRAM=true \
    ./x.py run  --bin prusti-rustc --features=vir_debug -- --edition=2021 <FILE_PATH>

Prusti Version:

I worked with 44140025235731f4fe0fecbfc013df50772b55bf on the rewrite-2023 branch.

One thing which I needed to change to even get that far is adding a continue; in prusti-dev/prusti-encoder/src/encoders/impure/fn_wand.rs:380 here

  for pred in rbp {
                let GenericKind::Param(b) = pred.0 else {
                    todo!("region bound pair: {pred:?}");
                };
                let ty::RegionKind::ReEarlyParam(a) = pred.1.kind() else {
                    continue; // added this
                    todo!("region bound pair: {pred:?}");
                };
                insert_edge(IndirectKey::Early(a), IndirectKey::Param(b));
            }

Viper Version

I am using this Viper package on my WSL.

https://github.com/viperproject/viper-ide/releases/download/v-2025-02-04-1042/ViperToolsLinux.zip

Java Version

openjdk 21.0.7 2025-04-15
OpenJDK Runtime Environment (build 21.0.7+6-Ubuntu-0ubuntu124.04)
OpenJDK 64-Bit Server VM (build 21.0.7+6-Ubuntu-0ubuntu124.04, mixed mode, sharing)