Higher-order profiling example

theories/examples/various.v

@@ -4,7 +4,7 @@
 *)
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import csum agree excl.
-From iris_logrel Require Import logrel examples.lock.
+From iris_logrel Require Import logrel examples.lock examples.counter.
 
 Section refinement.
   Context `{logrelG Σ}.
@@ -299,4 +299,227 @@ Section refinement.
     rel_load_l. rel_load_r.
     iApply bin_log_related_nat.
   Qed.
+
+  (** Higher-order profiling *)
+  Definition τg := TArrow TUnit TUnit.
+  Definition τf := TArrow τg TUnit.
+  Definition p : val := λ: "g", let: "c" := ref #0 in
+                                (λ: <>, FG_increment "c" #();; "g" #(), λ: <>, !"c").
+  (** The idea for the invariant is that we have to states:
+       a) c1 = n, c2 = n
+       b) c1 = n+1, c2 = n
+      We start in state (a) and can only transition to the state (b) by giving away an exclusive token.
+      But once we have transitioned to (b), we remain there forever.
+      To that extent we use to resources algebras two model two of those conditions, and we tie it all together in the invariant.
+  *)
+  Definition i6 `{oneshotG Σ} `{inG Σ (exclR unitR)} (c1 c2 : loc) γ γ' :=
+    (∃ (n : nat),
+     (c1 ↦ᵢ #n ∗ c2 ↦ₛ #n ∗ pending γ)
+   ∨ (c1 ↦ᵢ #(S n) ∗ c2 ↦ₛ #n ∗ shot γ ∗ own γ' (Excl ())))%I.
+  Lemma profiled_g `{oneshotG Σ} `{inG Σ (exclR unitR)} γ γ' c1 c2 g1 g2 Δ Γ :
+    inv shootN (i6 c1 c2 γ γ') -∗
+    ⟦ τg ⟧ Δ (g1, g2) -∗
+    {⊤,⊤;Δ;Γ} ⊨
+      (FG_increment #c1 #() ;; g1 #())
+    ≤log≤
+      (FG_increment #c2 #() ;; g2 #()) : TUnit.
+  Proof.
+    iIntros "#Hinv #Hg".
+    iApply (bin_log_related_seq); auto; last first.
+    { iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit).
+      iApply (related_ret ⊤). iApply interp_ret; eauto using to_of_val.
+      iApply bin_log_related_unit. }
+    rel_rec_l.
+    rel_apply_l (bin_log_FG_increment_logatomic _
+      (fun (n : nat) => (c2 ↦ₛ #n ∗ pending γ) ∨ (c2 ↦ₛ #(n-1) ∗ shot γ ∗ own γ' (Excl ()) ∗ ⌜1 ≤ n⌝))%I).
+    iAlways.
+    iInv shootN as (n) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht)]" "Hcl";
+      iModIntro; iExists _; iFrame.
+    - iSplitL "Hc2 Ht".
+      { iLeft. iFrame. }
+      iSplit.
+      { iDestruct 1 as (m) "[Hc1 [(Hc2 & Ht) | (Hc2 & Ht & Ht' & %)]]";
+        iApply ("Hcl" with "[-]"); iNext.
+        + iExists m. iLeft. iFrame.
+        + iExists (m-1). iRight.
+          rewrite minus_Sn_m // /= -minus_n_O.
+          iFrame. }
+      { iIntros (m) "[Hc1 Hc]".
+        iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]".
+        - unlock FG_increment. simpl.
+          rel_rec_r. rel_rec_r.
+          rel_load_r. rel_rec_r.
+          rel_op_r.
+          rel_cas_suc_r.
+          rel_if_r.
+          iMod ("Hcl" with "[-]") as "_".
+          { iNext. iExists (S m). iFrame. iLeft; iFrame. }
+          iApply bin_log_related_unit.
+        - unlock FG_increment. simpl.
+          rel_rec_r. rel_rec_r.
+          rel_load_r. rel_rec_r.
+          rel_op_r.
+          rel_cas_suc_r.
+          rel_if_r.
+          iMod ("Hcl" with "[-]") as "_".
+          { iNext. iExists m.
+            rewrite minus_Sn_m // /= -minus_n_O.
+            iFrame. iRight; iFrame. }
+            iApply bin_log_related_unit. }
+    - iSplitL "Hc2 Ht".
+      { rewrite /= -minus_n_O. iRight. iFrame.
+        iDestruct "Ht" as "[$ $]".
+        iPureIntro. omega. }
+      iSplit.
+      { iDestruct 1 as (m) "[Hc1 [(Hc2 & Ht) | (Hc2 & Ht & Ht' & %)]]";
+        iApply ("Hcl" with "[-]"); iNext.
+        + iExists m. iLeft. iFrame.
+        + iExists (m-1). iRight.
+          rewrite minus_Sn_m // /= -minus_n_O.
+          iFrame. }
+      { iIntros (m) "[Hc1 Hc]".
+        iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]".
+        - unlock FG_increment. simpl.
+          rel_rec_r. rel_rec_r.
+          rel_load_r. rel_rec_r.
+          rel_op_r.
+          rel_cas_suc_r.
+          rel_if_r.
+          iMod ("Hcl" with "[-]") as "_".
+          { iNext. iExists (S m). iFrame. iLeft; iFrame. }
+          iApply bin_log_related_unit.
+        - unlock FG_increment. simpl.
+          rel_rec_r. rel_rec_r.
+          rel_load_r. rel_rec_r.
+          rel_op_r.
+          rel_cas_suc_r.
+          rel_if_r.
+          iMod ("Hcl" with "[-]") as "_".
+          { iNext. iExists m.
+            rewrite minus_Sn_m // /= -minus_n_O.
+            iFrame. iRight; iFrame. }
+            iApply bin_log_related_unit. }
+  Qed.
+
+  Lemma profiled_g' `{oneshotG Σ} `{inG Σ (exclR unitR)} γ γ' c1 c2 g1 g2 Δ Γ :
+    inv shootN (i6 c1 c2 γ γ') -∗
+    ⟦ τg ⟧ Δ (g1, g2) -∗
+    {⊤,⊤;Δ;Γ} ⊨
+      (λ: <>, FG_increment #c1 #() ;; g1 #())
+    ≤log≤
+      (λ: <>, FG_increment #c2 #() ;; g2 #()) : τg.
+  Proof.
+    iIntros "#Hinv #Hg".
+    iApply bin_log_related_arrow_val; auto.
+    iAlways. iIntros (? ?) "[% %]". simplify_eq/=.
+    rel_seq_l. rel_seq_r.
+    iApply profiled_g; eauto.
+  Qed.
+
+  Lemma refinement6 `{oneshotG Σ} `{inG Σ (exclR unitR)} Γ :
+    Γ ⊨
+      (λ: "f" "g" "f'",
+       let: "pg" := p "g" in
+       let: "g'" := Fst "pg" in
+       let: "g''" := Snd "pg" in
+       "f" "g'";; "g'" #();; "f'" "g'";; "g''" #())
+    ≤log≤
+      (λ: "f" "g" "f'",
+       let: "pg" := p "g" in
+       let: "g'" := Fst "pg" in
+       let: "g''" := Snd "pg" in
+       "f" "g'";; "g" #();; "f'" "g'";; "g''" #() + #1)
+    : TArrow τf (TArrow τg (TArrow τf TNat)).
+  Proof.
+    iIntros (Δ).
+    iApply bin_log_related_arrow_val; auto.
+    iIntros "!#" (f1 f2) "#Hf". fold interp.
+    rel_let_l. rel_let_r.
+    iApply bin_log_related_arrow_val; auto.
+    iIntros "!#" (g1 g2)"#Hg". fold interp.
+    rel_let_l. rel_let_r.
+    iApply bin_log_related_arrow_val; auto.
+    iIntros "!#" (f'1 f'2) "#Hf'". fold interp.
+    rel_let_l. rel_let_r.
+    unlock p. simpl.
+    rel_let_l. rel_let_r.
+    rel_alloc_l as c1 "Hc1".
+    rel_alloc_r as c2 "Hc2".
+    iApply fupd_logrel.
+    iMod new_pending as (γ) "Ht". (*TODO typeclasses for this?*)
+    iMod (own_alloc (Excl ())) as (γ') "Ht'"; first done.
+    iModIntro.
+    iMod (inv_alloc shootN _ (i6 c1 c2 γ γ') with "[Hc1 Hc2 Ht]") as "#Hinv".
+    { iNext. iExists 0. iLeft. iFrame. }
+    rel_let_l. rel_let_r.
+    rel_let_l. rel_let_r.
+    rel_proj_l. rel_proj_r.
+    rel_let_l. rel_let_r.
+    rel_proj_l. rel_proj_r.
+    rel_let_l. rel_let_r.
+    iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit); auto.
+    { iApply (bin_log_related_app _ _ _ _ _ _ _ τg TUnit with "[Hf]").
+      iApply (related_ret ⊤). iApply interp_ret; eauto using to_of_val.
+      iApply profiled_g'; eauto. }
+    rel_seq_l.
+    rel_bind_l (FG_increment _). rel_rec_l.
+    (* rel_apply_l (bin_log_FG_increment_logatomic _ *)
+    (*   (fun (n : nat) => own γ' (Excl ()) ∗ (c2 ↦ₛ #n ∗ pending γ) ∨ (c2 ↦ₛ #(n-1) ∗ shot γ ∗ ⌜1 ≤ n⌝))%I). *)
+    unlock {2}FG_increment. simpl.
+    (* rel_rec_l. TODO: doesn't work :( *)
+    iLöb as "IH".
+    rel_pure_l (App (Rec "inc" _ _) _).
+    rel_load_l_atomic.
+    iInv shootN as (n) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht & Ht'2)]" "Hcl";
+      iModIntro; iExists _; iFrame; last first.
+    { iDestruct (own_valid_2 with "Ht' Ht'2") as %Hfoo.
+      inversion Hfoo. }
+    iNext. iIntros "Hc1".
+    iMod ("Hcl" with "[Hc1 Hc2 Ht]") as "_".
+    { iNext. iExists n. iLeft. iFrame. }
+    (* rel_let_l. TODO: doesn't work :( *)
+    rel_pure_l (App (Lam "c" _) _).
+    rel_op_l.
+    rel_cas_l_atomic.
+    iInv shootN as (m) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht & Ht'2)]" "Hcl";
+      iModIntro; iExists _; iFrame; last first.
+    { iDestruct (own_valid_2 with "Ht' Ht'2") as %Hfoo.
+      inversion Hfoo. }
+    iSplit.
+    - iIntros (?).
+      iNext. iIntros "Hc1".
+      iMod ("Hcl" with "[Hc1 Hc2 Ht]") as "_".
+      { iNext. iExists m. iLeft. iFrame. }
+      rel_if_l.
+      by iApply "IH".
+    - iIntros (?); simplify_eq/=.
+      iNext. iIntros "Hc1".
+      iApply fupd_logrel.
+      iMod (shoot γ with "Ht") as "#Hs".
+      iMod ("Hcl" with "[Hc1 Hc2 Hs Ht']") as "_".
+      { iNext. iExists n. iRight. iFrame. done. }
+      iModIntro.
+      rel_if_l.
+      rel_seq_l.
+      iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit); auto.
+      { iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit TUnit with "[Hg]").
+        iApply (related_ret ⊤). iApply interp_ret; eauto using to_of_val.
+        iApply bin_log_related_unit. }
+      iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit); auto.
+      { iApply (bin_log_related_app _ _ _ _ _ _ _ τg TUnit with "[Hf]").
+        iApply (related_ret ⊤). iApply interp_ret; eauto using to_of_val.
+        by iApply profiled_g'. }
+      rel_seq_l. rel_seq_r.
+      rel_load_l_atomic.
+      iInv shootN as (m) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht & Ht')]" "Hcl";
+        iModIntro; iExists _; iFrame.
+      { iExFalso. by iApply shot_not_pending. }
+      iNext. iIntros "Hc1".
+      rel_load_r. rel_op_r.
+      iMod ("Hcl" with "[-]") as "_".
+      { iNext. iExists m. iRight. iFrame. }
+      rewrite Nat.add_1_r.
+      iApply bin_log_related_nat.
+  Qed.
+
 End refinement.