About heap restriction in PPtr

[zpzigi754]

In the document about PPtr, it is mentioned that the target object should be allocated through heap.

However, in the low-level programming, many objects could be allocated without using heap.

Is there any way to circumvent the heap-related restriction in PPtr?
If one wants to use PPtr-like structure for the raw pointer not pointing to the heap, what is the biggest challenge to overcome?

It would be great if verus team support this feature: PPtr for non-heap objects.

[tjhance]

The next generation of Verus pointer support is something that is being actively worked on. The first step is to create a more precise model of pointers, which you can see in vstd/raw_ptr.rs. (However, I would not recommend using it yet.) The new interface is going to operate on the actual Rust pointer types (*mut T and *const T) rather than PPtr. I expect we'll eventually have ways to manipulate pointers that point to stack variables, cell interiors, and so on.

[zpzigi754]

Thank you very much for the explanation and the reference, @tjhance. Good to hear the news about verus's next generation pointer support!

Is there any reason that you do not recommend using the APIs (e.g., ptr_mut_write, ptr_mut_read, and ptr_ref) in vstd/raw_ptr.rs yet? I see the relevant PR in #1052.

[tjhance]

The simple reason is that it's still a work-in-progress. It doesn't have enough features to be useful.

[zpzigi754]

@tjhance, raw pointers have been updated in #1244. Do you now recommend using vstd/raw_ptr.rs?

[tjhance]

Yes. Unfortunately, they still don't support the feature requested by this issue. However, we are getting closer.