more explanation about init_ctor spec

Author: aa755

rocq-brick-libcpp/proof/shared_ptr/specs.v

@@ -108,6 +108,9 @@ Section specs.
             ; info_type := tCtor ("std::shared_ptr".<<Atype ty>>) [Tptr ty] |} (fun (this:ptr) =>
     \arg{p:ptr} "ownedPtr" (Vptr p)
     \pre{p} dynAllocatedR ty p
+    (* 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. 
+       We frame away the 0th piece in this spec. A derived spec can be proven where that framing away is not done *)
     \pre{Rpiece: nat -> Rep} [∗ list] ctid ∈ allButFirstPieceId,
       p |-> Rpiece ctid
     \pre [|([∗ list] ctid ∈ allPieceIds, Rpiece ctid)