AsymScheme games inadequately represent CPA

[MarkusKL]

It seems to me, that the examples of CPA related games in AsymScheme.v inadequately represent their textbook counterpart (e.g. Joy of Cryptography, Sec. 15).

In the textbook, KeyGen is called once at initialization. In the the code, KeyGen is evaluated on every call to CHALLENGE, which means that the public key is re-rolled for every message.
As a consequence, the public key is not accessible to the adversary before choosing a challenge, because it has not been generated yet.

I belive, that the following formulation is an adequate representation of the PK-OTS$ game-pair: https://github.com/MarkusKL/nominal-ssprove/blob/0140853451a0d36a5105e3d319be863f2d95fd8d/theories/Example/PK/Scheme.v
It evaluates KeyGen when GETPK is called instead.
However, to complete the ElGamal to DDH reduction I have had to use an altered version of the DDH game-pair: https://github.com/MarkusKL/nominal-ssprove/blob/0140853451a0d36a5105e3d319be863f2d95fd8d/theories/Example/PK/DDH.v

I am happy to elaborate or discuss solutions, let me know what you find.