Review std::optional<unsigned char> specification and proofs - #168
mahadkhan811 wants to merge 2 commits into
Conversation
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | db1581e |
| fmdeps/BRiCk/ | main | 389d262 |
| fmdeps/auto/ | main | 1158e34 |
| fmdeps/auto-docs/ | main | 6490c5f |
| bluerock/NOVA/ | skylabs-proof | bbb220a |
| bluerock/bhv/ | skylabs-main | e6646bb |
| fmdeps/ci/ | main | 6a09c2f |
| vendored/elpi/ | skylabs-master | c0b9653 |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| vendored/rocq/ | skylabs-master | bef7df5 |
| fmdeps/rocq-agent-toolkit/ | main | 227bb83 |
| vendored/rocq-elpi/ | skylabs-master | 7dee592 |
| vendored/rocq-equations/ | skylabs-main | 9cf8471 |
| vendored/rocq-iris/ | skylabs-master | a7af9f7 |
| vendored/rocq-lsp/ | skylabs-main | 64ef78a |
| vendored/rocq-stdlib/ | skylabs-master | 00897b3 |
| vendored/rocq-stdpp/ | skylabs-master | 0c5e505 |
| fmdeps/skylabs-fm/ | main | 69d6d20 |
| vendored/vsrocq/ | skylabs-main | ee79e7a |
No Changes in Warnings or Errors
| Before | New | Fixed | After | |
|---|---|---|---|---|
| Errors | 0 | 0 | 0 | 0 |
| Warnings | 117 | 0 | 0 | 117 |
Code quality details
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +0.00% | 197191.3 | 197191.3 | +0.0 | total |
| +0.00% | 53107.4 | 53107.4 | +0.0 | ├ translation units |
| +0.00% | 144083.9 | 144083.9 | +0.0 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +0.00% | 197191.3 | 197191.3 | +0.0 | total |
| +0.00% | 53107.4 | 53107.4 | +0.0 | ├ translation units |
| +0.00% | 144083.9 | 144083.9 | +0.0 | └ proofs and tests |
pgiarrusso-sl
left a comment
pgiarrusso-sl
left a comment
There was a problem hiding this comment.
My review is not complete, but I have some initial feedback.
At the high level:
-
compared to #110, this PR defines
Reps concretely instead of usingParameter/Axioms. This probably is a good idea, since it reduces the risk of vacuous/incorrect assumptions, but it makes the specs harder to apply to other versions, so we should discuss further. -
I will add some small comments on the code, but I will mark some as "nitpicks" because at the moment I don't know if it's worth addressing them — or lack budget to review fixes.
| Inductive state : Type := | ||
| | empty | ||
| | engaged (byte : Z). | ||
|
|
There was a problem hiding this comment.
This abstract is isomorphic to option Z, that's good. But the model seems to fail SwEng 101 — it reimplements it instead of reusing it.
| sl.lock | ||
| Definition optional_base_implR `{Σ : cpp_logic, σ : genv} | ||
| (q : cQp.t) : Rep := | ||
| structR | ||
| "std::_Optional_base_impl<unsigned char, std::_Optional_base<unsigned char, 1b, 1b>>" | ||
| q. | ||
| #[only(cfracsplittable,type_ptr,lazy_unfold(export))] derive optional_base_implR. |
There was a problem hiding this comment.
I wouldn't expect this predicate.
| CFracValid1 storageR. | ||
| Proof. constructor. intros q s. rewrite storageR.unlock. destruct s; apply _. Qed. | ||
| #[global] Instance storageR_cfrac_splittable `{Σ : cpp_logic, σ : genv} : | ||
| CFracSplittable_1 storageR := {}. |
There was a problem hiding this comment.
No action needed, but we should avoid CFracSplittable instances ( SkyLabsAI/BRiCk#282)
The LLM is confused because #[only(cfracsplittable)] derive R. doesn't produce CFracSplittable_1,
but I can't blame the model.
| CFracSplittable_1 storageR := {}. |
|
|
||
| (* Use [optional_value_ptr.unlock] when proving facts about the nested byte. *) | ||
| sl.lock | ||
| Definition optional_value_ptr `{σ : genv} (this : ptr) : ptr := |
There was a problem hiding this comment.
This should be an Abbreviation not locked.
| *) | ||
| Require Import skylabs.auto.cpp.prelude.proof. | ||
| Require Export skylabs.brick.libstdcpp.optional.model. | ||
|
|
There was a problem hiding this comment.
Software engineering problem: names like storageR are ambiguous when imported unqualified.
Action needed: best to wrap these predicates using NES.Begin and NES.End for namespacing; here, NES.Begin std.optional.
Recommended action: search any examples that violate this guideline, and fix them.
| CFracValid1 storageR. | ||
| Proof. constructor. intros q s. rewrite storageR.unlock. destruct s; apply _. Qed. | ||
| #[global] Instance storageR_cfrac_splittable `{Σ : cpp_logic, σ : genv} : | ||
| CFracSplittable_1 storageR := {}. |
There was a problem hiding this comment.
Nitpick not to fix here, but we should avoid CFracSplittable instances ( SkyLabsAI/BRiCk#282)
The LLM is confused because #[only(cfracsplittable)] derive R. doesn't produce CFracSplittable_1,
but I can't blame the model for being confused.
| CFracSplittable_1 storageR := {}. |
| - Are the representation and contract definitions idiomatic for this | ||
| repository? | ||
| - Do the three selected proofs demonstrate useful consequences of the spec, | ||
| rather than merely restating it? |
There was a problem hiding this comment.
- The abstract state should be
option Z, but at least is isomorphic to it. - The contract/specs look good at first sight.
- Some reps are not idiomatic, and I'm not yet sure they're used?
- The selected proofs seem actual consequences (unlike the old
oracleones). Coverage seems a bit low, but I assume that's because we wanted a small PR for review. Larger coverage will be required for real use..
2 participants
Summary
This PR adds a focused review packet for the
std::optional<unsigned char>specification on libstdc++ 12.It includes:
Qed.;Fail Qed.andAbort.;The client and proof directories are divided explicitly into
positive/andnegative/. All files are contained underspec-review/optional-unsigned-char/and are not connected to the repository Dune build.Review focus
Feedback is requested on:
Pipeline implementation, mutation testing, and generated execution evidence are outside this review.
Validation
Start with the review README.