feat(vector): specs for data, empty

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

@@ -770,6 +770,40 @@ NES.Begin std.
         Definition SpecFor_erase_range := RegisterSpec erase_range.
         #[global] Existing Instance SpecFor_erase_range.
 
+        (** <<bool empty() const noexcept;>>
+
+            <https://eel.is/c++draft/container.reqmts> -- whether <<size() == 0>>.
+            Total: it only reads the spine. *)
+        Definition empty :=
+          let qf := function_qualifiers.Nc in
+          specify.template.method vector "empty" qf Tbool [] $
+            \this this
+            \with q size st
+            \prepost this |-> spineR q size st
+            \post[Vbool (bool_decide (size = 0))] emp.
+        #[global] Hint Opaque empty : sl_opacity.
+        #[global] Arguments empty : simpl never.
+        Definition SpecFor_empty := RegisterSpec empty.
+        #[global] Existing Instance SpecFor_empty.
+
+        (** <<T* data() noexcept;>> and <<const T* data() const noexcept;>>
+
+            <https://eel.is/c++draft/vector.data> -- the base pointer of the
+            elements, which is null for a vector that never allocated. Total;
+            using the result needs ownership of the elements, as with
+            <<operator[]>>. *)
+        Definition data c :=
+          let qf := function_qualifiers.mk c false Prvalue in
+          specify.template.method vector "data" qf (Tptr (Tconst_if c ty)) [] $
+            \this this
+            \with q size st
+            \prepost this |-> spineR q size st
+            \post[Vptr (base_pointer st)] emp.
+        #[global] Hint Opaque data : sl_opacity.
+        #[global] Arguments data : simpl never.
+        Definition SpecFor_data := RegisterSpec data.
+        #[global] Existing Instance SpecFor_data.
+
         Definition size `{!IsAllocator alloc_ty} :=
           let qf := function_qualifiers.Nc in
           specify.template.method vector "size" qf size_type [] $
@@ -857,6 +891,8 @@ NES.Begin std.
           resize_default **
           resize **
           size **
+          empty **
+          MaybeConst data **
           MaybeConst begin_spec **
           MaybeConst end_spec.
         #[global] Hint Opaque specs : typeclass_instances sl_opacity.

rocq-brick-libstdcpp/test/dune.inc

@@ -395,6 +395,18 @@
   	 (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps test.cpp))
 )
+(subdir vector
+ (rule
+  (targets data_ub_cpp.v.stderr data_ub_cpp.v)
+  (alias test_ast)
+  (deps
+   (:input data_ub.cpp)
+   (env_var CPP2V_DOCKER_ENABLED)
+   (glob_files_rec ../*.hpp))
+  (action
+  	 (with-stderr-to data_ub_cpp.v.stderr (run cpp2v -v %{input} -o data_ub_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps data_ub.cpp))
+)
 (subdir vector
  (rule
   (targets erase_ub_cpp.v.stderr erase_ub_cpp.v)

rocq-brick-libstdcpp/test/vector/data_ub.cpp

@@ -0,0 +1,26 @@
+/*
+ * Copyright (c) 2026 SkyLabs AI, Inc.
+ * This software is distributed under the terms of the BedRock Open-Source License.
+ * See the LICENSE-BedRock file in the repository root for details.
+ */
+// Accesses through vector::data() outside the elements.
+//
+// These are undefined behavior: data() points to the vector's elements
+// ([vector.data]), and reading past them is an out-of-bounds access
+// ([expr.add]/4), as is dereferencing the null data() of an empty vector
+// ([expr.unary.op]/1). ASan reports both.
+// data_ub_proof.v shows that the vector specs reject each one;
+// data_ub_proof.expected records where the proofs get stuck.
+// Their UB-free twins are in TestDataEmpty in test.cpp.
+#include <vector>
+
+int data_past_end() {
+    std::vector<int> v;
+    v.push_back(1);
+    return v.data()[v.size()];
+}
+
+int data_empty() {
+    std::vector<int> v;
+    return *v.data();
+}

rocq-brick-libstdcpp/test/vector/data_ub_proof.expected

@@ -0,0 +1,124 @@
+1 goal
+
+  thread_info : biIndex
+  _Σ : gFunctors
+  Σ : cpp_logic thread_info _Σ
+  σ : genv
+  _H_ : source ⊧ σ
+  _PostPred_ : ptr → mpred
+  PostCond : PostCondition
+  v_addr : ptr
+  st' : std.vector.InternalState
+  GUARDS : GWs.GUARDS
+  _x_ : valid<"int"> 1
+  _H_0 : 0 ≤ 0 + 1
+  _H_1 : list.ListSizeZ [1] (0 + 1 - 0)
+  _H_2 : 0 < 0 + 1
+  p : ptr
+  ============================
+  _ : denoteModule source
+  _ : std.vector.default_ctor "int" "std::allocator<int>"
+  _ : std.vector.ctor_with_alloc "int" "std::allocator<int>"
+  _ : std.vector.sized_ctor "int" "std::allocator<int>"
+  _ : std.vector.init_ctor "int" "std::allocator<int>"
+  _ : std.vector.copy_alloc_ctor "int" "std::allocator<int>"
+  _ : std.vector.move_alloc_ctor "int" "std::allocator<int>"
+  _ : std.vector.copy_ctor "int" "std::allocator<int>"
+  _ : std.vector.move_ctor "int" "std::allocator<int>"
+  _ : std.vector.dtor "int" "std::allocator<int>"
+  _ : std.vector.subscript "int" "std::allocator<int>" true
+  _ : std.vector.subscript "int" "std::allocator<int>" false
+  _ : std.vector.push_back_copy "int" "std::allocator<int>"
+  _ : std.vector.push_back_move "int" "std::allocator<int>"
+  _ : std.vector.pop_back "int" "std::allocator<int>"
+  _ : std.vector.front "int" "std::allocator<int>" true
+  _ : std.vector.front "int" "std::allocator<int>" false
+  _ : std.vector.back "int" "std::allocator<int>" true
+  _ : std.vector.back "int" "std::allocator<int>" false
+  _ : std.vector.clear "int" "std::allocator<int>"
+  _ : std.vector.erase_one "int" "std::allocator<int>"
+  _ : std.vector.erase_range "int" "std::allocator<int>"
+  _ : std.vector.resize_default "int" "std::allocator<int>"
+  _ : std.vector.resize "int" "std::allocator<int>"
+  _ : std.vector.size "int" "std::allocator<int>"
+  _ : std.vector.empty "int" "std::allocator<int>"
+  _ : std.vector.data "int" "std::allocator<int>" true
+  _ : std.vector.data "int" "std::allocator<int>" false
+  _ : std.vector.begin_spec "int" "std::allocator<int>" true
+  _ : std.vector.begin_spec "int" "std::allocator<int>" false
+  _ : std.vector.end_spec "int" "std::allocator<int>" true
+  _ : std.vector.end_spec "int" "std::allocator<int>" false
+  _ : std.allocator.ctor "int"
+  _ : std.allocator.dtor "int"
+  _ : type_ptr "std::vector<int, std::allocator<int>>" v_addr
+  _ : std.vector.base_pointer st' |-> typed_sliceR "int" 0 (0 + 1)
+  _ : valid_ptr (std.vector.base_pointer st')
+  _ : validP<"int*"> (Vptr (std.vector.base_pointer st'))
+  --------------------------------------□
+  _ : PostCond
+  _ : std.vector.base_pointer st' .[ "int" ! 0 ] |-> intR 1$m 1
+  _ : v_addr
+      |-> std.vector.spineR "int" "std::allocator<int>" 1$m (0 + 1) st'
+  --------------------------------------∗
+  ∃ (v : val) (q : cQp.t),
+    std.vector.base_pointer st' .[ "int" ! 1 ] |-> primR "int" q v ∗
+    (std.vector.base_pointer st' .[ "int" ! 1 ] |-> primR "int" q v -∗
+     p |-> primR "int" 1$m v -∗ ::interp { (1 >*> 1) >*> (1 >*> 1) })
+1 goal
+
+  thread_info : biIndex
+  _Σ : gFunctors
+  Σ : cpp_logic thread_info _Σ
+  σ : genv
+  _H_ : source ⊧ σ
+  _PostPred_ : ptr → mpred
+  PostCond : PostCondition
+  v_addr : ptr
+  GUARDS : GWs.GUARDS
+  p : ptr
+  ============================
+  _ : denoteModule source
+  _ : std.vector.default_ctor "int" "std::allocator<int>"
+  _ : std.vector.ctor_with_alloc "int" "std::allocator<int>"
+  _ : std.vector.sized_ctor "int" "std::allocator<int>"
+  _ : std.vector.init_ctor "int" "std::allocator<int>"
+  _ : std.vector.copy_alloc_ctor "int" "std::allocator<int>"
+  _ : std.vector.move_alloc_ctor "int" "std::allocator<int>"
+  _ : std.vector.copy_ctor "int" "std::allocator<int>"
+  _ : std.vector.move_ctor "int" "std::allocator<int>"
+  _ : std.vector.dtor "int" "std::allocator<int>"
+  _ : std.vector.subscript "int" "std::allocator<int>" true
+  _ : std.vector.subscript "int" "std::allocator<int>" false
+  _ : std.vector.push_back_copy "int" "std::allocator<int>"
+  _ : std.vector.push_back_move "int" "std::allocator<int>"
+  _ : std.vector.pop_back "int" "std::allocator<int>"
+  _ : std.vector.front "int" "std::allocator<int>" true
+  _ : std.vector.front "int" "std::allocator<int>" false
+  _ : std.vector.back "int" "std::allocator<int>" true
+  _ : std.vector.back "int" "std::allocator<int>" false
+  _ : std.vector.clear "int" "std::allocator<int>"
+  _ : std.vector.erase_one "int" "std::allocator<int>"
+  _ : std.vector.erase_range "int" "std::allocator<int>"
+  _ : std.vector.resize_default "int" "std::allocator<int>"
+  _ : std.vector.resize "int" "std::allocator<int>"
+  _ : std.vector.size "int" "std::allocator<int>"
+  _ : std.vector.empty "int" "std::allocator<int>"
+  _ : std.vector.data "int" "std::allocator<int>" true
+  _ : std.vector.data "int" "std::allocator<int>" false
+  _ : std.vector.begin_spec "int" "std::allocator<int>" true
+  _ : std.vector.begin_spec "int" "std::allocator<int>" false
+  _ : std.vector.end_spec "int" "std::allocator<int>" true
+  _ : std.vector.end_spec "int" "std::allocator<int>" false
+  _ : std.allocator.ctor "int"
+  _ : std.allocator.dtor "int"
+  _ : type_ptr "std::vector<int, std::allocator<int>>" v_addr
+  _ : valid_ptr nullptr
+  _ : validP<"int*"> (Vptr nullptr)
+  --------------------------------------□
+  _ : PostCond
+  _ : v_addr |-> std.vector.R_null "int" "std::allocator<int>" 1$m
+  --------------------------------------∗
+  ∃ (v : val) (q : cQp.t), reference_to "int" nullptr ∗
+    nullptr |-> primR "int" q v ∗
+    (nullptr |-> primR "int" q v -∗
+     p |-> primR "int" 1$m v -∗ ::interp { 1 >*> 1 })

rocq-brick-libstdcpp/test/vector/data_ub_proof.v

@@ -0,0 +1,33 @@
+(*
+ * Copyright (c) 2026 SkyLabs AI, Inc.
+ * This software is distributed under the terms of the BedRock Open-Source License.
+ * See the LICENSE-BedRock file in the repository root for details.
+ *)
+Require Import skylabs.auto.cpp.prelude.proof.
+Require Import skylabs.brick.libstdcpp.allocator.spec.
+Require Import skylabs.brick.libstdcpp.vector.spec.
+
+Require Import skylabs.brick.libstdcpp.test.vector.data_ub_cpp.
+
+(** * The vector specs reject accesses through [data()] outside the elements
+
+    Each client in [data_ub.cpp] gets stuck reading an element that the vector
+    does not own; see data_ub_proof.expected. *)
+
+Section with_cpp.
+  Context `{Σ : cpp_logic} {σ : genv}.
+
+  cpp.spec "data_past_end()" from source as data_past_end_spec with (
+    \prepost std.vector.specs "int" (std.allocator.T "int")
+    \prepost std.allocator.specs "int"
+    \post{v}[Vint v] emp).
+  Lemma data_past_end_ok : verify[source] data_past_end_spec.
+  Proof. verify_spec; rewrite /std.vector.specs /std.allocator.specs; go. Show. Fail Qed. Abort.
+
+  cpp.spec "data_empty()" from source as data_empty_spec with (
+    \prepost std.vector.specs "int" (std.allocator.T "int")
+    \prepost std.allocator.specs "int"
+    \post{v}[Vint v] emp).
+  Lemma data_empty_ok : verify[source] data_empty_spec.
+  Proof. verify_spec; rewrite /std.vector.specs /std.allocator.specs; go. Show. Fail Qed. Abort.
+End with_cpp.

rocq-brick-libstdcpp/test/vector/test.cpp

@@ -125,6 +125,21 @@ TestErase() {
     test(v.size() == 0);
 }
 
+void
+TestDataEmpty() {
+    vector<int> v;
+    test(v.empty());
+    v.push_back(1);
+    v.push_back(2);
+    test(!v.empty());
+    int* p = v.data();
+    p[0] = 5;
+    test(v[0] == 5);
+    const vector<int>& cv = v;
+    test(cv.data() == p);
+    test(cv.data()[1] == 2);
+}
+
 int
 main() {
     TestBasic();
@@ -133,5 +148,6 @@ main() {
     TestForEach();
     TestAllocCtor();
     TestErase();
+    TestDataEmpty();
     return 0;
 }

rocq-brick-libstdcpp/test/vector/test_cpp_proof.v

@@ -188,6 +188,9 @@ Section with_cpp.
     cpp.spec "TestErase()" as test_erase with
         (\post emp).
 
+    cpp.spec "TestDataEmpty()" as test_data_empty with
+        (\post emp).
+
     cpp.spec "main()" as main with
         (\post[Vint 0] emp).
 
@@ -286,6 +289,14 @@ Section with_cpp.
     Definition test_erase_B := [LINK] test_erase_ok.
     #[local] Hint Resolve test_erase_B : sl_opacity.
 
+    Lemma test_data_empty_ok : verify[ source ] test_data_empty.
+    Proof using MOD.
+      verify_spec.
+      go.
+    Qed.
+    Definition test_data_empty_B := [LINK] test_data_empty_ok.
+    #[local] Hint Resolve test_data_empty_B : sl_opacity.
+
     Lemma test_ok : verify[ source ] test_spec.
     Proof using MOD.
       verify_spec.