index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Util
/
NatUtil.v
Commit message (
Expand
)
Author
Age
*
Add transparent equality proofs for fixed wordT
Jason Gross
2017-01-21
*
Add nat_beq_to_eq
Jason Gross
2017-01-19
*
Fix 8.4 build issue
Jason Gross
2016-10-23
*
Prove an admitted NatUtil lemma
Jason Gross
2016-10-23
*
integrate bitwise operations
Andres Erbsen
2016-10-12
*
Equality for nat in natutil
Jason Gross
2016-09-16
*
Add natutil
Jason Gross
2016-08-16
*
Convert defined and mostly proven, modulo several admitted lemmas about Z ope...
jadep
2016-08-09
*
Fix 8.4 build.
jadep
2016-07-25
*
A couple new util lemmas
jadep
2016-07-25
*
Add another lemma about +, <= to arith
Jason Gross
2016-07-20
*
Fix for Coq 8.4 (omega used to be weaker)
Jason Gross
2016-07-18
*
Add more natsimplify le_dec lemmas
Jason Gross
2016-07-18
*
Add more NatUtil lemmas
Jason Gross
2016-07-18
*
Add natsimplify lemmas about eq_nat_dec
Jason Gross
2016-07-18
*
Added lemmas to ZUtil and NatUtil (for Testbit)
jadep
2016-07-18
*
Fix NatUtil for 8.4
Jason Gross
2016-07-08
*
Add useful tactics and util lemmas
Jason Gross
2016-07-08
*
Add a NatUtil lemma and db
Jason Gross
2016-07-08
*
Fix ListUtil for Coq 8.4
Jason Gross
2016-07-07
*
Add [update_nth] to ListUtil, change [set_nth]
Jason Gross
2016-07-06
*
Prove that a ^ k <> 0
Jason Gross
2016-06-30
*
Merge
jadep
2016-06-14
|
\
*
|
progress on second stage (conditional constant-time subtraction) of canonical...
jadep
2016-06-13
|
*
8.5 fixes
Jason Gross
2016-06-10
|
/
*
moved lemmas from ModularBaseSystemProofs to various Util files
jadep
2016-04-20
*
Finish absolutizing imports
Jason Gross
2016-03-10
*
Factor out some bedrock dependencies into WordUtil
Jason Gross
2016-02-25
*
a few lemmas in util about powers of 2 in Bedrock's various rewritten forms
Jade Philipoom
2016-02-15
*
Util: added util lemmas needed to instantiate EdDSA25519.
Jade Philipoom
2016-01-05