Switch steps to not redundantly include code

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