ch:dependent-session-types: indexed protocol traces
Problem and result. Check a finite endpoint trace that sends a length, substitutes that length in the continuation, sends a vector, and terminates. The invariants are dual endpoint polarity, one endpoint advance per communication, and equality of the substituted payload index. Acceptance requires the valid length-two trace and both nearby rejection cases.
Representation. The companion stores a small protocol state, an optional natural index, and an endpoint token containing a channel identity and protocol generation. A fully indexed process datatype could enforce the continuation index and linear advance statically, but then a mismatched trace could not be supplied as diagnostic input. The finite state representation makes both failures observable while keeping the substitution site explicit.
First complete version. Implement termination and length transmission. The length transition writes Some length into the protocol state and advances the endpoint generation. A length-two trace now reaches the vector transition with the residual classifier
Remaining cases. Add vector transmission by comparing the payload length with the stored index and the supplied endpoint generation with the current one. Add the ATS-style bounded repeat unfolding last: it emits one element action per successor and reaches end only at zero. This follows functional substitution first, linear endpoint accounting second, and the separate indexed-protocol comparison last.
A failing version. Replace the length transition by one that stores no index. The valid trace, the mismatch rejection, and the dedicated substitution oracle all fail. Separately, bypassing the endpoint-generation comparison makes duplicate-endpoint fail. Stopping unfoldRepeat one element early fails both array fixtures.
Acceptance test. Require accepted: end, rejected: expected Vec 2, and rejected: endpoint reused, together with the fourth substitution line, both array lines, and an empty audit. Replay all three named mutations as recorded in subappendix E.9; that executable record alone stores the accepted source identity.
Mathematical boundary. The checker illustrates the classifier agreement of lemma 102.5. It does not prove functional or channel substitution, preservation, closed global progress, an asynchronous protocol theorem, or the ATS static sort.