aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
...
| * | 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
* | | | stuck trying to figure out dependently typed continuation passing styleGravatar Andres Erbsen2016-07-06
* | | | add new interface to ModularBaseSystemGravatar Andres Erbsen2016-07-03
* | | | Tuple: lift functions from lists to tuplesGravatar Andres Erbsen2016-07-03
* | | | remove PseudoMersenneRepGravatar Andres Erbsen2016-07-03
| | | * 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
| | | * Merge pull request #19 from JasonGross/rename-z-lemmasGravatar Jason Gross2016-07-03
| | | |\
| | | * \ Merge pull request #12 from mit-plv/licenseGravatar Andres Erbsen2016-07-02
| | | |\ \
| | | | | * 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 more caches to .gitignore (nra, csdp)Gravatar Jason Gross2016-07-01
* | | | Add fraction inequality reasoning tactics to ZUtilGravatar Jason Gross2016-07-01
* | | | Update .gitignore with lia, nia cachesGravatar 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
* | | | Update crypto-defects.mdGravatar Andres Erbsen2016-06-29
* | | | Update crypto-defects.mdGravatar Andres Erbsen2016-06-29
* | | | Update crypto-defects.mdGravatar Andres Erbsen2016-06-29
* | | | Update crypto-defects.mdGravatar Andres Erbsen2016-06-29
* | | | Update crypto-defects.mdGravatar Andres Erbsen2016-06-29
* | | | Update crypto-defects.mdGravatar Andres Erbsen2016-06-29
* | | | Update crypto-defects.mdGravatar Andres Erbsen2016-06-29
| * | | encode operation in ModularBaseSystem now uses bitwise operators, taking adva...Gravatar jadep2016-06-29
* | | | Update crypto-defects.mdGravatar Andres Erbsen2016-06-29
* | | | Update crypto-defects.mdGravatar Andres Erbsen2016-06-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-14 06:57:48 +0000