54 Commits

Author SHA1 Message Date
904f6375be Consolidate per-operator trace lifting into GGraph.Embed + Trace.embed
Each graph-composition operator includes its operands via an index
translation preserving node payloads and edges. Capture that once as
GGraph.Embed (a structure, not a class: for g ; g both inclusions share
the type Embed g (g <~> g), so instance resolution could pick the wrong
copy) with five named witnesses, and replace the five structurally
identical trace-lifting inductions in Properties.lean with a single
generic Trace.embed plus one-line corollaries.

The same witnesses' nodes_eq fields will back the upcoming AST-id/CFG
label bijection, so the per-operator content is stated exactly once.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-02 15:06:40 -05:00
8cd053a242 Migrate Reaching.lean to projections via a generic Trace.steps
Finish the projection migration for reaching definitions by replacing the
accumulator-style runOfTrace*From definitions and their hand-rolled
re-association lemmas with a single analysis-agnostic projection:
Trace.steps / Traceₗ.steps, the chronological List of executed
(index, statement) pairs. Its four simp lemmas are one-line inductions,
with all re-association falling out of mathlib's List.append_assoc and
List.reverse_append.

Run is now an abbrev for List (State × BasicStmt) (latest-first, so
LastAssign keeps its first-match structure) and runOfTrace is just
steps.reverse.

Also hoist the generic reaches_final_post into Forward.lean, letting
analyze_correct' be stated directly about S.Post (prog.trace hrun).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-02 09:01:09 -05:00
0e6976f9b4 Migrate most of the codebase (sans Reaching.lean / LICM left) to projections 2026-07-01 22:56:29 -05:00
10b8fa97ca Add left-and-right open traces to help formalization
Co-Authored-By: OpenAI Codex <codex@openai.com>
2026-07-01 19:27:06 -05:00
8ed48cf444 Add non-state parameterized 'Reaches' relation 2026-07-01 13:02:39 -05:00
37d88f070a Remove 'prog.code s = some bs' argument to eval 2026-06-30 23:21:00 -05:00
6c05e401c1 Document Program.lean 2026-06-29 10:42:01 -05:00
fe5098095a Reorganize proofs to make 'Program' accessible to files in Language/ 2026-06-29 10:41:40 -05:00
59afbdaf71 Rename StateInterp to match the style of the rest of the codebase 2026-06-29 10:00:01 -05:00
490c472d22 Start documenting FiniteMap.lean 2026-06-29 08:59:51 -05:00
d1a11a9b2c Use alpha and beta for FiniteMap type variables 2026-06-29 08:59:37 -05:00
2598df690c Slightly tweak AboveBelow proofs 2026-06-29 08:16:55 -05:00
47d54f5b4b Further simplify proofs in AboveBelow
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-28 15:01:24 -05:00
8fa822b2e6 Improve performance by caching CFG building
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-28 14:39:14 -05:00
d66a7d0e3e Clean up and document AboveBelow 2026-06-28 14:38:12 -05:00
778e974dfb Prove that analysis results apply to all states, not just the final one
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-28 14:24:46 -05:00
319fa272ac Switch Reaching analysis to use Finset for more efficiency
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-28 09:46:54 -05:00
86bc33ee26 Register cases rules on lattice carriers for aesop automation
Tag the finite lattice carrier types with `@[aesop safe cases]`
(`AboveBelow`, `Sign`) so aesop performs the dominant proof step in this
framework -- case-splitting a lattice element -- automatically. Combined
with the existing `@[simp]` operation lemmas, this collapses the recurring
"case-split then reduce" proofs to a bare `aesop`:

  * AboveBelow's six lattice axioms drop their explicit `rcases`
  * Sign/Constant `plus_mono₂`/`minus_mono₂` become `by aesop`
  * Constant `plus_valid`/`minus_valid` shrink to a 2-line `rcases <;> simp_all`
  * `not_mk_lt_mk` is reexpressed via `le_cases`

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-27 20:01:01 -05:00
9e0702b5f5 Replace AboveBelow lattice-axiom case bashes with aesop
The six lattice axioms (sup/inf comm/assoc, absorption) all close with a
uniform `rcases <;> aesop`, removing the per-lemma simp-lemma lists that had
to be kept in sync with the Max/Min definitions.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-27 19:49:13 -05:00
445187837c Add Trace.concat notation and apply at call sites
Introduce `tr₁ ++< he >++ tr₂` scoped notation for `Trace.concat`
(precedence 65, right-associative, mirroring `++`) and use it
throughout Properties.lean.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-27 19:46:19 -05:00
1a49689edc Apply aesop to reduce proofs
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-27 19:30:01 -05:00
b1b3b0d2fe Add more documentation
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2026-06-27 19:20:23 -05:00
379438ec17 Add more documentation 2026-06-27 18:56:59 -05:00
1120e01605 Add some documentation 2026-06-27 18:56:59 -05:00
b6b30958aa Add proof of reaching definition analysis
This requires a few pieces:

* Make node tags use `Fin n` intead of natural numbers. This makes
  it possible to build a finite lattice over AST nodes, and also
  ensure automatic, total indexing from CFG nodes into the AST that
  created them. For this, use the elaborator to derive the ordering
  statements etc. where possible.
* Adjust the forward framework to enable proofs that don't just state
  correctness on the environment, but also on an arbitrary additional
  state accumulated from traversing the trace.
* State the reaching definition analysis's correctness in terms
  of this new framework.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-27 18:56:59 -05:00
5737805125 Remove maximal chain witness from FiniteHeightLattice
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-26 15:04:18 -05:00
e738eb4294 Usw OrderBot / OrderTop for lattice witnesses
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Co-Authored-By: OpenAI Codex <codex@openai.com>
2026-06-26 14:49:57 -05:00
6a6ed521ca Slightly tweak LICM implementation
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2026-06-26 12:16:04 -05:00
c38c10fe9e Add a sketch of loop invariant code motion
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-26 12:16:04 -05:00
c367f130cf Add tagging machinery to assign unique IDs to AST nodes
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-26 12:16:04 -05:00
a5f533d67a Use a direct N-way unzip instead of induction over product size
This makes a finite-height proof for any `Fin n -> a` lattice
immediate, and precludes the need for IterProd and Prod altogether.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-26 12:16:04 -05:00
c281d78d1d Add documentation for IterProd 2026-06-26 12:16:04 -05:00
1a843747bf Delete unused code and moved some lemmas into Lattice.lean
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-26 12:16:04 -05:00
352e0bb8cc Fold Isomorphism module into Lattice.lean
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2026-06-26 12:16:04 -05:00
a12b6c0c3c Write more documentation
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2026-06-25 19:36:26 -05:00
cbad43efdc Make FiniteHeightLattice extend Lattice and derive Top/Bot
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-25 18:55:09 -05:00
acef0f202b Add titles to documented modules
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2026-06-25 18:55:09 -05:00
c2ad0db668 Update comments in Graph and make map be a Functor instance
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2026-06-25 18:55:09 -05:00
a5235f6fbc Add documentation to some modules. 2026-06-25 18:55:09 -05:00
e2df847139 Adopt lemma as the default keyword
Convert every theorem to lemma (mathlib's default) except the headline results a
reader of each module seeks out: analyze_correct (Forward/Sign/Constant),
aFix_eq/aFix_le (Fixedpoint), trace (Language), and Stmt.cfg_sufficient
(Language/Properties). lemma and theorem are interchangeable keywords, so no
references change.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-25 14:08:10 -05:00
5c9c8ac55c Fix formatting nits in Lattice.lean and Unit.lean
- Spa/Lattice.lean: add the missing space in the PointedLTSeries binder list
  ((f t : α) (n : ℕ)).
- Spa/Lattice/Unit.lean: use rfl instead of refl _, and split the ~200-column
  longestChain record literal across lines, one field per line.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-25 14:06:50 -05:00
ec2e789d5c Spell out evalB as evalBasicStmt
Replace the ad-hoc truncation `evalB`/`evalB_mono` in
Spa/Analysis/Forward/Adapters.lean with `evalBasicStmt`/`evalBasicStmt_mono`.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-25 14:06:38 -05:00
a3ecefd415 Rename IterProd instances off the inst* prefix
The `inst*` prefix is reserved for compiler-generated instance names; writing it
by hand is non-idiomatic. Rename the recursive instances in Spa/Lattice/IterProd.lean
to descriptive lowerCamelCase matching the file's `def fixedHeight`:
instLattice -> lattice, instDecidableEq -> decidableEq, instFiniteHeight -> finiteHeight.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-25 14:05:59 -05:00
5ac881559d Switch FiniteMap Fin n -> L representation
This helps automatically derive lattice laws for it

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-25 14:05:59 -05:00
c4e5747b6d Turn buildCfg into a method
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2026-06-25 09:49:44 -05:00
341a0b80b4 Add computation lemmas on GGraphs + map to Graphs.lean
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-25 09:26:15 -05:00
4506f7c242 Delete dead code from Base.lean
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2026-06-25 09:12:11 -05:00
94278a6389 Add computational reaching-definitions analysis
Introduce a finite-height lattice instance for Bool, then build the
reaching-definitions analysis on top of the forward framework:

* Spa/Lattice/Bool.lean: FiniteHeightLattice Bool (the two-element
  lattice false ≤ true), making FiniteMap A Bool ks a finite-height
  "power set" lattice for free.
* Spa/Analysis/Reaching.lean: DefSet prog = FiniteMap prog.State Bool
  prog.states as the per-variable lattice of definition sites, with a
  StmtEvaluator whose transfer function performs a strong update
  (assignment to k at node s sets k's def-set to {s}).

The analysis computes a least fixed point and produces correct
reaching-definitions sets. Soundness (relating def-sets to actual
execution provenance) is deferred; not yet exposed in Spa.lean.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-25 09:12:11 -05:00
a721a8be8b Generalize graphs over their node content
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-24 16:03:34 -05:00
9ab43b34ef Use mathlib definition of inverses for Isomorphism.lean
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2026-06-24 14:32:50 -05:00
97a9150bf3 Simplify the strict-step extraction in LTSeries.exists_unzip
Derive c.head < c 1 from the series' StrictMono instance and Fin.one_pos'
instead of unfolding c.step with manual Fin.succ index arithmetic.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-24 14:23:13 -05:00
93f913a699 Clean up namespaces in the analysis framework
- Wrap the forward-analysis framework in a Spa.Forward namespace so its
  generic names (analyze, result, joinAll, variablesAt, ...) no longer
  sit flat in Spa, matching the ConstAnalysis/SignAnalysis convention.
- Merge the split Graph namespace in Graphs.lean by relocating buildCfg.
- Use nested namespace Spa / Fixedpoint instead of Spa.Fixedpoint.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-24 13:56:16 -05:00
7fb9d9aa19 Clean up Lattice.lean's namespaces
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2026-06-24 13:56:16 -05:00
f23705a93e 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>
2026-06-23 15:11:34 -05:00
39 changed files with 3111 additions and 1339 deletions

View File

@@ -1,31 +1,37 @@
import Spa.Analysis.Sign
import Spa.Analysis.Constant
import Spa.Analysis.Reaching
import Spa.Language.Notation
namespace Spa
def testCode : Stmt :=
.andThen (.basic (.assign "zero" (.num 0)))
(.andThen (.basic (.assign "pos" (.add (.var "zero") (.num 1))))
(.andThen (.basic (.assign "neg" (.sub (.var "zero") (.num 1))))
(.basic (.assign "unknown" (.add (.var "pos") (.var "neg"))))))
def testCode : Stmt := [obj_stmt|
zero := 0;
pos := zero + 1;
neg := zero - 1;
unknown := pos + neg
]
def testCodeCond₁ : Stmt :=
.andThen (.basic (.assign "var" (.num 1)))
(.ifElse (.var "var")
(.basic (.assign "var" (.add (.var "var") (.num 1))))
(.andThen (.basic (.assign "var" (.sub (.var "var") (.num 1))))
(.basic (.assign "var" (.num 1)))))
def testCodeCond₁ : Stmt := [obj_stmt|
var := 1;
if var {
var := var + 1
} else {
var := var - 1;
var := 1
}
]
def testCodeCond₂ : Stmt :=
.andThen (.basic (.assign "var" (.num 1)))
(.ifElse (.var "var")
(.basic (.assign "x" (.num 1)))
(.basic .noop))
def testCodeCond₂ : Stmt := [obj_stmt|
var := 1;
if var { x := 1 } else { noop }
]
def testProgram : Program := testCode
def testProgram : Program := { rootStmt := testCode }
end Spa
def main : IO Unit :=
IO.println (Spa.ConstAnalysis.output Spa.testProgram ++ "\n" ++
Spa.SignAnalysis.output Spa.testProgram)
Spa.SignAnalysis.output Spa.testProgram ++ "\n" ++
Spa.ReachingAnalysis.output Spa.testProgram)

View File

@@ -1,12 +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
import Spa.Language.Graphs
import Spa.Language.Traces
@@ -20,3 +19,10 @@ 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

View File

@@ -5,6 +5,8 @@ import Spa.Showable
namespace Spa
open Forward
abbrev ConstLattice : Type := AboveBelow
namespace ConstAnalysis
@@ -25,24 +27,22 @@ def minus : ConstLattice → ConstLattice → ConstLattice
| _, top => top
| mk z₁, mk z₂ => mk (z₁ - z₂)
theorem plus_mono₂ : Monotone₂ plus :=
lemma plus_mono₂ : Monotone₂ plus :=
AboveBelow.monotone₂_of_strict plus
(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)
(fun y => by aesop) (fun x => by aesop)
(fun y hy => by aesop) (fun x hx => by aesop)
theorem minus_mono₂ : Monotone₂ minus :=
lemma minus_mono₂ : Monotone₂ minus :=
AboveBelow.monotone₂_of_strict minus
(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)
(fun y => by aesop) (fun x => by aesop)
(fun y hy => by aesop) (fun x hx => by aesop)
def interpConst : ConstLattice Value Prop
| .bot, _ => False
| .top, _ => True
| .mk z, v => v = .int z
theorem interpConst_mk_disjoint {z₁ z₂ : } (hne : z₁ z₂) {v : Value} :
lemma 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
theorem eval_mono (e : Expr) : Monotone (eval prog e) := by
lemma 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 @@ theorem 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,39 +91,17 @@ instance exprEvaluator : ExprEvaluator ConstLattice prog :=
def output : String :=
show' (result ConstLattice prog)
theorem plus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : }
lemma 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₁
· 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₂]
rcases g₁ with _ | _ | c₁ <;> rcases g₂ with _ | _ | c₂ <;>
simp_all [plus, constInterpretation, interpConst]
theorem minus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : }
lemma 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₁
· 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₂]
rcases g₁ with _ | _ | c₁ <;> rcases g₂ with _ | _ | c₂ <;>
simp_all [minus, constInterpretation, interpConst]
instance eval_valid : ValidExprEvaluator ConstLattice prog := by
constructor
@@ -157,7 +135,14 @@ instance eval_valid : ValidExprEvaluator ConstLattice prog := by
theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
variablesAt prog.finalState (result ConstLattice prog) ρ :=
Spa.analyze_correct ConstLattice prog hrun
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
end ConstAnalysis

View File

@@ -5,38 +5,37 @@ import Spa.Fixedpoint
namespace Spa
variable {L : Type} [Lattice L] {prog : Program} [E : StmtEvaluator L prog]
namespace Forward
variable {L : Type} [FiniteHeightLattice L] {prog : Program} [E : StmtEvaluator L prog]
def updateVariablesForState (s : prog.State) (sv : StateVariables L prog) :
VariableValues L prog :=
(prog.code s).foldl (fun vs bs => E.eval s bs vs) (variablesAt s sv)
VariableValues L prog := E.eval s (variablesAt s sv)
theorem updateVariablesForState_mono (s : prog.State) :
lemma updateVariablesForState_mono (s : prog.State) :
Monotone (updateVariablesForState (L := L) s) := fun _ _ hle =>
foldl_mono' (prog.code s) _ (E.eval_mono s ·) (variablesAt_le hle 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
theorem updateAll_mono : Monotone (updateAll (L := L) (prog := prog)) :=
lemma updateAll_mono : Monotone (updateAll (L := L) (prog := prog)) :=
FiniteMap.generalizedUpdate_monotone monotone_id updateVariablesForState_mono
theorem updateAll_mem_eq {s : prog.State} {vs : VariableValues L prog}
lemma 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
theorem variablesAt_updateAll (s : prog.State) (sv : StateVariables L prog) :
lemma 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)
theorem analyze_mono : Monotone (analyze (L := L) (prog := prog)) := fun _ _ hle =>
lemma analyze_mono : Monotone (analyze (L := L) (prog := prog)) := fun _ _ hle =>
updateAll_mono (joinAll_mono hle)
variable [DecidableEq L]
@@ -46,74 +45,130 @@ def result : StateVariables L prog :=
Fixedpoint.aFix analyze analyze_mono
variable (L prog) in
theorem result_eq : result L prog = analyze (result L prog) :=
lemma result_eq : result L prog = analyze (result L prog) :=
Fixedpoint.aFix_eq analyze analyze_mono
theorem joinForKey_initialState :
lemma joinForKey_initialState :
joinForKey prog.initialState (result L prog) = botV L prog := by
rw [joinForKey, prog.incoming_initialState_eq_nil]
rfl
variable [I : LatticeInterpretation L] [V : ValidStmtEvaluator L prog]
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 []))
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)
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 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
section
variable [S : StateInterpretation L prog] [V : ValidStateEvaluator L prog]
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
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
rw [variablesAt_updateAll]
exact updateVariablesForState_matches hbss hvs
exact V.valid s₁ s₂ tr hnode hvs
theorem stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env}
(hjoin : joinForKey s₁ (result L prog) ρ)
(hbss : EvalBasicStmts ρ₁ (prog.code s₁) ρ₂) :
variablesAt s₁ (result L prog) ρ₂ := by
lemma stepTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
(tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ)
(hjoin : joinForKey s₂ (result L prog) (S.Pre tr))
(hnode : EvalBasicStmtOpt ρ₂ (prog.code s₂) ρ₃) :
variablesAt s₂ (result L prog) (S.Post (tr ++ hnode)) := by
rw [result_eq L prog]
refine updateAll_matches hbss ?_
refine updateAll_matches tr hnode ?_
rw [variablesAt_joinAll]
exact hjoin
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 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)
/-- 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 V in
theorem interp_joinForKey_initialState :
joinForKey prog.initialState (result L prog) [] := by
rw [joinForKey_initialState]
exact interp_botV_nil
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
induction tr with
| single hnode => rfl
| edge hnode hedge rest ih => simp [reaches_final, Reaches.post, ih]
variable (L prog) in
theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
/-- 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 _ _ []) ?_
rw [joinForKey_initialState]
exact ValidStateEvaluator.botV_init
variable (L prog) in
theorem analyze_correct'
{ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
variablesAt prog.finalState (result L prog) (S.Post (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 ρ) :
variablesAt prog.finalState (result L prog) ρ :=
walkTrace interp_joinForKey_initialState (prog.trace hrun)
analyze_correct' L prog hrun
end Forward
end Spa

View File

@@ -2,53 +2,63 @@ 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
theorem updateVariablesFromExpression_mono (k : String) (e : Expr) :
lemma 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 evalB (_ : prog.State) (bs : BasicStmt)
def evalBasicStmt (bs : BasicStmt)
(vs : VariableValues L prog) : VariableValues L prog :=
match bs with
| .assign k e => updateVariablesFromExpression k e vs
| .noop => vs
theorem evalB_mono (s : prog.State) (bs : BasicStmt) :
Monotone (evalB (L := L) (prog := prog) s bs) := by
lemma evalBasicStmt_mono (bs : BasicStmt) :
Monotone (evalBasicStmt (L := L) (prog := prog) 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 :=
evalB, evalB_mono
evalBasicStmtOpt prog.code,
by intro s; simp; exact (evalBasicStmtOpt_mono (prog.code s))
instance ExprEvaluator.toStmtEvaluator_valid [LatticeInterpretation L]
[ValidExprEvaluator L prog] : ValidStmtEvaluator L prog := by
constructor
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
| 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'
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
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
end Spa

View File

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

View File

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

View File

@@ -0,0 +1,135 @@
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

View File

@@ -5,12 +5,16 @@ 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 => "+"
@@ -53,23 +57,15 @@ def minus : SignLattice → SignLattice → SignLattice
| mk .zero, mk .minus => mk .plus
| mk .zero, mk .zero => mk .zero
theorem plus_mono₂ : Monotone₂ plus :=
lemma plus_mono₂ : Monotone₂ plus :=
AboveBelow.monotone₂_of_strict plus
(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))
(fun y => by aesop) (fun x => by aesop)
(fun y hy => by aesop) (fun x hx => by aesop)
theorem minus_mono₂ : Monotone₂ minus :=
lemma minus_mono₂ : Monotone₂ minus :=
AboveBelow.monotone₂_of_strict minus
(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))
(fun y => by aesop) (fun x => by aesop)
(fun y hy => by aesop) (fun x hx => by aesop)
def interpSign : SignLattice Value Prop
| .bot, _ => False
@@ -78,7 +74,7 @@ def interpSign : SignLattice → Value → Prop
| .mk .zero, v => v = .int 0
| .mk .minus, v => n : , v = .int (-(n + 1))
theorem interpSign_mk_disjoint {s₁ s₂ : Sign} (hne : s₁ s₂) {v : Value} :
lemma 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
@@ -123,7 +119,7 @@ def eval : Expr → VariableValues SignLattice prog → SignLattice
| .num 0, _ => .mk .zero
| .num (_ + 1), _ => .mk .plus
theorem eval_mono (e : Expr) : Monotone (eval prog e) := by
lemma eval_mono (e : Expr) : Monotone (eval prog e) := by
induction e with
| add e₁ e₂ ih₁ ih₂ =>
intro vs₁ vs₂ h
@@ -135,12 +131,12 @@ theorem 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 _
@@ -152,18 +148,18 @@ def output : String :=
show' (result SignLattice prog)
/-- A nonneg-shifted interpretation `∃ n : , z = n + 1` just means `z` is positive. -/
private theorem int_pos_iff (z : ) : ( n : , z = (n : ) + 1) 0 < z := by
private lemma 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 theorem int_neg_iff (z : ) : ( n : , z = -((n : ) + 1)) z < 0 := by
private lemma int_neg_iff (z : ) : ( n : , z = -((n : ) + 1)) z < 0 := by
constructor
· rintro n, rfl; omega
· intro h; exact (-z - 1).toNat, by omega
theorem plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : }
lemma 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₂ <;>
@@ -172,7 +168,7 @@ theorem plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : }
at h₁ h₂ <;>
omega
theorem minus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : }
lemma 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₂ <;>
@@ -215,7 +211,14 @@ instance eval_valid : ValidExprEvaluator SignLattice prog := by
theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
variablesAt prog.finalState (result SignLattice prog) ρ :=
Spa.analyze_correct SignLattice prog hrun
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
end SignAnalysis

View File

@@ -2,7 +2,7 @@ import Spa.Lattice
namespace Spa
theorem eval_combine₂ {O : Type*} [Preorder O] {combine : O O O}
lemma 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₂)

View File

@@ -1,10 +1,12 @@
import Spa.Lattice
namespace Spa.Fixedpoint
namespace Spa
namespace Fixedpoint
open FiniteHeightLattice (height)
variable {α : Type*} [Lattice α] [DecidableEq α] [FiniteHeightLattice α]
variable {α : Type*} [DecidableEq α] [FiniteHeightLattice α]
def doStep (f : α α) (hf : Monotone f) :
(g : ) (c : LTSeries α), c.length + g = height (α := α) + 1
@@ -22,8 +24,7 @@ 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 simpa [RelSeries.last_singleton]
using FiniteHeightLattice.bot_le α (f ))
(by simp)
def aFix (f : α α) (hf : Monotone f) : α :=
(fix f hf).1
@@ -32,12 +33,13 @@ theorem aFix_eq (f : αα) (hf : Monotone f) :
aFix f hf = f (aFix f hf) :=
(fix f hf).2
theorem doStep_le (f : α α) (hf : Monotone f)
lemma 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
@@ -47,6 +49,8 @@ theorem 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 simpa using FiniteHeightLattice.bot_le α a)
doStep_le f hf ha _ _ _ _ (by simp)
end Spa.Fixedpoint
end Fixedpoint
end Spa

View File

@@ -1,7 +1,17 @@
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

View File

@@ -1,24 +0,0 @@
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

View File

@@ -3,56 +3,4 @@ import Spa.Language.Semantics
import Spa.Language.Graphs
import Spa.Language.Traces
import Spa.Language.Properties
import Mathlib.Data.Finset.Sort
import Mathlib.Data.String.Basic
namespace Spa
structure Program where
rootStmt : Stmt
namespace Program
variable (p : Program)
def 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
import Spa.Language.Program

View File

@@ -1,7 +1,19 @@
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)
@@ -9,11 +21,15 @@ 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)
@@ -21,34 +37,23 @@ inductive Stmt where
| whileLoop (e : Expr) (s : Stmt)
deriving DecidableEq
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)
/-- Variables mentioned in this expression. -/
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

View File

@@ -3,45 +3,113 @@ 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
structure Graph where
/-- 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
size :
nodes : Fin size List BasicStmt
nodes : Fin size α
edges : List (Fin size × Fin size)
inputs : List (Fin size)
outputs : List (Fin size)
namespace Graph
namespace GGraph
abbrev Index (g : Graph) : Type := Fin g.size
variable {α β : Type}
abbrev Edge (g : Graph) : Type := g.Index × g.Index
/-- An index (node) in the CFG. -/
abbrev Index (g : GGraph α) : Type := Fin g.size
def comp (g₁ g₂ : Graph) : Graph where
/-- 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
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 "" => Graph.comp
@[inherit_doc] scoped infixr:70 "" => GGraph.overlay
def link (g₁ g₂ : Graph) : Graph where
/-- 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
size := g₁.size + g₂.size
nodes := Fin.append g₁.nodes g₂.nodes
edges := g₁.edges.finCastAddProd g₂.size ++ g₂.edges.finNatAddProd g₁.size ++
@@ -49,78 +117,244 @@ def link (g₁ g₂ : Graph) : Graph where
inputs := g₁.inputs.finCastAdd g₂.size
outputs := g₂.outputs.finNatAdd g₁.size
@[inherit_doc] scoped infixr:70 "" => Graph.link
@[inherit_doc] scoped infixr:70 "" => GGraph.sequence
/-- 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 input of the new loop. -/
def loopIn (g : GGraph α) : Fin (2 + g.size) := (0 : 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
/-- 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
def loop (g : Graph) : Graph where
/-- 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
size := 2 + g.size
nodes := Fin.append (fun _ : Fin 2 => []) g.nodes
nodes := Fin.append (fun _ : Fin 2 => none) g.nodes
edges := g.edges.finNatAddProd 2 ++
(g.inputs.finNatAdd 2).map (g.loopIn, ·) ++
(g.outputs.finNatAdd 2).map (·, g.loopOut) ++
((g.loopIn, ·) <$> g.inputs.finNatAdd 2) ++
((·, g.loopOut) <$> g.outputs.finNatAdd 2) ++
[(g.loopOut, g.loopIn), (g.loopIn, g.loopOut)]
inputs := [g.loopIn]
outputs := [g.loopOut]
@[simp] theorem loop_inputs (g : Graph) : (loop g).inputs = [g.loopIn] := rfl
@[simp] lemma loop_inputs (g : GGraph (Option β)) : (loop g).inputs = [g.loopIn] := rfl
@[simp] theorem loop_outputs (g : Graph) : (loop g).outputs = [g.loopOut] := rfl
@[simp] lemma loop_outputs (g : GGraph (Option β)) : (loop g).outputs = [g.loopOut] := rfl
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
/-- Creates a single-node graph whose node contains the given value. -/
def singleton (a : α) : GGraph α where
size := 1
nodes := fun _ => bss
nodes := fun _ => a
edges := []
inputs := [0]
outputs := [0]
def wrap (g : Graph) : Graph :=
singleton [] g singleton []
/-- 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
end Graph
open Graph in
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
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
end Spa

View File

@@ -0,0 +1,60 @@
import Spa.Language.Base
namespace Spa
/-!
Scoped quotation syntax for writing object-language programs.
`[obj_expr| … ]` builds an `Expr`, `[obj_stmt| … ]` builds a `Stmt`.
Example:
```
[obj_stmt|
zero := 0;
pos := zero + 1;
if pos { x := 1 } else { noop };
while x { x := x - 1 }
]
```
-/
/-- Expressions of the object language. -/
declare_syntax_cat obj_expr
syntax num : obj_expr
syntax ident : obj_expr
syntax:65 obj_expr:65 " + " obj_expr:66 : obj_expr
syntax:65 obj_expr:65 " - " obj_expr:66 : obj_expr
syntax "(" obj_expr ")" : obj_expr
/-- Statements of the object language. -/
declare_syntax_cat obj_stmt
syntax "noop" : obj_stmt
syntax ident " := " obj_expr : obj_stmt
syntax "if " obj_expr " { " obj_stmt " } " "else" " { " obj_stmt " } " : obj_stmt
syntax "while " obj_expr " { " obj_stmt " } " : obj_stmt
syntax:50 obj_stmt:51 "; " obj_stmt:50 : obj_stmt
syntax "(" obj_stmt ")" : obj_stmt
scoped syntax "[obj_expr| " obj_expr " ]" : term
scoped syntax "[obj_stmt| " obj_stmt " ]" : term
scoped macro_rules
| `([obj_expr| $n:num]) => `(Expr.num $n)
| `([obj_expr| $x:ident]) => `(Expr.var $(Lean.quote x.getId.toString))
| `([obj_expr| $a + $b]) => `(Expr.add [obj_expr| $a] [obj_expr| $b])
| `([obj_expr| $a - $b]) => `(Expr.sub [obj_expr| $a] [obj_expr| $b])
| `([obj_expr| ($e:obj_expr)]) => `([obj_expr| $e])
scoped macro_rules
| `([obj_stmt| noop]) => `(Stmt.basic .noop)
| `([obj_stmt| $x:ident := $e]) =>
`(Stmt.basic (.assign $(Lean.quote x.getId.toString) [obj_expr| $e]))
| `([obj_stmt| $s₁ ; $s₂]) => `(Stmt.andThen [obj_stmt| $s₁] [obj_stmt| $s₂])
| `([obj_stmt| if $e { $s₁ } else { $s₂ }]) =>
`(Stmt.ifElse [obj_expr| $e] [obj_stmt| $s₁] [obj_stmt| $s₂])
| `([obj_stmt| while $e { $s }]) => `(Stmt.whileLoop [obj_expr| $e] [obj_stmt| $s])
| `([obj_stmt| ($s:obj_stmt)]) => `([obj_stmt| $s])
end Spa

View File

@@ -0,0 +1,77 @@
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

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}
theorem Trace.comp_left {idx₁ idx₂ : g₁.Index}
/-- 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
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
/-- 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) ρ₁ ρ₂ := 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_map_of_mem _ he)
Trace (g₁ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ :=
tr.embed (GGraph.Embed.overlayLeft g₁ g₂)
theorem Trace.comp_right {idx₁ idx₂ : g₂.Index}
/-- 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}
(tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) :
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)
Trace (g₁ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ :=
tr.embed (GGraph.Embed.overlayRight g₁ g₂)
theorem Trace.link_left {idx₁ idx₂ : g₁.Index}
/-- 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}
(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 [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))
Trace (g₁ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ :=
tr.embed (GGraph.Embed.sequenceLeft g₁ g₂)
theorem Trace.link_right {idx₁ idx₂ : g₂.Index}
/-- 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}
(tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) :
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))
Trace (g₁ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ :=
tr.embed (GGraph.Embed.sequenceRight g₁ g₂)
theorem EndToEndTrace.comp_left (etr : EndToEndTrace g₁ ρ₁ ρ₂) :
/-- Equivalent of `Trace.overlay_left` for end-to-end traces. -/
noncomputable def EndToEndTrace.overlay_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.comp_left
tr.overlay_left
theorem EndToEndTrace.comp_right (etr : EndToEndTrace g₂ ρ₁ ρ₂) :
/-- Equivalent of `Trace.overlay_right` for end-to-end traces. -/
noncomputable def EndToEndTrace.overlay_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.comp_right
tr.overlay_right
theorem EndToEndTrace.concat {ρ₃ : Env} (etr₁ : EndToEndTrace g₁ ρ₁ ρ₂)
/-- 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₁ ρ₁ ρ₂)
(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₂,
Trace.concat tr₁.link_left ?_ tr₂.link_right
tr₁.sequence_left ++< ?_ >++ tr₂.sequence_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}
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)))
/-- 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)
private theorem loop_nodes_at_in :
(Graph.loop g).nodes g.loopIn = [] :=
Fin.append_left (fun _ : Fin 2 => []) g.nodes 0
/-- 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_out :
(Graph.loop g).nodes g.loopOut = [] :=
Fin.append_left (fun _ : Fin 2 => []) g.nodes 1
/-- 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
theorem EndToEndTrace.loop (etr : EndToEndTrace g ρ₁ ρ₂) :
/-- Equivlaent of `Trace.loop` for end-to-end traces. -/
noncomputable def 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,15 +132,17 @@ theorem 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.concat (Trace.single (loop_nodes_at_in EvalBasicStmts.nil)) hin
(Trace.concat tr.loop hout (Trace.single (loop_nodes_at_out EvalBasicStmts.nil)))
exact Trace.single (loop_nodes_at_in EvalBasicStmtOpt.none) ++< hin >++
tr.loop ++< hout >++ Trace.single (loop_nodes_at_out EvalBasicStmtOpt.none)
private theorem loop_edge_out_in :
/-- 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 :
((g.loopOut, g.loopIn) : (Graph.loop g).Edge) (Graph.loop g).edges := by
refine List.mem_append_right _ ?_
exact List.mem_cons_self _ _
theorem EndToEndTrace.loop_concat (etr₁ : EndToEndTrace (Graph.loop g) ρ₁ ρ₂)
/-- 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) ρ₁ ρ₂)
(etr₂ : EndToEndTrace (Graph.loop g) ρ₂ ρ₃) :
EndToEndTrace (Graph.loop g) ρ₁ ρ₃ := by
obtain i₁, h₁, i₂, h₂, tr₁ := etr₁
@@ -148,86 +150,77 @@ theorem EndToEndTrace.loop_concat (etr₁ : EndToEndTrace (Graph.loop g) ρ₁
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 _,
Trace.concat tr₁ loop_edge_out_in tr₂
tr₁ ++< loop_edge_out_in >++ tr₂
theorem EndToEndTrace.loop_empty {ρ : Env} : EndToEndTrace (Graph.loop g) ρ ρ := by
/-- A loop can be executed zero times. -/
noncomputable def 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.concat (Trace.single (loop_nodes_at_in EvalBasicStmts.nil)) hedge
(Trace.single (loop_nodes_at_out EvalBasicStmts.nil))
Trace.single (loop_nodes_at_in EvalBasicStmtOpt.none) ++< hedge >++
Trace.single (loop_nodes_at_out EvalBasicStmtOpt.none)
end Loop
/-! ### Singletons, wrap, and the main result -/
theorem EndToEndTrace.singleton {bss : List BasicStmt} {ρ₁ ρ₂ : Env}
(h : EvalBasicStmts ρ₁ bss ρ₂) : EndToEndTrace (Graph.singleton bss) ρ₁ ρ₂ :=
/-- A CFG consisting of only a single node has a trace through it corresponding to that node. -/
noncomputable def EndToEndTrace.singleton {o : Option BasicStmt} {ρ₁ ρ₂ : Env}
(h : EvalBasicStmtOpt ρ₁ o ρ₂) : EndToEndTrace (Graph.singleton o) ρ₁ ρ₂ :=
(0 : Fin 1), List.mem_singleton_self _, (0 : Fin 1), List.mem_singleton_self _,
Trace.single h
theorem EndToEndTrace.singleton_nil (ρ : Env) :
EndToEndTrace (Graph.singleton []) ρ ρ :=
EndToEndTrace.singleton EvalBasicStmts.nil
/-- 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.wrap {g : Graph} {ρ₁ ρ₂ : Env}
/-- Invoking 'Graph.wrap` (which ensures a single entry and exit node for a CFG)
does not invalidate traces in the original graph. -/
noncomputable def EndToEndTrace.wrap {g : Graph} {ρ₁ ρ₂ : Env}
(etr : EndToEndTrace g ρ₁ ρ₂) : EndToEndTrace (Graph.wrap g) ρ₁ ρ₂ :=
(EndToEndTrace.singleton_nil ρ₁).concat (etr.concat (EndToEndTrace.singleton_nil ρ₂))
theorem buildCfg_sufficient {s : Stmt} {ρ₁ ρ₂ : Env}
(h : EvalStmt ρ₁ s ρ₂) : EndToEndTrace (buildCfg s) ρ₁ ρ₂ := by
/-- Key result: the control flow graph admits every execution that's made
possible by a language's semantics. Thus, the CFG encodes _at least_ all
semantically-possible executions. Informally, we can conclude from this
that if we compute a result that using the graph's edges to determine
what's possible, this result will not disagree with the semantics.
Note that a CFG like $K_4$ (where the nodes are basic blocks) is
technically also a sufficient graph, but is very likely meaningless in that
it grossly overestimates the possible execution paths in the language, and
thus is bound to produce less-than-specific results. There is as yet no
result in this framework that the CFG we produce is _minimal_: loosely,
posessing only edges for things that are admitted by the semantics.
This is difficult to state (in its strongest form, this would
require the CFG to be able to detect something like `while (alwaysFalse)`,
and so remains a TODO. -/
noncomputable def Stmt.cfg_sufficient {s : Stmt} {ρ₁ ρ₂ : Env}
(h : EvalStmt ρ₁ s ρ₂) : EndToEndTrace s.cfg ρ₁ ρ₂ := by
induction h with
| basic ρ₁ ρ₂ bs hbs =>
exact EndToEndTrace.singleton (EvalBasicStmts.cons hbs EvalBasicStmts.nil)
exact EndToEndTrace.singleton (EvalBasicStmtOpt.some hbs)
| andThen ρ₁ ρ₂ ρ₃ s₁ s₂ _ _ ih₁ ih₂ =>
exact ih₁.concat ih₂
| ifTrue ρ₁ ρ₂ e z s₁ s₂ _ _ _ ih =>
exact ih.comp_left
exact ih.overlay_left
| ifFalse ρ₁ ρ₂ e s₁ s₂ _ _ ih =>
exact ih.comp_right
exact ih.overlay_right
| whileTrue ρ₁ ρ₂ ρ₃ e z s _ _ _ _ ih₁ ih₂ =>
exact (ih₁.loop).loop_concat ih₂
| whileFalse ρ e s _ =>
exact EndToEndTrace.loop_empty
/-! ### The wrapped graph's entry has no predecessors (Agda's "ugly" block) -/
namespace Program
def Graph.wrapInput (g : Graph) : (Graph.wrap g).Index :=
(0 : Fin 1).castAdd ((g Graph.singleton []).size)
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.wrapOutput (g : Graph) : (Graph.wrap g).Index :=
Fin.natAdd 1 ((Fin.natAdd g.size (0 : Fin 1)))
end Program
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

View File

@@ -2,12 +2,27 @@ 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
@@ -15,6 +30,8 @@ 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) :
@@ -26,18 +43,25 @@ inductive EvalExpr : Env → Expr → Value → Prop
EvalExpr ρ e₁ (.int z₁) EvalExpr ρ e₂ (.int z₂)
EvalExpr ρ (.sub e₁ e₂) (.int (z₁ - z₂))
inductive EvalBasicStmt : Env BasicStmt Env Prop
/-- 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
| noop (ρ : Env) : EvalBasicStmt ρ .noop ρ
| assign (ρ : Env) (x : String) (e : Expr) (v : Value) :
EvalExpr ρ e v EvalBasicStmt ρ (.assign x e) ((x, v) :: ρ)
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 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 EvalStmt : Env Stmt Env Prop
/-- 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
| basic (ρ₁ ρ₂ : Env) (bs : BasicStmt) :
EvalBasicStmt ρ₁ bs ρ₂ EvalStmt ρ₁ (.basic bs) ρ₂
| andThen (ρ₁ ρ₂ ρ₃ : Env) (s₁ s₂ : Stmt) :
@@ -57,6 +81,15 @@ inductive EvalStmt : Env → Stmt → Env → Prop
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

View File

@@ -0,0 +1,18 @@
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

View File

@@ -0,0 +1,417 @@
# 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
```

View File

@@ -0,0 +1,509 @@
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

View File

@@ -0,0 +1,104 @@
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

View File

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

View File

@@ -0,0 +1,29 @@
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

View File

@@ -0,0 +1,46 @@
# 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`.

View File

@@ -1,26 +1,266 @@
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
inductive Trace (g : Graph) : g.Index g.Index Env Env Prop
/-- 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
| single {ρ₁ ρ₂ : Env} {idx : g.Index} :
EvalBasicStmts ρ₁ (g.nodes idx) ρ₂ Trace g idx idx ρ₁ ρ₂
EvalBasicStmtOpt ρ₁ (g.nodes idx) ρ₂ Trace g idx idx ρ₁ ρ₂
| edge {ρ₁ ρ₂ ρ₃ : Env} {idx₁ idx₂ idx₃ : g.Index} :
EvalBasicStmts ρ₁ (g.nodes idx₁) ρ₂ (idx₁, idx₂) g.edges
EvalBasicStmtOpt ρ₁ (g.nodes idx₁) ρ₂ (idx₁, idx₂) g.edges
Trace g idx₂ idx₃ ρ₂ ρ₃ Trace g idx₁ idx₃ ρ₁ ρ₃
theorem Trace.concat {g : Graph} {idx₁ idx₂ idx₃ idx₄ : g.Index}
/-!
## 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}
{ρ₁ ρ₂ ρ₃ : Env} (tr₁ : Trace g idx₁ idx₂ ρ₁ ρ₂)
(he : (idx₂, idx₃) g.edges) (tr₂ : Trace g idx₃ idx₄ ρ₂ ρ₃) :
Trace g idx₁ idx₄ ρ₁ ρ₃ := by
induction tr₁ with
| single hbs => exact Trace.edge hbs he tr₂
| edge hbs he' _ ih => exact Trace.edge hbs he' (ih he tr₂)
Trace g idx₁ idx₄ ρ₁ ρ₃ :=
match tr₁ with
| single hbs => edge hbs he tr₂
| edge hbs he' tr₁' => edge hbs he' (tr₁'.concat he tr₂)
inductive EndToEndTrace (g : Graph) (ρ₁ ρ₂ : Env) : Prop
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
| 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

View File

@@ -1,8 +1,32 @@
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 ·))
@@ -11,18 +35,20 @@ section Folds
variable {α β : Type*} [Preorder α] [Preorder β]
theorem foldr_mono {l₁ l₂ : List α} (f : α β β) {b₁ b₂ : β}
/-- (right) folds are monotonic in both their arguments if the underlying accumulator function is. -/
lemma foldr_mono {l₁ l₂ : List α} (f : α β β) {b₁ b₂ : β}
(hl : List.Forall₂ (· ·) l₁ l₂) (hb : b₁ b₂)
(hf₁ : b, Monotone fun a => f a b) (hf₂ : a, Monotone (f a)) :
(hf₁ : b, Monotone (f · 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)
theorem foldl_mono {l₁ l₂ : List α} (f : β α β) {b₁ b₂ : β}
/-- (left) folds are monotinic in both their arguments if the underlying accumulator function is. -/
lemma foldl_mono {l₁ l₂ : List α} (f : β α β) {b₁ b₂ : β}
(hl : List.Forall₂ (· ·) l₁ l₂) (hb : b₁ b₂)
(hf₁ : a, Monotone fun b => f b a) (hf₂ : b, Monotone (f b)) :
(hf₁ : a, Monotone (f · a)) (hf₂ : b, Monotone (f b ·)) :
l₁.foldl f b₁ l₂.foldl f b₂ := by
induction hl generalizing b₁ b₂ with
| nil => exact hb
@@ -30,61 +56,96 @@ theorem foldl_mono {l₁ l₂ : List α} (f : β → α → β) {b₁ b₂ : β}
exact ih (le_trans (hf₁ _ hb) (hf₂ _ hxy))
omit [Preorder α] in
theorem foldr_mono' (l : List α) (f : α β β)
(hf : a, Monotone (f a ·)) : Monotone fun b => l.foldr f b := by
/-- (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
intro b₁ b₂ hb
induction l with
| nil => exact hb
| cons x xs ih => exact hf x ih
omit [Preorder α] in
theorem foldl_mono' (l : List α) (f : β α β)
/-- (left) folds on a particular list are monotonic if the underlying accumulator is monotonic in its accumulator argument. -/
lemma 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
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
/-- 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 _ _)
class FiniteHeightLattice (α : Type*) [Lattice α] extends Bot α, Top α where
/-- 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
height :
longestChain : PointedLTSeries α height
chains_bounded : BoundedChains α 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
-- a < ... < z
-- ----------- length <= height
namespace FiniteHeightLattice
variable (α : Type*) [Lattice α] [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.
theorem bot_le (a : α) : ( : α) a := FixedHeight.bot_le a
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
end FiniteHeightLattice

View File

@@ -1,7 +1,38 @@
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
@@ -34,206 +65,125 @@ instance : Min (AboveBelow α) where
| mk _, bot => bot
| mk x, top => mk x
@[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 : α) :
@[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 : α) :
(mk x mk y : AboveBelow α) = if x = y then mk x else top := rfl
@[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 : α) :
@[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 : α) :
(mk x mk y : AboveBelow α) = if x = y then mk x else bot := rfl
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)
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
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
theorem le_iff {a b : AboveBelow α} : a b a b = b := sup_eq_right.symm
lemma le_iff {a b : AboveBelow α} : a b a b = b := sup_eq_right.symm
theorem bot_le' (a : AboveBelow α) : (bot : AboveBelow α) a :=
lemma bot_le' (a : AboveBelow α) : (bot : AboveBelow α) a :=
le_iff.mpr (bot_sup a)
theorem le_top' (a : AboveBelow α) : a (top : AboveBelow α) :=
lemma le_top' (a : AboveBelow α) : a (top : AboveBelow α) :=
le_iff.mpr (sup_top a)
theorem bot_lt_mk (x : α) : (bot : AboveBelow α) < mk x :=
lt_of_le_of_ne (bot_le' _) (by simp)
instance : OrderBot (AboveBelow α) where
bot := bot
bot_le := bot_le'
theorem mk_lt_top (x : α) : (mk x : AboveBelow α) < top :=
lt_of_le_of_ne (le_top' _) (by simp)
instance : OrderTop (AboveBelow α) where
top := top
le_top := le_top'
theorem bot_lt_top : (bot : AboveBelow α) < top :=
lt_of_le_of_ne (bot_le' _) (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 le_cases {a b : AboveBelow α} (h : a b) :
lemma le_cases {a b : AboveBelow α} (h : a b) :
a = bot b = top a = b := by
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)
rw [le_iff] at h
rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp_all
/-- 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 γ]
/-- 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 γ]
(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 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 -/
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', *]
section Interp
variable {V : Type*} {P : AboveBelow α V Prop}
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 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_inf_of
/-- 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
(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
· 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
· next heq => subst heq; exact h.1
· next hne => exact absurd h (hdisj hne v)
rcases s₁ with _ | _ | x <;> rcases s₂ with _ | _ | y <;> simp_all
split
· exact h.2
· next hne => exact (hdisj hne v h.1 h.2).elim
end Interp
/-- 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 α
/-- synthetic rank of an element, used to prove chain bounds. -/
private def rank : AboveBelow α
| bot => 0
| mk _ => 1
| top => 2
/-- 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
/-- 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
intro h
obtain hle, hne := lt_iff_le_and_ne.mp h
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)
rcases le_cases hle with h | h | h <;> simp_all
theorem rank_strictMono : StrictMono (rank : AboveBelow α ) := by
/-- The rank of elements is strictly monotonic. -/
lemma rank_strictMono : StrictMono (rank : AboveBelow α ) := by
intro a b hab
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)
rcases a with _ | _ | x <;> rcases b with _ | _ | y <;>
simp_all [rank, not_mk_lt_mk, (bot_le' _).not_lt, (le_top' _).not_lt]
theorem boundedChains : BoundedChains (AboveBelow α) 2 := fun c => by
/-- All chains in the above-below lattice have at most 2 comparisons. -/
lemma 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
bot := bot
top := top
toLattice := inferInstance
toOrderBot := inferInstance
toOrderTop := inferInstance
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

View File

@@ -0,0 +1,39 @@
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

View File

@@ -1,425 +1,207 @@
import Spa.Lattice.IterProd
import Spa.Isomorphism
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`.
-/
namespace Spa
def FiniteMap (A B : Type*) (ks : List A) : Type _ :=
{ l : List (A × B) // l.map Prod.fst = ks }
/-- Key-value map with domain `α` and codomain `β`, with possible keys $\textit{ks} \subseteq \alpha$. -/
def FiniteMap (α β : Type*) (ks : List α) : Type _ := Fin ks.length β
namespace FiniteMap
variable {A B : Type*} {ks : List A}
variable {α β : Type*} {ks : List α}
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 [Lattice β] : Lattice (FiniteMap α β ks) :=
inferInstanceAs (Lattice (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 [FiniteHeightLattice β] : FiniteHeightLattice (FiniteMap α β ks) :=
inferInstanceAs (FiniteHeightLattice (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 [DecidableEq β] : DecidableEq (FiniteMap α β ks) :=
inferInstanceAs (DecidableEq (Fin ks.length β))
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
instance : Membership (α × β) (FiniteMap α β ks) :=
fun fm p => i : Fin ks.length, ks.get i = p.1 fm i = p.2
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
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_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
def MemKey (k : α) (_fm : FiniteMap α β ks) : Prop := k ks
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
lemma MemKey_iff {k : α} {fm : FiniteMap α β ks} : MemKey k fm k ks := Iff.rfl
variable [Lattice B]
instance {k : α} {fm : FiniteMap α β ks} [DecidableEq α] : Decidable (MemKey k fm) :=
decidable_of_iff _ MemKey_iff.symm
instance : Max (FiniteMap A B ks) where
max fm₁ fm :=
combine (· ·) fm₁.val fm₂.val,
(combine_spine _ (spine_eq fm₁ fm₂)).trans fm₁.property
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 : Min (FiniteMap A B ks) where
min 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)
@[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
lemma le_def [Lattice β] {fm₁ fm₂ : FiniteMap α β ks} :
fm₁ fm₂ i, fm₁ i fm₂ i := Iff.rfl
section Locate
variable [DecidableEq A]
variable [DecidableEq α]
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
/-- 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
end Locate
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
variable [Lattice β]
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 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
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}
lemma mem_sup {fm₁ fm₂ : FiniteMap α β ks} {k : α} {v : β}
(h : (k, v) fm₁ fm₂) :
v₁ v₂, v = v₁ v₂ (k, v₁) fm₁ (k, v₂) fm₂ :=
mem_combine _ (spine_eq fm₁ fm₂) h
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
section Updating
variable [DecidableEq A]
variable [DecidableEq α]
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
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
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')
omit [Lattice β] in
lemma eq_of_mem_updating {k : α} {v : β} {fm : FiniteMap α β ks}
{ks' : List α} {g : α β} (hk : k ks')
(h : (k, v) updating fm ks' g) : v = g k := by
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
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]
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')
omit [Lattice β] in
lemma mem_of_mem_updating {k : α} {v : β} {fm : FiniteMap α β ks}
{ks' : List α} {g : α β} (hk : k ks')
(h : (k, v) updating fm ks' g) : (k, v) fm := by
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
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)]
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) :
lemma updating_mono {fm₁ fm₂ : FiniteMap α β ks} {ks' : List α}
{g₁ g₂ : α β} (hfm : fm₁ fm₂) (hg : k, g₁ k g₂ k) :
updating fm₁ ks' g₁ updating fm₂ ks' g₂ := by
rw [le_iff] at hfm
simp only [updating_val]
exact updating_mono_list hg hfm
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
end Updating
section GeneralizedUpdate
variable [DecidableEq A] {L : Type*} [Lattice L]
variable [DecidableEq α] {L : Type*} [Lattice L]
def generalizedUpdate (f : L FiniteMap A B ks) (g : A L B)
(ks' : List A) (l : L) : FiniteMap A B ks :=
def generalizedUpdate (f : L FiniteMap α β ks) (g : α L β)
(ks' : List α) : L FiniteMap α β ks := fun l =>
(f l).updating ks' (fun k => g k l)
variable {f : L FiniteMap A B ks} {g : A L B} {ks' : List A}
variable {f : L FiniteMap α β ks} {g : α L β} {ks' : List α}
theorem generalizedUpdate_monotone (hf : Monotone f)
lemma 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 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_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_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
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
end GeneralizedUpdate
section ValuesAt
variable [DecidableEq A]
variable [DecidableEq α]
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 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
def valuesAt (fm : FiniteMap A B ks) (ks' : List A) : List B :=
ks'.filterMap (fun k => lookup? k fm.val)
/-- 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
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
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
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
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
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) :
lemma valuesAt_le {fm fm : FiniteMap α β ks} (hle : fm₁ fm₂)
(ks' : List α) :
List.Forall₂ (· ·) (valuesAt fm₁ ks') (valuesAt fm₂ ks') := by
induction ks' with
| nil => exact List.Forall₂.nil
| cons k ks'' ih =>
have hrel := lookup?_forall₂ (le_iff.mp hle) k
have hrel := lookup_rel hle k
rw [valuesAt, valuesAt, List.filterMap_cons, List.filterMap_cons]
revert hrel
generalize lookup? k fm₁.val = o₁
generalize lookup? k fm₂.val = o₂
generalize fm₁.lookup k = o₁
generalize fm₂.lookup k = o₂
intro hrel
cases hrel with
| none => simpa [valuesAt] using ih
@@ -427,120 +209,6 @@ theorem valuesAt_le {fm₁ fm₂ : FiniteMap A B 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

View File

@@ -0,0 +1,38 @@
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

View File

@@ -1,50 +0,0 @@
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

View File

@@ -1,98 +0,0 @@
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 Normal file
View File

@@ -0,0 +1,128 @@
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

View File

@@ -1,18 +1,14 @@
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
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
instance : FiniteHeightLattice PUnit := FiniteHeightLattice.ofUnique PUnit
end Spa

View File

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

View File

@@ -0,0 +1,102 @@
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