index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Experiments
/
NewPipeline
/
Toplevel1.v
Commit message (
Expand
)
Author
Age
*
Move a lemma
Jason Gross
2018-08-13
*
Fix a wrong bound computation (on negatives), fix a proof
Jason Gross
2018-08-13
*
Finish relax interp proofs
Jason Gross
2018-08-07
*
Fix an issue with the previous commit
Jason Gross
2018-08-07
*
Start setting up abs-int interp proofs
Jason Gross
2018-08-06
*
Finish AbsInt Wf proofs
Jason Gross
2018-08-04
*
Generalize type.eqv a bit
Jason Gross
2018-07-30
*
Integrate Wf and Interp proofs
Jason Gross
2018-07-30
*
Move the associator pass to the rewriter
Jason Gross
2018-07-26
*
Montgomery reduction in new pipeline
Jason Gross
2018-07-21
*
vm_compute in peel_interp_app
Jason Gross
2018-07-18
*
Better error message printing
Jason Gross
2018-07-12
*
Make Z.div_mod_to_quot_rem stronger
Jason Gross
2018-07-10
*
Remove nested proofs
Jason Gross
2018-07-03
*
Add support for annotating generated C functions with comments
Jason Gross
2018-07-03
*
Synthesize selectznz
Jason Gross
2018-07-03
*
Allow passing functions to synthesize on the command line, and scmul for 25519
Jason Gross
2018-07-03
*
No subst01 in mulmod
Jason Gross
2018-07-03
*
Start with a better template for carry_square
Jason Gross
2018-07-03
*
Don't subst01 in square
Jason Gross
2018-07-03
*
synthesize square
Jason Gross
2018-07-03
*
WIP
Jason Gross
2018-07-03
*
Pass around lists of strings for error messages
Jason Gross
2018-06-17
*
New pipeline, split among files
Jason Gross
2018-06-17