From b16f14fdfdccce03c114c8e580f0df256591ef6f Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Tue, 9 Jun 2026 23:32:38 -0700 Subject: [PATCH] Lean migration: typeclass-based parameter passing, as in the Agda original MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- LEAN_MIGRATION.md | 8 +- lean/Spa/Analysis/Constant.lean | 159 +++++--------------- lean/Spa/Analysis/Forward.lean | 127 ++++++++-------- lean/Spa/Analysis/Forward/Adapters.lean | 38 +++-- lean/Spa/Analysis/Forward/Evaluation.lean | 39 +++-- lean/Spa/Analysis/Forward/Lattices.lean | 60 ++++---- lean/Spa/Analysis/Sign.lean | 168 ++++++---------------- lean/Spa/Fixedpoint.lean | 49 ++++--- lean/Spa/Language/Semantics.lean | 5 +- lean/Spa/Lattice.lean | 17 ++- lean/Spa/Lattice/AboveBelow.lean | 69 +++++++++ lean/Spa/Lattice/FiniteMap.lean | 6 + 12 files changed, 338 insertions(+), 407 deletions(-) diff --git a/LEAN_MIGRATION.md b/LEAN_MIGRATION.md index 9f99323..5a7aaf7 100644 --- a/LEAN_MIGRATION.md +++ b/LEAN_MIGRATION.md @@ -45,8 +45,8 @@ validate phase by phase. | `Language/Traces.agda` | custom, same `Trace`/`EndToEndTrace`/`++⟨_⟩` | | | `Language/Properties.agda` | custom, same lemma inventory (`Trace-∙ˡ/ʳ`, `Trace-↦ˡ/ʳ`, `Trace-loop`, `EndToEndTrace-*`, `wrap-preds-∅`, `buildCfg-sufficient`) | the "ugly" `↑-≢` Fin-disjointness block should shrink via `Fin.castAdd_ne_natAdd`-style mathlib lemmas | | `Language.agda` (`Program` record) | custom, same fields/lemmas (`trace`, `vars`, `states`, `incoming`, `initialState-pred-∅`, …) | | -| `Analysis/Forward/{Lattices,Evaluation,Adapters}.agda`, `Analysis/Forward.agda` | custom, same structure: `VariableValues`, `StateVariables`, `joinForKey`/`joinAll`, `StmtEvaluator`/`ExprEvaluator` + validity, expr→stmt adapter, `analyze`, `result`, `analyze-correct` | section variables instead of parameterized modules | -| `Analysis/Sign.agda`, `Analysis/Constant.agda` | custom, same definitions | the four monotonicity **postulates** become real proofs by `decide` (finite lattice, decidable `≤`) | +| `Analysis/Forward/{Lattices,Evaluation,Adapters}.agda`, `Analysis/Forward.agda` | custom, same structure: `VariableValues`, `StateVariables`, `joinForKey`/`joinAll`, `StmtEvaluator`/`ExprEvaluator` + validity, expr→stmt adapter, `analyze`, `result`, `analyze-correct` | section variables instead of parameterized modules; everything Agda passed as an instance argument (`IsFiniteHeightLattice`, the evaluators, `LatticeInterpretation`, the validity records) is a typeclass resolved by instance search | +| `Analysis/Sign.agda`, `Analysis/Constant.agda` | custom, same definitions | the four monotonicity **postulates** become real proofs (any `⊥`-strict/`⊤`-dominating operation on a flat lattice is monotone: `AboveBelow.monotone₂_of_strict`) | | `Main.agda` | `lake exe spa` | same test programs, same printed output | ## Phases & checkpoints @@ -91,7 +91,9 @@ correspondence tables live in the header comment of each Lean file. - The four monotonicity **postulates** in `Analysis/Sign.agda` and `Analysis/Constant.agda` are now proved theorems (via - `AboveBelow.le_cases`), so the Lean development is postulate-free. + `AboveBelow.monotone₂_of_strict`: any operation on the flat lattice that + is strict in `⊥` and dominated by `⊤` is monotone, whatever its table), + so the Lean development is postulate-free. - ~2200 lines of map machinery (`Lattice/Map.agda`, `Lattice/MapSet.agda`, much of `Lattice/FiniteMap.agda`) collapse into the spine-pinned `FiniteMap` + `Finset`; the `IterProd` isomorphism no longer needs diff --git a/lean/Spa/Analysis/Constant.lean b/lean/Spa/Analysis/Constant.lean index dd13650..f72aa86 100644 --- a/lean/Spa/Analysis/Constant.lean +++ b/lean/Spa/Analysis/Constant.lean @@ -4,11 +4,13 @@ Port of `Analysis/Constant.agda`. Correspondence: showable, ≡-equiv, ≡-Decidable-ℤ ↦ (mathlib/derived instances) ConstLattice (AboveBelow ℤ) ↦ ConstLattice - AB.Plain (+ 0) ↦ constFixedHeight + AB.Plain (+ 0) ↦ the AboveBelow FiniteHeightLattice instance, + seeded by `Inhabited ℤ` (default `0`) plus, minus ↦ plus, minus plus-Monoˡ/ʳ, minus-Monoˡ/ʳ (postulates in Agda!) ↦ plus_mono_left/right, minus_mono_left/right - — now actually proved, via AboveBelow.le_cases + — now actually proved, via + AboveBelow.monotone₂_of_strict plus-Mono₂, minus-Mono₂ ↦ plus_mono₂, minus_mono₂ ⟦_⟧ᶜ ↦ interpConst ⟦⟧ᶜ-respects-≈ᶜ ↦ (trivial with `=`) @@ -30,10 +32,6 @@ namespace Spa abbrev ConstLattice : Type := AboveBelow ℤ -/-- Agda: `AB.Plain (+ 0)`'s `fixedHeight`. -/ -def constFixedHeight : FixedHeight ConstLattice 2 := - AboveBelow.plainFixedHeight (0 : ℤ) - namespace ConstAnalysis open AboveBelow in @@ -54,81 +52,33 @@ def minus : ConstLattice → ConstLattice → ConstLattice | _, top => top | mk z₁, mk z₂ => mk (z₁ - z₂) +/-- Agda: `plus-Mono₂` (its components were postulates in Agda; `plus` is a +strict operation on the flat lattice, so monotonicity holds regardless of the +constant table). -/ +theorem 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) + /-- Agda: `plus-Monoˡ` — a postulate there, a theorem here. -/ -theorem plus_mono_left (s₂ : ConstLattice) : Monotone (plus · s₂) := by - intro a b h - rcases AboveBelow.le_cases h with rfl | rfl | rfl - · rcases s₂ with _ | _ | y <;> rcases b with _ | _ | x <;> - simp only [plus] <;> - first - | exact le_refl _ - | exact AboveBelow.le_top' _ - | exact AboveBelow.bot_le' _ - · rcases s₂ with _ | _ | y <;> rcases a with _ | _ | x <;> - simp only [plus] <;> - first - | exact le_refl _ - | exact AboveBelow.le_top' _ - · exact le_refl _ +theorem plus_mono_left (s₂ : ConstLattice) : Monotone (plus · s₂) := plus_mono₂.1 s₂ /-- Agda: `plus-Monoʳ` — a postulate there, a theorem here. -/ -theorem plus_mono_right (s₁ : ConstLattice) : Monotone (plus s₁) := by - intro a b h - rcases AboveBelow.le_cases h with rfl | rfl | rfl - · rcases s₁ with _ | _ | x <;> rcases b with _ | _ | y <;> - simp only [plus] <;> - first - | exact le_refl _ - | exact AboveBelow.le_top' _ - | exact AboveBelow.bot_le' _ - · rcases s₁ with _ | _ | x <;> rcases a with _ | _ | y <;> - simp only [plus] <;> - first - | exact le_refl _ - | exact AboveBelow.le_top' _ - · exact le_refl _ +theorem plus_mono_right (s₁ : ConstLattice) : Monotone (plus s₁) := plus_mono₂.2 s₁ -/-- Agda: `plus-Mono₂`. -/ -theorem plus_mono₂ : Monotone₂ plus := - ⟨plus_mono_left, plus_mono_right⟩ +/-- Agda: `minus-Mono₂` (likewise from strictness of `minus`). -/ +theorem 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) /-- Agda: `minus-Monoˡ` — a postulate there, a theorem here. -/ -theorem minus_mono_left (s₂ : ConstLattice) : Monotone (minus · s₂) := by - intro a b h - rcases AboveBelow.le_cases h with rfl | rfl | rfl - · rcases s₂ with _ | _ | y <;> rcases b with _ | _ | x <;> - simp only [minus] <;> - first - | exact le_refl _ - | exact AboveBelow.le_top' _ - | exact AboveBelow.bot_le' _ - · rcases s₂ with _ | _ | y <;> rcases a with _ | _ | x <;> - simp only [minus] <;> - first - | exact le_refl _ - | exact AboveBelow.le_top' _ - · exact le_refl _ +theorem minus_mono_left (s₂ : ConstLattice) : Monotone (minus · s₂) := minus_mono₂.1 s₂ /-- Agda: `minus-Monoʳ` — a postulate there, a theorem here. -/ -theorem minus_mono_right (s₁ : ConstLattice) : Monotone (minus s₁) := by - intro a b h - rcases AboveBelow.le_cases h with rfl | rfl | rfl - · rcases s₁ with _ | _ | x <;> rcases b with _ | _ | y <;> - simp only [minus] <;> - first - | exact le_refl _ - | exact AboveBelow.le_top' _ - | exact AboveBelow.bot_le' _ - · rcases s₁ with _ | _ | x <;> rcases a with _ | _ | y <;> - simp only [minus] <;> - first - | exact le_refl _ - | exact AboveBelow.le_top' _ - · exact le_refl _ - -/-- Agda: `minus-Mono₂`. -/ -theorem minus_mono₂ : Monotone₂ minus := - ⟨minus_mono_left, minus_mono_right⟩ +theorem minus_mono_right (s₁ : ConstLattice) : Monotone (minus s₁) := minus_mono₂.2 s₁ /-- Agda: `⟦_⟧ᶜ`. -/ def interpConst : ConstLattice → Value → Prop @@ -144,48 +94,18 @@ theorem interpConst_mk_disjoint {z₁ z₂ : ℤ} (hne : z₁ ≠ z₂) {v : Val injection h₂ with hz exact hne hz -/-- Agda: `⟦⟧ᶜ-⊔ᶜ-∨`. -/ +/-- Agda: `⟦⟧ᶜ-⊔ᶜ-∨` (via the factored flat-lattice lemma). -/ theorem interpConst_sup {s₁ s₂ : ConstLattice} (v : Value) - (h : interpConst s₁ v ∨ interpConst s₂ v) : interpConst (s₁ ⊔ s₂) v := by - rcases s₁ with _ | _ | z₁ - · rcases h with h | h - · exact h.elim - · rw [AboveBelow.bot_sup] - exact h - · exact trivial - · rcases s₂ with _ | _ | z₂ - · rcases h with h | h - · rw [AboveBelow.sup_bot] - exact h - · exact h.elim - · rw [AboveBelow.sup_top] - exact trivial - · by_cases hz : z₁ = z₂ - · subst hz - rw [AboveBelow.mk_sup_mk, if_pos rfl] - rcases h with h | h <;> exact h - · rw [AboveBelow.mk_sup_mk, if_neg hz] - exact trivial + (h : interpConst s₁ v ∨ interpConst s₂ v) : interpConst (s₁ ⊔ s₂) v := + AboveBelow.interp_sup_of (fun _ h => h) (fun _ => trivial) v h -/-- Agda: `⟦⟧ᶜ-⊓ᶜ-∧`. -/ +/-- Agda: `⟦⟧ᶜ-⊓ᶜ-∧` (via the factored flat-lattice lemma). -/ theorem interpConst_inf {s₁ s₂ : ConstLattice} (v : Value) - (h : interpConst s₁ v ∧ interpConst s₂ v) : interpConst (s₁ ⊓ s₂) v := by - rcases s₁ with _ | _ | z₁ - · exact h.1 - · rw [AboveBelow.top_inf] - exact h.2 - · rcases s₂ with _ | _ | z₂ - · exact h.2 - · rw [AboveBelow.inf_top] - exact h.1 - · by_cases hz : z₁ = z₂ - · subst hz - rw [AboveBelow.mk_inf_mk, if_pos rfl] - exact h.1 - · exact absurd h (interpConst_mk_disjoint hz) + (h : interpConst s₁ v ∧ interpConst s₂ v) : interpConst (s₁ ⊓ s₂) v := + AboveBelow.interp_inf_of (fun hne _ => interpConst_mk_disjoint hne) v h -/-- Agda: `latticeInterpretationᶜ`. -/ -def constInterpretation : LatticeInterpretation ConstLattice where +/-- Agda: `latticeInterpretationᶜ` (an instance there too). -/ +instance constInterpretation : LatticeInterpretation ConstLattice where interp := interpConst interp_sup := fun {l₁ l₂} v h => interpConst_sup (s₁ := l₁) (s₂ := l₂) v h interp_inf := fun {l₁ l₂} v h => interpConst_inf (s₁ := l₁) (s₂ := l₂) v h @@ -224,12 +144,12 @@ theorem eval_mono (e : Expr) : Monotone (eval prog e) := by exact le_refl _ /-- Agda: the `ConstEval` instance. -/ -def exprEvaluator : ExprEvaluator ConstLattice prog := +instance exprEvaluator : ExprEvaluator ConstLattice prog := ⟨eval prog, eval_mono prog⟩ /-- Agda: `WithProg.result`/`output`. -/ def output : String := - show' (result constFixedHeight (exprEvaluator prog).toStmtEvaluator) + show' (result ConstLattice prog) /-- Agda: `plus-valid`. -/ theorem plus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ} @@ -267,9 +187,9 @@ theorem minus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ} show Value.int (z₁ - z₂) = Value.int (c₁ - c₂) rw [hz₁, hz₂] -/-- Agda: `eval-valid` / `ConstEvalValid`. -/ -theorem eval_valid : - IsValidExprEvaluator (exprEvaluator prog) constInterpretation := by +/-- Agda: `eval-valid` / the `ConstEvalValid` instance. -/ +instance eval_valid : ValidExprEvaluator ConstLattice prog := by + constructor intro vs ρ e v hev induction hev with | num n => @@ -300,11 +220,8 @@ theorem eval_valid : /-- Agda: `WithProg.analyze-correct`. -/ theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : - interpV constInterpretation - (variablesAt prog.finalState - (result constFixedHeight (exprEvaluator prog).toStmtEvaluator)) ρ := - Spa.analyze_correct constFixedHeight - ((exprEvaluator prog).toStmtEvaluator_valid (eval_valid prog)) hrun + interpV (variablesAt prog.finalState (result ConstLattice prog)) ρ := + Spa.analyze_correct ConstLattice prog hrun end ConstAnalysis diff --git a/lean/Spa/Analysis/Forward.lean b/lean/Spa/Analysis/Forward.lean index 1652c3d..f1edba5 100644 --- a/lean/Spa/Analysis/Forward.lean +++ b/lean/Spa/Analysis/Forward.lean @@ -2,6 +2,12 @@ Port of `Analysis/Forward.agda` (`WithProg`, `WithStmtEvaluator`, `WithValidInterpretation`). +As in Agda, the statement evaluator, the lattice interpretation and the +evaluator's validity proof are instance arguments (`{{evaluator}}`, +`{{latticeInterpretationˡ}}`, `{{validEvaluator}}`); `result` and +`analyze_correct` take `L` and `prog` explicitly, mirroring the Agda call +shape `WithProg.result L prog`. + Correspondence: updateVariablesForState, -Monoʳ ↦ updateVariablesForState, _mono updateAll, updateAll-Mono, @@ -26,139 +32,136 @@ import Spa.Fixedpoint namespace Spa -variable {L : Type} [Lattice L] [DecidableEq L] {prog : Program} {h : ℕ} - (fhL : FixedHeight L h) (E : StmtEvaluator L prog) +variable {L : Type} [Lattice L] {prog : Program} [E : StmtEvaluator L prog] /-- Agda: `updateVariablesForState`. -/ 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) -omit [DecidableEq L] in /-- Agda: `updateVariablesForState-Monoʳ`. -/ theorem updateVariablesForState_mono (s : prog.State) : - Monotone (updateVariablesForState E s) := fun _ _ hle => + Monotone (updateVariablesForState (L := L) s) := fun _ _ hle => foldl_mono' (prog.code s) _ (fun bs => E.eval_mono s bs) (variablesAt_le hle s) /-- Agda: `updateAll`. -/ def updateAll (sv : StateVariables L prog) : StateVariables L prog := - FiniteMap.generalizedUpdate id (fun s sv => updateVariablesForState E s sv) + FiniteMap.generalizedUpdate id (fun s sv => updateVariablesForState s sv) prog.states sv -omit [DecidableEq L] in /-- Agda: `updateAll-Mono`. -/ -theorem updateAll_mono : Monotone (updateAll E) := - FiniteMap.generalizedUpdate_monotone monotone_id (updateVariablesForState_mono E) +theorem updateAll_mono : Monotone (updateAll (L := L) (prog := prog)) := + FiniteMap.generalizedUpdate_monotone monotone_id updateVariablesForState_mono -omit [DecidableEq L] in /-- Agda: `updateAll-k∈ks-≡`. -/ theorem updateAll_mem_eq {s : prog.State} {vs : VariableValues L prog} - {sv : StateVariables L prog} (hmem : (s, vs) ∈ updateAll E sv) : - vs = updateVariablesForState E s sv := + {sv : StateVariables L prog} (hmem : (s, vs) ∈ updateAll sv) : + vs = updateVariablesForState s sv := FiniteMap.generalizedUpdate_mem_eq (prog.states_complete s) hmem -omit [DecidableEq L] in /-- Agda: `variablesAt-updateAll`. -/ theorem variablesAt_updateAll (s : prog.State) (sv : StateVariables L prog) : - variablesAt s (updateAll E sv) = updateVariablesForState E s sv := - updateAll_mem_eq E (variablesAt_mem s (updateAll E sv)) + variablesAt s (updateAll sv) = updateVariablesForState s sv := + updateAll_mem_eq (variablesAt_mem s (updateAll sv)) + +variable [FiniteHeightLattice L] /-- Agda: `analyze`. -/ def analyze (sv : StateVariables L prog) : StateVariables L prog := - updateAll E (joinAll fhL sv) + updateAll (joinAll sv) -omit [DecidableEq L] in /-- Agda: `analyze-Mono`. -/ -theorem analyze_mono : Monotone (analyze fhL E) := fun _ _ hle => - updateAll_mono E (joinAll_mono fhL hle) +theorem analyze_mono : Monotone (analyze (L := L) (prog := prog)) := fun _ _ hle => + updateAll_mono (joinAll_mono hle) +variable [DecidableEq L] + +variable (L prog) in /-- Agda: `result` (the least fixpoint of `analyze`). -/ def result : StateVariables L prog := - Fixedpoint.aFix (statesFixedHeight L prog fhL) (analyze fhL E) (analyze_mono fhL E) + Fixedpoint.aFix analyze analyze_mono +variable (L prog) in /-- Agda: `result≈analyze-result`. -/ -theorem result_eq : result fhL E = analyze fhL E (result fhL E) := - Fixedpoint.aFix_eq (statesFixedHeight L prog fhL) (analyze fhL E) (analyze_mono fhL E) +theorem result_eq : result L prog = analyze (result L prog) := + Fixedpoint.aFix_eq analyze analyze_mono + +/-- Agda: `joinForKey-initialState-⊥ᵛ`. -/ +theorem joinForKey_initialState : + joinForKey prog.initialState (result L prog) = botV L prog := by + rw [joinForKey, prog.incoming_initialState_eq_nil] + rfl /-! ### Semantic correctness (Agda: `WithValidInterpretation`) -/ -variable {I : LatticeInterpretation L} {E} -variable (hE : IsValidStmtEvaluator E I) -include hE +variable [I : LatticeInterpretation L] [V : ValidStmtEvaluator L prog] -omit [DecidableEq L] in +omit [FiniteHeightLattice L] [DecidableEq L] in /-- Agda: `eval-fold-valid`. -/ theorem eval_fold_valid {s : prog.State} {bss : List BasicStmt} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env} - (hbss : EvalBasicStmts ρ₁ bss ρ₂) (hvs : interpV I vs ρ₁) : - interpV I (bss.foldl (fun vs bs => E.eval s bs vs) vs) ρ₂ := by + (hbss : EvalBasicStmts ρ₁ bss ρ₂) (hvs : interpV vs ρ₁) : + interpV (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 (hE hbs hvs) + | cons hbs _ ih => exact ih (ValidStmtEvaluator.valid hbs hvs) -omit [DecidableEq L] in +omit [FiniteHeightLattice L] [DecidableEq L] in /-- Agda: `updateVariablesForState-matches`. -/ theorem updateVariablesForState_matches {s : prog.State} {sv : StateVariables L prog} {ρ₁ ρ₂ : Env} (hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂) - (hvs : interpV I (variablesAt s sv) ρ₁) : - interpV I (updateVariablesForState E s sv) ρ₂ := - eval_fold_valid hE hbss hvs + (hvs : interpV (variablesAt s sv) ρ₁) : + interpV (updateVariablesForState s sv) ρ₂ := + eval_fold_valid hbss hvs -omit [DecidableEq L] in +omit [FiniteHeightLattice L] [DecidableEq L] in /-- Agda: `updateAll-matches`. -/ theorem updateAll_matches {s : prog.State} {sv : StateVariables L prog} {ρ₁ ρ₂ : Env} (hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂) - (hvs : interpV I (variablesAt s sv) ρ₁) : - interpV I (variablesAt s (updateAll E sv)) ρ₂ := by + (hvs : interpV (variablesAt s sv) ρ₁) : + interpV (variablesAt s (updateAll sv)) ρ₂ := by rw [variablesAt_updateAll] - exact updateVariablesForState_matches hE hbss hvs + exact updateVariablesForState_matches hbss hvs /-- Agda: `stepTrace`. -/ theorem stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env} - (hjoin : interpV I (joinForKey fhL s₁ (result fhL E)) ρ₁) + (hjoin : interpV (joinForKey s₁ (result L prog)) ρ₁) (hbss : EvalBasicStmts ρ₁ (prog.code s₁) ρ₂) : - interpV I (variablesAt s₁ (result fhL E)) ρ₂ := by - rw [result_eq fhL E] - refine updateAll_matches hE hbss ?_ + interpV (variablesAt s₁ (result L prog)) ρ₂ := by + rw [result_eq L prog] + refine updateAll_matches hbss ?_ rw [variablesAt_joinAll] exact hjoin /-- Agda: `walkTrace`. -/ theorem walkTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} - (hjoin : interpV I (joinForKey fhL s₁ (result fhL E)) ρ₁) + (hjoin : interpV (joinForKey s₁ (result L prog)) ρ₁) (tr : Trace prog.graph s₁ s₂ ρ₁ ρ₂) : - interpV I (variablesAt s₂ (result fhL E)) ρ₂ := by + interpV (variablesAt s₂ (result L prog)) ρ₂ := by induction tr with - | single hbss => exact stepTrace fhL hE hjoin hbss + | single hbss => exact stepTrace hjoin hbss | @edge _ ρ' _ i₁ i₂ _ hbss hedge _ ih => - have hstep : interpV I (variablesAt i₁ (result fhL E)) ρ' := - stepTrace fhL hE hjoin hbss - have hmem : variablesAt i₁ (result fhL E) - ∈ (result fhL E).valuesAt (prog.incoming i₂) := + have hstep : interpV (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 fhL E)) - exact ih (interpV_foldr fhL I hstep hmem) + (prog.mem_incoming_of_edge hedge) (variablesAt_mem i₁ (result L prog)) + exact ih (interpV_foldr hstep hmem) -omit hE in -/-- Agda: `joinForKey-initialState-⊥ᵛ`. -/ -theorem joinForKey_initialState : - joinForKey fhL prog.initialState (result fhL E) = botV L prog fhL := by - rw [joinForKey, prog.incoming_initialState_eq_nil] - rfl - -omit hE in +omit V in /-- Agda: `⟦joinAll-initialState⟧ᵛ∅`. -/ theorem interpV_joinForKey_initialState : - interpV I (joinForKey fhL prog.initialState (result fhL E)) [] := by + interpV (joinForKey prog.initialState (result L prog)) [] := by rw [joinForKey_initialState] - exact interpV_botV_nil fhL I + exact interpV_botV_nil +variable (L prog) in /-- Agda: `analyze-correct` — the analysis result at the final state soundly describes every terminating execution of the program. -/ theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : - interpV I (variablesAt prog.finalState (result fhL E)) ρ := - walkTrace fhL hE (interpV_joinForKey_initialState fhL (E := E) (I := I)) - (prog.trace hrun) + interpV (variablesAt prog.finalState (result L prog)) ρ := + walkTrace interpV_joinForKey_initialState (prog.trace hrun) end Spa diff --git a/lean/Spa/Analysis/Forward/Adapters.lean b/lean/Spa/Analysis/Forward/Adapters.lean index 8be9d53..9e24abb 100644 --- a/lean/Spa/Analysis/Forward/Adapters.lean +++ b/lean/Spa/Analysis/Forward/Adapters.lean @@ -6,8 +6,8 @@ Correspondence: updateVariablesFromExpression-Mono ↦ updateVariablesFromExpression_mono (the -k∈ks-≡ / -k∉ks-backward renames ↦ used directly from FiniteMap) evalᵇ, evalᵇ-Monoʳ ↦ evalB, evalB_mono - stmtEvaluator (instance) ↦ ExprEvaluator.toStmtEvaluator - evalᵇ-valid, validStmtEvaluator ↦ ExprEvaluator.toStmtEvaluator_valid + stmtEvaluator (instance) ↦ instance StmtEvaluator L prog + evalᵇ-valid, validStmtEvaluator ↦ instance ValidStmtEvaluator L prog (the Agda `k ≟ˢ k'` case split is subsumed by `cases` on `Env.Mem`, whose `here` case forces `k' = k`) @@ -16,43 +16,41 @@ import Spa.Analysis.Forward.Evaluation namespace Spa -variable {L : Type} [Lattice L] {prog : Program} +variable {L : Type} [Lattice L] {prog : Program} [E : ExprEvaluator L prog] /-- Agda: `updateVariablesFromExpression` — set the single key `k` to the value of `e` (the `GeneralizedUpdate` with `ks = [k]`). -/ -def updateVariablesFromExpression (E : ExprEvaluator L prog) (k : String) - (e : Expr) (vs : VariableValues L prog) : VariableValues 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 /-- Agda: `updateVariablesFromExpression-Mono`. -/ -theorem updateVariablesFromExpression_mono (E : ExprEvaluator L prog) - (k : String) (e : Expr) : - Monotone (updateVariablesFromExpression E k e) := +theorem updateVariablesFromExpression_mono (k : String) (e : Expr) : + Monotone (updateVariablesFromExpression (L := L) (prog := prog) k e) := FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => E.eval_mono e) /-- Agda: `evalᵇ`. -/ -def evalB (E : ExprEvaluator L prog) (_ : prog.State) (bs : BasicStmt) +def evalB (_ : prog.State) (bs : BasicStmt) (vs : VariableValues L prog) : VariableValues L prog := match bs with - | .assign k e => updateVariablesFromExpression E k e vs + | .assign k e => updateVariablesFromExpression k e vs | .noop => vs /-- Agda: `evalᵇ-Monoʳ`. -/ -theorem evalB_mono (E : ExprEvaluator L prog) (s : prog.State) (bs : BasicStmt) : - Monotone (evalB E s bs) := by +theorem evalB_mono (s : prog.State) (bs : BasicStmt) : + Monotone (evalB (L := L) (prog := prog) s bs) := by cases bs with - | assign k e => exact updateVariablesFromExpression_mono E k e + | assign k e => exact updateVariablesFromExpression_mono k e | noop => exact monotone_id /-- Agda: the `stmtEvaluator` instance of `ExprToStmtAdapter`. -/ -def ExprEvaluator.toStmtEvaluator (E : ExprEvaluator L prog) : - StmtEvaluator L prog := - ⟨evalB E, evalB_mono E⟩ +instance ExprEvaluator.toStmtEvaluator : StmtEvaluator L prog := + ⟨evalB, evalB_mono⟩ /-- Agda: `evalᵇ-valid` / the `validStmtEvaluator` instance. -/ -theorem ExprEvaluator.toStmtEvaluator_valid (E : ExprEvaluator L prog) - {I : LatticeInterpretation L} (hE : IsValidExprEvaluator E I) : - IsValidStmtEvaluator E.toStmtEvaluator I := by +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 @@ -65,7 +63,7 @@ theorem ExprEvaluator.toStmtEvaluator_valid (E : ExprEvaluator L prog) 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 hE hev hvs + 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 diff --git a/lean/Spa/Analysis/Forward/Evaluation.lean b/lean/Spa/Analysis/Forward/Evaluation.lean index 8708187..8dd465d 100644 --- a/lean/Spa/Analysis/Forward/Evaluation.lean +++ b/lean/Spa/Analysis/Forward/Evaluation.lean @@ -1,15 +1,15 @@ /- Port of `Analysis/Forward/Evaluation.agda`. +All four records were consumed through Agda instance arguments (`{{evaluator : +StmtEvaluator}}`, `{{validEvaluator : ValidStmtEvaluator …}}`), so they are +typeclasses here as well. + Correspondence: StmtEvaluator (eval, eval-Monoʳ) ↦ StmtEvaluator (eval, eval_mono) ExprEvaluator (eval, eval-Monoʳ) ↦ ExprEvaluator (eval, eval_mono) - IsValidExprEvaluator ↦ IsValidExprEvaluator - IsValidStmtEvaluator ↦ IsValidStmtEvaluator - ValidExprEvaluator, - ValidStmtEvaluator (records) ↦ (the `IsValid…` Props are passed - directly; the wrapper records existed - for Agda instance resolution) + ValidExprEvaluator ↦ ValidExprEvaluator (valid) + ValidStmtEvaluator ↦ ValidStmtEvaluator (valid) -/ import Spa.Analysis.Forward.Lattices @@ -18,27 +18,26 @@ namespace Spa variable (L : Type) [Lattice L] (prog : Program) /-- Agda: `StmtEvaluator`. -/ -structure StmtEvaluator where +class StmtEvaluator where eval : prog.State → BasicStmt → VariableValues L prog → VariableValues L prog eval_mono : ∀ s bs, Monotone (eval s bs) /-- Agda: `ExprEvaluator`. -/ -structure ExprEvaluator where +class ExprEvaluator where eval : Expr → VariableValues L prog → L eval_mono : ∀ e, Monotone (eval e) -variable {L prog} +/-- Agda: `ValidExprEvaluator`. -/ +class ValidExprEvaluator [ExprEvaluator L prog] [I : LatticeInterpretation L] : + Prop where + valid : ∀ {vs : VariableValues L prog} {ρ : Env} {e : Expr} {v : Value}, + EvalExpr ρ e v → interpV vs ρ → I.interp (ExprEvaluator.eval e vs) v -/-- Agda: `IsValidExprEvaluator`. -/ -def IsValidExprEvaluator (E : ExprEvaluator L prog) - (I : LatticeInterpretation L) : Prop := - ∀ {vs : VariableValues L prog} {ρ : Env} {e : Expr} {v : Value}, - EvalExpr ρ e v → interpV I vs ρ → I.interp (E.eval e vs) v - -/-- Agda: `IsValidStmtEvaluator`. -/ -def IsValidStmtEvaluator (E : StmtEvaluator L prog) - (I : LatticeInterpretation L) : Prop := - ∀ {s : prog.State} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env} {bs : BasicStmt}, - EvalBasicStmt ρ₁ bs ρ₂ → interpV I vs ρ₁ → interpV I (E.eval s bs vs) ρ₂ +/-- Agda: `ValidStmtEvaluator`. -/ +class ValidStmtEvaluator [E : StmtEvaluator L prog] [LatticeInterpretation L] : + Prop where + valid : ∀ {s : prog.State} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env} + {bs : BasicStmt}, + EvalBasicStmt ρ₁ bs ρ₂ → interpV vs ρ₁ → interpV (E.eval s bs vs) ρ₂ end Spa diff --git a/lean/Spa/Analysis/Forward/Lattices.lean b/lean/Spa/Analysis/Forward/Lattices.lean index 0468bd9..3dae6c1 100644 --- a/lean/Spa/Analysis/Forward/Lattices.lean +++ b/lean/Spa/Analysis/Forward/Lattices.lean @@ -5,12 +5,13 @@ The Agda module instantiates `Lattice.FiniteMap` twice (variables ↦ abstract values, states ↦ variable maps) and re-exports everything with ᵛ/ᵐ suffixes. In Lean the two instantiations are `abbrev`s and the FiniteMap API is used directly; the module parameters (the finite-height lattice `L`, the program) -become section variables. +become section variables, with the finite-height structure and the lattice +interpretation arriving by instance resolution as in Agda. Correspondence: VariableValues, StateVariables ↦ VariableValues, StateVariables isLatticeᵛ/isLatticeᵐ, ⊔ᵛ, ≼ᵛ … ↦ (the FiniteMap Lattice instances) - fixedHeightᵛ ↦ varsFixedHeight + fixedHeightᵛ, fixedHeightᵐ ↦ (the FiniteMap FiniteHeightLattice instance) ⊥ᵛ, ⊥ᵛ-contains-bottoms ↦ botV, FiniteMap.bot_contains_bots states-in-Map ↦ states_memKey variablesAt ↦ variablesAt @@ -39,22 +40,9 @@ abbrev VariableValues : Type := FiniteMap String L prog.vars /-- Agda: `StateVariables`. -/ abbrev StateVariables : Type := FiniteMap prog.State (VariableValues L prog) prog.states -variable {h : ℕ} - -/-- Agda: `fixedHeightᵛ`. -/ -def varsFixedHeight (fhL : FixedHeight L h) : - FixedHeight (VariableValues L prog) (prog.vars.length * h) := - FiniteMap.fixedHeight fhL prog.vars - -/-- Agda: `⊥ᵛ`. -/ -def botV (fhL : FixedHeight L h) : VariableValues L prog := - (varsFixedHeight L prog fhL).bot - -/-- Agda: `fixedHeight` on `StateVariables` (assembled in `Forward.agda`'s -fixpoint call; named here for reuse). -/ -def statesFixedHeight (fhL : FixedHeight L h) : - FixedHeight (StateVariables L prog) (prog.states.length * (prog.vars.length * h)) := - FiniteMap.fixedHeight (varsFixedHeight L prog fhL) prog.states +/-- Agda: `⊥ᵛ` (the bottom of `fixedHeightᵛ`, now found by instance search). -/ +def botV [FiniteHeightLattice L] : VariableValues L prog := + FiniteHeightLattice.bot (VariableValues L prog) variable {L prog} @@ -81,16 +69,16 @@ theorem variablesAt_le {sv₁ sv₂ : StateVariables L prog} (hle : sv₁ ≤ sv FiniteMap.le_of_mem_mem prog.states_nodup hle (variablesAt_mem s sv₁) (variablesAt_mem s sv₂) -variable (fhL : FixedHeight L h) +variable [FiniteHeightLattice L] /-- Agda: `joinForKey`. -/ def joinForKey (k : prog.State) (sv : StateVariables L prog) : VariableValues L prog := - (sv.valuesAt (prog.incoming k)).foldr (· ⊔ ·) (botV L prog fhL) + (sv.valuesAt (prog.incoming k)).foldr (· ⊔ ·) (botV L prog) /-- Agda: `joinForKey-Mono`. -/ theorem joinForKey_mono (k : prog.State) : - Monotone (joinForKey fhL k) := by + Monotone (joinForKey (L := L) k) := by intro sv₁ sv₂ hle exact foldr_mono _ (FiniteMap.valuesAt_le hle (prog.incoming k)) (le_refl _) (fun b _ _ hab => sup_le_sup_right hab b) @@ -98,40 +86,42 @@ theorem joinForKey_mono (k : prog.State) : /-- Agda: `joinAll` (the "Exercise 4.26" generalized update with `f = id`). -/ def joinAll (sv : StateVariables L prog) : StateVariables L prog := - FiniteMap.generalizedUpdate id (joinForKey fhL) prog.states sv + FiniteMap.generalizedUpdate id joinForKey prog.states sv /-- Agda: `joinAll-Mono`. -/ -theorem joinAll_mono : Monotone (joinAll (prog := prog) fhL) := - FiniteMap.generalizedUpdate_monotone monotone_id (joinForKey_mono fhL) +theorem joinAll_mono : Monotone (joinAll (L := L) (prog := prog)) := + FiniteMap.generalizedUpdate_monotone monotone_id joinForKey_mono /-- Agda: `joinAll-k∈ks-≡`. -/ theorem joinAll_mem_eq {s : prog.State} {vs : VariableValues L prog} - {sv : StateVariables L prog} (h : (s, vs) ∈ joinAll fhL sv) : - vs = joinForKey fhL s sv := + {sv : StateVariables L prog} (h : (s, vs) ∈ joinAll sv) : + vs = joinForKey s sv := FiniteMap.generalizedUpdate_mem_eq (prog.states_complete s) h /-- Agda: `variablesAt-joinAll`. -/ theorem variablesAt_joinAll (s : prog.State) (sv : StateVariables L prog) : - variablesAt s (joinAll fhL sv) = joinForKey fhL s sv := - joinAll_mem_eq fhL (variablesAt_mem s (joinAll fhL sv)) + variablesAt s (joinAll sv) = joinForKey s sv := + joinAll_mem_eq (variablesAt_mem s (joinAll sv)) /-! ### Lifting an interpretation to variable maps -/ -variable (I : LatticeInterpretation L) +variable [I : LatticeInterpretation L] +omit [FiniteHeightLattice L] in /-- Agda: `⟦_⟧ᵛ`. -/ def interpV (vs : VariableValues L prog) (ρ : Env) : Prop := ∀ (k : String) (l : L), (k, l) ∈ vs → ∀ (v : Value), Env.Mem (k, v) ρ → I.interp l v /-- Agda: `⟦⊥ᵛ⟧ᵛ∅`. -/ -theorem interpV_botV_nil : interpV I (botV L prog fhL) [] := by +theorem interpV_botV_nil : interpV (botV L prog) [] := by intro k l _ v hmem cases hmem +omit [FiniteHeightLattice L] in /-- Agda: `⟦⟧ᵛ-⊔ᵛ-∨`. -/ theorem interpV_sup {vs₁ vs₂ : VariableValues L prog} {ρ : Env} - (h : interpV I vs₁ ρ ∨ interpV I vs₂ ρ) : interpV I (vs₁ ⊔ vs₂) ρ := by + (h : interpV vs₁ ρ ∨ interpV vs₂ ρ) : interpV (vs₁ ⊔ vs₂) ρ := by intro k l hmem v hv obtain ⟨l₁, l₂, rfl, h₁, h₂⟩ := FiniteMap.mem_sup hmem rcases h with h | h @@ -141,13 +131,13 @@ theorem interpV_sup {vs₁ vs₂ : VariableValues L prog} {ρ : Env} /-- Agda: `⟦⟧ᵛ-foldr`. -/ theorem interpV_foldr {vs : VariableValues L prog} {vss : List (VariableValues L prog)} {ρ : Env} - (hvs : interpV I vs ρ) (hmem : vs ∈ vss) : - interpV I (vss.foldr (· ⊔ ·) (botV L prog fhL)) ρ := by + (hvs : interpV vs ρ) (hmem : vs ∈ vss) : + interpV (vss.foldr (· ⊔ ·) (botV L prog)) ρ := by induction vss with | nil => cases hmem | cons vs' vss' ih => rcases List.mem_cons.mp hmem with rfl | hmem' - · exact interpV_sup I (Or.inl hvs) - · exact interpV_sup I (Or.inr (ih hmem')) + · exact interpV_sup (Or.inl hvs) + · exact interpV_sup (Or.inr (ih hmem')) end Spa diff --git a/lean/Spa/Analysis/Sign.lean b/lean/Spa/Analysis/Sign.lean index 8db44df..53e92e6 100644 --- a/lean/Spa/Analysis/Sign.lean +++ b/lean/Spa/Analysis/Sign.lean @@ -5,11 +5,13 @@ Correspondence: Sign (+ / - / 0ˢ) ↦ Sign.plus / Sign.minus / Sign.zero _≟ᵍ_, ≡-equiv, ≡-Decidable ↦ deriving DecidableEq SignLattice (AboveBelow) ↦ SignLattice - AB.Plain 0ˢ ↦ signFixedHeight (AboveBelow.plainFixedHeight .zero) + AB.Plain 0ˢ ↦ the AboveBelow FiniteHeightLattice instance, + seeded by `Inhabited Sign := ⟨.zero⟩` plus, minus ↦ plus, minus plus-Monoˡ/ʳ, minus-Monoˡ/ʳ (postulates in Agda!) ↦ plus_mono_left/right, minus_mono_left/right — - now actually proved, via AboveBelow.le_cases + now actually proved, via + AboveBelow.monotone₂_of_strict plus-Mono₂, minus-Mono₂ ↦ plus_mono₂, minus_mono₂ ⟦_⟧ᵍ ↦ interpSign ⟦⟧ᵍ-respects-≈ᵍ ↦ (trivial with `=`) @@ -41,15 +43,12 @@ instance : Showable Sign := | .minus => "-" | .zero => "0"⟩ -/-- Agda: the module parameter `x = 0ˢ` of `AB.Plain`. -/ +/-- Agda: the module parameter `x = 0ˢ` of `AB.Plain` (it seeds the +`FiniteHeightLattice (AboveBelow Sign)` instance). -/ instance : Inhabited Sign := ⟨.zero⟩ abbrev SignLattice : Type := AboveBelow Sign -/-- Agda: `AB.Plain 0ˢ`'s `fixedHeight`. -/ -def signFixedHeight : FixedHeight SignLattice 2 := - AboveBelow.plainFixedHeight Sign.zero - open AboveBelow in /-- Agda: `plus`. -/ def plus : SignLattice → SignLattice → SignLattice @@ -84,81 +83,39 @@ def minus : SignLattice → SignLattice → SignLattice | mk .zero, mk .minus => mk .plus | mk .zero, mk .zero => mk .zero +/-- Agda: `plus-Mono₂` (its components were postulates in Agda; `plus` is a +strict operation on the flat lattice, so monotonicity holds regardless of the +sign table). -/ +theorem 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)) + /-- Agda: `plus-Monoˡ` — a postulate there, a theorem here. -/ -theorem plus_mono_left (s₂ : SignLattice) : Monotone (plus · s₂) := by - intro a b h - rcases AboveBelow.le_cases h with rfl | rfl | rfl - · rcases s₂ with _ | _ | y <;> rcases b with _ | _ | x <;> - simp only [plus] <;> - first - | exact le_refl _ - | exact AboveBelow.le_top' _ - | exact AboveBelow.bot_le' _ - · rcases s₂ with _ | _ | y <;> rcases a with _ | _ | x <;> - simp only [plus] <;> - first - | exact le_refl _ - | exact AboveBelow.le_top' _ - · exact le_refl _ +theorem plus_mono_left (s₂ : SignLattice) : Monotone (plus · s₂) := plus_mono₂.1 s₂ /-- Agda: `plus-Monoʳ` — a postulate there, a theorem here. -/ -theorem plus_mono_right (s₁ : SignLattice) : Monotone (plus s₁) := by - intro a b h - rcases AboveBelow.le_cases h with rfl | rfl | rfl - · rcases s₁ with _ | _ | x <;> rcases b with _ | _ | y <;> - simp only [plus] <;> - first - | exact le_refl _ - | exact AboveBelow.le_top' _ - | exact AboveBelow.bot_le' _ - · rcases s₁ with _ | _ | x <;> rcases a with _ | _ | y <;> - simp only [plus] <;> - first - | exact le_refl _ - | exact AboveBelow.le_top' _ - · exact le_refl _ +theorem plus_mono_right (s₁ : SignLattice) : Monotone (plus s₁) := plus_mono₂.2 s₁ -/-- Agda: `plus-Mono₂`. -/ -theorem plus_mono₂ : Monotone₂ plus := - ⟨plus_mono_left, plus_mono_right⟩ +/-- Agda: `minus-Mono₂` (likewise from strictness of `minus`). -/ +theorem 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)) /-- Agda: `minus-Monoˡ` — a postulate there, a theorem here. -/ -theorem minus_mono_left (s₂ : SignLattice) : Monotone (minus · s₂) := by - intro a b h - rcases AboveBelow.le_cases h with rfl | rfl | rfl - · rcases s₂ with _ | _ | y <;> rcases b with _ | _ | x <;> - simp only [minus] <;> - first - | exact le_refl _ - | exact AboveBelow.le_top' _ - | exact AboveBelow.bot_le' _ - · rcases s₂ with _ | _ | y <;> rcases a with _ | _ | x <;> - simp only [minus] <;> - first - | exact le_refl _ - | exact AboveBelow.le_top' _ - · exact le_refl _ +theorem minus_mono_left (s₂ : SignLattice) : Monotone (minus · s₂) := minus_mono₂.1 s₂ /-- Agda: `minus-Monoʳ` — a postulate there, a theorem here. -/ -theorem minus_mono_right (s₁ : SignLattice) : Monotone (minus s₁) := by - intro a b h - rcases AboveBelow.le_cases h with rfl | rfl | rfl - · rcases s₁ with _ | _ | x <;> rcases b with _ | _ | y <;> - simp only [minus] <;> - first - | exact le_refl _ - | exact AboveBelow.le_top' _ - | exact AboveBelow.bot_le' _ - · rcases s₁ with _ | _ | x <;> rcases a with _ | _ | y <;> - simp only [minus] <;> - first - | exact le_refl _ - | exact AboveBelow.le_top' _ - · exact le_refl _ - -/-- Agda: `minus-Mono₂`. -/ -theorem minus_mono₂ : Monotone₂ minus := - ⟨minus_mono_left, minus_mono_right⟩ +theorem minus_mono_right (s₁ : SignLattice) : Monotone (minus s₁) := minus_mono₂.2 s₁ /-- Agda: `⟦_⟧ᵍ`. -/ def interpSign : SignLattice → Value → Prop @@ -197,48 +154,18 @@ theorem interpSign_mk_disjoint {s₁ s₂ : Sign} (hne : s₁ ≠ s₂) {v : Val injection hv with hz omega -/-- Agda: `⟦⟧ᵍ-⊔ᵍ-∨`. -/ +/-- Agda: `⟦⟧ᵍ-⊔ᵍ-∨` (via the factored flat-lattice lemma). -/ theorem interpSign_sup {s₁ s₂ : SignLattice} (v : Value) - (h : interpSign s₁ v ∨ interpSign s₂ v) : interpSign (s₁ ⊔ s₂) v := by - rcases s₁ with _ | _ | x - · rcases h with h | h - · exact h.elim - · rw [AboveBelow.bot_sup] - exact h - · exact trivial - · rcases s₂ with _ | _ | y - · rcases h with h | h - · rw [AboveBelow.sup_bot] - exact h - · exact h.elim - · rw [AboveBelow.sup_top] - exact trivial - · by_cases hxy : x = y - · subst hxy - rw [AboveBelow.mk_sup_mk, if_pos rfl] - rcases h with h | h <;> exact h - · rw [AboveBelow.mk_sup_mk, if_neg hxy] - exact trivial + (h : interpSign s₁ v ∨ interpSign s₂ v) : interpSign (s₁ ⊔ s₂) v := + AboveBelow.interp_sup_of (fun _ h => h) (fun _ => trivial) v h -/-- Agda: `⟦⟧ᵍ-⊓ᵍ-∧`. -/ +/-- Agda: `⟦⟧ᵍ-⊓ᵍ-∧` (via the factored flat-lattice lemma). -/ theorem interpSign_inf {s₁ s₂ : SignLattice} (v : Value) - (h : interpSign s₁ v ∧ interpSign s₂ v) : interpSign (s₁ ⊓ s₂) v := by - rcases s₁ with _ | _ | x - · exact h.1 - · rw [AboveBelow.top_inf] - exact h.2 - · rcases s₂ with _ | _ | y - · exact h.2 - · rw [AboveBelow.inf_top] - exact h.1 - · by_cases hxy : x = y - · subst hxy - rw [AboveBelow.mk_inf_mk, if_pos rfl] - exact h.1 - · exact absurd h (interpSign_mk_disjoint hxy) + (h : interpSign s₁ v ∧ interpSign s₂ v) : interpSign (s₁ ⊓ s₂) v := + AboveBelow.interp_inf_of (fun hne _ => interpSign_mk_disjoint hne) v h -/-- Agda: `latticeInterpretationᵍ`. -/ -def signInterpretation : LatticeInterpretation SignLattice where +/-- Agda: `latticeInterpretationᵍ` (an instance there too). -/ +instance signInterpretation : LatticeInterpretation SignLattice where interp := interpSign interp_sup := fun {l₁ l₂} v h => interpSign_sup (s₁ := l₁) (s₂ := l₂) v h interp_inf := fun {l₁ l₂} v h => interpSign_inf (s₁ := l₁) (s₂ := l₂) v h @@ -282,12 +209,12 @@ theorem eval_mono (e : Expr) : Monotone (eval prog e) := by cases n <;> exact le_refl _ /-- Agda: the `SignEval` instance. -/ -def exprEvaluator : ExprEvaluator SignLattice prog := +instance exprEvaluator : ExprEvaluator SignLattice prog := ⟨eval prog, eval_mono prog⟩ /-- Agda: `WithProg.result`/`output` — the analysis result, printed. -/ def output : String := - show' (result signFixedHeight (exprEvaluator prog).toStmtEvaluator) + show' (result SignLattice prog) /-- Agda: `plus-valid`. -/ theorem plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ} @@ -365,9 +292,9 @@ theorem minus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ} subst h₂ omega -/-- Agda: `eval-valid` / `SignEvalValid`. -/ -theorem eval_valid : - IsValidExprEvaluator (exprEvaluator prog) signInterpretation := by +/-- Agda: `eval-valid` / the `SignEvalValid` instance. -/ +instance eval_valid : ValidExprEvaluator SignLattice prog := by + constructor intro vs ρ e v hev induction hev with | num n => @@ -400,11 +327,8 @@ theorem eval_valid : /-- Agda: `WithProg.analyze-correct`. -/ theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : - interpV signInterpretation - (variablesAt prog.finalState - (result signFixedHeight (exprEvaluator prog).toStmtEvaluator)) ρ := - Spa.analyze_correct signFixedHeight - ((exprEvaluator prog).toStmtEvaluator_valid (eval_valid prog)) hrun + interpV (variablesAt prog.finalState (result SignLattice prog)) ρ := + Spa.analyze_correct SignLattice prog hrun end SignAnalysis diff --git a/lean/Spa/Fixedpoint.lean b/lean/Spa/Fixedpoint.lean index 6fd9771..8c282dd 100644 --- a/lean/Spa/Fixedpoint.lean +++ b/lean/Spa/Fixedpoint.lean @@ -7,6 +7,10 @@ steps, or we would build a `<`-chain longer than the longest one. We deliberately do *not* use mathlib's `OrderHom.lfp` (different proof approach, and not computable). +As in Agda — where the module took `{{flA : IsFiniteHeightLattice A h …}}` — +the finite-height structure arrives by instance resolution +(`[FiniteHeightLattice α]`); only `f` and its monotonicity are explicit. + Correspondence: doStep ↦ Spa.Fixedpoint.doStep (the chain argument now carries `a₁ = ⊥` and its length in the @@ -21,55 +25,58 @@ import Spa.Lattice namespace Spa.Fixedpoint -variable {α : Type*} [Lattice α] [DecidableEq α] {h : ℕ} +open FiniteHeightLattice (height fixedHeight) + +variable {α : Type*} [Lattice α] [DecidableEq α] [FiniteHeightLattice α] /-- Agda: `doStep`. `g` is gas; the invariant `c.length + g = h + 1` guarantees that when gas runs out the chain contradicts boundedness. -/ -def doStep (fh : FixedHeight α h) (f : α → α) (hf : Monotone f) : - ∀ (g : ℕ) (c : LTSeries α), c.length + g = h + 1 → +def doStep (f : α → α) (hf : Monotone f) : + ∀ (g : ℕ) (c : LTSeries α), c.length + g = height (α := α) + 1 → c.last ≤ f c.last → {a : α // a = f a} | 0, c, hlen, _ => - absurd (fh.bounded c) (by omega) + absurd ((fixedHeight (α := α)).bounded c) (by omega) | g + 1, c, hlen, hle => if heq : c.last = f c.last then ⟨c.last, heq⟩ else - doStep fh f hf g (c.snoc (f c.last) (lt_of_le_of_ne hle heq)) + doStep f hf g (c.snoc (f c.last) (lt_of_le_of_ne hle heq)) (by simp [RelSeries.snoc]; omega) (by rw [RelSeries.last_snoc]; exact hf hle) /-- Agda: `fix`. Start iterating from `⊥`. -/ -def fix (fh : FixedHeight α h) (f : α → α) (hf : Monotone f) : {a : α // a = f a} := - doStep fh f hf (h + 1) (RelSeries.singleton _ fh.bot) +def fix (f : α → α) (hf : Monotone f) : {a : α // a = f a} := + doStep f hf (height (α := α) + 1) (RelSeries.singleton _ (FiniteHeightLattice.bot α)) (by simp) - (by simpa [RelSeries.last_singleton] using fh.bot_le (f fh.bot)) + (by simpa [RelSeries.last_singleton] + using FiniteHeightLattice.bot_le α (f (FiniteHeightLattice.bot α))) /-- Agda: `aᶠ`. -/ -def aFix (fh : FixedHeight α h) (f : α → α) (hf : Monotone f) : α := - (fix fh f hf).1 +def aFix (f : α → α) (hf : Monotone f) : α := + (fix f hf).1 /-- Agda: `aᶠ≈faᶠ`. -/ -theorem aFix_eq (fh : FixedHeight α h) (f : α → α) (hf : Monotone f) : - aFix fh f hf = f (aFix fh f hf) := - (fix fh f hf).2 +theorem aFix_eq (f : α → α) (hf : Monotone f) : + aFix f hf = f (aFix f hf) := + (fix f hf).2 /-- Agda: `stepPreservesLess` — iteration stays below any fixed point. -/ -theorem doStep_le (fh : FixedHeight α h) (f : α → α) (hf : Monotone f) +theorem doStep_le (f : α → α) (hf : Monotone f) {b : α} (hb : b = f b) : - ∀ (g : ℕ) (c : LTSeries α) (hlen : c.length + g = h + 1) + ∀ (g : ℕ) (c : LTSeries α) (hlen : c.length + g = height (α := α) + 1) (hle : c.last ≤ f c.last), c.last ≤ b → - (doStep fh f hf g c hlen hle : α) ≤ b - | 0, c, hlen, _ => fun _ => absurd (fh.bounded c) (by omega) + (doStep f hf g c hlen hle : α) ≤ b + | 0, c, hlen, _ => fun _ => absurd ((fixedHeight (α := α)).bounded c) (by omega) | g + 1, c, hlen, hle => fun hcb => by rw [doStep] split · exact hcb - · exact doStep_le fh f hf hb g _ _ _ + · exact doStep_le f hf hb g _ _ _ (by rw [RelSeries.last_snoc]; exact le_of_le_of_eq (hf hcb) hb.symm) /-- Agda: `aᶠ≼` — `aFix` is below every fixed point of `f`. -/ -theorem aFix_le (fh : FixedHeight α h) (f : α → α) (hf : Monotone f) - {a : α} (ha : a = f a) : aFix fh f hf ≤ a := - doStep_le fh f hf ha _ _ _ _ (by simpa using fh.bot_le a) +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) end Spa.Fixedpoint diff --git a/lean/Spa/Language/Semantics.lean b/lean/Spa/Language/Semantics.lean index b9ccf92..f849885 100644 --- a/lean/Spa/Language/Semantics.lean +++ b/lean/Spa/Language/Semantics.lean @@ -79,8 +79,9 @@ inductive EvalStmt : Env → Stmt → Env → Prop EvalExpr ρ e (.int 0) → EvalStmt ρ (.whileLoop e s) ρ -/-- Agda: `LatticeInterpretation`. -/ -structure LatticeInterpretation (L : Type*) [Lattice L] where +/-- Agda: `LatticeInterpretation` (used there as an instance argument `⦃·⦄`, +hence a typeclass here). -/ +class LatticeInterpretation (L : Type*) [Lattice L] where interp : L → Value → Prop interp_sup : ∀ {l₁ l₂ : L} (v : Value), interp l₁ v ∨ interp l₂ v → interp (l₁ ⊔ l₂) v diff --git a/lean/Spa/Lattice.lean b/lean/Spa/Lattice.lean index 3ddb9a3..f6beae5 100644 --- a/lean/Spa/Lattice.lean +++ b/lean/Spa/Lattice.lean @@ -118,7 +118,10 @@ def FixedHeight.cast {α : Type*} [Preorder α] {m n : ℕ} (h : m = n) @[simp] theorem FixedHeight.cast_bot {α : Type*} [Preorder α] {m n : ℕ} (h : m = n) (fh : FixedHeight α m) : (fh.cast h).bot = fh.bot := rfl -/-- Agda: `IsFiniteHeightLattice` / `FiniteHeightLattice` (bundled). -/ +/-- Agda: `IsFiniteHeightLattice` / `FiniteHeightLattice` (bundled). Like the +Agda code (which took `IsFiniteHeightLattice` as an instance argument `⦃·⦄`), +this is a typeclass; downstream modules pick it up by instance resolution +rather than threading a `FixedHeight` value. -/ class FiniteHeightLattice (α : Type*) [Lattice α] where height : ℕ fixedHeight : FixedHeight α height @@ -150,4 +153,16 @@ theorem bot_le (fh : FixedHeight α h) : fh.KnownBot := by end FixedHeight +namespace FiniteHeightLattice + +variable (α : Type*) [Lattice α] [FiniteHeightLattice α] + +/-- Agda: the `⊥` of `Chain.Height`, with the type explicit. -/ +def bot : α := (fixedHeight (α := α)).bot + +/-- Agda: `⊥≼` for the instance bottom. -/ +theorem bot_le (a : α) : bot α ≤ a := FixedHeight.bot_le _ a + +end FiniteHeightLattice + end Spa diff --git a/lean/Spa/Lattice/AboveBelow.lean b/lean/Spa/Lattice/AboveBelow.lean index db0a11d..1f2b585 100644 --- a/lean/Spa/Lattice/AboveBelow.lean +++ b/lean/Spa/Lattice/AboveBelow.lean @@ -155,6 +155,75 @@ theorem le_cases {a b : AboveBelow α} (h : a ≤ b) : · rw [if_neg hxy] at hsup exact absurd hsup (by simp) +/-- Monotonicity for *strict* operations on flat lattices: if `f` sends `⊥` to +`⊥` (in either argument) and `⊤` to `⊤` (against any non-`⊥` argument), it is +monotone in both arguments — regardless of its values on plain elements. +`Analysis/Sign.agda` and `Analysis/Constant.agda` postulated exactly these +monotonicity facts for their `plus`/`minus`, all of which have this shape. -/ +theorem monotone₂_of_strict {β γ : Type*} [DecidableEq β] [DecidableEq γ] + (f : AboveBelow α → AboveBelow β → AboveBelow γ) + (hbotl : ∀ y, f bot y = bot) (hbotr : ∀ x, f x bot = bot) + (htopl : ∀ y, y ≠ bot → f top y = top) + (htopr : ∀ x, x ≠ bot → f x top = top) : Monotone₂ f := by + constructor + · intro 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 + 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 + +The `⟦⟧-⊔-∨` / `⟦⟧-⊓-∧` proofs of `Analysis/Sign.agda` and +`Analysis/Constant.agda` are the same case analysis; only the meaning of the +plain elements differs. Factored here, they need just `P ⊥ ↦ False`, +`P ⊤ ↦ True`, and (for `⊓`) disjointness of distinct plain elements. -/ + +section Interp + +variable {V : Type*} {P : AboveBelow α → V → Prop} + +/-- Agda: `⟦⟧ᵍ-⊔ᵍ-∨` / `⟦⟧ᶜ-⊔ᶜ-∨`, generalized. -/ +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 + +/-- Agda: `⟦⟧ᵍ-⊓ᵍ-∧` / `⟦⟧ᶜ-⊓ᶜ-∧`, generalized. -/ +theorem interp_inf_of + (hdisj : ∀ {x y : α}, x ≠ y → ∀ v, ¬(P (mk x) v ∧ P (mk y) v)) + {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∧ P s₂ v) : P (s₁ ⊓ s₂) v := by + rcases s₁ with _ | _ | x + · 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) + +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 α → ℕ diff --git a/lean/Spa/Lattice/FiniteMap.lean b/lean/Spa/Lattice/FiniteMap.lean index 50c0209..23b345b 100644 --- a/lean/Spa/Lattice/FiniteMap.lean +++ b/lean/Spa/Lattice/FiniteMap.lean @@ -639,6 +639,12 @@ def fixedHeight {hB : ℕ} (fhB : FixedHeight B hB) (ks : List A) : (ofIter ks) toIter (ofIter_monotone ks) toIter_monotone (toIter_ofIter ks) (fun fm => ofIter_toIter fm)).cast (by ring) +/-- Agda: `isFiniteHeightLattice`/`finiteHeightLattice` of `Lattice/FiniteMap.agda` +(there instance arguments; here an instance). -/ +instance [IB : FiniteHeightLattice B] : FiniteHeightLattice (FiniteMap A B ks) where + height := ks.length * IB.height + fixedHeight := fixedHeight IB.fixedHeight ks + omit [Lattice B] in /-- Agda: `to-build`. -/ theorem mem_ofIter_build {b : B} : ∀ {ks : List A} {k : A} {v : B},