sipa changed the topic of #bitcoin-wizards to: This channel is for discussing theoretical ideas with regard to cryptocurrencies, not about short-term Bitcoin development | http://bitcoin.ninja/ | This channel is logged. | For logs and more information, visit http://bitcoin.ninja
Murch has quit [Quit: Snoozing.]
thrmo has quit [Quit: Waiting for .007]
rmwb has joined #bitcoin-wizards
gnusha has joined #bitcoin-wizards
rmwb has quit [Remote host closed the connection]
rmwb has joined #bitcoin-wizards
TheoStorm has quit [Ping timeout: 244 seconds]
mn3monic has quit [Excess Flood]
mn3monic has joined #bitcoin-wizards
Zenton has quit [Ping timeout: 240 seconds]
Zenton has joined #bitcoin-wizards
TheoStorm has joined #bitcoin-wizards
Belkaar has quit [Ping timeout: 240 seconds]
Belkaar has joined #bitcoin-wizards
Belkaar has joined #bitcoin-wizards
Belkaar has quit [Changing host]
TheoStorm has quit [Ping timeout: 260 seconds]
TheoStorm has joined #bitcoin-wizards
TheoStorm has quit [Ping timeout: 240 seconds]
rmwb has quit [Remote host closed the connection]
Zenton has quit [Read error: Connection reset by peer]
Zenton has joined #bitcoin-wizards
CheckDavid has quit [Quit: Connection closed for inactivity]
Chris_Stewart_5 has quit [Ping timeout: 272 seconds]
TheoStorm has joined #bitcoin-wizards
RubenSomsen has joined #bitcoin-wizards
TheoStorm has quit [Ping timeout: 252 seconds]
_tin has quit [Ping timeout: 240 seconds]
Emcy has quit [Ping timeout: 245 seconds]
Zenton has quit [Ping timeout: 245 seconds]
Zenton has joined #bitcoin-wizards
gnusha has quit [Quit: leaving]
gnusha has joined #bitcoin-wizards
gnusha has left #bitcoin-wizards [#bitcoin-wizards]
bsm117532 has quit [Ping timeout: 240 seconds]
gnusha has joined #bitcoin-wizards
TheoStorm has joined #bitcoin-wizards
rmwb has joined #bitcoin-wizards
TheoStorm has quit [Ping timeout: 240 seconds]
rmwb has quit [Ping timeout: 245 seconds]
rmwb has joined #bitcoin-wizards
TheoStorm has joined #bitcoin-wizards
TheoStorm has quit [Ping timeout: 252 seconds]
<kanzure>
someone is asking me for "a guide on writing coq proofs for bitcoin code"; i assume he means an example of theorem proving for large projects other than bitcoin.
rh0nj has quit [Remote host closed the connection]
rh0nj has joined #bitcoin-wizards
TheoStorm has joined #bitcoin-wizards
<aj>
kanzure: https://sel4.systems/ is the best practical example i know of, but it's isabelle not coq. there's http://compcert.inria.fr/ on the coq side, but not sure how practical it is.
<kanzure>
oh yes. thank you.
<aj>
kanzure: coq proofs for smart contract usage seems interesting and practical to me; i keep waiting to see what roconnor comes up with for simplicity for that though
<aj>
kanzure: think he's presenting in .. novemberish? on that with some actual code, touch wood
<kanzure>
the inbound request was a reply to my sort of off-the-cuff tweet about "y'all know that theorem proving all of bitcoin/libconsensus is huge cost right?" https://twitter.com/kanzure/status/1044785300214620161
<kanzure>
i don't know what the costs really would be, but roconnor likes to say "at least 10x" and i like to say the minimum is something like the cost of hiring an army of developers to resolve all pull request merge conflicts for the entire open queue for the respective authors (e.g. especially for libconsensus code movement stuff) plus the army for review on top of that.
<kanzure>
huh this document says "$1k/LOC" ?
<sipa>
huh as in "so low" or "so high" ?
<kanzure>
huh as in fascinating :)
<kanzure>
doc also says sel4 is 10k LOC, and has 480k LOC of isabelle proofs
<aj>
that figure's what they expect a priori for EAL6 assurance "semiformally verified design and tested" https://en.wikipedia.org/wiki/Evaluation_Assurance_Level rather than what it cost to do the formal verification i think?
spinza has quit [Quit: Coyote finally caught up with me...]
<gmaxwell>
sel4 is also the only non-trivial formally verified program I'm aware of that also proves really useful properties about its dynamic behavior.
spinza has joined #bitcoin-wizards
gribble has quit [Remote host closed the connection]
tombusby has quit [Remote host closed the connection]
tombusby has joined #bitcoin-wizards
_tin has joined #bitcoin-wizards
TheoStorm has quit [Ping timeout: 252 seconds]
warren_ is now known as warren
gribble has joined #bitcoin-wizards
TheoStorm has joined #bitcoin-wizards
bitconner has quit [Ping timeout: 245 seconds]
_tin has quit [Ping timeout: 260 seconds]
tromp has quit [Remote host closed the connection]
tromp has joined #bitcoin-wizards
TheoStorm has quit [Ping timeout: 252 seconds]
Krellan has joined #bitcoin-wizards
shesek has quit [Ping timeout: 246 seconds]
TheoStorm has joined #bitcoin-wizards
Zenton has quit [Ping timeout: 240 seconds]
<maaku>
kanzure: roconnor's work proving the correctness of the sha2 jet in simplicity is probably relevant
bitconner has joined #bitcoin-wizards
TheoStorm has quit [Ping timeout: 252 seconds]
SopaXorzTaker has joined #bitcoin-wizards
deusexbeer has quit [Ping timeout: 252 seconds]
deusexbeer has joined #bitcoin-wizards
TheoStorm has joined #bitcoin-wizards
phwalkr has joined #bitcoin-wizards
setpill has joined #bitcoin-wizards
phwalkr has quit [Ping timeout: 252 seconds]
phwalkr has joined #bitcoin-wizards
TheoStorm has quit [Ping timeout: 260 seconds]
TheoStorm has joined #bitcoin-wizards
TheoStorm has quit [Ping timeout: 240 seconds]
Zenton has joined #bitcoin-wizards
TheoStorm has joined #bitcoin-wizards
SopaXorzTaker has quit [Remote host closed the connection]
TheoStorm has quit [Ping timeout: 252 seconds]
phwalkr has quit [Ping timeout: 240 seconds]
AaronvanW has joined #bitcoin-wizards
TheoStorm has joined #bitcoin-wizards
TheoStorm has quit [Quit: Leaving]
TheoStorm has joined #bitcoin-wizards
phwalkr has joined #bitcoin-wizards
tombusby has quit [Remote host closed the connection]
tombusby has joined #bitcoin-wizards
belcher has joined #bitcoin-wizards
intcat has quit [Ping timeout: 256 seconds]
intcat has joined #bitcoin-wizards
thrmo has joined #bitcoin-wizards
Krellan has quit [Ping timeout: 252 seconds]
Krellan has joined #bitcoin-wizards
Zenton has quit [Read error: Connection reset by peer]
Zenton has joined #bitcoin-wizards
reallll has joined #bitcoin-wizards
reallll has quit [Remote host closed the connection]
belcher has quit [Ping timeout: 245 seconds]
belcher has joined #bitcoin-wizards
Chris_Stewart_5 has joined #bitcoin-wizards
phwalkr has quit [Remote host closed the connection]
phwalkr has joined #bitcoin-wizards
phwalkr has quit [Ping timeout: 250 seconds]
bildramer1 has joined #bitcoin-wizards
bildramer has quit [Ping timeout: 252 seconds]
Krellan has quit [Ping timeout: 240 seconds]
Guyver2 has joined #bitcoin-wizards
Krellan has joined #bitcoin-wizards
Guyver2_ has joined #bitcoin-wizards
Guyver2_ has quit [Client Quit]
Emcy has joined #bitcoin-wizards
Emcy has quit [Read error: Connection reset by peer]
Emcy has joined #bitcoin-wizards
Chris_Stewart_5 has quit [Ping timeout: 244 seconds]
rh0nj has quit [Remote host closed the connection]
rh0nj has joined #bitcoin-wizards
gertjaap has joined #bitcoin-wizards
Chris_Stewart_5 has joined #bitcoin-wizards
rmwb has joined #bitcoin-wizards
rmwb has quit [Ping timeout: 250 seconds]
michaelsdunn1 has joined #bitcoin-wizards
SopaXorzTaker has joined #bitcoin-wizards
phwalkr has quit [Ping timeout: 264 seconds]
tromp has quit [Remote host closed the connection]
tromp has joined #bitcoin-wizards
SopaXorzTaker has quit [Quit: Leaving]
phwalkr has joined #bitcoin-wizards
rmwb has joined #bitcoin-wizards
rmwb has quit [Ping timeout: 240 seconds]
Krellan has quit [Read error: Connection reset by peer]
Krellan has joined #bitcoin-wizards
dnaleor has quit [Quit: Leaving]
p0nziph0ne has quit [Ping timeout: 246 seconds]
TheoStorm has joined #bitcoin-wizards
Krellan has quit [Ping timeout: 250 seconds]
<roconnor>
Over the summer I also did some evaluation of VerifiableC and verfied the correctness of libsecp256k1's 32-bit field multiplication implementation.
<roconnor>
gmaxwell: compcert is probably also non-trivial, but I haven't looked at it carefully.
p0nziph0ne has joined #bitcoin-wizards
tromp has quit [Remote host closed the connection]
tromp has joined #bitcoin-wizards
phwalkr has quit [Ping timeout: 264 seconds]
phwalkr has joined #bitcoin-wizards
Krellan has joined #bitcoin-wizards
<roconnor>
Of course even trivial things could be useful to verify, like which pointer arguments are allowed to alias and which ones aren't.
Krellan has quit [Ping timeout: 250 seconds]
Krellan has joined #bitcoin-wizards
dougsland has joined #bitcoin-wizards
m8tion has joined #bitcoin-wizards
Krellan has quit [Ping timeout: 260 seconds]
Krellan has joined #bitcoin-wizards
m8tion has quit [Client Quit]
m8tion has joined #bitcoin-wizards
Krellan has quit [Ping timeout: 250 seconds]
Krellan has joined #bitcoin-wizards
m8tion has quit [Quit: Leaving]
m8tion has joined #bitcoin-wizards
rmwb has joined #bitcoin-wizards
m8tion has quit [Remote host closed the connection]
Murch has joined #bitcoin-wizards
phwalkr has quit [Remote host closed the connection]
p0nziph0ne has quit [Quit: Leaving]
m8tion has joined #bitcoin-wizards
m8tion has quit [Client Quit]
m8tion has joined #bitcoin-wizards
m8tion has quit [Remote host closed the connection]
Zenton has quit [Ping timeout: 240 seconds]
Chris_Stewart_5 has quit [Quit: WeeChat 1.4]
_tin has joined #bitcoin-wizards
rmwb has quit [Ping timeout: 260 seconds]
morcos has quit [Remote host closed the connection]
morcos has joined #bitcoin-wizards
p0nziph0ne has joined #bitcoin-wizards
phwalkr has joined #bitcoin-wizards
enemabandit has quit [Ping timeout: 240 seconds]
nehan_ has joined #bitcoin-wizards
nehan_ has quit [Client Quit]
phwalkr has quit [Ping timeout: 244 seconds]
belcher has quit [Quit: Leaving]
phwalkr has joined #bitcoin-wizards
phwalkr has quit [Read error: Connection reset by peer]
phwalkr has joined #bitcoin-wizards
_tin has quit [Ping timeout: 250 seconds]
dougsland has quit [Ping timeout: 244 seconds]
Krellan has quit [Ping timeout: 264 seconds]
Krellan has joined #bitcoin-wizards
enemabandit has joined #bitcoin-wizards
enemabandit has quit [Client Quit]
Krellan has quit [Ping timeout: 240 seconds]
shesek has joined #bitcoin-wizards
shesek has joined #bitcoin-wizards
shesek has quit [Changing host]
Krellan has joined #bitcoin-wizards
<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.
<gmaxwell>
yes, there are a lot of things where less than cosmic properties are proven.
phwalkr has quit [Ping timeout: 245 seconds]
Krellan has quit [Ping timeout: 250 seconds]
phwalkr has joined #bitcoin-wizards
Krellan has joined #bitcoin-wizards
Zenton has joined #bitcoin-wizards
deusexbeer has quit [Quit: Konversation terminated!]
Zenton has quit [Ping timeout: 240 seconds]
tromp has quit [Remote host closed the connection]
tromp has joined #bitcoin-wizards
_tin has joined #bitcoin-wizards
phwalkr has quit [Remote host closed the connection]
phwalkr has joined #bitcoin-wizards
Guest78471 has quit [Ping timeout: 240 seconds]
tromp has quit [Remote host closed the connection]
tromp has joined #bitcoin-wizards
schmidty has joined #bitcoin-wizards
schmidty is now known as Guest93963
tromp has quit [Remote host closed the connection]
stefanwouldgo has quit [Ping timeout: 256 seconds]
thrmo has joined #bitcoin-wizards
Murch has quit [Quit: Snoozing.]
bitconner has joined #bitcoin-wizards
bitconner has quit [Ping timeout: 244 seconds]
Zenton has joined #bitcoin-wizards
<roconnor>
the synthesis itself isn't proven correct, but it is very good none the less.
<sipa>
roconnor: are you sure?
<roconnor>
That's the what I remember from talking with them at HACS.
<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.
<roconnor>
that said, they use a *very* limited subset of C.
<roconnor>
But still, systematically generating C code from higher-level source code that is verified is very good.
<roconnor>
it avoid tweetNACL style typographical errors.
vtnerd has quit [Read error: Connection reset by peer]
vtnerd_ has joined #bitcoin-wizards
<sipa>
roconnor: oh, right, the actual conversion to C is not proven
<sipa>
but the internal representation which is very close to C is
<roconnor>
yes.
bitconner has joined #bitcoin-wizards
Chris_Stewart_5 has quit [Read error: Connection reset by peer]
Murch has joined #bitcoin-wizards
thrmo_ has joined #bitcoin-wizards
Murch has quit [Client Quit]
thrmo has quit [Ping timeout: 256 seconds]
<roconnor>
at least it is very syntactically close to C. Whether it is semantically close to C is the more thorny issue.
rmwb has joined #bitcoin-wizards
thrmo_ is now known as thrmo
wildermind has quit [Quit: Connection closed for inactivity]
<gmaxwell>
although the kind of code it writes its basically trivial circuits, no? not something with a lot of semantic surprises.
Murch has joined #bitcoin-wizards
<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.
<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.
<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.
<sipa>
those are all very detectable errors with sanitizers and valgrind etc
rmwb has quit [Ping timeout: 260 seconds]
<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.
<roconnor>
I'm particularly interested in generating Simplicity and proving the translator correct.