From b28994e1d23b451b868a6d32062cd8bc10657fe6 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Tue, 31 Dec 2024 00:29:39 -0800 Subject: [PATCH] Tighten exported definitions in Forward.agda Signed-off-by: Danila Fedorin --- Analysis/Forward.agda | 94 ++++++++++++++++++++++++------------------- 1 file changed, 52 insertions(+), 42 deletions(-) diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda index a77f30c..3e4627c 100644 --- a/Analysis/Forward.agda +++ b/Analysis/Forward.agda @@ -78,10 +78,11 @@ module WithProg (prog : Program) where ; ⊥-contains-bottoms to ⊥ᵛ-contains-bottoms ) - ≈ᵛ-dec = ≈ˡ-dec⇒≈ᵛ-dec ≈ˡ-dec - joinSemilatticeᵛ = IsFiniteHeightLattice.joinSemilattice isFiniteHeightLatticeᵛ - fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ - ⊥ᵛ = Chain.Height.⊥ fixedHeightᵛ + private + ≈ᵛ-dec = ≈ˡ-dec⇒≈ᵛ-dec ≈ˡ-dec + joinSemilatticeᵛ = IsFiniteHeightLattice.joinSemilattice isFiniteHeightLatticeᵛ + fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ + ⊥ᵛ = Chain.Height.⊥ fixedHeightᵛ -- Finally, the map we care about is (state -> (variables -> value)). Bring that in. module StateVariablesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟_ isLatticeᵛ states @@ -109,45 +110,46 @@ module WithProg (prog : Program) where ( ≈-sym to ≈ᵐ-sym ) - ≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec - fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ + private + ≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec + fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ - -- We now have our (state -> (variables -> value)) map. - -- 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 - -- retrieve the variable values at each state. + -- We now have our (state -> (variables -> value)) map. + -- 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 + -- retrieve the variable values at each state. - 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 : State) (sv : StateVariables) → s ∈kᵐ sv + states-in-Map s sv@(m , ksv≡states) rewrite ksv≡states = states-complete s - variablesAt : State → StateVariables → VariableValues - variablesAt s sv = proj₁ (locateᵐ {s} {sv} (states-in-Map s sv)) + variablesAt : State → StateVariables → VariableValues + variablesAt s sv = proj₁ (locateᵐ {s} {sv} (states-in-Map s 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 : State) (sv : StateVariables) → (s , variablesAt s sv) ∈ᵐ 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₂ = - m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ sv₁ sv₂ sv₁≈sv₂ - (states-in-Map 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₂ = + m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ sv₁ sv₂ sv₁≈sv₂ + (states-in-Map s sv₁) (states-in-Map s sv₂) - -- build up the 'join' function, which follows from Exercise 4.26's - -- - -- L₁ → (A → L₂) - -- - -- Construction, with L₁ = (A → L₂), and f = id + -- 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 → VariableValues - joinForKey k states = foldr _⊔ᵛ_ ⊥ᵛ (states [ incoming k ]) + joinForKey : State → StateVariables → VariableValues + 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) + -- 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ˡ + 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 @@ -158,11 +160,12 @@ module WithProg (prog : Program) where ; f'-k∈ks-≡ to joinAll-k∈ks-≡ ) - variablesAt-joinAll : ∀ (s : State) (sv : StateVariables) → - variablesAt s (joinAll sv) ≡ joinForKey s sv - variablesAt-joinAll s sv - 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 + private + variablesAt-joinAll : ∀ (s : State) (sv : StateVariables) → + variablesAt s (joinAll sv) ≡ joinForKey s sv + variablesAt-joinAll s sv + 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 field @@ -170,7 +173,7 @@ module WithProg (prog : Program) where eval-Mono : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ˡ_ (eval e) -- With 'join' in hand, we need to perform abstract evaluation. - module _ {{evaluator : Evaluator}} where + private module WithEvaluator {{evaluator : Evaluator}} where open Evaluator evaluator -- 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)) = 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ˡ using () renaming @@ -294,6 +300,8 @@ module WithProg (prog : Program) where ⟦⟧ᵛ-⊔ᵛ-∨ {vs₁ = vs'} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ (inj₂ (⟦⟧ᵛ-foldr ⟦vs⟧ρ vs∈vss')) + open WithInterpretation + module _ {{evaluator : Evaluator}} {{interpretation : LatticeInterpretation isLatticeˡ}} where open Evaluator evaluator open LatticeInterpretation interpretation @@ -312,7 +320,7 @@ module WithProg (prog : Program) where field valid : IsValid - module _ {{validInterpretation : ValidInterpretation}} where + module WithValidInterpretation {{validInterpretation : ValidInterpretation}} where open ValidInterpretation validInterpretation 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 {ρ} ∅,s⇒ρ = walkTrace {initialState} {finalState} {[]} {ρ} ⟦joinAll-initialState⟧ᵛ∅ (trace ∅,s⇒ρ) + + open WithValidInterpretation using (analyze-correct) public