The merged 𝒞_flat/𝒞_reord: both are the same kind of operation — a single left-to-right walk over a block's statements — so this file goes straight from ComputablePlusCal.Block to List GuardedPlusCal.AtomicBranch, with no intermediate AST (no separate 𝒞_flat-output/ 𝒞_reord-input staging type). Runs after 𝒞_cflow/𝒞_par (Computable2Guarded/CFlow.lean/ Par.lean), so no if/while survives anywhere in the tree (𝒞_cflow already rewrote every one into either/await), and every assign carries exactly one (Ref, Expr) pair (𝒞_par already reduced every parallel assignment) — both are runtime facts checked defensively (GuardedError.internalInvariantViolated), not type-level ones, same precedent CFlow.lean itself already uses for while-must-be-block-front.

walkBlock threads two accumulators in original encounter order — guards (with/await/receive) and actions (everything else). Neither is reordered within itself; only guards jump actions they were originally sequenced after, and a floated guard is rewritten as it goes:

𝒞_reord(r ≔ e ; await e') = await e'[e\r] ; r ≔ e
𝒞_flat(B ; either{B₁}or…or{Bₙ} ; B') = either{B;B₁;B'}or…or{B;Bₙ;B'}

A guard is only ever appended to guards, so guards keep their relative order and one reading a variable a preceding receive writes stays after it. A goto ends a branch, packaging (guards, actions, label) into one AtomicBranch.

@[reducible, inline]

abbrev Guard : Type

Equations

• Guard = ComputableGuardedPlusCal.Statement true false

@[reducible, inline]

abbrev Action : Type

Equations

• Action = ComputableGuardedPlusCal.Statement false false

partial def FlatReord.walkBlock {m : Type → Type} [Monad m] [MonadDiagnostic Empty GuardedError m] {b : Bool} (guards : List Guard) (actions : List Action) : ComputablePlusCal.Block b → m (List ComputableGuardedPlusCal.AtomicBranch)

The entry point: walkBlock [] [] block for a top-level labelled AtomicBlock's own body.

partial def FlatReord.walkStep {m : Type → Type} [Monad m] [MonadDiagnostic Empty GuardedError m] {b : Bool} (guards : List Guard) (actions : List Action) (s : ComputablePlusCal.Statement false) (rest : ComputablePlusCal.Block b) : m (List ComputableGuardedPlusCal.AtomicBranch)

One non-terminal statement s, given rest — everything else in s's own containing block, continuing after it.

partial def FlatReord.walkTerminal {m : Type → Type} [Monad m] [MonadDiagnostic Empty GuardedError m] {b : Bool} (guards : List Guard) (actions : List Action) (s : ComputablePlusCal.Statement b) : m (List ComputableGuardedPlusCal.AtomicBranch)

The block's own final statement — no rest exists beyond it (any dangling non-goto end gets absorbed into a begin-position walkStep call instead, by Block.append's own splicing, before ever reaching here — see the module doc).