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

• [x] main impl

core::result::Result

• [x] main impl

core::clone::Clone

• [x] snapshot equality with opt-out mechanism

core::default::Default

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

specific default values

• [x] (), bool, char, numbers (the types specified here)
• [x] 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

• [x] impl for core::option::Option
• [x] impl for core::option::Result

core::mem::size_of

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

core::convert::From/Into

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

Slices/Arrays

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

Indexing is currently blocked due to #1221.

alloc::vec::Vec

• [ ] Deref as slice (#1221)
• [ ] forwarding of most operations to as_slice (#1221)
• [ ] vec! macro (requires unsizing from above, but very simple given that!)

alloc::string::String

• [ ] Deref as str (#1221)
• [ ] forwarding of most operations to as_str (#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 (#1311)

core::ops Binary Ops for References

• [x] specify how these ops are equivalent to applying to deref'd values
• [ ] the same for comparisons (#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.

[Pointerbender]

Once this PR has laid the ground-work for adding specs to the Rust standard library, how hard/easy would it be for an advanced end-user to contribute standard library specs for iterators to Prusti? :) Would it be as easy as adding a bunch of #[extern_spec]s under prusti-contracts/prusti-std/src/ or would it require some extra development first to be able to extern_spec iterator logic? Thanks for building this btw, I'm really looking forward to using this already! :D

[Aurel300]

Once this PR has laid the ground-work for adding specs to the Rust standard library, how hard/easy would it be for an advanced end-user to contribute standard library specs for iterators to Prusti? :) Would it be as easy as adding a bunch of #[extern_spec]s under prusti-contracts/prusti-std/src/ or would it require some extra development first to be able to extern_spec iterator logic? Thanks for building this btw, I'm really looking forward to using this already! :D

Adding specs to prusti-std would indeed be the general idea. We do already have an iterator methodology, which I will be submitting to prusti-std at some point after this PR. In some cases, we will find issues (some of which Julian has linked in the description of this PR) that would block the specs we want to write. Some of these issues can be quite heavy, for example: supporting references in structs.

[juliand665]

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