Recursive sessions through replicated services

TheoremSelection preserves persistent offers#✓fully proved

Choice selection cannot discard a persistent SOURCE offer: sums do not expose OfferedIn, and selecting an actual communicating guard exposes no persistent offer.

theorem offered_select {s : Nat} {p q : Proc} (h : Select p q) :
    OfferedIn s p → OfferedIn s q

Uses 3 · Used by 1

Statement usesProcesses of the π-calculus · Guarded-choice resolution in the π-calculus · Persistent service offer on a given name

Used byPersistent service offers survive one reduction step

TheoremPersistent service offers survive one reduction step#✓fully proved

ALL5 canonical Step rules retain every actual persistent source service offer. This is valid for arbitrary Pi syntax, WITHOUT a HasType premise.

theorem offered_step {s : Nat} {p q : Proc} (h : PiCalculus.Step p q) :
    OfferedIn s p → OfferedIn s q

Uses 9 · Used by 2

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Persistent service offer on a given name

Proof usesStructural congruence of π-calculus processes · Channel name in the π-calculus · Guarded-choice resolution in the π-calculus · Substitution for the innermost bound variable of a process · Structural congruence preserves persistent service offers · Selection preserves persistent offers

Used byDeclared signature offers survive one reduction step · Service availability survives one reduction step

TheoremDeclared signature offers survive one reduction step#✓fully proved

Exact declared signature lookup plus an actual persistent offer is retained by every canonical Step, at unchanged shared environment/signature.

theorem Offered.step {Γ : ServiceEnv} {s : Nat} {sig : ServiceSignature} {p q : Proc}
    (h : Offered Γ p s sig) (hs : PiCalculus.Step p q) : Offered Γ q s sig

Uses 7 · Used by 1

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Declared persistent service offer · Shared service environment · Shared service signature

Proof usesPersistent service offer on a given name · Persistent service offers survive one reduction step

Used byDeclared signature offers survive finite reduction

TheoremDeclared signature offers survive finite reduction#✓fully proved

Every finite actual reduction preserves each SOURCE persistent signature offer. No liveness, all-schedules fairness or eventual service invocation is asserted.

theorem Offered.reachable {Γ : ServiceEnv} {s : Nat} {sig : ServiceSignature} {p q : Proc}
    (h : Offered Γ p s sig) (hr : Relation.ReflTransGen PiCalculus.Step p q) :
    Offered Γ q s sig

Uses 6

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Declared persistent service offer · Shared service environment · Shared service signature

Proof usesDeclared signature offers survive one reduction step

DefinitionAvailability of all declared services#✓fully proved

Every declared shared signature has an ACTUAL persistent offer in current syntax. There is NO typing, Step, future trace, ready pair or step-closure field.

def Available (Γ : ServiceEnv) (p : Proc) : Prop :=
  ∀ s sig, Γ.lookup s = some sig → OfferedIn s p

Uses 4 · Used by 14

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 · Structural congruence preserves service availability · All declared services are available in the pending state · Services stay available at every phase · Service availability survives finite reduction · Repeated-session traces with typing, availability and progress · Repeated-session traces with preserved typing and availability · Service availability survives one reduction step · Exposed shared requests step when declared services are available · 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

TheoremAvailability as offers of all declared signatures#✓fully proved

Availability is exactly current declared signature lookup plus persistent syntax.

theorem available_iff_offered {Γ : ServiceEnv} {p : Proc} :
    Available Γ p ↔ ∀ s sig, Γ.lookup s = some sig → Offered Γ p s sig

Uses 6

Statement usesProcesses of the π-calculus · Availability of all declared services · Declared persistent service offer · Shared service environment · Shared service signature

Proof usesPersistent service offer on a given name

TheoremStructural congruence preserves service availability#✓fully proved

All canonical structural laws preserve current syntactic availability.

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

Uses 7 · Used by 2

Statement usesStructural congruence of π-calculus processes · Processes of the π-calculus · Availability of all declared services · Shared service environment

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

Used byExposed shared requests step when declared services are available · Global runtime progress at balanced interfaces given availability

TheoremService availability survives one reduction step#✓fully proved

Strong actual syntactic availability survives ANY canonical Step.

theorem Available.step {Γ : ServiceEnv} {p q : Proc} (h : Available Γ p)
    (hs : PiCalculus.Step p q) : Available Γ q

Uses 6 · Used by 1

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Availability of all declared services · Shared service environment

Proof usesShared service signature · Persistent service offers survive one reduction step

Used byService availability survives finite reduction

TheoremService availability survives finite reduction#✓fully proved

Finite actual reductions preserve source syntactic availability; preservation is PROVED here, not encoded into its definition. This is not a progress theorem.

theorem Available.reachable {Γ : ServiceEnv} {p q : Proc} (h : Available Γ p)
    (hr : Relation.ReflTransGen PiCalculus.Step p q) : Available Γ q

Uses 5 · Used by 3

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Availability of all declared services · Shared service environment

Proof usesService availability survives one reduction step

Used byServices stay available at every phase · Qualified progress at every reachable runtime state · Qualified progress at reachable closed runtime states

TheoremIdle processes have no unguarded output#✓fully proved

Idle is syntax-only and excludes a canonical exposed output, including inside parallel, restriction and inert replicated templates.

theorem Idle.no_unguarded_output {Γ : ServiceEnv} {p : Proc} (h : Idle Γ p) :
    ¬ PiCalculus.HasUnguardedOutput p

Uses 6 · Used by 3

Statement usesUnguarded output in a process · Processes of the π-calculus · Idle process as a structural service template · Shared service environment

Proof usesChannel name in the π-calculus · Structural shared-service template

Used byEvery phase of the restricted repeated session can step · Idle processes cannot step · Every phase of the repeated session can step

TheoremIdle processes cannot step#✓fully proved

Idle services cannot Step, even through arbitrary canonical congruence.

theorem Idle.no_step {Γ : ServiceEnv} {p : Proc} (h : Idle Γ p) (q : Proc) :
    ¬ PiCalculus.Step p q

Uses 6

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Idle process as a structural service template · Shared service environment

Proof usesEvery reduction source has an unguarded output · Idle processes have no unguarded output

TheoremInvoking a replicated service is a reduction step#✓fully proved

Canonical replication unfolds and communicates on a real shared trigger.

theorem service_invocation_step (s : Nat) (b : Name) (body : Proc) :
    PiCalculus.Step (.par (.out (.const s) b .nil) (.repl (.inp (.const s) body)))
      (.par (PiCalculus.subst body b) (.repl (.inp (.const s) body)))

Uses 6 · Used by 2

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Reduction relation of the π-calculus · Substitution for the innermost bound variable of a process

Proof usesStructural congruence of π-calculus processes · Guarded-choice resolution in the π-calculus

Used bySender-invoked state steps by invoking the receiver trigger · Pending state steps by invoking the sender trigger

DefinitionOne-state recurring send graph#✓fully proved

Every edge of this reachable one-state graph performs a session send.

def recurringGraph : Graph := ⟨1, fun _ => .sendName ⟨0, by decide⟩⟩

Uses 2 · Used by 1

Statement usesFinite guarded regular protocol graph · Node of a guarded protocol graph

Used byRecurring send protocol

DefinitionRecurring send protocol#✓fully proved

Initial cursor of the one-state recurring send protocol.

def recurringProtocol : Protocol := .regular recurringGraph ⟨0, by decide⟩ false

Uses 3 · Used by 6

Statement usesFinite guarded regular protocol graph · Endpoint protocol with guarded regular recursion · One-state recurring send graph

Used byThe receiver worker is runtime-typed · Semantic advances of the recurring interface are the identity · Fixed-rank capability of the recurring session · The dual recurring protocol unfolds to a receive of itself · The recurring protocol unfolds to a send of itself · The sender worker is runtime-typed

DefinitionFixed-rank capability of the recurring session#✓fully proved

The recurring session keeps one literal static capability rank throughout.

def recurringCap : Capability := ⟨7, recurringProtocol⟩

Uses 3 · Used by 13

Statement usesEndpoint capability with a dependency rank · Endpoint protocol with guarded regular recursion · Recurring send protocol

Used byThe state after both trigger invocations is typed · Every phase of the restricted repeated session can step · The pending state is typed at the two-role interface · The receiver reentry request is runtime-typed · Receiver service signature of the recurring example · The receiver worker is runtime-typed · Semantic advances of the recurring interface are the identity · The recurring interface is balanced · Two-role linear interface of the recurring session · The sender reentry request is runtime-typed · Sender service signature of the recurring example · The sender worker is runtime-typed · The state after the sender invocation is typed

TheoremThe recurring protocol unfolds to a send of itself#✓fully proved

Literal guarded self-loop unfolding, not an unreachable extra graph node.

theorem recurring_unfold : recurringProtocol.unfold = .sendName recurringProtocol

Uses 3 · Used by 2

Statement usesEndpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Recurring send protocol

Used bySemantic advances of the recurring interface are the identity · The sender worker is runtime-typed

TheoremThe dual recurring protocol unfolds to a receive of itself#✓fully proved

The peer's literal guarded cursor returns to the same receive protocol.

theorem recurring_dual_unfold :
    recurringProtocol.dual.unfold = .recvName recurringProtocol.dual

Uses 4 · Used by 2

Statement usesEndpoint protocol with guarded regular recursion · Dual of an endpoint protocol · One-step unfolding of a protocol · Recurring send protocol

Used byThe receiver worker is runtime-typed · Semantic advances of the recurring interface are the identity

DefinitionSender worker process#✓fully proved

Worker code has one session action and a real endpoint-transfer reentry.

def senderWorker (b : Name) : Proc := .out b (.const 712) (.out (.const 710) b .nil)

Uses 2 · Used by 12

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

Used byState after both trigger invocations · The state after both trigger invocations is typed · Both services are offered at every phase · Sender-invoked state steps by invoking the receiver trigger · Replicated sender daemon · The sender daemon is typed with empty ownership · Pending state steps by invoking the sender trigger · Substitution instantiates the sender worker's endpoint · The sender worker is runtime-typed · State after the sender trigger invocation · The state after the sender invocation is typed · Session action steps back to the pending state

DefinitionReceiver worker process#✓fully proved

A received session endpoint survives the worker's passive input binder.

def receiverWorker (b : Name) : Proc := .inp b (.out (.const 711) (liftName 0 b) .nil)

Uses 3 · Used by 9

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Lifting free de Bruijn indices of a π-calculus name

Used byState after both trigger invocations · The state after both trigger invocations is typed · Both services are offered at every phase · Replicated receiver daemon · The receiver daemon is typed with empty ownership · Sender-invoked state steps by invoking the receiver trigger · Substitution instantiates the receiver worker's endpoint · The receiver worker is runtime-typed · Session action steps back to the pending state

DefinitionReplicated sender daemon#✓fully proved

Sender replication captures only shared constants and its per-invocation formal.

def senderDaemon : Proc := .repl (.inp (.const 710) (senderWorker (.var 0)))

Uses 3 · Used by 12

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Sender worker process

Used byState after both trigger invocations · The state after both trigger invocations is typed · Every phase of the restricted repeated session can step · Pending state with two role transfers · The pending state is typed at the two-role interface · Every phase of the repeated session can step · Sender-invoked state steps by invoking the receiver trigger · The sender daemon is typed with empty ownership · Pending state steps by invoking the sender trigger · State after the sender trigger invocation · The state after the sender invocation is typed · Session action steps back to the pending state

DefinitionReplicated receiver daemon#✓fully proved

Receiver replication likewise receives, rather than captures, its endpoint.

def receiverDaemon : Proc := .repl (.inp (.const 711) (receiverWorker (.var 0)))

Uses 3 · Used by 12

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Receiver worker process

Used byState after both trigger invocations · The state after both trigger invocations is typed · Every phase of the restricted repeated session can step · Pending state with two role transfers · The pending state is typed at the two-role interface · Every phase of the repeated session can step · The receiver daemon is typed with empty ownership · Sender-invoked state steps by invoking the receiver trigger · Pending state steps by invoking the sender trigger · State after the sender trigger invocation · The state after the sender invocation is typed · Session action steps back to the pending state

DefinitionSender-role transfer to its trigger#✓fully proved

Transfer the actual sender-role endpoint to its shared trigger.

def senderRequest (b : Name) : Proc := .out (.const 710) b .nil

Uses 2 · Used by 6

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

Used byPending state with two role transfers · The pending state is typed at the two-role interface · Both services are offered at every phase · Pending state steps by invoking the sender trigger · The sender reentry request is runtime-typed · Session action steps back to the pending state

DefinitionReceiver-role transfer to its trigger#✓fully proved

Transfer the actual opposite-role endpoint to its shared trigger.

def receiverRequest (b : Name) : Proc := .out (.const 711) b .nil

Uses 2 · Used by 10

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

Used byPending state with two role transfers · The pending state is typed at the two-role interface · Both services are offered at every phase · Sender-invoked state steps by invoking the receiver trigger · The receiver reentry request is runtime-typed · Data substitution yields the receiver's return request · Pending state steps by invoking the sender trigger · State after the sender trigger invocation · The state after the sender invocation is typed · Session action steps back to the pending state

DefinitionPending state with two role transfers#✓fully proved

Persistent services plus TWO pending role transfers, on one physical endpoint.

def pending (b : Name) : Proc := .par (.par (senderRequest b) senderDaemon)
  (.par (receiverRequest b) receiverDaemon)

Uses 6 · Used by 18

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Replicated receiver daemon · Receiver-role transfer to its trigger · Replicated sender daemon · Sender-role transfer to its trigger

Used byEvery phase of the restricted repeated session can step · All declared services are available in the pending state · The pending state is typed at the two-role interface · Phases of the repeated-session execution · Services stay available at every phase · Every phase of the repeated session can step · Both services are offered at every phase · Every phase is reachable from the pending state · Each phase steps to the next · Every phase is typed at the two-role interface · Every phase is typed by preservation from the pending state · Every round count has a trace returning to the pending state · Repeated-session traces with typing, availability and progress · Repeated-session traces with preserved typing and availability · Pending state steps by invoking the sender trigger · Session action steps back to the pending state · Every round has a session action on the same endpoint · Arbitrarily long typed repeated-session traces

DefinitionState after the sender trigger invocation#✓fully proved

After one trigger invocation, the opposite request and both daemons remain.

def sentInvoked (b : Name) : Proc := .par (.par (senderWorker b) senderDaemon)
  (.par (receiverRequest b) receiverDaemon)

Uses 6 · Used by 14

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Replicated receiver daemon · Receiver-role transfer to its trigger · Replicated sender daemon · Sender worker process

Used byEvery phase of the restricted repeated session can step · Phases of the repeated-session execution · Every phase of the repeated session can step · Both services are offered at every phase · Each phase steps to the next · Every phase is typed at the two-role interface · Sender-invoked state steps by invoking the receiver trigger · Every round count has a trace returning to the pending state · Repeated-session traces with typing, availability and progress · Repeated-session traces with preserved typing and availability · Pending state steps by invoking the sender trigger · The state after the sender invocation is typed · Every round has a session action on the same endpoint · Arbitrarily long typed repeated-session traces

DefinitionState after both trigger invocations#✓fully proved

Both received-role workers can now communicate on their actual session name.

def bothInvoked (b : Name) : Proc := .par (.par (senderWorker b) senderDaemon)
  (.par (receiverWorker b) receiverDaemon)

Uses 6 · Used by 14

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Replicated receiver daemon · Receiver worker process · Replicated sender daemon · Sender worker process

Used byThe state after both trigger invocations is typed · Every phase of the restricted repeated session can step · Phases of the repeated-session execution · Every phase of the repeated session can step · Both services are offered at every phase · Each phase steps to the next · Every phase is typed at the two-role interface · Sender-invoked state steps by invoking the receiver trigger · Every round count has a trace returning to the pending state · Repeated-session traces with typing, availability and progress · Repeated-session traces with preserved typing and availability · Session action steps back to the pending state · Every round has a session action on the same endpoint · Arbitrarily long typed repeated-session traces

TheoremSubstitution instantiates the sender worker's endpoint#✓fully proved

Capture-safe first trigger communication instantiates the actual bound endpoint.

theorem sender_subst (b : Name) : PiCalculus.subst (senderWorker (.var 0)) b = senderWorker b

Uses 4

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Substitution for the innermost bound variable of a process · Sender worker process

TheoremSubstitution instantiates the receiver worker's endpoint#✓fully proved

Receiver preserves the actual endpoint under its inner passive input binder.

theorem receiver_subst (b : Name) :
    PiCalculus.subst (receiverWorker (.var 0)) b = receiverWorker b

Uses 4

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Substitution for the innermost bound variable of a process · Receiver worker process

TheoremPending state steps by invoking the sender trigger#✓fully proved

The first real trigger Step, leaving both persistent daemons untouched.

theorem sender_invocation (b : Name) : PiCalculus.Step (pending b) (sentInvoked b)

Uses 11 · Used by 1

Statement usesChannel name in the π-calculus · Reduction relation of the π-calculus · Pending state with two role transfers · State after the sender trigger invocation

Proof usesProcesses of the π-calculus · Replicated receiver daemon · Receiver-role transfer to its trigger · Replicated sender daemon · Sender-role transfer to its trigger · Sender worker process · Invoking a replicated service is a reduction step

Used byEach phase steps to the next

TheoremSender-invoked state steps by invoking the receiver trigger#✓fully proved

The second actual trigger Step, not a pre-generated finite unrolling.

theorem receiver_invocation (b : Name) : PiCalculus.Step (sentInvoked b) (bothInvoked b)

Uses 11 · Used by 1

Statement usesChannel name in the π-calculus · Reduction relation of the π-calculus · State after both trigger invocations · State after the sender trigger invocation

Proof usesProcesses of the π-calculus · Replicated receiver daemon · Receiver-role transfer to its trigger · Receiver worker process · Replicated sender daemon · Sender worker process · Invoking a replicated service is a reduction step

Used byEach phase steps to the next

TheoremInterchange law for four parallel components#✓fully proved

Four canonical parallel components regroup without evaluating any body.

theorem parallel_interchange (a b c d : Proc) :
    Cong (.par (.par a b) (.par c d)) (.par (.par a c) (.par b d))

Uses 2 · Used by 1

Statement usesStructural congruence of π-calculus processes · Processes of the π-calculus

Used bySession action steps back to the pending state

TheoremData substitution yields the receiver's return request#✓fully proved

A passive input removes ONLY its data binder, retaining the actual endpoint.

theorem receiver_return_subst (b : Name) :
    PiCalculus.subst (.out (.const 711) (liftName 0 b) .nil) (.const 712) = receiverRequest b

Uses 7 · Used by 1

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Lifting free de Bruijn indices of a π-calculus name · Substitution for the innermost bound variable of a process · Receiver-role transfer to its trigger

Proof usesSubstitution of a name into a π-calculus name · Substitution cancels name lifting

Used bySession action steps back to the pending state

TheoremSession action steps back to the pending state#✓fully proved

Actual session action restores BOTH pending endpoint-role transfers and daemons.

theorem session_and_reentry (b : Name) : PiCalculus.Step (bothInvoked b) (pending b)

Uses 17 · Used by 2

Statement usesChannel name in the π-calculus · Reduction relation of the π-calculus · State after both trigger invocations · Pending state with two role transfers

Proof usesStructural congruence of π-calculus processes · Processes of the π-calculus · Guarded-choice resolution in the π-calculus · Lifting free de Bruijn indices of a π-calculus name · Substitution for the innermost bound variable of a process · Interchange law for four parallel components · Replicated receiver daemon · Receiver-role transfer to its trigger · Receiver worker process · Data substitution yields the receiver's return request · Replicated sender daemon · Sender-role transfer to its trigger · Sender worker process

Used byEach phase steps to the next · Every round has a session action on the same endpoint

DefinitionSender service signature of the recurring example#✓fully proved

Static sender and receiver permissions use opposite roles, exact rank7 types.

def senderSignature (r : Role) : ServiceSignature := ⟨0, r, recurringCap⟩

Uses 4 · Used by 8

Statement usesEndpoint capability with a dependency rank · Endpoint role on a π name · Shared service signature · Fixed-rank capability of the recurring session

Used byA fresh endpoint singleton is separated from the triggers · All declared services are available in the pending state · Both services are offered at every phase · The receiver trigger declares the receiver signature · The sender daemon is typed with empty ownership · The sender trigger declares the sender signature · The sender reentry request is runtime-typed · Service environment declaring the two triggers

DefinitionReceiver service signature of the recurring example#✓fully proved

Opposite-role receive permission retains the exact literal dual capability.

def receiverSignature (r : Role) : ServiceSignature := ⟨0, r.opposite, recurringCap.dual⟩

Uses 6 · Used by 8

Statement usesEndpoint capability with a dependency rank · Dual of an endpoint capability · Endpoint role on a π name · Opposite endpoint role · Shared service signature · Fixed-rank capability of the recurring session

Used byA fresh endpoint singleton is separated from the triggers · All declared services are available in the pending state · Both services are offered at every phase · The receiver daemon is typed with empty ownership · The receiver trigger declares the receiver signature · The receiver reentry request is runtime-typed · The sender trigger declares the sender signature · Service environment declaring the two triggers

DefinitionService environment declaring the two triggers#✓fully proved

Two distinct declared constant triggers; declaration alone is not an offer.

def services (r : Role) : ServiceEnv := (Finmap.singleton 710 (senderSignature r)).insert
  711 (receiverSignature r)

Uses 5 · Used by 24

Statement usesEndpoint role on a π name · Shared service environment · Shared service signature · Receiver service signature of the recurring example · Sender service signature of the recurring example

Used byThe state after both trigger invocations is typed · Every phase of the restricted repeated session can step · A fresh endpoint singleton is separated from the triggers · All declared services are available in the pending state · The pending state is typed at the two-role interface · Services stay available at every phase · Every phase of the repeated session can step · Both services are offered at every phase · 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 trigger declares the receiver signature · 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 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 · Arbitrarily long typed repeated-session traces

DefinitionEndpoint distinct from both service triggers#✓fully proved

Session endpoints are physically distinct from BOTH declared shared triggers.

def EndpointFresh (b : Name) : Prop := b ≠ .const 710 ∧ b ≠ .const 711

Uses 1 · Used by 16

Statement usesChannel name in the π-calculus

Used byThe state after both trigger invocations is typed · A fresh endpoint singleton is separated from the triggers · Lifting preserves trigger freshness of an endpoint · The pending state is typed at the two-role interface · Every phase of the repeated session can step · 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 reentry request is runtime-typed · The receiver worker is runtime-typed · Repeated-session traces with typing, availability and progress · Repeated-session traces with preserved typing and availability · 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

TheoremThe sender trigger declares the sender signature#✓fully proved

Actual sender signature lookup with literal role, cap rank and raw protocol.

theorem sender_declared (r : Role) : (services r).lookup 710 = some (senderSignature r)

Uses 6 · Used by 3

Statement usesEndpoint role on a π name · Shared service signature · Sender service signature of the recurring example · Service environment declaring the two triggers

Proof usesShared service environment · Receiver service signature of the recurring example

Used byBoth services are offered at every phase · The sender daemon is typed with empty ownership · The sender reentry request is runtime-typed

TheoremThe receiver trigger declares the receiver signature#✓fully proved

The other trigger declares exactly the opposite-role receive permission.

theorem receiver_declared (r : Role) : (services r).lookup 711 = some (receiverSignature r)

Uses 5 · Used by 3

Statement usesEndpoint role on a π name · Shared service signature · Receiver service signature of the recurring example · Service environment declaring the two triggers

Proof usesSender service signature of the recurring example

Used byBoth services are offered at every phase · The receiver daemon is typed with empty ownership · The receiver reentry request is runtime-typed

TheoremLifting preserves trigger freshness of an endpoint#✓fully proved

Actual canonical lifting cannot turn a distinct endpoint into a service constant.

theorem EndpointFresh.lift {b : Name} (h : EndpointFresh b) : EndpointFresh (liftName 0 b)

Uses 3 · Used by 1

Statement usesChannel name in the π-calculus · Lifting free de Bruijn indices of a π-calculus name · Endpoint distinct from both service triggers

Used byThe receiver worker is runtime-typed

TheoremA fresh endpoint singleton is separated from the triggers#✓fully proved

The exact actual-role singleton does not capture a shared trigger as a linear name.

theorem endpoint_separated (r role : Role) (b : Name) (c : Capability) (hb : EndpointFresh b) :
    Separated (services r) (Finmap.singleton (⟨b, role⟩ : Key) c)

Uses 11 · Used by 4

Statement usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Polarized endpoint key · Endpoint role on a π name · Endpoint distinct from both service triggers · Separation of owned linear names from shared names · Service environment declaring the two triggers

Proof usesShared service signature · Receiver service signature of the recurring example · Sender service signature of the recurring example · Singleton context with a nonshared name is separated

Used byThe 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

TheoremErasing a singleton's only key leaves the empty map#✓fully proved

Erasing the actual sole endpoint leaves exactly the empty ownership map. Shared by request and delegation consumers instead of duplicating lookup proofs.

theorem erase_singleton (e : Key) (c : Capability) :
    (Finmap.singleton e c : Context).erase e = ∅

Uses 4 · Used by 2

Statement usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Polarized endpoint key · Endpoint role on a π name

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

TheoremNil is runtime-typed with empty ownership#✓fully proved

Nil embeds the finite ranked fragment with genuinely empty ownership.

theorem nil_typed (n : Nat) (Γ : ServiceEnv) : HasType n Γ ∅ .nil

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

Proof usesChannel name in the π-calculus · Name scoped at a binder depth · Completed ownership map · The empty ownership map is completed · Priority-ranked conversion typing judgement · Finite ranked typing embeds into runtime typing under separation · Empty ownership is separated from shared names

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

TheoremThe sender reentry request is runtime-typed#✓fully proved

Reentry transfers the actual sender capability out, preserving role/rank/code.

theorem sender_request_typed {n : Nat} (r : Role) (b : Name) (hb : b.ClosedAt n)
    (hf : EndpointFresh b) : HasType n (services r)
    (Finmap.singleton (⟨b, r⟩ : Key) recurringCap) (senderRequest b)

Uses 24 · Used by 2

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Endpoint capability with a dependency rank · Polarized endpoint key · Endpoint role on a π name · Endpoint distinct from both service triggers · Runtime typing with guarded shared replication · Fixed-rank capability of the recurring session · Sender-role transfer to its trigger · Service environment declaring the two triggers

Proof usesProcesses of the π-calculus · Equivalence of endpoint capabilities · Reflexivity of capability equivalence · Finite endpoint ownership map · Priority of a shared invocation over active owned keys · Separation of owned linear names from shared names · Shared service environment · Shared service signature · A fresh endpoint singleton is separated from the triggers · Erasing a singleton's only key leaves the empty map · Invocation priority for a singleton of rank above the priority · Nil is runtime-typed with empty ownership · Sender service signature of the recurring example · The sender trigger declares the sender signature

Used byThe pending state is typed at the two-role interface · The sender worker is runtime-typed

TheoremThe receiver reentry request is runtime-typed#✓fully proved

Reentry of the opposite role likewise consumes EXACTLY its own linear slot.

theorem receiver_request_typed {n : Nat} (r : Role) (b : Name) (hb : b.ClosedAt n)
    (hf : EndpointFresh b) : HasType n (services r)
    (Finmap.singleton (⟨b, r.opposite⟩ : Key) recurringCap.dual) (receiverRequest b)

Uses 26 · Used by 3

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Endpoint capability with a dependency rank · Dual of an endpoint capability · Polarized endpoint key · Endpoint role on a π name · Opposite endpoint role · Endpoint distinct from both service triggers · Runtime typing with guarded shared replication · Receiver-role transfer to its trigger · Fixed-rank capability of the recurring session · Service environment declaring the two triggers

Proof usesProcesses of the π-calculus · Equivalence of endpoint capabilities · Reflexivity of capability equivalence · Finite endpoint ownership map · Priority of a shared invocation over active owned keys · Separation of owned linear names from shared names · Shared service environment · Shared service signature · A fresh endpoint singleton is separated from the triggers · Erasing a singleton's only key leaves the empty map · Invocation priority for a singleton of rank above the priority · Nil is runtime-typed with empty ownership · Receiver service signature of the recurring example · The receiver trigger declares the receiver signature

Used byThe pending state is typed at the two-role interface · The receiver worker is runtime-typed · The state after the sender invocation is typed

TheoremThe sender worker is runtime-typed#✓fully proved

One linear session send keeps the same actual guarded protocol cursor and rank.

theorem sender_worker_typed {n : Nat} (r : Role) (b : Name) (hb : b.ClosedAt n)
    (hf : EndpointFresh b) : HasType n (services r)
    (Finmap.singleton (⟨b, r⟩ : Key) recurringCap) (senderWorker b)

Uses 22 · Used by 3

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Endpoint capability with a dependency rank · Polarized endpoint key · Endpoint role on a π name · Endpoint distinct from both service triggers · Runtime typing with guarded shared replication · Fixed-rank capability of the recurring session · Sender worker process · Service environment declaring the two triggers

Proof usesProcesses of the π-calculus · Finite endpoint ownership map · 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 · Shared service environment · A fresh endpoint singleton is separated from the triggers · Recurring send protocol · The recurring protocol unfolds to a send of itself · The sender reentry request is runtime-typed · A guard owning only its own endpoint satisfies the condition

Used byThe state after both trigger invocations is typed · The sender daemon is typed with empty ownership · The state after the sender invocation is typed

TheoremThe receiver worker is runtime-typed#✓fully proved

One receive retains the outer received endpoint through its passive input binder.

theorem receiver_worker_typed {n : Nat} (r : Role) (b : Name) (hb : b.ClosedAt n)
    (hf : EndpointFresh b) : HasType n (services r)
    (Finmap.singleton (⟨b, r.opposite⟩ : Key) recurringCap.dual) (receiverWorker b)

Uses 31 · Used by 2

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Endpoint capability with a dependency rank · Dual of an endpoint capability · Polarized endpoint key · Endpoint role on a π name · Opposite endpoint role · Endpoint distinct from both service triggers · Runtime typing with guarded shared replication · Receiver worker process · Fixed-rank capability of the recurring session · Service environment declaring the two triggers

Proof usesLifting preserves name scoping · Processes of the π-calculus · Lifting free de Bruijn indices of a π-calculus name · Finite endpoint ownership map · Lifting an ownership map past a binder · Lifting a singleton ownership map · Guard priority condition on active endpoints · Renaming the physical name of an endpoint key · Endpoint protocol with guarded regular recursion · Dual of an endpoint protocol · One-step unfolding of a protocol · Lifting preserves trigger freshness of an endpoint · Separation of owned linear names from shared names · Shared service environment · A fresh endpoint singleton is separated from the triggers · The receiver reentry request is runtime-typed · Recurring send protocol · The dual recurring protocol unfolds to a receive of itself · A guard owning only its own endpoint satisfies the condition

Used byThe state after both trigger invocations is typed · The receiver daemon is typed with empty ownership

TheoremThe sender daemon is typed with empty ownership#✓fully proved

The sender daemon starts with NO captured linear capability, only its fresh formal.

theorem sender_daemon_typed (n : Nat) (r : Role) : HasType n (services r) ∅ senderDaemon

Uses 16 · Used by 3

Statement usesEndpoint capability with a dependency rank · Finite endpoint ownership map · Polarized endpoint key · Endpoint role on a π name · Runtime typing with guarded shared replication · Replicated sender daemon · Service environment declaring the two triggers

Proof usesChannel name in the π-calculus · Name scoped at a binder depth · The empty ownership map is completed · Typing rule for a replicated input on a shared name · Sender service signature of the recurring example · Sender worker process · The sender trigger declares the sender signature · The sender worker is runtime-typed · Empty ownership is separated from shared names

Used byThe state after both trigger invocations is typed · The pending state is typed at the two-role interface · The state after the sender invocation is typed

TheoremThe receiver daemon is typed with empty ownership#✓fully proved

The receiver daemon likewise captures no linear endpoint, in either orientation.

theorem receiver_daemon_typed (n : Nat) (r : Role) : HasType n (services r) ∅ receiverDaemon

Uses 16 · Used by 3

Statement usesEndpoint capability with a dependency rank · Finite endpoint ownership map · Polarized endpoint key · Endpoint role on a π name · Runtime typing with guarded shared replication · Replicated receiver daemon · Service environment declaring the two triggers

Proof usesChannel name in the π-calculus · Name scoped at a binder depth · The empty ownership map is completed · Typing rule for a replicated input on a shared name · Receiver service signature of the recurring example · Receiver worker process · The receiver trigger declares the receiver signature · The receiver worker is runtime-typed · Empty ownership is separated from shared names

Used byThe state after both trigger invocations is typed · The pending state is typed at the two-role interface · The state after the sender invocation is typed

DefinitionTwo-role linear interface of the recurring session#✓fully proved

Actual linear interface, one sender role and its opposite receiver role.

def recurringInterface (b : Name) (r : Role) : Context :=
  Finmap.singleton ⟨b, r⟩ recurringCap ∪ Finmap.singleton ⟨b, r.opposite⟩ recurringCap.dual

Uses 8 · Used by 14

Statement usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Dual of an endpoint capability · Finite endpoint ownership map · Polarized endpoint key · Endpoint role on a π name · Opposite endpoint role · Fixed-rank capability of the recurring session

Used byThe state after both trigger invocations is typed · Every phase of the restricted repeated session can step · The pending state is typed at the two-role interface · Every phase of the repeated session can step · 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 · Semantic advances of the recurring interface are the identity · The recurring interface is balanced · Steps preserve typing at the recurring interface · Repeated-session traces with typing, availability and progress · Repeated-session traces with preserved typing and availability · The state after the sender invocation is typed · Arbitrarily long typed repeated-session traces

TheoremThe pending state is typed at the two-role interface#✓fully proved

The real pending state owns two distinct opposite keys, not daemon captures.

theorem pending_typed {n : Nat} (r : Role) (b : Name) (hb : b.ClosedAt n)
    (hf : EndpointFresh b) : HasType n (services r) (recurringInterface b r) (pending b)

Uses 24 · Used by 2

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Endpoint role on a π name · Endpoint distinct from both service triggers · Runtime typing with guarded shared replication · Pending state with two role transfers · Two-role linear interface of the recurring session · Service environment declaring the two triggers

Proof usesProcesses of the π-calculus · Endpoint capability with a dependency rank · Dual of an endpoint capability · Finite endpoint ownership map · Polarized endpoint key · Opposite endpoint role · Shared service environment · Replicated receiver daemon · Receiver-role transfer to its trigger · The receiver daemon is typed with empty ownership · The receiver reentry request is runtime-typed · Fixed-rank capability of the recurring session · Replicated sender daemon · Sender-role transfer to its trigger · The sender daemon is typed with empty ownership · The sender reentry request is runtime-typed

Used byEvery phase is typed at the two-role interface · Every phase is typed by preservation from the pending state

TheoremThe state after the sender invocation is typed#✓fully proved

First invocation transfers the exact sender slot into one worker; frame unchanged.

theorem sentInvoked_typed {n : Nat} (r : Role) (b : Name) (hb : b.ClosedAt n)
    (hf : EndpointFresh b) : HasType n (services r) (recurringInterface b r) (sentInvoked b)

Uses 24 · Used by 1

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Endpoint role on a π name · Endpoint distinct from both service triggers · Runtime typing with guarded shared replication · Two-role linear interface of the recurring session · State after the sender trigger invocation · Service environment declaring the two triggers

Proof usesProcesses of the π-calculus · Endpoint capability with a dependency rank · Dual of an endpoint capability · Finite endpoint ownership map · Polarized endpoint key · Opposite endpoint role · Shared service environment · Replicated receiver daemon · Receiver-role transfer to its trigger · The receiver daemon is typed with empty ownership · The receiver reentry request is runtime-typed · Fixed-rank capability of the recurring session · Replicated sender daemon · Sender worker process · The sender daemon is typed with empty ownership · The sender worker is runtime-typed

Used byEvery phase is typed at the two-role interface

TheoremThe state after both trigger invocations is typed#✓fully proved

Both workers own their actual distinct roles after the two trigger communications.

theorem bothInvoked_typed {n : Nat} (r : Role) (b : Name) (hb : b.ClosedAt n)
    (hf : EndpointFresh b) : HasType n (services r) (recurringInterface b r) (bothInvoked b)

Uses 24 · Used by 1

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Endpoint role on a π name · Endpoint distinct from both service triggers · Runtime typing with guarded shared replication · State after both trigger invocations · Two-role linear interface of the recurring session · Service environment declaring the two triggers

Proof usesProcesses of the π-calculus · Endpoint capability with a dependency rank · Dual of an endpoint capability · Finite endpoint ownership map · Polarized endpoint key · Opposite endpoint role · Shared service environment · Replicated receiver daemon · Receiver worker process · The receiver daemon is typed with empty ownership · The receiver worker is runtime-typed · Fixed-rank capability of the recurring session · Replicated sender daemon · Sender worker process · The sender daemon is typed with empty ownership · The sender worker is runtime-typed

Used byEvery phase is typed at the two-role interface

DefinitionPhases of the repeated-session execution#✓fully proved

Three phases of actual execution; this does not generate unrolled Pi code.

def phase (b : Name) (i : Nat) : Proc :=
  match i % 3 with
  | 0 => pending b
  | 1 => sentInvoked b
  | _ => bothInvoked b

Uses 5 · Used by 15

Statement usesChannel name in the π-calculus · Processes of the π-calculus · State after both trigger invocations · Pending state with two role transfers · State after the sender trigger invocation

Used byEvery phase of the restricted repeated session can step · All declared services are available in the pending state · Services stay available at every phase · Every phase of the repeated session can step · Both services are offered at every phase · Every phase is reachable from the pending state · Each phase steps to the next · 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 · Every round count has a trace returning to the pending state · Repeated-session traces with typing, availability and progress · Repeated-session traces with preserved typing and availability · Every round has a session action on the same endpoint · Arbitrarily long typed repeated-session traces

TheoremEach phase steps to the next#✓fully proved

Every consecutive phase has a real canonical Step, including session reentry.

theorem phase_step (b : Name) (i : Nat) : PiCalculus.Step (phase b i) (phase b (i + 1))

Uses 10 · Used by 6

Statement usesChannel name in the π-calculus · Reduction relation of the π-calculus · Phases of the repeated-session execution

Proof usesProcesses of the π-calculus · State after both trigger invocations · Pending state with two role transfers · Sender-invoked state steps by invoking the receiver trigger · Pending state steps by invoking the sender trigger · State after the sender trigger invocation · Session action steps back to the pending state

Used byEvery phase is reachable from the pending state · Each next phase is typed by subject reduction · Every round count has a trace returning to the pending state · Repeated-session traces with typing, availability and progress · Repeated-session traces with preserved typing and availability · Arbitrarily long typed repeated-session traces

TheoremEvery round count has a trace returning to the pending state#✓fully proved

For EVERY requested count, a nonzero trace returns to the identical pending code. It has exactly three times (m+1) actual Steps, never a reflexive reachability proof.

theorem repeatable_trace (b : Name) (m : Nat) :
    ∃ f : Fin (3 * (m + 1) + 1) → Proc,
      f ⟨0, by omega⟩ = pending b ∧
      f ⟨3 * (m + 1), Nat.lt_succ_self _⟩ = pending b ∧
      (∀ i : Fin (3 * (m + 1)), PiCalculus.Step (f i.castSucc) (f i.succ)) ∧
      ∀ j : Fin (m + 1),
        f ⟨3 * j.val + 2, by omega⟩ = bothInvoked b ∧
          f ⟨3 * j.val + 3, by omega⟩ = pending b

Uses 8

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Reduction relation of the π-calculus · State after both trigger invocations · Pending state with two role transfers

Proof usesPhases of the repeated-session execution · Each phase steps to the next · State after the sender trigger invocation

TheoremEvery round has a session action on the same endpoint#✓fully proved

EVERY round contains an actual action on the SAME session endpoint b.

theorem session_round_phase (b : Name) (i : Nat) :
    phase b (3 * i + 2) = bothInvoked b ∧ phase b (3 * i + 3) = pending b ∧
      PiCalculus.Step (phase b (3 * i + 2)) (phase b (3 * i + 3))

Uses 8 · Used by 3

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Reduction relation of the π-calculus · State after both trigger invocations · Pending state with two role transfers · Phases of the repeated-session execution

Proof usesState after the sender trigger invocation · Session action steps back to the pending state

Used byRepeated-session traces with typing, availability and progress · Repeated-session traces with preserved typing and availability · Arbitrarily long typed repeated-session traces

TheoremEvery phase is typed at the two-role interface#✓fully proved

Every actual runtime phase retains the same exact two-role linear interface.

theorem phase_typed {n : Nat} (r : Role) (b : Name) (hb : b.ClosedAt n)
    (hf : EndpointFresh b) (i : Nat) :
    HasType n (services r) (recurringInterface b r) (phase b i)

Uses 15 · Used by 2

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Endpoint role on a π name · Endpoint distinct from both service triggers · Runtime typing with guarded shared replication · Phases of the repeated-session execution · Two-role linear interface of the recurring session · Service environment declaring the two triggers

Proof usesProcesses of the π-calculus · State after both trigger invocations · The state after both trigger invocations is typed · Pending state with two role transfers · The pending state is typed at the two-role interface · State after the sender trigger invocation · The state after the sender invocation is typed

Used byEach next phase is typed by subject reduction · Arbitrarily long typed repeated-session traces

TheoremArbitrarily long typed repeated-session traces#✓fully proved

Arbitrarily long NONZERO actual execution with ownership at EVERY state. The conclusion is a trace; no trace/Step/result is part of service admission.

theorem typed_repeatable_trace {n : Nat} (r : Role) (b : Name) (hb : b.ClosedAt n)
    (hf : EndpointFresh b) (m : Nat) :
    ∃ f : Fin (3 * (m + 1) + 1) → Proc,
      f ⟨0, by omega⟩ = pending b ∧
      f ⟨3 * (m + 1), Nat.lt_succ_self _⟩ = pending b ∧
      (∀ i : Fin (3 * (m + 1)), PiCalculus.Step (f i.castSucc) (f i.succ)) ∧
      (∀ i, HasType n (services r) (recurringInterface b r) (f i)) ∧
      ∀ j : Fin (m + 1),
        f ⟨3 * j.val + 2, by omega⟩ = bothInvoked b ∧
          f ⟨3 * j.val + 3, by omega⟩ = pending b

Uses 16

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Processes of the π-calculus · Reduction relation of the π-calculus · Endpoint role on a π name · Endpoint distinct from both service triggers · Runtime typing with guarded shared replication · State after both trigger invocations · Pending state with two role transfers · Two-role linear interface of the recurring session · Service environment declaring the two triggers

Proof usesPhases of the repeated-session execution · Each phase steps to the next · Every phase is typed at the two-role interface · State after the sender trigger invocation · Every round has a session action on the same endpoint

TheoremEvery phase is reachable from the pending state#✓fully proved

Induction on actual Step count reaches each phase of the persistent runtime code.

theorem phase_reachable (b : Name) (i : Nat) :
    Relation.ReflTransGen PiCalculus.Step (pending b) (phase b i)

Uses 6 · Used by 2

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Reduction relation of the π-calculus · Pending state with two role transfers · Phases of the repeated-session execution

Proof usesEach phase steps to the next

Used byServices stay available at every phase · Every phase is typed by preservation from the pending state

TheoremBoth services are offered at every phase#✓fully proved

Actual unguarded daemons offer BOTH declared services at EVERY runtime phase.

theorem phase_offers (b : Name) (r : Role) (i : Nat) :
    Offered (services r) (phase b i) 710 (senderSignature r) ∧
      Offered (services r) (phase b i) 711 (receiverSignature r)

Uses 19 · Used by 1

Statement usesChannel name in the π-calculus · Endpoint role on a π name · Declared persistent service offer · Phases of the repeated-session execution · Receiver service signature of the recurring example · Sender service signature of the recurring example · Service environment declaring the two triggers

Proof usesProcesses of the π-calculus · Persistent service offer on a given name · Shared service signature · State after both trigger invocations · Pending state with two role transfers · Receiver-role transfer to its trigger · Receiver worker process · The receiver trigger declares the receiver signature · Sender-role transfer to its trigger · Sender worker process · The sender trigger declares the sender signature · State after the sender trigger invocation

Used byAll declared services are available in the pending state

TheoremThe recurring interface is balanced#✓fully proved

Both literal opposite-role self-loop slots form an ACTUAL balanced initial interface; balance is derived from lookup/code facts, not a ready-pair hypothesis.

theorem recurring_balanced (b : Name) (r : Role) :
    Conversion.Balanced (recurringInterface b r)

Uses 15 · Used by 4

Statement usesChannel name in the π-calculus · Semantic balance of a linear context · Endpoint role on a π name · Two-role linear interface of the recurring session

Proof usesEndpoint capability with a dependency rank · Equivalence of endpoint capabilities · Reflexivity of capability equivalence · Dual of an endpoint capability · Capability duality is an involution · Finite endpoint ownership map · Polarized endpoint key · Peer endpoint key · Opposite endpoint role · Role reversal is an involution · Fixed-rank capability of the recurring session

Used byEvery phase of the repeated session can step · Each next phase is typed by subject reduction · Every phase is typed by preservation from the pending state · Steps preserve typing at the recurring interface

TheoremSemantic advances of the recurring interface are the identity#✓fully proved

EVERY faithful advance of this actual literal self-loop interface is exact identity. This is a code-level property of the concrete regular cursors, not a claim that arbitrary equivalent recursive codes stay syntactically unchanged.

theorem recurring_advance_identity {b : Name} {r : Role} {Ξ : Context}
    (h : Conversion.SemanticAdvance (recurringInterface b r) Ξ) : Ξ = recurringInterface b r

Uses 23 · Used by 3

Statement usesChannel name in the π-calculus · Finite endpoint ownership map · Semantic advancement of a communicating endpoint pair · Endpoint role on a π name · Two-role linear interface of the recurring session

Proof usesEndpoint capability with a dependency rank · Equivalence of endpoint capabilities · Dual of an endpoint capability · Reinserting an owned capability changes nothing · Uniqueness of capability lookups · Matching send and receive heads of two capabilities · Finite guarded regular protocol graph · Polarized endpoint key · Peer endpoint key · Endpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Dual of an endpoint protocol · One-step unfolding of a protocol · Opposite endpoint role · Fixed-rank capability of the recurring session · Recurring send protocol · The dual recurring protocol unfolds to a receive of itself · The recurring protocol unfolds to a send of itself

Used byEach next phase is typed by subject reduction · Every phase is typed by preservation from the pending state · Steps preserve typing at the recurring interface

TheoremSteps preserve typing at the recurring interface#✓fully proved

ANY actually runtime-typed process at the concrete recurring interface keeps that EXACT interface after a canonical Step, by GENERAL preservation and the literal self-loop code property. No phase, readiness or schedule hypothesis.

theorem recurring_step_preserved {n : Nat} {p q : Proc} (r : Role) (b : Name)
    (h : HasType n (services r) (recurringInterface b r) p) (hs : PiCalculus.Step p q) :
    HasType n (services r) (recurringInterface b r) q

Uses 14

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Reduction relation of the π-calculus · Endpoint role on a π name · Runtime typing with guarded shared replication · Two-role linear interface of the recurring session · Service environment declaring the two triggers

Proof usesFinite endpoint ownership map · Semantic balance implies semantic compatibility · Semantic peer compatibility of an ownership map · Semantic advancement of a communicating endpoint pair · Subject reduction for runtime typing at compatible interfaces · Semantic advances of the recurring interface are the identity · The recurring interface is balanced

TheoremEach next phase is typed by subject reduction#✓fully proved

GENERAL runtime subject reduction applies to every recursive phase (hence all THREE phase kinds) in BOTH role orientations, at the exact self-loop interface.

theorem phase_step_preserved {n : Nat} (r : Role) (b : Name) (hb : b.ClosedAt n)
    (hf : EndpointFresh b) (i : Nat) :
    HasType n (services r) (recurringInterface b r) (phase b (i + 1))

Uses 17

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Endpoint role on a π name · Endpoint distinct from both service triggers · Runtime typing with guarded shared replication · Phases of the repeated-session execution · Two-role linear interface of the recurring session · Service environment declaring the two triggers

Proof usesFinite endpoint ownership map · Semantic balance implies semantic compatibility · Semantic peer compatibility of an ownership map · Semantic advancement of a communicating endpoint pair · Subject reduction for runtime typing at compatible interfaces · Each phase steps to the next · Every phase is typed at the two-role interface · Semantic advances of the recurring interface are the identity · The recurring interface is balanced

TheoremEvery phase is typed by preservation from the pending state#✓fully proved

Every phase's ownership follows from the INITIAL pending typing and GENERAL finite runtime preservation, not repeated application of concrete phase typing.

theorem phase_typed_by_preservation {n : Nat} (r : Role) (b : Name) (hb : b.ClosedAt n)
    (hf : EndpointFresh b) (i : Nat) :
    HasType n (services r) (recurringInterface b r) (phase b i)

Uses 18 · Used by 4

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Endpoint role on a π name · Endpoint distinct from both service triggers · Runtime typing with guarded shared replication · Phases of the repeated-session execution · Two-role linear interface of the recurring session · Service environment declaring the two triggers

Proof usesFinite endpoint ownership map · Semantic balance implies semantic compatibility · Semantic peer compatibility of an ownership map · Semantic advancement of a communicating endpoint pair · Multi-step subject reduction at compatible interfaces · Pending state with two role transfers · The pending state is typed at the two-role interface · Every phase is reachable from the pending state · Semantic advances of the recurring interface are the identity · The recurring interface is balanced

Used byEvery phase of the restricted repeated session can step · Every phase of the repeated session can step · Repeated-session traces with typing, availability and progress · Repeated-session traces with preserved typing and availability

TheoremAll declared services are available in the pending state#✓fully proved

Initial actual replicated daemons supply EVERY declared signature, not just requests or shared permissions. Availability remains a syntactic predicate.

theorem initial_available (b : Name) (r : Role) : Available (services r) (pending b)

Uses 12 · Used by 1

Statement usesChannel name in the π-calculus · Endpoint role on a π name · Availability of all declared services · Pending state with two role transfers · Service environment declaring the two triggers

Proof usesDeclared persistent service offer · Persistent service offer on a given name · Shared service signature · Phases of the repeated-session execution · Both services are offered at every phase · Receiver service signature of the recurring example · Sender service signature of the recurring example

Used byServices stay available at every phase

TheoremServices stay available at every phase#✓fully proved

GENERAL persistent-offer reduction closure preserves the real source daemons through every finite actual prefix of the recursive execution.

theorem phase_available_by_reduction (b : Name) (r : Role) (i : Nat) :
    Available (services r) (phase b i)

Uses 9 · Used by 4

Statement usesChannel name in the π-calculus · Endpoint role on a π name · Availability of all declared services · Phases of the repeated-session execution · Service environment declaring the two triggers

Proof usesService availability survives finite reduction · All declared services are available in the pending state · Pending state with two role transfers · Every phase is reachable from the pending state

Used byEvery phase of the restricted repeated session can step · Every phase of the repeated session can step · Repeated-session traces with typing, availability and progress · Repeated-session traces with preserved typing and availability

TheoremRepeated-session traces with preserved typing and availability#✓fully proved

EVERY m has one nonzero finite SAME-session trace with all neighbor Steps, ALL round markers, ownership derived by GENERAL runtime preservation, and actual persistent availability derived by GENERAL reduction closure at EVERY state.

theorem repeatable_trace_preserved {n : Nat} (r : Role) (b : Name) (hb : b.ClosedAt n)
    (hf : EndpointFresh b) (m : Nat) :
    ∃ f : Fin (3 * (m + 1) + 1) → Proc,
      f ⟨0, by omega⟩ = pending b ∧
      f ⟨3 * (m + 1), Nat.lt_succ_self _⟩ = pending b ∧
      (∀ i : Fin (3 * (m + 1)), PiCalculus.Step (f i.castSucc) (f i.succ)) ∧
      (∀ i, HasType n (services r) (recurringInterface b r) (f i)) ∧
      (∀ i, Available (services r) (f i)) ∧
      ∀ j : Fin (m + 1),
        f ⟨3 * j.val + 2, by omega⟩ = bothInvoked b ∧
          f ⟨3 * j.val + 3, by omega⟩ = pending b

Uses 18

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Processes of the π-calculus · Reduction relation of the π-calculus · Endpoint role on a π name · Availability of all declared services · Endpoint distinct from both service triggers · Runtime typing with guarded shared replication · State after both trigger invocations · Pending state with two role transfers · Two-role linear interface of the recurring session · Service environment declaring the two triggers

Proof usesPhases of the repeated-session execution · Services stay available at every phase · Each phase steps to the next · Every phase is typed by preservation from the pending state · State after the sender trigger invocation · Every round has a session action on the same endpoint

TheoremEvery phase of the repeated session can step#✓fully proved

GENERAL qualified progress produces an ACTUAL Step at every recursive phase, BOTH roles and arbitrary scoped endpoint. Idle is excluded by exposed output syntax, not by assuming the previously selected execution or readiness.

theorem phase_general_step {n : Nat} (r : Role) (b : Name) (hb : b.ClosedAt n)
    (hf : EndpointFresh b) (i : Nat) : ∃ q, PiCalculus.Step (phase b i) q

Uses 22 · Used by 1

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Processes of the π-calculus · Reduction relation of the π-calculus · Endpoint role on a π name · Endpoint distinct from both service triggers · Phases of the repeated-session execution

Proof usesUnguarded output in a process · Lifting free de Bruijn indices of a π-calculus name · Global runtime progress at balanced interfaces given availability · Idle process as a structural service template · Idle processes have no unguarded output · State after both trigger invocations · Pending state with two role transfers · Services stay available at every phase · Every phase is typed by preservation from the pending state · Replicated receiver daemon · Two-role linear interface of the recurring session · The recurring interface is balanced · Replicated sender daemon · State after the sender trigger invocation · Service environment declaring the two triggers

Used byRepeated-session traces with typing, availability and progress

TheoremEvery phase of the restricted repeated session can step#✓fully proved

GENERAL empty-interface progress includes the genuine private session in BOTH orientations/all phases. Actual output syntax forces its Step branch.

theorem bound_phase_general_step (r : Role) (i : Nat) :
    ∃ q, PiCalculus.Step (.nu (phase (.var 0) i)) q

Uses 31

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Reduction relation of the π-calculus · Endpoint role on a π name · Phases of the repeated-session execution

Proof usesUnguarded output in a process · Lifting free de Bruijn indices of a π-calculus name · Endpoint capability with a dependency rank · Dual of an endpoint capability · Capability duality is an involution · Finite endpoint ownership map · Binding a fresh dual pair under restriction · Restriction binding over the empty map · Polarized endpoint key · Runtime typing with guarded shared replication · Closed runtime processes are idle or step given availability · Idle process as a structural service template · Idle processes have no unguarded output · Separation of owned linear names from shared names · Shared service environment · State after both trigger invocations · Pending state with two role transfers · Services stay available at every phase · Every phase is typed by preservation from the pending state · Replicated receiver daemon · Fixed-rank capability of the recurring session · Two-role linear interface of the recurring session · Replicated sender daemon · State after the sender trigger invocation · Empty ownership is separated from shared names · Service environment declaring the two triggers

TheoremRepeated-session traces with typing, availability and progress#✓fully proved

EVERY m has a SAME-witness counted repeated-session trace, all state types, actual availability and ALL marked session edges, plus GENERAL progress at EVERY state (including the last). This is not all-schedules fairness or termination.

theorem repeatable_trace_global {n : Nat} (r : Role) (b : Name) (hb : b.ClosedAt n)
    (hf : EndpointFresh b) (m : Nat) :
    ∃ f : Fin (3 * (m + 1) + 1) → Proc,
      f ⟨0, by omega⟩ = pending b ∧
      f ⟨3 * (m + 1), Nat.lt_succ_self _⟩ = pending b ∧
      (∀ i : Fin (3 * (m + 1)), PiCalculus.Step (f i.castSucc) (f i.succ)) ∧
      (∀ i, HasType n (services r) (recurringInterface b r) (f i)) ∧
      (∀ i, Available (services r) (f i)) ∧
      (∀ i, ∃ q, PiCalculus.Step (f i) q) ∧
      ∀ j : Fin (m + 1),
        f ⟨3 * j.val + 2, by omega⟩ = bothInvoked b ∧
          f ⟨3 * j.val + 3, by omega⟩ = pending b

Uses 19

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Processes of the π-calculus · Reduction relation of the π-calculus · Endpoint role on a π name · Availability of all declared services · Endpoint distinct from both service triggers · Runtime typing with guarded shared replication · State after both trigger invocations · Pending state with two role transfers · Two-role linear interface of the recurring session · Service environment declaring the two triggers

Proof usesPhases of the repeated-session execution · Services stay available at every phase · Every phase of the repeated session can step · Each phase steps to the next · Every phase is typed by preservation from the pending state · State after the sender trigger invocation · Every round has a session action on the same endpoint

TheoremUnguarded shared input communicates with a matching output#✓fully proved

Actual input syntax supplies an ACTUAL canonical Step with any matching shared-constant output. Payload and continuation are not finite-unrolled, and nested private/parallel/replica wrappers are handled by existing Cong/Step.

theorem accept_invocation_step {s : Nat} {p : Proc} (h : AcceptIn s p) (b : Name) (c : Proc) :
    ∃ q, PiCalculus.Step (.par (.out (.const s) b c) p) q

Uses 9 · Used by 1

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

Proof usesStructural congruence of π-calculus processes · Guarded-choice resolution in the π-calculus · Lifting free de Bruijn indices of a π-calculus name · Lifting free de Bruijn indices of a π-calculus process · Substitution for the innermost bound variable of a process

Used byOffered service communicates with a matching shared output

TheoremOffered service communicates with a matching shared output#✓fully proved

A persistent offered input exposes real canonical communication, including nested templates and DONE endpoint payloads; no typing or active-key premise.

theorem offered_invocation_step {s : Nat} {p : Proc} (h : OfferedIn s p) (b : Name) (c : Proc) :
    ∃ q, PiCalculus.Step (.par (.out (.const s) b c) p) q

Uses 6 · Used by 1

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Reduction relation of the π-calculus · Persistent service offer on a given name

Proof usesUnguarded shared input communicates with a matching output · Offered services have an unguarded shared input

Used byExposed shared requests step when declared services are available

74 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.