DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Use 'interp' to add [[ bla ]] notation for analysis

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin
2026-06-23 13:29:54 -05:00
parent 8ce6e5e4e4
commit ed88f4ce94
5 changed files with 34 additions and 32 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
lean/Spa/Analysis/Constant.lean
View File

@@ -156,7 +156,7 @@ instance eval_valid : ValidExprEvaluator ConstLattice prog := by
exact minus_valid h₁ h₂ exact minus_valid h₁ h₂
theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : 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 Spa.analyze_correct ConstLattice prog hrun
end ConstAnalysis end ConstAnalysis

34
lean/Spa/Analysis/Forward.lean
View File

@@ -59,8 +59,8 @@ variable [I : LatticeInterpretation L] [V : ValidStmtEvaluator L prog]
omit [FiniteHeightLattice L] [DecidableEq L] in omit [FiniteHeightLattice L] [DecidableEq L] in
theorem eval_fold_valid {s : prog.State} {bss : List BasicStmt} theorem eval_fold_valid {s : prog.State} {bss : List BasicStmt}
{vs : VariableValues L prog} {ρ₁ ρ₂ : Env} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env}
(hbss : EvalBasicStmts ρ₁ bss ρ₂) (hvs : interpV vs ρ₁) : (hbss : EvalBasicStmts ρ₁ bss ρ₂) (hvs : ⟦ vs ⟧ ρ₁) :
interpV (bss.foldl (fun vs bs => E.eval s bs vs) vs) ρ₂ := by ⟦ bss.foldl (fun vs bs => E.eval s bs vs) vs ⟧ ρ₂ := by
induction hbss generalizing vs with induction hbss generalizing vs with
| nil => exact hvs | nil => exact hvs
| cons hbs _ ih => exact ih (ValidStmtEvaluator.valid hbs 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} theorem updateVariablesForState_matches {s : prog.State}
{sv : StateVariables L prog} {ρ₁ ρ₂ : Env} {sv : StateVariables L prog} {ρ₁ ρ₂ : Env}
(hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂) (hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂)
(hvs : interpV (variablesAt s sv) ρ₁) : (hvs : ⟦ variablesAt s sv ⟧ ρ₁) :
interpV (updateVariablesForState s sv) ρ₂ := ⟦ updateVariablesForState s sv ⟧ ρ₂ :=
eval_fold_valid hbss hvs eval_fold_valid hbss hvs
omit [FiniteHeightLattice L] [DecidableEq L] in omit [FiniteHeightLattice L] [DecidableEq L] in
theorem updateAll_matches {s : prog.State} {sv : StateVariables L prog} theorem updateAll_matches {s : prog.State} {sv : StateVariables L prog}
{ρ₁ ρ₂ : Env} (hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂) {ρ₁ ρ₂ : Env} (hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂)
(hvs : interpV (variablesAt s sv) ρ₁) : (hvs : ⟦ variablesAt s sv ⟧ ρ₁) :
interpV (variablesAt s (updateAll sv)) ρ₂ := by ⟦ variablesAt s (updateAll sv) ⟧ ρ₂ := by
rw [variablesAt_updateAll] rw [variablesAt_updateAll]
exact updateVariablesForState_matches hbss hvs exact updateVariablesForState_matches hbss hvs
theorem stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env} theorem stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env}
(hjoin : interpV (joinForKey s₁ (result L prog)) ρ₁) (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁)
(hbss : EvalBasicStmts ρ₁ (prog.code s₁) ρ₂) : (hbss : EvalBasicStmts ρ₁ (prog.code s₁) ρ₂) :
interpV (variablesAt s₁ (result L prog)) ρ₂ := by ⟦ variablesAt s₁ (result L prog) ⟧ ρ₂ := by
rw [result_eq L prog] rw [result_eq L prog]
refine updateAll_matches hbss ?_ refine updateAll_matches hbss ?_
rw [variablesAt_joinAll] rw [variablesAt_joinAll]
exact hjoin exact hjoin
theorem walkTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} 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₂ ρ₁ ρ₂) : (tr : Trace prog.graph s₁ s₂ ρ₁ ρ₂) :
interpV (variablesAt s₂ (result L prog)) ρ₂ := by ⟦ variablesAt s₂ (result L prog) ⟧ ρ₂ := by
induction tr with induction tr with
| single hbss => exact stepTrace hjoin hbss | single hbss => exact stepTrace hjoin hbss
| @edge _ ρ' _ i₁ i₂ _ hbss hedge _ ih => | @edge _ ρ' _ i₁ i₂ _ hbss hedge _ ih =>
have hstep : interpV (variablesAt i₁ (result L prog)) ρ' := have hstep : ⟦ variablesAt i₁ (result L prog) ⟧ ρ' :=
stepTrace hjoin hbss stepTrace hjoin hbss
have hmem : variablesAt i₁ (result L prog) have hmem : variablesAt i₁ (result L prog)
∈ (result L prog).valuesAt (prog.incoming i₂) := ∈ (result L prog).valuesAt (prog.incoming i₂) :=
FiniteMap.mem_valuesAt prog.states_nodup FiniteMap.mem_valuesAt prog.states_nodup
(prog.mem_incoming_of_edge hedge) (variablesAt_mem i₁ (result L prog)) (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 omit V in
theorem interpV_joinForKey_initialState : theorem interp_joinForKey_initialState :
interpV (joinForKey prog.initialState (result L prog)) [] := by ⟦ joinForKey prog.initialState (result L prog) ⟧ [] := by
rw [joinForKey_initialState] rw [joinForKey_initialState]
exact interpV_botV_nil exact interp_botV_nil
variable (L prog) in variable (L prog) in
theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
interpV (variablesAt prog.finalState (result L prog)) ρ := ⟦ variablesAt prog.finalState (result L prog) ⟧ ρ :=
walkTrace interpV_joinForKey_initialState (prog.trace hrun) walkTrace interp_joinForKey_initialState (prog.trace hrun)
end Spa end Spa

4
lean/Spa/Analysis/Forward/Evaluation.lean
View File

@@ -15,12 +15,12 @@ class ExprEvaluator where
class ValidExprEvaluator [ExprEvaluator L prog] [I : LatticeInterpretation L] : class ValidExprEvaluator [ExprEvaluator L prog] [I : LatticeInterpretation L] :
Prop where Prop where
valid : ∀ {vs : VariableValues L prog} {ρ : Env} {e : Expr} {v : Value}, 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] : class ValidStmtEvaluator [E : StmtEvaluator L prog] [LatticeInterpretation L] :
Prop where Prop where
valid : ∀ {s : prog.State} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env} valid : ∀ {s : prog.State} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env}
{bs : BasicStmt}, {bs : BasicStmt},
EvalBasicStmt ρ₁ bs ρ₂ → interpV vs ρ₁ → interpV (E.eval s bs vs) ρ₂ EvalBasicStmt ρ₁ bs ρ₂ → ⟦ vs ⟧ ρ₁ → ⟦ E.eval s bs vs ⟧ ρ₂
end Spa end Spa

24
lean/Spa/Analysis/Forward/Lattices.lean
View File

@@ -1,5 +1,6 @@
import Spa.Language import Spa.Language
import Spa.Lattice.FiniteMap import Spa.Lattice.FiniteMap
import Spa.Interp
namespace Spa namespace Spa
@@ -66,32 +67,33 @@ theorem variablesAt_joinAll (s : prog.State) (sv : StateVariables L prog) :
variable [I : LatticeInterpretation L] variable [I : LatticeInterpretation L]
omit [FiniteHeightLattice L] in omit [FiniteHeightLattice L] in
def interpV (vs : VariableValues L prog) (ρ : Env) : Prop := instance : Interp (VariableValues L prog) (Env → Prop) where
∀ (k : String) (l : L), (k, l) ∈ vs → interp (vs : VariableValues L prog) (ρ : Env) : Prop :=
∀ (v : Value), Env.Mem (k, v) ρ → I.interp l v ∀ (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 intro k l _ v hmem
cases hmem cases hmem
omit [FiniteHeightLattice L] in omit [FiniteHeightLattice L] in
theorem interpV_sup {vs₁ vs₂ : VariableValues L prog} {ρ : Env} theorem interp_sup {vs₁ vs₂ : VariableValues L prog} {ρ : Env}
(h : interpV vs₁ ρ ∨ interpV vs₂ ρ) : interpV (vs₁ ⊔ vs₂) ρ := by (h : ⟦ vs₁⟧ ρ ∨ ⟦ vs₂ ⟧ ρ) : ⟦ vs₁ ⊔ vs₂ ⟧ ρ := by
intro k l hmem v hv intro k l hmem v hv
obtain ⟨l₁, l₂, rfl, h₁, h₂⟩ := FiniteMap.mem_sup hmem obtain ⟨l₁, l₂, rfl, h₁, h₂⟩ := FiniteMap.mem_sup hmem
rcases h with h | h rcases h with h | h
· exact I.interp_sup v (Or.inl (h _ _ h₁ _ hv)) · exact I.interp_sup v (Or.inl (h _ _ h₁ _ hv))
· exact I.interp_sup v (Or.inr (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} {vss : List (VariableValues L prog)} {ρ : Env}
(hvs : interpV vs ρ) (hmem : vs ∈ vss) : (hvs : ⟦ vs ⟧ ρ) (hmem : vs ∈ vss) :
interpV (vss.foldr (· ⊔ ·) (botV L prog)) ρ := by ⟦ vss.foldr (· ⊔ ·) (botV L prog) ⟧ ρ := by
induction vss with induction vss with
| nil => cases hmem | nil => cases hmem
| cons vs' vss' ih => | cons vs' vss' ih =>
rcases List.mem_cons.mp hmem with rfl | hmem' rcases List.mem_cons.mp hmem with rfl | hmem'
· exact interpV_sup (Or.inl hvs) · exact interp_sup (Or.inl hvs)
· exact interpV_sup (Or.inr (ih hmem')) · exact interp_sup (Or.inr (ih hmem'))
end Spa end Spa

2
lean/Spa/Analysis/Sign.lean
View File

@@ -214,7 +214,7 @@ instance eval_valid : ValidExprEvaluator SignLattice prog := by
exact minus_valid h₁ h₂ exact minus_valid h₁ h₂
theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : 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 Spa.analyze_correct SignLattice prog hrun
end SignAnalysis end SignAnalysis