From 8d0d41fc63700c31570a85141ab276f4ea3d7779 Mon Sep 17 00:00:00 2001 From: Mathieu Fehr Date: Mon, 19 Jan 2026 00:47:57 +0000 Subject: [PATCH 1/3] Generalize IRContext.WellFormed by allowing missing uses In the proofs related to `insertIntoCurrent`, we need to be in a state where the IR is well formed except for some uses. --- Veir/ForLean.lean | 7 +++++++ Veir/IR/WellFormed.lean | 18 +++++++++++++----- Veir/Rewriter/WellFormed/Rewriter/Value.lean | 1 + 3 files changed, 21 insertions(+), 5 deletions(-) diff --git a/Veir/ForLean.lean b/Veir/ForLean.lean index 91d9e49..906d76e 100644 --- a/Veir/ForLean.lean +++ b/Veir/ForLean.lean @@ -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. -/ @@ -115,6 +117,11 @@ theorem Nat.eq_iff_forall_lessthan : deriving instance DecidableEq for Except +@[simp, grind =] +theorem Std.ExtHashSet.filter_empty {α : Type} [Hashable α] [BEq α] [LawfulBEq α] (f : α → Bool) : + (∅ : Std.ExtHashSet α).filter f = ∅ := by + grind + section ranges open Std diff --git a/Veir/IR/WellFormed.lean b/Veir/IR/WellFormed.lean index 90efae9..b62c426 100644 --- a/Veir/IR/WellFormed.lean +++ b/Veir/IR/WellFormed.lean @@ -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 (λ 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 (λ 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) : @@ -790,10 +792,16 @@ theorem BlockPtr.operationList.mem : noncomputable def ValuePtr.defUseArray (value : ValuePtr) (ctx : IRContext) (hctx : ctx.WellFormed) (hvalue : value.InBounds ctx) : Array OpOperandPtr := (hctx.valueDefUseChains value hvalue).choose +theorem test : + ValuePtr.DefUse value ctx array → + array = array' → + ValuePtr.DefUse value ctx array' := by + grind + @[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 ↔ diff --git a/Veir/Rewriter/WellFormed/Rewriter/Value.lean b/Veir/Rewriter/WellFormed/Rewriter/Value.lean index 633a75c..79496ec 100644 --- a/Veir/Rewriter/WellFormed/Rewriter/Value.lean +++ b/Veir/Rewriter/WellFormed/Rewriter/Value.lean @@ -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 => From 8f9cc3e50e426c184f6ed21b6263974b1757eea6 Mon Sep 17 00:00:00 2001 From: Mathieu Fehr Date: Tue, 20 Jan 2026 13:09:08 +0000 Subject: [PATCH 2/3] Remove old code --- Veir/IR/WellFormed.lean | 6 ------ 1 file changed, 6 deletions(-) diff --git a/Veir/IR/WellFormed.lean b/Veir/IR/WellFormed.lean index b62c426..d71e41e 100644 --- a/Veir/IR/WellFormed.lean +++ b/Veir/IR/WellFormed.lean @@ -792,12 +792,6 @@ theorem BlockPtr.operationList.mem : noncomputable def ValuePtr.defUseArray (value : ValuePtr) (ctx : IRContext) (hctx : ctx.WellFormed) (hvalue : value.InBounds ctx) : Array OpOperandPtr := (hctx.valueDefUseChains value hvalue).choose -theorem test : - ValuePtr.DefUse value ctx array → - array = array' → - ValuePtr.DefUse value ctx array' := by - grind - @[grind .] theorem ValuePtr.defUseArrayWF {hctx : IRContext.WellFormed ctx} : ValuePtr.DefUse value ctx (ValuePtr.defUseArray value ctx hctx hvalue) := by From 0ec1f46d2bb8b94886b8c028166967402c0bd5be Mon Sep 17 00:00:00 2001 From: Mathieu Fehr Date: Tue, 20 Jan 2026 13:33:23 +0000 Subject: [PATCH 3/3] Change unicode lambda to `fun` --- Veir/IR/WellFormed.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Veir/IR/WellFormed.lean b/Veir/IR/WellFormed.lean index d71e41e..fb03a5f 100644 --- a/Veir/IR/WellFormed.lean +++ b/Veir/IR/WellFormed.lean @@ -611,9 +611,9 @@ structure IRContext.WellFormed (ctx : IRContext) (missingSuccessorUses : Std.ExtHashSet BlockOperandPtr := ∅) : Prop where inBounds : ctx.FieldsInBounds valueDefUseChains (valuePtr : ValuePtr) (valuePtrInBounds : valuePtr.InBounds ctx) : - ∃ array, ValuePtr.DefUse valuePtr ctx array (missingOperandUses.filter (λ use => (use.get! ctx).value = valuePtr)) + ∃ 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 (missingSuccessorUses.filter (λ use => (use.get! ctx).value = blockPtr)) + ∃ 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) :