diff --git a/lean/Spa/Language.lean b/lean/Spa/Language.lean index ae9f4a6..2ac6d06 100644 --- a/lean/Spa/Language.lean +++ b/lean/Spa/Language.lean @@ -3,64 +3,4 @@ import Spa.Language.Semantics import Spa.Language.Graphs import Spa.Language.Traces import Spa.Language.Properties -import Mathlib.Data.Finset.Sort -import Mathlib.Data.String.Basic - -namespace Spa - -structure Program where - rootStmt : Stmt - /-- A memoized copy of the control-flow graph. This field is an - implementation detail to avoid re-computing `Graph.wrap` and `Stmt.cfg` - every time the program's control flow graph is needed -/ - cfgCache : Thunk Graph := Thunk.mk fun _ => Graph.wrap rootStmt.cfg - -namespace Program - -variable (p : Program) - --- Runtime implementation of `cfg`: read the memoized graph. -private def cfgImpl : Graph := p.cfgCache.get - -@[implemented_by cfgImpl] -def cfg : Graph := Graph.wrap p.rootStmt.cfg - -abbrev State : Type := p.cfg.Index - -def initialState : p.State := p.rootStmt.cfg.wrapInput - -def finalState : p.State := p.rootStmt.cfg.wrapOutput - -noncomputable def trace {ρ : Env} (h : EvalStmt [] p.rootStmt ρ) : - Trace p.cfg p.initialState p.finalState [] ρ := by - obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := EndToEndTrace.wrap (Stmt.cfg_sufficient h) - rw [Graph.wrap_inputs, List.mem_singleton] at h₁ - rw [Graph.wrap_outputs, List.mem_singleton] at h₂ - subst h₁; subst h₂ - exact tr - -def vars : List String := p.rootStmt.vars.sort (· ≤ ·) - -lemma vars_nodup : p.vars.Nodup := Finset.sort_nodup _ _ - -def states : List p.State := p.cfg.indices - -lemma states_complete (s : p.State) : s ∈ p.states := p.cfg.mem_indices s - -lemma states_nodup : p.states.Nodup := p.cfg.nodup_indices - -def code (st : p.State) : Option BasicStmt := p.cfg.nodes st - -def incoming (s : p.State) : List p.State := p.cfg.predecessors s - -lemma incoming_initialState_eq_nil : p.incoming p.initialState = [] := - Graph.wrap_predecessors_eq_nil p.rootStmt.cfg p.initialState - (by rw [Graph.wrap_inputs]; exact List.mem_singleton_self _) - -lemma mem_incoming_of_edge {s₁ s₂ : p.State} - (h : (s₁, s₂) ∈ p.cfg.edges) : s₁ ∈ p.incoming s₂ := - p.cfg.mem_predecessors_of_edge h - -end Program - -end Spa +import Spa.Language.Program diff --git a/lean/Spa/Language/Graphs.lean b/lean/Spa/Language/Graphs.lean index 6f7503d..81bd5ee 100644 --- a/lean/Spa/Language/Graphs.lean +++ b/lean/Spa/Language/Graphs.lean @@ -25,6 +25,15 @@ indexing into a list. -/ +/-- Logically, when combining `Fin`s from two distinct pools, + the combination is disjoint. -/ +lemma Fin.castAdd_ne_natAdd {n m : ℕ} (i : Fin n) (j : Fin m) : + Fin.castAdd m i ≠ Fin.natAdd n j := by + intro h + have := congrArg Fin.val h + simp only [Fin.coe_castAdd, Fin.coe_natAdd] at this + omega + /-- Bump the upper bound of a list of `Fin`s without changing their value. -/ def List.finCastAdd {n : ℕ} (l : List (Fin n)) (m : ℕ) : List (Fin (n + m)) := l.map (Fin.castAdd m) @@ -157,6 +166,22 @@ def singleton (a : α) : GGraph α where def wrap (g : GGraph (Option β)) : GGraph (Option β) := singleton none ⤳ g ⤳ singleton none +/-- The input / entry node generated by `GGraph.wrap`. -/ +def wrapInput (g : GGraph (Option β)) : (wrap g).Index := + (0 : Fin 1).castAdd ((g ⤳ singleton none).size) + +/-- The output / exit node generated by `GGraph.wrap`. -/ +def wrapOutput (g : GGraph (Option β)) : (wrap g).Index := + Fin.natAdd 1 ((Fin.natAdd g.size (0 : Fin 1))) + +/-- The `wrapInput` is, indeed, the graph's only input after `wrap`. -/ +lemma wrap_inputs (g : GGraph (Option β)) : + (wrap g).inputs = [g.wrapInput] := rfl + +/-- The `wrapInput` is, indeed, the graph's only output after `wrap`. -/ +lemma wrap_outputs (g : GGraph (Option β)) : + (wrap g).outputs = [g.wrapOutput] := rfl + @[simp] lemma map_singleton (f : α → β) (a : α) : f <$> singleton a = singleton (f a) := rfl @@ -205,6 +230,35 @@ lemma nodup_indices : g.indices.Nodup := def predecessors (idx : g.Index) : List g.Index := g.indices.filter (fun idx' => (idx', idx) ∈ g.edges) +/-- When sequencing (proven here with `Graph.singleton` on the left), no edges + exist from the right-hand graph back to the left. -/ +private lemma not_mem_edges_castAdd_sequence {g₂ : GGraph (Option β)} (i : Fin 1) + (idx : (singleton none ⤳ g₂).Index) : + ((idx, i.castAdd g₂.size) : (singleton none ⤳ g₂).Edge) + ∉ (singleton none ⤳ g₂).edges := by + intro h + rcases List.mem_append.mp h with h' | h' + · rcases List.mem_append.mp h' with h'' | h'' + · -- lifted edges of `singleton []`: there are none + simp [singleton, List.finCastAddProd] at h'' + · -- lifted edges of g₂: targets are natAdd + obtain ⟨e, _, heq⟩ := List.mem_map.mp h'' + exact Fin.castAdd_ne_natAdd i e.2 (congrArg Prod.snd heq).symm + · -- product edges: targets are natAdd'd inputs of g₂ + obtain ⟨-, hb⟩ := List.mem_product.mp h' + obtain ⟨j, -, heq⟩ := List.mem_map.mp hb + exact Fin.castAdd_ne_natAdd i j heq.symm + +/-- The input node of a graph after `Graph.wrap` has no predecessors. -/ +lemma wrap_predecessors_eq_nil (g : GGraph (Option β)) (idx : (wrap g).Index) + (h : idx ∈ (wrap g).inputs) : + (wrap g).predecessors idx = [] := by + rw [wrap_inputs, List.mem_singleton] at h + subst h + rw [GGraph.predecessors, List.filter_eq_nil_iff] + intro idx' _ + simpa using not_mem_edges_castAdd_sequence (g₂ := g ⤳ singleton none) 0 idx' + /-- There's there's an edge between two nodes `idx₁` and `idx₂`, then `idx₁` is the predecessor of `idx₂`. -/ lemma mem_predecessors_of_edge {idx₁ idx₂ : g.Index} @@ -225,7 +279,7 @@ abbrev Graph : Type := GGraph (Option BasicStmt) namespace Graph -export GGraph (overlay sequence loop singleton wrap loop_inputs loop_outputs) +export GGraph (overlay sequence loop singleton wrap loop_inputs loop_outputs wrapInput wrapOutput wrap_inputs wrap_outputs) @[inherit_doc] scoped infixr:70 " ∙ " => GGraph.overlay @[inherit_doc] scoped infixr:70 " ⤳ " => GGraph.sequence diff --git a/lean/Spa/Language/Program.lean b/lean/Spa/Language/Program.lean new file mode 100644 index 0000000..eeb6c97 --- /dev/null +++ b/lean/Spa/Language/Program.lean @@ -0,0 +1,56 @@ +import Spa.Language.Base +import Spa.Language.Semantics +import Spa.Language.Graphs +import Mathlib.Data.Finset.Sort +import Mathlib.Data.String.Basic + +namespace Spa + +structure Program where + rootStmt : Stmt + /-- A memoized copy of the control-flow graph. This field is an + implementation detail to avoid re-computing `Graph.wrap` and `Stmt.cfg` + every time the program's control flow graph is needed -/ + cfgCache : Thunk Graph := Thunk.mk fun _ => Graph.wrap rootStmt.cfg + +namespace Program + +variable (p : Program) + +-- Runtime implementation of `cfg`: read the memoized graph. +private def cfgImpl : Graph := p.cfgCache.get + +@[implemented_by cfgImpl] +def cfg : Graph := Graph.wrap p.rootStmt.cfg + +abbrev State : Type := p.cfg.Index + +def vars : List String := p.rootStmt.vars.sort (· ≤ ·) + +lemma vars_nodup : p.vars.Nodup := Finset.sort_nodup _ _ + +def states : List p.State := p.cfg.indices + +lemma states_complete (s : p.State) : s ∈ p.states := p.cfg.mem_indices s + +lemma states_nodup : p.states.Nodup := p.cfg.nodup_indices + +def code (st : p.State) : Option BasicStmt := p.cfg.nodes st + +def incoming (s : p.State) : List p.State := p.cfg.predecessors s + +def initialState : p.State := Graph.wrapInput p.rootStmt.cfg + +def finalState : p.State := Graph.wrapOutput p.rootStmt.cfg + +lemma mem_incoming_of_edge {s₁ s₂ : p.State} + (h : (s₁, s₂) ∈ p.cfg.edges) : s₁ ∈ p.incoming s₂ := + p.cfg.mem_predecessors_of_edge h + +lemma incoming_initialState_eq_nil : p.incoming p.initialState = [] := + GGraph.wrap_predecessors_eq_nil p.rootStmt.cfg p.initialState + (by rw [Graph.wrap_inputs]; exact List.mem_singleton_self _) + +end Program + +end Spa diff --git a/lean/Spa/Language/Properties.lean b/lean/Spa/Language/Properties.lean index 0e40f2b..8a03684 100644 --- a/lean/Spa/Language/Properties.lean +++ b/lean/Spa/Language/Properties.lean @@ -23,13 +23,6 @@ namespace Spa open Graph -lemma Fin.castAdd_ne_natAdd {n m : ℕ} (i : Fin n) (j : Fin m) : - Fin.castAdd m i ≠ Fin.natAdd n j := by - intro h - have := congrArg Fin.val h - simp only [Fin.coe_castAdd, Fin.coe_natAdd] at this - omega - section Embeddings variable {g₁ g₂ : Graph} {ρ₁ ρ₂ : Env} @@ -246,49 +239,17 @@ noncomputable def Stmt.cfg_sufficient {s : Stmt} {ρ₁ ρ₂ : Env} | whileFalse ρ e s _ => exact EndToEndTrace.loop_empty -/-- The input / entry node generated by `Graph.wrap`. -/ -def Graph.wrapInput (g : Graph) : (Graph.wrap g).Index := - (0 : Fin 1).castAdd ((g ⤳ Graph.singleton none).size) +namespace Program -/-- The output / exit node generated by `Graph.wrap`. -/ -def Graph.wrapOutput (g : Graph) : (Graph.wrap g).Index := - Fin.natAdd 1 ((Fin.natAdd g.size (0 : Fin 1))) +noncomputable def trace (p : Program) {ρ : Env} (h : EvalStmt [] p.rootStmt ρ) : + Trace p.cfg p.initialState p.finalState [] ρ := by + obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := EndToEndTrace.wrap (Stmt.cfg_sufficient h) + rw [Graph.wrap_inputs, List.mem_singleton] at h₁ + rw [Graph.wrap_outputs, List.mem_singleton] at h₂ + subst h₁; subst h₂ + exact tr -/-- The `Graph.wrapInput` is, indeed, the graph's only input after `Graph.wrap`. -/ -lemma Graph.wrap_inputs (g : Graph) : - (Graph.wrap g).inputs = [g.wrapInput] := rfl +end Program -/-- The `Graph.wrapInput` is, indeed, the graph's only output after `Graph.wrap`. -/ -lemma Graph.wrap_outputs (g : Graph) : - (Graph.wrap g).outputs = [g.wrapOutput] := rfl - -/-- When sequencing (proven here with `Graph.singleton` on the left), no edges - exist from the right-hand graph back to the left. -/ -private lemma not_mem_edges_castAdd_sequence {g₂ : Graph} (i : Fin 1) - (idx : (Graph.singleton none ⤳ g₂).Index) : - ((idx, i.castAdd g₂.size) : (Graph.singleton none ⤳ g₂).Edge) - ∉ (Graph.singleton none ⤳ g₂).edges := by - intro h - rcases List.mem_append.mp h with h' | h' - · rcases List.mem_append.mp h' with h'' | h'' - · -- lifted edges of `singleton []`: there are none - simp [Graph.singleton, List.finCastAddProd] at h'' - · -- lifted edges of g₂: targets are natAdd - obtain ⟨e, _, heq⟩ := List.mem_map.mp h'' - exact Fin.castAdd_ne_natAdd i e.2 (congrArg Prod.snd heq).symm - · -- product edges: targets are natAdd'd inputs of g₂ - obtain ⟨-, hb⟩ := List.mem_product.mp h' - obtain ⟨j, -, heq⟩ := List.mem_map.mp hb - exact Fin.castAdd_ne_natAdd i j heq.symm - -/-- The input node of a graph after `Graph.wrap` has no predecessors. -/ -lemma Graph.wrap_predecessors_eq_nil (g : Graph) (idx : (Graph.wrap g).Index) - (h : idx ∈ (Graph.wrap g).inputs) : - (Graph.wrap g).predecessors idx = [] := by - rw [Graph.wrap_inputs, List.mem_singleton] at h - subst h - rw [GGraph.predecessors, List.filter_eq_nil_iff] - intro idx' _ - simpa using not_mem_edges_castAdd_sequence (g₂ := g ⤳ Graph.singleton none) 0 idx' end Spa diff --git a/lean/Spa/Language/Traces.lean b/lean/Spa/Language/Traces.lean index 71bc13f..55478fb 100644 --- a/lean/Spa/Language/Traces.lean +++ b/lean/Spa/Language/Traces.lean @@ -1,5 +1,6 @@ import Spa.Language.Semantics import Spa.Language.Graphs +import Spa.Language.Program /-!