From 48e720ea88bdb2f2f37d3057b41c8d1d3bafb988 Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Sun, 4 Oct 2026 01:22:34 -0400
Subject: [PATCH 01/31] define thread id type as wrapped integer

---
 rocq-brick-libstdcpp/proof/runtime/pred.v | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/runtime/pred.v b/rocq-brick-libstdcpp/proof/runtime/pred.v
index ca8c1c76..a455e72b 100644
--- a/rocq-brick-libstdcpp/proof/runtime/pred.v
+++ b/rocq-brick-libstdcpp/proof/runtime/pred.v
@@ -9,13 +9,12 @@ Require Import skylabs.auto.cpp.prelude.proof.
 Require Import skylabs.auto.core.hints.cancelx_notation.
 Require Import skylabs.iris.extra.proofmode.proofmode.
 
-Parameter thread_idT : Type.
-#[global] Declare Instance thread_idT_inh : Inhabited thread_idT.
-#[global] Declare Instance thread_idT_eq_dec : EqDecision thread_idT.
-#[global] Declare Instance thread_idT_countable : Countable thread_idT.
+Import wrap.
 
-Canonical Structure thread_idTO := leibnizO thread_idT.
+Variant ThreadIdT := .
+Definition thread_idT := WrapN ThreadIdT.
 
+Canonical Structure thread_idTO := leibnizO thread_idT.
 Canonical Structure thread_idT_bi_index : biIndex := BiIndex thread_idT _ eq _.
 
 Parameter HasStdThreads : forall `{Σ : cpp_logic}, Type.

From e7a4130c2fd26f3f1d18466e5c4e9937196a7c0b Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Sun, 4 Oct 2026 01:23:30 -0400
Subject: [PATCH 02/31] provide support for thread id as first class C++ values

---
 rocq-brick-libstdcpp/proof/runtime/pred.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/rocq-brick-libstdcpp/proof/runtime/pred.v b/rocq-brick-libstdcpp/proof/runtime/pred.v
index a455e72b..0b60952c 100644
--- a/rocq-brick-libstdcpp/proof/runtime/pred.v
+++ b/rocq-brick-libstdcpp/proof/runtime/pred.v
@@ -28,6 +28,9 @@ Existing Class HasStdThreads.
   *)
 Parameter threadTI : forall `{HasStdThreads}, thread_info -ml> thread_idT_bi_index.
 
+Definition Vthread (tid : thread_idT) := Vn (unwrapN tid).
+#[global] Instance Vthread_type_compat : TypeCompat "unsigned long" Vthread := {}.
+
 (** [current_thread thr] means that the current thread is [thr].
 
     For more information on monalities, consult tls_modalities.

From 728d8c248b204d9d3edb04c386188208768a3c3e Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Sun, 4 Oct 2026 01:24:12 -0400
Subject: [PATCH 03/31] define process id

---
 rocq-brick-libstdcpp/proof/runtime/pred.v | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/rocq-brick-libstdcpp/proof/runtime/pred.v b/rocq-brick-libstdcpp/proof/runtime/pred.v
index 0b60952c..6fac343e 100644
--- a/rocq-brick-libstdcpp/proof/runtime/pred.v
+++ b/rocq-brick-libstdcpp/proof/runtime/pred.v
@@ -11,9 +11,14 @@ Require Import skylabs.iris.extra.proofmode.proofmode.
 
 Import wrap.
 
+Variant ProcIdT := .
+Definition proc_idT := WrapN ProcIdT.
 Variant ThreadIdT := .
 Definition thread_idT := WrapN ThreadIdT.
 
+Canonical Structure proc_idTO := leibnizO proc_idT.
+Canonical Structure proc_idT_bi_index : biIndex := BiIndex proc_idT _ eq _.
+
 Canonical Structure thread_idTO := leibnizO thread_idT.
 Canonical Structure thread_idT_bi_index : biIndex := BiIndex thread_idT _ eq _.
 
@@ -21,11 +26,13 @@ Parameter HasStdThreads : forall `{Σ : cpp_logic}, Type.
 #[global] Arguments HasStdThreads {_ _} Σ.
 Existing Class HasStdThreads.
 
-(** The projection of the thread from the thread information.
+(** The projection of respectively the process id and thread id from the
+    thread information.
 
   NOTE: This is effectively a field of `HasStdThreads`, but since that
   is registered as an Axiom, we use another Parameter for this.
   *)
+Parameter procTI : forall `{HasStdThreads}, thread_info -ml> proc_idT_bi_index.
 Parameter threadTI : forall `{HasStdThreads}, thread_info -ml> thread_idT_bi_index.
 
 Definition Vthread (tid : thread_idT) := Vn (unwrapN tid).

From ba0fdfcfcc8293c494f9432167164099c8c21399 Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Sun, 4 Oct 2026 01:24:38 -0400
Subject: [PATCH 04/31] re-export prelude definitions

---
 rocq-brick-libstdcpp/proof/runtime/pred.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/rocq-brick-libstdcpp/proof/runtime/pred.v b/rocq-brick-libstdcpp/proof/runtime/pred.v
index 6fac343e..bf9caf8e 100644
--- a/rocq-brick-libstdcpp/proof/runtime/pred.v
+++ b/rocq-brick-libstdcpp/proof/runtime/pred.v
@@ -3,7 +3,7 @@ Require Import skylabs.bi.tls_modalities_rep.
 Require Import skylabs.bi.weakly_objective.
 Require Import skylabs.auto.cpp.weakly_local_with.
 
-Require Import skylabs.auto.cpp.prelude.pred.
+Require Export skylabs.auto.cpp.prelude.pred.
 Require Import skylabs.auto.cpp.prelude.proof.
 
 Require Import skylabs.auto.core.hints.cancelx_notation.

From 9fca5f8038b8782d10e116d6c085a4488005d266 Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Sun, 4 Oct 2026 01:52:26 -0400
Subject: [PATCH 05/31] define weakly objective with respect to process id

---
 .../proof/runtime/objective.v                 | 172 ++++++++++++++++++
 1 file changed, 172 insertions(+)
 create mode 100644 rocq-brick-libstdcpp/proof/runtime/objective.v

diff --git a/rocq-brick-libstdcpp/proof/runtime/objective.v b/rocq-brick-libstdcpp/proof/runtime/objective.v
new file mode 100644
index 00000000..62fe94a4
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/runtime/objective.v
@@ -0,0 +1,172 @@
+
+Require Import skylabs.lang.cpp.logic.
+
+Require Import skylabs.bi.tls_modalities.
+Require Import skylabs.bi.tls_modalities_rep.
+Require Import skylabs.bi.weakly_objective.
+Require Import skylabs.cpp.slice.
+Require Import skylabs.auto.cpp.weakly_local_with.
+
+Require Export skylabs.brick.libstdcpp.runtime.pred.
+
+Require Import skylabs.iris.extra.proofmode.proofmode.
+
+Module Type PROC_OBJECTIVE_AXIOM_TYPE.
+Section proc_objective_axiom.
+  Context `{Σ : !cpp_logic ti Σ0, σ : genv, !HasStdThreads Σ}.
+
+  #[global] Declare Instance tptsto_pd_local_weakly_obj p ty q a :
+      WeaklyLocalWith procTI (tptsto ty q p a).
+  #[global] Declare Instance padding_pd_local_weakly_obj q cls :
+      WeaklyLocalWithR procTI (structR cls q).
+  #[global] Declare Instance mdc_path_pd_local_weakly_obj n path q p :
+      WeaklyLocalWith procTI (mdc_path n path q p).
+  #[global] Declare Instance type_ptr_pd_local_weakly_obj p ty :
+      WeaklyLocalWith procTI (type_ptr ty p).
+  #[global] Declare Instance valid_ptr_pd_local_weakly_obj p ty :
+      WeaklyLocalWith procTI (_valid_ptr ty p).
+  #[global] Declare Instance anyR_pd_local_weakly_obj ty q :
+      WeaklyLocalWithR procTI (anyR ty q).
+  #[global] Declare Instance has_type_pd_weakly_obj v ty :
+      WeaklyLocalWith procTI (has_type v ty).
+End proc_objective_axiom.
+End PROC_OBJECTIVE_AXIOM_TYPE.
+
+Declare Module Export PROC_OBJECTIVE_AXIOM : PROC_OBJECTIVE_AXIOM_TYPE.
+
+Section upstream.
+
+  Lemma weakly_objective_of_obs {ix} {PROP : bi} {P : ix -mon> PROP} Q :
+    (Q -> WeaklyObjective P) ->
+    Observe [| Q |] P ->
+    WeaklyObjective P.
+  Proof.
+    move => HP /observe_monPred_at Hobs i j Hij.
+    iIntros "A"%string. iDestruct (Hobs with "A") as %?.
+    by iStopProof; apply: HP.
+  Qed.
+
+  Lemma weakly_objectiveR_of_obs {ix jx} {PROP : bi} {P : ix -mon> jx -mon> PROP} Q :
+    (Q -> WeaklyObjectiveR P) ->
+    Observe [| Q |] P ->
+    WeaklyObjectiveR P.
+  Proof.
+    rewrite !WeaklyObjectiveR_monPred_at => HP Hobs p.
+    eapply weakly_objective_of_obs, _ => HQ.
+    by apply: HP.
+  Qed.
+
+  Lemma weakly_local_of_obs {ix jx} {PROP : bi} {P : ix -mon> PROP} Q (L : ix -ml> jx) :
+    (Q -> WeaklyLocalWith L P) ->
+    Observe [| Q |] P ->
+    WeaklyLocalWith L P.
+  Proof.
+    rewrite -!weakly_objective_weakly_local_with => HP Hobs j.
+    apply weakly_objective_of_obs with (Q := Q), _ => HQ.
+    by apply: HP.
+  Qed.
+
+  Lemma weakly_localR_of_obs {ix jx kx} {PROP : bi} {P : ix -mon> jx -mon> PROP} Q (L : jx -ml> kx) :
+    (Q -> WeaklyLocalWithR L P) ->
+    Observe [| Q |] P ->
+    WeaklyLocalWithR L P.
+  Proof.
+    rewrite !WeaklyLocalWithR_monPred_at => HP Hobs p.
+    eapply weakly_local_of_obs, _ => HQ.
+    by apply: HP.
+  Qed.
+
+End upstream.
+
+Section derived_pd_local_weakly_local_withR.
+  Context `{Σ : !cpp_logic ti Σ0, σ : genv, !HasStdThreads Σ}.
+
+  Lemma WeaklyLocalWithR_iff_WeaklyObjective_at (R : Rep) :
+    WeaklyLocalWithR procTI R <-> forall (p : ptr) pd, WeaklyObjective (@(procTI, pd) p |-> R).
+  Proof.
+    rewrite WeaklyLocalWithR_iff_WeaklyLocalWith_at; apply forall_proper => p.
+    by rewrite -weakly_objective_weakly_local_with.
+  Qed.
+
+  #[global] Instance validR_pd_local_weakly_obj :
+    WeaklyLocalWithR procTI validR.
+  Proof. rewrite validR_eq /validR_def /=. apply _. Qed.
+
+  #[global] Instance tptstoR_pd_local_weakly_obj ty q v :
+    WeaklyLocalWithR procTI (tptstoR ty q v).
+  Proof.
+    rewrite WeaklyLocalWithR_iff_WeaklyLocalWith_at => p.
+    rewrite _at_tptstoR; apply _.
+  Qed.
+
+  #[global] Instance tptsto_fuzzyR_pd_local_weakly_obj ty q v :
+    WeaklyLocalWithR procTI (tptsto_fuzzyR ty q v).
+  Proof.
+    rewrite WeaklyLocalWithR_iff_WeaklyLocalWith_at => p.
+    rewrite _at_tptsto_fuzzyR; apply _.
+  Qed.
+
+  #[global] Instance primR_pd_local_weakly_obj ty q v :
+    WeaklyLocalWithR procTI (primR ty q v).
+  Proof.
+    rewrite WeaklyLocalWithR_iff_WeaklyLocalWith_at => p.
+    rewrite _at_primR; apply _.
+  Qed.
+
+  #[global] Instance uninitR_pd_local_weakly_obj ty q :
+    WeaklyLocalWithR procTI (uninitR ty q).
+  Proof. rewrite uninitR.unlock; apply _. Qed.
+
+  #[global] Instance type_ptrR_pd_local_weakly_obj ty :
+    WeaklyLocalWithR procTI (type_ptrR ty).
+  Proof. rewrite type_ptrR_eq /type_ptrR_def; apply _. Qed.
+
+  #[global] Instance derivationR_pd_local_weakly_obj n path q :
+    WeaklyLocalWithR procTI (derivationR n path q).
+  Proof. rewrite derivationR.unlock. apply _. Qed.
+
+  Lemma arrayR_pd_local_weakly_obj_lookup
+    {X} ty (Rs : X → Rep) (xs : list X) :
+    (∀ n x, xs !! n = Some x →
+            WeaklyLocalWithR procTI ((.[ ty ! n ]) |-> Rs x)) →
+    WeaklyLocalWithR procTI (arrayR ty Rs xs).
+  Proof.
+    intros HRs.
+    rewrite arrayR_eq /arrayR_def arrR_eq /arrR_def.
+    repeat first [ apply sep_weakly_local_withR | apply _ ].
+    apply big_sepL_weakly_local_withR_lookup => n R.
+    rewrite list_lookup_fmap fmap_Some _offsetR_sep => - [x] [Hx ->].
+    apply sep_weakly_local_withR, HRs; [apply _ | ].
+    rewrite lookupZ_Some_to_nat !Nat2Z.id.
+    by split; first lia.
+  Qed.
+
+  Lemma array_sliceR_pd_local_weakly_obj_lookup m n
+    {X} ty (Rs : X → Rep) (xs : list X) :
+    (∀ i x, xs !! i = Some x →
+            (0 ≤ i < n - m)%Z ->
+            WeaklyLocalWithR procTI ((.[ ty ! i ]) |-> Rs x)) →
+    WeaklyLocalWithR procTI (array_sliceR ty m n Rs xs).
+  Proof.
+    intros HR.
+    apply weakly_localR_of_obs with (Q := lengthZ xs = (n - m)%Z), _ => Hlen.
+    rewrite array_sliceR.unlock.
+    apply sep_weakly_local_withR; first apply _.
+    apply WeaklyLocalWithR_offsetR, arrayR_pd_local_weakly_obj_lookup => i x Hix.
+    have ? := lookupZ_Some Hix.
+    by apply HR; last lia.
+  Qed.
+
+  #[global] Instance arrayR_pd_local_weakly_obj
+    {X} ty (Rs : X → Rep) (xs : list X)
+    `{∀ (x : X), WeaklyLocalWithR procTI (Rs x)} :
+    WeaklyLocalWithR procTI (arrayR ty Rs xs).
+  Proof. by apply arrayR_pd_local_weakly_obj_lookup, _. Qed.
+
+  #[global] Instance array_sliceR_pd_local_weakly_obj
+    {X} ty (Rs : X → Rep) (xs : list X) m n
+    `{∀ (x : X), WeaklyLocalWithR procTI (Rs x)} :
+    WeaklyLocalWithR procTI (array_sliceR ty m n Rs xs).
+  Proof. by apply array_sliceR_pd_local_weakly_obj_lookup, _. Qed.
+
+End derived_pd_local_weakly_local_withR.

From 6a051038098f2a225d9fded7e7aad1dd2752c259 Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Sun, 4 Oct 2026 02:06:07 -0400
Subject: [PATCH 06/31] skeleton for pthread.h specification

---
 rocq-brick-libstdcpp/proof/dune.inc        | 12 ++++++++++++
 rocq-brick-libstdcpp/proof/pthread/inc.hpp |  7 +++++++
 rocq-brick-libstdcpp/proof/pthread/pred.v  | 13 +++++++++++++
 rocq-brick-libstdcpp/proof/pthread/spec.v  | 11 +++++++++++
 4 files changed, 43 insertions(+)
 create mode 100644 rocq-brick-libstdcpp/proof/pthread/inc.hpp
 create mode 100644 rocq-brick-libstdcpp/proof/pthread/pred.v
 create mode 100644 rocq-brick-libstdcpp/proof/pthread/spec.v

diff --git a/rocq-brick-libstdcpp/proof/dune.inc b/rocq-brick-libstdcpp/proof/dune.inc
index 52ff904b..dbb871ac 100644
--- a/rocq-brick-libstdcpp/proof/dune.inc
+++ b/rocq-brick-libstdcpp/proof/dune.inc
@@ -167,6 +167,18 @@
   	 (with-stderr-to inc_new_cpp.v.stderr (run cpp2v -v %{input} -o inc_new_cpp.v --no-elaborate --templates=inc_new_cpp_templates.v  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps inc_new.cpp))
 )
+(subdir pthread
+ (rule
+  (targets inc_hpp.v.stderr inc_hpp.v inc_hpp_templates.v)
+  (alias test_ast)
+  (deps
+   (:input inc.hpp)
+   (env_var CPP2V_DOCKER_ENABLED)
+   (glob_files_rec ../*.hpp))
+  (action
+  	 (with-stderr-to inc_hpp.v.stderr (run cpp2v -v %{input} -o inc_hpp.v --no-elaborate --templates=inc_hpp_templates.v  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps inc.hpp))
+)
 (subdir semaphore
  (rule
   (targets inc_hpp.v.stderr inc_hpp.v inc_hpp_templates.v)
diff --git a/rocq-brick-libstdcpp/proof/pthread/inc.hpp b/rocq-brick-libstdcpp/proof/pthread/inc.hpp
new file mode 100644
index 00000000..46ddc5be
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/pthread/inc.hpp
@@ -0,0 +1,7 @@
+/*
+ * Copyright (c) 2025 SkyLabs AI, Inc.
+ * This software is distributed under the terms of the BedRock Open-Source License.
+ * See the LICENSE-BedRock file in the repository root for details.
+ */
+
+#include <pthread.h>
diff --git a/rocq-brick-libstdcpp/proof/pthread/pred.v b/rocq-brick-libstdcpp/proof/pthread/pred.v
new file mode 100644
index 00000000..9d434f9c
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/pthread/pred.v
@@ -0,0 +1,13 @@
+(*
+ * Copyright (c) 2026 SkyLabs AI, Inc.
+ * This software is distributed under the terms of the BedRock Open-Source License.
+ * See the LICENSE-BedRock file in the repository root for details.
+ *)
+Require Export skylabs.brick.libstdcpp.runtime.pred.
+Require Export skylabs.brick.libstdcpp.runtime.objective.
+
+Require Import skylabs.auto.cpp.prelude.spec.
+(* TODO: add this to a prelude *)
+Require Import skylabs.cpp.slice.
+
+Require Import skylabs.brick.libstdcpp.pthread.inc_hpp.
diff --git a/rocq-brick-libstdcpp/proof/pthread/spec.v b/rocq-brick-libstdcpp/proof/pthread/spec.v
new file mode 100644
index 00000000..b943896c
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/pthread/spec.v
@@ -0,0 +1,11 @@
+(*
+ * Copyright (c) 2025 SkyLabs AI, Inc.
+ * This software is distributed under the terms of the BedRock Open-Source License.
+ * See the LICENSE-BedRock file in the repository root for details.
+ *)
+Require Import skylabs.brick.libstdcpp.pthread.pred.
+Require Import skylabs.brick.libstdcpp.pthread.inc_hpp.
+
+Require Export skylabs.bi.tls_modalities.
+
+Require Import skylabs.auto.cpp.prelude.spec.

From e29af874352334c1e85a3f4befe111e923acd328 Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Sun, 4 Oct 2026 02:08:11 -0400
Subject: [PATCH 07/31] simple predicates and specs for pthread_attr_t

---
 rocq-brick-libstdcpp/proof/pthread/pred.v | 50 +++++++++++++++++++++++
 rocq-brick-libstdcpp/proof/pthread/spec.v | 32 +++++++++++++++
 2 files changed, 82 insertions(+)

diff --git a/rocq-brick-libstdcpp/proof/pthread/pred.v b/rocq-brick-libstdcpp/proof/pthread/pred.v
index 9d434f9c..ce482bdb 100644
--- a/rocq-brick-libstdcpp/proof/pthread/pred.v
+++ b/rocq-brick-libstdcpp/proof/pthread/pred.v
@@ -11,3 +11,53 @@ Require Import skylabs.auto.cpp.prelude.spec.
 Require Import skylabs.cpp.slice.
 
 Require Import skylabs.brick.libstdcpp.pthread.inc_hpp.
+
+Import wrap.
+
+(* UPSTREAM *)
+#[global] Hint Extern 0 (CFractional (fun q => match ?x with | _ => _ end)) =>
+  destruct x : typeclass_instances.
+
+Module pthread_attr.
+
+  (** cpp.class does not support unions *)
+  (* cpp.class "pthread_attr_t" prefix "" from source dataclass. *)
+
+  Variant T := Bytes (_ : list N) | Align (_ : Z).
+
+  Parameter default : T.
+
+  Definition selector (x : option T) : option nat :=
+    match x with
+    | None | Some (Bytes _) => Some 0%nat
+    | Some (Align _) => Some 1%nat
+    end.
+
+  mlock
+  Definition R `{Σ : cpp_logic, σ : genv} (q : cQp.t) (x : option T) : Rep :=
+    match x with
+    | None =>
+        ∃ xs, _field "__size"%cpp_name |-> array_sliceR "char" 0 56 (fun x => charR q x) xs
+    | Some (Bytes xs) =>
+        _field "__size"%cpp_name |-> array_sliceR "char" 0 56 (fun x => charR q x) xs
+    | Some (Align n) =>
+        _field "__align"%cpp_name |-> longR q n
+    end ∗
+    unionR "pthread_attr_t" q (selector x) .
+  #[only(cfractional,cfracvalid,ascfractional,type_ptr,lazy_unfold)] derive R.
+
+Section with_cpp.
+  Import rep.RepFor.
+  Import RepScheme.
+
+  Context `{Σ : cpp_logic,σ : genv}.
+
+  #[global] Instance R_learnable :
+      Cbn (Learn (any ==> learn_eq ==> learn_hints.fin) R) := ltac:(solve_learnable).
+
+  #[global] Instance repfor `{!HasStdThreads Σ} {σ : genv} :
+    rep.RepFor.C "pthread_attr_t" [ArgType.CFrac; ArgType.Model _]
+      R := {}.
+
+End with_cpp.
+End pthread_attr.
diff --git a/rocq-brick-libstdcpp/proof/pthread/spec.v b/rocq-brick-libstdcpp/proof/pthread/spec.v
index b943896c..f0b21b7f 100644
--- a/rocq-brick-libstdcpp/proof/pthread/spec.v
+++ b/rocq-brick-libstdcpp/proof/pthread/spec.v
@@ -9,3 +9,35 @@ Require Import skylabs.brick.libstdcpp.pthread.inc_hpp.
 Require Export skylabs.bi.tls_modalities.
 
 Require Import skylabs.auto.cpp.prelude.spec.
+
+Module pthread_attr.
+  Export pthread_attr.
+
+  cpp.spec "pthread_attr_t::pthread_attr_t()"
+    from source
+    as ctor_spec
+    with ( \this this
+           \post this |-> pthread_attr.R 1$m None ).
+
+  cpp.spec "pthread_attr_t::~pthread_attr_t()"
+    from source
+    as dtor_spec
+    with ( \this this
+           \pre{x} this |-> pthread_attr.R 1$m x
+           \post emp ).
+
+  cpp.spec "pthread_attr_init"
+    as init_spec
+    from source
+    with (\arg{pattr} "attr" (Vptr pattr)
+          \pre{attr}    pattr |-> pthread_attr.R 1$m attr
+          \post[Vint 0] pattr |-> pthread_attr.R 1$m (Some pthread_attr.default)).
+
+  cpp.spec "pthread_attr_destroy"
+    as destroy_spec
+    from source
+    with (\arg{pattr} "attr" (Vptr pattr)
+          \pre{attr}    pattr |-> pthread_attr.R 1$m attr
+          \post[Vint 0] ∃ x, pattr |-> pthread_attr.R 1$m x).
+
+End pthread_attr.

From 3d99af6436697bd2131ece116e0d473ae4001e99 Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Sun, 4 Oct 2026 04:04:50 -0400
Subject: [PATCH 08/31] specify error codes

---
 rocq-brick-libstdcpp/proof/pthread/inc.hpp |  5 ++++
 rocq-brick-libstdcpp/proof/pthread/pred.v  | 27 ++++++++++++++++++++++
 2 files changed, 32 insertions(+)

diff --git a/rocq-brick-libstdcpp/proof/pthread/inc.hpp b/rocq-brick-libstdcpp/proof/pthread/inc.hpp
index 46ddc5be..1d5cff3d 100644
--- a/rocq-brick-libstdcpp/proof/pthread/inc.hpp
+++ b/rocq-brick-libstdcpp/proof/pthread/inc.hpp
@@ -5,3 +5,8 @@
  */
 
 #include <pthread.h>
+#include <errno.h>
+
+enum pthread_errno : int {
+    CANCELED = -1, // same as PTHREAD_CANCELED but it is not a valid way to define an enum,
+};
diff --git a/rocq-brick-libstdcpp/proof/pthread/pred.v b/rocq-brick-libstdcpp/proof/pthread/pred.v
index ce482bdb..293d9376 100644
--- a/rocq-brick-libstdcpp/proof/pthread/pred.v
+++ b/rocq-brick-libstdcpp/proof/pthread/pred.v
@@ -18,6 +18,8 @@ Import wrap.
 #[global] Hint Extern 0 (CFractional (fun q => match ?x with | _ => _ end)) =>
   destruct x : typeclass_instances.
 
+cpp.enum "pthread_errno" from source variant.
+
 Module pthread_attr.
 
   (** cpp.class does not support unions *)
@@ -61,3 +63,28 @@ Section with_cpp.
 
 End with_cpp.
 End pthread_attr.
+
+Module pthread.
+
+  (** pthread_join, some error codes are returned via a void pointer. *)
+  mlock
+  Definition canceled `{Σ : cpp_logic,σ : genv} (p : ptr) : mpred :=
+    let int_size := int_rank.bitsN int_rank.Iint in
+    let addr := trim int_size (pthread_errno.to_Z pthread_errno.CANCELED) in
+    pinned_ptr (Z.to_N addr) p.
+
+  #[global] Instance learn_canceled `{Σ : cpp_logic, σ : genv} p0 p1 :
+    Learnable
+      (pthread.canceled p0)
+      (pthread.canceled p1)
+      [p0 = p1] := ltac:(solve_learnable).
+
+  #[global]
+  Instance pers_canceled `{Σ : cpp_logic, σ : genv} p : Persistent (pthread.canceled p).
+  Proof. rewrite pthread.canceled.unlock /=; apply  _. Qed.
+
+  #[global]
+  Instance affine_canceled `{Σ : cpp_logic, σ : genv} p : Affine (pthread.canceled p).
+  Proof. rewrite pthread.canceled.unlock /=; apply  _. Qed.
+
+End pthread.

From 426c9f0749091dd17a8fecdca04018e3f76cdc8f Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Sun, 4 Oct 2026 04:05:47 -0400
Subject: [PATCH 09/31] predicates for threads

---
 rocq-brick-libstdcpp/proof/pthread/pred.v | 62 +++++++++++++++++++++++
 1 file changed, 62 insertions(+)

diff --git a/rocq-brick-libstdcpp/proof/pthread/pred.v b/rocq-brick-libstdcpp/proof/pthread/pred.v
index 293d9376..891fc1c6 100644
--- a/rocq-brick-libstdcpp/proof/pthread/pred.v
+++ b/rocq-brick-libstdcpp/proof/pthread/pred.v
@@ -65,6 +65,9 @@ End with_cpp.
 End pthread_attr.
 
 Module pthread.
+  Import auto.telescopes auto.telescopes.TeleNotations.
+
+  Record gname := { _ghost : iprop.gname }.
 
   (** pthread_join, some error codes are returned via a void pointer. *)
   mlock
@@ -87,4 +90,63 @@ Module pthread.
   Instance affine_canceled `{Σ : cpp_logic, σ : genv} p : Affine (pthread.canceled p).
   Proof. rewrite pthread.canceled.unlock /=; apply  _. Qed.
 
+  Variant thread_state := RunningOrCompleted | CanceledOrCompleted.
+
+  (** [handle γ spawner tid P Pc] is a token returned when thread creation succeeds. [P] and [Pc]
+      are respectively the postcondition of the thread and its cancelation postcondition. [handle]
+      can be given to <<pthread_join>> to retrieve ownership of left by a thread's termination. It
+      can also be given to <<pthread_cancel>> to retrieve resources from the aborted thread.
+
+      [handle] also specifies the thread id of the spawning thread so that the precondition of [pthread_join]
+      can rule out two threads trying to mutually join with each other.  *)
+  Parameter handle : forall `{Σ : cpp_logic,!HasStdThreads Σ}
+                       (γ : gname) (spawner tid : thread_idT)
+                       (state : thread_state)
+                       (Post : ptr -> mpred)
+                       (Post_cancel : mpred), mpred.
+
+  (** [cancelation γ tid Pc] is a token given to a newly created thread which allows it to test for
+      pending cancelation and return resources ownership. *)
+  Parameter cancelation : forall `{Σ : cpp_logic,!HasStdThreads Σ}
+                             (γ : gname) (tid : thread_idT)
+                             {T : tele} (Post_cancel : T -> mpred), mpred.
+
+  mlock
+  Definition R `{Σ : cpp_logic, σ : genv} (q : cQp.t) (id : thread_idT) :=
+    ulongR q (unwrapN id).
+  #[only(cfractional,cfracvalid,ascfractional,type_ptr,lazy_unfold)] derive R.
+
+  (* TODO: fix [lazy_unfold] derivation. [q] and [q'] need to be distinct variables. *)
+  #[global] Instance R_defined_using' `{Σ : cpp_logic, σ : genv} (q q' : cQp.t) (id : thread_idT) (arg : val) :
+    lazy_unfold.AutoUnlocking.DefinedUsing
+      (pthread.R q id)
+      (primR "unsigned long" q' arg) := {}.
+
+Section with_cpp.
+  Import rep.RepFor.
+  Import RepScheme.
+
+  Context `{Σ : cpp_logic,σ : genv,!HasStdThreads Σ}.
+
+  #[global] Instance R_learnable :
+      Cbn (Learn (learn_eq ==> any ==> learn_eq ==> learn_hints.fin) R) := ltac:(solve_learnable).
+
+
+  Definition learn_eq_dep {T U V} : Learning V → Learning (forall x : T, U x → V) :=
+    fun '{|unLearning := k|} =>
+      {|unLearning := fun L R ls => forall a a' b b', k (L a b) (R a' b') ((existT a b = existT a' b') :: ls) |}.
+
+  #[global] Instance cancelation_learnable :
+    Cbn (Learn (learn_eq ==> req_eq ==> learn_eq_dep ==> learn_hints.fin)
+           pthread.cancelation) := ltac:(solve_learnable).
+
+  #[global] Instance handle_learnable :
+    Cbn (Learn (learn_eq ==> learn_eq ==> req_eq ==> learn_eq ==> learn_eq ==> learn_eq ==> learn_hints.fin)
+           pthread.handle) := ltac:(solve_learnable).
+
+  #[global] Instance repfor `{!HasStdThreads Σ} {σ : genv} :
+    rep.RepFor.C "pthread_t" [ArgType.CFrac; ArgType.Model _]
+      R := {}.
+
+End with_cpp.
 End pthread.

From a60a02406a3115100943ff7817516e22affbe4b8 Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Sun, 4 Oct 2026 04:15:43 -0400
Subject: [PATCH 10/31] spec for pthread_create

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

diff --git a/rocq-brick-libstdcpp/proof/pthread/spec.v b/rocq-brick-libstdcpp/proof/pthread/spec.v
index f0b21b7f..8e49494d 100644
--- a/rocq-brick-libstdcpp/proof/pthread/spec.v
+++ b/rocq-brick-libstdcpp/proof/pthread/spec.v
@@ -41,3 +41,65 @@ Module pthread_attr.
           \post[Vint 0] ∃ x, pattr |-> pthread_attr.R 1$m x).
 
 End pthread_attr.
+
+Module pthread.
+  Export pthread.
+  Import auto.telescopes auto.telescopes.TeleNotations.
+
+  Definition starter_kind : okind :=
+      tFunction (cc:=CC_C) "void*" ["void*"%cpp_type].
+
+  Definition starter_spec `{Σ : cpp_logic, σ : genv} `{!HasStdThreads Σ}
+      (argT stateT : tele)
+      (Pre : ptr -> argT -> mpred)
+      (Post : ptr -> argT -> ptr -> mpred)
+      (Post_c : ptr -> argT -> stateT -> mpred) : WpSpec_cpp_val :=
+    \arg{argp} "arg" (Vptr argp)
+    \pre{arg} Pre argp arg
+    \prepost{tid} current_thread tid
+    \prepost{γ}   pthread.cancelation γ tid (Post_c argp arg)
+    \post{retp}[Vptr retp] Post argp arg retp.
+
+  mlock
+  Definition starter_specR `{Σ : cpp_logic, σ : genv} `{!HasStdThreads Σ}
+      (argT stateT : tele)
+      (Pre : ptr -> argT -> mpred)
+      (Post : ptr -> argT -> ptr -> mpred)
+      (Post_c : ptr -> argT -> stateT -> mpred) : Rep :=
+    unmaterialized_specR starter_kind
+      (starter_spec argT stateT Pre Post Post_c)  .
+
+Section with_cpp.
+
+  Context `{Σ : cpp_logic, σ : genv}.
+  Context `{!HasStdThreads Σ}.
+
+  cpp.spec "pthread_create"
+     as create_spec
+     from source
+     with ( \arg{idp}        "tid"   (Vptr idp)
+            \pre{id0}         idp |-> oprimR "unsigned long" 1$m id0
+            \arg{attrp}      "attr"  (Vptr attrp)
+            \let attr := pthread_attr.default (* we limit ourselves to the standard flags for now *)
+            \prepost{q_attr}  attrp |-> pthread_attr.R q_attr (Some attr)
+            \arg{starterp}   "start" (Vptr starterp)
+            \with argT stateT Pre Post Post_c
+            \pre              starterp |-> starter_specR argT stateT Pre Post Post_c
+            \arg{argp}       "arg"   (Vptr argp)
+            \pre{arg : argT}  Pre argp arg
+            \prepost{this_thread} current_thread this_thread
+            \require WeaklyLocalWith procTI (Pre argp arg)
+            \require forall retp, WeaklyLocalWith procTI (Post argp arg retp)
+            \require ∀p.. s, WeaklyLocalWith procTI (Post_c argp arg s)
+            \post{err}[Vint err]
+               if bool_decide (err = 0) then
+                 ∃ γt tid,
+                   pthread.handle γt this_thread tid RunningOrCompleted
+                       (Post argp arg) (bi_texist (Post_c argp arg)) ∗
+                   idp |-> pthread.R 1$m tid
+               else
+                 Pre argp arg ∗
+                 idp |-> oprimR "unsigned long" 1$m id0 ).
+
+End with_cpp.
+End pthread.

From 859baf33a46f5a4394e751b6e243d6d963387fd6 Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Sun, 4 Oct 2026 04:24:11 -0400
Subject: [PATCH 11/31] spec for pthread_join

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

diff --git a/rocq-brick-libstdcpp/proof/pthread/spec.v b/rocq-brick-libstdcpp/proof/pthread/spec.v
index 8e49494d..96aefce8 100644
--- a/rocq-brick-libstdcpp/proof/pthread/spec.v
+++ b/rocq-brick-libstdcpp/proof/pthread/spec.v
@@ -101,5 +101,30 @@ Section with_cpp.
                  Pre argp arg ∗
                  idp |-> oprimR "unsigned long" 1$m id0 ).
 
+  cpp.spec "pthread_join"
+     as join_spec
+     from source
+     with ( \arg{tid}      "tid"   (Vthread tid)
+            \arg{retp}     "ret"   (Vptr retp)
+            \pre{ret0}      retp |-> oprimR "void*" 1$m ret0
+            \prepost{this_thread} current_thread this_thread
+            \pre{γ s P Pc}  pthread.handle γ this_thread tid s P Pc
+            \post[Vint 0] (* the precondition rules out the errors that [pthread_join] can report:
+                              - deadlocks
+                              - thread is not joinable (our specs don't allow us to create such threads yet)
+                              - thread id does not designate an existing thread
+                              - thread is being joined by other thread *)
+               ∃ ret,
+                 retp |-> ptrR<"void"> 1$m ret ∗
+                 match s with
+                 | RunningOrCompleted => P ret
+                 | CanceledOrCompleted =>
+                   ∃ pCANCELED,
+                     canceled pCANCELED ∗
+                     if bool_decide (ret = pCANCELED)
+                       then Pc
+                       else P ret
+                 end ).
+
 End with_cpp.
 End pthread.

From a6860da26066f2008b8e482f859e9fdf39996dcc Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Sun, 4 Oct 2026 04:26:08 -0400
Subject: [PATCH 12/31] spec for pthread_cancel and pthread_testcancel

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

diff --git a/rocq-brick-libstdcpp/proof/pthread/spec.v b/rocq-brick-libstdcpp/proof/pthread/spec.v
index 96aefce8..187037bd 100644
--- a/rocq-brick-libstdcpp/proof/pthread/spec.v
+++ b/rocq-brick-libstdcpp/proof/pthread/spec.v
@@ -126,5 +126,22 @@ Section with_cpp.
                        else P ret
                  end ).
 
+  cpp.spec "pthread_cancel"
+     as cancel_spec
+     from source
+     with ( \arg{tid}     "tid"   (Vthread tid)
+            \with spawner
+            \pre{γ P Pc}  pthread.handle γ spawner tid RunningOrCompleted P Pc
+            \post[Vint 0]
+               pthread.handle γ spawner tid CanceledOrCompleted P Pc ).
+
+  cpp.spec "pthread_testcancel"
+     as testcancel_spec
+     from source
+     with ( \prepost{γ tid T Pc}  pthread.cancelation γ tid (T := T) Pc
+            \prepost              current_thread tid
+            \prepost{s}           Pc s
+            \post emp ).
+
 End with_cpp.
 End pthread.

From 7a365b884e34ff0ce8e1e9817a653965f9aa004e Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Sun, 4 Oct 2026 19:17:48 -0400
Subject: [PATCH 13/31] spec for pthread ctor and dtor

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

diff --git a/rocq-brick-libstdcpp/proof/pthread/spec.v b/rocq-brick-libstdcpp/proof/pthread/spec.v
index 187037bd..521d351b 100644
--- a/rocq-brick-libstdcpp/proof/pthread/spec.v
+++ b/rocq-brick-libstdcpp/proof/pthread/spec.v
@@ -74,6 +74,17 @@ Section with_cpp.
   Context `{Σ : cpp_logic, σ : genv}.
   Context `{!HasStdThreads Σ}.
 
+  cpp.spec "pthread_t::pthread_t()"
+    from source
+    as ctor_spec
+    with ( \this this
+           \post ∃ tid, this |-> pthread.R 1$m tid ).
+
+  cpp.spec "pthread_t::~pthread_t()"
+    from source
+    as dtor_spec
+    inline.
+
   cpp.spec "pthread_create"
      as create_spec
      from source

From bbf3a093a156ab58586a9d1b370170d5a7ea444d Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Mon, 5 Oct 2026 01:29:05 -0400
Subject: [PATCH 14/31] hints to find a function pointer's specification

---
 rocq-brick-libstdcpp/proof/pthread/hints.v | 73 ++++++++++++++++++++++
 1 file changed, 73 insertions(+)
 create mode 100644 rocq-brick-libstdcpp/proof/pthread/hints.v

diff --git a/rocq-brick-libstdcpp/proof/pthread/hints.v b/rocq-brick-libstdcpp/proof/pthread/hints.v
new file mode 100644
index 00000000..5bf709e2
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/pthread/hints.v
@@ -0,0 +1,73 @@
+(*
+ * Copyright (c) 2025 SkyLabs AI, Inc.
+ * This software is distributed under the terms of the BedRock Open-Source License.
+ * See the LICENSE-BedRock file in the repository root for details.
+ *)
+Require Import skylabs.brick.libstdcpp.pthread.pred.
+Require Import skylabs.brick.libstdcpp.pthread.spec.
+Require Import skylabs.auto.cpp.prelude.spec.
+
+Section with_cpp.
+  Import pthread.
+  Import auto.telescopes auto.telescopes.TeleNotations.
+
+  Context `{Σ : cpp_logic, σ : genv}.
+  Context `{!HasStdThreads Σ}.
+
+  Class ThreadFunction (nm : globname) (P : mpred)
+      (argT stateT : tele)
+      (Pre : ptr -> argT -> mpred)
+      (Post : ptr -> argT -> ptr -> mpred)
+      (Post_c : ptr -> argT -> stateT -> mpred) :=
+    thread_function : P |-- _global nm |-> unmaterialized_specR starter_kind (starter_spec _ _ Pre Post Post_c).
+  #[global] Hint Mode ThreadFunction + + - - - - - : typeclass_instances.
+
+  #[program]
+  Definition fptr_spec_C P nm argT' stateT' Pre' Post' Post_c' :=
+    \cancelx
+    \using P
+    \guard ThreadFunction nm P argT' stateT' Pre' Post' Post_c'
+    \bound argT stateT Pre Post Post_c
+    \proving _global nm |-> starter_specR argT stateT Pre Post Post_c
+    \let P0 := fun t => ptr → tele_arg t → mpred
+    \let P1 := fun t => ptr → tele_arg t → ptr → mpred
+    \let P2 := fun t0 t1 => ptr -> tele_arg t0 → tele_arg t1 → mpred
+    (* \let x := existT (P := fun t => ptr → tele_arg t → ptr → mpred) argT  *)
+    (* \through [|  = existT argT' Pre' |] *)
+    \through [| existT (P := P0) argT Pre = existT argT' Pre' |]
+    \through [| existT (P := P1) argT Post = existT argT' Post' |]
+    \through [| existT (P := fun x => sigT (P2 x)) argT (existT (P := P2 _) stateT Post_c) =
+                existT argT' (existT stateT' Post_c') |]
+    \end.
+  Admit Obligations.
+
+  #[program]
+  Definition exists_tele_app_B {PROP : bi} {t : tele} (P : t -pt> PROP) :=
+    \cancelx
+    \bound_existential x
+    \proving tele_app P x
+    \through (∃p.. a, {instantiate x := a} ∗ tele_app P a)%I
+    \end.
+  Admit Obligations.
+
+  #[program]
+  Definition exists_tele_app_boxed_F {PROP : bi} {t : tele} (P : t -pt> PROP) x `{!IsAnyVariable x} :=
+    \fwd
+    \using □ tele_app P x
+    \deduce (∃p.. a, [| x = a |] ∗ tele_app P a)%I
+    \end.
+  Admit Obligations.
+  #[program]
+  Definition exists_tele_app_F {PROP : bi} {t : tele} (P : t -pt> PROP) x `{!IsAnyVariable x} :=
+    \fwd
+    \using tele_app P x
+    \deduce (∃p.. a, [| x = a |] ∗ tele_app P a)%I
+    \end.
+  Admit Obligations.
+
+End with_cpp.
+
+#[global] Hint Resolve fptr_spec_C : br_hints.
+#[global] Hint Resolve exists_tele_app_B : br_hints.
+#[global] Hint Resolve exists_tele_app_F | 1 : br_hints.
+#[global] Hint Resolve exists_tele_app_boxed_F | 0 : br_hints.

From 4dd89f05714bd49666c24f37062c15f234f13cd6 Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Mon, 5 Oct 2026 01:30:43 -0400
Subject: [PATCH 15/31] test case for pthread specs

---
 rocq-brick-libstdcpp/proof/dune.inc         | 12 ++++
 rocq-brick-libstdcpp/proof/pthread/test.cpp | 64 +++++++++++++++++++++
 2 files changed, 76 insertions(+)
 create mode 100644 rocq-brick-libstdcpp/proof/pthread/test.cpp

diff --git a/rocq-brick-libstdcpp/proof/dune.inc b/rocq-brick-libstdcpp/proof/dune.inc
index dbb871ac..1e08e050 100644
--- a/rocq-brick-libstdcpp/proof/dune.inc
+++ b/rocq-brick-libstdcpp/proof/dune.inc
@@ -179,6 +179,18 @@
   	 (with-stderr-to inc_hpp.v.stderr (run cpp2v -v %{input} -o inc_hpp.v --no-elaborate --templates=inc_hpp_templates.v  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps inc.hpp))
 )
+(subdir pthread
+ (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 semaphore
  (rule
   (targets inc_hpp.v.stderr inc_hpp.v inc_hpp_templates.v)
diff --git a/rocq-brick-libstdcpp/proof/pthread/test.cpp b/rocq-brick-libstdcpp/proof/pthread/test.cpp
new file mode 100644
index 00000000..4f42ad57
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/pthread/test.cpp
@@ -0,0 +1,64 @@
+
+#include <pthread.h>
+#include <assert.h>
+
+void* thread_fn(void* data) {
+    int* counter = static_cast<int*>(data);
+    ++*counter;
+    return nullptr;
+}
+
+void multithreaded_broken () {
+    int counter = 0;
+    int err;
+    void *result;
+    pthread_attr_t attr;
+    pthread_t child;
+
+    pthread_attr_init(&attr);
+    if (pthread_create(&child, &attr, thread_fn, &counter) != 0)
+        return;
+    counter++; // problem here
+    pthread_join(child, &result);
+}
+
+void* cancelable_thread(void* data) {
+    int* counter = static_cast<int*>(data);
+    ++*counter;
+    pthread_testcancel();
+    ++*counter;
+    pthread_testcancel();
+    ++*counter;
+    return nullptr;
+}
+
+// This function is meant to encapsulate an unsound use of void pointer and can't be verified.
+bool is_canceled(void** result) {
+    return *result == PTHREAD_CANCELED; // this is not a valid use of pointers.
+}
+
+void multithreaded_ok () {
+    int counter1 = 0;
+    int counter2 = 0;
+    int err;
+    void *result;
+    pthread_attr_t attr;
+    pthread_t child1, child2;
+    pthread_attr_init(&attr);
+
+    if (pthread_create(&child1, &attr, thread_fn, &counter1) != 0)
+        return;
+    if (pthread_create(&child2, &attr, cancelable_thread, &counter2) != 0) {
+        pthread_join(child1, &result);
+        return;
+    }
+    pthread_cancel(child2);
+    pthread_join(child2, &result);
+    if (is_canceled(&result)) {
+        assert (0 < counter2 && counter2 <= 2);
+    } else {
+        assert (counter2 == 3);
+    }
+    pthread_join(child1, &result);
+    assert (counter1 == 1);
+}

From 1014f2a1075a8536ab7d3310346e09058674c152 Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Mon, 5 Oct 2026 01:51:21 -0400
Subject: [PATCH 16/31] proof of the pthread test case

---
 rocq-brick-libstdcpp/proof/pthread/test.v | 127 ++++++++++++++++++++++
 1 file changed, 127 insertions(+)
 create mode 100644 rocq-brick-libstdcpp/proof/pthread/test.v

diff --git a/rocq-brick-libstdcpp/proof/pthread/test.v b/rocq-brick-libstdcpp/proof/pthread/test.v
new file mode 100644
index 00000000..e973bcbe
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/pthread/test.v
@@ -0,0 +1,127 @@
+(*
+ * Copyright (c) 2025 SkyLabs AI, Inc.
+ * This software is distributed under the terms of the BedRock Open-Source License.
+ * See the LICENSE-BedRock file in the repository root for details.
+ *)
+Require Import skylabs.brick.libstdcpp.mutex.requirements.
+
+Require Import skylabs.brick.libstdcpp.pthread.pred.
+Require Import skylabs.brick.libstdcpp.pthread.spec.
+Require Import skylabs.brick.libstdcpp.pthread.hints.
+
+Require Import skylabs.brick.libstdcpp.pthread.test_cpp.
+
+Require Import skylabs.auto.cpp.prelude.proof.
+
+Section with_cpp.
+  Import auto.telescopes auto.telescopes.TeleNotations.
+
+  Context `{Σ : cpp_logic, σ : genv}.
+  Context {HAS_THREADS : HasStdThreads Σ}.
+  Context `{!test_cpp.source ⊧ σ}.
+
+  cpp.spec "thread_fn(void*)" as thread_fn_spec with
+      ( \arg{argp} "arg" (Vptr argp)
+        \pre{x}  argp |-> intR 1$m x
+        \post*   argp |-> intR 1$m (x + 1)
+        \require valid<"int"> (x + 1)
+        \post[Vptr nullptr] emp ).
+
+  cpp.spec "cancelable_thread(void*)" as cancelable_thread_spec with
+      ( \arg{argp} "arg" (Vptr argp)
+        \pre{x}       argp |-> intR 1$m x
+        \post*        argp |-> intR 1$m (x + 3)
+        \require      valid<"int"> (x + 3)  (* TODO: validP / valid should be interchageable *)
+        \prepost{tid} current_thread tid
+        \let cancel_post :=
+          tele_app (t := [tele _ : Z])
+            (fun x' => argp |-> intR 1$m x' ∗
+                    [| x < x' < x +3 |])%I
+        \prepost{γ}   pthread.cancelation γ tid cancel_post
+        \post[Vptr nullptr] emp ).
+
+    cpp.spec "multithreaded_broken()" as multithreaded_broken_spec with
+      ( \post emp ).
+
+    cpp.spec "multithreaded_ok()" as multithreaded_ok_spec with
+      ( \post emp ).
+
+    (* can't be verified because of its use of void pointers *)
+    cpp.spec "is_canceled(void**)" as is_canceled_spec with
+      ( \arg{p} "p" (Vptr p)
+        \prepost{q retp} p |-> ptrR<"void"> q retp
+        \pre{pCANCELED} pthread.canceled pCANCELED
+        \post[Vbool (bool_decide (retp = pCANCELED))] emp ).
+
+    cpp.spec "__assert_fail" as assert_fail_spec with
+      ( \arg{p0} "" (Vptr p0)
+        \arg{p1} "" (Vptr p1)
+        \arg{n}  "" (Vint n)
+        \arg{p3} "" (Vptr p3)
+        \require False
+        \post emp ).
+
+End with_cpp.
+
+Section with_cpp.
+  Import auto.telescopes auto.telescopes.TeleNotations.
+
+  Context `{Σ : cpp_logic, σ : genv}.
+  Context {HAS_THREADS : HasStdThreads Σ}.
+  Context `{Hmodule : !test_cpp.source ⊧ σ}.
+  Set Default Proof Using "Hmodule".
+
+  #[local] Arguments tele_app _ _ & _.
+  #[local] Hint Opaque tele_app : sl_opacity.
+
+  #[global] Instance thread_fn_is_thread :
+    ThreadFunction "thread_fn(void*)" thread_fn_spec
+      [tele (_ : Z)]
+      [tele]
+      (fun p => tele_app (fun x => p |-> intR 1$m x ∗ [| valid<"int"> (x + 1) |]))%I
+      (fun p => tele_app (fun x _retp => p |-> intR 1$m (x + 1)))%I
+      (fun p => tele_app (fun _ => tele_app False%I)).
+  Proof. eapply specify_mono; work. Qed.
+
+  #[global] Instance cancelable_thread_fn_is_thread :
+    ThreadFunction "cancelable_thread(void*)" cancelable_thread_spec
+      [tele (_ : Z)]
+      [tele (_ : Z)]
+      (fun p => tele_app $ fun x => p |-> intR 1$m x ∗ [| valid<"int"> (x + 3) |] )%I
+      (fun p => tele_app $ fun x _retp => p |-> intR 1$m (x + 3))%I
+      (fun p => tele_app $ fun x => tele_app $ fun x' => p |-> intR 1$m x' ∗ [| x < x' < x +3 |] )%I.
+  Proof. eapply specify_mono; work. Qed.
+
+  Lemma thread_fn_ok : verify[source] thread_fn_spec.
+  Proof.
+    verify_spec. go.
+  Qed.
+
+  Lemma cancelable_thread_ok : verify[source] cancelable_thread_spec.
+  Proof. verify_spec. go. Qed.
+
+  Lemma multithreaded_broken_ok : verify[source] multithreaded_broken_spec.
+  Proof.
+    verify_spec. go.
+    wp_if.
+    { go. }
+    go.
+    (* fails here because thread owns local variable [counter] *)
+  Fail Qed.
+  Abort.
+
+  Lemma multithreaded_ok_ok : verify[source] multithreaded_ok_spec.
+  Proof.
+    verify_spec. go.
+      (* fork thread 1 *)
+    wp_if; go; [].
+      (* fork thread 2 *)
+    wp_if.
+    { go. }
+    go.
+    wp_if.
+    { go. }
+    go.
+  Qed.
+
+End with_cpp.

From f479c0760ba404bbc0059e3a4dc3f659d86525c0 Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Mon, 5 Oct 2026 02:20:05 -0400
Subject: [PATCH 17/31] revert Module Export

---
 rocq-brick-libstdcpp/proof/runtime/pred.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/rocq-brick-libstdcpp/proof/runtime/pred.v b/rocq-brick-libstdcpp/proof/runtime/pred.v
index bf9caf8e..6fac343e 100644
--- a/rocq-brick-libstdcpp/proof/runtime/pred.v
+++ b/rocq-brick-libstdcpp/proof/runtime/pred.v
@@ -3,7 +3,7 @@ Require Import skylabs.bi.tls_modalities_rep.
 Require Import skylabs.bi.weakly_objective.
 Require Import skylabs.auto.cpp.weakly_local_with.
 
-Require Export skylabs.auto.cpp.prelude.pred.
+Require Import skylabs.auto.cpp.prelude.pred.
 Require Import skylabs.auto.cpp.prelude.proof.
 
 Require Import skylabs.auto.core.hints.cancelx_notation.

From 9f626f9cd1e193326907bfc8a8488a73b202ad25 Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Mon, 5 Oct 2026 13:51:42 -0400
Subject: [PATCH 18/31] remove pthread cancelation specs

---
 rocq-brick-libstdcpp/proof/pthread/spec.v | 16 ----------------
 1 file changed, 16 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/pthread/spec.v b/rocq-brick-libstdcpp/proof/pthread/spec.v
index 521d351b..934fd635 100644
--- a/rocq-brick-libstdcpp/proof/pthread/spec.v
+++ b/rocq-brick-libstdcpp/proof/pthread/spec.v
@@ -137,22 +137,6 @@ Section with_cpp.
                        else P ret
                  end ).
 
-  cpp.spec "pthread_cancel"
-     as cancel_spec
-     from source
-     with ( \arg{tid}     "tid"   (Vthread tid)
-            \with spawner
-            \pre{γ P Pc}  pthread.handle γ spawner tid RunningOrCompleted P Pc
-            \post[Vint 0]
-               pthread.handle γ spawner tid CanceledOrCompleted P Pc ).
-
-  cpp.spec "pthread_testcancel"
-     as testcancel_spec
-     from source
-     with ( \prepost{γ tid T Pc}  pthread.cancelation γ tid (T := T) Pc
-            \prepost              current_thread tid
-            \prepost{s}           Pc s
-            \post emp ).
 
 End with_cpp.
 End pthread.

From 9e6af0abbe403387edc5f68a5b9fd08fcecb170c Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Mon, 5 Oct 2026 13:52:49 -0400
Subject: [PATCH 19/31] remove cancelation-related predicates

---
 rocq-brick-libstdcpp/proof/pthread/hints.v | 23 ++++-----
 rocq-brick-libstdcpp/proof/pthread/pred.v  | 43 +++-------------
 rocq-brick-libstdcpp/proof/pthread/spec.v  | 60 ++++++++++------------
 3 files changed, 44 insertions(+), 82 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/pthread/hints.v b/rocq-brick-libstdcpp/proof/pthread/hints.v
index 5bf709e2..a50d7a56 100644
--- a/rocq-brick-libstdcpp/proof/pthread/hints.v
+++ b/rocq-brick-libstdcpp/proof/pthread/hints.v
@@ -15,29 +15,26 @@ Section with_cpp.
   Context `{!HasStdThreads Σ}.
 
   Class ThreadFunction (nm : globname) (P : mpred)
-      (argT stateT : tele)
+      (argT : tele)
       (Pre : ptr -> argT -> mpred)
-      (Post : ptr -> argT -> ptr -> mpred)
-      (Post_c : ptr -> argT -> stateT -> mpred) :=
-    thread_function : P |-- _global nm |-> unmaterialized_specR starter_kind (starter_spec _ _ Pre Post Post_c).
-  #[global] Hint Mode ThreadFunction + + - - - - - : typeclass_instances.
+      (Post : ptr -> argT -> thread_idT -> mpred) :=
+    thread_function : P |-- _global nm |-> unmaterialized_specR starter_kind (starter_spec _ Pre Post).
+  #[global] Hint Mode ThreadFunction + + - - - : typeclass_instances.
 
   #[program]
-  Definition fptr_spec_C P nm argT' stateT' Pre' Post' Post_c' :=
+  Definition fptr_spec_C P nm argT' Pre' Post' :=
     \cancelx
     \using P
-    \guard ThreadFunction nm P argT' stateT' Pre' Post' Post_c'
-    \bound argT stateT Pre Post Post_c
-    \proving _global nm |-> starter_specR argT stateT Pre Post Post_c
+    \guard ThreadFunction nm P argT' Pre' Post'
+    \bound argT Pre Post
+    \proving _global nm |-> starter_specR argT Pre Post
     \let P0 := fun t => ptr → tele_arg t → mpred
-    \let P1 := fun t => ptr → tele_arg t → ptr → mpred
-    \let P2 := fun t0 t1 => ptr -> tele_arg t0 → tele_arg t1 → mpred
+    \let P1 := fun t => ptr → tele_arg t → thread_idT → mpred
+    (* \let P2 := fun t0 t1 => ptr -> tele_arg t0 → tele_arg t1 → mpred *)
     (* \let x := existT (P := fun t => ptr → tele_arg t → ptr → mpred) argT  *)
     (* \through [|  = existT argT' Pre' |] *)
     \through [| existT (P := P0) argT Pre = existT argT' Pre' |]
     \through [| existT (P := P1) argT Post = existT argT' Post' |]
-    \through [| existT (P := fun x => sigT (P2 x)) argT (existT (P := P2 _) stateT Post_c) =
-                existT argT' (existT stateT' Post_c') |]
     \end.
   Admit Obligations.
 
diff --git a/rocq-brick-libstdcpp/proof/pthread/pred.v b/rocq-brick-libstdcpp/proof/pthread/pred.v
index 891fc1c6..0f661ea3 100644
--- a/rocq-brick-libstdcpp/proof/pthread/pred.v
+++ b/rocq-brick-libstdcpp/proof/pthread/pred.v
@@ -69,29 +69,6 @@ Module pthread.
 
   Record gname := { _ghost : iprop.gname }.
 
-  (** pthread_join, some error codes are returned via a void pointer. *)
-  mlock
-  Definition canceled `{Σ : cpp_logic,σ : genv} (p : ptr) : mpred :=
-    let int_size := int_rank.bitsN int_rank.Iint in
-    let addr := trim int_size (pthread_errno.to_Z pthread_errno.CANCELED) in
-    pinned_ptr (Z.to_N addr) p.
-
-  #[global] Instance learn_canceled `{Σ : cpp_logic, σ : genv} p0 p1 :
-    Learnable
-      (pthread.canceled p0)
-      (pthread.canceled p1)
-      [p0 = p1] := ltac:(solve_learnable).
-
-  #[global]
-  Instance pers_canceled `{Σ : cpp_logic, σ : genv} p : Persistent (pthread.canceled p).
-  Proof. rewrite pthread.canceled.unlock /=; apply  _. Qed.
-
-  #[global]
-  Instance affine_canceled `{Σ : cpp_logic, σ : genv} p : Affine (pthread.canceled p).
-  Proof. rewrite pthread.canceled.unlock /=; apply  _. Qed.
-
-  Variant thread_state := RunningOrCompleted | CanceledOrCompleted.
-
   (** [handle γ spawner tid P Pc] is a token returned when thread creation succeeds. [P] and [Pc]
       are respectively the postcondition of the thread and its cancelation postcondition. [handle]
       can be given to <<pthread_join>> to retrieve ownership of left by a thread's termination. It
@@ -101,15 +78,7 @@ Module pthread.
       can rule out two threads trying to mutually join with each other.  *)
   Parameter handle : forall `{Σ : cpp_logic,!HasStdThreads Σ}
                        (γ : gname) (spawner tid : thread_idT)
-                       (state : thread_state)
-                       (Post : ptr -> mpred)
-                       (Post_cancel : mpred), mpred.
-
-  (** [cancelation γ tid Pc] is a token given to a newly created thread which allows it to test for
-      pending cancelation and return resources ownership. *)
-  Parameter cancelation : forall `{Σ : cpp_logic,!HasStdThreads Σ}
-                             (γ : gname) (tid : thread_idT)
-                             {T : tele} (Post_cancel : T -> mpred), mpred.
+                       (Post : mpred), mpred.
 
   mlock
   Definition R `{Σ : cpp_logic, σ : genv} (q : cQp.t) (id : thread_idT) :=
@@ -136,12 +105,12 @@ Section with_cpp.
     fun '{|unLearning := k|} =>
       {|unLearning := fun L R ls => forall a a' b b', k (L a b) (R a' b') ((existT a b = existT a' b') :: ls) |}.
 
-  #[global] Instance cancelation_learnable :
-    Cbn (Learn (learn_eq ==> req_eq ==> learn_eq_dep ==> learn_hints.fin)
-           pthread.cancelation) := ltac:(solve_learnable).
+  #[global] Instance handle_learnable_1 :
+    Cbn (Learn (learn_eq ==> learn_eq ==> req_eq ==> learn_eq ==> learn_hints.fin)
+           pthread.handle) := ltac:(solve_learnable).
 
-  #[global] Instance handle_learnable :
-    Cbn (Learn (learn_eq ==> learn_eq ==> req_eq ==> learn_eq ==> learn_eq ==> learn_eq ==> learn_hints.fin)
+  #[global] Instance handle_learnable_2 :
+    Cbn (Learn (req_eq ==> learn_eq ==> learn_eq ==> learn_eq ==> learn_hints.fin)
            pthread.handle) := ltac:(solve_learnable).
 
   #[global] Instance repfor `{!HasStdThreads Σ} {σ : genv} :
diff --git a/rocq-brick-libstdcpp/proof/pthread/spec.v b/rocq-brick-libstdcpp/proof/pthread/spec.v
index 934fd635..99357755 100644
--- a/rocq-brick-libstdcpp/proof/pthread/spec.v
+++ b/rocq-brick-libstdcpp/proof/pthread/spec.v
@@ -46,28 +46,37 @@ Module pthread.
   Export pthread.
   Import auto.telescopes auto.telescopes.TeleNotations.
 
+  (** [pthread] specs
+
+      This module specifies thread creation and joining. Unsupported are the following features of
+      pthread:
+      - detaching threads;
+      - canceling threads;
+      - joining a thread by threads other than their creator.
+
+      This prevents possible deadlocks when joining threads or race conditions when two threads both
+      try to cancel the same thread.
+   *)
+
   Definition starter_kind : okind :=
       tFunction (cc:=CC_C) "void*" ["void*"%cpp_type].
 
   Definition starter_spec `{Σ : cpp_logic, σ : genv} `{!HasStdThreads Σ}
-      (argT stateT : tele)
+      (argT : tele)
       (Pre : ptr -> argT -> mpred)
-      (Post : ptr -> argT -> ptr -> mpred)
-      (Post_c : ptr -> argT -> stateT -> mpred) : WpSpec_cpp_val :=
+      (Post : ptr -> argT -> thread_idT -> mpred) : WpSpec_cpp_val :=
     \arg{argp} "arg" (Vptr argp)
-    \pre{arg} Pre argp arg
     \prepost{tid} current_thread tid
-    \prepost{γ}   pthread.cancelation γ tid (Post_c argp arg)
-    \post{retp}[Vptr retp] Post argp arg retp.
+    \pre{arg} Pre argp arg
+    \post[Vptr nullptr] Post argp arg tid.
 
   mlock
   Definition starter_specR `{Σ : cpp_logic, σ : genv} `{!HasStdThreads Σ}
-      (argT stateT : tele)
+      (argT : tele)
       (Pre : ptr -> argT -> mpred)
-      (Post : ptr -> argT -> ptr -> mpred)
-      (Post_c : ptr -> argT -> stateT -> mpred) : Rep :=
+      (Post : ptr -> argT -> thread_idT -> mpred) : Rep :=
     unmaterialized_specR starter_kind
-      (starter_spec argT stateT Pre Post Post_c)  .
+      (starter_spec argT Pre Post)  .
 
 Section with_cpp.
 
@@ -94,19 +103,18 @@ Section with_cpp.
             \let attr := pthread_attr.default (* we limit ourselves to the standard flags for now *)
             \prepost{q_attr}  attrp |-> pthread_attr.R q_attr (Some attr)
             \arg{starterp}   "start" (Vptr starterp)
-            \with argT stateT Pre Post Post_c
-            \pre              starterp |-> starter_specR argT stateT Pre Post Post_c
+            \with argT Pre Post
+            \pre              starterp |-> starter_specR argT Pre Post
             \arg{argp}       "arg"   (Vptr argp)
             \pre{arg : argT}  Pre argp arg
-            \prepost{this_thread} current_thread this_thread
+            \with this_thread
+            \prepost          current_thread this_thread
             \require WeaklyLocalWith procTI (Pre argp arg)
-            \require forall retp, WeaklyLocalWith procTI (Post argp arg retp)
-            \require ∀p.. s, WeaklyLocalWith procTI (Post_c argp arg s)
+            \require forall tid, WeaklyLocalWith procTI (Post argp arg tid)
             \post{err}[Vint err]
                if bool_decide (err = 0) then
                  ∃ γt tid,
-                   pthread.handle γt this_thread tid RunningOrCompleted
-                       (Post argp arg) (bi_texist (Post_c argp arg)) ∗
+                   pthread.handle γt this_thread tid (Post argp arg tid) ∗
                    idp |-> pthread.R 1$m tid
                else
                  Pre argp arg ∗
@@ -116,27 +124,15 @@ Section with_cpp.
      as join_spec
      from source
      with ( \arg{tid}      "tid"   (Vthread tid)
-            \arg{retp}     "ret"   (Vptr retp)
-            \pre{ret0}      retp |-> oprimR "void*" 1$m ret0
+            \arg           "ret"   (Vptr nullptr)
             \prepost{this_thread} current_thread this_thread
-            \pre{γ s P Pc}  pthread.handle γ this_thread tid s P Pc
+            \pre{γ P}      pthread.handle γ this_thread tid P
             \post[Vint 0] (* the precondition rules out the errors that [pthread_join] can report:
                               - deadlocks
                               - thread is not joinable (our specs don't allow us to create such threads yet)
                               - thread id does not designate an existing thread
                               - thread is being joined by other thread *)
-               ∃ ret,
-                 retp |-> ptrR<"void"> 1$m ret ∗
-                 match s with
-                 | RunningOrCompleted => P ret
-                 | CanceledOrCompleted =>
-                   ∃ pCANCELED,
-                     canceled pCANCELED ∗
-                     if bool_decide (ret = pCANCELED)
-                       then Pc
-                       else P ret
-                 end ).
-
+                 P ).
 
 End with_cpp.
 End pthread.

From 666b89d242caa60c36055db6f994283098176f21 Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Mon, 5 Oct 2026 13:53:51 -0400
Subject: [PATCH 20/31] remove testing of thread cancelation

---
 rocq-brick-libstdcpp/proof/pthread/test.cpp | 22 +++++----------------
 1 file changed, 5 insertions(+), 17 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/pthread/test.cpp b/rocq-brick-libstdcpp/proof/pthread/test.cpp
index 4f42ad57..22d026ab 100644
--- a/rocq-brick-libstdcpp/proof/pthread/test.cpp
+++ b/rocq-brick-libstdcpp/proof/pthread/test.cpp
@@ -11,7 +11,6 @@ void* thread_fn(void* data) {
 void multithreaded_broken () {
     int counter = 0;
     int err;
-    void *result;
     pthread_attr_t attr;
     pthread_t child;
 
@@ -19,7 +18,7 @@ void multithreaded_broken () {
     if (pthread_create(&child, &attr, thread_fn, &counter) != 0)
         return;
     counter++; // problem here
-    pthread_join(child, &result);
+    pthread_join(child, nullptr);
 }
 
 void* cancelable_thread(void* data) {
@@ -32,16 +31,10 @@ void* cancelable_thread(void* data) {
     return nullptr;
 }
 
-// This function is meant to encapsulate an unsound use of void pointer and can't be verified.
-bool is_canceled(void** result) {
-    return *result == PTHREAD_CANCELED; // this is not a valid use of pointers.
-}
-
 void multithreaded_ok () {
     int counter1 = 0;
     int counter2 = 0;
     int err;
-    void *result;
     pthread_attr_t attr;
     pthread_t child1, child2;
     pthread_attr_init(&attr);
@@ -49,16 +42,11 @@ void multithreaded_ok () {
     if (pthread_create(&child1, &attr, thread_fn, &counter1) != 0)
         return;
     if (pthread_create(&child2, &attr, cancelable_thread, &counter2) != 0) {
-        pthread_join(child1, &result);
+        pthread_join(child1, nullptr);
         return;
     }
-    pthread_cancel(child2);
-    pthread_join(child2, &result);
-    if (is_canceled(&result)) {
-        assert (0 < counter2 && counter2 <= 2);
-    } else {
-        assert (counter2 == 3);
-    }
-    pthread_join(child1, &result);
+    pthread_join(child2, nullptr);
+    pthread_join(child1, nullptr);
     assert (counter1 == 1);
+    assert (counter2 == 3);
 }

From e69222c8979728c4936e7839f41f4e85dd1b01f7 Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Mon, 5 Oct 2026 13:54:14 -0400
Subject: [PATCH 21/31] inline comment in test

---
 rocq-brick-libstdcpp/proof/pthread/test.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/rocq-brick-libstdcpp/proof/pthread/test.cpp b/rocq-brick-libstdcpp/proof/pthread/test.cpp
index 22d026ab..671c3af2 100644
--- a/rocq-brick-libstdcpp/proof/pthread/test.cpp
+++ b/rocq-brick-libstdcpp/proof/pthread/test.cpp
@@ -42,6 +42,10 @@ void multithreaded_ok () {
     if (pthread_create(&child1, &attr, thread_fn, &counter1) != 0)
         return;
     if (pthread_create(&child2, &attr, cancelable_thread, &counter2) != 0) {
+        // Here, it is important that the precondition of `pthread_join` excludes dead-lock because
+        // otherwise, we could not retrieve the ownership of the local variable `counter1` when a
+        // deadlock is detected. The absence of deadlock is assured by requiring the thread that
+        // spawned a thread to also be the one to join it.
         pthread_join(child1, nullptr);
         return;
     }

From 2755e24b5dcae39571e51d7272f3eaeda90d84ac Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Mon, 5 Oct 2026 13:55:55 -0400
Subject: [PATCH 22/31] remove thread cancelation in test proofs

---
 rocq-brick-libstdcpp/proof/pthread/test.v | 29 +++--------------------
 1 file changed, 3 insertions(+), 26 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/pthread/test.v b/rocq-brick-libstdcpp/proof/pthread/test.v
index e973bcbe..da150b78 100644
--- a/rocq-brick-libstdcpp/proof/pthread/test.v
+++ b/rocq-brick-libstdcpp/proof/pthread/test.v
@@ -32,12 +32,6 @@ Section with_cpp.
         \pre{x}       argp |-> intR 1$m x
         \post*        argp |-> intR 1$m (x + 3)
         \require      valid<"int"> (x + 3)  (* TODO: validP / valid should be interchageable *)
-        \prepost{tid} current_thread tid
-        \let cancel_post :=
-          tele_app (t := [tele _ : Z])
-            (fun x' => argp |-> intR 1$m x' ∗
-                    [| x < x' < x +3 |])%I
-        \prepost{γ}   pthread.cancelation γ tid cancel_post
         \post[Vptr nullptr] emp ).
 
     cpp.spec "multithreaded_broken()" as multithreaded_broken_spec with
@@ -46,13 +40,6 @@ Section with_cpp.
     cpp.spec "multithreaded_ok()" as multithreaded_ok_spec with
       ( \post emp ).
 
-    (* can't be verified because of its use of void pointers *)
-    cpp.spec "is_canceled(void**)" as is_canceled_spec with
-      ( \arg{p} "p" (Vptr p)
-        \prepost{q retp} p |-> ptrR<"void"> q retp
-        \pre{pCANCELED} pthread.canceled pCANCELED
-        \post[Vbool (bool_decide (retp = pCANCELED))] emp ).
-
     cpp.spec "__assert_fail" as assert_fail_spec with
       ( \arg{p0} "" (Vptr p0)
         \arg{p1} "" (Vptr p1)
@@ -77,19 +64,15 @@ Section with_cpp.
   #[global] Instance thread_fn_is_thread :
     ThreadFunction "thread_fn(void*)" thread_fn_spec
       [tele (_ : Z)]
-      [tele]
       (fun p => tele_app (fun x => p |-> intR 1$m x ∗ [| valid<"int"> (x + 1) |]))%I
-      (fun p => tele_app (fun x _retp => p |-> intR 1$m (x + 1)))%I
-      (fun p => tele_app (fun _ => tele_app False%I)).
+      (fun p => tele_app (fun x _tid => p |-> intR 1$m (x + 1)))%I.
   Proof. eapply specify_mono; work. Qed.
 
   #[global] Instance cancelable_thread_fn_is_thread :
-    ThreadFunction "cancelable_thread(void*)" cancelable_thread_spec
-      [tele (_ : Z)]
+    ThreadFunction "cancelable_thread(void* )" cancelable_thread_spec
       [tele (_ : Z)]
       (fun p => tele_app $ fun x => p |-> intR 1$m x ∗ [| valid<"int"> (x + 3) |] )%I
-      (fun p => tele_app $ fun x _retp => p |-> intR 1$m (x + 3))%I
-      (fun p => tele_app $ fun x => tele_app $ fun x' => p |-> intR 1$m x' ∗ [| x < x' < x +3 |] )%I.
+      (fun p => tele_app $ fun x _retp => p |-> intR 1$m (x + 3))%I.
   Proof. eapply specify_mono; work. Qed.
 
   Lemma thread_fn_ok : verify[source] thread_fn_spec.
@@ -97,9 +80,6 @@ Section with_cpp.
     verify_spec. go.
   Qed.
 
-  Lemma cancelable_thread_ok : verify[source] cancelable_thread_spec.
-  Proof. verify_spec. go. Qed.
-
   Lemma multithreaded_broken_ok : verify[source] multithreaded_broken_spec.
   Proof.
     verify_spec. go.
@@ -119,9 +99,6 @@ Section with_cpp.
     wp_if.
     { go. }
     go.
-    wp_if.
-    { go. }
-    go.
   Qed.
 
 End with_cpp.

From e3da4ae39b170d58a44de73796a26aca9e1464e2 Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Mon, 5 Oct 2026 15:01:43 -0400
Subject: [PATCH 23/31] remove support for `pthread_attr_t`

---
 rocq-brick-libstdcpp/proof/pthread/pred.v | 51 -----------------------
 rocq-brick-libstdcpp/proof/pthread/spec.v | 36 +---------------
 2 files changed, 1 insertion(+), 86 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/pthread/pred.v b/rocq-brick-libstdcpp/proof/pthread/pred.v
index 0f661ea3..1517bba4 100644
--- a/rocq-brick-libstdcpp/proof/pthread/pred.v
+++ b/rocq-brick-libstdcpp/proof/pthread/pred.v
@@ -14,58 +14,7 @@ Require Import skylabs.brick.libstdcpp.pthread.inc_hpp.
 
 Import wrap.
 
-(* UPSTREAM *)
-#[global] Hint Extern 0 (CFractional (fun q => match ?x with | _ => _ end)) =>
-  destruct x : typeclass_instances.
-
-cpp.enum "pthread_errno" from source variant.
-
-Module pthread_attr.
-
-  (** cpp.class does not support unions *)
-  (* cpp.class "pthread_attr_t" prefix "" from source dataclass. *)
-
-  Variant T := Bytes (_ : list N) | Align (_ : Z).
-
-  Parameter default : T.
-
-  Definition selector (x : option T) : option nat :=
-    match x with
-    | None | Some (Bytes _) => Some 0%nat
-    | Some (Align _) => Some 1%nat
-    end.
-
-  mlock
-  Definition R `{Σ : cpp_logic, σ : genv} (q : cQp.t) (x : option T) : Rep :=
-    match x with
-    | None =>
-        ∃ xs, _field "__size"%cpp_name |-> array_sliceR "char" 0 56 (fun x => charR q x) xs
-    | Some (Bytes xs) =>
-        _field "__size"%cpp_name |-> array_sliceR "char" 0 56 (fun x => charR q x) xs
-    | Some (Align n) =>
-        _field "__align"%cpp_name |-> longR q n
-    end ∗
-    unionR "pthread_attr_t" q (selector x) .
-  #[only(cfractional,cfracvalid,ascfractional,type_ptr,lazy_unfold)] derive R.
-
-Section with_cpp.
-  Import rep.RepFor.
-  Import RepScheme.
-
-  Context `{Σ : cpp_logic,σ : genv}.
-
-  #[global] Instance R_learnable :
-      Cbn (Learn (any ==> learn_eq ==> learn_hints.fin) R) := ltac:(solve_learnable).
-
-  #[global] Instance repfor `{!HasStdThreads Σ} {σ : genv} :
-    rep.RepFor.C "pthread_attr_t" [ArgType.CFrac; ArgType.Model _]
-      R := {}.
-
-End with_cpp.
-End pthread_attr.
-
 Module pthread.
-  Import auto.telescopes auto.telescopes.TeleNotations.
 
   Record gname := { _ghost : iprop.gname }.
 
diff --git a/rocq-brick-libstdcpp/proof/pthread/spec.v b/rocq-brick-libstdcpp/proof/pthread/spec.v
index 99357755..0339e24b 100644
--- a/rocq-brick-libstdcpp/proof/pthread/spec.v
+++ b/rocq-brick-libstdcpp/proof/pthread/spec.v
@@ -10,38 +10,6 @@ Require Export skylabs.bi.tls_modalities.
 
 Require Import skylabs.auto.cpp.prelude.spec.
 
-Module pthread_attr.
-  Export pthread_attr.
-
-  cpp.spec "pthread_attr_t::pthread_attr_t()"
-    from source
-    as ctor_spec
-    with ( \this this
-           \post this |-> pthread_attr.R 1$m None ).
-
-  cpp.spec "pthread_attr_t::~pthread_attr_t()"
-    from source
-    as dtor_spec
-    with ( \this this
-           \pre{x} this |-> pthread_attr.R 1$m x
-           \post emp ).
-
-  cpp.spec "pthread_attr_init"
-    as init_spec
-    from source
-    with (\arg{pattr} "attr" (Vptr pattr)
-          \pre{attr}    pattr |-> pthread_attr.R 1$m attr
-          \post[Vint 0] pattr |-> pthread_attr.R 1$m (Some pthread_attr.default)).
-
-  cpp.spec "pthread_attr_destroy"
-    as destroy_spec
-    from source
-    with (\arg{pattr} "attr" (Vptr pattr)
-          \pre{attr}    pattr |-> pthread_attr.R 1$m attr
-          \post[Vint 0] ∃ x, pattr |-> pthread_attr.R 1$m x).
-
-End pthread_attr.
-
 Module pthread.
   Export pthread.
   Import auto.telescopes auto.telescopes.TeleNotations.
@@ -99,9 +67,7 @@ Section with_cpp.
      from source
      with ( \arg{idp}        "tid"   (Vptr idp)
             \pre{id0}         idp |-> oprimR "unsigned long" 1$m id0
-            \arg{attrp}      "attr"  (Vptr attrp)
-            \let attr := pthread_attr.default (* we limit ourselves to the standard flags for now *)
-            \prepost{q_attr}  attrp |-> pthread_attr.R q_attr (Some attr)
+            \arg             "attr"  (Vptr nullptr)
             \arg{starterp}   "start" (Vptr starterp)
             \with argT Pre Post
             \pre              starterp |-> starter_specR argT Pre Post

From 89150867febe8e732870002f95d8f8baa74b4a93 Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Mon, 5 Oct 2026 15:02:14 -0400
Subject: [PATCH 24/31] remove `pthread_attr_t` from test case

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

diff --git a/rocq-brick-libstdcpp/proof/pthread/test.cpp b/rocq-brick-libstdcpp/proof/pthread/test.cpp
index 671c3af2..18262776 100644
--- a/rocq-brick-libstdcpp/proof/pthread/test.cpp
+++ b/rocq-brick-libstdcpp/proof/pthread/test.cpp
@@ -11,11 +11,9 @@ void* thread_fn(void* data) {
 void multithreaded_broken () {
     int counter = 0;
     int err;
-    pthread_attr_t attr;
     pthread_t child;
 
-    pthread_attr_init(&attr);
-    if (pthread_create(&child, &attr, thread_fn, &counter) != 0)
+    if (pthread_create(&child, nullptr, thread_fn, &counter) != 0)
         return;
     counter++; // problem here
     pthread_join(child, nullptr);
@@ -35,13 +33,11 @@ void multithreaded_ok () {
     int counter1 = 0;
     int counter2 = 0;
     int err;
-    pthread_attr_t attr;
     pthread_t child1, child2;
-    pthread_attr_init(&attr);
 
-    if (pthread_create(&child1, &attr, thread_fn, &counter1) != 0)
+    if (pthread_create(&child1, nullptr, thread_fn, &counter1) != 0)
         return;
-    if (pthread_create(&child2, &attr, cancelable_thread, &counter2) != 0) {
+    if (pthread_create(&child2, nullptr, cancelable_thread, &counter2) != 0) {
         // Here, it is important that the precondition of `pthread_join` excludes dead-lock because
         // otherwise, we could not retrieve the ownership of the local variable `counter1` when a
         // deadlock is detected. The absence of deadlock is assured by requiring the thread that

From 0712d95293965db51a953f27b9b856b15f6a27cf Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Mon, 5 Oct 2026 16:53:04 -0400
Subject: [PATCH 25/31] replace WeaklyObjective with Objective

---
 rocq-brick-libstdcpp/proof/pthread/spec.v     |   4 +-
 .../proof/runtime/objective.v                 | 246 +++++++++++-------
 2 files changed, 154 insertions(+), 96 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/pthread/spec.v b/rocq-brick-libstdcpp/proof/pthread/spec.v
index 0339e24b..476da94a 100644
--- a/rocq-brick-libstdcpp/proof/pthread/spec.v
+++ b/rocq-brick-libstdcpp/proof/pthread/spec.v
@@ -75,8 +75,8 @@ Section with_cpp.
             \pre{arg : argT}  Pre argp arg
             \with this_thread
             \prepost          current_thread this_thread
-            \require WeaklyLocalWith procTI (Pre argp arg)
-            \require forall tid, WeaklyLocalWith procTI (Post argp arg tid)
+            \require LocalWith procTI (Pre argp arg)
+            \require forall tid, LocalWith procTI (Post argp arg tid)
             \post{err}[Vint err]
                if bool_decide (err = 0) then
                  ∃ γt tid,
diff --git a/rocq-brick-libstdcpp/proof/runtime/objective.v b/rocq-brick-libstdcpp/proof/runtime/objective.v
index 62fe94a4..43ca3a5e 100644
--- a/rocq-brick-libstdcpp/proof/runtime/objective.v
+++ b/rocq-brick-libstdcpp/proof/runtime/objective.v
@@ -16,19 +16,19 @@ Section proc_objective_axiom.
   Context `{Σ : !cpp_logic ti Σ0, σ : genv, !HasStdThreads Σ}.
 
   #[global] Declare Instance tptsto_pd_local_weakly_obj p ty q a :
-      WeaklyLocalWith procTI (tptsto ty q p a).
+      LocalWith procTI (tptsto ty q p a).
   #[global] Declare Instance padding_pd_local_weakly_obj q cls :
-      WeaklyLocalWithR procTI (structR cls q).
+      LocalWithR procTI (structR cls q).
   #[global] Declare Instance mdc_path_pd_local_weakly_obj n path q p :
-      WeaklyLocalWith procTI (mdc_path n path q p).
+      LocalWith procTI (mdc_path n path q p).
   #[global] Declare Instance type_ptr_pd_local_weakly_obj p ty :
-      WeaklyLocalWith procTI (type_ptr ty p).
+      LocalWith procTI (type_ptr ty p).
   #[global] Declare Instance valid_ptr_pd_local_weakly_obj p ty :
-      WeaklyLocalWith procTI (_valid_ptr ty p).
+      LocalWith procTI (_valid_ptr ty p).
   #[global] Declare Instance anyR_pd_local_weakly_obj ty q :
-      WeaklyLocalWithR procTI (anyR ty q).
+      LocalWithR procTI (anyR ty q).
   #[global] Declare Instance has_type_pd_weakly_obj v ty :
-      WeaklyLocalWith procTI (has_type v ty).
+      LocalWith procTI (has_type v ty).
 End proc_objective_axiom.
 End PROC_OBJECTIVE_AXIOM_TYPE.
 
@@ -36,137 +36,195 @@ Declare Module Export PROC_OBJECTIVE_AXIOM : PROC_OBJECTIVE_AXIOM_TYPE.
 
 Section upstream.
 
-  Lemma weakly_objective_of_obs {ix} {PROP : bi} {P : ix -mon> PROP} Q :
-    (Q -> WeaklyObjective P) ->
+  Context {PROP : bi}.
+  Context {I J K : biIndex}.
+
+  Lemma objective_of_obs {P : I -mon> PROP} Q :
+    (Q -> Objective P) ->
     Observe [| Q |] P ->
-    WeaklyObjective P.
+    Objective P.
   Proof.
-    move => HP /observe_monPred_at Hobs i j Hij.
+    move => HP /observe_monPred_at Hobs i j.
     iIntros "A"%string. iDestruct (Hobs with "A") as %?.
     by iStopProof; apply: HP.
   Qed.
 
-  Lemma weakly_objectiveR_of_obs {ix jx} {PROP : bi} {P : ix -mon> jx -mon> PROP} Q :
-    (Q -> WeaklyObjectiveR P) ->
-    Observe [| Q |] P ->
-    WeaklyObjectiveR P.
-  Proof.
-    rewrite !WeaklyObjectiveR_monPred_at => HP Hobs p.
-    eapply weakly_objective_of_obs, _ => HQ.
-    by apply: HP.
-  Qed.
-
-  Lemma weakly_local_of_obs {ix jx} {PROP : bi} {P : ix -mon> PROP} Q (L : ix -ml> jx) :
-    (Q -> WeaklyLocalWith L P) ->
-    Observe [| Q |] P ->
-    WeaklyLocalWith L P.
-  Proof.
-    rewrite -!weakly_objective_weakly_local_with => HP Hobs j.
-    apply weakly_objective_of_obs with (Q := Q), _ => HQ.
-    by apply: HP.
-  Qed.
-
-  Lemma weakly_localR_of_obs {ix jx kx} {PROP : bi} {P : ix -mon> jx -mon> PROP} Q (L : jx -ml> kx) :
-    (Q -> WeaklyLocalWithR L P) ->
-    Observe [| Q |] P ->
-    WeaklyLocalWithR L P.
-  Proof.
-    rewrite !WeaklyLocalWithR_monPred_at => HP Hobs p.
-    eapply weakly_local_of_obs, _ => HQ.
-    by apply: HP.
-  Qed.
+  Section LocalWith.
+
+    Lemma LocalWith_of_obs {P : I -mon> PROP} Q {L : I -ml> K} :
+      (Q -> LocalWith L P) ->
+      Observe [| Q |] P ->
+      LocalWith L P.
+    Proof.
+      rewrite -!objective_local_with => HP Hobs j.
+      apply objective_of_obs with (Q := Q), _ => HQ.
+      by apply: HP.
+    Qed.
+
+    #[global] Instance LocalWith_only_provable P {L : I -ml> K} :
+      LocalWith (PROP := PROP) L [| P |].
+    Proof.
+      rewrite -objective_local_with => ?.
+      rewrite monPred_exactly_at_only_provable.
+      apply _.
+    Qed.
+
+  End LocalWith.
+  Section LocalWithR.
+
+    Lemma LocalWithR_of_obs {P : J -mon> I -mon> PROP} Q {L : I -ml> K} :
+      (Q -> LocalWithR L P) ->
+      Observe [| Q |] P ->
+      LocalWithR L P.
+    Proof.
+      rewrite !LocalWithR_monPred_at => HP Hobs p.
+      eapply LocalWith_of_obs, _ => HQ.
+      by apply: HP.
+    Qed.
+
+    #[global] Instance LocalWithR_only_provable P {L : I -ml> J} :
+      LocalWithR (PROP := PROP) L [| P |].
+    Proof.
+      rewrite -objective_local_withR => ? ?.
+      rewrite monPred_at_only_provable.
+      rewrite monPred_exactly_at_only_provable.
+      apply _.
+    Qed.
+
+  End LocalWithR.
 
 End upstream.
 
-Section derived_pd_local_weakly_local_withR.
+Section derived_local_withR.
   Context `{Σ : !cpp_logic ti Σ0, σ : genv, !HasStdThreads Σ}.
+  Implicit Types p : ptr.
 
-  Lemma WeaklyLocalWithR_iff_WeaklyObjective_at (R : Rep) :
-    WeaklyLocalWithR procTI R <-> forall (p : ptr) pd, WeaklyObjective (@(procTI, pd) p |-> R).
+  Section upstream.
+
+    Lemma LocalWithR_iff_LocalWith_at (R : Rep) {J} {L : ti -ml> J} :
+      LocalWithR L R <-> forall p, LocalWith L (p |-> R).
+    Proof.
+      rewrite -objective_local_withR; apply forall_proper => p.
+      by rewrite !objective_local_with plogic.monPred_at_at.
+    Qed.
+
+    Lemma LocalWithR_iff_Objective_at (R : Rep) {J} {L : ti -ml> J} :
+      LocalWithR L R <-> forall (p : ptr) i, Objective (@(L, i) p |-> R).
+    Proof.
+      rewrite -objective_local_withR; apply forall_proper => p.
+      by rewrite !objective_local_with plogic.monPred_at_at.
+    Qed.
+
+    #[global] Instance LocalWithR_as_Rep (P : ptr -> mpred) {J} {L : ti -ml> J} :
+      (forall p, LocalWith L (P p)) ->
+      LocalWithR L (as_Rep P).
+    Proof.
+      rewrite LocalWithR_iff_LocalWith_at => Hp p.
+      by rewrite _at_as_Rep.
+    Qed.
+
+    Section LocalWith.
+
+      #[global] Instance LocalWith_at (R : Rep) {J} {L : ti -ml> J} :
+        LocalWithR L R -> forall p, LocalWith L (p |-> R).
+      Proof. rewrite LocalWithR_iff_LocalWith_at; apply _. Qed.
+
+    End LocalWith.
+
+    Section LocalWithR.
+
+      #[global] Instance LocalWithR_offsetR (R : Rep) {J} {L : ti -ml> J} :
+        LocalWithR L R -> forall o : offset, LocalWithR L (o |-> R).
+      Proof.
+        rewrite LocalWithR_iff_LocalWith_at => HR o.
+        rewrite LocalWithR_iff_LocalWith_at => p.
+        by rewrite _at_offsetR.
+      Qed.
+
+    End LocalWithR.
+
+  End upstream.
+
+  #[global] Instance validR_pd_local_obj :
+    LocalWithR procTI validR.
   Proof.
-    rewrite WeaklyLocalWithR_iff_WeaklyLocalWith_at; apply forall_proper => p.
-    by rewrite -weakly_objective_weakly_local_with.
+    rewrite LocalWithR_iff_LocalWith_at => p.
+    rewrite _at_validR; apply _.
   Qed.
 
-  #[global] Instance validR_pd_local_weakly_obj :
-    WeaklyLocalWithR procTI validR.
-  Proof. rewrite validR_eq /validR_def /=. apply _. Qed.
-
-  #[global] Instance tptstoR_pd_local_weakly_obj ty q v :
-    WeaklyLocalWithR procTI (tptstoR ty q v).
+  #[global] Instance tptstoR_pd_local_obj ty q v :
+    LocalWithR procTI (tptstoR ty q v).
   Proof.
-    rewrite WeaklyLocalWithR_iff_WeaklyLocalWith_at => p.
+    rewrite LocalWithR_iff_LocalWith_at => p.
     rewrite _at_tptstoR; apply _.
   Qed.
 
-  #[global] Instance tptsto_fuzzyR_pd_local_weakly_obj ty q v :
-    WeaklyLocalWithR procTI (tptsto_fuzzyR ty q v).
+  #[global] Instance tptsto_fuzzyR_pd_local_obj ty q v :
+    LocalWithR procTI (tptsto_fuzzyR ty q v).
   Proof.
-    rewrite WeaklyLocalWithR_iff_WeaklyLocalWith_at => p.
+    rewrite LocalWithR_iff_LocalWith_at => p.
     rewrite _at_tptsto_fuzzyR; apply _.
   Qed.
 
-  #[global] Instance primR_pd_local_weakly_obj ty q v :
-    WeaklyLocalWithR procTI (primR ty q v).
+  #[global] Instance primR_pd_local_obj ty q v :
+    LocalWithR procTI (primR ty q v).
   Proof.
-    rewrite WeaklyLocalWithR_iff_WeaklyLocalWith_at => p.
+    rewrite LocalWithR_iff_LocalWith_at => p.
     rewrite _at_primR; apply _.
   Qed.
 
-  #[global] Instance uninitR_pd_local_weakly_obj ty q :
-    WeaklyLocalWithR procTI (uninitR ty q).
+  #[global] Instance uninitR_pd_local_obj ty q :
+    LocalWithR procTI (uninitR ty q).
   Proof. rewrite uninitR.unlock; apply _. Qed.
 
-  #[global] Instance type_ptrR_pd_local_weakly_obj ty :
-    WeaklyLocalWithR procTI (type_ptrR ty).
-  Proof. rewrite type_ptrR_eq /type_ptrR_def; apply _. Qed.
+  #[global] Instance type_ptrR_pd_local_obj ty :
+    LocalWithR procTI (type_ptrR ty).
+  Proof. rewrite type_ptrR_eq /type_ptrR_def. apply _. Qed.
 
-  #[global] Instance derivationR_pd_local_weakly_obj n path q :
-    WeaklyLocalWithR procTI (derivationR n path q).
+  #[global] Instance derivationR_pd_local_obj n path q :
+    LocalWithR procTI (derivationR n path q).
   Proof. rewrite derivationR.unlock. apply _. Qed.
 
-  Lemma arrayR_pd_local_weakly_obj_lookup
+  (** TODO: allow references to list in assumptions:
+      << (∀ i x, xs !! i = Some x -> LocalWithR procTI (Rs x)) >>
+   *)
+  Lemma arrayR_pd_local_obj_lookup
     {X} ty (Rs : X → Rep) (xs : list X) :
-    (∀ n x, xs !! n = Some x →
-            WeaklyLocalWithR procTI ((.[ ty ! n ]) |-> Rs x)) →
-    WeaklyLocalWithR procTI (arrayR ty Rs xs).
+    (∀ x, LocalWithR procTI (Rs x)) →
+    LocalWithR procTI (arrayR ty Rs xs).
   Proof.
     intros HRs.
     rewrite arrayR_eq /arrayR_def arrR_eq /arrR_def.
-    repeat first [ apply sep_weakly_local_withR | apply _ ].
-    apply big_sepL_weakly_local_withR_lookup => n R.
-    rewrite list_lookup_fmap fmap_Some _offsetR_sep => - [x] [Hx ->].
-    apply sep_weakly_local_withR, HRs; [apply _ | ].
-    rewrite lookupZ_Some_to_nat !Nat2Z.id.
-    by split; first lia.
+    repeat first [ apply sep_local_withR | apply _ ].
+    rewrite big_opL_fmap.
+    apply _.
   Qed.
 
-  Lemma array_sliceR_pd_local_weakly_obj_lookup m n
+  (** TODO: allow references to list in assumptions:
+      << (∀ i x, xs !! i = Some x -> LocalWithR procTI (Rs x)) >>
+   *)
+  Lemma array_sliceR_pd_local_obj_lookup m n
     {X} ty (Rs : X → Rep) (xs : list X) :
-    (∀ i x, xs !! i = Some x →
-            (0 ≤ i < n - m)%Z ->
-            WeaklyLocalWithR procTI ((.[ ty ! i ]) |-> Rs x)) →
-    WeaklyLocalWithR procTI (array_sliceR ty m n Rs xs).
+    (∀ x, LocalWithR procTI (Rs x)) →
+    LocalWithR procTI (array_sliceR ty m n Rs xs).
   Proof.
     intros HR.
-    apply weakly_localR_of_obs with (Q := lengthZ xs = (n - m)%Z), _ => Hlen.
     rewrite array_sliceR.unlock.
-    apply sep_weakly_local_withR; first apply _.
-    apply WeaklyLocalWithR_offsetR, arrayR_pd_local_weakly_obj_lookup => i x Hix.
-    have ? := lookupZ_Some Hix.
-    by apply HR; last lia.
+    apply sep_local_withR; first apply _.
+    apply LocalWithR_offsetR, arrayR_pd_local_obj_lookup => x.
+    apply _.
   Qed.
 
-  #[global] Instance arrayR_pd_local_weakly_obj
+  #[global] Instance arrayR_pd_local_obj
     {X} ty (Rs : X → Rep) (xs : list X)
-    `{∀ (x : X), WeaklyLocalWithR procTI (Rs x)} :
-    WeaklyLocalWithR procTI (arrayR ty Rs xs).
-  Proof. by apply arrayR_pd_local_weakly_obj_lookup, _. Qed.
+    `{∀ (x : X), LocalWithR procTI (Rs x)} :
+    LocalWithR procTI (arrayR ty Rs xs).
+  Proof. by apply arrayR_pd_local_obj_lookup, _. Qed.
 
-  #[global] Instance array_sliceR_pd_local_weakly_obj
+  #[global] Instance array_sliceR_pd_local_obj
     {X} ty (Rs : X → Rep) (xs : list X) m n
-    `{∀ (x : X), WeaklyLocalWithR procTI (Rs x)} :
-    WeaklyLocalWithR procTI (array_sliceR ty m n Rs xs).
-  Proof. by apply array_sliceR_pd_local_weakly_obj_lookup, _. Qed.
+    `{∀ (x : X), LocalWithR procTI (Rs x)} :
+    LocalWithR procTI (array_sliceR ty m n Rs xs).
+  Proof. by apply array_sliceR_pd_local_obj_lookup, _. Qed.
 
-End derived_pd_local_weakly_local_withR.
+End derived_local_withR.

From ec1371139b238f13e784afc0fb4a20c8601385d1 Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Tue, 6 Oct 2026 20:11:11 -0400
Subject: [PATCH 26/31] move test case to test directory

---
 rocq-brick-libstdcpp/proof/dune.inc           | 24 -------------------
 rocq-brick-libstdcpp/test/dune.inc            | 12 ++++++++++
 .../{proof => test}/pthread/test.cpp          |  0
 .../{proof => test}/pthread/test.v            |  0
 4 files changed, 12 insertions(+), 24 deletions(-)
 rename rocq-brick-libstdcpp/{proof => test}/pthread/test.cpp (100%)
 rename rocq-brick-libstdcpp/{proof => test}/pthread/test.v (100%)

diff --git a/rocq-brick-libstdcpp/proof/dune.inc b/rocq-brick-libstdcpp/proof/dune.inc
index 1e08e050..52ff904b 100644
--- a/rocq-brick-libstdcpp/proof/dune.inc
+++ b/rocq-brick-libstdcpp/proof/dune.inc
@@ -167,30 +167,6 @@
   	 (with-stderr-to inc_new_cpp.v.stderr (run cpp2v -v %{input} -o inc_new_cpp.v --no-elaborate --templates=inc_new_cpp_templates.v  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps inc_new.cpp))
 )
-(subdir pthread
- (rule
-  (targets inc_hpp.v.stderr inc_hpp.v inc_hpp_templates.v)
-  (alias test_ast)
-  (deps
-   (:input inc.hpp)
-   (env_var CPP2V_DOCKER_ENABLED)
-   (glob_files_rec ../*.hpp))
-  (action
-  	 (with-stderr-to inc_hpp.v.stderr (run cpp2v -v %{input} -o inc_hpp.v --no-elaborate --templates=inc_hpp_templates.v  -- -std=c++20 -stdlib=libstdc++ ))))
- (alias (name srcs) (deps inc.hpp))
-)
-(subdir pthread
- (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 semaphore
  (rule
   (targets inc_hpp.v.stderr inc_hpp.v inc_hpp_templates.v)
diff --git a/rocq-brick-libstdcpp/test/dune.inc b/rocq-brick-libstdcpp/test/dune.inc
index 37b1b7bf..5ec8f414 100644
--- a/rocq-brick-libstdcpp/test/dune.inc
+++ b/rocq-brick-libstdcpp/test/dune.inc
@@ -311,6 +311,18 @@
   	 (with-stderr-to demo_cpp.v.stderr (run cpp2v -v %{input} -o demo_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps demo.cpp))
 )
+(subdir pthread
+ (rule
+  (targets test_cpp.v.stderr test_cpp.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  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps test.cpp))
+)
 (subdir shared_mutex
  (rule
   (targets test_cpp.v.stderr test_cpp.v)
diff --git a/rocq-brick-libstdcpp/proof/pthread/test.cpp b/rocq-brick-libstdcpp/test/pthread/test.cpp
similarity index 100%
rename from rocq-brick-libstdcpp/proof/pthread/test.cpp
rename to rocq-brick-libstdcpp/test/pthread/test.cpp
diff --git a/rocq-brick-libstdcpp/proof/pthread/test.v b/rocq-brick-libstdcpp/test/pthread/test.v
similarity index 100%
rename from rocq-brick-libstdcpp/proof/pthread/test.v
rename to rocq-brick-libstdcpp/test/pthread/test.v

From 9c1051864b26b0afc2e1d6f69df890f5e0a164cc Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Tue, 6 Oct 2026 20:18:47 -0400
Subject: [PATCH 27/31] pthread test: use existing cassert specs

---
 rocq-brick-libstdcpp/test/pthread/test.cpp |  2 +-
 rocq-brick-libstdcpp/test/pthread/test.v   | 11 ++---------
 2 files changed, 3 insertions(+), 10 deletions(-)

diff --git a/rocq-brick-libstdcpp/test/pthread/test.cpp b/rocq-brick-libstdcpp/test/pthread/test.cpp
index 18262776..3aebf9de 100644
--- a/rocq-brick-libstdcpp/test/pthread/test.cpp
+++ b/rocq-brick-libstdcpp/test/pthread/test.cpp
@@ -1,6 +1,6 @@
 
 #include <pthread.h>
-#include <assert.h>
+#include <cassert>
 
 void* thread_fn(void* data) {
     int* counter = static_cast<int*>(data);
diff --git a/rocq-brick-libstdcpp/test/pthread/test.v b/rocq-brick-libstdcpp/test/pthread/test.v
index da150b78..b3dfc068 100644
--- a/rocq-brick-libstdcpp/test/pthread/test.v
+++ b/rocq-brick-libstdcpp/test/pthread/test.v
@@ -8,8 +8,9 @@ Require Import skylabs.brick.libstdcpp.mutex.requirements.
 Require Import skylabs.brick.libstdcpp.pthread.pred.
 Require Import skylabs.brick.libstdcpp.pthread.spec.
 Require Import skylabs.brick.libstdcpp.pthread.hints.
+Require Import skylabs.brick.libstdcpp.cassert.spec.
 
-Require Import skylabs.brick.libstdcpp.pthread.test_cpp.
+Require Import skylabs.brick.libstdcpp.test.pthread.test_cpp.
 
 Require Import skylabs.auto.cpp.prelude.proof.
 
@@ -40,14 +41,6 @@ Section with_cpp.
     cpp.spec "multithreaded_ok()" as multithreaded_ok_spec with
       ( \post emp ).
 
-    cpp.spec "__assert_fail" as assert_fail_spec with
-      ( \arg{p0} "" (Vptr p0)
-        \arg{p1} "" (Vptr p1)
-        \arg{n}  "" (Vint n)
-        \arg{p3} "" (Vptr p3)
-        \require False
-        \post emp ).
-
 End with_cpp.
 
 Section with_cpp.

From b7656cf88a815a16165bd3adf2daab12dd55343a Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Tue, 6 Oct 2026 21:46:03 -0400
Subject: [PATCH 28/31] fix dune.inc

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

diff --git a/rocq-brick-libstdcpp/proof/dune.inc b/rocq-brick-libstdcpp/proof/dune.inc
index 52ff904b..dbb871ac 100644
--- a/rocq-brick-libstdcpp/proof/dune.inc
+++ b/rocq-brick-libstdcpp/proof/dune.inc
@@ -167,6 +167,18 @@
   	 (with-stderr-to inc_new_cpp.v.stderr (run cpp2v -v %{input} -o inc_new_cpp.v --no-elaborate --templates=inc_new_cpp_templates.v  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps inc_new.cpp))
 )
+(subdir pthread
+ (rule
+  (targets inc_hpp.v.stderr inc_hpp.v inc_hpp_templates.v)
+  (alias test_ast)
+  (deps
+   (:input inc.hpp)
+   (env_var CPP2V_DOCKER_ENABLED)
+   (glob_files_rec ../*.hpp))
+  (action
+  	 (with-stderr-to inc_hpp.v.stderr (run cpp2v -v %{input} -o inc_hpp.v --no-elaborate --templates=inc_hpp_templates.v  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps inc.hpp))
+)
 (subdir semaphore
  (rule
   (targets inc_hpp.v.stderr inc_hpp.v inc_hpp_templates.v)

From 1040213c9c8838ea12daa1223fbb65095e8c1e6d Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Wed, 7 Oct 2026 10:23:29 -0400
Subject: [PATCH 29/31] upstreamed some Objective lemmas

---
 .../proof/runtime/objective.v                 | 109 +-----------------
 1 file changed, 1 insertion(+), 108 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/runtime/objective.v b/rocq-brick-libstdcpp/proof/runtime/objective.v
index 43ca3a5e..3d176bea 100644
--- a/rocq-brick-libstdcpp/proof/runtime/objective.v
+++ b/rocq-brick-libstdcpp/proof/runtime/objective.v
@@ -5,7 +5,7 @@ Require Import skylabs.bi.tls_modalities.
 Require Import skylabs.bi.tls_modalities_rep.
 Require Import skylabs.bi.weakly_objective.
 Require Import skylabs.cpp.slice.
-Require Import skylabs.auto.cpp.weakly_local_with.
+Require Import skylabs.auto.cpp.local_with.
 
 Require Export skylabs.brick.libstdcpp.runtime.pred.
 
@@ -34,117 +34,10 @@ End PROC_OBJECTIVE_AXIOM_TYPE.
 
 Declare Module Export PROC_OBJECTIVE_AXIOM : PROC_OBJECTIVE_AXIOM_TYPE.
 
-Section upstream.
-
-  Context {PROP : bi}.
-  Context {I J K : biIndex}.
-
-  Lemma objective_of_obs {P : I -mon> PROP} Q :
-    (Q -> Objective P) ->
-    Observe [| Q |] P ->
-    Objective P.
-  Proof.
-    move => HP /observe_monPred_at Hobs i j.
-    iIntros "A"%string. iDestruct (Hobs with "A") as %?.
-    by iStopProof; apply: HP.
-  Qed.
-
-  Section LocalWith.
-
-    Lemma LocalWith_of_obs {P : I -mon> PROP} Q {L : I -ml> K} :
-      (Q -> LocalWith L P) ->
-      Observe [| Q |] P ->
-      LocalWith L P.
-    Proof.
-      rewrite -!objective_local_with => HP Hobs j.
-      apply objective_of_obs with (Q := Q), _ => HQ.
-      by apply: HP.
-    Qed.
-
-    #[global] Instance LocalWith_only_provable P {L : I -ml> K} :
-      LocalWith (PROP := PROP) L [| P |].
-    Proof.
-      rewrite -objective_local_with => ?.
-      rewrite monPred_exactly_at_only_provable.
-      apply _.
-    Qed.
-
-  End LocalWith.
-  Section LocalWithR.
-
-    Lemma LocalWithR_of_obs {P : J -mon> I -mon> PROP} Q {L : I -ml> K} :
-      (Q -> LocalWithR L P) ->
-      Observe [| Q |] P ->
-      LocalWithR L P.
-    Proof.
-      rewrite !LocalWithR_monPred_at => HP Hobs p.
-      eapply LocalWith_of_obs, _ => HQ.
-      by apply: HP.
-    Qed.
-
-    #[global] Instance LocalWithR_only_provable P {L : I -ml> J} :
-      LocalWithR (PROP := PROP) L [| P |].
-    Proof.
-      rewrite -objective_local_withR => ? ?.
-      rewrite monPred_at_only_provable.
-      rewrite monPred_exactly_at_only_provable.
-      apply _.
-    Qed.
-
-  End LocalWithR.
-
-End upstream.
-
 Section derived_local_withR.
   Context `{Σ : !cpp_logic ti Σ0, σ : genv, !HasStdThreads Σ}.
   Implicit Types p : ptr.
 
-  Section upstream.
-
-    Lemma LocalWithR_iff_LocalWith_at (R : Rep) {J} {L : ti -ml> J} :
-      LocalWithR L R <-> forall p, LocalWith L (p |-> R).
-    Proof.
-      rewrite -objective_local_withR; apply forall_proper => p.
-      by rewrite !objective_local_with plogic.monPred_at_at.
-    Qed.
-
-    Lemma LocalWithR_iff_Objective_at (R : Rep) {J} {L : ti -ml> J} :
-      LocalWithR L R <-> forall (p : ptr) i, Objective (@(L, i) p |-> R).
-    Proof.
-      rewrite -objective_local_withR; apply forall_proper => p.
-      by rewrite !objective_local_with plogic.monPred_at_at.
-    Qed.
-
-    #[global] Instance LocalWithR_as_Rep (P : ptr -> mpred) {J} {L : ti -ml> J} :
-      (forall p, LocalWith L (P p)) ->
-      LocalWithR L (as_Rep P).
-    Proof.
-      rewrite LocalWithR_iff_LocalWith_at => Hp p.
-      by rewrite _at_as_Rep.
-    Qed.
-
-    Section LocalWith.
-
-      #[global] Instance LocalWith_at (R : Rep) {J} {L : ti -ml> J} :
-        LocalWithR L R -> forall p, LocalWith L (p |-> R).
-      Proof. rewrite LocalWithR_iff_LocalWith_at; apply _. Qed.
-
-    End LocalWith.
-
-    Section LocalWithR.
-
-      #[global] Instance LocalWithR_offsetR (R : Rep) {J} {L : ti -ml> J} :
-        LocalWithR L R -> forall o : offset, LocalWithR L (o |-> R).
-      Proof.
-        rewrite LocalWithR_iff_LocalWith_at => HR o.
-        rewrite LocalWithR_iff_LocalWith_at => p.
-        by rewrite _at_offsetR.
-      Qed.
-
-    End LocalWithR.
-
-  End upstream.
-
   #[global] Instance validR_pd_local_obj :
     LocalWithR procTI validR.
   Proof.

From 17373e468f26a4b153c52c6d2936916b2b538d46 Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Wed, 7 Oct 2026 15:11:48 -0400
Subject: [PATCH 30/31] remove dead code

---
 rocq-brick-libstdcpp/proof/pthread/inc.hpp | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/pthread/inc.hpp b/rocq-brick-libstdcpp/proof/pthread/inc.hpp
index 1d5cff3d..46ddc5be 100644
--- a/rocq-brick-libstdcpp/proof/pthread/inc.hpp
+++ b/rocq-brick-libstdcpp/proof/pthread/inc.hpp
@@ -5,8 +5,3 @@
  */
 
 #include <pthread.h>
-#include <errno.h>
-
-enum pthread_errno : int {
-    CANCELED = -1, // same as PTHREAD_CANCELED but it is not a valid way to define an enum,
-};

From c3dc661a36d6d2efb52da237e2842a38fea8a73f Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Wed, 7 Oct 2026 15:11:58 -0400
Subject: [PATCH 31/31] fix spacing

---
 rocq-brick-libstdcpp/proof/pthread/pred.v | 38 +++++++++++------------
 rocq-brick-libstdcpp/proof/pthread/spec.v |  2 +-
 2 files changed, 20 insertions(+), 20 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/pthread/pred.v b/rocq-brick-libstdcpp/proof/pthread/pred.v
index 1517bba4..109bc066 100644
--- a/rocq-brick-libstdcpp/proof/pthread/pred.v
+++ b/rocq-brick-libstdcpp/proof/pthread/pred.v
@@ -40,31 +40,31 @@ Module pthread.
       (pthread.R q id)
       (primR "unsigned long" q' arg) := {}.
 
-Section with_cpp.
-  Import rep.RepFor.
-  Import RepScheme.
+  Section with_cpp.
+    Import rep.RepFor.
+    Import RepScheme.
 
-  Context `{Σ : cpp_logic,σ : genv,!HasStdThreads Σ}.
+    Context `{Σ : cpp_logic,σ : genv,!HasStdThreads Σ}.
 
-  #[global] Instance R_learnable :
-      Cbn (Learn (learn_eq ==> any ==> learn_eq ==> learn_hints.fin) R) := ltac:(solve_learnable).
+    #[global] Instance R_learnable :
+        Cbn (Learn (learn_eq ==> any ==> learn_eq ==> learn_hints.fin) R) := ltac:(solve_learnable).
 
 
-  Definition learn_eq_dep {T U V} : Learning V → Learning (forall x : T, U x → V) :=
-    fun '{|unLearning := k|} =>
-      {|unLearning := fun L R ls => forall a a' b b', k (L a b) (R a' b') ((existT a b = existT a' b') :: ls) |}.
+    Definition learn_eq_dep {T U V} : Learning V → Learning (forall x : T, U x → V) :=
+      fun '{|unLearning := k|} =>
+        {|unLearning := fun L R ls => forall a a' b b', k (L a b) (R a' b') ((existT a b = existT a' b') :: ls) |}.
 
-  #[global] Instance handle_learnable_1 :
-    Cbn (Learn (learn_eq ==> learn_eq ==> req_eq ==> learn_eq ==> learn_hints.fin)
-           pthread.handle) := ltac:(solve_learnable).
+    #[global] Instance handle_learnable_1 :
+      Cbn (Learn (learn_eq ==> learn_eq ==> req_eq ==> learn_eq ==> learn_hints.fin)
+             pthread.handle) := ltac:(solve_learnable).
 
-  #[global] Instance handle_learnable_2 :
-    Cbn (Learn (req_eq ==> learn_eq ==> learn_eq ==> learn_eq ==> learn_hints.fin)
-           pthread.handle) := ltac:(solve_learnable).
+    #[global] Instance handle_learnable_2 :
+      Cbn (Learn (req_eq ==> learn_eq ==> learn_eq ==> learn_eq ==> learn_hints.fin)
+             pthread.handle) := ltac:(solve_learnable).
 
-  #[global] Instance repfor `{!HasStdThreads Σ} {σ : genv} :
-    rep.RepFor.C "pthread_t" [ArgType.CFrac; ArgType.Model _]
-      R := {}.
+    #[global] Instance repfor `{!HasStdThreads Σ} {σ : genv} :
+      rep.RepFor.C "pthread_t" [ArgType.CFrac; ArgType.Model _]
+        R := {}.
 
-End with_cpp.
+  End with_cpp.
 End pthread.
diff --git a/rocq-brick-libstdcpp/proof/pthread/spec.v b/rocq-brick-libstdcpp/proof/pthread/spec.v
index 476da94a..f6d9df88 100644
--- a/rocq-brick-libstdcpp/proof/pthread/spec.v
+++ b/rocq-brick-libstdcpp/proof/pthread/spec.v
@@ -27,7 +27,7 @@ Module pthread.
    *)
 
   Definition starter_kind : okind :=
-      tFunction (cc:=CC_C) "void*" ["void*"%cpp_type].
+    tFunction (cc:=CC_C) "void*" ["void*"%cpp_type].
 
   Definition starter_spec `{Σ : cpp_logic, σ : genv} `{!HasStdThreads Σ}
       (argT : tele)