ch:refinement-types: ch:refinement-types

First prove the requested commutation lemma by induction on $e_1$: $$\begin{array}{}\text{(}\ast \text{)}& e_1[a/x]{▹}_y{e}_2=(e_1{▹}_y{e}_2)[a/x].\end{array}$$ All binders are alpha-renamed fresh for $a,e_2,x,y$. If $e_1=b$ is an atom, the two sides are $e_2[b[a/x]/y]$ and $e_2[b/y][a/x]$; ordinary capture-avoiding substitution commutes because $x\ne y$, $y\notin \mathrm{fv}(a)$, and $x\notin \mathrm{fv}(e_2)$. For $e_1=\mathsf{let}z=c\mathsf{in}e$, both sides retain the same fresh head let and $(\ast )$ for $e$ identifies their tails. The conditional clause distributes bind composition into both branches, so the two branch induction hypotheses prove $(\ast )$. For $e_1=\mathsf{error}$, both sides are $\mathsf{error}$.

Now induct on $e_0$. If $e_0=a$ is an atom, the desired equation is exactly $(\ast )$: $$(e_1[a/x]){▹}_y{e}_2=(e_1{▹}_y{e}_2)[a/x].$$ If $e_0=\mathsf{let}z=c\mathsf{in}e$, alpha-rename $z$ fresh. Both sides retain $\mathsf{let}z=c\mathsf{in}(-)$, and the induction hypothesis for $e$ equates the two tails. If $e_0$ is a conditional, expanding the definition on both sides gives conditionals with the same test; apply the induction hypothesis separately to the then and else branches. Finally, $$(\mathsf{error}{▹}_x{e}_1){▹}_y{e}_2=\mathsf{error}=\mathsf{error}{▹}_x(e_1{▹}_y{e}_2).$$ These are all expression forms, so associativity holds modulo exactly the capture-avoiding renamings stipulated by the definition.

Both (a) and (b) are well formed. In (a), the domain adds $L_a$ to the scope and the codomain binder adds $\nu$, so $\nu -L_a\le -1$ passes WF-Base. In (b), the domain adds $i$ and the array codomain binder contributes $L_{\nu }$, so $L_{\nu }-i\le 0$ is likewise scoped.

Expression (c) is rejected. A function-shaped declaration contributes no predicate vertex, so $f$ is absent from $V(f:(\mathsf{int}\to \mathsf{int}))$; the occurrence of $f$ in $\nu -f\le 0$ fails the premise of WF-Base. Expression (d) is well formed in the empty context: $L_{\nu }$ is the distinguished vertex supplied by the array refinement binder itself, and $\mathbf{0}$ is always available.

The graph edges, written in the order of the hypotheses, are $$y\stackrel{2}{\to }x,z\stackrel{-4}{\to }y,x\stackrel{1}{\to }z.$$ Their identifiers form the adjacent cycle $y\to x\to z\to y$. The replay checker verifies the common endpoints and calculates Thus this three-edge list is a contradiction certificate.

After replacing the last constant by $2$, take $$h(\mathbf{0})=0,h(x)=0,h(z)=2,h(y)=-2.$$ Then $h(x)-h(y)=2$, $h(y)-h(z)=-4$, and $h(z)-h(x)=2$. All three constraints hold, so the zero-weight cycle is not a contradiction.

Introduce the fresh vertex $z$ for the source refinement. Its upper-bound atom contributes the edge $L_a\stackrel{-1}{\to }z$. The target asks for $z-L_a\le 0$, and that one-edge path has weight $-1\le 0$. Hence S-Base gives the displayed subtype judgment. The source’s lower-bound edge $z\stackrel{0}{\to }\mathbf{0}$ is present but is not needed for this goal.

For the reverse direction, let $a$ be a one-element array and assign $z=1$. Then $z-L_a=0$, so the weaker target refinement is satisfied. But the putative reverse target contains $z-L_a\le -1$, namely $0\le -1$, which is false. This valuation refutes the entailment premise of the reverse S-Base instance.

Without the nonempty input refinement, exact length and shift synthesis still give $n=L_a$ and $i=n-1$. Therefore the upper-bound goal has the path $$L_a\stackrel{0}{\to }n\stackrel{-1}{\to }i,$$ of weight $-1$, which certifies $i-L_a\le -1$.

The lower-bound goal is $\mathbf{0}-i\le 0$. Its available route is $$i\stackrel{1}{\to }n\stackrel{0}{\to }{L}_a\stackrel{0}{\to }\mathbf{0},$$ whose weight is $1$, not at most $0$. This failure is genuine: set $$h(\mathbf{0})=0,h(L_a)=h(n)=0,h(i)=-1.$$ The potential satisfies both equalities $n=L_a$, $i=n-1$, and the implicit length constraint, but it makes . Hence no certificate for the lower bound exists.

Write $F=\mathsf{fix}f(x).e_1:x:s\to t$. Inversion before the E-Fix step supplies $$f:(x:s\to t),x:s⊢e_1\Leftarrow t,\cdot ⊢v\Leftarrow s,y:t[v/x]⊢e_2\Leftarrow u,$$ with $y\notin \mathrm{fv}(u)$. Rule D-Fix, followed by reflexive subtyping and D-Sub, gives $$\cdot ⊢F\Leftarrow x:s\to t.$$ Substitution for the function variable is therefore $$x:s⊢e_1[F/f]\Leftarrow t;$$ the types do not change because a function-shaped $f$ supplies no predicate vertex. Substitution for the argument is then $$\cdot ⊢e_1[F/f,v/x]\Leftarrow t[v/x].$$ Finally lemma 10.22, with the displayed continuation premise, gives $$\cdot ⊢e_1[F/f,v/x]{▹}_y{e}_2\Leftarrow u,$$ which is exactly the reduct’s required type.

With only $\mathbf{0}-\nu \le 0$, the candidate invariant says $i\ge 0$ and contains no relation between $i$ and $L_a$. Take $L_a=1$, $i=2$, and $j=1$. The else guard is satisfied, the shift equation $j=i-1$ holds, and $j\ge 0$. The read’s upper VC is nevertheless $$j-L_a\le -1,\text{that is}0\le -1,$$ so the assignment is rejected.

Now add $\nu -L_a\le 1$. At entry, $n=L_a$ satisfies both $n\ge 0$ and $n-L_a\le 1$. In the recursive branch, the guard gives $i\ge 1$, hence $j=i-1\ge 0$, while $i-L_a\le 1$ gives $j-L_a\le 0\le 1$. Thus the recursive call preserves both qualifiers. The same valuation $L_a=1,i=2,j=1$ satisfies them, but still makes $j=L_a$ and falsifies the strict read bound. The nearby qualifier is inductive but too weak for array safety.

For $A=⟨7⟩$, E-Len first yields $$E=\mathsf{let}z=\mathsf{get}A1\mathsf{in}z.$$ The bounds conjunction is $0\le 1$ followed by . Guard elaboration therefore produces The first test is true, so E-IfT selects the inner conditional. The second test is false, so E-IfF yields $\mathsf{error}$. The failing test is the strict upper bound ; evaluation never reaches the stuck get.

The consumer does not compare the producer’s certificates with the producer’s claimed VC list. At protocol step 2 it reruns the deterministic generator on $\cdot ⊢\mathit{last}\Leftarrow t$, producing the complete list $\mathcal{C}$, including the bounds VC for the get. At step 3 it matches the supplied bundle $\mathrm{\Pi }$ against this recomputed list. Because $\mathrm{\Pi }$ has no certificate for the recomputed get VC, matching or replay fails and evaluation is never enabled at step 4.

If the consumer instead accepted a producer-supplied VC list, the malicious producer could delete precisely the obligations that make an unsafe term untypable and then provide valid certificates for the harmless remainder. Acceptance would no longer imply that every VC generated by the fixed checker is valid. Therefore checker correctness could not yield $\cdot ⊢e\Leftarrow t$, and preservation/progress could not be invoked. The first implication of theorem 10.32 would be false; VC recomputation is the step that binds the evidence to the actual program and policy.

In the empty context the only nonconstant vertex available to a refinement is $\nu$. After normalization, every atom is one of $$\nu \le k,k\le \nu ,\text{a constant truth value},$$ for some $k\in \mathbb{Z}$. A finite conjunction collects finitely many upper and lower bounds. If a constant conjunct is false, its denotation is empty. Otherwise, taking the least upper bound $U$ and greatest lower bound $L$ that occur, its denotation is one of $$\mathbb{Z},\{n\mid n\le U\},\{n\mid L\le n\},\{n\mid L\le n\le U\},\varnothing .$$ Every nonempty unbounded case contains consecutive integers and hence an odd integer. Every bounded interval is finite, whereas the set of even integers is infinite in both directions. The empty case and all of $\mathbb{Z}$ are also plainly wrong. Thus no predicate in this conjunction-only difference fragment denotes exactly the even integers.