{-# OPTIONS --without-K --copatterns #-}
open import Type
open import Data.Two
open import Data.Maybe
open import Data.Product
open import Data.One
open import Data.Two
open import Control.Strategy renaming (run to runStrategy; map to mapStrategy)

open import Function

open import Relation.Binary
open import Relation.Binary.PropositionalEquality

import Game.IND-CPA-dagger
import Game.IND-CPA

module Game.Transformation.CPA-CPAd
  (PubKey    : ★)
  (SecKey    : ★)
  (Message   : ★)
  (CipherText : ★)

  -- randomness supply for, encryption, key-generation, adversary, adversary state
  (Rₑ Rₖ Rₐ† : ★)
  (KeyGen : Rₖ → PubKey × SecKey)
  (Enc    : PubKey → Message → Rₑ → CipherText)
  (Dec    : SecKey → CipherText → Message)
  
where

Rₐ = Rₑ × Rₐ†

module CPA  = Game.IND-CPA        PubKey SecKey Message CipherText Rₑ Rₖ Rₐ  𝟙 KeyGen Enc
module CPA† = Game.IND-CPA-dagger PubKey SecKey Message CipherText Rₑ Rₖ Rₐ† 𝟙 KeyGen Enc

open CPA  using (EXP; R; Adversary; module Adversary)
open CPA† using () renaming (EXP to EXP†; R to R†; Adversary to Adversary†; module Adversary to Adversary†)

R→R† : R → R†
R→R† ((rₑ′ , rₐ†) , rₖ , rₑ , _) = rₐ† , rₖ , rₑ , rₑ′ , _

R†→R : R† → R
R†→R (rₐ† , rₖ , rₑ , rₑ′ , _) = (rₑ′ , rₐ†) , rₖ , rₑ , _

-- inv

[rₑ↔rₑ′]† : R† → R†
[rₑ↔rₑ′]† (rₐ† , rₖ , rₑ , rₑ′ , _) = (rₐ† , rₖ , rₑ′ , rₑ , _)

[rₑ↔rₑ′] : R → R
[rₑ↔rₑ′] ((rₑ′ , rₐ†) , rₖ , rₑ , _) = ((rₑ , rₐ†) , rₖ , rₑ′ , _)

[rₑ↔rₑ′]-inv : ∀ r → [rₑ↔rₑ′] ([rₑ↔rₑ′] r) ≡ r
[rₑ↔rₑ′]-inv r = refl

module Transformations (A† : Adversary†) where

  --open Adversary
  module A† = Adversary† A†
  m†  = A†.m
  b′† = A†.b′

  -- For these three transformations we just forward the messages
  m : Rₐ → PubKey → 𝟚 → Message
  m (_ , rₐ†) = m† rₐ†

{-
  fix[t=_] : (t : 𝟚) → Adversary
  m  fix[t= t ] = m′
  b′ fix[t= t ] (rₑ , rₐ†) pk cb = b′† rₐ† pk cb (Enc pk (m† rₐ† pk t) rₑ)
-}

  fix[t=_] : (t : 𝟚) → Adversary
  fix[t= t ] = record { m = m ; b′ = b′ }
   where
    b′ : ∀ _ _ _ → _
    b′ (rₑ , rₐ†) pk cb = b′† rₐ† pk cb (Enc pk (m† rₐ† pk t) rₑ)

  fix[b=_] : (b : 𝟚) → Adversary
  fix[b= b ] = record { m = m ; b′ = b′ }
   where
    b′ : ∀ _ _ _ → _
    b′ (rₑ , rₐ†) pk ct = b′† rₐ† pk (Enc pk (m† rₐ† pk b) rₑ) ct

  fix[t=]-prop : ∀ b t r → EXP b fix[t= t ] r ≡ EXP† b t A† (R→R† r)
  fix[t=]-prop _ _ _ = refl

  fix[b=]-prop : ∀ b t r → EXP t fix[b= b ] r ≡ EXP† b t A† ([rₑ↔rₑ′]† (R→R† r))
  fix[b=]-prop _ _ _ = refl

open import Relation.Binary.PropositionalEquality
module _
  (Dist : ★)
  (0d : Dist)
  (dist : (f g : R → 𝟚) → Dist)
  (dist-comm : (f g : R → 𝟚) → dist f g ≡ dist g f)
  (dist-≗ : {f g : R → 𝟚} → f ≗ g → dist f g ≡ 0d)
  (Negligible : Dist → ★)
  (0d-Negigible : ∀ {d} → d ≡ 0d → Negligible d)
  (_+Dist_ : Dist → Dist → Dist)
  (+Dist-Negligible : ∀ {x y} → Negligible x → Negligible y → Negligible (x +Dist y))
  (neg-dist-trans : {f g h : R → 𝟚} → Negligible (dist f g) → Negligible (dist g h) → Negligible (dist f h))
  (CPA-secure : ∀ b A → Negligible (dist (EXP b A) (EXP (not b) A)))
  where

  _~_ : (f g : R → 𝟚) → ★
  f ~ g = Negligible (dist f g)

  _~†_ : (f g : R† → 𝟚) → ★
  f ~† g = (f ∘ R→R†) ~ (g ∘ R→R†)

  infixr  _∙_
  _∙_ : Transitive _~_
  _∙_ = neg-dist-trans

  !_  : Symmetric _~_
  !_ {f} {g} = subst Negligible (dist-comm f g)

  ≗→~ : {f g : R → 𝟚} → f ≗ g → f ~ g
  ≗→~ {f} {g} f≗g = 0d-Negigible (dist-≗ f≗g)

  module _ (A† : Adversary†)
     (SUI : (f : R → R) (f-iso : f ∘ f ≗ id) (h : R → 𝟚) → (h ∘ f) ~ h)
    where
    open Transformations A†

    CPA†-secure : EXP† 0₂ 1₂ A† ~† EXP† 1₂ 0₂ A†
    CPA†-secure = CPA-secure 0₂ fix[t= 1₂ ]
                ∙ SUI [rₑ↔rₑ′] [rₑ↔rₑ′]-inv _
                ∙ CPA-secure 1₂ fix[b= 1₂ ]
                ∙ ≗→~ (λ r → fix[b=]-prop 1₂ 0₂ r)
                ∙ SUI [rₑ↔rₑ′] [rₑ↔rₑ′]-inv _

-- -}
-- -}
-- -}
-- -}
-- -}