index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Add Z.peano_rect
Jason Gross
2017-06-13
*
Fill in mul_split to wbw montgomery
Jason Gross
2017-06-13
*
Add Z.mul_split
Jason Gross
2017-06-13
*
WBW-montgomery: Fill in most context variables
Jason Gross
2017-06-13
*
finish computational portions of operations needed for Montgomery, and sketch...
jadep
2017-06-12
*
Remove use of id_tuple_with_alt_proof
Jason Gross
2017-06-12
*
Add a Show to keep track of where we are in karatsuba
Jason Gross
2017-06-12
*
Handle IdWithAlt in the simplifier
Jason Gross
2017-06-12
*
Add some more constant notations
Jason Gross
2017-06-12
*
WIP on src/Specific/IntegrationTestKaratsubaMul.v
Jason Gross
2017-06-12
*
Push bounds side conditions through the pipeline
Jason Gross
2017-06-12
*
Fix zrange notation levels
Jason Gross
2017-06-12
*
Add CompileInterpSideConditions.v
Jason Gross
2017-06-12
*
Add snd_interpf_side_conditions_gen_Some
Jason Gross
2017-06-12
*
Add Named.InterpSideConditions
Jason Gross
2017-06-12
*
Handle multiple lite-unmade-vofiles
Jason Gross
2017-06-12
*
Fix lite target (typo in makefile fn call)
Jason Gross
2017-06-12
*
Add Z.InterpSideConditions
Jason Gross
2017-06-12
*
Add InterpSideConditions
Jason Gross
2017-06-12
*
Have interped_op_side_conditions return a pointed_Prop
Jason Gross
2017-06-12
*
Better support for coq_makefile2 with fewer warnings
Jason Gross
2017-06-12
*
Drop unused [bn] notation
Jason Gross
2017-06-12
*
Drop some small hyps in light of small_add change
Jason Gross
2017-06-12
*
Remove eval_small_bounded_numlimbs
Jason Gross
2017-06-12
*
Initial stab at id_with_alt
Jason Gross
2017-06-11
*
Add dummy version of IdWithAlt to compilers
Jason Gross
2017-06-11
*
Factor karatsuba through IdfunWithAlt, add test
Jason Gross
2017-06-11
*
Add unfold lemmas for id_with_alt
Jason Gross
2017-06-11
*
Add IdfunWithAlt
Jason Gross
2017-06-11
*
Don't print directory when entering coqprime folder
Jason Gross
2017-06-11
*
Be more forceful about clearing before abstract in glue code
Jason Gross
2017-06-11
*
Add script to remake Tactics.v file
Jason Gross
2017-06-11
*
Add clearbody_all
Jason Gross
2017-06-11
*
Fix loop notations, add for loops
Jason Gross
2017-06-11
*
Reserve some more notations
Jason Gross
2017-06-11
*
cps notations WIP...
Andres Erbsen
2017-06-11
*
cps and loop notations WIP
Andres Erbsen
2017-06-11
*
Finish admits in WordByWord/Proofs.v
Jason Gross
2017-06-10
*
Add mod_pull_div{,_full}
Jason Gross
2017-06-10
*
More powerful replace_neg_with_pos
Jason Gross
2017-06-10
*
Fix a typo
Jason Gross
2017-06-10
*
Rename power_mod_full to mod_pow_full for similarity with std lib
Jason Gross
2017-06-10
*
Add Z.pow_mod_Proper
Jason Gross
2017-06-10
*
Minor changes to a proof in progress
Jason Gross
2017-06-10
*
Remove useless small_from_bound; drop R_big
Jason Gross
2017-06-10
*
Add proofs about numlimbs
Jason Gross
2017-06-10
*
Add constraint on scmul scalar
Jason Gross
2017-06-10
*
Update context to not need eval_nonneg
Jason Gross
2017-06-10
*
Add redc_bound
Jason Gross
2017-06-10
*
Create crypto-defects.md
Andres Erbsen
2017-06-10
[next]