add GhostCell proof
I propose we add the GhostCell proof to the lambda-rust master. This is basically a cleanup and forward-port of the existing proof for that paper. The original proofs are by Joshua Yanovski.
The branch isn't done yet, I'll add more commits here as I make progress, but if you have comments already, feel free to chime in. :) I'll do my best to make the individual commits meaningful, so reviewing commit-by-commit is probably best.
-
Lifetime logic basics -
Type system changes -
BrandedVec proof -
GhostCell proof
Merge request reports
Activity
added 1 commit
- 6e8a164e - add derived 'meta' mechanism to lifetime logic: associate a lifetime with metadata (via a gname)
added 1 commit
- 33a5350a - make external lifetime context inclusion syntactic, and adjust type system and existing proofs
added 1 commit
- e31b0779 - make external lifetime context inclusion syntactic, and adjust type system and existing proofs
added 1 commit
- f3b9d2f0 - make external lifetime context inclusion syntactic, and adjust type system and existing proofs
added 1 commit
- 8f4ec5f4 - make external lifetime context inclusion syntactic, and adjust type system and existing proofs
I now also ported the BrandedVec and GhostCell proofs to current lambda-rust and Iris. Those proofs are likely more convoluted than they need to be; I did not try to remove all the redundancy but I did ensure that they pass with
Set Mangle Names. Set Default Goal Selector "!".So, they should not be unduly fragile or hard to maintain.
This is ready for review. I don't know if anyone actually wants to review this in detail, though -- @jjourdan @robbertkrebbers please let me know how to proceed. As far as I am concerned we can just land this.
