Payload and continuation branches of an endpoint action to Tree equivalence is a congruence for endpoint sending

InductivePayload and continuation branches of an endpoint action#✓fully proved

The two distinct children of an endpoint action.

inductive TypeBranch where
  | payload
  | continuation
  deriving DecidableEq

Used by 5

Used byTree-equivalent protocols have matching heads · Head-matching relations are bisimulations · Visible edge of a protocol tree after root unfolding · Root unfolding preserves protocol-tree edges · Labels of observable protocol-tree edges

InductiveLabels of observable protocol-tree edges#✓fully proved

Observable guarded tree edges. Endpoint metadata is never erased.

inductive TypeLabel where
  | sendName
  | recvName
  | sendEndpoint (role : Role) (rank : Nat) (branch : TypeBranch)
  | recvEndpoint (role : Role) (rank : Nat) (branch : TypeBranch)
  deriving DecidableEq

Uses 2 · Used by 11

Statement usesEndpoint role on a π name · Payload and continuation branches of an endpoint action

Used byCoinduction principle for protocol tree equivalence · Tree-equivalent protocols have matching heads · Head-matching relations are bisimulations · Labelled transition system of protocol-tree observations · Protocol tree equivalence is reflexive · Protocol tree equivalence is symmetric · Protocol tree equivalence is transitive · Regular-tree equivalence of protocols as bisimilarity · A protocol is tree-equivalent to its unfolding · Visible edge of a protocol tree after root unfolding · Root unfolding preserves protocol-tree edges

InductiveVisible edge of a protocol tree after root unfolding#✓fully proved

One visible tree edge obtained by the existing guarded root unfolding.

inductive TypeEdge : Protocol → TypeLabel → Protocol → Prop where
  | sendName {p s : Protocol} : p.unfold = .sendName s → TypeEdge p .sendName s
  | recvName {p s : Protocol} : p.unfold = .recvName s → TypeEdge p .recvName s
  | sendPayload {p t s : Protocol} {r : Role} {k : Nat} :
      p.unfold = .sendEndpoint r k t s → TypeEdge p (.sendEndpoint r k .payload) t
  | sendNext {p t s : Protocol} {r : Role} {k : Nat} :
      p.unfold = .sendEndpoint r k t s → TypeEdge p (.sendEndpoint r k .continuation) s
  | recvPayload {p t s : Protocol} {r : Role} {k : Nat} :
      p.unfold = .recvEndpoint r k t s → TypeEdge p (.recvEndpoint r k .payload) t
  | recvNext {p t s : Protocol} {r : Role} {k : Nat} :
      p.unfold = .recvEndpoint r k t s → TypeEdge p (.recvEndpoint r k .continuation) s

Uses 5 · Used by 5

Statement usesEndpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name · Payload and continuation branches of an endpoint action · Labels of observable protocol-tree edges

Used byTree-equivalent protocols have matching heads · Head-matching relations are bisimulations · Labelled transition system of protocol-tree observations · A protocol is tree-equivalent to its unfolding · Root unfolding preserves protocol-tree edges

DefinitionLabelled transition system of protocol-tree observations#✓fully proved

Canonical CSLib LTS instance for guarded type-tree observations only.

def protocolTree : Cslib.LTS Protocol TypeLabel := ⟨TypeEdge⟩

Uses 3 · Used by 8

Statement usesEndpoint protocol with guarded regular recursion · Visible edge of a protocol tree after root unfolding · Labels of observable protocol-tree edges

Used byCoinduction principle for protocol tree equivalence · Tree-equivalent protocols have matching heads · Head-matching relations are bisimulations · Protocol tree equivalence is reflexive · Protocol tree equivalence is symmetric · Protocol tree equivalence is transitive · Regular-tree equivalence of protocols as bisimilarity · A protocol is tree-equivalent to its unfolding

DefinitionRegular-tree equivalence of protocols as bisimilarity#✓fully proved

Equirecursive regular-tree equality is canonical strong bisimilarity, not equality of graph codes, cursors or finite constructor syntax.

def Protocol.TreeEquiv : Protocol → Protocol → Prop := Cslib.LTS.HomBisimilarity protocolTree

Uses 3 · Used by 68

Statement usesEndpoint protocol with guarded regular recursion · Labels of observable protocol-tree edges · Labelled transition system of protocol-tree observations

Used byOwnership-map equivalence preserves completion · Semantic advances of the recurring interface are the identity · Coinduction principle for protocol tree equivalence · Tree-equivalent protocols have matching heads · Tree equivalence is a congruence for name receiving · Protocol tree equivalence is reflexive · Tree equivalence is a congruence for endpoint sending · Tree equivalence is a congruence for name sending · Protocol tree equivalence is symmetric · Protocol tree equivalence is transitive · Characterization of tree equivalence by matching heads · A protocol is tree-equivalent to its unfolding · Unfolding both protocols preserves and reflects tree equivalence · Tree equivalence preserves completion of a protocol · Duality preserves protocol tree equivalence · Duality preserves capability equivalence · Equivalence of endpoint capabilities · Output typing at a code equivalent to one send then end · Tree equivalence is a congruence for endpoint receiving · Reflexivity of capability equivalence · Symmetry of capability equivalence · Transitivity of capability equivalence · Duality preserves and reflects protocol tree equivalence · Protocol tree equivalence is an equivalence relation · Tree equivalence of endpoint receives, componentwise · Tree equivalence of endpoint sends, componentwise · Peer of a passive send head has an equivalent receive head · Retyping along ownership-map equivalence · Endpoint delegation preserves conversion typing · Peer of an endpoint send head has an equivalent receive head · Head communication preserves conversion typing · Passive head communication preserves conversion typing · Minimum guard leaf cannot own an equivalent dual peer · Subject reduction at the empty interface · Conversion head communication yields a semantic advance · Head preservation for a conversion-ranked opposite pair · Progress for semantically balanced conversion frontiers · Endpoint head communication preserves conversion ranked typing · Passive head communication preserves conversion ranked typing · Equivalent contexts preserve the guard condition · Equivalent contexts preserve conversion ranked typing · Same-name conversion guards are opposite and communicate · Conversion ranked subject reduction at the empty interface · Equivalent retyping preserves invocation priority · Runtime typing transfers to an equivalent linear context · Endpoint head communication preserves runtime typing · Runtime head communication advances or keeps the interface · Runtime minimum guard leaf cannot own an equivalent dual peer · Passive head communication preserves runtime typing · Balanced runtime frontiers are idle or step given availability · Same-name linear guards at a compatible interface communicate · Subject reduction for runtime typing at the empty interface · Matching send and receive heads of two capabilities · Semantic advancement preserves balance · Semantic advancement preserves compatibility · Semantic advancement extends from the left part to the whole union · Typed head communication yields a semantic advancement · Lifting preserves semantic advancement · Literally dual capabilities have literally dual continuations · Semantic advancement preserves the context's domain · Raw dual advancement is a semantic advancement · Semantic advancement preserves capability ranks · Semantic advancement of a communicating endpoint pair · Communication heads give a send-head observation · Binder swapping preserves semantic advancement · Semantic advancement is raw under literal compatibility · Outer semantic advances lift past a private binding · Semantic advance under a private binding is private or outer

TheoremProtocol tree equivalence is reflexive#✓fully proved

Reflexivity comes from the canonical CSLib bisimilarity API.

theorem Protocol.TreeEquiv.refl (p : Protocol) : p.TreeEquiv p

Uses 4 · Used by 3

Statement usesEndpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity

Proof usesLabels of observable protocol-tree edges · Labelled transition system of protocol-tree observations

Used byReflexivity of capability equivalence · Protocol tree equivalence is an equivalence relation · Raw dual advancement is a semantic advancement

TheoremProtocol tree equivalence is symmetric#✓fully proved

Symmetry comes from the canonical CSLib bisimilarity API.

theorem Protocol.TreeEquiv.symm {p q : Protocol} (h : p.TreeEquiv q) : q.TreeEquiv p

Uses 4 · Used by 9

Statement usesEndpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity

Proof usesLabels of observable protocol-tree edges · Labelled transition system of protocol-tree observations

Used byUnfolding both protocols preserves and reflects tree equivalence · Tree equivalence preserves completion of a protocol · Symmetry of capability equivalence · Protocol tree equivalence is an equivalence relation · Peer of a passive send head has an equivalent receive head · Endpoint delegation preserves conversion typing · Peer of an endpoint send head has an equivalent receive head · Endpoint head communication preserves conversion ranked typing · Endpoint head communication preserves runtime typing

TheoremProtocol tree equivalence is transitive#✓fully proved

Transitivity comes from composition of canonical CSLib bisimulations.

theorem Protocol.TreeEquiv.trans {p q r : Protocol} (h : p.TreeEquiv q)
    (h' : q.TreeEquiv r) : p.TreeEquiv r

Uses 4 · Used by 3

Statement usesEndpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity

Proof usesLabels of observable protocol-tree edges · Labelled transition system of protocol-tree observations

Used byUnfolding both protocols preserves and reflects tree equivalence · Transitivity of capability equivalence · Protocol tree equivalence is an equivalence relation

TheoremRoot unfolding preserves protocol-tree edges#✓fully proved

Root unfolding exposes exactly the same observation edges.

theorem typeEdge_unfold {p q : Protocol} {l : TypeLabel} :
    TypeEdge p.unfold l q ↔ TypeEdge p l q

Uses 7 · Used by 1

Statement usesEndpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Visible edge of a protocol tree after root unfolding · Labels of observable protocol-tree edges

Proof usesProtocol unfolding is idempotent · Endpoint role on a π name · Payload and continuation branches of an endpoint action

Used byA protocol is tree-equivalent to its unfolding

TheoremA protocol is tree-equivalent to its unfolding#✓fully proved

One unfolding is semantically equivalent even though its code changes.

theorem Protocol.treeEquiv_unfold (p : Protocol) : p.TreeEquiv p.unfold

Uses 7 · Used by 1

Statement usesEndpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · One-step unfolding of a protocol

Proof usesVisible edge of a protocol tree after root unfolding · Labels of observable protocol-tree edges · Labelled transition system of protocol-tree observations · Root unfolding preserves protocol-tree edges

Used byUnfolding both protocols preserves and reflects tree equivalence

InductiveHead and branch matching of protocols up to a child relation#✓fully proved

Exact head and branch correspondence for a relation on child trees. Payload and continuation are related separately; only metadata is literal.

inductive HeadMatch (R : Protocol → Protocol → Prop) : Protocol → Protocol → Prop where
  | done : HeadMatch R .done .done
  | sendName {s t : Protocol} : R s t → HeadMatch R (.sendName s) (.sendName t)
  | recvName {s t : Protocol} : R s t → HeadMatch R (.recvName s) (.recvName t)
  | sendEndpoint {r : Role} {k : Nat} {p q s t : Protocol} :
      R p q → R s t → HeadMatch R (.sendEndpoint r k p s) (.sendEndpoint r k q t)
  | recvEndpoint {r : Role} {k : Nat} {p q s t : Protocol} :
      R p q → R s t → HeadMatch R (.recvEndpoint r k p s) (.recvEndpoint r k q t)

Uses 2 · Used by 21

Statement usesEndpoint protocol with guarded regular recursion · Endpoint role on a π name

Used byCoinduction principle for protocol tree equivalence · Tree-equivalent protocols have matching heads · Head-matching relations are bisimulations · Head matching is monotone in the child relation · Tree equivalence is a congruence for name receiving · Tree equivalence is a congruence for endpoint sending · Tree equivalence is a congruence for name sending · Characterization of tree equivalence by matching heads · Tree equivalence preserves completion of a protocol · Head matching transfers to dual protocols · Duality preserves protocol tree equivalence · Output typing at a code equivalent to one send then end · Tree equivalence is a congruence for endpoint receiving · Tree equivalence of endpoint receives, componentwise · Tree equivalence of endpoint sends, componentwise · Peer of a passive send head has an equivalent receive head · Retyping along ownership-map equivalence · Peer of an endpoint send head has an equivalent receive head · Equivalent contexts preserve conversion ranked typing · Runtime typing transfers to an equivalent linear context · Same-name linear guards at a compatible interface communicate

TheoremHead matching is monotone in the child relation#✓fully proved

Head matching is monotone in the child relation.

theorem HeadMatch.mono {R S : Protocol → Protocol → Prop} {p q : Protocol}
    (h : HeadMatch R p q) (hrs : ∀ a b, R a b → S a b) : HeadMatch S p q

Uses 3 · Used by 2

Statement usesHead and branch matching of protocols up to a child relation · Endpoint protocol with guarded regular recursion

Proof usesEndpoint role on a π name

Used byCharacterization of tree equivalence by matching heads · Duality preserves protocol tree equivalence

TheoremHead-matching relations are bisimulations#✓fully proved

A relation matching literal unfolded heads and both child branches is a canonical CSLib bisimulation. This is the coinductive proof rule, not an axiom.

theorem headMatch_isBisimulation {R : Protocol → Protocol → Prop}
    (hR : ∀ p q, R p q → HeadMatch R p.unfold q.unfold) :
    Cslib.LTS.IsBisimulation protocolTree protocolTree R

Uses 9 · Used by 1

Statement usesHead and branch matching of protocols up to a child relation · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Labels of observable protocol-tree edges · Labelled transition system of protocol-tree observations

Proof usesFinite guarded regular protocol graph · Endpoint role on a π name · Payload and continuation branches of an endpoint action · Visible edge of a protocol tree after root unfolding

Used byCoinduction principle for protocol tree equivalence

TheoremTree-equivalent protocols have matching heads#✓fully proved

Canonical bisimilarity determines literal head metadata and both semantically equivalent child branches. No graph-code equality is required.

theorem Protocol.TreeEquiv.head {p q : Protocol} (h : p.TreeEquiv q) :
    HeadMatch Protocol.TreeEquiv p.unfold q.unfold

Uses 11 · Used by 12

Statement usesHead and branch matching of protocols up to a child relation · Endpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · One-step unfolding of a protocol

Proof usesFinite guarded regular protocol graph · Unfolding never yields a regular-cursor protocol · Endpoint role on a π name · Payload and continuation branches of an endpoint action · Visible edge of a protocol tree after root unfolding · Labels of observable protocol-tree edges · Labelled transition system of protocol-tree observations

Used byCharacterization of tree equivalence by matching heads · Tree equivalence preserves completion of a protocol · Duality preserves protocol tree equivalence · Output typing at a code equivalent to one send then end · Tree equivalence of endpoint receives, componentwise · Tree equivalence of endpoint sends, componentwise · Peer of a passive send head has an equivalent receive head · Retyping along ownership-map equivalence · Peer of an endpoint send head has an equivalent receive head · Equivalent contexts preserve conversion ranked typing · Runtime typing transfers to an equivalent linear context · Same-name linear guards at a compatible interface communicate

TheoremCoinduction principle for protocol tree equivalence#✓fully proved

Coinduction on an explicitly supplied tree relation, checked by CSLib.

theorem Protocol.TreeEquiv.coind {R : Protocol → Protocol → Prop}
    (hR : ∀ a b, R a b → HeadMatch R a.unfold b.unfold) {p q : Protocol}
    (hpq : R p q) : p.TreeEquiv q

Uses 7 · Used by 2

Statement usesHead and branch matching of protocols up to a child relation · Endpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · One-step unfolding of a protocol

Proof usesLabels of observable protocol-tree edges · Head-matching relations are bisimulations · Labelled transition system of protocol-tree observations

Used byCharacterization of tree equivalence by matching heads · Duality preserves protocol tree equivalence

TheoremCharacterization of tree equivalence by matching heads#✓fully proved

Exact semantic root/branch characterization, in BOTH directions.

theorem Protocol.treeEquiv_iff_head {p q : Protocol} :
    p.TreeEquiv q ↔ HeadMatch Protocol.TreeEquiv p.unfold q.unfold

Uses 7 · Used by 4

Statement usesHead and branch matching of protocols up to a child relation · Endpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · One-step unfolding of a protocol

Proof usesHead matching is monotone in the child relation · Coinduction principle for protocol tree equivalence · Tree-equivalent protocols have matching heads

Used byTree equivalence is a congruence for name receiving · Tree equivalence is a congruence for endpoint sending · Tree equivalence is a congruence for name sending · Tree equivalence is a congruence for endpoint receiving

TheoremUnfolding both protocols preserves and reflects tree equivalence#✓fully proved

Unfolding on either or both sides leaves the regular tree unchanged.

theorem Protocol.treeEquiv_unfold_iff {p q : Protocol} :
    p.unfold.TreeEquiv q.unfold ↔ p.TreeEquiv q

Uses 6

Statement usesEndpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · One-step unfolding of a protocol

Proof usesProtocol tree equivalence is symmetric · Protocol tree equivalence is transitive · A protocol is tree-equivalent to its unfolding

TheoremTree equivalence is a congruence for name sending#✓fully proved

Constructor congruence matches same-direction name continuations.

theorem Protocol.TreeEquiv.sendName {p q : Protocol} (h : p.TreeEquiv q) :
    (Protocol.sendName p).TreeEquiv (.sendName q)

Uses 5

Statement usesEndpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity

Proof usesHead and branch matching of protocols up to a child relation · Characterization of tree equivalence by matching heads · One-step unfolding of a protocol

TheoremTree equivalence is a congruence for name receiving#✓fully proved

Constructor congruence also matches input direction separately.

theorem Protocol.TreeEquiv.recvName {p q : Protocol} (h : p.TreeEquiv q) :
    (Protocol.recvName p).TreeEquiv (.recvName q)

Uses 5

Statement usesEndpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity

Proof usesHead and branch matching of protocols up to a child relation · Characterization of tree equivalence by matching heads · One-step unfolding of a protocol

TheoremTree equivalence is a congruence for endpoint sending#✓fully proved

Payload and continuation congruence do not conflate the two branches.

theorem Protocol.TreeEquiv.sendEndpoint {p q s t : Protocol} (hp : p.TreeEquiv q)
    (hs : s.TreeEquiv t) (r : Role) (k : Nat) :
    (Protocol.sendEndpoint r k p s).TreeEquiv (.sendEndpoint r k q t)

Uses 6 · Used by 1

Statement usesEndpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Endpoint role on a π name

Proof usesHead and branch matching of protocols up to a child relation · Characterization of tree equivalence by matching heads · One-step unfolding of a protocol

Used byTree equivalence of endpoint sends, componentwise

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.