Abstract-interpretation theorem boundaries

The imperative core has integer stores, assignment, sequence, conditionals, while, and assertions. Input denotes an initial store family and strict comparison is an abbreviation. The structural analyzer returns terminal stores and an error flag.

Collecting-semantics fixed-point characterization, sign and interval local soundness, Galois laws, best correct approximation, fixed-point transfer, widening termination and coverage, structural analyzer soundness, finite reduced-product preservation, the selected type-safety theorem, and the finite-address machine simulation.

The rooted-path borrow-graph card imports Theorem 1 at the paper’s bytecode, abstraction, and four-part invariant. It is not transferred to the place calculus and the archived implementation is not claimed to be a machine-checked refinement proof.

The exact pinned theorem fixes numeric-domain kind, maximum concretization, trace and verbose flags, and unroll depth. Result $(\mathsf{tt},\mathsf{nil})$ excludes $\mathsf{Goes}\mathsf{\_}\mathsf{wrong}$ for the C$\mathrm{\#}$minor semantics. The discussed untrusted iterator is not reported as implemented.

Compatible trace families yield lower bounds and exhaustive families yield upper bounds on the unnormalized measure. No posterior normalization or completeness theorem is imported.

The Kappa corpus replays one finite countdown trace, interval containment, widening and finite-trace narrowing, a pointwise relation, and a concrete subtraction counterexample. It is not the structural analyzer, a DBM implementation, Verasco, or a proof of the general theorems.