ch:multiparty-sessions: projection audit

Problem and invariant. Project the sale example from a finite global AST, replay its sender-tagged FIFO transitions, and check that distinct addresses discharge linearity vacuously. Separately project a finite choreography, regenerate endpoints after changing it, and reject an uninformed merge.

Two representations. The companion implements the fragments of global/local syntax needed by the sale protocol and of choreography/control syntax needed by the branch example. Both projections and partial merges are executable. The fragments remain deliberately smaller than the repaired Coq calculus and the Pirouette development.

First complete version. Introduce roles, labels, payloads, global and local ASTs, and partial projection. Add FIFO enqueue/consume and the direct shared-address dependency case detector. Then introduce the choreography/control ASTs, partial control merge, endpoint regeneration, and the hand-written endpoint comparison.

A failing version. Delete equality of branch-specific send expressions from control merge. The program still checks, but the missing-branch-knowledge oracle fails.

Acceptance test and boundary. Run the four commands and require the exact eight-line output and empty audit. This is finite executable evidence only; it does not prove ECOOP subject reduction, communication safety, Pirouette projection, or deadlock freedom.