00:47:13Guest8623:Guest8623 is now known as amiller
01:53:40Pan0ram1x:Pan0ram1x is now known as Guest7999
02:07:32Sub|zzz:Sub|zzz is now known as SubCreative
03:15:13kanzure:if there was a way to hash the set of consensus rules, it would be interesting to vanity grind on those rules until the hash function spits out a string that starts with bitcoin
03:16:29kanzure:er, just as an amusing way to communicate your intent when you talk about a consensus rule set, instead of just saying "bitcoin" you would be communicating the exact rule set you are specifically referring to, at least in as much as collisions haven't been found or might be difficult to create through that scheme
03:16:59gmaxwell:kanzure: hah, I've joked before that the consensus rules should be hashed and we should have named the system the hash.
03:17:02gmaxwell::P
03:17:37kanzure:i stumbled into this idea over dinner with andytoshi so he might have primed me and you might have primed him
03:17:42kanzure:so this might be your idea....
03:19:10gmaxwell:A better version, I don't think that I considered grinding it.
03:19:28kanzure:well also, what exactly would be hashed? :\
03:19:37kanzure:if this was cellular automata perhaps the answer would be more obvious
03:19:51gmaxwell:One might observe that the hash of the genesis block is considerably lower than one would expect for the threshold difficiulty.
03:20:31gmaxwell:kanzure: the bytecode of the consensus rules. I've previously proposed we should be moving all the consensus rules into a bytecode with a very simple interpeter.
03:20:40gmaxwell:This is part of where the interest in moxie comes from.
03:21:06kanzure:but what about things like highest block picking rules
03:21:16kanzure:surely that is important enough to go into the hash thing?
03:21:26gmaxwell:that could be inside it as well.
03:21:44andytoshi:i was thinking to vanity-grind some moxie no-ops, but actually changing the rules is a neat idea
03:22:20kanzure:i'm also not sure what to do about updates and bugfixes. you could grind some more until you hit on some bogus rules or no-ops that allow you to get "BITCOIN" but then what... just because it says "BITCOIN" does not mean this variant is bitcoin compatible or a good idea at all :)
03:24:03kanzure:i guess the ultimate dream is some proof of bitcoin compatibility, and then any statement that can be proven is (by definition of the proof system) definitely bitcoin-compatible?
03:24:13kanzure:and then you grind on those statements
03:24:15gmaxwell:obviously one must define the hash function such that the first version says bitcoin trivially, and future versions can only be hashed by asking the prior version to hash them, and the prior version only lets them hash to bitcoin if you burned a lot of bitcoin to create then new version.
03:24:57kanzure:hah proof of burn. okay.
03:27:07gmaxwell:e.g. it's a certitifcate chain where each version authenticates its successor.
03:29:05kanzure:so you can only reduce bitcoin-compatibility going forward?
03:30:00kanzure:huh i don't know why i asked that. i had a good reason to think there was some sort of "convergence", but i've lost it.
03:30:06kanzure:also what about competing forks where both same-depth versions had same BTC amounts burned and are both valid ?
03:31:10gmaxwell:well I wasn't saying that such a mechenism was sufficient.
03:33:09kanzure:anyway yes i agree that instead of going for "BITCOIN" it should just be whatever the original hash turns out to be
04:46:03nullbyte:
08:08:52lclc_bnc:lclc_bnc is now known as lclc
08:40:28lclc:lclc is now known as lclc_bnc
09:05:16hitchcock.freenode.net:topic is: This channel is not about short-term Bitcoin development | http://bitcoin.ninja/ | This channel is logged. | For logs and more information, visit http://bitcoin.ninja
09:05:16hitchcock.freenode.net:Users on #bitcoin-wizards: andy-logbot damethos orik eslbaer_ paveljanik bvu bendavenport Transisto copumpkin tacotime adlai thrasher` yamamushi TheSeven MoALTz_ atgreen roconnor RoboTeddy nuke_ DoctorBTC Dr-G3 d1ggy_ Guest7999 DougieBot5000 mortale catlasshrugged PaulCapestany op_mul justanotheruser nsh luny HaltingState Guest82541 shesek nullbyte austeritysucks Graftec c0rw1n cluckj Hunger- Quanttek hashtagg adam3us kyletorpey Shiftos gribble ebfull hashtag_ epscy
09:05:16hitchcock.freenode.net:Users on #bitcoin-wizards: Greed Iriez ajweiss BlueMatt mbelshe Emcy_ NikolaiToryzin Graet wizkid057 jaekwon dansmith_btc Starduster midnightmagic starsoccer huseby samson_ Grishnakh Luke-Jr SubCreative BrainOverfl0w yoleaux burcin [d__d] gavinandresen danneu catcow TD-Linux ryan-c smooth Alanius AdrianG tromp Fistful_of_coins pigeons Dyaheon- Cory jbenet livegnik MRL-Relay pi07r sadgit throughnothing lechuga_ poggy JonTitor iddo hollandais amiller Tjopper LarsLarsen
09:05:16hitchcock.freenode.net:Users on #bitcoin-wizards: Muis kumavis michagogo artifexd lnovy cfields btc__ rasengan gavink hguux_ Meeh yrashk a5m0 jgarzik Keefe berndj fluffypony morcos spinza bosma Logicwax stonecoldpat sl01 optimator wiz null_radix roasbeef_ hktud0 BigBitz [\\\] mappum gnusha otoburb mr_burdell s1w go1111111 HM2 Apocalyptic sdaftuar btcdrak CryptOprah jcorgan forrestv tromp_ PRab lclc_bnc harrow @gmaxwell isis brand0 eric Krellan @ChanServ jaromil petertodd helo v3Rve espes__
09:05:16hitchcock.freenode.net:Users on #bitcoin-wizards: nickler ahmed_ warren fenn phantomcircuit kanzure bobke BananaLotus coryfields Anduck Eliel nanotube gwillen wumpus heath EasyAt asoltys_ K1773R comboy @andytoshi warptangent Guest38445 phedny so crescendo Taek @sipa sneak azariah kinlo
09:10:52lclc_bnc:lclc_bnc is now known as lclc
09:48:56d1ggy_:d1ggy_ is now known as d1ggy
10:44:24adlai:gmaxwell: "One exciting enhancement to this idea I have is making the power H(header||nonce..." what do you mean by "the power"? is that a thinko for "the POW"?
10:44:32adlai:(from https://en.bitcoin.it/wiki/User:Gmaxwell/alt_ideas)
11:12:30lclc:lclc is now known as lclc_bnc
11:26:22nuke_:nuke_ is now known as nuke1989
12:03:40Guest82541:Guest82541 is now known as maaku
12:26:11lclc_bnc:lclc_bnc is now known as lclc
13:41:51adam3us:about naming ^^ much, it seems like u dont want to call your project *coin or people will auto assume its an alt and ignore.
13:42:11lclc:lclc is now known as lclc_bnc
13:48:14midnightmagic:new name: "jimmy" . "jimmy turn the lights back on..! jimmy!"
14:17:08spinza_:spinza_ is now known as spinza
15:38:21kanzure:adam3us2: well, vanity grinding to get "BITCOIN*" is a little pointless because even non-bitcoin rule-sets could do the same. as long as it has verifiable correctness, i suppose it wouldn't be damaging.
15:56:19kanzure:.title http://kryptoslogic.blogspot.com/2015/01/openssls-squaring-bug-and-opportunistic.html
15:56:19yoleaux:Kryptos Logic Research: OpenSSL's squaring bug, and opportunistic formal verification
16:01:40lclc_bnc:lclc_bnc is now known as lclc
16:07:16gmaxwell:Thats very much relevant to my interests. Alas, they say nothing useful about the difficult problem of bridging the gap between software and input to the solver-- there they rewrote the code by hand (which is failure prone and takes time), do they expect someone to do that for all of the 400kloc of openssl?; or that current SMT solvers reason very poorly about finite-ranged numbers (basically of
16:07:22gmaxwell:all the available ones I've used, Z3 is pretty much the only one that would even return an answer on a problem as simple as that).
16:11:48kanzure:"Note that while we are using Z3 here for its convenient Python bindings," oh that is nice of them
16:13:02kanzure:hmm... http://z3.codeplex.com/
16:18:47gmaxwell:and it's lovely non-commercial use only license? :)
16:23:03kanzure:non-commercial is troubling... i don't think i've ever seen a good definition that works and doesn't break everything.
16:23:16Eliel:let me guess, that will cause problems for using it with bitcoin.
16:24:22Eliel:Although, considering that microsoft appears to have a pro-bitcoin strategy brewing, they might be open to discussion about the license.
16:43:06gmaxwell:Eliel: it's a sham; it's more or less impossible to use anything "non-commercial" in any case where you wouldn't just use it with a "all rights reserved never use this at all license"
16:43:43gmaxwell:(fortunately people happily use "all rights reserved never use this at all" without fear all the time)
16:44:14Eliel:heh, true
16:44:48gmaxwell:but if that were the only barrier involved here I'd be super happy.
16:46:01gmaxwell:The hard parts are usefully extracting the code into a from that the SMT solver can do something with; usefully expressing the hypothesis you wish to prove (and knowing that the hypothesis is right), ... and then deailing with the frequent fallout when the prover gets stuck.
16:46:59Eliel:that's why I'd personally love to have the consensus code written in Haskell :P
16:47:28gmaxwell:Eliel: uh. with implicit, hidden computational and memory complexity?
16:47:52gmaxwell:Haskell has a nicely powerful type system which is still no replacement for formal methods.
16:51:50Eliel:well, perhaps somewhat simplified haskell.
17:06:08gmaxwell:kanzure: hey, their proof appears to be wrong too.
17:06:44gmaxwell:kanzure: consider the case where c2,c1,c0,a,b are all UINT_MAX.
17:22:13Eliel:gmaxwell: is there a language that implements formal methods properly?
17:22:55gmaxwell:Coq.
17:24:04copumpkin:a few others, but chances are most things you want to do you'd do in coq
17:35:47gmaxwell:kanzure: it showed up on HN and I connected there: https://news.ycombinator.com/item?id=8866401
17:39:47kanzure:whois nanolith
17:42:36kanzure:"From an epistemological perspective, a test suite to confirm a property using chosen examples is not nearly as good as a formal proof that guarantees a property over a given domain. For simple cases, such as branch coverage, the test suite may be good enough. As complexity increases, or when testing things like modular arithmetic over an elliptic curve, unit testing leads to false confidence. But, just like in empirical testing, it's ...
17:42:42kanzure:... possible to build bad proofs. This is where the specialization comes in. There may be plenty of competent engineers who can hack at a test suite, but their results will not be nearly as comprehensive as someone trained in formal verification. It all comes down to epistemology. What do we know, and how do we know it? What possible defects exist in our system, and how bad can they be?"
17:44:17kanzure:epistemology is simple if you deny knowing anything at all :)
17:44:45kanzure:although this is less useful hehe
17:45:32gmaxwell:I probably don't disagree with what he really means; but I think the argument there is vacuous; you could replace formal methods with Aura-alignment and argue the same thing.
18:00:38luny`:luny` is now known as luny
18:01:50Eliel:I don't think that's even an argument, really. Just information without any arguments to back it up. No way to verify it unless you already know a lot about the subject matter.
18:47:23c0rw1n_:c0rw1n_ is now known as c0rw1n
18:50:46gmaxwell:hurrah:
18:51:00gmaxwell:" Update
18:51:02gmaxwell:Somebody points out that the proof is incorrect; the issue here is that we are working over the bitvector logic, which makes our proof implicitly modulo 296. The underlying assumption here, which we also made, is that the result fits into the 3 output words. This is reasonable in the context in which the function is used, but without context it does make the proof incorrect. An easy way to correc
18:51:08gmaxwell:t this is to add a few bits of slack to account for overflow:"
18:51:24gmaxwell:(I'm really happy that they didn't split hairs on it being incorrect)
18:51:47gmaxwell:(might have been polite to credit me though)
19:13:00Eliel:ah, they substituted you for somebody.
19:13:09gmaxwell:Cool!
19:13:35gmaxwell:oh hm?
19:13:50gmaxwell:It's still somebody. Thats fine.
19:13:53Eliel:ah, I get the feeling you misunderstood. I should probably have ordered the words otherwise.
19:14:04gmaxwell:yea.
19:17:22Eliel:(currently sick with a slight fever, it's affecting my thinking a bit)
19:24:13lclc:lclc is now known as lclc_bnc
21:09:52Guyver2:Guyver2 has left #bitcoin-wizards
23:05:20NewLiberty:NewLiberty is now known as NewLiberty-afk