From f84a1c923c14d982abcedaef60d66a06cf737d7a Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 9 Mar 2024 23:06:47 -0800 Subject: [PATCH] Prove that the 'join' transformation is monotonic Signed-off-by: Danila Fedorin --- Analysis/Sign.agda | 54 ++++++++++++++++++++++++++++++++++++++++-- Language.agda | 12 ++++++++++ Lattice.agda | 2 +- Lattice/FiniteMap.agda | 25 +++++++++---------- 4 files changed, 78 insertions(+), 15 deletions(-) diff --git a/Analysis/Sign.agda b/Analysis/Sign.agda index e259b4e..f8cfd96 100644 --- a/Analysis/Sign.agda +++ b/Analysis/Sign.agda @@ -1,11 +1,14 @@ module Analysis.Sign where open import Data.String using (String) renaming (_≟_ to _≟ˢ_) +open import Data.Product using (proj₁) +open import Data.List using (foldr) open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans) open import Relation.Nullary using (¬_; Dec; yes; no) open import Language open import Lattice +open import Utils using (Pairwise) import Lattice.Bundles.FiniteValueMap private module FixedHeightFiniteMap = Lattice.Bundles.FiniteValueMap.FromFiniteHeightLattice @@ -31,7 +34,9 @@ module _ (prog : Program) where open Program prog -- embelish 'sign' with a top and bottom element. - open import Lattice.AboveBelow Sign _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵍ_ as AB renaming (AboveBelow to SignLattice; ≈-dec to ≈ᵍ-dec) + open import Lattice.AboveBelow Sign _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵍ_ as AB + using () + renaming (AboveBelow to SignLattice; ≈-dec to ≈ᵍ-dec) -- 'sign' has no underlying lattice structure, so use the 'plain' above-below lattice. open AB.Plain using () renaming (finiteHeightLattice to finiteHeightLatticeᵍ-if-inhabited) @@ -40,16 +45,61 @@ module _ (prog : Program) where -- The variable -> sign map is a finite value-map with keys strings. Use a bundle to avoid explicitly specifying operators. open FixedHeightFiniteMap String SignLattice _≟ˢ_ finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec + using () renaming ( finiteHeightLattice to finiteHeightLatticeᵛ ; FiniteMap to VariableSigns ; _≈_ to _≈ᵛ_ + ; _⊔_ to _⊔ᵛ_ ; ≈-dec to ≈ᵛ-dec ) + open FiniteHeightLattice finiteHeightLatticeᵛ + using () + renaming + ( ⊔-Monotonicˡ to ⊔ᵛ-Monotonicˡ + ; ⊔-Monotonicʳ to ⊔ᵛ-Monotonicʳ + ; _≼_ to _≼ᵛ_ + ; joinSemilattice to joinSemilatticeᵛ + ; ⊔-idemp to ⊔ᵛ-idemp + ) + + ⊥ᵛ = proj₁ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight finiteHeightLatticeᵛ))) -- Finally, the map we care about is (state -> (variables -> sign)). Bring that in. - open FixedHeightFiniteMap State VariableSigns _≟_ finiteHeightLatticeᵛ states-Unique ≈ᵛ-dec + module StateVariablesFiniteMap = FixedHeightFiniteMap State VariableSigns _≟_ finiteHeightLatticeᵛ states-Unique ≈ᵛ-dec + open StateVariablesFiniteMap + using (_[_]; m₁≼m₂⇒m₁[ks]≼m₂[ks]) renaming ( finiteHeightLattice to finiteHeightLatticeᵐ ; FiniteMap to StateVariables + ; isLattice to isLatticeᵐ + ) + open FiniteHeightLattice finiteHeightLatticeᵐ + using () + renaming (_≼_ to _≼ᵐ_) + + -- build up the 'join' function, which follows from Exercise 4.26's + -- + -- L₁ → (A → L₂) + -- + -- Construction, with L₁ = (A → L₂), and f = id + + joinForKey : State → StateVariables → VariableSigns + joinForKey k states = foldr _⊔ᵛ_ ⊥ᵛ (states [ incoming k ]) + + -- The per-key join is made up of map key accesses (which are monotonic) + -- and folds using the join operation (also monotonic) + + joinForKey-Mono : ∀ (k : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (joinForKey k) + joinForKey-Mono k {fm₁} {fm₂} fm₁≼fm₂ = + foldr-Mono joinSemilatticeᵛ joinSemilatticeᵛ (fm₁ [ incoming k ]) (fm₂ [ incoming k ]) _⊔ᵛ_ ⊥ᵛ ⊥ᵛ + (m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ (incoming k) fm₁≼fm₂) + (⊔ᵛ-idemp ⊥ᵛ) ⊔ᵛ-Monotonicʳ ⊔ᵛ-Monotonicˡ + + -- The name f' comes from the formulation of Exercise 4.26. + + open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) joinForKey joinForKey-Mono states + renaming + ( f' to joinAll + ; f'-Monotonic to joinAll-Mono ) diff --git a/Language.agda b/Language.agda index 97dcca7..d9d25e2 100644 --- a/Language.agda +++ b/Language.agda @@ -91,3 +91,15 @@ record Program : Set where _≟_ : IsDecidable (_≡_ {_} {State}) _≟_ = _≟ᶠ_ + + -- Computations for incoming and outgoing edged will have to change too + -- when we support branching etc. + + incoming : State → List State + incoming + with length + ... | 0 = (λ ()) + ... | suc n' = (λ + { zero → [] + ; (suc f') → (inject₁ f') ∷ [] + }) diff --git a/Lattice.agda b/Lattice.agda index c78ea7d..d51e919 100644 --- a/Lattice.agda +++ b/Lattice.agda @@ -124,7 +124,7 @@ module _ {a} {A : Set a} open IsSemilattice lA using (_≼_) id-Mono : Monotonic _≼_ _≼_ (λ x → x) - id-Mono a₁≼a₂ = a₁≼a₂ + id-Mono {a₁} {a₂} a₁≼a₂ = a₁≼a₂ module _ {a b} {A : Set a} {B : Set b} {_≈₁_ : A → A → Set a} {_⊔₁_ : A → A → A} diff --git a/Lattice/FiniteMap.agda b/Lattice/FiniteMap.agda index d8c3b3e..3dab758 100644 --- a/Lattice/FiniteMap.agda +++ b/Lattice/FiniteMap.agda @@ -132,23 +132,24 @@ module WithKeys (ks : List A) where ; isLattice = isLattice } - module _ {l} {L : Set l} + module GeneralizedUpdate + {l} {L : Set l} {_≈ˡ_ : L → L → Set l} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L} - (lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_) where + (lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_) + (f : L → FiniteMap) (f-Monotonic : Monotonic (IsLattice._≼_ lL) _≼_ f) + (g : A → L → B) (g-Monotonicʳ : ∀ k → Monotonic (IsLattice._≼_ lL) _≼₂_ (g k)) + (ks : List A) where + open IsLattice lL using () renaming (_≼_ to _≼ˡ_) - module _ (f : L → FiniteMap) (f-Monotonic : Monotonic _≼ˡ_ _≼_ f) - (g : A → L → B) (g-Monotonicʳ : ∀ k → Monotonic _≼ˡ_ _≼₂_ (g k)) - (ks : List A) where + updater : L → A → B + updater l k = g k l - updater : L → A → B - updater l k = g k l + f' : L → FiniteMap + f' l = (f l) updating ks via (updater l) - f' : L → FiniteMap - f' l = (f l) updating ks via (updater l) - - f'-Monotonic : Monotonic _≼ˡ_ _≼_ f' - f'-Monotonic {l₁} {l₂} l₁≼l₂ = f'-Monotonicᵐ lL (proj₁ ∘ f) f-Monotonic g g-Monotonicʳ ks l₁≼l₂ + f'-Monotonic : Monotonic _≼ˡ_ _≼_ f' + f'-Monotonic {l₁} {l₂} l₁≼l₂ = f'-Monotonicᵐ lL (proj₁ ∘ f) f-Monotonic g g-Monotonicʳ ks l₁≼l₂ all-equal-keys : ∀ (fm₁ fm₂ : FiniteMap) → (Map.keys (proj₁ fm₁) ≡ Map.keys (proj₁ fm₂)) all-equal-keys (fm₁ , km₁≡ks) (fm₂ , km₂≡ks) = trans km₁≡ks (sym km₂≡ks)