Closed conversion-ranked networks are completed or can step to Progress at reachable states of closed conversion-ranked networks
TheoremClosed conversion-ranked networks are completed or can step#✓fully proved
Cslib.SessionTypes.Endpoint.Conversion.RankedType.progress_empty
A closed finite ranked network is completed or takes an ACTUAL canonical step. Ambient passive-name depth is arbitrary; no readiness witness is supplied.
theorem RankedType.progress_empty {n : Nat} {p : Proc} (h : RankedType n ∅ p) :
Cong p .nil ∨ ∃ q, PiCalculus.Step p qinductive Proc where
| nil : Proc
| out (a b : Name) (p : Proc) : Proc
| inp (a : Name) (p : Proc) : Proc
| par (p q : Proc) : Proc
| nu (p : Proc) : Proc
| repl (p : Proc) : Proc
| sum (p q : Proc) : Proc
deriving DecidableEq, ReprCSLibExt/Languages/PiCalculus/Basic.lean:52
inductive RankedType : Nat → Context → Proc → Prop where
| nil {n : Nat} {Δ : Context} :
Δ.Completed → (∀ e ∈ Δ, e.name.ClosedAt n) → RankedType n Δ .nil
| outName {n : Nat} {Δ : Context} {e : Key} {c : Capability}
{b : Name} {s : Protocol} {p : Proc} :
GuardMin Δ e c.rank → Δ.lookup e = some c → c.protocol.unfold = .sendName s →
e.name.ClosedAt n → b.ClosedAt n →
RankedType n (Δ.insert e ⟨c.rank, s⟩) p → RankedType n Δ (.out e.name b p)
| inpName {n : Nat} {Δ : Context} {e : Key} {c : Capability}
{s : Protocol} {p : Proc} :
GuardMin Δ e c.rank → Δ.lookup e = some c → c.protocol.unfold = .recvName s →
e.name.ClosedAt n →
⋯CSLibExt/Languages/SessionTypes/Endpoint/RankedConversionTyping.lean:30
inductive Cong : Proc → Proc → Prop
| refl (p : Proc) : Cong p p
| symm {p q : Proc} : Cong p q → Cong q p
| trans {p q r : Proc} : Cong p q → Cong q r → Cong p r
| par_comm (p q : Proc) : Cong (.par p q) (.par q p)
| par_assoc (p q r : Proc) : Cong (.par (.par p q) r) (.par p (.par q r))
| par_nil (p : Proc) : Cong (.par p .nil) p
| par_cong {p p' q q' : Proc} : Cong p p' → Cong q q' →
Cong (.par p q) (.par p' q')
| nu_cong {p p' : Proc} : Cong p p' → Cong (.nu p) (.nu p')
| scope (p q : Proc) :
Cong (.par (.nu p) q) (.nu (.par p (liftProc 0 q)))
⋯CSLibExt/Languages/PiCalculus/Basic.lean:137
inductive Step : Proc → Proc → Prop
| commSelect {a : Name} {b : Name} {p' q' p q : Proc} :
Select p (.out a b p') → Select q (.inp a q') →
Step (.par p q) (.par p' (subst q' b))
| parL {p p' q : Proc} : Step p p' → Step (.par p q) (.par p' q)
| parR {p p' q : Proc} : Step p p' → Step (.par q p) (.par q p')
| nu {p p' : Proc} : Step p p' → Step (.nu p) (.nu p')
| cong {p p' q q' : Proc} : Cong p p' → Step p' q' → Cong q' q →
Step p qCSLibExt/Languages/PiCalculus/Basic.lean:172
Uses 9 · Used by 1
Statement usesStructural congruence of π-calculus processes · Processes of the π-calculus · Reduction relation of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Priority-ranked conversion typing judgement · Polarized endpoint key
TheoremProgress at reachable states of closed conversion-ranked networks#✓fully proved
Cslib.SessionTypes.Endpoint.Conversion.RankedType.reachable_progress
Global progress holds at every finite reachable state of a closed ranked network. No fairness, eventual liveness or recursive termination is asserted.
theorem RankedType.reachable_progress {n : Nat} {p q : Proc} (h : RankedType n ∅ p)
(hr : Relation.ReflTransGen PiCalculus.Step p q) :
Cong q .nil ∨ ∃ r, PiCalculus.Step q rinductive Proc where
| nil : Proc
| out (a b : Name) (p : Proc) : Proc
| inp (a : Name) (p : Proc) : Proc
| par (p q : Proc) : Proc
| nu (p : Proc) : Proc
| repl (p : Proc) : Proc
| sum (p q : Proc) : Proc
deriving DecidableEq, ReprCSLibExt/Languages/PiCalculus/Basic.lean:52
inductive RankedType : Nat → Context → Proc → Prop where
| nil {n : Nat} {Δ : Context} :
Δ.Completed → (∀ e ∈ Δ, e.name.ClosedAt n) → RankedType n Δ .nil
| outName {n : Nat} {Δ : Context} {e : Key} {c : Capability}
{b : Name} {s : Protocol} {p : Proc} :
GuardMin Δ e c.rank → Δ.lookup e = some c → c.protocol.unfold = .sendName s →
e.name.ClosedAt n → b.ClosedAt n →
RankedType n (Δ.insert e ⟨c.rank, s⟩) p → RankedType n Δ (.out e.name b p)
| inpName {n : Nat} {Δ : Context} {e : Key} {c : Capability}
{s : Protocol} {p : Proc} :
GuardMin Δ e c.rank → Δ.lookup e = some c → c.protocol.unfold = .recvName s →
e.name.ClosedAt n →
⋯CSLibExt/Languages/SessionTypes/Endpoint/RankedConversionTyping.lean:30
inductive Step : Proc → Proc → Prop
| commSelect {a : Name} {b : Name} {p' q' p q : Proc} :
Select p (.out a b p') → Select q (.inp a q') →
Step (.par p q) (.par p' (subst q' b))
| parL {p p' q : Proc} : Step p p' → Step (.par p q) (.par p' q)
| parR {p p' q : Proc} : Step p p' → Step (.par q p) (.par q p')
| nu {p p' : Proc} : Step p p' → Step (.nu p) (.nu p')
| cong {p p' q q' : Proc} : Cong p p' → Step p' q' → Cong q' q →
Step p qCSLibExt/Languages/PiCalculus/Basic.lean:172
inductive Cong : Proc → Proc → Prop
| refl (p : Proc) : Cong p p
| symm {p q : Proc} : Cong p q → Cong q p
| trans {p q r : Proc} : Cong p q → Cong q r → Cong p r
| par_comm (p q : Proc) : Cong (.par p q) (.par q p)
| par_assoc (p q r : Proc) : Cong (.par (.par p q) r) (.par p (.par q r))
| par_nil (p : Proc) : Cong (.par p .nil) p
| par_cong {p p' q q' : Proc} : Cong p p' → Cong q q' →
Cong (.par p q) (.par p' q')
| nu_cong {p p' : Proc} : Cong p p' → Cong (.nu p) (.nu p')
| scope (p q : Proc) :
Cong (.par (.nu p) q) (.nu (.par p (liftProc 0 q)))
⋯CSLibExt/Languages/PiCalculus/Basic.lean:137
2 fully proved
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.