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

Prove the recursive step of trace walking

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-05-09 17:56:47 -07:00
parent a22c0c9252
commit 80069e76e6
1 changed files with 17 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
Analysis/Forward.agda
View File

@ -10,7 +10,7 @@ module Analysis.Forward
open import Data.Empty using (⊥-elim) open import Data.Empty using (⊥-elim)
open import Data.String using (String) renaming (_≟_ to _≟ˢ_) open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
open import Data.Nat using (suc) open import Data.Nat using (suc)
open import Data.Product using (_×_; proj₁; _,_) open import Data.Product using (_×_; proj₁; proj₂; _,_)
open import Data.List using (List; _∷_; []; foldr; foldl; cartesianProduct; cartesianProductWith) open import Data.List using (List; _∷_; []; foldr; foldl; cartesianProduct; cartesianProductWith)
open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_) open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
open import Data.List.Relation.Unary.Any as Any using () open import Data.List.Relation.Unary.Any as Any using ()
@ -76,11 +76,12 @@ module WithProg (prog : Program) where
-- 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
open StateVariablesFiniteMap open StateVariablesFiniteMap
using (_[_]; m₁≼m₂⇒m₁[ks]≼m₂[ks]) using (_[_]; []-∈; m₁≼m₂⇒m₁[ks]≼m₂[ks])
renaming renaming
( FiniteMap to StateVariables ( FiniteMap to StateVariables
; isLattice to isLatticeᵐ ; isLattice to isLatticeᵐ
; _≈_ to _≈ᵐ_ ; _≈_ to _≈ᵐ_
; _∈_ to _∈ᵐ_
; _∈k_ to _∈kᵐ_ ; _∈k_ to _∈kᵐ_
; locate to locateᵐ ; locate to locateᵐ
; _≼_ to _≼ᵐ_ ; _≼_ to _≼ᵐ_
@ -113,6 +114,9 @@ module WithProg (prog : Program) where
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 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-≈ = {!!} variablesAt-≈ = {!!}
@ -312,3 +316,14 @@ module WithProg (prog : Program) where
walkTrace : ∀ {s₁ s₂ ρ₁ ρ₂} → ⟦ joinForKey s₁ result ⟧ᵛ ρ₁ → Trace {graph} s₁ s₂ ρ₁ ρ₂ → ⟦ variablesAt s₂ result ⟧ᵛ ρ₂ walkTrace : ∀ {s₁ s₂ ρ₁ ρ₂} → ⟦ joinForKey s₁ result ⟧ᵛ ρ₁ → Trace {graph} s₁ s₂ ρ₁ ρ₂ → ⟦ variablesAt s₂ result ⟧ᵛ ρ₂
walkTrace {s₁} {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-single ρ₁,bss⇒ρ₂) = walkTrace {s₁} {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-single ρ₁,bss⇒ρ₂) =
stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂ stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂
walkTrace {s₁} {s₂} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-edge {ρ₂ = ρ} {idx₂ = s} ρ₁,bss⇒ρ s₁→s₂ tr) =
let
⟦result-s₁⟧ρ =
stepTrace {s₁} {ρ₁} {ρ} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ
s₁∈incomingStates =
[]-∈ result (edge⇒incoming s₁→s₂)
(variablesAt-∈ s₁ result)
⟦joinForKey-s⟧ρ =
⟦⟧ᵛ-foldr ⟦result-s₁⟧ρ s₁∈incomingStates
in
walkTrace ⟦joinForKey-s⟧ρ tr