[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

[1715699889]

1715699889

[1715699889]

1715699889

[1715699889]

1715699889

[1715699889]

1715699889

[1715699889]

1715699889

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

[Bill White]

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

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

[TrackCoin]

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

[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?

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?

The logic/framework of Egal (the mathgate proof checker) is simple type theory. This goes back to Church (1940) and is well-understood. On top of that there's a set theory (Tarski-Grothendieck). If this turned out to be inconsistent, it would be a surprising mathematical result. (By way of contrast, if Coq turned out to be inconsistent, it would mean the type theory needs to be patched in the next release.)

Notice: We are less than 64 blocks from the snapshot, so it should occur within in the next 12 hours.

[Bill White]

Bitcoin is less than 13 blocks away from the last block to be included in the snapshot (349,999). This is a final reminder to remove bitcoins from exchanges if you want to be able to claim the corresponding initial distribution for Qeditas.

Edit: The 350,000th block has been mined. When the snapshot data is ready, I will post it for those who want to verify its accuracy.

[Bill White]

The snapshot is available:

https://mega.co.nz/#F!0xhzUbTS!h-LeyiTbF9dXgusKCc_bfQ

It contains the balances of all p2pkh and p2sh addresses as of block 350,000 (after txs in block 349,999 and before txs in block 350,000). Native multisig and raw scripts were converted to p2sh.

If anyone notices an address with an incorrect balance, please post here to let me know.

[Bill White]

There is a Coq formalization corresponding to Qeditas available here:

git clone git://qeditas.org/qeditastheory.git

It is far more detailed than the white paper, but is likely not as readable. It is mostly an extension of the "ledgertheory" Coq development I posted two months ago.

[Trent Russell]

There's a recent thread on the coq-club mailing list about a way to prove False in Coq:

https://sympa.inria.fr/sympa/arc/coq-club/2015-03/msg00134.html

[Bill White]

There's a recent thread on the coq-club mailing list about a way to prove False in Coq:

https://sympa.inria.fr/sympa/arc/coq-club/2015-03/msg00134.html

Thank you for pointing me to this discussion. At this point I don't see a way to build Qeditas on top of Coq while ensuring consistency. Unless someone can suggest a way, my inclination is to build Qeditas on top of Egal.

[Bill White]

Here is an update on Qeditas.

I have written code for compact trees (a variant of a Merkle Patricia tree, see https://bitcointalk.org/index.php?topic=949880) and used it to create the initial compact tree corresponding to the snapshot. Unfortunately, there are some efficiency issues and it's clear more work is required to make the code practical. Keeping the whole tree in memory is too RAM intensive (the full tree requires roughly 1.6 GB). Also computing hashroots (if no intermediate hashes are stored) takes far too long. I have some ideas for how to fix these issues, but it does mean things are taking longer than expected. I would still like to get the network running in April, but it may run into May.

In other news: I believe I have an easy way for people to buy and sell their claims from the snapshot. People can use their bitcoin address to "endorse" their claim to a Qeditas address. Here is an example of how this work.

Address 1LvNDhCXmiWwQ3yeukjMLZYgW7HT9wCMru had a balance of 1.5 mbits at the time of the snapshot.

Suppose Alice is has the private key for this Bitcoin address.

Suppose Bob with the Qeditas address QVmqaNmBE3GbTPG3kqNh75mYpA6uUcxs35 wants to buy this claim from Alice.

Alice can sign a message

"endorse QVmqaNmBE3GbTPG3kqNh75mYpA6uUcxs35"

with her bitcoin address. Qeditas will use such a signed message to allow Bob to spend from the Qeditas address corresponding to 1LvNDhCXmiWwQ3yeukjMLZYgW7HT9wCMru.

Presumably Bob will pay some bitcoins to Alice's address above in exchange for this endorsement (although at an exchange rate of 10000:1, Bob would only need to pay Alice 15 satoshis).

Note that this will not require Alice to download or use Qeditas or any third party software.

Please post if you have any questions. Otherwise I will try to post updates as appropriate.

[kushti]

Another concern around using 350K Bitcoin's snapshot. As you're going to use Proof-of-Stake, and majority of Bitcoin holders will no participate in the Qeditas consensus from day 1, so generating balance will be low during early days. In this case, system could be overtaken by a big holder, history attack is also possible(you'll need to introduce checkpoints) etc.

How do you want to solve compact Merkle tree problems?

What's new in the 'qeditastheory'  in comparison with the 'ledgertheory'?

[yampi]

How was the distribution balances calculated?
Are these balances in lowest unit forms?

[Bill White]

Another concern around using 350K Bitcoin's snapshot. As you're going to use Proof-of-Stake, and majority of Bitcoin holders will no participate in the Qeditas consensus from day 1, so generating balance will be low during early days. In this case, system could be overtaken by a big holder, history attack is also possible(you'll need to introduce checkpoints) etc.

I agree with the concern. I think if a single large bitcoin holder wants to overtake the network in the first few days, they are likely to succeed. The hope is that there are enough participants at different balance levels to prevent this, but it's a real danger.

As for checkpoints, I like the solution Nxt uses of not allowing reorganizations beyond N blocks and plan to use this in Qeditas. This makes the criteria "weakly subjective" in Vitalik Buterin's terminology, but realistically I think this is good enough. To be honest, I think even in a POW network like Bitcoin, if there were a reorganization beyond 24 hours there would likely be some kind of social (human) consensus very quickly to deny the reorganization. If I'm right about that, the criteria Bitcoin uses is not truly "objective."

How do you want to solve compact Merkle tree problems?

I'm still experimenting, but the idea is simple. The "real" tree is a sparsely populated binary tree of depth 162 with account assets at the leaves. Instead of holding the full compact tree in memory, I break it into several parts and save the different parts into files. (I could use a database, but I don't think I need one.) I can describe these "parts" as follows:

The top of the tree: from the root through the first 6 levels.
The midsections of the tree: from level 6 to level 14.
The bottom parts: the rest of the way to the leaves.

The numbers are a bit arbitrary, and there's actually a general data type that can be used to choose multiple ways of breaking the tree into parts. For simplicity, let's assume it's broken up as above.

A transaction mentions certain addresses. The leaves corresponding to those addresses are to be transformed. For this reason we need each "bottom part" that contains one of these leaves. We also need the particular midsections above those selected bottom parts. The top part is always needed. All these parts are loaded into memory to do the transformation. This should be a very small part of the tree in practice.

After the transformation in order to save the new (transformed) tree, only the new versions of the selected bottom parts, midsections and top part must be saved. The unselected parts are unchanged and we already have them saved in files.

Another side effect is that to calculate the hashroot of the full tree is very easy since it can start hashing from the tops of the midsections.

There are, of course, tradeoffs. On one extreme is not to break up the tree at all. In that case too much RAM is consumed and the operation of computing the hashroot takes too long (since every intermediate hash needs to be computed). On another extreme, every single node in the tree could be saved in files. I haven't tried this, but I think it would require too many file operations.

Does this sound reasonable? Do you know of some better techniques to handle this?

What's new in the 'qeditastheory'  in comparison with the 'ledgertheory'?

I will answer this in another reply since it will be a bit longer.

[Bill White]

How was the distribution balances calculated?
Are these balances in lowest unit forms?

The distribution given to an address was determined by the sum of the satoshis in the unspent transaction outputs to that address as of the snapshot (Block 350,000, not counting this block).

The lowest Qeditas monetary unit is a cant (short for Cantor). It corresponds to 0.0001 satoshis in the snapshot. This means the number of satoshis in the snapshot will be multiplied by 10,000 in order to determine the number of initial cants.

Example:

Suppose someone has a bitcoin address A, and there were two unspent transaction outputs to A as of the snapshot. One tx output to A was worth 10 satoshis and the other was worth 1 satoshi. The balance of A is 11 satoshis in the snapshot.

In the initial distribution the Qeditas version of address A will have a balance of 11 * 10,000 cants, i.e., 110,000 cants.

Of course, "cants" like "satoshis" are too small to be a useful unit in most cases. A more reasonable level would be a fraenk (short for Fraenkel), which corresponds to 10¹² cants.

Example:

Suppose someone has a bitcoin address B that had a balance of 2 bitcoins (200 million satoshis) as of the snapshot.

In the initial distribution the Qeditas version of address B will have a balance of 2 fraenks (2 * 10¹² cants).

Fraenks are like bitcoins (as units) and cants are like a small fraction of a satoshi.

Does this answer your questions?

[Bill White]

What's new in the 'qeditastheory'  in comparison with the 'ledgertheory'?

First, a few minor things:

I changed "addresses" and also "mtrees" and "ctrees" to use 168 bits (edit: 162 bits) instead of 160. This was to account for having different "kinds" of addresses. Now I've decided I only need 4 kinds, so the "right" number would be 162. (The 4 kinds of addresses are p2pkh, p2sh, hashes of terms, intentions (hashes of nonced data), but this isn't in the Coq code.)

MathData.v

There is a new file MathData.v that contains a skeleton of higher-order logic (simple types, terms and proofs). It isn't a real formalization of higher-order logic, but is just enough to know what kind of "data" would be in a publication and what it means for some "data" to use/support an object or proposition. Here "data" means a sequence of mathematical parameters, definitions, axioms and theorems (with proofs). If the data contains a proposition as an axiom and this is justified by the fact that the proposition has been proven before, then the data "uses" the proposition. Essentially the data is building on someone's previous work.

Assets.v

Assets.v has been extended to contain several new kinds of preassets. In ledgertheory there were only "currency" and "publication". In qeditastheory there are

• currency: the currency units as before.
• bounty: currency units locked to a proposition. The idea is that this can only be spent by someone who publishes a proof of the proposition. (In the implementation it should also be spendable by someone who proves the negation of the proposition.)
• owns: this records ownership of a mathematical object or proposition by an address. (A boolean is used to determine if it's being owned as an object or proposition. This is a little obscure and in the ocaml implementation I'm making separate preassets of OwnsObj and OwnsProp.)
• rights: rights can be spent to make use of an object or propostion in a publication. (Again, a boolean determines if it's an object or proposition. Again, the implementation will split into RightsObj and RightsProp.)
• intention: this is just some hash that must be published in advance of publishing a "publication." It's part of a protocol intended to prevent an attacker from taking someones publication and then immediately publishing it as his or her own work. An "intention" (a hashed nonce of the publication) must be published and confirmed before a "publication" can be confirmed.
• publication: this is a placeholder for publishing "data" (as in MathData above). There's also a place for a "nonce" for the purpose of checking if the appropriate "intention" has already been sufficiently confirmed.

I changed "obligations" from using lists of addresses (intended to handle multisig) to just using addresses. I can do this since I decided to support p2sh addresses.

There are also a number of new definitions and results about rights and so on (e.g., rights_mentioned).

Transactions.v

There are only a few changes here.

There are some additional checks for whether or not a transaction is valid (see tx_valid and tx_outputs_valid). For example, the transaction cannot declare two different owners of the address of a mathematical term. (Well, it's complicated. There can be one owner of an address "as an object" and a different owner of an address "as a proposition." Using booleans helped make some of these statements in a concise, but tricky way.)

Signatures are generalized (see "gensignat"). The idea is to allow for "ordinary signatures" and for "endorsement signature".  The endorsed signature will be a combination of a bitcoin signed message of the form "endorse Q" and a signature of the transaction by the key for Q. This is what will allow for bitcoin users to "endorse" their part of the distribution to a Qeditas user without needing to use Qeditas.

There is also a new kind of obligation for simply "moving" assets (see check_move_obligation and check_tx_signatures). Suppose an asset A is held in an address B but only the private key for a different address C is allowed to "spend" A. (This could be the case because C is allowing B to stake with the asset.) There's a potential attack in which someone keeps sending unwanted assets to B which B cannot spend. To mitigate this, I decided that B can sign for a transaction which simply "moves" the asset A. The "move" would send the asset to a separate address without changing the underlying preasset or the obligation for spending it (only C will be able to "spend" it).

LedgerStates.v
MTrees.v
CTrees.v

These are similar to before, but with many new cases due to the new preassets. Also, there must be new definitions about "consuming rights" and so on.

Once we get to this stage, there is a new important distinction. In ledgertheory sometimes we needed to check that a certain asset exists (in order to spend it). In qeditastheory we sometimes need to also check that a certain asset does not exist. For example we may need to verify that some address corresponding to a proposition does not yet have an owner. In order to check that no asset of a certain form is held at an address, we need the full list of assets at the address. There are many new definitions and results about this new "full" case (e.g., see mtree_full_approx_addr and In_full_needed_owns).

Blocks.v

There are a number of new properties corresponding to rights and ownership and so on (the new preassets).

In addition I took away some of the use of dependent types for describing blocks and block chains. I think in ledgertheory dependent types were overused in Blocks.v in ways that complicated things more than was really needed.

[kushti]

Thank you for the detailed explanation, Bill. I think about using you compact trees in my Scorex project, so I will have to think about effective implementation as well,  but it will be not within next days. Unfortunately, I've never read about data structures like this.

Have you started to work on consensus part? PoS + PoR sounds attractive

[Bill White]

Thank you for the detailed explanation, Bill. I think about using you compact trees in my Scorex project, so I will have to think about effective implementation as well,  but it will be not within next days. Unfortunately, I've never read about data structures like this.

Have you started to work on consensus part? PoS + PoR sounds attractive

I haven't yet started implementing the consensus part, but will let you know.

What is Scorex? Do you have a link?

[kushti]

I haven't yet started implementing the consensus part, but will let you know.

What is Scorex? Do you have a link?

It's the compact(<4K lines of Scala code) cryptocurrency engine for hackers, intentionally not production-ready. Pre-release code is already on Github https://github.com/ConsensusResearch/Scorex-Lagonaki , but it's too early to use it, I need to implement disk persistance for state and fix some networking issues. There are two consensus algos in the code, Qora-like and Nxt-like, with possibility to switch by changing 1 line of code (in Constants.scala).  The purpose of Scorex atm is to play with consensus in almost-real-world environment, then I want to add an implementation of some scalability proposal, also I have(very rough atm) idea about scalable smart contracts implementation(w. private contracts support in decentralized environment), I'll describe the idea to you in PMs when I will have more clear picture.  Also the project is open to other researchers willing to implement proof-of-concept within days, not weeks or months.

[Bill White]

Another update is due.

The good news is that the code to swap parts of the compact Merkle tree in and out of RAM is working, so this problem is solved. I may need to do more work to make it more efficient, but I've moved on to implementing other parts now.

The bad news is that it's clear the code as a whole will not be ready by the end of April. I think it's best not to try to give an estimate at the moment.

I've spent some time looking at Egal (the proof checker mathgate used) again. It's led me to think about improvements I can make to Qeditas.

One nice feature of Egal is that previous definitions can be imported simply as a parameter in a document, as long as a hash value identifying it as a specific term is given. Using this feature an author can avoid repeating every definition all the way back to the primitives in every document. However, some definitions are needed so often (e.g., equality, negation, conjunction, etc.) that it doesn't make sense to repeat these definitions in every document in which they're used. Egal handled this by having "signature" files. It seems to be similar to importing a module in Coq. I think Qeditas should also handle signatures.

It also seems that Egal is only weakly tied to Tarski-Grothendieck set theory. In principle it should be able to do proof checking for any theory that can be expressed in simple type theory. I think it's a good idea to also allow the publications of theories. If one of these theories turned out to be inconsistent, the inconsistency should be localized to that theory. Initially I think there will be two theories: the empty theory (just simply type theory) and Tarski-Grothendieck set theory.

Both theories and signatures introduce a new complication: In order to verify correctness of a document depending on a theory/signature, a Qeditas node must be able to look up the details of the theory/signature. This means each node will need to explicitly keep a copy of all theories and signatures. This would only become a problem if people created lots of "spam" theories and signatures. The best way I can think of to prevent such spam is to have a very high burn requirement when a theory or signature is published.

Suppose whenever a theory or signature is published by a transaction, the transaction must burn 21 fraenks per KB. Since there is a hard limit of 21 million fraenks, this ensures that there will never be more than 1 GB of theory/signature data. Hopefully this will be sufficiently costly to encourage people to design theories and signatures carefully before publishing them.

I'm modifying the Coq sources in qeditastheory to add signatures and theories. I have also made some modifications to the Coq source so that hashes of important data (e.g., documents, terms, and so on) is computed as a root of a Merkle tree. This modification will be necessary to support the proof of retrievability aspect of the consensus mechanism.

I hope to commit updates to the qeditastheory github git repo later this afternoon.

git clone git://qeditas.org/qeditastheory.git

[Daedelus]

Just FYI, I think Kushti released Scorex a couple of days ago, if you're interested in knowing more.

[Bill White]

Just FYI, I think Kushti released Scorex a couple of days ago, if you're interested in knowing more.

Thank you for letting me know. I have my hands full at the moment, but it's definitely on my agenda to look into what he's done as soon as I have some extra time.

[cryptic4000]

i dont understand anything.. but looks good 

lol. Maybe you should rephrase "I am ready with my BTC for gamble. Game is on."

[kushti]

Can you recommend any books / tutorial on Egal? Even with Coq (which is pretty popular) I have problems on regular basis with finding information able to help me in the internets. I'm not a mathematician

Do you have ETA for opensourcing Qeditas code in Ocaml?

[Bill White]

Can you recommend any books / tutorial on Egal? Even with Coq (which is pretty popular) I have problems on regular basis with finding information able to help me in the internets. I'm not a mathematician

As far as I know the only thing written about Egal is the manual: http://mathgate.info/egalmanual.pdf
It also comes with the source code: http://mathgate.info/egal.tgz

Without going into a review, the manual isn't very professionally written. Nevertheless, it was a valuable resource when I started trying to understand the code in December. I'm not sure the manual is good as a tutorial, but the first chapter does have some very simple examples.

Do you have ETA for opensourcing Qeditas code in Ocaml?

My intention has been to get a test version working before opensourcing it. This has taken longer than I expected. I will estimate mid-May, but it's only an estimate.

[Trent Russell]

Can you recommend any books / tutorial on Egal? Even with Coq (which is pretty popular) I have problems on regular basis with finding information able to help me in the internets. I'm not a mathematician

As far as I know the only thing written about Egal is the manual: http://mathgate.info/egalmanual.pdf
It also comes with the source code: http://mathgate.info/egal.tgz

Without going into a review, the manual isn't very professionally written. Nevertheless, it was a valuable resource when I started trying to understand the code in December. I'm not sure the manual is good as a tutorial, but the first chapter does have some very simple examples.

If someone wants to look at introductory examples, there are a lot of them in the documents from last year's treasure hunt.

https://mathgate.info/d/doc.php

Edit: Just looked at the manual. Looks like these documents are talked about in chapter 6.

[provenceday]

it's interesting.

will look this later.

[Bill White]

it's interesting.

will look this later.

Great!

If someone wants to look at introductory examples, there are a lot of them in the documents from last year's treasure hunt.

https://mathgate.info/d/doc.php

Edit: Just looked at the manual. Looks like these documents are talked about in chapter 6.

Thank you for posting this link. I should've thought of it yesterday.

[d-leit]

i will look at Egal, but i would still be more likely to try things out if it used Coq instead.

about selling claims you wrote this:

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.

and:

Address 1LvNDhCXmiWwQ3yeukjMLZYgW7HT9wCMru had a balance of 1.5 mbits at the time of the snapshot.

Suppose Alice is has the private key for this Bitcoin address.

Suppose Bob with the Qeditas address QVmqaNmBE3GbTPG3kqNh75mYpA6uUcxs35 wants to buy this claim from Alice.

Alice can sign a message

"endorse QVmqaNmBE3GbTPG3kqNh75mYpA6uUcxs35"

with her bitcoin address. Qeditas will use such a signed message to allow Bob to spend from the Qeditas address corresponding to 1LvNDhCXmiWwQ3yeukjMLZYgW7HT9wCMru.

Presumably Bob will pay some bitcoins to Alice's address above in exchange for this endorsement (although at an exchange rate of 10000:1, Bob would only need to pay Alice 15 satoshis).

Note that this will not require Alice to download or use Qeditas or any third party software.

Please post if you have any questions. Otherwise I will try to post updates as appropriate.

Do you still plan to use this "endorse" idea to buy people's claims? If so, you could begin buying these signed endorsements already (pre-lounch), right? i have two addresses that had about 0.4 bitcoins in them each, so i guess you're saying you would pay me 0.00008 for two signed endorsements messages? probably the fee isn't worth sending me 0.00008 bitcoins. It seems like practically you could only buy claims of people who have addresses with a lot of bitcoins.

[Bill White]

i will look at Egal, but i would still be more likely to try things out if it used Coq instead.

Now that I am modifying the plan to allow for generic theories/signatures, the choice of theorem prover is not so vital. Qeditas will probably use the type checking/proof checking code from Egal, but that's all. To publish a Qeditas document only the "compiled" document will be required and it should be easy to make modifications to a number of theorem provers to produce the kind of document Qeditas expects. It's conceivable that some users will produce the documents with a slightly modified version of Coq while others will produce them with a slightly modified version of Egal.

Do you still plan to use this "endorse" idea to buy people's claims? If so, you could begin buying these signed endorsements already (pre-lounch), right? i have two addresses that had about 0.4 bitcoins in them each, so i guess you're saying you would pay me 0.00008 for two signed endorsements messages? probably the fee isn't worth sending me 0.00008 bitcoins. It seems like practically you could only buy claims of people who have addresses with a lot of bitcoins.

Yes, I do still plan to buy people's claims as bitcoin-signed "endorsements." Maybe for small claims like the ones you are describing it makes sense to buy combine many of the bitcoin payments into one bitcoin transaction with many small outputs. I'll think about a way to do this.

[Bill White]

The Coq code corresponding to the theory of Qeditas has been updated to include theories and signatures:

git clone git://qeditas.org/qeditastheory.git

Allowing general theories will make Qeditas more flexible as it will be able to support different foundations. Signatures will allow people to more easily import common definitions and previous results into their documents.

In addition the part of the formalization dealing with the underlying logic is now more detailed (MathData.v).

My previous estimate for when the first ocaml code would be released was in mid-May, but it is likely I will need another week.

[Nthused]

So a bit like CLAM ?

[Bill White]

So a bit like CLAM ?

The initial Qeditas distribution is like CLAM in that it is based on a snapshot of the Bitcoin block chain. There are three differences: The initial distribution of Qeditas fraenks will be the same as the number of bitcoins at the corresponding address at the time of the snapshot. Secondly, Qeditas is only using the Bitcoin block chain, whereas CLAM also used Litecoin and Dogecoin. Finally, using endorsement messages it will be possible to sell Qeditas units without needing to download the Qeditas software or compromising the corresponding private keys.

[Bill White]

I created a fork of Egal to support Qeditas.

git clone git://qeditas.org/egal.git

github is warning me about my profile being hidden from the public for some reason. If github doesn't show it to you, you might still be able to clone it:

git clone https://github.com/billlwhite/egal.git

For the most part this fork is the same as the Egal released last year which can still be found here:

http://mathgate.info/egalrelease.php

(Incidentally, there are still 9 theorems in the file oldformaldocs/CategoryProblems.mg with bitcoin "treasures". I have been able to prove all the theorems and released my solutions as oldformaldocs/CategoryPartialSolns.mg, but in 9 cases I don't have a proof that gives the right private key.)

There's a minor difference in how polymorphic definitions are handled that makes this fork of Egal in some ways incompatible with the original Egal, but I included a new command line argument "-polyexpand" that replicates the old behavior.

The main thing that is new is the ability to create Qeditas theories, signatures and documents. Qeditas documents are in a binary format which is not intended to be created directly. Egal can be used to specify documents in an ASCII format that can be written and read by humans. This new fork of Egal can output the binary format Qeditas requires. To support this some of the code I've written for Qeditas was included in a subdirectory src/qeditas.

Several examples based on the mathgate documents can be found in qeditasdocs1 and qeditasdocs2.

Since there's interest in using Coq instead of Egal, someone familiar with Coq might be interested in doing something similar with Coq. I suspect the simplest method for creating Qeditas documents with Coq is to translate from compiled Coq files to Qeditas documents.

The code for Qeditas itself is still in production. I keep hoping I will have a preliminary version of Qeditas ready within a week. Hopefully this prediction will soon be correct.

[Bill White]

Just in case bitcointalk.org goes down for a significant amount of time again, I'll point out that I have the domain qeditas.org. Currently it's just a collection of Qeditas related links (e.g., a link to this thread), but I could make it the place for announcements if it becomes necessary.

[jamesjde]

I am unable to see any of the GitHub content (404).

[Trent Russell]

I am unable to see any of the GitHub content (404).

Same for me.

Edit: But cloning does seem to work. Strange.

Code:

git clone https://github.com/billlwhite/egal.git

[Bill White]

This is unpleasant news to wake up to, but thanks for informing me. I will look into alternatives to github.

[Bill White]

github has unhidden my profile, so the repositories should all be visible via the links again now. I may set up my own git server to remove this unnecessary dependence on a third party site (github).

Edit (June 26 2015): The git repos are now hosted at qeditas.org.

Code:

git clone git://qeditas.org/qeditas.git
git clone git://qeditas.org/qeditastheory.git
git clone git://qeditas.org/cryptohash.git
git clone git://qeditas.org/ledgertheory.git
git clone git://qeditas.org/egal.git

They can also be viewed using gitweb here:

qeditas.org/gitweb

[Trent Russell]

I've tried to compile your fork of Egal, but I can't even get started. I'm using Tails OS which doesn't have make. This means I can't compile using the usual configure, make, make install. (Tails OS doesn't have ocaml either, but I compiled ocaml for Tails earlier.) I could start Tails with the ability to sudo, install make, and then Egal might compile, but this is a time consuming process.

The original Egal included a bash script makebytecode that compiled the bytecode version without requiring make. I tried using this old script on your fork, but it doesn't work. First, the script expects there to be a bin directory, which is not in your Egal. This is easy enough to fix with mkdir bin. Then calling the script I got this:

Code:

365 states, 24874 transitions, table size 101686 bytes
File "src/mgcheck.ml", line 40, characters 0-23:
Error: Unbound module Axioms

At this point, I decided to give up and write this post. Can you include a script like the old makebytecode that can compile Egal without make?

[Bill White]

I've tried to compile your fork of Egal, but I can't even get started. I'm using Tails OS which doesn't have make. This means I can't compile using the usual configure, make, make install. (Tails OS doesn't have ocaml either, but I compiled ocaml for Tails earlier.) I could start Tails with the ability to sudo, install make, and then Egal might compile, but this is a time consuming process.

The original Egal included a bash script makebytecode that compiled the bytecode version without requiring make. I tried using this old script on your fork, but it doesn't work. First, the script expects there to be a bin directory, which is not in your Egal. This is easy enough to fix with mkdir bin. Then calling the script I got this:

Code:

365 states, 24874 transitions, table size 101686 bytes
File "src/mgcheck.ml", line 40, characters 0-23:
Error: Unbound module Axioms

At this point, I decided to give up and write this post. Can you include a script like the old makebytecode that can compile Egal without make?

Thank you for the feedback. I thought I had an empty bin directory in the repo, but I was wrong. This has been fixed. I also modified the old Egal's makebytecode script to work for the new Egal and added it. You should now be able to compile Egal using makebytecode as long as openssl, ocamllex and ocamlc are in your bash path.

[Trent Russell]

Thank you for the feedback. I thought I had an empty bin directory in the repo, but I was wrong. This has been fixed. I also modified the old Egal's makebytecode script to work for the new Egal and added it. You should now be able to compile Egal using makebytecode as long as openssl, ocamllex and ocamlc are in your bash path.

Just to confirm, the new makebytecode script does compile under Tails for me now.

[Bill White]

I added some ocaml code to the qeditas git repo:

git clone git://qeditas.org/qeditas.git

It includes code for type checking and proof checking, cryptography related code, and code for assets (including documents with definitions, proofs, etc.), transactions, compact trees (a form of Merkle tree for approximating the state) and blocks. There is still a significant amount to be done (consensus code, networking code, interface). However, it's probably best for the code so far to be public. This shows the project is progressing and gives people a chance to comment on the code or ask questions about it.

It can be compiled with configure and make or with the script makebytecode.

In some ways Qeditas has diverged from the Coq formalization (qeditastheory). After adding theories, it was unclear how to handle ownership of objects and propositions. Someone can claim ownership of a proposition after proving it, but it was unclear if this ownership should be specific to a theory or should be for all theories. Making it general seems to be wrong because some propositions are provable in some theories but not in others. As a simple example, consider excluded middle, i.e., the proposition (forall x:Prop, x or not x). On the other hand, making ownership specific to theories introduces the problem that someone could simply start a new theory with a minor difference from an existing theory and then copy and republish all the work done for the existing theory.

My decision for now is to have (potentially) separate owners for both the general version and the specific version. This means Alice can be the first to prove excluded middle in Theory A and become the owner of the general version as well as the specific version for Theory A. Later Bob could prove excluded middle in a different Theory B, but he could only claim ownership of the specific version for Theory B (since Alice already owns the general version). If someone wanted to import excluded middle (without a proof) in Theory A, Alice could require the purchase of two kinds of rights: general and specific. If someone wanted to import excluded middle (without a proof) in Theory B, Alice could require general rights and Bob could require specific rights.

Qeditas will support "bounties" on unproven propositions, but these should only be placed on the theory specific versions. If there is a bounty on a general proposition, then anyone can publish an inconsistent theory (e.g., the theory with one axiom: False), give a trivial proof of the proposition in that theory, and then claim the bounty. This restriction on bounties should be enforced at the protocol level, but it currently isn't.

The code for signing via endorsements is there (see signat.ml and script.ml). Endorsements are Bitcoin signed text messages of the form

Qeditas endorsement <Qeditas address>
endorse <Qeditas address>

People can use these to sell their initial distribution even before the Qeditas network is running. I will make a separate post about endorsements with details.

[Bill White]

I'm once again having trouble with github, so none of my repositories are visible at the moment. It's unfortunate since github is such a popular website for open source projects, but I suspect the best option is for me to stop using them. I will set up git on a server I control and find some way that people can still clone and pull the code from it. I will also need to go through my posts and remove the links to my github account.

In the meantime, it's still possible to clone my five repositories in their current state even without my account being visible. I have up to date copies already, but if anyone else wants them:

git clone https://github.com/billlwhite/cryptohash.git
git clone https://github.com/billlwhite/ledgertheory.git
git clone https://github.com/billlwhite/qeditastheory.git
git clone https://github.com/billlwhite/egal.git
git clone https://github.com/billlwhite/qeditas.git

It's unclear how much longer they'll be there. In any case, I won't be updating them on github anymore.

[sfultong]

Using bitbucket or another public git repo provider is probably more expedient. It's rather bizarre that you've experienced visibility issues with github.

[Bill White]

Using bitbucket or another public git repo provider is probably more expedient. It's rather bizarre that you've experienced visibility issues with github.

Thank you for the suggestion. I looked at bitbucket briefly the first time github made my account invisible, but at this point I'd just prefer to minimize my dependence on third parties.

The five git repos I had on github are now available to be cloned from qeditas.org:

Code:

git clone git://qeditas.org/qeditas.git
git clone git://qeditas.org/qeditastheory.git
git clone git://qeditas.org/cryptohash.git
git clone git://qeditas.org/ledgertheory.git
git clone git://qeditas.org/egal.git

They can also be viewed using gitweb here:

qeditas.org/gitweb

If someone wants to contribute, clone the relevant repo and then send me the information so that I can add your repo as a remote. Then let me know (here or PM or billwhite at bitmessage.ch) when you have pull requests.

[Bill White]

I added some (untested) consensus code. It's proof-of-stake with a bit of proof-of-storage. The code is in block.ml:

http://qeditas.org/gitweb/?p=qeditas.git;a=blob;f=src/block.ml;h=852f51b4c8cb1147970fc48ef40df54a62a20c51;hb=HEAD

Every block is signed by a staker who has a hit. The function check_hit determines if there's a hit. A hit is determined by hashing the assetid of the staker with the number of seconds since the last block ("deltatime") and a stake modifier. If there is no proof-of-storage element, there is a hit if the hash value is less than the target times the number of coins in the staked asset.

I was originally thinking of calculating the stake modifier like Blackcoin does (or at least the description of Blackcoin in the Neucoin white paper). In the end I did something a little simpler. It can be gamed a bit, but I think it's not enough to be dangerous. I prefer a transparent method of choosing the stake modifier to an obscure one.

For each block there is a 256-bit current stake modifier and a 256-bit future stake modifier. The current stake modifier is the one used to determine the current hit. The next stake modifier is obtained by dropping one bit, shifting all the bits, and adding a new bit popped from the future stake modifier. The person who stakes the block can freely choose one new bit to push onto the new future stake modifier. Note that this means the stake modifier for the next 256 blocks is always known.

The proof-of-storage component works as follows: If the staker includes a valid proof-of-storage, then the coins in the staked asset count for 25% more when calculating if there is a hit. A valid proof-of-storage is either an approximate term (tm) or an approximate document (pdoc). It should be such that everything is abbreviated by a hash except one leaf. When this leaf is hashed along with the hashroot of the tm/pdoc and the address of the staker, it should give a special kind of hash (1 chance in 65536). This can be used so that a staker can know in advance which proofs-of-storage are possible. In addition, the proof-of-storage should hash with the deltatime and stake modifier to give a value less than the current target times the modified stake with the extra 25%.

The main thing that remains is to write the networking code and to start testing.

When the real chain starts, it will need to be seeded with 512 bits for the current and future stake modifier. My plan is to announce a Bitcoin block height in advance. When a block of that height is mined (and not orphaned), then everyone can apply sha256 to the block hash to obtain 256 bits for the current stake modifier and then apply sha256 again for the future stake modifier. This is a way to ensure the initial 256 stake modifiers were not chosen maliciously.

I expect to do at least one test run before the real staking begins. I will announce any such test run here.

[Bill White]

Given the way stake modifiers are computed, it makes sense to insist that an asset is at least 512 blocks old (or from the initial distribution) before it can stake. Consequently, the first 512 blocks must be staked from the initial distribution. I was concerned that there wouldn't be enough actively staking assets to make it through this initial phase, but I've thought of a way to ensure it.

As I wrote in the white paper, Qeditas units will have 4 more decimal points of precision than Bitcoin. One satoshi in a Bitcoin address at the snapshot will correspond to 10,000 Cantors (cants) in the initial distribution for Qeditas. I had intended to distribute this as one asset per address, but instead I will split it over 100 assets. For example, if you had 1 satoshi in an address, then the corresponding Qeditas address will start with 100 assets worth 100 cants each. More realistically, if you had 0.1 bitcoins in an address, then the corresponding Qeditas address will start with 100 assets worth 0.001 fraenks (1 zerm) each.

This way even if someone only has one funded address, they will still be able to stake up to 100 times in the first 512 blocks. After the first 512 blocks, staking rewards will start to become eligible to stake.

[Bill White]

It's time for another update. I am currently testing and modifying the consensus code. The first tests made it clear that once the first block rewards mature (after 512 blocks) they stake far more often than the initial distribution. To avoid this, I'm including coinage. Coins mature after 512 blocks and then age linearly quadratically for 16384 blocks (approximately 16 weeks). The coins in the initial distribution start out as mature. (Otherwise, there would be no coins to stake for the first 512 blocks.) Since the initial distribution starts aging immediately and the first block rewards only start aging after 512 blocks, addresses with a reasonable balance in the initial distribution should continue having a chance to stake even after block rewards start maturing.

On another note, I added a "proof of forfeiture" component which is similar to the Slasher idea described in early 2014 by Vitalik Buterin:

https://blog.ethereum.org/2014/01/15/slasher-a-punitive-proof-of-stake-algorithm/

I hadn't intended to do this because I didn't see short term forks as a serious problem. However, I now think there is a potential problem. Suppose B0 is a block. Suppose Alice and Bob sign different successor blocks B1 and B1'. Other participants need to know whether to sign a successor to B1 or B1'. Using the current stake modifier, the same participant will have the power to sign a successor to B1, to B1', to neither, or to both. The economically rational decision is to sign two successors: B2 to B1 and B2' to B1'. The reason is that if the staker only signs one, there is a chance that his choice will be orphaned and he will lose the staking reward. This same argument is a reason for every participant to sign two (or more successors), leaving a future (economically irrational) staker to decide which fork will win.

In summary, I don't see a serious problem if some participants sign blocks on different branches, but I do see a serious problem if every participant signs blocks on different branches.

To counteract this, the signer of a block can include a "proof of forfeiture" in the block. Such a proof consists (more or less) of two block header chains (each of length <= 6) which prove there is a fork from a common point to two block headers signed using the same staker's address. If such a proof is included, the coinstake transaction is allowed to include as inputs any currency assets owned by the double signer which were created in the last 6 blocks. In essence, the double signer forfeits his stake rewards to the new signer who exposed the double signing.

What remains is to do more testing and to write the networking code.

[Bill White]

I wasn't happy with the testing results, so I modified how coins age. Coins now age quadratically: the coinage is essentially (floor(B/512))^2 where B is the number of blocks since the asset's creation. The maximum value for B is 16384 (about 16 weeks) at which point the coinage remains at the maximum coinage of 32^2 = 1024. There are two exceptions to this:

1. The initial distribution starts off with the maximum coinage.

2. Addresses can have assets that are "locked" until a certain block. Locked assets age twice as quickly, but then lose the ability to stake at all 32 blocks before they become spendable. (Such locks can be used to loan stake to a third party staker without losing the ability to spend the asset later.)

The exact details coinage are still open to being changed based on testing. The goal is to ensure that if no "bitcoin whales" are staking, then the first weeks of stake rewards do not overwhelm the staking ability of the initial distribution. In one of the latest tests, someone who had 0.025 bitcoins in the snapshot would've been able to stake block 3844 (roughly 26 days). In reality, this will depend on how much of the initial distribution is being staked during those first 26 days.

[Bill White]

The testing branch now contains some unit tests. Some of the unit tests failed which required debugging, so lots of the code has changed. Unit tests still need to be written for assets, transactions, ctrees, ctree grafts and blocks.

When I originally talked about signed endorsements I said they would have the form "endorse <Qeditas address>". However, in the first version of the code the message was expected to be "Qeditas endorsement <Qeditas address>". The "endorse <Qeditas>" format is simpler, so I changed the code to match it. I also edited a post in this thread from June which claimed the format would be the longer one.

Earlier there was some discussion of having a market for signed endorsements before the network starts running. This probably isn't a good idea. There would be nothing preventing someone from selling their endorsements multiple times.

[Bill White]

Quick update: I've finished writing unit tests for the assets module. These are committed in the testing branch. Unit tests for transactions, compact trees and blocks still need to be written. Also, the networking code still needs to be written.

[Bill White]

There are about 26 formal documents that were released with Egal, and obviously Qeditas should be able to process all of these (e.g., check the proofs). To ensure this, I added serializations of those Egal documents in files on the testing branch of Qeditas and added unit tests to check them. Fortunately, they all do check properly (though the code is slow). In the process it became clear that having one exception "CheckingFailure" was inadequate, and so now there are a number of new exceptions which make it clearer why checking fails.

[kushti]

Nice to see progress with the project!

From PoS algo description, it seems grinding  by deltatime is possible (like proposed for Neucoin: https://nxtforum.org/general-discussion/neucoin's-40-page-white-paper-rebuts-all-nothing-at-stake-objections/msg176475/#msg176475 ).

[Bill White]

Nice to see progress with the project!

From PoS algo description, it seems grinding  by deltatime is possible (like proposed for Neucoin: https://nxtforum.org/general-discussion/neucoin's-40-page-white-paper-rebuts-all-nothing-at-stake-objections/msg176475/#msg176475 ).

Thank you. Regarding grinding over the time stamp, the situation should become clearer once the first trial run starts. I can say two things at the moment. First, the term "grinding" suggests searching over a large space (thus becoming proof of work). A search space of 7200 (each second for the next 2 hours) wouldn't qualify as proof of work, in my opinion. Nevertheless, the real question is whether or not a staker could gain some advantage by using a time stamp in the future. It's not clear to me what the advantage would be, for the same reasons koubiac gave in the discussion at nxtforum.

(Edit, September 14, 2015: Reading the next paragraph again, it's misleading. Rather than rewrite it, I will write a separate post below.)

In the specific case of Qeditas, here's what I would expect to happen. Suppose Alice sees she can stake 3600s from now. She can create and sign a block with the corresponding future time stamp and publish it. Bob will see the time stamp is in the future. If Bob will be able to stake in less than 3600s, there is no reason for him to build on Alice's block. He can instead create his own block (closer to the current time) and publish it. Suppose Bob will be able to stake in 3700s from now. He could create a successor to Alice's block now and hope participants will continue to build on this chain. However, it seems more likely that someone other than Alice will be able to stake in less than 3600s from now. If that's the case, then someone, Carol, will publish a block with a more appropriate time stamp. Presumably people would build on Carol's block. If that's the case, Alice and Bob will have endangered their opportunities to stake 3600s and 3700s from now. The reason is that Qeditas allows a staker to forfeit the rewards of a recent staker who signed blocks on two branches. If Alice or Bob signed a block in the near future, a staker that follows could use their original published blocks to take their rewards.

In practice, we will have to see what happens.  Can you describe a scenario in which a staker can gain an advantage (stake more blocks?) by claiming a time stamp in the future?

[kushti]

Nice to see progress with the project!

From PoS algo description, it seems grinding  by deltatime is possible (like proposed for Neucoin: https://nxtforum.org/general-discussion/neucoin's-40-page-white-paper-rebuts-all-nothing-at-stake-objections/msg176475/#msg176475 ).

Thank you. Regarding grinding over the time stamp, the situation should become clearer once the first trial run starts. I can say two things at the moment. First, the term "grinding" suggests searching over a large space (thus becoming proof of work). A search space of 7200 (each second for the next 2 hours) wouldn't qualify as proof of work, in my opinion. Nevertheless, the real question is whether or not a staker could gain some advantage by using a time stamp in the future. It's not clear to me what the advantage would be, for the same reasons koubiac gave in the discussion at nxtforum.

In the specific case of Qeditas, here's what I would expect to happen. Suppose Alice sees she can stake 3600s from now. She can create and sign a block with the corresponding future time stamp and publish it. Bob will see the time stamp is in the future. If Bob will be able to stake in less than 3600s, there is no reason for him to build on Alice's block. He can instead create his own block (closer to the current time) and publish it. Suppose Bob will be able to stake in 3700s from now. He could create a successor to Alice's block now and hope participants will continue to build on this chain. However, it seems more likely that someone other than Alice will be able to stake in less than 3600s from now. If that's the case, then someone, Carol, will publish a block with a more appropriate time stamp. Presumably people would build on Carol's block. If that's the case, Alice and Bob will have endangered their opportunities to stake 3600s and 3700s from now. The reason is that Qeditas allows a staker to forfeit the rewards of a recent staker who signed blocks on two branches. If Alice or Bob signed a block in the near future, a staker that follows could use their original published blocks to take their rewards.

In practice, we will have to see what happens.  Can you describe a scenario in which a staker can gain an advantage (stake more blocks?) by claiming a time stamp in the future?

1. I'm naming any iteration over parameter space(allowed by a protocol) instead of using a parameter as planned as "grinding attack". Terminology isn't stable here still. It's interesting where is a line to split PoW/smallspace "grinding attacks", if we're going to a more precise terminology.

2. If every forger will follow Alice, so all the possible blocks for coming 2 hours will be published immediately. Also please note we're talking not about standard software implementation(where timestamping is honest), but some modified software, so forgers behaviour isn't predictable(a forger could extend any fork allowed by a protocol, or multiple of them in fact).

3. Alice have a chance to extend a chain immediately, and if longest chain rules that's about more blocks to produce. Maybe other blockchain quality functions are safe to that, I don't sure atm.

[Bill White]

In the specific case of Qeditas, here's what I would expect to happen. Suppose Alice sees she can stake 3600s from now. She can create and sign a block with the corresponding future time stamp and publish it. Bob will see the time stamp is in the future. If Bob will be able to stake in less than 3600s, there is no reason for him to build on Alice's block. He can instead create his own block (closer to the current time) and publish it. Suppose Bob will be able to stake in 3700s from now. He could create a successor to Alice's block now and hope participants will continue to build on this chain. However, it seems more likely that someone other than Alice will be able to stake in less than 3600s from now. If that's the case, then someone, Carol, will publish a block with a more appropriate time stamp. Presumably people would build on Carol's block. If that's the case, Alice and Bob will have endangered their opportunities to stake 3600s and 3700s from now. The reason is that Qeditas allows a staker to forfeit the rewards of a recent staker who signed blocks on two branches. If Alice or Bob signed a block in the near future, a staker that follows could use their original published blocks to take their rewards.

In practice, we will have to see what happens.  Can you describe a scenario in which a staker can gain an advantage (stake more blocks?) by claiming a time stamp in the future?

1. I'm naming any iteration over parameter space(allowed by a protocol) instead of using a parameter as planned as "grinding attack". Terminology isn't stable here still. It's interesting where is a line to split PoW/smallspace "grinding attacks", if we're going to a more precise terminology.

2. If every forger will follow Alice, so all the possible blocks for coming 2 hours will be published immediately. Also please note we're talking not about standard software implementation(where timestamping is honest), but some modified software, so forgers behaviour isn't predictable(a forger could extend any fork allowed by a protocol, or multiple of them in fact).

3. Alice have a chance to extend a chain immediately, and if longest chain rules that's about more blocks to produce. Maybe other blockchain quality functions are safe to that, I don't sure atm.

After rereading the paragraph I wrote describing what I would expect to happen with Qeditas, I realized that I had forgotten some details about how proof of stake in Qeditas has been implemented.  I implied that if Alice sees she can stake 3600s from now, she can either sign a block now with a future time stamp or wait for an hour and sign a block then. This was wrong. Alice's ability to stake in 3600s depends on the current stake modifier which changes with each block. She (along with everyone else) will know in advance what the current stake modifier will be for the next 256 blocks (roughly the next 2 days), so she can still precompute whether or not she will get the chance to stake in the next few hours whether she signs a block with a false future time stamp now or not. If she will get another chance to sign a block, then signing one that is likely to be orphaned now will risk her chance to stake in the near future (due to forfeiture of recent rewards for proven double signers). On the other hand, if her chance to stake "now" with a false future time stamp will be her only chance to stake in the near future (the next hour or so), then it is rational for her to sign a block with the false future time stamp and publish it. It would still be up to others whether or not to build on her block. Obviously if other participants also had the chance to stake with the current stake modifier within the next hour, then they would be inclined to publish their own blocks with a more accurate time stamp. Adding the block with the earliest time stamp should lead to the chain with the most cumulative stake.

Regarding grinding, I have been more concerned about possible grinding attacks on the future stake modifier. I've designed the code that each time someone stakes a block they can choose 1 bit that will be part of the stake modifiers 257 - 512 blocks in the future. In principle, a staker could explore some subset of some of the possible stake modifiers in the future in order to determine whether its advantagous for him to choose a 0 or a 1. Optimally, everyone would choose the bit randomly, but it's unrealistic to expect this. I expect people will learn that sometimes they can precompute if a 0 or a 1 is likely to help them stake at some point roughly 2 days in the future and choose that bit selfishly. I also expect that most of the time neither bit will be obviously preferable and so the choice will effectively be random. As long as the new bit is chosen randomly often enough, it should prevent a large staker from taking over the network (i.e., staking every block). As always, however, this is an experiment for which we don't yet know the results.

[sfultong]

Hi Bill,

I notice you haven't pushed any changes to the git repos recently. How are things coming?

Briefly looking through your code, it doesn't seem like you have worked on creating the ledger snapshot from bitcoin. That's actually what I'm going to be working on right now, with my bitcoin spinoff toolkit.

I was tempted to write the spinoff toolkit in ocaml (I much prefer it to C++) and maybe submit a pull request to you, but ultimately I wanted something that was easy to integrate with existing cryptocurrency codebases and something that more of the general public could contribute to. Of course, in reality, I'm unlikely to get contributions either way.

Well, I hope things are going well for you. Qeditas seems like a very exciting and daunting project.

[Bill White]

Hi Bill,

I notice you haven't pushed any changes to the git repos recently. How are things coming?

Briefly looking through your code, it doesn't seem like you have worked on creating the ledger snapshot from bitcoin. That's actually what I'm going to be working on right now, with my bitcoin spinoff toolkit.

I was tempted to write the spinoff toolkit in ocaml (I much prefer it to C++) and maybe submit a pull request to you, but ultimately I wanted something that was easy to integrate with existing cryptocurrency codebases and something that more of the general public could contribute to. Of course, in reality, I'm unlikely to get contributions either way.

Well, I hope things are going well for you. Qeditas seems like a very exciting and daunting project.

The Qeditas code is in progress, but still unfinished. I decided to push my most recent commits to the remote repository this morning. Coincidentally, the thing I've been doing the past few days is creating the initial ledger (as a compact/Merkle tree) from the snapshot I made of the Bitcoin block chain last March.

You're correct that code to create a snapshot is not in any of the git repositories. I did write some ocaml code to do this (in cooperation with bitcoind) but most of the code is a mess. For example, there are references to specific directories and filenames where I saved intermediate results. It took roughly 6 weeks (from mid-February to the end of March of this year) to successfully construct the snapshot I wanted (through the first 350,000 blocks). The end result of the snapshot is here:

https://mega.co.nz/#F!0xhzUbTS!h-LeyiTbF9dXgusKCc_bfQ

It's split into p2pkh balances and p2sh balances. In each case the address is given as the important 20 bytes in hex and then the balance of satoshis at the snapshot. There are also two small python scripts people can use to check their balances by giving the corresponding Bitcoin address. Once I had the snapshot I wanted to move on to coding Qeditas itself, so I never spent more time with the code to generate the snapshot.

The biggest problem I faced were resource bounds. What I would try to do would either require more RAM than I had, too much disk space or too much time. I spent most of my time modifying my strategy to compute the snapshot to work around these bounds. A more reasonable strategy probably would have been to buy more advanced hardware. Here are a few things I can say that might be helpful:

1. The blocks are all stored in .bitcoin/blocks/*.dat files and one can read the relevant data from there without needing bitcoind (now bitcoin-cli I suppose). However, it is dangerous. The files include orphan blocks. I'm also unsure whether the blocks are guaranteed to be in the correct order. After realizing this, I used bitcoind with getblockhash to explicitly give me the hash of each of the 350,000 blocks in the main chain. At this point it's possible to use the *.dat files to read blocks, skipping orphans, or it's possible to use bitcoind getblock with each of these hashes. I tried both, and am no longer sure which variant was used to make the final snapshot.

2. I went through all the txs in the main chain and computed that only the first 7 bytes of the 32 byte hash is needed to uniquely identify the tx. There are two exceptions of txs for which there are 'twin' txs with the same txid (since the txs look exactly the same):

d5d27987d2a3dfc724e359870c6644b40e497bdc0589a033220fe15429d88599
e3bf3d07d4b0375638d5f1db5255fe07ba2c4cb067cd81b84ee974b6585fb468

These were due to bugs in bitcoin having to do with ignored coinbase inputs. I chose to ignore the duplicate and only count each tx once. My understanding is that in bitcoin the relevant txos can only be spent once in spite of being in the block chain twice.

The important point is that it was sufficient to only use 7 bytes to identify txs instead of 32. Since there have been many txs since the end of March, it's possible 7 bytes is no longer enough.

3. My first attempt to create a snapshot was to go forward through the blocks and store all utxos until they were spent. In principle, at the end I would have had all the utxos and hence the snapshot. This ran out of memory. As a workaround, I tried reading a certain number of blocks and then saving the state (utxos so far) and then restarting. This still wasn't good enough. Then I tried saving all the txs in reverse order. I kept in memory all the spent txos that I had not yet seen created. Each time I encountered a new txo, it was either known to be spent in the future or I would know it should go into the snapshot. This also ran out of memory. At this point, I would have to carefully review my notes to see what exactly I did, but it's at least clear that I saved some very large files named "spentxxx" and "unspentxxx" where xxx ranged from 000 to roughly 250 -- mirroring the names of the block*.dat files. I do roughly remember that I created some of these files by processing the blocks forward and the other files by processing the blocks backward, and extracting the snapshot from a combination of the information.

I hope you can find a more robust solution. Creating a snapshot was a surprisingly difficult hurdle for creating a spinoff.

[sfultong]

Thanks Bill, that's very helpful.

Did you filter out dust?

[Bill White]

I didn't filter out dust. It's a reasonable thing to do. I just checked and roughly 9.5% of addresses in the snapshot have 1 satoshi.

I'm changing the units in Qeditas to have 4 extra decimal places, so those addresses will start with 10,000 cants (the atomic currency unit of Qeditas). It's obviously still dust though.

[rendravolt]

Thanks dev, this is what I need. 

[Zombier0]

Clams did it befor but i see n reason why u cannot also

[Trent Russell]

Clams did it befor but i see n reason why u cannot also

I'm a fan of Clams, but I don't think it's considered a "spin-off" of Bitcoin. They did distribute partially using a snapshot of funded Bitcoin addresses, but the amount each address got was the same -- it wasn't proportional to the number of bitcoins there.

As far as I know, there really hasn't been a "spin-off" of Bitcoin yet. Qeditas might be the first real "spin-off"...if...well, let me just ask. Any new ETA for Qeditas?

[Bill White]

Any new ETA for Qeditas?

At the moment I'm writing networking code. Once this code seems to be working, everyone interested can start running  nodes in a testing phase. During that phase we'll stake and start building a block chain, but it won't count. It's likely that there will be problems and the test will need to be reset and restarted a few times. (By "reset" I mean we will start from the snapshot distribution ledger each time. Rewards from staking during the testing phase will be forgotten.) Once things seem to work well for a week, I'll announce that the network will start for real about a week in advance. My intention is to say the network will start when Bitcoin reaches a certain block height divisible by 1000 (e.g., 384000). The hash of that Bitcoin block will be used to initialize the Qeditas stake modifier and at that moment we can all begin staking and building the real Qeditas block chain.

As for a specific ETA, the earliest possible time that the Qeditas network could start running for real is in two or three weeks. It's more realistic to think it will start sometime in December. I've been trying to avoid giving estimates until a test version is ready. Each task has taken much longer than I expected.

In the meantime, I'd encourage anyone who might want to participate in the testing phase to check out the git repository and see if the unittests pass for you. The unit tests are in the testing branch.

git clone git://qeditas.org/qeditas.git
git checkout testing
./configure
make
./bin/unittests

The code is written to run in linux. It might work with Mac OS. I would be very surprised if it were to compile and run under Windows.

I want the code to work with the Tails Live OS. This is an OS everyone on a desktop should be able to run without needing to install it. Tails doesn't have developer tools like make or ocaml. I can supply a version of ocaml that works and then a bytecode version of Qeditas can be compiled and run with Tails. The script "makebytecode" is included for this purpose.

More specific instructions will follow when the code is ready to try a test network.

[Zombier0]

Clams did it befor but i see n reason why u cannot also

I'm a fan of Clams, but I don't think it's considered a "spin-off" of Bitcoin. They did distribute partially using a snapshot of funded Bitcoin addresses, but the amount each address got was the same -- it wasn't proportional to the number of bitcoins there.

As far as I know, there really hasn't been a "spin-off" of Bitcoin yet. Qeditas might be the first real "spin-off"...if...well, let me just ask. Any new ETA for Qeditas?

Oh so this will send me as many of 'new coin' as i have BTCs?

[Trent Russell]

Clams did it befor but i see n reason why u cannot also

I'm a fan of Clams, but I don't think it's considered a "spin-off" of Bitcoin. They did distribute partially using a snapshot of funded Bitcoin addresses, but the amount each address got was the same -- it wasn't proportional to the number of bitcoins there.

As far as I know, there really hasn't been a "spin-off" of Bitcoin yet. Qeditas might be the first real "spin-off"...if...well, let me just ask. Any new ETA for Qeditas?

Oh so this will send me as many of 'new coin' as i have BTCs?

Yes, at least according the OP. Actually, the snapshot was already taken (at block 350000), so you should already know how much of the initial distribution you have. The OP linked to this mega folder with the snapshot:

https://mega.nz/#F!0xhzUbTS!h-LeyiTbF9dXgusKCc_bfQ

It's 208MB. While writing this reply I decided to download it and check some of my addresses, and it seems to be correct for me (for when the snapshot was taken):

Code:

./checkp2pkh 1FtRzWPDwi8ygSzu6S9GQMb1mP4v1TTmTH
a34bd63d3f9403b8ae55e63b91344d094623b7ce:46311490

./checkp2pkh 1874LQvnDWbLjLoaSfEnq3RpkPtidAEshN
4dee28f0c1f2c7556593593083aafc1d0f38178e:25000000

My addresses 1FtRzWPDwi8ygSzu6S9GQMb1mP4v1TTmTH and 1874LQvnDWbLjLoaSfEnq3RpkPtidAEshN did have 0.46311490 btc (46311490 satoshis) and 0.25 btc (25000000 satoshis) at block 350000.

(Note: I had to make the python script checkp2pkh executable for checking the snapshot addresses to work.)

[Bill White]

Oh so this will send me as many of 'new coin' as i have BTCs?

You have precisely as many Qeditas "fraenks" as you had btc in each address after the first 350,000 Bitcoin blocks (found at a certain time on March 30, 2015). One of the original purposes of this preannouncement thread was to give people advance notice that I would be taking the snapshot, in case anyone wanted to withdraw some bitcoins from exchanges or other third-party services.

The term "fraenks" is short for Fraenkel, an important figure in the foundations of mathematics. As set out in the white paper (http://qeditas.org/qeditas.pdf) there will be four more decimal places for the Qeditas monetary units. I've named each multiple of a thousand using the name of a different figure who contributed to the foundations of mathematics.

Basic Unit: cant (Cantor). If you had 1 satoshi in a Bitcoin address, then you have 10,000 cants in the corresponding  Qeditas address.
https://en.wikipedia.org/wiki/Georg_Cantor

1000 cants = 1 freg (Frege).
https://en.wikipedia.org/wiki/Gottlob_Frege

1000 fregs = 1 church (Church). If you had 1 microbit ("bit") in a Bitcoin address, then you have 1 church in the corresponding Qeditas address.
https://en.wikipedia.org/wiki/Alonzo_Church

1000 churches = 1 zerm (Zermelo). If you had 1 millibit in a Bitcoin address, then you have 1 zerm in the corresponding Qeditas address.
https://en.wikipedia.org/wiki/Ernst_Zermelo

1000 zerms = 1 fraenk (Fraenkel). If you had 1 bitcoin in a Bitcoin address, then you have 1 fraenk in the corresponding Qeditas address.
https://en.wikipedia.org/wiki/Abraham_Fraenkel

1000 fraenks = 1 groth (Grothendieck).
https://en.wikipedia.org/wiki/Alexander_Grothendieck

Most of these are historical figures. Grothendieck just died late last year.

Yes, at least according the OP. Actually, the snapshot was already taken (at block 350000), so you should already know how much of the initial distribution you have. The OP linked to this mega folder with the snapshot:

https://mega.nz/#F!0xhzUbTS!h-LeyiTbF9dXgusKCc_bfQ

It's 208MB. While writing this reply I decided to download it and check some of my addresses, and it seems to be correct for me (for when the snapshot was taken):

Code:

./checkp2pkh 1FtRzWPDwi8ygSzu6S9GQMb1mP4v1TTmTH
a34bd63d3f9403b8ae55e63b91344d094623b7ce:46311490

./checkp2pkh 1874LQvnDWbLjLoaSfEnq3RpkPtidAEshN
4dee28f0c1f2c7556593593083aafc1d0f38178e:25000000

My addresses 1FtRzWPDwi8ygSzu6S9GQMb1mP4v1TTmTH and 1874LQvnDWbLjLoaSfEnq3RpkPtidAEshN did have 0.46311490 btc (46311490 satoshis) and 0.25 btc (25000000 satoshis) at block 350000.

(Note: I had to make the python script checkp2pkh executable for checking the snapshot addresses to work.)

Thanks for checking and confirming. I'm surprised the python scripts aren't executable. I suppose it's easy enough for people who want to check to do "chmod u+x check*" before using them. By the way, the hex you see before the number of satoshis at the address represents the important 20 bytes of the address. These 20 bytes determine where the corresponding asset in the compact tree for the initial distribution is. It is also the asset id of the corresponding asset. An "asset id" in Qeditas is like the pair (txid,vout) in Bitcoin, in that it uniquely identifies something which can be "spent" by a transaction.

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

i still think using Coq is would be the more practical choice if you want people to use the system. But there is evidence for what you say. i have just read on the coq-club mailing list in response to vm_compute being part of the trusted kernel of Coq:

The actual implementation of vm_compute is not formally verified, though, and, yes, it is part of the trusted kernel. Empirically, based on the rate of discovery of proofs of False, it looks as reliable as the rest of the Coq implementation.

lol

good to see progress on qeditas. good luck.

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

i still think using Coq is would be the more practical choice if you want people to use the system. But there is evidence for what you say. i have just read on the coq-club mailing list in response to vm_compute being part of the trusted kernel of Coq:

The actual implementation of vm_compute is not formally verified, though, and, yes, it is part of the trusted kernel. Empirically, based on the rate of discovery of proofs of False, it looks as reliable as the rest of the Coq implementation.

lol

good to see progress on qeditas. good luck.

It would probably be impossible to use Coq directly in its current stage of development. Actually, in some ways Qeditas has changed (with the addition of theories) over the past months to be closer to Isabelle: simple type theory + primitives and axioms, except proof terms are vital in Qeditas where Isabelle follows the LCF approach.

In the end, though, Qeditas is really occupying a different space than theorem provers like Coq or Isabelle. Qeditas is like a large library with a careful indexing system for the contents of the books in the library. Theorem provers like Coq and Isabelle are more like the producers of the books for the library. It would not surprise me if eventually most of the content published in Qeditas were created using provers like Coq and Isabelle.

[kushti]

Dear Bill,

Thanks for detailed explanation of PoS in the Qeditas system. I need to go through source code now.

I did look through project source code yesterday. Initial thoughts: comments are needed sometimes, it's better to split unittests into separate files(few K LOCs single file isn't a convenient choice in a long-term), some reports with aggregation on tests running results would be a boon.

So on next weekend I would like to contribute a bit, with unittests probably and maybe play with properties tests as well. As I see other possible contributors in the topic, let's collaborate. We need for some issue tracking as well from some point as well.

[Bill White]

Dear Bill,

Thanks for detailed explanation of PoS in the Qeditas system. I need to go through source code now.

I did look through project source code yesterday. Initial thoughts: comments are needed sometimes, it's better to split unittests into separate files(few K LOCs single file isn't a convenient choice in a long-term), some reports with aggregation on tests running results would be a boon.

So on next weekend I would like to contribute a bit, with unittests probably and maybe play with properties tests as well. As I see other possible contributors in the topic, let's collaborate. We need for some issue tracking as well from some point as well.

Thank you for the feedback. I certainly agree that more comments are needed. In general documentation would be very helpful. It's difficult to force myself to write documentation while in coding mode. Hopefully after a testnet is running I can spend some time adding comments and documentation. In the meantime, if you have questions about some specific functions or files, I can try to answer here.

Yes, the unittests.ml file (in the testing branch) got out of hand, especially once I began adding code to test the functions in Ctre. I'm putting splitting it into separate files on my "to do" list.

Of course, I will be happy if you or others want to contribute code, comments, or questions. Do you have a clone of qeditas.git that I could add as a remote? If so, I could pull from it and merge in your contributions. It might also make sense if I put a public key for you on the git server giving you commit access, but I should probably give some thought to the process of giving people commit access first.

Regarding "issue tracking" -- do you have a suggestion for how we could do this? I suppose it's usually done through github. Is there some standard software I could run on qeditas.org for this purpose? Alternatively, is there a (privacy respecting) third party site that could be used for this?

[kushti]

Hi Bill! I hope you're doing well!

1. I'm a newbie in OCaml so it's better not to give me a right to commit  and review all the changes from me

2. Github is most popular option for issues/features/roadmap tracking these days probably. But if you have problems with it, we can try BitBucket or GitLab, both are pretty good(especially the latter imho). We can use one of many project management tools as well.

3. I can add some comments if you wish so

[Bill White]

Hi Bill! I hope you're doing well!

1. I'm a newbie in OCaml so it's better not to give me a right to commit  and review all the changes from me

2. Github is most popular option for issues/features/roadmap tracking these days probably. But if you have problems with it, we can try BitBucket or GitLab, both are pretty good(especially the latter imho). We can use one of many project management tools as well.

3. I can add some comments if you wish so

Thank you for the suggestions. GitLab looks reasonable since I can (in principle) run it on my server. I'm not opposed to you (or someone else) cloning the git repository and putting it on github. As you probably remember (but I'll repeat it for those who are new to the thread) I originally had qeditas on github. At some point they hid my repositories and said I needed to contact them to unhide it. I did contact them. They made the repositories visible and said it shouldn't happen again. When it did happen again within a few weeks, I decided it was best to no longer rely upon them. That's why the git repos are now on qeditas.org. I cancelled my github account.

Nevertheless, I am not opposed to github being used as long as I do not need an account there. If you put a clone of the repo on github, I will add it as a remote. (I don't think I need an github account to do add a github repo as a remote, but I also haven't tried yet. My guess is that I would only need an account to push to the github repo.) If that works, I should be able to pull and merge your changes. This is a possible way you could add some comments and have them included in the repo on qeditas.org.

[Bill White]

I've mentioned in earlier posts that it will be possible for people to claim ("spend") part of the initial distribution using Bitcoin signed "endorsements". I've decide (and updated the code) to also allow staking to be done this way as well -- for the special case of a p2pkh Bitcoin address endorsing a p2pkh Qeditas address.

Originally I intended such "endorsements" to make it easier for Bitcoin holders to sell their part of the distribution by simply signing a message ("endorse <Buyer's Qeditas address>"). Now it's clear to me that everyone may want to claim their part of the distribution using endorsements, since it never requires giving the corresponding Bitcoin private key to the Qeditas software.

I'll have a separate format for testnet endorsements so we can experiment without signing an endorsement that will be valid on the mainnet. For now, that format will be

"testnet:endorse <Qeditas address>"

It's possible that at some point we will want to start the testnet over from scratch and switch to "testnet2:endorse ..." or "testnet3:endorse ..." Obvously such endorsements are intended for testing and will not work on the mainnet. As with all testnets, they should have no monetary value.

Here's a concrete example. I recently started a fresh bitcoind and it generated a wallet with the fresh bitcoin address 1EMyzMEGdjR9QxGXhqN4ZrgtkuVauQRCt. I took the private key (which I'll indicate here by) Lprivatekey and imported it into my Qeditas wallet.

Code:

qeditascli importbtcprivkey Lprivatekey

This also informed me of the corresponding Qeditas (p2pkh) address: QLqM6HdwT6cEaZ3Hx39rBqeKQ1rCpfwcSH

There are no Qeditas assets at this address, of course, just as there have never been bitcoins at 1EMyzMEGdjR9QxGXhqN4ZrgtkuVauQRCt.

However, one of the Bitcoin addresses I do control that had funds in the snapshot is 1LdCQAdQaxT6SjrZhSSKizCtBJBxsTg5z9. Using bitcoind with a wallet that had the private key for this address, I signed the message "testnet:endorse QLqM6HdwT6cEaZ3Hx39rBqeKQ1rCpfwcSH". The signature of the message was:

G2mbgyCbv3rcdkvltUbYiOEwYlobc9XOTbtcQJaUoKZyeejvDkz98+Jft+v1HQlTCZi/bMRnCgYwOADf3uGUBhQ=

(You can verify with a Bitcoin client that the signature matches the message above signed by the address above.)

The Qeditas address corresponding to 1LdCQAdQaxT6SjrZhSSKizCtBJBxsTg5z9 is QgEBWTv7mRKusswb7mkorFzWgZ8g7u5vMS. Since the Bitcoin address had 20,000 satoshis (0.0002 bitcoins) at the snapshot, the Qeditas address has 200,000,000 cants (0.0002 fraenks) in the initial distribution.

I imported this endorsement into my Qeditas wallet:

Code:

qeditascli importendorsement QgEBWTv7mRKusswb7mkorFzWgZ8g7u5vMS QLqM6HdwT6cEaZ3Hx39rBqeKQ1rCpfwcSH G2mbgyCbv3rcdkvltUbYiOEwYlobc9XOTbtcQJaUoKZyeejvDkz98+Jft+v1HQlTCZi/bMRnCgYwOADf3uGUBhQ=

The Qeditas wallet now has enough information to sign txs spending the funds at QgEBWTv7mRKusswb7mkorFzWgZ8g7u5vMS, or staking funds held at the address.

It seemed to be a good idea to take the time to explain this in a post now before the testnet begins running. I have some hope that a testnet may be running in the next few days. The code is incredibly slow, so don't expect too much in terms of performance. I also expect there will be bugs and the testnet will need to be restarted multiple times.

If you want to prepare a Qeditas wallet for participating in the testnet, you can do the following (assuming you're on linux and have ocaml):

Code:

git clone git://qeditas.org/qeditas.git
mkdir ~/.qeditas
cd qeditas
git checkout dev
./configure
make

If all went well, you'll have executables "qeditascli", "qeditasd" and "qeditasstk" in the qeditas/bin dir. For simplicity, I'll assume this directory is on your PATH.

You should create a qeditas.conf file in ~/.qeditas saying you're using testnet, you're staking and optionally giving your ip if you're listening for peers. Here's how mine looks:

Code:

staking=1
testnet=1
ip=108.61.219.125

Generate a fresh bitcoin address with its private key (in WIF format). Then you can use qeditascli to import this private key as indicated above. This will tell you the corresponding Qeditas address. You can then sign a testnet endorsement (using Bitcoin) and import the endorsement (using qeditascli) as I did above.

If someone wants to take part in the testnet, but did not have bitcoins at the time of the snapshot (March 30, 2015), I can sign 10 or so testnet endorsements. (Again, these will only be useful on the testnet, not on the mainnet later.) To do so, do the steps above until you need to sign the endorsement. At that point post the address Qeditas gave you when you used importbtcprivkey. I can then post a signed testnet endorsement that you'll be able to import into your Qeditas wallet.

By the way, if you do all that, you're welcome to try to run qeditasd. It will try to connect to my node, if my node is running. Since I keep restarting it for testing, you will just need to be lucky to connect. Also, at the moment you won't really be able to stake or even verify that your Qeditas funds are in the initial ledger.

[Trent Russell]

I'm trying this out, but having some trouble. First, with the endorsements, I do have some bitcoin addresses that had a balance in the snapshot. For example, 1FtRzWPDwi8ygSzu6S9GQMb1mP4v1TTmTH. I can sign a message like you suggested, but then to use importendorsement I need to give the Qeditas address that corresponds to 1FtRzWPDwi8ygSzu6S9GQMb1mP4v1TTmTH. Where do I get this?

Having "qeditascli help" might be useful.

I also tried out qeditasd and got some confusing output:

Code:

Initializing random seed
Listening for incoming connections.
about to start staker
started staker
Could not determine a starting point for staking. Not staking.
Pausing staking since found hit
Added connection; post handshake
my time = 1444985716
their time = 1444985716
addr_recv2 = 108.61.219.125:20804
addr_from2 = 108.61.219.125:20804
Handshake failed. (No Verack)

It seems to say it starts the staker, can't determine a "starting point" (?) and decides not to stake. And then it says it's pausing the staking "since found hit". If it wasn't staking how did it find a hit?

Then it says it's adding a connection and says it's "post handshake". After that it says "Handshake failed." How can the handshake fail if it's "post handshake"?

[Bill White]

I'm trying this out, but having some trouble. First, with the endorsements, I do have some bitcoin addresses that had a balance in the snapshot. For example, 1FtRzWPDwi8ygSzu6S9GQMb1mP4v1TTmTH. I can sign a message like you suggested, but then to use importendorsement I need to give the Qeditas address that corresponds to 1FtRzWPDwi8ygSzu6S9GQMb1mP4v1TTmTH. Where do I get this?

Having "qeditascli help" might be useful.

I also tried out qeditasd and got some confusing output:

Code:

Initializing random seed
Listening for incoming connections.
about to start staker
started staker
Could not determine a starting point for staking. Not staking.
Pausing staking since found hit
Added connection; post handshake
my time = 1444985716
their time = 1444985716
addr_recv2 = 108.61.219.125:20804
addr_from2 = 108.61.219.125:20804
Handshake failed. (No Verack)

It seems to say it starts the staker, can't determine a "starting point" (?) and decides not to stake. And then it says it's pausing the staking "since found hit". If it wasn't staking how did it find a hit?

Then it says it's adding a connection and says it's "post handshake". After that it says "Handshake failed." How can the handshake fail if it's "post handshake"?

Thank you for the feedback. Regarding the question about addresses, you can use "btctoqedaddr" to obtain the Qeditas address corresponding to a Bitcoin address. Example:

Code:

qeditascli btctoqedaddr 1FtRzWPDwi8ygSzu6S9GQMb1mP4v1TTmTH
Qeditas address QbVR6ofw8B1o7b5vWmTkXdNeGe1dHEYRf9 corresponds to Bitcoin address 1FtRzWPDwi8ygSzu6S9GQMb1mP4v1TTmTH

I will need to look more closely into the other issues.

[Bill White]

Having "qeditascli help" might be useful.

There is now such a help command.

I also tried out qeditasd and got some confusing output:

Code:

Initializing random seed
Listening for incoming connections.
about to start staker
started staker
Could not determine a starting point for staking. Not staking.
Pausing staking since found hit
Added connection; post handshake
my time = 1444985716
their time = 1444985716
addr_recv2 = 108.61.219.125:20804
addr_from2 = 108.61.219.125:20804
Handshake failed. (No Verack)

It seems to say it starts the staker, can't determine a "starting point" (?) and decides not to stake. And then it says it's pausing the staking "since found hit". If it wasn't staking how did it find a hit?

Then it says it's adding a connection and says it's "post handshake". After that it says "Handshake failed." How can the handshake fail if it's "post handshake"?

The fact that the staker can't determine a starting point is likely because you don't have the initial ledger. The data for the initial ledger is roughly 200MB in a special format. I will likely provide a download when it's more certain the format won't change. Nodes shouldn't need the full ledger though. Instead Qeditas nodes should be able to request the part of the ledger they need. The code for making such requests is partially written, but not yet functional.

I'm not sure about the "post handshake"/"Handshake failed" issue, but I suspect these were referring to two different connections. I added a new IP address for a "fallback" node and your node may have successfully connected to one (resulting in the "post handshake" information) but failed to connect to the other.

I've been making significant changes to the way nodes initially connect, so things are unstable at the moment.

[sfultong]

hi Bill,

What is the method you're using for allowing people to claim p2sh amounts? This has been a bit of a headache for me, and I think I've finally settled on having them submit the hex string of a transaction that would transfer the funds in bitcoin proper, along with the p2sh address and the input index for the transaction. I can probably assume there will be one input and hardcode that index to 0.

[Bill White]

hi Bill,

What is the method you're using for allowing people to claim p2sh amounts? This has been a bit of a headache for me, and I think I've finally settled on having them submit the hex string of a transaction that would transfer the funds in bitcoin proper, along with the p2sh address and the input index for the transaction. I can probably assume there will be one input and hardcode that index to 0.

The short answer is that each p2sh will start with a currency asset equal to its snapshot balance. In order to spend this asset in a Qeditas tx, a generalized signature is required. One example of such a generalized signature is a Bitcoin script that evaluates to true (where OP_CHECKSIG and OP_MULTISIG occurrences in the script are checked against a hash of the Qeditas tx). There are also other alternatives using endorsements, but all of the alternatives require giving an appropriate script. I have not written code to help users create such a script, but may in time.

Here are a few more details. (Even if it is more information than you want, it may be helpful for people in the future.)

I wrote an interpreter for Bitcoin's script language that will be part of Qeditas. (Actually, I've omitted OP_RIPEMD160 and OP_SHA1.)

http://qeditas.org/gitweb/?p=qeditas.git;a=blob;f=src/script.mli;h=32b2947e65f53db89fae62749bb0307d3f677151;hb=fe9271b8e7fee04b253dc5611ca500784772dfdd
http://qeditas.org/gitweb/?p=qeditas.git;a=blob;f=src/script.ml;h=6903b03aa62ad2bd39efb002f66d731b299b057b;hb=fe9271b8e7fee04b253dc5611ca500784772dfdd

In the interface file above (script.mli) there is a datatype "gensignat". This is for generalized signatures. The first two cases cover ordinary p2pkh and p2sh signatures. (The other cases are for signatures via endorsements.) These generalized signatures are checked using verify_gensignat. In the special case of a p2sh signature, a function verify_p2sh is called. (The function verify_p2sh is also exposed in the script.mli interface file.)

A "p2sh" signature here is simply a list of integers, which should be a list of bytes. This list of bytes is the script.

To see the code that really interprets a script, look at eval_script and eval_script_if. Handling OP_IF is tricky.

[sfultong]

Hi Bill,

I've posted the results of my snapshot creation code, compared to your snapshot, over in the spinoff thread. There seem to only be minor disagreements.

Next I'll compare our P2SH results, which should be pretty quick now I've got everything set up. I converted all non-standard pubkey scripts in utxos to p2sh form. I'm guessing you did the same.

[Bill White]

Hi Bill,

I've posted the results of my snapshot creation code, compared to your snapshot, over in the spinoff thread. There seem to only be minor disagreements.

Next I'll compare our P2SH results, which should be pretty quick now I've got everything set up. I converted all non-standard pubkey scripts in utxos to p2sh form. I'm guessing you did the same.

It's good to hear the snapshots mostly agree. I have started to look into why they disagree, and will post more details on the spin-offs thread. Some of the disagreements are corner cases (like the genesis block reward). However, it definitely seems like there are some balances in my snapshot that are wrong, and I will resolve this before launching Qeditas.

[Bill White]

A Qeditas update is overdue. A working testnet is still out of reach for now. I've shifted focus to cleanup and documentation for the time being.

In the dev branch I created a subdirectory doc/techdoc. There are tex files there in which the code can be documented and explained. Very little is there so far, but feel free to add documentation or just add questions and requests for documentation in the tex code. Here's how to create a pdf from the sources:

Code:

latex qeditastechdoc
bibtex qeditastechdoc
makeindex qeditastechdoc
latex qeditastechdoc
latex qeditastechdoc
dvipdf qeditastechdoc

Here is a link to the current pdf version, which I will attempt to keep up to date: qeditas.org/qeditastechdoc.pdf

Also, Kushti made the suggestion that the unittests code be factored, and I've done this to some degree.

[Bill White]

Significantly more content has been added to the technical documentation, but most of it is still a skeleton.

http://qeditas.org/qeditastechdoc.pdf

The current focus is Chapter 6 describing the mathdata code. This is where terms and proofs are defined, and where the proof checking code is. If there is a bug in this code, it could invalidate the project. (Fortunately it is less than 2000 lines of code.) Given the importance of its correctness, I want to try to give a careful description of what the code is supposed to do so that others can audit the code. Currently there is a description of the basic OCaml types representing simple types, terms and proof terms. If anyone has feedback, please let me know.

[Trent Russell]

Regarding the initial distribution, you might look at what's been happening with clams the past month or two. A big "digger" appeared who had about half a million clams from the initial distribution. It's caused a massive drop in the price, of course, but also arguments within the community. I don't know how this could be avoided, but it's probably best to think about it pre-launch.

[Bill White]

Regarding the initial distribution, you might look at what's been happening with clams the past month or two. A big "digger" appeared who had about half a million clams from the initial distribution. It's caused a massive drop in the price, of course, but also arguments within the community. I don't know how this could be avoided, but it's probably best to think about it pre-launch.

Thank you for pointing me to this. I have not had time to keep up with the Clams project, but it's clearly a good idea for me to look into it further.

[Bill White]

While writing the documentation yesterday, I found bugs that would have been fatal for the project. Details are below. It has me rethinking my goals in terms of a timeline for Qeditas. It's probably safe to say that the network will likely not be up and running anytime soon.

Before describing the bugs, allow me to note that I have updated the current version of the technical documentation:
http://qeditas.org/qeditastechdoc.pdf

Also note that I stopped merging from the dev branch to the master branch in September. If you want to keep up to date with what progress has been made, watch the dev branch:
http://qeditas.org/gitweb/?p=qeditas.git;a=log;h=refs/heads/dev
My intention is to start merging from the dev branch into the master branch when the code base is reasonably stable.

Now, let me describe the bugs. This is in the mathdata module, in the file mathdata.ml. The documentation is Section 6.7 of the linked pdf above. One of the functions is tmtpshift, which should shift type variables (in de Bruijn representation). Here is how the code looked before yesterday:

Code:

let rec tmtpshift i j m =
  term_count_check ();
  match m with
  | DB(k) when k < i -> DB(k)
  | DB(k) -> DB(k+j)
  | Ap(m1,m2) -> Ap(tmtpshift i j m1,tmtpshift i j m2)
  | Lam(a1,m1) -> Lam(a1,tmtpshift i j m1)
  | Imp(m1,m2) -> Imp(tmtpshift i j m1,tmtpshift i j m2)
  | All(a1,m1) -> All(a1,tmtpshift i j m1)
  | TTpAp(m1,a1) -> TTpAp(tmtpshift i j m1,tpshift i j a1)
  | TTpLam(m1) -> TTpLam(tmtpshift (i+1) j m1)
  | TTpAll(m1) -> TTpAll(tmtpshift (i+1) j m1)
  | _ -> m

Here i and j are integers and m is a term.

There are two serious problems here. Firstly, the function should shift type variables, not term variables. Hence the first two cases handling DB (de Bruijn term variables) should not be included at all. The effect of including them was that the function would shift both type variables and term variables. Secondly, the type variables in the type argument "a1" of the Lam and All binder cases should have been shifted using tpshift. Since tpshift was not called on these arguments, type variables in these types would not have been shifted.

It's likely that either of these problems could have been exploited to prove false (an inconsistency), making the system useless as a library of formalized mathematics.

The corrected current version is as follows:

Code:

let rec tmtpshift i j m =
  term_count_check ();
  match m with
  | Ap(m1,m2) -> Ap(tmtpshift i j m1,tmtpshift i j m2)
  | Lam(a1,m1) -> Lam(tpshift i j a1,tmtpshift i j m1)
  | Imp(m1,m2) -> Imp(tmtpshift i j m1,tmtpshift i j m2)
  | All(a1,m1) -> All(tpshift i j a1,tmtpshift i j m1)
  | TTpAp(m1,a1) -> TTpAp(tmtpshift i j m1,tpshift i j a1)
  | TTpLam(m1) -> TTpLam(tmtpshift (i+1) j m1)
  | TTpAll(m1) -> TTpAll(tmtpshift (i+1) j m1)
  | _ -> m

While much of the code in mathdata was ported from Egal, I was responsible for introducing these errors when I added support for type variables in Qeditas. It's clear that I copied the function tmsubst and failed to make some intended modifications.

The fact that there were bugs in a fundamental part of the code base has given me pause. I do not know what timeline makes sense, but it's clear to me that Qeditas should not be launched until there has been a thorough code review.

[Bill White]

There is now a completed first draft of the technical documentation for the mathdata module (Chapter 6).

http://qeditas.org/qeditastechdoc.pdf

If someone wants to help out, reading Chapter 6 and comparing it to the code in mathdata.ml would certainly be helpful:

http://qeditas.org/gitweb/?p=qeditas.git;a=blob_plain;f=src/mathdata.ml;hb=e48c8d5335c4aff1a4c121eaf795d7373df56a2b

I would be happy to answer questions if any arise.

While writing this documentation I found more errors in the code, some of which could have been critical. There certainly could be even more still.

On a positive note, the code in mathdata.ml is now less than 1500 lines. I realized approximately 200 lines inherited from Egal were apparently to optimize which definitions get expanded during proof checking. This seems out of place in Qeditas, so I replaced it with simpler code to expand all definitions during proof checking. Terms can get very large by expanding definitions, but in the worst case one must do so anyway. Besides, there are resource bounds in Qeditas that will cause exceptions to be raised if terms get too large.

[Bill White]

Over the course of the past few weeks it's become clear to me that I will not be able to finish Qeditas on my own, at least not in the near future.

I wrote some partial networking code, but in tests it simply doesn't perform as I'd hoped. To be specific, two nodes would communicate and exchange block headers, but they often would not come to consensus and would simply continue to stake on their own blocks. It would be better for the system if someone with experience writing peer-to-peer / consensus code were to write this part of the code. It's perhaps best if the project takes a hiatus until someone with such experience decides to take up the challenge.

The networking / consensus portion isn't the only unfinished part. I also tried to write "daemon/command line interface" executables, but became unhappy with the code and stopped.

It's unrealistic for someone else to start trying to understand (much less extend) the current state of the code without good documentation. This has been the primary reason the past few weeks I've been writing the technical documentation. It is still unfinished, but at this point there is a first draft of every chapter except 8 and 9. I am still working on these. Chapters 10 and 12 briefly describe the current state of the networking and interface code, but I wouldn't suggest someone try to fix the code I wrote for these parts. It probably makes more sense for someone with a clear design in mind to recode the networking and top level from scratch.

As always, the current state of the technical documentation is here:

http://qeditas.org/qeditastechdoc.pdf

I can also announce that I carefully compared my snapshot with the one of sfultong. This led me to discover several hundred unspendable txouts in the Bitcoin block chain. I have updated the snapshot to remove the corresponding addresses. The new snapshot is available here:

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

[Trent Russell]

It sounds like the kind of code you're missing is code that all cryptocurrencies already have. Why don't you just port the code from some existing coin?

[Bill White]

It sounds like the kind of code you're missing is code that all cryptocurrencies already have. Why don't you just port the code from some existing coin?

This is a reasonable suggestion. Almost all cryptocurrencies are coded in C++, with NXT in Java being an exception. If someone wants to port the code from C++ or Java into OCaml, I'm happy for the help. As I have little experience with either language, I should not be the one porting from them.

[Trent Russell]

It sounds like the kind of code you're missing is code that all cryptocurrencies already have. Why don't you just port the code from some existing coin?

This is a reasonable suggestion. Almost all cryptocurrencies are coded in C++, with NXT in Java being an exception. If someone wants to port the code from C++ or Java into OCaml, I'm happy for the help. As I have little experience with either language, I should not be the one porting from them.

I didn't mean porting to ocaml. I meant porting the code (still in C++ or Java) from their project to yours. Everything doesn't have to be written in ocaml.

[Trent Russell]

After some searching, I found an open source p2p file sharing program written in ocaml called "MLDonkey":

https://en.wikipedia.org/wiki/MLDonkey

Maybe this has networking code you can use?

[Bill White]

I didn't mean porting to ocaml. I meant porting the code (still in C++ or Java) from their project to yours. Everything doesn't have to be written in ocaml.

Oh, thanks for clarifying. I have been trying to write everything in OCaml, but maybe this has been a mistake. (For example, the sha256 and ripemd160 code is very slow and should probably call a C implementation.) I'll think about whether the code from another cryptocurrency could be mixed in with the OCaml code in some way.

Also, thank you for the pointer to MLDonkey. I will read about it and see if some of its code could be helpful.

[sfultong]

Sorry to hear that you probably won't be able to finish on your own, Bill. It did seem like a very ambitious project, so I guess I'm not too surprised.

If there were only more traction for ML family languages in the greater programming community. Someday I hope to see a total functional language with refinement types catch on. Once I'm done with my cryptocurrency efforts, I want to contribute to unisonweb.

[Bill White]

Sorry to hear that you probably won't be able to finish on your own, Bill. It did seem like a very ambitious project, so I guess I'm not too surprised.

If there were only more traction for ML family languages in the greater programming community. Someday I hope to see a total functional language with refinement types catch on. Once I'm done with my cryptocurrency efforts, I want to contribute to unisonweb.

Thank you for the condolences. Qeditas has turned out to require far more work than I expected. What I originally thought would take a month or two has almost taken a year. I am trying to remain optimistic that someone with the necessary skills will fill in the remaining gaps, eventually.

[Bill White]

There is now a completed version of the technical documentation:

http://qeditas.org/qeditastechdoc.pdf

I expect from time to time I will revise parts of it and push the changes to the git repo, but I won't generally be announcing it on this thread unless there's a reason to do so.  I merged the "dev" branch into the "master" branch, so at the moment they are the same.

The website qeditas.org is in no danger of expiring at the moment, but in case it becomes inaccessible for some reason, I uploaded current versions of the relevant git repos to mega:

https://mega.nz/#!4tAnHJIJ!BsKwweNJ4N6m0nXLcdS59CdBbY5FPsMYDWvhTw0Kh48
https://mega.nz/#!F54hjYrL!5dmF54wh6DSS0WyWGJCg5eSXg188sfrZFFcHwK_ZmKQ
https://mega.nz/#!F8IgAIaY!EDfV8ivWSwbHzAHWkoGwWB0Q2Akg96izejnWAUfpc5I

If someone has questions, comments, or feedback generally, feel free to post here. I will occasionally check the thread for new activity. From now on, however, I will consider the project to be on hiatus.

[Trent Russell]

I was working with the code for Clams and thought of how I might be able to modify it to provide the network infrastructure you need for Qeditas. Clam transactions have a "clamspeech" part which can hold arbitrary data. This could be used (or abused?) to have dummy Clam transactions whose main content is a clamspeech part carrying Qeditas data (txs, blocks, ctrees, etc). In addition to giving a way of sharing the data between peers, the dummy txs with the Qeditas data can be stored in the local leveldb tx database.

I forked Clams, made some modifications and renamed it "qednet". It's on github with a "trdev" branch that has the actual modifications:

https://github.com/trentrussell/qednet/tree/trdev

I also put the Qeditas git repo back on github. There's also a "trdev" branch there, but I haven't started modifying anything yet:

https://github.com/trentrussell/qeditas

I'm thinking Qeditas (ocaml) can start qednet (C++) in a process. Qednet will connect up with peers and share inventory/data (this works already). Qeditas will be notified when there are new Qeditas transactions or Qeditas blocks. Qeditas can then ask qednet (via rpc commands) for the actual data which Qeditas can verify and organize (e.g., finding the "best" current block/ledger).

I should probably say that I'm not really a C++ programmer. The parts of the qednet code that didn't directly come from Clams was mostly copy-paste-modify from code in Clams. There is also some strange bug the first time I try to run qednetd. I'd expect it to make the .qednet directory and then advise the user on making a qednet.conf file. Instead the first time I run it it makes the .qednet directory and then dies with a seg fault. The second time I run it it warns that I need to -reindex. I don't actually need to -reindex (there are no blocks). Instead I run it a third time and it prompts me to make a qednet.conf file. After making the qednet.conf, I can run it a fourth time and it starts working. If this bug sounds familiar to anyone let me know.

I'm not sure any of this will work well enough to really start Qeditas, but at least it might keep the Qeditas project alive with a test network.

PS: To check if the first block is valid, I need the ctree corresponding to the initial ledger. I guess one node needs this and then it can get shared. @Bill: You posted a link to the initial distribution, but it's text files with address hashes and amounts. Do you have the ctree itself available somewhere?

[Bill White]

I was working with the code for Clams and thought of how I might be able to modify it to provide the network infrastructure you need for Qeditas. Clam transactions have a "clamspeech" part which can hold arbitrary data. This could be used (or abused?) to have dummy Clam transactions whose main content is a clamspeech part carrying Qeditas data (txs, blocks, ctrees, etc). In addition to giving a way of sharing the data between peers, the dummy txs with the Qeditas data can be stored in the local leveldb tx database.

I forked Clams, made some modifications and renamed it "qednet". It's on github with a "trdev" branch that has the actual modifications:

https://github.com/trentrussell/qednet/tree/trdev

I also put the Qeditas git repo back on github. There's also a "trdev" branch there, but I haven't started modifying anything yet:

https://github.com/trentrussell/qeditas

I'm thinking Qeditas (ocaml) can start qednet (C++) in a process. Qednet will connect up with peers and share inventory/data (this works already). Qeditas will be notified when there are new Qeditas transactions or Qeditas blocks. Qeditas can then ask qednet (via rpc commands) for the actual data which Qeditas can verify and organize (e.g., finding the "best" current block/ledger).

I should probably say that I'm not really a C++ programmer. The parts of the qednet code that didn't directly come from Clams was mostly copy-paste-modify from code in Clams. There is also some strange bug the first time I try to run qednetd. I'd expect it to make the .qednet directory and then advise the user on making a qednet.conf file. Instead the first time I run it it makes the .qednet directory and then dies with a seg fault. The second time I run it it warns that I need to -reindex. I don't actually need to -reindex (there are no blocks). Instead I run it a third time and it prompts me to make a qednet.conf file. After making the qednet.conf, I can run it a fourth time and it starts working. If this bug sounds familiar to anyone let me know.

I'm not sure any of this will work well enough to really start Qeditas, but at least it might keep the Qeditas project alive with a test network.

PS: To check if the first block is valid, I need the ctree corresponding to the initial ledger. I guess one node needs this and then it can get shared. @Bill: You posted a link to the initial distribution, but it's text files with address hashes and amounts. Do you have the ctree itself available somewhere?

This sounds like an interesting approach. I will need to look more closely before I can say more.

Regarding the initial ctree, I do have a binary version. It consists of approximately 100,000 files each of which contains part of the ctree. The files range in size from 74 bytes to 769042 bytes. However, the large one is an outlier. The next largest files are 146365 bytes and then 57852 bytes.

A compressed directory with all these files is available from mega here:

https://mega.nz/#!tgghSCKZ!aXnBE1d7nI65quPpiGvgLOOrTg3ODeuSud1BqAxvLkQ

It is roughly 250MB total.

There is Qeditas code for loading these files and obtaining the part of the ctree they represent. In particular, see the function get_ctree_abbrev. You will first need to set ctreedatadir:

Code:

Config.ctreedatadir := "/fullpathto/initctrees"

The initial ledger root is af8de840af01805f1dbe9f1312c388efeea1e619. An abbreviation for a ctree with this ledger root is named 0b7f6f55f3b4b05a9a7bd99d01a087d799e01b9c. This can be loaded and viewed as follows:

Code:

let cinittop = Ctre.get_ctree_abbrev (Hash.hexstring_hashval "0b7f6f55f3b4b05a9a7bd99d01a087d799e01b9c");;
val cinittop : Ctre.ctree =
  Ctre.CLeft
   (Ctre.CBin
     (Ctre.CAbbrev
       ((1442101457l, 180266486l, 913955555l, 2050428135l, -929962841l),
       (2055486346l, 214952729l, -1159736634l, -1343903178l, 337615324l)),
     Ctre.CAbbrev
      ((-1653840840l, 739647671l, -1962027568l, 372448381l, -1899755430l),
      (1623437078l, 1755382547l, -619214889l, -762676765l, 1420032299l))))

This represents the top two levels. The first two bits indicate the type of address: p2pkh, p2sh, term, publication. Since there are initially no terms or publications, the right child of the root is empty. This is why cinittop starts with "CLeft". The next "CBin" splits into the left (p2pkh) and right (p2sh).

If we simply look at the left child, it has root "(1442101457l, 180266486l, 913955555l, 2050428135l, -929962841l)" and abbrev hash "(2055486346l, 214952729l, -1159736634l, -1343903178l, 337615324l)". Note that hash values are represented by 5 32-bit integers. You can also see it in hex as follows:

Code:

Hash.hashval_hexstring (2055486346l, 214952729l, -1159736634l, -1343903178l, 337615324l);;
- : string = "7a843b8a0ccfeb19badfd2c6afe5aa36141f99dc"

There is a file named 7a843b8a0ccfeb19badfd2c6afe5aa36141f99dc holding the ctree which hashes to this value. It can be loaded as follows:

Code:

let cp2pkhinittop = Ctre.get_ctree_abbrev (2055486346l, 214952729l, -1159736634l, -1343903178l, 337615324l);;
val cp2pkhinittop : Ctre.ctree =
  Ctre.CBin
   (Ctre.CBin
     (Ctre.CBin
       (Ctre.CBin
         (Ctre.CBin
           (Ctre.CBin
             (Ctre.CBin
               (Ctre.CBin
                 (Ctre.CAbbrev
                   ((1966404489l, 484598006l, 138518841l, 1976927092l,
                     -869398977l),
                   (1262074113l, 53533383l, 1018187993l, 684848879l,
                    1620505634l)),
...

This corresponds to the p2pkh contents split into 256 "abbrevs" based on the first byte of the p2pkh address. I'm only showing the first abbrev, corresponding to p2pkh addresses with an initial 0 byte. We can load this subtree as well:

Code:

let cp2pkhinit00 = Ctre.get_ctree_abbrev (1262074113l, 53533383l, 1018187993l, 684848879l, 1620505634l);;

This will give a tree with 8 levels again, splitting based on the second byte of the address. The abbrev hash for the left-most subtree is (1602475596l, -1426117715l, -1600090211l, -2046806429l, 138862169l)
(i.e., 5f83d64caaff2bada0a08f9d860036630846de59). This subtree contains all the contents of address for which the first two bytes are 0.

Code:

let cp2khinit0000 = Ctre.get_ctree_abbrev (1602475596l, -1426117715l, -1600090211l, -2046806429l, 138862169l);;

I hope this helps.

[Trent Russell]

Thanks. I was able to extend the C++ code to have a "savedatafromfile" command and used it to save all the initial ctree abbrev files into the leveldb database. It takes up about 330MB total.

I can then get them back upon demand:

Code:

qednetd loaddata qctreeabbrev 0b7f6f55f3b4b05a9a7bd99d01a087d799e01b9c
ba55f4b8d10abea5f63679dae37a370ce7c891e4a77a843b8a0ccfeb19badfd2c6afe5aa36141f99dced6423c361b100b95d6ca886b698e1e8732446d0021b7eb5400b1d98d8be38bc9656cc1ba71acd5f01

In principle another node should be able to get the data from a peer:

Code:

qednet getdata qctreeabbrev 0b7f6f55f3b4b05a9a7bd99d01a087d799e01b9c

But it doesn't get sent for some reason, so it's still work in progress.

Edit: I found the problem, so now ctrees can be requested from peers.

[Trent Russell]

I have added some code for Qeditas to call qednet for things. Things are looking good so far.

One thing, though. I looked at the "frame" used to create the initial distribution ctree (in qeditasinit.ml in the initdistr branch):

Code:

let fr10 = flevs 8 FAll;;
let fr2pk = flevs 8 fr10;;
let fr2s = flevs 8 fr10;;
let fr0 = FAbbrev(FBin(FBin(FAbbrev(fr2pk),FAbbrev(fr2s)),FAll));;

I wanted to save this frame in the database and potentially share it with peers, but the serialization of it was surprisingly large (over 100K). Looking closer it was clear this could be improved by using sharing. I changed the serialization code (seo_frame and sei_frame) to check if the two children of a binary FBin node are equal and treat this separately from the "real" binary case. This made the serialization of the frame above only 9 bytes(!).

Here's the modified serialization code:

https://github.com/trentrussell/qeditas/blob/trdev/src/ctre.ml#L706

I tried to do things the same was as was described in the Serialization chapter of:

http://qeditas.org/qeditastechdoc.pdf

[Bill White]

I have added some code for Qeditas to call qednet for things. Things are looking good so far.

One thing, though. I looked at the "frame" used to create the initial distribution ctree (in qeditasinit.ml in the initdistr branch):

Code:

let fr10 = flevs 8 FAll;;
let fr2pk = flevs 8 fr10;;
let fr2s = flevs 8 fr10;;
let fr0 = FAbbrev(FBin(FBin(FAbbrev(fr2pk),FAbbrev(fr2s)),FAll));;

I wanted to save this frame in the database and potentially share it with peers, but the serialization of it was surprisingly large (over 100K). Looking closer it was clear this could be improved by using sharing. I changed the serialization code (seo_frame and sei_frame) to check if the two children of a binary FBin node are equal and treat this separately from the "real" binary case. This made the serialization of the frame above only 9 bytes(!).

Here's the modified serialization code:

https://github.com/trentrussell/qeditas/blob/trdev/src/ctre.ml#L706

I tried to do things the same was as was described in the Serialization chapter of:

http://qeditas.org/qeditastechdoc.pdf

This change makes sense, and your code conforms to the style of the other serialization code. One issue worth noting is that two different serializations can deserialize to the same frame (one using sharing and one not), but this shouldn't be a problem.

I still haven't yet looked at the C++ qednet code, but hope to do so soon. Thank you for your efforts.

[Trent Russell]

Since it seems like there's still lots of time before Qeditas will launch, I want to propose that the units in the initial distribution slowly decrease over time. Specifically, I'm thinking that the distribution from the snapshot that can be claimed is 100% for roughly the first 5 years, but then halves along with the block reward every 4 years. I wrote code that does this in one of my Qeditas branches:

https://github.com/trentrussell/qeditas/blob/trdevnf/src/assets.ml#L92

A situation occurred in the Clam community recently where someone found out they had a significant amount of clams from the initial distribution and over a couple of months "dug" them ("digging" is the way clams are claimed) and sold them on the market. Not only did this hurt the price of clams a lot, it also fractured the community. Some insisted that "digging" be stopped to avoid a big digger event happening again. Others insisted that stopping digging would be breaking the promise of the original distribution.

To avoid a similar debate in Qeditas, I think it's a good idea to already know that the threat of someone with a massive distribution from the snapshot is temporary. At the same time, everyone should have sufficient time to make their claim. Five years seems like a reasonable amount of time. After that, those with Qeditas currency from the initial distribution can still make their claim, but they will effectively get less. This halving would continue for roughly 200 years until the remaining units from the initial distribution is 0. Another reason this is a good idea is that there's no way to tell the difference between "lost" coins and unclaimed coins. Over time, unclaimed coins (from the initial distribution) disappear, leading to more certainty about the coin supply.

Bill wrote me that he has "mixed feelings" about reducing the initial distribution over time like this, but is "open to being persuaded." He suggested I ask for comments on the thread. I'll let him say more about his opinions on the matter if he wants.

Thoughts? Is this controversial?

[Bill White]

Bill wrote me that he has "mixed feelings" about reducing the initial distribution over time like this, but is "open to being persuaded." He suggested I ask for comments on the thread. I'll let him say more about his opinions on the matter if he wants.

Thoughts? Is this controversial?

It's perhaps fair to say that your proposal hasn't generated controversy. I don't have a strong objection to slowly decreasing the amount of initial distribution that can be claimed. It's consistent with the Spin-Off idea, so long as there is sufficient time for everyone to claim their part of the distribution. Five years certainly seems like enough time to become aware of the project and make a judgment about it.

[gshumway]

Hi. Have you stopped to work on this project?

[Bill White]

Hi. Have you stopped to work on this project?

Thank you for your interest.

Due to being busy with other things, I have not directly done any work on Qeditas since December. Nevertheless, I have been exchanging private messages with someone who has been experimenting with his own fork of the code. I must admit I haven't looked closely at his progress, but hope to spend some time reviewing it soon. Perhaps he will want to say more.

Generally speaking, anyone who wants to help bring Qeditas to reality is welcome. It turned out to be much more work than originally estimated. The idea of combining formalized mathematics with a cryptocurrency still appeals to me. I am certainly still interested in seeing the project completed, even if it takes years instead of months.

[Trent Russell]

Due to being busy with other things, I have not directly done any work on Qeditas since December. Nevertheless, I have been exchanging private messages with someone who has been experimenting with his own fork of the code. I must admit I haven't looked closely at his progress, but hope to spend some time reviewing it soon. Perhaps he will want to say more.

OK. I can give a short summary of what I've been doing.

In January I tried using a fork of Clams to do the networking and database storage for Qeditas. This worked well enough that I had two or three nodes running a testnet for about a week. There were problems though and I don't think it makes sense to inherit a lot of code and dependencies that aren't needed. So now I'm trying to directly code the networking and database code in ocaml with the rest of Qeditas.

One technical point might be worth mentioning: I got rid of "frames" entirely. Now ledger trees (ctrees) are always stored and communicated as "elements"  -- essentially 9 levels with hashes summarizing the lowest levels (except leaves).

It's like fixing the "frame" to be one that abstracts every nine levels.

If all goes well, at some point I should be able to get some kind of testnet running. If so, I'll say more about how others can run a testnet node too. But I don't know if "at some point" will be next month or next year. Even at that point, I wouldn't recommend starting a mainnet until the testnet has run without a problem for a few months and people have had a chance to review the code.

[gshumway]

Really glad to hear you are still interesting in this project.) I think qeditas idea is really great and important.

I would be glad to help in development, but I havent't enough skills right now (I'm a C++ developer without deep math education), but I'm learning and I hope I can be useful in a several monthes or about. Tell me please if you know some tasks where I can participate right now,  I'll be glad to do smth. useful.)

[Bill White]

Really glad to hear you are still interesting in this project.) I think qeditas idea is really great and important.

I would be glad to help in development, but I havent't enough skills right now (I'm a C++ developer without deep math education), but I'm learning and I hope I can be useful in a several monthes or about. Tell me please if you know some tasks where I can participate right now,  I'll be glad to do smth. useful.)

This is good to hear. I do have some ideas how someone with C++ (or C) knowledge could improve Qeditas, and I will write more about this later.

[Bill White]

After spending some time reviewing Trent Russell's code, I have merged it into the dev branch: http://qeditas.org/gitweb/?p=qeditas.git;a=log;h=refs/heads/dev

This gives all of us a common code base to branch off of, in case anyone wants to contribute.

The white paper had not been updated in over a year, so I spent some time bringing it into agreement with the current status and plan. For example, the white paper now discusses the plan to have claim windows during which the value of the unclaimed initial distribution will halve every 4 years after the first 5 years.

The latest draft of the white paper is here: http://qeditas.org/qeditas.pdf

One thing is worth explicitly discussing now. The snapshot from block 350,000 is now over a year old. While I am not opposed to using a more recent snapshot instead, I am opposed to taking such a snapshot myself. Taking and preparing such a snapshot is very tedious and time-consuming, and I have no interest in doing this again. If someone feels strongly that a more recent snapshot should be used, please prepare it for me. Otherwise, I will simply use the earlier snapshot. There are stronger arguments in favor of using the older snapshot, or perhaps combining the older snapshot with a newer one. For example, the earlier snapshot was announced in advance as the one on which the Qeditas distribution would be based. It may be considered unfair to change that now.

My next task is to update the technical documentation to reflect the changes in the code. Then I will create a version people can download, try to compile, and check their balances. To check a balance, people will need to also download the initial ledger tree, which is roughly 700MB. This data will be separate from the git repo.

[gshumway]

Hello.

I can prepare a newer snapshot if you are interested in it. I don't think it is a real difference,  but can do it if you need it to save your time.) Tell me please if it should be done and I start to work.

[Bill White]

Hello.

I can prepare a newer snapshot if you are interested in it. I don't think it is a real difference,  but can do it if you need it to save your time.) Tell me please if it should be done and I start to work.

You can if you want, but it's probably better to wait. The earliest I can imagine the Qeditas network launching is in late 2016. It's likely that if someone wants a fresher snapshot, then they will want it to be nearer to the time of the launch than now. The user sfultong (earlier in this thread) did some work to help people create snapshots. I am not sure of the status of his work, but if you do decide to take a snapshot his work might help you.

Something that would be much more helpful (and probably easier) would be to integrate the Qeditas OCaml code with some standard library for persistent storage of key-value pairs, like leveldb. Trent Russell tried to do this, but encountered some difficulties. In the end, he implemented his own file based storage "database" module. I have recently finished documenting his database code in Chapter 6 of the Technical Documentation:

http://qeditas.org/qeditastechdoc.pdf

That code is in src/db.ml and src/db.mli in the dev branch.

Integrating with leveldb (or something similar) would almost certainly have better performance.

There is a chapter in the OCaml manual that explains how to call C functions:

http://caml.inria.fr/pub/docs/manual-ocaml/intfc.html

A similar task would be to have the Qeditas OCaml code call C functions to do the hashing (sha256 and ripemd160). There must be open source C implementations of these hashing functions, and I suspect calling C versions instead of the current OCaml versions would significantly improve performance.

[Trent Russell]

Here's a link to a branch where I tried to use leveldb:

https://github.com/trentrussell/qeditas/tree/trdevnfth-leveldb

It actually does compile, at least for me on debian. I got leveldb-1.18 and then compiled it. To compile qeditas I first had to set some directories are set using the configure file:

Code:

./configure -leveldb=<fullpathtoleveldbdir> -ocamlinclude=<ocamldir>/lib/ocaml
make

I have in my notes though that in some situation I got an error like:

Code:

Error: Error on dynamically loaded library: ./bin/dlldb.so: ./bin/dlldb.so: undefined symbol: _ZN7leveldb2DB4OpenERKNS_7OptionsERKSsPPS0_

Instead of trying to figure this out, I switched to just saving things in files. I assume this is some kind of linking error which would be easy to resolve if I knew more about it.

[Bill White]

I have decided to do the first alpha release. Most of the important functionality is still missing, but at least this gives a chance for people to try to compile and run the code.  It will not connect to a network. At the moment, the main things a user can do is import addresses into a wallet and print the assets they have in the initial distribution.  (Again, the initial distribution was based on Bitcoin block height 350,000. This is fine for the testnet, but I am open to changing it for the mainnet when the time comes.)

You can download the release 0.0.1rc2 either from qeditas.org:

qeditas.org/qeditas-0.0.1rc2.tar.gz

or from mega.nz:

https://mega.nz/#!MhAUUA6S!cTe33Yd5P4p7WYU5fFuWAC-kmqKhzhfFIv0h4bRRLBU

If you want to verify the integrity, here is the sha256sum:

1a88b885f0e4dd5c663440326047ca1b316e5875c5697d3930deb314dbbd2773

There is a README.md file that explains how to compile and run Qeditas, as well as how to import (watch) addresses and print the assets held at those addresses.

(There are also commands for importing private keys. Just to be safe, I recommend no one tries this with private keys that held bitcoins. Importing as a watch address is sufficient for now. When the time comes to test staking, the assets in the initial distribution can be controlled via endorsements. You will never need to import a private key that held bitcoins.)

You will need OCaml to compile Qeditas.

If you want to print the assets in the initial distribution, you will need one version of the initial ledger tree. I have created and
uploaded three versions: one with the full ledger tree (656MB), one with only the p2pkh addresses (606MB) and one with only the p2sh addresses (39MB). These files are too big to download from qeditas.org, so they are at mega. (You only need one.) Here are the links and the sha256sum to verify the integrity.

qeditas-db-initdistr-full.tgz
https://mega.nz/#!Ap5ylL4C!WLy3bTvMWSwuIKVQvmW7BOT7t38WWLeU8bVlRxt7CtE
sha256sum: 6687d1f4bd4a6c2263276e83f6a27f3d7df465f8adfaa6322f950cb9ae58faf4

qeditas-db-initdistr-p2pkhonly.tgz
https://mega.nz/#!t5YnjJBZ!1LUVDNm9p7PYI51bA2__m323zwnBK3aG0r82_sGY7Qs
sha256sum: d48201961b2d2b904b1aad5911131d3f23714ac30d25daa085e9d45850afdded

qeditas-db-initdistr-p2shonly.tgz on mega:
https://mega.nz/#!NlpTSY5I!eg2MYZeKLF0W30yngBlXprqrMnmqfz_Mx3QKOtIrjO0
sha256sum: fc3c39f7b87de31f9c4b46dfce2eeec0e1691bb7863455311ec3e8a875f06134

The README.md file explains what to do with the file once you download it. (Again, you only need one. If you want to check both p2pkh and p2sh addresses, you'll need the full one.)

Here is a PGP signed copy of the links and hashes above, for those who are extra cautious. My PGP key is available at https://pgp.mit.edu/ (search for billwhite@bitmessage.ch).

Code:

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

qeditas-0.0.1rc2.tar.gz
qeditas.org/qeditas-0.0.1rc2.tar.gz
https://mega.nz/#!MhAUUA6S!cTe33Yd5P4p7WYU5fFuWAC-kmqKhzhfFIv0h4bRRLBU
1a88b885f0e4dd5c663440326047ca1b316e5875c5697d3930deb314dbbd2773

qeditas-db-initdistr-full.tgz
https://mega.nz/#!Ap5ylL4C!WLy3bTvMWSwuIKVQvmW7BOT7t38WWLeU8bVlRxt7CtE
sha256sum: 6687d1f4bd4a6c2263276e83f6a27f3d7df465f8adfaa6322f950cb9ae58faf4

qeditas-db-initdistr-p2pkhonly.tgz
https://mega.nz/#!t5YnjJBZ!1LUVDNm9p7PYI51bA2__m323zwnBK3aG0r82_sGY7Qs
sha256sum: d48201961b2d2b904b1aad5911131d3f23714ac30d25daa085e9d45850afdded

qeditas-db-initdistr-p2shonly.tgz on mega:
https://mega.nz/#!NlpTSY5I!eg2MYZeKLF0W30yngBlXprqrMnmqfz_Mx3QKOtIrjO0
sha256sum: fc3c39f7b87de31f9c4b46dfce2eeec0e1691bb7863455311ec3e8a875f06134
-----BEGIN PGP SIGNATURE-----

iQIcBAEBCgAGBQJXVvoaAAoJEBTKnDJBv3qS5BwP/3iR8LBer/ex9FM8xdx8H9iN
uYioy7j+6Sr+zenW7ZxKsReMtxXNsk27sKJni7hAbZWN0JJPFQpZpMzGNmH3ZqAc
NzOidm+XtdSn8HKiGfW0QVmizblOpR0CWxmTD/VXSbZFaOIUr9NCVXgRo+UyaR2u
gEZisk6IFAh66cA6reS1dhg5j8Cb/svtOUTiVd6RQMK1WinNOxbqJUj8eSO5XPKr
07FoXZm/NB5FyfSfvh7zET/SnHDujV0hwEvZ6PnlAL2TlRlRfanoBYIpuQXan3ZH
iOwMBXRQ/ALOEwwOCx+Pw0i0bzZL/qVeYNwTT6nSpO/X3rnVT7QYzWt0ToabgFEz
TnPvYwH3ImgRwnar2G+1IDIWhY4wPK2bVsnnwzBfvFkaGeNH8g11DuhkglWQJJ8i
T4CAn70LV469lMoK/BZtFZEWrLP/TgGmXuFQnExMsBrERRXjpUoSRTGbFAH1c2qH
acaoP9Tt/W9qVvOhYYK0Ui3bqFOQ5tRda8phngDOgFrE+nFjpl3u5rYRkawfWu9E
trQBt7CKK9YzqZbKan+sLV/ynLULVuHuqR/dlyWZWfGdxS24misSBfXZm8ELOyy0
2d+vyvwP/y1XeRsx6xZ23qgcrpI0giGmVHGdcoXEHKSMiAj5pPLDHuu/C0jAvJvY
HP5Gx5sqGPk1ikGhPQax
=GjWN
-----END PGP SIGNATURE-----

Of course, I can imagine there may be problems. Feel free to post here about the problems and we can try to fix them. The purpose of this release is simply to get an initial idea of what issues to expect.

Here are two issues I can preemptively address:

Qeditas has only been tested under Linux. I would be surprised if it worked under Windows.  It probably works under Mac OSX, but this has not been tested.  Others are welcome to attempt to use Qeditas under Windows, but I can not imagine myself investing effort into a Windows version.

There is no GUI. When you run the executable you will be in a console in which you can give commands. I have no plans to build a GUI, but someone else is welcome to do so.

[gshumway]

Congratulations on your first release!)

I am at Windows PC right now, so I'll try to install it under Windows today.

Trent Russell, thank you for sharing your work with leveldb integration,  I'll try to fix library issue if it is possible and will share result if I will find something useful.

[TrueAnon]

I feel like Mexican food after having read this coin name!

[Bill White]

Congratulations on your first release!)

I am at Windows PC right now, so I'll try to install it under Windows today.

Thank you. If it turns out to work under Windows, I will be happily surprised. If it turns out to require some minor modifications to work under Windows, please let me know. In that case, I can do a new release with the modifications.

[d-leit]

I feel like Mexican food after having read this coin name!

lol..after this comment is the first time i am having an idea how to pronounce it!

[Bill White]

I feel like Mexican food after having read this coin name!

lol..after this comment is the first time i am having an idea how to pronounce it!

I assume this is intended as a (humorous) reference to quesadillas. This is actually close to how I pronounce it, except there are three syllables with the stress on the first.

Here is an attempt to give the pronunciation using the IPA.

https://en.wikipedia.org/wiki/Help:IPA_for_English

quesadilla (/ˌkeɪsəˈdiːjə/)
qeditas (/ ˈ keɪ diː tɑːs /)

[gshumway]

I'm failed to make it working under the Windows,  but may be it is because of my poor OCaml envirinment knowledge,  I'll try it one more time today or tmorrow. I've tested it under the Linux (Ubuntu) and all is correct as far as I can see.) I haven't tried to use it with C code yet, will try to do it this weekend.

[Bill White]

I'm failed to make it working under the Windows,  but may be it is because of my poor OCaml envirinment knowledge,  I'll try it one more time today or tmorrow. I've tested it under the Linux (Ubuntu) and all is correct as far as I can see.) I haven't tried to use it with C code yet, will try to do it this weekend.

Thank you for trying under Windows. It isn't surprising that it does not work immediately.

If you are getting OCaml errors, feel free to post them here or send them to me in a private message. If I recognize the errors, I might be able to advise you.

One possibility is to use Cygwin: https://cygwin.com/. It is supposed to simulate a linux environment withing Windows.

[gshumway]

At the end of the day I've managed to build and start it under the Windows,  and it works correctly.)

The only problem is src/qeditas.ml,  line 331:

Code:

    let dur = open_in_bin "/dev/urandom" in (*** this is to compute a nonce for the node to prevent self conns; it doesn't need to be cryptographically secure ***)

I've used a real file with real path instead of the "/dev/urandom" as a simplest workaround, I need more OCaml knowledge to fix it correctly, I can't do it right now.

I'll share Windows build instructions later, after I test it on clear Windows installation and choose the simplest way to build the project.

[Bill White]

At the end of the day I've managed to build and start it under the Windows,  and it works correctly.)

The only problem is src/qeditas.ml,  line 331:

Code:

    let dur = open_in_bin "/dev/urandom" in (*** this is to compute a nonce for the node to prevent self conns; it doesn't need to be cryptographically secure ***)

I've used a real file with real path instead of the "/dev/urandom" as a simplest workaround, I need more OCaml knowledge to fix it correctly, I can't do it right now.

I'll share Windows build instructions later, after I test it on clear Windows installation and choose the simplest way to build the project.

That is great to hear! Thank you for your work.

Regarding the call to /dev/urandom, this could be replaced by something giving random numbers that do not need to be cryptographically secure. However, in the end we will definitely need to be able to obtain cryptographically secure random numbers. In linux I can get these from /dev/random. There must be some way to obtain cryptographically secure random numbers in Windows, in a way that can be called from OCaml.

[gshumway]

It seams that main Windows build problem was because of the big number of the C++ compilers installed on my PC.) All is simple and working without big problems on clear Windows installation:
 1. Install MinGW with MSYS (http://mingw.org/,  use 64bit toolchain)
 2. Install OCPWin (https://www.typerex.org/ocpwin.html,  use compiled with mingw package)
 3. Add OCPWin bin directory to system PATH environment variable.
 4. Open MSYS and navigate to qeditas sources
 5. Fix the problem in sources,  mentioned in previous post,  for example change "/dev/urandom" to "urandom" and place non-empty file with name urandom near the qeditas.exe in the future.
 6. Use usual configure & make to build qeditas.exe (set install and data directory in configure args)

That's all.

Now I'm trying to build Trent Russel's branch with leveldb.

What about dev/urandom: I hope to find universal way to get random numbers in OCaml,  if there is no such way (it would be surprising) we can add C-based module to generate such numbers that will work on any platform.

[mishra1994u]

How was the distribution balances calculated?
Are these balances in lowest unit forms?

[Bill White]

How was the distribution balances calculated?
Are these balances in lowest unit forms?

The distribution is based on a snapshot of the Bitcoin balances as of block 350,000.

Qeditas is currently displaying the balances in terms of the lowest units ("cants"). An address that had 1 satoshi in the snapshot starts with 1000 cants in Qeditas. (In other words, Qeditas has 3 extra digits of precision.) Perhaps it would be a better idea to display the number of fraenks instead, since 1 fraenk corresponds to 1 bitcoin. It would be easier for people to check that the distribution is correct.

[Bill White]

I made two minor changes based on the comments above and tagged a "0.0.1" version. The source code is here:

http://qeditas.org/qeditas-0.0.1.tar.gz

The changes are:

1. There is now a check to see if the file "/dev/urandom" exists before attempting to open it. As gshumway noted, this file does not exist under Windows. The purpose was simply to create a nonce for the node (to prevent it from trying to connect to itself), so if "/dev/urandom" does not exist, then the current time is simply used as a nonce. This is a temporary solution. Hopefully Qeditas 0.0.1 will now compile and run under windows without modifying the source code.

2. I changed the behavior of "printassets" so that it prints the number of fraenks. If you had, for example, 0.1 bitcoins in an address at the time of the snapshot, then you have 0.1 fraenks at the corresponding Qeditas address. (More information about the currency units is in the white paper.)
I have been working on the staking and networking code. The next step will be to distribute a release candidate for 0.0.2. It should have the basic ability to connect and stake (all testnet, of course). My expectation is that we will restart from a new testnet genesis once a week or so a few times before trying to stake for longer periods.

In order to stake, users will need to import testnet endorsements. (Importing the appropriate private key would also work, but I do not recommend this.) Importing testnet endorsements is already possible in the current release (0.0.1).

Here is a brief explanation of how to create and import a testnet endorsement. This is only for practice, since the testnet addresses will have a different format starting with the next release.*

1. Create a fresh bitcoin private key. Qeditas cannot do this for you yet. Do not use a private key from your bitcoin wallet. As an example, I went to bitaddress.org and generated a paper wallet with bitcoin private key: KyPNZNdF7vRKJqFED2fuLMqAT8oq191TmeRyVEZdbgo3kGL9mq99

2. Start Qeditas and import this private key into your Qeditas (testnet) wallet:

Code:

./bin/qeditas -testnet
> importbtcprivkey KyPNZNdF7vRKJqFED2fuLMqAT8oq191TmeRyVEZdbgo3kGL9mq99
Imported key for address QjTYZmD1HSKim9wTcnTVzD4kBhHFKkDY5r

The corresponding Qeditas address is QjTYZmD1HSKim9wTcnTVzD4kBhHFKkDY5r

3. Find a bitcoin address that had a balance at Block 350,000 (before the txs in this block were processed) for which you have the private key. An example for me is the address 1LvNDhCXmiWwQ3yeukjMLZYgW7HT9wCMru which had a balance of 0.0015 btc. There are 0.0015 fraenks at the corresponding Qeditas address. You can verify this by importing the address as a watch address in your wallet:

Code:

> importwatchbtcaddr 1LvNDhCXmiWwQ3yeukjMLZYgW7HT9wCMru
Importing as Qeditas address QgXMKzVExBPkqC4gL63qTqLK1NEAMsuzcq
> printassets
Assets in ledger with root 66c029f4c29b351785c0480cedc9449b64332dfa:
...
Watched assets:
QgXMKzVExBPkqC4gL63qTqLK1NEAMsuzcq:
37cfcd67a77ded709ff0b03c1d80ed5fbed8b33f [0] Currency 0.0015 fraenks (150000000 cants)

This means the corresponding Qeditas address is QgXMKzVExBPkqC4gL63qTqLK1NEAMsuzcq, and in the initial distribution it controls one asset, a currency asset with 0.0015 fraenks. The 40 character hex string
37cfcd67a77ded709ff0b03c1d80ed5fbed8b33f is the 20 byte asset id. The "0" in brackets means the asset was created at height 0 (the initial distribution).

4. Using the private key for the bitcoin address from Step 3, sign a message of the form "testnet:endorse <Qeditas Address>". For example, I could endorse QjTYZmD1HSKim9wTcnTVzD4kBhHFKkDY5r as a Qeditas address that can sign for the 0.0015 fraenks by signing the message

Code:

testnet:endorse QjTYZmD1HSKim9wTcnTVzD4kBhHFKkDY5r

with the private key for 1LvNDhCXmiWwQ3yeukjMLZYgW7HT9wCMru. The signature will be a long base 64 encoded string (of roughly 90 characters). Since I have revealed the private key for this example address, I will not sign such an endorsement. Instead,

Code:

IKtfPT5fnrN2FmzGk+MY2fHARxtwJXDCqOo5Zk14RsGXHcYCRKRqY5ZsBNGckq631TRPWLj4NI69iMp4fNe9j3U=

is a signature for

Code:

testnet:endorse QgBfPc2jSS5JTe5sncpKoKUAmKQ9mTBCm5

The private key for QgBfPc2jSS5JTe5sncpKoKUAmKQ9mTBCm5 is in my wallet, and was imported as in Step 1.

5. Import this endorsement into your wallet using "importendorsement" as "importendorsement <from address> <to address> <signature>". In my case:

Code:

> importendorsement QgXMKzVExBPkqC4gL63qTqLK1NEAMsuzcq QgBfPc2jSS5JTe5sncpKoKUAmKQ9mTBCm5 IKtfPT5fnrN2FmzGk+MY2fHARxtwJXDCqOo5Zk14RsGXHcYCRKRqY5ZsBNGckq631TRPWLj4NI69iMp4fNe9j3U=
just verified endorsement signature:
...
endorse QgBfPc2jSS5JTe5sncpKoKUAmKQ9mTBCm5

After importing the endorsement in my case, I can use the private key for QgBfPc2jSS5JTe5sncpKoKUAmKQ9mTBCm5 to sign for QgXMKzVExBPkqC4gL63qTqLK1NEAMsuzcq. In particular, I can use the asset above with 0.0015 fraenks for staking during the testnet.

These endorsements are only for the testnet. Endorsements on the mainnet will be signed messages without the "testnet:" prefix.

*Edit: The examples above work in 0.0.1, but will not work in future versions. In 0.0.1 testnet addresses are idential to mainnet addresses. This was an oversight which will be corrected in the next release.

[Bill White]

The work on the Qeditas code is progressing, though slowly again. I hope to give a more detailed update soon. Given the Ethereum hard fork today, I decided to make a statement regarding conditions under which Qeditas should (and more importantly should not) hard fork.

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

Today, July 20, 2016, the Ethereum community hard-forked in order to reverse the outcome of an ill-fated, buggy Ethereum program ("the DAO"). I play no role in the Ethereum community, but thought it would be an important opportunity to state, in advance, my position if something similar were to occur with Qeditas in the future.

It is quite likely that "buggy" propositions (and even "buggy" theories) will be published in the Qeditas block chain. For example, someone may formulate a conjecture they believe to be a formal version of The Riemann Hypothesis (or some other Millennium Problem). Under this belief, many people may contribute large bounties to encourage the resolution of the conjecture. Such bounties will encourage others to look more carefully at the conjecture, and someone may discover a flaw in the formulation. This flaw may mean that it is not a version of The Riemann Hypothesis, but instead is some other easily resolved conjecture. The person who discovers this can resolve the conjecture and claim the bounties.

This is, to be clear, part of the intended operation of the system. It is common for people to make mistakes when formalizing mathematics (just as programming mistakes are common). The only way these mistakes are found is by having intelligent people look very carefully at the formalization (or "code").

In such a case, it is conceivable that some of the people who contributed to the bounties would be disappointed, and might even suggest a hard fork to return the bounties to the contributors.

For my part, I would never support such an action in principle or in practice. If I were still actively developing Qeditas and such a hard fork were to occur, I would either support the original chain or abandon the project as a failure.

There are situations in which a hard fork might be needed. For example, if there were a bug in the consensus code or in the proof checker itself. Someone making use of the system as designed would never form a valid justification for a Qeditas hard fork.

Bill White
Qeditas Developer
July 20, 2016
-----BEGIN PGP SIGNATURE-----

iQIcBAEBCgAGBQJXj9HIAAoJEBTKnDJBv3qSXCAP/34V+O3khxfdcrityOFrey0P
iSWoLfvCgWA6spLyjNv06IdyeaWPALToxgy8FISPmxobCMXrQ33fvM40v0+4BuqC
xplGHuQgxAEX7Z1dk2K4OzTDkblxDR2gglZy2/3Tox0TZ6l5FwA5KrnmU9AxLZhy
KKCAdouKYi072Ix3dxtIIRUN1Yt20+pjmOj+L+QdTEnw7e9lZr26KxAYRjxERLRE
n5Mtw/7oT66kdvryEy4QY5GVeXkSnwFsFH/5hr5GTu8Q+kigXaVhKYQJJ0BMs3ol
Ua6fwVZoYJijPyqEKpoBl0RTj9iPoqnyVWDgSzs8o3/EUqfqCMKulMSShNc6Cs2m
53M8jp9vTCHN8nQbMaji16aq6bp5D9RxhXJcYLNN4W4zZIJgo6Hh1+4lCzNIcLfO
p1GeEFxyT1R1yvFQNWaoXrKjklW/jfOXy+nw99kGRM8wbGZsHnf4NPSEqJIMve0P
YKbtn4iyoeS+pBfUvQVE78gtAsfT3JBvTRM69MQqfzMulJPiCSte0E6fgPgZnihy
wxmpaUlLdH++1ZEMDMldMtb/jCpqDBZ6SDEDSfolCj6tbi8Q1TxMwiu5Qc0ovzgB
p1yoYAIUrBTP/2BNYBnEWTGb+Jv4SejH6fUX/PTPjXuyllsxmxS6V5GC8ZHHQfzp
VvVU24vUicreUxxsV2d1
=BN1Z
-----END PGP SIGNATURE-----

[ldc73]

I wanted to say That I like the project. I recently made a post about my idea for "TrueCoin" and someone pointed me to here.

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

as an idea it should do similar things

Reading the White Paper, but I am just not sure where I can find more Information about the logic or Foundation. also it there more Information about the proof of stake in Something?

Compared against "TrueCoin" do You think There is an argument that Qeditas issimilar?

[Bill White]

I wanted to say That I like the project. I recently made a post about my idea for "TrueCoin" and someone pointed me to here.

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

as an idea it should do similar things

Reading the White Paper, but I am just not sure where I can find more Information about the logic or Foundation. also it there more Information about the proof of stake in Something?

Compared against "TrueCoin" do You think There is an argument that Qeditas issimilar?

Thank you for your interest. Your "TrueCoin" idea does seem similar in spirit. One difference is that you describe TrueCoin as relying on the "useful Proof of Work" of proving mathematical theorems while Qeditas is planned to be (primarily) Proof of Stake. However, in Qeditas someone can increase their stake by proving theorems with bounties or by proving theorems others find useful (by collecting royalties). Perhaps this process can be seen as a simulation of a "useful Proof of Work."

The Qeditas White Paper provides an overview only. If you are interested in the details of the underlying logic (simple type theory), you can find those details in Chapter 7 of the Technical Documentation. The logic is the framework and users will need to publish a "theory" (primitives and axioms) to act as a mathematical foundation. (By default, the empty theory can be used, but this will have limited expressive power.)

The details of Proof of Stake are not fully described yet. Chapter 12 of the Technical Documentation should contain this information at some point, but even the single paragraph that currently comprises Chapter 12 is out-of-date and misleading. The best information can be found in the first half of Chapter 10. Also, Section 1.1 of Chapter 9 describes how coin-age is computed.

Here is a link to the Technical Documentation:

http://qeditas.org/qeditastechdoc.pdf

I hope this answers your questions. Honestly, it was not completely clear to me what you were asking, so please feel free to ask again if I have misinterpreted.

[ldc73]

reading the kinds of possible explanations you pointed to moved me to have questions about stake:

Three types Of possessions that can stake emerge:

1. unlocked
2. locked up rewards
3. locked up non-rewards

one: can you say what This separated camps is for? these "locked up" are all complicated. and What is the reason rewards are different behavior?

two: in 9.1.1 it seems that camps 1 & 2 each age according to some laws ONce they become "mature" -- and they become "mature" after 512 blocks. is it correct though that camp 3 (locked up non-rewards) has it that it matures in some 8 blocks? can you give a clue what is the reason for this very fast becoming "mature" here?  It seems to lack stability in principle since you possibly can stake every 8 Blocks with the same locked up non-reward?

three: in 10.1 the idea of "stake modifier" is being discussed there. it seems that at each block the stake modifier for the next 256 blocks are known, as well the fact the next 256 part is known. I Can project a problem. the locked up non-reward can be used to stake 8 blocks next and I can known the stake modifier for this next 8 blocks. now how to solve this problem?

[Bill White]

reading the kinds of possible explanations you pointed to moved me to have questions about stake:

Three types Of possessions that can stake emerge:

1. unlocked
2. locked up rewards
3. locked up non-rewards

one: can you say what This separated camps is for? these "locked up" are all complicated. and What is the reason rewards are different behavior?

two: in 9.1.1 it seems that camps 1 & 2 each age according to some laws ONce they become "mature" -- and they become "mature" after 512 blocks. is it correct though that camp 3 (locked up non-rewards) has it that it matures in some 8 blocks? can you give a clue what is the reason for this very fast becoming "mature" here?  It seems to lack stability in principle since you possibly can stake every 8 Blocks with the same locked up non-reward?

three: in 10.1 the idea of "stake modifier" is being discussed there. it seems that at each block the stake modifier for the next 256 blocks are known, as well the fact the next 256 part is known. I Can project a problem. the locked up non-reward can be used to stake 8 blocks next and I can known the stake modifier for this next 8 blocks. now how to solve this problem?

Currency units can be "locked" until a given block height for two reasons. First, block rewards should be unspendable for a certain amount of time, since a reorganization of the block chain might delete the reward. Second, locking assets allows people to trustlessly loan coins to be staked (since the "lock" in the obligation may have a different spending address than the address holding/staking the asset).

I considered only allowing locked assets to stake, but this presents a bootstrapping problem. At the beginning the ledger only has unlocked assets. This is why unlocked assets can stake. An alternative would be to only allow unlocked assets to stake if they are from the initial distribution.

The reason why locked rewards age slowly is that I noticed in simulations that block rewards can otherwise begin to quickly dominate the staking process.

Locked non-rewards are the main assets I expect to be staking. The short maturation time (8 blocks) and the fact that they immediately stake with their full coin-age reflects this intention. In effect, I expect the first few blocks to be staked by unlocked assets from the initial distribution and for these blocks to contain txs creating locked assets which should begin doing most of the staking at that point.

You are correct that the stake modifier is known for the next 256 blocks (and partially known for the 256 after that). I do not see an issue with locked assets. Even if the locked assets stake more often than other assets (as intended), the fact that they (and the resulting rewards) are locked for a significant number of future blocks should prevent attacks.

[ldc73]

three: in 10.1 the idea of "stake modifier" is being discussed there. it seems that at each block the stake modifier for the next 256 blocks are known, as well the fact the next 256 part is known. I Can project a problem. the locked up non-reward can be used to stake 8 blocks next and I can known the stake modifier for this next 8 blocks. now how to solve this problem?

You are correct that the stake modifier is known for the next 256 blocks (and partially known for the 256 after that). I do not see an issue with locked assets. Even if the locked assets stake more often than other assets (as intended), the fact that they (and the resulting rewards) are locked for a significant number of future blocks should prevent attacks.

the problem I mean is not solved. It is not just from the locks to oppose trusted -- the problem is Now combination:

The fact in 8 blocks time it can stake.

The stake modifier in 8 blocks, given the explanation, is as known.

This all means someone can to test and to realize If creating an locked will allow him IN 8 blocks with (to the time) proposal. If locked pattern will not allow him to stake, they can test other possible (according to a different address, still by him) will allow him works. for he can try as many as he wants to he finds the outcome will stake. this should be a serious consideration

[Bill White]

the problem I mean is not solved. It is not just from the locks to oppose trusted -- the problem is Now combination:

The fact in 8 blocks time it can stake.

The stake modifier in 8 blocks, given the explanation, is as known.

This all means someone can to test and to realize If creating an locked will allow him IN 8 blocks with (to the time) proposal. If locked pattern will not allow him to stake, they can test other possible (according to a different address, still by him) will allow him works. for he can try as many as he wants to he finds the outcome will stake. this should be a serious consideration

Oh, now I think I see what you mean, and you are correct. You are describing a "stake grinding" attack. I opened Qeditas up to this attack when I reduced the maturation age of locked non-rewards to 8 blocks. To avoid this attack, no asset should be able to stake until at least 512 blocks after its creation.

This will make passing through the bootstrapping phase (the first 512 blocks) difficult since there will need to be at least 512 distinct assets from the initial distribution attempting to stake. I only have approximately 10 such assets myself. Realistically, if there aren't sufficient participants for 512 assets to stake, then I suppose the mainnet should be delayed until there are. If there never are sufficient participants, then perhaps Qeditas will simply remain as a Proof of Concept implementation others can learn from.

None of this will prevent starting a testnet. On the testnet, I have decided to permit "fake endorsements" using a private key I hold. In this way, I can reallocate arbitrary coins on the testnet. My plan is to use this to give away (testnet) coins corresponding to the early Bitcoin block rewards. (To be clear: this is only for the testnet. Satoshi's complete portion of the Qeditas distribution on the mainnet will be available for Satoshi to claim.) In this way, it will be easy to ensure that there are over 512 assets staking when the testnet starts. I am still hopeful that a Qeditas testnet can be started sometime reasonably soon, though not hopeful enough to give an estimate. Finding out about this grinding attack makes me even more reluctant to give estimated dates.

[ldc73]

interesting

I am happy when you've agreed on the problem with the attack.

I hope further it goes out as helped and gives hit and energy for fighting It not disappointed.

[Bill White]

interesting

I am happy when you've agreed on the problem with the attack.

I hope further it goes out as helped and gives hit and energy for fighting It not disappointed.

It is definitely better to find these kinds of issues earlier rather than later. Thank you for having a close look and finding the issue. Qeditas can definitely benefit from having more pairs of eyes looking into it.

[Bill White]

The current state of Qeditas is as follows:

A testnet version (not yet released) is able to connect with peers (on a local network for the moment) and share the most important information, e.g., block headers, block deltas, and so on. Each attempt to run it has resulted in a fork within roughly the first 200 blocks, so there are definitely bugs. The debugging process is tedious and it is difficult to estimate how long it will take. Perhaps I will simply stop giving updates on this thread until there is a version that seems to run locally without forking. If and when that time should come, my plan is to release another alpha version (0.0.2) so that interested people can try the testnet. During this initial trial phase the testnet will probably be reset on a weekly basis.

[Bill White]

I am happy to confirm that Qeditas is now an IOHK project. The first post of this thread has been edited to reflect this. The code base can now be found on github: https://github.com/input-output-hk/qeditas. If you wish to collaborate on the Qeditas project, there is a contact page on the corresponding IOHK page: https://iohk.io/projects/qeditas/.

[ldc73]

there is a new thing for this? I do not a where to look for new   version.

[aliibrahim80]

I cloned the Qeditas source code from IOHK's github and have been using it to play with some ideas. Here is the most up-to-date branch of mine:

https://github.com/aliibrahim80/qeditas/tree/sha256hashval

In addition to the work I've done, I have merged in mariashka's modifications to the "mathdata" code. She verified the code in Coq and factored the ocaml code into three modules: logic, mathdata and checking. Her branch is here:

https://github.com/input-output-hk/qeditas/tree/verified-mathdata

I don't think it was ever pointed out on this thread, but there were problems with the initial distribution database. The balances appear to all be correct, but the wrong hashes were used to refer to assets. This propagated all the way up to the root of the initial ledger ctree. mariashka wrote code to fix this, and using this I got a fixed version. After making more changes (using only sha256 instead of sha256+ripemd160), I had to regenerate the database.  Here is a copy of the version of the database (about 1GB) with the initial ledger tree I am currently using:

https://mega.nz/#!JGx1VSwY!04XmXU0Zv0iye4Sa2LhSvp7ERh_HiJAKn_2IsQsYkN4

Here is a summary of the changes I have made so far:

The first thing I did was to add a proof-of-burn component to the consensus code. It is only simulated for now, but the idea is to sometimes burn some proof-of-work coins in order to embed the current block/state into a proof-of-work block chain. This would make sure someone could not privately create a long-range attack chain. This would also supply a source for "randomness" for the stake modifier. (The previous version of allowing stakers to choose bits for future stake modifiers seemed unsafe to me.)

I added some json support and added a "createtx" command that takes a representation of a tx in json and converts it to the internal representation.

One potentially major problem I found was that multiple threads could be calling the sha256 and ripemd160 code, and these could corrupt intermediate results (race conditions). I added locking that should avoid these race conditions.

In an effort to make things faster and safer, I changed the "hashval" type from being 160 bits (5 int32s) to 256 bits (8 int32s). These values are calculated using sha256, where previously the 160 bit hashvals were computed using sha256 followed by ripemd160. This change roughly halves the amount of hashing to be done and does seem to make the code noticably faster.  I also thought this would be safer since it's possible that using 160 bits would make the system vulnerable to a "birthday paradox" (finding a collision using only 2^80 tries). Since hashvals are used to identify objects and propositions, such collisions seem like they could cause serious problems. For example, someone could try to find a collision between two sets which can be demonstrated to be different. I added the explicit hashval for such identifiers to the Owns and Rights preassets and use these to identify the corresponding object or proposition instead of relying on the address (which is still 160 bits) where the asset is contained.

I completely removed the proof-of-storage component from the consensus algorithm, mainly because it was easier to delete it than try to understand it to be honest.

A commitment of the blockdelta (including the merkle root of txs and their signatures) were added to the blockheader. Surprisingly before there was no such commitment. Given a blockheader there was no way to identify a definite blockdelta that would correspond to it. If a blockdelta were supplied to a node that did not support the blockheader, then there would be no way to know if the header should be ignored or if the wrong blockdelta was supplied (perhaps as an attack).

In addition, the header now contains a hash of the signature of the previous block header (except for the genesis block). Again, this is to prevent attackers from supplying false signatures later in an effort to make previously valid blocks appear to be invalid.

Aside from minor bug fixes, the rest of the work had to do with trying to debug the networking code. Basically every message sent and received is logged in their own files now (in a binary form). This helps me with debugging when things go wrong in the network.

I like the idea for Qeditas, but the current state of the code is slow and has bugs. Fortunately, my impression is that most of the bugs are in parts of the code (e.g., the networking code) that do not correspond to the more important parts that have a corresponding Coq verification. The slowness of the code could probably be compensated for by significantly adjusting the average block time (e.g., from 10 minutes to 240 minutes -- 4 blocks a day). A very slow block time like this would give people time to react to problems if they appeared while the system is running. Also, a slow block time would mean more information could be burned into a proof-of-work chains without it rising to a level their chain might consider "spam."

I am not sure how much of my changes IOHK wants to take, but of course they are welcome to pick and choose, take all or none. Since I'm making major changes, it might make more sense for me to create a renamed/rebranded independent fork. I am open to discussion about either having Qeditas adopt my changes or renaming.

[ldc73]

good

enough incentive to see more usable progress being shown on This experiment

in addition to represents An interesting application

making The bitcoin cash spinoff shows consequences that spinoff consensus networks can continue and can conceive of financial interest

[aliibrahim80]

I created a Qeditas fork called Dalilcoin. The testnet is now running and the mainnet should start in a few weeks. Updates and discussion will be at the dalilcoin subreddit.

The part of theorem proving is mostly the same as Qeditas. I did disable publications of theories and signatures since this adds a layer of complexity and is not well tested.

The consensus algorithm now uses Proof of Burn combined with Proof of Stake. Proof of burn means burning litecoins while putting block information about the Dalilcoin chain into the Litecoin tx. Since the Dalilcoin code is slow, I decided to make block times very slow. On average there should be 4 blocks per day -- a 6 hour block time.

The initial distribution of Dalilcoin fraenks is the same as the Qeditas snapshot from 2015. In order to prevent the initial distribution from eclipsing newly staked Dalilcoin fraenks, and to give a sense of urgency about claiming the airdrop, the amount of the unclaimed initial distribution will be halved roughly every 6 months. If you had 1 bitcoin in an address at the time of the Qeditas snapshot, then you have 1 Dalilcoin fraenk. In six months, if unclaimed, you will only be able to claim 0.5 Dalilcoin fraenks, and so on.

The Qeditas thread seemed like the best place to announce this, but further discussion should be moved to the dalilcoin subreddit.

[aliibrahim80]

It is not clear if the last two posts were asking about Qeditas or Dalilcoin. Dalilcoin is definitely not an ICO. The initial distribution is an airdrop determined by the Qeditas snapshot (see the original post of this thread for details), and it was my understanding Qeditas was also not going to have an ICO (but that is not my decision to make).

If you are interested in purchasing Dalilcoin fraenks, find someone who held bitcoin at the time of the snapshot and make an offer to buy their Dalilcoin fraenks from the airdrop.

The Dalilcoin mainnet is launching today (April 8, 2018) when Litecoin reaches block height 1400000. Discussion about Dalilcoin should be moved to the dalilcoin subreddit. I am only rarely checking bitcointalk.

Edit: The Dalilcoin mainnet is now live. A link to the github repo is on the dalilcoin subreddit.

[tootiterko]

When will i be able to sell tokens  bought during ICO on stock exchanges?