index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Util
Commit message (
Expand
)
Author
Age
*
Add Unit.v
Jason Gross
2016-06-23
*
Add equality on sum types
Jason Gross
2016-06-23
*
Improve some tactics and lemmas
Jason Gross
2016-06-23
*
[break_match] should not be local
Jason Gross
2016-06-23
*
Add tactics to Tactics, at most 2 sq-roots to Algebra
Jason Gross
2016-06-23
*
Fix broken notations (hopefully)
Jason Gross
2016-06-22
*
Fix missing notations
Jason Gross
2016-06-22
*
Aggregate all level specifications not in Spec/*
Jason Gross
2016-06-22
*
Fix for broken abstract
Jason Gross
2016-06-22
*
Add decidability util file
Jason Gross
2016-06-22
*
remove trailing whitespace from src/
Andres Erbsen
2016-06-20
*
Variosu 8.5 fixes
Jason Gross
2016-06-20
*
Merge branch 'field-experiment'
Andres Erbsen
2016-06-20
|
\
|
*
tuple tooling
Andres Erbsen
2016-06-20
|
*
port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try fewer...
Andres Erbsen
2016-06-18
*
|
Merge
jadep
2016-06-14
|
\
\
*
|
|
Finished admits for canonicalization proofs.
jadep
2016-06-14
*
|
|
progress on second stage (conditional constant-time subtraction) of canonical...
jadep
2016-06-13
|
*
|
Fix for Coq 8.4pl2
Jason Gross
2016-06-11
*
|
|
starting rewrite using different definition of map
jadep
2016-06-11
|
|
/
|
/
|
|
*
8.5 fixes
Jason Gross
2016-06-10
|
/
*
Merge branch 'master' of github.mit.edu:plv/fiat-crypto
jadep
2016-05-25
|
\
|
*
Remove unfolding, rewrite -> setoid_rewrite
Jason Gross
2016-05-24
*
|
First stage of canonicalization proofs complete; proved 3 carry loops reduce ...
jadep
2016-05-20
|
/
*
Proved decode_point_eq in Ed25519 (comparing encodings is equivalent to
jadep
2016-04-29
*
Cleanup: mostly moving lemmas to Util files, some moving lemmas to more gener...
jadep
2016-04-28
*
Cleanup of GF25519
jadep
2016-04-20
*
moved lemmas from ModularBaseSystemProofs to various Util files
jadep
2016-04-20
*
Merge branch 'master' of github.mit.edu:plv/fiat-crypto
jadep
2016-04-19
|
\
*
|
Added lemmas to Util/ that are needed for testbit.
jadep
2016-04-19
|
*
Add a tactic for field inequalities
Jason Gross
2016-04-19
|
/
*
Retrieved updated version of Util/IterAssocOp and modified ExtendedCoordinate...
jadep
2016-04-14
*
Reverting Util/IterAssocOp to an earlier version for compatibility with Compl...
jadep
2016-04-12
*
Merge branch 'master' of github.mit.edu:plv/fiat-crypto
jadep
2016-03-30
|
\
|
*
Finish absolutizing imports
Jason Gross
2016-03-10
*
|
IterAssocOp: now uses arbitrary representation of scalar that implements testbit
Jade Philipoom
2016-03-08
*
|
IterAssocOp : now takes a bound argument instead of just using size of exponent
Jade Philipoom
2016-03-07
|
/
*
IterAssocOp : proved iter_op with function exponential
Jade Philipoom
2016-03-03
*
tweak to NumTheoryUtil so it builds on older Coq versions
Jade Philipoom
2016-03-03
*
generic binary exponentiation correctness proof in 3 one-liners
Andres Erbsen
2016-02-26
*
ModularArithmetic: reasonable-time FieldToZ inv implementation
Andres Erbsen
2016-02-26
*
Factor out some bedrock dependencies into WordUtil
Jason Gross
2016-02-25
*
a few lemmas in util about powers of 2 in Bedrock's various rewritten forms
Jade Philipoom
2016-02-15
*
tweaks to util files, including automation for proving positivity/nonnegativi...
Jade Philipoom
2016-02-15
*
GaloisTheory: added lemmas useful for proving Euler's Criterion with GF. NumT...
Jade Philipoom
2016-02-02
*
NumTheoryUtil: proved Fermat's Little Theorem.
Jade Philipoom
2016-01-23
*
NumTheoryUtil : code cleanup; moved some lemmas to ZUtil.
Jade Philipoom
2016-01-23
*
Import coqprime; use it to prove Euler's criterion.
Jade Philipoom
2016-01-20
*
Merge branch 'master' of github.mit.edu:plv/fiat-crypto
Jade Philipoom
2016-01-13
|
\
*
|
euler's criterion reduced to fermat's little theorem and two lemmas about pri...
Jade Philipoom
2016-01-13
[next]