aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic
Commit message (Collapse)AuthorAge
* Changed [auto]s to [eauto]s in ModularBaseSystemProofs for 8.5 compatibility.Gravatar jadep2016-07-07
|
* Merged changes, including new ZUtil conventions.Gravatar jadep2016-07-06
|\
* | Factored out some proofs that rely only on base being powers of two, and ↵Gravatar jadep2016-07-06
| | | | | | | | defined conversion between two such bases. This will allow conversion between the pseudomersenne base representation and the wire format. Also relocated some lemmas to Util.
| * Implement and prove Barrett reduction on Z (#18)Gravatar Jason Gross2016-07-03
| | | | | | | | | | | | | | | | Implement and prove Barrett reduction on Z This will serve as the high-level algorithm for modular reduction. We follow Wikipedia very closely, except where we can do better (I believe @jadephilipoom is updating Wikipedia).
| * Make ZUtil more uniformGravatar Jason Gross2016-07-02
| | | | | | | | | | | | | | | | The standard library uses Z.*, and Z* and Z_* are compatibility notations. We follow suit. Also, eliminate a few lemmas that are duplicates of ones in the standard library.
* | added and proved shift/or decode operation 'decode_bitwise'Gravatar jadep2016-06-30
| |
* | encode operation in ModularBaseSystem now uses bitwise operators, taking ↵Gravatar jadep2016-06-29
| | | | | | | | advantage of the fact that base elements are required to be powers of 2
* | BaseSystem encode function is no longer naive; it does a mod/div loop rather ↵Gravatar jadep2016-06-28
|/ | | | than sticking the value of the Z input in the first digit. The condition that c is positive has been added to PseudoMersenneBaseParams--it is necessary for this encode and for canonicalization, for which it was previously a section variable.
* Aggregate all level specifications not in Spec/*Gravatar Jason Gross2016-06-22
| | | | | This prevents notation conflicts (see comment in Notations.v for more explanation).
* remove trailing whitespace from src/Gravatar Andres Erbsen2016-06-20
|
* Merge branch 'field-experiment'Gravatar Andres Erbsen2016-06-20
|\ | | | | | | includes broken files to be removed in next commit
| * [F q] is [Algebra.field]Gravatar Andres Erbsen2016-06-20
| |
| * port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try ↵Gravatar Andres Erbsen2016-06-18
| | | | | | | | fewer nonzero ports. remove FField and FNsatz
* | Canonicalization is now automated in GF25519 and added to GF1305.Gravatar jadep2016-06-17
| |
* | Specific version of freeze for GF25519 (automation still needs a little work)Gravatar jadep2016-06-17
| |
| * move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheoremsGravatar Andres Erbsen2016-06-17
| |
| * Z is integral domainGravatar Andres Erbsen2016-06-16
| |
* | PseudoMersenneBaseRep.mul now carries by default (made possible by strictly ↵Gravatar jadep2016-06-15
| | | | | | | | base-length digit vectors)
* | changed representation definition to require digits vector to be the exact ↵Gravatar jadep2016-06-15
| | | | | | | | length of the base vector
* | Added canonicalization to ModularBaseSystemOpt.Gravatar jadep2016-06-15
| |
* | MergeGravatar jadep2016-06-14
|\ \
* | | Finished admits for canonicalization proofs.Gravatar jadep2016-06-14
| | |
* | | reversed modulus_digits and proved a few admitsGravatar jadep2016-06-13
| | |
* | | progress on second stage (conditional constant-time subtraction) of ↵Gravatar jadep2016-06-13
| | | | | | | | | | | | canonicalization proofs
| * | More Coq 8.4pl2 fixesGravatar Jason Gross2016-06-11
| | |
* | | starting rewrite using different definition of mapGravatar jadep2016-06-11
| |/ |/|
| * More changes for 8.5Gravatar Jason Gross2016-06-10
| | | | | | | | [Local Coercion :=] changed meanings. Use [Let] and [Local Coercion] for consistent behavior
| * 8.5 fixesGravatar Jason Gross2016-06-10
|/
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-05-25
|\
| * PrimeFieldTheorems fermat inverse lemma: prove admitGravatar Andres Erbsen2016-05-24
| |
* | First stage of canonicalization proofs complete; proved 3 carry loops reduce ↵Gravatar jadep2016-05-20
| | | | | | | | input digits to their minimal widths. Remaining : name fixes and second stage -- proving that we subtract q iff the reduced input is over q (in the range [2^k-c, 2^k-1])
| * F: pow_nat_iter_op_correctGravatar Andres Erbsen2016-05-18
| |
| * F: fermat inversion lemma refactorGravatar Andres Erbsen2016-05-18
|/
* Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid ↵Gravatar jadep2016-05-09
| | | | unsigned integer underflow. Also changed rep in Specific proofs so that it is PseudoMersenneBaseRep.rep rather than ModularBaseSystem.rep; these are equivalent but the first is the abstraction level we want.
* Cleanup: mostly moving lemmas to Util files, some moving lemmas to more ↵Gravatar jadep2016-04-28
| | | | general contexts.
* refactor field lemmas out of ed25519Gravatar Andres Erbsen2016-04-25
|
* automated most of the code in GF25519Gravatar jadep2016-04-21
|
* Cleanup of GF25519Gravatar jadep2016-04-20
|
* Pulled generalized code out of GF25519 so that it can be used for other moduliGravatar jadep2016-04-20
|
* moved lemmas from ModularBaseSystemProofs to various Util filesGravatar jadep2016-04-20
|
* Add a tactic for field inequalitiesGravatar Jason Gross2016-04-19
| | | | | Pair programming with Andres, a better proof of unifiedAddM1'_rep, some progress on twistedAddAssoc.
* Merge and refactor of GF25519Gravatar jadep2016-04-11
|
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-03-30
|\
| * Ed25519: d is nonsquareGravatar Andres Erbsen2016-03-20
| |
* | made BaseVector instance globalGravatar Jade Philipoom2016-03-20
| |
* | refactor of Basesystem and ModularBaseSystem; includes general code ↵Gravatar Jade Philipoom2016-03-20
| | | | | | | | organization and changes to pseudomersenne base parameters that require bases to be expressed as powers of 2, which reduces the burden of proof on the caller and allows carry functions to use bitwise operations rather than mod and division
* | Refactored BaseSystem and ModularBaseSystem.Gravatar Jade Philipoom2016-03-11
| |
| * 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 ```
| * Use [rewrite] rather than [change] to speed up QedGravatar Jason Gross2016-03-08
|/ | | | | | | | | | | | | [Opaque] tells kernel unification to defer unfolding a constant as long as possible. This is not a problem for [change], when the functions are small and directly convertible. It's disastrous for [Qed]/[Defined], which (if I understand correctly) try to unify [Opaquemul x' y'] with [mul x y] by fully unfolding [mul] and [x] and [y] before trying to unfold [Opaquemul]; when [x] and [y] are large, this takes a very long time. Rewrite avoids this by telling Coq *how* to unify [Opaquemul x' y'] with [mul x y] (namely, by unifying [Opaquemul] with [mul], and then [x] with [x'] and [y] with [y']).
* CompleteEdwardsCurveTheorems: associativity proof that times out on QedGravatar Andres Erbsen2016-03-03
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 12:30:29 +0000