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

open import Type
open import Data.Bit
open import Data.Maybe
open import Data.Product
open import Control.Strategy renaming (run to runStrategy)
import Game.IND-CPA-utils
  
module Game.IND-CCA
  (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

Adversary : ★
Adversary = Rₐ → PubKey → DecRound (CPAAdversary Bit)

R : ★
R = Rₐ × Rₖ × Rₑ

Experiment : ★
Experiment = Adversary → R → Bit

EXP : Bit → Experiment
EXP b adv (rₐ , rₖ , rₑ) with KeyGen rₖ
... | pk , sk = b′ where
  module AdvCPA = CPAAdversary (runStrategy (Dec sk) (adv rₐ pk))
  mb = proj AdvCPA.get-m b
  c  = Enc pk mb rₑ
  b′ = AdvCPA.put-c c