Provide Specs for the Standard Library

[juliand665]

As part of my thesis under @Aurel300, this pull request adds specifications to the most popular types & functions in the Rust Standard Library. I am using data gathered through qrates to inform decisions on what specs to prioritize, along with a sense of logical units, e.g. covering all members of the unconstrained Option<T> or Result<T, E> impls, rather than only specifying the subset of these methods that sees the most usage.

Outline of Planned & Completed Specifications

These specs are very much a work in progress and far from complete at the moment, though what is there should be sound.

core::option::Option

• main impl

core::result::Result

• main impl

core::clone::Clone

• snapshot equality with opt-out mechanism

core::default::Default

• purity (for usage in specs) with opt-out mechanism

specific default values

• (), bool, char, numbers (the types specified here)
• other commonly-used types

core::ops::Deref

• purity (for usage in specs) with opt-out mechanism

This is currently blocked due to #1221.

core::ops::Index/core::ops::IndexMut

• purity (for usage in specs) with opt-out mechanism

This is similarly blocked due to #1221.

core::ops::Try

• impl for core::option::Option
• impl for core::option::Result

core::mem::size_of

• trait to allow users to specify what this method will return for their type
• via the above, numbers, which are by far the most commonly-passed types

core::convert::From/Into

• purity (for usage in specs) with opt-out mechanism
• numeric conversions, which are again very common

Slices/Arrays

• indexing with usize (built-in)
• length (built-in)
• "unsizing" arrays to slices

Indexing is currently blocked due to #1221.

alloc::vec::Vec

• Deref as slice (Error when using pure functions that return a reference #1221)
• forwarding of most operations to as_slice (Error when using pure functions that return a reference #1221)
• vec! macro (requires unsizing from above, but very simple given that!)

alloc::string::String

• Deref as str (Error when using pure functions that return a reference #1221)
• forwarding of most operations to as_str (Error when using pure functions that return a reference #1221)
• &str to String conversion using From/Into
  I envision Strings and Vecs to work very similarly, mostly powered by a pure as_str/as_slice that acts as the source of truth. Unfortunately, that approach (like so much other stuff) is currently blocked, but I think the issue is so fundamental that it's better to just resolve it directly than to find a temporary workaround.

core::cmp::PartialEq/core::cmp::PartialOrd

These are currently blocked due to #1311.

Ranges

• contains on inclusive & half-open ranges, for loops & invariants (Inheritance of Purity from Trait Specs #1311)

core::ops Binary Ops for References

• specify how these ops are equivalent to applying to deref'd values
• the same for comparisons (Inheritance of Purity from Trait Specs #1311)

These operations don't have blanket impls for when one or both sides are a reference, but their implementations are unified using macros, which probably makes sense for us to replicate.

Smart Pointers (e.g. alloc::rc::Rc)

This fundamentally relies on Deref and is thus also blocked by #1221.
Once that is resolved, specifying their Deref implementation as pure and expressing transfer into and out of a box via e.g. ensures(old(x) === snap(result.deref())) should go a long way towards specifying this type usefully.
Note that Box already has builtin support in Prusti, partly because Rust itself already treats it specially (e.g. that *box can move out of the box).

[Pointerbender]

core::mem::size_of
trait to allow users to specify what this method will return for their type

That's exciting stuff! Would this also be possible for core::mem::align_of, by any chance? :)

[juliand665]

Would this also be possible for core::mem::align_of, by any chance? :)

Sure! For the values so far, size and alignment seem to be the same, so that should be really simple. Interestingly, it seems that align_of is not commonly called with these types. I'll specify it anyway since it's so simple though.

[juliand665]

Oh yeah, to establish a link: this resolves #941!

[LrWm3]

is this something that could be partially merged?