index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
BoundedArithmetic
Commit message (
Expand
)
Author
Age
*
Add src/BoundedArithmetic/Eta.v
Jason Gross
2016-10-13
*
Fix for missing Nat.log2 in 8.4
Jason Gross
2016-10-11
*
Fix for missing Nat.log2 in 8.4
Jason Gross
2016-10-11
*
Add some admitted x86->ZLike proofs
Jason Gross
2016-10-10
*
Work around bug 5003 (broken omega on projections)
Jason Gross
2016-10-10
*
Add definitions for x86
Jason Gross
2016-10-10
*
Add repeated multiple
Jason Gross
2016-10-10
*
Add shl,shr,shrd to repeated doubling
Jason Gross
2016-10-09
*
Add proofs for doubling shl,shr,shrd
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
*
Add testbit_add_shiftl_full
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
*
Add some doubling constructions to bounded arith
Jason Gross
2016-10-04
*
Add some more instructions
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
*
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
*
Work around bug #5112 ([Arguments id /] broken)
Jason Gross
2016-09-30
*
More map -> List.map
Jason Gross
2016-09-29
*
Add a comment with an example
Jason Gross
2016-09-26
*
Drop CSE from Fancy Machine
Jason Gross
2016-09-22
*
Use dlet, not llet
Jason Gross
2016-09-22
*
Don't inline everything in Montgomery and Barrett
Jason Gross
2016-09-22
*
Integrate suggestions from Andres
Jason Gross
2016-08-25
*
Rework bounded proofs
Jason Gross
2016-08-24
*
More slight cleanups
Jason Gross
2016-08-24
*
Clean up DoubleBounded
Jason Gross
2016-08-24
*
Coq 8.4 fixes
Jason Gross
2016-08-24
*
Weaken the condition on smaller_bound
Jason Gross
2016-08-23
*
Hook up the bounded interface, finish proofs
Jason Gross
2016-08-23
*
Revert "Add _valid properties"
Jason Gross
2016-08-23
*
Add _valid properties
Jason Gross
2016-08-23
*
Fix some things
Jason Gross
2016-08-23
*
Add TODO
Jason Gross
2016-08-23
*
Rework interface to support rewriting database
Jason Gross
2016-08-23
*
alternative machine interface specification proposal
Andres Erbsen
2016-08-23
*
Initial work on an architecture interface for ℤ/nℤ
Jason Gross
2016-08-23