Inversion of runtime typing for replication to Adding a restriction around nil preserves runtime typing

TheoremInversion of runtime typing for replication#✓fully proved

General replica inversion retains completed/scoped/separated AMBIENT annotations and the structurally guarded BODY typed at EXACT EMPTY ownership.

theorem HasType.repl_inv {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p : Proc}
    (h : HasType n Γ Δ (.repl p)) :
    Δ.Completed ∧ (∀ e ∈ Δ, e.name.ClosedAt n) ∧ Separated Γ Δ ∧
      ServiceTemplate Γ p ∧ HasType n Γ ∅ p

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

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

Used byStructural congruence preserves runtime typing

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

A literal input template exposes its declared signature and fresh received BODY; completed ambient annotations are NOT inherited by that BODY.

theorem HasType.service_inv {n : Nat} {Γ : ServiceEnv} {Δ : Context} {s : Nat} {p : Proc}
    (h : HasType n Γ Δ (.repl (.inp (.const s) p))) :
    ∃ sig, Δ.Completed ∧ Γ.lookup s = some sig ∧
      HasType (n + 1) Γ (Finmap.singleton ⟨.var 0, sig.role⟩ sig.capability) p

Uses 16 · Used by 1

Statement usesChannel name in the π-calculus · 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 · Shared service environment · Shared service signature

Proof usesName scoped at a binder depth · Inversion of runtime typing for input on a shared name · Typed replication has a body with empty ownership · Replicated runtime processes have completed ownership · Separation of owned linear names from shared names · Structural shared-service template

Used byTyped replicated shared inputs are offered services

TheoremTyped replicated shared inputs are offered services#✓fully proved

Typing-derived actual literal-input offering survives completed ambient annotations.

theorem HasType.service_offered {n : Nat} {Γ : ServiceEnv} {Δ : Context} {s : Nat} {p : Proc}
    (h : HasType n Γ Δ (.repl (.inp (.const s) p))) :
    ∃ sig, Offered Γ (.repl (.inp (.const s) p)) s sig

Uses 13

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Finite endpoint ownership map · Runtime typing with guarded shared replication · Declared persistent service offer · Shared service environment · Shared service signature

Proof usesEndpoint capability with a dependency rank · Completed ownership map · Polarized endpoint key · Endpoint role on a π name · Inversion of runtime typing for a replicated shared input · Persistent service offer on a given name

TheoremInserting a completed entry preserves invocation priority#✓fully proved

A completed frame is ignored by shared priority, with NO active-payload exemption.

theorem InvocationPriority.insert_completed {sig : ServiceSignature} {Δ : Context}
    (h : InvocationPriority sig Δ) {z : Key} {u : Capability} (hu : u.protocol.unfold = .done) :
    InvocationPriority sig (Δ.insert z u)

Uses 9 · Used by 1

Statement usesChannel name in 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 · Priority of a shared invocation over active owned keys · Shared service signature

Used byWeakening runtime typing by one fresh completed entry

TheoremWeakening runtime typing by one fresh completed entry#✓fully proved

ALL10 rules admit a fresh COMPLETED ambient annotation. Its name is scoped and nonshared; accept/serve BODY ownership is unchanged, never captured.

theorem HasType.weaken_completed {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p : Proc}
    (h : HasType n Γ Δ p) {z : Key} {u : Capability} (hz : z ∉ Δ)
    (hu : u.protocol.unfold = .done) (hscope : z.name.ClosedAt n)
    (hshared : ∀ s sig, Γ.lookup s = some sig → z.name ≠ .const s) :
    HasType n Γ (Δ.insert z u) p

Uses 36 · 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 · 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 usesLifting free de Bruijn indices of a π-calculus name · Equivalence of endpoint capabilities · Completed ownership map · Inserting a completed capability preserves completion · Binding a fresh dual pair under restriction · Restriction binding commutes with inserting an outer key · Inserting a key absent from the other side preserves disjointness · Erasing a different key commutes with insertion · Restriction binding preserves absence of an outer key · Updating an owned key keeps absent keys absent · Lifting preserves absence of a key · Lifting an ownership map past a binder · Context lifting commutes with insertion · Guard priority condition on active endpoints · Adding a completed role preserves the guard condition · A lifted key is never a freshly bound key · Renaming the physical name of an endpoint key · Priority of a shared invocation over active owned keys · Inserting a completed entry preserves invocation priority · Separation of owned linear names from shared names · Inserting a nonshared key preserves separation · Structural shared-service template · Lifting preserves and reflects name scoping · Injectivity of name lifting

Used byWeakening runtime typing by a disjoint completed context · Runtime typing absorbs a role absent from its parallel partner

TheoremWeakening runtime typing by a disjoint completed context#✓fully proved

A disjoint completed/scoped/nonshared finite ambient frame can be reattached. The actual replica/accept BODY is not expanded by those annotations.

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

Uses 17 · 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

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 runtime typing by one fresh completed entry · Erasing an owned key preserves separation

Used byStructural congruence preserves runtime typing · Shared invocation and input worker preserve the combined interface

TheoremErasing an owned key preserves invocation priority#✓fully proved

Removing an owned key preserves the shared priority inequalities on the remainder.

theorem InvocationPriority.erase {sig : ServiceSignature} {Δ : Context}
    (h : InvocationPriority sig Δ) (z : Key) : InvocationPriority sig (Δ.erase z)

Uses 9 · Used by 1

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

Proof usesEndpoint protocol with guarded regular recursion · One-step unfolding of a protocol

Used byErasing a key whose name is absent preserves runtime typing

TheoremOwned names absent from a runtime process are completed#✓fully proved

An owned name absent from ALL subject/payload/binder-adjusted positions already has an actual done unfolding, including in the shared runtime rules.

theorem HasType.absent_lookup_completed {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p : Proc}
    (h : HasType n Γ Δ p) {z : Key} {t : Capability}
    (hz : Δ.lookup z = some t) (hab : NameAbsent z.name p) : t.protocol.unfold = .done

Uses 26 · Used by 1

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Polarized endpoint key · Absence of a physical name from a process · 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 · Lifting free de Bruijn indices of a π-calculus name · 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 · Lookups in a lifted ownership map · Guard priority condition on active endpoints · A lifted key is never a freshly bound key · Renaming the physical name of an endpoint key · 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 byRuntime typing absorbs a role absent from its parallel partner

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

ALL10 runtime rules support erasure only under real all-position absence. Accept/serve ambient erasure does NOT alter their exact fresh/empty BODY domains.

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

Uses 33 · Used by 1

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Polarized endpoint key · Absence of a physical name from a process · Endpoint role on a π name · Runtime typing with guarded shared replication · Shared service environment

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

Used byRuntime typing is preserved by reverse scope extrusion

TheoremEquivalent retyping preserves separation from shared names#✓fully proved

Semantic capability changes do not change owned physical names or Γ separation.

theorem Separated.retype {Γ : ServiceEnv} {Δ Ξ : Context} (hs : Separated Γ Δ)
    (he : ContextEquivalent Δ Ξ) : Separated Γ Ξ

Uses 12 · Used by 1

Statement usesFinite endpoint ownership map · Pointwise equivalence of ownership maps · Separation of owned linear names from shared names · Shared service environment

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 · Polarized endpoint key · Endpoint role on a π name · Shared service signature

Used byRuntime typing transfers to an equivalent linear context

TheoremEquivalent retyping preserves invocation priority#✓fully proved

Actual active-payload ranks preserve the strict shared invocation priority.

theorem InvocationPriority.retype {sig : ServiceSignature} {Δ Ξ : Context}
    (hg : InvocationPriority sig Δ) (he : ContextEquivalent Δ Ξ) : InvocationPriority sig Ξ

Uses 15 · Used by 1

Statement usesFinite endpoint ownership map · Pointwise equivalence of ownership maps · Priority of a shared invocation over active owned keys · Shared service signature

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 · Polarized 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 byRuntime typing transfers to an equivalent linear context

TheoremRuntime typing transfers to an equivalent linear context#✓fully proved

ALL10 runtime rules retype at arbitrary equivalent linear contexts, with Γ UNCHANGED. Actual payload codes, literal cap ranks and empty BODY contexts are retained.

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

Uses 39 · Used by 2

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Pointwise equivalence of ownership maps · 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 · 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 · Priority of a shared invocation over active owned keys · Equivalent retyping preserves invocation priority · Separation of owned linear names from shared names · Equivalent retyping preserves separation from shared names · Shared service signature · Structural shared-service template

Used byRuntime typing is invariant under equivalent linear contexts · Runtime typing under substitution of a transmitted endpoint

TheoremRuntime typing is invariant under equivalent linear contexts#✓fully proved

Equivalent linear interfaces preserve runtime typing in BOTH directions at exactly the same shared environment, process and ambient depth.

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

Uses 7

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Pointwise equivalence of ownership maps · Runtime typing with guarded shared replication · Shared service environment

Proof usesSymmetry of ownership-map equivalence · Runtime typing transfers to an equivalent linear context

TheoremEach owned key of a runtime typing is scoped at ambient depth#✓fully proved

Every actual owned key is scoped at the runtime derivation's ambient depth.

theorem HasType.lookup_closedAt {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p : Proc}
    (h : HasType n Γ Δ p) {z : Key} {t : Capability} (hz : Δ.lookup z = some t) :
    z.name.ClosedAt n

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

Proof usesLifting free de Bruijn indices of a π-calculus name · 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 · Lookups in a lifted ownership map · Guard priority condition on active endpoints · A lifted key is never a freshly bound key · Renaming the physical name of an endpoint key · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Priority of a shared invocation over active owned keys · Separation of owned linear names from shared names · Shared service signature · Structural shared-service template · Lifting preserves and reflects name scoping

Used byWhole owned context of a runtime typing is scoped at ambient depth · Shared invocation and input worker preserve the combined interface

TheoremWhole owned context of a runtime typing is scoped at ambient depth#✓fully proved

Scope applies to the actual complete owned domain, not only active subjects.

theorem HasType.context_closedAt {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p : Proc}
    (h : HasType n Γ Δ p) : ∀ e ∈ Δ, e.name.ClosedAt n

Uses 10 · 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 · Polarized endpoint key · Runtime typing with guarded shared replication · Shared service environment

Proof usesEndpoint role on a π name · Each owned key of a runtime typing is scoped at ambient depth

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

TheoremTyped service templates own only completed entries#✓fully proved

A typed structurally guarded template owns only completed AMBIENT entries. Its input and replica BODY proofs remain separate and may use their own formal key.

theorem HasType.template_completed {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p : Proc}
    (h : HasType n Γ Δ p) (ht : ServiceTemplate Γ p) : Δ.Completed

Uses 25 · Used by 4

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Completed ownership map · 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 · Lifting free de Bruijn indices of a π-calculus name · Endpoint capability with a dependency rank · Equivalence of endpoint capabilities · Dual of an endpoint capability · Binding a fresh dual pair under restriction · Lifting an ownership map past a binder · Lookups in a lifted ownership map · Guard priority condition on active endpoints · Polarized endpoint key · A lifted key is never a freshly bound key · Renaming the physical name of an endpoint key · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · 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 byRemoving a restriction around nil preserves runtime typing · Typed service templates retype at any well-formed completed context · Structural congruence preserves runtime typing · Minimum active key is the subject of a runtime frontier leaf

TheoremTyped service templates retype at any well-formed completed context#✓fully proved

Structurally guarded typed templates can replace only their COMPLETED ambient annotations. Fresh input/empty replica BODY proofs are retained unchanged.

theorem HasType.template_reannotate {n : Nat} {Γ : ServiceEnv} {Δ Θ : Context} {p : Proc}
    (h : HasType n Γ Δ p) (ht : ServiceTemplate Γ p) (hc : Θ.Completed)
    (hs : ∀ e ∈ Θ, e.name.ClosedAt n) (hd : Separated Γ Θ) : HasType n Γ Θ p

Uses 37 · 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 · Structural shared-service template

Proof usesLifting free de Bruijn indices of a π-calculus name · Equivalence of endpoint capabilities · Dual of an endpoint capability · Inserting a completed capability preserves completion · Rekeying preserves completion · Binding a fresh dual pair under restriction · The empty ownership map is completed · Lifting an ownership map past a binder · Positive role lookup after restriction binding · Keys of a rekeyed ownership map · Collision-free rekeying of an ownership map · Guard priority condition on active endpoints · Renaming the physical name of an endpoint key · Injective renamings act injectively on endpoint keys · Endpoint protocol with guarded regular recursion · Dual of an endpoint protocol · One-step unfolding of a protocol · Unfolding commutes with protocol duality · Endpoint role on a π name · Typed service templates own only completed entries · Priority of a shared invocation over active owned keys · Binding a private pair preserves separation · Shared service signature · Empty ownership is separated from shared names · Lifting preserves and reflects name scoping · Injectivity of name lifting

Used byTyped service templates retype at empty ownership · Structural congruence preserves runtime typing

TheoremTyped service templates retype at empty ownership#✓fully proved

Clearing completed template annotations produces the EXACT empty BODY required by replica admission; this is not unconditional active-resource erasure.

theorem HasType.template_empty {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p : Proc}
    (h : HasType n Γ Δ p) (ht : ServiceTemplate Γ p) : HasType n Γ ∅ p

Uses 12 · Used by 1

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 · The empty ownership map is completed · Typed service templates retype at any well-formed completed context · Empty ownership is separated from shared names

Used byStructural congruence preserves runtime typing

TheoremRemoving a restriction around nil preserves runtime typing#✓fully proved

Removing a nil restriction retains its actual completed/scoped/separated ambient.

theorem HasType.nu_nil_elim {n : Nat} {Γ : ServiceEnv} {Δ : Context}
    (h : HasType n Γ Δ (.nu .nil)) : HasType n Γ Δ .nil

Uses 13 · Used by 1

Statement usesProcesses of 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 · Completed ownership map · Polarized endpoint key · Whole owned context of a runtime typing is scoped at ambient depth · Runtime typing separates owned names from shared services · Typed service templates own only completed entries · Separation of owned linear names from shared names

Used byStructural congruence preserves runtime typing

TheoremAdding a restriction around nil preserves runtime typing#✓fully proved

Introducing a nil restriction chooses a genuinely completed literal-dual pair.

theorem HasType.nu_nil_intro {n : Nat} {Γ : ServiceEnv} {Δ : Context}
    (h : HasType n Γ Δ .nil) : HasType n Γ Δ (.nu .nil)

Uses 30 · Used by 1

Statement usesProcesses of 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 · Lifting free de Bruijn indices of a π-calculus name · Endpoint capability with a dependency rank · Dual of an endpoint capability · Completed ownership map · Inserting a completed capability preserves completion · Rekeying preserves completion · Binding a fresh dual pair under restriction · Lifting an ownership map past a binder · Keys of 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 protocol with guarded regular recursion · Dual of an endpoint protocol · One-step unfolding of a protocol · Unfolding commutes with protocol duality · Endpoint role on a π name · Inversion of runtime typing for the nil process · Runtime typing separates owned names from shared services · Separation of owned linear names from shared names · Binding a private pair preserves separation · Lifting preserves and reflects name scoping · Injectivity of name lifting

Used byStructural congruence preserves runtime typing

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.