aboutsummaryrefslogtreecommitdiff
path: root/src/Spec/ModularArithmetic.v
Commit message (Collapse)AuthorAge
* Import prim token notations before using themGravatar Jason Gross2018-08-24
| | | | | | | | | | | This is required for compatibility with https://github.com/coq/coq/pull/8064, where prim token notations no longer follow `Require`, but instead follow `Import`. c.f. https://github.com/coq/coq/pull/8064#issuecomment-415493362 Almost all changes were made via https://gist.github.com/JasonGross/5d4558edf8f5c2c548a3d96c17820169#file-fix-py
* enforce use of [F.zero], [F.one]; prove Ed25519 admitsGravatar Andres Erbsen2017-07-07
|
* rename-everythingGravatar Andres Erbsen2017-04-06
|
* use [positive] for [F] modulus, char_ge_C instead of char_gt_CGravatar Andres Erbsen2017-03-02
|
* ModularArithmetic: conversions between [F] and [nat]Gravatar Andres Erbsen2016-09-16
|
* [cbv beta] in the beginning of Obligation Tactic for 8.5Gravatar Andres Erbsen2016-08-08
|
* [F] has its own module nowGravatar Andres Erbsen2016-08-05
| | | | | | [ZToField] -> [F.of_Z] [FieldToZ] -> [F.to_Z] [Zmod.lem] -> [F.lem]
* Refactor ModularArithmetic into Zmod, expand DecidableGravatar Andres Erbsen2016-08-04
| | | | | | | | | | | | 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
* compute on [F q]!Gravatar Andres Erbsen2016-07-20
|
* More changes for 8.5Gravatar Jason Gross2016-06-10
| | | | [Local Coercion :=] changed meanings. Use [Let] and [Local Coercion] for consistent behavior
* Finish absolutizing importsGravatar Jason Gross2016-03-10
| | | | | | | | | | | | The file coqprime/Coqprime/ListAux.v was importing List, which was confusing machines on which mathclasses was also installed. Using https://github.com/JasonGross/coq-tools ```bash make -kj10 cd src git ls-files "*.v" | xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Crypto ```
* update F Coercions and tutorialGravatar Andres Erbsen2016-02-14
|
* prove existance of F inv, implement pow -- CompleteEdwardsCurve.unifiedAdd ↵Gravatar Andres Erbsen2016-02-13
| | | | Closed Under Global Context
* implement F_oppGravatar Andres Erbsen2016-02-12
|
* Define F m, a replacement for GF with several benefits.Gravatar Andres Erbsen2016-02-11
| | | | | | | | | | | | | - F has a human readable complete specification - F is a parametric type, not a parametric module - Different F instances can be disambiguated by type inference, which is more conventient that notation scopes. - F has significant support for non-prime moduli - It should be relatively easy to port existing GF code to F. Since the repository currently contains code referencing both F and GF, it makes sense to keep the names different for now. Later, F may or may not be renamed to GF.
* fresh take at specifications using implicit arguments instead of module ↵Gravatar Andres Erbsen2016-02-07
parameters
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 15:52:37 +0000