zCDP definition unnecessarily weakens zCDP composition bound #45
Description
Our definition of zCDPBound _ ε corresponds to (ε^2/2)-zCDP from the literature. This difference is mostly harmless, but since the abstract DP system is specified in terms of ε it means that the abstract composition bound only provides ((ε1+ε2)^2/2)-zCDP, while it could provide (ε1^2/2 + ε2^2/2)-zCDP.
Changing the definition of zCDP to match the literature would allow us to improve this bound, though it would have a sizable impact on the existing codebase. The loose step in the adaptive composition proof is made explicit here, but the loose step in the non-adaptive composition bound is more deeply embedded in the proof.