game1FO'_goodbad_o2h_left_class.qrhl

# Autogenerated file (by replacing game0FO -> game0FO', game1FO -> game1FO', etc. etc. in game1FO_goodbad_o2h_left_class.qrhl)

include "ClassicalQueryG.qrhl".
include "decapsQuery1.qrhl".
include "Adv_INDCCA_encFO.qrhl".
include "queryG.qrhl".
include "queryH.qrhl".

# Relative to game1FO'_goodbad_o2h_left', we unwrap Adv_O2H_Game1FO' and
# replace ClassicalQueryG(queryG) and queryH_Hq(queryG) and decapsQuery1_G(queryG)
# back by G gin, queryH, decapsQuery1.
  
program game1FO'_goodbad_o2h_left_class := {
  count <- 0;
  (S,G,G',z') <$ goodbad_o2h_distr;
  (pk,sk) <- z';
  Hr <$ uniform UNIV;
  H0 <$ uniform UNIV;
  Hq <$ uniform UNIV;
  prfk <$ keygenPRF;
  mstar <$ uniform (msg_spaceT undefined);
  gin <- mstar;
  gout <- G gin;
  cstar <- encr () pk mstar gout;
  Kstar <$ uniform UNIV;
  in_pk <- pk;
  in_cstar <- cstar;
  gin <- undefined;
  gout <- undefined;
  H <- mk_Hq Hq H0 G pk;
  call Adv_INDCCA_encFO(queryG,queryH,decapsQuery1);
}.