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

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.

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:


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.

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.

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.

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.

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.

There is now such a help command.


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.

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:


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

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:


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

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

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.

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.

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

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.

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.

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:


lol

good to see progress on qeditas. good luck.

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.


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.

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


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

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

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.