From df4d072f2278fdd92638a459e75a8ff4237e0010 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 9 Aug 2026 18:17:02 -0500 Subject: [PATCH] Clean up comments in Graphs.lean and Program.lean --- lean/Spa/Language/Graphs.lean | 74 ++++++++++++++-------------------- lean/Spa/Language/Program.lean | 3 +- 2 files changed, 32 insertions(+), 45 deletions(-) diff --git a/lean/Spa/Language/Graphs.lean b/lean/Spa/Language/Graphs.lean index 23a3efb..6d285a1 100644 --- a/lean/Spa/Language/Graphs.lean +++ b/lean/Spa/Language/Graphs.lean @@ -215,33 +215,29 @@ lemma wrap_outputs (g : GGraph (Option β)) : /-! ### Embeddings -Each composition operator includes its operands into the result via an index -translation that preserves node payloads and edges. `Embed` captures exactly -those two facts, so anything defined from `nodes` and `edges` (traces, node -labels, …) can be transported along an embedding once, instead of once per -operator. +To be able to reason compositionally about traces through the graphs, +we need to be able to reason about how a trace within a sub-graph maps +to the full graph. Fortunately, graphs are built using composition operators, +and these composition operators always include their arguments as embedded +subgraphs in the full result. Moreover, each embedding "just" offsets the +existing node IDs by a given amount. -`Embed` is deliberately a structure rather than a class: for `g ⤳ g`, both the -left and the right inclusion inhabit the same type `Embed g (g ⤳ g)`, so -instance resolution could silently pick the wrong copy. Embeddings into a -composed graph are non-canonical by design; a named witness says which -inclusion is meant. - -Concretely, every embedding here is a *constant index shift*: `∙` and `⤳` lay -their operands out in consecutive blocks via `Fin.append`, and `loop` prepends its -two synthetic nodes. Storing the offset rather than an arbitrary function makes -the range of an embedding an interval by construction (`Embed.mem_range_iff`), -which is the "is this node inside that subgraph?" test. -/ +This section formalizes this fact by providing an `Embed` type that +represents an offset-based embedding, and showing that such an embedding +exists for all arguments given to graph composition operators. Furthermore, +because of the offset-based embedding, we can determine whether a node +came from a particular subgraph simply by examining its offset and sub-graph +size. This is captured by `Embed.mem_range_iff`. -/ /-- Translate an index of `g` into `h` by a constant offset. -/ -def shift {g h : GGraph α} (off : ℕ) (hle : g.size + off ≤ h.size) (i : g.Index) : +private def shift {g h : GGraph α} (off : ℕ) (hle : g.size + off ≤ h.size) (i : g.Index) : h.Index := ⟨off + i.val, by omega⟩ @[simp] lemma shift_val {g h : GGraph α} {off : ℕ} (hle : g.size + off ≤ h.size) (i : g.Index) : (shift (h := h) off hle i).val = off + i.val := rfl -/-- An embedding of `g` into `h`: a constant index shift preserving node payloads - and edges. -/ +/-- A special-case embedding of `g` into `h` in which all edges and nodes + of `g` are present in `h` at a given offset `off`. -/ structure Embed (g h : GGraph α) where off : ℕ size_le : g.size + off ≤ h.size @@ -269,7 +265,7 @@ lemma Embed.mem_range_iff {g h : GGraph α} (e : Embed g h) (j : h.Index) : the `Fin.append` lemmas are stated in — so this lets them keep those proofs verbatim while `Embed` stores only the offset. The trailing two arguments are boilerplate at every call site and default to discharging themselves. -/ -def Embed.ofIndexMap {g h : GGraph α} (off : ℕ) (k : g.Index → h.Index) +private def Embed.ofIndexMap {g h : GGraph α} (off : ℕ) (k : g.Index → h.Index) (hn : ∀ i, h.nodes (k i) = g.nodes i) (hem : ∀ {e : g.Edge}, e ∈ g.edges → (k e.1, k e.2) ∈ h.edges) (hle : g.size + off ≤ h.size := by @@ -283,45 +279,49 @@ def Embed.ofIndexMap {g h : GGraph α} (off : ℕ) (k : g.Index → h.Index) have hs : ∀ i, shift (h := h) off hle i = k i := fun i => Fin.ext (by simp [hk]) rw [hs, hs]; exact hem hmem -/-- Embeddings compose; offsets add. -/ +/-- Embeddings compose (offsets add). -/ def Embed.trans {g₁ g₂ g₃ : GGraph α} (e₁ : Embed g₁ g₂) (e₂ : Embed g₂ g₃) : Embed g₁ g₃ := - .ofIndexMap (e₂.off + e₁.off) (fun i => e₂.f (e₁.f i)) + ofIndexMap (e₂.off + e₁.off) (fun i => e₂.f (e₁.f i)) (fun i => (e₂.nodes_eq (e₁.f i)).trans (e₁.nodes_eq i)) (fun he => e₂.edges_mem (e₁.edges_mem he)) (hle := by have := e₁.size_le; have := e₂.size_le; omega) (hk := fun i => by simp; omega) -/-! The five inclusions `Stmt.cfg` uses, one per composition operator. Each `_f` -lemma recovers the `Fin.castAdd`/`Fin.natAdd` form for callers stating indices -that way (`Spa/Language/Properties.lean`). -/ - /-- The left operand's inclusion into a sequenced graph. -/ def Embed.sequenceLeft (g₁ g₂ : GGraph α) : Embed g₁ (g₁ ⤳ g₂) := - .ofIndexMap 0 (fun i => i.castAdd g₂.size) (Fin.append_left g₁.nodes g₂.nodes) + ofIndexMap 0 (fun i => i.castAdd g₂.size) (Fin.append_left g₁.nodes g₂.nodes) (fun he => List.mem_append_left _ (List.mem_append_left _ (List.mem_map_of_mem _ he))) /-- The right operand's inclusion into a sequenced graph. -/ def Embed.sequenceRight (g₁ g₂ : GGraph α) : Embed g₂ (g₁ ⤳ g₂) := - .ofIndexMap g₁.size (fun i => i.natAdd g₁.size) (Fin.append_right g₁.nodes g₂.nodes) + ofIndexMap g₁.size (fun i => i.natAdd g₁.size) (Fin.append_right g₁.nodes g₂.nodes) (fun he => List.mem_append_left _ (List.mem_append_right _ (List.mem_map_of_mem _ he))) /-- The left operand's inclusion into an overlaid graph. -/ def Embed.overlayLeft (g₁ g₂ : GGraph α) : Embed g₁ (g₁ ∙ g₂) := - .ofIndexMap 0 (fun i => i.castAdd g₂.size) (Fin.append_left g₁.nodes g₂.nodes) + ofIndexMap 0 (fun i => i.castAdd g₂.size) (Fin.append_left g₁.nodes g₂.nodes) (fun he => List.mem_append_left _ (List.mem_map_of_mem _ he)) /-- The right operand's inclusion into an overlaid graph. -/ def Embed.overlayRight (g₁ g₂ : GGraph α) : Embed g₂ (g₁ ∙ g₂) := - .ofIndexMap g₁.size (fun i => i.natAdd g₁.size) (Fin.append_right g₁.nodes g₂.nodes) + ofIndexMap g₁.size (fun i => i.natAdd g₁.size) (Fin.append_right g₁.nodes g₂.nodes) (fun he => List.mem_append_right _ (List.mem_map_of_mem _ he)) /-- The body's inclusion into a `loop` graph. -/ def Embed.loop (g : GGraph (Option β)) : Embed g (GGraph.loop g) := - .ofIndexMap 2 (fun i => i.natAdd 2) (Fin.append_right (fun _ : Fin 2 => none) g.nodes) + ofIndexMap 2 (fun i => i.natAdd 2) (Fin.append_right (fun _ : Fin 2 => none) g.nodes) (fun he => List.mem_append_left _ (List.mem_append_left _ (List.mem_append_left _ (List.mem_map_of_mem _ he)))) +/-- A `singleton` subgraph has exactly one node; this is where it sits in the ambient graph. -/ +def Embed.singletonIndex {a : α} {h : GGraph α} (e : Embed (singleton a) h) : h.Index := + e.f ⟨0, Nat.zero_lt_one⟩ + +@[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⟩ + /-! `shift` puts the offset on the left (`off + i.val`), matching `Fin.natAdd`, so every right inclusion is *definitionally* the form `Spa/Language/Properties.lean` states its trace indices in. Only the left inclusions need a bridge, since their @@ -331,18 +331,6 @@ 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 aaf98da..3accd57 100644 --- a/lean/Spa/Language/Program.lean +++ b/lean/Spa/Language/Program.lean @@ -31,8 +31,7 @@ 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). -/ +/-- The root statement's CFG sits inside the program's CFG. -/ 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) _)