{-# OPTIONS --without-K --copatterns #-}

open import Type
open import Data.Maybe
open import Data.Product
open import Data.One
open import Data.Bit
open import Control.Strategy

open import Relation.Binary.PropositionalEquality

import Game.IND-CPA-utils
import Game.IND-CPA
import Game.IND-CCA

module Game.Transformation.CCA-CPA
  (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

open Game.IND-CPA-utils Message CipherText
module CCA = Game.IND-CCA PubKey SecKey Message CipherText Rₑ Rₖ Rₐ   KeyGen Enc Dec
module CPA = Game.IND-CPA PubKey SecKey Message CipherText Rₑ Rₖ Rₐ 𝟙 KeyGen Enc

A-transform : CPA.Adversary → CCA.Adversary
A-transform A rₐ pk = done CPApart where
    module A = CPA.Adversary A
    mb = A.m rₐ pk
    CPApart : CPAAdversary _
    get-m CPApart = mb 0b , mb 1b
    put-c CPApart = A.b′ rₐ pk

correct : ∀ {rₑ rₖ rₐ} b adv → CPA.EXP b adv               (rₐ , rₖ , rₑ , _)
                             ≡ CCA.EXP b (A-transform adv) (rₐ , rₖ , rₑ)
correct 1b adv = refl
correct 0b adv = refl