From b134c143ca3140af0f35e2a75f869fe54942a201 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sat, 20 Apr 2024 21:37:28 -0700
Subject: [PATCH] Start working on proving 'sufficiency'

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Language/Properties.agda | 25 +++++++++++++++++++++++--
 MonotonicState.agda      |  4 ++--
 2 files changed, 25 insertions(+), 4 deletions(-)

diff --git a/Language/Properties.agda b/Language/Properties.agda
index c5dea39..e3138a4 100644
--- a/Language/Properties.agda
+++ b/Language/Properties.agda
@@ -3,15 +3,17 @@ module Language.Properties where
 open import Language.Base
 open import Language.Semantics
 open import Language.Graphs
+open import Language.Traces
 
 open import MonotonicState _⊆_ ⊆-trans renaming (MonotonicState to MonotonicGraphFunction)
+open import Utils using (_⊗_; _,_)
 open Relaxable {{...}}
 
 open import Data.Fin using (zero)
-open import Data.List using (List)
+open import Data.List using (List; _∷_; [])
 open import Data.Vec using (_∷_; [])
 open import Data.Vec.Properties using (cast-is-id; lookup-++ˡ; lookup-++ʳ)
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; subst)
 
 relax-preserves-[]≡ : ∀ (g₁ g₂ : Graph) (g₁⊆g₂ : g₁ ⊆ g₂) (idx : Graph.Index g₁) →
                       g₁ [ idx ] ≡ g₂ [ relax g₁⊆g₂ idx ]
@@ -29,3 +31,22 @@ instance
 
 pushBasicBlock-works : ∀ (bss : List BasicStmt) → Always (λ g idx → g [ idx ] ≡ bss) (pushBasicBlock bss)
 pushBasicBlock-works bss = MkAlways (λ g → lookup-++ʳ (Graph.nodes g) (bss ∷ []) zero)
+
+TransformsEnv : ∀ (ρ₁ ρ₂ : Env) → DependentPredicate (Graph.Index ⊗ Graph.Index)
+TransformsEnv ρ₁ ρ₂ g (idx₁ , idx₂) = Trace {g} idx₁ idx₂ ρ₁ ρ₂
+
+instance
+    TransformsEnvMonotonic : ∀ {ρ₁ ρ₂ : Env} → MonotonicPredicate (TransformsEnv ρ₁ ρ₂)
+    TransformsEnvMonotonic = {!!}
+
+buildCfg-sufficient : ∀ {ρ₁ ρ₂ : Env} {s : Stmt} → ρ₁ , s ⇒ˢ ρ₂ → Always (TransformsEnv ρ₁ ρ₂) (buildCfg s)
+buildCfg-sufficient {ρ₁} {ρ₂} {⟨ bs ⟩} (⇒ˢ-⟨⟩ ρ₁ ρ₂ bs ρ₁,bs⇒ρ₂) =
+    pushBasicBlock-works (bs ∷ [])
+    map-reason
+        (λ g idx g[idx]≡[bs] → Trace-single (subst (ρ₁ ,_⇒ᵇˢ ρ₂)
+                                                   (sym g[idx]≡[bs])
+                                                   (ρ₁,bs⇒ρ₂ ∷ [])))
+buildCfg-sufficient {ρ₁} {ρ₂} {s₁ then s₂} (⇒ˢ-then ρ₁ ρ ρ₂ s₁ s₂ ρ₁,s₁⇒ρ₂ ρ₂,s₂⇒ρ₃) =
+    (buildCfg-sufficient ρ₁,s₁⇒ρ₂ ⟨⊗⟩-reason buildCfg-sufficient ρ₂,s₂⇒ρ₃)
+    update-reason {!!}
+    map-reason {!!}
diff --git a/MonotonicState.agda b/MonotonicState.agda
index b126a0f..4830b3a 100644
--- a/MonotonicState.agda
+++ b/MonotonicState.agda
@@ -173,7 +173,7 @@ _map-reason_ : ∀ {T₁ T₂ : S → Set s}
                {P : DependentPredicate T₁} {Q : DependentPredicate T₂}
                {m : MonotonicState T₁}
                {f : ∀ (s : S) → T₁ s → T₂ s} →
-               Always P m → (∀ (s : S) (t₁ : T₁ s) (t₂ : T₂ s) → P s t₁ → Q s t₂) →
+               Always P m → (∀ (s : S) (t₁ : T₁ s) → P s t₁ → Q s (f s t₁)) →
                Always Q (m map f)
 _map-reason_ {P = P} {Q = Q} {m = m} {f = f} (MkAlways aP) P⇒Q =
     MkAlways impl
@@ -181,4 +181,4 @@ _map-reason_ {P = P} {Q = Q} {m = m} {f = f} (MkAlways aP) P⇒Q =
         impl : ∀ s₁ → let (s₂ , t , _) = (m map f) s₁ in Q s₂ t
         impl s
             with p ← aP s
-            with (s' , (t₁ , s≼s')) ← m s = P⇒Q s' t₁ (f s' t₁) p
+            with (s' , (t₁ , s≼s')) ← m s = P⇒Q s' t₁ p