support actual raw ptrs 4real

[tjhance]

Initial support for *mut T and *const T.

I have put off supporting these types for a long time because it requires figuring out What Actually Are Pointers In Rust, and leaving behind the kinda-idealized "a pointer is an address" model of PPtr. This was sort of philosophical because I like the idealized model and think it's closer to the Right Thing for greenfield verified code. However, the lack of support for the 'actual' Rust pointer types is increasingly a bottleneck for verifying the standard library, so here we are.

This PR adds VIR support for the *mut and *const, a model for pointers, and a few elementary operations. Similar to slices and arrays, pointer types are implemented as a Primitive type in VIR, with the actual 'view' model and operations defined in vstd. Both *mut T and *const T are encoded by the same type, and they are distinguished via a decoration. You can cast freely between them. (I confirmed with the Rust opsem team that there isn't actually any semantic difference between the two.)

The model

OK, I made it sound really intimidating, but when you really dig into it, it kind of isn't.

A pointer consists of three things:

• An address
• The "metadata" (the length for DSTs, and the vtable for a dyn type)
• The provenance (See the docs or the RFC.)

To handle provenance, we're just going to treat it as an abstract type. Maybe we'll add more axioms about it later, but I think it won't matter that much. I think for a lot of applications you can just use the *mut T, treating it like some abstract identifier without really worrying about what its model is.

One mistake I made with PPtr was specifying everything in terms of the address; for example, the model of PointsTo used a usize address rather than the PPtr itself, which means you were always having to get the address of the pointer to do anything with it. For the new API, I rectified this. In the new PointsTo object, the pointer is just, you know, a pointer, *mut T, as it should be.

I didn't actually modify PPtr itself, partly because I wanted to start from a fresh slate, and partly because a lot of code already depends on PPtr. I think once *mut is fleshed out, we can probably just verify PPtr in terms of *mut anyway.

The only features I added were the basic pointer read and write functionality, same as usual. In the future, we'll implement:

• Allocation and deallocation
• PointsToRaw equivalent
• DST support
• Pointer arithmetic and address-related operations
• Strict provenance API

[utaal]

I was late to the party on this, but it's very cool that you don't need an unsafe block because writes and reads go through Verus-defined functions -- I hadn't considered that implication of the fact that just having raw pointers and passing them around is not unsafe per se.