Creusot rejects these generic definitions with trait constraints

[Lysxia]

These are definitions which compile with plain rustc, but not creusot:

use creusot_contracts::*;
pub fn min<O: PartialOrd>(a: O, b: O) -> O {
    if a < b {
        a
    } else {
        b
    }
}

Error message:

error[E0277]: the trait bound `O: creusot_contracts::DeepModel` is not satisfied
  --> src/lib.rs:11:8
   |
11 |     if a < b {
   |        ^^^^^ the trait `creusot_contracts::DeepModel` is not implemented for `O`

error[E0277]: the trait bound `<O as creusot_contracts::DeepModel>::DeepModelTy: creusot_contracts::OrdLogic` is not satisfied
  --> src/lib.rs:11:8
   |
11 |     if a < b {
   |        ^^^^^ the trait `creusot_contracts::OrdLogic` is not implemented for `<O as creusot_contracts::DeepModel>::DeepModelTy`

---

use creusot_contracts::*;
pub fn f<I: Iterator>(i: &mut I) {
    for _ in i {}
}

(Adding a #[invariant(true)] doesn't help)

Error message:

error[E0277]: the trait bound `<&mut I as std::iter::IntoIterator>::IntoIter: creusot_contracts::Iterator` is not satisfied
  --> src/lib.rs:12:14
   |
12 |     for _ in i {}
   |              ^ the trait `creusot_contracts::Iterator` is not implemented for `<&mut I as std::iter::IntoIterator>::IntoIter`

error[E0277]: the trait bound `&mut I: creusot_contracts::IntoIterator` is not satisfied
  --> src/lib.rs:12:14
   |
12 |     for _ in i {}
   |              ^ the trait `creusot_contracts::Iterator` is not implemented for `&mut I`, which is required by `&mut I: creusot_contracts::IntoIterator`
   |
   = help: the following other types implement trait `creusot_contracts::Iterator`:
             creusot_contracts::std::iter::MapInv<I, <I as std::iter::Iterator>::Item, F>
             std::collections::vec_deque::Iter<'a, T>
             std::iter::Cloned<I>
             std::iter::Copied<I>
             std::iter::Empty<T>
             std::iter::Enumerate<I>
             std::iter::Filter<I, F>
             std::iter::Fuse<I>
           and 14 others
   = note: required for `&mut I` to implement `creusot_contracts::IntoIterator`

error[E0277]: the trait bound `&mut I: creusot_contracts::Iterator` is not satisfied
  --> src/lib.rs:12:14
   |
12 |     for _ in i {}
   |              ^ the trait `creusot_contracts::Iterator` is not implemented for `&mut I`
   |
   = help: the following other types implement trait `creusot_contracts::Iterator`:
             creusot_contracts::std::iter::MapInv<I, <I as std::iter::Iterator>::Item, F>
             std::collections::vec_deque::Iter<'a, T>
             std::iter::Cloned<I>
             std::iter::Copied<I>
             std::iter::Empty<T>
             std::iter::Enumerate<I>
             std::iter::Filter<I, F>
             std::iter::Fuse<I>
           and 14 others

[Lysxia]

I'm trying to define traits that gather the necessary constraints, e.g.,

// Extends std::PartialOrd with additional constraints for translation
trait MyPartialOrd where
    Self: PartialOrd + DeepModel,
    <Self as DeepModel>::DeepModelTy: OrdLogic {
}

However the constraint on the associated type doesn't seem to work

pub fn min<O: MyPartialOrd>(a: O, b: O) -> O {
    if a < b {
        a
    } else {
        b
    }
}

error[E0277]: the trait bound `<O as creusot_contracts::DeepModel>::DeepModelTy: creusot_contracts::OrdLogic` is not satisfied
  --> src/lib.rs:33:8
   |
33 |     if a < b {
   |        ^^^^^ the trait `creusot_contracts::OrdLogic` is not implemented for `<O as creusot_contracts::DeepModel>::DeepModelTy`

thread 'rustc' panicked at creusot/src/translation/pearlite/normalize.rs:35:29:
could not resolve trait instance (DefId(20:4549 ~ creusot_contracts[1d45]::logic::ord::OrdLogic::lt_log), [Alias(Projection, AliasTy { args: [O/#0], def_id: DefId(20:848 ~ creusot_contracts[1d45]::model::DeepModel::DeepModelTy) })])

---

UPDATE: found a variant that works

trait MyOrd
where
    Self: Ord + DeepModel<DeepModelTy: OrdLogic>,
    {}

pub fn min<A: MyOrd>(x: A) {
}

The previous variant seems to rely on an unimplemented feature of trait resolution.

• There is a general workaround in the crate imply_hack (from last week!), which, for specific traits, specializes to something like my example just above

• I found it in this comment https://github.com/rust-lang/rust/issues/44491#issuecomment-2496196742

• which I stumbled upon by random walk through several links related to this missing feature:

  • https://stackoverflow.com/questions/77943027/rust-associated-type-bounds-on-supertrait-from-subtrait
  • https://github.com/rust-lang/rfcs/blob/master/text/2089-implied-bounds.md

[xldenis]

I think the issue here is that extern_spec is not doing its job, it should be re-inforcing the trait bounds when you compile with creusot.

[Lysxia]

How does it do that? the only way I can think of is to somehow shadow traits from std but I don't see where that is happening (which is why I was trying to do it manually)?

[xldenis]

we have extern_spec declarations for traits which are meant to then inject the bounds automatically via ParamEnv in creusot. That second part has always been sort of buggy though.

[jhjourdan]

I think the issue here is that extern_spec is not doing its job, it should be re-inforcing the trait bounds when you compile with creusot.

I think it does that, but this fails, because it cannot find the bound because of rust-lang/rust#44491.

[jhjourdan]

trait MyOrd
where
    Self: Ord + DeepModel<DeepModelTy: OrdLogic>,
    {}

Cannot this be written:

trait MyOrd: Ord + DeepModel<DeepModelTy: OrdLogic>,
    {}