From 655b7de68490875112a7ec66f8f53a16036041f8 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Tue, 6 Oct 2026 19:30:35 -0500
Subject: [PATCH] Switch steps to not redundantly include code

---
 lean/Spa/Analysis/Reaching.lean | 28 ++++++++++++++--------------
 lean/Spa/Language/Traces.lean   | 19 ++++++++++---------
 2 files changed, 24 insertions(+), 23 deletions(-)

diff --git a/lean/Spa/Analysis/Reaching.lean b/lean/Spa/Analysis/Reaching.lean
index 323e878..02bff45 100644
--- a/lean/Spa/Analysis/Reaching.lean
+++ b/lean/Spa/Analysis/Reaching.lean
@@ -40,20 +40,20 @@ instance stmtEvaluator : StmtEvaluator (DefSet prog) prog :=
 def output : String :=
   show' (result (DefSet prog) prog)
 
-/-- The statements a trace executed, paired with the state each executed at,
-    most recent first (matching `LastAssign`, which scans for the most recent
-    assignment). This is `Path.steps` (chronological) reversed, so facts about
-    concatenating traces reduce to mathlib's `List.append`/`List.reverse` lemmas. -/
-abbrev Run (prog : Program) : Type := List (prog.State × BasicStmt)
+/-- Executed nodes, most recent first. Instructions are read from `prog.code`.
+    This is `Path.steps` (chronological) reversed, so facts about concatenating
+    traces reduce to mathlib's `List.append`/`List.reverse` lemmas. -/
+abbrev Run (prog : Program) : Type := List prog.State
 
+/-- The first node in a newest-first history whose instruction assigns `x`. -/
 @[aesop unsafe cases]
 inductive LastAssign (prog : Program) (x : String) : Run prog → prog.State → Prop
-  | here (s : prog.State) (e : Expr) (rest : Run prog) :
-      LastAssign prog x ((s, .assign x e) :: rest) s
-  | there (s : prog.State) (bs : BasicStmt) (hc : prog.code s = some bs)
-      (rest : Run prog) {n : prog.State} :
-      (∀ e, bs ≠ .assign x e) → LastAssign prog x rest n →
-      LastAssign prog x ((s, bs) :: rest) n
+  | here (s : prog.State) (e : Expr) (rest : Run prog)
+      (hc : prog.code s = some (.assign x e)) :
+      LastAssign prog x (s :: rest) s
+  | there (s : prog.State) (rest : Run prog) {n : prog.State} :
+      (∀ e, prog.code s ≠ some (.assign x e)) → LastAssign prog x rest n →
+      LastAssign prog x (s :: rest) n
 
 def runOfPath {a b : Configuration prog.cfg} (p : Path prog.cfg a b) : Run prog :=
   p.steps.reverse
@@ -97,16 +97,16 @@ private lemma valid_step (s : prog.State) {ρ₁ ρ₂ : Env}
   cases hbs with
   | noop =>
     simp [eval, hcode, EvalBasicStmtOpt.steps]
-    intro x assigners hmem n hla; aesop
+    intro x assigners hmem n hla; aesop (add simp hcode)
   | assign x e v hev =>
     simp [eval, hcode, EvalBasicStmtOpt.steps]; intro k assigners hmem n hla
     by_cases hx : k = x
     · subst hx
       have hd := FiniteMap.generalizedUpdate_mem_eq (List.mem_singleton.mpr rfl) hmem
-      rcases hla <;> simp [hd] <;> aesop
+      rcases hla <;> simp [hd] <;> aesop (add simp hcode)
     · have hmem' := FiniteMap.generalizedUpdate_not_mem_backward
         (fun hc => hx (List.mem_singleton.mp hc)) hmem
-      aesop
+      aesop (add simp hcode)
 
 instance validStateEvaluator : ValidStateEvaluator (DefSet prog) prog where
   valid := by
diff --git a/lean/Spa/Language/Traces.lean b/lean/Spa/Language/Traces.lean
index 409dc10..878cf14 100644
--- a/lean/Spa/Language/Traces.lean
+++ b/lean/Spa/Language/Traces.lean
@@ -186,27 +186,28 @@ instance {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
     HAppend (Traceₗ g idx₁ idx₂ ρ₁ ρ₂) (EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃)
       (Trace g idx₁ idx₂ ρ₁ ρ₃) := ⟨Traceₗ.appendStep⟩
 
-/-- The (index, statement) pairs executed by a single optional-statement step. -/
+/-- The node executed by an optional-statement step; empty nodes are omitted. -/
 def EvalBasicStmtOpt.steps {α : Type*} (idx : α) {ρ₁ ρ₂ : Env} {obs : Option BasicStmt} :
-    EvalBasicStmtOpt ρ₁ obs ρ₂ → List (α × BasicStmt)
+    EvalBasicStmtOpt ρ₁ obs ρ₂ → List α
   | .none => []
-  | .some (bs := bs) _ => [(idx, bs)]
+  | .some _ => [idx]
 
-def Step.steps {g : Graph} {a b : Configuration g} : Step g a b → List (g.Index × BasicStmt)
+def Step.steps {g : Graph} {a b : Configuration g} : Step g a b → List g.Index
   | .execute (i := i) h => h.steps i
   | .edge _ => []
 
-/-- Executed statements in chronological order; edges and empty nodes contribute nothing. -/
-def Path.steps {g : Graph} {a b : Configuration g} : Path g a b → List (g.Index × BasicStmt)
+/-- Executed nodes in chronological order; edges and empty nodes contribute nothing.
+The instruction at each node is given by `g.nodes`, rather than copied into the history. -/
+def Path.steps {g : Graph} {a b : Configuration g} : Path g a b → List g.Index
   | .nil => []
   | .cons s p => s.steps ++ p.steps
 
 abbrev Trace.steps {g : Graph} {i j : g.Index} {ρ₁ ρ₂ : Env}
-    (p : Trace g i j ρ₁ ρ₂) : List (g.Index × BasicStmt) := Path.steps p
+    (p : Trace g i j ρ₁ ρ₂) : List g.Index := Path.steps p
 abbrev Traceₗ.steps {g : Graph} {i j : g.Index} {ρ₁ ρ₂ : Env}
-    (p : Traceₗ g i j ρ₁ ρ₂) : List (g.Index × BasicStmt) := Path.steps p
+    (p : Traceₗ g i j ρ₁ ρ₂) : List g.Index := Path.steps p
 abbrev Traceᵣ.steps {g : Graph} {i j : g.Index} {ρ₁ ρ₂ : Env}
-    (p : Traceᵣ g i j ρ₁ ρ₂) : List (g.Index × BasicStmt) := Path.steps p
+    (p : Traceᵣ g i j ρ₁ ρ₂) : List g.Index := Path.steps p
 
 @[simp] lemma Path.steps_append {g : Graph} {a b c : Configuration g}
     (p : Path g a b) (q : Path g b c) :