Clean up comments in Graphs.lean and Program.lean
This commit is contained in:
@@ -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) :
|
||||
|
||||
@@ -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) _)
|
||||
|
||||
Reference in New Issue
Block a user