From 5837fdf19bd9b4337bdcb7b88ef54bf1434a6180 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Wed, 8 May 2024 22:29:36 -0700 Subject: [PATCH] Prove that 'updateAll' has preservation Signed-off-by: Danila Fedorin --- Analysis/Forward.agda | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda index 270a4d8..be5e944 100644 --- a/Analysis/Forward.agda +++ b/Analysis/Forward.agda @@ -52,7 +52,6 @@ module WithProg (prog : Program) where ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ ; ∈k-dec to ∈k-decᵛ ; all-equal-keys to all-equal-keysᵛ - ; forget to forgetᵛ ) public open IsLattice isLatticeᵛ @@ -181,6 +180,7 @@ module WithProg (prog : Program) where renaming ( f' to updateAll ; f'-Monotonic to updateAll-Mono + ; f'-k∈ks-≡ to updateAll-k∈ks-≡ ) -- Finally, the whole analysis consists of getting the 'join' @@ -201,6 +201,12 @@ module WithProg (prog : Program) where renaming (aᶠ to result) public + variablesAt-updateAll : ∀ (s : State) (sv : StateVariables) → + variablesAt s (updateAll sv) ≡ updateVariablesForState s sv + variablesAt-updateAll s 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 + module WithInterpretation (latticeInterpretationˡ : LatticeInterpretation isLatticeˡ) where open LatticeInterpretation latticeInterpretationˡ using () @@ -237,3 +243,7 @@ module WithProg (prog : Program) where updateVariablesForState-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ updateVariablesForState s sv ⟧ᵛ ρ₂ updateVariablesForState-matches = updateVariablesFromStmt-fold-matches + + updateAll-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ variablesAt s (updateAll sv) ⟧ᵛ ρ₂ + updateAll-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁ rewrite variablesAt-updateAll s sv = + updateVariablesForState-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁