Testing for agreement between Lean and Z3 semantics - #11
Conversation
Summary of ChangesHello, 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 significantly enhances the semantic consistency between Lean and Z3 for integer arithmetic operations, particularly division and modulo. It integrates the 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. 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. 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 the mod operator and adds comprehensive tests to verify the semantic agreement between Lean and Z3 for various binary operations, including edge cases like division by zero. The changes are well-structured, touching the lexer, parser, operational semantics, and verifier to correctly integrate the new operator. The verifier's approach to handling division and modulo by asserting a non-zero divisor is a solid improvement. I have a couple of suggestions to enhance code quality by addressing code duplication and removing dead code, aligning with the project's style guide.
| first | ||
| | (refine ⟨.int (a / b), ?_, ?_⟩ | ||
| · simp [TinyML.evalBinOp, hne_zero] | ||
| · exact hpost (.int (a / b)) ρ_r st₂ .int _ hΨ_post | ||
| (by intro v hv; simp [Term.freeVars] at hv | ||
| rcases hv with hv | hv | ||
| · exact (sl.wfIn_mono hsl_wf hdecls_r) v hv | ||
| · exact hsr_wf v hv) | ||
| (by simp [Term.eval, UnOp.eval, BinOp.eval, hsl_ρ_r, hsr_eval]) | ||
| (.int _)) | ||
| | (refine ⟨.int (a % b), ?_, ?_⟩ | ||
| · simp [TinyML.evalBinOp, hne_zero] | ||
| · exact hpost (.int (a % b)) ρ_r st₂ .int _ hΨ_post | ||
| (by intro v hv; simp [Term.freeVars] at hv | ||
| rcases hv with hv | hv | ||
| · exact (sl.wfIn_mono hsl_wf hdecls_r) v hv | ||
| · exact hsr_wf v hv) | ||
| (by simp [Term.eval, UnOp.eval, BinOp.eval, hsl_ρ_r, hsr_eval]) | ||
| (.int _)) |
There was a problem hiding this comment.
This block has a significant amount of duplicated code for the div and mod cases. The proof tactics for well-formedness (wfIn) and evaluation (eval) are identical in both branches of the first block. This duplication can be reduced by extracting the common proof tactics into let-bindings, which improves readability and maintainability, adhering to the style guide's principle of avoiding duplication.
let wf_proof := by
intro v hv; simp [Term.freeVars] at hv
rcases hv with hv | hv
· exact (sl.wfIn_mono hsl_wf hdecls_r) v hv
· exact hsr_wf v hv
let eval_proof := by simp [Term.eval, UnOp.eval, BinOp.eval, hsl_ρ_r, hsr_eval]
first
| (refine ⟨.int (a / b), ?_, ?_⟩
· simp [TinyML.evalBinOp, hne_zero]
· exact hpost (.int (a / b)) ρ_r st₂ .int _ hΨ_post wf_proof eval_proof (.int _))
| (refine ⟨.int (a % b), ?_, ?_⟩
· simp [TinyML.evalBinOp, hne_zero]
· exact hpost (.int (a % b)) ρ_r st₂ .int _ hΨ_post wf_proof eval_proof (.int _))
References
- The style guide recommends avoiding code duplication. The current implementation for
divandmodproof cases contains repeated tactic blocks that can be refactored. (link)
| def checkIntBinOp (name : String) (op : BinOp .int .int .int) (a b : Int) | ||
| : VerifM (String × Bool) := do | ||
| let lhs := Term.binop op (.const (.i a)) (.const (.i b)) | ||
| let rhs : Term .int := .const (.i (op.eval a b)) | ||
| let ok ← VerifM.check (Formula.eq .int lhs rhs) | ||
| return (s!"{name}({a}, {b})", ok) |
There was a problem hiding this comment.
The function checkIntBinOp is defined here but is not used anywhere in the file. The main function uses runTest to execute the tests. This unused function constitutes dead code and should be removed to improve maintainability, as per the project's style guide.
References
- The style guide's completion discipline states that dead code, such as abandoned helper functions, should be deleted. (link)
1 participant
Building on #10, this PR adds a test that compares the semantics of various operations, including div and mod between Z3 and Lean to make sure there are no accidental discrepancies.