Migrate most of the codebase (sans Reaching.lean / LICM left) to projections

2026-07-01 22:56:29 -05:00
parent 10b8fa97ca
commit 0e6976f9b4
7 changed files with 139 additions and 136 deletions
--- a/lean/Spa/Analysis/Constant.lean
+++ b/lean/Spa/Analysis/Constant.lean
@@ -134,14 +134,14 @@ instance eval_valid : ValidExprEvaluator ConstLattice prog := by
    exact minus_valid h₁ h₂

 theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
-    ⟦ variablesAt prog.finalState (result ConstLattice prog) ⟧ ρ () :=
+    ⟦ variablesAt prog.finalState (result ConstLattice prog) ⟧ ρ :=
  Forward.analyze_correct ConstLattice prog hrun

 theorem analyze_correct_at {ρf : Env} (hrun : EvalStmt [] prog.rootStmt ρf)
-    {s : prog.State} {ρin ρout : Env} {stin stout : PUnit}
-    (hr : Reaches (L := ConstLattice) (prog.trace hrun) PUnit.unit s ρin ρout stin stout) :
-    ⟦ joinForKey s (result ConstLattice prog) ⟧ ρin stin
-      ∧ ⟦ variablesAt s (result ConstLattice prog) ⟧ ρout stout :=
+    {s : prog.State} {ρin ρout : Env}
+    (hr : Reaches (prog.trace hrun) s ρin ρout) :
+    ⟦ joinForKey s (result ConstLattice prog) ⟧ ρin
+      ∧ ⟦ variablesAt s (result ConstLattice prog) ⟧ ρout :=
  Forward.analyze_correct_at ConstLattice prog hrun hr

 end ConstAnalysis
--- a/lean/Spa/Analysis/Forward.lean
+++ b/lean/Spa/Analysis/Forward.lean
@@ -55,70 +55,38 @@ lemma joinForKey_initialState :

 class ValidStateEvaluator (L : Type) [FiniteHeightLattice L] (prog : Program)
    [E : StmtEvaluator L prog] [S : StateInterpretation L prog] where
-  step : (s : prog.State) → {ρ₁ ρ₂ : Env} → EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂ → S.St ρ₁ → S.St ρ₂
-  valid : ∀ (s : prog.State) {ρ₁ ρ₂ : Env}
-    {vs : VariableValues L prog} {st : S.St ρ₁},
-    (hbs : EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂) → ⟦ vs ⟧ ρ₁ st →
-    ⟦ E.eval s vs ⟧ ρ₂ (step s hbs st)
-  botV_init : ⟦ botV L prog ⟧ [] S.init
+  valid : ∀ (s₁ s₂ : prog.State) {ρ₁ ρ₂ ρ₃: Env}
+    {vs : VariableValues L prog},
+    (tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂) →
+    (hbs : EvalBasicStmtOpt ρ₂ (prog.cfg.nodes s₂) ρ₃) → ⟦ vs ⟧ (S.Pre tr) →
+    ⟦ E.eval s₂ vs ⟧ (S.Post (tr ++ hbs))
+  botV_init : ⟦ botV L prog ⟧ (S.Pre (Traceₗ.single prog.cfg prog.initialState []))

 instance [LatticeInterpretation L] [ValidStmtEvaluator L prog] :
    ValidStateEvaluator L prog where
-  step := by intro _ _ _ _ _; exact PUnit.unit
-  valid := by intro _ _ _ _ _ hbs hvs; exact ValidStmtEvaluator.valid hbs hvs
+  valid := by intro _ _ _ _ _ _ tr hbs hvs; exact ValidStmtEvaluator.valid hbs hvs
  botV_init := by intro k l _ v hmem; cases hmem

 section
 variable [S : StateInterpretation L prog] [V : ValidStateEvaluator L prog]

-noncomputable def stepNode (s : prog.State) {ρ₁ ρ₂ : Env}
-    (h : EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂) (st : S.St ρ₁) : S.St ρ₂ :=
-  V.step s h st
-
-noncomputable def stepTraceState :
-    {s₁ s₂ : prog.State} → {ρ₁ ρ₂ : Env} →
-    Trace prog.cfg s₁ s₂ ρ₁ ρ₂ → S.St ρ₁ → S.St ρ₂
-  | s₁, _, _, _, .single hnode, st => stepNode s₁ hnode st
-  | s₁, _, _, _, .edge hnode _ subtr, st =>
-      stepTraceState subtr (stepNode s₁ hnode st)
-
-/-- `Reaches tr st₁ s ρin ρout stin stout` witnesses that, when the trace `tr`
-    (starting at state `st₁`) is executed, node `s` is visited at some point: `ρin`
-    and `ρout` are the concrete environments just before and after `s`'s basic block
-    runs, and `stin`/`stout` are the corresponding abstract execution states. A node
-    inside a loop is reached once per iteration, each with its own environments. -/
-inductive Reaches : {s₁ s₂ : prog.State} → {ρ₁ ρ₂ : Env} →
-    Trace prog.cfg s₁ s₂ ρ₁ ρ₂ → S.St ρ₁ →
-    (s : prog.State) → (ρin ρout : Env) → S.St ρin → S.St ρout → Prop
-  | single_here {s₁ : prog.State} {ρ₁ ρ₂ : Env} {st₁ : S.St ρ₁}
-      (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂) :
-      Reaches (.single hnode) st₁ s₁ ρ₁ ρ₂ st₁ (stepNode s₁ hnode st₁)
-  | edge_here {s₁ s₂ s₃ : prog.State} {ρ₁ ρ₂ ρ₃ : Env} {st₁ : S.St ρ₁}
-      (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂)
-      (hedge : (s₁, s₂) ∈ prog.cfg.edges) (rest : Trace prog.cfg s₂ s₃ ρ₂ ρ₃) :
-      Reaches (.edge hnode hedge rest) st₁ s₁ ρ₁ ρ₂ st₁ (stepNode s₁ hnode st₁)
-  | edge_there {s₁ s₂ s₃ : prog.State} {ρ₁ ρ₂ ρ₃ : Env} {st₁ : S.St ρ₁}
-      (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂)
-      (hedge : (s₁, s₂) ∈ prog.cfg.edges) (rest : Trace prog.cfg s₂ s₃ ρ₂ ρ₃)
-      {s : prog.State} {ρin ρout : Env} {stin : S.St ρin} {stout : S.St ρout} :
-      Reaches rest (stepNode s₁ hnode st₁) s ρin ρout stin stout →
-      Reaches (.edge hnode hedge rest) st₁ s ρin ρout stin stout
-
 omit [DecidableEq L] in
-lemma updateAll_matches {s : prog.State} {sv : StateVariables L prog}
-    {ρ₁ ρ₂ : Env} {st : S.St ρ₁}
-    (hnode : EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂)
-    (hvs : ⟦ variablesAt s sv ⟧ ρ₁ st) :
-    ⟦ variablesAt s (updateAll sv) ⟧ ρ₂ (stepNode s hnode st) := by
+lemma updateAll_matches {s₁ s₂ : prog.State} {sv : StateVariables L prog}
+    {ρ₁ ρ₂ ρ₃ : Env}
+    (tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂)
+    (hnode : EvalBasicStmtOpt ρ₂ (prog.code s₂) ρ₃)
+    (hvs : ⟦ variablesAt s₂ sv ⟧ (S.Pre tr)) :
+    ⟦ variablesAt s₂ (updateAll sv) ⟧ (S.Post (tr ++ hnode)) := by
  rw [variablesAt_updateAll]
-  exact V.valid s hnode hvs
+  exact V.valid s₁ s₂ tr hnode hvs

-lemma stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env} {st : S.St ρ₁}
-    (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁ st)
-    (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂) :
-    ⟦ variablesAt s₁ (result L prog) ⟧ ρ₂ (stepNode s₁ hnode st) := by
+lemma stepTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
+    (tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂)
+    (hjoin : ⟦ joinForKey s₂ (result L prog) ⟧ (S.Pre tr))
+    (hnode : EvalBasicStmtOpt ρ₂ (prog.code s₂) ρ₃) :
+    ⟦ variablesAt s₂ (result L prog) ⟧ (S.Post (tr ++ hnode)) := by
  rw [result_eq L prog]
-  refine updateAll_matches hnode ?_
+  refine updateAll_matches tr hnode ?_
  rw [variablesAt_joinAll]
  exact hjoin

@@ -127,49 +95,41 @@ lemma stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env} {st : S.St ρ₁}
    way it over-approximates both the environment entering that node (via `joinForKey`)
    and the environment leaving it (via `variablesAt`). The intermediate `variablesAt`
    evidence used to be computed and discarded inside `walkTrace`; here it is returned. -/
-lemma walkTrace_reaches {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} {st₁ : S.St ρ₁}
-    {s : prog.State} {ρin ρout : Env} {stin : S.St ρin} {stout : S.St ρout}
-    {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂}
-    (hr : Reaches tr st₁ s ρin ρout stin stout)
-    (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁ st₁) :
-    ⟦ joinForKey s (result L prog) ⟧ ρin stin
-      ∧ ⟦ variablesAt s (result L prog) ⟧ ρout stout := by
+lemma walkTrace_reaches {s₁ s₂ s₃: prog.State} {ρ₁ ρ₂ ρ₃: Env}
+    {s : prog.State} {ρin ρout : Env}
+    {tr : Trace prog.cfg s₂ s₃ ρ₂ ρ₃}
+    (hr : Reaches tr s ρin ρout)
+    (trₗ : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂)
+    (hjoin : ⟦ joinForKey s₂ (result L prog) ⟧ (S.Pre trₗ)) :
+    ⟦ joinForKey s (result L prog) ⟧ (S.Pre (trₗ ++ hr.pre))
+      ∧ ⟦ variablesAt s (result L prog) ⟧ (S.Post (trₗ ++ hr.post)) := by
  induction hr with
-  | single_here hnode => exact ⟨hjoin, stepTrace hjoin hnode⟩
-  | edge_here hnode hedge rest => exact ⟨hjoin, stepTrace hjoin hnode⟩
+  | single_here hnode =>
+    simp [Reaches.pre, Reaches.post]
+    refine ⟨?_, ?_⟩ <;> try simpa [HAppend.hAppend]
+    exact stepTrace trₗ hjoin hnode
+  | edge_here hnode hedge rest =>
+    simp [Reaches.pre, Reaches.post]
+    refine ⟨?_, ?_⟩ <;> try simpa [HAppend.hAppend]
+    exact stepTrace trₗ hjoin hnode
  | edge_there hnode hedge rest hr' ih =>
-    have hstep := stepTrace hjoin hnode
+    have hstep := stepTrace trₗ hjoin hnode
    have hmem := FiniteMap.mem_valuesAt prog.states_nodup
      (prog.mem_incoming_of_edge hedge) (variablesAt_mem _ (result L prog))
-    exact ih (interp_foldr hstep hmem)
+    simpa [Reaches.pre, Reaches.post, HAppend.hAppend] using
+      ih ((trₗ ++ hnode).addEdge hedge)
+        (interp_foldr (S.post_pre (trₗ ++ hnode) hedge hstep) hmem)

 omit [DecidableEq L] in
 /-- The final node of a trace is always reached, with the environment/state the trace
    ends in. Used to recover the final-state soundness theorem from `walkTrace_reaches`. -/
-lemma reaches_final {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} (st₁ : S.St ρ₁)
+def reaches_final {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
    (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) :
-    ∃ ρin, ∃ stin : S.St ρin,
-      Reaches tr st₁ s₂ ρin ρ₂ stin (stepTraceState tr st₁) := by
-  induction tr with
-  | single hnode => exact ⟨_, _, .single_here hnode⟩
-  | edge hnode hedge rest ih =>
-    obtain ⟨ρin, stin, hr⟩ := ih (stepNode _ hnode st₁)
-    exact ⟨ρin, stin, .edge_there hnode hedge rest hr⟩
-
-lemma walkTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} {st₁ : S.St ρ₁}
-    (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁ st₁)
-    (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) :
-    ⟦ variablesAt s₂ (result L prog) ⟧ ρ₂ (stepTraceState tr st₁) := by
-  obtain ⟨_, _, hr⟩ := reaches_final st₁ tr
-  exact (walkTrace_reaches hr hjoin).2
-
-variable (L prog) in
-theorem analyze_correct_state {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
-    ⟦ variablesAt prog.finalState (result L prog) ⟧ ρ
-      (stepTraceState (prog.trace hrun) S.init) := by
-  refine walkTrace ?_ (prog.trace hrun)
-  rw [joinForKey_initialState]
-  exact ValidStateEvaluator.botV_init
+    Σ ρin, Reaches tr s₂ ρin ρ₂ :=
+  match tr with
+  | .single hnode => ⟨_, .single_here hnode⟩
+  | .edge hnode hedge rest =>
+    let ⟨ρin, r'⟩ := reaches_final rest; ⟨ρin, .edge_there hnode hedge _ r'⟩

 variable (L prog) in
 /-- Soundness at every program point reached during execution: for any node `s` visited
@@ -177,21 +137,30 @@ variable (L prog) in
    environment entering `s` and the one leaving it. The final-state theorem
    `analyze_correct_state` is the special case where `s` is `prog.finalState`. -/
 theorem analyze_correct_at {ρf : Env} (hrun : EvalStmt [] prog.rootStmt ρf)
-    {s : prog.State} {ρin ρout : Env} {stin : S.St ρin} {stout : S.St ρout}
-    (hr : Reaches (prog.trace hrun) S.init s ρin ρout stin stout) :
-    ⟦ joinForKey s (result L prog) ⟧ ρin stin
-      ∧ ⟦ variablesAt s (result L prog) ⟧ ρout stout := by
-  refine walkTrace_reaches hr ?_
+    {s : prog.State} {ρin ρout : Env}
+    (hr : Reaches (prog.trace hrun) s ρin ρout) :
+    ⟦ joinForKey s (result L prog) ⟧ (S.Pre hr.pre)
+      ∧ ⟦ variablesAt s (result L prog) ⟧ (S.Post hr.post) := by
+  refine walkTrace_reaches hr (Traceₗ.single _ _ []) ?_
  rw [joinForKey_initialState]
  exact ValidStateEvaluator.botV_init

+variable (L prog) in
+theorem analyze_correct'
+    {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
+    ⟦ variablesAt prog.finalState (result L prog) ⟧ (S.Post (reaches_final (prog.trace hrun)).2.post) := by
+  let idk₀ := prog.trace hrun
+  have ⟨_, idk₁⟩ := reaches_final idk₀
+  have ⟨_, idk₂⟩ := analyze_correct_at L prog hrun idk₁
+  assumption
+
 end

 variable (L prog) in
 theorem analyze_correct [LatticeInterpretation L] [ValidStmtEvaluator L prog]
    {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
-    ⟦ variablesAt prog.finalState (result L prog) ⟧ ρ () :=
-  analyze_correct_state L prog hrun
+    ⟦ variablesAt prog.finalState (result L prog) ⟧ ρ :=
+  analyze_correct' L prog hrun

 end Forward

--- a/lean/Spa/Analysis/Forward/Evaluation.lean
+++ b/lean/Spa/Analysis/Forward/Evaluation.lean
@@ -17,12 +17,12 @@ class ExprEvaluator where
 class ValidExprEvaluator [ExprEvaluator L prog] [I : LatticeInterpretation L] :
    Prop where
  valid : ∀ {vs : VariableValues L prog} {ρ : Env} {e : Expr} {v : Value},
-    EvalExpr ρ e v → ⟦ vs ⟧ ρ () → I.interp (ExprEvaluator.eval e vs) v
+    EvalExpr ρ e v → ⟦ vs ⟧ ρ → I.interp (ExprEvaluator.eval e vs) v

 class ValidStmtEvaluator [E : StmtEvaluator L prog] [LatticeInterpretation L] :
    Prop where
  valid : ∀ {s : prog.State} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env},
-    EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂ → ⟦ vs ⟧ ρ₁ () → ⟦ E.eval s vs ⟧ ρ₂ ()
+    EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂ → ⟦ vs ⟧ ρ₁ → ⟦ E.eval s vs ⟧ ρ₂

 end Forward

--- a/lean/Spa/Analysis/Forward/Lattices.lean
+++ b/lean/Spa/Analysis/Forward/Lattices.lean
@@ -65,22 +65,28 @@ lemma variablesAt_joinAll (s : prog.State) (sv : StateVariables L prog) :
  joinAll_mem_eq (variablesAt_mem s (joinAll sv))

 class StateInterpretation (L : Type) [Lattice L] (prog : Program) where
-  St : Env → Type
-  init : St []
-  interp : VariableValues L prog → (ρ : Env) → St ρ → Prop
-  interp_sup : ∀ {vs₁ vs₂ : VariableValues L prog} {ρ : Env} {st : St ρ},
-    interp vs₁ ρ st ∨ interp vs₂ ρ st → interp (vs₁ ⊔ vs₂) ρ st
-  interp_inf : ∀ {vs₁ vs₂ : VariableValues L prog} {ρ : Env} {st : St ρ},
-    interp vs₁ ρ st ∧ interp vs₂ ρ st → interp (vs₁ ⊓ vs₂) ρ st
+  Proj : Type
+  Pre : ∀ {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}, Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂ → Proj
+  Post : ∀ {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}, Trace prog.cfg s₁ s₂ ρ₁ ρ₂ → Proj
+
+  interp : VariableValues L prog → (p : Proj) → Prop
+  interp_sup : ∀ {vs₁ vs₂ : VariableValues L prog} {p : Proj},
+    interp vs₁ p ∨ interp vs₂ p → interp (vs₁ ⊔ vs₂) p
+  interp_inf : ∀ {vs₁ vs₂ : VariableValues L prog} {p : Proj},
+    interp vs₁ p ∧ interp vs₂ p → interp (vs₁ ⊓ vs₂) p
+
+  post_pre : ∀ {vs} {s₁ s₂ s₃: prog.State} {ρ₁ ρ₂ : Env}
+    (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) (hedge : (s₂, s₃) ∈ prog.cfg.edges),
+    interp vs (Post tr) → interp vs (Pre (tr.addEdge hedge))

 instance [S : StateInterpretation L prog] :
-    Interp (VariableValues L prog) ((ρ : Env) → S.St ρ → Prop) :=
+    Interp (VariableValues L prog) (S.Proj → Prop) :=
  ⟨S.interp⟩

 lemma interp_foldr [S : StateInterpretation L prog]
    {vs : VariableValues L prog} {vss : List (VariableValues L prog)}
-    {ρ : Env} {st : S.St ρ} (hvs : ⟦ vs ⟧ ρ st) (hmem : vs ∈ vss) :
-    ⟦ vss.foldr (· ⊔ ·) (botV L prog) ⟧ ρ st := by
+    {p : S.Proj} (hvs : ⟦ vs ⟧ p) (hmem : vs ∈ vss) :
+    ⟦ vss.foldr (· ⊔ ·) (botV L prog) ⟧ p := by
  induction vss with
  | nil => cases hmem
  | cons vs' vss' ih =>
@@ -91,20 +97,24 @@ lemma interp_foldr [S : StateInterpretation L prog]
 variable [I : LatticeInterpretation L]

 instance : StateInterpretation L prog where
-  St := fun _ => PUnit
-  init := PUnit.unit
-  interp vs ρ _ := ∀ (k : String) (l : L), (k, l) ∈ vs →
+  Proj := Env
+  Pre := fun {_ _ _ ρ₂} _ => ρ₂
+  Post := fun {_ _ _ ρ₂} _ => ρ₂
+
+  interp vs ρ := ∀ (k : String) (l : L), (k, l) ∈ vs →
    ∀ (v : Value), Env.Mem (k, v) ρ → I.interp l v
  interp_sup := by
-    intro vs₁ vs₂ ρ st h k l hmem v hv
+    intro vs₁ vs₂ ρ h k l hmem v hv
    obtain ⟨l₁, l₂, rfl, h₁, h₂⟩ := FiniteMap.mem_sup hmem
    rcases h with h | h
    · exact I.interp_sup v (Or.inl (h _ _ h₁ _ hv))
    · exact I.interp_sup v (Or.inr (h _ _ h₂ _ hv))
  interp_inf := by
-    intro vs₁ vs₂ ρ st h k l hmem v hv
+    intro vs₁ vs₂ ρ h k l hmem v hv
    obtain ⟨l₁, l₂, rfl, h₁, h₂⟩ := FiniteMap.mem_inf hmem
    exact I.interp_inf v ⟨h.1 _ _ h₁ _ hv, h.2 _ _ h₂ _ hv⟩
+  post_pre := by simp
+

 end Forward

--- a/lean/Spa/Analysis/Sign.lean
+++ b/lean/Spa/Analysis/Sign.lean
@@ -210,14 +210,14 @@ instance eval_valid : ValidExprEvaluator SignLattice prog := by
    exact minus_valid h₁ h₂

 theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
-    ⟦ variablesAt prog.finalState (result SignLattice prog) ⟧ ρ () :=
+    ⟦ variablesAt prog.finalState (result SignLattice prog) ⟧ ρ :=
  Forward.analyze_correct SignLattice prog hrun

 theorem analyze_correct_at {ρf : Env} (hrun : EvalStmt [] prog.rootStmt ρf)
-    {s : prog.State} {ρin ρout : Env} {stin stout : PUnit}
-    (hr : Reaches (L := SignLattice) (prog.trace hrun) PUnit.unit s ρin ρout stin stout) :
-    ⟦ joinForKey s (result SignLattice prog) ⟧ ρin stin
-      ∧ ⟦ variablesAt s (result SignLattice prog) ⟧ ρout stout :=
+    {s : prog.State} {ρin ρout : Env}
+    (hr : Reaches (prog.trace hrun) s ρin ρout) :
+    ⟦ joinForKey s (result SignLattice prog) ⟧ ρin
+      ∧ ⟦ variablesAt s (result SignLattice prog) ⟧ ρout :=
  Forward.analyze_correct_at SignLattice prog hrun hr

 end SignAnalysis