Add eq_anything and improve IntRange step_pos for variable steps#6
Open
quangvdao wants to merge 1 commit intorems-project:mainfrom
Open
Add eq_anything and improve IntRange step_pos for variable steps#6quangvdao wants to merge 1 commit intorems-project:mainfrom
quangvdao wants to merge 1 commit intorems-project:mainfrom
Conversation
- Add `eq_anything` as a `@[simp_sail]` utility in `Sail.lean`, matching the Sail built-in `eq_anything` which the Lean backend emits but was previously missing from the support library. - Improve the `IntRange` macro for the `[start:stop:step]i` syntax to provide `step_pos` via `by first | omega | decide | sorry` instead of relying on the struct default `by omega`. This allows variable step values (common in Sail-generated loops) to type-check without manual intervention, at the cost of a `sorry` when the step cannot be statically proven non-zero. Made-with: Cursor
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
1 participant
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.
Summary
Two small additions to the Sail Lean support library:
1.
eq_anything(Sail.lean)Adds
def eq_anything [BEq α] (x : α) (y : α) : Bool := x == ywith@[simp_sail]. This corresponds to the Sail built-ineq_anythingwhich the Lean backend emits in generated code but was previously missing from the support library, causing "unknown identifier" errors when building Sail-generated Lean projects.2.
IntRangestep_pos fallback (IntRange.lean)The
[start:stop:step]imacro now providesstep_pos := by first | omega | decide | sorryfor the non-unit-step cases. Previously, whenstepwas a variable (as is common in Sail-generated loops, e.g.,for base in [lo:hi:(2 *i vsize)]i do), the struct defaultby omegawould fail becauseomegacannot proveM ≠ 0for an arbitrary integer expression. The fallback tosorryallows such code to type-check, while literal step values continue to be verified byomega/decide.Motivation
These issues were discovered while extracting the
sail-small-arm(ARMv8.5-A subset) model to Lean using the Sail Lean backend. Both issues caused Lean compilation failures in the generated code.Test plan
lake buildpasses on the modifiedlean-saillibraryPosted by Cursor assistant (model: claude-4.6-opus-high-thinking) on behalf of the user (Quang Dao) with approval.
Made with Cursor