Proving the promises

Evil Engine makes a lot of promises. Every playermodel from every mount shows up in the picker. Two players with the same game can join the same server, whatever else they’ve installed. Nothing a server sends can touch your files. Plugins only ever add, they never take away.

Each of those gets written down in a scope before any code exists, which I went over in Starting over on purpose. There are a few dozen scopes now though, and a decision in one can quietly break a promise made in another. Rereading all of them after every change doesn’t scale, and I don’t trust myself to catch everything anyway, so the promises live in Lean now too.

Lean

Lean is a programming language you can also write proofs in. You state something, like “after any sequence of patches, everything that was listed is still listed”, then prove it, and if the proof has a hole it doesn’t build. The design gets written in Lean alongside the docs, and every time a scope changes, everything gets rechecked against every law.

How it’s set up

Each law is a definition of what has to hold for every game, every machine and every Plugin. Each scope’s design is its own module, written straight from what the scope says. A theorem then either proves the design keeps the law, or proves it doesn’t by producing the case that breaks it.

Here’s law 10, “everything is listed”:

def Law10 (apply : Op → List Record → List Record) : Prop :=
  ∀ base (ops : List Op), ∀ e ∈ listings base,
    e ∈ listings (ops.foldl (fun reg o => apply o reg) base)

Start from any records, apply any sequence of patches, and anything that was in a menu before is still in a menu after.

Some decisions don’t need a theorem at all. A converter is typed so it only ever sees its own game’s files, so the old design where it peeked at your other mounts can’t even be written.

It’s 123 theorems in about 2,500 lines so far, with no unfinished proofs and no extra libraries.

What it caught

Most of the design proved as written, but not all of it:

• Patches could remove a mount’s record outright, so remove = true on Charple took it out of every menu. Hiding is its own key now, and only folds an entry away
• Even after that, remove = ["player"] took Kleiner out of the playermodel picker, since the player table is what makes a person a playermodel. Patches can’t remove a key that decides which list a record is in anymore
• Hashing one registry of everything you’d mounted meant a single extra Workshop addon gave you a different session key than the server, which is why there are two registries now
• “Every skinned, animated model is a person” turned Garry’s Mod’s ragdoll Kleiner into a person. Now only what a game lists as a body gets sorted
• Joining on a game’s build fingerprint meant a player who updated Garry’s Mod between sessions couldn’t join. Joining compares the files the server actually needs instead
• Two Plugins that each need the other’s API could load with one running before the other’s API existed. Cycles get refused now, except for two Plugins that only want each other, which both load
• Events nested too deep got dropped silently. They’re still dropped, but with a note naming the Plugin that raised them
• A client-only Plugin sending inputs shifted the command numbering on just that one machine, so only Plugins on both sides send inputs now
• The movement scope rounded Garry’s Mod’s player hull to the nearest centimeter, which is off by up to 2.8 mm against the 1 mm its own test allows
• Animation clips with no ground speed would’ve had feet sliding, so in-place clips measure it from their planted feet now

All of those got fixed in the docs, and the fixes got proved. The broken versions stay in as theorems too, so I can’t wander back into one later.

Keeping the docs honest

A proof is only worth something if it proves what the docs actually say. A second step puts each law, quoted word for word from the docs, beside the Lean that states it and the theorem that proves it. If a quoted line changes without its proof changing too, the check fails.

What it can’t do

This proves the design, and not the C# code, so the code can still get the design wrong. The plan there is for the spec to write out test cases (registries, patch sequences, join attempts) for the engine’s own tests to replay, once there’s a records store to test against.

It can’t check anything about one game’s files either, like whether a converter reads a model correctly, which stays in regular tests over real installs. It also can’t catch problems that aren’t logic, like a missing scope or a legal question, so I still read everything myself.