| Commit message (Collapse) | Author | Age |
|
|
|
|
|
| |
[ZToField] -> [F.of_Z]
[FieldToZ] -> [F.to_Z]
[Zmod.lem] -> [F.lem]
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
ModularArithmetic now uses Algebra lemmas in various places instead of
custom manual proofs. Similarly, Util.Decidable is used to state and
prove the relevant decidability results.
Backwards-incompatible changes:
F_some_lemma -> Zmod.some_lemma
Arguments ZToField _%Z _%Z : clear implicits.
inv_spec says inv x * x = 1, not x * inv x = 1
|
| |
|
| |
|
| |
|
|
|
|
|
| |
Fix for Warning: Nested proofs are deprecated and will stop working in a
future Coq version [deprecated-nested-proofs,deprecated]
|
| |
|
|
- PointEncoding (these will hopefully come back soon)
- EdDSAProofs (not a priority to bring back, but not hard either)
- Ed25519 spec bits and pieces which were not finished anyway
|