Same-name linear guards at a compatible interface communicate to Qualified progress at reachable closed runtime states

TheoremSame-name linear guards at a compatible interface communicate#✓fully proved

Actual disjoint same-name linear leaves at an INITIALLY compatible interface have opposite directions and construct a canonical Step. Shapes/nonalias are internally exposed outputs in the GLOBAL proof, not caller readiness hypotheses.

theorem same_name_linear_guards_step {n : Nat} {Γ : ServiceEnv} {Λ Θ : Context}
    {g h : Proc} {a : Name} (hg : HasType n Γ Λ g) (hh : HasType n Γ Θ h)
    (hd : Finmap.Disjoint Λ Θ) (hc : Conversion.Compatible (Λ ∪ Θ))
    (hn : ∀ s sig, Γ.lookup s = some sig → a ≠ .const s)
    (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 36 · 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 · Polarized endpoint key · Endpoint role on a π name · Runtime typing with guarded shared replication · Shared service environment · Shared service signature

Proof usesStructural congruence of π-calculus processes · Name scoped at a binder depth · 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 · Completed ownership map · Binding a fresh dual pair under restriction · Lifting an ownership map past a binder · Communicating subjects have semantically dual capabilities · Finite guarded regular protocol graph · Guard priority condition on active endpoints · Head and branch matching of protocols up to a child relation · Endpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Tree-equivalent protocols have matching heads · Dual of an endpoint protocol · One-step unfolding of a protocol · Unfolding commutes with protocol duality · Inversion of runtime input on a nonshared subject · Priority of a shared invocation over active owned keys · Separation of owned linear names from shared names · Structural shared-service template · Capability whose head is a send with a given continuation

Used byBalanced runtime frontiers are idle or step given availability

TheoremBalanced runtime frontiers are idle or step given availability#✓fully proved

A typed balanced runtime frontier with actual persistent service availability is syntactically Idle OR takes an ACTUAL canonical Step. Shared requests are handled even if all owned keys are done; minimum/peer leaves are derived internally.

theorem GuardedFrontier.progress {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p : Proc}
    (hf : GuardedFrontier Γ p) (ht : HasType n Γ Δ p) (hb : Conversion.Balanced Δ)
    (hav : Available Γ p) : Idle Γ p ∨ ∃ q, PiCalculus.Step p q

Uses 35 · Used by 1

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Finite endpoint ownership map · Semantic balance of a linear context · Availability of all declared services · Guarded frontier of guards and idle service templates · Runtime typing with guarded shared replication · Idle process as a structural service template · Shared service environment

Proof usesStructural congruence of π-calculus processes · Channel 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 · 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 · Request-free completed runtime frontiers are service templates · Minimum active key is the subject of a runtime frontier leaf · Exposed shared requests step when declared services are available · Runtime typing separates owned names from shared services · Process with no exposed output on a declared shared name · Request-freeness is invariant under structural congruence · Runtime minimum guard leaf cannot own an equivalent dual peer · Same-name linear guards at a compatible interface communicate

Used byGlobal runtime progress at balanced interfaces given availability

TheoremChoice selection is the identity on runtime-typed processes#✓fully proved

Canonical choice selection is identity on an actually runtime-typed root: there is no sum rule, although replication is admitted. No finiteLinear erasure.

theorem HasType.select_eq {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p q : Proc}
    (h : HasType n Γ Δ p) (hs : Select p q) : p = q

Uses 21 · Used by 1

Statement usesProcesses of the π-calculus · Guarded-choice resolution in the π-calculus · Finite endpoint ownership map · Runtime typing with guarded shared replication · Shared service environment

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 · Priority of a shared invocation over active owned keys · Separation of owned linear names from shared names · Shared service signature · Structural shared-service template

Used bySubject reduction for runtime typing at compatible interfaces

TheoremSubject reduction for runtime typing at compatible interfaces#✓fully proved

From a runtime-typed source at an INITIALLY semantically compatible linear interface, ALL5 canonical Step constructors preserve Γ/n, typing and compatibility. The actual residual interface is unchanged OR has one faithful SemanticAdvance. Shared transfers are exact identity; private projection uses the chosen literal pair.

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

Uses 31 · Used by 5

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Finite endpoint ownership map · Semantic peer compatibility of an ownership map · Semantic advancement of a communicating endpoint pair · Runtime typing with guarded shared replication · Shared service environment

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 · 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 · Polarized endpoint key · Endpoint role on a π name · Structural congruence preserves runtime typing · Runtime head communication advances or keeps the interface · Inversion of runtime typing for restriction · Inversion of runtime typing for parallel composition · Choice selection is the identity on runtime-typed processes · Runtime typing separates owned names from shared services · Separation of owned linear names from shared names · Semantic advance preserves shared-linear separation

Used byEach next phase is typed by subject reduction · Steps preserve typing at the recurring interface · Multi-step subject reduction at compatible interfaces · Subject reduction for runtime typing at balanced interfaces · Subject reduction for runtime typing at the empty interface

TheoremSubject reduction for runtime typing at balanced interfaces#✓fully proved

An INITIALLY semantically balanced runtime interface derives compatibility and retains balance and the exact zero-or-one external advance after ANY Step.

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

Uses 11

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Finite endpoint ownership map · Semantic balance of a linear context · Semantic advancement of a communicating endpoint pair · Runtime typing with guarded shared replication · Shared service environment

Proof usesSemantic balance implies semantic compatibility · Semantic peer compatibility of an ownership map · Semantic advancement preserves balance · Subject reduction for runtime typing at compatible interfaces

TheoremSubject reduction for runtime typing at the empty interface#✓fully proved

An empty linear interface is initially balanced/compatible and remains EXACTLY empty through any runtime Step, including private sessions and shared services.

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

Uses 21 · Used by 1

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Polarized endpoint key · Runtime typing with guarded shared replication · Shared service environment

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 · 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 · Subject reduction for runtime typing at compatible interfaces

Used byMulti-step subject reduction at the empty interface

TheoremMulti-step subject reduction at compatible interfaces#✓fully proved

From an INITIALLY compatible runtime interface, finite actual reductions retain typing/compatibility and accumulate a trace of faithful semantic advances. Shared/private identity steps introduce no fake external advancement.

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

Uses 8 · Used by 2

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Finite endpoint ownership map · Semantic peer compatibility of an ownership map · Semantic advancement of a communicating endpoint pair · Runtime typing with guarded shared replication · Shared service environment

Proof usesSubject reduction for runtime typing at compatible interfaces

Used byEvery phase is typed by preservation from the pending state · Multi-step subject reduction at balanced interfaces

TheoremMulti-step subject reduction at balanced interfaces#✓fully proved

Every finite reachable state from an INITIALLY balanced runtime interface retains semantic balance and an ACTUAL faithful advancement trace, not progress.

theorem HasType.reachable_balanced {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p q : Proc}
    (h : HasType n Γ Δ p) (hb : Conversion.Balanced Δ)
    (hr : Relation.ReflTransGen PiCalculus.Step p q) :
    ∃ Ξ, HasType n Γ Ξ q ∧ Conversion.Balanced Ξ ∧
      Relation.ReflTransGen Conversion.SemanticAdvance Δ Ξ

Uses 11 · Used by 1

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Finite endpoint ownership map · Semantic balance of a linear context · Semantic advancement of a communicating endpoint pair · Runtime typing with guarded shared replication · Shared service environment

Proof usesSemantic balance implies semantic compatibility · Semantic peer compatibility of an ownership map · Semantic advancement preserves balance · Multi-step subject reduction at compatible interfaces

Used byQualified progress at every reachable runtime state

TheoremMulti-step subject reduction at the empty interface#✓fully proved

Finite runtime execution from an empty interface preserves exact empty ownership. This safety result does not identify idle replicas with Cong nil.

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

Uses 8 · Used by 1

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Polarized endpoint key · Runtime typing with guarded shared replication · Shared service environment

Proof usesSubject reduction for runtime typing at the empty interface

Used byQualified progress at reachable closed runtime states

TheoremGlobal runtime progress at balanced interfaces given availability#✓fully proved

GLOBAL progress at arbitrary ambient n/shared Γ/actual balanced Δ/process p, qualified ONLY by runtime typing, INITIAL semantic balance and EXISTING persistent availability of ALL declared signatures. Result is actual Idle syntax OR a canonical Step. No frontier/normal form/readiness/Step/fairness/representative is supplied.

theorem HasType.progress_balanced {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p : Proc}
    (h : HasType n Γ Δ p) (hb : Conversion.Balanced Δ) (ha : Available Γ p) :
    Idle Γ p ∨ ∃ q, PiCalculus.Step p q

Uses 19 · Used by 3

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Finite endpoint ownership map · Semantic balance of a linear context · Availability of all declared services · Runtime typing with guarded shared replication · Idle process as a structural service template · Shared service environment

Proof usesStructural congruence of π-calculus processes · Endpoint capability with a dependency rank · Binding a fresh dual pair under restriction · Binding a dual private pair preserves balance · Structural congruence preserves service availability · Guarded frontier of guards and idle service templates · Balanced runtime frontiers are idle or step given availability · Guarded normal form: restrictions over a guarded frontier · Guarded normal form of a typed process keeps its typing · Inversion of runtime typing for restriction · Idleness is invariant under structural congruence

Used byEvery phase of the repeated session can step · Closed runtime processes are idle or step given availability · Qualified progress at every reachable runtime state

TheoremClosed runtime processes are idle or step given availability#✓fully proved

Closed empty-interface runtime progress, at arbitrary passive-name depth, requires the SAME actual all-declared-service availability. Idle includes waiting replicas/accepts and nil; no termination or scheduler fairness is asserted.

theorem HasType.progress_empty {n : Nat} {Γ : ServiceEnv} {p : Proc}
    (h : HasType n Γ ∅ p) (ha : Available Γ p) : Idle Γ p ∨ ∃ q, PiCalculus.Step p q

Uses 11 · Used by 2

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Polarized endpoint key · Availability of all declared services · Runtime typing with guarded shared replication · Idle process as a structural service template · Shared service environment

Proof usesThe empty context is semantically balanced · Global runtime progress at balanced interfaces given availability

Used byEvery phase of the restricted repeated session can step · Qualified progress at reachable closed runtime states

TheoremQualified progress at every reachable runtime state#✓fully proved

Every finite canonical reduction from an initially balanced, available typed runtime retains qualified GLOBAL progress. Safety supplies actual balanced residual ownership/advance trace, and Available.reachable supplies current persistent syntax.

theorem HasType.reachable_progress {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p q : Proc}
    (h : HasType n Γ Δ p) (hb : Conversion.Balanced Δ) (ha : Available Γ p)
    (hr : Relation.ReflTransGen PiCalculus.Step p q) : Idle Γ q ∨ ∃ r, PiCalculus.Step q r

Uses 12

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Finite endpoint ownership map · Semantic balance of a linear context · Availability of all declared services · Runtime typing with guarded shared replication · Idle process as a structural service template · Shared service environment

Proof usesSemantic advancement of a communicating endpoint pair · Service availability survives finite reduction · Global runtime progress at balanced interfaces given availability · Multi-step subject reduction at balanced interfaces

TheoremQualified progress at reachable closed runtime states#✓fully proved

Finite reachable empty-interface states retain the same qualified progress; this is one-step safety/progress, not all-schedules eventual responsiveness.

theorem HasType.reachable_progress_empty {n : Nat} {Γ : ServiceEnv} {p q : Proc}
    (h : HasType n Γ ∅ p) (ha : Available Γ p)
    (hr : Relation.ReflTransGen PiCalculus.Step p q) : Idle Γ q ∨ ∃ r, PiCalculus.Step q r

Uses 12

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Polarized endpoint key · Availability of all declared services · Runtime typing with guarded shared replication · Idle process as a structural service template · Shared service environment

Proof usesService availability survives finite reduction · Closed runtime processes are idle or step given availability · Multi-step subject reduction at the empty interface

13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.