From 4fc11fe6cab548e5cbde4686d7324e0bd552bb9a Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Sun, 18 Jan 2026 13:51:04 -0500 Subject: [PATCH 01/31] moved specs from fv-workspace --- _CoqProject | 26 -- rocq-brick-libstdcpp/proof/dune | 1 + rocq-brick-libstdcpp/proof/dune.inc | 18 ++ .../proof/shared_ptr/inc_shared_ptr.cpp | 1 + rocq-brick-libstdcpp/proof/shared_ptr/specs.v | 296 ++++++++++++++++++ .../proof/shared_ptr/test.cpp | 15 + rocq-brick-libstdcpp/proof/shared_ptr/test.v | 194 ++++++++++++ 7 files changed, 525 insertions(+), 26 deletions(-) delete mode 100644 _CoqProject create mode 100644 rocq-brick-libstdcpp/proof/shared_ptr/inc_shared_ptr.cpp create mode 100644 rocq-brick-libstdcpp/proof/shared_ptr/specs.v create mode 100644 rocq-brick-libstdcpp/proof/shared_ptr/test.cpp create mode 100644 rocq-brick-libstdcpp/proof/shared_ptr/test.v diff --git a/_CoqProject b/_CoqProject deleted file mode 100644 index 3a9d7b64..00000000 --- a/_CoqProject +++ /dev/null @@ -1,26 +0,0 @@ -# AUTO-GENERATED CONTENT, EDIT `gen-_CoqProject-dune.sh` INSTEAD - -# Avoid warnings about entries in this _CoqProject --arg -w -arg -cannot-open-path -# Warning settings from `dune` project files --arg -w -arg -notation-overridden --arg -w -arg -custom-entry-overridden --arg -w -arg -redundant-canonical-projection --arg -w -arg -ambiguous-paths --arg -w -arg -notation-incompatible-prefix -# Turn warning on hints into error: --arg -w -arg +deprecated-hint-without-locality --arg -w -arg +deprecated-instance-without-locality --arg -w -arg +deprecated-tacopt-without-locality --arg -w -arg +future-coercion-class-field --arg -w -arg +unknown-option --arg -w -arg +sl-transparent-constants - -# Plugin directory. --I _build/install/default/lib - -# Specified logical paths for directories (for .v and .vo files). --Q _build/default/rocq-brick-libstdcpp/proof/ skylabs.brick.libstdcpp --Q rocq-brick-libstdcpp/proof/ skylabs.brick.libstdcpp --Q _build/default/rocq-brick-libstdcpp/test/ skylabs.brick.libstdcpp.test --Q rocq-brick-libstdcpp/test/ skylabs.brick.libstdcpp.test diff --git a/rocq-brick-libstdcpp/proof/dune b/rocq-brick-libstdcpp/proof/dune index 486a0081..7d9779a2 100644 --- a/rocq-brick-libstdcpp/proof/dune +++ b/rocq-brick-libstdcpp/proof/dune @@ -21,6 +21,7 @@ skylabs.iris.extra Equations Equations.Prop Equations.Type skylabs.lang.cpp + skylabs.cpp.stdlib skylabs.ltac2.logger skylabs.auto.core ; diff --git a/rocq-brick-libstdcpp/proof/dune.inc b/rocq-brick-libstdcpp/proof/dune.inc index dd493569..708b0810 100644 --- a/rocq-brick-libstdcpp/proof/dune.inc +++ b/rocq-brick-libstdcpp/proof/dune.inc @@ -80,3 +80,21 @@ (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_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)) +) 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..50cb3901 --- /dev/null +++ b/rocq-brick-libstdcpp/proof/shared_ptr/inc_shared_ptr.cpp @@ -0,0 +1 @@ +#include 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..e8d9905d --- /dev/null +++ b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v @@ -0,0 +1,296 @@ +(** Specs of shared_ptr. +We do not cover interaction with weak_ptr. +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], chosen by the implementation, would typically be 2^64, to prevent overflow of the reference counter. + +To ensure the destructor proof goes through, the init ctor requires [ [∗ list] ctid ∈ allPieceIds, Rpiece ctid) |-- anyR ty 1]. This becomes a part of [SharedPtrR]. +If anyR does not make sense for Tnamed, then it should be replaced with [wp (default_ctor of Tnamed) emp]. + +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. +Because BRiCk only supports SC atomics, the proof only works as if the stdlib implementation used SC atomics or had sufficient barriers (the actual defn of SharedPtrR will be different in that case due to limitations on invariants in weak memory reasoning). + +- 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 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. + +- These specs in this file allow you to change the ownership split protocol (between the various shared_ptr objects protecting the same payload object ptr) later on (see lemma [redistributePayloadOwnership]), as long as the caller can cough up all pieces and objects associated with the payload (see [allPiecesAndObjs]). +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.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.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 Import iris.algebra.excl. + + +Record CtrlBlockId : Set := + { + pieceRightLocs: list gname; (* each stores a unit. N -> gname may be tricky for constructor proof *) + dataLoc: ptr; + }. + +#[local] Open Scope N_scope. +Definition maxContention : positive. Proof. Admitted. + +Definition ctrOffset: offset. Proof. Admitted. +(** offset of the field storing ownedPtr in any shared_ptr object *) +Definition ownedPtrOffset: offset. Proof. Admitted. +(** offset of the field storing ctrlBlock pointer in any shared_ptr object *) +Definition ctrlBlockPtrOffset: offset. Proof. Admitted. + +Lemma maxContentionLb : 2^32 <= Npos maxContention. Proof. Admitted. +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). + +Section specs. + Context `{Σ : cpp_logic, MOD:inc_shared_ptr_cpp.module ⊧ σ}. + #[local] Existing Instance br.ghost.excl_inG. + + + 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. + + + Definition sptrInv (id: CtrlBlockId) (Rpiece : nat -> Rep) (ownedPtr:ptr) (pieceOut : nat ->bool) : mpred := + let ctrVal := countLN pieceOut allPieceIds in + (dataLoc id),, ctrOffset |-> atomic.R "long" 1 (Z.of_N ctrVal) + ** (if (bool_decide (ctrVal = 0)) + then emp + else ownedPtr |-> alloc.tokenR ty 1%Qp + ** ([∗ list] pieceid ∈ allPieceIds, + if pieceOut pieceid then pieceRight id pieceid else ownedPtr |-> Rpiece pieceid)). + + (** Currently, we assume the control block is just an atomic counter. + In reality, it is probably a struct. so move the atomicR to some defn ctrlBlockR *) + Definition SharedPtrR (id: CtrlBlockId) (Rpiece : nat -> Rep) (ownedPtr:ptr) : Rep := + structR ("std::shared_ptr".<>) 1 + ** [| ([∗ list] pieceid ∈ allPieceIds, Rpiece pieceid) |-- anyR ty 1 |] + ** ownedPtrOffset |-> primR (Tptr ty) 1 (Vptr ownedPtr) + ** ctrlBlockPtrOffset |-> primR (Tptr (Tnamed ("std::atomic".<>))) 1 (Vptr (dataLoc id)) + ** [| ownedPtr<>nullptr |] (* use NullSharedPtr otherwise *) + ** [| lengthN (pieceRightLocs id) = Npos maxContention |] + ** pureR (inv nroot (Exists (pieceOut : nat ->bool), sptrInv id Rpiece ownedPtr pieceOut)). + + Definition NullSharedPtrR : Rep := + structR ("std::shared_ptr".<>) 1 + ** ownedPtrOffset |-> primR (Tptr ty) 1 (Vptr nullptr) + ** ctrlBlockPtrOffset |-> primR (Tptr (Tnamed ("std::atomic".<>))) 1 (Vptr nullptr). + + + Definition init_ctor := + specify {| info_name := (Nscoped ("std::shared_ptr".<>) (Nctor [Tptr ty])).<> + ; info_type := tCtor ("std::shared_ptr".<>) [Tptr ty] |} (fun (this:ptr) => + \arg{p:ptr} "ownedPtr" (Vptr p) + \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 p |-> alloc.tokenR ty 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 [|([∗ list] pieceid ∈ allPieceIds, Rpiece pieceid) + |-- anyR ty 1 |] + (* ^^ if anyR is not meaningful for non-scalar types, + replace this with wp of default destructor *) + \post Exists (ctrlBlockId: CtrlBlockId), + this |-> SharedPtrR ctrlBlockId 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".<>). + Definition move_ctor := + specify.template.ctor spty [Trv_ref ((Tnamed spty))] $ + \this this + \arg{other:ptr} "other" (Vptr other) + \pre{ctrlBlockId ownedPtr Rpiece} other |-> SharedPtrR ctrlBlockId Rpiece ownedPtr + \post other |-> NullSharedPtrR + ** this |-> SharedPtrR ctrlBlockId 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} + this |-> (match null as b return (if b then unit else prod CtrlBlockId nat) -> Rep with + | false => fun sid=> + SharedPtrR sid.1 Rpiece p + ** Rpiece sid.2 + | true => fun sid=> NullSharedPtrR + 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) + \pre{id pieceid p Rpiece} other |-> SharedPtrR id Rpiece p + \pre pieceRight id pieceid (* this will be returned by destructor *) + \pre [| N.of_nat pieceid < Npos maxContention|]%N + \post + p|->Rpiece pieceid ** this |-> SharedPtrR id Rpiece p + ** other |-> SharedPtrR id Rpiece p. + + Definition SpecFor_copy_ctor := RegisterSpec copy_ctor. + #[global] Existing Instance SpecFor_copy_ctor. + + (** Copy-ctor from null: produces another null shared_ptr. + No token is required. TODO: unify this spec with the spec above, using dependent types, as done in the destructor spec *) + Definition copy_ctor_null := + specify.template.ctor spty [Tref (Tconst (Tnamed spty))] $ + \this this + \arg{other:ptr} "other" (Vptr other) + \pre other |-> NullSharedPtrR + \post this |-> NullSharedPtrR + ** other |-> NullSharedPtrR. + + + Definition SP_acc (mid: Z) := ("std::__shared_ptr_access" .<< + Atype ty, + Avalue (Eint 2 "enum __gnu_cxx::_Lock_policy"), + Avalue (Eint mid "bool"), + Avalue (Eint 0 "bool") >>)%cpp_name. + + Definition SP_impl := ("std::__shared_ptr" .<< + Atype ty, + Avalue (Eint 2 "enum __gnu_cxx::_Lock_policy") >>)%cpp_name. + + (** Reconstruct the most-derived object pointer from the base-subobject "this". *) + Definition upcast_offset (mid: Z) : offset := + (o_derived σ (SP_acc mid) SP_impl ,, o_derived σ SP_impl spty). + + Definition deref := + specify.template.op (SP_acc 0) OOStar function_qualifiers.Nc (Tref ty) [] $ + \this this + \prepost{id p Rpiece} this |-> (upcast_offset 0) |-> SharedPtrR id 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 0) OOArrow function_qualifiers.Nc (Tptr ty) [] $ + \this this + \prepost{id p Rpiece} this |-> (upcast_offset 0) |-> SharedPtrR id 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 id (p:ptr) op Rpiece + : Observe (type_ptr (Tnamed ("std::shared_ptr".<>)) p) (p|->SharedPtrR id Rpiece op):= _. + + Definition observeSharedTypeF q t Rpiece op:= @observe_fwd _ _ _ (sharedR_typeptr_observe q t Rpiece op). + + Definition allPiecesAndObjs Rpiece id (ownedPtr: ptr) (pieceOut: nat->bool) : Rep := + ([∗ list] pieceid ∈ allPieceIds, + if pieceOut pieceid + then pureR (ownedPtr |-> Rpiece pieceid) + ** pureR (Exists (base:ptr), base |->SharedPtrR id Rpiece ownedPtr) + else pureR (pieceRight id pieceid)). + + Lemma redistributePayloadOwnership {Rpieceold Rpiecenew: nat -> Rep} (pieceOut : nat -> bool) id ownedPtr: + allPiecesAndObjs Rpieceold id ownedPtr pieceOut + |-- |={⊤}=> allPiecesAndObjs Rpiecenew id ownedPtr pieceOut. + Proof. Admitted. + + End tty. + + Definition init_ctor_arr ety := + specify {| info_name := (Nscoped ("std::shared_ptr".<>) (Nctor [Tptr ety])).<> + ; info_type := tCtor ("std::shared_ptr".<>) [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 p |-> alloc.tokenR ty 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 [|([∗ list] pieceid ∈ allPieceIds, Rpiece pieceid) + |-- anyR ty 1 |] + (* ^^ if anyR is not meaningful for non-scalar types, + replace this with wp of default destructor *) + \post Exists (ctrlBlockId: CtrlBlockId), + this |-> SharedPtrR (Tincomplete_array ety) ctrlBlockId 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{id p Rpiece} this |-> (upcast_offset (Tincomplete_array ety) 1) |-> SharedPtrR (Tincomplete_array ety ) id Rpiece p + \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_null + deref arrow init_ctor_arr subscript + : sl_opacity. + +End specs. +#[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..ea5015b5 --- /dev/null +++ b/rocq-brick-libstdcpp/proof/shared_ptr/test.cpp @@ -0,0 +1,15 @@ +#include + +std::shared_ptr testshared1() { + auto x= std::shared_ptr(new int); + *x=1; + return x; + } + +std::shared_ptr testsharedarr() { + auto x= std::shared_ptr(new int[2]); + x[0]=1; + x[1]=2; + return x; + } + 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..5a6b68cd --- /dev/null +++ b/rocq-brick-libstdcpp/proof/shared_ptr/test.v @@ -0,0 +1,194 @@ +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. + + +(* 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. + rewrite <- big_sepL_emp with (l:=(list_difference l [x])). + apply big_opL_proper. + intros ? id Hl. + case_decide;[ | reflexivity]. + subst. + apply elem_of_list_lookup_2 in Hl. + apply elem_of_list_difference in Hl. + forward_reason. + apply False_rect. + simpl in *. + set_solver. +Qed. + +Section proofs. + Opaque SharedPtrR. + Context `{Σ : cpp_logic, MOD:test_cpp.module ⊧ σ} + {hf:fracG () _Σ}. + + + cpp.spec "testshared1()" as testshared1spec with ( + \pre emp + \post{p:ptr}[Vptr p] Exists payload sid, + p |-> SharedPtrR "int" sid (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 elem_of_list_lookup_2 in Hl. + autorewrite with equiv in Hl. + resolveDecide lia. + reflexivity. + } + autorewrite with equiv. + reflexivity. + Qed. + + Opaque NullSharedPtrR. + #[global] Instance lll: LearnEq4 SharedPtrR := + ltac:(solve_learnable). + +Set Default Goal Selector "!". + Lemma prf2: verify[module] 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. + rewrite <- _at_big_sepL. + unfold allButFirstPieceId. + rewrite allButFirstEmp. go. + provePure. + { + unfold allPieceIds. + rewrite -> seqprefix with (prelen:=1%nat) by lia. + simpl. + rewrite allButFirstEmp. go. + } + go. + normalize_ptrs. + go. + normalize_ptrs. + repeat iExists _. + eagerUnifyC. + go. + iExists true. + go. + repeat iExists _. + go. + + Admitted. + + (* dummy spec: needs fix *) + cpp.spec "testsharedarr()" as testsharedarrspec with ( + \pre emp + \post{p:ptr}[Vptr p] Exists payload sid, + p |-> SharedPtrR "int[]" sid (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: verify[module] testsharedarrspec. + Proof using MOD. + verify_spec. + go. {admit. } + let r := sharedPtrRpieceFromPost in + set (Rpiece := r). + iExists Rpiece. + go. + iExists 2%N. + simpl. + eagerUnifyU. + go. + normalize_ptrs. + eagerUnifyU. + go. + rewrite <- _at_big_sepL. + unfold allButFirstPieceId. + rewrite allButFirstEmp. go. + provePure. + { + unfold Rpiece. + unfold allPieceIds. + rewrite -> seqprefix with (prelen:=1%nat) by lia. + simpl. + rewrite allButFirstEmp. + go. + } + go. + normalize_ptrs. + go. + normalize_ptrs. + go. + simpl. + unfold replicateN. + simpl. + repeat rewrite arrayR_cons. + go. + normalize_ptrs. + go. + normalize_ptrs. + go. + (* TODO: proof needs rework after alloc.tokenR transition. *) + repeat rewrite arrayR_cons. + go. + normalize_ptrs. + go. + repeat rewrite arrayR_nil. + go. + + Admitted. +End proofs. From 430b828915c270281ad2f695f3e9642601feb971 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Sun, 18 Jan 2026 21:27:59 -0500 Subject: [PATCH 02/31] fixed test proofs of shared_ptr --- rocq-brick-libstdcpp/proof/shared_ptr/test.v | 23 ++++++++++++++------ 1 file changed, 16 insertions(+), 7 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/test.v b/rocq-brick-libstdcpp/proof/shared_ptr/test.v index 5a6b68cd..430b17d1 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/test.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/test.v @@ -125,10 +125,11 @@ Set Default Goal Selector "!". go. iExists true. go. - repeat iExists _. + iExists nullptr. + iExists tt. + iExists (fun _ => emp). go. - - Admitted. + Qed. (* dummy spec: needs fix *) cpp.spec "testsharedarr()" as testsharedarrspec with ( @@ -141,10 +142,10 @@ Set Default Goal Selector "!". ). - Lemma prf3: verify[module] testsharedarrspec. + Lemma prf3: (SIZE_MAX = 2^64)%N -> verify[module] testsharedarrspec. Proof using MOD. verify_spec. - go. {admit. } + go;[lia|]. let r := sharedPtrRpieceFromPost in set (Rpiece := r). iExists Rpiece. @@ -154,6 +155,9 @@ Set Default Goal Selector "!". eagerUnifyU. go. normalize_ptrs. + ring_simplify_goal_Z. + normalize_ptrs. + go. eagerUnifyU. go. rewrite <- _at_big_sepL. @@ -182,6 +186,12 @@ Set Default Goal Selector "!". go. normalize_ptrs. go. + iExists true. + go. + iExists nullptr. + iExists tt. + iExists (fun _ => emp). + go. (* TODO: proof needs rework after alloc.tokenR transition. *) repeat rewrite arrayR_cons. go. @@ -189,6 +199,5 @@ Set Default Goal Selector "!". go. repeat rewrite arrayR_nil. go. - - Admitted. + Qed. End proofs. From c8cbf2f870763bc1241266a26cf201da9dddb1e8 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Mon, 27 Jul 2026 12:08:03 -0400 Subject: [PATCH 03/31] porting shared_ptr specs to latest upstream abiut a month ago --- rocq-brick-libstdcpp/proof/shared_ptr/specs.v | 8 ++++---- rocq-brick-libstdcpp/proof/shared_ptr/test.v | 1 + 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v index e8d9905d..1b144fc6 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v @@ -26,11 +26,11 @@ A common pattern where this can be useful is when the thread that calls new need *) 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.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.cpp.stdlib.algorithms.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. diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/test.v b/rocq-brick-libstdcpp/proof/shared_ptr/test.v index 430b17d1..61ea7b10 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/test.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/test.v @@ -53,6 +53,7 @@ Proof using. Qed. Section proofs. + #[local] Set Warnings "-sl-transparent-constants". Opaque SharedPtrR. Context `{Σ : cpp_logic, MOD:test_cpp.module ⊧ σ} {hf:fracG () _Σ}. From 0b559d7b862e4349c41ed59eee9a69d5420a7420 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Sat, 5 Sep 2026 21:33:26 -0400 Subject: [PATCH 04/31] Require nonnull pointers in memcpy specification Empty array slices hold at nullptr. Explicitly exclude null source and destination pointers even for zero-length calls, matching the C++23 library contract. Reported as SkyLabsAI/brick-libcpp#170. Checked the spec through Proof General and Dune. --- rocq-brick-libstdcpp/proof/cstring/spec.v | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/rocq-brick-libstdcpp/proof/cstring/spec.v b/rocq-brick-libstdcpp/proof/cstring/spec.v index f977cad8..1303d4f8 100644 --- a/rocq-brick-libstdcpp/proof/cstring/spec.v +++ b/rocq-brick-libstdcpp/proof/cstring/spec.v @@ -3,6 +3,8 @@ * This software is distributed under the terms of the BedRock Open-Source License. * See the LICENSE-BedRock file in the repository root for details. *) +Set Default Goal Selector "!". + Require Import skylabs.auto.cpp.specs. Require Import skylabs.auto.cpp.prelude.proof. @@ -182,6 +184,8 @@ Context `{Σ : cpp_logic, module ⊧ σ}. (\arg{dest_p} "__dest" (Vptr dest_p) \arg{src_p} "__src" (Vptr src_p) \arg{z} "__n" (Vint z) + (* Empty slices admit nullptr; the C++23 library contract does not. *) + \pre [| dest_p <> nullptr /\ src_p <> nullptr |] \prepost{q bytes} src_p |-> array_sliceR Tuchar 0 z (fun b : Z => ucharR q b) bytes \pre{l} dest_p |-> array_sliceR Tuchar 0 z (fun _ : unit => anyR Tuchar 1$m) l (*(replicateZ z tt)*) \post[Vptr dest_p] dest_p |-> array_sliceR Tuchar 0 z (fun b : Z => ucharR 1$m b) bytes). From 510e531b83507712a2ff7c711edab1d1718b4cdb Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Mon, 7 Sep 2026 00:10:49 -0400 Subject: [PATCH 05/31] Port local shared_ptr specs to upstream source and atomic namespaces Use the generated source translation unit and open std.atomic after its upstream namespace move. Keep the existing contracts and representations unchanged. The specs file checks to EOF in Emacs and compiles in the composed workspace build. --- rocq-brick-libstdcpp/proof/shared_ptr/specs.v | 5 ++++- rocq-brick-libstdcpp/proof/shared_ptr/test.v | 2 +- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v index 1b144fc6..f6147436 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v @@ -26,6 +26,7 @@ A common pattern where this can be useful is when the thread that calls new need *) Require Import skylabs.auto.cpp.proof. +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. @@ -38,6 +39,8 @@ Require Import skylabs.cpp.spec.concepts.experimental. Require Import skylabs.brick.libstdcpp.shared_ptr.inc_shared_ptr_cpp. Require Import iris.algebra.excl. +NES.Open std.atomic. + Record CtrlBlockId : Set := { @@ -63,7 +66,7 @@ Definition countLN {A : Type} (f : A -> bool) (l : list A) : N := lengthN (filter f l). Section specs. - Context `{Σ : cpp_logic, MOD:inc_shared_ptr_cpp.module ⊧ σ}. + Context `{Σ : cpp_logic, MOD:inc_shared_ptr_cpp.source ⊧ σ}. #[local] Existing Instance br.ghost.excl_inG. diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/test.v b/rocq-brick-libstdcpp/proof/shared_ptr/test.v index 61ea7b10..8cd97e9c 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/test.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/test.v @@ -55,7 +55,7 @@ Qed. Section proofs. #[local] Set Warnings "-sl-transparent-constants". Opaque SharedPtrR. - Context `{Σ : cpp_logic, MOD:test_cpp.module ⊧ σ} + Context `{Σ : cpp_logic, MOD:test_cpp.source ⊧ σ} {hf:fracG () _Σ}. From f0da353006611df1e535740d44a6bbbc9e7350e7 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Tue, 22 Sep 2026 11:53:00 -0400 Subject: [PATCH 06/31] Fix shared_ptr destructor payload address In the non-null branch, require the outstanding Rpiece at the pointee p rather than at the shared_ptr handle this. Preserve the null branch and the returned pieceRight token. Checked shared_ptr/specs.v to EOF through Emacs/Proof General and rebuilt monad/monadproofs/proofs/all.vo in the composed workspace. No client proof edits, new axioms, or admitted items. --- rocq-brick-libstdcpp/proof/shared_ptr/specs.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v index f6147436..ce348e5c 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v @@ -154,11 +154,12 @@ Section specs. specify.template.dtor spty $ \this this \pre{(null:bool) (p:ptr) (sid: if null then unit else prod CtrlBlockId nat) Rpiece} - this |-> (match null as b return (if b then unit else prod CtrlBlockId nat) -> Rep with + (* 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=> - SharedPtrR sid.1 Rpiece p - ** Rpiece sid.2 - | true => fun sid=> NullSharedPtrR + this |-> SharedPtrR sid.1 Rpiece p + ** p |-> Rpiece sid.2 + | true => fun sid=> this |-> NullSharedPtrR end) sid \post (match null as b return (if b then unit else prod CtrlBlockId nat) -> mpred with From dbc2fdf78835f85692c056040f9e4be155703d7c Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Tue, 22 Sep 2026 21:22:53 -0400 Subject: [PATCH 07/31] Allow fractional ownership of shared_ptr source handles Fraction the handle fields and structR only; keep acquisition tokens and payload pieces separate. Copy and accessors preserve arbitrary source fractions, while construction returns full ownership and move/destruction require it. Prove the fraction instances and a copy/destroy client regression under the existing assumed library specs. Port both existing examples to the current automation. Interactive checks passed for specs.v, both existing examples, the new regression, and Monad exec_specs.v. Dune built both example files. The central all.vo rebuild was interrupted before completion because a separately reviewed destruction-interface revision will change the same dependency; the final combined revision must pass that gate. No new axioms or admits. --- .../proof/shared_ptr/fractional_copy.v | 50 +++++++++++++ rocq-brick-libstdcpp/proof/shared_ptr/specs.v | 72 +++++++++++-------- rocq-brick-libstdcpp/proof/shared_ptr/test.v | 20 +++--- 3 files changed, 102 insertions(+), 40 deletions(-) create mode 100644 rocq-brick-libstdcpp/proof/shared_ptr/fractional_copy.v 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..4eaaeb7a --- /dev/null +++ b/rocq-brick-libstdcpp/proof/shared_ptr/fractional_copy.v @@ -0,0 +1,50 @@ +(** 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.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 +void copy_then_destroy(std::shared_ptr 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 : LearnEq5 SharedPtrR := + ltac:(solve_learnable). + + cpp.spec "copy_then_destroy(const std::shared_ptr&)" + from source as copy_then_destroy_spec with ( + \arg{other : ptr} "source" (Vref other) + \prepost{q id p Rpiece} + other |-> SharedPtrR "int" q id 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. + verify_spec. + go. + iExists pieceid. + go. + iExists false, p, (id, pieceid), Rpiece. + go. + Qed. +End with_cpp. diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v index ce348e5c..d071f316 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v @@ -94,19 +94,33 @@ Section specs. (** Currently, we assume the control block is just an atomic counter. In reality, it is probably a struct. so move the atomicR to some defn ctrlBlockR *) - Definition SharedPtrR (id: CtrlBlockId) (Rpiece : nat -> Rep) (ownedPtr:ptr) : Rep := - structR ("std::shared_ptr".<>) 1 + (* [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) (Rpiece : nat -> Rep) (ownedPtr:ptr) : Rep := + structR ("std::shared_ptr".<>) q ** [| ([∗ list] pieceid ∈ allPieceIds, Rpiece pieceid) |-- anyR ty 1 |] - ** ownedPtrOffset |-> primR (Tptr ty) 1 (Vptr ownedPtr) - ** ctrlBlockPtrOffset |-> primR (Tptr (Tnamed ("std::atomic".<>))) 1 (Vptr (dataLoc id)) + ** ownedPtrOffset |-> primR (Tptr ty) q (Vptr ownedPtr) + ** ctrlBlockPtrOffset |-> primR (Tptr (Tnamed ("std::atomic".<>))) q (Vptr (dataLoc id)) ** [| ownedPtr<>nullptr |] (* use NullSharedPtr otherwise *) ** [| lengthN (pieceRightLocs id) = Npos maxContention |] ** pureR (inv nroot (Exists (pieceOut : nat ->bool), sptrInv id Rpiece ownedPtr pieceOut)). - Definition NullSharedPtrR : Rep := - structR ("std::shared_ptr".<>) 1 - ** ownedPtrOffset |-> primR (Tptr ty) 1 (Vptr nullptr) - ** ctrlBlockPtrOffset |-> primR (Tptr (Tnamed ("std::atomic".<>))) 1 (Vptr nullptr). + Definition NullSharedPtrR (q : cQp.t) : Rep := + structR ("std::shared_ptr".<>) q + ** ownedPtrOffset |-> primR (Tptr ty) q (Vptr nullptr) + ** ctrlBlockPtrOffset |-> primR (Tptr (Tnamed ("std::atomic".<>))) q (Vptr nullptr). + + #[global] Instance SharedPtrR_fractional id Rpiece p : + CFractional (fun q => SharedPtrR q id Rpiece p) := _. + #[global] Instance SharedPtrR_as_fractional q id Rpiece p : + AsCFractional (SharedPtrR q id Rpiece p) + (fun q => SharedPtrR q id 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. Definition init_ctor := @@ -130,7 +144,7 @@ Section specs. (* ^^ if anyR is not meaningful for non-scalar types, replace this with wp of default destructor *) \post Exists (ctrlBlockId: CtrlBlockId), - this |-> SharedPtrR ctrlBlockId Rpiece p + this |-> SharedPtrR 1$m ctrlBlockId 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 *) ). @@ -143,9 +157,9 @@ Section specs. specify.template.ctor spty [Trv_ref ((Tnamed spty))] $ \this this \arg{other:ptr} "other" (Vptr other) - \pre{ctrlBlockId ownedPtr Rpiece} other |-> SharedPtrR ctrlBlockId Rpiece ownedPtr - \post other |-> NullSharedPtrR - ** this |-> SharedPtrR ctrlBlockId Rpiece ownedPtr. + \pre{ctrlBlockId ownedPtr Rpiece} other |-> SharedPtrR 1$m ctrlBlockId Rpiece ownedPtr + \post other |-> NullSharedPtrR 1$m + ** this |-> SharedPtrR 1$m ctrlBlockId Rpiece ownedPtr. Definition SpecFor_move_ctor := RegisterSpec move_ctor. #[global] Existing Instance SpecFor_move_ctor. @@ -157,9 +171,9 @@ Section specs. (* 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 sid.1 Rpiece p + this |-> SharedPtrR 1$m sid.1 Rpiece p ** p |-> Rpiece sid.2 - | true => fun sid=> this |-> NullSharedPtrR + | 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 @@ -175,12 +189,11 @@ Section specs. specify.template.ctor spty [Tref (Tconst (Tnamed spty))] $ \this this \arg{other:ptr} "other" (Vptr other) - \pre{id pieceid p Rpiece} other |-> SharedPtrR id Rpiece p - \pre pieceRight id pieceid (* this will be returned by destructor *) + \prepost{q id p Rpiece} other |-> SharedPtrR q id 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 id Rpiece p - ** other |-> SharedPtrR id Rpiece p. + p|->Rpiece pieceid ** this |-> SharedPtrR 1$m id Rpiece p. Definition SpecFor_copy_ctor := RegisterSpec copy_ctor. #[global] Existing Instance SpecFor_copy_ctor. @@ -191,9 +204,8 @@ Section specs. specify.template.ctor spty [Tref (Tconst (Tnamed spty))] $ \this this \arg{other:ptr} "other" (Vptr other) - \pre other |-> NullSharedPtrR - \post this |-> NullSharedPtrR - ** other |-> NullSharedPtrR. + \prepost{q} other |-> NullSharedPtrR q + \post this |-> NullSharedPtrR 1$m. Definition SP_acc (mid: Z) := ("std::__shared_ptr_access" .<< @@ -213,7 +225,7 @@ Section specs. Definition deref := specify.template.op (SP_acc 0) OOStar function_qualifiers.Nc (Tref ty) [] $ \this this - \prepost{id p Rpiece} this |-> (upcast_offset 0) |-> SharedPtrR id Rpiece p + \prepost{q id p Rpiece} this |-> (upcast_offset 0) |-> SharedPtrR q id Rpiece p \post[Vref p] emp. Definition SpecFor_deref := RegisterSpec deref. @@ -223,23 +235,23 @@ Section specs. Definition arrow := specify.template.op (SP_acc 0) OOArrow function_qualifiers.Nc (Tptr ty) [] $ \this this - \prepost{id p Rpiece} this |-> (upcast_offset 0) |-> SharedPtrR id Rpiece p + \prepost{q id p Rpiece} this |-> (upcast_offset 0) |-> SharedPtrR q id 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 id (p:ptr) op Rpiece - : Observe (type_ptr (Tnamed ("std::shared_ptr".<>)) p) (p|->SharedPtrR id Rpiece op):= _. + #[global] Instance sharedR_typeptr_observe q id (p:ptr) op Rpiece + : Observe (type_ptr (Tnamed ("std::shared_ptr".<>)) p) (p|->SharedPtrR q id Rpiece op):= _. - Definition observeSharedTypeF q t Rpiece op:= @observe_fwd _ _ _ (sharedR_typeptr_observe q t Rpiece op). + Definition observeSharedTypeF q id t Rpiece op:= @observe_fwd _ _ _ (sharedR_typeptr_observe q id t Rpiece op). Definition allPiecesAndObjs Rpiece id (ownedPtr: ptr) (pieceOut: nat->bool) : Rep := ([∗ list] pieceid ∈ allPieceIds, if pieceOut pieceid then pureR (ownedPtr |-> Rpiece pieceid) - ** pureR (Exists (base:ptr), base |->SharedPtrR id Rpiece ownedPtr) + ** pureR (Exists (base:ptr), base |->SharedPtrR 1$m id Rpiece ownedPtr) else pureR (pieceRight id pieceid)). Lemma redistributePayloadOwnership {Rpieceold Rpiecenew: nat -> Rep} (pieceOut : nat -> bool) id ownedPtr: @@ -265,7 +277,7 @@ Section specs. (* ^^ if anyR is not meaningful for non-scalar types, replace this with wp of default destructor *) \post Exists (ctrlBlockId: CtrlBlockId), - this |-> SharedPtrR (Tincomplete_array ety) ctrlBlockId Rpiece p + this |-> SharedPtrR (Tincomplete_array ety) 1$m ctrlBlockId 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 *) ). @@ -277,7 +289,7 @@ Section specs. 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{id p Rpiece} this |-> (upcast_offset (Tincomplete_array ety) 1) |-> SharedPtrR (Tincomplete_array ety ) id Rpiece p + \prepost{q id p Rpiece} this |-> (upcast_offset (Tincomplete_array ety) 1) |-> SharedPtrR (Tincomplete_array ety ) q id Rpiece p \post[Vref (p.[ety ! index])] emp. Definition SpecFor_subscript := RegisterSpec subscript. @@ -295,6 +307,6 @@ Ltac sharedPtrRpieceFromPost := match goal with H: context[@PostCondition ?a ?b ?c ?d] |- _ => match c with - | context[SharedPtrR _ _ ?rp _ ] => constr:(rp) + | context[SharedPtrR _ _ _ ?rp _ ] => constr:(rp) end end. diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/test.v b/rocq-brick-libstdcpp/proof/shared_ptr/test.v index 8cd97e9c..c128fff3 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/test.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/test.v @@ -39,13 +39,14 @@ Proof using. assert (f ** (emp)%I ≡ f) as Heq by (apply right_id; eauto with typeclass_instances). rewrite <- Heq at 1. f_equiv. - rewrite <- big_sepL_emp with (l:=(list_difference l [x])). + 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 elem_of_list_lookup_2 in Hl. - apply elem_of_list_difference in Hl. + apply list_elem_of_lookup_2 in Hl. + apply list_elem_of_difference in Hl. forward_reason. apply False_rect. simpl in *. @@ -62,7 +63,7 @@ Section proofs. cpp.spec "testshared1()" as testshared1spec with ( \pre emp \post{p:ptr}[Vptr p] Exists payload sid, - p |-> SharedPtrR "int" sid (fun ctid => if bool_decide (ctid=0%nat) then anyR "int" 1 else emp) payload + p |-> SharedPtrR "int" 1$m sid (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) @@ -78,7 +79,7 @@ Section proofs. Proof using. erewrite big_opL_proper with (g := fun _ _=> emp). 2:{ intros ? ? Hl. - apply elem_of_list_lookup_2 in Hl. + apply list_elem_of_lookup_2 in Hl. autorewrite with equiv in Hl. resolveDecide lia. reflexivity. @@ -88,11 +89,11 @@ Section proofs. Qed. Opaque NullSharedPtrR. - #[global] Instance lll: LearnEq4 SharedPtrR := + #[global] Instance lll: LearnEq5 SharedPtrR := ltac:(solve_learnable). Set Default Goal Selector "!". - Lemma prf2: verify[module] testshared1spec. + Lemma prf2: verify[source] testshared1spec. Proof using MOD. verify_spec. pose proof maxContentionLb. @@ -136,14 +137,14 @@ Set Default Goal Selector "!". cpp.spec "testsharedarr()" as testsharedarrspec with ( \pre emp \post{p:ptr}[Vptr p] Exists payload sid, - p |-> SharedPtrR "int[]" sid (fun ctid => if bool_decide (ctid=0%nat) then anyR "int[2]" 1 else emp) payload + p |-> SharedPtrR "int[]" 1$m sid (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[module] testsharedarrspec. + Lemma prf3: (SIZE_MAX = 2^64)%N -> verify[source] testsharedarrspec. Proof using MOD. verify_spec. go;[lia|]. @@ -151,7 +152,6 @@ Set Default Goal Selector "!". set (Rpiece := r). iExists Rpiece. go. - iExists 2%N. simpl. eagerUnifyU. go. From 82a6dde78c700648e4f9153c1d336536e76f1f1d Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Tue, 22 Sep 2026 21:26:03 -0400 Subject: [PATCH 08/31] Track complete managed types in shared_ptr control identities Record the complete payload type, including array extent, in CtrlBlockId. Use that type for allocation tokens and reconstruction, with delete_compat connecting it to the public shared_ptr element type. Constructor specs return the actual allocation type. This prevents the array model from treating T[] as an allocated complete object. Both constructor examples now assert the exact managed type. Specs and examples check in Emacs; Dune built test.vo and fractional_copy.vo. No new axioms or admits. The full Monad build will be checked after the separate destruction-condition revision. --- rocq-brick-libstdcpp/proof/shared_ptr/specs.v | 8 ++++++-- rocq-brick-libstdcpp/proof/shared_ptr/test.v | 2 ++ 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v index d071f316..005bc70d 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v @@ -46,6 +46,7 @@ Record CtrlBlockId : Set := { pieceRightLocs: list gname; (* each stores a unit. N -> gname may be tricky for constructor proof *) dataLoc: ptr; + payload_type: type; (* Complete allocation type, including the length of an array. *) }. #[local] Open Scope N_scope. @@ -88,7 +89,7 @@ Section specs. (dataLoc id),, ctrOffset |-> atomic.R "long" 1 (Z.of_N ctrVal) ** (if (bool_decide (ctrVal = 0)) then emp - else ownedPtr |-> alloc.tokenR ty 1%Qp + else ownedPtr |-> alloc.tokenR (payload_type id) 1%Qp ** ([∗ list] pieceid ∈ allPieceIds, if pieceOut pieceid then pieceRight id pieceid else ownedPtr |-> Rpiece pieceid)). @@ -98,7 +99,8 @@ Section specs. piece. In particular, splitting [q] does not create a [pieceRight]. *) Definition SharedPtrR (q : cQp.t) (id: CtrlBlockId) (Rpiece : nat -> Rep) (ownedPtr:ptr) : Rep := structR ("std::shared_ptr".<>) q - ** [| ([∗ list] pieceid ∈ allPieceIds, Rpiece pieceid) |-- anyR ty 1 |] + ** [| delete_compat ty (payload_type id) |] + ** [| ([∗ list] pieceid ∈ allPieceIds, Rpiece pieceid) |-- anyR (payload_type id) 1 |] ** ownedPtrOffset |-> primR (Tptr ty) q (Vptr ownedPtr) ** ctrlBlockPtrOffset |-> primR (Tptr (Tnamed ("std::atomic".<>))) q (Vptr (dataLoc id)) ** [| ownedPtr<>nullptr |] (* use NullSharedPtr otherwise *) @@ -144,6 +146,7 @@ Section specs. (* ^^ if anyR is not meaningful for non-scalar types, replace this with wp of default destructor *) \post Exists (ctrlBlockId: CtrlBlockId), + [| payload_type ctrlBlockId = ty |] ** this |-> SharedPtrR 1$m ctrlBlockId 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 *) @@ -277,6 +280,7 @@ Section specs. (* ^^ if anyR is not meaningful for non-scalar types, replace this with wp of default destructor *) \post Exists (ctrlBlockId: CtrlBlockId), + [| payload_type ctrlBlockId = ty |] ** this |-> SharedPtrR (Tincomplete_array ety) 1$m ctrlBlockId 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 *) diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/test.v b/rocq-brick-libstdcpp/proof/shared_ptr/test.v index c128fff3..4c11f669 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/test.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/test.v @@ -63,6 +63,7 @@ Section proofs. cpp.spec "testshared1()" as testshared1spec with ( \pre emp \post{p:ptr}[Vptr p] Exists payload sid, + [| payload_type sid = "int"%cpp_type |] ** p |-> SharedPtrR "int" 1$m sid (fun ctid => if bool_decide (ctid=0%nat) then anyR "int" 1 else emp) payload ** payload |-> intR (cQp.m 1) 1 ** ([∗ list] ctid ∈ allButFirstPieceId, @@ -137,6 +138,7 @@ Set Default Goal Selector "!". cpp.spec "testsharedarr()" as testsharedarrspec with ( \pre emp \post{p:ptr}[Vptr p] Exists payload sid, + [| payload_type sid = "int[2]"%cpp_type |] ** p |-> SharedPtrR "int[]" 1$m sid (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, From 38d52f14b62f1c9b51c239795071a3dbfa8eab00 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Tue, 22 Sep 2026 22:14:20 -0400 Subject: [PATCH 09/31] Permit update-aware destruction of shared_ptr payloads Replace the pure all-pieces-to-anyR condition with a persistent capability to run destruction of the complete managed type. This supports cancelling payload invariants and invoking nontrivial member destructors, while retaining the allocation token separately for deallocation. Constructor callers must establish the capability; it is not a new axiom. Port scalar/array constructor examples and prove guarded_int_destroy using existing cancellation and destruction rules. Keep the copy/destroy regression. Independent read-only review found no introduced blocker. Library operations remain assumed specs; this is not a proof of libstdc++ bodies or of VarCodeR. Validation: changed files checked interactively, test.vo and fractional_copy.vo built, the complete monad/monadproofs/proofs/all.vo build succeeded, and all.v checked through EOF in Emacs (locked-end 4034). No new axioms, admits, production C++ changes, or proof exclusions. --- .../proof/shared_ptr/fractional_copy.v | 23 ++++++++++++++ rocq-brick-libstdcpp/proof/shared_ptr/specs.v | 30 ++++++++++++------- rocq-brick-libstdcpp/proof/shared_ptr/test.v | 19 ++++++++---- 3 files changed, 55 insertions(+), 17 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/fractional_copy.v b/rocq-brick-libstdcpp/proof/shared_ptr/fractional_copy.v index 4eaaeb7a..68ce9022 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/fractional_copy.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/fractional_copy.v @@ -3,6 +3,7 @@ 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. @@ -47,4 +48,26 @@ Section with_cpp. iExists false, p, (id, pieceid), Rpiece. 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/specs.v b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v index 005bc70d..304f67ac 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v @@ -4,8 +4,12 @@ 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], chosen by the implementation, would typically be 2^64, to prevent overflow of the reference counter. -To ensure the destructor proof goes through, the init ctor requires [ [∗ list] ctid ∈ allPieceIds, Rpiece ctid) |-- anyR ty 1]. This becomes a part of [SharedPtrR]. -If anyR does not make sense for Tnamed, then it should be replaced with [wp (default_ctor of Tnamed) emp]. +The init constructor requires [payload_destructible]: collecting every payload +piece must suffice to run the managed object's destruction. This persistent +capability becomes part of [SharedPtrR]. Unlike a plain entailment to [anyR], +it allows ghost updates before destruction and accounts for nontrivial member +destructors. It must be supplied by the constructor's caller, not 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 @@ -70,6 +74,16 @@ Section specs. Context `{Σ : cpp_logic, MOD:inc_shared_ptr_cpp.source ⊧ σ}. #[local] Existing Instance br.ghost.excl_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). + Section tty. Context (ty:type). @@ -100,7 +114,7 @@ Section specs. Definition SharedPtrR (q : cQp.t) (id: CtrlBlockId) (Rpiece : nat -> Rep) (ownedPtr:ptr) : Rep := structR ("std::shared_ptr".<>) q ** [| delete_compat ty (payload_type id) |] - ** [| ([∗ list] pieceid ∈ allPieceIds, Rpiece pieceid) |-- anyR (payload_type id) 1 |] + ** pureR (payload_destructible (payload_type id) Rpiece) ** ownedPtrOffset |-> primR (Tptr ty) q (Vptr ownedPtr) ** ctrlBlockPtrOffset |-> primR (Tptr (Tnamed ("std::atomic".<>))) q (Vptr (dataLoc id)) ** [| ownedPtr<>nullptr |] (* use NullSharedPtr otherwise *) @@ -141,10 +155,7 @@ Section specs. We frame away the 0th piece in this spec. A derived spec can be proven where that framing away is not done *) \pre p |-> alloc.tokenR ty 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 [|([∗ list] pieceid ∈ allPieceIds, Rpiece pieceid) - |-- anyR ty 1 |] - (* ^^ if anyR is not meaningful for non-scalar types, - replace this with wp of default destructor *) + \pre payload_destructible ty Rpiece \post Exists (ctrlBlockId: CtrlBlockId), [| payload_type ctrlBlockId = ty |] ** this |-> SharedPtrR 1$m ctrlBlockId Rpiece p @@ -275,10 +286,7 @@ Section specs. \let{len} ty := Tarray ety len \pre p |-> alloc.tokenR ty 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 [|([∗ list] pieceid ∈ allPieceIds, Rpiece pieceid) - |-- anyR ty 1 |] - (* ^^ if anyR is not meaningful for non-scalar types, - replace this with wp of default destructor *) + \pre payload_destructible ty Rpiece \post Exists (ctrlBlockId: CtrlBlockId), [| payload_type ctrlBlockId = ty |] ** this |-> SharedPtrR (Tincomplete_array ety) 1$m ctrlBlockId Rpiece p diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/test.v b/rocq-brick-libstdcpp/proof/shared_ptr/test.v index 4c11f669..d1ff9175 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/test.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/test.v @@ -112,13 +112,17 @@ Set Default Goal Selector "!". rewrite <- _at_big_sepL. unfold allButFirstPieceId. rewrite allButFirstEmp. go. - provePure. + assert (Hdestroy : emp |-- payload_destructible "int" Rpiece). { - unfold allPieceIds. + unfold Rpiece. + unfold payload_destructible, allPieceIds. rewrite -> seqprefix with (prelen:=1%nat) by lia. simpl. - rewrite allButFirstEmp. go. + setoid_rewrite (allButFirstEmp "int"). go. + rewrite destroy_val_wp_destroy_val. + go. } + rewrite <- Hdestroy. go. normalize_ptrs. go. @@ -166,15 +170,18 @@ Set Default Goal Selector "!". rewrite <- _at_big_sepL. unfold allButFirstPieceId. rewrite allButFirstEmp. go. - provePure. + assert (Hdestroy : emp |-- payload_destructible "int[2]" Rpiece). { unfold Rpiece. - unfold allPieceIds. + unfold payload_destructible, allPieceIds. rewrite -> seqprefix with (prelen:=1%nat) by lia. simpl. - rewrite allButFirstEmp. + setoid_rewrite (allButFirstEmp "int[2]"). + go. + rewrite destroy_val_wp_destroy_val. go. } + rewrite <- Hdestroy. go. normalize_ptrs. go. From 5a891491f3ad7dc3048643e8ba5d5e53efb31fcf Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Tue, 22 Sep 2026 23:33:04 -0400 Subject: [PATCH 10/31] Prove a finite pool of shared-pointer acquisition tokens Define an auth_nat invariant owning the available exclusive piece rights. Prove allocation, take, refund, additive credit splitting, a reservation round-trip, and the capacity bound. Use existing ghost-state rules only; do not assume shared_ptr method specs or introduce axioms. Keep library protocol corrections separate. --- .../proof/shared_ptr/token_pool.v | 295 ++++++++++++++++++ 1 file changed, 295 insertions(+) create mode 100644 rocq-brick-libstdcpp/proof/shared_ptr/token_pool.v 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. From 530932fac3eb7ca388fbce33eda5c5af14493192 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Wed, 23 Sep 2026 12:53:35 -0400 Subject: [PATCH 11/31] Tie shared-pointer destruction to the handle's acquired piece Add the piece index to SharedPtrR and back it with fractional ghost ownership. Available indices retain their full witness in the invariant, including at zero count. Copy fixes the acquired index, moves preserve it, and destruction requires and refunds that index. Prove outstandingness and positive-count consequences independently of the assumed C++ method specs. Port scalar, array, and fractional-copy client tests without changing their proof bodies. No new axioms or admits. Validated interactively in Emacs and with dune build monad/monadproofs/proofs/all.vo and the shared_ptr/test.vo target in the composed workspace. --- .../proof/shared_ptr/fractional_copy.v | 6 +- .../proof/shared_ptr/handle_liveness.v | 113 ++++++++++++++++++ rocq-brick-libstdcpp/proof/shared_ptr/specs.v | 77 ++++++++---- rocq-brick-libstdcpp/proof/shared_ptr/test.v | 6 +- 4 files changed, 173 insertions(+), 29 deletions(-) create mode 100644 rocq-brick-libstdcpp/proof/shared_ptr/handle_liveness.v diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/fractional_copy.v b/rocq-brick-libstdcpp/proof/shared_ptr/fractional_copy.v index 68ce9022..21c6d6b5 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/fractional_copy.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/fractional_copy.v @@ -26,14 +26,14 @@ Section with_cpp. Context `{Sigma : cpp_logic, MOD : source ⊧ σ}. #[local] Hint Opaque SharedPtrR pieceRight : sl_opacity. - #[local] Instance learn_shared : LearnEq5 SharedPtrR := + #[local] Instance learn_shared : LearnEq6 SharedPtrR := ltac:(solve_learnable). cpp.spec "copy_then_destroy(const std::shared_ptr&)" from source as copy_then_destroy_spec with ( \arg{other : ptr} "source" (Vref other) - \prepost{q id p Rpiece} - other |-> SharedPtrR "int" q id Rpiece p + \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 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..c85f9c95 --- /dev/null +++ b/rocq-brick-libstdcpp/proof/shared_ptr/handle_liveness.v @@ -0,0 +1,113 @@ +(** 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 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/specs.v b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v index 304f67ac..22c2e1d9 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v @@ -19,6 +19,10 @@ Because BRiCk only supports SC atomics, the proof only works as if the stdlib im - 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. @@ -42,6 +46,7 @@ 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 Import iris.algebra.excl. +Require Import iris.algebra.frac. NES.Open std.atomic. @@ -49,6 +54,7 @@ NES.Open std.atomic. 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 allocation type, including the length of an array. *) }. @@ -73,6 +79,7 @@ Definition countLN {A : Type} (f : A -> bool) (l : list A) : N := 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 @@ -96,22 +103,43 @@ Section specs. | Some g => own (A := exclR unitO) g (Excl ()) | None => emp (* bad argument, pieceid > maxContention *) end. - + + (* 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 (dataLoc id),, ctrOffset |-> atomic.R "long" 1 (Z.of_N ctrVal) + ** ([∗ list] pieceid ∈ allPieceIds, + if pieceOut pieceid then pieceRight id pieceid + else pieceHandle id 1 pieceid) ** (if (bool_decide (ctrVal = 0)) then emp else ownedPtr |-> alloc.tokenR (payload_type id) 1%Qp ** ([∗ list] pieceid ∈ allPieceIds, - if pieceOut pieceid then pieceRight id pieceid else ownedPtr |-> Rpiece pieceid)). + if pieceOut pieceid then emp else ownedPtr |-> Rpiece pieceid)). (** Currently, we assume the control block is just an atomic counter. In reality, it is probably a struct. so move the atomicR to some defn ctrlBlockR *) (* [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) (Rpiece : nat -> Rep) (ownedPtr:ptr) : Rep := + Definition SharedPtrR (q : cQp.t) (id: CtrlBlockId) (pieceid : nat) + (Rpiece : nat -> Rep) (ownedPtr:ptr) : Rep := structR ("std::shared_ptr".<>) q ** [| delete_compat ty (payload_type id) |] ** pureR (payload_destructible (payload_type id) Rpiece) @@ -119,6 +147,9 @@ Section specs. ** ctrlBlockPtrOffset |-> primR (Tptr (Tnamed ("std::atomic".<>))) q (Vptr (dataLoc id)) ** [| 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 := @@ -126,11 +157,11 @@ Section specs. ** ownedPtrOffset |-> primR (Tptr ty) q (Vptr nullptr) ** ctrlBlockPtrOffset |-> primR (Tptr (Tnamed ("std::atomic".<>))) q (Vptr nullptr). - #[global] Instance SharedPtrR_fractional id Rpiece p : - CFractional (fun q => SharedPtrR q id Rpiece p) := _. - #[global] Instance SharedPtrR_as_fractional q id Rpiece p : - AsCFractional (SharedPtrR q id Rpiece p) - (fun q => SharedPtrR q id Rpiece p) q. + #[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 := _. @@ -158,7 +189,7 @@ Section specs. \pre payload_destructible ty Rpiece \post Exists (ctrlBlockId: CtrlBlockId), [| payload_type ctrlBlockId = ty |] ** - this |-> SharedPtrR 1$m ctrlBlockId Rpiece p + 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 *) ). @@ -171,9 +202,9 @@ Section specs. specify.template.ctor spty [Trv_ref ((Tnamed spty))] $ \this this \arg{other:ptr} "other" (Vptr other) - \pre{ctrlBlockId ownedPtr Rpiece} other |-> SharedPtrR 1$m ctrlBlockId Rpiece ownedPtr + \pre{ctrlBlockId pieceid ownedPtr Rpiece} other |-> SharedPtrR 1$m ctrlBlockId pieceid Rpiece ownedPtr \post other |-> NullSharedPtrR 1$m - ** this |-> SharedPtrR 1$m ctrlBlockId Rpiece ownedPtr. + ** this |-> SharedPtrR 1$m ctrlBlockId pieceid Rpiece ownedPtr. Definition SpecFor_move_ctor := RegisterSpec move_ctor. #[global] Existing Instance SpecFor_move_ctor. @@ -185,7 +216,7 @@ Section specs. (* 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 Rpiece p + this |-> SharedPtrR 1$m sid.1 sid.2 Rpiece p ** p |-> Rpiece sid.2 | true => fun sid=> this |-> NullSharedPtrR 1$m end) sid @@ -203,11 +234,11 @@ Section specs. specify.template.ctor spty [Tref (Tconst (Tnamed spty))] $ \this this \arg{other:ptr} "other" (Vptr other) - \prepost{q id p Rpiece} other |-> SharedPtrR q id Rpiece p + \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 Rpiece p. + p|->Rpiece pieceid ** this |-> SharedPtrR 1$m id pieceid Rpiece p. Definition SpecFor_copy_ctor := RegisterSpec copy_ctor. #[global] Existing Instance SpecFor_copy_ctor. @@ -239,7 +270,7 @@ Section specs. Definition deref := specify.template.op (SP_acc 0) OOStar function_qualifiers.Nc (Tref ty) [] $ \this this - \prepost{q id p Rpiece} this |-> (upcast_offset 0) |-> SharedPtrR q id Rpiece p + \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. @@ -249,23 +280,23 @@ Section specs. Definition arrow := specify.template.op (SP_acc 0) OOArrow function_qualifiers.Nc (Tptr ty) [] $ \this this - \prepost{q id p Rpiece} this |-> (upcast_offset 0) |-> SharedPtrR q id Rpiece p + \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 (p:ptr) op Rpiece - : Observe (type_ptr (Tnamed ("std::shared_ptr".<>)) p) (p|->SharedPtrR q id Rpiece op):= _. + #[global] Instance sharedR_typeptr_observe q id pieceid (p:ptr) op Rpiece + : Observe (type_ptr (Tnamed ("std::shared_ptr".<>)) p) (p|->SharedPtrR q id pieceid Rpiece op):= _. - Definition observeSharedTypeF q id t Rpiece op:= @observe_fwd _ _ _ (sharedR_typeptr_observe q id t Rpiece op). + Definition observeSharedTypeF q id pieceid t Rpiece op:= @observe_fwd _ _ _ (sharedR_typeptr_observe q id pieceid t Rpiece op). Definition allPiecesAndObjs Rpiece id (ownedPtr: ptr) (pieceOut: nat->bool) : Rep := ([∗ list] pieceid ∈ allPieceIds, if pieceOut pieceid then pureR (ownedPtr |-> Rpiece pieceid) - ** pureR (Exists (base:ptr), base |->SharedPtrR 1$m id Rpiece ownedPtr) + ** pureR (Exists (base:ptr), base |->SharedPtrR 1$m id pieceid Rpiece ownedPtr) else pureR (pieceRight id pieceid)). Lemma redistributePayloadOwnership {Rpieceold Rpiecenew: nat -> Rep} (pieceOut : nat -> bool) id ownedPtr: @@ -289,7 +320,7 @@ Section specs. \pre payload_destructible ty Rpiece \post Exists (ctrlBlockId: CtrlBlockId), [| payload_type ctrlBlockId = ty |] ** - this |-> SharedPtrR (Tincomplete_array ety) 1$m ctrlBlockId Rpiece p + 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 *) ). @@ -301,7 +332,7 @@ Section specs. 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 p Rpiece} this |-> (upcast_offset (Tincomplete_array ety) 1) |-> SharedPtrR (Tincomplete_array ety ) q id Rpiece p + \prepost{q id pieceid p Rpiece} this |-> (upcast_offset (Tincomplete_array ety) 1) |-> SharedPtrR (Tincomplete_array ety ) q id pieceid Rpiece p \post[Vref (p.[ety ! index])] emp. Definition SpecFor_subscript := RegisterSpec subscript. @@ -319,6 +350,6 @@ Ltac sharedPtrRpieceFromPost := match goal with H: context[@PostCondition ?a ?b ?c ?d] |- _ => match c with - | context[SharedPtrR _ _ _ ?rp _ ] => constr:(rp) + | context[SharedPtrR _ _ _ _ ?rp _ ] => constr:(rp) end end. diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/test.v b/rocq-brick-libstdcpp/proof/shared_ptr/test.v index d1ff9175..51697cc5 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/test.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/test.v @@ -64,7 +64,7 @@ Section proofs. \pre emp \post{p:ptr}[Vptr p] Exists payload sid, [| payload_type sid = "int"%cpp_type |] ** - p |-> SharedPtrR "int" 1$m sid (fun ctid => if bool_decide (ctid=0%nat) then anyR "int" 1 else emp) payload + 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) @@ -90,7 +90,7 @@ Section proofs. Qed. Opaque NullSharedPtrR. - #[global] Instance lll: LearnEq5 SharedPtrR := + #[global] Instance lll: LearnEq6 SharedPtrR := ltac:(solve_learnable). Set Default Goal Selector "!". @@ -143,7 +143,7 @@ Set Default Goal Selector "!". \pre emp \post{p:ptr}[Vptr p] Exists payload sid, [| payload_type sid = "int[2]"%cpp_type |] ** - p |-> SharedPtrR "int[]" 1$m sid (fun ctid => if bool_decide (ctid=0%nat) then anyR "int[2]" 1 else emp) payload + 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) From 4b702ccfa06b91819b340be0b60bdebd2d82915d Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Wed, 23 Sep 2026 20:02:30 -0400 Subject: [PATCH 12/31] Bound shared-pointer capacity by the signed libstdc++ counter Replace the admitted capacity and incorrect 2^32 lower bound with a sealed definition of INT_MAX (2^31 - 1) and proved bounds. Check the _Atomic_word ABI in the include translation unit and document the finite outstanding-handle argument. Use a module lock rather than plain Opaque: vm_compute otherwise unfolds the capacity and can expand the billion-element ghost-token sequence. The existing constructor tests and fractional-copy regression check without proof-script changes; both new arithmetic lemmas are closed under the global context. --- .../proof/shared_ptr/inc_shared_ptr.cpp | 9 +++++- rocq-brick-libstdcpp/proof/shared_ptr/specs.v | 32 +++++++++++++++++-- 2 files changed, 37 insertions(+), 4 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/inc_shared_ptr.cpp b/rocq-brick-libstdcpp/proof/shared_ptr/inc_shared_ptr.cpp index 50cb3901..5112bd81 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/inc_shared_ptr.cpp +++ b/rocq-brick-libstdcpp/proof/shared_ptr/inc_shared_ptr.cpp @@ -1 +1,8 @@ -#include +#include +#include +#include + +// 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/specs.v b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v index 22c2e1d9..9b0df2e0 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v @@ -2,7 +2,9 @@ We do not cover interaction with weak_ptr. 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], chosen by the implementation, would typically be 2^64, to prevent overflow of the reference counter. +[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. The init constructor requires [payload_destructible]: collecting every payload piece must suffice to run the managed object's destruction. This persistent @@ -60,7 +62,32 @@ Record CtrlBlockId : Set := }. #[local] Open Scope N_scope. -Definition maxContention : positive. Proof. Admitted. +(** 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 ctrOffset: offset. Proof. Admitted. (** offset of the field storing ownedPtr in any shared_ptr object *) @@ -68,7 +95,6 @@ Definition ownedPtrOffset: offset. Proof. Admitted. (** offset of the field storing ctrlBlock pointer in any shared_ptr object *) Definition ctrlBlockPtrOffset: offset. Proof. Admitted. -Lemma maxContentionLb : 2^32 <= Npos maxContention. Proof. Admitted. 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 )). From 33683b9bca5b26571159b99b1b0d844ea6bb7abc Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Thu, 24 Sep 2026 17:57:47 -0400 Subject: [PATCH 13/31] Fix shared_ptr handle layout and prove const conversion --- .../proof/shared_ptr/layout.v | 166 ++++++++++++++++++ rocq-brick-libstdcpp/proof/shared_ptr/specs.v | 59 ++++--- .../test/shared_ptr/const_conversion.v | 49 ++++++ 3 files changed, 249 insertions(+), 25 deletions(-) create mode 100644 rocq-brick-libstdcpp/proof/shared_ptr/layout.v create mode 100644 rocq-brick-libstdcpp/test/shared_ptr/const_conversion.v 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..7bf8f4f1 --- /dev/null +++ b/rocq-brick-libstdcpp/proof/shared_ptr/layout.v @@ -0,0 +1,166 @@ +(** 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. + +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] 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. + +#[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 complete_type.NMFacts.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 complete_type.NMFacts.add_neq_o. + { apply complete_type.NMFacts.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 -> complete_type.NMFacts.add_neq_o, + complete_type.NMFacts.add_neq_o. + { apply complete_type.NMFacts.add_eq_o, NM.E.eq_refl. } + all: 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 -> complete_type.NMFacts.add_neq_o, + complete_type.NMFacts.add_neq_o, complete_type.NMFacts.add_neq_o. + { apply complete_type.NMFacts.add_eq_o, NM.E.eq_refl. } + all: 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/specs.v b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v index 9b0df2e0..f2fcfd21 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v @@ -47,11 +47,15 @@ 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 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 := { @@ -90,10 +94,6 @@ Lemma maxContention_fits_int : (0 < Z.pos maxContention < 2^31)%Z. Proof. rewrite maxContention.unlock. split; reflexivity. Qed. Definition ctrOffset: offset. Proof. Admitted. -(** offset of the field storing ownedPtr in any shared_ptr object *) -Definition ownedPtrOffset: offset. Proof. Admitted. -(** offset of the field storing ctrlBlock pointer in any shared_ptr object *) -Definition ctrlBlockPtrOffset: offset. Proof. Admitted. Definition maxContentionQp := pos_to_Qp maxContention. Definition allPieceIds : list nat := (seq 0 (Pos.to_nat maxContention)). @@ -160,17 +160,15 @@ Section specs. ** ([∗ list] pieceid ∈ allPieceIds, if pieceOut pieceid then emp else ownedPtr |-> Rpiece pieceid)). - (** Currently, we assume the control block is just an atomic counter. - In reality, it is probably a struct. so move the atomicR to some defn ctrlBlockR *) + (** 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 := - structR ("std::shared_ptr".<>) q + SharedPtrHandleR ty q ownedPtr (dataLoc id) ** [| delete_compat ty (payload_type id) |] ** pureR (payload_destructible (payload_type id) Rpiece) - ** ownedPtrOffset |-> primR (Tptr ty) q (Vptr ownedPtr) - ** ctrlBlockPtrOffset |-> primR (Tptr (Tnamed ("std::atomic".<>))) q (Vptr (dataLoc id)) ** [| ownedPtr<>nullptr |] (* use NullSharedPtr otherwise *) ** [| lengthN (pieceRightLocs id) = Npos maxContention |] ** [| lengthN (pieceHandleLocs id) = Npos maxContention |] @@ -179,9 +177,7 @@ Section specs. ** pureR (inv nroot (Exists (pieceOut : nat ->bool), sptrInv id Rpiece ownedPtr pieceOut)). Definition NullSharedPtrR (q : cQp.t) : Rep := - structR ("std::shared_ptr".<>) q - ** ownedPtrOffset |-> primR (Tptr ty) q (Vptr nullptr) - ** ctrlBlockPtrOffset |-> primR (Tptr (Tnamed ("std::atomic".<>))) q (Vptr nullptr). + SharedPtrHandleR ty q nullptr nullptr. #[global] Instance SharedPtrR_fractional id i Rpiece p : CFractional (fun q => SharedPtrR q id i Rpiece p) := _. @@ -195,6 +191,27 @@ Section specs. AsCFractional (NullSharedPtrR q) NullSharedPtrR q. Proof. split; [done | apply _]. Qed. + #[local] Definition SharedPtrHandleR_const_C := + [CANCEL] SharedPtrHandleR_const. + #[local] Hint Opaque pieceHandle payload_destructible 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".<>) (Nctor [Tptr ty])).<> @@ -279,22 +296,12 @@ Section specs. \post this |-> NullSharedPtrR 1$m. - Definition SP_acc (mid: Z) := ("std::__shared_ptr_access" .<< - Atype ty, - Avalue (Eint 2 "enum __gnu_cxx::_Lock_policy"), - Avalue (Eint mid "bool"), - Avalue (Eint 0 "bool") >>)%cpp_name. - - Definition SP_impl := ("std::__shared_ptr" .<< - Atype ty, - Avalue (Eint 2 "enum __gnu_cxx::_Lock_policy") >>)%cpp_name. - (** Reconstruct the most-derived object pointer from the base-subobject "this". *) Definition upcast_offset (mid: Z) : offset := - (o_derived σ (SP_acc mid) SP_impl ,, o_derived σ SP_impl spty). + (o_derived σ (SP_acc ty mid) (SP_impl ty) ,, o_derived σ (SP_impl ty) spty). Definition deref := - specify.template.op (SP_acc 0) OOStar function_qualifiers.Nc (Tref ty) [] $ + 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. @@ -304,7 +311,7 @@ Section specs. #[global] Hint Opaque deref : sl_opacity. Definition arrow := - specify.template.op (SP_acc 0) OOArrow function_qualifiers.Nc (Tptr ty) [] $ + 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. @@ -370,6 +377,8 @@ Section specs. : sl_opacity. End specs. +#[global] Hint Opaque SharedPtrR NullSharedPtrR : sl_opacity. +#[global] Hint Resolve SharedPtrR_const_C NullSharedPtrR_const_C : sl_opacity. #[global] Hint Resolve observeSharedTypeF : sl_opacity. Ltac sharedPtrRpieceFromPost := 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 +static_assert(sizeof(std::shared_ptr) == 16); +static_assert(sizeof(std::shared_ptr) == 16); +static_assert(sizeof(std::shared_ptr) == 16); +static_assert(sizeof(std::shared_ptr) == 16); +static_assert(sizeof(std::shared_ptr) == 16); +static_assert(sizeof(std::shared_ptr) == 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. From 05ebfc8504076dd6fc6ee5e8313e6b51082de9b6 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Thu, 24 Sep 2026 18:02:35 -0400 Subject: [PATCH 14/31] Use explicit branches in shared_ptr layout lookup proofs --- rocq-brick-libstdcpp/proof/shared_ptr/layout.v | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/layout.v b/rocq-brick-libstdcpp/proof/shared_ptr/layout.v index 7bf8f4f1..af940c4c 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/layout.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/layout.v @@ -132,7 +132,8 @@ Proof. rewrite -> complete_type.NMFacts.add_neq_o, complete_type.NMFacts.add_neq_o. { apply complete_type.NMFacts.add_eq_o, NM.E.eq_refl. } - all: 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] Lemma SP_lookup_count ty : @@ -146,7 +147,9 @@ Proof. rewrite -> complete_type.NMFacts.add_neq_o, complete_type.NMFacts.add_neq_o, complete_type.NMFacts.add_neq_o. { apply complete_type.NMFacts.add_eq_o, NM.E.eq_refl. } - all: intro H; apply NM.eqL in H; discriminate. + { 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 From 5c88fc1df29e2007dc0225eb588c1e3847360fa9 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Sat, 26 Sep 2026 20:14:15 -0400 Subject: [PATCH 15/31] Mark shared pointer representation opaque for SL search --- rocq-brick-libstdcpp/proof/shared_ptr/specs.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v index f2fcfd21..99f059b3 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v @@ -130,6 +130,8 @@ Section specs. | 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. *) From ba48a0a8211c924c1451556fe65461b1da5ecb6d Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Fri, 9 Oct 2026 12:36:24 -0400 Subject: [PATCH 16/31] Correct shared-pointer counter ownership and retirement Model libstdc++'s _M_use_count as its actual raw int field rather than an abstract atomic at an admitted offset. Keep physical counter and payload resources only in the positive-count invariant; prove that the retired invariant contains only ghost tokens. Document the remaining partial-control-block boundary and excluded weak_ptr operations. Shared-pointer implementation specs remain assumed. Checked fractional_copy, token_pool, and handle_liveness targets. --- .../proof/shared_ptr/handle_liveness.v | 12 +++++++++ rocq-brick-libstdcpp/proof/shared_ptr/specs.v | 25 +++++++++++++++---- 2 files changed, 32 insertions(+), 5 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/handle_liveness.v b/rocq-brick-libstdcpp/proof/shared_ptr/handle_liveness.v index c85f9c95..10dc2746 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/handle_liveness.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/handle_liveness.v @@ -14,6 +14,18 @@ Section with_cpp. #[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. diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v index 99f059b3..7dc2fc33 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v @@ -93,8 +93,6 @@ 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 ctrOffset: offset. Proof. Admitted. - 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 )). @@ -152,15 +150,32 @@ Section specs. Definition sptrInv (id: CtrlBlockId) (Rpiece : nat -> Rep) (ownedPtr:ptr) (pieceOut : nat ->bool) : mpred := let ctrVal := countLN pieceOut allPieceIds in - (dataLoc id),, ctrOffset |-> atomic.R "long" 1 (Z.of_N ctrVal) - ** ([∗ list] pieceid ∈ allPieceIds, + ([∗ list] pieceid ∈ allPieceIds, if pieceOut pieceid then pieceRight id pieceid else pieceHandle id 1 pieceid) ** (if (bool_decide (ctrVal = 0)) then emp - else ownedPtr |-> alloc.tokenR (payload_type id) 1%Qp + else (dataLoc id) ., + (SP_counted_base .:: Nid "_M_use_count") + |-> intR 1$m (Z.of_N ctrVal) + ** ownedPtr |-> alloc.tokenR (payload_type id) 1%Qp ** ([∗ 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] 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. + + This remains a partial control-block model for the assumed library + specs, not a verified libstdc++ implementation. A complete body proof + must additionally own the control-block allocation, dynamic-class and + deleter fields, account for its implicit weak reference, and justify + the actual acquire/release operations. No external weak_ptr operations + are covered by this interface. *) (** The control-block model above remains abstract. [SharedPtrHandleR] describes the complete handle, not the object its [_M_pi] points to. *) From 3c3b9d4d41fe1e49d6a5536e7c0d357594694f3e Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Mon, 12 Oct 2026 12:40:30 -0400 Subject: [PATCH 17/31] Model separate and combined shared-pointer allocations Replace the mandatory standalone payload allocation in sptrInv with an existential allocation case. Preserve public SharedPtrR parameters and the indexed copy-credit protocol. Default make_shared objects retain their enclosing allocation; array factories retain the backing allocation and the tail control-block placement token. Keep the existing separate new/new[] routes. Document that custom deleters, custom allocators, aliasing, overwrite factories, and external weak_ptr operations remain unsupported. No new axioms or factory specs; this is an allocation-component correction, not verification of the still-partial control-block model or C++ library bodies. Checked allocation, specs, and liveness interactively; allocation_test, fractional_copy, handle_liveness, and shared_ptr/test.vo build. Full Monad all.vo validation is running separately. --- .../proof/shared_ptr/allocation.v | 102 ++++++++++++++++++ .../proof/shared_ptr/allocation_test.v | 81 ++++++++++++++ rocq-brick-libstdcpp/proof/shared_ptr/specs.v | 29 +++-- 3 files changed, 205 insertions(+), 7 deletions(-) create mode 100644 rocq-brick-libstdcpp/proof/shared_ptr/allocation.v create mode 100644 rocq-brick-libstdcpp/proof/shared_ptr/allocation_test.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..fdde65e8 --- /dev/null +++ b/rocq-brick-libstdcpp/proof/shared_ptr/allocation.v @@ -0,0 +1,102 @@ +(** Allocation ownership for the default libstdc++ shared-pointer constructors. + This is only the allocation part of the control-block invariant: it does + not own the payload fields or the reference counters. + + Custom deleters, custom allocators, aliasing constructors, and + make_shared_for_overwrite are not supported. The internal __sp_array_delete + used by shared_ptr(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", + 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", + Avalue (Eint 2 "enum __gnu_cxx::_Lock_policy") >>)%cpp_name + end. + +Section with_cpp. + Context `{Sigma : cpp_logic} {CU : genv}. + + (** 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) (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 => + root |-> alloc.tokenR (Tnamed cn) 1%Qp ** + owned |-> alloc.tokenR payload_ty 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. + 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), + [| 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 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. *) + root |-> alloc.tokenR (Tnamed cn) 1%Qp ** + provides_storage (shared_inplace_storage payload_ty root) + owned payload_ty + end + end. +End with_cpp. + +#[global] Hint Opaque SharedAllocationR : 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..44e91e08 --- /dev/null +++ b/rocq-brick-libstdcpp/proof/shared_ptr/allocation_test.v @@ -0,0 +1,81 @@ +(** 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. + +Section with_cpp. + Context `{Sigma : cpp_logic} {CU : genv}. + + (** The ordinary new/new[] route retains both allocation tokens. *) + Example separate_allocations (ty : type) (root owned : ptr) : + root |-> alloc.tokenR (Tnamed (shared_control_name SeparateAllocation ty)) 1 ** + owned |-> alloc.tokenR ty 1 + |-- SharedAllocationR SeparateAllocation ty + (root ,, o_base CU (shared_control_name SeparateAllocation ty) + SP_counted_base) owned. + Proof. + unfold SharedAllocationR. + rewrite <- (bi.exist_intro root). + go. + Qed. + + (** A combined named object needs no token allocating the payload itself. *) + Example combined_object (nm : name) (root owned : ptr) : + root |-> alloc.tokenR + (Tnamed (shared_control_name CombinedAllocation (Tnamed nm))) 1 ** + provides_storage (shared_inplace_storage (Tnamed nm) root) owned (Tnamed nm) + |-- SharedAllocationR CombinedAllocation (Tnamed nm) + (root ,, o_base CU + (shared_control_name CombinedAllocation (Tnamed nm)) SP_counted_base) + owned. + Proof. + unfold SharedAllocationR. + rewrite <- (bi.exist_intro root). + 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) + (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 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) + (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). + 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", + 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", + Avalue (Eint 2 "enum __gnu_cxx::_Lock_policy") >>)%cpp_name. +Proof. reflexivity. Qed. diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v index 7dc2fc33..0835d444 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v @@ -1,5 +1,11 @@ (** Specs of shared_ptr. We do not cover interaction with weak_ptr. +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. The latter is a representation correction, +not a proof or a new assumed spec of make_shared; factory specs remain to be +provided when verifying those calls. See [SharedAllocationR]. 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 @@ -48,6 +54,7 @@ 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 Import iris.algebra.excl. Require Import iris.algebra.frac. @@ -62,7 +69,8 @@ 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 allocation type, including the length of an array. *) + payload_type: type; (* Complete managed-object type, including array length. + Not necessarily the type of an independent allocation. *) }. #[local] Open Scope N_scope. @@ -158,7 +166,9 @@ Section specs. else (dataLoc id) ., (SP_counted_base .:: Nid "_M_use_count") |-> intR 1$m (Z.of_N ctrVal) - ** ownedPtr |-> alloc.tokenR (payload_type id) 1%Qp + ** (Exists kind : shared_allocation_kind, + SharedAllocationR kind (payload_type id) + (dataLoc id) ownedPtr) ** ([∗ list] pieceid ∈ allPieceIds, if pieceOut pieceid then emp else ownedPtr |-> Rpiece pieceid)). @@ -171,11 +181,14 @@ Section specs. permits closing the invariant before running a reentrant destructor. This remains a partial control-block model for the assumed library - specs, not a verified libstdc++ implementation. A complete body proof - must additionally own the control-block allocation, dynamic-class and - deleter fields, account for its implicit weak reference, and justify - the actual acquire/release operations. No external weak_ptr operations - are covered by this interface. *) + specs, not a verified libstdc++ implementation. It now retains the + appropriate allocation ownership in [SharedAllocationR]. + A complete body proof must additionally own the remaining control-block + fields and dynamic-class witnesses, account for its implicit weak + reference, and justify the actual acquire/release operations. For an + array factory it must also connect _M_n/_S_tail to the retained allocation + size and recover the padding for deallocation. No external weak_ptr + operations are covered by this interface. *) (** The control-block model above remains abstract. [SharedPtrHandleR] describes the complete handle, not the object its [_M_pi] points to. *) @@ -184,6 +197,8 @@ Section specs. Definition SharedPtrR (q : cQp.t) (id: CtrlBlockId) (pieceid : nat) (Rpiece : nat -> Rep) (ownedPtr:ptr) : Rep := SharedPtrHandleR ty q ownedPtr (dataLoc id) + (* This is managed-type compatibility, not permission to delete ownedPtr. + The allocation case inside sptrInv determines what can be deallocated. *) ** [| delete_compat ty (payload_type id) |] ** pureR (payload_destructible (payload_type id) Rpiece) ** [| ownedPtr<>nullptr |] (* use NullSharedPtr otherwise *) From a762951f15b301b3625819248093309beab91661 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Tue, 13 Oct 2026 23:32:50 -0400 Subject: [PATCH 18/31] Specify non-array make_shared with certified payload construction Require the actual construct_at specialization and payload destruction capability instead of assuming arbitrary constructor behavior. Preserve forwarded-argument effects and return the initial handle, payload piece, and bounded copy rights using the existing combined-allocation representation. Exclude enable_shared_from_this through an explicit inheritance guard, retain the array-factory and weak-pointer limitations, and test mutable, const, and rvalue calls. Prove the sample payload constructor, destructor, placement allocation, and linked construction obligation. Export payload_destructible opacity for clients. Validation: interactive spec and regression checks; monad/monadproofs/proofs/all.v checked to EOF in Emacs; all.vo built successfully. Final dependency build took 1241.290 seconds; new regression fixture took 333.571 seconds in that parallel build. (cherry picked from commit c0ed806251bf7b0ad6510261e4c73e3d34dc1d19) --- .../proof/shared_ptr/make_shared.v | 119 ++++++++++ .../proof/shared_ptr/make_shared_test.v | 217 ++++++++++++++++++ rocq-brick-libstdcpp/proof/shared_ptr/specs.v | 7 +- 3 files changed, 339 insertions(+), 4 deletions(-) create mode 100644 rocq-brick-libstdcpp/proof/shared_ptr/make_shared.v create mode 100644 rocq-brick-libstdcpp/proof/shared_ptr/make_shared_test.v 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..0479b7d6 --- /dev/null +++ b/rocq-brick-libstdcpp/proof/shared_ptr/make_shared.v @@ -0,0 +1,119 @@ +(** The normal-return interface of the non-array std::make_shared, 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 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. *) +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 ⊧ σ}. + + Definition make_shared_no_esft (ty : type) : Prop := + match erase_qualifiers ty with + | Tnamed cls => forall path base, + class_derives cls path -> base ∈ cls :: path -> + forall pack, + base <> Ninst "std::enable_shared_from_this" pack /\ + base <> Ninst "std::__enable_shared_from_this" pack + | _ => True + end. + + Lemma make_shared_no_esft_no_bases cls layout : + glob_def σ 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) -> + make_shared_no_esft (Tnamed cls). + Proof. + intros Hlayout Hbases Hname path base Hpath Hin pack. + inversion Hpath; subst. + { apply elem_of_cons in Hin. destruct Hin as [-> | Hin]. + { apply Hname. } + { inversion Hin. } } + { match goal with + | H : _ !! cls = Some (Gstruct ?st) |- _ => + change (glob_def σ cls = Some (Gstruct st)) in H; + rewrite Hlayout in H; injection H as Heq; subst st + end. + match goal with + | H : _ ∈ layout.(s_bases) |- _ => rewrite Hbases in H; inversion H + end. } + Qed. + + (** 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. + [after] includes source ownership and other constructor side effects. *) + Definition make_shared_construction (ty : type) (args : list type) + (values : list val) (Rpiece : nat -> Rep) (before after : 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) ** + p |-> ([∗ list] i ∈ allPieceIds, Rpiece i) ** after. + + (* 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 + 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 [| make_shared_no_esft ty |] + \pre [| match erase_qualifiers ty with + | Tarray _ _ | Tincomplete_array _ => False + | _ => True + end |] + \pre{Rpiece before after} + make_shared_construction ty args values Rpiece before after + \pre before + \pre payload_destructible ty Rpiece + \post{retp : ptr} [Vptr retp] + Exists (id : CtrlBlockId) (p : ptr), + [| payload_type id = ty |] ** + retp |-> SharedPtrR ty 1$m id 0 Rpiece p ** + p |-> Rpiece 0%nat ** + ([∗ list] i ∈ allButFirstPieceId, pieceRight id i) ** after. + + 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..54e2607b --- /dev/null +++ b/rocq-brick-libstdcpp/proof/shared_ptr/make_shared_test.v @@ -0,0 +1,217 @@ +(** 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 +struct Payload { + int value; + explicit Payload(int n) : value(n) {} +}; +std::shared_ptr make_payload(int& n) { + return std::make_shared(n); +} +std::shared_ptr make_const_payload(int const& n) { + return std::make_shared(n); +} +std::shared_ptr make_rvalue_payload(int&& n) { + return std::make_shared(static_cast(n)); +} +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 : make_shared_no_esft "Payload". + Proof using MOD. + eapply make_shared_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{Rpiece before after} + make_shared_construction "Payload" ["int&"%cpp_type] [Vref argp] + Rpiece before after + \pre before + \pre payload_destructible "Payload" Rpiece + \post{retp : ptr} [Vptr retp] + Exists (id : CtrlBlockId) (p : ptr), + [| payload_type id = "Payload"%cpp_type |] ** + retp |-> SharedPtrR "Payload" 1$m id 0 Rpiece p ** + p |-> Rpiece 0%nat ** + ([∗ list] i ∈ allButFirstPieceId, pieceRight id i) ** after + ). + + Lemma make_payload_ok : verify[source] make_payload_spec. + Proof using MOD. + have Hnoesft := payload_no_esft. + verify_spec. + go. + iExists [Vref argp], Rpiece, before, after. + 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{Rpiece before after} + make_shared_construction "const Payload" ["const int&"%cpp_type] [Vref argp] + Rpiece before after + \pre before + \pre payload_destructible "const Payload" Rpiece + \post{retp : ptr} [Vptr retp] + Exists (id : CtrlBlockId) (p : ptr), + [| payload_type id = "const Payload"%cpp_type |] ** + retp |-> SharedPtrR "const Payload" 1$m id 0 Rpiece p ** + p |-> Rpiece 0%nat ** + ([∗ list] i ∈ allButFirstPieceId, pieceRight id i) ** after + ). + + 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], Rpiece, before, after. + 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{Rpiece before after} + make_shared_construction "Payload" ["int"%cpp_type] [Vref argp] + Rpiece before after + \pre before + \pre payload_destructible "Payload" Rpiece + \post{retp : ptr} [Vptr retp] + Exists (id : CtrlBlockId) (p : ptr), + [| payload_type id = "Payload"%cpp_type |] ** + retp |-> SharedPtrR "Payload" 1$m id 0 Rpiece p ** + p |-> Rpiece 0%nat ** + ([∗ list] i ∈ allButFirstPieceId, pieceRight id i) ** after + ). + + 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], Rpiece, before, after. + 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&)" inline. + Lemma construct_payload_ok (q : cQp.t) (qflag : Qp) (argp : ptr) (n : Z) + (Rpiece : nat -> Rep) (after : mpred) : + verify[source] + (make_shared_construction "Payload" ["int&"%cpp_type] [Vref argp] + Rpiece + (argp |-> intR q n ** + _global "std::is_array_v" |-> boolR qflag$c false ** + Forall p : ptr, p |-> PayloadR 1$m n -* + p |-> ([∗ list] i ∈ allPieceIds, Rpiece i) ** after) + (argp |-> intR q n ** + _global "std::is_array_v" |-> boolR qflag$c false ** after)). + 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) + (_x_4 |-> ([∗ list] i ∈ allPieceIds, Rpiece i) ** after)). + go. + Qed. + + Lemma construct_payload_from_code (q : cQp.t) (qflag : Qp) + (argp : ptr) (n : Z) (Rpiece : nat -> Rep) (after : mpred) : + denoteModule source |-- + make_shared_construction "Payload" ["int&"%cpp_type] [Vref argp] + Rpiece + (argp |-> intR q n ** + _global "std::is_array_v" |-> boolR qflag$c false ** + Forall p : ptr, p |-> PayloadR 1$m n -* + p |-> ([∗ list] i ∈ allPieceIds, Rpiece i) ** after) + (argp |-> intR q n ** + _global "std::is_array_v" |-> boolR qflag$c false ** after). + Proof using MOD. + wapply (construct_payload_ok q qflag argp n Rpiece 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/specs.v b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v index 0835d444..59c217eb 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v @@ -3,9 +3,8 @@ We do not cover interaction with weak_ptr. 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. The latter is a representation correction, -not a proof or a new assumed spec of make_shared; factory specs remain to be -provided when verifying those calls. See [SharedAllocationR]. +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 @@ -409,7 +408,7 @@ Section specs. : sl_opacity. End specs. -#[global] Hint Opaque SharedPtrR NullSharedPtrR : sl_opacity. +#[global] Hint Opaque SharedPtrR NullSharedPtrR payload_destructible : sl_opacity. #[global] Hint Resolve SharedPtrR_const_C NullSharedPtrR_const_C : sl_opacity. #[global] Hint Resolve observeSharedTypeF : sl_opacity. From a71634acdc525589f56e39906906a7669a2e4612 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Wed, 14 Oct 2026 14:22:05 -0400 Subject: [PATCH 19/31] Own the primary libstdc++ allocator base subobject Include __new_allocator ownership in allocator.R. Preserve the empty void and top-level cv-qualified specializations, and derive fractional laws without expanding the conditional through the generic derive tactic. This repairs the existing assumed allocator lifecycle interface; it adds no axiom. Checked the Intercode const conversion and the complete Monad all.vo suite. (cherry picked from commit 8da27b2fc1446aba57ef67f2851db42c6480480d) --- rocq-brick-libstdcpp/proof/allocator/spec.v | 23 +++++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) 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. From 5ff760bf0cf6b75c1e0dc4c950cb96685a33ec28 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Wed, 14 Oct 2026 14:22:14 -0400 Subject: [PATCH 20/31] Specify bounded shared_ptr copy assignment Add the approved generic library interface for a nonempty fractional source and a distinct, possibly empty destination. Require acquisition of a new piece before returning the old destination's piece right. Keep self-assignment and empty sources outside this interface. Add a cpp.prog client regression; this does not verify the library implementation. The full Monad all.vo suite passes. (cherry picked from commit 427b0ddef7dc6514c3338a80feeee47157754073) --- .../proof/shared_ptr/assignment.v | 49 +++++++++++++++++ .../proof/shared_ptr/assignment_test.v | 55 +++++++++++++++++++ 2 files changed, 104 insertions(+) create mode 100644 rocq-brick-libstdcpp/proof/shared_ptr/assignment.v create mode 100644 rocq-brick-libstdcpp/proof/shared_ptr/assignment_test.v 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 +std::shared_ptr& assign(std::shared_ptr& destination, + std::shared_ptr 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&, const std::shared_ptr&)" + 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. From 141fcc76231f90a0c3a7b475e8f57f8774a3aeff Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Wed, 14 Oct 2026 20:10:51 -0400 Subject: [PATCH 21/31] Unify make_shared payload ownership with raw-pointer adoption Let the verified construct_at obligation return an allocation-dependent descriptor, all pieces for its fixed recipe, and the matching destruction capability. make_shared returns a handle using exactly that descriptor and family; SharedPtrR, raw-pointer adoption, copy credits, and destruction interfaces are unchanged. Model libstdc++'s managed remove_cv_t with top-level drop_qualifiers, preserving pointee constness. Document intentional disposal of placement-new metadata without discarding allocation ownership. Port the forwarding and constructor regressions and add a pointer-to-const factory client. Checked interactively in Emacs; Monad proofs/all.v checks to EOF and proofs/all.vo builds. No new axioms or admits. (cherry picked from commit f9f1402270e44cd8471964f3c14ed028e3dc441f) --- .../proof/shared_ptr/make_shared.v | 43 +++++-- .../proof/shared_ptr/make_shared_test.v | 117 ++++++++++++------ 2 files changed, 107 insertions(+), 53 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/make_shared.v b/rocq-brick-libstdcpp/proof/shared_ptr/make_shared.v index 0479b7d6..f2efabfc 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/make_shared.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/make_shared.v @@ -16,7 +16,14 @@ 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. *) + 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. @@ -63,9 +70,15 @@ Section with_cpp. 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. - [after] includes source ownership and other constructor side effects. *) - Definition make_shared_construction (ty : type) (args : list type) - (values : list val) (Rpiece : nat -> Rep) (before after : mpred) : mpred := + 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) $ @@ -79,7 +92,9 @@ Section with_cpp. \post{p : ptr} [Vptr p] provides_storage storage p ty ** p |-> new_token.R 1%Qp (new_token.mk ty storage 0) ** - p |-> ([∗ list] i ∈ allPieceIds, Rpiece i) ** after. + 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 @@ -88,6 +103,9 @@ Section with_cpp. 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. The handle + remains shared_ptr; 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 >>)) @@ -101,16 +119,15 @@ Section with_cpp. | Tarray _ _ | Tincomplete_array _ => False | _ => True end |] - \pre{Rpiece before after} - make_shared_construction ty args values Rpiece before after + \pre{{D} (pieces : D -> nat -> Rep) before after} + make_shared_construction managed args values pieces before after \pre before - \pre payload_destructible ty Rpiece \post{retp : ptr} [Vptr retp] - Exists (id : CtrlBlockId) (p : ptr), - [| payload_type id = ty |] ** - retp |-> SharedPtrR ty 1$m id 0 Rpiece p ** - p |-> Rpiece 0%nat ** - ([∗ list] i ∈ allButFirstPieceId, pieceRight id i) ** after. + Exists (d : D) (id : CtrlBlockId) (p : ptr), + [| payload_type id = managed |] ** + 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. diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/make_shared_test.v b/rocq-brick-libstdcpp/proof/shared_ptr/make_shared_test.v index 54e2607b..2204dbef 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/make_shared_test.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/make_shared_test.v @@ -30,6 +30,9 @@ std::shared_ptr make_const_payload(int const& n) { std::shared_ptr make_rvalue_payload(int&& n) { return std::make_shared(static_cast(n)); } +std::shared_ptr make_pointer_payload(int const*& p) { + return std::make_shared(p); +} Payload* construct_payload(Payload* p, int& n) { return std::construct_at(p, n); } @@ -53,17 +56,16 @@ Section with_cpp. cpp.spec "make_payload(int&)" from source as make_payload_spec with ( \arg{argp : ptr} "n" (Vref argp) \prepost argp |-> type_ptrR "int" - \pre{Rpiece before after} + \pre{{D} (pieces : D -> nat -> Rep) before after} make_shared_construction "Payload" ["int&"%cpp_type] [Vref argp] - Rpiece before after + pieces before after \pre before - \pre payload_destructible "Payload" Rpiece \post{retp : ptr} [Vptr retp] - Exists (id : CtrlBlockId) (p : ptr), + Exists (d : D) (id : CtrlBlockId) (p : ptr), [| payload_type id = "Payload"%cpp_type |] ** - retp |-> SharedPtrR "Payload" 1$m id 0 Rpiece p ** - p |-> Rpiece 0%nat ** - ([∗ list] i ∈ allButFirstPieceId, pieceRight id i) ** after + 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. @@ -71,24 +73,25 @@ Section with_cpp. have Hnoesft := payload_no_esft. verify_spec. go. - iExists [Vref argp], Rpiece, before, after. + 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{Rpiece before after} - make_shared_construction "const Payload" ["const int&"%cpp_type] [Vref argp] - Rpiece before after + \pre{{D} (pieces : D -> nat -> Rep) before after} + make_shared_construction "Payload" ["const int&"%cpp_type] [Vref argp] + pieces before after \pre before - \pre payload_destructible "const Payload" Rpiece \post{retp : ptr} [Vptr retp] - Exists (id : CtrlBlockId) (p : ptr), - [| payload_type id = "const Payload"%cpp_type |] ** - retp |-> SharedPtrR "const Payload" 1$m id 0 Rpiece p ** - p |-> Rpiece 0%nat ** - ([∗ list] i ∈ allButFirstPieceId, pieceRight id i) ** after + 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. @@ -96,24 +99,25 @@ Section with_cpp. have Hnoesft := payload_no_esft. verify_spec. go. - iExists [Vref argp], Rpiece, before, after. + 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{Rpiece before after} + \pre{{D} (pieces : D -> nat -> Rep) before after} make_shared_construction "Payload" ["int"%cpp_type] [Vref argp] - Rpiece before after + pieces before after \pre before - \pre payload_destructible "Payload" Rpiece \post{retp : ptr} [Vptr retp] - Exists (id : CtrlBlockId) (p : ptr), + Exists (d : D) (id : CtrlBlockId) (p : ptr), [| payload_type id = "Payload"%cpp_type |] ** - retp |-> SharedPtrR "Payload" 1$m id 0 Rpiece p ** - p |-> Rpiece 0%nat ** - ([∗ list] i ∈ allButFirstPieceId, pieceRight id i) ** after + 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. @@ -121,7 +125,36 @@ Section with_cpp. have Hnoesft := payload_no_esft. verify_spec. go. - iExists [Vref argp], Rpiece, before, after. + 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. @@ -172,17 +205,19 @@ Section with_cpp. (* The client supplies a partition of genuine field ownership, not a constructor axiom for an arbitrary [Rpiece]. *) #[local] cpp.spec "std::forward(int&)" inline. - Lemma construct_payload_ok (q : cQp.t) (qflag : Qp) (argp : ptr) (n : Z) - (Rpiece : nat -> Rep) (after : mpred) : + 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] - Rpiece + pieces (argp |-> intR q n ** _global "std::is_array_v" |-> boolR qflag$c false ** Forall p : ptr, p |-> PayloadR 1$m n -* - p |-> ([∗ list] i ∈ allPieceIds, Rpiece i) ** after) - (argp |-> intR q n ** - _global "std::is_array_v" |-> boolR qflag$c false ** after)). + 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" |-> boolR qflag$c false ** after d)). Proof using MOD. verify_spec. go. @@ -194,23 +229,25 @@ Section with_cpp. go. rewrite (bi.forall_elim _x_4). wapply (bi.wand_elim_l (_x_4 |-> PayloadR 1$m n) - (_x_4 |-> ([∗ list] i ∈ allPieceIds, Rpiece i) ** after)). + (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 (q : cQp.t) (qflag : Qp) - (argp : ptr) (n : Z) (Rpiece : nat -> Rep) (after : mpred) : + 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] - Rpiece + pieces (argp |-> intR q n ** _global "std::is_array_v" |-> boolR qflag$c false ** Forall p : ptr, p |-> PayloadR 1$m n -* - p |-> ([∗ list] i ∈ allPieceIds, Rpiece i) ** after) - (argp |-> intR q n ** - _global "std::is_array_v" |-> boolR qflag$c false ** after). + 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" |-> boolR qflag$c false ** after d). Proof using MOD. - wapply (construct_payload_ok q qflag argp n Rpiece after). + 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. From 70ee50caaf49c693ae6d40dbeee8a0387c094092 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Tue, 20 Oct 2026 23:48:55 -0400 Subject: [PATCH 22/31] Port shared-pointer allocation ownership to upstream allocation metadata (cherry picked from commit 76391a40c6701cddf9fb7b93accbdc31f41a6afd) --- .../proof/shared_ptr/allocation.v | 19 +++++++++------ .../proof/shared_ptr/allocation_test.v | 24 ++++++++++++------- .../proof/shared_ptr/layout.v | 21 +++++++++------- 3 files changed, 40 insertions(+), 24 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/allocation.v b/rocq-brick-libstdcpp/proof/shared_ptr/allocation.v index fdde65e8..40dd2ac4 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/allocation.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/allocation.v @@ -70,8 +70,9 @@ Section with_cpp. [| control = root ,, o_base CU cn SP_counted_base |] ** match kind with | SeparateAllocation => - root |-> alloc.tokenR (Tnamed cn) 1%Qp ** - owned |-> alloc.tokenR payload_ty 1%Qp + Exists control_alignment payload_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 _ _ => @@ -79,22 +80,26 @@ Section with_cpp. 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), + 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 total ** + 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. *) - root |-> alloc.tokenR (Tnamed cn) 1%Qp ** - provides_storage (shared_inplace_storage payload_ty root) - owned payload_ty + 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. diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/allocation_test.v b/rocq-brick-libstdcpp/proof/shared_ptr/allocation_test.v index 44e91e08..5abf13be 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/allocation_test.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/allocation_test.v @@ -13,22 +13,27 @@ Section with_cpp. Context `{Sigma : cpp_logic} {CU : genv}. (** The ordinary new/new[] route retains both allocation tokens. *) - Example separate_allocations (ty : type) (root owned : ptr) : - root |-> alloc.tokenR (Tnamed (shared_control_name SeparateAllocation ty)) 1 ** - owned |-> alloc.tokenR ty 1 + 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 (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), + <- (bi.exist_intro payload_alignment). go. Qed. (** A combined named object needs no token allocating the payload itself. *) - Example combined_object (nm : name) (root owned : ptr) : - root |-> alloc.tokenR - (Tnamed (shared_control_name CombinedAllocation (Tnamed nm))) 1 ** + 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) (root ,, o_base CU @@ -37,6 +42,8 @@ Section with_cpp. Proof. unfold SharedAllocationR. rewrite <- (bi.exist_intro root). + cbn [erase_qualifiers]. + rewrite <- (bi.exist_intro alignment). go. Qed. @@ -44,11 +51,12 @@ Section with_cpp. 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 total ** + 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) @@ -61,7 +69,7 @@ Section with_cpp. 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 control_size), <- (bi.exist_intro alignment). go. Qed. End with_cpp. diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/layout.v b/rocq-brick-libstdcpp/proof/shared_ptr/layout.v index af940c4c..ac9aef3f 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/layout.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/layout.v @@ -2,6 +2,7 @@ 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. @@ -98,6 +99,8 @@ Definition shared_ptr_const_tu (ty : type) : translation_unit := (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)). @@ -105,7 +108,7 @@ Proof. rewrite VmEq_eq_iff. change (NM.find (SP_name ty) (types (shared_ptr_const_tu ty)) = Some (Gstruct (SP_outer_struct ty))). - apply complete_type.NMFacts.add_eq_o. + apply SPNameMapFacts.add_eq_o. apply NM.E.eq_refl. Qed. @@ -116,8 +119,8 @@ Proof. rewrite VmEq_eq_iff. change (NM.find (SP_impl ty) (types (shared_ptr_const_tu ty)) = Some (Gstruct (SP_impl_struct ty))). - rewrite complete_type.NMFacts.add_neq_o. - { apply complete_type.NMFacts.add_eq_o, NM.E.eq_refl. } + rewrite SPNameMapFacts.add_neq_o. + { apply SPNameMapFacts.add_eq_o, NM.E.eq_refl. } { intro H. apply NM.eqL in H. discriminate. } Qed. @@ -129,9 +132,9 @@ Proof. 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 -> complete_type.NMFacts.add_neq_o, - complete_type.NMFacts.add_neq_o. - { apply complete_type.NMFacts.add_eq_o, NM.E.eq_refl. } + 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. @@ -144,9 +147,9 @@ Proof. change (NM.find SP_count (types (shared_ptr_const_tu ty)) = Some (Gstruct SP_count_struct)). unfold shared_ptr_const_tu. cbn [types]. - rewrite -> complete_type.NMFacts.add_neq_o, - complete_type.NMFacts.add_neq_o, complete_type.NMFacts.add_neq_o. - { apply complete_type.NMFacts.add_eq_o, NM.E.eq_refl. } + 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. } From 728d6f3f3767056b163769c5daeda43db12b7028 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Wed, 21 Oct 2026 01:18:52 -0400 Subject: [PATCH 23/31] Declare the translation-unit dependency of the shared-pointer regression (cherry picked from commit 3327240fb254cd3f14416c722c4a02b37d94d4f9) --- rocq-brick-libstdcpp/proof/shared_ptr/fractional_copy.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/fractional_copy.v b/rocq-brick-libstdcpp/proof/shared_ptr/fractional_copy.v index 21c6d6b5..86e88a5e 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/fractional_copy.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/fractional_copy.v @@ -40,7 +40,7 @@ Section with_cpp. ). Lemma copy_then_destroy_ok : verify[source] copy_then_destroy_spec. - Proof. + Proof using MOD. verify_spec. go. iExists pieceid. From cc13f844983912a985e1863389fced15afd80fdd Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Thu, 29 Oct 2026 13:19:38 -0400 Subject: [PATCH 24/31] docs(shared_ptr): state concurrency limits and update regression comments PR: https://github.com/SkyLabsAI/brick-libcpp/pull/10 --- rocq-brick-libstdcpp/proof/shared_ptr/specs.v | 7 ++++++- rocq-brick-libstdcpp/proof/shared_ptr/test.v | 5 +++-- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v index 59c217eb..ce52faa9 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v @@ -21,7 +21,12 @@ 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. -Because BRiCk only supports SC atomics, the proof only works as if the stdlib implementation used SC atomics or had sufficient barriers (the actual defn of SharedPtrR will be different in that case due to limitations on invariants in weak memory reasoning). +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. diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/test.v b/rocq-brick-libstdcpp/proof/shared_ptr/test.v index 51697cc5..f2079f52 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/test.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/test.v @@ -138,7 +138,9 @@ Set Default Goal Selector "!". go. Qed. - (* dummy spec: needs fix *) + (* 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 emp \post{p:ptr}[Vptr p] Exists payload sid, @@ -202,7 +204,6 @@ Set Default Goal Selector "!". iExists tt. iExists (fun _ => emp). go. - (* TODO: proof needs rework after alloc.tokenR transition. *) repeat rewrite arrayR_cons. go. normalize_ptrs. From 787bc979b7e828472ac6334457fabaff08dc97ff Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Thu, 29 Oct 2026 20:39:04 -0400 Subject: [PATCH 25/31] Prove an executable shared-pointer inheritance exclusion checker Decide the complete exported base graph with a finite worklist. Reject missing and opaque declarations instead of accepting an unknown hierarchy. Use the boolean in make_shared; defer automatic hints and dedicated checker cases as requested. PR: https://github.com/SkyLabsAI/brick-libcpp/pull/10 --- .../proof/shared_ptr/make_shared.v | 34 +-- .../proof/shared_ptr/make_shared_test.v | 4 +- .../proof/shared_ptr/no_esft.v | 259 ++++++++++++++++++ rocq-brick-libstdcpp/proof/shared_ptr/specs.v | 1 + 4 files changed, 263 insertions(+), 35 deletions(-) create mode 100644 rocq-brick-libstdcpp/proof/shared_ptr/no_esft.v diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/make_shared.v b/rocq-brick-libstdcpp/proof/shared_ptr/make_shared.v index f2efabfc..c27b376d 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/make_shared.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/make_shared.v @@ -34,38 +34,6 @@ Import linearity. Section with_cpp. Context `{Sigma : cpp_logic, MOD : inc_shared_ptr_cpp.source ⊧ σ}. - Definition make_shared_no_esft (ty : type) : Prop := - match erase_qualifiers ty with - | Tnamed cls => forall path base, - class_derives cls path -> base ∈ cls :: path -> - forall pack, - base <> Ninst "std::enable_shared_from_this" pack /\ - base <> Ninst "std::__enable_shared_from_this" pack - | _ => True - end. - - Lemma make_shared_no_esft_no_bases cls layout : - glob_def σ 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) -> - make_shared_no_esft (Tnamed cls). - Proof. - intros Hlayout Hbases Hname path base Hpath Hin pack. - inversion Hpath; subst. - { apply elem_of_cons in Hin. destruct Hin as [-> | Hin]. - { apply Hname. } - { inversion Hin. } } - { match goal with - | H : _ !! cls = Some (Gstruct ?st) |- _ => - change (glob_def σ cls = Some (Gstruct st)) in H; - rewrite Hlayout in H; injection H as Heq; subst st - end. - match goal with - | H : _ ∈ layout.(s_bases) |- _ => rewrite Hbases in H; inversion H - end. } - Qed. - (** 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 @@ -114,7 +82,7 @@ Section with_cpp. \pre [| pack = map Atype args |] \pre [| parameter_types = map (trv_ref QM) args |] \pre [| length values = length args |] - \pre [| make_shared_no_esft ty |] + \pre [| shared_ptr_no_esftb ty = true |] \pre [| match erase_qualifiers ty with | Tarray _ _ | Tincomplete_array _ => False | _ => True diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/make_shared_test.v b/rocq-brick-libstdcpp/proof/shared_ptr/make_shared_test.v index 2204dbef..cb641e79 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/make_shared_test.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/make_shared_test.v @@ -44,9 +44,9 @@ Section with_cpp. #[local] Instance learn_shared : LearnEq6 SharedPtrR := ltac:(solve_learnable). - Lemma payload_no_esft : make_shared_no_esft "Payload". + Lemma payload_no_esft : shared_ptr_no_esftb "Payload" = true. Proof using MOD. - eapply make_shared_no_esft_no_bases. + eapply shared_ptr_no_esft_no_bases. { eapply (@glob_def_genv_compat_struct σ "Payload"%cpp_name source MOD). vm_compute. reflexivity. } { reflexivity. } 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/specs.v b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v index ce52faa9..6c389b42 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v @@ -59,6 +59,7 @@ 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. From 8b2b39b5699a603c6324f8149603d892c0e65c9f Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Thu, 29 Oct 2026 20:39:04 -0400 Subject: [PATCH 26/31] Guard raw shared-pointer adoption against weak-handle initialization Require shared_ptr_no_esftb in init_ctor, matching make_shared. Framing payload ownership unchanged is invalid when adoption initializes enable_shared_from_this. Array adoption is unchanged because it skips that initialization. PR: https://github.com/SkyLabsAI/brick-libcpp/pull/10 --- rocq-brick-libstdcpp/proof/shared_ptr/specs.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v index 6c389b42..6d92da71 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v @@ -1,5 +1,5 @@ (** Specs of shared_ptr. -We do not cover interaction with weak_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 @@ -254,6 +254,9 @@ Section specs. specify {| info_name := (Nscoped ("std::shared_ptr".<>) (Nctor [Tptr ty])).<> ; info_type := tCtor ("std::shared_ptr".<>) [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 From b5a487ac292094df90b3e97d6d3c4e051e3f5dd0 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Thu, 29 Oct 2026 20:39:32 -0400 Subject: [PATCH 27/31] Require managed-array bounds for shared_ptr subscript Tie the subscript index to the complete managed array type recorded by the control block. Port both indexed writes in the existing array client. PR: https://github.com/SkyLabsAI/brick-libcpp/pull/10 --- rocq-brick-libstdcpp/proof/shared_ptr/specs.v | 2 ++ rocq-brick-libstdcpp/proof/shared_ptr/test.v | 6 ++++++ 2 files changed, 8 insertions(+) diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v index 6d92da71..f13aa750 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v @@ -406,6 +406,8 @@ Section specs. \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. diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/test.v b/rocq-brick-libstdcpp/proof/shared_ptr/test.v index f2079f52..67ff0c99 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/test.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/test.v @@ -198,6 +198,12 @@ Set Default Goal Selector "!". go. normalize_ptrs. go. + iExists 2%N. + go. + iExists 2%N. + go. + normalize_ptrs. + go. iExists true. go. iExists nullptr. From 4bf0fb3411063b28550785f48cc7c57cd43a7c9d Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Thu, 29 Oct 2026 20:39:32 -0400 Subject: [PATCH 28/31] Replace unrestricted payload redistribution with a proved migration Require equivalent whole ownership, every live handle and unused right, and explicit invariant modality conditions. Retire the old ghost invariant and allocate a new protocol while preserving all physical handles, allocations, and the count. Prove a non-pointwise partition exchange regression for an equality-ordered SC index; add no axioms. PR: https://github.com/SkyLabsAI/brick-libcpp/pull/10 --- .../proof/shared_ptr/redistribution.v | 357 ++++++++++++++++++ .../proof/shared_ptr/redistribution_test.v | 84 +++++ rocq-brick-libstdcpp/proof/shared_ptr/specs.v | 21 +- 3 files changed, 449 insertions(+), 13 deletions(-) create mode 100644 rocq-brick-libstdcpp/proof/shared_ptr/redistribution.v create mode 100644 rocq-brick-libstdcpp/proof/shared_ptr/redistribution_test.v 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..e4543d7b --- /dev/null +++ b/rocq-brick-libstdcpp/proof/shared_ptr/redistribution.v @@ -0,0 +1,357 @@ +(** 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 + SharedPtrHandleR : sl_opacity. + + #[local] Lemma alloc_protocol control managed (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 |] ** + 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 |} + end. + unfold protocol_tokens, invariant_tokens, pieceRight, pieceHandle. + cbn [pieceRightLocs pieceHandleLocs dataLoc payload_type]. + 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_destructible (payload_type 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] 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) ** + (Exists kind, SharedAllocationR kind (payload_type id) (dataLoc id) p). + #[local] Hint Opaque counter_allocation : sl_opacity. + + #[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. + iExists t. 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. iExists t. 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_destructible (payload_type id) Rold |-- + payload_destructible (payload_type id) Rnew). + { unfold 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) 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. rewrite a2 a3. 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. + 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..de5b8a9b --- /dev/null +++ b/rocq-brick-libstdcpp/proof/shared_ptr/redistribution_test.v @@ -0,0 +1,84 @@ +(** 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, 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, SharedAllocationR, one_int_piece. + 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 index f13aa750..1d7a6ff4 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v @@ -40,7 +40,14 @@ The proof will atomically increment the counter to take out the Rpiece from the - 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. -- These specs in this file allow you to change the ownership split protocol (between the various shared_ptr objects protecting the same payload object ptr) later on (see lemma [redistributePayloadOwnership]), as long as the caller can cough up all pieces and objects associated with the payload (see [allPiecesAndObjs]). +- 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)). *) @@ -365,18 +372,6 @@ Section specs. Definition observeSharedTypeF q id pieceid t Rpiece op:= @observe_fwd _ _ _ (sharedR_typeptr_observe q id pieceid t Rpiece op). - Definition allPiecesAndObjs Rpiece id (ownedPtr: ptr) (pieceOut: nat->bool) : Rep := - ([∗ list] pieceid ∈ allPieceIds, - if pieceOut pieceid - then pureR (ownedPtr |-> Rpiece pieceid) - ** pureR (Exists (base:ptr), base |->SharedPtrR 1$m id pieceid Rpiece ownedPtr) - else pureR (pieceRight id pieceid)). - - Lemma redistributePayloadOwnership {Rpieceold Rpiecenew: nat -> Rep} (pieceOut : nat -> bool) id ownedPtr: - allPiecesAndObjs Rpieceold id ownedPtr pieceOut - |-- |={⊤}=> allPiecesAndObjs Rpiecenew id ownedPtr pieceOut. - Proof. Admitted. - End tty. Definition init_ctor_arr ety := From 062f1537f1418565af273f06d8e3491dc7f02c65 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Fri, 30 Oct 2026 17:50:11 -0400 Subject: [PATCH 29/31] Require the selected whole-delete capability for raw shared_ptr adoption Retain cleanup mode and allocation alignment through the control-block protocol and proved redistribution. Keep make_shared payload destruction separate from raw delete. Check class-specific scalar/array delete lookup and runtime effects; verify raw int clients against complete deletion obligations. PR: https://github.com/SkyLabsAI/brick-libcpp/pull/10 --- .../proof/shared_ptr/allocation.v | 5 +- .../proof/shared_ptr/allocation_test.v | 9 +- .../proof/shared_ptr/make_shared.v | 1 + .../proof/shared_ptr/redistribution.v | 36 +++-- .../proof/shared_ptr/redistribution_test.v | 10 +- rocq-brick-libstdcpp/proof/shared_ptr/specs.v | 128 +++++++++++++++--- .../proof/shared_ptr/test.cpp | 48 ++++++- rocq-brick-libstdcpp/proof/shared_ptr/test.v | 52 +++++-- 8 files changed, 235 insertions(+), 54 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/allocation.v b/rocq-brick-libstdcpp/proof/shared_ptr/allocation.v index 40dd2ac4..88ab278d 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/allocation.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/allocation.v @@ -64,13 +64,14 @@ Section with_cpp. .:: Nid "_M_storage"). Definition SharedAllocationR (kind : shared_allocation_kind) - (payload_ty : type) (control owned : ptr) : mpred := + (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 payload_alignment, + 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 => diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/allocation_test.v b/rocq-brick-libstdcpp/proof/shared_ptr/allocation_test.v index 5abf13be..083a56c2 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/allocation_test.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/allocation_test.v @@ -18,14 +18,13 @@ Section with_cpp. 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 + |-- 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), - <- (bi.exist_intro payload_alignment). + rewrite <- (bi.exist_intro control_alignment). go. Qed. @@ -35,7 +34,7 @@ Section with_cpp. 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) + |-- SharedAllocationR CombinedAllocation (Tnamed nm) None (root ,, o_base CU (shared_control_name CombinedAllocation (Tnamed nm)) SP_counted_base) owned. @@ -60,7 +59,7 @@ Section with_cpp. 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) + |-- SharedAllocationR CombinedAllocation (Tarray ety len) None (root ,, o_base CU cn SP_counted_base) owned. Proof. intros Hpayload Hcontrol Hbounds. diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/make_shared.v b/rocq-brick-libstdcpp/proof/shared_ptr/make_shared.v index c27b376d..1e5ce058 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/make_shared.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/make_shared.v @@ -93,6 +93,7 @@ Section with_cpp. \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. diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/redistribution.v b/rocq-brick-libstdcpp/proof/shared_ptr/redistribution.v index e4543d7b..4eae4b74 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/redistribution.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/redistribution.v @@ -80,13 +80,15 @@ Section redistribution. #[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 (out : nat -> bool) : + #[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 |] ** + 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. @@ -96,10 +98,10 @@ Section redistribution. 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 |} + dataLoc := control; payload_type := managed; payload_delete := cleanup |} end. unfold protocol_tokens, invariant_tokens, pieceRight, pieceHandle. - cbn [pieceRightLocs pieceHandleLocs dataLoc payload_type]. + 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). @@ -162,12 +164,13 @@ Section redistribution. [| delete_compat ty (payload_type id) /\ p <> nullptr /\ lengthN (pieceRightLocs id) = N.pos maxContention /\ lengthN (pieceHandleLocs id) = N.pos maxContention |] ** - payload_destructible (payload_type id) R ** + 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 -> @@ -219,8 +222,9 @@ Section redistribution. Qed. Definition counter_allocation id p count : mpred := dataLoc id ., (SP_counted_base .:: Nid "_M_use_count") |-> intR 1$m (Z.of_N count) ** - (Exists kind, SharedAllocationR kind (payload_type id) (dataLoc 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) -> @@ -256,7 +260,6 @@ Section redistribution. end. rewrite Hcount bool_decide_false; last lia. rewrite Hpieces. unfold counter_allocation. go. - iExists t. go. Qed. #[local] Lemma retired_protocol id R p : @@ -282,7 +285,7 @@ Section redistribution. (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. iExists t. go. + setoid_rewrite Hpiece. go. Qed. (** Repartitioning requires every live handle and every unused acquisition @@ -312,9 +315,12 @@ Section redistribution. intros Hi Hout Hwhole. assert (Hlive : (0 < countLN out allPieceIds)%N). { eapply countLN_positive_of_member; eauto. } - assert (Hdestruct : payload_destructible (payload_type id) Rold |-- - payload_destructible (payload_type id) Rnew). - { unfold payload_destructible. setoid_rewrite <- Hwhole. reflexivity. } + 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))). @@ -333,14 +339,16 @@ Section redistribution. (|={⊤ ∖ ↑nroot,⊤}=> emp)%I). go. iExists t. go. wapply Hrepartition. go. - wapply (alloc_protocol (dataLoc id) (payload_type id) out). 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. rewrite a2 a3. reflexivity. } + { unfold counter_allocation, 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)). @@ -349,7 +357,7 @@ Section redistribution. 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. + unfold protocol_knowledge. rewrite a3 Hcleanup. wapply Hdestruct. go. Qed. End redistribution. diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/redistribution_test.v b/rocq-brick-libstdcpp/proof/shared_ptr/redistribution_test.v index de5b8a9b..c46ccb6d 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/redistribution_test.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/redistribution_test.v @@ -41,8 +41,9 @@ Section tests. Example int_partition_timeless id p q n : Timeless (Exists out, sptrInv id (fun _ => intR q n) p out). Proof. - unfold sptrInv, pieceRight, pieceHandle, SharedAllocationR. - apply _. + unfold sptrInv, pieceRight, pieceHandle, payload_allocation. + destruct (payload_delete id) as [[op alignment]|]; + unfold SharedAllocationR; apply _. Qed. End tests. @@ -74,8 +75,9 @@ Section sc_test. Proof. intros Hlive Hout. eapply redistributePayloadOwnership with (live := live). - { unfold sptrInv, pieceRight, pieceHandle, SharedAllocationR, one_int_piece. - apply _. } + { 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. } diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v index 1d7a6ff4..e06c517c 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v @@ -11,12 +11,21 @@ We cover the following usage: block. For the supported libstdc++ ABI it is [INT_MAX], not the pointer-sized unsigned maximum; see the definition below. -The init constructor requires [payload_destructible]: collecting every payload -piece must suffice to run the managed object's destruction. This persistent -capability becomes part of [SharedPtrR]. Unlike a plain entailment to [anyR], -it allows ghost updates before destruction and accounts for nontrivial member -destructors. It must be supplied by the constructor's caller, not assumed as -an unconditional property of arbitrary payload predicates. +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 @@ -53,6 +62,7 @@ A common pattern where this can be useful is when the thread that calls new need *) 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. @@ -83,6 +93,9 @@ Record CtrlBlockId : Set := 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. @@ -120,6 +133,36 @@ 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])).<>, + 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. @@ -135,6 +178,49 @@ Section specs. 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. + + #[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). @@ -178,9 +264,7 @@ Section specs. else (dataLoc id) ., (SP_counted_base .:: Nid "_M_use_count") |-> intR 1$m (Z.of_N ctrVal) - ** (Exists kind : shared_allocation_kind, - SharedAllocationR kind (payload_type id) - (dataLoc id) ownedPtr) + ** payload_allocation id ownedPtr ** ([∗ list] pieceid ∈ allPieceIds, if pieceOut pieceid then emp else ownedPtr |-> Rpiece pieceid)). @@ -209,10 +293,10 @@ Section specs. Definition SharedPtrR (q : cQp.t) (id: CtrlBlockId) (pieceid : nat) (Rpiece : nat -> Rep) (ownedPtr:ptr) : Rep := SharedPtrHandleR ty q ownedPtr (dataLoc id) - (* This is managed-type compatibility, not permission to delete ownedPtr. - The allocation case inside sptrInv determines what can be deallocated. *) + (* 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_destructible (payload_type id) Rpiece) + ** pureR (payload_releasable id Rpiece) ** [| ownedPtr<>nullptr |] (* use NullSharedPtr otherwise *) ** [| lengthN (pieceRightLocs id) = Npos maxContention |] ** [| lengthN (pieceHandleLocs id) = Npos maxContention |] @@ -237,7 +321,8 @@ Section specs. #[local] Definition SharedPtrHandleR_const_C := [CANCEL] SharedPtrHandleR_const. - #[local] Hint Opaque pieceHandle payload_destructible sptrInv : sl_opacity. + #[local] Hint Opaque pieceHandle payload_releasable payload_allocation + 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)) @@ -274,11 +359,14 @@ Section specs. (* ^ 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 p |-> alloc.tokenR ty 1%Qp + \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_destructible ty Rpiece + \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 *) @@ -383,11 +471,14 @@ Section specs. 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 p |-> alloc.tokenR ty 1%Qp + \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_destructible ty Rpiece + \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 *) @@ -414,7 +505,8 @@ Section specs. : sl_opacity. End specs. -#[global] Hint Opaque SharedPtrR NullSharedPtrR payload_destructible : sl_opacity. +#[global] Hint Opaque SharedPtrR NullSharedPtrR payload_destructible + payload_deletable payload_releasable payload_allocation : sl_opacity. #[global] Hint Resolve SharedPtrR_const_C NullSharedPtrR_const_C : sl_opacity. #[global] Hint Resolve observeSharedTypeF : sl_opacity. diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/test.cpp b/rocq-brick-libstdcpp/proof/shared_ptr/test.cpp index ea5015b5..cfef48c9 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/test.cpp +++ b/rocq-brick-libstdcpp/proof/shared_ptr/test.cpp @@ -12,4 +12,50 @@ std::shared_ptr testsharedarr() { 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 p(::new ClassDelete); + } + if (scalar_deletions != 1 || array_deletions != 0) return 1; + { + std::shared_ptr p(::new ClassDelete[2]); + } + if (scalar_deletions != 1 || array_deletions != 1) return 2; + { + std::shared_ptr p = std::make_shared(); + std::shared_ptr a = std::make_shared(2); + } + if (scalar_deletions != 1 || array_deletions != 1) return 3; + return 0; +} + +void test_shared_copy_empty(std::shared_ptr const& source) { + std::shared_ptr copy(source); +} + +#ifdef SHARED_PTR_DELETE_EFFECTS_TEST +int main() { + std::shared_ptr 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 index 67ff0c99..4f4736bb 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/test.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/test.v @@ -12,6 +12,36 @@ 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. @@ -61,7 +91,7 @@ Section proofs. cpp.spec "testshared1()" as testshared1spec with ( - \pre emp + \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 @@ -109,18 +139,19 @@ Set Default Goal Selector "!". 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 : emp |-- payload_destructible "int" Rpiece). + assert (Hdestroy : denoteModule source ** operator_delete_size |-- + payload_deletable "int" "operator delete(void*, unsigned long)" None Rpiece). { unfold Rpiece. - unfold payload_destructible, allPieceIds. + unfold payload_deletable, allPieceIds. rewrite -> seqprefix with (prelen:=1%nat) by lia. simpl. setoid_rewrite (allButFirstEmp "int"). go. - rewrite destroy_val_wp_destroy_val. - go. } rewrite <- Hdestroy. go. @@ -142,7 +173,7 @@ Set Default Goal Selector "!". 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 emp + \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 @@ -169,19 +200,20 @@ Set Default Goal Selector "!". go. eagerUnifyU. go. + iExists source. + iExists "operator delete[](void*)"%cpp_name. rewrite <- _at_big_sepL. unfold allButFirstPieceId. rewrite allButFirstEmp. go. - assert (Hdestroy : emp |-- payload_destructible "int[2]" Rpiece). + assert (Hdestroy : denoteModule source ** operator_delete_array |-- + payload_deletable "int[2]" "operator delete[](void*)" None Rpiece). { unfold Rpiece. - unfold payload_destructible, allPieceIds. + unfold payload_deletable, allPieceIds. rewrite -> seqprefix with (prelen:=1%nat) by lia. simpl. setoid_rewrite (allButFirstEmp "int[2]"). go. - rewrite destroy_val_wp_destroy_val. - go. } rewrite <- Hdestroy. go. From b5d03853016907ae8e58df985cd2d81e1c1e3177 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Fri, 30 Oct 2026 17:50:11 -0400 Subject: [PATCH 30/31] Register one shared_ptr copy spec covering empty and live handles Derive the null and nonnull specializations from the common contract. Prove fractional copy-and-destroy clients for both branches through ordinary spec discovery, without a null-only registered assumption. PR: https://github.com/SkyLabsAI/brick-libcpp/pull/10 --- .../proof/shared_ptr/fractional_copy.v | 23 +++++++- rocq-brick-libstdcpp/proof/shared_ptr/specs.v | 52 ++++++++++++++++--- 2 files changed, 67 insertions(+), 8 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/fractional_copy.v b/rocq-brick-libstdcpp/proof/shared_ptr/fractional_copy.v index 86e88a5e..423897fc 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/fractional_copy.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/fractional_copy.v @@ -43,12 +43,33 @@ Section with_cpp. Proof using MOD. verify_spec. go. - iExists pieceid. + 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&)" + 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. *) diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v index e06c517c..660e4076 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v @@ -409,6 +409,25 @@ Section specs. 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) @@ -418,18 +437,37 @@ Section specs. \post p|->Rpiece pieceid ** this |-> SharedPtrR 1$m id pieceid Rpiece p. - Definition SpecFor_copy_ctor := RegisterSpec copy_ctor. - #[global] Existing Instance SpecFor_copy_ctor. - - (** Copy-ctor from null: produces another null shared_ptr. - No token is required. TODO: unify this spec with the spec above, using dependent types, as done in the destructor spec *) 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 := @@ -500,7 +538,7 @@ Section specs. #[global] Existing Instance SpecFor_subscript. #[global] Hint Opaque - init_ctor move_ctor dtor_spec copy_ctor copy_ctor_null + init_ctor move_ctor dtor_spec copy_ctor copy_ctor_nonnull copy_ctor_null deref arrow init_ctor_arr subscript : sl_opacity. From b75080712cfc8fbf76095dce27a6c6306bd6e986 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Sun, 1 Nov 2026 19:02:21 -0500 Subject: [PATCH 31/31] Retain physical shared-pointer control-block ownership Keep the implicit weak counter and an abstract layout remainder once in the shared invariant. Preserve that ownership during ghost-ID redistribution and check its exclusivity. The layout predicate and its Timeless law are explicit assumed library interfaces; no library-body correctness is claimed. Intended upstream destination: https://github.com/SkyLabsAI/brick-libcpp/pull/10 (not yet published). --- .../proof/shared_ptr/allocation.v | 53 +++++++++++++++++-- .../proof/shared_ptr/allocation_test.v | 24 ++++++++- .../proof/shared_ptr/redistribution.v | 4 +- rocq-brick-libstdcpp/proof/shared_ptr/specs.v | 37 +++++++++---- 4 files changed, 102 insertions(+), 16 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/allocation.v b/rocq-brick-libstdcpp/proof/shared_ptr/allocation.v index 88ab278d..837bf9e0 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/allocation.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/allocation.v @@ -1,6 +1,7 @@ (** Allocation ownership for the default libstdc++ shared-pointer constructors. - This is only the allocation part of the control-block invariant: it does - not own the payload fields or the reference counters. + [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 @@ -53,6 +54,51 @@ Definition shared_control_name (kind : shared_allocation_kind) 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. *) @@ -105,4 +151,5 @@ Section with_cpp. end. End with_cpp. -#[global] Hint Opaque SharedAllocationR : sl_opacity. +#[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 index 083a56c2..627224fa 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/allocation_test.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/allocation_test.v @@ -7,11 +7,33 @@ Require Import skylabs.brick.libstdcpp.shared_ptr.allocation. Set Default Goal Selector "!". Set Warnings "+sl-transparent-constants". -Import linearity. +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) : diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/redistribution.v b/rocq-brick-libstdcpp/proof/shared_ptr/redistribution.v index 4eae4b74..aa143b69 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/redistribution.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/redistribution.v @@ -222,6 +222,7 @@ Section redistribution. 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. @@ -346,7 +347,8 @@ Section redistribution. { 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, payload_allocation. rewrite a2 a3 b0. reflexivity. } + { 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. diff --git a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v index 660e4076..82dc6341 100644 --- a/rocq-brick-libstdcpp/proof/shared_ptr/specs.v +++ b/rocq-brick-libstdcpp/proof/shared_ptr/specs.v @@ -208,6 +208,18 @@ Section specs. 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. @@ -264,6 +276,7 @@ Section specs. 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)). @@ -276,15 +289,17 @@ Section specs. that state by [pieceHandle_live] in [handle_liveness.v]. This also permits closing the invariant before running a reentrant destructor. - This remains a partial control-block model for the assumed library - specs, not a verified libstdc++ implementation. It now retains the - appropriate allocation ownership in [SharedAllocationR]. - A complete body proof must additionally own the remaining control-block - fields and dynamic-class witnesses, account for its implicit weak - reference, and justify the actual acquire/release operations. For an - array factory it must also connect _M_n/_S_tail to the retained allocation - size and recover the padding for deallocation. No external weak_ptr - operations are covered by this interface. *) + [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. *) @@ -321,7 +336,7 @@ Section specs. #[local] Definition SharedPtrHandleR_const_C := [CANCEL] SharedPtrHandleR_const. - #[local] Hint Opaque pieceHandle payload_releasable payload_allocation + #[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 : @@ -544,7 +559,7 @@ Section specs. End specs. #[global] Hint Opaque SharedPtrR NullSharedPtrR payload_destructible - payload_deletable payload_releasable payload_allocation : sl_opacity. + 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.