From 2cfd0a2fb7155495407e983a3ddb64d5655bbae3 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Tue, 9 Jun 2026 19:30:42 -0700 Subject: [PATCH] Lean migration: Phase 5 (language, CFGs, traces, Program) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Spa.Language.Base: Expr/BasicStmt/Stmt + HasVar relations; StringSet lifts to Finset String - Spa.Language.Semantics: Value/Env/Env.Mem, big-step relations, LatticeInterpretation (respects-≈ field drops out with =) - Spa.Language.Graphs: Graph with nodes : Fin size → List BasicStmt (Vec lookup lemmas lift to Fin.append_left/right), comp/link/loop/ skipto/singleton/wrap/buildCfg, predecessors via List.finRange - Spa.Language.Traces: Trace + EndToEndTrace (Prop-valued) - Spa.Language.Properties: trace embeddings, loop lemmas, buildCfg_sufficient; the 80-line Fin-disjointness block reduces to castAdd_ne_natAdd + mathlib list lemmas - Spa.Language: Program (vars via Finset.sort — toList is noncomputable) Co-Authored-By: Claude Fable 5 --- .claude/settings.json | 9 + LEAN_MIGRATION.md | 2 +- lean/Spa.lean | 6 + lean/Spa/Language.lean | 90 ++++++++++ lean/Spa/Language/Base.lean | 78 +++++++++ lean/Spa/Language/Graphs.lean | 169 ++++++++++++++++++ lean/Spa/Language/Properties.lean | 282 ++++++++++++++++++++++++++++++ lean/Spa/Language/Semantics.lean | 90 ++++++++++ lean/Spa/Language/Traces.lean | 38 ++++ 9 files changed, 763 insertions(+), 1 deletion(-) create mode 100644 .claude/settings.json create mode 100644 lean/Spa/Language.lean create mode 100644 lean/Spa/Language/Base.lean create mode 100644 lean/Spa/Language/Graphs.lean create mode 100644 lean/Spa/Language/Properties.lean create mode 100644 lean/Spa/Language/Semantics.lean create mode 100644 lean/Spa/Language/Traces.lean diff --git a/.claude/settings.json b/.claude/settings.json new file mode 100644 index 0000000..4bd390f --- /dev/null +++ b/.claude/settings.json @@ -0,0 +1,9 @@ +{ + "permissions": { + "allow": [ + "Bash(lake build)", + "Bash(lake build *)", + "Bash(export PATH=\"$HOME/.elan/bin:$PATH\")" + ] + } +} diff --git a/LEAN_MIGRATION.md b/LEAN_MIGRATION.md index 28c8971..17d529b 100644 --- a/LEAN_MIGRATION.md +++ b/LEAN_MIGRATION.md @@ -78,6 +78,6 @@ validate phase by phase. - [x] Phase 2 - [x] Phase 3 - [x] Phase 4 -- [ ] Phase 5 +- [x] Phase 5 - [ ] Phase 6 - [ ] Phase 7 diff --git a/lean/Spa.lean b/lean/Spa.lean index 1fb1ff1..352d792 100644 --- a/lean/Spa.lean +++ b/lean/Spa.lean @@ -6,3 +6,9 @@ import Spa.Lattice.Prod import Spa.Lattice.AboveBelow import Spa.Lattice.IterProd import Spa.Lattice.FiniteMap +import Spa.Language.Base +import Spa.Language.Semantics +import Spa.Language.Graphs +import Spa.Language.Traces +import Spa.Language.Properties +import Spa.Language diff --git a/lean/Spa/Language.lean b/lean/Spa/Language.lean new file mode 100644 index 0000000..e1596c1 --- /dev/null +++ b/lean/Spa/Language.lean @@ -0,0 +1,90 @@ +/- +Port of `Language.agda` (the `Program` record and re-exports). + +Correspondence: + Program record ↦ structure Program (defs in the `Program` namespace) + graph ↦ Program.graph + State ↦ Program.State + initialState ↦ Program.initialState + finalState ↦ Program.finalState + trace ↦ Program.trace + vars, vars-Unique ↦ Program.vars, Program.vars_nodup + (Finset.toList + Finset.nodup_toList replace + `to-Listˢ` and the intrinsic MapSet uniqueness) + states, states-complete, states-Unique + ↦ Program.states, .states_complete, .states_nodup + code ↦ Program.code + _≟_, _≟ᵉ_ ↦ (instances, automatic for Fin/products) + incoming ↦ Program.incoming + initialState-pred-∅ ↦ Program.incoming_initialState_eq_nil + edge⇒incoming ↦ Program.mem_incoming_of_edge +-/ +import Spa.Language.Base +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 + +namespace Program + +variable (p : Program) + +def graph : Graph := Graph.wrap (buildCfg p.rootStmt) + +abbrev State : Type := p.graph.Index + +def initialState : p.State := (buildCfg p.rootStmt).wrapInput + +def finalState : p.State := (buildCfg p.rootStmt).wrapOutput + +/-- Agda: `Program.trace`. -/ +theorem trace {ρ : Env} (h : EvalStmt [] p.rootStmt ρ) : + Trace p.graph p.initialState p.finalState [] ρ := by + obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := EndToEndTrace.wrap (buildCfg_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 + +/-- Agda: `vars` (via `vars-Set = Stmt-vars rootStmt`). `Finset.toList` is +noncomputable, so the variables are listed in sorted order instead — this is +the computable stand-in for MapSet's `to-List`. -/ +def vars : List String := p.rootStmt.vars.sort (· ≤ ·) + +/-- Agda: `vars-Unique`. -/ +theorem vars_nodup : p.vars.Nodup := Finset.sort_nodup _ _ + +def states : List p.State := p.graph.indices + +/-- Agda: `states-complete`. -/ +theorem states_complete (s : p.State) : s ∈ p.states := p.graph.mem_indices s + +/-- Agda: `states-Unique`. -/ +theorem states_nodup : p.states.Nodup := p.graph.nodup_indices + +/-- Agda: `code`. -/ +def code (st : p.State) : List BasicStmt := p.graph.nodes st + +/-- Agda: `incoming`. -/ +def incoming (s : p.State) : List p.State := p.graph.predecessors s + +/-- Agda: `initialState-pred-∅`. -/ +theorem incoming_initialState_eq_nil : p.incoming p.initialState = [] := + Graph.wrap_predecessors_eq_nil (buildCfg p.rootStmt) p.initialState + (by rw [Graph.wrap_inputs]; exact List.mem_singleton_self _) + +/-- Agda: `edge⇒incoming`. -/ +theorem mem_incoming_of_edge {s₁ s₂ : p.State} + (h : (s₁, s₂) ∈ p.graph.edges) : s₁ ∈ p.incoming s₂ := + p.graph.mem_predecessors_of_edge h + +end Program + +end Spa diff --git a/lean/Spa/Language/Base.lean b/lean/Spa/Language/Base.lean new file mode 100644 index 0000000..2c596d5 --- /dev/null +++ b/lean/Spa/Language/Base.lean @@ -0,0 +1,78 @@ +/- +Port of `Language/Base.agda`. + +`StringSet` (built on `Lattice/MapSet.agda`, itself on `Lattice/Map.agda`) is +lifted to mathlib's `Finset String`: `insertˢ ↦ insert`, `emptyˢ ↦ ∅`, +`singletonˢ ↦ {·}`, `_⊔ˢ_ ↦ ∪`, `to-List ↦ Finset.toList` (with +`Finset.nodup_toList` standing in for the intrinsic `Unique` proof). + +Constructor renaming (Agda mixfix has no direct Lean counterpart): + _+_ ↦ Expr.add _-_ ↦ Expr.sub `_ ↦ Expr.var #_ ↦ Expr.num + _←_ ↦ BasicStmt.assign noop ↦ BasicStmt.noop + ⟨_⟩ ↦ Stmt.basic _then_ ↦ Stmt.andThen + if_then_else_ ↦ Stmt.ifElse while_repeat_ ↦ Stmt.whileLoop + +The `_∈ᵉ_` / `_∈ᵇ_` variable-occurrence relations are ported as +`Expr.HasVar` / `BasicStmt.HasVar`; the commented-out lemmas relating them to +`Expr-vars` remain unported (they were commented out in the Agda, too). +-/ +import Mathlib.Data.Finset.Basic + +namespace Spa + +inductive Expr where + | add (e₁ e₂ : Expr) + | sub (e₁ e₂ : Expr) + | var (x : String) + | num (n : ℕ) + deriving DecidableEq + +inductive BasicStmt where + | assign (x : String) (e : Expr) + | noop + deriving DecidableEq + +inductive Stmt where + | basic (bs : BasicStmt) + | andThen (s₁ s₂ : Stmt) + | ifElse (e : Expr) (s₁ s₂ : Stmt) + | whileLoop (e : Expr) (s : Stmt) + deriving DecidableEq + +/-- Agda: `_∈ᵉ_`. -/ +inductive Expr.HasVar : String → Expr → Prop + | addLeft {e₁ e₂ k} : Expr.HasVar k e₁ → Expr.HasVar k (.add e₁ e₂) + | addRight {e₁ e₂ k} : Expr.HasVar k e₂ → Expr.HasVar k (.add e₁ e₂) + | subLeft {e₁ e₂ k} : Expr.HasVar k e₁ → Expr.HasVar k (.sub e₁ e₂) + | subRight {e₁ e₂ k} : Expr.HasVar k e₂ → Expr.HasVar k (.sub e₁ e₂) + | here {k} : Expr.HasVar k (.var k) + +/-- Agda: `_∈ᵇ_`. -/ +inductive BasicStmt.HasVar : String → BasicStmt → Prop + | assignLeft {k e} : BasicStmt.HasVar k (.assign k e) + | assignRight {k k' e} : Expr.HasVar k e → BasicStmt.HasVar k (.assign k' e) + +/-- Agda: `Expr-vars`. -/ +def Expr.vars : Expr → Finset String + | .add l r => l.vars ∪ r.vars + | .sub l r => l.vars ∪ r.vars + | .var s => {s} + | .num _ => ∅ + +/-- Agda: `BasicStmt-vars`. -/ +def BasicStmt.vars : BasicStmt → Finset String + | .assign x e => {x} ∪ e.vars + | .noop => ∅ + +/-- Agda: `Stmt-vars`. -/ +def Stmt.vars : Stmt → Finset String + | .basic bs => bs.vars + | .andThen s₁ s₂ => s₁.vars ∪ s₂.vars + | .ifElse e s₁ s₂ => (e.vars ∪ s₁.vars) ∪ s₂.vars + | .whileLoop e s => e.vars ∪ s.vars + +/-- Agda: `Stmts-vars`. -/ +def Stmt.varsList (ss : List Stmt) : Finset String := + ss.foldr (fun s acc => s.vars ∪ acc) ∅ + +end Spa diff --git a/lean/Spa/Language/Graphs.lean b/lean/Spa/Language/Graphs.lean new file mode 100644 index 0000000..c7756b3 --- /dev/null +++ b/lean/Spa/Language/Graphs.lean @@ -0,0 +1,169 @@ +/- +Port of `Language/Graphs.agda`. + +Representation note: `nodes : Vec (List BasicStmt) size` becomes +`nodes : Fin size → List BasicStmt`. With that, the `Data.Vec` lookup/append +lemma stack (`lookup-++ˡ/ʳ`, `cast-is-id`, …) lifts into mathlib's +`Fin.append` with `Fin.append_left` / `Fin.append_right`. + +Correspondence: + _↑ˡ_/_↑ʳ_ (on Fin) ↦ Fin.castAdd / Fin.natAdd (mathlib) + _↑ˡⁱ_/_↑ʳⁱ_ ↦ liftIdxL / liftIdxR + _↑ˡᵉ_/_↑ʳᵉ_ ↦ liftEdgeL / liftEdgeR + _∙_ ↦ Graph.comp (scoped notation ∙) + _↦_ ↦ Graph.link (scoped notation ⤳) + loop ↦ Graph.loop + _skipto_ ↦ Graph.skipto + _[_] ↦ Graph.nodes (plain application) + singleton, wrap ↦ Graph.singleton, Graph.wrap + buildCfg ↦ buildCfg + indices ↦ List.finRange (mathlib; `fins` from Utils.agda) + indices-complete ↦ List.mem_finRange + indices-Unique ↦ List.nodup_finRange + predecessors ↦ Graph.predecessors + edge⇒predecessor ↦ Graph.mem_predecessors_of_edge + predecessor⇒edge ↦ Graph.edge_of_mem_predecessors +-/ +import Spa.Language.Base +import Mathlib.Data.Fin.Tuple.Basic +import Mathlib.Data.List.ProdSigma +import Mathlib.Data.List.FinRange + +namespace Spa + +structure Graph where + size : ℕ + nodes : Fin size → List BasicStmt + edges : List (Fin size × Fin size) + inputs : List (Fin size) + outputs : List (Fin size) + +namespace Graph + +abbrev Index (g : Graph) : Type := Fin g.size + +abbrev Edge (g : Graph) : Type := g.Index × g.Index + +/-- Agda: `_↑ˡⁱ_`. -/ +def liftIdxL {n : ℕ} (l : List (Fin n)) (m : ℕ) : List (Fin (n + m)) := + l.map (Fin.castAdd m) + +/-- Agda: `_↑ʳⁱ_`. -/ +def liftIdxR (n : ℕ) {m : ℕ} (l : List (Fin m)) : List (Fin (n + m)) := + l.map (Fin.natAdd n) + +/-- Agda: `_↑ˡᵉ_` (with `_↑ˡ_` on pairs inlined). -/ +def liftEdgeL {n : ℕ} (l : List (Fin n × Fin n)) (m : ℕ) : + List (Fin (n + m) × Fin (n + m)) := + l.map (fun e => (e.1.castAdd m, e.2.castAdd m)) + +/-- Agda: `_↑ʳᵉ_` (with `_↑ʳ_` on pairs inlined). -/ +def liftEdgeR (n : ℕ) {m : ℕ} (l : List (Fin m × Fin m)) : + List (Fin (n + m) × Fin (n + m)) := + l.map (fun e => (e.1.natAdd n, e.2.natAdd n)) + +/-- Agda: `_∙_` — disjoint union. -/ +def comp (g₁ g₂ : Graph) : Graph where + size := g₁.size + g₂.size + nodes := Fin.append g₁.nodes g₂.nodes + edges := liftEdgeL g₁.edges g₂.size ++ liftEdgeR g₁.size g₂.edges + inputs := liftIdxL g₁.inputs g₂.size ++ liftIdxR g₁.size g₂.inputs + outputs := liftIdxL g₁.outputs g₂.size ++ liftIdxR g₁.size g₂.outputs + +@[inherit_doc] scoped infixr:70 " ∙ " => Graph.comp + +/-- Agda: `_↦_` — sequencing: all outputs of `g₁` feed all inputs of `g₂`. -/ +def link (g₁ g₂ : Graph) : Graph where + size := g₁.size + g₂.size + nodes := Fin.append g₁.nodes g₂.nodes + edges := liftEdgeL g₁.edges g₂.size ++ liftEdgeR g₁.size g₂.edges ++ + (liftIdxL g₁.outputs g₂.size).product (liftIdxR g₁.size g₂.inputs) + inputs := liftIdxL g₁.inputs g₂.size + outputs := liftIdxR g₁.size g₂.outputs + +@[inherit_doc] scoped infixr:70 " ⤳ " => Graph.link + +/-- The entry node of a `loop` graph. -/ +def loopIn (g : Graph) : Fin (2 + g.size) := (0 : Fin 2).castAdd g.size + +/-- The exit node of a `loop` graph. -/ +def loopOut (g : Graph) : Fin (2 + g.size) := (1 : Fin 2).castAdd g.size + +/-- Agda: `loop`. -/ +def loop (g : Graph) : Graph where + size := 2 + g.size + nodes := Fin.append (fun _ : Fin 2 => []) g.nodes + edges := liftEdgeR 2 g.edges ++ + (liftIdxR 2 g.inputs).map (g.loopIn, ·) ++ + (liftIdxR 2 g.outputs).map (·, g.loopOut) ++ + [(g.loopOut, g.loopIn), (g.loopIn, g.loopOut)] + inputs := [g.loopIn] + outputs := [g.loopOut] + +@[simp] theorem loop_inputs (g : Graph) : (loop g).inputs = [g.loopIn] := rfl + +@[simp] theorem loop_outputs (g : Graph) : (loop g).outputs = [g.loopOut] := rfl + +/-- Agda: `_skipto_` (unused by `buildCfg`, ported for parity). -/ +def skipto (g₁ g₂ : Graph) : Graph where + size := g₁.size + g₂.size + nodes := Fin.append g₁.nodes g₂.nodes + edges := liftEdgeL g₁.edges g₂.size ++ liftEdgeR g₁.size g₂.edges ++ + (liftIdxL g₁.inputs g₂.size).product (liftIdxR g₁.size g₂.inputs) + inputs := liftIdxL g₁.inputs g₂.size + outputs := liftIdxR g₁.size g₂.inputs + +/-- Agda: `singleton`. -/ +def singleton (bss : List BasicStmt) : Graph where + size := 1 + nodes := fun _ => bss + edges := [] + inputs := [0] + outputs := [0] + +/-- Agda: `wrap`. -/ +def wrap (g : Graph) : Graph := + singleton [] ⤳ g ⤳ singleton [] + +end Graph + +open Graph in +/-- Agda: `buildCfg`. -/ +def buildCfg : Stmt → Graph + | .basic bs => Graph.singleton [bs] + | .andThen s₁ s₂ => buildCfg s₁ ⤳ buildCfg s₂ + | .ifElse _ s₁ s₂ => buildCfg s₁ ∙ buildCfg s₂ + | .whileLoop _ s => Graph.loop (buildCfg s) + +namespace Graph + +variable (g : Graph) + +/-- Agda: `indices` (`fins` is mathlib's `List.finRange`). -/ +def indices : List g.Index := List.finRange g.size + +/-- Agda: `indices-complete`. -/ +theorem mem_indices (idx : g.Index) : idx ∈ g.indices := + List.mem_finRange idx + +/-- Agda: `indices-Unique`. -/ +theorem nodup_indices : g.indices.Nodup := + List.nodup_finRange g.size + +/-- Agda: `predecessors`. -/ +def predecessors (idx : g.Index) : List g.Index := + g.indices.filter (fun idx' => (idx', idx) ∈ g.edges) + +/-- Agda: `edge⇒predecessor`. -/ +theorem mem_predecessors_of_edge {idx₁ idx₂ : g.Index} + (h : (idx₁, idx₂) ∈ g.edges) : idx₁ ∈ g.predecessors idx₂ := + List.mem_filter.mpr ⟨g.mem_indices idx₁, by simpa using h⟩ + +/-- Agda: `predecessor⇒edge`. -/ +theorem edge_of_mem_predecessors {idx₁ idx₂ : g.Index} + (h : idx₁ ∈ g.predecessors idx₂) : (idx₁, idx₂) ∈ g.edges := by + simpa using (List.mem_filter.mp h).2 + +end Graph + +end Spa diff --git a/lean/Spa/Language/Properties.lean b/lean/Spa/Language/Properties.lean new file mode 100644 index 0000000..c67983d --- /dev/null +++ b/lean/Spa/Language/Properties.lean @@ -0,0 +1,282 @@ +/- +Port of `Language/Properties.agda`. + +Correspondence: + ↑-≢ (and the whole "ugly" Fin-disjointness block: + idx→f∉↑ʳᵉ, idx→f∉pair, idx→f∉cart, help, helpAll) + ↦ Fin.castAdd_ne_natAdd + not_mem_edges_castAdd_link + (mathlib `List.mem_append`/`mem_map`/`mem_product` + replace the hand-rolled membership eliminations) + wrap-preds-∅ ↦ wrap_predecessors_eq_nil + wrap-input, wrap-output ↦ Graph.wrapInput/wrapOutput + wrap_inputs/wrap_outputs + Trace-∙ˡ/ʳ ↦ Trace.comp_left / Trace.comp_right + Trace-↦ˡ/ʳ ↦ Trace.link_left / Trace.link_right + Trace-loop ↦ Trace.loop + EndToEndTrace-∙ˡ/ʳ ↦ EndToEndTrace.comp_left / .comp_right + loop-edge-groups, + loop-edge-help ↦ (inlined: the four edge groups are reached through + `List.mem_append` directly) + EndToEndTrace-loop ↦ EndToEndTrace.loop + EndToEndTrace-loop² ↦ EndToEndTrace.loop_concat + EndToEndTrace-loop⁰ ↦ EndToEndTrace.loop_empty + _++_ ↦ EndToEndTrace.concat + EndToEndTrace-singleton ↦ EndToEndTrace.singleton (+ .singleton_nil) + EndToEndTrace-wrap ↦ EndToEndTrace.wrap + buildCfg-sufficient ↦ buildCfg_sufficient +-/ +import Spa.Language.Traces + +namespace Spa + +open Graph + +/-- Agda: `↑-≢`. -/ +theorem 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 + +/-! ### Trace embeddings -/ + +section Embeddings + +variable {g₁ g₂ : Graph} {ρ₁ ρ₂ : Env} + +/-- Agda: `Trace-∙ˡ`. -/ +theorem Trace.comp_left {idx₁ idx₂ : g₁.Index} + (tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) : + Trace (g₁ ∙ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by + induction tr with + | single hbs => + exact Trace.single (by rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, + Fin.append_left]) + | edge hbs he _ ih => + refine Trace.edge ?_ ?_ ih + · rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_left] + · exact List.mem_append_left _ (List.mem_map_of_mem _ he) + +/-- Agda: `Trace-∙ʳ`. -/ +theorem Trace.comp_right {idx₁ idx₂ : g₂.Index} + (tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) : + Trace (g₁ ∙ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by + induction tr with + | single hbs => + exact Trace.single (by rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, + Fin.append_right]) + | edge hbs he _ ih => + refine Trace.edge ?_ ?_ ih + · rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_right] + · exact List.mem_append_right _ (List.mem_map_of_mem _ he) + +/-- Agda: `Trace-↦ˡ`. -/ +theorem Trace.link_left {idx₁ idx₂ : g₁.Index} + (tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) : + Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by + induction tr with + | single hbs => + exact Trace.single (by rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, + Fin.append_left]) + | edge hbs he _ ih => + refine Trace.edge ?_ ?_ ih + · rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_left] + · exact List.mem_append_left _ (List.mem_append_left _ (List.mem_map_of_mem _ he)) + +/-- Agda: `Trace-↦ʳ`. -/ +theorem Trace.link_right {idx₁ idx₂ : g₂.Index} + (tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) : + Trace (g₁ ⤳ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by + induction tr with + | single hbs => + exact Trace.single (by rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, + Fin.append_right]) + | edge hbs he _ ih => + refine Trace.edge ?_ ?_ ih + · rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_right] + · exact List.mem_append_left _ + (List.mem_append_right _ (List.mem_map_of_mem _ he)) + +/-- Agda: `EndToEndTrace-∙ˡ`. -/ +theorem EndToEndTrace.comp_left (etr : EndToEndTrace g₁ ρ₁ ρ₂) : + EndToEndTrace (g₁ ∙ g₂) ρ₁ ρ₂ := by + obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr + exact ⟨i₁.castAdd g₂.size, List.mem_append_left _ (List.mem_map_of_mem _ h₁), + i₂.castAdd g₂.size, List.mem_append_left _ (List.mem_map_of_mem _ h₂), + tr.comp_left⟩ + +/-- Agda: `EndToEndTrace-∙ʳ`. -/ +theorem EndToEndTrace.comp_right (etr : EndToEndTrace g₂ ρ₁ ρ₂) : + EndToEndTrace (g₁ ∙ g₂) ρ₁ ρ₂ := by + obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr + exact ⟨i₁.natAdd g₁.size, List.mem_append_right _ (List.mem_map_of_mem _ h₁), + i₂.natAdd g₁.size, List.mem_append_right _ (List.mem_map_of_mem _ h₂), + tr.comp_right⟩ + +/-- Agda: `_++_` — sequencing end-to-end traces over `⤳`. -/ +theorem EndToEndTrace.concat {ρ₃ : Env} (etr₁ : EndToEndTrace g₁ ρ₁ ρ₂) + (etr₂ : EndToEndTrace g₂ ρ₂ ρ₃) : EndToEndTrace (g₁ ⤳ g₂) ρ₁ ρ₃ := by + obtain ⟨i₁, h₁, i₂, h₂, tr₁⟩ := etr₁ + obtain ⟨j₁, k₁, j₂, k₂, tr₂⟩ := etr₂ + refine ⟨i₁.castAdd g₂.size, List.mem_map_of_mem _ h₁, + j₂.natAdd g₁.size, List.mem_map_of_mem _ k₂, + Trace.concat tr₁.link_left ?_ tr₂.link_right⟩ + exact List.mem_append_right _ + (List.mem_product.mpr ⟨List.mem_map_of_mem _ h₂, List.mem_map_of_mem _ k₁⟩) + +end Embeddings + +/-! ### Loops -/ + +section Loop + +variable {g : Graph} {ρ₁ ρ₂ ρ₃ : Env} + +/-- Agda: `Trace-loop`. -/ +theorem Trace.loop {idx₁ idx₂ : g.Index} (tr : Trace g idx₁ idx₂ ρ₁ ρ₂) : + Trace (Graph.loop g) (idx₁.natAdd 2) (idx₂.natAdd 2) ρ₁ ρ₂ := by + induction tr with + | single hbs => + exact Trace.single (by + rwa [show (Graph.loop g).nodes = Fin.append (fun _ : Fin 2 => []) g.nodes from rfl, + Fin.append_right]) + | edge hbs he _ ih => + refine Trace.edge ?_ ?_ ih + · rwa [show (Graph.loop g).nodes = Fin.append (fun _ : Fin 2 => []) g.nodes from rfl, + Fin.append_right] + · exact List.mem_append_left _ (List.mem_append_left _ + (List.mem_append_left _ (List.mem_map_of_mem _ he))) + +private theorem loop_nodes_at_in : + (Graph.loop g).nodes g.loopIn = [] := + Fin.append_left (fun _ : Fin 2 => []) g.nodes 0 + +private theorem loop_nodes_at_out : + (Graph.loop g).nodes g.loopOut = [] := + Fin.append_left (fun _ : Fin 2 => []) g.nodes 1 + +/-- Agda: `EndToEndTrace-loop`. -/ +theorem EndToEndTrace.loop (etr : EndToEndTrace g ρ₁ ρ₂) : + EndToEndTrace (Graph.loop g) ρ₁ ρ₂ := by + obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr + -- the edge in → (2 ↑ʳ i₁), reached through the second edge group + have hin : (g.loopIn, i₁.natAdd 2) ∈ (Graph.loop g).edges := by + refine List.mem_append_left _ (List.mem_append_left _ (List.mem_append_right _ ?_)) + exact List.mem_map_of_mem _ (List.mem_map_of_mem _ h₁) + -- the edge (2 ↑ʳ i₂) → out, reached through the third edge group + have hout : (i₂.natAdd 2, g.loopOut) ∈ (Graph.loop g).edges := by + refine List.mem_append_left _ (List.mem_append_right _ ?_) + exact List.mem_map_of_mem _ (List.mem_map_of_mem _ h₂) + refine ⟨g.loopIn, List.mem_singleton_self _, g.loopOut, List.mem_singleton_self _, ?_⟩ + exact Trace.concat (Trace.single (loop_nodes_at_in ▸ EvalBasicStmts.nil)) hin + (Trace.concat tr.loop hout (Trace.single (loop_nodes_at_out ▸ EvalBasicStmts.nil))) + +private theorem loop_edge_out_in : + ((g.loopOut, g.loopIn) : (Graph.loop g).Edge) ∈ (Graph.loop g).edges := by + refine List.mem_append_right _ ?_ + exact List.mem_cons_self _ _ + +/-- Agda: `EndToEndTrace-loop²`. -/ +theorem EndToEndTrace.loop_concat (etr₁ : EndToEndTrace (Graph.loop g) ρ₁ ρ₂) + (etr₂ : EndToEndTrace (Graph.loop g) ρ₂ ρ₃) : + EndToEndTrace (Graph.loop g) ρ₁ ρ₃ := by + obtain ⟨i₁, h₁, i₂, h₂, tr₁⟩ := etr₁ + obtain ⟨j₁, k₁, j₂, k₂, tr₂⟩ := etr₂ + simp only [Graph.loop_inputs, Graph.loop_outputs, List.mem_singleton] at h₁ h₂ k₁ k₂ + subst h₁; subst h₂; subst k₁; subst k₂ + exact ⟨g.loopIn, List.mem_singleton_self _, g.loopOut, List.mem_singleton_self _, + Trace.concat tr₁ loop_edge_out_in tr₂⟩ + +/-- Agda: `EndToEndTrace-loop⁰`. -/ +theorem EndToEndTrace.loop_empty {ρ : Env} : EndToEndTrace (Graph.loop g) ρ ρ := by + have hedge : ((g.loopIn, g.loopOut) : (Graph.loop g).Edge) ∈ (Graph.loop g).edges := + List.mem_append_right _ (List.mem_cons_of_mem _ (List.mem_cons_self _ _)) + exact ⟨g.loopIn, List.mem_singleton_self _, g.loopOut, List.mem_singleton_self _, + Trace.concat (Trace.single (loop_nodes_at_in ▸ EvalBasicStmts.nil)) hedge + (Trace.single (loop_nodes_at_out ▸ EvalBasicStmts.nil))⟩ + +end Loop + +/-! ### Singletons, wrap, and the main result -/ + +/-- Agda: `EndToEndTrace-singleton`. -/ +theorem EndToEndTrace.singleton {bss : List BasicStmt} {ρ₁ ρ₂ : Env} + (h : EvalBasicStmts ρ₁ bss ρ₂) : EndToEndTrace (Graph.singleton bss) ρ₁ ρ₂ := + ⟨(0 : Fin 1), List.mem_singleton_self _, (0 : Fin 1), List.mem_singleton_self _, + Trace.single h⟩ + +/-- Agda: `EndToEndTrace-singleton[]`. -/ +theorem EndToEndTrace.singleton_nil (ρ : Env) : + EndToEndTrace (Graph.singleton []) ρ ρ := + EndToEndTrace.singleton EvalBasicStmts.nil + +/-- Agda: `EndToEndTrace-wrap`. -/ +theorem EndToEndTrace.wrap {g : Graph} {ρ₁ ρ₂ : Env} + (etr : EndToEndTrace g ρ₁ ρ₂) : EndToEndTrace (Graph.wrap g) ρ₁ ρ₂ := + (EndToEndTrace.singleton_nil ρ₁).concat (etr.concat (EndToEndTrace.singleton_nil ρ₂)) + +/-- Agda: `buildCfg-sufficient` — every terminating execution is witnessed by +an end-to-end trace through the control-flow graph. -/ +theorem buildCfg_sufficient {s : Stmt} {ρ₁ ρ₂ : Env} + (h : EvalStmt ρ₁ s ρ₂) : EndToEndTrace (buildCfg s) ρ₁ ρ₂ := by + induction h with + | basic ρ₁ ρ₂ bs hbs => + exact EndToEndTrace.singleton (EvalBasicStmts.cons hbs EvalBasicStmts.nil) + | andThen ρ₁ ρ₂ ρ₃ s₁ s₂ _ _ ih₁ ih₂ => + exact ih₁.concat ih₂ + | ifTrue ρ₁ ρ₂ e z s₁ s₂ _ _ _ ih => + exact ih.comp_left + | ifFalse ρ₁ ρ₂ e s₁ s₂ _ _ ih => + exact ih.comp_right + | whileTrue ρ₁ ρ₂ ρ₃ e z s _ _ _ _ ih₁ ih₂ => + exact (ih₁.loop).loop_concat ih₂ + | whileFalse ρ e s _ => + exact EndToEndTrace.loop_empty + +/-! ### The wrapped graph's entry has no predecessors (Agda's "ugly" block) -/ + +/-- The input of `wrap g` (Agda: `wrap-input`). -/ +def Graph.wrapInput (g : Graph) : (Graph.wrap g).Index := + (0 : Fin 1).castAdd ((g ⤳ Graph.singleton []).size) + +/-- The output of `wrap g` (Agda: `wrap-output`). -/ +def Graph.wrapOutput (g : Graph) : (Graph.wrap g).Index := + Fin.natAdd 1 ((Fin.natAdd g.size (0 : Fin 1))) + +theorem Graph.wrap_inputs (g : Graph) : + (Graph.wrap g).inputs = [g.wrapInput] := rfl + +theorem Graph.wrap_outputs (g : Graph) : + (Graph.wrap g).outputs = [g.wrapOutput] := rfl + +/-- Agda: `help`/`helpAll` — no edge of `singleton [] ⤳ g₂` ends at a +`castAdd`-injected node (all edge targets are `natAdd`s). -/ +private theorem not_mem_edges_castAdd_link {g₂ : Graph} (i : Fin 1) + (idx : (Graph.singleton [] ⤳ g₂).Index) : + ((idx, i.castAdd g₂.size) : (Graph.singleton [] ⤳ g₂).Edge) + ∉ (Graph.singleton [] ⤳ 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, Graph.liftEdgeL] 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 + +/-- Agda: `wrap-preds-∅` — the entry node of a wrapped graph has no +incoming edges. -/ +theorem 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 [Graph.predecessors, List.filter_eq_nil_iff] + intro idx' _ + simpa using not_mem_edges_castAdd_link (g₂ := g ⤳ Graph.singleton []) 0 idx' + +end Spa diff --git a/lean/Spa/Language/Semantics.lean b/lean/Spa/Language/Semantics.lean new file mode 100644 index 0000000..b9ccf92 --- /dev/null +++ b/lean/Spa/Language/Semantics.lean @@ -0,0 +1,90 @@ +/- +Port of `Language/Semantics.agda`. + +Correspondence: + Value (↑ᶻ) ↦ Value.int + Env ↦ Env (= List (String × Value)) + _∈_ (env lookup) ↦ Env.Mem + _,_⇒ᵉ_ ↦ EvalExpr + _,_⇒ᵇ_ ↦ EvalBasicStmt + _,_⇒ᵇˢ_ ↦ EvalBasicStmts + _,_⇒ˢ_ ↦ EvalStmt + LatticeInterpretation: + ⟦_⟧ ↦ interp + ⟦⟧-respects-≈ ↦ (trivial with `=`; field dropped) + ⟦⟧-⊔-∨ ↦ interp_sup + ⟦⟧-⊓-∧ ↦ interp_inf + (the `Utils` combinators `_⇒_`, `_∨_`, `_∧_` are inlined as plain logic) +-/ +import Spa.Language.Base +import Spa.Lattice + +namespace Spa + +inductive Value where + | int (z : ℤ) + deriving DecidableEq + +def Env : Type := List (String × Value) + +/-- Agda: `_∈_` on environments — lookup respecting shadowing. -/ +inductive Env.Mem : String × Value → Env → Prop + | here (s : String) (v : Value) (ρ : Env) : Env.Mem (s, v) ((s, v) :: ρ) + | there (s s' : String) (v v' : Value) (ρ : Env) : + ¬(s = s') → Env.Mem (s, v) ρ → Env.Mem (s, v) ((s', v') :: ρ) + +/-- Agda: `_,_⇒ᵉ_`. -/ +inductive EvalExpr : Env → Expr → Value → Prop + | num (ρ : Env) (n : ℕ) : EvalExpr ρ (.num n) (.int n) + | var (ρ : Env) (x : String) (v : Value) : + Env.Mem (x, v) ρ → EvalExpr ρ (.var x) v + | add (ρ : Env) (e₁ e₂ : Expr) (z₁ z₂ : ℤ) : + EvalExpr ρ e₁ (.int z₁) → EvalExpr ρ e₂ (.int z₂) → + EvalExpr ρ (.add e₁ e₂) (.int (z₁ + z₂)) + | sub (ρ : Env) (e₁ e₂ : Expr) (z₁ z₂ : ℤ) : + EvalExpr ρ e₁ (.int z₁) → EvalExpr ρ e₂ (.int z₂) → + EvalExpr ρ (.sub e₁ e₂) (.int (z₁ - z₂)) + +/-- Agda: `_,_⇒ᵇ_`. -/ +inductive EvalBasicStmt : Env → BasicStmt → Env → Prop + | noop (ρ : Env) : EvalBasicStmt ρ .noop ρ + | assign (ρ : Env) (x : String) (e : Expr) (v : Value) : + EvalExpr ρ e v → EvalBasicStmt ρ (.assign x e) ((x, v) :: ρ) + +/-- Agda: `_,_⇒ᵇˢ_`. -/ +inductive EvalBasicStmts : Env → List BasicStmt → Env → Prop + | nil {ρ : Env} : EvalBasicStmts ρ [] ρ + | cons {ρ₁ ρ₂ ρ₃ : Env} {bs : BasicStmt} {bss : List BasicStmt} : + EvalBasicStmt ρ₁ bs ρ₂ → EvalBasicStmts ρ₂ bss ρ₃ → + EvalBasicStmts ρ₁ (bs :: bss) ρ₃ + +/-- Agda: `_,_⇒ˢ_`. -/ +inductive EvalStmt : Env → Stmt → Env → Prop + | basic (ρ₁ ρ₂ : Env) (bs : BasicStmt) : + EvalBasicStmt ρ₁ bs ρ₂ → EvalStmt ρ₁ (.basic bs) ρ₂ + | andThen (ρ₁ ρ₂ ρ₃ : Env) (s₁ s₂ : Stmt) : + EvalStmt ρ₁ s₁ ρ₂ → EvalStmt ρ₂ s₂ ρ₃ → + EvalStmt ρ₁ (.andThen s₁ s₂) ρ₃ + | ifTrue (ρ₁ ρ₂ : Env) (e : Expr) (z : ℤ) (s₁ s₂ : Stmt) : + EvalExpr ρ₁ e (.int z) → ¬(z = 0) → EvalStmt ρ₁ s₁ ρ₂ → + EvalStmt ρ₁ (.ifElse e s₁ s₂) ρ₂ + | ifFalse (ρ₁ ρ₂ : Env) (e : Expr) (s₁ s₂ : Stmt) : + EvalExpr ρ₁ e (.int 0) → EvalStmt ρ₁ s₂ ρ₂ → + EvalStmt ρ₁ (.ifElse e s₁ s₂) ρ₂ + | whileTrue (ρ₁ ρ₂ ρ₃ : Env) (e : Expr) (z : ℤ) (s : Stmt) : + EvalExpr ρ₁ e (.int z) → ¬(z = 0) → EvalStmt ρ₁ s ρ₂ → + EvalStmt ρ₂ (.whileLoop e s) ρ₃ → + EvalStmt ρ₁ (.whileLoop e s) ρ₃ + | whileFalse (ρ : Env) (e : Expr) (s : Stmt) : + EvalExpr ρ e (.int 0) → + EvalStmt ρ (.whileLoop e s) ρ + +/-- Agda: `LatticeInterpretation`. -/ +structure LatticeInterpretation (L : Type*) [Lattice L] where + interp : L → Value → Prop + interp_sup : ∀ {l₁ l₂ : L} (v : Value), + interp l₁ v ∨ interp l₂ v → interp (l₁ ⊔ l₂) v + interp_inf : ∀ {l₁ l₂ : L} (v : Value), + interp l₁ v ∧ interp l₂ v → interp (l₁ ⊓ l₂) v + +end Spa diff --git a/lean/Spa/Language/Traces.lean b/lean/Spa/Language/Traces.lean new file mode 100644 index 0000000..92019d1 --- /dev/null +++ b/lean/Spa/Language/Traces.lean @@ -0,0 +1,38 @@ +/- +Port of `Language/Traces.agda`. + +Correspondence: + Trace ↦ Trace (a `Prop`-valued inductive; only used in proofs) + _++⟨_⟩_ ↦ Trace.concat + EndToEndTrace ↦ EndToEndTrace (a `Prop`-valued structure, like `∃`; its + fields are accessed by destructuring inside proofs) +-/ +import Spa.Language.Semantics +import Spa.Language.Graphs + +namespace Spa + +/-- Agda: `Trace`. -/ +inductive Trace (g : Graph) : g.Index → g.Index → Env → Env → Prop + | single {ρ₁ ρ₂ : Env} {idx : g.Index} : + EvalBasicStmts ρ₁ (g.nodes idx) ρ₂ → Trace g idx idx ρ₁ ρ₂ + | edge {ρ₁ ρ₂ ρ₃ : Env} {idx₁ idx₂ idx₃ : g.Index} : + EvalBasicStmts ρ₁ (g.nodes idx₁) ρ₂ → (idx₁, idx₂) ∈ g.edges → + Trace g idx₂ idx₃ ρ₂ ρ₃ → Trace g idx₁ idx₃ ρ₁ ρ₃ + +/-- Agda: `_++⟨_⟩_`. -/ +theorem Trace.concat {g : Graph} {idx₁ idx₂ idx₃ idx₄ : g.Index} + {ρ₁ ρ₂ ρ₃ : Env} (tr₁ : Trace g idx₁ idx₂ ρ₁ ρ₂) + (he : (idx₂, idx₃) ∈ g.edges) (tr₂ : Trace g idx₃ idx₄ ρ₂ ρ₃) : + Trace g idx₁ idx₄ ρ₁ ρ₃ := by + induction tr₁ with + | single hbs => exact Trace.edge hbs he tr₂ + | edge hbs he' _ ih => exact Trace.edge hbs he' (ih he tr₂) + +/-- Agda: `EndToEndTrace` (an existential package, destructured in proofs). -/ +inductive EndToEndTrace (g : Graph) (ρ₁ ρ₂ : Env) : Prop + | intro (idx₁ : g.Index) (idx₁_mem : idx₁ ∈ g.inputs) + (idx₂ : g.Index) (idx₂_mem : idx₂ ∈ g.outputs) + (trace : Trace g idx₁ idx₂ ρ₁ ρ₂) : EndToEndTrace g ρ₁ ρ₂ + +end Spa