aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Collapse)AuthorAge
* Update _CoqProjectGravatar Jason Gross2016-06-23
|
* Remove vestigal BoundedWord machineryGravatar Robert Sloan2016-06-23
|
* Update _CoqProjectGravatar Robert Sloan2016-06-23
|
* Remove unstable Pipeline.v examples from _CoqProjectGravatar Robert Sloan2016-06-23
|
* Add Language.v, Conversion.v to _CoqProjectGravatar Robert Sloan2016-06-23
|
* Add Pseudize, Vectorize, Wordize to the build processGravatar Robert Sloan2016-06-22
|
* Merge with public masterGravatar Robert Sloan2016-06-22
|\
| * Aggregate all level specifications not in Spec/*Gravatar Jason Gross2016-06-22
| | | | | | | | | | This prevents notation conflicts (see comment in Notations.v for more explanation).
| * Update _CoqProjectGravatar Jason Gross2016-06-22
| |
* | Merge with plv/masterGravatar Robert Sloan2016-06-22
|\|
| * move nsatz into tactics directoryGravatar Andres Erbsen2016-06-20
| |
| * remove obsolete rep mechanismGravatar Andres Erbsen2016-06-20
| |
| * Remove anything incompatible with new algebraic hierarcyGravatar Andres Erbsen2016-06-20
| | | | | | | | | | | | - 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
| * Merge branch 'field-experiment'Gravatar Andres Erbsen2016-06-20
| |\ | | | | | | | | | includes broken files to be removed in next commit
| | * tuple toolingGravatar Andres Erbsen2016-06-20
| | |
| | * port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try ↵Gravatar Andres Erbsen2016-06-18
| | | | | | | | | | | | fewer nonzero ports. remove FField and FNsatz
| | * move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheoremsGravatar Andres Erbsen2016-06-17
| | |
| | * nsatz: reimplement, integrate, demonstrateGravatar Andres Erbsen2016-06-15
| | |
| | * [field] and [nsatz] do things now againGravatar Andres Erbsen2016-06-14
| | |
| * | Add coqprime that works with 8.5, bundle bedrockGravatar Jason Gross2016-06-10
| | | | | | | | | | | | | | | | | | This simplifes the build process, and also allows us to try to build with 8.5. We autodetect the version of Coq in the Makefile to decide which version of coqprime to build.
| | * generic field definitionGravatar Andres Erbsen2016-06-07
| |/
* | Meshing Assembly machinery into the MakefileGravatar Robert Sloan2016-06-06
| |
* | merging with masterGravatar Robert Sloan2016-06-06
|\|
* | merging with masterGravatar Robert Sloan2016-06-06
|\ \
* | | PseudoMedialConversion doneGravatar Robert Sloan2016-05-31
| | |
| | * F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more ↵Gravatar Andres Erbsen2016-05-24
| | | | | | | | | | | | broken...
| | * Completed encoding reorganization; factored sign_bit out of PointEncodings ↵Gravatar jadep2016-04-28
| | | | | | | | | | | | and finished encoding admits.
| | * Reorganization and revision of Encoding code and redefinition of sign_bit ↵Gravatar jadep2016-04-25
| | | | | | | | | | | | function.
| | * added GF1305 (modulus is 2^130 - 5, base has length 5 with all digits having ↵Gravatar jadep2016-04-21
| | | | | | | | | | | | weight 2^26)
| | * Pulled generalized code out of GF25519 so that it can be used for other moduliGravatar jadep2016-04-20
| | |
| | * 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.
| | | * Add a tactic for field inequalitiesGravatar Jason Gross2016-04-19
| | | | | | | | | | | | | | | | | | | | Pair programming with Andres, a better proof of unifiedAddM1'_rep, some progress on twistedAddAssoc.
| | * | Removed old iter_op version and its last dependency.Gravatar jadep2016-04-15
| | |/
* | | Breaking out State into its own fileGravatar Robert Sloan2016-04-04
| | |
| | * Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-03-30
| | |\
* | | | add Assembly to CoqProjectGravatar Robert Sloan2016-03-29
| | | |
* | | | merge with plv/masterGravatar Robert Sloan2016-03-29
| |_|/ |/| |
* | | state top-level derivation for Ed25519.verifyGravatar Andres Erbsen2016-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
* | CompleteEdwardsCurveTheorems: associativity proof that times out on QedGravatar Andres Erbsen2016-03-03
| |
* | ModularArithmetic: [field] tactic that respects opacity, prettify ↵Gravatar Andres Erbsen2016-02-28
| | | | | | | | ExtendedCoordinates, outline Edwards curve associativity
* | generic binary exponentiation correctness proof in 3 one-linersGravatar 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.
* proved most of point encoding admits, fixed some build system issues (dead ↵Gravatar Jade Philipoom2016-02-16
| | | | imports of PointFormats and Galois things)
* added point encodings; some admits remainGravatar Jade Philipoom2016-02-16
|
* fixed renamed files and added imports for encodingsGravatar Jade Philipoom2016-02-15
|
* mergeGravatar Jade Philipoom2016-02-15
|\
* | added generic encoding specGravatar Jade Philipoom2016-02-15
| |
| * Finish seperating our specs: remove old non-specified codeGravatar Andres Erbsen2016-02-15
|/
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 18:59:48 +0000