add Reflection theory

[oskgo]

The theory allows you to lift probability expressions to distributions, entirely within the logic thanks to bypr with two arguments and rnd.

Unlike the existing proc op and rndsem tactics this theory can handle calls to abstract modules. AFAICT the only real limitation in current EasyCrypt is the suboptimal UI. The distribution is provided through an existential in a lemma, so it cannot be used in top level operators and thus needs to be reintroduced in every lemma.

Extracted and adapted from the artifacts of “Reflection, Rewinding, and Coin-Toss in EasyCrypt” by Denis Firsov and Dominique Unruh.

cc: @dfirsov @dominique-unruh

[fdupress]

@dfirsov and @dominique-unruh are you happy for this to be included in EC's source code and distributed under the terms of the MIT licence/license? It would be helpful if you could explicitly licence the original definitions and proofs under similarly permissive terms (BSD or MIT, or one of the permissive CCs), but agreement here is probably fine.

Let us know, also, how you prefer this to be attributed.

[dfirsov]

@dfirsov and @dominique-unruh are you happy for this to be included in EC's source code and distributed under the terms of the MIT licence/license? It would be helpful if you could explicitly licence the original definitions and proofs under similarly permissive terms (BSD or MIT, or one of the permissive CCs), but agreement here is probably fine.

Let us know, also, how you prefer this to be attributed.

Yes, absolutely! Feel free to include our development in the EC's source code.

It would be nice if you would just mention the respective eprint (https://ia.cr/2021/1078).

[dominique-unruh]

Yes, you have my consent to include the paper under the MIT license.
Please add an attribution to the original authors (Denis Firsov and Dominique Unruh). (I am not sure whether MIT license formally requires it.)
And please add a citation to the published paper. (E.g., "Unruh, Firsov, Reflection, rewinding, and coin-toss in EasyCrypt, CPP 2022, doi: 10.1145/3497775.35036".)

Sorry for the back and forth but Denis responded before seeing my email on the topic.

[fdupress]

Sorry for the back and forth but Denis responded before seeing my email on the topic.

This is absolutely not a problem—that's why I asked you both :)

We'll attribute co-authorship in the commit message, and point to the peer-reviewed proceedings version of the paper in commit message and a comment.

Thank you both for the contribution!

[oskgo]

I used previous commits of yours for the (required) co-author email. @dfirsov, the email I found seems to be private. The main author email is hidden in the web-ui by default, but this is not the case for co-authors. If you'd like to hide your email can you follow the steps at this link to get me a github noreply email I can use?

[dfirsov]

I used previous commits of yours for the (required) co-author email. @dfirsov, the email I found seems to be private. The main author email is hidden in the web-ui by default, but this is not the case for co-authors. If you'd like to hide your email can you follow the steps at this link to get me a github noreply email I can use?

No, actually I don't want to hide my email and also my "Keep my email addresses private" setting is off.