appendix sectionsignatures

Symbolic-execution and noninterference boundaries

SymImp-DL

Signature.: Integer variables, fixed input oracles, copy-plus-constant assignments, sequencing, conditionals, assertions, and while; guards and conjunctive path conditions are difference constraints. Symbolic states carry a store, condition, and fresh-input cursor.
Locally proved.: Expression correspondence, one- and finite-step simulation, path soundness, loop-free finite-path coverage, preservation of coverage under locally checked negative-cycle pruning, subsumption, and model-to-test correctness with deterministic replay.
Certificate boundary.: Unsatisfiability means an explicit, locally checked strictly negative cycle. Satisfiability means a locally checked integer map plus replay. Unsupported formulas and unknown retain the path. No external solver is a premise of the theorem.
Separate extension.: SymImp-DL $\lor$ adds Boolean conditions and guarded stores and has its own representation lemma. No core coverage theorem is transferred without new simulation cases.
Not claimed.: General SMT completeness, unbounded-search termination, unrestricted-loop coverage, heap or concurrent symbolic execution, quantified or floating-point theories, or residual-program generation.

Signature.: A deterministic sequential imperative language over a finite security lattice and fixed-labelled mutable store. Command typing carries an explicit program-counter label.
Locally proved.: Program-counter monotonicity, subject reduction, expression agreement, high-context confinement, two-run unwinding, and termination-insensitive noninterference for pairs of terminating evaluations.
DCC comparison.: The separate functional card reconstructs Algehed–Bernardy Theorem 8 for the original DCC from their shallow Theorem 3, translation type preservation (Theorem 5), reduction preservation (Theorem 6), strong normalization, confluence, and protected-Boolean reflection. It is not a theorem about mutable imperative stores.
Artifact boundary.: The Kappa checker tests the two-point instance. The pinned DCC Agda sources contain named postulates for their published proof interface. A static hole scan is not reported as a fresh Agda typecheck.
Not claimed.: Termination-sensitive security, declassification, concurrency, probabilistic observation, quantitative leakage, term-sensitive relations, or results for other DCC variants.