Precise Reasoning about Container-Internal Pointers with Logical Pinning

on YouTube ↗23m

" summary

Claims a lightweight borrowing discipline called logical pinning that decouples address exposure from ownership so container-internal pointers can be tracked precisely with four states owned/offered/borrowed/missing. It proves pointer-stability for in-place writes so map-style updates preserve exposed pointers, models an M operation that offers a pointer without losing verifier information, verifies small pointer-manipulating programs, and mechanizes all results in the Rocq proof assistant using the CFML library.

AI-written summary · about

" chapters (11)

1. 0:00Logical pinning for container pointers
2. 1:26Container internal pointers hard to reason
3. 3:13Limitations of separation logic
4. 4:37Key observations on container ops
5. 5:20Logical pinning solution core idea
6. 7:27Pointer stability with classification
7. 9:54Logical pinning in Iris framework
8. 10:16Logical pinning explained step-by-step
9. 14:33API specs for pointer validity
10. 16:59Summary of logical pinning
11. 18:49Q&A