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

Prove that 'updateAll' has preservation

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-05-08 22:29:36 -07:00
parent 4350919871
commit 5837fdf19b
1 changed files with 11 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
Analysis/Forward.agda
View File

@ -52,7 +52,6 @@ module WithProg (prog : Program) where
; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ
; ∈k-dec to ∈k-decᵛ ; ∈k-dec to ∈k-decᵛ
; all-equal-keys to all-equal-keysᵛ ; all-equal-keys to all-equal-keysᵛ
; forget to forgetᵛ
) )
public public
open IsLattice isLatticeᵛ open IsLattice isLatticeᵛ
@ -181,6 +180,7 @@ module WithProg (prog : Program) where
renaming renaming
( f' to updateAll ( f' to updateAll
; f'-Monotonic to updateAll-Mono ; f'-Monotonic to updateAll-Mono
; f'-k∈ks-≡ to updateAll-k∈ks-≡
) )
-- Finally, the whole analysis consists of getting the 'join' -- Finally, the whole analysis consists of getting the 'join'
@ -201,6 +201,12 @@ module WithProg (prog : Program) where
renaming (aᶠ to result) renaming (aᶠ to result)
public 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 module WithInterpretation (latticeInterpretationˡ : LatticeInterpretation isLatticeˡ) where
open LatticeInterpretation latticeInterpretationˡ open LatticeInterpretation latticeInterpretationˡ
using () using ()
@ -237,3 +243,7 @@ module WithProg (prog : Program) where
updateVariablesForState-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ updateVariablesForState s sv ⟧ᵛ ρ₂ updateVariablesForState-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ updateVariablesForState s sv ⟧ᵛ ρ₂
updateVariablesForState-matches = updateVariablesFromStmt-fold-matches 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⟧ρ₁