[PRE-ANN] Qeditas: A Formal Library as a Bitcoin Spin-Off

[Bill White]

Qeditas is a project to apply block chain technology to support the construction of a library of formalized mathematics. It is intended to be a realization (or possibly revival) of the QED project, as described in the QED Manifesto.

More information can be found at the website: https://iohk.io/projects/qeditas/. The white paper giving a high level description of Qeditas is here: http://qeditas.org/docs/qeditas.pdf

The short version: Bitcoin is for money; Ethereum is for computation; Qeditas is for deduction.

Comments are welcome. I'm assuming this project will be more of academic interest than monetary, but everyone is free to take part for their own reasons.
IOHK is leading the Qeditas project. If you are interested in collaborating, please contact them.

Git Repos

The code for Qeditas is on github: https://github.com/input-output-hk/qeditas

Technical documentation is of the code is available here:

http://qeditas.org/docs/QeditasTechDoc.pdf

Consensus Mechanism

The plan is for Qeditas to be a combination of proof of stake and proof of storage. Some more information is in the white paper. The proof of stake component is

Spin-Off and Snapshot

Qeditas will be a Bitcoin Spin-Off in the sense of Peter R's thread:

https://bitcointalk.org/index.php?topic=563972.0

The current plan is to take a snapshot of the Bitcoin block chain up to (not iincluding) the block at height 350,000. At this point 2/3 of the Bitcoin distribution will be complete. This block should be published on (approximately) March 31, 2015. If you have bitcoins under your (sole) control, then you will have a corresponding initial distribution in Qeditas. Your part of the initial distribution will be easiest to claim if it is in an ordinary pay-to-public-key-hash (p2pkh) address. I will include pay-to-script-hash (p2sh) addresses as well, but the claim process will be more involved and in a small number of cases p2sh claims may fail if they make use of uncommon parts of the script language.

The primary reason for this pre-announcement is to give everyone a chance to ensure their bitcoins are under their control (not on exchanges) and (preferably) in a p2pkh address. If your bitcoins are not under your control as of block 350,000, then the corresponding Qeditas units will also not be under your control.

Update: The 350,000th block has been mined. The snapshot is available here:

https://mega.nz/#!IkBUzT5A!P4Ea4zLiJtnzFTHyqxyiNFZ00_N3E45Ra6LmFoVqCao

[notsofast]

This method of distribution is really interesting, piggybacking Bitcoin's wide distribution.

Will read the whitepaper and offer more comments when I've finished it.

[sologap]

i dont understand anything.. but looks good 

[David Latapie]

Interesting. How will it be different from CLAM, distribution-wise?

I hope no retarded exchange will add this coin, since it is not supposed to be for money.

[deedou]

The short version: Bitcoin is for money; Etherium is for computation; Qeditas is for deduction.

~~~~~~~~~~~~~~~~~~~~~```

it should be all for money,thats correct .

[Bill White]

Interesting. How will it be different from CLAM, distribution-wise?

My understanding is that the CLAM project gave a fixed amount of clams (about 4) to each address with a "non-dust" amount of bitcoins, litecoins or dogecoins on a certain date in 2014. Those with many bitcoins in few addresses got few clams. Those with few millibits in many addresses got many clams. This means there was a significant redistribution of wealth. Qeditas will use a snapshot intended to preserve the wealth distribution in the Bitcoin block chain. That's the main difference between the approach of CLAM vs. a spin-off in the sense of Peter R. (Additionally, the snapshot will be only of Bitcoin, not Litecoin or Dogecoin.)

Another difference is that users should be able to claim their part of the distribution by signing a text message without revealing their private key. The CLAM approach (importing wallets) was viewed as being suspicious or dangerous to some. (To be fair, I haven't heard of any Clam-related thefts.)

i dont understand anything.. but looks good  

I am happy to hear it looks good. As for not understanding, people are welcome to ask questions. It might help improve the draft of the paper.

make a mining period also
like 1 month mining period where 10-20% of the total coins are mined.

There are two reasons to have PoW mining: to secure the network and to distribute the coins. There will already be a wide distribution of the first 2/3 of the coins according to the snapshot. The remaining 1/3 will be distributed according to a similar schedule as Bitcoin. I am open to using PoW as part of a hybrid consensus mechanism to help secure the network, but I am not convinced it's necessary. On the contrary, I suspect that for new networks with few participants, PoW might provide an attack vector for someone with old mining equipment that is otherwise unprofitable to use.

The short version: Bitcoin is for money; Etherium is for computation; Qeditas is for deduction.

~~~~~~~~~~~~~~~~~~~~~```

it should be all for money,thats correct .

Certainly I expect the coins in Ethereum and Qeditas will have some level of monetary value. My "short version" is intended to emphasize the primary intended use case for each network. Now that I read it again saying "Bitcoin is for money" is inaccurate. Perhaps "Bitcoin is for the transfer of value" would be better.

[Nxtblg]

My understanding is that the CLAM project gave a fixed amount of clams (about 4) to each address with a "non-dust" amount of bitcoins, litecoins or dogecoins on a certain date in 2014. Those with many bitcoins in few addresses got few clams. Those with few millibits in many addresses got many clams. This means there was a significant redistribution of wealth.

I think that approach was taken to get around the problem of what to do about the exchanges.

[provenceday]

Will do some research later.

[sloopy]

I am very interested in this.
I am a small BTC miner and may be able to point some gear towards this concept.
I will watch this thread, and please let me know how I may become more involved.

[olcaytu2005]

i need to read again . Really interesting but hard to understand for me. (not coz of your article, my english is not much good  )

[Bill White]

There is now a 'test' snapshot up to block 348,000. It's available as text files from this MEGA folder:

https://mega.co.nz/#F!g94EEbiQ!fVb37nZh0DDZRI8KhJE6nA

There are 4 files. The files checkp2pkh and checkp2sh are small python scripts to help people easily check for balances. The balances themselves are stored in the two files p2pkhbalances and p2shbalances. (p2pkh means "pay to public key hash" -- addresses that start with a 1 -- and p2sh means "pay to script hash" -- addresses that start with a 3.)

Each entry is one line in one of the p2*hbalances files. The line begins with 40 hex characters (giving the 20 bytes identifying the address), a colon, and then the number of satoshis. If you know the hex version of your address, then you can simply grep for the balance. Otherwise the python scripts will convert an ordinary address (base58) to hex and find the entry in the file for you. Here are three examples (each with 1.5 millibits):

Code:

./checkp2pkh 1LvNDhCXmiWwQ3yeukjMLZYgW7HT9wCMru
da822601f6a31934f9d1cb4c4763994d0d64eecb:150000

./checkp2pkh 15muB9t6z5UZBCWTkTApgEUYnMZdcnumKo
345e5be71ff89ddfff563b00fc945921409cbf38:150000

./checkp2sh 37GxXLE4tiFEKwsLzNGFdHyjVfUEbj6wt2
3d43eeeb48412e0aa12f799c1600e063074476eb:150000

This gives people can check if the balance of their addresses are correct so far before I take the real snapshot (up to block 350,000) in a few days. If you're interested in the project, please make sure as many of your bitcoins as possible are under your control as of block 350,000.

I decided to convert all native multiscript outputs into p2sh outputs. If you are looking for a particular native multiscript output, hash the script to obtain the p2sh address.

[proletariat]

My understanding is that the CLAM project gave a fixed amount of clams (about 4) to each address with a "non-dust" amount of bitcoins, litecoins or dogecoins on a certain date in 2014. Those with many bitcoins in few addresses got few clams. Those with few millibits in many addresses got many clams. This means there was a significant redistribution of wealth. Qeditas will use a snapshot intended to preserve the wealth distribution in the Bitcoin block chain. That's the main difference between the approach of CLAM vs. a spin-off in the sense of Peter R. (Additionally, the snapshot will be only of Bitcoin, not Litecoin or Dogecoin.)

What's wrong with wealth redistribution? the exchanges will get the most shares with BTC from their customers and few of these customers will ever know about Qeditas until it's too late.

[d-leit]

Interesting idea. In the white paper you seem unsure if you'll use Coq as the prover. You should definitely use Coq. i didn't really get why you're reluctant to commit to it?

Also, proletariat has a good point about exchanges. i don't keep coins on exchanges so it's no big deal to me, but am ok if you redistribute.

[Bill White]

What's wrong with wealth redistribution? the exchanges will get the most shares with BTC from their customers and few of these customers will ever know about Qeditas until it's too late.

I appreciate your input. The issue of whether the block chain should be preserved or there should be some redistribution was debated at length in Peter R's thread (linked in the OP). I found the arguments in favor of preserving the block chain more persuasive. The code will be open source. It's possible someone will start a second network with a redistribution perceived as more fair and overtake Qeditas.

Regarding the specific issue of exchanges, those who understand cryptocurrencies know that they forego certain opportunities by allowing third parties to hold their coins. The general spin-offs idea is quite old now. Concretely, even if Clams is not considered a spin-off, those holding coins on exchanges still lost out on Clams they might have gotten. Nevertheless, I recognize it's an issue, and that's why I wanted to ensure this Qeditas preannouncement gave people a chance to have as many coins at Block 350,000 under their control as possible.

[Bill White]

Interesting idea. In the white paper you seem unsure if you'll use Coq as the prover. You should definitely use Coq. i didn't really get why you're reluctant to commit to it?

My primary concern is consistency. If someone were to prove False in the system, then every proposition would be (trivially) provable. As the white paper remarked, False was proven in Coq twice at proofmarket.org. It seems the first time False was redefined (sounds like Pollack inconsistency); this is easy to avoid. The second time it seems Coq 8.4pl3 was actually proven inconsistent. Coq is a very nice system, but it is also still experimental.

My current thinking is that the Qeditas proof checker should be like Coq, but more restricted. The intention of the restrictions is to ensure (as much as possible) consistency. Perhaps people could prove theorems in Coq and then do a second check that the Qeditas proof checker also accepts the proof. I must admit, however, that there are some issues with the logic of Coq (e.g., universe levels and termination checking) where I'm not yet sure what restrictions would be appropriate.

Ideas?

[kushti]

1. Bill, do you have any ETA on more detailed spec?

2. Why Bitcoin distribution? With this, you'll get a lot of never touched Satoshi's money & bitcoin centralized exchanges & feds holding arrested bitcoins & hackers did steal a lot recently into the new economy, and that looks a bit weird 

[Bill White]

1. Bill, do you have any ETA on more detailed spec?

At the moment, I am going back and forth between implementation in OCaml and modifying a corresponding (partial) specification in Coq. My hope is to release a first version of the OCaml code in mid-April. I expect to start off with a test run or two at that point. Hopefully by May the network will be running. The Coq code (which can act as a formal specification of part of it) will hopefully be released at around the same time. If there's enough interest, I might produce another pdf document to try to explain things after that.

2. Why Bitcoin distribution? With this, you'll get a lot of never touched Satoshi's money & bitcoin centralized exchanges & feds holding arrested bitcoins & hackers did steal a lot recently into the new economy, and that looks a bit weird 

The initial distribution of a coin -- especially one that incorporates proof-of-stake -- is always tricky. I'm obviously very interested in the success of the project, but I have no interest in engaging in a presale or doing crowdfunding. The spin-offs thread of Peter R presented what seems to me to be a very good solution to the problem. The arguments given there in favor of using the Bitcoin block chain convinced me.

Of course, I could modify the distribution, but I would like the distribution to be simple and clear. If I were to start making modifications, then there would always be the suspicion that the modifications are in my favor. I will contrast with Clams. (First, to be positive, it seems Clams has managed to build up a community based on their interesting distribution strategy. This shows a distribution based on another block chain can be a successful way to start a coin.) The distribution used by Clams could easily have been manipulated simply by someone (with advance knowledge) splitting their bitcoins into many addresses. (I'm not accusing them of that myself nor do I have evidence of it.) Using Peter's Principle (a coin-proportional distribution) makes this kind of manipulation impossible. In addition, I have made sure to announce the block in advance. I don't think Clams did this. Incidentally, I suspect Satoshi and exchanges got a high percentage of Clams anyway, since they use many addresses.

It's simplest just to leave the distribution as it is initially. I don't particularly want exchanges, federal agencies and hackers to have a large part of the distribution. However, redistributing in advance may have unintended and controversial side effects.

After the network starts, I expect there will be a great deal of market-based redistribution. The Peter R thread also discusses this:

For the people here who are questioning the "fairness" of this proposal, I ask you to reconsider your assumptions after analyzing the economic incentives at play here: 

Let's say you truly believe that a proof-of-stake (PoS) system is better than a proof-of-work system and the market would be wise to adopt this if only given a chance.  When the PoS spin-off launches, many bitcoin holders will dump their "free coins" at say a valuation equal to 0.01% of the bitcoin market cap.  This means that for an investment of X BTC, you could amplify your wealth by a factor of 10,000X if you are correct and PoS becomes dominant.  You would be rewarded for your insight by natural market mechanisms.  You know most bitcoin users will remain impartial (they will be holders by default) so your PoS coin will naturally have a wide user base if it is in fact useful. 

Spin-offs also benefit the community as a whole:

-Bitcoin users that remain impartial to the experiment should appreciate spin-offs because they automatically get piggybacked to the new network with little effort on their part and without risk to their cryptocurrency wealth.   

-Alt-coins doubters should appreciate spin-offs because they represent free money that they can immediately dump on the open market. 

The plan is that people will be able to "claim" their initial distribution by simply signing a message using a bitcoin client. (They will not need to share their private key with a third party or external program to do this.) This will allow people who are not interested in Qeditas to sell their (Qeditas) fraenks to someone for bitcoin (or an altcoin or some fiat currency). They will never even need to download Qeditas related software to do this. This is another difference from Clams. Clams did not include an independent way to claim the initial distribution. It seems that a consequence of this is that the Clams network is currently dominated by a third party (Just Dice) which makes it very easy for people to claim their clams.

Those interested in Qeditas at the beginning should be able to buy these claims for a very cheap price:

When your coin launches, it may trade at 0.01% of the bitcoin market cap.  You can buy 10,000 of your alt coins for 1 BTC.  If you continue to develop your alt, and if people begin to agree that it is useful, your 10,000 alt coins will be worth more than 1 BTC (possibly a lot more).

Since I am interested in the success of Qeditas, I would be willing to buy 10,000 (Qeditas) fraenks for 1 bitcoin when the network starts. I suppose a developer being forced to buy his own coin is a bit strange, but it's also part of why I like the idea. I hope it makes it clear to reasonable people that this is a project I'm doing because I believe in it.

[d-leit]

Interesting idea. In the white paper you seem unsure if you'll use Coq as the prover. You should definitely use Coq. i didn't really get why you're reluctant to commit to it?

My primary concern is consistency. If someone were to prove False in the system, then every proposition would be (trivially) provable. As the white paper remarked, False was proven in Coq twice at proofmarket.org. It seems the first time False was redefined (sounds like Pollack inconsistency); this is easy to avoid. The second time it seems Coq 8.4pl3 was actually proven inconsistent. Coq is a very nice system, but it is also still experimental.

My current thinking is that the Qeditas proof checker should be like Coq, but more restricted. The intention of the restrictions is to ensure (as much as possible) consistency. Perhaps people could prove theorems in Coq and then do a second check that the Qeditas proof checker also accepts the proof. I must admit, however, that there are some issues with the logic of Coq (e.g., universe levels and termination checking) where I'm not yet sure what restrictions would be appropriate.

Ideas?

i don't know enough about the internals of Coq to really say. "like Coq, but more restricted" sounds like that mathgate proof checker. Does it not have these issues? i tried to use it briefly last summer. To be honest it was hard to write correct proofs in it (no real feedback for errors). It was too annoying (even with the promise of free bitcoins) so i quickly gave up.

[nakaone]

very interesting approach - will read the wp later

[Trent Russell]

Interesting. I'll keep an eye on this as well. I can help test it when it's ready.

By the way, there's a typo in the white paper, Section 8:  "require for the Qeditas" should be "require for Qeditas" or "require for the Qeditas project".

i don't know enough about the internals of Coq to really say. "like Coq, but more restricted" sounds like that mathgate proof checker. Does it not have these issues? i tried to use it briefly last summer. To be honest it was hard to write correct proofs in it (no real feedback for errors). It was too annoying (even with the promise of free bitcoins) so i quickly gave up.

I didn't find it so difficult to use, at least in the beginning when the problems were easy (and free). Looking back I wish I'd spent more time trying to get more bitcoins proving theorems, but at the time I wasn't willing to risk 10 mbits a week.