PowerShell: add foreach abstract-state analysis

IMPLEMENTATION_PLAN.md

@@ -256,8 +256,10 @@ priorities.
       roles, ancestry, completeness, nullable decoded spans, compatibility
       operators, and exact shared `Clause` identity. The strict DTO rejects
       unknown fields and always requires unparseable projections to be empty.
-      The PowerShell manifest now owns all 361 entries and round-trips exactly;
-      explicit false/null assertions remain opt-in and generator-preserved.
+      The PowerShell manifest owns the first 361 entries and round-trips them
+      exactly; isolated-state v0.3 entries 362-372 remain explicitly curated
+      until the generator accepts a case-specific initial-state mode. Explicit
+      false/null assertions remain opt-in and generator-preserved.
 - [x] Deliver the first Bash `$()` substitution slice for supported
       simple-command arguments and redirect targets. Direct tests and corpus
       entries pin multiple and nested ordering, exact ancestry/spans, isolated
@@ -303,7 +305,7 @@ priorities.
       transfers, and occurrence-specific redirect values remain fail closed.
       Next add the Netclaw approval matrix before calling the Bash consumer
       integration complete.
-- [ ] Complete PowerShell `foreach` value and state analysis and add the
+- [ ] Complete PowerShell `foreach` integration and add the
       Netclaw approval-matrix cases. The structural slice now preserves literal
       scalar/array and executable iterator forms, recursively parses bodies,
       projects iterator and loop-body ancestry, survives decoded wrappers, and
@@ -326,15 +328,29 @@ priorities.
       guards a pinned documented preference inventory plus fresh-host built-ins
       with a live PowerShell oracle, composes case-insensitive distinct nested
       bindings, and leaves pipeline
-      objects, null, overflow, wrappers, redirects, same-name overwrites, and
-      post-loop state conservative. Task 7.4 must add ordered persistent scope
-      and location transfers without restoring parser-frame bindings. Expand the
-      design corpus for cardinality, mutation, separators, wrappers, redirects,
-      and transition caps before tasks 7.4-7.7. The simple-command slice is
+      objects, null, overflow, wrappers, and redirects conservative. The
+      PowerShell-specific state pass now owns ordered persistent bindings,
+      same-name overwrites, empty and zero-or-more execution, occurrence joins,
+      failure-aware `Set-Location`, current-runspace subexpressions, child-host
+      isolation, and the shared 4096-transition budget. Parser-frame location
+      attribution is cloned so empty bodies do not leak and possibly reached
+      mutations cannot leave a false exact cwd; outcome projection rebases exact
+      failure continuations and sanitizes unknown joins. The mutation inventory
+      inspects both verbs and parameter binding: common variable writers,
+      PowerShell 7 command-specific writers, accepted abbreviations and inline
+      values, and opaque splats invalidate later observing proofs, including
+      both outcome partitions of specialized `Set-Location` analysis. Alternate
+      binder dashes and unsupported module-qualified cmdlets now fail closed
+      consistently inside structural regions. Computed `Invoke-Expression`
+      invalidates later current-runspace binding, command-resolution, and cwd
+      proofs and fails atomically as an unmodeled loop transfer. Expand the design corpus for
+      aliases, cmdlets/native commands, pipelines, wrappers, redirects, and the
+      remaining adversarial/oracle matrix before tasks 7.5-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.
+      by the 372-entry executable corpus.
 - [ ] Deliver Bash `for ... in` and PowerShell `foreach` as the first two
       language-specific vertical slices, then extract only the shared analysis
       proven by both implementations.

SPEC.POWERSHELL.md

@@ -452,6 +452,25 @@ Recognized variable, alias, function, or module mutation invalidates later
 proofs in every observing scope; cwd-only mutation retains the independent
 initial-state assertion.
 
+Mutation is recognized from the effective parameter vector as well as the
+verb. Common parameter writers `-OutVariable` / `-ov`, `-PipelineVariable` /
+`-pv`, `-ErrorVariable` / `-ev`, `-WarningVariable` / `-wv`, and
+`-InformationVariable` / `-iv` invalidate later observing proofs, including
+accepted unambiguous prefixes such as `-OutV` and `-PipelineV` and inline forms
+such as `-ov:name`. Command-specific writers include `Tee-Object -Variable`,
+`Import-LocalizedData -BindingVariable` / `-Variable`,
+`Invoke-RestMethod -SessionVariable` / `-SV`, `-ResponseHeadersVariable` /
+`-RHV`, and `-StatusCodeVariable`, plus `Invoke-WebRequest -SessionVariable` /
+`-SV`; their accepted unambiguous prefixes have the same effect. An opaque
+splat may supply any such parameter and is therefore a possible mutation.
+Because command type and custom advanced-function metadata are runtime facts,
+an otherwise unclassified command carrying one of the common writer forms is
+treated conservatively rather than assumed native.
+When `Set-Location` carries a recognized writer, the writer effect composes
+with both its success and failure cwd outcomes. In particular, a failure-gated
+continuation after `-ErrorVariable` cannot retain a proved prior value merely
+because location analysis selected the failure partition.
+
 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
@@ -484,6 +503,35 @@ does not isolate location. Branch exits retain an exact cwd only when every
 supported alternative agrees; disagreement becomes `Unknown`. Loop exits
 include the zero-iteration state. The parser does not publish a finite cwd set.
 
+`foreach` assignments use a case-insensitive persistent binding map rather than
+lexical push/pop restoration. A proved nonempty ordered iterable leaves its
+last assigned value after the loop; a same-name nested loop overwrites that
+value. A proved empty iterable performs no body transition and preserves the
+incoming binding and location. A zero-or-more iterable joins the zero path with
+all reachable iteration exits. Repeated visits join facts for each authored
+occurrence, and all concrete or fixed-point visits share the parse-wide 4096
+transition budget.
+
+`Set-Location` has separate success and failure transfers: success takes the
+proved filesystem target location, while failure retains the incoming location.
+A successful non-filesystem or unproved target invalidates binding and
+command-resolution proofs in addition to making cwd unknown. `&&`
+continues from success, `||` from failure, and statement sequence consumes
+their join. `$()` and parenthesized groups share current-runspace state;
+decoded child hosts isolate their exit state. Unsupported directory-stack or
+state/command-resolution mutations, including `Import-Alias`,
+`Import-PSSession`, and `New-Module`, remain fail
+closed. Provider-capable item
+mutators invalidate binding proofs when their target provider is not proved;
+dynamic values alone do not invalidate a proved filesystem target. Loop parsing uses cloned
+compatibility attribution so an unreachable body cannot leak a parse-time
+location, and a possibly reached mutation cannot leave a false exact path.
+Outcome projection also rebases cwd-dependent compatibility arguments, clause
+elements, redirects, and attribution to an exact occurrence cwd. Unknown joins
+clear those resolutions and retain the `<dynamic-cwd>` marker. Decoded child
+hosts retain inherited invocation-cwd attribution on their compatibility
+leaves while isolating child exit state.
+
 Stable v0.3 continues to defer `do`, `switch`, functions, definitions,
 class/type bodies, and arbitrary execution-bearing expressions outside the
 bounded forms above.
@@ -775,6 +823,14 @@ the values those parameters consume do **not** advance the index. So in
 The colon form `-Name:value` (§5) always binds — `-Name` is value-binding,
 `value` its value — regardless of the tables below.
 
+PowerShell accepts U+2013 EN DASH, U+2014 EM DASH, and U+2015 HORIZONTAL BAR
+in place of the leading ASCII parameter dash. Stable v0.3 deliberately fails
+those forms atomically. The retained v0.2 `Arg.IsFlag` member derives from an
+ASCII `-` in verbatim `Arg.Raw`; treating an alternate dash as a positional
+literal is unsafe, while normalizing `Raw` would violate source provenance.
+Support therefore requires a later additive representation that can preserve
+both facts.
+
 #### 6.5.2 The binding tables
 
 Two case-insensitive static tables drive the decision, keyed by
@@ -1126,8 +1182,12 @@ interprets the block.
 PowerShell `$()` runs in the current runspace scope. A `Set-Location` inside a
 subexpression affects later inner commands, the containing command after value
 evaluation, and following outer commands. Unknown location mutations propagate
-as unknown. This differs from Bash command substitution, whose state is
-isolated from the containing shell.
+as unknown. Because `Set-Location` can fail, an ungated statement sequence also
+joins the prior location; a success-gated `&&` continuation may use the proved
+new location. The v0.2 compatibility leaf remains authored evidence, while the
+v0.3 occurrence analysis is the failure-aware security fact and sanitizes stale
+exact compatibility attribution. This differs from Bash command substitution,
+whose state is isolated from the containing shell.
 
 `OpaqueRegionScanner` is grammar-agnostic but escapes on backslash; the
 PowerShell script-block, array, and hash paths give it a backtick-escape mode
@@ -1247,12 +1307,17 @@ missing payloads, and ambiguous parameter binding set
 `ParsedCommand.IsUnparseable = true`; an incoming pipeline is dynamic even
 when an explicit literal argument also appears. These rules prevent a clean,
 persistently approvable `Invoke-Expression` clause from hiding runtime code.
-Because computed code can call `Set-Location` in the current scope, a direct
-dynamic payload also makes location attribution dynamic for every following
-relative path.
+Because computed code can mutate variables, aliases, functions, modules, and
+location in the current scope, a direct dynamic payload invalidates every
+following binding and command-resolution proof and makes location attribution
+dynamic for every following relative path. The same rule applies to `iex`, a
+static call-operator spelling, and the supported module-qualified spelling.
 
 The dot-source invocation operator and unsupported module-qualified cmdlets
-are unparseable rather than being exposed under a misleading raw verb. The
+are unparseable rather than being exposed under a misleading raw verb. This
+validation applies independently to every simple command inside structural
+lists, pipelines, loops, groups, and substitutions, including built-in
+cmdlets such as `Tee-Object` whose verb is not in the approved-verb table. The
 one supported module-qualified wrapper remains
 `Microsoft.PowerShell.Utility\Invoke-Expression`. A quoted string is a command
 identity only when preceded by the call operator `&`; otherwise it is an

SPEC.md

@@ -318,7 +318,35 @@ 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.
+independent initial-runspace assertion. A computed `Invoke-Expression` payload
+can mutate every one of those facts in the current runspace; it therefore
+invalidates later binding and command-resolution proofs and makes later cwd
+attribution unknown.
+
+Variable mutation recognition includes argument-vector binding, not only the
+invoked verb. The PowerShell common parameters `-OutVariable` / `-ov`,
+`-PipelineVariable` / `-pv`, `-ErrorVariable` / `-ev`, `-WarningVariable` /
+`-wv`, and `-InformationVariable` / `-iv`, including accepted unambiguous
+prefixes and inline `:` values, invalidate later observing proofs. The same
+rule covers PowerShell 7 variable-writing parameters on `Tee-Object`,
+`Import-LocalizedData`, `Invoke-RestMethod`, and `Invoke-WebRequest`. An opaque
+splat can supply any of those parameter keys and therefore also invalidates
+later proofs. A recognized writer on `Set-Location` composes with its
+success/failure cwd transfer and invalidates bindings on both reachable
+outcomes; location analysis does not bypass argument-vector mutation. This
+check is conservative for a command whose runtime command
+type is unavailable; treating a possible native argument as a writer can
+cause a prompt, but ignoring an advanced-function writer can authorize a stale
+value.
+
+PowerShell also accepts U+2013 EN DASH, U+2014 EM DASH, and U+2015 HORIZONTAL
+BAR as parameter prefixes. Stable v0.3 fails a token beginning with one of
+those alternate dashes atomically rather than exposing it as a literal
+positional argument: the retained v0.2 `Arg.IsFlag` contract recognizes only
+an ASCII `-`, so normalizing the authored `Raw` spelling would either lose
+provenance or require a breaking API change. Unsupported module-qualified
+cmdlets are likewise rejected inside structural regions, not only in a flat
+command; the existing module-qualified `Invoke-Expression` exception remains.
 
 For a successful result, every authored simple command appears once in
 `Syntax`, once in `Commands`, and once in `Clauses`, with all three projections
@@ -696,6 +724,53 @@ its static resolution. In particular, compatibility projection may not retain
 the configured `$HOME` resolution after a loop binds `HOME`, even though that
 binding is outside the v0.3 supported-name boundary.
 
+#### PowerShell bounded `foreach` state
+
+PowerShell `foreach` analysis owns a case-insensitive persistent binding map;
+the structural parser does not push and restore lexical loop bindings. A proved
+nonempty ordered plan leaves the final assigned value after the loop, including
+when a nested loop reuses the same name. A proved empty plan performs no body
+transition and preserves the incoming binding and cwd. A zero-or-more plan
+joins its zero-iteration entry with every reachable iteration exit. Repeated
+visits to one authored occurrence join effective argument and cwd facts rather
+than selecting a representative visit.
+
+Concrete and fixed-point PowerShell loop visits share the parse-wide 4096
+transition budget. Overflow makes the complete parse unparseable and publishes
+no partial command or compatibility projection.
+
+`Set-Location` is modeled from the complete effective argument vector. Its
+success exit takes the proved filesystem target cwd and its failure exit retains
+the incoming cwd. A successful non-filesystem or unproved target also
+invalidates binding and command-resolution proofs because relative provider
+operations may mutate that state. `&&` consumes only success, `||` only failure, and statement
+sequence consumes their join. The analyzer publishes no finite cwd set, so any
+disagreement becomes `Unknown`. Unsupported location-stack operations,
+state/command-resolution mutation, and dynamic dispatch remain fail closed.
+For provider-capable item mutators, a target that cannot be proved outside the
+Alias, Function, Variable, and Environment providers invalidates binding
+proofs; a dynamic value with a proved filesystem target does not.
+
+PowerShell `$()` and parenthesized groups propagate supported state in the
+current runspace. Decoded child hosts isolate their exit state and do not
+inherit the isolated initial-state assertion unless their own invocation proves
+it. Compatibility parse-time location attribution is cloned for loop iterator
+and body parsing: a proved empty body cannot leak a location change, while a
+possibly reached loop mutation poisons any stale exact compatibility
+attribution rather than choosing one execution path.
+
+After outcome analysis, cwd-dependent compatibility arguments, clause
+elements, redirects, and cwd attribution are rebased to the occurrence's exact
+cwd. When the occurrence cwd is unknown, cwd-dependent resolutions are cleared
+and attribution uses the existing `<dynamic-cwd>` marker. A success-path parse
+location therefore cannot leak into an exact failure continuation. Decoded
+child-host leaves retain their inherited invocation-cwd attribution for this
+projection even though child exit state remains isolated.
+
+Correcting a v0.2 compatibility `Redirect` does not by itself mark the v0.3
+occurrence complete. Occurrence-level redirect value completeness remains
+governed by the explicit redirect analysis contract below.
+
 ### Explicit redirect analysis (v0.3)
 
 Occurrence-specific redirect analysis is additive. The existing `Redirect`