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
*
Fix comment-in-string issues
Jason Gross
2017-06-29
*
More C Notations for uin8_t-valued addcarryx
Jason Gross
2017-06-29
*
Remove a [Check]
Jason Gross
2017-06-29
*
Use -std=gnu11 for older versions of gcc
Jason Gross
2017-06-28
*
match C code in Jacobian addition
Andres Erbsen
2017-06-27
*
p256 compilation and benchmarks with manual kludges
Andres Erbsen
2017-06-27
*
proved eval_mod and eval_div (last remaining eval_ admits in Saturated)
jadep
2017-06-27
*
More proof fixing
Jason Gross
2017-06-26
*
Add a comment for nonzero_cps
Jason Gross
2017-06-26
*
Fix a broken proof
Jason Gross
2017-06-26
*
Factor out admitted proof into admitted lemma
Jason Gross
2017-06-26
*
Remove an admit
Jason Gross
2017-06-26
*
make display
Jason Gross
2017-06-26
*
Add nonzero synthesis
Jason Gross
2017-06-26
*
remove unused admit (has been moved to Tuple.v)
jadep
2017-06-26
*
indentation
Jason Gross
2017-06-25
*
Prove map2_zselect
Jason Gross
2017-06-25
*
Prove map2_append
Jason Gross
2017-06-25
*
Allow disabling adc-fusion
Jason Gross
2017-06-25
*
make display on p256
Andres Erbsen
2017-06-25
*
Fixes #219
jadep
2017-06-25
*
write and prove Tuple.map2_cps
jadep
2017-06-25
*
make display
Jason Gross
2017-06-25
*
Convert adc to sbb when doing [0 - x]
Jason Gross
2017-06-25
*
Revert "Convert adc to sbb when doing [0 - x]"
Jason Gross
2017-06-25
*
Convert adc to sbb when doing [0 - x]
Jason Gross
2017-06-24
*
make display
Jason Gross
2017-06-24
*
Fix some things not being unfolded
Jason Gross
2017-06-24
*
make display
Jason Gross
2017-06-24
*
Propogate neg through constant multiplication
Jason Gross
2017-06-24
*
Clean up some montgomery wbw instantiation, make display
Jason Gross
2017-06-24
*
Remove admits
Jason Gross
2017-06-24
*
Fill in axioms for sub_then_maybe_add; this required fiddling with updated ar...
jadep
2017-06-24
*
made conditional_add a wrapper, defined and proved sub_then_maybe_add
jadep
2017-06-24
*
Make a 'conditionals' section in Columns, and move conditional_add there
jadep
2017-06-24
*
make bench
Andres Erbsen
2017-06-23
*
Weierstrass Jacobian mixed addition
Andres Erbsen
2017-06-23
*
Fix an issue with notations
Jason Gross
2017-06-22
*
Add notation for logical or
Jason Gross
2017-06-22
*
make display
Jason Gross
2017-06-22
*
Add (partially admitted) integration tests for add, sub, opp
Jason Gross
2017-06-22
*
Fix a typo in push_Zmod that was causing looping
Jason Gross
2017-06-22
*
P256: Partial work on add, sub, opp
Jason Gross
2017-06-22
*
Fix an [sz] that shouldn't have been removed in the previous commit
Jason Gross
2017-06-22
*
P256: Keep around < eval N bounds
Jason Gross
2017-06-22
*
Add sig_conj_by_impl2
Jason Gross
2017-06-22
*
Work around bug #5615 (constr not being updated)
Jason Gross
2017-06-22
*
move Specifi p256 files into their own directory
Andres Erbsen
2017-06-22
*
Fix some minor naming bugs in sig_assoc tactics
Jason Gross
2017-06-22
*
Add tighter bounds to MontgomeryP256{,_128}
Jason Gross
2017-06-22
[next]