From 59afbdaf71ab7c668cd50edc36ca14c595c58e74 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Mon, 29 Jun 2026 10:00:01 -0500
Subject: [PATCH] Rename StateInterp to match the style of the rest of the
 codebase

---
 lean/Spa/Analysis/Forward.lean          | 4 ++--
 lean/Spa/Analysis/Forward/Lattices.lean | 8 ++++----
 lean/Spa/Analysis/Reaching.lean         | 2 +-
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/lean/Spa/Analysis/Forward.lean b/lean/Spa/Analysis/Forward.lean
index cb9042c..f51dc8f 100644
--- a/lean/Spa/Analysis/Forward.lean
+++ b/lean/Spa/Analysis/Forward.lean
@@ -64,7 +64,7 @@ lemma joinForKey_initialState :
   rfl
 
 class ValidStateEvaluator (L : Type) [FiniteHeightLattice L] (prog : Program)
-    [E : StmtEvaluator L prog] [S : StateInterp L prog] where
+    [E : StmtEvaluator L prog] [S : StateInterpretation L prog] where
   step : (s : prog.State) → {ρ₁ ρ₂ : Env} → {bs : BasicStmt} →
     prog.code s = some bs → EvalBasicStmt ρ₁ bs ρ₂ → S.St ρ₁ → S.St ρ₂
   valid : ∀ (s : prog.State) {ρ₁ ρ₂ : Env} {bs : BasicStmt}
@@ -80,7 +80,7 @@ instance [LatticeInterpretation L] [ValidStmtEvaluator L prog] :
   botV_init := by intro k l _ v hmem; cases hmem
 
 section
-variable [S : StateInterp L prog] [V : ValidStateEvaluator L prog]
+variable [S : StateInterpretation L prog] [V : ValidStateEvaluator L prog]
 
 noncomputable def stepStmtOrNone (s : prog.State) {ρ₁ ρ₂ : Env} :
     (o : Option BasicStmt) → prog.code s = o → EvalBasicStmtOpt ρ₁ o ρ₂ →
diff --git a/lean/Spa/Analysis/Forward/Lattices.lean b/lean/Spa/Analysis/Forward/Lattices.lean
index 1af6aa4..5234b1a 100644
--- a/lean/Spa/Analysis/Forward/Lattices.lean
+++ b/lean/Spa/Analysis/Forward/Lattices.lean
@@ -64,7 +64,7 @@ lemma variablesAt_joinAll (s : prog.State) (sv : StateVariables L prog) :
     variablesAt s (joinAll sv) = joinForKey s sv :=
   joinAll_mem_eq (variablesAt_mem s (joinAll sv))
 
-class StateInterp (L : Type) [Lattice L] (prog : Program) where
+class StateInterpretation (L : Type) [Lattice L] (prog : Program) where
   St : Env → Type
   init : St []
   interp : VariableValues L prog → (ρ : Env) → St ρ → Prop
@@ -73,11 +73,11 @@ class StateInterp (L : Type) [Lattice L] (prog : Program) where
   interp_inf : ∀ {vs₁ vs₂ : VariableValues L prog} {ρ : Env} {st : St ρ},
     interp vs₁ ρ st ∧ interp vs₂ ρ st → interp (vs₁ ⊓ vs₂) ρ st
 
-instance [S : StateInterp L prog] :
+instance [S : StateInterpretation L prog] :
     Interp (VariableValues L prog) ((ρ : Env) → S.St ρ → Prop) :=
   ⟨S.interp⟩
 
-lemma interp_foldr [S : StateInterp L prog]
+lemma interp_foldr [S : StateInterpretation L prog]
     {vs : VariableValues L prog} {vss : List (VariableValues L prog)}
     {ρ : Env} {st : S.St ρ} (hvs : ⟦ vs ⟧ ρ st) (hmem : vs ∈ vss) :
     ⟦ vss.foldr (· ⊔ ·) (botV L prog) ⟧ ρ st := by
@@ -90,7 +90,7 @@ lemma interp_foldr [S : StateInterp L prog]
 
 variable [I : LatticeInterpretation L]
 
-instance : StateInterp L prog where
+instance : StateInterpretation L prog where
   St := fun _ => PUnit
   init := PUnit.unit
   interp vs ρ _ := ∀ (k : String) (l : L), (k, l) ∈ vs →
diff --git a/lean/Spa/Analysis/Reaching.lean b/lean/Spa/Analysis/Reaching.lean
index f4a4eed..fdbd202 100644
--- a/lean/Spa/Analysis/Reaching.lean
+++ b/lean/Spa/Analysis/Reaching.lean
@@ -58,7 +58,7 @@ inductive LastAssign (prog : Program) (x : String) : Run prog → prog.NodeId 
       (∀ e, bs ≠ .assign x e) → LastAssign prog x rest n →
       LastAssign prog x (Run.cons s bs hc rest) n
 
-instance stateInterp : StateInterp (DefSet prog) prog where
+instance stateInterp : StateInterpretation (DefSet prog) prog where
   St := fun _ => Run prog
   init := Run.nil
   interp vs _ run := ∀ (x : String) (assigners : DefSet prog), (x, assigners) ∈ vs →