C*: Unifying Program and Proof in C

Proof-Spec-Impl Capsules

EN | 中文

A verified library should be usable like an ordinary library: the client includes a header, calls a function, and continues. This section explains how C* supports this style of use. The idea is to keep three artifacts together: a C implementation fragment, the specification under which clients use it, and the proof that the implementation satisfies the specification. Together, they form a contracted function called a proof-spec-impl capsule (PSI capsule, or Ψ-capsule for short). Once a capsule is verified, its contract guarantees the safety of calls, and the proof inside it need not be repeated at call sites.

The Cost of Repeating a Proof

Consider the list-reversal loop from the forward-proof section. Its body executes four ordinary C statements, two of which access memory that the symbolic state describes only through the abstract predicate sllsll. Before reading or writing v->tailv->tail, we must expose the node at vv; after the write, we must restore the invariant:

// 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));
}

This pattern recurs at every program point that accesses 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

Writing these steps inline 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 contain ten copies of essentially the same proof code. When the predicate’s definition changes, all ten need maintenance.

Abstraction leak. The client’s proof must refer to field_addrfield_addr, data_atdata_at, and the predicate’s internal existentials. The predicate lets clients reason about “a list holding ll”, but inlining the unfold–refold steps requires every client to reason about the representation as well.

The operational machinery already packages reusable proof steps: an unfold like the one above can be declared once as an operation and applied elsewhere. A PSI capsule packages the C code together with these proof steps, so the call site contains no proof code.

Anatomy of a Capsule

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 the abstraction 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 #require of the definitions module its contracts mention
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 #require of the definitions module its contracts mention
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
Artifact Where it lives Who consumes it
Specification the shared *_SPEC*_SPEC contract macro clients, at every call site
Implementation the bare C statements in the body the compiled program
Proof the [[cst::proof]][[cst::proof]] blocks around them the verifier, once

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. A header may itself #require#require the modules its contracts depend on; such dependencies are transitive and deduplicated, so a client names only the unit. 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 abstracts over data_atdata_at; more complex developments can add further layers of predicates. 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.

First Capsules: Array Cell Access

The first pair of capsules wraps a single array subscript access 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 states that pp points to a byte array whose contents are the logical list xsxs; the array’s extent is the length of that list. The standard library provides integer-indexed list 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. The contracts below use the same operators.

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;

(In a macro, a backtick quotation must fit on a single macro line, so even long require clauses cannot wrap.)

The require clause states that the caller owns the array, that nn is its length, and that ii is in bounds. These are the three facts needed for a safe access. Stated once, they serve both as the interface and as the premises of the internal safety argument.

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 and justified by a proved lemma. Its schema illustrates how the operational style from the previous sections applies here:

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, which describes the rest of the array with cell ii split out. We can follow these steps through the symbolic states in the body. After the open:

The bare statement buf[i] = ch;buf[i] = ch; now writes to a data_atdata_at cell, so the symbolic-execution engine handles it without proof code:

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, expressing the cell update as a list update:

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

The read capsule. A proof block placed after returnreturn has no symbolic state to transform, so a value-returning capsule first reads into a local 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 proof sandwich still applies, with two bare statements instead of one. The close steps for reads and writes use different pure lemmas: after a read, the cell still holds inth i xsinth i xs, so folding requires the fact that replace_inth i (inth i xs) xsreplace_inth i (inth i xs) xs equals xsxs. This is one of several small list lemmas that the unit proves once, alongside 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 "psi_examples/units/char_array_unit.h"
#require "psi_examples/units/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 "psi_examples/units/char_array_unit.h"
#require "psi_examples/units/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;
}

Composing the two calls requires the client to prove only list properties: 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 these obligations in a few lines each, using lemmas exported by the unit. The client needs no heap reasoning involving data_atdata_at, holes, or folding. That reasoning has already been checked inside the capsule.

A Capsule Suite for Linked Lists

Both array capsules keep the same abstract view in their preconditions and postconditions. The linked-list unit below publishes four accessors over the familiar sllsll predicate, each illustrating a different contract design.

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;

All four use 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. Because every capsule’s precondition describes 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. It produces fact(~(p == 0i))fact(~(p == 0i)), which the fold operation later consumes. Thus, the unfold establishes the premise needed for the fold.

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 accesses a data_atdata_at cell, and the fold restores sll p__pre (h :: t)sll p__pre (h :: t). The client retains the same list and gains the fact that the returned value is its head. write_headwrite_head uses the same proof 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? In the definition of sllsll, the tail pointer is existentially bound, so the caller has no name for it. This interface gives the caller separate ownership of the tail. Retaining sll p (h :: t)sll p (h :: t) alongside that ownership would describe the tail resource twice; holding the tail pointer as a value alone does not duplicate ownership. The postcondition gives 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 unfolds the list and performs one bare read, without folding it back: the postcondition deliberately exposes the lower layer. A client that calls read_tailread_tail must then carry the exposed-node view in its own contract or fold it back itself. The choice of postcondition layer determines how the client can use the result; this interface gives the client access to the lower layer.

Accounting for every resource: write_tailwrite_tail. The last capsule illustrates how a contract accounts for detached resources. Redirecting p->tailp->tail to a second list takes one pointer store, but detaches the old tail, whose ownership must still be accounted for in separation logic. The contract returns ownership of the old tail to the caller and uses the return value to identify it.

#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 contains both the redirected node and the detached old tail:

The fold consumes the two node cells together with sll new_tail__pre t2sll new_tail__pre t2; the tail cell’s current value determines which list is folded in. This leaves sll p__pre (h :: t2)sll p__pre (h :: t2) and the separate resource sll q0 tsll q0 t for the returnreturn:

The four accessors, side by side:

Capsule Contract layer (pre ->-> post) What the client learns or owns
read_headread_head sllsll ->-> sllsll the head value, as a fact
write_headwrite_head sllsll ->-> sllsll the same list with a new head
read_tailread_tail sllsll ->-> exposed node the tail pointer and the exposed node view
write_tailwrite_tail sll ** sllsll ** sll ->-> sll ** sllsll ** sll the list with its new tail, plus ownership of the old tail

A client uses this suite through ordinary C calls. The tail-swapping wrapper below verifies without proof code: the engine unifies the ghost parameters hh, tt, t2t2 with the caller’s resources and matches the postcondition automatically:

#include "psi_examples/units/sll_unit.h"
#require "psi_examples/units/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 "psi_examples/units/sll_unit.h"
#require "psi_examples/units/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;
}

Proven, Not Trusted

Packaging unsafe internals behind a safe interface is an established practice in Rust’s standard library and ecosystem. Comparing this practice with capsules clarifies the additional guarantee a capsule provides.

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 {}

Safe client code cannot break the invariant, so the module boundary serves as a safety boundary. The guarantee at that boundary depends on the implementation inside it. The /// # Safety/// # Safety comment records the argument in prose, and the compiler accepts the unsafe implunsafe impl without checking that argument. A mistake in the argument invalidates the guarantees that every safe client relies on.

A PSI capsule follows the same interface discipline, with calls safe by contract, and also verifies the implementation inside the capsule. The proof blocks in the capsule body are checked step by step, down to the HOL Light kernel. When the unit passes verification, a machine-checked theorem establishes that the bare statement, executed from any state satisfying the precondition, reestablishes the postcondition, including the invariants and refolding.

Safe abstraction over unsafeunsafe (Rust) PSI capsule (C*)
Safety property stated in /// # Safety/// # Safety prose comments the contract macro, machine-readable
Internal correctness audited by humans, then trusted proven; kernel-checked
A mistake inside means undefined behavior in a client verification fails at the capsule
Client obligation type-check against the safe API symbolic state matches the precondition

When a Capsule Fails to Apply

A capsule call is verified like any contracted call: the engine matches the current symbolic state against the precondition. When the match fails, the error quotes the statement with a ▸▸ marker, gives its position in the caller, and prints the symbolic state at that point. Most call-site failures fall into the following cases, which can be identified from the error message:

Symptom First check
the spatial resource is not found Is the state at the capsule’s layer? Bring a folded view (or one already unfolded past that layer) to the contract’s layer, or choose a capsule at the current layer.
a pure precondition is not discharged Does the branch contain the needed fact(...)fact(...), such as a bounds fact or a non-null fact, as an explicit conjunct? Establish it before the call.
postcondition existentials do not close The engine instantiates witnesses by matching data_atdata_at; a remaining obligation usually refers to the witness in a syntactic form that needs one rewrite.
the verifier reports a leaked resource The call dropped memory that the contract gives the caller ownership of, such as an old tail or a detached node. Consume or return the resource; separation logic does not allow it to be discarded.

The repeated unfold–refold proofs discussed at the start of this section no longer occur at call sites, eliminating errors introduced in individual copies. The proof is checked once, inside the capsule.

Summary

  • 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 use #include#include + #require#require to import capsules and call them as plain C; the unfold–refold reasoning is checked once, inside the capsule.
  • 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 and replaces trusted prose with a kernel-checked proof. The engine and the specifications of the outside world remain in the trusted base.