Prove that variables in a program all come from the program's code

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

Language.agda

@@ -3,12 +3,14 @@ module Language where
 open import Data.Nat using (ℕ; suc; pred)
 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.Vec using (Vec; foldr; lookup; _∷_)
 open import Data.List using ([]; _∷_; List) renaming (foldr to foldrˡ; map to mapˡ)
+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₁) renaming (_≟_ to _≟ᶠ_)
 open import Data.Fin.Properties using (suc-injective)
-open import Relation.Binary.PropositionalEquality using (cong; _≡_)
+open import Relation.Binary.PropositionalEquality using (cong; _≡_; refl)
 open import Relation.Nullary using (¬_)
 open import Function using (_∘_)
 
@@ -30,18 +32,110 @@ open import Lattice.MapSet String _≟ˢ_
         ; insert to insertˢ
         ; to-List to to-Listˢ
         ; empty to emptyˢ
+        ; singleton to singletonˢ
         ; _⊔_ to _⊔ˢ_
+        ; `_ to `ˢ_
+        ; _∈_ to _∈ˢ_
+        ; ⊔-preserves-∈k₁ to ⊔ˢ-preserves-∈k₁
+        ; ⊔-preserves-∈k₂ to ⊔ˢ-preserves-∈k₂
         )
 
+data _∈ᵉ_ : String → Expr → Set where
+    in⁺₁ : ∀ {e₁ e₂ : Expr} {k : String} → k ∈ᵉ e₁ → k ∈ᵉ (e₁ + e₂)
+    in⁺₂ : ∀ {e₁ e₂ : Expr} {k : String} → k ∈ᵉ e₂ → k ∈ᵉ (e₁ + e₂)
+    in⁻₁ : ∀ {e₁ e₂ : Expr} {k : String} → k ∈ᵉ e₁ → k ∈ᵉ (e₁ - e₂)
+    in⁻₂ : ∀ {e₁ e₂ : Expr} {k : String} → k ∈ᵉ e₂ → k ∈ᵉ (e₁ - e₂)
+    here : ∀ {k : String} → k ∈ᵉ (` k)
+
+data _∈ᵗ_ : String → Stmt → Set where
+    in←₁ : ∀ {k : String} {e : Expr} → k ∈ᵗ (k ← e)
+    in←₂ : ∀ {k k' : String} {e : Expr} → k ∈ᵉ e → k ∈ᵗ (k' ← e)
+
 private
     Expr-vars : Expr → StringSet
     Expr-vars (l + r) = Expr-vars l ⊔ˢ Expr-vars r
     Expr-vars (l - r) = Expr-vars l ⊔ˢ Expr-vars r
-    Expr-vars (` s) = insertˢ s emptyˢ
+    Expr-vars (` s) = singletonˢ s
     Expr-vars (# _) = emptyˢ
 
+    ∈-Expr-vars⇒∈ : ∀ {k : String} (e : Expr) → k ∈ˢ (Expr-vars e) → k ∈ᵉ e
+    ∈-Expr-vars⇒∈ {k} (e₁ + e₂) k∈vs
+        with Expr-Provenance k ((`ˢ (Expr-vars e₁)) ∪ (`ˢ (Expr-vars e₂))) k∈vs
+    ...   | in₁ (single k,tt∈vs₁) _ = (in⁺₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁)))
+    ...   | in₂ _ (single k,tt∈vs₂) = (in⁺₂ (∈-Expr-vars⇒∈ e₂ (forget k,tt∈vs₂)))
+    ...   | bothᵘ (single k,tt∈vs₁) _ = (in⁺₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁)))
+    ∈-Expr-vars⇒∈ {k} (e₁ - e₂) k∈vs
+        with Expr-Provenance k ((`ˢ (Expr-vars e₁)) ∪ (`ˢ (Expr-vars e₂))) k∈vs
+    ...   | in₁ (single k,tt∈vs₁) _ = (in⁻₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁)))
+    ...   | in₂ _ (single k,tt∈vs₂) = (in⁻₂ (∈-Expr-vars⇒∈ e₂ (forget k,tt∈vs₂)))
+    ...   | bothᵘ (single k,tt∈vs₁) _ = (in⁻₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁)))
+    ∈-Expr-vars⇒∈ {k} (` k) (RelAny.here refl) = here
+
+    ∈⇒∈-Expr-vars : ∀ {k : String} {e : Expr} → k ∈ᵉ e → k ∈ˢ (Expr-vars e)
+    ∈⇒∈-Expr-vars {k} {e₁ + e₂} (in⁺₁ k∈e₁) =
+        ⊔ˢ-preserves-∈k₁ {m₁ = Expr-vars e₁}
+                         {m₂ = Expr-vars e₂}
+                         (∈⇒∈-Expr-vars k∈e₁)
+    ∈⇒∈-Expr-vars {k} {e₁ + e₂} (in⁺₂ k∈e₂) =
+        ⊔ˢ-preserves-∈k₂ {m₁ = Expr-vars e₁}
+                         {m₂ = Expr-vars e₂}
+                         (∈⇒∈-Expr-vars k∈e₂)
+    ∈⇒∈-Expr-vars {k} {e₁ - e₂} (in⁻₁ k∈e₁) =
+        ⊔ˢ-preserves-∈k₁ {m₁ = Expr-vars e₁}
+                         {m₂ = Expr-vars e₂}
+                         (∈⇒∈-Expr-vars k∈e₁)
+    ∈⇒∈-Expr-vars {k} {e₁ - e₂} (in⁻₂ k∈e₂) =
+        ⊔ˢ-preserves-∈k₂ {m₁ = Expr-vars e₁}
+                         {m₂ = Expr-vars e₂}
+                         (∈⇒∈-Expr-vars k∈e₂)
+    ∈⇒∈-Expr-vars here = RelAny.here refl
+
     Stmt-vars : Stmt → StringSet
-    Stmt-vars (x ← e) = insertˢ x (Expr-vars e)
+    Stmt-vars (x ← e) = (singletonˢ x) ⊔ˢ (Expr-vars e)
+
+    ∈-Stmt-vars⇒∈ : ∀ {k : String} (s : Stmt) → k ∈ˢ (Stmt-vars s) → k ∈ᵗ s
+    ∈-Stmt-vars⇒∈ {k} (k' ← e) k∈vs
+        with Expr-Provenance k ((`ˢ (singletonˢ k')) ∪ (`ˢ (Expr-vars e))) k∈vs
+    ...   | in₁ (single (RelAny.here refl)) _ = in←₁
+    ...   | in₂ _ (single k,tt∈vs') = in←₂ (∈-Expr-vars⇒∈ e (forget k,tt∈vs'))
+    ...   | bothᵘ (single (RelAny.here refl)) _ = in←₁
+
+    ∈⇒∈-Stmt-vars : ∀ {k : String} {s : Stmt} → k ∈ᵗ s → k ∈ˢ (Stmt-vars s)
+    ∈⇒∈-Stmt-vars {k} {k ← e} in←₁ =
+        ⊔ˢ-preserves-∈k₁ {m₁ = singletonˢ k}
+                         {m₂ = Expr-vars e}
+                         (RelAny.here refl)
+    ∈⇒∈-Stmt-vars {k} {k' ← e} (in←₂ k∈e) =
+        ⊔ˢ-preserves-∈k₂ {m₁ = singletonˢ k'}
+                         {m₂ = Expr-vars e}
+                         (∈⇒∈-Expr-vars k∈e)
+
+    Stmts-vars : ∀ {n : ℕ} → Vec Stmt n → StringSet
+    Stmts-vars = foldr (λ n → StringSet)
+                       (λ {k} stmt acc → (Stmt-vars stmt) ⊔ˢ acc) emptyˢ
+
+    ∈-Stmts-vars⇒∈ : ∀ {n : ℕ} {k : String} (ss : Vec Stmt n) →
+                     k ∈ˢ (Stmts-vars ss) → Σ (Fin n) (λ f → k ∈ᵗ lookup ss f)
+    ∈-Stmts-vars⇒∈ {suc n'} {k} (s ∷ ss') k∈vss
+        with Expr-Provenance k ((`ˢ (Stmt-vars s)) ∪ (`ˢ (Stmts-vars ss'))) k∈vss
+    ...   | in₁ (single k,tt∈vs) _ = (zero , ∈-Stmt-vars⇒∈ s (forget k,tt∈vs))
+    ...   | in₂ _ (single k,tt∈vss') =
+            let
+                (f' , k∈s') = ∈-Stmts-vars⇒∈ ss' (forget k,tt∈vss')
+            in
+                (suc f' , k∈s')
+    ...   | bothᵘ (single k,tt∈vs) _ = (zero , ∈-Stmt-vars⇒∈ s (forget k,tt∈vs))
+
+    ∈⇒∈-Stmts-vars : ∀ {n : ℕ} {k : String} {ss : Vec Stmt n} {f : Fin n} →
+                     k ∈ᵗ lookup ss f → k ∈ˢ (Stmts-vars ss)
+    ∈⇒∈-Stmts-vars {suc n} {k} {s ∷ ss'} {zero} k∈s =
+        ⊔ˢ-preserves-∈k₁ {m₁ = Stmt-vars s}
+                         {m₂ = Stmts-vars ss'}
+                         (∈⇒∈-Stmt-vars k∈s)
+    ∈⇒∈-Stmts-vars {suc n} {k} {s ∷ ss'} {suc f'} k∈ss' =
+        ⊔ˢ-preserves-∈k₂ {m₁ = Stmt-vars s}
+                         {m₂ = Stmts-vars ss'}
+                         (∈⇒∈-Stmts-vars {n} {k} {ss'} {f'} k∈ss')
 
     -- Creating a new number from a natural number can never create one
     -- equal to one you get from weakening the bounds on another number.
@@ -71,8 +165,7 @@ record Program : Set where
 
     private
         vars-Set : StringSet
-        vars-Set = foldr (λ n → StringSet)
+        vars-Set = Stmts-vars stmts
-                         (λ {k} stmt acc → (Stmt-vars stmt) ⊔ˢ acc) emptyˢ stmts
 
     vars : List String
     vars = to-Listˢ vars-Set
@@ -83,15 +176,18 @@ record Program : Set where
     State : Set
     State = Fin length
 
-    code : State → Stmt
-    code = lookup stmts
-
     states : List State
     states = proj₁ (indices length)
 
     states-Unique : Unique states
     states-Unique = proj₂ (indices length)
 
+    code : State → Stmt
+    code = lookup stmts
+
+    vars-complete : ∀ {k : String} (s : State) → k ∈ᵗ (code s) → k ∈ˡ vars
+    vars-complete {k} s = ∈⇒∈-Stmts-vars {length} {k} {stmts} {s}
+
     _≟_ : IsDecidable (_≡_ {_} {State})
     _≟_ = _≟ᶠ_
 

Lattice/Map.agda

@@ -553,11 +553,18 @@ open ImplInsert _⊔₂_ using
     ; union-preserves-∈₂
     ; union-preserves-∉
     ; union-preserves-∈k₁
+    ; union-preserves-∈k₂
     )
 
 ⊔-combines : ∀ {k : A} {v₁ v₂ : B} {m₁ m₂ : Map} → (k , v₁) ∈ m₁ → (k , v₂) ∈ m₂ → (k , v₁ ⊔₂ v₂) ∈ (m₁ ⊔ m₂)
 ⊔-combines {k} {v₁} {v₂} {kvs₁ , u₁} {kvs₂ , u₂} k,v₁∈m₁ k,v₂∈m₂ = union-combines u₁ u₂ k,v₁∈m₁ k,v₂∈m₂
 
+⊔-preserves-∈k₁ : ∀ {k : A} → {m₁ m₂ : Map} → k ∈k m₁ → k ∈k (m₁ ⊔ m₂)
+⊔-preserves-∈k₁ {k} {(l₁ , _)} {(l₂ , _)} k∈km₁ = union-preserves-∈k₁ {l₁ = l₁} {l₂ = l₂} k∈km₁
+
+⊔-preserves-∈k₂ : ∀ {k : A} → {m₁ m₂ : Map} → k ∈k m₂ → k ∈k (m₁ ⊔ m₂)
+⊔-preserves-∈k₂ {k} {(l₁ , _)} {(l₂ , _)} k∈km₁ = union-preserves-∈k₂ {l₁ = l₁} {l₂ = l₂} k∈km₁
+
 open ImplInsert _⊓₂_ using
     ( restrict-needs-both
     ; updates

Lattice/MapSet.agda

@@ -6,18 +6,28 @@ open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
 module Lattice.MapSet {a : Level} (A : Set a) (≡-dec-A : Decidable (_≡_ {a} {A})) where
 
 open import Data.List using (List; map)
-open import Data.Product using (proj₁)
+open import Data.Product using (_,_; proj₁)
 open import Function using (_∘_)
 
 open import Lattice.Unit using (⊤; tt) renaming (_≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_; isLattice to ⊤-isLattice)
 import Lattice.Map
 
 private module UnitMap = Lattice.Map A ⊤ _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A ⊤-isLattice
-open UnitMap using (Map)
+open UnitMap
-open UnitMap using
+    using (Map; Expr; ⟦_⟧)
-    ( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_; empty
+    renaming
+        ( Expr-Provenance to Expr-Provenanceᵐ
+        )
+open UnitMap
+    using
+        ( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_; _∪_ ; _∩_ ; `_; empty; forget
         ; isUnionSemilattice; isIntersectSemilattice; isLattice; lattice
-    ) public
+        ; Provenance
+        ; ⊔-preserves-∈k₁
+        ; ⊔-preserves-∈k₂
+        )
+    renaming (_∈k_ to _∈_) public
+open Provenance public
 
 MapSet : Set a
 MapSet = Map
@@ -27,3 +37,9 @@ to-List = map proj₁ ∘ proj₁
 
 insert : A → MapSet → MapSet
 insert k = UnitMap.insert k tt
+
+singleton : A → MapSet
+singleton k = UnitMap.insert k tt empty
+
+Expr-Provenance : ∀ (k : A) (e : Expr) → k ∈ ⟦ e ⟧ → Provenance k tt e
+Expr-Provenance k e k∈e = let (tt , (prov , _)) = Expr-Provenanceᵐ k e k∈e in prov