Analyze remote Invoke-Command regions

IMPLEMENTATION_PLAN.md

@@ -350,7 +350,11 @@ priorities.
       delivered for ordinary, adjacent, quoted, here-string, redirect, standalone,
       call-operator, dynamic-identity, and host-wrapper positions, with
       current-scope state propagation and bounded expression rejection pinned
-      by the 383-entry executable corpus.
+      by the 393-entry executable corpus. Remote/session/SSH/VM/container
+      `Invoke-Command` now starts from arbitrary child state, isolates all exit
+      effects, publishes synchronous/once only for one proved target, and
+      publishes concurrent timing for multiple targets or enabled asynchronous
+      switches while keeping dynamic cardinality fail closed.
 - [ ] Deliver typed PowerShell script-block execution regions before calling
       tasks 7.5-7.7 complete. The corrected contract adds an execution-region
       syntax node with independent origin, phase, timing, and cardinality rather than a
@@ -443,8 +447,8 @@ priorities.
       mutator such as `Set-Alias` being rebound to `Set-Item` before a later
       authored `Set-Alias Env:...` invocation.
       The generator-owned executable corpus now supports per-entry initial-
-      state mode and includes the promoted Parallel design case. Pinned child
-      runspace jobs and remote/session invocation remain before deferred
+      state mode and includes the promoted Parallel and remote/session cases.
+      Pinned child runspace jobs remain before deferred
       breakpoint/event/completion actions; then unknown
       receiver and nested/adversarial matrices. Preserve script blocks proved
       to be data as opaque values, expose ambiguous bodies with incomplete

SPEC.POWERSHELL.md

@@ -532,14 +532,28 @@ The version-pinned PowerShell 7 catalog covers:
 | `ForEach-Object -Parallel` | Process | Concurrent | OncePerInputObject | child runspace; runspace-local exit isolated; process-wide effects conservative |
 | `Where-Object -FilterScript` | Filter | Synchronous | OncePerInputObject | current runspace |
 | in-process `Invoke-Command -ScriptBlock` | Main | Synchronous | Once | child scope unless `-NoNewScope`; shared location |
-| remote/session/SSH/VM/container `Invoke-Command` | Main | proved from complete parameter set | Unknown unless targets are proved | remote/child state; exit isolated |
+| remote/session/SSH/VM/container `Invoke-Command` | Main | Synchronous for one proved target; Concurrent for multiple targets or enabled `-AsJob` / `-InDisconnectedSession`; otherwise Unknown | Once for one proved target; otherwise Unknown | arbitrary remote state; exit isolated |
 | `Measure-Command -Expression`, `Trace-Command -Expression` | Main | Synchronous | Once | current scope and location |
 | `Start-Job -InitializationScript` | Initialization | Concurrent | Once | child process before Main |
 | `Start-Job -ScriptBlock` | Main | Concurrent | Once | child process; exit isolated |
 | `New-Module -ScriptBlock` | Initialization | Synchronous | Once | module state; current-runspace effects analyzed separately |
 | `Set-PSBreakpoint -Action`, event `-Action` | Action | Deferred | ZeroOrMore | trigger-time state Unknown without proof |
 | `Register-ArgumentCompleter -ScriptBlock` | Completion | Deferred | ZeroOrMore | completion-time state Unknown without proof |
 
+Remote `Invoke-Command` bodies begin with Unknown working directory, bindings,
+aliases, functions, modules, profiles, and command resolution. Local parser
+state is not an inheritance proof for a remote host or persistent session, and
+remote exit state never flows into the invoking host continuation. A complete
+literal, quoted, URI, GUID, or hashtable target proves one activation. A
+complete top-level comma-separated target list, whether named, inline, or
+positional, proves concurrent scheduling but maps to public cardinality
+`Unknown`, because the public enum intentionally has no once-per-target value.
+Quoted, backtick-escaped, or nested commas remain part of one target value. A
+dynamic target or session collection leaves both
+timing and cardinality `Unknown` unless an enabled `-AsJob` or
+`-InDisconnectedSession` independently proves concurrent scheduling. Explicit
+`:$false` switch values do not prove concurrency.
+
 Parallel child runspaces do not inherit ordinary caller variables or aliases,
 and their runspace-local variable and location exit state does not flow into the
 host continuation. They do share process-wide state such as the environment

openspec/changes/v0-3-structured-shell-analysis/design.md

@@ -372,6 +372,7 @@ PowerShell 7.6.4 probes demonstrate that these are independent dimensions:
 | `ForEach-Object { ... }` | shared current runspace | shared | synchronous / once per input |
 | `Where-Object { ... }` | shared current runspace | shared | synchronous / once per input |
 | local `Invoke-Command { ... }` | child scope unless `-NoNewScope` | shared | synchronous / once |
+| remote/session/SSH/VM/container `Invoke-Command { ... }` | arbitrary remote state; no local binding proof | arbitrary remote location; exit isolated | one target synchronous/once; multiple or async concurrent; otherwise unknown |
 | `Measure-Command { ... }` / `Trace-Command -Expression { ... }` | shared current scope | shared | synchronous / once |
 | `Start-Job { ... }` | child process state | inherited initial location; exit isolated | concurrent / once |
 | `ForEach-Object -Parallel { ... }` | child runspace state; process-wide effects may escape | inherited initial location; runspace-local exit isolated | concurrent / once per input |
@@ -399,6 +400,17 @@ wildcards, and set overflow collapse to all unproved command names. This
 prevents both an alias to `Set-Item` and a rebound `Set-Alias` mutator from
 hiding an environment-provider write without tainting unrelated names.
 
+Remote `Invoke-Command` does not reuse local cwd, binding, alias, function,
+module, profile, or command-resolution facts. The remote body is always
+authorization-visible but incomplete under that arbitrary initial state, and
+its exit state never affects the invoking host continuation. A complete single
+target proves synchronous/once execution. A complete top-level multiple-target
+list, an enabled `-AsJob`, or an enabled `-InDisconnectedSession` proves
+concurrent execution; quoted, escaped, or nested commas remain scalar, and
+multiple or dynamic targets retain cardinality `Unknown`. A dynamic
+target also retains timing `Unknown` unless one of those enabled switches proves
+concurrency. An explicit false switch value does not change scheduling facts.
+
 `SimpleCommandSyntax.ExecutionRegions` preserves authored script-block order.
 The analyzer separately applies semantic phase order. PowerShell's binder can
 assign Begin, Process, and End roles to multiple `ForEach-Object` blocks even

openspec/changes/v0-3-structured-shell-analysis/specs/bounded-shell-analysis/spec.md

@@ -653,14 +653,45 @@ execute synchronously in the current scope. In-process `Invoke-Command`
 without `-NoNewScope` isolates ordinary assignment while sharing location;
 `-NoNewScope` shares supported state. The in-process parameter set does not
 support `-AsJob` and is always synchronous/once. Remote/session/SSH/VM/container
-targets, multiple targets, and remote `-AsJob` SHALL retain only facts proved
-from the complete parameter set.
+`Invoke-Command` SHALL start from Unknown remote cwd, bindings, aliases,
+functions, modules, profiles, and command resolution, and SHALL NOT flow remote
+exit state into the invoking host. One complete proved target SHALL publish
+Synchronous timing and Once cardinality. Multiple complete proved targets SHALL
+publish Concurrent timing and Unknown cardinality. Named, inline, and positional
+target arrays SHALL bind consistently. Only a top-level unescaped comma SHALL
+separate targets; quoted, backtick-escaped, and structurally nested commas SHALL
+remain part of one target. An enabled remote `-AsJob`
+or `-InDisconnectedSession` SHALL publish Concurrent timing independently of
+target cardinality. A dynamic target or session collection SHALL otherwise
+retain Unknown timing and Unknown cardinality. Explicit false-valued switches
+SHALL NOT prove concurrency.
 
 #### Scenario: In-process Invoke-Command does not invent AsJob semantics
 - **WHEN** PowerShell parses `Invoke-Command -ScriptBlock { Get-Date }`
 - **THEN** the region is synchronous and activates once
 - **THEN** analysis does not model `-AsJob` as an in-process option
 
+#### Scenario: One remote target has an isolated synchronous region
+- **WHEN** isolated-mode PowerShell parses `Invoke-Command -ComputerName server -ScriptBlock { Get-Item child.txt }; Get-Item host.txt`
+- **THEN** the region timing is Synchronous and its cardinality is Once
+- **THEN** the body working directory and mutable state are Unknown and incomplete
+- **THEN** the following host command retains its exact local state
+
+#### Scenario: Remote asynchronous switches prove only concurrency
+- **WHEN** PowerShell parses a remote invocation with enabled `-AsJob` or `-InDisconnectedSession`
+- **THEN** the execution region timing is Concurrent
+- **THEN** target cardinality is proved independently
+- **THEN** an explicit `:$false` value does not change synchronous single-target scheduling
+
+#### Scenario: Multiple and dynamic remote targets remain bounded
+- **WHEN** PowerShell parses a complete two-computer target list
+- **THEN** the execution region timing is Concurrent and cardinality is Unknown
+- **WHEN** the comma is instead quoted, backtick-escaped, or nested in one hashtable
+- **THEN** it does not prove multiple targets
+- **WHEN** PowerShell instead parses a runtime `-Session $session` target
+- **THEN** timing and cardinality are Unknown unless an enabled asynchronous switch independently proves Concurrent timing
+- **THEN** every remote body command remains visible and incomplete
+
 #### Scenario: Direct invocation origin survives without source text
 - **WHEN** a consumer receives direct call and dot-source execution-region nodes
 - **THEN** their origins are `DirectCall` and `DotSource` respectively

src/ShellSyntaxTree/Internal/Pwsh/Parsing/PwshForEachValueAnalysis.cs

@@ -2018,6 +2018,14 @@ flow.OnFailure is AnalysisContext failure
                 flow);
         }
 
+        if (binding.ParameterSet == PwshExecutionRegionParameterSet.InvokeRemote)
+        {
+            return AnalyzeRemoteInvokeCommand(
+                regions,
+                receiverInput,
+                flow);
+        }
+
         if (binding.ParameterSet == PwshExecutionRegionParameterSet.NewModuleScriptBlock)
         {
             var bodyInput = PwshPersistentStateMutation.HasVariableWritingArgument(
@@ -2288,6 +2296,37 @@ private PwshFlowResult AnalyzeInProcessInvokeCommand(
             : fallback;
     }
 
+    private PwshFlowResult AnalyzeRemoteInvokeCommand(
+        IReadOnlyList<ExecutionRegionSyntax> regions,
+        AnalysisContext receiverInput,
+        PwshFlowResult hostFlow)
+    {
+        var executionRegionEffectCount = _executionRegionEffectCount;
+        var nonRegionStateMutationCount = _nonRegionStateMutationCount;
+        var locationStateMutationCount = _locationStateMutationCount;
+        var childScopeEscapeRiskCount = _childScopeEscapeRiskCount;
+        var childRunspaceProcessEscapeRiskCount =
+            _childRunspaceProcessEscapeRiskCount;
+        try
+        {
+            TryAnalyzeRegionSequence(
+                regions,
+                receiverInput.CreateRemoteInput(),
+                out _);
+        }
+        finally
+        {
+            _executionRegionEffectCount = executionRegionEffectCount + regions.Count;
+            _nonRegionStateMutationCount = nonRegionStateMutationCount;
+            _locationStateMutationCount = locationStateMutationCount;
+            _childScopeEscapeRiskCount = childScopeEscapeRiskCount;
+            _childRunspaceProcessEscapeRiskCount =
+                childRunspaceProcessEscapeRiskCount;
+        }
+
+        return hostFlow;
+    }
+
     private PwshFlowResult AnalyzePipelineCallbackRegions(
         PwshExecutionRegionBindingResult binding,
         IReadOnlyList<ExecutionRegionSyntax> regions,
@@ -2521,6 +2560,8 @@ private static bool IsSupportedExecutionRegionReceiver(
                 AllBindingsAreCompleteWithTiming(
                     binding.Bindings,
                     ExecutionRegionTiming.Concurrent),
+            PwshExecutionRegionParameterSet.InvokeRemote =>
+                AllBindingsAreComplete(binding.Bindings),
             PwshExecutionRegionParameterSet.MeasureExpression or
                 PwshExecutionRegionParameterSet.TraceExpression or
                 PwshExecutionRegionParameterSet.InvokeInProcess or
@@ -2534,6 +2575,25 @@ PwshExecutionRegionParameterSet.ForEachScriptBlock or
         };
     }
 
+    private static bool AllBindingsAreComplete(
+        IReadOnlyList<PwshExecutionRegionBinding> bindings)
+    {
+        if (bindings.Count == 0)
+        {
+            return false;
+        }
+
+        for (var index = 0; index < bindings.Count; index++)
+        {
+            if (!bindings[index].IsComplete)
+            {
+                return false;
+            }
+        }
+
+        return true;
+    }
+
     private static bool AllBindingsAreCompleteWithTiming(
         IReadOnlyList<PwshExecutionRegionBinding> bindings,
         ExecutionRegionTiming timing)
@@ -4380,6 +4440,19 @@ internal AnalysisContext CreateChildProcessInput() =>
                 ProcessWideStateInvalidated,
                 Array.Empty<BindingFrame>());
 
+        internal AnalysisContext CreateRemoteInput() =>
+            // The target host or persistent session can have arbitrary cwd,
+            // variables, aliases, functions, modules, and profiles. Its exit
+            // state is isolated from the invoking host.
+            new(
+                workingDirectory: null,
+                canPromote: false,
+                commandResolutionInvalidated: true,
+                allRunspaceCommandResolutionMayReachProcessMutation: false,
+                Array.Empty<string>(),
+                processWideStateInvalidated: false,
+                Array.Empty<BindingFrame>());
+
         internal AnalysisContext CreateChildRunspaceInput() =>
             // Caller aliases and ordinary variables do not initialize a Parallel
             // child runspace; explicit $using: values remain conservatively unknown.