aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Fix for broken 8.5 build in ListUtilGravatar Jason Gross2016-07-06
* fixed indentation for new lemmas in ZUtilGravatar jadep2016-07-06
* Merged changes, including new ZUtil conventions.Gravatar jadep2016-07-06
|\
* \ Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-07-06
|\ \
* | | Factored out some proofs that rely only on base being powers of two, and defi...Gravatar jadep2016-07-06
| | * Define the spec of Weierstrass curves (#6)Gravatar Jason Gross2016-07-03
| | * Implement and prove Barrett reduction on Z (#18)Gravatar Jason Gross2016-07-03
| | * Indentation in ZUtilGravatar Jason Gross2016-07-02
| | * Make ZUtil more uniformGravatar Jason Gross2016-07-02
| | * super_nsatz: Handle x^2 = y^2 -> x <> -y -> x = yGravatar Jason Gross2016-07-02
| | * Fix for 8.4 evarsGravatar Jason Gross2016-07-01
| | * Add ZUtil hintsGravatar Jason Gross2016-07-01
| | * Add more hints to ZUtilGravatar Jason Gross2016-07-01
| | * Add more hints in ZUtilGravatar Jason Gross2016-07-01
| | * Add more ZUtil hintsGravatar Jason Gross2016-07-01
| | * Add more hints to ZUtilGravatar Jason Gross2016-07-01
| | * Simplify a proof that no longer needs more hintsGravatar Jason Gross2016-07-01
| | * Add hint databases and a proof about Z.log2Gravatar Jason Gross2016-07-01
| | * Add some proofs about Z.div and Z.mulGravatar Jason Gross2016-07-01
| | * Add [specialize_by] tacticGravatar Jason Gross2016-07-01
| | * Fix a typo in Zsplit_sumsGravatar Jason Gross2016-07-01
| | * Add tactic to split sums and differences in inequalitiesGravatar Jason Gross2016-07-01
| | * 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
* | | added and proved shift/or decode operation 'decode_bitwise'Gravatar jadep2016-06-30
| | * Add pow_Zpow to Util.ZUtilGravatar Jason Gross2016-06-30
| | * Simplify conservative_common_denominatorGravatar Jason Gross2016-06-29
| | * Don't generate goals [False] in conservative_common_denominator_allGravatar Jason Gross2016-06-29
| | * Fix [only_two_square_roots] to not loopGravatar Jason Gross2016-06-29
| | * Allow side-conditions in common denom. all in hypsGravatar Jason Gross2016-06-29
| | * Handle fractions in denominatorsGravatar Jason Gross2016-06-29
| | * Clear symmetric duplicates in clear_algebraic_duplicatesGravatar Jason Gross2016-06-29
* | | encode operation in ModularBaseSystem now uses bitwise operators, taking adva...Gravatar jadep2016-06-29
* | | BaseSystem encode function is no longer naive; it does a mod/div loop rather ...Gravatar jadep2016-06-28
| | * Fix a typo in the previous commitGravatar Jason Gross2016-06-28
| | * [super_nstaz]: Handle side-conditions from [nsatz]Gravatar Jason Gross2016-06-28
| |/
| * Revert "CompleteEdwardsCurveTheorems: build on 8.4 after field_algebra cahnge"Gravatar Andres Erbsen2016-06-28
| * No more anomalies from super_nsatz, hopefullyGravatar Jason Gross2016-06-28
| * Fix field_algebra in 8.4Gravatar Jason Gross2016-06-28
| * CompleteEdwardsCurveTheorems: build on 8.4 after field_algebra cahngeGravatar Andres Erbsen2016-06-28
| * Fix a typo (missing .)Gravatar Jason Gross2016-06-28
| * Fix super_nsatz tactic to be better about orderingGravatar Jason Gross2016-06-28
| * EdDSARefinement: work around rewrite_strat for 8.4Gravatar Andres Erbsen2016-06-28
| * Tuple: from_list_to_listGravatar Andres Erbsen2016-06-28
| * Try a faster way of solving some inequalities resulting from common_denominatorGravatar Jason Gross2016-06-27
| * Actual fix for super_nsatzGravatar Jason Gross2016-06-27
| * Fix super_nstaz to not errorGravatar Jason Gross2016-06-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 10:32:32 +0000