spec for thread creation with pthread.h

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)

rocq-brick-libstdcpp/proof/pthread/hints.v

@@ -0,0 +1,70 @@
+(*
+ * 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 : tele)
+      (Pre : ptr -> argT -> mpred)
+      (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' Pre' Post' :=
+    \cancelx
+    \using P
+    \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 → 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' |]
+    \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.

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>

rocq-brick-libstdcpp/proof/pthread/pred.v

@@ -0,0 +1,70 @@
+(*
+ * 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.
+
+Import wrap.
+
+Module pthread.
+
+  Record gname := { _ghost : iprop.gname }.
+
+  (** [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)
+                       (Post : 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 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 repfor `{!HasStdThreads Σ} {σ : genv} :
+      rep.RepFor.C "pthread_t" [ArgType.CFrac; ArgType.Model _]
+        R := {}.
+
+  End with_cpp.
+End pthread.

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

@@ -0,0 +1,104 @@
+(*
+ * 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.
+
+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 : tele)
+      (Pre : ptr -> argT -> mpred)
+      (Post : ptr -> argT -> thread_idT -> mpred) : WpSpec_cpp_val :=
+    \arg{argp} "arg" (Vptr argp)
+    \prepost{tid} current_thread tid
+    \pre{arg} Pre argp arg
+    \post[Vptr nullptr] Post argp arg tid.
+
+  mlock
+  Definition starter_specR `{Σ : cpp_logic, σ : genv} `{!HasStdThreads Σ}
+      (argT : tele)
+      (Pre : ptr -> argT -> mpred)
+      (Post : ptr -> argT -> thread_idT -> mpred) : Rep :=
+    unmaterialized_specR starter_kind
+      (starter_spec argT Pre Post)  .
+
+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
+     with ( \arg{idp}        "tid"   (Vptr idp)
+            \pre{id0}         idp |-> oprimR "unsigned long" 1$m id0
+            \arg             "attr"  (Vptr nullptr)
+            \arg{starterp}   "start" (Vptr starterp)
+            \with argT Pre Post
+            \pre              starterp |-> starter_specR argT Pre Post
+            \arg{argp}       "arg"   (Vptr argp)
+            \pre{arg : argT}  Pre argp arg
+            \with this_thread
+            \prepost          current_thread this_thread
+            \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,
+                   pthread.handle γt this_thread tid (Post argp arg tid) ∗
+                   idp |-> pthread.R 1$m tid
+               else
+                 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           "ret"   (Vptr nullptr)
+            \prepost{this_thread} current_thread this_thread
+            \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 *)
+                 P ).
+
+End with_cpp.
+End pthread.

rocq-brick-libstdcpp/proof/runtime/objective.v

@@ -0,0 +1,123 @@
+
+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.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 :
+      LocalWith procTI (tptsto ty q p a).
+  #[global] Declare Instance padding_pd_local_weakly_obj q cls :
+      LocalWithR procTI (structR cls q).
+  #[global] Declare Instance mdc_path_pd_local_weakly_obj n path q p :
+      LocalWith procTI (mdc_path n path q p).
+  #[global] Declare Instance type_ptr_pd_local_weakly_obj p ty :
+      LocalWith procTI (type_ptr ty p).
+  #[global] Declare Instance valid_ptr_pd_local_weakly_obj p ty :
+      LocalWith procTI (_valid_ptr ty p).
+  #[global] Declare Instance anyR_pd_local_weakly_obj ty q :
+      LocalWithR procTI (anyR ty q).
+  #[global] Declare Instance has_type_pd_weakly_obj v ty :
+      LocalWith 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 derived_local_withR.
+  Context `{Σ : !cpp_logic ti Σ0, σ : genv, !HasStdThreads Σ}.
+  Implicit Types p : ptr.
+
+  #[global] Instance validR_pd_local_obj :
+    LocalWithR procTI validR.
+  Proof.
+    rewrite LocalWithR_iff_LocalWith_at => p.
+    rewrite _at_validR; apply _.
+  Qed.
+
+  #[global] Instance tptstoR_pd_local_obj ty q v :
+    LocalWithR procTI (tptstoR ty q v).
+  Proof.
+    rewrite LocalWithR_iff_LocalWith_at => p.
+    rewrite _at_tptstoR; apply _.
+  Qed.
+
+  #[global] Instance tptsto_fuzzyR_pd_local_obj ty q v :
+    LocalWithR procTI (tptsto_fuzzyR ty q v).
+  Proof.
+    rewrite LocalWithR_iff_LocalWith_at => p.
+    rewrite _at_tptsto_fuzzyR; apply _.
+  Qed.
+
+  #[global] Instance primR_pd_local_obj ty q v :
+    LocalWithR procTI (primR ty q v).
+  Proof.
+    rewrite LocalWithR_iff_LocalWith_at => p.
+    rewrite _at_primR; apply _.
+  Qed.
+
+  #[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_obj ty :
+    LocalWithR procTI (type_ptrR ty).
+  Proof. rewrite type_ptrR_eq /type_ptrR_def. apply _. Qed.
+
+  #[global] Instance derivationR_pd_local_obj n path q :
+    LocalWithR procTI (derivationR n path q).
+  Proof. rewrite derivationR.unlock. apply _. Qed.
+
+  (** 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) :
+    (∀ 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_local_withR | apply _ ].
+    rewrite big_opL_fmap.
+    apply _.
+  Qed.
+
+  (** 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) :
+    (∀ x, LocalWithR procTI (Rs x)) →
+    LocalWithR procTI (array_sliceR ty m n Rs xs).
+  Proof.
+    intros HR.
+    rewrite array_sliceR.unlock.
+    apply sep_local_withR; first apply _.
+    apply LocalWithR_offsetR, arrayR_pd_local_obj_lookup => x.
+    apply _.
+  Qed.
+
+  #[global] Instance arrayR_pd_local_obj
+    {X} ty (Rs : X → Rep) (xs : list X)
+    `{∀ (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_obj
+    {X} ty (Rs : X → Rep) (xs : list X) m n
+    `{∀ (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_local_withR.