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
*
Add more notation constants
Jason Gross
2017-10-18
*
Make use of faster interp rewriting
Jason Gross
2017-10-17
*
Add InterpRewriting
Jason Gross
2017-10-17
*
Turn on parenthetization in C output
Jason Gross
2017-10-17
*
Unify notation printing to allow changing it all at once
Jason Gross
2017-10-17
*
Fix some type annotations for better non-unfolding
Jason Gross
2017-10-17
*
Add support for parenthesizing all CNotations expressions
Jason Gross
2017-10-16
*
Add more constants
Jason Gross
2017-10-16
*
Add some more power-of-two notations
Jason Gross
2017-10-16
*
Add more notations
Jason Gross
2017-10-16
*
Add some constants from montgomery
Jason Gross
2017-10-15
*
Fix some issues with reification debug printing
Jason Gross
2017-10-15
*
Add more constant notations from solinas primes
Jason Gross
2017-10-15
*
Add SmartFlatTypeMap_Pair
Jason Gross
2017-10-14
*
Fix a bug in CommonSubexpressionEliminationProperties.v
Jason Gross
2017-10-13
*
Add some SmartMap tuple lemmas
Jason Gross
2017-10-13
*
Fix a spelling error
Jason Gross
2017-10-13
*
Factor out truncation_bounds
Jason Gross
2017-10-13
*
Add comment to Compilers/Z/Bounds/Interpretation.v
Jason Gross
2017-10-13
*
Add some helper compilation lemmas
Jason Gross
2017-10-13
*
Add reflective compose, notation for Z.Syntax.{Expr,Interp}
Jason Gross
2017-10-12
*
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
[next]