Difference refinements and source proof-carrying code

The system of chapter 10 is a separate, nondependent calculus. Its base types, values, atoms, computations, and expressions are Here $k,n,n_i\in \mathbb{Z}$. Terms are A-normal by grammar. Bind composition, with capture-avoiding renaming before its let clause, is Reduction is on closed terms. For $A=⟨n_0,\dots ,n_{m-1}⟩$ its complete root table is

$q=n+k\text{ in }\mathbb{Z}$

$\mathsf{let}x=n+k\mathsf{in}e⟼e[q/x]$

$\mathsf{let}x=\mathsf{len}A\mathsf{in}e⟼e[m/x]$

$\mathsf{let}x=\mathsf{get}Ai\mathsf{in}e⟼e[n_i/x]$

$\mathsf{let}y=(\lambda x.e_1:x:s\to t)v\mathsf{in}{e}_2⟼e_1[v/x]{▹}_y{e}_2$

$F=(\mathsf{fix}f(x).e_1:x:s\to t)$

$\mathsf{let}y=Fv\mathsf{in}{e}_2⟼e_1[F/f,v/x]{▹}_y{e}_2$

$\delta \text{ is true}$

$\mathsf{if}\delta \mathsf{then}{e}_1\mathsf{else}{e}_2⟼e_1$

$\delta \text{ is false}$

$\mathsf{if}\delta \mathsf{then}{e}_1\mathsf{else}{e}_2⟼e_2$

There is no reduction root for an out-of-bounds get and no congruence relation: the grammar exposes the next computation at the head of a let.

Predicate vertices, atoms, conjunctions, and types are $L_a$ abbreviates $\mathsf{len}(a)$. An integer declaration contributes $x$ to the vertex scope, an array declaration contributes $L_x$, and a function declaration contributes no vertex. Put ${\mu }_{\mathsf{int}}(\nu )=\nu$ and ${\mu }_{\mathsf{arr}}(\nu )=L_{\nu }$. The complement of one integer atom is $$\overline{r-s\le k}:=s-r\le -k-1.$$ Literal substitution replaces an integer literal $n$ by $\mathbf{0}+n$ and an array literal of length $m$ by $\mathbf{0}+m$, then moves constants to the right side of $\le$. Contexts and their complete formation table are

$\cdot \mathsf{ctx}$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢t\mathsf{type}$$x\notin \mathrm{dom}(\mathrm{\Gamma })$

$\mathrm{\Gamma },x:t\mathsf{ctx}$

$\mathrm{\Gamma }\mathsf{ctx}$$\delta \text{ over }V(\mathrm{\Gamma })$

$\mathrm{\Gamma },\delta \mathsf{ctx}$

$\mathrm{\Gamma }\mathsf{ctx}$$p\text{ over }V(\mathrm{\Gamma })\cup \{{\mu }_B(\nu )\}$

$\mathrm{\Gamma }⊢\{\nu :B\mid p\}\mathsf{type}$

$\mathrm{\Gamma }⊢s\mathsf{type}$$\mathrm{\Gamma },x:s⊢t\mathsf{type}$

$\mathrm{\Gamma }⊢x:s\to t\mathsf{type}$

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

The context embedding and semantic entailment are A valuation maps integer variables to integers and array variables to finite integer arrays, interprets $L_a$ by array length, and satisfies $\mathrm{\Gamma }$ when it satisfies $\lfloor \mathrm{\Gamma }\rfloor$. The judgment $\mathrm{\Gamma }\vDash p$ means that every such valuation satisfying $\mathrm{\Gamma }$ satisfies $p$.

For certificate replay, $G_{\mathrm{\Gamma }}$ has vertices $\mathbf{0}$ and $V(\mathrm{\Gamma })$. Every replayed goal atom is required to use only those vertices. Each hypothesis $r-s\le k$ contributes an identified edge $s\stackrel{k}{\to }r$, and every array vertex contributes the implicit edge $L_a\stackrel{0}{\to }\mathbf{0}$. A path certificate for $r-s\le k$ is a possibly empty adjacent edge list from $s$ to $r$ with weight sum at most $k$. A contradiction certificate is a nonempty adjacent cyclic edge list of negative sum. The replay checker re-reads the identified edges, verifies adjacency and endpoints, adds weights in $\mathbb{Z}$, and checks the final bound. A conjunctive goal accepts one contradiction certificate or one path certificate per conjunct. These checks, rather than an external solver’s answer, are the certificate judgment.

Subtyping has exactly two rules. Every displayed type is well formed; $z$ is fresh in the base rule, and arrow binders are alpha-aligned.

$z\notin \mathrm{dom}(\mathrm{\Gamma })$$\mathrm{\Gamma },z:\{\nu :B\mid p\}\vDash q[z/\nu ]$

For an integer atom, $(x,0)$ and $(\mathbf{0},n)$ are its representatives; for an array atom, $(L_a,0)$ and $(\mathbf{0},m)$ are its length representatives. The exact result constructors and get precondition are The second through fourth lines use the representative appropriate to their argument. Atoms and computations synthesize; expressions check. The complete declarative table is

$x:t\in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢x\Rightarrow t$

$\mathrm{\Gamma }⊢n\Rightarrow \mathsf{EqI}(\mathbf{0},n)$

$A\text{ has length }m$

$\mathrm{\Gamma }⊢A\Rightarrow {\mathsf{Array}}_m$

$\mathrm{\Gamma }⊢x:s\to t\mathsf{type}$$\mathrm{\Gamma },x:s⊢e\Leftarrow t$

$\mathrm{\Gamma }⊢(\lambda x.e:x:s\to t)\Rightarrow x:s\to t$

$\mathrm{\Gamma }⊢x:s\to t\mathsf{type}$$\mathrm{\Gamma },f:(x:s\to t),x:s⊢e\Leftarrow t$

$\mathrm{\Gamma }⊢(\mathsf{fix}f(x).e:x:s\to t)\Rightarrow x:s\to t$

$\mathrm{\Gamma }⊢a\Rightarrow s$$|s|=\mathsf{int}$

$\mathrm{\Gamma }⊢a+k{\Rightarrow }_c\mathsf{Shift}(a,k)$

$\mathrm{\Gamma }⊢a\Rightarrow s$$|s|=\mathsf{arr}$

$\mathrm{\Gamma }⊢\mathsf{len}a{\Rightarrow }_c\mathsf{Length}(a)$

$\mathrm{\Gamma }⊢a\Rightarrow s$$|s|=\mathsf{arr}$$\mathrm{\Gamma }⊢i\Rightarrow u$$|u|=\mathsf{int}$$\mathrm{\Gamma }\vDash \mathsf{Bnd}(a,i)$

$\mathrm{\Gamma }⊢\mathsf{get}ai{\Rightarrow }_c\mathsf{int}$

$\mathrm{\Gamma }⊢f\Rightarrow x:s\to t$$\mathrm{\Gamma }⊢a\Leftarrow s$

$\mathrm{\Gamma }⊢fa{\Rightarrow }_{c}t[a/x]$

$\mathrm{\Gamma }⊢a\Rightarrow s$

$\mathrm{\Gamma }⊢a\Leftarrow t$

$\mathrm{\Gamma }⊢c{\Rightarrow }_{c}s$$\mathrm{\Gamma },x:s⊢e\Leftarrow t$$x\notin \mathrm{fv}(t)$

$\mathrm{\Gamma }⊢\mathsf{let}x=c\mathsf{in}e\Leftarrow t$

$\mathrm{\Gamma },\delta \mathsf{ctx}$$\mathrm{\Gamma },\delta ⊢e_1\Leftarrow t$$\mathrm{\Gamma },\bar{\delta }⊢e_2\Leftarrow t$

$\mathrm{\Gamma }⊢\mathsf{if}\delta \mathsf{then}{e}_1\mathsf{else}{e}_2\Leftarrow t$

$\mathrm{\Gamma }⊢t\mathsf{type}$

$\mathrm{\Gamma }⊢\mathsf{error}\Leftarrow t$

The VC generator has the three partial 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}.$$ Its subtyping translation, with $z$ fresh, is It fails on a shape mismatch, an ill-formed displayed type, or a failed recursive call. With $\mathsf{A}$, $\mathsf{Comp}$, and $\mathsf{K}$ denoting the three deterministic partial functions, the atom clauses are Every annotation and entry is also checked for well-formedness. 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 The checking clauses, where $e_{\delta }=\mathsf{if}\delta \mathsf{then}{e}_1\mathsf{else}{e}_2$, are No other clause is implicit. A generated sequent is accepted only after the certificate checker above accepts its evidence.

For finite-qualifier inference, $K$ is a finite set of predicate unknowns and each $Q_{\kappa }$ is a finite set of well-scoped difference atoms. An assignment $$\eta \in \prod _{\kappa \in K}\mathcal{P}(Q_{\kappa })$$ replaces $\kappa$ by the conjunction of the chosen subset; the empty subset means $\mathsf{true}$. Enumeration instantiates the annotated program, runs the displayed VC generator, and accepts the first assignment for which every generated VC has checked replay evidence. This is the entire Liquid fragment: it introduces no additional typing or entailment rule.

The first-order dynamic guard is a source term defined by It is not a higher-order contract wrapper. The source proof-carrying-code package is $(e,t,\mathrm{\Pi })$. Its consumer parses the chapter grammar and checks well-formedness; recomputes the complete VC list for $\cdot ⊢e\Leftarrow t$; matches $\mathrm{\Pi }$ against that recomputed list and replays every certificate; and enables the displayed source reduction only after all checks accept. Producer-supplied VC lists are ignored.

For the erasure boundary, simple types and contexts are $$\tau ::=\mathsf{int}\mid \mathsf{arr}\mid \tau \to \tau ,\mathrm{\Xi }::=\cdot \mid \mathrm{\Xi },x:\tau .$$ Erasure maps refinements to their base shape, dependent arrows to simple arrows, declarations pointwise, and guard entries to nothing. It is homomorphic on terms except for erasing lambda and fixpoint refinements from annotations; dynamic conditionals and $\mathsf{error}$ remain. The target has the three judgments $\mathrm{\Xi }{⊢}_{0}a\Rightarrow \tau$, $\mathrm{\Xi }{⊢}_{0}c{\Rightarrow }_c\tau$, and $\mathrm{\Xi }{⊢}_{0}e\Leftarrow \tau$. Its complete term table is

$x:\tau \in \mathrm{\Xi }$

$\mathrm{\Xi }{⊢}_{0}x\Rightarrow \tau$

$\mathrm{\Xi }{⊢}_{0}n\Rightarrow \mathsf{int}$

$\mathrm{\Xi }{⊢}_{0}A\Rightarrow \mathsf{arr}$

$\mathrm{\Xi },x:\tau {⊢}_{0}e\Leftarrow \sigma$

$\mathrm{\Xi }{⊢}_0(\lambda x.e:\tau \to \sigma )\Rightarrow \tau \to \sigma$

$\mathrm{\Xi },f:(\tau \to \sigma ),x:\tau {⊢}_{0}e\Leftarrow \sigma$

$\mathrm{\Xi }{⊢}_0(\mathsf{fix}f(x).e:\tau \to \sigma )\Rightarrow \tau \to \sigma$

$\mathrm{\Xi }{⊢}_{0}a\Rightarrow \mathsf{int}$

$\mathrm{\Xi }{⊢}_{0}a+k{\Rightarrow }_c\mathsf{int}$

$\mathrm{\Xi }{⊢}_{0}a\Rightarrow \mathsf{arr}$

$\mathrm{\Xi }{⊢}_0\mathsf{len}a{\Rightarrow }_c\mathsf{int}$

$\mathrm{\Xi }{⊢}_{0}a\Rightarrow \mathsf{arr}$$\mathrm{\Xi }{⊢}_{0}i\Rightarrow \mathsf{int}$

$\mathrm{\Xi }{⊢}_0\mathsf{get}ai{\Rightarrow }_c\mathsf{int}$

$\mathrm{\Xi }{⊢}_{0}f\Rightarrow \tau \to \sigma$$\mathrm{\Xi }{⊢}_{0}a\Leftarrow \tau$

$\mathrm{\Xi }{⊢}_{0}fa{\Rightarrow }_c\sigma$

$\mathrm{\Xi }{⊢}_{0}a\Rightarrow \tau$

$\mathrm{\Xi }{⊢}_{0}a\Leftarrow \tau$

$\mathrm{\Xi }{⊢}_{0}c{\Rightarrow }_c\tau$$\mathrm{\Xi },x:\tau {⊢}_{0}e\Leftarrow \sigma$

$\mathrm{\Xi }{⊢}_0\mathsf{let}x=c\mathsf{in}e\Leftarrow \sigma$

$\delta \text{ over }V(\mathrm{\Xi })$$\mathrm{\Xi }{⊢}_0{e}_1\Leftarrow \tau$$\mathrm{\Xi }{⊢}_0{e}_2\Leftarrow \tau$

$\mathrm{\Xi }{⊢}_0\mathsf{if}\delta \mathsf{then}{e}_1\mathsf{else}{e}_2\Leftarrow \tau$

$\mathrm{\Xi }{⊢}_0\tau \mathsf{type}$

$\mathrm{\Xi }{⊢}_0\mathsf{error}\Leftarrow \tau$

Simple formation has exactly the three base/arrow constructors of $\tau$; there is no target subtyping judgment. The target deliberately omits the source bounds premise from ST-Get.