Another work bug?

Author: pgiarrusso-sl

rocq-brick-libstdcpp/proof/mutex/demo_cpp_proof.v

@@ -32,7 +32,7 @@ Definition CR
   structR "C" q **
   _field "C::mut" |-> recursive_mutex.R γ.(recursive_mutex.lock_gname) q **
   as_Rep (fun this : ptr =>
-    recursive_mutex.inv_rmutex γ (∃ a_b : tele_arg _, tele_app (P this) a_b)).
+    recursive_mutex.inv_rmutex γ (∃ a b, this |-> CR' a b)).
 
 #[only(cfractional,ascfractional,type_ptr)] derive CR.
 #[only(lazy_unfold)] derive CR.
@@ -50,32 +50,78 @@ Section with_cpp.
      \arg{x} "x" (Vint x)
      \prepost{γ q} this |-> CR γ q
      \prepost{q'} recursive_mutex.token γ.(recursive_mutex.lock_gname) q'
-     \pre{args th} recursive_mutex.acquireable γ th args (TT:=TT) (P this)
-     \post recursive_mutex.acquireable γ th (TT:=TT) (recursive_mutex.update (TT:=TT) (fun (a b : Z) => mk (trim 64 (a+x)) b) args) (P this)).
+     \pre{args th} recursive_mutex.acquireable γ th args (TT:=TT) (fun a b => this |-> CR' a b)
+     \post recursive_mutex.acquireable γ th (TT:=TT) (recursive_mutex.update (TT:=TT) (fun (a b : Z) => mk (trim 64 (a+x)) b) args) (fun a b => this |-> CR' a b)).
 
   cpp.spec "C::update_b(long)" as C_update_b from demo_cpp.source with
     (\this this
      \arg{x} "x" (Vint x)
      \prepost{γ q} this |-> CR γ q
      \prepost{q'} recursive_mutex.token γ.(recursive_mutex.lock_gname) q'
-     \pre{args th} recursive_mutex.acquireable γ th args (TT:=TT) (P this)
-     \post recursive_mutex.acquireable γ th (TT:=TT) (recursive_mutex.update (TT:=TT) (fun (a b : Z) => mk a (trim 64 (b + x))) args) (P this)).
+     \pre{args th} recursive_mutex.acquireable γ th args (TT:=TT) (fun a b => this |-> CR' a b)
+     \post recursive_mutex.acquireable γ th (TT:=TT) (recursive_mutex.update (TT:=TT) (fun (a b : Z) => mk a (trim 64 (b + x))) args) (fun a b => this |-> CR' a b)).
 
   #[global] Instance CR_learn : Cbn (Learn (learn_eq ==> any ==> learn_hints.fin) CR).
   Proof. solve_learnable. Qed.
 
+  Import recursive_mutex.
+
+  #[global] Instance: `{Proper (equiv ==> equiv) (inv_rmutex γ)}.
+  Proof. rewrite inv_rmutex.unlock. solve_proper. Qed.
+
+  #[program]
+  Definition inv_rmutex_iff_C γ :=
+    \cancelx
+    \preserving{P1} inv_rmutex γ P1
+    \proving{P2} inv_rmutex γ P2
+    \through [| P1 ⊣⊢@{mpredI} P2 |]
+    \end.
+  Next Obligation. work. by setoid_subst. Qed.
+  #[local] Hint Resolve inv_rmutex_iff_C : br_hints.
+
+  #[program]
+  Definition inv_rmutex_wand_C γ :=
+    \cancelx
+    \preserving{P1} inv_rmutex γ P1
+    \proving{P2} inv_rmutex γ P2
+    \through □ (P1 ∗-∗ P2)
+    \end.
+  Next Obligation.
+    rewrite inv_rmutex.unlock.
+    iIntros "%% A %P2 #[? ?]".
+    iApply (inv_iff with "A").
+    iIntros "!> !>"; iSplit; ework with br_erefl; case_match; work.
+  Qed.
+  (* #[local] Hint Resolve inv_rmutex_wand_C : br_hints. *)
+
+  Lemma CR'_tele_equiv (this : ptr) :
+    (∃ a b : Z, this |-> CR' a b) ⊣⊢
+    ∃ xs : TT, tele_app (TT := TT) (λ a b : Z, this |-> CR' a b) xs.
+  Proof.
+    iSplit.
+    { iDestruct 1 as (a b) "?"; iExists (mk a b); work. }
+    iDestruct 1 as ([a [b []]]) "?"; iExists a, b; work.
+  Qed.
+  #[local] Hint Resolve CR'_tele_equiv : br_hints.
+
+  Lemma CR'_self_eq (this : ptr) :
+    (∃ a b : Z, this |-> CR' a b) ⊣⊢
+    (∃ a b : Z, this |-> CR' a b).
+  Proof. done. Qed.
+  #[local] Hint Resolve CR'_self_eq : br_hints.
+
   Lemma update_a_ok : verify[source] "C::update_a(long)".
   Proof.
     verify_spec; go.
     iExists TT.
     go.
-
-    rewrite P.unlock /=.
     destruct args as [a [b []]]; simpl; go.
-    iExists TT, _, _, (mk (trim 64 (a + x)) b).
+    iExists TT, (P this), _, (mk (trim 64 (a + x)) b).
+    go.
+    rewrite P.unlock.
     go.
     erewrite recursive_mutex.update_eq; last done; cbn.
-    rewrite P.unlock; work.
+    work.
   Qed.
 
   Lemma update_b_ok : verify[source] "C::update_b(long)".
@@ -84,31 +130,31 @@ Section with_cpp.
     iExists TT.
     go.
 
-    rewrite P.unlock /=.
     destruct args as [a [b []]]; simpl; go.
     iExists TT, _, _, (mk a (trim 64 (b + x))).
     go.
     erewrite recursive_mutex.update_eq; last done; cbn.
-    rewrite P.unlock; work.
+    work.
   Qed.
 
   cpp.spec "C::transfer(int)" as C_transfer_int from demo_cpp.source with
     (\this this
       \arg{x} "x" (Vint x)
       \prepost{γ q} this |-> CR γ q
       \prepost{q'} recursive_mutex.token γ.(recursive_mutex.lock_gname) q'
-      \pre{args th} recursive_mutex.acquireable γ th args (TT:=TT) (P this)
-      \post recursive_mutex.acquireable γ th (TT:=TT) (recursive_mutex.update (TT:=TT) (fun (a b : Z) => mk (trim 64 (a+x)) (trim 64 (b-x))) args) (P this)).
+      \pre{args th} recursive_mutex.acquireable γ th args (TT:=TT) (fun a b => this |-> CR' a b)
+      \post recursive_mutex.acquireable γ th (TT:=TT) (recursive_mutex.update (TT:=TT) (fun (a b : Z) => mk (trim 64 (a+x)) (trim 64 (b-x))) args) (fun a b => this |-> CR' a b)).
 
   Lemma transfer_ok : verify[source] "C::transfer(int)".
   Proof.
     verify_spec; go.
     iExists TT.
     go.
+    destruct args as [a[b []]]; simpl.
+    go.
     iExists TT.
     go.
     erewrite recursive_mutex.update_eq; last done; cbn.
-    destruct args as [a[b []]]; simpl.
     work.
   Qed.