< GitHub157>
bitcoin/0.12 fe98533 Jonas Schnelli: [Qt] Disable some menu items during splashscreen/verification state...
< GitHub27>
[bitcoin] laanwj closed pull request #8302: 0.12.2: [Qt] Disable some menu items during splashscreen/verification state (0.12...Mf1607-012qtDebugSplash) https://github.com/bitcoin/bitcoin/pull/8302
< GitHub157>
bitcoin/0.12 1233cb4 Wladimir J. van der Laan: Merge #8302: 0.12.2: [Qt] Disable some menu items during splashscreen/verification state...
< MarcoFalke>
Of course windows test are timing out, ow
< MarcoFalke>
I am not sure why they don't work in parallel "out of the box"
< MarcoFalke>
Maybe wine can't handle it?
< sipa>
reduce their parallelism?
< MarcoFalke>
There is already an overhead of about 2 for just using wine. Then, disabling parallel is another slowdown by 4.
< MarcoFalke>
So about 8 times longer rpc test for windows
< sipa>
fun.
< luke-jr>
what? why would WINE have any overhead?
<@wumpus>
luke-jr: that's not really clear, I'd expect an overhead at startup/shutdown due to setting up the 'virtual windows environment', but not on networking
< GitHub175>
[bitcoin] jtimon opened pull request #8328: Consensus: Rename: Move consensus code to the consensus directory (master...0.12.99-consensus-rename) https://github.com/bitcoin/bitcoin/pull/8328
< jtimon>
ping kanzure ^^
< jtimon>
quite trivial to review, just touches the makefile and a bunch of includes
< jtimon>
and the same question kind of applies to the other 2 consensus checks in there
< jtimon>
in other words would it be crazy to move all those checks to just connectblock? why?
< jtimon>
or in other words, is it necessary or advantageous to call ContextualCheckBlock() in other places other than ConnectBlock() in some way I'm missing?
< jtimon>
answers from anyone welcomed
< sipa>
jtimon: contextualcheckblock runs before storing a block on disk, connectblock after
< sipa>
so everything that can be in contextualcheckblock should be, as it make attacks that cause disk space wasting harder
< jtimon>
I see, so the advantage is to discard offending blocks before storing them on disk for checks that are relatively cheap
< jtimon>
I didn't knew we stored invalid blocks at all
< jtimon>
why do we store invalid blocks?
< sipa>
because we can't know until we reorg the chainstate
< sipa>
we may accept a block on a side branch that does not overtake the best chai yet
< sipa>
*chain
< jtimon>
but it's still valid, no?
< sipa>
we can't know that without reorg
< sipa>
because we need the utxo set for its parent
< jtimon>
we can know whether a block is valid in its chain without knowing whether it belongs to the "longest" chain or not, right?
< sipa>
in theory, yes
< sipa>
in practice, no
< sipa>
because we don't have its utxoset we can't validate
< jtimon>
oh, I see, we never build incompatible utxo histories
< sipa>
right, we just have a single utxo set for the tip
< sipa>
and delay full validation until we're forced to switch tips
< jtimon>
I thought that was part of the CCoinsViewCache purpose...
< jtimon>
but I guess yeah, it doesn't make sense to fully validate until you're forced to reorg by the accumulated pow, storing that block is cheaper I guess
< sipa>
no, that's just so we don't have to write everything to disk immediately
< sipa>
now, pow is the most expensive thing for an attacker
< sipa>
so everything that comes after pow validation and corruption checks does not matter very much
< sipa>
why are you asking, btw?
< sipa>
ah, i know
< sipa>
iswitnessenabled depends on versionbits
< jtimon>
mhmm, why do we validate any part of a block that we don't see as belonging to the longest chain at all?
< sipa>
because we at least need to know whether it is actually the right block
< sipa>
a peer could change one transaction before relay
< jtimon>
sipa: it was part of my latest consensus refactor branch to get rid of ContextualCheckBlock()
< sipa>
and in that case we must punish the peer, but not mark the block as invalid
< sipa>
so an invariant is that all blocks on disk are known to actually match the blocks whose headers we know
< jtimon>
if we know it's not making a longer chain, why bother validating BIP113 ?
< sipa>
validating bip113 is not necessary i think
< sipa>
but the segwit commitment check is
< sipa>
before storing on disk
< jtimon>
that's useful, what about the bip34 check in ContextualCheckBlock(), can it be moved out?
< sipa>
i believe so
< jtimon>
ok, thanks
< jtimon>
but not the new segwit one, fine
< jtimon>
well, I would prefer to pass the consensus validation flags instead of calling IsWitnessEnabled() from there
< jtimon>
but I should try to write that first before discussing it further
< sdaftuar>
reviewers, please review some open PRs for 0.13.0: #8295, #8305, #8312
< BTCking>
AMAZING! My bitcoin-grower is now ready. Send me some bitcoin (1btc, 2btc, etc.) and get MUCH more back INSTANTLY. This uses Block-chain explanding technology! Proven safe & secure. You cannot lose. PM me to begin!!
< sipa>
BTCking: fuck off
< * BTCking>
slaps sipa around a bit with a large trout
< BTCking>
AMAZING! My bitcoin-grower is now ready. Send me some bitcoin (1btc, 2btc, etc.) and get MUCH more back INSTANTLY. This uses Block-chain explanding technology! Proven safe & secure. You cannot lose. PM me to begin!!
< GitHub65>
[bitcoin] jtimon opened pull request #8329: Consensus: MOVEONLY: Move functions for tx verification (master...0.12.99-consensus-moveonly-tx) https://github.com/bitcoin/bitcoin/pull/8329
< jtimon>
kanzure: ping again, still quite simple to review and re-write
< gmaxwell>
sdaftuar: maybe it doesn't matter because its a corner case, but #8305 makes it look like it will effectively discard the dangling header-- it pushmessages a getheaders and returns, without AcceptBlockHeader or UpdateBlockAvailability.
< sdaftuar>
oh, UpdateBlocKAvailability, hmm
< gmaxwell>
Is the expectation that it'll come back in via the getheaders, and that the remote end won't do anything smart like not send it because it already did? (I guess thats reasonable?) though the lack of updateavailablity probably means we'll send a redundant announcement in that direction.
< sdaftuar>
well there's no way to avoid getting the headers message back to you
< sdaftuar>
if you set hashstop equal to the hash of that header, it'll still appear in the response
< sdaftuar>
i don't think the remote end is allowed to not re-send, though i suppose lack of a spec makes this a difficult statement to concretely make
< sdaftuar>
but we expect the contents of a headers message to be a linear connecting chain
< gmaxwell>
K. That makes sense, I thought that was the assumption but wanted to be sure (I think it's correct.)
< sdaftuar>
i guess there could be an advantage to setting hashLastUnknownBlock if a header doesn't connect... that would mean that if a different peer supplied the missing headers, we could download the block from the peer who made the announcement
< sdaftuar>
but that would only matter if the peer didn't respond to the getheaders being pushed in this patch
< gmaxwell>
so now let me ask, if I send you a header that doesn't connect because of timestamp stupidity. And I'm your only peer. If there are two blocks in a row during the time when the prior header will be rejected... When will it start connecting again? I'll get the flag false on me, then it'll never be sent to true, since all further headers I send will also not connect.
< sdaftuar>
which is a weird corner case
< gmaxwell>
On the update front, I was mostly think in terms of not sending surpflous compact block messages.
< sdaftuar>
when you respond to the getheaders, the bit is cleared
< midnightmagic>
;;isitdown github.com
< gribble>
github.com is up
< sdaftuar>
and the headers will start connecting again
< sdaftuar>
well,
< sdaftuar>
unless the time stamp is still broken
< gmaxwell>
hm. I was thinking that it wouldn't be set to true if the getheaders reply also didn't connect due to bad timestamps.
< xinxi>
Hi guys
< xinxi>
Anybody here?
< sdaftuar>
gmaxwell: yeah, i can't solve the problem of a bunch of blocks in a row all being invalid to one peer but not another
< sdaftuar>
but typically, the first block is too far ahead
< sdaftuar>
and then by the time the next block comes in, you would be able to accept both
< sdaftuar>
if you'd be willing to try
< sdaftuar>
but we have no "try" mechanism currently
< sdaftuar>
i guess the question is, what should we do if a peer is relaying many blocks in a row that are all actually too far in the future?
< sdaftuar>
i just fall back to the current behavior of failing/disconnecting
< sdaftuar>
i did briefly think about whether it would be feasible to somehow accept headers that are too far in the future, but i'm pretty sure that's a major rewrite to our consensus logic
< sdaftuar>
(accept them, so that you could re-try them later)
< sdaftuar>
gmaxwell: perhaps we could always send a getheaders if the peer is whitelisted?
< gmaxwell>
I don't think that would be an awful thing, but I don't think it addresses the concern-- you shouldn't only fail to fail if you have whitelisted peers.
< sdaftuar>
i guess i could do the thing you imply -- actually just check to see if the headers connect, and use that to re-set the bit
< gmaxwell>
maybe I'm misunderstanding, but that situation I'm thinking about is if you're slow on time by a few seconds, rejected a block, then the next comes in, and it still doesn't connect... you're going to stop sending getheaders after that. Then no others will connect from that peer. The time is a bit freaky, since it's a temporary failure.
< sdaftuar>
yes, i agree your example is a correct one
< sdaftuar>
i'm just trying to distinguish that from an example where an attacker sends you a chain that's far into the future
< gmaxwell>
I think we award a little bit of misbehaving there. Ironically, for sync purposes it might be better to immediately disconnect: at least that will clear the flag! :)
< gmaxwell>
relying on DOS disconnect to make progress is weird though, but I think thats the answer here: after some number non-connecting blocks I think you'll disconnect the peer. When you reconnect, the flag will be true and you'll try to sync again.
< gmaxwell>
sdaftuar: to prevent looping, why not store the most recent ID. And don't getheader again if it's the same?
< gmaxwell>
e.g. block announce, doesn't connect, store the most recent ID and getheader. Get headers, still doesn't connect and most recent ID is the same. Stop.
< sdaftuar>
sorry, what is most recent ID?
< gmaxwell>
when the headers response comes in take the ID (hash) of the latest block in the reply. And do not keep requesting headers when that value hasn't changed for this peer.
< gmaxwell>
I announce X, X doesn't connect. Remember X, request headers. Headers come in, they tell you a bunch of junk ending at X. Still doesn't connect. Stop.
< sdaftuar>
gmaxwell: i guess i just worry about assuming too much about the broken implementations out there
< sdaftuar>
eg maybe the peer who was sending me 160kb of junk was sending me random junk
< gmaxwell>
Well thats what misbehaving is for.
< sdaftuar>
but in your example, wouldn't that behavior result in infinite loop?
< gmaxwell>
The headers reply would end with the block X, which we already had remembered, so we would stop there.
< gmaxwell>
no loop. then they later announce block y, and we'd getheaders again. and hopefully connect.
< gmaxwell>
So basically one headers retry per novel header they send.
< sdaftuar>
i'm specifically referring to peers that are totally broken and on initial getheaders sync, they send us 2000 headers that don't connect
< sdaftuar>
i don't want to assume too much about how that peer is doing that
< gmaxwell>
sure, whatever, testnet node on mainnet or whatnot.
< sdaftuar>
if getting it wrong means 160kb over and over again...
< gmaxwell>
just don't assume it's malicious, since there are better ways to waste our bandwidth for malicious peers.
< sdaftuar>
well you're suggesting we assume it's deterministic i think. which is hopefully true, but if it's not, then sadness
< gmaxwell>
yes, indeed, and actually the 2000 limit gets in the way too.
< sdaftuar>
i mean, i think in practice your suggestion probably works, i was just hoping for something more robust to accidental disaster
< gmaxwell>
speaking of 2000, I'm not seeing how what you suggest doesn't actually break sync.
< sipa>
can i get a summary of the problem?
< gmaxwell>
oh nevermind last comment, I was mistaking the order.
< sdaftuar>
sipa: i noticed on testnet that i had a node that would fall out of sync, because its one peer would occasionally send a block header (using headers announcements) that was too far in the future
< gmaxwell>
(I was thinking that we'd request headers, if there was more than 2000 missing, that they sent the later headers first)
< sdaftuar>
so the peer thought the header was valid, but the local node would reject
< sdaftuar>
this is a case i had never thought of when working on the headers announcements stuff
< sdaftuar>
since the announcing peer doesn't realize the recipient rejects the header, they continue to announce blocks on top of the header
< sipa>
sdaftuar: yes, i get that
< sipa>
but you have a patch for that
< sdaftuar>
resulting in headers announcements that don't connect for the recipient, and then eventually disconnect
< xinxi>
hey guys, I want to make Bitcoin provably correct.
< sdaftuar>
oh right. so gmaxwell wonders if we can avoid failure in the case where two blocks come in quickly, where the first block is still invalid when the second one is announced
< sdaftuar>
my patch doesn't address that
< xinxi>
I am serious.
< sipa>
xinxi: you'll need to be a bit more specific
< sipa>
what part do you want to prove?
< gmaxwell>
sipa: and sdaftuar is concerned that relaxations will leave it in a state where its constantly requesting headers over and over again.
< xinxi>
sipa: thank you for your attention. Yeah, basically, I think bugs are still in the C++ implementation. And I want to make sure it's absolutely correct.
< xinxi>
so there will be no bugs.
< sipa>
xinxi: that implies you have a specification for correct to compare to
< gmaxwell>
I think this could be addressed by just adding a small amount of DOS each time.
< gmaxwell>
Correct with respect to a specification may well be meaningless if the specification is not "correct" in a broader sense.
< xinxi>
sipa: yeah, I want to work out a formal specification as well.
< sipa>
xinxi: for the consensus logic, the code implementation is the specification, so it is by definition correct
< xinxi>
something like mathematical theorems about the code.
< sipa>
xinxi: however, being able to verify that the behaviour of that code does not change between releases would be incredibly valuable
< sipa>
unfortunately, due to historical reasons mostly, the consensus code is not well separated from the rest
< gmaxwell>
sdaftuar: e.g. I think we could just trigger a getheaders on any header message with only a single header in it that doesn't connect, and add a small dos penalty.
< xinxi>
sipa: I understand what you mean. The code, as a specification, may not be consistent with itself.
< gmaxwell>
sdaftuar: then every new block that shows up on the network will cause us to retry to connect.
< morcos>
i know this sounds kind of janky, but it seems to me that a lot of this sync logic is stuff that to a human is kind of obviously stupid. i wonder if putting in a bit of belt and suspender check on things getting stuck might make sense.
< sipa>
xinxi: indeed. not consistent with itself, or not consistent with other implementations/versions
< gmaxwell>
sdaftuar: and eventually it will either connect, or disconnect the peer.
< xinxi>
sipa: also, you may not want to treat bugs as part of the specification like the heartbleed bug in OpenSSL should not be part of OpenSSL.
< sipa>
xinxi: we have to
< btcdrak>
xinxi: there is a slow and arduous process of extracting the consensus code into a separate library which will make things a lot easier in the long run.
< morcos>
for instance very 60 secs you clear out some state such as fLastHeadersConnected and perhaps nSyncStarted (maybe only if we're not actively receiving headers)
< morcos>
i'm sure we can imagine other things that kind of get stuck
< gmaxwell>
morcos: you mean like a periodic, pick a random peer and restart our efforts to sync with it? and loudly logging that the sync state machine has failed if that accomplishes anything?
< sipa>
xinxi: even if we would write down a specification for the behaviour, and every one would agree that that spec is indeed the behaviour we want
< sipa>
xinxi: what if we then find a bug, and the code does something slightly different?
< sdaftuar>
gmaxwell: i think that sounds pretty good, though the DoS score should decay back down once headers that do connect are received, right? otherwise, over a long enough period of time, you eventually disconnect your peer
< morcos>
gmaxwell: yes something along those lines, i like the idea of loudly announcing it so we try to make stuff work in general, but that next time we miss something, hopefully it kind of autorecovers (like power cycling)
< btcdrak>
xinxi: the problem is it's quite disruptive to the codebase and causes everyone's pull-requests to need rebasing so it tends to get done slowly and in bursts. yes it's called libconsensus
< gmaxwell>
sdaftuar: yea, :( the whole dos score thing is kinda lame.
< xinxi>
btcdrak: but still, that probably reduces bugs in the consensus part, but still it does not guarantee the correctness.
< sipa>
xinxi: the code would have a bug, arguably. but we can't tell everyone to change their code, so it will need to be the document that had to be changed
< gmaxwell>
morcos: I agree with that in principle. We don't however, want to end up with a web of redundant mechenisms, potentially interacting.
< sipa>
xinxi: so we've usually said that a specification for bitcoin would be descriptive but not prescriptive... the laws of the network are those implemented by the code that people choose to run, not by an abstract descriptio
< morcos>
a bigger web you mean?
< gmaxwell>
morcos: hah
< sdaftuar>
unfortunately some of the bugs we've encountered (eg that hasHeaders thing that got reverted) wouldn't be fixed on restart either
< sipa>
for 0.14 i think we need to refactor the sync code
< * sdaftuar>
ducks
< sipa>
many parallel mechanisms and duplicated code
< gmaxwell>
sdaftuar: you could instead have a simple counter, set to zero whenever you connect, incremented on every non-connecting header response. And dos score only when it hits a threshold to avoid that effect.
< sipa>
no blame anywhere, but we've accumulated too much technical debt
< sdaftuar>
gmaxwell: yep that's what i was thinking too
< gmaxwell>
sdaftuar: I believe thats the first sync stuck bug I've ever seen that wasn't fixed on a restart.
< sdaftuar>
i think i've seen 0.9 nodes not be able to recover from restart
< xinxi>
sipa: we don't have to be like that. I was motivated by the project CompCert and SEL4. SEL4 is a OS kernel that's proved to be 100% consistent with the specification.
< sipa>
xinxi: that implies you have a specification
< sipa>
as i've said before, we can't have one
< sipa>
we can describe the current behaviour
< gmaxwell>
sdaftuar: well there was also the "stops on too many orphans" stuff between ~0.8 and 0.10.
< sipa>
and then formally prove that future code matches that behaviour
< gmaxwell>
(where it would start fetching blocks backwards, run into a 750 block orphan limit then stop, but even that could recover with enough restarts)
< xinxi>
sipa: I just don't understand the factor that stops us from driving a formal specification from the code.
< gmaxwell>
sdaftuar: in any case, I think doing get headers triggered on single header responses, and counting the failures, and DOSing on too many failures... would address both our concerns here.
< sipa>
xinxi: deriving? yes, we could
< sdaftuar>
gmaxwell: sounds right to me as well. for 0.13.0?
< sipa>
xinxi: i guess my point is that the only way to write a formal specification is by extracting it from the actually implemented and deployed code
< xinxi>
sipa: yeah, that's where we can start from.
< sipa>
xinxi: and not from behaviour that humans write
< btcdrak>
xinxi: the difficulty is if the code differs from the written specification the code wins. Even if you class it as a bug, changing it is extremely hard because you have to change the network consensus. There are examples where this has happened and we've just had to live with the bug.
< gmaxwell>
Yes, I think it wouldn't be more complex than that patch you currently have. (this is also not just a testnet problem-- we're just fortunate that miners have lately not be excessively rolling their timestamps forward...)
< btcdrak>
xinxi: the other problem is unknown bugs which we might not be aware of, rare edge cases say, are actually part of the consensus rules even if we dont know it.
< sdaftuar>
ok i'll see if i can whip up an improved patch
< gmaxwell>
btcdrak: the kind of "formal specification" in the sense of SEL4 can be proven to agree with the code (effectively, the specification is at least as complex as the implementation)
< btcdrak>
xinxi: so it's hard to document things you dont know
< xinxi>
@btcdrak those rare edge bugs can be eliminated by formal proofs I think.
< btcdrak>
xinxi: seems like a very worthwhile pursuit though.
< xinxi>
so the motivation of this is to avoid catastrophic failures of Bitcoin.
< sipa>
xinxi: for example, for a long time, bitcoin relied on OpenSSL's signature parsing code
< sipa>
xinxi: people thought they knew what this code did
< sipa>
xinxi: and reimplemented the logic in other places
< sipa>
but nobody checked that what they thought actually matched what openssl was doing
< sipa>
turns out, it didn't
< sipa>
so now bitcoin's "specification" implicitly depended on OpenSSL's implementation
< xinxi>
sipa: this kind of inconsistencies can be eliminated by formal proofs as well.
< sipa>
xinxi: absolutely
< sipa>
xinxi: but only if they would take OpenSSL's code into account and analyse it, and not treat it as a black box
< gmaxwell>
xinxi: I'm not sure if you have a grasp of the difficulty of what you're thinking about, go look at the size of the SEL4 kernel. I believe it's about 4000 lines of C. The isabelle specification for it is something like a half million lines, and though it proves many useful things about it, it falls far short of proving so much that agreement with the spec would be equivilent to correct in a hum
< gmaxwell>
an sense.
< sipa>
and this cross-layer effect on consensus makes it IMHO nearly impossible
< xinxi>
gmaxwell: it's about 9000 lines of code.
< sipa>
but i am not an expert on the state of the art of formal code proofs
< gmaxwell>
xinxi: k, my figures are from memory thus approximate.
< xinxi>
gmaxwell: SEL4 has to guarantee high efficiency. So the code has to be written in C which is difficult to prove.
< gmaxwell>
xinxi: yes, and Bitcoin has to achieve high efficiency, efficiency is a security parameter for us.
< xinxi>
For Bitcoin, the programming language is not a big issue, and using languages like Coq, which enables a unified way for both coding and proofs could make it a lot easier.
< gmaxwell>
No. incorrect.
< gmaxwell>
If nodes are not fast enough the system will stop converging, at some point this results in a total consensus failure.
< xinxi>
I think OCaml is quite decent in terms of efficiency. Coq can generate OCaml code.
< sipa>
well we're not going to rewrite the consensus code in another language!
< gmaxwell>
Coq can generate C code via the compcert formalization (see VST).
< xinxi>
gmaxwell: here we go.
< sipa>
(or at least not without proving that the existing code matches the new code)
< xinxi>
how many lines of code are there for the consensus part?
< xinxi>
rewriting the consensus part is not infeasible after you separate it out.
< sipa>
do you include the cryptography library? the c++ standard library? the kernel?
< gmaxwell>
Far more than SEL4, the crypto part of it alone is that big.
< sipa>
changes in any of those can affect consensus
< sipa>
at some point you have to make an abstraction
< kanzure>
"formal proofs" cannot eliminate edge cases, they can only prove that the edge case exists
< xinxi>
sipa: we can leave cryptography part there first. C++ is just hopeless for verification. It's too complicated.
< sipa>
xinxi: then i think there is nothing we can do
< kanzure>
xinxi: how are you migrating the network precisely?
< kanzure>
wtf?
< gmaxwell>
chill chill.
< sipa>
these are intesting things to discuss
< Chris_Stewart_5>
xinxi: I think someone wrote a libsecp256k1 for ocaml if you are serious about implementing
< Chris_Stewart_5>
using ctypes
< sipa>
Chris_Stewart_5: what if the ocaml implementation doesn't match the C one?
< sipa>
we won't know without analysing the one that is actually used
< sipa>
(libsecp256k1, by the way, does have formal proofs for part of its operation)
< xinxi>
I mean we can separate out libconsensus first, and then use Coq to rewrite it and generate a provably correct version of libconsensus.
< kanzure>
xinxi: there are a lot of subtle side effects from the actual running network, but everyone in here still thinks it would be valuable to pursue formal verification anyway
< sipa>
xinxi: how will you prove that the existing libconsensus (which only does script validation, not full block validation) matches that Coq specification?
< kanzure>
libconsensus imho should be a priority similar to segwit
< sipa>
kanzure: i agree. but we first need a plan for what 'libconsensus' means. people have been talking about it for ages, and have meant very different (and conflicting) things with it
< xinxi>
sipa: we don't prove the existing libconsensus. We derive the formal specification based on the existing libconsensus, and then write another libconsensus in Coq.
< kanzure>
sipa: maybe we can hijack the milan conference for these purposes (scaling bitcoin 3)
< GitHub72>
[bitcoin] JeremyRubin opened pull request #8330: WIP: Structure Packing Optimizations in CTransaction and CTxMemPoolEntry (master...structurepacking) https://github.com/bitcoin/bitcoin/pull/8330
< Chris_Stewart_5>
sipa: It just binds to the C library, so unless there is a bug in ctypes you should be ok
< sipa>
xinxi: does you derivation prove that the specification matches the current libconsensus?
< sipa>
sorry; does you derivation result in a specification that provably captures the current behaviour?
< xinxi>
sipa: no. do they have to match exactly?
< sipa>
Yes.
< xinxi>
we just take off there.
< kanzure>
can coq do outputs re: "behavior is definitely undefined here"?
< sipa>
xinxi: the specification for the network is the actually deployed code
< sipa>
any divergence from it can result in a network fork
< xinxi>
sipa: I think there can be slight difference?
< sipa>
xinxi: such as?
< sipa>
if you can't describe the current code exactly, we're done
< kanzure>
once you announce a difference, soeone will probably try to trigger those circumstances anyway :)
< sipa>
we won't rewrite the consensus layer in another language without certainty that it does not introduce any changes compared to the current code
< xinxi>
have you guys talked about this before?
< kanzure>
endlessly
< sipa>
yes
< xinxi>
many times?
< sipa>
xinxi: i don't think you're understanding what i'm saying
< sipa>
we do not prescribe the rules of the network
< kanzure>
xinxi: there is high interest in our community in formal verification and libconsensus and coq.
< Chris_Stewart_5>
^^^
< petertodd>
sipa: along with the pragmatic requirement that the new language have a sufficiently large community of programmers to be maintainable - unusual languages don't need that criteria
< sipa>
petertodd: agree, but i wasn't going to bring that up
< sipa>
the first point is that our compatibility concerns are way beyond almost any other system
< xinxi>
@petertodd that may not be a problem. Later the code will be proof driven. And the core team writes the specification, and the committers need to prove the correctness of their code, which makes them impossible to make any mistakes.
< kanzure>
xinxi: this seems like something you would like to work on?
< sipa>
xinxi: i'm getting annoyed
< sipa>
xinxi: the core team does not write the specification
< xinxi>
@kanzure yes, it is. And two professors in my school, i.e. National University of Singapore, are willing to work in it as well. They are experts on software verification.
< petertodd>
...and the specification will change over time as new features are soft-forked in, and specification flaws are fixed
< sipa>
xinxi: that's very interesting
< xinxi>
and we may have big funding support.
< xinxi>
the purpose is simple. we want to make bitcoin reliable.
< sipa>
xinxi: but i first want to understand why you say "< xinxi> sipa: I think there can be slight difference?"
< Chris_Stewart_5>
petertodd: Specifications can be changed overtime, and theoretically the proofs should reflect those changes
< xinxi>
the impact could be huge.
< kanzure>
xinxi: there are many bitcoin developers who want that as well. i think you could easily find collaborators from this conversation.
< petertodd>
xinxi: it's not going to be huge - the reliability of the consensus specification/implementation hasn't been a major problem for bitcoin - other problems are far higher-impact (scaling)
< petertodd>
xinxi: I'd suggest you focus your efforts on smart-contract use-cases, where specification flaws have been a huge problem (ethereum dao)
< sipa>
hey
< kanzure>
petertodd: nooo we do need some people thinking about libconsensus things
< xinxi>
petertodd: I think we are just lucky that Bitcoin has not yet experienced any catastrophic attacks?
< Chris_Stewart_5>
petertodd: I disagree, the consensus layer is the bedrock of bitcoin, if we screw that up in a major way we are done
< kanzure>
smart contract stuff is already getting formal verification attention, i woudn't worry about that, it was fairly high profile and papers have been published already
< petertodd>
kanzure: I'm not saying we don't, it's just that from the point of view of a researcher, they're going to get better return on their time by doing other things
< kanzure>
disagree
< xinxi>
petertodd: not all researchers work for papers.
< petertodd>
xinxi: it's not luck... it's how we make changes - turns out that intense review works
< xinxi>
impact is much more important.
< Chris_Stewart_5>
petertodd: Until it doesn't
< Chris_Stewart_5>
Bitcoin has already had issues with this in the past
< xinxi>
petertodd: OpenSSL has been used by so many people. Still it has serious bugs.
< Chris_Stewart_5>
Bip66 (or was it 62) comes to mind
< sipa>
how many consensus failures in bitcoin can you name? :)
< sipa>
yes, that's one
< sipa>
the march 2013 fork was another one
< btcdrak>
xinxi: you should probably also have a conversation with jtimon (who just pinged out). he's going a lot of the libconsensus stuff.
< petertodd>
Chris_Stewart_5: there's no reason to think yet that formal proofs actually do any better in practice, because the pool of talent that can work on them is much smaller
< sipa>
and bitcoin's scripting language before the removal of OP_VER was also a consensus problem
< sipa>
i don't know of any others tbh
< petertodd>
xinxi: indeed, which is why OpenSSL got replaced by libsecp256k1
< sipa>
OP_VER was in 2010
< sipa>
and all the others were due to supporting libraries
< xinxi>
btcdrak: Yeah some one mentioned him to me.
< sipa>
(shameless plug)
< sipa>
xinxi: it gives you an idea of how complicated it was to find some of the actually known consensus failures in bitcoin
< sipa>
the fact that no easier ones have been found may give an indication
< Chris_Stewart_5>
petertodd: I think there actually has been some considerable interest in the formal verification community in bitcoin. I've talked to a handful of researchers myself and I don't think directing them away from the core protocol is a good idea
< xinxi>
I mean the provably correct version of libconsensus may not be consistent with the existing one. The most serious result would be a hard fork, rigth?
< xinxi>
But after that, we will take off. And Bitcoin will be much more secure than before.
< sipa>
xinxi: but we'll need a hard fork to get there?
< xinxi>
if the provably correct version is done, is it worth to have a hard fork?
< sipa>
maybe
< petertodd>
Chris_Stewart_5: I'm not saying there isn't interest, I'm saying that if you want to make a high impact with formal verification deployed in production, Bitcoin isn't interesting because the risks of deploying formal verification in production are higher than the theoretical benefits
< sipa>
xinxi: but there are requirements beyond just correctness
< petertodd>
Chris_Stewart_5: whereas with smart-contract systems, the risks of the existing approaches are known to be very high - likely too high to be practical - so the risks of alternate approaches are less in comparison
< sipa>
xinxi: such as performance, and ease of maintenance
< btcdrak>
xinxi: there are other things than correctness which can cause consensus failure.
< xinxi>
petertodd: sorry, peter, I think current smart contract platforms are trying to solve some hypothetical problems. But this is a bit irrelevant.
< petertodd>
xinxi: speaking of performance, will your formal verification techniques be able to guarantee bounds on execution time/space?
< kanzure>
is jl2012 in singapore?
< btcdrak>
hk
< kanzure>
damn
< sipa>
jl2012 is in hong kong
< sipa>
what petertodd said
< petertodd>
xinxi: *ethereum* is trying to solve a hypothetical problem; systems like R3's Corda are solving very real problems. Yes, they may be problems in centralized systems, but that doesn't make those problems any less real.
< sipa>
i think proving time and space bounds (ideally on the current code!) is probably more useful in practice than a formal specification (which i expect to be much more complicated than you expect, if it is to have production value)
< xinxi>
petertodd: I think most smart contracts should run on AWS. That's much more efficient and easy to use.
< xinxi>
sipa: why do we need to prove time and space bounds?
< petertodd>
xinxi: smart contracts are about verification, not computation; "should run on AWS" makes no sense
< sipa>
xinxi: because if an attack exists that can make validation slow on some nodes, you can take advantage of that (a miner could knock out competition, or get a propagation advantage)
< petertodd>
xinxi: if you exceed the time/space bounds allowed by the actual implementation, the system fails to reach consensus
< sipa>
xinxi: if an attack exists that can make memory grow unbounded, you can knock out validation
< petertodd>
xinxi: in fact, it's fair to say that much of the current development effort is ultimately about making the upper-bound time cost of a block lower
< sipa>
xinxi: for bitcoin's security assumptions to hold, verification of blocks must be negligable in time compared to the block production rate
< xinxi>
sipa: that sounds like the scalability issues that you guys are trying to solve.
< sipa>
well, it's much more a problem today than fear of consensus failure
< xinxi>
petertodd: a simpler way to do smart contracts is to have trustworthy organization to run a platform on AWS and then people can run their smart contracts on the platform. It's scalable, efficient, and can also be verified.
< petertodd>
xinxi: the whole point of smart contracts in banking is to get away from that model
< btcdrak>
xinxi: but we are interested in decentralised systems; there's special about yet another centralised system.
< sipa>
petertodd, xinxi: i think centralized smart contract design is a bit off topic here
< petertodd>
xinxi: verifying computaitons are done correctly is not easy
< xinxi>
petertodd: yeah, we can use Bitcoin in that AWS based smart contract platform. It does not have to be decentralized.
< petertodd>
sipa: point is, I think xinxi would be much better off solving problems in that problem space first, as they're easier to solve with more impact, and that'll give them tools to tackle bitcoin later; misunderstandings about that problem space are indicative of serious misunderstandings with how bitcoin works
< petertodd>
xinxi: again, do you understand my point about verification vs. computation?
< xinxi>
petertodd: you are right. A third party's platform cannot be fully trusted and thus full verification is impossible. But most people's smart contracts don't need that kind of strong verification.
< xinxi>
To me, Bitcoin is great because it is solving a real problem.
< Chris_Stewart_5>
xinxi: Having a formally verified library of smart contracts would be useful. As in any programming language you end up having design patterns, you will see the emergence of patterns in smart contracts imo
< xinxi>
Chris_Stewart_5: it is truly useful in some extreme cases.
< petertodd>
xinxi: I suspect you're unclear as to what smart contracts even do... the sane use-cases I'm talking about, are to formalize legal contracts, allowing adherence to them to be verified - that only works because you can take the state you're in - legally speaking - and verify that it matches the smart contracts (aka protocol definitions)
< xinxi>
And the biggest concern of Bitcoin to me is not the lack of functions but its security. Many people still think it is too young and not reliable enough and could fail completely and thus don't want to adopt it.
< petertodd>
xinxi: bitcoin is exactly the same, except that on top of that, PoW allows our state to converge to a single consensus history
< petertodd>
xinxi: the most likely way bitcoin will fail right now is a failure of decentralization, which is very closely tied to scalability
< sipa>
petertodd: agree, but i still think smart contracts is off topic here.
< sipa>
of the type you're describing
< petertodd>
sipa: again, I'm trying to explain to xinxi how this stuff works - not make smart contracts the topic...
< sipa>
ok, great
< sipa>
xinxi: i think it's unlikely that people will accept a hard fork to switch to a more formally provable consensus implementation
< xinxi>
petertodd: to me, smart contracts are just contracts in code.
< sipa>
i think you're talking about different things
< petertodd>
xinxi: that's not any different from what I said... legal contracts are verification, not computation - they're about conditions that need to be met for something to be valid - aka a protocol specification
< petertodd>
xinxi: equally, the definition of the bitcoin protocol is what the bitcoin implementation accepts as valid - the fact the code that does that is somewhat intermixed with code that records state is just a historical mistake
< xinxi>
yeah, a coded contracts can be run on AWS and still legally binding.
< xinxi>
you just write the legal part in terms of conditions.
< sipa>
xinxi: but if it has very clear benefits (like performance/resource bounds), is easy to work with... maybe, but that's not something for us to decide
< btcdrak>
xinxi: in this space smart contracts are self enforcing contract
< sipa>
xinxi: i don't think people should ever expect a future hard forking change to succeed
< petertodd>
xinxi: why do you keep saying AWS here? that's completely missing the point: what you want is to be able to show to someone else (e.g a judge, but hopefully it doesn't go that far) that the smart contract hasn't been upheld
< sipa>
xinxi: so imho for formal verification to be practical in the short term, it has to be about the currently deployed code
< petertodd>
btcdrak: self-enforcing because of the underlying proof-of-work layers ensuring consensus, and the fact that people widely choose to accept the outputs of the system - bitcoin being a perfect - albeit inflexible - example
< xinxi>
My point is current smart contract platforms are mostly solving hypothetical problems.
< petertodd>
sipa: yeah, pragmatically speaking, replacing the entire codebase in a hardfork is going to be incredibly controversial at best
< sipa>
petertodd: indeed
< sipa>
petertodd, xinxi: again, please take that discussion elsewhere. yes, there is some overlap that is relevant here. but discussion about what problems smart contracts are solving is not
< petertodd>
sipa: ack
< xinxi>
sipa: yeah. My focus is still formal verification.
< sipa>
thanks
< sipa>
xinxi: have you read my BIP66 writeup above?
< xinxi>
So you are Pieter?
< sipa>
yes
< xinxi>
cool
< sipa>
i think it is useful to illustrate the difficulty of consensus problems
< sipa>
of finding
< kanzure>
btcdrak: bitcoincore.org/en/team/ is lacking usernames
< btcdrak>
kanzure: really could do with a bio page. people's user handles are not always consistent across platforms
< xinxi>
sipa: please let met read it first.
< petertodd>
xinxi: we'll, lets continue the discussion in another hour or two after you read it :)
< petertodd>
bbl!
< sipa>
xinxi: (i'll only mention this once): bitcoin core's cryptography library (libsecp256k1) does have some modest attempts at formally verifying pieces of the code, and help there would also be very welcome. It's much less ambitious than proving properties about bitcoin's consensus code, but also much easier to accomplish something in my opinion
< kanzure>
sipa: don't you guys have that libsecp256k1 paper at some point? :D
< xinxi>
sipa: that's understandable. It takes huge amount of money to get started.
< sipa>
also, #secp256k1 for that
< Chris_Stewart_5>
sipa: I just read the email, however the hard fork last July wasn't related to the implementation of BIP66 , it was just spv mining correct?
< sipa>
that was not a hard fork
< sipa>
just miners creating invalid blocks
< sipa>
and it triggered when bip65 activated
< sipa>
not bip66, which was a year earlier
< Chris_Stewart_5>
Seems that OP_CLTV was activated ~7 months ago?
< Chris_Stewart_5>
I distinctly remember the issue being July 4th of last year
< btcdrak>
yes, he means BIP66
< Chris_Stewart_5>
oh ok
< sipa>
oh, i'm misremembering
< btcdrak>
CLTV went without a hitch.
< sipa>
apologies
< Chris_Stewart_5>
np
< btcdrak>
I dont know, I think we must give a punishment.
< Chris_Stewart_5>
Seven more years of reading openssl!
< btcdrak>
too harsh. maybe no computer! and go to bed early!
< sipa>
hah
< xinxi>
sipa: so you wrote most of secp256k1?
< xinxi>
The email seems fantastic.
< xinxi>
It's truly a tough journey.
< sipa>
xinxi: i started it; most of the fancier optimizations and verifications/tests were proposed or implemented by others
< xinxi>
sipa: that's interesting. I saw it's written in C intead of C++. I thought you deliberately did that for verification?
< sipa>
xinxi: it started as C++, actually, but gmaxwell suggested converting it to C to aide with formal verification
< sipa>
as there are more analysis tools available for C than C++
< sipa>
this was very early on
< xinxi>
sipa: fantastic! I am so glad to see it's formally verified!
< sipa>
i wouldn't say it's formally verified
< sipa>
just some pieces
< xinxi>
C++ is just too complicated to verify.
< sipa>
i can discuss more on #secp256k1
< xinxi>
Is it a channel?
< sipa>
yes
< xinxi>
sipa: let's talk there.
< GitHub44>
[bitcoin] dooglus opened pull request #8331: Fix three 'comparison between signed and unsigned integer expressions' warnings. (master...fix-compilation-warnings) https://github.com/bitcoin/bitcoin/pull/8331