From ac99bc047ae426801780f5a9d2b7a3a415db5311 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Tue, 6 Oct 2026 20:16:35 -0500
Subject: [PATCH] Show that if x is not assigned within a segment, its value
 remains as before

---
 lean/Spa.lean                         |  1 +
 lean/Spa/Analysis/Reaching/Paths.lean | 54 +++++++++++++++++++++++++++
 2 files changed, 55 insertions(+)
 create mode 100644 lean/Spa/Analysis/Reaching/Paths.lean

diff --git a/lean/Spa.lean b/lean/Spa.lean
index 9aa3513..7583ecd 100644
--- a/lean/Spa.lean
+++ b/lean/Spa.lean
@@ -22,5 +22,6 @@ import Spa.Analysis.Utils
 import Spa.Analysis.Sign
 import Spa.Analysis.Constant
 import Spa.Analysis.Reaching
+import Spa.Analysis.Reaching.Paths
 import Spa.Transformation.Licm
 import Spa.Transformation.Constant
diff --git a/lean/Spa/Analysis/Reaching/Paths.lean b/lean/Spa/Analysis/Reaching/Paths.lean
new file mode 100644
index 0000000..1f96385
--- /dev/null
+++ b/lean/Spa/Analysis/Reaching/Paths.lean
@@ -0,0 +1,54 @@
+import Spa.Analysis.Reaching
+import Spa.Language.TraceProperties
+
+namespace Spa
+namespace ReachingAnalysis
+
+/-- The most recent assignment occurs in the history being searched. -/
+lemma LastAssign.mem {prog : Program} {x : String} {run : Run prog} {d : prog.State}
+    (h : LastAssign prog x run d) : d ∈ run := by
+  induction h <;> aesop
+
+/-- Appending older history cannot displace an already-found assignment. -/
+lemma LastAssign.append {prog : Program} {x : String} {new : Run prog} {d : prog.State}
+    (h : LastAssign prog x new d) (old : Run prog) :
+    LastAssign prog x (new ++ old) d := by
+  induction h with
+  | here s rhs rest hc => exact .here s rhs _ hc
+  | there s rest hn h ih => exact .there s _ hn ih
+
+/-- A history containing a write to `x` has a most recent assignment to `x`. -/
+lemma lastAssign_of_write {prog : Program} {x : String} {run : Run prog}
+    (hw : ∃ d ∈ run, ∃ rhs, prog.code d = some (.assign x rhs)) :
+    ∃ d, LastAssign prog x run d := by
+  induction run with
+  | nil => simp at hw
+  | cons d rest ih =>
+      by_cases hx : ∃ rhs, prog.code d = some (.assign x rhs)
+      · obtain ⟨rhs, hc⟩ := hx
+        exact ⟨d, .here d rhs rest hc⟩
+      · have hw' : ∃ j ∈ rest, ∃ rhs, prog.code j = some (.assign x rhs) := by
+          obtain ⟨j, hm, rhs, hc⟩ := hw
+          rcases List.mem_cons.mp hm with rfl | hm
+          · exact False.elim (hx ⟨rhs, hc⟩)
+          · exact ⟨j, hm, rhs, hc⟩
+        obtain ⟨j, hj⟩ := ih hw'
+        exact ⟨j, .there d rest (by simpa using hx) hj⟩
+
+/-- Outside reaching definitions rule out any write in a confined intervening
+path. No equality of static sites is used to infer equality of events. -/
+lemma Path.preserves_of_lastAssign_outside {prog : Program}
+    {a b c : Configuration prog.cfg} (pre : Path prog.cfg a b) (seg : Path prog.cfg b c)
+    {x : String} (sites : Set prog.State)
+    (hin : ∀ d ∈ seg.steps, d ∈ sites)
+    (hout : ∀ d, LastAssign prog x (runOfPath prog (pre.append seg)) d → d ∉ sites) :
+    ∀ v, Env.Mem (x, v) b.2 ↔ Env.Mem (x, v) c.2 := by
+  apply seg.preserves_unwritten
+  intro d hm rhs hc
+  obtain ⟨j, hl⟩ := lastAssign_of_write ⟨d, List.mem_reverse.mpr hm, rhs, hc⟩
+  apply hout j
+  · simpa [runOfPath, List.reverse_append] using hl.append (runOfPath prog pre)
+  · exact hin j (List.mem_reverse.mp hl.mem)
+
+end ReachingAnalysis
+end Spa