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
Commit message (
Expand
)
Author
Age
*
Add nonzero synthesis
Jason Gross
2017-06-26
*
Allow disabling adc-fusion
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
*
Propogate neg through constant multiplication
Jason Gross
2017-06-24
*
Add notation for logical or
Jason Gross
2017-06-22
*
Work around bug #5615 (constr not being updated)
Jason Gross
2017-06-22
*
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
*
Add more simplification passes (de-doubling opp)
Jason Gross
2017-06-20
*
Add more Z-notations
Jason Gross
2017-06-20
*
Add another fusion to adc-fusion
Jason Gross
2017-06-20
*
Use solve_wf_side_condition to synch the depth of auto with wf
Jason Gross
2017-06-20
*
Add more constant notations
Jason Gross
2017-06-20
*
Add more constants
Jason Gross
2017-06-18
*
Better simplification of mulsplit
Jason Gross
2017-06-18
*
Fix typo in format
Jason Gross
2017-06-18
*
Add fake notation for addcarryx_u128 and similar
Jason Gross
2017-06-18
*
Add some notations for mulx
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
*
Add cnotations for addcarryx with uint8_t
Jason Gross
2017-06-18
*
Add convenience for supporting uint8
Jason Gross
2017-06-18
*
Add notations
Jason Gross
2017-06-18
*
Adding more (possibly unneeded) simplification
Jason Gross
2017-06-18
*
Try more simplification
Jason Gross
2017-06-17
*
Drop the 0-carry bit before bounds analysis
Jason Gross
2017-06-17
*
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 more simplification to pipeline
Jason Gross
2017-06-17
*
Add linearization to inline pairs in post-bounds pipeline
Jason Gross
2017-06-17
*
Add extra simplification to simplifier for adc
Jason Gross
2017-06-17
*
Add more constants
Jason Gross
2017-06-17
*
Unfold Z.mul_split_at_bitwidth for reification
Jason Gross
2017-06-17
*
Add some more display constants
Jason Gross
2017-06-17
*
Add bool into P256
Jason Gross
2017-06-17
*
Remove fails; if we fail too strongly, we miss debugging information
Jason Gross
2017-06-17
*
Add back failure at level 100
Jason Gross
2017-06-17
*
Better error messages in reification
Jason Gross
2017-06-17
*
Revert PR #203
Jason Gross
2017-06-16
*
Fix CArrayNotations
Jason Gross
2017-06-16
*
Revert "Revert "Add CArrayNotations""
Jason Gross
2017-06-16
*
Revert "Add CArrayNotations"
Jason Gross
2017-06-15
*
Add CArrayNotations
Jason Gross
2017-06-15
*
Display Z operations with ℤ attached
Jason Gross
2017-06-15
*
Eliminate well-bounded IdWithAlt from final output
Jason Gross
2017-06-15
*
Add constant-pushing IdWithAlt optimization
Jason Gross
2017-06-14
*
Rework and speed up arithmetic simplifier proofs
Jason Gross
2017-06-14
*
Make rewrite_eta_match_base_type_impl a bit faster
Jason Gross
2017-06-13
[next]