Extend specifications for [new] for array forms

rocq-brick-libstdcpp/proof/dune.inc

@@ -26,6 +26,15 @@
   	 (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 new
+ (rule
+  (targets inc_new_cpp.v.stderr inc_new_cpp.v)
+  (alias test_ast)
+  (deps (:input inc_new.cpp) (glob_files_rec ../*.hpp) (universe))
+  (action
+  	 (with-stderr-to inc_new_cpp.v.stderr (run cpp2v -v %{input} -o inc_new_cpp.v  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps inc_new.cpp))
+)
 (subdir semaphore
  (rule
   (targets inc_hpp.v.stderr inc_hpp.v)

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

@@ -0,0 +1,280 @@
+Require Import bluerock.auto.cpp.proof.
+Require Export bluerock.brick.libstdcpp.new.spec.
+
+#[only(lazy_unfold(global))] derive alloc.tokenR.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic} {σ : genv}.
+
+  (** ** Hints for proving [alloc.token] from [new_token.R].
+
+     - <<_using_>> hints rely on [size_of _ ty = Some ...] to already be provable, while non
+       <<using>> hints introduce this fact and have higher hint cost.
+       This fact is otherwise lost because it is expressed within [alloc.token].
+     - <<_0>> lemmas special case for non-array allocations which are common and ensure that
+       the allocation overhead at the C++ level is 0. (Allocation overhead of the allocator-level is
+       separately captured in [allocatedR].)
+   *)
+  #[program]
+  Definition token_prove_using_C (p : ptr) q storage_p overhead ty sz
+    (_ : size_of _ ty = Some sz) :=
+    \cancelx
+    \consuming p |-> new_token.R q (new_token.mk ty storage_p overhead)
+    \proving p |-> alloc.tokenR ty q
+    \through storage_p .[ Tbyte ! -overhead ] |-> allocatedR q (overhead + sz)
+    \end.
+  Next Obligation.
+    rewrite alloc.tokenR.unlock. work.
+  Qed.
+
+  #[program]
+  Definition token_prove_C (p : ptr) q storage_p overhead ty :=
+    \cancelx
+    \consuming p |-> new_token.R q (new_token.mk ty storage_p overhead)
+    \proving p |-> alloc.tokenR ty q
+    \deduce{sz} [| size_of _ ty = Some sz |]
+    \through storage_p .[ Tbyte ! -overhead ] |-> allocatedR q (overhead + sz)
+    \end.
+  Next Obligation.
+    intros; iIntros "X".
+    iDestruct (observe [| exists sz, size_of _ _ = _ |] with "X") as "%".
+    destruct H; simpl in *.
+    rewrite alloc.tokenR.unlock. iDestruct "X" as "?"; work.
+  Qed.
+
+  (* special cases for the above two hints when the overhead is 0 *)
+  #[program]
+  Definition token_prove_using_0_C (p : ptr) q storage_p ty sz
+    (_ : size_of _ ty = Some sz) :=
+    \cancelx
+    \consuming p |-> new_token.R q (new_token.mk ty storage_p 0)
+    \proving p |-> alloc.tokenR ty q
+    \through storage_p |-> allocatedR q sz
+    \end.
+  Next Obligation.
+    rewrite alloc.tokenR.unlock. work.
+    normalize_ptrs. iStopProof; f_equiv. f_equiv. lia.
+  Qed.
+
+  #[program]
+  Definition token_prove_0_C (p : ptr) q storage_p ty :=
+    \cancelx
+    \consuming p |-> new_token.R q (new_token.mk ty storage_p 0)
+    \proving p |-> alloc.tokenR ty q
+    \deduce{sz} [| size_of _ ty = Some sz |]
+    \through storage_p |-> allocatedR q sz
+    \end.
+  Next Obligation.
+    intros; iIntros "X".
+    iDestruct (observe [| exists sz, size_of _ _ = _ |] with "X") as "%".
+    destruct H; simpl in *.
+    rewrite alloc.tokenR.unlock. iDestruct "X" as "?"; work.
+    normalize_ptrs. iStopProof; f_equiv; f_equiv; lia.
+  Qed.
+
+
+  (** ** Hints for proving [new_token.R] *)
+  #[program]
+  Definition token_use_non_array_C (p : ptr) ty q (_ : TCEq (is_array_type ty) false) :=
+    \cancelx
+    \consuming p |-> alloc.tokenR (σ:=σ) ty q
+    \proving{(storage_p : ptr) overhead} p |-> new_token.R q (new_token.mk ty storage_p overhead)
+    \deduce{(storage_p' : ptr) sz} [| size_of _ ty = Some sz |]
+    \deduce storage_p' |-> allocatedR q sz
+    \through [| storage_p = storage_p' |]
+    \through [| overhead = 0 |]%N
+    \end.
+  Next Obligation.
+    intros.
+    rewrite alloc.tokenR.unlock.
+    iIntros "X"; iDestruct "X" as (????) "[X ?]".
+    iDestruct (observe [| overhead = 0%N |] with "X") as "%".
+    subst. normalize_ptrs.
+    iExists storage_p.
+    iDestruct "X" as "?".
+    work.
+  Qed.
+
+  #[program]
+  Definition token_use_array_C (p : ptr) ty q :=
+    \cancelx
+    \consuming p |-> alloc.tokenR (σ:=σ) ty q
+    \proving{(storage_p : ptr) overhead} p |-> new_token.R q (new_token.mk ty storage_p overhead)
+    \deduce{(storage_p' : ptr) (overhead' : N) sz} [| size_of _ ty = Some sz |]
+    \deduce storage_p' .[ Tbyte ! -overhead' ] |-> allocatedR q (overhead' + sz)
+    \through [| storage_p = storage_p' |]
+    \through [| overhead = overhead' |]%N
+    \end.
+  Next Obligation.
+    rewrite alloc.tokenR.unlock. work.
+    iExists storage_p.
+    work.
+    iExists overhead. work.
+  Qed.
+
+  #[global] Instance alloc_token_new_token_learnable ty q q' a b c :
+    Learnable (alloc.tokenR ty q) (new_token.R q' (new_token.mk a b c)) [ty = a].
+  Proof. solve_learnable. Qed.
+  #[global] Instance allocatedR_learn : Cbn (Learn (any ==> learn_eq ==> learn_hints.fin) allocatedR).
+  Proof. solve_learnable. Qed.
+
+  #[global] Instance token_learn : Cbn (Learn (learn_eq ==> learn_eq ==> any ==> learn_hints.fin) alloc.tokenR).
+  Proof. solve_learnable. Qed.
+
+  (** <<delete nullptr>> hints
+      The needs for hints at that AST level is sub-optimal, but something that requires
+      a bit more infrastructure to automate. Specifically, [wp_delete_null] reduces to
+      a conjunction which requires splitting the proof. However, this split can be
+      avoided if <<operator delete(nullptr, ...)>> is effectively a no-op (as its
+      specification says that it should be). A better phrasing of this might be a class
+      like [TrivialOnNull function_name] which would allow us to generalize these proofs.
+   *)
+  #[program]
+  Definition wp_delete_null_operator_delete_size_C module cls Q
+    (Hdelete : delete_operator.delete_for module "operator delete(void*, unsigned long)" cls =[Vm]=> Some ("operator delete(void*, unsigned long)"%cpp_name, delete_operator.mk None true false))
+    {sz} (Hsizeof : sizeof._size_of module cls =[Vm]=> Some sz)
+    :=
+    \cancelx
+    \using operator_delete_size
+    \using denoteModule module
+    \proving wp_delete_null "operator delete(void*, unsigned long)" cls Q
+    \through Q
+    \end.
+  Next Obligation.
+    intros * Hdel * Hsize.
+    rewrite wp_delete_null.unlock.
+    iIntros "[#? #M] ?".
+    iDestruct (observe [| _ ⊧ _ |] with "M") as "%".
+    inversion Hdel.
+    erewrite delete_operator.delete_for_submodule;
+      [ | eassumption
+      | apply genv_compat_submodule; eauto ].
+    work. inversion Hsize as [Hx]; clear Hsize.
+    rewrite wp_invoke_delete.unlock; simpl.
+    work.
+    rewrite /delete_operator.type_for/=.
+    iApply invoke.use_cptrR; eauto; eauto.
+    simpl.
+    go.
+  Qed.
+
+  #[program]
+  Definition wp_delete_null_operator_delete_C module cls Q
+    (Hdelete : delete_operator.delete_for module "operator delete(void* )" cls =[Vm]=> Some ("operator delete(void* )"%cpp_name, delete_operator.mk None false false))
+    {sz} (Hsizeof : sizeof._size_of module cls =[Vm]=> Some sz)
+    :=
+    \cancelx
+    \using operator_delete
+    \using denoteModule module
+    \proving wp_delete_null "operator delete(void* )" cls Q
+    \through Q
+    \end.
+  Next Obligation.
+    intros * Hdel * Hsize.
+    rewrite wp_delete_null.unlock.
+    iIntros "[#? #M] ?".
+    iDestruct (observe [| _ ⊧ _ |] with "M") as "%".
+    inversion Hdel.
+    erewrite delete_operator.delete_for_submodule;
+      [ | eassumption
+      | apply genv_compat_submodule; eauto ].
+    work. inversion Hsize as [Hx]; clear Hsize.
+    rewrite wp_invoke_delete.unlock; simpl.
+    work.
+    rewrite /delete_operator.type_for/=.
+    iApply invoke.use_cptrR; eauto; eauto.
+    simpl.
+    go.
+  Qed.
+
+  #[program]
+  Definition wp_delete_null_operator_delete_array_size_C module cls Q
+    (Hdelete : delete_operator.delete_for module "operator delete[](void*, unsigned long)" (Tincomplete_array cls) =[Vm]=> Some ("operator delete[](void*, unsigned long)"%cpp_name, delete_operator.mk None true false))
+    {sz} (Hsizeof : sizeof._size_of module cls =[Vm]=> Some sz)
+    :=
+    \cancelx
+    \using operator_delete_array_size
+    \using denoteModule module
+    \proving wp_delete_null "operator delete[](void*, unsigned long)" (Tincomplete_array cls) Q
+    \through Q
+    \end.
+  Next Obligation.
+    intros * Hdel * Hsize.
+    rewrite wp_delete_null.unlock.
+    iIntros "[#? #M] ?".
+    iDestruct (observe [| _ ⊧ _ |] with "M") as "%".
+    inversion Hdel.
+    erewrite delete_operator.delete_for_submodule;
+      [ | eassumption
+      | apply genv_compat_submodule; eauto ].
+    work. inversion Hsize as [Hx]; clear Hsize.
+    rewrite wp_invoke_delete.unlock; simpl.
+    work.
+    iApply invoke.use_cptrR; eauto; eauto.
+    simpl. go.
+  Qed.
+
+  #[program]
+  Definition wp_delete_null_operator_delete_array_C module cls Q
+    (Hdelete : delete_operator.delete_for module "operator delete[](void* )" (Tincomplete_array cls) =[Vm]=> Some ("operator delete[](void* )"%cpp_name, delete_operator.mk None false false))
+    {sz} (Hsizeof : sizeof._size_of module cls =[Vm]=> Some sz)
+    :=
+    \cancelx
+    \using operator_delete_array
+    \using denoteModule module
+    \proving wp_delete_null "operator delete[](void* )" (Tincomplete_array cls) Q
+    \through Q
+    \end.
+  Next Obligation.
+    intros * Hdel * Hsize.
+    rewrite wp_delete_null.unlock.
+    iIntros "[#? #M] ?".
+    iDestruct (observe [| _ ⊧ _ |] with "M") as "%".
+    inversion Hdel.
+    erewrite delete_operator.delete_for_submodule;
+      [ | eassumption
+      | apply genv_compat_submodule; eauto ].
+    work. inversion Hsize as [Hx]; clear Hsize.
+    rewrite wp_invoke_delete.unlock; simpl.
+    work.
+    iApply invoke.use_cptrR; eauto; eauto.
+    go.
+  Qed.
+
+  #[program]
+  Definition wp_delete_null_operator_delete_fixed_array_C module cls array_size Q
+    (Hdelete : delete_operator.delete_for module "operator delete[](void*, unsigned long)" (Tarray cls array_size) =[Vm]=> Some ("operator delete[](void*, unsigned long)"%cpp_name, delete_operator.mk None true false))
+    {sz} (Hsizeof : sizeof._size_of module cls =[Vm]=> Some sz)
+    :=
+    \cancelx
+    \using operator_delete_array_size
+    \using denoteModule module
+    \proving wp_delete_null "operator delete[](void*, unsigned long)" (Tarray cls array_size) Q
+    \through Q
+    \end.
+  Next Obligation.
+    intros * Hdel * Hsize.
+    rewrite wp_delete_null.unlock.
+    iIntros "[#? #M] ?".
+    iDestruct (observe [| _ ⊧ _ |] with "M") as "%".
+    inversion Hdel.
+    erewrite delete_operator.delete_for_submodule;
+      [ | eassumption
+      | apply genv_compat_submodule; eauto ].
+    work. inversion Hsize as [Hx]; clear Hsize.
+    rewrite wp_invoke_delete.unlock; simpl.
+    work.
+    iApply invoke.use_cptrR; eauto; eauto.
+    go.
+  Qed.
+
+End with_cpp.
+
+#[global] Hint Resolve wp_delete_null_operator_delete_size_C wp_delete_null_operator_delete_C : db_bluerock_wp.
+#[global] Hint Resolve wp_delete_null_operator_delete_array_C wp_delete_null_operator_delete_array_size_C
+ wp_delete_null_operator_delete_fixed_array_C : db_bluerock_wp.
+
+#[global] Hint Resolve token_prove_C token_prove_0_C | 100 : br_opacity.
+#[global] Hint Resolve token_prove_using_C token_prove_using_0_C | 99 : br_opacity.
+#[global] Hint Resolve token_use_non_array_C | 99 : br_opacity.
+#[global] Hint Resolve token_use_array_C | 100 : br_opacity.

rocq-brick-libstdcpp/proof/new/inc_new.cpp

@@ -0,0 +1 @@
+#include <new>

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

@@ -0,0 +1,87 @@
+Require Import iris.proofmode.tactics.
+Require Import bluerock.auto.cpp.prelude.pred.
+Require Import bluerock.auto.cpp.elpi.derive.bi.
+Require Import bluerock.brick.libstdcpp.new.inc_new_cpp.
+#[local] Set Primitive Projections.
+
+cpp.enum "std::align_val_t" from source alias.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, source ⊧ σ}.
+
+  (** The ownership of the allocator data structures.
+
+   This would include ownership such as free lists and allocator data structures.
+   In C++, these are generally ambient, so this is exposed as a predicate
+   rather than a representation predicate.
+
+   NOTE/TODO: The current interface exposes but does **not** use `allocatorP`,
+   because doing so would effectively require
+   threading this ownership everywhere which is not very ergonomic; however,
+   formally, this makes the interface un-realizable.
+
+   More investigation is needed to understand how to encapsulate this ownership
+   (and other ownership like it). The most promising option to date is to use
+   thread-local invariants, but this still introduces some level of verbosity.
+   *)
+  Parameter allocatorP : forall {σ : genv}, Qp -> mpred.
+  #[only(fractional,fracvalid)] derive allocatorP.
+
+  (** The allocation meta-data **owned by the allocator**.
+
+      In a normal implementation of <<malloc>>, this is a few bytes before the
+      returned pointer that stores meta data, e.g. the size of the allocation.
+
+      NOTE: While C++ often stores the size of the array next to a dynamically
+      allocated array, the memory that backs this is **not** part of [allocatedR].
+      That memory is owned by the C++ abstract machine.
+   *)
+  Parameter allocatedR : forall {σ : genv}, Qp -> N -> Rep.
+  #[only(fractional,asfractional,fracvalid,timeless)] derive allocatedR.
+  #[global] Instance: Cbn (Learn (any ==> learn_eq ==> learn_hints.fin) allocatedR).
+  Proof. solve_learnable. Qed.
+
+End with_cpp.
+
+NES.Begin alloc.
+
+  (** [token ty sz q] bundles the dynamic allocation tokens provided by
+      the C++ abstract machine with the [allocatedR] fact from the allocation library.
+   *)
+  br.lock
+  Definition tokenR `{Σ : cpp_logic} {σ : genv} (ty : type) (q : Qp) : Rep :=
+    Exists storage_p overhead sz,
+      [| size_of _ ty = Some sz |] **
+      new_token.R q {| new_token.alloc_ty := ty ; new_token.storage_ptr := storage_p ; new_token.overhead := overhead |} **
+      pureR (storage_p .[ "unsigned char" ! -overhead ] |-> allocatedR q (overhead + sz)).
+  #[only(fractional,asfractional,fracvalid,timeless)] derive new_token.R.
+  #[only(fracvalid,timeless)] derive tokenR.
+
+  #[local] Open Scope string_scope. (* for IPM *)
+  #[global] Instance tokenR_xxx `{Σ : cpp_logic} {σ : genv} ty
+    : Fractional (tokenR ty).
+  Proof.
+    rewrite tokenR.unlock.
+    repeat first [ apply _
+                 | apply fractional_exist; intros ].
+    { apply observe_2_sep_l.
+      apply observe_2_only_provable_impl.
+      congruence. }
+    { apply observe_2_exist; intros.
+      apply observe_2_sep_r, observe_2_sep_l.
+      iIntros "A B".
+      iDestruct (observe_2 [| _ = _ |] with "A B") as "%".
+      inversion H; eauto. }
+    { do 2 (apply observe_2_exist; intros).
+      apply observe_2_sep_r, observe_2_sep_l.
+      iIntros "A B".
+      iDestruct (observe_2 [| _ = _ |] with "A B") as "%".
+      inversion H; eauto. }
+  Qed.
+  (* We should be able to derive this, but <<derive>> gets stuck trying to prove the above instance
+  #[only(asfractional)] derive tokenR.
+   *)
+
+   #[global] Instance tokenR_asfractional `{Σ : cpp_logic} {σ : genv} (ty : type) (q : Qp) : AsFractional (tokenR ty q) (tokenR ty) q.
+  Proof. solve_as_frac. Qed.
+NES.End alloc.