creusot icon indicating copy to clipboard operation
creusot copied to clipboard

Published 20 hours ago • verified publisher icon creusot-rs

Add pointer specs needed to verify `swap` on slices

Open Lysxia opened this issue 6 months ago • 1 comments

Stuff needed to verify swap on slices.

Lysxia avatar May 16 '25 10:05 Lysxia

TODO:

  • [x] Handle size_of
  • [x] Allow conversions in logic between *mut and *const
  • [x] Finish the pointer specs and document their rationale

Lysxia avatar May 21 '25 12:05 Lysxia

With this batch of methods I've reached the milestone of verifying 7/10 of the unsafe slice methods (the "easy" ones) from the verify-rust-std challenge.

Lysxia avatar Oct 30 '25 14:10 Lysxia

(I have put reviewing this on my TODO list, but I am rather busy these days...)

jhjourdan avatar Nov 06 '25 15:11 jhjourdan