From f21ebdcf467dfdb85f5e5a177f03f4ea21a6fe0a Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 10 Mar 2024 18:13:01 -0700 Subject: [PATCH] Start working on the evaluation operation. Proving monotonicity is the main hurdle here. Signed-off-by: Danila Fedorin --- Analysis/Sign.agda | 43 ++++++++++++++++++++++++++++++++++++- Language.agda | 9 +++++++- Lattice/FiniteMap.agda | 6 ++++++ Lattice/FiniteValueMap.agda | 5 ++--- Utils.agda | 5 +++++ 5 files changed, 63 insertions(+), 5 deletions(-) diff --git a/Analysis/Sign.agda b/Analysis/Sign.agda index d572668..9781bd8 100644 --- a/Analysis/Sign.agda +++ b/Analysis/Sign.agda @@ -1,9 +1,11 @@ module Analysis.Sign where open import Data.String using (String) renaming (_≟_ to _≟ˢ_) +open import Data.Nat using (suc) open import Data.Product using (_×_; proj₁; _,_) open import Data.List using (List; _∷_; []; foldr; cartesianProduct; cartesianProductWith) -open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans) +open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst) open import Relation.Nullary using (¬_; Dec; yes; no) open import Data.Unit using (⊤) @@ -108,6 +110,10 @@ module _ (prog : Program) where ; _≈_ to _≈ᵛ_ ; _⊔_ to _⊔ᵛ_ ; ≈-dec to ≈ᵛ-dec + ; _∈_ to _∈ᵛ_ + ; _∈k_ to _∈kᵛ_ + ; _updating_via_ to _updatingᵛ_via_ + ; locate to locateᵛ ) open FiniteHeightLattice finiteHeightLatticeᵛ using () @@ -129,6 +135,8 @@ module _ (prog : Program) where ( finiteHeightLattice to finiteHeightLatticeᵐ ; FiniteMap to StateVariables ; isLattice to isLatticeᵐ + ; _∈k_ to _∈kᵐ_ + ; locate to locateᵐ ) open FiniteHeightLattice finiteHeightLatticeᵐ using () @@ -159,3 +167,36 @@ module _ (prog : Program) where ( f' to joinAll ; f'-Monotonic to joinAll-Mono ) + + -- With 'join' in hand, we need to perform abstract evaluation. + + vars-in-Map : ∀ (k : String) (vs : VariableSigns) → + k ∈ˡ vars → k ∈kᵛ vs + vars-in-Map k vs@(m , kvs≡vars) k∈vars rewrite kvs≡vars = k∈vars + + states-in-Map : ∀ (s : State) (sv : StateVariables) → s ∈kᵐ sv + states-in-Map s sv@(m , ksv≡states) rewrite ksv≡states = states-complete s + + eval : ∀ (e : Expr) → (∀ k → k ∈ᵉ e → k ∈ˡ vars) → VariableSigns → SignLattice + eval (e₁ + e₂) k∈e⇒k∈vars vs = + plus (eval e₁ (λ k k∈e₁ → k∈e⇒k∈vars k (in⁺₁ k∈e₁)) vs) + (eval e₂ (λ k k∈e₂ → k∈e⇒k∈vars k (in⁺₂ k∈e₂)) vs) + eval (e₁ - e₂) k∈e⇒k∈vars vs = + minus (eval e₁ (λ k k∈e₁ → k∈e⇒k∈vars k (in⁻₁ k∈e₁)) vs) + (eval e₂ (λ k k∈e₂ → k∈e⇒k∈vars k (in⁻₂ k∈e₂)) vs) + eval (` k) k∈e⇒k∈vars vs = proj₁ (locateᵛ {k} {vs} (vars-in-Map k vs (k∈e⇒k∈vars k here))) + eval (# 0) _ _ = [ 0ˢ ]ᵍ + eval (# (suc n')) _ _ = [ + ]ᵍ + + updateForState : State → StateVariables → VariableSigns + updateForState s sv + with code s in p + ... | k ← e = + let + (vs , s,vs∈sv) = locateᵐ {s} {sv} (states-in-Map s sv) + k∈e⇒k∈codes = λ k k∈e → subst (λ stmt → k ∈ᵗ stmt) (sym p) (in←₂ k∈e) + k∈e⇒k∈vars = λ k k∈e → vars-complete s (k∈e⇒k∈codes k k∈e) + in + vs updatingᵛ (k ∷ []) via (λ _ → eval e k∈e⇒k∈vars vs) + + -- module Test = StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ joinAll joinAll-Mono diff --git a/Language.agda b/Language.agda index 1d18050..50c2ae9 100644 --- a/Language.agda +++ b/Language.agda @@ -15,7 +15,7 @@ open import Relation.Nullary using (¬_) open import Function using (_∘_) open import Lattice -open import Utils using (Unique; Unique-map; empty; push) +open import Utils using (Unique; Unique-map; empty; push; x∈xs⇒fx∈fxs) data Expr : Set where _+_ : Expr → Expr → Expr @@ -156,6 +156,10 @@ private , push (z≢mapsfs inds') (Unique-map suc suc-injective unids') ) + indices-complete : ∀ (n : ℕ) (f : Fin n) → f ∈ˡ (proj₁ (indices n)) + indices-complete (suc n') zero = RelAny.here refl + indices-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (indices-complete n' f')) + -- For now, just represent the program and CFG as one type, without branching. record Program : Set where @@ -179,6 +183,9 @@ record Program : Set where states : List State states = proj₁ (indices length) + states-complete : ∀ (s : State) → s ∈ˡ states + states-complete = indices-complete length + states-Unique : Unique states states-Unique = proj₂ (indices length) diff --git a/Lattice/FiniteMap.agda b/Lattice/FiniteMap.agda index 3dab758..48f7b00 100644 --- a/Lattice/FiniteMap.agda +++ b/Lattice/FiniteMap.agda @@ -69,9 +69,15 @@ module WithKeys (ks : List A) where km₁≡ks ) + _∈_ : A × B → FiniteMap → Set (a ⊔ℓ b) + _∈_ k,v (m₁ , _) = k,v ∈ˡ (proj₁ m₁) + _∈k_ : A → FiniteMap → Set a _∈k_ k (m₁ , _) = k ∈ˡ (keysᵐ m₁) + locate : ∀ {k : A} {fm : FiniteMap} → k ∈k fm → Σ B (λ v → (k , v) ∈ fm) + locate {k} {fm = (m , _)} k∈kfm = locateᵐ {k} {m} k∈kfm + _updating_via_ : FiniteMap → List A → (A → B) → FiniteMap _updating_via_ (m₁ , ksm₁≡ks) ks f = ( m₁ updatingᵐ ks via f diff --git a/Lattice/FiniteValueMap.agda b/Lattice/FiniteValueMap.agda index 287654d..d5e4bce 100644 --- a/Lattice/FiniteValueMap.agda +++ b/Lattice/FiniteValueMap.agda @@ -33,7 +33,6 @@ open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB using ( subset-impl ; locate; forget - ; _∈_ ; Map-functional ; Expr-Provenance ; Expr-Provenance-≡ @@ -103,7 +102,7 @@ module IterProdIsomorphism where _⊔ⁱᵖ_ {ks} = IP._⊔_ (length ks) _∈ᵐ_ : ∀ {ks : List A} → A × B → FiniteMap ks → Set - _∈ᵐ_ {ks} k,v fm = k,v ∈ proj₁ fm + _∈ᵐ_ {ks} = _∈_ ks -- The left inverse is: from (to x) = x from-to-inverseˡ : ∀ {ks : List A} (uks : Unique ks) → @@ -156,7 +155,7 @@ module IterProdIsomorphism where private first-key-in-map : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) → - Σ B (λ v → (k , v) ∈ proj₁ fm) + Σ B (λ v → (k , v) ∈ᵐ fm) first-key-in-map (((k , v) ∷ _ , _) , refl) = (v , here refl) from-first-value : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) → diff --git a/Utils.agda b/Utils.agda index 6c58ba4..825975b 100644 --- a/Utils.agda +++ b/Utils.agda @@ -54,6 +54,11 @@ All-x∈xs : ∀ {a} {A : Set a} (xs : List A) → All (λ x → x ∈ xs) xs All-x∈xs [] = [] All-x∈xs (x ∷ xs') = here refl ∷ map there (All-x∈xs xs') +x∈xs⇒fx∈fxs : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {x : A} {xs : List A} → + x ∈ xs → (f x) ∈ mapˡ f xs +x∈xs⇒fx∈fxs f (here refl) = here refl +x∈xs⇒fx∈fxs f (there x∈xs') = there (x∈xs⇒fx∈fxs f x∈xs') + iterate : ∀ {a} {A : Set a} (n : ℕ) → (f : A → A) → A → A iterate 0 _ a = a iterate (suc n) f a = f (iterate n f a)