Abstract interpretation and checked invariants

For a concrete transformer $F:C\to C$, an abstract transformer $F^{\mathrm{♯}}:A\to A$, and a monotone concretization $\gamma :A\to C$, the local simulation obligation is $$F\gamma ⊑\gamma F^{\mathrm{♯}}.$$ If both transformers are monotone on complete lattices, fixed-point transfer gives $$\mathrm{lfp}(F)⊑\gamma (\mathrm{lfp}(F^{\mathrm{♯}})).$$ Any checked $A$ satisfying $F^{\mathrm{♯}}(A)⊑A$ is likewise sound: Park induction gives $\mathrm{lfp}(F)⊑\gamma (A)$.

The structural analyzer returns a pair $({\mathsf{post}}^{\mathrm{♯}}(c,A),{\mathsf{err}}^{\mathrm{♯}}(c,A))$. Its terminal-store and error obligations are Tests must satisfy Assume-Sound; loops use a pre-fixed invariant. An interval widening drops a decreasing lower endpoint to $-\mathrm{\infty }$ and an increasing upper endpoint to $+\mathrm{\infty }$. DBM copy-plus-constant assignment updates, for every node $w$, $$D_{xw}^{\prime }=D_{yw}+k,D_{wx}^{\prime }=D_{wy}-k,D_{xx}^{\prime }=0,$$ and then closes the matrix. Entrywise DBM extrapolation drops every weakened finite entry to $+\mathrm{\infty }$ and therefore terminates on a finite matrix.

The CESK-star comparison uses the simply typed source rules

$\mathrm{\Gamma },x:A⊢e:B$

$\mathrm{\Gamma }⊢\lambda x.e:A\to B$

$\mathrm{\Gamma }⊢e_1:A\to B$$\mathrm{\Gamma }⊢e_2:A$

$\mathrm{\Gamma }⊢e_1{e}_2:B$

Its representative CEK transitions are

$⟨e_0{e}_1,\rho ,\kappa ⟩⟶⟨e_0,\rho ,\mathsf{ar}(e_1,\rho ,\kappa )⟩$

$v_0\mathsf{value}$

$⟨v_0,\rho ,\mathsf{ar}(e_1,{\rho }_1,\kappa )⟩⟶⟨e_1,{\rho }_1,\mathsf{fn}(v_0,\kappa )⟩$

$v_1\mathsf{value}$

$⟨v_1,{\rho }_1,\mathsf{fn}(⟨\lambda x.e,{\rho }_0⟩,\kappa )⟩⟶⟨e,{\rho }_0[x\mapsto v_1],\kappa ⟩$

The three imported theorem cards retain separate signatures: the CESK-star one-step simulation abstracts a concrete machine step; Move’s borrow-graph theorem preserves $\mathsf{Inv}(s,\mathsf{Abs}(s))$; Verasco’s vanalysis_correct excludes $\mathsf{Goes}\mathsf{\_}\mathsf{wrong}$ after the five section parameters and result $(\mathsf{tt},\mathsf{nil})$ are fixed.