GuardedPlusCal.Algorithm.WellScoped, a Prop — Guarded2Network's refinement proof precondition, assumed as a hypothesis wherever that proof needs it rather than derived from Elaborator/Computable2Guarded's own behavior.

Same "no duplicate / no shadow" discipline as WellFormedness.WellScoped.CorePlusCal's Prop, adapted to GuardedPlusCal's post-Computable2Guarded shape: every if/while/either/ nested-with has already been rewritten into AtomicBranch's flat precondition/action split, so there's no nested Block to recurse into the way CorePlusCal.Statement.WellScopedIn's .with case does. The only name-introducing construct left is a precondition's own .with, and — unlike CorePlusCal's nested with, whose body-scope closes at } — a flattened precondition's later statements (guard and action) really do see an earlier .with's binding, so its freshness has to be threaded sequentially down the flat guard list rather than checked once against one shared inScope (CorePlusCal.Block.WellScopedIn's ∀ s ∈ B.begin, … pattern would be wrong here — it'd let two sibling .withs reuse the same name). receive/send/assign/multicast's targets aren't required to resolve against any particular scope class here, matching CorePlusCal.WellScoped's own choice not to re-derive "every reference resolves" (redundant with Computable2Guarded's success, whose input already passed TypedPlusCal.Algorithm.checkWellScoped) — nothing here derives full reference resolution.

Beyond binder positions it also carries the two receive restrictions (GuardedPlusCal.PreconditionReceives): one channel per process, and no receive target indexing its own channel. WellFormedness/Restrictions.lean checks both executably over TypedPlusCal; they are restated here as Props because Guarded2Network's refinement proof needs them and has no other source for them: the executable checks exist so that the proof can assume them. That is why the structures below are concrete over ComputableGuardedPlusCal rather than generic in Typ/Expr: Ref.freeVars is.

def GuardedPlusCal.Declarations.names {Typ Expr : Type} (d : Declarations Typ Expr) : List String

Every name a Declarations value binds — the GuardedPlusCal counterpart of CorePlusCal.Declarations.names.

Equations

• One or more equations did not get rendered due to their size.

def GuardedPlusCal.PreconditionWellScopedIn {Typ Expr : Type} (inScope : List String) : List (Statement Typ Expr true false) → Prop

Whether a precondition's own flat guard list introduces no duplicate/shadowed name, given inScope already holds — with's binder must be fresh against inScope and every earlier with in the same list; await/receive bind nothing. The Prop counterpart of what GuardedPlusCal.Thread.toNetwork (Guarded2Network/PlusCal.lean) relies on implicitly when it threads a receive's destination straight into later guards without renaming.

Equations

• GuardedPlusCal.PreconditionWellScopedIn inScope [] = True
• GuardedPlusCal.PreconditionWellScopedIn inScope (GuardedPlusCal.Statement.with name ann bound e :: rest) = (name ∉ inScope ∧ GuardedPlusCal.PreconditionWellScopedIn (name :: inScope) rest)
• GuardedPlusCal.PreconditionWellScopedIn inScope (GuardedPlusCal.Statement.await e :: rest) = GuardedPlusCal.PreconditionWellScopedIn inScope rest
• GuardedPlusCal.PreconditionWellScopedIn inScope (GuardedPlusCal.Statement.receive c r coe :: rest) = GuardedPlusCal.PreconditionWellScopedIn inScope rest

theorem GuardedPlusCal.wellscoped_mono_of_subset {Typ Expr : Type} {stmts : List (Statement Typ Expr true false)} {inScope inScope' : List String} : inScope' ⊆ inScope → PreconditionWellScopedIn inScope stmts → PreconditionWellScopedIn inScope' stmts

A larger forbidden set only makes freshness harder to satisfy, never easier — well-scoped against inScope is well-scoped against any subset of it. Lets a caller holding the whole-algorithm Algorithm.WellScoped fact (inScope = globalNames ++ p.localState.names) specialize down to whatever smaller inScope a specific lemma invocation actually needs.

theorem GuardedPlusCal.fresh_of_wellscoped_of_not_mem {inScope : List String} {e : ComputableTLAPlus.Expression ComputableTLAPlus.Typ} (sub : ∀ z ∈ e.freeVars, z ∈ inScope) {stmts : List (ComputableGuardedPlusCal.Statement true false)} : PreconditionWellScopedIn inScope stmts → ∀ s ∈ stmts, ∀ (name : String), Statement.boundName? s = some name → name ∉ e.freeVars

The other direction from Expression.not_mem_of_fresh, packaged over a whole flat guard list: every name a with in stmts binds avoids e's free variables — the capture-avoidance side condition Guarded2Network/PlusCal.lean's substGuard needs when it substitutes e (an earlier receive's consumption expression) into a later guard.

structure GuardedPlusCal.PreconditionReceives (c₀ : ComputableGuardedPlusCal.Ref) (stmts : List (ComputableGuardedPlusCal.Statement true false)) : Prop

The two receive restrictions WellFormedness/Restrictions.lean checks executably over TypedPlusCal (checkOneReceive, checkRefRestrictions), restated as a Prop over one precondition's flat guard list — the form Guarded2Network's refinement proof consumes.

Neither is stylistic: with two channels the consumption site x := Head(inbox) cannot tell which channel a message arrived on, and a receive whose target name indexes its own channel moves the ChanKey the refinement invariant pins out from under it. The executable checks exist so that this proof can assume them; this is the assumption they justify.

Concrete rather than generic in Typ/Expr, because Ref.freeVars is.

• one_channel (c r : Ref ComputableTLAPlus.Typ ComputablePlusCal.Expression) (coe : TypedTLAPlus.Coercion) : Statement.receive c r coe ∈ stmts → c = c₀

  Every receive here names the same channel — the process's one mailbox.

• target_not_in_channel (c r : ComputableGuardedPlusCal.Ref) (coe : TypedTLAPlus.Coercion) : Statement.receive c r coe ∈ stmts → r.name ∉ Ref.freeVars c

  No receive's target is a name its own channel is indexed by.

• target_lc (c r : ComputableGuardedPlusCal.Ref) (coe : TypedTLAPlus.Coercion) : Statement.receive c r coe ∈ stmts → ∀ (eᵢ : ComputablePlusCal.Expression), Sum.inr eᵢ ∈ r.args → ComputableTLAPlus.Expression.LC eᵢ

  Every index expression of a receive's target reference is locally closed. Elaboration resolves every binder, so a source reference's path carries no dangling de Bruijn index; the consumption assignment Guarded2Network synthesizes for the receive substitutes the target through later guards, and that substitution is sound only on locally-closed operands.

def GuardedPlusCal.AtomicBranch.WellScopedIn (inScope : List String) (c₀ : ComputableGuardedPlusCal.Ref) (Br : ComputableGuardedPlusCal.AtomicBranch) : Prop

Br's own precondition (if any) is well-scoped against inScope and receives only from c₀ — the action block binds nothing, so there's nothing further to check there (same reasoning as CorePlusCal.WellScoped not inspecting .assign/.send/etc.'s expressions).

Equations

• One or more equations did not get rendered due to their size.

structure GuardedPlusCal.Process.WellScoped (p : ComputableGuardedPlusCal.Process) (globalNames : List String) : Prop

p has no duplicate name in any scope, no name shadows an enclosing scope's, and every receive it makes is from the one channel it listens on — the GuardedPlusCal counterpart of CorePlusCal.WellScoped's per-process conjunct.

The mailbox is existential rather than a field: this is a Prop, and which channel it is does not matter to any consumer — only that one channel serves the whole process, which is what Restrictions.lean's checkOneReceive establishes by installing the first receive's channel and comparing the rest against it.

• locals_nodup : p.localState.names.Nodup
• locals_no_shadow (n : String) : n ∈ p.localState.names → n ∉ globalNames
• branches_ws : ∃ (mailbox : ComputableGuardedPlusCal.Ref), ∀ thread ∈ p.threads, ∀ blk ∈ thread, ∀ Br ∈ blk.branches, AtomicBranch.WellScopedIn (globalNames ++ p.localState.names) mailbox Br

structure GuardedPlusCal.Algorithm.WellScoped (algo : ComputableGuardedPlusCal.Algorithm) : Prop

The GuardedPlusCal counterpart of CorePlusCal.WellScoped — Guarded2Network's refinement proof precondition.

• global_nodup : algo.globalState.names.Nodup
• procs_ws (p : Process ComputableTLAPlus.Typ ComputablePlusCal.Expression) : p ∈ algo.processes → p.WellScoped algo.globalState.names