diff --git a/lean/Spa/Analysis/Forward.lean b/lean/Spa/Analysis/Forward.lean index f1edba5..28c500f 100644 --- a/lean/Spa/Analysis/Forward.lean +++ b/lean/Spa/Analysis/Forward.lean @@ -1,30 +1,3 @@ -/- -Port of `Analysis/Forward.agda` (`WithProg`, `WithStmtEvaluator`, -`WithValidInterpretation`). - -As in Agda, the statement evaluator, the lattice interpretation and the -evaluator's validity proof are instance arguments (`{{evaluator}}`, -`{{latticeInterpretationˡ}}`, `{{validEvaluator}}`); `result` and -`analyze_correct` take `L` and `prog` explicitly, mirroring the Agda call -shape `WithProg.result L prog`. - -Correspondence: - updateVariablesForState, -Monoʳ ↦ updateVariablesForState, _mono - updateAll, updateAll-Mono, - updateAll-k∈ks-≡ ↦ updateAll, updateAll_mono, updateAll_mem_eq - analyze, analyze-Mono ↦ analyze, analyze_mono - result, result≈analyze-result ↦ result, result_eq - variablesAt-updateAll ↦ variablesAt_updateAll - eval-fold-valid ↦ eval_fold_valid - updateVariablesForState-matches ↦ updateVariablesForState_matches - updateAll-matches ↦ updateAll_matches - stepTrace ↦ stepTrace (the `subst`/`⟦⟧ᵛ-respects-≈ᵛ` - plumbing becomes plain rewriting with `=`) - walkTrace ↦ walkTrace - joinForKey-initialState-⊥ᵛ ↦ joinForKey_initialState - ⟦joinAll-initialState⟧ᵛ∅ ↦ interpV_joinForKey_initialState - analyze-correct ↦ analyze_correct --/ import Spa.Analysis.Forward.Lattices import Spa.Analysis.Forward.Evaluation import Spa.Analysis.Forward.Adapters @@ -34,70 +7,56 @@ namespace Spa variable {L : Type} [Lattice L] {prog : Program} [E : StmtEvaluator L prog] -/-- Agda: `updateVariablesForState`. -/ def updateVariablesForState (s : prog.State) (sv : StateVariables L prog) : VariableValues L prog := (prog.code s).foldl (fun vs bs => E.eval s bs vs) (variablesAt s sv) -/-- Agda: `updateVariablesForState-Monoʳ`. -/ theorem updateVariablesForState_mono (s : prog.State) : Monotone (updateVariablesForState (L := L) s) := fun _ _ hle => - foldl_mono' (prog.code s) _ (fun bs => E.eval_mono s bs) (variablesAt_le hle s) + foldl_mono' (prog.code s) _ (E.eval_mono s ·) (variablesAt_le hle s) -/-- Agda: `updateAll`. -/ def updateAll (sv : StateVariables L prog) : StateVariables L prog := - FiniteMap.generalizedUpdate id (fun s sv => updateVariablesForState s sv) + FiniteMap.generalizedUpdate id updateVariablesForState prog.states sv -/-- Agda: `updateAll-Mono`. -/ theorem updateAll_mono : Monotone (updateAll (L := L) (prog := prog)) := FiniteMap.generalizedUpdate_monotone monotone_id updateVariablesForState_mono -/-- Agda: `updateAll-k∈ks-≡`. -/ theorem updateAll_mem_eq {s : prog.State} {vs : VariableValues L prog} {sv : StateVariables L prog} (hmem : (s, vs) ∈ updateAll sv) : vs = updateVariablesForState s sv := FiniteMap.generalizedUpdate_mem_eq (prog.states_complete s) hmem -/-- Agda: `variablesAt-updateAll`. -/ theorem variablesAt_updateAll (s : prog.State) (sv : StateVariables L prog) : variablesAt s (updateAll sv) = updateVariablesForState s sv := updateAll_mem_eq (variablesAt_mem s (updateAll sv)) variable [FiniteHeightLattice L] -/-- Agda: `analyze`. -/ def analyze (sv : StateVariables L prog) : StateVariables L prog := updateAll (joinAll sv) -/-- Agda: `analyze-Mono`. -/ theorem analyze_mono : Monotone (analyze (L := L) (prog := prog)) := fun _ _ hle => updateAll_mono (joinAll_mono hle) variable [DecidableEq L] variable (L prog) in -/-- Agda: `result` (the least fixpoint of `analyze`). -/ def result : StateVariables L prog := Fixedpoint.aFix analyze analyze_mono variable (L prog) in -/-- Agda: `result≈analyze-result`. -/ theorem result_eq : result L prog = analyze (result L prog) := Fixedpoint.aFix_eq analyze analyze_mono -/-- Agda: `joinForKey-initialState-⊥ᵛ`. -/ theorem joinForKey_initialState : joinForKey prog.initialState (result L prog) = botV L prog := by rw [joinForKey, prog.incoming_initialState_eq_nil] rfl -/-! ### Semantic correctness (Agda: `WithValidInterpretation`) -/ - variable [I : LatticeInterpretation L] [V : ValidStmtEvaluator L prog] omit [FiniteHeightLattice L] [DecidableEq L] in -/-- Agda: `eval-fold-valid`. -/ theorem eval_fold_valid {s : prog.State} {bss : List BasicStmt} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env} (hbss : EvalBasicStmts ρ₁ bss ρ₂) (hvs : interpV vs ρ₁) : @@ -107,7 +66,6 @@ theorem eval_fold_valid {s : prog.State} {bss : List BasicStmt} | cons hbs _ ih => exact ih (ValidStmtEvaluator.valid hbs hvs) omit [FiniteHeightLattice L] [DecidableEq L] in -/-- Agda: `updateVariablesForState-matches`. -/ theorem updateVariablesForState_matches {s : prog.State} {sv : StateVariables L prog} {ρ₁ ρ₂ : Env} (hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂) @@ -116,7 +74,6 @@ theorem updateVariablesForState_matches {s : prog.State} eval_fold_valid hbss hvs omit [FiniteHeightLattice L] [DecidableEq L] in -/-- Agda: `updateAll-matches`. -/ theorem updateAll_matches {s : prog.State} {sv : StateVariables L prog} {ρ₁ ρ₂ : Env} (hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂) (hvs : interpV (variablesAt s sv) ρ₁) : @@ -124,7 +81,6 @@ theorem updateAll_matches {s : prog.State} {sv : StateVariables L prog} rw [variablesAt_updateAll] exact updateVariablesForState_matches hbss hvs -/-- Agda: `stepTrace`. -/ theorem stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env} (hjoin : interpV (joinForKey s₁ (result L prog)) ρ₁) (hbss : EvalBasicStmts ρ₁ (prog.code s₁) ρ₂) : @@ -134,7 +90,6 @@ theorem stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env} rw [variablesAt_joinAll] exact hjoin -/-- Agda: `walkTrace`. -/ theorem walkTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} (hjoin : interpV (joinForKey s₁ (result L prog)) ρ₁) (tr : Trace prog.graph s₁ s₂ ρ₁ ρ₂) : @@ -151,15 +106,12 @@ theorem walkTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} exact ih (interpV_foldr hstep hmem) omit V in -/-- Agda: `⟦joinAll-initialState⟧ᵛ∅`. -/ theorem interpV_joinForKey_initialState : interpV (joinForKey prog.initialState (result L prog)) [] := by rw [joinForKey_initialState] exact interpV_botV_nil variable (L prog) in -/-- Agda: `analyze-correct` — the analysis result at the final state soundly -describes every terminating execution of the program. -/ theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : interpV (variablesAt prog.finalState (result L prog)) ρ := walkTrace interpV_joinForKey_initialState (prog.trace hrun)