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

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.

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?

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.

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


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

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:


In principle another node should be able to get the data from a peer:
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.

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?

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.

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.

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.

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.

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?

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.

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.

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?

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

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.

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:


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:


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.

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.

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.