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
*
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
*
Account for future changes of #219
Jason Gross
2017-06-22
*
src/Demo.v: a 200-line introduction to BaseSystem ideas
Andres Erbsen
2017-06-21
*
Prove In_to_list_left_tl, In_left_hd, to_list_left_append
Jason Gross
2017-06-21
*
Prove some admitted lemmas about uweight
Jason Gross
2017-06-21
*
compile src/Specific/IntegrationTestMontgomeryP256.s
Andres Erbsen
2017-06-21
*
Use is_bounded_by_None_repeat_In_iff_lt, remove axiom
Jason Gross
2017-06-20
*
Add is_bounded_by_None_repeat_In_iff_lt
Jason Gross
2017-06-20
*
make display
Jason Gross
2017-06-20
*
Also key adc->sbb on the carry-bit being negative
Jason Gross
2017-06-20
*
Add more simplification passes (de-doubling opp)
Jason Gross
2017-06-20
*
make display
Jason Gross
2017-06-20
*
Add more simplification passes (de-doubling opp)
Jason Gross
2017-06-20
*
make display
Jason Gross
2017-06-20
*
Enable a-nf for montgomery
Jason Gross
2017-06-20
*
make display
Jason Gross
2017-06-20
*
Add more Z-notations
Jason Gross
2017-06-20
*
make display
Jason Gross
2017-06-20
*
Add another fusion to adc-fusion
Jason Gross
2017-06-20
*
changed number of limbs partway through conditional_sub; was n, now S n
jadep
2017-06-20
*
Add fold_left_orb_true, fold_left_orb_pull
Jason Gross
2017-06-20
*
Use solve_wf_side_condition to synch the depth of auto with wf
Jason Gross
2017-06-20
*
make display
Jason Gross
2017-06-20
*
make display (new conditional_sub)
Jason Gross
2017-06-20
*
Make use of new conditional_subtract
Jason Gross
2017-06-20
*
Remove duplicate [small p] hypothesis from small_conditional_sub
Jason Gross
2017-06-20
*
Add conditional_sub_id to uncps globally
Jason Gross
2017-06-20
*
Add more constant notations
Jason Gross
2017-06-20
*
Add is_bounded_by_None_repeat_In_iff
Jason Gross
2017-06-20
*
make bench
Jason Gross
2017-06-20
*
check in icc-compiled IntegrationTestMontgomeryP256.s
Andres Erbsen
2017-06-20
*
sed mulx appropriately
Andres Erbsen
2017-06-20
*
defined conditional_sub (see #207) -- small_conditional_sub admitted, eval_co...
jadep
2017-06-20
*
rename Columns.sub_cps to make it clear that no balance is added
jadep
2017-06-20
*
Don't depend on classical axioms for small_add
Jason Gross
2017-06-20
*
Make use of new small_add
Jason Gross
2017-06-20
*
Weaken preconditions on small_add
Jason Gross
2017-06-20
*
Strip trailing whitespace
Jason Gross
2017-06-20
*
Better specs (F-based) for mulmod
Jason Gross
2017-06-19
*
No small in MP256 spec (wrong place), s/native/vm/
Jason Gross
2017-06-19
*
Improve mulmod_256 specs
Jason Gross
2017-06-19
*
[Require NatUtil] should not change [tauto]
Jason Gross
2017-06-19
*
Fix build error
Jason Gross
2017-06-19
*
fixed precondition on small_add
jadep
2017-06-19
*
Add smallness of output to montgomery synthesis
Jason Gross
2017-06-19
*
make display
Jason Gross
2017-06-18
[next]