--- Log opened Wed Sep 26 00:00:19 2018 00:01 -!- Zenton [~user@unaffiliated/vicenteh] has quit [Ping timeout: 240 seconds] 00:14 < maaku> kanzure: roconnor's work proving the correctness of the sha2 jet in simplicity is probably relevant 00:18 -!- bitconner [~conner@c-73-170-56-77.hsd1.ca.comcast.net] has joined #bitcoin-wizards 00:38 -!- TheoStorm [~dnaleor@host-lzquwqj.cbn1.zeelandnet.nl] has quit [Ping timeout: 252 seconds] 00:41 -!- SopaXorzTaker [~SopaXorzT@unaffiliated/sopaxorztaker] has joined #bitcoin-wizards 00:43 -!- deusexbeer [~deusexbee@095-129-170-104-dynamic-pool-adsl.wbt.ru] has quit [Ping timeout: 252 seconds] 00:44 -!- deusexbeer [~deusexbee@079-170-138-066-dynamic-pool-adsl.wbt.ru] has joined #bitcoin-wizards 00:51 -!- TheoStorm [~dnaleor@host-lzquwqj.cbn1.zeelandnet.nl] has joined #bitcoin-wizards 00:58 -!- phwalkr [~phwalkr@192.32.61.94.rev.vodafone.pt] has joined #bitcoin-wizards 01:01 -!- setpill [~setpill@unaffiliated/setpill] has joined #bitcoin-wizards 01:03 -!- phwalkr [~phwalkr@192.32.61.94.rev.vodafone.pt] has quit [Ping timeout: 252 seconds] 01:06 -!- phwalkr [~phwalkr@192.32.61.94.rev.vodafone.pt] has joined #bitcoin-wizards 01:09 -!- TheoStorm [~dnaleor@host-lzquwqj.cbn1.zeelandnet.nl] has quit [Ping timeout: 260 seconds] 01:13 -!- TheoStorm [~dnaleor@host-lzquwqj.cbn1.zeelandnet.nl] has joined #bitcoin-wizards 01:40 -!- TheoStorm [~dnaleor@host-lzquwqj.cbn1.zeelandnet.nl] has quit [Ping timeout: 240 seconds] 01:43 -!- Zenton [~user@unaffiliated/vicenteh] has joined #bitcoin-wizards 01:52 -!- TheoStorm [~dnaleor@host-lzquwqj.cbn1.zeelandnet.nl] has joined #bitcoin-wizards 01:55 -!- SopaXorzTaker [~SopaXorzT@unaffiliated/sopaxorztaker] has quit [Remote host closed the connection] 02:10 -!- TheoStorm [~dnaleor@host-lzquwqj.cbn1.zeelandnet.nl] has quit [Ping timeout: 252 seconds] 02:12 -!- phwalkr [~phwalkr@192.32.61.94.rev.vodafone.pt] has quit [Ping timeout: 240 seconds] 02:19 -!- AaronvanW [~AaronvanW@unaffiliated/aaronvanw] has joined #bitcoin-wizards 02:23 -!- TheoStorm [~dnaleor@host-lzquwqj.cbn1.zeelandnet.nl] has joined #bitcoin-wizards 02:29 -!- TheoStorm [~dnaleor@host-lzquwqj.cbn1.zeelandnet.nl] has quit [Quit: Leaving] 02:29 -!- TheoStorm [~dnaleor@host-lzquwqj.cbn1.zeelandnet.nl] has joined #bitcoin-wizards 02:37 -!- phwalkr [~phwalkr@192.32.61.94.rev.vodafone.pt] has joined #bitcoin-wizards 02:48 -!- tombusby [~tombusby@gateway/tor-sasl/tombusby] has quit [Remote host closed the connection] 02:48 -!- tombusby [~tombusby@gateway/tor-sasl/tombusby] has joined #bitcoin-wizards 03:12 -!- belcher [~belcher@unaffiliated/belcher] has joined #bitcoin-wizards 03:13 -!- intcat [~zshlyk@gateway/tor-sasl/intcat] has quit [Ping timeout: 256 seconds] 03:15 -!- intcat [~zshlyk@gateway/tor-sasl/intcat] has joined #bitcoin-wizards 03:20 -!- thrmo [~thrmo@gateway/tor-sasl/thrmo] has joined #bitcoin-wizards 03:24 -!- Krellan [~Krellan@2601:640:4000:9258:1c1:5844:3ef1:ae96] has quit [Ping timeout: 252 seconds] 03:25 -!- Krellan [~Krellan@2601:640:4000:9258:1c1:5844:3ef1:ae96] has joined #bitcoin-wizards 03:27 -!- Zenton [~user@unaffiliated/vicenteh] has quit [Read error: Connection reset by peer] 03:27 -!- Zenton [~user@unaffiliated/vicenteh] has joined #bitcoin-wizards 03:44 -!- reallll [~belcher@unaffiliated/belcher] has joined #bitcoin-wizards 03:44 -!- reallll [~belcher@unaffiliated/belcher] has quit [Remote host closed the connection] 03:47 -!- belcher [~belcher@unaffiliated/belcher] has quit [Ping timeout: 245 seconds] 03:58 -!- belcher [~belcher@unaffiliated/belcher] has joined #bitcoin-wizards 04:10 -!- Chris_Stewart_5 [~chris@unaffiliated/chris-stewart-5/x-3612383] has joined #bitcoin-wizards 04:13 -!- phwalkr [~phwalkr@192.32.61.94.rev.vodafone.pt] has quit [Remote host closed the connection] 04:14 -!- phwalkr [~phwalkr@192.32.61.94.rev.vodafone.pt] has joined #bitcoin-wizards 04:18 -!- phwalkr [~phwalkr@192.32.61.94.rev.vodafone.pt] has quit [Ping timeout: 250 seconds] 04:20 -!- bildramer1 [~bildramer@p2003004D8D312900AC9BCCA14258DFA9.dip0.t-ipconnect.de] has joined #bitcoin-wizards 04:22 -!- bildramer [~bildramer@p2003004D8D312900A89B25B3523CE832.dip0.t-ipconnect.de] has quit [Ping timeout: 252 seconds] 04:24 -!- Krellan [~Krellan@2601:640:4000:9258:1c1:5844:3ef1:ae96] has quit [Ping timeout: 240 seconds] 04:25 -!- Guyver2 [~Guyver@guyver2.xs4all.nl] has joined #bitcoin-wizards 04:25 -!- Krellan [~Krellan@2601:640:4000:9258:1c1:5844:3ef1:ae96] has joined #bitcoin-wizards 04:25 -!- Guyver2_ [~Guyver@guyver2.xs4all.nl] has joined #bitcoin-wizards 04:26 -!- Guyver2_ [~Guyver@guyver2.xs4all.nl] has quit [Client Quit] 04:37 -!- Emcy [~Emcy@unaffiliated/emcy] has joined #bitcoin-wizards 04:44 -!- Emcy [~Emcy@unaffiliated/emcy] has quit [Read error: Connection reset by peer] 04:47 -!- Emcy [~Emcy@unaffiliated/emcy] has joined #bitcoin-wizards 05:08 -!- Chris_Stewart_5 [~chris@unaffiliated/chris-stewart-5/x-3612383] has quit [Ping timeout: 244 seconds] 05:09 -!- bitconner [~conner@c-73-170-56-77.hsd1.ca.comcast.net] has quit [Ping timeout: 245 seconds] 05:34 -!- dnaleor [~dnaleor@host-lzquwqj.cbn1.zeelandnet.nl] has joined #bitcoin-wizards 05:38 -!- elichai2 [uid212594@gateway/web/irccloud.com/x-mwggotwszylbocsc] has joined #bitcoin-wizards 05:38 -!- TheoStorm [~dnaleor@host-lzquwqj.cbn1.zeelandnet.nl] has quit [Ping timeout: 252 seconds] 05:40 -!- wildermind [uid300433@gateway/web/irccloud.com/x-dynacuzwtavcelxx] has joined #bitcoin-wizards 05:40 -!- Krellan [~Krellan@2601:640:4000:9258:1c1:5844:3ef1:ae96] has quit [Ping timeout: 260 seconds] 05:40 -!- Krellan [~Krellan@2601:640:4000:9258:1c1:5844:3ef1:ae96] has joined #bitcoin-wizards 05:42 -!- setpill [~setpill@unaffiliated/setpill] has quit [Quit: o/] 05:48 -!- phwalkr [~phwalkr@192.32.61.94.rev.vodafone.pt] has joined #bitcoin-wizards 05:52 -!- phwalkr [~phwalkr@192.32.61.94.rev.vodafone.pt] has quit [Ping timeout: 245 seconds] 06:02 -!- phwalkr [~phwalkr@192.32.61.94.rev.vodafone.pt] has joined #bitcoin-wizards 06:20 -!- rmwb [~rmwb@199.178.233.220.static.exetel.com.au] has quit [Ping timeout: 252 seconds] 06:23 -!- enemabandit [~enemaband@185.227.37.188.rev.vodafone.pt] has joined #bitcoin-wizards 06:26 -!- gertjaap [~gertjaap@88.208.3.158] has quit [Quit: ZNC 1.7.1 - https://znc.in] 06:27 -!- rh0nj [~rh0nj@136.243.139.96] has quit [Remote host closed the connection] 06:28 -!- rh0nj [~rh0nj@136.243.139.96] has joined #bitcoin-wizards 06:28 -!- gertjaap [uid322815@gateway/web/irccloud.com/x-mlsdkwtfgfbkvgmj] has joined #bitcoin-wizards 06:33 -!- Chris_Stewart_5 [~chris@unaffiliated/chris-stewart-5/x-3612383] has joined #bitcoin-wizards 06:58 -!- rmwb [~rmwb@199.178.233.220.static.exetel.com.au] has joined #bitcoin-wizards 07:02 -!- rmwb [~rmwb@199.178.233.220.static.exetel.com.au] has quit [Ping timeout: 250 seconds] 07:12 -!- michaelsdunn1 [~michaelsd@unaffiliated/michaelsdunn1] has joined #bitcoin-wizards 07:21 -!- SopaXorzTaker [~SopaXorzT@unaffiliated/sopaxorztaker] has joined #bitcoin-wizards 07:30 -!- phwalkr [~phwalkr@192.32.61.94.rev.vodafone.pt] has quit [Ping timeout: 264 seconds] 07:31 -!- tromp [~tromp@ip-217-103-3-94.ip.prioritytelecom.net] has quit [Remote host closed the connection] 07:32 -!- tromp [~tromp@ip-217-103-3-94.ip.prioritytelecom.net] has joined #bitcoin-wizards 07:32 -!- SopaXorzTaker [~SopaXorzT@unaffiliated/sopaxorztaker] has quit [Quit: Leaving] 07:34 -!- phwalkr [~phwalkr@192.32.61.94.rev.vodafone.pt] has joined #bitcoin-wizards 07:35 -!- rmwb [~rmwb@199.178.233.220.static.exetel.com.au] has joined #bitcoin-wizards 07:49 -!- rmwb [~rmwb@199.178.233.220.static.exetel.com.au] has quit [Ping timeout: 240 seconds] 08:05 -!- Krellan [~Krellan@2601:640:4000:9258:1c1:5844:3ef1:ae96] has quit [Read error: Connection reset by peer] 08:09 -!- Krellan [~Krellan@2601:640:4000:9258:1c1:5844:3ef1:ae96] has joined #bitcoin-wizards 08:13 -!- dnaleor [~dnaleor@host-lzquwqj.cbn1.zeelandnet.nl] has quit [Quit: Leaving] 08:15 -!- p0nziph0ne [p0nziph0ne@gateway/vpn/privateinternetaccess/p0nziph0ne] has quit [Ping timeout: 246 seconds] 08:16 -!- TheoStorm [~dnaleor@host-lzquwqj.cbn1.zeelandnet.nl] has joined #bitcoin-wizards 08:18 -!- Krellan [~Krellan@2601:640:4000:9258:1c1:5844:3ef1:ae96] has quit [Ping timeout: 250 seconds] 08:23 < roconnor> Over the summer I also did some evaluation of VerifiableC and verfied the correctness of libsecp256k1's 32-bit field multiplication implementation. 08:24 < roconnor> gmaxwell: compcert is probably also non-trivial, but I haven't looked at it carefully. 08:26 -!- p0nziph0ne [p0nziph0ne@gateway/vpn/privateinternetaccess/p0nziph0ne] has joined #bitcoin-wizards 08:28 -!- tromp [~tromp@ip-217-103-3-94.ip.prioritytelecom.net] has quit [Remote host closed the connection] 08:28 -!- tromp [~tromp@ip-217-103-3-94.ip.prioritytelecom.net] has joined #bitcoin-wizards 08:29 -!- phwalkr [~phwalkr@192.32.61.94.rev.vodafone.pt] has quit [Ping timeout: 264 seconds] 08:37 -!- phwalkr [~phwalkr@192.32.61.94.rev.vodafone.pt] has joined #bitcoin-wizards 08:39 -!- Krellan [~Krellan@2601:640:4000:9258:1c1:5844:3ef1:ae96] has joined #bitcoin-wizards 08:41 < roconnor> Of course even trivial things could be useful to verify, like which pointer arguments are allowed to alias and which ones aren't. 08:43 -!- Krellan [~Krellan@2601:640:4000:9258:1c1:5844:3ef1:ae96] has quit [Ping timeout: 250 seconds] 08:49 -!- Krellan [~Krellan@2601:640:4000:9258:1c1:5844:3ef1:ae96] has joined #bitcoin-wizards 08:50 -!- dougsland [~douglas@c-24-34-137-83.hsd1.nh.comcast.net] has joined #bitcoin-wizards 08:53 -!- m8tion [~user@88.190.249.49] has joined #bitcoin-wizards 08:54 -!- Krellan [~Krellan@2601:640:4000:9258:1c1:5844:3ef1:ae96] has quit [Ping timeout: 260 seconds] 08:54 -!- Krellan [~Krellan@2601:640:4000:9258:1c1:5844:3ef1:ae96] has joined #bitcoin-wizards 08:57 -!- m8tion [~user@88.190.249.49] has quit [Client Quit] 08:57 -!- m8tion [~user@88.190.249.49] has joined #bitcoin-wizards 08:59 -!- Krellan [~Krellan@2601:640:4000:9258:1c1:5844:3ef1:ae96] has quit [Ping timeout: 250 seconds] 09:00 -!- Krellan [~Krellan@2601:640:4000:9258:1c1:5844:3ef1:ae96] has joined #bitcoin-wizards 09:04 -!- m8tion [~user@88.190.249.49] has quit [Quit: Leaving] 09:15 -!- m8tion [~user@88.190.249.49] has joined #bitcoin-wizards 09:15 -!- rmwb [~rmwb@199.178.233.220.static.exetel.com.au] has joined #bitcoin-wizards 09:16 -!- m8tion [~user@88.190.249.49] has quit [Remote host closed the connection] 09:20 -!- Murch [~murch@50-200-105-218-static.hfc.comcastbusiness.net] has joined #bitcoin-wizards 09:22 -!- phwalkr [~phwalkr@192.32.61.94.rev.vodafone.pt] has quit [Remote host closed the connection] 09:25 -!- p0nziph0ne [p0nziph0ne@gateway/vpn/privateinternetaccess/p0nziph0ne] has quit [Quit: Leaving] 09:28 -!- m8tion [~user@88.190.249.49] has joined #bitcoin-wizards 09:28 -!- m8tion [~user@88.190.249.49] has quit [Client Quit] 09:28 -!- m8tion [~user@88.190.249.49] has joined #bitcoin-wizards 09:29 -!- m8tion [~user@88.190.249.49] has quit [Remote host closed the connection] 09:30 -!- Zenton [~user@unaffiliated/vicenteh] has quit [Ping timeout: 240 seconds] 09:32 -!- Chris_Stewart_5 [~chris@unaffiliated/chris-stewart-5/x-3612383] has quit [Quit: WeeChat 1.4] 09:33 -!- _tin [~tyn@73.93.141.255] has joined #bitcoin-wizards 09:33 -!- rmwb [~rmwb@199.178.233.220.static.exetel.com.au] has quit [Ping timeout: 260 seconds] 09:34 -!- morcos [~morcos@gateway/tor-sasl/morcos] has quit [Remote host closed the connection] 09:34 -!- morcos [~morcos@gateway/tor-sasl/morcos] has joined #bitcoin-wizards 09:36 -!- p0nziph0ne [p0nziph0ne@gateway/vpn/privateinternetaccess/p0nziph0ne] has joined #bitcoin-wizards 09:53 -!- phwalkr [~phwalkr@194.210.89.118] has joined #bitcoin-wizards 09:53 -!- enemabandit [~enemaband@185.227.37.188.rev.vodafone.pt] has quit [Ping timeout: 240 seconds] 09:54 -!- nehan_ [~nehan@c-73-17-151-171.hsd1.ma.comcast.net] has joined #bitcoin-wizards 09:55 -!- nehan_ [~nehan@c-73-17-151-171.hsd1.ma.comcast.net] has quit [Client Quit] 09:57 -!- phwalkr [~phwalkr@194.210.89.118] has quit [Ping timeout: 244 seconds] 09:58 -!- belcher [~belcher@unaffiliated/belcher] has quit [Quit: Leaving] 10:01 -!- phwalkr [~phwalkr@194.210.89.118] has joined #bitcoin-wizards 10:01 -!- phwalkr [~phwalkr@194.210.89.118] has quit [Read error: Connection reset by peer] 10:01 -!- phwalkr [~phwalkr@194.210.89.118] has joined #bitcoin-wizards 10:03 -!- _tin [~tyn@73.93.141.255] has quit [Ping timeout: 250 seconds] 10:05 -!- dougsland [~douglas@c-24-34-137-83.hsd1.nh.comcast.net] has quit [Ping timeout: 244 seconds] 10:07 -!- Krellan [~Krellan@2601:640:4000:9258:1c1:5844:3ef1:ae96] has quit [Ping timeout: 264 seconds] 10:08 -!- Krellan [~Krellan@2601:640:4000:9258:1c1:5844:3ef1:ae96] has joined #bitcoin-wizards 10:12 -!- enemabandit [~enemaband@16.77.54.77.rev.vodafone.pt] has joined #bitcoin-wizards 10:15 -!- enemabandit [~enemaband@16.77.54.77.rev.vodafone.pt] has quit [Client Quit] 10:17 -!- Krellan [~Krellan@2601:640:4000:9258:1c1:5844:3ef1:ae96] has quit [Ping timeout: 240 seconds] 10:17 -!- shesek [~shesek@bzq-84-110-234-213.red.bezeqint.net] has joined #bitcoin-wizards 10:17 -!- shesek [~shesek@bzq-84-110-234-213.red.bezeqint.net] has quit [Changing host] 10:17 -!- shesek [~shesek@unaffiliated/shesek] has joined #bitcoin-wizards 10:17 -!- Krellan [~Krellan@2601:640:4000:9258:1c1:5844:3ef1:ae96] has joined #bitcoin-wizards 10:19 < gmaxwell> 08:41:41 < roconnor> Of course even trivial things could be useful to verify, like which pointer arguments are allowed to alias and which ones aren't. 10:19 < gmaxwell> yes, there are a lot of things where less than cosmic properties are proven. 10:22 -!- phwalkr [~phwalkr@194.210.89.118] has quit [Ping timeout: 245 seconds] 10:22 -!- Krellan [~Krellan@2601:640:4000:9258:1c1:5844:3ef1:ae96] has quit [Ping timeout: 250 seconds] 10:23 -!- phwalkr [~phwalkr@194.210.89.118] has joined #bitcoin-wizards 10:27 -!- Krellan [~Krellan@2601:640:4000:9258:1c1:5844:3ef1:ae96] has joined #bitcoin-wizards 10:34 -!- Zenton [~user@unaffiliated/vicenteh] has joined #bitcoin-wizards 10:41 -!- deusexbeer [~deusexbee@079-170-138-066-dynamic-pool-adsl.wbt.ru] has quit [Quit: Konversation terminated!] 10:45 -!- Zenton [~user@unaffiliated/vicenteh] has quit [Ping timeout: 240 seconds] 10:48 -!- tromp [~tromp@ip-217-103-3-94.ip.prioritytelecom.net] has quit [Remote host closed the connection] 10:48 -!- tromp [~tromp@ip-217-103-3-94.ip.prioritytelecom.net] has joined #bitcoin-wizards 10:51 -!- _tin [~tyn@104-56-112-203.lightspeed.sntcca.sbcglobal.net] has joined #bitcoin-wizards 10:55 -!- phwalkr [~phwalkr@194.210.89.118] has quit [Remote host closed the connection] 10:56 -!- phwalkr [~phwalkr@fwalunos-vip.estig.ipb.pt] has joined #bitcoin-wizards 10:56 -!- Guest78471 [~schmidty@104-7-216-111.lightspeed.austtx.sbcglobal.net] has quit [Ping timeout: 240 seconds] 10:59 -!- tromp [~tromp@ip-217-103-3-94.ip.prioritytelecom.net] has quit [Remote host closed the connection] 10:59 -!- tromp [~tromp@ip-217-103-3-94.ip.prioritytelecom.net] has joined #bitcoin-wizards 11:07 -!- schmidty [~schmidty@104-7-216-111.lightspeed.austtx.sbcglobal.net] has joined #bitcoin-wizards 11:07 -!- schmidty is now known as Guest93963 11:13 -!- tromp [~tromp@ip-217-103-3-94.ip.prioritytelecom.net] has quit [Remote host closed the connection] 11:13 -!- enemabandit [~enemaband@16.77.54.77.rev.vodafone.pt] has joined #bitcoin-wizards 11:14 -!- tromp [~tromp@ip-217-103-3-94.ip.prioritytelecom.net] has joined #bitcoin-wizards 11:18 -!- phwalkr [~phwalkr@fwalunos-vip.estig.ipb.pt] has quit [Quit: Leaving...] 11:19 -!- thrmo [~thrmo@gateway/tor-sasl/thrmo] has quit [Quit: Waiting for .007] 11:28 -!- Chris_Stewart_5 [~chris@unaffiliated/chris-stewart-5/x-3612383] has joined #bitcoin-wizards 11:31 -!- rmwb [~rmwb@199.178.233.220.static.exetel.com.au] has joined #bitcoin-wizards 11:49 -!- rmwb [~rmwb@199.178.233.220.static.exetel.com.au] has quit [Ping timeout: 252 seconds] 11:49 -!- tombusby [~tombusby@gateway/tor-sasl/tombusby] has quit [Ping timeout: 256 seconds] 11:53 -!- tombusby_ [~tombusby@gateway/tor-sasl/tombusby] has joined #bitcoin-wizards 12:07 -!- stefanwouldgo [2504fbbe@gateway/web/freenode/ip.37.4.251.190] has joined #bitcoin-wizards 12:09 < stefanwouldgo> I thought the way they synthesized EC libraries using COQ was really interesting: https://people.csail.mit.edu/jgross/personal-website/papers/2017-fiat-crypto-pldi-draft.pdf 12:13 -!- stefanwouldgo [2504fbbe@gateway/web/freenode/ip.37.4.251.190] has quit [Ping timeout: 256 seconds] 12:43 -!- thrmo [~thrmo@gateway/tor-sasl/thrmo] has joined #bitcoin-wizards 12:46 -!- Murch [~murch@50-200-105-218-static.hfc.comcastbusiness.net] has quit [Quit: Snoozing.] 12:53 -!- bitconner [~conner@c-73-170-56-77.hsd1.ca.comcast.net] has joined #bitcoin-wizards 12:58 -!- bitconner [~conner@c-73-170-56-77.hsd1.ca.comcast.net] has quit [Ping timeout: 244 seconds] 12:58 -!- Zenton [~user@unaffiliated/vicenteh] has joined #bitcoin-wizards 12:59 < roconnor> the synthesis itself isn't proven correct, but it is very good none the less. 13:00 < sipa> roconnor: are you sure? 13:09 < roconnor> That's the what I remember from talking with them at HACS. 13:10 < roconnor> the generated C code is simply Coq code pretty printed using Coq's notation mechinisim with no understanding as to what C is or means. 13:10 < roconnor> that said, they use a *very* limited subset of C. 13:11 < roconnor> But still, systematically generating C code from higher-level source code that is verified is very good. 13:17 < roconnor> it avoid tweetNACL style typographical errors. 13:26 -!- vtnerd [~Lee@173-23-103-30.client.mchsi.com] has quit [Read error: Connection reset by peer] 13:26 -!- vtnerd_ [~Lee@173-23-103-30.client.mchsi.com] has joined #bitcoin-wizards 13:28 < sipa> roconnor: oh, right, the actual conversion to C is not proven 13:29 < sipa> but the internal representation which is very close to C is 13:31 < roconnor> yes. 13:32 -!- bitconner [~conner@c-73-170-56-77.hsd1.ca.comcast.net] has joined #bitcoin-wizards 13:36 -!- Chris_Stewart_5 [~chris@unaffiliated/chris-stewart-5/x-3612383] has quit [Read error: Connection reset by peer] 13:41 -!- Murch [~murch@50-200-105-218-static.hfc.comcastbusiness.net] has joined #bitcoin-wizards 13:42 -!- thrmo_ [~thrmo@gateway/tor-sasl/thrmo] has joined #bitcoin-wizards 13:45 -!- Murch [~murch@50-200-105-218-static.hfc.comcastbusiness.net] has quit [Client Quit] 13:45 -!- thrmo [~thrmo@gateway/tor-sasl/thrmo] has quit [Ping timeout: 256 seconds] 13:45 < roconnor> at least it is very syntactically close to C. Whether it is semantically close to C is the more thorny issue. 13:47 -!- rmwb [~rmwb@199.178.233.220.static.exetel.com.au] has joined #bitcoin-wizards 13:52 -!- thrmo_ is now known as thrmo 13:55 -!- wildermind [uid300433@gateway/web/irccloud.com/x-dynacuzwtavcelxx] has quit [Quit: Connection closed for inactivity] 13:58 < gmaxwell> although the kind of code it writes its basically trivial circuits, no? not something with a lot of semantic surprises. 14:01 -!- Murch [~murch@50-200-105-218-static.hfc.comcastbusiness.net] has joined #bitcoin-wizards 14:04 < roconnor> I agree. I mean you could make mistakes by like generating the wrong size int variable types, or using signed instead of unsigned, but it is hard to imagine making a subtle error. Most kinds of errors would be catastrophic. 14:05 < roconnor> I suppose you could make errors like, trying to set bits in uninitialized variables that compile correctly in practice ... at the right optimization level. 14:05 < gmaxwell> but I think it's a great distinction, if it were formally verrified through you could say that if you compiled it with compcert the proofs would hold all the way though... and that wouldn't be the case here. 14:05 < sipa> those are all very detectable errors with sanitizers and valgrind etc 14:06 -!- rmwb [~rmwb@199.178.233.220.static.exetel.com.au] has quit [Ping timeout: 260 seconds] 14:07 < roconnor> gmaxwell: the good news is that extending the work to generate, for example VerifableC proofs, is a very resonable way to proceed given their existing work. 14:08 < roconnor> I'm particularly interested in generating Simplicity and proving the translator correct. 14:08 -!- vtnerd_ [~Lee@173-23-103-30.client.mchsi.com] has quit [Quit: ZNC 1.7.1 - https://znc.in] 14:09 -!- vtnerd [~Lee@173-23-103-30.client.mchsi.com] has joined #bitcoin-wizards 14:24 -!- bitconner [~conner@c-73-170-56-77.hsd1.ca.comcast.net] has quit [Ping timeout: 252 seconds] 14:25 -!- tromp [~tromp@ip-217-103-3-94.ip.prioritytelecom.net] has quit [Remote host closed the connection] 14:25 -!- tromp [~tromp@ip-217-103-3-94.ip.prioritytelecom.net] has joined #bitcoin-wizards 14:28 -!- Guyver2 [~Guyver@guyver2.xs4all.nl] has quit [Quit: Going offline, see ya! (www.adiirc.com)] 14:41 -!- p0nziph0ne [p0nziph0ne@gateway/vpn/privateinternetaccess/p0nziph0ne] has quit [Quit: Leaving] 14:41 -!- bitconner [~conner@136.24.75.121] has joined #bitcoin-wizards 14:48 -!- tromp [~tromp@ip-217-103-3-94.ip.prioritytelecom.net] has quit [Remote host closed the connection] 14:48 -!- tromp [~tromp@ip-217-103-3-94.ip.prioritytelecom.net] has joined #bitcoin-wizards 14:49 -!- PaulTroon [~Paul@h-5-150-248-150.NA.cust.bahnhof.se] has joined #bitcoin-wizards 14:51 -!- tromp [~tromp@ip-217-103-3-94.ip.prioritytelecom.net] has quit [Remote host closed the connection] 14:51 -!- tromp [~tromp@ip-217-103-3-94.ip.prioritytelecom.net] has joined #bitcoin-wizards 14:54 -!- son0p_ [~ff@190.240.56.104] has joined #bitcoin-wizards 14:59 -!- nuncanada2 [~dude@187.65.68.135] has joined #bitcoin-wizards 15:00 -!- nuncanada [~dude@187.65.68.135] has quit [Ping timeout: 252 seconds] 15:11 -!- Guest93963 [~schmidty@104-7-216-111.lightspeed.austtx.sbcglobal.net] has quit [Ping timeout: 240 seconds] 15:14 -!- elichai2 [uid212594@gateway/web/irccloud.com/x-mwggotwszylbocsc] has quit [Quit: Connection closed for inactivity] 15:37 -!- michaelsdunn1 [~michaelsd@unaffiliated/michaelsdunn1] has quit [Remote host closed the connection] 15:43 -!- vtnerd [~Lee@173-23-103-30.client.mchsi.com] has quit [Read error: Connection reset by peer] 15:44 -!- vtnerd [~Lee@173-23-103-30.client.mchsi.com] has joined #bitcoin-wizards 15:45 -!- tromp [~tromp@ip-217-103-3-94.ip.prioritytelecom.net] has quit [Remote host closed the connection] 15:45 -!- tromp [~tromp@ip-217-103-3-94.ip.prioritytelecom.net] has joined #bitcoin-wizards 15:52 -!- tromp [~tromp@ip-217-103-3-94.ip.prioritytelecom.net] has quit [Remote host closed the connection] 15:52 -!- tromp [~tromp@ip-217-103-3-94.ip.prioritytelecom.net] has joined #bitcoin-wizards 15:55 -!- enemabandit [~enemaband@16.77.54.77.rev.vodafone.pt] has quit [Ping timeout: 272 seconds] 16:01 -!- CheckDavid [uid14990@gateway/web/irccloud.com/x-lycqqxozwbpjxxip] has joined #bitcoin-wizards 16:04 -!- rmwb [~rmwb@199.178.233.220.static.exetel.com.au] has joined #bitcoin-wizards 16:12 -!- PaulTroon [~Paul@h-5-150-248-150.NA.cust.bahnhof.se] has quit [Ping timeout: 252 seconds] 16:22 -!- rockhouse [~rockhouse@unaffiliated/rockhouse] has quit [Quit: Ping timeout (120 seconds)] 16:22 -!- rockhouse [~rockhouse@unaffiliated/rockhouse] has joined #bitcoin-wizards 16:23 -!- rmwb [~rmwb@199.178.233.220.static.exetel.com.au] has quit [Ping timeout: 252 seconds] 16:41 -!- tromp [~tromp@ip-217-103-3-94.ip.prioritytelecom.net] has quit [Remote host closed the connection] 16:41 -!- tromp [~tromp@ip-217-103-3-94.ip.prioritytelecom.net] has joined #bitcoin-wizards 16:43 -!- son0p_ [~ff@190.240.56.104] has quit [Quit: leaving] 16:49 -!- deusexbeer [~deusexbee@079-170-138-066-dynamic-pool-adsl.wbt.ru] has joined #bitcoin-wizards 16:52 -!- DougieBot5000_ [~DougieBot@unaffiliated/dougiebot5000] has joined #bitcoin-wizards 16:53 -!- DougieBot5000 [~DougieBot@unaffiliated/dougiebot5000] has quit [Killed (verne.freenode.net (Nickname regained by services))] 16:53 -!- DougieBot5000_ is now known as DougieBot5000 16:57 -!- Murch [~murch@50-200-105-218-static.hfc.comcastbusiness.net] has quit [Quit: Snoozing.] 17:07 -!- Murch [~murch@50-200-105-218-static.hfc.comcastbusiness.net] has joined #bitcoin-wizards 17:11 -!- Krellan [~Krellan@2601:640:4000:9258:1c1:5844:3ef1:ae96] has quit [Ping timeout: 260 seconds] 17:12 -!- Krellan [~Krellan@2601:640:4000:9258:1c1:5844:3ef1:ae96] has joined #bitcoin-wizards 17:57 -!- rusty [~rusty@pdpc/supporter/bronze/rusty] has joined #bitcoin-wizards 18:13 -!- bildramer1 [~bildramer@p2003004D8D312900AC9BCCA14258DFA9.dip0.t-ipconnect.de] has quit [Ping timeout: 240 seconds] 18:21 -!- rmwb [~rmwb@199.178.233.220.static.exetel.com.au] has joined #bitcoin-wizards 18:25 -!- Emcy [~Emcy@unaffiliated/emcy] has quit [Read error: Connection reset by peer] 18:28 -!- Emcy [~Emcy@unaffiliated/emcy] has joined #bitcoin-wizards 18:28 -!- mn3monic [jsz@unaffiliated/mn3monic] has quit [Excess Flood] 18:29 -!- mn3monic [jsz@unaffiliated/mn3monic] has joined #bitcoin-wizards 18:32 -!- thrmo [~thrmo@gateway/tor-sasl/thrmo] has quit [Ping timeout: 256 seconds] 18:36 -!- rmwb [~rmwb@199.178.233.220.static.exetel.com.au] has quit [Ping timeout: 240 seconds] 18:51 -!- _tin [~tyn@104-56-112-203.lightspeed.sntcca.sbcglobal.net] has quit [Ping timeout: 244 seconds] 19:03 -!- nuncanada3 [~dude@187.65.68.135] has joined #bitcoin-wizards 19:06 -!- nuncanada2 [~dude@187.65.68.135] has quit [Ping timeout: 244 seconds] 19:26 -!- Murch [~murch@50-200-105-218-static.hfc.comcastbusiness.net] has quit [Quit: Snoozing.] 19:28 -!- Belkaar [~Belkaar@unaffiliated/belkaar] has quit [Ping timeout: 260 seconds] 19:28 -!- Belkaar [~Belkaar@xdsl-78-35-73-147.netcologne.de] has joined #bitcoin-wizards 19:28 -!- Belkaar [~Belkaar@xdsl-78-35-73-147.netcologne.de] has quit [Changing host] 19:28 -!- Belkaar [~Belkaar@unaffiliated/belkaar] has joined #bitcoin-wizards 19:51 -!- CheckDavid [uid14990@gateway/web/irccloud.com/x-lycqqxozwbpjxxip] has quit [Quit: Connection closed for inactivity] 19:52 -!- Newyorkadam [~Newyorkad@wikipedia/Newyorkadam] has joined #bitcoin-wizards 19:53 -!- dougsland [~douglas@c-73-234-93-65.hsd1.nh.comcast.net] has joined #bitcoin-wizards 19:56 -!- nuncanada3 [~dude@187.65.68.135] has quit [Quit: Leaving] 20:18 -!- dougsland [~douglas@c-73-234-93-65.hsd1.nh.comcast.net] has quit [Ping timeout: 260 seconds] 20:34 -!- rmwb [~rmwb@199.178.233.220.static.exetel.com.au] has joined #bitcoin-wizards 20:47 -!- rmwb [~rmwb@199.178.233.220.static.exetel.com.au] has quit [Ping timeout: 245 seconds] 20:58 -!- jb55 [~jb55@S010660e327dca171.vc.shawcable.net] has joined #bitcoin-wizards 21:29 -!- Logicwax [~Logicwax@c-76-126-174-152.hsd1.ca.comcast.net] has quit [Ping timeout: 246 seconds] 21:33 -!- molz [~molly@unaffiliated/molly] has joined #bitcoin-wizards 21:34 -!- mol [~molly@unaffiliated/molly] has quit [Ping timeout: 272 seconds] 22:46 -!- rmwb [~rmwb@199.178.233.220.static.exetel.com.au] has joined #bitcoin-wizards 22:59 -!- rmwb [~rmwb@199.178.233.220.static.exetel.com.au] has quit [Ping timeout: 240 seconds] 23:18 -!- Newyorkadam [~Newyorkad@wikipedia/Newyorkadam] has quit [Quit: Newyorkadam] 23:20 -!- go1111111 [go1111111@gateway/vpn/privateinternetaccess/go1111111] has quit [Ping timeout: 246 seconds] 23:33 -!- emzy [~quassel@unaffiliated/emzy] has quit [Ping timeout: 252 seconds] 23:36 -!- go1111111 [~go1111111@104.156.98.86] has joined #bitcoin-wizards 23:36 -!- emzy [~quassel@raspberry.emzy.de] has joined #bitcoin-wizards 23:56 -!- Newyorkadam [~Newyorkad@wikipedia/Newyorkadam] has joined #bitcoin-wizards --- Log closed Thu Sep 27 00:00:20 2018