Refinement Types and Proof-Carrying Programs

Definition 10.1 — Source calculus, bind composition, and reduction¶

Every intermediate computation is named by a let, and every computation operand is already an atom—a variable or value. Consequently a closed nonfinal term has at most one active redex, at its outer let or conditional. Integer literals range over all of $\mathbb{Z}$, array literals contain integers, and every function value carries its full arrow annotation. Here $k$ is a literal constant, so $a+k$ is the only arithmetic primitive. This restriction matters: the exact relation $z=x+k$ is expressible by two difference constraints, whereas $z=x+y$ is not. Each test $\delta$ is one difference constraint, so taking a branch adds a predicate in the same logic. The term $\mathsf{error}$ is a checked failure, not a value. The conditional scrutinee $\delta$ is a logical difference atom, not a Boolean-valued term. At runtime all its vertices have integer values, and the truth value of the resulting inequality selects the branch.

This is the standard difference-logic fragment: formulas built from conjunctions of inequalities $x-y\le k$. Allowing arbitrary addition such as $z=x+y$ would leave this fragment for Presburger arithmetic, which is still decidable but requires a substantially heavier procedure. Allowing products of variables leaves difference logic and would require a different arithmetic theory and certificate format; no decision claim for that extension is made here. The narrow fragment is intentional: it lets us state and prove the complete certificate checker rather than trust an opaque solver.

Definition 22.2 — Bind composition¶

Function application is a computation and must therefore occur on the right-hand side of a let. To reduce such an application without leaving the A-normal grammar, define bind composition $e_1{▹}_x{e}_2$ by recursion on $e_1$: Bound variables are renamed before the second clause when necessary. Bind composition substitutes an A-normal computation into its continuation while preserving the A-normal grammar.

Definition 22.3 — Reduction¶

Reduction is defined on closed terms. Closed atoms are values. For a literal array $A$ with entries $n_0,\dots ,n_{m-1}$, the rules are as follows.

Term substitution acts inside $\delta$ using the normalizing predicate substitution of definition 10.3. After closing substitution, every integer variable and array-length vertex has therefore become an integer literal, and a test normalizes to a comparison between integer constants. Exactly one of E-IfT and E-IfF applies. There is deliberately no rule for an out-of-bounds $\mathsf{get}$. Such a term is stuck, and ruling it out will be the safety theorem rather than a convention inside evaluation.

Definition 10.3 — Difference predicates, refinement types, and substitution¶

Write $L_a$ as an abbreviation for the measure $\mathsf{len}(a)$; it is not a new program variable. In a scope, the vertices available to predicates are $$r::=\mathbf{0}\mid x\mid L_a,$$ where $x$ and $a$ range over raw term-variable names and $\mathbf{0}$ denotes the integer zero. Grammar alone does not assign a shape to those names: definition 10.4 admits $x$ only for an integer-shaped declaration and $L_a$ only for an array-shaped declaration. A difference atom and a predicate are $$\delta ::=r_1-r_2\le k,p::=\mathsf{true}\mid \delta \wedge p.$$ Thus predicates are finite conjunctions only. We use the derived writings for $r_1-r_2\le -1$, $r_1\le r_2$ for $r_1-r_2\le 0$, and $r_1=r_2$ for the conjunction $r_1-r_2\le 0\wedge r_2-r_1\le 0$. Negating one atom stays in the language because integers are discrete: $$\overline{r_1-r_2\le k}:=r_2-r_1\le -k-1.$$ There is no disjunction, multiplication, sum of two vertices, array equality, or arbitrary quantifier-free linear arithmetic.

For a base-type binder $\nu$, its observable vertex is ${\mu }_{\mathsf{int}}(\nu )=\nu$ and ${\mu }_{\mathsf{arr}}(\nu )=L_{\nu }$. Types are $$t::=\{\nu :B\mid p\}\mid x:s\to t.$$ A refinement type $\{\nu :B\mid p\}$ restricts the values of base type $B$ to those whose distinguished binder $\nu$ satisfies $p$. The binder $x$ of an arrow may occur in the codomain only through $x$ when $s$ has integer shape, or through $L_x$ when $s$ has array shape. A function-typed $x$ has no predicate vertex. We abbreviate $\{\nu :B\mid \mathsf{true}\}$ by $B$.

Literal substitution is normalized back into the grammar. Replacing an integer variable by $n$ replaces its vertex by $\mathbf{0}+n$; replacing $L_a$ by an array literal of length $m$ replaces it by $\mathbf{0}+m$; constants are moved to the right of $\le$. For instance, $$(x-L_a\le -1)[3/x,⟨4,5⟩/a]\text{normalizes to}\mathbf{0}-\mathbf{0}\le -2.$$ Substitution for function variables changes no predicate. Under these clauses, $t[a/x]$ is total and capture avoiding for every well-shaped atom $a$.

Definition 10.4 — Scopes, well-formed contexts, and types¶

A context is a list $\mathrm{\Gamma }::=\cdot \mid \mathrm{\Gamma },x:t\mid \mathrm{\Gamma },\delta$ with distinct term variables. Its vertex scope $V(\mathrm{\Gamma })$ contains $x$ for an integer-shaped entry, $L_x$ for an array-shaped entry, and no vertex for a function-shaped entry. If $p$ is a conjunction, $\mathrm{\Gamma },p$ abbreviates the context obtained by appending its atoms in order. The following rules define well-formedness; “$p$ over $W$” means that every vertex of $p$ belongs to $W\cup \{\mathbf{0}\}$. $\mathrm{\Gamma }{\vDash }_{\mathsf{all}}p$ means that every valuation satisfying the refinements and guards in $\mathrm{\Gamma }$ also satisfies $p$. By contrast, $\mathrm{\Gamma }⊢a\Rightarrow t$ is a syntactic typing judgment.

The shape $|t|$ is obtained by erasing predicates: $|\{\nu :B\mid p\}|=B$ and $|x:s\to t|=|s|\to |t|$.

Definition 10.5 — Context embedding and entailment¶

The predicate contributed by a base entry is obtained by replacing the distinguished vertex by the entry’s vertex: For arrays, $p[x/\nu ]$ replaces $L_{\nu }$ by $L_x$. We write $\rho \vDash \mathrm{\Gamma }$ when $\rho \vDash \lfloor \mathrm{\Gamma }\rfloor$, and $\mathrm{\Gamma }{\vDash }_{\mathsf{all}}p$ when every valuation of the variables of $\mathrm{\Gamma }$ that satisfies $\mathrm{\Gamma }$ also satisfies $p$. Array valuations are actual finite arrays, so $\mathbf{0}-L_a\le 0$ is valid for every array variable $a$. $\rho \vDash \mathrm{\Gamma }$ is a fact about one valuation; $\mathrm{\Gamma }{\vDash }_{\mathsf{all}}p$ quantifies over all such $\rho$.

Definition 10.6 — Constraint graph and replay certificates¶

For a context $\mathrm{\Gamma }$, form the weighted directed multigraph $G_{\mathrm{\Gamma }}$. Its vertices are $\mathbf{0}$ and the vertices in $V(\mathrm{\Gamma })$. Each hypothesis $r_1-r_2\le k$ contributes the edge $r_2\stackrel{k}{\to }{r}_1$: this includes every atom in every base-type entry of $\lfloor \mathrm{\Gamma }\rfloor$ and every explicit guard entry, not merely the latter. For every array vertex $L_a$, add the implicit length edge $L_a\stackrel{0}{\to }\mathbf{0}$, which expresses $0\le L_a$. Edges carry identifiers, so duplicate constraints remain distinguishable.

If $h$ assigns integers to vertices with $h(\mathbf{0})=0$, then it satisfies the graph when $$h(v)\le h(u)+k\text{for every edge }u\stackrel{k}{\to }v.$$ This is exactly satisfaction of the corresponding difference constraints. Because the length edges force $h(L_a)\ge 0$, every satisfying $h$ is realized by a program valuation: assign $h(x)$ to integer $x$ and choose, independently for each $a$, any integer array of length $h(L_a)$.

Definition 10.6 — Constraint graph and replay certificates¶

For a goal $r_1-r_2\le k$, a path certificate is a possibly empty list of edge identifiers forming a directed path from $r_2$ to $r_1$ whose integer weight sum is at most $k$. Thus the empty list certifies $r_1-r_1\le k$ when $0\le k$. A contradiction certificate is a nonempty cyclic list of edge identifiers in $G_{\mathrm{\Gamma }}$ whose weight sum is negative.

The checker re-reads every named edge from $G_{\mathrm{\Gamma }}$, checks adjacency and the required endpoints, adds weights as mathematical integers, and checks the final inequality. For a conjunctive goal it accepts either one contradiction certificate for the context or one path certificate for each conjunct. Parsing, edge lookup, adjacency, and unbounded integer addition are therefore part of the trusted checker.

Definition 10.11 — Declarative subtyping¶

Base refinement subtyping is implication. For arrows, a function of the subtype must handle every argument promised by the supertype, so the domain premise is ; codomains are compared under $x:t_1$. The printed glyph is shared with the structural subtyping relation of chapter 8, but this judgment is refinement subtyping under a logical context. No rule or law of the earlier relation is imported here.

All conclusion types must be well formed in their respective contexts. A function at the left arrow can be applied to every $s_1$, whereas a context using the right arrow checks its argument at $t_1$; hence S-Arrow requires . Because these are the only two subtyping rules, every derivation preserves outer shape: S-Base relates base refinements and S-Arrow relates arrows. Thus “same shape” means the outer constructor equality obtained by this rule inversion.

Definition 10.14 — Exact base types and declarative typing¶

Atoms synthesize singleton refinements. For an integer atom $a$ represented by $(r,k)$, the two constraints are $\nu -r\le k$ and $r-\nu \le -k$. Write ${\mathsf{rep}}_{\mathsf{I}}(a)=(r,k)$, where $(x,0)$ represents an integer variable $x$ and $(\mathbf{0},n)$ represents the literal $n$. For an array atom $a$, write ${\mathsf{rep}}_{\mathsf{L}}(a)=(r,k)$ for its length representative, where $(L_a,0)$ represents an array variable and $(\mathbf{0},m)$ represents an array literal of length $m$. Define The exact integer type of $n$ is $\mathsf{EqI}(\mathbf{0},n)$.

If $i$ has integer representative $(r_i,k_i)$ and $a$ has length representative $(r_a,k_a)$, define the bounds predicate $$\mathsf{Bnd}(a,i):=(\mathbf{0}-r_i\le k_i)\wedge (r_i-r_a\le k_a-k_i-1).$$ The first conjunct is $0\le i$ and the second is , after moving offsets to the right.

Typing is declarative but bidirectional. Atoms and computations synthesize; expressions check.

Rule D-Sub is the only subsumption rule, and it applies only when a synthesized atom meets an expected type. The side condition of D-Let prevents a local name from escaping in the result type. Dependency is nevertheless useful inside the body, where the exact type synthesized for the computation becomes a hypothesis.

Definition 10.15 — VC generation¶

${\mathsf{K}}_{\mathrm{\Gamma }}(e,t)$ either fails structurally or returns the finite sequents whose validity is equivalent to $\mathrm{\Gamma }⊢e\Leftarrow t$. Each emitted verification condition (VC) is a sequent $(\mathrm{\Gamma };p)$, discharged by checking $\mathrm{\Gamma }{\vDash }_{\mathsf{all}}p$. Define the partial finite translation $\mathsf{SubVC}(\mathrm{\Gamma };s,t)$ recursively. With $z$ fresh and arrow binders alpha-aligned, its successful clauses are The translation fails on a shape mismatch, an ill-formed input type, or a failed recursive call. The first arrow call compares $t_1$ with $s_1$, which is the contravariant premise of S-Arrow.

The executable checker uses judgments $$\mathrm{\Gamma }⊢a\Rightarrow t\mid \mathcal{C},\mathrm{\Gamma }⊢c{\Rightarrow }_{c}t\mid \mathcal{C},\mathrm{\Gamma }⊢e\Leftarrow t\mid \mathcal{C}.$$ The function ${\mathsf{A}}_{\mathrm{\Gamma }}(a)$ returns an atom type and a VC list; ${\mathsf{Comp}}_{\mathrm{\Gamma }}(c)$ returns a computation type and a VC list; and ${\mathsf{K}}_{\mathrm{\Gamma }}(e,t)$ returns the VCs for checking $e$ against $t$. The get clause emits the two conjuncts of $\mathsf{Bnd}(a,i)$, and $\mathsf{SubVC}$ emits one implication at each base refinement. Write $\uplus$ for union of finite VC lists. A clause fails when its shape or well-formedness test fails. Put $${\mathcal{B}}_{\mathrm{\Gamma }}(a,i)=\{(\mathrm{\Gamma };\delta )\mid \delta \text{ is a conjunct of }\mathsf{Bnd}(a,i)\}.$$ The computation clauses are Abbreviate the conditional source expression by $e_{\delta }$. The checking clauses are where $e_{\delta }=\mathsf{if}\delta \mathsf{then}{e}_1\mathsf{else}{e}_2$. Every clause first checks its context and input types for well-formedness. Arithmetic occurs only in the sequents emitted by $\mathsf{SubVC}$ and the get clause.