Add more machinery to use embeddings as "proofs of child-ship"

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) :

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 (· ≤ ·)