import Protocol.Coherence.Consume
import Protocol.Coherence.GraphDelta
import Protocol.Coherence.EdgeCoherence
import Protocol.Coherence.StoreTyping
import Protocol.Coherence.Preservation
import Protocol.Coherence.SelectPreservation
import Protocol.Coherence.HeadPreservationSend
import Protocol.Coherence.HeadPreservationSelect
import Protocol.Coherence.ValidLabels
import Protocol.Coherence.Renaming
import Protocol.Coherence.ConfigEquiv
import Protocol.Coherence.Unified
import Protocol.Coherence.RoleSwap
import Protocol.Coherence.Delegation
import Protocol.Coherence.ErasureCharacterization
import Protocol.Coherence.Conserved
import Protocol.Coherence.Minimality


/-! # MPST Coherence

This module defines the coherence invariant for multiparty session types.

In binary session types, coherence states that after consuming in-flight messages,
dual endpoints have dual types. In MPST, this generalizes to:

**For each directed edge (p → q) in session s:**
1. The sender's local type G[s,p] is consistent with what was sent on D[s,p,q]
2. The receiver's local type G[s,q] is consistent with what must be received on D[s,p,q]
3. The communication patterns match: sends to q align with branches from p

## Consume Function

The `Consume` function models how a local type evolves as buffered messages arrive.
For role p's view:
- `Consume L [] = some L` (no messages → unchanged)
- `Consume (recv q T L) (T :: ts) = Consume L ts` (receive consumes a message)
- `Consume (branch q bs) _ = ...` (branch must handle incoming label)

## Coherence Invariant

`Coherent G D` states that for every session and every **active** directed edge:
- Sender's continuation after sending matches what's in the queue
- Receiver's continuation after consuming matches sender's intent

## Proof Technique: Edge Case Analysis

The key preservation proofs (`coherent_send_preserved`, `coherent_recv_preserved`)
proceed by case analysis on which edge we're checking coherence for:

1. **e = updated edge**: The sender's/receiver's local type changed, trace changed
2. **e involves modified endpoint**: The other endpoint of e was modified
3. **e unrelated**: Neither endpoint was modified, environments unchanged at e

This 3-way case split is the core proof technique for coherence preservation.
Adapted from binary session types where the split is: a = e, a = e.dual, a unrelated.
-/
