Prove that the var->lattice maps respect equality

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Analysis/Forward.agda

@@ -7,17 +7,19 @@ module Analysis.Forward
     (isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_)
     (≈ˡ-dec : IsDecidable _≈ˡ_) where
 
+open import Data.Empty using (⊥-elim)
 open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
 open import Data.Nat using (suc)
 open import Data.Product using (_×_; proj₁; _,_)
-open import Data.List using (List; _∷_; []; foldr; cartesianProduct; cartesianProductWith)
+open import Data.List using (List; _∷_; []; foldr; foldl; cartesianProduct; cartesianProductWith)
 open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
+open import Data.List.Relation.Unary.Any as Any using ()
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Data.Unit using (⊤)
-open import Function using (_∘_)
+open import Function using (_∘_; flip)
 
-open import Utils using (Pairwise)
+open import Utils using (Pairwise; _⇒_)
 import Lattice.FiniteValueMap
 
 open IsFiniteHeightLattice isFiniteHeightLatticeˡ
@@ -26,6 +28,7 @@ open IsFiniteHeightLattice isFiniteHeightLatticeˡ
         ( isLattice to isLatticeˡ
         ; fixedHeight to fixedHeightˡ
         ; _≼_ to _≼ˡ_
+        ; ≈-sym to ≈ˡ-sym
         )
 
 module WithProg (prog : Program) where
@@ -93,6 +96,17 @@ module WithProg (prog : Program) where
     ≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec
     fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ
 
+    -- We now have our (state -> (variables -> value)) map.
+    -- Define a couple of helpers to retrieve values from it. Specifically,
+    -- since the State type is as specific as possible, it's always possible to
+    -- retrieve the variable values at each state.
+
+    states-in-Map : ∀ (s : State) (sv : StateVariables) → s ∈kᵐ sv
+    states-in-Map s sv@(m , ksv≡states) rewrite ksv≡states = states-complete s
+
+    variablesAt : State → StateVariables → VariableValues
+    variablesAt s sv = proj₁ (locateᵐ {s} {sv} (states-in-Map s sv))
+
     -- build up the 'join' function, which follows from Exercise 4.26's
     --
     --    L₁ → (A → L₂)
@@ -116,8 +130,15 @@ module WithProg (prog : Program) where
         renaming
             ( f' to joinAll
             ; f'-Monotonic to joinAll-Mono
+            ; f'-k∈ks-≡ to joinAll-k∈ks-≡
             )
 
+    variablesAt-joinAll : ∀ (s : State) (sv : StateVariables) →
+                          variablesAt s (joinAll sv) ≡ joinForKey s sv
+    variablesAt-joinAll s sv
+        with (vs , s,vs∈usv) ← locateᵐ {s} {joinAll sv} (states-in-Map s (joinAll sv)) =
+        joinAll-k∈ks-≡ {l = sv} (states-complete s) s,vs∈usv
+
     -- With 'join' in hand, we need to perform abstract evaluation.
     module WithEvaluator (eval : Expr → VariableValues → L)
                          (eval-Mono : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ˡ_ (eval e)) where
@@ -131,12 +152,11 @@ module WithProg (prog : Program) where
                 renaming
                     ( f' to updateVariablesFromExpression
                     ; f'-Monotonic to updateVariablesFromExpression-Mono
+                    ; f'-k∈ks-≡ to updateVariablesFromExpression-k∈ks-≡
+                    ; f'-k∉ks-backward to updateVariablesFromExpression-k∉ks-backward
                     )
                 public
 
-        states-in-Map : ∀ (s : State) (sv : StateVariables) → s ∈kᵐ sv
-        states-in-Map s sv@(m , ksv≡states) rewrite ksv≡states = states-complete s
-
         -- The per-state update function makes use of the single-key setter,
         -- updateVariablesFromExpression, for the case where the statement
         -- is an assignment.
@@ -155,11 +175,7 @@ module WithProg (prog : Program) where
 
         updateVariablesForState : State → StateVariables → VariableValues
         updateVariablesForState s sv =
-            let
-                bss = code s
-                (vs , s,vs∈sv) = locateᵐ {s} {sv} (states-in-Map s sv)
-            in
-                foldr updateVariablesFromStmt vs bss
+            foldl (flip updateVariablesFromStmt) (variablesAt s sv) (code s)
 
         updateVariablesForState-Monoʳ : ∀ (s : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (updateVariablesForState s)
         updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂ =
@@ -169,14 +185,15 @@ module WithProg (prog : Program) where
                 (vs₂ , s,vs₂∈sv₂) = locateᵐ {s} {sv₂} (states-in-Map s sv₂)
                 vs₁≼vs₂ = m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ sv₁ sv₂ sv₁≼sv₂ s,vs₁∈sv₁ s,vs₂∈sv₂
             in
-                foldr-Mono' (IsLattice.joinSemilattice isLatticeᵛ) bss
-                            updateVariablesFromStmt updateVariablesFromStmt-Monoʳ
+                foldl-Mono' (IsLattice.joinSemilattice isLatticeᵛ) bss
+                            (flip updateVariablesFromStmt) updateVariablesFromStmt-Monoʳ
                             vs₁≼vs₂
 
         open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states
             renaming
                 ( f' to updateAll
                 ; f'-Monotonic to updateAll-Mono
+                ; f'-k∈ks-≡ to updateAll-k∈ks-≡
                 )
 
         -- Finally, the whole analysis consists of getting the 'join'
@@ -194,5 +211,62 @@ 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) →
+                                variablesAt s (updateAll sv) ≡ updateVariablesForState s sv
+        variablesAt-updateAll s sv
+            with (vs , s,vs∈usv) ← locateᵐ {s} {updateAll sv} (states-in-Map s (updateAll sv)) =
+            updateAll-k∈ks-≡ {l = sv} (states-complete s) s,vs∈usv
+
+        module WithInterpretation (latticeInterpretationˡ : LatticeInterpretation isLatticeˡ) where
+            open LatticeInterpretation latticeInterpretationˡ
+                using ()
+                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
+
+            module WithValidity (interpretationValidˡ : InterpretationValid) where
+
+                updateVariablesFromStmt-matches : ∀ {bs vs ρ₁ ρ₂} → ρ₁ , bs ⇒ᵇ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ updateVariablesFromStmt bs vs ⟧ᵛ ρ₂
+                updateVariablesFromStmt-matches {_} {vs} {ρ₁} {ρ₁} (⇒ᵇ-noop ρ₁) ⟦vs⟧ρ₁ = ⟦vs⟧ρ₁
+                updateVariablesFromStmt-matches {_} {vs} {ρ₁} {_} (⇒ᵇ-← ρ₁ k e v ρ,e⇒v) ⟦vs⟧ρ₁ {k'} {l} k',l∈vs' {v'} k',v'∈ρ₂
+                    with k ≟ˢ k' | k',v'∈ρ₂
+                ...   | yes refl | here _ v _
+                        rewrite updateVariablesFromExpression-k∈ks-≡ k e {l = vs} (Any.here refl) k',l∈vs' =
+                        interpretationValidˡ ρ,e⇒v ⟦vs⟧ρ₁
+                ...   | yes k≡k' | there _ _ _ _ _ k'≢k _ = ⊥-elim (k'≢k (sym k≡k'))
+                ...   | no k≢k' | here _ _ _ = ⊥-elim (k≢k' refl)
+                ...   | no k≢k'  | there _ _ _ _ _ _ k',v'∈ρ₁ =
+                        let
+                            k'∉[k] = (λ { (Any.here refl) → k≢k' refl })
+                            k',l∈vs = updateVariablesFromExpression-k∉ks-backward k e {l = vs} k'∉[k] k',l∈vs'
+                        in
+                            ⟦vs⟧ρ₁ k',l∈vs k',v'∈ρ₁
+
+                updateVariablesFromStmt-fold-matches : ∀ {bss vs ρ₁ ρ₂} → ρ₁ , bss ⇒ᵇˢ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ foldl (flip updateVariablesFromStmt) vs bss ⟧ᵛ ρ₂
+                updateVariablesFromStmt-fold-matches [] ⟦vs⟧ρ = ⟦vs⟧ρ
+                updateVariablesFromStmt-fold-matches {bs ∷ bss'} {vs} {ρ₁} {ρ₂} (ρ₁,bs⇒ρ ∷ ρ,bss'⇒ρ₂) ⟦vs⟧ρ₁ =
+                    updateVariablesFromStmt-fold-matches {bss'} {updateVariablesFromStmt bs vs} ρ,bss'⇒ρ₂ (updateVariablesFromStmt-matches ρ₁,bs⇒ρ ⟦vs⟧ρ₁)
+
+                updateVariablesForState-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ updateVariablesForState s sv ⟧ᵛ ρ₂
+                updateVariablesForState-matches = updateVariablesFromStmt-fold-matches
+
+                updateAll-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ variablesAt s (updateAll sv) ⟧ᵛ ρ₂
+                updateAll-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁ rewrite variablesAt-updateAll s sv =
+                    updateVariablesForState-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁

Lattice.agda

@@ -137,7 +137,7 @@ module _ {a b} {A : Set a} {B : Set b}
     const-Mono : ∀ (x : B) → Monotonic _≼₁_ _≼₂_ (λ _ → x)
     const-Mono x _ = ⊔₂-idemp x
 
-    open import Data.List as List using (List; foldr; _∷_)
+    open import Data.List as List using (List; foldr; foldl; _∷_)
     open import Utils using (Pairwise; _∷_)
 
     foldr-Mono : ∀ (l₁ l₂ : List A) (f : A → B → B) (b₁ b₂ : B) →
@@ -150,13 +150,22 @@ module _ {a b} {A : Set a} {B : Set b}
         ≼₂-trans (f-Mono₁ (foldr f b₁ xs) x≼y)
                  (f-Mono₂ y (foldr-Mono xs ys f b₁ b₂ xs≼ys b₁≼b₂ f-Mono₁ f-Mono₂))
 
+    foldl-Mono : ∀ (l₁ l₂ : List A) (f : B → A → B) (b₁ b₂ : B) →
+                 Pairwise _≼₁_ l₁ l₂ → b₁ ≼₂ b₂ →
+                 (∀ a → Monotonic _≼₂_ _≼₂_ (λ b → f b a)) →
+                 (∀ b → Monotonic _≼₁_ _≼₂_ (f b)) →
+                 foldl f b₁ l₁ ≼₂ foldl f b₂ l₂
+    foldl-Mono List.[] List.[] f b₁ b₂ _ b₁≼b₂ _ _ = b₁≼b₂
+    foldl-Mono (x ∷ xs) (y ∷ ys) f b₁ b₂ (x≼y ∷ xs≼ys) b₁≼b₂ f-Mono₁ f-Mono₂ =
+        foldl-Mono xs ys f (f b₁ x) (f b₂ y) xs≼ys (≼₂-trans (f-Mono₁ x b₁≼b₂) (f-Mono₂ b₂ x≼y)) f-Mono₁ f-Mono₂
+
 module _ {a b} {A : Set a} {B : Set b}
          {_≈₂_ : B → B → Set b} {_⊔₂_ : B → B → B}
          (lB : IsSemilattice B _≈₂_ _⊔₂_) where
 
     open IsSemilattice lB using () renaming (_≼_ to _≼₂_; ⊔-idemp to ⊔₂-idemp; ≼-trans to ≼₂-trans)
 
-    open import Data.List as List using (List; foldr; _∷_)
+    open import Data.List as List using (List; foldr; foldl; _∷_)
     open import Utils using (Pairwise; _∷_)
 
     foldr-Mono' : ∀ (l : List A) (f : A → B → B) →
@@ -165,6 +174,12 @@ module _ {a b} {A : Set a} {B : Set b}
     foldr-Mono' List.[] f _ b₁≼b₂ = b₁≼b₂
     foldr-Mono' (x ∷ xs) f f-Mono₂ b₁≼b₂ = f-Mono₂ x (foldr-Mono' xs f f-Mono₂ b₁≼b₂)
 
+    foldl-Mono' : ∀ (l : List A) (f : B → A → B) →
+                  (∀ b → Monotonic _≼₂_ _≼₂_ (λ a → f a b)) →
+                  Monotonic _≼₂_ _≼₂_ (λ b → foldl f b l)
+    foldl-Mono' List.[] f _ b₁≼b₂ = b₁≼b₂
+    foldl-Mono' (x ∷ xs) f f-Mono₁ b₁≼b₂ = foldl-Mono' xs f f-Mono₁ (f-Mono₁ x b₁≼b₂)
+
 record IsLattice {a} (A : Set a)
     (_≈_ : A → A → Set a)
     (_⊔_ : A → A → A)

Lattice/FiniteMap.agda

@@ -35,6 +35,11 @@ open import Lattice.Map ≡-dec-A lB as Map
         ; keys to keysᵐ
         ; _updating_via_ to _updatingᵐ_via_
         ; updating-via-keys-≡ to updatingᵐ-via-keys-≡
+        ; updating-via-k∈ks to updatingᵐ-via-k∈ks
+        ; updating-via-k∈ks-≡ to updatingᵐ-via-k∈ks-≡
+        ; updating-via-∈k-forward to updatingᵐ-via-∈k-forward
+        ; updating-via-k∉ks-forward to updatingᵐ-via-k∉ks-forward
+        ; updating-via-k∉ks-backward to updatingᵐ-via-k∉ks-backward
         ; f'-Monotonic to f'-Monotonicᵐ
         ; _≼_ to _≼ᵐ_
         ; ∈k-dec to ∈k-decᵐ
@@ -83,6 +88,8 @@ module WithKeys (ks : List A) where
     _∈k_ : A → FiniteMap → Set a
     _∈k_ k (m₁ , _) = k ∈ˡ (keysᵐ m₁)
 
+    open Map using (forget) public
+
     ∈k-dec = ∈k-decᵐ
 
     locate : ∀ {k : A} {fm : FiniteMap} → k ∈k fm → Σ B (λ v → (k , v) ∈ fm)
@@ -171,6 +178,21 @@ module WithKeys (ks : List A) where
         f'-Monotonic : Monotonic _≼ˡ_ _≼_ f'
         f'-Monotonic {l₁} {l₂} l₁≼l₂ = f'-Monotonicᵐ lL (proj₁ ∘ f) f-Monotonic g g-Monotonicʳ ks l₁≼l₂
 
+        f'-∈k-forward : ∀ {k l} → k ∈k (f l) → k ∈k (f' l)
+        f'-∈k-forward {k} {l} = updatingᵐ-via-∈k-forward (proj₁ (f l)) ks (updater l)
+
+        f'-k∈ks : ∀ {k l} → k ∈ˡ ks → k ∈k (f' l) → (k , updater l k) ∈ (f' l)
+        f'-k∈ks {k} {l} = updatingᵐ-via-k∈ks (proj₁ (f l)) (updater l)
+
+        f'-k∈ks-≡ : ∀ {k v l} → k ∈ˡ ks → (k , v) ∈ (f' l) → v ≡ updater l k
+        f'-k∈ks-≡ {k} {v} {l} = updatingᵐ-via-k∈ks-≡ (proj₁ (f l)) (updater l)
+
+        f'-k∉ks-forward : ∀ {k v l} → ¬ k ∈ˡ ks → (k , v) ∈ (f l) → (k , v) ∈ (f' l)
+        f'-k∉ks-forward {k} {v} {l} = updatingᵐ-via-k∉ks-forward (proj₁ (f l)) (updater l)
+
+        f'-k∉ks-backward : ∀ {k v l} → ¬ k ∈ˡ ks → (k , v) ∈ (f' l) → (k , v) ∈ (f l)
+        f'-k∉ks-backward {k} {v} {l} = updatingᵐ-via-k∉ks-backward (proj₁ (f l)) (updater l)
+
     all-equal-keys : ∀ (fm₁ fm₂ : FiniteMap) → (Map.keys (proj₁ fm₁) ≡ Map.keys (proj₁ fm₂))
     all-equal-keys (fm₁ , km₁≡ks) (fm₂ , km₂≡ks) = trans km₁≡ks (sym km₂≡ks)
 

Lattice/FiniteValueMap.agda

@@ -32,7 +32,7 @@ open import Isomorphism using (IsInverseˡ; IsInverseʳ)
 open import Lattice.Map ≡-dec-A lB
     using
         ( subset-impl
-        ; locate; forget
+        ; locate
         ; Map-functional
         ; Expr-Provenance
         ; Expr-Provenance-≡