𝒞_par: eliminates parallel assignment (r1≔e1 ‖ … ‖ rn≔en) by hoisting every RHS, and every compound Ref's own index expressions, into fresh with-bound temporaries evaluated up front, then re-emitting n ordinary single-target assignments in the original order. Same type in, same type out (ComputablePlusCal.Statement/.Block/.Branches). The invariant it establishes — GuardedPlusCal.Statement.assign takes a single (Ref, Expr) pair — is a runtime fact about ComputablePlusCal.Statement.assign's List, maintained by this pass alone rather than by the type.

𝒞_par(r1≔e1 ‖ … ‖ rn≔en) =
  with v1=e1 do … with vn=en do (
    𝒞_par(r1, λr1. …) … 𝒞_par(rn, λrn. …)
    r1 := v1; … ; rn := vn )
  where 𝒞_par(x, f) = f(x)
        𝒞_par(r[e1,…,en], f) = 𝒞_par(r, λr0. with y1=e1 do … with yn=en do f(r0[y1,…,yn]))
        𝒞_par(r.x, f) = 𝒞_par(r, λr0. f(r0.x))

Reference-recursion, generalized to this project's flat Ref.args : List (String ⊕ Expression) (the field-access prerequisite, Core/TypedPlusCal/Syntax.lean's module doc): walked left to right, a .inl field segment passes straight through with no fresh variable (the r.x case above), a .inr indexExpr segment binds one fresh temp (the r[e] case) — simpler than a recursive-prefix formulation since this project's Ref is already flat, no nested Ref-within-Ref.

A length-≤1 assignment list passes through untouched. Aliasing is only a concern between multiple simultaneous writes; running the general temp-var recipe on a single assignment would be correct but pure noise.

Every synthesized with carries its own ann : Typ field past this pass: FlatReord's walk hands it, unchanged, to GuardedPlusCal.Statement.with's own ann field. The outer RHS bindings (vᵢ's type must match rᵢ's own result type for rᵢ := vᵢ to be well-typed) and the inner index-temp bindings (each index expression's own type) both get their real type now, via Ref.resultType/.indexType respectively (Core/ComputablePlusCal/Syntax.lean) — cheap structural recomputation from Ref.baseType, no re-running inference needed (Ref.baseType's own doc comment, Core/ TypedPlusCal/Syntax.lean, explains why).

partial def ComputablePlusCal.Statement.par {m : Type → Type} [Monad m] [MonadFresh m] {b : Bool} (s : Statement b) : m (Statement b)

𝒞_par over a single statement — an ordinary congruence except at .assign, the one case this pass actually rewrites.

partial def ComputablePlusCal.Block.par {m : Type → Type} [Monad m] [MonadFresh m] {b : Bool} : Block b → m (Block b)

partial def ComputablePlusCal.Branches.par {m : Type → Type} [Monad m] [MonadFresh m] {b : Bool} : Branches b → m (Branches b)

def ComputablePlusCal.Algorithm.par {m : Type → Type} [Monad m] [MonadFresh m] (algo : Algorithm) : m Algorithm

𝒞_par over a whole algorithm: applied per (label, Block) pair, across every thread of every process.

Equations

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