Almost prove correctness

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

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