index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Compilers
Commit message (
Expand
)
Author
Age
*
Coq 8.5 can't handle symbol-free notations
Jason Gross
2017-10-06
*
Clean up TestCase a bit
Jason Gross
2017-10-06
*
Add another constant
Jason Gross
2017-10-06
*
Make some typeclasses opaque
Jason Gross
2017-10-02
*
Speed up reification a little bit
Jason Gross
2017-10-02
*
Update constants files
Jason Gross
2017-09-21
*
Unfold tuple arguments in reflective pipeline
Jason Gross
2017-07-08
*
Fix CSE_sym denote
Jason Gross
2017-07-07
*
Fix proofs broken by previous commit
Jason Gross
2017-07-07
*
Stronger contexts
Jason Gross
2017-07-07
*
Remove some admitted lemmas
Jason Gross
2017-07-07
*
Fix a mis-aligned comment marker in CNotations script
Jason Gross
2017-07-03
*
change notation `_ == _ ? _ : _ ` to `cmovznz(_, _, _)`
Jason Gross
2017-06-29
*
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
*
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
[next]