Proving an Authorization Table with Bend

Intro

Every web app has a small table that decides who may 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, may 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 the cases nobody thought of checked too.

So I wrote the table again in Bend, stated what must always hold as laws, and let Bend’s checker prove them.

TL;DR: Bend 2 combines Lean-style proofs with fast parallel code. I modelled role_route in about 110 lines, 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), and 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: one row per route, one column per method, and a brass pin stands where a role may 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 the law says must stay empty: four ride the gantry, and 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, which is exactly what the checker refuses. Click for the next law, 1 to 3 turn the knobs. The figure was built 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 Homie’s request guard. A role (RFC 0016) may read the meta, query and stream routes, log out, search logs only with the logs page, and use the GitHub picker only in session mode with the workflows page (RFC 0017). Everything else answers 403.

Law-Driven Development

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

• LAWS.bend states the laws. The human writes it; 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: SOME PROOFS FAIL while any law is open or false, ALL PROOFS CHECK once 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. 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):
  {==}

The other laws are proven by case analysis: match on the route (and, where it matters, the method or the store), and every case computes down to {==}.

The Model

The model is the Rust function with paths classified into twelve routes and methods into four. The method is checked 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. After, each rule is a law that holds for every role, method and store, or the build says no:

The second row is the quiet one. When someone adds a route to the Rust code and forgets the role check, 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 evolved: it opened to roles for the demo’s per-session watches, and 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 law’s for list. The law means the same; the proof becomes a straight case analysis.

Issue 2: Proofs That Would 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, and the model got more faithful on the way.

Issue 3: Bend Proves the Model, Not the Rust

Symptom

Nothing broke, which was the problem: a perfect proof about a model that has 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) against a direct transcription of the model. Change one without the other and a test fails.

CI Without a Piped Installer

The official install is curl ... | sh. CI instead downloads the same release tarballs the installer would, pinned by version and sha256 (the installer script carries the same checksums), and 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. A law that says the wrong thing is proven just as happily; that is why the human owns LAWS.bend.
• The proof covers the decision, not its wiring: classifying a path into a route is covered by the Rust test, not by Bend.
• --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 would have written anyway. Then the checker reads it too.
3. Shape the model like the code. The proofs got simpler when the model matched the Rust’s order of checks.
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