Proof-Spec-Impl Capsules

A verified library should feel like a library: the client includes a header, calls a function, and moves on. This section shows how C* gets there. The idea is to package three artifacts that normally drift apart — a C implementation fragment, the specification clients use it at, and the proof that justifies one against the other — into a single contracted function, called a proof-spec-impl capsule (PSI capsule, or Ψ-capsule for short). Once a capsule is verified, any call to it is safe by contract, and the proof work it encapsulates is never repeated at a call site.

Consider once more the list-reversal loop from the forward-proof section. Its body executes four ordinary C statements — but two of them touch memory that the symbolic state describes only through the abstract predicate sllsll. Before v->tailv->tail may be read or written, the node at vv has to be exposed; after the write, the invariant has to be restored:

// v != 0, so l2 is a cons: unfold sll vv l2 into its head/tail cells.
[[cst::proof]] {
  thm ent = undisch_rule(
      spec_rule(`l2:(int)list`, spec_rule(`vv:addr`, sll_unfold)));
  cst_set_symbolic_state(
      local_apply(cst_get_symbolic_state(), ent));
}
struct list *t = v->tail;
v->tail = w;
w = v;
v = t;
// Re-establish the invariant: fold the node back onto the reversed prefix.
[[cst::proof]] {
  // ... a REVERSE/APPEND equation rev_eq is proved here first ...
  thm fold = undisch_rule(spec_rule(`wv:addr`,
      spec_rule(`REVERSE (l1:(int)list)`,
          spec_rule(`xv:int`, spec_rule(`vv:addr`, sll_fold)))));
  thm ent = rewrite_rule(THM_LIST(gsym_rule(rev_eq)), fold);
  cst_set_symbolic_state(
      local_apply(cst_get_symbolic_state(), ent));
}

// v != 0, so l2 is a cons: unfold sll vv l2 into its head/tail cells.
[[cst::proof]] {
  thm ent = undisch_rule(
      spec_rule(`l2:(int)list`, spec_rule(`vv:addr`, sll_unfold)));
  cst_set_symbolic_state(
      local_apply(cst_get_symbolic_state(), ent));
}
struct list *t = v->tail;
v->tail = w;
w = v;
v = t;
// Re-establish the invariant: fold the node back onto the reversed prefix.
[[cst::proof]] {
  // ... a REVERSE/APPEND equation rev_eq is proved here first ...
  thm fold = undisch_rule(spec_rule(`wv:addr`,
      spec_rule(`REVERSE (l1:(int)list)`,
          spec_rule(`xv:int`, spec_rule(`vv:addr`, sll_fold)))));
  thm ent = rewrite_rule(THM_LIST(gsym_rule(rev_eq)), fold);
  cst_set_symbolic_state(
      local_apply(cst_get_symbolic_state(), ent));
}

The pattern deserves a name because it recurs at every program point that touches an abstract data structure:

unfold the current view (sll, an array predicate, ...)
  -> expose the underlying data_at cells
  -> perform the one memory read or write
  -> restore any invariant the write disturbed
  -> fold the high-level view back up

unfold the current view (sll, an array predicate, ...)
  -> expose the underlying data_at cells
  -> perform the one memory read or write
  -> restore any invariant the write disturbed
  -> fold the high-level view back up

Written inline, this dance has two costs.

Proof duplication. The unfold–refold steps depend only on the shape of the predicate, not on the surrounding function. Ten functions that each write one tailtail field will carry ten copies of essentially the same proof code — and when the predicate’s definition changes, all ten need maintenance.

Abstraction leak. The client’s proof must speak about field_addrfield_addr, data_atdata_at, and the predicate’s internal existentials. The predicate was introduced precisely so that clients could reason at the level of “a list holding ll”; inlining the unfold–refold steps drags every client back down to the representation.

The operational machinery already packages the reusable steps — an unfold like the one above can be declared once, as an operation, and applied anywhere. A PSI capsule takes the remaining step: it packages the code together with its steps, so the call site contains no proof at all.

Concretely, a capsule is an ordinary contracted C function whose body is a proof sandwich: proof code that opens the abstraction, one (or a few) bare C statements, and proof code that folds it back. Its contract is written once, as a single macro shared by the declaration in the header and the definition in the source file:

unit.h :  #define FOO_SPEC                       // the one contract macro
            [[cst::param(...)]]                  //   = the safe interface
            [[cst::require(...)]]
            [[cst::ensure(...)]]
          ret foo(args) FOO_SPEC;                // declaration reuses the macro
          // plus the predicate exports clients need to state their own specs
unit.c :  ret foo(args) FOO_SPEC {               // definition reuses the same macro
            [[cst::proof]] { open_X(...); }      // proof: expose the underlying cells
            /* one real C read or write */       // implementation
            [[cst::proof]] { close_X(...); }     // proof: restore invariants, refold
          }
client :  #include "unit.h"
          #require "unit.c"
          ... foo(args) ...                      // a plain C call, no proof code

unit.h :  #define FOO_SPEC                       // the one contract macro
            [[cst::param(...)]]                  //   = the safe interface
            [[cst::require(...)]]
            [[cst::ensure(...)]]
          ret foo(args) FOO_SPEC;                // declaration reuses the macro
          // plus the predicate exports clients need to state their own specs
unit.c :  ret foo(args) FOO_SPEC {               // definition reuses the same macro
            [[cst::proof]] { open_X(...); }      // proof: expose the underlying cells
            /* one real C read or write */       // implementation
            [[cst::proof]] { close_X(...); }     // proof: restore invariants, refold
          }
client :  #include "unit.h"
          #require "unit.c"
          ... foo(args) ...                      // a plain C call, no proof code

Two further conventions matter in practice.

Clients wire capsules in with #include#include + #require#require. The header contributes the contracts and predicate declarations; #require#require tells the verifier where the (already verified) definitions live. After that, calling a capsule is symbolic execution against its contract — exactly like calling any contracted function.

Capsules live at a chosen layer of the predicate hierarchy. A predicate like sllsll sits above data_atdata_at; richer developments stack further layers on top. Each capsule fixes the layer of its contract, and the caller picks the capsule whose contract matches the current symbolic state, rather than manually unfolding down to the layer a lower-level interface would demand. The same underlying statement — one field write — can be exposed through different capsules at different layers.

The first pair of capsules wraps the smallest possible implementation — one array subscript — behind an abstract view of a byte buffer. The predicate is a monomorphic wrapper over the standard library’s array_atarray_at:

PROOF thm char_array_def = new_fun_definition(
    `char_array (p:addr) (xs:(int)list) : hprop =
       array_at p Tchar (ilength xs) xs`);

PROOF thm char_array_def = new_fun_definition(
    `char_array (p:addr) (xs:(int)list) : hprop =
       array_at p Tchar (ilength xs) xs`);

char_array p xschar_array p xs says that pp points to a byte array whose contents are the logical list xsxs; the array’s extent is the list’s own length. The standard library speaks about lists with integer-indexed operators — ilength xsilength xs for the length, inth i xsinth i xs for element ii, and replace_inth i v xsreplace_inth i v xs for the list with element ii replaced by vv — and the contracts below use the same vocabulary.

The unit publishes two capsules. Their contracts are the safe interface:

#define CHAR_ARRAY_READ_SPEC                                                  \
  [[cst::param(`xs:(int)list`)]]                                              \
  [[cst::require(`char_array buf xs ** fact(n == ilength xs) ** fact(0i <= i) ** fact(i < n)`)]] \
  [[cst::ensure(`char_array buf xs ** fact(__return == inth i xs)`)]]
#define CHAR_ARRAY_WRITE_SPEC                                                 \
  [[cst::param(`xs:(int)list`)]]                                              \
  [[cst::require(`char_array buf xs ** fact(n == ilength xs) ** fact(0i <= i) ** fact(i < n)`)]] \
  [[cst::ensure(`char_array buf (replace_inth i ch xs)`)]]
char char_array_read(char *buf, int n, int i) CHAR_ARRAY_READ_SPEC;
void char_array_write(char *buf, int n, int i, char ch) CHAR_ARRAY_WRITE_SPEC;

#define CHAR_ARRAY_READ_SPEC                                                  \
  [[cst::param(`xs:(int)list`)]]                                              \
  [[cst::require(`char_array buf xs ** fact(n == ilength xs) ** fact(0i <= i) ** fact(i < n)`)]] \
  [[cst::ensure(`char_array buf xs ** fact(__return == inth i xs)`)]]
#define CHAR_ARRAY_WRITE_SPEC                                                 \
  [[cst::param(`xs:(int)list`)]]                                              \
  [[cst::require(`char_array buf xs ** fact(n == ilength xs) ** fact(0i <= i) ** fact(i < n)`)]] \
  [[cst::ensure(`char_array buf (replace_inth i ch xs)`)]]
char char_array_read(char *buf, int n, int i) CHAR_ARRAY_READ_SPEC;
void char_array_write(char *buf, int n, int i, char ch) CHAR_ARRAY_WRITE_SPEC;

(One quirk of the macro form: a backtick quotation must sit on a single macro line, so require clauses run wide rather than wrap.)

Read the require clause as a sentence: the caller owns the array, promises that nn is its length, and promises that ii is in bounds. Notice that these are exactly the facts an in-bounds access needs — the safe interface and the internal safety argument are the same three facts, stated once.

The write capsule. Its definition expands the same CHAR_ARRAY_WRITE_SPECCHAR_ARRAY_WRITE_SPEC macro and wraps one bare store:

void char_array_write(char *buf, int n, int i, char ch) CHAR_ARRAY_WRITE_SPEC
{
  [[cst::proof]] { open_char_array(`buf__pre:addr`, `i__pre:int`); }
  buf[i] = ch;
  [[cst::proof]] { close_char_array_write(`buf__pre:addr`, `i__pre:int`); }
}

void char_array_write(char *buf, int n, int i, char ch) CHAR_ARRAY_WRITE_SPEC
{
  [[cst::proof]] { open_char_array(`buf__pre:addr`, `i__pre:int`); }
  buf[i] = ch;
  [[cst::proof]] { close_char_array_write(`buf__pre:addr`, `i__pre:int`); }
}

open_char_arrayopen_char_array is a packaged operation, declared once in the unit with a proved lemma behind it. Its schema is worth reading — it is the operational style doing exactly what the previous sections promised:

decl_operation(open_char_array_op,
  TERM_LIST(`p:addr`, `i:int`),
  TERM_LIST(`char_array (KEY (p:addr)) (CAPTURE (xs:(int)list))`),
  TERM_LIST(`0i <= (i:int)`, `i < ilength (xs:(int)list)`),
  `data_at (p + i * sizeof Tchar) Tchar (inth i xs) **
   char_array_hole p i xs`)

decl_operation(open_char_array_op,
  TERM_LIST(`p:addr`, `i:int`),
  TERM_LIST(`char_array (KEY (p:addr)) (CAPTURE (xs:(int)list))`),
  TERM_LIST(`0i <= (i:int)`, `i < ilength (xs:(int)list)`),
  `data_at (p + i * sizeof Tchar) Tchar (inth i xs) **
   char_array_hole p i xs`)

It consumes the char_arraychar_array resource at pp (capturing the current list xsxs), checks the two bounds facts, and produces cell ii as a bare data_atdata_at plus char_array_hole p i xschar_array_hole p i xs — the rest of the array, with cell ii split out. Watching the symbolic state across the body shows the whole story. After the open:

The bare statement buf[i] = ch;buf[i] = ch; is now an ordinary store into an ordinary data_atdata_at cell — the symbolic-execution engine handles it with no proof code at all:

Only the focused cell changed: inth i__pre xsinth i__pre xs became ch__prech__pre. Finally close_char_array_writeclose_char_array_write folds the hole and the updated cell back into a whole array, turning the pointwise store into a list update:

This final state matches the postcondition, and the capsule verifies with no VCs left over.

The read capsule. One wrinkle: a proof block placed after returnreturn has no symbolic state to transform, so a value-returning capsule reads into a local first and folds the array back before returning:

char char_array_read(char *buf, int n, int i) CHAR_ARRAY_READ_SPEC
{
  [[cst::proof]] { open_char_array(`buf__pre:addr`, `i__pre:int`); }
  char ch = buf[i];
  [[cst::proof]] { close_char_array_read(`buf__pre:addr`, `i__pre:int`); }
  return ch;
}

char char_array_read(char *buf, int n, int i) CHAR_ARRAY_READ_SPEC
{
  [[cst::proof]] { open_char_array(`buf__pre:addr`, `i__pre:int`); }
  char ch = buf[i];
  [[cst::proof]] { close_char_array_read(`buf__pre:addr`, `i__pre:int`); }
  return ch;
}

The sandwich is intact; the bare fragment is two statements instead of one. The close step for a read differs from the close for a write in the pure lemma it rests on: the cell still holds inth i xsinth i xs, so folding must recognize replace_inth i (inth i xs) xsreplace_inth i (inth i xs) xs as xsxs itself — one of a handful of small list lemmas the unit proves once, next to the operations that use them.

A client. With the unit verified, a client includes the header, requires the source, and calls the capsules as plain C:

#include "char_array_unit.h"
#require "char_array_unit.c"
char write_then_read(char *buf, int n, int i, char ch)
    [[cst::param(`xs:(int)list`)]]
    [[cst::require(`char_array buf xs ** fact(n == ilength xs)
                    ** fact(0i <= i) ** fact(i < n)`)]]
    [[cst::ensure(`char_array buf (replace_inth i ch xs)
                   ** fact(__return == ch)`)]]
{
  char_array_write(buf, n, i, ch);
  [[cst::proof]] { /* pure-fact glue: replace_inth preserves ilength */ }
  char got = char_array_read(buf, n, i);
  [[cst::proof]] { /* pure-fact glue: inth i (replace_inth i ch xs) == ch */ }
  return got;
}

#include "char_array_unit.h"
#require "char_array_unit.c"
char write_then_read(char *buf, int n, int i, char ch)
    [[cst::param(`xs:(int)list`)]]
    [[cst::require(`char_array buf xs ** fact(n == ilength xs)
                    ** fact(0i <= i) ** fact(i < n)`)]]
    [[cst::ensure(`char_array buf (replace_inth i ch xs)
                   ** fact(__return == ch)`)]]
{
  char_array_write(buf, n, i, ch);
  [[cst::proof]] { /* pure-fact glue: replace_inth preserves ilength */ }
  char got = char_array_read(buf, n, i);
  [[cst::proof]] { /* pure-fact glue: inth i (replace_inth i ch xs) == ch */ }
  return got;
}

Between the two calls the client’s proof obligation is purely about lists — that replace_inthreplace_inth preserves the length (so the read’s precondition holds for the updated list), and that reading index ii of the updated list yields chch. The two elided proof blocks discharge exactly those, in a few lines each, from lemmas the unit exports. What the client never touches is the heap: no data_atdata_at, no hole, no folding. That reasoning happened once, inside the capsule.

Arrays made a gentle start because both capsules could keep the same abstract view on both sides of the contract. Linked lists are where capsule design gets interesting: the unit below publishes four accessors over the familiar sllsll predicate, and each one forces a different design decision.

int          read_head (struct list *p) SLL_READ_HEAD_SPEC;
void         write_head(struct list *p, int x) SLL_WRITE_HEAD_SPEC;
struct list *read_tail (struct list *p) SLL_READ_TAIL_SPEC;
struct list *write_tail(struct list *p, struct list *new_tail) SLL_WRITE_TAIL_SPEC;

int          read_head (struct list *p) SLL_READ_HEAD_SPEC;
void         write_head(struct list *p, int x) SLL_WRITE_HEAD_SPEC;
struct list *read_tail (struct list *p) SLL_READ_TAIL_SPEC;
struct list *write_tail(struct list *p, struct list *new_tail) SLL_WRITE_TAIL_SPEC;

Behind all four sit just two operations, declared once in the unit: an unfold that opens a non-empty sllsll into its head cell, tail cell, and successor list, and a fold that reassembles them. One detail repays attention: because every capsule’s precondition names the list as a cons — sll p (h :: t)sll p (h :: t) — the unfold operation matches that shape by pattern and needs no separate non-nullness premise. Instead it produces fact(~(p == 0i))fact(~(p == 0i)), which is exactly the premise the fold operation consumes later. The two operations hand each other their obligations.

Staying at the layer: read_headread_head and write_headwrite_head. Both contracts keep sllsll on both sides:

#define SLL_READ_HEAD_SPEC                                                    \
  [[cst::param(`h:int`, `t:(int)list`)]]                                      \
  [[cst::require(`sll p (h :: t)`)]]                                          \
  [[cst::ensure(`sll p (h :: t) ** fact(__return == h)`)]]
int read_head(struct list *p) SLL_READ_HEAD_SPEC
{
  [[cst::proof]] { unfold_sll(`p__pre:addr`, `q0:addr`); }
  int v = p->head;
  [[cst::proof]] { fold_sll(`p__pre:addr`); }
  return v;
}

#define SLL_READ_HEAD_SPEC                                                    \
  [[cst::param(`h:int`, `t:(int)list`)]]                                      \
  [[cst::require(`sll p (h :: t)`)]]                                          \
  [[cst::ensure(`sll p (h :: t) ** fact(__return == h)`)]]
int read_head(struct list *p) SLL_READ_HEAD_SPEC
{
  [[cst::proof]] { unfold_sll(`p__pre:addr`, `q0:addr`); }
  int v = p->head;
  [[cst::proof]] { fold_sll(`p__pre:addr`); }
  return v;
}

The read then targets a plain data_atdata_at cell, and the fold restores sll p__pre (h :: t)sll p__pre (h :: t) — the client sees a list go in and the same list come out, plus the fact that the returned value is its head. write_headwrite_head is the same sandwich around p->head = x;p->head = x;, ensuring sll p (x :: t)sll p (x :: t).

Forced down a layer: read_tailread_tail. What should read_tailread_tail promise about its return value? Inside the definition of sllsll, the tail pointer lives under an existential — it has no name a caller could mention. Returning it makes it public, and that decision shows up in the contract: once the caller holds the tail pointer as a value, the node can no longer hide behind sll p (h :: t)sll p (h :: t), because the same resource would then be described twice. The honest postcondition hands the caller the exposed view, with __return__return serving as the witness:

#define SLL_READ_TAIL_SPEC                                                    \
  [[cst::param(`h:int`, `t:(int)list`)]]                                      \
  [[cst::require(`sll p (h :: t)`)]]                                          \
  [[cst::ensure(`data_at (field_addr p Tlist Fhead) Tint h ** data_at (field_addr p Tlist Ftail) Tptr __return ** sll __return t`)]]

#define SLL_READ_TAIL_SPEC                                                    \
  [[cst::param(`h:int`, `t:(int)list`)]]                                      \
  [[cst::require(`sll p (h :: t)`)]]                                          \
  [[cst::ensure(`data_at (field_addr p Tlist Fhead) Tint h ** data_at (field_addr p Tlist Ftail) Tptr __return ** sll __return t`)]]

The body is an unfold, one bare read, and — deliberately — no fold: the layer drop is the point. A client that calls read_tailread_tail must carry the exposed-node view in its own contract from then on (or fold it back itself). Choosing the layer of a capsule’s postcondition is the central design act here; publishing this one interface at the lower layer is what makes it useful.

Accounting for every resource: write_tailwrite_tail. The most instructive capsule is the last one. Redirecting p->tailp->tail to a second list is one pointer store — but it orphans the old tail, and separation logic will not let owned memory silently vanish. The contract must say where the old tail went, and the natural answer is: back to the caller, as the return value.

#define SLL_WRITE_TAIL_SPEC                                                   \
  [[cst::param(`h:int`, `t:(int)list`, `t2:(int)list`)]]                      \
  [[cst::require(`sll p (h :: t) ** sll new_tail t2`)]]                       \
  [[cst::ensure(`sll p (h :: t2) ** sll __return t`)]]
struct list *write_tail(struct list *p, struct list *new_tail) SLL_WRITE_TAIL_SPEC
{
  [[cst::proof]] { unfold_sll(`p__pre:addr`, `q0:addr`); }
  struct list *old_tail = p->tail;
  p->tail = new_tail;
  [[cst::proof]] { fold_sll(`p__pre:addr`); }
  return old_tail;
}

#define SLL_WRITE_TAIL_SPEC                                                   \
  [[cst::param(`h:int`, `t:(int)list`, `t2:(int)list`)]]                      \
  [[cst::require(`sll p (h :: t) ** sll new_tail t2`)]]                       \
  [[cst::ensure(`sll p (h :: t2) ** sll __return t`)]]
struct list *write_tail(struct list *p, struct list *new_tail) SLL_WRITE_TAIL_SPEC
{
  [[cst::proof]] { unfold_sll(`p__pre:addr`, `q0:addr`); }
  struct list *old_tail = p->tail;
  p->tail = new_tail;
  [[cst::proof]] { fold_sll(`p__pre:addr`); }
  return old_tail;
}

After the two bare statements, the state holds the redirected node and the detached old tail side by side:

The fold consumes the two node cells together with sll new_tail__pre t2sll new_tail__pre t2 — the tail cell’s current value decides which list gets folded in — leaving sll p__pre (h :: t2)sll p__pre (h :: t2) and, free-standing, sll q0 tsll q0 t for the returnreturn:

The four accessors, side by side:

A client of this suite reads like ordinary C. The tail-swapping wrapper below verifies with zero proof code — the engine unifies the ghost parameters hh, tt, t2t2 against the caller’s own resources and matches the postcondition by itself:

#include "sll_unit.h"
#require "sll_unit.c"
struct list *tail_swap(struct list *p, struct list *q)
    [[cst::param(`h:int`, `t:(int)list`, `t2:(int)list`)]]
    [[cst::require(`sll p (h :: t) ** sll q t2`)]]
    [[cst::ensure(`sll p (h :: t2) ** sll __return t`)]]
{
  struct list *old = write_tail(p, q);
  return old;
}

#include "sll_unit.h"
#require "sll_unit.c"
struct list *tail_swap(struct list *p, struct list *q)
    [[cst::param(`h:int`, `t:(int)list`, `t2:(int)list`)]]
    [[cst::require(`sll p (h :: t) ** sll q t2`)]]
    [[cst::ensure(`sll p (h :: t2) ** sll __return t`)]]
{
  struct list *old = write_tail(p, q);
  return old;
}

Packaging unsafe internals behind a safe interface is not a new idea; it is, notably, the discipline that Rust’s standard library and ecosystem are built on. The comparison is worth making carefully, because it locates exactly what a capsule adds.

A safe Rust abstraction follows a three-part pattern: define a type carrying an invariant the compiler cannot see; enforce the invariant by field privacy and by auditing every method that could disturb it; consume the invariant in code that is only correct because it holds. Where the internals must do something the compiler cannot check, the author writes unsafeunsafe, and documents the reasoning in prose:

/// # Safety
///
/// `MyHandle` owns its buffer exclusively, so it may be
/// transferred across threads.
unsafe impl Send for MyHandle {}

/// # Safety
///
/// `MyHandle` owns its buffer exclusively, so it may be
/// transferred across threads.
unsafe impl Send for MyHandle {}

From the outside, this works remarkably well: safe client code cannot break the invariant, and the module boundary becomes a safety boundary. But look at what stands behind the boundary. The /// # Safety/// # Safety comment is prose; the unsafe implunsafe impl is accepted by fiat. The compiler takes the author’s word for it, and a subtle mistake inside the module silently voids the guarantees of every safe client.

A PSI capsule offers the same interface discipline — any client call is safe by contract — with one addition: the inside of the box is itself proven. The proof blocks in the capsule body are not comments; they are checked, step by step, down to the HOL Light kernel. When the unit passes verification, there is a machine-checked theorem that the one bare statement, executed from any state satisfying the precondition, reestablishes the postcondition — invariants, refolding, and all.

A capsule call is verified like any contracted call: the engine matches the current symbolic state against the precondition. Most failures at a call site are one of a small number of shapes:

The failure mode that is conspicuously absent is the one the section began with: a hand-written unfold–refold going subtly wrong at one of its many copies. That proof exists in exactly one place — inside the capsule — and it has already been checked.

• A PSI capsule binds implementation, specification, and proof into one contracted C function; the three artifacts evolve together, and the contract macro shared by declaration and definition keeps interface and obligation identical.
• The body is a proof sandwich — open the abstraction, a bare statement or two, fold it back — built from the reusable operations of the operational style.
• Clients wire capsules in with #include#include + #require#require and call them as plain C; the unfold–refold reasoning happens once, inside the capsule, not at call sites.
• Capsules are published at a layer of the predicate hierarchy, and the caller picks the capsule matching the current symbolic state.
• Relative to safe-over-unsafeunsafe encapsulation, a capsule keeps the safe interface but replaces trusted prose with a kernel-checked proof — while remaining honest that the engine and the world-facing specifications stay in the trusted base.