From 8d0d87d2d9ae63ad54036eac83d7cf0879e09d5e Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Wed, 8 May 2024 20:50:21 -0700
Subject: [PATCH] Start on proofs of correctness

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Analysis/Forward.agda | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda
index ac1c832..b161c25 100644
--- a/Analysis/Forward.agda
+++ b/Analysis/Forward.agda
@@ -7,11 +7,13 @@ 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.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 (⊤)
@@ -50,6 +52,7 @@ module WithProg (prog : Program) where
             ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ
             ; ∈k-dec to ∈k-decᵛ
             ; all-equal-keys to all-equal-keysᵛ
+            ; forget to forgetᵛ
             )
         public
     open IsLattice isLatticeᵛ
@@ -131,6 +134,8 @@ 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
 
@@ -196,3 +201,32 @@ module WithProg (prog : Program) where
             using ()
             renaming (aᶠ to result)
             public
+
+        module WithInterpretation (latticeInterpretationˡ : LatticeInterpretation isLatticeˡ) where
+            open LatticeInterpretation latticeInterpretationˡ
+                using ()
+                renaming (⟦_⟧ to ⟦_⟧ˡ)
+
+            ⟦_⟧ᵛ : VariableValues → Env → Set
+            ⟦_⟧ᵛ vs ρ = ∀ {k l} → (k , l) ∈ᵛ vs → ∀ {v} → (k , v) Language.∈ ρ → ⟦ 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'∈ρ₁