From 1eecf45c0ff554619220fa24eb1af1661cbf9b74 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 9 Aug 2026 17:30:38 -0500
Subject: [PATCH] Add more machinery to use embeddings as "proofs of
 child-ship"

---
 lean/Spa/Language/Graphs.lean  | 12 ++++++++++++
 lean/Spa/Language/Program.lean |  6 ++++++
 2 files changed, 18 insertions(+)

diff --git a/lean/Spa/Language/Graphs.lean b/lean/Spa/Language/Graphs.lean
index 9c68457..23a3efb 100644
--- a/lean/Spa/Language/Graphs.lean
+++ b/lean/Spa/Language/Graphs.lean
@@ -331,6 +331,18 @@ Deliberately not `@[simp]`: they rewrite `Embed.f` back into `Fin.castAdd` form,
 discarding the offset that `Embed.mem_range_iff` — and the subgraph-containment
 tests built on it — reason with. -/
 
+/-- A `singleton` subgraph has exactly one node; this is where it sits in the
+    ambient graph.  This is how a traversal that has descended to a `Stmt.basic`
+    reads off its CFG index, since `(Stmt.basic bs).cfg` is `singleton (some bs)`. -/
+def Embed.singletonIndex {a : α} {h : GGraph α} (e : Embed (singleton a) h) : h.Index :=
+  e.f ⟨0, Nat.zero_lt_one⟩
+
+/-- …and the node there carries exactly that statement — so an index obtained this
+    way comes with its payload already identified, with no lookup and no `Option`. -/
+@[simp] lemma Embed.nodes_singletonIndex {a : α} {h : GGraph α}
+    (e : Embed (singleton a) h) : h.nodes e.singletonIndex = a :=
+  e.nodes_eq ⟨0, Nat.zero_lt_one⟩
+
 lemma Embed.sequenceLeft_f (g₁ g₂ : GGraph α) (i : g₁.Index) :
     (Embed.sequenceLeft g₁ g₂).f i = i.castAdd g₂.size := Fin.ext (Nat.zero_add _)
 lemma Embed.overlayLeft_f (g₁ g₂ : GGraph α) (i : g₁.Index) :
diff --git a/lean/Spa/Language/Program.lean b/lean/Spa/Language/Program.lean
index 854a146..aaf98da 100644
--- a/lean/Spa/Language/Program.lean
+++ b/lean/Spa/Language/Program.lean
@@ -31,6 +31,12 @@ def cfg : Graph := Graph.wrap p.rootStmt.cfg
 /-- A state in the control flow `Spa.Graph` of this program. -/
 abbrev State : Type := p.cfg.Index
 
+/-- The root statement's CFG sits inside the program's CFG (that graph `wrap`ped
+    in an entry and an exit node). -/
+def rootEmbed : GGraph.Embed p.rootStmt.cfg p.cfg :=
+  (GGraph.Embed.sequenceLeft p.rootStmt.cfg (Graph.singleton none)).trans
+    (GGraph.Embed.sequenceRight (Graph.singleton none) _)
+
 /-- Variables mentioned or defined in this program. -/
 def vars : List String := p.rootStmt.vars.sort (· ≤ ·)