Chore: move (and extend) mutex tests

rocq-brick-libstdcpp/proof/dune.inc

@@ -53,15 +53,6 @@
   	 (with-stderr-to inc_hpp.v.stderr (run cpp2v -v %{input} -o inc_hpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps inc.hpp))
 )
-(subdir mutex
- (rule
-  (targets test_cpp.v.stderr test_cpp.v)
-  (alias test_ast)
-  (deps (:input test.cpp) (glob_files_rec ../*.hpp) (universe))
-  (action
-  	 (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
- (alias (name srcs) (deps test.cpp))
-)
 (subdir new
  (rule
   (targets inc_new_cpp.v.stderr inc_new_cpp.v)

rocq-brick-libstdcpp/proof/mutex/inc.hpp

@@ -2,8 +2,3 @@
 
 template class std::lock_guard<std::mutex>;
 template class std::scoped_lock<std::mutex, std::mutex>;
-
-inline void foo() {
-  std::mutex m1, m2;
-  std::scoped_lock lock(m1, m2);
-}

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

@@ -1,3 +1,4 @@
 Require Export skylabs.brick.libstdcpp.mutex.spec.mutex.
 Require Export skylabs.brick.libstdcpp.mutex.spec.lock_guard.
 Require Export skylabs.brick.libstdcpp.mutex.spec.recursive_mutex.
+Require Export skylabs.brick.libstdcpp.mutex.spec.scoped_lock.

rocq-brick-libstdcpp/proof/mutex/spec/lock_guard.v

@@ -33,10 +33,15 @@ Module lock_guard.
   Fail #[only(cfractional,cfracvalid,ascfractional)] derive R.
 
   #[only(cfracvalid)] derive R.
+
 Section with_cpp.
   Context `{Σ : cpp_logic, σ : genv}.
   Context {HAS_THREADS : HasStdThreads Σ}.
 
+  #[global] Instance R_learn :
+    Cbn (Learn (learn_eq ==> any ==> learn_eq ==> learn_hints.fin) lock_guard.R) :=
+    ltac:(solve_learnable).
+
   Set Printing Coercions.
 
   Section with_R_cfrac'.

rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v

@@ -57,19 +57,6 @@ Module scoped_lock.
           mp1 |-> mutex.R g1 q1$m P1 ** mutex.token g1 q1 **
           mp2 |-> mutex.R g2 q2$m P2 ** mutex.token g2 q2
       ).
-
-      cpp.spec "foo()" as foo_spec from source with
-      (
-        \persist{thr} current_thread thr
-        \post emp
-      ).
-
-      Lemma foo_ok : verify[source] foo_spec.
-      Proof.
-        verify_spec; go.
-        iExists emp; go.
-        iExists emp; go.
-      Qed.
     End with_threads.
   End with_cpp.
 

rocq-brick-libstdcpp/test/dune.inc

@@ -80,6 +80,15 @@
   	 (with-stderr-to N6_print_sizeof_cpp.v.stderr (run cpp2v -v %{input} -o N6_print_sizeof_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps N6_print_sizeof.cpp))
 )
+(subdir mutex
+ (rule
+  (targets test_cpp.v.stderr test_cpp.v)
+  (alias test_ast)
+  (deps (:input test.cpp) (glob_files_rec ../*.hpp) (universe))
+  (action
+  	 (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps test.cpp))
+)
 (subdir new
  (rule
   (targets demo_cpp.v.stderr demo_cpp.v)

rocq-brick-libstdcpp/test/mutex/test.cpp

@@ -0,0 +1,21 @@
+#include <mutex>
+
+using namespace std;
+
+void test_mutex() {
+  std::mutex m;
+  m.lock();
+  m.unlock();
+}
+
+void test_lock_guard() {
+  std::mutex m;
+  {
+    std::lock_guard<std::mutex> lm(m);
+  }
+}
+
+void test_scoped_lock() {
+  std::mutex m1, m2;
+  std::scoped_lock lock(m1, m2);
+}

rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v

@@ -0,0 +1,32 @@
+Require Import skylabs.auto.cpp.prelude.proof.
+Require Import skylabs.brick.libstdcpp.mutex.spec.
+Require Import skylabs.brick.libstdcpp.test.mutex.test_cpp.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, σ : genv} {HAS_THREADS : HasStdThreads Σ}.
+
+  cpp.spec "test_mutex()" as test_mutex_spec from source with (\post emp).
+
+  Theorem test_mutex_ok : verify[source] "test_mutex()".
+  Proof.
+    verify_spec; go.
+    iExists emp; go.
+  Qed.
+
+  cpp.spec "test_lock_guard()" as test_lock_guard_spec from source with (\post emp).
+
+  Lemma test_lock_guard_ok : verify[source] "test_lock_guard()".
+  Proof.
+    verify_spec; go.
+    iExists emp; go.
+  Qed.
+
+  cpp.spec "test_scoped_lock()" as test_scoped_lock_spec from source with (\post emp).
+
+  Lemma test_scoped_lock_ok : verify[source] "test_scoped_lock()".
+  Proof.
+    verify_spec; go.
+    iExists emp; go.
+    iExists emp; go.
+  Qed.
+End with_cpp.