A framework for executable UC specifications.
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

197 lines
8.5KB

  1. module Yggdrasil.World where
  2. open import Data.Bool using (Bool)
  3. open import Data.Empty using (⊥-elim)
  4. open import Data.List using (List; _∷_; []; map)
  5. open import Data.Maybe using (Maybe; nothing; just) renaming (map to mmap)
  6. open import Data.Nat using (ℕ; zero; suc)
  7. open import Data.Product using (_×_; Σ; ∃; ∃-syntax; proj₁) renaming (_,_ to ⟨_,_⟩)
  8. open import Data.Sum using (_⊎_; inj₁; inj₂)
  9. open import Function using (_∘_)
  10. open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
  11. open import Level using (Level; Lift) renaming (suc to lsuc; lift to llift)
  12. open import Yggdrasil.Probability using (Dist; pure; _>>=_; lift)
  13. open import Yggdrasil.List using (_∈_; here; there)
  14. record Query (ℓ : Level) : Set (lsuc ℓ) where
  15. field
  16. A : Set ℓ
  17. B : A → Set ℓ
  18. record Node (ℓ : Level) : Set (lsuc ℓ)
  19. record WorldType (ℓ : Level) : Set (lsuc ℓ)
  20. --data Action↯ {ℓ : Level} (Γ : WorldType ℓ) : Set ℓ → Set (lsuc ℓ)
  21. data Action↑ {ℓ : Level} (N : Node ℓ) : Set ℓ → Set (lsuc ℓ)
  22. data Action↓ {ℓ : Level} (Γ : WorldType ℓ) : Set ℓ → Set (lsuc ℓ)
  23. data Action {ℓ : Level} (Γ : WorldType ℓ) : Set ℓ → Set (lsuc ℓ)
  24. data WorldState {ℓ : Level} (Γ : WorldType ℓ) : Set (lsuc ℓ)
  25. data WorldStates {ℓ : Level} : List (WorldType ℓ) → Set (lsuc ℓ)
  26. record Node ℓ where
  27. inductive
  28. field
  29. state : Set ℓ
  30. chld : List (WorldType ℓ)
  31. qry : List (Query ℓ)
  32. open Node
  33. record Call (ℓ : Level) (N : Node ℓ) : Set (lsuc ℓ) where
  34. inductive
  35. constructor call
  36. field
  37. A : Set ℓ
  38. B : A → Set ℓ
  39. δ : (state N) → (x : A) → (state N) × Action↑ N (B x)
  40. weaken : ∀ {ℓ N} → Call ℓ N → Query ℓ
  41. weaken c = record { A = Call.A c; B = Call.B c }
  42. record WorldType ℓ where
  43. inductive
  44. field
  45. node : Node ℓ
  46. adv : List (Call ℓ node)
  47. hon : List (Call ℓ node)
  48. open WorldType
  49. data _⊑_ {ℓ : Level} : (Γ₁ Γ₂ : WorldType ℓ) → Set (lsuc ℓ) where
  50. here : ∀ {Γ} → Γ ⊑ Γ
  51. there : ∀ {Γ₁ Γ₂ Γ₃} → Γ₂ ∈ chld (node Γ₃) → Γ₁ ⊑ Γ₂ → Γ₁ ⊑ Γ₃
  52. ⊑-trans : ∀ {ℓ} {Γ₁ Γ₂ Γ₃ : WorldType ℓ} → Γ₁ ⊑ Γ₂ → Γ₂ ⊑ Γ₃ → Γ₁ ⊑ Γ₃
  53. ⊑-trans ⊑Γ here = ⊑Γ
  54. ⊑-trans ⊑Γ (there Γ′∈ ⊑Γ′) = there Γ′∈ (⊑-trans ⊑Γ ⊑Γ′)
  55. ⊑-right : ∀ {ℓ} {Γ₁ Γ₂ Γ₃ : WorldType ℓ} → Γ₂ ⊑ Γ₃ → Γ₁ ∈ chld (node Γ₂) → Γ₁ ⊑ Γ₃
  56. ⊑-right Γ⊑ ∈Γ = ⊑-trans (there ∈Γ here) Γ⊑
  57. data Action {ℓ} Γ where
  58. _↑ : ∀ {A} → Action↓ {ℓ} Γ A → Action {ℓ} Γ A
  59. abort : ∀ {A} → Action Γ A
  60. dist : ∀ {A} → Dist A → Action Γ A
  61. call↯ : ∀ {Γ′} {f : Call ℓ (node Γ′)} → f ∈ (adv Γ′) → Γ′ ⊑ Γ → (x : Call.A f) →
  62. Action Γ (Call.B f x)
  63. _>>=_ : ∀ {A B} → Action Γ A → (A → Action Γ B) → Action Γ B
  64. --A = Action↯ Γ A ⊎ Action↓ Γ A
  65. --data Action↯ {ℓ} Γ where
  66. -- abort : ∀ {A} → Action↯ Γ A
  67. -- dist : ∀ {A} → Dist A → Action↯ Γ A
  68. -- call↯ : ∀ {Γ′} {f : Call ℓ (node Γ′)} → f ∈ (adv Γ′) → Γ′ ⊑ Γ → (x : Call.A f) →
  69. -- Action↯ Γ (Call.B f x)
  70. -- _>>=_ : ∀ {A B} → Action↯ Γ A → (A → Action↯ Γ B) → Action↯ Γ B
  71. data Action↓ {ℓ} Γ where
  72. call↓ : ∀ {f} → f ∈ (hon Γ) → (x : Call.A f) → Action↓ Γ (Call.B f x)
  73. data Action↑ {ℓ} N where
  74. abort : ∀ {A} → Action↑ N A
  75. dist : ∀ {A} → Dist A → Action↑ N A
  76. query : ∀ {q} → q ∈ qry N → (x : Query.A q) → Action↑ N (Query.B q x)
  77. _↑_ : ∀ {Γ A} → Action↓ Γ A → Γ ∈ chld N → Action↑ N A
  78. _>>=_ : ∀ {A B} → Action↑ N A → (A → Action↑ N B) → Action↑ N B
  79. data WorldStates {ℓ} where
  80. [] : WorldStates []
  81. _∷_ : ∀ {Γ Γs} → WorldState Γ → WorldStates Γs → WorldStates (Γ ∷ Γs)
  82. data WorldState {ℓ} Γ where
  83. stnode : state (node Γ) → WorldStates (chld (node Γ)) → WorldState Γ
  84. World : (ℓ : Level) → Set (lsuc ℓ)
  85. World ℓ = Σ (WorldType ℓ) WorldState
  86. data _∈↑_ {ℓ : Level} (q : Query ℓ) (Γ : WorldType ℓ) : Set (lsuc ℓ) where
  87. path : ∀ {Γ′} → Γ′ ⊑ Γ → q ∈ qry (node Γ′) → q ∈↑ Γ
  88. Oracle : ∀ {ℓ} → WorldType ℓ → Set (lsuc ℓ)
  89. Oracle Γ = ∀ {q} → q ∈↑ Γ → (x : Query.A q) → Action Γ (Query.B q x)
  90. record Strategy {ℓ : Level} (Γ : WorldType ℓ) (A : Set ℓ) : Set (lsuc ℓ) where
  91. constructor strat
  92. field
  93. init : Action Γ A
  94. oracle : Oracle Γ
  95. get : ∀ {ℓ Γ₁ Γ₂} → Γ₁ ⊑ Γ₂ → WorldState {ℓ} Γ₂ → state (node Γ₁)
  96. get here (stnode Σ _) = Σ
  97. get (there Γ′∈ ⊑Γ) (stnode _ Σs) = get ⊑Γ (lookup Γ′∈ Σs)
  98. where
  99. lookup : ∀ {Γ Γs} → Γ ∈ Γs → WorldStates Γs → WorldState Γ
  100. lookup here (Σ ∷ _) = Σ
  101. lookup (there Γ′∈) (_ ∷ Σs) = lookup Γ′∈ Σs
  102. set : ∀ {ℓ Γ₁ Γ₂} → Γ₁ ⊑ Γ₂ → WorldState {ℓ} Γ₂ → state (node Γ₁) →
  103. WorldState {ℓ} Γ₂
  104. set here (stnode Σ Σs) Σ′ = stnode Σ′ Σs
  105. set (there Γ′∈ ⊑Γ) (stnode Σ Σs) Σ′ = stnode Σ (set′ Γ′∈ ⊑Γ Σs Σ′)
  106. where
  107. set′ : ∀ {Γ₁ Γ₂ Γs} → Γ₂ ∈ Γs → Γ₁ ⊑ Γ₂ → WorldStates Γs →
  108. state (node Γ₁) → WorldStates Γs
  109. set′ here ⊑Γ (Σ ∷ Σs) Σ′ = set ⊑Γ Σ Σ′ ∷ Σs
  110. set′ (there Γ∈) ⊑Γ (Σ ∷ Σs) Σ′ = Σ ∷ set′ Γ∈ ⊑Γ Σs Σ′
  111. ⌊exec⌋ : ∀ {ℓ Γ A} → Strategy {ℓ} Γ A → WorldState {ℓ} Γ → ℕ →
  112. Dist (Maybe (Lift (lsuc ℓ) A))
  113. exec : ∀ {ℓ Γ A} → Strategy {ℓ} Γ A → WorldState {ℓ} Γ → ℕ →
  114. Dist (Maybe (A × WorldState {ℓ} Γ))
  115. exec′ : ∀ {ℓ Γ A} → Oracle Γ → Action Γ A → WorldState {ℓ} Γ → ℕ →
  116. Dist (Maybe (A × WorldState {ℓ} Γ))
  117. --exec↯ : ∀ {ℓ Γ A} → Oracle Γ → Action↯ Γ A → WorldState {ℓ} Γ → ℕ →
  118. -- Dist (Maybe (A × WorldState {ℓ} Γ))
  119. exec↓ : ∀ {ℓ Γ₁ Γ₂ A} → Oracle Γ₁ → Action↓ Γ₂ A → WorldState {ℓ} Γ₁ →
  120. Γ₂ ⊑ Γ₁ → ℕ → Dist (Maybe (A × WorldState {ℓ} Γ₁))
  121. exec↑ : ∀ {ℓ Γ₁ Γ₂ N A} → Oracle Γ₁ → Action↑ N A → WorldState {ℓ} Γ₁ →
  122. Γ₂ ⊑ Γ₁ → N ≡ node Γ₂ → ℕ → Dist (Maybe (A × WorldState {ℓ} Γ₁))
  123. -- NOTE: Gas is only used for termination here, it is NOT a computational model.
  124. ⌊exec⌋ str Σ g = (exec str Σ g) >>= (pure ∘ mmap (llift ∘ proj₁))
  125. exec (strat α O) Σ g = exec′ O α Σ g
  126. exec′ _ _ _ zero = pure nothing
  127. exec′ O (α ↑) Σ g = exec↓ O α Σ here g
  128. exec′ _ abort _ _ = pure nothing
  129. exec′ O (dist D) Σ (suc g) = lift D >>= λ{ (llift x) → pure (just ⟨ x , Σ ⟩ ) }
  130. exec′ O (call↯ {f = f} f∈ ⊑Γ x) Σ (suc g) = let
  131. σ = get ⊑Γ Σ
  132. ⟨ σ′ , α ⟩ = Call.δ f σ x
  133. Σ′ = set ⊑Γ Σ σ′
  134. in exec↑ O α Σ′ ⊑Γ refl g
  135. -- exec′ O (α ↯) Σ g = exec↯ O α Σ g
  136. exec′ O (α >>= β) Σ (suc g) = (exec′ O α Σ (suc g)) >>= λ{
  137. (just ⟨ x , Σ′ ⟩) → exec′ O (β x) Σ′ g;
  138. nothing → pure nothing }
  139. -- exec↯ _ _ _ zero = pure nothing
  140. -- exec↯ _ abort _ _ = pure nothing
  141. -- exec↯ O (dist D) Σ (suc g) = lift D >>= λ{ (llift x) → pure (just ⟨ x , Σ ⟩ ) }
  142. -- exec↯ O (call↯ {f = f} f∈ ⊑Γ x) Σ (suc g) = let
  143. -- σ = get ⊑Γ Σ
  144. -- ⟨ σ′ , α ⟩ = Call.δ f σ x
  145. -- Σ′ = set ⊑Γ Σ σ′
  146. -- in exec↑ O α Σ′ ⊑Γ refl g
  147. -- exec↯ O (α >>= β) Σ (suc g) = (exec↯ O α Σ (suc g)) >>= λ{
  148. -- (just ⟨ x , Σ′ ⟩) → exec↯ O (β x) Σ′ g;
  149. -- nothing → pure nothing }
  150. exec↓ _ _ _ _ zero = pure nothing
  151. exec↓ O (call↓ {f = f} f∈ x) Σ ⊑Γ (suc g) = let
  152. σ = get ⊑Γ Σ
  153. ⟨ σ′ , α ⟩ = Call.δ f σ x
  154. Σ′ = set ⊑Γ Σ σ′
  155. in exec↑ O α Σ′ ⊑Γ refl g
  156. exec↑ _ _ _ _ _ zero = pure nothing
  157. exec↑ O abort Σ ⊑Γ N≡ (suc g) = pure nothing
  158. exec↑ O (dist D) Σ ⊑Γ N≡ (suc g) = lift D >>=
  159. λ{ (llift x) → pure (just ⟨ x , Σ ⟩) }
  160. exec↑ O (query {q = q} q∈ x) Σ ⊑Γ refl (suc g) =
  161. exec′ O (O (path ⊑Γ q∈) x) Σ g
  162. exec↑ O (α ↑ Γ′∈) Σ ⊑Γ refl (suc g) = exec↓ O α Σ (⊑-right ⊑Γ Γ′∈) g
  163. exec↑ O (α >>= β) Σ ⊑Γ N≡ (suc g) = (exec↑ O α Σ ⊑Γ N≡ (suc g)) >>= λ{
  164. (just ⟨ x , Σ′ ⟩) → exec↑ O (β x) Σ′ ⊑Γ N≡ g;
  165. nothing → pure nothing }