I have reviewed rust/std/lib.rsspec and noticed the following:

• verifast/bin/rust/std/lib.rsspec

  Line 942 in 264ab9e

  // SOUNDNESS ISSUE: We currently don't prevent blocks of memory allocated by an allocator from outliving the allocator itself!! https://github.com/verifast/verifast/issues/829

  no longer seems to be an issue with [Rust] pred points_to_at_lft #853 having been merged.
• It seems that there is no requirement that unsafe markers on specifications agree to their definitions. Examples include

  verifast/bin/rust/std/lib.rsspec

  Line 625 in 264ab9e

  fn new_unchecked(ptr: *mut T) -> Unique<T>;

  or

  verifast/bin/rust/std/lib.rsspec

  Line 755 in 264ab9e

  fn from_size_align_unchecked(size: usize, align: usize) -> Layout;

  . This tripped me up a bit as I expected all safe functions to have //@ req true.