It has been one of my strong pursuit to figure out a properly encrypted and decentralised communication setup. Matrix’s claim to provide that is pretty strong against other alternatives. I’ve been using Riot, the most feature rich Matrix client, but mainly as an IRC bouncer.

Just the other day I read this awesome guide on Running your own secure communication service with Matrix and Jitsi and realised it’s not that difficult nowadays to setup all the pieces of the puzzle.

And so if I want to follow those steps shown in the above article but rather do it in NixOS - another project I am really excited about - how easy/difficult it would be ?

Well apart from minor tweaks, it was pretty straightforward and I would argue more simpler than how its done for a Debian based system. Following is the rundown of how I made the relevant steps work for my setup. I am not going to repeat all the nice technical explanations of above article. So anyone following should first read the above article.

Before we begin, I would also like to address one difference from the basic premise of the above article - Unlike in the above article the main domain (dangerousdemos.net) is already pointing to an existing blog hosted from a Github repository. I think this might be a case for many like me who already have a domain name serving a static blog (like this one) but want to setup Matrix via the subdomains.

So lets begin,

NixOS

With NixOS every step is declarative and hence we don’t have to worry about the mechanical rigor as is the case with most of the steps in the original article. What it entails for us broadly are these 3 steps (apart from some additional stuff)

• Update /etc/nixos/configuration.nix
• Run sudo nixos-rebuild switch
• Done!

NixOS made following the original article really easy as I could make mistakes and not worry because I could rollback and start again. Let that sink in as I think that in itself is mind-blowing.

DNS

Let’s use the same domain name - dangerousdemos.net - as used in the original article for our explanations. As mentioned above, we have one change here that the root domain already is redirecting to the static blog hosted in Github Pages. So we need to setup A records for the following subdomains:

• matrix.dangerousdemos.net (for Synapse)
• riot.dangerousdemos.net (for Riot/Web)
• jitsi.dangerousdemos.net (for Jitsi)
• turn.dangerousdemos.net (for coturn based TURN server that in original article is taken care by jitsi-meet installer)

Its important for all these to setup in the DNS before we run our configurations so that LetsEncrypt challenge flow works fine or else we might face errors.

Firewall

We need to ensure that following ports are open in the NixOS firewall for all the configurations to work fine

 # /etc/nixos/configuration.nix

  networking.firewall = {
    allowedUDPPorts = [ 5349 5350];
    allowedTCPPorts = [ 80 443 3478 3479];
  }

Nginx with LetsEncrypt

# /etc/nixos/configuration.nix


 services.nginx = {
   enable = true;
   virtualHosts = {

     ## virtual host for Syapse
     "matrix.dangerousdemos.net" = {
       ## for force redirecting HTTP to HTTPS
       forceSSL = true;
       ## this setting takes care of all LetsEncrypt business
       enableACME = true;
       locations."/" = {
         proxyPass = "http://localhost:8008";
       };
     };

     ## virtual host for Riot/Web
     "riot.dangerousdemos.net" = {
       ## for force redirecting HTTP to HTTPS
       forceSSL = true;
       ## this setting takes care of all LetsEncrypt business
       enableACME = true;
       ## root points to the riot-web package content, also configured via Nix
       locations."/" = {
           root = pkgs.riot-web;
       };
     };

     ## virtual host for Jitsi, reusing the same hostname as used
     ## while configuring jitsi-meet
     ${config.services.jitsi-meet.hostName} = {
       enableACME = true;
       forceSSL = true;
     };
   };

   ## other nginx specific best practices
   recommendedGzipSettings = true;
   recommendedOptimisation = true;
   recommendedTlsSettings = true;
 };

The above setups Nginx along with LetsEncrypt. If it’s required (like in the original article) to setup main domain as a virtual host then make an additional entry inside virtualHosts

"dangerousdemos.net" = {
  forceSSL = true;
  enableACME = true;
  locations."/" = {
    root = "/var/www/dangerousdemos.net"
  }
}

Synapse

 # /etc/nixos/configuration.nix

  services.matrix-synapse = {
    enable = true;

    ## domain for the Matrix IDs
    server_name = "dangerousdemos.net";

    ## enable metrics collection
    enable_metrics = true;

    ## enable user registration
    enable_registration = true;

    ## Synapse guys recommend to use PostgreSQL over SQLite
    database_type = "psycopg2";

    ## database setup clarified later
    database_args = {
      password = "synapse";
    };

    ## default http listener which nginx will passthrough to
    listeners = [
      {
        port = 8008;
        tls = false;
        resources = [
          {
            compress = true;
            names = ["client" "webclient" "federation"];
          }
        ];
      }
    ];

    ## coturn based TURN server integration (TURN server setup mentioned later),
    ## shared secret generated while configuring coturn
    ## and reused here (power of Nix being a real programming language)
    turn_uris = [
      "turn:turn.dangerousdemos.net:3478?transport=udp"
      "turn:turn.dangerousdemos.net:3478?transport=tcp"
    ];
    turn_shared_secret = config.services.coturn.static-auth-secret;
  };

Unlike in the original article we will do what’s recommended by Synapse team and configure PostgreSQL. In the current NixOS configuration for services.matrix-synapse it might be configuring PostgreSQL automatically based on the database_type setting but that will change in the new versions of NixOS where PostgreSQL setups need to happen separately. Here’s how we will do it for Synapse

 # /etc/nixos/configuration.nix

  services.postgresql = {
    enable = true;

    ## postgresql user and db name remains in the
    ## service.matrix-synapse.database_args setting which
    ## by default is matrix-synapse
    initialScript = pkgs.writeText "synapse-init.sql" ''
        CREATE ROLE "matrix-synapse" WITH LOGIN PASSWORD 'synapse';
        CREATE DATABASE "matrix-synapse" WITH OWNER "matrix-synapse"
            TEMPLATE template0
            LC_COLLATE = "C"
            LC_CTYPE = "C";
        '';
  };

Federation setting

Original article’s description for how to configure so that Matrix could find one’s server is nice. I am just leveraging that with one additional setting required when there is already a static blog running via Github Pages pointing to base domain:

• create a file having this path .well-known/matrix/server in the top level of the Github repository serving the static site having the following content

  { "m.server": "matrix.dangerousdemos.net:443" }

• Github Pages via Jekyll exclude dotfiles/dotdirs from serving, so we need to explicitly include them by creating _config.yml at the top level of the Github repository having the following content

  include: [".well-known"]

Riot/Web

riot-web is a package already available within Nix packages which will take care of getting the right release package along with signature verification. So we can safely add the same to systemPackages like this

 # /etc/nixos/configuration.nix

  environment = {
    systemPackages = with pkgs; [
        riot-web
    ];
  };

However, we need to let know Nix of the additional configuration required once riot-web is setup. That we could do via overlays. This is another advantage of declarative package management where we state in clear terms the state of our system which also help us revert in case unexpected happens.

 # /etc/nixos/configuration.nix

  nixpkgs.overlays = [
    (self: super: {
        riot-web = super.riot-web.override {
            conf = {
                 default_server_config = {
                    "m.homeserver" = {
                        "base_url" = "https://matrix.dangerousdemos.net";
                        "server_name" = "dangerousdemos.net";
                    };
                    "m.identity_server" = {
                        "base_url" = "https://vector.im";
                    };
                 };

                 ## jitsi will be setup later,
                 ## but we need to add to Riot configuration
                 jitsi.preferredDomain = "jitsi.dangerousdemos.net";
            };
        };
    })
  ];

Jitsi

Finally we head towards our last leg of configurations - setting up jitsi-meet. Unfortunately, current master and stable channels of Nix packages lack jitsi-meet and other supporting packages required to setup Jitsi. However, it will change pretty soon thanks to the awesome work from user mmilata in this pull request. It’s feature complete and might come as part of the next Nix release (20.03). However, we can already use the same via NUR.

 # /etc/nixos/configuration.nix

  imports =
    let
      nur-no-pkgs =
        import (
          builtins.fetchTarball
          "https://github.com/nix-community/NUR/archive/master.tar.gz"
        ) {};
    in
      [
        nur-no-pkgs.repos.mmilata.modules.jitsi-meet
      ];

The above import add only the new service to setup jitsi-meet without any other OS specific stuff. And the configuration for the new service would auto-magically setup the related software (like videobridge & jicofo) to have a functioning Jitsi. We can then add a new virtual host to the Nginx configuration with the Jitsi hostName mentioned below (shown above in Nginx Section)

 # /etc/nixos/configuration.nix

  services.jitsi-meet = {
    enable = true;
    hostName = "jitsi.dangerousdemos.net";

    ## this setting is going to add relevant ports to
    ## networking.firewall.allowedTCPPorts &
    ## networking.firewall.allowedUDPPorts
    videobridge.openFirewall = true;
  };

TURN server

jitsi-meet Debian package takes care of setting up TURN server but in our case we need to take care of it ourselves. I followed the instructions mentioned in this documentation. Nix already has a service configuration to setup coturn. Once set up, we will integrate the relevant parts to Synapse (which we have already done above).

 # /etc/nixos/configuration.nix

  services.coturn = {
    enable = true;
    use-auth-secret = true;
    static-auth-secret = "XJmzTf6VixzX5pDZKHOxtiUenkKzr10tlhBWYoti5DvCxR4TM9XlRHxII3Ml6yV2";
    realm = "turn.dangerousdemos.net";
    no-tcp-relay = true;
    no-tls = true;
    no-dtls = true;
    extraConfig = ''
        user-quota=12
        total-quota=1200
        denied-peer-ip=10.0.0.0-10.255.255.255
        denied-peer-ip=192.168.0.0-192.168.255.255
        denied-peer-ip=172.16.0.0-172.31.255.255

        allowed-peer-ip=192.168.191.127
    '';
  };

static-auth-secret generated above is via the tool pwgen which in Nix we could do like this

$ nix-shell -p pwgen --command "pwgen -s 64 1"
XJmzTf6VixzX5pDZKHOxtiUenkKzr10tlhBWYoti5DvCxR4TM9XlRHxII3Ml6yV2

Conclusion

Once we have all the above configuration in place, now is the time to finally run them all. This will take time to get all the necessary stuff downloaded and setup.

$ sudo nixos-rebuild switch

However, once its done you can launch Riot/Web, register a new user, create a room with someone else from the same MatrixVerse, have end-to-end encrypted conversation, and also start having a video call via Jitsi. All that infrastructure now being 100% owned by you with a protocol enforcing privacy and decentralisation. And finally every piece here is fully open-source.

In these times of covert and overt surveillance its imperative to take matters at your hand. And when right tools make it simple to set them up and easy to reason their behavior, it’s a nice feeling.

The blogpost Classical Logic in Haskell established a way to prove equivalences between logical propositions and law of excluded middle by writing intances of Iso for the same propositions wrapped in a newtype. Vladimir’s post contain proofs of some important propositions. I had fun proving them myself. I wanted to continue with some more.

Recently, I did the Logic and Proof course to learn both proof techniques and Lean theorem prover. It was fun. So I picked few propositions from the exercises of the Propositional Logic in Lean chapter to try write equivalence proofs for them.

Below are the propositions as newtypes (their logical notations mentioned as comment) and subsequently the Iso instances to prove their equivalences with Lem. As mentioned in the original blogpost, one nice way to progress here is by taking clues from the type system itself in the form of typed holes.

Let’s set some language pragmas

:set -XMultiParamTypeClasses
:set -XRankNTypes
:set -XInstanceSigs
:set -XScopedTypeVariables
:set -XTupleSections

Required Iso class from the original blogpost put inside a module so that it can be imported for rest of the sections

module Proof where
import Data.Void (Void, absurd)

class Iso a b where
    to :: a -> b
    from :: b -> a
    
-- Law of excluded middle
-- forall P. P \/ -P
newtype Lem m = 
    Lem
        (forall a .
            m (Either a (a -> m Void)))    

import Data.Void
import Proof

And now the propositions…

-- forall. P,Q. P /\ (P -> Q) -> Q

import Control.Monad.Fix

newtype Prop1 m = 
    Prop1 
        (forall a b. 
            (a , (a -> m b)) -> m b)
            
-- proof, implication elimination <==> LEM
instance Monad m => Proof.Iso (Prop1 m) (Lem m) where
    from :: Lem m -> Prop1 m
    from _ = Prop1 $ uncurry (flip id)
            
    to :: Prop1 m -> Lem m
    to (Prop1 i) = Lem $ fmap Left $ i (id, pure . fix)

-- forall. P,Q. P -> - (- P /\ B)

newtype Prop2 m = 
    Prop2
        (forall a b.
            (a -> m (((a -> m Void), b) -> m Void)))
            
-- proof, Prop2 <==> LEM
instance Monad m => Proof.Iso (Prop2 m) (Lem m) where
    to :: Prop2 m -> Lem m
    to (Prop2 p) = Lem $ pure $ Right proof where
        proof :: a -> m Void
        proof x = p x >>= ($ (proof, x))
    
    from :: Lem m -> Prop2 m
    from (Lem l) = Prop2 $ flip fmap l . proof where
        proof :: a -> Either a (a -> m Void) -> (((a -> m Void), b) -> m Void)
        proof x = either (flip fst) (\f _ -> f x)
        

-- forall. P,Q. - (P /\ Q) -> (P -> - Q)
import Control.Applicative (liftA2)

newtype Prop3 m = 
    Prop3
        (forall a b.
            ((a,b) -> m Void) -> m (a -> m (b -> m Void)))
            
-- proof, Prop3 <==> LEM
instance Monad m => Proof.Iso (Prop3 m) (Lem m) where
    to :: Prop3 m -> Lem m
    to (Prop3 p) = Lem 
                    $ fmap Right 
                    $ proof 
                        >>= 
                        (\f -> pure (liftA2 (>>=) f (flip id))) 
                where
                proof :: m (a -> m (a -> m Void))
                proof = p (\(x,y) -> proof >>= (($ y) =<<) . ($ x))
        
    from :: Lem m -> Prop3 m
    from (Lem l) = Prop3
                    $ (\f ->
                            pure
                                $ \a ->
                                    either (const . f . (a ,)) id <$> l)

-- forall. P,Q. -P /\ -Q -> - (P \/ Q)

newtype Prop4 m = 
    Prop4
        (forall a b.
            ((a -> m Void , b -> m Void) -> m (Either a b ->  m Void)))
            
-- proof, Prop4 <==> LEM
instance Monad m => Proof.Iso (Prop4 m) (Lem m) where
    to :: Prop4 m -> Lem m
    to (Prop4 p) = Lem 
                    $ pure 
                    $ Right 
                        ((proof >>=) . flip id . Left)
                where
                proof :: m (Either a a -> m Void)
                proof = curry p ((proof >>=)
                                . flip id
                                . Left) 
                                ((proof >>=)
                                . flip id
                                . Right)
        
    from :: Lem m -> Prop4 m
    from _ = Prop4 $ uncurry $ (pure .) . either

This is an IHaskell Notebook which is pretty cool for above kind of experiments. Much more feature rich than GHCi. I got the inspiration from Vaibhav Sagar who writes all his posts as IHaskell Notebooks.

This year was mostly uneventful unlike 2017. However, I did do a lot more technical reading - mostly papers and a few books - than previous years. Professionally things changed quite drastically. I am now meant to do mostly research-y things than what used to be half & half with engineering before. Not that I complain, my feelings are on the contrary actually. But this whole new setting at work, both from an operations & vision standpoint, is still clumsy and need more time to shape up well.

I am beginning to focus on the areas of Knowledge Engineering. I want to tie it with fascinating things from Type Systems. I believe their shared foundations in Mathematical Logic will provide interesting things to work on. And my choice of technology to realise any such research will be Haskell, mostly.

So apart from spending most of the time reading papers on the history of knowledge bases, their representation, and reasoning I also tried to get used to logic and proofs. During one such excavation, I landed on a course aptly named Logic and Proof which uses this beautiful language called Lean to write the proofs. Lean, like Haskell, has its roots in Microsoft Research. It, like Agda, is dependently typed language which also provides means to do inductive/automated theorem proving. It was my first foray into the world of computational theorem proving and some serious work with dependent types (I did dabble with Idris but it is better not to talk about that). Working with Lean and learning more about its origins and background type systems research gave me ideas that I believe are relevant to knowledge systems.

With Lean, I digressed heavily into learning dependent types, this time with a larger vision to make them useful for knowledge systems. And hence I got this amazing book called The Little Typer. It provides the necessary foundations for me to relate dependent types, higher-order logic, relational programming, and eventually their role in knowledge systems. I am nowhere close to anything concrete to go after but I am having fun peeling the layers of these seemingly disjoint fields converging together elegantly.

Haskell with its dependent typing tools is nowhere close to things that Lean and Agda could do today. But it’s still amazing how far the current type system could take you. Sandy Maguire’s new book is how I am trying to get my head around all those esoteric corners of Haskell. It’s pretty good.

I also want to mention one other thing that is happening coincidentally and maybe right now I am not able to leverage it to its full extent only coz of my lack of understanding but I am pretty sure it will be something that I will be leaning a lot in future. And that is Edward Kmett’s Twitch videos on his creation of Guanxi. Ed’s videos are highly motivational (for some apparent indescribable reason).

Finally, I also want to highlight that I continued persevering with Nix irrespective of it still not friendly as a package manager in macOS. I realised that there’s no other way, right now, to reading nixpkgs source code to make stuff work properly with Nix especially in macOS. Hopefully, it will improve and I will also do my best towards that goal. But Nix is the future of so-called devops that I believe in and I want it to succeed at all costs.

As my daughter grows up to her 3rd year of existence in 2019, I am hoping her to be a bit more independent and me getting a bit more time off work to try to contribute to some open source Haskell projects. Having a 2-year-old kid around when you are trying to do some focussed programming session is not a happy setting (no offence to any 2-year-olds).

I learnt a lot of new things in 2018 that now I think I have some roadmap for next year to channel my energies on. But none of them is related to Deep Learning, Blockchain, or Microservices unfortunately !!

The Final

Croatia 2 - France 4

It could not have been more engaging and dramatic than what unfolded as one of the best World Cup finals of recent times. The game started with Croatians putting their heart and soul into the game. They created the first scare for France and were relentless in their pursuit to score early. It was first 15-20 minutes of a gripping game of Croatian attack & pressure tactics. Unfortunately French got it past Croatian net for no credit of theirs. Croatian reply by the amazing Perisic was spellbinding. VAR came to the rescue of France as it’s been from their first game. I believe the resulting penalty was the turning point of the game.

The second half belonged to France. They showed their class with superb ball control and creative ball passing. Both Pogba’s and Mbappe’s goals were astounding. They are the signs of a team worthy of being a champion. Croatia, in the end, succumbed due to a bit of bad luck and a better opponent.

As the curtains dropped, I consider this edition of the World Cup to be one of the best of the modern era. It was full of honest surprises and impressive comebacks. But more than ever this World Cup was for those who dared to dream and deliberated on it by having fun rather than for those who either got complacent or were bored with the game.

3rd & 4th place game

England 0 - Belgium 2

Belgians came back with their inventive & creative gameplay. It was a treat to watch. England did not change much on playing boring football. It was fantastic watching Hazard & De Bruyne sweating & overcoming clueless English midfield & defence. Hazard, in particular, created more chances than out-of-form Lukaku could handle. Belgium in a way deserved more than the 3rd place. And England needs to find fun in their game to start with.

Semifinal #2

England 1 - Croatia 2

Ivan Sršen describing the mood as Croatian goalkeeper saved the decisive penalty against Russia in quarterfinal

For a brief moment at least, to me and perhaps to all of us in the bar, it felt as though the war was finally over.

Ivan also talks about the legacy of Croatian football and background of some current Croatian players like Modrić and Lovren. It highlights the significance of Croatian progress in this World Cup.

Football, the so-called beautiful game, only needs a pair of legs and pile of passion. That way it binds people from every stratum of society.

Last night the Croatian players showcased matured & infallible football. It was a gripping game. Barring that superb 4th-minute free-kick, England had nothing to showcase in the whole 120 minutes. The Croatian players, like their coach, had a unique sense of calmness and deep focus. Which led them to dominate England in the whole match. England, as I have earlier mentioned as well, lacked both individual skills & collective playmaking. Their early lead was never meant to stand against the pressing Croatian attack.

Croatia will face a much tougher & skilful opposition in France in the final. They should work on improving their pass accuracy and man-tagging in the back, especially for the speedster Mbappe. But this nail-biting win over England should lift their spirits. They will attempt to cause the unthinkable for their country as they have done with their lives.

Semifinal #1

Belgium 0 - France 1

Kylian Mbappé is a revolution. 4 mins in the match the way he ran from midfield to almost inside the Belgium goal post with the ball set the tone of the rest of the match. It would have been more misery for Belgium if his out of form teammate Giroud would have converted some wonderful passes. Belgium suffered from a lack of interest shown by their centre-forward Lukaku. He hardly kicked the ball in the overall match. Hazard was persistent & De Bruyne tried his best to create chances from the flanks. Second half substitution of Mertens brought some much-needed energy to the team. But they suffered from a similar conundrum that Brazil had against them in the quarterfinal. France after scoring the crucial goal went to a full defensive mode. Which was kind of expected. It was a nice game & I feel bad for the Belgs. This was the best team they could ever have. France on the, on the other hand, is clear if Mbappé maintains his pace & check his cheekiness.

England has the best chance to go for the cup and hosts, unfortunately, had to stop at Quarters.

Sweden 0 - England 2

This English team is playing like a well-oiled machine. Lacking individual skills they rely more on each other & set pieces to deliver. And they are doing that pretty well. They now have clear shot to the finals. And depending on who will stand on the other side if this team play sensibly they might do the unthinkable.

Russia 2 (3) - Croatia 2 (4)

It might be the loudest game of the tournament. Much of that roar was for host nation Russia. Russians did not disappoint at all. It was a game of blistering pace & passion. Croatia, as I had previously pointed out, is playing with all their heart. They have not shown any sign of big tournament chill like many other underdogs. Which make their case against England in semis pretty interesting.

It will be again a European crown like last time.

Uruguay 0 - France 2

It was a game of tussle between Uruguayan desperation & French persuasion. Without Cavani, the Uruguayan attack was like an already amputated man losing his last leg. Suarez tried his best to muster a number of chances. But none of his teammates had the vision or talent to work with them. France realised that & made sure they don’t do anything silly on the back. French game had the same fluidity like last time. Mbappe showed some interesting skills both with his legs & drama. However, I felt Uruguayans were not that bewildered by French defence. Which might be enough for Martinez’s jubilant men to easily triumph in the semis.

Brazil 1 - Belgium 2

This was the best match of the tournament so far for me (many consider Belgium’s last match with Japan to be the best). It was a great night of football where teams played to their best with a worthy winner in the end. Brazil’s painstaking efforts to penetrate Belgium defence was a treat to watch. Also quite heartbreaking. Belgium’s superb tactic to make De Bruyne play from the centre with Lukaku in the flanks split wide open Brazilian defence. Lukaku was unstoppable & Hazard was critical. But I would say the real hero of the match was Courtois. His gravity-defying saves took the match away from Brazil.

Tite’s plan to not start with Firmino again might be a bad move. He along with Costa made quite an impression in the second half. However, I felt Brazil lacks a physically strong attacking player who could withstand the pushing & shoving to rush inside a stubborn defence. Current talents like Neymar & Coutinho are too feeble to make their way in & hence spend most of the time strolling around the penalty circle. Brazil also missed some straightforward chances which are a criminal offence in the World Cup. Brazil did not disappoint like last time. I wish they progress further next time in Qatar.

In the meantime, I am betting on Belgium as champions.

Knockouts Day 3

Sweeden & Switzerland should be banned for playing the most boring game of the World Cup. And England narrowly missed their exit.

Columbia 1 (3) - England 1 (4)

Watching English players on the field is like watching a Twitch stream of someone playing the latest version of EA Sports’ FIFA. Their gameplay and style were so mechanical that it bored me to death. Columbians, on the other hand, showed exquisite legwork whenever they found time after doing those unnecessary pushing, shoving, and play-acting drama. The game was more of reality tv than a real sport. I pity the referee who should avoid travelling to South America anytime soon. England’s path till finals henceforth is easy (assuming Croatia don’t panic against Russia and then get beaten by the English luck). Also, their next game should be called off by sending Sweeden home for wasting the time of thousands of spectators with the most dreadful game of the tournament against Switzerland.