Reverse restriction swap preserves conversion typing to Erasing a key whose name is absent preserves conversion ranked typing

TheoremReverse restriction swap preserves conversion typing#✓fully proved

Reverse nested restriction commutation uses the canonical involution.

theorem HasType.nu_swap_reverse {n : Nat} {Δ : Context} {p : Proc}
    (h : HasType n Δ (.nu (.nu (swapProc 0 p)))) : HasType n Δ (.nu (.nu p))

Uses 6 · Used by 1

Statement usesProcesses of the π-calculus · Swapping adjacent binders throughout a process · Finite endpoint ownership map · Conversion-enabled endpoint typing judgement

Proof usesSwapping nested restrictions preserves conversion typing · Process swap is an involution

Used byStructural congruence preserves conversion typing

TheoremStructural congruence preserves conversion typing#✓fully proved

Every existing canonical structural congruence preserves endpoint typing in both directions with exactly the same depth and ownership. Unsupported choice/replication shapes are rejected by the typing-derived finite invariant.

theorem HasType.cong_iff {n : Nat} {Δ : Context} {p q : Proc} (hc : Cong p q) :
    HasType n Δ p ↔ HasType n Δ q

Uses 31 · Used by 1

Statement usesStructural congruence of π-calculus processes · Processes of the π-calculus · Finite endpoint ownership map · Conversion-enabled endpoint typing judgement

Proof usesChannel name in the π-calculus · Name scoped at a binder depth · Lifting free de Bruijn indices of a π-calculus process · Swapping adjacent binders throughout a process · 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 · Conversion-typed processes have no sum or replication · Restriction inversion for conversion typing · Removing a restriction around nil preserves conversion typing · Adding a restriction around nil preserves conversion typing · Swapping nested restrictions preserves conversion typing · Reverse restriction swap preserves conversion typing · Parallel reassociation preserves conversion typing · Reverse parallel reassociation preserves conversion typing · Parallel commutation preserves conversion typing · Parallel inversion for conversion typing · Removing a parallel nil preserves conversion typing · Adding a parallel nil preserves conversion typing · Scope extrusion preserves conversion typing in both directions · Finite linear π fragment without choice or replication · Polarized endpoint key · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name

Used bySubject reduction at a compatible conversion interface

TheoremSubject reduction at a compatible conversion interface#✓fully proved

From a typed source at an initially compatible interface, all five canonical reduction constructors preserve typing and compatibility, with one matched external subject-pair advancement or an unchanged interface when communication is private. No fragment or enabled-edge premise is required.

theorem HasType.subject_reduction {n : Nat} {Δ : Context} {p q : Proc}
    (h : HasType n Δ p) (hco : Compatible Δ) (hs : PiCalculus.Step p q) :
    ∃ Ξ, HasType n Ξ q ∧ Compatible Ξ ∧ (Ξ = Δ ∨ SemanticAdvance Δ Ξ)

Uses 29 · Used by 3

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Finite endpoint ownership map · Semantic peer compatibility of an ownership map · Conversion-enabled endpoint typing judgement · Semantic advancement of a communicating endpoint pair

Proof usesStructural congruence of π-calculus processes · Channel name in the π-calculus · Guarded-choice resolution in the π-calculus · Substitution for the innermost bound variable of a process · Endpoint capability with a dependency rank · Binding a fresh dual pair under restriction · 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 · Structural congruence preserves conversion typing · Conversion-typed processes have no sum or replication · Typed head communication yields a semantic advancement · Restriction inversion for conversion typing · Parallel inversion for conversion typing · Semantic advancement preserves compatibility · Semantic advancement preserves disjointness from a frame · Semantic advancement extends from the left part to the whole union · Semantic advancement extends from the right part to a disjoint union · Semantic advance under a private binding is private or outer · Finite linear π fragment without choice or replication · Polarized endpoint key · Endpoint role on a π name · Selection is trivial on the choice-free fragment

Used byTyping and compatibility persist along finite executions · Subject reduction at a balanced interface · Subject reduction at the empty interface

TheoremSubject reduction at a balanced interface#✓fully proved

A typed source with a balanced initial interface retains typing and balance after any canonical step. Balance supplies the required compatibility; the exact zero-or-one external advancement evidence is retained.

theorem HasType.subject_reduction_balanced {n : Nat} {Δ : Context} {p q : Proc}
    (h : HasType n Δ p) (hb : Balanced Δ) (hs : PiCalculus.Step p q) :
    ∃ Ξ, HasType n Ξ q ∧ Balanced Ξ ∧ (Ξ = Δ ∨ SemanticAdvance Δ Ξ)

Uses 10

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Finite endpoint ownership map · Semantic balance of a linear context · Conversion-enabled endpoint typing judgement · Semantic advancement of a communicating endpoint pair

Proof usesSemantic balance implies semantic compatibility · Semantic peer compatibility of an ownership map · Subject reduction at a compatible conversion interface · Semantic advancement preserves balance

TheoremSubject reduction at the empty interface#✓fully proved

An empty-interface typed network retains empty-interface typing through any canonical step. The empty context is balanced, hence compatible, including communication behind restrictions and pre/post congruence.

theorem HasType.subject_reduction_empty {n : Nat} {p q : Proc}
    (h : HasType n ∅ p) (hs : PiCalculus.Step p q) : HasType n ∅ q

Uses 20 · Used by 1

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Conversion-enabled endpoint typing judgement · Polarized endpoint key

Proof usesChannel name in the π-calculus · Equivalence of endpoint capabilities · Dual of an endpoint capability · Semantic balance implies semantic compatibility · Matching send and receive heads of two capabilities · Semantic peer compatibility of an ownership map · Subject reduction at a compatible conversion interface · Semantic advancement of a communicating endpoint pair · The empty context is semantically balanced · Peer endpoint key · Endpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Dual of an endpoint protocol · Endpoint role on a π name

Used byEmpty-interface typing persists along finite executions

TheoremTyping and compatibility persist along finite executions#✓fully proved

A typed source at an initially semantically compatible interface retains typing and compatibility through finite actual execution, with a finite trace of faithful advances. This is safety, not progress or termination.

theorem HasType.reachable {n : Nat} {Δ : Context} {p q : Proc} (h : HasType n Δ p)
    (hc : Compatible Δ) (hr : Relation.ReflTransGen PiCalculus.Step p q) :
    ∃ Ξ, HasType n Ξ q ∧ Compatible Ξ ∧ Relation.ReflTransGen SemanticAdvance Δ Ξ

Uses 7

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Finite endpoint ownership map · Semantic peer compatibility of an ownership map · Conversion-enabled endpoint typing judgement · Semantic advancement of a communicating endpoint pair

Proof usesSubject reduction at a compatible conversion interface

TheoremEmpty-interface typing persists along finite executions#✓fully proved

Every finite reachable closed state retains the exact empty interface.

theorem HasType.reachable_empty {n : Nat} {p q : Proc} (h : HasType n ∅ p)
    (hr : Relation.ReflTransGen PiCalculus.Step p q) : HasType n ∅ q

Uses 7

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Conversion-enabled endpoint typing judgement · Polarized endpoint key

Proof usesSubject reduction at the empty interface

InductivePriority-ranked conversion typing judgement#✓fully proved

Linear ownership typing with a strict priority check at every guard. There is no reduction, enabled-edge, progress or preservation field.

Cslib.SessionTypes.Endpoint.Conversion.RankedType · 34 lines

inductive RankedType : Nat → Context → Proc → Prop where
  | nil {n : Nat} {Δ : Context} :
      Δ.Completed → (∀ e ∈ Δ, e.name.ClosedAt n) → RankedType n Δ .nil
  | outName {n : Nat} {Δ : Context} {e : Key} {c : Capability}
      {b : Name} {s : Protocol} {p : Proc} :
      GuardMin Δ e c.rank → Δ.lookup e = some c → c.protocol.unfold = .sendName s →
      e.name.ClosedAt n → b.ClosedAt n →
      RankedType n (Δ.insert e ⟨c.rank, s⟩) p → RankedType n Δ (.out e.name b p)
  | inpName {n : Nat} {Δ : Context} {e : Key} {c : Capability}
      {s : Protocol} {p : Proc} :
      GuardMin Δ e c.rank → Δ.lookup e = some c → c.protocol.unfold = .recvName s →
      e.name.ClosedAt n →
      RankedType (n + 1) (Context.lift 0 (Δ.insert e ⟨c.rank, s⟩)) p →
      RankedType n Δ (.inp e.name p)
  | outEndpoint {n : Nat} {Δ : Context} {e d : Key} {c v : Capability}
      {k : Nat} {t s : Protocol} {p : Proc} :
      GuardMin Δ e c.rank → Δ.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 →
      RankedType n ((Δ.erase d).insert e ⟨c.rank, s⟩) p →
      RankedType n Δ (.out e.name d.name p)
  | inpEndpoint {n : Nat} {Δ : Context} {e : Key} {c : Capability}
      {r : Role} {k : Nat} {t s : Protocol} {p : Proc} :
      GuardMin Δ e c.rank → Δ.lookup e = some c →
      c.protocol.unfold = .recvEndpoint r k t s → e.name.ClosedAt n →
      RankedType (n + 1)
        ((Context.lift 0 (Δ.insert e ⟨c.rank, s⟩)).insert ⟨.var 0, r⟩ ⟨k, t⟩) p →
      RankedType n Δ (.inp e.name p)
  | par {n : Nat} {Δ Θ : Context} {p q : Proc} :
      Finmap.Disjoint Δ Θ → RankedType n Δ p → RankedType n Θ q →
      RankedType n (Δ ∪ Θ) (.par p q)
  | nu {n : Nat} {Δ : Context} {c : Capability} {p : Proc} :
      RankedType (n + 1) (Context.bind c Δ) p → RankedType n Δ (.nu p)

Uses 14 · Used by 55

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 · Guard priority condition on active endpoints · Polarized endpoint key · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name

Used byNil is runtime-typed with empty ownership · Completed conversion-ranked frontiers are congruent to nil · Erasing a key whose name is absent preserves conversion ranked typing · Minimum active role is the subject of a conversion frontier leaf · Forgetting priorities yields conversion typing · Conversion-ranked input subjects are active · Minimum guard leaf cannot own an equivalent dual peer · Nil typing lifts to conversion ranked typing · 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 · 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 · Adding a role unused by the partner preserves conversion ranked typing · Binder lifting preserves conversion ranked 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 conversion ranked typing · Context equivalence transports conversion ranked typing both ways · Same-name conversion guards are opposite and communicate · Forward scope extrusion preserves conversion ranked typing · Endpoint substitution preserves conversion ranked typing · Split-derived freshness for conversion endpoint substitution · Passive substitution preserves conversion ranked typing · Binder swap preserves conversion ranked typing · Conversion ranked typing descends from a lifted process · Weakening conversion ranked typing by a disjoint completed context · Structural congruence preserves conversion ranked typing · Conversion-ranked processes have a typed frontier normal form · Removing a restriction around nil preserves conversion ranked typing · Restricting nil preserves conversion ranked typing · Swapping two restrictions preserves conversion ranked typing · Reverse restriction swap preserves conversion ranked typing · Parallel reassociation preserves conversion ranked typing · Reverse parallel reassociation preserves conversion ranked typing · Parallel commutation preserves conversion ranked typing · Removing a parallel nil preserves conversion ranked typing · Adding a parallel nil preserves conversion ranked typing · Global progress of conversion-ranked processes at balanced interfaces · Finite runs keep conversion ranked typing at compatible interfaces · Reachable closed conversion-ranked states keep the empty interface · Restoring the bound pair preserves conversion ranked typing · Conversion ranked typing is invariant under scope extrusion · Reverse scope extrusion preserves conversion ranked typing · Conversion ranked subject reduction at compatible interfaces · Conversion ranked subject reduction at balanced interfaces · Conversion ranked subject reduction at the empty interface · Closed conversion-ranked networks are completed or can step · Progress at reachable states of closed conversion-ranked networks · Finite ranked typing embeds into runtime typing under separation

TheoremForgetting priorities yields conversion typing#✓fully proved

Forgetting guard priorities derives the existing conversion judgement.

theorem RankedType.hasType {n : Nat} {Δ : Context} {p : Proc}
    (h : RankedType n Δ p) : HasType n Δ p

Uses 16 · Used by 9

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Conversion-enabled endpoint typing judgement · Priority-ranked conversion 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 · Guard priority condition on active endpoints · Polarized endpoint key · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name

Used byMinimum active role is the subject of a conversion frontier leaf · Adding a role unused by the partner preserves conversion ranked typing · Same-name conversion guards are opposite and communicate · Structural congruence preserves conversion ranked typing · Conversion-ranked processes have a typed frontier normal form · Removing a restriction around nil preserves conversion ranked typing · Restricting nil preserves conversion ranked typing · Removing a parallel nil preserves conversion ranked typing · Conversion ranked subject reduction at compatible interfaces

TheoremRanked typing embeds into conversion ranked typing#✓fully proved

Explicit seven-case raw-ranked embedding, not theorem-value inheritance.

theorem RankedType.of_raw {n : Nat} {Δ : Context} {p : Proc}
    (h : Endpoint.RankedType n Δ p) : RankedType n Δ p

Uses 17

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Priority-ranked conversion typing judgement · Priority-ranked 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 · Reflexivity of capability equivalence · Completed ownership map · Binding a fresh dual pair under restriction · Lifting an ownership map past a binder · Guard priority condition on active endpoints · Polarized endpoint key · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name

TheoremParallel inversion for conversion ranked typing#✓fully proved

Ranked parallel typing exposes its actual disjoint ownership split.

theorem RankedType.par_inv {n : Nat} {Δ : Context} {p q : Proc}
    (h : RankedType n Δ (.par p q)) :
    ∃ Γ Θ, Δ = Γ ∪ Θ ∧ Finmap.Disjoint Γ Θ ∧ RankedType n Γ p ∧ RankedType n Θ q

Uses 15 · Used by 10

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Priority-ranked conversion typing judgement · Polarized endpoint key · Endpoint role on a π name

Proof usesName scoped at a binder depth · Equivalence of endpoint capabilities · Completed ownership map · Binding a fresh dual pair under restriction · Lifting an ownership map past a binder · Guard priority condition on active endpoints · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol

Used byCompleted conversion-ranked frontiers are congruent to nil · Minimum active role is the subject of a conversion frontier leaf · Forward scope extrusion preserves conversion ranked typing · Structural congruence preserves conversion ranked typing · Parallel reassociation preserves conversion ranked typing · Reverse parallel reassociation preserves conversion ranked typing · Parallel commutation preserves conversion ranked typing · Removing a parallel nil preserves conversion ranked typing · Reverse scope extrusion preserves conversion ranked typing · Conversion ranked subject reduction at compatible interfaces

TheoremRestriction inversion for conversion ranked typing#✓fully proved

Restriction chooses an actual literal-dual pair.

theorem RankedType.nu_inv {n : Nat} {Δ : Context} {p : Proc}
    (h : RankedType n Δ (.nu p)) : ∃ c, RankedType (n + 1) (Context.bind c Δ) p

Uses 15 · Used by 6

Statement usesProcesses of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Binding a fresh dual pair under restriction · Priority-ranked conversion typing judgement

Proof usesChannel name in the π-calculus · Name scoped at a binder depth · Equivalence of endpoint capabilities · Completed ownership map · Lifting an ownership map past a binder · Guard priority condition on active endpoints · Polarized endpoint key · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name

Used byForward scope extrusion preserves conversion ranked typing · Structural congruence preserves conversion ranked typing · Swapping two restrictions preserves conversion ranked typing · Global progress of conversion-ranked processes at balanced interfaces · Reverse scope extrusion preserves conversion ranked typing · Conversion ranked subject reduction at compatible interfaces

TheoremNil typing lifts to conversion ranked typing#✓fully proved

Nil adds no priority premise beyond actual completed and scoped ownership.

theorem RankedType.nil_of_hasType {n : Nat} {Δ : Context} (h : HasType n Δ .nil) :
    RankedType n Δ .nil

Uses 10 · Used by 2

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Conversion-enabled endpoint typing judgement · Priority-ranked conversion typing judgement

Proof usesChannel name in the π-calculus · Name scoped at a binder depth · Endpoint capability with a dependency rank · Completed ownership map · Nil inversion for conversion typing · Polarized endpoint key

Used byRemoving a restriction around nil preserves conversion ranked typing · Restricting nil preserves conversion ranked typing

TheoremConversion-ranked output subjects are active#✓fully proved

Literal output is active and checks every other owned active key.

theorem RankedType.out_active {n : Nat} {Δ : Context} {a b : Name} {p : Proc}
    (h : RankedType n Δ (.out a b p)) :
    ∃ e c, e.name = a ∧ Δ.lookup e = some c ∧ c.protocol.unfold ≠ .done ∧ GuardMin Δ e c.rank

Uses 16 · Used by 3

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Priority-ranked conversion typing judgement · Guard priority condition on active endpoints · 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 · Equivalence of endpoint capabilities · Completed ownership map · Binding a fresh dual pair under restriction · Lifting an ownership map past a binder · Send heads are active for both payload sorts

Used byCompleted conversion-ranked frontiers are congruent to nil · Minimum active role is the subject of a conversion frontier leaf · Minimum guard leaf cannot own an equivalent dual peer

TheoremConversion-ranked input subjects are active#✓fully proved

Literal input is active before either payload kind is received.

theorem RankedType.inp_active {n : Nat} {Δ : Context} {a : Name} {p : Proc}
    (h : RankedType n Δ (.inp a p)) :
    ∃ e c, e.name = a ∧ Δ.lookup e = some c ∧ c.protocol.unfold ≠ .done ∧ GuardMin Δ e c.rank

Uses 16 · Used by 3

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Priority-ranked conversion typing judgement · Guard priority condition on active endpoints · 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 · Equivalence of endpoint capabilities · Completed ownership map · Binding a fresh dual pair under restriction · Lifting an ownership map past a binder · Finite guarded regular protocol graph

Used byCompleted conversion-ranked frontiers are congruent to nil · Minimum active role is the subject of a conversion frontier leaf · Minimum guard leaf cannot own an equivalent dual peer

TheoremMinimum active role is the subject of a conversion frontier leaf#✓fully proved

A minimum active role is exposed as the EXACT subject of an actual leaf. The disjoint ownership split and canonical rearrangement are DERIVED outputs; no ready guard or normalizing typing result is required from the caller.

theorem GuardFrontier.expose_minimum {n : Nat} {Δ : Context} {p : Proc}
    (hf : GuardFrontier p) (ht : RankedType n Δ p) {e : Key} {c : Capability}
    (he : Δ.lookup e = some c) (ha : c.protocol.unfold ≠ .done)
    (hmin : ∀ x v, Δ.lookup x = some v → v.protocol.unfold ≠ .done → c.rank ≤ v.rank) :
    ∃ Γ Θ g r, Δ = Γ ∪ Θ ∧ Finmap.Disjoint Γ Θ ∧ Γ.lookup e = some c ∧
      Cong p (.par g r) ∧ RankedType n Γ g ∧ RankedType n Θ r ∧
      ((∃ b t, g = .out e.name b t) ∨ (∃ t, g = .inp e.name t)) ∧ GuardFrontier r

Uses 20 · Used by 1

Statement usesStructural congruence of π-calculus processes · Channel name in the π-calculus · Processes of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Priority-ranked conversion typing judgement · Parallel guard frontier · 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 · Nil inversion for conversion typing · Forgetting priorities yields conversion typing · Conversion-ranked input subjects are active · Conversion-ranked output subjects are active · Parallel inversion for conversion ranked typing · Guard priority condition on active endpoints · A minimum active role owned by a guard is its subject key

Used byProgress for semantically balanced conversion frontiers

TheoremCompleted conversion-ranked frontiers are congruent to nil#✓fully proved

A frontier with no active ownership cannot contain a live prefix. Completion is the PROCESS congruence to nil, not a completed empty interface.

theorem GuardFrontier.completed_nil {n : Nat} {Δ : Context} {p : Proc}
    (hf : GuardFrontier p) (ht : RankedType n Δ p) (hc : Δ.Completed) : Cong p .nil

Uses 16 · Used by 1

Statement usesStructural congruence of π-calculus processes · Processes of the π-calculus · Finite endpoint ownership map · Completed ownership map · Priority-ranked conversion typing judgement · Parallel guard frontier

Proof usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Conversion-ranked input subjects are active · Conversion-ranked output subjects are active · Parallel inversion for conversion ranked typing · Guard priority condition on active endpoints · Polarized endpoint key · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name

Used byProgress for semantically balanced conversion frontiers

TheoremMinimum guard leaf cannot own an equivalent dual peer#✓fully proved

A semantic equal-rank active peer cannot inhabit the selected minimum guard.

theorem minimum_peer_separate {n : Nat} {Γ : Context} {g : Proc} {e : Key} {c d : Capability}
    (ht : RankedType n Γ g) (he : Γ.lookup e = some c) (ha : c.protocol.unfold ≠ .done)
    (hmin : ∀ x v, Γ.lookup x = some v → v.protocol.unfold ≠ .done → c.rank ≤ v.rank)
    (hshape : (∃ b t, g = .out e.name b t) ∨ (∃ t, g = .inp e.name t))
    (hd : d.Equivalent c.dual) : Γ.lookup e.opposite ≠ some d

Uses 21 · Used by 1

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Endpoint capability with a dependency rank · Equivalence of endpoint capabilities · Dual of an endpoint capability · Finite endpoint ownership map · Priority-ranked conversion typing judgement · Polarized endpoint key · Peer endpoint key · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name

Proof usesDuality preserves activity of a capability · Uniqueness of capability lookups · Conversion-ranked input subjects are active · Conversion-ranked output subjects are active · Guard priority condition on active endpoints · An endpoint key differs from its peer · Regular-tree equivalence of protocols as bisimilarity · Tree equivalence preserves completion of a protocol · A minimum active role owned by a guard is its subject key

Used byProgress for semantically balanced conversion frontiers

TheoremWeakening conversion ranked typing by a completed capability#✓fully proved

Adding a fresh completed capability preserves every guard inequality through all seven rules. No active capability can be added by this theorem.

theorem RankedType.weaken_completed {n : Nat} {Δ : Context} {p : Proc}
    (h : RankedType n Δ p) {z : Key} {u : Capability} (hz : z ∉ Δ)
    (hu : u.protocol.unfold = .done) (hscope : z.name.ClosedAt n) :
    RankedType n (Δ.insert z u) p

Uses 28 · Used by 2

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 · Priority-ranked conversion typing judgement · Polarized endpoint key · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name

Proof usesLifting free de Bruijn indices of a π-calculus name · Equivalence of endpoint capabilities · Completed ownership map · Inserting a completed capability preserves completion · Binding a fresh dual pair under restriction · Restriction binding commutes with inserting an outer key · Inserting a key absent from the other side preserves disjointness · Erasing a different key commutes with insertion · Restriction binding preserves absence of an outer key · Updating an owned key keeps absent keys absent · Lifting preserves absence of a key · Lifting an ownership map past a binder · Context lifting commutes with insertion · Guard priority condition on active endpoints · Adding a completed role preserves the guard condition · A lifted key is never a freshly bound key · Renaming the physical name of an endpoint key · Lifting preserves and reflects name scoping

Used byAdding a role unused by the partner preserves conversion ranked typing · Weakening conversion ranked typing by a disjoint completed context

TheoremErasing a key whose name is absent preserves conversion ranked typing#✓fully proved

Actual all-position physical-name absence permits erasure in the refinement too. Subject and payload lookup obligations are never discarded.

theorem RankedType.erase_nameAbsent {n : Nat} {Δ : Context} {p : Proc}
    (h : RankedType n Δ p) {z : Key} (hab : NameAbsent z.name p) :
    RankedType n (Δ.erase z) p

Uses 26 · Used by 1

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Priority-ranked conversion typing judgement · Polarized endpoint key · Absence of a physical name from a process · Endpoint role on a π name

Proof usesName scoped at a binder depth · Lifting free de Bruijn indices of a π-calculus name · Equivalence of endpoint capabilities · Completed ownership map · Erasing a key preserves completion · Binding a fresh dual pair under restriction · Restriction binding commutes with erasing an owned outer key · Erasing a different key commutes with insertion · Erasing an absent key changes nothing · Erasure distributes over union · Lifting an ownership map past a binder · Context lifting commutes with erasing an owned key · Guard priority condition on active endpoints · Erasing a role preserves the guard condition · A lifted key is never a freshly bound key · Renaming the physical name of an endpoint key · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol

Used byReverse scope extrusion preserves conversion ranked typing

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.