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

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

[1715031051]

1715031051

[1715031051]

1715031051

[1715031051]

1715031051

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