ch:session-types: protocol traces

Problem and invariant. Check that two finite traces have opposite outer actions and equal payload types at every position. Empty traces pair inaction with inaction, and choice requires select/offer with the same label.

Two representations. A recursive protocol datatype can preserve binders explicitly. The companion instead stores one pre-unrolled request/answer trace as a finite trace ending in a delimiter that is not a process action. The first supports a coinductive checker; the second keeps termination and every accepted comparison executable in portable Kappa while proving nothing about recursive duality.

First complete version. Define payloads, actions, the involutive action-dual table, action equality, and lockstep trace comparison. Add termination, tensor, and choice cases before the pre-unrolled request/answer trace. Add one mismatched payload only after all positive cases pass.

A failing version. Map left selection to a right offer. It remains well typed, but only the left-choice oracle changes to FAIL.

Acceptance test and boundary. Run all four commands and require six PASS lines, the summary, and an empty audit. The result checks finite traces, not process reduction, logical progress, recursive duality in general, or graded communication.