From 8a85c4497cb78b63d67b9061eada168bcd8361fd Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 10 Mar 2024 21:25:46 -0700 Subject: [PATCH] Prove that evaluation is monotonic and complete sign analysis Other than monotonicity of plus and minus, god damn it. Signed-off-by: Danila Fedorin --- Analysis/Sign.agda | 57 ++++++++++++++++++++++++++++++++++++---------- 1 file changed, 45 insertions(+), 12 deletions(-) diff --git a/Analysis/Sign.agda b/Analysis/Sign.agda index e7bf084..14a0ceb 100644 --- a/Analysis/Sign.agda +++ b/Analysis/Sign.agda @@ -103,8 +103,9 @@ module _ (prog : Program) where open Program prog -- The variable -> sign map is a finite value-map with keys strings. Use a bundle to avoid explicitly specifying operators. - open Lattice.FiniteValueMap.WithKeys _≟ˢ_ isLatticeᵍ vars - using (m₁≼m₂⇒m₁[k]≼m₂[k]) + module VariableSignsFiniteMap = Lattice.FiniteValueMap.WithKeys _≟ˢ_ isLatticeᵍ vars + open VariableSignsFiniteMap + using () renaming ( FiniteMap to VariableSigns ; isLattice to isLatticeᵛ @@ -116,6 +117,7 @@ module _ (prog : Program) where ; _∈k_ to _∈kᵛ_ ; _updating_via_ to _updatingᵛ_via_ ; locate to locateᵛ + ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ ) open IsLattice isLatticeᵛ using () @@ -145,13 +147,17 @@ module _ (prog : Program) where ; _∈k_ to _∈kᵐ_ ; locate to locateᵐ ; _≼_ to _≼ᵐ_ + ; ≈₂-dec⇒≈-dec to ≈ᵛ-dec⇒≈ᵐ-dec + ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ ) open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟_ isLatticeᵛ states-Unique ≈ᵛ-dec _ fixedHeightᵛ using () renaming - ( isFiniteHeightLattice to isFiniteHeightLatticeᵛ + ( isFiniteHeightLattice to isFiniteHeightLatticeᵐ ) + ≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec + -- build up the 'join' function, which follows from Exercise 4.26's -- -- L₁ → (A → L₂) @@ -201,6 +207,7 @@ module _ (prog : Program) where eval-Mono : ∀ (e : Expr) (k∈e⇒k∈vars : ∀ k → k ∈ᵉ e → k ∈ˡ vars) → Monotonic _≼ᵛ_ _≼ᵍ_ (eval e k∈e⇒k∈vars) eval-Mono (e₁ + e₂) k∈e⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂ = let + -- TODO: can this be done with less boilerplate? k∈e₁⇒k∈vars = λ k k∈e₁ → k∈e⇒k∈vars k (in⁺₁ k∈e₁) k∈e₂⇒k∈vars = λ k k∈e₂ → k∈e⇒k∈vars k (in⁺₂ k∈e₂) g₁vs₁ = eval e₁ k∈e₁⇒k∈vars vs₁ @@ -214,6 +221,7 @@ module _ (prog : Program) where (plus-Monoʳ g₁vs₂ {g₂vs₁} {g₂vs₂} (eval-Mono e₂ k∈e₂⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂)) eval-Mono (e₁ - e₂) k∈e⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂ = let + -- TODO: here too -- can this be done with less boilerplate? k∈e₁⇒k∈vars = λ k k∈e₁ → k∈e⇒k∈vars k (in⁻₁ k∈e₁) k∈e₂⇒k∈vars = λ k k∈e₂ → k∈e⇒k∈vars k (in⁻₂ k∈e₂) g₁vs₁ = eval e₁ k∈e₁⇒k∈vars vs₁ @@ -230,24 +238,49 @@ module _ (prog : Program) where (v₁ , k,v₁∈vs₁) = locateᵛ {k} {vs₁} (vars-in-Map k vs₁ (k∈e⇒k∈vars k here)) (v₂ , k,v₂∈vs₂) = locateᵛ {k} {vs₂} (vars-in-Map k vs₂ (k∈e⇒k∈vars k here)) in - m₁≼m₂⇒m₁[k]≼m₂[k] vs₁ vs₂ vs₁≼vs₂ k,v₁∈vs₁ k,v₂∈vs₂ + m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ vs₁ vs₂ vs₁≼vs₂ k,v₁∈vs₁ k,v₂∈vs₂ eval-Mono (# 0) _ _ = ≈ᵍ-refl eval-Mono (# (suc n')) _ _ = ≈ᵍ-refl + private module _ (k : String) (e : Expr) (k∈e⇒k∈vars : ∀ k → k ∈ᵉ e → k ∈ˡ vars) where + open VariableSignsFiniteMap.GeneralizedUpdate vars isLatticeᵛ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) (λ _ → eval e k∈e⇒k∈vars) (λ _ → eval-Mono e k∈e⇒k∈vars) (k ∷ []) + renaming + ( f' to updateVariablesFromExpression + ; f'-Monotonic to updateVariablesFromExpression-Mono + ) + public - updateForState : State → StateVariables → VariableSigns - updateForState s sv - with code s in p - ... | k ← e = + updateVariablesForState : State → StateVariables → VariableSigns + updateVariablesForState s sv + -- More weirdness here. Apparently, capturing the with-equality proof + -- using 'in p' makes code that reasons about this function (below) + -- throw ill-typed with-abstraction errors. Instead, make use of the + -- fact that later with-clauses are generalized over earlier ones to + -- construct a specialization of vars-complete for (code s). + with code s | (λ k → vars-complete {k} s) + ... | k ← e | k∈codes⇒k∈vars = 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) + updateVariablesFromExpression k e (λ k k∈e → k∈codes⇒k∈vars k (in←₂ k∈e)) vs - open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ joinAll (λ {a₁} {a₂} a₁≼a₂ → joinAll-Mono {a₁} {a₂} a₁≼a₂) updateForState {!!} states + updateVariablesForState-Monoʳ : ∀ (s : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (updateVariablesForState s) + updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂ + with code s | (λ k → vars-complete {k} s) + ... | k ← e | k∈codes⇒k∈vars = + let + (vs₁ , s,vs₁∈sv₁) = locateᵐ {s} {sv₁} (states-in-Map s sv₁) + (vs₂ , s,vs₂∈sv₂) = locateᵐ {s} {sv₂} (states-in-Map s sv₂) + vs₁≼vs₂ = m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ sv₁ sv₂ sv₁≼sv₂ s,vs₁∈sv₁ s,vs₂∈sv₂ + in + updateVariablesFromExpression-Mono k e (λ k k∈e → k∈codes⇒k∈vars k (in←₂ k∈e)) {vs₁} {vs₂} vs₁≼vs₂ + + open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ joinAll (λ {a₁} {a₂} a₁≼a₂ → joinAll-Mono {a₁} {a₂} a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states renaming ( f' to updateAll ; f'-Monotonic to updateAll-Mono ) + + open import Fixedpoint ≈ᵐ-dec isFiniteHeightLatticeᵐ updateAll (λ {m₁} {m₂} m₁≼m₂ → updateAll-Mono {m₁} {m₂} m₁≼m₂) + using () + renaming (aᶠ to signs)