Skip to content

feat(Crypto): Generalize encryption schemes over arbitrary monads#581

Open
dtumad wants to merge 3 commits into
leanprover:mainfrom
dtumad:dtumad/monad-generic-encryption-schemes
Open

feat(Crypto): Generalize encryption schemes over arbitrary monads#581
dtumad wants to merge 3 commits into
leanprover:mainfrom
dtumad:dtumad/monad-generic-encryption-schemes

Conversation

@dtumad
Copy link
Copy Markdown

@dtumad dtumad commented May 20, 2026

This PR modifies the definition of encScheme to allow the computations to happen in any monad m given a MonadLiftT m PMF instance (and further a LawfulMonadLiftT instance for some proofs.

Also adds a new HasUniformSelectFinset m typeclass asserting the m can model uniform selection from finite sets, which is needed for the proof of Shanon's theorem in particular.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant