Browse Source

Start reworking the security model.

gas-move-test
Thomas Kerber 1 year ago
parent
commit
afb135392a
Signed by: Thomas Kerber <t.kerber@ed.ac.uk> GPG Key ID: 8489B911F9ED617B
3 changed files with 181 additions and 74 deletions
  1. +12
    -5
      Yggdrasil/Probability.agda
  2. +110
    -44
      Yggdrasil/Security.agda
  3. +59
    -25
      Yggdrasil/World.agda

+ 12
- 5
Yggdrasil/Probability.agda View File

@@ -13,10 +13,11 @@ open import Data.Nat.Properties using (≤-trans; ≤-refl)
open import Data.List.Properties using (length-filter; length-map)
open import Data.Product using (_×_; ∃; ∃-syntax; proj₁) renaming (_,_ to ⟨_,_⟩)
open import Data.Rational using (ℚ) renaming (_≤?_ to _ℚ≤?_; _≤_ to _ℚ≤_)
open import Function using (_∘_)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Nullary.Decidable using (True; fromWitness)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; trans; cong)
open import Level using (Level; Lift; lift) renaming (suc to lsuc)
open import Level using (Level; Lift; lower; _⊔_) renaming (suc to lsuc; lift to llift)
open import Yggdrasil.List using (_∈_; with-proof)
import Yggdrasil.Rational as ℚ

@@ -46,12 +47,18 @@ length-all-fin zero = refl
length-all-fin (suc n) = cong suc (trans (length-map suc (all-fin n)) (length-all-fin n))

count : ∀ {ℓ n} {P : PrFin {ℓ} n → Set ℓ} → ((f : PrFin {ℓ} n) → Dec (P f)) → ℕ
count {n = n} dec = length (filter dec (map lift (all-fin (suc (suc n)))))
count {n = n} dec = length (filter dec (map llift (all-fin (suc (suc n)))))

data Dist {ℓ : Level} : Set ℓ → Set (lsuc ℓ) where
pure : ∀ {A : Set ℓ} → A → Dist A
sample : ∀ {n : ℕ} → Dist (PrFin n)
bind : ∀ {A B : Set ℓ} → Dist A → (A → Dist B) → Dist B
sample : ∀ {n : ℕ} → Dist (PrFin {ℓ} n)
_>>=_ : ∀ {A B : Set ℓ} → Dist A → (A → Dist B) → Dist B

lift : {ℓ₁ ℓ₂ : Level} {A : Set ℓ₁} → Dist A → Dist (Lift ℓ₂ A)
lift (pure x) = pure (llift x)
lift {ℓ₁} {ℓ₂} (sample {n = n}) = sample {n = n} >>=
(pure ∘ llift ∘ llift ∘ lower)
lift {ℓ₂ = ℓ} (D >>= f) = lift {ℓ₂ = ℓ} D >>= (lift ∘ f ∘ lower)

≡⇒≤ : {a b : ℕ} → a ≡ b → a ℕ≤ b
≡⇒≤ refl = ≤-refl
@@ -70,7 +77,7 @@ data Pr[_[_]]≡_ {ℓ : Level} : {A : Set ℓ} → (P : A → Set ℓ) → Dist
Pr[ P₁ [ D ]]≡ p₁ →
((x : A) → P₁ x → Pr[ P₂ [ f x ]]≡ p₂) →
((x : A) → ¬ (P₁ x) → Pr[ P₂ [ f x ]]≡ p₃) →
Pr[ P₂ [ bind D f ]]≡ (case p₁ p₂ p₃)
Pr[ P₂ [ D >>= f ]]≡ (case p₁ p₂ p₃)

record _≈[_]≈_ {ℓ : Level} {A : Set ℓ} (d₁ : Dist A) (ε : ℚ) (d₂ : Dist A) : Set (lsuc ℓ) where
field

+ 110
- 44
Yggdrasil/Security.agda View File

@@ -5,63 +5,129 @@ open import Data.Product using (_×_; Σ; Σ-syntax; proj₁; proj₂; ∃; ∃-
open import Data.Nat using (ℕ)
open import Data.Maybe using (Maybe) renaming (map to mmap)
open import Data.Unit using (⊤; tt)
open import Function using (_∘_)
open import Level using (Level; Lift; lift) renaming (suc to lsuc)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Yggdrasil.List using (_∈_; here; there; with-proof; map≡-implies-∈≡)
open import Yggdrasil.World using (WorldType; WorldState; World; Call; Strategy; Node; Action↑; weaken; call; call↓; _↑_; stnode; _∷_; []; exec)
open import Yggdrasil.World using (WorldType; WorldState; World; Oracle; Call; Strategy; Node; Action; weaken; call; call↓; _↑_; stnode; _∷_; []; exec; _⊑_; Query; _∈↑_; abort; dist; _>>=_; call↯; query; path; _↑)
open import Yggdrasil.Probability using (Dist; _>>=_; pure)
open WorldType
open Node

data Guess {ℓ : Level} : Set ℓ where
real? ideal? : Guess

data Outcome : Set where
↯ ✔ : Outcome
data Action↯ {ℓ : Level} (Γᵢ Γᵣ : WorldType ℓ)
{hon-≡ : map weaken (hon Γᵢ) ≡ map weaken (hon Γᵣ)} : Set ℓ →
Set (lsuc ℓ) where
query : ∀ {Γ′ q} → q ∈ qry (node Γ′) → Γ′ ⊑ Γᵢ → (x : Query.A q) → Action↯ Γᵢ Γᵣ (Query.B q x)
abort : ∀ {A} → Action↯ Γᵢ Γᵣ A
dist : ∀ {A} → Dist A → Action↯ Γᵢ Γᵣ A
call↯ : ∀ {Γ′} {f : Call ℓ (node Γ′)} → f ∈ (adv Γ′) → Γ′ ⊑ Γᵣ → (x : Call.A f) →
Action↯ Γᵢ Γᵣ (Call.B f x)
_>>=_ : ∀ {A B} → Action↯ Γᵢ Γᵣ {hon-≡} A → (A → Action↯ Γᵢ Γᵣ {hon-≡} B) →
Action↯ Γᵢ Γᵣ B

record RouterConfig {ℓ : Level} : Set (lsuc ℓ) where
record Simulator {ℓ : Level} (Γᵢ Γᵣ : WorldType ℓ) : Set (lsuc ℓ) where
field
real : World ℓ
ideal : World ℓ
sim : Σ[ σ ∈ Set ℓ ] (σ × (∀ {c} → σ → c ∈ adv (proj₁ ideal) →
σ × (Σ (Call ℓ (node (proj₁ real))) (_∈ adv (proj₁ real)))))
hon-≡ : map weaken (hon (proj₁ ideal)) ≡ map weaken (hon (proj₁ real))
hon-≡ : map weaken (hon Γᵢ) ≡ map weaken (hon Γᵣ)
state : Set ℓ
initial : state
call↯-map : ∀ {Γ′} {f : Call ℓ (node Γ′)} → f ∈ (adv Γ′) → Γ′ ⊑ Γᵢ →
(x : Call.A f) → Action↯ Γᵢ Γᵣ {hon-≡} (Call.B f x)
query-map : ∀ {q} → q ∈↑ Γᵣ → (x : Query.A q) → Action↯ Γᵢ Γᵣ {hon-≡} (Query.B q x)

open RouterConfig
open Simulator

router-world-type : ∀ {ℓ} → RouterConfig {ℓ} → WorldType ℓ
router-world-type {ℓ} rc = record
{ node = router-node
; adv = []
; hon = map (λ{c → call (Call.A (proj₁ c)) (Call.B (proj₁ c)) (hon-map′ c)})
(with-proof (hon (proj₁ (ideal rc))))
}
where
router-node : Node ℓ
router-node = record
{ state = Σ (Guess {ℓ}) (λ{ ideal? → Lift ℓ ⊤ ; real? → proj₁ (sim rc)})
; chld = proj₁ (ideal rc) ∷ proj₁ (real rc) ∷ []
; qry = []
}
hon-map′ : (c : Σ (Call ℓ (node (proj₁ (ideal rc)))) (_∈ (hon (proj₁ (ideal rc))))) →
state router-node → (x : Call.A (proj₁ c)) →
(state router-node) × Action↑ router-node (Call.B (proj₁ c) x)
hon-map′ ⟨ call A B δ , ∈ideal ⟩ ⟨ ideal? , lift tt ⟩ x
= ⟨ ⟨ ideal? , lift tt ⟩ , call↓ ∈ideal x ↑ here ⟩
hon-map′ ⟨ call A B δ , ∈ideal ⟩ ⟨ real? , σ ⟩ x with map≡-implies-∈≡ (hon-≡ rc) ∈ideal
... | ⟨ _ , ⟨ ∈real , refl ⟩ ⟩ = ⟨ ⟨ real? , σ ⟩ , call↓ ∈real x ↑ there here ⟩
Actionᵢ⇒Actionᵣ : ∀ {ℓ : Level} {Γᵢ Γᵣ : WorldType ℓ} {A : Set ℓ} →
Simulator Γᵢ Γᵣ → Oracle Γᵢ → Action Γᵢ A → Action Γᵣ A
Action↯⇒Action : ∀ {ℓ : Level} {Γᵢ Γᵣ : WorldType ℓ} {A : Set ℓ} →
(S : Simulator Γᵢ Γᵣ) → Oracle Γᵢ → Action↯ Γᵢ Γᵣ {hon-≡ S} A → Action Γᵣ A

router-world-state : ∀ {ℓ} → (rc : RouterConfig {ℓ}) → Guess {ℓ} →
WorldState (router-world-type rc)
router-world-state rc real? = stnode ⟨ real? , proj₁ (proj₂ (sim rc)) ⟩
(proj₂ (ideal rc) ∷ proj₂ (real rc) ∷ [])
router-world-state rc ideal? = stnode ⟨ ideal? , lift tt ⟩
(proj₂ (ideal rc) ∷ proj₂ (real rc) ∷ [])
Actionᵢ⇒Actionᵣ S O ((call↓ ∈Γᵢ x) ↑) with map≡-implies-∈≡ (hon-≡ S) ∈Γᵢ
... | ⟨ _ , ⟨ ∈Γᵣ , refl ⟩ ⟩ = call↓ ∈Γᵣ x ↑
Actionᵢ⇒Actionᵣ _ _ abort = abort
Actionᵢ⇒Actionᵣ _ _ (dist D) = dist D
Actionᵢ⇒Actionᵣ S O (call↯ ∈Γ Γ⊑ x) = Action↯⇒Action S O (call↯-map S ∈Γ Γ⊑ x)
Actionᵢ⇒Actionᵣ S O (α >>= β) = (Actionᵢ⇒Actionᵣ S O α) >>=
(Actionᵢ⇒Actionᵣ S O ∘ β)

router-strategy : ∀ {ℓ A} → (rc : RouterConfig {ℓ}) →
Strategy (proj₁ (ideal rc)) A → Strategy (router-world-type rc) A
router-strategy = ?
-- FIXME: The termination checker (understandably) doesn't like this. Can we
-- delay the recursion to runtime?
Action↯⇒Action S O (query ∈Γ Γ⊑ x) = {!Actionᵢ⇒Actionᵣ S O (O (path Γ⊑ ∈Γ) x)!}
Action↯⇒Action _ _ abort = abort
Action↯⇒Action _ _ (dist D) = dist D
Action↯⇒Action _ _ (call↯ ∈Γ Γ⊑ x) = call↯ ∈Γ Γ⊑ x
Action↯⇒Action S O (α >>= β) = (Action↯⇒Action S O α) >>=
(Action↯⇒Action S O ∘ β)

yggdrasil-game : ∀ {ℓ} → (rc : RouterConfig {ℓ}) →
Strategy (proj₁ (ideal rc)) Guess → Guess {ℓ} → ℕ → Maybe (Guess {ℓ})
yggdrasil-game rc str world gas = mmap proj₁ (exec (router-strategy rc str)
(router-world-state rc world) gas)

record Challenge {ℓ : Level} : Set (lsuc ℓ) where
field
Γᵣ : WorldType ℓ
Γᵢ : WorldType ℓ
Σᵣ : WorldState Γᵣ
Σᵢ : WorldState Γᵢ
sim : Simulator Γᵢ Γᵣ
--sim : Σ[ σ ∈ Set ℓ ] (σ × (∀ {c} → σ → c ∈ adv (proj₁ ideal) →
-- σ × (Σ (Call ℓ (node (proj₁ real))) (_∈ adv (proj₁ real)))))
-- strategy :

--exec-ideal : {ℓ : Level} → (c : Challenge {ℓ}) → (s : Strategy (proj₁ (ideal c)))

--private
-- relevel : {ℓ₁ ℓ₂ : Level} → Guess {ℓ₁} → Guess {ℓ₂}
-- relevel real? = real?
-- relevel ideal? = ideal?
--
--data Outcome : Set where
-- ↯ ✔ : Outcome
--
--record RouterConfig {ℓ : Level} : Set (lsuc ℓ) where
-- field
-- real : World ℓ
-- ideal : World ℓ
-- sim : Σ[ σ ∈ Set ℓ ] (σ × (∀ {c} → σ → c ∈ adv (proj₁ ideal) →
-- σ × (Σ (Call ℓ (node (proj₁ real))) (_∈ adv (proj₁ real)))))
-- hon-≡ : map weaken (hon (proj₁ ideal)) ≡ map weaken (hon (proj₁ real))
--
--open RouterConfig
--
--router-world-type : ∀ {ℓ} → RouterConfig {ℓ} → WorldType ℓ
--router-world-type {ℓ} rc = record
-- { node = router-node
-- ; adv = []
-- ; hon = map (λ{c → call (Call.A (proj₁ c)) (Call.B (proj₁ c)) (hon-map′ c)})
-- (with-proof (hon (proj₁ (ideal rc))))
-- }
-- where
-- router-node : Node ℓ
-- router-node = record
-- { state = Σ (Guess {ℓ}) (λ{ ideal? → Lift ℓ ⊤ ; real? → proj₁ (sim rc)})
-- ; chld = proj₁ (ideal rc) ∷ proj₁ (real rc) ∷ []
-- ; qry = []
-- }
-- hon-map′ : (c : Σ (Call ℓ (node (proj₁ (ideal rc)))) (_∈ (hon (proj₁ (ideal rc))))) →
-- state router-node → (x : Call.A (proj₁ c)) →
-- (state router-node) × Action↑ router-node (Call.B (proj₁ c) x)
-- hon-map′ ⟨ call A B δ , ∈ideal ⟩ ⟨ ideal? , lift tt ⟩ x
-- = ⟨ ⟨ ideal? , lift tt ⟩ , call↓ ∈ideal x ↑ here ⟩
-- hon-map′ ⟨ call A B δ , ∈ideal ⟩ ⟨ real? , σ ⟩ x with map≡-implies-∈≡ (hon-≡ rc) ∈ideal
-- ... | ⟨ _ , ⟨ ∈real , refl ⟩ ⟩ = ⟨ ⟨ real? , σ ⟩ , call↓ ∈real x ↑ there here ⟩
--
--router-world-state : ∀ {ℓ} → (rc : RouterConfig {ℓ}) → Guess {ℓ} →
-- WorldState (router-world-type rc)
--router-world-state rc real? = stnode ⟨ real? , proj₁ (proj₂ (sim rc)) ⟩
-- (proj₂ (ideal rc) ∷ proj₂ (real rc) ∷ [])
--router-world-state rc ideal? = stnode ⟨ ideal? , lift tt ⟩
-- (proj₂ (ideal rc) ∷ proj₂ (real rc) ∷ [])

--router-strategy : ∀ {ℓ A} → (rc : RouterConfig {ℓ}) →
-- Strategy (proj₁ (ideal rc)) A → Strategy (router-world-type rc) A
--router-strategy = ?
--
--yggdrasil-game : ∀ {ℓ} → (rc : RouterConfig {ℓ}) →
-- Strategy (proj₁ (ideal rc)) Guess → Guess {ℓ} → ℕ → Dist (Maybe (Guess {lsuc ℓ}))
--yggdrasil-game rc str world gas =
-- (exec (router-strategy rc str) (router-world-state rc world) gas) >>=
-- (pure ∘ mmap (relevel ∘ proj₁))

+ 59
- 25
Yggdrasil/World.agda View File

@@ -8,7 +8,8 @@ open import Data.Nat using (ℕ; zero; suc)
open import Data.Product using (_×_; Σ; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
open import Level using (Level) renaming (suc to lsuc)
open import Level using (Level) renaming (suc to lsuc; lift to llift)
open import Yggdrasil.Probability using (Dist; pure; _>>=_; lift)
open import Yggdrasil.List using (_∈_; here; there)

record Query (ℓ : Level) : Set (lsuc ℓ) where
@@ -18,11 +19,10 @@ record Query (ℓ : Level) : Set (lsuc ℓ) where

record Node (ℓ : Level) : Set (lsuc ℓ)
record WorldType (ℓ : Level) : Set (lsuc ℓ)
data Action↯ {ℓ : Level} (Γ : WorldType ℓ) : Set ℓ → Set (lsuc ℓ)
--data Action↯ {ℓ : Level} (Γ : WorldType ℓ) : Set ℓ → Set (lsuc ℓ)
data Action↑ {ℓ : Level} (N : Node ℓ) : Set ℓ → Set (lsuc ℓ)
data Action↓ {ℓ : Level} (Γ : WorldType ℓ) : Set ℓ → Set (lsuc ℓ)
Action : {ℓ : Level} → WorldType ℓ → Set ℓ → Set (lsuc ℓ)
Action Γ A = Action↯ Γ A ⊎ Action↓ Γ A
data Action {ℓ : Level} (Γ : WorldType ℓ) : Set ℓ → Set (lsuc ℓ)

data WorldState {ℓ : Level} (Γ : WorldType ℓ) : Set (lsuc ℓ)
data WorldStates {ℓ : Level} : List (WorldType ℓ) → Set (lsuc ℓ)
@@ -67,16 +67,28 @@ data _⊑_ {ℓ : Level} : (Γ₁ Γ₂ : WorldType ℓ) → Set (lsuc ℓ) wher
⊑-right : ∀ {ℓ} {Γ₁ Γ₂ Γ₃ : WorldType ℓ} → Γ₂ ⊑ Γ₃ → Γ₁ ∈ chld (node Γ₂) → Γ₁ ⊑ Γ₃
⊑-right Γ⊑ ∈Γ = ⊑-trans (there ∈Γ here) Γ⊑

data Action↯ {ℓ} Γ where
data Action {ℓ} Γ where
_↑ : ∀ {A} → Action↓ {ℓ} Γ A → Action {ℓ} Γ A
abort : ∀ {A} → Action Γ A
dist : ∀ {A} → Dist A → Action Γ A
call↯ : ∀ {Γ′} {f : Call ℓ (node Γ′)} → f ∈ (adv Γ′) → Γ′ ⊑ Γ → (x : Call.A f) →
Action↯ Γ (Call.B f x)
Action Γ (Call.B f x)
_>>=_ : ∀ {A B} → Action Γ A → (A → Action Γ B) → Action Γ B

--A = Action↯ Γ A ⊎ Action↓ Γ A
--data Action↯ {ℓ} Γ where
-- abort : ∀ {A} → Action↯ Γ A
-- dist : ∀ {A} → Dist A → Action↯ Γ A
-- call↯ : ∀ {Γ′} {f : Call ℓ (node Γ′)} → f ∈ (adv Γ′) → Γ′ ⊑ Γ → (x : Call.A f) →
-- Action↯ Γ (Call.B f x)
-- _>>=_ : ∀ {A B} → Action↯ Γ A → (A → Action↯ Γ B) → Action↯ Γ B

data Action↓ {ℓ} Γ where
call↓ : ∀ {f} → f ∈ (hon Γ) → (x : Call.A f) → Action↓ Γ (Call.B f x)

data Action↑ {ℓ} N where
abort : ∀ {A} → Action↑ N A
pure : ∀ {A} → A → Action↑ N A
dist : ∀ {A} → Dist A → Action↑ N A
query : ∀ {q} → q ∈ qry N → (x : Query.A q) → Action↑ N (Query.B q x)
_↑_ : ∀ {Γ A} → Action↓ Γ A → Γ ∈ chld N → Action↑ N A
_>>=_ : ∀ {A B} → Action↑ N A → (A → Action↑ N B) → Action↑ N B
@@ -122,38 +134,59 @@ set (there Γ′∈ ⊑Γ) (stnode Σ Σs) Σ′ = stnode Σ (set′ Γ′∈
set′ (there Γ∈) ⊑Γ (Σ ∷ Σs) Σ′ = Σ ∷ set′ Γ∈ ⊑Γ Σs Σ′

exec : ∀ {ℓ Γ A} → Strategy {ℓ} Γ A → WorldState {ℓ} Γ → ℕ →
Maybe (A × WorldState {ℓ} Γ)
exec↯ : ∀ {ℓ Γ A} → Oracle Γ → Action↯ Γ A → WorldState {ℓ} Γ → ℕ →
Maybe (A × WorldState {ℓ} Γ)
Dist (Maybe (A × WorldState {ℓ} Γ))
exec′ : ∀ {ℓ Γ A} → Oracle Γ → Action Γ A → WorldState {ℓ} Γ → ℕ →
Dist (Maybe (A × WorldState {ℓ} Γ))
--exec↯ : ∀ {ℓ Γ A} → Oracle Γ → Action↯ Γ A → WorldState {ℓ} Γ → ℕ →
-- Dist (Maybe (A × WorldState {ℓ} Γ))
exec↓ : ∀ {ℓ Γ₁ Γ₂ A} → Oracle Γ₁ → Action↓ Γ₂ A → WorldState {ℓ} Γ₁ →
Γ₂ ⊑ Γ₁ → ℕ → Maybe (A × WorldState {ℓ} Γ₁)
Γ₂ ⊑ Γ₁ → ℕ → Dist (Maybe (A × WorldState {ℓ} Γ₁))
exec↑ : ∀ {ℓ Γ₁ Γ₂ N A} → Oracle Γ₁ → Action↑ N A → WorldState {ℓ} Γ₁ →
Γ₂ ⊑ Γ₁ → N ≡ node Γ₂ → ℕ → Maybe (A × WorldState {ℓ} Γ₁)
Γ₂ ⊑ Γ₁ → N ≡ node Γ₂ → ℕ → Dist (Maybe (A × WorldState {ℓ} Γ₁))

exec (strat (inj₁ α) O) Σ g = exec↯ O α Σ g
exec (strat (inj₂ α) O) Σ g = exec↓ O α Σ here g
-- NOTE: Gas is only used for termination here, it is NOT a computational model.
exec (strat α O) Σ g = exec′ O α Σ g

exec↯ _ _ _ zero = nothing
exec↯ O (call↯ {f = f} f∈ ⊑Γ x) Σ (suc g) = let
exec′ _ _ _ zero = pure nothing
exec′ O (α ↑) Σ g = exec↓ O α Σ here g
exec′ _ abort _ _ = pure nothing
exec′ O (dist D) Σ (suc g) = lift D >>= λ{ (llift x) → pure (just ⟨ x , Σ ⟩ ) }
exec′ O (call↯ {f = f} f∈ ⊑Γ x) Σ (suc g) = let
σ = get ⊑Γ Σ
⟨ σ′ , α ⟩ = Call.δ f σ x
Σ′ = set ⊑Γ Σ σ′
in exec↑ O α Σ′ ⊑Γ refl g

exec↓ _ _ _ _ zero = nothing
-- exec′ O (α ↯) Σ g = exec↯ O α Σ g
exec′ O (α >>= β) Σ (suc g) = (exec′ O α Σ (suc g)) >>= λ{
(just ⟨ x , Σ′ ⟩) → exec′ O (β x) Σ′ g;
nothing → pure nothing }

-- exec↯ _ _ _ zero = pure nothing
-- exec↯ _ abort _ _ = pure nothing
-- exec↯ O (dist D) Σ (suc g) = lift D >>= λ{ (llift x) → pure (just ⟨ x , Σ ⟩ ) }
-- exec↯ O (call↯ {f = f} f∈ ⊑Γ x) Σ (suc g) = let
-- σ = get ⊑Γ Σ
-- ⟨ σ′ , α ⟩ = Call.δ f σ x
-- Σ′ = set ⊑Γ Σ σ′
-- in exec↑ O α Σ′ ⊑Γ refl g
-- exec↯ O (α >>= β) Σ (suc g) = (exec↯ O α Σ (suc g)) >>= λ{
-- (just ⟨ x , Σ′ ⟩) → exec↯ O (β x) Σ′ g;
-- nothing → pure nothing }

exec↓ _ _ _ _ zero = pure nothing
exec↓ O (call↓ {f = f} f∈ x) Σ ⊑Γ (suc g) = let
σ = get ⊑Γ Σ
⟨ σ′ , α ⟩ = Call.δ f σ x
Σ′ = set ⊑Γ Σ σ′
in exec↑ O α Σ′ ⊑Γ refl g

exec↑ _ _ _ _ _ zero = nothing
exec↑ O abort Σ ⊑Γ N≡ (suc g) = nothing
exec↑ O (pure x) Σ ⊑Γ N≡ (suc g) = just ⟨ x , Σ ⟩
exec↑ _ _ _ _ _ zero = pure nothing
exec↑ O abort Σ ⊑Γ N≡ (suc g) = pure nothing
exec↑ O (dist D) Σ ⊑Γ N≡ (suc g) = lift D >>=
λ{ (llift x) → pure (just ⟨ x , Σ ⟩) }
exec↑ O (query {q = q} q∈ x) Σ ⊑Γ refl (suc g) =
exec (strat (O (path ⊑Γ q∈) x) O) Σ g
exec′ O (O (path ⊑Γ q∈) x) Σ g
exec↑ O (α ↑ Γ′∈) Σ ⊑Γ refl (suc g) = exec↓ O α Σ (⊑-right ⊑Γ Γ′∈) g
exec↑ O (α >>= β) Σ ⊑Γ N≡ (suc g) with exec↑ O α Σ ⊑Γ N≡ (suc g)
... | just ⟨ x , Σ′ ⟩ = exec↑ O (β x) Σ′ ⊑Γ N≡ g
... | nothing = nothing
exec↑ O (α >>= β) Σ ⊑Γ N≡ (suc g) = (exec↑ O α Σ ⊑Γ N≡ (suc g)) >>= λ{
(just ⟨ x , Σ′ ⟩) → exec↑ O (β x) Σ′ ⊑Γ N≡ g;
nothing → pure nothing }

Loading…
Cancel
Save