Lean migration: Phase 6 (forward analysis framework)
- Spa.Analysis.Forward.Lattices: VariableValues/StateVariables (FiniteMap instantiations), fixed heights, variablesAt, joinForKey/joinAll, interpV and its sup/foldr lemmas - Spa.Analysis.Forward.Evaluation: StmtEvaluator/ExprEvaluator + validity (the Agda Valid* instance records become plain Props) - Spa.Analysis.Forward.Adapters: expr-to-stmt evaluator adapter + validity - Spa.Analysis.Forward: updateAll, analyze, result (least fixpoint via the gas-based Fixedpoint), walkTrace, analyze_correct — the framework's main soundness theorem Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
77
lean/Spa/Analysis/Forward/Adapters.lean
Normal file
77
lean/Spa/Analysis/Forward/Adapters.lean
Normal file
@@ -0,0 +1,77 @@
|
||||
/-
|
||||
Port of `Analysis/Forward/Adapters.agda` (`ExprToStmtAdapter`).
|
||||
|
||||
Correspondence:
|
||||
updateVariablesFromExpression ↦ updateVariablesFromExpression
|
||||
updateVariablesFromExpression-Mono ↦ updateVariablesFromExpression_mono
|
||||
(the -k∈ks-≡ / -k∉ks-backward renames ↦ used directly from FiniteMap)
|
||||
evalᵇ, evalᵇ-Monoʳ ↦ evalB, evalB_mono
|
||||
stmtEvaluator (instance) ↦ ExprEvaluator.toStmtEvaluator
|
||||
evalᵇ-valid, validStmtEvaluator ↦ ExprEvaluator.toStmtEvaluator_valid
|
||||
(the Agda `k ≟ˢ k'` case split is
|
||||
subsumed by `cases` on `Env.Mem`,
|
||||
whose `here` case forces `k' = k`)
|
||||
-/
|
||||
import Spa.Analysis.Forward.Evaluation
|
||||
|
||||
namespace Spa
|
||||
|
||||
variable {L : Type} [Lattice L] {prog : Program}
|
||||
|
||||
/-- Agda: `updateVariablesFromExpression` — set the single key `k` to the
|
||||
value of `e` (the `GeneralizedUpdate` with `ks = [k]`). -/
|
||||
def updateVariablesFromExpression (E : ExprEvaluator L prog) (k : String)
|
||||
(e : Expr) (vs : VariableValues L prog) : VariableValues L prog :=
|
||||
FiniteMap.generalizedUpdate id (fun _ vs => E.eval e vs) [k] vs
|
||||
|
||||
/-- Agda: `updateVariablesFromExpression-Mono`. -/
|
||||
theorem updateVariablesFromExpression_mono (E : ExprEvaluator L prog)
|
||||
(k : String) (e : Expr) :
|
||||
Monotone (updateVariablesFromExpression E k e) :=
|
||||
FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => E.eval_mono e)
|
||||
|
||||
/-- Agda: `evalᵇ`. -/
|
||||
def evalB (E : ExprEvaluator L prog) (_ : prog.State) (bs : BasicStmt)
|
||||
(vs : VariableValues L prog) : VariableValues L prog :=
|
||||
match bs with
|
||||
| .assign k e => updateVariablesFromExpression E k e vs
|
||||
| .noop => vs
|
||||
|
||||
/-- Agda: `evalᵇ-Monoʳ`. -/
|
||||
theorem evalB_mono (E : ExprEvaluator L prog) (s : prog.State) (bs : BasicStmt) :
|
||||
Monotone (evalB E s bs) := by
|
||||
cases bs with
|
||||
| assign k e => exact updateVariablesFromExpression_mono E k e
|
||||
| noop => exact monotone_id
|
||||
|
||||
/-- Agda: the `stmtEvaluator` instance of `ExprToStmtAdapter`. -/
|
||||
def ExprEvaluator.toStmtEvaluator (E : ExprEvaluator L prog) :
|
||||
StmtEvaluator L prog :=
|
||||
⟨evalB E, evalB_mono E⟩
|
||||
|
||||
/-- Agda: `evalᵇ-valid` / the `validStmtEvaluator` instance. -/
|
||||
theorem ExprEvaluator.toStmtEvaluator_valid (E : ExprEvaluator L prog)
|
||||
{I : LatticeInterpretation L} (hE : IsValidExprEvaluator E I) :
|
||||
IsValidStmtEvaluator E.toStmtEvaluator I := by
|
||||
intro s vs ρ₁ ρ₂ bs hbs hvs
|
||||
cases hbs with
|
||||
| noop => exact hvs
|
||||
| assign k e v hev =>
|
||||
intro k' l hk'l v' hv'
|
||||
cases hv' with
|
||||
| here =>
|
||||
have hk'l₀ : (k, l) ∈ FiniteMap.generalizedUpdate (ks := prog.vars) id
|
||||
(fun _ vs => E.eval e vs) [k] vs := hk'l
|
||||
have hl := FiniteMap.generalizedUpdate_mem_eq (f := id)
|
||||
(g := fun _ vs => E.eval e vs) (List.mem_singleton_self k) hk'l₀
|
||||
rw [hl]
|
||||
exact hE hev hvs
|
||||
| there _ _ _ _ _ hne hmem' =>
|
||||
have hk'l₀ : (k', l) ∈ FiniteMap.generalizedUpdate (ks := prog.vars) id
|
||||
(fun _ vs => E.eval e vs) [k] vs := hk'l
|
||||
have hk'l' : (k', l) ∈ (id vs : VariableValues L prog) :=
|
||||
FiniteMap.generalizedUpdate_not_mem_backward
|
||||
(fun hmem => hne (List.mem_singleton.mp hmem)) hk'l₀
|
||||
exact hvs _ _ hk'l' _ hmem'
|
||||
|
||||
end Spa
|
||||
44
lean/Spa/Analysis/Forward/Evaluation.lean
Normal file
44
lean/Spa/Analysis/Forward/Evaluation.lean
Normal file
@@ -0,0 +1,44 @@
|
||||
/-
|
||||
Port of `Analysis/Forward/Evaluation.agda`.
|
||||
|
||||
Correspondence:
|
||||
StmtEvaluator (eval, eval-Monoʳ) ↦ StmtEvaluator (eval, eval_mono)
|
||||
ExprEvaluator (eval, eval-Monoʳ) ↦ ExprEvaluator (eval, eval_mono)
|
||||
IsValidExprEvaluator ↦ IsValidExprEvaluator
|
||||
IsValidStmtEvaluator ↦ IsValidStmtEvaluator
|
||||
ValidExprEvaluator,
|
||||
ValidStmtEvaluator (records) ↦ (the `IsValid…` Props are passed
|
||||
directly; the wrapper records existed
|
||||
for Agda instance resolution)
|
||||
-/
|
||||
import Spa.Analysis.Forward.Lattices
|
||||
|
||||
namespace Spa
|
||||
|
||||
variable (L : Type) [Lattice L] (prog : Program)
|
||||
|
||||
/-- Agda: `StmtEvaluator`. -/
|
||||
structure StmtEvaluator where
|
||||
eval : prog.State → BasicStmt → VariableValues L prog → VariableValues L prog
|
||||
eval_mono : ∀ s bs, Monotone (eval s bs)
|
||||
|
||||
/-- Agda: `ExprEvaluator`. -/
|
||||
structure ExprEvaluator where
|
||||
eval : Expr → VariableValues L prog → L
|
||||
eval_mono : ∀ e, Monotone (eval e)
|
||||
|
||||
variable {L prog}
|
||||
|
||||
/-- Agda: `IsValidExprEvaluator`. -/
|
||||
def IsValidExprEvaluator (E : ExprEvaluator L prog)
|
||||
(I : LatticeInterpretation L) : Prop :=
|
||||
∀ {vs : VariableValues L prog} {ρ : Env} {e : Expr} {v : Value},
|
||||
EvalExpr ρ e v → interpV I vs ρ → I.interp (E.eval e vs) v
|
||||
|
||||
/-- Agda: `IsValidStmtEvaluator`. -/
|
||||
def IsValidStmtEvaluator (E : StmtEvaluator L prog)
|
||||
(I : LatticeInterpretation L) : Prop :=
|
||||
∀ {s : prog.State} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env} {bs : BasicStmt},
|
||||
EvalBasicStmt ρ₁ bs ρ₂ → interpV I vs ρ₁ → interpV I (E.eval s bs vs) ρ₂
|
||||
|
||||
end Spa
|
||||
153
lean/Spa/Analysis/Forward/Lattices.lean
Normal file
153
lean/Spa/Analysis/Forward/Lattices.lean
Normal file
@@ -0,0 +1,153 @@
|
||||
/-
|
||||
Port of `Analysis/Forward/Lattices.agda`.
|
||||
|
||||
The Agda module instantiates `Lattice.FiniteMap` twice (variables ↦ abstract
|
||||
values, states ↦ variable maps) and re-exports everything with ᵛ/ᵐ suffixes.
|
||||
In Lean the two instantiations are `abbrev`s and the FiniteMap API is used
|
||||
directly; the module parameters (the finite-height lattice `L`, the program)
|
||||
become section variables.
|
||||
|
||||
Correspondence:
|
||||
VariableValues, StateVariables ↦ VariableValues, StateVariables
|
||||
isLatticeᵛ/isLatticeᵐ, ⊔ᵛ, ≼ᵛ … ↦ (the FiniteMap Lattice instances)
|
||||
fixedHeightᵛ ↦ varsFixedHeight
|
||||
⊥ᵛ, ⊥ᵛ-contains-bottoms ↦ botV, FiniteMap.bot_contains_bots
|
||||
states-in-Map ↦ states_memKey
|
||||
variablesAt ↦ variablesAt
|
||||
variablesAt-∈ ↦ variablesAt_mem
|
||||
variablesAt-≈ ↦ (congruence, trivial with `=`)
|
||||
joinForKey, joinForKey-Mono ↦ joinForKey, joinForKey_mono
|
||||
joinAll, joinAll-Mono,
|
||||
joinAll-k∈ks-≡ ↦ joinAll, joinAll_mono, joinAll_mem_eq
|
||||
variablesAt-joinAll ↦ variablesAt_joinAll
|
||||
⟦_⟧ᵛ ↦ interpV
|
||||
⟦⊥ᵛ⟧ᵛ∅ ↦ interpV_botV_nil
|
||||
⟦⟧ᵛ-respects-≈ᵛ ↦ (trivial with `=`)
|
||||
⟦⟧ᵛ-⊔ᵛ-∨ ↦ interpV_sup
|
||||
⟦⟧ᵛ-foldr ↦ interpV_foldr
|
||||
-/
|
||||
import Spa.Language
|
||||
import Spa.Lattice.FiniteMap
|
||||
|
||||
namespace Spa
|
||||
|
||||
variable (L : Type) [Lattice L] (prog : Program)
|
||||
|
||||
/-- Agda: `VariableValues`. -/
|
||||
abbrev VariableValues : Type := FiniteMap String L prog.vars
|
||||
|
||||
/-- Agda: `StateVariables`. -/
|
||||
abbrev StateVariables : Type := FiniteMap prog.State (VariableValues L prog) prog.states
|
||||
|
||||
variable {h : ℕ}
|
||||
|
||||
/-- Agda: `fixedHeightᵛ`. -/
|
||||
def varsFixedHeight (fhL : FixedHeight L h) :
|
||||
FixedHeight (VariableValues L prog) (prog.vars.length * h) :=
|
||||
FiniteMap.fixedHeight fhL prog.vars
|
||||
|
||||
/-- Agda: `⊥ᵛ`. -/
|
||||
def botV (fhL : FixedHeight L h) : VariableValues L prog :=
|
||||
(varsFixedHeight L prog fhL).bot
|
||||
|
||||
/-- Agda: `fixedHeight` on `StateVariables` (assembled in `Forward.agda`'s
|
||||
fixpoint call; named here for reuse). -/
|
||||
def statesFixedHeight (fhL : FixedHeight L h) :
|
||||
FixedHeight (StateVariables L prog) (prog.states.length * (prog.vars.length * h)) :=
|
||||
FiniteMap.fixedHeight (varsFixedHeight L prog fhL) prog.states
|
||||
|
||||
variable {L prog}
|
||||
|
||||
omit [Lattice L] in
|
||||
/-- Agda: `states-in-Map`. -/
|
||||
theorem states_memKey (s : prog.State) (sv : StateVariables L prog) :
|
||||
FiniteMap.MemKey s sv :=
|
||||
FiniteMap.memKey_iff.mpr (prog.states_complete s)
|
||||
|
||||
/-- Agda: `variablesAt`. -/
|
||||
def variablesAt (s : prog.State) (sv : StateVariables L prog) :
|
||||
VariableValues L prog :=
|
||||
(FiniteMap.locate (states_memKey s sv)).1
|
||||
|
||||
omit [Lattice L] in
|
||||
/-- Agda: `variablesAt-∈`. -/
|
||||
theorem variablesAt_mem (s : prog.State) (sv : StateVariables L prog) :
|
||||
(s, variablesAt s sv) ∈ sv :=
|
||||
(FiniteMap.locate (states_memKey s sv)).2
|
||||
|
||||
/-- Agda: `m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ`, specialized the way `Forward.agda` uses it. -/
|
||||
theorem variablesAt_le {sv₁ sv₂ : StateVariables L prog} (hle : sv₁ ≤ sv₂)
|
||||
(s : prog.State) : variablesAt s sv₁ ≤ variablesAt s sv₂ :=
|
||||
FiniteMap.le_of_mem_mem prog.states_nodup hle
|
||||
(variablesAt_mem s sv₁) (variablesAt_mem s sv₂)
|
||||
|
||||
variable (fhL : FixedHeight L h)
|
||||
|
||||
/-- Agda: `joinForKey`. -/
|
||||
def joinForKey (k : prog.State) (sv : StateVariables L prog) :
|
||||
VariableValues L prog :=
|
||||
(sv.valuesAt (prog.incoming k)).foldr (· ⊔ ·) (botV L prog fhL)
|
||||
|
||||
/-- Agda: `joinForKey-Mono`. -/
|
||||
theorem joinForKey_mono (k : prog.State) :
|
||||
Monotone (joinForKey fhL k) := by
|
||||
intro sv₁ sv₂ hle
|
||||
exact foldr_mono _ (FiniteMap.valuesAt_le hle (prog.incoming k)) (le_refl _)
|
||||
(fun b _ _ hab => sup_le_sup_right hab b)
|
||||
(fun a _ _ hab => sup_le_sup_left hab a)
|
||||
|
||||
/-- Agda: `joinAll` (the "Exercise 4.26" generalized update with `f = id`). -/
|
||||
def joinAll (sv : StateVariables L prog) : StateVariables L prog :=
|
||||
FiniteMap.generalizedUpdate id (joinForKey fhL) prog.states sv
|
||||
|
||||
/-- Agda: `joinAll-Mono`. -/
|
||||
theorem joinAll_mono : Monotone (joinAll (prog := prog) fhL) :=
|
||||
FiniteMap.generalizedUpdate_monotone monotone_id (joinForKey_mono fhL)
|
||||
|
||||
/-- Agda: `joinAll-k∈ks-≡`. -/
|
||||
theorem joinAll_mem_eq {s : prog.State} {vs : VariableValues L prog}
|
||||
{sv : StateVariables L prog} (h : (s, vs) ∈ joinAll fhL sv) :
|
||||
vs = joinForKey fhL s sv :=
|
||||
FiniteMap.generalizedUpdate_mem_eq (prog.states_complete s) h
|
||||
|
||||
/-- Agda: `variablesAt-joinAll`. -/
|
||||
theorem variablesAt_joinAll (s : prog.State) (sv : StateVariables L prog) :
|
||||
variablesAt s (joinAll fhL sv) = joinForKey fhL s sv :=
|
||||
joinAll_mem_eq fhL (variablesAt_mem s (joinAll fhL sv))
|
||||
|
||||
/-! ### Lifting an interpretation to variable maps -/
|
||||
|
||||
variable (I : LatticeInterpretation L)
|
||||
|
||||
/-- Agda: `⟦_⟧ᵛ`. -/
|
||||
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
|
||||
|
||||
/-- Agda: `⟦⊥ᵛ⟧ᵛ∅`. -/
|
||||
theorem interpV_botV_nil : interpV I (botV L prog fhL) [] := by
|
||||
intro k l _ v hmem
|
||||
cases hmem
|
||||
|
||||
/-- Agda: `⟦⟧ᵛ-⊔ᵛ-∨`. -/
|
||||
theorem interpV_sup {vs₁ vs₂ : VariableValues L prog} {ρ : Env}
|
||||
(h : interpV I vs₁ ρ ∨ interpV I vs₂ ρ) : interpV I (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))
|
||||
|
||||
/-- Agda: `⟦⟧ᵛ-foldr`. -/
|
||||
theorem interpV_foldr {vs : VariableValues L prog}
|
||||
{vss : List (VariableValues L prog)} {ρ : Env}
|
||||
(hvs : interpV I vs ρ) (hmem : vs ∈ vss) :
|
||||
interpV I (vss.foldr (· ⊔ ·) (botV L prog fhL)) ρ := by
|
||||
induction vss with
|
||||
| nil => cases hmem
|
||||
| cons vs' vss' ih =>
|
||||
rcases List.mem_cons.mp hmem with rfl | hmem'
|
||||
· exact interpV_sup I (Or.inl hvs)
|
||||
· exact interpV_sup I (Or.inr (ih hmem'))
|
||||
|
||||
end Spa
|
||||
Reference in New Issue
Block a user