index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Reflection
Commit message (
Expand
)
Author
Age
*
: assert is not valid 8.4 syntax
Jason Gross
2016-11-17
*
Add Un{Return,Abs}_eta
Jason Gross
2016-11-16
*
Add : assert to a bunch of arguments
Jason Gross
2016-11-16
*
Split fixedpoint in interpf
Jason Gross
2016-11-16
*
Arguments for Un{Return,Abs}
Jason Gross
2016-11-16
*
Add UnReturn, UnAbs
Jason Gross
2016-11-16
*
Support for 128-bit words
Jason Gross
2016-11-14
*
Add word-size-independent interpretations
Jason Gross
2016-11-14
*
Fix reification of neg
Jason Gross
2016-11-11
*
Make [neg] a unary operation in reflection
Jason Gross
2016-11-11
*
Remove more conditional subtract
Jason Gross
2016-11-11
*
Remove extra conditional subtract things
Jason Gross
2016-11-11
*
Remove special code for reified conditional sub
Jason Gross
2016-11-11
*
More proof fixes
Jason Gross
2016-11-10
*
Minimize diff with master, fix some proofs that were broken
Jason Gross
2016-11-10
*
Merge with master
Rob Sloan
2016-11-09
|
\
|
*
Fix for 8.4
Jason Gross
2016-11-09
|
*
Switch to accurate bounds for lor
Jason Gross
2016-11-09
*
|
Rebase + remove WordizeUtil dependency from Z/Interpretations
Rob Sloan
2016-11-09
|
\
\
|
|
*
Remove last admitted lemma in src/Reflection/Z/Interpretations/Relations.v
Jason Gross
2016-11-09
|
|
/
*
|
Finished WordUtil, word operations in Z/Interpretation
Rob Sloan
2016-11-09
*
|
Not quite done with WordUtil lemmas.
Robert Sloan
2016-11-08
|
\
\
|
|
*
Fix for Coq 8.4
Jason Gross
2016-11-08
|
|
*
Some fixes for 8.4 differences
Jason Gross
2016-11-08
|
|
*
More progress on src/Reflection/Z/Interpretations/Relations.v
Jason Gross
2016-11-08
|
|
*
Fix 8.4 build ([value] is a constant)
Jason Gross
2016-11-08
|
|
/
|
*
Factor related_Z_op (except conditional_sub)
Jason Gross
2016-11-08
|
*
More factoring in related_Z_op
Jason Gross
2016-11-08
|
*
Fix some qualified name issues with previous commit
Jason Gross
2016-11-08
|
*
Add word64ToZ_{neg,cmovne,cmovle,conditional_subtract}
Jason Gross
2016-11-08
|
*
Remove lor admit in relations
Jason Gross
2016-11-08
|
*
Minor refactoring of related_Z_op
Jason Gross
2016-11-07
|
*
Finish related_bounds_t_map1_tuple2
Jason Gross
2016-11-07
|
*
More progress on related_bounds_t_map1_tuple2
Jason Gross
2016-11-07
|
*
More progress on t_map1_tuple2 lemmas
Jason Gross
2016-11-07
|
*
Add flat_interp_tuple_untuple'
Jason Gross
2016-11-07
|
*
Add flat_interp_untuple'_tuple
Jason Gross
2016-11-07
|
*
Some progress on Relations admits
Adam Chlipala
2016-11-07
|
*
More reorg in Reflection/Z/Interpretations/Relations.v
Jason Gross
2016-11-06
|
*
Do some of the related_Z_op proofs
Jason Gross
2016-11-06
|
*
Refactor various reflective things
Jason Gross
2016-11-06
|
*
Fixes for Coq 8.4
Jason Gross
2016-11-06
|
*
Preliminary support: conditional sub as primitive
Jason Gross
2016-11-06
|
*
Add syntactic tuples
Jason Gross
2016-11-06
|
*
Add support for dependent reification
Jason Gross
2016-11-06
|
*
More partial proofs
Jason Gross
2016-11-06
|
*
Prove inversion principles for bounded words
Jason Gross
2016-11-06
|
*
Add related_word64_boundsi'
Jason Gross
2016-11-05
|
*
Split off some things from Interpretations
Jason Gross
2016-11-05
|
*
Fix implicit arguments
Jason Gross
2016-11-05
[next]