From 6839900026f230aaf0c2e3552e98b15fd402f45c Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Wed, 29 Apr 2026 18:53:30 +0200
Subject: [PATCH] scoped_lock proof sketch

---
 .../proof/mutex/proof/scoped_lock.v           | 37 +++++++++++++++++++
 1 file changed, 37 insertions(+)
 create mode 100644 rocq-brick-libstdcpp/proof/mutex/proof/scoped_lock.v

diff --git a/rocq-brick-libstdcpp/proof/mutex/proof/scoped_lock.v b/rocq-brick-libstdcpp/proof/mutex/proof/scoped_lock.v
new file mode 100644
index 00000000..0758ca02
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/mutex/proof/scoped_lock.v
@@ -0,0 +1,37 @@
+Require Import skylabs.auto.cpp.prelude.proof.
+Require Import skylabs.brick.libstdcpp.mutex.spec.scoped_lock.
+Require Import skylabs.brick.libstdcpp.mutex.spec.unique_lock.
+
+Require Import skylabs.brick.libstdcpp.mutex.inc_hpp.
+
+Import linearity.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, σ : genv}.
+  Context {HAS_THREADS : HasStdThreads Σ}.
+
+  Import scoped_lock.
+
+  cpp.spec "std::tie<...<std::mutex, std::mutex>>(std::mutex&, std::mutex&)" from source inline.
+  cpp.spec "std::tuple<...<std::mutex&, std::mutex&>>::tuple<1b, 1b>(std::mutex&, std::mutex&)" from source inline.
+  cpp.spec "std::lock<std::mutex, std::mutex, ...<>>(std::mutex&, std::mutex&)" from source inline.
+
+  Lemma ctor_ok : verify?[source] ctor_spec.
+  Proof.
+    verify_spec; go.
+    iExists _; go.
+    by rewrite left_id_L.
+  Qed.
+
+  Lemma dtor_ok : verify[source] dtor_spec.
+  Proof.
+    verify_spec.
+    rewrite !R.unlock.
+    go; try by ego.
+    iExists _; go.
+    rewrite !left_id_L.
+    go.
+  Qed.
+
+End with_cpp.
+