index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Rewriter.v
Commit message (
Expand
)
Author
Age
*
Automate more of the rewriter, and factor out rule-specific things
Jason Gross
2019-04-11
*
Automate more of the rewriter reification, proof
Jason Gross
2019-04-09
*
Add UnderLets flat_map interp proofs,other changes
Jason Gross
2019-04-04
*
Add Z.combine_at_bitwidth
Jason Gross
2019-04-02
*
Factor out rewriter rules
Jason Gross
2019-03-31
*
Fix a non-terminated comment
Jason Gross
2019-03-31
*
Add some comments based on CR requests
Jason Gross
2019-03-31
*
Finish reifying list lemmas
Jason Gross
2019-03-31
*
Add constr_fail and constr_fail_with
Jason Gross
2019-03-31
*
Get new Barrett proofs to generate Fancy code as before
jadep
2019-03-25
*
Reify most rewrite rules
Jason Gross
2019-03-07
*
Fix unfolding of pattern.base.lookup_default
Jason Gross
2019-03-05
*
Fix an issue with a proof from the previous commit
Jason Gross
2019-03-04
*
Add support for reifying `zrange` and `option`
Jason Gross
2019-02-18
*
Insert casts before literals during bounds analysis
Jason Gross
2019-02-11
*
Remove an unused argument
Jason Gross
2019-02-01
*
Uncps unify_extracted
Jason Gross
2019-02-01
*
Constant-propogate 0+x and x+0 after bounds
Jason Gross
2019-01-16
*
Add a rewrite rule to collapse constant casts
Jason Gross
2019-01-16
*
move src/Experiments/NewPipeline/ to src/
Andres Erbsen
2019-01-09