aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
* Add fraction inequality reasoning tactics to ZUtilGravatar Jason Gross2016-07-01
* Add a proof of 2 * x - x = xGravatar Jason Gross2016-06-30
* Add a classification of n / m < 0Gravatar Jason Gross2016-06-30
* Add a tactic for making use of destructed <? in ZGravatar Jason Gross2016-06-30
* Prove that a ^ k <> 0Gravatar Jason Gross2016-06-30
* Add pow_Zpow to Util.ZUtilGravatar Jason Gross2016-06-30
* Fix field_algebra in 8.4Gravatar Jason Gross2016-06-28
* Fix super_nsatz tactic to be better about orderingGravatar Jason Gross2016-06-28
* Tuple: from_list_to_listGravatar Andres Erbsen2016-06-28
* Add [destruct_head] tacticsGravatar Jason Gross2016-06-27
* Add [break_match] for hypothesesGravatar Jason Gross2016-06-27
* Add decidable instances for sumwise and fieldwiseGravatar Jason Gross2016-06-27
* Add a tactic for dealing with equalities of [sum]Gravatar Jason Gross2016-06-27
* EdDSA: prove things about specGravatar Andres Erbsen2016-06-25
* Various nsatz and field tactic improvementsGravatar Jason Gross2016-06-24
* Use Decidable machinery for is_eq_decGravatar Jason Gross2016-06-24
* Add Unit.vGravatar Jason Gross2016-06-23
* Add equality on sum typesGravatar Jason Gross2016-06-23
* Improve some tactics and lemmasGravatar Jason Gross2016-06-23
* [break_match] should not be localGravatar Jason Gross2016-06-23
* Add tactics to Tactics, at most 2 sq-roots to AlgebraGravatar Jason Gross2016-06-23
* Fix broken notations (hopefully)Gravatar Jason Gross2016-06-22
* Fix missing notationsGravatar Jason Gross2016-06-22
* Aggregate all level specifications not in Spec/*Gravatar Jason Gross2016-06-22
* Fix for broken abstractGravatar Jason Gross2016-06-22
* Add decidability util fileGravatar Jason Gross2016-06-22
* remove trailing whitespace from src/Gravatar Andres Erbsen2016-06-20
* Variosu 8.5 fixesGravatar Jason Gross2016-06-20
* Merge branch 'field-experiment'Gravatar Andres Erbsen2016-06-20
|\
| * tuple toolingGravatar Andres Erbsen2016-06-20
| * port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try fewer...Gravatar Andres Erbsen2016-06-18
* | MergeGravatar jadep2016-06-14
|\ \
* | | Finished admits for canonicalization proofs.Gravatar jadep2016-06-14
* | | progress on second stage (conditional constant-time subtraction) of canonical...Gravatar jadep2016-06-13
| * | Fix for Coq 8.4pl2Gravatar Jason Gross2016-06-11
* | | starting rewrite using different definition of mapGravatar jadep2016-06-11
| |/ |/|
| * 8.5 fixesGravatar Jason Gross2016-06-10
|/
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-05-25
|\
| * Remove unfolding, rewrite -> setoid_rewriteGravatar Jason Gross2016-05-24
* | First stage of canonicalization proofs complete; proved 3 carry loops reduce ...Gravatar jadep2016-05-20
|/
* Proved decode_point_eq in Ed25519 (comparing encodings is equivalent toGravatar jadep2016-04-29
* Cleanup: mostly moving lemmas to Util files, some moving lemmas to more gener...Gravatar jadep2016-04-28
* Cleanup of GF25519Gravatar jadep2016-04-20
* moved lemmas from ModularBaseSystemProofs to various Util filesGravatar jadep2016-04-20
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-04-19
|\
* | Added lemmas to Util/ that are needed for testbit.Gravatar jadep2016-04-19
| * Add a tactic for field inequalitiesGravatar Jason Gross2016-04-19
|/
* Retrieved updated version of Util/IterAssocOp and modified ExtendedCoordinate...Gravatar jadep2016-04-14
* Reverting Util/IterAssocOp to an earlier version for compatibility with Compl...Gravatar jadep2016-04-12
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-03-30
|\
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 23:18:33 +0000