index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
Commit message (
Expand
)
Author
Age
*
Allow printing more easily readable code in errors
Jason Gross
2018-07-09
*
Prove that to_bytesmod partitions
Jason Gross
2018-07-08
*
Shuffle some ZUtil lemmas around
Jason Gross
2018-07-08
*
Fix an infinite loop in Z.peel_le
Jason Gross
2018-07-06
*
Factor eval_reduce_square_exact a bit differently
Jason Gross
2018-07-03
*
Remove nested proofs
Jason Gross
2018-07-03
*
Fix hints, hopefully
Jason Gross
2018-07-03
*
clean
Jason Gross
2018-07-03
*
Finish reduce_square proof
Jason Gross
2018-07-03
*
Try to fix square again
Jason Gross
2018-07-03
*
Fix a typo, start on proof
Jason Gross
2018-07-03
*
Fix a reification issue
Jason Gross
2018-07-03
*
Try a different reduce_square
Jason Gross
2018-07-03
*
WIP better square
Jason Gross
2018-07-03
*
Fix missing arg
Jason Gross
2018-07-03
*
Add missing space
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
*
Correctly reify match on prod
Jason Gross
2018-07-03
*
Add select
Jason Gross
2018-07-03
*
Comment out some code that's too slow
Jason Gross
2018-07-03
*
Allow passing functions to synthesize on the command line, and scmul for 25519
Jason Gross
2018-07-03
*
Pull out *2 in square, don't turn *2 into <<1
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
*
static in c
Jason Gross
2018-07-03
*
static void
Jason Gross
2018-07-03
*
WIP
Jason Gross
2018-07-03
*
Add ZUtil, list lemmas
Jason Gross
2018-07-02
*
Fix a notation issue in previous commit
Jason Gross
2018-07-02
*
Add more ListUtil proofs
Jason Gross
2018-07-02
*
Add some list lemmas
Jason Gross
2018-07-02
*
Make all parameters implicit
Jasper Hugunin
2018-07-02
*
Prefer relations of the form [eq ==> eq ==> ... ==> eq] in setoids
Jason Gross
2018-07-01
*
Add useful list lemmas
Jason Gross
2018-06-29
*
Add ZUtil.Sorting
Jason Gross
2018-06-29
*
Revert "Add more schemes for prod"
Jason Gross
2018-06-28
*
Add more schemes for prod
Jason Gross
2018-06-28
*
Remove useless Requires
Jason Gross
2018-06-28
*
Try out stronger land, lor bounds
Jason Gross
2018-06-27
*
Add is_tighter_than_bool lemmas
Jason Gross
2018-06-27
*
Add lnot mod pull/push lemmas
Jason Gross
2018-06-27
*
Add missing Z.lnot_0 hints
Jason Gross
2018-06-27
*
Add more Z const hints
Jason Gross
2018-06-27
*
Remove lneg in favor of lnot_modulo (lneg was wrong)
Jason Gross
2018-06-27
*
Add some Z.land, Z.lor hints
Jason Gross
2018-06-27
*
Add a couple of zrange lemmas
Jason Gross
2018-06-26
*
Add specialize_all_ways, fix a proof in src/Compilers/Z/ArithmeticSimplifierI...
Jason Gross
2018-06-26
[next]