cstring: reviewed specs, with test clients — slice 1#53
Open
LennartATSkylabsAI wants to merge 1 commit intomainfrom
Open
cstring: reviewed specs, with test clients — slice 1#53LennartATSkylabsAI wants to merge 1 commit intomainfrom
LennartATSkylabsAI wants to merge 1 commit intomainfrom
Conversation
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.2 | 124414.2 | -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.2 | 124414.2 | -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
changed the title
pgiarrusso-sl
changed the title
Closed
LennartATSkylabsAI
force-pushed
the
lennart/cstring-reviewed-specs
branch
from
ed85cfb to
0da3573
Compare
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | e8e81bb |
| fmdeps/BRiCk/ | main | 9ab35f8 |
| fmdeps/auto/ | main | e640dd6 |
| 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% | 124424.5 | 124424.5 | -0.0 | total |
| -0.00% | 22637.5 | 22637.5 | -0.0 | ├ translation units |
| +0.00% | 101787.0 | 101787.0 | +0.0 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -0.00% | 124424.5 | 124424.5 | -0.0 | total |
| -0.00% | 22637.5 | 22637.5 | -0.0 | ├ translation units |
| +0.00% | 101787.0 | 101787.0 | +0.0 | └ proofs and tests |
| if bool_decide (c = 0) then Some 0 else None | ||
| | BS.String ch rest => | ||
| if bool_decide (c = byte_ord ch) then Some 0 | ||
| else option_map (fun off => (1 + off)%Z) (strchr rest c) |
Contributor
There was a problem hiding this comment.
Here and below I'd expect
Suggested change
| else option_map (fun off => (1 + off)%Z) (strchr rest c) | |
| else Z.succ <$> (strchr rest c) |
- we have more theory for fmap
- less sure on Z.succ vs 1 +, but we use N.succ...
Contributor
There was a problem hiding this comment.
Taking a look since this might break clients.
| | BS.EmptyString => None | ||
| | BS.String ch rest => | ||
| if contains ch accept then Some 0 | ||
| else option_map (fun off => (1 + off)%Z) (strpbrk rest accept) |
Contributor
There was a problem hiding this comment.
Suggested change
| else option_map (fun off => (1 + off)%Z) (strpbrk rest accept) | |
| else Z.succ <$> (strpbrk rest accept) |
| | BS.EmptyString => None | ||
| | BS.String _ rest => | ||
| if prefix needle haystack then Some 0 | ||
| else option_map (fun off => (1 + off)%Z) (strstr rest needle) |
Contributor
There was a problem hiding this comment.
Suggested change
| else option_map (fun off => (1 + off)%Z) (strstr rest needle) | |
| else Z.succ <$> (strstr rest needle) |
| | nil => None | ||
| | b :: rest => | ||
| if bool_decide (b = byte_of_int c) then Some 0 | ||
| else option_map (fun off => (1 + off)%Z) (memchr rest c) |
Contributor
There was a problem hiding this comment.
Suggested change
| else option_map (fun off => (1 + off)%Z) (memchr rest c) | |
| else Z.succ <$> (memchr rest c) |
Comment on lines
+16
to
+29
| Notation search_result p found := | ||
| (match found with | ||
| | Some 0 => Vptr p | ||
| | Some off => Vptr (p .[ Tchar ! off ]) | ||
| | None => Vptr nullptr | ||
| end) (only parsing). | ||
|
|
||
| Notation byte_search_result byte_ty p found := | ||
| match found with | ||
| | Some 0 => Vptr p | ||
| | Some off => Vptr (p .[ byte_ty ! off ]) | ||
| | None => Vptr nullptr | ||
| end (only parsing). | ||
|
|
Contributor
There was a problem hiding this comment.
- I wouldn't expect specs to do pointer normalization
- Factoring
Vptrout helps reasoning - These are duplicates.
Suggested change
| Notation search_result p found := | |
| (match found with | |
| | Some 0 => Vptr p | |
| | Some off => Vptr (p .[ Tchar ! off ]) | |
| | None => Vptr nullptr | |
| end) (only parsing). | |
| Notation byte_search_result byte_ty p found := | |
| match found with | |
| | Some 0 => Vptr p | |
| | Some off => Vptr (p .[ byte_ty ! off ]) | |
| | None => Vptr nullptr | |
| end (only parsing). | |
| Notation byte_search_result byte_ty p found := | |
| Vptr (match found with | |
| | Some off => (p .[ byte_ty ! off ]) | |
| | None => nullptr | |
| end) (only parsing). | |
| Notation search_result p found := | |
| (byte_search_result Tchar p found) (only parsing). |
Comment on lines
+126
to
+129
| (* sound but weak in C++17: memchr behaves as if it reads the bytes | ||
| sequentially and stops as soon as a matching bytes is found: if the array | ||
| pointed to by ptr is smaller than count, but the match is found within the | ||
| array, the behavior is well-defined. *) |
Contributor
There was a problem hiding this comment.
"Sound but weak" is not appropriate for the spec with the \require.
This comment needs to be next to the weak version.
Comment on lines
+130
to
+157
| cpp.spec "memchr(void*, int, unsigned long)" as memchr_mut_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 => True | ||
| | None => (n <= hi)%Z | ||
| end | ||
| (*equivalently: \require hi >= n \/ (hi < n /\ exists off, memchr bytes c = Some off)*) | ||
| \post[byte_search_result Tuchar s_p | ||
| (memchr (takeZ n bytes) c)] emp). | ||
|
|
||
| cpp.spec "memchr(const void*, int, unsigned long)" as memchr_const_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 => True | ||
| | None => (n <= hi)%Z | ||
| end | ||
| (*equivalently: \require hi >= n \/ (hi < n /\ exists off, memchr bytes c = Some off)*) | ||
| \post[byte_search_result Tuchar s_p | ||
| (memchr (takeZ n bytes) c)] emp). | ||
|
|
Contributor
There was a problem hiding this comment.
No, we should leave this out as agreed. I'm okay commenting it out:
- proofs of clients will choose one of these specs — I think with this code they'd choose the strong bad version. We don't have a robust way to give non-default specs.
- this is unsound in earlier versions
- it's unclear how to best phrase it
- my opinion is 99% of clients shouldn't use the strong spec at all.
Suggested change
| cpp.spec "memchr(void*, int, unsigned long)" as memchr_mut_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 => True | |
| | None => (n <= hi)%Z | |
| end | |
| (*equivalently: \require hi >= n \/ (hi < n /\ exists off, memchr bytes c = Some off)*) | |
| \post[byte_search_result Tuchar s_p | |
| (memchr (takeZ n bytes) c)] emp). | |
| cpp.spec "memchr(const void*, int, unsigned long)" as memchr_const_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 => True | |
| | None => (n <= hi)%Z | |
| end | |
| (*equivalently: \require hi >= n \/ (hi < n /\ exists off, memchr bytes c = Some off)*) | |
| \post[byte_search_result Tuchar s_p | |
| (memchr (takeZ n bytes) c)] emp). | |
| (* Strong, but unsound before C++17, and awkward | |
| (* | |
| cpp.spec "memchr(void*, int, unsigned long)" as memchr_mut_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 => True | |
| | None => (n <= hi)%Z | |
| end | |
| (*equivalently: \require hi >= n \/ (hi < n /\ exists off, memchr bytes c = Some off)*) | |
| \post[byte_search_result Tuchar s_p | |
| (memchr (takeZ n bytes) c)] emp). | |
| cpp.spec "memchr(const void*, int, unsigned long)" as memchr_const_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 => True | |
| | None => (n <= hi)%Z | |
| end | |
| (*equivalently: \require hi >= n \/ (hi < n /\ exists off, memchr bytes c = Some off)*) | |
| \post[byte_search_result Tuchar s_p | |
| (memchr (takeZ n bytes) c)] emp). | |
| *) |
| rewrite arrayLR.unlock; arith_simpl; work. | ||
| rewrite _at_sub_0; [trivial|done]. | ||
| Qed. | ||
| Hint Resolve cstring_arrayLR : sl_opacity. |
Contributor
There was a problem hiding this comment.
Suggested change
| Hint Resolve cstring_arrayLR : sl_opacity. | |
| #[local] Hint Resolve cstring_arrayLR : sl_opacity. |
| rewrite _at_sub_0; [|done]. | ||
| rewrite /cstring.R /zstring.R; iFrame; done. | ||
| Qed. | ||
| Hint Resolve arrayLR_cstring : sl_opacity. |
Contributor
There was a problem hiding this comment.
Suggested change
| Hint Resolve arrayLR_cstring : sl_opacity. | |
| #[local] Hint Resolve arrayLR_cstring : sl_opacity. |
| if bool_decide (c = 0) then Some 0 else None | ||
| | BS.String ch rest => | ||
| if bool_decide (c = byte_ord ch) then Some 0 | ||
| else option_map (fun off => (1 + off)%Z) (strchr rest c) |
Contributor
There was a problem hiding this comment.
Taking a look since this might break clients.
LennartATSkylabsAI
force-pushed
the
lennart/cstring-reviewed-specs
branch
from
0da3573 to
79b0732
Compare
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | e8e81bb |
| fmdeps/BRiCk/ | main | 902bdd0 |
| fmdeps/auto/ | main | b45c3e8 |
| fmdeps/auto-docs/ | main | bfa8f2d |
| bluerock/NOVA/ | skylabs-proof | 6cbef03 |
| bluerock/bhv/ | skylabs-main | 448828c |
| fmdeps/ci/ | main | 6dff30c |
| 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 | 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 | 62d34c3 |
| vendored/vsrocq/ | skylabs-main | 5b4527e |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -0.00% | 124547.9 | 124547.9 | -0.0 | total |
| -0.00% | 22655.3 | 22655.3 | -0.0 | ├ translation units |
| +0.00% | 101892.6 | 101892.6 | +0.0 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -0.00% | 124547.9 | 124547.9 | -0.0 | total |
| -0.00% | 22655.3 | 22655.3 | -0.0 | ├ translation units |
| +0.00% | 101892.6 | 101892.6 | +0.0 | └ proofs and tests |
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
2 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.
This PR isolates reviewed specs from #48 and proofs of litmus tests
for 'true string' (as opposed to memchr etc) functions.
lessons-learned.md and proofs / proof attempts for remaining functions remain in #48.