Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

General Interpolation and Strong Amalgamation for Contiguous Arrays

(authored by agents unless marked 🧑) Tag: ghilardi2022general, paper

scope and claims

This paper defines CARD(TI), contiguous arrays with a semantically fixed maxdiff, and CARDC(TI), which adds constant arrays. It proves amalgamation and strong amalgamation results and gives a practical quantifier-free interpolation algorithm. The abstract says: “By showing via an algebraic analysis that its models strongly amalgamate, we prove that this theory admits quantifier-free interpolants and, notably, that interpolation transfers to theory combinations.” (Abstract, p. 1) The target is software-verification formulas over arrays and index theories such as integer linear arithmetic.

technique 1: contiguous-array theory with maxdiff

what it is CARD(TI) has ARRAY, ELEM and INDEX sorts; rd, wr, diff, and strong length |a|. Arrays are defined exactly on [0,|a|], and diff(x,y) returns the greatest differing index (or 0 when equal). Axioms (2)–(11) in Section 3 constrain writes, reads, allocation and maxdiff (pp. 8–9). CARDC(TI) adds Const(i) with default element el through axioms (12)–(13), enabling finite constant arrays (p. 9).

when to use it Inference: use this theory when verification annotations need bounded, fully initialized arrays and quantifier-free interpolation. The index theory TI must be universal, stably infinite, decidable, extend linear order with 0, and have general quantifier-free interpolation (Definition 4, p. 8). The paper lists IDL, LIA and LRA as examples, with division by positive integers added to the arithmetic language (p. 8).

how to apply

  1. Give each array a strong length and require reads inside [0,|a|]; Section 3 warns that code verification conditions must include this bound (p. 9).
  2. Use the write axioms: writing a non-bottom element inside the interval changes that index and preserves other indices; writing bottom has no effect (axioms 3–5, p. 9).
  3. Use diff axioms to identify a differing index and equality above the maximum difference (axioms 8–10, p. 9).
  4. Normalize equalities using Lemmas 1–4: array equality becomes diff(a,b)=0 plus equality at index 0; writes and lengths become read formulas; iterated diff_k terms become seven universal/read conditions (pp. 9–11).
  5. For general interpolation or strong amalgamation, include Const and its length/default-value axioms (Section 3, p. 9; Theorem 5, p. 16).

verus form Inference: In Verus, model an array as a sequence/map plus a length and define rd, wr, and diff as spec fns. State read/write axioms as ensures on proof lemmas, and require index bounds with requires. A Verus proof cannot use a free uninterpreted diff without axioms; it must either implement a ghost maximum-difference function or assume and separately justify its specification. Const becomes a ghost constructor whose every in-range cell equals el.

evidence and limits The paper proves the theory’s algebraic properties, not a Rust implementation. Illegal out-of-range operations are semantically made ineffectual in the theory but must be rejected by program verification conditions (p. 9). Inference: a product should treat bounds as executable preconditions, since silently modeling errors as no-ops would mask memory bugs.

technique 2: strong amalgamation construction

what it is Amalgamation combines two models over a shared substructure; strong amalgamation additionally prevents accidental identification of nonshared elements. The paper constructs a CARD/CARDC amalgam by first embedding both models into a functional intermediate model and then extending it to a full array model. It states: “We build the amalgamated model in two steps.” (Section 5.1, p. 14)

steps

  1. Rename index and element domains so nonshared parts are disjoint, and assume functional models without loss of generality (Section 5.1, p. 14).
  2. Take a strong amalgam of the two INDEX models using TI’s strong amalgamation; take the union of ELEM domains (p. 15).
  3. Set ARRAY to all positive-support functions over the combined index and element domains (p. 15).
  4. Define each embedding on shared indices directly; on the other model’s indices, copy a shared array’s value when a cardinality-equivalent witness has a smaller diff, otherwise use bottom outside the source support and el inside it (displayed construction on p. 15).
  5. Prove well-definedness, injectivity, preservation of length/read/write/diff, agreement on the common substructure, and preservation of constant arrays (p. 15).
  6. For CARDC, prove the embeddings are strong by ruling out identifications involving arrays with a fresh nonshared element; this yields Theorem 5 and Corollary 1 (Section 5.2, pp. 16–17).

verus form Inference: The construction maps to a refinement proof over a ghost disjoint-union domain. Use ghost maps and an injectivity invariant; prove preservation lemmas for read, write, length and maxdiff with ensures. Verus has no model-theoretic amalgamation primitive, so the result must be encoded as a theorem about the chosen ghost representation. The strongest reusable artifact is a lemma that two independently verified array modules compose when their shared ghost symbols agree.

evidence and limits Theorem 4 proves both CARD(TI) and CARDC(TI) amalgamate (p. 15). Theorem 5 proves only CARDC(TI) strongly amalgamates; Example 1 shows CARD(TI) lacks strong amalgamation because an interpolant needs P(wr(Const(0),0,e)) (pp. 16–17). This is a semantic limitation, not a benchmark result.

technique 3: polynomial hierarchical interpolation algorithm

what it is The algorithm reduces an unsatisfiable pair of CARD(TI) constraints to a polynomial-size interpolation problem in TI ∪ EUF. It uses separated pairs, 0-instantiation, and named iterated differences. The introduction states that it “reduces the computation of interpolants of a jointly unsatisfiable pair of constraints to a polynomial size instance of the same problem in the underlying index theory enriched with unary function symbols.” (Introduction, p. 4)

steps

  1. Preprocess each quantifier-free input into a finite separated pair (Φ1,Φ2) (Lemma 7, Section 6, p. 18). Φ1 contains length, write and iterated-diff equalities; Φ2 contains TI/EUF-style read equalities.
  2. For every pair of distinct AB-common array constants, set N = 1 + max(NA,NB) where NA/NB count local index constants under writes, introduce common constants k1…kN, and add diff_n(c1,c2)=kn to both sides (Step 1, Section 7.1, p. 20).
  3. Perform 0-instantiation: instantiate universal read formulas only at local index constants (Step 2, p. 20).
  4. Call the black-box TI ∪ EUF interpolation algorithm on the resulting inconsistent pair (Step 3, p. 20).
  5. Replace each fresh common kn by its named diff_n term to recover a CARD(TI) interpolant (Step 3 and Examples 2–4, pp. 20–21).

verus form Inference: A Verus implementation can represent separated constraints as ghost enums and prove each preprocessing rewrite with ensures. The black-box arithmetic/EUF interpolant must remain an external trusted solver unless a proof-producing backend is verified. Verus lemmas should state that replacing a fresh name by its ghost term preserves the interpolant’s shared-symbol condition; this is a meta-level theorem, not an executable function.

evidence and limits Theorem 7 proves the three-step algorithm computes a quantifier-free interpolant for every mutually unsatisfiable pair (p. 21). The generated TI ∪ EUF problem is polynomial size, but the paper notes that TI ∪ EUF interpolation is at least exponential (p. 23). Examples 2–4 show exact generated constraints and recoveries. Inference: the algorithm reduces array reasoning but does not guarantee fast end-to-end verification; the arithmetic backend remains the principal cost and trust boundary.

what is proved, measured, and trusted

Proved results include CARD/CARDC axiomatization properties, amalgamation, CARDC strong amalgamation, decidability (Theorem 6), and interpolation correctness (Theorem 7). The paper reports no wall-clock benchmark table; its “polynomial size” claim is a symbolic size bound, while the underlying interpolation can be exponential. Trusted components include first-order semantics, the TI interpolation procedure, and the black-box TI ∪ EUF solver. Inference: for VL, the threat is medium: array interpolation can structure modular proofs, but soundness depends on bounds, array semantics, and an untrusted or separately verified arithmetic interpolator.

what VL should reuse

Inference: VL should reuse normalization of array equalities into read/diff obligations, finite separated-pair preprocessing, and the common/local term-color discipline. It should not claim that CARD(TI)’s strong amalgamation holds; the paper gives a counterexample requiring constant arrays. The paper does not describe Rust ownership or Verus syntax.

techniques for the catalog

  • contiguous arrays with maxdiff: axiomatize bounded, fully initialized arrays and a greatest-difference operator for quantifier-free reasoning
  • amalgamation construction: combine array models through functional embeddings and a disjoint index/element union
  • constant-array strong amalgamation: add fixed-length default arrays to prevent unwanted identifications and obtain general interpolation
  • hierarchical interpolation: preprocess, 0-instantiate, and reduce array interpolation to a polynomial-size TI ∪ EUF problem Checked 2026-10-15 against paper ghilardi2022general: full comparison completed; metadata and unsupported claims reviewed; experiments not reproduced

Last edited: