Browse Source

Almost working example!

gas-move-test
Thomas Kerber 1 year ago
parent
commit
b7de611e6e
Signed by: Thomas Kerber <t.kerber@ed.ac.uk> GPG Key ID: 8489B911F9ED617B
3 changed files with 294 additions and 99 deletions
  1. +165
    -0
      Yggdrasil/Examples/SecureChannel.agda
  2. +76
    -61
      Yggdrasil/Security.agda
  3. +53
    -38
      Yggdrasil/World.agda

+ 165
- 0
Yggdrasil/Examples/SecureChannel.agda View File

@@ -0,0 +1,165 @@
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.Maybe using (Maybe; just; nothing)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
open import Level using (Level; Lift; lift)
open import Relation.Binary.PropositionalEquality using (refl)
open import Yggdrasil.World
open import Yggdrasil.List
open import Yggdrasil.Security
open import Yggdrasil.Probability using (pure)

open Action↑
open Action↓
open Action↯
open WorldStates

πᵢ-SecureChannel : {ℓ : Level} → (M L : Set ℓ) → (M → L) → World ℓ
πᵢ-SecureChannel M L l = record
{ Γ = record
{ node = mknode (Maybe M) [] (mknquery L ⊤ ∷ [])
; adv = []
; hon =
ncall ⊤ (Maybe M) (λ _ → read) ∷
ncall M ⊤ (λ m → write (just m) >> query here (l m) >> return tt) ∷
[]
}
; Σ = stnode nothing []
}

πᵢ-AuthChannel : {ℓ : Level} → Set ℓ → World ℓ
πᵢ-AuthChannel M = record
{ Γ = record
{ node = mknode (Maybe M) [] (mknquery M ⊤ ∷ [])
; adv = []
; hon =
ncall ⊤ (Maybe M) (λ _ → read) ∷
ncall M ⊤ (λ m → write (just m) >> query here m >> return tt) ∷
[]
}
; Σ = stnode nothing []
}

πᵢ-PKE : {ℓ : Level} → (M C PK L : Set ℓ) → (M → L) → (PK → PK → Bool) →
(C → C → Bool) → World ℓ
πᵢ-PKE M C PK L l pk?= c?= = record
{ Γ = record
{ node = mknode (Maybe (PK × List (M × C))) []
(mknquery L C ∷ mknquery ⊤ PK ∷ [])
; adv = []
; hon =
ncall C (Maybe M) (λ c → read >>= λ
{ nothing → return nothing
; (just ⟨ _ , log ⟩) → return (in-log c log)
}) ∷
ncall (PK × M) (Maybe C) (λ{ ⟨ pk′ , m ⟩ → read >>= λ
{ nothing → return nothing
; (just ⟨ pk , log ⟩) → if pk?= pk pk′ then
query here (l m) >>=
(λ c → write (just ⟨ pk , ⟨ m , c ⟩ ∷ log ⟩) >>
return (just c)) else
return nothing
}}) ∷
ncall ⊤ PK (λ _ → query (there here) tt >>=
(λ pk → write (just ⟨ pk , [] ⟩) >> return pk)) ∷
[]
}
; Σ = stnode nothing []
}
where
in-log : C → List (M × C) → Maybe M
in-log c [] = nothing
in-log c (⟨ m , c′ ⟩ ∷ log) = if c?= c c′ then just m else in-log c log

πᵣ-SecureChannel : {ℓ : Level} → (M C PK L : Set ℓ) → (M → L) →
(PK → PK → Bool) → (C → C → Bool) → World ℓ
πᵣ-SecureChannel M C PK L l pk?= c?= = record
{ Γ = record
{ node = mknode (Maybe PK) (
World.Γ (πᵢ-PKE M C PK L l pk?= c?=) ∷
World.Γ (πᵢ-AuthChannel C) ∷
[])
[]
; adv = []
; hon =
ncall ⊤ (Maybe M) (λ _ → call↓ here tt ↑ there here >>= λ
{ nothing → return nothing
; (just c) → call↓ here c ↑ here
}) ∷
ncall M ⊤ (λ m → let
dosend = λ pk m → call↓ (there here) ⟨ pk , m ⟩ ↑ here >>= (λ
{ nothing → abort -- The public key we set was refused!
; (just c) → call↓ (there here) c ↑ (there here)
})
in read >>= λ
{ nothing → call↓ (there (there here)) tt ↑ here >>= (λ pk →
write (just pk) >> dosend pk m)
; (just pk) → dosend pk m
}) ∷
[]
}
; Σ = stnode nothing (
World.Σ (πᵢ-PKE M C PK L l pk?= c?=) ∷
World.Σ (πᵢ-AuthChannel C) ∷
[])
}

BitString : ∀ {ℓ} → Set ℓ
BitString {ℓ} = Lift ℓ (List Bool)

bitstring?= : ∀ {ℓ} → BitString {ℓ} → BitString {ℓ} → Bool
bitstring?= (lift []) (lift []) = true
bitstring?= (lift (_ ∷ _)) (lift []) = false
bitstring?= (lift []) (lift (_ ∷ _)) = false
bitstring?= {ℓ} (lift (true ∷ xs)) (lift (true ∷ ys)) = bitstring?= {ℓ} (lift xs) (lift ys)
bitstring?= {ℓ} (lift (false ∷ xs)) (lift (false ∷ ys)) = bitstring?= {ℓ} (lift xs) (lift ys)
bitstring?= (lift (true ∷ xs)) (lift (false ∷ ys)) = false
bitstring?= (lift (false ∷ xs)) (lift (true ∷ ys)) = false

_>>↯_ : ∀ {ℓ Σ Γᵢ Γᵣ A B hon-≡} → Action↯ {ℓ} Σ Γᵢ Γᵣ {hon-≡} A →
Action↯ {ℓ} Σ Γᵢ Γᵣ {hon-≡} B →
Action↯ {ℓ} Σ Γᵢ Γᵣ {hon-≡} B
α >>↯ β = α >>= (λ _ → β)

S-SecureChannel : {ℓ : Level} → (M C PK L : Set ℓ) → (l : M → L) →
(pk?= : PK → PK → Bool) → (c?= : C → C → Bool) →
Simulator (πᵢ-SecureChannel M L l) (πᵣ-SecureChannel M C PK L l pk?= c?=)
S-SecureChannel {ℓ} M C PK L l pk?= c?= = record
{ hon-≡ = refl
; state = Lift ℓ Bool
; initial = lift false
; call↯-map = λ
{ () here
; () (there here here)
; _ (there here (there () _))
; () (there (there here) here)
; _ (there (there here) (there () _))
; _ (there (there (there ())) _)
}
; query-map = λ
{ (path here here) l → read >>= let
perform-leak = query here (there here here) l >>= (λ c →
query here (there (there here) here) c)
in λ
-- 1. on the first leakage seen, query a π-PKE public key (ignore it).
-- 2. on *all* leakages seen, query a π-PKE ciphertext with the leakage
-- 3. finally, query a π-AuthChannel message, with the previous ciphertext.
{ (lift false) → query (there here) (there here here) tt >>↯ perform-leak
; (lift true) → perform-leak
}
; (path here (there ()))
; (path (there () _) _)
}
}

secure : {ℓ : Level} → (M C PK L : Set ℓ) → (l : M → L) →
(pk?= : PK → PK → Bool) → (c?= : C → C → Bool) →
πᵢ-SecureChannel M L l ≃ πᵣ-SecureChannel M C PK L l pk?= c?=
secure {ℓ} M C PK L l pk?= c?= = record
{ g-exec-min = ?
; g-sim-min = ?
; simulator = S-SecureChannel M C PK L l pk?= c?=
; proof = ?
}

+ 76
- 61
Yggdrasil/Security.agda View File

@@ -9,14 +9,13 @@ open import Data.Product using (_×_; Σ; Σ-syntax; proj₁; proj₂; ∃; ∃-
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.Unit using (⊤; tt)
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)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; cong; sym)
open import Relation.Nullary.Decidable using (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)
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)
open import Yggdrasil.Probability using (Dist; _>>=_; pure; _≈[_]≈_)
open import Yggdrasil.Rational using (_÷_)
open WorldType
@@ -34,81 +33,97 @@ instance
data Guess {ℓ : Level} : Set ℓ where
real? ideal? : Guess

data Action↯ {ℓ : Level} (Γᵢ Γᵣ : WorldType ℓ)
data Action↯ {ℓ : Level} (σ : Set ℓ) (Γᵢ Γᵣ : 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 Simulator {ℓ : Level} (Γᵢ Γᵣ : WorldType ℓ) : Set (lsuc ℓ) where
read : Action↯ σ Γᵢ Γᵣ σ
write : σ → Action↯ σ Γᵢ Γᵣ ⊤
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

-- FIXME: Am I an idiot? Shouldn't the simulator map attacks against *real*
-- protocols to attacks against *ideal* protocols?
record Simulator {ℓ : Level} (πᵢ πᵣ : World ℓ) : Set (lsuc ℓ) where
Γᵢ : WorldType ℓ
Γᵢ = World.Γ πᵢ
Γᵣ : WorldType ℓ
Γᵣ = World.Γ πᵣ
field
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)
call↯-map : ∀ {Γ′} {f : Call ℓ (node Γ′)} → f ∈ (adv Γ′) → Γ′ ⊑ Γ
(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)

open Simulator

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

Actionᵢ⇒Actionᵣ _ _ zero _ = abort
Actionᵢ⇒Actionᵣ S O (suc g) ((call↓ ∈Γᵢ x) ↑) with map≡-implies-∈≡ (hon-≡ S) ∈Γᵢ
... | ⟨ _ , ⟨ ∈Γᵣ , refl ⟩ ⟩ = call↓ ∈Γᵣ x ↑
Actionᵢ⇒Actionᵣ _ _ _ abort = abort
Actionᵢ⇒Actionᵣ _ _ _ (dist D) = dist D
Actionᵢ⇒Actionᵣ S O (suc g) (call↯ ∈Γ Γ⊑ x) = Action↯⇒Action S O g (call↯-map S ∈Γ Γ⊑ x)
Actionᵢ⇒Actionᵣ S O (suc g) (α >>= β) = (Actionᵢ⇒Actionᵣ S O (suc g) α) >>=
(Actionᵢ⇒Actionᵣ S O g ∘ β)

Action↯⇒Action _ _ zero _ = abort
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
Action↯⇒Action _ _ _ (call↯ ∈Γ Γ⊑ x) = call↯ ∈Γ Γ⊑ x
Action↯⇒Action S O (suc g) (α >>= β) = (Action↯⇒Action S O (suc g) α) >>=
(Action↯⇒Action S O g ∘ β)

extract-oracle : ∀ {ℓ Γᵢ Γᵣ} → Simulator {ℓ} Γᵢ Γᵣ → Oracle Γᵢ → ℕ → Oracle Γᵣ
extract-oracle S O g ∈Γ x = Action↯⇒Action S O g (query-map S ∈Γ x)

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

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-∈≡ (sym (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 (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 (query-map S ∈Γ x)
>>= without-state

simulated-strategy : ∀ {ℓ πᵢ πᵣ A} → Simulator {ℓ} πᵢ πᵣ →
Strategy (World.Γ πᵣ) A → ℕ → Strategy (World.Γ πᵢ) A
simulated-strategy S str g = strat
(Actionᵢ⇒Actionᵣ S (oracle str) g (init str))
(Actionᵣ⇒Actionᵢ S (oracle str) (initial S) g (init str) >>= without-state)
(extract-oracle S (oracle str) g)

record Challenge {ℓ : Level} : Set (lsuc ℓ) where
field
Γᵢ : WorldType ℓ
Γᵣ : WorldType ℓ
Σᵢ : WorldState Γᵢ
Σᵣ : WorldState Γᵣ
sim : Simulator Γᵢ Γᵣ

record Adv[_]≤_ {ℓ : Level} (c : Challenge {ℓ}) (ε : ℚ) :
record Adv[_,_]≤_ {ℓ : Level} (πᵢ πᵣ : World ℓ) (ε : ℚ) :
Set (lsuc (lsuc ℓ)) where
field
g-exec-min : ℕ
g-sim-min : ℕ
simulator : Simulator πᵢ πᵣ
proof : (g-exec g-sim : ℕ) → g-exec-min ≤ g-exec → g-sim-min ≤ g-sim →
(str : Strategy (Challenge.Γᵢ c) Guess) →
(⌊exec⌋ str (Challenge.Σᵢ c) g-exec)
(str : Strategy (World.Γ πᵣ) Guess) →
(⌊exec⌋ (simulated-strategy simulator str g-sim) (World.Σ πᵢ) g-exec)
≈[ ε ]≈
(⌊exec⌋ (simulated-strategy (Challenge.sim c) str g-sim) (Challenge.Σᵣ c)
g-exec)
(⌊exec⌋ str (World.Σ πᵣ) g-exec)

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

private
+-≡0ˡ : ∀ {n m} → n + m ≡ 0 → n ≡ 0
@@ -119,5 +134,5 @@ private
^≢0 {n} {zero} ()
^≢0 {n} {suc m} n^sm≡0 = ^≢0 {n} {m} (+-≡0ˡ n^sm≡0)

Computational : {ℓ : Level} → ℕ → (ℕ → Challenge {ℓ}) → Set (lsuc (lsuc ℓ))
Computational κ f = Adv[ f κ ]≤ (_÷_ 1 (2 ^ κ) {fromWitnessFalse (^≢0 {1} {κ})})
_≈_ : {ℓ : Level} → (πᵢ πᵣ : ℕ → World ℓ) → ℕ → Set (lsuc (lsuc ℓ))
_≈_ πᵢ πᵣ κ = Adv[ πᵢ κ , πᵣ κ ]≤ (_÷_ 1 (2 ^ κ) {fromWitnessFalse (^≢0 {1} {κ})})

+ 53
- 38
Yggdrasil/World.agda View File

@@ -5,7 +5,7 @@ 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₁) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
@@ -13,14 +13,20 @@ open import Level using (Level; Lift) renaming (suc to lsuc; lift to llift)
open import Yggdrasil.Probability using (Dist; pure; _>>=_; lift)
open import Yggdrasil.List using (_∈_; here; there)

data ⊤ {ℓ : Level} : Set ℓ where
tt : ⊤

record Query (ℓ : Level) : Set (lsuc ℓ) where
constructor mkquery
field
A : Set ℓ
B : A → Set ℓ

mknquery : {ℓ : Level} → Set ℓ → Set ℓ → Query ℓ
mknquery A B = mkquery A (λ _ → B)

record Node (ℓ : Level) : Set (lsuc ℓ)
record WorldType (ℓ : Level) : Set (lsuc ℓ)
--data Action↯ {ℓ : Level} (Γ : WorldType ℓ) : Set ℓ → Set (lsuc ℓ)
data Action↑ {ℓ : Level} (N : Node ℓ) : Set ℓ → Set (lsuc ℓ)
data Action↓ {ℓ : Level} (Γ : WorldType ℓ) : Set ℓ → Set (lsuc ℓ)
data Action {ℓ : Level} (Γ : WorldType ℓ) : Set ℓ → Set (lsuc ℓ)
@@ -30,6 +36,7 @@ data WorldStates {ℓ : Level} : List (WorldType ℓ) → Set (lsuc ℓ)

record Node ℓ where
inductive
constructor mknode
field
state : Set ℓ
chld : List (WorldType ℓ)
@@ -43,13 +50,18 @@ record Call (ℓ : Level) (N : Node ℓ) : Set (lsuc ℓ) where
field
A : Set ℓ
B : A → Set ℓ
δ : (state N) → (x : A) → (state N) × Action↑ N (B x)
δ : (x : A) → Action↑ N (B x)

-- A non-dependently typed instance of call.
ncall : {ℓ : Level} {N : Node ℓ} → (A B : Set ℓ) → (A → Action↑ N B) → Call ℓ N
ncall A B δ = call A (λ _ → B) δ

weaken : ∀ {ℓ N} → Call ℓ N → Query ℓ
weaken c = record { A = Call.A c; B = Call.B c }

record WorldType ℓ where
inductive
constructor tynode
field
node : Node ℓ
adv : List (Call ℓ node)
@@ -76,24 +88,28 @@ data Action {ℓ} Γ where
Action Γ (Call.B f x)
_>>=_ : ∀ {A B} → Action Γ A → (A → Action Γ B) → Action Γ B

--A = Action↯ Γ A ⊎ Action↓ Γ A
--data Action↯ {ℓ} Γ where

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

data Action↑ {ℓ} N where
read : Action↑ N (state N)
write : state N → Action↑ N ⊤
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
-- out how that works in agda.
return : ∀ {ℓ N A} → A → Action↑ {ℓ} N A
return x = dist (pure x)

infixl 1 _>>=_ _>>_

_>>_ : ∀ {ℓ N A B} → Action↑ {ℓ} N A → Action↑ {ℓ} N B → Action↑ {ℓ} N B
α >> β = α >>= (λ _ → β)

data WorldStates {ℓ} where
[] : WorldStates []
_∷_ : ∀ {Γ Γs} → WorldState Γ → WorldStates Γs → WorldStates (Γ ∷ Γs)
@@ -101,8 +117,10 @@ data WorldStates {ℓ} where
data WorldState {ℓ} Γ where
stnode : state (node Γ) → WorldStates (chld (node Γ)) → WorldState Γ

World : (ℓ : Level) → Set (lsuc ℓ)
World ℓ = Σ (WorldType ℓ) WorldState
record World (ℓ : Level) : Set (lsuc ℓ) where
field
Γ : WorldType ℓ
Σ : WorldState Γ

data _∈↑_ {ℓ : Level} (q : Query ℓ) (Γ : WorldType ℓ) : Set (lsuc ℓ) where
path : ∀ {Γ′} → Γ′ ⊑ Γ → q ∈ qry (node Γ′) → q ∈↑ Γ
@@ -140,57 +158,36 @@ exec : ∀ {ℓ Γ A} → Strategy {ℓ} Γ A → WorldState {ℓ} Γ → ℕ
Dist (Maybe (A × WorldState {ℓ} Γ))
exec′ : ∀ {ℓ Γ A} → Oracle Γ → Action Γ A → WorldState {ℓ} Γ → ℕ →
Dist (Maybe (A × WorldState {ℓ} Γ))
--exec↯ : ∀ {ℓ Γ A} → Oracle Γ → Action↯ Γ A → WorldState {ℓ} Γ → ℕ →
exec↓ : ∀ {ℓ Γ₁ Γ₂ A} → Oracle Γ₁ → Action↓ Γ₂ A → WorldState {ℓ} Γ₁ →
Γ₂ ⊑ Γ₁ → ℕ → Dist (Maybe (A × WorldState {ℓ} Γ₁))
exec↑ : ∀ {ℓ Γ₁ Γ₂ N A} → Oracle Γ₁ → Action↑ N A → WorldState {ℓ} Γ₁ →
Γ₂ ⊑ Γ₁ → N ≡ node Γ₂ → ℕ → Dist (Maybe (A × WorldState {ℓ} Γ₁))
exec↑ : ∀ {ℓ Γ₁ Γ₂ A} → Oracle Γ₁ → Action↑ (node Γ₂) A → WorldState {ℓ} Γ₁ →
Γ₂ ⊑ Γ₁ → ℕ → Dist (Maybe (A × WorldState {ℓ} Γ₁))

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

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′ O (α >>= β) Σ (suc g) = (exec′ O α Σ (suc g)) >>= λ{
exec′ O α Σ zero = pure nothing
exec′ O (α ↑) Σ g = exec↓ O α Σ here g
exec′ O abort Σ g = pure nothing
exec′ O (dist D) Σ (suc g) = lift D >>= λ{ (llift x) → pure (just ⟨ x , Σ ⟩ ) }
exec′ O (call↯ {f = f} f∈ ⊑Γ x) Σ (suc g) = exec↑ O (Call.δ f x) Σ ⊑Γ 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 = pure nothing
exec↑ O abort Σ ⊑Γ N≡ (suc g) = pure nothing
exec↑ O (dist D) Σ ⊑Γ N≡ (suc g) = lift D >>=
exec↓ _ _ _ _ zero = pure nothing
exec↓ O (call↓ {f = f} f∈ x) Σ ⊑Γ (suc g) = exec↑ O (Call.δ f x) Σ ⊑Γ g

exec↑ O α Σ ⊑Γ zero = pure nothing
exec↑ O read Σ ⊑Γ _ = pure (just ⟨ get ⊑Γ Σ , Σ ⟩)
exec↑ O (write σ) Σ ⊑Γ _ = pure (just ⟨ tt , set ⊑Γ Σ σ ⟩)
exec↑ O abort Σ ⊑Γ _ = pure nothing
exec↑ O (dist D) Σ ⊑Γ _ = lift D >>=
λ{ (llift x) → pure (just ⟨ x , Σ ⟩) }
exec↑ O (query {q = q} q∈ x) Σ ⊑Γ refl (suc g) =
exec′ O (O (path ⊑Γ q∈) x) Σ g
exec↑ O (α ↑ Γ′∈) Σ ⊑Γ refl (suc g) = exec↓ O α Σ (⊑-right ⊑Γ Γ′∈) g
exec↑ O (α >>= β) Σ ⊑Γ N≡ (suc g) = (exec↑ O α Σ ⊑Γ N≡ (suc g)) >>= λ{
(just ⟨ x , Σ′ ⟩) → exec↑ O (β x) Σ′ ⊑Γ N≡ g;
nothing → pure nothing }
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))
>>= λ{
(just ⟨ x , Σ′ ⟩) → exec↑ O (β x) Σ′ ⊑Γ g;
nothing → pure nothing }

Loading…
Cancel
Save