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
*
Add a Ztestbit_full database
Jason Gross
2016-10-09
*
Some work on x86 and bounded repeated things
Jason Gross
2016-10-09
*
Add some bounded decode/and things
Jason Gross
2016-10-09
*
Split up DoubleBoundedProofs, add proofs
Jason Gross
2016-10-07
*
Stronger Ztestbit, convert_to_ztestbit
Jason Gross
2016-10-07
*
More zsimplify lemmas, stronger Ztestbit
Jason Gross
2016-10-07
*
Add eta_expand to Prod.v
Jason Gross
2016-10-07
*
Add a variant of [map] on reflective things that changes the interp function
Jason Gross
2016-10-07
*
Weaken hyps of lor_range, add it to zarith
Jason Gross
2016-10-07
*
Moved lemma to ZUtil and added an extra lemma jgross needed
jadep
2016-10-06
*
Add testbit_add_shiftl_full
Jason Gross
2016-10-06
*
Use zutil_arith for side-conditions in testbit
Jason Gross
2016-10-06
*
Add Z.pow_le_mono_{r,l} to zarith
Jason Gross
2016-10-06
*
Add a lemma to Ztestbit about large indices
Jason Gross
2016-10-06
*
Do shl, shr doubling in terms of or
Jason Gross
2016-10-06
*
Add more bounded assembly lemmas
Jason Gross
2016-10-06
*
Moved PointEncoding out of Spec
jadep
2016-10-06
*
Fixed a lingering inappropriate use of Logic.eq
jadep
2016-10-06
*
Moved conversion logic out of Pow2BaseProofs into its own file
jadep
2016-10-06
*
More zsimplify lemmas
Jason Gross
2016-10-04
*
Add Zplus_minus to zsimplify
Jason Gross
2016-10-04
*
Weaken hyps of zutil lemma
Jason Gross
2016-10-04
*
Add a variant of add_shift_mod
Jason Gross
2016-10-04
*
Add some doubling constructions to bounded arith
Jason Gross
2016-10-04
*
Add ZUtil lemma
Jason Gross
2016-10-04
*
Add ZUtil lemma
Jason Gross
2016-10-04
*
Add Zmult_lt_compat_r to zarith
Jason Gross
2016-10-04
*
Prevent infinite loops by not dealing with 0 mod _
Jason Gross
2016-10-04
*
Handle 0 mod _ in push_Zmod
Jason Gross
2016-10-04
*
Handle ?x mod ?x in push_Zmod
Jason Gross
2016-10-04
*
Add some more instructions
Jason Gross
2016-10-04
*
Z.ltb_to_lt now also handles eqb
Jason Gross
2016-10-04
*
Add instructions with carry flags
Jason Gross
2016-10-04
*
Add spec for x86 (#72)
Jason Gross
2016-10-04
*
fix 8.4 build
jadep
2016-10-03
*
A couple hotfixes; recent commits somehow broke things
jadep
2016-10-03
*
Wrote proofs necessary to fill in all point-encoding related context variable...
jadep
2016-10-03
*
Add bitwise and, remove mkl from fancy
Jason Gross
2016-10-03
*
Work around bug 5107 (broken return inference)
Jason Gross
2016-10-03
*
Work around bug #5112 ([Arguments id /] broken)
Jason Gross
2016-10-03
*
Ed25519: use Global Instance
Andres Erbsen
2016-10-03
*
Spec: add ed25519
Andres Erbsen
2016-10-03
*
Fix a spelling typo
Jason Gross
2016-10-02
*
Add homomorphism composition
Jason Gross
2016-09-30
*
Add group and homomorphism lemmas
Jason Gross
2016-09-30
*
Weaken surjective_homomorphism_from_group
Jason Gross
2016-09-30
*
Work around bug #5112 ([Arguments id /] broken)
Jason Gross
2016-09-30
*
Silence warnings about Require in GenericFieldPow
Jason Gross
2016-09-30
*
More map -> List.map
Jason Gross
2016-09-29
*
map -> List.map (not Tuple.map)
Jason Gross
2016-09-29
[next]