(* --------------------------------------------------------------------
 * Copyright (c) - 2012--2016 - IMDEA Software Institute
 * Copyright (c) - 2012--2021 - Inria
 * Copyright (c) - 2012--2021 - Ecole Polytechnique
 *
 * Distributed under the terms of the CeCILL-B-V1 license
 * -------------------------------------------------------------------- *)

require import Bool Core Int List.
require import DBool.

type pkey, skey, ptxt, ctxt.

module type Scheme = {
  proc kg() : pkey * skey
  proc enc(pk:pkey, m:ptxt) : ctxt
}.

module type Adversary = {
  proc choose(pk:pkey) : ptxt * ptxt
  proc guess(c:ctxt)   : bool
}.

module CPA (S:Scheme) (A:Adversary) = {
  proc main() : bool = {
    var pk, sk, m0, m1, c, b, b';

    (pk, sk) <@ S.kg();
    (m0, m1) <@ A.choose(pk);
    b        <$ {0,1};
    c        <@ S.enc(pk, b ? m1 : m0);
    b'       <@ A.guess(c);
    return (b' = b);
  }
}.