Topic: [PRE-ANN] Qeditas: A Formal Library as a Bitcoin Spin-Off - page 8. (Read 14991 times)

I have to Study about this...without know cant tell anything but can tell much Good Luck....

Thanks for pointing this out. I fixed it. When the time comes I will contact you about the testing phase.

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 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.

very interesting approach - will read the wp later

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.

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.


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:


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:


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.

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 

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 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.

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.

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.

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):


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.

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

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.

Will do some research later.

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

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 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.


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.


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.

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

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

it should be all for money,thats correct .

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.

i dont understand anything.. but looks good