Successfully prove that monotonic updates preserve existing indices

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

Language.agda

@@ -1,20 +1,25 @@
 module Language where
 
 open import Data.Nat using (ℕ; suc; pred; _≤_) renaming (_+_ to _+ⁿ_)
-open import Data.Nat.Properties using (m≤n⇒m≤n+o; ≤-reflexive)
+open import Data.Nat.Properties using (m≤n⇒m≤n+o; ≤-reflexive; +-assoc; +-comm)
 open import Data.Integer using (ℤ; +_) renaming (_+_ to _+ᶻ_; _-_ to _-ᶻ_)
 open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
 open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
-open import Data.Vec using (Vec; foldr; lookup; _∷_; []; _++_)
-open import Data.List using ([]; _∷_; List) renaming (foldr to foldrˡ; map to mapˡ)
+open import Data.Vec using (Vec; foldr; lookup; _∷_; []; _++_; cast)
+open import Data.Vec.Properties using (++-assoc; ++-identityʳ; lookup-++ˡ)
+open import Data.Vec.Relation.Binary.Equality.Cast using (cast-is-id)
+open import Data.List using ([]; _∷_; List) renaming (foldr to foldrˡ; map to mapˡ; _++_ to _++ˡ_)
+open import Data.List.Properties using () renaming (++-assoc to ++ˡ-assoc; map-++ to mapˡ-++ˡ; ++-identityʳ to ++ˡ-identityʳ)
 open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
 open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any as RelAny using ()
-open import Data.Fin using (Fin; suc; zero; fromℕ; inject₁; inject≤; _↑ʳ_) renaming (_≟_ to _≟ᶠ_)
+open import Data.List.Relation.Unary.Any.Properties using (++⁺ʳ)
+open import Data.Fin using (Fin; suc; zero; fromℕ; inject₁; inject≤; _↑ʳ_; _↑ˡ_) renaming (_≟_ to _≟ᶠ_; cast to castᶠ)
 open import Data.Fin.Properties using (suc-injective)
-open import Relation.Binary.PropositionalEquality using (subst; cong; _≡_; refl)
+open import Relation.Binary.PropositionalEquality as Eq using (subst; cong; _≡_; sym; trans; refl)
 open import Relation.Nullary using (¬_)
 open import Function using (_∘_)
+open Eq.≡-Reasoning using (begin_; step-≡; _∎)
 
 open import Lattice
 open import Utils using (Unique; Unique-map; empty; push; x∈xs⇒fx∈fxs; _⊗_; _,_)
@@ -84,6 +89,7 @@ module Graphs where
     open Semantics
 
     record Graph : Set where
+        constructor MkGraph
         field
             size : ℕ
 
@@ -97,47 +103,54 @@ module Graphs where
             nodes : Vec (List BasicStmt) size
             edges : List Edge
 
+    ↑ˡ-Edge : ∀ {n} → (Fin n × Fin n) → ∀ m → (Fin (n +ⁿ m) × Fin (n +ⁿ m))
+    ↑ˡ-Edge (idx₁ , idx₂) m = (idx₁ ↑ˡ m , idx₂ ↑ˡ m)
+
     _[_] : ∀ (g : Graph) → Graph.Index g → List BasicStmt
     _[_] g idx = lookup (Graph.nodes g) idx
 
-    _⊆_ : Graph → Graph → Set
-    _⊆_ g₁ g₂ =
-        Σ (Graph.size g₁ ≤ Graph.size g₂) (λ n₁≤n₂ →
-            ( ∀ (idx : Graph.Index g₁) → g₁ [ idx ] ≡ g₂ [ inject≤ idx n₁≤n₂ ]
-            × ∀ (idx₁ idx₂ : Graph.Index g₁) → (idx₁ , idx₂) ∈ˡ (Graph.edges g₁) →
-                (inject≤ idx₁ n₁≤n₂ , inject≤ idx₂ n₁≤n₂) ∈ˡ (Graph.edges g₂)
-            ))
+    record _⊆_ (g₁ g₂ : Graph) : Set where
+        constructor Mk-⊆
+        field
+            n : ℕ
+            sg₂≡sg₁+n : Graph.size g₂ ≡ Graph.size g₁ +ⁿ n
+            g₁[]≡g₂[] : ∀ (idx : Graph.Index g₁) →
+                        lookup (Graph.nodes g₁) idx ≡
+                        lookup (cast sg₂≡sg₁+n (Graph.nodes g₂)) (idx ↑ˡ n)
+            e∈g₁⇒e∈g₂ : ∀ (e : Graph.Edge g₁) →
+                        e ∈ˡ (Graph.edges g₁) →
+                        (↑ˡ-Edge e n) ∈ˡ (subst (λ m → List (Fin m × Fin m)) sg₂≡sg₁+n (Graph.edges g₂))
 
-    -- Note: inject≤ doesn't seem to work as nicely with vector lookups.
-    --       The ↑ˡ and ↑ʳ operators are way nicer. Can we reformulate the
-    --       ⊆ property to use them?
+    flatten-casts : ∀ {s₁ s₂ s₃ n₁ n₂ : ℕ}
+                    (p : s₂ +ⁿ n₂ ≡ s₃) (q : s₁ +ⁿ n₁ ≡ s₂) (r : s₁ +ⁿ (n₁ +ⁿ n₂) ≡ s₃)
+                    (idx : Fin s₁) →
+                    castᶠ p ((castᶠ q (idx ↑ˡ n₁)) ↑ˡ n₂) ≡ castᶠ r (idx ↑ˡ (n₁ +ⁿ n₂))
+    flatten-casts refl refl r zero = refl
+    flatten-casts {(suc s₁)} {s₂} {s₃} {n₁} {n₂} refl refl r (suc idx')
+        rewrite flatten-casts refl refl (sym (+-assoc s₁ n₁ n₂)) idx' = refl
 
-    n≤n+m : ∀ (n m : ℕ) → n ≤ n +ⁿ m
-    n≤n+m n m = m≤n⇒m≤n+o m (≤-reflexive (refl {x = n}))
+    ⊆-trans : ∀ {g₁ g₂ g₃ : Graph} → g₁ ⊆ g₂ → g₂ ⊆ g₃ → g₁ ⊆ g₃
+    ⊆-trans {MkGraph s₁ ns₁ es₁} {MkGraph s₂ ns₂ es₂} {MkGraph s₃ ns₃ es₃}
+            (Mk-⊆ n₁ p₁@refl g₁[]≡g₂[] e∈g₁⇒e∈g₂) (Mk-⊆ n₂ p₂@refl g₂[]≡g₃[] e∈g₂⇒e∈g₃) = record
+        { n = n₁ +ⁿ n₂
+        ; sg₂≡sg₁+n = +-assoc s₁ n₁ n₂
+        ; g₁[]≡g₂[] = {!!}
+        ; e∈g₁⇒e∈g₂ = {!!}
+        --     lookup ns₁ idx ≡ lookup (cast p₁ ns₂) (idx ↑ˡ n) -- by g₁[]≡g₂[]
 
-    lookup-++ˡ : ∀ {a} {A : Set a} {n m : ℕ} (xs : Vec A n) (ys : Vec A m)
-                   (idx : Fin n) → lookup xs idx ≡ lookup (xs ++ ys) (inject≤ idx (n≤n+m n m))
-    lookup-++ˡ = {!!}
+        --     lookup (cast p₁ ns₂) (idx ↑ˡ n) ≡ lookup ns₂ (Fin.cast (sym p₁) (idx ↑ˡ n)) -- by lookup-cast₁
+        --                                                            -------- s₁ + n₁ → s₂
+        --                                                                     ---------- Fin (s₁ + n₁)
+        --                                                  ----------------------------- Fin s₂
 
-    pushBasicBlock : List BasicStmt → (g₁ : Graph) → Σ Graph (λ g₂ → Graph.Index g₂ × g₁ ⊆ g₂)
-    pushBasicBlock bss g₁ =
-        let
-            size' = Graph.size g₁ +ⁿ 1
-            size≤size' = n≤n+m (Graph.size g₁) 1
-            inject-Edge = λ (idx₁ , idx₂) → (inject≤ idx₁ size≤size' , inject≤ idx₂ size≤size')
-        in
-            ( record
-                { size = size'
-                ; nodes = Graph.nodes g₁ ++ (bss ∷ [])
-                ; edges = mapˡ inject-Edge (Graph.edges g₁)
-                }
-            , ( (Graph.size g₁) ↑ʳ zero
-              , ( size≤size'
-                , λ idx → lookup-++ˡ (Graph.nodes g₁) (bss ∷ []) idx
-                , λ idx₁ idx₂ e∈es → x∈xs⇒fx∈fxs inject-Edge e∈es
-                )
-              )
-            )
+        --     lookup ns₂ (Fin.cast (sym p₁) (idx ↑ˡ n)) ≡ lookup (cast p₂ ns₃) ((Fin.cast (sym p₁) (idx ↑ˡ n₁) ↑ˡ n₂)) -- by g₂[]≡g₃[]
+
+        --     lookup (cast p₂ ns₃) ((Fin.cast (sym p₁) (idx ↑ˡ n₁) ↑ˡ  n₂)) ≡ lookup ns₃ (Fin.cast (sym p₂) ((Fin.cast (sym p₁) (idx ↑ˡ n₁) ↑ˡ  n₂))) -- by lookup-cast₂
+
+        --     lookup ns₃ (Fin.cast (sym p₂) ((Fin.cast (sym p₁) (idx ↑ˡ n₁) ↑ˡ  n₂))) ≡ lookup ns₃ (Fin.cast (sym (+-assoc s₁ n₁ n₂)) (idx ↑ˡ (n₁ + n₂))) -- by flatten-casts
+        --
+        --     lookup ns₃ (Fin.cast (sym (+-assoc s₁ n₁ n₂)) (idx ↑ˡ (n₁ + n₂))) ≡ lookup (cast (+-assoc s₁ n₁ n₂) ns₃) (idx ↑ˡ (n₁ + n₂)) ∎
+        }
 
     record Relaxable (T : Graph → Set) : Set where
         field relax : ∀ {g₁ g₂ : Graph} → g₁ ⊆ g₂ → T g₁ → T g₂
@@ -145,14 +158,14 @@ module Graphs where
     instance
         IndexRelaxable : Relaxable Graph.Index
         IndexRelaxable = record
-            { relax = λ g₁⊆g₂ idx → inject≤ idx (proj₁ g₁⊆g₂)
+            { relax = λ { (Mk-⊆ n refl _ _) idx → idx ↑ˡ n }
             }
 
         EdgeRelaxable : Relaxable Graph.Edge
         EdgeRelaxable = record
-            { relax = λ {g₁} {g₂} g₁⊆g₂ (idx₁ , idx₂) →
-                ( Relaxable.relax IndexRelaxable {g₁} {g₂} g₁⊆g₂ idx₁
-                , Relaxable.relax IndexRelaxable {g₁} {g₂} g₁⊆g₂ idx₂
+            { relax = λ g₁⊆g₂ (idx₁ , idx₂) →
+                ( Relaxable.relax IndexRelaxable g₁⊆g₂ idx₁
+                , Relaxable.relax IndexRelaxable g₁⊆g₂ idx₂
                 )
             }
 
@@ -168,6 +181,92 @@ module Graphs where
 
     open Relaxable {{...}} public
 
+    relax-preserves-[]≡ : ∀ (g₁ g₂ : Graph) (g₁⊆g₂ : g₁ ⊆ g₂) (idx : Graph.Index g₁) →
+                          g₁ [ idx ] ≡ g₂ [ relax g₁⊆g₂ idx ]
+    relax-preserves-[]≡ g₁ g₂ (Mk-⊆ n refl g₁[]≡g₂[] _) idx =
+        trans (g₁[]≡g₂[] idx) (cong (λ vec → lookup vec (idx ↑ˡ n))
+                                    (cast-is-id refl (Graph.nodes g₂)))
+
+    MonotonicGraphFunction : (Graph → Set) → Set
+    MonotonicGraphFunction T = (g₁ : Graph) → Σ Graph (λ g₂ → T g₂ × g₁ ⊆ g₂)
+
+    infixr 2 _⟨⊗⟩_
+    _⟨⊗⟩_ : ∀ {T₁ T₂ : Graph → Set} {{ T₁Relaxable : Relaxable T₁ }} →
+          MonotonicGraphFunction T₁ → MonotonicGraphFunction T₂ →
+          MonotonicGraphFunction (T₁ ⊗ T₂)
+    _⟨⊗⟩_ {{r}} f₁ f₂ g
+        with (g' , (t₁ , g⊆g')) ← f₁ g
+        with (g'' , (t₂ , g'⊆g'')) ← f₂ g' =
+        (g'' , ((Relaxable.relax r g'⊆g'' t₁ , t₂) , ⊆-trans g⊆g' g'⊆g''))
+
+    infixl 2 _update_
+    _update_ : ∀ {T : Graph → Set} {{ TRelaxable : Relaxable T }} →
+             MonotonicGraphFunction T → (∀ (g : Graph) → T g → Σ Graph (λ g' → g ⊆ g')) →
+             MonotonicGraphFunction T
+    _update_ {{r}} f mod g
+        with (g' , (t , g⊆g')) ← f g
+        with (g'' , g'⊆g'') ← mod g' t =
+        (g'' , ((Relaxable.relax r g'⊆g'' t , ⊆-trans g⊆g' g'⊆g'')))
+
+    infixl 2 _map_
+    _map_ : ∀ {T₁ T₂ : Graph → Set} →
+          MonotonicGraphFunction T₁ → (∀ (g : Graph) → T₁ g → T₂ g) →
+          MonotonicGraphFunction T₂
+    _map_ f fn g = let (g' , (t₁ , g⊆g')) = f g in (g' , (fn g' t₁ , g⊆g'))
+
+    module Construction where
+        pushBasicBlock : List BasicStmt → MonotonicGraphFunction Graph.Index
+        pushBasicBlock bss g =
+            ( record
+                { size = Graph.size g +ⁿ 1
+                ; nodes = Graph.nodes g ++ (bss ∷ [])
+                ; edges = mapˡ (λ e → ↑ˡ-Edge e 1) (Graph.edges g)
+                }
+            , ( Graph.size g ↑ʳ zero
+              , record
+                  { n = 1
+                  ; sg₂≡sg₁+n = refl
+                  ; g₁[]≡g₂[] = λ idx → trans (sym (lookup-++ˡ (Graph.nodes g) (bss ∷ []) idx)) (sym (cong (λ vec → lookup vec (idx ↑ˡ 1)) (cast-is-id refl (Graph.nodes g ++ (bss ∷ [])))))
+                  ; e∈g₁⇒e∈g₂ = λ e e∈g₁ → x∈xs⇒fx∈fxs (λ e' → ↑ˡ-Edge e' 1) e∈g₁
+                  }
+              )
+            )
+
+        addEdges : ∀ (g : Graph) → List (Graph.Edge g) → Σ Graph (λ g' → g ⊆ g')
+        addEdges g es =
+            ( record
+                { size = Graph.size g
+                ; nodes = Graph.nodes g
+                ; edges = es ++ˡ Graph.edges g
+                }
+            , record
+                { n = 0
+                ; sg₂≡sg₁+n = +-comm 0 (Graph.size g)
+                ; g₁[]≡g₂[] = {!!}
+                ; e∈g₁⇒e∈g₂ = {!!}
+                }
+            )
+
+        pushEmptyBlock : MonotonicGraphFunction Graph.Index
+        pushEmptyBlock = pushBasicBlock []
+
+        buildCfg : Stmt → MonotonicGraphFunction (Graph.Index ⊗ Graph.Index)
+        buildCfg ⟨ bs₁ ⟩ = pushBasicBlock (bs₁ ∷ []) map (λ g idx → (idx , idx))
+        buildCfg (s₁ then s₂) =
+            (buildCfg s₁ ⟨⊗⟩ buildCfg s₂)
+            update (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄)) → addEdges g ((idx₂ , idx₃) ∷ []) })
+            map (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄)) → (idx₁ , idx₄) })
+        buildCfg (if _ then s₁ else s₂) =
+            (buildCfg s₁ ⟨⊗⟩ buildCfg s₂ ⟨⊗⟩ pushEmptyBlock ⟨⊗⟩ pushEmptyBlock)
+            update (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄) , idx , idx') →
+                      addEdges g ((idx , idx₁) ∷ (idx , idx₃) ∷ (idx₂ , idx') ∷ (idx₄ , idx') ∷ []) })
+            map (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄) , idx , idx') → (idx , idx') })
+        buildCfg (while _ repeat s) =
+            (buildCfg s ⟨⊗⟩ pushEmptyBlock ⟨⊗⟩ pushEmptyBlock)
+            update (λ { g ((idx₁ , idx₂) , idx , idx') →
+                      addEdges g ((idx , idx') ∷ (idx₂ , idx) ∷ []) })
+            map (λ { g ((idx₁ , idx₂) , idx , idx') → (idx , idx') })
+
 open import Lattice.MapSet _≟ˢ_
     renaming
         ( MapSet to StringSet

Utils.agda

@@ -69,5 +69,6 @@ data Pairwise {a} {b} {c} {A : Set a} {B : Set b} (P : A → B → Set c) : List
           P x y → Pairwise P xs ys →
           Pairwise P (x ∷ xs) (y ∷ ys)
 
+infixr 2 _⊗_
 data _⊗_ {a p q} {A : Set a} (P : A → Set p) (Q : A → Set q) : A → Set (a ⊔ℓ p ⊔ℓ q) where
     _,_ : ∀ {val : A} → P val → Q val → (P ⊗ Q) val