diff --git a/lean/Spa/Analysis/Constant.lean b/lean/Spa/Analysis/Constant.lean index 4270536..fca4896 100644 --- a/lean/Spa/Analysis/Constant.lean +++ b/lean/Spa/Analysis/Constant.lean @@ -137,12 +137,11 @@ theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : ⟦ 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} - (hr : Reaches (prog.trace hrun) s ρin ρout) : +theorem analyze_correct_at {s : prog.State} {ρin ρout : Env} + (hr : Reaches s ρin ρout) : ⟦ joinForKey s (result ConstLattice prog) ⟧ ρin ∧ ⟦ variablesAt s (result ConstLattice prog) ⟧ ρout := - Forward.analyze_correct_at ConstLattice prog hrun hr + Forward.analyze_correct_at ConstLattice prog hr end ConstAnalysis diff --git a/lean/Spa/Analysis/Forward.lean b/lean/Spa/Analysis/Forward.lean index 69c7984..81cbdd2 100644 --- a/lean/Spa/Analysis/Forward.lean +++ b/lean/Spa/Analysis/Forward.lean @@ -90,75 +90,54 @@ lemma stepTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} rw [variablesAt_joinAll] exact hjoin -/-- Soundness at *every* visited node: if the analysis result over-approximates the - incoming environment at the start of the trace, then at each node reached along the - 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₂ 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 => - 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 trₗ hjoin hnode - have hmem := FiniteMap.mem_valuesAt prog.states_nodup - (prog.mem_incoming_of_edge hedge) (variablesAt_mem _ (result L prog)) - simpa [Reaches.pre, Reaches.post, HAppend.hAppend] using - ih ((trₗ ++ hnode).addEdge hedge) - (interp_foldr (S.post_pre (trₗ ++ hnode) hedge hstep) hmem) +/-- Soundness propagates along an execution prefix: if the analysis is sound at + `s₂` for the run so far (`trₗ`), then it is sound wherever the further prefix + `mid` ends up. -/ +lemma walkPrefix : ∀ {s₂ s : prog.State} {ρ₂ ρin : Env} + (mid : Traceₗ prog.cfg s₂ s ρ₂ ρin) {s₁ : prog.State} {ρ₁ : Env} + (trₗ : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂), + ⟦ joinForKey s₂ (result L prog) ⟧ (S.Pre trₗ) → + ⟦ joinForKey s (result L prog) ⟧ (S.Pre (trₗ ++ mid)) := by + intro s₂ s ρ₂ ρin mid + induction mid with + | nil => intro s₁ ρ₁ trₗ hjoin; simpa [HAppend.hAppend, Traceₗ.append] using hjoin + | cons hnode hedge rest ih => + intro s₁ ρ₁ trₗ hjoin + 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)) + simpa [HAppend.hAppend, Traceₗ.append] 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`. -/ -def reaches_final {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} - (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) : - Σ ρ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'⟩ + ends in. Used to recover the final-state soundness theorem from `walkPrefix`. -/ +def reaches_final {s : prog.State} {ρ : Env} + (tr : Trace prog.cfg prog.initialState s [] ρ) : Σ ρin, Reaches s ρin ρ := + ⟨_, ⟨tr.split.2.1, tr.split.2.2⟩⟩ omit [DecidableEq L] in -/-- Reaching the final node covers the whole trace. -/ -@[simp] lemma reaches_final_post {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} - (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) : - (reaches_final tr).2.post = tr := by - induction tr with - | single hnode => rfl - | edge hnode hedge rest ih => simp [reaches_final, Reaches.post, ih] +@[simp] lemma reaches_final_post {s : prog.State} {ρ : Env} + (tr : Trace prog.cfg prog.initialState s [] ρ) : + (reaches_final tr).2.post = tr := Trace.split_append tr variable (L prog) in -/-- Soundness at every program point reached during execution: for any node `s` visited - by the run `hrun` (witnessed by `hr`), the analysis result over-approximates both the - 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} - (hr : Reaches (prog.trace hrun) s ρin ρout) : +/-- Soundness at every program point an execution actually visits: the analysis + over-approximates both the environment entering that point and the one leaving + it. -/ +theorem analyze_correct_at {s : prog.State} {ρin ρout : Env} (hr : Reaches 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 + ∧ ⟦ variablesAt s (result L prog) ⟧ (S.Post hr.post) := + have hpre := walkPrefix hr.pre Traceₗ.nil + (by rw [joinForKey_initialState]; exact ValidStateEvaluator.botV_init) + ⟨hpre, stepTrace hr.pre hpre hr.step⟩ variable (L prog) in theorem analyze_correct' {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : ⟦ variablesAt prog.finalState (result L prog) ⟧ (S.Post (prog.trace hrun)) := by - have h := (analyze_correct_at L prog hrun (reaches_final (prog.trace hrun)).2).2 + have h := (analyze_correct_at L prog (reaches_final (prog.trace hrun)).2).2 rwa [reaches_final_post] at h end diff --git a/lean/Spa/Analysis/Reaching.lean b/lean/Spa/Analysis/Reaching.lean index cdf0400..1a43354 100644 --- a/lean/Spa/Analysis/Reaching.lean +++ b/lean/Spa/Analysis/Reaching.lean @@ -118,12 +118,11 @@ theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : (runOfTrace prog (prog.trace hrun)) := Forward.analyze_correct' (DefSet prog) prog hrun -theorem analyze_correct_at {ρf : Env} (hrun : EvalStmt [] prog.rootStmt ρf) - {s : prog.State} {ρin ρout : Env} - (hr : Reaches (prog.trace hrun) s ρin ρout) : +theorem analyze_correct_at {s : prog.State} {ρin ρout : Env} + (hr : Reaches s ρin ρout) : ⟦ joinForKey s (result (DefSet prog) prog) ⟧ (runOfTraceₗ prog hr.pre) ∧ ⟦ variablesAt s (result (DefSet prog) prog) ⟧ (runOfTrace prog hr.post) := - Forward.analyze_correct_at (DefSet prog) prog hrun hr + Forward.analyze_correct_at (DefSet prog) prog hr end ReachingAnalysis diff --git a/lean/Spa/Analysis/Sign.lean b/lean/Spa/Analysis/Sign.lean index 02aa356..0c35674 100644 --- a/lean/Spa/Analysis/Sign.lean +++ b/lean/Spa/Analysis/Sign.lean @@ -228,12 +228,11 @@ theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : ⟦ 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} - (hr : Reaches (prog.trace hrun) s ρin ρout) : +theorem analyze_correct_at {s : prog.State} {ρin ρout : Env} + (hr : Reaches s ρin ρout) : ⟦ joinForKey s (result SignLattice prog) ⟧ ρin ∧ ⟦ variablesAt s (result SignLattice prog) ⟧ ρout := - Forward.analyze_correct_at SignLattice prog hrun hr + Forward.analyze_correct_at SignLattice prog hr end SignAnalysis diff --git a/lean/Spa/Language/Traces.lean b/lean/Spa/Language/Traces.lean index c2a68f7..2c8e779 100644 --- a/lean/Spa/Language/Traces.lean +++ b/lean/Spa/Language/Traces.lean @@ -217,50 +217,30 @@ inductive EndToEndTrace (g : Graph) (ρ₁ ρ₂ : Env) : Type (idx₂ : g.Index) (idx₂_mem : idx₂ ∈ g.outputs) (trace : Trace g idx₁ idx₂ ρ₁ ρ₂) : EndToEndTrace g ρ₁ ρ₂ -inductive Reaches {prog : Program} : {s₁ s₂ : prog.State} → {ρ₁ ρ₂ : Env} → - Trace prog.cfg s₁ s₂ ρ₁ ρ₂ → - (s : prog.State) → (ρin ρout : Env) → Type - | single_here {s₁ : prog.State} {ρ₁ ρ₂ : Env} - (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂) : - Reaches (.single hnode) s₁ ρ₁ ρ₂ - | edge_here {s₁ s₂ s₃ : prog.State} {ρ₁ ρ₂ ρ₃ : Env} - (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂) - (hedge : (s₁, s₂) ∈ prog.cfg.edges) (rest : Trace prog.cfg s₂ s₃ ρ₂ ρ₃) : - Reaches (.edge hnode hedge rest) s₁ ρ₁ ρ₂ - | edge_there {s₁ s₂ s₃ : prog.State} {ρ₁ ρ₂ ρ₃ : Env} - (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂) - (hedge : (s₁, s₂) ∈ prog.cfg.edges) (rest : Trace prog.cfg s₂ s₃ ρ₂ ρ₃) - {s : prog.State} {ρin ρout : Env} : - Reaches rest s ρin ρout → - Reaches (.edge hnode hedge rest) s ρin ρout +/-- Every trace splits into the prefix that arrives at its last node and that node's own step. -/ +def Trace.split {g : Graph} {i₁ i₂ : g.Index} {ρ₁ ρ₂ : Env} : + Trace g i₁ i₂ ρ₁ ρ₂ → Σ ρ, Traceₗ g i₁ i₂ ρ₁ ρ × EvalBasicStmtOpt ρ (g.nodes i₂) ρ₂ + | .single hnode => ⟨_, .nil, hnode⟩ + | .edge hnode hedge rest => + let ⟨ρ, pre, step⟩ := rest.split + ⟨ρ, .cons hnode hedge pre, step⟩ -def Reaches.pre {prog : Program} {s₁ s₂ s: prog.State} - {ρ₁ ρ₂ ρin ρout : Env} {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} : - (r : Reaches tr s ρin ρout) → Traceₗ prog.cfg s₁ s ρ₁ ρin - | .single_here _ => .nil - | .edge_here _ _ _ => .nil - | .edge_there hnode hedge _ r => .cons hnode hedge r.pre +@[simp] lemma Trace.split_append {g : Graph} {i₁ i₂ : g.Index} {ρ₁ ρ₂ : Env} + (tr : Trace g i₁ i₂ ρ₁ ρ₂) : tr.split.2.1 ++ tr.split.2.2 = tr := by + induction tr with + | single hnode => rfl + | edge hnode hedge rest ih => + show Traceₗ.appendStep _ _ = _ + simpa [Trace.split, Traceₗ.appendStep, Traceₗ.appendTrace] using ih -def Reaches.post {prog : Program} {s₁ s₂ s: prog.State} - {ρ₁ ρ₂ ρin ρout : Env} {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} : - (r : Reaches tr s ρin ρout) → Trace prog.cfg s₁ s ρ₁ ρout - | .single_here hnode => .single hnode - | .edge_here hnode _ _ => .single hnode - | .edge_there hnode hedge _ r => .edge hnode hedge r.post +structure Reaches {prog : Program} (s : prog.State) (ρin ρout : Env) : Type where + pre : Traceₗ prog.cfg prog.initialState s [] ρin + step : EvalBasicStmtOpt ρin (prog.code s) ρout -def Reaches.first {prog : Program} {s₁ s₂ s: prog.State} - {ρ₁ ρ₂ ρin ρout : Env} {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} : - (r : Reaches tr s ρin ρout) → Σ ρ₁', Reaches tr s₁ ρ₁ ρ₁' - | .single_here hnode => ⟨_, .single_here hnode⟩ - | .edge_here hnode hedge hrest => ⟨_, .edge_here hnode hedge hrest⟩ - | .edge_there hnode hedge hrest tmp' => ⟨_, .edge_here hnode hedge hrest⟩ - -def Reaches.step {prog : Program} {s₁ s₂ s: prog.State} - {ρ₁ ρ₂ ρin ρout : Env} {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} : - (r : Reaches tr s ρin ρout) → EvalBasicStmtOpt ρin (prog.code s) ρout - | .single_here hnode => hnode - | .edge_here hnode hedge hrest => hnode - | .edge_there hnode hedge hrest tmp' => tmp'.step +/-- Forget the environment before the last evaluated state. -/ +def Reaches.post {prog : Program} {s : prog.State} {ρin ρout : Env} + (r : Reaches s ρin ρout) : Trace prog.cfg prog.initialState s [] ρout := + r.pre ++ r.step end Spa