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 <noreply@anthropic.com>

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
 

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

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

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

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

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