From 7d2928ed81495d52909de0bdee90a003888d7ec0 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 10 May 2024 22:31:47 -0700 Subject: [PATCH] Prove that the sign analysis is correct Signed-off-by: Danila Fedorin --- Analysis/Sign.agda | 86 +++++++++++++++++++++++++++++++++++++++++----- Main.agda | 2 +- 2 files changed, 78 insertions(+), 10 deletions(-) diff --git a/Analysis/Sign.agda b/Analysis/Sign.agda index 5d44338..636d96e 100644 --- a/Analysis/Sign.agda +++ b/Analysis/Sign.agda @@ -1,8 +1,8 @@ module Analysis.Sign where -open import Data.Integer using (ℤ; +_; -[1+_]) -open import Data.Nat using (ℕ; suc; zero) -open import Data.Product using (Σ; proj₁; _,_) +open import Data.Integer as Int using (ℤ; +_; -[1+_]) +open import Data.Nat as Nat using (ℕ; suc; zero) +open import Data.Product using (Σ; proj₁; proj₂; _,_) open import Data.Sum using (inj₁; inj₂) open import Data.Empty using (⊥; ⊥-elim) open import Data.Unit using (⊤; tt) @@ -115,7 +115,7 @@ postulate minus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ ⟦_⟧ᵍ ⊥ᵍ _ = ⊥ ⟦_⟧ᵍ ⊤ᵍ _ = ⊤ ⟦_⟧ᵍ [ + ]ᵍ v = Σ ℕ (λ n → v ≡ ↑ᶻ (+_ (suc n))) -⟦_⟧ᵍ [ 0ˢ ]ᵍ v = Σ ℕ (λ n → v ≡ ↑ᶻ (+_ zero)) +⟦_⟧ᵍ [ 0ˢ ]ᵍ v = v ≡ ↑ᶻ (+_ zero) ⟦_⟧ᵍ [ - ]ᵍ v = Σ ℕ (λ n → v ≡ ↑ᶻ -[1+ n ]) ⟦⟧ᵍ-respects-≈ᵍ : ∀ {s₁ s₂ : SignLattice} → s₁ ≈ᵍ s₂ → ⟦ s₁ ⟧ᵍ ⇒ ⟦ s₂ ⟧ᵍ @@ -141,12 +141,12 @@ postulate minus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ s₁≢s₂⇒¬s₁∧s₂ : ∀ {s₁ s₂ : Sign} → ¬ s₁ ≡ s₂ → ∀ {v} → ¬ ((⟦ [ s₁ ]ᵍ ⟧ᵍ ∧ ⟦ [ s₂ ]ᵍ ⟧ᵍ) v) s₁≢s₂⇒¬s₁∧s₂ { + } { + } +≢+ _ = ⊥-elim (+≢+ refl) s₁≢s₂⇒¬s₁∧s₂ { + } { - } _ ((n , refl) , (m , ())) -s₁≢s₂⇒¬s₁∧s₂ { + } { 0ˢ } _ ((n , refl) , (m , ())) -s₁≢s₂⇒¬s₁∧s₂ { 0ˢ } { + } _ ((n , refl) , (m , ())) +s₁≢s₂⇒¬s₁∧s₂ { + } { 0ˢ } _ ((n , refl) , ()) +s₁≢s₂⇒¬s₁∧s₂ { 0ˢ } { + } _ (refl , (m , ())) s₁≢s₂⇒¬s₁∧s₂ { 0ˢ } { 0ˢ } +≢+ _ = ⊥-elim (+≢+ refl) -s₁≢s₂⇒¬s₁∧s₂ { 0ˢ } { - } _ ((n , refl) , (m , ())) +s₁≢s₂⇒¬s₁∧s₂ { 0ˢ } { - } _ (refl , (m , ())) s₁≢s₂⇒¬s₁∧s₂ { - } { + } _ ((n , refl) , (m , ())) -s₁≢s₂⇒¬s₁∧s₂ { - } { 0ˢ } _ ((n , refl) , (m , ())) +s₁≢s₂⇒¬s₁∧s₂ { - } { 0ˢ } _ ((n , refl) , ()) s₁≢s₂⇒¬s₁∧s₂ { - } { - } +≢+ _ = ⊥-elim (+≢+ refl) ⟦⟧ᵍ-⊓ᵍ-∧ : ∀ {s₁ s₂ : SignLattice} → (⟦ s₁ ⟧ᵍ ∧ ⟦ s₂ ⟧ᵍ) ⇒ ⟦ s₁ ⊓ᵍ s₂ ⟧ᵍ @@ -222,7 +222,75 @@ module WithProg (prog : Program) where eval-Mono (# 0) _ = ≈ᵍ-refl eval-Mono (# (suc n')) _ = ≈ᵍ-refl - open ForwardWithProg.WithEvaluator eval eval-Mono using (result) + module ForwardWithEval = ForwardWithProg.WithEvaluator eval eval-Mono + open ForwardWithEval using (result) -- For debugging purposes, print out the result. output = show result + + module ForwardWithInterp = ForwardWithEval.WithInterpretation latticeInterpretationᵍ + open ForwardWithInterp using (⟦_⟧ᵛ; InterpretationValid) + + -- This should have fewer cases -- the same number as the actual 'plus' above. + -- But agda only simplifies on first argument, apparently, so we are stuck + -- listing them all. + plus-valid : ∀ {g₁ g₂} {z₁ z₂} → ⟦ g₁ ⟧ᵍ (↑ᶻ z₁) → ⟦ g₂ ⟧ᵍ (↑ᶻ z₂) → ⟦ plus g₁ g₂ ⟧ᵍ (↑ᶻ (z₁ Int.+ z₂)) + plus-valid {⊥ᵍ} {_} ⊥ _ = ⊥ + plus-valid {[ + ]ᵍ} {⊥ᵍ} _ ⊥ = ⊥ + plus-valid {[ - ]ᵍ} {⊥ᵍ} _ ⊥ = ⊥ + plus-valid {[ 0ˢ ]ᵍ} {⊥ᵍ} _ ⊥ = ⊥ + plus-valid {⊤ᵍ} {⊥ᵍ} _ ⊥ = ⊥ + plus-valid {⊤ᵍ} {[ + ]ᵍ} _ _ = tt + plus-valid {⊤ᵍ} {[ - ]ᵍ} _ _ = tt + plus-valid {⊤ᵍ} {[ 0ˢ ]ᵍ} _ _ = tt + plus-valid {⊤ᵍ} {⊤ᵍ} _ _ = tt + plus-valid {[ + ]ᵍ} {[ + ]ᵍ} (n₁ , refl) (n₂ , refl) = (_ , refl) + plus-valid {[ + ]ᵍ} {[ - ]ᵍ} _ _ = tt + plus-valid {[ + ]ᵍ} {[ 0ˢ ]ᵍ} (n₁ , refl) refl = (_ , refl) + plus-valid {[ + ]ᵍ} {⊤ᵍ} _ _ = tt + plus-valid {[ - ]ᵍ} {[ + ]ᵍ} _ _ = tt + plus-valid {[ - ]ᵍ} {[ - ]ᵍ} (n₁ , refl) (n₂ , refl) = (_ , refl) + plus-valid {[ - ]ᵍ} {[ 0ˢ ]ᵍ} (n₁ , refl) refl = (_ , refl) + plus-valid {[ - ]ᵍ} {⊤ᵍ} _ _ = tt + plus-valid {[ 0ˢ ]ᵍ} {[ + ]ᵍ} refl (n₂ , refl) = (_ , refl) + plus-valid {[ 0ˢ ]ᵍ} {[ - ]ᵍ} refl (n₂ , refl) = (_ , refl) + plus-valid {[ 0ˢ ]ᵍ} {[ 0ˢ ]ᵍ} refl refl = refl + plus-valid {[ 0ˢ ]ᵍ} {⊤ᵍ} _ _ = tt + + -- Same for this one. It should be easier, but Agda won't simplify. + minus-valid : ∀ {g₁ g₂} {z₁ z₂} → ⟦ g₁ ⟧ᵍ (↑ᶻ z₁) → ⟦ g₂ ⟧ᵍ (↑ᶻ z₂) → ⟦ minus g₁ g₂ ⟧ᵍ (↑ᶻ (z₁ Int.- z₂)) + minus-valid {⊥ᵍ} {_} ⊥ _ = ⊥ + minus-valid {[ + ]ᵍ} {⊥ᵍ} _ ⊥ = ⊥ + minus-valid {[ - ]ᵍ} {⊥ᵍ} _ ⊥ = ⊥ + minus-valid {[ 0ˢ ]ᵍ} {⊥ᵍ} _ ⊥ = ⊥ + minus-valid {⊤ᵍ} {⊥ᵍ} _ ⊥ = ⊥ + minus-valid {⊤ᵍ} {[ + ]ᵍ} _ _ = tt + minus-valid {⊤ᵍ} {[ - ]ᵍ} _ _ = tt + minus-valid {⊤ᵍ} {[ 0ˢ ]ᵍ} _ _ = tt + minus-valid {⊤ᵍ} {⊤ᵍ} _ _ = tt + minus-valid {[ + ]ᵍ} {[ + ]ᵍ} _ _ = tt + minus-valid {[ + ]ᵍ} {[ - ]ᵍ} (n₁ , refl) (n₂ , refl) = (_ , refl) + minus-valid {[ + ]ᵍ} {[ 0ˢ ]ᵍ} (n₁ , refl) refl = (_ , refl) + minus-valid {[ + ]ᵍ} {⊤ᵍ} _ _ = tt + minus-valid {[ - ]ᵍ} {[ + ]ᵍ} (n₁ , refl) (n₂ , refl) = (_ , refl) + minus-valid {[ - ]ᵍ} {[ - ]ᵍ} _ _ = tt + minus-valid {[ - ]ᵍ} {[ 0ˢ ]ᵍ} (n₁ , refl) refl = (_ , refl) + minus-valid {[ - ]ᵍ} {⊤ᵍ} _ _ = tt + minus-valid {[ 0ˢ ]ᵍ} {[ + ]ᵍ} refl (n₂ , refl) = (_ , refl) + minus-valid {[ 0ˢ ]ᵍ} {[ - ]ᵍ} refl (n₂ , refl) = (_ , refl) + minus-valid {[ 0ˢ ]ᵍ} {[ 0ˢ ]ᵍ} refl refl = refl + minus-valid {[ 0ˢ ]ᵍ} {⊤ᵍ} _ _ = tt + + eval-Valid : InterpretationValid + eval-Valid (⇒ᵉ-+ ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ = + plus-valid (eval-Valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-Valid ρ,e₂⇒z₂ ⟦vs⟧ρ) + eval-Valid (⇒ᵉ-- ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ = + minus-valid (eval-Valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-Valid ρ,e₂⇒z₂ ⟦vs⟧ρ) + eval-Valid {vs} (⇒ᵉ-Var ρ x v x,v∈ρ) ⟦vs⟧ρ + with ∈k-decᵛ x (proj₁ (proj₁ vs)) + ... | yes x∈kvs = ⟦vs⟧ρ (proj₂ (locateᵛ {x} {vs} x∈kvs)) x,v∈ρ + ... | no x∉kvs = tt + eval-Valid (⇒ᵉ-ℕ ρ 0) _ = refl + eval-Valid (⇒ᵉ-ℕ ρ (suc n')) _ = (n' , refl) + + open ForwardWithInterp.WithValidity eval-Valid using (analyze-correct) public diff --git a/Main.agda b/Main.agda index b847237..8675cbd 100644 --- a/Main.agda +++ b/Main.agda @@ -37,6 +37,6 @@ testProgram = record { rootStmt = testCode } -open WithProg testProgram using (output) +open WithProg testProgram using (output; analyze-correct) main = run {0ℓ} (putStrLn output)