ch:refinement-types: ch:refinement-types

Problem, result, and invariant. Build a producer and consumer for the chapter’s difference-constraint certificates. The observable result is the eight-case report in appendix E. The consumer invariant is that every accepted proof names existing graph edges, follows adjacent endpoints, and establishes the requested bound or a strictly negative closed cycle.

Representation. Represent an atom $r-s\le k$ by an identified edge from $s$ to $r$ of weight $k$. Keep vertices, edge identifiers, paths, cycles, program steps, and qualifiers as nominal data. This separates certificate replay from Kappa’s own type relation and prevents a Boolean “verified” flag from standing in for evidence.

First complete version. Generate graph edges from assumptions, exact lengths, and literal shifts. At each array read generate both $0\le i$ and . Replay a path by looking up each identifier, checking adjacency, summing weights, and comparing the first and last vertices with the goal. Replay a contradiction only when the path is nonempty, closed, and has negative total weight.

Remaining cases. Recompute the verification-condition list from the object program instead of trusting a producer-supplied list. Add fuelled finite search, but accept a search result only after replay. Exercise $\mathit{last}$, $\mathit{lastOrZero}$, malformed certificates, the negative-cycle example, and powerset qualifier search with both the sufficient and nearby inadequate upper bounds.

A failing version. Accept a path without checking adjacent endpoints. The program still typechecks, but a path can splice unrelated edges and the malformed-certificate case fails. Weakening the generated lower goal or accepting a zero-weight cycle supplies two independent controls with named failures.

Acceptance test. Run the four gates recorded in appendix E. Require the exact eight PASS lines, the frozen final summary, and audit output []. Replay at least one bound-weakening mutation and one malformed-evidence mutation; each must keep the source type-correct while making the output oracle fail.

Mathematical boundary. The artifact executes graph construction, finite search, certificate replay, and finite qualifier enumeration on the named corpus. It proves neither certificate exactness nor checker correctness, array safety, Liquid relative completeness, or proof-carrying-code soundness.