A sketch of a refinement-based setup. by gmalecha-at-skylabs · Pull Request #40 · SkyLabsAI/brick-libcpp

gmalecha-at-skylabs · 2026-02-13T04:59:24Z

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.

skylabs-ai-ci · 2026-02-13T05:06:39Z

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

skylabs-ai-ci · 2026-03-05T04:24:56Z

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

skylabs-ai-ci · 2026-04-08T20:01:51Z

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 · 2026-04-11T15:11:57Z

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

pgiarrusso-sl · 2026-04-13T18:58:11Z

+{ do : evt -> PROP -> PROP
+  (** This is effectively an <<AU>> that performs the event and then continues *)
+}.
+


Implementation note: This class has no mode — that's a problem. But should it be deduced via TC inference?

gmalecha-at-skylabs · 2026-04-13T19:54:57Z

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

Introduce a generic [SepHandler] that embeds arbitrary actions into predicate transformers.

Other cleanup to start expanding.

skylabs-ai-ci · 2026-05-01T18:37:19Z

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 · 2026-05-01T18:41:56Z

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

gmalecha-at-skylabs · 2026-05-01T18:42:29Z

+CoInductive itree {E : Type -> Type} {T : Type} : Type :=
+| Ret (_ : T)
+| Tau (_ : itree)
+| Do {U} (_ : E U) (_ : U -> itree).
+#[global] Arguments itree E T : clear implicits.
+
+Section with_E.
+  Context {E : Type -> Type}.
+
+  CoFixpoint bind {T U} (it : itree E T) (k : T -> itree E U) : itree E U :=
+    match it with
+    | Ret v => k v
+    | Tau it => Tau (bind it k)
+    | Do e k' => Do e (fun x => bind (k' x) k)
+    end.
+
+End with_E.


It would be nice to replace this with the actual itree library. https://rocq-prover.org/p/coq-itree/5.2.1

skylabs-ai-ci · 2026-05-01T18:49:13Z

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 · 2026-05-01T19:31:51Z

+
+    Generally, this will be an <AU> that proves that <evt> is a valid next event.
+ *)
+Class SepHandler (PROP : bi) (evt : Type) : Type :=


(Still no mode?)

gmalecha-at-skylabs self-assigned this Feb 13, 2026

pgiarrusso-sl force-pushed the paolo/eval-old-release branch from 3594482 to a6e495d Compare February 17, 2026 14:49

pgiarrusso-sl force-pushed the paolo/eval-old-release branch from a6e495d to ef8cae9 Compare February 27, 2026 16:45

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

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 commented Apr 7, 2026

View reviewed changes

Comment thread rocq-brick-libstdcpp/test/geeks_for_geeks_examples/spec.v Outdated

gmalecha-at-skylabs force-pushed the gmalecha/refinement-iostream branch from 7ed54b8 to fbdf351 Compare April 8, 2026 19:54

gmalecha-at-skylabs requested a review from mansky1 April 8, 2026 19:56

gmalecha-at-skylabs added the enhancement New feature or request label Apr 8, 2026

gmalecha-at-skylabs commented Apr 8, 2026

View reviewed changes

Comment thread rocq-brick-libstdcpp/proof/iostream/spec.v Outdated

gmalecha-at-skylabs commented Apr 9, 2026

View reviewed changes

Comment thread rocq-brick-libstdcpp/proof/iostream/spec.v Outdated

pgiarrusso-sl reviewed Apr 13, 2026

View reviewed changes

gmalecha-at-skylabs force-pushed the gmalecha/refinement-iostream branch from 817c28a to 7eb3908 Compare April 13, 2026 19:07

gmalecha-at-skylabs added 11 commits May 1, 2026 08:18

A sketch of a refinement-based setup.

9fff975

Fleshing out the example.

159dce6

Re-organize the refinement setup

e35dff2

Introduce a generic [SepHandler] that embeds arbitrary actions into predicate transformers.

WIP

88d17a5

Working on the proofs.

966c93e

Proof cleanup

4ec8a04

Changing the event interface to [N]

a07a78c

Other cleanup to start expanding.

Proof of [N4_sum]

635fd64

Fix iostream spec

1dda8d7

Verify the [_swap_a] files

6d28ca4

Ported all of the examples

aad71ce

Re-organization

0308df5

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

Some notes about refinement

7607482

gmalecha-at-skylabs commented May 1, 2026

View reviewed changes

pgiarrusso-sl reviewed May 1, 2026

View reviewed changes

gmalecha-at-skylabs requested review from pgiarrusso-sl and simon-skylabs May 4, 2026 14:49

Conversation

gmalecha-at-skylabs commented Feb 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

skylabs-ai-ci Bot commented Feb 13, 2026

CI summary (Details)

Active Repos

Passive Repos

Performance

Uh oh!

skylabs-ai-ci Bot commented Mar 5, 2026

CI summary (Details)

Active Repos

Passive Repos

Performance

Uh oh!

Uh oh!

Uh oh!

skylabs-ai-ci Bot commented Apr 8, 2026

CI summary (Details)

Active Repos

Passive Repos

Performance

Uh oh!

Uh oh!

gmalecha-at-skylabs commented Apr 11, 2026

Uh oh!

pgiarrusso-sl Apr 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

gmalecha-at-skylabs commented Apr 13, 2026

Uh oh!

skylabs-ai-ci Bot commented May 1, 2026

CI summary (Details)

Active Repos

Passive Repos

Performance

Uh oh!

gmalecha-at-skylabs commented May 1, 2026

Uh oh!

gmalecha-at-skylabs May 1, 2026

Choose a reason for hiding this comment

Uh oh!

skylabs-ai-ci Bot commented May 1, 2026

CI summary (Details)

Active Repos

Passive Repos

Performance

Uh oh!

pgiarrusso-sl May 1, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

gmalecha-at-skylabs commented Feb 13, 2026 •

edited

Loading

pgiarrusso-sl Apr 13, 2026 •

edited

Loading