Issue in lifetime checking with imported Verus crates

[zhengyao-lin]

Hello! I encountered an issue similar to #1249.
Basically I have a crate A importing crate B. And Verus emits many trait impl errors in the form of

error: the trait bound `Tail: T44_Combinator` is not satisfied
...

note: This error was found in Verus pass: ownership checking of tracked code` at the end.

where Tail and Combinator are both defined in crate B,

This seems to have happened during lifetime checking (no error if I do --no-lifetime), so I looked at the rust code emitted for lifetime checking (using --log lifetime), and the output .verus-log/crate-lifetime.rs is indeed omitting impls mentioned in the errors.
For example, impl T44_Combinator is missing for Tail for the error message above.

In .verus-log/crate-lifetime.rs, the only place where the impl T44_Combinator for Tail is needed is in an associated type definition:

impl T44_Combinator for D41_AlgorithmIdentifier {
    type A40_Result<'a43_a, > = .... <D93_Tail as T44_Combinator>::A40_Result<'a43_a, > ...;
    ...
}

(some code is omitted for readability)
D41_AlgorithmIdentifier is defined in crate B

Also this only happens if I separate crates A and B (no issue if I do it in the same crate).

The full .verus-log/crate-lifetime.rs file is here:
crate-lifetime.rs.txt

[y1ca1]

I wish we could assign a Blocking label to this issue. This is essentially preventing many Verus library crates from being a library.

[zhengyao-lin]

Question: if I use --no-lifetime with --compile, the lifetime is still going to be checked at the end and there's is no soundness issue, right?

[tjhance]

That's not correct — running with --no-lifetime will cause proof-mode lifetime-checking to be skipped.

[Chris-Hawblitzel]

Can you try the lifetime-trait-impl branch?

[zhengyao-lin]

Hi Chris, thanks for working on this!

I cherry-picked your fix (b909615) to the commit 25303cd before #1289 (after that verus crashed for a different reason).
And it crashes now with this message:

thread 'rustc' panicked at rust_verify/src/spans.rs:221:9:
assertion failed: original_hi <= original_end_pos

This can be reproduced by running cd chain && make in this branch https://github.com/zhengyao-lin/x509/tree/chain-bug