Hi,

I have two games defined as follows:

```
game0 = TRY do {
α::nat ← sample_uniform (order G⇩p);
x::'y ← (𝒜::nat ⇒ 'y spmf) α;
_ :: unit ← assert_spmf (a x);
return_spmf True
} ELSE return_spmf False
```

and

```
game1 = TRY do {
α::nat ← sample_uniform (order G⇩p);
x::'y ← (𝒜::nat ⇒ 'y spmf) α;
_ :: unit ← assert_spmf (a x);
_ :: unit ← assert_spmf (b x);
return_spmf True
} ELSE return_spmf False
```

Now I want to show that the advantage the Adversary A can have in game0 is greater-equal to the advantage it can have in game1 , which is trivially true (or at least I thought so..) as game1 literally adds one assert to game0.

However, the proof is not easy (for me).

I would greatly appreciate any help or advice in proving this thing. I already looked through the SPMF theory, but couldn't find anything, but a lot of measure lemmas, which left me clueless.

Ah one more thing, the goal looks like this:

```
spmf (game0 A) True <= spmf (game1) True
```

Thanks for your time :)

hi Tobias, have you looked at https://eprint.iacr.org/2018/941 ?

In this case, you need to apply some form of "identical-until-bad" reasoning (see Section 3.6) -- which I do agree was a bit heavyweight when I tried it

Hi Yong,

thanks a lot for the hint. I looked at it when I started with CryptHOL, but my understanding wasn't good enough to think of it again.

But looks exactly like what I need to do, so thanks a lot! That saved definitely a lot of hours searching around :)

FWIW: I found it much easier to start with `spmf`

only when trying this out, I'm still totally lost on `gpv`

s if I have to be honest :laughing:

I can relate, even spmf is hard for me now, luckily I don't have to deal with gpv for my project :laughing:

In case someone every stumbles upon this, I managed to proof this thing without a failure-event proof.

Its the lemma "spmf_reduction" in this file:https://github.com/tobias-rothmann/KZG-Polynomial-Commitment-Scheme/blob/main/KZG_poly_bind.thy#L624

I don't know anything about CryptHOL, but I'd prove this by relational reasoning, without going down all the level to computing integrals. You can insert a `_ :: unit ← assert_pmf True`

in the first program at the location where the additional line in the second one is, and then you can prove `rel_spmf (=) game1 game0`

compositionally because the two programs are syntactically completely equal except for that one line, and that should give you what you need.

Manuel Eberl said:

I don't know anything about CryptHOL, but I'd prove this by relational reasoning, without going down all the level to computing integrals. You can insert a

`_ :: unit ← assert_pmf True`

in the first program at the location where the additional line in the second one is, and then you can prove`rel_spmf (=) game1 game0`

compositionally because the two programs are syntactically completely equal except for that one line, and that should give you what you need.

Ahh thanks for the hint! Didn't think of it, I'll try it out and update accordingly sometime soon. Thanks :)

Last updated: Dec 07 2023 at 08:19 UTC