--- Day changed Thu Jul 05 2018
00:04 -!- kallewoof_ [~quassel@fp96f94c66.tkyc515.ap.nuro.jp] has joined #secp256k1     
00:06 -!- kallewoof [~kallewoof@240d:1a:759:6000:a7b1:451a:8874:e1ac] has quit [Quit: WeeChat 1.9.1]     
00:06 -!- kallewoof_ is now known as kallewoof     
02:56 -!- luke-jr [~luke-jr@unaffiliated/luke-jr] has quit [Ping timeout: 240 seconds]     
03:08 -!- luke-jr [~luke-jr@unaffiliated/luke-jr] has joined #secp256k1     
04:53 -!- luke-jr [~luke-jr@unaffiliated/luke-jr] has quit [Ping timeout: 264 seconds]     
04:53 -!- luke-jr [~luke-jr@unaffiliated/luke-jr] has joined #secp256k1     
05:30 -!- belcher_ [~belcher@unaffiliated/belcher] has joined #secp256k1     
08:34 < andytoshi> bluematt notices that we call `secp256k1_ecmult_gen_blind` at the end of `secp256k1_ecmult_gen_context_build` regardless of whether we do static precomp or not
08:34 < andytoshi> which means that `context_create` is not threadsafe when static precomputation is used
10:55 -!- deusexbeer [~deusexbee@095-129-175-145-dynamic-pool-adsl.wbt.ru] has quit [Ping timeout: 264 seconds]     
10:56 -!- deusexbeer [~deusexbee@095-129-170-014-dynamic-pool-adsl.wbt.ru] has joined #secp256k1     
11:05 < gmaxwell> We really need to get a setup going so we can measure sidechannels. Otherwise our improvements are all just flying blind.
11:10 -!- belcher_ [~belcher@unaffiliated/belcher] has quit [Ping timeout: 256 seconds]     
11:23 < gmaxwell> andytoshi: I can't figure out what you're saying there?  You were expecting multiple threads should be able to create() on the same context object and/or someone should be able to create a context object while someone else uses it?
11:24 < gmaxwell> At first I thought you were saying that create was mutating the static data, and I was horrified, but I see it was not.
11:31 < sipa> andytoshi: context_create creates a new object; by definition no other thread can have access to it before it's returned
11:31 < sipa> so it's implicitly thread safe
12:20 -!- deusexbeer [~deusexbee@095-129-170-014-dynamic-pool-adsl.wbt.ru] has quit [Ping timeout: 240 seconds]     
12:21 -!- deusexbeer [~deusexbee@080-250-076-058-dynamic-pool-adsl.wbt.ru] has joined #secp256k1     
12:21 -!- belcher_ [~belcher@unaffiliated/belcher] has joined #secp256k1     
12:32 -!- deusexbeer [~deusexbee@080-250-076-058-dynamic-pool-adsl.wbt.ru] has quit [Quit: Konversation terminated!]     
13:05 < andytoshi> ah, yeh, i'm an idiot
13:05 < andytoshi> i thought it was mutating the static data
13:06 < roconnor_> I've completed my verification of secp256k1_fe_mul_inner from field_10x26_impl.h using Verified C, at least as far as you can go using Verified C.
13:06 < andytoshi> sipa: not entirely, in the case of static precomp
13:07 < roconnor_> For those interested, I have a trimmed file @ https://www.pastery.net/prpqbr/ that removes the long proof and shows the specification and relevent lemmas and definitions.
13:07 < sipa> andytoshi: how so?
13:08 < andytoshi> sipa: with static precomp the returned context object has a pointer into static data, and every context object will have the same pointer
13:08 < roconnor_> This week I completed the correctness lemmas of the functional implmentation showing that it produces a correct representative and the respresenative has magnitude 1.
13:08 < sipa> andytoshi: so?
13:08 < roconnor_> This combined with last weeks proof showing that the C code is a refinement of the functional implementation completes the proof.
13:09 < andytoshi> sipa: so it's not "by definition" that context_create is threadsafe
13:09 < andytoshi> it's because it's careful not to mutate anything related to the static data
13:09 < sipa> andytoshi: it's a pointer to constant data; if it's modified, that's UB; if it isn't modified, it doesn't need synchronization
13:10 < roconnor_> of course, I didn't expect there to be a bugs in the implementation.  This was mostly an exercise in using Verified C.
13:11 < andytoshi> sipa: oh, ok, i didn't see that it was constant
13:11 < andytoshi> it's not a constant pointer.
13:11 < andytoshi> roconnor_: awesome :)
13:12 < sipa> andytoshi: it's not a constant pointer? hmm
13:12 < andytoshi> yeah, i think we could change that, it'd just be an extra couple of lines of conditional compilation
13:12 < andytoshi> anyway, the reason i bring this up is that matt and i were talking about making the whole context object static so that the static precomp mode would involve no mallocing at all
13:13 < andytoshi> or alternately, providing a way through the API to change malloc
13:13 < sipa> right, there could be a fully static precomputed ctx object
13:35 -!- deusexbeer [~deusexbee@080-250-076-058-dynamic-pool-adsl.wbt.ru] has joined #secp256k1     
13:54 < nickler> roconnor_: very nice. Are there parts where you see a higher likelihood of bugs (f.e. newer code) that can be verified in a similar way without requiring an unreasonable amount of effort?
14:04 < roconnor_> I'm not so familiar with the libsecp256k1 development, so I don't know if I can answer the question myself.
14:05 < roconnor_> It's a bit unclear what unreasonable effort is.  I have tenative plans to continue validation of the library in the future.  As I build up this work, I'll end up with suitable definitions in Coq to make proofs easier.
14:05 < roconnor_> But it isn't clear to me yet how easy it will end up.
14:06 < roconnor_> I can say, that this C codes is pretty easy to verify in that there are essentially no loops and everything is straight line code.
14:06 < roconnor_> It's about as nice from a verification standpoint as you can get.
14:07 < roconnor_> In fact, because it is so nice, there might be alternative verification tools that are more suitable for this task than a general purpose tool like Verified C.
14:09 < nickler> Would verification of scalar multiplication make sense?
14:09 < roconnor_> absolutely.
14:12 -!- reallll [~belcher@unaffiliated/belcher] has joined #secp256k1     
14:14 -!- belcher_ [~belcher@unaffiliated/belcher] has quit [Ping timeout: 256 seconds]     
14:17 -!- reallll [~belcher@unaffiliated/belcher] has quit [Ping timeout: 256 seconds]     
14:31 < gmaxwell> roconnor_: we did write it with it being analyizable as a goal too... If you have feedback on things which are easier or harder to deal with we'd like to hear it.
14:32 < gmaxwell> andytoshi: we have a way through defines to change malloc.
14:33 < gmaxwell> but not the api. I generally feel kinda sad about function pointers in general, as they're oppturnities to redirect control flow.
14:34 < gmaxwell> andytoshi: so we can't make it totally static without killing the ability to have any randomization at all... that would be kind of sad.
14:34 < andytoshi> though #defines is probably fine
14:35 < andytoshi> yeah, that's very frustrating
14:35 < gmaxwell> OTOH we don't really have any way to gauge the value of the randomization.
14:50 < roconnor_> gmaxwell: I don't have much feedback.  Everything was more or less fine.  It was particularly useful that there is a point in the code (about line 733) where secp256k1_fe_mul_inner switches from reading from the `a` array to writing to the `r` array and there is no overlap.
14:50 < roconnor_> I suppose it would be hard to write it any other way though.
14:51 < roconnor_> It was useful in that it made reasoning about the possible aliasing between `a` and `r` not so bad.
15:43 < maaku> how do you efficiently check if R.y is a quadratic residue?
15:44 < sipa> you can compute its Jacobi symbol mod p
15:44 < sipa> which is faster than computing an inverse
15:44 < sipa> (but not much)
15:46 < maaku> wait you can use the inverse to do this? am i missing something obvious?
15:46 < gmaxwell> if you were making a code size at all costs implementation, you can use the sqrt to perform the test.
15:46 < sipa> no     
15:46 < gmaxwell> (which you'd have for computing y for public keys.
15:46 < gmaxwell> )     
15:47 < maaku> oh ok you're just comparing efficiency, i see
15:47 < maaku> thanks sipa, gmaxwell
15:48 < gmaxwell> maaku: well also you implement a fast inverse and a jacobi symbol very similarly. (using extgcd)
15:48 < sipa> maaku: Jacobi symbol is defined as a ** ((p-1)/2) mod p
15:48 < sipa> but there are more efficient ways of computing it
15:48 < sipa> gmaxwell: jacobi is even simpler due to not needing to rewind the extgcd to get the actual inverse out
15:49 < sipa> at least in theory
15:51 < gmaxwell> We should probably include in the BIP as appendexes how to compute the jacobi symbol.
15:52 < gmaxwell> And give examples using power, extgcd, and sqrt.
15:52 < gmaxwell> lest we get someone complaining because they don't know how to implement it.
16:08 < maaku> has anyone implemented batch verification for secp256k1 yet?
16:15 < andytoshi> for musig?
16:15 < andytoshi> err schnorr
16:16 < andytoshi> yes https://github.com/apoelstra/secp256k1/blob/2018-04-taproot/src/modules/musig/main_impl.h#L708
21:40 -!- ynakasone [~ynakasone@zz2014411797B6F89E82.userreverse.dion.ne.jp] has joined #secp256k1     
21:59 -!- ynakasone [~ynakasone@zz2014411797B6F89E82.userreverse.dion.ne.jp] has quit []