aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Add decidable equality with nilGravatar Jason Gross2017-08-13
* Factor out some of the preglue synthesis codeGravatar Jason Gross2017-07-08
* Unfold tuple arguments in reflective pipelineGravatar Jason Gross2017-07-08
* Add cbv_runtime in Arithmetic/CoreGravatar Jason Gross2017-07-08
* Make some tactics a bit more powerfulGravatar Jason Gross2017-07-08
* Fix Demo.vGravatar Jason Gross2017-07-08
* More fine-grained tactics importsGravatar Jason Gross2017-07-08
* More fine-grained importsGravatar Jason Gross2017-07-08
* Add UnfoldArgGravatar Jason Gross2017-07-08
* Fix CSE_sym denoteGravatar Jason Gross2017-07-07
* Fix proofs broken by previous commitGravatar Jason Gross2017-07-07
* Stronger contextsGravatar Jason Gross2017-07-07
* Remove some admitted lemmasGravatar Jason Gross2017-07-07
* enforce use of [F.zero], [F.one]; prove Ed25519 admitsGravatar Andres Erbsen2017-07-07
* prove ModularArithmeticTheorems admitsGravatar Andres Erbsen2017-07-06
* Curves/Edwards/Affine: prove point compression admitsGravatar Andres Erbsen2017-07-06
* prove an admit in ArithmeticSynthesisTestGravatar Andres Erbsen2017-07-06
* make benchGravatar Andres Erbsen2017-07-06
* make benchGravatar Jason Gross2017-07-06
* Fix a typo that ends up not matteringGravatar Jason Gross2017-07-06
* benchmark NISTZ256 with and without adxGravatar Andres Erbsen2017-07-05
* make benchGravatar Andres Erbsen2017-07-05
* make benchGravatar Andres Erbsen2017-07-04
* use att style assembly with icc, test itGravatar Andres Erbsen2017-07-04
* test p256 mixed additionGravatar Andres Erbsen2017-07-04
* work around GCC issues 81294 and 81300Gravatar Andres Erbsen2017-07-03
* fix mulx argument order using sed, test feadd, femul (fails due to #234)Gravatar Andres Erbsen2017-07-03
* Fix a mis-aligned comment marker in CNotations scriptGravatar Jason Gross2017-07-03
* Fix display targetGravatar Jason Gross2017-07-03
* X25519 test (passed on first try)Gravatar Andres Erbsen2017-07-02
* automate P256 integrationGravatar Andres Erbsen2017-07-02
* Merge branch 'use-cmovznz' of https://github.com/JasonGross/fiat-cryptoGravatar Andres Erbsen2017-07-02
|\
* | Closed under the global contextGravatar Andres Erbsen2017-07-02
* | prove [MontgomeryAPI.small_add]Gravatar Andres Erbsen2017-07-02
* | fix [small_div] argumentsGravatar Andres Erbsen2017-07-02
* | [small] admits progress...Gravatar Andres Erbsen2017-07-01
* | make displayGravatar Andres Erbsen2017-07-01
* | proved small_sat_addGravatar jadep2017-07-01
* | changes to log files after running make cGravatar jadep2017-07-01
* | change opp to runtime_oppGravatar jadep2017-07-01
* | proved remaining [eval] admits in MontgomeryAPIGravatar jadep2017-07-01
* | Prove saturated carrying-subtraction-chain correctGravatar jadep2017-07-01
* | Prove saturated carrying-addition-chain correctGravatar jadep2017-06-30
* | add missing importGravatar jadep2017-06-30
* | Fix misnamed references in Specific/ (broke after saturated arithetic reorg)Gravatar jadep2017-06-30
* | Reorganization of saturated arithmeticGravatar jadep2017-06-29
* | create directory for saturated arithmetic in preparation for splitting into m...Gravatar jadep2017-06-29
* | Merge branch 'addsubchains'Gravatar jadep2017-06-29
|\ \
| * | Remove a [Check]Gravatar Jason Gross2017-06-29
* | | new add/carry chain logic with admitted proofsGravatar jadep2017-06-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 21:26:36 +0000