Request-freeness is invariant under structural congruence to Runtime head communication advances or keeps the interface

TheoremRequest-freeness is invariant under structural congruence#✓fully proved

All canonical structural laws preserve absence of an exposed shared request.

theorem RequestFree.cong_iff {Γ : ServiceEnv} {p q : Proc} (h : Cong p q) :
    RequestFree Γ p ↔ RequestFree Γ q

Uses 10 · Used by 1

Statement usesStructural congruence of π-calculus processes · Processes of the π-calculus · Process with no exposed output on a declared shared name · Shared service environment

Proof usesChannel name in the π-calculus · Lifting free de Bruijn indices of a π-calculus process · Swapping adjacent binders throughout a process · Request-freeness is invariant under lifting · Request-freeness is invariant under binder swapping · Shared service signature

Used byBalanced runtime frontiers are idle or step given availability

TheoremService templates are request-free#✓fully proved

Existing guarded templates have no exposed output/request.

theorem ServiceTemplate.request_free {Γ : ServiceEnv} {p : Proc} (h : ServiceTemplate Γ p) :
    RequestFree Γ p

Uses 5 · Used by 1

Statement usesProcesses of the π-calculus · Process with no exposed output on a declared shared name · Shared service environment · Structural shared-service template

Proof usesChannel name in the π-calculus

Used byNon-request-free frontier exposes a shared output up to congruence

TheoremLifting preserves guarded frontiers#✓fully proved

Canonical lifting maps guards and existing idle templates literally.

theorem GuardedFrontier.lift {Γ : ServiceEnv} {p : Proc} (h : GuardedFrontier Γ p) (k : Nat) :
    GuardedFrontier Γ (liftProc k p)

Uses 8 · Used by 2

Statement usesProcesses of the π-calculus · Lifting free de Bruijn indices of a π-calculus process · Guarded frontier of guards and idle service templates · Shared service environment

Proof usesChannel name in the π-calculus · Lifting free de Bruijn indices of a π-calculus name · Structural shared-service template · Service templates are invariant under lifting

Used byLifting preserves guarded normal forms · Parallel composition preserves guarded normal forms up to congruence

TheoremLifting preserves guarded normal forms#✓fully proved

Lifting preserves the actual unguarded private restriction tower.

theorem GuardedNormal.lift {Γ : ServiceEnv} {p : Proc} (h : GuardedNormal Γ p) (k : Nat) :
    GuardedNormal Γ (liftProc k p)

Uses 6 · Used by 1

Statement usesProcesses of the π-calculus · Lifting free de Bruijn indices of a π-calculus process · Guarded normal form: restrictions over a guarded frontier · Shared service environment

Proof usesGuarded frontier of guards and idle service templates · Lifting preserves guarded frontiers

Used byParallel composition preserves guarded normal forms up to congruence

TheoremParallel composition preserves guarded normal forms up to congruence#✓fully proved

All private restrictions on either component are extruded canonically; no process execution or ready pair is stored in the normal form.

theorem GuardedNormal.parallel {Γ : ServiceEnv} {p q : Proc} (hp : GuardedNormal Γ p)
    (hq : GuardedNormal Γ q) : ∃ r, Cong (.par p q) r ∧ GuardedNormal Γ r

Uses 8 · Used by 1

Statement usesStructural congruence of π-calculus processes · Processes of the π-calculus · Guarded normal form: restrictions over a guarded frontier · Shared service environment

Proof usesLifting free de Bruijn indices of a π-calculus process · Guarded frontier of guards and idle service templates · Lifting preserves guarded frontiers · Lifting preserves guarded normal forms

Used byRuntime-typed processes are congruent to a guarded normal form

TheoremRuntime-typed processes are congruent to a guarded normal form#✓fully proved

ALL10 runtime rules derive a syntactic normal form internally. Replicas remain actual guarded templates; no recursive process is erased to finite typing.

theorem HasType.syntax_normal {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p : Proc}
    (h : HasType n Γ Δ p) : ∃ q, Cong p q ∧ GuardedNormal Γ q

Uses 24 · Used by 1

Statement usesStructural congruence of π-calculus processes · Processes of the π-calculus · Finite endpoint ownership map · Guarded normal form: restrictions over a guarded frontier · 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 · Guarded frontier of guards and idle service templates · Parallel composition preserves guarded normal forms up to congruence · 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 byGuarded normal form of a typed process keeps its typing

TheoremGuarded normal form of a typed process keeps its typing#✓fully proved

Actual runtime normalization retains SAME Γ/n/Δ through the proved Cong invariance; this theorem supplies the frontier, never the GLOBAL caller.

theorem HasType.frontier_normal {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p : Proc}
    (h : HasType n Γ Δ p) : ∃ q, Cong p q ∧ HasType n Γ Δ q ∧ GuardedNormal Γ q

Uses 8 · Used by 1

Statement usesStructural congruence of π-calculus processes · Processes of the π-calculus · Finite endpoint ownership map · Guarded normal form: restrictions over a guarded frontier · Runtime typing with guarded shared replication · Shared service environment

Proof usesStructural congruence preserves runtime typing · Runtime-typed processes are congruent to a guarded normal form

Used byGlobal runtime progress at balanced interfaces given availability

TheoremRequest-free runtime outputs have an active linear subject#✓fully proved

A request-free output has an ACTUAL active linear subject and GuardMin.

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

Uses 22 · Used by 3

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · 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 · Runtime typing with guarded shared replication · Process with no exposed output on a declared shared name · Shared service environment

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 · Priority of a shared invocation over active owned keys · Separation of owned linear names from shared names · Shared service signature · Structural shared-service template · Send heads are active for both payload sorts

Used byRequest-free completed runtime frontiers are service templates · Minimum active key is the subject of a runtime frontier leaf · Runtime minimum guard leaf cannot own an equivalent dual peer

TheoremRuntime inputs are active linear or have completed ownership#✓fully proved

Linear inputs expose active subjects; once-only shared accepts have only completed AMBIENT ownership and may wait quiescently.

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

Uses 21 · Used by 2

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Completed ownership map · 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 · Runtime typing with guarded shared replication · Shared service environment

Proof usesName scoped at a binder depth · Equivalence of endpoint capabilities · Binding a fresh dual pair under restriction · Lifting an ownership map past a binder · Finite guarded regular protocol graph · 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 byMinimum active key is the subject of a runtime frontier leaf · Runtime minimum guard leaf cannot own an equivalent dual peer

TheoremRequest-free completed runtime frontiers are service templates#✓fully proved

With no actual requests or active owned keys, typing derives ACTUAL idle service-template syntax, not merely an empty/completed interface.

theorem GuardedFrontier.completed_idle {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p : Proc}
    (hf : GuardedFrontier Γ p) (ht : HasType n Γ Δ p) (hr : RequestFree Γ p)
    (hc : Δ.Completed) : ServiceTemplate Γ p

Uses 25 · Used by 1

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Completed ownership map · Guarded frontier of guards and idle service templates · Runtime typing with guarded shared replication · Process with no exposed output on a declared shared name · Shared service environment · Structural shared-service template

Proof usesChannel name in the π-calculus · Name scoped at a binder depth · Endpoint capability with a dependency rank · Equivalence of endpoint capabilities · Binding a fresh dual pair under restriction · Lifting an ownership map past a binder · Finite guarded regular protocol graph · 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 · Request-free runtime outputs have an active linear subject · Inversion of runtime typing for parallel composition · Priority of a shared invocation over active owned keys · Separation of owned linear names from shared names · Shared service signature

Used byBalanced runtime frontiers are idle or step given availability

TheoremMinimum active key is the subject of a runtime frontier leaf#✓fully proved

A minimum over ALL actual active owned keys exposes the EXACT linear subject of a real runtime leaf. Idle templates/accept ambient are completed; shared outputs are excluded only by the internally established request-free case.

theorem GuardedFrontier.expose_minimum {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p : Proc}
    (hf : GuardedFrontier Γ p) (ht : HasType n Γ Δ p) (hr : RequestFree Γ 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) ∧ HasType n Γ Λ g ∧ HasType n Γ Θ r ∧
      ((∃ b t, g = .out e.name b t) ∨ (∃ t, g = .inp e.name t)) ∧ GuardedFrontier Γ r

Uses 25 · 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 · Polarized endpoint key · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name · Guarded frontier of guards and idle service templates · Runtime typing with guarded shared replication · Process with no exposed output on a declared shared name · Shared service environment

Proof usesName scoped at a binder depth · Completed ownership map · The empty ownership map is completed · Guard priority condition on active endpoints · Runtime inputs are active linear or have completed ownership · Request-free runtime outputs have an active linear subject · Inversion of runtime typing for parallel composition · Typed service templates own only completed entries · Separation of owned linear names from shared names · Structural shared-service template · Empty ownership is separated from shared names · A minimum active role owned by a guard is its subject key

Used byBalanced runtime frontiers are idle or step given availability

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

The equal-rank semantic peer of a minimum active role cannot share its actual guard leaf. Opposite roles on the SAME physical name are distinct keys.

theorem minimum_peer_separate {n : Nat} {Γ : ServiceEnv} {Δ : Context} {g : Proc}
    {e : Key} {c d : Capability} (ht : HasType n Γ Δ g) (hr : RequestFree Γ 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)
    (hs : (∃ 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 24 · 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 · Polarized endpoint key · Peer endpoint key · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name · Runtime typing with guarded shared replication · Process with no exposed output on a declared shared name · Shared service environment

Proof usesDuality preserves activity of a capability · Completed ownership map · Uniqueness of capability lookups · 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 · Runtime inputs are active linear or have completed ownership · Request-free runtime outputs have an active linear subject · A minimum active role owned by a guard is its subject key

Used byBalanced runtime frontiers are idle or step given availability

TheoremNon-request-free frontier exposes a shared output up to congruence#✓fully proved

A non-request-free frontier yields an ACTUAL declared output leaf through canonical par rearrangement. Neither readiness nor a progress result is supplied.

theorem GuardedFrontier.expose_request {Γ : ServiceEnv} {p : Proc} (hf : GuardedFrontier Γ p)
    (hn : ¬ RequestFree Γ p) :
    ∃ s sig b c r, Γ.lookup s = some sig ∧ Cong p (.par (.out (.const s) b c) r)

Uses 9 · Used by 1

Statement usesStructural congruence of π-calculus processes · Channel name in the π-calculus · Processes of the π-calculus · Guarded frontier of guards and idle service templates · Process with no exposed output on a declared shared name · Shared service environment · Shared service signature

Proof usesStructural shared-service template · Service templates are request-free

Used byExposed shared requests step when declared services are available

TheoremExposed shared requests step when declared services are available#✓fully proved

Any actual exposed request fires under the EXISTING all-declared-services availability qualifier, even with ZERO active owned keys or a DONE payload. The Step is constructed from actual offered input syntax, not stored in Available.

theorem GuardedFrontier.request_progress {Γ : ServiceEnv} {p : Proc} (hf : GuardedFrontier Γ p)
    (hn : ¬ RequestFree Γ p) (ha : Available Γ p) : ∃ q, PiCalculus.Step p q

Uses 13 · Used by 1

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Availability of all declared services · Guarded frontier of guards and idle service templates · Process with no exposed output on a declared shared name · Shared service environment

Proof usesStructural congruence of π-calculus processes · Channel name in the π-calculus · Structural congruence preserves service availability · Non-request-free frontier exposes a shared output up to congruence · Persistent service offer on a given name · Shared service signature · Offered service communicates with a matching shared output

Used byBalanced runtime frontiers are idle or step given availability

TheoremShared invocation and input worker preserve the combined interface#✓fully proved

A declared shared invocation and ANY typed input worker preserve their EXACT combined linear interface. The actual owned payload is substituted, not the advertised raw protocol; completed receiver annotations remain ambient.

theorem HasType.shared_head {n : Nat} {Γ : ServiceEnv} {Δ Θ : Context}
    {s : Nat} {sig : ServiceSignature} {b : Name} {p q : Proc}
    (hs : Γ.lookup s = some sig) (hd : Finmap.Disjoint Δ Θ)
    (hout : HasType n Γ Δ (.out (.const s) b p))
    (hin : HasType n Γ Θ (.inp (.const s) q)) :
    HasType n Γ (Δ ∪ Θ) (.par p (PiCalculus.subst q b))

Uses 25 · 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 · Finite endpoint ownership map · Polarized endpoint key · Endpoint role on a π name · Runtime typing with guarded shared replication · Shared service environment · Shared service signature

Proof usesName scoped at a binder depth · Equivalence of endpoint capabilities · Completed ownership map · Owned keys are absent from the other side of a disjoint split · Lifting an ownership map past a binder · Lifting the empty ownership map · Moving a capability across a union preserves the union · Inversion of runtime typing for input on a shared name · Output on a declared shared name is a service invocation · Each owned key of a runtime typing is scoped at ambient depth · Runtime typing separates owned names from shared services · Runtime typing under substitution of a transmitted endpoint · Weakening runtime typing by a disjoint completed context · Priority of a shared invocation over active owned keys · Separation of owned linear names from shared names

Used byRuntime head communication advances or keeps the interface

TheoremInversion of runtime input on a nonshared subject#✓fully proved

A nonshared input subject exposes a genuine linear passive or endpoint head. The shared accept alternative is excluded by actual subject nonalias.

theorem HasType.linear_input_inv {n : Nat} {Γ : ServiceEnv} {Δ : Context} {a : Name} {p : Proc}
    (h : HasType n Γ Δ (.inp a p))
    (hn : ∀ s sig, Γ.lookup s = some sig → a ≠ .const s) :
    ∃ e c, e.name = a ∧ Δ.lookup e = some c ∧
      ((∃ s, c.protocol.unfold = .recvName s ∧
          HasType (n + 1) Γ (Context.lift 0 (Δ.insert e ⟨c.rank, s⟩)) p) ∨
       ∃ r k t s, c.protocol.unfold = .recvEndpoint r k t s ∧
          HasType (n + 1) Γ
            ((Context.lift 0 (Δ.insert e ⟨c.rank, s⟩)).insert ⟨.var 0, r⟩ ⟨k, t⟩) p)

Uses 20 · 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 · Polarized endpoint key · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name · Runtime typing with guarded shared replication · Shared service environment · Shared service signature

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

Used byEndpoint head communication preserves runtime typing · Passive head communication preserves runtime typing · Same-name linear guards at a compatible interface communicate

TheoremSemantic advance preserves shared-linear separation#✓fully proved

Faithful semantic advancement preserves shared/linear separation by its actual owned-domain invariance, including every completed entry.

theorem Separated.advance {Γ : ServiceEnv} {Δ Ξ : Context}
    (h : Separated Γ Δ) (ha : Conversion.SemanticAdvance Δ Ξ) : Separated Γ Ξ

Uses 10 · Used by 1

Statement usesFinite endpoint ownership map · Semantic advancement of a communicating endpoint pair · Separation of owned linear names from shared names · Shared service environment

Proof usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Semantic advancement preserves the context's domain · Polarized endpoint key · Endpoint role on a π name · Shared service signature

Used bySubject reduction for runtime typing at compatible interfaces

TheoremPassive head communication preserves runtime typing#✓fully proved

At an INITIALLY compatible disjoint interface, a linear passive head retains both actual carrier codes and every runtime continuation guard at unchanged Γ.

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

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 · Finite endpoint ownership map · Semantic peer compatibility of an ownership map · 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 · Runtime typing with guarded shared replication · Separation of owned linear names from shared names · Shared service environment

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 · Communicating subjects have semantically dual capabilities · Peer of a passive send head has an equivalent receive head · Finite guarded regular protocol graph · Inversion of runtime input on a nonshared subject · Runtime typing under passive name substitution · Disjoint owned keys on one name have opposite roles

Used byRuntime head communication advances or keeps the interface

TheoremEndpoint head communication preserves runtime typing#✓fully proved

At an INITIALLY compatible split, linear endpoint communication transfers ACTUAL v and keeps the receiver's independent advertised payload/tail codes. The Γ-preserving runtime substitution retains all continuation priorities.

theorem endpoint_head_preservation {n k : Nat} {Γ : ServiceEnv} {Λ Θ : Context}
    {e f : Key} {c v : Capability} {t s : Protocol} {p q : Proc}
    (hd : Finmap.Disjoint Λ Θ) (hsep : Separated Γ Λ) (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 : HasType n Γ ((Λ.erase f).insert e ⟨c.rank, s⟩) p)
    (hq : HasType n Γ Θ (.inp e.name q)) (hb : f.name.ClosedAt n)
    (hco : Conversion.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 ∧
      HasType n Γ (((Λ ∪ Θ).insert e ⟨c.rank, s⟩).insert e.opposite ⟨d.rank, u⟩)
        (.par p (PiCalculus.subst q f.name))

Uses 30 · 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 · 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 · Runtime typing with guarded shared replication · Separation of owned linear names from shared names · Shared service environment

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 · 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 · Inversion of runtime input on a nonshared subject · Endpoint substitution with side conditions derived from a split · Disjoint owned keys on one name have opposite roles

Used byRuntime head communication advances or keeps the interface

TheoremRuntime head communication advances or keeps the interface#✓fully proved

At an INITIALLY semantically compatible linear interface, actual runtime heads either advance the paired linear subjects faithfully or transfer on a shared service with the EXACT unchanged interface. Mixed shared/linear heads are excluded by source separation, not a finite-fragment erasure or supplied result field.

theorem HasType.head_advance {n : Nat} {Γ : ServiceEnv} {Δ : Context} {a b : Name} {p q : Proc}
    (h : HasType n Γ Δ (.par (.out a b p) (.inp a q))) (hco : Conversion.Compatible Δ) :
    ∃ Ξ, HasType n Γ Ξ (.par p (PiCalculus.subst q b)) ∧ Conversion.Compatible Ξ ∧
      (Ξ = Δ ∨ Conversion.SemanticAdvance Δ Ξ)

Uses 33 · 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 · Semantic advancement of a communicating endpoint pair · Runtime typing with guarded shared replication · Shared service environment

Proof usesName scoped at a binder depth · Endpoint capability with a dependency rank · Equivalence of endpoint capabilities · Dual of an endpoint capability · Completed ownership map · Binding a fresh dual pair under restriction · Lifting an ownership map past a binder · Matching send and receive heads of two capabilities · Semantic advancement preserves compatibility · Guard priority condition on active endpoints · 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 · Inversion of runtime typing for parallel composition · Shared invocation and input worker preserve the combined interface · Priority of a shared invocation over active owned keys · Separation of owned linear names from shared names · Shared service signature · Structural shared-service template · Endpoint head communication preserves runtime typing · Passive head communication preserves runtime typing

Used bySubject reduction for runtime typing at compatible interfaces

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.