feat: proofs for constant folding tables

Veir.lean

@@ -14,6 +14,7 @@ import Veir.Printer
 import Veir.PatternRewriter.Basic
 import Veir.PatternRewriter.Puddle
 import Veir.Interfaces.FoldInterfaces
+import Veir.Interfaces.FoldInterfaces.TableProofs
 import Veir.Interfaces.ControlFlowInterfaces
 import Veir.Passes.ArithToLLVM.Proofs
 import Veir.Passes.Canonicalize.Proofs

Veir/IR/OpInfo.lean

@@ -71,7 +71,13 @@ class HasOpInfo (opCode: Type)
   operation folds entirely or not at all, so a table entry for a multi-result
   operation must decide every result. Implementations are responsible for
   returning an in-range operand or a constant conforming to the corresponding
-  result type.
+  result type. Operand replacements must have the corresponding result type.
+
+  The local semantic contract is `FoldTable.CorrectAt`, defined separately in
+  `Veir.Interfaces.FoldInterfaces.Correctness` to keep this interface independent
+  of the interpreter. It requires refinement for every well-typed completion
+  of the known operands, with no memory or control-flow effects, and does not
+  treat interpreter failure as evidence of correctness.
   -/
   tryFold : (op : opCode) → propertiesOf op → Array TypeAttr →
     Array (Option RuntimeValue) → Option (Array FoldDecision) := fun _ _ _ _ => none

Veir/Interfaces/FoldInterfaces/Correctness.lean

@@ -0,0 +1,94 @@
+module
+
+public import Veir.Interpreter.Refinement.Basic
+
+/-!
+# Local correctness of dialect fold tables
+
+These contracts concern the decisions returned by `HasOpInfo.tryFold`. They do
+not concern constant materialization, the folding driver, or rewriting the IR.
+Operand and result types describe a single operation signature; entry proofs
+state the signatures they support explicitly.
+-/
+
+public section
+
+namespace Veir
+
+/-- A replacement has the result's exact type, and any operand index is in range. -/
+@[expose]
+def FoldDecision.HasType (operandTypes : Array TypeAttr) (decision : FoldDecision)
+    (resultType : TypeAttr) : Prop :=
+  match decision with
+  | .useOperand j => operandTypes[j]? = some resultType
+  | .useConstant value => value.Conforms resultType
+
+/-- There is one well-typed replacement for each result, in result order. -/
+@[expose]
+def FoldDecision.HasTypes (decisions : Array FoldDecision)
+    (operandTypes resultTypes : Array TypeAttr) : Prop :=
+  decisions.size = resultTypes.size ∧
+    ∀ i (h : i < decisions.size), HasType operandTypes decisions[i] resultTypes[i]!
+
+/-- Interpret a decision without creating any IR. Invalid operand indices fail. -/
+@[expose]
+def FoldDecision.resolve (operands : Array RuntimeValue) : FoldDecision → Option RuntimeValue
+  | .useOperand j => operands[j]?
+  | .useConstant value => some value
+
+/-- Interpret all decisions, preserving their order and checking every operand index. -/
+@[expose]
+def FoldDecision.resolveAll (decisions : Array FoldDecision) (operands : Array RuntimeValue) :
+    Option (Array RuntimeValue) :=
+  List.toArray <$> decisions.toList.mapM (FoldDecision.resolve operands)
+
+namespace FoldTable
+
+/-- Known operands have the declared types; unknown operands impose no value constraint.
+The arrays must have the same length. -/
+@[expose]
+def InputsConform (known : Array (Option RuntimeValue)) (operandTypes : Array TypeAttr) : Prop :=
+  known.size = operandTypes.size ∧
+    ∀ i, i < known.size → ∀ v, known[i]! = some v → v.Conforms operandTypes[i]!
+
+/-- A runtime assignment agrees with every known operand. Unknown operands may
+be any conforming value, including poison. The arrays must have the same length. -/
+@[expose]
+def Agrees (known : Array (Option RuntimeValue)) (operands : Array RuntimeValue) : Prop :=
+  known.size = operands.size ∧
+    ∀ i, i < known.size → ∀ v, known[i]! = some v → operands[i]! = v
+
+/-- A successful interpretation has no memory or control-flow effect, and its
+results are refined by the replacements. UB permits any replacements, but an
+interpreter failure never establishes correctness. -/
+@[expose]
+def Refines (source : Interp (Array RuntimeValue × MemoryState × Option ControlFlowAction))
+    (replacements : Array RuntimeValue) (initialMemory : MemoryState) : Prop :=
+  match source with
+  | .fail => False
+  | .ub => True
+  | .ok (results, memory, action) =>
+    results ⊒ replacements ∧ memory = initialMemory ∧ action = none
+
+/-- Correctness of every successful table lookup at the given operation signature.
+
+Typing is required independently of execution, including when the source has UB.
+Semantic correctness quantifies over all well-typed completions of the known
+operands, all memories, successor arrays, and data layouts. It uses the operation
+interpreter directly, so it does not rely on the driver's poison handling or
+evaluation fallback. Returning `none` creates no obligation.
+-/
+@[expose]
+def CorrectAt (op : OpCode) (properties : propertiesOf op)
+    (operandTypes resultTypes : Array TypeAttr) : Prop :=
+  ∀ known decisions, InputsConform known operandTypes →
+    HasOpInfo.tryFold op properties resultTypes known = some decisions →
+    FoldDecision.HasTypes decisions operandTypes resultTypes ∧
+    ∀ operands, RuntimeValue.ArrayConforms operands operandTypes → Agrees known operands →
+      ∀ memory successors layout,
+        ∃ replacements, FoldDecision.resolveAll decisions operands = some replacements ∧
+          Refines (interpretOp' op properties resultTypes operands successors memory layout)
+            replacements memory
+
+end FoldTable
+end Veir

Veir/Interfaces/FoldInterfaces/Lemmas.lean

@@ -0,0 +1,89 @@
+module
+
+public import Veir.Interfaces.FoldInterfaces.Correctness
+public import Veir.Interpreter.Refinement.Lemmas
+
+import all Veir.IR.Attribute
+
+/-! Helpers for proving local fold-table correctness. -/
+
+public section
+
+namespace Veir
+open Data
+
+/-- Recover the integer operands from their declared widths. -/
+theorem RuntimeValue.ArrayConforms.int_pair
+    (h : RuntimeValue.ArrayConforms operands
+      #[(IntegerType.mk w₁ : TypeAttr), (IntegerType.mk w₂ : TypeAttr)]) :
+    ∃ lhs rhs, operands = #[.int w₁ lhs, .int w₂ rhs] := by
+  have hs : operands.size = 2 := h.1
+  have h0 := h.2 0 (by omega)
+  have h1 := h.2 1 (by omega)
+  simp at h0 h1
+  obtain ⟨lhs, hl⟩ := RuntimeValue.Conforms.integerType h0
+  obtain ⟨rhs, hr⟩ := RuntimeValue.Conforms.integerType h1
+  refine ⟨lhs, rhs, ?_⟩
+  apply Array.ext <;> grind
+
+/-- Recover a single register operand, regardless of its allocation. -/
+theorem RuntimeValue.ArrayConforms.reg_single {type : RegisterType}
+    (h : RuntimeValue.ArrayConforms operands #[(type : TypeAttr)]) :
+    ∃ value, operands = #[.reg value] := by
+  obtain ⟨value, rfl⟩ := Array.size_eq_one_iff.mp h.1
+  have hv := h.2 0 (by simp)
+  simp at hv
+  obtain ⟨reg, rfl⟩ := RuntimeValue.Conforms.registerType hv
+  exact ⟨reg, rfl⟩
+
+/-- Typing a single replacement reduces to typing its decision. -/
+@[simp]
+theorem FoldDecision.hasTypes_singleton :
+    HasTypes #[decision] operands #[type] ↔ HasType operands decision type := by
+  simp [HasTypes]
+
+/-- Typing two replacements reduces to their individual typing obligations. -/
+@[simp]
+theorem FoldDecision.hasTypes_pair :
+    HasTypes #[a, b] operands #[ta, tb] ↔
+      HasType operands a ta ∧ HasType operands b tb := by
+  simp [HasTypes, Nat.forall_lt_succ_left']
+
+/-- Refinement of two results is pointwise. -/
+@[simp]
+theorem RuntimeValue.arrayIsRefinedBy_pair :
+    #[a, b] ⊒ #[c, d] ↔ a ⊒ c ∧ b ⊒ d := by
+  simp only [arrayIsRefinedBy_cons, arrayIsRefinedBy_nil, and_true]
+
+/-- Reduce an integer binary fold with a known right operand to its typing and
+value semantics. The lookup describes which decisions are returned; this helper
+handles width agreement and every consistent runtime completion. The right
+operand may depend on its width, for example zero or all ones. -/
+theorem FoldTable.correctAt_int_rhs
+    (rhs : (width : Nat) → LLVM.Int width)
+    (lookup : ∀ known results,
+      HasOpInfo.tryFold op properties resultTypes known = some results →
+      ∃ left width, known = #[left, some (.int width (rhs width))] ∧ results = decisions)
+    (typed : FoldDecision.HasTypes decisions
+      #[(IntegerType.mk w : TypeAttr), (IntegerType.mk w : TypeAttr)] resultTypes)
+    (evaluate : ∀ lhs memory successors layout,
+      ∃ replacements,
+        FoldDecision.resolveAll decisions #[.int w lhs, .int w (rhs w)] = some replacements ∧
+        Refines (interpretOp' op properties resultTypes
+          #[.int w lhs, .int w (rhs w)] successors memory layout) replacements memory) :
+    CorrectAt op properties
+      #[(IntegerType.mk w : TypeAttr), (IntegerType.mk w : TypeAttr)] resultTypes := by
+  intro known results hKnown hFold
+  obtain ⟨left, width, rfl, rfl⟩ := lookup known results hFold
+  have hw := hKnown.2 1 (by simp) (.int width (rhs width)) (by simp)
+  simp [RuntimeValue.Conforms, Attribute.asType] at hw
+  subst width
+  refine ⟨typed, ?_⟩
+  intro operands hOperands hAgree memory successors layout
+  obtain ⟨lhs, actualRhs, rfl⟩ := hOperands.int_pair
+  have hr := hAgree.2 1 (by simp) (.int w (rhs w)) (by simp)
+  simp at hr
+  subst actualRhs
+  exact evaluate lhs memory successors layout
+
+end Veir

Veir/Interfaces/FoldInterfaces/TableProofs.lean

@@ -0,0 +1,140 @@
+module
+
+public import Veir.Interfaces.FoldInterfaces.Lemmas
+
+import all Veir.Data.Refinement
+import all Veir.IR.Attribute
+import all Veir.Interpreter.Basic
+import all Veir.GlobalOpInfo
+import all Veir.Dialects.Arith.OpInfo
+import all Veir.Dialects.LLVM.OpInfo
+import all Veir.Dialects.RISCV.OpInfo
+import all Veir.Data.LLVM.Int.Basic
+import all Veir.Data.RISCV.Reg.Basic
+
+/-!
+# Proofs for dialect fold-table entries
+
+Each theorem covers every successful lookup of its opcode, with arbitrary
+known operands and properties. Signatures are stated directly, without an IR
+context or assumptions about the folding driver. Integer widths are arbitrary.
+-/
+
+public section
+
+namespace Veir
+open Data
+
+private theorem fold_add_zero (x : LLVM.Int w) (nsw nuw : Bool) :
+    LLVM.Int.add x (.val (0#w)) nsw nuw = x := by
+  cases x with
+  | poison => rfl
+  | val x =>
+    simp [LLVM.Int.add, Id.run, BitVec.saddOverflow, BitVec.uaddOverflow,
+      Nat.not_le.mpr x.isLt, Int.not_le.mpr (BitVec.toInt_lt (x := x)),
+      Int.not_lt.mpr (BitVec.le_toInt x)]
+
+private theorem overflow_zero (x : LLVM.Int w) :
+    LLVM.Int.uaddOverflowFlag x (.val (0#w)) ⊒ .val (0#1) := by
+  cases x with
+  | poison => simp [LLVM.Int.uaddOverflowFlag, Id.run, isRefinedBy]
+  | val x =>
+    simp [LLVM.Int.uaddOverflowFlag, Id.run, BitVec.uaddOverflow,
+      Nat.not_le.mpr x.isLt, isRefinedBy]
+
+private theorem arith_addi_lookup
+    (h : HasOpInfo.tryFold (OpCode.arith .addi) properties types known = some decisions) :
+    ∃ lhs bw, known = #[lhs, some (.int bw (.val 0))] ∧
+      decisions = #[.useOperand 0] := by
+  change Arith.tryFold .addi properties types known = some decisions at h
+  unfold Arith.tryFold at h
+  repeat first | split at h | contradiction
+  all_goals grind [Array.toList_inj]
+
+private theorem arith_addui_extended_lookup
+    (h : HasOpInfo.tryFold (OpCode.arith .addui_extended) properties types known = some decisions) :
+    ∃ lhs bw, known = #[lhs, some (.int bw (.val 0))] ∧
+      decisions = #[.useOperand 0, .useConstant (.int 1 (.val 0))] := by
+  change Arith.tryFold .addui_extended properties types known = some decisions at h
+  unfold Arith.tryFold at h
+  repeat first | split at h | contradiction
+  all_goals grind [Array.toList_inj]
+
+private theorem llvm_add_lookup
+    (h : HasOpInfo.tryFold (OpCode.llvm .add) properties types known = some decisions) :
+    ∃ lhs bw, known = #[lhs, some (.int bw (.val 0))] ∧
+      decisions = #[.useOperand 0] := by
+  change Llvm.tryFold .add properties types known = some decisions at h
+  unfold Llvm.tryFold at h
+  repeat first | split at h | contradiction
+  all_goals grind [Array.toList_inj]
+
+private theorem riscv_andi_lookup
+    (h : HasOpInfo.tryFold (OpCode.riscv .andi) properties types known = some decisions) :
+    properties.value.value = 0 ∧ decisions = #[.useConstant (.reg ⟨0⟩)] := by
+  change Riscv.tryFold .andi properties types known = some decisions at h
+  unfold Riscv.tryFold at h
+  repeat first | split at h | contradiction
+  all_goals grind
+
+/-- The arithmetic add-zero entry, including arbitrary overflow flags and poison inputs. -/
+theorem Arith.tryFold_addi_correct (properties : Arith.propertiesOf .addi) (w : Nat) :
+    FoldTable.CorrectAt (.arith .addi) properties
+      #[(IntegerType.mk w : TypeAttr), (IntegerType.mk w : TypeAttr)]
+      #[(IntegerType.mk w : TypeAttr)] := by
+  apply FoldTable.correctAt_int_rhs (fun width => .val (0#width))
+    (fun _ _ h => arith_addi_lookup h)
+  · simp [FoldDecision.HasType]
+  · intro lhs memory successors layout
+    refine ⟨#[.int w lhs], ?_, ?_⟩
+    · simp [FoldDecision.resolveAll, FoldDecision.resolve]
+    · simp [Veir.interpretOp', Arith.interpretOp', LLVM.Int.cast_self, fold_add_zero,
+        FoldTable.Refines]
+
+/-- The extended-add entry refines both results, even when the unknown operand
+is poison: its poison overflow flag may be replaced with concrete false. -/
+theorem Arith.tryFold_addui_extended_correct (w : Nat) :
+    FoldTable.CorrectAt (.arith .addui_extended) ()
+      #[(IntegerType.mk w : TypeAttr), (IntegerType.mk w : TypeAttr)]
+      #[(IntegerType.mk w : TypeAttr), (IntegerType.mk 1 : TypeAttr)] := by
+  apply FoldTable.correctAt_int_rhs (fun width => .val (0#width))
+    (fun _ _ h => arith_addui_extended_lookup h)
+  · rw [FoldDecision.hasTypes_pair]; exact ⟨rfl, rfl⟩
+  · intro lhs memory successors layout
+    refine ⟨#[.int w lhs, .int 1 (.val 0)], ?_, ?_⟩
+    · simp [FoldDecision.resolveAll, FoldDecision.resolve]
+    · simp [Veir.interpretOp', Arith.interpretOp', LLVM.Int.cast_self, fold_add_zero,
+        FoldTable.Refines, RuntimeValue.isRefinedBy, overflow_zero]
+
+/-- LLVM add-zero is correct for every width and every choice of overflow flags. -/
+theorem Llvm.tryFold_add_correct (properties : Llvm.propertiesOf .add) (w : Nat) :
+    FoldTable.CorrectAt (.llvm .add) properties
+      #[(IntegerType.mk w : TypeAttr), (IntegerType.mk w : TypeAttr)]
+      #[(IntegerType.mk w : TypeAttr)] := by
+  apply FoldTable.correctAt_int_rhs (fun width => .val (0#width))
+    (fun _ _ h => llvm_add_lookup h)
+  · simp [FoldDecision.HasType]
+  · intro lhs memory successors layout
+    refine ⟨#[.int w lhs], ?_, ?_⟩
+    · simp [FoldDecision.resolveAll, FoldDecision.resolve]
+    · simp [Veir.interpretOp', Llvm.interpretOp', LLVM.Int.cast_self, fold_add_zero,
+        FoldTable.Refines]
+
+/-- The RISC-V immediate-and-zero entry is correct for every register value.
+The operand and result may have different register allocations. The successful
+lookup itself establishes that the immediate is zero. -/
+theorem Riscv.tryFold_andi_correct (properties : Riscv.propertiesOf .andi)
+    (operandType resultType : RegisterType) :
+    FoldTable.CorrectAt (.riscv .andi) properties
+      #[(operandType : TypeAttr)] #[(resultType : TypeAttr)] := by
+  intro known decisions _ hFold
+  obtain ⟨hZero, rfl⟩ := riscv_andi_lookup hFold
+  constructor
+  · rw [FoldDecision.hasTypes_singleton]; trivial
+  · intro operands hOperands _ memory successors layout
+    obtain ⟨value, rfl⟩ := hOperands.reg_single
+    refine ⟨#[.reg ⟨0⟩], ?_, ?_⟩
+    · simp [FoldDecision.resolveAll, FoldDecision.resolve]
+    · simp [Veir.interpretOp', Riscv.interpretOp', hZero, RISCV.andi, FoldTable.Refines]
+
+end Veir