index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
Commit message (
Expand
)
Author
Age
*
Factor out some of the preglue synthesis code
Jason Gross
2017-07-08
*
Unfold tuple arguments in reflective pipeline
Jason Gross
2017-07-08
*
Add cbv_runtime in Arithmetic/Core
Jason Gross
2017-07-08
*
Make some tactics a bit more powerful
Jason Gross
2017-07-08
*
Fix Demo.v
Jason Gross
2017-07-08
*
More fine-grained tactics imports
Jason Gross
2017-07-08
*
More fine-grained imports
Jason Gross
2017-07-08
*
Add UnfoldArg
Jason Gross
2017-07-08
*
Fix CSE_sym denote
Jason Gross
2017-07-07
*
Fix proofs broken by previous commit
Jason Gross
2017-07-07
*
Stronger contexts
Jason Gross
2017-07-07
*
Remove some admitted lemmas
Jason Gross
2017-07-07
*
enforce use of [F.zero], [F.one]; prove Ed25519 admits
Andres Erbsen
2017-07-07
*
prove ModularArithmeticTheorems admits
Andres Erbsen
2017-07-06
*
Curves/Edwards/Affine: prove point compression admits
Andres Erbsen
2017-07-06
*
prove an admit in ArithmeticSynthesisTest
Andres Erbsen
2017-07-06
*
make bench
Andres Erbsen
2017-07-06
*
make bench
Jason Gross
2017-07-06
*
Fix a typo that ends up not mattering
Jason Gross
2017-07-06
*
benchmark NISTZ256 with and without adx
Andres Erbsen
2017-07-05
*
make bench
Andres Erbsen
2017-07-05
*
make bench
Andres Erbsen
2017-07-04
*
use att style assembly with icc, test it
Andres Erbsen
2017-07-04
*
test p256 mixed addition
Andres Erbsen
2017-07-04
*
work around GCC issues 81294 and 81300
Andres Erbsen
2017-07-03
*
fix mulx argument order using sed, test feadd, femul (fails due to #234)
Andres Erbsen
2017-07-03
*
Fix a mis-aligned comment marker in CNotations script
Jason Gross
2017-07-03
*
Fix display target
Jason Gross
2017-07-03
*
X25519 test (passed on first try)
Andres Erbsen
2017-07-02
*
automate P256 integration
Andres Erbsen
2017-07-02
*
Merge branch 'use-cmovznz' of https://github.com/JasonGross/fiat-crypto
Andres Erbsen
2017-07-02
|
\
*
|
Closed under the global context
Andres Erbsen
2017-07-02
*
|
prove [MontgomeryAPI.small_add]
Andres Erbsen
2017-07-02
*
|
fix [small_div] arguments
Andres Erbsen
2017-07-02
*
|
[small] admits progress...
Andres Erbsen
2017-07-01
*
|
make display
Andres Erbsen
2017-07-01
*
|
proved small_sat_add
jadep
2017-07-01
*
|
changes to log files after running make c
jadep
2017-07-01
*
|
change opp to runtime_opp
jadep
2017-07-01
*
|
proved remaining [eval] admits in MontgomeryAPI
jadep
2017-07-01
*
|
Prove saturated carrying-subtraction-chain correct
jadep
2017-07-01
*
|
Prove saturated carrying-addition-chain correct
jadep
2017-06-30
*
|
add missing import
jadep
2017-06-30
*
|
Fix misnamed references in Specific/ (broke after saturated arithetic reorg)
jadep
2017-06-30
*
|
Reorganization of saturated arithmetic
jadep
2017-06-29
*
|
create directory for saturated arithmetic in preparation for splitting into m...
jadep
2017-06-29
*
|
Merge branch 'addsubchains'
jadep
2017-06-29
|
\
\
|
*
|
Remove a [Check]
Jason Gross
2017-06-29
*
|
|
new add/carry chain logic with admitted proofs
jadep
2017-06-29
*
|
|
Skeleton for add/subtract chains (see #222)
jadep
2017-06-29
[next]