From 80069e76e657712581e8f621247f7d7f14121252 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Thu, 9 May 2024 17:56:47 -0700
Subject: [PATCH] Prove the recursive step of trace walking

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

diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda
index 26d2e83..6b612cd 100644
--- a/Analysis/Forward.agda
+++ b/Analysis/Forward.agda
@@ -10,7 +10,7 @@ module Analysis.Forward
 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.Product using (_×_; proj₁; proj₂; _,_)
 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 ()
@@ -76,11 +76,12 @@ 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])
         renaming
             ( FiniteMap to StateVariables
             ; isLattice to isLatticeᵐ
             ; _≈_ to _≈ᵐ_
+            ; _∈_ to _∈ᵐ_
             ; _∈k_ to _∈kᵐ_
             ; locate to locateᵐ
             ; _≼_ to _≼ᵐ_
@@ -113,6 +114,9 @@ module WithProg (prog : Program) where
     variablesAt : State → StateVariables → VariableValues
     variablesAt s sv = proj₁ (locateᵐ {s} {sv} (states-in-Map s sv))
 
+    variablesAt-∈ : ∀ (s : State) (sv : StateVariables) → (s , variablesAt s sv) ∈ᵐ sv
+    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-≈ = {!!}
 
@@ -312,3 +316,14 @@ module WithProg (prog : Program) where
                 walkTrace : ∀ {s₁ s₂ ρ₁ ρ₂} → ⟦ joinForKey s₁ result ⟧ᵛ ρ₁ → Trace {graph} s₁ s₂ ρ₁ ρ₂ → ⟦ variablesAt s₂ result ⟧ᵛ ρ₂
                 walkTrace {s₁} {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-single ρ₁,bss⇒ρ₂) =
                     stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂
+                walkTrace {s₁} {s₂} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-edge {ρ₂ = ρ} {idx₂ = s} ρ₁,bss⇒ρ s₁→s₂ tr) =
+                    let
+                        ⟦result-s₁⟧ρ =
+                            stepTrace {s₁} {ρ₁} {ρ} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ
+                        s₁∈incomingStates =
+                            []-∈ result (edge⇒incoming s₁→s₂)
+                                        (variablesAt-∈ s₁ result)
+                        ⟦joinForKey-s⟧ρ =
+                            ⟦⟧ᵛ-foldr ⟦result-s₁⟧ρ s₁∈incomingStates
+                    in
+                        walkTrace ⟦joinForKey-s⟧ρ tr