𝒞_cflow: eliminates if/while by rewriting them into either/await congruences. Same type in, same type out (ComputablePlusCal.Statement/.Block/.Branches) — if/while are eliminated as a runtime fact, not type-encoded; only the producer maintains the invariant that while must be immediately preceded by a label.

𝒞_cflow(l: while e do {B1}; B2; goto l') = l: if e then {B1; goto l} else {B2; goto l'}
𝒞_cflow(if e then B1 else B2) = either {await e; B1} or {await ¬e; B2}

if's rewrite is an ordinary per-statement congruence: both branches already share the if's own terminal-ness, recurse and reassemble. while's rewrite operates at the block level, not per-statement: since a while must be immediately preceded by a real label (already enforced by the desugarer), it's always the first statement of its containing block, so Block.cflow special-cases while cond B1 :: rest and absorbs whatever followed the while (rest) into the loop-exit branch. The loop-continue branch reuses B1's own terminal statement directly if it's already terminal (a labelled step was extracted from the loop body, already ending in a goto back to the loop's own label); otherwise it synthesizes that goto itself (coerceGoto) — matching the doc comment on ElaboratedPlusCal.Statement.while's own B field exactly.

¬e is built directly as opCall (var "\\neg" ...) [e], the same shape Desugarer/TLAPlus.lean's PrefixOperator.canonicalName/Elaborator/Declarations.lean's builtin-Γ₀ entry for \neg already establish for this operator.

partial def ComputablePlusCal.Statement.cflow {m : Type → Type} [Monad m] [MonadDiagnostic Empty GuardedError m] {b : Bool} (label : String) (s : Statement b) : m (Statement b)

𝒞_cflow over a single statement. label is the enclosing top-level block's own label, threaded through unchanged (only ever consulted by Block.cflow's while-rewrite; harmless, unused for statements nested where a while can't legally occur).

partial def ComputablePlusCal.Block.cflow {m : Type → Type} [Monad m] [MonadDiagnostic Empty GuardedError m] {b : Bool} (label : String) (B : Block b) : m (Block b)

𝒞_cflow over a block — the one place while actually gets rewritten, per the module doc above.

partial def ComputablePlusCal.Branches.cflow {m : Type → Type} [Monad m] [MonadDiagnostic Empty GuardedError m] {b : Bool} (label : String) : Branches b → m (Branches b)

def ComputablePlusCal.Algorithm.cflow {m : Type → Type} [Monad m] [MonadDiagnostic Empty GuardedError m] (algo : Algorithm) : m Algorithm

𝒞_cflow over a whole algorithm: applied per (label, Block) pair, across every thread of every process — the label a while inside that block would need for coerceGoto, per the module doc above.

Equations

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