From 829109176fd8f649c90e457fa371fab708e1a75d Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Wed, 19 Aug 2026 20:11:42 +0200
Subject: [PATCH 01/14] Copy snapshot of atomic specs

---
 rocq-brick-libstdcpp/proof/atomic/inc_int.cpp |   2 +
 rocq-brick-libstdcpp/proof/atomic/pred.v      |  54 +++
 rocq-brick-libstdcpp/proof/atomic/spec.v      | 357 ++++++++++++++++++
 rocq-brick-libstdcpp/proof/atomic/test.cpp    |  99 +++++
 .../proof/atomic/test_cpp_proof.v             | 226 +++++++++++
 5 files changed, 738 insertions(+)
 create mode 100644 rocq-brick-libstdcpp/proof/atomic/inc_int.cpp
 create mode 100644 rocq-brick-libstdcpp/proof/atomic/pred.v
 create mode 100644 rocq-brick-libstdcpp/proof/atomic/spec.v
 create mode 100644 rocq-brick-libstdcpp/proof/atomic/test.cpp
 create mode 100644 rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v

diff --git a/rocq-brick-libstdcpp/proof/atomic/inc_int.cpp b/rocq-brick-libstdcpp/proof/atomic/inc_int.cpp
new file mode 100644
index 00000000..fd52b45e
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/atomic/inc_int.cpp
@@ -0,0 +1,2 @@
+#include <atomic>
+template<> class std::atomic<int>;
diff --git a/rocq-brick-libstdcpp/proof/atomic/pred.v b/rocq-brick-libstdcpp/proof/atomic/pred.v
new file mode 100644
index 00000000..ddf95972
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/atomic/pred.v
@@ -0,0 +1,54 @@
+(**
+ * Copyright (C) 2025 SkyLabs AI, Inc.
+ * All rights reserved.
+ *
+ * SPDX-License-Identifier: LGPL-2.1 WITH BlueRock Exception for use over network, see repository root for details.
+ *)
+Require Import skylabs.auto.cpp.spec.
+Require Import skylabs.cpp.spec.concepts.
+Require skylabs.cpp.stdlib.atomic.inc_int_cpp.
+
+Require Import skylabs.cpp.spec.concepts.
+
+(** * Interface to Atomic<T> *)
+(**
+These specifications assume that all memory order parameters (template,
+function arguments) are _SEQ_CST. In the C++ code, redefine the other
+memory order macros to __ATOMIC_SEQ_CST.
+*)
+
+cpp.enum "std::memory_order" from (inc_int_cpp.source) variant.
+#[global] Notation Tmemory_order := {%cpp_type[inc_int_cpp.source] "std::memory_order"} (only parsing).
+
+Module Type ATOMIC_PREDS.
+
+  (** Type [t] indexing our spec models the type name T in Atomic<T>. *)
+
+  (** The type where the actual methods are implemented *)
+  #[global] Notation base_name ty :=
+    (Ninst "std::__1::__atomic_base" [Atype ty; Avalue (Eint 0 Tbool)]).
+  #[global] Notation base_name1 ty :=
+    (Ninst "std::__1::__atomic_base" [Atype ty; Avalue (Eint 1 Tbool)]).
+  (** The type <<std::atomic<T>>> *)
+  #[global] Notation class_name ty := (Ninst "std::__1::atomic" [Atype ty]).
+  #[global] Notation T ty := (Tnamed (class_name ty)).
+
+  (** Abstract predicates *)
+
+  (** Fraction [q] ownership of atomically accessible value [v]. *)
+  Parameter R : ∀ `{Σ : cpp_logic} {σ : genv} (ty : type) `{PV : @PrimVal ty A} (q : cQp.t) (x : A), Rep.
+
+  Section R_props.
+    Context `{Σ : cpp_logic} {σ : genv} `{PV : @PrimVal ty A}.
+    Notation R := (R ty (PV:=PV)).
+
+    #[global] Declare Instance R_frac : CFractional1 R.
+    #[global] Declare Instance R_timeless : Timeless2 R.
+    #[global] Declare Instance R_frac_valid : CFracValid1 R.
+    #[global] Declare Instance R_agree : Cbn (Learn (any ==> learn_eq ==> learn_hints.fin) R).
+    #[global] Declare Instance R_type : Typed2 (class_name ty) R.
+  End R_props.
+
+End ATOMIC_PREDS.
+
+Declare Module atomic : ATOMIC_PREDS.
diff --git a/rocq-brick-libstdcpp/proof/atomic/spec.v b/rocq-brick-libstdcpp/proof/atomic/spec.v
new file mode 100644
index 00000000..b7a83714
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/atomic/spec.v
@@ -0,0 +1,357 @@
+(**
+ * Copyright (C) 2025 SkyLabs AI, Inc.
+ * All rights reserved.
+ *
+ * SPDX-License-Identifier: LGPL-2.1 WITH BlueRock Exception for use over network, see repository root for details.
+ *)
+Require Import skylabs.auto.cpp.spec.
+Require Import skylabs.cpp.spec.concepts.
+Require Import skylabs.cpp.stdlib.atomic.inc_int_cpp.
+
+Require Import skylabs.cpp.spec.concepts.
+Require Export skylabs.cpp.stdlib.atomic.pred.
+
+Module atomic_specs (Import atomic : ATOMIC_PREDS).
+
+  #[global] Hint Opaque R : sl_opacity.
+
+  Section spec.
+    Context `{Σ : cpp_logic} {σ : genv}.
+    Context (ty : type).
+    Context `{!PrimVal ty A,!DefaultValue ty A}.
+    Notation s := (class_name ty) (only parsing).	(** [Atomic<T>] *)
+    Notation b0 := (base_name ty) (only parsing).
+    Notation b1 := (base_name1 ty) (only parsing).
+    Notation R := (R ty).
+    Notation bR q v := (_derived b0 b1 ,, _derived b1 s |-> R q%cQp v) (only parsing).
+
+    Definition default_ctor : mpred :=
+      specify.template.ctor s [] $
+        \this this
+        \post this |-> R 1$m (default_val ty).
+    #[global] Hint Opaque default_ctor : sl_opacity.
+    #[global] Arguments default_ctor : simpl never.
+    Definition SpecFor_default_ctor := RegisterSpec default_ctor.
+    #[global] Existing Instance SpecFor_default_ctor.
+
+    Definition ctor : mpred :=
+      specify.template.ctor s [ty] $
+        \this this
+        \arg{n} "v" (Vinj ty n)
+        \post this |-> R 1$m n.
+    #[global] Hint Opaque ctor : sl_opacity.
+    #[global] Arguments ctor : simpl never.
+    Definition SpecFor_ctor := RegisterSpec ctor.
+    #[global] Existing Instance SpecFor_ctor.
+
+    Definition dtor : mpred :=
+      specify.template.dtor s $
+        \this this
+        \pre{n} this |-> R 1$m n
+        \post emp.
+    #[global] Hint Opaque dtor : sl_opacity.
+    #[global] Arguments dtor : simpl never.
+    Definition SpecFor_dtor := RegisterSpec dtor.
+    #[global] Existing Instance SpecFor_dtor.
+
+    (** *** <<load>> & <<store>> *)
+    Definition do_load (this : ptr) (K : A -> mpred) : mpred :=
+      AR1 << ∃∃ n q, this |-> bR q n >> @ top, empty << K n >>.
+    #[global] Hint Opaque do_load : typeclass_instances sl_opacity.
+
+    Definition load : mpred :=
+      specify.template.method b0 "load" function_qualifiers.N ty [Tmemory_order] $
+        \this this
+        \arg "mo" (memory_order.to_val memory_order.seq_cst)
+        \pre{K} do_load this K
+        \post{n}[Vinj ty n] K n.
+    #[global] Hint Opaque load : sl_opacity.
+    #[global] Arguments load : simpl never.
+    Definition SpecFor_load := RegisterSpec load.
+    #[global] Existing Instance SpecFor_load.
+
+    Definition load_const : mpred :=
+      specify.template.method b0 "load" function_qualifiers.Nc ty [Tmemory_order] $
+        \this this
+        \arg "mo" (memory_order.to_val memory_order.seq_cst)
+        \pre{K} do_load this K
+        \post{n}[Vinj ty n] K n.
+    #[global] Hint Opaque load_const : sl_opacity.
+    #[global] Arguments load_const : simpl never.
+    Definition SpecFor_load_const := RegisterSpec load_const.
+    #[global] Existing Instance SpecFor_load_const.
+
+    Definition do_store (this : ptr) (n : A) (K : mpred) : mpred :=
+      AC1 << ∀ m, this |-> bR 1$m m >> @ top, empty
+          << this |-> bR 1$m n, COMM K >>.
+    #[global] Hint Opaque do_store : typeclass_instances sl_opacity.
+
+    Definition store : mpred :=
+      specify.template.method b0 "store" function_qualifiers.N Tvoid [ty; Tmemory_order] $
+        \this this
+        \arg{n} "v" (Vinj ty n)
+        \arg "mo" (memory_order.to_val memory_order.seq_cst)
+        \pre{K} do_store this n K
+        \post K.
+    #[global] Hint Opaque store : sl_opacity.
+    #[global] Arguments store : simpl never.
+    Definition SpecFor_store := RegisterSpec store.
+    #[global] Existing Instance SpecFor_store.
+
+    (** *** <<operator=>> *)
+    Definition assign : mpred :=
+      specify.template.op b0 OOEqual function_qualifiers.N ty [ty] $
+        \this this
+        \arg{n} "v" (Vinj ty n)
+        \pre{K} do_store this n K
+        \post[Vinj ty n] K.
+    #[global] Hint Opaque assign : sl_opacity.
+    #[global] Arguments assign : simpl never.
+    Definition SpecFor_assign := RegisterSpec assign.
+    #[global] Existing Instance SpecFor_assign.
+
+    (** *** <<operator ty>> *)
+    Definition cast : mpred :=
+      specify.template.conv b0 ty function_qualifiers.Nc $
+        \this this
+        \pre{K} do_load this K
+        \post{n}[Vinj ty n] K n.
+    #[global] Hint Opaque cast : sl_opacity.
+    #[global] Arguments cast : simpl never.
+    Definition SpecFor_cast := RegisterSpec cast.
+    #[global] Existing Instance SpecFor_cast.
+
+    (** *** <<exchange>> *)
+    Definition do_exchange (this : ptr) (n : A) (K : A -> mpred) : mpred :=
+      AU1 << ∀ m, this |-> bR 1$m m >> @ top, empty
+          <<      this |-> bR 1$m n, COMM K m >>.
+    #[global] Hint Opaque do_exchange : typeclass_instances sl_opacity.
+
+    Definition exchange : mpred :=
+      specify.template.method b0 "exchange" function_qualifiers.N ty
+          [ty; Tmemory_order] $
+        \this this
+        \arg{desired} "desired" (Vinj ty desired)
+        \arg "mo" (memory_order.to_val memory_order.seq_cst)
+        \pre{K} do_exchange this desired K
+        \post{m}[Vinj ty m] K m.
+    #[global] Hint Opaque exchange : sl_opacity.
+    #[global] Arguments exchange : simpl never.
+    Definition SpecFor_exchange := RegisterSpec exchange.
+    #[global] Existing Instance SpecFor_exchange.
+
+    (** *** <<compare_exchange_weak>> & <<compare_exchange_strong>> *)
+    Definition do_compare_exchange (weak : bool) (this expected_p : ptr) (expected desired : A)
+        (K : bool -> mpred) : mpred :=
+      AU1 << ∀ cur, this |-> bR 1$m cur >> @ top, empty
+        << ∃ success m',
+          [| if weak then (* lifting the test on [weak] is probably a bit easier to work with *)
+               (success = true /\ cur = expected /\ m' = desired) \/
+               (success = false /\ m' = cur)
+             else
+               (success = true /\ cur = expected /\ m' = desired) \/
+               (success = false /\ cur <> expected /\ m' = cur)
+          |] **
+          this |-> bR 1$m m',
+        COMM
+          expected_p |-> primR ty 1$m (Vinj ty cur) -*
+          K success
+        >>.
+    #[global] Hint Opaque do_compare_exchange : typeclass_instances sl_opacity.
+
+    (** NOTE: the difference between the following two specs is not immediately obvious. *)
+    Definition compare_exchange_strong : mpred :=
+      specify.template.method b0 "compare_exchange_strong" function_qualifiers.N "bool"
+          [Tref ty; ty; Tmemory_order; Tmemory_order] $
+        \this this
+        \arg{expected_p} "o" (Vref expected_p)
+        \arg{desired} "n" (Vinj ty desired)
+        \arg "mo_success" (memory_order.to_val memory_order.seq_cst)
+        \arg "mo_failure" (memory_order.to_val memory_order.seq_cst)
+        \pre{expected} expected_p |-> primR ty 1$m (Vinj ty expected)
+        \pre{K} do_compare_exchange false this expected_p expected desired K
+        \post{b}[Vbool b] K b.
+    #[global] Hint Opaque compare_exchange_strong : sl_opacity.
+    #[global] Arguments compare_exchange_strong : simpl never.
+    Definition SpecFor_compare_exchange_strong := RegisterSpec compare_exchange_strong.
+    #[global] Existing Instance SpecFor_compare_exchange_strong.
+
+    Definition compare_exchange_strong_1 : mpred :=
+      specify.template.method b0 "compare_exchange_strong" function_qualifiers.N "bool"
+        [Tref ty; ty; Tmemory_order] $
+        \this this
+        \arg{expected_p} "o" (Vref expected_p)
+        \arg{desired} "n" (Vinj ty desired)
+        \arg "mo" (memory_order.to_val memory_order.seq_cst)
+        \pre{expected} expected_p |-> primR ty 1$m (Vinj ty expected)
+        \pre{K} do_compare_exchange false this expected_p expected desired K
+        \post{b}[Vbool b] K b.
+    #[global] Hint Opaque compare_exchange_strong_1 : sl_opacity.
+    #[global] Arguments compare_exchange_strong_1 : simpl never.
+    Definition SpecFor_compare_exchange_strong_1 := RegisterSpec compare_exchange_strong_1.
+    #[global] Existing Instance SpecFor_compare_exchange_strong_1.
+
+    Definition compare_exchange_weak : mpred :=
+      specify.template.method b0 "compare_exchange_weak" function_qualifiers.N "bool"
+        [Tref ty; ty; Tmemory_order; Tmemory_order] $
+        \this this
+        \arg{expected_p} "o" (Vref expected_p)
+        \arg{desired} "n" (Vinj ty desired)
+        \arg "mo_success" (memory_order.to_val memory_order.seq_cst)
+        \arg "mo_failure" (memory_order.to_val memory_order.seq_cst)
+        \pre{expected} expected_p |-> primR ty 1$m (Vinj ty expected)
+        \pre{K} do_compare_exchange true this expected_p expected desired K
+        \post{b}[Vbool b] K b.
+    #[global] Hint Opaque compare_exchange_weak : sl_opacity.
+    #[global] Arguments compare_exchange_weak : simpl never.
+    Definition SpecFor_compare_exchange_weak := RegisterSpec compare_exchange_weak.
+    #[global] Existing Instance SpecFor_compare_exchange_weak.
+
+    Definition compare_exchange_weak_1 : mpred :=
+      specify.template.method b0 "compare_exchange_weak" function_qualifiers.N "bool"
+        [Tref ty; ty; Tmemory_order] $
+        \this this
+        \arg{expected_p} "o" (Vref expected_p)
+        \arg{desired} "n" (Vinj ty desired)
+        \arg "mo" (memory_order.to_val memory_order.seq_cst)
+        \pre{expected} expected_p |-> primR ty 1$m (Vinj ty expected)
+        \pre{K} do_compare_exchange true this expected_p expected desired K
+        \post{b}[Vbool b] K b.
+    #[global] Hint Opaque compare_exchange_weak_1 : sl_opacity.
+    #[global] Arguments compare_exchange_weak_1 : simpl never.
+    Definition SpecFor_compare_exchange_weak_1 := RegisterSpec compare_exchange_weak_1.
+    #[global] Existing Instance SpecFor_compare_exchange_weak_1.
+
+  End spec.
+
+  Section bundled_spec.
+    Context `{Σ : cpp_logic} {σ : genv}.
+    Context (ty : type).
+    Context `{!PrimVal ty A,!DefaultValue ty A}.
+
+    Definition specs :=
+      ctor ty **
+      default_ctor ty **
+      dtor ty **
+      load ty **
+      load_const ty **
+      store ty    **
+      assign ty   **
+      cast ty     **
+      exchange ty **
+      compare_exchange_strong ty **
+      compare_exchange_strong_1 ty **
+      compare_exchange_weak ty **
+      compare_exchange_weak_1 ty.
+  End bundled_spec.
+
+  Class UnOp (ty : type) (A : Type) (op_name : OverloadableOperator) :=
+  { atomic_un_op : A -> A
+  }.
+
+  Class BinOp (ty1 ty2 : type) (A B : Type) (op_name : OverloadableOperator) (fun_name : ident) :=
+  { atomic_bin_op : A -> B -> A
+  }.
+
+  Section with_ty.
+    Context `{Σ : cpp_logic} {σ : genv}.
+    Context (ty : type).
+    Context `{PrimVal ty A}.
+
+    #[local] Notation s := (class_name ty) (only parsing).	(** [Atomic<T>] *)
+    #[local] Notation b1 := (base_name1 ty) (only parsing).
+    #[local] Notation bR q v := (_derived b1 s |-> R ty q v) (only parsing).
+
+    (** Apply operation [op] to the atomic cell pointed by [this],
+    and return the old contents to continuation [K]. *)
+    #[local] Definition do_op (op : A -> A) (this : ptr) (K : A -> mpred) : mpred :=
+      AC1 << ∀ m, this |-> bR 1$m m >> @ top, empty
+          << this |-> bR 1$m (op m), COMM K m >>.
+    #[global] Hint Opaque do_op : typeclass_instances sl_opacity.
+
+    Section with_unop.
+      Context `{!UnOp ty A op_name}.
+
+      (** Triple for unary operators that return the new value *)
+      Definition unop_fetch : mpred :=
+        specify.template.op b1 op_name function_qualifiers.N ty [] $
+          \this this
+          \pre{K} do_op atomic_un_op this K
+          \post{m}[Vinj ty (atomic_un_op m)] K m.
+
+      #[global] Hint Opaque unop_fetch : sl_opacity.
+      #[global] Arguments unop_fetch : simpl never.
+      Definition SpecFor_unop_fetch := RegisterSpec unop_fetch.
+      #[global] Existing Instance SpecFor_unop_fetch.
+
+      (** Triple for unary operators that return the old value *)
+      Definition fetch_unop : mpred :=
+        specify.template.op b1 op_name function_qualifiers.N ty [Tint] $
+          \this this
+          \arg{dummy} "dummy" (Vint dummy)
+          \pre{K} do_op atomic_un_op this K
+          \post{m}[Vinj ty m] K m.
+
+      #[global] Hint Opaque fetch_unop : sl_opacity.
+      #[global] Arguments fetch_unop : simpl never.
+      Definition SpecFor_fetch_unop := RegisterSpec fetch_unop.
+      #[global] Existing Instance SpecFor_fetch_unop.
+    End with_unop.
+
+    Section with_binop.
+      Context `{!BinOp ty tyM A B op_name fun_name}.
+      Context `{!PrimVal tyM B}.
+
+      (** Triple for binary operators that return the new value *)
+      Definition binop_fetch : mpred :=
+        specify.template.op b1 op_name function_qualifiers.N ty [tyM] $
+          \this this
+          \arg{n : B} "v" (Vinj tyM n)
+          \pre{K} do_op (flip atomic_bin_op n) this K
+          \post{m}[Vinj ty (atomic_bin_op m n)] K m.
+      #[global] Hint Opaque binop_fetch : sl_opacity.
+      #[global] Arguments binop_fetch : simpl never.
+      Definition SpecFor_binop_fetch := RegisterSpec binop_fetch.
+      #[global] Existing Instance SpecFor_binop_fetch.
+
+      (** Triple for methods that return the old value *)
+      Definition fetch_binop : mpred :=
+        specify.template.method b1 fun_name function_qualifiers.N ty [tyM; Tmemory_order] $
+          \this this
+          \arg{n : B} "v" (Vinj tyM n)
+          \arg "mo" (memory_order.to_val memory_order.seq_cst)
+          \pre{K} do_op (flip atomic_bin_op n) this K
+          \post{m}[Vinj ty m] K m.
+      #[global] Hint Opaque fetch_binop : sl_opacity.
+      #[global] Arguments fetch_binop : simpl never.
+      Definition SpecFor_fetch_binop := RegisterSpec fetch_binop.
+      #[global] Existing Instance SpecFor_fetch_binop.
+    End with_binop.
+  End with_ty.
+
+  (** TODO fix overflow handling. *)
+  Definition add_raw (sz : int_rank.t) (sgn : signed) (a b : Z) : Z :=
+    if sgn is Signed then to_signed (int_rank.bitsize sz) (a + b)
+    else to_unsigned (int_rank.bitsize sz) (a + b).
+
+  #[global] Instance num_add {sz sgn} :
+    BinOp (Tnum sz sgn) (Tnum sz sgn) Z Z OOPlusEqual "fetch_add" :=
+  {| atomic_bin_op := add_raw sz sgn |}.
+  (* TODO character types? *)
+
+  (** TODO fix overflow handling. *)
+  #[global] Instance num_sub {sz sgn} :
+    BinOp (Tnum sz sgn) (Tnum sz sgn) Z Z OOMinusEqual "fetch_sub" :=
+  {| atomic_bin_op a b := add_raw sz sgn a (-b) |}.
+
+  #[global] Instance ptr_add {σ : genv} {ty} :
+    BinOp (Tptr ty) Tptrdiff_t ptr Z OOPlusEqual "fetch_add" :=
+  {| atomic_bin_op (p : ptr) b := p .[ ty ! b ] |}.
+
+  #[global] Instance ptr_sub {σ : genv} {ty} :
+    BinOp (Tptr ty) Tptrdiff_t ptr Z OOMinusEqual "fetch_sub" :=
+  {| atomic_bin_op (p : ptr) b := p .[ ty ! -b ] |}.
+
+End atomic_specs.
+
+Include (atomic_specs atomic).
diff --git a/rocq-brick-libstdcpp/proof/atomic/test.cpp b/rocq-brick-libstdcpp/proof/atomic/test.cpp
new file mode 100644
index 00000000..8578b703
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/atomic/test.cpp
@@ -0,0 +1,99 @@
+/**
+ * Copyright (C) 2025 BlueRock Security, Inc.
+ * All rights reserved.
+ *
+ * SPDX-License-Identifier: LGPL-2.1 WITH BlueRock Exception for use over network, see repository root for details.
+ */
+#include <atomic>
+#include <cassert>
+
+using namespace std;
+
+void
+test(bool b, const char* msg = nullptr) {
+    assert(b);
+}
+
+void
+TestDefaultConstructor() {
+    std::atomic<int> atomicInt;
+    test(atomicInt.load() == 0);
+}
+
+void
+TestParameterizedConstructor() {
+    int initialValue = 10;
+    std::atomic<int> atomicInt(initialValue);
+    test(atomicInt.load() == initialValue);
+}
+
+void
+TestLoad() {
+    std::atomic<int> atomicInt(42);
+    test(42 == atomicInt.load());
+    test(42 == atomicInt);
+}
+
+void
+TestStore() {
+    std::atomic<int> atomicInt;
+    atomicInt.store(25);
+    test(atomicInt.load() == 25);
+}
+
+void
+TestCAS() {
+    std::atomic<int> atomicInt{57};
+    int var = 13;
+    atomicInt.compare_exchange_strong(var, 25);
+    test(var == 57);
+    test(atomicInt.load() == 57);
+    var = 57;
+    atomicInt.compare_exchange_strong(var, 25);
+    test(var == 57);
+    test(atomicInt.load() == 25);
+    test(25 == atomicInt.exchange(13));
+    test(atomicInt.load() == 13);
+}
+
+void
+TestArith() {
+    std::atomic<int> atomicInt{57};
+    assert(60 == (atomicInt += 3));
+    assert(60 == atomicInt.load());
+}
+
+void
+TestFetchAdd() {
+    std::atomic<int> atomicInt{10};
+    assert(10 == atomicInt.fetch_add(1));
+    assert(11 == atomicInt.load());
+    assert(11 == atomicInt.fetch_add(1));
+    assert(12 == atomicInt);
+    assert(12 == atomicInt++);
+    assert(13 == atomicInt);
+    assert(14 == ++atomicInt);
+    assert(19 == (atomicInt += 5));
+
+    int x[11] = {0};
+    std::atomic<int*> atomicPtr{x};
+    assert(x == atomicPtr.fetch_add(1));
+    assert(x+1 == atomicPtr.load());
+    assert(x+1 == atomicPtr.fetch_add(1));
+    assert(x+2 == atomicPtr);
+    assert(x+2 == atomicPtr++);
+    assert(x+3 == atomicPtr);
+    assert(x+4 == ++atomicPtr);
+    assert(x+9 == (atomicPtr += 5));
+}
+
+int
+main() {
+    TestDefaultConstructor();
+    TestParameterizedConstructor();
+    TestLoad();
+    TestStore();
+    TestCAS();
+    TestArith();
+    return 0;
+}
diff --git a/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v b/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v
new file mode 100644
index 00000000..db2006fb
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v
@@ -0,0 +1,226 @@
+(**
+ * Copyright (C) 2025 SkyLabs AI, Inc.
+ * All rights reserved.
+ *
+ * SPDX-License-Identifier: LGPL-2.1 WITH BlueRock Exception for use over network, see repository root for details.
+ *)
+Require Import skylabs.auto.cpp.proof.
+Require Import skylabs.cpp.stdlib.cassert.spec.
+Require Import skylabs.cpp.stdlib.atomic.spec.
+Require Import skylabs.cpp.stdlib.test.atomic.test_cpp.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, σ : genv}.
+
+  Notation GLOBALS q := (_global "std::__1::memory_order_seq_cst" |-> primR "enum std::__1::memory_order" q 5).
+
+  Section specs.
+    Context `{MOD : test_cpp.source ⊧ σ}.
+
+    cpp.spec "test(bool, const char*)" as test_spec with
+      (\arg "b" (Vbool true)
+       \arg{p} "" (Vptr p)
+       \post emp).
+
+    cpp.spec "TestDefaultConstructor()" as test_default_ctor with
+        (\prepost{q} GLOBALS q
+         \post emp).
+
+    cpp.spec "TestParameterizedConstructor()" as test_parameterized_ctor with
+        (\prepost{q} GLOBALS q
+         \post emp).
+
+    cpp.spec "TestLoad()" as test_load with
+        (\prepost{q} GLOBALS q
+         \post emp).
+
+    cpp.spec "TestStore()" as test_store with
+        (\prepost{q} GLOBALS q
+         \post emp).
+
+    cpp.spec "TestCAS()" as test_cas with
+        (\prepost{q} GLOBALS q
+         \post emp).
+
+    cpp.spec "TestArith()" as test_arith with
+        (\prepost{q} GLOBALS q
+         \post emp).
+
+    cpp.spec "TestFetchAdd()" as test_fetch_add with
+        (\prepost{q} GLOBALS q
+         \post emp).
+
+    cpp.spec "main()" as main with
+        (\prepost{q} GLOBALS q
+         \post[Vint 0] emp).
+
+    Definition specs :=
+      test_default_ctor **
+      test_parameterized_ctor **
+      test_load **
+      test_store **
+      test_cas **
+      test_arith.
+    #[global] Hint Opaque specs : sl_opacity.
+
+  End specs.
+
+  #[local] Hint Resolve fractional.UNSAFE_read_prim_cancel : sl_opacity.
+
+  Notation BASE p := (p ,, _base "std::__1::atomic<int>" "std::__1::__atomic_base<int, 1b>" ,, _base "std::__1::__atomic_base<int, 1b>" "std::__1::__atomic_base<int, 0b>").
+
+  Notation BASE1 p := (p ,, _base "std::__1::atomic<int>" "std::__1::__atomic_base<int, 1b>").
+
+  #[program]
+  Definition do_load_C (p : ptr) :=
+    \cancelx
+    \using denoteModule test_cpp.source
+    \consuming{q (n : Z)} p |-> atomic.R "int" q n
+    \proving{(K : Z -> mpred) (_ : IsExistential K)} do_load Tint (BASE p) K
+    \instantiate K := (fun x : Z => p |-> atomic.R "int" q n ** [| x = n |])
+    \end@{mpredI}.
+  Next Obligation.
+    intros. iIntros "[#M ?]" (?? ->).
+    iDestruct (observe [| _ ⊧ _ |] with "M") as "%".
+    rewrite /do_load.
+    iAcIntro. rewrite /commit_acc.
+    iDestruct (fupd_mask_subseteq) as ">Y"; [ | iModIntro ]; eauto.
+    work; normalize_ptrs.
+    work. iExists q. work.
+    iMod "Y". iModIntro.
+    normalize_ptrs. work.
+  Qed.
+  #[program]
+  Definition do_store_C (p : ptr) :=
+    \cancelx
+    \using denoteModule test_cpp.source
+    \consuming{(n : Z)} p |-> atomic.R "int" 1$m n
+    \proving{K (_ : IsExistential K) v} do_store Tint (BASE p) v K
+    \instantiate K := (p |-> atomic.R "int" 1$m v)
+    \end@{mpredI}.
+  Next Obligation.
+    intros. iIntros "[#M ?]" (??? ->).
+    iDestruct (observe [| _ ⊧ _ |] with "M") as "%".
+    rewrite /do_load.
+    iAcIntro. rewrite /commit_acc.
+    iDestruct (fupd_mask_subseteq) as ">Y"; [ | iModIntro ]; eauto.
+    work; normalize_ptrs.
+    work.
+    iMod "Y". iModIntro.
+    normalize_ptrs. work.
+  Qed.
+  (* TODO: this is not the most general hint *)
+  #[program]
+  Definition do_compare_exchange_C (p p' : ptr) old new :=
+    \cancelx
+    \using (denoteModule test_cpp.source : mpred)
+    \consuming{n} p |-> atomic.R "int" 1$m (n : Z)
+    \proving{K (_ : IsExistential K)}
+      do_compare_exchange "int" false (BASE p) p' old new K
+    \instantiate K := (fun res =>
+                         if bool_decide (n = old) then
+                           p |-> atomic.R "int" 1$m new **
+                           p' |-> primR "int" 1$m old ** [| res = true |]
+                         else
+                           p |-> atomic.R "int" 1$m n **
+                           p' |-> primR "int" 1$m n ** [| res = false |])
+    \end@{mpredI}.
+  Next Obligation.
+    intros. iIntros "[#M ?]" (?? ->).
+    iDestruct (observe [| _ ⊧ _ |] with "M") as "%".
+    rewrite /do_compare_exchange.
+    iAuIntro1. rewrite /atomic1_acc.
+    iDestruct (fupd_mask_subseteq) as ">Y"; [ | iModIntro ]; eauto.
+    work. normalize_ptrs. work.
+    { iMod "Y". iModIntro. normalize_ptrs. work. }
+    { iMod "Y"; iModIntro. normalize_ptrs. work.
+      case_bool_decide.
+      { subst. lazymatch goal with H : _ \/ _ |- _ => destruct H end. intuition. work.
+        exfalso; tauto. }
+      { lazymatch goal with H : _ \/ _ |- _ => destruct H end; try by exfalso; tauto.
+        intuition; subst. work. } }
+  Qed.
+  #[program]
+  Definition do_exchange_C (p : ptr) new :=
+    \cancelx
+    \using denoteModule test_cpp.source
+    \consuming{n} p |-> atomic.R "int" 1$m n
+    \proving{K (_ : IsExistential K)}
+      do_exchange "int" (BASE p) new K
+    \instantiate K := (fun res => [| res = n |] **
+                         p |-> atomic.R "int" 1$m new)
+    \end@{mpredI}.
+  Next Obligation.
+    intros. iIntros "[#M ?]" (?? ->).
+    iDestruct (observe [| _ ⊧ _ |] with "M") as "%".
+    rewrite /do_compare_exchange.
+    iAuIntro1. rewrite /atomic1_acc.
+    iDestruct (fupd_mask_subseteq) as ">Y"; [ | iModIntro ]; eauto.
+    work. normalize_ptrs. work.
+    { iMod "Y". iModIntro. normalize_ptrs. work. }
+    { iMod "Y"; iModIntro. normalize_ptrs. work. }
+  Qed.
+
+  #[program]
+  Definition do_op_C (p : ptr) (op : Z -> Z) :=
+    \cancelx
+    \using denoteModule test_cpp.source
+    \consuming{n} p |-> atomic.R "int" 1$m n
+    \proving{K (_ : IsExistential K)}
+      spec.do_op "int" op (BASE1 p) K
+    \instantiate K := (fun res => [| res = n |] **
+                               p |-> atomic.R "int" 1$m (op n))
+    \end@{mpredI}.
+  Next Obligation.
+    intros. iIntros "[#M ?]" (?? ->).
+    iDestruct (observe [| _ ⊧ _ |] with "M") as "%".
+    rewrite /spec.do_op.
+    iAcIntro. rewrite /commit_acc.
+    iDestruct (fupd_mask_subseteq) as ">Y"; [ | iModIntro ]; eauto.
+    work.
+    iMod "Y"; iModIntro; work.
+  Qed.
+
+  Hint Resolve do_compare_exchange_C do_exchange_C : sl_opacity.
+  Hint Resolve do_load_C do_store_C : sl_opacity.
+  Hint Resolve do_op_C : sl_opacity.
+
+  Notation OK spec :=
+    (verify?[test_cpp.source] spec) (only parsing).
+
+  Set Typeclasses Debug.
+  Goal SpecFor source "std::__1::atomic<int*>::fetch_add(long, enum std::__1::memory_order)"%cpp_name.
+  Fail apply _.
+  About SpecFor_fetch_binop.
+  Check (SpecFor_fetch_binop "int*").
+  class_apply (SpecFor_fetch_binop "int*").
+  Goal SpecFor source "std::__1::__atomic_base<int, 1b>::operator++(int)".
+  apply _.
+
+  Lemma arith_ok : OK test_fetch_add.
+  Proof. verify_spec. go.
+
+  Qed.
+
+  Lemma cas_ok : OK test_cas.
+  Proof. verify_spec. go. Qed.
+
+  Lemma default_ctor_ok : OK test_default_ctor.
+  Proof. verify_spec; go. Qed.
+
+  Lemma param_ctor_ok : OK test_parameterized_ctor.
+  Proof. verify_spec; go. Qed.
+
+  Lemma load_ok : OK test_load.
+  Proof. verify_spec; go. Qed.
+
+  Lemma store_ok : OK test_store.
+  Proof. verify_spec; go. Qed.
+
+  Lemma main_ok : OK main.
+  Proof.
+    rewrite /specs.
+    verify_spec. go.
+  Qed.
+
+End with_cpp.

From 189175f0599362cda8c81a1ffc52946bd3267054 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Wed, 19 Aug 2026 20:16:44 +0200
Subject: [PATCH 02/14] Notation -> Abbreviation

---
 rocq-brick-libstdcpp/proof/atomic/pred.v         | 12 ++++++------
 rocq-brick-libstdcpp/proof/atomic/spec.v         | 16 ++++++++--------
 .../proof/atomic/test_cpp_proof.v                |  8 ++++----
 3 files changed, 18 insertions(+), 18 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/atomic/pred.v b/rocq-brick-libstdcpp/proof/atomic/pred.v
index ddf95972..0cb14603 100644
--- a/rocq-brick-libstdcpp/proof/atomic/pred.v
+++ b/rocq-brick-libstdcpp/proof/atomic/pred.v
@@ -18,20 +18,20 @@ memory order macros to __ATOMIC_SEQ_CST.
 *)
 
 cpp.enum "std::memory_order" from (inc_int_cpp.source) variant.
-#[global] Notation Tmemory_order := {%cpp_type[inc_int_cpp.source] "std::memory_order"} (only parsing).
+#[global] Abbreviation Tmemory_order := {%cpp_type[inc_int_cpp.source] "std::memory_order"} (only parsing).
 
 Module Type ATOMIC_PREDS.
 
   (** Type [t] indexing our spec models the type name T in Atomic<T>. *)
 
   (** The type where the actual methods are implemented *)
-  #[global] Notation base_name ty :=
+  #[global] Abbreviation base_name ty :=
     (Ninst "std::__1::__atomic_base" [Atype ty; Avalue (Eint 0 Tbool)]).
-  #[global] Notation base_name1 ty :=
+  #[global] Abbreviation base_name1 ty :=
     (Ninst "std::__1::__atomic_base" [Atype ty; Avalue (Eint 1 Tbool)]).
   (** The type <<std::atomic<T>>> *)
-  #[global] Notation class_name ty := (Ninst "std::__1::atomic" [Atype ty]).
-  #[global] Notation T ty := (Tnamed (class_name ty)).
+  #[global] Abbreviation class_name ty := (Ninst "std::__1::atomic" [Atype ty]).
+  #[global] Abbreviation T ty := (Tnamed (class_name ty)).
 
   (** Abstract predicates *)
 
@@ -40,7 +40,7 @@ Module Type ATOMIC_PREDS.
 
   Section R_props.
     Context `{Σ : cpp_logic} {σ : genv} `{PV : @PrimVal ty A}.
-    Notation R := (R ty (PV:=PV)).
+    Abbreviation R := (R ty (PV:=PV)).
 
     #[global] Declare Instance R_frac : CFractional1 R.
     #[global] Declare Instance R_timeless : Timeless2 R.
diff --git a/rocq-brick-libstdcpp/proof/atomic/spec.v b/rocq-brick-libstdcpp/proof/atomic/spec.v
index b7a83714..d0e4e633 100644
--- a/rocq-brick-libstdcpp/proof/atomic/spec.v
+++ b/rocq-brick-libstdcpp/proof/atomic/spec.v
@@ -19,11 +19,11 @@ Module atomic_specs (Import atomic : ATOMIC_PREDS).
     Context `{Σ : cpp_logic} {σ : genv}.
     Context (ty : type).
     Context `{!PrimVal ty A,!DefaultValue ty A}.
-    Notation s := (class_name ty) (only parsing).	(** [Atomic<T>] *)
-    Notation b0 := (base_name ty) (only parsing).
-    Notation b1 := (base_name1 ty) (only parsing).
-    Notation R := (R ty).
-    Notation bR q v := (_derived b0 b1 ,, _derived b1 s |-> R q%cQp v) (only parsing).
+    Abbreviation s := (class_name ty) (only parsing).	(** [Atomic<T>] *)
+    Abbreviation b0 := (base_name ty) (only parsing).
+    Abbreviation b1 := (base_name1 ty) (only parsing).
+    Abbreviation R := (R ty).
+    Abbreviation bR q v := (_derived b0 b1 ,, _derived b1 s |-> R q%cQp v) (only parsing).
 
     Definition default_ctor : mpred :=
       specify.template.ctor s [] $
@@ -258,9 +258,9 @@ Module atomic_specs (Import atomic : ATOMIC_PREDS).
     Context (ty : type).
     Context `{PrimVal ty A}.
 
-    #[local] Notation s := (class_name ty) (only parsing).	(** [Atomic<T>] *)
-    #[local] Notation b1 := (base_name1 ty) (only parsing).
-    #[local] Notation bR q v := (_derived b1 s |-> R ty q v) (only parsing).
+    #[local] Abbreviation s := (class_name ty) (only parsing).	(** [Atomic<T>] *)
+    #[local] Abbreviation b1 := (base_name1 ty) (only parsing).
+    #[local] Abbreviation bR q v := (_derived b1 s |-> R ty q v) (only parsing).
 
     (** Apply operation [op] to the atomic cell pointed by [this],
     and return the old contents to continuation [K]. *)
diff --git a/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v b/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v
index db2006fb..43f048a0 100644
--- a/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v
+++ b/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v
@@ -12,7 +12,7 @@ Require Import skylabs.cpp.stdlib.test.atomic.test_cpp.
 Section with_cpp.
   Context `{Σ : cpp_logic, σ : genv}.
 
-  Notation GLOBALS q := (_global "std::__1::memory_order_seq_cst" |-> primR "enum std::__1::memory_order" q 5).
+  Abbreviation GLOBALS q := (_global "std::__1::memory_order_seq_cst" |-> primR "enum std::__1::memory_order" q 5).
 
   Section specs.
     Context `{MOD : test_cpp.source ⊧ σ}.
@@ -67,9 +67,9 @@ Section with_cpp.
 
   #[local] Hint Resolve fractional.UNSAFE_read_prim_cancel : sl_opacity.
 
-  Notation BASE p := (p ,, _base "std::__1::atomic<int>" "std::__1::__atomic_base<int, 1b>" ,, _base "std::__1::__atomic_base<int, 1b>" "std::__1::__atomic_base<int, 0b>").
+  Abbreviation BASE p := (p ,, _base "std::__1::atomic<int>" "std::__1::__atomic_base<int, 1b>" ,, _base "std::__1::__atomic_base<int, 1b>" "std::__1::__atomic_base<int, 0b>").
 
-  Notation BASE1 p := (p ,, _base "std::__1::atomic<int>" "std::__1::__atomic_base<int, 1b>").
+  Abbreviation BASE1 p := (p ,, _base "std::__1::atomic<int>" "std::__1::__atomic_base<int, 1b>").
 
   #[program]
   Definition do_load_C (p : ptr) :=
@@ -185,7 +185,7 @@ Section with_cpp.
   Hint Resolve do_load_C do_store_C : sl_opacity.
   Hint Resolve do_op_C : sl_opacity.
 
-  Notation OK spec :=
+  Abbreviation OK spec :=
     (verify?[test_cpp.source] spec) (only parsing).
 
   Set Typeclasses Debug.

From 2b7279bb5e0fd7232a409fb90ff99a9ca1e1d30f Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Wed, 19 Aug 2026 22:08:55 +0200
Subject: [PATCH 03/14] Spec: add missing modes

---
 rocq-brick-libstdcpp/proof/atomic/spec.v | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/atomic/spec.v b/rocq-brick-libstdcpp/proof/atomic/spec.v
index d0e4e633..96150800 100644
--- a/rocq-brick-libstdcpp/proof/atomic/spec.v
+++ b/rocq-brick-libstdcpp/proof/atomic/spec.v
@@ -248,10 +248,13 @@ Module atomic_specs (Import atomic : ATOMIC_PREDS).
   Class UnOp (ty : type) (A : Type) (op_name : OverloadableOperator) :=
   { atomic_un_op : A -> A
   }.
+  #[global] Hint Mode UnOp ! - ! : typeclass_instances.
 
   Class BinOp (ty1 ty2 : type) (A B : Type) (op_name : OverloadableOperator) (fun_name : ident) :=
   { atomic_bin_op : A -> B -> A
   }.
+  #[global] Hint Mode BinOp ! - ! - ! - : typeclass_instances.
+  #[global] Hint Mode BinOp ! - ! - - ! : typeclass_instances.
 
   Section with_ty.
     Context `{Σ : cpp_logic} {σ : genv}.
@@ -270,14 +273,14 @@ Module atomic_specs (Import atomic : ATOMIC_PREDS).
     #[global] Hint Opaque do_op : typeclass_instances sl_opacity.
 
     Section with_unop.
-      Context `{!UnOp ty A op_name}.
+      Context `{UO : !UnOp ty A op_name}.
 
       (** Triple for unary operators that return the new value *)
       Definition unop_fetch : mpred :=
         specify.template.op b1 op_name function_qualifiers.N ty [] $
           \this this
-          \pre{K} do_op atomic_un_op this K
-          \post{m}[Vinj ty (atomic_un_op m)] K m.
+          \pre{K} do_op (atomic_un_op (UnOp := UO)) this K
+          \post{m}[Vinj ty (atomic_un_op (UnOp := UO) m)] K m.
 
       #[global] Hint Opaque unop_fetch : sl_opacity.
       #[global] Arguments unop_fetch : simpl never.
@@ -289,7 +292,7 @@ Module atomic_specs (Import atomic : ATOMIC_PREDS).
         specify.template.op b1 op_name function_qualifiers.N ty [Tint] $
           \this this
           \arg{dummy} "dummy" (Vint dummy)
-          \pre{K} do_op atomic_un_op this K
+          \pre{K} do_op (atomic_un_op (UnOp := UO)) this K
           \post{m}[Vinj ty m] K m.
 
       #[global] Hint Opaque fetch_unop : sl_opacity.
@@ -299,7 +302,7 @@ Module atomic_specs (Import atomic : ATOMIC_PREDS).
     End with_unop.
 
     Section with_binop.
-      Context `{!BinOp ty tyM A B op_name fun_name}.
+      Context `{BO : !BinOp ty tyM A B op_name fun_name}.
       Context `{!PrimVal tyM B}.
 
       (** Triple for binary operators that return the new value *)
@@ -307,8 +310,8 @@ Module atomic_specs (Import atomic : ATOMIC_PREDS).
         specify.template.op b1 op_name function_qualifiers.N ty [tyM] $
           \this this
           \arg{n : B} "v" (Vinj tyM n)
-          \pre{K} do_op (flip atomic_bin_op n) this K
-          \post{m}[Vinj ty (atomic_bin_op m n)] K m.
+          \pre{K} do_op (flip (atomic_bin_op (BinOp := BO)) n) this K
+          \post{m}[Vinj ty (atomic_bin_op (BinOp := BO) m n)] K m.
       #[global] Hint Opaque binop_fetch : sl_opacity.
       #[global] Arguments binop_fetch : simpl never.
       Definition SpecFor_binop_fetch := RegisterSpec binop_fetch.
@@ -320,7 +323,7 @@ Module atomic_specs (Import atomic : ATOMIC_PREDS).
           \this this
           \arg{n : B} "v" (Vinj tyM n)
           \arg "mo" (memory_order.to_val memory_order.seq_cst)
-          \pre{K} do_op (flip atomic_bin_op n) this K
+          \pre{K} do_op (flip (atomic_bin_op (BinOp := BO)) n) this K
           \post{m}[Vinj ty m] K m.
       #[global] Hint Opaque fetch_binop : sl_opacity.
       #[global] Arguments fetch_binop : simpl never.

From 99af02284f95ddd6d6c56b9b6834b624006aca38 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Thu, 20 Aug 2026 11:47:22 +0200
Subject: [PATCH 04/14] Add UnOp instance for num ++

---
 rocq-brick-libstdcpp/proof/atomic/spec.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/rocq-brick-libstdcpp/proof/atomic/spec.v b/rocq-brick-libstdcpp/proof/atomic/spec.v
index 96150800..0d59cb70 100644
--- a/rocq-brick-libstdcpp/proof/atomic/spec.v
+++ b/rocq-brick-libstdcpp/proof/atomic/spec.v
@@ -337,6 +337,10 @@ Module atomic_specs (Import atomic : ATOMIC_PREDS).
     if sgn is Signed then to_signed (int_rank.bitsize sz) (a + b)
     else to_unsigned (int_rank.bitsize sz) (a + b).
 
+  #[global] Instance num_plusplus {sz sgn} :
+    UnOp (Tnum sz sgn) Z OOPlusPlus :=
+  {| atomic_un_op := add_raw sz sgn 1 |}.
+
   #[global] Instance num_add {sz sgn} :
     BinOp (Tnum sz sgn) (Tnum sz sgn) Z Z OOPlusEqual "fetch_add" :=
   {| atomic_bin_op := add_raw sz sgn |}.

From ccfdf307fe27cd65cf3635273a289717ab50bb88 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Wed, 19 Aug 2026 20:14:21 +0200
Subject: [PATCH 05/14] TMP build rules (to redo)

---
 rocq-brick-libstdcpp/proof/dune.inc | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/rocq-brick-libstdcpp/proof/dune.inc b/rocq-brick-libstdcpp/proof/dune.inc
index 14a82e4b..0abf4551 100644
--- a/rocq-brick-libstdcpp/proof/dune.inc
+++ b/rocq-brick-libstdcpp/proof/dune.inc
@@ -11,6 +11,30 @@
   	 (with-stderr-to inc_algorithms_cpp.v.stderr (run cpp2v -v %{input} -o inc_algorithms_cpp.v --no-elaborate --templates=inc_algorithms_cpp_templates.v  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps inc_algorithms.cpp))
 )
+(subdir atomic
+ (rule
+  (targets inc_int_cpp.v.stderr inc_int_cpp.v inc_int_cpp_templates.v)
+  (alias test_ast)
+  (deps
+   (:input inc_int.cpp)
+   (env_var CPP2V_DOCKER_ENABLED)
+   (glob_files_rec ../*.hpp))
+  (action
+  	 (with-stderr-to inc_int_cpp.v.stderr (run cpp2v -v %{input} -o inc_int_cpp.v --no-elaborate --templates=inc_int_cpp_templates.v  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps inc_int.cpp))
+)
+(subdir atomic
+ (rule
+  (targets test_cpp.v.stderr test_cpp.v test_cpp_templates.v)
+  (alias test_ast)
+  (deps
+   (:input test.cpp)
+   (env_var CPP2V_DOCKER_ENABLED)
+   (glob_files_rec ../*.hpp))
+  (action
+  	 (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v --no-elaborate --templates=test_cpp_templates.v  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps test.cpp))
+)
 (subdir cassert
  (rule
   (targets inc_cassert_cpp.v.stderr inc_cassert_cpp.v inc_cassert_cpp_templates.v)

From 9ed1f633f61e034ce1c1bd905ef6bb914f411912 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Wed, 19 Aug 2026 20:14:13 +0200
Subject: [PATCH 06/14] tweak

---
 rocq-brick-libstdcpp/proof/atomic/pred.v           | 2 +-
 rocq-brick-libstdcpp/proof/atomic/spec.v           | 4 ++--
 rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v | 6 +++---
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/atomic/pred.v b/rocq-brick-libstdcpp/proof/atomic/pred.v
index 0cb14603..7c13c109 100644
--- a/rocq-brick-libstdcpp/proof/atomic/pred.v
+++ b/rocq-brick-libstdcpp/proof/atomic/pred.v
@@ -6,7 +6,7 @@
  *)
 Require Import skylabs.auto.cpp.spec.
 Require Import skylabs.cpp.spec.concepts.
-Require skylabs.cpp.stdlib.atomic.inc_int_cpp.
+Require skylabs.brick.libstdcpp.atomic.inc_int_cpp.
 
 Require Import skylabs.cpp.spec.concepts.
 
diff --git a/rocq-brick-libstdcpp/proof/atomic/spec.v b/rocq-brick-libstdcpp/proof/atomic/spec.v
index 0d59cb70..34cc407f 100644
--- a/rocq-brick-libstdcpp/proof/atomic/spec.v
+++ b/rocq-brick-libstdcpp/proof/atomic/spec.v
@@ -6,10 +6,10 @@
  *)
 Require Import skylabs.auto.cpp.spec.
 Require Import skylabs.cpp.spec.concepts.
-Require Import skylabs.cpp.stdlib.atomic.inc_int_cpp.
+Require Import skylabs.brick.libstdcpp.atomic.inc_int_cpp.
 
 Require Import skylabs.cpp.spec.concepts.
-Require Export skylabs.cpp.stdlib.atomic.pred.
+Require Export skylabs.brick.libstdcpp.atomic.pred.
 
 Module atomic_specs (Import atomic : ATOMIC_PREDS).
 
diff --git a/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v b/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v
index 43f048a0..dab345fc 100644
--- a/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v
+++ b/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v
@@ -5,9 +5,9 @@
  * SPDX-License-Identifier: LGPL-2.1 WITH BlueRock Exception for use over network, see repository root for details.
  *)
 Require Import skylabs.auto.cpp.proof.
-Require Import skylabs.cpp.stdlib.cassert.spec.
-Require Import skylabs.cpp.stdlib.atomic.spec.
-Require Import skylabs.cpp.stdlib.test.atomic.test_cpp.
+Require Import skylabs.brick.libstdcpp.cassert.spec.
+Require Import skylabs.brick.libstdcpp.atomic.spec.
+Require Import skylabs.brick.libstdcpp.test.atomic.test_cpp.
 
 Section with_cpp.
   Context `{Σ : cpp_logic, σ : genv}.

From d7576909286a5df108afcf23144a667b0b038c98 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Wed, 19 Aug 2026 20:20:09 +0200
Subject: [PATCH 07/14] Remove __1

---
 rocq-brick-libstdcpp/proof/atomic/pred.v           | 6 +++---
 rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/atomic/pred.v b/rocq-brick-libstdcpp/proof/atomic/pred.v
index 7c13c109..0eaffa01 100644
--- a/rocq-brick-libstdcpp/proof/atomic/pred.v
+++ b/rocq-brick-libstdcpp/proof/atomic/pred.v
@@ -26,11 +26,11 @@ Module Type ATOMIC_PREDS.
 
   (** The type where the actual methods are implemented *)
   #[global] Abbreviation base_name ty :=
-    (Ninst "std::__1::__atomic_base" [Atype ty; Avalue (Eint 0 Tbool)]).
+    (Ninst "std::__atomic_base" [Atype ty; Avalue (Eint 0 Tbool)]).
   #[global] Abbreviation base_name1 ty :=
-    (Ninst "std::__1::__atomic_base" [Atype ty; Avalue (Eint 1 Tbool)]).
+    (Ninst "std::__atomic_base" [Atype ty; Avalue (Eint 1 Tbool)]).
   (** The type <<std::atomic<T>>> *)
-  #[global] Abbreviation class_name ty := (Ninst "std::__1::atomic" [Atype ty]).
+  #[global] Abbreviation class_name ty := (Ninst "std::atomic" [Atype ty]).
   #[global] Abbreviation T ty := (Tnamed (class_name ty)).
 
   (** Abstract predicates *)
diff --git a/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v b/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v
index dab345fc..c4d508f7 100644
--- a/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v
+++ b/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v
@@ -12,7 +12,7 @@ Require Import skylabs.brick.libstdcpp.test.atomic.test_cpp.
 Section with_cpp.
   Context `{Σ : cpp_logic, σ : genv}.
 
-  Abbreviation GLOBALS q := (_global "std::__1::memory_order_seq_cst" |-> primR "enum std::__1::memory_order" q 5).
+  Abbreviation GLOBALS q := (_global "std::memory_order_seq_cst" |-> primR "enum std::memory_order" q 5).
 
   Section specs.
     Context `{MOD : test_cpp.source ⊧ σ}.
@@ -67,9 +67,9 @@ Section with_cpp.
 
   #[local] Hint Resolve fractional.UNSAFE_read_prim_cancel : sl_opacity.
 
-  Abbreviation BASE p := (p ,, _base "std::__1::atomic<int>" "std::__1::__atomic_base<int, 1b>" ,, _base "std::__1::__atomic_base<int, 1b>" "std::__1::__atomic_base<int, 0b>").
+  Abbreviation BASE p := (p ,, _base "std::atomic<int>" "std::__atomic_base<int, 1b>" ,, _base "std::__atomic_base<int, 1b>" "std::__atomic_base<int, 0b>").
 
-  Abbreviation BASE1 p := (p ,, _base "std::__1::atomic<int>" "std::__1::__atomic_base<int, 1b>").
+  Abbreviation BASE1 p := (p ,, _base "std::atomic<int>" "std::__atomic_base<int, 1b>").
 
   #[program]
   Definition do_load_C (p : ptr) :=

From d3eed7a0f32cde043c7162b72e40611cf75b49ee Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Wed, 19 Aug 2026 20:17:08 +0200
Subject: [PATCH 08/14] TMP for move from tests

---
 rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v b/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v
index c4d508f7..4b53ba1e 100644
--- a/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v
+++ b/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v
@@ -7,7 +7,8 @@
 Require Import skylabs.auto.cpp.proof.
 Require Import skylabs.brick.libstdcpp.cassert.spec.
 Require Import skylabs.brick.libstdcpp.atomic.spec.
-Require Import skylabs.brick.libstdcpp.test.atomic.test_cpp.
+(* Require Import skylabs.brick.libstdcpp.test.atomic.test_cpp. *)
+Require Import skylabs.brick.libstdcpp.atomic.test_cpp.
 
 Section with_cpp.
   Context `{Σ : cpp_logic, σ : genv}.

From 2282384e055c18956263049ac92fdf2e3bcfe3c5 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Wed, 19 Aug 2026 20:35:38 +0200
Subject: [PATCH 09/14] WIP on merging base classes

---
 rocq-brick-libstdcpp/proof/atomic/pred.v |  4 +---
 rocq-brick-libstdcpp/proof/atomic/spec.v | 21 +++++++++++----------
 2 files changed, 12 insertions(+), 13 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/atomic/pred.v b/rocq-brick-libstdcpp/proof/atomic/pred.v
index 0eaffa01..995d3dc0 100644
--- a/rocq-brick-libstdcpp/proof/atomic/pred.v
+++ b/rocq-brick-libstdcpp/proof/atomic/pred.v
@@ -26,9 +26,7 @@ Module Type ATOMIC_PREDS.
 
   (** The type where the actual methods are implemented *)
   #[global] Abbreviation base_name ty :=
-    (Ninst "std::__atomic_base" [Atype ty; Avalue (Eint 0 Tbool)]).
-  #[global] Abbreviation base_name1 ty :=
-    (Ninst "std::__atomic_base" [Atype ty; Avalue (Eint 1 Tbool)]).
+    (Ninst "std::__atomic_base" [Atype ty]).
   (** The type <<std::atomic<T>>> *)
   #[global] Abbreviation class_name ty := (Ninst "std::atomic" [Atype ty]).
   #[global] Abbreviation T ty := (Tnamed (class_name ty)).
diff --git a/rocq-brick-libstdcpp/proof/atomic/spec.v b/rocq-brick-libstdcpp/proof/atomic/spec.v
index 34cc407f..f958cef0 100644
--- a/rocq-brick-libstdcpp/proof/atomic/spec.v
+++ b/rocq-brick-libstdcpp/proof/atomic/spec.v
@@ -20,10 +20,11 @@ Module atomic_specs (Import atomic : ATOMIC_PREDS).
     Context (ty : type).
     Context `{!PrimVal ty A,!DefaultValue ty A}.
     Abbreviation s := (class_name ty) (only parsing).	(** [Atomic<T>] *)
-    Abbreviation b0 := (base_name ty) (only parsing).
-    Abbreviation b1 := (base_name1 ty) (only parsing).
+    Abbreviation b := (base_name ty) (only parsing).
+    Abbreviation b0 := b (only parsing).
+    Abbreviation b1 := b (only parsing).
     Abbreviation R := (R ty).
-    Abbreviation bR q v := (_derived b0 b1 ,, _derived b1 s |-> R q%cQp v) (only parsing).
+    Abbreviation bR q v := (_derived b s |-> R q%cQp v) (only parsing).
 
     Definition default_ctor : mpred :=
       specify.template.ctor s [] $
@@ -60,7 +61,7 @@ Module atomic_specs (Import atomic : ATOMIC_PREDS).
     #[global] Hint Opaque do_load : typeclass_instances sl_opacity.
 
     Definition load : mpred :=
-      specify.template.method b0 "load" function_qualifiers.N ty [Tmemory_order] $
+      specify.template.method b "load" function_qualifiers.N ty [Tmemory_order] $
         \this this
         \arg "mo" (memory_order.to_val memory_order.seq_cst)
         \pre{K} do_load this K
@@ -262,8 +263,8 @@ Module atomic_specs (Import atomic : ATOMIC_PREDS).
     Context `{PrimVal ty A}.
 
     #[local] Abbreviation s := (class_name ty) (only parsing).	(** [Atomic<T>] *)
-    #[local] Abbreviation b1 := (base_name1 ty) (only parsing).
-    #[local] Abbreviation bR q v := (_derived b1 s |-> R ty q v) (only parsing).
+    #[local] Abbreviation b := (base_name ty) (only parsing).
+    #[local] Abbreviation bR q v := (_derived b s |-> R ty q v) (only parsing).
 
     (** Apply operation [op] to the atomic cell pointed by [this],
     and return the old contents to continuation [K]. *)
@@ -277,7 +278,7 @@ Module atomic_specs (Import atomic : ATOMIC_PREDS).
 
       (** Triple for unary operators that return the new value *)
       Definition unop_fetch : mpred :=
-        specify.template.op b1 op_name function_qualifiers.N ty [] $
+        specify.template.op b op_name function_qualifiers.N ty [] $
           \this this
           \pre{K} do_op (atomic_un_op (UnOp := UO)) this K
           \post{m}[Vinj ty (atomic_un_op (UnOp := UO) m)] K m.
@@ -289,7 +290,7 @@ Module atomic_specs (Import atomic : ATOMIC_PREDS).
 
       (** Triple for unary operators that return the old value *)
       Definition fetch_unop : mpred :=
-        specify.template.op b1 op_name function_qualifiers.N ty [Tint] $
+        specify.template.op b op_name function_qualifiers.N ty [Tint] $
           \this this
           \arg{dummy} "dummy" (Vint dummy)
           \pre{K} do_op (atomic_un_op (UnOp := UO)) this K
@@ -307,7 +308,7 @@ Module atomic_specs (Import atomic : ATOMIC_PREDS).
 
       (** Triple for binary operators that return the new value *)
       Definition binop_fetch : mpred :=
-        specify.template.op b1 op_name function_qualifiers.N ty [tyM] $
+        specify.template.op b op_name function_qualifiers.N ty [tyM] $
           \this this
           \arg{n : B} "v" (Vinj tyM n)
           \pre{K} do_op (flip (atomic_bin_op (BinOp := BO)) n) this K
@@ -319,7 +320,7 @@ Module atomic_specs (Import atomic : ATOMIC_PREDS).
 
       (** Triple for methods that return the old value *)
       Definition fetch_binop : mpred :=
-        specify.template.method b1 fun_name function_qualifiers.N ty [tyM; Tmemory_order] $
+        specify.template.method b fun_name function_qualifiers.N ty [tyM; Tmemory_order] $
           \this this
           \arg{n : B} "v" (Vinj tyM n)
           \arg "mo" (memory_order.to_val memory_order.seq_cst)

From dd657538ef7323d01e84e283da08b9308bfecc4f Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Wed, 19 Aug 2026 22:09:14 +0200
Subject: [PATCH 10/14] test_cpp_proof: adapt to alternative implementation

---
 rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v b/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v
index 4b53ba1e..40add411 100644
--- a/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v
+++ b/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v
@@ -68,10 +68,9 @@ Section with_cpp.
 
   #[local] Hint Resolve fractional.UNSAFE_read_prim_cancel : sl_opacity.
 
-  Abbreviation BASE p := (p ,, _base "std::atomic<int>" "std::__atomic_base<int, 1b>" ,, _base "std::__atomic_base<int, 1b>" "std::__atomic_base<int, 0b>").
-
-  Abbreviation BASE1 p := (p ,, _base "std::atomic<int>" "std::__atomic_base<int, 1b>").
+  Abbreviation BASE p := (p ,, _base "std::atomic<int>" "std::__atomic_base<int>").
 
+  Ltac normalize_ptrs := idtac.
   #[program]
   Definition do_load_C (p : ptr) :=
     \cancelx
@@ -168,7 +167,7 @@ Section with_cpp.
     \using denoteModule test_cpp.source
     \consuming{n} p |-> atomic.R "int" 1$m n
     \proving{K (_ : IsExistential K)}
-      spec.do_op "int" op (BASE1 p) K
+      spec.do_op "int" op (BASE p) K
     \instantiate K := (fun res => [| res = n |] **
                                p |-> atomic.R "int" 1$m (op n))
     \end@{mpredI}.

From 4356835663050fcf18faa494ef3b7199ea021267 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Thu, 20 Aug 2026 12:28:33 +0200
Subject: [PATCH 11/14] Disable pointer tests

---
 rocq-brick-libstdcpp/proof/atomic/test.cpp | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/atomic/test.cpp b/rocq-brick-libstdcpp/proof/atomic/test.cpp
index 8578b703..9f27b3e6 100644
--- a/rocq-brick-libstdcpp/proof/atomic/test.cpp
+++ b/rocq-brick-libstdcpp/proof/atomic/test.cpp
@@ -75,16 +75,16 @@ TestFetchAdd() {
     assert(14 == ++atomicInt);
     assert(19 == (atomicInt += 5));
 
-    int x[11] = {0};
-    std::atomic<int*> atomicPtr{x};
-    assert(x == atomicPtr.fetch_add(1));
-    assert(x+1 == atomicPtr.load());
-    assert(x+1 == atomicPtr.fetch_add(1));
-    assert(x+2 == atomicPtr);
-    assert(x+2 == atomicPtr++);
-    assert(x+3 == atomicPtr);
-    assert(x+4 == ++atomicPtr);
-    assert(x+9 == (atomicPtr += 5));
+    // int x[11] = {0};
+    // std::atomic<int*> atomicPtr{x};
+    // assert(x == atomicPtr.fetch_add(1));
+    // assert(x+1 == atomicPtr.load());
+    // assert(x+1 == atomicPtr.fetch_add(1));
+    // assert(x+2 == atomicPtr);
+    // assert(x+2 == atomicPtr++);
+    // assert(x+3 == atomicPtr);
+    // assert(x+4 == ++atomicPtr);
+    // assert(x+9 == (atomicPtr += 5));
 }
 
 int

From c2b6a8ab2c268354df27205f36f27d9d317a448f Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Thu, 20 Aug 2026 12:28:27 +0200
Subject: [PATCH 12/14] WIP on thread id

---
 rocq-brick-libstdcpp/proof/atomic/test.cpp        | 15 +++++++++++++++
 .../proof/atomic/test_cpp_proof.v                 |  5 +++++
 2 files changed, 20 insertions(+)

diff --git a/rocq-brick-libstdcpp/proof/atomic/test.cpp b/rocq-brick-libstdcpp/proof/atomic/test.cpp
index 9f27b3e6..36c7fac5 100644
--- a/rocq-brick-libstdcpp/proof/atomic/test.cpp
+++ b/rocq-brick-libstdcpp/proof/atomic/test.cpp
@@ -6,6 +6,7 @@
  */
 #include <atomic>
 #include <cassert>
+#include <thread>
 
 using namespace std;
 
@@ -14,6 +15,20 @@ test(bool b, const char* msg = nullptr) {
     assert(b);
 }
 
+void testThreadId(std::thread::id i) {
+  std::atomic<std::thread::id> owner{};
+  std::atomic<std::thread::id> owner2{i};
+  std::thread::id i2 = owner;
+  owner = i;
+}
+
+// void testThreadId(std::thread::id id) {
+//   std::atomic<std::thread::id> owner{};
+//   std::atomic<std::thread::id> owner2{id};
+//   owner;
+//   owner = id;
+// }
+
 void
 TestDefaultConstructor() {
     std::atomic<int> atomicInt;
diff --git a/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v b/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v
index 40add411..fd2ac037 100644
--- a/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v
+++ b/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v
@@ -55,6 +55,11 @@ Section with_cpp.
         (\prepost{q} GLOBALS q
          \post[Vint 0] emp).
 
+    cpp.spec "testThreadId(std::thread::id)" as testThreadId with (
+      \arg{p} "" (Vptr p)
+      \prepost{q} GLOBALS q
+      \post emp).
+
     Definition specs :=
       test_default_ctor **
       test_parameterized_ctor **

From ba449522548f0bd750f80e30c8d40676714fe9b5 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Thu, 20 Aug 2026 20:31:42 +0200
Subject: [PATCH 13/14] atomic: fix namespacing

---
 rocq-brick-libstdcpp/proof/atomic/spec.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/rocq-brick-libstdcpp/proof/atomic/spec.v b/rocq-brick-libstdcpp/proof/atomic/spec.v
index f958cef0..c3b949e3 100644
--- a/rocq-brick-libstdcpp/proof/atomic/spec.v
+++ b/rocq-brick-libstdcpp/proof/atomic/spec.v
@@ -362,4 +362,6 @@ Module atomic_specs (Import atomic : ATOMIC_PREDS).
 
 End atomic_specs.
 
+NES.Begin std.atomic.
 Include (atomic_specs atomic).
+NES.End std.atomic.

From 7967331b224f52126dbe9b39730358e68fcfa0b6 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Thu, 20 Aug 2026 20:32:09 +0200
Subject: [PATCH 14/14] WIP on thread_id proofs

---
 .../proof/atomic/test_cpp_proof.v             | 169 ++++++++++++++++--
 rocq-brick-libstdcpp/proof/thread/pred.v      |   6 +
 rocq-brick-libstdcpp/proof/thread/spec.v      |   0
 3 files changed, 161 insertions(+), 14 deletions(-)
 create mode 100644 rocq-brick-libstdcpp/proof/thread/pred.v
 create mode 100644 rocq-brick-libstdcpp/proof/thread/spec.v

diff --git a/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v b/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v
index fd2ac037..547b6ee4 100644
--- a/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v
+++ b/rocq-brick-libstdcpp/proof/atomic/test_cpp_proof.v
@@ -5,11 +5,80 @@
  * SPDX-License-Identifier: LGPL-2.1 WITH BlueRock Exception for use over network, see repository root for details.
  *)
 Require Import skylabs.auto.cpp.proof.
+Require Import skylabs.cpp.spec.argr.
+Require Import skylabs.brick.libstdcpp.runtime.pred.
 Require Import skylabs.brick.libstdcpp.cassert.spec.
-Require Import skylabs.brick.libstdcpp.atomic.spec.
+(* Require Import skylabs.brick.libstdcpp.atomic.spec. *)
 (* Require Import skylabs.brick.libstdcpp.test.atomic.test_cpp. *)
 Require Import skylabs.brick.libstdcpp.atomic.test_cpp.
 
+NES.Begin std.thread.id.
+  Section with_cpp.
+    Context `{Σ : cpp_logic, σ : genv}.
+
+    Parameter R : forall (q : cQp.t) (ot : option thread_idT), Rep.
+    #[only(cfracsplittable, type_ptr="std::thread::id")] derive R.
+
+    cpp.spec (default_ctor "std::thread::id") as ctor_spec from source with (
+      \this this
+      \post this |-> R 1$m None
+    ).
+
+    cpp.spec (const_copy_ctor "std::thread::id") as const_copy_ctor_spec from source with (
+      \this this
+      \arg{p} "" (Vptr p)
+      (* TODO p |-> R *)
+      \post this |-> R 1$m None
+    ).
+
+    cpp.spec (dtor "std::thread::id") as dtor_spec from source with (
+      \this this
+      \pre this |-> R 1$m None
+      \post emp
+    ).
+
+(* cpp.spec *)
+(* "std::thread::id" *)
+  End with_cpp.
+NES.End std.thread.id.
+
+NES.Begin std.atomic.thread.id.
+  Section with_cpp.
+    Context `{Σ : cpp_logic, σ : genv}.
+
+    Parameter R : forall (q : cQp.t) (ot : option thread_idT), Rep.
+
+    cpp.spec (default_ctor "std::atomic<std::thread::id>") as default_ctor from source with (
+      \this this
+      \post this |-> R 1$m None
+    ).
+
+    cpp.spec (dtor "std::atomic<std::thread::id>") as dtor from source with (
+      \this this
+      \pre this |-> R 1$m None
+      \post emp
+    ).
+
+    cpp.spec "std::atomic<std::thread::id>::atomic(std::thread::id)" as atomic_id_ctor from source with (
+      \this this
+      \argR{q m} "" (std.thread.id.R q m)
+      \post this |-> R 1$m m
+    ).
+
+    cpp.spec "std::atomic<std::thread::id>::operator=(std::thread::id)" as atomic_id_op_eq from source with (
+      \this this
+      \argR{q m} "" (std.thread.id.R q m)
+      \pre this |-> R 1$m None
+      (* \post{r}[Vref r] this |-> R 1$m m *)
+      \post{r}[Vref r] this |-> R 1$m m ** r |-> std.thread.id.R 1$m m
+    ).
+
+    cpp.spec "std::atomic<std::thread::id>::operator std::thread::id() const" as atomic_read_op from source with (
+    ).
+
+  End with_cpp.
+NES.End std.atomic.thread.id.
+
 Section with_cpp.
   Context `{Σ : cpp_logic, σ : genv}.
 
@@ -18,6 +87,41 @@ Section with_cpp.
   Section specs.
     Context `{MOD : test_cpp.source ⊧ σ}.
 
+    cpp.spec "testThreadId(std::thread::id)" as testThreadId with (
+      \arg{p} "" (Vptr p)
+      \prepost{q} GLOBALS q
+      \post emp).
+
+
+    Goal verify?[source] testThreadId.
+    Proof.
+      verify_spec; go.
+
+    (*
+Warning:
+The following dependencies are missing specifications:
+"std::atomic<std::thread::id>::atomic()"%cpp_name
+"std::thread::id::id(const std::thread::id&)"%cpp_name
+"std::atomic<std::thread::id>::atomic(std::thread::id)"%cpp_name
+"std::atomic<std::thread::id>::operator=(std::thread::id)"%cpp_name
+"std::atomic<std::thread::id>::~atomic()"%cpp_name
+"std::thread::id::~id()"%cpp_name
+[sl-missing-spec-dependencies,sl,default]
+
+     *)
+
+    Definition ctor : mpred :=
+      specify.template.ctor s [ty] $
+        \this this
+        \arg{n} "v" (Vptr ty n)
+        \post this |-> R 1$m n.
+    #[global] Hint Opaque ctor : sl_opacity.
+    #[global] Arguments ctor : simpl never.
+    Definition SpecFor_ctor := RegisterSpec ctor.
+    #[global] Existing Instance SpecFor_ctor. *)
+
+
+
     cpp.spec "test(bool, const char*)" as test_spec with
       (\arg "b" (Vbool true)
        \arg{p} "" (Vptr p)
@@ -55,11 +159,6 @@ Section with_cpp.
         (\prepost{q} GLOBALS q
          \post[Vint 0] emp).
 
-    cpp.spec "testThreadId(std::thread::id)" as testThreadId with (
-      \arg{p} "" (Vptr p)
-      \prepost{q} GLOBALS q
-      \post emp).
-
     Definition specs :=
       test_default_ctor **
       test_parameterized_ctor **
@@ -193,17 +292,58 @@ Section with_cpp.
   Abbreviation OK spec :=
     (verify?[test_cpp.source] spec) (only parsing).
 
-  Set Typeclasses Debug.
-  Goal SpecFor source "std::__1::atomic<int*>::fetch_add(long, enum std::__1::memory_order)"%cpp_name.
-  Fail apply _.
-  About SpecFor_fetch_binop.
-  Check (SpecFor_fetch_binop "int*").
+(*
+    Definition ctor : mpred :=
+      specify.template.ctor s [ty] $
+        \this this
+        \arg{n} "v" (Vinj ty n)
+        \post this |-> R 1$m n.
+    #[global] Hint Opaque ctor : sl_opacity.
+    #[global] Arguments ctor : simpl never.
+    Definition SpecFor_ctor := RegisterSpec ctor.
+    #[global] Existing Instance SpecFor_ctor. *)
+
+
+
+
+(* "std::atomic<std::thread::id>::atomic()"%cpp_name
+"std::thread::id::id(const std::thread::id&)"%cpp_name
+"std::atomic<std::thread::id>::atomic(std::thread::id)"%cpp_name
+"std::atomic<std::thread::id>::operator=(std::thread::id)"%cpp_name
+"std::atomic<std::thread::id>::~atomic()"%cpp_name
+"std::thread::id::~id()"%cpp_name *)
+
+
+  Goal SpecFor source "std::__atomic_base<int>::fetch_add(int, enum std::memory_order)"%cpp_name.
+    apply _.
+    Goal SpecFor source "std::atomic<int*>::fetch_add(long, enum std::memory_order)"%cpp_name.
+      Set Typeclasses Debug.
+      Fail apply _.
+
+  #[global] Instance num_plusplus {sz sgn} :
+    UnOp (Tnum sz sgn) Z OOPlusPlus :=
+  {| atomic_un_op := add_raw sz sgn 1 |}.
+
+  (* Goal SpecFor source "std::__atomic_base<int>::operator++()".
+  apply _. *)
+  (* Set Typeclasses Debug. *)
+
+  Lemma fetch_add_ok : OK test_fetch_add.
+  Proof. verify_spec; go. Qed.
+
+  Lemma arith_ok : OK test_arith.
+  Proof. verify_spec; go. Qed.
+
+    Check (SpecFor_fetch_binop "int").
+    About SpecFor_fetch_binop.
+    class_apply (SpecFor_fetch_binop "int").
+
+      About SpecFor_fetch_binop.
+      Check (SpecFor_fetch_binop "int*").
   class_apply (SpecFor_fetch_binop "int*").
-  Goal SpecFor source "std::__1::__atomic_base<int, 1b>::operator++(int)".
+  Goal SpecFor source "std::__atomic_base<int, 1b>::operator++(int)".
   apply _.
 
-  Lemma arith_ok : OK test_fetch_add.
-  Proof. verify_spec. go.
 
   Qed.
 
@@ -228,4 +368,5 @@ Section with_cpp.
     verify_spec. go.
   Qed.
 
+
 End with_cpp.
diff --git a/rocq-brick-libstdcpp/proof/thread/pred.v b/rocq-brick-libstdcpp/proof/thread/pred.v
new file mode 100644
index 00000000..8f05d106
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/thread/pred.v
@@ -0,0 +1,6 @@
+Require Import skylabs.auto.cpp.prelude.pred.
+Require Import skylabs.brick.libstdcpp.runtime.pred.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic}.
+End with_cpp.
diff --git a/rocq-brick-libstdcpp/proof/thread/spec.v b/rocq-brick-libstdcpp/proof/thread/spec.v
new file mode 100644
index 00000000..e69de29b