Browse Source

Find serious problem in the simulated execution (the simulator's state is lost).

tabularasa
Thomas Kerber 11 months ago
parent
commit
46d31107f6
Signed by: Thomas Kerber <tk@drwx.org> GPG Key ID: 8489B911F9ED617B
2 changed files with 89 additions and 50 deletions
  1. 51
    22
      Yggdrasil/Security.agda
  2. 38
    28
      Yggdrasil/World.agda

+ 51
- 22
Yggdrasil/Security.agda View File

@@ -4,6 +4,7 @@ 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; _≤_; _^_; _+_)
@@ -15,7 +16,7 @@ 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 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)
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.Rational using (_÷_)
open WorldType
@@ -61,15 +62,13 @@ 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)

open Simulator

Actionᵣ⇒Actionᵢ : ∀ {ℓ : Level} {πᵢ πᵣ : World ℓ} {A : Set ℓ} →
(S : Simulator πᵢ πᵣ) → Oracle (World.Γ πᵣ) → state S → ℕ →
Action (World.Γ πᵣ) A → Action (World.Γ πᵢ) (A × state S)
(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.Γ πᵣ) → state S → ℕ →
Action↯ (state S) (World.Γ πᵢ) (World.Γ πᵣ) {hon-≡ S} A →
Action (World.Γ πᵢ) (A × state S)
(S : Simulator πᵢ πᵣ) → Oracle (World.Γ πᵣ) → Simulator.state S → ℕ →
Action↯ (Simulator.state S) (World.Γ πᵢ) (World.Γ πᵣ) {Simulator.hon-≡ S} A →
Action (World.Γ πᵢ) (A × Simulator.state S)

private
with-state : ∀ {ℓ Γ A Σ} → Σ → A → Action {ℓ} Γ (A × Σ)
@@ -78,15 +77,19 @@ private
without-state : ∀ {ℓ Γ} {A Σ : Set ℓ} → (A × Σ) → Action {ℓ} Γ A
without-state ⟨ x , _ ⟩ = dist (pure x)

-- WAIT -- Does the state actually properly survive?
-- FIXME: No, it doesn't. This is probably *unavoidable* without adding state
-- to the execution definition. Do this.
Actionᵣ⇒Actionᵢ _ _ _ zero _ = abort
Actionᵣ⇒Actionᵢ S O σ (suc g) ((call↓ {f} ∈Γᵣ x) ↑) with map≡-implies-∈≡ (sym (hon-≡ S)) ∈Γᵣ
Actionᵣ⇒Actionᵢ S O σ (suc 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 (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ᵢ S O σ (suc 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 ⟨ σ , σ ⟩)
@@ -101,27 +104,53 @@ Action↯⇒Action S O σ (suc g) (α >>= β) = (Action↯⇒Action S O σ (suc

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
extract-oracle S O g ∈Γ x = Action↯⇒Action S O (initial S) g
(Simulator.query-map S ∈Γ x) >>= without-state
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

record Adv[_,_]≤_ {ℓ : Level} (πᵢ πᵣ : World ℓ) (ε : ℚ) :
Set (lsuc (lsuc ℓ)) where
Γᵣ : WorldType ℓ
Γᵣ = World.Γ πᵣ
Γᵢ : WorldType ℓ
Γᵢ = World.Γ πᵢ
Σᵣ : WorldState Γᵣ
Σᵣ = World.Σ πᵣ
Σᵢ : WorldState Γᵢ
Σᵢ = World.Σ πᵢ
field
sim-gas : Strategy (World.Γ πᵣ) Guess → ℕ
sim-gas : ℕ
gas-map : ℕ → ℕ
simulator : Simulator πᵢ πᵣ
proof : (g : ℕ) →
(str : Strategy (World.Γ πᵣ) Guess) →
(⌊exec⌋ (simulated-strategy simulator str (sim-gas str)) (World.Σ πᵢ)
(gas-map g))
≈[ ε ]≈
(⌊exec⌋ str (World.Σ πᵣ) g)
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 ℓ} →
-- (S : Simulator πᵢ πᵣ) → Oracle (World.Γ πᵣ) → Simulator.state S → ℕ →
-- Action (World.Γ πᵣ) A → Action (World.Γ πᵢ) (A × Simulator.state S)


-- (str : Strategy Γᵣ Guess) →
-- (⌊exec⌋ (simulated-strategy simulator str (sim-gas str)) (World.Σ πᵢ)
-- (gas-map g))
-- ≈[ ε ]≈
-- (⌊exec⌋ str (World.Σ πᵣ) g)

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

+ 38
- 28
Yggdrasil/World.agda View File

@@ -152,42 +152,52 @@ set (there Γ′∈ ⊑Γ) (stnode Σ Σs) Σ′ = stnode Σ (set′ Γ′∈
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⌋ : ∀ {ℓ Γ A} → Strategy {ℓ} Γ A → WorldState {ℓ} Γ → ℕ →
Dist (Maybe (Lift (lsuc ℓ) A))
exec : ∀ {ℓ Γ A} → Strategy {ℓ} Γ A → WorldState {ℓ} Γ → ℕ →
Dist (Maybe (A × WorldState {ℓ} Γ))
exec′ : ∀ {ℓ Γ A} → Oracle Γ → Action Γ A → WorldState {ℓ} Γ → ℕ →
Dist (Maybe (A × WorldState {ℓ} Γ))
Dist (Result (Lift (lsuc ℓ) A))
exec : ∀ {ℓ Γ A} → Oracle Γ → Action Γ A → WorldState {ℓ} Γ → ℕ →
Dist (Result (A × WorldState {ℓ} Γ))
exec↓ : ∀ {ℓ Γ₁ Γ₂ A} → Oracle Γ₁ → Action↓ Γ₂ A → WorldState {ℓ} Γ₁ →
Γ₂ ⊑ Γ₁ → ℕ → Dist (Maybe (A × WorldState {ℓ} Γ₁))
Γ₂ ⊑ Γ₁ → ℕ → Dist (Result (A × WorldState {ℓ} Γ₁))
exec↑ : ∀ {ℓ Γ₁ Γ₂ A} → Oracle Γ₁ → Action↑ (node Γ₂) A → WorldState {ℓ} Γ₁ →
Γ₂ ⊑ Γ₁ → ℕ → Dist (Maybe (A × WorldState {ℓ} Γ₁))
Γ₂ ⊑ Γ₁ → ℕ → Dist (Result (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′ 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⌋ (strat α O) Σ g = (exec O α Σ 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 >>= λ{
(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 ;
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 nothing
exec↑ O read Σ ⊑Γ _ = pure (just ⟨ get ⊑Γ Σ , Σ ⟩)
exec↑ O (write σ) Σ ⊑Γ _ = pure (just ⟨ tt , set ⊑Γ Σ σ ⟩)
exec↑ O abort Σ ⊑Γ _ = pure nothing
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 >>=
λ{ (llift x) → pure (just ⟨ x , Σ ⟩) }
exec↑ O (query {q = q} q∈ x) Σ ⊑Γ (suc g) = exec O (O (path ⊑Γ q∈) x) Σ g
λ{ (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))
>>= λ{
(just ⟨ x , Σ′ ⟩) → exec↑ O (β x) Σ′ ⊑Γ g;
nothing → pure nothing }
(result ⟨ x , Σ′ ⟩) → exec↑ O (β x) Σ′ ⊑Γ g ;
abort → pure abort ;
out-of-gas → pure out-of-gas }

Loading…
Cancel
Save