Documentation

WellFormedness.Restrictions

The expression walker: one unified recursive walk over every TypedTLAPlus.Expression reachable from the algorithm — every statement's own embedded expression(s), every Ref.args index expression, and (transitively) every operator/function body reachable by a call the algorithm makes, directly or indirectly. Threading one walker rather than three avoids re-deriving "which expression positions exist in a statement" three times, and gets the transitive check for free: recursing into a called declaration's body re-applies every check to it, not just the temporal/action one.

The recursion/resolution/memoization machinery — ResolvedDecl, Decl.resolve, resolveInModule, Expression.walkReachable, and the statement-level traversal (Statement/Algorithm.walkReachable) — lives in WellFormedness/Reachability.lean, shared with Typed2Computable's later use of the same walk. This file supplies the actual checks below as two callbacks, visitStatement/visitExpr, run once per node in the same pre-order the walk visits nodes, before recursing into children.

source
def TypedTLAPlus.Expression.checkNode {m : Type → Type} [Monad m] [MonadDiagnostic WellFormednessWarning WellFormednessError m] [MonadForeignLookup m] (currentModule : String) (ownDecls : List Decl) (path : List String) (e : TypedPlusCal.Expression) :
m Unit

The per-node checks alone, no recursion of its own — TypedPlusCal.Statement.walkReachable's shared traversal (WellFormedness/Reachability.lean) calls this once per node, as its visitExpr, forwarding into Expression.walkReachable for the actual recursion/resolution/memoization. Uses resolveInModule directly for the global-variable check — it must fire on every reference to a global variable, not just the first, unlike the transitive into-the-body recursion, which the walk already memoizes for its own purposes.

Equations
Instances For
    source
    def TypedPlusCal.Statement.checkRefRestrictions {m : Type → Type} [Monad m] [MonadDiagnostic WellFormednessWarning WellFormednessError m] {b : Bool} (s : Statement b) :
    m Unit

    The channel-shapedness check over s's own non-expression positions — assign's LHS Refs and receive's destination Ref r, neither of which is an Expression node the shared walk's visitExpr would see (Ref carries its own resolved baseType so Ref.resultType can recompute the reference's result type directly, without Γ — see Core/TypedPlusCal/Syntax.lean). send's/receive's channel argument c is legitimately Channel-shaped and exempted — only its index expressions (Ref.args, walked by TypedPlusCal.Statement.walkReachable itself) are checked. Supplied as walkReachable's visitStatement; the expression-position checks are Expression.checkNode, supplied as its visitExpr.

    Equations
    Instances For

      One receiving channel per process #

      Guarded2Network compiles every receive in a process into reads off one shared inbox sequence, fed by a .rx thread per channel. That is only faithful while a process receives from a single channel: with two, both .rx threads append into the same inbox, the channel a message came from is no longer recoverable at the consumption site, and x := Head(inbox) can hand a receive(c₂, x) a message that arrived on c₁. The pass's own per-thread dedup compounds it — .rx threads are deduplicated by channel name, so receive(agt[self], …) and receive(agt[other], …) in one thread produce a single .rx thread draining only the first.

      The Network PlusCal semantics assumes this away by construction: a process's rxₚ drains mailboxₚ, the one channel it listens on. Checked here rather than assumed, so the refinement proof's precondition is one the front end actually enforces.

      The reference channel is the process's declared @mailbox, and a process containing a receive must declare one: the channel a process listens on is what the compiled inbox stands for, so it is written down rather than read off whichever receive the walk reaches first. The mirror case is not an error — a @mailbox on a process with no receive is a warning, and the field is dropped, which is why this check returns the process rather than Unit. Between them the field becomes total on receiving processes: afterwards p.mailbox is .some c exactly when the process receives, and c is the channel it receives on.

      A process set additionally has to index its channel by self. process (a \in Agents) declares many instances at once, and one channel per process text is not one channel per instance: receive(coord, m) would give every instance the same FIFO, so the messages one instance drains into its own inbox are messages another instance was equally entitled to. The refinement invariant cannot even be stated there — the source FIFO would have to equal several instances' inboxes concatenated, with nothing fixing the order. chan[self] resolves to a different ChanKey per instance, which is what makes each instance's inbox account for exactly its own channel. A =-shaped process is a single instance and needs no such index.

      source
      def TypedPlusCal.Process.checkReceiveChannels {m : Type → Type} [Monad m] [MonadDiagnostic WellFormednessWarning WellFormednessError m] (p : Process) :
      m Process

      Every receive reachable in p — including those nested inside if/while/either/with (Statement.forEachNode) — names p's declared @mailbox, indexed by self when p is a process set («=|∈» = false is the ∈ case: Parser_/PlusCal.lean sets true for =).

      Returns p, with its mailbox cleared when it declared one and no receive used it — the one non-fatal outcome here, warned about and then normalized away rather than rejected. Position for that warning is p.id's own, the same one WellFormedness/Declarations.lean's checkNoLocalChannels points at: the annotation itself carries none of its own, and a bare @mailbox: ch; has no index expression to borrow one from.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def TypedPlusCal.Algorithm.checkReceiveChannels {m : Type → Type} [Monad m] [MonadDiagnostic WellFormednessWarning WellFormednessError m] (algo : Algorithm) :
        m Algorithm

        Process.checkReceiveChannels over every process of algo, threading each rewritten process back into the algorithm. Kept out of Algorithm.checkRestrictions's shared walk: that walk's visitStatement callback sees a statement with no record of which process it came from, and this check is process-scoped by nature.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def TypedPlusCal.Algorithm.checkRestrictions {m : Type → Type} [Monad m] [MonadDiagnostic WellFormednessWarning WellFormednessError m] [MonadForeignLookup m] (currentModule : String) (ownDecls : List Decl) (algo : Algorithm) :
          m Unit

          Runs all the above checks over a whole algorithm, via the shared TypedPlusCal.Algorithm.walkReachable (WellFormedness/Reachability.lean), supplying Statement.checkRefRestrictions/Expression.checkNode as its two callbacks. currentModule/ ownDecls come from the enclosing TypedModule (WellFormedness/WellFormedness.lean) — this pass alone doesn't have them, since it only receives the embedded pcalAlgorithm. The ReachabilityClosure memoization is scoped to this one call — a private StateT layer, run from {} and discarded (.run') once this returns: whether an operator was already walked while checking a previous module has no bearing on checking this one.

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