A chat server that runs itself

A room is a shard of a keyed topic. RoomTalk shards by room, so delivering to the right room is the bus's job, and a room never sees another room's traffic. No room keeps a member list.

type ChatLine { room: Int; who: String; text: String; }
type Join     { room: Int; who: String; }

topic RoomTalk { payload: ChatLine; keyed_by room; }
topic Joins    { payload: Join; }

Session tags come from a sealed signer. @sealed makes the key readable only from inside the locus's own methods, so the rest of the program can ask for a signature and never holds the key. secret_use marks the one privileged operation for the rule written below.

@sealed locus SessionSigner {
    params { key: Int = 40961; }
    @effects(is: {secret_use})
    fn stamp(room: Int) -> Int { return room * 31 + self.key % 997; }
}

A room subscribes to its own shard and stamps every line it relays. The room calls stamp on the guest's behalf, and that mediation is about to become law.

locus Room {
    params { room: Int = 0; lines: Int = 0; s: SessionSigner = SessionSigner { }; }
    bus {
        subscribe RoomTalk as post where key == self.room;
    }
    fn post(line: ChatLine) {
        self.lines = self.lines + 1;
        let tag = self.s.stamp(line.room);
        println("[room ", line.room, " #", tag, "] ", line.who, ": ", line.text);
    }
}

The spam guard is here to show supervision working. Its closure demands one warmup, and the assembly below constructs it wrong on purpose. The transcript shows the closure failing, the parent's on_failure firing, restart re-running birth, and the closure passing. Recovery is written in the program text, where an ops runbook would usually hold it.

locus SpamGuard {
    params { warmups: Int = 0; }
    closure warmed_up {
        self.warmups ~~ 1 within 0;
        epoch birth;
    }
    birth() {
        self.warmups = self.warmups + 1;
        println("~ spam guard warm (attempt ", self.warmups, ")");
    }
}

The doorman greets joins on an ordinary unkeyed topic. Not everything needs a shard.

locus Doorman {
    params { seen: Int = 0; }
    bus { subscribe Joins as greet; }
    fn greet(j: Join) {
        self.seen = self.seen + 1;
        println("* ", j.who, " joined room ", j.room);
    }
}

Participants are scripted so this page can run itself: join, say hello, ask the eternal question. A deployed chat server would put them behind a transport binding, and nothing else on this page would change.

locus Participant {
    params { name: String = "guest"; room: Int = 0; }
    bus { publish RoomTalk; publish Joins; }
    run() {
        Joins <- Join { room: self.room, who: self.name };
        RoomTalk <- ChatLine { room: self.room, who: self.name, text: "hello" };
        RoomTalk <- ChatLine { room: self.room, who: self.name, text: "anyone here?" };
    }
}

Two one-line groups, because the rule below quantifies over them, and over every participant and room anyone adds later.

group participants = { Participant };
group rooms        = { Room };

The claim says guests may reach the signer only through rooms. The first draft said forbid reaches(participants, effects(secret_use)) outright, and the compiler rejected the design with the witness Participant::run -(publishes "RoomTalk")-> Room::post -> SessionSigner::stamp. Guests do reach the signer, through the room, because the room stamps on their behalf. avoiding rooms states the real rule, which is mediation. Hand a participant its own signer and the claim catches the bypass:

main locus ChatServer {
    params {
        lobby: Room = Room { room: 0 };
        dev: Room = Room { room: 1 };
        door: Doorman = Doorman { };
        guard: SpamGuard = SpamGuard { warmups: -1 };
        ada: Participant = Participant { name: "ada", room: 0 };
        lin: Participant = Participant { name: "lin", room: 1 };
        alan: Participant = Participant { name: "alan", room: 0 };
    }
    on_failure(g: SpamGuard, err: ClosureViolation) {
        println("! ", err.closure, " failed on ", err.locus, " — restarting");
        restart (g);
    }
    claims {
        guests_sign_only_via_rooms:
            forbid reaches(participants, effects(secret_use))
                avoiding rooms;
    }
    run() { }
}
fn main() { ChatServer { }; }

Give a guest a signer of its own — and let it stamp.
- locus Participant {
-     params { name: String = "guest"; room: Int = 0; }
+     params { name: String = "guest"; room: Int = 0; s: SessionSigner = SessionSigner { }; }

$ hale check chat.hl
chat.hl:75:9: type error: claim `guests_sign_only_via_rooms` violated: `participants` reaches `effects(secret_use)` — witness: `Participant::run` -> `SessionSigner::stamp`
            guests_sign_only_via_rooms:
            ^^^^^^^^^^^^^^^^^^^^^^^^^^
chat.hl:50:22: type error: claim `guests_sign_only_via_rooms`: the boundary into `effects(secret_use)` is crossed by this call
            let forged = self.s.stamp(self.room);
                         ^^^^^^^^^^^^^^^^^^^^^^^
chat.hl:7:15: type error: claim `guests_sign_only_via_rooms`: the forbidden destination `SessionSigner` is declared here
    @sealed locus SessionSigner {
                  ^^^^^^^^^^^^^

$ hale run chat.hl
~ spam guard warm (attempt 0)
* ada joined room 0
[room 0 #84] ada: hello
[room 0 #84] ada: anyone here?
* lin joined room 1
[room 1 #115] lin: hello
[room 1 #115] lin: anyone here?
* alan joined room 0
[room 0 #84] alan: hello
[room 0 #84] alan: anyone here?
! warmed_up failed on SpamGuard — restarting
~ spam guard warm (attempt 1)