Weakening conversion ranked typing by a disjoint completed context to Adding a role unused by the partner preserves conversion ranked typing

TheoremWeakening conversion ranked typing by a disjoint completed context#✓fully proved

Reattaching a disjoint completed finite context preserves all guards.

theorem RankedType.weaken_completed_union {n : Nat} {Δ Θ : Context} {p : Proc}
    (h : RankedType n Δ p) (hd : Finmap.Disjoint Δ Θ) (hc : Θ.Completed)
    (hs : ∀ e ∈ Θ, e.name.ClosedAt n) : RankedType n (Δ ∪ Θ) p

Uses 14 · Used by 1

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 · Priority-ranked conversion typing judgement · Polarized endpoint key · Endpoint role on a π name

Proof usesErasing a key preserves completion · Insertion after erasing the same key · Reinserting an owned capability changes nothing · Inserting a left-absent key into a union updates the right part · Weakening conversion ranked typing by a completed capability

Used byRemoving a parallel nil preserves conversion ranked typing

TheoremEquivalent contexts preserve the guard condition#✓fully proved

Same domains, literal cap ranks and actual done equivalence preserve GuardMin.

theorem GuardMin.retype {Δ Ξ : Context} {e : Key} {k : Nat} (hg : GuardMin Δ e k)
    (he : ContextEquivalent Δ Ξ) : GuardMin Ξ e k

Uses 14 · Used by 2

Statement usesFinite endpoint ownership map · Pointwise equivalence of ownership maps · Guard priority condition on active endpoints · Polarized endpoint key

Proof usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Equivalence of endpoint capabilities · Lookups transfer along ownership-map equivalence · Symmetry of ownership-map equivalence · Endpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Tree equivalence preserves completion of a protocol · One-step unfolding of a protocol · Endpoint role on a π name

Used byEquivalent contexts preserve conversion ranked typing · Runtime typing transfers to an equivalent linear context

TheoremEquivalent contexts preserve conversion ranked typing#✓fully proved

GENERAL arbitrary-depth, arbitrary-context retyping, by all seven typing constructors. Target ownership, ranks and every unfolded branch are derived.

theorem RankedType.retype {n : Nat} {Δ Ξ : Context} {p : Proc}
    (h : RankedType n Δ p) (he : ContextEquivalent Δ Ξ) : RankedType n Ξ p

Uses 32 · Used by 2

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Pointwise equivalence of ownership maps · 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 · Reflexivity of capability equivalence · Symmetry of capability equivalence · Transitivity of capability equivalence · Completed ownership map · Binding a fresh dual pair under restriction · Lifting an ownership map past a binder · Binding equivalent fresh pairs preserves ownership-map equivalence · Ownership-map equivalence preserves completion · Erasure preserves ownership-map equivalence · Equivalent insertions preserve ownership-map equivalence · Lifting preserves ownership-map equivalence · Lookups transfer along ownership-map equivalence · Ownership-map equivalence preserves key scoping · Equivalence of a disjoint union splits into equivalent parts · Finite guarded regular protocol graph · Guard priority condition on active endpoints · Equivalent contexts preserve the guard condition · Head and branch matching of protocols up to a child relation · Polarized endpoint key · Endpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Tree-equivalent protocols have matching heads · One-step unfolding of a protocol · Endpoint role on a π name

Used byContext equivalence transports conversion ranked typing both ways · Endpoint substitution preserves conversion ranked typing

TheoremContext equivalence transports conversion ranked typing both ways#✓fully proved

Equivalence transports typing in BOTH directions at the same process/depth.

theorem RankedType.retype_iff {n : Nat} {Δ Ξ : Context} {p : Proc}
    (he : ContextEquivalent Δ Ξ) : RankedType n Δ p ↔ RankedType n Ξ p

Uses 6

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Pointwise equivalence of ownership maps · Priority-ranked conversion typing judgement

Proof usesSymmetry of ownership-map equivalence · Equivalent contexts preserve conversion ranked typing

TheoremCollision-free renaming preserves conversion ranked typing#✓fully proved

GENERAL name transport with collision freedom on actual owned keys and canonical ambient name scope; protocol codes, roles and ranks stay exact.

theorem RankedType.rename {n m : Nat} {Δ : Context} {p : Proc} {f : Name → Name}
    (h : RankedType n Δ p) (hscope : ∀ a, a.ClosedAt n → (f a).ClosedAt m)
    (hf : Set.InjOn (Key.mapName f) {e | e ∈ Δ}) :
    RankedType m (Context.rekey (Key.mapName f) Δ hf) (mapProc f p)

Uses 35 · Used by 5

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 · Collision-free rekeying of an ownership map · Priority-ranked conversion typing judgement · Polarized endpoint key · Renaming the physical name of an endpoint key · Capture-safe renaming of processes

Proof usesEquivalence of endpoint capabilities · Completed ownership map · Rekeying preserves completion · Binding a fresh dual pair under restriction · Injective rekeying preserves disjoint ownership · Injectivity of rekeying survives erasing a key · Injectivity of rekeying survives updating an owned key · Injectivity of rekeying under a restriction binding · Injectivity of rekeying passes under a binder · Injectivity of rekeying after receiving a fresh role · Lifting an ownership map past a binder · Lookups in a rekeyed ownership map · Keys of a rekeyed ownership map · Rekeying commutes with binding a private pair · Collision-free rekeying commutes with erasing an owned key · Collision-free rekeying commutes with insertion · Rekeying under a binder is the lift of the outer rekeying · Collision-free rekeying commutes with a disjoint union · Guard priority condition on active endpoints · Injective rekeying preserves the guard condition · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name · Extension of a name map under a binder · Extending a scoped name map under a binder keeps it scoped

Used byBinder lifting preserves conversion ranked typing · Endpoint substitution preserves conversion ranked typing · Passive substitution preserves conversion ranked typing · Binder swap preserves conversion ranked typing · Swapping two restrictions preserves conversion ranked typing

TheoremBinder lifting preserves conversion ranked typing#✓fully proved

Lift uses the canonical cutoff-aware name and process operations.

theorem RankedType.lift {n : Nat} {Δ : Context} {p : Proc} (h : RankedType n Δ p) (k : Nat) :
    RankedType (n + 1) (Context.lift k Δ) (liftProc k p)

Uses 18 · Used by 1

Statement usesProcesses of the π-calculus · Lifting free de Bruijn indices of a π-calculus process · Finite endpoint ownership map · Lifting an ownership map past a binder · Priority-ranked conversion typing judgement

Proof usesChannel name in the π-calculus · Name scoped at a binder depth · Lifting preserves name scoping · Lifting free de Bruijn indices of a π-calculus name · Endpoint capability with a dependency rank · Collision-free rekeying of an ownership map · Collision-free renaming preserves conversion ranked typing · Polarized endpoint key · Renaming the physical name of an endpoint key · Injective renamings act injectively on endpoint keys · Injectivity of name lifting · Capture-safe renaming of processes · Process renaming by a lift is process lifting

Used byForward scope extrusion preserves conversion ranked typing

TheoremBinder swap preserves conversion ranked typing#✓fully proved

Swap retains roles, protocols and ranks while permuting two ambient binders.

theorem RankedType.swap {n k : Nat} {Δ : Context} {p : Proc}
    (h : RankedType n Δ p) (hk : k + 1 < n) :
    RankedType n (Context.swap k Δ) (swapProc k p)

Uses 18

Statement usesProcesses of the π-calculus · Swapping adjacent binders throughout a process · Finite endpoint ownership map · Swapping two ambient binders in an ownership context · Priority-ranked conversion typing judgement

Proof usesChannel name in the π-calculus · Name scoped at a binder depth · Swapping adjacent de Bruijn indices in a name · Endpoint capability with a dependency rank · Collision-free rekeying of an ownership map · Collision-free renaming preserves conversion ranked typing · Polarized endpoint key · Renaming the physical name of an endpoint key · Injective renamings act injectively on endpoint keys · Swapping binders in scope preserves name scoping · Capture-safe renaming of processes · Process renaming by a swap is the restriction swap · Injectivity of name swapping

TheoremEndpoint substitution preserves conversion ranked typing#✓fully proved

GENERAL endpoint substitution: retain the ACTUAL transmitted capability's code and rank at the sent polarized key, allowing its opposite-role alias. Collision freedom is needed only for that exact key and canonical substitution.

theorem RankedType.subst_endpoint {n : Nat} {Δ : Context} {b : Name} {r : Role}
    {c v : Capability} {p : Proc}
    (h : RankedType (n + 1) ((Context.lift 0 Δ).insert ⟨.var 0, r⟩ c) p)
    (he : v.Equivalent c) (hb : b.ClosedAt n) (hfresh : (⟨b, r⟩ : Key) ∉ Δ) :
    RankedType n (Δ.insert ⟨b, r⟩ v) (PiCalculus.subst p b)

Uses 25 · Used by 1

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Processes of the π-calculus · Substitution for the innermost bound variable of a process · Endpoint capability with a dependency rank · Equivalence of endpoint capabilities · Finite endpoint ownership map · Lifting an ownership map past a binder · Priority-ranked conversion typing judgement · Polarized endpoint key · Endpoint role on a π name

Proof usesName substitution preserves scoping · Substitution of a name into a π-calculus name · Substitution of a name into a π-calculus process at a cutoff · Symmetry of capability equivalence · Received-endpoint substitution is injective when the role is fresh · Collision-free rekeying of an ownership map · Received-endpoint substitution moves the bound role to the sent key · Equivalent insertions preserve ownership-map equivalence · Reflexivity of ownership-map equivalence · Collision-free renaming preserves conversion ranked typing · Equivalent contexts preserve conversion ranked typing · Renaming the physical name of an endpoint key · Capture-safe renaming of processes · Process renaming by a substitution is process substitution

Used bySplit-derived freshness for conversion endpoint substitution

TheoremSplit-derived freshness for conversion endpoint substitution#✓fully proved

GENERAL split-derived freshness: actual payload ownership and the receiver's already-owned carrier derive non-aliasing even after advancement.

theorem RankedType.subst_endpoint_from_split {n : Nat} {Γ Θ : Context} {b : Name} {r : Role}
    {c v old next : Capability} {e : Key} {p : Proc}
    (hd : Finmap.Disjoint Γ Θ) (hv : Γ.lookup ⟨b, r⟩ = some v)
    (hc : Θ.lookup e = some old)
    (h : RankedType (n + 1) ((Context.lift 0 (Θ.insert e next)).insert ⟨.var 0, r⟩ c) p)
    (he : v.Equivalent c) (hb : b.ClosedAt n) :
    RankedType n ((Θ.insert e next).insert ⟨b, r⟩ v) (PiCalculus.subst p b)

Uses 14 · Used by 1

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Processes of the π-calculus · Substitution for the innermost bound variable of a process · Endpoint capability with a dependency rank · Equivalence of endpoint capabilities · Finite endpoint ownership map · Lifting an ownership map past a binder · Priority-ranked conversion typing judgement · Polarized endpoint key · Endpoint role on a π name

Proof usesUpdating an owned key keeps absent keys absent · Owned keys are absent from the other side of a disjoint split · Endpoint substitution preserves conversion ranked typing

Used byEndpoint head communication preserves conversion ranked typing

TheoremPassive substitution preserves conversion ranked typing#✓fully proved

GENERAL passive substitution transports all scoped positions but adds NO capability. The input context contains only lifted outer ownership.

theorem RankedType.subst_passive {n : Nat} {Δ : Context} {p : Proc} {b : Name}
    (h : RankedType (n + 1) (Context.lift 0 Δ) p) (hb : b.ClosedAt n) :
    RankedType n Δ (PiCalculus.subst p b)

Uses 19 · Used by 2

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Processes of the π-calculus · Substitution for the innermost bound variable of a process · Finite endpoint ownership map · Lifting an ownership map past a binder · Priority-ranked conversion typing judgement

Proof usesName substitution preserves scoping · Substitution of a name into a π-calculus name · Substitution of a name into a π-calculus process at a cutoff · Endpoint capability with a dependency rank · Passive substitution is injective on lifted outer keys · Collision-free rekeying of an ownership map · Passive substitution leaves the linear context unchanged · Collision-free renaming preserves conversion ranked typing · Polarized endpoint key · Renaming the physical name of an endpoint key · Capture-safe renaming of processes · Process renaming by a substitution is process substitution

Used byPassive head communication preserves conversion ranked typing · Conversion ranked typing descends from a lifted process

TheoremInversion of conversion-ranked input typing#✓fully proved

Input inversion retains its actual advertised code and typed continuation.

theorem RankedType.inp_inv {n : Nat} {Δ : Context} {a : Name} {p : Proc}
    (h : RankedType n Δ (.inp a p)) :
    ∃ e c, e.name = a ∧ Δ.lookup e = some c ∧
      ((∃ s, c.protocol.unfold = .recvName s ∧
          RankedType (n + 1) (Context.lift 0 (Δ.insert e ⟨c.rank, s⟩)) p) ∨
       ∃ r k t s, c.protocol.unfold = .recvEndpoint r k t s ∧
          RankedType (n + 1)
            ((Context.lift 0 (Δ.insert e ⟨c.rank, s⟩)).insert ⟨.var 0, r⟩ ⟨k, t⟩) p)

Uses 15 · Used by 3

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Lifting an ownership map past a binder · 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 usesName scoped at a binder depth · Equivalence of endpoint capabilities · Completed ownership map · Binding a fresh dual pair under restriction · Guard priority condition on active endpoints

Used byEndpoint head communication preserves conversion ranked typing · Passive head communication preserves conversion ranked typing · Same-name conversion guards are opposite and communicate

TheoremPassive head communication preserves conversion ranked typing#✓fully proved

GENERAL passive communicating-head preservation at a semantically compatible actual split, with literal receiver-tail and rank evidence.

theorem ranked_passive_head_preservation {n : Nat} {Γ Θ : Context} {e : Key} {c : Capability}
    {s : Protocol} {b : Name} {p q : Proc}
    (hd : Finmap.Disjoint Γ Θ) (hc : Γ.lookup e = some c)
    (hh : c.protocol.unfold = .sendName s)
    (hp : RankedType n (Γ.insert e ⟨c.rank, s⟩) p) (hq : RankedType n Θ (.inp e.name q))
    (hb : b.ClosedAt n) (hco : Compatible (Γ ∪ Θ)) :
    ∃ d u, Θ.lookup e.opposite = some d ∧ d.rank = c.rank ∧
      d.protocol.unfold = .recvName u ∧ u.TreeEquiv s.dual ∧
      RankedType n (((Γ ∪ Θ).insert e ⟨c.rank, s⟩).insert e.opposite ⟨d.rank, u⟩)
        (.par p (PiCalculus.subst q b))

Uses 26 · Used by 1

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Processes of the π-calculus · Substitution for the innermost bound variable of a process · Endpoint capability with a dependency rank · Finite endpoint ownership map · Semantic peer compatibility of an ownership map · Priority-ranked conversion typing judgement · Polarized endpoint key · Peer endpoint key · Endpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Dual of an endpoint protocol · One-step unfolding of a protocol · Endpoint role on a π name

Proof usesEquivalence of endpoint capabilities · Dual of an endpoint capability · Updating an owned key preserves a disjoint split · Lifting an ownership map past a binder · Updating owned keys on both sides of a disjoint union · Inversion of conversion-ranked input typing · Passive substitution preserves conversion ranked typing · Communicating subjects have semantically dual capabilities · Peer of a passive send head has an equivalent receive head · Finite guarded regular protocol graph · Disjoint owned keys on one name have opposite roles

Used byHead preservation for a conversion-ranked opposite pair

TheoremEndpoint head communication preserves conversion ranked typing#✓fully proved

At an initially semantically compatible disjoint split, endpoint head communication transfers EXACT v, retaining the receiver's separately equivalent advertised payload/tail codes.

theorem ranked_endpoint_head_preservation {n k : Nat} {Γ Θ : Context} {e f : Key}
    {c v : Capability} {t s : Protocol} {p q : Proc}
    (hd : Finmap.Disjoint Γ Θ) (hc : Γ.lookup e = some c)
    (hh : c.protocol.unfold = .sendEndpoint f.role k t s)
    (hv : Γ.lookup f = some v) (hvt : v.Equivalent ⟨k, t⟩) (hne : e ≠ f)
    (hp : RankedType n ((Γ.erase f).insert e ⟨c.rank, s⟩) p)
    (hq : RankedType n Θ (.inp e.name q)) (hb : f.name.ClosedAt n)
    (hco : Compatible (Γ ∪ Θ)) :
    ∃ d t' u, Θ.lookup e.opposite = some d ∧ d.rank = c.rank ∧
      d.protocol.unfold = .recvEndpoint f.role k t' u ∧ t'.TreeEquiv t ∧ u.TreeEquiv s.dual ∧
      RankedType n (((Γ ∪ Θ).insert e ⟨c.rank, s⟩).insert e.opposite ⟨d.rank, u⟩)
        (.par p (PiCalculus.subst q f.name))

Uses 28 · Used by 1

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Processes of the π-calculus · Substitution for the innermost bound variable of a process · Endpoint capability with a dependency rank · Equivalence of endpoint capabilities · Finite endpoint ownership map · Semantic peer compatibility of an ownership map · Priority-ranked conversion typing judgement · Polarized endpoint key · Peer endpoint key · Endpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Dual of an endpoint protocol · One-step unfolding of a protocol · Endpoint role on a π name

Proof usesTransitivity of capability equivalence · Dual of an endpoint capability · Capability transfer with carrier updates preserves disjointness · Lifting an ownership map past a binder · Combined context after delegation and two carrier updates · Inversion of conversion-ranked input typing · Split-derived freshness for conversion endpoint substitution · Communicating subjects have semantically dual capabilities · Peer of an endpoint send head has an equivalent receive head · Finite guarded regular protocol graph · Protocol tree equivalence is symmetric · Disjoint owned keys on one name have opposite roles

Used byHead preservation for a conversion-ranked opposite pair

TheoremHead preservation for a conversion-ranked opposite pair#✓fully proved

A typed opposite-head pair at an initially semantically compatible interface yields packed literal-head preservation. Both actual heads and payload/tail correspondence are conclusions, not fields in a protocol or admission predicate.

theorem RankedType.head_preservation {n : Nat} {Δ : Context} {a b : Name} {p q : Proc}
    (h : RankedType n Δ (.par (.out a b p) (.inp a q))) (hco : Compatible Δ) :
    ∃ e c d s u, e.name = a ∧ Δ.lookup e = some c ∧ Δ.lookup e.opposite = some d ∧
      d.rank = c.rank ∧ u.TreeEquiv s.dual ∧
      ((c.protocol.unfold = .sendName s ∧ d.protocol.unfold = .recvName u) ∨
       ∃ f v k t t', f.name = b ∧ Δ.lookup f = some v ∧ v.Equivalent ⟨k, t⟩ ∧
         c.protocol.unfold = .sendEndpoint f.role k t s ∧
         d.protocol.unfold = .recvEndpoint f.role k t' u ∧ t'.TreeEquiv t) ∧
      RankedType n ((Δ.insert e ⟨c.rank, s⟩).insert e.opposite ⟨d.rank, u⟩)
        (.par p (PiCalculus.subst q b))

Uses 22 · Used by 1

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Substitution for the innermost bound variable of a process · Endpoint capability with a dependency rank · Equivalence of endpoint capabilities · Finite endpoint ownership map · Semantic peer compatibility of an ownership map · Priority-ranked conversion typing judgement · Polarized endpoint key · Peer endpoint key · Endpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Dual of an endpoint protocol · 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 · Endpoint head communication preserves conversion ranked typing · Passive head communication preserves conversion ranked typing · Guard priority condition on active endpoints

Used byConversion head communication yields a semantic advance

TheoremConversion head communication yields a semantic advance#✓fully proved

For a ranked-typed opposite-head pair at an initially semantically compatible interface, head preservation constructs a faithful semantic advance and a compatible ranked residual.

theorem RankedType.head_advance {n : Nat} {Δ : Context} {a b : Name} {p q : Proc}
    (h : RankedType n Δ (.par (.out a b p) (.inp a q))) (hc : Compatible Δ) :
    ∃ Ξ, RankedType n Ξ (.par p (PiCalculus.subst q b)) ∧ Compatible Ξ ∧ SemanticAdvance Δ Ξ

Uses 20 · Used by 1

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Substitution for the innermost bound variable of a process · Finite endpoint ownership map · Semantic peer compatibility of an ownership map · Priority-ranked conversion typing judgement · Semantic advancement of a communicating endpoint pair

Proof usesEndpoint capability with a dependency rank · Equivalence of endpoint capabilities · Dual of an endpoint capability · Matching send and receive heads of two capabilities · Head preservation for a conversion-ranked opposite pair · Semantic advancement preserves compatibility · Polarized endpoint key · Peer endpoint key · Endpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Dual of an endpoint protocol · One-step unfolding of a protocol · Endpoint role on a π name

Used byConversion ranked subject reduction at compatible interfaces

TheoremSame-name conversion guards are opposite and communicate#✓fully proved

For disjoint ranked-typed same-name leaves at a semantically compatible combined interface, literal guard shapes have opposite directions and yield an actual canonical Step.

theorem same_name_guards_step {n : Nat} {Γ Θ : Context} {g h : Proc} {a : Name}
    (hg : RankedType n Γ g) (hh : RankedType n Θ h)
    (hd : Finmap.Disjoint Γ Θ) (hc : Compatible (Γ ∪ Θ))
    (sg : (∃ b p, g = .out a b p) ∨ (∃ p, g = .inp a p))
    (sh : (∃ b p, h = .out a b p) ∨ (∃ p, h = .inp a p)) :
    ∃ q, PiCalculus.Step (.par g h) q

Uses 29 · Used by 1

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

Proof usesStructural congruence of π-calculus processes · Guarded-choice resolution in the π-calculus · Substitution for the innermost bound variable of a process · Equivalence of endpoint capabilities · Duality preserves capability equivalence · Dual of an endpoint capability · Lifting an ownership map past a binder · Output inversion for conversion typing · Forgetting priorities yields conversion typing · Inversion of conversion-ranked input typing · Communicating subjects have semantically dual capabilities · Peer of an endpoint send head has an equivalent receive head · Peer of a passive send head has an equivalent receive head · Finite guarded regular protocol graph · Endpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Dual of an endpoint protocol · One-step unfolding of a protocol · Unfolding commutes with protocol duality · Capability whose head is a send with a given continuation

Used byProgress for semantically balanced conversion frontiers

TheoremProgress for semantically balanced conversion frontiers#✓fully proved

GENERAL balanced ranked frontier progress. A minimum over ALL active owned roles exposes two distinct opposite subject leaves, from which actual canonical communication follows. Completion is process-level Cong to nil.

theorem GuardFrontier.progress {n : Nat} {Δ : Context} {p : Proc}
    (hf : GuardFrontier p) (ht : RankedType n Δ p) (hb : Balanced Δ) :
    Cong p .nil ∨ ∃ q, PiCalculus.Step p q

Uses 28 · Used by 1

Statement usesStructural congruence of π-calculus processes · Processes of the π-calculus · Reduction relation of the π-calculus · Finite endpoint ownership map · Semantic balance of a linear context · Priority-ranked conversion typing judgement · Parallel guard frontier

Proof usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Equivalence of endpoint capabilities · Dual of an endpoint capability · Duality preserves activity of a capability · Completed ownership map · Existence of a least-rank active binding · Semantic balance implies semantic compatibility · Semantic peer compatibility of an ownership map · Compatibility restricts to the left part of a union · Completed 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 · Same-name conversion guards are opposite and communicate · Polarized endpoint key · Peer endpoint key · Endpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Tree equivalence preserves completion of a protocol · One-step unfolding of a protocol · Endpoint role on a π name

Used byGlobal progress of conversion-ranked processes at balanced interfaces

TheoremConversion ranked typing descends from a lifted process#✓fully proved

Reflection of an actual lifted term recovers every priority and context entry.

theorem RankedType.unlift {n : Nat} {Γ : Context} {q : Proc}
    (h : RankedType (n + 1) Γ (liftProc 0 q)) (hΓ : ∀ e ∈ Γ, e.name ≠ .var 0) :
    RankedType n (Context.lower Γ hΓ) q

Uses 14 · Used by 1

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Lifting free de Bruijn indices of a π-calculus process · Endpoint capability with a dependency rank · Finite endpoint ownership map · Lowering of an outer context past a fresh binder · Priority-ranked conversion typing judgement · Polarized endpoint key

Proof usesSubstitution for the innermost bound variable of a process · Substitution of a name into a π-calculus process at a cutoff · Lifting an ownership map past a binder · Lifting a lowered context recovers it · Passive substitution preserves conversion ranked typing · Substitution cancels process lifting

Used byReverse scope extrusion preserves conversion ranked typing

TheoremForward scope extrusion preserves conversion ranked typing#✓fully proved

Extrusion lifts the partner's real ownership while retaining every guard.

theorem RankedType.scope_forward {n : Nat} {Δ : Context} {p q : Proc}
    (h : RankedType n Δ (.par (.nu p) q)) :
    RankedType n Δ (.nu (.par p (liftProc 0 q)))

Uses 15 · Used by 1

Statement usesProcesses of the π-calculus · Lifting free de Bruijn indices of a π-calculus process · Finite endpoint ownership map · Priority-ranked conversion typing judgement

Proof usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Binding a fresh dual pair under restriction · Restriction binding of a disjoint union · Binding a fresh pair keeps disjointness from a lifted context · Lifting an ownership map past a binder · Binder lifting preserves conversion ranked typing · Restriction inversion for conversion ranked typing · Parallel inversion for conversion ranked typing · Polarized endpoint key · Endpoint role on a π name

Used byConversion ranked typing is invariant under scope extrusion

TheoremAdding a role unused by the partner preserves conversion ranked typing#✓fully proved

Moving a partner-owned role back requires actual absence to DERIVE completion from conversion typing before refined completed weakening is applied.

theorem RankedType.insert_from_absent_partner {n : Nat} {Γ Ξ : Context} {p q : Proc}
    {e : Key} {c : Capability} (hp : RankedType n Γ p) (hq : RankedType n Ξ q)
    (hc : (Γ ∪ Ξ).lookup e = some c) (hab : NameAbsent e.name q)
    (he : e.name.ClosedAt n) : RankedType n (Γ.insert e c) p

Uses 13 · Used by 1

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 · Absence of a physical name from a process · Endpoint role on a π name

Proof usesReinserting an owned capability changes nothing · Owned capabilities with absent names are completed · Forgetting priorities yields conversion typing · Weakening conversion ranked typing by a completed capability

Used byRestoring the bound pair preserves conversion ranked typing

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.