Skip to content

Generalize IRContext.WellFormed by allowing missing uses #128

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
math-fehr merged 3 commits into from
Jan 20, 2026
Merged

Generalize IRContext.WellFormed by allowing missing uses #128

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
8d0d41f
Generalize IRContext.WellFormed by allowing missing uses
math-fehr Jan 19, 2026
8f9cc3e
Remove old code
math-fehr Jan 20, 2026
0ec1f46
Change unicode lambda to `fun`
math-fehr Jan 20, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions Veir/ForLean.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
module

public import Std.Data.ExtHashSet

public section

/-- Checks if a UInt8 character is an alphabetic character or underscore in UTF-8. -/
Expand Down Expand Up @@ -115,6 +117,11 @@ theorem Nat.eq_iff_forall_lessthan :

deriving instance DecidableEq for Except

@[simp, grind =]
Copy link
Collaborator

@ineol ineol Jan 20, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it really necessary??

Copy link
Collaborator Author

@math-fehr math-fehr Jan 20, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So https://leanprover-community.github.io/mathlib4_docs/Std/Data/ExtHashSet/Lemmas.html#Std.ExtHashSet.filter_eq_empty_iff is the nearest theorem, otherwise there is no existing theorem like this.
grind = is necessary for some proofs when I checked.

theorem Std.ExtHashSet.filter_empty {α : Type} [Hashable α] [BEq α] [LawfulBEq α] (f : α → Bool) :
(∅ : Std.ExtHashSet α).filter f = ∅ := by
grind

section ranges

open Std
Expand Down
12 changes: 7 additions & 5 deletions Veir/IR/WellFormed.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -606,12 +606,14 @@ structure Region.WellFormed (region : Region) (ctx : IRContext) (regionPtr : Reg
inBounds : region.FieldsInBounds ctx
parent_op {op} (heq : region.parent = some op) : ∃ i, i < op.getNumRegions! ctx → op.getRegion! ctx i = regionPtr

structure IRContext.WellFormed (ctx : IRContext) : Prop where
structure IRContext.WellFormed (ctx : IRContext)
(missingOperandUses : Std.ExtHashSet OpOperandPtr := ∅)
(missingSuccessorUses : Std.ExtHashSet BlockOperandPtr := ∅) : Prop where
inBounds : ctx.FieldsInBounds
valueDefUseChains (valuePtr : ValuePtr) (valuePtrInBounds : valuePtr.InBounds ctx) :
∃ array, ValuePtr.DefUse valuePtr ctx array
∃ array, ValuePtr.DefUse valuePtr ctx array (missingOperandUses.filter (fun use => (use.get! ctx).value = valuePtr))
blockDefUseChains (blockPtr : BlockPtr) (blockPtrInBounds : blockPtr.InBounds ctx) :
∃ array, BlockPtr.DefUse blockPtr ctx array
∃ array, BlockPtr.DefUse blockPtr ctx array (missingSuccessorUses.filter (fun use => (use.get! ctx).value = blockPtr))
opChain (blockPtr : BlockPtr) (blockPtrInBounds : blockPtr.InBounds ctx) :
∃ array, BlockPtr.OpChain blockPtr ctx array
blockChain (regionPtr : RegionPtr) (regionPtrInBounds : regionPtr.InBounds ctx) :
Expand Down Expand Up @@ -792,8 +794,8 @@ noncomputable def ValuePtr.defUseArray (value : ValuePtr) (ctx : IRContext) (hct

@[grind .]
theorem ValuePtr.defUseArrayWF {hctx : IRContext.WellFormed ctx} :
ValuePtr.DefUse value ctx (ValuePtr.defUseArray value ctx hctx hvalue) :=
Exists.choose_spec (hctx.valueDefUseChains value hvalue)
ValuePtr.DefUse value ctx (ValuePtr.defUseArray value ctx hctx hvalue) := by
grind [ValuePtr.defUseArray]

theorem ValuePtr.defUseArray_contains_operand_use :
(operand.get ctx operandInBounds).value = value ↔
Expand Down
1 change: 1 addition & 0 deletions Veir/Rewriter/WellFormed/Rewriter/Value.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -112,6 +112,7 @@ theorem Rewriter.replaceUse_WellFormed (ctx: IRContext) (use : OpOperandPtr) (ne
have ⟨array, harray⟩ := hWf.valueDefUseChains value (by grind)
have ⟨newArray, hnewArray⟩ := hWf.valueDefUseChains newValue (by grind)
have ⟨array', hArray'⟩ := hWf.valueDefUseChains valuePtr (by grind)
simp only [Std.ExtHashSet.filter_empty]
apply Rewriter.replaceUse_DefUse
(value := value) (array := array) (array' := newArray) (array'' := array') <;> grind
case blockDefUseChains =>
Expand Down