From 519ea510130b1f4d804901bca3a643a862ae59bf Mon Sep 17 00:00:00 2001 From: Mathieu Fehr Date: Tue, 20 Jan 2026 01:26:31 +0000 Subject: [PATCH 1/2] Prove that insertIntoCurrent and removeFromCurrent preserves well-formedness This proof required generalizing WellFormed to handle missing uses, so we did not have it before. --- Veir/ForLean.lean | 20 +++++ Veir/Rewriter/LinkedList/WellFormed.lean | 108 ++++++++++++++++++++++- 2 files changed, 126 insertions(+), 2 deletions(-) diff --git a/Veir/ForLean.lean b/Veir/ForLean.lean index 906d76e..2549a52 100644 --- a/Veir/ForLean.lean +++ b/Veir/ForLean.lean @@ -122,6 +122,26 @@ theorem Std.ExtHashSet.filter_empty {α : Type} [Hashable α] [BEq α] [LawfulBE (∅ : Std.ExtHashSet α).filter f = ∅ := by grind +theorem Std.ExtHashSet.filter_erase_eq {α : Type} [Hashable α] [BEq α] [LawfulBEq α] + (s : Std.ExtHashSet α) (a : α) (f : α → Bool) : + (s.erase a).filter f = (s.filter f).erase a := by + grind + +theorem Std.ExtHashSet.filter_insert_eq_of_true_eq {α : Type} [Hashable α] [BEq α] [LawfulBEq α] + (s : Std.ExtHashSet α) (a : α) (f : α → Bool) : + f a = true → + (s.insert a).filter f = (s.filter f).insert a := by + grind + +theorem Std.ExtHashSet.filter_insert_eq_of_false_eq {α : Type} [Hashable α] [BEq α] [LawfulBEq α] + (s : Std.ExtHashSet α) (a : α) (f : α → Bool) : + f a = false → + (s.insert a).filter f = s.filter f := by + intro h + ext; grind + +end + section ranges open Std diff --git a/Veir/Rewriter/LinkedList/WellFormed.lean b/Veir/Rewriter/LinkedList/WellFormed.lean index c023764..8753468 100644 --- a/Veir/Rewriter/LinkedList/WellFormed.lean +++ b/Veir/Rewriter/LinkedList/WellFormed.lean @@ -45,7 +45,7 @@ theorem ValuePtr.defUse_OpOperandPtr_insertIntoCurrent_self_empty grind [ValuePtr.defUse_OpOperandPtr_insertIntoCurrent_self] theorem ValuePtr.defUse_OpOperandPtr_insertIntoCurrent_other - {value value' : ValuePtr} (valueNe : value ≠ value') {hvalue : use ∈ missingUses'} + {value value' : ValuePtr} (valueNe : value ≠ value') (hvalue : use ∈ missingUses') (hWF : value.DefUse ctx array missingUses) (hWF' : value'.DefUse ctx array' missingUses') : value.DefUse (use.insertIntoCurrent ctx (by grind) ctxInBounds) array missingUses := by @@ -87,6 +87,57 @@ theorem Region.wellFormed_OpOperandPtr_insertIntoCurrent (RegionPtr.get! regionPtr (use.insertIntoCurrent ctx useInBounds ctxInBounds)).WellFormed (use.insertIntoCurrent ctx useInBounds ctxInBounds) regionPtr := by apply Region.WellFormed_unchanged (ctx := ctx) <;> grind +theorem IRContext.wellFormed_OpOperandPtr_insertIntoCurrent + {ctx : IRContext} {use : OpOperandPtr} {useInBounds} {ctxInBounds} + (useMissing : use ∈ missingOperandUses) + (hWF : ctx.WellFormed missingOperandUses missingSuccessorUses) : + (use.insertIntoCurrent ctx useInBounds ctxInBounds).WellFormed (missingOperandUses.erase use) missingSuccessorUses := by + constructor + · grind + · intros valuePtr valuePtrInBounds + have ⟨array, h⟩ := hWF.valueDefUseChains valuePtr (by grind) + by_cases hvalue: (use.get! ctx).value = valuePtr + · apply Exists.intro _ + simp only [Std.ExtHashSet.filter_erase_eq] + apply ValuePtr.defUse_OpOperandPtr_insertIntoCurrent_self + · grind + · apply cast (a := h); congr + grind + · let valuePtr' := (use.get! ctx).value + have ⟨array', h'⟩ := hWF.valueDefUseChains valuePtr' (by grind) + apply Exists.intro _ + simp only [Std.ExtHashSet.filter_erase_eq] + apply ValuePtr.defUse_OpOperandPtr_insertIntoCurrent_other + (value' := valuePtr') (by grind) (hWF' := h') (hvalue := by grind) + apply cast (a := h); congr + simp only [OpOperandPtr.get!_OpOperandPtr_insertIntoCurrent] + ext; grind + · intros blockPtr blockPtrInBounds + have ⟨array, h⟩ := hWF.blockDefUseChains blockPtr (by grind) + apply Exists.intro _ + apply BlockPtr.defUse_OpOperandPtr_insertIntoCurrent + simp only [BlockOperandPtr.get!_OpOperandPtr_insertIntoCurrent] + apply h + · intros blockPtr blockPtrInBounds + have ⟨_, h⟩ := hWF.opChain blockPtr (by grind) + apply Exists.intro _ + apply BlockPtr.opChain_OpOperandPtr_insertIntoCurrent + apply h + · intros regionPtr regionPtrInBounds + have ⟨_, h⟩ := hWF.blockChain regionPtr (by grind) + apply Exists.intro _ + apply RegionPtr.blockChain_OpOperandPtr_insertIntoCurrent + apply h + · intros opPtr opPtrInBounds + have := hWF.operations opPtr (by grind) + grind [Operation.wellFormed_OpOperandPtr_insertIntoCurrent] + · intros blockPtr blockPtrInBounds + have := hWF.blocks blockPtr (by grind) + grind [Block.wellFormed_OpOperandPtr_insertIntoCurrent] + · intros regionPtr regionPtrInBounds + have := hWF.regions regionPtr (by grind) + grind [Region.wellFormed_OpOperandPtr_insertIntoCurrent] + /- OpOperandPtr.removeFromCurrent -/ theorem OpOperandPtr.back!_array_getElem_removeFromCurrent_eq_of_DefUse @@ -147,7 +198,7 @@ theorem ValuePtr.DefUse.getElem?_zero_erase_array_eq grind [Array.getElem_of_mem, ValuePtr.DefUse, ValuePtr.DefUse.erase_getElem_array_eq_eraseIdx] theorem ValuePtr.defUse_removeFromCurrent_self - {value : ValuePtr} {hvalue : use ∈ array} + {value : ValuePtr} (hvalue : use ∈ array) (hWF: value.DefUse ctx array missingUses) : value.DefUse (use.removeFromCurrent ctx (by grind) ctxInBounds) (array.erase use) (missingUses.insert use) := by have hUseValue : (use.get! ctx).value = value := by grind [ValuePtr.DefUse.useValue] @@ -221,6 +272,59 @@ theorem Region.wellFormed_OpOperandPtr_removeFromCurrent (RegionPtr.get! regionPtr (use.removeFromCurrent ctx useInBounds ctxInBounds)).WellFormed (use.removeFromCurrent ctx useInBounds ctxInBounds) regionPtr := by apply Region.WellFormed_unchanged (ctx := ctx) <;> grind + +theorem IRContext.wellFormed_OpOperandPtr_removeFromCurrent + {ctx : IRContext} {use : OpOperandPtr} {useInBounds} {ctxInBounds} + (useMissing : use ∉ missingOperandUses) + (hWF : ctx.WellFormed missingOperandUses missingSuccessorUses) : + (use.removeFromCurrent ctx useInBounds ctxInBounds).WellFormed (missingOperandUses.insert use) missingSuccessorUses := by + constructor + · grind + · intros valuePtr valuePtrInBounds + have ⟨array, h⟩ := hWF.valueDefUseChains valuePtr (by grind) + by_cases hvalue: (use.get! ctx).value = valuePtr + · apply Exists.intro _ + simp (disch := grind) only [Std.ExtHashSet.filter_insert_eq_of_true_eq] + apply ValuePtr.defUse_removeFromCurrent_self (array := array) + · grind [h.allUsesInChain] + · apply cast (a := h); congr + grind + · let valuePtr' := (use.get! ctx).value + have ⟨array', h'⟩ := hWF.valueDefUseChains valuePtr' (by grind) + apply Exists.intro _ + simp (disch := grind) only [Std.ExtHashSet.filter_insert_eq_of_false_eq] + apply ValuePtr.defUse_removeFromCurrent_other + (value' := valuePtr') (by grind) (hWF' := h') + · apply cast (a := h); congr + grind + · grind [h'.allUsesInChain] + · intros blockPtr blockPtrInBounds + have ⟨array, h⟩ := hWF.blockDefUseChains blockPtr (by grind) + apply Exists.intro _ + apply BlockPtr.defUse_OpOperandPtr_removeFromCurrent + simp only [BlockOperandPtr.get!_OpOperandPtr_removeFromCurrent] + apply h + · intros blockPtr blockPtrInBounds + have ⟨_, h⟩ := hWF.opChain blockPtr (by grind) + apply Exists.intro _ + apply BlockPtr.opChain_OpOperandPtr_removeFromCurrent + apply h + · intros regionPtr regionPtrInBounds + have ⟨_, h⟩ := hWF.blockChain regionPtr (by grind) + apply Exists.intro _ + apply RegionPtr.blockChain_OpOperandPtr_removeFromCurrent + apply h + · intros opPtr opPtrInBounds + have := hWF.operations opPtr (by grind) + grind [Operation.wellFormed_OpOperandPtr_removeFromCurrent] + · intros blockPtr blockPtrInBounds + have := hWF.blocks blockPtr (by grind) + grind [Block.wellFormed_OpOperandPtr_removeFromCurrent] + · intros regionPtr regionPtrInBounds + have := hWF.regions regionPtr (by grind) + grind [Region.wellFormed_OpOperandPtr_removeFromCurrent] + + section BlockOperandPtr.insertIntoCurrent theorem BlockOperandPtr.get!_BlockOperandPtr_insertIntoCurrent_of_value_ne From 6a3a37c774faa483587676fc33bd911f8d8713dc Mon Sep 17 00:00:00 2001 From: Mathieu Fehr Date: Tue, 20 Jan 2026 13:37:59 +0000 Subject: [PATCH 2/2] Remove double newlines --- Veir/Rewriter/LinkedList/WellFormed.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Veir/Rewriter/LinkedList/WellFormed.lean b/Veir/Rewriter/LinkedList/WellFormed.lean index 8753468..465848c 100644 --- a/Veir/Rewriter/LinkedList/WellFormed.lean +++ b/Veir/Rewriter/LinkedList/WellFormed.lean @@ -272,7 +272,6 @@ theorem Region.wellFormed_OpOperandPtr_removeFromCurrent (RegionPtr.get! regionPtr (use.removeFromCurrent ctx useInBounds ctxInBounds)).WellFormed (use.removeFromCurrent ctx useInBounds ctxInBounds) regionPtr := by apply Region.WellFormed_unchanged (ctx := ctx) <;> grind - theorem IRContext.wellFormed_OpOperandPtr_removeFromCurrent {ctx : IRContext} {use : OpOperandPtr} {useInBounds} {ctxInBounds} (useMissing : use ∉ missingOperandUses) @@ -324,7 +323,6 @@ theorem IRContext.wellFormed_OpOperandPtr_removeFromCurrent have := hWF.regions regionPtr (by grind) grind [Region.wellFormed_OpOperandPtr_removeFromCurrent] - section BlockOperandPtr.insertIntoCurrent theorem BlockOperandPtr.get!_BlockOperandPtr_insertIntoCurrent_of_value_ne