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

Compare commits

base: DanilaFe:fable-lean-migration
Branches Tags
DanilaFe:main DanilaFe:fable-lean-migration DanilaFe:dag-lattice-builder
..
compare: DanilaFe:30d2960fca7e0c345f7357789995f595c9267c77
Branches Tags
DanilaFe:fable-lean-migration DanilaFe:dag-lattice-builder DanilaFe:main

1 Commits
fable-lean ... 30d2960fca

Author SHA1 Message Date
Danila Fedorin
30d2960fca Add scoped quotation syntax for object-language programs 
Introduce [spa_e| ... ] for Expr and [spa| ... ] for Stmt, scoped to the
Spa namespace via a dedicated syntax category and macro_rules. This removes
the deeply nested .andThen / .basic (.assign ...) boilerplate when writing
programs; Main.lean's test programs are rewritten to use it.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_018Yq5SmPQfNfzAEUpUXRo66
 2026-06-23 14:28:06 -05:00
38 changed files with 1321 additions and 3028 deletions
Expand all files Collapse all files

6
lean/Main.lean
View File

@@ -1,6 +1,5 @@
import Spa.Analysis.Sign
import Spa.Analysis.Constant
import Spa.Analysis.Reaching
import Spa.Language.Notation
namespace Spa
@@ -27,11 +26,10 @@ def testCodeCond₂ : Stmt := [obj_stmt|
if var { x := 1 } else { noop }
]
def testProgram : Program := { rootStmt := testCode }
def testProgram : Program := ⟨testCode⟩
end Spa
def main : IO Unit :=
IO.println (Spa.ConstAnalysis.output Spa.testProgram ++ "\n" ++
Spa.SignAnalysis.output Spa.testProgram ++ "\n" ++
Spa.ReachingAnalysis.output Spa.testProgram)
Spa.SignAnalysis.output Spa.testProgram)

11
lean/Spa.lean
View File

@@ -1,9 +1,11 @@
import Spa.Lattice
import Spa.Fixedpoint
import Spa.Isomorphism
import Spa.Lattice.Unit
import Spa.Lattice.Prod
import Spa.Lattice.AboveBelow
import Spa.Lattice.IterProd
import Spa.Lattice.FiniteMap
import Spa.Lattice.Bool
import Spa.Language.Base
import Spa.Language.Notation
import Spa.Language.Semantics
@@ -19,10 +21,3 @@ import Spa.Showable
import Spa.Analysis.Utils
import Spa.Analysis.Sign
import Spa.Analysis.Constant
import Spa.Language.Tagged.Id
import Spa.Language.Tagged.Derive
import Spa.Language.Tagged.Basic
import Spa.Language.Tagged.Properties
import Spa.Language.Tagged.Graphs
import Spa.Analysis.Reaching
import Spa.Transformation.Licm

71
lean/Spa/Analysis/Constant.lean
View File

@@ -5,8 +5,6 @@ import Spa.Showable
namespace Spa
open Forward
abbrev ConstLattice : Type := AboveBelow ℤ
namespace ConstAnalysis
@@ -27,22 +25,24 @@ def minus : ConstLattice → ConstLattice → ConstLattice
| _, top => top
| mk z₁, mk z₂ => mk (z₁ - z₂)
lemma plus_mono₂ : Monotone₂ plus :=
theorem plus_mono₂ : Monotone₂ plus :=
AboveBelow.monotone₂_of_strict plus
(fun y => by aesop) (fun x => by aesop)
(fun y hy => by aesop) (fun x hx => by aesop)
(fun y => by cases y <;> rfl) (fun x => by cases x <;> rfl)
(fun y hy => by cases y <;> first | exact absurd rfl hy | rfl)
(fun x hx => by cases x <;> first | exact absurd rfl hx | rfl)
lemma minus_mono₂ : Monotone₂ minus :=
theorem minus_mono₂ : Monotone₂ minus :=
AboveBelow.monotone₂_of_strict minus
(fun y => by aesop) (fun x => by aesop)
(fun y hy => by aesop) (fun x hx => by aesop)
(fun y => by cases y <;> rfl) (fun x => by cases x <;> rfl)
(fun y hy => by cases y <;> first | exact absurd rfl hy | rfl)
(fun x hx => by cases x <;> first | exact absurd rfl hx | rfl)
def interpConst : ConstLattice → Value → Prop
| .bot, _ => False
| .top, _ => True
| .mk z, v => v = .int z
lemma interpConst_mk_disjoint {z₁ z₂ : ℤ} (hne : z₁ ≠ z₂) {v : Value} :
theorem interpConst_mk_disjoint {z₁ z₂ : ℤ} (hne : z₁ ≠ z₂) {v : Value} :
¬(interpConst (.mk z₁) v ∧ interpConst (.mk z₂) v) := by
rintro ⟨h₁, h₂⟩
rw [h₁] at h₂
@@ -63,7 +63,7 @@ def eval : Expr → VariableValues ConstLattice prog → ConstLattice
if h : FiniteMap.MemKey k vs then (FiniteMap.locate h).1 else .top
| .num n, _ => .mk n
lemma eval_mono (e : Expr) : Monotone (eval prog e) := by
theorem eval_mono (e : Expr) : Monotone (eval prog e) := by
induction e with
| add e₁ e₂ ih₁ ih₂ =>
intro vs₁ vs₂ h
@@ -75,12 +75,12 @@ lemma eval_mono (e : Expr) : Monotone (eval prog e) := by
intro vs₁ vs₂ h
simp only [eval]
by_cases hk : k ∈ prog.vars
· rw [dif_pos (FiniteMap.MemKey_iff.mpr hk),
dif_pos (FiniteMap.MemKey_iff.mpr hk)]
· rw [dif_pos (FiniteMap.memKey_iff.mpr hk),
dif_pos (FiniteMap.memKey_iff.mpr hk)]
exact FiniteMap.le_of_mem_mem prog.vars_nodup h
(FiniteMap.locate _).2 (FiniteMap.locate _).2
· rw [dif_neg (fun hm => hk (FiniteMap.MemKey_iff.mp hm)),
dif_neg (fun hm => hk (FiniteMap.MemKey_iff.mp hm))]
· rw [dif_neg (fun hm => hk (FiniteMap.memKey_iff.mp hm)),
dif_neg (fun hm => hk (FiniteMap.memKey_iff.mp hm))]
| num n =>
intro vs₁ vs₂ _
exact le_refl _
@@ -91,17 +91,39 @@ instance exprEvaluator : ExprEvaluator ConstLattice prog :=
def output : String :=
show' (result ConstLattice prog)
lemma plus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ}
theorem plus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ}
(h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
⟦plus g₁ g₂⟧ (.int (z₁ + z₂)) := by
rcases g₁ with _ | _ | c₁ <;> rcases g₂ with _ | _ | c₂ <;>
simp_all [plus, constInterpretation, interpConst]
rcases g₁ with _ | _ | c₁
· exact h₁.elim
· rcases g₂ with _ | _ | c₂
· exact h₂.elim
· exact trivial
· exact trivial
· rcases g₂ with _ | _ | c₂
· exact h₂.elim
· exact trivial
· injection h₁ with hz₁
injection h₂ with hz₂
show Value.int (z₁ + z₂) = Value.int (c₁ + c₂)
rw [hz₁, hz₂]
lemma minus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ}
theorem minus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ}
(h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
⟦minus g₁ g₂⟧ (.int (z₁ - z₂)) := by
rcases g₁ with _ | _ | c₁ <;> rcases g₂ with _ | _ | c₂ <;>
simp_all [minus, constInterpretation, interpConst]
rcases g₁ with _ | _ | c₁
· exact h₁.elim
· rcases g₂ with _ | _ | c₂
· exact h₂.elim
· exact trivial
· exact trivial
· rcases g₂ with _ | _ | c₂
· exact h₂.elim
· exact trivial
· injection h₁ with hz₁
injection h₂ with hz₂
show Value.int (z₁ - z₂) = Value.int (c₁ - c₂)
rw [hz₁, hz₂]
instance eval_valid : ValidExprEvaluator ConstLattice prog := by
constructor
@@ -135,14 +157,7 @@ instance eval_valid : ValidExprEvaluator ConstLattice prog := by
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) :
⟦ joinForKey s (result ConstLattice prog) ⟧ ρin
∧ ⟦ variablesAt s (result ConstLattice prog) ⟧ ρout :=
Forward.analyze_correct_at ConstLattice prog hrun hr
Spa.analyze_correct ConstLattice prog hrun
end ConstAnalysis

173
lean/Spa/Analysis/Forward.lean
View File

@@ -5,37 +5,38 @@ import Spa.Fixedpoint
namespace Spa
namespace Forward
variable {L : Type} [FiniteHeightLattice L] {prog : Program} [E : StmtEvaluator L prog]
variable {L : Type} [Lattice L] {prog : Program} [E : StmtEvaluator L prog]
def updateVariablesForState (s : prog.State) (sv : StateVariables L prog) :
VariableValues L prog := E.eval s (variablesAt s sv)
VariableValues L prog :=
(prog.code s).foldl (fun vs bs => E.eval s bs vs) (variablesAt s sv)
lemma updateVariablesForState_mono (s : prog.State) :
theorem updateVariablesForState_mono (s : prog.State) :
Monotone (updateVariablesForState (L := L) s) := fun _ _ hle =>
E.eval_mono s (variablesAt_le hle s)
foldl_mono' (prog.code s) _ (E.eval_mono s ·) (variablesAt_le hle s)
def updateAll (sv : StateVariables L prog) : StateVariables L prog :=
FiniteMap.generalizedUpdate id updateVariablesForState
prog.states sv
lemma updateAll_mono : Monotone (updateAll (L := L) (prog := prog)) :=
theorem updateAll_mono : Monotone (updateAll (L := L) (prog := prog)) :=
FiniteMap.generalizedUpdate_monotone monotone_id updateVariablesForState_mono
lemma updateAll_mem_eq {s : prog.State} {vs : VariableValues L prog}
theorem updateAll_mem_eq {s : prog.State} {vs : VariableValues L prog}
{sv : StateVariables L prog} (hmem : (s, vs) ∈ updateAll sv) :
vs = updateVariablesForState s sv :=
FiniteMap.generalizedUpdate_mem_eq (prog.states_complete s) hmem
lemma variablesAt_updateAll (s : prog.State) (sv : StateVariables L prog) :
theorem variablesAt_updateAll (s : prog.State) (sv : StateVariables L prog) :
variablesAt s (updateAll sv) = updateVariablesForState s sv :=
updateAll_mem_eq (variablesAt_mem s (updateAll sv))
variable [FiniteHeightLattice L]
def analyze (sv : StateVariables L prog) : StateVariables L prog :=
updateAll (joinAll sv)
lemma analyze_mono : Monotone (analyze (L := L) (prog := prog)) := fun _ _ hle =>
theorem analyze_mono : Monotone (analyze (L := L) (prog := prog)) := fun _ _ hle =>
updateAll_mono (joinAll_mono hle)
variable [DecidableEq L]
@@ -45,130 +46,74 @@ def result : StateVariables L prog :=
Fixedpoint.aFix analyze analyze_mono
variable (L prog) in
lemma result_eq : result L prog = analyze (result L prog) :=
theorem result_eq : result L prog = analyze (result L prog) :=
Fixedpoint.aFix_eq analyze analyze_mono
lemma joinForKey_initialState :
theorem joinForKey_initialState :
joinForKey prog.initialState (result L prog) = botV L prog := by
rw [joinForKey, prog.incoming_initialState_eq_nil]
rfl
class ValidStateEvaluator (L : Type) [FiniteHeightLattice L] (prog : Program)
[E : StmtEvaluator L prog] [S : StateInterpretation L prog] where
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 []))
variable [I : LatticeInterpretation L] [V : ValidStmtEvaluator L prog]
instance [LatticeInterpretation L] [ValidStmtEvaluator L prog] :
ValidStateEvaluator L prog where
valid := by intro _ _ _ _ _ _ tr hbs hvs; exact ValidStmtEvaluator.valid hbs hvs
botV_init := by intro k l _ v hmem; cases hmem
omit [FiniteHeightLattice L] [DecidableEq L] in
theorem eval_fold_valid {s : prog.State} {bss : List BasicStmt}
{vs : VariableValues L prog} {ρ₁ ρ₂ : Env}
(hbss : EvalBasicStmts ρ₁ bss ρ₂) (hvs : ⟦ vs ⟧ ρ₁) :
⟦ bss.foldl (fun vs bs => E.eval s bs vs) vs ⟧ ρ₂ := by
induction hbss generalizing vs with
| nil => exact hvs
| cons hbs _ ih => exact ih (ValidStmtEvaluator.valid hbs hvs)
section
variable [S : StateInterpretation L prog] [V : ValidStateEvaluator L prog]
omit [FiniteHeightLattice L] [DecidableEq L] in
theorem updateVariablesForState_matches {s : prog.State}
{sv : StateVariables L prog} {ρ₁ ρ₂ : Env}
(hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂)
(hvs : ⟦ variablesAt s sv ⟧ ρ₁) :
⟦ updateVariablesForState s sv ⟧ ρ₂ :=
eval_fold_valid hbss hvs
omit [DecidableEq L] in
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
omit [FiniteHeightLattice L] [DecidableEq L] in
theorem updateAll_matches {s : prog.State} {sv : StateVariables L prog}
{ρ₁ ρ₂ : Env} (hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂)
(hvs : ⟦ variablesAt s sv ⟧ ρ₁) :
⟦ variablesAt s (updateAll sv) ⟧ ρ₂ := by
rw [variablesAt_updateAll]
exact V.valid s₁ s₂ tr hnode hvs
exact updateVariablesForState_matches hbss hvs
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
theorem stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env}
(hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁)
(hbss : EvalBasicStmts ρ₁ (prog.code s₁) ρ₂) :
⟦ variablesAt s₁ (result L prog) ⟧ ρ₂ := by
rw [result_eq L prog]
refine updateAll_matches tr hnode ?_
refine updateAll_matches hbss ?_
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)
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'⟩
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
theorem walkTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
(hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁)
(tr : Trace prog.graph s₁ s₂ ρ₁ ρ₂) :
⟦ variablesAt s₂ (result L prog) ⟧ ρ₂ := by
induction tr with
| single hnode => rfl
| edge hnode hedge rest ih => simp [reaches_final, Reaches.post, ih]
| single hbss => exact stepTrace hjoin hbss
| @edge _ ρ' _ i₁ i₂ _ hbss hedge _ ih =>
have hstep : ⟦ variablesAt i₁ (result L prog) ⟧ ρ' :=
stepTrace hjoin hbss
have hmem : variablesAt i₁ (result L prog)
∈ (result L prog).valuesAt (prog.incoming i₂) :=
FiniteMap.mem_valuesAt prog.states_nodup
(prog.mem_incoming_of_edge hedge) (variablesAt_mem i₁ (result L prog))
exact ih (interp_foldr hstep hmem)
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) :
⟦ 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 _ _ []) ?_
omit V in
theorem interp_joinForKey_initialState :
⟦ joinForKey prog.initialState (result L prog) ⟧ [] := by
rw [joinForKey_initialState]
exact ValidStateEvaluator.botV_init
exact interp_botV_nil
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
rwa [reaches_final_post] at h
end
variable (L prog) in
theorem analyze_correct [LatticeInterpretation L] [ValidStmtEvaluator L prog]
{ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
⟦ variablesAt prog.finalState (result L prog) ⟧ ρ :=
analyze_correct' L prog hrun
end Forward
walkTrace interp_joinForKey_initialState (prog.trace hrun)
end Spa

58
lean/Spa/Analysis/Forward/Adapters.lean
View File

@@ -2,63 +2,53 @@ import Spa.Analysis.Forward.Evaluation
namespace Spa
namespace Forward
variable {L : Type} [Lattice L] {prog : Program} [E : ExprEvaluator L prog]
def updateVariablesFromExpression (k : String) (e : Expr)
(vs : VariableValues L prog) : VariableValues L prog :=
FiniteMap.generalizedUpdate id (fun _ vs => E.eval e vs) [k] vs
lemma updateVariablesFromExpression_mono (k : String) (e : Expr) :
theorem updateVariablesFromExpression_mono (k : String) (e : Expr) :
Monotone (updateVariablesFromExpression (L := L) (prog := prog) k e) :=
FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => E.eval_mono e)
def evalBasicStmt (bs : BasicStmt)
def evalB (_ : prog.State) (bs : BasicStmt)
(vs : VariableValues L prog) : VariableValues L prog :=
match bs with
| .assign k e => updateVariablesFromExpression k e vs
| .noop => vs
lemma evalBasicStmt_mono (bs : BasicStmt) :
Monotone (evalBasicStmt (L := L) (prog := prog) bs) := by
theorem evalB_mono (s : prog.State) (bs : BasicStmt) :
Monotone (evalB (L := L) (prog := prog) s bs) := by
cases bs with
| assign k e => exact updateVariablesFromExpression_mono k e
| noop => exact monotone_id
def evalBasicStmtOpt (obs : Option BasicStmt)
(vs : VariableValues L prog) : VariableValues L prog :=
match obs with
| none => vs
| some bs => evalBasicStmt bs vs
lemma evalBasicStmtOpt_mono (obs : Option BasicStmt) :
Monotone (evalBasicStmtOpt (L := L) (prog := prog) obs) := by
cases obs <;> unfold evalBasicStmtOpt
· exact monotone_id
· apply evalBasicStmt_mono
instance ExprEvaluator.toStmtEvaluator : StmtEvaluator L prog :=
⟨evalBasicStmtOpt ∘ prog.code,
by intro s; simp; exact (evalBasicStmtOpt_mono (prog.code s))⟩
⟨evalB, evalB_mono⟩
instance ExprEvaluator.toStmtEvaluator_valid [LatticeInterpretation L]
[ValidExprEvaluator L prog] : ValidStmtEvaluator L prog := by
constructor
simp [StmtEvaluator.eval, evalBasicStmtOpt]
intro s vs ρ₁ ρ₂; generalize prog.code s = obs; intro hev hvs
rcases hev with _ | @⟨_,bs,hev⟩ <;> try simpa
rcases hev with _ | @⟨k, e, v, hev⟩ <;> try simpa
intros k' l' hkl' v' hρ
rcases hρ with _ | ⟨_,_,_,_,_,hne,hmem⟩ <;> simp [evalBasicStmt] at hkl'
· have hl := FiniteMap.generalizedUpdate_mem_eq (f := id)
(g := fun _ vs => E.eval e vs) (List.mem_singleton_self k) hkl'
rewrite [hl]; simp
intro s vs ρ₁ ρ₂ bs hbs hvs
cases hbs with
| noop => exact hvs
| assign k e v hev =>
intro k' l hk'l v' hv'
cases hv' with
| here =>
have hk'l₀ : (k, l) ∈ FiniteMap.generalizedUpdate (ks := prog.vars) id
(fun _ vs => E.eval e vs) [k] vs := hk'l
have hl := FiniteMap.generalizedUpdate_mem_eq (f := id)
(g := fun _ vs => E.eval e vs) (List.mem_singleton_self k) hk'l₀
rw [hl]
exact ValidExprEvaluator.valid hev hvs
· have hl := FiniteMap.generalizedUpdate_not_mem_backward
(fun hmem => hne (List.mem_singleton.mp hmem)) hkl'
apply hvs _ _ hl _ hmem
end Forward
| there _ _ _ _ _ hne hmem' =>
have hk'l₀ : (k', l) ∈ FiniteMap.generalizedUpdate (ks := prog.vars) id
(fun _ vs => E.eval e vs) [k] vs := hk'l
have hk'l' : (k', l) ∈ (id vs : VariableValues L prog) :=
FiniteMap.generalizedUpdate_not_mem_backward
(fun hmem => hne (List.mem_singleton.mp hmem)) hk'l₀
exact hvs _ _ hk'l' _ hmem'
end Spa

13
lean/Spa/Analysis/Forward/Evaluation.lean
View File

@@ -2,13 +2,11 @@ import Spa.Analysis.Forward.Lattices
namespace Spa
namespace Forward
variable (L : Type) [Lattice L] (prog : Program)
class StmtEvaluator where
eval : prog.State → VariableValues L prog → VariableValues L prog
eval_mono : ∀ s, Monotone (eval s)
eval : prog.State → BasicStmt → VariableValues L prog → VariableValues L prog
eval_mono : ∀ s bs, Monotone (eval s bs)
class ExprEvaluator where
eval : Expr → VariableValues L prog → L
@@ -21,9 +19,8 @@ class ValidExprEvaluator [ExprEvaluator L prog] [I : LatticeInterpretation L] :
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 ⟧ ρ₂
end Forward
valid : ∀ {s : prog.State} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env}
{bs : BasicStmt},
EvalBasicStmt ρ₁ bs ρ₂ → ⟦ vs ⟧ ρ₁ → ⟦ E.eval s bs vs ⟧ ρ₂
end Spa

86
lean/Spa/Analysis/Forward/Lattices.lean
View File

@@ -4,8 +4,6 @@ import Spa.Interp
namespace Spa
namespace Forward
variable (L : Type) [Lattice L] (prog : Program)
abbrev VariableValues : Type := FiniteMap String L prog.vars
@@ -18,20 +16,20 @@ def botV [FiniteHeightLattice L] : VariableValues L prog :=
variable {L prog}
omit [Lattice L] in
lemma states_memKey (s : prog.State) (sv : StateVariables L prog) :
theorem states_memKey (s : prog.State) (sv : StateVariables L prog) :
FiniteMap.MemKey s sv :=
FiniteMap.MemKey_iff.mpr (prog.states_complete s)
FiniteMap.memKey_iff.mpr (prog.states_complete s)
def variablesAt (s : prog.State) (sv : StateVariables L prog) :
VariableValues L prog :=
(FiniteMap.locate (states_memKey s sv)).1
omit [Lattice L] in
lemma variablesAt_mem (s : prog.State) (sv : StateVariables L prog) :
theorem variablesAt_mem (s : prog.State) (sv : StateVariables L prog) :
(s, variablesAt s sv) ∈ sv :=
(FiniteMap.locate (states_memKey s sv)).2
lemma variablesAt_le {sv₁ sv₂ : StateVariables L prog} (hle : sv₁ ≤ sv₂)
theorem variablesAt_le {sv₁ sv₂ : StateVariables L prog} (hle : sv₁ ≤ sv₂)
(s : prog.State) : variablesAt s sv₁ ≤ variablesAt s sv₂ :=
FiniteMap.le_of_mem_mem prog.states_nodup hle
(variablesAt_mem s sv₁) (variablesAt_mem s sv₂)
@@ -42,7 +40,7 @@ def joinForKey (k : prog.State) (sv : StateVariables L prog) :
VariableValues L prog :=
(sv.valuesAt (prog.incoming k)).foldr (· ⊔ ·) (botV L prog)
lemma joinForKey_mono (k : prog.State) :
theorem joinForKey_mono (k : prog.State) :
Monotone (joinForKey (L := L) k) := by
intro sv₁ sv₂ hle
exact foldr_mono _ (FiniteMap.valuesAt_le hle (prog.incoming k)) (le_refl _)
@@ -52,70 +50,50 @@ lemma joinForKey_mono (k : prog.State) :
def joinAll (sv : StateVariables L prog) : StateVariables L prog :=
FiniteMap.generalizedUpdate id joinForKey prog.states sv
lemma joinAll_mono : Monotone (joinAll (L := L) (prog := prog)) :=
theorem joinAll_mono : Monotone (joinAll (L := L) (prog := prog)) :=
FiniteMap.generalizedUpdate_monotone monotone_id joinForKey_mono
lemma joinAll_mem_eq {s : prog.State} {vs : VariableValues L prog}
theorem joinAll_mem_eq {s : prog.State} {vs : VariableValues L prog}
{sv : StateVariables L prog} (h : (s, vs) ∈ joinAll sv) :
vs = joinForKey s sv :=
FiniteMap.generalizedUpdate_mem_eq (prog.states_complete s) h
lemma variablesAt_joinAll (s : prog.State) (sv : StateVariables L prog) :
theorem variablesAt_joinAll (s : prog.State) (sv : StateVariables L prog) :
variablesAt s (joinAll sv) = joinForKey s sv :=
joinAll_mem_eq (variablesAt_mem s (joinAll sv))
class StateInterpretation (L : Type) [Lattice L] (prog : Program) where
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) (S.Proj → Prop) :=
⟨S.interp⟩
lemma interp_foldr [S : StateInterpretation L prog]
{vs : VariableValues L prog} {vss : List (VariableValues L prog)}
{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 =>
rcases List.mem_cons.mp hmem with rfl | hmem'
· exact S.interp_sup (Or.inl hvs)
· exact S.interp_sup (Or.inr (ih hmem'))
/-! ### Lifting an interpretation to variable maps -/
variable [I : LatticeInterpretation L]
instance : StateInterpretation L prog where
Proj := Env
Pre := fun {_ _ _ ρ₂} _ => ρ₂
Post := fun {_ _ _ ρ₂} _ => ρ₂
interp vs ρ := ∀ (k : String) (l : L), (k, l) ∈ vs →
omit [FiniteHeightLattice L] in
instance : Interp (VariableValues L prog) (Env → Prop) where
interp (vs : VariableValues L prog) (ρ : Env) : Prop :=
∀ (k : String) (l : L), (k, l) ∈ vs →
∀ (v : Value), Env.Mem (k, v) ρ → I.interp l v
interp_sup := by
intro vs₁ vs₂ ρ h k l hmem v hv
theorem interp_botV_nil : ⟦ botV L prog ⟧ [] := by
intro k l _ v hmem
cases hmem
omit [FiniteHeightLattice L] in
theorem interp_sup {vs₁ vs₂ : VariableValues L prog} {ρ : Env}
(h : ⟦ vs₁⟧ ρ ∨ ⟦ vs₂ ⟧ ρ) : ⟦ vs₁ ⊔ vs₂ ⟧ ρ := by
intro 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₂ ρ 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
theorem interp_foldr {vs : VariableValues L prog}
{vss : List (VariableValues L prog)} {ρ : Env}
(hvs : ⟦ vs ⟧ ρ) (hmem : vs ∈ vss) :
⟦ vss.foldr (· ⊔ ·) (botV L prog) ⟧ ρ := by
induction vss with
| nil => cases hmem
| cons vs' vss' ih =>
rcases List.mem_cons.mp hmem with rfl | hmem'
· exact interp_sup (Or.inl hvs)
· exact interp_sup (Or.inr (ih hmem'))
end Spa

135
lean/Spa/Analysis/Reaching.lean
View File

@@ -1,135 +0,0 @@
import Spa.Analysis.Forward
import Spa.Lattice.Finset
import Spa.Language.Tagged.Graphs
import Spa.Showable
namespace Spa
open Forward
instance {n : ℕ} : Showable (Finset (Fin n)) :=
⟨fun s =>
"{" ++ (List.finRange n).foldr
(fun i rest => if i ∈ s then show' i ++ ", " ++ rest else rest) ""
++ "}"⟩
abbrev DefSet (prog : Program) : Type := Finset prog.NodeId
namespace ReachingAnalysis
variable (prog : Program)
def genSet (s : prog.State) : DefSet prog := (prog.nodeIdOf s).elim {} (fun x => {x})
def eval (s : prog.State) (vs : VariableValues (DefSet prog) prog) : VariableValues (DefSet prog) prog :=
match prog.code s with
| none => vs
| some bs =>
match bs with
| .assign k _ => FiniteMap.generalizedUpdate id (fun _ _ => genSet prog s) [k] vs
| .noop => vs
lemma eval_mono (s : prog.State) :
Monotone (eval prog s) := by
intros vs₁ vs₂ hle
unfold eval; split <;> try simpa
split <;> try simpa
apply FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => monotone_const)
assumption
instance stmtEvaluator : StmtEvaluator (DefSet prog) prog :=
⟨eval prog, eval_mono prog⟩
def output : String :=
show' (result (DefSet prog) prog)
/-- The statements a trace executed, paired with the state each executed at,
most recent first (matching `LastAssign`, which scans for the most recent
assignment). This is `Trace.steps` (chronological) reversed, so facts about
concatenating traces reduce to mathlib's `List.append`/`List.reverse` lemmas. -/
abbrev Run (prog : Program) : Type := List (prog.State × BasicStmt)
@[aesop unsafe cases]
inductive LastAssign (prog : Program) (x : String) : Run prog → prog.NodeId → Prop
| here (s : prog.State) (e : Expr) (hc : prog.code s = some (.assign x e))
(rest : Run prog) :
LastAssign prog x ((s, .assign x e) :: rest) (prog.nodeIdOfNonempty s hc)
| there (s : prog.State) (bs : BasicStmt) (hc : prog.code s = some bs)
(rest : Run prog) {n : prog.NodeId} :
(∀ e, bs ≠ .assign x e) → LastAssign prog x rest n →
LastAssign prog x ((s, bs) :: rest) n
def runOfTraceₗ {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
(tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂) : Run prog :=
tr.steps.reverse
def runOfTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
(tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) : Run prog :=
tr.steps.reverse
instance stateInterp : StateInterpretation (DefSet prog) prog where
Proj := Run prog
Pre := @runOfTraceₗ prog
Post := @runOfTrace prog
interp vs run := ∀ (x : String) (assigners : DefSet prog), (x, assigners) ∈ vs →
∀ (n : prog.NodeId), LastAssign prog x run n → n ∈ assigners
interp_sup := by
intro vs₁ vs₂ run h x assigners hmem n hla
obtain ⟨a₁, a₂, rfl, h₁, h₂⟩ := FiniteMap.mem_sup hmem
aesop (add simp Finset.mem_union)
interp_inf := by
intro vs₁ vs₂ run h x assigners hmem n hla
obtain ⟨a₁, a₂, rfl, h₁, h₂⟩ := FiniteMap.mem_inf hmem
aesop (add simp Finset.mem_inter)
post_pre := by
intro vs s₁ s₂ s₃ ρ₁ ρ₂ tr hedge hvs
simpa [runOfTrace, runOfTraceₗ] using hvs
private lemma valid_step (s : prog.State) {ρ₁ ρ₂ : Env}
{obs : Option BasicStmt} (hcode : prog.code s = obs)
(hbs : EvalBasicStmtOpt ρ₁ obs ρ₂)
{vs : VariableValues (DefSet prog) prog} {run : Run prog}
(hvs : ⟦vs⟧ run) :
⟦eval prog s vs⟧ ((hbs.steps s).reverse ++ run) := by
cases hbs with
| none => simpa [eval, hcode, EvalBasicStmtOpt.steps] using hvs
| some hbs =>
cases hbs with
| noop =>
simp [eval, hcode, EvalBasicStmtOpt.steps]
intro x assigners hmem n hla; aesop
| assign x e v hev =>
simp [eval, hcode, EvalBasicStmtOpt.steps]; intro k assigners hmem n hla
by_cases hx : k = x
· subst hx
have hd := FiniteMap.generalizedUpdate_mem_eq (List.mem_singleton.mpr rfl) hmem
rcases hla
<;> simp [Program.nodeIdOfNonempty, hd, genSet, Option.get] <;> aesop
· have hmem' := FiniteMap.generalizedUpdate_not_mem_backward
(fun hc => hx (List.mem_singleton.mp hc)) hmem
aesop
instance validStateEvaluator : ValidStateEvaluator (DefSet prog) prog where
valid := by
intro s₁ s₂ ρ₁ ρ₂ ρ₃ vs tr hbs hvs
show ⟦eval prog s₂ vs⟧ (runOfTrace prog (tr ++ hbs))
simpa [runOfTrace, runOfTraceₗ] using valid_step prog s₂ rfl hbs hvs
botV_init := by intro x assigners _ n hla; cases hla
theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
⟦ variablesAt prog.finalState (result (DefSet prog) prog) ⟧
(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) :
⟦ 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
end ReachingAnalysis
end Spa

53
lean/Spa/Analysis/Sign.lean
View File

@@ -5,16 +5,12 @@ import Spa.Showable
namespace Spa
open Forward
inductive Sign where
| plus
| minus
| zero
deriving DecidableEq
attribute [aesop safe cases] Sign
instance : Showable Sign :=
⟨fun
| .plus => "+"
@@ -57,15 +53,23 @@ def minus : SignLattice → SignLattice → SignLattice
| mk .zero, mk .minus => mk .plus
| mk .zero, mk .zero => mk .zero
lemma plus_mono₂ : Monotone₂ plus :=
theorem plus_mono₂ : Monotone₂ plus :=
AboveBelow.monotone₂_of_strict plus
(fun y => by aesop) (fun x => by aesop)
(fun y hy => by aesop) (fun x hx => by aesop)
(fun y => by cases y <;> rfl)
(fun x => by rcases x with _ | _ | s <;> first | rfl | (cases s <;> rfl))
(fun y hy => by cases y <;> first | exact absurd rfl hy | rfl)
(fun x hx => by
rcases x with _ | _ | s <;>
first | exact absurd rfl hx | rfl | (cases s <;> rfl))
lemma minus_mono₂ : Monotone₂ minus :=
theorem minus_mono₂ : Monotone₂ minus :=
AboveBelow.monotone₂_of_strict minus
(fun y => by aesop) (fun x => by aesop)
(fun y hy => by aesop) (fun x hx => by aesop)
(fun y => by cases y <;> rfl)
(fun x => by rcases x with _ | _ | s <;> first | rfl | (cases s <;> rfl))
(fun y hy => by cases y <;> first | exact absurd rfl hy | rfl)
(fun x hx => by
rcases x with _ | _ | s <;>
first | exact absurd rfl hx | rfl | (cases s <;> rfl))
def interpSign : SignLattice → Value → Prop
| .bot, _ => False
@@ -74,7 +78,7 @@ def interpSign : SignLattice → Value → Prop
| .mk .zero, v => v = .int 0
| .mk .minus, v => ∃ n : ℕ, v = .int (-(n + 1))
lemma interpSign_mk_disjoint {s₁ s₂ : Sign} (hne : s₁ ≠ s₂) {v : Value} :
theorem interpSign_mk_disjoint {s₁ s₂ : Sign} (hne : s₁ ≠ s₂) {v : Value} :
¬(interpSign (.mk s₁) v ∧ interpSign (.mk s₂) v) := by
rintro ⟨h₁, h₂⟩
rcases s₁ <;> rcases s₂ <;> try exact hne rfl
@@ -119,7 +123,7 @@ def eval : Expr → VariableValues SignLattice prog → SignLattice
| .num 0, _ => .mk .zero
| .num (_ + 1), _ => .mk .plus
lemma eval_mono (e : Expr) : Monotone (eval prog e) := by
theorem eval_mono (e : Expr) : Monotone (eval prog e) := by
induction e with
| add e₁ e₂ ih₁ ih₂ =>
intro vs₁ vs₂ h
@@ -131,12 +135,12 @@ lemma eval_mono (e : Expr) : Monotone (eval prog e) := by
intro vs₁ vs₂ h
simp only [eval]
by_cases hk : k ∈ prog.vars
· rw [dif_pos (FiniteMap.MemKey_iff.mpr hk),
dif_pos (FiniteMap.MemKey_iff.mpr hk)]
· rw [dif_pos (FiniteMap.memKey_iff.mpr hk),
dif_pos (FiniteMap.memKey_iff.mpr hk)]
exact FiniteMap.le_of_mem_mem prog.vars_nodup h
(FiniteMap.locate _).2 (FiniteMap.locate _).2
· rw [dif_neg (fun hm => hk (FiniteMap.MemKey_iff.mp hm)),
dif_neg (fun hm => hk (FiniteMap.MemKey_iff.mp hm))]
· rw [dif_neg (fun hm => hk (FiniteMap.memKey_iff.mp hm)),
dif_neg (fun hm => hk (FiniteMap.memKey_iff.mp hm))]
| num n =>
intro vs₁ vs₂ _
cases n <;> exact le_refl _
@@ -148,18 +152,18 @@ def output : String :=
show' (result SignLattice prog)
/-- A nonneg-shifted interpretation `∃ n : ℕ, z = n + 1` just means `z` is positive. -/
private lemma int_pos_iff (z : ℤ) : (∃ n : ℕ, z = (n : ℤ) + 1) ↔ 0 < z := by
private theorem int_pos_iff (z : ℤ) : (∃ n : ℕ, z = (n : ℤ) + 1) ↔ 0 < z := by
constructor
· rintro ⟨n, rfl⟩; omega
· intro h; exact ⟨(z - 1).toNat, by omega⟩
/-- Dually, `∃ n : ℕ, z = -(n + 1)` just means `z` is negative. -/
private lemma int_neg_iff (z : ℤ) : (∃ n : ℕ, z = -((n : ℤ) + 1)) ↔ z < 0 := by
private theorem int_neg_iff (z : ℤ) : (∃ n : ℕ, z = -((n : ℤ) + 1)) ↔ z < 0 := by
constructor
· rintro ⟨n, rfl⟩; omega
· intro h; exact ⟨(-z - 1).toNat, by omega⟩
lemma plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
theorem plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
(h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
⟦plus g₁ g₂⟧ (.int (z₁ + z₂)) := by
rcases g₁ with _ | _ | s₁ <;> rcases g₂ with _ | _ | s₂ <;>
@@ -168,7 +172,7 @@ lemma plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
at h₁ h₂ ⊢ <;>
omega
lemma minus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
theorem minus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
(h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
⟦minus g₁ g₂⟧ (.int (z₁ - z₂)) := by
rcases g₁ with _ | _ | s₁ <;> rcases g₂ with _ | _ | s₂ <;>
@@ -211,14 +215,7 @@ instance eval_valid : ValidExprEvaluator SignLattice prog := by
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) :
⟦ joinForKey s (result SignLattice prog) ⟧ ρin
∧ ⟦ variablesAt s (result SignLattice prog) ⟧ ρout :=
Forward.analyze_correct_at SignLattice prog hrun hr
Spa.analyze_correct SignLattice prog hrun
end SignAnalysis

2
lean/Spa/Analysis/Utils.lean
View File

@@ -2,7 +2,7 @@ import Spa.Lattice
namespace Spa
lemma eval_combine₂ {O : Type*} [Preorder O] {combine : O → O → O}
theorem eval_combine₂ {O : Type*} [Preorder O] {combine : O → O → O}
(hmono : Monotone₂ combine) {o₁ o₂ o₃ o₄ : O}
(h₁ : o₁ ≤ o₃) (h₂ : o₂ ≤ o₄) : combine o₁ o₂ ≤ combine o₃ o₄ :=
le_trans (hmono.1 o₂ h₁) (hmono.2 o₃ h₂)

20
lean/Spa/Fixedpoint.lean
View File

@@ -1,12 +1,10 @@
import Spa.Lattice
namespace Spa
namespace Fixedpoint
namespace Spa.Fixedpoint
open FiniteHeightLattice (height)
variable {α : Type*} [DecidableEq α] [FiniteHeightLattice α]
variable {α : Type*} [Lattice α] [DecidableEq α] [FiniteHeightLattice α]
def doStep (f : α → α) (hf : Monotone f) :
∀ (g : ℕ) (c : LTSeries α), c.length + g = height (α := α) + 1 →
@@ -24,7 +22,8 @@ def doStep (f : α → α) (hf : Monotone f) :
def fix (f : α → α) (hf : Monotone f) : {a : α // a = f a} :=
doStep f hf (height (α := α) + 1) (RelSeries.singleton _ ⊥)
(by simp)
(by simp)
(by simpa [RelSeries.last_singleton]
using FiniteHeightLattice.bot_le α (f ⊥))
def aFix (f : α → α) (hf : Monotone f) : α :=
(fix f hf).1
@@ -33,13 +32,12 @@ theorem aFix_eq (f : α → α) (hf : Monotone f) :
aFix f hf = f (aFix f hf) :=
(fix f hf).2
lemma doStep_le (f : α → α) (hf : Monotone f)
theorem doStep_le (f : α → α) (hf : Monotone f)
{b : α} (hb : b = f b) :
∀ (g : ℕ) (c : LTSeries α) (hlen : c.length + g = height (α := α) + 1)
(hle : c.last ≤ f c.last), c.last ≤ b →
(doStep f hf g c hlen hle : α) ≤ b
| 0, c, hlen, _ => fun _ =>
absurd (FiniteHeightLattice.chains_bounded c) (by omega)
| 0, c, hlen, _ => fun _ => absurd (FiniteHeightLattice.chains_bounded c) (by omega)
| g + 1, c, hlen, hle => fun hcb => by
rw [doStep]
split
@@ -49,8 +47,6 @@ lemma doStep_le (f : α → α) (hf : Monotone f)
theorem aFix_le (f : α → α) (hf : Monotone f)
{a : α} (ha : a = f a) : aFix f hf ≤ a :=
doStep_le f hf ha _ _ _ _ (by simp)
doStep_le f hf ha _ _ _ _ (by simpa using FiniteHeightLattice.bot_le α a)
end Fixedpoint
end Spa
end Spa.Fixedpoint

10
lean/Spa/Interp.lean
View File

@@ -1,17 +1,7 @@
import Mathlib.Tactic.TypeStar
/-!
# Interpretation to a Semantic Domain
This file serves to introduce the double-angle-bracket "denotation"
notation by prodiving a class instance `Interp`, whose single
method `interp` is what the double brackets map to. -/
namespace Spa
/-- A type `α` that implements this class has denotation / meaning
in the semantic domain `dom`. -/
class Interp (α : Type*) (dom : outParam Type*) where
interp : α → dom

24
lean/Spa/Isomorphism.lean Normal file
View File

@@ -0,0 +1,24 @@
import Spa.Lattice
namespace Spa
def FiniteHeightLattice.transport {α β : Type*} [Lattice α] [Lattice β]
[I : FiniteHeightLattice α] (f : α → β) (g : β → α)
(hf : Monotone f) (hg : Monotone g)
(hgf : ∀ a, g (f a) = a) (hfg : ∀ b, f (g b) = b) :
FiniteHeightLattice β where
bot := f ⊥
top := f ⊤
height := I.height
longestChain :=
{ series :=
I.longestChain.series.map f
(hf.strictMono_of_injective (Function.LeftInverse.injective hgf))
head_series := congrArg f I.longestChain.head_series
last_series := congrArg f I.longestChain.last_series
length_series := I.longestChain.length_series }
chains_bounded := fun c =>
I.chains_bounded
(c.map g (hg.strictMono_of_injective (Function.LeftInverse.injective hfg)))
end Spa

54
lean/Spa/Language.lean
View File

@@ -3,4 +3,56 @@ import Spa.Language.Semantics
import Spa.Language.Graphs
import Spa.Language.Traces
import Spa.Language.Properties
import Spa.Language.Program
import Mathlib.Data.Finset.Sort
import Mathlib.Data.String.Basic
namespace Spa
structure Program where
rootStmt : Stmt
namespace Program
variable (p : Program)
def graph : Graph := Graph.wrap (buildCfg p.rootStmt)
abbrev State : Type := p.graph.Index
def initialState : p.State := (buildCfg p.rootStmt).wrapInput
def finalState : p.State := (buildCfg p.rootStmt).wrapOutput
theorem trace {ρ : Env} (h : EvalStmt [] p.rootStmt ρ) :
Trace p.graph p.initialState p.finalState [] ρ := by
obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := EndToEndTrace.wrap (buildCfg_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 (· ≤ ·)
theorem vars_nodup : p.vars.Nodup := Finset.sort_nodup _ _
def states : List p.State := p.graph.indices
theorem states_complete (s : p.State) : s ∈ p.states := p.graph.mem_indices s
theorem states_nodup : p.states.Nodup := p.graph.nodup_indices
def code (st : p.State) : List BasicStmt := p.graph.nodes st
def incoming (s : p.State) : List p.State := p.graph.predecessors s
theorem incoming_initialState_eq_nil : p.incoming p.initialState = [] :=
Graph.wrap_predecessors_eq_nil (buildCfg p.rootStmt) p.initialState
(by rw [Graph.wrap_inputs]; exact List.mem_singleton_self _)
theorem mem_incoming_of_edge {s₁ s₂ : p.State}
(h : (s₁, s₂) ∈ p.graph.edges) : s₁ ∈ p.incoming s₂ :=
p.graph.mem_predecessors_of_edge h
end Program
end Spa

33
lean/Spa/Language/Base.lean
View File

@@ -1,19 +1,7 @@
import Mathlib.Data.Finset.Basic
/-!
# Base Language
This file defines the core object language for the program analysis and
transformation. It's a very basic imperative language. The `Spa/Language/Tagged/Basic.lean`
file provides an auto-derived version of the `Expr`, `BasicStmt`, and `Stmt` data
types with unique IDs per condtructor, enabling in-AST pointers.
-/
namespace Spa
/-- A value-producing expression. Currently, this cannot have side effects. -/
inductive Expr where
| add (e₁ e₂ : Expr)
| sub (e₁ e₂ : Expr)
@@ -21,15 +9,11 @@ inductive Expr where
| num (n : ℕ)
deriving DecidableEq
/-- A statement that cannot alter control flow (and thus, can be part of a basic block).
This differs from, e.g., a loop, which can cause execution to jump to its top several times. -/
inductive BasicStmt where
| assign (x : String) (e : Expr)
| noop
deriving DecidableEq
/-- Any statements, which may or may not change program state (variable assignments). -/
inductive Stmt where
| basic (bs : BasicStmt)
| andThen (s₁ s₂ : Stmt)
@@ -37,23 +21,34 @@ inductive Stmt where
| whileLoop (e : Expr) (s : Stmt)
deriving DecidableEq
/-- Variables mentioned in this expression. -/
inductive Expr.HasVar : String → Expr → Prop
| addLeft {e₁ e₂ k} : Expr.HasVar k e₁ → Expr.HasVar k (.add e₁ e₂)
| addRight {e₁ e₂ k} : Expr.HasVar k e₂ → Expr.HasVar k (.add e₁ e₂)
| subLeft {e₁ e₂ k} : Expr.HasVar k e₁ → Expr.HasVar k (.sub e₁ e₂)
| subRight {e₁ e₂ k} : Expr.HasVar k e₂ → Expr.HasVar k (.sub e₁ e₂)
| here {k} : Expr.HasVar k (.var k)
inductive BasicStmt.HasVar : String → BasicStmt → Prop
| assignLeft {k e} : BasicStmt.HasVar k (.assign k e)
| assignRight {k k' e} : Expr.HasVar k e → BasicStmt.HasVar k (.assign k' e)
def Expr.vars : Expr → Finset String
| .add l r => l.vars ∪ r.vars
| .sub l r => l.vars ∪ r.vars
| .var s => {s}
| .num _ => ∅
/-- Variables assigned or mentioned in this basic statement. -/
def BasicStmt.vars : BasicStmt → Finset String
| .assign x e => {x} ∪ e.vars
| .noop => ∅
/-- Variables assigned or mentioned in this statement. -/
def Stmt.vars : Stmt → Finset String
| .basic bs => bs.vars
| .andThen s₁ s₂ => s₁.vars ∪ s₂.vars
| .ifElse e s₁ s₂ => (e.vars ∪ s₁.vars) ∪ s₂.vars
| .whileLoop e s => e.vars ∪ s.vars
def Stmt.varsList (ss : List Stmt) : Finset String :=
ss.foldr (fun s acc => s.vars ∪ acc) ∅
end Spa

356
lean/Spa/Language/Graphs.lean
View File

@@ -3,113 +3,45 @@ import Mathlib.Data.Fin.Tuple.Basic
import Mathlib.Data.List.ProdSigma
import Mathlib.Data.List.FinRange
/-!
# Algebraic Control Flow Graphs
This file defines control flow graphs and operations to naturally compose them,
making it possible to inductively covnert a program in the object language
(see `Spa.Stmt` in `Spa/Language/Base.lean`) into its corresponding graph.
Graphs are, in general, parameterized by their "payload" (the per-node data); see `GGraph`.
This is useful because other operations, such as finding the CFG node corresponding
to an AST node, are performed by embellishing a graph's basic blocks with their AST
identifiers.
The operations are deliberately a little bit sloppy here, creating empty / statement-less
CFG nodes. Additionally, the current CFG construction algorithm doesn't group
consecutive statements in a single notional basic block into one node.
This makes graph construction much easier to define, and might save us the
trouble of (when trying to find the CFG node for an AST node) doing
indexing into a list.
-/
/-- Logically, when combining `Fin`s from two distinct pools,
the combination is disjoint. -/
lemma Fin.castAdd_ne_natAdd {n m : ℕ} (i : Fin n) (j : Fin m) :
Fin.castAdd m i ≠ Fin.natAdd n j := by
intro h
have := congrArg Fin.val h
simp only [Fin.coe_castAdd, Fin.coe_natAdd] at this
omega
/-- Bump the upper bound of a list of `Fin`s without changing their value. -/
def List.finCastAdd {n : ℕ} (l : List (Fin n)) (m : ℕ) : List (Fin (n + m)) :=
l.map (Fin.castAdd m)
/-- Bump the upper bound of a list of `Fin`s by adding the amount to their value. -/
def List.finNatAdd {m : ℕ} (l : List (Fin m)) (n : ℕ) : List (Fin (n + m)) :=
l.map (Fin.natAdd n)
/-- Bump the upper bound of a list of `Fin` pairs without changing their value. -/
def List.finCastAddProd {n : ℕ} (l : List (Fin n × Fin n)) (m : ℕ) :
List (Fin (n + m) × Fin (n + m)) :=
l.map (fun e => (e.1.castAdd m, e.2.castAdd m))
/-- Bump the upper bound of a list of `Fin` pairs by adding the amount to their value. -/
def List.finNatAddProd {m : ℕ} (l : List (Fin m × Fin m)) (n : ℕ) :
List (Fin (n + m) × Fin (n + m)) :=
l.map (fun e => (e.1.natAdd n, e.2.natAdd n))
namespace Spa
/-- Graph with general (`α`-labeled) nodes. By using a tuple `Fin size → α`
and writing `edges` over the `Fin size`, guarantees all edges are between real nodes.
To make graph composition via operations not force a
[`alga`](https://hackage.haskell.org/package/algebraic-graphs)-style "connect"-based
algebra, explicitly defines `inputs` and `outputs`, which are the only nodes that
get connected when graphs are sequenced. This makes the graph construction
operations more naturally fit with how CFGs are created from `Stmt`s. -/
structure GGraph (α : Type) where
structure Graph where
size : ℕ
nodes : Fin size → α
nodes : Fin size → List BasicStmt
edges : List (Fin size × Fin size)
inputs : List (Fin size)
outputs : List (Fin size)
namespace GGraph
namespace Graph
variable {α β : Type}
abbrev Index (g : Graph) : Type := Fin g.size
/-- An index (node) in the CFG. -/
abbrev Index (g : GGraph α) : Type := Fin g.size
abbrev Edge (g : Graph) : Type := g.Index × g.Index
/-- An edge in the CFG. -/
abbrev Edge (g : GGraph α) : Type := g.Index × g.Index
instance : Functor GGraph where
map {α β : Type} (f : α → β) (g : GGraph α) : GGraph β :=
{ size := g.size,
nodes := f ∘ g.nodes
edges := g.edges,
inputs := g.inputs,
outputs := g.outputs }
@[simp] lemma map_size (f : α → β) (g : GGraph α) : (f <$> g).size = g.size := rfl
@[simp] lemma map_edges (f : α → β) (g : GGraph α) : (f <$> g).edges = g.edges := rfl
@[simp] lemma map_inputs (f : α → β) (g : GGraph α) : (f <$> g).inputs = g.inputs := rfl
@[simp] lemma map_outputs (f : α → β) (g : GGraph α) : (f <$> g).outputs = g.outputs := rfl
/-- Overlay two graphs: create a new graph whose nodes and edges come from two
sub-graphs, without inserting any additional edges. Also combines the
input and output node sets. -/
def overlay (g₁ g₂ : GGraph α) : GGraph α where
def comp (g₁ g₂ : Graph) : Graph where
size := g₁.size + g₂.size
nodes := Fin.append g₁.nodes g₂.nodes
edges := g₁.edges.finCastAddProd g₂.size ++ g₂.edges.finNatAddProd g₁.size
inputs := g₁.inputs.finCastAdd g₂.size ++ g₂.inputs.finNatAdd g₁.size
outputs := g₁.outputs.finCastAdd g₂.size ++ g₂.outputs.finNatAdd g₁.size
@[inherit_doc] scoped infixr:70 " ∙ " => GGraph.overlay
@[inherit_doc] scoped infixr:70 " ∙ " => Graph.comp
/-- Sequence two CFGs: create a combined graph whose nodes and edges come
from two subgraphs, __and__ make all the outputs of the left graph have edges to
all the inputs of the right graph. By the semantics of CFGs, this
encodes the fact that code first traverses the basic blocks in theleft
graph, and does the same for the right graph. -/
def sequence (g₁ g₂ : GGraph α) : GGraph α where
def link (g₁ g₂ : Graph) : Graph where
size := g₁.size + g₂.size
nodes := Fin.append g₁.nodes g₂.nodes
edges := g₁.edges.finCastAddProd g₂.size ++ g₂.edges.finNatAddProd g₁.size ++
@@ -117,244 +49,78 @@ def sequence (g₁ g₂ : GGraph α) : GGraph α where
inputs := g₁.inputs.finCastAdd g₂.size
outputs := g₂.outputs.finNatAdd g₁.size
@[inherit_doc] scoped infixr:70 " ⤳ " => GGraph.sequence
@[inherit_doc] scoped infixr:70 " ⤳ " => Graph.link
/-- When a graph `g` is wrapped in a `loop`, the index / node corresponding
to the input of the new loop. -/
def loopIn (g : GGraph α) : Fin (2 + g.size) := (0 : Fin 2).castAdd g.size
/-- The entry node of a `loop` graph. -/
def loopIn (g : Graph) : Fin (2 + g.size) := (0 : Fin 2).castAdd g.size
/-- When a graph `g` is wrapped in a `loop`, the index / node corresponding
to the output of the new loop. -/
def loopOut (g : GGraph α) : Fin (2 + g.size) := (1 : Fin 2).castAdd g.size
/-- The exit node of a `loop` graph. -/
def loopOut (g : Graph) : Fin (2 + g.size) := (1 : Fin 2).castAdd g.size
/-- Creates a zero-or-more loop loop in the CFG: connects all the output
nodes of the CFG back to the graph's beginning, and also introduces a path
to a new ending node (see `loopOut`) which bypasses the entire graph.
Notably, both the new input (`loopIn`) and new output (`loopOut`)
nodes are necessary for correctness: adding a path from inputs to a
hypothetical no-op end node encodes something like "just the first statement is executed".
Similarly, just adding a path from a a hypothetical no-op beginning node
to the outputs encodes "just the last statement is executed".
This is technically sloppy (see module comment), but it's simple.
-/
def loop (g : GGraph (Option β)) : GGraph (Option β) where
def loop (g : Graph) : Graph where
size := 2 + g.size
nodes := Fin.append (fun _ : Fin 2 => none) g.nodes
nodes := Fin.append (fun _ : Fin 2 => []) g.nodes
edges := g.edges.finNatAddProd 2 ++
((g.loopIn, ·) <$> g.inputs.finNatAdd 2) ++
((·, g.loopOut) <$> g.outputs.finNatAdd 2) ++
(g.inputs.finNatAdd 2).map (g.loopIn, ·) ++
(g.outputs.finNatAdd 2).map (·, g.loopOut) ++
[(g.loopOut, g.loopIn), (g.loopIn, g.loopOut)]
inputs := [g.loopIn]
outputs := [g.loopOut]
@[simp] lemma loop_inputs (g : GGraph (Option β)) : (loop g).inputs = [g.loopIn] := rfl
@[simp] theorem loop_inputs (g : Graph) : (loop g).inputs = [g.loopIn] := rfl
@[simp] lemma loop_outputs (g : GGraph (Option β)) : (loop g).outputs = [g.loopOut] := rfl
@[simp] theorem loop_outputs (g : Graph) : (loop g).outputs = [g.loopOut] := rfl
/-- Creates a single-node graph whose node contains the given value. -/
def singleton (a : α) : GGraph α where
def skipto (g₁ g₂ : Graph) : Graph where
size := g₁.size + g₂.size
nodes := Fin.append g₁.nodes g₂.nodes
edges := g₁.edges.finCastAddProd g₂.size ++ g₂.edges.finNatAddProd g₁.size ++
(g₁.inputs.finCastAdd g₂.size).product (g₂.inputs.finNatAdd g₁.size)
inputs := g₁.inputs.finCastAdd g₂.size
outputs := g₂.inputs.finNatAdd g₁.size
def singleton (bss : List BasicStmt) : Graph where
size := 1
nodes := fun _ => a
nodes := fun _ => bss
edges := []
inputs := [0]
outputs := [0]
/-- Creates a new graph with a single input and single output node. Useful to ensure there's
a single point of entry and single point of exit. -/
def wrap (g : GGraph (Option β)) : GGraph (Option β) :=
singleton none ⤳ g ⤳ singleton none
/-- The input / entry node generated by `GGraph.wrap`. -/
def wrapInput (g : GGraph (Option β)) : (wrap g).Index :=
(0 : Fin 1).castAdd ((g ⤳ singleton none).size)
/-- The output / exit node generated by `GGraph.wrap`. -/
def wrapOutput (g : GGraph (Option β)) : (wrap g).Index :=
Fin.natAdd 1 ((Fin.natAdd g.size (0 : Fin 1)))
/-- The `wrapInput` is, indeed, the graph's only input after `wrap`. -/
lemma wrap_inputs (g : GGraph (Option β)) :
(wrap g).inputs = [g.wrapInput] := rfl
/-- The `wrapInput` is, indeed, the graph's only output after `wrap`. -/
lemma wrap_outputs (g : GGraph (Option β)) :
(wrap g).outputs = [g.wrapOutput] := rfl
@[simp] lemma map_singleton (f : α → β) (a : α) :
f <$> singleton a = singleton (f a) := rfl
@[simp] lemma map_overlay (f : α → β) (g₁ g₂ : GGraph α) :
f<$> (g₁ ∙ g₂) = f <$> g₁ ∙ f <$> g₂ := by
rcases g₁ with ⟨n₁, nd₁, e₁, i₁, o₁⟩; rcases g₂ with ⟨n₂, nd₂, e₂, i₂, o₂⟩
simp only [Functor.map, GGraph.overlay]
congr 1
funext i
refine Fin.addCases ?_ ?_ i <;> intro j <;> simp [Fin.append_left, Fin.append_right]
@[simp] lemma map_sequence (f : α → β) (g₁ g₂ : GGraph α) :
f <$> (g₁ ⤳ g₂) = (f <$> g₁) ⤳ (f <$> g₂) := by
rcases g₁ with ⟨n₁, nd₁, e₁, i₁, o₁⟩; rcases g₂ with ⟨n₂, nd₂, e₂, i₂, o₂⟩
simp only [Functor.map, GGraph.sequence]
congr 1
funext i
refine Fin.addCases ?_ ?_ i <;> intro j <;> simp [Fin.append_left, Fin.append_right]
@[simp] lemma map_loop (h : β → γ) (g : GGraph (Option β)) :
(Option.map h) <$> (loop g) = loop (Option.map h <$> g) := by
rcases g with ⟨n, nd, e, i, o⟩
simp only [Functor.map, GGraph.loop]
congr 1
funext i
refine Fin.addCases ?_ ?_ i <;> intro j <;> simp [Fin.append_left, Fin.append_right]
@[simp] lemma map_wrap (h : β → γ) (g : GGraph (Option β)) :
(Option.map h) <$> wrap g = wrap (Option.map h <$> g) := by
simp [GGraph.wrap, GGraph.map_sequence, GGraph.map_singleton]
/-! ### Embeddings
Each composition operator includes its operands into the result via an index
translation that preserves node payloads and edges. `Embed` captures exactly
those two facts, so anything defined from `nodes` and `edges` (traces, node
labels, …) can be transported along an embedding once, instead of once per
operator.
`Embed` is deliberately a structure rather than a class: for `g ⤳ g`, both the
left and the right inclusion inhabit the same type `Embed g (g ⤳ g)`, so
instance resolution could silently pick the wrong copy. Embeddings into a
composed graph are non-canonical by design; a named witness says which
inclusion is meant. -/
/-- An embedding of graph `g` into graph `h`: an index translation that
preserves node payloads and edges. -/
structure Embed (g h : GGraph α) where
f : g.Index → h.Index
nodes_eq : ∀ i, h.nodes (f i) = g.nodes i
edges_mem : ∀ {e : g.Edge}, e ∈ g.edges → (f e.1, f e.2) ∈ h.edges
/-- Embeddings compose. -/
def Embed.trans {g₁ g₂ g₃ : GGraph α} (e₁ : Embed g₁ g₂) (e₂ : Embed g₂ g₃) :
Embed g₁ g₃ where
f := e₂.f ∘ e₁.f
nodes_eq i := (e₂.nodes_eq (e₁.f i)).trans (e₁.nodes_eq i)
edges_mem he := e₂.edges_mem (e₁.edges_mem he)
/-- The left operand's inclusion into a sequenced graph. -/
def Embed.sequenceLeft (g₁ g₂ : GGraph α) : Embed g₁ (g₁ ⤳ g₂) where
f i := i.castAdd g₂.size
nodes_eq i := Fin.append_left g₁.nodes g₂.nodes i
edges_mem he := List.mem_append_left _ (List.mem_append_left _ (List.mem_map_of_mem _ he))
/-- The right operand's inclusion into a sequenced graph. -/
def Embed.sequenceRight (g₁ g₂ : GGraph α) : Embed g₂ (g₁ ⤳ g₂) where
f i := i.natAdd g₁.size
nodes_eq i := Fin.append_right g₁.nodes g₂.nodes i
edges_mem he := List.mem_append_left _ (List.mem_append_right _ (List.mem_map_of_mem _ he))
/-- The left operand's inclusion into an overlaid graph. -/
def Embed.overlayLeft (g₁ g₂ : GGraph α) : Embed g₁ (g₁ ∙ g₂) where
f i := i.castAdd g₂.size
nodes_eq i := Fin.append_left g₁.nodes g₂.nodes i
edges_mem he := List.mem_append_left _ (List.mem_map_of_mem _ he)
/-- The right operand's inclusion into an overlaid graph. -/
def Embed.overlayRight (g₁ g₂ : GGraph α) : Embed g₂ (g₁ ∙ g₂) where
f i := i.natAdd g₁.size
nodes_eq i := Fin.append_right g₁.nodes g₂.nodes i
edges_mem he := List.mem_append_right _ (List.mem_map_of_mem _ he)
/-- The body's inclusion into a `loop` graph. -/
def Embed.loop (g : GGraph (Option β)) : Embed g (loop g) where
f i := i.natAdd 2
nodes_eq i := Fin.append_right (fun _ : Fin 2 => none) g.nodes i
edges_mem he := List.mem_append_left _ (List.mem_append_left _
(List.mem_append_left _ (List.mem_map_of_mem _ he)))
variable (g : GGraph α)
/-- All the nodes in the graph. -/
def indices : List g.Index := List.finRange g.size
/-- All of the graph's indices are listed in `indices`. -/
lemma mem_indices (idx : g.Index) : idx ∈ g.indices :=
List.mem_finRange idx
/-- `indices` does not have duplicates. -/
lemma nodup_indices : g.indices.Nodup :=
List.nodup_finRange g.size
/-- Predecessors of a particular node in the graph. --/
def predecessors (idx : g.Index) : List g.Index :=
g.indices.filter (fun idx' => (idx', idx) ∈ g.edges)
/-- 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₂ : GGraph (Option β)} (i : Fin 1)
(idx : (singleton none ⤳ g₂).Index) :
((idx, i.castAdd g₂.size) : (singleton none ⤳ g₂).Edge)
∉ (singleton none ⤳ g₂).edges := by
intro h
rcases List.mem_append.mp h with h' | h'
· rcases List.mem_append.mp h' with h'' | h''
· -- lifted edges of `singleton []`: there are none
simp [singleton, List.finCastAddProd] at h''
· -- lifted edges of g₂: targets are natAdd
obtain ⟨e, _, heq⟩ := List.mem_map.mp h''
exact Fin.castAdd_ne_natAdd i e.2 (congrArg Prod.snd heq).symm
· -- product edges: targets are natAdd'd inputs of g₂
obtain ⟨-, hb⟩ := List.mem_product.mp h'
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 wrap_predecessors_eq_nil (g : GGraph (Option β)) (idx : (wrap g).Index)
(h : idx ∈ (wrap g).inputs) :
(wrap g).predecessors idx = [] := by
rw [wrap_inputs, List.mem_singleton] at h
subst h
rw [GGraph.predecessors, List.filter_eq_nil_iff]
intro idx' _
simpa using not_mem_edges_castAdd_sequence (g₂ := g ⤳ singleton none) 0 idx'
/-- There's there's an edge between two nodes `idx₁` and `idx₂`,
then `idx₁` is the predecessor of `idx₂`. -/
lemma mem_predecessors_of_edge {idx₁ idx₂ : g.Index}
(h : (idx₁, idx₂) ∈ g.edges) : idx₁ ∈ g.predecessors idx₂ :=
List.mem_filter.mpr ⟨g.mem_indices idx₁, by simpa using h⟩
/-- A node is a predecessor of another node only if there's an
edge between them. -/
lemma edge_of_mem_predecessors {idx₁ idx₂ : g.Index}
(h : idx₁ ∈ g.predecessors idx₂) : (idx₁, idx₂) ∈ g.edges := by
simpa using (List.mem_filter.mp h).2
end GGraph
/-- "Normal" graphs, for the purposes of the analyses in this
framework, have basic statements in their nodes, and nothing else. -/
abbrev Graph : Type := GGraph (Option BasicStmt)
namespace Graph
export GGraph (overlay sequence loop singleton wrap loop_inputs loop_outputs wrapInput wrapOutput wrap_inputs wrap_outputs)
@[inherit_doc] scoped infixr:70 " ∙ " => GGraph.overlay
@[inherit_doc] scoped infixr:70 " ⤳ " => GGraph.sequence
def wrap (g : Graph) : Graph :=
singleton [] ⤳ g ⤳ singleton []
end Graph
open Graph in
def Stmt.cfg : Stmt → Graph
-- A basic statement goes into a single basic block
| .basic bs => singleton (some bs)
-- Sequencing of statements corresponds naturally to CFG sequencing
| .andThen s₁ s₂ => s₁.cfg ⤳ s₂.cfg
-- An if can execute either one branch or the other; overlap them.
-- Subsequent sequencing (etc.) will end up creating the forks and joins.
| .ifElse _ s₁ s₂ => s₁.cfg ∙ s₂.cfg
-- The `loop` construct was developed specifically for zero-or-more loops like this.
| .whileLoop _ s => loop s.cfg
def buildCfg : Stmt → Graph
| .basic bs => Graph.singleton [bs]
| .andThen s₁ s₂ => buildCfg s₁ ⤳ buildCfg s₂
| .ifElse _ s₁ s₂ => buildCfg s₁ ∙ buildCfg s₂
| .whileLoop _ s => Graph.loop (buildCfg s)
namespace Graph
variable (g : Graph)
def indices : List g.Index := List.finRange g.size
theorem mem_indices (idx : g.Index) : idx ∈ g.indices :=
List.mem_finRange idx
theorem nodup_indices : g.indices.Nodup :=
List.nodup_finRange g.size
def predecessors (idx : g.Index) : List g.Index :=
g.indices.filter (fun idx' => (idx', idx) ∈ g.edges)
theorem mem_predecessors_of_edge {idx₁ idx₂ : g.Index}
(h : (idx₁, idx₂) ∈ g.edges) : idx₁ ∈ g.predecessors idx₂ :=
List.mem_filter.mpr ⟨g.mem_indices idx₁, by simpa using h⟩
theorem edge_of_mem_predecessors {idx₁ idx₂ : g.Index}
(h : idx₁ ∈ g.predecessors idx₂) : (idx₁, idx₂) ∈ g.edges := by
simpa using (List.mem_filter.mp h).2
end Graph
end Spa

77
lean/Spa/Language/Program.lean
View File

@@ -1,77 +0,0 @@
import Spa.Language.Base
import Spa.Language.Semantics
import Spa.Language.Graphs
import Mathlib.Data.Finset.Sort
import Mathlib.Data.String.Basic
namespace Spa
/-- A self-contained program to be evaluated, analyzed, and transformed. -/
structure Program where
/-- The statement at the top level of the program. Since `Spa.Stmt` contains
sequencing via `Spa.Stmt.andThen`, this can encode any number of
statements. -/
rootStmt : Stmt
/-- A memoized copy of the control-flow graph. This field is an
implementation detail to avoid re-computing `Spa.GGraph.wrap` and `Spa.Stmt.cfg`
every time the program's control flow graph is needed -/
cfgCache : Thunk Graph := Thunk.mk fun _ => Graph.wrap rootStmt.cfg
namespace Program
variable (p : Program)
-- Runtime implementation of `cfg`: read the memoized graph.
private def cfgImpl : Graph := p.cfgCache.get
/-- The control flow graph corresponding to this graph. -/
@[implemented_by cfgImpl]
def cfg : Graph := Graph.wrap p.rootStmt.cfg
/-- A state in the control flow `Spa.Graph` of this program. -/
abbrev State : Type := p.cfg.Index
/-- Variables mentioned or defined in this program. -/
def vars : List String := p.rootStmt.vars.sort (· ≤ ·)
/-- `vars` has no duplicates. -/
lemma vars_nodup : p.vars.Nodup := Finset.sort_nodup _ _
/-- All the states in the program's control flow `Spa.Graph`. -/
def states : List p.State := p.cfg.indices
/-- All states in the CFG are contained in `states`. -/
lemma states_complete (s : p.State) : s ∈ p.states := p.cfg.mem_indices s
/-- `states` has no duplicates. -/
lemma states_nodup : p.states.Nodup := p.cfg.nodup_indices
/-- Given a node of the program's CFG, return the code at that node.
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. -/
def incoming (s : p.State) : List p.State := p.cfg.predecessors s
/-- The entry point of the program's CFG. -/
def initialState : p.State := Graph.wrapInput p.rootStmt.cfg
/-- The exit point of the program's CFG. -/
def finalState : p.State := Graph.wrapOutput p.rootStmt.cfg
/-- `incoming` is a faithful representation of edges in the CFG. -/
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
/-- The `initialState` has no incoming edges (it's the program start). -/
lemma incoming_initialState_eq_nil : p.incoming p.initialState = [] :=
GGraph.wrap_predecessors_eq_nil p.rootStmt.cfg p.initialState
(by rw [Graph.wrap_inputs]; exact List.mem_singleton_self _)
end Program
end Spa

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

@@ -1,126 +1,126 @@
import Spa.Language.Traces
/-!
# Properties of the Object Language, CFGs, and Traces
This module encodes some properties of the language, mostly those having to do
with connecting the computational view (the `Spa.Graph`s, on which static
analyses are executed) to the semantic view (such as `EvalStmt`, which
encodes the expected formal behavior of the language). In particular,
to prove that our computationally-implemented static analyses are correct,
we need to show that our computational model of their execution (the CFG)
matches the formal description. Thus, the key result `cfg_sufficient`.
Many lemmas and definitions here aim are used to prove that result,
by allowing inductive proofs on the construction of the CFG:
the bits where we _build up_ the trace corresponding to each
proof tree are exactly those when we have two graphs (through
which traces exist) and we want to combine these graphs, while
showing also that a combined trace exists as well. -/
namespace Spa
open Graph
theorem Fin.castAdd_ne_natAdd {n m : ℕ} (i : Fin n) (j : Fin m) :
Fin.castAdd m i ≠ Fin.natAdd n j := by
intro h
have := congrArg Fin.val h
simp only [Fin.coe_castAdd, Fin.coe_natAdd] at this
omega
/-! ### Trace embeddings -/
section Embeddings
variable {g₁ g₂ : Graph} {ρ₁ ρ₂ : Env}
/-- Transport a trace along a graph embedding: an embedding preserves node
payloads and edges, which is everything a trace is made of. This is the
single induction behind all the per-operator lifting corollaries below. -/
noncomputable def Trace.embed {g h : Graph} (e : GGraph.Embed g h)
{idx₁ idx₂ : g.Index} (tr : Trace g idx₁ idx₂ ρ₁ ρ₂) :
Trace h (e.f idx₁) (e.f idx₂) ρ₁ ρ₂ := by
theorem Trace.comp_left {idx₁ idx₂ : g₁.Index}
(tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) :
Trace (g₁ ∙ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by
induction tr with
| single hbs => exact Trace.single (by rwa [e.nodes_eq])
| edge hbs he _ ih => exact Trace.edge (by rwa [e.nodes_eq]) (e.edges_mem he) ih
| single hbs =>
exact Trace.single (by rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl,
Fin.append_left])
| edge hbs he _ ih =>
refine Trace.edge ?_ ?_ ih
· rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_left]
· exact List.mem_append_left _ (List.mem_map_of_mem _ he)
/-- When two graphs are overlaid, for each trace in the left graph,
a corresponding trace exists in the combined graph. -/
noncomputable def Trace.overlay_left {idx₁ idx₂ : g₁.Index}
(tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) :
Trace (g₁ ∙ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ :=
tr.embed (GGraph.Embed.overlayLeft g₁ g₂)
/-- When two graphs are overlaid, for each trace in the right graph,
a corresponding trace exists in the combined graph. -/
noncomputable def Trace.overlay_right {idx₁ idx₂ : g₂.Index}
theorem Trace.comp_right {idx₁ idx₂ : g₂.Index}
(tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) :
Trace (g₁ ∙ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ :=
tr.embed (GGraph.Embed.overlayRight g₁ g₂)
Trace (g₁ ∙ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by
induction tr with
| single hbs =>
exact Trace.single (by rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl,
Fin.append_right])
| edge hbs he _ ih =>
refine Trace.edge ?_ ?_ ih
· rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_right]
· exact List.mem_append_right _ (List.mem_map_of_mem _ he)
/-- When two graphs are sequenced, for each trace in the first graph,
a corresponding trace exists in the combined graph. -/
noncomputable def Trace.sequence_left {idx₁ idx₂ : g₁.Index}
theorem Trace.link_left {idx₁ idx₂ : g₁.Index}
(tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) :
Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ :=
tr.embed (GGraph.Embed.sequenceLeft g₁ g₂)
Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by
induction tr with
| single hbs =>
exact Trace.single (by rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl,
Fin.append_left])
| edge hbs he _ ih =>
refine Trace.edge ?_ ?_ ih
· rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_left]
· exact List.mem_append_left _ (List.mem_append_left _ (List.mem_map_of_mem _ he))
/-- When two graphs are sequenced, for each trace in the second graph,
a corresponding trace exists in the combined graph. -/
noncomputable def Trace.sequence_right {idx₁ idx₂ : g₂.Index}
theorem Trace.link_right {idx₁ idx₂ : g₂.Index}
(tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) :
Trace (g₁ ⤳ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ :=
tr.embed (GGraph.Embed.sequenceRight g₁ g₂)
Trace (g₁ ⤳ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by
induction tr with
| single hbs =>
exact Trace.single (by rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl,
Fin.append_right])
| edge hbs he _ ih =>
refine Trace.edge ?_ ?_ ih
· rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_right]
· exact List.mem_append_left _
(List.mem_append_right _ (List.mem_map_of_mem _ he))
/-- Equivalent of `Trace.overlay_left` for end-to-end traces. -/
noncomputable def EndToEndTrace.overlay_left (etr : EndToEndTrace g₁ ρ₁ ρ₂) :
theorem EndToEndTrace.comp_left (etr : EndToEndTrace g₁ ρ₁ ρ₂) :
EndToEndTrace (g₁ ∙ g₂) ρ₁ ρ₂ := by
obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr
exact ⟨i₁.castAdd g₂.size, List.mem_append_left _ (List.mem_map_of_mem _ h₁),
i₂.castAdd g₂.size, List.mem_append_left _ (List.mem_map_of_mem _ h₂),
tr.overlay_left⟩
tr.comp_left⟩
/-- Equivalent of `Trace.overlay_right` for end-to-end traces. -/
noncomputable def EndToEndTrace.overlay_right (etr : EndToEndTrace g₂ ρ₁ ρ₂) :
theorem EndToEndTrace.comp_right (etr : EndToEndTrace g₂ ρ₁ ρ₂) :
EndToEndTrace (g₁ ∙ g₂) ρ₁ ρ₂ := by
obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr
exact ⟨i₁.natAdd g₁.size, List.mem_append_right _ (List.mem_map_of_mem _ h₁),
i₂.natAdd g₁.size, List.mem_append_right _ (List.mem_map_of_mem _ h₂),
tr.overlay_right⟩
tr.comp_right⟩
/-- When two graphs are sequenced, two end-to-end traces through the respective
graphs can be sequenced to create an end-to-end trace in the combined
graph. This is only possible for end-to-end traces and not for general
`Trace`s, because sequencing only introduces edges from the output nodes
of one graph to the input nodes of another graph. A non-end-to-end trace
need to conclude at the output node, so it cannot necessarily be sequenced
with a trace in another graph. -/
noncomputable def EndToEndTrace.concat {ρ₃ : Env} (etr₁ : EndToEndTrace g₁ ρ₁ ρ₂)
theorem EndToEndTrace.concat {ρ₃ : Env} (etr₁ : EndToEndTrace g₁ ρ₁ ρ₂)
(etr₂ : EndToEndTrace g₂ ρ₂ ρ₃) : EndToEndTrace (g₁ ⤳ g₂) ρ₁ ρ₃ := by
obtain ⟨i₁, h₁, i₂, h₂, tr₁⟩ := etr₁
obtain ⟨j₁, k₁, j₂, k₂, tr₂⟩ := etr₂
refine ⟨i₁.castAdd g₂.size, List.mem_map_of_mem _ h₁,
j₂.natAdd g₁.size, List.mem_map_of_mem _ k₂,
tr₁.sequence_left ++< ?_ >++ tr₂.sequence_right⟩
Trace.concat tr₁.link_left ?_ tr₂.link_right⟩
exact List.mem_append_right _
(List.mem_product.mpr ⟨List.mem_map_of_mem _ h₂, List.mem_map_of_mem _ k₁⟩)
end Embeddings
/-! ### Loops -/
section Loop
variable {g : Graph} {ρ₁ ρ₂ ρ₃ : Env}
/-- A trace through a body CFG still exists (up to reindexing) in a zero-or-more loop CFG. -/
noncomputable def Trace.loop {idx₁ idx₂ : g.Index} (tr : Trace g idx₁ idx₂ ρ₁ ρ₂) :
Trace (Graph.loop g) (idx₁.natAdd 2) (idx₂.natAdd 2) ρ₁ ρ₂ :=
tr.embed (GGraph.Embed.loop g)
theorem Trace.loop {idx₁ idx₂ : g.Index} (tr : Trace g idx₁ idx₂ ρ₁ ρ₂) :
Trace (Graph.loop g) (idx₁.natAdd 2) (idx₂.natAdd 2) ρ₁ ρ₂ := by
induction tr with
| single hbs =>
exact Trace.single (by
rwa [show (Graph.loop g).nodes = Fin.append (fun _ : Fin 2 => []) g.nodes from rfl,
Fin.append_right])
| edge hbs he _ ih =>
refine Trace.edge ?_ ?_ ih
· rwa [show (Graph.loop g).nodes = Fin.append (fun _ : Fin 2 => []) g.nodes from rfl,
Fin.append_right]
· exact List.mem_append_left _ (List.mem_append_left _
(List.mem_append_left _ (List.mem_map_of_mem _ he)))
/-- The beginning node of a loop graph is empty. -/
private lemma loop_nodes_at_in :
(Graph.loop g).nodes g.loopIn = none :=
Fin.append_left (fun _ : Fin 2 => none) g.nodes 0
private theorem loop_nodes_at_in :
(Graph.loop g).nodes g.loopIn = [] :=
Fin.append_left (fun _ : Fin 2 => []) g.nodes 0
/-- The ending node of a loop graph is empty. -/
private lemma loop_nodes_at_out :
(Graph.loop g).nodes g.loopOut = none :=
Fin.append_left (fun _ : Fin 2 => none) g.nodes 1
private theorem loop_nodes_at_out :
(Graph.loop g).nodes g.loopOut = [] :=
Fin.append_left (fun _ : Fin 2 => []) g.nodes 1
/-- Equivlaent of `Trace.loop` for end-to-end traces. -/
noncomputable def EndToEndTrace.loop (etr : EndToEndTrace g ρ₁ ρ₂) :
theorem EndToEndTrace.loop (etr : EndToEndTrace g ρ₁ ρ₂) :
EndToEndTrace (Graph.loop g) ρ₁ ρ₂ := by
obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr
-- the edge in → (2 ↑ʳ i₁), reached through the second edge group
@@ -132,17 +132,15 @@ noncomputable def EndToEndTrace.loop (etr : EndToEndTrace g ρ₁ ρ₂) :
refine List.mem_append_left _ (List.mem_append_right _ ?_)
exact List.mem_map_of_mem _ (List.mem_map_of_mem _ h₂)
refine ⟨g.loopIn, List.mem_singleton_self _, g.loopOut, List.mem_singleton_self _, ?_⟩
exact Trace.single (loop_nodes_at_in ▸ EvalBasicStmtOpt.none) ++< hin >++
tr.loop ++< hout >++ Trace.single (loop_nodes_at_out ▸ EvalBasicStmtOpt.none)
exact Trace.concat (Trace.single (loop_nodes_at_in ▸ EvalBasicStmts.nil)) hin
(Trace.concat tr.loop hout (Trace.single (loop_nodes_at_out ▸ EvalBasicStmts.nil)))
/-- The zero-or-more times loop has an edge to return back to the top, to continue after an iteration. -/
private lemma loop_edge_out_in :
private theorem loop_edge_out_in :
((g.loopOut, g.loopIn) : (Graph.loop g).Edge) ∈ (Graph.loop g).edges := by
refine List.mem_append_right _ ?_
exact List.mem_cons_self _ _
/-- Two traces through a loop can be combined, since a loop can be executed any number of times. -/
noncomputable def EndToEndTrace.loop_concat (etr₁ : EndToEndTrace (Graph.loop g) ρ₁ ρ₂)
theorem EndToEndTrace.loop_concat (etr₁ : EndToEndTrace (Graph.loop g) ρ₁ ρ₂)
(etr₂ : EndToEndTrace (Graph.loop g) ρ₂ ρ₃) :
EndToEndTrace (Graph.loop g) ρ₁ ρ₃ := by
obtain ⟨i₁, h₁, i₂, h₂, tr₁⟩ := etr₁
@@ -150,77 +148,86 @@ noncomputable def EndToEndTrace.loop_concat (etr₁ : EndToEndTrace (Graph.loop
simp only [Graph.loop_inputs, Graph.loop_outputs, List.mem_singleton] at h₁ h₂ k₁ k₂
subst h₁; subst h₂; subst k₁; subst k₂
exact ⟨g.loopIn, List.mem_singleton_self _, g.loopOut, List.mem_singleton_self _,
tr₁ ++< loop_edge_out_in >++ tr₂⟩
Trace.concat tr₁ loop_edge_out_in tr₂⟩
/-- A loop can be executed zero times. -/
noncomputable def EndToEndTrace.loop_empty {ρ : Env} : EndToEndTrace (Graph.loop g) ρ ρ := by
theorem EndToEndTrace.loop_empty {ρ : Env} : EndToEndTrace (Graph.loop g) ρ ρ := by
have hedge : ((g.loopIn, g.loopOut) : (Graph.loop g).Edge) ∈ (Graph.loop g).edges :=
List.mem_append_right _ (List.mem_cons_of_mem _ (List.mem_cons_self _ _))
exact ⟨g.loopIn, List.mem_singleton_self _, g.loopOut, List.mem_singleton_self _,
Trace.single (loop_nodes_at_in ▸ EvalBasicStmtOpt.none) ++< hedge >++
Trace.single (loop_nodes_at_out ▸ EvalBasicStmtOpt.none)⟩
Trace.concat (Trace.single (loop_nodes_at_in ▸ EvalBasicStmts.nil)) hedge
(Trace.single (loop_nodes_at_out ▸ EvalBasicStmts.nil))⟩
end Loop
/-- 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) ρ₁ ρ₂ :=
/-! ### Singletons, wrap, and the main result -/
theorem EndToEndTrace.singleton {bss : List BasicStmt} {ρ₁ ρ₂ : Env}
(h : EvalBasicStmts ρ₁ bss ρ₂) : EndToEndTrace (Graph.singleton bss) ρ₁ ρ₂ :=
⟨(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
theorem EndToEndTrace.singleton_nil (ρ : Env) :
EndToEndTrace (Graph.singleton []) ρ ρ :=
EndToEndTrace.singleton EvalBasicStmts.nil
/-- 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}
theorem 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
theorem buildCfg_sufficient {s : Stmt} {ρ₁ ρ₂ : Env}
(h : EvalStmt ρ₁ s ρ₂) : EndToEndTrace (buildCfg s) ρ₁ ρ₂ := by
induction h with
| basic ρ₁ ρ₂ bs hbs =>
exact EndToEndTrace.singleton (EvalBasicStmtOpt.some hbs)
exact EndToEndTrace.singleton (EvalBasicStmts.cons hbs EvalBasicStmts.nil)
| andThen ρ₁ ρ₂ ρ₃ s₁ s₂ _ _ ih₁ ih₂ =>
exact ih₁.concat ih₂
| ifTrue ρ₁ ρ₂ e z s₁ s₂ _ _ _ ih =>
exact ih.overlay_left
exact ih.comp_left
| ifFalse ρ₁ ρ₂ e s₁ s₂ _ _ ih =>
exact ih.overlay_right
exact ih.comp_right
| whileTrue ρ₁ ρ₂ ρ₃ e z s _ _ _ _ ih₁ ih₂ =>
exact (ih₁.loop).loop_concat ih₂
| whileFalse ρ e s _ =>
exact EndToEndTrace.loop_empty
namespace Program
/-! ### The wrapped graph's entry has no predecessors (Agda's "ugly" block) -/
noncomputable def trace (p : Program) {ρ : 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 Graph.wrapInput (g : Graph) : (Graph.wrap g).Index :=
(0 : Fin 1).castAdd ((g ⤳ Graph.singleton []).size)
end Program
def Graph.wrapOutput (g : Graph) : (Graph.wrap g).Index :=
Fin.natAdd 1 ((Fin.natAdd g.size (0 : Fin 1)))
theorem Graph.wrap_inputs (g : Graph) :
(Graph.wrap g).inputs = [g.wrapInput] := rfl
theorem Graph.wrap_outputs (g : Graph) :
(Graph.wrap g).outputs = [g.wrapOutput] := rfl
private theorem not_mem_edges_castAdd_link {g₂ : Graph} (i : Fin 1)
(idx : (Graph.singleton [] ⤳ g₂).Index) :
((idx, i.castAdd g₂.size) : (Graph.singleton [] ⤳ g₂).Edge)
∉ (Graph.singleton [] ⤳ g₂).edges := by
intro h
rcases List.mem_append.mp h with h' | h'
· rcases List.mem_append.mp h' with h'' | h''
· -- lifted edges of `singleton []`: there are none
simp [Graph.singleton, List.finCastAddProd] at h''
· -- lifted edges of g₂: targets are natAdd
obtain ⟨e, _, heq⟩ := List.mem_map.mp h''
exact Fin.castAdd_ne_natAdd i e.2 (congrArg Prod.snd heq).symm
· -- product edges: targets are natAdd'd inputs of g₂
obtain ⟨-, hb⟩ := List.mem_product.mp h'
obtain ⟨j, -, heq⟩ := List.mem_map.mp hb
exact Fin.castAdd_ne_natAdd i j heq.symm
theorem Graph.wrap_predecessors_eq_nil (g : Graph) (idx : (Graph.wrap g).Index)
(h : idx ∈ (Graph.wrap g).inputs) :
(Graph.wrap g).predecessors idx = [] := by
rw [Graph.wrap_inputs, List.mem_singleton] at h
subst h
rw [Graph.predecessors, List.filter_eq_nil_iff]
intro idx' _
simpa using not_mem_edges_castAdd_link (g₂ := g ⤳ Graph.singleton []) 0 idx'
end Spa

47
lean/Spa/Language/Semantics.lean
View File

@@ -2,27 +2,12 @@ import Spa.Language.Base
import Spa.Lattice
import Spa.Interp
/-!
# Operational Semantics
This file contains the operational semantics for the object language defined in
`Spa.Language.Base`. Right now, all values in the language are integers.
The semantics are big-step, and lead to a fully constructed proof tree
containing the derivation connecting the initial and final states.
All pretty standard.
-/
namespace Spa
/-- A value in the object language. Currently, the only possible case is
an integer. -/
inductive Value where
| int (z : ℤ)
deriving DecidableEq
/-- An environment mapping variables to their values. -/
def Env : Type := List (String × Value)
inductive Env.Mem : String × Value → Env → Prop
@@ -30,8 +15,6 @@ inductive Env.Mem : String × Value → Env → Prop
| there (s s' : String) (v v' : Value) (ρ : Env) :
¬(s = s') → Env.Mem (s, v) ρ → Env.Mem (s, v) ((s', v') :: ρ)
/-- Inference rules for evaluating an expression (`Spa.Expr`) in a given
environment. Pretty standard big-step expression evaluation. -/
inductive EvalExpr : Env → Expr → Value → Prop
| num (ρ : Env) (n : ℕ) : EvalExpr ρ (.num n) (.int n)
| var (ρ : Env) (x : String) (v : Value) :
@@ -43,25 +26,18 @@ inductive EvalExpr : Env → Expr → Value → Prop
EvalExpr ρ e₁ (.int z₁) → EvalExpr ρ e₂ (.int z₂) →
EvalExpr ρ (.sub e₁ e₂) (.int (z₁ - z₂))
/-- Inference rules for evaluating a basic statement (`Spa.BasicStmt`) in
a given environment, potentially changing the environment.
Pretty standard big-step evaluation. -/
inductive EvalBasicStmt : Env → BasicStmt → Env → Type
inductive EvalBasicStmt : Env → BasicStmt → Env → Prop
| noop (ρ : Env) : EvalBasicStmt ρ .noop ρ
| assign (ρ : Env) (x : String) (e : Expr) (v : Value) :
EvalExpr ρ e v → EvalBasicStmt ρ (.assign x e) ((x, v) :: ρ)
/-- Inference rules for evaluating a basic-statement-or-nothing,
which is the current representation of CFGs nodes. -/
inductive EvalBasicStmtOpt : Env → Option BasicStmt → Env → Type
| none {ρ : Env} : EvalBasicStmtOpt ρ Option.none ρ
| some {ρ₁ ρ₂ : Env} {bs : BasicStmt} :
EvalBasicStmt ρ₁ bs ρ₂ → EvalBasicStmtOpt ρ₁ (Option.some bs) ρ₂
inductive EvalBasicStmts : Env → List BasicStmt → Env → Prop
| nil {ρ : Env} : EvalBasicStmts ρ [] ρ
| cons {ρ₁ ρ₂ ρ₃ : Env} {bs : BasicStmt} {bss : List BasicStmt} :
EvalBasicStmt ρ₁ bs ρ₂ → EvalBasicStmts ρ₂ bss ρ₃ →
EvalBasicStmts ρ₁ (bs :: bss) ρ₃
/-- Inference rules for evaluating statements (`Spa.Stmt`) in a given
environment, potentially changing the environment.
Pretty standard big-step evaluation. -/
inductive EvalStmt : Env → Stmt → Env → Type
inductive EvalStmt : Env → Stmt → Env → Prop
| basic (ρ₁ ρ₂ : Env) (bs : BasicStmt) :
EvalBasicStmt ρ₁ bs ρ₂ → EvalStmt ρ₁ (.basic bs) ρ₂
| andThen (ρ₁ ρ₂ ρ₃ : Env) (s₁ s₂ : Stmt) :
@@ -81,15 +57,6 @@ inductive EvalStmt : Env → Stmt → Env → Type
EvalExpr ρ e (.int 0) →
EvalStmt ρ (.whileLoop e s) ρ
/-- For the purpose of static analysis, lattices we define describe program
state, or better yet, they describe _values_ in the program.
This class should be provided by each analysis' lattice (see also `Spa/Analysis/Forward.lean`)
to describe what each lattice value means in terms of the language.
In addition to providing the interpretation (`Spa.Interp`), the lattice
combinators `⊔` and `⊓` must respect disjunction and conjunction respectively.
This is because possible paths through a control flow graph (`Spa/Language/Graphs.lean`),
are tied to lattice operations used by the analysis engine. -/
class LatticeInterpretation (L : Type*) [Lattice L] extends Interp L (Value → Prop) where
interp_sup : ∀ {l₁ l₂ : L} (v : Value),
interp l₁ v ∨ interp l₂ v → interp (l₁ ⊔ l₂) v

18
lean/Spa/Language/Tagged/Basic.lean
View File

@@ -1,18 +0,0 @@
import Spa.Language.Base
import Spa.Language.Tagged.Id
import Spa.Language.Tagged.Derive
derive_tagged Spa.Expr Spa.BasicStmt Spa.Stmt
namespace Spa
def tagStmt (s : Stmt) : Stmt.Tagged RawId := (s.tag 0).1
def Stmt.Tagged.subtreeIds {τ : Type} (s : Stmt.Tagged τ) : List τ :=
s.foldTags (· :: ·) []
def Stmt.Tagged.isInLoopBody {τ : Type} [DecidableEq τ]
(body : Stmt.Tagged τ) (id : τ) : Bool :=
decide (id ∈ body.subtreeIds)
end Spa

417
lean/Spa/Language/Tagged/DESCENDANT-TRACKING.md
View File

@@ -1,417 +0,0 @@
# Descendant tracking (parked)
This is the formally-verified **interval-labeling / descendant** machinery that
used to live in `Id.lean` and `Properties.lean`. It let you decide "is node `a`
a descendant of node `b`?" with two integer comparisons on their identifiers,
and *proved* that numeric test equivalent to structural subtree containment.
It was removed because the descendant test is a *computational optimization*:
the same question can be answered by walking the AST, and nothing in the current
pipeline needs the fast test yet. The proofs (a rose-tree flattening + a
postorder `Good` invariant) are a real mechanization cost to carry. Parked here
so it can be restored verbatim when LICM actually wants it.
## What stays in the live code
- `NodeId` collapses to a single unique index (`{ post : ℕ }`); `tag` still
assigns each node a distinct postorder number.
- The bidirectional mapping (`erase`/`tag` + `erase_tagStmt`) stays in
`Properties.lean`.
- The labelled-CFG id↔state mapping (`Cfg.lean`) is independent of this and is
unaffected.
## Revival checklist
1. In `Id.lean`, give `NodeId` back its descendant-count field and the test:
```lean
structure NodeId where
post : ℕ
desc : ℕ -- number of proper descendants (subtree size − 1); leaf = 0
deriving DecidableEq, Repr
namespace NodeId
/-- Left endpoint of the node's postorder interval `[lo, post]`. -/
def lo (a : NodeId) : ℕ := a.post - a.desc
/-- `a` is a descendant-or-self of `b`: `a.post` lies in `b`'s interval. -/
def DescendantOf (a b : NodeId) : Prop := b.lo ≤ a.post ∧ a.post ≤ b.post
instance (a b : NodeId) : Decidable (DescendantOf a b) := by
unfold DescendantOf; infer_instance
end NodeId
```
2. In `Derive.lean`, make the generated `tag` store the descendant count again:
change the emitted identifier in `mkTag` from `(⟨$last⟩ : $nId)` back to
`(⟨$last, $last - n⟩ : $nId)`.
3. Paste the Lean block below back into `Properties.lean` (after the round-trip
theorems). It builds against the `id.lo = lo`-premise form of `Good` and the
childcount (`desc`) identifier. The headline result is
`descendant_iff_tagStmt`; everything else is supporting machinery.
## The parked proofs
```lean
/-- A rose tree of identifiers: the uniform shape underlying all three tagged
AST types, used to reason about the postorder labeling generically. -/
inductive IdTree where
| node (id : NodeId) (children : List IdTree)
namespace IdTree
def rootId : IdTree → NodeId
| .node id _ => id
@[simp] theorem rootId_node (id : NodeId) (cs : List IdTree) :
(IdTree.node id cs).rootId = id := rfl
mutual
def subtrees : IdTree → List IdTree
| .node id cs => .node id cs :: subtreesList cs
def subtreesList : List IdTree → List IdTree
| [] => []
| c :: cs => subtrees c ++ subtreesList cs
end
@[simp] theorem subtrees_node (id : NodeId) (cs : List IdTree) :
subtrees (.node id cs) = .node id cs :: subtreesList cs := rfl
@[simp] theorem subtreesList_nil : subtreesList [] = [] := rfl
@[simp] theorem subtreesList_cons (c : IdTree) (cs : List IdTree) :
subtreesList (c :: cs) = subtrees c ++ subtreesList cs := rfl
def posts (t : IdTree) : List ℕ := (subtrees t).map (fun s => s.rootId.post)
def postsList (cs : List IdTree) : List ℕ := (subtreesList cs).map (fun s => s.rootId.post)
@[simp] theorem posts_node (id : NodeId) (cs : List IdTree) :
posts (.node id cs) = id.post :: postsList cs := rfl
@[simp] theorem postsList_nil : postsList [] = [] := rfl
@[simp] theorem postsList_cons (c : IdTree) (cs : List IdTree) :
postsList (c :: cs) = posts c ++ postsList cs := by
simp [posts, postsList]
end IdTree
def Expr.Tagged.toIdTree : Expr.Tagged NodeId → IdTree
| .add t a b => .node t [a.toIdTree, b.toIdTree]
| .sub t a b => .node t [a.toIdTree, b.toIdTree]
| .var t _ => .node t []
| .num t _ => .node t []
def BasicStmt.Tagged.toIdTree : BasicStmt.Tagged NodeId → IdTree
| .assign t _ e => .node t [e.toIdTree]
| .noop t => .node t []
def Stmt.Tagged.toIdTree : Stmt.Tagged NodeId → IdTree
| .basic t bs => .node t [bs.toIdTree]
| .andThen t a b => .node t [a.toIdTree, b.toIdTree]
| .ifElse t e a b => .node t [e.toIdTree, a.toIdTree, b.toIdTree]
| .whileLoop t e s => .node t [e.toIdTree, s.toIdTree]
mutual
inductive Good : ℕ → IdTree → Prop
| mk {lo : ℕ} {id : NodeId} {cs : List IdTree} :
id.lo = lo → GoodChildren lo cs id.post →
Good lo (.node id cs)
inductive GoodChildren : ℕ → List IdTree → ℕ → Prop
| nil {pos : ℕ} : GoodChildren pos [] pos
| cons {cur : ℕ} {c : IdTree} {cs : List IdTree} {pos : ℕ} :
Good cur c → GoodChildren (c.rootId.post + 1) cs pos →
GoodChildren cur (c :: cs) pos
end
theorem Good.lo_le_post {lo : ℕ} {t : IdTree} (h : Good lo t) : lo ≤ t.rootId.post := by
cases h with
| mk hlo _ => simp only [NodeId.lo] at hlo; simp only [IdTree.rootId_node]; omega
theorem GoodChildren.cur_le_pos : ∀ {cur : ℕ} (cs : List IdTree) {pos : ℕ},
GoodChildren cur cs pos → cur ≤ pos
| _, [], _, h => by cases h; exact le_rfl
| _, c :: cs, _, h => by
cases h with
| cons hc hcs =>
have := hc.lo_le_post
have := GoodChildren.cur_le_pos cs hcs
omega
mutual
theorem Good.mem_posts : ∀ {lo : ℕ} (t : IdTree), Good lo t →
∀ x, x ∈ IdTree.posts t ↔ lo ≤ x ∧ x ≤ t.rootId.post
| _, .node id cs, h, x => by
cases h with
| mk hlo hch =>
simp only [IdTree.posts_node, List.mem_cons, IdTree.rootId_node]
rw [GoodChildren.mem_postsList cs hch x]
simp only [NodeId.lo] at hlo
omega
theorem GoodChildren.mem_postsList : ∀ {cur : ℕ} (cs : List IdTree) {pos : ℕ},
GoodChildren cur cs pos → ∀ x, x ∈ IdTree.postsList cs ↔ cur ≤ x ∧ x < pos
| _, [], _, h, x => by
cases h
simp only [IdTree.postsList_nil]
constructor
· intro hx; exact absurd hx (List.not_mem_nil x)
· rintro ⟨h1, h2⟩; exfalso; omega
| _, c :: cs, _, h, x => by
cases h with
| cons hc hcs =>
simp only [IdTree.postsList_cons, List.mem_append]
rw [Good.mem_posts c hc x, GoodChildren.mem_postsList cs hcs x]
have := hc.lo_le_post
have := GoodChildren.cur_le_pos cs hcs
omega
end
mutual
theorem Good.nodup_posts : ∀ {lo : ℕ} (t : IdTree), Good lo t → (IdTree.posts t).Nodup
| _, .node id cs, h => by
cases h with
| mk hlo hch =>
simp only [IdTree.posts_node, List.nodup_cons]
refine ⟨?_, GoodChildren.nodup_postsList cs hch⟩
intro hmem
rw [GoodChildren.mem_postsList cs hch id.post] at hmem
omega
theorem GoodChildren.nodup_postsList : ∀ {cur : ℕ} (cs : List IdTree) {pos : ℕ},
GoodChildren cur cs pos → (IdTree.postsList cs).Nodup
| _, [], _, h => by cases h; simp only [IdTree.postsList_nil, List.nodup_nil]
| _, c :: cs, _, h => by
cases h with
| cons hc hcs =>
simp only [IdTree.postsList_cons, List.nodup_append]
refine ⟨Good.nodup_posts c hc, GoodChildren.nodup_postsList cs hcs, ?_⟩
intro x hx1 hx2
rw [Good.mem_posts c hc x] at hx1
rw [GoodChildren.mem_postsList cs hcs x] at hx2
omega
end
mutual
theorem Good.subtree_good : ∀ {lo : ℕ} (t : IdTree), Good lo t →
∀ s ∈ IdTree.subtrees t, Good s.rootId.lo s
| _, .node id cs, h, s, hs => by
cases h with
| mk hlo hch =>
rw [IdTree.subtrees_node, List.mem_cons] at hs
rcases hs with rfl | hs
· simp only [IdTree.rootId_node]; rw [hlo]; exact Good.mk hlo hch
· exact GoodChildren.subtree_good cs hch s hs
theorem GoodChildren.subtree_good : ∀ {cur : ℕ} (cs : List IdTree) {pos : ℕ},
GoodChildren cur cs pos → ∀ s ∈ IdTree.subtreesList cs, Good s.rootId.lo s
| _, [], _, _, s, hs => by simp only [IdTree.subtreesList_nil, List.not_mem_nil] at hs
| _, c :: cs, _, h, s, hs => by
cases h with
| cons hc hcs =>
rw [IdTree.subtreesList_cons, List.mem_append] at hs
rcases hs with hs | hs
· exact Good.subtree_good c hc s hs
· exact GoodChildren.subtree_good cs hcs s hs
end
mutual
theorem IdTree.subtrees_subset : ∀ (t : IdTree) {b : IdTree},
b ∈ subtrees t → subtrees b ⊆ subtrees t
| .node id cs, b, hb => by
rw [subtrees_node, List.mem_cons] at hb
rcases hb with rfl | hb
· exact fun _ h => h
· intro x hx
rw [subtrees_node, List.mem_cons]
exact Or.inr (IdTree.subtreesList_subset cs hb hx)
theorem IdTree.subtreesList_subset : ∀ (cs : List IdTree) {b : IdTree},
b ∈ subtreesList cs → subtrees b ⊆ subtreesList cs
| [], b, hb => by simp only [subtreesList_nil, List.not_mem_nil] at hb
| c :: cs, b, hb => by
rw [subtreesList_cons, List.mem_append] at hb
intro x hx
rw [subtreesList_cons, List.mem_append]
rcases hb with hb | hb
· exact Or.inl (IdTree.subtrees_subset c hb hx)
· exact Or.inr (IdTree.subtreesList_subset cs hb hx)
end
theorem IdTree.eq_of_post_eq {l : List IdTree}
(h : (l.map (fun s => s.rootId.post)).Nodup) {a c : IdTree}
(ha : a ∈ l) (hc : c ∈ l) (hpost : a.rootId.post = c.rootId.post) : a = c := by
induction l with
| nil => exact absurd ha (List.not_mem_nil a)
| cons d ds ih =>
simp only [List.map_cons, List.nodup_cons] at h
obtain ⟨hd, htl⟩ := h
simp only [List.mem_cons] at ha hc
rcases ha with rfl | ha <;> rcases hc with rfl | hc
· rfl
· exfalso; apply hd; rw [hpost]; exact List.mem_map_of_mem _ hc
· exfalso; apply hd; rw [← hpost]; exact List.mem_map_of_mem _ ha
· exact ih htl ha hc
theorem descendant_iff_of_good {lo : ℕ} {t : IdTree} (hg : Good lo t)
{a b : IdTree} (ha : a ∈ IdTree.subtrees t) (hb : b ∈ IdTree.subtrees t) :
a.rootId.DescendantOf b.rootId ↔ a ∈ IdTree.subtrees b := by
have hgb : Good b.rootId.lo b := Good.subtree_good t hg b hb
constructor
· rintro ⟨h1, h2⟩
have hmem : a.rootId.post ∈ IdTree.posts b := by
rw [Good.mem_posts b hgb a.rootId.post]; exact ⟨h1, h2⟩
rw [IdTree.posts, List.mem_map] at hmem
obtain ⟨c, hc_mem, hc_post⟩ := hmem
have hc_t : c ∈ IdTree.subtrees t := IdTree.subtrees_subset t hb hc_mem
have hac : a = c :=
IdTree.eq_of_post_eq (hg.nodup_posts t) ha hc_t hc_post.symm
rw [hac]; exact hc_mem
· intro hsub
have hmem : a.rootId.post ∈ IdTree.posts b := by
rw [IdTree.posts, List.mem_map]; exact ⟨a, hsub, rfl⟩
rw [Good.mem_posts b hgb a.rootId.post] at hmem
exact hmem
/-! ### Tagging produces a good tree
We bridge from the `tag` traversal to the abstract `Good` invariant, by induction
on the plain AST. Each lemma also records that the returned counter is one past
the root's postorder index. -/
theorem Expr.tag_spec : ∀ (e : Expr) (n : ℕ),
Good n (e.tag n).1.toIdTree ∧ (e.tag n).1.toIdTree.rootId.post + 1 = (e.tag n).2 := by
intro e
induction e with
| num k =>
intro n
refine ⟨?_, ?_⟩
· simp only [Expr.tag, Expr.Tagged.toIdTree]
exact Good.mk (by simp only [NodeId.lo]; omega) GoodChildren.nil
· simp only [Expr.tag, Expr.Tagged.toIdTree, IdTree.rootId_node]
| var x =>
intro n
refine ⟨?_, ?_⟩
· simp only [Expr.tag, Expr.Tagged.toIdTree]
exact Good.mk (by simp only [NodeId.lo]; omega) GoodChildren.nil
· simp only [Expr.tag, Expr.Tagged.toIdTree, IdTree.rootId_node]
| add a b iha ihb =>
intro n
obtain ⟨gA, pA⟩ := iha n
obtain ⟨gB, pB⟩ := ihb (a.tag n).2
have lA := gA.lo_le_post
have lB := gB.lo_le_post
refine ⟨?_, ?_⟩
· simp only [Expr.tag, Expr.Tagged.toIdTree]
refine Good.mk ?_ ?_
· simp only [NodeId.lo]; omega
· refine GoodChildren.cons gA ?_
rw [pA]; refine GoodChildren.cons gB ?_; rw [pB]; exact GoodChildren.nil
· simp only [Expr.tag, Expr.Tagged.toIdTree, IdTree.rootId_node]
| sub a b iha ihb =>
intro n
obtain ⟨gA, pA⟩ := iha n
obtain ⟨gB, pB⟩ := ihb (a.tag n).2
have lA := gA.lo_le_post
have lB := gB.lo_le_post
refine ⟨?_, ?_⟩
· simp only [Expr.tag, Expr.Tagged.toIdTree]
refine Good.mk ?_ ?_
· simp only [NodeId.lo]; omega
· refine GoodChildren.cons gA ?_
rw [pA]; refine GoodChildren.cons gB ?_; rw [pB]; exact GoodChildren.nil
· simp only [Expr.tag, Expr.Tagged.toIdTree, IdTree.rootId_node]
theorem BasicStmt.tag_spec : ∀ (bs : BasicStmt) (n : ℕ),
Good n (bs.tag n).1.toIdTree ∧ (bs.tag n).1.toIdTree.rootId.post + 1 = (bs.tag n).2 := by
intro bs
cases bs with
| noop =>
intro n
refine ⟨?_, ?_⟩
· simp only [BasicStmt.tag, BasicStmt.Tagged.toIdTree]
exact Good.mk (by simp only [NodeId.lo]; omega) GoodChildren.nil
· simp only [BasicStmt.tag, BasicStmt.Tagged.toIdTree, IdTree.rootId_node]
| assign x e =>
intro n
obtain ⟨gE, pE⟩ := Expr.tag_spec e n
have lE := gE.lo_le_post
refine ⟨?_, ?_⟩
· simp only [BasicStmt.tag, BasicStmt.Tagged.toIdTree]
refine Good.mk ?_ ?_
· simp only [NodeId.lo]; omega
· refine GoodChildren.cons gE ?_
rw [pE]; exact GoodChildren.nil
· simp only [BasicStmt.tag, BasicStmt.Tagged.toIdTree, IdTree.rootId_node]
theorem Stmt.tag_spec : ∀ (s : Stmt) (n : ℕ),
Good n (s.tag n).1.toIdTree ∧ (s.tag n).1.toIdTree.rootId.post + 1 = (s.tag n).2 := by
intro s
induction s with
| basic bs =>
intro n
obtain ⟨gBs, pBs⟩ := BasicStmt.tag_spec bs n
have lBs := gBs.lo_le_post
refine ⟨?_, ?_⟩
· simp only [Stmt.tag, Stmt.Tagged.toIdTree]
refine Good.mk ?_ ?_
· simp only [NodeId.lo]; omega
· refine GoodChildren.cons gBs ?_
rw [pBs]; exact GoodChildren.nil
· simp only [Stmt.tag, Stmt.Tagged.toIdTree, IdTree.rootId_node]
| andThen a b iha ihb =>
intro n
obtain ⟨gA, pA⟩ := iha n
obtain ⟨gB, pB⟩ := ihb (a.tag n).2
have lA := gA.lo_le_post
have lB := gB.lo_le_post
refine ⟨?_, ?_⟩
· simp only [Stmt.tag, Stmt.Tagged.toIdTree]
refine Good.mk ?_ ?_
· simp only [NodeId.lo]; omega
· refine GoodChildren.cons gA ?_
rw [pA]; refine GoodChildren.cons gB ?_; rw [pB]; exact GoodChildren.nil
· simp only [Stmt.tag, Stmt.Tagged.toIdTree, IdTree.rootId_node]
| ifElse e a b iha ihb =>
intro n
obtain ⟨gE, pE⟩ := Expr.tag_spec e n
obtain ⟨gA, pA⟩ := iha (e.tag n).2
obtain ⟨gB, pB⟩ := ihb (a.tag (e.tag n).2).2
have lE := gE.lo_le_post
have lA := gA.lo_le_post
have lB := gB.lo_le_post
refine ⟨?_, ?_⟩
· simp only [Stmt.tag, Stmt.Tagged.toIdTree]
refine Good.mk ?_ ?_
· simp only [NodeId.lo]; omega
· refine GoodChildren.cons gE ?_
rw [pE]; refine GoodChildren.cons gA ?_
rw [pA]; refine GoodChildren.cons gB ?_; rw [pB]; exact GoodChildren.nil
· simp only [Stmt.tag, Stmt.Tagged.toIdTree, IdTree.rootId_node]
| whileLoop e s ih =>
intro n
obtain ⟨gE, pE⟩ := Expr.tag_spec e n
obtain ⟨gS, pS⟩ := ih (e.tag n).2
have lE := gE.lo_le_post
have lS := gS.lo_le_post
refine ⟨?_, ?_⟩
· simp only [Stmt.tag, Stmt.Tagged.toIdTree]
refine Good.mk ?_ ?_
· simp only [NodeId.lo]; omega
· refine GoodChildren.cons gE ?_
rw [pE]; refine GoodChildren.cons gS ?_; rw [pS]; exact GoodChildren.nil
· simp only [Stmt.tag, Stmt.Tagged.toIdTree, IdTree.rootId_node]
/-- A freshly tagged program is a well-tagged tree (rooted at postorder start `0`). -/
theorem good_tagStmt (s : Stmt) : Good 0 (tagStmt s).toIdTree :=
(Stmt.tag_spec s 0).1
/-- **Descendant characterization.** The numeric `NodeId.DescendantOf` relation on
two nodes of a tagged program holds exactly when one is structurally contained in
the other's subtree. -/
theorem descendant_iff_tagStmt (s : Stmt) {a b : IdTree}
(ha : a ∈ IdTree.subtrees (tagStmt s).toIdTree)
(hb : b ∈ IdTree.subtrees (tagStmt s).toIdTree) :
a.rootId.DescendantOf b.rootId ↔ a ∈ IdTree.subtrees b :=
descendant_iff_of_good (good_tagStmt s) ha hb
```

509
lean/Spa/Language/Tagged/Derive.lean
View File

@@ -1,509 +0,0 @@
import Lean
import Mathlib.Tactic.DeriveTraversable
import Spa.Language.Base
import Spa.Language.Tagged.Id
/-!
# The `derive_tagged` command
`derive_tagged T₁ T₂ … Tₙ` takes a family of (possibly mutually recursive)
inductive types and generates, for each `Tᵢ`:
* a *tagged* mirror inductive `Tᵢ.Tagged (τ : Type)`, in which every constructor
carries a leading `tag : τ` field and every field whose type is a family
member is retyped to its `.Tagged τ` counterpart;
* `Tᵢ.Tagged.erase : Tᵢ.Tagged τ → Tᵢ`, forgetting all tags;
* `Tᵢ.tag : Tᵢ → ℕ → Tᵢ.Tagged RawId × ℕ`, assigning every node a unique
`RawId` (its postorder index) by a single unified traversal that threads a
counter; the whole family shares one counter, so identifiers are unique across
types.
The generated declarations have exactly the shape of the hand-written reference;
see `Spa/Language/Tagged/Basic.lean` (which invokes this command) and the proofs
in `Spa/Language/Tagged/Properties.lean`.
Scope: the generator handles non-indexed inductives whose constructor fields are
either scalars or *direct* references to a family member (which covers the object
language). Nested occurrences such as `List Tᵢ` are not supported.
-/
open Lean Elab Command Meta
namespace Spa.DeriveTagged
/-- One constructor field, classified as a recursive family reference or a scalar
(whose type syntax we keep verbatim for the mirror inductive). -/
structure FieldData where
isRec : Bool
recType : Name
typeStx : Term
/-- A constructor: its original (full) name, short name, and fields. -/
structure CtorData where
origName : Name
shortName : Name
fields : Array FieldData
/-- A family member together with its constructors. -/
structure TypeData where
name : Name
ctors : Array CtorData
def taggedOf (n : Name) : Name := n ++ `Tagged
def eraseOf (n : Name) : Name := n ++ `Tagged ++ `erase
def rootTagOf (n : Name) : Name := n ++ `Tagged ++ `rootTag
def tagOf (n : Name) : Name := n ++ `tag
def foldTagsOf (n : Name) : Name := n ++ `Tagged ++ `foldTags
def wfOf (n : Name) : Name := n ++ `Tagged ++ `WF
def narrowOf (n : Name) : Name := n ++ `Tagged ++ `narrow
def narrowEraseOf (n : Name) : Name := n ++ `Tagged ++ `narrow_erase
def tagLeOf (n : Name) : Name := n ++ `tag_le
def tagRootTagPostOf (n : Name) : Name := n ++ `tag_rootTag_post
def tagWfOf (n : Name) : Name := n ++ `tag_wf
/-- Project the `i`-th conjunct (1-based) out of `hyp`, which has type a
right-nested `And` of `total` conjuncts, e.g. `hyp |>.2 |>.2 |>.1`. -/
def projAnd {m : Type → Type} [Monad m] [MonadQuotation m]
(hyp : Term) (i total : Nat) : m Term := do
let mut t := hyp
for _ in [0:i-1] do
t ← `($t |>.2)
if i < total then
t ← `($t |>.1)
return t
/-- Combine a non-empty array of propositions into a right-nested conjunction. -/
def mkAndR {m : Type → Type} [Monad m] [MonadQuotation m]
(cs : Array Term) : m Term := do
let mut t := cs.back!
for c in cs.pop.reverse do
t ← `($c ∧ $t)
return t
/-- For a constructor, return one entry per *recursive* field: its argument
identifier, the family member it references, and the start-counter expression at
which it is tagged (`n`, then `(a.tag n).2`, …) — the same threading `mkTag`
uses. -/
def recChildren (cd : CtorData) (argNames : Array Ident) (nStart : Term) :
CommandElabM (Array (Ident × Name × Term)) := do
let mut res : Array (Ident × Name × Term) := #[]
let mut cur := nStart
for (f, a) in cd.fields.zip argNames do
if f.isRec then
res := res.push (a, f.recType, cur)
cur ← `(($(mkIdent (tagOf f.recType)) $a $cur) |>.2)
return res
/-- Inspect the family, classifying each constructor field. -/
def gather (family : Array Name) (τ : Ident) : TermElabM (Array TypeData) := do
let famSet : NameSet := family.foldl (·.insert ·) {}
family.mapM fun tn => do
let iv ← getConstInfoInduct tn
let ctors ← iv.ctors.toArray.mapM fun cn => do
let cv ← getConstInfoCtor cn
let fields ← forallTelescopeReducing cv.type fun args _ => do
let fieldArgs := args.extract iv.numParams args.size
fieldArgs.mapM fun a => do
let ty ← inferType a
match ty.getAppFn.constName? with
| some hn =>
if famSet.contains hn then
return { isRec := true, recType := hn, typeStx := ← `($(mkIdent (taggedOf hn)) $τ) }
else
return { isRec := false, recType := default, typeStx := ← Lean.PrettyPrinter.delab ty }
| none =>
return { isRec := false, recType := default, typeStx := ← Lean.PrettyPrinter.delab ty }
return { origName := cn, shortName := cn.componentsRev.head!, fields }
return { name := tn, ctors }
/-- The arrow type `τ → <fields…> → Self τ` of a tagged constructor. -/
def ctorArrow (cd : CtorData) (self : Term) (τ : Ident) : TermElabM Term := do
let mut t := self
for f in cd.fields.reverse do
t ← `($(f.typeStx) → $t)
`($τ → $t)
/-- The tagged mirror inductives, one per family member. The family is a DAG
(`Expr ← BasicStmt ← Stmt`), not genuinely mutual, so they are emitted as
separate inductives in dependency order rather than a `mutual` block.
`Functor`/`Traversable` instances are derived separately by `mkDeriveInstances`
below rather than via an inline `deriving` clause. -/
def mkInductives (tds : Array TypeData) (τ : Ident) :
CommandElabM (Array (TSyntax `command)) := do
tds.mapM fun td => do
let self ← `($(mkIdent (taggedOf td.name)) $τ)
let ctors ← td.ctors.mapM fun cd => do
let aty ← Command.liftTermElabM (ctorArrow cd self τ)
`(Lean.Parser.Command.ctor| | $(mkIdent cd.shortName):ident : $aty)
`(command| inductive $(mkIdent (taggedOf td.name)):ident ($τ : Type) where $ctors*)
/-- A `deriving instance Functor, Traversable for Tᵢ.Tagged` command per family
member. Since every tagged type is a single-parameter, direct-recursive
inductive in `τ`, Mathlib's deriving handler produces clean (`sorry`-free)
instances, giving `map`, `traverse`, and the `Traversable.foldr`/`toList` folds
for free.
These are emitted as *separate* commands in dependency order (rather than an
inline `deriving` clause on each inductive) for two reasons: deriving
`Stmt.Tagged` needs the `Expr.Tagged`/`BasicStmt.Tagged` instances already in
scope, and — because every member's type name ends in `.Tagged` — the handler's
auto-generated instance name (`instFunctorTagged`, built from the type's last
component) collides across the family unless each derive sees the environment
the previous one updated; separate commands give it that, so the names
disambiguate to `instFunctorTagged`, `instFunctorTagged_1`, ….
The hand-written `foldTags` is retained alongside these: it is a
structural-recursion fold that `simp`/`decide` reduce cleanly, unlike the
abstract `Traversable.foldr` (defined via the `FreeMonoid`/`Const` applicative),
which reduces under `decide`/`rfl` but not naive `simp` unfolding. -/
def mkDeriveInstances (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
tds.mapM fun td =>
`(command| deriving instance Functor, Traversable for $(mkIdent (taggedOf td.name)))
/-- The `erase` functions, one per family member (separate defs in dependency
order — each calls only already-defined lower members). -/
def mkErase (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
tds.mapM fun td => do
let mut pats : Array Term := #[]
let mut rhss : Array Term := #[]
for cd in td.ctors do
let argNames := (Array.range cd.fields.size).map (fun i => mkIdent (.mkSimple s!"a{i}"))
let pat ← `($(mkIdent (taggedOf td.name ++ cd.shortName)) _ $argNames*)
let eraseArgs ← (cd.fields.zip argNames).mapM fun (f, a) =>
if f.isRec then `($(mkIdent (eraseOf f.recType)) $a) else pure a
let rhs ← `($(mkIdent cd.origName) $eraseArgs*)
pats := pats.push pat
rhss := rhss.push rhs
`(command| def $(mkIdent (eraseOf td.name)) {τ : Type} :
$(mkIdent (taggedOf td.name)) τ → $(mkIdent td.name) :=
fun x => match x with $[| $pats => $rhss]*)
/-- The `rootTag` accessors (one non-recursive `def` per type). -/
def mkRootTag (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
let tIdent := mkIdent `t
tds.mapM fun td => do
let mut pats : Array Term := #[]
let mut rhss : Array Term := #[]
for cd in td.ctors do
let hole ← `(_)
let wilds := Array.mkArray cd.fields.size hole
pats := pats.push (← `($(mkIdent (taggedOf td.name ++ cd.shortName)) $tIdent $wilds*))
rhss := rhss.push tIdent
`(command| def $(mkIdent (rootTagOf td.name)) {τ : Type} :
$(mkIdent (taggedOf td.name)) τ → τ :=
fun x => match x with $[| $pats => $rhss]*)
/-- The postorder `tag` functions, one per family member (separate defs in
dependency order). -/
def mkTag (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
let nId := mkIdent ``Spa.RawId
tds.mapM fun td => do
let mut pats : Array Term := #[]
let mut rhss : Array Term := #[]
for cd in td.ctors do
let argNames := (Array.range cd.fields.size).map (fun i => mkIdent (.mkSimple s!"a{i}"))
let pat ← `($(mkIdent cd.origName) $argNames*)
let mut cur : Term ← `(n)
let mut lets : Array (Ident × Term) := #[]
let mut taggedArgs : Array Term := #[]
let mut ri := 0
for (f, a) in cd.fields.zip argNames do
if f.isRec then
let rName := mkIdent (.mkSimple s!"r{ri}")
let rhsCall ← `($(mkIdent (tagOf f.recType)) $a $cur)
lets := lets.push (rName, rhsCall)
taggedArgs := taggedArgs.push (← `($rName |>.1))
cur ← `($rName |>.2)
ri := ri + 1
else
taggedArgs := taggedArgs.push a
let last := cur
let tagged ← `($(mkIdent (taggedOf td.name ++ cd.shortName))
(⟨$last⟩ : $nId) $taggedArgs*)
let mut body ← `(($tagged, $last + 1))
for (rName, rhs) in lets.reverse do
body ← `(let $rName := $rhs; $body)
pats := pats.push pat
rhss := rhss.push body
`(command| def $(mkIdent (tagOf td.name)) :
$(mkIdent td.name) → Nat → $(mkIdent (taggedOf td.name)) $nId × Nat :=
fun e n => match e with $[| $pats => $rhss]*)
/-- The tag-fold functions: `foldTags f acc t` applies `f` to every tag in `t`,
right-to-left, threading `acc`. This is the `Foldable`/`foldr`-over-tags the
hand-written collectors (e.g. `subtreeIds`) reduce to. One separate def per
family member (the family is a DAG, so no `mutual` block is needed). -/
def mkFoldTags (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
let τ := mkIdent `τ
let m := mkIdent `M
let fId := mkIdent `f
let accId := mkIdent `acc
let tagId := mkIdent `t
tds.mapM fun td => do
let mut pats : Array Term := #[]
let mut rhss : Array Term := #[]
for cd in td.ctors do
let argNames := (Array.range cd.fields.size).map (fun i => mkIdent (.mkSimple s!"a{i}"))
let pat ← `($(mkIdent (taggedOf td.name ++ cd.shortName)) $tagId $argNames*)
let mut body : Term := accId
for (fld, a) in (cd.fields.zip argNames).reverse do
if fld.isRec then
body ← `($(mkIdent (foldTagsOf fld.recType)) $fId $body $a)
body ← `($fId $tagId $body)
pats := pats.push pat
rhss := rhss.push body
`(command| def $(mkIdent (foldTagsOf td.name)) {$τ:ident : Type} {$m:ident : Type}
($fId : $τ → $m → $m) ($accId : $m) :
$(mkIdent (taggedOf td.name)) $τ → $m :=
fun x => match x with $[| $pats => $rhss]*)
/-- The well-formedness predicate `T.Tagged.WF : T.Tagged RawId → Prop`: every
recursive child's root tag has a strictly smaller postorder index than the node's
own tag, and each child is itself well-formed. Leaf constructors are `True`. -/
def mkWF (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
let tId := mkIdent `t
let rawId := mkIdent ``Spa.RawId
tds.mapM fun td => do
let mut pats : Array Term := #[]
let mut rhss : Array Term := #[]
for cd in td.ctors do
let hasRec := cd.fields.any (·.isRec)
let mut patArgs : Array Term := #[]
let mut recArgs : Array Ident := #[]
let mut i := 0
for f in cd.fields do
if f.isRec then
let a := mkIdent (.mkSimple s!"a{i}")
patArgs := patArgs.push a
recArgs := recArgs.push a
else
patArgs := patArgs.push (← `(_))
i := i + 1
let tagBind : Term ← if hasRec then `($tId) else `(_)
let pat ← `($(mkIdent (taggedOf td.name ++ cd.shortName)) $tagBind $patArgs*)
let rhs ← if recArgs.isEmpty then `(True) else do
let bounds ← recArgs.mapM fun a => `($(a).rootTag.post < $(tId).post)
let wfs ← recArgs.mapM fun a => `($(a).WF)
mkAndR (bounds ++ wfs)
pats := pats.push pat
rhss := rhss.push rhs
`(command| def $(mkIdent (wfOf td.name)) :
$(mkIdent (taggedOf td.name)) $rawId → Prop :=
fun x => match x with $[| $pats => $rhss]*)
/-- The `narrow` coercion `T.Tagged RawId → T.Tagged (Fin N)`, given a bound on
the root tag and a well-formedness proof. Each node's tag becomes the `Fin N`
built from its postorder index, and recursion threads the bound through `lt_trans`
and the (definitionally unfolded) `WF` conjunction. -/
def mkNarrow (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
let rawId := mkIdent ``Spa.RawId
let tId := mkIdent `t
let nId := mkIdent `N
let hId := mkIdent `h
let hwfId := mkIdent `hwf
let tgId := mkIdent `tg
tds.mapM fun td => do
let self ← `($(mkIdent (taggedOf td.name)) $rawId)
let mut patss : Array (Array Term) := #[]
let mut rhss : Array Term := #[]
for cd in td.ctors do
let argNames := (Array.range cd.fields.size).map fun i => mkIdent (.mkSimple s!"a{i}")
let ctorPat ← `($(mkIdent (taggedOf td.name ++ cd.shortName)) $tgId $argNames*)
let k := (cd.fields.filter (·.isRec)).size
let mut newArgs : Array Term := #[]
let mut ri := 0
for (f, a) in cd.fields.zip argNames do
if f.isRec then
let bound ← projAnd hwfId (ri + 1) (2 * k)
let wf ← projAnd hwfId (k + ri + 1) (2 * k)
newArgs := newArgs.push (← `($(a).narrow (lt_trans $bound $hId) $wf))
ri := ri + 1
else
newArgs := newArgs.push a
let built ← `($(mkIdent (taggedOf td.name ++ cd.shortName)) ⟨$(tgId).post, $hId⟩ $newArgs*)
let nPat ← `(_)
let hPat ← `($hId)
let hwfPat : Term ← if k == 0 then `(_) else `($hwfId)
patss := patss.push #[ctorPat, nPat, hPat, hwfPat]
rhss := rhss.push built
`(command| def $(mkIdent (narrowOf td.name)) : ($tId : $self) → {$nId : ℕ} →
$(tId).rootTag.post < $nId → $(tId).WF → $(mkIdent (taggedOf td.name)) (Fin $nId)
$[| $[$patss],* => $rhss]*)
/-- `T.tag_rootTag_post`: the root tag of a freshly tagged node is exactly one
below the threaded-out counter, i.e. the node itself is numbered last (postorder).
A uniform `cases <;> simp` discharges every constructor. -/
def mkTagRootTagPost (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
let eId := mkIdent `e
let nId := mkIdent `n
tds.mapM fun td =>
`(command| theorem $(mkIdent (tagRootTagPostOf td.name))
($eId : $(mkIdent td.name)) ($nId : ℕ) :
($(eId).tag $nId).1.rootTag.post + 1 = ($(eId).tag $nId).2 := by
cases $eId:ident <;>
simp [$(mkIdent (tagOf td.name)):ident, $(mkIdent (rootTagOf td.name)):ident])
/-- `T.tag_le`: tagging only ever advances the counter (`n ≤ (e.tag n).2`).
Proved by induction; each arm threads the counter through its recursive children
(using the relevant `tag_le`/induction hypothesis) and closes with `omega`. -/
def mkTagLe (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
let eId := mkIdent `e
let nId := mkIdent `n
tds.mapM fun td => do
let mut ctorLabels : Array Ident := #[]
let mut binderss : Array (Array Ident) := #[]
let mut tacs : Array (TSyntax ``Lean.Parser.Tactic.tacticSeq) := #[]
for cd in td.ctors do
let argNames := (Array.range cd.fields.size).map fun i => mkIdent (.mkSimple s!"a{i}")
let mut ihBinders : Array Ident := #[]
let mut haveTacs : Array (TSyntax `tactic) := #[]
let mut cur : Term ← `($nId)
let mut i := 0
for (f, a) in cd.fields.zip argNames do
if f.isRec then
let fact ← if f.recType == td.name then
`($(mkIdent (.mkSimple s!"ih{i}")) $cur)
else
`($(mkIdent (tagLeOf f.recType)) $a $cur)
if f.recType == td.name then
ihBinders := ihBinders.push (mkIdent (.mkSimple s!"ih{i}"))
haveTacs := haveTacs.push (← `(tactic| have := $fact))
cur ← `(($(mkIdent (tagOf f.recType)) $a $cur) |>.2)
i := i + 1
let simpTac ← `(tactic| simp only [$(mkIdent (tagOf td.name)):ident])
let omegaTac ← `(tactic| omega)
let allTacs := #[simpTac] ++ haveTacs ++ #[omegaTac]
ctorLabels := ctorLabels.push (mkIdent cd.shortName)
binderss := binderss.push (argNames ++ ihBinders)
tacs := tacs.push (← `(tacticSeq| $[$allTacs]*))
`(command| theorem $(mkIdent (tagLeOf td.name)) ($eId : $(mkIdent td.name)) ($nId : ℕ) :
$nId ≤ ($(eId).tag $nId).2 := by
induction $eId:ident generalizing $nId:ident with
$[| $ctorLabels:ident $binderss* => $tacs]*)
/-- `T.tag_wf`: a freshly tagged term is well-formed. Each recursive child's
bound conjunct is closed by `omega` from that child's `tag_rootTag_post` plus the
`tag_le` of every later child (which bounds the threaded-out counter), and each
well-formedness conjunct is the child's induction hypothesis / `tag_wf`. -/
def mkTagWf (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
let eId := mkIdent `e
let nId := mkIdent `n
tds.mapM fun td => do
let mut ctorLabels : Array Ident := #[]
let mut binderss : Array (Array Ident) := #[]
let mut tacs : Array (TSyntax ``Lean.Parser.Tactic.tacticSeq) := #[]
for cd in td.ctors do
let argNames := (Array.range cd.fields.size).map fun i => mkIdent (.mkSimple s!"a{i}")
-- recursive children: (arg, recType, startCounter, sameType?, fieldIndex)
let mut recs : Array (Ident × Name × Term × Bool × Nat) := #[]
let mut cur : Term ← `($nId)
let mut i := 0
for (f, a) in cd.fields.zip argNames do
if f.isRec then
recs := recs.push (a, f.recType, cur, f.recType == td.name, i)
cur ← `(($(mkIdent (tagOf f.recType)) $a $cur) |>.2)
i := i + 1
let k := recs.size
let ihBinders := (recs.filter (·.2.2.2.1)).map fun r => mkIdent (.mkSimple s!"ih{r.2.2.2.2}")
let tac : TSyntax ``Lean.Parser.Tactic.tacticSeq ← if k == 0 then
`(tacticSeq| exact True.intro)
else do
let mut comps : Array Term := #[]
-- bound conjuncts
for idx in [0:k] do
let (a, rt, s, _, _) := recs[idx]!
let mut bHaves : Array (TSyntax `tactic) :=
#[← `(tactic| have := $(mkIdent (tagRootTagPostOf rt)) $a $s)]
for j in [idx+1:k] do
let (aj, rtj, sj, _, _) := recs[j]!
bHaves := bHaves.push (← `(tactic| have := $(mkIdent (tagLeOf rtj)) $aj $sj))
bHaves := bHaves.push (← `(tactic| omega))
comps := comps.push (← `(by $(← `(tacticSeq| $[$bHaves]*))))
-- well-formedness conjuncts
for idx in [0:k] do
let (a, rt, s, same, fi) := recs[idx]!
comps := comps.push <| ← if same then `($(mkIdent (.mkSimple s!"ih{fi}")) $s)
else `($(mkIdent (tagWfOf rt)) $a $s)
let simpTac ← `(tactic| simp only
[$(mkIdent (tagOf td.name)):ident, $(mkIdent (wfOf td.name)):ident])
let exactTac ← `(tactic| exact ⟨$comps,*⟩)
`(tacticSeq| $[$(#[simpTac, exactTac])]*)
ctorLabels := ctorLabels.push (mkIdent cd.shortName)
binderss := binderss.push (argNames ++ ihBinders)
tacs := tacs.push tac
`(command| theorem $(mkIdent (tagWfOf td.name)) ($eId : $(mkIdent td.name)) ($nId : ℕ) :
($(eId).tag $nId).1.WF := by
induction $eId:ident generalizing $nId:ident with
$[| $ctorLabels:ident $binderss* => $tacs]*)
/-- `T.Tagged.narrow_erase`: narrowing the tag type does not change the erased
(untagged) term. A per-constructor `simp` with the local `narrow`/`erase`
equations, the lower members' `narrow_erase`, and the induction hypotheses. -/
def mkNarrowErase (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
let rawId := mkIdent ``Spa.RawId
let tId := mkIdent `t
let nId := mkIdent `N
let hId := mkIdent `h
let hwfId := mkIdent `hwf
let tgId := mkIdent `tg
tds.mapM fun td => do
let mut ctorLabels : Array Ident := #[]
let mut binderss : Array (Array Ident) := #[]
let mut tacs : Array (TSyntax ``Lean.Parser.Tactic.tacticSeq) := #[]
for cd in td.ctors do
let argNames := (Array.range cd.fields.size).map fun i => mkIdent (.mkSimple s!"a{i}")
let mut lemmas : Array Term :=
#[← `($(mkIdent (narrowOf td.name))), ← `($(mkIdent (eraseOf td.name)))]
let mut ihBinders : Array Ident := #[]
let mut seenLower : Array Name := #[]
let mut i := 0
for f in cd.fields do
if f.isRec then
if f.recType == td.name then
let ih := mkIdent (.mkSimple s!"ih{i}")
ihBinders := ihBinders.push ih
lemmas := lemmas.push (← `($ih))
else if !seenLower.contains f.recType then
seenLower := seenLower.push f.recType
lemmas := lemmas.push (← `($(mkIdent (narrowEraseOf f.recType))))
i := i + 1
let introTac ← `(tactic| intro $nId $hId $hwfId)
let simpTac ← `(tactic| simp [$[$lemmas:term],*])
ctorLabels := ctorLabels.push (mkIdent cd.shortName)
binderss := binderss.push (#[tgId] ++ argNames ++ ihBinders)
tacs := tacs.push (← `(tacticSeq| $[$(#[introTac, simpTac])]*))
`(command| theorem $(mkIdent (narrowEraseOf td.name)) :
($tId : $(mkIdent (taggedOf td.name)) $rawId) → ∀ {$nId : ℕ}
($hId : $(tId).rootTag.post < $nId) ($hwfId : $(tId).WF),
($(tId).narrow $hId $hwfId).erase = $(tId).erase := by
intro $tId:ident
induction $tId:ident with
$[| $ctorLabels:ident $binderss* => $tacs]*)
/-- `derive_tagged T₁ … Tₙ` — generate tagged mirrors, `erase`, and `tag` for the
given family of inductives. -/
syntax (name := deriveTaggedCmd) "derive_tagged " ident+ : command
@[command_elab deriveTaggedCmd]
def elabDeriveTagged : CommandElab := fun stx => do
match stx with
| `(derive_tagged $ids*) =>
let family ← ids.mapM fun i => Command.liftCoreM (realizeGlobalConstNoOverload i)
let τ := mkIdent `τ
let tds ← Command.liftTermElabM (gather family τ)
for d in (← mkInductives tds τ) do elabCommand d
for d in (← mkDeriveInstances tds) do elabCommand d
for d in (← mkRootTag tds) do elabCommand d
for d in (← mkErase tds) do elabCommand d
for d in (← mkTag tds) do elabCommand d
for d in (← mkFoldTags tds) do elabCommand d
for d in (← mkWF tds) do elabCommand d
for d in (← mkNarrow tds) do elabCommand d
for d in (← mkTagRootTagPost tds) do elabCommand d
for d in (← mkTagLe tds) do elabCommand d
for d in (← mkTagWf tds) do elabCommand d
for d in (← mkNarrowErase tds) do elabCommand d
| _ => throwUnsupportedSyntax
end Spa.DeriveTagged

104
lean/Spa/Language/Tagged/Graphs.lean
View File

@@ -1,104 +0,0 @@
import Spa.Language
import Spa.Language.Graphs
import Spa.Language.Tagged.Basic
import Spa.Language.Tagged.Properties
namespace Spa
open GGraph
def Stmt.Tagged.cfg {τ : Type} : Stmt.Tagged τ → GGraph (Option (BasicStmt.Tagged τ))
| .basic _ bs => GGraph.singleton (some bs)
| .andThen _ s₁ s₂ => s₁.cfg ⤳ s₂.cfg
| .ifElse _ _ s₁ s₂ => s₁.cfg ∙ s₂.cfg
| .whileLoop _ _ s => GGraph.loop s.cfg
theorem Stmt.Tagged.cfg_graph {τ : Type} : ∀ (t : Stmt.Tagged τ),
(Option.map BasicStmt.Tagged.erase) <$> t.cfg = t.erase.cfg
| .basic _ bs => by simp [Stmt.Tagged.cfg, Stmt.cfg, Stmt.Tagged.erase, BasicStmt.Tagged.erase]
| .andThen _ s₁ s₂ => by
simp [Stmt.Tagged.cfg, Stmt.cfg, Stmt.Tagged.erase, Stmt.Tagged.cfg_graph s₁, Stmt.Tagged.cfg_graph s₂]
| .ifElse _ _ s₁ s₂ => by
simp [Stmt.Tagged.cfg, Stmt.cfg, Stmt.Tagged.erase, Stmt.Tagged.cfg_graph s₁, Stmt.Tagged.cfg_graph s₂]
| .whileLoop _ _ s => by
simp [Stmt.Tagged.cfg, Stmt.cfg, Stmt.Tagged.erase, Stmt.Tagged.cfg_graph s]
def GGraph.nodeLabel {τ : Type} (g : GGraph (Option (BasicStmt.Tagged τ))) (i : g.Index) :
Option τ :=
(g.nodes i).map BasicStmt.Tagged.rootTag
def GGraph.stateOf {τ : Type} [DecidableEq τ] (g : GGraph (Option (BasicStmt.Tagged τ)))
(id : τ) : Option g.Index :=
g.indices.find? (fun i => decide (g.nodeLabel i = some id))
theorem GGraph.stateOf_label {τ : Type} [DecidableEq τ]
{g : GGraph (Option (BasicStmt.Tagged τ))} {id : τ}
{i : g.Index} (h : g.stateOf id = some i) : g.nodeLabel i = some id := by
rw [GGraph.stateOf] at h
simpa using List.find?_some h
namespace Program
variable (p : Program)
def tagged : Stmt.Tagged RawId := tagStmt p.rootStmt
def size : ℕ := p.tagged.rootTag.post + 1
theorem size_pos : 0 < p.size := Nat.succ_pos _
abbrev NodeId : Type := Fin p.size
theorem tagged_wf : p.tagged.WF := Stmt.tag_wf p.rootStmt 0
def taggedFin : Stmt.Tagged p.NodeId :=
p.tagged.narrow (Nat.lt_succ_self _) p.tagged_wf
def taggedCfg : GGraph (Option (BasicStmt.Tagged p.NodeId)) :=
GGraph.wrap p.taggedFin.cfg
theorem taggedCfg_erase :
(Option.map BasicStmt.Tagged.erase) <$> p.taggedCfg = p.cfg := by
rw [taggedCfg, GGraph.map_wrap, Stmt.Tagged.cfg_graph, taggedFin,
Stmt.Tagged.narrow_erase, tagged, erase_tagStmt]
rfl
theorem taggedCfg_size : p.taggedCfg.size = p.cfg.size := by
conv_rhs => rw [← p.taggedCfg_erase]
rfl
def nodeIdOf (s : p.State) : Option p.NodeId :=
p.taggedCfg.nodeLabel (Fin.cast p.taggedCfg_size.symm s)
def stateOfNodeId (id : p.NodeId) : Option p.State :=
(p.taggedCfg.stateOf id).map (Fin.cast p.taggedCfg_size)
theorem cfg_nodes_eq (s : p.State) :
p.cfg.nodes s = Option.map BasicStmt.Tagged.erase
(p.taggedCfg.nodes (Fin.cast p.taggedCfg_size.symm s)) := by
have key : ∀ (g : Graph) (hsz : p.taggedCfg.size = g.size),
(Option.map BasicStmt.Tagged.erase) <$> p.taggedCfg = g →
∀ i : Fin g.size,
g.nodes i = Option.map BasicStmt.Tagged.erase
(p.taggedCfg.nodes (Fin.cast hsz.symm i)) := by
intro g hsz hg i
subst hg
rfl
exact key p.cfg p.taggedCfg_size p.taggedCfg_erase s
theorem nodeIdOf_isSome_of_code {s : p.State} {bs : BasicStmt}
(h : p.code s = some bs) : (p.nodeIdOf s).isSome = true := by
have hc : Option.map BasicStmt.Tagged.erase
(p.taggedCfg.nodes (Fin.cast p.taggedCfg_size.symm s)) = some bs := by
rw [← p.cfg_nodes_eq s]; exact h
unfold Program.nodeIdOf GGraph.nodeLabel
cases hcase : p.taggedCfg.nodes (Fin.cast p.taggedCfg_size.symm s) with
| none => rw [hcase] at hc; simp at hc
| some tbs => simp
def nodeIdOfNonempty (s : p.State) {bs : BasicStmt} (h : p.code s = some bs) : p.NodeId :=
(p.nodeIdOf s).get (p.nodeIdOf_isSome_of_code h)
end Program
end Spa

9
lean/Spa/Language/Tagged/Id.lean
View File

@@ -1,9 +0,0 @@
import Mathlib.Data.Nat.Notation
namespace Spa
structure RawId where
post : ℕ
deriving DecidableEq, Repr
end Spa

29
lean/Spa/Language/Tagged/Properties.lean
View File

@@ -1,29 +0,0 @@
import Spa.Language.Tagged.Basic
namespace Spa
@[simp] theorem Expr.erase_tag (e : Expr) (n : ℕ) : (e.tag n).1.erase = e := by
induction e generalizing n with
| add a b iha ihb => simp [Expr.tag, Expr.Tagged.erase, iha, ihb]
| sub a b iha ihb => simp [Expr.tag, Expr.Tagged.erase, iha, ihb]
| var x => simp [Expr.tag, Expr.Tagged.erase]
| num k => simp [Expr.tag, Expr.Tagged.erase]
@[simp] theorem BasicStmt.erase_tag (bs : BasicStmt) (n : ℕ) :
(bs.tag n).1.erase = bs := by
cases bs with
| assign x e => simp [BasicStmt.tag, BasicStmt.Tagged.erase]
| noop => simp [BasicStmt.tag, BasicStmt.Tagged.erase]
@[simp] theorem Stmt.erase_tag (s : Stmt) (n : ℕ) : (s.tag n).1.erase = s := by
induction s generalizing n with
| basic bs => simp [Stmt.tag, Stmt.Tagged.erase]
| andThen a b iha ihb => simp [Stmt.tag, Stmt.Tagged.erase, iha, ihb]
| ifElse e a b iha ihb => simp [Stmt.tag, Stmt.Tagged.erase, iha, ihb]
| whileLoop e s ih => simp [Stmt.tag, Stmt.Tagged.erase, ih]
/-- Erasing a freshly tagged program recovers it. -/
theorem erase_tagStmt (s : Stmt) : (tagStmt s).erase = s := by
simp [tagStmt]
end Spa

46
lean/Spa/Language/Tagged/TODO.md
View File

@@ -1,46 +0,0 @@
# Tagged AST — follow-ups
## Descendant tracking — parked
The interval-labeling descendant test and its correctness proof
(`descendant_iff_tagStmt` and supporting rose-tree/`Good` machinery) have been
removed from the live code and parked in `DESCENDANT-TRACKING.md`, with a revival
checklist. It's a computational optimization not yet needed; revive it (and the
`NodeId.desc` field) when LICM wants fast ancestor queries.
## ID → CFG-state mapping — plan part B — DONE
`Graphs.lean` now defines a payload-generic `GGraph α` (with `Graph := GGraph
(List BasicStmt)` as the concrete CFG), so the labelled CFG **reuses** the graph
combinators instead of mirroring them. In `Cfg.lean`:
`buildCfgL : Stmt.Tagged NodeId → GGraph (List (BasicStmt.Tagged NodeId))` is just
`buildCfg` at the tagged payload; `buildCfgL_graph :
(buildCfgL t).map (List.map erase) = buildCfg t.erase` connects it to the real
CFG; and `GGraph.nodeLabel`/`GGraph.stateOf` read a node's id straight from its
payload (`stateOf_label` is the soundness). No `LGraph`, no separate `label`
field, no duplicated combinators.
## ID → CFG-state mapping — totality — DONE
The `Option`-valued `nodeIdOf`/`stateOfNodeId` are now proven total on the inputs
that matter (`Graphs.lean`), via a payload-list characterization of the CFG:
- `GGraph.nodeList` flattens `nodes` into the list of payloads, with combinator
lemmas (`nodeList_comp/link/loop/wrap`) reducing it through the CFG builders.
- `Stmt.Tagged.basics` lists a program's basic statements; the master lemma
`Stmt.Tagged.cfg_nodeList_filter` (and its program-level
`taggedCfg_nodeList_filter`) shows the non-empty CFG nodes are *exactly* the
singletons `[bs]` for `bs ∈ basics`.
- AST ⇒ CFG: `exists_state_of_mem_basics` (a state with payload `[bs]`) and
`stateOfNodeId_isSome` (the search succeeds).
- CFG ⇒ AST: `exists_basic_of_code_ne_nil` (a non-empty node is `[bs]`, with
`code = [bs.erase]` and `nodeIdOf = some bs.rootTag`) and `nodeIdOf_isSome`.
All `propext`/`Quot.sound`-only (no `sorry`, no choice).
Remaining nice-to-have:
- Injectivity: distinct basic-statement ids map to distinct states, giving a
two-sided id ↔ state correspondence (upgrading the existence results above to a
genuine bijection, and pinning `stateOfNodeId (bs.rootTag)` to *the* state
holding `bs`). The `tag`-uniqueness fact this needs (`Nodup` of postorder tags)
was part of the parked descendant machinery in `DESCENDANT-TRACKING.md`.

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

@@ -1,266 +1,26 @@
import Spa.Language.Semantics
import Spa.Language.Graphs
import Spa.Language.Program
/-!
# Program Traces
This module defines program traces tied to Control Flow Graphs, or CFGs
(see `Spa.GGraph` and `Spa.Graph`). These traces boil town to sequences of
basic-block executions (really, `Spa.BasicStmt` executions), each of which must
have an actual basic block in the graph _and_ be connected to the previous
basic block by an edge. In this way, traces encode executions admitted
by the CFG.
While the regular `Trace` is just _any_ path through the graph, an
`EndToEndTrace` is a path from the entry node to the exit node, denoting
full program execution.
Properties about graphs and language semantics (especially,
the fact that the graph contains the proper basic block and edges
to represent any program execution according to the
language's big-step semantics `EvalStmt`) is found
in `Spa/Language/Properties.lean`.
-/
namespace Spa
/-- A partial trace through a graph `g`, starting right before
the execution of the basic block at the first index, and
ending right after the execution of the basic block at the last index. -/
inductive Trace (g : Graph) : g.Index → g.Index → Env → Env → Type
inductive Trace (g : Graph) : g.Index → g.Index → Env → Env → Prop
| single {ρ₁ ρ₂ : Env} {idx : g.Index} :
EvalBasicStmtOpt ρ₁ (g.nodes idx) ρ₂ → Trace g idx idx ρ₁ ρ₂
EvalBasicStmts ρ₁ (g.nodes idx) ρ₂ → Trace g idx idx ρ₁ ρ₂
| edge {ρ₁ ρ₂ ρ₃ : Env} {idx₁ idx₂ idx₃ : g.Index} :
EvalBasicStmtOpt ρ₁ (g.nodes idx₁) ρ₂ → (idx₁, idx₂) ∈ g.edges →
EvalBasicStmts ρ₁ (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. -/
def Trace.concat {g : Graph} {idx₁ idx₂ idx₃ idx₄ : g.Index}
theorem 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₄ ρ₁ ρ₃ :=
match tr₁ with
| single hbs => edge hbs he tr₂
| edge hbs he' tr₁' => edge hbs he' (tr₁'.concat he tr₂)
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₂)
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)
@[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₃ ρ₁ ρ₃
| .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₂ ρ₁ ρ₃ := 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₃ ρ₂ ρ₃ →
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
/-!
## Trace Steps
Analyses that care about *which statements executed* (e.g. reaching
definitions) need to project a trace down to its list of executed statements.
Defining that projection here, once, as a chronological mathlib `List` means
all the re-association facts about concatenating traces come for free from
`List.append_assoc` and friends, instead of being re-proven per analysis. -/
/-- The (index, statement) pairs executed by a single optional-statement step:
none if the node is empty, and the node's statement otherwise. -/
def EvalBasicStmtOpt.steps {α : Type*} (idx : α) {ρ₁ ρ₂ : Env} {obs : Option BasicStmt} :
EvalBasicStmtOpt ρ₁ obs ρ₂ → List (α × BasicStmt)
| .none => []
| .some (bs := bs) _ => [(idx, bs)]
/-- The statements executed by a left-open trace, in chronological order. -/
def Traceₗ.steps {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ : Env} :
Traceₗ g idx₁ idx₂ ρ₁ ρ₂ → List (g.Index × BasicStmt)
| .nil => []
| .cons (idx₁ := idx) hnode _ rest => hnode.steps idx ++ rest.steps
/-- The statements executed by a trace, in chronological order. -/
def Trace.steps {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ : Env} :
Trace g idx₁ idx₂ ρ₁ ρ₂ → List (g.Index × BasicStmt)
| .single (idx := idx) hnode => hnode.steps idx
| .edge (idx₁ := idx) hnode _ rest => hnode.steps idx ++ rest.steps
@[simp] lemma Traceₗ.steps_append {g : Graph} {idx₁ idx₂ idx₃ : g.Index}
{ρ₁ ρ₂ ρ₃ : Env} (tr₁ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂)
(tr₂ : Traceₗ g idx₂ idx₃ ρ₂ ρ₃) :
(tr₁ ++ tr₂).steps = tr₁.steps ++ tr₂.steps := by
show (tr₁.append tr₂).steps = _
induction tr₁ <;> simp [Traceₗ.append, Traceₗ.steps, *]
@[simp] lemma Traceₗ.steps_appendTrace {g : Graph} {idx₁ idx₂ idx₃ : g.Index}
{ρ₁ ρ₂ ρ₃ : Env} (tr₁ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂)
(tr₂ : Trace g idx₂ idx₃ ρ₂ ρ₃) :
(tr₁ ++ tr₂).steps = tr₁.steps ++ tr₂.steps := by
show (tr₁.appendTrace tr₂).steps = _
induction tr₁ <;> simp [Traceₗ.appendTrace, Traceₗ.steps, Trace.steps, *]
@[simp] lemma Traceₗ.steps_appendStep {g : Graph} {idx₁ idx₂ : g.Index}
{ρ₁ ρ₂ ρ₃ : Env} (tr : Traceₗ g idx₁ idx₂ ρ₁ ρ₂)
(hbs : EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃) :
(tr ++ hbs).steps = tr.steps ++ hbs.steps idx₂ :=
Traceₗ.steps_appendTrace tr (Trace.single hbs)
@[simp] lemma Trace.steps_addEdge {g : Graph} {idx₁ idx₂ idx₃ : g.Index}
{ρ₁ ρ₂ : Env} (tr : Trace g idx₁ idx₂ ρ₁ ρ₂)
(hedge : (idx₂, idx₃) ∈ g.edges) :
(tr.addEdge hedge).steps = tr.steps := by
induction tr <;> simp [Trace.addEdge, Trace.steps, Traceₗ.steps, *]
@[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
inductive EndToEndTrace (g : Graph) (ρ₁ ρ₂ : Env) : Prop
| 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 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
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
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
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
end Spa

129
lean/Spa/Lattice.lean
View File

@@ -1,32 +1,8 @@
import Mathlib.Order.Lattice
import Mathlib.Order.RelSeries
/-!
# Lattice Definitions
This file provides some definitions for lattices. It used to be more critical
when this was an Agda project, since it defined (semi)lattices, the ordering
relation, etc. However, these have been lifted into `Mathlib.Order.Lattice`
etc.. What remains are a couple of theorems about folds, as well
as `FiniteHeightLattice`, the core concept of lattice-based static
program analyses. See the documentation on that class for more information. -/
namespace Option
/-- Equality-sensitive eliminator for options in which the `some` case
is sensitive to the base `β`. This makes it mirror a one-element fold
more closely. -/
def elimEq {α : Type*} {β : Sort*} :
(o : Option α) → β → ((a : α) → o = some a → β → β) → β
| none, b, _ => b
| some a, b, f => f a rfl b
end Option
namespace Spa
/-- Predicate for binary functions independently monotone in both their arguments. -/
def Monotone₂ {α β γ : Type*} [Preorder α] [Preorder β] [Preorder γ]
(f : α → β → γ) : Prop :=
(∀ b, Monotone (f · b)) ∧ (∀ a, Monotone (f a ·))
@@ -35,20 +11,18 @@ section Folds
variable {α β : Type*} [Preorder α] [Preorder β]
/-- (right) folds are monotonic in both their arguments if the underlying accumulator function is. -/
lemma foldr_mono {l₁ l₂ : List α} (f : α → β → β) {b₁ b₂ : β}
theorem foldr_mono {l₁ l₂ : List α} (f : α → β → β) {b₁ b₂ : β}
(hl : List.Forall₂ (· ≤ ·) l₁ l₂) (hb : b₁ ≤ b₂)
(hf₁ : ∀ b, Monotone (f · b)) (hf₂ : ∀ a, Monotone (f a ·)) :
(hf₁ : ∀ b, Monotone fun a => f a b) (hf₂ : ∀ a, Monotone (f a)) :
l₁.foldr f b₁ ≤ l₂.foldr f b₂ := by
induction hl with
| nil => exact hb
| cons hxy _ ih =>
exact le_trans (hf₁ _ hxy) (hf₂ _ ih)
/-- (left) folds are monotinic in both their arguments if the underlying accumulator function is. -/
lemma foldl_mono {l₁ l₂ : List α} (f : β → α → β) {b₁ b₂ : β}
theorem foldl_mono {l₁ l₂ : List α} (f : β → α → β) {b₁ b₂ : β}
(hl : List.Forall₂ (· ≤ ·) l₁ l₂) (hb : b₁ ≤ b₂)
(hf₁ : ∀ a, Monotone (f · a)) (hf₂ : ∀ b, Monotone (f b ·)) :
(hf₁ : ∀ a, Monotone fun b => f b a) (hf₂ : ∀ b, Monotone (f b)) :
l₁.foldl f b₁ ≤ l₂.foldl f b₂ := by
induction hl generalizing b₁ b₂ with
| nil => exact hb
@@ -56,96 +30,61 @@ lemma foldl_mono {l₁ l₂ : List α} (f : β → α → β) {b₁ b₂ : β}
exact ih (le_trans (hf₁ _ hb) (hf₂ _ hxy))
omit [Preorder α] in
/-- (right) folds on a particular list are monotonic if the underlying accumulator is monotonic in its accumulator argument. -/
lemma foldr_mono' (l : List α) (f : α → β → β)
(hf : ∀ a, Monotone (f a ·)) : Monotone (l.foldr f ·) := by
theorem foldr_mono' (l : List α) (f : α → β → β)
(hf : ∀ a, Monotone (f a ·)) : Monotone fun b => l.foldr f b := by
intro b₁ b₂ hb
induction l with
| nil => exact hb
| cons x xs ih => exact hf x ih
omit [Preorder α] in
/-- (left) folds on a particular list are monotonic if the underlying accumulator is monotonic in its accumulator argument. -/
lemma foldl_mono' (l : List α) (f : β → α → β)
theorem foldl_mono' (l : List α) (f : β → α → β)
(hf : ∀ a, Monotone (f · a)) : Monotone fun b => l.foldl f b := by
intro b₁ b₂ hb
induction l generalizing b₁ b₂ with
| nil => exact hb
| cons x xs ih => exact ih (hf x hb)
omit [Preorder α] in
/-- The equality-aware eliminator (that also alters its behavior dependent on base case)
for option is monotonic. -/
lemma elimEq_self_mono (o : Option α) (g : (a : α) → o = some a → β → β)
(hg : ∀ a h, Monotone (g a h)) :
Monotone (o.elimEq · g) := by
cases o with
| none => exact monotone_id
| some a => exact hg a rfl
end Folds
/-- Predicate on types with `Preorder` that claims all $<$ chains in the type have at most `n` comparisons. -/
def BoundedChains (α : Type*) [Preorder α] (n : ℕ) : Prop :=
∀ c : LTSeries α, c.length ≤ n
/-- Since a singleton type's preorder has no nonempty `<` chains,
they are vacuously bounded by any minimum height. -/
lemma boundedChains_of_subsingleton (α : Type*) [Preorder α] [Subsingleton α]
(n : ℕ) : BoundedChains α n := fun c => by
by_contra hc
push_neg at hc
exact (c.step ⟨0, by omega⟩).ne (Subsingleton.elim _ _)
structure PointedLTSeries (α : Type*) (f t : α)(n : ℕ) [Preorder α] where
series : LTSeries α
head_series : series.head = f
last_series : series.last = t
length_series : series.length = n
/-- A finite height lattice is a lattice in which all chains $a < \ldots < z$ have a maximum height `height`. -/
class FiniteHeightLattice (α : Type*) extends Lattice α, OrderBot α, OrderTop α where
class FiniteHeightLattice (α : Type*) [Lattice α] extends Bot α, Top α where
height : ℕ
longestChain : PointedLTSeries α ⊥ ⊤ height
chains_bounded : BoundedChains α height
-- a < ... < z
-- ----------- length <= height
namespace FixedHeight
variable {α : Type*} [Lattice α] {h : ℕ}
theorem bot_le [FiniteHeightLattice α] : ∀ (a : α), ⊥ ≤ a := by
intro a
by_cases heq : ⊥ ⊓ a = ⊥
· exact inf_eq_left.mp heq
· exfalso
have lc := FiniteHeightLattice.longestChain (α := α)
have hlt : ⊥ ⊓ a < lc.series.head := by
rw [lc.head_series]
exact lt_of_le_of_ne inf_le_left heq
have hbound := FiniteHeightLattice.chains_bounded (lc.series.cons (⊥ ⊓ a) hlt)
rw [RelSeries.cons_length, lc.length_series] at hbound
omega
end FixedHeight
namespace FiniteHeightLattice
/-- This is something like a lemma about isomorphic types having the same height.
Given a finite-height lattice `α`, lattice `β`, and a `Monotone` bijection
between the two, we can show that lattice `β` also has a finite height.
variable (α : Type*) [Lattice α] [FiniteHeightLattice α]
The proof is fairly trivial: any chain in `β` can be transported to a chain in `α`,
and must be bounded by the same height by `FiniteHeightLattice.chains_bounded`. -/
def transport {α β : Type*} [Lattice β]
[I : FiniteHeightLattice α] (f : α → β) (g : β → α)
(hf : Monotone f) (hg : Monotone g)
(hfg : Function.LeftInverse f g) :
FiniteHeightLattice β where
toLattice := inferInstance
toOrderBot := {
bot := f (⊥ : α)
bot_le := fun b => by
rw [← hfg b]
exact hf (_root_.bot_le : (⊥ : α) ≤ g b) }
toOrderTop := {
top := f (⊤ : α)
le_top := fun b => by
rw [← hfg b]
exact hf (_root_.le_top : g b ≤ (⊤ : α)) }
height := I.height
chains_bounded := fun c =>
I.chains_bounded (c.map g (hg.strictMono_of_injective hfg.injective))
/-- A `Unique` lattice trivially has finite height: its only chain is the singleton
`[default]`, and there are no nontrivial `<` chains in a subsingleton. -/
def ofUnique (α : Type*) [Lattice α] [Unique α] :
FiniteHeightLattice α where
toLattice := inferInstance
toOrderBot := {
bot := default
bot_le := fun _ => le_of_eq (Subsingleton.elim _ _) }
toOrderTop := {
top := default
le_top := fun _ => le_of_eq (Subsingleton.elim _ _) }
height := 0
chains_bounded := boundedChains_of_subsingleton α 0
theorem bot_le (a : α) : (⊥ : α) ≤ a := FixedHeight.bot_le a
end FiniteHeightLattice

246
lean/Spa/Lattice/AboveBelow.lean
View File

@@ -1,38 +1,7 @@
import Spa.Lattice
/-!
# The Above-Below Lattice
This file defines the `AboveBelow` lattice, which takes a flat domain
$a_1, \ldots, a_n \in \alpha$ and lifts it into a lattice bounded
above by a synthetic $\top$ element, and below by a synthetic $\bot$
element.
$$
\begin{array}{ccccc}
&& \top && \\
& \swarrow & \downarrow & \searrow & \\
a_1 & & … & & a_n \\
& \searrow & \downarrow & \swarrow & \\
&& \bot &&
\end{array}
$$
This lattice is also a `Spa.FiniteHeightLattice`, because no chain can
exceed the bottom-to-top chain $\bot < a_i < \top$.
The above-below lattice is helpful for for analyses such as
`Spa/Analysis/Sign.lean` and `Spa/Analysis/Constant.lean`, whose
classifications of values (by sign or by exact value) do not have
any inherent structure beyond "matching exactly".
-/
namespace Spa
/-- The above-below lattice, with bottom element `bot` and top element `top`. -/
@[aesop safe cases]
inductive AboveBelow (α : Type*) where
| bot
| top
@@ -65,125 +34,206 @@ instance : Min (AboveBelow α) where
| mk _, bot => bot
| mk x, top => mk x
@[simp] lemma bot_sup (x : AboveBelow α) : bot ⊔ x = x := rfl
@[simp] lemma top_sup (x : AboveBelow α) : top ⊔ x = top := rfl
@[simp] lemma sup_bot (x : AboveBelow α) : x ⊔ bot = x := by cases x <;> rfl
@[simp] lemma sup_top (x : AboveBelow α) : x ⊔ top = top := by cases x <;> rfl
@[simp] lemma mk_sup_mk (x y : α) :
@[simp] theorem bot_sup (x : AboveBelow α) : bot ⊔ x = x := rfl
@[simp] theorem top_sup (x : AboveBelow α) : top ⊔ x = top := rfl
@[simp] theorem sup_bot (x : AboveBelow α) : x ⊔ bot = x := by cases x <;> rfl
@[simp] theorem sup_top (x : AboveBelow α) : x ⊔ top = top := by cases x <;> rfl
@[simp] theorem mk_sup_mk (x y : α) :
(mk x ⊔ mk y : AboveBelow α) = if x = y then mk x else top := rfl
@[simp] lemma bot_inf (x : AboveBelow α) : bot ⊓ x = bot := rfl
@[simp] lemma top_inf (x : AboveBelow α) : top ⊓ x = x := rfl
@[simp] lemma inf_bot (x : AboveBelow α) : x ⊓ bot = bot := by cases x <;> rfl
@[simp] lemma inf_top (x : AboveBelow α) : x ⊓ top = x := by cases x <;> rfl
@[simp] lemma mk_inf_mk (x y : α) :
@[simp] theorem bot_inf (x : AboveBelow α) : bot ⊓ x = bot := rfl
@[simp] theorem top_inf (x : AboveBelow α) : top ⊓ x = x := rfl
@[simp] theorem inf_bot (x : AboveBelow α) : x ⊓ bot = bot := by cases x <;> rfl
@[simp] theorem inf_top (x : AboveBelow α) : x ⊓ top = x := by cases x <;> rfl
@[simp] theorem mk_inf_mk (x y : α) :
(mk x ⊓ mk y : AboveBelow α) = if x = y then mk x else bot := rfl
protected lemma sup_comm (a b : AboveBelow α) : a ⊔ b = b ⊔ a := by aesop
protected lemma sup_assoc (a b c : AboveBelow α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) := by aesop
protected lemma inf_comm (a b : AboveBelow α) : a ⊓ b = b ⊓ a := by aesop
protected lemma inf_assoc (a b c : AboveBelow α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) := by aesop
protected lemma sup_inf_self (a b : AboveBelow α) : a ⊔ a ⊓ b = a := by aesop
protected lemma inf_sup_self (a b : AboveBelow α) : a ⊓ (a ⊔ b) = a := by aesop
protected theorem sup_comm (a b : AboveBelow α) : a ⊔ b = b ⊔ a := by
rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp only
[bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk]
split_ifs with h₁ h₂ h₂ <;> simp_all
protected theorem sup_assoc (a b c : AboveBelow α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) := by
rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases c with _ | _ | z <;>
simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk]
split_ifs <;> simp_all
protected theorem inf_comm (a b : AboveBelow α) : a ⊓ b = b ⊓ a := by
rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp only
[bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk]
split_ifs with h₁ h₂ h₂ <;> simp_all
protected theorem inf_assoc (a b c : AboveBelow α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) := by
rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases c with _ | _ | z <;>
simp only [bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk]
split_ifs <;> simp_all
protected theorem sup_inf_self (a b : AboveBelow α) : a ⊔ a ⊓ b = a := by
rcases a with _ | _ | x <;> rcases b with _ | _ | y <;>
simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk,
bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] <;>
try (split_ifs <;> simp_all)
protected theorem inf_sup_self (a b : AboveBelow α) : a ⊓ (a ⊔ b) = a := by
rcases a with _ | _ | x <;> rcases b with _ | _ | y <;>
simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk,
bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] <;>
try (split_ifs <;> simp_all)
instance : Lattice (AboveBelow α) :=
Lattice.mk' AboveBelow.sup_comm AboveBelow.sup_assoc
AboveBelow.inf_comm AboveBelow.inf_assoc
AboveBelow.sup_inf_self AboveBelow.inf_sup_self
lemma le_iff {a b : AboveBelow α} : a ≤ b ↔ a ⊔ b = b := sup_eq_right.symm
theorem le_iff {a b : AboveBelow α} : a ≤ b ↔ a ⊔ b = b := sup_eq_right.symm
lemma bot_le' (a : AboveBelow α) : (bot : AboveBelow α) ≤ a :=
theorem bot_le' (a : AboveBelow α) : (bot : AboveBelow α) ≤ a :=
le_iff.mpr (bot_sup a)
lemma le_top' (a : AboveBelow α) : a ≤ (top : AboveBelow α) :=
theorem le_top' (a : AboveBelow α) : a ≤ (top : AboveBelow α) :=
le_iff.mpr (sup_top a)
instance : OrderBot (AboveBelow α) where
bot := bot
bot_le := bot_le'
theorem bot_lt_mk (x : α) : (bot : AboveBelow α) < mk x :=
lt_of_le_of_ne (bot_le' _) (by simp)
instance : OrderTop (AboveBelow α) where
top := top
le_top := le_top'
theorem mk_lt_top (x : α) : (mk x : AboveBelow α) < top :=
lt_of_le_of_ne (le_top' _) (by simp)
lemma bot_lt_mk (x : α) : (bot : AboveBelow α) < mk x := lt_of_le_of_ne (bot_le' _) (by simp)
lemma mk_lt_top (x : α) : (mk x : AboveBelow α) < top := lt_of_le_of_ne (le_top' _) (by simp)
lemma bot_lt_top : (bot : AboveBelow α) < top := lt_of_le_of_ne (bot_le' _) (by simp)
theorem bot_lt_top : (bot : AboveBelow α) < top :=
lt_of_le_of_ne (bot_le' _) (by simp)
lemma le_cases {a b : AboveBelow α} (h : a ≤ b) :
theorem le_cases {a b : AboveBelow α} (h : a ≤ b) :
a = bot ∨ b = top ∨ a = b := by
rw [le_iff] at h
rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp_all
have hsup := le_iff.mp h
rcases a with _ | _ | x <;> rcases b with _ | _ | y
· exact Or.inl rfl
· exact Or.inr (Or.inl rfl)
· exact Or.inl rfl
· exact absurd hsup (by simp)
· exact Or.inr (Or.inl rfl)
· exact absurd hsup (by simp)
· exact absurd hsup (by simp)
· exact Or.inr (Or.inl rfl)
· rw [mk_sup_mk] at hsup
by_cases hxy : x = y
· exact Or.inr (Or.inr (by rw [hxy]))
· rw [if_neg hxy] at hsup
exact absurd hsup (by simp)
/-- If `f` sends `⊥` to `⊥` (in both arguments) and `⊤` to `⊤`
(against any non-`⊥` argument), it is monotone in both arguments.
The values of the the elements in `α` are irrelevant since they
are always incomparable. This makes it easy to prove monotonicity
for operations that "just" combine their flat elements, or give up. -/
lemma monotone₂_of_strict {β γ : Type*} [DecidableEq β] [DecidableEq γ]
/-- Monotonicity for *strict* operations on flat lattices: if `f` sends `⊥` to
`⊥` (in either argument) and `⊤` to `⊤` (against any non-`⊥` argument), it is
monotone in both arguments — regardless of its values on plain elements.
`Analysis/Sign.agda` and `Analysis/Constant.agda` postulated exactly these
monotonicity facts for their `plus`/`minus`, all of which have this shape. -/
theorem monotone₂_of_strict {β γ : Type*} [DecidableEq β] [DecidableEq γ]
(f : AboveBelow α → AboveBelow β → AboveBelow γ)
(hbotl : ∀ y, f bot y = bot) (hbotr : ∀ x, f x bot = bot)
(htopl : ∀ y, y ≠ bot → f top y = top)
(htopr : ∀ x, x ≠ bot → f x top = top) : Monotone₂ f := by
constructor <;> intro c a b hab <;>
rcases eq_or_ne c bot with rfl | hc <;>
rcases le_cases hab with rfl | rfl | rfl <;>
simp [hbotl, hbotr, htopl, htopr, bot_le', le_top', *]
constructor
· intro y a b hab
show f a y ≤ f b y
rcases le_cases hab with rfl | rfl | rfl
· rw [hbotl]; exact bot_le' _
· rcases eq_or_ne y bot with rfl | hy
· rw [hbotr, hbotr]
· rw [htopl y hy]; exact le_top' _
· exact le_rfl
· intro x a b hab
show f x a ≤ f x b
rcases le_cases hab with rfl | rfl | rfl
· rw [hbotr]; exact bot_le' _
· rcases eq_or_ne x bot with rfl | hx
· rw [hbotl, hbotl]
· rw [htopr x hx]; exact le_top' _
· exact le_rfl
/-! ### Interpretations of flat lattices -/
section Interp
variable {V : Type*} {P : AboveBelow α → V → Prop}
/-- As long as the interpretation of a the above-below lattice respects the
fact that `bot` means "impossible", interpreting the above-below
lattice agrees with its `⊔`. -/
lemma interp_sup_of (hbot : ∀ v, ¬P bot v) (htop : ∀ v, P top v)
{s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∨ P s₂ v) : P (s₁ ⊔ s₂) v := by aesop
theorem interp_sup_of (hbot : ∀ v, ¬P bot v) (htop : ∀ v, P top v)
{s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∨ P s₂ v) : P (s₁ ⊔ s₂) v := by
rcases s₁ with _ | _ | x
· rw [bot_sup]; exact h.resolve_left (hbot v)
· rw [top_sup]; exact htop v
· rcases s₂ with _ | _ | y
· rw [sup_bot]; exact h.resolve_right (hbot v)
· rw [sup_top]; exact htop v
· rw [mk_sup_mk]
split
· next heq => subst heq; exact h.elim id id
· exact htop v
/-- As long as two distinct values in the flat domain don't overlap,
interpreting the above-below lattice agrees with its `⊔` -/
lemma interp_inf_of
theorem interp_inf_of
(hdisj : ∀ {x y : α}, x ≠ y → ∀ v, ¬(P (mk x) v ∧ P (mk y) v))
{s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∧ P s₂ v) : P (s₁ ⊓ s₂) v := by
rcases s₁ with _ | _ | x <;> rcases s₂ with _ | _ | y <;> simp_all
rcases s₁ with _ | _ | x
· rw [bot_inf]; exact h.1
· rw [top_inf]; exact h.2
· rcases s₂ with _ | _ | y
· rw [inf_bot]; exact h.2
· rw [inf_top]; exact h.1
· rw [mk_inf_mk]
split
· exact h.2
· next hne => exact (hdisj hne v h.1 h.2).elim
· next heq => subst heq; exact h.1
· next hne => exact absurd h (hdisj hne v)
end Interp
/-- synthetic rank of an element, used to prove chain bounds. -/
private def rank : AboveBelow α → ℕ
/-- Rank of an element: `⊥ ↦ 0`, `[x] ↦ 1`, `⊤ ↦ 2`. Used to bound chains
(Agda's `isLongest` / `x≺[y]⇒x≡⊥` / `[x]≺y⇒y≡⊤` case analysis lives here). -/
def rank : AboveBelow α → ℕ
| bot => 0
| mk _ => 1
| top => 2
/-- It's not possible for any two lifted flat-domain elements to be less
than one another. -/
lemma not_mk_lt_mk (x y : α) : ¬(mk x : AboveBelow α) < mk y := by
/-- Agda: the impossibility of `[x] ≺ [y]` (combines `x≺[y]⇒x≡⊥` and
`[x]≺y⇒y≡⊤`: the flat middle layer is an antichain). -/
theorem not_mk_lt_mk (x y : α) : ¬(mk x : AboveBelow α) < mk y := by
intro h
obtain ⟨hle, hne⟩ := lt_iff_le_and_ne.mp h
rcases le_cases hle with h | h | h <;> simp_all
have hsup := le_iff.mp hle
rw [mk_sup_mk] at hsup
by_cases hxy : x = y
· rw [if_pos hxy] at hsup
exact hne hsup
· rw [if_neg hxy] at hsup
exact absurd hsup (by simp)
/-- The rank of elements is strictly monotonic. -/
lemma rank_strictMono : StrictMono (rank : AboveBelow α → ℕ) := by
theorem rank_strictMono : StrictMono (rank : AboveBelow α → ℕ) := by
intro a b hab
rcases a with _ | _ | x <;> rcases b with _ | _ | y <;>
simp_all [rank, not_mk_lt_mk, (bot_le' _).not_lt, (le_top' _).not_lt]
rcases a with _ | _ | x <;> rcases b with _ | _ | y
· exact absurd hab (lt_irrefl _)
· simp [rank]
· simp [rank]
· exact absurd hab (bot_le' _).not_lt
· exact absurd hab (lt_irrefl _)
· exact absurd hab (le_top' _).not_lt
· exact absurd hab (bot_le' _).not_lt
· simp [rank]
· exact absurd hab (not_mk_lt_mk x y)
/-- All chains in the above-below lattice have at most 2 comparisons. -/
lemma boundedChains : BoundedChains (AboveBelow α) 2 := fun c => by
theorem boundedChains : BoundedChains (AboveBelow α) 2 := fun c => by
have h := LTSeries.head_add_length_le_nat (c.map rank rank_strictMono)
rw [LTSeries.head_map, LTSeries.last_map, LTSeries.map_length] at h
have h2 : rank c.last ≤ 2 := by cases c.last <;> simp [rank]
omega
instance [Inhabited α] : FiniteHeightLattice (AboveBelow α) where
toLattice := inferInstance
toOrderBot := inferInstance
toOrderTop := inferInstance
bot := bot
top := top
height := 2
longestChain :=
{ series :=
((RelSeries.singleton _ bot).snoc (mk default)
(by rw [RelSeries.last_singleton]; exact bot_lt_mk default)).snoc top
(by rw [RelSeries.last_snoc]; exact mk_lt_top default)
head_series := by simp
last_series := by simp
length_series := by simp [RelSeries.snoc, RelSeries.append] }
chains_bounded := boundedChains
end AboveBelow

39
lean/Spa/Lattice/Bool.lean
View File

@@ -1,39 +0,0 @@
import Spa.Lattice
import Mathlib.Order.BooleanAlgebra
namespace Spa
/-! ### `Bool` as a finite-height lattice
`Bool` is the two-element lattice `false ≤ true` (with `⊥ = false`, `⊤ = true`).
It is the building block of the "power set" lattice `FiniteMap A Bool ks`, used by
the reaching-definitions analysis to represent sets of definition sites. -/
namespace Bool
/-- Rank of a boolean: `false ↦ 0`, `true ↦ 1`. Used to bound chains, mirroring
`AboveBelow.rank`. -/
def rank : Bool → ℕ
| false => 0
| true => 1
lemma rank_strictMono : StrictMono rank := by
intro a b hab
cases a <;> cases b <;> revert hab <;> decide
lemma boundedChains : BoundedChains Bool 1 := fun c => by
have h := LTSeries.head_add_length_le_nat (c.map rank rank_strictMono)
rw [LTSeries.head_map, LTSeries.last_map, LTSeries.map_length] at h
have h2 : rank c.last ≤ 1 := by cases c.last <;> simp [rank]
omega
instance : FiniteHeightLattice Bool where
toLattice := inferInstance
toOrderBot := inferInstance
toOrderTop := inferInstance
height := 1
chains_bounded := boundedChains
end Bool
end Spa

608
lean/Spa/Lattice/FiniteMap.lean
View File

@@ -1,207 +1,425 @@
import Spa.Lattice.Tuple
import Mathlib.Data.List.Nodup
/-!
# Finite Maps
This file defines _finite maps_, or key-value maps with a finite domain. This
is encoded as a map from `Fin` into the value type. Finite maps form a
lattice from pointwise composition: $(f \land g) k = f k \land g k$,
and, provided the domain `\beta` is of finite height, so is the map
lattice as a whole.
In fact, the isomorphism is described and proven in `Spa/Lattice/Tuple.lean`.
-/
import Spa.Lattice.IterProd
import Spa.Isomorphism
namespace Spa
/-- Key-value map with domain `α` and codomain `β`, with possible keys $\textit{ks} \subseteq \alpha$. -/
def FiniteMap (α β : Type*) (ks : List α) : Type _ := Fin ks.length → β
def FiniteMap (A B : Type*) (ks : List A) : Type _ :=
{ l : List (A × B) // l.map Prod.fst = ks }
namespace FiniteMap
variable {α β : Type*} {ks : List α}
variable {A B : Type*} {ks : List A}
instance [Lattice β] : Lattice (FiniteMap α β ks) :=
inferInstanceAs (Lattice (Fin ks.length → β))
instance [DecidableEq A] [DecidableEq B] : DecidableEq (FiniteMap A B ks) :=
fun a b => decidable_of_iff (a.val = b.val) Subtype.ext_iff.symm
instance [FiniteHeightLattice β] : FiniteHeightLattice (FiniteMap α β ks) :=
inferInstanceAs (FiniteHeightLattice (Fin ks.length → β))
theorem spine_eq (fm₁ fm₂ : FiniteMap A B ks) :
fm₁.val.map Prod.fst = fm₂.val.map Prod.fst :=
fm₁.property.trans fm₂.property.symm
instance [DecidableEq β] : DecidableEq (FiniteMap α β ks) :=
inferInstanceAs (DecidableEq (Fin ks.length → β))
def combine (f : B → B → B) (l₁ l₂ : List (A × B)) : List (A × B) :=
List.zipWith (fun p q => (p.1, f p.2 q.2)) l₁ l₂
instance : Membership (α × β) (FiniteMap α β ks) :=
⟨fun fm p => ∃ i : Fin ks.length, ks.get i = p.1 ∧ fm i = p.2⟩
theorem combine_spine (f : B → B → B) : ∀ {l₁ l₂ : List (A × B)},
l₁.map Prod.fst = l₂.map Prod.fst →
(combine f l₁ l₂).map Prod.fst = l₁.map Prod.fst
| [], [], _ => rfl
| p :: l₁, q :: l₂, h => by
simp only [List.map_cons, List.cons.injEq] at h
simp only [combine, List.zipWith_cons_cons, List.map_cons]
exact congrArg _ (combine_spine f h.2)
| [], _ :: _, h => by simp at h
| _ :: _, [], h => by simp at h
lemma mem_iff {fm : FiniteMap α β ks} {p : α × β} :
p ∈ fm ↔ ∃ i : Fin ks.length, ks.get i = p.1 ∧ fm i = p.2 := Iff.rfl
theorem combine_comm (f : B → B → B) (hf : ∀ a b, f a b = f b a) :
∀ {l₁ l₂ : List (A × B)}, l₁.map Prod.fst = l₂.map Prod.fst →
combine f l₁ l₂ = combine f l₂ l₁
| [], [], _ => rfl
| p :: l₁, q :: l₂, h => by
simp only [List.map_cons, List.cons.injEq] at h
simp only [combine, List.zipWith_cons_cons]
rw [h.1, hf]
exact congrArg _ (combine_comm f hf h.2)
| [], _ :: _, h => by simp at h
| _ :: _, [], h => by simp at h
def MemKey (k : α) (_fm : FiniteMap α β ks) : Prop := k ∈ ks
theorem combine_assoc (f : B → B → B) (hf : ∀ a b c, f (f a b) c = f a (f b c)) :
∀ {l₁ l₂ l₃ : List (A × B)},
l₁.map Prod.fst = l₂.map Prod.fst → l₂.map Prod.fst = l₃.map Prod.fst →
combine f (combine f l₁ l₂) l₃ = combine f l₁ (combine f l₂ l₃)
| [], [], [], _, _ => rfl
| p :: l₁, q :: l₂, r :: l₃, h₁₂, h₂₃ => by
simp only [List.map_cons, List.cons.injEq] at h₁₂ h₂₃
simp only [combine, List.zipWith_cons_cons]
rw [hf]
exact congrArg _ (combine_assoc f hf h₁₂.2 h₂₃.2)
| [], [], _ :: _, _, h => by simp at h
| [], _ :: _, _, h, _ => by simp at h
| _ :: _, [], _, h, _ => by simp at h
| _ :: _, _ :: _, [], _, h => by simp at h
lemma MemKey_iff {k : α} {fm : FiniteMap α β ks} : MemKey k fm ↔ k ∈ ks := Iff.rfl
theorem combine_absorb (f g : B → B → B) (hfg : ∀ a b, f a (g a b) = a) :
∀ {l₁ l₂ : List (A × B)}, l₁.map Prod.fst = l₂.map Prod.fst →
combine f l₁ (combine g l₁ l₂) = l₁
| [], [], _ => rfl
| p :: l₁, q :: l₂, h => by
simp only [List.map_cons, List.cons.injEq] at h
simp only [combine, List.zipWith_cons_cons, hfg]
exact congrArg _ (combine_absorb f g hfg h.2)
| [], _ :: _, h => by simp at h
| _ :: _, [], h => by simp at h
instance {k : α} {fm : FiniteMap α β ks} [DecidableEq α] : Decidable (MemKey k fm) :=
decidable_of_iff _ MemKey_iff.symm
variable [Lattice B]
lemma mem_key_of_mem {k : α} {v : β} {fm : FiniteMap α β ks}
(h : (k, v) ∈ fm) : MemKey k fm := by
obtain ⟨i, hi, _⟩ := h
have hik : ks.get i = k := hi
exact hik ▸ ks.get_mem i
instance : Max (FiniteMap A B ks) where
max fm₁ fm₂ :=
⟨combine (· ⊔ ·) fm₁.val fm₂.val,
(combine_spine _ (spine_eq fm₁ fm₂)).trans fm₁.property⟩
def toList (fm : FiniteMap α β ks) : List (α × β) :=
(List.finRange ks.length).map fun i => (ks.get i, fm i)
instance : Min (FiniteMap A B ks) where
min fm₁ fm₂ :=
⟨combine (· ⊓ ·) fm₁.val fm₂.val,
(combine_spine _ (spine_eq fm₁ fm₂)).trans fm₁.property⟩
lemma le_def [Lattice β] {fm₁ fm₂ : FiniteMap α β ks} :
fm₁ ≤ fm₂ ↔ ∀ i, fm₁ i ≤ fm₂ i := Iff.rfl
@[simp] theorem sup_val (fm₁ fm₂ : FiniteMap A B ks) :
(fm₁ ⊔ fm₂).val = combine (· ⊔ ·) fm₁.val fm₂.val := rfl
@[simp] theorem inf_val (fm₁ fm₂ : FiniteMap A B ks) :
(fm₁ ⊓ fm₂).val = combine (· ⊓ ·) fm₁.val fm₂.val := rfl
instance : Lattice (FiniteMap A B ks) :=
Lattice.mk'
(fun a b => Subtype.ext (combine_comm _ sup_comm (spine_eq a b)))
(fun a b c => Subtype.ext (combine_assoc _ sup_assoc (spine_eq a b) (spine_eq b c)))
(fun a b => Subtype.ext (combine_comm _ inf_comm (spine_eq a b)))
(fun a b c => Subtype.ext (combine_assoc _ inf_assoc (spine_eq a b) (spine_eq b c)))
(fun a b => Subtype.ext (combine_absorb _ _ (fun _ _ => sup_inf_self) (spine_eq a b)))
(fun a b => Subtype.ext (combine_absorb _ _ (fun _ _ => inf_sup_self) (spine_eq a b)))
instance : Membership (A × B) (FiniteMap A B ks) :=
⟨fun fm p => p ∈ fm.val⟩
omit [Lattice B] in
theorem mem_def {p : A × B} {fm : FiniteMap A B ks} : p ∈ fm ↔ p ∈ fm.val :=
Iff.rfl
def MemKey (k : A) (fm : FiniteMap A B ks) : Prop :=
k ∈ fm.val.map Prod.fst
omit [Lattice B] in
theorem memKey_iff {k : A} {fm : FiniteMap A B ks} : MemKey k fm ↔ k ∈ ks := by
rw [MemKey, fm.property]
instance {k : A} {fm : FiniteMap A B ks} [DecidableEq A] :
Decidable (MemKey k fm) :=
decidable_of_iff _ memKey_iff.symm
omit [Lattice B] in
theorem mem_key_of_mem {k : A} {v : B} {fm : FiniteMap A B ks}
(h : (k, v) ∈ fm) : MemKey k fm :=
List.mem_map_of_mem _ h
section Locate
variable [DecidableEq α]
variable [DecidableEq A]
/-- Recover the value stored under a present key. -/
def locate {k : α} {fm : FiniteMap α β ks} (h : MemKey k fm) :
{v : β // (k, v) ∈ fm} :=
let i : Fin ks.length := ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩
⟨fm i, i, List.idxOf_get _, rfl⟩
private def locateList (k : A) :
(l : List (A × B)) → k ∈ l.map Prod.fst → {v : B // (k, v) ∈ l}
| [], h => absurd h (by simp)
| p :: l', h =>
if heq : p.1 = k then
⟨p.2, by rw [← heq]; exact List.mem_cons_self ..⟩
else
let ⟨v, hv⟩ := locateList k l' (by
rcases List.mem_cons.mp h with h' | h'
· exact absurd h'.symm heq
· exact h')
⟨v, List.mem_cons_of_mem _ hv⟩
def locate {k : A} {fm : FiniteMap A B ks} (h : MemKey k fm) :
{v : B // (k, v) ∈ fm} :=
locateList k fm.val h
end Locate
variable [Lattice β]
theorem combine_eq_right_iff : ∀ {l₁ l₂ : List (A × B)},
l₁.map Prod.fst = l₂.map Prod.fst →
(combine (· ⊔ ·) l₁ l₂ = l₂ ↔
List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂)
| [], [], _ => by simp [combine]
| p :: l₁, q :: l₂, h => by
simp only [List.map_cons, List.cons.injEq] at h
simp only [combine, List.zipWith_cons_cons, List.cons.injEq,
List.forall₂_cons, Prod.ext_iff]
rw [show List.zipWith (fun p q : A × B => (p.1, p.2 ⊔ q.2)) l₁ l₂
= combine (· ⊔ ·) l₁ l₂ from rfl,
combine_eq_right_iff h.2]
constructor
· rintro ⟨⟨hk, hv⟩, hrest⟩
exact ⟨⟨hk, sup_eq_right.mp hv⟩, hrest⟩
· rintro ⟨⟨hk, hv⟩, hrest⟩
exact ⟨⟨hk, sup_eq_right.mpr hv⟩, hrest⟩
| [], _ :: _, h => by simp at h
| _ :: _, [], h => by simp at h
lemma le_of_mem_mem (hks : ks.Nodup) {fm₁ fm₂ : FiniteMap α β ks}
(hle : fm₁ ≤ fm₂) {k : α} {v₁ v₂ : β}
(h₁ : (k, v₁) ∈ fm₁) (h₂ : (k, v₂) ∈ fm₂) : v₁ ≤ v₂ := by
obtain ⟨i, hi, rfl⟩ := h₁
obtain ⟨j, hj, rfl⟩ := h₂
have hij : i = j := hks.get_inj_iff.mp (hi.trans hj.symm)
subst hij
exact le_def.mp hle i
theorem le_iff {fm₁ fm₂ : FiniteMap A B ks} :
fm₁ ≤ fm₂ ↔
List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) fm₁.val fm₂.val := by
rw [← sup_eq_right, ← combine_eq_right_iff (spine_eq fm₁ fm₂), Subtype.ext_iff,
sup_val]
lemma mem_sup {fm₁ fm₂ : FiniteMap α β ks} {k : α} {v : β}
private theorem forall₂_spine : ∀ {l₁ l₂ : List (A × B)},
List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂ →
l₁.map Prod.fst = l₂.map Prod.fst
| _, _, List.Forall₂.nil => rfl
| _, _, List.Forall₂.cons hpq hrest => by
simp [List.map_cons, hpq.1, forall₂_spine hrest]
private theorem forall₂_mem_mem {l₁ l₂ : List (A × B)}
(hf : List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂) :
(l₁.map Prod.fst).Nodup →
∀ {k : A} {v₁ v₂ : B}, (k, v₁) ∈ l₁ → (k, v₂) ∈ l₂ → v₁ ≤ v₂ := by
induction hf with
| nil =>
intro _ k v₁ v₂ h₁ _
simp at h₁
| @cons p q l₁' l₂' hpq hrest ih =>
intro hnd k v₁ v₂ h₁ h₂
simp only [List.map_cons, List.nodup_cons] at hnd
have hspine := forall₂_spine hrest
rcases List.mem_cons.mp h₁ with heq₁ | h₁'
· rcases List.mem_cons.mp h₂ with heq₂ | h₂'
· rw [← heq₁, ← heq₂] at hpq
exact hpq.2
· exfalso
apply hnd.1
rw [show p.1 = k from (congrArg Prod.fst heq₁).symm, hspine]
exact List.mem_map_of_mem _ h₂'
· rcases List.mem_cons.mp h₂ with heq₂ | h₂'
· exfalso
apply hnd.1
rw [hpq.1, show q.1 = k from (congrArg Prod.fst heq₂).symm]
exact List.mem_map_of_mem _ h₁'
· exact ih hnd.2 h₁' h₂'
theorem le_of_mem_mem (hks : ks.Nodup) {fm₁ fm₂ : FiniteMap A B ks}
(hle : fm₁ ≤ fm₂) {k : A} {v₁ v₂ : B}
(h₁ : (k, v₁) ∈ fm₁) (h₂ : (k, v₂) ∈ fm₂) : v₁ ≤ v₂ :=
forall₂_mem_mem (le_iff.mp hle) (fm₁.property.symm ▸ hks) h₁ h₂
omit [Lattice B] in
private theorem mem_combine (f : B → B → B) : ∀ {l₁ l₂ : List (A × B)} {k : A} {v : B},
l₁.map Prod.fst = l₂.map Prod.fst →
(k, v) ∈ combine f l₁ l₂ →
∃ v₁ v₂, v = f v₁ v₂ ∧ (k, v₁) ∈ l₁ ∧ (k, v₂) ∈ l₂
| [], [], _, _, _, h => by simp [combine] at h
| p :: l₁, q :: l₂, k, v, hsp, h => by
simp only [List.map_cons, List.cons.injEq] at hsp
simp only [combine, List.zipWith_cons_cons] at h
rcases List.mem_cons.mp h with heq | h'
· injection heq with hk hv
exact ⟨p.2, q.2, hv,
by rw [hk]; simp,
by rw [hk, hsp.1]; simp⟩
· obtain ⟨v₁, v₂, hv, h₁, h₂⟩ := mem_combine f hsp.2 h'
exact ⟨v₁, v₂, hv, List.mem_cons_of_mem _ h₁, List.mem_cons_of_mem _ h₂⟩
theorem mem_sup {fm₁ fm₂ : FiniteMap A B ks} {k : A} {v : B}
(h : (k, v) ∈ fm₁ ⊔ fm₂) :
∃ v₁ v₂, v = v₁ ⊔ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ := by
obtain ⟨i, hi, rfl⟩ := h
exact ⟨fm₁ i, fm₂ i, rfl, ⟨i, hi, rfl⟩, ⟨i, hi, rfl⟩⟩
lemma mem_inf {fm₁ fm₂ : FiniteMap α β ks} {k : α} {v : β}
(h : (k, v) ∈ fm₁ ⊓ fm₂) :
∃ v₁ v₂, v = v₁ ⊓ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ := by
obtain ⟨i, hi, rfl⟩ := h
exact ⟨fm₁ i, fm₂ i, rfl, ⟨i, hi, rfl⟩, ⟨i, hi, rfl⟩⟩
∃ v₁ v₂, v = v₁ ⊔ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ :=
mem_combine _ (spine_eq fm₁ fm₂) h
section Updating
variable [DecidableEq α]
variable [DecidableEq A]
def updating (fm : FiniteMap α β ks) (ks' : List α) (g : α → β) : FiniteMap α β ks :=
fun i => if ks.get i ∈ ks' then g (ks.get i) else fm i
def updating (fm : FiniteMap A B ks) (ks' : List A) (g : A → B) :
FiniteMap A B ks :=
⟨fm.val.map (fun p => if p.1 ∈ ks' then (p.1, g p.1) else p), by
rw [List.map_map,
show (Prod.fst ∘ fun p : A × B => if p.1 ∈ ks' then (p.1, g p.1) else p)
= Prod.fst from funext fun p => by by_cases h : p.1 ∈ ks' <;> simp [h]]
exact fm.property⟩
omit [Lattice β] in
lemma eq_of_mem_updating {k : α} {v : β} {fm : FiniteMap α β ks}
{ks' : List α} {g : α → β} (hk : k ∈ ks')
omit [Lattice B] in
@[simp] theorem updating_val (fm : FiniteMap A B ks) (ks' : List A) (g : A → B) :
(updating fm ks' g).val
= fm.val.map (fun p => if p.1 ∈ ks' then (p.1, g p.1) else p) := rfl
omit [Lattice B] in
theorem memKey_updating {k : A} {fm : FiniteMap A B ks} {ks' : List A} {g : A → B} :
MemKey k (updating fm ks' g) ↔ MemKey k fm := by
rw [memKey_iff, memKey_iff]
omit [Lattice B] in
theorem eq_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
{ks' : List A} {g : A → B} (hk : k ∈ ks')
(h : (k, v) ∈ updating fm ks' g) : v = g k := by
obtain ⟨i, hi, rfl⟩ := h
show (if ks.get i ∈ ks' then g (ks.get i) else fm i) = g k
rw [if_pos (by rw [hi]; exact hk), hi]
obtain ⟨p, hp, heq⟩ := List.mem_map.mp h
by_cases hmem : p.1 ∈ ks'
· rw [if_pos hmem] at heq
injection heq with h1 h2
rw [← h2, h1]
· rw [if_neg hmem] at heq
rw [heq] at hmem
exact absurd hk hmem
omit [Lattice β] in
lemma mem_of_mem_updating {k : α} {v : β} {fm : FiniteMap α β ks}
{ks' : List α} {g : α → β} (hk : k ∉ ks')
omit [Lattice B] in
theorem mem_updating {k : A} {fm : FiniteMap A B ks} {ks' : List A} {g : A → B}
(hk : k ∈ ks') (hmem : MemKey k fm) : (k, g k) ∈ updating fm ks' g := by
obtain ⟨v, hv⟩ := locate hmem
exact List.mem_map.mpr ⟨(k, v), hv, by simp [hk]⟩
omit [Lattice B] in
theorem mem_updating_of_not_mem {k : A} {v : B} {fm : FiniteMap A B ks}
{ks' : List A} {g : A → B} (hk : k ∉ ks') (h : (k, v) ∈ fm) :
(k, v) ∈ updating fm ks' g :=
List.mem_map.mpr ⟨(k, v), h, by simp [hk]⟩
omit [Lattice B] in
theorem mem_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
{ks' : List A} {g : A → B} (hk : k ∉ ks')
(h : (k, v) ∈ updating fm ks' g) : (k, v) ∈ fm := by
obtain ⟨i, hi, rfl⟩ := h
refine ⟨i, hi, ?_⟩
show fm i = (if ks.get i ∈ ks' then g (ks.get i) else fm i)
rw [if_neg (by rw [hi]; exact hk)]
obtain ⟨p, hp, heq⟩ := List.mem_map.mp h
by_cases hmem : p.1 ∈ ks'
· rw [if_pos hmem] at heq
injection heq with h1 _
rw [← h1] at hk
exact absurd hmem hk
· rw [if_neg hmem] at heq
exact heq ▸ hp
lemma updating_mono {fm₁ fm₂ : FiniteMap α β ks} {ks' : List α}
{g₁ g₂ : α → β} (hfm : fm₁ ≤ fm₂) (hg : ∀ k, g₁ k ≤ g₂ k) :
private theorem updating_mono_list {ks' : List A} {g₁ g₂ : A → B}
(hg : ∀ k, g₁ k ≤ g₂ k) {l₁ l₂ : List (A × B)}
(hl : List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂) :
List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2)
(l₁.map fun p => if p.1 ∈ ks' then (p.1, g₁ p.1) else p)
(l₂.map fun p => if p.1 ∈ ks' then (p.1, g₂ p.1) else p) := by
induction hl with
| nil => exact List.Forall₂.nil
| @cons x y l₁' l₂' hpq hrest ih =>
simp only [List.map_cons]
refine List.Forall₂.cons ?_ ih
obtain ⟨hk, hv⟩ := hpq
by_cases h : x.1 ∈ ks'
· rw [if_pos h, if_pos (hk ▸ h)]
exact ⟨hk, hk ▸ hg x.1⟩
· rw [if_neg h, if_neg (fun hy => h (hk.symm ▸ hy))]
exact ⟨hk, hv⟩
theorem updating_mono {fm₁ fm₂ : FiniteMap A B ks} {ks' : List A}
{g₁ g₂ : A → B} (hfm : fm₁ ≤ fm₂) (hg : ∀ k, g₁ k ≤ g₂ k) :
updating fm₁ ks' g₁ ≤ updating fm₂ ks' g₂ := by
rw [le_def]
intro i
show (if ks.get i ∈ ks' then g₁ (ks.get i) else fm₁ i)
≤ (if ks.get i ∈ ks' then g₂ (ks.get i) else fm₂ i)
split
· exact hg (ks.get i)
· exact le_def.mp hfm i
rw [le_iff] at hfm ⊢
simp only [updating_val]
exact updating_mono_list hg hfm
end Updating
section GeneralizedUpdate
variable [DecidableEq α] {L : Type*} [Lattice L]
variable [DecidableEq A] {L : Type*} [Lattice L]
def generalizedUpdate (f : L → FiniteMap α β ks) (g : α → L → β)
(ks' : List α) : L → FiniteMap α β ks := fun l =>
def generalizedUpdate (f : L → FiniteMap A B ks) (g : A → L → B)
(ks' : List A) (l : L) : FiniteMap A B ks :=
(f l).updating ks' (fun k => g k l)
variable {f : L → FiniteMap α β ks} {g : α → L → β} {ks' : List α}
variable {f : L → FiniteMap A B ks} {g : A → L → B} {ks' : List A}
lemma generalizedUpdate_monotone (hf : Monotone f)
theorem generalizedUpdate_monotone (hf : Monotone f)
(hg : ∀ k, Monotone (g k)) : Monotone (generalizedUpdate f g ks') :=
fun _ _ hl => updating_mono (hf hl) (fun k => hg k hl)
omit [Lattice β] [Lattice L] in
lemma generalizedUpdate_mem_eq {k : α} {v : β} {l : L} (hk : k ∈ ks')
(h : (k, v) ∈ generalizedUpdate f g ks' l) : v = g k l :=
eq_of_mem_updating (g := fun k => g k l) hk h
omit [Lattice B] [Lattice L] in
theorem generalizedUpdate_memKey {k : A} {l : L}
(h : MemKey k (f l)) : MemKey k (generalizedUpdate f g ks' l) := by
unfold generalizedUpdate
exact memKey_updating.mpr h
omit [Lattice β] [Lattice L] in
lemma generalizedUpdate_not_mem_backward {k : α} {v : β} {l : L} (hk : k ∉ ks')
(h : (k, v) ∈ generalizedUpdate f g ks' l) : (k, v) ∈ f l :=
mem_of_mem_updating hk h
omit [Lattice B] [Lattice L] in
theorem generalizedUpdate_mem {k : A} {l : L} (hk : k ∈ ks')
(h : MemKey k (f l)) : (k, g k l) ∈ generalizedUpdate f g ks' l := by
unfold generalizedUpdate
exact mem_updating hk h
omit [Lattice B] [Lattice L] in
theorem generalizedUpdate_mem_eq {k : A} {v : B} {l : L} (hk : k ∈ ks')
(h : (k, v) ∈ generalizedUpdate f g ks' l) : v = g k l := by
unfold generalizedUpdate at h
exact eq_of_mem_updating (g := fun k => g k l) hk h
omit [Lattice B] [Lattice L] in
theorem generalizedUpdate_not_mem_forward {k : A} {v : B} {l : L} (hk : k ∉ ks')
(h : (k, v) ∈ f l) : (k, v) ∈ generalizedUpdate f g ks' l := by
unfold generalizedUpdate
exact mem_updating_of_not_mem hk h
omit [Lattice B] [Lattice L] in
theorem generalizedUpdate_not_mem_backward {k : A} {v : B} {l : L} (hk : k ∉ ks')
(h : (k, v) ∈ generalizedUpdate f g ks' l) : (k, v) ∈ f l := by
unfold generalizedUpdate at h
exact mem_of_mem_updating hk h
end GeneralizedUpdate
section ValuesAt
variable [DecidableEq α]
variable [DecidableEq A]
/-- The value stored under `k`, if `k` is a key. -/
private def lookup (fm : FiniteMap α β ks) (k : α) : Option β :=
if h : k ∈ ks then some (fm ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none
private def lookup? (k : A) : List (A × B) → Option B
| [] => none
| p :: l' => if p.1 = k then some p.2 else lookup? k l'
/-- The values stored under the keys `ks'` (skipping any that are not keys). -/
def valuesAt (fm : FiniteMap α β ks) (ks' : List α) : List β :=
ks'.filterMap fm.lookup
def valuesAt (fm : FiniteMap A B ks) (ks' : List A) : List B :=
ks'.filterMap (fun k => lookup? k fm.val)
omit [Lattice β] in
lemma mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap α β ks} {k : α} {v : β}
{ks' : List α} (hk : k ∈ ks') (h : (k, v) ∈ fm) : v ∈ valuesAt fm ks' := by
refine List.mem_filterMap.mpr ⟨k, hk, ?_⟩
obtain ⟨i, hi, rfl⟩ := h
have hik : ks.get i = k := hi
have hmem : k ∈ ks := hik ▸ ks.get_mem i
show (if h : k ∈ ks then
some (fm ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none) = some (fm i)
rw [dif_pos hmem]
have : (⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr hmem⟩ : Fin ks.length) = i :=
hks.get_inj_iff.mp (by rw [List.idxOf_get, hi])
rw [this]
omit [Lattice B] in
private theorem lookup?_eq_some_of_mem : ∀ {l : List (A × B)},
(l.map Prod.fst).Nodup → ∀ {k : A} {v : B}, (k, v) ∈ l →
lookup? k l = some v
| [], _, _, _, h => by simp at h
| p :: l', hnd, k, v, h => by
simp only [List.map_cons, List.nodup_cons] at hnd
rcases List.mem_cons.mp h with heq | h'
· rw [← heq]
simp [lookup?]
· rw [lookup?, if_neg ?_]
· exact lookup?_eq_some_of_mem hnd.2 h'
· intro hpk
subst hpk
have := List.mem_map_of_mem Prod.fst h'
exact hnd.1 this
private lemma lookup_rel {fm₁ fm₂ : FiniteMap α β ks} (hle : fm₁ ≤ fm₂) (k : α) :
Option.Rel (· ≤ ·) (fm₁.lookup k) (fm₂.lookup k) := by
show Option.Rel _
(if h : k ∈ ks then some (fm₁ ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none)
(if h : k ∈ ks then some (fm₂ ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none)
by_cases hk : k ∈ ks
· rw [dif_pos hk, dif_pos hk]; exact Option.Rel.some (le_def.mp hle _)
· rw [dif_neg hk, dif_neg hk]; exact Option.Rel.none
omit [Lattice B] in
theorem mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap A B ks} {k : A} {v : B}
{ks' : List A} (hk : k ∈ ks') (h : (k, v) ∈ fm) : v ∈ valuesAt fm ks' :=
List.mem_filterMap.mpr
⟨k, hk, lookup?_eq_some_of_mem (fm.property.symm ▸ hks) h⟩
lemma valuesAt_le {fm₁ fm₂ : FiniteMap α β ks} (hle : fm₁ ≤ fm₂)
(ks' : List α) :
private theorem lookup?_forall₂ {l₁ l₂ : List (A × B)}
(h : List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂) (k : A) :
Option.Rel (· ≤ ·) (lookup? k l₁) (lookup? k l₂) := by
induction h with
| nil => exact Option.Rel.none
| @cons p q l₁ l₂ hpq hrest ih =>
rw [lookup?, lookup?]
by_cases hc : q.1 = k
· rw [if_pos hc, if_pos (hpq.1.trans hc)]
exact Option.Rel.some hpq.2
· rw [if_neg hc, if_neg (fun hp => hc (hpq.1 ▸ hp))]
exact ih
theorem valuesAt_le {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂)
(ks' : List A) :
List.Forall₂ (· ≤ ·) (valuesAt fm₁ ks') (valuesAt fm₂ ks') := by
induction ks' with
| nil => exact List.Forall₂.nil
| cons k ks'' ih =>
have hrel := lookup_rel hle k
have hrel := lookup?_forall₂ (le_iff.mp hle) k
rw [valuesAt, valuesAt, List.filterMap_cons, List.filterMap_cons]
revert hrel
generalize fm₁.lookup k = o₁
generalize fm₂.lookup k = o₂
generalize lookup? k fm₁.val = o₁
generalize lookup? k fm₂.val = o₂
intro hrel
cases hrel with
| none => simpa [valuesAt] using ih
@@ -209,6 +427,120 @@ lemma valuesAt_le {fm₁ fm₂ : FiniteMap α β ks} (hle : fm₁ ≤ fm₂)
end ValuesAt
section Iso
omit [Lattice B] in
theorem val_ne_nil {k : A} {ks' : List A} (fm : FiniteMap A B (k :: ks')) :
fm.val ≠ [] := fun h => by
have hp := fm.property
rw [h] at hp
simp at hp
def headVal {k : A} {ks' : List A} : FiniteMap A B (k :: ks') → B
| ⟨[], h⟩ => absurd h (by simp)
| ⟨p :: _, _⟩ => p.2
def pop {k : A} {ks' : List A} : FiniteMap A B (k :: ks') → FiniteMap A B ks'
| ⟨[], h⟩ => absurd h (by simp)
| ⟨_ :: l, h⟩ =>
⟨l, by simp only [List.map_cons, List.cons.injEq] at h; exact h.2⟩
omit [Lattice B] in
theorem val_eq_cons {k : A} {ks' : List A} :
∀ fm : FiniteMap A B (k :: ks'), fm.val = (k, fm.headVal) :: fm.pop.val
| ⟨[], h⟩ => absurd h (by simp)
| ⟨p :: l, h⟩ => by
simp only [List.map_cons, List.cons.injEq] at h
simp [headVal, pop, ← h.1]
def toIter : {ks : List A} → FiniteMap A B ks → IterProd B PUnit ks.length
| [], _ => PUnit.unit
| _ :: _, fm => (fm.headVal, toIter fm.pop)
def ofIter : (ks : List A) → IterProd B PUnit ks.length → FiniteMap A B ks
| [], _ => ⟨[], rfl⟩
| k :: ks', ip =>
⟨(k, ip.1) :: (ofIter ks' ip.2).val, by
simp [(ofIter ks' ip.2).property]⟩
omit [Lattice B] in
theorem ofIter_toIter : ∀ {ks : List A} (fm : FiniteMap A B ks),
ofIter ks (toIter fm) = fm
| [], fm => by
obtain ⟨val, hprop⟩ := fm
cases val with
| nil => rfl
| cons p l => exact absurd hprop (by simp)
| k :: ks', fm => Subtype.ext (by
show (k, fm.headVal) :: (ofIter ks' (toIter fm.pop)).val = fm.val
rw [ofIter_toIter fm.pop, ← val_eq_cons fm])
omit [Lattice B] in
theorem toIter_ofIter : ∀ (ks : List A) (ip : IterProd B PUnit ks.length),
toIter (ofIter ks ip) = ip
| [], _ => rfl
| k :: ks', ip => by
show (headVal (ofIter (k :: ks') ip), toIter (pop (ofIter (k :: ks') ip))) = ip
rw [show pop (ofIter (k :: ks') ip) = ofIter ks' ip.2 from rfl,
toIter_ofIter ks' ip.2]
rfl
theorem headVal_le {k : A} {ks' : List A} {fm₁ fm₂ : FiniteMap A B (k :: ks')}
(h : fm₁ ≤ fm₂) : fm₁.headVal ≤ fm₂.headVal := by
have h' := le_iff.mp h
rw [val_eq_cons fm₁, val_eq_cons fm₂] at h'
exact (List.forall₂_cons.mp h').1.2
theorem pop_le {k : A} {ks' : List A} {fm₁ fm₂ : FiniteMap A B (k :: ks')}
(h : fm₁ ≤ fm₂) : fm₁.pop ≤ fm₂.pop := by
rw [le_iff]
have h' := le_iff.mp h
rw [val_eq_cons fm₁, val_eq_cons fm₂] at h'
exact (List.forall₂_cons.mp h').2
theorem toIter_monotone : ∀ {ks : List A},
Monotone (toIter : FiniteMap A B ks → IterProd B PUnit ks.length)
| [] => fun _ _ _ => le_refl _
| _ :: _ => fun _ _ h =>
Prod.mk_le_mk.mpr ⟨headVal_le h, toIter_monotone (pop_le h)⟩
theorem ofIter_monotone : ∀ (ks : List A), Monotone (ofIter (A := A) (B := B) ks)
| [] => fun _ _ _ => le_refl _
| k :: ks' => fun ip₁ ip₂ h => by
rw [le_iff]
show List.Forall₂ _ ((k, ip₁.1) :: (ofIter ks' ip₁.2).val)
((k, ip₂.1) :: (ofIter ks' ip₂.2).val)
exact List.Forall₂.cons ⟨rfl, h.1⟩ (le_iff.mp (ofIter_monotone ks' h.2))
def fixedHeight [FiniteHeightLattice B] (ks : List A) :
FiniteHeightLattice (FiniteMap A B ks) :=
FiniteHeightLattice.transport
(ofIter ks) toIter (ofIter_monotone ks) toIter_monotone
(toIter_ofIter ks) (fun fm => ofIter_toIter fm)
instance [FiniteHeightLattice B] : FiniteHeightLattice (FiniteMap A B ks) :=
fixedHeight ks
omit [Lattice B] in
theorem mem_ofIter_build {b : B} : ∀ {ks : List A} {k : A} {v : B},
(k, v) ∈ ofIter ks (IterProd.build b PUnit.unit ks.length) → v = b
| [], _, _, h => by simp [ofIter, mem_def] at h
| k' :: ks', k, v, h => by
rcases List.mem_cons.mp h with heq | h'
· exact (Prod.ext_iff.mp heq).2
· exact mem_ofIter_build h'
theorem bot_contains_bots [FiniteHeightLattice B] {k : A} {v : B}
(h : (k, v) ∈ (fixedHeight ks).bot) : v = (⊥ : B) := by
have hbot : (fixedHeight ks).bot
= ofIter ks (IterProd.build (⊥ : B) (⊥ : PUnit) ks.length) := by
show ofIter ks (IterProd.fixedHeight (A := B) (B := PUnit) ks.length).bot = _
rw [IterProd.bot_fixedHeight]
rw [hbot] at h
exact mem_ofIter_build h
end Iso
end FiniteMap
end Spa

38
lean/Spa/Lattice/Finset.lean
View File

@@ -1,38 +0,0 @@
import Spa.Lattice
import Mathlib.Data.Finset.Lattice.Basic
import Mathlib.Data.Fintype.Lattice
import Mathlib.Data.Fintype.Card
/-! # Power Sets of Finite Type
For a `Fintype α`, `Finset α` is the power-set lattice: `⊔` is union, `⊓` is
intersection, `⊥ = ∅`, `⊤ = univ`. This lattice also has a finite height.
The `Finset α` representation s isomorphic to `Fin α → Bool`, but far more
efficient because it avoids building up stacks of layered closures. -/
namespace Spa
variable {α : Type*} [Fintype α] [DecidableEq α]
omit [Fintype α] [DecidableEq α] in
private lemma finset_card_strictMono : StrictMono (Finset.card : Finset α → ℕ) :=
fun _ _ h => Finset.card_lt_card h
omit [DecidableEq α] in
/-- A strictly increasing chain of finsets grows its cardinality by at least one
each step, and cardinality is capped by `Fintype.card α`. -/
lemma finset_boundedChains : BoundedChains (Finset α) (Fintype.card α) := fun c => by
have h := LTSeries.head_add_length_le_nat (c.map Finset.card finset_card_strictMono)
rw [LTSeries.head_map, LTSeries.last_map, LTSeries.map_length] at h
have h2 : c.last.card ≤ Fintype.card α := Finset.card_le_univ _
omega
instance instFiniteHeightFinset : FiniteHeightLattice (Finset α) where
toLattice := inferInstance
toOrderBot := inferInstance
toOrderTop := inferInstance
height := Fintype.card α
chains_bounded := finset_boundedChains
end Spa

50
lean/Spa/Lattice/IterProd.lean Normal file
View File

@@ -0,0 +1,50 @@
import Spa.Lattice.Prod
import Spa.Lattice.Unit
namespace Spa
universe u
def IterProd (A B : Type u) : ℕ → Type u
| 0 => B
| k + 1 => A × IterProd A B k
namespace IterProd
variable {A B : Type u}
instance instLattice [Lattice A] [Lattice B] :
∀ k, Lattice (IterProd A B k)
| 0 => inferInstanceAs (Lattice B)
| k + 1 => @Prod.instLattice A (IterProd A B k) _ (instLattice k)
instance instDecidableEq [DecidableEq A] [DecidableEq B] :
∀ k, DecidableEq (IterProd A B k)
| 0 => inferInstanceAs (DecidableEq B)
| k + 1 => @instDecidableEqProd A (IterProd A B k) _ (instDecidableEq k)
def build (a : A) (b : B) : (k : ℕ) → IterProd A B k
| 0 => b
| k + 1 => (a, build a b k)
variable [Lattice A] [Lattice B]
def fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] :
∀ k, FiniteHeightLattice (IterProd A B k)
| 0 => inferInstanceAs (FiniteHeightLattice B)
| k + 1 => @Spa.prod A (IterProd A B k) _ (instLattice k) _ (fixedHeight k)
instance instFiniteHeight [FiniteHeightLattice A] [FiniteHeightLattice B] (k : ℕ) :
FiniteHeightLattice (IterProd A B k) := fixedHeight k
theorem bot_fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] :
∀ k, (fixedHeight (A := A) (B := B) k).bot = build (⊥ : A) (⊥ : B) k
| 0 => rfl
| k + 1 => by
show ((⊥ : A), (fixedHeight (A := A) (B := B) k).bot)
= ((⊥ : A), build (⊥ : A) (⊥ : B) k)
rw [bot_fixedHeight k]
end IterProd
end Spa

98
lean/Spa/Lattice/Prod.lean Normal file
View File

@@ -0,0 +1,98 @@
import Spa.Lattice
namespace Spa
section Unzip
variable {α β : Type*} [PartialOrder α] [PartialOrder β]
theorem LTSeries.exists_unzip (c : LTSeries (α × β)) :
∃ (c₁ : LTSeries α) (c₂ : LTSeries β),
c₁.head = c.head.1 ∧ c₁.last = c.last.1 ∧
c₂.head = c.head.2 ∧ c₂.last = c.last.2 ∧
c.length ≤ c₁.length + c₂.length := by
suffices H : ∀ (n : ℕ) (c : LTSeries (α × β)), c.length = n →
∃ (c₁ : LTSeries α) (c₂ : LTSeries β),
c₁.head = c.head.1 ∧ c₁.last = c.last.1 ∧
c₂.head = c.head.2 ∧ c₂.last = c.last.2 ∧
c.length ≤ c₁.length + c₂.length from H c.length c rfl
intro n
induction n with
| zero =>
intro c hn
refine ⟨RelSeries.singleton _ c.head.1, RelSeries.singleton _ c.head.2,
rfl, ?_, rfl, ?_, by simp [hn]⟩ <;>
· have hlast : Fin.last c.length = 0 := by ext; simp [hn]
simp [RelSeries.last, RelSeries.head, hlast]
| succ n ih =>
intro c hn
have h0 : c.length ≠ 0 := by omega
obtain ⟨c₁, c₂, hh₁, hl₁, hh₂, hl₂, hlen⟩ :=
ih (c.tail h0) (by simp [RelSeries.tail_length, hn])
rw [RelSeries.last_tail] at hl₁ hl₂
rw [RelSeries.head_tail] at hh₁ hh₂
rw [RelSeries.tail_length] at hlen
have hstep : c.head < c 1 := by
have h := c.step ⟨0, by omega⟩
have h1 : (⟨0, by omega⟩ : Fin c.length).succ = 1 := by
ext; simp [Fin.val_one, Nat.mod_eq_of_lt (by omega : 1 < c.length + 1)]
rwa [h1] at h
obtain ⟨hle1, hle2⟩ := Prod.le_def.mp hstep.le
rcases eq_or_lt_of_le hle1 with heq1 | hlt1 <;>
rcases eq_or_lt_of_le hle2 with heq2 | hlt2
· exact absurd (Prod.ext heq1 heq2) hstep.ne
· refine ⟨c₁, c₂.cons c.head.2 (hh₂ ▸ hlt2),
hh₁.trans heq1.symm, hl₁, RelSeries.head_cons .., by
rw [RelSeries.last_cons]; exact hl₂, by
simp only [RelSeries.cons_length]; omega⟩
· refine ⟨c₁.cons c.head.1 (hh₁ ▸ hlt1), c₂,
RelSeries.head_cons .., by
rw [RelSeries.last_cons]; exact hl₁,
hh₂.trans heq2.symm, hl₂, by
simp only [RelSeries.cons_length]; omega⟩
· refine ⟨c₁.cons c.head.1 (hh₁ ▸ hlt1), c₂.cons c.head.2 (hh₂ ▸ hlt2),
RelSeries.head_cons .., by
rw [RelSeries.last_cons]; exact hl₁,
RelSeries.head_cons .., by
rw [RelSeries.last_cons]; exact hl₂, by
simp only [RelSeries.cons_length]; omega⟩
end Unzip
section FixedHeight
variable {α β : Type*} [Lattice α] [Lattice β]
instance prod [A : FiniteHeightLattice α] [B : FiniteHeightLattice β] :
FiniteHeightLattice (α × β) where
bot := ((⊥ : α), (⊥ : β))
top := ((⊤ : α), (⊤ : β))
height := A.height + B.height
longestChain :=
{ series :=
RelSeries.smash
(A.longestChain.series.map (fun a => (a, (⊥ : β)))
(fun _ _ h => Prod.mk_lt_mk_iff_left.mpr h))
(B.longestChain.series.map (fun b => ((⊤ : α), b))
(fun _ _ h => Prod.mk_lt_mk_iff_right.mpr h))
(by simp [A.longestChain.last_series, B.longestChain.head_series])
head_series :=
(RelSeries.head_smash _).trans
((LTSeries.head_map _ _ _).trans
(congrArg (·, (⊥ : β)) A.longestChain.head_series))
last_series :=
(RelSeries.last_smash _).trans
((LTSeries.last_map _ _ _).trans
(congrArg ((⊤ : α), ·) B.longestChain.last_series))
length_series := by
show A.longestChain.series.length + B.longestChain.series.length = _
rw [A.longestChain.length_series, B.longestChain.length_series] }
chains_bounded := fun c => by
obtain ⟨c₁, c₂, -, -, -, -, hlen⟩ := LTSeries.exists_unzip c
have h₁ := A.chains_bounded c₁
have h₂ := B.chains_bounded c₂
omega
end FixedHeight
end Spa

128
lean/Spa/Lattice/Tuple.lean
View File

@@ -1,128 +0,0 @@
import Spa.Lattice
import Mathlib.Data.Fin.Tuple.Basic
import Mathlib.Algebra.Order.BigOperators.Group.Finset
/-!
# Finite Tuple Lattices
This file provides a proof that, in addition to being a lattice, the function
space `Fin n → β` is itself a `Spa.FiniteHeightLattice` if the element type
`β` is a lattice.
Finite tuple lattices are the workhorse behind `FiniteMap`, whose carrier is
`Fin ks.length → β`.
The proof proceeds by "unzipping" a chain (`LTSeries`):
$$
(a_1, b_1, c_1) < \ldots < (a_1, b_1, c_o) < \ldots < (a_1, b_m, c_o) <
\ldots < (a_n, b_m, c_o)
$$
In which, at each step, at least one of the components must have increased
(otherwise, the chain is not striclty increasing), into `n` chains
(`LTSeries`).
$$
\begin{aligned}
a_1 < \ldots < a_n \\
b_1 < \ldots < b_m \
c_1 < \ldots < c_o \
\end{aligned}
$$
Because at least one of the two "unzipped" chains grows with each element of
the product chain, the full chain length can't exceed the sum of the
components. By the definition of finite height, these two chains are bounded,
and therefore, the product chain is bounded too. -/
namespace Spa
namespace Tuple
variable {β : Type*}
section Unzip
variable [PartialOrder β]
open Classical in -- chain bounds are in Prop, so classical helps here.
/-- The generalized unzip: any chain in `Fin n → β` decomposes into a family of
per-tuple-coordinate chains in `β`, agreeing with the original at each end, whose
lengths sum to an upper bound on the original chain's length. -/
lemma exists_unzip {n : ℕ} (c : LTSeries (Fin n → β)) :
∃ cs : Fin n → LTSeries β,
(∀ i, (cs i).head = c.head i) ∧ (∀ i, (cs i).last = c.last i) ∧
c.length ≤ ∑ i, (cs i).length := by
suffices H : ∀ (m : ℕ) (c : LTSeries (Fin n → β)), c.length = m →
∃ cs : Fin n → LTSeries β,
(∀ i, (cs i).head = c.head i) ∧ (∀ i, (cs i).last = c.last i) ∧
c.length ≤ ∑ i, (cs i).length from H c.length c rfl
intro m
induction m with
| zero =>
intro c hn
have hlast : (Fin.last c.length) = 0 := by ext; simp [hn]
have hhl : c.last = c.head := by rw [RelSeries.last, RelSeries.head, hlast]
refine ⟨fun i => RelSeries.singleton _ (c.head i), fun i => ?_, fun i => ?_, ?_⟩
· exact RelSeries.head_singleton _
· rw [RelSeries.last_singleton, hhl]
· simp [hn, RelSeries.singleton]
| succ m ih =>
intro c hn
have h0 : c.length ≠ 0 := by omega
haveI : NeZero c.length := ⟨h0⟩
obtain ⟨cs', hh', hl', hlen'⟩ := ih (c.tail h0) (by rw [RelSeries.tail_length]; omega)
have hstep : c.head < c 1 := c.strictMono Fin.one_pos'
obtain ⟨hle, j, hjlt⟩ := Pi.lt_def.mp hstep
have hh'1 : ∀ i, (cs' i).head = c 1 i := fun i => by rw [hh' i, RelSeries.head_tail]
refine ⟨fun i =>
if hlt : c.head i < c 1 i then
(cs' i).cons (c.head i) (by rw [hh'1 i]; exact hlt)
else cs' i,
fun i => ?_, fun i => ?_, ?_⟩
· by_cases hlt : c.head i < c 1 i
· simp only [dif_pos hlt, RelSeries.head_cons]
· simp only [dif_neg hlt]
rw [hh'1 i]
exact ((lt_or_eq_of_le (hle i)).resolve_left hlt).symm
· by_cases hlt : c.head i < c 1 i
· simp only [dif_pos hlt, RelSeries.last_cons, hl' i, RelSeries.last_tail]
· simp only [dif_neg hlt, hl' i, RelSeries.last_tail]
· calc c.length
= (c.tail h0).length + 1 := by rw [RelSeries.tail_length]; omega
_ ≤ (∑ i, (cs' i).length) + 1 := Nat.add_le_add_right hlen' 1
_ ≤ ∑ i, (if hlt : c.head i < c 1 i then
(cs' i).cons (c.head i) (by rw [hh'1 i]; exact hlt) else cs' i).length :=
Nat.succ_le_of_lt (Finset.sum_lt_sum (fun i _ => by
split
· rw [RelSeries.cons_length]; omega
· exact le_rfl)
⟨j, Finset.mem_univ j, by rw [dif_pos hjlt, RelSeries.cons_length]; omega⟩)
end Unzip
section FiniteHeight
variable [FiniteHeightLattice β]
instance instFiniteHeight {n : ℕ} : FiniteHeightLattice (Fin n → β) where
toLattice := inferInstance
toOrderBot := inferInstance
toOrderTop := inferInstance
height := n * FiniteHeightLattice.height (α := β)
chains_bounded := fun c => by
obtain ⟨cs, _, _, hbound⟩ := exists_unzip c
refine hbound.trans ?_
calc ∑ i, (cs i).length
≤ ∑ _i : Fin n, FiniteHeightLattice.height (α := β) :=
Finset.sum_le_sum (fun i _ => FiniteHeightLattice.chains_bounded (cs i))
_ = n * FiniteHeightLattice.height (α := β) := by
simp [Finset.sum_const, Finset.card_univ, Fintype.card_fin]
end FiniteHeight
end Tuple
end Spa

20
lean/Spa/Lattice/Unit.lean
View File

@@ -1,14 +1,18 @@
import Spa.Lattice
/-!
# Unit Lattice
This file provides a proof that in addition to being a lattice,
`PUnit` is a `Spa.FiniteHeightLattice`. This is a fairly trivial result. -/
namespace Spa
instance : FiniteHeightLattice PUnit := FiniteHeightLattice.ofUnique PUnit
theorem boundedChains_of_subsingleton (α : Type*) [Preorder α] [Subsingleton α]
(n : ℕ) : BoundedChains α n := fun c => by
by_contra hc
push_neg at hc
exact (c.step ⟨0, by omega⟩).ne (Subsingleton.elim _ _)
instance : FiniteHeightLattice PUnit where
bot := PUnit.unit
top := PUnit.unit
height := 0
longestChain := { series := RelSeries.singleton _ PUnit.unit, head_series := refl _, last_series := refl _, length_series := refl _ }
chains_bounded := boundedChains_of_subsingleton PUnit 0
end Spa

3
lean/Spa/Showable.lean
View File

@@ -30,8 +30,7 @@ instance {α : Type*} [Showable α] : Showable (AboveBelow α) :=
instance {α β : Type*} {ks : List α} [Showable α] [Showable β] :
Showable (FiniteMap α β ks) :=
⟨fun fm =>
"{" ++ (FiniteMap.toList fm).foldr
(fun p rest => show' p.1 ++ " ↦ " ++ show' p.2 ++ ", " ++ rest) ""
"{" ++ fm.val.foldr (fun p rest => show' p.1 ++ " ↦ " ++ show' p.2 ++ ", " ++ rest) ""
++ "}"⟩
end Spa

102
lean/Spa/Transformation/Licm.lean
View File

@@ -1,102 +0,0 @@
import Spa.Analysis.Reaching
import Spa.Language.Tagged.Graphs
/-!
# Finding loop-invariant assignments (LICM groundwork)
This wires the **reaching-definitions** analysis (`Spa/Analysis/Reaching.lean`)
to the **tagged AST** to *find* — not yet move — assignments inside a `while`
loop whose right-hand side depends only on definitions made *outside* the loop.
These are the candidates a later LICM pass could hoist.
The pipeline, for each assignment immediately enclosed by a loop:
1. locate its CFG state via the tagged-graph bridge (`Program.stateOfNodeId`);
2. read the reaching definitions at the assignment's *entry*
(`joinForKey s result` — the join over predecessors, i.e. before the
assignment itself runs);
3. union the definition sets of the RHS variables;
4. map each definition site back to its `RawId` (`Program.nodeIdOf`) and check
it is **not** inside the loop body (structural `subtreeIds` membership).
If every reaching definition of every RHS variable lies outside the loop, the
assignment is reported as loop-invariant. This is the first-order check ("all
reaching definitions outside the loop"); transitive/iterated invariance and the
actual hoisting are out of scope here.
-/
namespace Spa
namespace LicmTransformation
open Forward
/-- An assignment found inside a loop, paired with the data needed to test its
invariance against that (immediately enclosing) loop. -/
structure Candidate (prog : Program) where
/-- The enclosing `whileLoop`'s tag (for reporting). -/
loopId : prog.NodeId
/-- Every node id inside the loop body (the "is-child-of-loop" set). -/
bodyIds : List prog.NodeId
/-- The assignment `BasicStmt`'s tag — what labels its CFG node. -/
assignId : prog.NodeId
/-- The variables read by the assignment's RHS. -/
rhsVars : List String
/-- Collect every assignment together with its *immediately enclosing* loop.
`enclosing` carries the current loop's tag and body id-set, or `none` outside any
loop (in which case assignments are skipped — only in-loop assignments are
candidates). -/
def collectCandidates (prog : Program) (enc : Option (prog.NodeId × List prog.NodeId)) :
Stmt.Tagged prog.NodeId → List (Candidate prog)
| .basic _ bs =>
match bs, enc with
| .assign t _ e, some (loopId, bodyIds) =>
[{ loopId := loopId, bodyIds := bodyIds, assignId := t,
rhsVars := e.erase.vars.sort (· ≤ ·) }]
| _, _ => []
| .andThen _ a b => collectCandidates prog enc a ++ collectCandidates prog enc b
| .ifElse _ _ a b => collectCandidates prog enc a ++ collectCandidates prog enc b
| .whileLoop loopT _ body =>
collectCandidates prog (some (loopT, body.subtreeIds)) body
/-- Read the definition set assigned to variable `k`, or `⊥` if absent. -/
def lookupDef (prog : Program) (vs : VariableValues (DefSet prog) prog)
(k : String) : DefSet prog :=
if h : FiniteMap.MemKey k vs then (FiniteMap.locate h).1 else ⊥
/-- The AST node ids marked as definition sites in a `DefSet`. With the
`Finset`-of-AST-ids lattice these are just the elements of the set. -/
def defSites (prog : Program) (d : DefSet prog) : List prog.NodeId :=
(List.finRange prog.size).filter (fun i => decide (i ∈ d))
/-- Is the candidate assignment loop-invariant: do all reaching definitions of
its RHS variables lie outside the loop body? Reaching sets are now keyed by AST
node id, so we compare against the loop-body ids directly (embedding the raw
body ids into `p.NodeId`). -/
def isInvariant (prog : Program) (c : Candidate prog) : Bool :=
match prog.stateOfNodeId c.assignId with
| none => false
| some s =>
let entry := joinForKey s (result (DefSet prog) prog)
let combined : DefSet prog :=
c.rhsVars.foldl (fun acc k => acc ⊔ lookupDef prog entry k) ⊥
(defSites prog combined).all (fun nid => ! decide (nid ∈ c.bodyIds))
/-- The loop-invariant assignments of `prog`, as `(loopId, assignId)` pairs. -/
def licmCandidates (prog : Program) : List (prog.NodeId × prog.NodeId) :=
(collectCandidates prog none prog.taggedFin).filterMap (fun c =>
if isInvariant prog c then some (c.loopId, c.assignId) else none)
/-- A human-readable report of the loop-invariant assignments. -/
def output (prog : Program) : String :=
match licmCandidates prog with
| [] => "no loop-invariant assignments found"
| cands =>
"loop-invariant assignments (loop ↦ assignment):\n" ++
String.intercalate "\n"
(cands.map (fun p => s!" loop #{p.1.val}: assignment #{p.2.val}"))
end LicmTransformation
end Spa