From 0e6976f9b4823629f9cb240537489cead35d1bc2 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Wed, 1 Jul 2026 22:56:29 -0500 Subject: [PATCH] Migrate most of the codebase (sans Reaching.lean / LICM left) to projections --- lean/Spa/Analysis/Constant.lean | 10 +- lean/Spa/Analysis/Forward.lean | 155 +++++++++------------- lean/Spa/Analysis/Forward/Evaluation.lean | 4 +- lean/Spa/Analysis/Forward/Lattices.lean | 40 +++--- lean/Spa/Analysis/Sign.lean | 10 +- lean/Spa/Language/Program.lean | 1 + lean/Spa/Language/Traces.lean | 55 +++++--- 7 files changed, 139 insertions(+), 136 deletions(-) diff --git a/lean/Spa/Analysis/Constant.lean b/lean/Spa/Analysis/Constant.lean index d9960aa..4270536 100644 --- a/lean/Spa/Analysis/Constant.lean +++ b/lean/Spa/Analysis/Constant.lean @@ -134,14 +134,14 @@ instance eval_valid : ValidExprEvaluator ConstLattice prog := by exact minus_valid h₁ h₂ theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : - ⟦ variablesAt prog.finalState (result ConstLattice prog) ⟧ ρ () := + ⟦ 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} {stin stout : PUnit} - (hr : Reaches (L := ConstLattice) (prog.trace hrun) PUnit.unit s ρin ρout stin stout) : - ⟦ joinForKey s (result ConstLattice prog) ⟧ ρin stin - ∧ ⟦ variablesAt s (result ConstLattice prog) ⟧ ρout stout := + {s : prog.State} {ρin ρout : Env} + (hr : Reaches (prog.trace hrun) s ρin ρout) : + ⟦ joinForKey s (result ConstLattice prog) ⟧ ρin + ∧ ⟦ variablesAt s (result ConstLattice prog) ⟧ ρout := Forward.analyze_correct_at ConstLattice prog hrun hr end ConstAnalysis diff --git a/lean/Spa/Analysis/Forward.lean b/lean/Spa/Analysis/Forward.lean index 28961cf..63efeb8 100644 --- a/lean/Spa/Analysis/Forward.lean +++ b/lean/Spa/Analysis/Forward.lean @@ -55,70 +55,38 @@ lemma joinForKey_initialState : class ValidStateEvaluator (L : Type) [FiniteHeightLattice L] (prog : Program) [E : StmtEvaluator L prog] [S : StateInterpretation L prog] where - step : (s : prog.State) → {ρ₁ ρ₂ : Env} → EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂ → S.St ρ₁ → S.St ρ₂ - valid : ∀ (s : prog.State) {ρ₁ ρ₂ : Env} - {vs : VariableValues L prog} {st : S.St ρ₁}, - (hbs : EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂) → ⟦ vs ⟧ ρ₁ st → - ⟦ E.eval s vs ⟧ ρ₂ (step s hbs st) - botV_init : ⟦ botV L prog ⟧ [] S.init + valid : ∀ (s₁ s₂ : prog.State) {ρ₁ ρ₂ ρ₃: Env} + {vs : VariableValues L prog}, + (tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂) → + (hbs : EvalBasicStmtOpt ρ₂ (prog.cfg.nodes s₂) ρ₃) → ⟦ vs ⟧ (S.Pre tr) → + ⟦ E.eval s₂ vs ⟧ (S.Post (tr ++ hbs)) + botV_init : ⟦ botV L prog ⟧ (S.Pre (Traceₗ.single prog.cfg prog.initialState [])) instance [LatticeInterpretation L] [ValidStmtEvaluator L prog] : ValidStateEvaluator L prog where - step := by intro _ _ _ _ _; exact PUnit.unit - valid := by intro _ _ _ _ _ hbs hvs; exact ValidStmtEvaluator.valid hbs hvs + valid := by intro _ _ _ _ _ _ tr hbs hvs; exact ValidStmtEvaluator.valid hbs hvs botV_init := by intro k l _ v hmem; cases hmem section variable [S : StateInterpretation L prog] [V : ValidStateEvaluator L prog] -noncomputable def stepNode (s : prog.State) {ρ₁ ρ₂ : Env} - (h : EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂) (st : S.St ρ₁) : S.St ρ₂ := - V.step s h st - -noncomputable def stepTraceState : - {s₁ s₂ : prog.State} → {ρ₁ ρ₂ : Env} → - Trace prog.cfg s₁ s₂ ρ₁ ρ₂ → S.St ρ₁ → S.St ρ₂ - | s₁, _, _, _, .single hnode, st => stepNode s₁ hnode st - | s₁, _, _, _, .edge hnode _ subtr, st => - stepTraceState subtr (stepNode s₁ hnode st) - -/-- `Reaches tr st₁ s ρin ρout stin stout` witnesses that, when the trace `tr` - (starting at state `st₁`) is executed, node `s` is visited at some point: `ρin` - and `ρout` are the concrete environments just before and after `s`'s basic block - runs, and `stin`/`stout` are the corresponding abstract execution states. A node - inside a loop is reached once per iteration, each with its own environments. -/ -inductive Reaches : {s₁ s₂ : prog.State} → {ρ₁ ρ₂ : Env} → - Trace prog.cfg s₁ s₂ ρ₁ ρ₂ → S.St ρ₁ → - (s : prog.State) → (ρin ρout : Env) → S.St ρin → S.St ρout → Prop - | single_here {s₁ : prog.State} {ρ₁ ρ₂ : Env} {st₁ : S.St ρ₁} - (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂) : - Reaches (.single hnode) st₁ s₁ ρ₁ ρ₂ st₁ (stepNode s₁ hnode st₁) - | edge_here {s₁ s₂ s₃ : prog.State} {ρ₁ ρ₂ ρ₃ : Env} {st₁ : S.St ρ₁} - (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂) - (hedge : (s₁, s₂) ∈ prog.cfg.edges) (rest : Trace prog.cfg s₂ s₃ ρ₂ ρ₃) : - Reaches (.edge hnode hedge rest) st₁ s₁ ρ₁ ρ₂ st₁ (stepNode s₁ hnode st₁) - | edge_there {s₁ s₂ s₃ : prog.State} {ρ₁ ρ₂ ρ₃ : Env} {st₁ : S.St ρ₁} - (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂) - (hedge : (s₁, s₂) ∈ prog.cfg.edges) (rest : Trace prog.cfg s₂ s₃ ρ₂ ρ₃) - {s : prog.State} {ρin ρout : Env} {stin : S.St ρin} {stout : S.St ρout} : - Reaches rest (stepNode s₁ hnode st₁) s ρin ρout stin stout → - Reaches (.edge hnode hedge rest) st₁ s ρin ρout stin stout - omit [DecidableEq L] in -lemma updateAll_matches {s : prog.State} {sv : StateVariables L prog} - {ρ₁ ρ₂ : Env} {st : S.St ρ₁} - (hnode : EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂) - (hvs : ⟦ variablesAt s sv ⟧ ρ₁ st) : - ⟦ variablesAt s (updateAll sv) ⟧ ρ₂ (stepNode s hnode st) := by +lemma updateAll_matches {s₁ s₂ : prog.State} {sv : StateVariables L prog} + {ρ₁ ρ₂ ρ₃ : Env} + (tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂) + (hnode : EvalBasicStmtOpt ρ₂ (prog.code s₂) ρ₃) + (hvs : ⟦ variablesAt s₂ sv ⟧ (S.Pre tr)) : + ⟦ variablesAt s₂ (updateAll sv) ⟧ (S.Post (tr ++ hnode)) := by rw [variablesAt_updateAll] - exact V.valid s hnode hvs + exact V.valid s₁ s₂ tr hnode hvs -lemma stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env} {st : S.St ρ₁} - (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁ st) - (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂) : - ⟦ variablesAt s₁ (result L prog) ⟧ ρ₂ (stepNode s₁ hnode st) := by +lemma stepTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} + (tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂) + (hjoin : ⟦ joinForKey s₂ (result L prog) ⟧ (S.Pre tr)) + (hnode : EvalBasicStmtOpt ρ₂ (prog.code s₂) ρ₃) : + ⟦ variablesAt s₂ (result L prog) ⟧ (S.Post (tr ++ hnode)) := by rw [result_eq L prog] - refine updateAll_matches hnode ?_ + refine updateAll_matches tr hnode ?_ rw [variablesAt_joinAll] exact hjoin @@ -127,49 +95,41 @@ lemma stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env} {st : S.St ρ₁} 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₂ : prog.State} {ρ₁ ρ₂ : Env} {st₁ : S.St ρ₁} - {s : prog.State} {ρin ρout : Env} {stin : S.St ρin} {stout : S.St ρout} - {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} - (hr : Reaches tr st₁ s ρin ρout stin stout) - (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁ st₁) : - ⟦ joinForKey s (result L prog) ⟧ ρin stin - ∧ ⟦ variablesAt s (result L prog) ⟧ ρout stout := by +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 => exact ⟨hjoin, stepTrace hjoin hnode⟩ - | edge_here hnode hedge rest => exact ⟨hjoin, stepTrace hjoin hnode⟩ + | 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 hjoin hnode + 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)) - exact ih (interp_foldr hstep hmem) + simpa [Reaches.pre, Reaches.post, HAppend.hAppend] 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`. -/ -lemma reaches_final {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} (st₁ : S.St ρ₁) +def reaches_final {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) : - ∃ ρin, ∃ stin : S.St ρin, - Reaches tr st₁ s₂ ρin ρ₂ stin (stepTraceState tr st₁) := by - induction tr with - | single hnode => exact ⟨_, _, .single_here hnode⟩ - | edge hnode hedge rest ih => - obtain ⟨ρin, stin, hr⟩ := ih (stepNode _ hnode st₁) - exact ⟨ρin, stin, .edge_there hnode hedge rest hr⟩ - -lemma walkTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} {st₁ : S.St ρ₁} - (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁ st₁) - (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) : - ⟦ variablesAt s₂ (result L prog) ⟧ ρ₂ (stepTraceState tr st₁) := by - obtain ⟨_, _, hr⟩ := reaches_final st₁ tr - exact (walkTrace_reaches hr hjoin).2 - -variable (L prog) in -theorem analyze_correct_state {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : - ⟦ variablesAt prog.finalState (result L prog) ⟧ ρ - (stepTraceState (prog.trace hrun) S.init) := by - refine walkTrace ?_ (prog.trace hrun) - rw [joinForKey_initialState] - exact ValidStateEvaluator.botV_init + Σ ρ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'⟩ variable (L prog) in /-- Soundness at every program point reached during execution: for any node `s` visited @@ -177,21 +137,30 @@ variable (L prog) in 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} {stin : S.St ρin} {stout : S.St ρout} - (hr : Reaches (prog.trace hrun) S.init s ρin ρout stin stout) : - ⟦ joinForKey s (result L prog) ⟧ ρin stin - ∧ ⟦ variablesAt s (result L prog) ⟧ ρout stout := by - refine walkTrace_reaches hr ?_ + {s : prog.State} {ρin ρout : Env} + (hr : Reaches (prog.trace hrun) 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 +variable (L prog) in +theorem analyze_correct' + {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : + ⟦ variablesAt prog.finalState (result L prog) ⟧ (S.Post (reaches_final (prog.trace hrun)).2.post) := by + let idk₀ := prog.trace hrun + have ⟨_, idk₁⟩ := reaches_final idk₀ + have ⟨_, idk₂⟩ := analyze_correct_at L prog hrun idk₁ + assumption + end variable (L prog) in theorem analyze_correct [LatticeInterpretation L] [ValidStmtEvaluator L prog] {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : - ⟦ variablesAt prog.finalState (result L prog) ⟧ ρ () := - analyze_correct_state L prog hrun + ⟦ variablesAt prog.finalState (result L prog) ⟧ ρ := + analyze_correct' L prog hrun end Forward diff --git a/lean/Spa/Analysis/Forward/Evaluation.lean b/lean/Spa/Analysis/Forward/Evaluation.lean index b248cd2..aff8283 100644 --- a/lean/Spa/Analysis/Forward/Evaluation.lean +++ b/lean/Spa/Analysis/Forward/Evaluation.lean @@ -17,12 +17,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 → ⟦ 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}, - EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂ → ⟦ vs ⟧ ρ₁ () → ⟦ E.eval s vs ⟧ ρ₂ () + EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂ → ⟦ vs ⟧ ρ₁ → ⟦ E.eval s vs ⟧ ρ₂ end Forward diff --git a/lean/Spa/Analysis/Forward/Lattices.lean b/lean/Spa/Analysis/Forward/Lattices.lean index 5234b1a..926f516 100644 --- a/lean/Spa/Analysis/Forward/Lattices.lean +++ b/lean/Spa/Analysis/Forward/Lattices.lean @@ -65,22 +65,28 @@ lemma variablesAt_joinAll (s : prog.State) (sv : StateVariables L prog) : joinAll_mem_eq (variablesAt_mem s (joinAll sv)) class StateInterpretation (L : Type) [Lattice L] (prog : Program) where - St : Env → Type - init : St [] - interp : VariableValues L prog → (ρ : Env) → St ρ → Prop - interp_sup : ∀ {vs₁ vs₂ : VariableValues L prog} {ρ : Env} {st : St ρ}, - interp vs₁ ρ st ∨ interp vs₂ ρ st → interp (vs₁ ⊔ vs₂) ρ st - interp_inf : ∀ {vs₁ vs₂ : VariableValues L prog} {ρ : Env} {st : St ρ}, - interp vs₁ ρ st ∧ interp vs₂ ρ st → interp (vs₁ ⊓ vs₂) ρ st + Proj : Type + Pre : ∀ {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}, Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂ → Proj + Post : ∀ {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}, Trace prog.cfg s₁ s₂ ρ₁ ρ₂ → Proj + + interp : VariableValues L prog → (p : Proj) → Prop + interp_sup : ∀ {vs₁ vs₂ : VariableValues L prog} {p : Proj}, + interp vs₁ p ∨ interp vs₂ p → interp (vs₁ ⊔ vs₂) p + interp_inf : ∀ {vs₁ vs₂ : VariableValues L prog} {p : Proj}, + interp vs₁ p ∧ interp vs₂ p → interp (vs₁ ⊓ vs₂) p + + post_pre : ∀ {vs} {s₁ s₂ s₃: prog.State} {ρ₁ ρ₂ : Env} + (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) (hedge : (s₂, s₃) ∈ prog.cfg.edges), + interp vs (Post tr) → interp vs (Pre (tr.addEdge hedge)) instance [S : StateInterpretation L prog] : - Interp (VariableValues L prog) ((ρ : Env) → S.St ρ → Prop) := + Interp (VariableValues L prog) (S.Proj → Prop) := ⟨S.interp⟩ lemma interp_foldr [S : StateInterpretation L prog] {vs : VariableValues L prog} {vss : List (VariableValues L prog)} - {ρ : Env} {st : S.St ρ} (hvs : ⟦ vs ⟧ ρ st) (hmem : vs ∈ vss) : - ⟦ vss.foldr (· ⊔ ·) (botV L prog) ⟧ ρ st := by + {p : S.Proj} (hvs : ⟦ vs ⟧ p) (hmem : vs ∈ vss) : + ⟦ vss.foldr (· ⊔ ·) (botV L prog) ⟧ p := by induction vss with | nil => cases hmem | cons vs' vss' ih => @@ -91,20 +97,24 @@ lemma interp_foldr [S : StateInterpretation L prog] variable [I : LatticeInterpretation L] instance : StateInterpretation L prog where - St := fun _ => PUnit - init := PUnit.unit - interp vs ρ _ := ∀ (k : String) (l : L), (k, l) ∈ vs → + Proj := Env + Pre := fun {_ _ _ ρ₂} _ => ρ₂ + Post := fun {_ _ _ ρ₂} _ => ρ₂ + + interp vs ρ := ∀ (k : String) (l : L), (k, l) ∈ vs → ∀ (v : Value), Env.Mem (k, v) ρ → I.interp l v interp_sup := by - intro vs₁ vs₂ ρ st h k l hmem v hv + intro vs₁ vs₂ ρ h 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)) interp_inf := by - intro vs₁ vs₂ ρ st h k l hmem v hv + intro vs₁ vs₂ ρ h k l hmem v hv obtain ⟨l₁, l₂, rfl, h₁, h₂⟩ := FiniteMap.mem_inf hmem exact I.interp_inf v ⟨h.1 _ _ h₁ _ hv, h.2 _ _ h₂ _ hv⟩ + post_pre := by simp + end Forward diff --git a/lean/Spa/Analysis/Sign.lean b/lean/Spa/Analysis/Sign.lean index 16a9e51..bc69ced 100644 --- a/lean/Spa/Analysis/Sign.lean +++ b/lean/Spa/Analysis/Sign.lean @@ -210,14 +210,14 @@ instance eval_valid : ValidExprEvaluator SignLattice prog := by exact minus_valid h₁ h₂ theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : - ⟦ variablesAt prog.finalState (result SignLattice prog) ⟧ ρ () := + ⟦ 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} {stin stout : PUnit} - (hr : Reaches (L := SignLattice) (prog.trace hrun) PUnit.unit s ρin ρout stin stout) : - ⟦ joinForKey s (result SignLattice prog) ⟧ ρin stin - ∧ ⟦ variablesAt s (result SignLattice prog) ⟧ ρout stout := + {s : prog.State} {ρin ρout : Env} + (hr : Reaches (prog.trace hrun) s ρin ρout) : + ⟦ joinForKey s (result SignLattice prog) ⟧ ρin + ∧ ⟦ variablesAt s (result SignLattice prog) ⟧ ρout := Forward.analyze_correct_at SignLattice prog hrun hr end SignAnalysis diff --git a/lean/Spa/Language/Program.lean b/lean/Spa/Language/Program.lean index 935aa39..854a146 100644 --- a/lean/Spa/Language/Program.lean +++ b/lean/Spa/Language/Program.lean @@ -50,6 +50,7 @@ lemma states_nodup : p.states.Nodup := p.cfg.nodup_indices At this time, for convenience of proofs, the CFGs have at most one basic statement, and multi-statement basic blocks are encoded as chains of blocks. Thus, this returns at most one `Spa.BasicStmt`. -/ +@[reducible] def code (st : p.State) : Option BasicStmt := p.cfg.nodes st /-- Get the predecessors of a particular CFG node / program state. -/ diff --git a/lean/Spa/Language/Traces.lean b/lean/Spa/Language/Traces.lean index a5afb6b..69008e8 100644 --- a/lean/Spa/Language/Traces.lean +++ b/lean/Spa/Language/Traces.lean @@ -93,12 +93,17 @@ def Trace.addEdge {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ : En | .single hnode, hedge => .cons hnode hedge .nil | .edge hnode hedge' rest, hedge => .cons hnode hedge' (rest.addEdge hedge) +@[aesop simp] def Traceₗ.append {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} : Traceₗ g idx₁ idx₂ ρ₁ ρ₂ → Traceₗ g idx₂ idx₃ ρ₂ ρ₃ → Traceₗ g idx₁ idx₃ ρ₁ ρ₃ | .nil, rhs => rhs | .cons hnode hedge rest, rhs => .cons hnode hedge (rest.append rhs) +@[simp] def traceₗ_append_nil {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ : Env} + {trₗ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂} : trₗ.append Traceₗ.nil = trₗ := by + induction trₗ <;> aesop + def Traceₗ.appendTrace {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} : Traceₗ g idx₁ idx₂ ρ₁ ρ₂ → Trace g idx₂ idx₃ ρ₂ ρ₃ → Trace g idx₁ idx₃ ρ₁ ρ₃ @@ -107,9 +112,7 @@ def Traceₗ.appendTrace {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ def Traceₗ.appendStep {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} : Traceₗ g idx₁ idx₂ ρ₁ ρ₂ → EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃ → - Trace g idx₁ idx₂ ρ₁ ρ₃ - | .nil, rhs => .single rhs - | .cons hnode hedge rest, rhs => .edge hnode hedge (rest.appendStep rhs) + Trace g idx₁ idx₂ ρ₁ ρ₃ := fun trₗ hbs => trₗ.appendTrace (Trace.single hbs) def Trace.appendRight {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} : Trace g idx₁ idx₂ ρ₁ ρ₂ → Traceᵣ g idx₂ idx₃ ρ₂ ρ₃ → @@ -133,53 +136,73 @@ instance instHAppendTraceTraceR {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ HAppend (Trace g idx₁ idx₂ ρ₁ ρ₂) (Traceᵣ g idx₂ idx₃ ρ₂ ρ₃) (Trace g idx₁ idx₃ ρ₁ ρ₃) where hAppend := Trace.appendRight +@[simp] lemma Traceₗ.append_addEdge {g : Graph} + {idx₁ idx₂ idx₃ idx₄ : g.Index} {ρ₁ ρ₂ ρ₃ ρ₄ : Env} + (trₗ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂) + (hnode : EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃) + (hedge : (idx₂, idx₃) ∈ g.edges) + (rest : Traceₗ g idx₃ idx₄ ρ₃ ρ₄) : + trₗ.append (Traceₗ.cons hnode hedge rest) = + (Trace.addEdge (trₗ.appendStep hnode) hedge).append rest := by + induction trₗ <;> simp [Traceₗ.append, Traceₗ.appendStep, Traceₗ.appendTrace, Trace.addEdge, *] + +@[simp] lemma Traceₗ.appendTrace_addEdge {g : Graph} + {idx₁ idx₂ idx₃ idx₄ : g.Index} {ρ₁ ρ₂ ρ₃ ρ₄ : Env} + (trₗ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂) + (hnode : EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃) + (hedge : (idx₂, idx₃) ∈ g.edges) + (rest : Trace g idx₃ idx₄ ρ₃ ρ₄) : + trₗ.appendTrace (Trace.edge hnode hedge rest) = + (Trace.addEdge (trₗ.appendStep hnode) hedge).appendTrace rest := by + induction trₗ <;> simp [Traceₗ.appendTrace, Traceₗ.appendStep, Trace.addEdge, *] + /-- A beginning-to-end trace corresponding to the CFG `g`. -/ inductive EndToEndTrace (g : Graph) (ρ₁ ρ₂ : Env) : Type | intro (idx₁ : g.Index) (idx₁_mem : idx₁ ∈ g.inputs) (idx₂ : g.Index) (idx₂_mem : idx₂ ∈ g.outputs) (trace : Trace g idx₁ idx₂ ρ₁ ρ₂) : EndToEndTrace g ρ₁ ρ₂ -inductive MyReaches {prog : Program} : {s₁ s₂ : prog.State} → {ρ₁ ρ₂ : Env} → +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₁) ρ₂) : - MyReaches (.single hnode) 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₃ ρ₂ ρ₃) : - MyReaches (.edge hnode hedge rest) 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} : - MyReaches rest s ρin ρout → - MyReaches (.edge hnode hedge rest) s ρin ρout + Reaches rest s ρin ρout → + Reaches (.edge hnode hedge rest) s ρin ρout -def MyReaches.pre {prog : Program} {s₁ s₂ s: prog.State} +def Reaches.pre {prog : Program} {s₁ s₂ s: prog.State} {ρ₁ ρ₂ ρin ρout : Env} {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} : - (r : MyReaches tr s ρin ρout) → Traceₗ prog.cfg s₁ s ρ₁ ρin + (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 -def MyReaches.post {prog : Program} {s₁ s₂ s: prog.State} +def Reaches.post {prog : Program} {s₁ s₂ s: prog.State} {ρ₁ ρ₂ ρin ρout : Env} {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} : - (r : MyReaches tr s ρin ρout) → Trace prog.cfg s₁ s ρ₁ ρout + (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 -def MyReaches.first {prog : Program} {s₁ s₂ s: prog.State} +def Reaches.first {prog : Program} {s₁ s₂ s: prog.State} {ρ₁ ρ₂ ρin ρout : Env} {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} : - (r : MyReaches tr s ρin ρout) → Σ ρ₁', MyReaches tr 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 MyReaches.step {prog : Program} {s₁ s₂ s: prog.State} +def Reaches.step {prog : Program} {s₁ s₂ s: prog.State} {ρ₁ ρ₂ ρin ρout : Env} {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} : - (r : MyReaches tr s ρin ρout) → EvalBasicStmtOpt ρin (prog.code s) ρout + (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