Extend specifications for [new] for array forms #11

gmalecha-at-skylabs · 2025-10-31T03:28:47Z

Introduce specifications for operator new[] (default which can throw exceptions)
Simplify the interface of dynAllocatedR and enhance the hints.
Introduce infrastructure for the tests directory.

Based on #6.

Some definitions still need to be upstreamed.

rlepigre-skylabs-ai · 2025-10-31T16:58:13Z

@gmalecha-at-skylabs I rebased this to test CI passing condition.

rocq-brick-libstdcpp/test/new/demo_cpp_proof.v

rocq-brick-libstdcpp/proof/new/pred.v

aa755 · 2025-10-31T18:47:10Z

I am surprised you didnt need this lemma. Did you patch the one in cpp2v? Perhaps the (merge) commit message here can reference the corresponding cpp2v commit SHA?

rocq-brick-libstdcpp/proof/new/hints.v

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

gmalecha-at-skylabs · 2025-10-31T18:53:52Z

I am surprised you didnt need this lemma. Did you patch the one in cpp2v? Perhaps the (merge) commit message here can reference the corresponding cpp2v commit SHA?

Yes. I updated the code in the automation repository. It is still under review though. I am going to try to prove it.

rocq-brick-libstdcpp/proof/new/pred.v

Blaisorblade

Some comments.

github-actions · 2025-11-10T03:32:57Z

Performance summary for https://github.com/SkylabsAI/brick-libcpp/actions/runs/19052828242

Relative	Master	MR	Change	Filename
-0.00%	116952.4	116952.4	-0.0	total
-0.00%	22016.4	22016.4	-0.0	├ translation units
+0.00%	94936.0	94936.0	+0.0	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename

-0.00%	116952.4	116952.4	-0.0	total
-0.00%	22016.4	22016.4	-0.0	├ translation units
+0.00%	94936.0	94936.0	+0.0	└ proofs and tests

github-actions · 2025-11-10T14:39:17Z

Performance summary for https://github.com/SkylabsAI/brick-libcpp/actions/runs/19235064127

Relative	Master	MR	Change	Filename
+0.00%	116952.4	116952.5	+0.1	total
+0.00%	22016.5	22016.4	+0.1	├ translation units
+0.00%	94936.0	94936.0	+0.0	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename

+0.00%	116952.4	116952.5	+0.1	total
+0.00%	22016.5	22016.4	+0.1	├ translation units
+0.00%	94936.0	94936.0	+0.0	└ proofs and tests

github-actions · 2025-11-10T14:55:16Z

Performance summary for https://github.com/SkylabsAI/brick-libcpp/actions/runs/19235491887

Relative	Master	MR	Change	Filename
-0.00%	116952.4	116952.4	-0.0	total
-0.00%	22016.4	22016.4	-0.0	├ translation units
+0.00%	94936.0	94936.0	+0.0	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename

-0.00%	116952.4	116952.4	-0.0	total
-0.00%	22016.4	22016.4	-0.0	├ translation units
+0.00%	94936.0	94936.0	+0.0	└ proofs and tests

rocq-brick-libstdcpp/proof/new/pred.v

…erator delete[]]. - Removes the size argument from [alloc.token]. - Adds additional reasoning principles for [new_token.R].

Documentation updates.

Co-authored-by: Paolo G. Giarrusso <[email protected]>

- [alloc.token] -> [alloc.tokenR]. - standardize automation.

github-actions · 2025-11-10T18:39:39Z

Performance summary for https://github.com/SkylabsAI/brick-libcpp/actions/runs/19241906797

Relative	Master	MR	Change	Filename
+0.00%	116925.2	116925.3	+0.1	total
+0.00%	22016.5	22016.4	+0.1	├ translation units
+0.00%	94908.8	94908.8	+0.0	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename

+0.00%	116925.2	116925.3	+0.1	total
+0.00%	22016.5	22016.4	+0.1	├ translation units
+0.00%	94908.8	94908.8	+0.0	└ proofs and tests

rocq-brick-libstdcpp/proof/new/pred.v

pgiarrusso-sl

Approved with comments. I annotated some that might be onerous to fix.

rocq-brick-libstdcpp/proof/new/hints.v

rocq-brick-libstdcpp/test/cpp2v-dune-gen.sh

rocq-brick-libstdcpp/test/dune

rocq-brick-libstdcpp/proof/new/spec_exc.v

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

rocq-brick-libstdcpp/proof/new/pred.v

github-actions · 2025-11-11T21:20:00Z

Performance summary for https://github.com/SkylabsAI/brick-libcpp/actions/runs/19278633382

Relative	Master	MR	Change	Filename
-0.00%	116925.9	116925.8	-0.1	total
-0.00%	22016.4	22016.5	-0.1	├ translation units
+0.00%	94909.4	94909.4	+0.0	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename

-0.00%	116925.9	116925.8	-0.1	total
-0.00%	22016.4	22016.5	-0.1	├ translation units
+0.00%	94909.4	94909.4	+0.0	└ proofs and tests

Co-authored-by: pgiarrusso-sl <[email protected]>

github-actions · 2025-11-12T04:12:48Z

Performance summary for https://github.com/SkylabsAI/brick-libcpp/actions/runs/19285978974

Relative	Master	MR	Change	Filename
-0.00%	116925.8	116925.8	-0.1	total
-0.00%	22016.4	22016.5	-0.1	├ translation units
+0.00%	94909.4	94909.4	+0.0	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename

-0.00%	116925.8	116925.8	-0.1	total
-0.00%	22016.4	22016.5	-0.1	├ translation units
+0.00%	94909.4	94909.4	+0.0	└ proofs and tests

Co-authored-by: pgiarrusso-sl <[email protected]>

github-actions · 2025-11-12T04:33:11Z

Performance summary for https://github.com/SkylabsAI/brick-libcpp/actions/runs/19286329512

Relative	Master	MR	Change	Filename
-0.00%	116925.8	116925.8	-0.1	total
-0.00%	22016.4	22016.5	-0.1	├ translation units
+0.00%	94909.4	94909.4	+0.0	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename

-0.00%	116925.8	116925.8	-0.1	total
-0.00%	22016.4	22016.5	-0.1	├ translation units
+0.00%	94909.4	94909.4	+0.0	└ proofs and tests

pgiarrusso-sl self-assigned this Oct 31, 2025

rlepigre-skylabs-ai force-pushed the gmalecha/new branch from d9d412d to 5a9629b Compare October 31, 2025 16:57

gmalecha-at-skylabs mentioned this pull request Oct 31, 2025

lemma, hints, and specs needed to enable proofs about new [] #6

Closed

aa755 reviewed Oct 31, 2025

View reviewed changes

rocq-brick-libstdcpp/test/new/demo_cpp_proof.v Outdated Show resolved Hide resolved

gmalecha-at-skylabs commented Oct 31, 2025

View reviewed changes

rocq-brick-libstdcpp/proof/new/pred.v Outdated Show resolved Hide resolved

gmalecha-at-skylabs commented Oct 31, 2025

View reviewed changes

rocq-brick-libstdcpp/proof/new/hints.v Show resolved Hide resolved

gmalecha-at-skylabs commented Oct 31, 2025

View reviewed changes

rocq-brick-libstdcpp/proof/new/hints.v Show resolved Hide resolved

aa755 reviewed Oct 31, 2025

View reviewed changes

rocq-brick-libstdcpp/proof/new/spec.v Show resolved Hide resolved

aa755 approved these changes Oct 31, 2025

View reviewed changes

pgiarrusso-sl self-requested a review October 31, 2025 21:56

pgiarrusso-sl removed their assignment Oct 31, 2025

Blaisorblade reviewed Nov 3, 2025

View reviewed changes

rocq-brick-libstdcpp/proof/new/pred.v Outdated Show resolved Hide resolved

rocq-brick-libstdcpp/proof/new/pred.v Outdated Show resolved Hide resolved

Blaisorblade reviewed Nov 3, 2025

View reviewed changes

pgiarrusso-sl mentioned this pull request Nov 4, 2025

Enhancements to array specifications SkylabsAI/BRiCk#26

Merged

gmalecha-at-skylabs force-pushed the gmalecha/new branch from ea4ba57 to 154e375 Compare November 10, 2025 14:30

aa755 reviewed Nov 10, 2025

View reviewed changes

rocq-brick-libstdcpp/proof/new/pred.v Outdated Show resolved Hide resolved

gmalecha-at-skylabs and others added 8 commits November 10, 2025 13:25

Preliminary specifications.

5318d10

Document <<operator new[]>>.

23d6328

Simplifying [alloc.token] and test cases for [operator new[]] and [op…

a952eb2

…erator delete[]]. - Removes the size argument from [alloc.token]. - Adds additional reasoning principles for [new_token.R].

Build infrastructure for the test directory.

dc658d0

Cleanup.

1af4d0f

Apply suggestions from code review

aa14c0a

Documentation updates.

Update rocq-brick-libstdcpp/proof/new/pred.v

de7ac44

Co-authored-by: Paolo G. Giarrusso <[email protected]>

Cleanup names and upstreaming.

529d556

- [alloc.token] -> [alloc.tokenR]. - standardize automation.

gmalecha-at-skylabs added 2 commits November 10, 2025 13:25

Add additional properties to the predicates around allocation.

bbc8f52

Introduce [allocatorP] for documentation purposes.

8533b4d

gmalecha-at-skylabs force-pushed the gmalecha/new branch from f634bfe to 8533b4d Compare November 10, 2025 18:26

aa755 reviewed Nov 10, 2025

View reviewed changes

rocq-brick-libstdcpp/proof/new/pred.v Show resolved Hide resolved

gmalecha-at-skylabs requested review from Blaisorblade and removed request for Blaisorblade November 11, 2025 01:56

pgiarrusso-sl approved these changes Nov 11, 2025

View reviewed changes

Apply suggestions from code review

fed88a4

Co-authored-by: pgiarrusso-sl <[email protected]>

gmalecha-at-skylabs force-pushed the gmalecha/new branch from 601a87b to fed88a4 Compare November 12, 2025 04:03

Update rocq-brick-libstdcpp/test/dune

e023422

Co-authored-by: pgiarrusso-sl <[email protected]>

gmalecha-at-skylabs self-assigned this Nov 12, 2025

aa755 mentioned this pull request Nov 12, 2025

specs of shared_ptr #10

Open

Extend specifications for [new] for array forms #11

Are you sure you want to change the base?

Extend specifications for [new] for array forms #11

Uh oh!

Conversation

gmalecha-at-skylabs commented Oct 31, 2025

Uh oh!

rlepigre-skylabs-ai commented Oct 31, 2025

Uh oh!

Uh oh!

Uh oh!

aa755 commented Oct 31, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

gmalecha-at-skylabs commented Oct 31, 2025

Uh oh!

Uh oh!

Uh oh!

Blaisorblade left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Nov 10, 2025

Uh oh!

github-actions bot commented Nov 10, 2025

Uh oh!

github-actions bot commented Nov 10, 2025

Uh oh!

Uh oh!

github-actions bot commented Nov 10, 2025

Uh oh!

Uh oh!

pgiarrusso-sl left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented Nov 11, 2025

Uh oh!

github-actions bot commented Nov 12, 2025

Uh oh!

github-actions bot commented Nov 12, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants