Compare commits

...

No commits in common. 'master' and 'oldhaskell' have entirely different histories.

  1. 2
      .gitignore
  2. 8
      ChangeLog.md
  3. 24
      README.md
  4. 2
      Setup.hs
  5. 257
      Yggdrasil/Examples/SecureChannel.agda
  6. 33
      Yggdrasil/List.agda
  7. 116
      Yggdrasil/Probability.agda
  8. 96
      Yggdrasil/Rational.agda
  9. 156
      Yggdrasil/Security.agda
  10. 375
      Yggdrasil/World.agda
  11. 2
      default.nix
  12. 7
      hydra.nix
  13. 107
      src/Yggdrasil/Adversarial.hs
  14. 98
      src/Yggdrasil/Distribution.hs
  15. 135
      src/Yggdrasil/ExecutionModel.hs
  16. 110
      src/Yggdrasil/Functionalities.hs
  17. 73
      src/Yggdrasil/HList.hs
  18. 105
      src/Yggdrasil/MetaProtocol.hs
  19. 83
      src/Yggdrasil/Nat.hs
  20. 65
      stack.yaml
  21. 35
      tests/ExecTests.hs
  22. 49
      tests/FunctTests.hs
  23. 11
      tests/Spec.hs
  24. 2
      yggdrasil.agda-lib
  25. 53
      yggdrasil.cabal
  26. BIN
      yggdrasil.jpg
  27. 13
      yggdrasil.nix

2
.gitignore

@ -0,0 +1,2 @@
/dist
/.stack-work

8
ChangeLog.md

@ -0,0 +1,8 @@
# Revision history for yggdrasil
## 0.1.0.0 -- 2018-09-10
* Provide an UC-like, strictly typed execution model.
* Provide randomness distributions.
* Provide a typed model for arbitrary adversaries.
* Implement random oracles, crs, and signatures.

24
README.md

@ -0,0 +1,24 @@
# Yggdrasil
![Yggdrasil - The Mundane Tree](https://git.drwx.org/phd/yggdrasil/raw/branch/master/yggdrasil.jpg)
Yggdrasil is a UC-based system for modelling security protocols.
## Not Asked Questions
Q: Why Haskell?
A: In an environment where things behave adversarially, having a very powerful
type system is useful to reason about what things *can* do. Further, pure,
functional languages allow restricting the communication between components
that should not communicate, and lend themselves more easily to formal
reasoning. Eventually the goal is to formally prove statements about execution
as well, but we are a long way off.
Q: Why AGPL?
A: AGPL is actually less strong than I'd like here, but stronger would be
unreasonable. I usually prefer permissive licenses, however it is crucial for
security protocols - and their implementation - to be available for public
scrutiny. If the use of AGPL results in one more protocol being made public, I
consider that a gain.

2
Setup.hs

@ -0,0 +1,2 @@
import Distribution.Simple
main = defaultMain

257
Yggdrasil/Examples/SecureChannel.agda

@ -1,257 +0,0 @@
module Yggdrasil.Examples.SecureChannel where
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 (_*_; zero; suc)
open import Data.Empty using (⊥-elim)
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 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 (there here) tt >>= λ
{ nothing → return nothing
; (just c) → call↓ here here c
}) ∷
ncall M ⊤ (λ m → let
doSend = λ pk m → call↓ (there here) here ⟨ pk , m ⟩ >>= (λ
{ nothing → abort -- The public key we set was refused!
; (just c) → call↓ (there here) (there here) c
})
in read >>= λ
{ nothing → call↓ (there (there here)) here tt >>= (λ 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) → (m?= : M → M → Bool) →
πᵢ-SecureChannel M L l ≃ πᵣ-SecureChannel M C PK L l pk?= c?=
secure {ℓ} M C PK L l pk?= c?= m?= = record
{ gas-map = _* 2
; simulator = S-SecureChannel M C PK L l pk?= c?=
; 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↓ here tt) ⟨
⟨ stnode (just m) [] , lift true ⟩ ,
stnode (just pk′) (
stnode (just ⟨ pk , log ⟩) [] ∷
stnode (just c) [] ∷
[])
⟩ inv → ⟨ ? , ⟨ ? , ? ⟩ ⟩
; g σ O (call↓ here tt) ⟨
⟨ stnode nothing [] , lift false ⟩ ,
stnode nothing (
stnode nothing [] ∷
stnode nothing [] ∷
[])
⟩ inv → ⟨ ? , ⟨ ? , ? ⟩ ⟩
; zero σ O (call↓ (there here) m) ⟨
⟨ stnode (just m′) [] , lift true ⟩ ,
stnode (just pk′) (
stnode (just ⟨ pk , log ⟩) [] ∷
stnode (just c) [] ∷
[])
⟩ inv → ⟨ ? , ⟨ ? , ? ⟩ ⟩
; (suc g) σ O (call↓ (there here) m) ⟨
⟨ stnode (just m′) [] , lift true ⟩ ,
stnode (just pk′) (
stnode (just ⟨ pk , log ⟩) [] ∷
stnode (just c) [] ∷
[])
⟩ inv → ⟨ ? , ⟨ ? , ? ⟩ ⟩
; g σ O (call↓ (there here) m) ⟨
⟨ stnode nothing [] , lift false ⟩ ,
stnode nothing (
stnode nothing [] ∷
stnode nothing [] ∷
[])
⟩ inv → ⟨ ? , ⟨ ? , ? ⟩ ⟩
; g σ O _ ⟨ ⟨ stnode nothing [] , lift true ⟩ , _ ⟩ inv → ⊥-elim ?
; g σ O _ ⟨
⟨ stnode _ [] , lift true ⟩ ,
stnode nothing _
⟩ ()
; g σ O _ ⟨
⟨ stnode _ [] , lift true ⟩ ,
stnode _ (stnode nothing [] ∷ _)
⟩ ()
; g σ O _ ⟨
⟨ stnode _ [] , lift true ⟩ ,
stnode _ (
stnode _ [] ∷
stnode nothing [] ∷
[])
⟩ ()
; g σ O _ ⟨ ⟨ stnode (just _) [] , lift false ⟩ , _ ⟩ inv → ⊥-elim ?
; g σ O _ ⟨
⟨ stnode _ [] , lift false ⟩ ,
stnode (just _) _
⟩ ()
; g σ O _ ⟨
⟨ stnode _ [] , lift false ⟩ ,
stnode _ (stnode (just _) [] ∷ _)
⟩ ()
; g σ O _ ⟨
⟨ stnode _ [] , lift false ⟩ ,
stnode _ (
stnode _ [] ∷
stnode (just _) [] ∷
[])
⟩ ()
; g σ O (call↓ (there (there ())) x) Σ inv
; g σ O (call↯ () here x) Σ inv
; g σ O (call↯ () (there here here) x) Σ inv
; g σ O (call↯ () (there (there here) here) x) Σ inv
; g σ O (call↯ ∈Γ (there (there (there ())) here) x) Σ inv
; g σ O (call↯ ∈Γ (there here (there () Γ⊑)) x) Σ inv
; g σ O (call↯ ∈Γ (there (there here) (there () Γ⊑)) x) Σ inv
; g σ O (call↯ ∈Γ (there (there (there ())) (there x₂ Γ⊑)) x) Σ inv
}
}

33
Yggdrasil/List.agda

@ -1,33 +0,0 @@
module Yggdrasil.List where
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 ⟩ ⟩

116
Yggdrasil/Probability.agda

@ -1,116 +0,0 @@
module Yggdrasil.Probability where
open import Agda.Builtin.FromNat using (Number)
import Data.Nat.Literals as ℕLit
import Data.Rational.Literals as ℚLit
import Data.Integer.Literals as ℤLit
open import Data.List using (List; _∷_; []; map; filter; length; foldr)
open import Data.Fin using (Fin; zero; suc)
open import Data.Integer using (ℤ; +_; _-_) renaming (_*_ to _ℤ*_)
open import Data.Nat using (ℕ; zero; suc; s≤s) renaming (_*_ to _ℕ*_; _≤?_ to _ℕ≤?_; _≤_ to _ℕ≤_)
open import Data.Nat.Literals
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; lower; _⊔_) renaming (suc to lsuc; lift to llift)
open import Yggdrasil.List using (_∈_; with-proof)
import Yggdrasil.Rational as ℚ
instance
ℕnumber : Number ℕ
ℕnumber = ℕLit.number
ℤnumber : Number ℤ
ℤnumber = ℤLit.number
ℚnumber : Number ℚ
ℚnumber = ℚLit.number
case : ℚ → ℚ → ℚ → ℚ
case Pr[A] Pr[B∣A] Pr[B∣¬A] = Pr[A] ℚ.* Pr[B∣A] ℚ.+ (1 ℚ.- Pr[A]) ℚ.* Pr[B∣¬A]
sum : List ℚ → ℚ
sum = foldr (ℚ._+_) 0
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)
length-all-fin : (n : ℕ) → length (all-fin n) ≡ n
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 llift (all-fin (suc (suc n)))))
data Dist {ℓ : Level} : Set ℓ → Set (lsuc ℓ) where
pure : ∀ {A : Set ℓ} → A → Dist A
sample : ∀ {n : ℕ} → Dist (PrFin {ℓ} n)
_>>=_ : ∀ {A B : Set ℓ} → Dist A → (A → Dist B) → Dist B
_>>=′_ : ∀ {ℓ A B} → Dist {ℓ} A → (A → Dist {ℓ} B) → Dist {ℓ} B
pure x >>=′ y = y x
sample >>=′ y = sample >>= y
(a >>= b) >>=′ y = (a >>= b) >>= y
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} >>=
(pure ∘ llift ∘ llift ∘ lower)
lift {ℓ₂ = ℓ} (D >>= f) = lift {ℓ₂ = ℓ} D >>= (lift ∘ f ∘ lower)
≡⇒≤ : {a b : ℕ} → a ≡ b → a ℕ≤ b
≡⇒≤ refl = ≤-refl
data Pr[_[_]]≡_ {ℓ : Level} : {A : Set ℓ} → (P : A → Set ℓ) → Dist A →
ℚ → Set (lsuc ℓ) where
pure-zero : {A : Set ℓ} {P : A → Set ℓ} → (x : A) → ¬ (P x) →
Pr[ P [ pure x ]]≡ 0
pure-one : {A : Set ℓ} {P : A → Set ℓ} → (x : A) → P x →
Pr[ P [ pure x ]]≡ 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₃ : ℚ} →
Pr[ P₁ [ D ]]≡ p₁ →
((x : A) → P₁ x → Pr[ P₂ [ f x ]]≡ p₂) →
((x : A) → ¬ (P₁ x) → Pr[ P₂ [ f x ]]≡ p₃) →
Pr[ P₂ [ D >>= f ]]≡ (case p₁ p₂ p₃)
record _≈[_]≈_ {ℓ : Level} {A : Set ℓ} (d₁ : Dist A) (ε : ℚ) (d₂ : Dist A) : Set (lsuc ℓ) where
field
elements : List A
pr₁ : (x : A) → x ∈ elements → ∃[ p ] Pr[ _≡ x [ d₁ ]]≡ p
pr₂ : (x : A) → x ∈ elements → ∃[ p ] Pr[ _≡ x [ d₂ ]]≡ p
elements-complete-d₁ : sum (map (λ{
⟨ x , x∈xs ⟩ → proj₁ (pr₁ x x∈xs)
}) (with-proof elements)) ≡ 1
elements-complete-d₂ : sum (map (λ{
⟨ x , x∈xs ⟩ → proj₁ (pr₂ x x∈xs)
}) (with-proof elements)) ≡ 1
ε-error : sum (map (λ{
⟨ x , x∈xs ⟩ → ℚ.∣ proj₁ (pr₁ x x∈xs) ℚ.- proj₁ (pr₂ x x∈xs) ∣
}) (with-proof elements)) ℚ≤ ε
_≃_ : {ℓ : Level} {A : Set ℓ} (d₁ d₂ : Dist A) → Set (lsuc ℓ)
d₁ ≃ d₂ = d₁ ≈[ 0 ]≈ d₂
postulate
≈-trans : {ℓ : Level} {A : Set ℓ} {d₁ d₂ d₃ : Dist A} {ε₁ ε₂ : ℚ} →
d₁ ≈[ ε₁ ]≈ d₂ → d₂ ≈[ ε₂ ]≈ d₃ → d₁ ≈[ ε₁ ℚ.+ ε₂ ]≈ d₃
≈-sym : {ℓ : Level} {A : Set ℓ} {d₁ d₂ : Dist A} {ε : ℚ} → d₁ ≈[ ε ]≈ d₂ →
d₂ ≈[ ε ]≈ d₁
≈-refl : {ℓ : Level} {A : Set ℓ} {d : Dist A} → d ≃ d

96
Yggdrasil/Rational.agda

@ -1,96 +0,0 @@
module Yggdrasil.Rational where
open import Data.Bool using (true; false; T)
open import Data.Integer as ℤ using (ℤ; +_; -[1+_])
open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Data.Nat.GCD as GCD using (GCD; gcd)
open import Data.Nat.Divisibility using (_∣_; divides)
open import Data.Nat.Coprimality using (Coprime; coprime?; gcd-coprime; Bézout-coprime)
open import Data.Nat.Properties using (*-comm; *-assoc)
open import Data.Product renaming (_,_ to ⟨_,_⟩)
open import Data.Rational using (ℚ) renaming (_÷_ to _÷†_)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Sign using (Sign) renaming (+ to s+; - to s-)
open import Relation.Nullary using (yes; no; ¬_)
open import Relation.Nullary.Decidable using (True; False; ⌊_⌋; fromWitness; fromWitnessFalse)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; _≢_; refl; subst₂; sym; cong; trans)
open Eq.≡-Reasoning using (_≡⟨_⟩_; _∎; begin_)
open ℚ
infixl 6 _+_ _-_
infixl 7 _*_ _÷_
private
1+≢*0 : ∀ x y → suc x ≢ y ℕ.* 0
1+≢*0 x zero ()
1+≢*0 x (suc y) = 1+≢*0 x y
1≢0 : ∀ {n} → suc n ≢ zero
1≢0 ()
simp : ∀ x y-1 → ℚ
simp x y-1 with GCD.Bézout.lemma x (suc y-1)
... | GCD.Bézout.result 0 (GCD.is ⟨ _ , divides y′ y-eq ⟩ _) _ =
⊥-elim (1+≢*0 y-1 y′ y-eq)
... | GCD.Bézout.result (suc d-1)
(GCD.is ⟨ divides x′ x-eq , divides y′ y-eq ⟩ _) bézout =
_÷†_ (+ x′) y′ {fromWitness (λ {i} → Bézout-coprime bézout′)}
{fromWitnessFalse y′≢0}
where
y = suc y-1
d = suc d-1
bézout′ : GCD.Bézout.Identity d (x′ ℕ.* d) (y′ ℕ.* d)
bézout′ = subst₂ (GCD.Bézout.Identity d) x-eq y-eq bézout
y′≢0 : y′ ≢ 0
y′≢0 y′≡0 = ⊥-elim (1≢0 (trans y-eq (cong (ℕ._* d) y′≡0)))
-_ : ℚ → ℚ
- q = _÷†_ (ℤ.- numerator q) (suc (denominator-1 q))
{fromWitness (λ{ {i} ⟨ i∣n , i∣d ⟩ → coprime q ⟨ ∣-abs⇒∣abs i (numerator q) i∣n , i∣d ⟩})}
where
-abs≡abs : ∀ i → ℤ.∣ ℤ.- i ∣ ≡ ℤ.∣ i ∣
-abs≡abs (+ zero) = refl
-abs≡abs (+ (suc n)) = refl
-abs≡abs -[1+ n ] = refl
∣-abs⇒∣abs : ∀ i j → i ∣ ℤ.∣ ℤ.- j ∣ → i ∣ ℤ.∣ j ∣
∣-abs⇒∣abs i j (divides k j=k*i) = divides k (sym (begin
k ℕ.* i ≡⟨ sym j=k*i ⟩
ℤ.∣ ℤ.- j ∣ ≡⟨ -abs≡abs j ⟩
ℤ.∣ j ∣ ∎))
_÷_ : ℤ → (d : ℕ) → {d≢0 : False (d ℕ.≟ 0)} → ℚ
_÷_ n zero {}
(+ n) ÷ (suc d-1) = simp n d-1
(-[1+ n-1 ]) ÷ (suc d-1) = - simp (suc n-1) d-1
∣_∣ : ℚ → ℚ
∣ q ∣ = _÷†_ (+ ℤ.∣ numerator q ∣) (suc (denominator-1 q)) {isCoprime q}
_+_ : ℚ → ℚ → ℚ
a + b = let
n-a = numerator a
d-a = suc (denominator-1 a)
n-b = numerator b
d-b = suc (denominator-1 b)
n-c = n-a ℤ.* (+ d-b) ℤ.+ n-b ℤ.* (+ d-a)
d-c = d-a ℕ.* d-b
in n-c ÷ d-c
_*_ : ℚ → ℚ → ℚ
a * b = let
n-a = numerator a
d-a = suc (denominator-1 a)
n-b = numerator b
d-b = suc (denominator-1 b)
n-c = n-a ℤ.* n-b
d-c = d-a ℕ.* d-b
in n-c ÷ d-c
_-_ : ℚ → ℚ → ℚ
a - b = a + (- b)

156
Yggdrasil/Security.agda

@ -1,156 +0,0 @@
module Yggdrasil.Security where
open import Agda.Builtin.FromNat using (Number)
import Data.Nat.Literals as ℕLit
import Data.Rational.Literals as ℚLit
import Data.Integer.Literals as ℤLit
open import Data.Bool using (Bool; true; false)
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; 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 (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; 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
open Strategy
instance
ℕnumber : Number ℕ
ℕnumber = ℕLit.number
ℤnumber : Number ℤ
ℤnumber = ℤLit.number
ℚnumber : Number ℚ
ℚnumber = ℚLit.number
data Guess {ℓ : Level} : Set ℓ where
real? ideal? : Guess
data Action↯ {ℓ : Level} (σ : Set ℓ) (Γᵢ Γᵣ : WorldType ℓ)
{hon-≡ : map weaken (hon Γᵢ) ≡ map weaken (hon Γᵣ)} : Set ℓ →
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
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↯ 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.Γ πᵣ) → ℕ →
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⊤ (σ × Simulator.state S) (World.Γ πᵢ) A
private
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
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 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
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 _≃_ {ℓ : Level} (πᵢ πᵣ : World ℓ) :
Set (lsuc (lsuc ℓ)) where
Γᵣ : WorldType ℓ
Γᵣ = World.Γ πᵣ
Γᵢ : WorldType ℓ
Γᵢ = World.Γ πᵢ
Σᵣ : WorldState Γᵣ
Σᵣ = World.Σ πᵣ
Σᵢ : WorldState Γᵢ
Σᵢ = World.Σ πᵢ
field
gas-map : ℕ → ℕ
simulator : Simulator πᵢ πᵣ
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)

375
Yggdrasil/World.agda

@ -1,375 +0,0 @@
module Yggdrasil.World where
open import Data.Bool using (Bool; T)
open import Data.List using (List; _∷_; []; map; _++_; length; lookup)
open import Data.List.Any using (here; there)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.Fin using (Fin)
open import Data.Maybe using (Maybe; just; nothing) renaming (map to mmap)
open import Data.Nat using (ℕ; suc)
open import Data.Product as Π using (_×_; ∃; ∃-syntax; proj₁; proj₂; map₂) renaming (_,_ to ⟨_,_⟩)
open import Data.String using (String)
import Data.String.Unsafe as S
open import Function using (id)
open import Level using (Level; _⊔_; Lift) renaming (suc to lsuc; zero to lzero)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
open import Relation.Nullary using (Dec; yes; no)
-- Auto-lifted variant of ⊤.
data ⊤ {ℓ : Level} : Set ℓ where
tt : ⊤
Table : ∀ {ℓ} → Set ℓ → Set ℓ
Table A = List (String × A)
_∪_ : ∀ {ℓ A} → Table {ℓ} A → Table {ℓ} A → Table {ℓ} A
_∪_ = _++_
module Weak where
record WeakState {ℓ : Level} : Set (lsuc ℓ)
record WeakTransition {ℓ : Level} (n : ℕ) : Set (lsuc ℓ) where
inductive
field
A : Set ℓ
B : A → Set ℓ
Σ : A → Fin n
record WeakState {ℓ} where
inductive
field
states : List (Set ℓ)
current : Fin (length states)
δ↑ : Fin (length states) → Table (WeakTransition {ℓ} (length states))
δ↓ : Fin (length states) → Table (WeakTransition {ℓ} (length states))
open Weak using (WeakState; WeakTransition)
open WeakState
record State {ℓ : Level} (Σʷ : WeakState {ℓ}) : Set (lsuc ℓ)
data Action {ℓ : Level} : {Σʷ₁ Σʷ₂ : WeakState {ℓ}} →
(Σ₁ : Fin (length (states Σʷ₁))) →
(Σ₂ : State Σʷ₂) → Set ℓ → Set (lsuc ℓ)
Transition↑ : {ℓ : Level} {Σʷ : WeakState {ℓ}} →
(Σ₁ : Fin (length (states Σʷ))) → WeakTransition {ℓ} (length (states Σʷ)) →
Set (lsuc ℓ)
Transition↑ {Σʷ = Σʷ} Σ₁ T = (x : A T) → Π.Σ
(State (record Σʷ { current = Σ T x }))
(λ Σ₂ → Action {Σʷ₁ = Σʷ} Σ₁ Σ₂ (B T x))
where open WeakTransition using (A; B; Σ)
Transition↓ : {ℓ : Level} {Σʷ : WeakState {ℓ}} →
WeakTransition {ℓ} (length (states Σʷ)) → Set ℓ
Transition↓ {Σʷ = Σʷ} T = (x : A T) → Π.Σ (Fin (length (states Σʷ)))
(λ n → lookup (states Σʷ) n)
where open WeakTransition using (A; Σ)
--data Transitions↑ {ℓ : Level} (Σ : Π.Σ (Set ℓ) id) :
-- Table (WeakTransition {ℓ}) → Set (lsuc ℓ) where
-- [] : Transitions↑ Σ []
-- _∷_ : ∀ {Σʷ T Ts name} → Transition↑ {Σʷ = Σʷ} Σ T → Transitions↑ Σ Ts →
-- Transitions↑ Σ (⟨ name , T ⟩ ∷ Ts)
--
--data Transitions↓ {ℓ : Level} :
-- Table (WeakTransition {ℓ}) → Set (lsuc ℓ) where
-- [] : Transitions↓ []
-- _∷_ : ∀ {T Ts name} → Transition↓ T → Transitions↓ Ts →
-- Transitions↓ (⟨ name , T ⟩ ∷ Ts)
--
record State {ℓ} Σʷ where
open WeakState
field
n : Fin (length (states Σʷ))
σ : lookup (states Σʷ) n
-- δ↑ : Transitions↑ ⟨ Σ , σ ⟩ (WeakState.δ↑ Σʷ)
-- δ↓ : Transitions↓ (WeakState.δ↓ Σʷ)
--
--⌊_⌋ : ∀ {ℓ Σʷ} → (Σ : State {ℓ} Σʷ) → Π.Σ (Set ℓ) id
--⌊ Σ ⌋ = ⟨ State.Σ Σ , State.σ Σ ⟩
--
--lookup↓ : ∀ {ℓ xs δ} → δ ∈ xs → (Ts : Transitions↓ {ℓ} xs) → Transition↓ (proj₂ δ)
--lookup↓ (here refl) (x ∷ _) = x
--lookup↓ (there ∈xs) (_ ∷ xs) = lookup↓ ∈xs xs
--
--∈↓ʷ⇒∈↓ : ∀ {ℓ Σʷ δ} {Σ : State Σʷ} → δ ∈ (WeakState.δ↓ Σʷ) →
-- Transition↓ {ℓ} (proj₂ δ)
--∈↓ʷ⇒∈↓ {Σ = Σ} δ∈ = lookup↓ δ∈ (State.δ↓ Σ)
----
----open Weak
----
--
data Action {ℓ} where
-- get : ∀ {Σʷ Σ} → Action {ℓ} {Σʷ} {Σʷ} ⌊ Σ ⌋ Σ (State.Σ Σ)
-- set : ∀ {Σʷ₁ Σʷ₂ Σ₁ Σ₂} → State.Σ Σ₂ → Action {ℓ} {Σʷ₁} {Σʷ₂} Σ₁ Σ₂ ⊤
-- call : ∀ {Σʷ δ} {Σ : State Σʷ} → (δ∈ : δ ∈ WeakState.δ↓ Σʷ) →
-- (x : WeakTransition.A (proj₂ δ)) →
-- Action {ℓ} {Σʷ} {WeakTransition.Σ (proj₂ δ) x} ⌊ Σ ⌋
-- (∈↓ʷ⇒∈↓ {Σ = Σ} δ∈ x)
-- (WeakTransition.B (proj₂ δ) x)
-- return : ∀ {Σʷ Σ A} → Action {ℓ} {Σʷ} {Σʷ} ⌊ Σ ⌋ Σ A
-- _>>=_ : ∀ {Σʷ₁ Σʷ₂ Σʷ₃ Σ₁ Σ₂ Σ₃ A B} →
-- Action {ℓ} {Σʷ₁} {Σʷ₂} (⌊_⌋ {Σʷ = Σʷ₁} Σ₁) Σ₂ A →
-- (A → Action {ℓ} {Σʷ₂} {Σʷ₃} ⌊ Σ₂ ⌋ Σ₃ B) →
-- Action {ℓ} {Σʷ₁} {Σʷ₃} ⌊ Σ₁ ⌋ Σ₃ B
--
--record ParallelComposable {ℓ₁ ℓ₂ : Level} (A : Set ℓ₁) {P : A → A → Set ℓ₂} :
-- Set (ℓ₁ ⊔ ℓ₂) where
-- field
-- _||_ : A → A → A
-- _∘_ : (x : A) → (y : A) → {_ : P x y} → A
--
--data InterfaceMatches {ℓ : Level} : ℕ → (Σʷ₁ Σʷ₂ : WeakState {ℓ}) → Set (lsuc ℓ) where
-- unreachable : ∀ {Σʷ₁ Σʷ₂} → InterfaceMatches 0 Σʷ₁ Σʷ₂
-- match : ∀ {n Σʷ₁ Σʷ₂ δ₁} →
-- -- For each interface in the outgoing to Σʷ₁
-- δ₁ ∈ WeakState.δ↓ Σʷ₁ →
-- Π.Σ (String × WeakTransition {ℓ}) (λ δ₂ →
-- -- A corresponding interface exists in the incoming of Σʷ₂
-- (δ₂ ∈ WeakState.δ↑ Σʷ₂) ×
-- -- With the same name
-- (proj₁ δ₁ ≡ proj₁ δ₂) ×
-- -- The same input type
-- Π.Σ (WeakTransition.A (proj₂ δ₁) ≡ WeakTransition.A (proj₂ δ₂)) (λ{
-- refl → (x : WeakTransition.A (proj₂ δ₁)) →
-- -- The same output type
-- WeakTransition.B (proj₂ δ₁) x ≡ WeakTransition.B (proj₂ δ₂) x ×
-- -- And preserving the fact that interfaces keep matching.
-- InterfaceMatches n (WeakTransition.Σ (proj₂ δ₁) x)
-- (WeakTransition.Σ (proj₂ δ₂) x)
-- })) →
-- InterfaceMatches (suc n) Σʷ₁ Σʷ₂
--
--instance
-- WeakStateParallelComposable : ∀ {ℓ : Level} → ParallelComposable {lsuc ℓ} (WeakState {ℓ}) {λ Σʷ₁ Σʷ₂ → ∀ n → InterfaceMatches n Σʷ₁ Σʷ₂}
-- WeakStateParallelComposable = record
-- { _||_ = _||_
-- ; _∘_ = λ Σʷ₁ Σʷ₂ → record
-- { δ↑ = ?
-- ; δ↓ = ?
-- }
-- }
-- where
-- open WeakState
-- open WeakTransition
-- invariant₁ : ∀ {ℓ} → WeakState {ℓ} → WeakTransition {ℓ} → WeakTransition {ℓ}
-- invariant₂ : ∀ {ℓ} → WeakState {ℓ} → WeakTransition {ℓ} → WeakTransition {ℓ}
-- _||_ : ∀ {ℓ} → WeakState {ℓ} → WeakState {ℓ} → WeakState {ℓ}
-- Σʷ₁ || Σʷ₂ = record
-- { δ↑ = map (map₂ (invariant₂ Σʷ₂)) (δ↑ Σʷ₁) ∪ map (map₂ (invariant₁ Σʷ₁)) (δ↑ Σʷ₂)
-- ; δ↓ = map (map₂ (invariant₂ Σʷ₂)) (δ↓ Σʷ₁) ∪ map (map₂ (invariant₁ Σʷ₁)) (δ↓ Σʷ₂)
-- }
-- invariant₁ Σʷ δ = record { A = A δ ; B = B δ ; Σ = λ x → Σʷ || Σ δ x }
-- invariant₂ Σʷ δ = record { A = A δ ; B = B δ ; Σ = λ x → Σ δ x || Σʷ }
-- ActionParallelComposable : ∀ {ℓ : Level} {Σʷ : WeakState {ℓ}} → (Σ : State Σʷ) → (A : Set ℓ) → ParallelComposable {ℓ} {P = InterfaceMatches
--ParallelComposable
-- 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₁; proj₂) renaming (_,_ to ⟨_,_⟩)
-- open import Data.Sum using (_⊎_; inj₁; inj₂)
-- open import Function using (_∘_)
-- open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
-- 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 : ⊤
--
-- data ⊥ {ℓ : Level} : Set ℓ where
--
-- T : ∀ {ℓ} → Bool → Set ℓ
-- T true = ⊤
-- T false = ⊥
--
-- 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} (N : Node ℓ) : 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 ℓ)
--
-- record Node ℓ where
-- inductive
-- constructor mknode
-- field
-- state : Set ℓ
-- chld : List (WorldType ℓ)
-- qry : List (Query ℓ)
--
-- open Node
--
--
-- record Call (ℓ : Level) (N : Node ℓ) : Set (lsuc ℓ) where
-- inductive
-- constructor call
-- field
-- A : Set ℓ
-- B : A → Set ℓ
-- δ : (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)
-- hon : List (Call ℓ node)
--
-- open WorldType
--
-- data _⊑_ {ℓ : Level} : (Γ₁ Γ₂ : WorldType ℓ) → Set (lsuc ℓ) where
-- here : ∀ {Γ} → Γ ⊑ Γ
-- there : ∀ {Γ₁ Γ₂ Γ₃} → Γ₂ ∈ chld (node Γ₃) → Γ₁ ⊑ Γ₂ → Γ₁ ⊑ Γ₃
--
-- ⊑-trans : ∀ {ℓ} {Γ₁ Γ₂ Γ₃ : WorldType ℓ} → Γ₁ ⊑ Γ₂ → Γ₂ ⊑ Γ₃ → Γ₁ ⊑ Γ₃
-- ⊑-trans ⊑Γ here = ⊑Γ
-- ⊑-trans ⊑Γ (there Γ′∈ ⊑Γ′) = there Γ′∈ (⊑-trans ⊑Γ ⊑Γ′)
--
-- ⊑-right : ∀ {ℓ} {Γ₁ Γ₂ Γ₃ : WorldType ℓ} → Γ₂ ⊑ Γ₃ → Γ₁ ∈ chld (node Γ₂) → Γ₁ ⊑ Γ₃
-- ⊑-right Γ⊑ ∈Γ = ⊑-trans (there ∈Γ here) Γ⊑
--
-- 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 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)
--
-- data WorldState {ℓ} Γ where
-- stnode : state (node Γ) → WorldStates (chld (node Γ)) → WorldState Γ
--
-- record World (ℓ : Level) : Set (lsuc ℓ) where
-- field
-- Γ : WorldType ℓ
-- Σ : WorldState Γ
--
-- data _∈↑_ {ℓ : Level} (q : Query ℓ) (Γ : WorldType ℓ) : Set (lsuc ℓ) where
-- path : ∀ {Γ′} → Γ′ ⊑ Γ → q ∈ qry (node Γ′) → q ∈↑ Γ
--
-- 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 ℓ) {S : Set ℓ} : Set (lsuc ℓ) where
-- constructor strat
-- field
-- state : S
-- init : Action⊤ S Γ A
-- oracle : Oracle S Γ
--
--
--
-- get : ∀ {ℓ Γ₁ Γ₂} → Γ₁ ⊑ Γ₂ → WorldState {ℓ} Γ₂ → state (node Γ₁)
-- get here (stnode Σ _) = Σ
-- get (there Γ′∈ ⊑Γ) (stnode _ Σs) = get ⊑Γ (lookup Γ′∈ Σs)
-- where
-- lookup : ∀ {Γ Γs} → Γ ∈ Γs → WorldStates Γs → WorldState Γ
-- lookup here (Σ ∷ _) = Σ
-- lookup (there Γ′∈) (_ ∷ Σs) = lookup Γ′∈ Σs
--
-- set : ∀ {ℓ Γ₁ Γ₂} → Γ₁ ⊑ Γ₂ → WorldState {ℓ} Γ₂ → state (node Γ₁) →
-- WorldState {ℓ} Γ₂
-- set here (stnode Σ Σs) Σ′ = stnode Σ′ Σs
-- set (there Γ′∈ ⊑Γ) (stnode Σ Σs) Σ′ = stnode Σ (set′ Γ′∈ ⊑Γ Σs Σ′)
-- where
-- set′ : ∀ {Γ₁ Γ₂ Γs} → Γ₂ ∈ Γs → Γ₁ ⊑ Γ₂ → WorldStates Γs →
-- state (node Γ₁) → WorldStates Γs
-- set′ here ⊑Γ (Σ ∷ Σs) Σ′ = set ⊑Γ Σ Σ′ ∷ Σs
-- set′ (there Γ∈) ⊑Γ (Σ ∷ Σs) Σ′ = Σ ∷ set′ Γ∈ ⊑Γ Σs Σ′
--
-- data Result {ℓ : Level} (A : Set ℓ) : Set ℓ where
-- abort : Result A
-- out-of-gas : Result A
-- result : A → Result A
--
-- rmap : ∀ {ℓ A B} → (A → B) → Result {ℓ} A → Result {ℓ} B
-- rmap _ abort = abort
-- rmap _ out-of-gas = out-of-gas
-- rmap f (result x) = result (f x)
--
-- exec : ∀ {ℓ S Γ A} → Strategy {ℓ} Γ A {S} → WorldState {ℓ} Γ → ℕ →
-- Dist (Result (Lift (lsuc ℓ) A))
-- 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 S α O) Σ g = (exec⊤ O α ⟨ S , Σ ⟩ g) >>=′ (pure ∘ rmap (llift ∘ proj₁))
--
-- 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) Σ 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↑ 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) Σ ⊑Γ 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 ;
-- out-of-gas → pure out-of-gas }

2
default.nix

@ -0,0 +1,2 @@
{ pkgs ? import <nixpkgs> { } }:
pkgs.haskellPackages.callPackage ./yggdrasil.nix { }

7
hydra.nix

@ -0,0 +1,7 @@
{ nixpkgs ? <nixpkgs> }:
let
pkgs = import nixpkgs { };
in {
yggdrasil = import ./default.nix { inherit pkgs; };
}

107
src/Yggdrasil/Adversarial.hs

@ -0,0 +1,107 @@
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
-- | Exposes type for reasoning about adversaries. Generally speaking, a
-- 'Functionality' may request interfaces from an 'Adversary', which need to be
-- supplied for it to run. The adversary also exposes some power to the
-- environment to arbitrarily control these interfaces. Functionalities should
-- be aware that the adversary may respond with anything correctly typed, and
-- is explicitly permitted to returning 'Nothing'. 'WithAdversary'' provides
-- an interface to repair unacceptable responses before the functionality
-- itself is called.
module Yggdrasil.Adversarial
( Adversary
, MaybeMap
, WithAdversary
, WithAdversary'(..)
, NoAdversary(..)
, DummyAdversary(..)
, CreateAdversarial(..)
) where
import Control.Arrow (second)
import Control.Monad.Trans.Class (lift)
import Yggdrasil.ExecutionModel (Action (Create),
Functionality (Functionality),
InterfaceMap, Interfaces, Operation,
Operations)
import Yggdrasil.HList (type (+|+), HList ((:::), Nil),
HSplit (hsplit))
-- | Maps a list of @'(in, out)@ type tuples to @'(in, 'Maybe' out)@.
type family MaybeMap (bs :: [(*, *)]) = (ys :: [(*, *)]) | ys -> bs where
MaybeMap '[] = '[]
MaybeMap ('( a, b) ': xs) = '( a, Maybe b) ': MaybeMap xs
-- | Allows construction of @[email protected] given a list of interfaces @[email protected] from the
-- adversary. The adversarial interfaces return 'Maybe's on all interfaces.
newtype WithAdversary s (ts :: [(*, *)]) b =
WithAdversary (HList (Interfaces s (MaybeMap ts)) -> b)
-- | Allows construction of a 'Functionality' with state @[email protected] and interface @[email protected]
-- whjen given a list of interfaces @[email protected] from the adversary. The adversarial
-- interface is corrected, by passing it through a filter ensuring valid
-- responses.
data WithAdversary' s c (as :: [(*, *)]) (bs :: [(*, *)]) =
WithAdversary' (HList (Interfaces s (MaybeMap as)) -> HList (Operations s c as))
(HList (Operations s c as) -> Functionality s c bs)
-- | An adversary is a functionality that exposes some interfaces to the
-- environment, and some interfaces returning 'Maybe's to some other party.
type Adversary s c as bs = Functionality s c (as +|+ MaybeMap bs)
-- | The empty adversary returns 'Nothing'.
class NoAdversary s (bs :: [(*, *)]) where
nullOperations :: HList (Operations s () (MaybeMap bs))
noAdversary :: Adversary s () '[] bs
noAdversary = Functionality () (nullOperations @s @bs)
instance NoAdversary s '[] where
nullOperations = Nil
instance NoAdversary s xs => NoAdversary s ('( a, b) ': xs) where
nullOperations = (\_ -> return Nothing) ::: nullOperations @s @xs
-- | A dummy adversary executes the interfaces the environments hands it.
class DummyAdversary s (bs :: [(*, *)]) where
operations ::
HList (Interfaces s (MaybeMap bs))
-> HList (Operations s () (MaybeMap bs))
dummyAdversary ::
HList (Interfaces s (MaybeMap bs)) -> Adversary s () '[] bs
dummyAdversary = Functionality () . operations @s @bs
instance DummyAdversary s '[] where
operations _ = Nil
instance DummyAdversary s bs => DummyAdversary s ('( a, b) ': bs) where
operations (b ::: bs) =
(lift . b :: Operation s () a (Maybe b)) :::
operations @s @bs bs
-- | Creates an adversarial functionality given a suitable adversary.
class CreateAdversarial s c as bs adv b where
createAdversarial ::
( HSplit (Interfaces s (as +|+ MaybeMap bs)) (Interfaces s as) (Interfaces s (MaybeMap bs))
, InterfaceMap s c (as +|+ MaybeMap bs)
)
=> Adversary s c as bs
-> adv
-> Action s (HList (Interfaces s as), b)
instance CreateAdversarial s c as bs (WithAdversary s bs b) b where
createAdversarial adv (WithAdversary f) = second f . hsplit <$> Create adv
instance CreateAdversarial s c as bs (WithAdversary' s c bs cs) (Functionality s c cs) where
createAdversarial adv (WithAdversary' g f) =
(\(a, b) -> (a, f (g b))) . hsplit <$> Create adv

98
src/Yggdrasil/Distribution.hs

@ -0,0 +1,98 @@
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
-- | Provides primitives for high-level cryptographic sampling.
module Yggdrasil.Distribution
( Distribution
, DistributionT(DistributionT, runDistT)
, Sampler(..)
, liftDistribution
, coin
, uniform
) where
import Control.Monad (ap, (>=>))
import Control.Monad.Trans.Class (MonadTrans (lift))
import Crypto.Random (SystemDRG, randomBytesGenerate)
import Data.Bits ((.&.))
import qualified Data.ByteArray as B
import Data.Functor.Identity (Identity (Identity), runIdentity)
import Data.Maybe (fromJust)
-- | Allows randomly sampling elements of type @[email protected]
type Distribution = DistributionT Identity
-- | Allows randomly sampling elements of type @[email protected] in the context of monad @[email protected]
newtype DistributionT m b = DistributionT
{ runDistT :: forall s. Sampler s =>
s -> m (b, s)
}
instance Monad m => Functor (DistributionT m) where
fmap f x = pure f <*> x
instance Monad m => Applicative (DistributionT m) where
pure x = DistributionT $ pure . (x, )
(<*>) = ap
instance Monad m => Monad (DistributionT m) where
a >>= b = DistributionT $ runDistT a >=> (\(a', s') -> runDistT (b a') s')
instance MonadTrans DistributionT where
lift m = DistributionT $ \s -> (, s) <$> m
-- | Provides randomness.
class Sampler s
where
-- | Produce a bit of randomness.
sampleCoin :: s -> (Bool, s)
-- | Samples a distribution.
sample :: s -> DistributionT m b -> m (b, s)
sample s d = runDistT d s
-- | Samples a distribution, discarding the result randomness.
sample' :: Monad m => s -> DistributionT m b -> m b
sample' s d = fst <$> sample s d
instance Sampler SystemDRG where
sampleCoin s = (b .&. 1 == 1, s')
where
(ba :: B.Bytes, s') = randomBytesGenerate 1 s
-- fromJust is safe, as the array is not empty.
(b, _) = fromJust $ B.uncons ba
-- | Lifts a 'Distribution' to an arbitrary monadic 'DistributionT'.
liftDistribution :: Monad m => Distribution b -> DistributionT m b
liftDistribution d = DistributionT $ return . runIdentity . runDistT d
-- | Tosses a fair coin.
coin :: Distribution Bool
coin = DistributionT (Identity . sampleCoin)
-- | A uniform 'Distribution' over all elements of @[a]@.
uniform :: [a] -> Distribution a
uniform xs = do
let l = length xs
let lg = ilog2 l
n <- samplen lg
if n > l
then uniform xs
else return (xs !! n)
where
ilog2 :: Int -> Int
ilog2 1 = 0
ilog2 n
| n > 1 = ilog2 (n `div` 2) + 1
ilog2 _ = error "attempted non-postive logarithm"
samplen :: Int -> Distribution Int
samplen 0 = return 0
samplen lg
| lg > 0 = do
n' <- samplen (lg - 1)
c <- coin
return $
(n' * 2) +
if c
then 1
else 0
samplen _ = error "attempted to sample negative logarithm"

135
src/Yggdrasil/ExecutionModel.hs

@ -0,0 +1,135 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
-- | Defines the basic model of execution for Yggdrasil. This is modelled
-- after, but not directly equal to, the
-- <https://eprint.iacr.org/2000/068 Universal Composability framework by Ran Canetti>.
--
-- Usage typically involves constructing a complex 'Action', and then 'run'ning
-- it.
module Yggdrasil.ExecutionModel
( Operation
, Action(Abort, Sample, Create, SecParam)
, Operations
, Interfaces
, Functionality(..)
, InterfaceMap(..)
, ForceSample(forceSample)
, run
) where
import Control.Monad (ap)
import Control.Monad.Fail (MonadFail (fail))
import Control.Monad.ST (ST, runST)
import Control.Monad.State.Lazy (StateT, runStateT)
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.Maybe (MaybeT (MaybeT), runMaybeT)
import Data.STRef (STRef, newSTRef, readSTRef,
writeSTRef)
import Yggdrasil.Distribution (Distribution, DistributionT (DistributionT, runDistT),
coin, liftDistribution)
import Yggdrasil.HList (HList ((:::), Nil))
-- | Describes what a node with internal state of type @[email protected] does when passed an
-- input of type @[email protected] by @Ref [email protected]
type Operation s c a b = a -> StateT c (Action s) b
-- | Given a list of tuples of input and output types, construct a
-- corresponding list of 'Operation' types.
type family Operations s c (xs :: [(*, *)]) = (ys :: [*]) | ys -> xs where
Operations s c '[] = '[]
Operations s c ('( a, b) ': xs) = Operation s c a b ': Operations s c xs
-- | Given a list of tuples of input and output types, construct a
-- corresponding list of 'Interface' types.
type family Interfaces s (xs :: [(*, *)]) = (ys :: [*]) | ys -> xs where
Interfaces s '[] = '[]
Interfaces s ('( a, b) ': xs) = (a -> Action s b) ': Interfaces s xs
-- | A functionality is a stateful node, with an initial state, and an
-- interface typed by a list of input/output type tuples, and defined through a
-- 'HList' of 'Operation's.
data Functionality s c ops =
Functionality c
(HList (Operations s c ops))
data SendRef s a b =
forall c. SendRef (STRef s c)
(Operation s c a b)
-- | Yggdrasil's version of 'IO'. Is self-contained, and can be opened with
-- 'run'.
data Action s b where
-- | Fail. This should be used over actual errors!
Abort :: Action s b
-- | Retrieves the security parameter of the running system.
SecParam :: Action s Int
-- | Samples from a distribution.
Sample :: Distribution b -> Action s b
Send :: SendRef s a b -> a -> Action s b
-- | Creates a new node from a functionality specification.
Create
:: InterfaceMap s c ops
=> Functionality s c (ops :: [(*, *)])
-> Action s (HList (Interfaces s ops))
Compose :: Action s c -> (c -> Action s b) -> Action s b
instance Functor (Action s) where
fmap f x = pure f <*> x
instance Applicative (Action s) where
pure = Sample . pure
(<*>) = ap
instance Monad (Action s) where
a >>= b = Compose a b
instance MonadFail (Action s) where
fail _ = Abort
-- | Simulates a world running an external action.
run :: (forall s. Action s b) -> DistributionT Maybe b
run a =
DistributionT $ \rng -> runST $ runMaybeT $ runDistT (run' a) rng
run' :: Action s b -> DistributionT (MaybeT (ST s)) b
run' Abort = DistributionT $ \_ -> MaybeT $ return Nothing
-- TODO: Make a parameter
run' SecParam = return 128
run' (Sample d) = liftDistribution d
run' (Send (SendRef (ptr :: STRef s c) op) msg) = do
c <- lift . lift $ readSTRef ptr
(b, c') <- run' (runStateT (op msg) c)
lift . lift $ writeSTRef ptr c'
return b
run' (Create (Functionality c ops)) = do
ptr <- lift . lift $ newSTRef c
return $ ifmap ptr ops
run' (Compose a f) = run' a >>= run' . f
-- | States we can create interfaces from operations. Implemented for all @[email protected]
class InterfaceMap s c (ts :: [(*, *)]) where
ifmap :: STRef s c -> HList (Operations s c ts) -> HList (Interfaces s ts)
instance InterfaceMap s c '[] where
ifmap _ Nil = Nil
instance InterfaceMap s c as => InterfaceMap s c ('( a, b) ': as) where
ifmap ref (x ::: xs) = Send (SendRef ref x) ::: ifmap ref xs
-- | States that we can forcibly sample from a type, such that with negligible
-- probabily there is a collision between samples.
class ForceSample t where
forceSample :: Action s t
instance ForceSample [Bool] where
forceSample = SecParam >>= (\sp -> sequence [Sample coin | _ <- [0 .. sp]])

110
src/Yggdrasil/Functionalities.hs

@ -0,0 +1,110 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
-- | A collection of common functionalities, ready for use.
module Yggdrasil.Functionalities
( ROState
, SigState
, commonRandomString
, randomOracle
, signature
) where
import Control.Monad.State.Lazy (get, modify, put)
import Control.Monad.Trans.Class (lift)
import Yggdrasil.Adversarial (WithAdversary' (WithAdversary'))
import Yggdrasil.Distribution (Distribution)
import Yggdrasil.ExecutionModel (Action (Sample),
ForceSample (forceSample),
Functionality (Functionality),
Interfaces, Operation, Operations)
import Yggdrasil.HList (HList ((:::), Nil))
import Yggdrasil.Nat (Zn)
crsOp :: Distribution b -> Operation s (Maybe b) () b
crsOp d () =
get >>= \case
Just x -> return x
Nothing -> do
x <- lift $ Sample d
put $ Just x
return x
-- | A CRS functionality over a given distribution.
commonRandomString :: Distribution b -> Functionality s (Maybe b) '[ '( (), b)]
commonRandomString d = Functionality Nothing (crsOp d ::: Nil)
-- | The state of a 'randomOracle'. Consists of previously recorded
-- query/response pairs.
type ROState a b = [(a, b)]
roLookup :: Eq a => a -> ROState a b -> Maybe b
roLookup _ [] = Nothing
roLookup x' ((x, y):_)
| x == x' = Just y
roLookup x (_:xs) = roLookup x xs
roOp :: Eq a => Distribution b -> Operation s (ROState a b) a b
roOp d x =
(roLookup x <$> get) >>= \case
Just y -> return y
Nothing -> do
y <- lift $ Sample d
modify ((x, y) :)
return y
-- | A random oracle functionality, over a given distribution.
randomOracle ::
Eq a => Distribution b -> Functionality s (ROState a b) '[ '( a, b)]
randomOracle d = Functionality [] (roOp d ::: Nil)
-- | The state of a 'signature' functionality. Consists of previously recorded
-- signatures, and their corresponding messages and signers.
type SigState s n msg sig = [(Zn n, (msg, sig))]
verifyOp ::
(Eq msg, Eq sig) => Operation s (SigState s n msg sig) (Zn n, (msg, sig)) Bool
verifyOp s = (s `elem`) <$> get
fixAdv ::
(Eq msg, Eq sig, ForceSample sig)
=> HList (Interfaces s '[ '( (Zn n, msg), Maybe sig)])
-> HList (Operations s (SigState s n msg sig) '[ '( (Zn n, msg), sig)])
fixAdv (sign ::: Nil) = sign' ::: Nil
where
sign' (p, msg) = do
sig <-
lift (sign (p, msg)) >>= \case
Just s -> do
st <- get
if (p, (msg, s)) `elem` st
then forceSample' msg p
else return s
Nothing -> forceSample' msg p
modify ((p, (msg, sig)) :)
return sig
forceSample' msg p = do
sig <- lift forceSample
st <- get
-- This may recursive infinitely iff the signature space is too small!
-- This is a feature, not a bug.
if (p, (msg, sig)) `elem` st
then forceSample' msg p
else return sig
-- | A robust signature functionality.
signature ::
(Eq msg, Eq sig, ForceSample sig)
=> WithAdversary' s (SigState s n msg sig)
'[ '( (Zn n, msg), sig)]
'[ '( (Zn n, msg), sig)
, '( (Zn n, (msg, sig)), Bool)
]
signature =
WithAdversary'
fixAdv
(\(sign ::: Nil) -> Functionality [] (sign ::: verifyOp ::: Nil))

73
src/Yggdrasil/HList.hs

@ -0,0 +1,73 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
-- | Provides heterogeneous lists through 'HList', as well as some type and
-- value level operations on them.
module Yggdrasil.HList
( HList(..)
, type (+|+)
, HAppend((+++))
, HSplit(hsplit)
, HSequence(hsequence)
, Applied
) where
infixr 5 :::
-- | A heterogeneous list.
data HList :: [*] -> * where
Nil :: HList '[]
(:::) :: a -> HList as -> HList (a ': as)
-- | Type-level appending of lists.
type family (as :: [k]) +|+ (bs :: [k]) :: [k] where
'[] +|+ bs = bs
(a ': as) +|+ bs = a ': (as +|+ bs)
-- | Value-level appending of 'HList's.
class HAppend as bs where
(+++) :: HList as -> HList bs -> HList (as +|+ bs)
instance HAppend '[] bs where
_ +++ bs = bs
instance HAppend as bs => HAppend (a ': as) bs where
(a ::: as) +++ bs = a ::: (as +++ bs)
-- | Split a 'HList' at the value level given the type-level components.
class HSplit hs as bs where
hsplit :: HList hs -> (HList as, HList bs)
instance HSplit bs '[] bs where
hsplit bs = (Nil, bs)
instance HSplit hs as bs => HSplit (a ': hs) (a ': as) bs where
hsplit (h ::: hs) =
let (as, bs) = hsplit @hs @as @bs hs
in (h ::: as, bs)
type family Applied m (as :: [k]) = (ys :: [k]) | ys -> as where
Applied m '[] = '[]
Applied m (a ': as) = m a ': Applied m as
class HSequence m as where
hsequence :: HList (Applied m as) -> m (HList as)
instance Monad m => HSequence m '[] where
hsequence Nil = return Nil
instance (Monad m, HSequence m as) => HSequence m (a ': as) where
hsequence (a ::: as) = do
a' <- a
as' <- hsequence @m @as as
return (a' ::: as')

105
src/Yggdrasil/MetaProtocol.hs

@ -0,0 +1,105 @@
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
module Yggdrasil.MetaProtocol
( MetaProtocol
, RelayN
, npartyIdeal
, npartyReal
) where
import Control.Monad.State.Lazy (get, put)
import Control.Monad.Trans.Class (lift)
import Yggdrasil.ExecutionModel (Action (Create),
Functionality (Functionality),
InterfaceMap, Interfaces,
Operations)
import Yggdrasil.HList (HList ((:::), Nil),
HSequence (hsequence))
import Yggdrasil.Nat (ForEach, ForEach (foreach),
IdApplied (idApplied), NCopies, Zn)
type MetaProtocol s c c' ops ops'
= Functionality s c ops -> Functionality s c' ops'
class RelayN s n (ops :: [(*, *)]) where
relayNOperations ::
(HList (Interfaces s (WithZn n ops)))
-> Zn n
-> (HList (Operations s () ops))
relayN ::
(HList (Interfaces s (WithZn n ops))) -> Zn n -> Functionality s () ops
relayN is n = Functionality () (relayNOperations @s @n @ops is n)
instance RelayN s n '[] where
relayNOperations _ _ = Nil
instance RelayN s n xs => RelayN s n ('( a, b) ': xs) where
relayNOperations (f ::: xs) n = lift . f . (n, ) ::: relayNOperations @s @n @xs xs n
type family WithZn n (ops :: [(*, *)]) = (ys :: [(*, *)]) | ys -> ops where
WithZn n '[] = '[]
WithZn n ('( a, b) ': xs) = '( (Zn n, a), b) ': WithZn n xs
npartyIdeal ::
forall s c n ops.
( ForEach n (Action s (HList (Interfaces s ops)))
, IdApplied (Action s) n (HList (Interfaces s ops))
, RelayN s n ops
, InterfaceMap s c (WithZn n ops)
, InterfaceMap s () ops
, HSequence (Action s) (NCopies n (HList (Interfaces s ops)))
)
=> MetaProtocol s c
(Maybe (HList (NCopies n (HList (Interfaces s ops)))))
(WithZn n ops)
'[ '( (), HList (NCopies n (HList (Interfaces s ops))))]
npartyIdeal f = Functionality Nothing (mkOp ::: Nil)
where
mkOp _ =
get >>= \case
Just i -> return i
Nothing -> do
f0 <- lift $ Create f
is <-
(lift .
hsequence . idApplied @(Action s) @n @(HList (Interfaces s ops)))
(foreach (\i -> Create (relayN @s @n @ops f0 i)))
put (Just is)
return is
npartyReal ::
forall s c n ops.
( ForEach n (Action s (HList (Interfaces s ops)))
, IdApplied (Action s) n (HList (Interfaces s ops))
, InterfaceMap s c ops
, HSequence (Action s) (NCopies n (HList (Interfaces s ops)))
)
=> MetaProtocol s c
(Maybe (HList (NCopies n (HList (Interfaces s ops)))))
ops