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

open import Type
open import Function
open import Data.Bit
open import Data.Two.Equality
open import Data.Maybe
open import Data.Product
open import Data.Unit

open import Data.Nat.NP hiding (_==_)
open import Data.Nat.Distance
--open import Rat

open import Explore.Core
open import Explore.Explorable
open import Explore.Product
open Operators
open import Relation.Binary.PropositionalEquality.NP
open import Control.Strategy renaming (run to runStrategy)

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

module Game.IND-CCA2
  (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

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

Adversary : 
Adversary = Rₐ  PubKey 
                   DecRound            -- first round of decryption queries
                     (CPAAdversary     -- choosen plaintext attack
                       (DecRound Bit)) -- second round of decryption queries

{-
TODO
Valid-Adv : Adv → Set
Valid-Adv adv = ∀ {rₐ rₓ pk c} → Valid (λ x → x ≢ c) {!!}
-}

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

EXP : Bit  Adversary  R  Bit
EXP b m (rₐ , rₖ , rₑ) with KeyGen rₖ
... | pk , sk = b′ where
  decRound = runStrategy (Dec sk)
  
  round1 = decRound (m rₐ pk)
  mb     = proj (get-m round1) b
  c      = Enc pk mb rₑ
  round2 = put-c round1 c
  b′     = decRound round2

game : Adversary  (Bit × R)  Bit
game A (b , r) = b == EXP b A r

module Cheating
   (m : Bit  Message)
   (m⁻¹ : Message  Bit)
   where

  cheatingA : Adversary
  cheatingA rₐ pk = done CPApart
    where CPApart : CPAAdversary _
          get-m CPApart   = tabulate₂ m
          put-c CPApart c = ask c (done  m⁻¹)

  module _
    (DecEnc :  rₖ rₑ m  let (pk , sk) = KeyGen rₖ in
                          Dec sk (Enc pk m rₑ)  m)
    (m⁻¹-m :  x  m⁻¹ (m x)  x)
    where

    cheatingA-always-wins :  r  game cheatingA r  1b
    cheatingA-always-wins (b , rₐ , rₖ , rₑ) =
      ap (_==_ b  m⁻¹) (DecEnc rₖ rₑ (proj (tabulate₂ m) b)  proj-tabulate₂ m b)  ==-≡1₂.reflexive (!(m⁻¹-m b))
  
module Advantage
  (μₑ : Explore₀ Rₑ)
  (μₖ : Explore₀ Rₖ)
  (μₐ : Explore₀ Rₐ)
  where
  μR : Explore₀ R
  μR = μₐ ×ᵉ μₖ ×ᵉ μₑ
  
  module μR = FromExplore₀ μR
  
  run : Bit  Adversary  
  run b adv = μR.count (EXP b adv)
  
  Advantage : Adversary  
  Advantage adv = dist (run 0b adv) (run 1b adv)
    
  --Advantageℚ : Adv → ℚ
  --Advantageℚ adv = Advantage adv / μR.Card
  
-- -}
-- -}
-- -}
-- -}