specs of shared_ptr

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

@@ -8,6 +8,8 @@ Require Import skylabs.auto.cpp.spec.
 
 Require Import skylabs.cpp.spec.concepts.
 
+Set Default Goal Selector "!".
+
 NES.Begin std.allocator_traits.
 
   Class IsAllocator `{Σ : cpp_logic,σ : genv} (ty : type) :=
@@ -26,8 +28,25 @@ NES.Begin std.allocator.
   #[global] Abbreviation N ty := (Ninst "std::allocator" [Atype ty]).
   #[global] Abbreviation T ty := (Tnamed (Ninst "std::allocator" [Atype ty])).
   sl.lock Definition R `{Σ : cpp_logic,σ : genv} (ty : type) (q : cQp.t) (_ : ()) : Rep :=
-    structR (N ty) q.
-  #[only(ascfractional,cfractional,cfracvalid,type_ptr)] derive R.
+    structR (N ty) q **
+    (* libstdc++'s primary allocator inherits __new_allocator. Its void and
+       top-level cv-qualified specializations are empty, without that base.
+       A pointer to const T is not itself top-level const. *)
+    if bool_decide (drop_qualifiers ty = Tvoid \/ take_qualifiers ty <> QM)
+    then emp else
+      _base (N ty) ("std::__new_allocator".<< Atype ty >>)%cpp_name |->
+        structR ("std::__new_allocator".<< Atype ty >>)%cpp_name q.
+  #[global] Instance R_cfrac `{Σ : cpp_logic, σ : genv} ty :
+    CFractional1 (R ty).
+  Proof.
+    rewrite R.unlock.
+    destruct (bool_decide
+      (drop_qualifiers ty = Tvoid \/ take_qualifiers ty <> QM)); apply _.
+  Qed.
+  #[global] Instance R_ascfrac `{Σ : cpp_logic, σ : genv} ty :
+    AsCFractional1 (R ty).
+  Proof. solve_as_cfrac. Qed.
+  #[only(cfracvalid,type_ptr)] derive R.
 
   #[global] Instance R_agree `{Σ : cpp_logic,σ : genv} ty q1 q2 a1 a2 : Observe2 [| a1 = a2 |] (R ty q1 a1) (R ty q2 a2).
   Proof. by destruct a1,a2; apply observe_2_intro_only_provable; iIntros "? ? !%". Qed.

rocq-brick-libstdcpp/proof/dune

@@ -24,6 +24,7 @@
   Equations.Prop
   Equations.Type
   skylabs.lang.cpp
+  skylabs.cpp.stdlib
   skylabs.lang.cpp.parser.plugin
   skylabs.ltac2.logger
   skylabs.auto.core

rocq-brick-libstdcpp/proof/dune.inc

@@ -191,6 +191,24 @@
   	 (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 shared_ptr
+ (rule
+  (targets inc_shared_ptr_cpp.v.stderr inc_shared_ptr_cpp.v)
+  (alias test_ast)
+  (deps (:input inc_shared_ptr.cpp) (glob_files_rec ../*.hpp) (universe))
+  (action
+  	 (with-stderr-to inc_shared_ptr_cpp.v.stderr (run cpp2v -v %{input} -o inc_shared_ptr_cpp.v  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps inc_shared_ptr.cpp))
+)
+(subdir shared_ptr
+ (rule
+  (targets test_cpp.v.stderr test_cpp.v)
+  (alias test_ast)
+ (deps (:input test.cpp) (glob_files_rec ../*.hpp) (universe))
+  (action
+  	 (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps test.cpp))
+)
 (subdir shared_mutex
  (rule
   (targets inc_hpp.v.stderr inc_hpp.v inc_hpp_templates.v)

rocq-brick-libstdcpp/proof/shared_ptr/allocation.v

@@ -0,0 +1,155 @@
+(** Allocation ownership for the default libstdc++ shared-pointer constructors.
+    [SharedAllocationR] owns allocation tokens only. [ControlBlockRestR]
+    separately owns the implicit weak count and the remaining control-block
+    layout; neither owns payload fields or the strong-reference counter.
+
+    Custom deleters, custom allocators, aliasing constructors, and
+    make_shared_for_overwrite are not supported. The internal __sp_array_delete
+    used by shared_ptr<T[]>(new T[n]) is the library's default array deleter,
+    not support for a caller-supplied deleter.
+
+    These definitions do not prove make_shared or add an assumed factory spec.
+    They remove the requirement that a make_shared payload have its own
+    allocator token. *)
+Require Import skylabs.auto.cpp.proof.
+Require Import skylabs.brick.libstdcpp.new.pred.
+Require Import skylabs.brick.libstdcpp.shared_ptr.layout.
+
+Set Default Goal Selector "!".
+Import linearity.
+
+Inductive shared_allocation_kind : Set :=
+| SeparateAllocation
+| CombinedAllocation.
+
+(** Array factories allocate using the innermost element type. *)
+Fixpoint shared_array_element (ty : type) : type :=
+  match ty with
+  | Tarray ety _ => shared_array_element ety
+  | Tqualified cv ety => Tqualified cv (shared_array_element ety)
+  | _ => ty
+  end.
+
+Definition shared_control_name (kind : shared_allocation_kind)
+    (payload_ty : type) : name :=
+  match kind, erase_qualifiers payload_ty with
+  | SeparateAllocation, Tarray _ _ =>
+      ("std::_Sp_counted_deleter".<< Atype (Tptr (SP_element payload_ty)),
+        Atype "std::__sp_array_delete", Atype "std::allocator<void>",
+        Avalue (Eint 2 "enum __gnu_cxx::_Lock_policy") >>)%cpp_name
+  | SeparateAllocation, _ =>
+      ("std::_Sp_counted_ptr".<< Atype (Tptr payload_ty),
+        Avalue (Eint 2 "enum __gnu_cxx::_Lock_policy") >>)%cpp_name
+  | CombinedAllocation, Tarray _ _ =>
+      ("std::_Sp_counted_array".<<
+        Atype (Tnamed ("std::allocator".<<
+          Atype (shared_array_element payload_ty) >>)),
+        Avalue (Eint 2 "enum __gnu_cxx::_Lock_policy") >>)%cpp_name
+  | CombinedAllocation, _ =>
+      ("std::_Sp_counted_ptr_inplace".<< Atype payload_ty,
+        Atype "std::allocator<void>",
+        Avalue (Eint 2 "enum __gnu_cxx::_Lock_policy") >>)%cpp_name
+  end.
+
+Section with_cpp.
+  Context `{Sigma : cpp_logic} {CU : genv}.
+
+  (** Abstract physical ownership for the supported default-deleter control
+      block, not a ghost capability or an invariant assertion. The dynamic
+      class is [shared_control_name kind payload_ty]; [control] points to its
+      _Sp_counted_base subobject and [owned] is its managed object.
+
+      Own the dynamic-class/base identities, dispatch information, remaining
+      initialized fields and padding. For separate allocation this includes
+      the stored managed pointer; for in-place objects, the allocator/storage
+      bookkeeping; for combined arrays, the element count, allocator and
+      tail-layout bookkeeping consistent with [payload_ty] and [owned].
+
+      Exclude BOTH reference-counter cells, payload ownership, allocation
+      tokens and [provides_storage]: those are separate conjuncts. This token
+      contains no outstanding-handle ghost names, so repartitioning the
+      payload can preserve it unchanged. No creation, copying or disposal law
+      is assumed here. The still-assumed library constructors must establish
+      it from the control block they construct, and final release consumes it.
+
+      TOFIXLATER: define this layout ownership for each supported libstdc++
+      control-block class when proving the library bodies. This abstraction
+      does not justify virtual dispatch, combined counter loads or weak-memory
+      synchronization by itself. See shared-pointer PR #10:
+      https://github.com/SkyLabsAI/brick-libcpp/pull/10 *)
+  Parameter ControlBlockLayoutR :
+    genv -> shared_allocation_kind -> type -> ptr -> ptr -> mpred.
+
+  (** Part of the abstract field-ownership interface, not a proved layout law.
+      Timelessness permits the existing ghost-only redistribution proof; it
+      does not permit dropping ownership or removing later from arbitrary P. *)
+  #[global] Declare Instance ControlBlockLayoutR_timeless kind ty control owned :
+    Timeless (ControlBlockLayoutR CU kind ty control owned).
+
+  (** With no external weak_ptr or enable_shared_from_this, every live strong
+      ownership group retains exactly one implicit weak reference. The final
+      release takes this ownership out of the invariant before changing the
+      weak count or disposing of the control block. *)
+  Definition ControlBlockRestR (kind : shared_allocation_kind)
+      (payload_ty : type) (control owned : ptr) : mpred :=
+    control ., (SP_counted_base .:: Nid "_M_weak_count") |-> intR 1$m 1 **
+    ControlBlockLayoutR CU kind payload_ty control owned.
+
+  #[global] Instance ControlBlockRestR_timeless kind ty control owned :
+    Timeless (ControlBlockRestR kind ty control owned).
+  Proof. unfold ControlBlockRestR. apply _. Qed.
+
+  (** The storage used by _Sp_counted_ptr_inplace::_M_ptr(). Do not equate
+      the placement-constructed object pointer to this storage pointer:
+      [provides_storage] below records their relationship. *)
+  Definition shared_inplace_storage (payload_ty : type) (root : ptr) : ptr :=
+    let cn := shared_control_name CombinedAllocation payload_ty in
+    root .,(cn .:: Nid "_M_impl")
+         .,((cn .:: Nid "_Impl") .:: Nid "_M_storage")
+         .,(("__gnu_cxx::__aligned_buffer".<< Atype payload_ty >>)
+              .:: Nid "_M_storage").
+
+  Definition SharedAllocationR (kind : shared_allocation_kind)
+      (payload_ty : type) (payload_alignment : option N)
+      (control owned : ptr) : mpred :=
+    let cn := shared_control_name kind payload_ty in
+    Exists root : ptr,
+      [| control = root ,, o_base CU cn SP_counted_base |] **
+      match kind with
+      | SeparateAllocation =>
+          Exists control_alignment,
+            root |-> alloc.tokenR_with_alignment (Tnamed cn) control_alignment 1%Qp **
+            owned |-> alloc.tokenR_with_alignment payload_ty payload_alignment 1%Qp
+      | CombinedAllocation =>
+          match erase_qualifiers payload_ty with
+          | Tarray _ _ =>
+              (* _Sp_counted_array is placement-constructed in the tail of
+                 the element allocation. [offset] includes alignment padding;
+                 [total] includes both objects and any unused tail bytes.
+                 Retain the allocation at [storage], not at the tail object.
+                 std::allocator uses scalar operator new, even for an array.
+                 Keep its actual alignment argument for matching deallocation.
+                 Exact _S_tail arithmetic and the other control-block fields
+                 belong to a future verification of the library bodies. *)
+              Exists (storage : ptr) (offset total payload_size control_size : N)
+                  (alignment : option N),
+                [| size_of CU payload_ty = Some payload_size |] **
+                [| size_of CU (Tnamed cn) = Some control_size |] **
+                [| (payload_size <= offset /\ offset + control_size <= total)%N |] **
+                storage |-> allocatedR 1%Qp false alignment total **
+                root |-> new_token.R 1%Qp
+                  (new_token.mk (Tnamed cn) (storage .[ Tuchar ! Z.of_N offset ]) 0) **
+                provides_storage storage owned payload_ty
+          | _ =>
+              (* One allocation for the enclosing control block, and only a
+                 placement/storage relationship for the managed object. *)
+              Exists alignment,
+                root |-> alloc.tokenR_with_alignment (Tnamed cn) alignment 1%Qp **
+                provides_storage (shared_inplace_storage payload_ty root)
+                  owned payload_ty
+          end
+      end.
+End with_cpp.
+
+#[global] Hint Opaque SharedAllocationR ControlBlockRestR
+  ControlBlockLayoutR : sl_opacity.

rocq-brick-libstdcpp/proof/shared_ptr/allocation_test.v

@@ -0,0 +1,110 @@
+(** Regression checks for the allocation part of SharedPtrR. These are
+    representation lemmas, not proofs of C++ factories or destructors. *)
+Require Import skylabs.auto.cpp.proof.
+Require Import skylabs.brick.libstdcpp.new.pred.
+Require Import skylabs.brick.libstdcpp.shared_ptr.layout.
+Require Import skylabs.brick.libstdcpp.shared_ptr.allocation.
+
+Set Default Goal Selector "!".
+Set Warnings "+sl-transparent-constants".
+Import linearity observe2_fwd.
+
+Section with_cpp.
+  Context `{Sigma : cpp_logic} {CU : genv}.
+
+  (** The weak counter is physical ownership, not just a pure count fact.
+      The opaque remainder is returned, never manufactured or discarded. *)
+  Example control_block_rest_fields kind ty control owned :
+    ControlBlockRestR kind ty control owned -|-
+      control ., (SP_counted_base .:: Nid "_M_weak_count") |-> intR 1$m 1 **
+      ControlBlockLayoutR CU kind ty control owned.
+  Proof. reflexivity. Qed.
+
+  #[local] Instance int_cell_exclusive (p : ptr) :
+    Observe2 False (p |-> intR 1$m 1) (p |-> intR 1$m 1).
+  Proof. apply _. Qed.
+  #[local] Definition int_cell_exclusive_F :=
+    ltac:(mk_obs2_fwd int_cell_exclusive).
+
+  Example control_block_rest_not_duplicable kind ty control owned :
+    ControlBlockRestR kind ty control owned **
+    ControlBlockRestR kind ty control owned |-- False.
+  Proof.
+    unfold ControlBlockRestR.
+    go using int_cell_exclusive_F.
+  Qed.
+
+  (** The ordinary new/new[] route retains both allocation tokens. *)
+  Example separate_allocations (ty : type) (root owned : ptr)
+      (control_alignment payload_alignment : option N) :
+    root |-> alloc.tokenR_with_alignment
+      (Tnamed (shared_control_name SeparateAllocation ty)) control_alignment 1 **
+    owned |-> alloc.tokenR_with_alignment ty payload_alignment 1
+    |-- SharedAllocationR SeparateAllocation ty payload_alignment
+          (root ,, o_base CU (shared_control_name SeparateAllocation ty)
+            SP_counted_base) owned.
+  Proof.
+    unfold SharedAllocationR.
+    rewrite <- (bi.exist_intro root).
+    rewrite <- (bi.exist_intro control_alignment).
+    go.
+  Qed.
+
+  (** A combined named object needs no token allocating the payload itself. *)
+  Example combined_object (nm : name) (root owned : ptr)
+      (alignment : option N) :
+    root |-> alloc.tokenR_with_alignment
+      (Tnamed (shared_control_name CombinedAllocation (Tnamed nm))) alignment 1 **
+    provides_storage (shared_inplace_storage (Tnamed nm) root) owned (Tnamed nm)
+    |-- SharedAllocationR CombinedAllocation (Tnamed nm) None
+          (root ,, o_base CU
+            (shared_control_name CombinedAllocation (Tnamed nm)) SP_counted_base)
+          owned.
+  Proof.
+    unfold SharedAllocationR.
+    rewrite <- (bi.exist_intro root).
+    cbn [erase_qualifiers].
+    rewrite <- (bi.exist_intro alignment).
+    go.
+  Qed.
+
+  (** The array allocation is owned at its beginning, not at the control block
+      placed after the last element. The count remains in [Tarray ety len]. *)
+  Example combined_array (ety : type) (len : N) (storage root owned : ptr)
+      (offset total payload_size control_size : N)
+      (alignment : option N)
+      (cn := shared_control_name CombinedAllocation (Tarray ety len)) :
+    size_of CU (Tarray ety len) = Some payload_size ->
+    size_of CU (Tnamed cn) = Some control_size ->
+    (payload_size <= offset /\ offset + control_size <= total)%N ->
+    storage |-> allocatedR 1 false alignment total **
+    root |-> new_token.R 1
+      (new_token.mk (Tnamed cn) (storage .[ Tuchar ! Z.of_N offset ]) 0) **
+    provides_storage storage owned (Tarray ety len)
+    |-- SharedAllocationR CombinedAllocation (Tarray ety len) None
+          (root ,, o_base CU cn SP_counted_base) owned.
+  Proof.
+    intros Hpayload Hcontrol Hbounds.
+    unfold SharedAllocationR.
+    rewrite <- (bi.exist_intro root).
+    cbn [erase_qualifiers].
+    rewrite <- (bi.exist_intro storage), <- (bi.exist_intro offset),
+      <- (bi.exist_intro total), <- (bi.exist_intro payload_size),
+      <- (bi.exist_intro control_size), <- (bi.exist_intro alignment).
+    go.
+  Qed.
+End with_cpp.
+
+(** Template arguments must preserve const, unlike erased heap types. *)
+Example const_array_control_name :
+  shared_control_name SeparateAllocation "const int[2]" =
+    ("std::_Sp_counted_deleter".<< Atype "const int*",
+      Atype "std::__sp_array_delete", Atype "std::allocator<void>",
+      Avalue (Eint 2 "enum __gnu_cxx::_Lock_policy") >>)%cpp_name.
+Proof. reflexivity. Qed.
+
+Example const_array_factory_control_name :
+  shared_control_name CombinedAllocation "const int[2]" =
+    ("std::_Sp_counted_array".<< Atype "std::allocator<const int>",
+      Avalue (Eint 2 "enum __gnu_cxx::_Lock_policy") >>)%cpp_name.
+Proof. reflexivity. Qed.

rocq-brick-libstdcpp/proof/shared_ptr/assignment.v

@@ -0,0 +1,49 @@
+(** Same-type copy assignment between distinct handles. This is an assumed
+    library interface, not a verification of libstdc++'s reference counting.
+
+    The source is nonempty; the destination may be empty. The old destination
+    payload piece is required because assignment can destroy that payload.
+    A fresh source slot is required before the old slot is refunded: libstdc++
+    increments the new counter before releasing the old one. The source's
+    own payload piece is neither required nor duplicated.
+
+    Distinct handles sharing one control block are allowed. In that case the
+    implementation leaves the counter unchanged; the logical transition
+    exchanges the old destination piece for the requested available piece.
+    Separating full destination ownership from source ownership excludes
+    self-assignment. Empty sources and aliasing/custom-deleter shared_ptrs
+    are outside this interface. *)
+Require Import skylabs.auto.cpp.proof.
+Require Import skylabs.brick.libstdcpp.shared_ptr.specs.
+
+Set Default Goal Selector "!".
+Set Warnings "+sl-transparent-constants".
+
+Section with_cpp.
+  Context `{Sigma : cpp_logic, MOD : inc_shared_ptr_cpp.source ⊧ σ}.
+  Context (ty : type).
+  #[local] Notation spty := ("std::shared_ptr".<< Atype ty >>)%cpp_name.
+
+  Definition copy_assign :=
+    specify.template.op spty OOEqual function_qualifiers.N
+      (Tref (Tnamed spty)) [Tref (Tconst (Tnamed spty))] $
+      \this this
+      \arg{other : ptr} "other" (Vref other)
+      \prepost{q id source_piece p Rpiece}
+        other |-> SharedPtrR ty q id source_piece Rpiece p
+      \pre{pieceid} pieceRight id pieceid
+      \pre [| (N.of_nat pieceid < N.pos maxContention)%N |]
+      \pre{(old_null : bool) old_id old_piece oldp oldR}
+        if old_null then this |-> NullSharedPtrR ty 1$m
+        else this |-> SharedPtrR ty 1$m old_id old_piece oldR oldp **
+          oldp |-> oldR old_piece
+      \post[Vref this]
+        this |-> SharedPtrR ty 1$m id pieceid Rpiece p **
+        p |-> Rpiece pieceid **
+        if old_null then emp else pieceRight old_id old_piece.
+
+  Definition SpecFor_copy_assign := RegisterSpec copy_assign.
+  #[global] Existing Instance SpecFor_copy_assign.
+End with_cpp.
+
+#[global] Hint Opaque copy_assign : sl_opacity.