What a receiving thread's step does to the refinement invariant.

The .rx thread is the one part of the compiled algorithm with no source counterpart at all: it owns no label and its step consumes none, so no source process ever schedules it, and the source therefore stutters while it runs. That is only sound if the step is invisible — and "invisible" here is a statement about procRelatesTo, not about states being equal, because an rx step does change the target's memory and FIFOs.

What it changes, it changes in exactly the way the invariant already accounts for. procRelatesTo says the source's queue at the process's channel is the target's queue with the process's inbox in front of it. An rx step moves one value across that boundary: off the head of the target's FIFO, onto the end of inbox. The concatenation is the same either way, which is why the source needs to take no step to keep up.

The trace is 1. Reception is not in Behavior's alphabet (Core/GuardedPlusCal/Semantics/Denotational.lean), which is what makes stuttering admissible rather than an observable the source failed to produce.

theorem Guarded2Network.rxStep_step {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} (hΞ : Ξ.WellScoped) {c : ComputableGuardedPlusCal.Ref} {inbox : String} {M₁ M₂ : ComputableTLAPlus.Memory V} {F₁ F₂ : GuardedPlusCal.FIFOs V} {ib : InboxState V} {ε : GuardedPlusCal.Trace V} {σ' : GuardedPlusCal.LocalState V} (hfresh : inbox ∉ GuardedPlusCal.Ref.freeVars c) (hmem : ∀ (x : String), x ≠ inbox → Finmap.lookup x M₁ = Finmap.lookup x M₂) (hinbox : ∃ (sv : V), Finmap.lookup inbox M₂ = some sv ∧ ComputableTLAPlus.ExprSemantics.isSeq sv ib.contents) (hkey : ∃ (cpath : List (ComputableTLAPlus.PathStep V)), List.Forall₂ (GuardedPlusCal.EvalStep Ξ Ω M₁) c.args cpath ∧ ib.key = (c.name, cpath)) (hsplit : Finmap.lookup ib.key F₁ = (fun (x : List V) => ib.contents ++ x) <$> Finmap.lookup ib.key F₂) (step : ((M₂, F₂, none), ε, σ') ∈ NetworkPlusCal.Thread.rxStep Ξ Ω c inbox) : ∃ (v : V) (M₂' : ComputableTLAPlus.Memory V) (F₂' : GuardedPlusCal.FIFOs V), ε = 1 ∧ σ' = (M₂', F₂', none) ∧ (∀ (x : String), x ≠ inbox → Finmap.lookup x M₁ = Finmap.lookup x M₂') ∧ (∃ (sv : V), Finmap.lookup inbox M₂' = some sv ∧ ComputableTLAPlus.ExprSemantics.isSeq sv (ib.contents ++ [v])) ∧ (∀ (k : GuardedPlusCal.ChanKey V), k ≠ ib.key → Finmap.lookup k F₂' = Finmap.lookup k F₂) ∧ Finmap.lookup ib.key F₁ = (fun (x : List V) => ib.contents ++ [v] ++ x) <$> Finmap.lookup ib.key F₂' ∧ Finmap.lookup ib.key F₂' ≠ none ∧ F₂'.size + 1 = F₂.size

A receiving thread's step is invisible to the source. The value it moves comes off the head of the target's FIFO and goes onto the end of inbox, so the source's queue — which the invariant says is inbox ++ target's queue — is unchanged, and the source keeps up by not moving.

Stated as the transformation of one InboxState: everything procRelatesTo and algRelatesTo ask about the pair ⟨key, contents⟩ still holds of ⟨key, contents ++ [v]⟩ against the stepped target. No label is mentioned — a .rx thread owns none, and its step produces .none.

inbox ∉ Ref.freeVars c is the same freshness this pass carries everywhere: without it the channel reference could resolve to a different key under the target's memory than under the source's, and the two sides' ChanKeys would not be the one the invariant names.

theorem Guarded2Network.procRelatesTo.rx_step {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} (hΞ : Ξ.WellScoped) {c : ComputableGuardedPlusCal.Ref} {inbox : String} {ib : InboxState V} {M₁ M₂ M₂' : ComputableTLAPlus.Memory V} {F₁ F₂ F₂' : GuardedPlusCal.FIFOs V} {L₁ L₂ : Set String} {ε : GuardedPlusCal.Trace V} (hfresh : inbox ∉ GuardedPlusCal.Ref.freeVars c) (h : procRelatesTo Ξ Ω (some (c, inbox)) (some ib) (M₁, L₁) (M₂, L₂)) (hsplit : Finmap.lookup ib.key F₁ = (fun (x : List V) => ib.contents ++ x) <$> Finmap.lookup ib.key F₂) (step : ((M₂, F₂, none), ε, M₂', F₂', none) ∈ NetworkPlusCal.Thread.rxStep Ξ Ω c inbox) : ∃ (v : V), ε = 1 ∧ procRelatesTo Ξ Ω (some (c, inbox)) (some { key := ib.key, contents := ib.contents ++ [v] }) (M₁, L₁) (M₂', L₂) ∧ (∀ (k : GuardedPlusCal.ChanKey V), k ≠ ib.key → Finmap.lookup k F₂' = Finmap.lookup k F₂) ∧ Finmap.lookup ib.key F₁ = (fun (x : List V) => ib.contents ++ [v] ++ x) <$> Finmap.lookup ib.key F₂' ∧ Finmap.lookup ib.key F₂' ≠ none ∧ F₂'.size + 1 = F₂.size

The same step, at the process level. rxStep_step with procRelatesTo's clauses assembled around it, which is the form the algorithm level meets: a receiving thread's step is one whole Algebra.step of the target, and the source answers it with no step at all.

The label set survives untouched: a .rx thread owns no label and its step consumes none, so procRelatesTo's L₂ = L₁ needs nothing done to it. That is what makes the extra thread invisible to the label bookkeeping as well as to the memory.

The FIFO clauses are returned rather than folded in: they belong to algRelatesTo, which quantifies over all instances' keys at once, so only their per-instance content can be established here.

theorem Guarded2Network.algRelatesTo.rx_step {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} (hΞ : Ξ.WellScoped) {ι : Type u} [DecidableEq ι] {mb : ι → Mailbox} {Ps Qs Qs' : GuardedPlusCal.Instances ι V} {F₁ F₂ F₂' : GuardedPlusCal.FIFOs V} {p : ι} {c : ComputableGuardedPlusCal.Ref} {inbox : String} {M₁ M₂ M₂' : ComputableTLAPlus.Memory V} {L₁ L₂ : Set String} {ε : GuardedPlusCal.Trace V} (hmb : mb p = some (c, inbox)) (hfresh : inbox ∉ GuardedPlusCal.Ref.freeVars c) (h : algRelatesTo Ξ Ω mb (Ps, F₁) (Qs, F₂)) (hS : Ps p = some (M₁, L₁)) (hin : Qs p = some (M₂, L₂)) (hstep : ((M₂, F₂, none), ε, M₂', F₂', none) ∈ NetworkPlusCal.Thread.rxStep Ξ Ω c inbox) (hQs : Qs' = Qs.update p (some (M₂', L₂))) : ε = 1 ∧ algRelatesTo Ξ Ω mb (Ps, F₁) (Qs', F₂') ∧ F₂'.size + 1 = F₂.size

And at the algorithm level: the source does not move at all. One instance takes a receiving thread's step; every other instance and every other FIFO key is untouched, so the whole algRelatesTo witness survives with one instance's InboxState extended by the value that moved.

This is the rx half of the per-step obligation the algorithm-level refinement discharges. It is answered with zero source steps — Relation.star.refl — which is why the source side of that refinement has to be Relation.star Aₛ.step rather than Aₛ.step: GuardedPlusCal.Algebra.reducing is defined as that star, so this is the goal's own shape rather than a weakening of it.