Difference-refinement array calculus

The calculus of chapter 10 is a call-by-value A-normal source language with integer and integer-array base values, integer shift by a literal, array length and read, annotated lambda and fixpoint values, application, let, one-atom conditionals, and checked $\mathsf{error}$. A base refinement is a finite conjunction of integer difference atoms over integer variables, array-length measures, and zero. There is no array equality, content measure, disjunction, general linear arithmetic, term-indexed type family, equality type, or conversion judgment.

Contexts contain typed declarations and difference-atom guards. Their semantic embedding is the conjunction of base refinements and guards. Base subtyping is implication in that exact semantics; arrow subtyping is contravariant in its domain and covariant in its codomain under the target-domain binder. Narrowing is lemma 10.12. Shape preservation, reflexivity, and transitivity are proposition 10.13.

Atoms and computations synthesize, while expressions check. Exact singleton synthesis records integer values and array lengths. The only logical premise at a read is $\mathsf{Bnd}(a,i)$. The deterministic $\mathsf{A}/\mathsf{Comp}/\mathsf{K}$ generator emits finite VC lists through the exact $\mathsf{SubVC}$ translation; it does not invoke an entailment oracle. Successful generation may emit invalid VCs. Conditional on a returned generation equation, the corresponding declarative judgment holds exactly when every emitted VC is valid. Conversely, every declarative derivation reconstructs a generation output of the displayed type with all VCs valid. This generation/validation separation is lemma 10.16, theorem 10.17.

Difference hypotheses are identified weighted graph edges, including an implicit nonnegative-length edge for every array. The trusted replay checker accepts adjacent bounded-weight paths or negative cycles and performs integer addition itself. Soundness, completeness, and certificate-producing decidability are lemma 10.7, theorem 10.9, corollary 10.10. An external solver or certificate search is not part of these theorems.

Closed reduction has exactly shift, length, in-bounds get, beta, fixpoint, and the two conditional roots. Bind composition preserves A-normal syntax. The structural package comprises context implication and narrowing, static substitution, precision under a narrowed declaration, weakening and value substitution, canonical forms, bind typing, and valid-guard discharge in lemma 10.12–lemma 10.23. Preservation, progress up to checked error, and array safety are theorem 10.24, theorem 10.25, corollary 10.26. No normalization theorem is claimed: annotated fixpoints are in the signature.

Each predicate unknown receives a finite, well-scoped qualifier set. Exhaustive enumeration terminates and is sound; it is complete only relative to those exact finite sets and the fixed template instance, as stated in theorem 10.28. There is no completeness theorem for arbitrary refinements or all safe programs.

First-order guard elaboration inserts nested source conditionals ending in $\mathsf{error}$. A checked bounds certificate justifies removing those tests for states satisfying the static context by theorem 10.30. The source PCC consumer recomputes VCs, ignores producer-supplied VC lists, and replays supplied evidence before evaluation. Its local acceptance theorem is theorem 10.32; no compiler, assembly-language safety policy, higher-order blame theorem, or SMT model is inherited.

Erasure targets the simply typed A-normal language with $\mathsf{int}$, $\mathsf{arr}$, and arrows. Dynamic conditionals remain, while logical context guards and refinements erase. Erasure preserves formation and typing by proposition 10.35; its converse fails at the unguarded last index. Result refinements may mention an input integer or its array length, but arbitrary terms cannot occur as type indices.

The pinned Kappa corpus described in appendix E runs VC generation, certificate replay, finite-qualifier selection, and eight grouped positive/negative cases. It is implementation evidence only, not an independent proof of the calculus or of the Kappa compiler.