index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Fancy
Commit message (
Collapse
)
Author
Age
*
split up Arithmetic (imports etc. not yet fixed, does not build)
jadep
2019-04-03
|
*
fix montgomery
jadep
2019-03-25
|
*
Get new Barrett proofs to generate Fancy code as before
jadep
2019-03-25
|
*
finish porting barrett and montgomery code to new glue style
jadep
2019-02-21
|
*
fix cast admits in Fancy
jadep
2019-02-15
|
*
clean up and factor out cast-admit so that [Print Assumptions] is more ↵
jadep
2019-02-08
|
|
|
|
fine-grained
*
cleanup
jadep
2019-02-08
|
*
remove some TODOs -- actually, the final proof does not rely on the unused ↵
jadep
2019-02-08
|
|
|
|
values
*
fix Montgomery proof and clean up a little
jadep
2019-02-08
|
*
remove 2: syntax so 8.7 builds
jadep
2019-02-07
|
*
Fix instruction-order admit; still neads cleanup
jadep
2019-02-07
|
*
Split up PushButtonSynthesis.v
Jason Gross
2019-01-18
|
|
|
|
Closes #497
*
Move print statements to Barrett and Montgomery files
jadep
2019-01-17
|
*
prune dependencies from Barrett256 and Montgomery256
jadep
2019-01-17
|
*
Prune dependencies of Prod.v and fix up
jadep
2019-01-17
|
*
Rename Translation.v
jadep
2019-01-17
|
*
Prune Translation.v deps and move tactics from other files [WIP]
jadep
2019-01-17
|
*
clean up and prune deps of Spec.v
jadep
2019-01-17
|
*
Fix up Montgomery
jadep
2019-01-17
|
*
separate toplevel2 into several files; fix up final barrett proof
jadep
2019-01-17