MarkusKL
MarkusKL
Locations and Inerfaces are based on fset from extructures. This PR changes it so that they are now based on fmap like packages already are. Improvements made by this PR:...
This issue is about replacing the dependecy [extructures](https://github.com/arthuraa/extructures) with [finmap](https://github.com/math-comp/finmap) In my attempt to do so I have made the following observations: - Advantage: finmap is based on choiceType rather...
It seems to me, that the examples of CPA related games in `AsymScheme.v` inadequately represent their textbook counterpart (e.g. Joy of Cryptography, Sec. 15). In the textbook, KeyGen is called...
It seems that the use of `fst` and `snd` are swapped in the ElGamal decryption algorithm in the examples. I would suggest adding a correctness game to `AsymScheme.v` and prove...
This PR lifts the requirement that choice_types are inhabited, which allows for significant simplifications. This also allows us to model all `finType`s as `choice_type` instead of just the inhabited ones,...
Some discussion here: #90 Flakes are not supported by the rocq-nix-toolbox (yet): https://github.com/rocq-community/coq-nix-toolbox/issues/359 https://github.com/rocq-community/coq-nix-toolbox/pull/361 I have moved over to developing with `nix-shell` based environment that uses the correct versions according...
Motivation: Currently, the definitions and lemmas about sub-distributions are drawn from the sub-package experimental_reals from mathcomp-analysis. The theory relies on some admitted `interchange_psum` theorem while newer mathcomp-analysis theories based on...