Danila Fedorin
b6b30958aa
This requires a few pieces: * Make node tags use `Fin n` intead of natural numbers. This makes it possible to build a finite lattice over AST nodes, and also ensure automatic, total indexing from CFG nodes into the AST that created them. For this, use the elaborator to derive the ordering statements etc. where possible. * Adjust the forward framework to enable proofs that don't just state correctness on the environment, but also on an arbitrary additional state accumulated from traversing the trace. * State the reaching definition analysis's correctness in terms of this new framework. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
59 lines
1.6 KiB
Lean4
59 lines
1.6 KiB
Lean4
import Spa.Language.Base
|
||
import Spa.Language.Semantics
|
||
import Spa.Language.Graphs
|
||
import Spa.Language.Traces
|
||
import Spa.Language.Properties
|
||
import Mathlib.Data.Finset.Sort
|
||
import Mathlib.Data.String.Basic
|
||
|
||
namespace Spa
|
||
|
||
structure Program where
|
||
rootStmt : Stmt
|
||
|
||
namespace Program
|
||
|
||
variable (p : Program)
|
||
|
||
def cfg : Graph := Graph.wrap p.rootStmt.cfg
|
||
|
||
abbrev State : Type := p.cfg.Index
|
||
|
||
def initialState : p.State := p.rootStmt.cfg.wrapInput
|
||
|
||
def finalState : p.State := p.rootStmt.cfg.wrapOutput
|
||
|
||
noncomputable def trace {ρ : Env} (h : EvalStmt [] p.rootStmt ρ) :
|
||
Trace p.cfg p.initialState p.finalState [] ρ := by
|
||
obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := EndToEndTrace.wrap (Stmt.cfg_sufficient h)
|
||
rw [Graph.wrap_inputs, List.mem_singleton] at h₁
|
||
rw [Graph.wrap_outputs, List.mem_singleton] at h₂
|
||
subst h₁; subst h₂
|
||
exact tr
|
||
|
||
def vars : List String := p.rootStmt.vars.sort (· ≤ ·)
|
||
|
||
lemma vars_nodup : p.vars.Nodup := Finset.sort_nodup _ _
|
||
|
||
def states : List p.State := p.cfg.indices
|
||
|
||
lemma states_complete (s : p.State) : s ∈ p.states := p.cfg.mem_indices s
|
||
|
||
lemma states_nodup : p.states.Nodup := p.cfg.nodup_indices
|
||
|
||
def code (st : p.State) : Option BasicStmt := p.cfg.nodes st
|
||
|
||
def incoming (s : p.State) : List p.State := p.cfg.predecessors s
|
||
|
||
lemma incoming_initialState_eq_nil : p.incoming p.initialState = [] :=
|
||
Graph.wrap_predecessors_eq_nil p.rootStmt.cfg p.initialState
|
||
(by rw [Graph.wrap_inputs]; exact List.mem_singleton_self _)
|
||
|
||
lemma mem_incoming_of_edge {s₁ s₂ : p.State}
|
||
(h : (s₁, s₂) ∈ p.cfg.edges) : s₁ ∈ p.incoming s₂ :=
|
||
p.cfg.mem_predecessors_of_edge h
|
||
|
||
end Program
|
||
|
||
end Spa
|