{
  lib,
  pkgs,
  config,
  options,
  ...
}:
let
  cfg = config.programs.benchexec;
  opt = options.programs.benchexec;

  filterUsers =
    x:
    if builtins.isString x then
      config.users.users ? ${x}
    else if builtins.isInt x then
      x
    else
      throw "filterUsers expects string (username) or int (UID)";

  uid =
    x:
    if builtins.isString x then
      config.users.users.${x}.uid
    else if builtins.isInt x then
      x
    else
      throw "uid expects string (username) or int (UID)";
in
{
  options.programs.benchexec = {
    enable = lib.mkEnableOption "BenchExec";
    package = lib.options.mkPackageOption pkgs "benchexec" { };

    users = lib.options.mkOption {
      type = with lib.types; listOf (either str int);
      description = ''
        Users that intend to use BenchExec.
        Provide usernames of users that are configured via {option}`${options.users.users}` as string,
        and UIDs of "mutable users" as integers.
        Control group delegation will be configured via systemd.
        For more information, see <https://github.com/sosy-lab/benchexec/blob/3.18/doc/INSTALL.md#setting-up-cgroups>.
      '';
      default = [ ];
      example = lib.literalExpression ''
        [
          "alice" # username of a user configured via ${options.users.users}
          1007    # UID of a mutable user
        ]
      '';
    };
  };

  config = lib.mkIf cfg.enable {
    assertions =
      (map (user: {
        assertion = config.users.users ? ${user};
        message = ''
          The user '${user}' intends to use BenchExec (via `${opt.users}`), but is not configured via `${options.users.users}`.
        '';
      }) (builtins.filter builtins.isString cfg.users))
      ++ (map (id: {
        assertion = config.users.mutableUsers;
        message = ''
          The user with UID '${id}' intends to use BenchExec (via `${opt.users}`), but mutable users are disabled via `${options.users.mutableUsers}`.
        '';
      }) (builtins.filter builtins.isInt cfg.users));

    environment.systemPackages = [ cfg.package ];

    # See <https://github.com/sosy-lab/benchexec/blob/3.18/doc/INSTALL.md#setting-up-cgroups>.
    systemd.services = builtins.listToAttrs (
      map (user: {
        name = "user@${builtins.toString (uid user)}";
        value = {
          serviceConfig.Delegate = "yes";
          overrideStrategy = "asDropin";
        };
      }) (builtins.filter filterUsers cfg.users)
    );

    # See <https://github.com/sosy-lab/benchexec/blob/3.18/doc/INSTALL.md#requirements>.
    virtualisation.lxc.lxcfs.enable = lib.mkDefault true;

    # See <https://github.com/sosy-lab/benchexec/blob/3.18/doc/INSTALL.md#requirements>.
    programs = {
      cpu-energy-meter.enable = lib.mkDefault true;
      pqos-wrapper.enable = lib.mkDefault true;
    };

    # See <https://github.com/sosy-lab/benchexec/blob/3.18/doc/INSTALL.md#kernel-requirements>.
    security.unprivilegedUsernsClone = true;
  };

  meta.maintainers = with lib.maintainers; [ lorenzleutgeb ];
}