require import AllCore Real Distr.
require (*--*) SKE_INDR.

type key, ptxt, ctxt.
type msg.

(** The security of padded encryption is parameterized by the
    additional "hiding qualities" provided by the padding. We only ask
    that sampling a valid ciphertext given its low-level leakage is
    the same as sampling a valid ciphertext given the high-level
    leakage of its padded version. **)
type leaks_m, leaks_p.
op leak_m: msg  -> leaks_m.
op leak_p: ptxt -> leaks_p.

op dC_m: leaks_m -> ctxt distr.
axiom dC_m_ll l: is_lossless (dC_m l).

op dC_p: leaks_p -> ctxt distr.
axiom dC_p_ll l: is_lossless (dC_p l).

op pad  : msg -> ptxt.
op unpad: ptxt -> msg option.

axiom pcan_pad m: unpad (pad m) = Some m.
axiom leak_pad m: dC_m (leak_m m) = dC_p (leak_p (pad m)).

clone SKE_INDR as CoreDefs with
  type eK    <- key,
  type ptxt  <- ptxt,
  type ctxt  <- ctxt,
  type leaks <- leaks_p,
  op   leak  <- leak_p,
  op   dC    <- dC_p
proof * by smt.

clone import SKE_INDR as PtE with
  type eK    <- key,
  type ptxt  <- msg,
  type ctxt  <- ctxt,
  type leaks <- leaks_m,
  op   leak  <- leak_m,
  op   dC    <- dC_m
proof * by smt.
import RCPA.

module PadThenEncrypt (S:CoreDefs.Enc_Scheme): Enc_Scheme = {
  proc keygen = S.keygen

  proc enc(k:key,m:msg): ctxt = {
    var c;

    c <@ S.enc(k,pad m);
    return c;
  }

  proc dec(k:key,c:ctxt): msg option = {
    var p;

    p <@ S.dec(k,c);
    return obind unpad p;
  }
}.

module RCPAa (A:RCPA_Adversary,O:CoreDefs.RCPA.RCPA_Oracles) = {
  module S = {
    proc enc(m:msg): ctxt = {
      var c;

      c  <@ O.enc(pad m);
      return c;
    }
  }

  proc distinguish = A(S).distinguish
}.

section RCPA.
  declare module S <: CoreDefs.Enc_Scheme { RCPA_Wrap, CoreDefs.RCPA.RCPA_Wrap }.
  declare module A <: RCPA_Adversary  { RCPA_Wrap, CoreDefs.RCPA.RCPA_Wrap, S }.

  local lemma PtE_Ideal &m:
    Pr[INDR_CPA(Ideal,A).main() @ &m: res]
    = Pr[CoreDefs.RCPA.INDR_CPA(CoreDefs.RCPA.Ideal,RCPAa(A)).main() @ &m: res].
  proof.
    byequiv=> //=; proc.
    call (_: true).
      by proc; inline *; auto; smt.
    by call (_: true).
  qed.

  lemma RCPA_preservation &m:
    `|Pr[INDR_CPA(PadThenEncrypt(S),A).main() @ &m: res]
      - Pr[INDR_CPA(Ideal,A).main() @ &m: res]|
    = `|Pr[CoreDefs.RCPA.INDR_CPA(S,RCPAa(A)).main() @ &m: res]
        - Pr[CoreDefs.RCPA.INDR_CPA(CoreDefs.RCPA.Ideal,RCPAa(A)).main() @ &m: res]|.
  proof.
    rewrite (PtE_Ideal &m); do !congr.
    byequiv=> //=; proc; inline *.
    call (_:    ={glob S}
             /\ ={k}(RCPA_Wrap,CoreDefs.RCPA.RCPA_Wrap)).
      by proc; inline *; wp; call (_: true); auto; smt.
    by call (_: true).
  qed.
end section RCPA.