From f4392b32c0607e7d650473983fb79c19d3c2e1c0 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 9 May 2024 19:01:36 -0700 Subject: [PATCH] Finish the last proof obligation for trace walking Signed-off-by: Danila Fedorin --- Analysis/Forward.agda | 6 ++++-- Lattice/FiniteMap.agda | 6 ++++++ Lattice/Map.agda | 9 +++++++++ 3 files changed, 19 insertions(+), 2 deletions(-) diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda index 8565dae..a5edcd9 100644 --- a/Analysis/Forward.agda +++ b/Analysis/Forward.agda @@ -82,7 +82,7 @@ module WithProg (prog : Program) where -- Finally, the map we care about is (state -> (variables -> value)). Bring that in. module StateVariablesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟_ isLatticeᵛ states open StateVariablesFiniteMap - using (_[_]; []-∈; m₁≼m₂⇒m₁[ks]≼m₂[ks]) + using (_[_]; []-∈; m₁≼m₂⇒m₁[ks]≼m₂[ks]; m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂) renaming ( FiniteMap to StateVariables ; isLattice to isLatticeᵐ @@ -124,7 +124,9 @@ module WithProg (prog : Program) where variablesAt-∈ s sv = proj₂ (locateᵐ {s} {sv} (states-in-Map s sv)) variablesAt-≈ : ∀ s sv₁ sv₂ → sv₁ ≈ᵐ sv₂ → variablesAt s sv₁ ≈ᵛ variablesAt s sv₂ - variablesAt-≈ = {!!} + variablesAt-≈ s sv₁ sv₂ sv₁≈sv₂ = + m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ sv₁ sv₂ sv₁≈sv₂ + (states-in-Map s sv₁) (states-in-Map s sv₂) -- build up the 'join' function, which follows from Exercise 4.26's -- diff --git a/Lattice/FiniteMap.agda b/Lattice/FiniteMap.agda index b4213eb..ee26419 100644 --- a/Lattice/FiniteMap.agda +++ b/Lattice/FiniteMap.agda @@ -32,6 +32,7 @@ open import Lattice.Map ≡-dec-A lB as Map ; _[_] to _[_]ᵐ ; []-∈ to []ᵐ-∈ ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ + ; m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ to m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ᵐ ; locate to locateᵐ ; keys to keysᵐ ; _updating_via_ to _updatingᵐ_via_ @@ -164,6 +165,11 @@ module WithKeys (ks : List A) where fm₁ ≼ fm₂ → (k , v₁) ∈ fm₁ → (k , v₂) ∈ fm₂ → v₁ ≼₂ v₂ m₁≼m₂⇒m₁[k]≼m₂[k] (m₁ , _) (m₂ , _) m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂ = m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ m₁ m₂ m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂ + m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ : ∀ (fm₁ fm₂ : FiniteMap) {k : A} → + fm₁ ≈ fm₂ → ∀ (k∈kfm₁ : k ∈k fm₁) (k∈kfm₂ : k ∈k fm₂) → + proj₁ (locate {fm = fm₁} k∈kfm₁) ≈₂ proj₁ (locate {fm = fm₂} k∈kfm₂) + m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ (m₁ , _) (m₂ , _) = m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ᵐ m₁ m₂ + module GeneralizedUpdate {l} {L : Set l} {_≈ˡ_ : L → L → Set l} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L} diff --git a/Lattice/Map.agda b/Lattice/Map.agda index 8e30306..847960c 100644 --- a/Lattice/Map.agda +++ b/Lattice/Map.agda @@ -1142,3 +1142,12 @@ m₁≼m₂⇒k∈km₁⇒k∈km₂ m₁ m₂ m₁≼m₂ k∈km₁ = (v' , (v≈v' , k,v'∈m₂)) = (proj₁ m₁≼m₂) _ _ k,v∈m₁m₂ in forget k,v'∈m₂ + +m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ : ∀ (m₁ m₂ : Map) {k : A} → + m₁ ≈ m₂ → ∀ (k∈km₁ : k ∈k m₁) (k∈km₂ : k ∈k m₂) → + proj₁ (locate {m = m₁} k∈km₁) ≈₂ proj₁ (locate {m = m₂} k∈km₂) +m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ m₁ m₂ {k} (m₁⊆m₂ , m₂⊆m₁) k∈km₁ k∈km₂ + with (v₁ , k,v₁∈m₁) ← locate {m = m₁} k∈km₁ + with (v₂ , k,v₂∈m₂) ← locate {m = m₂} k∈km₂ + with (v₂' , (v₁≈v₂' , k,v₂'∈m₂)) ← m₁⊆m₂ k v₁ k,v₁∈m₁ + rewrite Map-functional {m = m₂} k,v₂∈m₂ k,v₂'∈m₂ = v₁≈v₂'