A chat server that runs itself
A complete chat server in one file: two rooms as shards of a keyed topic, a sealed signer stamping every relayed line, a deliberately mis-constructed spam guard that supervision repairs mid-transcript, and three scripted participants so the whole thing runs itself. The centerpiece is the claim — guests reach the signer only through rooms — which this page's own first draft got wrong, and the compiler corrected.
Rooms are not objects with member lists — they are a keyed topic. `RoomTalk` shards by `room`, so delivery to the right room is the bus's job, and a room never sees another room's traffic.
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` means the key is readable only from inside the locus's own methods — the rest of the program holds a phone number, not the key — and `secret_use` marks the one privileged operation for the law 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. Note who calls `stamp`: the room, on the guest's behalf. 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 exists to show supervision working, not to be clever: its closure demands one warmup, and the assembly below constructs it wrong on purpose. Watch the transcript — the closure fails, the parent's `on_failure` fires, `restart` re-runs birth, the closure passes. Recovery is part of the program text, not an ops runbook.
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. In a deployed chat server these would sit behind a transport binding; 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 law below quantifies over them — and over every participant and room anyone adds later.
group participants = { Participant };
group rooms = { Room };The claim is the page's centerpiece: guests may only reach the signer via rooms. Not "never" — the first draft said `forbid reaches(participants, effects(secret_use))` outright, and the compiler rejected the honest 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` is the real law — mediation, not prohibition. 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)
! warmed_up failed on SpamGuard — restarting
~ spam guard warm (attempt 1)
* 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?