index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Compilers
/
Z
/
ArithmeticSimplifier.v
Commit message (
Expand
)
Author
Age
*
Add reflective compose, notation for Z.Syntax.{Expr,Interp}
Jason Gross
2017-10-12
*
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
*
Propogate neg through constant multiplication
Jason Gross
2017-06-24
*
Also key adc->sbb on the carry-bit being negative
Jason Gross
2017-06-20
*
Better simplification of mulsplit
Jason Gross
2017-06-18
*
Better test for simplifier
Jason Gross
2017-06-18
*
Stronger simplification of adc too add when we can prove the carry is 0
Jason Gross
2017-06-18
*
Be a bit more forceful in eliminating zeros in arith simpl
Jason Gross
2017-06-17
*
More arithmetic simplification for adc, mul
Jason Gross
2017-06-17
*
Add extra simplification to simplifier for adc
Jason Gross
2017-06-17
*
Eliminate well-bounded IdWithAlt from final output
Jason Gross
2017-06-15
*
Add constant-pushing IdWithAlt optimization
Jason Gross
2017-06-14
*
Reify Z.mul_with_split_at_bitwidth
Jason Gross
2017-06-13
*
Handle IdWithAlt in the simplifier
Jason Gross
2017-06-12
*
Add dummy version of IdWithAlt to compilers
Jason Gross
2017-06-11
*
Add compiler optimization for [Zselect (-x) _ _]
Jason Gross
2017-05-20
*
Get sbb conversion working in the pipeline
Jason Gross
2017-05-20
*
Add adc -> sbb to arithmetic simplifer
Jason Gross
2017-05-20
*
Add SubWithGetBorrow to reflective machinery
Jason Gross
2017-05-20
*
Add reflective machinery for adc, zselect
Jason Gross
2017-05-17
*
rename-everything
Andres Erbsen
2017-04-06