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).

[msprotz]

@Nadrieril any chance of being able to allow-list a set of useful functions from std that we would like to extract via charon? I'm bumping into min-related issues again. Thanks.

[Nadrieril]

There are three issues at play here as far as I can tell:

1. The fact that an impl Ord for X does not generally give us access to the corresponding min() impl; that's Translate defaulted trait methods implementations charon#180.
2. The fact that even if we had this min() impl, it would be opaque so we'd have to pass --include std::cmp::{impl Ord for _} to charon a lot if you want its body.
3. The fact that you often want to replace such methods with your own version in Eurydice, and you'd want this to be made more convenient than using the name matcher.

1 is on my list but is not easy so I haven't made much progress lately. I'll get back to it, @sonmarcho has been requesting it too. 2. seems reasonable to improve but we'd have to discuss what the exact goal is. 3. I'm mildly opposed to, that's what the name matcher is for.

[msprotz]

I'm actually using the name matcher for this and it's totally fine, no? This: https://github.com/AeneasVerif/eurydice/blob/main/lib/AstOfLlbc.ml#L182 maintains a mapping from trait impls / functions / etc. to builtin versions.

[msprotz]

So my comment is, yes, I do care about 1. and 2. but I think I don't care so much about 3. (unless I misunderstood)

[Nadrieril]

Ok perfect, we're aligned then :) Next step is provided methods then