WIP on agent-generated ctime specs by pgiarrusso-sl · Pull Request #46 · SkyLabsAI/brick-libcpp

pgiarrusso-sl · 2026-04-09T12:21:34Z

Relevant to https://github.com/SkyLabsAI/agent-foundation/issues/37.

skylabs-ai-ci · 2026-04-09T12:29:31Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Base branch	Base commit	PR
fmdeps/brick-libcpp/	paolo/agent-ctime	a696737	main	cd4b46f	#46

Passive Repos

Repo	Job Branch	Job Commit
./	main	64a8e0d
fmdeps/BRiCk/	main	9ebe298
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

Looks nice!

gmalecha-at-skylabs · 2026-04-09T12:31:53Z

@@ -0,0 +1,44 @@
+(*
+ * Copyright (c) 2025 SkyLabs AI, Inc.


Suggested change

* Copyright (c) 2025 SkyLabs AI, Inc.

* Copyright (c) 2026 SkyLabs AI, Inc.

gmalecha-at-skylabs · 2026-04-09T12:32:33Z

@@ -0,0 +1,49 @@
+(*
+ * Copyright (c) 2025 SkyLabs AI, Inc.


Suggested change

* Copyright (c) 2025 SkyLabs AI, Inc.

* Copyright (c) 2026 SkyLabs AI, Inc.

gmalecha-at-skylabs · 2026-04-09T12:35:33Z

+Definition clock_t_model := Z.
+Definition time_t_model := Z.
+
+Parameter clock_result : clock_t_model -> Prop.


Maybe prefer naming this clock_t_wf or something like that?

gmalecha-at-skylabs · 2026-04-09T12:37:31Z

+     \post{t}[Vint t]
+       [| current_time_result t |] **
+       if bool_decide (timer_p = nullptr) then emp
+       else timer_p |-> primR Tlong 1$m (Vint t)).


Would it make sense to have a notation for time_tR?

gmalecha-at-skylabs · 2026-04-09T12:39:51Z

+  Parameter tmR_hidden :
+    cQp.t -> tm_model -> Z -> cstring.t -> Rep.
+  #[only(type_ptr="tm", cfracsplittable)] derive tmR_hidden.


Most of these are "obvious", but I don't really understand this one. It doesn't seem like the Z and cstring.t are relevant.

grep finds the answer in design.md:

tmR hides non-standard tm_gmtoff and tm_zone fields behind tmR_hidden, while timespecR tracks only tv_sec and tv_nsec.

See the source code:

/* ISO C `broken-down time' structure. */ struct tm { int tm_sec; /* Seconds. [0-60] (1 leap second) */ int tm_min; /* Minutes. [0-59] */ int tm_hour; /* Hours. [0-23] */ int tm_mday; /* Day. [1-31] */ int tm_mon; /* Month. [0-11] */ int tm_year; /* Year - 1900. */ int tm_wday; /* Day of week. [0-6] */ int tm_yday; /* Days in year.[0-365] */ int tm_isdst; /* DST. [-1/0/1]*/ # ifdef __USE_MISC long int tm_gmtoff; /* Seconds east of UTC. */ const char *tm_zone; /* Timezone abbreviation. */ # else long int __tm_gmtoff; /* Seconds east of UTC. */ const char *__tm_zone; /* Timezone abbreviation. */ # endif };

However, this is "malicious genie" compliance: the agent executed the plan, and since the plan forgets other fields, so did the agent.

Definition tmR (q : cQp.t) (tm : tm_model) : Rep := Exists gmtoff zone, tmR_hidden q tm gmtoff zone.

But the fix was easy

Please review again tmR, against both the plan and its job.

The agent even realized that, since tmR_hidden exposes a cstring.t model, it must owns the actual string, which is questionable. The agent correctly suggested exposing a ptr. I suggested exposing nothing to defer the whole question — it turns out this field points to static storage so the discipline requires more care.

skylabs-ai-ci · 2026-04-09T14:11:05Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Base branch	Base commit	PR
fmdeps/brick-libcpp/	paolo/agent-ctime	feb8836	main	cd4b46f	#46

Passive Repos

Repo	Job Branch	Job Commit
./	main	64a8e0d
fmdeps/BRiCk/	main	9ebe298
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

skylabs-ai-ci · 2026-04-09T18:19:44Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Base branch	Base commit	PR
fmdeps/brick-libcpp/	paolo/agent-ctime	7f50507	main	e96a0fc	#46

Passive Repos

Repo	Job Branch	Job Commit
./	main	64a8e0d
fmdeps/BRiCk/	main	594f065
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%	123490.4	123490.4	+0.0	total
+0.00%	22636.8	22636.8	+0.0	├ translation units
+0.00%	100853.6	100853.6	+0.0	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename

+0.00%	123490.4	123490.4	+0.0	total
+0.00%	22636.8	22636.8	+0.0	├ translation units
+0.00%	100853.6	100853.6	+0.0	└ proofs and tests

pgiarrusso-sl · 2026-04-09T22:58:19Z

+     \prepost{q tm_in} tm_p |-> tmR q tm_in
+     \post{t}[Vint t]
+       Exists tm_out,
+         [| mktime_result tm_in tm_out t |] **
+         tm_p |-> tmR q tm_out).


Buggy! I only noticed because tmR_learnable broke some client proof.

pgiarrusso-sl · 2026-04-09T22:58:38Z

+       if bool_decide (res = nullptr) then emp
+       else Exists out,
+         [| asctime_text_of tm out |] **
+         [| cstring.size out = 25 |] **


pgiarrusso-sl · 2026-04-09T22:59:31Z

+         [| utc_time_to_tm t tm |] **
+         res |-> tmR (cQp.const qret) tm **
+         □ (Forall (qret' : Qp),
+             res |-> tmR (cQp.const qret') tm ={⊤}=∗ emp)).


String-like borrowing 👀

skylabs-ai-ci · 2026-04-09T23:13:28Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Base branch	Base commit	PR
fmdeps/brick-libcpp/	paolo/agent-ctime	1430d35	main	e96a0fc	#46

Passive Repos

Repo	Job Branch	Job Commit
./	main	64a8e0d
fmdeps/BRiCk/	main	594f065
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%	123490.4	123490.4	+0.0	total
+0.00%	22636.8	22636.8	+0.0	├ translation units
+0.00%	100853.6	100853.6	+0.0	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename

+0.00%	123490.4	123490.4	+0.0	total
+0.00%	22636.8	22636.8	+0.0	├ translation units
+0.00%	100853.6	100853.6	+0.0	└ proofs and tests

skylabs-ai-ci · 2026-04-10T14:57:43Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Base branch	Base commit	PR
fmdeps/brick-libcpp/	paolo/agent-ctime	29dfeb8	main	e96a0fc	#46

Passive Repos

Repo	Job Branch	Job Commit
./	main	64a8e0d
fmdeps/BRiCk/	main	594f065
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%	123490.4	123490.4	-0.0	total
-0.00%	22636.8	22636.8	-0.0	├ translation units
+0.00%	100853.6	100853.6	+0.0	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename

-0.00%	123490.4	123490.4	-0.0	total
-0.00%	22636.8	22636.8	-0.0	├ translation units
+0.00%	100853.6	100853.6	+0.0	└ proofs and tests

> To fix the fatal failure, switch from `verify[module]` to `verify?[module]`, like you did before.

skylabs-ai-ci · 2026-04-15T08:16:33Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Base branch	Base commit	PR
fmdeps/brick-libcpp/	paolo/agent-ctime	e2347ff	main	e96a0fc	#46

Passive Repos

Repo	Job Branch	Job Commit
./	main	6d9572d
fmdeps/BRiCk/	main	ceb6c7b
fmdeps/auto/	main	d39dc2d
fmdeps/auto-docs/	main	9f57097
bluerock/NOVA/	skylabs-proof	e9a69cc
bluerock/bhv/	skylabs-main	e1da62f
fmdeps/ci/	main	f2d3e2d
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	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%	123301.6	123301.6	-0.0	total
-0.00%	22636.8	22636.8	-0.0	├ translation units
+0.00%	100664.8	100664.8	+0.0	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename

-0.00%	123301.6	123301.6	-0.0	total
-0.00%	22636.8	22636.8	-0.0	├ translation units
+0.00%	100664.8	100664.8	+0.0	└ proofs and tests

skylabs-ai-ci · 2026-04-23T13:23:41Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Base branch	Base commit	PR
fmdeps/brick-libcpp/	paolo/agent-ctime	60690bc	main	e96a0fc	#46

Passive Repos

Repo	Job Branch	Job Commit
./	main	e8e81bb
fmdeps/BRiCk/	main	e219b6b
fmdeps/auto/	main	26885ed
fmdeps/auto-docs/	main	9f57097
bluerock/NOVA/	skylabs-proof	e9a69cc
bluerock/bhv/	skylabs-main	e1da62f
fmdeps/ci/	main	749706e
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	3bed8c2
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%	123356.6	123356.6	-0.0	total
-0.00%	22637.5	22637.5	-0.0	├ translation units
+0.00%	100719.1	100719.1	+0.0	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename

-0.00%	123356.6	123356.6	-0.0	total
-0.00%	22637.5	22637.5	-0.0	├ translation units
+0.00%	100719.1	100719.1	+0.0	└ proofs and tests

gmalecha-at-skylabs reviewed Apr 9, 2026

View reviewed changes

pgiarrusso-sl commented Apr 9, 2026

View reviewed changes

pgiarrusso-sl mentioned this pull request Apr 13, 2026

Specifying POD construction/destruction is impossible SkyLabsAI/BRiCk#113

Open

pgiarrusso-sl added 14 commits April 15, 2026 10:07

First attempt at agent-generated ctime specs

7593257

Delete debugging nonsense from specs

732bd10

Iterate on specs

4f3e7eb

One more pass

16cbfca

More proof repairs

1633ab8

Manual proof repair

d44541c

Automated proof repair for new prelude

52521f6

Fix bug reports

d14c16e

> To fix the fatal failure, switch from `verify[module]` to `verify?[module]`, like you did before.

Add tmR_learnable, fix mktime spec and clients

06f90a7

Some more proof repair

f73b6ff

Next attempt

1b22996

Agent-generated edits (weakens lemmas)

0bfdab9

Revise helper lemmas by hand (strengthens lemmas again)

862bc06

More agent work on tmR/tmR_hidden

ce49386

pgiarrusso-sl force-pushed the paolo/agent-ctime branch from 9ce6863 to ce49386 Compare April 15, 2026 08:07

pgiarrusso-sl mentioned this pull request Apr 21, 2026

Refactor specs in unique_lock #47

Closed

pgiarrusso-sl added 2 commits April 23, 2026 15:14

More edits

65332e8

Questionable edits

98ef5fc

WIP outputs (valuable?)

d4abf5a

	* Copyright (c) 2025 SkyLabs AI, Inc.
	* Copyright (c) 2026 SkyLabs AI, Inc.

Conversation

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

Uh oh!

Uh oh!

skylabs-ai-ci Bot commented Apr 9, 2026

CI summary (Details)

Active Repos

Passive Repos

Performance

Uh oh!

gmalecha-at-skylabs 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 Apr 9, 2026

CI summary (Details)

Active Repos

Passive Repos

Performance

Uh oh!

skylabs-ai-ci Bot commented Apr 9, 2026

CI summary (Details)

Active Repos

Passive Repos

Performance

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

pgiarrusso-sl Apr 9, 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!

skylabs-ai-ci Bot commented Apr 9, 2026

CI summary (Details)

Active Repos

Passive Repos

Performance

Uh oh!

skylabs-ai-ci Bot commented Apr 10, 2026

CI summary (Details)

Active Repos

Passive Repos

Performance

Uh oh!

skylabs-ai-ci Bot commented Apr 15, 2026

CI summary (Details)

Active Repos

Passive Repos

Performance

Uh oh!

skylabs-ai-ci Bot commented Apr 23, 2026

CI summary (Details)

Active Repos

Passive Repos

Performance

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

pgiarrusso-sl commented Apr 9, 2026 •

edited

Loading

pgiarrusso-sl Apr 9, 2026 •

edited

Loading