History

On February 10th 2015 David Kaloper-Meršinjak and Hannes Mehnert launched (read also Amir's description) our bug bounty program in the form of our Bitcoin Piñata MirageOS unikernel. Thanks again to IPredator for both hosting our services and lending us the 10 Bitcoins! We analysed a bit more in depth after running it for five months. Mindy recently wrote about whacking the Bitcoin Piñata.

On March 18th 2018, after more than three years, IPredator, the lender of the Bitcoins,…

History

On February 10th 2015 David Kaloper-Meršinjak and Hannes Mehnert launched (read also Amir's description) our bug bounty program in the form of our Bitcoin Piñata MirageOS unikernel. Thanks again to IPredator for both hosting our services and lending us the 10 Bitcoins! We analysed a bit more in depth after running it for five months. Mindy recently wrote about whacking the Bitcoin Piñata.

On March 18th 2018, after more than three years, IPredator, the lender of the Bitcoins, repurposed the 10 Bitcoins for other projects. Initially, we thought that the Piñata would maybe run for a month or two, but IPredator, David, and I decided to keep it running. The update of the Piñata's bounty is a good opportunity to reflect on the project.

The 10 Bitcoin in the Piñata were fluctuating in price over time, at peak worth 165000€.

From the start of the Piñata project, we published the source code, the virtual machine image, and the versions of the used libraries in a git repository. Everybody could develop their exploits locally before launching them against our Piñata. The Piñata provides TLS endpoints, which require private keys and certificates. These are generated by the Piñata at startup, and the secret for the Bitcoin wallet is provided as a command line argument.

Initially the Piñata was deployed on a Linux/Xen machine, later it was migrated to a FreeBSD host using BHyve and VirtIO with solo5, and in December 2017 it was migrated to native BHyve (using ukvm-bin and solo5). We also changed the Piñata code to accomodate for updates, such as the MirageOS 3.0 release, and the discontinuation of floating point numbers for timestamps (asn1-combinators 0.2.0, x509 0.6.0, tls 0.9.0).

Motivation

We built the Piñata for many purposes: to attract security professionals to evaluate our from-scratch developed TLS stack, to gather empirical data for our Usenix Security 15 paper, and as an improvement to current bug bounty programs.

Most bug bounty programs require communication via forms and long wait times for human experts to evaluate the potential bug. This evaluation is subjective, intransparent, and often requires signing of non-disclosure agreements (NDA), even before the evaluation starts.

Our Piñata automates these parts, getting rid of wait times and NDAs. To get the private wallet key that holds the bounty, you need to successfully establish an authenticated TLS session or find a flaw elsewhere in the stack, which allows to read arbitrary memory. Everyone can track transactions of the blockchain and see if the wallet still contains the bounty.

Of course, the Piñata can't prove that our stack is secure, and it can't prove that the access to the wallet is actually inside. But trust us, it is!

Observations

I still remember vividly the first nights in February 2015, being so nervous that I woke up every two hours and checked the blockchain. Did the Piñata still have the Bitcoins? I was familiar with the code of the Piñata and was afraid there might be a bug which allows to bypass authentication or leak the private key. So far, this doesn't seem to be the case.

In April 2016 we stumbled upon an information disclosure in the virtual network device driver for Xen in MirageOS. Given enough bandwidth, this could have been used to access the private wallet key. We upgraded the Piñata and released the MirageOS Security Advisory 00.

We analysed the Piñata's access logs to the and bucketed them into website traffic and bounty connections. We are still wondering what happened in July 2015 and July 2017 where the graph shows spikes. Could it be a presentation mentioning the Piñata, or a new automated tool which tests for TLS vulnerabilities, or an increase in market price for Bitcoins?

The cumulative graph shows that more than 500,000 accesses to the Piñata website, and more than 150,000 attempts at connecting to the Piñata bounty.

You can short-circuit the client and server Piñata endpoint and observe the private wallet key being transferred on your computer, TLS encrypted with the secret exchanged by client and server, using socat -x TCP:ownme.ipredator.se:10000 TCP:ownme.ipredator.se:10002.

If you attempted to exploit the Piñata, please let us know what you tried! Via

hannesm@mastodon.social or a GitHub issue.

Since the start of 2018 we are developing robust software and systems at robur. If you like our work and want to support us with donations or development contracts, please get in touch with team@robur.io. Robur is a project of the German non-profit Center for the cultivation of technology. Donations to robur are tax-deductible in Europe.

@yomimono or @hannesm surely know if people have tried crowbar on the BTC Piñata. – @kensan@mastodon.social

tl;dr - yes, and it seems that ocaml-x509 is not trivially easy to trick.

Background

The Bitcoin Piñata

In 2015 David Kaloper-Mersinjak and Hannes Mehnert released ocaml-tls, an implementation of TLS (formerly known as SSL) written fully in OCaml. A full writeup of the stack is available in their Usenix Security 2015 paper, and as a series of blog posts on mirage.io. To acc…

@yomimono or @hannesm surely know if people have tried crowbar on the BTC Piñata. – @kensan@mastodon.social

tl;dr - yes, and it seems that ocaml-x509 is not trivially easy to trick.

Background

The Bitcoin Piñata

In 2015 David Kaloper-Mersinjak and Hannes Mehnert released ocaml-tls, an implementation of TLS (formerly known as SSL) written fully in OCaml. A full writeup of the stack is available in their Usenix Security 2015 paper, and as a series of blog posts on mirage.io. To accompany the release they also deployed a fully-automated bug bounty for the security stack – the bitcoin piñata.

The piñata will establish TLS connections only with endpoints presenting a certificate signed by its own, undisclosed certificate authority, but allows an attacker to easily listen to the encrypted traffic. The piñata always sends the same plaintext in such a connection: the private key to a wallet containing approximately 10 bitcoin. If the attacker can decrypt the ciphertext, or trick the piñata into negotiating a TLS connection with another host and disclosing the key, the information (and therefore the money) is theirs.

Crowbar

Crowbar is a library for writing tests. It combines a property-based API (like QuickCheck) with a coverage-driven generator of test cases (like the fuzzer American Fuzzy Lop). Crowbar tries to find counterexamples to stated properties by prioritizing the generation of test cases which touch more code. It is very good at finding counterexamples.

Testing ocaml-x509

TLS connections are usually authenticated via X509 certificates. ocaml-tls uses ocaml-x509 for this purpose, which is written as a standalone library. There is a clear separation of concerns between ocaml-x509 and ocaml-tls, and a straightforward API for certificate operations in ocaml-x509; both features help tremendously in writing tests for certificate handling.

Stating Tests

Of the possible operations in X509, the most interesting in the context of the BTC piñata are those related to certificate validation. We expect the piñata to check whether a certificate provided by the attacker has a trust chain to any CA it is aware of. This suggests a property we might want to find a counterexample to: * certificates signed by CA m will not be judged valid unless CA m is provided as a trust anchor.

If we can find a counterexample, we’re well on the way to getting the piñata to negotiate a TLS connection with an endpoint presenting a certificate not signed by the CA it generated at boot time.

Generating Certificates

In order to test this property, we need to be able to call X509.Validation.verify_chain_of_trust with something of type X509.CA.t (representing the certificate authority; for the piñata, this is a known and trusted value) and something of type X509.t (representing the certificate; for the piñata, this is presented by the remote host of the TLS connection).

For our tests, we’ll allow Crowbar’s random generators to specify most parts of the certificate, with the important exception of the key material – generating this randomly will cause the execution of each test to be very slow, and it’s not the goal of this testing to try to brute-force the key of our test CA.

The generators for certificates are largely automatically created by ppx_deriving_crowbar, although some manual help is needed to include generators for data types in dependencies used by X509 (and generators for their dependencies and dependencies’ dependencies). A maximalist interpretation can be seen in this iteration of the tests, which uses ppx_deriving to automatically generate equality tests and pretty-printers as well as generators for many of the relevant types.

Increasing Stability

Since we want all randomness in the test execution to be driven by the fuzzer, it’s important to remove other sources of entropy in the code execution. Luckily, ocaml-x509 and the cryptography library underneath it, nocrypto, were written considerately, and there is a facility for providing a constant seed to the pseudorandom number generator. Using the same seed across all test runs removes noise from the measurement of coverage between different test runs.

Running Tests

Tests built with the Crowbar library need to be run via afl-fuzz. To automatically launch afl-fuzz in a manner that uses all available computing resources and reports failures as quickly as possible, we used ocaml-bun. You can see the results of such a test run in Travis CI here.

The number of executions per second is appallingly low for OCaml native code running in afl-fuzz (cryptography is hard!); to compensate I ran this code over a weekend locally instead of briefly on whatever free resources Travis would give me.

Results

Many certificates with silly sets of extensions were generated:

`Priv_key_period (`Not_after (0066-02-08 09:28:58 +00:00))
`Subject_alt_name ([`EDI_party (((Some "mmmmmmmmmxmmmmmmmmmmmmmrs\146n\020sh&&&&&&&&&&.&&&'&&t\014the&w[rn Bx WrV"),
                                 "c\130 s'\186\186\186\186\186\186\186Te@rica tbiitx WrVc\127 s', or soTe@wos\127\141\018o\139\255repeeseb u"));
                                                      `Other ((0.32, "t \228ay of\015t"))])
                                                      `Priv_key_period (`Not_after (1088-06-01 06:08:11 +00:00))

`CRL_distribution_points ([((Some `Relative ([`Generation ("EEElE$EE \127\255E'EEElEEEYE$EE\151ai4RgEbEE\151a\214\214\214\235\214\214\214\214bnt\225")
                                               ])),
                            None,
                            (Some [`Surname ("~~~~~~~~~~EEEYE$EEB\127\255E'EEElEEEYE$EE\151a\214\214\214\235\214\214\214\214\214\214\214\214\214\214\214\214\198\214\214\214\215\214\214\214\214 \214")
                                    ]))
                            ])

`Certificate_issuer ([])
`Policies ([`Something (0.36.3703494230495416691)])`Certificate_issuer (
[])
`Subject_alt_name ([`Other ((2.2839008736452811263, "\140abbi\131\129\b',"));
                     `URI ("'[cay@")])

As we hoped, a certificate signed by the wrong CA with these sets of extensions don’t validate. ocaml-x509 isn’t tricked by arbitrarily ridiculous sets of extensions in a signed certificate, and I didn’t manage to steal any bitcoin.

Future and Related Work

None of this work targets ocaml-tls or any of the more general parts of the stack run by the piñata. Notably, neither tcpip which provides the TCP, IPv4, and Ethernet implementations, nor any of the hypervisor-specific virtual network devices, are examined by this work. (This includes mirage-net-xen, the originator of the only MirageOS security advisory to date.) With releases of all tooling used to test ocaml-x509 available via opam, this is easier to rectify than it previously was!

Acknowledgements

Thanks to OCaml Labs for funding this work, IPredator for stuffing the piñata, and robur.io for future and continuing work in building resilient systems.

As we are preparing to work on the Tezos Protocol, we’re still actively keeping the pace on the block explorer TZScan.io, adding cool information for baking accounts. We’d like to allow people to see who is contributing to the network and to understand the distribution of rolls, rights, etc.

For starters, we are showing the roll balance used for baking in the current cycle and the rolls history of a baker.

http://tzscan.io/tz1MqVR7hnZwH1FoQ7swjamanNxrXtNVAQ7v?default=baking

Enjoy, mo…

As we are preparing to work on the Tezos Protocol, we’re still actively keeping the pace on the block explorer TZScan.io, adding cool information for baking accounts. We’d like to allow people to see who is contributing to the network and to understand the distribution of rolls, rights, etc.

For starters, we are showing the roll balance used for baking in the current cycle and the rolls history of a baker.

http://tzscan.io/tz1MqVR7hnZwH1FoQ7swjamanNxrXtNVAQ7v?default=baking

Enjoy, more to come in the next weeks!

O(1) Labs is a small, well-funded startup aiming to develop the first cryptocurrency protocol that can deliver on the promise of supporting real-world applications and widespread use. Our team is based in San Francisco, and we are funded by top investors (including Polychain, Metastable, and Naval Ravikant).

Cryptocurrency is a domain where correctness really counts. As such, a cornerstone of our approach is a focus on building reliable software through the use of statically-typed functional pr…

O(1) Labs is a small, well-funded startup aiming to develop the first cryptocurrency protocol that can deliver on the promise of supporting real-world applications and widespread use. Our team is based in San Francisco, and we are funded by top investors (including Polychain, Metastable, and Naval Ravikant).

Cryptocurrency is a domain where correctness really counts. As such, a cornerstone of our approach is a focus on building reliable software through the use of statically-typed functional programming languages. This is reflected in our OCaml codebase and style of structuring code around DSLs, as well as in the design of the smart-contracts platform we’re developing.

There is no need to have prior experience in cryptography, and we're hiring engineers to work on a bunch of exciting projects including:

• Our OCaml DSL for writing zk-SNARKs (a cryptographic primitive for certified computation).
• The design of a virtual machine and higher-level languages for smart contracts (there a lot of interesting challenges here since the VM has to be efficient inside SNARKs).
• Working on the core networking, cryptography, and reliability aspects of the protocol.

This is a chance to join a small, collaborative team and have a ton of independence while working on fascinating cross-disciplinary problems in computing. We also offer competitive compensation both in salary and equity, as well as top-of-the-market benefits.

Ideal candidates will be interested in any of:

• functional programming
• programming language theory
• security
• distributed systems
• cryptography
• cryptocurrency

There are no hard requirements and we’re more interested in learning about your individual background.

We are committed to building a diverse, inclusive company. People of color, LGBTQ individuals, women, and people with disabilities are strongly encouraged to apply.

Get information on how to apply for this position.

In some occasions, using the Coq proof assistant stops resembling a normal software development activity, and becomes more similar to puzzle solving.

Similarly to the excellent video games of the Zachtronics studio (TIS-100, SpaceChem, …), the system provides you with puzzles where obstacles have to be side-stepped using a fair amount of tricks and ingenuity, and finally solving the problem has often no other utility than the satisfaction of having completed it.

In this blog-post, I would li…

In some occasions, using the Coq proof assistant stops resembling a normal software development activity, and becomes more similar to puzzle solving.

Similarly to the excellent video games of the Zachtronics studio (TIS-100, SpaceChem, …), the system provides you with puzzles where obstacles have to be side-stepped using a fair amount of tricks and ingenuity, and finally solving the problem has often no other utility than the satisfaction of having completed it.

In this blog-post, I would like to present what I think is one such situation. What the puzzle is, how we solved it, and why you shouldn’t probably do that if you like spending your time in a useful manner.

Prelude

A few months ago, I was wondering if it was possible to count the number of exists in front of the goal, using Ltac (the tactic language of Coq). That is, write a tactic that would for example produce 3 on the following goal:

====================================
  exists x y z : nat, x + y = z

“That’s easy”, I thought. “I will just write a recursive function in Ltac”. First, we check that we can get the body of the exists by matching on the goal – this seems to work as expected:

Goal exists x y z : nat, x + y = z.
  match goal with |- exists x, ?G' => idtac G' end.
  (* Prints (exists y z : nat, x + y = z) *)

Then, we write a tactic to do this recursively, walking down the type of the goal until there is no exists in front of it.

Ltac count_exists_naive_aux G n :=
  lazymatch G with
  | exists x, ?G' => count_exists_naive_aux G' (S n)
  | _ => constr:(n)
  end.

Ltac count_exists_naive :=
  match goal with |- ?G =>
    let x := count_exists_naive_aux G 0 in
    pose x
  end.

But this does not work, and fails with the error below. It seems Ltac does not handle terms with free variables.

Error: Must evaluate to a closed term
offending expression:
G
this is an object of type constr_under_binders

At this point, the reasonable choice would be to give up, write specialized versions of the tactic for 0 to 7 exists (who has goals with more than 7 exists anyway?), and wait for one of the successors of Ltac (Ltac2 maybe?) to come up without these limitations. Unreasonably, I sought the help of Cyprien Mangin, my local puzzle game and Coq expert, and we came up with the following solution.

A first idea: “destruct”ing the goal

A first idea: one thing that we can do iteratively on a exists x y z ... term is splitting it using destruct – if we have it as an hypothesis. For example:

(* Goal:
   H : exists x y z : nat, x + y = z
   ====================================
     True
*)

  Ltac count_in_hyp H acc kont :=
    lazymatch type of H with
    | exists _, _ => destruct H as [? H]; count_in_hyp H (S acc) kont
    | _ => kont acc
    end.

  count_in_hyp H 0 ltac:(fun n => pose n).

(* Goal:
   x, x0, x1 : nat
   H : x + x0 = x1
   n := 3 : nat
   ====================================
     True
*)

Notice we had to do the “standard trick” of writing the tactic in continuation passing style (using kont here as a continuation to return the number of exists). This is required since a Ltac tactic cannot do side-effects on the goal (here, destruct) and at the same time return a term.

Now, we want to count the number of exists in the goal, not in an hypothesis. How could we turn the goal into an hypothesis – after all, these exists are something we need to provide, not something we get. In fact, it is possible to get a sub-goal with an hypothesis of the same type as the goal – simply, this sub-goal won’t be much relevant for proving the goal. We define the following helper lemma:

Definition helper_lemma : forall P Q, (P -> True) -> Q -> Q :=
  fun P Q _ Q_proof => Q_proof.

Applying this lemma produces an extra sub-goal with an hypothesis of type P. Notice how the proof term corresponding to this sub-goal is completely discarded in the definition of helper_lemma: this sub-goal is only relevant for our Ltac tricks. To get a sub-goal which allows destructing the exists in front of the goal, we do:

(* Goal:
   ====================================
     exists x y z : nat, x + y = z
*)

  match goal with |- ?G => apply (helper_lemma G) end;
  [ intro H | ].

(* Goal 1:
   H : exists x y z : nat, x + y = z
   ====================================
     True

   Goal 2:
   ====================================
     exists x y z : nat, x + y = z
*)

  count_in_hyp H 0 ltac:(fun n => pose n).

(* Goal 1:
   x, x0, x1 : nat
   H : x + x0 = x1
   n := 3 : nat
   ====================================
     True

   Goal 2:
   ====================================
     exists x y z : nat, x + y = z
*)

Second idea: communicating through evars

We are not done yet: we can count the number of exists in the first – dummy – sub-goal, but we need to transmit this information to the main sub-goal.

The second idea is to propagate this information using an “evar”. An evar is a Coq term representing a “hole”: its definition is not known yet, and will be given later in the proof. This discipline only exists when constructing the proof: evars do not appear in the proof term, where everything happens in order.

The idea here is to introduce an evar before applying our auxiliary helper_lemma. This evar will appear in the context of both sub-goals introduced by the lemma: in the first one, we can “instantiate” it (ie. set its definition) with the number of exists computed, and use it in the second sub-goal.

This gives us:

  evar (n : nat).

(* Goal:
   n := ?n : nat
   ====================================
     exists x y z : nat, x + y = z
*)

  match goal with |- ?G => apply (helper_lemma G) end;
  [ intro H;
    let x := count_in_hyp H 0 in
    instantiate (n := x);
    exact I
  | ].

(* Goal:
   n := 3 : nat
   ====================================
     exists x y z : nat, x + y = z
*)

Hurray! It works. We can wrap this in a reusable tactic:

Ltac count_in_ty G kont :=
  let n := fresh "n" in
  evar (n : nat);
  apply (helper_lemma G); [
    let H := fresh in
    intro H; count_in_hyp H 0 ltac:(fun x => instantiate (n := x));
    exact I
  | kont n ].

Third idea: cleaning up

The tactic above indeed works, and successfully counts the number of exists in the goal. However, it is still a bit messy. In particular, the trick of using a helper lemma shows up in the proof term. Using Show Proof after running count_in_ty on the goal yields:

(let n := 3 in
 helper_lemma (exists x y z : nat, x + y = z) (exists x y z : nat, x + y = z)
   (fun H : exists x y z : nat, x + y = z =>
    match H with
    | ex_intro _ x (ex_intro _ x0 (ex_intro _ _ _)) => I
    end) ?Goal)

This is mostly noise! Indeed, helper_lemma P Q H1 H2 is equivalent to simply H2 – we only use the lemma for our Ltac tricks, and ideally, this should not appear in the final proof term. We can do better. The third idea is to isolate the messy proof term containing helper_lemma, and simplify it after it has been produced by counting the exists. Isolating the proof term can be achieved with the following pattern:

  let n := constr:(ltac:(mytactic) : nat) in
  ...

constr:() and ltac:() are both quotations: the first one indicates that its contents must be parsed as a Coq term, and the second one that it must be parsed as a tactic. Their combination above indicates that we want to produce a term (of type nat), and to run the tactic mytactic to produce it.

mytactic will run on a goal of type nat, and the proof term it produces by proving this goal will become the definition of n. Let us replace mytactic by our counting tactic (its continuation being simply exact to prove the nat goal using the result of the count):

(* Goal:
   ====================================
     exists x y z : nat, x + y = z
*)

  match goal with |- ?G =>
    let n := constr:(ltac:(count_in_ty G ltac:(fun n => exact n)) : nat) in
    pose n
  end.

(* Goal:
   n := ((let n := 3 in
          helper_lemma (exists x y z : nat, x + y = z) nat
            (fun H : exists x y z : nat, x + y = z =>
             match H with
             | ex_intro _ x (ex_intro _ x0 (ex_intro _ _ _)) => I
             end) n)
         :
         nat) : nat
   ============================
   exists x y z : nat, x + y = z
*)

The messy proof-term is now part of the definition. We now just have to simplify it, e.g. using eval cbv in n:

  match goal with |- ?G =>
    let n := constr:(ltac:(count_in_ty G ltac:(fun n => exact n)) : nat) in
    let n := (eval cbv in n) in
    pose n
  end.

(* Goal:
   n := 3 : nat
   ============================
   exists x y z : nat, x + y = z
*)

  Show Proof.

(* Prints: (let n := 3 in ?Goal) *)

And there you have it! Here is the whole implementation of count_exists:

Ltac count_in_hyp H acc kont :=
  lazymatch type of H with
  | exists _, _ => destruct H as [? H]; count_in_hyp H (S acc) kont
  | _ => kont acc
  end.

Definition helper_lemma : forall P Q, (P -> True) -> Q -> Q :=
  fun P Q _ Q_proof => Q_proof.

Ltac count_in_ty G kont :=
  let n := fresh "n" in
  evar (n : nat);
  apply (helper_lemma G); [
    let H := fresh in
    intro H; count_in_hyp H 0 ltac:(fun x => instantiate (n := x));
    exact I
  | kont n ].

Ltac count_exists kont :=
  match goal with |- ?G =>
    let n := constr:(ltac:(count_in_ty G ltac:(fun n => exact n)) : nat) in
    let n := (eval cbv in n) in
    kont n
  end.

This time of the year is, just like Christmas time, a time for laughs and magic… although the magic we are talking about, in the OCaml community, is not exactly nice, nor beautiful. Let’s say that we are somehow akin to many religions: we know magic does exist , but that it is satanic and shouldn’t be introduced to children.

Introducing Just The Right Time (JTRT)

Let me first introduce you to the concept of ‘Just The Right Time’ [1]. JTRT is somehow a ‘Just In…

This time of the year is, just like Christmas time, a time for laughs and magic… although the magic we are talking about, in the OCaml community, is not exactly nice, nor beautiful. Let’s say that we are somehow akin to many religions: we know magic does exist , but that it is satanic and shouldn’t be introduced to children.

Introducing Just The Right Time (JTRT)

Let me first introduce you to the concept of ‘Just The Right Time’ [1]. JTRT is somehow a ‘Just In Time’ compiler, but one that runs at the right time, not at some random moment decided by a contrived heuristic.

How does the compiler know when that specific good moment occurs? Well, he doesn’t, and that’s the point: you certainly know far better. In the OCaml world, we like good performances, like any other, but we prefer predictable ones to performances that may sometimes be awesome, and sometimes really slow. And we are ready to trade off some annotations for better predictability (or is it just me trying to give the impression that my opinion is everyone’s opinion…). Don’t forget that OCaml is a compiled language; hence the average generated code is good enough. Runtime compilation only matters for some subtle situations where a patterns gets repeated a lot, and you don’t know about that pattern before receiving some inputs.

Of course the tradeoff wouldn’t be the same in Javascript if you had to write something like that to get your code to perform decently.

function fact(n) {
   "compile this";
   if (n == 0) {
      "compile this too";
      return 1
   } else {
      "Yes, I really want to compile that";
      return (n * fact(n - 1););
   }
 }

The magical ‘this_is_the_right_time’ function

There are already nice tools for doing that in OCaml. In particular, you should look at metaocaml, which is an extension of the language that has been maintained for years. But it requires you to think a bit about what your program is doing and add a few types, here and there.

Fortunately, today is the day you may want to try this ugly weekend hack instead.

To add a bit of context, let’s say there are 1/ the Dirty Little Tricks, and 2/ the Other Kind of Ugly Hacks. We are presenting one of the latter; the kind of hacks for which you are both ashamed and a bit proud (but you should really be a lot more ashamed). I’ve made quite a few of those, and this one would probably rank well among the top 5 (and I’m deeply sorry about the other ones that are still in production somewhere…).

This is composed of two parts: a small compiler patch, and a runtime library. That library only exposes the following single function:

val this_is_the_right_time : 'a -> 'a

Let’s take an example:

let f x =
  let y = x + x in
  let g z = z * y in
  g

let multiply_by_six = f 3

You can ‘optimize’ it by changing it to:

let f x =
  let y = x + x in
  let g z = z * y in
  g

let multiply_by_six = this_is_the_right_time (f 3)

That’s all. By stating that this is the right time, you told the compiler to take that function and do its magic on it.

How the f**k does that work?!

The compiler patch is quite simple. It adds to every function some annotation to allow the compiler to know enough things about it. (It is annotated with its representation in the Flambda IR.) This is just a partial dump of the compiler memory state when transforming the Flambda IR to clambda. I tried to do it in some more ‘disciplined’ way (it used some magic to traverse the compiler internal memory representation to create a static version of it in the binary), but ‘ld’ was not so happy linking a ~500MB binary. So I went the ‘marshal’ way.

This now means that at runtime the program can find the representation of the closures. To give an example of the kind of code you really shouldn’t write, here is the magic invocation to retrieve that representation:

 let extract_representation_from_closure (value:'a)
                                 : Flambda.set_of_closures =
   let obj = Obj.repr value in
   let size = Obj.size obj in
   let id = Obj.obj (Obj.field obj (size - 2)) in
   let marshalled = Obj.field obj (size - 1) in
   (Marshal.from_string marshalled 0).(id)

With that, we now know the layout of the closure and we can extract all the variables that it binds. We can further inspect the value of those bound variables, and build an IR representation for them. That’s the nice thing about having an untyped IR, you can produce some even when you lost the types. It will just probably be quite wrong, but who cares…

Now that we know everything about our closure, we can rebuild it, and so will we. As we can’t statically build a non-closed function (the flambda IR happens after closure conversion), we will instead build a closed function that allocates the closure for us. For our example, it would look like this:

 let build_my_closure previous_version_of_the_closure =
   let closure_field_y = previous_version_of_the_closure.y in
   fun z -> z * 6 (* closure_field_y * closure_field_y *)

In that case the function that we are building is closed, so we don’t need the old closure to extract its field. But this shows the generic pattern. This would be used like that:

 let this_is_the_right_time optimize_this =
   let ir_version = extract_representation_from_closure optimize_this in
   let build_my_closure = magic_building_function ir_version in
   build_my_closure optimize_this

I won’t go too much into the details of the ‘magic_building_function’, because it would be quite tedious. Let’s just say that it is using mechanisms provided for the native toplevel of OCaml.

A more sensible example

To finish on something a bit more interesting than ‘time_6’, let’s suppose that we designed a super nice language whose AST and evaluator are:

 type expr =
 | Add of expr * expr
 | Const of int
 | Var

let rec eval_expr expr x =
  match expr with
  | Add (e1, e2) -> eval_expr e1 x + eval_expr e2 x
  | Const i -> i
  | Var -> x

But we want to optimize it a bit, and hence wrote a super powerful pass:

 let rec optimize expr =
   match expr with
   | Add (Const n1, Add (e, Const n2)) -> Add (Const (n1 + n2), optimize e)
   | Add (e1, e2) -> Add (optimize e1, optimize e2)
   | _ -> expr

The user writes some expression, that gets parsed to Add (Const 11, Add (Var, Const 22)), it goes through optimizing and results in Add (Const 33, Var). Then you find that this looks like the right time.

let optimized =
   this_is_the_right_time 
        (fun x -> (eval_expr (optimize user_ast) x))

Annnnd… nothing happens. The reason being that there is no way to distinguish between mutable and immutable values at runtime, hence the safe assumption is to assume that everything is mutable, which limits optimizations a lot. So let’s enable the ‘special’ mode:

incorrect_mode := true

And MAGIC happens! The code that gets spitted out is exactly what we want (that is fun x -> 33 + x).

Conclusion

Just so that you know, I don’t really recommend using it. It’s buggy, and many details are left unresolved (I suspect that the names you would come up for that kind of details would often sound like ‘segfault’). Flambda was not designed to be used that way. In particular, there are some invariants that must be maintained, like the uniqueness of variables and functions… that we completely disregarded. That lead to some ‘funny’ behaviors (like ‘power 2 8′ returning 512…). It is possible to do that correctly, but that would require far more than a few hours’ hacking. This might be a lot easier with the upcoming version of Flambda.

So this is far from ready, and it’s not going to be anytime soon (supposing that this is a good idea, which I’m still not convinced it is).

But if you still want to play with it: the sources are available.

[1] Not that it exists in real-world.

Jane Street is a proprietary quantitative trading firm, focusing primarily on trading equities and equity derivatives. We use innovative technology, a scientific approach, and a deep understanding of markets to stay successful in our highly competitive field. We operate around the clock and around the globe, employing over 500 people in offices in New York, London and Hong Kong.

The markets in which we trade change rapidly, but our intellectual approach changes faster still. Every day, we have …

Jane Street is a proprietary quantitative trading firm, focusing primarily on trading equities and equity derivatives. We use innovative technology, a scientific approach, and a deep understanding of markets to stay successful in our highly competitive field. We operate around the clock and around the globe, employing over 500 people in offices in New York, London and Hong Kong.

The markets in which we trade change rapidly, but our intellectual approach changes faster still. Every day, we have new problems to solve and new theories to test. Our entrepreneurial culture is driven by our talented team of traders and programmers. At Jane Street, we don't come to work wanting to leave. We come to work excited to test new theories, have thought-provoking discussions, and maybe sneak in a game of ping-pong or two. Keeping our culture casual and our employees happy is of paramount importance to us.

As Jane Street grows, the quality of the development tools we use matters more and more. We increasingly work on the OCaml compiler itself: adding useful language features, fine-tuning the type system and improving the performance of the generated code. Alongside this, we also work on the surrounding toolchain, developing new tools for profiling, debugging, documentation and build automation.

We're looking to hire a developer with experience working on compilers to join us. That experience might be from working on a production compiler in industry or from working on research compilers in an academic setting. No previous experience with OCaml or functional programming languages is required.

We’re looking for candidates for both our London and New York offices. Benefits and compensation are highly competitive.

Software Developer

Jane Street is a proprietary quantitative trading firm, focusing primarily on trading equities and equity derivatives. We use innovative technology, a scientific approach, and a deep understanding of markets to stay successful in our highly competitive field. We operate around the clock and around the globe, employing over 500 people in offices in New York, London and Hong Kong.

The markets in which we trade change rapidly, but our intellectual approach changes faster still…

Software Developer

Jane Street is a proprietary quantitative trading firm, focusing primarily on trading equities and equity derivatives. We use innovative technology, a scientific approach, and a deep understanding of markets to stay successful in our highly competitive field. We operate around the clock and around the globe, employing over 500 people in offices in New York, London and Hong Kong.

The markets in which we trade change rapidly, but our intellectual approach changes faster still. Every day, we have new problems to solve and new theories to test. Our entrepreneurial culture is driven by our talented team of traders and programmers. At Jane Street, we don't come to work wanting to leave. We come to work excited to test new theories, have thought-provoking discussions, and maybe sneak in a game of ping-pong or two. Keeping our culture casual and our employees happy is of paramount importance to us.

We are looking to hire great software developers with an interest in functional programming. OCaml, a statically typed functional programming language with similarities to Haskell, Scheme, Erlang, F# and SML, is our language of choice. We've got the largest team of OCaml developers in any industrial setting, and probably the world's largest OCaml codebase. We use OCaml for running our entire business, supporting everything from research to systems administration to trading systems. If you're interested in seeing how functional programming plays out in the real world, there's no better place.

The atmosphere is informal and intellectual. There is a focus on education, and people learn about software and trading, both through formal classes and on the job. The work is challenging, and you get to see the practical impact of your efforts in quick and dramatic terms. Jane Street is also small enough that people have the freedom to get involved in many different areas of the business. Compensation is highly competitive, and there's a lot of room for growth.

You can learn more about Jane Street and our technology from our main site, janestreet.com. You can also look at a a talk given at CMU about why Jane Street uses functional programming (http://ocaml.janestreet.com/?q=node/61), and our programming blog (http://ocaml.janestreet.com).

We also have extensive benefits, including:

• 90% book reimbursement for work-related books
• 90% tuition reimbursement for continuing education
• Excellent, zero-premium medical and dental insurance
• Free lunch delivered daily from a selection of restaurants
• Catered breakfasts and fresh brewed Peet's coffee
• An on-site, private gym in New York with towel service
• Kitchens fully stocked with a variety of snack choices
• Full company 401(k) match up to 6% of salary, vests immediately

More information at http://janestreet.com/culture/benefits/

A new release of Alt-Ergo (version 2.1.0) is available on Alt-Ergo’s website: https://alt-ergo.ocamlpro.com/#releases. An OPAM package for it will be published soon.
In this release, we mainly improved the CDCL-based SAT solver to get performances similar to/better than the old Tableaux-like SAT. The CDCL solver is now the default Boolean reasoner. The full list of CHANGES is available here.
Despite our various tests, you may still encounter some issues with this new solver.  Please, don&…

A new release of Alt-Ergo (version 2.1.0) is available on Alt-Ergo’s website: https://alt-ergo.ocamlpro.com/#releases. An OPAM package for it will be published soon.
In this release, we mainly improved the CDCL-based SAT solver to get performances similar to/better than the old Tableaux-like SAT. The CDCL solver is now the default Boolean reasoner. The full list of CHANGES is available here.
Despite our various tests, you may still encounter some issues with this new solver.  Please, don’t hesitate to report bugs, ask questions, and give your feedback!

Update – TZScan.io can now work on top of the zeronet (zeronet.tzscan.io), we hope it can help the developers community monitor the network. You can now switch between the alphanet & zeronet networks!

OCamlPro is pleased to announce an update of TzScan (http://tzscan.io), its Tezos block explorer to ease the use of the Tezos network.

In addition to some minor bugfixes, the main novelties are:

• Health of the network with stats about the blocks, endorsements, bakers, etc.
• Display of futu…

Update – TZScan.io can now work on top of the zeronet (zeronet.tzscan.io), we hope it can help the developers community monitor the network. You can now switch between the alphanet & zeronet networks!

OCamlPro is pleased to announce an update of TzScan (http://tzscan.io), its Tezos block explorer to ease the use of the Tezos network.

In addition to some minor bugfixes, the main novelties are:

• Health of the network with stats about the blocks, endorsements, bakers, etc.
• Display of future baker’s rights in the current cycle
• For each account, a more detailed balance including the bonds, rewards, fees, etc. for the current cycle and its future baking positions
• A new feature to inject signed operations in the network
• In the detailed block’s view, all blocks are displayed at the same level in alternative chains
• UI improvements on desktop, tablet and mobile

We are still working hard trying to improve and add new features to TzScan. Further enhancements and optimizations are to come. Enjoy and play with our explorer.

If you have suggestions or bugs, please send us reports at contact@tzscan.io

OCamlPro is proud to release a first version of TzScan (http://tzscan.io), its Tezos
block explorer to ease the use of the Tezos network.

What TzScan can do for you :

– Several charts on blocks, operations, network, volumes, fees, and more,
– Marketcap and Futures/IOU prices from coinmarket.com,
– Blocks, operations, accounts and contracts detail pages,
– Public API to get information about blocks, operations, accounts and more,
– Documentation on different concept…

OCamlPro is proud to release a first version of TzScan (http://tzscan.io), its Tezos
block explorer to ease the use of the Tezos network.

What TzScan can do for you :

– Several charts on blocks, operations, network, volumes, fees, and more,
– Marketcap and Futures/IOU prices from coinmarket.com,
– Blocks, operations, accounts and contracts detail pages,
– Public API to get information about blocks, operations, accounts and more,
– Documentation on different concepts of Tezos like Endorsements, Nonces, etc.

What we tried to do with TzScan is to show differently the Tezos network to have a better understanding of what is really going on by showing the main points of Proof of Stake. Further enhancements and optimization are to come but enjoy and play with our explorer.

If you have suggestions or bugs, please send us reports at contact@tzscan.io !

As a tradition, we took part in this year’s Journées Francophones des Langages Applicatifs (JFLA 2018) that was chaired by LRI’s Sylvie Boldo and hosted in Banyuls the last week of January. That was a nice opportunity to present a live demo of a multisignature smart-contract entirely written in the #Liquidity language designed at OCamlPro, and deployed live on the Tezos alphanet (the slides are now available, see at the end of the post).

Tezos is the only blockchain to use a strong…

As a tradition, we took part in this year’s Journées Francophones des Langages Applicatifs (JFLA 2018) that was chaired by LRI’s Sylvie Boldo and hosted in Banyuls the last week of January. That was a nice opportunity to present a live demo of a multisignature smart-contract entirely written in the #Liquidity language designed at OCamlPro, and deployed live on the Tezos alphanet (the slides are now available, see at the end of the post).

Tezos is the only blockchain to use a strongly typed, functional language, with a formal semantic and an interpreter validated by the use of GADTs (generalized abstract data-types). This stack-based language, named Michelson, is somewhat tricky to use as-is, the absence of variables (among others) necessitating to manipulate the stack directly. For this reason, we have developed, starting in June 2017, a higher level language, Liquidity, implementing the type system of Michelson in a subset of OCaml.

In addition to the compiler which allows to compile Liquidity programs to Michelson ones, we have developed a decompiler which, from Michelson code, can recover a Liquidity version, much easier to look at and understand (for humans). This tool is of some significance considering that contracts will be stored on the blockchain in Michelson format, making them more approachable and understandable for end users.

To facilitate designing contracts and foster Liquidity adoption we have also developed a web application. This app offers somewhat bare-bone editors for Liquidity and Michelson, allows compilation in the browser directly, deployment of Liquidity contracts and interaction with them (using the Tezos alphanet).

This blog post presents these different tools in more detail.

Michelson

Michelson is a stack-based, functional, statically and strongly typed language. It comes with a set of built-in base types like strings, Booleans, unbounded integers and naturals, lists, pairs, option types, union (of two) types, sets, maps. There also a number of domain dependent types like amounts (in tezzies), cryptographic keys and signatures, dates, etc. A Michelson program consists in a structured sequence of instructions, each of which operates on the stack. The program takes as inputs a parameter as well as a storage and returns a result and a new value for the storage. They can fail at runtime with the instruction FAIL, or another error (call of a failing contract, out of gas, etc.), but most instructions that could fail return an option instead (e.g. EDIV returns None when dividing by zero). The following example is a smart contract which implements a voting system on the blockchain. The storage consists in a map from possible votes (as strings) to integers counting number of votes. A transaction to this contract must be made with an amount (accessible with instruction AMOUNT) greater or equal to 5 tezzies and a parameter which is a valid vote. If one of these conditions is not respected, the execution, and thus the transaction, fail. Otherwise the program retrieves the previous number of votes in the storage and increments them. At the end of the execution, the stack contains the pair composed of the value Unit and the updated map (the new storage).

parameter string;
storage (map string int);
return unit;
code
  { # Pile = [ Pair parameter storage ]
    PUSH tez "5.00"; AMOUNT; COMPARE; LT;
    IF # Is AMOUNT < 5 tz ?
      { FAIL }
      {
        DUP; DUP; CAR; DIP { CDR }; GET; # GET parameter storage
        IF_NONE # Is it a valid vote ?
          { FAIL }
          { # Some x, x now in the stack
            PUSH int 1; ADD; SOME; # Some (x + 1)
            DIP { DUP; CAR; DIP { CDR } }; SWAP; UPDATE;
            # UPDATE parameter (Some (x + 1)) storage
            PUSH unit Unit; PAIR; # Pair Unit new_storage
          }
      };
  }

Michelson has several specificities:

• Typing a Michelson program is done by types propagation, and not à la Milner. Polymorphic types are forbidden and type annotations are required when a type is ambiguous (e.g. empty list).
• Functions (lambdas) are pure and are not closures, i.e. they must have an empty environment. For instance, a function passed to another contract as parameter acts in a purely functional way, only accessing the environment of the new contract.
• Method calls is preformed with the instruction TRANSFER_TOKENS: it requires an empty stack (not counting its arguments). It takes as argument the current storage, saves it before the call is made, and finally returns it after the call together with the result. This forces developers to save anything worth saving in the current storage, while keeping in mind that a reentring call can happend (the returned storage might be different).

We won’t explain the semantics of Michelson here, a good one in big step form is available here.

The Liquidity Language

Liquidity is also a functional, statically and strongly typed language that compiles down to the stack-based language Michelson. Its syntax is a subset of OCaml and its semantic is given by its compilation schema. By making the choice of staying close to Michelson in spirit while offering higher level constraints, Liquidity allows to easily write legible smart contracts with the same safety guaranties offered by Michelson. In particular we decided that it was important to keep the purely functional aspect of the language so that simply reading a contract is not obscured by effects and global state. In addition, the OCaml syntax makes Liquidity an immediately accessible tool to programmers who already know OCaml while its limited span makes the learning curve not too steep.

The following example is a liquidity version of the vote contract. Its inner workings are rather obvious for anyone who has already programmed in a ML-like language.

[%%version 0.15]

type votes = (string, int) map

let%init storage (myname : string) =
  Map.add myname 0 (Map ["ocaml", 0; "pro", 0])

let%entry main
    (parameter : string)
    (storage : votes)
  : unit * votes =

  let amount = Current.amount() in

  if amount < 5.00tz then
    Current.failwith "Not enough money, at least 5tz to vote"
  else
    match Map.find parameter storage with
    | None -> Current.failwith "Bad vote"
    | Some x ->
        let storage = Map.add parameter (x+1) storage in
        ( (), storage )

A Liquidity contract starts with an optional version meta-information. The compiler can reject the program if it is written in a too old version of the language or if it is itself not recent enough. Then comes a set of type and function definitions. It is also possible to specify an initial storage (constant, or a non-constant storage initializer) with let%init storage. Here we define a type abbreviation votes for a map from strings to integers. It is the structure that we will use to store our vote counts.

The storage initializer creates a map containing two bindings, "ocaml" to 0 and "pro" to 0 to which we add another vote option depending on the argument myname given at deploy time.

The entry point of the program is a function main defined with a special annotation let%entry. It takes as arguments a call parameter (parameter) and a storage (storage) and returns a pair whose first element is the result of the call, and second element is a potentially modified storage.

The above program defines a local variable amount which contains the amount of the transaction which generated the call. It checks that it is greater than 5 tezzies. If not, we fail with an explanatory message. Then the program retrieves the number of votes for the chosen option given as parameter. If the vote is not a valid one (i.e., there is no binding in the map), execution fails. Otherwise, the current number of votes is bound to the name x. Storage is updated by incrementing the number of votes for the chosen option. The built-in function Map.add adds a new binding (here, it replaces a previously existing binding) and returns the modified map. The program terminates, in the normal case, on its last expression which is its returned value (a pair containing () — the contract only modifies the storage — and the storage itself).

A reference manual for Liquidity is available here. It gives a relatively complete overview of the available types, built-in functions and constructs of the language.

Compilation

Encodings

Because Liquidity is a lot richer than Michelson, some types and constructs must be simplified or encoded. Record types are translated to right-associated pairs with as many components as the record has fields. t1 is encoded as t1' in the following example.

type t1 = { a: int; b: string; c: bool}
type t1’ = (int * (string * bool))

Field accesses in a record is translated to accesses in the corresponding tuples (pairs). Sum (or union) types are translated using the built-in variant type (this is the or type in Michelson). t2 is encoded as t2' in the following example.

type ('a, 'b) variant = Left of 'a | Right of `b

type t2 = A of int | B of string | C
type t2’ = (int, (string, unit) variant) variant

Similarly, pattern matching on expressions of a sum type is translated to nested pattern matchings on variant typed expressions. An example translation is the following:

match x with
| A i -> something1(i)
| B s -> something2(s)
| C -> something3

match x with
| Left i -> something1(i)
| Right r -> match r with
             | Left s -> something2(s)
             | Right -> something3

Liquidity also supports closures while Michelson only allows pure lambdas. Closures are translated by lambda-lifting, i.e. encoded as pairs whose first element is a lambda and second element is the closure environment. The resulting lambda takes as argument a pair composed of the closure’s argument and environment. Adequate transformations are also performed for built-in functions that take lambdas as arguments (e.g. in List.map) to allow closures instead.

Compilation schema

This little section is a bit more technical, so if you don’t care how Liquidity is compiled precisely, you can skip over to the next one.

We note by Γ, [|x|]_d ⊢ X ↑^t compilation of the Liquidity instruction x, in environment Γ. Γ is a map associating variable names to a position in the stack. The compilation algorithm also maintains the size of the current stack (at compilation of instruction x), denoted by d in the previous expression. Below is a non-deterministic version of the compilation schema, the one implemented in the Liquidity compiler being a determinized version.

The result of compiling x is a Michelson instruction (or sequence of instructions) X together with a Boolean transfer information t. The instruction Contract.call (or TRANSFER_TOKENS in Michelson) needs an empty stack to evaluate, so the compiler empties the stack before translating this call. However, the various branches of a Michelson program must have the same stack type. This is why we need to maintain this information so that the compiler can empty stacks in some parts of the program.

Some of the rules have parts annotated with ?_b. This suffix denotes a potential reset or erasing. In particular:

• For sets, Γ?_b is ∅ if b evaluates to false, and Γ otherwise.
• For integers, d?_b is 0 if b evaluates to false, and d otherwise.
• For instructions, (X)?_b is {} if b evaluates to false, and X otherwise.

For instance, by looking at rule CONST, we can see that compiling a Liquidity constant simply consists in pushing this constant on the stack. To handle variables in a simple manner, the rule VAR tells us to look in the environment Γ for the index associated to the variable we want to compile. Then, instruction D(U)ⁱP puts at the top of the stack a copy of the element present at depth i. Variables are added to Γ with the Liquidity instruction let ... in or with any instruction that binds an new symbol, like fun for instance.

Decompilation from Michelson

While Michelson programs are high level compared to other bytecodes, it remains difficult for a blockchain end-user to understand what a Michelson program does exactly by looking at it. However, following the idea that “code is law”, a user should be able to read a contract and understand its precise semantic. Thus, we have developed a decompiler from Michelson to Liquidity, which allows to recover a much more readable and understandable representation of a program on the blockchain.

The decompilation of Michelson code follows the diagram below where:

• Cleaning consists in simplifying Michelson code to accelerate the whole process and simplify the following task. For now it consists in ereasing instructions whose continuation is a failure.
• Symbolic Execution consists in executing the Michelson program with symbolic inputs, and by replacing every value placed in the stacj by a node containing the instruction that generated it. Each node of this graph can be seen as an expression of the target program, which can be bound to a variable name. Edges to this node represent future occurrences of this variable.
• Decompilation consists in transforming the graph generated by the previous step in a Liquidity syntax tree. Names for variables are recovered from annotations produced by the Liquidity compiler (in case we decompile a Michelson program that was generated from Liquidty), or are chosen on the fly when no annotation is present (e.g. if the Michelson program was written by hand).

Finally the program is typed (to ensure no mistakes were made), simplified and pretty printed.

Example of decompilation

parameter bool;
return int;
storage int;
code {DUP; CAR;
      DIP { CDR; PUSH int 1 };  # stack is: parameter :: 1 :: storage
      IF # if parameter = true
         { DROP; DUP; }         # stack is storage :: storage
         { }                    # stack is 1 :: storage
         ;
      PAIR;
     }

This example illustrate some of the difficulties of the decompilation process: Liquidity is a purely functional language where each construction is an expression returning a value; Michelson handles the stack directly, which is impossible to concretize in in Liquidity (values in the stack don’t have the same type, as opposed to values in a list). In this example, depending on the value of parameter the contract returns either the content of the storage, or the integer 1. In the Michelson code, the programmer used the instruction IF, but its branches do not return a value and only operates by modifying (or not) the stack.

[%%version 0.15]
type storage = int
let%entry main (parameter : bool) (storage : storage) : (int * storage) =
    ((if parameter then storage else 1), storage)

The above translation to Liquidity also contains an if, but it has to return a value. The graph below is the result of the symbolic execution phase on the Michelson program. The IF instruction is decomposed in several nodes, but does not contain any remaining instruction: the result of this if is in fact the difference between the stack resulting from the execution of the then branch and from the else branch. It is denoted by the node N_IF_END_RESULT 0 (if there were multiple of these nodes with different indexes, the result of the if would have been a tuple, corresponding to the multiple changes in the stack).

Try-Liquidity

You can go to http://liquidity-lang.org/edit to try out Liquidity in your browser.

The first thing to do (if you want to deploy and interact with a contract) is to go into the settings menu. There you can set your Tezos private key (use one that you generated for the alphanet for the moment) or the source (i.e. your public key hash, which is derived from your private key if you set it).

You can also change which Tezos node you want to interact with (the first one should do, but you can also set one of your choosing such as one running locally on your machine). The timestamp shown next to the node name indicates how long ago was produced the last block that it knows of. Transactions that you make on a node that is not synchronized will not be included in the main chain.

You should now see your account with its balance in the top bar:

In the main editor window, you can select a few Liquidity example contracts or write your own. For this small tutorial, we will select multisig.liq which is a minimal multi-signature wallet contract. It allows anyone to send money to it, but it requires a certain number of predefined owners to agree before making a withdrawal.

Clicking on the button Compile should make the editor blink green (when there are no errors) and the compiled Michelson will appear on the editor on the right.

Let’s now deploy this contract on the Tezos alphanet. By going into the Deploy (or paper airplane icon) tab, we can choose our set of owners for the multisig contract and the minimum number of owners to be in agreement before a withdrawal can proceed. Here I put down two account addresses for which I possess the private keys, and I want the two owners to agree before any transaction is approved (2p is the natural number 2).

Then I can either forge the deployment operation which is then possible to sign offline and inject in the Tezos chain by other means, or I can directly deploy this contract (if the private key is set in settings). If deployment is successful, we can see both the deployment operation and the new contract on a block explorer by clicking on the provided links.

Now we can query the blockchain to examine our newly deployed contract. Head over to the Examine tab. The address field should already be filled with our contract handle. We just have to click on Retrieve balance and storage.

The contract has 3tz on its balance because we chose to initialize it this way. On the right is the current storage of the contract (in Liquidity syntax) which is a record with four fields. Notice that the actions field is an empty map.

Let’s make a few calls to this contract. Head over to the Call tab and fill-in the parameter and the amount. We can send for instance 5.00tz with the parameter Pay. Clicking on the button Call generates a transaction which we can observe on a block explorer. More importantly if we go back to the Examine tab, we can now retrieve the new information and see that the storage is unchanged but the balance is 8.00tz.

We can also make a call to withdraw money from the contract. This is done by passing a parameter of the form:

Manage (
  Some {
    destination = tz1brR6c9PY3SSfBDu7Qxdhsz3pvNRDwf68a;
    amount = 2tz;
})

This is a proposition of transfer of funds in the amount of 2.00tz from the contract to the destination tz1brR6c9PY3SSfBDu7Qxdhsz3pvNRDwf68a.

The balance of the contract has not changed (it is still 8.00tz) but the storage has been modified. That is because this multisig contract requires two owners to agree before proceeding. The proposition is stored in the map actions and is associated to the owner who made said proposition.

{
  owners =
    (Set
       [tz1XT2pgiSRWQqjHv5cefW7oacdaXmCVTKrU;
       tz1brR6c9PY3SSfBDu7Qxdhsz3pvNRDwf68a]);
  actions =
    (Map
       [(tz1brR6c9PY3SSfBDu7Qxdhsz3pvNRDwf68a,
          {
            destination = tz1brR6c9PY3SSfBDu7Qxdhsz3pvNRDwf68a;
            amount = 2.00tz
          })]);
  owners_length = 2p;
  min_agree = 2p
}

We can now open a new browser tab and point it to http://liquidity-lang.org/edit, but this time we fill in the private key for the second owner tz1XT2pgiSRWQqjHv5cefW7oacdaXmCVTKrU. We choose the multisig contract in the Liquidity editor and fill-in the contract address in the call tab with the same one as in the other session TZ1XvTpoSUeP9zZeCNWvnkc4FzuUighQj918 (you can double check the icons for the two contracts are identical). For the the withdrawal to proceed, this owner has to make the exact same proposition so let’s make a call with the same parameter:

Manage (
  Some {
    destination = tz1brR6c9PY3SSfBDu7Qxdhsz3pvNRDwf68a;
    amount = 2tz;
})

The call should also succeed. When we examine the contract, we can now see that its balance is down to 6.00tz and that the field actions of its storage has been reinitialized to the empty map. In addition, we can update the balance of our first account (by clicking on the circle arrow icon in the tob bar) to see that it is now up an extra 2.00tz and that was the destination of the proposed (and agreed on) withdrawal. All is well!

We have seen how to compile, deploy, call and examine Liquidity contracts on the Tezos alphanet using our online editor. Experiment with your own contracts and let us know how that works for you!

• Slides in English
• and French

Since 2017 is just over, now is probably the best time to review what happened during this hectic year at OCamlPro… Here are our big 2017 achievements, in the world of blockchains (the Liquidity smart contract language, Tezos and the Tezos ICO,  etc.), of OCaml (with OPAM 2, flambda 2 etc.), and of formal methods (Alt-Ergo etc.)

Since 2017 is just over, now is probably the best time to review what happened during this hectic year at OCamlPro… Here are our big 2017 achievements, in the world of blockchains (the Liquidity smart contract language, Tezos and the Tezos ICO,  etc.), of OCaml (with OPAM 2, flambda 2 etc.), and of formal methods (Alt-Ergo etc.)

2018

At the end of 2017, I resigned from my PostDoc position at University of Cambridge (in the rems project). Early December 2017 I organised the 4th MirageOS hack retreat, with which I'm very satisfied. In March 2018 the 5th retreat will happen (please sign up!).

In 2018 I moved to Berlin and started to work for the (non-profit) Center for the cultivation of technology with our robur.io project "At robur, we build performant bespoke minimal operating systems for high-assurance se…

2018

At the end of 2017, I resigned from my PostDoc position at University of Cambridge (in the rems project). Early December 2017 I organised the 4th MirageOS hack retreat, with which I'm very satisfied. In March 2018 the 5th retreat will happen (please sign up!).

In 2018 I moved to Berlin and started to work for the (non-profit) Center for the cultivation of technology with our robur.io project "At robur, we build performant bespoke minimal operating systems for high-assurance services". robur is only possible by generous donations in autumn 2017, enthusiastic collaborateurs, supportive friends, and a motivated community, thanks to all. We will receive funding from the prototypefund to work on a CalDAV server implementation in OCaml targeting MirageOS. We're still looking for donations and further funding, please get in touch. Apart from CalDAV, I want to start the year by finishing several projects which I discovered on my hard drive. This includes DNS, opam signing, TCP, ... . My personal goal for 2018 is to develop a flexible mirage deploy, because after configuring and building a unikernel, I want to get it smoothly up and running (spoiler: I already use albatross in production).

To kick off (3% of 2018 is already used) this year, I'll talk in more detail about µDNS, an opinionated from-scratch re-engineered DNS library, which I've been using since Christmas 2017 in production for ns.nqsb.io and ns.robur.io. The development started in March 2017, and continued over several evenings and long weekends. My initial motivation was to implement a recursive resolver to run on my laptop. I had a working prototype in use on my laptop over 4 months in the summer 2017, but that code was not in a good shape, so I went down the rabbit hole and (re)wrote a server (and learned more about GADT). A configurable resolver needs a server, as local overlay, usually anyways. Furthermore, dynamic updates are standardised and thus a configuration interface exists inside the protocol, even with hmac-signatures for authentication! Coincidentally, I started to solve another issue, namely automated management of let's encrypt certificates (see this branch for an initial hack). On my journey, I also reported a cache poisoning vulnerability, which was fixed in Docker for Windows.

But let's get started with some content. Please keep in mind that while the code is publicly available, it is not yet released (mainly since the test coverage is not high enough, and the lack of documentation). I appreciate early adopters, please let me know if you find any issues or find a use case which is not straightforward to solve. This won't be the last article about DNS this year - persistent storage, resolver, let's encrypt support are still missing.

What is DNS?

The domain name system is a core Internet protocol, which translates domain names to IP addresses. A domain name is easier to memorise for human beings than an IP address. DNS is hierarchical and decentralised. It was initially "specified" in Nov 1987 in RFC 1034 and RFC 1035. Nowadays it spans over more than 20 technical RFCs, 10 security related, 5 best current practises and another 10 informational. The basic encoding and mechanisms did not change.

On the Internet, there is a set of root servers (administrated by IANA) which provide the information about which name servers are authoritative for which top level domain (such as ".com"). They provide the information about which name servers are responsible for which second level domain name (such as "example.com"), and so on. There are at least two name servers for each domain name in separate networks - in case one is unavailable the other can be reached.

The building blocks for DNS are: the resolver, a stub (gethostbyname provided by your C library) or caching forwarding resolver (at your ISP), which send DNS packets to another resolver, or a recursive resolver which, once seeded with the root servers, finds out the IP address of a requested domain name. The other part are authoritative servers, which reply to requests for their configured domain.

To get some terminology, a DNS client sends a query, consisting of a domain name and a query type, and expects a set of answers, which are called resource records, and contain: name, time to live, type, and data. The resolver iteratively requests resource records from authoritative servers, until the requested domain name is resolved or fails (name does not exist, server failure, server offline).

DNS usually uses UDP as transport which is not reliable and limited to 512 byte payload on the Internet (due to various middleboxes). DNS can also be transported via TCP, and even via TLS over UDP or TCP. If a DNS packet transferred via UDP is larger than 512 bytes, it is cut at the 512 byte mark, and a bit in its header is set. The receiver can decide whether to use the 512 bytes of information, or to throw it away and attempt a TCP connection.

DNS packet

The packet encoding starts with a 16bit identifier followed by a 16bit header (containing operation, flags, status code), and four counters, each 16bit, specifying the amount of resource records in the body: questions, answers, authority records, and additional records. The header starts with one bit operation (query or response), four bits opcode, various flags (recursion, authoritative, truncation, ...), and the last four bit encode the response code.

A question consists of a domain name, a query type, and a query class. A resource record additionally contains a 32bit time to live, a length, and the data.

Each domain name is a case sensitive string of up to 255 bytes, separated by . into labels of up to 63 bytes each. A label is either encoded by its length followed by the content, or by an offset to the start of a label in the current DNS frame (poor mans compression). Care must be taken during decoding to avoid cycles in offsets. Common operations on domain names are comparison: equality, ordering, and also whether some domain name is a subdomain of another domain name, should be efficient. My initial representation naïvely was a list of strings, now it is an array of strings in reverse order. This speeds up common operations by a factor of 5 (see test/bench.ml).

The only really used class is IN (for Internet), as mentioned in RFC 6895. Various query types (MD, MF, MB, MG, MR, NULL, AFSDB, ...) are barely or never used. There is no need to convolute the implementation and its API with these legacy options (if you have a use case and see those in the wild, please tell me).

My implemented packet decoding does decompression, only allows valid internet domain names, and may return a partial parse - to use as many resource records in truncated packets as possible. There are no exceptions raised, the parsing uses a monadic style error handling. Since label decompression requires the parser to know absolute offsets, the original buffer and the offset is manually passed around at all times, instead of using smaller views on the buffer. The decoder does not allow for gaps, when the outer resource data length specifies a byte length which is not completely consumed by the specific resource data subparser (an A record must always consume four bytes). Failing to check this can lead to a way to exfiltrate data without getting noticed.

Each zone (a served domain name) contains a SOA "start of authority" entry, which includes the primary nameserver name, the hostmaster's email address (both encoded as domain name), a serial number of the zone, a refresh, retry, expiry, and minimum interval (all encoded as 32bit unsigned number in seconds). Common resource records include A, which payload is 32bit IPv4 address. A nameserver (NS) record carries a domain name as payload. A mail exchange (MX) whose payload is a 16bit priority and a domain name. A CNAME record is an alias to another domain name. These days, there are even records to specify the certificate authority authorisation (CAA) records containing a flag (critical), a tag ("issue") and a value ("letsencrypt.org").

Server

The operation of a DNS server is to listen for a request and serve a reply. Data to be served can be canonically encoded (the RFC describes the format) in a zone file. Apart from insecurity in DNS server implementations, another attack vector are amplification attacks where an attacker crafts a small UDP frame with a fake source IP address, and the server answers with a large response to that address which may lead to a DoS attack. Various mitigations exist including rate limiting, serving large replies only via TCP, ...

Internally, the zone file data is stored in a tree (module Dns_trie implementation), where each node contains two maps: sub, which key is a label and value is a subtree and dns_map (module Dns_map), which key is a resource record type and value is the resource record. Both use the OCaml Map ("also known as finite maps or dictionaries, given a total ordering function over the keys. All operations over maps are purely applicative (no side-effects). The implementation uses balanced binary trees, and therefore searching and insertion take time logarithmic in the size of the map").

The server looks up the queried name, and in the returned Dns_map the queried type. The found resource records are sent as answer, which also includes the question and authority information (NS records of the zone) and additional glue records (IP addresses of names mentioned earlier in the same zone).

Dns_map

The data structure which contains resource record types as key, and a collection of matching resource records as values. In OCaml the value type must be homogenous - using a normal sum type leads to an unneccessary unpacking step (or lacking type information):

let lookup_ns t =
  match Map.find NS t with
  | None -> Error `NotFound
  | Some (NS nameservers) -> Ok nameservers
  | Some _ -> Error `NotFound

Instead, I use in my current rewrite generalized algebraic data types (read OCaml manual and Mads Hartmann blog post about use cases for GADTs, Andreas Garnæs about using GADTs for GraphQL type modifiers) to preserve a relation between key and value (and A record has a list of IPv4 addresses and a ttl as value) - similar to hmap, but different: a closed key-value mapping (the GADT), no int for each key and mutable state. Thanks to Justus Matthiesen for helping me with GADTs and this code. Look into the interface and implementation.

(* an ordering relation, I dislike using int for that *)
module Order = struct
  type (_,_) t =
    | Lt : ('a, 'b) t
    | Eq : ('a, 'a) t
    | Gt : ('a, 'b) t
end

module Key = struct
  (* The key and its value type *)
  type _ t =
    | Soa : (int32 * Dns_packet.soa) t
    | A : (int32 * Ipaddr.V4.t list) t
    | Ns : (int32 * Dns_name.DomSet.t) t
    | Cname : (int32 * Dns_name.t) t

  (* we need a total order on our keys *)
  let compare : type a b. a t -> b t -> (a, b) Order.t = fun t t' ->
    let open Order in
    match t, t' with
    | Cname, Cname -> Eq | Cname, _ -> Lt | _, Cname -> Gt
    | Ns, Ns -> Eq | Ns, _ -> Lt | _, Ns -> Gt
    | Soa, Soa -> Eq | Soa, _ -> Lt | _, Soa -> Gt
    | A, A -> Eq
end

type 'a key = 'a Key.t

(* our OCaml Map with an encapsulated constructor as key *)
type k = K : 'a key -> k
module M = Map.Make(struct
    type t = k
    (* the price I pay for not using int as three-state value *)
    let compare (K a) (K b) = match Key.compare a b with
      | Order.Lt -> -1
      | Order.Eq -> 0
      | Order.Gt -> 1
  end)

(* v contains a key and value pair, wrapped by a single constructor *)
type v = V : 'a key * 'a -> v

(* t is the main type of a Dns_map, used by clients *)
type t = v M.t

(* retrieve a typed value out of the store *)
let get : type a. a Key.t -> t -> a = fun k t ->
  match M.find (K k) t with
  | V (k', v) ->
    (* this comparison is superfluous, just for the types *)
    match Key.compare k k' with
    | Order.Eq -> v
    | _ -> assert false

This helps me to programmaticaly retrieve tightly typed values from the cache, important when code depends on concrete values (i.e. when there are domain names, look these up as well and add as additional records). Look into server/dns_server.ml

Dynamic updates, notifications, and authentication

Dynamic updates specify in-protocol record updates (supported for example by nsupdate from ISC bind-tools), notifications are used by primary servers to notify secondary servers about updates, which then initiate a zone transfer to retrieve up to date data. Shared hmac secrets are used to ensure that the transaction (update, zone transfer) was authorised. These are all protocol extensions, there is no need to use out-of-protocol solutions.

The server logic for update and zone transfer frames is slightly more complex, and includes a dependency upon an authenticator (implemented using the nocrypto library, and ptime).

Deployment and Let's Encrypt

To deploy servers without much persistent data, an authentication schema is hardcoded in the dns-server: shared secrets are also stored as DNS entries (DNSKEY), and _transfer.zone, _update.zone, and _key-management.zone names are introduced to encode the permissions. A _transfer key also needs to encode the IP address of the primary (to know where to request zone transfers) and secondary IP (to know where to send notifications).

Please have a look at ns.robur.io and the examples for more details. The shared secrets are provided as boot parameter of the unikernel.

I hacked maker's ocaml-letsencrypt library to use µDNS and sending update frames to the given IP address. I already used this to have letsencrypt issue various certificates for my domains.

There is no persistent storage of updates yet, but this can be realised by implementing a secondary (which is notified on update) that writes every new zone to persistent storage (e.g. disk or git). I also plan to have an automated Let's Encrypt certificate unikernel which listens for certificate signing requests and stores signed certificates in DNS. Luckily the year only started and there's plenty of time left.

I'm interested in feedback, either via twitter hannesm@mastodon.social or an issue on the data repository.

I’ve done a lot of stuff in the last half of 2017, but not much of it has made it here. Here’s a roundup of things published/spoken/embroidered/etc in other places:

• a cycling trip near Seattle, the San Juan Islands, and Vancouver Island
• some TCP fanart
• a writeup on bun on the ocamllabs blog
• a talk on fuzzing in the CI/CD pipeline given at DevOps Days Madison
• a full-size cross-stitched reproduction of a scene from The Secret of Monkey Island (VGA remake)
• my reflections on the lat…

I’ve done a lot of stuff in the last half of 2017, but not much of it has made it here. Here’s a roundup of things published/spoken/embroidered/etc in other places:

• a cycling trip near Seattle, the San Juan Islands, and Vancouver Island
• some TCP fanart
• a writeup on bun on the ocamllabs blog
• a talk on fuzzing in the CI/CD pipeline given at DevOps Days Madison
• a full-size cross-stitched reproduction of a scene from The Secret of Monkey Island (VGA remake)
• my reflections on the late-2017 MirageOS hack retreat in Marrakesh (raw text)
• a writeup on ppx_deriving_crowbar on the ocamllabs blog
• some utop fanart, which is not yet complete
• a talk at the 34th Chaos Communication Congress (resilience track) on library operating systems (translated into French and German - click the gear in the lower right!)

Also, how about some direct links to software projects?

• bun, a project for integrating Crowbar tests into cloud-based CI pipelines
• ppx_deriving_crowbar, an experimental ppx_deriving plugin for automatically deriving generators for use in crowbar
• ocaml-test-stdlib, Crowbar tests for the Map and Set functors in the OCaml standard library run in Travis CI using bun
• ocaml-test-omp, a Crowbar test for ocaml-migrate-parsetree using ppx_deriving_crowbar to automatically derive the types in OCaml’s parsetree.mli
• certify, a three-year-old tool for generating X509 certificates that just saw its proper first release.

Oh yeah, and also a bit of software community service:

• lots of work on MirageOS
• I joined the ranks of opam-repository maintainers

A post like this, standing in the doorway of a new year, invites some thoughts about the future as well as the past. I don’t have time for deep thoughts on this (my old cert expires in 18 minutes as of this writing, and I’d like to deploy this post before then), but I hope that in 2018, we can keep taking our time and attention away from those who would profit off of us, and continue making a better world.

testing ocaml-migrate-parsetree with ppx_deriving_crowbar

Early feedback on Crowbar suggested that some automated method of constructing generators might be useful. It wasn’t necessary to do this immediately for the demonstration of testing the OCaml standard library’s Map and Set functors with Crowbar, but what about more complicated types? Like, say, the complicated and heavily mutually recursive types that compose OCaml parsetrees?

With an eye to solving this problem, I looked into a …

testing ocaml-migrate-parsetree with ppx_deriving_crowbar

Early feedback on Crowbar suggested that some automated method of constructing generators might be useful. It wasn’t necessary to do this immediately for the demonstration of testing the OCaml standard library’s Map and Set functors with Crowbar, but what about more complicated types? Like, say, the complicated and heavily mutually recursive types that compose OCaml parsetrees?

With an eye to solving this problem, I looked into a few options and finally settled on using ppx_deriving. ppx_deriving is “a library simplifying type-driven code generation”, and not just for the author of an automatic code-generating tool, but also for the user who might wish to use such tools, or the maintainer who wants to be sure that multiple tools can be used together easily. Using ppx_deriving, one can annotate a type t:

type t = {
  a : int;
  b : Parsetree.core_type;
} [@@deriving myplugin]

and myplugin will have a chance to generate code based on the structure of t.

I was able to create such a tool for Crowbar, creatively named ppx_deriving_crowbar. The plugin is still in an experimental state, but mostly fulfills the requirements for ppx_deriving plugins set out in that project’s README. It is capable of making generators for OCaml 4.05 parsetrees and certificates for the x509 library, and probably much more!

OCaml migrate parse tree

Earlier this year, this blog post [2] explored the implementation of a small preprocessor extension (ppx).

The code of the above article worked well enough at the time but as written, exhibits a problem : new releases of the OCaml compiler are generally accompanied by evolutions of the OCaml parse tree. The effect of this is, a ppx written against a specific version of the compiler will "break" in the presence o…

OCaml migrate parse tree

Earlier this year, this blog post [2] explored the implementation of a small preprocessor extension (ppx).

The code of the above article worked well enough at the time but as written, exhibits a problem : new releases of the OCaml compiler are generally accompanied by evolutions of the OCaml parse tree. The effect of this is, a ppx written against a specific version of the compiler will "break" in the presence of later releases of the compiler. As pointed out in [3], the use of ppx's in the OCaml eco-system these days is ubiquitous. If each new release of the OCaml compiler required sychronized updates of each and every ppx in opam, getting new releases of the compiler out would soon become a near impossibilty.

Mitigation of the above problem is provided by the ocaml-migrate-parsetree library. The library provides the means to convert parsetrees from one OCaml version to another. This allows the ppx rewriter to write against a specific version of the parsetree and lets the library take care of rolling parsetrees backwards and forwards in versions as necessary. In this way, the resulting ppx is "forward compatible" with newer OCaml versions without requiring ppx code updates.

To get the ppx_id_of code from the earlier blog post usable with ocaml-migrate-parsetree required a couple of small tweaks to make it OCaml 4.02.0 compatible. The changes from the original code were slight and not of significant enough interest to be worth presenting here. What is worth looking at is what it then took to switch the code to use ocaml-migrate-parsetree. The answer is : very little!

open Migrate_parsetree
open OCaml_402.Ast

open Ast_mapper
open Ast_helper
open Asttypes
open Parsetree
open Longident

(* The original ppx as written before goes here!
   .                    .                   .
   .                    .                   .
   .                    .                   .
*)

let () = Driver.register ~name:"id_of" (module OCaml_402) id_of_mapper

References:
[1] "A Guide to Extension Points in OCaml" -- Whitequark (blog post 2014)
[2] "Preprocessor extensions for code generation" -- Shayne Fletcher (blog post 2017)
[3] "Extension Points - 3 Years Later" -- Rudi Grinberg (blog post 2017)

Our next OCaml Compiler Hacking event will be on Thursday 7th December in The Thomas Gray Room at Pembroke College, Cambridge.

If you're planning to come along, it'd be helpful if you could indicate interest via Doodle and sign up to the mailing list to receive updates.

When: Thursday 7 December 2017, 19:00 - 22:30

Where: The Thomas Gray Room, Pembroke College, Cambridge CB2 1RF

Who: anyone interested in improving OCaml. Knowledge of OCaml programming will obviously be helpful, but p…

Our next OCaml Compiler Hacking event will be on Thursday 7th December in The Thomas Gray Room at Pembroke College, Cambridge.

If you're planning to come along, it'd be helpful if you could indicate interest via Doodle and sign up to the mailing list to receive updates.

When: Thursday 7 December 2017, 19:00 - 22:30

Where: The Thomas Gray Room, Pembroke College, Cambridge CB2 1RF

Who: anyone interested in improving OCaml. Knowledge of OCaml programming will obviously be helpful, but prior experience of working on OCaml internals isn't necessary.

Refreshments: Finger buffet in hack room.

What: fixing bugs, implementing new features, learning about OCaml internals

Wiki: https://github.com/ocamllabs/compiler-hacking/wiki

This hack evening focuses on fixing up opam packages as well as work on the OCaml compiler.

The OCaml 4.06 release featured safe-string as the default rather than optional as per previous releases. The focus of this event will be to work on the opam repository to fix up as many packages as possible, and also to publish a guide on ocamllabs.io detailing how to migrate your packages for wider use.

The evening will also feature a short (5-10 min) presentation about recent MirageOS Marrakech Hack Retreat.​

After several years of using GitHub specifically for its pull request system, the Coq development team has migrated the Coq bug tracker and Cocorico, the Coq wiki to GitHub as well.

More information about the migration of the Coq bug tracker may be found in this blog post.

More information about the migration of Cocorico, the Coq wiki, may be found on this wiki page.

Finally, the GitHub repository is now the repository we push to (as opposed to a mirror). Make sure that your git clone is tra…

After several years of using GitHub specifically for its pull request system, the Coq development team has migrated the Coq bug tracker and Cocorico, the Coq wiki to GitHub as well.

More information about the migration of the Coq bug tracker may be found in this blog post.

More information about the migration of Cocorico, the Coq wiki, may be found on this wiki page.

Finally, the GitHub repository is now the repository we push to (as opposed to a mirror). Make sure that your git clone is tracking https://github.com/coq/coq.git to be always up-to-date.