One atomic branch, compiled.

stepBranch (Guarded2Network/PlusCal.lean) does two things to a branch: it walks the precondition with processPrecondition, and it converts the action block statement by statement with convertActionStmt — prepending the consumption assignments the walk hoisted out to the action block rather than leaving them where the receives were.

So this file is two lemmas and their composition. actionBlock_refines lifts Lemmas/Statement.lean's per-statement action_refines over a whole block, which is one StrongRefinement.Comp per statement and nothing more — the action language is unchanged by this pass, so no reordering is involved. Lemmas/Precondition.lean's processPrecondition_spec covers the other half. Composing them is where the assignments move from the precondition's right edge (where the precondition triple leaves them) to the action block's left edge (where the pass actually puts them), which is one associativity step.

Freshness stays a hypothesis here, as it does at every level of this proof: these are syntactic conditions on the source program and on the pass's generated inbox, and discharging them needs the passes before this one (type checking, well-formedness).

@[simp]

theorem Guarded2Network.Block.map_end {α β : Bool → Type} {f : ⦃b : Bool⦄ → α b → β b} {b : Bool} {S : α b} : GuardedPlusCal.Block.map f (GuardedPlusCal.Block.end S) = GuardedPlusCal.Block.end (f S)

Block.map distributes over cons, and leaves end alone. Both hold by rfl — Block.map rewrites begin pointwise and last once — and are named so that a cons_end_induct over a mapped block can rewrite rather than unfold.

@[simp]

theorem Guarded2Network.Block.map_cons {α β : Bool → Type} {f : ⦃b : Bool⦄ → α b → β b} {b : Bool} {S : α false} {B : GuardedPlusCal.Block α b} : GuardedPlusCal.Block.map f (GuardedPlusCal.Block.cons S B) = GuardedPlusCal.Block.cons (f S) (GuardedPlusCal.Block.map f B)

Block.map distributes over cons, and leaves end alone. Both hold by rfl — Block.map rewrites begin pointwise and last once — and are named so that a cons_end_induct over a mapped block can rewrite rather than unfold.

theorem Guarded2Network.actionBlock_refines {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} (hΞ : Ξ.WellScoped) {mbox : Mailbox} {pref : GuardedPlusCal.ChanKey V → List V} {b : Bool} {A : GuardedPlusCal.Block (ComputableGuardedPlusCal.Statement false) b} (fresh : ∀ S ∈ A.begin, Fresh mbox S) (freshLast : Fresh mbox A.last) : StrongRefinement (relatesTo Ξ Ω mbox pref) Trace.Rτ (GuardedPlusCal.Block.reducing (fun ⦃x : Bool⦄ => GuardedPlusCal.Statement.reducing Ξ Ω) A) (GuardedPlusCal.Block.aborting (fun ⦃x : Bool⦄ => GuardedPlusCal.Statement.aborting Ξ Ω) (fun ⦃x : Bool⦄ => GuardedPlusCal.Statement.reducing Ξ Ω) A) (GuardedPlusCal.Block.diverging (fun ⦃x : Bool⦄ => GuardedPlusCal.Statement.diverging) (fun ⦃x : Bool⦄ => GuardedPlusCal.Statement.reducing Ξ Ω) A) (GuardedPlusCal.Block.reducing (fun ⦃x : Bool⦄ => NetworkPlusCal.Statement.reducing Ξ Ω) (GuardedPlusCal.Block.map (fun ⦃x : Bool⦄ => convertActionStmt) A)) (GuardedPlusCal.Block.aborting (fun ⦃x : Bool⦄ => NetworkPlusCal.Statement.aborting Ξ Ω) (fun ⦃x : Bool⦄ => NetworkPlusCal.Statement.reducing Ξ Ω) (GuardedPlusCal.Block.map (fun ⦃x : Bool⦄ => convertActionStmt) A)) (GuardedPlusCal.Block.diverging (fun ⦃x : Bool⦄ => NetworkPlusCal.Statement.diverging) (fun ⦃x : Bool⦄ => NetworkPlusCal.Statement.reducing Ξ Ω) (GuardedPlusCal.Block.map (fun ⦃x : Bool⦄ => convertActionStmt) A)) ∅ ∅

An action block refines, statement by statement. action_refines lifted over a whole block by one StrongRefinement.Comp per statement.

Nothing is reordered and nothing is generated: convertActionStmt is a relabelling of the same statement into the target language, so this is the plain structural lift. All the work of this pass is in the precondition, which is why that half needed a whole file and this one is an induction.

Divergence is ∅ throughout, as everywhere else in this development — no statement of either language diverges.

def Guarded2Network.IsRxThread (mbox : Mailbox) (c₀ : ComputableGuardedPlusCal.Ref) (inbox : String) (T : ComputableNetworkPlusCal.Thread) : Prop

Every thread of a list is a receive loop on this process's channel and inbox, under a label the pass generated. Stated on the bare list rather than on ThreadState because Thread.toNetwork hands the accumulator's rxThreads back as a plain list, and the levels above it never see the state again.

All three extra conjuncts ride along for the same reason the rest does: stepBranch is the only place a receiving thread is ever appended, so it is the only place any of them can be established. The process level is what spends them. Generated keeps a receiving thread's label out of the source's, or a code thread could be scheduled at it. c₀ makes the mailbox the algorithm level assigns the process name the same channel its receiving thread drains — a process has only one channel (BranchesFresh.rfresh), so there is only one to name. mbox = .some (c₀, inbox) rules out the other mailbox: a thread is registered only for a branch that receives, and a branch that receives is what BranchesFresh.mbox_some says has a mailbox at all. And the channel does not mention the generated name, which is ReceiveFresh's first clause and what ProcessRefines.rxThread reports it for — a relay resolves its channel in a memory the relay itself is about to write inbox in. algRelatesTo.step_or_stutter/.immediateAbort read it off rxThread at the resolved instance.

Equations

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

def Guarded2Network.RxOnly (mbox : Mailbox) (c₀ : ComputableGuardedPlusCal.Ref) (inbox : String) (Ts : List ComputableNetworkPlusCal.Thread) : Prop

Every thread of a list is a receive loop on this process's channel and inbox, under a label the pass generated. Stated on the bare list rather than on ThreadState because Thread.toNetwork hands the accumulator's rxThreads back as a plain list, and the levels above it never see the state again.

All three extra conjuncts ride along for the same reason the rest does: stepBranch is the only place a receiving thread is ever appended, so it is the only place any of them can be established. The process level is what spends them. Generated keeps a receiving thread's label out of the source's, or a code thread could be scheduled at it. c₀ makes the mailbox the algorithm level assigns the process name the same channel its receiving thread drains — a process has only one channel (BranchesFresh.rfresh), so there is only one to name. mbox = .some (c₀, inbox) rules out the other mailbox: a thread is registered only for a branch that receives, and a branch that receives is what BranchesFresh.mbox_some says has a mailbox at all. And the channel does not mention the generated name, which is ReceiveFresh's first clause and what ProcessRefines.rxThread reports it for — a relay resolves its channel in a memory the relay itself is about to write inbox in. algRelatesTo.step_or_stutter/.immediateAbort read it off rxThread at the resolved instance.

Equations

• Guarded2Network.RxOnly mbox c₀ inbox Ts = ∀ T ∈ Ts, Guarded2Network.IsRxThread mbox c₀ inbox T

def Guarded2Network.InboxLocal (inbox : String) (e : String × ComputableTLAPlus.Typ × Bool × Option (Bool × ComputablePlusCal.Expression)) : Prop

One entry of the locals list the pass invents: the inbox, declared as a sequence and initialized empty.

Owed to Algorithm.init, which is the only thing that reads it: a compiled instance's memory has to bind inbox to something isSeq-related to the empty inbox contents, and this is what says the declaration puts it there.

Equations

• Guarded2Network.InboxLocal inbox e = ∃ (τ : SurfaceTLAPlus.Typ), e = (inbox, τ.seq, false, some (true, ComputableTLAPlus.Expression.seq [] τ))

def Guarded2Network.InboxInit (inbox : String) (ne : String × ComputablePlusCal.Expression) : Prop

The same declaration after GuardedPlusCal.initsOf has kept only what InitProc reads — the name and the initializer. The type annotation and the constant flag play no part in what an initial memory is, so this is all Algorithm.init ever sees of the local the pass declares.

Equations

• Guarded2Network.InboxInit inbox ne = ∃ (τ : ComputableTLAPlus.Typ), ne = (inbox, ComputableTLAPlus.Expression.seq [] τ)

theorem Guarded2Network.initOf_inboxLocal {inbox : String} {e : String × ComputableTLAPlus.Typ × Bool × Option (Bool × ComputablePlusCal.Expression)} (h : InboxLocal inbox e) : ∃ (ne : String × ComputablePlusCal.Expression), GuardedPlusCal.initOf e = some ne ∧ InboxInit inbox ne

initOf keeps an InboxLocal and turns it into an InboxInit — the one step between the two definitions above, and the reason neither has to be unfolded where they meet.

def Guarded2Network.BranchReceives (Br : ComputableGuardedPlusCal.AtomicBranch) : Prop

A branch that receives at all — what makes the pass register a receiving thread, and so what the registration fact is conditioned on.

Existential where BranchesFresh's fields are universal, and the difference is not cosmetic: those are hypotheses, discharged once per receive a branch has, while this is what a conclusion is conditioned on, and one receive is all it takes.

Equations

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

structure Guarded2Network.BranchRefines {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (mbox : Mailbox) (pref : GuardedPlusCal.ChanKey V → List V) (Br : ComputableGuardedPlusCal.AtomicBranch) (Br' : ComputableNetworkPlusCal.AtomicBranch) : Prop

What one compiled branch owes its source: the refinement, and agreement on where the branch goes next. Named because the block level quantifies over it — a compiled block's branches are pairwise this, List.Forall₂-style — and a bare StrongRefinement conjunction cannot be the argument of a relation combinator.

• refines : StrongRefinement (relatesTo Ξ Ω mbox pref) Trace.Rτ (GuardedPlusCal.AtomicBranch.reducing Ξ Ω Br) (GuardedPlusCal.AtomicBranch.aborting Ξ Ω Br) ∅ (NetworkPlusCal.AtomicBranch.reducing Ξ Ω Br') (NetworkPlusCal.AtomicBranch.aborting Ξ Ω Br') ∅ ∅ ∅

  The branch refines its source, precondition and action block together.

• last_eq : Br'.action.last = convertActionStmt Br.action.last

  And it leaves for the same place: Block.prepend does not touch last, and convertActionBlock maps it pointwise, so a terminal goto survives compilation unchanged.

• blockTransfer {M₁ M₂ : ComputableTLAPlus.Memory V} {F₁ F₂ : GuardedPlusCal.FIFOs V} {ε : GuardedPlusCal.Trace V} : (∀ (c : ComputableGuardedPlusCal.Ref) (ib : String), mbox = some (c, ib) → ib ∉ GuardedPlusCal.Ref.freeVars c) → relatesTo Ξ Ω mbox pref (M₁, F₁, none) (M₂, F₂, none) → (∀ (c : ComputableGuardedPlusCal.Ref) (ib : String) (cpath : List (ComputableTLAPlus.PathStep V)), mbox = some (c, ib) → List.Forall₂ (GuardedPlusCal.EvalStep Ξ Ω M₁) c.args cpath → Finmap.lookup (c.name, cpath) F₂ = some []) → ((M₂, F₂, none), ε) ∈ NetworkPlusCal.AtomicBranch.blocking Ξ Ω Br' → ((M₁, F₁, none), ε) ∈ GuardedPlusCal.AtomicBranch.blocking Ξ Ω Br ∨ ((M₁, F₁, none), ε) ∈ GuardedPlusCal.AtomicBranch.aborting Ξ Ω Br

  And where the compiled branch blocks, the source blocks or aborts — provided the mailbox channel is drained (hdrain, the fact the algorithm level reads off relayBlocking) and the mailbox reference does not mention the generated inbox (hib, a freshness fact relayBlocking supplies alongside). The precondition-only half of the refinement: an action never blocks, so a blocked branch is a blocked precondition, and the walk's blocking field carries that transfer.

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

What a whole label's worth of branches owes: every compiled branch is some source branch, refined. Deliberately weaker than the positional List.Forall₂ a single compiled block satisfies.

Positional pairing is more than any consumer uses — blockRefines_step only ever asks for some source branch matching the target one it was handed, which is Forall₂.exists_left — and it is more than a label can supply. Process.codeTable lets a label denote the union of every block carrying it, and nothing in the front end rejects two blocks with one label, so the branch lists at a label are concatenations rather than a pair of aligned lists. This is what survives that.

Equations

• Guarded2Network.BranchesRefine Ξ Ω mbox pref brs brs' = ∀ Br' ∈ brs', ∃ Br ∈ brs, Guarded2Network.BranchRefines Ξ Ω mbox pref Br Br'

theorem Guarded2Network.BranchesRefine.of_forall₂ {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} {mbox : Mailbox} {pref : GuardedPlusCal.ChanKey V → List V} {brs : List ComputableGuardedPlusCal.AtomicBranch} {brs' : List ComputableNetworkPlusCal.AtomicBranch} (h : List.Forall₂ (BranchRefines Ξ Ω mbox pref) brs brs') : BranchesRefine Ξ Ω mbox pref brs brs'

One compiled block's branches, as a whole label's worth — the positional form forgetting its positions.