From ab40a27e784dbbd07f790235a527e8afd1ca3a84 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sat, 27 Apr 2024 14:56:19 -0700
Subject: [PATCH] Formulate correctness of buildCfg using end-to-end traces

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Language/Properties.agda |  6 +++++-
 Language/Traces.agda     | 24 +++++++++++++++++-------
 2 files changed, 22 insertions(+), 8 deletions(-)

diff --git a/Language/Properties.agda b/Language/Properties.agda
index ff7bc65..6c0d268 100644
--- a/Language/Properties.agda
+++ b/Language/Properties.agda
@@ -8,7 +8,7 @@ open import Language.Traces
 open import Data.Fin as Fin using (zero)
 open import Data.List using (_∷_; [])
 open import Data.List.Membership.Propositional.Properties as ListMemProp using ()
-open import Data.Product using (Σ; _,_)
+open import Data.Product using (Σ; _,_; _×_)
 open import Data.Vec.Properties using (lookup-++ˡ; ++-identityʳ; lookup-++ʳ)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym)
 
@@ -81,3 +81,7 @@ Trace-loop : ∀ (g₁ : Graph) {idx₁ idx₂ : Graph.Index g₁} {ρ₁ ρ₂
 Trace-loop g₁ {idx₁} {idx₁} (Trace-single ρ₁⇒ρ₂) = Trace-single ρ₁⇒ρ₂
 Trace-loop g₁ {idx₁} (Trace-edge ρ₁⇒ρ idx₁→idx tr') =
     Trace-edge ρ₁⇒ρ (ListMemProp.∈-++⁺ˡ idx₁→idx) (Trace-loop g₁ tr')
+
+buildCfg-sufficient : ∀ {s : Stmt} {ρ₁ ρ₂ : Env} → ρ₁ , s ⇒ˢ ρ₂ →
+                      EndToEndTrace {buildCfg s} ρ₁ ρ₂
+buildCfg-sufficient = {!!}
diff --git a/Language/Traces.agda b/Language/Traces.agda
index 9169295..e1d6527 100644
--- a/Language/Traces.agda
+++ b/Language/Traces.agda
@@ -1,24 +1,34 @@
 module Language.Traces where
 
-open import Language.Base public
-open import Language.Semantics public
-open import Language.Graphs public
+open import Language.Base
+open import Language.Semantics using (Env; _,_⇒ᵇˢ_)
+open import Language.Graphs
 
 open import Data.Product using (_,_)
-open import Data.List.Membership.Propositional as MemProp using ()
+open import Data.List.Membership.Propositional using (_∈_)
 
 module _ {g : Graph} where
-    open Graph g using (Index; edges)
+    open Graph g using (Index; edges; inputs; outputs)
 
     data Trace : Index → Index → Env → Env → Set where
         Trace-single : ∀ {ρ₁ ρ₂ : Env} {idx : Index} →
                        ρ₁ , (g [ idx ]) ⇒ᵇˢ ρ₂ → Trace idx idx ρ₁ ρ₂
         Trace-edge : ∀ {ρ₁ ρ₂ ρ₃ : Env} {idx₁ idx₂ idx₃ : Index} →
-                     ρ₁ , (g [ idx₁ ]) ⇒ᵇˢ ρ₂ → (idx₁ , idx₂) MemProp.∈ edges →
+                     ρ₁ , (g [ idx₁ ]) ⇒ᵇˢ ρ₂ → (idx₁ , idx₂) ∈ edges →
                      Trace idx₂ idx₃ ρ₂ ρ₃ → Trace idx₁ idx₃ ρ₁ ρ₃
 
     _++⟨_⟩_ : ∀ {idx₁ idx₂ idx₃ idx₄ : Index} {ρ₁ ρ₂ ρ₃ : Env} →
-           Trace idx₁ idx₂ ρ₁ ρ₂ → (idx₂ , idx₃) MemProp.∈ edges →
+           Trace idx₁ idx₂ ρ₁ ρ₂ → (idx₂ , idx₃) ∈ edges →
            Trace idx₃ idx₄ ρ₂ ρ₃ → Trace idx₁ idx₄ ρ₁ ρ₃
     _++⟨_⟩_ (Trace-single ρ₁⇒ρ₂) idx₂→idx₃ tr = Trace-edge ρ₁⇒ρ₂ idx₂→idx₃ tr
     _++⟨_⟩_ (Trace-edge ρ₁⇒ρ₂ idx₁→idx' tr') idx₂→idx₃ tr = Trace-edge ρ₁⇒ρ₂ idx₁→idx' (tr' ++⟨ idx₂→idx₃ ⟩ tr)
+
+    record EndToEndTrace (ρ₁ ρ₂ : Env) : Set where
+        field
+            idx₁ : Index
+            idx₁∈inputs : idx₁ ∈ inputs
+
+            idx₂ : Index
+            idx₂∈outputs : idx₂ ∈ outputs
+
+            trace : Trace idx₁ idx₂ ρ₁ ρ₂