Skip to content

specifications for std::vector and std::find#64

Open
simon-skylabs wants to merge 2 commits into
mainfrom
simon/std-vector
Open

specifications for std::vector and std::find#64
simon-skylabs wants to merge 2 commits into
mainfrom
simon/std-vector

Conversation

@simon-skylabs
Copy link
Copy Markdown
Contributor

@simon-skylabs simon-skylabs commented May 28, 2026

No description provided.

@skylabs-ai-ci
Copy link
Copy Markdown

skylabs-ai-ci Bot commented May 28, 2026

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Base branch Base commit PR
fmdeps/brick-libcpp/ simon/std-vector 63e818e main 9f54d9a #64

Passive Repos
Repo Job Branch Job Commit
./ main 7d2ee30
fmdeps/BRiCk/ main 094eace
fmdeps/auto/ main a3e8ce2
fmdeps/auto-docs/ main d4c3641
bluerock/NOVA/ skylabs-proof dc3d314
bluerock/bhv/ skylabs-main a803e73
fmdeps/ci/ main e54841c
vendored/elpi/ skylabs-master aa4475f
vendored/flocq/ skylabs-master cf9cc84
fmdeps/fm-tools/ main e5188db
psi/protos/ main 8fe3e7c
psi/backend/ main 0b5fea6
psi/ide/ main 6b596cf
psi/data/ main 82cb305
vendored/rocq/ skylabs-master 2ede3c9
fmdeps/rocq-agent-toolkit/ main 3eed23a
vendored/rocq-elpi/ skylabs-master 103a742
vendored/rocq-equations/ skylabs-main a8c4832
vendored/rocq-ext-lib/ skylabs-master 94a6630
vendored/rocq-iris/ skylabs-master 3ad4ddd
vendored/rocq-lsp/ skylabs-main a8b7272
vendored/rocq-stdlib/ skylabs-master bc07423
vendored/rocq-stdpp/ skylabs-master e01d802
fmdeps/skylabs-fm/ main 06f1cd3
vendored/vsrocq/ skylabs-main 5b4527e

Performance

Relative Master MR Change Filename
-0.00% 127674.0 127674.0 -0.0 total
-0.00% 22800.3 22800.3 -0.0 ├ translation units
+0.00% 104873.7 104873.7 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
-0.00% 127674.0 127674.0 -0.0 total
-0.00% 22800.3 22800.3 -0.0 ├ translation units
+0.00% 104873.7 104873.7 +0.0 └ proofs and tests

@gmalecha-at-skylabs gmalecha-at-skylabs self-requested a review May 29, 2026 03:01
gmalecha-at-skylabs
gmalecha-at-skylabs approved these changes May 29, 2026
View reviewed changes
Copy link
Copy Markdown
Collaborator

@gmalecha-at-skylabs gmalecha-at-skylabs left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good. We need to address the license information and a few other cosmetic things, but otherwise we should get it merged.

Comment thread rocq-brick-libstdcpp/proof/algorithms/spec.v
Comment thread rocq-brick-libstdcpp/proof/iterator/spec.v
Comment on lines +659 to +660
(** TODO: update comment to reflect changes to this *)
Module Type CODE_SNIPPETS (U : common.UNIT).
Copy link
Copy Markdown
Collaborator

@gmalecha-at-skylabs gmalecha-at-skylabs May 29, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks like it needs to be moved to the test directory?

Comment thread rocq-brick-libstdcpp/proof/vector/spec.v
Comment on lines +856 to +858
Module Type VECTOR := VECTOR_PREDS <+ VECTOR_SPECS.

Declare Module vector : VECTOR.
Copy link
Copy Markdown
Collaborator

@gmalecha-at-skylabs gmalecha-at-skylabs May 29, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there a benefit to this structure over simply having things at the top-level?

Copy link
Copy Markdown
Contributor Author

@simon-skylabs simon-skylabs May 29, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think so. I'll remove it

Comment thread rocq-brick-libstdcpp/test/vector/test_cpp_proof.v
* 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.proof.
Copy link
Copy Markdown
Collaborator

@gmalecha-at-skylabs gmalecha-at-skylabs May 29, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should probably modernize this to use prelude.proof.

Copy link
Copy Markdown
Contributor Author

@simon-skylabs simon-skylabs May 29, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes but we should check that we can fix the proofs first.

Copy link
Copy Markdown
Contributor Author

@simon-skylabs simon-skylabs May 29, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually prelude.proof, is included in prelude.test

Comment thread rocq-brick-libstdcpp/test/vector/test.cpp
Comment thread rocq-brick-libstdcpp/test/vector/test_cpp_proof.v
Section proofs.
Context `{MOD : test_cpp.module ⊧ σ}.
Import linearity auto_frac.
Import wp_path.WpPrimRSep.
Copy link
Copy Markdown
Collaborator

@gmalecha-at-skylabs gmalecha-at-skylabs May 29, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Did we decide to deprecate this?

Copy link
Copy Markdown
Contributor Author

@simon-skylabs simon-skylabs May 29, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There was an effort to retire it that I haven't managed to complete yet. Some array hints were tricky to adjust. We can give it another try.

Comment thread rocq-brick-libstdcpp/test/vector/test_cpp_proof.v
Comment on lines +90 to +98
Lemma copy_assign_ok :
denoteModule module |-- copy_assign_spec.
Proof using MOD.
verify_spec. go with pick_frac.
(* errors.Errors.UNSUPPORTED.body
"wp_method_shift: defaulted methods"%pstring *)
Fail Qed.
Admitted.
Definition copy_assign_B := [LINK] copy_assign_ok.
Copy link
Copy Markdown
Collaborator

@gmalecha-at-skylabs gmalecha-at-skylabs May 29, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If the body doesn't exist, then it doesn't seem like it should be necessary for the proof.

Comment thread rocq-brick-libstdcpp/test/vector/test_cpp_proof.v
Definition test_for_each_B := [LINK] test_for_each_ok.
#[local] Hint Resolve test_for_each_B : sl_opacity.

Lemma sum_ok : verify[ module ] sum_spec.
Copy link
Copy Markdown
Collaborator

@gmalecha-at-skylabs gmalecha-at-skylabs May 29, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just modernization.

Suggested change
Lemma sum_ok : verify[ module ] sum_spec.
Lemma sum_ok : verify[ source ] sum_spec.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@gmalecha-at-skylabs gmalecha-at-skylabs gmalecha-at-skylabs approved these changes

At least 1 approving review is required to merge this pull request.

Assignees

@simon-skylabs simon-skylabs

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@simon-skylabs @gmalecha-at-skylabs