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

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

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

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

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

I added some ocaml code to the qeditas git repo:

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

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

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

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

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

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

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

Qeditas endorsement
endorse

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

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

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

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

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


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

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

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


They can also be viewed using gitweb here:

qeditas.org/gitweb

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

Same for me.

Edit: But cloning does seem to work. Strange.

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

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

I created a fork of Egal to support Qeditas.

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

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

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

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

http://mathgate.info/egalrelease.php

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

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

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

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

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

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

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

So a bit like CLAM ?

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

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

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

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

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

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


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

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

about selling claims you wrote this:


and:


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

Great!


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

it's interesting.

will look this later.

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

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

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

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

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


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