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

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

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.

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-06T16:54:42Z

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 · 2026-05-07T13:36:53Z

+     the event signature. *)
+  #[program]
+  Definition OS (E : coPset) γ : Ostream :=
+    {| do evt K := Step.requester Area E γ evt K |}%I.


Prefer evt for single events and evts for multiple ones.

Suggested change

{| do evt K := Step.requester Area E γ evt K |}%I.

{| do evts K := Step.requester Area E γ evts K |}%I.

pgiarrusso-sl · 2026-05-07T13:37:07Z

+     the event signature. *)
+  #[program]
+  Definition OS (E : coPset) γ : Ostream :=
+  {| do evt K := Step.requester HelloWorld E γ evt K |}%I.


Here (and throughout):

Suggested change

{| do evt K := Step.requester HelloWorld E γ evt K |}%I.

{| do evts K := Step.requester HelloWorld E γ evts K |}%I.

pgiarrusso-sl

We agreed to keep both specs side by side.

I'll review accordingly.

pgiarrusso-sl · 2026-05-07T14:12:02Z

+    iIntros "_" (??? ->). iIntros "$".
+  Qed.
+End to_auto.
+#[global] Hint Resolve pick_ex_C | 200 : sl_opacity.


Upstreamed?

pgiarrusso-sl

Some more comments.

pgiarrusso-sl · 2026-05-07T14:16:56Z

+      (_ : AnySteps Mid evts Post)
+    : AnySteps Pre (evt :: evts) Post
+  | Refine {Pre'} {_ : ∅ ⊂ Pre} (_ : Pre' ⊆ Pre) {es Post} :
+    AnySteps Pre' es Post -> AnySteps Pre es Post.


It seems this does not allow tau steps?

Also, it seems AnySteps might satisfy some rules — I wasn't sure, so wrote proofs and noticed a mismatch with my assumptions:

#57

pgiarrusso-sl · 2026-05-07T14:20:18Z

+
+  Class AnyStep  (Pre : propset T) (evt : E) (Post : propset T) : Prop :=
+  { _safe : forall s, s ∈ Pre -> exists s', step s (Some evt) s'
+  ; _steps_to : forall s', s' ∈ Post -> ∃ s, s ∈ Pre /\ step s (Some evt) s' }.


Suggested change

; _steps_to : forall s', s' ∈ Post -> ∃ s, s ∈ Pre /\ step s (Some evt) s' }.

(** [AnyStep Pre evt Post] means [Post] is _the_ set of all [evt]-successors to [Pre],

where [post] is an [evt]-successor to [pre] if and only if [step pre (Some evt) post].

Here we exclude tau steps.

*)

Class AnyStep (Pre : propset T) (evt : E) (Post : propset T) : Prop :=

{ _sound : forall s, s ∈ Pre -> exists s', step s (Some evt) s'

; _complete : forall s', s' ∈ Post -> ∃ s, s ∈ Pre /\ step s (Some evt) s' }.

This comment is currently wrong without my suggested fix to _safe.

pgiarrusso-sl · 2026-05-07T14:36:10Z

+  Context {T E} (step : T -> option E -> T -> Prop).
+
+  Class AnyStep  (Pre : propset T) (evt : E) (Post : propset T) : Prop :=
+  { _safe : forall s, s ∈ Pre -> exists s', step s (Some evt) s'


Can I assume

Suggested change

{ _safe : forall s, s ∈ Pre -> exists s', step s (Some evt) s'

{ _safe : forall s, s ∈ Pre -> exists s', step s (Some evt) s' /\ s ∈ Post

pgiarrusso-sl · 2026-05-07T14:48:14Z

+    intros.
+    iIntros "F" (?) "K".
+    rewrite /Step.requester.
+  Admitted.


Should we fix this and other admits before merging?

skylabs-ai-ci · 2026-05-07T16:09:08Z

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

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

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

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

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

gmalecha-at-skylabs commented May 1, 2026

View reviewed changes

Comment thread rocq-brick-libstdcpp/proof/iostream/itree.v

pgiarrusso-sl reviewed May 1, 2026

View reviewed changes

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

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

pgiarrusso-sl reviewed May 7, 2026

View reviewed changes

pgiarrusso-sl requested changes May 7, 2026

View reviewed changes

pgiarrusso-sl reviewed May 7, 2026

View reviewed changes

gmalecha-at-skylabs added 3 commits May 7, 2026 11:51

Rename [iostream] -> [iostream_trace]

fed2e2e

Refinement-based specifications of iostream

0db042e

Split out [itree_prop] and do some cleanup

5200a21

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

	{\| do evt K := Step.requester Area E γ evt K \|}%I.
	{\| do evts K := Step.requester Area E γ evts K \|}%I.

	{\| do evt K := Step.requester HelloWorld E γ evt K \|}%I.
	{\| do evts K := Step.requester HelloWorld E γ evts K \|}%I.

-  ; _steps_to : forall s', s' ∈ Post -> ∃ s, s ∈ Pre /\ step s (Some evt) s' }.
+  (** [AnyStep Pre evt Post] means [Post] is _the_ set of all [evt]-successors to [Pre],
+  where [post] is an [evt]-successor to [pre] if and only if [step pre (Some evt) post].
+ Here we exclude tau steps.
+  *)
+  Class AnyStep  (Pre : propset T) (evt : E) (Post : propset T) : Prop :=
+  { _sound : forall s, s ∈ Pre -> exists s', step s (Some evt) s'
+  ; _complete : forall s', s' ∈ Post -> ∃ s, s ∈ Pre /\ step s (Some evt) s' }.

	{ _safe : forall s, s ∈ Pre -> exists s', step s (Some evt) s'
	{ _safe : forall s, s ∈ Pre -> exists s', step s (Some evt) s' /\ s ∈ Post

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!

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!

Uh oh!

skylabs-ai-ci Bot commented May 1, 2026

CI summary (Details)

Active Repos

Passive Repos

Performance

Uh oh!

Uh oh!

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

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

pgiarrusso-sl left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

pgiarrusso-sl left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

skylabs-ai-ci Bot commented May 7, 2026

CI summary (Details)

Active Repos

Passive Repos

Performance

Uh oh!

Reviewers

gmalecha-at-skylabs commented Feb 13, 2026 •

edited

Loading

pgiarrusso-sl commented May 6, 2026 •

edited

Loading