aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* proved eval_drop_highGravatar jadep2017-06-18
* define strong small and re-prove small_add and small_compact with that defini...Gravatar jadep2017-06-18
* make scmul discard its carry in a saner way; rather than concatenating it in ...Gravatar jadep2017-06-18
* make display with new constantsGravatar Jason Gross2017-06-18
* make displayGravatar Jason Gross2017-06-18
* Add notationsGravatar Jason Gross2017-06-18
* make displayGravatar Jason Gross2017-06-18
* Adding more (possibly unneeded) simplificationGravatar Jason Gross2017-06-18
* Use uint128_t for 128-bit montgomeryGravatar Jason Gross2017-06-17
* make displayGravatar Jason Gross2017-06-17
* add 128-bit display fileGravatar Jason Gross2017-06-17
* Add 128-bit version of montgomery for testingGravatar Jason Gross2017-06-17
* make displayGravatar Jason Gross2017-06-17
* Try more simplificationGravatar Jason Gross2017-06-17
* make displayGravatar Jason Gross2017-06-17
* Drop the 0-carry bit before bounds analysisGravatar Jason Gross2017-06-17
* make displayGravatar Jason Gross2017-06-17
* Be a bit more forceful in eliminating zeros in arith simplGravatar Jason Gross2017-06-17
* Add eq_ZToWordGravatar Jason Gross2017-06-17
* More arithmetic simplification for adc, mulGravatar Jason Gross2017-06-17
* make displayGravatar Jason Gross2017-06-17
* Remove a PrintGravatar Jason Gross2017-06-17
* Fix scmul bounds issueGravatar jadep2017-06-17
* More eye-catching naming scheme for nm in saturatedGravatar Jason Gross2017-06-17
* make displayGravatar Jason Gross2017-06-17
* Add more simplification to pipelineGravatar Jason Gross2017-06-17
* make displayGravatar Jason Gross2017-06-17
* Make use of non-uniform tuple-based addGravatar Jason Gross2017-06-17
* make displayGravatar Jason Gross2017-06-17
* Enable profiling in integration test mont 256Gravatar Jason Gross2017-06-17
* Add linearization to inline pairs in post-bounds pipelineGravatar Jason Gross2017-06-17
* make displayGravatar Jason Gross2017-06-17
* Add extra simplification to simplifier for adcGravatar Jason Gross2017-06-17
* Make displayGravatar Jason Gross2017-06-17
* Add more constantsGravatar Jason Gross2017-06-17
* Unfold Z.mul_split_at_bitwidth for reificationGravatar Jason Gross2017-06-17
* Don't make curves proofs on travis (hopefully fast enough build)Gravatar Jason Gross2017-06-17
* Make displayGravatar Jason Gross2017-06-17
* Add some more display constantsGravatar Jason Gross2017-06-17
* Add bool into P256Gravatar Jason Gross2017-06-17
* make displayGravatar Jason Gross2017-06-17
* Finish MontgomeryP256 (less conditional subtract)Gravatar Jason Gross2017-06-17
* Remove fails; if we fail too strongly, we miss debugging informationGravatar Jason Gross2017-06-17
* Try to fail a bit faster in bad reificationGravatar Jason Gross2017-06-17
* Add back failure at level 100Gravatar Jason Gross2017-06-17
* Better error messages in reificationGravatar Jason Gross2017-06-17
* Add initial IntegrationTestMontgomeryP256.vGravatar Jason Gross2017-06-17
* Better reification tactic debuggingGravatar Jason Gross2017-06-17
* Fix a typoGravatar Jason Gross2017-06-17
* Define m in p256Gravatar Jason Gross2017-06-17