Skip to content

feat(vector): specs for data, empty - #216

Merged
jhaag-skylabs-ai merged 2 commits into
mainfrom
jhaag/vector-data-empty
Oct 27, 2026
Merged

feat(vector): specs for data, empty#216
jhaag-skylabs-ai merged 2 commits into
mainfrom
jhaag/vector-data-empty

Conversation

@jhaag-skylabs-ai

@jhaag-skylabs-ai jhaag-skylabs-ai commented Oct 14, 2026

Copy link
Copy Markdown
Contributor

Specs for std::vector::empty() const and both data() overloads, against spineR (vector.data, container.reqmts), following the std::array specs:

  • empty() returns bool_decide (size = 0).
  • data() returns base_pointer st, which is null for a vector that never allocated.

Both are total. Using data()'s result needs ownership of the elements, exactly as with operator[].

Tests:

  • TestDataEmpty (in test/vector/test.cpp, called from main) checks empty() before and after push_back, writes through data(), and reads through the const overload.
  • test/vector/data_ub.cpp has two UB clients, each the twin of a line in TestDataEmpty: a read one past the last element and *v.data() on an empty vector. ASan reports both. data_ub_proof.v shows that each gets stuck on the missing element ownership (index 1 of a one-element vector, and nullptr). The stuck goals are recorded in data_ub_proof.expected.

test/dune.inc is regenerated by dune-gen.sh for the new .cpp.

🤖 Generated with Claude Code

@skylabs-ai-ci

skylabs-ai-ci Bot commented Oct 14, 2026

Copy link
Copy Markdown

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Branch Tip Base branch Base commit PR
fmdeps/brick-libcpp/ jhaag/vector-data-empty 15fa6c1 8c7ef83 main 5c55bbd #216

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.14% 196811.8 197081.0 +269.1 total
+0.11% - 217.2 +217.2 ├ newly appeared files (2)
+0.03% 196811.8 196863.8 +52.0 └ common files
-0.01% 53525.0 53522.2 -2.9 ├ translation units
+0.04% 143286.8 143341.6 +54.8 └ proofs and tests
Full Results
Relative Master MR Change Filename
-0.37% 762.1 759.3 -2.9 fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/vector/test_cpp.v
+11.64% 468.9 523.5 +54.6 fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v
+0.14% 196811.8 197081.0 +269.1 total
+0.11% - 217.2 +217.2 ├ newly appeared files (2)
+0.03% 196811.8 196863.8 +52.0 └ common files
-0.01% 53525.0 53522.2 -2.9 ├ translation units
+0.04% 143286.8 143341.6 +54.8 └ proofs and tests

@jhaag-skylabs-ai jhaag-skylabs-ai mentioned this pull request Oct 14, 2026
Merged
@jhaag-skylabs-ai
jhaag-skylabs-ai marked this pull request as ready for review October 21, 2026 21:10
@skylabs-ai-ci

skylabs-ai-ci Bot commented Oct 23, 2026

Copy link
Copy Markdown

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Branch Tip Base branch Base commit PR
fmdeps/brick-libcpp/ jhaag/vector-data-empty 4eb7dd0 25d72d9 main 44eb191 #216

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.14% 194775.1 195049.9 +274.8 total
+0.11% - 223.7 +223.7 ├ newly appeared files (2)
+0.03% 194775.1 194826.2 +51.1 └ common files
+0.01% 48965.5 48968.0 +2.5 ├ translation units
+0.03% 145809.6 145858.2 +48.6 └ proofs and tests
Full Results
Relative Master MR Change Filename
-0.27% 433.1 431.9 -1.2 fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/vector/iter_bounds.v
+0.37% 676.3 678.8 +2.5 fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/vector/test_cpp.v
+11.00% 451.3 501.0 +49.6 fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v
+0.14% 194775.1 195049.9 +274.8 total
+0.11% - 223.7 +223.7 ├ newly appeared files (2)
+0.03% 194775.1 194826.2 +51.1 └ common files
+0.01% 48965.5 48968.0 +2.5 ├ translation units
+0.03% 145809.6 145858.2 +48.6 └ proofs and tests

@simon-skylabs
simon-skylabs force-pushed the jhaag/vector-data-empty branch from 25d72d9 to 0cea485 Compare October 27, 2026 19:49
@skylabs-ai-ci

skylabs-ai-ci Bot commented Oct 27, 2026

Copy link
Copy Markdown

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Branch Tip Base branch Base commit PR
fmdeps/brick-libcpp/ jhaag/vector-data-empty fe8924b 0cea485 main 192c9dd #216

Passive Repos
Repo Job Branch Job Commit
./ main 781c507
fmdeps/BRiCk/ main 2ce8ed0
fmdeps/auto/ main ff6306c
fmdeps/auto-docs/ main 918aa33
bluerock/NOVA/ skylabs-proof 02f6828
bluerock/bhv/ skylabs-main e235791
fmdeps/brick-libgtest/ main 495b855
fmdeps/ci/ main b480641
vendored/elpi/ skylabs-master c0b9653
vendored/flocq/ skylabs-master cf9cc84
vendored/rocq/ skylabs-master 7c6eef8
fmdeps/rocq-agent-toolkit/ main 53fde9a
vendored/rocq-elpi/ skylabs-master 7dee592
vendored/rocq-equations/ skylabs-main 9cf8471
vendored/rocq-iris/ skylabs-master 285745a
vendored/rocq-stdlib/ skylabs-master 00897b3
vendored/rocq-stdpp/ skylabs-master ba29dba
fmdeps/skylabs-fm/ main ffa586f
vendored/vsrocq/ skylabs-main 03db19e

Changes in Warnings or Errors

Before New Fixed After
Errors 0 ${\color{red}1}$ 0 1
Warnings 76 ${\color{red}1}$ ${\color{green}1}$ 76

Performance

Relative Master MR Change Filename
-0.23% 199110.0 198657.9 -452.2 total
-0.34% 677.4 - -677.4 ├ disappeared files (1)
+0.11% - 225.3 +225.3 ├ newly appeared files (2)
-0.00% 198432.6 198432.5 -0.1 └ common files
-0.00% 49396.3 49396.0 -0.3 ├ translation units
+0.00% 149036.3 149036.6 +0.2 └ proofs and tests
Full Results
Relative Master MR Change Filename
-0.23% 199110.0 198657.9 -452.2 total
-0.34% 677.4 - -677.4 ├ disappeared files (1)
+0.11% - 225.3 +225.3 ├ newly appeared files (2)
-0.00% 198432.6 198432.5 -0.1 └ common files
-0.00% 49396.3 49396.0 -0.3 ├ translation units
+0.00% 149036.3 149036.6 +0.2 └ proofs and tests

@skylabs-ai-ci

skylabs-ai-ci Bot commented Oct 27, 2026

Copy link
Copy Markdown

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Branch Tip Base branch Base commit PR
fmdeps/brick-libcpp/ jhaag/vector-data-empty de1dfac da04bdd main 192c9dd #216

Passive Repos
Repo Job Branch Job Commit
./ main 781c507
fmdeps/BRiCk/ main 2ce8ed0
fmdeps/auto/ main ff6306c
fmdeps/auto-docs/ main 918aa33
bluerock/NOVA/ skylabs-proof 02f6828
bluerock/bhv/ skylabs-main e235791
fmdeps/brick-libgtest/ main 495b855
fmdeps/ci/ main b480641
vendored/elpi/ skylabs-master c0b9653
vendored/flocq/ skylabs-master cf9cc84
vendored/rocq/ skylabs-master 7c6eef8
fmdeps/rocq-agent-toolkit/ main 53fde9a
vendored/rocq-elpi/ skylabs-master 7dee592
vendored/rocq-equations/ skylabs-main 9cf8471
vendored/rocq-iris/ skylabs-master 285745a
vendored/rocq-stdlib/ skylabs-master 00897b3
vendored/rocq-stdpp/ skylabs-master ba29dba
fmdeps/skylabs-fm/ main ffa586f
vendored/vsrocq/ skylabs-main 03db19e

Changes in Warnings or Errors

Before New Fixed After
Errors 0 ${\color{red}1}$ 0 1
Warnings 76 ${\color{red}1}$ ${\color{green}1}$ 76

Performance

Relative Master MR Change Filename
-0.23% 199110.0 198657.9 -452.2 total
-0.34% 677.4 - -677.4 ├ disappeared files (1)
+0.11% - 225.3 +225.3 ├ newly appeared files (2)
-0.00% 198432.6 198432.5 -0.1 └ common files
-0.00% 49396.3 49396.0 -0.3 ├ translation units
+0.00% 149036.3 149036.6 +0.2 └ proofs and tests
Full Results
Relative Master MR Change Filename
-0.23% 199110.0 198657.9 -452.2 total
-0.34% 677.4 - -677.4 ├ disappeared files (1)
+0.11% - 225.3 +225.3 ├ newly appeared files (2)
-0.00% 198432.6 198432.5 -0.1 └ common files
-0.00% 49396.3 49396.0 -0.3 ├ translation units
+0.00% 149036.3 149036.6 +0.2 └ proofs and tests

jhaag-skylabs-ai and others added 2 commits October 27, 2026 18:08
@jhaag-skylabs-ai @claude Simon Hudon
feat(vector): specs for data, empty
a07f15d 
Specify `std::vector::empty() const` and both `data()` overloads against
`spineR`: `empty` returns whether the size is zero, `data` returns the
base pointer, which is null for a vector that never allocated. Both are
total; using `data()`'s result needs ownership of the elements, as with
`operator[]`.

TestDataEmpty verifies writes and reads through `data()`. The UB clients
in data_ub.cpp (a read one past the last element, and `*v.data()` on an
empty vector) get stuck on the missing element ownership; the stuck goals
are recorded in data_ub_proof.expected.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Simon Hudon
update test output
4fd1d71
@simon-skylabs
simon-skylabs force-pushed the jhaag/vector-data-empty branch from da04bdd to 4fd1d71 Compare October 27, 2026 22:09
@skylabs-ai-ci

skylabs-ai-ci Bot commented Oct 27, 2026

Copy link
Copy Markdown

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Branch Tip Base branch Base commit PR
fmdeps/brick-libcpp/ jhaag/vector-data-empty 6f849e2 4fd1d71 main 192c9dd #216

Passive Repos
Repo Job Branch Job Commit
./ main 781c507
fmdeps/BRiCk/ main 2ce8ed0
fmdeps/auto/ main ff6306c
fmdeps/auto-docs/ main 918aa33
bluerock/NOVA/ skylabs-proof 02f6828
bluerock/bhv/ skylabs-main e235791
fmdeps/brick-libgtest/ main 495b855
fmdeps/ci/ main b480641
vendored/elpi/ skylabs-master c0b9653
vendored/flocq/ skylabs-master cf9cc84
vendored/rocq/ skylabs-master 7c6eef8
fmdeps/rocq-agent-toolkit/ main 53fde9a
vendored/rocq-elpi/ skylabs-master 7dee592
vendored/rocq-equations/ skylabs-main 9cf8471
vendored/rocq-iris/ skylabs-master 285745a
vendored/rocq-stdlib/ skylabs-master 00897b3
vendored/rocq-stdpp/ skylabs-master ba29dba
fmdeps/skylabs-fm/ main ffa586f
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.14% 199110.0 199388.6 +278.5 total
+0.11% - 225.3 +225.3 ├ newly appeared files (2)
+0.03% 199110.0 199163.2 +53.2 └ common files
-0.00% 49396.3 49396.0 -0.3 ├ translation units
+0.04% 149713.8 149767.3 +53.5 └ proofs and tests
Full Results
Relative Master MR Change Filename
+7.87% 677.4 730.7 +53.3 fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v
+0.14% 199110.0 199388.6 +278.5 total
+0.11% - 225.3 +225.3 ├ newly appeared files (2)
+0.03% 199110.0 199163.2 +53.2 └ common files
-0.00% 49396.3 49396.0 -0.3 ├ translation units
+0.04% 149713.8 149767.3 +53.5 └ proofs and tests

@jhaag-skylabs-ai
jhaag-skylabs-ai merged commit dc3d407 into main Oct 27, 2026
1 check passed
@jhaag-skylabs-ai
jhaag-skylabs-ai deleted the jhaag/vector-data-empty branch October 27, 2026 22:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@simon-skylabs simon-skylabs simon-skylabs approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@jhaag-skylabs-ai @simon-skylabs