krn: synthesis with constraints

Some values are not written but found: a port no other app uses, memory that fits a host, a database host in the right environment. yen.lib.krn is µKanren with constraints. It has logic variables, unification over attrsets, lists and scalars, and goals that run in both directions.

{ yen, lib, ... }:
{
  yen.kinds.fleet = {
    spawns.host = _: yen.host;
    sinks.out.reduce = yen.lib.reduce.merge;
  };
  yen.kinds.host.fields.apps = yen.lib.is (v: lib.isList v && lib.all lib.isString v);

  yen.fleet.main = { };
  yen.host.lb.apps = [
    "grafana"
    "loki"
    "prometheus"
  ];
  yen.flake = { out, ... }: out;
}

# µKanren with finite domains: give each app a port in 8080..8083, all different, prometheus before grafana.
{ yen, lib, ... }:
let
  inherit (yen.lib.krn)
    run
    runAll
    freshNamed
    infd
    distinctfd
    ltfd
    eq
    label
    runFuel
    ;
  ports =
    apps: q:
    freshNamed apps (vs: [
      (infd (lib.attrValues vs) 8080 8083)
      (distinctfd (lib.attrValues vs))
      (ltfd vs.prometheus vs.grafana)
      (eq q vs)
      (label (lib.attrValues vs))
    ]);
  lb = yen.host.lb;
in
{
  yen.aspects.ports = {
    at = yen.kinds.fleet;
    out.ports = {
      first = run 1 (ports lb.apps); # one answer
      count = lib.length (runAll (ports lb.apps)); # every answer
      # the same relation, run backward: which app can take 8080?
      on8080 = lib.unique (
        lib.concatMap (a: lib.attrNames (lib.filterAttrs (_: p: p == 8080) a)) (runAll (ports lb.apps))
      );
      # a bounded search: `complete = false` means "stopped", never "no answer"
      bounded = removeAttrs (runFuel 1 5 (ports lb.apps)) [ "answers" ];
    };
    errors = lib.optional (run 1 (ports lb.apps) == [ ]) "ports: no assignment for lb";
  };
}

{
  bounded = {
    complete = false;
  };
  count = 12;
  first = [
    {
      grafana = 8081;
      loki = 8082;
      prometheus = 8080;
    }
  ];
  on8080 = [
    "prometheus"
    "loki"
  ];
}

grafana can never take 8080: prometheus must be lower. The same relation, read backward, says so.

Goal	Meaning
`eq u v`, `fresh`, `freshNamed`, `disj`, `conde`, `project`	µKanren: unify, new variables, any of, clauses, read a value
`neq u v`	`u` and `v` never unify
`dom x [ … ]`, `infd xs lo hi`	finite domains
`lefd`, `ltfd`, `plusfd x y z`, `neqfd`, `distinctfd xs`	propagation over domains
`label xs`	enumerate what is left, smallest domain first
`cons`, `appendo`, `membero`, `fromList`, `toList`	relational lists
`facto rows pattern`	a table of facts
`run n`, `runAll`, `runC n`	answers; `runC` adds the constraints left on fresh variables
`runFuel n fuel`, `runAllFuel fuel`, `maximize fuel measure`	bounded search: `{ answers; complete; }`

Contribute Community Sponsor