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

Add more documentation

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin
2026-06-27 19:20:23 -05:00
parent 379438ec17
commit b1b3b0d2fe
1 changed files with 26 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

30
lean/Spa/Language/Properties.lean
View File

@@ -198,21 +198,38 @@ noncomputable def EndToEndTrace.loop_empty {ρ : Env} : EndToEndTrace (Graph.loo
end Loop
/-! ### Singletons, wrap, and the main result -/
/-- A CFG consisting of only a single node has a trace through it corresponding to that node. -/
noncomputable def EndToEndTrace.singleton {o : Option BasicStmt} {ρ₁ ρ₂ : Env}
(h : EvalBasicStmtOpt ρ₁ o ρ₂) : EndToEndTrace (Graph.singleton o) ρ₁ ρ₂ :=
⟨(0 : Fin 1), List.mem_singleton_self _, (0 : Fin 1), List.mem_singleton_self _,
Trace.single h⟩
/-- If a CFG's only node is empty, the no-op trace exists through it. -/
noncomputable def EndToEndTrace.singleton_nil (ρ : Env) :
EndToEndTrace (Graph.singleton none) ρ ρ :=
EndToEndTrace.singleton EvalBasicStmtOpt.none
/-- Invoking 'Graph.wrap` (which ensures a single entry and exit node for a CFG)
does not invalidate traces in the original graph. -/
noncomputable def EndToEndTrace.wrap {g : Graph} {ρ₁ ρ₂ : Env}
(etr : EndToEndTrace g ρ₁ ρ₂) : EndToEndTrace (Graph.wrap g) ρ₁ ρ₂ :=
(EndToEndTrace.singleton_nil ρ₁).concat (etr.concat (EndToEndTrace.singleton_nil ρ₂))
/-- Key result: the control flow graph admits every execution that's made
possible by a language's semantics. Thus, the CFG encodes _at least_ all
semantically-possible executions. Informally, we can conclude from this
that if we compute a result that using the graph's edges to determine
what's possible, this result will not disagree with the semantics.
Note that a CFG like $K_4$ (where the nodes are basic blocks) is
technically also a sufficient graph, but is very likely meaningless in that
it grossly overestimates the possible execution paths in the language, and
thus is bound to produce less-than-specific results. There is as yet no
result in this framework that the CFG we produce is _minimal_: loosely,
posessing only edges for things that are admitted by the semantics.
This is difficult to state (in its strongest form, this would
require the CFG to be able to detect something like `while (alwaysFalse)`,
and so remains a TODO. -/
noncomputable def Stmt.cfg_sufficient {s : Stmt} {ρ₁ ρ₂ : Env}
(h : EvalStmt ρ₁ s ρ₂) : EndToEndTrace s.cfg ρ₁ ρ₂ := by
induction h with
@@ -229,20 +246,24 @@ noncomputable def Stmt.cfg_sufficient {s : Stmt} {ρ₁ ρ₂ : Env}
| whileFalse ρ e s _ =>
exact EndToEndTrace.loop_empty
/-! ### The wrapped graph's entry has no predecessors (Agda's "ugly" block) -/
/-- The input / entry node generated by `Graph.wrap`. -/
def Graph.wrapInput (g : Graph) : (Graph.wrap g).Index :=
(0 : Fin 1).castAdd ((g ⤳ Graph.singleton none).size)
/-- The output / exit node generated by `Graph.wrap`. -/
def Graph.wrapOutput (g : Graph) : (Graph.wrap g).Index :=
Fin.natAdd 1 ((Fin.natAdd g.size (0 : Fin 1)))
/-- The `Graph.wrapInput` is, indeed, the graph's only input after `Graph.wrap`. -/
lemma Graph.wrap_inputs (g : Graph) :
(Graph.wrap g).inputs = [g.wrapInput] := rfl
/-- The `Graph.wrapInput` is, indeed, the graph's only output after `Graph.wrap`. -/
lemma Graph.wrap_outputs (g : Graph) :
(Graph.wrap g).outputs = [g.wrapOutput] := rfl
/-- When sequencing (proven here with `Graph.singleton` on the left), no edges
exist from the right-hand graph back to the left. -/
private lemma not_mem_edges_castAdd_sequence {g₂ : Graph} (i : Fin 1)
(idx : (Graph.singleton none ⤳ g₂).Index) :
((idx, i.castAdd g₂.size) : (Graph.singleton none ⤳ g₂).Edge)
@@ -260,6 +281,7 @@ private lemma not_mem_edges_castAdd_sequence {g₂ : Graph} (i : Fin 1)
obtain ⟨j, -, heq⟩ := List.mem_map.mp hb
exact Fin.castAdd_ne_natAdd i j heq.symm
/-- The input node of a graph after `Graph.wrap` has no predecessors. -/
lemma Graph.wrap_predecessors_eq_nil (g : Graph) (idx : (Graph.wrap g).Index)
(h : idx ∈ (Graph.wrap g).inputs) :
(Graph.wrap g).predecessors idx = [] := by