From 9520c870d5d643a0dc6c61eb8a3d1671756e586c Mon Sep 17 00:00:00 2001 From: Jasper Haag Date: Wed, 14 Oct 2026 16:59:21 -0400 Subject: [PATCH 1/3] feat(vector): specs for erase, iterator operator+ and const conversion Specify `vector::erase(const_iterator)` and `erase(const_iterator, const_iterator)`: neither reallocates, so the base pointer is unchanged, the size drops by the number of erased elements, the later elements keep their values, and the result points at the first element after the erased ones. Clients also need the iterator's `operator+(difference_type) const`, which, like `operator++`, does not check bounds yet, and the converting constructor from `iterator` to `const_iterator`. TestErase names its iterators before converting or comparing them, as TestIntIter does: binding a temporary iterator to a const reference needs wp_make_const on the locked iterator representation, which automation does not do. erase_ub_proof.v shows that `erase(end())` gets stuck on `1 < 1`. Co-Authored-By: Claude Opus 5.5 (1M context) --- rocq-brick-libstdcpp/proof/vector/spec.v | 88 +++++++++++++++ rocq-brick-libstdcpp/test/dune.inc | 12 ++ rocq-brick-libstdcpp/test/vector/erase_ub.cpp | 22 ++++ .../test/vector/erase_ub_proof.expected | 106 ++++++++++++++++++ .../test/vector/erase_ub_proof.v | 35 ++++++ rocq-brick-libstdcpp/test/vector/test.cpp | 28 +++++ .../test/vector/test_cpp_proof.v | 13 +++ 7 files changed, 304 insertions(+) create mode 100644 rocq-brick-libstdcpp/test/vector/erase_ub.cpp create mode 100644 rocq-brick-libstdcpp/test/vector/erase_ub_proof.expected create mode 100644 rocq-brick-libstdcpp/test/vector/erase_ub_proof.v diff --git a/rocq-brick-libstdcpp/proof/vector/spec.v b/rocq-brick-libstdcpp/proof/vector/spec.v index 5e0e2a44..351a087e 100644 --- a/rocq-brick-libstdcpp/proof/vector/spec.v +++ b/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 <>, 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 <> to <>, + 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. + (** <> + + , + ("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 (take (Z.to_nat i) xs ++ drop (Z.to_nat 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. + + (** <> + + ("[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 (take (Z.to_nat i) xs ++ drop (Z.to_nat 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 ** diff --git a/rocq-brick-libstdcpp/test/dune.inc b/rocq-brick-libstdcpp/test/dune.inc index 88118bf7..51e0f8d2 100644 --- a/rocq-brick-libstdcpp/test/dune.inc +++ b/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) diff --git a/rocq-brick-libstdcpp/test/vector/erase_ub.cpp b/rocq-brick-libstdcpp/test/vector/erase_ub.cpp new file mode 100644 index 00000000..1d87fb0c --- /dev/null +++ b/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 + +void erase_end() { + std::vector v; + v.push_back(1); + std::vector::iterator e = v.end(); + std::vector::const_iterator last = e; + v.erase(last); +} diff --git a/rocq-brick-libstdcpp/test/vector/erase_ub_proof.expected b/rocq-brick-libstdcpp/test/vector/erase_ub_proof.expected new file mode 100644 index 00000000..f71136be --- /dev/null +++ b/rocq-brick-libstdcpp/test/vector/erase_ub_proof.expected @@ -0,0 +1,106 @@ +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 + _H_0 : 0 < 0 + 1 + _H_1 : 0 ≤ 0 + 1 + _H_2 : list.ListSizeZ [1] (0 + 1 - 0) + _p_ : ptr + ============================ + _ : denoteModule source + _ : std.vector.iterator.iter_to_const "int" "std::allocator" + _ : std.vector.default_ctor "int" "std::allocator" + _ : std.vector.ctor_with_alloc "int" "std::allocator" + _ : std.vector.sized_ctor "int" "std::allocator" + _ : std.vector.init_ctor "int" "std::allocator" + _ : std.vector.copy_alloc_ctor "int" "std::allocator" + _ : std.vector.move_alloc_ctor "int" "std::allocator" + _ : std.vector.copy_ctor "int" "std::allocator" + _ : std.vector.move_ctor "int" "std::allocator" + _ : std.vector.dtor "int" "std::allocator" + _ : std.vector.subscript "int" "std::allocator" true + _ : std.vector.subscript "int" "std::allocator" false + _ : std.vector.push_back_copy "int" "std::allocator" + _ : std.vector.push_back_move "int" "std::allocator" + _ : std.vector.pop_back "int" "std::allocator" + _ : std.vector.front "int" "std::allocator" true + _ : std.vector.front "int" "std::allocator" false + _ : std.vector.back "int" "std::allocator" true + _ : std.vector.back "int" "std::allocator" false + _ : std.vector.clear "int" "std::allocator" + _ : std.vector.erase_one "int" "std::allocator" + _ : std.vector.erase_range "int" "std::allocator" + _ : std.vector.resize_default "int" "std::allocator" + _ : std.vector.resize "int" "std::allocator" + _ : std.vector.size "int" "std::allocator" + _ : std.vector.begin_spec "int" "std::allocator" true + _ : std.vector.begin_spec "int" "std::allocator" false + _ : std.vector.end_spec "int" "std::allocator" true + _ : std.vector.end_spec "int" "std::allocator" false + _ : std.vector.iterator.iter_default_ctor false "int" "std::allocator" + _ : std.vector.iterator.iter_copy_ctor false "int" "std::allocator" + _ : std.vector.iterator.iter_dtor false "int" "std::allocator" + _ : std.vector.iterator.iter_move_assign false "int" "std::allocator" + _ : std.vector.iterator.iter_deref false "int" "std::allocator" + _ : std.vector.iterator.iter_op_post_inc false "int" "std::allocator" + _ : std.vector.iterator.iter_op_pre_inc false "int" "std::allocator" + _ : std.vector.iterator.iter_op_plus false "int" "std::allocator" + _ : std.vector.iterator.iter_op_eq false "int" "std::allocator" + _ : std.vector.iterator.iter_op_ne false "int" "std::allocator" + _ : std.vector.iterator.iter_default_ctor true "int" "std::allocator" + _ : std.vector.iterator.iter_copy_ctor true "int" "std::allocator" + _ : std.vector.iterator.iter_dtor true "int" "std::allocator" + _ : std.vector.iterator.iter_move_assign true "int" "std::allocator" + _ : std.vector.iterator.iter_deref true "int" "std::allocator" + _ : std.vector.iterator.iter_op_post_inc true "int" "std::allocator" + _ : std.vector.iterator.iter_op_pre_inc true "int" "std::allocator" + _ : std.vector.iterator.iter_op_plus true "int" "std::allocator" + _ : std.vector.iterator.iter_op_eq true "int" "std::allocator" + _ : std.vector.iterator.iter_op_ne true "int" "std::allocator" + _ : std.allocator.ctor "int" + _ : std.allocator.dtor "int" + _ : type_ptr "std::vector>" v_addr + _ : type_ptr "int" (std.vector.base_pointer st' .[ "int" ! 0 ]) + _ : type_ptr + "__gnu_cxx::__normal_iterator>>" + e_addr + _ : type_ptr + "__gnu_cxx::__normal_iterator>>" + last_addr + _ : type_ptr + "__gnu_cxx::__normal_iterator>>" + 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" 1$m (1 - 1) st' ∗ + pureR + (std.vector.base_pointer st' + |-> array_sliceR "int" 0 (1 - 1) (λ v : Z, intR 1$m v) + (take (Z.to_nat 1) [1] ++ drop (Z.to_nat 1 + 1) [1]))) -∗ + ::interp + { FreeTemps.delete + "__gnu_cxx::__normal_iterator>>" + p >*> + 1 } diff --git a/rocq-brick-libstdcpp/test/vector/erase_ub_proof.v b/rocq-brick-libstdcpp/test/vector/erase_ub_proof.v new file mode 100644 index 00000000..03b31b47 --- /dev/null +++ b/rocq-brick-libstdcpp/test/vector/erase_ub_proof.v @@ -0,0 +1,35 @@ +(* + * 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 ( + \prepost std.vector.specs "int" (std.allocator.T "int") + \prepost std.vector.iterator.specs false "int" (std.allocator.T "int") + \prepost std.vector.iterator.specs true "int" (std.allocator.T "int") + \prepost std.vector.iterator.iter_to_const "int" (std.allocator.T "int") + \prepost std.allocator.specs "int" + \post emp). + Lemma erase_end_ok : verify[source] erase_end_spec. + Proof. + verify_spec. + rewrite /std.vector.specs /std.vector.iterator.specs /std.allocator.specs. + go. Show. Fail Qed. + Abort. +End with_cpp. diff --git a/rocq-brick-libstdcpp/test/vector/test.cpp b/rocq-brick-libstdcpp/test/vector/test.cpp index 9a69ec1f..e03b97b9 100644 --- a/rocq-brick-libstdcpp/test/vector/test.cpp +++ b/rocq-brick-libstdcpp/test/vector/test.cpp @@ -98,6 +98,33 @@ 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 v; + v.push_back(1); + v.push_back(2); + v.push_back(3); + vector::iterator b = v.begin(); + vector::const_iterator first = b; + auto it = v.erase(first); + test(*it == 2); + test(v.size() == 2); + vector::iterator b1 = v.begin() + 1; + vector::const_iterator last = b1; + auto it1 = v.erase(last); + auto e1 = v.end(); + test(it1 == e1); + vector::iterator b2 = v.begin(); + vector::iterator e2 = v.end(); + vector::const_iterator f2 = b2; + vector::const_iterator l2 = e2; + v.erase(f2, l2); + test(v.size() == 0); +} + int main() { TestBasic(); @@ -105,5 +132,6 @@ main() { TestIntIter(); TestForEach(); TestAllocCtor(); + TestErase(); return 0; } diff --git a/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v b/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v index 91b979d7..648aca3a 100644 --- a/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v +++ b/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) From e5a2d182ef69c68e1a412c75534db61db4bbf2c1 Mon Sep 17 00:00:00 2001 From: Jasper Haag Date: Thu, 22 Oct 2026 17:34:00 -0400 Subject: [PATCH 2/3] refactor(vector): use takeZ/dropZ in erase specs; drop explicit preposts in erase_ub test The erase_ub test picks up the registered specs without listing them, so the recorded goal now only shows the specs it uses. Co-Authored-By: Claude Opus 5.5 --- rocq-brick-libstdcpp/proof/vector/spec.v | 4 +- .../test/vector/erase_ub_proof.expected | 52 ++----------------- .../test/vector/erase_ub_proof.v | 9 +--- 3 files changed, 8 insertions(+), 57 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/vector/spec.v b/rocq-brick-libstdcpp/proof/vector/spec.v index 351a087e..188a269c 100644 --- a/rocq-brick-libstdcpp/proof/vector/spec.v +++ b/rocq-brick-libstdcpp/proof/vector/spec.v @@ -740,7 +740,7 @@ NES.Begin std. \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 (take (Z.to_nat i) xs ++ drop (Z.to_nat i + 1) xs). + 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. @@ -766,7 +766,7 @@ NES.Begin std. \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 (take (Z.to_nat i) xs ++ drop (Z.to_nat j) xs). + 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. diff --git a/rocq-brick-libstdcpp/test/vector/erase_ub_proof.expected b/rocq-brick-libstdcpp/test/vector/erase_ub_proof.expected index f71136be..c0a970cd 100644 --- a/rocq-brick-libstdcpp/test/vector/erase_ub_proof.expected +++ b/rocq-brick-libstdcpp/test/vector/erase_ub_proof.expected @@ -18,57 +18,15 @@ _p_ : ptr ============================ _ : denoteModule source - _ : std.vector.iterator.iter_to_const "int" "std::allocator" _ : std.vector.default_ctor "int" "std::allocator" - _ : std.vector.ctor_with_alloc "int" "std::allocator" - _ : std.vector.sized_ctor "int" "std::allocator" - _ : std.vector.init_ctor "int" "std::allocator" - _ : std.vector.copy_alloc_ctor "int" "std::allocator" - _ : std.vector.move_alloc_ctor "int" "std::allocator" - _ : std.vector.copy_ctor "int" "std::allocator" - _ : std.vector.move_ctor "int" "std::allocator" _ : std.vector.dtor "int" "std::allocator" - _ : std.vector.subscript "int" "std::allocator" true - _ : std.vector.subscript "int" "std::allocator" false - _ : std.vector.push_back_copy "int" "std::allocator" - _ : std.vector.push_back_move "int" "std::allocator" - _ : std.vector.pop_back "int" "std::allocator" - _ : std.vector.front "int" "std::allocator" true - _ : std.vector.front "int" "std::allocator" false - _ : std.vector.back "int" "std::allocator" true - _ : std.vector.back "int" "std::allocator" false - _ : std.vector.clear "int" "std::allocator" - _ : std.vector.erase_one "int" "std::allocator" - _ : std.vector.erase_range "int" "std::allocator" - _ : std.vector.resize_default "int" "std::allocator" - _ : std.vector.resize "int" "std::allocator" - _ : std.vector.size "int" "std::allocator" - _ : std.vector.begin_spec "int" "std::allocator" true - _ : std.vector.begin_spec "int" "std::allocator" false - _ : std.vector.end_spec "int" "std::allocator" true _ : std.vector.end_spec "int" "std::allocator" false - _ : std.vector.iterator.iter_default_ctor false "int" "std::allocator" - _ : std.vector.iterator.iter_copy_ctor false "int" "std::allocator" - _ : std.vector.iterator.iter_dtor false "int" "std::allocator" - _ : std.vector.iterator.iter_move_assign false "int" "std::allocator" - _ : std.vector.iterator.iter_deref false "int" "std::allocator" - _ : std.vector.iterator.iter_op_post_inc false "int" "std::allocator" - _ : std.vector.iterator.iter_op_pre_inc false "int" "std::allocator" - _ : std.vector.iterator.iter_op_plus false "int" "std::allocator" - _ : std.vector.iterator.iter_op_eq false "int" "std::allocator" - _ : std.vector.iterator.iter_op_ne false "int" "std::allocator" - _ : std.vector.iterator.iter_default_ctor true "int" "std::allocator" + _ : std.vector.erase_one "int" "std::allocator" _ : std.vector.iterator.iter_copy_ctor true "int" "std::allocator" _ : std.vector.iterator.iter_dtor true "int" "std::allocator" - _ : std.vector.iterator.iter_move_assign true "int" "std::allocator" - _ : std.vector.iterator.iter_deref true "int" "std::allocator" - _ : std.vector.iterator.iter_op_post_inc true "int" "std::allocator" - _ : std.vector.iterator.iter_op_pre_inc true "int" "std::allocator" - _ : std.vector.iterator.iter_op_plus true "int" "std::allocator" - _ : std.vector.iterator.iter_op_eq true "int" "std::allocator" - _ : std.vector.iterator.iter_op_ne true "int" "std::allocator" - _ : std.allocator.ctor "int" - _ : std.allocator.dtor "int" + _ : std.vector.iterator.iter_dtor false "int" "std::allocator" + _ : std.vector.iterator.iter_to_const "int" "std::allocator" + _ : std.vector.push_back_move "int" "std::allocator" _ : type_ptr "std::vector>" v_addr _ : type_ptr "int" (std.vector.base_pointer st' .[ "int" ! 0 ]) _ : type_ptr @@ -98,7 +56,7 @@ pureR (std.vector.base_pointer st' |-> array_sliceR "int" 0 (1 - 1) (λ v : Z, intR 1$m v) - (take (Z.to_nat 1) [1] ++ drop (Z.to_nat 1 + 1) [1]))) -∗ + (takeZ 1 [1] ++ dropZ (1 + 1) [1]))) -∗ ::interp { FreeTemps.delete "__gnu_cxx::__normal_iterator>>" diff --git a/rocq-brick-libstdcpp/test/vector/erase_ub_proof.v b/rocq-brick-libstdcpp/test/vector/erase_ub_proof.v index 03b31b47..53a0290d 100644 --- a/rocq-brick-libstdcpp/test/vector/erase_ub_proof.v +++ b/rocq-brick-libstdcpp/test/vector/erase_ub_proof.v @@ -19,17 +19,10 @@ Require Import skylabs.brick.libstdcpp.test.vector.erase_ub_cpp. Section with_cpp. Context `{Σ : cpp_logic} {σ : genv}. - cpp.spec "erase_end()" from source as erase_end_spec with ( - \prepost std.vector.specs "int" (std.allocator.T "int") - \prepost std.vector.iterator.specs false "int" (std.allocator.T "int") - \prepost std.vector.iterator.specs true "int" (std.allocator.T "int") - \prepost std.vector.iterator.iter_to_const "int" (std.allocator.T "int") - \prepost std.allocator.specs "int" - \post emp). + 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. - rewrite /std.vector.specs /std.vector.iterator.specs /std.allocator.specs. go. Show. Fail Qed. Abort. End with_cpp. From 3c5ed503885715f10afdc9378e050de52175600c Mon Sep 17 00:00:00 2001 From: Jasper Haag Date: Fri, 23 Oct 2026 09:25:13 -0400 Subject: [PATCH 3/3] fix: repair .expected output after rebasing on main --- rocq-brick-libstdcpp/test/vector/erase_ub_proof.expected | 3 --- 1 file changed, 3 deletions(-) diff --git a/rocq-brick-libstdcpp/test/vector/erase_ub_proof.expected b/rocq-brick-libstdcpp/test/vector/erase_ub_proof.expected index c0a970cd..e4e51190 100644 --- a/rocq-brick-libstdcpp/test/vector/erase_ub_proof.expected +++ b/rocq-brick-libstdcpp/test/vector/erase_ub_proof.expected @@ -12,9 +12,6 @@ e_addr, last_addr, p : ptr GUARDS : GWs.GUARDS _x_ : valid<"int"> 1 - _H_0 : 0 < 0 + 1 - _H_1 : 0 ≤ 0 + 1 - _H_2 : list.ListSizeZ [1] (0 + 1 - 0) _p_ : ptr ============================ _ : denoteModule source