Tree equivalence is a congruence for endpoint receiving to Conversion-typed processes are well scoped

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

Endpoint receive congruence preserves literal role/rank metadata.

theorem Protocol.TreeEquiv.recvEndpoint {p q s t : Protocol} (hp : p.TreeEquiv q)
    (hs : s.TreeEquiv t) (r : Role) (k : Nat) :
    (Protocol.recvEndpoint r k p s).TreeEquiv (.recvEndpoint 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 receives, componentwise

TheoremHead matching transfers to dual protocols#✓fully proved

Dualizing a head changes subject direction and continuation orientation, but leaves payload orientation and role/rank metadata untouched.

theorem HeadMatch.dual {R S : Protocol → Protocol → Prop} {p q : Protocol}
    (h : HeadMatch R p q) (hpayload : ∀ a b, R a b → S a b)
    (hnext : ∀ a b, R a b → S a.dual b.dual) : HeadMatch S p.dual q.dual
Uses 4 · Used by 1
Statement usesHead and branch matching of protocols up to a child relation · Endpoint protocol with guarded regular recursion · Dual of an endpoint protocol
Proof usesEndpoint role on a π name
Used byDuality preserves protocol tree equivalence

TheoremDuality preserves protocol tree equivalence#✓fully proved

Semantic equivalence is preserved by actual protocol duality, including recursive payloads with independently chosen orientation.

theorem Protocol.TreeEquiv.dual {p q : Protocol} (h : p.TreeEquiv q) :
    p.dual.TreeEquiv q.dual
Uses 10 · Used by 2
Statement usesEndpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Dual of an endpoint protocol
Proof usesHead and branch matching of protocols up to a child relation · Head matching transfers to dual protocols · Head matching is monotone in the child relation · Coinduction principle for protocol tree equivalence · Tree-equivalent protocols have matching heads · One-step unfolding of a protocol · Unfolding commutes with protocol duality
Used byDuality preserves capability equivalence · Duality preserves and reflects protocol tree equivalence

TheoremDuality preserves and reflects protocol tree equivalence#✓fully proved

Duality both preserves and reflects equivalence, not only one direction.

theorem Protocol.treeEquiv_dual_iff {p q : Protocol} :
    p.dual.TreeEquiv q.dual ↔ p.TreeEquiv q
Uses 5
Statement usesEndpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Dual of an endpoint protocol
Proof usesDuality preserves protocol tree equivalence · Protocol duality is an involution

TheoremProtocol tree equivalence is an equivalence relation#✓fully proved

The semantic type relation is a genuine equivalence relation.

theorem Protocol.treeEquiv_equivalence : Equivalence Protocol.TreeEquiv
Uses 5
Statement usesEndpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity
Proof usesProtocol tree equivalence is reflexive · Protocol tree equivalence is symmetric · Protocol tree equivalence is transitive

TheoremTree equivalence of endpoint sends, componentwise#✓fully proved

Exact endpoint-send characterization exposes literal metadata equality and separate semantic payload/continuation equivalences for conversion.

theorem Protocol.treeEquiv_sendEndpoint_iff {r r' : Role} {k k' : Nat}
    {p q s t : Protocol} :
    (Protocol.sendEndpoint r k p s).TreeEquiv (.sendEndpoint r' k' q t) ↔
      r = r' ∧ k = k' ∧ p.TreeEquiv q ∧ s.TreeEquiv t
Uses 8
Statement usesEndpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Endpoint role on a π name
Proof usesFinite guarded regular protocol graph · Head and branch matching of protocols up to a child relation · Tree-equivalent protocols have matching heads · Tree equivalence is a congruence for endpoint sending · One-step unfolding of a protocol

TheoremTree equivalence of endpoint receives, componentwise#✓fully proved

Receive characterization preserves the same independent payload metadata.

theorem Protocol.treeEquiv_recvEndpoint_iff {r r' : Role} {k k' : Nat}
    {p q s t : Protocol} :
    (Protocol.recvEndpoint r k p s).TreeEquiv (.recvEndpoint r' k' q t) ↔
      r = r' ∧ k = k' ∧ p.TreeEquiv q ∧ s.TreeEquiv t
Uses 8
Statement usesEndpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Endpoint role on a π name
Proof usesFinite guarded regular protocol graph · Head and branch matching of protocols up to a child relation · Tree-equivalent protocols have matching heads · Tree equivalence is a congruence for endpoint receiving · One-step unfolding of a protocol

TheoremTree equivalence preserves completion of a protocol#✓fully proved

Activity/completion is invariant under semantic type equivalence.

theorem Protocol.TreeEquiv.done_iff {p q : Protocol} (h : p.TreeEquiv q) :
    p.unfold = .done ↔ q.unfold = .done
Uses 8 · Used by 8
Statement usesEndpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · One-step unfolding of a protocol
Proof usesFinite guarded regular protocol graph · Head and branch matching of protocols up to a child relation · Tree-equivalent protocols have matching heads · Protocol tree equivalence is symmetric · Endpoint role on a π name
Used byOwnership-map equivalence preserves completion · Output typing at a code equivalent to one send then end · Minimum guard leaf cannot own an equivalent dual peer · Progress for semantically balanced conversion frontiers · Equivalent contexts preserve the guard condition · Equivalent retyping preserves invocation priority · Runtime minimum guard leaf cannot own an equivalent dual peer · Balanced runtime frontiers are idle or step given availability

DefinitionEquivalence of endpoint capabilities#✓fully proved

Capability equivalence explicitly retains the enclosing capability rank, which is not an observation of Protocol.TreeEquiv.

def Capability.Equivalent (c d : Capability) : Prop :=
  c.rank = d.rank ∧ c.protocol.TreeEquiv d.protocol
Uses 3 · Used by 136
Statement usesEndpoint capability with a dependency rank · Endpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity
Used byBinding equivalent fresh pairs preserves ownership-map equivalence · Ownership-map equivalence preserves semantic compatibility · Ownership-map equivalence preserves completion · Pointwise equivalence of ownership maps · Erasure preserves ownership-map equivalence · Equivalent insertions preserve ownership-map equivalence · Lifting preserves ownership-map equivalence · Lookups transfer along ownership-map equivalence · Equivalent ownership maps have the same keys · Ownership-map equivalence from two-way lookup correspondence · Equivalence of a union restricts to its left part · Reflexivity of ownership-map equivalence · Equivalent capabilities give equivalent singleton maps · Symmetry of ownership-map equivalence · Transitivity of ownership-map equivalence · Union preserves ownership-map equivalence · The receiver reentry request is runtime-typed · Semantic advances of the recurring interface are the identity · The recurring interface is balanced · The sender reentry request is runtime-typed · Conversion-typed processes are well scoped · Semantic peer compatibility of an ownership map · Syntactic compatibility implies semantic compatibility · Duality preserves capability equivalence · Conversion-enabled endpoint typing judgement · Base endpoint typing embeds into conversion typing · Output inversion for conversion typing · Reflexivity of capability equivalence · Symmetry of capability equivalence · Transitivity of capability equivalence · Owned capabilities with absent names are completed · Communicating subjects have semantically dual capabilities · Erasing a role with an absent name preserves typing · Conversion-typed processes have no sum or replication · Nil inversion for conversion typing · Restriction inversion for conversion typing · Parallel inversion for conversion typing · Peer of a passive send head has an equivalent receive head · Collision-free renaming preserves conversion typing · Retyping along ownership-map equivalence · Endpoint substitution preserves conversion typing · Endpoint substitution with freshness from a disjoint split · Weakening conversion typing by a completed capability · Endpoint delegation preserves conversion typing · Peer of an endpoint send head has an equivalent receive head · Head communication preserves conversion typing · Input inversion for conversion typing · Passive head communication preserves conversion typing · Structural congruence preserves conversion typing · Erasing a key whose name is absent preserves conversion ranked typing · Forgetting priorities yields conversion typing · Conversion-ranked input subjects are active · Minimum guard leaf cannot own an equivalent dual peer · Restriction inversion for conversion ranked typing · Ranked typing embeds into conversion ranked typing · Conversion-ranked output subjects are active · Parallel inversion for conversion ranked typing · Priority-ranked conversion typing judgement · Subject reduction at the empty interface · Weakening conversion ranked typing by a completed capability · Conversion head communication yields a semantic advance · Head preservation for a conversion-ranked opposite pair · Inversion of conversion-ranked input typing · Progress for semantically balanced conversion frontiers · Endpoint head communication preserves conversion ranked typing · Passive head communication preserves conversion ranked typing · Collision-free renaming preserves conversion ranked typing · Equivalent contexts preserve the guard condition · Equivalent contexts preserve conversion ranked typing · Same-name conversion guards are opposite and communicate · Endpoint substitution preserves conversion ranked typing · Split-derived freshness for conversion endpoint substitution · Structural congruence preserves conversion ranked typing · Conversion ranked subject reduction at the empty interface · Inversion of runtime typing for input on a shared name · Runtime-typed processes are scoped at the ambient depth · Environment extension preserves runtime typing under separation · Runtime typing with guarded shared replication · Output on a declared shared name is a service invocation · Inversion of runtime typing for the nil process · Inversion of runtime typing for restriction · Finite ranked typing embeds into runtime typing under separation · Output subjects are owned endpoints or declared shared names · Inversion of runtime typing for parallel composition · Typed replication has a body with empty ownership · Replicated runtime processes have completed ownership · Runtime typing separates owned names from shared services · Owned names absent from a runtime process are completed · Erasing a key whose name is absent preserves runtime typing · Each owned key of a runtime typing is scoped at ambient depth · Inversion of runtime typing for replication · Equivalent retyping preserves separation from shared names · Equivalent retyping preserves invocation priority · Runtime typing transfers to an equivalent linear context · Typed service templates own only completed entries · Typed service templates retype at any well-formed completed context · Weakening runtime typing by one fresh completed entry · Structural congruence preserves runtime typing · Runtime typing under renamings that fix and avoid shared names · Runtime typing under substitution of a transmitted endpoint · Endpoint substitution with side conditions derived from a split · Request-free completed runtime frontiers are service templates · Endpoint head communication preserves runtime typing · Runtime head communication advances or keeps the interface · Runtime inputs are active linear or have completed ownership · Inversion of runtime input on a nonshared subject · Request-free runtime outputs have an active linear subject · Runtime minimum guard leaf cannot own an equivalent dual peer · Passive head communication preserves runtime typing · Shared invocation and input worker preserve the combined interface · Runtime-typed processes are congruent to a guarded normal form · Balanced runtime frontiers are idle or step given availability · Same-name linear guards at a compatible interface communicate · Choice selection is the identity on runtime-typed processes · Subject reduction for runtime typing at the empty interface · Semantic balance of a linear context · Semantic advancement preserves balance · The empty context is semantically balanced · Raw balance implies semantic balance · Semantic balance implies semantic compatibility · 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 · 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 · Binder swapping preserves semantic advancement · Semantic advancement is raw under literal compatibility · Binding a dual private pair preserves compatibility · Binding a dual private pair preserves balance · Outer semantic advances lift past a private binding · Semantic advance under a private binding is private or outer · Equivalent retyping preserves semantic balance · Union of disjoint balanced contexts is balanced

TheoremReflexivity of capability equivalence#✓fully proved

Reflexivity retains rank and the exact protocol tree.

theorem Capability.Equivalent.refl (c : Capability) : c.Equivalent c
Uses 5 · Used by 14
Statement usesEndpoint capability with a dependency rank · Equivalence of endpoint capabilities
Proof usesEndpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Protocol tree equivalence is reflexive
Used byReflexivity of ownership-map equivalence · The receiver reentry request is runtime-typed · The recurring interface is balanced · The sender reentry request is runtime-typed · Syntactic compatibility implies semantic compatibility · Base endpoint typing embeds into conversion typing · Retyping along ownership-map equivalence · Ranked typing embeds into conversion ranked typing · Equivalent contexts preserve conversion ranked typing · Runtime typing transfers to an equivalent linear context · Raw balance implies semantic balance · Raw dual advancement is a semantic advancement · Binding a dual private pair preserves compatibility · Binding a dual private pair preserves balance

TheoremSymmetry of capability equivalence#✓fully proved

Symmetry preserves the separately required rank equality.

theorem Capability.Equivalent.symm {c d : Capability} (h : c.Equivalent d) :
    d.Equivalent c
Uses 5 · Used by 12
Statement usesEndpoint capability with a dependency rank · Equivalence of endpoint capabilities
Proof usesEndpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Protocol tree equivalence is symmetric
Used byOwnership-map equivalence preserves semantic compatibility · Lifting preserves ownership-map equivalence · Symmetry of ownership-map equivalence · Retyping along ownership-map equivalence · Endpoint substitution preserves conversion typing · Equivalent contexts preserve conversion ranked typing · Endpoint substitution preserves conversion ranked typing · Runtime typing transfers to an equivalent linear context · Runtime typing under substitution of a transmitted endpoint · Semantic advancement preserves balance · Semantic advancement preserves compatibility · Equivalent retyping preserves semantic balance

TheoremTransitivity of capability equivalence#✓fully proved

Transitivity composes rank equality and regular-tree equivalence.

theorem Capability.Equivalent.trans {c d e : Capability} (h : c.Equivalent d)
    (h' : d.Equivalent e) : c.Equivalent e
Uses 5 · Used by 9
Statement usesEndpoint capability with a dependency rank · Equivalence of endpoint capabilities
Proof usesEndpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Protocol tree equivalence is transitive
Used byOwnership-map equivalence preserves semantic compatibility · Transitivity of ownership-map equivalence · Retyping along ownership-map equivalence · Endpoint delegation preserves conversion typing · Endpoint head communication preserves conversion ranked typing · Equivalent contexts preserve conversion ranked typing · Runtime typing transfers to an equivalent linear context · Endpoint head communication preserves runtime typing · Equivalent retyping preserves semantic balance

TheoremDuality preserves capability equivalence#✓fully proved

Duality retains the separate rank and preserves protocol-tree equivalence.

theorem Capability.Equivalent.dual {c d : Capability} (h : c.Equivalent d) :
    c.dual.Equivalent d.dual
Uses 6 · Used by 7
Statement usesEndpoint capability with a dependency rank · Equivalence of endpoint capabilities · Dual of an endpoint capability
Proof usesEndpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Duality preserves protocol tree equivalence
Used byBinding equivalent fresh pairs preserves ownership-map equivalence · Ownership-map equivalence preserves semantic compatibility · Same-name conversion guards are opposite and communicate · Same-name linear guards at a compatible interface communicate · Semantic advancement preserves balance · Semantic advancement preserves compatibility · Equivalent retyping preserves semantic balance

DefinitionSemantic peer compatibility of an ownership map#✓fully proved

Semantic peer compatibility keeps actual capability ranks equal and compares dual protocol trees, not merely their direction or payload metadata.

def Compatible (Δ : Context) : Prop :=
  ∀ e c d, Δ.lookup e = some c → Δ.lookup e.opposite = some d → d.Equivalent c.dual
Uses 8 · Used by 39
Statement usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Equivalence of endpoint capabilities · Dual of an endpoint capability · Finite endpoint ownership map · Polarized endpoint key · Peer endpoint key · Endpoint role on a π name
Used byOwnership-map equivalence preserves semantic compatibility · Each next phase is typed by subject reduction · Every phase is typed by preservation from the pending state · Steps preserve typing at the recurring interface · Syntactic compatibility implies semantic compatibility · Communicating subjects have semantically dual capabilities · Endpoint delegation preserves conversion typing · Head communication preserves conversion typing · Passive head communication preserves conversion typing · Typing and compatibility persist along finite executions · Subject reduction at a compatible conversion interface · Subject reduction at a balanced interface · 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 · Same-name conversion guards are opposite and communicate · Finite runs keep conversion ranked typing at compatible interfaces · Conversion ranked subject reduction at compatible interfaces · Conversion ranked subject reduction at balanced interfaces · Conversion ranked subject reduction at the empty interface · Endpoint head communication preserves runtime typing · Runtime head communication advances or keeps the interface · Passive head communication preserves runtime typing · Balanced runtime frontiers are idle or step given availability · Multi-step subject reduction at compatible interfaces · Multi-step subject reduction at balanced interfaces · Same-name linear guards at a compatible interface communicate · Subject reduction for runtime typing at compatible interfaces · Subject reduction for runtime typing at balanced interfaces · Subject reduction for runtime typing at the empty interface · Semantic balance implies semantic compatibility · Semantic advancement preserves compatibility · Typed head communication yields a semantic advancement · Binding a dual private pair preserves compatibility · Compatibility restricts to the left part of a union · Compatibility restricts to the right part of a disjoint union

TheoremSyntactic compatibility implies semantic compatibility#✓fully proved

Old syntactic peer compatibility implies the semantic condition.

theorem compatible_of_raw {Δ : Context} (h : Endpoint.Compatible Δ) : Compatible Δ
Uses 11
Statement usesCompatibility of a partial endpoint interface · Finite endpoint ownership map · Semantic peer compatibility of an ownership map
Proof usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Equivalence of endpoint capabilities · Reflexivity of capability equivalence · Dual of an endpoint capability · Polarized endpoint key · Peer endpoint key · Endpoint role on a π name

InductiveConversion-enabled endpoint typing judgement#✓fully proved

Seven syntax-directed rules. No readiness, Step, retyping, preservation or consistent raw representative is a typing premise. Endpoint input installs its actual advertised code; endpoint output transfers the actual owned slot.

Cslib.SessionTypes.Endpoint.Conversion.HasType · 32 lines 
inductive HasType : Nat → Context → Proc → Prop where
  | nil {n : Nat} {Δ : Context} :
      Δ.Completed → (∀ e ∈ Δ, e.name.ClosedAt n) → HasType n Δ .nil
  | outName {n : Nat} {Δ : Context} {e : Key} {c : Capability}
      {b : Name} {s : Protocol} {p : Proc} :
      Δ.lookup e = some c → c.protocol.unfold = .sendName s →
      e.name.ClosedAt n → b.ClosedAt n →
      HasType n (Δ.insert e ⟨c.rank, s⟩) p → HasType n Δ (.out e.name b p)
  | inpName {n : Nat} {Δ : Context} {e : Key} {c : Capability}
      {s : Protocol} {p : Proc} :
      Δ.lookup e = some c → c.protocol.unfold = .recvName s → e.name.ClosedAt n →
      HasType (n + 1) (Context.lift 0 (Δ.insert e ⟨c.rank, s⟩)) p →
      HasType n Δ (.inp e.name p)
  | outEndpoint {n : Nat} {Δ : Context} {e d : Key} {c v : Capability}
      {k : Nat} {t s : Protocol} {p : Proc} :
      Δ.lookup e = some c → c.protocol.unfold = .sendEndpoint d.role k t s →
      Δ.lookup d = some v → v.Equivalent ⟨k, t⟩ → e ≠ d →
      e.name.ClosedAt n → d.name.ClosedAt n →
      HasType n ((Δ.erase d).insert e ⟨c.rank, s⟩) p →
      HasType n Δ (.out e.name d.name p)
  | inpEndpoint {n : Nat} {Δ : Context} {e : Key} {c : Capability}
      {r : Role} {k : Nat} {t s : Protocol} {p : Proc} :
      Δ.lookup e = some c → c.protocol.unfold = .recvEndpoint r k t s →
      e.name.ClosedAt n →
      HasType (n + 1)
        ((Context.lift 0 (Δ.insert e ⟨c.rank, s⟩)).insert ⟨.var 0, r⟩ ⟨k, t⟩) p →
      HasType n Δ (.inp e.name p)
  | par {n : Nat} {Δ Θ : Context} {p q : Proc} :
      Finmap.Disjoint Δ Θ → HasType n Δ p → HasType n Θ q →
      HasType n (Δ ∪ Θ) (.par p q)
  | nu {n : Nat} {Δ : Context} {c : Capability} {p : Proc} :
      HasType (n + 1) (Context.bind c Δ) p → HasType n Δ (.nu p)
Uses 13 · Used by 50
Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Processes of the π-calculus · Endpoint capability with a dependency rank · Equivalence of endpoint capabilities · Finite endpoint ownership map · Completed ownership map · Binding a fresh dual pair under restriction · Lifting an ownership map past a binder · Polarized endpoint key · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name
Used byConversion-typed processes are well scoped · Base endpoint typing embeds into conversion typing · Output typing at a code equivalent to one send then end · Output inversion for conversion typing · Owned capabilities with absent names are completed · Erasing a role with an absent name preserves typing · Conversion-typed processes have no sum or replication · Lifting past a binder preserves conversion typing · Typed nil admits a completed scoped capability · Nil inversion for conversion typing · Restriction inversion for conversion typing · Parallel inversion for conversion typing · Removing a parallel nil preserves conversion typing · Collision-free renaming preserves conversion typing · Retyping along ownership-map equivalence · Ownership-map equivalence preserves typing in both directions · Endpoint substitution preserves conversion typing · Endpoint substitution with freshness from a disjoint split · Passive name substitution preserves conversion typing · Swapping adjacent binders preserves conversion typing · Weakening conversion typing by a completed capability · Weakening conversion typing by a disjoint completed context · Endpoint delegation preserves conversion typing · Head communication preserves conversion typing · Input inversion for conversion typing · Adding a role unused by the partner preserves conversion typing · Removing a restriction around nil preserves conversion typing · Adding a restriction around nil preserves conversion typing · Swapping nested restrictions preserves conversion typing · Parallel reassociation preserves conversion typing · Reverse parallel reassociation preserves conversion typing · Parallel commutation preserves conversion typing · Adding a parallel nil preserves conversion typing · Passive head communication preserves conversion typing · Restoring the bound pair to the restricted component · Forward scope extrusion preserves conversion typing · Scope extrusion preserves conversion typing in both directions · Reverse scope extrusion preserves conversion typing · Lowering a lifted process preserves conversion typing · Structural congruence preserves conversion typing · Forgetting priorities yields conversion typing · Nil typing lifts to conversion ranked typing · Reverse restriction swap preserves conversion typing · Typing and compatibility persist along finite executions · Empty-interface typing persists along finite executions · Subject reduction at a compatible conversion interface · Subject reduction at a balanced interface · Subject reduction at the empty interface · Restricting nil preserves conversion ranked typing · Typed head communication yields a semantic advancement

TheoremBase endpoint typing embeds into conversion typing#✓fully proved

Actual seven-rule induction embeds the raw judgement. This does not transport the raw judgement's substitution or progress theorem to new terms.

theorem HasType.of_raw {n : Nat} {Δ : Context} {p : Proc}
    (h : Endpoint.HasType n Δ p) : HasType n Δ p
Uses 16
Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Conversion-enabled endpoint typing judgement · Linear endpoint typing of π-calculus processes
Proof usesChannel name in the π-calculus · Name scoped at a binder depth · Endpoint capability with a dependency rank · Equivalence of endpoint capabilities · Reflexivity of capability equivalence · Completed ownership map · Binding a fresh dual pair under restriction · Lifting an ownership map past a binder · Polarized endpoint key · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name

TheoremOutput typing at a code equivalent to one send then end#✓fully proved

Local finite-tail conversion: replacing a one-send-then-end protocol by an equivalent code yields a usable output subject, retaining its actual next code and rank. This is not arbitrary context retyping.

theorem one_action_tail {n k : Nat} {Γ : Context} {d : Key} {b : Name} {t : Protocol}
    (hc : Γ.Completed) (hscope : ∀ e ∈ Γ, e.name.ClosedAt n)
    (hd : d.name.ClosedAt n) (hb : b.ClosedAt n)
    (ht : (Protocol.sendName .done).TreeEquiv t) :
    HasType n (Γ.insert d ⟨k, t⟩) (.out d.name b .nil)
Uses 17
Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Processes of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Completed ownership map · Conversion-enabled endpoint typing judgement · Polarized endpoint key · Endpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Endpoint role on a π name
Proof usesInserting a completed capability preserves completion · Finite guarded regular protocol graph · Head and branch matching of protocols up to a child relation · Tree equivalence preserves completion of a protocol · Tree-equivalent protocols have matching heads · One-step unfolding of a protocol

TheoremOutput inversion for conversion typing#✓fully proved

Conversion output inversion exposes actual owned payload metadata and semantic comparison, never a supplied retyping result.

theorem HasType.out_inv {n : Nat} {Δ : Context} {a b : Name} {p : Proc}
    (h : HasType n Δ (.out a b p)) :
    ∃ e c, e.name = a ∧ Δ.lookup e = some c ∧
      ((∃ s, c.protocol.unfold = .sendName s) ∨
       ∃ d v k t s, d.name = b ∧ Δ.lookup d = some v ∧
         c.protocol.unfold = .sendEndpoint d.role k t s ∧ v.Equivalent ⟨k, t⟩)
Uses 14 · Used by 1
Statement usesChannel name in the π-calculus · Processes of the π-calculus · Endpoint capability with a dependency rank · Equivalence of endpoint capabilities · Finite endpoint ownership map · Conversion-enabled endpoint typing judgement · Polarized endpoint key · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name
Proof usesName scoped at a binder depth · Completed ownership map · Binding a fresh dual pair under restriction · Lifting an ownership map past a binder
Used bySame-name conversion guards are opposite and communicate

TheoremConversion-typed processes are well scoped#✓fully proved

Canonical scope follows from the seven conversion rules.

theorem HasType.closedAt {n : Nat} {Δ : Context} {p : Proc} (h : HasType n Δ p) : p.ClosedAt n
Uses 15
Statement usesProcesses of the π-calculus · Locally closed processes at a binder depth · Finite endpoint ownership map · Conversion-enabled endpoint typing judgement
Proof usesChannel name in the π-calculus · Name scoped at a binder depth · Endpoint capability with a dependency rank · Equivalence of endpoint capabilities · Completed ownership map · Binding a fresh dual pair under restriction · Lifting an ownership map past a binder · Polarized endpoint key · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name
20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.