feat(vector): specs for `erase`, iterator `operator+` and `const_iterator` conversion by jhaag-skylabs-ai · Pull Request #219 · SkyLabsAI/brick-libcpp

jhaag-skylabs-ai · 2026-10-14T20:59:23Z

Specs for std::vector::erase (vector.modifiers, sequence.reqmts), plus the two iterator operations clients need to call it:

erase(const_iterator pos) requires 0 ≤ i < size ("q denotes a valid dereferenceable constant iterator").
erase(const_iterator first, const_iterator last) requires 0 ≤ i ≤ j ≤ size.
In both, nothing reallocates: the base pointer is unchanged, the contents become takeZ i xs ++ dropZ (i + 1) xs (resp. takeZ i xs ++ dropZ j xs), and the result is an iterator at i. The later elements move down by move assignment, so each keeps its value, as push_back_move already assumes for its target.
__normal_iterator::operator+(difference_type) const. Like operator++, it does not check bounds yet; see the TODO there.
The converting constructor from iterator to const_iterator, a constructor template in libstdc++. It is stated directly with _global … |-> unmaterialized_specR, since specify.template.ctor does not produce instantiated constructor names.

The iterator model does not invalidate iterators, so a stale iterator that still points inside the new size is admitted; that is #211. There is no rejection test for it.

Tests:

TestErase (in test/vector/test.cpp, called from main) erases the first element, then the last (checking the result equals end()), then the whole range. The glue lemma specs_ok now includes the const_iterator specs for int and the conversion.
TestErase names its iterators before converting or comparing them, as TestIntIter already does with it3 = v.end(). Binding a temporary iterator to a const& (e.g. v.erase(v.begin())) needs wp_make_const on the locked iterator.R_base, which automation does not do.
test/vector/erase_ub.cpp: erase(end()). _GLIBCXX_DEBUG reports it; ASan does not. erase_ub_proof.v shows that it gets stuck on 1 < 1; the goal is recorded in erase_ub_proof.expected.

Size: +255 lines, of which 64 are the recorded .expected goal. test/dune.inc is regenerated by dune-gen.sh; it will conflict trivially with #216, and regenerating resolves it.

🤖 Generated with Claude Code

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) <noreply@anthropic.com>

skylabs-ai-ci · 2026-10-14T21:12:17Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Branch Tip	Base branch	Base commit	PR
fmdeps/brick-libcpp/	jhaag/vector-erase	aa39b44	9520c87	main	5c55bbd	#219

Passive Repos

Repo	Job Branch	Job Commit
./	main	fe784a5
fmdeps/BRiCk/	main	3ecdb99
fmdeps/auto/	main	ce73039
fmdeps/auto-docs/	main	f59f39c
bluerock/NOVA/	skylabs-proof	e55e7f4
bluerock/bhv/	skylabs-main	69a194d
fmdeps/brick-libgtest/	main	aeeddad
fmdeps/ci/	main	60c77e3
vendored/elpi/	skylabs-master	c0b9653
vendored/flocq/	skylabs-master	cf9cc84
vendored/rocq/	skylabs-master	fcb26f5
fmdeps/rocq-agent-toolkit/	main	f49e242
vendored/rocq-elpi/	skylabs-master	7dee592
vendored/rocq-equations/	skylabs-main	9cf8471
vendored/rocq-iris/	skylabs-master	a7af9f7
vendored/rocq-lsp/	skylabs-main	64ef78a
vendored/rocq-stdlib/	skylabs-master	00897b3
vendored/rocq-stdpp/	skylabs-master	0c5e505
fmdeps/skylabs-fm/	main	afbf401
vendored/vsrocq/	skylabs-main	ee79e7a

No Changes in Warnings or Errors

	Before	New	Fixed	After
Errors	0	0	0	0
Warnings	75	0	0	75

Performance

Relative	Master	MR	Change	Filename
+0.23%	196811.8	197272.3	+460.4	total
+0.12%	-	234.4	+234.4	├ newly appeared files (2)
+0.11%	196811.8	197037.9	+226.1	└ common files
+0.01%	53525.0	53531.8	+6.7	├ translation units
+0.15%	143286.8	143506.1	+219.3	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
+0.88%	762.1	768.9	+6.7	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/vector/test_cpp.v
+46.64%	468.9	687.6	+218.7	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v

+0.23%	196811.8	197272.3	+460.4	total
+0.12%	-	234.4	+234.4	├ newly appeared files (2)
+0.11%	196811.8	197037.9	+226.1	└ common files
+0.01%	53525.0	53531.8	+6.7	├ translation units
+0.15%	143286.8	143506.1	+219.3	└ proofs and tests

…sts 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 <noreply@anthropic.com>

skylabs-ai-ci · 2026-10-22T21:47:34Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Branch Tip	Base branch	Base commit	PR
fmdeps/brick-libcpp/	jhaag/vector-erase	ff8f547	e5a2d18	main	44eb191	#219

Passive Repos

Repo	Job Branch	Job Commit
./	main	781c507
fmdeps/BRiCk/	main	f08d690
fmdeps/auto/	main	9008c20
fmdeps/auto-docs/	main	5a40c23
bluerock/NOVA/	skylabs-proof	0573bd1
bluerock/bhv/	skylabs-main	3704d69
fmdeps/brick-libgtest/	main	e0d33c6
fmdeps/ci/	main	2b73b2d
vendored/elpi/	skylabs-master	c0b9653
vendored/flocq/	skylabs-master	cf9cc84
vendored/rocq/	skylabs-master	7c6eef8
fmdeps/rocq-agent-toolkit/	main	3369c0f
vendored/rocq-elpi/	skylabs-master	7dee592
vendored/rocq-equations/	skylabs-main	9cf8471
vendored/rocq-iris/	skylabs-master	a7af9f7
vendored/rocq-stdlib/	skylabs-master	00897b3
vendored/rocq-stdpp/	skylabs-master	0c5e505
fmdeps/skylabs-fm/	main	14654de
vendored/vsrocq/	skylabs-main	03db19e

No Changes in Warnings or Errors

	Before	New	Fixed	After
Errors	0	0	0	0
Warnings	76	0	0	76

Performance

Relative	Master	MR	Change	Filename
+0.23%	194679.7	195121.7	+442.0	total
+0.12%	-	227.4	+227.4	├ newly appeared files (2)
+0.11%	194679.7	194894.2	+214.6	└ common files
+0.01%	48965.5	48972.6	+7.1	├ translation units
+0.14%	145714.2	145921.6	+207.4	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-0.28%	433.0	431.8	-1.2	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/vector/iter_bounds.v
+1.05%	676.3	683.4	+7.1	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/vector/test_cpp.v
+46.35%	451.2	660.3	+209.1	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v

+0.23%	194679.7	195121.7	+442.0	total
+0.12%	-	227.4	+227.4	├ newly appeared files (2)
+0.11%	194679.7	194894.2	+214.6	└ common files
+0.01%	48965.5	48972.6	+7.1	├ translation units
+0.14%	145714.2	145921.6	+207.4	└ proofs and tests

skylabs-ai-ci · 2026-10-23T13:38:10Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Branch Tip	Base branch	Base commit	PR
fmdeps/brick-libcpp/	jhaag/vector-erase	7815a29	3c5ed50	main	44eb191	#219

Passive Repos

Repo	Job Branch	Job Commit
./	main	781c507
fmdeps/BRiCk/	main	f08d690
fmdeps/auto/	main	9dd42cf
fmdeps/auto-docs/	main	5a40c23
bluerock/NOVA/	skylabs-proof	0573bd1
bluerock/bhv/	skylabs-main	3704d69
fmdeps/brick-libgtest/	main	e0d33c6
fmdeps/ci/	main	4270397
vendored/elpi/	skylabs-master	c0b9653
vendored/flocq/	skylabs-master	cf9cc84
vendored/rocq/	skylabs-master	7c6eef8
fmdeps/rocq-agent-toolkit/	main	b307188
vendored/rocq-elpi/	skylabs-master	7dee592
vendored/rocq-equations/	skylabs-main	9cf8471
vendored/rocq-iris/	skylabs-master	a7af9f7
vendored/rocq-stdlib/	skylabs-master	00897b3
vendored/rocq-stdpp/	skylabs-master	0c5e505
fmdeps/skylabs-fm/	main	1a00bf8
vendored/vsrocq/	skylabs-main	03db19e

No Changes in Warnings or Errors

	Before	New	Fixed	After
Errors	0	0	0	0
Warnings	76	0	0	76

Performance

Relative	Master	MR	Change	Filename
+0.23%	194775.1	195218.3	+443.2	total
+0.12%	-	227.4	+227.4	├ newly appeared files (2)
+0.11%	194775.1	194990.9	+215.7	└ common files
+0.01%	48965.5	48972.6	+7.1	├ translation units
+0.14%	145809.6	146018.3	+208.6	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-0.27%	433.1	432.0	-1.2	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/vector/iter_bounds.v
+1.05%	676.3	683.4	+7.1	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/vector/test_cpp.v
+46.34%	451.3	660.5	+209.2	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v

+0.23%	194775.1	195218.3	+443.2	total
+0.12%	-	227.4	+227.4	├ newly appeared files (2)
+0.11%	194775.1	194990.9	+215.7	└ common files
+0.01%	48965.5	48972.6	+7.1	├ translation units
+0.14%	145809.6	146018.3	+208.6	└ proofs and tests

pgiarrusso-sl requested a review from simon-skylabs October 16, 2026 16:00

jhaag-skylabs-ai marked this pull request as ready for review October 21, 2026 21:10

simon-skylabs approved these changes Oct 22, 2026

View reviewed changes

Comment thread rocq-brick-libstdcpp/proof/vector/spec.v Resolved

Comment thread rocq-brick-libstdcpp/proof/vector/spec.v Resolved

Comment thread rocq-brick-libstdcpp/test/vector/erase_ub_proof.expected Resolved

Comment thread rocq-brick-libstdcpp/test/vector/erase_ub_proof.v Resolved

refactor(vector): use takeZ/dropZ in erase specs; drop explicit prepo…

e5a2d18

…sts 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 <noreply@anthropic.com>

jhaag-skylabs-ai enabled auto-merge October 22, 2026 21:34

fix: repair .expected output after rebasing on main

3c5ed50

jhaag-skylabs-ai merged commit 88b7092 into main Oct 23, 2026
1 check passed

jhaag-skylabs-ai deleted the jhaag/vector-erase branch October 23, 2026 13:40

Navigation Menu

Repository navigation

feat(vector): specs for `erase`, iterator `operator+` and `const_iterator` conversion - #219

feat(vector): specs for `erase`, iterator `operator+` and `const_iterator` conversion#219
jhaag-skylabs-ai merged 3 commits into
mainfrom
jhaag/vector-erase

jhaag-skylabs-ai commented Oct 14, 2026 •

edited

Loading

Uh oh!

skylabs-ai-ci Bot commented Oct 14, 2026

Passive Repos

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

skylabs-ai-ci Bot commented Oct 22, 2026

Passive Repos

Uh oh!

skylabs-ai-ci Bot commented Oct 23, 2026

Passive Repos

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

jhaag-skylabs-ai commented Oct 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

skylabs-ai-ci Bot commented Oct 14, 2026

CI summary (Details)

Active Repos

Passive Repos

No Changes in Warnings or Errors

Performance

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

skylabs-ai-ci Bot commented Oct 22, 2026

CI summary (Details)

Active Repos

Passive Repos

No Changes in Warnings or Errors

Performance

Uh oh!

skylabs-ai-ci Bot commented Oct 23, 2026

CI summary (Details)

Active Repos

Passive Repos

No Changes in Warnings or Errors

Performance

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

jhaag-skylabs-ai commented Oct 14, 2026 •

edited

Loading