Browse Source

Start working on probability stuff.

gas-move-test
Thomas Kerber 1 year ago
parent
commit
5286d8340f
Signed by: Thomas Kerber <t.kerber@ed.ac.uk> GPG Key ID: 8489B911F9ED617B
4 changed files with 141 additions and 13 deletions
  1. +26
    -1
      Yggdrasil/List.agda
  2. +75
    -0
      Yggdrasil/Probability.agda
  3. +39
    -12
      Yggdrasil/Security.agda
  4. +1
    -0
      Yggdrasil/World.agda

+ 26
- 1
Yggdrasil/List.agda View File

@@ -1,8 +1,33 @@
module Yggdrasil.List where

open import Data.List using (List; _∷_)
open import Data.List using (List; _∷_; []; map)
open import Data.Product using (_×_; Σ; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

data _∈_ {ℓ : Level} {A : Set ℓ} : A → List A → Set ℓ where
here : {x : A} {xs : List A} → x ∈ (x ∷ xs)
there : {x y : A} {xs : List A} → y ∈ xs → y ∈ (x ∷ xs)

with-proof : ∀ {ℓ} {A : Set ℓ} → (l : List A) → List (Σ A (_∈ l))
with-proof [] = []
with-proof (x ∷ xs) = ⟨ x , here ⟩ ∷ map (λ{⟨ x , ∈xs ⟩ → ⟨ x , there ∈xs ⟩})
(with-proof xs)

head-≡ : ∀ {ℓ} {A : Set ℓ} {l₁ l₂ : List A} {x y : A} → x ∷ l₁ ≡ y ∷ l₂ → x ≡ y
head-≡ refl = refl

tail-≡ : ∀ {ℓ} {A : Set ℓ} {l₁ l₂ : List A} {x y : A} → x ∷ l₁ ≡ y ∷ l₂ →
l₁ ≡ l₂
tail-≡ refl = refl

map≡-implies-∈≡ : ∀ {ℓ} {A B C : Set ℓ} {f₁ : A → C} {f₂ : B → C} {l₁ : List A}
{l₂ : List B} {x : A} → map f₁ l₁ ≡ map f₂ l₂ →
x ∈ l₁ → ∃[ y ] ((y ∈ l₂) × (f₁ x ≡ f₂ y))
map≡-implies-∈≡ {l₁ = x ∷ xs} {l₂ = []} () here
map≡-implies-∈≡ {l₁ = x ∷ xs} {l₂ = []} () (there ∈xs)
map≡-implies-∈≡ {l₁ = x ∷ xs} {l₂ = y ∷ ys} map≡ here =
⟨ y , ⟨ here , head-≡ map≡ ⟩ ⟩
map≡-implies-∈≡ {l₁ = x ∷ xs} {l₂ = y ∷ ys} map≡ (there ∈xs) = let
⟨ y , ⟨ ∈ys , x≡y ⟩ ⟩ = map≡-implies-∈≡ (tail-≡ map≡) ∈xs
in ⟨ y , ⟨ there ∈ys , x≡y ⟩ ⟩

+ 75
- 0
Yggdrasil/Probability.agda View File

@@ -0,0 +1,75 @@
module Yggdrasil.Probability where

open import Data.List using (List; _∷_; []; map; filter; length)
open import Data.Fin using (Fin; zero; suc)
open import Data.Integer using (+_; _-_) renaming (_*_ to _ℤ*_)
open import Data.Nat using (ℕ; zero; suc) renaming (_*_ to _ℕ*_)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
open import Data.Rational using (ℚ; _÷_; _≤?_)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Nullary.Decidable using (True)
open import Level using (Level; Lift; lift) renaming (suc to lsuc)

data [0,1] : Set where
interval : (q : ℚ) → {≤1 : True (q ≤? (+ 1 ÷ 1))} {0≤ : True ((+ 0 ÷ 1) ≤? q)} → [0,1]

1-_ : [0,1] → [0,1]
1- (interval q {q≤1} {0≤q}) = let
n = ℚ.numerator q
d = suc (ℚ.denominator-1 q)
n′ = + d - n
n′∣̷d = ?
1-q = _÷_ n′ d {n′∣̷d}
1-q≤1 = ?
0≤1-q = ?
in interval 1-q {1-q≤1} {0≤1-q}

_*_ : [0,1] → [0,1] → [0,1]
(interval q₁ {q₁≤1} {0≤q₁}) * (interval q₂ {q₂≤1} {0≤q₂}) = let
n₁ = ℚ.numerator q₁
n₂ = ℚ.numerator q₂
d₁ = suc (ℚ.denominator-1 q₁)
d₂ = suc (ℚ.denominator-1 q₂)
n′ = n₁ ℤ* n₂
d′ = d₁ ℕ* d₂
q₁*q₂ = ?
q₁*q₂≤1 = ?
0≤q₁*q₂ = ?
in interval q₁*q₂ {q₁*q₂≤1} {0≤q₁*q₂}

case : [0,1] → [0,1] → [0,1] → [0,1]
case = ?

_/_ : ℕ → ℕ → [0,1]
_/_ = ?

PrFin : ∀ {ℓ} → ℕ → Set ℓ
PrFin {ℓ} n = Lift ℓ (Fin (suc (suc n)))

all-fin : (n : ℕ) → List (Fin n)
all-fin zero = []
all-fin (suc n) = zero ∷ map suc (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)))))

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

data Pr[_[_]]≡_ {ℓ : Level} : {A : Set ℓ} → (P : A → Set ℓ) → Dist A →
[0,1] → Set (lsuc ℓ) where
pure-zero : {A : Set ℓ} {P : A → Set ℓ} → (x : A) → ¬ (P x) →
Pr[ P [ pure x ]]≡ (interval (+ 0 ÷ 1))
pure-one : {A : Set ℓ} {P : A → Set ℓ} → (x : A) → P x →
Pr[ P [ pure x ]]≡ (interval (+ 1 ÷ 1))
sample-count : {n : ℕ} {P : PrFin n → Set ℓ} →
(dec : (f : PrFin n) → Dec (P f)) →
Pr[ P [ sample {n = n} ]]≡ (count dec / suc (suc n))
conditional : {A B : Set ℓ} {D : Dist A} {f : A → Dist B} {P₁ : A → Set ℓ}
{P₂ : B → Set ℓ} {p₁ p₂ p₃ : [0,1]} →
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₃)

+ 39
- 12
Yggdrasil/Security.agda View File

@@ -1,12 +1,16 @@
module Yggdrasil.Security where

open import Data.List using (map)
open import Data.Product using (_×_; Σ; Σ-syntax; proj₁; proj₂; ∃; ∃-syntax)
open import Level using (Level) renaming (suc to lsuc)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Yggdrasil.List using (_∈_)
open import Yggdrasil.World using (WorldType; World; Call; Strategy; weaken)
open import Data.List using (_∷_; []; map)
open import Data.Product using (_×_; Σ; Σ-syntax; proj₁; proj₂; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Data.Nat using (ℕ)
open import Data.Maybe using (Maybe) renaming (map to mmap)
open import Data.Unit using (⊤; tt)
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 WorldType
open Node

data Guess {ℓ : Level} : Set ℓ where
real? ideal? : Guess
@@ -16,7 +20,6 @@ data Outcome : Set where

record RouterConfig {ℓ : Level} : Set (lsuc ℓ) where
field
ref : Guess {ℓ}
real : World ℓ
ideal : World ℓ
sim : Σ[ σ ∈ Set ℓ ] (σ × (∀ {c} → σ → c ∈ adv (proj₁ ideal) →
@@ -26,15 +29,39 @@ record RouterConfig {ℓ : Level} : Set (lsuc ℓ) where
open RouterConfig

router-world-type : ∀ {ℓ} → RouterConfig {ℓ} → WorldType ℓ
router-world-type = ?
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 : ∀ {ℓ} → RouterConfig {ℓ} → Guess {ℓ} → World ℓ
router-world = ?
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 {ℓ} → Outcome
yggdrasil-game = ?
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)

+ 1
- 0
Yggdrasil/World.agda View File

@@ -38,6 +38,7 @@ open Node

record Call (ℓ : Level) (N : Node ℓ) : Set (lsuc ℓ) where
inductive
constructor call
field
A : Set ℓ
B : A → Set ℓ

Loading…
Cancel
Save