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
...
*
Uncps unify_extracted
Jason Gross
2019-02-01
*
Reduce more in mulmod and squaremod
Jason Gross
2019-01-26
*
Add an example to SlowPrimeSynthesisExamples.v
Jason Gross
2019-01-26
*
Also display the carry chain in a comment
Jason Gross
2019-01-26
*
Add better computation of carry chain
Jason Gross
2019-01-26
*
Actually support Nat.eqb in reification
Jason Gross
2019-01-25
*
Support Nat.eqb in reification
Jason Gross
2019-01-25
*
Add remove_duplicates
Jason Gross
2019-01-24
*
Make trivial instances explicit
Maxime Dénès
2019-01-24
*
Give slightly more standard usage strings
Jason Gross
2019-01-23
*
Mention the separator (spaces) of the list arg
Jason Gross
2019-01-23
*
Split up PushButtonSynthesis.v
Jason Gross
2019-01-18
*
Define String.replace
Jason Gross
2019-01-18
*
Be stricter about rejecting command line arguments
Jason Gross
2019-01-18
*
Don't allow r[0~>0] ranges in fancy synthesis
Jason Gross
2019-01-17
*
Remove ? notation
Jason Gross
2019-01-17
*
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
*
Make Montgomery take arguments separately instead of as a pair
jadep
2019-01-17
*
separate toplevel2 into several files; fix up final barrett proof
jadep
2019-01-17
*
Constant-propogate 0+x and x+0 after bounds
Jason Gross
2019-01-16
*
Add a rewrite rule to collapse constant casts
Jason Gross
2019-01-16
*
Add some more basic ZRange lemmas
Jason Gross
2019-01-15
*
Move StringMap into Strings/
Jason Gross
2019-01-15
*
Add StringMap
Jason Gross
2019-01-15
*
Add String_as_OT
Jason Gross
2019-01-15
*
Ensure that we only left-shift on unsigned values
Jason Gross
2019-01-15
*
Fix computation of INTX_MIN
Jason Gross
2019-01-15
*
Don't cast signed to unsigned before shifting
Jason Gross
2019-01-15
*
We don't need to encode c with taps in WBW montgomery
Jason Gross
2019-01-14
*
Autocompute s and c in WBW Montgomery
Jason Gross
2019-01-14
*
remove old pipeline
Andres Erbsen
2019-01-09
*
move src/Experiments/NewPipeline/ to src/
Andres Erbsen
2019-01-09
*
Fix for 8.7
Jason Gross
2019-01-07
*
Merge remote-tracking branch 'origin/fix_fancy4'
Andres Erbsen
2019-01-07
|
\
*
|
Update README.md
Jason Gross
2019-01-05
*
|
prove admit
Andres Erbsen
2019-01-05
*
|
build on Coq master
Andres Erbsen
2019-01-05
*
|
new pipeline: refactor glue, split into more files
Jason Gross
2019-01-05
|
*
Update fancy rewriter output with new compilation output
Jason Gross
2019-01-03
|
*
Finish proving fancy rewrite rules
Jason Gross
2019-01-03
|
*
Fix bounds checking on shift
Jason Gross
2019-01-03
|
*
comment out broken code so things build
jadep
2019-01-03
|
*
try to fix fancy rewrite rules; current output is incorrect
jadep
2019-01-03
|
*
WIP
jadep
2019-01-03
[prev]
[next]