Programs that talk to the world

How the Program core describes programs that issue commands, states the protocols they follow, and proves clients and handlers separately.

A program that opens a file, sends a request or reads a clock depends on something outside itself. Lema describes such a program as a value: a tree of the commands it may issue and the replies it may get back. The definitions are in lean/core/CoreV2.lean, the Program core (Core v2).

A capability application is built from these values. A trusted runner performs their commands, and application code never calls an extern (How programs reach the outside world). The code below is copied from the repository. The theorems of CoreV2.lean, and the ConnectionV2.lean example, were accepted by the pinned Lean 4.34.1 kernel through the API (crates/lema-cli/tests/core_v2.rs). The Program core reference lists the rest.

Programs as trees of commands and replies

inductive Prog (C : Type) (R : C → Type) (A : Type) : Type where
  | ret : A → Prog C R A
  | call : (c : C) → (R c → Prog C R A) → Prog C R A

C is the type of commands. R c is the type of the reply to command c, so different commands can have different kinds of reply. A is the program’s result. ret a finishes with a. call c k issues c, and when a reply r arrives it continues as k r. The continuation sees the reply before it chooses the next command. Here is a program from the same file that opens two handles and closes both:

def twoHandles : Prog HandleOp (fun _ => Nat) Unit :=
  .call .open fun a =>
    .call .open fun b =>
      .call (.close a) fun _ =>
        .call (.close b) fun _ => .ret ()

A program is a data structure, so a theorem about it can range over every branch, and so over every reply the outside world could send.

Contracts, implementations and the two sides

A contract works over an abstract protocol state S. It says when a command may run, how the state moves, and what the reply promises:

structure Contract (C : Type) (R : C → Type) (S : Type) where
  pre : S → C → Prop
  next : (s : S) → (c : C) → R c → S
  post : S → (c : C) → R c → Prop

The smallest contract in the repository is the counter in lean/core/ReplaceV2.lean. It is written against the Contract of Core v2, received by ID:

/-- A counter: each tick replies with the count so far. -/
def counter : Received.Contract Unit (fun _ => Nat) Nat :=
  Received.mkContract (fun _ _ => True) (fun s _ _ => s + 1) (fun s _ r => r = s)

There is one command, a tick (Unit), and its reply is a Nat. Every tick is allowed (pre is True), each tick adds one to the state (next), and the reply promises the count so far (post). next takes the reply as well as the command, so a contract can also model operations that may fail. For example, whether a connection is open afterwards can depend on what open answered. In the handles contract of CoreV2.lean, the state says which handle numbers are open. close h requires h to be open, and post promises that open returns a handle that was not open.

An implementation is a total model with private state M, which the contract never sees:

/-- Total mathematical operation model, not a claim about blocking OS I/O. -/
structure Impl (C : Type) (R : C → Type) (M : Type) where
  step : M → (c : C) → R c × M

Two propositions connect a contract to the code on either side of it. Safe is the client side: a program follows the contract and ends in a state and result that satisfy Q.

def Safe {C : Type} {R : C → Type} {S A : Type}
    (K : Contract C R S) (Q : S → A → Prop) : Prog C R A → S → Prop :=
  Prog.rec (fun a s => Q s a)
    (fun c _ ih s => K.pre s c ∧ ∀ r, K.post s c r → ih r (K.next s c r))

In words, ret a is safe when Q s a holds. call c k is safe when c is allowed now and, for every reply that keeps the promise, the rest of the program is safe from the next state. twoHandles_safe proves twoHandles safe on handles, ending with every handle closed. Without the promise it is provably unsafe (twoHandles_unsafe_unpromised), because the second open could return the first handle. A program can also be well typed and still break the protocol. forbidden in lean/core/ConnectionV2.lean receives before it opens, and forbidden_not_safe proves it unsafe.

Implements is the handler side. From states related by an invariant Inv, every allowed command gets a reply that keeps the promise and keeps the invariant.

def Implements {C : Type} {R : C → Type} {S M : Type}
    (K : Contract C R S) (h : Impl C R M) (Inv : S → M → Prop) : Prop :=
  ∀ s m c, Inv s m → K.pre s c →
    K.post s c (h.step m c).1 ∧ Inv (K.next s c (h.step m c).1) (h.step m c).2

CoreV2.lean also has an implementation named counter, unrelated to the contract above. It hands out handles from a running count, and counter_implements proves Implements handles counter Unused.

Joining the two sides

theorem sound {C : Type} {R : C → Type} {S M A : Type}
    (K : Contract C R S) (h : Impl C R M) (Inv : S → M → Prop)
    (law : Implements K h Inv) (Q : S → A → Prop) (p : Prog C R A) :
    ∀ s m, Safe K Q p s → Inv s m →
      Allowed K s (trace h p m) ∧
      Inv (after K s (trace h p m)) (run h p m).2 ∧
      Q (after K s (trace h p m)) (run h p m).1

Take a client proved safe against a contract, and run it on an implementation proved to implement the same contract. The run produces a trace the contract allows, keeps the invariant, and returns a result that satisfies the client’s postcondition. The two proofs never mention each other. They meet only at the contract. twoHandles_runs is this theorem applied to twoHandles_safe and counter_implements.

On its own, Safe is relative to the promise. A contract whose promise no reply keeps makes every program safe. Safe says something about actual runs only through sound and replacement, whose premises require an implementation that keeps the promise.

Replacing an implementation

def Simulates {C : Type} {R : C → Type} {S M N : Type}
    (K : Contract C R S) (first : Impl C R M) (second : Impl C R N)
    (Rel : S → M → N → Prop) : Prop :=
  ∀ s m n c, Rel s m n → K.pre s c →
    ∃ r m' n', first.step m c = (r, m') ∧ second.step n c = (r, n') ∧
      K.post s c r ∧ Rel (K.next s c r) m' n'

theorem replacement {C : Type} {R : C → Type} {S M N A : Type}
    (K : Contract C R S) (first : Impl C R M) (second : Impl C R N)
    (Rel : S → M → N → Prop) (law : Simulates K first second Rel)
    (Q : S → A → Prop) (p : Prog C R A) :
    ∀ s m n, Safe K Q p s → Rel s m n →
      (run first p m).1 = (run second p n).1 ∧
      trace first p m = trace second p n ∧
      Rel (after K s (trace first p m)) (run first p m).2 (run second p n).2

Simulates asks the two implementations to agree only on commands the contract allows. Their private states can have different types (M and N). replacement then gives every safe program the same result and the same trace on both. Simulates has no start states, so a relation that never holds proves it vacuously. Replaces in lean/core/Replaces.lean adds related start states, and that is the claim the store’s replace method reads.

For the counter contract above, ReplaceV2.lean has two implementations. plain keeps the count, and offset keeps the count plus five. shifted_steps proves Simulates counter plain offset Shifted, where Shifted s m n is m = s ∧ n = s + 5. plain_offset proves Replaces 0 0 5 counter plain offset Shifted. So every client that is safe on counter from count 0 gets the same result from plain started at 0 as from offset started at 5. Contracts, implementations and proofs shows the code.

Composing and layering

def bind {C : Type} {R : C → Type} {A B : Type}
    (p : Prog C R A) (f : A → Prog C R B) : Prog C R B :=
  match p with
  | .ret a => f a
  | .call c k => Prog.call c (fun r => bind (k r) f)

def interp {C D : Type} {R : C → Type} {E : D → Type} {A : Type}
    (module : (d : D) → Prog C R (E d)) (p : Prog D E A) : Prog C R A :=
  match p with
  | .ret a => Prog.ret a
  | .call d k => bind (module d) (fun r => interp module (k r))

bind runs one program and feeds its result to the next. safe_bind reduces the safety of the pair to the safety of the first program, with the second’s safety as its postcondition:

theorem safe_bind {C : Type} {R : C → Type} {S A B : Type}
    (K : Contract C R S) (Q : S → B → Prop)
    (p : Prog C R A) (f : A → Prog C R B) :
    ∀ s, Safe K Q (bind p f) s ↔
      Safe K (fun t a => Safe K Q (f a) t) p s

interp is for layers. It replaces each high-level command d with a program over lower-level commands, module d. safe_interp takes a relation between the high-level and low-level states. Suppose that, from related states, each allowed module d is safe on the low-level contract, keeps the high-level promise and leaves the states related. Then every program that is safe on the high-level contract becomes, after interp, a program that is safe on the low-level one, with its postcondition read through the relation. A proof about the upper layer and a proof about each translated command are enough. Nobody has to prove the combined program from scratch.

Unindexed programs, separate proofs

Some systems put the protocol into the program’s type, so that a program that receives before it opens does not type-check. Lema does not, and the reason comes from content addressing. A program’s type is its statement, and the statement’s ID is part of the program’s identity. If the protocol were in the type, tightening the protocol or proving a second property would change the program’s type, its ID, and the ID of everything that cites it. With Prog unindexed and Safe a separate proposition, the program keeps its ID, and any number of contracts and proofs can be attached to it later (lean/core/rules.md). There is also a present limit: the exporter accepts inductive families with parameters only, and refuses indexed ones.

The design has costs:

• A program that breaks its protocol is still well typed, as forbidden shows. The check is a separate proof that someone has to write.
• Prog is inductive, so every path through a program is finite, and proofs go by structural induction. (With infinitely many possible replies there may be no single bound on path length.) A server that runs forever is not one program. Repeating is the job of whatever runs it.
• A continuation is a function, so one step can hide any amount of pure work. lean/core/Fueled.lean adds fueled programs, whose work between commands has a bound read off the program. That bound is checked locally only; its store acceptance test has not been run.
• run and trace are checked mathematical semantics. That real I/O behaves like the model is tested at the runner’s boundary, or assumed (the OS and the network).

Prior work

The pieces are not new. Commands with dependent reply types are Hancock and Setzer’s interaction systems (“Interactive programs in dependent type theory”, 2000). Prog is the free monad over the container that C and R form (Abbott, Altenkirch and Ghani, “Containers”, 2005), with ret as its unit and bind as its bind. Keeping operations as syntax and giving them meaning separately, as interp and run do, is the idea of effect handlers (Plotkin and Pretnar, “Handlers of algebraic effects”, 2009). Interaction trees (Xia et al., POPL 2020) use the same shape coinductively and add silent steps, so they can describe programs that never stop. Prog is the inductive, terminating case. Safe is a weakest-precondition transformer in Dijkstra’s sense, and safe_bind is the rule for sequential composition. Where the ideas come from traces these and the sources of Implements and Simulates.