Binder lifting preserves separation to Inversion of runtime typing for input on a shared name

TheoremBinder lifting preserves separation#✓fully proved

Actual binder lifting preserves nonshared physical names: constants cannot be newly produced by lifting a linear variable.

theorem Separated.lift {Γ : ServiceEnv} {Δ : Context} (h : Separated Γ Δ) (k : Nat) :
    Separated Γ (Context.lift k Δ)

Uses 15 · Used by 3

Statement usesFinite endpoint ownership map · Lifting an ownership map past a binder · Separation of owned linear names from shared names · Shared service environment

Proof usesChannel name in the π-calculus · Lifting free de Bruijn indices of a π-calculus name · Endpoint capability with a dependency rank · Lookups in a rekeyed ownership map · Collision-free rekeying of an ownership map · Polarized endpoint key · Renaming the physical name of an endpoint key · Injective renamings act injectively on endpoint keys · Endpoint role on a π name · Shared service signature · Injectivity of name lifting

Used byBinding a private pair preserves separation · Environment extension preserves runtime typing under separation · Finite ranked typing embeds into runtime typing under separation

TheoremBinding a private pair preserves separation#✓fully proved

A literal private pair has variable names, never declared shared constants.

theorem Separated.bind {Γ : ServiceEnv} {Δ : Context} (h : Separated Γ Δ) (c : Capability) :
    Separated Γ (Context.bind c Δ)

Uses 13 · Used by 5

Statement usesEndpoint capability with a dependency rank · Finite endpoint ownership map · Binding a fresh dual pair under restriction · Separation of owned linear names from shared names · Shared service environment

Proof usesChannel name in the π-calculus · Dual of an endpoint capability · Lifting an ownership map past a binder · Polarized endpoint key · Endpoint role on a π name · Inserting a nonshared key preserves separation · Binder lifting preserves separation · Shared service signature

Used byEnvironment extension preserves runtime typing under separation · Finite ranked typing embeds into runtime typing under separation · Adding a restriction around nil preserves runtime typing · Typed service templates retype at any well-formed completed context · Structural congruence preserves runtime typing

TheoremSeparation restricts to the left part of a union#✓fully proved

A left child of the actual ownership union retains static shared-name separation.

theorem Separated.union_left {Γ : ServiceEnv} {Δ Θ : Context} (h : Separated Γ (Δ ∪ Θ)) :
    Separated Γ Δ

Uses 8 · Used by 3

Statement usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Polarized endpoint key · Endpoint role on a π name · Separation of owned linear names from shared names · Shared service environment

Proof usesShared service signature

Used byEnvironment extension preserves runtime typing under separation · Finite ranked typing embeds into runtime typing under separation · Runtime typing is preserved by reverse scope extrusion

TheoremSeparation restricts to the right part of a disjoint union#✓fully proved

Disjointness prevents right-child lookup shadowing by the left ownership domain.

theorem Separated.union_right {Γ : ServiceEnv} {Δ Θ : Context} (h : Separated Γ (Δ ∪ Θ))
    (hd : Finmap.Disjoint Δ Θ) : Separated Γ Θ

Uses 8 · Used by 2

Statement usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Polarized endpoint key · Endpoint role on a π name · Separation of owned linear names from shared names · Shared service environment

Proof usesShared service signature

Used byEnvironment extension preserves runtime typing under separation · Finite ranked typing embeds into runtime typing under separation

InductiveRuntime typing with guarded shared replication#✓fully proved

Ten syntax-directed rules over canonical Pi, fixed static ranks and actual ownership. Accept/serve may carry completed ambient annotations, never body capture.

Cslib.SessionTypes.Endpoint.Runtime.HasType · 46 lines

inductive HasType : Nat → ServiceEnv → Context → Proc → Prop where
  | nil {n : Nat} {Γ : ServiceEnv} {Δ : Context} :
      Δ.Completed → (∀ e ∈ Δ, e.name.ClosedAt n) → Separated Γ Δ → HasType n Γ Δ .nil
  | outName {n : Nat} {Γ : ServiceEnv} {Δ : Context} {e : Key} {c : Capability}
      {b : Name} {s : Protocol} {p : Proc} :
      GuardMin Δ e c.rank → Separated Γ Δ → Δ.lookup e = some c →
      c.protocol.unfold = .sendName s → e.name.ClosedAt n → b.ClosedAt n →
      HasType n Γ (Δ.insert e ⟨c.rank, s⟩) p → HasType n Γ Δ (.out e.name b p)
  | inpName {n : Nat} {Γ : ServiceEnv} {Δ : Context} {e : Key} {c : Capability}
      {s : Protocol} {p : Proc} :
      GuardMin Δ e c.rank → Separated Γ Δ → Δ.lookup e = some c →
      c.protocol.unfold = .recvName s → e.name.ClosedAt n →
      HasType (n + 1) Γ (Context.lift 0 (Δ.insert e ⟨c.rank, s⟩)) p →
      HasType n Γ Δ (.inp e.name p)
  | outEndpoint {n : Nat} {Γ : ServiceEnv} {Δ : Context} {e d : Key} {c v : Capability}
      {k : Nat} {t s : Protocol} {p : Proc} :
      GuardMin Δ e c.rank → Separated Γ Δ → Δ.lookup e = some c →
      c.protocol.unfold = .sendEndpoint d.role k t s → Δ.lookup d = some v →
      v.Equivalent ⟨k, t⟩ → e ≠ d → e.name.ClosedAt n → d.name.ClosedAt n →
      HasType n Γ ((Δ.erase d).insert e ⟨c.rank, s⟩) p →
      HasType n Γ Δ (.out e.name d.name p)
  | inpEndpoint {n : Nat} {Γ : ServiceEnv} {Δ : Context} {e : Key} {c : Capability}
      {r : Role} {k : Nat} {t s : Protocol} {p : Proc} :
      GuardMin Δ e c.rank → Separated Γ Δ → Δ.lookup e = some c →
      c.protocol.unfold = .recvEndpoint r k t s → e.name.ClosedAt n →
      HasType (n + 1) Γ
        ((Context.lift 0 (Δ.insert e ⟨c.rank, s⟩)).insert ⟨.var 0, r⟩ ⟨k, t⟩) p →
      HasType n Γ Δ (.inp e.name p)
  | invoke {n : Nat} {Γ : ServiceEnv} {Δ : Context} {s : Nat} {sig : ServiceSignature}
      {e : Key} {v : Capability} {p : Proc} :
      Γ.lookup s = some sig → Separated Γ Δ → Δ.lookup e = some v →
      e.role = sig.role → v.Equivalent sig.capability → InvocationPriority sig Δ →
      e.name.ClosedAt n → HasType n Γ (Δ.erase e) p → HasType n Γ Δ (.out (.const s) e.name p)
  | accept {n : Nat} {Γ : ServiceEnv} {Δ : Context} {s : Nat} {sig : ServiceSignature}
      {p : Proc} :
      Γ.lookup s = some sig → Δ.Completed → (∀ e ∈ Δ, e.name.ClosedAt n) → Separated Γ Δ →
      HasType (n + 1) Γ (Finmap.singleton ⟨.var 0, sig.role⟩ sig.capability) p →
      HasType n Γ Δ (.inp (.const s) p)
  | serve {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p : Proc} :
      ServiceTemplate Γ p → HasType n Γ ∅ p → Δ.Completed →
      (∀ e ∈ Δ, e.name.ClosedAt n) → Separated Γ Δ → HasType n Γ Δ (.repl p)
  | par {n : Nat} {Γ : ServiceEnv} {Δ Θ : Context} {p q : Proc} :
      Finmap.Disjoint Δ Θ → HasType n Γ Δ p → HasType n Γ Θ q →
      HasType n Γ (Δ ∪ Θ) (.par p q)
  | nu {n : Nat} {Γ : ServiceEnv} {Δ : Context} {c : Capability} {p : Proc} :
      Separated Γ Δ → HasType (n + 1) Γ (Context.bind c Δ) p → HasType n Γ Δ (.nu p)

Uses 19 · Used by 85

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

Used byThe state after both trigger invocations is typed · Every phase of the restricted repeated session can step · Nil is runtime-typed with empty ownership · The pending state is typed at the two-role interface · Each next phase is typed by subject reduction · Every phase is typed at the two-role interface · Every phase is typed by preservation from the pending state · The receiver daemon is typed with empty ownership · The receiver reentry request is runtime-typed · The receiver worker is runtime-typed · Steps preserve typing at the recurring interface · Repeated-session traces with typing, availability and progress · Repeated-session traces with preserved typing and availability · The sender daemon is typed with empty ownership · The sender reentry request is runtime-typed · The sender worker is runtime-typed · The state after the sender invocation is typed · Arbitrarily long typed repeated-session traces · Inversion of runtime typing for input on a shared name · Runtime-typed processes are scoped at the ambient depth · Environment extension preserves runtime typing under separation · Output on a declared shared name is a service invocation · Inversion of runtime typing for the nil process · Inversion of runtime typing for restriction · Finite ranked typing embeds into runtime typing under separation · Output subjects are owned endpoints or declared shared names · Inversion of runtime typing for parallel composition · Typed replication has a body with empty ownership · Replicated runtime processes have completed ownership · Runtime typing separates owned names from shared services · Typing rule for a replicated input on a shared name · Owned names absent from a runtime process are completed · Whole owned context of a runtime typing is scoped at ambient depth · Erasing a key whose name is absent preserves runtime typing · Each owned key of a runtime typing is scoped at ambient depth · Removing a restriction around nil preserves runtime typing · Adding a restriction around nil preserves runtime typing · Inversion of runtime typing for replication · Runtime typing transfers to an equivalent linear context · Runtime typing is invariant under equivalent linear contexts · Inversion of runtime typing for a replicated shared input · Typed replicated shared inputs are offered services · Typed service templates own only completed entries · Typed service templates retype at empty ownership · Typed service templates retype at any well-formed completed context · Weakening runtime typing by one fresh completed entry · Weakening runtime typing by a disjoint completed context · Structural congruence preserves runtime typing · Runtime typing absorbs a role absent from its parallel partner · Binder lifting preserves runtime typing · Runtime typing under renamings that fix and avoid shared names · Runtime typing restores both bound roles to the restricted side · Runtime typing is preserved by forward scope extrusion · Runtime typing is invariant under scope extrusion · Runtime typing is preserved by reverse scope extrusion · Runtime typing under substitution of a transmitted endpoint · Endpoint substitution with side conditions derived from a split · Runtime typing under passive name substitution · Binder swapping preserves runtime typing · Runtime typing reflects through binder lifting · Request-free completed runtime frontiers are service templates · Endpoint head communication preserves runtime typing · Minimum active key is the subject of a runtime frontier leaf · Guarded normal form of a typed process keeps its typing · Runtime head communication advances or keeps the interface · Runtime inputs are active linear or have completed ownership · Inversion of runtime input on a nonshared subject · Request-free runtime outputs have an active linear subject · Runtime minimum guard leaf cannot own an equivalent dual peer · Passive head communication preserves runtime typing · Shared invocation and input worker preserve the combined interface · Runtime-typed processes are congruent to a guarded normal form · Balanced runtime frontiers are idle or step given availability · Global runtime progress at balanced interfaces given availability · Closed runtime processes are idle or step given availability · Multi-step subject reduction at compatible interfaces · Multi-step subject reduction at balanced interfaces · Multi-step subject reduction at the empty interface · Qualified progress at every reachable runtime state · Qualified progress at reachable closed runtime states · Same-name linear guards at a compatible interface communicate · Choice selection is the identity on runtime-typed processes · Subject reduction for runtime typing at compatible interfaces · Subject reduction for runtime typing at balanced interfaces · Subject reduction for runtime typing at the empty interface

TheoremFinite ranked typing embeds into runtime typing under separation#✓fully proved

Real ALL7-rule induction embeds finite ranked typing, including delegation; there is no finite-judgement constructor in the new runtime typing.

theorem HasType.of_finite {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p : Proc}
    (h : Conversion.RankedType n Δ p) (hs : Separated Γ Δ) : HasType n Γ Δ p

Uses 25 · Used by 1

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Priority-ranked conversion typing judgement · Runtime typing with guarded shared replication · Separation of owned linear names from shared names · 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 · Binding a private pair preserves separation · Erasing an owned key preserves separation · Inserting a nonshared key preserves separation · Binder lifting preserves separation · Separation restricts to the left part of a union · Separation restricts to the right part of a disjoint union · Shared service signature

Used byNil is runtime-typed with empty ownership

DefinitionExtension of a shared service environment#✓fully proved

Old shared declarations retain their EXACT signature in the larger environment.

def EnvExtends (Γ Ξ : ServiceEnv) : Prop :=
  ∀ s sig, Γ.lookup s = some sig → Ξ.lookup s = some sig

Uses 2 · Used by 2

Statement usesShared service environment · Shared service signature

Used byService templates survive environment extension · Environment extension preserves runtime typing under separation

TheoremService templates survive environment extension#✓fully proved

A declared guarded template remains such under literal signature extension.

theorem ServiceTemplate.env_extend {Γ Ξ : ServiceEnv} {p : Proc}
    (h : ServiceTemplate Γ p) (he : EnvExtends Γ Ξ) : ServiceTemplate Ξ p

Uses 6 · Used by 1

Statement usesProcesses of the π-calculus · Extension of a shared service environment · Shared service environment · Structural shared-service template

Proof usesChannel name in the π-calculus · Shared service signature

Used byEnvironment extension preserves runtime typing under separation

TheoremEnvironment extension preserves runtime typing under separation#✓fully proved

General Γ-extension requires static separation of ALL actual owned names. The proof establishes fresh lifted/private/received BODY names, rather than assuming environment monotonicity or carrying a future/result field.

theorem HasType.env_extend {n : Nat} {Γ Ξ : ServiceEnv} {Δ : Context} {p : Proc}
    (h : HasType n Γ Δ p) (he : EnvExtends Γ Ξ) (hs : Separated Ξ Δ) : HasType n Ξ Δ p

Uses 30

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Extension of a shared service environment · Runtime typing with guarded shared replication · Separation of owned linear names from shared names · 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 · Binding a private pair preserves separation · Erasing an owned key preserves separation · Inserting a nonshared key preserves separation · Binder lifting preserves separation · Separation restricts to the left part of a union · Separation restricts to the right part of a disjoint union · Shared service signature · Structural shared-service template · Service templates survive environment extension · Empty ownership is separated from shared names · Singleton context with a nonshared name is separated

TheoremRuntime typing separates owned names from shared services#✓fully proved

Completed ambient annotations still obey actual shared/linear name separation.

theorem HasType.separated {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p : Proc}
    (h : HasType n Γ Δ p) : Separated Γ Δ

Uses 20 · Used by 13

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Runtime typing with guarded shared replication · Separation of owned linear names from shared names · 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 · Shared service signature · Structural shared-service template

Used byRemoving a restriction around nil preserves runtime typing · Adding a restriction around nil preserves runtime typing · Structural congruence preserves runtime typing · Runtime typing absorbs a role absent from its parallel partner · Binder lifting preserves runtime typing · Runtime typing is preserved by forward scope extrusion · Runtime typing is preserved by reverse scope extrusion · Runtime typing under substitution of a transmitted endpoint · Runtime typing under passive name substitution · Binder swapping preserves runtime typing · Shared invocation and input worker preserve the combined interface · Balanced runtime frontiers are idle or step given availability · Subject reduction for runtime typing at compatible interfaces

TheoremReplicated runtime processes have completed ownership#✓fully proved

Replication has only COMPLETED ambient ownership, not necessarily empty annotation.

theorem HasType.repl_completed {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p : Proc}
    (h : HasType n Γ Δ (.repl p)) : Δ.Completed

Uses 20 · Used by 1

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Completed 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 · 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 byInversion of runtime typing for a replicated shared input

TheoremTyped replication has a body with empty ownership#✓fully proved

Replicated BODY ownership is exactly EMPTY, while ambient annotations may be completed.

theorem HasType.repl_body_empty {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p : Proc}
    (h : HasType n Γ Δ (.repl p)) : ServiceTemplate Γ p ∧ HasType n Γ ∅ p

Uses 20 · Used by 2

Statement usesProcesses 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 · Structural shared-service template

Proof usesChannel name in the π-calculus · Name 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 · 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

Used byInversion of runtime typing for a replicated shared input · Structural congruence preserves runtime typing

TheoremRuntime-typed processes are scoped at the ambient depth#✓fully proved

Every rule derives the EXISTING canonical process-scope predicate, including fresh service parameters and empty-capture replicated template bodies.

theorem HasType.closedAt {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p : Proc}
    (h : HasType n Γ Δ p) : p.ClosedAt n

Uses 21

Statement usesProcesses of the π-calculus · Locally closed processes at a binder depth · 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

TheoremTyping rule for a replicated input on a shared name#✓fully proved

A literal shared-input replica is an admissible structural template, with its received BODY at the fresh singleton and replica BODY at EMPTY ownership.

theorem HasType.serve_input {n : Nat} {Γ : ServiceEnv} {Δ : Context} {s : Nat}
    {sig : ServiceSignature} {p : Proc} (hs : Γ.lookup s = some sig)
    (hp : HasType (n + 1) Γ (Finmap.singleton ⟨.var 0, sig.role⟩ sig.capability) p)
    (hc : Δ.Completed) (hscope : ∀ e ∈ Δ, e.name.ClosedAt n) (hd : Separated Γ Δ) :
    HasType n Γ Δ (.repl (.inp (.const s) p))

Uses 15 · 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 · Completed ownership map · Polarized endpoint key · Endpoint role on a π name · Runtime typing with guarded shared replication · Separation of owned linear names from shared names · Shared service environment · Shared service signature

Proof usesThe empty ownership map is completed · Structural shared-service template · Empty ownership is separated from shared names

Used byThe receiver daemon is typed with empty ownership · The sender daemon is typed with empty ownership

TheoremInversion of runtime typing for the nil process#✓fully proved

Nil has only actual completed, scoped, separated ambient ownership.

theorem HasType.nil_inv {n : Nat} {Γ : ServiceEnv} {Δ : Context} (h : HasType n Γ Δ .nil) :
    Δ.Completed ∧ (∀ e ∈ Δ, e.name.ClosedAt n) ∧ Separated Γ Δ

Uses 20 · 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 · Completed ownership map · Polarized endpoint key · Runtime typing with guarded shared replication · Separation of owned linear names from shared names · Shared service environment

Proof usesEquivalence of endpoint capabilities · 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 · Endpoint role on a π name · Priority of a shared invocation over active owned keys · Shared service signature · Structural shared-service template

Used byAdding a restriction around nil preserves runtime typing · Structural congruence preserves runtime typing

TheoremInversion of runtime typing for parallel composition#✓fully proved

Parallel inversion derives the actual disjoint linear split at unchanged Γ.

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

Uses 20 · Used by 7

Statement usesChannel name in the π-calculus · Processes of the π-calculus · 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

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 · 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 byStructural congruence preserves runtime typing · Runtime typing is preserved by forward scope extrusion · Runtime typing is preserved by reverse scope extrusion · Request-free completed runtime frontiers are service templates · Minimum active key is the subject of a runtime frontier leaf · Runtime head communication advances or keeps the interface · Subject reduction for runtime typing at compatible interfaces

TheoremInversion of runtime typing for restriction#✓fully proved

Restriction inversion exposes a real literal-dual bound pair, not a representative.

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

Uses 20 · Used by 5

Statement usesProcesses of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Binding a fresh dual pair under restriction · Runtime typing with guarded shared replication · Shared service environment

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 · 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 byStructural congruence preserves runtime typing · Runtime typing is preserved by forward scope extrusion · Runtime typing is preserved by reverse scope extrusion · Global runtime progress at balanced interfaces given availability · Subject reduction for runtime typing at compatible interfaces

TheoremOutput subjects are owned endpoints or declared shared names#✓fully proved

Actual output subjects are linear-owned or declared shared constants.

theorem HasType.output_subject {n : Nat} {Γ : ServiceEnv} {Δ : Context} {a b : Name} {p : Proc}
    (h : HasType n Γ Δ (.out a b p)) :
    (∃ e c, e.name = a ∧ Δ.lookup e = some c) ∨
      ∃ s sig, a = .const s ∧ Γ.lookup s = some sig

Uses 20

Statement usesChannel name in the π-calculus · Processes of the π-calculus · 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 · 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 · Priority of a shared invocation over active owned keys · Separation of owned linear names from shared names · Structural shared-service template

TheoremOutput on a declared shared name is a service invocation#✓fully proved

A declared shared output is necessarily an actual endpoint-transfer invocation.

theorem HasType.invoke_inv {n : Nat} {Γ : ServiceEnv} {Δ : Context} {s : Nat}
    {sig : ServiceSignature} {b : Name} {p : Proc}
    (h : HasType n Γ Δ (.out (.const s) b p)) (hs : Γ.lookup s = some sig) :
    ∃ e v, e.name = b ∧ Δ.lookup e = some v ∧ e.role = sig.role ∧
      v.Equivalent sig.capability ∧ InvocationPriority sig Δ ∧
      HasType n Γ (Δ.erase e) p

Uses 20 · Used by 1

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Endpoint capability with a dependency rank · Equivalence of endpoint capabilities · Finite endpoint ownership map · Polarized endpoint key · Endpoint role on a π name · Runtime typing with guarded shared replication · Priority of a shared invocation over active owned keys · Shared service environment · Shared service signature

Proof usesName scoped at a binder depth · 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 · Separation of owned linear names from shared names · Structural shared-service template

Used byShared invocation and input worker preserve the combined interface

TheoremInversion of runtime typing for input on a shared name#✓fully proved

A declared shared input has completed ambient annotations and EXACT fresh singleton BODY ownership, not captured ambient capabilities.

theorem HasType.accept_inv {n : Nat} {Γ : ServiceEnv} {Δ : Context} {s : Nat}
    {sig : ServiceSignature} {p : Proc}
    (h : HasType n Γ Δ (.inp (.const s) p)) (hs : Γ.lookup s = some sig) :
    Δ.Completed ∧ (∀ e ∈ Δ, e.name.ClosedAt n) ∧ Separated Γ Δ ∧
      HasType (n + 1) Γ (Finmap.singleton ⟨.var 0, sig.role⟩ sig.capability) p

Uses 20 · 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 · Completed ownership map · Polarized endpoint key · Endpoint role on a π name · Runtime typing with guarded shared replication · Separation of owned linear names from shared names · Shared service environment · Shared service signature

Proof usesEquivalence of endpoint capabilities · 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 · Priority of a shared invocation over active owned keys · Structural shared-service template

Used byInversion of runtime typing for a replicated shared input · Shared invocation and input worker preserve the combined interface

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.