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

open import Type
open import Function
open import Data.Bit
open import Data.Maybe
open import Data.Product
open import Data.One
open import Control.Strategy renaming (run to runStrategy; map to mapStrategy)

open import Relation.Binary.PropositionalEquality

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

module Game.Transformation.CCA2-CCA
  (PubKey    : )
  (SecKey    : )
  (Message   : )
  (CipherText : )

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

open Game.IND-CPA-utils Message CipherText

CPA-A-transform : CPAAdversary Bit  CPAAdversary (DecRound Bit)
get-m (CPA-A-transform A) = get-m A
put-c (CPA-A-transform A) = done  put-c A

module CCA2 = Game.IND-CCA2 PubKey SecKey Message CipherText Rₑ Rₖ Rₐ KeyGen Enc Dec 
module CCA  = Game.IND-CCA  PubKey SecKey Message CipherText Rₑ Rₖ Rₐ KeyGen Enc Dec

A-transform : CCA.Adversary  CCA2.Adversary
A-transform adv = adv' where
    adv' : _  _  _ 
    adv' rₐ pk = mapStrategy CPA-A-transform (adv rₐ pk)
  {-
  m' : _ → _ → _
  m' rₐ pk = m rₐ pk

  d' : _ → _ → _ → (_ : _) → _
  d' rₐ' rₓ pk c = Pick (d rₐ' rₓ pk c)
  -}

{-
valid-transform : ∀ adv → CCA2.Valid-Adv (A-transform adv)
valid-transform adv = tt
-}

correct :  b adv r  CCA.EXP  b adv               r
                     CCA2.EXP b (A-transform adv) r
correct b adv (rₐ , rₖ , rₑ)
 =  cong  A  runStrategy (Dec sk) (put-c A (Enc pk (proj (get-m A) b) rₑ)))
         (sym (run-map (Dec sk) CPA-A-transform (adv rₐ pk)))

         where k  = KeyGen rₖ
               pk = proj₁ k
               sk = proj₂ k