Skip to content
Snippets Groups Projects
Commit 7bd646da authored by Daniël Louwrink's avatar Daniël Louwrink
Browse files

use auth pattern for state interp

parent fbd36a11
No related branches found
No related tags found
No related merge requests found
...@@ -10,6 +10,7 @@ Class lrustPreG Σ := HeapPreG { ...@@ -10,6 +10,7 @@ Class lrustPreG Σ := HeapPreG {
lrust_preG_heap_freeable :> inG Σ (authR heap_freeableUR); lrust_preG_heap_freeable :> inG Σ (authR heap_freeableUR);
lrust_preG_shared :> inG Σ (authR sharedUR); lrust_preG_shared :> inG Σ (authR sharedUR);
lrust_preG_active :> inG Σ (authR activeUR); lrust_preG_active :> inG Σ (authR activeUR);
lrust_preG_interp :> inG Σ interpR;
}. }.
Definition lrustΣ : gFunctors := Definition lrustΣ : gFunctors :=
...@@ -17,7 +18,8 @@ Definition lrustΣ : gFunctors := ...@@ -17,7 +18,8 @@ Definition lrustΣ : gFunctors :=
GFunctor (constRF (authR heapUR)); GFunctor (constRF (authR heapUR));
GFunctor (constRF (authR heap_freeableUR)); GFunctor (constRF (authR heap_freeableUR));
GFunctor (constRF (authR sharedUR)); GFunctor (constRF (authR sharedUR));
GFunctor (constRF (authR activeUR)) ]. GFunctor (constRF (authR activeUR));
GFunctor (constRF interpR) ].
Instance subG_heapPreG {Σ} : subG lrustΣ Σ lrustPreG Σ. Instance subG_heapPreG {Σ} : subG lrustΣ Σ lrustPreG Σ.
Proof. solve_inG. Qed. Proof. solve_inG. Qed.
...@@ -31,7 +33,7 @@ Proof. ...@@ -31,7 +33,7 @@ Proof.
iMod (own_alloc ( ( : heap_freeableUR))) as () "Hfγ"; iMod (own_alloc ( ( : heap_freeableUR))) as () "Hfγ";
first by apply auth_auth_valid. first by apply auth_auth_valid.
set (Hheap := HeapG _ _ _ ). set (Hheap := HeapG _ _ _ ).
set (Hstbor := StborG _ _ _ 1%positive). set (Hstbor := StborG _ _ _ _ 1%positive 2%positive).
set (Hrust := LRustG _ _ Hheap Hstbor). set (Hrust := LRustG _ _ Hheap Hstbor).
iModIntro. iExists (λ σ _, heap_ctx σ.(state_mem) stbor_ctx_dummy σ.(state_stbor))%I, (λ _, True%I). iSplitL. iModIntro. iExists (λ σ _, heap_ctx σ.(state_mem) stbor_ctx_dummy σ.(state_stbor))%I, (λ _, True%I). iSplitL.
{ iSplit; last done. iExists ∅. by iFrame. } { iSplit; last done. iExists ∅. by iFrame. }
......
This diff is collapsed.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment