Name map fixing every declared shared constant to Inserting a nonshared key preserves separation

DefinitionName map fixing every declared shared constant#✓fully proved

A name map leaves every declared shared constant literally fixed.

def FixesShared (Γ : ServiceEnv) (f : Name → Name) : Prop :=
  ∀ s sig, Γ.lookup s = some sig → f (.const s) = .const s

Uses 3 · Used by 3

Statement usesChannel name in the π-calculus · Shared service environment · Shared service signature

Used byService templates are preserved by renamings fixing shared names · Binder extension preserves fixing of shared constants · Runtime typing under renamings that fix and avoid shared names

DefinitionNonaliasing of owned-name images with shared constants#✓fully proved

Actual owned-key images cannot alias a declared shared physical name.

def NonAliases (Γ : ServiceEnv) (Δ : Context) (f : Name → Name) : Prop :=
  ∀ e ∈ Δ, ∀ s sig, Γ.lookup s = some sig → f e.name ≠ .const s

Uses 6 · Used by 14

Statement usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Polarized endpoint key · Shared service environment · Shared service signature

Used byErasing an owned key preserves nonaliasing · Updating an already-owned key preserves nonaliasing · Every name map is nonaliasing on empty ownership · Separation gives nonaliasing for binder lifting · Separation gives nonaliasing for binder swapping · Rekeying along a nonaliasing name map yields separation · Nonaliasing survives binding a private session pair · Binder extension preserves nonaliasing of lifted contexts · Nonaliasing survives adding a received parameter under a binder · Nonaliasing restricts to the left part of a union · Nonaliasing restricts to the right part of a union · Passive substitution creates no owned shared-name alias · Nonshared endpoint substitution keeps owned names nonshared · Runtime typing under renamings that fix and avoid shared names

TheoremBinder extension preserves fixing of shared constants#✓fully proved

Binder extension still fixes shared constants, which are unchanged by lifting.

theorem FixesShared.under {Γ : ServiceEnv} {f : Name → Name} (h : FixesShared Γ f) :
    FixesShared Γ (under f)

Uses 6 · Used by 2

Statement usesChannel name in the π-calculus · Name map fixing every declared shared constant · Shared service environment · Extension of a name map under a binder

Proof usesLifting free de Bruijn indices of a π-calculus name · Shared service signature

Used byService templates are preserved by renamings fixing shared names · Runtime typing under renamings that fix and avoid shared names

TheoremRekeying along a nonaliasing name map yields separation#✓fully proved

The actual target ownership rekey has static name separation, not a desired type result.

theorem NonAliases.separated {Γ : ServiceEnv} {Δ : Context} {f : Name → Name}
    (h : NonAliases Γ Δ f) (hf : Set.InjOn (Key.mapName f) {e | e ∈ Δ}) :
    Separated Γ (Context.rekey (Key.mapName f) Δ hf)

Uses 12 · Used by 1

Statement usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Collision-free rekeying of an ownership map · Polarized endpoint key · Renaming the physical name of an endpoint key · Nonaliasing of owned-name images with shared constants · Separation of owned linear names from shared names · Shared service environment

Proof usesLookups in a rekeyed ownership map · Endpoint role on a π name · Shared service signature

Used byRuntime typing under renamings that fix and avoid shared names

TheoremErasing an owned key preserves nonaliasing#✓fully proved

Erasure restricts the actual owned domain and cannot add a name-map alias.

theorem NonAliases.erase {Γ : ServiceEnv} {Δ : Context} {f : Name → Name}
    (h : NonAliases Γ Δ f) (e : Key) : NonAliases Γ (Δ.erase e) f

Uses 8 · 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 · Nonaliasing of owned-name images with shared constants · Shared service environment

Proof usesShared service signature

Used byRuntime typing under renamings that fix and avoid shared names

TheoremUpdating an already-owned key preserves nonaliasing#✓fully proved

Advancing an already-owned key leaves the name-map domain unchanged.

theorem NonAliases.insert_owned {Γ : ServiceEnv} {Δ : Context} {f : Name → Name}
    (h : NonAliases Γ Δ f) {e : Key} (he : e ∈ Δ) (c : Capability) :
    NonAliases Γ (Δ.insert e c) f

Uses 8 · 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 · Nonaliasing of owned-name images with shared constants · Shared service environment

Proof usesShared service signature

Used byRuntime typing under renamings that fix and avoid shared names

TheoremEvery name map is nonaliasing on empty ownership#✓fully proved

Empty BODY ownership imposes no linear-image nonalias obligations.

theorem nonaliases_empty (Γ : ServiceEnv) (f : Name → Name) : NonAliases Γ ∅ f

Uses 7 · Used by 1

Statement usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Polarized endpoint key · Nonaliasing of owned-name images with shared constants · Shared service environment

Proof usesShared service signature

Used byRuntime typing under renamings that fix and avoid shared names

TheoremBinder extension preserves nonaliasing of lifted contexts#✓fully proved

Binder extension maps lifted owned names to lifted images, never new shared constants.

theorem NonAliases.under_lift {Γ : ServiceEnv} {Δ : Context} {f : Name → Name}
    (h : NonAliases Γ Δ f) : NonAliases Γ (Context.lift 0 Δ) (under f)

Uses 16 · Used by 3

Statement usesChannel name in the π-calculus · Finite endpoint ownership map · Lifting an ownership map past a binder · Nonaliasing of owned-name images with shared constants · Shared service environment · Extension of a name map under a binder

Proof usesLifting free de Bruijn indices of a π-calculus name · Endpoint capability with a dependency rank · 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 · Shared service signature · Injectivity of name lifting · Extended name map commutes with lifting outer names

Used byNonaliasing survives binding a private session pair · Nonaliasing survives adding a received parameter under a binder · Runtime typing under renamings that fix and avoid shared names

TheoremNonaliasing survives adding a received parameter under a binder#✓fully proved

A newly received parameter remains var0 under the canonical binder map.

theorem NonAliases.under_received {Γ : ServiceEnv} {Δ : Context} {f : Name → Name}
    (h : NonAliases Γ Δ f) (r : Role) (c : Capability) :
    NonAliases Γ ((Context.lift 0 Δ).insert ⟨.var 0, r⟩ c) (under f)

Uses 11 · Used by 1

Statement usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Lifting an ownership map past a binder · Polarized endpoint key · Endpoint role on a π name · Nonaliasing of owned-name images with shared constants · Shared service environment · Extension of a name map under a binder

Proof usesBinder extension preserves nonaliasing of lifted contexts · Shared service signature

Used byRuntime typing under renamings that fix and avoid shared names

TheoremNonaliasing survives binding a private session pair#✓fully proved

Both private-role keys are fresh var0; only actual outer names need nonalias transport.

theorem NonAliases.under_bind {Γ : ServiceEnv} {Δ : Context} {f : Name → Name}
    (h : NonAliases Γ Δ f) (c : Capability) : NonAliases Γ (Context.bind c Δ) (under f)

Uses 13 · Used by 1

Statement usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Binding a fresh dual pair under restriction · Nonaliasing of owned-name images with shared constants · Shared service environment · Extension of a name map under a binder

Proof usesDual of an endpoint capability · Lifting an ownership map past a binder · Polarized endpoint key · Endpoint role on a π name · Binder extension preserves nonaliasing of lifted contexts · Shared service signature

Used byRuntime typing under renamings that fix and avoid shared names

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

Actual left-domain restriction of an ownership union preserves map nonalias.

theorem NonAliases.union_left {Γ : ServiceEnv} {Δ Θ : Context} {f : Name → Name}
    (h : NonAliases Γ (Δ ∪ Θ) f) : NonAliases Γ Δ f

Uses 7 · 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 · Nonaliasing of owned-name images with shared constants · Shared service environment

Used byRuntime typing under renamings that fix and avoid shared names

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

Actual right-domain restriction likewise preserves map nonalias.

theorem NonAliases.union_right {Γ : ServiceEnv} {Δ Θ : Context} {f : Name → Name}
    (h : NonAliases Γ (Δ ∪ Θ) f) : NonAliases Γ Θ f

Uses 7 · 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 · Nonaliasing of owned-name images with shared constants · Shared service environment

Used byRuntime typing under renamings that fix and avoid shared names

TheoremService templates are preserved by renamings fixing shared names#✓fully proved

Structural templates transport through a declared-constant-fixing name map; input BODY typing is handled separately, not hidden in this shape predicate.

theorem ServiceTemplate.rename {Γ : ServiceEnv} {p : Proc} {f : Name → Name}
    (h : ServiceTemplate Γ p) (hf : FixesShared Γ f) : ServiceTemplate Γ (mapProc f p)

Uses 9 · Used by 1

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Name map fixing every declared shared constant · Shared service environment · Structural shared-service template · Capture-safe renaming of processes

Proof usesBinder extension preserves fixing of shared constants · Shared service signature · Extension of a name map under a binder

Used byRuntime typing under renamings that fix and avoid shared names

TheoremRekeying preserves shared invocation priority#✓fully proved

Rekeying retains actual cap values and therefore shared-priority comparisons.

theorem InvocationPriority.rekey {sig : ServiceSignature} {Δ : Context} {f : Name → Name}
    (h : InvocationPriority sig Δ) (hf : Set.InjOn (Key.mapName f) {e | e ∈ Δ}) :
    InvocationPriority sig (Context.rekey (Key.mapName f) Δ hf)

Uses 12 · Used by 1

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

Proof usesLookups in a rekeyed ownership map · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name

Used byRuntime typing under renamings that fix and avoid shared names

TheoremRekeying the empty context gives the empty context#✓fully proved

An empty owned context stays empty under the canonical context rekey operation.

theorem rekey_empty (f : Name → Name)
    (hf : Set.InjOn (Key.mapName f) {e | e ∈ (∅ : Context)}) :
    Context.rekey (Key.mapName f) ∅ hf = ∅

Uses 8 · Used by 1

Statement usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Collision-free rekeying of an ownership map · Polarized endpoint key · Renaming the physical name of an endpoint key

Proof usesKeys of a rekeyed ownership map · Endpoint role on a π name

Used byRuntime typing under renamings that fix and avoid shared names

TheoremRekeying a singleton moves its key and keeps its capability#✓fully proved

Rekeying a singleton moves its actual key and retains its capability verbatim.

theorem rekey_singleton (f : Name → Name) (e : Key) (c : Capability)
    (hf : Set.InjOn (Key.mapName f) {d | d ∈ (Finmap.singleton e c : Context)}) :
    Context.rekey (Key.mapName f) (Finmap.singleton e c) hf =
      Finmap.singleton (Key.mapName f e) c

Uses 9 · Used by 1

Statement usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Collision-free rekeying of an ownership map · Polarized endpoint key · Renaming the physical name of an endpoint key

Proof usesLookups in a rekeyed ownership map · Keys of a rekeyed ownership map · Endpoint role on a π name

Used byRuntime typing under renamings that fix and avoid shared names

TheoremSeparation gives nonaliasing for binder lifting#✓fully proved

Canonical binder lifting cannot send a nonshared owned name into the shared namespace.

theorem Separated.nonaliases_lift {Γ : ServiceEnv} {Δ : Context} (h : Separated Γ Δ) (k : Nat) :
    NonAliases Γ Δ (liftName k)

Uses 11 · Used by 1

Statement usesLifting free de Bruijn indices of a π-calculus name · Finite endpoint ownership map · Nonaliasing of owned-name images with shared constants · Separation of owned linear names from shared names · Shared service environment

Proof usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Polarized endpoint key · Endpoint role on a π name · Shared service signature · Injectivity of name lifting

Used byBinder lifting preserves runtime typing

TheoremSeparation gives nonaliasing for binder swapping#✓fully proved

Canonical binder swapping likewise preserves actual owned-name nonalias.

theorem Separated.nonaliases_swap {Γ : ServiceEnv} {Δ : Context} (h : Separated Γ Δ) (k : Nat) :
    NonAliases Γ Δ (swapNameAt k)

Uses 11 · Used by 1

Statement usesSwapping adjacent de Bruijn indices in a name · Finite endpoint ownership map · Nonaliasing of owned-name images with shared constants · Separation of owned linear names from shared names · Shared service environment

Proof usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Polarized endpoint key · Endpoint role on a π name · Shared service signature · Injectivity of name swapping

Used byBinder swapping preserves runtime typing

TheoremErasing an owned key preserves separation#✓fully proved

Erasing an actual owned key cannot create a shared/linear name alias.

theorem Separated.erase {Γ : ServiceEnv} {Δ : Context} (h : Separated Γ Δ) (e : Key) :
    Separated Γ (Δ.erase e)

Uses 8 · Used by 4

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 · Erasing a key whose name is absent preserves runtime typing · Weakening runtime typing by a disjoint completed context

TheoremInserting a nonshared key preserves separation#✓fully proved

Inserting a statically nonshared key preserves physical-name separation.

theorem Separated.insert {Γ : ServiceEnv} {Δ : Context} (h : Separated Γ Δ)
    (e : Key) (c : Capability) (he : ∀ s sig, Γ.lookup s = some sig → e.name ≠ .const s) :
    Separated Γ (Δ.insert e c)

Uses 8 · Used by 4

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 · Shared service signature

Used byBinding a private pair preserves separation · Environment extension preserves runtime typing under separation · Finite ranked typing embeds into runtime typing under separation · Weakening runtime typing by one fresh completed entry

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.