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 <- Hq cstar;
  in_pk <- pk;
  in_cstar <- cstar;
  gin <- undefined;
  gout <- undefined;
  H <- mk_Hq Hq H0 G pk;
  call Adv_INDCCA_encFO(queryG,queryH,decapsQuery1);
}.