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

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