ch:symbolic-execution: ch:symbolic-execution

Problem and invariant. Every accepted failure needs a model satisfying every path atom and a concrete replay with the recorded outcome. Every accepted unsatisfiability claim needs a closed, strictly negative graph cycle.

Two representations. An arbitrary solver formula is expressive. The companion’s atom and edge lists instead expose every trusted comparison and retain unknown.

First complete version. Implement concrete evaluation, symbolic affine terms, and a bounded work-list explorer that generates the four $\mathsf{Fork}$ paths. Check models before replay, then check certificate-edge incidence, cycle closure, and strict weight sum.

Observable result. Nine named passes distinguish generated paths, safe and failed inputs, accepted and rejected cycles, a foreign edge, a malformed model, retained unknown, and branch reversal.

A failing version. Replace total < 0 by total <= 0. The unchanged zero-cycle oracle fails although the mutation still typechecks.

Acceptance test. Run the four Kappa commands in appendix E and require the exact transcript and empty audit. Restore strict negativity. Typecheck Representation.agda separately only when Agda is available.

Mathematical boundary. The finite checker does not prove solver completeness, loop coverage, or the general simulation theorem.