From 4ac9dffa9b046ba51e6b0de943942e0dbf4b1e1e Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Wed, 8 May 2024 22:53:21 -0700 Subject: [PATCH] Prove that the var->lattice maps respect equality Signed-off-by: Danila Fedorin --- Analysis/Forward.agda | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda index 45c51e2..aed8fa9 100644 --- a/Analysis/Forward.agda +++ b/Analysis/Forward.agda @@ -19,7 +19,7 @@ open import Relation.Nullary using (¬_; Dec; yes; no) open import Data.Unit using (⊤) open import Function using (_∘_; flip) -open import Utils using (Pairwise) +open import Utils using (Pairwise; _⇒_) import Lattice.FiniteValueMap open IsFiniteHeightLattice isFiniteHeightLatticeˡ @@ -28,6 +28,7 @@ open IsFiniteHeightLattice isFiniteHeightLatticeˡ ( isLattice to isLatticeˡ ; fixedHeight to fixedHeightˡ ; _≼_ to _≼ˡ_ + ; ≈-sym to ≈ˡ-sym ) module WithProg (prog : Program) where @@ -210,7 +211,7 @@ module WithProg (prog : Program) where -- The fixed point of the 'analyze' function is our final goal. open import Fixedpoint ≈ᵐ-dec isFiniteHeightLatticeᵐ analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂) using () - renaming (aᶠ to result) + renaming (aᶠ to result; aᶠ≈faᶠ to result≈analyze-result) public variablesAt-updateAll : ∀ (s : State) (sv : StateVariables) → @@ -222,11 +223,21 @@ module WithProg (prog : Program) where module WithInterpretation (latticeInterpretationˡ : LatticeInterpretation isLatticeˡ) where open LatticeInterpretation latticeInterpretationˡ using () - renaming (⟦_⟧ to ⟦_⟧ˡ) + renaming (⟦_⟧ to ⟦_⟧ˡ; ⟦⟧-respects-≈ to ⟦⟧ˡ-respects-≈ˡ) ⟦_⟧ᵛ : VariableValues → Env → Set ⟦_⟧ᵛ vs ρ = ∀ {k l} → (k , l) ∈ᵛ vs → ∀ {v} → (k , v) Language.∈ ρ → ⟦ l ⟧ˡ v + + ⟦⟧ᵛ-respects-≈ᵛ : ∀ {vs₁ vs₂ : VariableValues} → vs₁ ≈ᵛ vs₂ → ⟦ vs₁ ⟧ᵛ ⇒ ⟦ vs₂ ⟧ᵛ + ⟦⟧ᵛ-respects-≈ᵛ {m₁ , _} {m₂ , _} + (m₁⊆m₂ , m₂⊆m₁) ρ ⟦vs₁⟧ρ {k} {l} k,l∈m₂ {v} k,v∈ρ = + let + (l' , (l≈l' , k,l'∈m₁)) = m₂⊆m₁ _ _ k,l∈m₂ + ⟦l'⟧v = ⟦vs₁⟧ρ k,l'∈m₁ k,v∈ρ + in + ⟦⟧ˡ-respects-≈ˡ (≈ˡ-sym l≈l') v ⟦l'⟧v + InterpretationValid : Set InterpretationValid = ∀ {vs ρ e v} → ρ , e ⇒ᵉ v → ⟦ vs ⟧ᵛ ρ → ⟦ eval e vs ⟧ˡ v