One thread, compiled.

Thread.toNetwork (Guarded2Network/PlusCal.lean) maps stepBlock over the thread's blocks at a ThreadState accumulator and hands back three things: the locals the pass invented, the receiving threads it registered, and the compiled code thread itself. So this file is stepBlock_spec under Spec.mapM_list, exactly as the level below is stepBranch_spec under it — and then the same statement once more at .run {}, which is the form the pass's own body presents.

Two of the three outputs get a conclusion. The compiled thread is ThreadRefines, the blocks pairwise BlockRefines; and the registered threads are RxOnly, each an .rx on this call's inbox. The locals get none: they are a declaration list, and what a compiled process owes about its declarations is a scoping question the process level asks, not a refinement one.

def Guarded2Network.ThreadRefines {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (mbox : Mailbox) (pref : GuardedPlusCal.ChanKey V → List V) (T : ComputableGuardedPlusCal.Thread) (T' : ComputableNetworkPlusCal.Thread) : Prop

What one compiled code thread owes its source: it is a .code thread at all, and its blocks are pairwise BlockRefines.

The .code half is not bookkeeping. A source thread is a list of blocks and a target thread is either that or a receive loop, so "the compiled thread is not itself an .rx" is a real thing to say — and it is what lets the process level split a compiled process's threads into the two groups ProcessRefines.label_cases dispatches a label into, code or receiving.

Equations

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

def Guarded2Network.ThreadReceives (T : ComputableGuardedPlusCal.Thread) : Prop

A thread one of whose blocks receives — the level at which the pass's registration promise is finally cashed, Thread.toNetwork being what hands rxThreads back as a list of threads.

Equations

• Guarded2Network.ThreadReceives T = ∃ blk ∈ T, Guarded2Network.BlockReceives blk

theorem Guarded2Network.Thread.toNetwork_spec {V : Type u} [ComputableTLAPlus.ExprSemantics V] [SeqBuiltins V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} {chans : Guarded2NetworkChans} {mbox : Mailbox} {c₀ : ComputableGuardedPlusCal.Ref} {inbox : String} {pref : GuardedPlusCal.ChanKey V → List V} {T : ComputableGuardedPlusCal.Thread} (hΞ : Ξ.WellScoped) (fresh : ∀ blk ∈ T, ∀ Br ∈ blk.branches, BranchesFresh mbox c₀ inbox Br) : ⦃⌜True⌝⦄ ComputableGuardedPlusCal.Thread.toNetwork chans inbox T ⦃Std.Do.PostCond.mayThrow fun (r : List (String × ComputableTLAPlus.Typ × Bool × Option (Bool × ComputablePlusCal.Expression)) × List ComputableNetworkPlusCal.Thread × ComputableNetworkPlusCal.Thread) => ⌜ThreadRefines Ξ Ω mbox pref T r.2.2 ∧ RxOnly mbox c₀ inbox r.2.1 ∧ (ThreadReceives T → r.2.1 ≠ []) ∧ (∀ e ∈ r.1, InboxLocal inbox e) ∧ (r.1 = [] ↔ r.2.1 = [])⌝⦄

One thread, compiled. The walk, plus reading the accumulator apart into the pass's three outputs.

Everything difficult already happened in stepBlock_spec; what this adds is the ThreadRefines packaging and the fact that the returned thread is .code — Thread.toNetwork builds it, so that half is rfl.