[WIP] Invariants #2973
[WIP] Invariants #2973
Conversation
gherrit-pr-id: G2e56baadbd39a08c821418704f521a2cdd8d0e1f
Summary of ChangesHello @joshlf, I'm Gemini Code Assist1! I'm currently reviewing this pull request and will post my feedback shortly. In the meantime, here's a summary to help you and other reviewers quickly get up to speed! This pull request introduces foundational support for defining and enforcing data structure invariants within the Hermes verification toolchain. By allowing users to specify invariants for Rust structs via doc comments, the system can now automatically generate corresponding Lean Highlights
🧠 New Feature in Public Preview: You can now enable Memory to help Gemini Code Assist learn from your team's feedback. This makes future code reviews more consistent and personalized to your project's style. Click here to enable Memory in your admin console. Changelog
Using Gemini Code AssistThe full guide for Gemini Code Assist can be found on our documentation page, here are some quick tips. Invoking Gemini You can request assistance from Gemini at any point by creating a comment using either
Customization To customize Gemini Code Assist for GitHub experience, repository maintainers can create a configuration file and/or provide a custom code review style guide (such as PEP-8 for Python) by creating and adding files to a Limitations & Feedback Gemini Code Assist may make mistakes. Please leave feedback on any instances where its feedback is incorrect or counter productive. You can react with 👍 and 👎 on @gemini-code-assist comments. If you're interested in giving your feedback about your experience with Gemini Code Assist for Github and other Google products, sign up here. You can also get AI-powered code generation, chat, as well as code reviews directly in the IDE at no cost with the Gemini Code Assist IDE Extension. Footnotes
|
![gemini-code-assist[bot]](https://avatars.githubusercontent.com/in/956858?s=60&v=4){kind=small}
There was a problem hiding this comment.
Code Review
This pull request introduces support for struct invariants, a significant and valuable feature for the verification pipeline. The changes span from parsing new ///@ lean invariant annotations to generating Verifiable typeclass instances and injecting validity checks for function arguments and return values in the generated Lean code. The implementation is comprehensive, including new tests that validate the end-to-end functionality.
My review focuses on improving code maintainability and performance. I've identified a case of code duplication in the parser and an opportunity to use a more efficient string building pattern in the desugaring logic.
Overall, this is a great addition. Addressing the feedback will make the new code more robust and easier to maintain.
| let invariant = if !invariant_lines.is_empty() { | ||
| let mut full_inv = invariant_lines.join("\n").trim().to_string(); | ||
| // Strip "is_valid self :=" or "is_valid :=" | ||
| if let Some(rest) = full_inv.strip_prefix("is_valid") { | ||
| let rest = rest.trim(); | ||
| if let Some(rest) = rest.strip_prefix("self") { | ||
| let rest = rest.trim(); | ||
| if let Some(rest) = rest.strip_prefix(":=") { | ||
| full_inv = rest.trim().to_string(); | ||
| } | ||
| } else if let Some(rest) = rest.strip_prefix(":=") { | ||
| full_inv = rest.trim().to_string(); | ||
| } | ||
| } | ||
| Some(full_inv) | ||
| } else { | ||
| None | ||
| }; |
There was a problem hiding this comment.
This block of code for stripping prefixes from the joined invariant string is very similar to the logic on lines 141-152, which operates on the first line of an invariant. This duplication can be avoided by extracting the logic into a helper function. This would improve maintainability and reduce the chance of bugs if the logic needs to be updated in the future.
A single helper function could be used in both places to keep the parsing logic consistent and DRY (Don't Repeat Yourself).
| for binder in binders { | ||
| if binder != "_" { | ||
| out.push_str(&format!(" /\\ Verifiable.is_valid {}", binder)); | ||
| } | ||
| } |
There was a problem hiding this comment.
Calling format! inside a loop to build a string can be inefficient due to repeated memory allocations. A more idiomatic and performant approach is to use std::fmt::Write's write! macro, which appends to the string without creating intermediate String objects.
You'll need to add use std::fmt::Write; at the top of the file.
| for binder in binders { | |
| if binder != "_" { | |
| out.push_str(&format!(" /\\ Verifiable.is_valid {}", binder)); | |
| } | |
| } | |
| for binder in binders { | |
| if binder != "_" { | |
| // The write! macro is more efficient here. | |
| write!(out, " /\\ Verifiable.is_valid {}", binder).unwrap(); | |
| } | |
| } |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## Gb85ad5e55a47c49ab2c049a2ec5972fc6d082e31 #2973 +/- ##
============================================================================
Coverage ? 92.02%
============================================================================
Files ? 19
Lines ? 6029
Branches ? 0
============================================================================
Hits ? 5548
Misses ? 481
Partials ? 0 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
2 participants
Latest Update: v2 — Compare vs v1
📚 Full Patch History
Links show the diff between the row version and the column version.
⬇️ Download this PR
Branch
git fetch origin refs/heads/G2e56baadbd39a08c821418704f521a2cdd8d0e1f && git checkout -b pr-G2e56baadbd39a08c821418704f521a2cdd8d0e1f FETCH_HEADCheckout
git fetch origin refs/heads/G2e56baadbd39a08c821418704f521a2cdd8d0e1f && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/G2e56baadbd39a08c821418704f521a2cdd8d0e1f && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.