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

Formulate correctness of buildCfg using end-to-end traces

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-04-27 14:56:19 -07:00
parent f555947184
commit ab40a27e78
2 changed files with 22 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
Language/Properties.agda
View File

@ -8,7 +8,7 @@ open import Language.Traces
open import Data.Fin as Fin using (zero) open import Data.Fin as Fin using (zero)
open import Data.List using (_∷_; []) open import Data.List using (_∷_; [])
open import Data.List.Membership.Propositional.Properties as ListMemProp using () open import Data.List.Membership.Propositional.Properties as ListMemProp using ()
open import Data.Product using (Σ; _,_) open import Data.Product using (Σ; _,_; _×_)
open import Data.Vec.Properties using (lookup-++ˡ; ++-identityʳ; lookup-++ʳ) open import Data.Vec.Properties using (lookup-++ˡ; ++-identityʳ; lookup-++ʳ)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym)
@ -81,3 +81,7 @@ Trace-loop : ∀ (g₁ : Graph) {idx₁ idx₂ : Graph.Index g₁} {ρ₁ ρ₂
Trace-loop g₁ {idx₁} {idx₁} (Trace-single ρ₁⇒ρ₂) = Trace-single ρ₁⇒ρ₂ Trace-loop g₁ {idx₁} {idx₁} (Trace-single ρ₁⇒ρ₂) = Trace-single ρ₁⇒ρ₂
Trace-loop g₁ {idx₁} (Trace-edge ρ₁⇒ρ idx₁→idx tr') = Trace-loop g₁ {idx₁} (Trace-edge ρ₁⇒ρ idx₁→idx tr') =
Trace-edge ρ₁⇒ρ (ListMemProp.∈-++⁺ˡ idx₁→idx) (Trace-loop g₁ tr') Trace-edge ρ₁⇒ρ (ListMemProp.∈-++⁺ˡ idx₁→idx) (Trace-loop g₁ tr')
buildCfg-sufficient : ∀ {s : Stmt} {ρ₁ ρ₂ : Env} → ρ₁ , s ⇒ˢ ρ₂ →
EndToEndTrace {buildCfg s} ρ₁ ρ₂
buildCfg-sufficient = {!!}

24
Language/Traces.agda
View File

@ -1,24 +1,34 @@
module Language.Traces where module Language.Traces where
open import Language.Base public open import Language.Base
open import Language.Semantics public open import Language.Semantics using (Env; _,_⇒ᵇˢ_)
open import Language.Graphs public open import Language.Graphs
open import Data.Product using (_,_) open import Data.Product using (_,_)
open import Data.List.Membership.Propositional as MemProp using () open import Data.List.Membership.Propositional using (_∈_)
module _ {g : Graph} where module _ {g : Graph} where
open Graph g using (Index; edges) open Graph g using (Index; edges; inputs; outputs)
data Trace : Index → Index → Env → Env → Set where data Trace : Index → Index → Env → Env → Set where
Trace-single : ∀ {ρ₁ ρ₂ : Env} {idx : Index} → Trace-single : ∀ {ρ₁ ρ₂ : Env} {idx : Index} →
ρ₁ , (g [ idx ]) ⇒ᵇˢ ρ₂ → Trace idx idx ρ₁ ρ₂ ρ₁ , (g [ idx ]) ⇒ᵇˢ ρ₂ → Trace idx idx ρ₁ ρ₂
Trace-edge : ∀ {ρ₁ ρ₂ ρ₃ : Env} {idx₁ idx₂ idx₃ : Index} → Trace-edge : ∀ {ρ₁ ρ₂ ρ₃ : Env} {idx₁ idx₂ idx₃ : Index} →
ρ₁ , (g [ idx₁ ]) ⇒ᵇˢ ρ₂ → (idx₁ , idx₂) MemProp.∈ edges → ρ₁ , (g [ idx₁ ]) ⇒ᵇˢ ρ₂ → (idx₁ , idx₂) ∈ edges →
Trace idx₂ idx₃ ρ₂ ρ₃ → Trace idx₁ idx₃ ρ₁ ρ₃ Trace idx₂ idx₃ ρ₂ ρ₃ → Trace idx₁ idx₃ ρ₁ ρ₃
_++⟨_⟩_ : ∀ {idx₁ idx₂ idx₃ idx₄ : Index} {ρ₁ ρ₂ ρ₃ : Env} → _++⟨_⟩_ : ∀ {idx₁ idx₂ idx₃ idx₄ : Index} {ρ₁ ρ₂ ρ₃ : Env} →
Trace idx₁ idx₂ ρ₁ ρ₂ → (idx₂ , idx₃) MemProp.∈ edges → Trace idx₁ idx₂ ρ₁ ρ₂ → (idx₂ , idx₃) ∈ edges →
Trace idx₃ idx₄ ρ₂ ρ₃ → Trace idx₁ idx₄ ρ₁ ρ₃ Trace idx₃ idx₄ ρ₂ ρ₃ → Trace idx₁ idx₄ ρ₁ ρ₃
_++⟨_⟩_ (Trace-single ρ₁⇒ρ₂) idx₂→idx₃ tr = Trace-edge ρ₁⇒ρ₂ idx₂→idx₃ tr _++⟨_⟩_ (Trace-single ρ₁⇒ρ₂) idx₂→idx₃ tr = Trace-edge ρ₁⇒ρ₂ idx₂→idx₃ tr
_++⟨_⟩_ (Trace-edge ρ₁⇒ρ₂ idx₁→idx' tr') idx₂→idx₃ tr = Trace-edge ρ₁⇒ρ₂ idx₁→idx' (tr' ++⟨ idx₂→idx₃ ⟩ tr) _++⟨_⟩_ (Trace-edge ρ₁⇒ρ₂ idx₁→idx' tr') idx₂→idx₃ tr = Trace-edge ρ₁⇒ρ₂ idx₁→idx' (tr' ++⟨ idx₂→idx₃ ⟩ tr)
record EndToEndTrace (ρ₁ ρ₂ : Env) : Set where
field
idx₁ : Index
idx₁∈inputs : idx₁ ∈ inputs
idx₂ : Index
idx₂∈outputs : idx₂ ∈ outputs
trace : Trace idx₁ idx₂ ρ₁ ρ₂