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>
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>
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>
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>
- 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>
LatticeInterpretation now extends Interp L (Value → Prop), so each analysis
defines only its LatticeInterpretation instance and gets the ⟦⟧ notation for
free. Drops the standalone per-analysis Interp instances (signInterp and the
anonymous constInterp). The Interp class is kept for other uses.
The interp*_mk_disjoint bootstrap lemmas now state on the raw interp function
since they feed the instance and run before any Interp instance exists; the
trivial sup/inf wrappers are inlined into the instance.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
These eight one-line projections of plus_mono₂/minus_mono₂ were never
referenced; eval_mono uses the bundled Monotone₂ facts directly.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Per convention, create a new instance for 'interpretable' thing,
with an fundep'ed semantic domain. I feel at peace with this notation
even though it conflicts with Mathlib's quotients.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The fable-based migration left a two-layer design (a standalone `FixedHeight α h`
struct, height carried as a type index, plus a `FiniteHeightLattice` wrapper).
This collapses it to the single `FiniteHeightLattice` typeclass (height as a
plain field, `⊥`/`⊤` via `extends Bot`/`Top`), and fixes the fallout so the
whole project builds again (`lake build` green).
- Lattice: repair `FixedHeight.bot_le` (compute the `▸` motive via a forward
`rw`, drop the leftover `fh.length_longestChain`) and the `bot_le` alias.
- Isomorphism: transport rewritten directly onto `FiniteHeightLattice`, taking
the source as an instance argument.
- Lattice/Prod, AboveBelow: `FixedHeight`-producing def + wrapper instance
collapsed into one `FiniteHeightLattice` instance. `head`/`last` proofs use
term-mode `congrArg` to bridge the `Bot`/`Top` defeq through the
under-construction instance projection (where `rw`+`rfl` cannot).
- Lattice/IterProd: `fixedHeight` recursion now yields a `FiniteHeightLattice`
(no height index, so the `.cast (by ring)` reassociations vanish);
`bot_fixedHeight` reprojected onto the def's own `.bot`.
- Lattice/FiniteMap: `fixedHeight`/`bot_contains_bots` go through transport with
the IterProd instance resolved by typeclass search; `punitFixedHeight`
replaced by the `PUnit` instance.
- Analysis/Forward/Lattices: `botV` uses `⊥` instead of the deleted
`FiniteHeightLattice.bot` accessor.
- Analysis/Sign: `num` case used unimported `ring`; the goal is a pure ℕ→ℤ
cast identity, closed with `norm_cast`. Also fixes the missing `show` in
`AboveBelow.monotone₂_of_strict` that left un-beta-reduced redexes.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The port had flattened Agda's instance arguments ({{flA}}, {{evaluator}},
{{latticeInterpretation}}, {{validEvaluator}}) into explicitly threaded
values (fhL, E, I, hE). Restore them as typeclasses:
- Spa.FiniteHeightLattice: now actually used — Fixedpoint takes the
instance instead of a FixedHeight value; FiniteMap gets the missing
instance (height = ks.length * height B), so varsFixedHeight /
statesFixedHeight / signFixedHeight / constFixedHeight plumbing
disappears (instance bottoms are defeq to the old ones)
- Spa.Analysis.Forward.Evaluation: StmtEvaluator/ExprEvaluator become
classes; the Valid* Props become Prop-classes, as in Agda
- Spa.Analysis.Forward.Adapters: the expr→stmt adapter and its validity
are instances (Agda: the ExprToStmtAdapter instances)
- LatticeInterpretation is a class; sign/const interpretations,
evaluators and validity proofs are instances; use sites read like the
Agda module applications: result SignLattice prog
Proof simplifications (same theorems, proofs factored):
- Spa.Lattice.AboveBelow.monotone₂_of_strict: any ⊥-strict/⊤-dominated
operation on a flat lattice is monotone — replaces the four near-
identical case bashes per analysis (postulates in Agda)
- Spa.Lattice.AboveBelow.interp_sup_of/interp_inf_of: the shared flat-
lattice interpretation case analysis, making interpSign_sup/inf and
interpConst_sup/inf one-liners
lake build green with zero warnings; lake exe spa output verified
byte-identical (diff) to the previous, Agda-verified output.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
- Spa.Showable: port of Showable.agda (quoted strings, map format) for
output parity
- Spa.Analysis.Utils: eval_combine₂
- Spa.Lattice.AboveBelow.le_cases: order of the flat lattice by cases
- Spa.Analysis.Sign / Spa.Analysis.Constant: the four monotonicity
POSTULATES from the Agda files are now proved theorems (via le_cases);
interpretations, evaluator validity, analyze_correct per analysis
- Main + lake exe spa: runs both analyses on the Agda test program;
constant analysis folds unknown=0, sign analysis gives unknown=⊤
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
- Spa.Analysis.Forward.Lattices: VariableValues/StateVariables (FiniteMap
instantiations), fixed heights, variablesAt, joinForKey/joinAll, interpV
and its sup/foldr lemmas
- Spa.Analysis.Forward.Evaluation: StmtEvaluator/ExprEvaluator + validity
(the Agda Valid* instance records become plain Props)
- Spa.Analysis.Forward.Adapters: expr-to-stmt evaluator adapter + validity
- Spa.Analysis.Forward: updateAll, analyze, result (least fixpoint via the
gas-based Fixedpoint), walkTrace, analyze_correct — the framework's main
soundness theorem
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
