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
*
Fix [sqrtW_sig]
Jason Gross
2016-11-02
*
Changes to sqrt for easier bounds proofs; currently blocked on broken proof i...
jadep
2016-11-02
*
Progress proving ERepDec_correct (included tweaking preconditions for Modular...
jadep
2016-11-02
*
Fixed reversed tuple in feDec
jadep
2016-11-02
*
Add a ZUtil lemma
Jason Gross
2016-11-02
*
Prove fe25519WToZ_ZToW, rename FooToBarToFoo to BarToFoo_FooToBar
Jason Gross
2016-11-01
*
Export strings in GF25519Reflective/Common
Jason Gross
2016-11-01
*
Fix and prove bounds for cmovne, cmovle; note a problem with the neg bound
Jason Gross
2016-11-01
*
Print out the computed bounds on the various ops
Jason Gross
2016-11-01
*
Parameterize bounded things over the limb length
Jason Gross
2016-11-01
*
Add fe25519WToZToW
Jason Gross
2016-11-01
*
Change hlist implicit status
Jason Gross
2016-11-01
*
Work around bug #5175 in 8.6
Jason Gross
2016-11-01
*
Move hlist to new file
Jason Gross
2016-11-01
*
Fix a typo in the previous commit
Jason Gross
2016-11-01
*
Generalize hlist
Jason Gross
2016-11-01
*
Add hlist to tuple
Jason Gross
2016-11-01
*
Make it easier to extract word64
Jason Gross
2016-10-31
*
Add version of [Apply] for [Interp] things
Jason Gross
2016-10-31
*
Add bounds type in Specific/GF25519Reflective/Common.v
Jason Gross
2016-10-31
*
Add Reflection.Application
Jason Gross
2016-10-31
*
Add SmartVarMap_hetero
Jason Gross
2016-10-31
*
Add some interpretations things, speed up proofs in Ed25519
Jason Gross
2016-10-31
*
Add [f] to things that use [exprf] or [flat_type]
Jason Gross
2016-10-31
*
Implicits for SmartVarMapT
Jason Gross
2016-10-31
*
Make it so that changing the list of wire bounds doesn't break the build
Jason Gross
2016-10-31
*
Add SmartVarMapT
Jason Gross
2016-10-31
*
Revert "Switch from word to Z"
Jason Gross
2016-10-31
*
Switch from word to Z
Jason Gross
2016-10-31
*
Switch to reflective bounded word in Ed25519
Jason Gross
2016-10-31
*
Safer definitions of shl, shr
Jason Gross
2016-10-31
*
Fix a typo making word calculations wrong
Jason Gross
2016-10-31
*
Use sigma types to fix extraction
Jason Gross
2016-10-31
*
Silence a warning
Jason Gross
2016-10-31
*
Significantly faster wordToN, I hope
Jason Gross
2016-10-31
*
Add src/Specific/GF25519Reflective.v
Jason Gross
2016-10-31
*
Interpret syntax with Let_In
Jason Gross
2016-10-31
*
Also construct relatedness proofs in reified
Jason Gross
2016-10-30
*
Fix tactic notation scope in the 8.5 build
Jason Gross
2016-10-30
*
Fix for 8.5 build?
Jason Gross
2016-10-30
*
Proved eq_enc_E_iff
jadep
2016-10-30
*
Fix some subtleties with equalities in point encodings
jadep
2016-10-30
*
Added new algebra lemma
jadep
2016-10-30
*
Remove an [About]
Jason Gross
2016-10-30
*
Renaming in Reflection/Z/Interpretations.v, admitted rel lemmas
Jason Gross
2016-10-30
*
Switch to a faster way of proving wf
Jason Gross
2016-10-30
*
Add trueify to src/Util/PartiallyReifiedProp.v
Jason Gross
2016-10-30
*
Add to_prop_and_reified_Prop
Jason Gross
2016-10-30
*
Add break_innermost_match
Jason Gross
2016-10-30
*
Fix a loop in PartiallyReifiedProp
Jason Gross
2016-10-30
[next]