One atomic block, compiled.

stepBlock (Guarded2Network/PlusCal.lean) maps stepBranch over the block's branches and keeps the label. So this file is stepBranch_spec under Spec.mapM_list, and the only thing worth saying about it is what the loop invariant carries.

Three things come out, and each is needed one level up. The branches are pairwise BranchRefines, which is the refinement itself. The label is unchanged, and every branch still ends on the same goto (BranchRefines.last_eq) — together, "the gotos agree": a block is entered by label and left by its branches' terminal statements, so a compiled block agreeing on neither would refine its source branch by branch and still be scheduled differently. And RxThreads is threaded through, since stepBranch is what appends to it and the thread level is what consumes it.

There is deliberately no StrongRefinement between block semantics here. AtomicBlock.reducing exists only on the NetworkPlusCal side (Core/NetworkPlusCal/Semantics/Denotational.lean's module doc says why: a source block is only ever existentially quantified, never required to match a target's type), so the pairwise statement over branches is the strongest thing statable — and it is what the process level wants anyway, since that is where a target branch gets matched to some source branch.

structure Guarded2Network.BranchesFresh (mbox : Mailbox) (c₀ : ComputableGuardedPlusCal.Ref) (inbox : String) (Br : ComputableGuardedPlusCal.AtomicBranch) : Prop

Every freshness hypothesis stepBranch_spec takes, at every branch of a block. Bundled because all six travel together from here up: they are conditions on the source program and on the pass's generated inbox, discharged by the passes before this one.

mbox is a parameter and mbox_some is what makes it one. A process with no receive is compiled without an inbox local and has to be related at .none (Mailbox's own doc); every other field here holds at either mailbox, and receive is the only construct that forces the .some one.

• mbox_some (c r : ComputableGuardedPlusCal.Ref) (coe : TypedTLAPlus.Coercion) : GuardedPlusCal.Statement.receive c r coe ∈ preconditionList Br.precondition → mbox = some (c₀, inbox)

  A branch that receives at all is a branch of a process with a mailbox.

• rfresh (c r : ComputableGuardedPlusCal.Ref) (coe : TypedTLAPlus.Coercion) : GuardedPlusCal.Statement.receive c r coe ∈ preconditionList Br.precondition → c = c₀ ∧ ReceiveFresh c r coe inbox

  Every receive in the precondition reads the process's one channel, and neither its channel nor its target mentions the generated inbox.

• gfresh (S : ComputableGuardedPlusCal.Statement true false) : S ∈ preconditionList Br.precondition → Fresh mbox S

  No precondition statement mentions the mailbox.

• pfresh : PairsFresh inbox (preconditionList Br.precondition)

  No with in the precondition binds a name a consumption pair reads.

• afresh (S : GuardedPlusCal.Statement ComputableTLAPlus.Typ ComputablePlusCal.Expression false false) : S ∈ Br.action.begin → Fresh mbox S

  Nor does any action statement mention the mailbox.

• alast : Fresh mbox Br.action.last

  Including the terminal one.

theorem Guarded2Network.BranchesFresh.none_of_no_receive {c₀ : ComputableGuardedPlusCal.Ref} {inbox : String} {Br : ComputableGuardedPlusCal.AtomicBranch} (norecv : ∀ (c r : ComputableGuardedPlusCal.Ref) (coe : TypedTLAPlus.Coercion), GuardedPlusCal.Statement.receive c r coe ∉ preconditionList Br.precondition) : BranchesFresh none c₀ inbox Br

A branch that never receives is fresh at .none for nothing. Every field above is a condition on the generated inbox, and at .none there is no inbox to condition on: Fresh .none is vacuous by definition, and mbox_some/rfresh/pfresh all quantify over the branch's receives, of which there are none.

This is what makes the .none mailbox reachable rather than merely statable, and so it is the whole point of mbox being a parameter. A process with no receive is compiled without an inbox local, so relatesTo (.some (c, inbox)) — which requires the target's memory to bind inbox — is false of it at Algorithm.init. .none is the only mailbox such a process can have, and this is how it gets one.

def Guarded2Network.BlockReceives (blk : ComputableGuardedPlusCal.AtomicBlock) : Prop

A block one of whose branches receives — BranchReceives at the level the walk above is over. What a block owes about receiving is conditioned on this, and one branch is enough: the pass registers a thread the first time any branch of any block of the thread asks for one.

Equations

• Guarded2Network.BlockReceives blk = ∃ Br ∈ blk.branches, Guarded2Network.BranchReceives Br

@[reducible]

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

What one compiled block owes its source: the same label, and branches pairwise BranchRefines.

The thread level quantifies over it — a compiled .code thread's blocks are pairwise this, List.Forall₂-style — for the same reason BranchRefines exists one level down: a conjunction cannot be the argument of a relation combinator.

A def rather than a structure on purpose. stepBlock_spec below is a mvcgen proof whose postcondition is assembled automatically from the loop invariant, and that assembly sees through a reducible conjunction where it would have to be taught a constructor.

Equations

• Guarded2Network.BlockRefines Ξ Ω mbox pref blk blk' = (blk'.label = blk.label ∧ List.Forall₂ (Guarded2Network.BranchRefines Ξ Ω mbox pref) blk.branches blk'.branches)