[WIP] Stitching engine #2971
[WIP] Stitching engine #2971
Conversation
gherrit-pr-id: G443fc7f8c3623131b48be56a7a16935a9fe8f234
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 a significant refactoring and enhancement to the Hermes tool's ability to "stitch" Rust code with Lean proofs. It establishes a new desugaring engine that interprets a more expressive specification language for Rust functions, allowing users to define 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
Activity
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 a "stitching engine" to translate user-provided specs in Rust doc comments into Lean theorems. This is a significant feature that simplifies the spec syntax for users to a more intuitive ensures |...| format. The implementation involves adding new desugar and translator modules, and refactoring the parser and pipeline to integrate this new logic. The changes are well-structured. My review includes a couple of suggestions to improve the quality of the generated Lean code and to fix a test case that wasn't correctly testing the new functionality.
| let res = parse_file(content); | ||
| if let Err(e) = &res { | ||
| println!("Error: {}", e); | ||
| } | ||
| assert!(res.is_ok()); |
There was a problem hiding this comment.
This test is currently calling syn::parse_file, which only checks if the provided string is valid Rust syntax. It doesn't test any of the spec extraction logic in this module.
To make this test effective, it should call extract_blocks and assert that the specs and proofs are parsed correctly.
let res = extract_blocks(content);
if let Err(e) = &res {
println!("Error: {}", e);
}
assert!(res.is_ok());
assert_eq!(res.unwrap().functions.len(), 1);| if !binders.is_empty() { | ||
| out.push_str("exists"); | ||
| for b in binders { | ||
| if b != "_" { | ||
| out.push_str(" "); | ||
| out.push_str(b); | ||
| } else { | ||
| // If it's "_", we usually need a name for the exists, | ||
| // but if the user didn't name it, maybe we auto-name it? | ||
| // Or Aeneas requires a name. | ||
| // Let's generate a temp name if needed or just skip? | ||
| // Lean `exists _, ...` is valid but we need to bind it in the equality check. | ||
| // Wait, `exists ret` -> `fwd ... = Result.ok ret`. | ||
| // If user put `_`, we can't name it in the equality check easily. | ||
| // Let's assume user gives names for now. | ||
| out.push_str(" _"); | ||
| } | ||
| } | ||
| out.push_str(",\n "); | ||
| } |
There was a problem hiding this comment.
The current logic for generating quantifiers can produce a redundant exists clause if a binder is _. For example, if the first binder is _, this loop generates exists _, ... and then the forward check generates exists v, ..., resulting in exists _, exists v, .... This is valid Lean syntax, but it's redundant and can be simplified.
To improve the generated code, let's collect only the named binders and generate a single exists clause for them. The forward check already handles the _ case for the return value by introducing its own existential quantifier.
let named_binders: Vec<_> = binders.iter().filter(|s| s.as_str() != "_").collect();
if !named_binders.is_empty() {
out.push_str("exists");
for b in named_binders {
out.push_str(" ");
out.push_str(b);
}
out.push_str(",\n ");
}
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## G101266ed5cfc0fe74d16aaae0785d9622e8da5be #2971 +/- ##
============================================================================
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: v4 — Compare vs v3
📚 Full Patch History
Links show the diff between the row version and the column version.
⬇️ Download this PR
Branch
git fetch origin refs/heads/G443fc7f8c3623131b48be56a7a16935a9fe8f234 && git checkout -b pr-G443fc7f8c3623131b48be56a7a16935a9fe8f234 FETCH_HEADCheckout
git fetch origin refs/heads/G443fc7f8c3623131b48be56a7a16935a9fe8f234 && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/G443fc7f8c3623131b48be56a7a16935a9fe8f234 && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.