DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Add left-and-right open traces to help formalization

Browse Source 
Co-Authored-By: OpenAI Codex <codex@openai.com>
This commit is contained in:
Danila Fedorin
2026-07-01 16:35:07 -05:00
parent 8ed48cf444
commit 10b8fa97ca
1 changed files with 100 additions and 11 deletions
Download Patch File Download Diff File Expand all files Collapse all files

111
lean/Spa/Language/Traces.lean
View File

@@ -37,20 +37,102 @@ inductive Trace (g : Graph) : g.Index → g.Index → Env → Env → Type
EvalBasicStmtOpt ρ₁ (g.nodes idx₁) ρ₂ → (idx₁, idx₂) ∈ g.edges →
Trace g idx₂ idx₃ ρ₂ ρ₃ → Trace g idx₁ idx₃ ρ₁ ρ₃
/-!
## Open Traces
A normal `Trace` starts right before one state, and ends right after another.
This is convenient for inductively proving correctness / sufficience, but
awkward because 1) no empty traces exist and 2) concatenation requires an extra
edge.
However, when attempting an "empty" trace, two types are equally possible:
traces that end _right before_ executing a state (`Traceₗ`) and
traces that begin _right after_ executing a state (`Traceᵣ`). They
are symmetric and can be concatenated with full traces on the left
and right, respectively. -/
/-- Left-open trace, representing execution that ends right before `idx₂`. -/
inductive Traceₗ (g : Graph) : g.Index → g.Index → Env → Env → Type where
| nil {idx : g.Index} {ρ : Env} : Traceₗ g idx idx ρ ρ
| cons {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
EvalBasicStmtOpt ρ₁ (g.nodes idx₁) ρ₂ →
(idx₁, idx₂) ∈ g.edges →
Traceₗ g idx₂ idx₃ ρ₂ ρ₃ → Traceₗ g idx₁ idx₃ ρ₁ ρ₃
def Traceₗ.single (g : Graph) (idx : g.Index) (ρ : Env) : Traceₗ g idx idx ρ ρ := .nil
/-- Right-open trace, representing execution that starts right after `idx₁`. -/
inductive Traceᵣ (g : Graph) : g.Index → g.Index → Env → Env → Type where
| nil {idx : g.Index} {ρ : Env} : Traceᵣ g idx idx ρ ρ
| cons {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
Traceᵣ g idx₁ idx₂ ρ₁ ρ₂ →
(idx₂, idx₃) ∈ g.edges →
EvalBasicStmtOpt ρ₂ (g.nodes idx₃) ρ₃ → Traceᵣ g idx₁ idx₃ ρ₁ ρ₃
def Traceᵣ.single (g : Graph) (idx : g.Index) (ρ : Env) : Traceᵣ g idx idx ρ ρ := .nil
/-- Sequence two traces together. Since the endpoint of the first trace
is _after_ its last basic block's execution, and the beginning of
the next trace is _before_ its first basic block's execution,
there must be an edge to connect the two. -/
noncomputable def Trace.concat {g : Graph} {idx₁ idx₂ idx₃ idx₄ : g.Index}
def Trace.concat {g : Graph} {idx₁ idx₂ idx₃ idx₄ : g.Index}
{ρ₁ ρ₂ ρ₃ : Env} (tr₁ : Trace g idx₁ idx₂ ρ₁ ρ₂)
(he : (idx₂, idx₃) ∈ g.edges) (tr₂ : Trace g idx₃ idx₄ ρ₂ ρ₃) :
Trace g idx₁ idx₄ ρ₁ ρ₃ := by
induction tr₁ with
| single hbs => exact Trace.edge hbs he tr₂
| edge hbs he' _ ih => exact Trace.edge hbs he' (ih he tr₂)
Trace g idx₁ idx₄ ρ₁ ρ₃ :=
match tr₁ with
| single hbs => edge hbs he tr₂
| edge hbs he' tr₁' => edge hbs he' (tr₁'.concat he tr₂)
scoped notation:65 tr₁:66 " ++< " he " >++ " tr₂:65 => Trace.concat tr₁ he tr₂
def Trace.addEdge {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ : Env} :
Trace g idx₁ idx₂ ρ₁ ρ₂ →
(idx₂, idx₃) ∈ g.edges →
Traceₗ g idx₁ idx₃ ρ₁ ρ₂
| .single hnode, hedge => .cons hnode hedge .nil
| .edge hnode hedge' rest, hedge => .cons hnode hedge' (rest.addEdge hedge)
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)
def Traceₗ.appendTrace {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 => .edge hnode hedge (rest.appendTrace rhs)
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)
def Trace.appendRight {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
Trace g idx₁ idx₂ ρ₁ ρ₂ → Traceᵣ g idx₂ idx₃ ρ₂ ρ₃ →
Trace g idx₁ idx₃ ρ₁ ρ₃
| lhs, .nil => lhs
| lhs, .cons rest hedge hnode => Trace.concat (lhs.appendRight rest) hedge (.single hnode)
instance instHAppendTraceLTraceL {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
HAppend (Traceₗ g idx₁ idx₂ ρ₁ ρ₂) (Traceₗ g idx₂ idx₃ ρ₂ ρ₃) (Traceₗ g idx₁ idx₃ ρ₁ ρ₃) where
hAppend := Traceₗ.append
instance instHAppendTraceLTrace {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
HAppend (Traceₗ g idx₁ idx₂ ρ₁ ρ₂) (Trace g idx₂ idx₃ ρ₂ ρ₃) (Trace g idx₁ idx₃ ρ₁ ρ₃) where
hAppend := Traceₗ.appendTrace
instance instHAppendTraceLStep {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
HAppend (Traceₗ g idx₁ idx₂ ρ₁ ρ₂) (EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃) (Trace g idx₁ idx₂ ρ₁ ρ₃) where
hAppend := Traceₗ.appendStep
instance instHAppendTraceTraceR {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
HAppend (Trace g idx₁ idx₂ ρ₁ ρ₂) (Traceᵣ g idx₂ idx₃ ρ₂ ρ₃) (Trace g idx₁ idx₃ ρ₁ ρ₃) where
hAppend := Trace.appendRight
/-- 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)
@@ -74,21 +156,28 @@ inductive MyReaches {prog : Program} : {s₁ s₂ : prog.State} → {ρ₁ ρ₂
MyReaches rest s ρin ρout →
MyReaches (.edge hnode hedge rest) s ρin ρout
noncomputable def MyReaches.prefix {prog : Program} {s₁ s₂ s: prog.State}
def MyReaches.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
| .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}
{ρ₁ ρ₂ ρin ρout : Env} {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} :
(r : MyReaches tr s ρin ρout) → Trace prog.cfg s₁ s ρ₁ ρout
| .single_here hnode => Spa.Trace.single hnode
| .edge_here hnode hedge hrest => Spa.Trace.single hnode
| .edge_there hnode hedge hrest tmp' => Spa.Trace.edge hnode hedge tmp'.prefix
| .single_here hnode => .single hnode
| .edge_here hnode _ _ => .single hnode
| .edge_there hnode hedge _ r => .edge hnode hedge r.post
noncomputable def MyReaches.first {prog : Program} {s₁ s₂ s: prog.State}
def MyReaches.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₁ ρ₁ ρ₁'
| .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⟩
noncomputable def MyReaches.step {prog : Program} {s₁ s₂ s: prog.State}
def MyReaches.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
| .single_here hnode => hnode