feat(vector): specs for erase, iterator operator+ and const_iterator conversion

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

@@ -332,6 +332,40 @@ NES.Begin std.
         Definition iter_op_pre_inc_SpecFor := RegisterSpec iter_op_pre_inc.
         #[global] Existing Instance iter_op_pre_inc_SpecFor.
 
+        (** <<__normal_iterator operator+(difference_type n) const;>>
+
+            Like <<operator++>>, this does not check bounds yet (see the TODO
+            there). *)
+        Definition iter_op_plus const ty alloc_ty :=
+          let qf := function_qualifiers.mk true false Prvalue in
+          specify.template.op (N_base const ty alloc_ty) OOPlus qf (T_base const ty alloc_ty) [Tlong] $
+            \this this
+            \arg{n} "" (Vint n)
+            \with basep i
+            \prepost{q} this |-> R_base const ty alloc_ty q basep i
+            \post{rp}[Vptr rp] rp |-> R_base const ty alloc_ty 1$m basep (i + n).
+        #[global] Hint Opaque iter_op_plus : sl_opacity.
+        #[global] Arguments iter_op_plus : simpl never.
+        Definition iter_op_plus_SpecFor := RegisterSpec iter_op_plus.
+        #[global] Existing Instance iter_op_plus_SpecFor.
+
+        (** The converting constructor from <<iterator>> to <<const_iterator>>,
+            a constructor template of <<__normal_iterator>> in libstdc++. *)
+        Definition iter_to_const ty alloc_ty :=
+          let argty := Tref (Tconst (T_base false ty alloc_ty)) in
+          _global (Ninst (Nscoped (N_base true ty alloc_ty) (Nctor [argty]))
+                     [Atype (Tptr ty); Atype Tvoid])
+          |-> unmaterialized_specR (tCtor (N_base true ty alloc_ty) [argty]) (
+            \this this
+            \arg{otherp} "" (Vptr otherp)
+            \with basep i
+            \prepost{q} otherp |-> R_base false ty alloc_ty q basep i
+            \post this |-> R_base true ty alloc_ty 1$m basep i).
+        #[global] Hint Opaque iter_to_const : sl_opacity.
+        #[global] Arguments iter_to_const : simpl never.
+        Definition iter_to_const_SpecFor := RegisterSpec iter_to_const.
+        #[global] Existing Instance iter_to_const_SpecFor.
+
         Definition iter_op_eq const ty alloc_ty :=
           specify.template.static_op NS OOEqualEqual
               [Atype (Tptr (Tconst_if const ty)); Atype (vector.T ty alloc_ty)]
@@ -370,6 +404,7 @@ NES.Begin std.
           iter_deref const ty alloc_ty **
           iter_op_post_inc const ty alloc_ty **
           iter_op_pre_inc const ty alloc_ty **
+          iter_op_plus const ty alloc_ty **
           iter_op_eq const ty alloc_ty **
           iter_op_ne const ty alloc_ty.
         #[global] Hint Opaque specs : typeclass_instances sl_opacity.
@@ -686,6 +721,57 @@ NES.Begin std.
         Definition SpecFor_resize := RegisterSpec (@resize).
         #[global] Existing Instance SpecFor_resize.
 
+        (** <<iterator erase(const_iterator pos);>>
+
+            <https://eel.is/c++draft/vector.modifiers>,
+            <https://eel.is/c++draft/sequence.reqmts> ("q denotes a valid
+            dereferenceable constant iterator to a"): removes the element at
+            [pos] without reallocating, and returns an iterator to the element
+            after it. The later elements move down by move assignment, so each
+            keeps its value. *)
+        Definition erase_one :=
+          let qf := function_qualifiers.N in
+          specify.template.method vector "erase" qf (iterator.T_base false ty alloc_ty) [iterator.T_base true ty alloc_ty] $
+            \this this
+            \arg{posp} "" (Vptr posp)
+            \with size st xs i
+            \prepost posp |-> iterator.R_base true ty alloc_ty 1$m (base_pointer st) i
+            \require 0 ≤ i < size
+            \pre this |-> R_cap (cQp.m 1) size st xs
+            \post{rp}[Vptr rp]
+              rp |-> iterator.R_base false ty alloc_ty 1$m (base_pointer st) i **
+              this |-> R_cap (cQp.m 1) (size - 1) st (takeZ i xs ++ dropZ (i + 1) xs).
+        #[global] Hint Opaque erase_one : sl_opacity.
+        #[global] Arguments erase_one : simpl never.
+        Definition SpecFor_erase_one := RegisterSpec erase_one.
+        #[global] Existing Instance SpecFor_erase_one.
+
+        (** <<iterator erase(const_iterator first, const_iterator last);>>
+
+            <https://eel.is/c++draft/sequence.reqmts> ("[q1, q2) is a valid
+            range in a"): removes the elements in [first, last) without
+            reallocating, and returns an iterator to the element that followed
+            them. *)
+        Definition erase_range :=
+          let qf := function_qualifiers.N in
+          specify.template.method vector "erase" qf (iterator.T_base false ty alloc_ty)
+              [iterator.T_base true ty alloc_ty; iterator.T_base true ty alloc_ty] $
+            \this this
+            \arg{firstp} "" (Vptr firstp)
+            \arg{lastp} "" (Vptr lastp)
+            \with size st xs i j
+            \prepost firstp |-> iterator.R_base true ty alloc_ty 1$m (base_pointer st) i
+            \prepost lastp |-> iterator.R_base true ty alloc_ty 1$m (base_pointer st) j
+            \require 0 ≤ i ≤ j ∧ j ≤ size
+            \pre this |-> R_cap (cQp.m 1) size st xs
+            \post{rp}[Vptr rp]
+              rp |-> iterator.R_base false ty alloc_ty 1$m (base_pointer st) i **
+              this |-> R_cap (cQp.m 1) (size - (j - i)) st (takeZ i xs ++ dropZ j xs).
+        #[global] Hint Opaque erase_range : sl_opacity.
+        #[global] Arguments erase_range : simpl never.
+        Definition SpecFor_erase_range := RegisterSpec erase_range.
+        #[global] Existing Instance SpecFor_erase_range.
+
         Definition size `{!IsAllocator alloc_ty} :=
           let qf := function_qualifiers.Nc in
           specify.template.method vector "size" qf size_type [] $
@@ -768,6 +854,8 @@ NES.Begin std.
           MaybeConst front  **
           MaybeConst back **
           clear **
+          erase_one **
+          erase_range **
           resize_default **
           resize **
           size **

rocq-brick-libstdcpp/test/dune.inc

@@ -359,6 +359,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 erase_ub_cpp.v.stderr erase_ub_cpp.v)
+  (alias test_ast)
+  (deps
+   (:input erase_ub.cpp)
+   (env_var CPP2V_DOCKER_ENABLED)
+   (glob_files_rec ../*.hpp))
+  (action
+  	 (with-stderr-to erase_ub_cpp.v.stderr (run cpp2v -v %{input} -o erase_ub_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps erase_ub.cpp))
+)
 (subdir vector
  (rule
   (targets test_cpp.v.stderr test_cpp.v)

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

@@ -0,0 +1,22 @@
+/*
+ * 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.
+ */
+// A call to vector::erase with the past-the-end iterator.
+//
+// This is undefined behavior: erase(q) requires "q denotes a valid
+// dereferenceable constant iterator to a" ([sequence.reqmts]), and end() is
+// not dereferenceable. _GLIBCXX_DEBUG reports it; ASan does not.
+// erase_ub_proof.v shows that the erase spec in vector/spec.v rejects it;
+// erase_ub_proof.expected records where the proof gets stuck.
+// Its UB-free twin erases the last element in TestErase in test.cpp.
+#include <vector>
+
+void erase_end() {
+    std::vector<int> v;
+    v.push_back(1);
+    std::vector<int>::iterator e = v.end();
+    std::vector<int>::const_iterator last = e;
+    v.erase(last);
+}

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

@@ -0,0 +1,61 @@
+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
+  e_addr, last_addr, p : ptr
+  GUARDS : GWs.GUARDS
+  _x_ : valid<"int"> 1
+  _p_ : ptr
+  ============================
+  _ : denoteModule source
+  _ : std.vector.default_ctor "int" "std::allocator<int>"
+  _ : std.vector.dtor "int" "std::allocator<int>"
+  _ : std.vector.end_spec "int" "std::allocator<int>" false
+  _ : std.vector.erase_one "int" "std::allocator<int>"
+  _ : std.vector.iterator.iter_copy_ctor true "int" "std::allocator<int>"
+  _ : std.vector.iterator.iter_dtor true "int" "std::allocator<int>"
+  _ : std.vector.iterator.iter_dtor false "int" "std::allocator<int>"
+  _ : std.vector.iterator.iter_to_const "int" "std::allocator<int>"
+  _ : std.vector.push_back_move "int" "std::allocator<int>"
+  _ : type_ptr "std::vector<int, std::allocator<int>>" v_addr
+  _ : type_ptr "int" (std.vector.base_pointer st' .[ "int" ! 0 ])
+  _ : type_ptr
+        "__gnu_cxx::__normal_iterator<int*, std::vector<int, std::allocator<int>>>"
+        e_addr
+  _ : type_ptr
+        "__gnu_cxx::__normal_iterator<const int*, std::vector<int, std::allocator<int>>>"
+        last_addr
+  _ : type_ptr
+        "__gnu_cxx::__normal_iterator<const int*, std::vector<int, std::allocator<int>>>"
+        p
+  --------------------------------------□
+  _ : PostCond
+  _ : e_addr
+      |-> std.vector.iterator.R "int" 1$m (std.vector.base_pointer st') 1
+  _ : last_addr
+      |-> std.vector.iterator.R_const "int" 1$m (std.vector.base_pointer st')
+            1
+  --------------------------------------∗
+  [| 1 < 1 |] ∗
+  ∀ x : ptr,
+    p
+    |-> std.vector.iterator.R_const "int" 1$m (std.vector.base_pointer st') 1 ∗
+    x |-> std.vector.iterator.R "int" 1$m (std.vector.base_pointer st') 1 ∗
+    v_addr
+    |-> (std.vector.spineR "int" "std::allocator<int>" 1$m (1 - 1) st' ∗
+         pureR
+           (std.vector.base_pointer st'
+            |-> array_sliceR "int" 0 (1 - 1) (λ v : Z, intR 1$m v)
+                  (takeZ 1 [1] ++ dropZ (1 + 1) [1]))) -∗
+    ::interp
+      { FreeTemps.delete
+          "__gnu_cxx::__normal_iterator<const int*, std::vector<int, std::allocator<int>>>"
+          p >*>
+        1 }

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

@@ -0,0 +1,28 @@
+(*
+ * 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.erase_ub_cpp.
+
+(** * The vector [erase] spec rejects the past-the-end iterator
+
+    [erase_end] gets stuck on [1 < 1]; see erase_ub_proof.expected. *)
+
+(* As in test_cpp_proof.v. *)
+#[local] Instance SplitRecord_prod A B : SplitRecord (@prod A B) := {}.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic} {σ : genv}.
+
+  cpp.spec "erase_end()" from source as erase_end_spec with (\post emp).
+  Lemma erase_end_ok : verify[source] erase_end_spec.
+  Proof.
+    verify_spec.
+    go. Show. Fail Qed.
+  Abort.
+End with_cpp.

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

@@ -98,12 +98,40 @@ TestAllocCtor() {
     test(v.size() == 0);
 }
 
+// Iterators are named before they are converted or compared, as in
+// TestIntIter: binding a temporary iterator to a const reference needs
+// wp_make_const on the locked iterator representation.
+void
+TestErase() {
+    vector<int> v;
+    v.push_back(1);
+    v.push_back(2);
+    v.push_back(3);
+    vector<int>::iterator b = v.begin();
+    vector<int>::const_iterator first = b;
+    auto it = v.erase(first);
+    test(*it == 2);
+    test(v.size() == 2);
+    vector<int>::iterator b1 = v.begin() + 1;
+    vector<int>::const_iterator last = b1;
+    auto it1 = v.erase(last);
+    auto e1 = v.end();
+    test(it1 == e1);
+    vector<int>::iterator b2 = v.begin();
+    vector<int>::iterator e2 = v.end();
+    vector<int>::const_iterator f2 = b2;
+    vector<int>::const_iterator l2 = e2;
+    v.erase(f2, l2);
+    test(v.size() == 0);
+}
+
 int
 main() {
     TestBasic();
     TestAggregate();
     TestIntIter();
     TestForEach();
     TestAllocCtor();
+    TestErase();
     return 0;
 }

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

@@ -185,6 +185,9 @@ Section with_cpp.
     cpp.spec "TestAggregate()" as test_aggregate with
         (\post emp).
 
+    cpp.spec "TestErase()" as test_erase with
+        (\post emp).
+
     cpp.spec "main()" as main with
         (\post[Vint 0] emp).
 
@@ -275,6 +278,14 @@ Section with_cpp.
     Definition test_aggregate_B := [LINK] test_aggregate_ok.
     #[local] Hint Resolve test_aggregate_B : sl_opacity.
 
+    Lemma test_erase_ok : verify[ source ] test_erase.
+    Proof using MOD.
+      verify_spec.
+      go.
+    Qed.
+    Definition test_erase_B := [LINK] test_erase_ok.
+    #[local] Hint Resolve test_erase_B : sl_opacity.
+
     Lemma test_ok : verify[ source ] test_spec.
     Proof using MOD.
       verify_spec.
@@ -300,6 +311,8 @@ Section with_cpp.
           std.vector.specs "unsigned" alloc_uint **
           std.vector.iterator.specs true "unsigned" alloc_uint **
           std.vector.iterator.specs false "int" alloc_int **
+          std.vector.iterator.specs true "int" alloc_int **
+          std.vector.iterator.iter_to_const "int" alloc_int **
           std.find_spec (std.vector.iterator.T "int") "int" source **
           std.allocator.specs "int" **
           std.cassert.specs)