{-# OPTIONS --without-K #-}
open import Type
open import Data.Two
open import Data.Product

module Game.EntropySmoothing
  (M    : )        -- Message
  (Hash : )
  (   : M  Hash) -- Hashing function
  (Rₐ   : )        -- Adversary randomness
  where

-- Entropy smoothing adversary
Adversary : 
Adversary = Rₐ  Hash  𝟚

-- The randomness supply needed for the entropy
-- smoothing games
R : 
R = M × Hash × Rₐ

-- Entropy smoothing experiment:
--   * input: adversary and randomness supply
--   * output b: adversary claims we are in game EXP b
Experiment : 
Experiment = Adversary  R  𝟚

-- In this game we always use ℋ on a random message
EXP₀ : Experiment
EXP₀ A (m , _ , rₐ) = A rₐ ( m)

-- In this game we just retrun a random Hash value
EXP₁ : Experiment
EXP₁ A (_ , h , rₐ) = A rₐ h

-- Package the two previous games
EXP : 𝟚  Experiment
EXP = proj (EXP₀ , EXP₁)

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