Error on `core::cmp::min` call

[jschneider-bensch]

The following causes eurydice to error out:

pub fn f(a: usize, b: usize) -> usize {
    a.min(b)
}

---

I ran it like so, perhaps I made a mistake here?

$ cd eurydice-mfe
$ RUSTFLAGS="--cfg eurydice" $CHARON_HOME/bin/charon
$ $EURYDICE_HOME/eurydice --log=* eurydice_mfe.llbc

The output I get is the following:

1/23
2/23
3/23
Visiting type: core::option::Option
enum core::option::Option<T>
  =
|  None()
|  Some(T)
4/23
Visiting type: core::cmp::Ordering
enum core::cmp::Ordering
  =
|  Less()
|  Equal()
|  Greater()
5/23
6/23
7/23
Visiting opaque function: core::cmp::impls::{(core::cmp::PartialEq<usize> for usize)#21}::eq
  opaque fn core::cmp::impls::{core::cmp::PartialEq<usize> for usize}#21::eq<0, 1>(&0 (usize), &1 (usize)) -> bool
--> args: &'0_0 (usize) ++ &'0_1 (usize), ret: bool
In this function, trait clause mapping is empty
8/23
Visiting opaque function: core::cmp::impls::{(core::cmp::PartialEq<usize> for usize)#21}::ne
  opaque fn core::cmp::impls::{core::cmp::PartialEq<usize> for usize}#21::ne<0, 1>(&0 (usize), &1 (usize)) -> bool
--> args: &'0_0 (usize) ++ &'0_1 (usize), ret: bool
In this function, trait clause mapping is empty
9/23
10/23
11/23
Visiting opaque function: core::cmp::impls::{(core::cmp::PartialOrd<usize> for usize)#58}::partial_cmp
  opaque fn core::cmp::impls::{core::cmp::PartialOrd<usize> for usize}#58::partial_cmp<0, 1>(&0 (usize), &1 (usize)) -> core::option::Option<core::cmp::Ordering>
--> args: &'0_0 (usize) ++ &'0_1 (usize), ret: core::option::Option<core::cmp::Ordering>
In this function, trait clause mapping is empty
12/23
Visiting opaque function: core::cmp::impls::{(core::cmp::PartialOrd<usize> for usize)#58}::lt
  opaque fn core::cmp::impls::{core::cmp::PartialOrd<usize> for usize}#58::lt<0, 1>(&0 (usize), &1 (usize)) -> bool
--> args: &'0_0 (usize) ++ &'0_1 (usize), ret: bool
In this function, trait clause mapping is empty
13/23
Visiting opaque function: core::cmp::impls::{(core::cmp::PartialOrd<usize> for usize)#58}::le
  opaque fn core::cmp::impls::{core::cmp::PartialOrd<usize> for usize}#58::le<0, 1>(&0 (usize), &1 (usize)) -> bool
--> args: &'0_0 (usize) ++ &'0_1 (usize), ret: bool
In this function, trait clause mapping is empty
14/23
Visiting opaque function: core::cmp::impls::{(core::cmp::PartialOrd<usize> for usize)#58}::ge
  opaque fn core::cmp::impls::{core::cmp::PartialOrd<usize> for usize}#58::ge<0, 1>(&0 (usize), &1 (usize)) -> bool
--> args: &'0_0 (usize) ++ &'0_1 (usize), ret: bool
In this function, trait clause mapping is empty
15/23
Visiting opaque function: core::cmp::impls::{(core::cmp::PartialOrd<usize> for usize)#58}::gt
  opaque fn core::cmp::impls::{core::cmp::PartialOrd<usize> for usize}#58::gt<0, 1>(&0 (usize), &1 (usize)) -> bool
--> args: &'0_0 (usize) ++ &'0_1 (usize), ret: bool
In this function, trait clause mapping is empty
16/23
17/23
Visiting opaque function: core::cmp::impls::{(core::cmp::Ord for usize)#59}::cmp
  opaque fn core::cmp::impls::{core::cmp::Ord for usize}#59::cmp<0, 1>(&0 (usize), &1 (usize)) -> core::cmp::Ordering
--> args: &'0_0 (usize) ++ &'0_1 (usize), ret: core::cmp::Ordering
In this function, trait clause mapping is empty
18/23
19/23
Visiting opaque function: core::cmp::Ord::min
  opaque fn core::cmp::Ord::min<Self>(Self, Self) -> Self
--> args: T@0 ++ T@0, ret: T@0
In this function, trait clause mapping is empty
20/23
Visiting function: eurydice_mfe::f
  fn eurydice_mfe::f(a^1 : usize, b^2 : usize) -> usize  
{
    v@0 : usize;
    a^1 : usize;
    b^2 : usize;
    v@3 : usize;
    v@4 : usize;

    v@3 := copy a^1;
    v@4 := copy b^2;
    v@0 := move core::cmp::impls::{core::cmp::Ord for usize}#59::min(move v@3, move v@4);
    drop v@4;
    drop v@3;
    return
  }
ty of locals: usize ++ usize ++ usize ++ usize ++ usize
ty of inputs: usize ++ usize
In this function, trait clause mapping is empty
type of binders: size_t, size_t
expression of place: { Expressions.var_id = 3; projection = [] }
expression of place: { Expressions.var_id = 1; projection = [] }
expression of place: { Expressions.var_id = 4; projection = [] }
expression of place: { Expressions.var_id = 2; projection = [] }
Visiting call: core::cmp::impls::{core::cmp::Ord for usize}#59::min
is_array_map: false
--> 0 type_args, 0 const_generics, 0 trait_refs
--> this is a trait method
--> 0 type_args, 0 const_generics, 0 trait_refs
--> trait_refs: 

--> pattern: core::cmp::Ord<usize>::min
--> type_args: 
Fatal error: exception Not_found

[msprotz]

Nice repro, thanks, I'll take a look

[msprotz]

Right so this is due to the fact that the body of definitions from core is not in scope. This ties in to AeneasVerif/charon#214 where we really need a language to specify what to extract, otherwise, extracting the entire universe is certain to trip Eurydice.

In the meanwhile, the only thing I can offer is for you to redefine your min trait locally.

Alternatively, I guess I could add a baked in definition but that's only if this is a major headache, as it would be hard to maintain going forward. Thanks.

[Nadrieril]

This is a mix of two issues: one is indeed AeneasVerif/charon#214 which is about to be fixed. The other is that impl core::cmp::Ord for usize does not override the default min() method of the trait Ord so we have nothing to translate even if we tried. This is tracked in AeneasVerif/charon#180.

[msprotz]

Thanks @Nadrieril . I wonder if we should have a list of baked in definitions at the charon level (or better, the hax-frontend level) so that we don't end up maintaining a set of "primitive" definitions that are hardcoded in abstract syntax in each of eurydice, aeneas, etc.

[Nadrieril]

It would indeed make sense for Charon to have a list of basic std functions that aren't marked opaque by default, if that's what you mean (in the context of this issue).