From a82d54666a8cae6a914a8faca3fdf743a7c53771 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Tue, 9 Jun 2026 20:52:08 -0700 Subject: [PATCH] Lean migration: Phase 7 (Sign + Constant analyses, executable) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - 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 --- LEAN_MIGRATION.md | 2 +- lean/Main.lean | 40 +++ lean/Spa.lean | 4 + lean/Spa/Analysis/Constant.lean | 311 +++++++++++++++++++++++ lean/Spa/Analysis/Sign.lean | 411 +++++++++++++++++++++++++++++++ lean/Spa/Analysis/Utils.lean | 15 ++ lean/Spa/Lattice/AboveBelow.lean | 21 ++ lean/Spa/Showable.lean | 47 ++++ lean/lakefile.toml | 4 + 9 files changed, 854 insertions(+), 1 deletion(-) create mode 100644 lean/Main.lean create mode 100644 lean/Spa/Analysis/Constant.lean create mode 100644 lean/Spa/Analysis/Sign.lean create mode 100644 lean/Spa/Analysis/Utils.lean create mode 100644 lean/Spa/Showable.lean diff --git a/LEAN_MIGRATION.md b/LEAN_MIGRATION.md index a19d755..fee90d8 100644 --- a/LEAN_MIGRATION.md +++ b/LEAN_MIGRATION.md @@ -80,4 +80,4 @@ validate phase by phase. - [x] Phase 4 - [x] Phase 5 - [x] Phase 6 -- [ ] Phase 7 +- [x] Phase 7 diff --git a/lean/Main.lean b/lean/Main.lean new file mode 100644 index 0000000..298a365 --- /dev/null +++ b/lean/Main.lean @@ -0,0 +1,40 @@ +/- +Port of `Main.agda`. Prints the constant- and sign-analysis results for the +test program (Agda: `putStrLn (output-Const ++ "\n" ++ output-Sign)`). +-/ +import Spa.Analysis.Sign +import Spa.Analysis.Constant + +namespace Spa + +/-- Agda: `testCode`. -/ +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")))))) + +/-- Agda: `testCodeCond₁`. -/ +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))))) + +/-- Agda: `testCodeCond₂`. -/ +def testCodeCond₂ : Stmt := + .andThen (.basic (.assign "var" (.num 1))) + (.ifElse (.var "var") + (.basic (.assign "x" (.num 1))) + (.basic .noop)) + +/-- Agda: `testProgram`. -/ +def testProgram : Program := ⟨testCode⟩ + +end Spa + +/-- Agda: `main`. -/ +def main : IO Unit := + IO.println (Spa.ConstAnalysis.output Spa.testProgram ++ "\n" ++ + Spa.SignAnalysis.output Spa.testProgram) diff --git a/lean/Spa.lean b/lean/Spa.lean index 2d83cf6..528a9d0 100644 --- a/lean/Spa.lean +++ b/lean/Spa.lean @@ -16,3 +16,7 @@ import Spa.Analysis.Forward.Lattices import Spa.Analysis.Forward.Evaluation import Spa.Analysis.Forward.Adapters import Spa.Analysis.Forward +import Spa.Showable +import Spa.Analysis.Utils +import Spa.Analysis.Sign +import Spa.Analysis.Constant diff --git a/lean/Spa/Analysis/Constant.lean b/lean/Spa/Analysis/Constant.lean new file mode 100644 index 0000000..dd13650 --- /dev/null +++ b/lean/Spa/Analysis/Constant.lean @@ -0,0 +1,311 @@ +/- +Port of `Analysis/Constant.agda`. + +Correspondence: + showable, ≡-equiv, ≡-Decidable-ℤ ↦ (mathlib/derived instances) + ConstLattice (AboveBelow ℤ) ↦ ConstLattice + AB.Plain (+ 0) ↦ constFixedHeight + 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 + plus-Mono₂, minus-Mono₂ ↦ plus_mono₂, minus_mono₂ + ⟦_⟧ᶜ ↦ interpConst + ⟦⟧ᶜ-respects-≈ᶜ ↦ (trivial with `=`) + ⟦⟧ᶜ-⊔ᶜ-∨, ⟦⟧ᶜ-⊓ᶜ-∧ ↦ interpConst_sup, interpConst_inf + s₁≢s₂⇒¬s₁∧s₂ ↦ interpConst_mk_disjoint + latticeInterpretationᶜ ↦ constInterpretation + WithProg.eval, eval-Monoʳ ↦ ConstAnalysis.eval, eval_mono + ConstEval ↦ ConstAnalysis.exprEvaluator + plus-valid, minus-valid ↦ plus_valid, minus_valid + eval-valid, ConstEvalValid ↦ eval_valid + output ↦ ConstAnalysis.output + analyze-correct ↦ ConstAnalysis.analyze_correct +-/ +import Spa.Analysis.Forward +import Spa.Analysis.Utils +import Spa.Showable + +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 +/-- Agda: `plus`. -/ +def plus : ConstLattice → ConstLattice → ConstLattice + | bot, _ => bot + | _, bot => bot + | top, _ => top + | _, top => top + | mk z₁, mk z₂ => mk (z₁ + z₂) + +open AboveBelow in +/-- Agda: `minus`. -/ +def minus : ConstLattice → ConstLattice → ConstLattice + | bot, _ => bot + | _, bot => bot + | top, _ => top + | _, top => top + | mk z₁, mk z₂ => mk (z₁ - z₂) + +/-- 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 _ + +/-- 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 _ + +/-- Agda: `plus-Mono₂`. -/ +theorem plus_mono₂ : Monotone₂ plus := + ⟨plus_mono_left, plus_mono_right⟩ + +/-- 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 _ + +/-- 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⟩ + +/-- Agda: `⟦_⟧ᶜ`. -/ +def interpConst : ConstLattice → Value → Prop + | .bot, _ => False + | .top, _ => True + | .mk z, v => v = .int z + +/-- Agda: `s₁≢s₂⇒¬s₁∧s₂`. -/ +theorem interpConst_mk_disjoint {z₁ z₂ : ℤ} (hne : z₁ ≠ z₂) {v : Value} : + ¬(interpConst (.mk z₁) v ∧ interpConst (.mk z₂) v) := by + rintro ⟨h₁, h₂⟩ + rw [h₁] at h₂ + injection h₂ with hz + exact hne hz + +/-- Agda: `⟦⟧ᶜ-⊔ᶜ-∨`. -/ +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 + +/-- Agda: `⟦⟧ᶜ-⊓ᶜ-∧`. -/ +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) + +/-- Agda: `latticeInterpretationᶜ`. -/ +def 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 + +variable (prog : Program) + +/-- Agda: `WithProg.eval`. -/ +def eval : Expr → VariableValues ConstLattice prog → ConstLattice + | .add e₁ e₂, vs => plus (eval e₁ vs) (eval e₂ vs) + | .sub e₁ e₂, vs => minus (eval e₁ vs) (eval e₂ vs) + | .var k, vs => + if h : FiniteMap.MemKey k vs then (FiniteMap.locate h).1 else .top + | .num n, _ => .mk n + +/-- Agda: `WithProg.eval-Monoʳ`. -/ +theorem eval_mono (e : Expr) : Monotone (eval prog e) := by + induction e with + | add e₁ e₂ ih₁ ih₂ => + intro vs₁ vs₂ h + exact eval_combine₂ plus_mono₂ (ih₁ h) (ih₂ h) + | sub e₁ e₂ ih₁ ih₂ => + intro vs₁ vs₂ h + exact eval_combine₂ minus_mono₂ (ih₁ h) (ih₂ h) + | var k => + 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)] + 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))] + | num n => + intro vs₁ vs₂ _ + exact le_refl _ + +/-- Agda: the `ConstEval` instance. -/ +def exprEvaluator : ExprEvaluator ConstLattice prog := + ⟨eval prog, eval_mono prog⟩ + +/-- Agda: `WithProg.result`/`output`. -/ +def output : String := + show' (result constFixedHeight (exprEvaluator prog).toStmtEvaluator) + +/-- Agda: `plus-valid`. -/ +theorem plus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ} + (h₁ : interpConst g₁ (.int z₁)) (h₂ : interpConst g₂ (.int z₂)) : + interpConst (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₂] + +/-- Agda: `minus-valid`. -/ +theorem minus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ} + (h₁ : interpConst g₁ (.int z₁)) (h₂ : interpConst g₂ (.int z₂)) : + interpConst (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₂] + +/-- Agda: `eval-valid` / `ConstEvalValid`. -/ +theorem eval_valid : + IsValidExprEvaluator (exprEvaluator prog) constInterpretation := by + intro vs ρ e v hev + induction hev with + | num n => + intro _ + show interpConst (eval prog (.num n) vs) (.int n) + rfl + | var x v hxv => + intro hvs + show interpConst (eval prog (.var x) vs) v + simp only [eval] + by_cases hk : FiniteMap.MemKey x vs + · rw [dif_pos hk] + exact hvs _ _ (FiniteMap.locate hk).2 _ hxv + · rw [dif_neg hk] + exact trivial + | add e₁ e₂ z₁ z₂ _ _ ih₁ ih₂ => + intro hvs + have h₁ : interpConst (eval prog e₁ vs) (.int z₁) := ih₁ hvs + have h₂ : interpConst (eval prog e₂ vs) (.int z₂) := ih₂ hvs + show interpConst (eval prog (.add e₁ e₂) vs) (.int (z₁ + z₂)) + exact plus_valid h₁ h₂ + | sub e₁ e₂ z₁ z₂ _ _ ih₁ ih₂ => + intro hvs + have h₁ : interpConst (eval prog e₁ vs) (.int z₁) := ih₁ hvs + have h₂ : interpConst (eval prog e₂ vs) (.int z₂) := ih₂ hvs + show interpConst (eval prog (.sub e₁ e₂) vs) (.int (z₁ - z₂)) + exact minus_valid h₁ h₂ + +/-- 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 + +end ConstAnalysis + +end Spa diff --git a/lean/Spa/Analysis/Sign.lean b/lean/Spa/Analysis/Sign.lean new file mode 100644 index 0000000..8db44df --- /dev/null +++ b/lean/Spa/Analysis/Sign.lean @@ -0,0 +1,411 @@ +/- +Port of `Analysis/Sign.agda`. + +Correspondence: + Sign (+ / - / 0ˢ) ↦ Sign.plus / Sign.minus / Sign.zero + _≟ᵍ_, ≡-equiv, ≡-Decidable ↦ deriving DecidableEq + SignLattice (AboveBelow) ↦ SignLattice + AB.Plain 0ˢ ↦ signFixedHeight (AboveBelow.plainFixedHeight .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 + plus-Mono₂, minus-Mono₂ ↦ plus_mono₂, minus_mono₂ + ⟦_⟧ᵍ ↦ interpSign + ⟦⟧ᵍ-respects-≈ᵍ ↦ (trivial with `=`) + ⟦⟧ᵍ-⊔ᵍ-∨, ⟦⟧ᵍ-⊓ᵍ-∧ ↦ interpSign_sup, interpSign_inf + s₁≢s₂⇒¬s₁∧s₂ ↦ interpSign_mk_disjoint + latticeInterpretationᵍ ↦ signInterpretation + WithProg.eval, eval-Monoʳ ↦ SignAnalysis.eval, eval_mono + SignEval (instance) ↦ SignAnalysis.exprEvaluator + plus-valid, minus-valid ↦ plus_valid, minus_valid + eval-valid, SignEvalValid ↦ eval_valid + output ↦ SignAnalysis.output + analyze-correct ↦ SignAnalysis.analyze_correct +-/ +import Spa.Analysis.Forward +import Spa.Analysis.Utils +import Spa.Showable + +namespace Spa + +inductive Sign where + | plus + | minus + | zero + deriving DecidableEq + +instance : Showable Sign := + ⟨fun + | .plus => "+" + | .minus => "-" + | .zero => "0"⟩ + +/-- Agda: the module parameter `x = 0ˢ` of `AB.Plain`. -/ +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 + | bot, _ => bot + | _, bot => bot + | top, _ => top + | _, top => top + | mk .plus, mk .plus => mk .plus + | mk .plus, mk .minus => top + | mk .plus, mk .zero => mk .plus + | mk .minus, mk .plus => top + | mk .minus, mk .minus => mk .minus + | mk .minus, mk .zero => mk .minus + | mk .zero, mk .plus => mk .plus + | mk .zero, mk .minus => mk .minus + | mk .zero, mk .zero => mk .zero + +open AboveBelow in +/-- Agda: `minus`. -/ +def minus : SignLattice → SignLattice → SignLattice + | bot, _ => bot + | _, bot => bot + | top, _ => top + | _, top => top + | mk .plus, mk .plus => top + | mk .plus, mk .minus => mk .plus + | mk .plus, mk .zero => mk .plus + | mk .minus, mk .plus => mk .minus + | mk .minus, mk .minus => top + | mk .minus, mk .zero => mk .minus + | mk .zero, mk .plus => mk .minus + | mk .zero, mk .minus => mk .plus + | mk .zero, mk .zero => mk .zero + +/-- 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 _ + +/-- 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 _ + +/-- Agda: `plus-Mono₂`. -/ +theorem plus_mono₂ : Monotone₂ plus := + ⟨plus_mono_left, plus_mono_right⟩ + +/-- 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 _ + +/-- 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⟩ + +/-- Agda: `⟦_⟧ᵍ`. -/ +def interpSign : SignLattice → Value → Prop + | .bot, _ => False + | .top, _ => True + | .mk .plus, v => ∃ n : ℕ, v = .int (n + 1) + | .mk .zero, v => v = .int 0 + | .mk .minus, v => ∃ n : ℕ, v = .int (-(n + 1)) + +/-- Agda: `s₁≢s₂⇒¬s₁∧s₂`. -/ +theorem interpSign_mk_disjoint {s₁ s₂ : Sign} (hne : s₁ ≠ s₂) {v : Value} : + ¬(interpSign (.mk s₁) v ∧ interpSign (.mk s₂) v) := by + rintro ⟨h₁, h₂⟩ + rcases s₁ <;> rcases s₂ <;> try exact hne rfl + all_goals simp only [interpSign] at h₁ h₂ + · obtain ⟨n₁, rfl⟩ := h₁ + obtain ⟨n₂, hv⟩ := h₂ + injection hv with hz + omega + · obtain ⟨n₁, rfl⟩ := h₁ + injection h₂ with hz + omega + · obtain ⟨n₁, rfl⟩ := h₁ + obtain ⟨n₂, hv⟩ := h₂ + injection hv with hz + omega + · obtain ⟨n₁, rfl⟩ := h₁ + injection h₂ with hz + omega + · subst h₁ + obtain ⟨n₂, hv⟩ := h₂ + injection hv with hz + omega + · subst h₁ + obtain ⟨n₂, hv⟩ := h₂ + injection hv with hz + omega + +/-- Agda: `⟦⟧ᵍ-⊔ᵍ-∨`. -/ +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 + +/-- Agda: `⟦⟧ᵍ-⊓ᵍ-∧`. -/ +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) + +/-- Agda: `latticeInterpretationᵍ`. -/ +def 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 + +namespace SignAnalysis + +/-! Agda: `module WithProg (prog : Program)`. -/ + +variable (prog : Program) + +/-- Agda: `WithProg.eval`. -/ +def eval : Expr → VariableValues SignLattice prog → SignLattice + | .add e₁ e₂, vs => plus (eval e₁ vs) (eval e₂ vs) + | .sub e₁ e₂, vs => minus (eval e₁ vs) (eval e₂ vs) + | .var k, vs => + if h : FiniteMap.MemKey k vs then (FiniteMap.locate h).1 else .top + | .num 0, _ => .mk .zero + | .num (_ + 1), _ => .mk .plus + +/-- Agda: `WithProg.eval-Monoʳ`. -/ +theorem eval_mono (e : Expr) : Monotone (eval prog e) := by + induction e with + | add e₁ e₂ ih₁ ih₂ => + intro vs₁ vs₂ h + exact eval_combine₂ plus_mono₂ (ih₁ h) (ih₂ h) + | sub e₁ e₂ ih₁ ih₂ => + intro vs₁ vs₂ h + exact eval_combine₂ minus_mono₂ (ih₁ h) (ih₂ h) + | var k => + 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)] + 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))] + | num n => + intro vs₁ vs₂ _ + cases n <;> exact le_refl _ + +/-- Agda: the `SignEval` instance. -/ +def 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) + +/-- Agda: `plus-valid`. -/ +theorem plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ} + (h₁ : interpSign g₁ (.int z₁)) (h₂ : interpSign g₂ (.int z₂)) : + interpSign (plus g₁ g₂) (.int (z₁ + z₂)) := by + rcases g₁ with _ | _ | s₁ + · exact h₁.elim + · rcases g₂ with _ | _ | s₂ + · exact h₂.elim + · exact trivial + · exact trivial + · rcases g₂ with _ | _ | s₂ + · exact h₂.elim + · rcases s₁ <;> exact trivial + · rcases s₁ <;> rcases s₂ <;> + simp only [plus, interpSign, Value.int.injEq] at h₁ h₂ ⊢ <;> + try trivial + · obtain ⟨n₁, rfl⟩ := h₁ + obtain ⟨n₂, rfl⟩ := h₂ + exact ⟨n₁ + n₂ + 1, by omega⟩ + · obtain ⟨n₁, rfl⟩ := h₁ + subst h₂ + exact ⟨n₁, by omega⟩ + · obtain ⟨n₁, rfl⟩ := h₁ + obtain ⟨n₂, rfl⟩ := h₂ + exact ⟨n₁ + n₂ + 1, by omega⟩ + · obtain ⟨n₁, rfl⟩ := h₁ + subst h₂ + exact ⟨n₁, by omega⟩ + · subst h₁ + obtain ⟨n₂, rfl⟩ := h₂ + exact ⟨n₂, by omega⟩ + · subst h₁ + obtain ⟨n₂, rfl⟩ := h₂ + exact ⟨n₂, by omega⟩ + · subst h₁ + subst h₂ + omega + +/-- Agda: `minus-valid`. -/ +theorem minus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ} + (h₁ : interpSign g₁ (.int z₁)) (h₂ : interpSign g₂ (.int z₂)) : + interpSign (minus g₁ g₂) (.int (z₁ - z₂)) := by + rcases g₁ with _ | _ | s₁ + · exact h₁.elim + · rcases g₂ with _ | _ | s₂ + · exact h₂.elim + · exact trivial + · exact trivial + · rcases g₂ with _ | _ | s₂ + · exact h₂.elim + · rcases s₁ <;> exact trivial + · rcases s₁ <;> rcases s₂ <;> + simp only [minus, interpSign, Value.int.injEq] at h₁ h₂ ⊢ <;> + try trivial + · obtain ⟨n₁, rfl⟩ := h₁ + obtain ⟨n₂, rfl⟩ := h₂ + exact ⟨n₁ + n₂ + 1, by omega⟩ + · obtain ⟨n₁, rfl⟩ := h₁ + subst h₂ + exact ⟨n₁, by omega⟩ + · obtain ⟨n₁, rfl⟩ := h₁ + obtain ⟨n₂, rfl⟩ := h₂ + exact ⟨n₁ + n₂ + 1, by omega⟩ + · obtain ⟨n₁, rfl⟩ := h₁ + subst h₂ + exact ⟨n₁, by omega⟩ + · subst h₁ + obtain ⟨n₂, rfl⟩ := h₂ + exact ⟨n₂, by omega⟩ + · subst h₁ + obtain ⟨n₂, rfl⟩ := h₂ + exact ⟨n₂, by omega⟩ + · subst h₁ + subst h₂ + omega + +/-- Agda: `eval-valid` / `SignEvalValid`. -/ +theorem eval_valid : + IsValidExprEvaluator (exprEvaluator prog) signInterpretation := by + intro vs ρ e v hev + induction hev with + | num n => + intro _ + show interpSign (eval prog (.num n) vs) (.int n) + cases n with + | zero => rfl + | succ n' => exact ⟨n', congrArg Value.int (by push_cast; ring)⟩ + | var x v hxv => + intro hvs + show interpSign (eval prog (.var x) vs) v + simp only [eval] + by_cases hk : FiniteMap.MemKey x vs + · rw [dif_pos hk] + exact hvs _ _ (FiniteMap.locate hk).2 _ hxv + · rw [dif_neg hk] + exact trivial + | add e₁ e₂ z₁ z₂ _ _ ih₁ ih₂ => + intro hvs + have h₁ : interpSign (eval prog e₁ vs) (.int z₁) := ih₁ hvs + have h₂ : interpSign (eval prog e₂ vs) (.int z₂) := ih₂ hvs + show interpSign (eval prog (.add e₁ e₂) vs) (.int (z₁ + z₂)) + exact plus_valid h₁ h₂ + | sub e₁ e₂ z₁ z₂ _ _ ih₁ ih₂ => + intro hvs + have h₁ : interpSign (eval prog e₁ vs) (.int z₁) := ih₁ hvs + have h₂ : interpSign (eval prog e₂ vs) (.int z₂) := ih₂ hvs + show interpSign (eval prog (.sub e₁ e₂) vs) (.int (z₁ - z₂)) + exact minus_valid h₁ h₂ + +/-- 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 + +end SignAnalysis + +end Spa diff --git a/lean/Spa/Analysis/Utils.lean b/lean/Spa/Analysis/Utils.lean new file mode 100644 index 0000000..bb9d5e3 --- /dev/null +++ b/lean/Spa/Analysis/Utils.lean @@ -0,0 +1,15 @@ +/- +Port of `Analysis/Utils.agda`. The `≼ᴼ-trans` module parameter lifts into the +`Preorder` instance. +-/ +import Spa.Lattice + +namespace Spa + +/-- Agda: `eval-combine₂`. -/ +theorem eval_combine₂ {O : Type*} [Preorder O] {combine : O → O → O} + (hmono : Monotone₂ combine) {o₁ o₂ o₃ o₄ : O} + (h₁ : o₁ ≤ o₃) (h₂ : o₂ ≤ o₄) : combine o₁ o₂ ≤ combine o₃ o₄ := + le_trans (hmono.1 o₂ h₁) (hmono.2 o₃ h₂) + +end Spa diff --git a/lean/Spa/Lattice/AboveBelow.lean b/lean/Spa/Lattice/AboveBelow.lean index 06937b9..db0a11d 100644 --- a/lean/Spa/Lattice/AboveBelow.lean +++ b/lean/Spa/Lattice/AboveBelow.lean @@ -134,6 +134,27 @@ theorem mk_lt_top (x : α) : (mk x : AboveBelow α) < top := theorem bot_lt_top : (bot : AboveBelow α) < top := lt_of_le_of_ne (bot_le' _) (by simp) +/-- The order of the flat lattice, by cases (used to discharge the +monotonicity obligations that were `postulate`d in `Analysis/Sign.agda` and +`Analysis/Constant.agda`). -/ +theorem 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) + /-- 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/Showable.lean b/lean/Spa/Showable.lean new file mode 100644 index 0000000..55d0e16 --- /dev/null +++ b/lean/Spa/Showable.lean @@ -0,0 +1,47 @@ +/- +Port of `Showable.agda` (plus the `Showable` instances that lived on +`Lattice/Map.agda` and `Lattice/AboveBelow.agda`). + +Lean has `ToString`, but its `String` instance does not quote (the Agda one +does), so to reproduce the Agda output exactly we port the class as-is. +-/ +import Spa.Lattice.FiniteMap +import Spa.Lattice.AboveBelow + +namespace Spa + +/-- Agda: `Showable` (`show` is a Lean keyword, hence `show'`). -/ +class Showable (α : Type*) where + show' : α → String + +export Showable (show') + +instance : Showable String := ⟨fun s => "\"" ++ s ++ "\""⟩ + +instance : Showable ℕ := ⟨toString⟩ + +instance : Showable ℤ := ⟨toString⟩ + +instance {n : ℕ} : Showable (Fin n) := ⟨fun i => toString i.val⟩ + +instance {α β : Type*} [Showable α] [Showable β] : Showable (α × β) := + ⟨fun p => "(" ++ show' p.1 ++ ", " ++ show' p.2 ++ ")"⟩ + +instance : Showable PUnit := ⟨fun _ => "()"⟩ + +/-- Agda: the `Showable` instance of `Lattice/AboveBelow.agda`. -/ +instance {α : Type*} [Showable α] : Showable (AboveBelow α) := + ⟨fun + | .bot => "⊥" + | .top => "⊤" + | .mk x => show' x⟩ + +/-- Agda: the `Showable` instance of `Lattice/Map.agda` (inherited by +`FiniteMap`). -/ +instance {α β : Type*} {ks : List α} [Showable α] [Showable β] : + Showable (FiniteMap α β ks) := + ⟨fun fm => + "{" ++ fm.val.foldr (fun p rest => show' p.1 ++ " ↦ " ++ show' p.2 ++ ", " ++ rest) "" + ++ "}"⟩ + +end Spa diff --git a/lean/lakefile.toml b/lean/lakefile.toml index dcb9686..512fa92 100644 --- a/lean/lakefile.toml +++ b/lean/lakefile.toml @@ -8,3 +8,7 @@ rev = "v4.17.0" [[lean_lib]] name = "Spa" + +[[lean_exe]] +name = "spa" +root = "Main"