From 91bfb4db329f2e5be53cc738cad49ff98acf1f15 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Thu, 30 Apr 2026 20:17:56 +0200 Subject: [PATCH 1/4] lock_guard: add missing hint --- rocq-brick-libstdcpp/proof/mutex/spec/lock_guard.v | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/lock_guard.v b/rocq-brick-libstdcpp/proof/mutex/spec/lock_guard.v index e80a4bf..a395a1b 100644 --- a/rocq-brick-libstdcpp/proof/mutex/spec/lock_guard.v +++ b/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'. From f36cd996393b2bc53576dd1b670cf3fbcd8cb031 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Thu, 30 Apr 2026 18:15:56 +0200 Subject: [PATCH 2/4] mutex spec: export other specs --- rocq-brick-libstdcpp/proof/mutex/spec.v | 1 + 1 file changed, 1 insertion(+) diff --git a/rocq-brick-libstdcpp/proof/mutex/spec.v b/rocq-brick-libstdcpp/proof/mutex/spec.v index 86814ab..d07e1ae 100644 --- a/rocq-brick-libstdcpp/proof/mutex/spec.v +++ b/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. From dba1ddc2e107b2034d114683d1d9f0d0f6e262b6 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Thu, 30 Apr 2026 18:00:34 +0200 Subject: [PATCH 3/4] Move mutex tests --- rocq-brick-libstdcpp/proof/dune.inc | 9 ------ rocq-brick-libstdcpp/proof/mutex/inc.hpp | 5 ---- .../proof/mutex/spec/scoped_lock.v | 13 -------- rocq-brick-libstdcpp/proof/mutex/test.cpp | 16 ---------- .../proof/mutex/test_cpp_proof.v | 18 ----------- rocq-brick-libstdcpp/test/dune.inc | 9 ++++++ rocq-brick-libstdcpp/test/mutex/test.cpp | 21 +++++++++++++ .../test/mutex/test_cpp_proof.v | 30 +++++++++++++++++++ 8 files changed, 60 insertions(+), 61 deletions(-) delete mode 100644 rocq-brick-libstdcpp/proof/mutex/test.cpp delete mode 100644 rocq-brick-libstdcpp/proof/mutex/test_cpp_proof.v create mode 100644 rocq-brick-libstdcpp/test/mutex/test.cpp create mode 100644 rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v diff --git a/rocq-brick-libstdcpp/proof/dune.inc b/rocq-brick-libstdcpp/proof/dune.inc index e5f2d43..b1133fe 100644 --- a/rocq-brick-libstdcpp/proof/dune.inc +++ b/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) diff --git a/rocq-brick-libstdcpp/proof/mutex/inc.hpp b/rocq-brick-libstdcpp/proof/mutex/inc.hpp index 5f56386..ff041bd 100644 --- a/rocq-brick-libstdcpp/proof/mutex/inc.hpp +++ b/rocq-brick-libstdcpp/proof/mutex/inc.hpp @@ -2,8 +2,3 @@ template class std::lock_guard; template class std::scoped_lock; - -inline void foo() { - std::mutex m1, m2; - std::scoped_lock lock(m1, m2); -} diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v b/rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v index 5f42cc3..cd2c506 100644 --- a/rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v +++ b/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. diff --git a/rocq-brick-libstdcpp/proof/mutex/test.cpp b/rocq-brick-libstdcpp/proof/mutex/test.cpp deleted file mode 100644 index 6c32bb5..0000000 --- a/rocq-brick-libstdcpp/proof/mutex/test.cpp +++ /dev/null @@ -1,16 +0,0 @@ -#include "inc.hpp" - -using namespace std; - -void test() { - std::mutex m; - m.lock(); - m.unlock(); -} - -void test2() { - std::mutex m; - { - std::lock_guard lm(m); - } -} diff --git a/rocq-brick-libstdcpp/proof/mutex/test_cpp_proof.v b/rocq-brick-libstdcpp/proof/mutex/test_cpp_proof.v deleted file mode 100644 index 1e956c8..0000000 --- a/rocq-brick-libstdcpp/proof/mutex/test_cpp_proof.v +++ /dev/null @@ -1,18 +0,0 @@ -Require Import skylabs.auto.cpp.prelude.proof. -Require Import skylabs.brick.libstdcpp.mutex.test_cpp. -Require Import skylabs.brick.libstdcpp.mutex.spec. - -Section with_cpp. - Context `{Σ : cpp_logic} {HAS_THREADS : HasStdThreads Σ}. - Context `{MOD : test_cpp.source ⊧ σ}. (* σ is the whole program *) - - cpp.spec "test()" as test_spec with - (\post emp). - - Theorem test_ok : verify[source] test_spec. - Proof using HAS_THREADS. - verify_spec; go. - iExists emp; go. - Qed. - -End with_cpp. diff --git a/rocq-brick-libstdcpp/test/dune.inc b/rocq-brick-libstdcpp/test/dune.inc index 7e1c50a..916b195 100644 --- a/rocq-brick-libstdcpp/test/dune.inc +++ b/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) diff --git a/rocq-brick-libstdcpp/test/mutex/test.cpp b/rocq-brick-libstdcpp/test/mutex/test.cpp new file mode 100644 index 0000000..1ad08c5 --- /dev/null +++ b/rocq-brick-libstdcpp/test/mutex/test.cpp @@ -0,0 +1,21 @@ +#include + +using namespace std; + +void test_mutex() { + std::mutex m; + m.lock(); + m.unlock(); +} + +void test_lock_guard() { + std::mutex m; + { + std::lock_guard lm(m); + } +} + +void test_scoped_lock() { + std::mutex m1, m2; + std::scoped_lock lock(m1, m2); +} diff --git a/rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v b/rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v new file mode 100644 index 0000000..f78ee27 --- /dev/null +++ b/rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v @@ -0,0 +1,30 @@ +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} {HAS_THREADS : HasStdThreads Σ}. + Context `{MOD : test_cpp.source ⊧ σ}. (* σ is the whole program *) + + cpp.spec "test_mutex()" as test_mutex_spec with + (\post emp). + + Theorem test_mutex_ok : verify[source] "test_mutex()". + Proof using HAS_THREADS. + verify_spec; go. + iExists emp; go. + Qed. + + cpp.spec "test_scoped_lock()" as test_scoped_lock_spec from source with + ( + \persist{thr} current_thread thr + \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. From 67cb7d46762961c1d6abdb9d7697e68b6bebd3bb Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Thu, 30 Apr 2026 20:20:05 +0200 Subject: [PATCH 4/4] Revise mutex tests --- .../test/mutex/test_cpp_proof.v | 22 ++++++++++--------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v b/rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v index f78ee27..ffe7ef4 100644 --- a/rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v +++ b/rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v @@ -3,23 +3,25 @@ Require Import skylabs.brick.libstdcpp.mutex.spec. Require Import skylabs.brick.libstdcpp.test.mutex.test_cpp. Section with_cpp. - Context `{Σ : cpp_logic} {HAS_THREADS : HasStdThreads Σ}. - Context `{MOD : test_cpp.source ⊧ σ}. (* σ is the whole program *) + Context `{Σ : cpp_logic, σ : genv} {HAS_THREADS : HasStdThreads Σ}. - cpp.spec "test_mutex()" as test_mutex_spec with - (\post emp). + cpp.spec "test_mutex()" as test_mutex_spec from source with (\post emp). Theorem test_mutex_ok : verify[source] "test_mutex()". - Proof using HAS_THREADS. + 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 - ( - \persist{thr} current_thread thr - \post emp - ). + 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.