subtrait mischief: subtrait Copy not available on type constrained to supertrait

[jonhnet]

In the enclosed recording, we get this error:

error: the trait bound `A1_T: std::marker::Copy` is not satisfied
   --> src/marshalling/IntegerMarshalling_v.rs:385:1
    |
385 | /
386 | | //         proof { T::as_int_ensures(); }
    | |___^

The first weird thing is that the spans are broken. The actual offending line, 384, says T::test_have_a_t(). That is a trait method defined at line 38 in the trait IntFormattable; notably, IntFormattable has Copy as a subtrait. Line 384 lives inside an impl block declared on line 303 as:

impl<T: IntFormattable /* + Copy */ > Marshal for IntFormat<T>

So T should definitely be Copy, by virtue of being IntFormattable.

@jaybosamiya suggested adding the + Copy on line 303 (commented out in this recording), which indeed makes the error message disappear.

I tried minimizing, but was unable to reproduce the behavior in a smaller form.

2024-06-05-14-26-37.zip

[jaybosamiya]

Minimized to ~8% of the above size, while triggering the same issue: 2024-06-05-17-44-02.zip

$ verus foo.rs
error: the trait bound `A1_T: std::marker::Copy` is not satisfied
  --> foo.rs:63:1
   |
63 |     }
   | ^^^^

error: aborting due to 1 previous error

note: This error was found in Verus pass: ownership checking of tracked code

error: aborting due to 2 previous errors

Minimization steps:

1. Run inline-crate on the above code (minor change needed to actually get it to run without erroring: move marshal.rs to marshal/mod.rs), to produce a single file foo.rs that triggers the issue.
2. Write an interestingness test (see below for my script that implements this): interesting.sh.
3. Run creduce --n 16 ./interesting.sh ./foo.rs to get auto-minimized version of the code.
4. Run verusfmt foo.rs to make it more readable.

Minimizer script (click to expand)

```sh #! /bin/bash # Confirm that there is a `/* + Copy */` in the code if grep -F '/* + Copy */' foo.rs >/dev/null; then true else echo "Uninteresting: no Copy comment" exit 1 fi # Run with verus, checking if we see a complaint timeout 10 verus foo.rs >/dev/null 2>stderr || true if grep 'std::marker::Copy` is not satisfied' stderr >/dev/null; then true else echo "Uninteresting: no copy unsatisfied" exit 1 fi # Copy over the file to bar.rs, enabling the Copy comment sed 's|/\* + Copy \*/| \+ Copy |g' foo.rs > bar.rs # Run with verus, checking if we see a complaint timeout 10 verus bar.rs >/dev/null 2>stderr || true if grep 'std::marker::Copy` is not satisfied' stderr >/dev/null; then echo "Uninteresting: complaint still remains" exit 1 else echo "Interesting!" exit 0 fi ```

[jaybosamiya]

Hopefully the above docs help with automatic minimization in the future for non-trivial cases such as the one triggered in this issue. For easier cases, https://github.com/verus-lang/verus/tree/main/source/tools/minimizers has some easy-to-use interestingness-test scripts (e.g., see rlimit_exceeded.sh).

[jonhnet]

Wow that autominimizer is pretty great.

[Chris-Hawblitzel]

Can you try with the most recent commit?

[jonhnet]

Yup, that seems to have fixed it. Thank you!