feat(Crypto): Generalize encryption schemes over arbitrary monads

[dtumad]

This PR modifies the definition of encScheme to allow the computations to happen in any monad m, and defines correctness in terms of a MonadLiftT m PMF instance (and further a LawfulMonadLiftT instance for some proofs). Also adds an example of a runnable version of otp by taking m to be FreeM (PFunctor.Obj {A := ℕ, B := BitVec}) with custom private lifting instances.

Also adds a new HasUniformBitVec m/LawfulUniformBitVec m typeclass asserting the m can model uniform selection of bitvectors, which is needed for the proof of Shanon's theorem in particular, as well as similar classes for finite sets and finite types.

[SamuelSchlesinger]

Thanks for the PR, though I'm not sure I understand the goal here yet: Are you planning to add a new variant of a perfectly secret encryption scheme? Did you plan to extract these for execution? Or did you plan to use this for computationally secure encryption schemes?

I believe, following Katz-Lindell, the latter would be best handled by a new definition altogether. It would be nice if the PR description contained a justification for the change along with a description.

[SamuelSchlesinger]

Didn't do a full review, curious to hear your response to my question before I do so.

[dtumad]

Did you plan to extract these for execution?

This was my main goal, I've pushed an actual example of making this runnable, although it involved some further refactoring to seperate PMF noncomputability. I just picked OTP as the example for this since it's simpler than the secret sharing construction.

Are you planning to add a new variant of a perfectly secret encryption scheme?

This seems unneeded I think given the uniqueness theorem.

I believe, following Katz-Lindell, the latter would be best handled by a new definition altogether. It would be nice if the PR description contained a justification for the change along with a description.

Agreed, I don't think this can really stretch to fit that.

[SamuelSchlesinger]

Fantastic, thank you for explaining! I'll make some time to review this in the coming week.