Specification of cstring#48
Closed
LennartATSkylabsAI wants to merge 11 commits intomainfrom
Closed
Conversation
LennartATSkylabsAI
changed the title
CI summary (Details)Active 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 |
LennartATSkylabsAI
requested review from
Janno,
gmalecha-at-skylabs and
pgiarrusso-sl
CI summary (Details)Active 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 |
CI summary (Details)Active 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 |
Comment on lines
+42
to
+47
| The current explicit `char[]` litmus tests are slightly different: cpp2v | ||
| generates stack-array initializer resources as concrete `arrayR` predicates. | ||
| Their proofs therefore use local `arrayR` splitting/recombination lemmas to | ||
| match the generated proof state directly. This should not be read as a general | ||
| preference for `arrayR` in library specs; it is a proof-local accommodation for | ||
| the shape of generated stack-buffer resources. |
Collaborator
There was a problem hiding this comment.
From a technical PoV: "cpp2v generates ..." should be "BRiCk generates ..." since the logic is BRiCk.
Is it getting this information from reading BRiCk rules? If it was looking at proof states, then it should be seeing things after the arrayLR hints kick in.
Author
There was a problem hiding this comment.
Resolved in later PR, where the proof file uses the import statements from other verification case studies.
Comment on lines
+14
to
+21
| Definition ab_0_cd_lit : literal_string.t := | ||
| {| | ||
| literal_string.bytes := | ||
| PrimStringAxioms.of_list | ||
| [Uint63Axioms.of_Z 97; Uint63Axioms.of_Z 98; Uint63Axioms.of_Z 0; | ||
| Uint63Axioms.of_Z 99; Uint63Axioms.of_Z 100]; | ||
| literal_string.bytes_per_char := 1; | ||
| |}. |
Collaborator
There was a problem hiding this comment.
We should really implement some notation that takes standard C++ strings with escapes, this is pretty difficult to read.
CI summary (Details)Active 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 |
CI summary (Details)Active 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 |
CI summary (Details)Active 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 |
| (* | ||
| Archived exact [unsigned char] array specs. These were useful for the first | ||
| byte-array slice, but they are too narrow for the standard [void*] memory | ||
| APIs, whose textual specifications operate on object bytes. |
Contributor
There was a problem hiding this comment.
I think these specs are closer to what we'd prefer — the problem is real but we had separate plans about it.
Contributor
There was a problem hiding this comment.
In the meeting, we concluded these specs should use arrayR or arrayLR — dealing with object representations is out of scope for these specs/MRs.
Comment on lines
+135
to
+138
| \prepost{q bytes} s_p |-> arrayLR Tuchar 0 (Z.of_N n) | ||
| (fun b : Z => ucharR q b) bytes | ||
| \require lengthZ bytes = Z.of_N n | ||
| \post[byte_search_result s_p (memchr bytes c)] emp). |
Contributor
There was a problem hiding this comment.
This seems a weird way to use arrayLR.
Contributor
There was a problem hiding this comment.
We wondered about the best idiom to write these specs;
https://github.com/SkyLabsAI/psi_PROVER.data/pull/130 shows the "natural" one fails.
Author
There was a problem hiding this comment.
When given the text from https://cppreference.com/cpp/string/byte/memchr, codex proposes this:
cpp.spec "memchr(void*, int, unsigned long)" as memchr_mut_array_spec with
(\arg{s_p} "__s" (Vptr s_p)
\arg{c} "__c" (Vint c)
\arg{n} "__n" (Vn n)
\prepost{q bytes} s_p |-> arrayLR Tuchar 0 (lengthZ bytes)
(fun b : Z => ucharR q b) bytes
\require match memchr bytes c with
| Some off => (off < Z.of_N n / Z.of_N n <= lengthZ bytes)%Z
| None => (Z.of_N n <= lengthZ bytes)%Z
end
\post[byte_search_result Tuchar s_p
(memchr (takeZ (Z.of_N n) bytes) c)] emp).
That's a bit unwieldy but permits bytes to be short than n.
Author
There was a problem hiding this comment.
(and replacing ZLength bytes with fresh 'hi' and using Vint/Z instead of Vn/N/Z.ofN makes it a little nicer:pp.spec "memchr(void*, int, unsigned long)" as memchr_mut_array_spec with
(\arg{s_p} "__s" (Vptr s_p)
\arg{c} "__c" (Vint c)
\arg{n} "__n" (Vint n)
\prepost{q hi bytes} s_p |-> arrayLR Tuchar 0 hi
(fun b : Z => ucharR q b) bytes
\require match memchr bytes c with
| Some off => (off < n / n <= hi)%Z
| None => (n <= hi)%Z
end
\post[byte_search_result Tuchar s_p
(memchr (takeZ n bytes) c)] emp).
Contributor
There was a problem hiding this comment.
\require lengthZ bytes = Z.of_N n is redundant after all.
Contributor
There was a problem hiding this comment.
These comments are missing triple-backticks to mark code blocks...
That's a bit unwieldy but permits bytes to be short than n.
Apparently I was wrong there — as pointed in the meeting.
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | e8e81bb |
| fmdeps/BRiCk/ | main | 9ab35f8 |
| fmdeps/auto/ | main | e2c9c3e |
| fmdeps/auto-docs/ | main | bfa8f2d |
| bluerock/NOVA/ | skylabs-proof | e9a69cc |
| bluerock/bhv/ | skylabs-main | e1da62f |
| fmdeps/ci/ | main | e32c9d8 |
| 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 | a7722d5 |
| 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% | 123357.1 | 123357.1 | +0.0 | total |
| +0.00% | 22637.5 | 22637.5 | +0.0 | ├ translation units |
| +0.00% | 100719.6 | 100719.6 | +0.0 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +0.00% | 123357.1 | 123357.1 | +0.0 | total |
| +0.00% | 22637.5 | 22637.5 | +0.0 | ├ translation units |
| +0.00% | 100719.6 | 100719.6 | +0.0 | └ proofs and tests |
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | e8e81bb |
| fmdeps/BRiCk/ | main | 9ab35f8 |
| fmdeps/auto/ | main | e2c9c3e |
| fmdeps/auto-docs/ | main | bfa8f2d |
| bluerock/NOVA/ | skylabs-proof | e9a69cc |
| bluerock/bhv/ | skylabs-main | e1da62f |
| fmdeps/ci/ | main | e32c9d8 |
| 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 | a7722d5 |
| 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% | 123357.1 | 123357.1 | +0.0 | total |
| +0.00% | 22637.5 | 22637.5 | +0.0 | ├ translation units |
| +0.00% | 100719.6 | 100719.6 | +0.0 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +0.00% | 123357.1 | 123357.1 | +0.0 | total |
| +0.00% | 22637.5 | 22637.5 | +0.0 | ├ translation units |
| +0.00% | 100719.6 | 100719.6 | +0.0 | └ proofs and tests |
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | e8e81bb |
| fmdeps/BRiCk/ | main | 9ab35f8 |
| fmdeps/auto/ | main | e2c9c3e |
| fmdeps/auto-docs/ | main | bfa8f2d |
| bluerock/NOVA/ | skylabs-proof | e9a69cc |
| bluerock/bhv/ | skylabs-main | e1da62f |
| fmdeps/ci/ | main | e32c9d8 |
| 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 | a7722d5 |
| 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% | 123357.1 | 123357.1 | +0.0 | total |
| +0.00% | 22637.5 | 22637.5 | +0.0 | ├ translation units |
| +0.00% | 100719.6 | 100719.6 | +0.0 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +0.00% | 123357.1 | 123357.1 | +0.0 | total |
| +0.00% | 22637.5 | 22637.5 | +0.0 | ├ translation units |
| +0.00% | 100719.6 | 100719.6 | +0.0 | └ proofs and tests |
| (\arg{s_p} "__s" (Vptr s_p) | ||
| \prepost{q s} s_p |-> cstring.R q s | ||
| \require valid<"unsigned long"> (cstring.strlen s) | ||
| \post[Vn (Z.to_N (cstring.strlen s))] emp). |
Contributor
There was a problem hiding this comment.
We fixed this in review. We should teach the agent (after merge).
| @@ -0,0 +1,36 @@ | |||
| (* | |||
Contributor
There was a problem hiding this comment.
Consider removing this _old file.
| @@ -0,0 +1,188 @@ | |||
| (* | |||
Contributor
There was a problem hiding this comment.
Consider removing this _old file.
| * This software is distributed under the terms of the BedRock Open-Source License. | ||
| * See the LICENSE-BedRock file in the repository root for details. | ||
| *) | ||
| Require Import skylabs.prelude.numbers. |
Contributor
There was a problem hiding this comment.
Consider removing this _old file.
| whether the model can produce an arithmetic expression that | ||
| `Arith.arith_simpl` can normalize. Avoid local tactics that know about one | ||
| test's concrete offsets or string literals. | ||
| - `ego` is not always redundant after `go`. In these litmus proofs it often |
Contributor
There was a problem hiding this comment.
I'd say go is redundant before ego, go. ego. is equivalent to ego.
Using go and fixing learning hints is often better.
Comment on lines
+86
to
+93
| - When proof automation is the goal, directional `_F` / `_B` / `_C`-style | ||
| hints are usually a better fit than borrowing lemmas. Borrowing lemmas are | ||
| continuation-oriented: open a view now, use it locally, and close it later. | ||
| Many reusable BRiCk proof steps are instead directional transformations: | ||
| decompose what is already in context, rebuild a canonical goal shape, or | ||
| replace one resource view by another. Keep semantically meaningful | ||
| split/rebuild steps as ordinary lemmas, and only package them as hints when | ||
| the step is routine enough that proof search should apply it opportunistically. |
Contributor
There was a problem hiding this comment.
Suggested change
| - When proof automation is the goal, directional `_F` / `_B` / `_C`-style | |
| hints are usually a better fit than borrowing lemmas. Borrowing lemmas are | |
| continuation-oriented: open a view now, use it locally, and close it later. | |
| Many reusable BRiCk proof steps are instead directional transformations: | |
| decompose what is already in context, rebuild a canonical goal shape, or | |
| replace one resource view by another. Keep semantically meaningful | |
| split/rebuild steps as ordinary lemmas, and only package them as hints when | |
| the step is routine enough that proof search should apply it opportunistically. |
Rejected as slop.
Comment on lines
+94
to
+96
| - For `\cancelx` hints, “provable” and “useful to automation” are different | ||
| thresholds. In this development, some `_guard` and `_using` variants could be | ||
| proved but still did not fire under `go`/`ego` at the relevant call site. |
Contributor
There was a problem hiding this comment.
This is verbose for
Suggested change
| - For `\cancelx` hints, “provable” and “useful to automation” are different | |
| thresholds. In this development, some `_guard` and `_using` variants could be | |
| proved but still did not fire under `go`/`ego` at the relevant call site. | |
| - Not all provable hints help client automation. |
which seems redundant
Suggested change
| - For `\cancelx` hints, “provable” and “useful to automation” are different | |
| thresholds. In this development, some `_guard` and `_using` variants could be | |
| proved but still did not fire under `go`/`ego` at the relevant call site. |
Comment on lines
+97
to
+100
| - If a side fact depends on a variable that will only be learned from the | ||
| consumed resources, putting that fact in `\using` may be too early. In such | ||
| cases, ordinary hint parameters or premises can be a better automation | ||
| surface than a more internal-looking `\cancelx` clause. |
Contributor
There was a problem hiding this comment.
This seems either meaningless, wrong or confusing?
| - Relatedly, ordinary hint parameters can sometimes outperform richer internal | ||
| clause structure. Even when a witness or equality seems conceptually “inside” | ||
| the hint, exposing it as an ordinary premise may let hint search instantiate | ||
| it more effectively. |
Contributor
There was a problem hiding this comment.
Slop
Suggested change
| it more effectively. |
Comment on lines
+116
to
+119
| - Hint matching is very intensional. A reformulation that replaces compound | ||
| expressions by variables such as `mid` and `k`, together with simple equality | ||
| premises, can fire much more reliably because it matches the post-call proof | ||
| state more directly. |
Contributor
There was a problem hiding this comment.
This is a terrible explanation of a true fact.
| from concrete data. In wrapper obligations, converting such a premise with | ||
| `%RedEq_eq` gives back an ordinary equality while keeping the client-facing | ||
| hint surface computation-friendly. | ||
| - In the `memset` family, a direct Family A opener can be worthwhile even when |
Contributor
There was a problem hiding this comment.
Do we have family A/B/C?
| @@ -0,0 +1,151 @@ | |||
| # Lessons Learned | |||
Contributor
There was a problem hiding this comment.
I'm not sure we should commit such lessons in a public repository. For now, I'd move it to a follow-up PR and merge the rest.
Contributor
There was a problem hiding this comment.
I've also left lots of comments about these lessons, even if we probably can't act on them here.
Comment on lines
+33
to
+35
| - When a standard API is phrased in terms of object representation bytes, avoid | ||
| overspecifying the storage type. An abstract byte predicate is closer to the | ||
| text than a spec that insists on a concrete `unsigned char[]` object. |
Contributor
There was a problem hiding this comment.
Outdated/counterproductive.
Suggested change
| - When a standard API is phrased in terms of object representation bytes, avoid | |
| overspecifying the storage type. An abstract byte predicate is closer to the | |
| text than a spec that insists on a concrete `unsigned char[]` object. |
Comment on lines
+25
to
+28
| - Match the abstraction to the API surface. Null-terminated string functions | ||
| want a string predicate such as `cstring.R`; counted byte APIs want a counted | ||
| byte predicate such as `object_bytesR`, not a string predicate with an | ||
| accidental terminator interpretation. |
Contributor
There was a problem hiding this comment.
Suggested change
| - Match the abstraction to the API surface. Null-terminated string functions | |
| want a string predicate such as `cstring.R`; counted byte APIs want a counted | |
| byte predicate such as `object_bytesR`, not a string predicate with an | |
| accidental terminator interpretation. |
-
The mention of
object_bytesRis outdated -
We did the opposite of what this advice suggests.
-
Lots of this advice seems a verbose way to be entirely redundant — "don't use
ARwhen a spec requiresBR" adds nothing to "write sound specifications" + the semantics of specs. Do we have that semantics?
…tial set of functions using ctring.R and a lower-level alternative cstringz.R
…spn, strcspn, strpbrk, and strstr
…non-ergonomic proofs)
…hr|move} remain ugly
LennartATSkylabsAI
force-pushed
the
lennart/cstring
branch
from
f19562d to
699fffd
Compare
CI summary (Details)Active 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 |
Collaborator
|
We won't merge this because we will merge #48 |
Author
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Parent issue: https://github.com/SkyLabsAI/agent-foundation/issues/78
Added project layout, md files for verification of cstring. Proved initial set of functions using cstring.R and a lower-level alternative cstringz.R.