[WIP] progress on rewrite lifting

Veir.lean

@@ -14,6 +14,7 @@ import Veir.Interfaces.FoldInterfaces
 import Veir.Passes.ArithToLLVM.Proofs
 import Veir.Passes.Canonicalize.Proofs
 import Veir.Passes.RISCVCombines.Proofs
+import Veir.PatternRewriter.Soundness
 import Veir.Benchmarks
 import Veir.Parser.Lexer
 import Veir.Interpreter

Veir/Benchmarks.lean

@@ -570,6 +570,10 @@ info: "builtin.module"() ({
 /--
 info: "builtin.module"() ({
   ^2():
+    %3 = "arith.constant"() <{"value" = 42 : i32}> : () -> i32
+    %4 = "arith.constant"() <{"value" = 1 : i32}> : () -> i32
+    %9 = "arith.constant"() <{"value" = 43 : i32}> : () -> i32
+    %6 = "arith.constant"() <{"value" = 1 : i32}> : () -> i32
     %10 = "arith.constant"() <{"value" = 44 : i32}> : () -> i32
     "test.test"(%10) : (i32) -> ()
 }) : () -> ()

Veir/Dominance.lean

@@ -201,3 +201,64 @@ axiom WfIRContext.Dom.blockArgument_not_dominatesIp_before_of_dominatesIp_firstO
     (opDom : op.dominatesIp (InsertPoint.atStart! block ctx.raw) ctx)
     (hMem : value ∈ block.getArguments! ctx.raw) :
     ¬ value.dominatesIp (InsertPoint.before op) ctx
+
+/-- A block argument dominates the end of its own block: it is in scope throughout the block body. -/
+axiom WfIRContext.Dom.blockArgument_dominatesIp_atEnd
+    (ctxDom : ctx.Dom) {block : BlockPtr} (blockIn : block.InBounds ctx.raw)
+    (hMem : value ∈ block.getArguments! ctx.raw) :
+    value.dominatesIp (InsertPoint.atEnd block) ctx
+
+/-- A result of an operation in a block body does not dominate that block's entry (the SSA
+property: results are defined strictly inside the block, not before it). -/
+axiom WfIRContext.Dom.opResult_not_dominatesIp_atStart!
+    (ctxDom : ctx.Dom) {op : OperationPtr} (opIn : op.InBounds ctx.raw)
+    {block : BlockPtr} (blockIn : block.InBounds ctx.raw)
+    (opInBlock : op ∈ block.operationList ctx.raw ctx.wellFormed blockIn)
+    {r : ValuePtr} (rResult : r ∈ op.getResults! ctx.raw) :
+    ¬ r.dominatesIp (InsertPoint.atStart! block ctx.raw) ctx
+
+/-- A result of an operation does not dominate the point before that same operation (the SSA
+property: a result is only defined once its own operation has run). -/
+axiom WfIRContext.Dom.opResult_not_dominatesIp_before_self
+    (ctxDom : ctx.Dom) {op : OperationPtr}
+    {r : ValuePtr} (rResult : r ∈ op.getResults! ctx.raw) :
+    ¬ r.dominatesIp (InsertPoint.before op) ctx
+
+/-!
+## Block-level dominance
+
+Dominance between blocks (the entry of `b₁` dominates every point of `b₂`). Used to discharge the
+cross-block antisymmetry argument in the pattern-rewriter soundness proof: a value forwarded by a
+rewrite cannot become an argument of a *different* block.
+-/
+
+variable {b₁ b₂ block bl : BlockPtr}
+
+/-- The dominance relation between two blocks: `b₁` dominates `b₂` when `b₁`'s entry dominates every
+program point of `b₂`. A block dominates itself. -/
+axiom BlockPtr.dominates (b₁ b₂ : BlockPtr) (ctx : WfIRContext OpInfo) : Prop
+
+/-- Block dominance is antisymmetric: two blocks that dominate each other are equal. -/
+axiom BlockPtr.dominates_antisymm :
+    b₁.dominates b₂ ctx → b₂.dominates b₁ ctx → b₁ = b₂
+
+/-- If a result `r` of an operation `op` living in `block` dominates the entry of a block `bl`, then
+`block` dominates `bl` (the definition site of `r` is in `block`, and `r` reaches all of `bl`). -/
+axiom WfIRContext.Dom.block_dominates_of_opResult_dominatesIp_atStart!
+    (ctxDom : ctx.Dom) {op : OperationPtr} (opIn : op.InBounds ctx.raw)
+    (blockIn : block.InBounds ctx.raw) (blIn : bl.InBounds ctx.raw)
+    (opInBlock : op ∈ block.operationList ctx.raw ctx.wellFormed blockIn)
+    {r : ValuePtr} (rResult : r ∈ op.getResults! ctx.raw)
+    (rDom : r.dominatesIp (InsertPoint.atStart! bl ctx.raw) ctx) :
+    block.dominates bl ctx
+
+/-- If an argument `w` of a block `bl` dominates a program point inside `block` (the end of a list of
+`block`'s operations, started from `block`'s entry), then `bl` dominates `block`: `w` is in scope
+from `bl`'s entry, so `bl`'s entry dominates that point, hence all of `block`. -/
+axiom WfIRContext.Dom.block_dominates_of_arg_dominatesIp_afterLast
+    (ctxDom : ctx.Dom) (blIn : bl.InBounds ctx.raw) (blockIn : block.InBounds ctx.raw)
+    {w : ValuePtr} (wArg : w ∈ bl.getArguments! ctx.raw)
+    {ops : List OperationPtr}
+    (hops : ∀ o ∈ ops, o ∈ block.operationList ctx.raw ctx.wellFormed blockIn)
+    (wDom : w.dominatesIp (InsertPoint.afterLast ops ctx.raw (.atStart! block ctx.raw)) ctx) :
+    bl.dominates block ctx

Veir/ForLean.lean

@@ -242,6 +242,32 @@ theorem getElem_idxOf [DecidableEq α] {l : List α} (h : l.idxOf x < l.length)
     l[l.idxOf x] = x := by
   induction l <;> grind
 
+/--
+Transfer a reflexive, transitive relation `P` across a `forIn` loop in the `Option` monad: if every
+successful step of the body relates its input state to its output state, then a successful run of the
+whole loop relates the initial state to the final one. Early exit (`ForInStep.done`) is covered
+because `ForInStep.value` reads the carried state in both branches.
+-/
+theorem forIn_option_rel {α σ : Type} (P : σ → σ → Prop)
+    (hrefl : ∀ s, P s s) (htrans : ∀ a b c, P a b → P b c → P a c)
+    (l : List α) (f : α → σ → Option (ForInStep σ))
+    (hf : ∀ a ∈ l, ∀ s step, f a s = some step → P s step.value) :
+    ∀ s s', forIn l s f = some s' → P s s' := by
+  induction l with
+  | nil => intro s s' h; simp at h; grind
+  | cons a as ih =>
+    intro s s' h
+    simp only [List.forIn_cons] at h
+    rcases hstep : f a s with _ | step
+    · rw [hstep] at h; simp at h
+    · rw [hstep] at h
+      have hP := hf a (by simp) s step hstep
+      cases step with
+      | done b => simp at h; subst h; exact hP
+      | yield b =>
+        simp only [bind] at h
+        exact htrans _ _ _ hP (ih (fun a ha => hf a (by simp [ha])) b s' (by simpa using h))
+
 end ForLean.List
 
 section

Veir/Interpreter/Basic.lean

@@ -385,6 +385,12 @@ instance : MonadLift Option Interp where
 
 instance : Inhabited (Interp α) := ⟨(none : Option (UBOr α))⟩
 
+/-- The interpreter monad is a chain-complete partial order with `none` as bottom (the flat order on
+`Option`). This steers `partial_fixpoint` (used for `interpretBlockCFG`) to take its least fixpoint in
+the `none`-bottom order, so that `interpretBlockCFG.fixpoint_induct`'s admissibility base case is the
+trivially-true `none` outcome — exactly what refinement/correctness proofs need. -/
+instance instCCPOInterp {α : Type} : Lean.Order.CCPO (Interp α) := Lean.Order.instCCPOOption
+
 /-- Signal undefined behaviour from inside the interpreter monad. -/
 @[inline] def Interp.ub : Interp α := some .ub
 

Veir/Interpreter/EquationLemma.lean

@@ -149,6 +149,7 @@ theorem interpretOp_equationLemmaAt {ctx : WfIRContext OpCode} {opInBounds} {sta
 /-- An interpreter state satisfies the `DefinesDominating` invariant at a program point if it
 defines all values that dominate that program point. This should be satisfied by any state in the
 interpreter. -/
+@[expose]
 def InterpreterState.DefinesDominating {ctx : WfIRContext OpCode} (state : InterpreterState ctx)
     (location : InsertPoint) (_locInBounds : location.InBounds ctx.raw := by grind) : Prop :=
   ∀ (value : ValuePtr) (_valueInBounds : value.InBounds ctx.raw),

Veir/Interpreter/Refinement/Basic.lean

@@ -27,7 +27,7 @@ open Veir.Data
 
 namespace Veir
 
-variable {OpInfo : Type} [HasOpInfo OpInfo] {ctx : WfIRContext OpInfo}
+variable {OpInfo : Type} [HasOpInfo OpInfo] {ctx ctx₁ ctx₂ : WfIRContext OpInfo}
 
 /-- Refinement relation between two runtime values. -/
 @[expose]
@@ -134,7 +134,7 @@ operation whose parent operation is `moduleOp`.
 structure OperationPtr.IsTopLevelFuncWithName (op : OperationPtr) (moduleOp : OperationPtr)
     (ctx : IRContext OpCode) (name : StringAttr) : Prop where
   isFunc : op.getOpType! ctx = .func .func
-  hasName : name = (op.getProperties! ctx Func.func).sym_name
+  hasName : name = (op.getProperties! ctx (OpCode.func Func.func)).sym_name
   isTopLevel : op.getParentOp! ctx = some moduleOp
 
 /--
@@ -163,20 +163,9 @@ def ValueMapping.applyToArray {ctx ctx' : WfIRContext OpInfo} (mapping : ValueMa
     (vals : Array ValuePtr) (valsIn : ∀ v ∈ vals, v.InBounds ctx.raw := by grind) : Array ValuePtr :=
   vals.attach.map (fun ⟨v, hv⟩ => (mapping ⟨v, valsIn v hv⟩).val)
 
-/--
-`mapping` *reflects* `op'`'s result pointers back to `op`'s if the only value it sends onto `op'`'s
-`i`-th result pointer is `op`'s `i`-th result pointer. Paired with the "fixes" equation
-`mapping.applyToArray (op.getResults! ..) = op'.getResults! ..`, this says `mapping` matches the two
-operations' results index-by-index without mapping any other value onto them. -/
-def ValueMapping.ReflectsResults {ctx ctx' : WfIRContext OpInfo} (mapping : ValueMapping ctx ctx')
-    (op op' : OperationPtr) : Prop :=
-  ∀ (val : ValuePtr) (valIn : val.InBounds ctx.raw) (i : Nat),
-    (mapping ⟨val, valIn⟩).val = op'.getResult i → val = op.getResult i
-
-/-- An operation `op` in `ctx` is *preserved* and renamed to an operation `op'` in `ctx'` by the
-mapping `mapping` if `op` and `op'` have the same type, properties, result types, successors, and
-their operands and results are related by `mapping`. Additionally, `mapping` must reflect `op'`'s
-results back to `op`'s, so no other value is sent onto `op'`'s results. -/
+/-- The *intrinsic-data frame* of an operation `op` in `ctx` renamed to `op'` in `ctx'` by `mapping`:
+`op` and `op'` have the same type, properties, result types, successors, and their operands and
+results are related by `mapping`. -/
 structure ValueMapping.PreservesOperation {ctx ctx' : WfIRContext OpInfo}
     (mapping : ValueMapping ctx ctx') (op op' : OperationPtr)
     (opIn : op.InBounds ctx.raw := by grind)
@@ -188,7 +177,6 @@ structure ValueMapping.PreservesOperation {ctx ctx' : WfIRContext OpInfo}
   successors : op'.getSuccessors! ctx'.raw = op.getSuccessors! ctx.raw
   operands : op'.getOperands! ctx'.raw = mapping.applyToArray (op.getOperands! ctx.raw)
   results : op'.getResults! ctx'.raw = mapping.applyToArray (op.getResults! ctx.raw) (by grind)
-  reflect : mapping.ReflectsResults op op'
 
 /--
 A variable state `state` is refined by `state'` through the value renaming `mapping`: every
@@ -289,6 +277,7 @@ A refinement relation for variable states in two different contexts at different
 This asserts that every value in `state` and in scope, that is mapped to a value in `state'` and
 in scope, have refining runtime values.
 -/
+@[expose]
 def VariableState.isRefinedByAt {ctx ctx' : WfIRContext OpInfo}
     (state : VariableState ctx) (state' : VariableState ctx')
     (mapping : ValueMapping ctx ctx') (s : RefinementPoint) (s' : RefinementPoint)
@@ -301,14 +290,77 @@ def VariableState.isRefinedByAt {ctx ctx' : WfIRContext OpInfo}
   sv ⊒ tv
 
 /--
-A refinement relation for intepreter states in two different locations.
-This asserts that memory is equal, and that the variable states are refined at the given points.
+An interpreter state `state` is refined by `state'` through the value mapping `mapping`, scoped
+to source point `s` and target point `s'`: they have the same memory, and the variable state of
+`state` is scoped-refined by the variable state of `state'` through `mapping` at `(s, s')`.
 -/
+@[expose]
 def InterpreterState.isRefinedByAt {ctx ctx' : WfIRContext OpInfo}
     (state : InterpreterState ctx) (state' : InterpreterState ctx')
     (mapping : ValueMapping ctx ctx') (s : RefinementPoint) (s' : RefinementPoint)
     (_sIn : s.InBounds ctx.raw := by grind) (_s'In : s'.InBounds ctx'.raw := by grind) : Prop :=
   state.memory = state'.memory ∧
   state.variables.isRefinedByAt state'.variables mapping s s'
 
+/-- Scope-weakening (antitone): `isRefinedByAt` at a *wider* pair of scopes implies it at a
+*narrower* pair. If every value in scope at `(t, t')` is in scope at `(s, s')`, the relation
+transports from `(s, s')` to `(t, t')`. -/
+theorem VariableState.isRefinedByAt.weaken {ctx ctx' : WfIRContext OpInfo}
+    {state : VariableState ctx} {state' : VariableState ctx'}
+    {mapping : ValueMapping ctx ctx'} {s s' t t' : RefinementPoint}
+    {sIn : s.InBounds ctx.raw} {s'In : s'.InBounds ctx'.raw}
+    {tIn : t.InBounds ctx.raw} {t'In : t'.InBounds ctx'.raw}
+    (h : state.isRefinedByAt state' mapping s s' sIn s'In)
+    (hsrc : ∀ (val : ValuePtr), val.InScopeAt t ctx → val.InScopeAt s ctx)
+    (htgt : ∀ (val : ValuePtr), val.InScopeAt t' ctx' → val.InScopeAt s' ctx') :
+    state.isRefinedByAt state' mapping t t' tIn t'In :=
+  fun val valIn hsc htsc sv tv hsv htv =>
+    h val valIn (hsrc val hsc) (htgt _ htsc) sv tv hsv htv
+
+/-- Interpreter-state version of `VariableState.isRefinedByAt.weaken`. -/
+theorem InterpreterState.isRefinedByAt.weaken {ctx ctx' : WfIRContext OpInfo}
+    {state : InterpreterState ctx} {state' : InterpreterState ctx'}
+    {mapping : ValueMapping ctx ctx'} {s s' t t' : RefinementPoint}
+    {sIn : s.InBounds ctx.raw} {s'In : s'.InBounds ctx'.raw}
+    {tIn : t.InBounds ctx.raw} {t'In : t'.InBounds ctx'.raw}
+    (h : state.isRefinedByAt state' mapping s s' sIn s'In)
+    (hsrc : ∀ (val : ValuePtr), val.InScopeAt t ctx → val.InScopeAt s ctx)
+    (htgt : ∀ (val : ValuePtr), val.InScopeAt t' ctx' → val.InScopeAt s' ctx') :
+    state.isRefinedByAt state' mapping t t' tIn t'In :=
+  ⟨h.1, h.2.weaken hsrc htgt⟩
+
+/--
+`mapping` *preserves dominance* from the source scope `s` (in `ctx`) to the target scope `s'` (in
+`ctx'`): every value *in scope* at `s` is mapped to a value *in scope* at `s'`. Scoped exactly like
+`isRefinedByAt`, this is a dominance homomorphism restricted to the values the refinement actually
+constrains, so stale/out-of-scope values are excused.
+
+This is the natural well-formedness condition on the value renaming produced by a rewrite. Its key
+consequence for the monotonicity proof is `PreservesDominance.image_not_mem_getResults`: the image of
+an in-scope value is never a result of the target operation.
+-/
+def ValueMapping.PreservesDominance {ctx ctx' : WfIRContext OpInfo}
+    (mapping : ValueMapping ctx ctx') (s s' : RefinementPoint)
+    (_sIn : s.InBounds ctx.raw := by grind) (_s'In : s'.InBounds ctx'.raw := by grind) : Prop :=
+  ∀ (val : ValuePtr) (valIn : val.InBounds ctx.raw),
+    val.InScopeAt s ctx → (mapping ⟨val, valIn⟩).val.InScopeAt s' ctx'
+
+/--
+Under dominance preservation at `(before op, before op')` and target dominance-wellformedness, the
+image of any value in scope just before `op` is **not** a result of `op'`: the image dominates
+`before op'` (dominance preservation), while a result of `op'` never dominates the point before `op'`
+(`ctx'.Dom`). This is the exact fact the monotonicity proof needs where the old `ReflectsResults`
+obligation used to be threaded — no `ctx.Dom` needed on the source.
+-/
+theorem ValueMapping.PreservesDominance.image_not_mem_getResults {ctx ctx' : WfIRContext OpInfo}
+    {mapping : ValueMapping ctx ctx'} {op op' : OperationPtr}
+    (opIn : op.InBounds ctx.raw) (opIn' : op'.InBounds ctx'.raw)
+    (ctxDom' : ctx'.Dom)
+    (hPres : mapping.PreservesDominance (.at (.before op)) (.at (.before op')))
+    {val : ValuePtr} (valIn : val.InBounds ctx.raw)
+    (hValDom : val.dominatesIp (InsertPoint.before op) ctx) :
+    (mapping ⟨val, valIn⟩).val ∉ op'.getResults! ctx'.raw :=
+  fun hmem =>
+    (ctxDom'.opResult_not_dominatesIp_before_self hmem) (hPres val valIn hValDom)
+
 end Veir

Veir/Interpreter/Refinement/Lemmas.lean

@@ -57,17 +57,21 @@ theorem Interp.isRefinedBy_refl_of_ne_none {α : Type} {R : α → α → Prop}
     (hR : ∀ a, R a a) (x : Interp α) (neNone : x ≠ none) : Interp.isRefinedBy R x x := by
   rcases x with _ | (x | _) <;> grind [Interp.isRefinedBy]
 
+/-- `isRefinedByAt` is reflexive under the identity mapping at any program point. -/
 @[simp, grind .]
-theorem VariableState.isRefinedBy_refl
-    {ctx : WfIRContext OpInfo} {state : VariableState ctx} :
-    state.isRefinedBy state id := by
-  grind [VariableState.isRefinedBy]
+theorem VariableState.isRefinedByAt_refl
+    {ctx : WfIRContext OpInfo} {state : VariableState ctx}
+    {p : InsertPoint} {pIn : p.InBounds ctx.raw} :
+    state.isRefinedByAt state id p p := by
+  grind [VariableState.isRefinedByAt]
 
+/-- `isRefinedByAt` is reflexive for `InterpreterState` under the identity mapping at any point. -/
 @[simp, grind .]
-theorem InterpreterState.isRefinedBy_refl
-    {ctx : WfIRContext OpInfo} {state : InterpreterState ctx} :
-    state.isRefinedBy state id := by
-  grind [InterpreterState.isRefinedBy, VariableState.isRefinedBy]
+theorem InterpreterState.isRefinedByAt_refl
+    {ctx : WfIRContext OpInfo} {state : InterpreterState ctx}
+    {p : InsertPoint} {pIn : p.InBounds ctx.raw} :
+    state.isRefinedByAt state id p p := by
+  grind [InterpreterState.isRefinedByAt]
 
 @[simp, grind .]
 theorem ControlFlowAction.isRefinedBy_refl (cf : ControlFlowAction) : cf ⊒ cf := by
@@ -216,16 +220,27 @@ theorem ValueMapping.applyToArray_getResults!_ext
     Array.getElem_attach] at hResults
   grind
 
-/-- If a value mapping reflects results from `op` to `op'`, then values that are not in
-`op` results are not mapped to values in `op'` results. -/
-@[grind .]
-theorem ValueMapping.ReflectsResults.not_mem_getResults
-    {ctx ctx' : WfIRContext OpInfo} {mapping : ValueMapping ctx ctx'} {op op' : OperationPtr}
-    {val : ValuePtr} (valIn : val.InBounds ctx.raw)
-    (hReflect : mapping.ReflectsResults op op')
-    (hNotMem : val ∉ op.getResults! ctx.raw) :
-    (mapping ⟨val, valIn⟩).val ∉ op'.getResults! ctx'.raw := by
-  intro hmem
-  simp only [OperationPtr.getResults!.mem_iff_exists_index] at hmem
-  have ⟨index, hindex, heq⟩ := hmem
-  grind [OperationPtr.getResults!.mem_iff_exists_index, hReflect val valIn index heq.symm]
+/-- Extensibility theorem for value mappings fixing a block's argument pointers across contexts. -/
+theorem ValueMapping.applyToArray_getArguments!_ext
+    {ctx ctx' : WfIRContext OpInfo} {block : BlockPtr}
+    {mapping : ValueMapping ctx ctx'}
+    (blockIn : block.InBounds ctx.raw)
+    (hArgs : mapping.applyToArray (block.getArguments! ctx.raw) = block.getArguments! ctx'.raw) :
+    ∀ (i : Nat) (hi : i < block.getNumArguments! ctx.raw),
+      (mapping ⟨block.getArgument i, (by grind)⟩).val = block.getArgument i := by
+  intro i hi
+  simp only [applyToArray, Array.ext_iff, Array.size_map, Array.size_attach,
+    BlockPtr.getArguments!.size_eq_getNumArguments!, Array.getElem_map,
+    Array.getElem_attach] at hArgs
+  grind
+
+/-! ## Conformance under refinement -/
+
+/-- Refinement preserves conformance to a type: if `sv ⊒ tv` and `sv` conforms to `ty`, then `tv`
+conforms to `ty`. -/
+@[grind →]
+theorem RuntimeValue.Conforms_of_isRefinedBy {sv tv : RuntimeValue} {ty : TypeAttr}
+    (href : sv ⊒ tv) (hconf : sv.Conforms ty) : tv.Conforms ty := by
+  obtain ⟨attr, hattr⟩ := ty
+  cases sv <;> cases attr <;> simp_all [RuntimeValue.isRefinedBy, RuntimeValue.Conforms]
+  all_goals cases tv <;> grind