We are pleased to announce our first DApp on Tezos: TzDrawIt!

TzDrawIt is a smart contract on Tezos betanet that allows you to draw pixels in an image. The full image is visible on a dedicated web site (http://tzdraw.it) and 4 thumbnails are displayed alternatively in the top-right corner of TzScan homepage. The instructions on how to submit pixels to the contract are detailed in the About tab on http://tzdraw.it, and a generator is provided to convert small PNG images to their corresponding Tez…

We are pleased to announce our first DApp on Tezos: TzDrawIt!

TzDrawIt is a smart contract on Tezos betanet that allows you to draw pixels in an image. The full image is visible on a dedicated web site (http://tzdraw.it) and 4 thumbnails are displayed alternatively in the top-right corner of TzScan homepage. The instructions on how to submit pixels to the contract are detailed in the About tab on http://tzdraw.it, and a generator is provided to convert small PNG images to their corresponding Tezos transactions.

An example of a simple transaction parameter to draw a single pixel at position (82, 37) with RGBA color (3, 0, 0, 255) is:

tezos-client transfer 1 from my_account to KT1WRUe3csC1jiThN9KUtaji2bd412upfn1E --fee 0 \
   --arg '{ Pair (Pair 82 37) (Pair 3 (Pair 0 (Pair 0 255))) }'

Note that alpha-blending is performed within the contract when transparency is different from 255. Pixels already drawn can only be overwritten by increasing the amount of tokens transmitted to the contract. The four thumbnails displayed on TzScan are centered on the four most expensive points on the drawing.

The TzDrawIt contract was originated on Tezos betanet Monday July 30, at 12:46 in block level 40659. It is visible here:

http://tzscan.io/KT1WRUe3csC1jiThN9KUtaji2bd412upfn1E

You can already see transactions that we submitted to draw the Tezos logo! You can also view the DApp state directly in Tzscan:

Note that, due to the current limitation on gas consumption per transaction in the Tezos protocol, you should not try to draw more than 40 pixels per transaction.
This contract will accept new transactions (i.e. pixel updates) for the next six months.

The Liquidity code and the generated Michelson code are also available on the dedicated webpage.

We hope you are going to enjoy this first app!

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/

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.

To be successful in tech, it’s well known that you must keep your skills up to date. The onus is on each individual to do this, no-one will do it for you, and companies that provide ongoing personal development are few and far between. Many companies would rather “remix our skills”, which means laying off workers with one skill (on statutory minimum terms) and hiring people with the new skill. Which is short-termist in the extreme; the new workers are no better than the old, th…

To be successful in tech, it’s well known that you must keep your skills up to date. The onus is on each individual to do this, no-one will do it for you, and companies that provide ongoing personal development are few and far between. Many companies would rather “remix our skills”, which means laying off workers with one skill (on statutory minimum terms) and hiring people with the new skill. Which is short-termist in the extreme; the new workers are no better than the old, they just happened to enter the workforce later, and the churn means there is no accumulation of institutional knowledge. If you were one of the newer workers, why would you voluntarily step onto this treadmill and if you were a client, why would you hire such a firm when it provides no value-add over just hiring the staff you need yourself? Anyway, I digress.

It is clear that C++11 was a enormous improvement over C++98. The list of new features is vast and all-encompassing, yet at the same time, backwards compatibility is preserved. You can have all the benefits of the new while preserving investment in the old (“legacy”). Upgrading your skills to C++11 was a very obvious thing to do, and because of the smooth transition, you could make quick wins as you brought yourself up to speed. That is just one example of the sort of thing I am talking about. You still need to put the effort in to learn it and seek out opportunities to use it, but the path from the old to the new is straightforward and there are early and frequent rewards along the way, and from there to C++14, 17, 20…

But I look around the current technology landscape and I see things that are only incremental improvements on existing programming languages or technologies and yet require a clean break with the past, which in practice means not only learning the new thing, but also rebuilding the ecosystem and tooling around it, porting/re-writing all the code, encountering all new bugs and edge cases, rediscovering the design patterns or new idioms in the language. The extent to which the new technology is “better” is dwarfed by the effort taken to use it, so where is the improved productivity coming from? Every project consists of either learning the language as you go, or maintaining and extending something written by someone who was learning the language as they went, perhaps gambling on getting in on the ground floor of the next big thing. But things only get big if people stick with them is the paradox!

So I am pretty comfortable with my decision to mostly ignore lots of new things, including but not limited to Go, Rust, Julia, Node.js, Perl6 in favour of deepening my skills in C++, R, Python and pushing into new problem domains (e.g. ML/AI) with my tried and trusted tools. When something comes along that is a big enough leap forward over any of them, of course I’ll jump – just like I did when I learnt Java in 1995 and was getting paid for it the same year! I had a lot of fun with OCaml and Haskell too, but neither gained significant traction in the end. I don’t see anything on the horizon, all the cutting edge stuff is appearing as libraries or features for my “big 3” while the newer ecosystems are scrambling to backfill their capabilities and will probably never match the breadth and depth, before falling out of fashion and fading away. I’ll be interested in any comments arguing why I’m wrong to discount them, or any pointers to things that are sufficiently advanced to be worth taking a closer look at.

We are happy to announce the opam 2.0.0 final release candidate!

This release features a few bugfixes over Release Candidate 3. It will be promoted to 2.0.0 proper within a few weeks, when the official repository format switches from 1.2.0 to 2.0.0. After that date, updates to the 1.2.0 repository may become limited, as new features are getting used in packages.

It is safe to update as soon as you see fit, since opam 2.0.0 supports the older formats. See the Upgrade Guide for details about the …

We are happy to announce the opam 2.0.0 final release candidate!

This release features a few bugfixes over Release Candidate 3. It will be promoted to 2.0.0 proper within a few weeks, when the official repository format switches from 1.2.0 to 2.0.0. After that date, updates to the 1.2.0 repository may become limited, as new features are getting used in packages.

It is safe to update as soon as you see fit, since opam 2.0.0 supports the older formats. See the Upgrade Guide for details about the new features and changes. If you are a package maintainer, you should keep publishing as before for now: the roadmap for the repository upgrade will be detailed shortly.

The opam.ocaml.org pages have also been refreshed a bit, and the new version showing the 2.0.0 branch of the repository is already online at http://opam.ocaml.org/2.0-preview/ (report any issues here).

1. From binaries: run

   sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)

   or download manually from the Github "Releases" page to your PATH. In this case, don't forget to run opam init --reinit -ni to enable sandboxing if you had version 2.0.0~rc manually installed.

2. From source, using opam:

   opam update; opam install opam-devel

   (then copy the opam binary to your PATH as explained, and don't forget to run opam init --reinit -ni to enable sandboxing if you had version 2.0.0~rc manually installed)

3. From source, manually: see the instructions in the README.

We hope you enjoy this new version, and remain open to bug reports and suggestions.

NOTE: this article is cross-posted on opam.ocaml.org and ocamlpro.com. Please head to the latter for the comments!

I have had the honor to lecture at the Oregon Programming Language Summer School 2018 on the topic of algebraic effects and handlers. The notes, materials and the lectures are available online:

• the GitHub repository with the course material
• the OPLSS lecture materials, including notes and video recordings of the lectures

I gave four lectures which started with the mathematics of algebraic theories, explained how they can be used to model computational effects, how we make a programming langu…

I have had the honor to lecture at the Oregon Programming Language Summer School 2018 on the topic of algebraic effects and handlers. The notes, materials and the lectures are available online:

• the GitHub repository with the course material
• the OPLSS lecture materials, including notes and video recordings of the lectures

I gave four lectures which started with the mathematics of algebraic theories, explained how they can be used to model computational effects, how we make a programming language out of them, and how to program with handlers.

OCamlPro is pleased to announce the latest update of TZScan (http://tzscan.io), its Tezos block explorer to ease the use of the Tezos network. TzScan is now ready for the protocol update scheduled for tomorrow. In addition to some minor bugfixes, the main novelties are:

• Displaying of obtained and expected rewards
• Adding of internal transactions of smart contracts
• Adding of delegation services
• Aliasing of known account and sponsors
• Improvements of UX, and faster navigation
• Improvements on deskt…

OCamlPro is pleased to announce the latest update of TZScan (http://tzscan.io), its Tezos block explorer to ease the use of the Tezos network. TzScan is now ready for the protocol update scheduled for tomorrow. In addition to some minor bugfixes, the main novelties are:

• Displaying of obtained and expected rewards
• Adding of internal transactions of smart contracts
• Adding of delegation services
• Aliasing of known account and sponsors
• Improvements of UX, and faster navigation
• Improvements on desktop, tablets and mobiles

We continue to maintain the alphanet and zeronet branches in parallel of the betanet.
We keep on working hard to improve and add new features to TzScan. Further enhancements and optimizations are to come. Enjoy and play with our explorer!
If you have any suggestions or bugs to report, please notify us at contact@tzscan.io

Bucket sort assumes input generated by a random process that distributes elements uniformly over the interval [0, 1).

The idea of bucket sort is to divide [0, 1) into n equal-sized subintervals or buckets, and then distribute the n input numbers into the buckets. To produce the output, sort the numbers in each bucket and then go through the buckets in order. Sorting a bucket can be done with insertion sort.

let rec insert x = function
  | [] -> [x]
  | h :: tl as ls ->
    if x <…

Bucket sort assumes input generated by a random process that distributes elements uniformly over the interval [0, 1).

The idea of bucket sort is to divide [0, 1) into n equal-sized subintervals or buckets, and then distribute the n input numbers into the buckets. To produce the output, sort the numbers in each bucket and then go through the buckets in order. Sorting a bucket can be done with insertion sort.

let rec insert x = function
  | [] -> [x]
  | h :: tl as ls ->
    if x < h then x :: ls else h :: insert x tl

let rec insertion_sort = function
  | [] | [_] as ls -> ls
  | h :: tl -> insert h (insertion_sort tl)

This code for bucket sort assumes the input is an n-element array a and that each element 0 ≤ a.(i) < 1. The code requires an auxillary array b.(0 .. n - 1) of lists (buckets).

let bucket_sort a =
  let n = Array.length a in
  let b = Array.make n [] in
  Array.iter
    (fun x ->
       let i =
         int_of_float (
           floor (float_of_int n *. x)
         ) in
        Array.set b i (x :: Array.get b i)
      ) a;
  Array.iteri
    (fun i l ->
       Array.set b i (insertion_sort l)
    ) b;
  Array.fold_left (fun acc bucket -> acc @ bucket) [] b
;;
bucket_sort [| 0.78; 0.17; 0.39; 0.26; 0.72; 0.94
             ; 0.21; 0.12; 0.23; 0.68|]

References:
[1] "Introduction to Algorithms" Section 9.4:Bucket Sort -- Cormen et. al. (Second ed.) 2001.

We are pleased to announce the release of a second release candidate for OPAM 2.0.0.

This new version brings us very close to a final 2.0.0 release, and in addition to many fixes, features big performance enhancements over the RC1.

Among the new features, we have squeezed in full sandboxing of package commands for both Linux and Mac OS, to protect our users from any misbehaving scripts.

NOTE: if upgrading manually from 2.0.0~rc, you need to run opam init --reinit -ni to enable sandboxing.

The ne…

We are pleased to announce the release of a second release candidate for OPAM 2.0.0.

This new version brings us very close to a final 2.0.0 release, and in addition to many fixes, features big performance enhancements over the RC1.

Among the new features, we have squeezed in full sandboxing of package commands for both Linux and Mac OS, to protect our users from any misbehaving scripts.

NOTE: if upgrading manually from 2.0.0~rc, you need to run opam init --reinit -ni to enable sandboxing.

The new release candidate also offers the possibility to setup a hook in your shell, so that you won’t need to run eval $(opam env) anymore. This is specially useful in combination with local switches, because with it enabled, you are guaranteed that running make from a project directory containing a local switch will use it.

The documentation has also been updated, and a preview of the opam 2 webpages can be browsed at http://opam.ocaml.org/2.0-preview/ (please report issues here). This provides the list of packages available for opam 2 (the 2.0 branch of opam-repository), including the compiler packages.

Installation instructions:

1. From binaries: run

   sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)

   or download manually from the Github “Releases” page to your PATH. In this case, don’t forget to run opam init --reinit -ni to enable sandboxing if you had version 2.0.0~rc manually installed.

2. From source, using opam:

   opam update; opam install opam-devel

   (then copy the opam binary to your PATH as explained, and don’t forget to run opam init --reinit -ni to enable sandboxing if you had version 2.0.0~rc manually installed)

3. From source, manually: see the instructions in the README.

Thanks a lot for testing out this new RC and reporting any issues you may find.

NOTE: this article is cross-posted on opam.ocaml.org and ocamlpro.com. Please head to the latter for comments!

In this blogpost we find out that it is possible to tweak the behavior of the Coq simpl tactic. We find it particularly useful when dealing with arithmetic goals on Z.

We just discovered an answer to a longstanding annoyance we faced when dealing with arithmetic Coq goals. Consider the following Coq goal, using integers on Z:

Require Import ZArith.
Open Scope Z_scope.

Goal forall a, 2 * a = 0 * a + a * 2.
  intros. simpl.

We call the simpl tactic to simplify 0 * a + ... into .... Unfort…

In this blogpost we find out that it is possible to tweak the behavior of the Coq simpl tactic. We find it particularly useful when dealing with arithmetic goals on Z.

We just discovered an answer to a longstanding annoyance we faced when dealing with arithmetic Coq goals. Consider the following Coq goal, using integers on Z:

Require Import ZArith.
Open Scope Z_scope.

Goal forall a, 2 * a = 0 * a + a * 2.
  intros. simpl.

We call the simpl tactic to simplify 0 * a + ... into .... Unfortunately, since * is defined by pattern matching on its first argument, simpl also unfolds 2 * a:

a : Z
============================
match a with
| 0 => 0
| Z.pos y' => Z.pos y'~0
| Z.neg y' => Z.neg y'~0
end = a * 2

This is both unconvenient and unsupported by automated tactics (such as omega or lia). One idea would be to make Z.mul opaque:

Opaque Z.mul.

This prevents both 2 * a and 0 * a from being simplified. This can be seen as a reasonable trade-off (omega will still be able to solve the goal).

However it also prevents reduction using eval compute, which breaks the PolTac library for example (interestingly, eval vm_compute ignores Opaque).

let x := (eval compute in (2*3)) in pose x.
(* x := 2*3 *)

let x := (eval vm_compute in (2*3)) in pose x.
(* x := 6 *)

A better solution can be found by reading the manual section for simpl (!). It is possible to customize for each definition the amount of unfolding performed by simpl. For example, the following instructs simpl to never unfold Z.mul:

Arguments Z.mul : simpl never.

Since this invocation only matters for simpl, eval compute and PolTac both continue to work.

let x := (eval compute in (2*3)) in pose x.
(* x := 6 *)

Goal forall a, 2 * a = 0 * a + a * 2.
  intros. simpl.
  (* 2 * a = 0 * a + a * 2 *)

And even better, we can achieve what we initially intended (which is to simplify away 0 * a), by instructing simpl to only unfold a definition if doing so does not introduce a match:

Arguments Z.mul : simpl nomatch.

Goal forall a, 2 * a = 0 * a + a * 2.
  intros. simpl.
  (* 2 * a = a * 2 *)

More configuration options are possible, and are thoroughly detailed in the manual page.

This article assumes familiarity with Dijkstra's shortest path algorithm. For a refresher, see [1]. The code assumes open Core is in effect and is online here.

The first part of the program organizes our thoughts about what we are setting out to compute. The signature summarizes the notion (for our purposes) of a graph definition in modular form. A module implementing this signature defines a type vertex_t for vertices, a type t for graphs and type extern_t

This article assumes familiarity with Dijkstra's shortest path algorithm. For a refresher, see [1]. The code assumes open Core is in effect and is online here.

The first part of the program organizes our thoughts about what we are setting out to compute. The signature summarizes the notion (for our purposes) of a graph definition in modular form. A module implementing this signature defines a type vertex_t for vertices, a type t for graphs and type extern_t : a representation of a t for interaction between an implemening module and its "outside world".

module type Graph_sig = sig
  type vertex_t [@@deriving sexp]
  type t [@@deriving sexp]
  type extern_t

  type load_error = [ `Duplicate_vertex of vertex_t ] [@@deriving sexp]
  exception Load_error of load_error [@@deriving sexp]

  val of_adjacency : extern_t -> [ `Ok of t | `Load_error of load_error ]
  val to_adjacency : t -> extern_t

  module Dijkstra : sig
    type state

    type error = [
      | `Relax of vertex_t
    ] [@@deriving sexp]
    exception Error of error [@@deriving sexp]

    val dijkstra : vertex_t -> t -> [ `Ok of state | `Error of error ]
    val d : state -> (vertex_t * float) list
    val shortest_paths : state -> (vertex_t * vertex_t list) list
  end

end

For reusability, the strategy for implementing graphs will be generic programming via functors over modules implementing s vertex type.

An implementation of the module type GRAPH defines a module type VERT which is required to provide a comparable type t. It further defines a module type S that is exactly module type Graph_sig above. Lastly, modules of type GRAPH provide a functor Make that maps any module of type VERT to new module of type S fixing extern_t to an adjacency list representation in terms of the native OCaml type 'a list and float to represent weights on edges.

module type GRAPH = sig
  module type VERT = sig
    type t[@@deriving sexp]
    include Comparable.S with type t := t
  end

  module type S = sig
    include Graph_sig
  end

  module Make : functor (V : VERT) ->
    S with type vertex_t = V.t
       and type extern_t = (V.t * (V.t * float) list) list
end

Implementation of module Graph is in outline this.

module Graph : GRAPH = struct
  module type VERT = sig
    type t[@@deriving sexp]
    include Comparable.S with type t := t
  end

  module type S = sig
    include Graph_sig
  end

  module Make : functor (V : VERT) ->
    S with type vertex_t = V.t
       and type extern_t = (V.t * (V.t * float) list) list
    =

    functor (V : VERT) -> struct
       ...
    end
end

Modules produced by applications of Make satisfy S. This requires suitable definitions of types vertext_t, t and extern_t. The modules Map and Set are available due to modules of type VERT being comparable in their type t.

      module Map = V.Map
      module Set = V.Set

      type vertex_t = V.t [@@deriving sexp]
      type t = (vertex_t * float) list Map.t [@@deriving sexp]
      type extern_t = (vertex_t * (vertex_t * float) list) list
      type load_error = [ `Duplicate_vertex of vertex_t ] [@@deriving sexp]
      exception Load_error of load_error [@@deriving sexp]

While the external representation extern_t of graphs is chosen to be an adjacency list representation in terms of association lists, the internal representation t is a vertex map of adjacency lists providing logarithmic loookup complexity. The conversion functions between the two representations "come for free" via module Map.

      let to_adjacency g = Map.to_alist g

      let of_adjacency_exn l =  match Map.of_alist l with
        | `Ok t -> t
        | `Duplicate_key c -> raise (Load_error (`Duplicate_vertex c))

      let of_adjacency l =
        try
          `Ok (of_adjacency_exn l)
        with
        | Load_error err -> `Load_error err

At this point the "scaffolding" for Dijkstra's algorithm, that part of GRAPH dealing with the representation of graphs is implemented.

The interpretation of Dijkstra's algorithm we adopt is functional : the idea is we loop over vertices relaxing their edges until all shortest paths are known. What we know on any recursive iteration of the loop is a current "state" (of the computation) and each iteration produces a new state. This next definition is the formal definition of type state.

      module Dijkstra = struct

        type state = {
          src    :                  vertex_t
        ; g      :                         t
        ; d      :               float Map.t
        ; pred   :            vertex_t Map.t
        ; s      :                     Set.t
        ; v_s    : (vertex_t * float) Heap.t
        }

• src : vertex_t, the source vertex;
• g : t, G the graph;
• d : float Map.t, d the shortest path weight estimates;
• pre : vertex_t Map.t, π the predecessor relation;
• s : Set.t, the set S of nodes for which the lower bound shortest path weight is known;
• v_s : (vertex_t * float) Heap.t, V - {S}, , the set of nodes of g for which the lower bound of the shortest path weight is not yet known ordered on their estimates.

Function invocation init src g compuates an initial state for the graph g containing the source node src. In the initial state, d is everywhere ∞ except for src which is 0. Set S (i.e. s) and the predecessor relation π (i.e. pred) are empty and the set V - {S} (i.e. v_s) contains all nodes.

        let init src g =
          let init x = match V.equal src x with
            | true -> 0.0 | false -> Float.infinity in
          let d = List.fold (Map.keys g) ~init:Map.empty
              ~f:(fun acc x -> Map.set acc ~key:x ~data:(init x)) in
          {
            src
          ; g
          ; s = Set.empty
          ; d
          ; pred = Map.empty
          ; v_s = Heap.of_list (Map.to_alist d)
                ~cmp:(fun (_, e1) (_, e2) -> Float.compare e1 e2)
          }

Relaxing an edge (u, v) with weight w (u, v) tests whether the shortest path to v so far can be improved by going through u and if so, updating d (v) and π (v) accordingly.

        type error = [
          | `Relax of vertex_t
        ] [@@deriving sexp]
        exception Error of error [@@deriving sexp]

        let relax state (u, v, w) =
          let {d; pred; v_s; _} = state in
          let dv = match Map.find d v with
            | Some dv -> dv
            | None -> raise (Error (`Relax v)) in
          let du = match Map.find d u with
            | Some du -> du
            | None -> raise (Error (`Relax u)) in
          if dv > du +. w then
            let dv = du +. w in
            (match Heap.find_elt v_s ~f:(fun (n, _) -> V.equal n v) with
            | Some tok -> ignore (Heap.update v_s tok (v, dv))
            | None -> raise (Error (`Relax v))
            );
            { state with
              d = Map.change d v
                  ~f:(function
                      | Some _ -> Some dv
                      | None -> raise (Error (`Relax v))
                    )
            ; pred = Map.set (Map.remove pred v) ~key:v ~data:u
            }
          else state

One iteration of the body of the loop of Dijkstra's algorithm consists of the node in V - {S} with the least shortest path weight estimate being moved to S and its edges relaxed.

        let dijkstra_exn src g =
          let rec loop ({s; v_s; _} as state) =
            match Heap.is_empty v_s with
            | true -> state
            | false ->
              let u = fst (Heap.pop_exn v_s) in
              loop (
                List.fold (Map.find_exn g u)
                  ~init:{ state with s = Set.add s u }
                  ~f:(fun state (v, w) -> relax state (u, v, w))
              )
          in loop (init src g)

        let dijkstra src g =
          try
            `Ok (dijkstra_exn src g)
          with
          | Error err -> `Error err

The shortest path estimates contained by a value of state is given by the projection d.

        let d state = Map.to_alist (state.d)

The shortest paths themselves are easily computed as,

   let path state n =
          let rec loop acc x =
            (match V.equal x state.src with
            | true -> x :: acc
            | false -> loop (x :: acc) (Map.find_exn state.pred x)
            ) in
          loop [] n

        let shortest_paths state =
          List.map (Map.keys state.g) ~f:(fun n -> (n, path state n))
      end
    end

The following program produces a concrete instance of the shortest path problem (with some evaluation output from the top-level).

module G : Graph.S with
  type vertex_t = char and type extern_t = (char * (char * float) list) list
  =
  Graph.Make (Char)

let g : G.t =
  match G.of_adjacency
          [ 's', ['u',  3.0; 'x', 5.0]
          ; 'u', ['x',  2.0; 'v', 6.0]
          ; 'x', ['v',  4.0; 'y', 6.0; 'u', 1.0]
          ; 'v', ['y',  2.0]
          ; 'y', ['v',  7.0]
          ]
  with
  | `Ok g -> g
  | `Load_error e -> failwiths "Graph load error : %s" e G.sexp_of_load_error
;;
let s = match (G.Dijkstra.dijkstra 's' g) with
  | `Ok s -> s
  | `Error e -> failwiths "Error : %s" e G.Dijkstra.sexp_of_error

;; G.Dijkstra.d s
- : (char * float) list =
[('s', 0.); ('u', 3.); ('v', 9.); ('x', 5.); ('y', 11.)]

;; G.Dijkstra.shortest_paths s
- : (char * char list) list =
[('s', ['s']); ('u', ['s'; 'u']); ('v', ['s'; 'u'; 'v']); ('x', ['s'; 'x']);
 ('y', ['s'; 'x'; 'y'])]

References:
[1] "Introduction to Algorithms" Section 24.3:Dijkstra's algorithm -- Cormen et. al. (Second ed.) 2001.

A new release of Alt-Ergo (version 2.2.0) is available.

You can get it from Alt-Ergo’s website. An OPAM package for it will be published in the next few days.

The major novelty of this release is a new experimental front-end that supports the SMT-LIB 2 language, extended prenex polymorphism. This extension is implemented as a standalone library, and is available here: https://github.com/Coquera/psmt2-frontend

The full list of CHANGES is available here. As usual, do not hesitate to report b…

A new release of Alt-Ergo (version 2.2.0) is available.

You can get it from Alt-Ergo’s website. An OPAM package for it will be published in the next few days.

The major novelty of this release is a new experimental front-end that supports the SMT-LIB 2 language, extended prenex polymorphism. This extension is implemented as a standalone library, and is available here: https://github.com/Coquera/psmt2-frontend

The full list of CHANGES is available here. As usual, do not hesitate to report bugs, to ask questions, or to give your feedback!

Original posted on linse's blog.

Image by Luc Viatour / https://Lucnix.be

In March 2018, I attended my first MirageOS hack retreat in Morrocco. MirageOS is a library operating system which allows everyone to build very small, specialized operating system kernels that are intended to run directly on the virtualization layer. The application code itself is the guest operating system kernel, and can be deployed at scale without the need for an extra containerization step in between. It is written …

Original posted on linse's blog.

Image by Luc Viatour / https://Lucnix.be

In March 2018, I attended my first MirageOS hack retreat in Morrocco. MirageOS is a library operating system which allows everyone to build very small, specialized operating system kernels that are intended to run directly on the virtualization layer. The application code itself is the guest operating system kernel, and can be deployed at scale without the need for an extra containerization step in between. It is written in OCaml and each kernel is built only with exactly the code that is necessary for the particular application. A pretty different approach from traditional operating systems. Linux feels huge all of a sudden.

I flew in from New York via Casablanca to Marrakesh, and then took a cab to the city center, to the main square, Jemaa El Fnaa. At Cafe de France, Hannes was picking me up and we walked back through the labyrinth of the Medina to the hostel Riad "Priscilla" where we lived with about 20 MirageOS folks, two turtles and a dog. We ate some food, and there were talks about Mirage's quickcheck-style fuzzing library Crowbar, and an API realized on top of a message queue written in OCaml.

Coming from compiler construction in Haskell and building "stateless" services for information retrieval in Scala, I have a good grasp of functional programming. The funny problem is I don't know much about OCaml yet.

At Etsy, I was part of the Core Platform team where we first used hhvm (Facebook's hip-hop virtual machine) on the API cluster, and then advocated to use their gradually typed "hack" language to introduce typing to the gigantic PHP codebase at Etsy. Dan Miller and I added types to the codebase with Facebook's hackificator, but then PHP 7 added the possibility of type annotations and great speedups, and PHP's own static analyzer phan was developed by Rasmus Lerdorf and Andrew Morrison to work with PHP's types. We abandoned the hackification approach. Why is this interesting? These were my first encounters with OCaml! The hack typechecker is written in OCaml, and Dan and I have read it to understand the gradual typing approach. Also, we played with pfff, a tool written in OCaml that allows structural edits on PHP programs, based on the abstact syntax tree. I made a list to translate between Haskell and OCaml syntax, and later Maggie Zhou and I used pfff to unify the syntax of several hundred endpoints in Etsy's internal API.

At the MirageOS retreat, I started my week reading "Real World OCaml", but got stuck because the examples did not work with the buildsystem used in the book. Stephen helped me to find a workaround, I made a PR to the book but it was closed since it is a temporary problem. Also, I started reading about OCaml's "lwt" library for concurrent programming. The abbreviation stands for lightweight threads and the library provides a monadic way to do multithreading, really similar to twitter futures in Scala. Asynchronous calls can be made in a thread, which then returns at some point when the call was successful or failed. We can do operations "inside" lwt with bind (>>=) in the same way we can flatMap over Futures in scala. The library also provides ways to run multiple threads in sequence or in parallel, and to block and wait. In the evening, there was a talk about a high-end smart card that based on a private start value can provide a succession of keys. The hardware is interesting, being the size of a credit card it has a small keypad and a screen. Some banks use these cards already (for their TAN system?), and we all got a sample card to play with.

One day I went swimming with Lix and Reynir, which was quite the adventure since the swimming pool was closed and we were not sure what to do. We still made it to the part that was still open, swam a lot and then got a cake for Hannes birthday which lead to a cake overflow since there were multiple cakes and an awesome party with candles, food and live music already. :D Thanks everyone for organizing!! Happy birthday Hannes!

I started reading another book, "OCaml from the very beginning", and working through it with Kugg. This book was more focused on algorithms and the language itself than on tooling and libraries, and the exercises were really fun to solve. Fire up OCaml's REPL utop and go! :D

At the same time I started reading the code for solo5 to get an understanding of the underlying hypervisor abstraction layer and the backends we compile to. This code is really a pleasure to read. It is called solo5 because of MirageOS's system calls, initially a set of 5 calls to the hypervisor, called hypercalls which sounds really futuristic. :D

So that's the other fun problem: I don't know too much about kernel programming yet. I did the Eudyptula (Linux kernel) challenge, an email-based challenge that sends you programming quests to learn about kernel programming. Over the course of the challenge, I've made my own Linux kernel module that says "Hello world!" but I have not built anything serious yet.

The next things I learned were configuring and compiling a MirageOS unikernel. Hannes showed me how this works. The config system is powerful and can be tailored to the unikernel we are about to build, via a config file. After configuring the build, we can build the kernel for a target backend of our choice. I started out with compiling to Unix, which means all network calls go through unix pipes and the unikernel runs as a simple unix binary in my host system, which is really useful for testing.

The next way to run MirageOS that I tried was running it in ukvm. For this setup you have to change the networking approach so that you can talk from the host system to you unikernel inside ukvm. In Linux you can use the Tun/Tap loopback interface for networking to wire up this connection.

We had a session with Jeremie about our vision for MirageOS which was super fun, and very interesting because people have all kinds of different backgrounds but the goals are still very aligned.

Another thing I learned was how to look at network traffic with wireshark. Sidney and I had previously recorded a TLS handshake with tcpdump and looked at the binary data in the pcap file with "hexfiend" next to Wikipedia to decode what we saw. Derpeter gave me a nice introduction about how to do this with wireshark, which knows about most protocols already and will do the decoding of the fields for us. We talked about all layers of the usual stack, other kinds of internet protocols, the iptables flow, and bgp / peeringDB. Quite interesting and I feel I have a pretty good foundational understanding about how the internet actually works now.

During the last days I wanted to write a unikernel that does something new, and I thought about monitoring, as there is no monitoring for MirageOS yet. I set up a grafana on my computer and sent some simple data packets to grafana from a unikernel, producing little peaks in a test graph. Reynir and I played with this a bit and restructured the program.

After this, the week was over, I walked back to Jemaa el Fnaa with Jeremie, I feel I learned a ton and yet am still at the very beginning, excited what to build next. On the way back I got stuck in a weird hotel in Casablanca due to the flight being cancelled, where I bumped into a Moroccan wedding and met some awesome travelling women from Brazil and the US who also got stuck. All in all a fun adventure!

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!

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.

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