parallel add

logsem · Aug 14, 2024 · bb58bd1 · bb58bd1
1 parent 8923f89
commit bb58bd1
Show file tree

Hide file tree

Showing 2 changed files with 108 additions and 6 deletions.
diff --git a/theories/base_logic/error_credits.v b/theories/base_logic/error_credits.v
@@ -13,6 +13,8 @@ Canonical Structure nonnegrealO : ofe := leibnizO nonnegreal.
 (** ** RA for the reals in the interval [0, 1) with addition as the operation. *)
 Section nonnegreal.
 
+  Global Instance nonnegreal_inhabited : Inhabited nonnegreal := populate (nnreal_one).
+
   #[local] Open Scope R.
   #[local] Open Scope NNR.
 

diff --git a/theories/coneris/examples/parallel_add.v b/theories/coneris/examples/parallel_add.v
@@ -33,6 +33,17 @@ Section lemmas.
     { by apply excl_auth_update. }
     done.
   Qed.
+
+  Local Lemma resource_nonneg (b:option bool): (0 <= 1 - Rpower 2 (bool_to_nat (ssrbool.isSome b) - 1))%R.
+  Proof.
+    destruct b as [[]|]; simpl.
+    - replace (1-1)%R with 0%R by lra.
+      rewrite Rpower_O; lra.
+    - replace (1-1)%R with 0%R by lra.
+      rewrite Rpower_O; lra.
+    - replace (0-1)%R with (-1)%R by lra.
+      rewrite Rpower_Ropp. rewrite Rpower_1; lra.
+  Qed. 
 End lemmas.
 
 
@@ -201,13 +212,102 @@ Proof.
   { rewrite /flipL.
     wp_pures.
     wp_bind (rand _)%E.
-    (* adding an extra question mark for nonnegreal doesnt work ?? *)
-    iInv "I" as (???) "K" "Hclose".
-    (* iDestruct (ghost_var_agree' with "[$Hγ1●][$]") as "->". *)
-    (* simpl in *. subst. *)
-    (* wp_apply (wp_couple_rand_adv_comp1 with "[Herr]"). *)
+    iInv "I" as (?????) ">( Hγ1● & Hγ2● & Hl & Herr & %H & -> & ->)" "Hclose".
+    iDestruct (ghost_var_agree' with "[$Hγ1●][$]") as "->".
+    simpl in *.
+    wp_apply (wp_couple_rand_adv_comp1 _ _ _ _
+                (λ x, if fin_to_nat x =? 0 then nnreal_one else mknonnegreal (1 - Rpower 2 (bool_to_nat (ssrbool.isSome b2) - 1))%R _) with "[$Herr]").
+    - rewrite SeriesC_finite_foldr; simpl.
+      rewrite H.
+      trans ((1 / (1 + 1) * (2 - Rpower 2 (bool_to_nat (ssrbool.isSome b2) - 1)) + 0))%R; first lra.
+      trans (1 / (1 + 1) *  (2 - 2*Rpower 2 (bool_to_nat (ssrbool.isSome b2) - 2)))%R; last lra.
+      assert (((Rpower 2 (bool_to_nat (ssrbool.isSome b2) - 1)) + 0)%R =
+              (( 2 * Rpower 2 (bool_to_nat (ssrbool.isSome b2) - 2)))%R); last lra.
+      assert (((INR (bool_to_nat (ssrbool.isSome b2)) - 1))%R = (1+(bool_to_nat (ssrbool.isSome b2) - 2)))%R as -> by lra.
+      rewrite Rpower_plus. rewrite Rpower_1; lra.
+    - iIntros (n) "Herr".
+      inv_fin n; simpl; first (iExFalso; by iApply (ec_contradict with "[$]")).
+      intros n. inv_fin n; last (intros n; inv_fin n).
+      iMod (ghost_var_update' _ (Some false) with "[$Hγ1●][$]") as "[Hγ1● Hγ1◯]".
+      iMod ("Hclose" with "[Hγ1● Hγ2● Hl Herr]") as "_".
+      { iNext. iExists _, _, _, (mknonnegreal _ _ ), _. iFrame.
+        repeat iSplit; iPureIntro; [|done|done].
+        rewrite S_INR.
+        simpl.
+        replace (INR (bool_to_nat (ssrbool.isSome b2)) + 1 - 2)%R with
+          (INR (bool_to_nat (ssrbool.isSome b2)) - 1)%R by lra.
+        lra.
+      }
+      iModIntro. wp_pures.
+      wp_apply conversion.wp_int_to_bool as "_"; first done.
+      wp_pures.
+      clear err H.
+      iInv "I" as (?????) ">( Hγ1● & Hγ2● & Hl & Herr & %H & -> & ->)" "Hclose".
+      iDestruct (ghost_var_agree' with "[$Hγ1●][$]") as "->".
+      wp_faa.
+      iMod (ghost_var_update' _ (Some true) with "[$Hγ1●][$]") as "[Hγ1● Hγ1◯]".
+      iMod ("Hclose" with "[Hγ1● Hγ2● Hl Herr]") as "_"; last done.
+      iNext. iExists _, _, _, (mknonnegreal _ _ ), _. iFrame; simpl.
+      repeat iSplit; iPureIntro; [done|done|lia]. 
   }
-Admitted.
+  { rewrite /flipL.
+    wp_pures.
+    wp_bind (rand _)%E.
+    iInv "I" as (?????) ">( Hγ1● & Hγ2● & Hl & Herr & %H & -> & ->)" "Hclose".
+    iDestruct (ghost_var_agree' with "[$Hγ2●][$]") as "->".
+    simpl in *.
+    wp_apply (wp_couple_rand_adv_comp1 _ _ _ _
+                (λ x, if fin_to_nat x =? 0 then nnreal_one else mknonnegreal (1 - Rpower 2 (bool_to_nat (ssrbool.isSome b1) - 1))%R _) with "[$Herr]").
+    - rewrite SeriesC_finite_foldr; simpl.
+      rewrite H.
+      trans ((1 / (1 + 1) * (2 - Rpower 2 (bool_to_nat (ssrbool.isSome b1) - 1)) + 0))%R; first lra.
+      rewrite Nat.add_0_r.
+      trans (1 / (1 + 1) *  (2 - 2*Rpower 2 (bool_to_nat (ssrbool.isSome b1) - 2)))%R; last lra.
+      assert (((Rpower 2 (bool_to_nat (ssrbool.isSome b1) - 1)) + 0)%R =
+              (( 2 * Rpower 2 (bool_to_nat (ssrbool.isSome b1) - 2)))%R); last lra.
+      assert (((INR (bool_to_nat (ssrbool.isSome b1)) - 1))%R = (1+(bool_to_nat (ssrbool.isSome b1) - 2)))%R as -> by lra.
+      rewrite Rpower_plus. rewrite Rpower_1; lra.
+    - iIntros (n) "Herr".
+      inv_fin n; simpl; first (iExFalso; by iApply (ec_contradict with "[$]")).
+      intros n. inv_fin n; last (intros n; inv_fin n).
+      iMod (ghost_var_update' _ (Some false) with "[$Hγ2●][$]") as "[Hγ2● Hγ2◯]".
+      iMod ("Hclose" with "[Hγ1● Hγ2● Hl Herr]") as "_".
+      { iNext. iExists _, _, _, (mknonnegreal _ _ ), _. iFrame.
+        repeat iSplit; iPureIntro; [|done|done].
+        rewrite plus_INR.
+        simpl.
+        replace (INR (bool_to_nat (ssrbool.isSome b1))+1 - 2)%R with
+          (INR (bool_to_nat (ssrbool.isSome b1)) - 1)%R; lra.
+      }
+      iModIntro. wp_pures.
+      wp_apply conversion.wp_int_to_bool as "_"; first done.
+      wp_pures.
+      clear err H.
+      iInv "I" as (?????) ">( Hγ1● & Hγ2● & Hl & Herr & %H & -> & ->)" "Hclose".
+      iDestruct (ghost_var_agree' with "[$Hγ2●][$]") as "->".
+      wp_faa.
+      iMod (ghost_var_update' _ (Some true) with "[$Hγ2●][$]") as "[Hγ2● Hγ2◯]".
+      iMod ("Hclose" with "[Hγ1● Hγ2● Hl Herr]") as "_"; last done.
+      iNext. iExists _, _, _, (mknonnegreal _ _ ), _. iFrame; simpl.
+      repeat iSplit; iPureIntro; [done|done|lia]. 
+  }
+  iIntros (??) "[Hγ1◯ Hγ2◯]".
+  iNext. wp_pures.
+  iInv "I" as (?????) ">( Hγ1● & Hγ2● & Hl & Herr & %H & -> & ->)" "Hclose".
+  wp_load.
+  iDestruct (ghost_var_agree' with "[$Hγ1●][$]") as "->".
+  iDestruct (ghost_var_agree' with "[$Hγ2●][$]") as "->".
+  iMod ("Hclose" with "[Hγ1● Hγ2● Hl Herr]") as "_".
+  - iNext. iFrame. iPureIntro. simpl. eexists _. repeat split; naive_solver.
+  - simpl. iApply "HΦ". iPureIntro. lia.
+    Unshelve.
+    all: try lra.
+    all: try apply cond_nonneg.
+    + pose proof resource_nonneg b2. lra.
+    + pose proof resource_nonneg b2. lra.
+    + pose proof resource_nonneg b1. lra.
+    + pose proof resource_nonneg b1. lra.
+Qed.
 
 End parallel_add.