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
/
Arithmetic.v
Commit message (
Expand
)
Author
Age
*
Add Proof using to arithmetic proofs
Jason Gross
2018-08-07
*
Montgomery reduction in new pipeline
Jason Gross
2018-07-21
*
Thunk nat_rect for better perf, list_{rect=>case}
Jason Gross
2018-07-17
*
Remove a lemma that's been moved to NatUtil
Jason Gross
2018-07-17
*
Add a stronger version of eval_reduce
Jason Gross
2018-07-14
*
Make Z.div_mod_to_quot_rem stronger
Jason Gross
2018-07-10
*
Prove that to_bytesmod partitions
Jason Gross
2018-07-08
*
Shuffle some ZUtil lemmas around
Jason Gross
2018-07-08
*
Factor eval_reduce_square_exact a bit differently
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
*
Add select
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
*
Start with a better template for carry_square
Jason Gross
2018-07-03
*
WIP
Jason Gross
2018-07-03
*
Remove useless Requires
Jason Gross
2018-06-28
*
Add [freeze] to Arithmetic
Jason Gross
2018-06-21
*
Add extend_to_length for non-uniform-length add, sub
Jason Gross
2018-06-19
*
Add a comment about sub
Jason Gross
2018-06-18
*
New pipeline, split among files
Jason Gross
2018-06-17