aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-04-19
|\
* | Defined a testbit variant for BaseSystem vectors and proved equivalence to ↵Gravatar jadep2016-04-19
| | | | | | | | Z.testbit.
* | Added lemmas to Util/ that are needed for testbit.Gravatar jadep2016-04-19
| |
| * Add a tactic for field inequalitiesGravatar Jason Gross2016-04-19
| | | | | | | | | | Pair programming with Andres, a better proof of unifiedAddM1'_rep, some progress on twistedAddAssoc.
| * ed25519 derivation: down to final encodingGravatar Andres Erbsen2016-04-17
| |
| * ed25519 derivation: use representation of FGravatar Andres Erbsen2016-04-17
| |
| * ed25519 derivation: wrangle non-unique representationsGravatar Andres Erbsen2016-04-16
| |
| * ed25519 derivation: stuck at main loopGravatar Andres Erbsen2016-04-16
| |
| * ed25519 derivation down to word until main equationGravatar Andres Erbsen2016-04-16
| |
* | Cleaned up and revised DoubleAndAdd.Gravatar jadep2016-04-15
| |
* | Removed old iter_op version and its last dependency.Gravatar jadep2016-04-15
|/
* Retrieved updated version of Util/IterAssocOp and modified ↵Gravatar jadep2016-04-14
| | | | ExtendedCoordinates and Ed25519 to use it.
* Fixed syntax error (missing bracket) in Ed25519 to make merge buildGravatar jadep2016-04-12
|
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-04-12
|\
* | Finished refactor of GF25519 (partial evaluation); code builds but needs to ↵Gravatar jadep2016-04-12
| | | | | | | | be reorganized, since many of the theorems in GF25519 are now generalized and do not need to be in Specific/.
* | Reverting Util/IterAssocOp to an earlier version for compatibility with ↵Gravatar jadep2016-04-12
| | | | | | | | CompleteEdwardsCurve/ExtendedCoordinates (we don't have testbit defined yet)
* | Merge and refactor of GF25519Gravatar jadep2016-04-11
| |
| * ed25519: continue derivationGravatar Andres Erbsen2016-04-08
| |
* | Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-03-30
|\|
| * Drop second projections in Ed25519Gravatar Jason Gross2016-03-29
| |
| * ed25519 derivation: pair programming with jgross... slow progressGravatar Andres Erbsen2016-03-24
| |
| * nicer verify() derivation starterGravatar Andres Erbsen2016-03-21
| |
| * state top-level derivation for Ed25519.verifyGravatar Andres Erbsen2016-03-20
| |
| * instantiate ed25519 sign in specGravatar Andres Erbsen2016-03-20
| |
| * Ed25519: d is nonsquareGravatar Andres Erbsen2016-03-20
| |
* | fix of GF25519 in progress; created instantiation of PseudoMersenneBaseParamsGravatar Jade Philipoom2016-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
| * extended coordinates setoid boilerplateGravatar Andres Erbsen2016-03-20
| |
* | 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 ```
| * Remove [Admitted]; [Qed] is now under a secondGravatar Jason Gross2016-03-08
| |
| * 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']).
* | IterAssocOp: now uses arbitrary representation of scalar that implements testbitGravatar Jade Philipoom2016-03-08
| |
* | IterAssocOp : now takes a bound argument instead of just using size of exponentGravatar Jade Philipoom2016-03-07
|/
* IterAssocOp : proved iter_op with function exponentialGravatar Jade Philipoom2016-03-03
|
* tweak to NumTheoryUtil so it builds on older Coq versionsGravatar Jade Philipoom2016-03-03
|
* CompleteEdwardsCurveTheorems: associativity proof that times out on QedGravatar Andres Erbsen2016-03-03
|
* Instance Fq_Integral_domain : @Integral_domain (F q) ...Gravatar Andres Erbsen2016-02-28
|
* ModularArithmetic: [field] tactic that respects opacity, prettify ↵Gravatar Andres Erbsen2016-02-28
| | | | ExtendedCoordinates, outline Edwards curve associativity
* Makefile: single-quotes for shell globbingGravatar Andres Erbsen2016-02-28
|
* generic binary exponentiation correctness proof in 3 one-linersGravatar Andres Erbsen2016-02-26
|
* ModularArithmetic: reasonable-time FieldToZ inv implementationGravatar Andres Erbsen2016-02-26
|
* Factor out some bedrock dependencies into WordUtilGravatar Jason Gross2016-02-25
| | | | Also move a definition about words, with a TODO about location, into WordUtil.
* cleanup of bounded iter_opGravatar Jade Philipoom2016-02-25
|
* efficient powmodGravatar Andres Erbsen2016-02-17
|
* update ModularArithmetic tutorialGravatar Andres Erbsen2016-02-17
|
* removed Print AssumptionsGravatar Jade Philipoom2016-02-16
|
* proved sqrt_solutions, the last remaining admit for point encodingsGravatar Jade Philipoom2016-02-16
|
* moved some theorems requiring q mod 8 = 5 precondition to PointEncoding from ↵Gravatar Jade Philipoom2016-02-16
| | | | CompleteEdwardsCurve, where the precondition is not in scope.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 17:19:39 +0000