Joachim Breitner

Blog

Verifying the code of the Internet Identity service

Published 2021-06-02 in sections English, Digital world.

The following post was meant to be posted at https://forum.dfinity.org/, but that discourse instance didn’t like it; maybe too much inline code, so I’m posting it here instead. To my regular blog audience, please excuse the lack of context. Please comment at the forum post. The text was later also posted on the DFINITY medium blog

You probably have used https://identity.ic0.app/ to log into various applications (the NNS UI, OpenChat etc.) before, and if you do that, you are trusting this service to take good care of your credentials. Furthermore, you might want to check that the Internet Identity is really not tracking you. So you want to know: Is this really running the code we claim it to run? Of course the following applies to other canisters as well, but I’ll stick to the Internet Identity in this case.

I’ll walk you through the steps of verifying that:

Find out what is running

A service on the Internet Computer, i.e. a canister, is a WebAssembly module. The Internet Computer does intentionally not allow you to just download the Wasm code of any canisters, because maybe some developer wants to keep their code private. But it does expose a hash of the Wasm module. The easiest way to get it is using dfx:

$ dfx canister --no-wallet --network ic info rdmx6-jaaaa-aaaaa-aaadq-cai
Controller: r7inp-6aaaa-aaaaa-aaabq-cai
Module hash: 0xd4af9277f3e8d26fd8cdc7874a9f47b6456587fbb2a64d61b6b6880d144d3c04

The “controller” here is the canister id of the governance canister. This tells you that the Internet Identity is controlled by the Network Nervous System (NNS), and its code can only be changed via proposals that are voted on. This is good; if the controller was just, say, me, I could just change the code of the Internet Identity and take over all your identities.

The “Module hash” is the SHA-256 hash of the .wasm that was deployed. So let’s follow that trace.

Finding the right commit

Since upgrades to the Internet Identity are done via proposals to the NNS, we should find a description of such a proposal in the https://github.com/ic-association/nns-proposals repository, in the proposals/network_canister_management directory.

Github’s list of recent NNS proposals

Github’s list of recent NNS proposals

We have to find the latest proposal upgrading the Internet Identity. The folder unfortunately contains proposals for many canisters, and the file naming isn’t super helpful. I usually go through the list from bottom and look at the second column, which contains the title of the latest commit creating or modifying a file.

In this case, the second to last is the one we care about: https://github.com/ic-association/nns-proposals/blob/main/proposals/network_canister_management/20210527T2203Z.md. This file lists rationales, gives an overview of changes and, most importantly, says that bd51eab is the commit we are upgrading to.

The file also says that the wasm hash is d4a…c04, which matches what we saw above. This is good: it seems we really found the youngest proposal upgrading the Internet Identity, and that the proposal actually went through.

WARNING: If you are paranoid, don’t trust this file. There is nothing preventing a proposal proposer to create a file pointing to one revision, but actually including other code in the proposal. That’s why the next steps are needed.

Getting the source

Now that we have the revision, we can get the source and check out revision bd51eab:

/tmp $ git clone https://github.com/dfinity/internet-identity
Klone nach 'internet-identity' ...
remote: Enumerating objects: 3959, done.
remote: Counting objects: 100% (344/344), done.
remote: Compressing objects: 100% (248/248), done.
remote: Total 3959 (delta 161), reused 207 (delta 92), pack-reused 3615
Empfange Objekte: 100% (3959/3959), 6.05 MiB | 3.94 MiB/s, Fertig.
Löse Unterschiede auf: 100% (2290/2290), Fertig.
/tmp $ cd internet-identity/
/tmp/internet-identity $ git checkout bd51eab
/tmp/internet-identity $ git log --oneline -n 1
bd51eab (HEAD, tag: mainnet-20210527T2203Z) Registers the seed phrase before showing it (#301)

In the last line you see that the Internet Identity team has tagged that revision with a tag name that contains the proposal description file name. Very tidy!

Reproducing the build

The README.md has the following build instructions:

Official build

The official build should ideally be reproducible, so that independent parties can validate that we really deploy what we claim to deploy.

We try to achieve some level of reproducibility using a Dockerized build environment. The following steps should build the official Wasm image

docker build -t internet-identity-service .
docker run --rm --entrypoint cat internet-identity-service /internet_identity.wasm > internet_identity.wasm
sha256sum internet_identity.wasm

The resulting internet_identity.wasm is ready for deployment as rdmx6-jaaaa-aaaaa-aaadq-cai, which is the reserved principal for this service.

It actually suffices to run the first command, as it also prints the hash (we don’t need to copy the .wasm out of the Docker canister):

/tmp/internet-identity $ docker build -t internet-identity-service .
…
Step 26/26 : RUN sha256sum internet_identity.wasm
 ---> Running in 1a04644b544c
d4af9277f3e8d26fd8cdc7874a9f47b6456587fbb2a64d61b6b6880d144d3c04  internet_identity.wasm
Removing intermediate container 1a04644b544c
 ---> bfe6a63a7980
Successfully built bfe6a63a7980
Successfully tagged internet-identity-service:latest

Success! The hashes match.

You don’t believe me? Try it yourself (and let us know if you get a different hash, maybe I got hacked). This may fail if you have too little RAM configured for Docker, 8GB should be enough.

At this point you have a trust path from the code sitting in front of you to the Internet Identity running at https://identity.ic0.app, including the front-end code, and you can start auditing the source code.

What about the canister id?

If you payed close attention you might have noticed that we got the module has for canister rdmx6-jaaaa-aaaaa-aaadq-cai, but we are accessing a web application at https://identity.ic0.app. So where is this connection?

In the future, I expect some form of a DNS-like “nice host name registry” on the Internet Computer that stores a mapping from nice names to canister ids, and that you will be able to query that to for “which canister serves rdmx6-jaaaa-aaaaa-aaadq-cai” in a secure way (e.g. using certified variables). But since we don’t have that yet, but still want you to be able to use a nice name for the Internet Identity (and not have to change the name later, which would cause headaches), we have hard-coded this mapping for now.

The relevant code here is the “Certifying Service Worker” that your browser downloads when accessing any *.ic0.app URL. This piece of code will then intercept all requests to that domain, map it to an query call, and then use certified variables to validate the response. And indeed, the mapping is in the code there:

const hostnameCanisterIdMap: Record<string, [string, string]> = {
  'identity.ic0.app': ['rdmx6-jaaaa-aaaaa-aaadq-cai', 'ic0.app'],
  'nns.ic0.app': ['qoctq-giaaa-aaaaa-aaaea-cai', 'ic0.app'],
  'dscvr.ic0.app': ['h5aet-waaaa-aaaab-qaamq-cai', 'ic0.page'],
};

What about other canisters?

In principle, the same approach works for other canisters, whether it’s OpenChat, the NNS canisters etc. But the details will differ, as every canister developer might have their own way of

  • communicating the location and revision of the source for their canisters
  • building the canisters

In particular, without a reproducible way of building the canister, this will fail, and that’s why projects like https://reproducible-builds.org/ are so important in general.

Don’t think, just defunctionalize

Published 2020-12-22 in sections English, Haskell.

TL;DR: CPS-conversion and defunctionalization can help you to come up with a constant-stack algorithm.

Update: Turns out I inadvertedly plagiarized the talk The Best Refactoring You’ve Never Heard Of by James Koppel. Please consider this a form of sincere flattery.

The starting point

Today, I’ll take you on a another little walk through the land of program transformations. Let’s begin with a simple binary tree, with value of unknown type in the leaves, as well as the canonical map function:

data T a = L a | B (T a) (T a)

map1 :: (a -> b) -> T a -> T b
map1 f (L x) = L (f x)
map1 f (B t1 t2) = B (map1 f t1) (map1 f t2)

As you can see, this map function is using the program stack as it traverses the tree. Our goal is now to come up with a map function that does not use the stack!

Why? Good question! In Haskell, there wouldn’t be a strong need for this, as the Haskell stack is allocated on the heap, just like your normal data, so there is plenty of stack space. But in other languages or environments, the stack space may have a hard limit, and it may be advised to not use unbounded stack space.

That aside, it’s a fun exercise, and that’s sufficient reason for me.

(In the following, I assume that tail-calls, i.e. those where a function end with another function call, but without modifying its result, do not actually use stack space. Once all recursive function calls are tail calls, the code is equivalent to an imperative loop, as we will see.)

Think?

We could now just stare at the problem (rather the code), and try to come up with a solution directly. We’d probably think “ok, as I go through the tree, I have to remember all the nodes above me… so I need a list of those nodes… and for each of these nodes, I also need to remember whether I am currently processing the left child, and yet have to look at the right one, or whether I am done with the left child… so what do I have to remember about the current node…?”

… ah, my brain spins already. Maybe eventually I figure it out, but why think when we can derive the solution? So let’s start with above map1, and rewrite it, in several, mechanical, steps into a stack-less, tail-recursive solution.

Go!

Before we set out, let me rewrite the map function using a local go helper, as follows:

map2 :: forall a b. (a -> b) -> T a -> T b
map2 f t = go t
  where
    go :: T a -> T b
    go (L x) = L (f x)
    go (B t1 t2) = B (go t1) (go t2)

This transformation (effectively the “static argument transformation”) has the nice advantage that we do not have to pass f around all the time, and that when we copy the function, I only have to change the top-level name, but not the names of the inner functions.

Also, I find it more aesthetically pleasing.

CPS

A blunt, effective tool to turn code that is not yet using tail-calls into code that only uses tail-calls is use continuation-passing style. If we have a function of type … -> t, we turn it into a function of type … -> (t -> r) -> r, where r is the type of the result we want at the very end. This means the function now receives an extra argument, often named k for continuation, and instead of returning some x, the function calls k x.

We can apply this to our go function. Here, both t and r happen to be T b; the type of finished trees:

map3 :: forall a b. (a -> b) -> T a -> T b
map3 f t = go t (\r -> r)
  where
    go :: T a -> (T b -> T b) -> T b
    go (L x) k  = k (L (f x))
    go (B t1 t2) k  = go t1 (\r1 -> go t2 (\r2 -> k (B r1 r2)))

Note that when initially call go, we pass the identity function (\r -> r) as the initial continuation.

Behold, suddenly all function calls are in tail position, and this codes does not use stack space! Technically, we are done, although it is not quite satisfying; all these lambdas floating around obscure the meaning of the code, are maybe a bit slow to execute, and also, we didn’t really learn much yet. This is certainly not the code we would have writing after “thinking hard”.

Defunctionalization

So let’s continue rewriting the code to something prettier, simpler. Something that does not use lambdas like this.

Again, there is a mechanical technique that can help it. It likely won't make the code prettier, but it will get rid of the lambdas, so let’s do that an clean up later.

The technique is called defunctionalization (because it replaces functional values by plain data values), and can be seen as a form of refinement.

Note that we pass around vales of type (T b -> T b), but we certainly don’t mean the full type (T b -> T b). Instead, only very specific values of that type occur in our program, So let us replace (T b -> T b) with a data type that contains representatives of just the values we actually use.

  1. We find at all values of type (T b -> T b). These are:

    • (\r -> r)
    • (\r1 -> go t2 (\r2 -> k (B r1 r2)))
    • (\r2 -> k (B r1 r2))
  2. We create a datatype with one constructor for each of these:

     data K = I | K1 | K2

    (This is not complete yet.)

  3. We introduce an interpretation function that turns a K back into a (T b -> T b):

    eval :: K -> (T b -> T b)
    eval = (* TBD *)
  4. In the function go, instead of taking a parameter of type (T b -> T b), we take a K. And when we actually use the continuation, we have to turn the K back to the function using eval:

    go :: T a -> K a b -> T b
    go (L x) k  = eval k (L (f x))
    go (B t1 t2) k = go t1 K1
    We also do this to the code fragments identified in the first step; these become:
    • (\r -> r)
    • (\r1 -> go t2 K2)
    • (\r2 -> eval k (B r1 r2))
  5. Now we complete the eval function: For each constructor, we simply map it to the corresponding lambda from step 1:

    eval :: K -> (T b -> T b)
    eval I = (\r -> r)
    eval K1 = (\r1 -> go t2 K2)
    eval K2 = (\r2 -> eval k (B r1 r2))
  6. This doesn’t quite work yet: We have variables on the right hand side that are not bound (t2, r1, k). So let’s add them to the constructors K1 and K2 as needed. This also changes the type K itself; it now needs to take type parameters.

This leads us to the following code:

data K a b
  = I
  | K1 (T a) (K a b)
  | K2 (T b) (K a b)

map4 :: forall a b. (a -> b) -> T a -> T b
map4 f t = go t I
  where
    go :: T a -> K a b -> T b
    go (L x) k  = eval k (L (f x))
    go (B t1 t2) k  = go t1 (K1 t2 k)

    eval :: K a b -> (T b -> T b)
    eval I = (\r -> r)
    eval (K1 t2 k) = (\r1 -> go t2 (K2 r1 k))
    eval (K2 r1 k) = (\r2 -> eval k (B r1 r2))

Not really cleaner or prettier, but everything is still tail-recursive, and we are now working with plain data.

We like lists

To clean it up a little bit, we can notice that the K data type really is just a list of values, where the values are either T a or T b. We do not need a custom data type for this! Instead of our K, we can just use the following, built from standard data types:

type K' a b = [Either (T a) (T b)]

Now I replace I with [], K1 t2 k with Left t2 : k and K2 r1 k with Right r1 : k. I also, very suggestively, rename go to down and eval to up:

map5 :: forall a b. (a -> b) -> T a -> T b
map5 f t = down t []
  where
    down :: T a -> K' a b -> T b
    down (L x) k  = up k (L (f x))
    down (B t1 t2) k  = down t1 (Left t2 : k)

    up :: K' a b -> T b -> T b
    up [] r = r
    up (Left  t2 : k) r1 = down t2 (Right r1 : k)
    up (Right r1 : k) r2 = up k (B r1 r2)

At this point, the code suddenly makes more sense again. In fact, I can try to verbalize it:

As we traverse the tree, we have to remember for all parent nodes, whether there is still something Left to do when we come back to it (so we remember a T a), or if we are done with that (so we have a T b). This is the list K' a b.

We begin to go down the left of the tree (noting that the right siblings are still left to do), until we hit a leaf. We transform the leaf, and then go up.

If we go up and hit the root, we are done. Else, if we go up and there is something Left to do, we remember the subtree that we just processed (as that is already in the Right form), and go down the other subtree. But if we go up and there is nothing Left to do, we put the two subtrees together and continue going up.

Quite neat!

The imperative loop

At this point we could stop: the code is pretty, makes sense, and has the properties we want. But let’s turn the dial a bit further and try to make it an imperative loop.

We know that if we have a single tail-recursive function, then that’s equivalent to a loop, with the function’s parameter turning into mutable variables. But we have two functions!

It turns out that if you have two functions a -> r and b -> r that have the same return type (which they necessarily have here, since we CPS-converted them further up), then those two functions are equivalent to a single function taking “a or b”, i.e. Either a b -> r. This really nothing else than the high-school level algebra rule of ra ⋅ rb = ra + b.

So (after reordering the arguments of down to put T b first) we can rewrite the code as

map6 :: forall a b. (a -> b) -> T a -> T b
map6 f t = go (Left t) []
  where
    go :: Either (T a) (T b) -> K' a b -> T b
    go (Left (L x))     k        = go (Right (L (f x))) k
    go (Left (B t1 t2)) k        = go (Left t1) (Left t2 : k)
    go (Right r)  []             = r
    go (Right r1) (Left  t2 : k) = go (Left t2) (Right r1 : k)
    go (Right r2) (Right r1 : k) = go (Right (B r1 r2)) k

Do you see the loop yet? If not, maybe it helps to compare it with the following equivalent imperative looking pseudo-code:

mapLoop :: forall a b. (a -> b) -> T a -> T b
mapLoop f t {
  var node = Left t;
  var parents = [];
  while (true) {
    switch (node) {
      Left (L x) -> node := Right (L (f x))
      Left (B t1 t2) -> node := Left t1; parents.push(Left t2)
      Right r1 -> {
        if (parents.len() == 0) {
          return r1;
        } else {
          switch (parents.pop()) {
            Left t2  -> node := Left t2; parents.push(Right r1);
            Right r2 -> node := Right (B r1 r2)
          }
        }
      }
    }
  }
}

Conclusion

I find it enlightening to see how apparently very different approaches to a problem (recursive, lazy functions and imperative loops) are connected by a series of rather mechanical transformations. When refactoring code, it is helpful to see if one can conceptualize the refactoring as one of those mechanical steps (refinement, type equivalences, defunctionalization, cps conversion etc.)

If you liked this post, you might enjoy my talk The many faces of isOrderedTree, which I have presented at MuniHac 2019 and Haskell Love 2020.

Named goals in Coq

Published 2020-12-05 in sections English, Coq.

TL;DR: Some mildly tricky tricks allow you to select subgoals by name, like in Isabelle. This leads to more readable proofs, and proofs that are more robust against changes.

The need for case names

Consider the following Coq proof, right out of the respected Software Foundations book, Chapter “Inductively Defined Propositions” (and slightly simplified):

Lemma star_app: forall T (s1 s2 : list T) (re : reg_exp T),
  s1 =~ Star re ->
  s2 =~ Star re ->
  s1 ++ s2 =~ Star re.
Proof.
  intros T s1 s2 re H1.
  remember (Star re) as re'.
   generalize dependent s2.
  induction H1.
  - (* MEmpty *) discriminate.
  - (* MChar *) discriminate.
  - (* MApp *) discriminate.
  - (* MUnionL *) discriminate.
  - (* MUnionR *) discriminate.
  - (* MStar0 *)
    injection Heqre' as Heqre''. intros s H. apply H.
  - (* MStarApp *)
    injection Heqre' as Heqre''.
    intros s3 H1. rewrite <- app_assoc.
    apply MStarApp.
    + apply H1_.
    + apply IHexp_match2.
      * rewrite Heqre''. reflexivity.
      * apply H1.
Qed.

This is a very typical example for a proof by induction over an inductively defined relation (in this case, the relations s =~ re which indicates that the string s matches the regular expression re): After some preparation, the invocation of a tactic like induction (could also be inversion or others) creates a number of new goals, one of for each rule of the relation. Then the modern(!) Coq user uses proof bullets to focus the goals, one after another, in order, to solve them.

We can see from this example that proof bullets (which were a big improvement) are not quite satisfactory, and the author of this proof felt the need to annotate each subproof with the case it corresponds to.

But these are mere comments! This is unsatisfactory, as there is nothing keeping them correct as my proof changes. And anyone who came to Coq from Isabelle is just flabbergasted that the state of art in Coq is still at that level…

So, wouldn’t it be great if

  • I could focus goals by their name (e.g. MEmpty)
  • Focus them in any order (so that refactoring of my data types do not break my proofs)
  • This even worked when simultaneously inducting over or inverting multiple relations?

Simulating named goals in Coq

Well, with a few tricks we can! It just takes three simple steps:

  1. I load a small file full of hacks (explained below):

    Require Import NamedCases.
  2. This allows me to prefix the type of the constructors of the inductive relations (i.e. the rules of the relation) with case <name>, …, as follows:

    Reserved Notation "s =~ re" (at level 80).
    Inductive exp_match {T} : list T -> reg_exp T -> Prop :=
      | MEmpty:
        case empty,
        [] =~ EmptyStr
      | MChar:
        case char,
        forall x,
        [x] =~ (Char x)
      | MApp:
        case app,
        forall s1 re1 s2 re2
        (H1 : s1 =~ re1)
        (H2 : s2 =~ re2),
        (s1 ++ s2) =~ (App re1 re2)
      | MUnionL:
        case union_l,
        forall s1 re1 re2
        (H1 : s1 =~ re1),
        s1 =~ (Union re1 re2)
      | MUnionR:
        case union_r,
        forall re1 s2 re2
        (H2 : s2 =~ re2),
        s2 =~ (Union re1 re2)
      | MStar0:
        case star0,
        forall re,
        [] =~ (Star re)
      | MStarApp:
        case star_app,
        forall s1 s2 re
        (H1 : s1 =~ re)
        (H2 : s2 =~ (Star re)),
        (s1 ++ s2) =~ (Star re)
      where "s =~ re" := (exp_match s re).

    This is the definition from the Software Foundations book; only the case <name>, lines are added.

  3. Now I can change the proof: After the induction tactic I use …; name_cases to name the cases, and then I can use the relatively new named goal focusing feature ([name]: { … }, which I suggested two years ago, and was implemented by Théo Zimmermann) to focus a specific case:

    Lemma star_app2: forall T (s1 s2 : list T) (re : reg_exp T),
      s1 =~ Star re ->
      s2 =~ Star re ->
      s1 ++ s2 =~ Star re.
    Proof.
      intros T s1 s2 re H1.
      remember (Star re) as re'.
       generalize dependent s2.
      induction H1; name_cases.
      [empty]: {
         discriminate.
      }
      [char]: {
         discriminate.
      }
      [app]: {
         discriminate.
      }
      [unionL]: {
         discriminate.
      }
      [unionR]: {
        discriminate.
      }
      [star0]: {
        injection Heqre' as Heqre''. intros s H. apply H.
      }
      [starApp]: {
        injection Heqre' as Heqre''.
        intros s3 H1. rewrite <- app_assoc.
        apply MStarApp; clear_names.
        + apply H1_.
        + apply IHexp_match2.
          * rewrite Heqre''. reflexivity.
          * apply H1.
       }
    Qed.

    The comments have turned into actual names!

Goal focusing is now just much more reliable. For example, let me try to discharge the boring cases by using …; try discriminate after the induction. This means there are suddenly only two goals left. With bullets, the first bullet would now suddenly focus a different goal, and my proof script would likely fail somewhere. With named goals, I get a helpful error message No such goal: empty and I can’t even enter the first subproof. So let me delete these goals and, just to show off, focus the remaining goals in the “wrong” order:

Lemma star_app: forall T (s1 s2 : list T) (re : reg_exp T),
  s1 =~ Star re ->
  s2 =~ Star re ->
  s1 ++ s2 =~ Star re.
Proof.
  intros T s1 s2 re H1.
  remember (Star re) as re'.
   generalize dependent s2.
  induction H1; name_cases; try discriminate.
  [starApp]: {
    injection Heqre' as Heqre''.
    intros s3 H1. rewrite <- app_assoc.
    apply MStarApp; clear_names.
    + apply H1_.
    + apply IHexp_match2.
      * rewrite Heqre''. reflexivity.
      * apply H1.
   }
  [star0]: {
    injection Heqre' as Heqre''. intros s H. apply H.
  }
Qed.

I did not explain the clear_names tactic yet that I had to use after apply MStarApp. What I am showing here is a hack, and it shows… these case names are extra hypothesis (of a trivially true type CaseName), and this tactic gets rid of it.

Even better than Isabelle

The above even works when there are multiple inductions/inversions involved. To give an example, let’s introduce another inductive predicate, and begin proving a lemma that one can do by induction on one and inversion on the other predicate.

Inductive Palindrome {T} : list T -> Prop :=
| EmptyPalin:
  case emptyP,
  Palindrome []
| SingletonPalin:
  case singletonP,
  forall x,
  Palindrome [x]
| GrowPalin:
  case growP,
  forall l x,
  Palindrome l -> Palindrome ([x] ++ l ++ [x])
.

Lemma palindrome_star_of_two:
  forall T (s : list T) x y,
  Palindrome s -> s =~ Star (App (Char x) (Char y)) ->
  s = [] \/ x = y.
Proof.
  intros T s x y HPalin HRe.
  induction HPalin; inversion HRe; name_cases.

At this point we have four open goals. Can you tell why there are four, and which ones they are?

Luckily, Show Existentials will tell us their names (and Coq 8.13 will just show them in the proof state window). These names not only help us focus the goal in a reliable way; they even assist us in understanding what goal we have to deal with. For example, the last goal arose from the GrowP rule and the StarApp rule. Neat!

  [emptyP_star0]: {
    left. reflexivity.
  }
  [emptyP_starApp]: {
     left. reflexivity.
  }
  [singletonP_starApp]: {
    inversion HRe; clear HRe.
    inversion H5; clear H5.
    inversion H10; clear H10.
    inversion H11; clear H11.
    subst.
    inversion H3.
  }
 [growP_starApp]: {
    admit. (* I did not complete the proof *)
 }

Under the hood (the hack)

The above actually works, but it works with a hack, and I wish that Coq’s induction tactic would just do the right thing here. I hope eventually this will be the case, and this section will just be curiosity… but until, it may actually be helpful.

  1. The trick1 is to leave “markers” in the proof state. We use a dedicate type CaseName, and a hypothesis name : CaseName indicates that this goal arose from the that case.

    Inductive CaseName := CaseNameI.

    With this, we can write StarApp: forall (starApp : CaseName), … to name this case.

  2. For a little bit of polish, we can introduce notation for that:

    Notation "'case' x , t" := (forall {x : CaseName}, t) (at level 200).

    This allows us to use the syntax you saw above.

  3. To easily discharge these CaseName assumptions when using the introduction forms, I wrote these tactics:

    Ltac clear_names := try exact CaseNameI.
    Ltac named_constructor  := constructor; [ exact CaseNameI | idtac .. ].
    Ltac named_econstructor := econstructor; [ exact CaseNameI | idtac .. ].
  4. Finally I wrote the tactic name_cases. What it does is relatively simple:

    For each subgoal: Take all hypotheses of type CaseName, concatenate their names, change the name of the current goal to that, and clear these hypotheses

    Unfortunately, my grasp of Coq tactic programming is rather rudimentary, and the only way I manged to solve this is a horrible monster of Ltac2, including hand-rolled imperative implementations of string concatenation and a little nested Ltac1 tactic within. You have been warned:

    From Ltac2 Require Import Ltac2.
    From Ltac2 Require Option.
    Set Default Proof Mode "Classic".
    Ltac name_cases := ltac2:(
      (* Horribly manual string manipulations. Does this mean I should
         go to the Ocaml level?
      *)
      let strcpy s1 s2 o :=
        let rec go := fun n =>
          match Int.lt n (String.length s2) with
          | true => String.set s1 (Int.add o n) (String.get s2 n); go (Int.add n 1)
          | false => ()
          end
        in go 0
      in
      let concat := fun s1 s2 =>
        let l := Int.add (Int.add (String.length s1) (String.length s2)) 1 in
        let s := String.make l (Char.of_int 95) in
        strcpy s s1 0;
        strcpy s s2 (Int.add (String.length s1) 1);
        s
      in
      Control.enter (let rec go () :=
        lazy_match! goal with
        | [ h1 : CaseName, h2 : CaseName |- _ ] =>
          (* Multiple case names? Combine them (and recurse) *)
          let h := concat (Ident.to_string h1) (Ident.to_string h2) in
          Std.clear [h1; h2];
          let h := Option.get (Ident.of_string h) in
          assert ($h := CaseNameI);
          go ()
        | [ _ : CaseName |- _ ] =>
          (* A single case name? Set current goal name accordingly. *)
          ltac1:(
            (* How to do this in ltac2? *)
            lazymatch goal with
            | [ H : CaseName |- _ ] => refine ?[H]; clear H
            end
          )
        | [ |- _ ] =>
          Control.backtrack_tactic_failure "Did not find any CaseName hypotheses"
        end
      in go)
    ).

    If someone feels like re-implementing this in a way that is more presentable, I’ll be happy to update this code (and learn something along the way

That’s all it takes!

Conclusion

With some mild hackery, we can get named cases in Coq, which I find indispensable in managing larger, evolving proofs. I wonder why this style is not more common, and available out of the box, but maybe it is just not known well enough? Maybe this blog post can help a bit here.


  1. I have vague recollections of seeing at least parts of this trick on some blog some years ago, and I do not claim originality here.

Distributing Haskell programs in a multi-platform zip file

Published 2020-11-09 in sections English, Haskell.

My maybe most impactful piece of code is tttool and the surrounding project, which allows you to create your own content for the Ravensburger Tiptoi™ platform. The program itself is a command line tool, and in this blog post I want to show how I go about building that program for Linux (both normal and static builds), Windows (cross-compiled from Linux), OSX (only on CI), all combined into and released as a single zip file.

Maybe some of it is useful or inspiring to my readers, or can even serve as a template. This being a blob post, though, note that it may become obsolete or outdated.

Ingredients

I am building on the these components:

Without the nix build system and package manger I probably woudn’t even attempt to pull of complex tasks that may, say, require a patched ghc. For many years I resisted learning about nix, but when I eventually had to, I didn’t want to go back.

This project provides an alternative Haskell build infrastructure for nix. While this is not crucial for tttool, it helps that they tend to have some cross-compilation-related patches more than the official nixpkgs. I also like that it more closely follows the cabal build work-flow, where cabal calculates a build plan based on your projects dependencies. It even has decent documentation (which is a new thing compared to two years ago).

Niv is a neat little tool to keep track of your dependencies. You can quickly update them with, say niv update nixpkgs. But what’s really great is to temporarily replace one of your dependencies with a local checkout, e.g. via NIV_OVERRIDE_haskellNix=$HOME/build/haskell/haskell.nix nix-instantiate -A osx-exe-bundle There is a Github action that will keep your niv-managed dependencies up-to-date.

This service (proprietary, but free to public stuff up to 10GB) gives your project its own nix cache. This means that build artifacts can be cached between CI builds or even build steps, and your contributors. A cache like this is a must if you want to use nix in more interesting ways where you may end up using, say, a changed GHC compiler. Comes with GitHub actions integration.

  • CI via Github actions

Until recently, I was using Travis, but Github actions are just a tad easier to set up and, maybe more important here, the job times are high enough that you can rebuild GHC if you have to, and even if your build gets canceled or times out, cleanup CI steps still happen, so that any new nix build products will still reach your nix cache.

The repository setup

All files discussed in the following are reflected at https://github.com/entropia/tip-toi-reveng/tree/7020cde7da103a5c33f1918f3bf59835cbc25b0c.

We are starting with a fairly normal Haskell project, with a single .cabal file (but multi-package projects should work just fine). To make things more interesting, I also have a cabal.project which configures one dependency to be fetched via git from a specific fork.

To start building the nix infrastructure, we can initialize niv and configure it to use the haskell.nix repo:

niv init
niv add input-output-hk/haskell.nix -n haskellNix

This creates nix/sources.json (which you can also edit by hand) and nix/sources.nix (which you can treat like a black box).

Now we can start writing the all-important default.nix file, which defines almost everything of interest here. I will just go through it line by line, and explain what I am doing here.

{ checkMaterialization ? false }:

This defines a flag that we can later set when using nix-build, by passing --arg checkMaterialization true, and which is off by default. I’ll get to that flag later.

let
  sources = import nix/sources.nix;
  haskellNix = import sources.haskellNix {};

This imports the sources as defined niv/sources.json, and loads the pinned revision of the haskell.nix repository.

  # windows crossbuilding with ghc-8.10 needs at least 20.09.
  # A peek at https://github.com/input-output-hk/haskell.nix/blob/master/ci.nix can help
  nixpkgsSrc = haskellNix.sources.nixpkgs-2009;
  nixpkgsArgs = haskellNix.nixpkgsArgs;

  pkgs = import nixpkgsSrc nixpkgsArgs;

Now we can define pkgs, which is “our” version of the nixpkgs package set, extended with the haskell.nix machinery. We rely on haskell.nix to pin of a suitable revision of the nixpkgs set (see how we are using their niv setup).

Here we could our own configuration, overlays, etc to nixpkgsArgs. In fact, we do in

  pkgs-osx = import nixpkgsSrc (nixpkgsArgs // { system = "x86_64-darwin"; });

to get the nixpkgs package set of an OSX machine.

  # a nicer filterSource
  sourceByRegex =
    src: regexes: builtins.filterSource (path: type:
      let relPath = pkgs.lib.removePrefix (toString src + "/") (toString path); in
      let match = builtins.match (pkgs.lib.strings.concatStringsSep "|" regexes); in
      ( type == "directory"  && match (relPath + "/") != null
      || match relPath != null)) src;

Next I define a little helper that I have been copying between projects, and which allows me to define the input to a nix derivation (i.e. a nix build job) with a set of regexes. I’ll use that soon.

  tttool-exe = pkgs: sha256:
    (pkgs.haskell-nix.cabalProject {

The cabalProject function takes a cabal project and turns it into a nix project, running cabal v2-configure under the hood to let cabal figure out a suitable build plan. Since we want to have multiple variants of the tttool, this is so far just a function of two arguments pkgs and sha256, which will be explained in a bit.

      src = sourceByRegex ./. [
          "cabal.project"
          "src/"
          "src/.*/"
          "src/.*.hs"
          ".*.cabal"
          "LICENSE"
        ];

The cabalProject function wants to know the source of the Haskell projects. There are different ways of specifying this; in this case I went for a simple whitelist approach. Note that cabal.project.freze (which exists in the directory) is not included.

      # Pinning the input to the constraint solver
      compiler-nix-name = "ghc8102";

The cabal solver doesn’t find out which version of ghc to use, that is still my choice. I am using GHC-8.10.2 here. It may require a bit of experimentation to see which version works for your project, especially when cross-compiling to odd targets.

      index-state = "2020-11-08T00:00:00Z";

I want the build to be deterministic, and not let cabal suddenly pick different package versions just because something got uploaded. Therefore I specify which snapshot of the Hackage package index it should consider.

      plan-sha256 = sha256;
      inherit checkMaterialization;

Here we use the second parameter, but I’ll defer the explanation for a bit.

      modules = [{
        # smaller files
        packages.tttool.dontStrip = false;
      }] ++

These “modules” are essentially configuration data that is merged in a structural way. Here we say that we want the tttool binary to be stripped (saves a few megabyte).

      pkgs.lib.optional pkgs.hostPlatform.isMusl {
        packages.tttool.configureFlags = [ "--ghc-option=-static" ];

Also, when we are building on the musl platform, that’s when we want to produce a static build, so let’s pass -static to GHC. This seems to be enough in terms of flags to produce static binaries. It helps that my project is using mostly pure Haskell libraries; if you link against C libraries you might have to jump through additional hoops to get static linking going. The haskell.nix documentation has a section on static building with some flags to cargo-cult.

        # terminfo is disabled on musl by haskell.nix, but still the flag
        # is set in the package plan, so override this
        packages.haskeline.flags.terminfo = false;
      };

This (again only used when the platform is musl) seems to be necessary to workaround what might be a big in haskell.nix.

    }).tttool.components.exes.tttool;

The cabalProject function returns a data structure with all Haskell packages of the project, and for each package the different components (libraries, tests, benchmarks and of course executables). We only care about the tttool executable, so let’s project that out.

  osx-bundler = pkgs: tttool:
   pkgs.stdenv.mkDerivation {
      name = "tttool-bundle";

      buildInputs = [ pkgs.macdylibbundler ];

      builder = pkgs.writeScript "tttool-osx-bundler.sh" ''
        source ${pkgs.stdenv}/setup

        mkdir -p $out/bin/osx
        cp ${tttool}/bin/tttool $out/bin/osx
        chmod u+w $out/bin/osx/tttool
        dylibbundler \
          -b \
          -x $out/bin/osx/tttool \
          -d $out/bin/osx \
          -p '@executable_path' \
          -i /usr/lib/system \
          -i ${pkgs.darwin.Libsystem}/lib
      '';
    };

This function, only to be used on OSX, takes a fully build tttool, finds all the system libraries it is linking against, and copies them next to the executable, using the nice macdylibbundler. This way we can get a self-contained executable.

A nix expert will notice that this probably should be written with pkgs.runCommandNoCC, but then dylibbundler fails because it lacks otool. This should work eventually, though.

in rec {
  linux-exe      = tttool-exe pkgs
     "0rnn4q0gx670nzb5zp7xpj7kmgqjmxcj2zjl9jqqz8czzlbgzmkh";
  windows-exe    = tttool-exe pkgs.pkgsCross.mingwW64
     "01js5rp6y29m7aif6bsb0qplkh2az0l15nkrrb6m3rz7jrrbcckh";
  static-exe     = tttool-exe pkgs.pkgsCross.musl64
     "0gbkyg8max4mhzzsm9yihsp8n73zw86m3pwvlw8170c75p3vbadv";
  osx-exe        = tttool-exe pkgs-osx
     "0rnn4q0gx670nzb5zp7xpj7kmgqjmxcj2zjl9jqqz8czzlbgzmkh";

Time to create the four versions of tttool. In each case we use the tttool-exe function from above, passing the package set (pkgs,…) and a SHA256 hash.

The package set is either the normal one, or it is one of those configured for cross compilation, building either for Windows or for Linux using musl, or it is the OSX package set that we instantiated earlier.

The SHA256 hash describes the result of the cabal plan calculation that happens as part of cabalProject. By noting down the expected result, nix can skip that calculation, or fetch it from the nix cache etc.

How do we know what number to put there, and when to change it? That’s when the --arg checkMaterialization true flag comes into play: When that is set, cabalProject will not blindly trust these hashes, but rather re-calculate them, and tell you when they need to be updated. We’ll make sure that CI checks them.

  osx-exe-bundle = osx-bundler pkgs-osx osx-exe;

For OSX, I then run the output through osx-bundler defined above, to make it independent of any library paths in /nix/store.

This is already good enough to build the tool for the various systems! The rest of the the file is related to packaging up the binaries, to tests, and various other things, but nothing too essentially. So if you got bored, you can more or less stop now.

  static-files = sourceByRegex ./. [
    "README.md"
    "Changelog.md"
    "oid-decoder.html"
    "example/.*"
    "Debug.yaml"
    "templates/"
    "templates/.*\.md"
    "templates/.*\.yaml"
    "Audio/"
    "Audio/digits/"
    "Audio/digits/.*\.ogg"
  ];

  contrib = ./contrib;

The final zip file that I want to serve to my users contains a bunch of files from throughout my repository; I collect them here.

  book = …;

The project comes with documentation in the form of a Sphinx project, which we build here. I’ll omit the details, because they are not relevant for this post (but of course you can peek if you are curious).

  os-switch = pkgs.writeScript "tttool-os-switch.sh" ''
    #!/usr/bin/env bash
    case "$OSTYPE" in
      linux*)   exec "$(dirname "''${BASH_SOURCE[0]}")/linux/tttool" "$@" ;;
      darwin*)  exec "$(dirname "''${BASH_SOURCE[0]}")/osx/tttool" "$@" ;;
      msys*)    exec "$(dirname "''${BASH_SOURCE[0]}")/tttool.exe" "$@" ;;
      cygwin*)  exec "$(dirname "''${BASH_SOURCE[0]}")/tttool.exe" "$@" ;;
      *)        echo "unsupported operating system $OSTYPE" ;;
    esac
  '';

The zipfile should provide a tttool command that works on all systems. To that end, I implement a simple platform switch using bash. I use pks.writeScript so that I can include that file directly in default.nix, but it would have been equally reasonable to just save it into nix/tttool-os-switch.sh and include it from there.

  release = pkgs.runCommandNoCC "tttool-release" {
    buildInputs = [ pkgs.perl ];
  } ''
    # check version
    version=$(${static-exe}/bin/tttool --help|perl -ne 'print $1 if /tttool-(.*) -- The swiss army knife/')
    doc_version=$(perl -ne "print \$1 if /VERSION: '(.*)'/" ${book}/book.html/_static/documentation_options.js)

    if [ "$version" != "$doc_version" ]
    then
      echo "Mismatch between tttool version \"$version\" and book version \"$doc_version\""
      exit 1
    fi

Now the derivation that builds the content of the release zip file. First I double check that the version number in the code and in the documentation matches. Note how ${static-exe} refers to a path with the built static Linux build, and ${book} the output of the book building process.

    mkdir -p $out/
    cp -vsr ${static-files}/* $out
    mkdir $out/linux
    cp -vs ${static-exe}/bin/tttool $out/linux
    cp -vs ${windows-exe}/bin/* $out/
    mkdir $out/osx
    cp -vsr ${osx-exe-bundle}/bin/osx/* $out/osx
    cp -vs ${os-switch} $out/tttool
    mkdir $out/contrib
    cp -vsr ${contrib}/* $out/contrib/
    cp -vsr ${book}/* $out
  '';

The rest of the release script just copies files from various build outputs that we have defined so far.

Note that this is using both static-exe (built on Linux) and osx-exe-bundle (built on Mac)! This means you can only build the release if you either have setup a remote osx builder (a pretty nifty feature of nix, which I unfortunately can’t use, since I don't have access to a Mac), or the build product must be available in a nix cache (which it is in my case, as I will explain later).

The output of this derivation is a directory with all the files I want to put in the release.

  release-zip = pkgs.runCommandNoCC "tttool-release.zip" {
    buildInputs = with pkgs; [ perl zip ];
  } ''
    version=$(bash ${release}/tttool --help|perl -ne 'print $1 if /tttool-(.*) -- The swiss army knife/')
    base="tttool-$version"
    echo "Zipping tttool version $version"
    mkdir -p $out/$base
    cd $out
    cp -r ${release}/* $base/
    chmod u+w -R $base
    zip -r $base.zip $base
    rm -rf $base
  '';

And now these files are zipped up. Note that this automatically determines the right directory name and basename for the zipfile.

This concludes the step necessary for a release.

  gme-downloads = …;
  tests = …;

These two definitions in default.nix are related to some simple testing, and again not relevant for this post.

  cabal-freeze = pkgs.stdenv.mkDerivation {
    name = "cabal-freeze";
    src = linux-exe.src;
    buildInputs = [ pkgs.cabal-install linux-exe.env ];
    buildPhase = ''
      mkdir .cabal
      touch .cabal/config
      rm cabal.project # so that cabal new-freeze does not try to use HPDF via git
      HOME=$PWD cabal new-freeze --offline --enable-tests || true
    '';
    installPhase = ''
      mkdir -p $out
      echo "-- Run nix-shell -A check-cabal-freeze to update this file" > $out/cabal.project.freeze
      cat cabal.project.freeze >> $out/cabal.project.freeze
    '';
  };

Above I mentioned that I still would like to be able to just run cabal, and ideally it should take the same library versions that the nix-based build does. But pinning the version of ghc in cabal.project is not sufficient, I also need to pin the precise versions of the dependencies. This is best done with a cabal.project.freeze file.

The above derivation runs cabal new-freeze in the environment set up by haskell.nix and grabs the resulting cabal.project.freeze. With this I can run nix-build -A cabal-freeze and fetch the file from result/cabal.project.freeze and add it to the repository.

  check-cabal-freeze = pkgs.runCommandNoCC "check-cabal-freeze" {
      nativeBuildInputs = [ pkgs.diffutils ];
      expected = cabal-freeze + /cabal.project.freeze;
      actual = ./cabal.project.freeze;
      cmd = "nix-shell -A check-cabal-freeze";
      shellHook = ''
        dest=${toString ./cabal.project.freeze}
        rm -f $dest
        cp -v $expected $dest
        chmod u-w $dest
        exit 0
      '';
    } ''
      diff -r -U 3 $actual $expected ||
        { echo "To update, please run"; echo "nix-shell -A check-cabal-freeze"; exit 1; }
      touch $out
    '';

But generated files in repositories are bad, so if that cannot be avoided, at least I want a CI job that checks if they are up to date. This job does that. What’s more, it is set up so that if I run nix-shell -A check-cabal-freeze it will update the file in the repository automatically, which is much more convenient than manually copying.

Lately, I have been using this pattern regularly when adding generated files to a repository: * Create one nix derivation that creates the files * Create a second derivation that compares the output of that derivation against the file in the repo * Create a derivation that, when run in nix-shell, updates that file. Sometimes that derivation is its own file (so that I can just run nix-shell nix/generate.nix), or it is merged into one of the other two.

This concludes the tour of default.nix.

The CI setup

The next interesting bit is the file .github/workflows/build.yml, which tells Github Actions what to do:

name: "Build and package"
on:
  pull_request:
  push:

Standard prelude: Run the jobs in this file upon all pushes to the repository, and also on all pull requests. Annoying downside: If you open a PR within your repository, everything gets built twice. Oh well.

jobs:
  build:
    strategy:
      fail-fast: false
      matrix:
        include:
        - target: linux-exe
          os: ubuntu-latest
        - target: windows-exe
          os: ubuntu-latest
        - target: static-exe
          os: ubuntu-latest
        - target: osx-exe-bundle
          os: macos-latest
    runs-on: ${{ matrix.os }}

The “build” job is a matrix job, i.e. there are four variants, one for each of the different tttool builds, together with an indication of what kind of machine to run this on.

    - uses: actions/checkout@v2
    - uses: cachix/install-nix-action@v12

We begin by checking out the code and installing nix via the install-nix-action.

    - name: "Cachix: tttool"
      uses: cachix/cachix-action@v7
      with:
        name: tttool
        signingKey: '${{ secrets.CACHIX_SIGNING_KEY }}'

Then we configure our Cachix cache. This means that this job will use build products from the cache if possible, and it will also push new builds to the cache. This requires a secret key, which you get when setting up your Cachix cache. See the nix and Cachix tutorial for good instructions.

    - run: nix-build --arg checkMaterialization true -A ${{ matrix.target }}

Now we can actually run the build. We set checkMaterialization to true so that CI will tell us if we need to update these hashes.

    # work around https://github.com/actions/upload-artifact/issues/92
    - run: cp -RvL result upload
    - uses: actions/upload-artifact@v2
      with:
        name: tttool (${{ matrix.target }})
        path: upload/

For convenient access to build products, e.g. from pull requests, we store them as Github artifacts. They can then be downloaded from Github’s CI status page.

  test:
    runs-on: ubuntu-latest
    needs: build
    steps:
    - uses: actions/checkout@v2
    - uses: cachix/install-nix-action@v12
    - name: "Cachix: tttool"
      uses: cachix/cachix-action@v7
      with:
        name: tttool
        signingKey: '${{ secrets.CACHIX_SIGNING_KEY }}'
    - run: nix-build -A tests

The next job repeats the setup, but now runs the tests. Because of needs: build it will not start before the builds job has completed. This also means that it should get the actual tttool executable to test from our nix cache.

  check-cabal-freeze:
    runs-on: ubuntu-latest
    steps:
    - uses: actions/checkout@v2
    - uses: cachix/install-nix-action@v12
    - name: "Cachix: tttool"
      uses: cachix/cachix-action@v7
      with:
        name: tttool
        signingKey: '${{ secrets.CACHIX_SIGNING_KEY }}'
    - run: nix-build -A check-cabal-freeze

The same, but now running the check-cabal-freeze test mentioned above. Quite annoying to repeat the setup instructions for each job…

  package:
    runs-on: ubuntu-latest
    needs: build
    steps:
    - uses: actions/checkout@v2
    - uses: cachix/install-nix-action@v12
    - name: "Cachix: tttool"
      uses: cachix/cachix-action@v7
      with:
        name: tttool
        signingKey: '${{ secrets.CACHIX_SIGNING_KEY }}'

    - run: nix-build -A release-zip

    - run: unzip -d upload ./result/*.zip
    - uses: actions/upload-artifact@v2
      with:
        name: Release zip file
        path: upload

Finally, with the same setup, but slightly different artifact upload, we build the release zip file. Again, we wait for build to finish so that the built programs are in the nix cache. This is especially important since this runs on linux, so it cannot build the OSX binary and has to rely on the cache.

Note that we don’t need to checkMaterialization again.

Annoyingly, the upload-artifact action insists on zipping the files you hand to it. A zip file that contains just a zipfile is kinda annoying, so I unpack the zipfile here before uploading the contents.

Conclusion

With this setup, when I do a release of tttool, I just bump the version numbers, wait for CI to finish building, run nix-build -A release-zip and upload result/tttool-n.m.zip. A single file that works on all target platforms. I have not yet automated making the actual release, but with one release per year this is fine.

Also, when trying out a new feature, I can easily create a branch or PR for that and grab the build products from Github’s CI, or ask people to try them out (e.g. to see if they fixed their bugs). Note, though, that you have to sign into Github before being able to download these artifacts.

One might think that this is a fairly hairy setup – finding the right combinations of various repertories so that cross-compilation works as intended. But thanks to nix’s value propositions, this does work! The setup presented here was a remake of a setup I did two years ago, with a much less mature haskell.nix. Back then, I committed a fair number of generated files to git, and juggled more complex files … but once it worked, it kept working for two years. I was indeed insulated from upstream changes. I expect that this setup will also continue to work reliably, until I choose to upgrade it again. Hopefully, then things are even more simple, and require less work-around or manual intervention.

Learn Haskell on CodeWorld writing Sokoban

Published 2020-09-27 in sections English, Haskell.

Two years ago, I held the CIS194 minicourse on Haskell at the University of Pennsylvania. In that installment of the course, I changed the first four weeks to teach the basics of Haskell using the online Haskell environment CodeWorld, and lead the students towards implementing the game Sokoban.

As it is customary for CIS194, I put my lecture notes and exercises online, and this has been used as a learning resources by people from all over the world. But since I have left the University of Pennsylvania, I lost the ability to update the text, and as the CodeWorld API has evolved, some of the examples and exercises no longer work.

Some recent complains about that, in bug reports against CodeWorld and in unrealistically flattering tweets (“Shame, this was the best Haskell course ever!!!”) motivated me to extract that material and turn it into an updated stand-alone tutorial that I can host myself.

So if you feel like learning Haskell without worrying about local installation, and while creating a reasonably fun game, head over to https://haskell-via-sokoban.nomeata.de/ and get started! Improvements can now also be contributed at https://github.com/nomeata/haskell-via-sokoban.

Credits go to Brent Yorgey, Richard Eisenberg and Noam Zilberstein, who held the previous installments of the course, and Chris Smith for creating the CodeWorld environment.

Tiptoi in Dresden

Published 2020-07-26 in sections Deutsch, Tiptoi.

Das tiptoi-Bastel-Projekt zieht immer weitere Kreise. Mit freudiger Überraschung erfuhr ich dass Markus Wacker, Professor an der HTW Dresden, gleich mehrere Projekte mit meinem tttool betreibt:

Vorlesung

Studenten in seiner Vorlesung lernen tatsächlich Programmieren mit der „Programmiersprache“, die ich für das tttool mehr oder weniger ad-hoc erfunden habe.

Der Wichtel aus dem c't-Artikel hat es nun auch auf Vorlesungsfolien geschafft

Der Wichtel aus dem c't-Artikel hat es nun auch auf Vorlesungsfolien geschafft

Bemerkenswert finde ich hier dass das schon seit einer Weile so geht, und wir auf der Tiptoi-Mailingliste davon nichts mitbekommen haben. Das heißt ja auch, dass die Software soweit ganz zuverlässig ihren Dienst tut.

Vielleicht bekomme ich ja mehr von jenen nun Tiptoi-Indoktrinierten Studenten mit, sobald sie dann selber Kinder im entsprechenden Alter haben…

Diplomarbeit

Seine Studentin Evelyn Zinnatova erstellte für die Staatliche Kunstsammlung Dresden eine haptisch und akustisch erlebbare Version eines Kupferstichs, in der so ziemliche alle Techniken zum Einsatz kamen, die einen Nerd erfreuen: 3D-Druck, Lasercutting und eben der Tiptoi-Stift. Kapitel 7 der äußerst umfangreichen Diplomarbeit „Piranesi zum Anfassen - Eine Druckgrafik wird erlebbar“ geht detailliert auf den Tiptoi-Stift, das GME-Dateiformat und das tttool ein. Die Arbeit hat sogar einen Preis eingeheimst, den „Dresden Excellence Award für hervorragende wissenschaftliche Arbeiten“.

Evelyn Zinnatova, der Tiptoi-Sift, und die 3D-Version des Kupferstichs auf dem Cover des Hochschulmagazin WISSEND

Evelyn Zinnatova, der Tiptoi-Sift, und die 3D-Version des Kupferstichs auf dem Cover des Hochschulmagazin WISSEND

Hier ist hervorzuheben dass diese Arbeit mit ausdrücklichem Einverständnis von Ravensburger erstellt worden ist, obwohl unsere „inoffizielle“ Software verwendet wurde. Ich hoffe das inspiriert weitere Künstler und Bastler zu öffentlichen, von Ravensburger abgesegneten Tiptoi-Projekten.

Und mehr…

Darüber hinaus plant Prof. Wacker auch Schülerpraktika mit dem Tiptoi-Stift, und noch weitere coole Projekte sind wohl in der Pipeline – ich bin gespannt!

Das Tiptoi-Projekt

Published 2020-07-16 in sections Deutsch, Tiptoi.

Der folgende Text ist kürzlich in Ausgabe 102 der Datenschleuder, dem Fachmagazin des Chaos Computer Clubs, erschienen. Wer ihn lieber auf Papier und mit weniger Tippfehlern lesen will, Interesse an den anderen Themen des Magazins hat oder einfach den CCC unterstützen will sollte erwägen, die Ausgabe zu bestellen, das Heft zu abonnieren oder gleich Mitglied im CCC zu werden. Vielen Dank an der Stelle an den Datenschleuder-Redakteur Philipp Matthias Schäfer für diese Gelegenheit und die Betreuung.


Mit dem tiptoi-Stift bespaßt Ravensburger seit einem Jahrzehnt erfolgreich Kinder im Alter von vier bis zehn, ganz wie geplant. Dass sie damit aber auch erfolgreich ausgewachsene Hacker bespaßen würden, die lieber eigene tiptoi-Werke kreieren, war vermutlich nicht vorgesehen. Doch wie kam es eigentlich dazu?

Der tiptoi-Stift ist ein grell-orangenes, leicht klobiges Gerät, mit dem man die vielen speziell dafür veröffentlichten Bücher, Spiele, Figuren etc. erkundet. Tippt man zum Beispiel die Kuh im Stall an, so hört man ein Muhen oder erfährt etwas Wissenswertes über die Kuh. Auch komplexere Interaktionen, bis hin zu kompletten Brettspielmechaniken, sind dabei möglich. Schnell stellt sich die Frage: Wie funktioniert das? Und dannn natürlich auch: kann ich das selber machen?

Der Tiptoi-Stift in Aktion -- hier schon mit der Monkey-Island-Adaption von Carsten Podszun.

Der Tiptoi-Stift in Aktion -- hier schon mit der Monkey-Island-Adaption von Carsten Podszun.

Getrieben von dieser Frage haben sich ein paar technisch Interessierte gefunden um die Funktionsweise des Stiftes zu reverse-engineeren und so die Werkzeuge zu schaffen, mit der jeder die Produkte von Ravensburger neu vertonen oder komplett neue Werke für den tiptoi erstellen kann. Wie man das selber macht ist in Handbüchern, Zeitschriftenartikeln und Videos beschrieben (siehe https://tttool.nomeata.de/). In diesem Artikel hier erzähle ich -- aus meiner persönlichen Perspektive -- wie dieses Projekt zu Stande kam, welche Hürden es zu nehmen gab und wo wir heute stehen.

Was davor geschah

Im Frühling 2013, mein Neffe ist gerade voll im tiptoi-Fieber, gehe ich auf erste Recherchen. Einiges über die Funktionsweise des Stiftes kann man sich selber erschließen: Die Bücher selbst enthalten keine Elektronik (auch keine RFID-Chips, wie manche erstmal vermuten), sondern sind mit einem feinen schwarzen Punktmuster überzogen, was man mit Lupe oder guten Augen erkennen kann, und das der Stift mit einer Kamera in der Spitze einliest. Zu jedem Produkt, das man kauft, lädt man eine .gme-Datei, etwa 10-100MB groß, auf den Stift, der sich als USB-Massenmedium ausgibt. Dies legt nahe, dass diese GME-Datei die Audiodateien und Spiellogik enthält. Bei jedem Produkt muss man erst ein dediziertes Anschaltfeld antippen; vermutlich lässt das den Stift wissen, welche Datei er laden muss.

Ich war natürlich nicht der erste, der sich so mit dem tiptoi-Stift beschäftigt hat, und fand weitere Informationen auf dem Blog „Geeky Thinking“ und im Mikrocontroller-Forum. Die erste Frage, die sich stellt, ist: kann man die Audio-Snippets in den GME-Dateien finden, um sie zu extrahieren oder gar zu ersetzen?

So hat Martin Oberhuber einfach mal dreist Ravensburger gefragt und erfahren:

Wir verwenden für die GME-Dateien ein proprietäres Format. Mir ist nicht bekannt, dass es möglich ist die eigentlichen Audiodaten (OGG Vorbis Komprimierung) daraus zu extrahieren

Auch wenn Ravensburger sicherlich nicht vorhatte, der Entschlüsselung des Formates Vorschub zu leisten, war das tatsächlich sehr hilfreich: Wie auch andere Binärformate beginnen OGG-Dateien immer mit den gleichen vier Bytes, den sogenannten magic bytes, hier OggS. Diese Bytefolge müssten ja demnach oft in der GME-Datei zu finden sein… war sie aber nicht. Zumindest nicht direkt, denn die ganze Datei ist „verschlüsselt“. Verschlüsselt nur in Anführungszeichen, denn es schien als ob jedes Byte der Audio-Dateien mit einem festen Wert ge-XOR-t wird (z.B. mit 0xAD - der Wert unterscheidet sich von GME-Datei zu GME-Datei). Diesen „Schlüssel“ kann man einfach durch Ausprobieren aller 256 möglichen Werte herausfinden: Der, der die meisten OggS-Strings in der Datei produziert ist wohl der richtige.

Nun wusste man, wo die Audio-Dateien liegen. Und man fand auch eine einfach gestrickte Tabelle in der Datei, in der alle Audio-Dateien mit Offset und Länge aufgeführt werden, so dass man sie gut einzeln extrahieren kann. Doch die Dateien waren irgendwie korrupt. Viktor fand noch heraus, dass wohl Nullbytes (0x00) nicht ge-XOR-t werden, und ich folgerte daraus, dass auch das Magic-Bytes selbst in Ruhe gelassen wird. Aber auch damit funktionierten die Audio-Dateien nicht, und für den Rest des Jahres passierte nichts mehr.

Ich hatte für meine Experimente ein bisschen Haskell-Code geschrieben, den ich auf dem Github-Bereich des Karlsruher entropia.de veröffentlichte.

Der Hahn macht Kuckuck

Das Projekt ruhte – bis kurz nach Weihnachten 2013. Jedes Jahr ist das eine spannende Zeit: Ein neuer Schwung tiptoi-Stifte schwappt in die Kinderzimmer, und die zugehörigen technikinteressierten Eltern haben ein paar Tage Zeit. Diese stießen nun auf mein GitHub-Projekt, fragten ob ich inzwischen weiter gekommen sei und schauten sich selber nochmal die Dateien an. Und endlich fand Matthias Weber den fehlenden Puzzlestein: Auch das Byte 0xFF sowie das Komplement des Schlüssels werden von der „Verschlüsselung“ in Ruhe gelassen! Damit ließen sich erstmal erfolgreich die Audio-Samples aus den GME-Dateien extrahieren und abspielen.

Die nächsten Tage waren spannend: Fünf Bastler, die sich nicht kannten, tauschten per E-Mail immer weitere Funde aus: Wir entdecken eine Art Tabelle, in der -- gemischt mit noch nicht verstandenen Steuerbefehlen -- die Audiodateien referenziert werden. Da wir nun die Audio-Dateien anhören konnten, konnten wir abschätzen, zu welcher Stelle im tiptoi-Buch die entsprechende Befehle gehören, und es entstanden erste Theorien, was die Steuerbefehle (Audio abspielen, Arithmetik, Sprünge) bedeuten und wie sie aufgebaut sind -- insbesondere Ulrich Sibiller ist hier viel zu verdanken. Ich selbst hatte zu der Zeit keine tiptoi-Hardware zur Hand und arbeitete bloß mit dem Hexeditor und den Beobachtungen der anderen. Die neusten Theorien baute ich stets in den Haskell-Code ein. Bisweilen nahmen diese Theorien absurde Züge an, die mit allerlei Sonderfällen und -regeln versuchten, sich den Beobachtungen anzupassen. Analogien zu den Epizykel der Astonomie vor der heliozentrischen Wende dürfen gezogen werden.

Aber bald gab es Erfolge zu vermelden. Am 5.1.2014 meldete Björn Grothkast, dass er erfolgreich eine Audio-Datei austauschen konnte, so dass der Hahn nun Kuckuck krähte. Eine Woche später war das Befehlsformat fast vollständig verstanden. Am 24.1. konnten wir erstmals eine funktionierende GME-Datei erzeugen und Anfang Februar habe ich meinem Neffen den tiptoi-Weltatlas mit Familiengeschichten neu vertont!

Muster gültig?

Die tiptoi-Produkte umzuprogrammieren macht schon Spaß, aber das nächste Ziel war natürlich, auch eigene Produkte zu gestalten. An sich klingt das einfach: Man gestaltet sein Buch, legt das OID-Muster aus feinen schwarzen Punkten darüber, druckt es aus, und erstellt eine dazu gehörigen GME-Datei.

Die Muster selbst sind nicht sehr kompliziert: alle Millimeter wiederholt sich ein Quadrat bestehend aus 4×4 Punkten. Sieben dieser 16 Punkte benutzt der Stift um sich zu orientieren, die anderen 9 sind jeweils in eine der vier Diagonalen verschoben, was somit – abzüglich 2 Bit für eine Checksumme – eine 16-Bit-Zahl kodiert. Bereits im Januar steuerte Tobias Bäumer ein (in JavaScript geschriebenes) Werkzeug bei, das diese Muster dekodiert und auch entsprechende Bilddateien erzeugen kann.

Ein OID-Muster. Die obere Zeile und linke Spalte dienen zur Orientierung, der Rest kodiert eine 16-Bit-Zahl

Ein OID-Muster. Die obere Zeile und linke Spalte dienen zur Orientierung, der Rest kodiert eine 16-Bit-Zahl

Diese werden sogar vom Stift erkannt, wenn man sie auf einem guten Laserdrucker ausdruckt! Allerdings liest der Stift eine andere Zahl aus als das Muster selbst kodiert. Der Stift unterstützt dankenswerterweise eine Art Debug-Modus, in dem er stets den eingelesenen Code -- auf Chinesisch -- vorliest. In mühsamer Kleinarbeit begannen nun @Ol-li, Patrick Spendrin und andere die OID-Muster unter der Lupe zu dekodieren, sich vom Stift die tatsächlich gelesene Zahl vorlesen zu lassen, und das in einer Tabelle zu sammeln. Leider ohne eine Regelmäßigkeit dahinter zu erkennen.

Massenmedien

Davon ließ Carsten Podszun sich nicht abschrecken und veröffentlichte im September 2014 ein Video-Tutorial auf YouTube, in dem er beschrieb, wie er eine Seite eines eigenen tiptoi-Buches komplett selber gestaltet hatte: von der Bildbearbeitung (Sättigung raus!), der Mustergenerierung (10×10 Pixel pro Muster), dem Druck (Farben und Muster gentrennt drucken) und der Programmierung mittels meines tttool.

So kam wieder neuer Schwung ins Projekt. Das tttool lernte die Muster als PNG- oder SVG-Datei auszugeben und dabei – zumindest für die uns bekannten Codes – zwischen den vom tiptoi-Stift und den im Muster kodierten Zahlen umzurechnen.

Inspiriert durch eine Anfrage vom Fablab Karlsruhe, ob Carsten und ich nicht dort einen Workshop anbieten wollten, spielten wir mit der Idee, einen Artikel über das tiptoi-Basteln zu schreiben. Wir erwägten damals tatsächlich die Datenschleuder, zielten dann aber doch nicht ganz so hoch und schrieben einen Text für die c't.

Weitere Publicity bekam das Projekt auf der Gulaschprogrammiernacht 2015 in Karlsruhe, auf der ich einen Vortrag gehalten und ein Workshop angeboten habe. Der Vortrag – eigentlich für die etwa 40 Technikaffinen im Publikum gedacht – wurde wie beim CCC üblich auch online gestellt, und inzwischen allein auf YouTube über 250.000 mal angeschaut. Wenn sich auch nur 1% davon inspirieren ließ, etwas mit dem tttool zu basteln, sind das 2500 Kinder, denen meine Bastelei Freude bereitet hat. Das ist ein sehr schöner und motivierender Gedanke.

Reifeprozess

Sehr hilfreich war auch dass Patrick Frey den “OidProducer” fand, ein chinesische Programm das OID-Muster für verschiedene Systeme erstellt. Darin fand er vollständige Tabelle, die der im Muster kodierte Zahl den vom Stift erkanntem Wert zuordnet. So müssen sich die Bastler mit dieser Komplikation nun nicht mehr herumschlagen.

Auch sonst wurde das Basteln mit dem tttool immer komfortabler: Um die Entwicklung zu beschleunigen kann das tttool die benötigten Audiodateien auch erstmal selbst per Text-to-Speech zu erzeugen, und einen übersichtlichen Bogen mit allen Felden eines Projekts erstellen. Mit ttaudio von Andreas Grimme und ttmp32gme von @thawn entstanden grafische Anwendungen, die auf das tttool aufbauen. Wir richteten eine Mailingliste ein, auf der sich über Tricks, Probleme und Projekte ausgetauscht wird. Eine stetig wachsende Galerie mit Erfolgsgeschichten schmückt die tttool-Webseite, und ein unfassendes Handbuch entstand.

Haskell?

Die Wahl von Haskell als Programmiersprache war eher dem Zufall geschuldet – es war einfach das geschickteste für meine ersten Experimente. Anfangs war ich selbst noch positiv überrascht, wie gut man mit Haskell auch binäre Daten verarbeiten kann und wie schnell ich neue Erkenntnisse meiner Mitstreiter umsetzen konnte. Inzwischen bin ich positiv überrascht, wie zuverlässig das Programm jetzt schon mehrere Jahre arbeitet, und es werden fast keine Bugs gemeldet, die an Programmierfehlern liegen. Auch die Plattformunabhängigkeit ist hervorragend: Selbst nur auf Linux unterwegs, konnte ich trotzdem auch Windows-Benutzer versorgen (anfangs per WINE, inzwischen per Cross-Compilation unter Nix). Inzwischen bestehen die tttool-Releases aus einer einzelnen ZIP-Datei, die unter Windows, OSX und (statisch gelinkt) allen Linuxen funktioniert – und das mit eingebautem Support für die Erzeugung von PNG, SVG und PDF.

Andererseits bedeutete die Wahl von Haskell sicherlich auch, dass ich weniger Code-Contributions bekommen habe und manches selber machen musste (oder durfte). Insgesamt habe ich es nie bereut, hier Haskell benutzt zu haben.

Darf man das denn?

Die wahrscheinlich häufigste Frage zu dem Projekt ist sicherlich: Darf ich das? Ist das legal? Bekomme ich Ärger von Ravensburger? Gibt es da Patente? Teilweise berichteten mir Leute nur in privaten Mails von ihren Projekten, statt sie auf der Mailingliste mit allen zu teilen.

Natürlich bin ich kein Anwalt und habe mich auch nur auf mein Bauchgefühl verlassen, aber meine Devise dabei war immer: wenn man niemanden stört, bekommt man auch kein Ärger. Welche Motivation sollte Ravensburger denn haben, Hobbyisten zu belangen? Das macht doch schon aus Publicity-Gründen keinen Sinn.

Tatsächlich wurden Mitarbeiter von Ravensburger auf das Projekt aufmerksam, und luden mich Anfang 2015 auf die Nürnberger Spielemesse ein. Für einen Brettspieler wie mich ist es natürlich ein schönes Schmankerl, diese für die Öffentlichkeit nicht zugängliche Fachmesse zu besuchen. Dort traf ich mich mit zwei Redakteuren (nicht Anwälten!), die sich sehr dafür interessierten, was wir da da so machen. Sie wollten wohl prüfen, ob Ravensburgers Interessen irgendwie berührt werden. Dies scheint nicht der Fall zu sein, und ich verlies das Treffen mit dem guten Gefühl, dass wir wohl ruhig so weiter machen können, solange nichts ruf- oder geschäftsschädigendes damit angestellt wird. Tatkräftige Hilfe, etwa mehr technische Information, ist von Ravensburger allerdings auch nicht zu erwarten.

Carston Podszun hatte mit seinen Basteleien ebenfalls die Aufmerksamkeit von Ravensburger geweckt und berichtet auch von stets wohlwollendem Interesse. Ich hoffe diese Erfahrungen nehmen einigen Bastlern ihre Sorge.

Um auch die letzten Sorgen zu nehmen wäre eine Einschätzung von jemand mit entsprechender Ahnung und Ausbildung sehr interessent. Kommentare bitte als Leserbrief an die Datenschleuder-Redaktion!

Ausblick

Die letzten Jahre ist es etwas ruhiger um das Projekt geworden. Das Dateiformat ist soweit entschlüsselt, dass auch komplexe Projekte umgesetzt werden können, etwa ein Taschenrechner, Geburtags-Schnitzeljagden oder ein Monkey-Island-Spiel zum Ausschneiden und Antipppen, und die Software wird immer wieder mal leicht verbessert.

Doch es gibt noch offene Baustellen: Manche GME-Dateien von Ravensburger enthalten ARM-Binärcode, der auf dem Stift direkt ausgeführt wird. Wenn wir verstehen würden, wie man solchen korrekt erzeugt und die Hardware anspricht, könnte man deutlich aufwendigere Logiken umsetzen. Oder vielleicht kann man auch die komplette Firmware des Stiftes durch eine eigene ersetzen – erste Erfolge, den tiptoi-Stift zu Flashen und eigenen ARM-Code auszuführen, sind vielversprechend und werden von Matthias Weber im snowbirdopter-Projekt vorangetrieben. Wem es nach diesem Text unter den Nägeln juckt, mal wieder ein bischen Reverse-Engineering zu betreiben, darf uns hier gerne unter die Arme greifen.

Selber basteln!

Lust auf eigene Basteleien? Auf https://tttool.entropia.de/ findest du die Galerie mit existierenden Projekten, das tttool zum Herunterladen, das „tttool-Handbuch“ sowie Links zu Videos und Magazinartikeln. Auf der tiptoi-Mailingliste helfen wir gerne weiter und freuen uns über Erfolgsberichte.

Template Haskell recompilation

Published 2020-07-01 in sections English, Haskell.

I was wondering: What happens if I have a Haskell module with Template Haskell that embeds some information from the environment (time, environment variables). Will such a module be reliable recompiled? And what if it gets recompiled, but the source code produced by Template Haskell is actually unchanged (e.g., because the environment variable has not changed), will all depending modules be recompiled (which would be bad)?

Here is a quick experiment, using GHC-8.8:

/tmp/th-recom-test $ cat Foo.hs
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -fforce-recomp #-}
module Foo where

import Language.Haskell.TH
import Language.Haskell.TH.Syntax
import System.Process

theMinute :: String
theMinute = $(runIO (readProcess "date" ["+%M"] "") >>= stringE)
[jojo@kirk:2] Mi, der 01.07.2020 um 17:18 Uhr ☺
/tmp/th-recom-test $ cat Main.hs
import Foo
main = putStrLn theMinute

Note that I had to set {-# OPTIONS_GHC -fforce-recomp #-} – by default, GHC will not recompile a module, even if it uses Template Haskell and runIO. If you are reading from a file you can use addDependentFile to tell the compiler about that depenency, but that does not help with reading from the environment.

So here is the test, and we get the desired behaviour: The Foo module is recompiled every time, but unless the minute has changed (see my prompt), Main is not recomipled:

/tmp/th-recom-test $ ghc --make -O2 Main.hs -o test
[1 of 2] Compiling Foo              ( Foo.hs, Foo.o )
[2 of 2] Compiling Main             ( Main.hs, Main.o )
Linking test ...
[jojo@kirk:2] Mi, der 01.07.2020 um 17:20 Uhr ☺
/tmp/th-recom-test $ ghc --make -O2 Main.hs -o test
[1 of 2] Compiling Foo              ( Foo.hs, Foo.o )
Linking test ...
[jojo@kirk:2] Mi, der 01.07.2020 um 17:20 Uhr ☺
/tmp/th-recom-test $ ghc --make -O2 Main.hs -o test
[1 of 2] Compiling Foo              ( Foo.hs, Foo.o )
[2 of 2] Compiling Main             ( Main.hs, Main.o ) [Foo changed]
Linking test ...

So all well!

Update: It seems that while this works with ghc --make, the -fforce-recomp does not cause cabal build to rebuild the module. That’s unfortunate.

Managed by an eleven year old

Published 2020-06-07 in sections English, Digital World.

This weekend I had some pretty good uncle time. My eleven year old nephew (after beating me in a fair match of tennis) wanted to play with his Lego Mindstorms set. He never even touches it unless I am around to help him, but then he quiet enjoys. As expected, when I ask him what we should try to build, he tends to come up with completely unrealistic or impossible ideas, and we have to somehow reduce the scope to something doable.

This time round, inspired by their autonomous vacuum cleaner, he wanted to build something like that. That was convenient, because now I could sell him what I wanted to try to do, namely make the robot follow a wall at more or less constant distance, as a useful first step.

We mounted the infra red distance sensor at an 45° angle to the front-left, and then I built a very simple control loop – measure the distance, subtract 40, apply a factor, and feed that into the “steering” input of the drive action, and repeat. I must admit that I was pretty proud to see just how well that very simple circuit worked: The little robot turned sharp corners in both directions, and otherwise drove nicely parallel and with constant distance to the wall.

I was satisfied with that achievement and would have happily ended it here before we might be disappointed by more ambitious and then failing goals.

But my nephew had not forgotten about the vacuum cleaner, and casually asked if I could make the robot draw an outline of its path, and thus of the room, on the display. Ok, where do I begin to explain just how unfeasible that is … yes, it seemed one can draw to the display. But how should the robot know where it is? How far it turns? How far it went? This is programming by connecting boxes, and I would not expect such an interface to allow for complex logic (right?). And I would need trigonometry and stuff.

But he didn’t quite believe it, and thus got me thinking … indeed, the arithmetic block can evaluate more complex formulas, involving sin  and cos  … so maybe if I can somehow keep track of where the robot is heading … well, let’s give it a try.

So by dragging boxes and connecting wires, I implemented a simple logic (three variables, x and y for current position, alpha for current heading; in each loop add the “steering” input onto alpha, and add (sin(alpha),cos(alpha)) onto the current position; throw in some linear factors to calibrate; draw pixel at (x, y)). And, to my nephew’s joy and my astonishment, the robot was drawing a curvy line that clearly correlates with the taken path!

It wasn’t respecting the angles perfectly, a square might not properly close, but half an hour earlier I would have actively bet against that we would pull this off!

After a few turns

After a few turns

I was, I must admit, a bit proud. But not only about the technical nerding, but also about my uncleing: That night, according to his parents, my nephew said that he can’t remember ever being so happy!

A Telegram bot in Haskell on Amazon Lambda

Published 2020-04-06 in sections English, Haskell.

I just had a weekend full of very successful serious geekery. On a whim I thought: “Wouldn't it be nice if people could interact with my game Kaleidogen also via a telegram bot?” This led me to learn about how I write a Telegram bot in Haskell and how I can deploy such a Haskell program to Amazon Lambda. In particular the latter bit might be interesting to some of my readers, so here is how went about it.

Kaleidogen

Kaleidogen is a little contemplative game (or toy game where, starting from just unicolored disks, you combine abstract circular patterns to breed more interesting patterns. See my FARM 2019 talk for more details, or check out the source repository. BTW, I am looking for help turning it into an Android app!

KaleidogenBot in action

KaleidogenBot in action

Amazon Lambda

Amazon Lambda is the “Function as a service” offering of Amazon Web Services. The idea is that you don’t rent a server, where you have to deal with managing the whole system and that you are paying for constantly, but you just upload the code that responds to outside requests, and AWS takes care of the rest: Starting and stopping instances, providing a secure base system etc. When nobody is using the service, no cost occurs.

This sounds ideal for hosting a toy Telegram bot: Most of the time nobody will be using it, and I really don't want to have to baby sit yet another service on my server. On Amazon Lambda, I can probably just forget about it.

But Haskell is not one of the officially supported languages on Amazon Lambda. So to run Haskell on Lambda, one has to solve two problems:

  • how to invoke the Haskell code on the server, and
  • how to build Haskell so that it runs on the Amazon Linux distribution

A Haskell runtime for Lambda

For the first we need a custom runtime. While this sounds complicated, it is actually a pretty simple concept: A runtime is an executable called bootstrap that queries the Lambda Runtime Interface for the next request to handle. The Lambda documentation is phrased as if this runtime has to be a dispatcher that calls the separate function’s handler. But it could just do all the things directly.

I found the Haskell package aws-lambda-haskell-runtime which provides precisely that: A function

runLambda :: (LambdaOptions -> IO (Either String LambdaResult)) -> IO ()

that talks to the Lambda Runtime API and invokes its argument on each message. The package also provides Template Haskell magic to collect “handlers“ of any JSON-able type and generates a dispatcher, like you might expect from other, more dynamic languages. But that was too much magic for me, so I ignored that and just wrote the handler manually:

main :: IO ()
main = runLambda run
  where
   run ::  LambdaOptions -> IO (Either String LambdaResult)
   run opts = do
    result <- handler (decodeObj (eventObject opts)) (decodeObj (contextObject opts))
    either (pure . Left . encodeObj) (pure . Right . LambdaResult . encodeObj) result

data Event = Event
  { path :: T.Text
  , body :: Maybe T.Text
  } deriving (Generic, FromJSON)

data Response = Response
  { statusCode :: Int
  , headers :: Value
  , body :: T.Text
  , isBase64Encoded :: Bool
  } deriving (Generic, ToJSON)

handler :: Event -> Context -> IO (Either String Response)
handler Event{body, path} context =

I expose my Lambda function to the world via Amazon’s API Gateway, configured to just proxy the HTTP requests. This means that my code receives a JSON data structure describing the HTTP request (here called Event, listing only the fields I care about), and it will respond with a Response, again as JSON.

The handler can then simply pattern-match on the path to decide what to do. For example this code handles URLs like /img/CAFFEEFACE.png, and responds with an image.

handler :: TC -> Event -> Context -> IO (Either String Response)
handler Event{body, path} context
    | Just bytes <- isImgPath path >>= T.decodeHex = do
        let pngData = genPurePNG bytes
        pure $ Right Response
            { statusCode = 200
            , headers = object [ "Content-Type" .= ("image/png" :: String) ]
            , isBase64Encoded = True
            , body = T.decodeUtf8 $ LBS.toStrict $ Base64.encode pngData
            }
    …

isImgPath :: T.Text -> Maybe T.Text
isImgPath  = T.stripPrefix "/img/" >=> T.stripSuffix ".png"

If this program would grow more, then one should probably use something more structured for routing here; maybe servant, or bridging towards wai apps (amost like wai-lamda, but that still assumes an existing runtime, instead of simply being the runtime). But for my purposes, no extra layers of indirection or abstraction are needed!

Deploying Haskell to Lambda

Building Haskell locally and deploying to different machiens is notoriously tricky; you often end up depending on a shared library that is not available on the other platform. The aws-lambda-haskell-runtime package, and similar projects like serverless-haskell, solve this using stack and Docker – two technologies that are probably great, but I never warmed up to them.

So instead adding layers and complexities, can I solve this instead my making things simpler? If I compiler my bootstrap into a static Linux binary, it should run on any Linux, including Amazon Linux.

Unfortunately, building Haskell programs statically is also notoriously tricky. But it is made much simpler by the work of Niklas Hambüchen and others in the context of the Nix package manager, coordinated in the static-haskell-nix project. The promise here is that once you have set up building your project with Nix, then getting a static version is just one flag away. The support is not completely upstreamed into nixpkgs proper yet, but their repository has a nix file that contains a nixpkgs set with their patches:

let pkgs = (import (sources.nixpkgs-static + "/survey/default.nix") {}).pkgs; in

This, plus a fairly standard nix setup to build the package, yields what I was hoping for:

$ nix-build -A kaleidogen
/nix/store/ppwyq4d964ahd6k56wsklh93vzw07ln0-kaleidogen-0.1.0.0
$ file result/bin/kaleidogen-amazon-lambda
result/bin/kaleidogen-amazon-lambda: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), statically linked, stripped
$ ls -sh result/bin/kaleidogen-amazon-lambda
6,7M result/bin/kaleidogen-amazon-lambda

If we put this file, named bootstrap, into a zip file and upload it to Amazon Lambda, then it just works! Creating the zip file is easily scripted using nix:

  function-zip = pkgs.runCommandNoCC "kaleidogen-lambda" {
    buildInputs = [ pkgs.zip ];
  } ''
    mkdir -p $out
    cp ${kaleidogen}/bin/kaleidogen-amazon-lambda bootstrap
    zip $out/function.zip bootstrap
  '';

So to upload this, I use this one-liner (line-wrapped for your convenience):

nix-build -A function-zip &&
aws lambda update-function-code --function-name kaleidogen \
  --zip-file fileb://result/function.zip

Thanks to how Nix pins all dependencies, I am fairly confident that I can return to this project in 4 months and still be able to build it.

Of course, I want continuous integration and deployment. So I build the project with GitHub Actions, using a cachix nix cache to significantly speed up the build, and auto-deploy to Lambda using aws-lambda-deploy; see my workflow file for details.

The Telegram part

The above allows me to run basically any stateless service, and a Telegram bot is nothing else: When configured to act as a WebHook, Telegram will send a request with a message to our Lambda function, where we can react on it.

The telegram-api package provides bindigs for the Telegram Bot API (although I had to use the repository version, as the version on Hackage has some bitrot). Slightly simplified I can write a handler for an Update:

handleUpdate :: Update -> TelegramClient ()
handleUpdate Update{ message = Just m } = do
  let c = ChatId (chat_id (chat m))
  liftIO $ printf "message from %s: %s\n" (maybe "?" user_first_name (from m)) (maybe "" T.unpack (text m))
  if "/start" `T.isPrefixOf` fromMaybe "" (text m)
  then do
    rm <- sendMessageM $ sendMessageRequest c "Hi! I am @KaleidogenBot. …"
    return ()
  else do
    m1 <- sendMessageM $ sendMessageRequest c "One moment…"
    withPNGFile  $ \pngFN -> do
      m2 <- uploadPhotoM $ uploadPhotoRequest c
        (FileUpload (Just "image/png") (FileUploadFile pngFN))
      return ()
handleUpdate _ u =
  liftIO $ putStrLn $ "Unhandled message: " ++ show u

and call this from the handler that I wrote above:

    …
    | path == "/telegram" =
      case eitherDecode (LBS.fromStrict (T.encodeUtf8 (fromMaybe "" body))) of
        Left err -> …
        Right update -> do
          runTelegramClient token manager $ handleUpdate Nothing update
          pure $ Right Response
            { statusCode = 200
            , headers = object [ "Content-Type" .= ("text/plain" :: String) ]
            , isBase64Encoded = False
            , body = "Done"
            }
    …

Note that the Lambda code receives the request as JSON data structure with a body that contains the original HTTP request body. Which, in this case, is itself JSON, so we have to decode that.

All that is left to do is to tell Telegram where this code lives:

curl --request POST \
  --url https://api.telegram.org/bot<token>/setWebhook
  --header 'content-type: application/json'
  --data '{"url": "https://api.kaleidogen.nomeata.de/telegram"}'

As a little add on, I also created a Telegram game for Kaleidogen. A Telegram game is nothing but a webpage that runs inside Telegram, so it wasn’t much work to wrap the Web version of Kaleidogen that way, but the resulting Telegram game (which you can access via https://core.telegram.org/bots/games) still looks pretty neat.

No /dev/dri/renderD128

I am mostly happy with this setup: My game is now available to more people in more ways. I don’t have to maintain any infrastructure. When nobody is using this bot no resources are wasted, and the costs of the service are neglectible -- this is unlikely to go beyond the free tier, and even if it would, the cost per generated image is roughly USD 0.000021.

There is one slight disappointment, though. What I find most intersting about Kaleidogen from a technical point of view is that when you play it in the browser, the images are not generated by my code. Instead, my code creates a WebGL shader program on the fly, and that program generates the image on your graphics card.

I even managed to make the GL rendering code work headlessly, i.e. from a command line program, using EGL and libgbm and a helper written in C. But it needs access to a graphics card via /dev/dri/renderD128. Amazon does not provide that to Lambda code, and neither do the other big Function-as-a-service providers. So I had to swallow my pride and reimplement the rendering in pure Haskell.

So if you think the bot is kinda slow, then that’s why. Despite properly optimizing the pure implementation (the inner loop does not do allocations and deals only with unboxed Double# values), the GL shader version is still three times as fast. Maybe in a few years GPU access will be so ubiquitous that it’s even on Amazon Lambda; then I can easily use that.