--- Day changed Thu Jun 28 2018 02:17 -!- meshcollider [uid246294@gateway/web/irccloud.com/x-ousphcxwzteoczwe] has quit [Quit: Connection closed for inactivity] 02:42 -!- arubi [~ese168@gateway/tor-sasl/ese168] has quit [Ping timeout: 250 seconds] 02:47 -!- arubi [~ese168@gateway/tor-sasl/ese168] has joined #secp256k1 03:09 -!- jtimon [~quassel@40.28.134.37.dynamic.jazztel.es] has joined #secp256k1 06:54 -!- roconnor [~roconnor@host-45-58-224-191.dyn.295.ca] has joined #secp256k1 07:13 -!- roconnor [~roconnor@host-45-58-224-191.dyn.295.ca] has quit [Ping timeout: 256 seconds] 07:28 -!- echonaut8 [~echonaut@46.101.192.134] has joined #secp256k1 07:28 -!- echonaut [~echonaut@46.101.192.134] has quit [Read error: Connection reset by peer] 07:35 -!- roconnor [~roconnor@host-45-58-224-191.dyn.295.ca] has joined #secp256k1 07:54 -!- belcher [~belcher@unaffiliated/belcher] has joined #secp256k1 09:01 -!- jtimon [~quassel@40.28.134.37.dynamic.jazztel.es] has quit [Ping timeout: 265 seconds] 10:40 -!- jtimon [~quassel@40.28.134.37.dynamic.jazztel.es] has joined #secp256k1 11:27 < roconnor> I've made it through my refinement proof for 10x26's secp256k1_fe_mul_inner while getting away with only a magnitude 10 precondition on the two inputs! 11:48 -!- belcher_ [~belcher@unaffiliated/belcher] has joined #secp256k1 11:51 -!- belcher [~belcher@unaffiliated/belcher] has quit [Ping timeout: 256 seconds] 12:05 -!- meshcollider [uid246294@gateway/web/irccloud.com/x-avzqsjlevhfuefdx] has joined #secp256k1 13:26 < andytoshi> wow, very cool 13:53 < roconnor> the refinement shows that my implementation of the field multiplication algorithm in Coq is equivalent to what is computed in C. 13:54 < roconnor> Next I need to show that my functional implementation is correct, and that will imply the C program is correct. 13:54 < roconnor> s/C program/C function/ 13:56 < roconnor> My Coq implementation opperates on mathematical integers, so the refinement proof demonstrates that there is no C integer overflow and nothing funny happens with the heap. 14:00 < andytoshi> awesome. i guess the heap stuff is straightforward since none of these functions use heap memory? 14:00 < andytoshi> oh, well, i guess they do index into arrays 14:01 -!- roconnor [~roconnor@host-45-58-224-191.dyn.295.ca] has quit [Ping timeout: 276 seconds] 14:12 < gmaxwell> roconnor: (when he comes back...) have you tried adding bugs to the C implementation and verifying that your proof no longer holds? 14:30 -!- roconnor [~roconnor@host-45-58-224-191.dyn.295.ca] has joined #secp256k1 14:32 < roconnor> andytoshi: The only thing tricky about the heap was trying to express that `r` and `a` may or may not be the same buffer. But that was mostly about separation logic rather than about the code itself. 14:32 < gmaxwell> 14:12:04 < gmaxwell> roconnor: (when he comes back...) have you tried adding bugs to the C implementation and verifying that your proof no longer holds? 14:32 < roconnor> gmaxwell: I'm not sure adding bugs will be useful. All but the most trival changes will just invalidate the proof. It is fairly tightly coupled to the code itself. 14:34 < roconnor> Keep in mind I haven't yet proven it correct; I've just proven it equivalent to a functional implementation in Coq. 14:34 < roconnor> So if there are some kinds of logical bugs, I've just duplicated them in my functional implementation. 14:34 < roconnor> (not that I'm expecting any bugs of course). 14:35 -!- meshcollider [uid246294@gateway/web/irccloud.com/x-avzqsjlevhfuefdx] has quit [Quit: Connection closed for inactivity] 14:46 < roconnor> Actually there are millions of other cavats: It only shows partial correctnes, not termination, it only really only proves it is compiled correctly by CompCert rather than any compliant C compiler, in particular it might still be invoking undefined behavour that CompCert has defined for itself, etc. etc. 14:47 < roconnor> For example, CompCert entirely ignores the register keyword AFAIU. 14:48 < gmaxwell> I don't think the register keyword is allowed to change program behavior... or am I confused? 14:49 < sipa> i believe so 14:49 < roconnor> Presumably a compliant C compiler is allowed to do whatever if you pass the same buffer to `a` and `b`. 14:50 < roconnor> where as in Verified C, you would be able to prove that mult "is correct" even if a and b are passed the same buffer. 14:50 < gmaxwell> you mean restrict not register. 14:50 < roconnor> er right sorry. 14:50 < roconnor> ha 14:51 < roconnor> my bad. 14:51 < sipa> restrict can only change behaviour from well specified to undefined 14:51 < roconnor> that' right. 14:52 < roconnor> But, Verified C ignores the restrict qualifier allowing you to prove facts about programs that are really undefined. 14:52 < roconnor> That all said, I did put it as part of the function spec that `b` is not allowed to alias with the other parameters. 14:53 < roconnor> but it would have been better if I was forced to do that. 15:04 -!- arubi [~ese168@gateway/tor-sasl/ese168] has quit [Remote host closed the connection] 15:04 -!- arubi [~ese168@gateway/tor-sasl/ese168] has joined #secp256k1 15:23 -!- roconnor [~roconnor@host-45-58-224-191.dyn.295.ca] has quit [Ping timeout: 260 seconds] 17:25 -!- instagibbs [~instagibb@pool-100-15-128-78.washdc.fios.verizon.net] has quit [Ping timeout: 256 seconds] 17:35 -!- instagibbs [~instagibb@pool-100-15-128-78.washdc.fios.verizon.net] has joined #secp256k1 17:58 -!- belcher_ [~belcher@unaffiliated/belcher] has quit [Quit: Leaving] 18:11 -!- roconnor [~roconnor@host-45-58-224-191.dyn.295.ca] has joined #secp256k1 19:21 -!- instagibbs [~instagibb@pool-100-15-128-78.washdc.fios.verizon.net] has quit [Ping timeout: 264 seconds] 19:29 -!- instagibbs [~instagibb@pool-100-15-128-78.washdc.fios.verizon.net] has joined #secp256k1 19:34 -!- instagibbs [~instagibb@pool-100-15-128-78.washdc.fios.verizon.net] has quit [Ping timeout: 260 seconds] 20:03 -!- instagibbs [~instagibb@pool-100-15-128-78.washdc.fios.verizon.net] has joined #secp256k1 21:16 -!- roconnor [~roconnor@host-45-58-224-191.dyn.295.ca] has quit [Ping timeout: 260 seconds] 21:21 -!- jtimon [~quassel@40.28.134.37.dynamic.jazztel.es] has quit [Ping timeout: 260 seconds] 21:21 -!- roconnor [~roconnor@host-45-58-224-191.dyn.295.ca] has joined #secp256k1 23:27 -!- echonaut8 [~echonaut@46.101.192.134] has quit [Read error: Connection reset by peer] 23:27 -!- echonaut [~echonaut@46.101.192.134] has joined #secp256k1