From ed88f4ce94ad3f512eb05510ea6c3bc49c668b49 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Tue, 23 Jun 2026 13:29:54 -0500 Subject: [PATCH] Use 'interp' to add [[ bla ]] notation for analysis Signed-off-by: Danila Fedorin --- lean/Spa/Analysis/Constant.lean | 2 +- lean/Spa/Analysis/Forward.lean | 34 +++++++++++------------ lean/Spa/Analysis/Forward/Evaluation.lean | 4 +-- lean/Spa/Analysis/Forward/Lattices.lean | 24 ++++++++-------- lean/Spa/Analysis/Sign.lean | 2 +- 5 files changed, 34 insertions(+), 32 deletions(-) diff --git a/lean/Spa/Analysis/Constant.lean b/lean/Spa/Analysis/Constant.lean index c644132..235cbbc 100644 --- a/lean/Spa/Analysis/Constant.lean +++ b/lean/Spa/Analysis/Constant.lean @@ -156,7 +156,7 @@ instance eval_valid : ValidExprEvaluator ConstLattice prog := by exact minus_valid h₁ h₂ theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : - interpV (variablesAt prog.finalState (result ConstLattice prog)) ρ := + ⟦ variablesAt prog.finalState (result ConstLattice prog) ⟧ ρ := Spa.analyze_correct ConstLattice prog hrun end ConstAnalysis diff --git a/lean/Spa/Analysis/Forward.lean b/lean/Spa/Analysis/Forward.lean index 28c500f..90e9025 100644 --- a/lean/Spa/Analysis/Forward.lean +++ b/lean/Spa/Analysis/Forward.lean @@ -59,8 +59,8 @@ variable [I : LatticeInterpretation L] [V : ValidStmtEvaluator L prog] omit [FiniteHeightLattice L] [DecidableEq L] in theorem eval_fold_valid {s : prog.State} {bss : List BasicStmt} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env} - (hbss : EvalBasicStmts ρ₁ bss ρ₂) (hvs : interpV vs ρ₁) : - interpV (bss.foldl (fun vs bs => E.eval s bs vs) vs) ρ₂ := by + (hbss : EvalBasicStmts ρ₁ bss ρ₂) (hvs : ⟦ vs ⟧ ρ₁) : + ⟦ bss.foldl (fun vs bs => E.eval s bs vs) vs ⟧ ρ₂ := by induction hbss generalizing vs with | nil => exact hvs | cons hbs _ ih => exact ih (ValidStmtEvaluator.valid hbs hvs) @@ -69,51 +69,51 @@ omit [FiniteHeightLattice L] [DecidableEq L] in theorem updateVariablesForState_matches {s : prog.State} {sv : StateVariables L prog} {ρ₁ ρ₂ : Env} (hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂) - (hvs : interpV (variablesAt s sv) ρ₁) : - interpV (updateVariablesForState s sv) ρ₂ := + (hvs : ⟦ variablesAt s sv ⟧ ρ₁) : + ⟦ updateVariablesForState s sv ⟧ ρ₂ := eval_fold_valid hbss hvs omit [FiniteHeightLattice L] [DecidableEq L] in theorem updateAll_matches {s : prog.State} {sv : StateVariables L prog} {ρ₁ ρ₂ : Env} (hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂) - (hvs : interpV (variablesAt s sv) ρ₁) : - interpV (variablesAt s (updateAll sv)) ρ₂ := by + (hvs : ⟦ variablesAt s sv ⟧ ρ₁) : + ⟦ variablesAt s (updateAll sv) ⟧ ρ₂ := by rw [variablesAt_updateAll] exact updateVariablesForState_matches hbss hvs theorem stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env} - (hjoin : interpV (joinForKey s₁ (result L prog)) ρ₁) + (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁) (hbss : EvalBasicStmts ρ₁ (prog.code s₁) ρ₂) : - interpV (variablesAt s₁ (result L prog)) ρ₂ := by + ⟦ variablesAt s₁ (result L prog) ⟧ ρ₂ := by rw [result_eq L prog] refine updateAll_matches hbss ?_ rw [variablesAt_joinAll] exact hjoin theorem walkTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} - (hjoin : interpV (joinForKey s₁ (result L prog)) ρ₁) + (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁) (tr : Trace prog.graph s₁ s₂ ρ₁ ρ₂) : - interpV (variablesAt s₂ (result L prog)) ρ₂ := by + ⟦ variablesAt s₂ (result L prog) ⟧ ρ₂ := by induction tr with | single hbss => exact stepTrace hjoin hbss | @edge _ ρ' _ i₁ i₂ _ hbss hedge _ ih => - have hstep : interpV (variablesAt i₁ (result L prog)) ρ' := + have hstep : ⟦ variablesAt i₁ (result L prog) ⟧ ρ' := stepTrace hjoin hbss have hmem : variablesAt i₁ (result L prog) ∈ (result L prog).valuesAt (prog.incoming i₂) := FiniteMap.mem_valuesAt prog.states_nodup (prog.mem_incoming_of_edge hedge) (variablesAt_mem i₁ (result L prog)) - exact ih (interpV_foldr hstep hmem) + exact ih (interp_foldr hstep hmem) omit V in -theorem interpV_joinForKey_initialState : - interpV (joinForKey prog.initialState (result L prog)) [] := by +theorem interp_joinForKey_initialState : + ⟦ joinForKey prog.initialState (result L prog) ⟧ [] := by rw [joinForKey_initialState] - exact interpV_botV_nil + exact interp_botV_nil variable (L prog) in theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : - interpV (variablesAt prog.finalState (result L prog)) ρ := - walkTrace interpV_joinForKey_initialState (prog.trace hrun) + ⟦ variablesAt prog.finalState (result L prog) ⟧ ρ := + walkTrace interp_joinForKey_initialState (prog.trace hrun) end Spa diff --git a/lean/Spa/Analysis/Forward/Evaluation.lean b/lean/Spa/Analysis/Forward/Evaluation.lean index 818ff04..27d8065 100644 --- a/lean/Spa/Analysis/Forward/Evaluation.lean +++ b/lean/Spa/Analysis/Forward/Evaluation.lean @@ -15,12 +15,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 → interpV 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} {bs : BasicStmt}, - EvalBasicStmt ρ₁ bs ρ₂ → interpV vs ρ₁ → interpV (E.eval s bs vs) ρ₂ + EvalBasicStmt ρ₁ bs ρ₂ → ⟦ vs ⟧ ρ₁ → ⟦ E.eval s bs vs ⟧ ρ₂ end Spa diff --git a/lean/Spa/Analysis/Forward/Lattices.lean b/lean/Spa/Analysis/Forward/Lattices.lean index bd3d36a..f10be81 100644 --- a/lean/Spa/Analysis/Forward/Lattices.lean +++ b/lean/Spa/Analysis/Forward/Lattices.lean @@ -1,5 +1,6 @@ import Spa.Language import Spa.Lattice.FiniteMap +import Spa.Interp namespace Spa @@ -66,32 +67,33 @@ theorem variablesAt_joinAll (s : prog.State) (sv : StateVariables L prog) : variable [I : LatticeInterpretation L] omit [FiniteHeightLattice L] in -def interpV (vs : VariableValues L prog) (ρ : Env) : Prop := - ∀ (k : String) (l : L), (k, l) ∈ vs → - ∀ (v : Value), Env.Mem (k, v) ρ → I.interp l v +instance : Interp (VariableValues L prog) (Env → Prop) where + interp (vs : VariableValues L prog) (ρ : Env) : Prop := + ∀ (k : String) (l : L), (k, l) ∈ vs → + ∀ (v : Value), Env.Mem (k, v) ρ → I.interp l v -theorem interpV_botV_nil : interpV (botV L prog) [] := by +theorem interp_botV_nil : ⟦ botV L prog ⟧ [] := by intro k l _ v hmem cases hmem omit [FiniteHeightLattice L] in -theorem interpV_sup {vs₁ vs₂ : VariableValues L prog} {ρ : Env} - (h : interpV vs₁ ρ ∨ interpV vs₂ ρ) : interpV (vs₁ ⊔ vs₂) ρ := by +theorem interp_sup {vs₁ vs₂ : VariableValues L prog} {ρ : Env} + (h : ⟦ vs₁⟧ ρ ∨ ⟦ vs₂ ⟧ ρ) : ⟦ vs₁ ⊔ vs₂ ⟧ ρ := by intro 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)) -theorem interpV_foldr {vs : VariableValues L prog} +theorem interp_foldr {vs : VariableValues L prog} {vss : List (VariableValues L prog)} {ρ : Env} - (hvs : interpV vs ρ) (hmem : vs ∈ vss) : - interpV (vss.foldr (· ⊔ ·) (botV L prog)) ρ := by + (hvs : ⟦ vs ⟧ ρ) (hmem : vs ∈ vss) : + ⟦ vss.foldr (· ⊔ ·) (botV L prog) ⟧ ρ := by induction vss with | nil => cases hmem | cons vs' vss' ih => rcases List.mem_cons.mp hmem with rfl | hmem' - · exact interpV_sup (Or.inl hvs) - · exact interpV_sup (Or.inr (ih hmem')) + · exact interp_sup (Or.inl hvs) + · exact interp_sup (Or.inr (ih hmem')) end Spa diff --git a/lean/Spa/Analysis/Sign.lean b/lean/Spa/Analysis/Sign.lean index 876ada0..4d01a90 100644 --- a/lean/Spa/Analysis/Sign.lean +++ b/lean/Spa/Analysis/Sign.lean @@ -214,7 +214,7 @@ instance eval_valid : ValidExprEvaluator SignLattice prog := by exact minus_valid h₁ h₂ theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : - interpV (variablesAt prog.finalState (result SignLattice prog)) ρ := + ⟦ variablesAt prog.finalState (result SignLattice prog) ⟧ ρ := Spa.analyze_correct SignLattice prog hrun end SignAnalysis