--- Day changed Mon Jul 11 2016
01:37 -!- arubi [~ese168@unaffiliated/arubi] has quit [Ping timeout: 272 seconds]
01:41 -!- arubi [~ese168@unaffiliated/arubi] has joined #secp256k1
04:25 -!- jtimon [~quassel@55.31.134.37.dynamic.jazztel.es] has joined #secp256k1
04:40 -!- arubi [~ese168@unaffiliated/arubi] has quit [Quit: Leaving]
04:41 -!- arubi [~ese168@unaffiliated/arubi] has joined #secp256k1
04:54 -!- arubi [~ese168@unaffiliated/arubi] has quit [Quit: Leaving]
04:55 -!- arubi [~ese168@unaffiliated/arubi] has joined #secp256k1
09:36 -!- sipa [~pw@2a02:348:86:3011::1] has quit [Changing host]
09:36 -!- sipa [~pw@unaffiliated/sipa1024] has joined #secp256k1
10:30 -!- droark [~droark@c-24-22-36-12.hsd1.or.comcast.net] has joined #secp256k1
10:39 -!- mdavid613 [~Adium@cpe-172-251-161-231.socal.res.rr.com] has joined #secp256k1
12:49 -!- jtimon [~quassel@55.31.134.37.dynamic.jazztel.es] has quit [Ping timeout: 276 seconds]
13:27 -!- btcdrak [uid165369@gateway/web/irccloud.com/x-kccfrqpobwcfhmhs] has joined #secp256k1
13:59 -!- moli [~molly@unaffiliated/molly] has joined #secp256k1
14:01 -!- xinxi [~xinxi@116.86.156.222] has joined #secp256k1
14:01 < xinxi> hello
14:01 < sipa> hi there
14:01 < xinxi> can I see the verification code?
14:02 < sipa> it may not be what you expect
14:02 < sipa> i know gmaxwell verified the 32-bit field implementation with frama-c to guarantee there are no integer overflows in it
14:02 < xinxi> it does not really matter. I just want to take a look.
14:02 < sipa> i don't know where the code is for that, though
14:03 < xinxi> Oh, I thought it should be embedded in the C code.
14:03 < sipa> there is a (human written) proof for correctness (just algebraic reduction) for the field multiplication code
14:03 < sipa> we have algebraic verification in sage for the point addition rules
14:04 < sipa> (and if github wasn't down for me, i'd give you a link)
14:04 < xinxi> it's still online.
14:04 < sipa> yes, so people have told me
14:04 < sipa> i'm sure it's a problem on my side, but i can't access the site :)
14:05 < xinxi> I see. Where are you Pieter?
14:05 < sipa> oh, indeed; i had hardcoded the ip for github.com in /etc/hosts
14:05 < xinxi> Switzerland.
14:06 < sipa> https://github.com/bitcoin-core/secp256k1/blob/master/src/field_10x26_impl.h#L444
14:06 < sipa> the comments of the form /* [...] = [...] */ are equations that relate the input and output variables
14:07 < sipa> and together they're a (human verifiable) proof the code is correct, under the assumption that none of the integers ever overflow
14:07 < sipa> this is checked in two ways; 1) in debug mode using the VERIFY_BITS checks and 2) by gmaxwell using frama-c, though i wonder where the code for that ended up
14:09 < xinxi> pretty cool.
14:10 < xinxi> I guess all the code can be verified using frama-c?
14:10 < sipa> the other types of verification are more algebraic
14:10 < sipa> in the sage/ subdirectory there are translations of the group addition formulas
14:10 < sipa> to python
14:11 < sipa> whuch are then evaluated using sage, but by passing in symbolic variable objects rather than specific numbers
14:11 < xinxi> nice.
14:12 < sipa> and then sage can prove equivalence under certain conditions that they match the mathematical elliptiv curve equations
14:12 -!- mdavid613 [~Adium@cpe-172-251-161-231.socal.res.rr.com] has quit [Quit: Leaving.]
14:12 < xinxi> Yeah, I've used sage before. It has quite decent symbolic computing support.
14:13 < sipa> interestingly: we once had a bug in one of the addition formula, which andytoshi found using a unit test later on (with an incredible amount of luck, really)
14:13 < sipa> the sage verification was only added after fixing that bug
14:14 < sipa> but if we feed the old buggy implementation into the sage logic, it correctly identifies exactly the conditions under which it was failing
14:14 < xinxi> Does sage found other bugs?
14:14 < sipa> no
14:15 < sipa> it never found a bug; we can only retroactive prove we would have found the one bug we knew existed
14:15 < xinxi> Anyway, now you have the confidence.
14:15 < sipa> aside from that, we also use extensive unit testing
14:15 < sipa> where there are some interesting techniques
14:15 < xinxi> yeah, I love unit testing too.
14:16 < xinxi> I love testing driving programming.
14:16 < sipa> one is using random 256-bit integers that are generated using an algorithm that produces  number biased torwards large sequences of 0s and 1s in its binary representation
14:16 < sipa> which are much more likely to trigger edge cases
14:17 < sipa> and we actually found a bug in OpenSSL using those (by having code that compared the result of our internal numeric results, while those were still implemented on top of openssl's bignum)
14:17 < sipa> the BN_sqr bug, if you have heard about it
14:19 < xinxi> OpenSSL seems really buggy.
14:19 < xinxi> But it's so widely used.
14:19 < xinxi> BTW, what's your PHD topic?
14:22 < sipa> totally unrelated. i worked on a domain specific language in haskell to describe constraint satisfaction problems
14:22 < xinxi> Pieter, it's a really nice talk to you. But it's just too late here 5:22am. I have to go to bed and will talk to you tomorrow.
14:23 < xinxi> I worked on recommender systems, a branch of machine learning.
14:23 < xinxi> it's not very relevant either.
14:23 < xinxi> :-)
14:23 < xinxi> i still love AI though.
14:23 < sipa> haha
14:23 < xinxi> but there is just too much hype right now.
14:23 < sipa> agree :)
14:23 < instagibbs> ah, fellow AI person
14:23  * instagibbs fist bump
14:24 < xinxi> OK, talk to you later.
14:24 < sipa> nice talking to you as well
14:27 -!- pigeons [~pigeons@94.242.209.214] has joined #secp256k1
14:34 -!- xinxi [~xinxi@116.86.156.222] has quit [Remote host closed the connection]
14:38 -!- arubi [~ese168@unaffiliated/arubi] has quit [Ping timeout: 240 seconds]
14:42 -!- arubi [~ese168@unaffiliated/arubi] has joined #secp256k1
14:43 -!- xinxi [~xinxi@116.86.156.222] has joined #secp256k1
14:44 -!- moli [~molly@unaffiliated/molly] has quit [Ping timeout: 240 seconds]
14:47 -!- xinxi [~xinxi@116.86.156.222] has quit [Ping timeout: 250 seconds]
15:15 -!- mdavid613 [~Adium@cpe-172-251-161-231.socal.res.rr.com] has joined #secp256k1
15:34 < gmaxwell> sipa: there is no special code for the frama-c verification, just switches to configure frama-c. (which I think I pastebinned here a while back)
15:35 < sipa> ah, nice
15:51 -!- moli [~molly@unaffiliated/molly] has joined #secp256k1
18:39 -!- xinxi [~xinxi@116.86.156.222] has joined #secp256k1
18:40 -!- luke-jr [~luke-jr@unaffiliated/luke-jr] has quit [Read error: Connection reset by peer]
18:43 -!- xinxi [~xinxi@116.86.156.222] has quit [Ping timeout: 240 seconds]
18:55 -!- afk11 [~afk11@unaffiliated/afk11] has quit [Ping timeout: 246 seconds]
18:56 -!- afk11 [~afk11@109.255.154.81] has joined #secp256k1
18:56 -!- afk11 [~afk11@109.255.154.81] has quit [Changing host]
18:56 -!- afk11 [~afk11@unaffiliated/afk11] has joined #secp256k1
19:14 -!- mdavid613 [~Adium@cpe-172-251-161-231.socal.res.rr.com] has quit [Quit: Leaving.]
19:58 -!- eragmus [sid136308@gateway/web/irccloud.com/x-euknuprnwapdmjif] has joined #secp256k1
20:26 -!- xinxi [~xinxi@116.86.156.222] has joined #secp256k1
20:31 -!- xinxi [~xinxi@116.86.156.222] has quit [Ping timeout: 252 seconds]
21:16 -!- luke-jr [~luke-jr@unaffiliated/luke-jr] has joined #secp256k1
21:58 -!- xinxi [~xinxi@116.86.156.222] has joined #secp256k1
22:07 -!- xinxi [~xinxi@116.86.156.222] has quit [Ping timeout: 276 seconds]
22:08 -!- xinxi [~xinxi@116.86.156.222] has joined #secp256k1
22:27 -!- xinxi_ [~xinxi@116.86.156.222] has joined #secp256k1
22:27 -!- xinxi [~xinxi@116.86.156.222] has quit [Read error: Connection reset by peer]
22:47 -!- xinxi_ [~xinxi@116.86.156.222] has quit [Remote host closed the connection]
22:50 -!- xinxi [~xinxi@116.86.156.222] has joined #secp256k1
22:55 -!- xinxi [~xinxi@116.86.156.222] has quit [Ping timeout: 260 seconds]
23:26 -!- xinxi [~xinxi@116.86.156.222] has joined #secp256k1
23:47 -!- xinxi [~xinxi@116.86.156.222] has quit [Remote host closed the connection]
23:57 -!- xinxi [~xinxi@116.86.156.222] has joined #secp256k1