{ self }:
{ config, lib, pkgs, ... }:
let
  config' = config;
  lib' = self.lib.x86_64-linux-x86_64-genode;
  pkgs' = self.packages.x86_64-linux-x86_64-genode;

  modulesPath = "${self.inputs.nixpkgs}/nixos/modules";

  cfg = config.genode;

  toVdi = config:
    import "${modulesPath}/../lib/make-disk-image.nix" {
      inherit config lib pkgs;
      diskSize = config.virtualbox.baseImageSize;
      partitionTableType = "legacy";
      fsType = "ext4";
      name = "nixos-${pkgs.stdenv.hostPlatform.system}.vdi";
      format = "vdi";
    };

  guestChildren = lib'.runDhallCommand "vbox.dhall" { } (''
    dhall > $out << END
    let Genode = env:DHALL_GENODE
    in [
  '' + builtins.concatStringsSep "," (lib.mapAttrsToList (vmName: cfg:
    let
      inherit (cfg) config;
      vdiFile = "${toVdi config}/nixos.vdi";
    in lib'.runDhallCommand "vbox.dhall" { } ''
      vdiUuid=$(${pkgs.virtualbox}/bin/VBoxManage showmediuminfo "${vdiFile}" | awk '/^UUID:/ {print $2}')
      dhall > $out << END
      { mapKey = "vbox-${vmName}"
      , mapValue =
          ${./dhall/vbox-guest.dhall}
            { vdiFilename = "${vdiFile}"
            , vdiUuid = "$vdiUuid"
            , memorySize = ${toString config.virtualbox.memorySize}
            , vmName = "${vmName}"
            }
      }
      END
    '') config.genode.guests) + ''
      ] : Genode.Init.Children.Type
      END
    '');

  initConfig = "${./dhall}/vbox-host.dhall ${guestChildren}";

  buildBootDescription =
    self.legacyPackages.x86_64-linux.callPackage ./buildBootDescription.nix {
      lib = lib';
    };

  bootDescription = buildBootDescription {
    inherit initConfig;
    imageInputs = map pkgs'.genodeSources.depot ([
      "acpi_drv"
      "ahci_drv"
      "chroot"
      "cached_fs_rom"
      "init"
      "input_filter"
      "ipxe_nic_drv"
      "libc"
      "libiconv"
      "log_core"
      "nit_fb"
      "nitpicker"
      "part_block"
      "platform_drv"
      "ps2_drv"
      "report_rom"
      "rom_logger"
      "rtc_drv"
      "rump"
      "stdcxx"
      "terminal"
      "terminal_log"
      "vbox5"
      "vfs"
      "vfs_audit"
      "vfs_ttf"
    ] ++ lib.optional (cfg.fbDriver == "vesa") "vesa_drv"
      ++ lib.optional (cfg.fbDriver == "intel") "intel_fb_drv")
      ++ (with pkgs'; [ base-nova block_router ]);
    extraBinaries = [
      "ld.lib.so"
      "libc.so"
      "libc_pipe.so"
      "libiconv.so"
      "libm.so"
      "libqemu-usb.so"
      "librump.so"
      "librump_fs.so"
      "libstdcxx.so"
      "libvfs.so"
      "libvfs_audit.so"
      "libvfs_rump.so"
      "libvfs_ttf.so"
    ];
    extraRoms = {
      "Inconsolata.ttf" =
        "${pkgs.inconsolata}/share/fonts/truetype/inconsolata/Inconsolata-Regular.ttf";
    };
  };

  firmware = lib'.novaImage "stage0" { gzip = true; } bootDescription;

in {

  options.genode = with lib; {
    fbDriver = mkOption {
      default = "vesa";
      type = types.enum [ "intel" "vesa" ];
      description = ''
        Set framebuffer driver.
      '';
    };
    guests = mkOption {
      type = types.attrsOf (types.submodule ({ config, options, name, ... }: {
        options = {

          config = mkOption {
            description = ''
              A specification of the desired configuration of this
              guest VM, as a NixOS module.
            '';
            type = mkOptionType {
              name = "Toplevel NixOS config";
              merge = loc: defs:
                (import "${modulesPath}/../lib/eval-config.nix" {
                  inherit (config'.nixpkgs) system;
                  modules =
                    [ "${modulesPath}/virtualisation/virtualbox-image.nix" ]
                    ++ (map (x: x.value) defs);
                  prefix = [ "guests" name ];
                }).config;
            };
          };

        };
      }));
      default = { };
    };
  };

  config = {
    system.build.genode = {
      inherit firmware;
      config = lib'.runDhallCommand "config.dhall" { }
        ''dhall > $out <<< "${initConfig}"'';
    };

    boot.loader.grub = {
      extraEntries = ''
        menuentry Genode on NOVA {
        	insmod multiboot2
        	insmod gzio
        	multiboot2 /bender
        	module2 /hypervisor hypervisor iommu novpid serial logmem
        	module2 /image.elf.gz image.elf
        }
      '';

      extraFiles = {
        "bender" = "${pkgs'.genodeSources}/tool/boot/bender";
        "hypervisor" = "${pkgs'.NOVA}/hypervisor-x86_64";
        "image.elf.gz" = "${firmware}/image.elf.gz";
      };
    };
  };
}