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
*
Prettier json file generation
Jason Gross
2017-10-14
*
Add generated json files from generate_parameters.py
Jason Gross
2017-10-14
*
Add curve-specific json files
Jason Gross
2017-10-14
*
Add SmartFlatTypeMap_Pair
Jason Gross
2017-10-14
*
Fix a bug in CommonSubexpressionEliminationProperties.v
Jason Gross
2017-10-13
*
Add pow_ceil_mul_nat_divide_upperbound
Jason Gross
2017-10-13
*
Add some SmartMap tuple lemmas
Jason Gross
2017-10-13
*
Fix a spelling error
Jason Gross
2017-10-13
*
Factor out truncation_bounds
Jason Gross
2017-10-13
*
Add comment to Compilers/Z/Bounds/Interpretation.v
Jason Gross
2017-10-13
*
Add some helper compilation lemmas
Jason Gross
2017-10-13
*
Add reflective compose, notation for Z.Syntax.{Expr,Interp}
Jason Gross
2017-10-12
*
Add update_by_tac_if_not_exists
Jason Gross
2017-10-10
*
TagList: make get error, and fix bugs
Jason Gross
2017-10-10
*
Add TagList
Jason Gross
2017-10-10
*
Add notations
Jason Gross
2017-10-10
*
Add UniformWeightInstances
Jason Gross
2017-10-09
*
Generalize phis
Jason Gross
2017-10-07
*
Factor out the compute bit of the compute notation in curve params
Jason Gross
2017-10-07
*
Factor out parameter-specific code
Jason Gross
2017-10-07
*
Coq 8.5 can't handle symbol-free notations
Jason Gross
2017-10-06
*
Fix display log
Jason Gross
2017-10-06
*
Clean up TestCase a bit
Jason Gross
2017-10-06
*
Add another constant
Jason Gross
2017-10-06
*
Add pow_ceil_mul_nat_nonneg
Jason Gross
2017-10-05
*
Add PoseTermWithName
Jason Gross
2017-10-05
*
Factor out some bits of ladderstep preglue
Jason Gross
2017-10-05
*
Add some ZUtil lemmas
Jason Gross
2017-10-03
*
Make some typeclasses opaque
Jason Gross
2017-10-02
*
Speed up reification a little bit
Jason Gross
2017-10-02
*
Add missing tactic in comment in ladderstep
Jason Gross
2017-09-27
*
Add src/Specific/X25519/C32/compiler.sh, update src/Specific/X25519/C64/scala...
Jason Gross
2017-09-27
*
Add curve25519-donna-c64 to etc/third_party
Jason Gross
2017-09-27
*
Add missing file
Jason Gross
2017-09-21
*
Add femul,fesqure for C32
Jason Gross
2017-09-21
*
Update constants files
Jason Gross
2017-09-21
*
Add extract_Expr
Jason Gross
2017-09-21
*
Split off tactics in IntegrationTestDisplayCommon
Jason Gross
2017-09-21
*
make bench
Jason Gross
2017-09-12
*
fsatz tests: 1/(1/x) = x
Andres Erbsen
2017-09-11
*
Fix more commented out alternatives
Jason Gross
2017-09-05
*
Fix commented out alternate version in ladderstep
Jason Gross
2017-09-05
*
Add decidable equality with nil
Jason Gross
2017-08-13
*
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
[next]