Browse Source

Fix various parts of the model.

tabularasa
Thomas Kerber 9 months ago
parent
commit
2f8864279a
Signed by: Thomas Kerber <t.kerber@ed.ac.uk> GPG Key ID: 8489B911F9ED617B
4 changed files with 169 additions and 139 deletions
  1. 32
    15
      Yggdrasil/Examples/SecureChannel.agda
  2. 6
    0
      Yggdrasil/Probability.agda
  3. 78
    78
      Yggdrasil/Security.agda
  4. 53
    46
      Yggdrasil/World.agda

+ 32
- 15
Yggdrasil/Examples/SecureChannel.agda View File

@@ -1,7 +1,7 @@
module Yggdrasil.Examples.SecureChannel where

open import Data.Bool using (Bool; true; false; if_then_else_)
open import Data.List using (List; []; _∷_)
open import Data.Bool using (Bool; true; false; if_then_else_; _∧_)
open import Data.List using (List; []; _∷_; any)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Nat using (_*_)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
@@ -13,7 +13,6 @@ open import Yggdrasil.Security
open import Yggdrasil.Probability using (pure)

open Action↑
open Action↓
open Action↯
open WorldStates

@@ -85,19 +84,19 @@ open WorldStates
[]
; adv = []
; hon =
ncall ⊤ (Maybe M) (λ _ → call↓ here tt ↑ there here >>= λ
ncall ⊤ (Maybe M) (λ _ → call↓ here (there here) tt >>= λ
{ nothing → return nothing
; (just c) → call↓ here c ↑ here
; (just c) → call↓ here here c
}) ∷
ncall M ⊤ (λ m → let
dosend = λ pk m → call↓ (there here) ⟨ pk , m ⟩ ↑ here >>= (λ
doSend = λ pk m → call↓ (there here) here ⟨ pk , m ⟩ >>= (λ
{ nothing → abort -- The public key we set was refused!
; (just c) → call↓ (there here) c ↑ (there here)
; (just c) → call↓ (there here) (there here) c
})
in read >>= λ
{ nothing → call↓ (there (there here)) tt ↑ here >>= (λ pk →
write (just pk) >> dosend pk m)
; (just pk) → dosend pk m
{ nothing → call↓ (there (there here)) here tt >>= (λ pk →
write (just pk) >> doSend pk m)
; (just pk) → doSend pk m
}) ∷
[]
}
@@ -156,11 +155,29 @@ S-SecureChannel {ℓ} M C PK L l pk?= c?= = record
}

secure : {ℓ : Level} → (M C PK L : Set ℓ) → (l : M → L) →
(pk?= : PK → PK → Bool) → (c?= : C → C → Bool) →
(pk?= : PK → PK → Bool) → (c?= : C → C → Bool) → (m?= : M → M → Bool) →
πᵢ-SecureChannel M L l ≃ πᵣ-SecureChannel M C PK L l pk?= c?=
secure {ℓ} M C PK L l pk?= c?= = record
{ sim-gas = λ _ → 1000
; gas-map = _* 10
secure {ℓ} M C PK L l pk?= c?= m?= = record
{ gas-map = _* 2
; simulator = S-SecureChannel M C PK L l pk?= c?=
; proof = λ{ g (strat α O) → ? }
; invariant = λ
{ ⟨ ⟨ stnode (just m) [] , lift true ⟩ ,
stnode (just pk) (
stnode (just ⟨ pk′ , stlog ⟩) [] ∷
stnode (just c) [] ∷
[]
) ⟩ → pk?= pk pk′ ∧ any (λ{ ⟨ m′ , c′ ⟩ → m?= m m′ ∧ c?= c c′ }) stlog
; ⟨ ⟨ stnode nothing [] , lift false ⟩ ,
stnode nothing (
stnode nothing [] ∷
stnode nothing [] ∷
[]
) ⟩ → true
; _ → false
}
; base-case = refl
; proof = λ
{ g σ O (call↓ ∈Γ x) Σ inv → ⟨ ? , ⟨ ? , ? ⟩ ⟩
; g σ O (call↯ ∈Γ Γ⊑ x) Σ inv → ⟨ ? , ⟨ ? , ? ⟩ ⟩
}
}

+ 6
- 0
Yggdrasil/Probability.agda View File

@@ -54,6 +54,12 @@ data Dist {ℓ : Level} : Set ℓ → Set (lsuc ℓ) where
sample : ∀ {n : ℕ} → Dist (PrFin {ℓ} n)
_>>=_ : ∀ {A B : Set ℓ} → Dist A → (A → Dist B) → Dist B

dmap : ∀ {ℓ A B} → (A → B) → Dist {ℓ} A → Dist {ℓ} B
dmap f d = d >>= (λ x → pure (f x))

_*_ : ∀ {ℓ A B} → Dist {ℓ} A → Dist {ℓ} B → Dist {ℓ} (A × B)
a * b = a >>= (λ x → b >>= (λ y → pure ⟨ x , y ⟩))

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

+ 78
- 78
Yggdrasil/Security.agda View File

@@ -9,15 +9,15 @@ open import Data.List using (_∷_; []; map)
open import Data.Product using (_×_; Σ; Σ-syntax; proj₁; proj₂; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Data.Nat using (ℕ; zero; suc; _≤_; _^_; _+_)
open import Data.Integer using (ℤ)
open import Data.Maybe using (Maybe) renaming (map to mmap)
open import Data.Maybe using (Maybe; just; nothing) renaming (map to mmap)
open import Data.Rational using (ℚ)
open import Function using (_∘_)
open import Level using (Level; Lift; lift) renaming (suc to lsuc)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; cong; sym)
open import Relation.Nullary.Decidable using (fromWitnessFalse)
open import Relation.Nullary.Decidable using (True; fromWitnessFalse)
open import Yggdrasil.List using (_∈_; here; there; with-proof; map≡-implies-∈≡)
open import Yggdrasil.World using (WorldType; WorldState; World; Oracle; Call; Strategy; Node; Action; weaken; call; call↓; _↑_; stnode; _∷_; []; ⌊exec⌋; _⊑_; Query; _∈↑_; abort; dist; _>>=_; call↯; query; path; _↑; strat; ⊤; tt; Action↓; exec↓)
open import Yggdrasil.Probability using (Dist; _>>=_; pure; _≈[_]≈_)
open import Yggdrasil.World using (WorldType; WorldState; World; Oracle; Call; Strategy; Node; weaken; call; call↓; stnode; _∷_; []; _⊑_; Query; _∈↑_; abort; dist; _>>=_; call↯; query; path; strat; ⊤; tt; Action⊤; read; write; exec⊤; Result; out-of-gas; result; rmap; T)
open import Yggdrasil.Probability as Pr using (Dist; _>>=_; pure; _≈[_]≈_; dmap; _*_; Pr[_[_]]≡_)
open import Yggdrasil.Rational using (_÷_)
open WorldType
open Node
@@ -47,8 +47,6 @@ data Action↯ {ℓ : Level} (σ : Set ℓ) (Γᵢ Γᵣ : WorldType ℓ)
_>>=_ : ∀ {A B} → Action↯ σ Γᵢ Γᵣ {hon-≡} A → (A → Action↯ σ Γᵢ Γᵣ {hon-≡} B) →
Action↯ σ Γᵢ Γᵣ B

record Simulator {ℓ : Level} (πᵢ πᵣ : World ℓ) : Set (lsuc ℓ) where
Γᵢ : WorldType ℓ
Γᵢ = World.Γ πᵢ
@@ -62,60 +60,55 @@ record Simulator {ℓ : Level} (πᵢ πᵣ : World ℓ) : Set (lsuc ℓ) where
(x : Call.A f) → Action↯ state Γᵢ Γᵣ {hon-≡} (Call.B f x)
query-map : ∀ {q} → q ∈↑ Γᵢ → (x : Query.A q) → Action↯ state Γᵢ Γᵣ {hon-≡} (Query.B q x)

Actionᵣ⇒Actionᵢ : ∀ {ℓ : Level} {πᵢ πᵣ : World ℓ} {A : Set ℓ} →
(S : Simulator πᵢ πᵣ) → Oracle (World.Γ πᵣ) → Simulator.state S → ℕ →
Action (World.Γ πᵣ) A → Action (World.Γ πᵢ) (A × Simulator.state S)
Action↯⇒Action : ∀ {ℓ : Level} {πᵢ πᵣ : World ℓ} {A : Set ℓ} →
(S : Simulator πᵢ πᵣ) → Oracle (World.Γ πᵣ) → Simulator.state S → ℕ →
Actionᵣ⇒Actionᵢ : ∀ {ℓ : Level} {πᵢ πᵣ : World ℓ} {A : Set ℓ} {σ}
(S : Simulator πᵢ πᵣ) → Oracle σ (World.Γ πᵣ) → ℕ →
Action⊤ σ (World.Γ πᵣ) A → Action⊤ (σ × Simulator.state S) (World.Γ πᵢ) A
Action↯⇒Action : ∀ {ℓ : Level} {πᵢ πᵣ : World ℓ} {A : Set ℓ} {σ}
(S : Simulator πᵢ πᵣ) → Oracle σ (World.Γ πᵣ) → ℕ →
Action↯ (Simulator.state S) (World.Γ πᵢ) (World.Γ πᵣ) {Simulator.hon-≡ S} A →
Action (World.Γ πᵢ) (A × Simulator.state S)
Action⊤ (σ × Simulator.state S) (World.Γ πᵢ) A

private
with-state : ∀ {ℓ Γ A Σ} → Σ → A → Action {ℓ} Γ (A × Σ)
with-state σ x = dist (pure ⟨ x , σ ⟩)

without-state : ∀ {ℓ Γ} {A Σ : Set ℓ} → (A × Σ) → Action {ℓ} Γ A
without-state ⟨ x , _ ⟩ = dist (pure x)

Actionᵣ⇒Actionᵢ _ _ _ zero _ = abort
Actionᵣ⇒Actionᵢ S O σ (suc g) ((call↓ {f} ∈Γᵣ x) ↑) with map≡-implies-∈≡
amap : ∀ {ℓ S Γ A B} → (A → B) → Action⊤ {ℓ} S Γ A → Action⊤ {ℓ} S Γ B
amap f α = α >>= (λ x → dist (pure (f x)))
Actionᵣ⇒Actionᵢ S O g read = amap proj₁ read
Actionᵣ⇒Actionᵢ S O g (write σ₁) = read >>= λ { ⟨ _ , σ₂ ⟩ → write ⟨ σ₁ , σ₂ ⟩ }
Actionᵣ⇒Actionᵢ S O g (call↓ {f} ∈Γᵣ x) with map≡-implies-∈≡
(sym (Simulator.hon-≡ S)) ∈Γᵣ
... | ⟨ _ , ⟨ ∈Γᵢ , refl ⟩ ⟩ = call↓ ∈Γᵢ x ↑ >>= with-state σ
Actionᵣ⇒Actionᵢ _ _ _ _ abort = abort
Actionᵣ⇒Actionᵢ _ _ σ _ (dist D) = dist D >>= with-state σ
Actionᵣ⇒Actionᵢ S O σ (suc g) (call↯ ∈Γ Γ⊑ x) = Action↯⇒Action S O σ g
... | ⟨ _ , ⟨ ∈Γᵢ , refl ⟩ ⟩ = call↓ ∈Γᵢ x
Actionᵣ⇒Actionᵢ _ _ _ abort = abort
Actionᵣ⇒Actionᵢ _ _ _ (dist D) = dist D
Actionᵣ⇒Actionᵢ S O g (call↯ ∈Γ Γ⊑ x) = Action↯⇒Action S O g
(Simulator.call↯-map S ∈Γ Γ⊑ x)
Actionᵣ⇒Actionᵢ S O σ (suc g) (α >>= β) = (Actionᵣ⇒Actionᵢ S O σ (suc g) α) >>=
λ{ ⟨ x , σ′ ⟩ → Actionᵣ⇒Actionᵢ S O σ′ g (β x) }

Action↯⇒Action _ _ _ zero _ = abort
Action↯⇒Action S O σ _ read = dist (pure ⟨ σ , σ ⟩)
Action↯⇒Action S O _ _ (write σ) = dist (pure ⟨ tt , σ ⟩)
Action↯⇒Action S O σ (suc g) (query ∈Γ Γ⊑ x) = Actionᵣ⇒Actionᵢ S O σ g (O (path Γ⊑ ∈Γ) x)
Action↯⇒Action _ _ _ _ abort = abort
Action↯⇒Action _ _ σ _ (dist D) = dist D >>= with-state σ
Action↯⇒Action _ _ σ _ (call↯ ∈Γ Γ⊑ x) = call↯ ∈Γ Γ⊑ x >>= with-state σ
Action↯⇒Action S O σ (suc g) (α >>= β) = (Action↯⇒Action S O σ (suc g) α) >>= λ{
⟨ x , σ′ ⟩ → Action↯⇒Action S O σ′ g (β x)
}

extract-oracle : ∀ {ℓ πᵢ πᵣ} → Simulator {ℓ} πᵢ πᵣ → Oracle (World.Γ πᵣ) → ℕ →
Oracle (World.Γ πᵢ)
extract-oracle S O g ∈Γ x = Action↯⇒Action S O (initial S) g
(Simulator.query-map S ∈Γ x) >>= without-state
Actionᵣ⇒Actionᵢ S O g (α >>= β) = (Actionᵣ⇒Actionᵢ S O g α) >>=
Actionᵣ⇒Actionᵢ S O g ∘ β

Action↯⇒Action S O g read = amap proj₂ read
Action↯⇒Action S O g (write σ₂) = read >>= λ { ⟨ σ₁ , _ ⟩ → write ⟨ σ₁ , σ₂ ⟩ }
Action↯⇒Action S O zero (query ∈Γ Γ⊑ x) = abort
Action↯⇒Action S O (suc g) (query ∈Γ Γ⊑ x) = Actionᵣ⇒Actionᵢ S O g (O (path Γ⊑ ∈Γ) x)
Action↯⇒Action S O g abort = abort
Action↯⇒Action S O g (dist D) = dist D
Action↯⇒Action S O g (call↯ ∈Γ Γ⊑ x) = call↯ ∈Γ Γ⊑ x
Action↯⇒Action S O g (α >>= β) = (Action↯⇒Action S O g α) >>=
Action↯⇒Action S O g ∘ β

extract-oracle : ∀ {ℓ σ πᵢ πᵣ} → (S : Simulator {ℓ} πᵢ πᵣ) →
Oracle σ (World.Γ πᵣ) → ℕ → Oracle (σ × Simulator.state S) (World.Γ πᵢ)
extract-oracle S O g ∈Γ x = Action↯⇒Action S O g
(query-map S ∈Γ x)
where open Simulator

simulated-strategy : ∀ {ℓ πᵢ πᵣ A} → Simulator {ℓ} πᵢ πᵣ →
Strategy (World.Γ πᵣ) A → ℕ → Strategy (World.Γ πᵢ) A
simulated-strategy S str g = strat
(Actionᵣ⇒Actionᵢ S (oracle str) (initial S) g (init str) >>= without-state)
(extract-oracle S (oracle str) g)
where open Simulator
data InterestingAction {ℓ : Level} (Γ : WorldType ℓ) : Set ℓ → Set (lsuc ℓ) where
call↓ : ∀ {f} → f ∈ (hon Γ) → (x : Call.A f) → InterestingAction Γ (Call.B f x)
call↯ : ∀ {Γ′} {f : Call ℓ (node Γ′)} → f ∈ (adv Γ′) → Γ′ ⊑ Γ →
(x : Call.A f) → InterestingAction Γ (Call.B f x)

toAction : ∀ {ℓ Γ A S} → InterestingAction {ℓ} Γ A → Action⊤ {ℓ} S Γ A
toAction (call↓ f∈ x) = call↓ f∈ x
toAction (call↯ ∈Γ Γ⊑ x) = call↯ ∈Γ Γ⊑ x

record Adv[_,_]≤_ {ℓ : Level} (πᵢ πᵣ : World ℓ) (ε : ℚ) :
record _≃_ {ℓ : Level} (πᵢ πᵣ : World ℓ) :
Set (lsuc (lsuc ℓ)) where
Γᵣ : WorldType ℓ
Γᵣ = World.Γ πᵣ
@@ -126,43 +119,38 @@ record Adv[_,_]≤_ {ℓ : Level} (πᵢ πᵣ : World ℓ) (ε : ℚ) :
Σᵢ : WorldState Γᵢ
Σᵢ = World.Σ πᵢ
field
sim-gas : ℕ
gas-map : ℕ → ℕ
simulator : Simulator πᵢ πᵣ
invariant : (WorldState Γᵢ × WorldState Γᵣ) × Simulator.state simulator → Bool
base-case : invariant ⟨ ⟨ Σᵢ , Σᵣ ⟩ , Simulator.initial simulator ⟩ ≡ true
proof : (g : ℕ) → (O : Oracle Γᵣ) → ∀ {A} → (α : Action↓ Γᵣ A) →
(Σ : ((WorldState Γᵢ × WorldState Γᵣ) × Simulator.state simulator)) →
invariant Σ ≡ true →
let
dᵢ = exec↓ (extract-oracle simulator O sim-gas)
(Actionᵣ⇒Actionᵢ simulator O (proj₂ Σ) sim-gas α)
(proj₁ (proj₁ Σ)) here g
in ?

--Actionᵣ⇒Actionᵢ : ∀ {ℓ : Level} {πᵢ πᵣ : World ℓ} {A : Set ℓ} →



_≃_ : {ℓ : Level} → (πᵢ πᵣ : World ℓ) → Set (lsuc (lsuc ℓ))
πᵢ ≃ πᵣ = Adv[ πᵢ , πᵣ ]≤ 0

private
+-≡0ˡ : ∀ {n m} → n + m ≡ 0 → n ≡ 0
+-≡0ˡ {zero} _ = refl
+-≡0ˡ {suc n} ()

^≢0 : ∀ {n m} → (suc n) ^ m ≢ 0
^≢0 {n} {zero} ()
^≢0 {n} {suc m} n^sm≡0 = ^≢0 {n} {m} (+-≡0ˡ n^sm≡0)

_≈_ : {ℓ : Level} → (πᵢ πᵣ : ℕ → World ℓ) → ℕ → Set (lsuc (lsuc ℓ))
_≈_ πᵢ πᵣ κ = Adv[ πᵢ κ , πᵣ κ ]≤ (_÷_ 1 (2 ^ κ) {fromWitnessFalse (^≢0 {1} {κ})})
invariant : ((WorldState Γᵢ × Simulator.state simulator) × WorldState Γᵣ) → Bool
base-case : invariant ⟨ ⟨ Σᵢ , Simulator.initial simulator ⟩ , Σᵣ ⟩ ≡ true
proof : (g : ℕ) →
∀ {S} →
(σ : S) →
(O : Oracle S Γᵣ) →
∀ {A} →
(α : InterestingAction Γᵣ A) →
(Σ : (WorldState Γᵢ × Simulator.state simulator) × WorldState Γᵣ) →
invariant Σ ≡ true →
let
Dᵢ = exec⊤ (extract-oracle simulator O (gas-map g))
(Actionᵣ⇒Actionᵢ simulator O (gas-map g) (toAction α))
⟨ ⟨ σ , proj₂ (proj₁ Σ) ⟩ , proj₁ (proj₁ Σ) ⟩ (gas-map g)
Dᵣ = exec⊤ O (toAction α) ⟨ σ , proj₂ Σ ⟩ g
Dₛ = dmap {B = Maybe ((WorldState Γᵢ × Simulator.state simulator) × WorldState Γᵣ)} (λ
{ ⟨ abort , _ ⟩ → nothing
; ⟨ out-of-gas , _ ⟩ → nothing
; ⟨ _ , abort ⟩ → nothing
; ⟨ _ , out-of-gas ⟩ → nothing
; ⟨ result ⟨ _ , ⟨ ⟨ _ , σ ⟩ , Σᵢ ⟩ ⟩
, result ⟨ _ , ⟨ _ , Σᵣ ⟩ ⟩ ⟩ →
just ⟨ ⟨ Σᵢ , σ ⟩ , Σᵣ ⟩
}) (Dᵢ * Dᵣ)
in
-- The results are indistinguishable.
(dmap (rmap (λ x → lift (proj₁ x))) Dᵢ Pr.≃ dmap (rmap (λ x → lift (proj₁ x))) Dᵣ) ×
-- The resulting environment states are indistinguishable.
(dmap (rmap (λ x → lift (proj₁ (proj₁ (proj₂ x))))) Dᵢ
Pr.≃
dmap (rmap (λ x → lift (proj₁ (proj₂ x)))) Dᵣ) ×
-- And any resulting system states are in the invariant.
(Pr[ (λ { nothing → ⊤; (just x) → T (invariant x) }) [ Dₛ ]]≡ 1)

+ 53
- 46
Yggdrasil/World.agda View File

@@ -1,11 +1,11 @@
module Yggdrasil.World where

open import Data.Bool using (Bool)
open import Data.Bool using (Bool; true; false)
open import Data.Empty using (⊥-elim)
open import Data.List using (List; _∷_; []; map)
open import Data.Maybe using (Maybe; nothing; just) renaming (map to mmap)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product using (_×_; ∃; ∃-syntax; proj₁) renaming (_,_ to ⟨_,_⟩)
open import Data.Product using (_×_; ∃; ∃-syntax; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
@@ -16,6 +16,12 @@ open import Yggdrasil.List using (_∈_; here; there)
data ⊤ {ℓ : Level} : Set ℓ where
tt : ⊤

data ⊥ {ℓ : Level} : Set ℓ where

T : ∀ {ℓ} → Bool → Set ℓ
T true = ⊤
T false = ⊥

record Query (ℓ : Level) : Set (lsuc ℓ) where
constructor mkquery
field
@@ -28,8 +34,7 @@ mknquery A B = mkquery A (λ _ → B)
record Node (ℓ : Level) : Set (lsuc ℓ)
record WorldType (ℓ : Level) : Set (lsuc ℓ)
data Action↑ {ℓ : Level} (N : Node ℓ) : Set ℓ → Set (lsuc ℓ)
data Action↓ {ℓ : Level} (Γ : WorldType ℓ) : Set ℓ → Set (lsuc ℓ)
data Action {ℓ : Level} (Γ : WorldType ℓ) : Set ℓ → Set (lsuc ℓ)
data Action⊤ {ℓ : Level} (S : Set ℓ) (Γ : WorldType ℓ) : Set ℓ → Set (lsuc ℓ)

data WorldState {ℓ : Level} (Γ : WorldType ℓ) : Set (lsuc ℓ)
data WorldStates {ℓ : Level} : List (WorldType ℓ) → Set (lsuc ℓ)
@@ -44,6 +49,7 @@ record Node ℓ where

open Node


record Call (ℓ : Level) (N : Node ℓ) : Set (lsuc ℓ) where
inductive
constructor call
@@ -80,24 +86,24 @@ data _⊑_ {ℓ : Level} : (Γ₁ Γ₂ : WorldType ℓ) → Set (lsuc ℓ) wher
⊑-right : ∀ {ℓ} {Γ₁ Γ₂ Γ₃ : WorldType ℓ} → Γ₂ ⊑ Γ₃ → Γ₁ ∈ chld (node Γ₂) → Γ₁ ⊑ Γ₃
⊑-right Γ⊑ ∈Γ = ⊑-trans (there ∈Γ here) Γ⊑

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)
_>>=_ : ∀ {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⊤ {ℓ} S Γ where
read : Action⊤ S Γ S
write : S → Action⊤ S Γ ⊤
call↓ : ∀ {f} → f ∈ (hon Γ) → (x : Call.A f) → Action⊤ S Γ (Call.B f x)
abort : ∀ {A} → Action⊤ S Γ A
dist : ∀ {A} → Dist A → Action⊤ S Γ A
call↯ : ∀ {Γ′} {f : Call ℓ (node Γ′)} → f ∈ (adv Γ′) → Γ′ ⊑ Γ →
(x : Call.A f) → Action⊤ S Γ (Call.B f x)
_>>=_ : ∀ {A B} → Action⊤ S Γ A → (A → Action⊤ S Γ B) → Action⊤ S Γ B

data Action↑ {ℓ} N where
read : Action↑ N (state N)
write : state N → Action↑ N ⊤
call↓ : ∀ {Γ f} → f ∈ (hon Γ) → Γ ∈ chld N → (x : Call.A f) →
Action↑ N (Call.B f x)
abort : ∀ {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

-- TODO: build full monad instances of all actions, and Dist -- once I figure
@@ -125,14 +131,17 @@ record World (ℓ : Level) : Set (lsuc ℓ) where
data _∈↑_ {ℓ : Level} (q : Query ℓ) (Γ : WorldType ℓ) : Set (lsuc ℓ) where
path : ∀ {Γ′} → Γ′ ⊑ Γ → q ∈ qry (node Γ′) → q ∈↑ Γ

Oracle : ∀ {ℓ} → WorldType ℓ → Set (lsuc ℓ)
Oracle Γ = ∀ {q} → q ∈↑ Γ → (x : Query.A q) → Action Γ (Query.B q x)
Oracle : ∀ {ℓ} → Set ℓ → WorldType ℓ → Set (lsuc ℓ)
Oracle S Γ = ∀ {q} → q ∈↑ Γ → (x : Query.A q) → Action⊤ S Γ (Query.B q x)

record Strategy {ℓ : Level} (Γ : WorldType ℓ) (A : Set ℓ) : Set (lsuc ℓ) where
record Strategy {ℓ : Level} (Γ : WorldType ℓ) (A : Set ℓ) {S : Set ℓ} : Set (lsuc ℓ) where
constructor strat
field
init : Action Γ A
oracle : Oracle Γ
state : S
init : Action⊤ S Γ A
oracle : Oracle S Γ



get : ∀ {ℓ Γ₁ Γ₂} → Γ₁ ⊑ Γ₂ → WorldState {ℓ} Γ₂ → state (node Γ₁)
get here (stnode Σ _) = Σ
@@ -162,41 +171,39 @@ rmap _ abort = abort
rmap _ out-of-gas = out-of-gas
rmap f (result x) = result (f x)

exec : ∀ {ℓ Γ A} → Strategy {ℓ} Γ A → WorldState {ℓ} Γ → ℕ →
exec : ∀ {ℓ S Γ A} → Strategy {ℓ} Γ A {S} → WorldState {ℓ} Γ → ℕ →
Dist (Result (Lift (lsuc ℓ) A))
exec : ∀ {ℓ Γ A} → Oracle Γ → Action Γ A → WorldState {ℓ} Γ → ℕ →
Dist (Result (A × WorldState {ℓ} Γ))
exec↓ : ∀ {ℓ Γ₁ Γ₂ A} → Oracle Γ₁ → Action↓ Γ₂ A → WorldState {ℓ} Γ₁ →
Γ₂ ⊑ Γ₁ → ℕ → Dist (Result (A × WorldState {ℓ} Γ₁))
exec↑ : ∀ {ℓ Γ₁ Γ₂ A} → Oracle Γ₁ → Action↑ (node Γ₂) A → WorldState {ℓ} Γ₁ →
Γ₂ ⊑ Γ₁ → ℕ → Dist (Result (A × WorldState {ℓ} Γ₁))
exec⊤ : ∀ {ℓ S Γ A} → Oracle S Γ → Action⊤ S Γ A → S × WorldState {ℓ} Γ → ℕ →
Dist (Result (A × (S × WorldState {ℓ} Γ)))
exec↑ : ∀ {ℓ S Γ₁ Γ₂ A} → Oracle S Γ₁ → Action↑ (node Γ₂) A →
(S × WorldState {ℓ} Γ₁) → Γ₂ ⊑ Γ₁ → ℕ → Dist (Result (A × (S × WorldState {ℓ} Γ₁)))

-- NOTE: Gas is only used for termination here, it is NOT a computational model.
exec (strat α O) Σ g = (exec O α Σ g) >>= (pure ∘ rmap (llift ∘ proj₁))
exec (strat S α O) Σ g = (exec O α ⟨ S , Σ g) >>= (pure ∘ rmap (llift ∘ proj₁))

exec O α Σ zero = pure out-of-gas
exec O (α ↑) Σ g = exec↓ O α Σ here g
exec O abort Σ g = pure abort
exec O (dist D) Σ (suc g) = lift D >>= λ{
exec⊤ O read Σ g = pure (result ⟨ proj₁ Σ , Σ ⟩)
exec⊤ O (write σ) Σ g = pure (result ⟨ tt , ⟨ σ , proj₂ Σ ⟩ ⟩)
exec⊤ O (call↓ {f = f} ∈Γ x) Σ g = exec↑ O (Call.δ f x) Σ here g
exec⊤ O abort Σ g = pure abort
exec⊤ O (dist D) Σ g = lift D >>= λ{
(llift x) → pure (result ⟨ x , Σ ⟩ ) }
exec O (call↯ {f = f} f∈ ⊑Γ x) Σ (suc g) = exec↑ O (Call.δ f x) Σ ⊑Γ g
exec O (α >>= β) Σ (suc g) = (exec O α Σ (suc g)) >>= λ{
(result ⟨ x , Σ′ ⟩) → exec O (β x) Σ′ g ;
exec⊤ O (call↯ {f = f} f∈ ⊑Γ x) Σ g = exec↑ O (Call.δ f x) Σ ⊑Γ g
exec⊤ O (α >>= β) Σ g = (exec⊤ O α Σ g) >>= λ{
(result ⟨ x , Σ′ ⟩) → exec O (β x) Σ′ g ;
abort → pure abort ;
out-of-gas → pure out-of-gas }

exec↓ _ _ _ _ zero = pure out-of-gas
exec↓ O (call↓ {f = f} f∈ x) Σ ⊑Γ (suc g) = exec↑ O (Call.δ f x) Σ ⊑Γ g

exec↑ O α Σ ⊑Γ zero = pure out-of-gas
exec↑ O read Σ ⊑Γ _ = pure (result ⟨ get ⊑Γ Σ , Σ ⟩)
exec↑ O (write σ) Σ ⊑Γ _ = pure (result ⟨ tt , set ⊑Γ Σ σ ⟩)
exec↑ O abort Σ ⊑Γ _ = pure abort
exec↑ O (dist D) Σ ⊑Γ _ = lift D >>=
exec↑ O read Σ ⊑Γ g = pure (result
⟨ get ⊑Γ (proj₂ Σ) , Σ ⟩)
exec↑ O (write σ) Σ ⊑Γ g = pure (result
⟨ tt , ⟨ proj₁ Σ , set ⊑Γ (proj₂ Σ) σ ⟩ ⟩)
exec↑ O abort Σ ⊑Γ g = pure abort
exec↑ O (dist D) Σ ⊑Γ g = lift D >>=
λ{ (llift x) → pure (result ⟨ x , Σ ⟩) }
exec↑ O (query {q = q} q∈ x) Σ ⊑Γ (suc g) = exec O (O (path ⊑Γ q∈) x) Σ g
exec↑ O (α ↑ Γ′∈) Σ ⊑Γ (suc g) = exec↓ O α Σ (⊑-right ⊑Γ Γ′∈) g
exec↑ O (α >>= β) Σ ⊑Γ (suc g) = (exec↑ O α Σ ⊑Γ (suc g))
exec↑ O (query {q = q} q∈ x) Σ ⊑Γ zero = pure out-of-gas
exec↑ O (query {q = q} q∈ x) Σ ⊑Γ (suc g) = exec⊤ O (O (path ⊑Γ q∈) x) Σ g
exec↑ O (call↓ {f = f} ∈Γ Γ∈ x) Σ ⊑Γ g = exec↑ O (Call.δ f x) Σ (⊑-right ⊑Γ Γ∈) g
exec↑ O (α >>= β) Σ ⊑Γ g = (exec↑ O α Σ ⊑Γ g)
>>= λ{
(result ⟨ x , Σ′ ⟩) → exec↑ O (β x) Σ′ ⊑Γ g ;
abort → pure abort ;

Loading…
Cancel
Save