add reentrant example

theories/examples/termination/eventloop.v

@@ -28,10 +28,10 @@ Section eventloop_code.
   Definition enqueue : val := push.
 
   Definition run : val :=
-      λ: "q", rec: "run" <> :=
+      rec: "run" "q" :=
       match: pop "q" with
         NONE => #()
-      | SOME "f" => "f" #() ;; "run" #()
+      | SOME "f" => "f" #() ;; "run" "q"
       end.
 
   Definition mkqueue : val :=
@@ -40,7 +40,7 @@ Section eventloop_code.
 End eventloop_code.
 Section eventloop_spec.
 
-  Context {SI} {Σ: gFunctors SI} `{Hheap: !heapG Σ} `{Htc: !tcG Σ} `{Hseq: !seqG Σ} (N : namespace).
+  Context {SI} {Σ: gFunctors SI} `{Hheap: !heapG Σ} `{Htc: !tcG Σ} `{Hseq: !seqG Σ}.
 
   Implicit Types (l: loc).
 
@@ -50,7 +50,10 @@ Section eventloop_spec.
     | x :: xs => ∃ l hd', ⌜hd = SOMEV #l⌝ ∗ l ↦ (x, hd') ∗ φ x ∗ stack_contents hd' xs φ
   end%I.
   Definition stack (l: loc) (xs: list val) (φ: val → iProp Σ): iProp Σ := (∃ hd, l ↦ hd ∗ stack_contents hd xs φ)%I.
-  Definition queue (q: val) : iProp Σ := (∃ l, ⌜q = #l⌝ ∗ na_inv seqG_name (N .@ l) (∃ xs, stack l xs (λ f, $ one ∗ SEQ f #() [{_, True}])))%I.
+  Definition queue (q: val) : iProp Σ := (∃ l, ⌜q = #l⌝ ∗ na_inv seqG_name (nroot .@ l) (∃ xs, stack l xs (λ f, $ one ∗ SEQ f #() [{_, True}])))%I.
+
+  Global Instance queue_persistent: Persistent (queue q).
+  Proof. apply _. Qed.
 
 
   Lemma new_stack_spec φ:
@@ -93,9 +96,9 @@ Section eventloop_spec.
   Qed.
 
   Lemma run_spec `{FiniteBoundedExistential SI} q :
-    queue q ∗ $ one ⊢ SEQ (run q #()) [{v, ⌜v = #()⌝ }].
+    queue q ∗ $ one ⊢ SEQ (run q) [{v, ⌜v = #()⌝ }].
   Proof.
-    iIntros "[#Q Hc] Hna". rewrite /run. do 2 wp_pure _.
+    iIntros "[#Q Hc] Hna". rewrite /run.
     iLöb as "IH". wp_pures.
     wp_bind (pop _). iDestruct "Q" as (l) "[-> I]".
     iMod (na_inv_acc_open _ _ _ with "I Hna") as "Hinv"; auto.
@@ -153,7 +156,7 @@ Section open_example.
   Variable external_code: val.
   Variable print: val.
   Variable q: val.
-  Context {SI} {Σ: gFunctors SI} `{Hheap: !heapG Σ} `{Htc: !tcG Σ} `{Hseq: !seqG Σ} (N : namespace).
+  Context {SI} {Σ: gFunctors SI} `{Hheap: !heapG Σ} `{Htc: !tcG Σ} `{Hseq: !seqG Σ}.
 
 
   Definition for_loop: val :=
@@ -189,7 +192,7 @@ Section open_example.
   Qed.
 
   Lemma example_spec `{FiniteBoundedExistential SI}:
-    queue N q ∗ $ (omul (one: ordA SI)) ∗ SEQ external_code #() [{ v, ∃ n: nat, ⌜v = #n⌝ }] ∗ (□ ∀ n: Z, SEQ print #n [{ _, True }]) ⊢
+    queue q ∗ $ (omul (one: ordA SI)) ∗ SEQ external_code #() [{ v, ∃ n: nat, ⌜v = #n⌝ }] ∗ (□ ∀ n: Z, SEQ print #n [{ _, True }]) ⊢
     SEQ example [{ _, True }].
   Proof.
     iIntros "(#Q & Hc & Hwp & #Hprint) Hna". rewrite /example.
@@ -209,3 +212,36 @@ Section open_example.
 
 End open_example.
 
+
+
+Section reentrant_example.
+
+  Variable print: val.
+  Context {SI} {Σ: gFunctors SI} `{Hheap: !heapG Σ} `{Htc: !tcG Σ} `{Hseq: !seqG Σ}.
+
+  Definition reentrant_example : expr :=
+    let: "q" := mkqueue #() in
+    let: "f" := λ: <>, enqueue "q" (λ: <>, print #42) in
+    enqueue "q" "f";;
+    run "q".
+
+  Lemma reentrant_example_spec `{FiniteBoundedExistential SI}:
+    $ (omul (one: ordA SI)) ∗  (□ ∀ n: Z, SEQ print #n [{ _, True }]) ⊢
+    SEQ reentrant_example [{ _, True }].
+  Proof.
+    iIntros "(Hc & #Hprint) Hna". rewrite /reentrant_example.
+    wp_bind (mkqueue _). iMod (mkqueue_spec with "Hna") as "_".
+    iIntros (q) "[Hna #Hq]". iModIntro. wp_pures.
+    iApply (tc_weaken (omul (one: ordA SI)) (natmul (5)%nat (one: ordA SI))); auto; first apply (ord_stepindex.limit_upper_bound (λ n, natmul n one)).
+    iFrame "Hc". iIntros "(Hc1 & Hc2 & Hc3 & Hc4 & Hc5 & _)".
+    wp_bind (enqueue _ _). iMod (enqueue_spec with "[$Hq $Hc1 $Hc2 Hc3 Hc4] Hna") as "_".
+    - iIntros "Hna". wp_pures. iApply (rwp_wand with "[Hna Hc3 Hc4]"); first iApply (enqueue_spec with "[$Hq $Hc3 $Hc4] Hna").
+      { iIntros "Hna". wp_pures. iMod ("Hprint" with "Hna") as "_"; auto. }
+      iIntros (v) "[$ _]".
+    - iIntros (v) "[Hna ->]". iModIntro. wp_pures.
+      iApply (rwp_wand with "[-]").
+      { iApply (run_spec with "[$Hq $Hc5] Hna"). }
+      iIntros (v) "[Hna ->]". iFrame.
+    Qed.
+
+End reentrant_example.