Proving an Authorization Table with Bend

Intro

Every web app has a small table that decides who can do what. Mine is a Rust function, role_route, in Homie. It answers whether a session with a read-only role, such as a visitor of the public demo, can use a route. It is about twenty lines, and it guards the only public door into the app. Unit tests check the cases someone thought of. I wanted a check of the cases nobody thought of too.

So I wrote the table again in Bend. I stated what must always hold as laws (statements the checker must prove for every input). Then I let the Bend checker prove them.

TL;DR: Bend 2 combines Lean-style proofs with fast parallel code. I modelled role_route in about 110 lines and stated five laws. A role never reaches an action route or an unknown route. The GitHub picker needs per-session watches and the workflows page. Only GET, HEAD and POST get through. bend PROOF.bend prints ALL PROOFS CHECK. --verdict rechecks with a kernel that is itself proven in Lean. Bend proves the model, not the Rust. So an exhaustive Rust test checks the real function against the model on all 480 combinations. CI runs both, with Bend and Lean pinned by sha256.

The Figure

The board is role_route. It has one row per route and one column per method. A brass pin stands where a role can pass. The three knurled knobs on the right are the inputs (the logs page, the workflows page, the per-session GitHub store). Their push rods raise and lower the pins they govern. Each comb is one law, with teeth exactly over the cells that the law says must stay empty. Four combs ride the gantry. The crosswise comb on the front rail sweeps the PUT and DELETE columns. A comb that crosses the board without touching a pin is a proof. Press B, and a forbidden pin rises in the action row. The first comb stops dead on it, and the readout says SOME PROOFS FAIL. That is exactly what the checker refuses. Click for the next law, and press 1 to 3 to turn the knobs. I built the figure with the anatomy skill.

The Situation

• Bend 2.0.38 (bend-lang.com), installed in ~/.bend. bend guide prints the whole language guide.
• Lean 4.34.0, only for bend PROOF.bend --verdict.
• The code under proof: role_route(role, method, path, github_session) in the Homie request guard. A role (RFC 0016) can read the meta, query and stream routes, and it can log out. It can search logs only with the logs page. It can use the GitHub picker only in session mode with the workflows page (RFC 0017). Everything else answers 403.

Law-Driven Development

The Bend convention splits the work between a human and an AI:

• LAWS.bend states the laws. The human writes it, and the AI does not touch it. A law with no proof is an open claim.
• PROOF.bend imports the laws and proves each with a def of the same name. The AI writes it, along with the code.
• bend PROOF.bend is the gate. It prints SOME PROOFS FAIL while any law is open or false, and ALL PROOFS CHECK when every law holds.

A law reads like the sentence it replaces:

# LAW: a role never reaches an action route (power, reconcile, refresh), with
# any method, any role and either GitHub store.
law no_actions:
  for role: R.Role
  for m: R.Method
  for ghs: Bool
  {R.role_route(role, m, R.Act{}, ghs) == False{} : Bool}

There are no tactics (the proof scripts of Lean). A proposition is a type, and a proof is a value of it. When both sides of an equality compute to the same term, {==} proves it:

# PROOF: role_route answers False for Act before it looks at anything else.
def Laws.no_actions(role, m, ghs):
  {==}

I prove the other laws by case analysis. The proof matches on the route (and, where it matters, the method or the store). Every case computes down to {==}.

The Model

The model is the Rust function, with paths classified into twelve routes and methods into four. The model checks the method first on every route, exactly as the Rust does:

def role_route(role: Role, m: Method, r: Route, ghs: Bool) -> Bool:
  match r:
    case Meta{}:
      is_read(m)
    case Logs{}:
      Bool.and(is_post(m), Role.logs(role))
    case GhWatch{}:
      Bool.and(is_post(m), picker(role, ghs))
    case Act{}:
      False{}
    # ... one case per route

What It Guards in Homie

Before, the rules lived in a twenty-line match and in tests that listed cases by hand. Now each rule is a law that holds for every role, method and store, or the build fails:

The second row is the easy one to miss. Someone can add a route to the Rust code and forget the role check. Then the model, the laws and the Rust test disagree, and CI fails before the route ships. The third row matters because of how the GitHub picker changed. It opened to roles for the per-session watches of the demo. The law pins that opening to exactly that mode.

Issue 1: The Checker Refused My Match

Symptom

'role' can't be matched in this position (it is matched after a local
statement or after a match on a later binder, ...)

Cause

Bend matches parameters in the order they are bound, for termination and soundness. My proof matched the route (the second parameter) and then the role (the first).

Fix

Put the parameter you split on first in the for list of the law. The law means the same. The proof becomes a straight case analysis.

Issue 2: Proofs That Did Not Compute

Symptom

Several cases stayed stuck instead of reducing to {==}.

Cause

Bool.and(a, b) only computes when a is known. My model put the role check first (Bool.and(Role.logs(role), is_post(m))). So a proof about methods got stuck on an unknown role.

Fix

Check the method first, which is also what the Rust does. The laws about methods then reduce at once. The model also got closer to the Rust.

Issue 3: Bend Proves the Model, Not the Rust

Symptom

Nothing broke, and that was the problem. A perfect proof about a model that drifted from the code proves nothing.

Cause

Bend checks Bend code. The function that runs in production is Rust.

Fix

A Rust test, role_routes_match_spec, runs the real role_route over every route path, five methods and every combination of the three inputs (480 cases). It compares each result against a direct transcription of the model. If you change one without the other, a test fails.

CI Without a Piped Installer

The official install is curl ... | sh. CI instead downloads the same release tarballs that the installer uses, pinned by version and sha256 (the installer script carries the same checksums). It caches Lean (580 MB) and the built kernel:

- run: bend PROOF.bend
- run: bend PROOF.bend --verdict

The job runs only when a .bend file, the model or the guarded Rust file changes. The first run took about a minute.

Limits

• The laws are only as good as their wording. The checker proves a law that says the wrong thing just as happily. That is why the human owns LAWS.bend.
• The proof covers the decision, not its wiring. The Rust test covers how a path maps to a route. Bend does not.
• --verdict needs Lean. Without it, you trust Bend’s own checker.

Lessons

1. Prove the smallest thing that guards the most. Twenty lines of routing decide whether a stranger can power off a VM.
2. Write the law as the sentence you write anyway. Then the checker reads it too.
3. Shape the model like the code. The proofs got simpler when the model matched the order of checks in the Rust.
4. Tie the model to the code with a test, or the proof drifts away from what runs.

References

• Bend
• GitHub: bendlang/bend
• GitHub: homie spec/roles.bend, LAWS.bend and PROOF.bend
• GitHub: homie RFC 0016, roles and a public demo
• GitHub: homie RFC 0017, personal GitHub watches per session
• Lean 4
• GitHub: wheresryan22/anatomy