DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Tighten exported definitions in Forward.agda

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin
2024-12-31 00:29:39 -08:00
parent 10332351ea
commit b28994e1d2
1 changed files with 52 additions and 42 deletions
Download Patch File Download Diff File Expand all files Collapse all files

94
Analysis/Forward.agda
View File

@@ -78,10 +78,11 @@ module WithProg (prog : Program) where
; ⊥-contains-bottoms to ⊥ᵛ-contains-bottoms ; ⊥-contains-bottoms to ⊥ᵛ-contains-bottoms
) )
≈ᵛ-dec = ≈ˡ-dec⇒≈ᵛ-dec ≈ˡ-dec private
joinSemilatticeᵛ = IsFiniteHeightLattice.joinSemilattice isFiniteHeightLatticeᵛ ≈ᵛ-dec = ≈ˡ-dec⇒≈ᵛ-dec ≈ˡ-dec
fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ joinSemilatticeᵛ = IsFiniteHeightLattice.joinSemilattice isFiniteHeightLatticeᵛ
⊥ᵛ = Chain.Height.⊥ fixedHeightᵛ fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ
⊥ᵛ = Chain.Height.⊥ fixedHeightᵛ
-- Finally, the map we care about is (state -> (variables -> value)). Bring that in. -- Finally, the map we care about is (state -> (variables -> value)). Bring that in.
module StateVariablesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟_ isLatticeᵛ states module StateVariablesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟_ isLatticeᵛ states
@@ -109,45 +110,46 @@ module WithProg (prog : Program) where
( ≈-sym to ≈ᵐ-sym ( ≈-sym to ≈ᵐ-sym
) )
≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec private
fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ ≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec
fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ
-- We now have our (state -> (variables -> value)) map. -- We now have our (state -> (variables -> value)) map.
-- Define a couple of helpers to retrieve values from it. Specifically, -- Define a couple of helpers to retrieve values from it. Specifically,
-- since the State type is as specific as possible, it's always possible to -- since the State type is as specific as possible, it's always possible to
-- retrieve the variable values at each state. -- retrieve the variable values at each state.
states-in-Map : ∀ (s : State) (sv : StateVariables) → s ∈kᵐ sv states-in-Map : ∀ (s : State) (sv : StateVariables) → s ∈kᵐ sv
states-in-Map s sv@(m , ksv≡states) rewrite ksv≡states = states-complete s states-in-Map s sv@(m , ksv≡states) rewrite ksv≡states = states-complete s
variablesAt : State → StateVariables → VariableValues variablesAt : State → StateVariables → VariableValues
variablesAt s sv = proj₁ (locateᵐ {s} {sv} (states-in-Map s sv)) variablesAt s sv = proj₁ (locateᵐ {s} {sv} (states-in-Map s sv))
variablesAt-∈ : ∀ (s : State) (sv : StateVariables) → (s , variablesAt s sv) ∈ᵐ sv variablesAt-∈ : ∀ (s : State) (sv : StateVariables) → (s , variablesAt s sv) ∈ᵐ sv
variablesAt-∈ s sv = proj₂ (locateᵐ {s} {sv} (states-in-Map s sv)) variablesAt-∈ s sv = proj₂ (locateᵐ {s} {sv} (states-in-Map s sv))
variablesAt-≈ : ∀ s sv₁ sv₂ → sv₁ ≈ᵐ sv₂ → variablesAt s sv₁ ≈ᵛ variablesAt s sv₂ variablesAt-≈ : ∀ s sv₁ sv₂ → sv₁ ≈ᵐ sv₂ → variablesAt s sv₁ ≈ᵛ variablesAt s sv₂
variablesAt-≈ s sv₁ sv₂ sv₁≈sv₂ = variablesAt-≈ s sv₁ sv₂ sv₁≈sv₂ =
m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ sv₁ sv₂ sv₁≈sv₂ m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ sv₁ sv₂ sv₁≈sv₂
(states-in-Map s sv₁) (states-in-Map s sv₂) (states-in-Map s sv₁) (states-in-Map s sv₂)
-- build up the 'join' function, which follows from Exercise 4.26's -- build up the 'join' function, which follows from Exercise 4.26's
-- --
-- L₁ → (A → L₂) -- L₁ → (A → L₂)
-- --
-- Construction, with L₁ = (A → L₂), and f = id -- Construction, with L₁ = (A → L₂), and f = id
joinForKey : State → StateVariables → VariableValues joinForKey : State → StateVariables → VariableValues
joinForKey k states = foldr _⊔ᵛ_ ⊥ᵛ (states [ incoming k ]) joinForKey k states = foldr _⊔ᵛ_ ⊥ᵛ (states [ incoming k ])
-- The per-key join is made up of map key accesses (which are monotonic) -- The per-key join is made up of map key accesses (which are monotonic)
-- and folds using the join operation (also monotonic) -- and folds using the join operation (also monotonic)
joinForKey-Mono : ∀ (k : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (joinForKey k) joinForKey-Mono : ∀ (k : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (joinForKey k)
joinForKey-Mono k {fm₁} {fm₂} fm₁≼fm₂ = joinForKey-Mono k {fm₁} {fm₂} fm₁≼fm₂ =
foldr-Mono joinSemilatticeᵛ joinSemilatticeᵛ (fm₁ [ incoming k ]) (fm₂ [ incoming k ]) _⊔ᵛ_ ⊥ᵛ ⊥ᵛ foldr-Mono joinSemilatticeᵛ joinSemilatticeᵛ (fm₁ [ incoming k ]) (fm₂ [ incoming k ]) _⊔ᵛ_ ⊥ᵛ ⊥ᵛ
(m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ (incoming k) fm₁≼fm₂) (m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ (incoming k) fm₁≼fm₂)
(⊔ᵛ-idemp ⊥ᵛ) ⊔ᵛ-Monotonicʳ ⊔ᵛ-Monotonicˡ (⊔ᵛ-idemp ⊥ᵛ) ⊔ᵛ-Monotonicʳ ⊔ᵛ-Monotonicˡ
-- The name f' comes from the formulation of Exercise 4.26. -- 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 open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) joinForKey joinForKey-Mono states
@@ -158,11 +160,12 @@ module WithProg (prog : Program) where
; f'-k∈ks-≡ to joinAll-k∈ks-≡ ; f'-k∈ks-≡ to joinAll-k∈ks-≡
) )
variablesAt-joinAll : ∀ (s : State) (sv : StateVariables) → private
variablesAt s (joinAll sv) ≡ joinForKey s sv variablesAt-joinAll : ∀ (s : State) (sv : StateVariables) →
variablesAt-joinAll s sv variablesAt s (joinAll sv) ≡ joinForKey s sv
with (vs , s,vs∈usv) ← locateᵐ {s} {joinAll sv} (states-in-Map s (joinAll sv)) = variablesAt-joinAll s sv
joinAll-k∈ks-≡ {l = sv} (states-complete s) s,vs∈usv with (vs , s,vs∈usv) ← locateᵐ {s} {joinAll sv} (states-in-Map s (joinAll sv)) =
joinAll-k∈ks-≡ {l = sv} (states-complete s) s,vs∈usv
record Evaluator : Set where record Evaluator : Set where
field field
@@ -170,7 +173,7 @@ module WithProg (prog : Program) where
eval-Mono : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ˡ_ (eval e) eval-Mono : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ˡ_ (eval e)
-- With 'join' in hand, we need to perform abstract evaluation. -- With 'join' in hand, we need to perform abstract evaluation.
module _ {{evaluator : Evaluator}} where private module WithEvaluator {{evaluator : Evaluator}} where
open Evaluator evaluator open Evaluator evaluator
-- For a particular evaluation function, we need to perform an evaluation -- For a particular evaluation function, we need to perform an evaluation
@@ -253,7 +256,10 @@ module WithProg (prog : Program) where
with (vs , s,vs∈usv) ← locateᵐ {s} {updateAll sv} (states-in-Map s (updateAll sv)) = with (vs , s,vs∈usv) ← locateᵐ {s} {updateAll sv} (states-in-Map s (updateAll sv)) =
updateAll-k∈ks-≡ {l = sv} (states-complete s) s,vs∈usv updateAll-k∈ks-≡ {l = sv} (states-complete s) s,vs∈usv
module _ {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}} where open WithEvaluator
open WithEvaluator using (result; analyze; result≈analyze-result) public
private module WithInterpretation {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}} where
open LatticeInterpretation latticeInterpretationˡ open LatticeInterpretation latticeInterpretationˡ
using () using ()
renaming renaming
@@ -294,6 +300,8 @@ module WithProg (prog : Program) where
⟦⟧ᵛ-⊔ᵛ-∨ {vs₁ = vs'} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ ⟦⟧ᵛ-⊔ᵛ-∨ {vs₁ = vs'} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ
(inj₂ (⟦⟧ᵛ-foldr ⟦vs⟧ρ vs∈vss')) (inj₂ (⟦⟧ᵛ-foldr ⟦vs⟧ρ vs∈vss'))
open WithInterpretation
module _ {{evaluator : Evaluator}} {{interpretation : LatticeInterpretation isLatticeˡ}} where module _ {{evaluator : Evaluator}} {{interpretation : LatticeInterpretation isLatticeˡ}} where
open Evaluator evaluator open Evaluator evaluator
open LatticeInterpretation interpretation open LatticeInterpretation interpretation
@@ -312,7 +320,7 @@ module WithProg (prog : Program) where
field field
valid : IsValid valid : IsValid
module _ {{validInterpretation : ValidInterpretation}} where module WithValidInterpretation {{validInterpretation : ValidInterpretation}} where
open ValidInterpretation validInterpretation open ValidInterpretation validInterpretation
updateVariablesFromStmt-matches : ∀ {bs vs ρ₁ ρ₂} → ρ₁ , bs ⇒ᵇ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ updateVariablesFromStmt bs vs ⟧ᵛ ρ₂ updateVariablesFromStmt-matches : ∀ {bs vs ρ₁ ρ₂} → ρ₁ , bs ⇒ᵇ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ updateVariablesFromStmt bs vs ⟧ᵛ ρ₂
@@ -391,3 +399,5 @@ module WithProg (prog : Program) where
analyze-correct : ∀ {ρ : Env} → [] , rootStmt ⇒ˢ ρ → ⟦ variablesAt finalState result ⟧ᵛ ρ analyze-correct : ∀ {ρ : Env} → [] , rootStmt ⇒ˢ ρ → ⟦ variablesAt finalState result ⟧ᵛ ρ
analyze-correct {ρ} ∅,s⇒ρ = walkTrace {initialState} {finalState} {[]} {ρ} ⟦joinAll-initialState⟧ᵛ∅ (trace ∅,s⇒ρ) analyze-correct {ρ} ∅,s⇒ρ = walkTrace {initialState} {finalState} {[]} {ρ} ⟦joinAll-initialState⟧ᵛ∅ (trace ∅,s⇒ρ)
open WithValidInterpretation using (analyze-correct) public