index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
PushButtonSynthesis
Commit message (
Expand
)
Author
Age
*
fix typo
jadep
2019-04-03
*
fix up imports in SmallExamples.v
jadep
2019-04-03
*
update import statements
jadep
2019-04-03
*
rename some things
jadep
2019-04-03
*
fix imports and qualifiers so everything builds
jadep
2019-04-03
*
remove extraneous module identifiers
jadep
2019-04-03
*
split up Arithmetic (imports etc. not yet fixed, does not build)
jadep
2019-04-03
*
Add constr_fail and constr_fail_with
Jason Gross
2019-03-31
*
fix montgomery
jadep
2019-03-25
*
finish proofs
jadep
2019-03-25
*
Get new Barrett proofs to generate Fancy code as before
jadep
2019-03-25
*
adapt barrett to new glue code
jadep
2019-02-21
*
Make Qed not take forever
jadep
2019-02-21
*
start adapting Montgomery to new glue code
jadep
2019-02-21
*
Use Preconditions: Postconditions:, rather than /\ and ->
Jason Gross
2019-02-02
*
More minor improvements in docstrings
Jason Gross
2019-02-02
*
Rename docstring generator based on Andres' suggestion
Jason Gross
2019-02-02
*
Update with davidben's and Andres' suggestions
Jason Gross
2019-02-02
*
Drop `map λ` bits in docstrings
Jason Gross
2019-02-02
*
Address code review comments to improve docstrings
Jason Gross
2019-02-02
*
Add autogenerated docstrings to synthesized code
Jason Gross
2019-02-02
*
Also display the carry chain in a comment
Jason Gross
2019-01-26
*
Add better computation of carry chain
Jason Gross
2019-01-26
*
Split up PushButtonSynthesis.v
Jason Gross
2019-01-18
*
move src/Experiments/NewPipeline/ to src/
Andres Erbsen
2019-01-09