From 0705df708e19694f1b5bda326d118bc32fe5751c Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 10 Mar 2024 16:41:21 -0700 Subject: [PATCH] Prove that variables in a program all come from the program's code Signed-off-by: Danila Fedorin --- Language.agda | 114 ++++++++++++++++++++++++++++++++++++++++---- Lattice/Map.agda | 7 +++ Lattice/MapSet.agda | 28 ++++++++--- 3 files changed, 134 insertions(+), 15 deletions(-) diff --git a/Language.agda b/Language.agda index 4b37771..1d18050 100644 --- a/Language.agda +++ b/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) - (λ {k} stmt acc → (Stmt-vars stmt) ⊔ˢ acc) emptyˢ stmts + vars-Set = Stmts-vars 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}) _≟_ = _≟ᶠ_ diff --git a/Lattice/Map.agda b/Lattice/Map.agda index 2c7daaf..f2d1364 100644 --- a/Lattice/Map.agda +++ b/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 diff --git a/Lattice/MapSet.agda b/Lattice/MapSet.agda index 17285da..2ce73c3 100644 --- a/Lattice/MapSet.agda +++ b/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 using - ( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_; empty - ; isUnionSemilattice; isIntersectSemilattice; isLattice; lattice - ) public +open UnitMap + using (Map; Expr; ⟦_⟧) + renaming + ( Expr-Provenance to Expr-Provenanceᵐ + ) +open UnitMap + using + ( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_; _∪_ ; _∩_ ; `_; empty; forget + ; isUnionSemilattice; isIntersectSemilattice; isLattice; lattice + ; 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