changes to ptr library

[tjhance]

This adds partial support for variable-length allocations in the ptr library.

Changes:

• In addition to PointsTo<V>, there is also an "untyped PointsTo" called PointsToRaw which maps to an uninitialized region of memory of arbitrary length.
• PointsTo<V> and PointsToRaw can be converted between each other, provided the size of V is known.
• There is now a new proof object called Dealloc (and DeallocRaw) which provides the ability to deallocate a region of memory. This has to be separate from PointsTo, because it's possible for a PointsTo object to point into a subregion of an allocation. However, it's not possible to deallocate part of an allocation.
  • The verified_vec example shows a nontrivial use of PointsTo and Dealloc.
• I replaced the implementation for alloc & dealloc with functions from the allocator_api. It's unstable, but it's easier to use than what we had before.
• In order to talk about the sizes of types, I added a SizeOf trait. This is incomplete because it doesn't have support from Verus to actually calculate a size or an alignment, and as such, it forces the user to make an assume when they implement the trait.

Right now the tests are failing because of a bug related to lifetime checking & Copy.

[tjhance]

status: currently requires a fix regarding lifetime checking and Copy

[tjhance]

status:

• The lifetime-checking issue with Copy is fixed thanks to chris.
• However, there's an issue related to provenance that needs to be fixed (the API currently lets you do something UB according to Rust's pointer provenance rules), so I'm going to keep this marked as a draft

[tjhance]

Was it necessary to use std::alloc? I think this won't work for people using no-std

[utaal]

cargo build-ing vstd fails with the allocator feature because it's only available on nightly. I don't see a way around that.

But indeed we need to figure out a strategy for no-vstd users.

[utaal]

If the question was specifically about std::alloc vs alloc::alloc, then no. Fixed now.
Also tested with --vstd-no-std and --vstd-no-alloc.