aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Work around bad design in CoqGravatar Jason Gross2016-07-19
* Add a distr_length databaseGravatar Jason Gross2016-07-19
* Remove stuff from PseudoMersenneBaseParamProofs.vGravatar Jason Gross2016-07-19
* {base} -> baseGravatar Jason Gross2016-07-19
* Move two_k_nonzero to PseudoMersenneBaseParamProofs.vGravatar Jason Gross2016-07-19
* Fix side-condition from previous commitGravatar Jason Gross2016-07-19
* Add another lemma to distr_lengthGravatar Jason Gross2016-07-19
* Use update_nth in add_to_nth (#26)Gravatar Jason Gross2016-07-19
* ext_base: now defined in terms of ext_limb_widthsGravatar Jason Gross2016-07-18
* Add a lemma about base_from_limb_widths and appGravatar Jason Gross2016-07-18
* Add a lemma about sum_firstnGravatar Jason Gross2016-07-18
* Add a ListUtil lemmaGravatar Jason Gross2016-07-18
* Move more proofs earlierGravatar Jason Gross2016-07-18
* Make Pow2BaseProofs independent of the def of add_to_nthGravatar Jason Gross2016-07-18
* Silence a warningGravatar Jason Gross2016-07-18
* Express carry_simple in terms of carry_genGravatar Jason Gross2016-07-18
* Fix for Coq 8.4 (missing lemmas)Gravatar Jason Gross2016-07-18
* Fix for Coq 8.4 (omega used to be weaker)Gravatar Jason Gross2016-07-18
* Add more distr_length proofs in BaseSystemProofsGravatar Jason Gross2016-07-18
* Add more natsimplify le_dec lemmasGravatar Jason Gross2016-07-18
* Add more NatUtil lemmasGravatar Jason Gross2016-07-18
* Add natsimplify lemmas about eq_nat_decGravatar Jason Gross2016-07-18
* Fix some typos in the previous commitGravatar Jason Gross2016-07-18
* Add some lemmas about nth_default in boundsGravatar Jason Gross2016-07-18
* Remove a nested proofGravatar Jason Gross2016-07-18
* Move some definitions to Pow2Base (#24)Gravatar Jason Gross2016-07-18
* ported IterAssocOp to use monoid rather than a billion context variables that...Gravatar jadep2016-07-18
* rewrote Testbit and factored out some necessary lemmas about 'uniform' bases ...Gravatar jadep2016-07-18
* Added lemmas to ZUtil and NatUtil (for Testbit)Gravatar jadep2016-07-18
* Fixed unsimplified multiplication definitions in Specific by separating out t...Gravatar jadep2016-07-18
* Merge branch 'master' of github.com:mit-plv/fiat-cryptoGravatar jadep2016-07-15
|\
* | proved an admit in field homomorphisms that turned out to be unprovable; I ad...Gravatar jadep2016-07-15
* | more changes to Specific for 8.4 compatibilityGravatar jadep2016-07-15
| * Experiments/SpecificCurve25519.v: curve25519 addition using small Z-sGravatar Andres Erbsen2016-07-13
| * tuple: applying functions to tuples of arbitrary lengthGravatar Andres Erbsen2016-07-12
|/
* re-cleaned operations in Specific and updated GF25519 to match GF1305Gravatar jadep2016-07-12
* cleaned Specific operations so they produce code without proof terms, and pro...Gravatar jadep2016-07-12
* removing experimental file accidentally included in last commitGravatar jadep2016-07-12
* pushing through a tweak to the arguments of [sub], and defining a field over ...Gravatar jadep2016-07-12
* prove that if something is isomorphic to a field, it is a fieldGravatar jadep2016-07-11
* Make [base] and [log_cap] notationsGravatar Jason Gross2016-07-11
* Merge of fixedlength and masterGravatar jadep2016-07-11
|\
* | ported Specific files to use ModularBaseSystemInterfaceGravatar jadep2016-07-11
| * s/conservative_common_denominator/common_denominator/gGravatar Andres Erbsen2016-07-11
| * rename [common_denominator] to [field_simplify_if_div]Gravatar Andres Erbsen2016-07-11
| * remove field_algebraGravatar Andres Erbsen2016-07-11
| * port CompleteEdwardsCurveTheorems (builds again)Gravatar Andres Erbsen2016-07-11
| * pose proof fails where specialize works (typeclass resolution / unification?)Gravatar Andres Erbsen2016-07-11
| * wrap nsatz in AlgebraGravatar Andres Erbsen2016-07-11
| * [congruence] is more powerful in 8.5 than in 8.4Gravatar Andres Erbsen2016-07-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 22:26:32 +0000