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
*
Fix missing parenthesis
jadep
2016-09-17
*
Remove unused lemma and standardized use of notations for [freeze] proofs
jadep
2016-09-17
*
deduplicate Let_In into src/Util/LetIn.v
Andres Erbsen
2016-09-17
*
Update .gitignore for Coq 8.6
Jason Gross
2016-09-16
*
Update .gitignore for Coq 8.6
Jason Gross
2016-09-16
*
Add λn reserved notation
Jason Gross
2016-09-16
*
Fix for Coq 8.5
Jason Gross
2016-09-16
*
Add more prop_of_option
Jason Gross
2016-09-16
*
Derive EdDSA.verify from equational specification
Andres Erbsen
2016-09-16
*
Algebra: prove an admit, add eq_r_opp_r_inv
Andres Erbsen
2016-09-16
*
IterAssocOp: parameters before arguments
Andres Erbsen
2016-09-16
*
ModularArithmetic: conversions between [F] and [nat]
Andres Erbsen
2016-09-16
*
Generalize InlineConst
Jason Gross
2016-09-16
*
Split off lemmas about [InlineConst]
Jason Gross
2016-09-16
*
Equality for nat in natutil
Jason Gross
2016-09-16
*
Add arguments for smartval
Jason Gross
2016-09-16
*
Fix a bad line
Jason Gross
2016-09-16
*
Add SmartVal
Jason Gross
2016-09-16
*
Add generalized version of Wf parameterized on rel
Jason Gross
2016-09-15
*
More 8.4 compatibility
jadep
2016-09-14
*
Tweaked automation for 8.4 compatibility
jadep
2016-09-14
*
Automated and cleaned up [freeze] carry-loop proofs
jadep
2016-09-13
*
Update old carry loop bounds proof; now is automated and also has analogous s...
jadep
2016-09-13
*
Moved lemmas to ZUtil
jadep
2016-09-13
*
Finished off last admits for proofs of bounds after 3 carry loops.
jadep
2016-09-13
*
[freeze] proofs : Mostly-complete proofs of bounds after 3 carry loops
jadep
2016-09-13
*
[freeze] proofs : proved bounds for second carry loop.
jadep
2016-09-13
*
Merge pull request #63 from JasonGross/fancy-barrett-montgomery
Jason Gross
2016-09-08
|
\
*
|
Fully qualify [Require]s
Jason Gross
2016-09-08
|
*
Move FancyMachine from Experiments to Specific
Jason Gross
2016-09-08
|
*
Address code review, add come comments and cleanup
Jason Gross
2016-09-08
|
*
Add Barrett and Montgomery for the 256-bit machine
Jason Gross
2016-09-07
|
/
*
Fixes for Coq 8.4
Jason Gross
2016-09-07
*
Bump submodule for better timing
Jason Gross
2016-09-07
*
Remove the need for coercions in well-typing of Reify
Jason Gross
2016-09-07
*
Add fastpath to reify, add coercions
Jason Gross
2016-09-07
*
Work around bug #5073 (lia)
Jason Gross
2016-09-07
*
Better spec in Montgomery.ZBounded
Jason Gross
2016-09-07
*
Key on the head of the operation in reification
Jason Gross
2016-09-07
*
Add Common Subexpression Elimination
Jason Gross
2016-09-06
*
Fix for 8.4's type inferencer being broken
Jason Gross
2016-09-06
*
Fix for changes in 8.4/8.5 behavior of [intro] w.r.t. refolding
Jason Gross
2016-09-06
*
Fix for 8.6 (context (correctly) no longer defaults to type_scope)
Jason Gross
2016-09-06
*
make 8.4 happier
jadep
2016-09-06
*
Finished sqrt in GF25519
jadep
2016-09-06
*
Pushed [freeze] through to GF25519 in preparation for defining [sqrt], cleani...
jadep
2016-09-06
*
Add interp_flat_type_gen_rel_pointwise
Jason Gross
2016-09-05
*
Add correctness of interpretation of linearize and inline_const
Jason Gross
2016-09-05
*
Add instances for interp_type_gen_rel_pointwise
Jason Gross
2016-09-05
*
Better implicits for interp_type_gen_rel_pointwise
Jason Gross
2016-09-05
[next]