From 93f913a6991b970728fb6e3bf38e149e10b4444e Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Wed, 24 Jun 2026 13:54:37 -0500 Subject: [PATCH] Clean up namespaces in the analysis framework - Wrap the forward-analysis framework in a Spa.Forward namespace so its generic names (analyze, result, joinAll, variablesAt, ...) no longer sit flat in Spa, matching the ConstAnalysis/SignAnalysis convention. - Merge the split Graph namespace in Graphs.lean by relocating buildCfg. - Use nested namespace Spa / Fixedpoint instead of Spa.Fixedpoint. Co-Authored-By: Claude Opus 4.8 --- lean/Spa/Analysis/Constant.lean | 4 +++- lean/Spa/Analysis/Forward.lean | 4 ++++ lean/Spa/Analysis/Forward/Adapters.lean | 4 ++++ lean/Spa/Analysis/Forward/Evaluation.lean | 4 ++++ lean/Spa/Analysis/Forward/Lattices.lean | 4 ++++ lean/Spa/Analysis/Sign.lean | 4 +++- lean/Spa/Fixedpoint.lean | 8 ++++++-- lean/Spa/Language/Graphs.lean | 18 +++++++----------- 8 files changed, 35 insertions(+), 15 deletions(-) diff --git a/lean/Spa/Analysis/Constant.lean b/lean/Spa/Analysis/Constant.lean index 235cbbc..9208753 100644 --- a/lean/Spa/Analysis/Constant.lean +++ b/lean/Spa/Analysis/Constant.lean @@ -5,6 +5,8 @@ import Spa.Showable namespace Spa +open Forward + abbrev ConstLattice : Type := AboveBelow ℤ namespace ConstAnalysis @@ -157,7 +159,7 @@ instance eval_valid : ValidExprEvaluator ConstLattice prog := by theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : ⟦ variablesAt prog.finalState (result ConstLattice prog) ⟧ ρ := - Spa.analyze_correct ConstLattice prog hrun + Forward.analyze_correct ConstLattice prog hrun end ConstAnalysis diff --git a/lean/Spa/Analysis/Forward.lean b/lean/Spa/Analysis/Forward.lean index 90e9025..b63d948 100644 --- a/lean/Spa/Analysis/Forward.lean +++ b/lean/Spa/Analysis/Forward.lean @@ -5,6 +5,8 @@ import Spa.Fixedpoint namespace Spa +namespace Forward + variable {L : Type} [Lattice L] {prog : Program} [E : StmtEvaluator L prog] def updateVariablesForState (s : prog.State) (sv : StateVariables L prog) : @@ -116,4 +118,6 @@ theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : ⟦ variablesAt prog.finalState (result L prog) ⟧ ρ := walkTrace interp_joinForKey_initialState (prog.trace hrun) +end Forward + end Spa diff --git a/lean/Spa/Analysis/Forward/Adapters.lean b/lean/Spa/Analysis/Forward/Adapters.lean index 07225d6..583daf3 100644 --- a/lean/Spa/Analysis/Forward/Adapters.lean +++ b/lean/Spa/Analysis/Forward/Adapters.lean @@ -2,6 +2,8 @@ import Spa.Analysis.Forward.Evaluation namespace Spa +namespace Forward + variable {L : Type} [Lattice L] {prog : Program} [E : ExprEvaluator L prog] def updateVariablesFromExpression (k : String) (e : Expr) @@ -51,4 +53,6 @@ instance ExprEvaluator.toStmtEvaluator_valid [LatticeInterpretation L] (fun hmem => hne (List.mem_singleton.mp hmem)) hk'l₀ exact hvs _ _ hk'l' _ hmem' +end Forward + end Spa diff --git a/lean/Spa/Analysis/Forward/Evaluation.lean b/lean/Spa/Analysis/Forward/Evaluation.lean index 27d8065..9f30b9f 100644 --- a/lean/Spa/Analysis/Forward/Evaluation.lean +++ b/lean/Spa/Analysis/Forward/Evaluation.lean @@ -2,6 +2,8 @@ import Spa.Analysis.Forward.Lattices namespace Spa +namespace Forward + variable (L : Type) [Lattice L] (prog : Program) class StmtEvaluator where @@ -23,4 +25,6 @@ class ValidStmtEvaluator [E : StmtEvaluator L prog] [LatticeInterpretation L] : {bs : BasicStmt}, EvalBasicStmt ρ₁ bs ρ₂ → ⟦ vs ⟧ ρ₁ → ⟦ E.eval s bs vs ⟧ ρ₂ +end Forward + end Spa diff --git a/lean/Spa/Analysis/Forward/Lattices.lean b/lean/Spa/Analysis/Forward/Lattices.lean index f10be81..c1fa27f 100644 --- a/lean/Spa/Analysis/Forward/Lattices.lean +++ b/lean/Spa/Analysis/Forward/Lattices.lean @@ -4,6 +4,8 @@ import Spa.Interp namespace Spa +namespace Forward + variable (L : Type) [Lattice L] (prog : Program) abbrev VariableValues : Type := FiniteMap String L prog.vars @@ -96,4 +98,6 @@ theorem interp_foldr {vs : VariableValues L prog} · exact interp_sup (Or.inl hvs) · exact interp_sup (Or.inr (ih hmem')) +end Forward + end Spa diff --git a/lean/Spa/Analysis/Sign.lean b/lean/Spa/Analysis/Sign.lean index 4d01a90..d5079ef 100644 --- a/lean/Spa/Analysis/Sign.lean +++ b/lean/Spa/Analysis/Sign.lean @@ -5,6 +5,8 @@ import Spa.Showable namespace Spa +open Forward + inductive Sign where | plus | minus @@ -215,7 +217,7 @@ instance eval_valid : ValidExprEvaluator SignLattice prog := by theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : ⟦ variablesAt prog.finalState (result SignLattice prog) ⟧ ρ := - Spa.analyze_correct SignLattice prog hrun + Forward.analyze_correct SignLattice prog hrun end SignAnalysis diff --git a/lean/Spa/Fixedpoint.lean b/lean/Spa/Fixedpoint.lean index 975f927..f0ee408 100644 --- a/lean/Spa/Fixedpoint.lean +++ b/lean/Spa/Fixedpoint.lean @@ -1,6 +1,8 @@ import Spa.Lattice -namespace Spa.Fixedpoint +namespace Spa + +namespace Fixedpoint open FiniteHeightLattice (height) @@ -49,4 +51,6 @@ theorem aFix_le (f : α → α) (hf : Monotone f) {a : α} (ha : a = f a) : aFix f hf ≤ a := doStep_le f hf ha _ _ _ _ (by simpa using FiniteHeightLattice.bot_le α a) -end Spa.Fixedpoint +end Fixedpoint + +end Spa diff --git a/lean/Spa/Language/Graphs.lean b/lean/Spa/Language/Graphs.lean index 727ace0..ca1109e 100644 --- a/lean/Spa/Language/Graphs.lean +++ b/lean/Spa/Language/Graphs.lean @@ -89,17 +89,6 @@ def singleton (bss : List BasicStmt) : Graph where def wrap (g : Graph) : Graph := singleton [] ⤳ g ⤳ singleton [] -end Graph - -open Graph in -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) def indices : List g.Index := List.finRange g.size @@ -123,4 +112,11 @@ theorem edge_of_mem_predecessors {idx₁ idx₂ : g.Index} end Graph +open Graph in +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) + end Spa