index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
ModularArithmetic
/
ModularBaseSystemListProofs.v
Commit message (
Expand
)
Author
Age
*
prove testbit_sub_pow2
Andres Erbsen
2016-10-29
*
Factor out cmov{l,ne} and neg
Jason Gross
2016-10-27
*
Created separate definitions for cmovne and cmovl for reification
jadep
2016-10-23
*
Modified [freeze] to be more reifyable
jadep
2016-10-22
*
Moved conversion logic out of Pow2BaseProofs into its own file
jadep
2016-10-06
*
Finished remaining admits in [freeze] proofs
jadep
2016-09-23
*
Reorganization, moving of lemmas to correct files, and 8.4 compatibility
jadep
2016-09-21
*
Proved specification of constant-time modulus comparison (except for one ZUti...
jadep
2016-09-21
*
Move side lemmas to appropriate files
jadep
2016-09-17
*
Fully qualify [Require]s
Jason Gross
2016-09-08
*
Pushed [freeze] through to GF25519 in preparation for defining [sqrt], cleani...
jadep
2016-09-06
*
Instantiated conversion both to (pack) and from (unpack) another set of limb ...
jadep
2016-08-16
*
Put ModularBaseSystem carries in terms of [carry_gen], and pushed this change...
jadep
2016-07-25
*
merge
jadep
2016-07-20
*
restructured ModularBaseSystem pipeline to put tuple conversion before Modula...
jadep
2016-07-20