Add PowerShell initial state contract

IMPLEMENTATION_PLAN.md

@@ -315,10 +315,15 @@ priorities.
       initial-runspace contract and wrapper-state metadata: ambient typed,
       read-only, scoped, alias, function, and module state can change binding
       assignment and command resolution, while child hosts inherit no fresh
-      state guarantee unless their own invocation proves it. Expand the design
-      corpus for cardinality, mutation, separators, wrappers, redirects, and
-      transition caps before tasks 7.3-7.7. The simple-command slice is delivered for
-      ordinary, adjacent, quoted, here-string, redirect, standalone,
+      state guarantee unless their own invocation proves it. The additive
+      `PwshInitialStateMode` API and safe-default contract are now locked;
+      `-NoProfile -NonInteractive` alone is explicitly insufficient without a
+      controlled startup, inherited environment, and module baseline. Design
+      cases select the mode individually and pin default `Unknown`. Tasks
+      7.3-7.4 must consume the contract rather than inferring isolation. Expand the
+      design corpus for cardinality, mutation, separators, wrappers, redirects,
+      and transition caps before tasks 7.3-7.7. The simple-command slice is
+      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 361-entry executable corpus.

README.md

@@ -117,8 +117,8 @@ public sealed class BashParser : IShellParser { /* … */ }
 public sealed class PwshParser : IShellParser { /* … */ }   // v0.2.0
 
 public abstract record ShellParserOptions { /* HomeDirectory, WorkingDirectory */ }
-public sealed record BashParserOptions : ShellParserOptions;
-public sealed record PwshParserOptions : ShellParserOptions;
+public sealed record BashParserOptions : ShellParserOptions; // InitialStateMode
+public sealed record PwshParserOptions : ShellParserOptions; // InitialStateMode
 
 public sealed record ParsedCommand { /* Source, Clauses, IsUnparseable, … */ }
 public sealed record Clause        { /* Operator, Verb, Args, Redirects, Elements, IsSubshell, IsCommandStringWrapped */ }

SPEC.POWERSHELL.md

@@ -115,11 +115,18 @@ public abstract record ShellParserOptions
 /// = ... }` still compiles.</summary>
 public sealed record BashParserOptions : ShellParserOptions;
 
-/// <summary>Configuration knobs for PwshParser. Empty in v0.2.0 — alias
-/// resolution is unconditional (§6.3) and the resolver knobs live on the
-/// shared ShellParserOptions base. Kept as a distinct type so a future
-/// PowerShell-only knob is an additive change, not a new type.</summary>
-public sealed record PwshParserOptions : ShellParserOptions;
+/// <summary>Declares which ambient PowerShell runspace facts the caller can prove.</summary>
+public enum PwshInitialStateMode
+{
+    Unknown,
+    IsolatedNonInteractiveNoProfile,
+}
+
+/// <summary>Configuration knobs for PwshParser.</summary>
+public sealed record PwshParserOptions : ShellParserOptions
+{
+    public PwshInitialStateMode InitialStateMode { get; init; }
+}
 
 /// <summary>PowerShell implementation of IShellParser.</summary>
 public sealed class PwshParser : IShellParser
@@ -407,6 +414,39 @@ after the structural grammar proves that the `ScriptBlock` token is the body
 of a recognized statement. An ordinary script-block argument remains one
 opaque `DynamicSkip` value and does not invent child execution.
 
+Publishing those exact or finite values also requires
+`PwshInitialStateMode.IsolatedNonInteractiveNoProfile`. The default `Unknown`
+mode still exposes the complete supported structure, but loop-body occurrences
+whose safety depends on the binding remain incomplete. The isolated mode is a
+caller assertion that the complete source runs in a newly spawned,
+non-interactive, no-profile PowerShell process with no reused or
+uncontrolled caller-initialized runspace state. Startup configuration and the
+inherited environment must also be controlled: module auto-loading is disabled,
+or available modules and module search paths are pinned to the same reviewed
+baseline used by policy. `-NoProfile -NonInteractive` alone is insufficient.
+A fixed bootstrap may establish those constraints only when it cannot define
+or mutate loop-bound variables or policy-relevant command identities. The mode
+does not permit assumptions about an interactive session, a runspace pool,
+profiles, startup scripts, or uncontrolled ambient variables, aliases,
+functions, and modules.
+
+Even under that assertion, only ordinary unscoped binding names that do not
+case-insensitively collide with PowerShell's automatic, constant, or read-only
+variables are eligible. Scoped/provider bindings such as `$global:x`,
+`$script:x`, `$private:x`, and `$env:X` fail the loop region closed. A typed,
+validated, constant, or read-only ambient binding therefore cannot coerce,
+reject, or otherwise alter a value the analyzer presents as an exact string.
+
+Parenthesized groups, `$()`, and static `Invoke-Expression` execute in the
+current runspace and share supported binding, command-resolution, and location
+state. Decoded `pwsh -Command` and `pwsh -EncodedCommand` payloads run in child
+hosts and do not inherit the parent's fresh-state assertion unless their own
+invocation independently proves the complete constrained-host contract; host
+flags alone do not prove the launch environment or module baseline.
+Recognized variable, alias, function, or module mutation invalidates later
+proofs in every observing scope; cwd-only mutation retains the independent
+initial-state assertion.
+
 A completely delimited `$()` used as an ordinary word, dynamic command
 identity after `&`, redirect value, foreach expression, double-quoted interpolation, or
 expandable here-string is recursively parsed as a command substitution. Its

SPEC.md

@@ -122,9 +122,18 @@ public sealed record BashParserOptions : ShellParserOptions
     public BashInitialStateMode InitialStateMode { get; init; }
 }
 
-/// <summary>Configuration knobs for PwshParser (v0.2.0). Empty — the
-/// resolver knobs live on ShellParserOptions.</summary>
-public sealed record PwshParserOptions : ShellParserOptions;
+/// <summary>Declares which ambient PowerShell runspace facts the caller can prove.</summary>
+public enum PwshInitialStateMode
+{
+    Unknown,
+    IsolatedNonInteractiveNoProfile,
+}
+
+/// <summary>Configuration knobs for PwshParser.</summary>
+public sealed record PwshParserOptions : ShellParserOptions
+{
+    public PwshInitialStateMode InitialStateMode { get; init; }
+}
 
 // The pre-v0.2.0 BashParserOptions body, now hoisted onto ShellParserOptions:
 public abstract record ShellParserOptions
@@ -270,6 +279,42 @@ as `RANDOM`, `LINENO`, `HOME`, `PATH`, `CDPATH`, and `IFS`. The boundary is
 extend-only: a later version may add a proved variable-state model or
 additional explicitly reviewed ordinary names.
 
+`PwshInitialStateMode.Unknown` is likewise the safe default. In this mode the
+parser may expose `foreach` structure and commands, but it does not publish an
+exact or finite loop-binding proof. Ambient PowerShell variables can be typed,
+read-only, constant, scoped, or validated, and ambient aliases, functions, and
+modules can change command resolution. Treating a loop assignment as a plain
+string assignment without excluding those facts would be unsound.
+
+`PwshInitialStateMode.IsolatedNonInteractiveNoProfile` is an explicit caller
+assertion that the complete source is executed by a newly spawned,
+non-interactive PowerShell process with profiles disabled and without a reused
+or uncontrolled caller-initialized runspace. The caller must also control
+startup configuration and the inherited environment: module auto-loading must
+be disabled, or the available modules and module search paths must be pinned to
+the same reviewed baseline used by policy. `-NoProfile -NonInteractive` alone
+does not establish this contract. A fixed bootstrap may establish these
+constraints only when it cannot define or mutate loop-bound variables or
+policy-relevant command identities.
+
+The mode does not erase PowerShell's built-in automatic variables. Exact and
+finite binding proofs remain limited to
+ordinary unscoped variable names that do not collide, case-insensitively, with
+automatic, constant, or read-only bindings known to the supported PowerShell
+runtime. Scoped/provider forms such as `$global:x`, `$script:x`, and `$env:X`
+are outside the bounded loop-binding grammar.
+
+The assertion applies only to the host that the caller actually constrains.
+Current-runspace regions such as `( ... )`, `$()`, and a static
+`Invoke-Expression` payload share supported variable, command-resolution, and
+location state. A decoded `pwsh -Command` or `pwsh -EncodedCommand` child does
+not inherit the assertion unless its own invocation contract independently
+proves the complete constrained-host environment, not merely `-NoProfile`.
+Recognized mutation of variables,
+aliases, functions, or modules invalidates later proofs wherever PowerShell
+scope rules make the mutation observable. Cwd-only state changes retain the
+independent initial-runspace assertion.
+
 For a successful result, every authored simple command appears once in
 `Syntax`, once in `Commands`, and once in `Clauses`, with all three projections
 referencing the identical in-memory `Clause` instance. Serialization is not

docs/CONSUMER_GUIDE.md

@@ -198,6 +198,34 @@ outside the first bounded scalar grammar. The parser also downgrades a decoded
 `export`; resolver-only option cloning for an exact cwd retains the independent
 variable-state assertion.
 
+PowerShell `foreach` value proofs require the parallel but shell-specific
+assertion. `PwshInitialStateMode.Unknown` is the safe default: the parser can
+still expose supported loop structure, but ambient typed, validated,
+read-only, scoped, alias, function, and module state prevents a closed-world
+binding proof. Select `IsolatedNonInteractiveNoProfile` only when the caller
+executes the complete source in a newly spawned noninteractive PowerShell
+process with profiles disabled and no reused or uncontrolled caller-initialized
+runspace. The launch must also disable module auto-loading or pin available
+modules and module search paths to the same reviewed baseline used by policy.
+A fixed bootstrap may establish those constraints only if it cannot define or
+mutate loop-bound variables or policy-relevant command identities:
+
+```csharp
+var parser = new PwshParser(new PwshParserOptions
+{
+    WorkingDirectory = workingDirectory,
+    InitialStateMode = PwshInitialStateMode.IsolatedNonInteractiveNoProfile,
+});
+```
+
+The assertion does not automatically cross `pwsh -Command` or
+`pwsh -EncodedCommand`; a child host needs its own independently proved launch
+contract. By contrast, `( ... )`, `$()`, and static `Invoke-Expression` share
+the current runspace and its mutations. Never select isolated mode for an
+interactive session or runspace pool merely to suppress approval prompts.
+`-NoProfile -NonInteractive` alone does not prove the inherited environment,
+startup configuration, or module baseline.
+
 Heredoc and Bash here-string bodies are stdin data, not implicit child commands
 or filesystem paths. Authorize any command substitutions surfaced from an
 expanding heredoc as normal occurrences, then let executable-specific policy

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

@@ -423,6 +423,32 @@ later scope that can observe it. A decoded `bash -c` after `export` therefore
 enters with `Unknown` initial variable state, while a cwd-only transfer retains
 the caller's variable-state assertion.
 
+PowerShell needs the same explicit boundary for different reasons.
+`PwshParserOptions.InitialStateMode` defaults to `Unknown`, which permits
+structural discovery but withholds exact or finite `foreach` binding proofs.
+`IsolatedNonInteractiveNoProfile` asserts that the complete source executes in
+a newly spawned noninteractive, no-profile PowerShell process rather than an
+interactive, pooled, reused, profile-initialized, or uncontrolled caller-initialized
+runspace. The caller also controls startup configuration and the inherited
+environment: module auto-loading is disabled, or available modules and module
+search paths are pinned to the policy's reviewed baseline. A fixed bootstrap
+may establish those constraints only when it cannot define or mutate
+loop-bound variables or policy-relevant command identities.
+`-NoProfile -NonInteractive` alone is not proof of that environment. Ambient
+PowerShell bindings can be typed, validated, constant,
+read-only, or scoped; aliases, functions, and modules can independently change
+command identity. Syntax alone cannot erase any of those facts.
+
+The positive binding grammar therefore accepts only ordinary unscoped names
+that do not case-insensitively collide with automatic, constant, or read-only
+variables known to the supported runtime. Current-runspace groups, `$()`, and
+static `Invoke-Expression` share supported binding, command-resolution, and cwd
+state. A decoded child `pwsh` host starts at `Unknown` unless its own invocation
+independently proves the complete constrained-host contract. Recognized
+variable, alias,
+function, or module mutation invalidates every later observing proof; a cwd-only
+transfer preserves the independent initial-runspace assertion.
+
 Effective values are shell facts, not executable semantics. The analysis must
 preserve both the authored shell classification and each proved effective
 value. PowerShell does not retroactively turn a string value such as `-Force`

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

@@ -168,6 +168,58 @@ the independently proved variable-state mode.
 - **THEN** the decoded child enters with unknown initial variable state
 - **THEN** the complete result is unparseable rather than publishing an isolated scalar proof
 
+### Requirement: PowerShell loop proofs require an explicit initial-runspace contract
+`PwshParserOptions.InitialStateMode` SHALL default to `Unknown`. In that mode,
+the parser MAY expose supported `foreach` structure and command occurrences,
+but SHALL NOT publish an exact or finite loop-binding proof whose semantics
+could be changed by ambient runspace state.
+
+`IsolatedNonInteractiveNoProfile` SHALL be an explicit caller assertion that
+the complete source runs in a newly spawned noninteractive PowerShell process,
+profiles are disabled, and the runspace has not been reused or initialized by
+uncontrolled caller variables, aliases, functions, or modules. The caller SHALL
+also control startup configuration and the inherited environment. Module
+auto-loading SHALL be disabled, or available modules and module search paths
+SHALL be pinned to the same reviewed baseline used by policy. A fixed bootstrap
+MAY establish those constraints only when it cannot define or mutate loop-bound
+variables or policy-relevant command identities. `-NoProfile -NonInteractive`
+alone SHALL NOT satisfy the contract. Exact and finite
+binding analysis SHALL remain limited to ordinary unscoped names that do not
+case-insensitively collide with automatic, constant, or read-only variables.
+Scoped/provider binding forms SHALL fail closed.
+
+Current-runspace groups, `$()`, and static `Invoke-Expression` payloads SHALL
+share supported binding, command-resolution, and cwd state. A decoded child
+PowerShell host SHALL NOT inherit the parent's fresh-state assertion unless
+that invocation independently proves the complete constrained-host contract.
+Host flags alone SHALL NOT prove the launch environment or module baseline.
+Recognized variable, alias, function, or module mutation SHALL invalidate later proofs in
+every observing scope; cwd-only mutation SHALL retain the independent
+initial-state assertion.
+
+#### Scenario: Unknown ambient PowerShell state withholds a finite proof
+- **WHEN** default-mode PowerShell parses `foreach ($f in @('a','b')) { Remove-Item -LiteralPath $f }`
+- **THEN** the loop structure and body command may remain visible
+- **THEN** the body occurrence is incomplete rather than assuming `$f` is an ordinary string binding
+
+#### Scenario: Isolated no-profile runspace permits an ordinary binding proof
+- **WHEN** the caller selects `IsolatedNonInteractiveNoProfile` for a newly spawned constrained host and parses `foreach ($f in @('a','b')) { Write-Output $f }`
+- **THEN** the bounded analyzer may publish the finite string domain `a`, `b`
+
+#### Scenario: Typed or read-only ambient binding is not erased by syntax
+- **WHEN** a reused runspace already contains `[int]$f` or a read-only `$f` and parses a loop that assigns string values
+- **THEN** default-mode analysis does not claim the authored strings are the effective loop values
+- **THEN** selecting isolated mode for that reused runspace would violate the caller contract
+
+#### Scenario: Child host does not inherit the parent's assertion
+- **WHEN** isolated-mode PowerShell parses a supported `pwsh -NoProfile -Command` child containing a `foreach`
+- **THEN** the child receives `Unknown` initial state unless the child invocation independently proves the complete constrained-host environment
+- **THEN** `-NoProfile` by itself does not prove the inherited environment or module baseline
+
+#### Scenario: Current-runspace evaluation shares state
+- **WHEN** a supported `$()` or static `Invoke-Expression` region mutates a loop-relevant binding or command-resolution fact
+- **THEN** every later observing occurrence is joined with or downgraded to the resulting conservative state
+
 ### Requirement: Shell values use explicit proof domains
 The analysis SHALL classify a policy-relevant shell value as exact, finite,
 bounded symbolic pattern, or unknown, and SHALL NOT present a weaker proof as a

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

@@ -128,6 +128,11 @@
     iterator/body state or command-resolution mutation and dynamic invocation
     fail atomically. Current-scope continuations after a loop remain incomplete;
     isolated child-host loops do not taint their outer continuation.
+- [x] 7.2a Add the explicit `PwshInitialStateMode` contract and safe default
+  before value analysis. Lock the constrained noninteractive no-profile host
+  and module baseline, current-runspace sharing, child-host noninheritance,
+  mutation invalidation, and ambient typed/read-only binding hazards in the
+  canonical specs and case-specific design corpus.
 - [ ] 7.3 Derive exact and finite string domains without treating pipeline objects as literal strings.
 - [ ] 7.4 Propagate PowerShell scope and location state according to the locked statement semantics.
 - [ ] 7.5 Cover aliases, cmdlets, native commands, nested loops, pipelines, script blocks, and wrapper boundaries.