index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Specific
/
MontgomeryP256_128.v
Commit message (
Expand
)
Author
Age
*
Factor out some of the preglue synthesis code
Jason Gross
2017-07-08
*
Fix misnamed references in Specific/ (broke after saturated arithetic reorg)
jadep
2017-06-30
*
Fix unfolding to not unfold sub_with_get_borrow in P256
Jason Gross
2017-06-29
*
More proof fixing
Jason Gross
2017-06-26
*
Remove an admit
Jason Gross
2017-06-26
*
Add nonzero synthesis
Jason Gross
2017-06-26
*
Clean up some montgomery wbw instantiation, make display
Jason Gross
2017-06-24
*
Add (partially admitted) integration tests for add, sub, opp
Jason Gross
2017-06-22
*
P256: Partial work on add, sub, opp
Jason Gross
2017-06-22
*
P256: Keep around < eval N bounds
Jason Gross
2017-06-22
*
Add tighter bounds to MontgomeryP256{,_128}
Jason Gross
2017-06-22
*
Make use of new conditional_subtract
Jason Gross
2017-06-20
*
No small in MP256 spec (wrong place), s/native/vm/
Jason Gross
2017-06-19
*
Improve mulmod_256 specs
Jason Gross
2017-06-19
*
Add smallness of output to montgomery synthesis
Jason Gross
2017-06-19
*
mulmod: sig type in terms of equivalence modulo p
Jason Gross
2017-06-18
*
Don't unfold MulSplit
Jason Gross
2017-06-18
*
Update wbw to work with new api
Jason Gross
2017-06-18
*
Use uint128_t for 128-bit montgomery
Jason Gross
2017-06-17
*
Add 128-bit version of montgomery for testing
Jason Gross
2017-06-17