ds_encT_real_game1.qrhl

include "ds_encT_real.qrhl".
include "game1.qrhl".

# GRAPH: EQ("ds_encT_real_game1","ds_encT_real","game1")
lemma ds_encT_real_game1: Pr[b=1 : ds_encT_real(rho)] = Pr[b=1 : game1(rho)].
 byqrhl.
 inline game1.
 inline ds_encT_real.

 equal.
  simp!.
 conseq post: ℭ𝔩𝔞[in_cstar1 = in_cstar2 ∧ in_pk1 = in_pk2 ∧ classA1 = classA2 ∧ b1 = b2 ∧ G1 = G2] ⊓ ⟦quantA1⟧ ≡𝔮 ⟦quantA2⟧.
  simp!.

 # cstar, rstar, in_pk, in_cstar
 wp 3 4.
 conseq post: ℭ𝔩𝔞[pk1=pk2 & G1=G2 ∧ mstar1=mstar2 ∧ classA1=classA2 ∧ b1=b2] ⊓ ⟦quantA1⟧ ≡𝔮 ⟦quantA2⟧.
  simp! encrT_def.

 rnd.
 conseq post: ℭ𝔩𝔞[pk1=pk2 & G1=G2 ∧ classA1=classA2 ∧ b1=b2] ⊓ ⟦quantA1⟧ ≡𝔮 ⟦quantA2⟧.
  simp! msg_spaceT_def.

 rnd.
 conseq post: ℭ𝔩𝔞[G1=G2 ∧ classA1=classA2 ∧ b1=b2] ⊓ ⟦quantA1⟧ ≡𝔮 ⟦quantA2⟧.
  simp! keygenT_def.

 rnd.
 skip.
 simp!.
qed.