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
...
*
Move ContextOk to ContextDefinitions
Jason Gross
2017-03-14
*
Add lemma about wff and interpf of Named
Jason Gross
2017-03-14
*
Add faster versions of destruct_head_*
Jason Gross
2017-03-14
*
Fix more unfolding
Jason Gross
2017-03-10
*
Fix more unfolding that shouldn't happen
Jason Gross
2017-03-10
*
Make sure interp_flat_type isn't unfolded in SmartMap
Jason Gross
2017-03-10
*
Add better SmartFlatTypeMapInterp2
Jason Gross
2017-03-08
*
Remove interp_genf from Named/Syntax
Jason Gross
2017-03-08
*
Remove stuff from Reflection/Named/Syntax
Jason Gross
2017-03-08
*
Add FMapContext, PositiveContext
Jason Gross
2017-03-08
*
Remove display .vo from default target
Jason Gross
2017-03-06
*
Fixes #127
jadep
2017-03-06
*
JavaDisplay depends on JavaNotations, not CNotations
Jason Gross
2017-03-06
*
Remove assert_preconditions; prove ring-ness of basesystem operations for bas...
jadep
2017-03-04
*
Separated out specific test cases for new base system
jadep
2017-03-04
*
Fixed admit left from fsatz port
jadep
2017-03-02
*
make 8.5 happy
Andres Erbsen
2017-03-02
*
fixup NewBasesystem
Andres Erbsen
2017-03-02
*
remove dangling file...
Andres Erbsen
2017-03-02
*
remove dangling file that gives a warning
Andres Erbsen
2017-03-02
*
remove undeclared lines from Ed25519Extraction.v
Andres Erbsen
2017-03-02
*
move large non-building chunks of Ed25519.v
Andres Erbsen
2017-03-02
*
deleted src/Specific/GF25519ExtendedAddCoordinates.v
Andres Erbsen
2017-03-02
*
fix src/Specific/GF25519Reflective/Reified/AddCoordinates.v
Andres Erbsen
2017-03-02
*
remove PointEncoding
Andres Erbsen
2017-03-02
*
CompleteEdwardsCurveTheorems: point compression
Andres Erbsen
2017-03-02
*
PrimeFieldTheorems: inv for isomorphic fields
Andres Erbsen
2017-03-02
*
use [positive] for [F] modulus, char_ge_C instead of char_gt_C
Andres Erbsen
2017-03-02
*
rewrite ExtendedCoordinates, fix Ed25519
Andres Erbsen
2017-03-02
*
edwards curves over isomorphic fields
Andres Erbsen
2017-03-02
*
src/Tactics/Algebra_syntax/Nsatz.v: power 1 only
Andres Erbsen
2017-03-02
*
WIP
Andres Erbsen
2017-03-02
*
address some code review comments
Andres Erbsen
2017-03-02
*
Weierstrass curve is a group
Andres Erbsen
2017-03-02
*
Attempt Weierstrass associativity again, good progress.
Andres Erbsen
2017-03-02
*
change weierstrass spec, prove most cases of associativity
Andres Erbsen
2017-03-02
*
split the algebra library; use fsatz more
Andres Erbsen
2017-03-02
*
fsatz, nsatz_solve_nonzero
Andres Erbsen
2017-03-02
*
use field_nsatz in CompleteEdwardsCurve.Pre
Andres Erbsen
2017-03-02
*
field_nsatz
Andres Erbsen
2017-03-02
*
make assert_preconditions way more sane; use vm_decide to kill most subgoals
jadep
2017-03-02
*
Separated out [carry] from other operations.
jadep
2017-03-02
*
Modify/add to NewBaseSystem to match with what is needed for proof of ring is...
jadep
2017-03-01
*
Fixed carry bugs (indexes need to be reversed, and we need to convert to/from...
jadep
2017-03-01
*
Defined [div] and [mod]; removed liftn_sig lemmas because they were actually ...
jadep
2017-03-01
*
Adjust implicits of flatten_binding_list_same_in_eq
Jason Gross
2017-03-01
*
Add flatten_binding_list_In_eq_iff, flatten_binding_list_same_in_eq
Jason Gross
2017-03-01
*
Add η principles for sigma types
Jason Gross
2017-03-01
*
Add dlet_nd notation
Jason Gross
2017-03-01
*
Switch to fully uncurried form for reflection
Jason Gross
2017-03-01
[prev]
[next]