diff --git a/rocq-brick-libstdcpp/proof/allocator/spec.v b/rocq-brick-libstdcpp/proof/allocator/spec.v
index d05df081..09e29c09 100644
--- a/rocq-brick-libstdcpp/proof/allocator/spec.v
+++ b/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.
diff --git a/rocq-brick-libstdcpp/proof/dune b/rocq-brick-libstdcpp/proof/dune
index 55024d2c..fdc513f9 100644
--- a/rocq-brick-libstdcpp/proof/dune
+++ b/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
diff --git a/rocq-brick-libstdcpp/proof/dune.inc b/rocq-brick-libstdcpp/proof/dune.inc
index 52ff904b..6710d779 100644
--- a/rocq-brick-libstdcpp/proof/dune.inc
+++ b/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)
diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/allocation.v b/rocq-brick-libstdcpp/proof/shared_ptr/allocation.v
new file mode 100644
index 00000000..837bf9e0
--- /dev/null
+++ b/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.
diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/allocation_test.v b/rocq-brick-libstdcpp/proof/shared_ptr/allocation_test.v
new file mode 100644
index 00000000..627224fa
--- /dev/null
+++ b/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.
diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/assignment.v b/rocq-brick-libstdcpp/proof/shared_ptr/assignment.v
new file mode 100644
index 00000000..ebc8191b
--- /dev/null
+++ b/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.
diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/assignment_test.v b/rocq-brick-libstdcpp/proof/shared_ptr/assignment_test.v
new file mode 100644
index 00000000..87481569
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/shared_ptr/assignment_test.v
@@ -0,0 +1,55 @@
+(** Checks spec discovery, fractional source ownership, the returned reference,
+    and old-piece refund. Library operation bodies remain assumed. *)
+Require Import skylabs.auto.cpp.proof.
+Require Import skylabs.lang.cpp.parser.plugin.cpp2v.
+Require Import skylabs.brick.libstdcpp.shared_ptr.assignment.
+Require Import skylabs.brick.libstdcpp.shared_ptr.specs.
+
+Set Default Goal Selector "!".
+Set Warnings "+sl-transparent-constants".
+Import linearity.
+#[local] Hint Resolve UNSAFE_read_prim_cancel : sl_opacity.
+Remove Hints _at_pick_cfrac_and_split_C _at_pick_frac_and_split_C
+  _at_split_specific_cfrac_C _at_split_specific_frac_C
+  : db_skylabs_syntactic.
+
+#[elaborate]
+cpp.prog source prog cpp:{{
+#include <memory>
+std::shared_ptr<int>& assign(std::shared_ptr<int>& destination,
+                             std::shared_ptr<int> const& source) {
+    return destination = source;
+}
+}}.
+
+Section with_cpp.
+  Context `{Sigma : cpp_logic, MOD : source ⊧ σ}.
+  #[local] Instance learn_shared : LearnEq6 SharedPtrR :=
+    ltac:(solve_learnable).
+
+  cpp.spec "assign(std::shared_ptr<int>&, const std::shared_ptr<int>&)"
+    from source as assign_spec with (
+      \arg{dest : ptr} "destination" (Vref dest)
+      \arg{other : ptr} "source" (Vref other)
+      \prepost{q id source_piece p Rpiece}
+        other |-> SharedPtrR "int" 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 dest |-> NullSharedPtrR "int" 1$m
+        else dest |-> SharedPtrR "int" 1$m old_id old_piece oldR oldp **
+          oldp |-> oldR old_piece
+      \post[Vref dest]
+        dest |-> SharedPtrR "int" 1$m id pieceid Rpiece p **
+        p |-> Rpiece pieceid **
+        if old_null then emp else pieceRight old_id old_piece
+    ).
+
+  Lemma assign_ok : verify[source] assign_spec.
+  Proof using MOD.
+    verify_spec.
+    go.
+    iExists pieceid, old_null, old_id, old_piece, oldp, oldR.
+    go.
+  Qed.
+End with_cpp.
diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/fractional_copy.v b/rocq-brick-libstdcpp/proof/shared_ptr/fractional_copy.v
new file mode 100644
index 00000000..423897fc
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/shared_ptr/fractional_copy.v
@@ -0,0 +1,94 @@
+(** Copying a shared handle only reads that handle. This client regression
+    keeps its ownership fractional and checks that destroying the new copy
+    returns the payload-acquisition token. It assumes the library operations;
+    it does not verify libstdc++'s atomic reference-count implementation. *)
+Require Import skylabs.auto.cpp.proof.
+Require Import skylabs.auto.invariants.
+Require Import skylabs.lang.cpp.parser.plugin.cpp2v.
+Require Import skylabs.brick.libstdcpp.shared_ptr.specs.
+
+Set Default Goal Selector "!".
+Import linearity.
+#[local] Hint Resolve UNSAFE_read_prim_cancel : sl_opacity.
+Remove Hints _at_pick_cfrac_and_split_C _at_pick_frac_and_split_C
+  _at_split_specific_cfrac_C _at_split_specific_frac_C
+  : db_skylabs_syntactic.
+
+#[elaborate]
+cpp.prog source prog cpp:{{
+#include <memory>
+void copy_then_destroy(std::shared_ptr<int> const& source) {
+    auto copy = source;
+}
+}}.
+
+Section with_cpp.
+  Context `{Sigma : cpp_logic, MOD : source ⊧ σ}.
+
+  #[local] Hint Opaque SharedPtrR pieceRight : sl_opacity.
+  #[local] Instance learn_shared : LearnEq6 SharedPtrR :=
+    ltac:(solve_learnable).
+
+  cpp.spec "copy_then_destroy(const std::shared_ptr<int>&)"
+    from source as copy_then_destroy_spec with (
+      \arg{other : ptr} "source" (Vref other)
+      \prepost{q id source_pieceid p Rpiece}
+        other |-> SharedPtrR "int" q id source_pieceid Rpiece p
+      \prepost{pieceid} pieceRight id pieceid
+      \pre [| (N.of_nat pieceid < N.pos maxContention)%N |]
+      \post emp
+    ).
+
+  Lemma copy_then_destroy_ok : verify[source] copy_then_destroy_spec.
+  Proof using MOD.
+    verify_spec.
+    go.
+    iExists q, false, id, source_pieceid, p, Rpiece, pieceid.
+    go.
+    iExists false, p, (id, pieceid), Rpiece.
+    go.
+  Qed.
+
+  cpp.spec "copy_then_destroy(const std::shared_ptr<int>&)"
+    from source as copy_then_destroy_empty_spec with (
+      \arg{other : ptr} "source" (Vref other)
+      \prepost{q} other |-> NullSharedPtrR "int" q
+      \post emp
+    ).
+
+  (** Uses ordinary spec discovery, not an extra null-only RegisterSpec. *)
+  Lemma copy_then_destroy_empty_ok : verify[source] copy_then_destroy_empty_spec.
+  Proof using MOD.
+    verify_spec.
+    go.
+    iExists q, true,
+      {| pieceRightLocs := []; pieceHandleLocs := [];
+         dataLoc := nullptr; payload_type := Tint; payload_delete := None |},
+      0%nat, nullptr, (fun _ => emp), 0%nat.
+    go.
+    iExists true, nullptr, tt, (fun _ => emp).
+    go.
+  Qed.
+
+  (* A destruction capability may recover its payload from an invariant.
+     This is the pointwise obligation in [payload_destructible], not a rule
+     turning arbitrary class bytes into a valid destructor precondition. *)
+  Lemma guarded_int_destroy (p : ptr) (gamma : gname) :
+    cinv nroot gamma (p |-> anyR "int" 1$m) ** cinv_own gamma 1
+    |-- destroy_val (genv_tu σ) "int" p emp.
+  Proof using MOD.
+    rewrite <- fupd_destroy_val.
+    eapply cinv_cancel_fwd with (P' := emp).
+    { set_solver. }
+    { go. }
+    {
+      rewrite <- fupd_destroy_val.
+      apply timeless_unlater.
+      { apply _. }
+      etrans.
+      2: { apply fupd_intro. }
+      rewrite destroy_val_wp_destroy_val.
+      go.
+    }
+  Qed.
+End with_cpp.
diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/handle_liveness.v b/rocq-brick-libstdcpp/proof/shared_ptr/handle_liveness.v
new file mode 100644
index 00000000..10dc2746
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/shared_ptr/handle_liveness.v
@@ -0,0 +1,125 @@
+(** The indexed handle token has two jobs: identify the payload piece required
+    at destruction, and exclude a released control block while any fraction
+    of a handle remains live. These are representation lemmas, independent of
+    the assumed C++ library method specs. *)
+Require Import skylabs.auto.cpp.proof.
+Require Import skylabs.brick.libstdcpp.shared_ptr.specs.
+
+Set Default Goal Selector "!".
+Import linearity observe2_fwd.
+
+Section with_cpp.
+  Context `{Sigma : cpp_logic} {CU : genv}.
+  #[local] Existing Instance br.ghost.frac_inG.
+  #[local] Hint Opaque pieceHandle pieceRight SharedPtrR sptrInv
+    payload_destructible : sl_opacity.
+
+  Lemma sptrInv_retired id Rpiece owned pieceOut :
+    countLN pieceOut allPieceIds = 0%N ->
+    sptrInv id Rpiece owned pieceOut -|-
+      ([∗ list] pieceid ∈ allPieceIds,
+        if pieceOut pieceid then pieceRight id pieceid
+        else pieceHandle id 1 pieceid).
+  Proof.
+    intro Hzero.
+    unfold sptrInv. rewrite Hzero bool_decide_true; [|reflexivity].
+    apply bi.sep_emp.
+  Qed.
+
+  Lemma pieceHandle_full_conflict id q i :
+    pieceHandle id q i ** pieceHandle id 1 i |-- False.
+  Proof.
+    unfold pieceHandle.
+    destruct (nth_error (pieceHandleLocs id) i) as [name |].
+    {
+      rewrite <- own_op, own_valid, algebra.discrete_validI.
+      apply bi.pure_mono.
+      exact (Qp.not_add_le_r q 1).
+    }
+    { go. }
+  Qed.
+
+  #[local] Definition pieceHandle_full_conflict_F :=
+    [FWD] pieceHandle_full_conflict.
+
+  (* An available slot owns the full token inside the invariant. Hence even
+     read-only fractional ownership of a handle excludes that state. *)
+  Lemma pieceHandle_outstanding id q i Rpiece owned pieceOut :
+    i ∈ allPieceIds ->
+    pieceHandle id q i ** sptrInv id Rpiece owned pieceOut
+    |-- [| pieceOut i = true |] **
+        pieceHandle id q i ** sptrInv id Rpiece owned pieceOut.
+  Proof.
+    intros Hi.
+    destruct (pieceOut i) eqn:Hout.
+    { go. }
+    unfold sptrInv.
+    rewrite -> big_op.big_sepL_difference_singleton with (x := i).
+    2: { exact Hi. }
+    2: { unfold allPieceIds. apply NoDup_seq. }
+    rewrite Hout.
+    go using pieceHandle_full_conflict_F.
+  Qed.
+
+  Lemma countLN_positive_of_member {A} (f : A -> bool) l i :
+    i ∈ l -> f i = true -> (0 < countLN f l)%N.
+  Proof.
+    intros Hi Hout.
+    assert (Hin : i ∈ filter f l).
+    {
+      apply list_elem_of_filter. split.
+      { by rewrite Hout. }
+      { exact Hi. }
+    }
+    unfold countLN.
+    destruct (filter f l) as [| head rest].
+    { inversion Hin. }
+    { unfold lengthN. simpl. lia. }
+  Qed.
+
+  Lemma pieceHandle_live id q i Rpiece owned pieceOut :
+    i ∈ allPieceIds ->
+    pieceHandle id q i ** sptrInv id Rpiece owned pieceOut
+    |-- [| (0 < countLN pieceOut allPieceIds)%N |] **
+        pieceHandle id q i ** sptrInv id Rpiece owned pieceOut.
+  Proof.
+    intros Hi.
+    etrans.
+    { exact (pieceHandle_outstanding id q i Rpiece owned pieceOut Hi). }
+    go using countLN_positive_of_member.
+  Qed.
+
+  #[local] Lemma pieceHandle_live_observe id q i Rpiece owned pieceOut :
+    i ∈ allPieceIds ->
+    Observe2 [| (0 < countLN pieceOut allPieceIds)%N |]
+      (pieceHandle id q i) (sptrInv id Rpiece owned pieceOut).
+  Proof.
+    intros Hi.
+    apply observe_2_intro.
+    { apply _. }
+    apply bi.wand_intro_r.
+    etrans.
+    { exact (pieceHandle_live id q i Rpiece owned pieceOut Hi). }
+    go.
+  Qed.
+  #[local] Definition pieceHandle_live_F :=
+    ltac:(mk_obs2_fwd pieceHandle_live_observe).
+
+  Lemma allPieceIds_member i :
+    (N.of_nat i < N.pos maxContention)%N -> i ∈ allPieceIds.
+  Proof.
+    unfold allPieceIds. rewrite elem_of_seq. lia.
+  Qed.
+  #[local] Hint Resolve allPieceIds_member : pure.
+
+  Lemma SharedPtrR_live ty q id i Rpiece owned (handle : ptr) pieceOut :
+    handle |-> SharedPtrR ty q id i Rpiece owned **
+    sptrInv id Rpiece owned pieceOut
+    |-- [| (0 < countLN pieceOut allPieceIds)%N |] **
+        handle |-> SharedPtrR ty q id i Rpiece owned **
+        sptrInv id Rpiece owned pieceOut.
+  Proof.
+    unfold SharedPtrR.
+    go using pieceHandle_live_F.
+  Qed.
+End with_cpp.
diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/inc_shared_ptr.cpp b/rocq-brick-libstdcpp/proof/shared_ptr/inc_shared_ptr.cpp
new file mode 100644
index 00000000..5112bd81
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/shared_ptr/inc_shared_ptr.cpp
@@ -0,0 +1,8 @@
+#include <memory>
+#include <limits>
+#include <type_traits>
+
+// specs.v reserves one piece index per representable positive strong count.
+// Check the libstdc++ ABI rather than inferring this bound from pointer size.
+static_assert(std::is_same_v<_Atomic_word, int>);
+static_assert(std::numeric_limits<_Atomic_word>::max() == 2147483647);
diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/layout.v b/rocq-brick-libstdcpp/proof/shared_ptr/layout.v
new file mode 100644
index 00000000..ac9aef3f
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/shared_ptr/layout.v
@@ -0,0 +1,172 @@
+(** The LP64 libstdc++ handle layout for the atomic lock policy. The pointee and
+    control block are not subobjects of the handle. *)
+Require Import skylabs.auto.cpp.proof.
+Require Import skylabs.auto.cpp.hints.const.
+Require Import Stdlib.FSets.FMapFacts.
+
+Set Default Goal Selector "!".
+Import linearity.
+
+Definition SP_name (ty : type) : name :=
+  ("std::shared_ptr".<< Atype ty >>)%cpp_name.
+
+Definition SP_impl (ty : type) : name :=
+  ("std::__shared_ptr".<< Atype ty,
+    Avalue (Eint 2 "enum __gnu_cxx::_Lock_policy") >>)%cpp_name.
+
+Definition SP_acc (ty : type) (is_array : Z) : name :=
+  ("std::__shared_ptr_access".<< Atype ty,
+    Avalue (Eint 2 "enum __gnu_cxx::_Lock_policy"),
+    Avalue (Eint is_array "bool"),
+    Avalue (Eint (if bool_decide (erase_qualifiers ty = Tvoid) then 1 else 0)
+      "bool") >>)%cpp_name.
+
+Definition SP_access (ty : type) : name :=
+  SP_acc ty (if is_array_type (erase_qualifiers ty) then 1 else 0).
+
+Definition SP_count : name :=
+  ("std::__shared_count".<<
+    Avalue (Eint 2 "enum __gnu_cxx::_Lock_policy") >>)%cpp_name.
+
+Definition SP_counted_base : name :=
+  ("std::_Sp_counted_base".<<
+    Avalue (Eint 2 "enum __gnu_cxx::_Lock_policy") >>)%cpp_name.
+
+(** [shared_ptr<T[]>] stores [T*], not a pointer to an array. Keep cv qualifiers when
+    removing exactly one array extent. *)
+Fixpoint SP_element (ty : type) : type :=
+  match ty with
+  | Tarray ety _ | Tincomplete_array ety | Tvariable_array ety _ => ety
+  | Tqualified cv ty => Tqualified cv (SP_element ty)
+  | _ => ty
+  end.
+
+Section with_cpp.
+  Context `{Sigma : cpp_logic} {CU : genv}.
+
+  Definition SharedPtrHandleR (ty : type) (q : cQp.t)
+      (owned control : ptr) : Rep :=
+    structR (SP_name ty) q **
+    _base (SP_name ty) (SP_impl ty) |->
+      (structR (SP_impl ty) q **
+       _base (SP_impl ty) (SP_access ty) |-> structR (SP_access ty) q **
+       _field (SP_impl ty .:: Nid "_M_ptr") |->
+         primR (Tptr (erase_qualifiers (SP_element ty))) q (Vptr owned) **
+       _field (SP_impl ty .:: Nid "_M_refcount") |->
+         (structR SP_count q **
+          _field (SP_count .:: Nid "_M_pi") |->
+            primR (Tptr (Tnamed SP_counted_base)) q (Vptr control))).
+
+  #[global] Instance SharedPtrHandleR_fractional ty owned control :
+    CFractional (fun q => SharedPtrHandleR ty q owned control) := _.
+
+  #[global] Instance SharedPtrHandleR_typeptr ty q owned control :
+    Observe (type_ptrR (Tnamed (SP_name ty)))
+      (SharedPtrHandleR ty q owned control) := _.
+End with_cpp.
+
+#[global] Hint Opaque SharedPtrHandleR : sl_opacity.
+
+(** A small type table makes LP64 ABI agreement an explicit, decidable obligation
+    of clients. No declaration about the managed object is needed. *)
+Definition SP_count_struct : Struct :=
+  Build_Struct []
+    [mkMember (field_name.Id "_M_pi") (Tptr (Tnamed SP_counted_base))
+      false None (Build_LayoutInfo 0)]
+    [] [] (SP_count .:: Ndtor) false None Standard 8 8.
+
+Definition SP_access_struct (ty : type) : Struct :=
+  Build_Struct [] [] [] []
+    (SP_access ty .:: Ndtor) true None POD 1 1.
+
+Definition SP_impl_struct (ty : type) : Struct :=
+  Build_Struct [(SP_access ty, Build_LayoutInfo 0)]
+    [mkMember (field_name.Id "_M_ptr") (Tptr (SP_element ty))
+       false None (Build_LayoutInfo 0);
+     mkMember (field_name.Id "_M_refcount") (Tnamed SP_count)
+       false None (Build_LayoutInfo 64)]
+    [] [] (SP_impl ty .:: Ndtor) false None Standard 16 8.
+
+Definition SP_outer_struct (ty : type) : Struct :=
+  Build_Struct [(SP_impl ty, Build_LayoutInfo 0)] [] [] []
+    (SP_name ty .:: Ndtor) false None Standard 16 8.
+
+Definition shared_ptr_const_tu (ty : type) : translation_unit :=
+  makeTranslationUnit empty
+    (NM.add (SP_name ty) (Gstruct (SP_outer_struct ty))
+      (NM.add (SP_impl ty) (Gstruct (SP_impl_struct ty))
+        (NM.add (SP_access ty) (Gstruct (SP_access_struct ty))
+          (NM.add SP_count (Gstruct SP_count_struct) empty))))
+    empty [] [] abi.abi_default empty empty empty empty.
+
+Module SPNameMapFacts := WFacts_fun NM.E NM.
+
+#[local] Lemma SP_lookup_outer ty :
+  (shared_ptr_const_tu ty).(types) !! SP_name ty =[Vm?]=>
+    Some (Gstruct (SP_outer_struct ty)).
+Proof.
+  rewrite VmEq_eq_iff.
+  change (NM.find (SP_name ty) (types (shared_ptr_const_tu ty)) =
+    Some (Gstruct (SP_outer_struct ty))).
+  apply SPNameMapFacts.add_eq_o.
+  apply NM.E.eq_refl.
+Qed.
+
+#[local] Lemma SP_lookup_impl ty :
+  (shared_ptr_const_tu ty).(types) !! SP_impl ty =[Vm?]=>
+    Some (Gstruct (SP_impl_struct ty)).
+Proof.
+  rewrite VmEq_eq_iff.
+  change (NM.find (SP_impl ty) (types (shared_ptr_const_tu ty)) =
+    Some (Gstruct (SP_impl_struct ty))).
+  rewrite SPNameMapFacts.add_neq_o.
+  { apply SPNameMapFacts.add_eq_o, NM.E.eq_refl. }
+  { intro H. apply NM.eqL in H. discriminate. }
+Qed.
+
+#[local] Lemma SP_lookup_access ty :
+  (shared_ptr_const_tu ty).(types) !! SP_access ty =[Vm?]=>
+    Some (Gstruct (SP_access_struct ty)).
+Proof.
+  rewrite VmEq_eq_iff.
+  change (NM.find (SP_access ty) (types (shared_ptr_const_tu ty)) =
+    Some (Gstruct (SP_access_struct ty))).
+  unfold shared_ptr_const_tu. cbn [types].
+  rewrite -> SPNameMapFacts.add_neq_o,
+    SPNameMapFacts.add_neq_o.
+  { apply SPNameMapFacts.add_eq_o, NM.E.eq_refl. }
+  { intro H. apply NM.eqL in H. discriminate. }
+  { intro H. apply NM.eqL in H. discriminate. }
+Qed.
+
+#[local] Lemma SP_lookup_count ty :
+  (shared_ptr_const_tu ty).(types) !! SP_count =[Vm?]=>
+    Some (Gstruct SP_count_struct).
+Proof.
+  rewrite VmEq_eq_iff.
+  change (NM.find SP_count (types (shared_ptr_const_tu ty)) =
+    Some (Gstruct SP_count_struct)).
+  unfold shared_ptr_const_tu. cbn [types].
+  rewrite -> SPNameMapFacts.add_neq_o,
+    SPNameMapFacts.add_neq_o, SPNameMapFacts.add_neq_o.
+  { apply SPNameMapFacts.add_eq_o, NM.E.eq_refl. }
+  { intro H. apply NM.eqL in H. discriminate. }
+  { intro H. apply NM.eqL in H. discriminate. }
+  { intro H. apply NM.eqL in H. discriminate. }
+Qed.
+
+#[local] Hint Resolve SP_lookup_outer SP_lookup_impl SP_lookup_access
+  SP_lookup_count | 0 : typeclass_instances sl_opacity.
+
+Section const.
+  Context `{Sigma : cpp_logic} {CU : genv}.
+
+  Lemma SharedPtrHandleR_const ty owned control :
+    const.CONST (shared_ptr_const_tu ty) (Tnamed (SP_name ty))
+      (fun q => SharedPtrHandleR ty q owned control).
+  Proof.
+    const.prove.
+    unfold SharedPtrHandleR.
+    go.
+  Qed.
+End const.
diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/make_shared.v b/rocq-brick-libstdcpp/proof/shared_ptr/make_shared.v
new file mode 100644
index 00000000..1e5ce058
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/shared_ptr/make_shared.v
@@ -0,0 +1,105 @@
+(** The normal-return interface of the non-array std::make_shared<T>, using
+    the C++20 construct_at interface for its initialization obligation.
+
+    Construction is NOT an axiom saying that arbitrary payload ownership can
+    be created. The caller supplies a spec for the actual construct_at<T,
+    Args...> specialization, including its forwarded arguments and side
+    effects. That obligation must be proved from the payload initialization,
+    using the payload's constructor specs. In particular, a forwarding
+    reference to a shared_ptr can cause a by-value constructor argument copy;
+    its copy credit belongs in [before], not in a hidden assumption.
+
+    This file specifies, but does not verify, libstdc++'s allocation and
+    control-block implementation. Allocation failure is not excluded by a
+    normal-return postcondition. Arrays, custom allocators/deleters, aliasing,
+    weak_ptr, enable_shared_from_this, and make_shared_for_overwrite are outside
+    this factory spec. The pure inheritance guard excludes the additional
+    weak-handle initialization performed after constructing such a payload.
+    The allocation representation still covers both array layouts; this file
+    adds no array-factory spec.
+
+    Unlike raw-pointer adoption, the combined-allocation factory intentionally
+    relinquishes the placement payload's [new_token.R] metadata: it calls the
+    destructor explicitly, not delete on the interior payload. The underlying
+    affine logic permits discarding this metadata. The enclosing allocation
+    token and [provides_storage] remain in [SharedAllocationR]; neither the
+    enclosing allocation nor any payload fields are discarded. *)
+Require Import skylabs.auto.cpp.proof.
+Require Import skylabs.brick.libstdcpp.shared_ptr.specs.
+
+Set Default Goal Selector "!".
+Set Warnings "+sl-transparent-constants".
+Import linearity.
+
+Section with_cpp.
+  Context `{Sigma : cpp_logic, MOD : inc_shared_ptr_cpp.source ⊧ σ}.
+
+  (** A construction obligation, not an assumed payload-constructor spec.
+      The input is raw, sufficiently large and aligned storage, not a live T.
+      Placement new may give the object a different logical pointer; keep
+      [provides_storage] and its lifetime token rather than equating pointers.
+      The client fixes [pieces], but construction produces its descriptor [d]:
+      e.g. the addresses of buffers allocated by the constructor. The same [d]
+      determines every piece, its destruction proof, and constructor side
+      effects [after d]. This is the same ownership used by the raw-pointer
+      constructor [init_ctor], obtained here after rather than before the call.
+      Neither path permits choosing a new piece family when copying. *)
+  Definition make_shared_construction {D : Type} (ty : type) (args : list type)
+      (values : list val) (pieces : D -> nat -> Rep)
+      (before : mpred) (after : D -> mpred) : mpred :=
+    specify.template.func "std::construct_at"
+      [Atype ty; Apack (map Atype args)] (Tptr ty)
+      (Tptr ty :: map (trv_ref QM) args) $
+      \arg{storage : ptr} "__location" (Vptr storage)
+      \args values
+      \pre{size alignment}
+        [| size_of σ ty = Some size /\ align_of ty = Some alignment |]
+      \pre [| storage <> nullptr |]
+      \pre storage |-> blockR size 1$m ** storage |-> alignedR alignment
+      \pre before
+      \post{p : ptr} [Vptr p]
+        provides_storage storage p ty **
+        p |-> new_token.R 1%Qp (new_token.mk ty storage 0) **
+        Exists d : D,
+          p |-> ([∗ list] i ∈ allPieceIds, pieces d i) **
+          payload_destructible ty (pieces d) ** after d.
+
+  (* Keep both parts of the function name as direct parameters for spec
+     discovery. Neither inverse [map Atype] inference nor reduction of the
+     reference-collapsing function in FindSpec is available. The checked
+     equalities below enforce a type-only pack and correct forwarding refs. *)
+  Definition make_shared_spec (ty : type) (pack : list temp_arg)
+      (parameter_types : list type) : mpred :=
+    let args := map (fun a => match a with Atype t => t | _ => Tvoid end) pack in
+    (* libstdc++'s _Sp_counted_ptr_inplace uses __remove_cv_t<T>. The handle
+       remains shared_ptr<T>; its managed object and destructor use this type. *)
+    let managed := drop_qualifiers ty in
+    specify.template.func "std::make_shared"
+      [Atype ty; Apack pack]
+      (Tnamed ("std::shared_ptr".<< Atype ty >>))
+      parameter_types $
+      \args{values : list val} values
+      \pre [| pack = map Atype args |]
+      \pre [| parameter_types = map (trv_ref QM) args |]
+      \pre [| length values = length args |]
+      \pre [| shared_ptr_no_esftb ty = true |]
+      \pre [| match erase_qualifiers ty with
+               | Tarray _ _ | Tincomplete_array _ => False
+               | _ => True
+               end |]
+      \pre{{D} (pieces : D -> nat -> Rep) before after}
+        make_shared_construction managed args values pieces before after
+      \pre before
+      \post{retp : ptr} [Vptr retp]
+        Exists (d : D) (id : CtrlBlockId) (p : ptr),
+          [| payload_type id = managed |] **
+          [| payload_delete id = None |] **
+          retp |-> SharedPtrR ty 1$m id 0 (pieces d) p **
+          p |-> pieces d 0%nat **
+          ([∗ list] i ∈ allButFirstPieceId, pieceRight id i) ** after d.
+
+  Definition SpecFor_make_shared := RegisterSpec (@make_shared_spec).
+  #[global] Existing Instance SpecFor_make_shared.
+End with_cpp.
+
+#[global] Hint Opaque make_shared_construction make_shared_spec : sl_opacity.
diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/make_shared_test.v b/rocq-brick-libstdcpp/proof/shared_ptr/make_shared_test.v
new file mode 100644
index 00000000..cb641e79
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/shared_ptr/make_shared_test.v
@@ -0,0 +1,254 @@
+(** Client regressions for factory spec discovery, forwarding, const payloads,
+    and retention of constructor side effects. These assume make_shared's
+    library spec; they do not verify its reference-count implementation. *)
+Require Import skylabs.auto.cpp.proof.
+Require Import skylabs.lang.cpp.parser.plugin.cpp2v.
+Require Import skylabs.brick.libstdcpp.shared_ptr.specs.
+Require Import skylabs.brick.libstdcpp.shared_ptr.make_shared.
+
+Set Default Goal Selector "!".
+Set Warnings "+sl-transparent-constants".
+Import linearity.
+#[local] Hint Resolve UNSAFE_read_prim_cancel : sl_opacity.
+Remove Hints _at_pick_cfrac_and_split_C _at_pick_frac_and_split_C
+  _at_split_specific_cfrac_C _at_split_specific_frac_C
+  : db_skylabs_syntactic.
+
+#[elaborate]
+cpp.prog source flags "-std=c++23" prog cpp:{{
+#include <memory>
+struct Payload {
+    int value;
+    explicit Payload(int n) : value(n) {}
+};
+std::shared_ptr<Payload> make_payload(int& n) {
+    return std::make_shared<Payload>(n);
+}
+std::shared_ptr<Payload const> make_const_payload(int const& n) {
+    return std::make_shared<Payload const>(n);
+}
+std::shared_ptr<Payload> make_rvalue_payload(int&& n) {
+    return std::make_shared<Payload>(static_cast<int&&>(n));
+}
+std::shared_ptr<int const*> make_pointer_payload(int const*& p) {
+    return std::make_shared<int const*>(p);
+}
+Payload* construct_payload(Payload* p, int& n) {
+    return std::construct_at(p, n);
+}
+}}.
+
+Section with_cpp.
+  Context `{Sigma : cpp_logic, MOD : source ⊧ σ}.
+
+  #[local] Instance learn_shared : LearnEq6 SharedPtrR :=
+    ltac:(solve_learnable).
+
+  Lemma payload_no_esft : shared_ptr_no_esftb "Payload" = true.
+  Proof using MOD.
+    eapply shared_ptr_no_esft_no_bases.
+    { eapply (@glob_def_genv_compat_struct σ "Payload"%cpp_name source MOD).
+      vm_compute. reflexivity. }
+    { reflexivity. }
+    { intros pack. split; discriminate. }
+  Qed.
+
+  cpp.spec "make_payload(int&)" from source as make_payload_spec with (
+    \arg{argp : ptr} "n" (Vref argp)
+    \prepost argp |-> type_ptrR "int"
+    \pre{{D} (pieces : D -> nat -> Rep) before after}
+      make_shared_construction "Payload" ["int&"%cpp_type] [Vref argp]
+        pieces before after
+    \pre before
+    \post{retp : ptr} [Vptr retp]
+      Exists (d : D) (id : CtrlBlockId) (p : ptr),
+        [| payload_type id = "Payload"%cpp_type |] **
+        retp |-> SharedPtrR "Payload" 1$m id 0 (pieces d) p **
+        p |-> pieces d 0%nat **
+        ([∗ list] i ∈ allButFirstPieceId, pieceRight id i) ** after d
+  ).
+
+  Lemma make_payload_ok : verify[source] make_payload_spec.
+  Proof using MOD.
+    have Hnoesft := payload_no_esft.
+    verify_spec.
+    go.
+    iExists [Vref argp], D, pieces, before, after.
+    go.
+    match goal with d : D |- _ => iExists d end.
+    go.
+  Qed.
+
+  cpp.spec "make_const_payload(const int&)" from source as make_const_payload_spec with (
+    \arg{argp : ptr} "n" (Vref argp)
+    \prepost argp |-> type_ptrR "int"
+    \pre{{D} (pieces : D -> nat -> Rep) before after}
+      make_shared_construction "Payload" ["const int&"%cpp_type] [Vref argp]
+        pieces before after
+    \pre before
+    \post{retp : ptr} [Vptr retp]
+      Exists (d : D) (id : CtrlBlockId) (p : ptr),
+        [| payload_type id = "Payload"%cpp_type |] **
+        retp |-> SharedPtrR "const Payload" 1$m id 0 (pieces d) p **
+        p |-> pieces d 0%nat **
+        ([∗ list] i ∈ allButFirstPieceId, pieceRight id i) ** after d
+  ).
+
+  Lemma make_const_payload_ok : verify[source] make_const_payload_spec.
+  Proof using MOD.
+    have Hnoesft := payload_no_esft.
+    verify_spec.
+    go.
+    iExists [Vref argp], D, pieces, before, after.
+    go.
+    match goal with d : D |- _ => iExists d end.
+    go.
+  Qed.
+
+  cpp.spec "make_rvalue_payload(int&&)" from source as make_rvalue_payload_spec with (
+    \arg{argp : ptr} "n" (Vref argp)
+    \prepost argp |-> type_ptrR "int"
+    \pre{{D} (pieces : D -> nat -> Rep) before after}
+      make_shared_construction "Payload" ["int"%cpp_type] [Vref argp]
+        pieces before after
+    \pre before
+    \post{retp : ptr} [Vptr retp]
+      Exists (d : D) (id : CtrlBlockId) (p : ptr),
+        [| payload_type id = "Payload"%cpp_type |] **
+        retp |-> SharedPtrR "Payload" 1$m id 0 (pieces d) p **
+        p |-> pieces d 0%nat **
+        ([∗ list] i ∈ allButFirstPieceId, pieceRight id i) ** after d
+  ).
+
+  Lemma make_rvalue_payload_ok : verify[source] make_rvalue_payload_spec.
+  Proof using MOD.
+    have Hnoesft := payload_no_esft.
+    verify_spec.
+    go.
+    iExists [Vref argp], D, pieces, before, after.
+    go.
+    match goal with d : D |- _ => iExists d end.
+    go.
+  Qed.
+
+  (* remove_cv_t removes only top-level qualifiers: the managed pointer's
+     pointee must stay const, including in the construction obligation. *)
+  cpp.spec "make_pointer_payload(const int*&)" from source as make_pointer_payload_spec with (
+    \arg{argp : ptr} "p" (Vref argp)
+    \prepost argp |-> type_ptrR "const int*"
+    \pre{{D} (pieces : D -> nat -> Rep) before after}
+      make_shared_construction "const int*" ["const int*&"%cpp_type] [Vref argp]
+        pieces before after
+    \pre before
+    \post{retp : ptr} [Vptr retp]
+      Exists (d : D) (id : CtrlBlockId) (p : ptr),
+        [| payload_type id = "const int*"%cpp_type |] **
+        retp |-> SharedPtrR "const int*" 1$m id 0 (pieces d) p **
+        p |-> pieces d 0%nat **
+        ([∗ list] i ∈ allButFirstPieceId, pieceRight id i) ** after d
+  ).
+
+  Lemma make_pointer_payload_ok : verify[source] make_pointer_payload_spec.
+  Proof using MOD.
+    verify_spec.
+    go.
+    iExists [Vref argp], D, pieces, before, after.
+    go.
+    match goal with d : D |- _ => iExists d end.
+    go.
+  Qed.
+
+  Definition PayloadR (q : cQp.t) (n : Z) : Rep :=
+    structR "Payload" q ** _field "Payload::value" |-> intR q n.
+  #[local] Hint Opaque PayloadR : sl_opacity.
+
+  cpp.spec "Payload::Payload(int)" from source as payload_ctor_spec with (
+    fun (this : ptr) =>
+      \arg{n : Z} "n" (Vint n)
+      \post this |-> PayloadR 1$m n
+  ).
+
+  Lemma payload_ctor_ok : verify[source] payload_ctor_spec.
+  Proof using MOD.
+    verify_spec.
+    go.
+    rewrite /PayloadR.
+    go.
+  Qed.
+
+  cpp.spec "Payload::~Payload()" from source as payload_dtor_spec with (
+    fun (this : ptr) =>
+      \pre{n} this |-> PayloadR 1$m n
+      \post emp
+  ).
+
+  Lemma payload_dtor_ok : verify[source] payload_dtor_spec.
+  Proof using MOD.
+    verify_spec.
+    rewrite /PayloadR.
+    go.
+  Qed.
+
+  cpp.spec "operator new(unsigned long, void*)" from source
+      as placement_new_spec with (
+    \arg{size : N} "size" (Vn size)
+    \arg{p : ptr} "p" (Vptr p)
+    \post [Vptr p] emp
+  ).
+
+  Lemma placement_new_ok : verify[source] placement_new_spec.
+  Proof using MOD.
+    verify_spec.
+    go.
+  Qed.
+
+  (* The client supplies a partition of genuine field ownership, not a
+     constructor axiom for an arbitrary [Rpiece]. *)
+  #[local] cpp.spec "std::forward<int&>(int&)" inline.
+  Lemma construct_payload_ok {D : Type}
+      (q : cQp.t) (qflag : Qp) (argp : ptr) (n : Z)
+      (pieces : D -> nat -> Rep) (after : D -> mpred) :
+    verify[source]
+      (make_shared_construction "Payload" ["int&"%cpp_type] [Vref argp]
+        pieces
+        (argp |-> intR q n **
+         _global "std::is_array_v<Payload>" |-> boolR qflag$c false **
+         Forall p : ptr, p |-> PayloadR 1$m n -*
+           Exists d : D, p |-> ([∗ list] i ∈ allPieceIds, pieces d i) **
+             payload_destructible "Payload" (pieces d) ** after d)
+        (fun d => argp |-> intR q n **
+         _global "std::is_array_v<Payload>" |-> boolR qflag$c false ** after d)).
+  Proof using MOD.
+    verify_spec.
+    go.
+    change (size_of σ "Payload" = Some size) in a.
+    rewrite (@sizeof._size_of_ok source σ MOD "Payload" 4 eq_refl) in a.
+    injection a as Hsize. subst size.
+    rewrite (@alignment._align_of_ok source σ MOD "Payload" 4 eq_refl) in b.
+    injection b as Halign. subst alignment.
+    go.
+    rewrite (bi.forall_elim _x_4).
+    wapply (bi.wand_elim_l (_x_4 |-> PayloadR 1$m n)
+      (Exists d : D, _x_4 |-> ([∗ list] i ∈ allPieceIds, pieces d i) **
+        payload_destructible "Payload" (pieces d) ** after d)).
+    go.
+  Qed.
+
+  Lemma construct_payload_from_code {D : Type} (q : cQp.t) (qflag : Qp)
+      (argp : ptr) (n : Z) (pieces : D -> nat -> Rep) (after : D -> mpred) :
+    denoteModule source |--
+      make_shared_construction "Payload" ["int&"%cpp_type] [Vref argp]
+        pieces
+        (argp |-> intR q n **
+         _global "std::is_array_v<Payload>" |-> boolR qflag$c false **
+         Forall p : ptr, p |-> PayloadR 1$m n -*
+           Exists d : D, p |-> ([∗ list] i ∈ allPieceIds, pieces d i) **
+             payload_destructible "Payload" (pieces d) ** after d)
+        (fun d => argp |-> intR q n **
+         _global "std::is_array_v<Payload>" |-> boolR qflag$c false ** after d).
+  Proof using MOD.
+    wapply (construct_payload_ok q qflag argp n pieces after).
+    go using (spec_bwd payload_ctor_ok), (spec_bwd payload_dtor_ok),
+      (spec_bwd placement_new_ok).
+  Qed.
+End with_cpp.
diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/no_esft.v b/rocq-brick-libstdcpp/proof/shared_ptr/no_esft.v
new file mode 100644
index 00000000..1e131689
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/shared_ptr/no_esft.v
@@ -0,0 +1,259 @@
+(** Exclusion of the payload mutation performed by enable_shared_from_this.
+    The proposition requires complete inheritance information and excludes
+    both public and internal enable_shared_from_this bases. The boolean search
+    decides that proposition. Opaque, unsupported, and missing declarations
+    are rejected rather than treated as evidence that a class has no bases. *)
+Require Import skylabs.auto.cpp.proof.
+
+Set Default Goal Selector "!".
+
+Section hierarchy.
+  Context {sigma : genv}.
+
+  Definition esft_name_ok (cls : name) : bool :=
+    match cls with
+    | Ninst template _ =>
+        bool_decide (template <> "std::enable_shared_from_this"%cpp_name /\
+          template <> "std::__enable_shared_from_this"%cpp_name)
+    | _ => true
+    end.
+
+  Lemma esft_name_ok_spec cls :
+    esft_name_ok cls = true <->
+    forall pack,
+      cls <> Ninst "std::enable_shared_from_this" pack /\
+      cls <> Ninst "std::__enable_shared_from_this" pack.
+  Proof.
+    destruct cls; simpl; try (split; [intros _ pack; split; discriminate | done]).
+    rewrite bool_decide_eq_true.
+    split.
+    { intros [Hstd Hinternal] pack. split; congruence. }
+    { intro H. destruct (H l) as [Hstd Hinternal]. split; congruence. }
+  Qed.
+
+  Definition esft_children (cls : name) : list name :=
+    match glob_def sigma cls with
+    | Some (Gstruct layout) => map fst layout.(s_bases)
+    | _ => []
+    end.
+
+  Definition esft_node_ok (cls : name) : bool :=
+    match glob_def sigma cls with
+    | Some (Gstruct _ | Gunion _ | Genum _ _) => esft_name_ok cls
+    | _ => false
+    end.
+
+  Definition esft_class_safe (cls : name) : Prop :=
+    forall base, rtc (fun parent child => child ∈ esft_children parent) cls base ->
+      esft_node_ok base = true.
+
+  Definition shared_ptr_no_esft (ty : type) : Prop :=
+    match erase_qualifiers ty with
+    | Tnamed cls => esft_class_safe cls
+    | _ => True
+    end.
+
+  Lemma esft_safe_node cls : esft_class_safe cls -> esft_node_ok cls = true.
+  Proof.
+    intros Hsafe. apply Hsafe. constructor.
+  Qed.
+
+  Lemma esft_safe_children cls :
+    esft_class_safe cls -> List.Forall esft_class_safe (esft_children cls).
+  Proof.
+    intros Hsafe. apply Forall_forall. intros base Hbase node Hpath.
+    apply Hsafe. econstructor; eauto.
+  Qed.
+
+  Lemma esft_closed_safe (done : list name) :
+    List.Forall (fun cls => esft_node_ok cls = true) done ->
+    (forall cls, cls ∈ done -> forall base, base ∈ esft_children cls -> base ∈ done) ->
+    forall cls, cls ∈ done -> esft_class_safe cls.
+  Proof.
+    intros Hnodes Hclosed cls Hin base Hpath. revert Hin.
+    induction Hpath as [node | parent child node Hedge Hpath IH]; intros Hin.
+    { exact (proj1 (Forall_forall _ _) Hnodes node Hin). }
+    apply IH. eapply Hclosed; eauto.
+  Qed.
+
+  (** Each declared class contributes its outgoing base edges at most once.
+      The initial work item plus all those edges therefore bounds queue pops,
+      including duplicates and cycles. *)
+  Definition esft_edge_cost (seen : list name) (entry : name * GlobDecl) : nat :=
+    if bool_decide (entry.1 ∈ seen) then 0 else
+      match entry.2 with
+      | Gstruct layout => length layout.(s_bases)
+      | _ => 0
+      end.
+
+  Definition esft_remaining_edges (seen : list name) : nat :=
+    list_sum (map (esft_edge_cost seen) (map_to_list sigma.(genv_tu).(types))).
+
+  Lemma esft_edge_cost_mono seen cls entry :
+    esft_edge_cost (cls :: seen) entry <= esft_edge_cost seen entry.
+  Proof.
+    unfold esft_edge_cost. repeat case_bool_decide; try set_solver; lia.
+  Qed.
+
+  Lemma esft_edge_sum_mono seen cls entries :
+    list_sum (map (esft_edge_cost (cls :: seen)) entries) <=
+    list_sum (map (esft_edge_cost seen) entries).
+  Proof.
+    induction entries as [| entry entries IH]; simpl; first lia.
+    pose proof (esft_edge_cost_mono seen cls entry). lia.
+  Qed.
+
+  Lemma esft_edge_sum_take seen cls layout entries :
+    cls ∉ seen -> (cls, Gstruct layout) ∈ entries ->
+    length layout.(s_bases) +
+      list_sum (map (esft_edge_cost (cls :: seen)) entries) <=
+      list_sum (map (esft_edge_cost seen) entries).
+  Proof.
+    intros Hfresh. induction entries as [| entry entries IH]; intros Hin.
+    { inversion Hin. }
+    apply elem_of_cons in Hin as [<- | Hin]; simpl.
+    { pose proof (esft_edge_sum_mono seen cls entries).
+      assert (Hnew : esft_edge_cost (cls :: seen) (cls, Gstruct layout) = 0).
+      { unfold esft_edge_cost. simpl. rewrite bool_decide_true; [done | set_solver]. }
+      assert (Hold : esft_edge_cost seen (cls, Gstruct layout) = length layout.(s_bases)).
+      { unfold esft_edge_cost. simpl. rewrite bool_decide_false; done. }
+      rewrite Hnew Hold.
+      lia. }
+    { specialize (IH Hin). pose proof (esft_edge_cost_mono seen cls entry). lia. }
+  Qed.
+
+  Lemma esft_remaining_take seen cls :
+    cls ∉ seen ->
+    length (esft_children cls) + esft_remaining_edges (cls :: seen) <=
+      esft_remaining_edges seen.
+  Proof.
+    intros Hfresh. unfold esft_children, esft_remaining_edges.
+    destruct (glob_def sigma cls) as [decl |] eqn:Hdecl.
+    { destruct decl; try apply esft_edge_sum_mono.
+      rewrite length_fmap.
+      apply esft_edge_sum_take; first exact Hfresh.
+      destruct (NM.map_to_list_elements _ _ _ Hdecl) as [before [after Hentries]].
+      rewrite Hentries. apply elem_of_app. right. by left. }
+    { apply esft_edge_sum_mono. }
+  Qed.
+
+  Fixpoint esft_walk (fuel : nat) (seen todo : list name) : bool :=
+    match todo with
+    | [] => true
+    | cls :: todo =>
+        match fuel with
+        | O => false
+        | S fuel =>
+            if bool_decide (cls ∈ seen) then esft_walk fuel seen todo
+            else esft_node_ok cls &&
+              esft_walk fuel (cls :: seen) (esft_children cls ++ todo)
+        end
+    end.
+
+  Lemma esft_walk_complete fuel seen todo :
+    length todo + esft_remaining_edges seen <= fuel ->
+    List.Forall esft_class_safe todo -> esft_walk fuel seen todo = true.
+  Proof.
+    revert seen todo. induction fuel as [| fuel IH]; intros seen todo Hfuel Hsafe;
+      destruct todo as [| cls todo]; first done.
+    { simpl in Hfuel. lia. }
+    { done. }
+    simpl. case_bool_decide as Hseen.
+    { apply IH; first (simpl in Hfuel; lia).
+      inversion Hsafe. assumption. }
+    apply andb_true_iff. inversion Hsafe as [| ? ? Hhead Htail]; subst.
+    split.
+    { exact (esft_safe_node cls Hhead). }
+    apply IH.
+    { pose proof (esft_remaining_take seen cls Hseen).
+      rewrite length_app. simpl in Hfuel. lia. }
+    apply Forall_app. split; last exact Htail.
+    exact (esft_safe_children cls Hhead).
+  Qed.
+
+  Lemma esft_walk_sound fuel seen todo :
+    List.Forall (fun cls => esft_node_ok cls = true) seen ->
+    (forall cls, cls ∈ seen -> forall base,
+      base ∈ esft_children cls -> base ∈ seen ++ todo) ->
+    esft_walk fuel seen todo = true ->
+    exists visited : list name,
+      (forall cls, cls ∈ seen ++ todo -> cls ∈ visited) /\
+      List.Forall (fun cls => esft_node_ok cls = true) visited /\
+      (forall cls, cls ∈ visited -> forall base,
+        base ∈ esft_children cls -> base ∈ visited).
+  Proof.
+    revert seen todo. induction fuel as [| fuel IH]; intros seen todo Hsafe Hclosed Hrun;
+      destruct todo as [| cls todo].
+    { exists seen. rewrite app_nil_r in Hclosed. rewrite app_nil_r.
+      split; first done. split; assumption. }
+    { discriminate Hrun. }
+    { exists seen. rewrite app_nil_r in Hclosed. rewrite app_nil_r.
+      split; first done. split; assumption. }
+    simpl in Hrun. case_bool_decide as Hseen.
+    { destruct (IH seen todo Hsafe) as [visited [Hcontains [Hnodes Hedges]]].
+      { intros node Hin base Hbase. specialize (Hclosed node Hin base Hbase). set_solver. }
+      { exact Hrun. }
+      exists visited. split; last (split; assumption).
+      intros node Hin. apply Hcontains. set_solver. }
+    apply andb_true_iff in Hrun as [Hnode Hrun].
+    destruct (IH (cls :: seen) (esft_children cls ++ todo)) as
+      [visited [Hcontains [Hnodes Hedges]]].
+    { constructor; assumption. }
+    { intros node Hin base Hbase. apply elem_of_cons in Hin as [-> | Hin].
+      { set_solver. }
+      specialize (Hclosed node Hin base Hbase). set_solver. }
+    { exact Hrun. }
+    exists visited. split; last (split; assumption).
+    intros node Hin. apply Hcontains. set_solver.
+  Qed.
+
+  Definition shared_ptr_no_esftb (ty : type) : bool :=
+    match erase_qualifiers ty with
+    | Tnamed cls =>
+        match esft_children cls with
+        | [] => esft_node_ok cls
+        | _ => esft_walk (S (esft_remaining_edges [])) [] [cls]
+        end
+    | _ => true
+    end.
+
+  Lemma shared_ptr_no_esftb_correct ty :
+    shared_ptr_no_esftb ty = true <-> shared_ptr_no_esft ty.
+  Proof.
+    unfold shared_ptr_no_esftb, shared_ptr_no_esft.
+    destruct (erase_qualifiers ty) as [] eqn:Hty; try tauto.
+    match type of Hty with _ = Tnamed ?name => rename name into cls end.
+    destruct (esft_children cls) as [| base bases] eqn:Hchildren.
+    { split; last apply esft_safe_node.
+      intros Hnode. apply (esft_closed_safe [cls]).
+      { constructor; first exact Hnode. constructor. }
+      { intros node Hcls child Hchild.
+        apply list_elem_of_singleton in Hcls. subst node.
+        rewrite Hchildren in Hchild. inversion Hchild. }
+      { by left. } }
+    split.
+    { intros Hrun.
+      destruct (esft_walk_sound (S (esft_remaining_edges [])) [] [cls]) as
+        [visited [Hcontains [Hnodes Hclosed]]].
+      { constructor. }
+      { intros node Hcls. inversion Hcls. }
+      { exact Hrun. }
+      apply (esft_closed_safe visited Hnodes Hclosed).
+      apply Hcontains. by left. }
+    { intros Hsafe. apply esft_walk_complete.
+      { simpl. lia. }
+      { constructor; first exact Hsafe. constructor. } }
+  Qed.
+  Lemma shared_ptr_no_esft_no_bases cls layout :
+    glob_def sigma cls = Some (Gstruct layout) -> layout.(s_bases) = [] ->
+    (forall pack,
+      cls <> Ninst "std::enable_shared_from_this" pack /\
+      cls <> Ninst "std::__enable_shared_from_this" pack) ->
+    shared_ptr_no_esftb (Tnamed cls) = true.
+  Proof.
+    intros Hlayout Hbases Hname.
+    unfold shared_ptr_no_esftb, esft_children, esft_node_ok.
+    cbn [erase_qualifiers]. rewrite Hlayout Hbases. simpl.
+    apply esft_name_ok_spec. exact Hname.
+  Qed.
+End hierarchy.
diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/redistribution.v b/rocq-brick-libstdcpp/proof/shared_ptr/redistribution.v
new file mode 100644
index 00000000..aa143b69
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/shared_ptr/redistribution.v
@@ -0,0 +1,367 @@
+(** Exclusive migration of a payload partition. This changes ghost protocol
+    identities, never the C++ handles, allocation, or reference count. *)
+Require Import skylabs.auto.cpp.proof.
+Require Import skylabs.brick.libstdcpp.shared_ptr.specs.
+Require Import skylabs.brick.libstdcpp.shared_ptr.handle_liveness.
+Require Import skylabs.brick.libstdcpp.shared_ptr.token_pool.
+Require Import iris.algebra.excl iris.algebra.frac.
+
+Set Default Goal Selector "!".
+Import linearity.
+
+Section redistribution.
+  Context `{Sigma : cpp_logic} {CU : genv}.
+  #[local] Existing Instance br.ghost.excl_inG.
+  #[local] Existing Instance br.ghost.frac_inG.
+
+  #[local] Lemma indexed_ownership {A} (xs : list A) (P : A -> mpred) fallback :
+    ([∗ list] x ∈ xs, P x) -|-
+    ([∗ list] i ∈ seq 0 (length xs),
+      match nth_error xs i with Some x => P x | None => fallback end).
+  Proof.
+    induction xs as [| x xs IH]; first reflexivity.
+    cbn [length seq]. rewrite !big_sepL_cons.
+    rewrite <- fmap_S_seq, big_sepL_fmap.
+    cbn [nth_error]. rewrite <- IH. reflexivity.
+  Qed.
+
+  #[local] Lemma conditional_sep_lists (out : nat -> bool)
+      (P Q : nat -> mpred) indices :
+    ([∗ list] i ∈ indices, P i) ** ([∗ list] i ∈ indices, Q i) -|-
+    ([∗ list] i ∈ indices,
+      (if out i then Q i else P i) ** (if out i then P i else Q i)).
+  Proof.
+    rewrite <- big_sepL_sep. apply big_sepL_proper.
+    intros k i Hi. destruct (out i); first apply bi.sep_comm. reflexivity.
+  Qed.
+
+  #[local] Lemma alloc_rights n :
+    (emp : mpred) |-- (|==> Exists names : list gname,
+      [| length names = n |] **
+      ([∗ list] name ∈ names, own (A := exclR unitO) name (Excl ())))%I.
+  Proof.
+    induction n as [| n IH].
+    { rewrite <- bupd_intro. go. iExists []. go. }
+    rewrite <- bi.emp_sep at 1.
+    etrans; first (apply bi.sep_mono;
+      [exact IH | exact (own_alloc (PROP := mpredI) (A := exclR unitO) (Excl ()) ltac:(done))]).
+    rewrite bupd_sep. apply bupd_mono. go.
+    match goal with names : list gname |- _ => iExists (t :: names) end. go.
+  Qed.
+
+  #[local] Lemma alloc_handles n :
+    (emp : mpred) |-- (|==> Exists names : list gname,
+      [| length names = n |] **
+      ([∗ list] name ∈ names, own (A := fracR) name 1%Qp))%I.
+  Proof.
+    induction n as [| n IH].
+    { rewrite <- bupd_intro. go. iExists []. go. }
+    rewrite <- bi.emp_sep at 1.
+    etrans; first (apply bi.sep_mono;
+      [exact IH | exact (own_alloc (PROP := mpredI) (A := fracR) 1%Qp ltac:(done))]).
+    rewrite bupd_sep. apply bupd_mono. go.
+    match goal with names : list gname |- _ => iExists (t :: names) end. go.
+  Qed.
+  Definition protocol_tokens id (out : nat -> bool) : mpred :=
+    [∗ list] i ∈ allPieceIds,
+      if out i then pieceHandle id 1 i else pieceRight id i.
+
+  Definition invariant_tokens id (out : nat -> bool) : mpred :=
+    [∗ list] i ∈ allPieceIds,
+      if out i then pieceRight id i else pieceHandle id 1 i.
+
+  Definition payload_pieces (R : nat -> Rep) (p : ptr) (out : nat -> bool) : mpred :=
+    [∗ list] i ∈ allPieceIds, if out i then p |-> R i else emp.
+
+  Definition handle_cells ty id (p : ptr) (handles : nat -> ptr)
+      (out : nat -> bool) : mpred :=
+    [∗ list] i ∈ allPieceIds,
+      if out i then handles i |-> SharedPtrHandleR ty 1$m p (dataLoc id) else emp.
+
+  #[local] Hint Opaque protocol_tokens invariant_tokens payload_pieces
+    handle_cells pieceHandle pieceRight sptrInv payload_destructible
+    payload_releasable payload_allocation
+    SharedPtrHandleR : sl_opacity.
+
+  #[local] Lemma alloc_protocol control managed cleanup (out : nat -> bool) :
+    (emp : mpred) |-- (|==> Exists id : CtrlBlockId,
+      [| dataLoc id = control /\ payload_type id = managed /\
+         lengthN (pieceRightLocs id) = N.pos maxContention /\
+         lengthN (pieceHandleLocs id) = N.pos maxContention /\
+         payload_delete id = cleanup |] **
+      protocol_tokens id out ** invariant_tokens id out)%I.
+  Proof.
+    rewrite <- bi.emp_sep at 1.
+    etrans; first (apply bi.sep_mono;
+      [exact (alloc_rights (Pos.to_nat maxContention)) |
+       exact (alloc_handles (Pos.to_nat maxContention))]).
+    rewrite bupd_sep. apply bupd_mono. go.
+    match goal with rights : list gname, handles : list gname |- _ =>
+      iExists {| pieceRightLocs := rights; pieceHandleLocs := handles;
+        dataLoc := control; payload_type := managed; payload_delete := cleanup |}
+    end.
+    unfold protocol_tokens, invariant_tokens, pieceRight, pieceHandle.
+    cbn [pieceRightLocs pieceHandleLocs dataLoc payload_type payload_delete].
+    rewrite <- big_sepL_sep.
+    setoid_rewrite (indexed_ownership _ (fun name => own (A := exclR unitO) name (Excl ())) emp).
+    setoid_rewrite (indexed_ownership _ (fun name => own (A := fracR) name 1%Qp) False%I).
+    unfold lengthN, allPieceIds.
+    rewrite <- conditional_sep_lists.
+    repeat match goal with
+    | Hlen : length ?xs = _ |- context[length ?xs] => rewrite Hlen
+    end.
+    go.
+  Qed.
+
+  #[local] Lemma token_pair_agrees id i (out inside : bool) :
+    (i < length (pieceRightLocs id))%nat ->
+    (if out then pieceHandle id 1 i else pieceRight id i) **
+    (if inside then pieceRight id i else pieceHandle id 1 i)
+    |-- [| inside = out |] ** pieceHandle id 1 i.
+  Proof.
+    intros Hi.
+    (* Retired copy rights contain only ghost ownership, not object storage. *)
+    assert (HA : Affine (pieceRight id i)).
+    { apply monPred_bi_affine, uPred_affine. }
+    destruct out, inside.
+    { etrans; first (apply bi.sep_elim_l; typeclasses eauto). go. }
+    { rewrite pieceHandle_full_conflict. go. }
+    { rewrite (TokenPool.pieceRight_exclusive id i Hi). go. }
+    { etrans; first (apply bi.sep_elim_r; typeclasses eauto). go. }
+  Qed.
+
+  #[local] Lemma tokens_agree id out inside :
+    lengthN (pieceRightLocs id) = N.pos maxContention ->
+    protocol_tokens id out ** invariant_tokens id inside |--
+      [| forall i, i ∈ allPieceIds -> inside i = out i |] **
+      invariant_tokens id (fun _ => false).
+  Proof.
+    intros Hlength. unfold protocol_tokens, invariant_tokens.
+    rewrite <- big_sepL_sep.
+    etrans.
+    { apply big_op.big_sepL_mono_elem. intros i Hi. apply token_pair_agrees.
+      unfold allPieceIds in Hi. apply elem_of_seq in Hi.
+      unfold lengthN in Hlength. lia. }
+    rewrite big_sepL_sep lemmas.big_sepL_only_provable Forall_forall. go.
+  Qed.
+
+  #[local] Lemma payload_pieces_partition R p out :
+    payload_pieces R p out ** payload_pieces R p (fun i => negb (out i))
+      -|- p |-> ([∗ list] i ∈ allPieceIds, R i).
+  Proof.
+    unfold payload_pieces. rewrite <- big_sepL_sep. rewrite _at_big_sepL.
+    apply big_sepL_proper. intros k i Hi.
+    destruct (out i); simpl; rewrite ?bi.sep_emp ?bi.emp_sep; reflexivity.
+  Qed.
+  (** Handle addresses are arguments, not hidden existential witnesses. *)
+  Definition allPiecesAndObjs ty R id (p : ptr) (handles : nat -> ptr)
+      (out : nat -> bool) : mpred :=
+    [∗ list] i ∈ allPieceIds,
+      if out i then p |-> R i ** handles i |-> SharedPtrR ty 1$m id i R p
+      else pieceRight id i.
+
+  Definition protocol_knowledge ty id R (p : ptr) : mpred :=
+    [| delete_compat ty (payload_type id) /\ p <> nullptr /\
+       lengthN (pieceRightLocs id) = N.pos maxContention /\
+       lengthN (pieceHandleLocs id) = N.pos maxContention |] **
+    payload_releasable id R **
+    inv nroot (Exists out, sptrInv id R p out).
+
+  #[local] Instance protocol_knowledge_persistent ty id R p :
+    Persistent (protocol_knowledge ty id R p) := _.
+  #[local] Hint Opaque allPiecesAndObjs protocol_knowledge : sl_opacity.
+  #[local] Opaque payload_releasable payload_allocation.
+
+  #[local] Lemma census_knowledge ty R id p handles out live :
+    live ∈ allPieceIds -> out live = true ->
+    allPiecesAndObjs ty R id p handles out |--
+      protocol_knowledge ty id R p ** allPiecesAndObjs ty R id p handles out.
+  Proof.
+    intros Hi Hlive. unfold allPiecesAndObjs.
+    rewrite (big_op.big_sepL_difference_singleton live) //.
+    2: { unfold allPieceIds. apply NoDup_seq. }
+    rewrite Hlive. unfold SharedPtrR, protocol_knowledge. go.
+  Qed.
+
+  #[local] Lemma census_split ty R id p handles out :
+    allPiecesAndObjs ty R id p handles out |--
+      handle_cells ty id p handles out ** protocol_tokens id out ** payload_pieces R p out.
+  Proof.
+    unfold allPiecesAndObjs, handle_cells, protocol_tokens, payload_pieces.
+    rewrite <- !big_sepL_sep.
+    apply big_sepL_mono. intros k i Hi.
+    destruct (out i); last go. unfold SharedPtrR. go.
+  Qed.
+
+  #[local] Lemma census_close ty R id p handles out :
+    protocol_knowledge ty id R p ** handle_cells ty id p handles out **
+    protocol_tokens id out ** payload_pieces R p out |--
+      allPiecesAndObjs ty R id p handles out.
+  Proof.
+    unfold allPiecesAndObjs, handle_cells, protocol_tokens, payload_pieces.
+    rewrite -!bi.sep_assoc -!big_sepL_sep.
+    rewrite -(bi.wand_elim_l' _ _ _ (bi.wand_entails _ _
+      (big_sepL_impl (fun _ i =>
+        (if out i then handles i |-> SharedPtrHandleR ty 1$m p (dataLoc id) else emp) **
+        (if out i then pieceHandle id 1 i else pieceRight id i) **
+        (if out i then p |-> R i else emp))%I
+        (fun _ i => if out i then p |-> R i **
+          handles i |-> SharedPtrR ty 1$m id i R p else pieceRight id i)%I
+        allPieceIds))).
+    setoid_rewrite bi.pure_impl_forall.
+    unfold protocol_knowledge. go.
+    match goal with Hfound : allPieceIds !! _ = Some ?i |- _ =>
+      rename i into index; rename Hfound into Hlookup
+    end.
+    assert (Hbound : (N.of_nat index < N.pos maxContention)%N).
+    { apply list_elem_of_lookup_2 in Hlookup.
+      unfold allPieceIds in Hlookup. apply elem_of_seq in Hlookup. lia. }
+    destruct (out index).
+    { unfold SharedPtrR. go. }
+    { go. }
+  Qed.
+  Definition counter_allocation id p count : mpred :=
+    dataLoc id ., (SP_counted_base .:: Nid "_M_use_count") |-> intR 1$m (Z.of_N count) **
+    control_block_rest id p **
+    payload_allocation id p.
+  #[local] Hint Opaque counter_allocation : sl_opacity.
+  #[local] Transparent payload_releasable payload_allocation.
+
+  #[local] Lemma countLN_agree (left right : nat -> bool) :
+    (forall i, i ∈ allPieceIds -> left i = right i) ->
+    countLN left allPieceIds = countLN right allPieceIds.
+  Proof.
+    unfold countLN. generalize allPieceIds as indices.
+    intros indices. induction indices as [| i indices IH]; intros Hsame; first reflexivity.
+    assert (Hhead : left i = right i) by (apply Hsame; by left).
+    assert (Htail : forall j, j ∈ indices -> left j = right j)
+      by (intros j Hj; apply Hsame; by right).
+    rewrite !filter_cons Hhead.
+    destruct (decide (right i)); simpl; rewrite ?lengthN_cons (IH Htail); reflexivity.
+  Qed.
+
+  #[local] Lemma reclaim_protocol id R p out inside :
+    lengthN (pieceRightLocs id) = N.pos maxContention ->
+    (0 < countLN out allPieceIds)%N ->
+    protocol_tokens id out ** sptrInv id R p inside |--
+      invariant_tokens id (fun _ => false) **
+      counter_allocation id p (countLN out allPieceIds) **
+      payload_pieces R p (fun i => negb (out i)).
+  Proof.
+    intros Hlength Hlive. unfold sptrInv. fold (invariant_tokens id inside).
+    wapply (tokens_agree id out inside Hlength). go.
+    match goal with H : forall i, i ∈ allPieceIds -> inside i = out i |- _ =>
+      pose proof (countLN_agree inside out H) as Hcount;
+      assert (Hpieces :
+        ([∗ list] i ∈ allPieceIds, if inside i then emp else p |-> R i) -|-
+        payload_pieces R p (fun i => negb (out i)))
+        by (unfold payload_pieces; apply big_sepL_proper; intros k i Hi;
+            apply list_elem_of_lookup_2 in Hi; rewrite (H i Hi);
+            destruct (out i); reflexivity)
+    end.
+    rewrite Hcount bool_decide_false; last lia.
+    rewrite Hpieces. unfold counter_allocation. go.
+  Qed.
+
+  #[local] Lemma retired_protocol id R p :
+    invariant_tokens id (fun _ => false) |-- Exists out, sptrInv id R p out.
+  Proof.
+    go. iExists (fun _ => false).
+    rewrite sptrInv_retired.
+    { unfold invariant_tokens. go. }
+    { unfold countLN. generalize allPieceIds as indices.
+      intros indices. induction indices as [| i indices IH]; first reflexivity.
+      rewrite filter_cons. simpl. exact IH. }
+  Qed.
+
+  #[local] Lemma active_protocol id R p out :
+    (0 < countLN out allPieceIds)%N ->
+    invariant_tokens id out ** counter_allocation id p (countLN out allPieceIds) **
+    payload_pieces R p (fun i => negb (out i)) |-- Exists actual, sptrInv id R p actual.
+  Proof.
+    intros Hlive. go. iExists out.
+    unfold sptrInv. rewrite bool_decide_false; last lia.
+    unfold invariant_tokens, counter_allocation, payload_pieces.
+    assert (Hpiece : forall i,
+      (if negb (out i) then p |-> R i else emp) -|-
+      (if out i then emp else p |-> R i)).
+    { intros i. destruct (out i); reflexivity. }
+    setoid_rewrite Hpiece. go.
+  Qed.
+
+  (** Repartitioning requires every live handle and every unused acquisition
+      right. The whole payload, not each individual piece, must be equivalent.
+      Old persistent invariant assertions are not rewritten: the old protocol
+      is retired and the result uses newly allocated ghost names.
+
+      Timelessness permits opening the old invariant without executing C++.
+      Weak objectivity permits allocating the new invariant. The regression
+      instantiates an equality-ordered SC index, where weak objectivity holds
+      for every assertion. For other thread-view orders, the allocation-token
+      interface does not currently discharge this premise automatically. *)
+  Lemma redistributePayloadOwnership ty (Rold Rnew : nat -> Rep)
+      id p handles out live
+      (Htimeless : Timeless (Exists actual, sptrInv id Rold p actual))
+      (Hobjective : forall fresh,
+        WeaklyObjective (Exists actual, sptrInv fresh Rnew p actual)) :
+    live ∈ allPieceIds -> out live = true ->
+    (forall payload : ptr,
+      payload |-> ([∗ list] i ∈ allPieceIds, Rold i) -|-
+      payload |-> ([∗ list] i ∈ allPieceIds, Rnew i)) ->
+    allPiecesAndObjs ty Rold id p handles out |--
+      |={⊤}=> Exists fresh : CtrlBlockId,
+        [| dataLoc fresh = dataLoc id /\ payload_type fresh = payload_type id |] **
+        allPiecesAndObjs ty Rnew fresh p handles out.
+  Proof.
+    intros Hi Hout Hwhole.
+    assert (Hlive : (0 < countLN out allPieceIds)%N).
+    { eapply countLN_positive_of_member; eauto. }
+    assert (Hdestruct : payload_releasable id Rold |--
+      payload_releasable id Rnew).
+    { unfold payload_releasable.
+      destruct (payload_delete id) as [[op alignment]|];
+        unfold payload_deletable, payload_destructible;
+        setoid_rewrite <- Hwhole; reflexivity. }
+    assert (Hrepartition : payload_pieces Rold p out **
+      payload_pieces Rold p (fun i => negb (out i)) |--
+      payload_pieces Rnew p out ** payload_pieces Rnew p (fun i => negb (out i))).
+    { rewrite !payload_pieces_partition Hwhole. reflexivity. }
+    wapply (census_knowledge ty Rold id p handles out live Hi Hout). go.
+    wapply (census_split ty Rold id p handles out). go.
+    unfold protocol_knowledge. go.
+    wapply (inv_acc_timeless ⊤ nroot
+      (Exists actual, sptrInv id Rold p actual) ltac:(set_solver)). go.
+    match goal with actual : nat -> bool |- _ =>
+      wapply (reclaim_protocol id Rold p out actual ltac:(assumption) Hlive)
+    end.
+    go.
+    wapply (retired_protocol id Rold p). go.
+    wapply (bi.wand_elim_l (Exists actual, sptrInv id Rold p actual)
+      (|={⊤ ∖ ↑nroot,⊤}=> emp)%I). go.
+    iExists t. go.
+    wapply Hrepartition. go.
+    wapply (alloc_protocol (dataLoc id) (payload_type id) (payload_delete id) out). go.
+    rename t into freshid.
+    assert (Hcells : handle_cells ty id p handles out -|-
+      handle_cells ty freshid p handles out).
+    { unfold handle_cells. rewrite a2. reflexivity. }
+    assert (Hcounter : counter_allocation id p (countLN out allPieceIds) -|-
+      counter_allocation freshid p (countLN out allPieceIds)).
+    { unfold counter_allocation, control_block_rest, payload_allocation.
+      rewrite a2 a3 b0. reflexivity. }
+    assert (Hcleanup : payload_releasable freshid Rnew -|- payload_releasable id Rnew).
+    { unfold payload_releasable. rewrite a3 b0. reflexivity. }
+    rewrite Hcells Hcounter.
+    wapply (active_protocol freshid Rnew p out Hlive). go.
+    wapply (inv_alloc nroot ⊤ (Exists actual, sptrInv freshid Rnew p actual)).
+    rewrite <- fupd_intro. go.
+    rewrite <- (bi.later_intro (Exists actual, sptrInv freshid Rnew p actual)).
+    rewrite bi.sep_exist_r. iExists t. go.
+    iExists freshid. go.
+    wapply (census_close ty Rnew freshid p handles out). go.
+    unfold protocol_knowledge. rewrite a3 Hcleanup.
+    wapply Hdestruct. go.
+  Qed.
+End redistribution.
+
+#[global] Hint Opaque allPiecesAndObjs : sl_opacity.
diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/redistribution_test.v b/rocq-brick-libstdcpp/proof/shared_ptr/redistribution_test.v
new file mode 100644
index 00000000..c46ccb6d
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/shared_ptr/redistribution_test.v
@@ -0,0 +1,86 @@
+(** A genuinely different partition, not pointwise-equivalent pieces. *)
+Require Import skylabs.auto.cpp.proof.
+Require Import skylabs.brick.libstdcpp.shared_ptr.specs.
+Require Import skylabs.brick.libstdcpp.shared_ptr.handle_liveness.
+Require Import skylabs.brick.libstdcpp.shared_ptr.redistribution.
+
+Set Default Goal Selector "!".
+Import linearity.
+
+Section tests.
+  Context `{Sigma : cpp_logic} {CU : genv}.
+
+  Definition exchange_first_two (R : nat -> Rep) (i : nat) : Rep :=
+    if decide (i = 0%nat) then R 1%nat else
+    if decide (i = 1%nat) then R 0%nat else R i.
+
+  Lemma exchange_first_two_whole R (p : ptr) :
+    p |-> ([∗ list] i ∈ allPieceIds, R i) -|-
+    p |-> ([∗ list] i ∈ allPieceIds, exchange_first_two R i).
+  Proof.
+    pose proof maxContentionLb as Hcap.
+    assert (H0 : 0%nat ∈ allPieceIds) by (apply allPieceIds_member; lia).
+    assert (H1 : 1%nat ∈ allPieceIds) by (apply allPieceIds_member; lia).
+    assert (Hnd : NoDup allPieceIds) by (unfold allPieceIds; apply NoDup_seq).
+    rewrite !_at_big_sepL.
+    rewrite (big_op.big_sepL_difference_two (fun i => p |-> R i)
+      allPieceIds 0%nat 1%nat ltac:(lia) H0 H1 Hnd).
+    rewrite (big_op.big_sepL_difference_two (fun i => p |-> exchange_first_two R i)
+      allPieceIds 0%nat 1%nat ltac:(lia) H0 H1 Hnd).
+    assert (Hrest :
+      ([∗ list] i ∈ list_difference allPieceIds [0%nat;1%nat], p |-> exchange_first_two R i)
+      -|- ([∗ list] i ∈ list_difference allPieceIds [0%nat;1%nat], p |-> R i)).
+    { apply big_sepL_proper. intros k i Hi.
+      apply list_elem_of_lookup_2 in Hi. apply list_elem_of_difference in Hi.
+      unfold exchange_first_two. rewrite !decide_False; set_solver. }
+    rewrite Hrest. cbn [exchange_first_two].
+    iSplit; unfold exchange_first_two; go.
+  Qed.
+
+  (** Ordinary scalar pieces satisfy the timelessness condition. *)
+  Example int_partition_timeless id p q n :
+    Timeless (Exists out, sptrInv id (fun _ => intR q n) p out).
+  Proof.
+    unfold sptrInv, pieceRight, pieceHandle, payload_allocation.
+    destruct (payload_delete id) as [[op alignment]|];
+      unfold SharedAllocationR; apply _.
+  Qed.
+
+End tests.
+
+(** Use a concrete, equality-ordered index, with no growing thread view.
+    Weak objectivity then follows for every assertion, including the library's
+    abstract allocation tokens. For a non-discrete index the general theorem
+    deliberately retains its explicit WeaklyObjective premise; the allocation
+    interface does not currently provide that law. *)
+Definition sc_index : biIndex := BiIndex unit _ eq _.
+
+Section sc_test.
+  Context {G : gFunctors} {Sigma : cpp_logic sc_index G} {CU : genv}.
+  #[local] Existing Instance Sigma.
+
+  #[local] Instance sc_index_symmetric : Symmetric (@sqsubseteq sc_index _).
+  Proof. intros [] []. done. Qed.
+
+  Definition one_int_piece (n : Z) (i : nat) : @Rep sc_index G Sigma :=
+    if decide (i = 0%nat) then intR 1$m n else emp.
+
+  Example move_int_piece id p handles out live n :
+    live ∈ allPieceIds -> out live = true ->
+    allPiecesAndObjs Tint (one_int_piece n) id p handles out |--
+    |={⊤}=> Exists fresh : CtrlBlockId,
+      [| dataLoc fresh = dataLoc id /\ payload_type fresh = payload_type id |] **
+      allPiecesAndObjs Tint (exchange_first_two (one_int_piece n))
+        fresh p handles out.
+  Proof.
+    intros Hlive Hout.
+    eapply redistributePayloadOwnership with (live := live).
+    { unfold sptrInv, pieceRight, pieceHandle, payload_allocation, one_int_piece.
+      destruct (payload_delete id) as [[op alignment]|];
+        unfold SharedAllocationR; apply _. }
+    { intros. apply _. }
+    { exact Hlive. }
+    { exact Hout. }
+    { apply exchange_first_two_whole. }
+  Qed.
+End sc_test.
diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v
new file mode 100644
index 00000000..82dc6341
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v
@@ -0,0 +1,572 @@
+(** Specs of shared_ptr.
+We do not cover interaction with weak_ptr or enable_shared_from_this.
+Custom deleters, custom allocators, aliasing constructors, and
+make_shared_for_overwrite are not supported by these specs.
+The representation supports separate allocations and make_shared's combined
+allocations, including arrays. See [SharedAllocationR]. The non-array factory
+spec is in shared_ptr/make_shared.v; neither file proves the library bodies.
+We cover the following usage:
+- after dynamically allocating a new object (using new or new[]), it is (typicall immediately) passed to the init constructor of shared_ptr (spec in [init_ctor] below). At this time, the caller's proof needs to come up with [Rpiece: nat->Rep], defining how the ownership of this newly allocated object will be split between various shared_ptr objects that refer to it. They pass in all pieces and get back the 0th piece: [Rpiece 0] and tokens [pieceRight ctrlid 1 ... pieceRight ctrlid (maxContention-1)] which the clients can use to later obtain ownership of those [Rpiece]s by calling the copy constructor. The last argument of [pieceRight] is the piece id. The first argument, [ctrlid], identifies a single protection unit (payload object pointer) that is reference counted. "ctrl" comes from the implementation using a dynamically allocated "control block" which has an atomic counter to track how many times the copy constructor has been called minus the number of such objects that have already been destructed.
+[maxContention] bounds the number of simultaneously live handles to one control
+block. For the supported libstdc++ ABI it is [INT_MAX], not the pointer-sized
+unsigned maximum; see the definition below.
+
+Raw-pointer adoption requires [payload_deletable]: every payload piece,
+together with the retained allocation token, must suffice for the whole
+selected delete/delete[] operation. A trivial destructor is not enough:
+class-specific operator delete may access external resources. Such resources
+must be included in the pieces, rather than framed away. This applies even to
+objects allocated by ::new and is distinct from a caller-supplied custom deleter.
+[shared_ptr_delete_operator] checks the exported default-deleter body to find
+the actual selected operation; it does not guess global operator delete.
+
+The make_shared factory instead requires [payload_destructible]. Its interior
+payload must be destroyed but must NOT be passed to delete. [payload_delete]
+records the choice and allocation alignment in the control-block identity;
+[payload_releasable] retains the corresponding persistent capability through
+copies, assignment, and repartitioning. Neither capability is assumed as an
+unconditional property of arbitrary payload predicates.
+
+The pieces may not always be fractional ownerships of an object (e.g. int). For example, when the shared_ptr protects an array, it is common to have every piece own an index of the array, so that different shared_ptr objects can be used to write to different indices concurrently, e.g. here: https://github.com/category-labs/monad/blob/90f8b796061aeaf78a2943c45eae5303f6ff7900/category/execution/ethereum/execute_block.cpp#L233
+
+- To gain confidence in the provability of these specs, we sketch a definition of [SharedPtrR]. The [inv] definition is the most tricky part of it: it stores all the [Rpiece] and [pieceRight] ownerships that need to be dished out later or to be used for deletion when the reference count goes to 0.
+The proposed ownership-transfer argument uses sequentially consistent (SC)
+invariant reasoning. It does not justify the actual libstdc++ acquire/release
+operations or prove that adding barriers suffices. The C++ method specs remain
+assumed; the checked ghost-state and client lemmas are not a verification of
+libstdc++'s concurrent implementation. A weak-memory justification may require
+a different SharedPtrR and ownership-transfer protocol.
+
+- When calling the copy constructor, the caller's proof has to come up with their pieceid (< maxContention) and give up
+[pieceRight ctrlid pieceid], which they only get back when the newly constructed object is deleted.
+They get [Rpiece pieceid] in return: their piece of the ownership of the payload object.
+The new handle records [pieceid], so its destructor must return that piece.
+Identical fractional payload pieces are still interchangeable; their acquisition
+indices are not. A fractional ghost token inside each handle witnesses that
+its index is outstanding, even when ownership of the handle itself is split.
+The control block id (representing the location of the atomic reference counter) remains the same.
+The proof will atomically increment the counter to take out the Rpiece from the invariant.
+
+- There is another Rep predicate: [NullSharedPtrR]: for the case when the shared ptr represents a dummy null ptr, e.g. after a move constructor transfers away the ownerships to a new object.
+
+- The proved [redistributePayloadOwnership] in shared_ptr/redistribution.v can
+change the payload partition when the caller owns every live handle and its
+piece, plus every unused acquisition right. It requires equivalence of the
+whole payload ownership, at least one live handle, and explicit Timeless and
+WeaklyObjective conditions for the invariant migration. It returns a new ghost
+control-block identity while retaining all physical addresses and the actual
+reference count. The old, unconstrained admitted redistribution rule has been
+replaced, not retained as an alternative interface.
+A common pattern where this can be useful is when the thread that calls new needs to initialize the object after wrapping it in a shared_ptr but before sharing it with other concurrent threads. So until that event, it will have the exclusive ownership of the entire object (Rpiece n = emp for n>0, Rpiece 0= objR 1) and later, we redistribute with (Rpiece n => objR (1/N)).
+
+*)
+
+Require Import skylabs.auto.cpp.proof.
+Require Import skylabs.auto.cpp.hints.new_delete.
+Set Default Goal Selector "!".
+Require Import skylabs.brick.libstdcpp.allocator.spec.
+Require Import skylabs.brick.libstdcpp.cassert.spec.
+Require Import skylabs.brick.libstdcpp.vector.spec.
+Require Import skylabs.cpp.stdlib.atomic.spec.
+Require Import skylabs.brick.libstdcpp.algorithms.spec.
+Require Import skylabs.brick.libstdcpp.new.pred.
+Require Import skylabs.brick.libstdcpp.new.hints.
+Require Import skylabs.cpp.spec.concepts.
+Require Import skylabs.cpp.spec.concepts.experimental.
+Require Import skylabs.brick.libstdcpp.shared_ptr.inc_shared_ptr_cpp.
+Require Export skylabs.brick.libstdcpp.shared_ptr.layout.
+Require Export skylabs.brick.libstdcpp.shared_ptr.allocation.
+Require Export skylabs.brick.libstdcpp.shared_ptr.no_esft.
+Require Import iris.algebra.excl.
+Require Import iris.algebra.frac.
+
+NES.Open std.atomic.
+
+(* Preserve the names previously defined in this module. *)
+Abbreviation SP_impl := layout.SP_impl.
+Abbreviation SP_acc := layout.SP_acc.
+
+Record CtrlBlockId : Set :=
+  {
+    pieceRightLocs: list gname; (* each stores a unit. N -> gname may be tricky for constructor proof *)
+    pieceHandleLocs: list gname; (* Fractional outstanding-index witnesses. *)
+    dataLoc: ptr;
+    payload_type: type; (* Complete managed-object type, including array length.
+                          Not necessarily the type of an independent allocation. *)
+    payload_delete: option (name * option N);
+    (* Some (operator, alignment): raw adoption, with the whole delete
+       operation prepaid. None: in-place payload, destruction only. *)
+  }.
+
+#[local] Open Scope N_scope.
+(** libstdc++ stores [_Sp_counted_base::_M_use_count] in [_Atomic_word], an
+    alias of signed [int] on our target. The generated C++ AST records [Tint]
+    for that field. [inc_shared_ptr.cpp] checks that [_Atomic_word] is [int]
+    and has maximum value 2147483647. A 64-bit pointer does not imply a
+    64-bit reference count.
+
+    There are exactly [maxContention] piece indices, including index zero
+    for the initial owner. Consuming an available [pieceRight] before a copy
+    means at most [maxContention - 1] handles were outstanding; incrementing
+    then remains within [INT_MAX]. Destruction returns that index, so the
+    limit concerns simultaneous handles, not the lifetime number of copies.
+
+    The previous admitted lower bound [2^32 <= maxContention] was incompatible
+    with this signed 32-bit count. Fix the capacity instead of merely weakening
+    that lower bound while leaving the actual maximum unconstrained. This is
+    a correction of the assumed library interface, not a proof of libstdc++'s
+    shared-pointer implementation. *)
+(* [Opaque] alone does not block [vm_compute]. Seal the definition so clients
+   cannot accidentally expand [seq 0 (Pos.to_nat maxContention)]. *)
+mlock Definition maxContention : positive := 2147483647%positive.
+
+Lemma maxContentionLb : 2^31 - 1 <= Npos maxContention.
+Proof. rewrite maxContention.unlock. exact (N.le_refl _). Qed.
+
+Lemma maxContention_fits_int : (0 < Z.pos maxContention < 2^31)%Z.
+Proof. rewrite maxContention.unlock. split; reflexivity. Qed.
+
+Definition maxContentionQp := pos_to_Qp maxContention.
+Definition allPieceIds : list nat := (seq 0 (Pos.to_nat maxContention)).
+Definition allButFirstPieceId := (seq 1 (Pos.to_nat maxContention -1 )).
+
+Definition countLN {A : Type} (f : A -> bool) (l : list A) : N :=
+  lengthN (filter f l).
+
+(** Read the delete-expression selected by Clang in the default libstdc++
+    disposal path. In particular, absence of a virtual destructor does NOT
+    imply global operator delete. Reject missing/unrecognized bodies. *)
+Definition shared_ptr_delete_operator (tu : translation_unit) (ty : type)
+    : option name :=
+  let '(nm, arr, ety, operand) :=
+    match erase_qualifiers ty with
+    | Tarray _ _ =>
+        let ety := SP_element ty in
+        ((Nscoped "std::__sp_array_delete"
+          (Nop function_qualifiers.Nc OOCall [Tptr ety])).<<Atype ety>>,
+         true, ety, Ecast Cl2r (Evar "__p" (Tptr ety)))
+    | _ =>
+        let cn := shared_control_name SeparateAllocation ty in
+        (Nscoped cn (Nfunction function_qualifiers.N "_M_dispose" []),
+         false, ty, Ecast Cl2r
+           (Emember true (Ethis (Tptr (Tnamed cn)))
+             (Nid "_M_ptr") false (Tptr ty)))
+    end in
+  match tu.(symbols) !! nm with
+  | Some (Omethod m) =>
+      match m.(m_body) with
+      | Some (UserDefined (Sseq [Sexpr (Edelete arr' op operand' ety')])) =>
+          if bool_decide (arr = arr' /\ ety = ety' /\ operand = operand')
+          then Some op else None
+      | _ => None
+      end
+  | _ => None
+  end.
+
+Section specs.
+  Context `{Σ : cpp_logic, MOD:inc_shared_ptr_cpp.source ⊧ σ}.
+  #[local] Existing Instance br.ghost.excl_inG.
+  #[local] Existing Instance br.ghost.frac_inG.
+
+  (* The capability may capture persistent destructor specs. [destroy_val]
+     already admits an initial fancy update, so callers may cancel payload
+     invariants before destroying the object. Final release must first close
+     the reference-count invariant, then invoke this capability. The allocation
+     token remains separate for the subsequent deallocation. *)
+  Definition payload_destructible (ty : type) (Rpiece : nat -> Rep) : mpred :=
+    □ (Forall p : ptr,
+      p |-> ([∗ list] pieceid ∈ allPieceIds, Rpiece pieceid) -*
+      destroy_val (genv_tu σ) ty p emp).
+
+  (** The allocation token and every payload piece jointly fund the actual
+      delete operation, including class-specific deallocation and its effects.
+      Callers can put any required external resources in the pieces. *)
+  Definition payload_deletable (ty : type) (op : name) (alignment : option N)
+      (Rpiece : nat -> Rep) : mpred :=
+    □ (Forall p : ptr,
+      (p |-> ([∗ list] pieceid ∈ allPieceIds, Rpiece pieceid) **
+       p |-> alloc.tokenR_with_alignment ty alignment 1%Qp) -*
+      wp_delete_dispatch op ty p emp).
+
+  Definition payload_releasable (id : CtrlBlockId) (Rpiece : nat -> Rep) : mpred :=
+    match payload_delete id with
+    | Some (op, alignment) =>
+        (* Keep selection evidence in each handle: the allocation invariant
+           alone does not distinguish different deallocation functions. *)
+        [| exists tu : translation_unit,
+             tu ⊧ σ /\
+             shared_ptr_delete_operator tu (payload_type id) = Some op |] **
+        payload_deletable (payload_type id) op alignment Rpiece
+    | None => payload_destructible (payload_type id) Rpiece
+    end.
+
+  Definition payload_allocation (id : CtrlBlockId) (p : ptr) : mpred :=
+    match payload_delete id with
+    | Some (_, alignment) =>
+        SharedAllocationR SeparateAllocation (payload_type id) alignment (dataLoc id) p
+    | None =>
+        SharedAllocationR CombinedAllocation (payload_type id) None (dataLoc id) p
+    end.
+
+  Definition control_block_rest (id : CtrlBlockId) (p : ptr) : mpred :=
+    ControlBlockRestR
+      (match payload_delete id with
+       | Some _ => SeparateAllocation
+       | None => CombinedAllocation
+       end)
+      (payload_type id) (dataLoc id) p.
+
+  #[global] Instance control_block_rest_timeless id p :
+    Timeless (control_block_rest id p).
+  Proof. unfold control_block_rest. apply _. Qed.
+
+  #[global] Instance payload_releasable_persistent id R :
+    Persistent (payload_releasable id R).
+  Proof.
+    unfold payload_releasable.
+    destruct (payload_delete id) as [[op alignment]|]; apply _.
+  Qed.
+
+  #[global] Instance payload_releasable_affine id R :
+    Affine (payload_releasable id R).
+  Proof.
+    unfold payload_releasable.
+    destruct (payload_delete id) as [[op alignment]|]; apply _.
+  Qed.
+
+  Section tty. Context (ty:type).
+
+  Import linearity.
+
+
+  (* just an exclusive token for each pieceid. can be defined with a simpler CMRA as fractionality is not needed. fgptsoQ has good automation support  *)
+  Definition pieceRight ctrlid pieceid : mpred :=
+    match nth_error (pieceRightLocs ctrlid) pieceid with
+    | Some g => own (A := exclR unitO) g (Excl ())
+    | None => emp (* bad argument, pieceid > maxContention *)
+    end.
+
+  #[global] Hint Opaque pieceRight : sl_opacity.
+
+  (* The full token is in the invariant while this index is available, and in
+     the handle while it is outstanding. Unlike [pieceRight], this token must
+     split when a client shares read ownership of the same handle. *)
+  Definition pieceHandle ctrlid (q : Qp) pieceid : mpred :=
+    match nth_error (pieceHandleLocs ctrlid) pieceid with
+    | Some g => own (A := fracR) g q
+    | None => False
+    end.
+
+  #[global] Instance pieceHandle_fractional id i :
+    Fractional (fun q => pieceHandle id q i).
+  Proof.
+    unfold pieceHandle.
+    destruct (nth_error (pieceHandleLocs id) i) as [g |].
+    { intros q1 q2. rewrite <- own_op. reflexivity. }
+    { apply _. }
+  Qed.
+
+  Definition sptrInv (id: CtrlBlockId) (Rpiece : nat -> Rep) (ownedPtr:ptr) (pieceOut : nat ->bool) : mpred :=
+    let ctrVal := countLN pieceOut allPieceIds in
+    ([∗ list] pieceid ∈ allPieceIds,
+               if pieceOut pieceid then pieceRight id pieceid
+               else pieceHandle id 1 pieceid)
+         ** (if (bool_decide (ctrVal = 0))
+              then emp
+              else (dataLoc id) .,
+                     (SP_counted_base .:: Nid "_M_use_count")
+                     |-> intR 1$m (Z.of_N ctrVal)
+                    ** control_block_rest id ownedPtr
+                    ** payload_allocation id ownedPtr
+                    ** ([∗ list] pieceid ∈ allPieceIds,
+                      if pieceOut pieceid then emp else ownedPtr |-> Rpiece pieceid)).
+
+  (** [_M_use_count] is a raw [int] accessed by atomic builtins, not a
+      [std::atomic<long>] subobject. The invariant protects its ownership.
+      At the last release all physical resources leave this invariant: the
+      releasing thread destroys the payload and frees the control block.
+      The zero-count state retains only ghost tokens. A live handle excludes
+      that state by [pieceHandle_live] in [handle_liveness.v]. This also
+      permits closing the invariant before running a reentrant destructor.
+
+      [control_block_rest] owns the weak counter at 1 and the abstract
+      remaining control-block layout, separately from allocation and payload
+      ownership. It is stored ONCE here, not duplicated in each handle.
+      Both raw-adoption and factory specs return this strengthened invariant;
+      their eventual body proofs must establish its physical ownership.
+
+      The layout token and its Timeless law remain assumed. A complete body
+      proof must define that token and justify dispatch, the combined load of
+      both counters, and actual acquire/release synchronization. For array
+      factories it must also connect _M_n/_S_tail to allocation size and
+      recover padding for deallocation. No external weak_ptr is supported. *)
+  
+  (** The control-block model above remains abstract. [SharedPtrHandleR]
+      describes the complete handle, not the object its [_M_pi] points to. *)
+  (* [q] describes this handle, not the shared control block or a payload
+     piece. In particular, splitting [q] does not create a [pieceRight]. *)
+  Definition SharedPtrR (q : cQp.t) (id: CtrlBlockId) (pieceid : nat)
+      (Rpiece : nat -> Rep) (ownedPtr:ptr) : Rep :=
+    SharedPtrHandleR ty q ownedPtr (dataLoc id)
+    (* Managed-type compatibility alone is not permission to delete ownedPtr.
+       The stable cleanup descriptor governs both the capability and allocation. *)
+    ** [| delete_compat ty (payload_type id) |]
+    ** pureR (payload_releasable id Rpiece)
+    ** [| ownedPtr<>nullptr |] (* use NullSharedPtr otherwise *)
+    ** [| lengthN (pieceRightLocs id) = Npos maxContention |]
+    ** [| lengthN (pieceHandleLocs id) = Npos maxContention |]
+    ** [| (N.of_nat pieceid < Npos maxContention)%N |]
+    ** pureR (pieceHandle id (cQp.frac q) pieceid)
+    ** pureR (inv nroot (Exists (pieceOut : nat ->bool), sptrInv id Rpiece ownedPtr pieceOut)).
+
+  Definition NullSharedPtrR (q : cQp.t) : Rep :=
+    SharedPtrHandleR ty q nullptr nullptr.
+
+  #[global] Instance SharedPtrR_fractional id i Rpiece p :
+    CFractional (fun q => SharedPtrR q id i Rpiece p) := _.
+  #[global] Instance SharedPtrR_as_fractional q id i Rpiece p :
+    AsCFractional (SharedPtrR q id i Rpiece p)
+      (fun q => SharedPtrR q id i Rpiece p) q.
+  Proof. split; [done | apply _]. Qed.
+  #[global] Instance NullSharedPtrR_fractional :
+    CFractional NullSharedPtrR := _.
+  #[global] Instance NullSharedPtrR_as_fractional q :
+    AsCFractional (NullSharedPtrR q) NullSharedPtrR q.
+  Proof. split; [done | apply _]. Qed.
+
+  #[local] Definition SharedPtrHandleR_const_C :=
+    [CANCEL] SharedPtrHandleR_const.
+  #[local] Hint Opaque pieceHandle payload_releasable payload_allocation control_block_rest
+    payload_destructible payload_deletable sptrInv : sl_opacity.
+
+  Lemma SharedPtrR_const id pieceid Rpiece ownedPtr :
+    const.CONST (shared_ptr_const_tu ty) (Tnamed (SP_name ty))
+      (fun q => SharedPtrR q id pieceid Rpiece ownedPtr).
+  Proof.
+    const.prove.
+    unfold SharedPtrR.
+    go using SharedPtrHandleR_const_C.
+  Qed.
+
+  Lemma NullSharedPtrR_const :
+    const.CONST (shared_ptr_const_tu ty) (Tnamed (SP_name ty))
+      NullSharedPtrR.
+  Proof. apply SharedPtrHandleR_const. Qed.
+
+  Definition SharedPtrR_const_C := [CANCEL] SharedPtrR_const.
+  Definition NullSharedPtrR_const_C := [CANCEL] NullSharedPtrR_const.
+
+
+  Definition init_ctor :=
+    specify {| info_name := (Nscoped ("std::shared_ptr".<<Atype ty>>) (Nctor [Tptr ty])).<<Atype ty, Atype "void">>
+            ; info_type := tCtor ("std::shared_ptr".<<Atype ty>>) [Tptr ty] |} (fun (this:ptr) =>
+    \arg{p:ptr} "ownedPtr" (Vptr p)
+    (* Adoption may initialize enable_shared_from_this's internal weak handle.
+       This interface frames the payload unchanged, so excludes that case. *)
+    \pre [| shared_ptr_no_esftb ty = true |]
+    \pre match ty with
+         | Tarray _ _ => False
+         | Tincomplete_array _ => False
+         | _ => emp
+        end
+        
+    \pre{Rpiece: nat -> Rep} [∗ list] pieceid ∈ allButFirstPieceId, p |-> Rpiece pieceid
+    (* ^ morally, the caller gives up all the pieces and gets back the 0th piece. The remaining pieces get stored in the invariant.
+       Should this object be destructed immediately, the destructor will need all the pieces to call delete. 
+       We frame away the 0th piece in this spec. A derived spec can be proven where that framing away is not done *)
+    \pre{tu op alignment} [| tu ⊧ σ |]
+    \pre [| shared_ptr_delete_operator tu ty = Some op |]
+    \pre p |-> alloc.tokenR_with_alignment ty alignment 1%Qp
+    (* ^ gets stored in the invariant. only gets taken out when the count becomes 0, to call delete. at that time the ownership of all other pieces are also taken out from the invariant *)
+    \pre payload_deletable ty op alignment Rpiece
+    \post Exists (ctrlBlockId: CtrlBlockId),
+       [| payload_type ctrlBlockId = ty |] **
+       [| payload_delete ctrlBlockId = Some (op, alignment) |] **
+       this |-> SharedPtrR 1$m ctrlBlockId 0 Rpiece p
+         ** ([∗ list] pieceid ∈ allButFirstPieceId, pieceRight ctrlBlockId pieceid)
+         (*  ^ the right to create [maxContention-1] more shared_ptr objects on this payload and claim the correponsing Rpiece ownerships at copy construction *)
+      ).
+
+  Definition SpecFor_init_ctor := RegisterSpec init_ctor.
+  #[global] Existing Instance SpecFor_init_ctor.
+
+  Notation spty := ("std::shared_ptr".<<Atype ty>>).
+  Definition move_ctor :=
+    specify.template.ctor spty [Trv_ref ((Tnamed spty))] $
+    \this this
+    \arg{other:ptr} "other" (Vptr other)
+    \pre{ctrlBlockId pieceid ownedPtr Rpiece} other |-> SharedPtrR 1$m ctrlBlockId pieceid Rpiece ownedPtr
+    \post other  |-> NullSharedPtrR 1$m
+          ** this |-> SharedPtrR 1$m ctrlBlockId pieceid Rpiece ownedPtr.
+
+  Definition SpecFor_move_ctor := RegisterSpec move_ctor.
+  #[global] Existing Instance SpecFor_move_ctor.
+
+  Definition dtor_spec :=
+    specify.template.dtor spty $
+    \this this
+    \pre{(null:bool) (p:ptr) (sid: if null then unit else prod CtrlBlockId nat) Rpiece}
+      (* The handle lives at [this]; its outstanding payload piece lives at [p]. *)
+      (match null as b return (if b then unit else prod CtrlBlockId nat) -> mpred with
+                | false => fun sid=>
+                             this |-> SharedPtrR 1$m sid.1 sid.2 Rpiece p
+                             ** p |-> Rpiece sid.2
+                | true => fun sid=> this |-> NullSharedPtrR 1$m
+                end) sid
+
+    \post (match null as b return (if b then unit else prod CtrlBlockId nat) -> mpred with
+                | false => fun sid=> pieceRight sid.1 sid.2
+                | true => fun sid=> emp
+                end) sid.
+  
+  Definition SpecFor_dtor := RegisterSpec dtor_spec.
+  #[global] Existing Instance SpecFor_dtor.
+
+
+  Definition copy_ctor :=
+    specify.template.ctor spty [Tref (Tconst (Tnamed spty))] $
+    \this this
+    \arg{other:ptr} "other" (Vptr other)
+    \prepost{q (null : bool) id source_pieceid p Rpiece}
+      if null then other |-> NullSharedPtrR q
+      else other |-> SharedPtrR q id source_pieceid Rpiece p
+    \pre{pieceid}
+      if null then emp
+      else pieceRight id pieceid ** [| N.of_nat pieceid < Npos maxContention |]%N
+    \post
+      if null then this |-> NullSharedPtrR 1$m
+      else p |-> Rpiece pieceid ** this |-> SharedPtrR 1$m id pieceid Rpiece p.
+
+  Definition SpecFor_copy_ctor := RegisterSpec copy_ctor.
+  #[global] Existing Instance SpecFor_copy_ctor.
+
+  (** These are derived specializations, not independent registered library
+      assumptions. Empty copying neither acquires a piece nor changes a count. *)
+  Definition copy_ctor_nonnull :=
+    specify.template.ctor spty [Tref (Tconst (Tnamed spty))] $
+    \this this
+    \arg{other:ptr} "other" (Vptr other)
+    \prepost{q id source_pieceid p Rpiece} other |-> SharedPtrR q id source_pieceid Rpiece p
+    \pre{pieceid} pieceRight id pieceid (* this will be returned by destructor *)
+    \pre [| N.of_nat pieceid < Npos maxContention|]%N
+    \post
+         p|->Rpiece pieceid ** this  |-> SharedPtrR 1$m id pieceid Rpiece p.
+                          
+  Definition copy_ctor_null :=
+    specify.template.ctor spty [Tref (Tconst (Tnamed spty))] $
+    \this this
+    \arg{other:ptr} "other" (Vptr other)
+    \prepost{q} other |-> NullSharedPtrR q
+    \post this  |-> NullSharedPtrR 1$m.
+
+  #[local] Hint Opaque SharedPtrR NullSharedPtrR : sl_opacity.
+
+  Lemma copy_ctor_nonnull_from_copy : copy_ctor |-- copy_ctor_nonnull.
+  Proof.
+    unfold copy_ctor, copy_ctor_nonnull.
+    apply specify_mono_fupd. go.
+    rewrite <- fupd_intro.
+    iExists q, false, id, source_pieceid, p, Rpiece, pieceid.
+    go.
+    rewrite <- fupd_intro. go.
+  Qed.
+
+  Lemma copy_ctor_null_from_copy : copy_ctor |-- copy_ctor_null.
+  Proof.
+    unfold copy_ctor, copy_ctor_null.
+    apply specify_mono_fupd. go.
+    rewrite <- fupd_intro.
+    iExists q, true,
+      {| pieceRightLocs := []; pieceHandleLocs := [];
+         dataLoc := nullptr; payload_type := ty; payload_delete := None |},
+      0%nat, nullptr, (fun _ => emp), 0%nat.
+    go.
+    rewrite <- fupd_intro. go.
+  Qed.
+
+  (** Reconstruct the most-derived object pointer from the base-subobject "this". *)
+  Definition upcast_offset (mid: Z) : offset :=
+    (o_derived σ (SP_acc ty mid) (SP_impl ty) ,, o_derived σ (SP_impl ty) spty).
+
+  Definition deref :=
+    specify.template.op (SP_acc ty 0) OOStar function_qualifiers.Nc (Tref ty) [] $
+       \this this
+       \prepost{q id pieceid p Rpiece} this |-> (upcast_offset 0) |-> SharedPtrR q id pieceid Rpiece p
+       \post[Vref p] emp.
+
+  Definition SpecFor_deref := RegisterSpec deref.
+  #[global] Existing Instance SpecFor_deref.
+  #[global] Hint Opaque deref : sl_opacity.
+
+  Definition arrow :=
+    specify.template.op (SP_acc ty 0) OOArrow function_qualifiers.Nc (Tptr ty) [] $
+       \this this
+       \prepost{q id pieceid p Rpiece} this |-> (upcast_offset 0) |-> SharedPtrR q id pieceid Rpiece p
+       \post[Vptr p] emp.
+
+  Definition SpecFor_arrow := RegisterSpec arrow.
+  #[global] Existing Instance SpecFor_arrow.
+  #[global] Hint Opaque arrow : sl_opacity.
+  
+  #[global] Instance sharedR_typeptr_observe q id pieceid (p:ptr) op Rpiece
+    : Observe (type_ptr (Tnamed ("std::shared_ptr".<<Atype ty>>)) p) (p|->SharedPtrR q id pieceid Rpiece op):= _.
+  
+  Definition observeSharedTypeF q id pieceid t Rpiece op:= @observe_fwd _ _ _ (sharedR_typeptr_observe q id pieceid t Rpiece op).
+
+  End tty.
+
+  Definition init_ctor_arr ety :=
+    specify {| info_name := (Nscoped ("std::shared_ptr".<<Atype (Tincomplete_array ety)>>) (Nctor [Tptr ety])).<<Atype ety, Atype "void">>
+            ; info_type := tCtor ("std::shared_ptr".<<Atype (Tincomplete_array ety)>>) [Tptr ety] |} (fun (this:ptr) =>
+    \arg{p:ptr} "ownedPtr" (Vptr p)
+    \pre{Rpiece: nat -> Rep} [∗ list] pieceid ∈ allButFirstPieceId, p |-> Rpiece pieceid
+    (* ^ morally, the caller gives up all the pieces and gets back the 0th piece. The remaining pieces get stored in the invariant.
+       Should this object be destructed immediately, the destructor will need all the pieces to call delete. 
+       We frame away the 0th piece in this spec. A derived spec can be proven where that framing away is not done *)
+    \let{len} ty := Tarray ety len
+    \pre{tu op alignment} [| tu ⊧ σ |]
+    \pre [| shared_ptr_delete_operator tu ty = Some op |]
+    \pre p |-> alloc.tokenR_with_alignment ty alignment 1%Qp
+    (* ^ gets stored in the invariant. only gets taken out when the count becomes 0, to call delete. at that time the ownership of all other pieces are also taken out from the invariant *)
+    \pre payload_deletable ty op alignment Rpiece
+    \post Exists (ctrlBlockId: CtrlBlockId),
+       [| payload_type ctrlBlockId = ty |] **
+       [| payload_delete ctrlBlockId = Some (op, alignment) |] **
+       this |-> SharedPtrR (Tincomplete_array ety) 1$m ctrlBlockId 0 Rpiece p
+         ** ([∗ list] pieceid ∈ allButFirstPieceId, pieceRight ctrlBlockId pieceid)
+         (*  ^ the right to create [maxContention-1] more shared_ptr objects on this payload and claim the correponsing Rpiece ownerships at copy construction *)
+      ).
+  
+  Definition SpecFor_init_ctor_arr := RegisterSpec init_ctor_arr.
+  #[global] Existing Instance SpecFor_init_ctor_arr.
+
+  Definition subscript ety:=
+    specify.template.op (SP_acc (Tincomplete_array ety) 1) OOSubscript function_qualifiers.Nc (Tref ety) ["long"%cpp_type] $
+      \this this
+      \arg{index} "index" (Vint index)
+      \prepost{q id pieceid p Rpiece} this |-> (upcast_offset (Tincomplete_array ety) 1) |-> SharedPtrR (Tincomplete_array ety ) q id pieceid Rpiece p
+      \pre{len : N} [| payload_type id = Tarray ety len |]
+      \pre [| (0 <= index < Z.of_N len)%Z |]
+      \post[Vref (p.[ety ! index])] emp.
+
+  Definition SpecFor_subscript := RegisterSpec subscript.
+  #[global] Existing Instance SpecFor_subscript.
+
+  #[global] Hint Opaque
+    init_ctor move_ctor dtor_spec copy_ctor copy_ctor_nonnull copy_ctor_null
+    deref arrow init_ctor_arr subscript
+    : sl_opacity.
+
+End specs.
+#[global] Hint Opaque SharedPtrR NullSharedPtrR payload_destructible
+  payload_deletable payload_releasable payload_allocation control_block_rest : sl_opacity.
+#[global] Hint Resolve SharedPtrR_const_C NullSharedPtrR_const_C : sl_opacity.
+#[global]
+  Hint Resolve observeSharedTypeF : sl_opacity.
+Ltac sharedPtrRpieceFromPost :=
+  match goal with
+    H: context[@PostCondition ?a ?b ?c ?d] |- _
+    => match c with
+       | context[SharedPtrR _ _ _ _ ?rp _ ] => constr:(rp)
+       end                            
+  end.
diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/test.cpp b/rocq-brick-libstdcpp/proof/shared_ptr/test.cpp
new file mode 100644
index 00000000..cfef48c9
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/shared_ptr/test.cpp
@@ -0,0 +1,61 @@
+#include<memory>
+
+std::shared_ptr<int> testshared1() {
+    auto x= std::shared_ptr<int>(new int);
+    *x=1;
+    return x;
+  }
+
+std::shared_ptr<int[]> testsharedarr() {
+    auto x= std::shared_ptr<int[]>(new int[2]);
+    x[0]=1;
+    x[1]=2;
+    return x;
+  }
+
+int scalar_deletions = 0;
+int array_deletions = 0;
+
+struct ClassDelete {
+    int value = 42;
+    static void operator delete(void* p) noexcept {
+        ++scalar_deletions;
+        ::operator delete(p);
+    }
+    static void operator delete[](void* p) noexcept {
+        ++array_deletions;
+        ::operator delete[](p);
+    }
+};
+
+// Global new does not suppress class-specific lookup at the later delete.
+int test_delete_effects() {
+    scalar_deletions = 0;
+    array_deletions = 0;
+    {
+        std::shared_ptr<ClassDelete> p(::new ClassDelete);
+    }
+    if (scalar_deletions != 1 || array_deletions != 0) return 1;
+    {
+        std::shared_ptr<ClassDelete[]> p(::new ClassDelete[2]);
+    }
+    if (scalar_deletions != 1 || array_deletions != 1) return 2;
+    {
+        std::shared_ptr<ClassDelete> p = std::make_shared<ClassDelete>();
+        std::shared_ptr<ClassDelete[]> a = std::make_shared<ClassDelete[]>(2);
+    }
+    if (scalar_deletions != 1 || array_deletions != 1) return 3;
+    return 0;
+}
+
+void test_shared_copy_empty(std::shared_ptr<int> const& source) {
+    std::shared_ptr<int> copy(source);
+}
+
+#ifdef SHARED_PTR_DELETE_EFFECTS_TEST
+int main() {
+    std::shared_ptr<int> empty;
+    test_shared_copy_empty(empty);
+    return test_delete_effects();
+}
+#endif
diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/test.v b/rocq-brick-libstdcpp/proof/shared_ptr/test.v
new file mode 100644
index 00000000..4f4736bb
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/shared_ptr/test.v
@@ -0,0 +1,252 @@
+Require Import skylabs.auto.cpp.proof.
+Require Import skylabs.cpp.stdlib.allocator.spec.
+Require Import skylabs.cpp.stdlib.cassert.spec.
+Require Import skylabs.cpp.stdlib.vector.spec.
+Require Import skylabs.cpp.stdlib.atomic.spec.
+Require Import skylabs.cpp.stdlib.algorithms.spec.
+Require Import skylabs.brick.libstdcpp.new.pred.
+Require Import skylabs.brick.libstdcpp.new.spec_exc.
+Require Import skylabs.brick.libstdcpp.new.hints.
+Require Import skylabs.cpp.spec.concepts.
+Require Import skylabs.cpp.spec.concepts.experimental.
+Require Import skylabs.brick.libstdcpp.shared_ptr.test_cpp.
+Require Import skylabs.brick.libstdcpp.shared_ptr.specs.
+
+Example selected_class_scalar_delete :
+  shared_ptr_delete_operator source "ClassDelete" =
+    Some "ClassDelete::operator delete(void*)"%cpp_name.
+Proof. vm_compute. reflexivity. Qed.
+
+Example selected_class_array_delete :
+  shared_ptr_delete_operator source "ClassDelete[2]" =
+    Some "ClassDelete::operator delete[](void*)"%cpp_name.
+Proof. vm_compute. reflexivity. Qed.
+
+
+Section deletion_selection.
+  Context `{Σ : cpp_logic} {σ : genv} {hf : fracG () _Σ}.
+  Set Default Goal Selector "!".
+  #[local] Hint Opaque pieceHandle sptrInv : sl_opacity.
+
+  Lemma raw_handle_retains_delete_selection ty q id i R p (handle : ptr) op alignment :
+    payload_delete id = Some (op, alignment) ->
+    handle |-> SharedPtrR ty q id i R p |--
+      [| exists tu : translation_unit,
+           tu ⊧ σ /\
+           shared_ptr_delete_operator tu (payload_type id) = Some op |].
+  Proof.
+    intros Hdelete.
+    unfold SharedPtrR, payload_releasable.
+    rewrite Hdelete.
+    go.
+  Qed.
+End deletion_selection.
+
+
+(* TODO: upstream the hints/lemmas, to where? *)
+Hint Resolve NoDup_seq : setsolver.
+Hint Rewrite elem_of_seq: equiv.
+Hint Rewrite @big_sepL_emp: equiv.
+
+Lemma seqprefix (prelen len start: nat):
+  (prelen <= len)%nat -> seq start len = (seq start prelen)++(seq (start+prelen) (len -prelen)).
+Proof using.
+  intros Hl.
+  replace len with (prelen+(len-prelen))%nat at 1 by lia.
+  rewrite seq_app.
+  reflexivity.
+Qed.
+  
+Lemma one_as_bigsep {PROP: bi} {A} {eqd: EqDecision A} (f  : PROP) l (x: A):
+  x ∈ l ->
+  NoDup l -> (* too strong: we only need x to be not duplicated *)
+  f -|- ([∗ list] id ∈ l, if bool_decide (id=x) then f else emp)%I.
+Proof using.
+  intros.
+  rewrite  -> big_op.big_sepL_difference_singleton with (x:=x) by assumption.
+  simpl.
+  case_bool_decide; [ | congruence].
+  assert (f ** (emp)%I ≡ f) as Heq by (apply right_id; eauto with typeclass_instances).
+  rewrite <- Heq at 1.
+  f_equiv.
+  transitivity ([∗ list] _ ∈ list_difference l [x], (emp : PROP))%I.
+  { symmetry. apply big_sepL_emp. }
+  apply big_opL_proper.
+  intros  ? id  Hl.
+  case_decide;[ | reflexivity].
+  subst.
+  apply list_elem_of_lookup_2 in Hl.
+  apply list_elem_of_difference in Hl.
+  forward_reason.
+  apply False_rect.
+  simpl in *.
+  set_solver.
+Qed.
+
+Section proofs.
+  #[local] Set Warnings "-sl-transparent-constants".
+  Opaque SharedPtrR.
+  Context `{Σ : cpp_logic, MOD:test_cpp.source ⊧ σ}
+  {hf:fracG () _Σ}.
+  
+
+  cpp.spec "testshared1()" as testshared1spec with (
+    \pre operator_delete_size
+    \post{p:ptr}[Vptr p] Exists payload sid,
+       [| payload_type sid = "int"%cpp_type |] **
+       p |-> SharedPtrR "int" 1$m sid 0 (fun ctid => if bool_decide (ctid=0%nat) then anyR "int" 1 else emp) payload
+       ** payload |-> intR (cQp.m 1) 1
+       ** ([∗ list] ctid ∈ allButFirstPieceId,
+              pieceRight sid ctid)
+    ).
+
+
+
+  Lemma allButFirstEmp ty : ([∗ list] x ∈ seq 1 (Pos.to_nat maxContention -1), 
+       if bool_decide (x = 0%nat)
+       then anyR ty 1$m
+       else emp)
+                         -|- emp.
+  Proof using.
+    erewrite  big_opL_proper with (g := fun _ _=> emp).
+    2:{ intros ? ? Hl.
+        apply list_elem_of_lookup_2 in Hl.
+        autorewrite with equiv in Hl.
+        resolveDecide lia.
+        reflexivity.
+    }
+    autorewrite with equiv.
+    reflexivity.
+  Qed.
+  
+  Opaque NullSharedPtrR.
+  #[global] Instance lll: LearnEq6 SharedPtrR :=
+    ltac:(solve_learnable).
+
+Set Default Goal Selector "!".  
+  Lemma prf2: verify[source] testshared1spec.
+  Proof using MOD.
+    verify_spec.
+    pose proof maxContentionLb.
+    go.
+    let r := sharedPtrRpieceFromPost in
+      set (Rpiece := r).
+    iExists Rpiece.
+    go.
+    simpl.
+    eagerUnifyU.
+    go.
+    normalize_ptrs.
+    eagerUnifyU.
+    go.
+    iExists source.
+    iExists "operator delete(void*, unsigned long)"%cpp_name.
+    rewrite <- _at_big_sepL.
+    unfold allButFirstPieceId.
+    rewrite allButFirstEmp. go.
+    assert (Hdestroy : denoteModule source ** operator_delete_size |--
+      payload_deletable "int" "operator delete(void*, unsigned long)" None Rpiece).
+    {
+      unfold Rpiece.
+      unfold payload_deletable, allPieceIds.
+      rewrite -> seqprefix with (prelen:=1%nat) by lia.
+      simpl.
+      setoid_rewrite (allButFirstEmp "int"). go.
+    }
+    rewrite <- Hdestroy.
+    go.
+    normalize_ptrs.
+    go.
+    normalize_ptrs.
+    repeat iExists _.
+    eagerUnifyC.
+    go.
+    iExists true.
+    go.
+    iExists nullptr.
+    iExists tt.
+    iExists (fun _ => emp).
+    go.
+  Qed.
+
+  (* Array client regression: retain the complete managed-array type and the
+     initialized elements. The shared-pointer library method specs are assumed;
+     [prf3] also states its allocation-size premise explicitly. *)
+  cpp.spec "testsharedarr()" as testsharedarrspec with (
+    \pre operator_delete_array
+    \post{p:ptr}[Vptr p] Exists payload sid,
+       [| payload_type sid = "int[2]"%cpp_type |] **
+       p |-> SharedPtrR "int[]" 1$m sid 0 (fun ctid => if bool_decide (ctid=0%nat) then anyR "int[2]" 1 else emp) payload
+       ** payload |-> arrayR "int" (fun t => intR 1 t) [1;2]%Z
+       ** ([∗ list] ctid ∈ allButFirstPieceId,
+              pieceRight sid ctid)
+      ).
+
+  
+  Lemma prf3: (SIZE_MAX = 2^64)%N -> verify[source] testsharedarrspec.
+  Proof using MOD.
+    verify_spec.
+    go;[lia|].
+    let r := sharedPtrRpieceFromPost in
+      set (Rpiece := r).
+    iExists Rpiece.
+    go.
+    simpl.
+    eagerUnifyU.
+    go.
+    normalize_ptrs.
+    ring_simplify_goal_Z.
+    normalize_ptrs.
+    go.
+    eagerUnifyU.
+    go.
+    iExists source.
+    iExists "operator delete[](void*)"%cpp_name.
+    rewrite <- _at_big_sepL.
+    unfold allButFirstPieceId.
+    rewrite allButFirstEmp. go.
+    assert (Hdestroy : denoteModule source ** operator_delete_array |--
+      payload_deletable "int[2]" "operator delete[](void*)" None Rpiece).
+    {
+      unfold Rpiece.
+      unfold payload_deletable, allPieceIds.
+      rewrite -> seqprefix with (prelen:=1%nat) by lia.
+      simpl.
+      setoid_rewrite (allButFirstEmp "int[2]").
+      go.
+    }
+    rewrite <- Hdestroy.
+    go.
+    normalize_ptrs.
+    go.
+    normalize_ptrs.
+    go.
+    simpl.
+    unfold replicateN.
+    simpl.
+    repeat rewrite arrayR_cons.
+    go.
+    normalize_ptrs.
+    go.
+    normalize_ptrs.
+    go.
+    iExists 2%N.
+    go.
+    iExists 2%N.
+    go.
+    normalize_ptrs.
+    go.
+    iExists true.
+    go.
+    iExists nullptr.
+    iExists tt.
+    iExists (fun _ => emp).
+    go.
+    repeat rewrite arrayR_cons.
+    go.
+    normalize_ptrs.
+    go.
+    repeat rewrite arrayR_nil.
+    go.
+  Qed.
+End proofs.
diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/token_pool.v b/rocq-brick-libstdcpp/proof/shared_ptr/token_pool.v
new file mode 100644
index 00000000..be51de54
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/shared_ptr/token_pool.v
@@ -0,0 +1,295 @@
+(** A finite pool of the existing shared-pointer acquisition tokens.
+    Credits account for available tokens; the persistent invariant alone does
+    not authorize a copy. These lemmas use ghost-state rules, not the assumed
+    C++ constructor or destructor specs. *)
+Require Import skylabs.auto.cpp.proof.
+Require Import skylabs.auto.invariants.
+Require Import skylabs.base_logic.lib.own_auth.
+Require Import skylabs.brick.libstdcpp.shared_ptr.specs.
+Require Import iris.algebra.auth iris.algebra.numbers.
+Require Import skylabs.iris.extra.bi.algebra.
+Require Import skylabs.iris.extra.proofmode.own_obs.
+
+Set Default Goal Selector "!".
+#[local] Set Warnings "+sl-transparent-constants".
+Import linearity.
+#[local] Hint Opaque SharedPtrR : sl_opacity.
+
+Module TokenPool.
+Section pool.
+  Context `{Sigma : cpp_logic}.
+  #[local] Existing Instances br.ghost.auth_nat_inG br.ghost.excl_inG.
+
+  Definition valid_indices (id : CtrlBlockId) (indices : gset nat) : Prop :=
+    forall i, i ∈ indices ->
+      (i < length (pieceRightLocs id))%nat /\
+      (N.of_nat i < N.pos maxContention)%N.
+
+  Definition credits (gamma : gname) (n : nat) : mpred :=
+    own gamma (◯ n : authR natUR).
+
+  Definition pool_body (gamma : gname) (id : CtrlBlockId)
+      (indices : gset nat) : mpred :=
+    Exists free : gset nat,
+      [| free ⊆ indices |] **
+      own gamma (● size free : authR natUR) **
+      [∗ set] i ∈ free, pieceRight id i.
+
+  Definition pool (ns : namespace) (gamma : gname) (id : CtrlBlockId)
+      (indices : gset nat) : mpred :=
+    [| valid_indices id indices |] ** inv ns (pool_body gamma id indices).
+
+  #[local] Hint Opaque pool pool_body credits pieceRight : sl_opacity.
+
+  #[global] Instance pool_persistent ns gamma id indices :
+    Persistent (pool ns gamma id indices) := _.
+
+  #[global] Instance pool_body_timeless gamma id indices :
+    Timeless (pool_body gamma id indices).
+  Proof.
+    unfold pool_body, pieceRight.
+    apply _.
+  Qed.
+
+  Lemma credits_add gamma n m :
+    credits gamma (n + m) -|- credits gamma n ** credits gamma m.
+  Proof.
+    unfold credits.
+    exact (own_op gamma (◯ n : authR natUR) (◯ m)).
+  Qed.
+
+  Lemma credits_zero gamma : emp |-- (|==> credits gamma 0)%I.
+  Proof.
+    exact (own_unit (PROP := mpredI) (A := authUR natUR) gamma).
+  Qed.
+
+  Lemma pieceRight_exclusive id i :
+    (i < length (pieceRightLocs id))%nat ->
+    pieceRight id i ** pieceRight id i |-- False.
+  Proof.
+    intros Hbound.
+    unfold pieceRight.
+    destruct (nth_error (pieceRightLocs id) i) as [name |] eqn:Hlookup.
+    {
+      rewrite <- own_op, own_valid, excl_op_validI.
+      reflexivity.
+    }
+    {
+      apply nth_error_None in Hlookup.
+      lia.
+    }
+  Qed.
+
+  #[local] Instance counter_bound gamma available used :
+    Observe2 [| (used <= available)%nat |]
+      (own gamma (● available : authR natUR)) (credits gamma used).
+  Proof.
+    unfold credits.
+    rewrite <- (nat_included used available).
+    exact (auth_both_included' gamma 1 available used).
+  Qed.
+
+  Lemma counter_take gamma available k :
+    (S k <= available)%nat ->
+    own gamma (● available : authR natUR) ** credits gamma (S k)
+    |-- (|==> own gamma (● (Nat.pred available) : authR natUR) **
+              credits gamma k)%I.
+  Proof.
+    intros Hbound.
+    unfold credits.
+    rewrite <- !own_op.
+    apply own_update.
+    apply auth_update, nat_local_update.
+    lia.
+  Qed.
+
+  Lemma counter_return gamma available :
+    own gamma (● available : authR natUR)
+    |-- (|==> own gamma (● (S available) : authR natUR) ** credits gamma 1)%I.
+  Proof.
+    unfold credits.
+    rewrite <- own_op.
+    apply own_update, auth_update_alloc, nat_local_update.
+    change (available + 1 = S available + 0)%nat.
+    lia.
+  Qed.
+
+  Lemma alloc E ns id indices :
+    valid_indices id indices ->
+    ([∗ set] i ∈ indices, pieceRight id i)
+    |-- (|={E}=> Exists gamma,
+        pool ns gamma id indices ** credits gamma (size indices))%I.
+  Proof.
+    intros Hvalid.
+    rewrite <- bi.emp_sep at 1.
+    etrans.
+    {
+      apply bi.sep_mono_l.
+      exact (own_alloc_auth (A := natUR) (size indices) ltac:(done)).
+    }
+    eapply useBupdS.
+    go.
+    rewrite <- fupd_exist.
+    iExists t.
+    unfold pool, credits.
+    rewrite <- fupd_frame_r.
+    go.
+    rewrite <- fupd_frame_l.
+    go.
+    assert (WeaklyObjective (pool_body t id indices)).
+    { unfold pool_body, pieceRight. apply _. }
+    wapply (inv_alloc ns E (pool_body t id indices)).
+    rewrite <- fupd_intro.
+    go.
+    unfold pool_body.
+    rewrite <- bi.later_intro.
+    rewrite bi.sep_exist_r.
+    iExists indices.
+    assert (indices ⊆ indices) by reflexivity.
+    go.
+  Qed.
+
+  Lemma take_body E gamma id indices k :
+    pool_body gamma id indices ** credits gamma (S k)
+    |-- (|={E}=> pool_body gamma id indices ** credits gamma k **
+        (Exists i, [| i ∈ indices |] ** pieceRight id i))%I.
+  Proof.
+    unfold pool_body at 1.
+    go.
+    rename t into free.
+    wapply (observe_2_uncurry_elim [| (S k <= size free)%nat |]
+      (own gamma (● size free : authR natUR)) (credits gamma (S k))).
+    go.
+    assert (Hnonempty : free <> ∅).
+    { intros ->. rewrite size_empty in H. lia. }
+    destruct (set_choose_L free Hnonempty) as [i Hi].
+    wapply (counter_take gamma (size free) k H).
+    go.
+    rewrite <- fupd_intro.
+    iExists i.
+    rewrite (big_sepS_delete _ free i Hi).
+    assert (i ∈ indices) by set_solver.
+    unfold pool_body.
+    rewrite bi.sep_exist_r.
+    iExists (free ∖ {[i]}).
+    assert (free ∖ {[i]} ⊆ indices) by set_solver.
+    rewrite size_difference; last set_solver.
+    rewrite size_singleton.
+    replace (size free - 1)%nat with (Nat.pred (size free)) by lia.
+    go.
+  Qed.
+
+  Lemma return_body E gamma id indices i :
+    valid_indices id indices -> i ∈ indices ->
+    pool_body gamma id indices ** pieceRight id i
+    |-- (|={E}=> pool_body gamma id indices ** credits gamma 1)%I.
+  Proof.
+    intros Hvalid Hi.
+    unfold pool_body at 1.
+    go.
+    rename t into free.
+    destruct (decide (i ∈ free)) as [Hin | Hout].
+    {
+      rewrite (big_sepS_delete _ free i Hin).
+      wapply (pieceRight_exclusive id i (proj1 (Hvalid i Hi))).
+      go.
+    }
+    {
+      wapply (counter_return gamma (size free)).
+      go.
+      rewrite <- fupd_intro.
+      unfold pool_body.
+      rewrite bi.sep_exist_r.
+      iExists ({[i]} ∪ free).
+      assert ({[i]} ∪ free ⊆ indices) by set_solver.
+      rewrite size_union; last set_solver.
+      rewrite size_singleton /=.
+      rewrite big_sepS_insert; last done.
+      go.
+    }
+  Qed.
+
+  (** Both public operations restore the caller's mask: the invariant is never
+      held open while a C++ constructor or destructor runs. *)
+  Lemma take E ns gamma id indices k :
+    ↑ns ⊆ E ->
+    pool ns gamma id indices ** credits gamma (S k)
+    |-- (|={E}=> credits gamma k **
+        (Exists i, [| i ∈ indices |] ** pieceRight id i))%I.
+  Proof.
+    intros Hmask.
+    unfold pool.
+    go.
+    wapply (inv_acc_timeless E ns (pool_body gamma id indices) Hmask).
+    go.
+    wapply (take_body (E ∖ ↑ns) gamma id indices k).
+    go.
+    wapply (bi.wand_elim_l (pool_body gamma id indices)
+      (|={E ∖ ↑ns,E}=> emp)%I).
+    go.
+    rewrite <- fupd_intro.
+    iExists t.
+    go.
+  Qed.
+
+  Lemma put E ns gamma id indices i :
+    ↑ns ⊆ E -> i ∈ indices ->
+    pool ns gamma id indices ** pieceRight id i
+    |-- (|={E}=> credits gamma 1)%I.
+  Proof.
+    intros Hmask Hi.
+    unfold pool.
+    go.
+    wapply (inv_acc_timeless E ns (pool_body gamma id indices) Hmask).
+    go.
+    wapply (return_body (E ∖ ↑ns) gamma id indices i H Hi).
+    go.
+    wapply (bi.wand_elim_l (pool_body gamma id indices)
+      (|={E ∖ ↑ns,E}=> emp)%I).
+    go.
+    rewrite <- fupd_intro.
+    go.
+  Qed.
+
+  Lemma excess_credits E ns gamma id indices :
+    ↑ns ⊆ E ->
+    pool ns gamma id indices ** credits gamma (S (size indices))
+    |-- (|={E}=> False)%I.
+  Proof.
+    intros Hmask.
+    unfold pool.
+    go.
+    wapply (inv_acc_timeless E ns (pool_body gamma id indices) Hmask).
+    go.
+    unfold pool_body.
+    go.
+    rename H into Hsubset.
+    wapply (observe_2_uncurry_elim [| (S (size indices) <= size free)%nat |]
+      (own gamma (● size free : authR natUR))
+      (credits gamma (S (size indices)))).
+    go.
+    exfalso.
+    pose proof (subseteq_size free indices Hsubset).
+    lia.
+  Qed.
+
+  (** Reserving a token and cancelling that reservation preserves the budget.
+      This is not a C++ copy/destruction proof: those operations must establish
+      the separate outstanding-piece protocol described by their specs. *)
+  Lemma reservation_round_trip E ns gamma id indices k :
+    ↑ns ⊆ E ->
+    pool ns gamma id indices ** credits gamma (S k)
+    |-- (|={E}=> credits gamma (S k))%I.
+  Proof.
+    intros Hmask.
+    wapply (take E ns gamma id indices k Hmask).
+    go.
+    wapply (put E ns gamma id indices t Hmask H).
+    go.
+    rewrite <- fupd_intro.
+    replace (S k) with (k + 1)%nat by lia.
+    rewrite credits_add.
+    go.
+  Qed.
+End pool.
+End TokenPool.
diff --git a/rocq-brick-libstdcpp/test/shared_ptr/const_conversion.v b/rocq-brick-libstdcpp/test/shared_ptr/const_conversion.v
new file mode 100644
index 00000000..887daeb1
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/shared_ptr/const_conversion.v
@@ -0,0 +1,49 @@
+(** Check the template flags and complete handle layout against libstdc++.
+    These tests use no shared_ptr method spec and do not open its invariant. *)
+Require Import skylabs.auto.cpp.proof.
+Require Import skylabs.lang.cpp.parser.plugin.cpp2v.
+Require Import skylabs.brick.libstdcpp.shared_ptr.specs.
+
+Set Default Goal Selector "!".
+Import linearity.
+
+#[elaborate]
+cpp.prog source prog cpp:{{
+#include <memory>
+static_assert(sizeof(std::shared_ptr<int>) == 16);
+static_assert(sizeof(std::shared_ptr<const int>) == 16);
+static_assert(sizeof(std::shared_ptr<int[]>) == 16);
+static_assert(sizeof(std::shared_ptr<const int[4]>) == 16);
+static_assert(sizeof(std::shared_ptr<void>) == 16);
+static_assert(sizeof(std::shared_ptr<const void>) == 16);
+}}.
+
+Definition handle_types : list type :=
+  [Tint; Tconst Tint; Tincomplete_array Tint; Tconst (Tarray Tint 4);
+   Tvoid; Tconst Tvoid].
+
+Example handle_layouts_match :
+  forallb (fun ty => bool_decide
+    (type_table_le (types (shared_ptr_const_tu ty)) (types source)))
+    handle_types = true.
+Proof. vm_compute. reflexivity. Qed.
+
+Section with_cpp.
+  Context `{Sigma : cpp_logic} {CU : genv}.
+
+  Example shared_const_roundtrip id i Rpiece owned (handle : ptr) :
+    handle |-> SharedPtrR (Tconst Tint) 1$m id i Rpiece owned
+    |-- wp_make_const source handle (Tnamed (SP_name (Tconst Tint)))
+      (wp_make_mutable source handle (Tnamed (SP_name (Tconst Tint)))
+        (handle |-> SharedPtrR (Tconst Tint) 1$m id i Rpiece owned)).
+  Proof. go. Qed.
+
+  Example null_array_const_roundtrip (handle : ptr) :
+    handle |-> NullSharedPtrR (Tincomplete_array Tint) 1$m
+    |-- wp_make_const source handle
+      (Tnamed (SP_name (Tincomplete_array Tint)))
+      (wp_make_mutable source handle
+        (Tnamed (SP_name (Tincomplete_array Tint)))
+        (handle |-> NullSharedPtrR (Tincomplete_array Tint) 1$m)).
+  Proof. go. Qed.
+End with_cpp.