[theories/modules] law of total probability

[alleystoughton]

Add module-based law of total probability for distributions with finite support.
Put it in theories/modules as it uses event partitioning.

[alleystoughton]

I don't understand why the EC library checking failed.

[alleystoughton]

I made the distribution a parameter to the procedure of the Rand module, instead of a theory parameter, and force pushed.

[alleystoughton]

I don't understand why the EC library checking failed.

I see, it's because I checked it with Alt-Ergo. Will fix this.

[alleystoughton]

I don't understand why the EC library checking failed.

It checked for me with Z3 (4.15.4) and CVC5 (1.3.2). Fixed to check with just Z3.

[fdupress]

Using make check before committing or pushing to the EC repo (but after moving your file to the EC working directory) should make use of the easycrypt.project we serve, which should ensure that the CI reproduces successes (barring regressions in SMT solvers, which are mostly rare now that we do not use Alt-Ergo).

I'll do a proper review + local edits when it's not a bank holiday, but wanted to guide your workflow to avoid you having to figure out why CI is failing in the future!