Shared service signature to Idleness is invariant under structural congruence

StructureShared service signature#✓fully proved

Shared permission describes a transferred endpoint, not owned linear state.

structure ServiceSignature where
  priority : Nat
  role : Role
  capability : Capability

Uses 2 · Used by 102

Statement usesEndpoint capability with a dependency rank · Endpoint role on a π name

Used byAvailability of all declared services · Availability as offers of all declared signatures · Structural congruence preserves service availability · A fresh endpoint singleton is separated from the triggers · All declared services are available in the pending state · Both services are offered at every phase · Declared signature offers survive finite reduction · The receiver trigger declares the receiver signature · The receiver reentry request is runtime-typed · Receiver service signature of the recurring example · The sender trigger declares the sender signature · The sender reentry request is runtime-typed · Sender service signature of the recurring example · Service environment declaring the two triggers · Declared signature offers survive one reduction step · Service availability survives one reduction step · Service templates are invariant under structural congruence · Declared service offers are invariant under congruence · Priority of a shared invocation over active owned keys · Invocation priority for a singleton of rank above the priority · Service templates are invariant under lifting · Declared persistent service offer · Separation of owned linear names from shared names · Empty ownership is separated from shared names · Singleton context with a nonshared name is separated · Shared service environment · Structural shared-service template · Service templates are invariant under binder swapping · Erasing an owned key preserves nonaliasing · Erasing an owned key preserves separation · Name map fixing every declared shared constant · Inserting a nonshared key preserves separation · Updating an already-owned key preserves nonaliasing · Nonaliasing of owned-name images with shared constants · Every name map is nonaliasing on empty ownership · Separation gives nonaliasing for binder lifting · Separation gives nonaliasing for binder swapping · Rekeying preserves shared invocation priority · Service templates are preserved by renamings fixing shared names · Rekeying along a nonaliasing name map yields separation · Binder extension preserves fixing of shared constants · Nonaliasing survives binding a private session pair · Binder extension preserves nonaliasing of lifted contexts · Nonaliasing survives adding a received parameter under a binder · Inversion of runtime typing for input on a shared name · Binding a private pair preserves separation · Runtime-typed processes are scoped at the ambient depth · Service templates survive environment extension · Environment extension preserves runtime typing under separation · Extension of a shared service environment · Runtime typing with guarded shared replication · Output on a declared shared name is a service invocation · Binder lifting preserves separation · 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 · Separation restricts to the left part of a union · Separation restricts to the right part of a disjoint union · Owned names absent from a runtime process are completed · Erasing an owned key preserves invocation priority · Erasing a key whose name is absent preserves runtime typing · Inserting a completed entry preserves invocation priority · Each owned key of a runtime typing is scoped at ambient depth · Inversion of runtime typing for replication · Equivalent retyping preserves separation from shared names · Equivalent retyping preserves invocation priority · Runtime typing transfers to an equivalent linear context · 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 any well-formed completed context · Weakening runtime typing by one fresh completed entry · Structural congruence preserves runtime typing · Binder lifting preserves runtime typing · Request-freeness is invariant under lifting · 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 · Process with no exposed output on a declared shared name · Runtime typing under substitution of a transmitted endpoint · Runtime typing under passive name substitution · Binder swapping preserves runtime typing · Request-freeness is invariant under binder swapping · Semantic advance preserves shared-linear separation · Request-free completed runtime frontiers are service templates · Request-freeness is invariant under structural congruence · Non-request-free frontier exposes a shared output up to congruence · 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 · Exposed shared requests step when declared services are available · Shared invocation and input worker preserve the combined interface · Runtime-typed processes are congruent to a guarded normal form · Same-name linear guards at a compatible interface communicate · Choice selection is the identity on runtime-typed processes

AbbreviationShared service environment#✓fully proved

Constant-only shared names use the existing Finmap, not a new name foundation.

abbrev ServiceEnv := Finmap (fun _ : Nat => ServiceSignature)

Uses 1 · Used by 138

Statement usesShared service signature

Used byAvailability of all declared services · Availability as offers of all declared signatures · The state after both trigger invocations is typed · Every phase of the restricted repeated session can step · Structural congruence preserves service availability · Nil is runtime-typed with empty ownership · Idle processes cannot step · Idle processes have no unguarded output · The pending state is typed at the two-role interface · Declared signature offers survive finite reduction · Service availability survives finite reduction · The receiver reentry request is runtime-typed · The receiver worker is runtime-typed · The sender trigger declares the sender signature · The sender reentry request is runtime-typed · The sender worker is runtime-typed · The state after the sender invocation is typed · Service environment declaring the two triggers · Declared signature offers survive one reduction step · Service availability survives one reduction step · Service templates are invariant under structural congruence · Declared service offers are invariant under congruence · Idleness is invariant under structural congruence · Idle process as a structural service template · Service templates are invariant under lifting · Declared persistent service offer · Separation of owned linear names from shared names · Empty ownership is separated from shared names · Singleton context with a nonshared name is separated · Structural shared-service template · Service templates are invariant under binder swapping · Erasing an owned key preserves nonaliasing · Erasing an owned key preserves separation · Name map fixing every declared shared constant · Inserting a nonshared key preserves separation · Updating an already-owned key preserves nonaliasing · Nonaliasing of owned-name images with shared constants · Every name map is nonaliasing on empty ownership · Separation gives nonaliasing for binder lifting · Separation gives nonaliasing for binder swapping · Service templates are preserved by renamings fixing shared names · Rekeying along a nonaliasing name map yields separation · Binder extension preserves fixing of shared constants · 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 · Inversion of runtime typing for input on a shared name · Binding a private pair preserves separation · Runtime-typed processes are scoped at the ambient depth · Service templates survive environment extension · Environment extension preserves runtime typing under separation · Extension of a shared service environment · Runtime typing with guarded shared replication · Output on a declared shared name is a service invocation · Binder lifting preserves separation · 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 · Separation restricts to the left part of a union · Separation restricts to the right part of a disjoint union · 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 · Equivalent retyping preserves separation from shared names · 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 · Guarded frontier of guards and idle service templates · Guarded normal form: restrictions over a guarded frontier · Runtime typing absorbs a role absent from its parallel partner · Binder lifting preserves runtime typing · Request-freeness is invariant under lifting · 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 · Process with no exposed output on a declared shared name · 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 · Request-freeness is invariant under binder swapping · Runtime typing reflects through binder lifting · Semantic advance preserves shared-linear separation · Request-free completed runtime frontiers are service templates · Request-freeness is invariant under structural congruence · Endpoint head communication preserves runtime typing · Minimum active key is the subject of a runtime frontier leaf · Non-request-free frontier exposes a shared output up to congruence · 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 · Lifting preserves guarded frontiers · Lifting preserves guarded normal forms · 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 · Parallel composition preserves guarded normal forms up to congruence · Passive head communication preserves runtime typing · Service templates are request-free · Exposed shared requests step when declared services are available · 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

DefinitionSeparation of owned linear names from shared names#✓fully proved

An owned linear endpoint is never a declared shared trigger's physical name.

def Separated (Γ : ServiceEnv) (Δ : Context) : Prop :=
  ∀ e c, Δ.lookup e = some c → ∀ s sig, Γ.lookup s = some sig → e.name ≠ .const s

Uses 7 · Used by 65

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

Used byEvery phase of the restricted repeated session can step · A fresh endpoint singleton is separated from the triggers · The receiver reentry request is runtime-typed · The receiver worker is runtime-typed · The sender reentry request is runtime-typed · The sender worker is runtime-typed · Empty ownership is separated from shared names · Singleton context with a nonshared name is separated · Erasing an owned key preserves separation · Inserting a nonshared key preserves separation · Separation gives nonaliasing for binder lifting · Separation gives nonaliasing for binder swapping · Rekeying along a nonaliasing name map yields separation · Inversion of runtime typing for input on a shared name · Binding a private pair preserves separation · Runtime-typed processes are scoped at the ambient depth · Environment extension preserves runtime typing under separation · Runtime typing with guarded shared replication · Output on a declared shared name is a service invocation · Binder lifting preserves separation · 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 · Separation restricts to the left part of a union · Separation restricts to the right part of a disjoint union · Owned names absent from a runtime process are completed · 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 · Equivalent retyping preserves separation from shared names · Runtime typing transfers to an equivalent linear context · Inversion of runtime typing for a replicated shared input · Typed service templates own only completed entries · 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 · 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 · Runtime typing is preserved by forward scope extrusion · Runtime typing is preserved by reverse scope extrusion · Endpoint substitution with side conditions derived from a split · Semantic advance preserves shared-linear separation · 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 · 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 · 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 · 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

DefinitionPriority of a shared invocation over active owned keys#✓fully proved

Shared invocation precedes every actual active owned LINEAR key; none exempt.

def InvocationPriority (sig : ServiceSignature) (Δ : Context) : Prop :=
  ∀ e c, Δ.lookup e = some c → c.protocol.unfold ≠ .done → sig.priority < c.rank

Uses 8 · Used by 38

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

Used byThe receiver reentry request is runtime-typed · The sender reentry request is runtime-typed · Invocation priority for a singleton of rank above the priority · Rekeying preserves shared invocation priority · 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 · Runtime typing with guarded shared replication · Output on a declared shared name is a service invocation · Inversion of runtime typing for the nil process · Inversion of runtime typing for restriction · 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 · Owned names absent from a runtime process are completed · Erasing an owned key preserves invocation priority · Erasing a key whose name is absent preserves runtime typing · Inserting a completed entry preserves invocation priority · Each owned key of a runtime typing is scoped at ambient depth · Inversion of runtime typing for replication · Equivalent retyping preserves invocation priority · Runtime typing transfers to an equivalent linear context · Typed service templates own only completed entries · Typed service templates retype at any well-formed completed context · Weakening runtime typing by one fresh completed entry · Structural congruence preserves runtime typing · Runtime typing under renamings that fix and avoid shared names · Request-free completed runtime frontiers are service templates · 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 · Shared invocation and input worker preserve the combined interface · Runtime-typed processes are congruent to a guarded normal form · Same-name linear guards at a compatible interface communicate · Choice selection is the identity on runtime-typed processes

TheoremEmpty ownership is separated from shared names#✓fully proved

Empty captured ownership has no linear/shared alias.

theorem separated_empty (Γ : ServiceEnv) : Separated Γ ∅

Uses 8 · Used by 10

Statement usesEndpoint capability with a dependency rank · Finite endpoint ownership map · Polarized endpoint key · Separation of owned linear names from shared names · Shared service environment

Proof usesChannel name in the π-calculus · Endpoint role on a π name · Shared service signature

Used byEvery phase of the restricted repeated session can step · Nil is runtime-typed with empty ownership · The receiver daemon is typed with empty ownership · The sender daemon is typed with empty ownership · Environment extension preserves runtime typing under separation · Typing rule for a replicated input on a shared name · Typed service templates retype at empty ownership · 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

TheoremSingleton context with a nonshared name is separated#✓fully proved

A singleton received/actual endpoint is separate exactly at its own name.

theorem separated_singleton {Γ : ServiceEnv} {e : Key} {c : Capability}
    (he : ∀ s sig, Γ.lookup s = some sig → e.name ≠ .const s) :
    Separated Γ (Finmap.singleton e c)

Uses 7 · Used by 2

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

Proof usesEndpoint role on a π name

Used byA fresh endpoint singleton is separated from the triggers · Environment extension preserves runtime typing under separation

TheoremInvocation priority for a singleton of rank above the priority#✓fully proved

Singleton invocation still compares the ACTIVE payload's actual cap rank.

theorem invocation_priority_singleton (sig : ServiceSignature) (e : Key) (c : Capability)
    (hr : sig.priority < c.rank) : InvocationPriority sig (Finmap.singleton e c)

Uses 8 · Used by 2

Statement usesEndpoint capability with a dependency rank · Polarized endpoint key · Priority of a shared invocation over active owned keys · Shared service signature

Proof usesChannel name in the π-calculus · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name

Used byThe receiver reentry request is runtime-typed · The sender reentry request is runtime-typed

DefinitionStructural shared-service template#✓fully proved

A template is a structural tree of declared shared inputs, never active outputs.

def ServiceTemplate (Γ : ServiceEnv) : Proc → Prop
  | .nil => True
  | .inp a _ => ∃ s, a = .const s ∧ s ∈ Γ
  | .par p q => ServiceTemplate Γ p ∧ ServiceTemplate Γ q
  | .nu p | .repl p => ServiceTemplate Γ p
  | .out .. | .sum .. => False

Uses 4 · Used by 45

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

Used byIdle processes have no unguarded output · Service templates are invariant under structural congruence · Idle process as a structural service template · Service templates are invariant under lifting · Service templates are invariant under binder swapping · Service templates are preserved by renamings fixing shared names · Inversion of runtime typing for input on a shared name · Runtime-typed processes are scoped at the ambient depth · Service templates survive environment extension · Environment extension preserves runtime typing under separation · Runtime typing with guarded shared replication · Output on a declared shared name is a service invocation · Inversion of runtime typing for the nil process · Inversion of runtime typing for restriction · 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 · Erasing a key whose name is absent preserves runtime typing · Each owned key of a runtime typing is scoped at ambient depth · Inversion of runtime typing for replication · Runtime typing transfers to an equivalent linear context · Inversion of runtime typing for a replicated shared input · 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 · Structural congruence preserves runtime typing · Guarded frontier of guards and idle service templates · Runtime typing under renamings that fix and avoid shared names · Request-free completed runtime frontiers are service templates · Minimum active key is the subject of a runtime frontier leaf · Non-request-free frontier exposes a shared output up to congruence · Runtime head communication advances or keeps the interface · Runtime inputs are active linear or have completed ownership · Lifting preserves guarded frontiers · Inversion of runtime input on a nonshared subject · Request-free runtime outputs have an active linear subject · Service templates are request-free · Runtime-typed processes are congruent to a guarded normal form · Same-name linear guards at a compatible interface communicate · Choice selection is the identity on runtime-typed processes

TheoremService templates are invariant under lifting#✓fully proved

Canonical lifting preserves literal shared constants through every structural wrapper.

theorem ServiceTemplate.lift_iff (Γ : ServiceEnv) (k : Nat) (p : Proc) :
    ServiceTemplate Γ (liftProc k p) ↔ ServiceTemplate Γ p

Uses 8 · Used by 2

Statement usesProcesses of the π-calculus · Lifting free de Bruijn indices of a π-calculus process · Shared service environment · Structural shared-service template

Proof usesChannel name in the π-calculus · Lifting free de Bruijn indices of a π-calculus name · Shared service signature · Injectivity of name lifting

Used byService templates are invariant under structural congruence · Lifting preserves guarded frontiers

TheoremService templates are invariant under binder swapping#✓fully proved

Canonical swap preserves template guards, including wrappers under nested binders.

theorem ServiceTemplate.swap_iff (Γ : ServiceEnv) (k : Nat) (p : Proc) :
    ServiceTemplate Γ (swapProc k p) ↔ ServiceTemplate Γ p

Uses 8 · Used by 1

Statement usesProcesses of the π-calculus · Swapping adjacent binders throughout a process · Shared service environment · Structural shared-service template

Proof usesChannel name in the π-calculus · Swapping adjacent de Bruijn indices in a name · Shared service signature · Injectivity of name swapping

Used byService templates are invariant under structural congruence

TheoremService templates are invariant under structural congruence#✓fully proved

ALL16 canonical Cong constructors preserve structural guarded templates in BOTH directions.

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

Uses 10 · Used by 2

Statement usesStructural congruence of π-calculus processes · Processes of the π-calculus · Shared service environment · Structural shared-service template

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

Used byIdleness is invariant under structural congruence · Structural congruence preserves runtime typing

DefinitionUnguarded shared input on a given name#✓fully proved

Actual unguarded shared input presence through structural wrappers; input stops here.

def AcceptIn (s : Nat) : Proc → Prop
  | .inp a _ => a = .const s
  | .par p q => AcceptIn s p ∨ AcceptIn s q
  | .nu p | .repl p => AcceptIn s p
  | .nil | .out .. | .sum .. => False

Uses 2 · Used by 5

Statement usesChannel name in the π-calculus · Processes of the π-calculus

Used byUnguarded shared input communicates with a matching output · Structural congruence preserves unguarded shared inputs · Offered services have an unguarded shared input · Structural congruence preserves persistent service offers · Persistent service offer on a given name

TheoremStructural congruence preserves unguarded shared inputs#✓fully proved

All canonical congruences preserve actual shared-input presence, not execution.

theorem accept_cong {s : Nat} {p q : Proc} (h : Cong p q) :
    AcceptIn s p ↔ AcceptIn s q

Uses 10 · Used by 1

Statement usesStructural congruence of π-calculus processes · Processes of the π-calculus · Unguarded shared input on a given name

Proof usesChannel name in the π-calculus · Lifting free de Bruijn indices of a π-calculus name · Lifting free de Bruijn indices of a π-calculus process · Swapping adjacent de Bruijn indices in a name · Swapping adjacent binders throughout a process · Injectivity of name lifting · Injectivity of name swapping

Used byStructural congruence preserves persistent service offers

DefinitionPersistent service offer on a given name#✓fully proved

Persistent services expose input leaves within actual replicated structural templates.

def OfferedIn (s : Nat) : Proc → Prop
  | .repl p => AcceptIn s p
  | .par p q => OfferedIn s p ∨ OfferedIn s q
  | .nu p => OfferedIn s p
  | .nil | .inp .. | .out .. | .sum .. => False

Uses 3 · Used by 15

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Unguarded shared input on a given name

Used byAvailability of all declared services · Availability as offers of all declared signatures · Structural congruence preserves service availability · All declared services are available in the pending state · Offered service communicates with a matching shared output · Selection preserves persistent offers · Persistent service offers survive one reduction step · Both services are offered at every phase · Declared signature offers survive one reduction step · Declared service offers are invariant under congruence · Declared persistent service offer · Offered services have an unguarded shared input · Structural congruence preserves persistent service offers · Typed replicated shared inputs are offered services · Exposed shared requests step when declared services are available

TheoremOffered services have an unguarded shared input#✓fully proved

Every persistent offered service has an actual unguarded input leaf.

theorem offered_accept {s : Nat} {p : Proc} (h : OfferedIn s p) : AcceptIn s p

Uses 4 · Used by 2

Statement usesProcesses of the π-calculus · Unguarded shared input on a given name · Persistent service offer on a given name

Proof usesChannel name in the π-calculus

Used byOffered service communicates with a matching shared output · Structural congruence preserves persistent service offers

TheoremStructural congruence preserves persistent service offers#✓fully proved

ALL16 actual Cong rules preserve persistent service offering, including wrappers inside replication and actual replica unfolding. No closure constructor is used.

theorem offered_cong {s : Nat} {p q : Proc} (h : Cong p q) :
    OfferedIn s p ↔ OfferedIn s q

Uses 13 · Used by 3

Statement usesStructural congruence of π-calculus processes · Processes of the π-calculus · Persistent service offer on a given name

Proof usesChannel name in the π-calculus · Lifting free de Bruijn indices of a π-calculus name · Lifting free de Bruijn indices of a π-calculus process · Swapping adjacent de Bruijn indices in a name · Swapping adjacent binders throughout a process · Unguarded shared input on a given name · Structural congruence preserves unguarded shared inputs · Offered services have an unguarded shared input · Injectivity of name lifting · Injectivity of name swapping

Used byStructural congruence preserves service availability · Persistent service offers survive one reduction step · Declared service offers are invariant under congruence

DefinitionDeclared persistent service offer#✓fully proved

Declared signature plus actual persistent guarded service syntax, never execution data.

def Offered (Γ : ServiceEnv) (p : Proc) (s : Nat) (sig : ServiceSignature) : Prop :=
  Γ.lookup s = some sig ∧ OfferedIn s p

Uses 4 · Used by 7

Statement usesProcesses of the π-calculus · Persistent service offer on a given name · Shared service environment · Shared service signature

Used byAvailability as offers of all declared signatures · All declared services are available in the pending state · Both services are offered at every phase · Declared signature offers survive finite reduction · Declared signature offers survive one reduction step · Declared service offers are invariant under congruence · Typed replicated shared inputs are offered services

DefinitionIdle process as a structural service template#✓fully proved

Quiescent structural service templates include waiting declared inputs and wrappers.

def Idle (Γ : ServiceEnv) (p : Proc) : Prop := ServiceTemplate Γ p

Uses 3 · Used by 10

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

Used byEvery phase of the restricted repeated session can step · Idle processes cannot step · Idle processes have no unguarded output · Every phase of the repeated session can step · Idleness is invariant under structural congruence · 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 · Qualified progress at every reachable runtime state · Qualified progress at reachable closed runtime states

TheoremDeclared service offers are invariant under congruence#✓fully proved

All canonical Cong constructors preserve each actual declared persistent offer.

theorem Offered.cong_iff {Γ : ServiceEnv} {p q : Proc} {s : Nat} {sig : ServiceSignature}
    (h : Cong p q) : Offered Γ p s sig ↔ Offered Γ q s sig

Uses 7

Statement usesStructural congruence of π-calculus processes · Processes of the π-calculus · Declared persistent service offer · Shared service environment · Shared service signature

Proof usesPersistent service offer on a given name · Structural congruence preserves persistent service offers

TheoremIdleness is invariant under structural congruence#✓fully proved

Idle is precisely structural guarded-template quiescence and is Cong-invariant.

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

Uses 5 · Used by 1

Statement usesStructural congruence of π-calculus processes · Processes of the π-calculus · Idle process as a structural service template · Shared service environment

Proof usesService templates are invariant under structural congruence

Used byGlobal runtime progress at balanced interfaces given availability

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.