ds_enc_real'.qrhl

# Autogenerated file (by replacing Adv_DS_encT -> Adv_DS_encT', etc. etc. in ds_enc_real.qrhl)

include "variables.qrhl".
include "Adv_DS_enc'.qrhl".

# **Requirements:**
#
# * A accesses c, b, pk
# * A does not access sk, m

# DS indistiguishability game 0, for punc_enc, adversary A
program ds_enc_real' := {
  (pk,sk) <$ keygen ();
  mstar <$ uniform (msg_space ());
  cstar <$ enc () pk mstar;
  in_pk <- pk;
  in_cstar <- cstar;
  call Adv_DS_enc';
}.