From 3d2a507f2ffabc096c08534d9a9a3826ee12c2a9 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Thu, 9 May 2024 22:49:53 -0700
Subject: [PATCH] Almost prove correctness

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Analysis/Forward.agda | 16 +++++++++++++++-
 Language.agda         |  6 ++++++
 2 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda
index b4ab689..678bccc 100644
--- a/Analysis/Forward.agda
+++ b/Analysis/Forward.agda
@@ -15,7 +15,7 @@ open import Data.Sum using (inj₁; inj₂)
 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.Binary.PropositionalEquality using (_≡_; refl; cong; sym; trans; subst)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Data.Unit using (⊤)
 open import Function using (_∘_; flip)
@@ -73,6 +73,7 @@ module WithProg (prog : Program) where
         using ()
         renaming
             ( isFiniteHeightLattice to isFiniteHeightLatticeᵛ
+            ; ⊥-contains-bottoms to ⊥ᵛ-contains-bottoms
             )
 
     ≈ᵛ-dec = ≈ˡ-dec⇒≈ᵛ-dec ≈ˡ-dec
@@ -254,6 +255,8 @@ module WithProg (prog : Program) where
             ⟦_⟧ᵛ : 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₂ , _}
@@ -352,3 +355,14 @@ module WithProg (prog : Program) where
                             ⟦⟧ᵛ-foldr ⟦result-s₁⟧ρ s₁∈incomingStates
                     in
                         walkTrace ⟦joinForKey-s⟧ρ tr
+
+                postulate initialState-pred-∅ : incoming initialState ≡ []
+
+                joinForKey-initialState-⊥ᵛ : joinForKey initialState result ≡ ⊥ᵛ
+                joinForKey-initialState-⊥ᵛ = cong (λ ins → foldr _⊔ᵛ_ ⊥ᵛ (result [ ins ])) initialState-pred-∅
+
+                ⟦joinAll-initialState⟧ᵛ∅ : ⟦ joinForKey initialState result ⟧ᵛ []
+                ⟦joinAll-initialState⟧ᵛ∅ = subst (λ vs → ⟦ vs ⟧ᵛ []) (sym joinForKey-initialState-⊥ᵛ) ⟦⊥ᵛ⟧ᵛ∅
+
+                analyze-correct : ∀ {ρ : Env} → [] , rootStmt ⇒ˢ ρ → ⟦ variablesAt finalState result ⟧ᵛ ρ
+                analyze-correct {ρ} ∅,s⇒ρ = walkTrace {initialState} {finalState} {[]} {ρ} ⟦joinAll-initialState⟧ᵛ∅ (trace ∅,s⇒ρ)
diff --git a/Language.agda b/Language.agda
index a35ee01..081192f 100644
--- a/Language.agda
+++ b/Language.agda
@@ -11,6 +11,7 @@ open import Data.Fin.Properties as FinProp using (suc-injective)
 open import Data.List as List using (List; []; _∷_)
 open import Data.List.Membership.Propositional as ListMem using ()
 open import Data.List.Membership.Propositional.Properties as ListMemProp using (∈-filter⁺)
+open import Data.List.Relation.Unary.Any as RelAny using ()
 open import Data.Nat using (ℕ; suc)
 open import Data.Product using (_,_; Σ; proj₁; proj₂)
 open import Data.Product.Properties as ProdProp using ()
@@ -42,6 +43,11 @@ record Program : Set where
     finalState : State
     finalState = proj₁ (wrap-output (buildCfg rootStmt))
 
+    trace : ∀ {ρ : Env} → [] , rootStmt ⇒ˢ ρ → Trace {graph} initialState finalState [] ρ
+    trace {ρ} ∅,s⇒ρ
+        with MkEndToEndTrace idx₁ (RelAny.here refl) idx₂ (RelAny.here refl) tr
+             ← EndToEndTrace-wrap (buildCfg-sufficient ∅,s⇒ρ) = tr
+
     private
         vars-Set : StringSet
         vars-Set = Stmt-vars rootStmt