Skip to content
{yen}

Invariants

An invariant is a rule about the whole fleet: “no server runs a desktop”, “no two hosts share an address”. yen.invariants.<name> gives Datalog rules over the fleet’s facts. A true bad: atom is a violation.

modules/fleet.nix
{ yen, lib, ... }:
{
  yen.kinds.fleet = {
    spawns.host = _: yen.host;
    sinks.out.reduce = yen.lib.reduce.merge;
  };
  yen.kinds.host.fields = {
    addr = lib.types.str;
    form = lib.types.enum [
      "server"
      "laptop"
    ];
  };


  yen.fleet.main = { };
  yen.host.web = {
    addr = "10.0.0.1";
    form = "server";
  };
  yen.host.db = {
    addr = "10.0.0.2";
    form = "server";
  };
  yen.host.thinkpad = {
    addr = "10.0.0.50";
    form = "laptop";
  };
  yen.aspects.desktop.at = s: (s.form or null) == "laptop";
  yen.aspects.postgres.at = yen.host.db;
  yen.flake = { out, ... }: out;
}
modules/invariants.nix
# Rules over `r.facts`. A true `bad:` atom is a violation. Facts: kind:K:ID, has:ASPECT:ID, val:FIELD:ID:VALUE, …
{ yen, lib, ... }:
{
  # no server runs a desktop
  yen.invariants.no-desktop-on-servers =
    { scopes, ... }:
    map (s: {
      head = "bad:desktop-on-server:${s.name}";
      pos = [ "has:desktop:${s.id}" ];
    }) (lib.filter (s: s.kind == "host" && s.form == "server") scopes);
  # no two hosts share an address: a rule across machines
  yen.invariants.unique-addr =
    { scopes, ... }:
    let
      hosts = lib.filter (s: s.kind == "host") scopes;
    in
    lib.concatMap (
      a:
      map (b: {
        head = "bad:same-addr:${a.name}:${b.name}";
        pos = [
          "val:addr:${a.id}:${a.addr}"
          "val:addr:${b.id}:${a.addr}"
        ];
      }) (lib.filter (b: a.name < b.name) hosts)
    ) hosts;
}

The function gets scopes, graph, active and facts. Facts are ground atoms:

FactHolds when
scope:ID, kind:K:IDa scope exists, and its kind
has:ASPECT:IDthe aspect is active at the scope
edge:SINK:FROM:TOan element is routed
val:FIELD:ID:VALUEa field has a scalar value
ref:FIELD:ID:KIND:NAMEa field refers to an instance
error:CODE:FROMan error record

This fleet holds:

result
{
  incomplete = [ ];
  invariants = [
    "no-desktop-on-servers"
    "unique-addr"
  ];
  ok = true;
  violations = [ ];
}

A change that breaks two rules

Section titled “A change that breaks two rules”
variants/mistakes.nix
# A desktop on a server, and a new host with a copied address.
{ yen, ... }:
{
  yen.aspects.desktop.at = yen.host.web;
  yen.host.spare = {
    addr = "10.0.0.2";
    form = "server";
  };
}
result
{
  ok = false;
  violations = [
    "bad:desktop-on-server:web"
    "bad:same-addr:db:spare"
  ];
}

r.check.why atom gives the rules that prove a violation. whyNot and proof work as in Datalog:

result
[
  {
    head = "bad:same-addr:db:spare";
    pos = [
      "val:addr:fleet:main/host:db:10.0.0.2"
      "val:addr:fleet:main/host:spare:10.0.0.2"
    ];
  }
]
Contribute Community Sponsor