index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Arithmetic
Commit message (
Expand
)
Author
Age
*
Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtil
Jason Gross
2018-08-23
*
Backwards compatible fix for some issues from https://github.com/coq/coq/pull...
Jason Gross
2018-08-04
*
Make Z.div_mod_to_quot_rem stronger
Jason Gross
2018-07-10
*
Make all parameters implicit
Jasper Hugunin
2018-07-02
*
remove comment
Jade Philipoom
2018-04-11
*
add a comment to rerun build
Jade Philipoom
2018-04-11
*
Automate some proofs a bit more
Jason Gross
2018-04-11
*
try to fix build on coq master
Jade Philipoom
2018-04-11
*
prove stronger bound on quotient error for barrett reduction
Jade Philipoom
2018-04-11
*
Review comments.
David Benjamin
2018-03-09
*
easy bits
David Benjamin
2018-03-09
*
Prove another Barrett reduction variant.
David Benjamin
2018-03-09
*
Fix naming issue
Jade Philipoom
2018-02-23
*
add equivalence proof for Montgomery reduce_via_partial_alt
Jade Philipoom
2018-02-23
*
Add MontgomeryAPI.encode and two lemmas about it
Jason Gross
2017-11-14
*
fix comment
jadep
2017-11-12
*
Fix another side condition issue
Jason Gross
2017-11-08
*
Fix a bug in previous commit
Jason Gross
2017-11-08
*
Add freeze rewrite lemmas to dbs
Jason Gross
2017-11-08
*
Add karatsuba, goldilocks lemmas to rewrite dbs
Jason Gross
2017-11-07
*
Move chained_carries' (now chained_carries_reduce)
Jason Gross
2017-11-07
*
Add more versions of basesystem_partial_evaluation_unfolder
Jason Gross
2017-11-07
*
Split off computational part of basesystem_partial_evaluation_RHS_gen
Jason Gross
2017-11-07
*
More use of Z.eqb_cps
Jason Gross
2017-11-07
*
Use div_cps and modulo_cps in more places
Jason Gross
2017-11-07
*
Make use of id_tuple_with_alt_cps'
Jason Gross
2017-11-06
*
Make use of from_associational_cps in more places
Jason Gross
2017-11-01
*
More use of Z.eqb_cps
Jason Gross
2017-11-01
*
Add another unfolding database
Jason Gross
2017-10-22
*
Fix bug in previous commit
Jason Gross
2017-10-20
*
Use div_cps, modulo_cps
Jason Gross
2017-10-20
*
Use fold_right_cps2 to get eqb_cps to get the right continuation type
Jason Gross
2017-10-19
*
Add more unfolds to basesystem_partial_evaluation_unfolder
Jason Gross
2017-10-19
*
Switch arithmetic to cps for Z * Z under the hood
Jason Gross
2017-10-19
*
Move tactics around in src/Arithmetic/CoreUnfolder.v
Jason Gross
2017-10-19
*
Pattern over cps lemmas in Arithmetic/Core
Jason Gross
2017-10-19
*
Unfold more things in basesystem_partial_evaluation_unfolder
Jason Gross
2017-10-18
*
Add some more things to basesystem_partial_evaluation_unfolder
Jason Gross
2017-10-18
*
Add basesystem_partial_evaluation_unfolder db
Jason Gross
2017-10-18
*
Unfold more things in core unfolder
Jason Gross
2017-10-18
*
Allow instantiating type arguments without reducing matches
Jason Gross
2017-10-18
*
Pattern more things in arithmetic/core
Jason Gross
2017-10-17
*
Add MulSplitUnfolder
Jason Gross
2017-10-17
*
Add faster arithmetic unfolding
Jason Gross
2017-10-15
*
Extend basesystem_partial_evaluation_RHS
Jason Gross
2017-10-15
*
Fix a typo in the previous commit
Jason Gross
2017-10-14
*
Split up solve_op_mod_eq
Jason Gross
2017-10-14
*
Add UniformWeightInstances
Jason Gross
2017-10-09
*
Add cbv_runtime in Arithmetic/Core
Jason Gross
2017-07-08
*
More fine-grained tactics imports
Jason Gross
2017-07-08
[next]