Joachim Breitner

Blog

Leaving DFINITY

Published 2021-06-19 in sections English.

Last Thursday was my last working day at DFINITY. There are various reasons why I felt that after almost three years the DFINITY Foundation isn’t quite the right place for me anymore, and this plan has been in the making for a while. Primarily, there are personal pull factors that strongly suggest that I’ll take a break from full time employment, so I decided to see the launch of the Internet Computer through and then leave.

DFINITY has hired some amazing people, and it was a great pleasure to work with them. I learned a lot (some Rust, a lot of Nix, and just how merciless Conway’s law is), and I dare say I had the opportunity to do some good work, contributing my part to make the Internet Computer a reality.

I am especially proud of the Interface Specification and the specification-driven design principles behind it. It even comes with a model reference implementation and acceptance test suite, and although we didn’t quite get to do formalization, those familiar with the DeepSpec project will recognize some influence of their concept of “deep specifications”.

Besides that, there is of course my work on the Motoko programming language, where I build the backend,a the Candid interoperability layer, where I helped with the formalism, formulated the a generic soundness criterion for Interface Description Languages in a higher order settings and formally verified that in Coq. Fortunately, all of this work is now Free Software or at least Open Source.

With so much work poured into this project, I continue to care about it, and you’ll see me post on the the developer forum and hack on Motoko. As the Internet Computer becomes gradually more open, I hope I can be gradually more involved again. But even without me contributing full-time I am sure that DFINITY and the Internet Computer will do well; when I left there were still plenty of smart, capable and enthusiastic people forging ahead.

So what’s next?

So far, I have rushed every professional transition in my life: When starting my PhD, when starting my postdoc, when starting my job at DFINITY, and every time I regretted it. So this time, I will take a proper break and will explore the world a bit (as far as that is possible given the pandemic). I will stresslessly contribute to various open source projects. I also hope to do more public outreach and teaching, writing more blog posts again, recording screencasts and giving talks and lectures. If you want to invite me to your user group/seminar/company/workshop, please let me know! Also, I might be up for small interesting projects in a while.

Beyond these, I have no concrete plans and am looking forward to the inspiration I might get from hiking through the Scandinavian wilderness. If you happen to stumble across my tent, please stop for a tea.

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

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:

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:

  • nix

    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.

  • haskell.nix

    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

    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.

  • Cachix.org

    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:

section on static building with some flags to cargo-cult.

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.

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.

install-nix-action.

nix and Cachix tutorial for good instructions.

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

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

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.

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

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

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!