Skip to content

Refinement-based specifications for iostream#40

Merged
rlepigre-skylabs-ai merged 8 commits into
mainfrom
gmalecha/refinement-iostream
May 27, 2026
Merged

Refinement-based specifications for iostream#40
rlepigre-skylabs-ai merged 8 commits into
mainfrom
gmalecha/refinement-iostream

Conversation

@gmalecha-at-skylabs
Copy link
Copy Markdown
Collaborator

@gmalecha-at-skylabs gmalecha-at-skylabs commented Feb 13, 2026 •
edited
Loading

This defines the semantics of ostream (and ultimately istream) in terms of events in a refinement style.

The idea is that a program would get an LTS that would include input and output events and that the Istream and Ostream classes would be tied to this overall specification. E.g. a program specification might be something like an itree like:

x <- input_string ;
print x;
ret tt

Which would block on certain input events and then repeat those going out. There are definitely some choices to be made around input.

@gmalecha-at-skylabs gmalecha-at-skylabs self-assigned this Feb 13, 2026
@skylabs-ai-ci
Copy link
Copy Markdown

skylabs-ai-ci Bot commented Feb 13, 2026

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Base commit PR
fmdeps/brick-libcpp/ gmalecha/refinement-iostream ede7c31 3594482 #40

Passive Repos
Repo Job Branch Job Commit
./ main 9259c2e
fmdeps/BRiCk/ main 6b2f050
fmdeps/auto/ main f6f2422
fmdeps/auto-docs/ main e83c1ad
bluerock/NOVA/ skylabs-proof 927947d
bluerock/bhv/ skylabs-main 37b86fb
fmdeps/ci/ main 33d6ba2
vendored/elpi/ skylabs-master aa4475f
fmdeps/fm-ci/ main e97f125
fmdeps/fm-tools/ main 46ed5a6
psi/protos/ main 8fe3e7c
psi/backend/ main b1f795a
psi/ide/ main 6b596cf
psi/data/ main 8248319
vendored/rocq/ skylabs-master 2ede3c9
fmdeps/rocq-agent-toolkit/ main 35433d5
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 7d620c1
vendored/vsrocq/ skylabs-main 5b4527e

Performance

Relative Master MR Change Filename
-0.00% 122785.4 122785.4 -0.0 total
-0.00% 22463.5 22463.5 -0.0 ├ translation units
+0.00% 100321.9 100321.9 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
-0.00% 122785.4 122785.4 -0.0 total
-0.00% 22463.5 22463.5 -0.0 ├ translation units
+0.00% 100321.9 100321.9 +0.0 └ proofs and tests

@gmalecha-at-skylabs gmalecha-at-skylabs force-pushed the gmalecha/refinement-iostream branch from 944dabf to 7ed54b8 Compare March 5, 2026 04:17
@skylabs-ai-ci
Copy link
Copy Markdown

skylabs-ai-ci Bot commented Mar 5, 2026

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Base commit PR
fmdeps/brick-libcpp/ gmalecha/refinement-iostream 07259fd 730dc61 #40

Passive Repos
Repo Job Branch Job Commit
./ main e5c342a
fmdeps/BRiCk/ main b79c734
fmdeps/auto/ main ffda14f
fmdeps/auto-docs/ main 9f57097
bluerock/NOVA/ skylabs-proof 996d600
bluerock/bhv/ skylabs-main b1ca30d
fmdeps/ci/ main 7712f8c
vendored/elpi/ skylabs-master aa4475f
fmdeps/fm-ci/ main 262fb04
fmdeps/fm-tools/ main 430933c
psi/protos/ main 8fe3e7c
psi/backend/ main 2a8240c
psi/ide/ main 6b596cf
psi/data/ main 62ed81e
vendored/rocq/ skylabs-master 2ede3c9
fmdeps/rocq-agent-toolkit/ main b19cff9
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 7d620c1
vendored/vsrocq/ skylabs-main 5b4527e

Performance

Relative Master MR Change Filename
-0.00% 122840.0 122840.0 -0.0 total
-0.00% 22632.7 22632.7 -0.0 ├ translation units
+0.00% 100207.4 100207.4 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
-0.00% 122840.0 122840.0 -0.0 total
-0.00% 22632.7 22632.7 -0.0 ├ translation units
+0.00% 100207.4 100207.4 +0.0 └ proofs and tests

@pgiarrusso-sl pgiarrusso-sl force-pushed the paolo/eval-old-release branch from 92f3990 to 31de00b Compare March 6, 2026 16:36
Base automatically changed from paolo/eval-old-release to main March 7, 2026 22:26
gmalecha-at-skylabs
gmalecha-at-skylabs commented Apr 7, 2026
View reviewed changes
Comment thread rocq-brick-libstdcpp/test/geeks_for_geeks_examples/spec.v Outdated
@gmalecha-at-skylabs gmalecha-at-skylabs force-pushed the gmalecha/refinement-iostream branch from 7ed54b8 to fbdf351 Compare April 8, 2026 19:54
@gmalecha-at-skylabs gmalecha-at-skylabs added the enhancement New feature or request label Apr 8, 2026
gmalecha-at-skylabs
gmalecha-at-skylabs commented Apr 8, 2026
View reviewed changes
Comment thread rocq-brick-libstdcpp/proof/iostream/spec.v Outdated
@skylabs-ai-ci
Copy link
Copy Markdown

skylabs-ai-ci Bot commented Apr 8, 2026

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Base branch Base commit PR
fmdeps/brick-libcpp/ gmalecha/refinement-iostream 72042d3 main e979b29 #40

Passive Repos
Repo Job Branch Job Commit
./ main 64a8e0d
fmdeps/BRiCk/ main 1aed69a
fmdeps/auto/ main e77b825
fmdeps/auto-docs/ main 9f57097
bluerock/NOVA/ skylabs-proof e9a69cc
bluerock/bhv/ skylabs-main 6c1999f
fmdeps/ci/ main 41c7609
vendored/elpi/ skylabs-master aa4475f
fmdeps/fm-ci/ main 262fb04
fmdeps/fm-tools/ main e17f6db
psi/protos/ main 8fe3e7c
psi/backend/ main 451fcaa
psi/ide/ main 6b596cf
psi/data/ main f283f23
vendored/rocq/ skylabs-master 2ede3c9
fmdeps/rocq-agent-toolkit/ main 61c9d23
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 7c3aae7
vendored/vsrocq/ skylabs-main 5b4527e

Performance

Relative Master MR Change Filename
+0.00% 123482.6 123482.6 +0.0 total
+0.00% 22636.8 22636.8 +0.0 ├ translation units
+0.00% 100845.8 100845.8 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
+0.00% 123482.6 123482.6 +0.0 total
+0.00% 22636.8 22636.8 +0.0 ├ translation units
+0.00% 100845.8 100845.8 +0.0 └ proofs and tests

gmalecha-at-skylabs
gmalecha-at-skylabs commented Apr 9, 2026
View reviewed changes
Comment thread rocq-brick-libstdcpp/proof/iostream/spec.v Outdated
@gmalecha-at-skylabs
Copy link
Copy Markdown
Collaborator Author

gmalecha-at-skylabs commented Apr 11, 2026

Currently blocked on https://github.com/SkyLabsAI/auto/pull/147

pgiarrusso-sl
pgiarrusso-sl reviewed Apr 13, 2026
View reviewed changes
Comment thread rocq-brick-libstdcpp/proof/iostream/spec.v Outdated
@gmalecha-at-skylabs gmalecha-at-skylabs force-pushed the gmalecha/refinement-iostream branch from 817c28a to 7eb3908 Compare April 13, 2026 19:07
@gmalecha-at-skylabs
Copy link
Copy Markdown
Collaborator Author

gmalecha-at-skylabs commented Apr 13, 2026

Comments from discussion with @pgiarrusso-sl:

  • Needs more documentation
  • Should port remaining examples
  • More examples that would be useful:
    • dependent input & output, e.g. echo
    • non-determinism, e.g. print a random number between 1 and 6

@gmalecha-at-skylabs gmalecha-at-skylabs force-pushed the gmalecha/refinement-iostream branch from dbcaa55 to 0308df5 Compare May 1, 2026 18:29
@skylabs-ai-ci
Copy link
Copy Markdown

skylabs-ai-ci Bot commented May 1, 2026

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Base branch Base commit PR
fmdeps/brick-libcpp/ gmalecha/refinement-iostream 0d8346b main a02df96 #40

Passive Repos
Repo Job Branch Job Commit
./ main e8e81bb
fmdeps/BRiCk/ main 9ab35f8
fmdeps/auto/ main 6deed31
fmdeps/auto-docs/ main bfa8f2d
bluerock/NOVA/ skylabs-proof 6cbef03
bluerock/bhv/ skylabs-main 448828c
fmdeps/ci/ main 3707442
vendored/elpi/ skylabs-master aa4475f
vendored/flocq/ skylabs-master cf9cc84
fmdeps/fm-ci/ main 262fb04
fmdeps/fm-tools/ main e17f6db
psi/protos/ main 8fe3e7c
psi/backend/ main a5fa400
psi/ide/ main 6b596cf
psi/data/ main 76acc2f
vendored/rocq/ skylabs-master 2ede3c9
fmdeps/rocq-agent-toolkit/ main ac7e4ec
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 62d34c3
vendored/vsrocq/ skylabs-main 5b4527e

Performance

Relative Master MR Change Filename
-0.00% 124414.1 124414.1 -0.0 total
-0.00% 22637.5 22637.5 -0.0 ├ translation units
+0.00% 101776.7 101776.7 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
-0.00% 124414.1 124414.1 -0.0 total
-0.00% 22637.5 22637.5 -0.0 ├ translation units
+0.00% 101776.7 101776.7 +0.0 └ proofs and tests

@gmalecha-at-skylabs
Copy link
Copy Markdown
Collaborator Author

gmalecha-at-skylabs commented May 1, 2026

I would like to take some of the input examples and refine them in a subsequent PR.

gmalecha-at-skylabs
gmalecha-at-skylabs commented May 1, 2026
View reviewed changes
Comment thread rocq-brick-libstdcpp/proof/iostream/itree.v
@skylabs-ai-ci
Copy link
Copy Markdown

skylabs-ai-ci Bot commented May 1, 2026

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Base branch Base commit PR
fmdeps/brick-libcpp/ gmalecha/refinement-iostream e1c192f main a02df96 #40

Passive Repos
Repo Job Branch Job Commit
./ main e8e81bb
fmdeps/BRiCk/ main 9ab35f8
fmdeps/auto/ main 6deed31
fmdeps/auto-docs/ main bfa8f2d
bluerock/NOVA/ skylabs-proof 6cbef03
bluerock/bhv/ skylabs-main 448828c
fmdeps/ci/ main 3707442
vendored/elpi/ skylabs-master aa4475f
vendored/flocq/ skylabs-master cf9cc84
fmdeps/fm-ci/ main 262fb04
fmdeps/fm-tools/ main e17f6db
psi/protos/ main 8fe3e7c
psi/backend/ main a5fa400
psi/ide/ main 6b596cf
psi/data/ main 76acc2f
vendored/rocq/ skylabs-master 2ede3c9
fmdeps/rocq-agent-toolkit/ main ac7e4ec
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 62d34c3
vendored/vsrocq/ skylabs-main 5b4527e

Performance

Relative Master MR Change Filename
+0.00% 124414.1 124414.1 +0.0 total
+0.00% 22637.5 22637.5 +0.0 ├ translation units
+0.00% 101776.7 101776.7 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
+0.00% 124414.1 124414.1 +0.0 total
+0.00% 22637.5 22637.5 +0.0 ├ translation units
+0.00% 101776.7 101776.7 +0.0 └ proofs and tests

pgiarrusso-sl
pgiarrusso-sl reviewed May 1, 2026
View reviewed changes
Comment thread rocq-brick-libstdcpp/proof/iostream/pred.v Outdated
@pgiarrusso-sl
Copy link
Copy Markdown
Contributor

pgiarrusso-sl commented May 6, 2026 •
edited
Loading

GitHub comments are down (https://www.githubstatus.com/incidents/f5pb5d5mr9yh) but:

  • high level: I don't think this is yet clear enough to replace the current trace specs
  • evt -> evts for type propset
  • pick_ex_C etc should be upstreamed
  • AnyStep(s) needs docs
  • the top-level main specs seem mostly understandable for printing hello world.

pgiarrusso-sl
pgiarrusso-sl reviewed May 7, 2026
View reviewed changes
Comment thread rocq-brick-libstdcpp/test/g4g/N12_area.v Outdated
pgiarrusso-sl
pgiarrusso-sl reviewed May 7, 2026
View reviewed changes
Comment thread rocq-brick-libstdcpp/test/g4g/N1_hello_world.v Outdated
pgiarrusso-sl
pgiarrusso-sl requested changes May 7, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@pgiarrusso-sl pgiarrusso-sl left a comment

Choose a reason for hiding this comment

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

We agreed to keep both specs side by side.

I'll review accordingly.

pgiarrusso-sl
pgiarrusso-sl reviewed May 7, 2026
View reviewed changes
Comment thread rocq-brick-libstdcpp/test/g4g/prelude.v
pgiarrusso-sl
pgiarrusso-sl reviewed May 7, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@pgiarrusso-sl pgiarrusso-sl left a comment

Choose a reason for hiding this comment

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

Some more comments.

Comment thread rocq-brick-libstdcpp/test/g4g/prelude.v
Comment thread rocq-brick-libstdcpp/test/g4g/prelude.v Outdated
Comment thread rocq-brick-libstdcpp/test/g4g/prelude.v Outdated
Comment thread rocq-brick-libstdcpp/test/g4g/N12_area.v
intros.
iIntros "F" (?) "K".
rewrite /Step.requester.
Admitted.
Copy link
Copy Markdown
Contributor

@pgiarrusso-sl pgiarrusso-sl May 7, 2026

Choose a reason for hiding this comment

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

Should we fix this and other admits before merging?

Copy link
Copy Markdown
Collaborator Author

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

Choose a reason for hiding this comment

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

Most of these larger issues are not formally blocked, but "good solutions" are blocked on SkyLabsAI/BRiCk#126

@gmalecha-at-skylabs gmalecha-at-skylabs force-pushed the gmalecha/refinement-iostream branch from 7607482 to 5200a21 Compare May 7, 2026 15:58
@skylabs-ai-ci
Copy link
Copy Markdown

skylabs-ai-ci Bot commented May 7, 2026

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Base branch Base commit PR
fmdeps/brick-libcpp/ gmalecha/refinement-iostream 1367da7 main 2014908 #40

Passive Repos
Repo Job Branch Job Commit
./ main b9f28b5
fmdeps/BRiCk/ main d94485e
fmdeps/auto/ main 63d5e05
fmdeps/auto-docs/ main 93d06b3
bluerock/NOVA/ skylabs-proof 6cbef03
bluerock/bhv/ skylabs-main 448828c
fmdeps/ci/ main 680889d
vendored/elpi/ skylabs-master aa4475f
vendored/flocq/ skylabs-master cf9cc84
fmdeps/fm-tools/ main fb160a9
psi/protos/ main 8fe3e7c
psi/backend/ main 0b5fea6
psi/ide/ main 6b596cf
psi/data/ main 76acc2f
vendored/rocq/ skylabs-master 2ede3c9
fmdeps/rocq-agent-toolkit/ main ac7e4ec
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 e8b88a7
vendored/vsrocq/ skylabs-main 5b4527e

Performance

Relative Master MR Change Filename
+0.00% 125661.1 125661.1 +0.0 total
+0.00% 22788.6 22788.6 +0.0 ├ translation units
+0.00% 102872.5 102872.5 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
+0.00% 125661.1 125661.1 +0.0 total
+0.00% 22788.6 22788.6 +0.0 ├ translation units
+0.00% 102872.5 102872.5 +0.0 └ proofs and tests

@skylabs-ai-ci
Copy link
Copy Markdown

skylabs-ai-ci Bot commented May 19, 2026

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Base branch Base commit PR
fmdeps/brick-libcpp/ gmalecha/refinement-iostream 9a9e912 main 2014908 #40

Passive Repos
Repo Job Branch Job Commit
./ main 7d2ee30
fmdeps/BRiCk/ main c72b430
fmdeps/auto/ main 0d84c2b
fmdeps/auto-docs/ main d4c3641
bluerock/NOVA/ skylabs-proof dc3d314
bluerock/bhv/ skylabs-main c46f5e3
fmdeps/ci/ main 9e6e574
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 76acc2f
vendored/rocq/ skylabs-master 2ede3c9
fmdeps/rocq-agent-toolkit/ main ac7e4ec
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 e8b88a7
vendored/vsrocq/ skylabs-main 5b4527e

Performance

Relative Master MR Change Filename
-0.00% 126789.9 126789.9 -0.0 total
-0.00% 22690.6 22690.6 -0.0 ├ translation units
+0.00% 104099.3 104099.3 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
-0.00% 126789.9 126789.9 -0.0 total
-0.00% 22690.6 22690.6 -0.0 ├ translation units
+0.00% 104099.3 104099.3 +0.0 └ proofs and tests

@gmalecha-at-skylabs gmalecha-at-skylabs mentioned this pull request May 19, 2026
Merged
@skylabs-ai-ci
Copy link
Copy Markdown

skylabs-ai-ci Bot commented May 22, 2026

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Base branch Base commit PR
fmdeps/brick-libcpp/ gmalecha/refinement-iostream 5284f04 main 2014908 #40

Passive Repos
Repo Job Branch Job Commit
./ main 7d2ee30
fmdeps/BRiCk/ main d621299
fmdeps/auto/ main 3d984a8
fmdeps/auto-docs/ main d4c3641
bluerock/NOVA/ skylabs-proof dc3d314
bluerock/bhv/ skylabs-main c46f5e3
fmdeps/ci/ main 9e6e574
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 ac7e4ec
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 e8b88a7
vendored/vsrocq/ skylabs-main 5b4527e

Performance

Relative Master MR Change Filename
-0.06% 127472.8 127390.8 -82.0 total
+0.00% 22690.6 22690.6 +0.0 ├ translation units
-0.08% 104700.2 104782.2 -82.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
-4.55% 37.7 36.0 -1.7 bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/captable.v
-2.70% 54.5 53.1 -1.5 bluerock/NOVA/build-proof/proof/pd_cpp_proof/hints.v
-2.29% 58.0 56.6 -1.3 bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/packet_ctor.v
-1.68% 67.9 66.8 -1.1 bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/insert.v
-1.02% 125.1 123.8 -1.3 bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/create.v
-0.92% 126.2 125.0 -1.2 bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/lookup.v
-0.86% 137.9 136.7 -1.2 bluerock/bhv/apps/vmm/proof/main_cpp_proof/proof.v
-0.86% 136.9 135.7 -1.2 bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/update.v
-0.77% 201.6 200.0 -1.6 bluerock/NOVA/build-proof/proof/sc_cpp_proof/create.v
-0.71% 192.4 191.0 -1.4 bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/set_virtio_net_header.v
-0.71% 260.9 259.1 -1.8 bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_sm.v
-0.60% 283.0 281.3 -1.7 bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/get_set_byte_requesters.v
-0.60% 305.8 304.0 -1.8 bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_pt.v
-0.58% 310.3 308.5 -1.8 bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/wp_vcpu_lemmas.v
-0.56% 328.2 326.4 -1.8 bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_hst.v
-0.55% 288.5 286.9 -1.6 bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_sm.v
-0.51% 320.5 318.9 -1.7 bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_obj.v
-0.51% 240.8 239.6 -1.2 bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/flood.v
-0.50% 276.9 275.6 -1.4 bluerock/NOVA/build-proof/proof/pd_cpp_proof/create.v
-0.46% 380.4 378.6 -1.8 bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ctrl_sm.v
-0.45% 270.9 269.7 -1.2 bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_gst.v
-0.45% 379.3 377.6 -1.7 bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_pd.v
-0.44% 280.4 279.1 -1.2 bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/delegate.v
-0.43% 392.8 391.1 -1.7 bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/extract_frame_header.v
-0.39% 335.9 334.6 -1.3 bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/walk.v
-0.39% 360.6 359.2 -1.4 bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/handle_data_abort.v
-0.39% 330.9 329.6 -1.3 bluerock/bhv/apps/vswitch/lib/forwarding/proof/transaction_protocol/hints.v
-0.39% 342.9 341.5 -1.3 bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_pt.v
-0.38% 324.3 323.1 -1.2 bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_dma.v
-0.37% 361.4 360.1 -1.3 bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/schedule.v
-0.37% 375.8 374.4 -1.4 bluerock/NOVA/build-proof/proof/sm_cpp_proof/dn.v
-0.36% 475.2 473.5 -1.7 bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/msr_framework.v
-0.34% 490.8 489.1 -1.7 bluerock/bhv/apps/vswitch/lib/port/proof/port/proof.v
-0.34% 549.6 547.8 -1.9 bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_sc.v
-0.33% 554.9 553.0 -1.8 bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_sc.v
-0.31% 546.4 544.6 -1.7 bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ctrl_pd.v
-0.30% 514.5 513.0 -1.5 bluerock/bhv/apps/vmm/proof/main_cpp_proof/run_vm.v
-0.26% 464.0 462.8 -1.2 bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_pd.v
-0.26% 538.2 536.8 -1.4 bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/ready_queues.v
-0.24% 509.0 507.7 -1.2 bluerock/bhv/apps/vmm/vml/devices/vpl011/proof/pl011_proof/recv.v
-0.24% 726.9 725.2 -1.7 bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/misc.v
-0.21% 759.4 757.8 -1.6 bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/setup.v
-0.21% 669.7 668.3 -1.4 bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/copy.v
-0.21% 686.3 684.9 -1.4 bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/virtual_interface.v
-0.18% 905.1 903.4 -1.7 bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/async_default_impl.v
-0.18% 862.8 861.2 -1.5 bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/proof.v
-0.14% 942.2 940.8 -1.4 bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/setup.v
-0.13% 1243.4 1241.9 -1.6 bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/sync_impl.v
-0.13% 1092.6 1091.3 -1.4 bluerock/bhv/apps/vmm/proof/main_cpp_proof/zeta_main.v
-0.12% 972.7 971.5 -1.2 bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/portal_cpp_proof.v
-0.12% 1160.2 1158.8 -1.4 bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/route.v
-0.06% 127472.8 127390.8 -82.0 total
+0.00% 22690.6 22690.6 +0.0 ├ translation units
-0.08% 104700.2 104782.2 -82.0 └ proofs and tests

@gmalecha-at-skylabs gmalecha-at-skylabs changed the title A sketch of a refinement-based setup. Refinement-based specifications for iostream May 22, 2026
@gmalecha-at-skylabs gmalecha-at-skylabs force-pushed the gmalecha/refinement-iostream branch from 5bc608b to 72aa8c3 Compare May 22, 2026 19:53
@skylabs-ai-ci
Copy link
Copy Markdown

skylabs-ai-ci Bot commented May 22, 2026

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Base branch Base commit PR
fmdeps/brick-libcpp/ gmalecha/refinement-iostream ea408b0 main 2014908 #40

Passive Repos
Repo Job Branch Job Commit
./ main 7d2ee30
fmdeps/BRiCk/ main b96cddc
fmdeps/auto/ main ee152ab
fmdeps/auto-docs/ main d4c3641
bluerock/NOVA/ skylabs-proof dc3d314
bluerock/bhv/ skylabs-main c46f5e3
fmdeps/ci/ main 9e6e574
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 6a99b06
vendored/vsrocq/ skylabs-main 5b4527e

Performance

Relative Master MR Change Filename
-0.00% 127291.9 127291.9 -0.0 total
-0.00% 22689.7 22689.8 -0.0 ├ translation units
+0.00% 104602.2 104602.2 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
-0.00% 127291.9 127291.9 -0.0 total
-0.00% 22689.7 22689.8 -0.0 ├ translation units
+0.00% 104602.2 104602.2 +0.0 └ proofs and tests

@gmalecha-at-skylabs gmalecha-at-skylabs force-pushed the gmalecha/refinement-iostream branch from 72aa8c3 to 48d9282 Compare May 24, 2026 12:41
@skylabs-ai-ci
Copy link
Copy Markdown

skylabs-ai-ci Bot commented May 24, 2026

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Base branch Base commit PR
fmdeps/brick-libcpp/ gmalecha/refinement-iostream 816a72c main 2014908 #40

Passive Repos
Repo Job Branch Job Commit
./ main 7d2ee30
fmdeps/BRiCk/ main b96cddc
fmdeps/auto/ main ee152ab
fmdeps/auto-docs/ main d4c3641
bluerock/NOVA/ skylabs-proof dc3d314
bluerock/bhv/ skylabs-main c46f5e3
fmdeps/ci/ main 9e6e574
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 6a99b06
vendored/vsrocq/ skylabs-main 5b4527e

Performance

Relative Master MR Change Filename
-0.00% 127291.9 127291.9 -0.0 total
-0.00% 22689.7 22689.8 -0.0 ├ translation units
+0.00% 104602.2 104602.2 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
-0.00% 127291.9 127291.9 -0.0 total
-0.00% 22689.7 22689.8 -0.0 ├ translation units
+0.00% 104602.2 104602.2 +0.0 └ proofs and tests

@gmalecha-at-skylabs gmalecha-at-skylabs force-pushed the gmalecha/refinement-iostream branch from 48d9282 to 7adf95f Compare May 25, 2026 01:40
@gmalecha-at-skylabs
Copy link
Copy Markdown
Collaborator Author

gmalecha-at-skylabs commented May 25, 2026

The larger issues with this are really blocked on SkyLabsAI/BRiCk#126. Spectra does not seem to be packaged well for large scale usage.

@skylabs-ai-ci
Copy link
Copy Markdown

skylabs-ai-ci Bot commented May 25, 2026

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Base branch Base commit PR
fmdeps/brick-libcpp/ gmalecha/refinement-iostream f0361a0 main 2014908 #40

Passive Repos
Repo Job Branch Job Commit
./ main 7d2ee30
fmdeps/BRiCk/ main 3c1f27d
fmdeps/auto/ main bc3902f
fmdeps/auto-docs/ main d4c3641
bluerock/NOVA/ skylabs-proof dc3d314
bluerock/bhv/ skylabs-main 60d5c0f
fmdeps/ci/ main 9e6e574
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 77df1a1
vendored/vsrocq/ skylabs-main 5b4527e

Performance

Relative Master MR Change Filename
+0.00% 127763.3 127763.3 +0.0 total
+0.00% 22708.0 22708.0 +0.0 ├ translation units
+0.00% 105055.3 105055.3 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
+0.00% 127763.3 127763.3 +0.0 total
+0.00% 22708.0 22708.0 +0.0 ├ translation units
+0.00% 105055.3 105055.3 +0.0 └ proofs and tests

pgiarrusso-sl
pgiarrusso-sl approved these changes May 26, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@pgiarrusso-sl pgiarrusso-sl left a comment

Choose a reason for hiding this comment

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

The admits still seem there, but it looks like I reviewed, so approving.

@rlepigre-skylabs-ai rlepigre-skylabs-ai merged commit 04f4e3a into main May 27, 2026
8 checks passed
@rlepigre-skylabs-ai rlepigre-skylabs-ai deleted the gmalecha/refinement-iostream branch May 27, 2026 12:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@pgiarrusso-sl pgiarrusso-sl pgiarrusso-sl approved these changes

@mansky1 mansky1 Awaiting requested review from mansky1

@simon-skylabs simon-skylabs Awaiting requested review from simon-skylabs

Assignees

@gmalecha-at-skylabs gmalecha-at-skylabs

Labels

enhancement New feature or request

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@gmalecha-at-skylabs @pgiarrusso-sl @rlepigre-skylabs-ai