Add some examples for finite nondeterminism

_CoqProject

@@ -37,6 +37,7 @@ theories/examples/stack/module_refinement.v
 theories/examples/stack/mailbox.v
 theories/examples/stack/helping.v
 theories/examples/various.v
+theories/examples/or.v
 theories/tests/typetest.v
 theories/tests/tactics.v
 theories/tests/tactics2.v

theories/examples/or.v

+From iris.proofmode Require Import tactics.
+From iris_logrel Require Export logrel examples.various.
+
+Definition or : val := λ: "e1" "e2",
+  let: "x" := ref #0 in
+  Fork ("x" <- #1);;
+  if: !"x" = #0
+  then "e1" #()
+  else "e2" #().
+
+Lemma or_type Γ :
+  typed Γ or
+        (TArrow (TArrow TUnit TUnit) (TArrow (TArrow TUnit TUnit)
+            TUnit)).
+Proof. solve_typed. Qed.
+Hint Resolve or_type : typeable.
+
+Section rules.
+  Context `{logrelG Σ}.
+
+  Lemma bin_log_related_or Δ Γ E e1 e2 e1' e2' :
+    ↑logrelN ⊆ E →
+    {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : TArrow TUnit TUnit -∗
+    {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : TArrow TUnit TUnit -∗
+    {E,E;Δ;Γ} ⊨ or e1 e2 ≤log≤ or e1' e2' : TUnit.
+  Proof.
+    iIntros (?) "He1 He2".
+    iApply (bin_log_related_app with "[He1] He2").
+    iApply (bin_log_related_app with "[] He1").
+    iApply binary_fundamental_masked; eauto with typeable.
+  Qed.
+
+  Lemma bin_log_or_choice_1_r_val Δ Γ E (v1 v2 : val) :
+    ↑logrelN ⊆ E →
+    Γ ⊢ₜ v1 : TArrow TUnit TUnit →
+    {E,E;Δ;Γ} ⊨ v1 #() ≤log≤ or v1 v2 : TUnit.
+  Proof.
+    iIntros (??).
+    unlock or. repeat rel_rec_r.
+    rel_alloc_r as x "Hx".
+    repeat rel_let_r.
+    rel_fork_r as j "Hj". rel_seq_r.
+    rel_load_r. repeat (rel_pure_r _).
+    iApply binary_fundamental_masked; eauto with typeable.
+  Qed.
+
+  Lemma bin_log_or_choice_1_r Δ Γ E (e1 : expr) (v2 : val) :
+    ↑logrelN ⊆ E →
+    Γ ⊢ₜ e1 : TArrow TUnit TUnit →
+    {E,E;Δ;Γ} ⊨ e1 #() ≤log≤ or e1 v2 : TUnit.
+  Proof.
+    iIntros (??).
+    rel_bind_l e1.
+    rel_bind_r e1.
+    iApply related_bind.
+    { iApply binary_fundamental_masked; eauto with typeable. }
+    iIntros ([f f']) "#Hf /=".
+    unlock or. repeat rel_rec_r.
+    rel_alloc_r as x "Hx".
+    repeat rel_let_r.
+    rel_fork_r as j "Hj". rel_seq_r.
+    rel_load_r. repeat (rel_pure_r _).
+    iApply related_ret. simpl.
+    iApply ("Hf" $! (#(),#())); eauto.
+  Qed.
+
+  Lemma bin_log_or_choice_1_r_body Δ Γ E (e1 : expr) (v2 : val) :
+    ↑logrelN ⊆ E →
+    Closed ∅ e1 →
+    Γ ⊢ₜ e1 : TUnit →
+    {E,E;Δ;Γ} ⊨ e1 ≤log≤ or (λ: <>, e1) v2 : TUnit.
+  Proof.
+    iIntros (???).
+    unlock or. repeat rel_rec_r.
+    rel_alloc_r as x "Hx".
+    repeat rel_let_r.
+    rel_fork_r as j "Hj". rel_seq_r.
+    rel_load_r. repeat (rel_pure_r _).
+    iApply binary_fundamental_masked; eauto with typeable.
+  Qed.
+
+  Lemma bin_log_related_spec_ctx Δ Γ E1 E2 e e' τ ℷ :
+    (ℷ ⊢ (∃ ρ, spec_ctx ρ) -∗ {E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ)%I →
+    (ℷ ⊢ {E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ)%I.
+  Proof.
+    intros Hp.
+    rewrite bin_log_related_eq /bin_log_related_def.
+    iIntros "Hctx". iIntros (vvs ρ') "#Hspec".
+    rewrite (persistentP (spec_ctx _)).
+    rewrite (uPred.always_sep_dup' (spec_ctx _)).
+    iDestruct "Hspec" as "#[Hspec #Hspec']".
+    iRevert "Hspec'".
+    rewrite (uPred.always_elim (spec_ctx _)).
+    iAssert (∃ ρ, spec_ctx ρ)%I as "Hρ".
+    { eauto. }
+    iClear "Hspec".
+    iRevert (vvs ρ').
+    fold (bin_log_related_def E1 E2 Δ Γ e e' τ).
+    rewrite -bin_log_related_eq.
+    iApply (Hp with "Hctx Hρ").
+  Qed.
+
+  Definition shootInv `{oneshotG Σ} x γ : iProp Σ :=
+    (x ↦ᵢ #0 ∗ pending γ ∨ x ↦ᵢ #1 ∗ shot γ)%I.
+  Ltac close_shoot := iNext; (iLeft + iRight); by iFrame.
+
+  Lemma assign_safe `{oneshotG Σ} x γ :
+    inv shootN (shootInv x γ)
+    ⊢ ▷ WP #x <- #1 {{ _, True }}.
+  Proof.
+    iIntros "#Hinv".
+    iNext. iInv shootN as ">[[Hx Ht] | [Hx Ht]]" "Hcl"; wp_store.
+    + iMod (shoot with "Ht") as "Ht".
+      iMod ("Hcl" with "[-]"); first close_shoot; eauto.
+    + iMod ("Hcl" with "[-]"); first close_shoot; eauto.
+  Qed.
+
+  Lemma bin_log_or_commute `{oneshotG Σ} Δ Γ E (v1 v2 : val) :
+    ↑shootN ⊆ E →
+    ↑logrelN ⊆ E →
+    Γ ⊢ₜ v1 : TArrow TUnit TUnit →
+    Γ ⊢ₜ v2 : TArrow TUnit TUnit →
+    {E,E;Δ;Γ} ⊨ or v2 v1 ≤log≤ or v1 v2 : TUnit.
+  Proof.
+    iIntros (????).
+    unlock or. repeat rel_rec_r. repeat rel_rec_l.
+    rel_alloc_l as x "Hx".
+    rel_alloc_r as y "Hy".
+    repeat rel_let_l. repeat rel_let_r.
+    rel_fork_r as j "Hj". rel_seq_r.
+    iApply fupd_logrel.
+    iMod new_pending as (γ) "Ht".
+    iModIntro.
+    iMod (inv_alloc shootN _ (shootInv x γ) with "[Hx Ht]") as "#Hinv".
+    { close_shoot. }
+    rel_fork_l.
+    iModIntro. iSplitR; [ by iApply assign_safe | ].
+    rel_seq_l.
+    rel_load_l_atomic.
+    iInv shootN as ">[[Hx Ht] | [Hx Ht]]" "Hcl"; 
+      iExists _; iFrame; iModIntro; iNext; iIntros "Hx";
+      rel_op_l; rel_if_l.
+    + apply bin_log_related_spec_ctx.
+      iDestruct 1 as (ρ1) "#Hρ1".
+      (* TODO: tp tactics should be aware of that ^ *)
+      tp_store j.
+      rel_load_r.
+      repeat (rel_pure_r _).
+      iMod ("Hcl" with "[-]"); first close_shoot.
+      iApply binary_fundamental_masked; eauto with typeable.
+    + rel_load_r.
+      repeat (rel_pure_r _).
+      iMod ("Hcl" with "[-]"); first close_shoot.
+      iApply binary_fundamental_masked; eauto with typeable.
+  Qed.
+
+  Lemma bin_log_or_idem_r Δ Γ E e :
+    Closed ∅ e →
+    ↑logrelN ⊆ E →
+    Γ ⊢ₜ e : TUnit →
+    {E,E;Δ;Γ} ⊨ e ≤log≤ or (λ: <>, e) (λ: <>, e) : TUnit.
+  Proof.
+    iIntros (???).
+    iPoseProof (bin_log_or_choice_1_r_body Δ _ _ e (λ: <>, e)) as "HZ"; eauto.
+    unlock. eauto. (* TODO :( *)
+  Qed.
+
+  Lemma bin_log_or_idem_l `{oneshotG Σ} Δ Γ E e :
+    Closed ∅ e →
+    ↑shootN ⊆ E →
+    ↑logrelN ⊆ E →
+    Γ ⊢ₜ e : TUnit →
+    {E,E;Δ;Γ} ⊨ or (λ: <>, e) (λ: <>, e) ≤log≤ e : TUnit.
+  Proof.
+    iIntros (????).
+    unlock or. repeat rel_rec_l.
+    rel_alloc_l as x "Hx".
+    repeat rel_let_l.
+    iApply fupd_logrel.
+    iMod new_pending as (γ) "Ht".
+    iModIntro.
+    iMod (inv_alloc shootN _ (shootInv x γ)%I with "[Hx Ht]") as "#Hinv".
+    { close_shoot. }
+    rel_fork_l.
+    iModIntro. iSplitR; [ by iApply assign_safe | ].
+    rel_seq_l.
+    rel_load_l_atomic.
+    iInv shootN as ">[[Hx Ht] | [Hx Ht]]" "Hcl"; 
+      iExists _; iFrame; iModIntro; iNext; iIntros "Hx";
+        rel_op_l; rel_if_l; rel_seq_l.
+    + iMod ("Hcl" with "[-]"); first close_shoot.
+      iApply binary_fundamental_masked; eauto with typeable.
+    + iMod ("Hcl" with "[-]"); first close_shoot.
+      iApply binary_fundamental_masked; eauto with typeable.    
+  Qed.
+
+  Lemma bin_log_or_bot_l `{oneshotG Σ} Δ Γ E e :
+    Closed ∅ e →
+    ↑shootN ⊆ E →
+    ↑logrelN ⊆ E →
+    Γ ⊢ₜ e : TUnit →
+    {E,E;Δ;Γ} ⊨ or (λ: <>, e) bot ≤log≤ e : TUnit.
+  Proof.
+    iIntros (????).
+    unlock or. repeat rel_rec_l.
+    rel_alloc_l as x "Hx".
+    repeat rel_let_l.
+    iApply fupd_logrel.
+    iMod new_pending as (γ) "Ht".
+    iModIntro.
+    iMod (inv_alloc shootN _ (shootInv x γ)%I with "[Hx Ht]") as "#Hinv".
+    { close_shoot. }
+    rel_fork_l.
+    iModIntro. iSplitR; [ by iApply assign_safe | ].
+    rel_seq_l.
+    rel_load_l_atomic.
+    iInv shootN as ">[[Hx Ht] | [Hx Ht]]" "Hcl"; 
+      iExists _; iFrame; iModIntro; iNext; iIntros "Hx";
+      rel_op_l; rel_if_l.
+    + iMod ("Hcl" with "[-]"); first close_shoot.
+      rel_seq_l.
+      iApply binary_fundamental_masked; eauto with typeable.
+    + iMod ("Hcl" with "[-]"); first close_shoot.
+      rel_apply_l (bot_l False). iIntros ([]).
+  Qed.
+
+  Lemma bin_log_or_bot_r Δ Γ E e :
+    Closed ∅ e →
+    ↑logrelN ⊆ E →
+    Γ ⊢ₜ e : TUnit →
+    {E,E;Δ;Γ} ⊨ e ≤log≤ or (λ: <>, e) bot : TUnit.
+  Proof.
+    iIntros (???).
+    iApply bin_log_or_choice_1_r_body; eauto.
+  Qed.
+
+End rules.