verus-lang / verus

Verified Rust for low-level systems code
MIT License
1.25k stars 72 forks source link

V1.82 #1325

Closed ziqiaozhou closed 1 month ago

ziqiaozhou commented 1 month ago

This draft PR is only created as a draft and is not intended to be merged to v1.79.

@utaal, this is the change I mentioned about supporting v1.82. The only issue I encountered is about negative trait and conflicted trait implementations.

conflicting implementations of trait `T57_IntoIterator` for type `&mut std::boxed::Box<[_], _>`

Or

found both positive and negative implementation of trait `T55_Iterator` for type `&mut std::boxed::Box<[_], _>`.

The way I bypass it for now is to check the polarity and add negative when needed. But still, I need to explicitly rule out Box cases.

Adding with_negative_coherence feature finally solved the issue I encountered. But I have 5 failed tests in example which is expected to fail and does fail. I may need to check the test lib and see why the failure is not recognized as a correct failure.