Add explicit PowerShell redirect analysis

IMPLEMENTATION_PLAN.md

@@ -318,8 +318,32 @@ priorities.
       they join multi-digit sources. Exact file targets now complete their
       containing occurrence, while cwd or value uncertainty still downgrades
       the redirect and occurrence after abstract-state joins. Direct lexer and
-      parser tests plus executable corpus cases pin the boundary. Next map the
-      PowerShell stream model, then prove the paired Netclaw redirect matrix.
+      parser tests plus executable corpus cases pin the boundary. Next prove
+      the paired Netclaw redirect matrix.
+- [x] Deliver occurrence-level PowerShell explicit redirect facts while
+      preserving the v0.2 compatibility projection. File output and append
+      retain default, numbered, or all-streams sources; the native-only merge
+      grammar preserves sources `2`–`6` or `*` and target descriptor `1`.
+      File targets remain complete when their value domain is Unknown, and an
+      isolated bounded `foreach` can promote redirect targets to exact or
+      finite absolute-path domains without publishing them as command
+      arguments. Live PowerShell 7.6.4 oracle cases correct two obsolete
+      grammar assumptions: `<` is reserved, and `1>&1`, `2>&3`, and `2>&-`
+      are syntax errors. `$null` remains explicit but incomplete because the
+      locked public operation vocabulary has no discard-sink member. Direct
+      tests and the generated executable corpus pin static, dynamic,
+      malformed, multiple, all-streams, merge, suffix-boundary, and loop-bound
+      cases. Adversarial review additionally forced outer wrapper redirect
+      provenance through cwd success/failure joins, native duplicate-source
+      rejection, identical `$null` / `${null}` sink handling, and removal of
+      stale parse-time cwd targets from unreachable relative redirects while
+      retaining cwd-independent absolute targets. A follow-up review also
+      separated parent-owned outer wrapper redirect provenance from decoded
+      child scope, preserving finite parent-loop targets without relaxing the
+      child command's independent completeness. A fourth review extended that
+      ownership through nested quoted and encoded child hosts: the outer
+      redirect now uses the outermost authoring invocation rather than the
+      nearest decoded child. Next prove the paired Netclaw redirect matrix.
 - [ ] 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,

SPEC.POWERSHELL.md

@@ -295,9 +295,9 @@ value            := word | quoted_string | here_string
                   | hash_literal         // @{ ... }  -> DynamicSkip Arg
                   | splat                // @var      -> DynamicSkip Arg
 redirect         := redirect_op target
-redirect_op      := ">" | ">>" | "<"
+redirect_op      := ">" | ">>"
                   | STREAM ">" | STREAM ">>"          // STREAM in {1..6, *}
-                  | STREAM ">&" STREAM                 // stream merge (2>&1)
+                  | MERGE_SOURCE ">&1"                 // MERGE_SOURCE in {2..6, *}
 target           := word | quoted_string | supported_subexpression | "$null"
 supported_subexpression := "$(" command ")"
 dynamic_command_name := variable | quoted_string | supported_subexpression
@@ -616,9 +616,17 @@ 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
+clear those resolutions and retain the `<dynamic-cwd>` marker. Explicit
+redirect targets also become Unknown unless provenance proves that the target
+is cwd-independent; an unreachable body never borrows the parse-time cwd.
+Decoded child
 hosts retain inherited invocation-cwd attribution on their compatibility
-leaves while isolating child exit state.
+leaves while isolating child exit state. A redirect authored outside the
+decoded wrapper payload is evaluated in the invocation scope before child
+launch, so its target may use a bounded parent-loop binding; redirects authored
+inside the decoded payload continue to use child scope. When decoded child
+hosts are nested, an outer redirect retains the outermost invocation scope
+that authored it rather than binding to the nearest decoded child scope.
 
 Stable v0.3 continues to defer `while`, `if`, `elseif`, `else`, `do`, `switch`,
 functions, definitions, class/type bodies, and arbitrary execution-bearing
@@ -727,11 +735,18 @@ Operators terminate the current token without surrounding whitespace —
 
 ### Redirect tokenization
 
-Recognized redirect operators, longest-match first: `>`, `>>`, `<`; `N>` and
+Recognized redirect operators, longest-match first: `>`, `>>`; `N>` and
 `N>>` for stream `N` in `{1,2,3,4,5,6}`; `*>` and `*>>` (all streams); and
-the stream-merge form `N>&N` (e.g. `2>&1`). A redirect target of `$null` is
-recognized as the discard sink. §8 covers how stream numbers map onto the
-`RedirectDirection` enum.
+the stream-merge forms `N>&1` for source stream `N` in `{2,3,4,5,6}` and
+`*>&1`. PowerShell reserves `<` for future use, success stream `1` cannot be
+a merge source, and merge targets other than success stream `1` are syntax
+errors. A redirect target of `$null` or `${null}` is recognized as the discard
+sink. §8 covers how stream numbers map onto the `RedirectDirection` enum.
+
+One command may redirect each source at most once. The unnumbered output
+source and explicit stream `1` are the same source; a merge and a file redirect
+also conflict when they consume the same numbered source. `*` remains its own
+source and may coexist with a numbered redirect, matching native PowerShell.
 
 ---
 
@@ -1098,8 +1113,9 @@ with the PowerShell-specific steps below. Resolution order:
    makes subsequent relative paths `DynamicSkip` (the working-directory-
    unknown mechanism, `SPEC.md` §9).
 
-A redirect target of `$null` sets `Redirect.IsDynamicSkip = true` — it is
-the discard sink, not a file; do not resolve it. The `LooksLikePath`
+A redirect target of `$null` or `${null}` sets
+`Redirect.IsDynamicSkip = true` — it is the discard sink, not a file; do not
+resolve it. The `LooksLikePath`
 heuristic (`SPEC.md` §8) additionally recognizes a leading `FileSystem::` /
 `Microsoft.PowerShell.Core\FileSystem::` qualifier.
 
@@ -1174,22 +1190,24 @@ about which stream produced it:
 
 | PowerShell redirect | `RedirectDirection` |
 |---|---|
-| `<` | `In` |
 | `>`, `1>` | `Out` |
 | `>>`, `1>>` | `Append` |
 | `2>` | `ErrOut` |
 | `2>>` | `ErrAppend` |
 | `3>`–`6>`, `*>` | `Out` (lossy — warning/verbose/debug/information/all) |
 | `3>>`–`6>>`, `*>>` | `Append` (lossy) |
-| stream merge `N>&M` (`2>&1`, `3>&1`, ...) | `ErrOut` when `N` is `2`, else `Out`; `Target` carries `&M` verbatim with `IsDynamicSkip=true` |
+| stream merge `N>&1` for `N` in `2`–`6`, or `*>&1` | `ErrOut` when `N` is `2`, else `Out`; `Target` carries `&1` verbatim with `IsDynamicSkip=true` |
 
 The table above remains the v0.2 `Redirect` compatibility mapping. v0.3 also
 populates `RedirectAnalysis`: `RedirectSourceKind.PowerShellAllStreams`
 preserves `*`, `Descriptor` preserves numeric streams, and `Operation`
-distinguishes file input/output/append from static descriptor duplication,
-close, and move. Static descriptor operations are not path-relevant. A
-variable, substitution, malformed suffix, or otherwise computed descriptor
-target remains unknown or incomplete rather than becoming a static exemption.
+distinguishes file output/append from static descriptor duplication. Static
+descriptor operations are not path-relevant. PowerShell's grammar does not
+admit descriptor close, move, computed merge targets, or file input
+redirection; those spellings make the whole parse unparseable. `$null` and
+`${null}`
+remains an incomplete explicit redirect until the public operation vocabulary
+has a discard-sink representation; consumers must continue to fail closed.
 
 ---
 

docs/CONSUMER_GUIDE.md

@@ -408,6 +408,58 @@ PowerShell streams 3-6 and `*>` currently map lossily onto the shared redirect
 enum. The target remains available for path policy, but consumers must not use
 `RedirectDirection` to recover the exact original PowerShell stream.
 
+In v0.3, authorize the parser-owned facts on every occurrence instead of
+re-parsing `ClauseElement.Raw` or the compatibility target:
+
+```csharp
+foreach (var redirect in occurrence.Redirects)
+{
+    if (!redirect.IsComplete)
+    {
+        return GateDecision.Prompt("redirect analysis is incomplete");
+    }
+
+    if (!redirect.IsPathRelevant)
+    {
+        EvaluateDescriptorOperation(
+            redirect.Source,
+            redirect.Operation,
+            redirect.TargetDescriptor);
+        continue;
+    }
+
+    if (redirect.Target.Kind is not (
+            ShellValueDomainKind.Exact or ShellValueDomainKind.FiniteSet))
+    {
+        return GateDecision.Prompt("redirect path is unknown");
+    }
+
+    foreach (var path in redirect.Target.Values)
+    {
+        EvaluatePath(path);
+    }
+}
+```
+
+Completeness and value precision are intentionally independent. For example,
+`Get-Date > $name` has a complete file-output operation with an `Unknown`
+target, so path policy still prompts. Under a caller-enforced isolated
+PowerShell initial state, `foreach ($f in @('one.txt','two.txt')) {
+Write-Output x > $f }` can instead expose a finite set of two absolute target
+paths. The loop target is not added to `EffectiveArguments`, because a
+redirect operand is not part of the command's argv.
+
+PowerShell stream facts retain numbered sources and the all-streams selector:
+`3>&1` is a complete non-path descriptor duplication from stream `3` to stream
+`1`, while `*>&1` retains `PowerShellAllStreams`. PowerShell itself rejects
+`< input.txt`, `1>&1`, `2>&3`, and `2>&-`; ShellSyntaxTree therefore marks the
+whole input unparseable rather than borrowing Bash descriptor rules. `$null`
+and `${null}` remain incomplete in the v0.3 model, so consumers must prompt or
+deny until a dedicated discard-sink operation is added. Native-invalid
+duplicate sources such as `> a 1> b` and `2>&1 2> b` also make the whole parse
+unparseable; consumers never need to reconcile competing facts for one
+PowerShell source stream.
+
 ## Compounds, pipelines, and wrapped commands
 
 `ParsedCommand.Clauses` is ordered. Each clause carries the operator that
@@ -428,6 +480,11 @@ verb-based policy should authorize; the surfaced inner clauses are.
 Redirects authored on the outer PowerShell wrapper remain attached to the last
 surfaced clause, so redirect policy still sees paths such as
 `pwsh -Command "git status" > audit.log`.
+The outer redirect is evaluated by the invoking PowerShell scope before child
+launch. It can therefore retain a finite parent-loop target domain even when
+the decoded child occurrence remains incomplete for independent child-runspace
+reasons. A redirect written inside the decoded `-Command` payload uses child
+scope instead.
 
 Supported PowerShell `$()` subexpressions are structural rather than hidden
 opaque values. The containing `SimpleCommandSyntax.Substitutions` records each

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

@@ -309,6 +309,10 @@ observations on Linux:
 | Each shell redirects to its escaped-dollar spelling of `$HOME".txt"` | Each creates exactly one file named `$HOME.txt` | Adjacent redirect fragments form one target |
 | Bash redirects unquoted and quoted `*.txt` in a directory with multiple `.txt` files | The unquoted form is an ambiguous redirect; the quoted form creates the literal file `*.txt` | `BashRedirect` requires one proved target and retains quote-sensitive glob eligibility |
 | PowerShell redirects quoted `~`, `*.txt`, `FileSystem::...`, and a FileSystem PSDrive path | Tilde, wildcard, provider, and drive semantics apply after quote removal | `PowerShellRedirect` is Path-like but remains separate from cmdlet and native argument contexts |
+| PowerShell parses `2>&1`, `6>&1`, and `*>&1`, but rejects `1>&1`, `2>&3`, and `*>&2` | Only non-success numbered streams or all streams can merge into success stream `1` | Explicit facts preserve the source stream and descriptor target `1`; all other merge shapes fail closed as syntax errors |
+| PowerShell parses `<` as a reserved-token syntax error | PowerShell 7.6 has no file-input redirection operator | `<` makes the whole parse unparseable rather than producing a compatibility `In` redirect |
+| PowerShell rejects `> a > b`, `> a 1> b`, `2>&1 2> b`, and `*> a *> b`, but accepts `*> a 2> b` | Each exact source may be redirected once; default output and stream `1` are identical while `*` is independent from numbered sources | Duplicate-source validation precedes publication of compatibility or explicit facts |
+| PowerShell treats `$null` and `${null}` as the same redirect sink | Bracing does not turn the automatic null variable into a filename | Both spellings remain explicit but incomplete until the public model has a discard-sink operation |
 
 Task 2.2 converts these probes into deterministic shell-oracle regressions on
 the implementation branch; the design corpus records their desired semantic
@@ -726,10 +730,17 @@ the occurrence analyzer then supplies the authoritative exact-or-unknown cwd
 facts. Outcome projection rebases cwd-dependent compatibility arguments,
 elements, redirects, and attribution when that occurrence cwd is exact. An
 unknown occurrence cwd clears those resolutions and retains the dynamic-cwd
-marker, so a parse location taken from the success partition cannot leak into
-an exact failure continuation. Decoded child-host compatibility leaves carry
+marker. Explicit redirect targets likewise become Unknown unless their
+provenance resolves without a cwd, so a parse location taken from a success or
+unreachable partition cannot leak into an exact failure continuation. Decoded
+child-host compatibility leaves carry
 the inherited invocation-cwd attribution needed by that projection, while the
-child's exit state remains isolated. General extraction of state primitives is
+child's exit state remains isolated. Redirect provenance distinguishes an
+outer wrapper redirect evaluated by the parent before child launch from an
+inner decoded redirect evaluated in child scope; only the outer form may use a
+bounded parent-loop binding. Nested decoded hosts do not change that owner: the
+outer redirect keeps the outermost invocation context that authored it rather
+than using the nearest child context. General extraction of state primitives is
 a post-v0.3 refactor and proceeds only after both language passes demonstrate
 identical behavior.
 

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

@@ -485,6 +485,23 @@ partition merely to publish exact continuation facts.
 - **THEN** each reached body occurrence retains the exact incoming cwd
 - **THEN** a structurally present but unreachable body or continuation still receives conservative cwd facts
 
+#### Scenario: Unreachable relative redirect has no parse-time cwd proof
+- **WHEN** isolated-mode PowerShell parses `foreach ($x in @()) { Write-Output x > relative.txt }`
+- **THEN** the body occurrence and its working directory remain incomplete or Unknown
+- **THEN** the explicit redirect target is Unknown rather than the parse-time absolute path
+- **THEN** an authored absolute redirect target may remain exact because it is cwd-independent
+
+#### Scenario: Outer child-host redirect uses parent binding
+- **WHEN** isolated-mode PowerShell parses `foreach ($f in @('one.txt','two.txt')) { pwsh -Command 'Get-Date' > $f }`
+- **THEN** the outer redirect target is the finite set of two parent-cwd paths
+- **THEN** the decoded child command may remain independently incomplete because child runspace facts are not inferred
+- **THEN** an inner redirect authored inside the decoded payload does not inherit the parent loop binding
+
+#### Scenario: Nested child hosts retain outer redirect ownership
+- **WHEN** the preceding outer redirect wraps two or more static `pwsh -Command` or `-EncodedCommand` child hosts
+- **THEN** the outer redirect target still uses the parent loop binding
+- **THEN** it does not bind to the nearest decoded child invocation scope
+
 #### Scenario: Duplicate iteration values retain order
 - **WHEN** isolated-mode Bash parses `for f in a b a; do :; done; printf '%s' "$f"`
 - **THEN** the internal iteration plan retains `a`, `b`, `a` in that order

openspec/changes/v0-3-structured-shell-analysis/specs/explicit-redirect-semantics/spec.md

@@ -17,6 +17,26 @@ SHALL be incomplete.
 - **THEN** the source is explicitly PowerShell all streams
 - **THEN** the target is a path-relevant file output rather than a guessed numeric descriptor
 
+#### Scenario: PowerShell static stream merge
+- **WHEN** PowerShell parses `Get-ChildItem 3>&1`
+- **THEN** the source is descriptor `3` and the operation duplicates to descriptor `1`
+- **THEN** the target is not path-relevant
+
+#### Scenario: Unsupported PowerShell redirect grammar fails closed
+- **WHEN** PowerShell receives `< input.txt`, `1>&1`, `2>&3`, or `2>&-`
+- **THEN** the whole parse is unparseable in agreement with the native parser
+- **THEN** no compatibility or explicit redirect fact is guessed from the malformed prefix
+
+#### Scenario: Duplicate PowerShell source redirect fails closed
+- **WHEN** PowerShell receives `> a > b`, `> a 1> b`, `2>&1 2> b`, or `*> a *> b`
+- **THEN** the whole parse is unparseable because one source is redirected twice
+- **THEN** `*> a 2> b` remains valid because all streams and stream `2` are distinct authored sources
+
+#### Scenario: PowerShell null sink spellings agree
+- **WHEN** PowerShell parses either `> $null` or `> ${null}`
+- **THEN** neither spelling is published as a path-relevant file target
+- **THEN** the explicit fact remains incomplete until a discard-sink operation is represented
+
 #### Scenario: Static descriptor duplication
 - **WHEN** Bash parses `dotnet test 2>&1`
 - **THEN** the redirect operation is descriptor duplicate

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

@@ -68,16 +68,16 @@
 - [x] 4.2 Classify Bash descriptor duplication, close, and move as static only for the complete literal descriptor grammar.
 - [x] 4.3 Keep variable-driven and otherwise computed Bash descriptor targets unknown or incomplete.
 - [x] 4.4 Lex and classify Bash `&>` and `&>>` independently from background-list operators.
-- [ ] 4.5 Map existing PowerShell stream redirects into the shared explicit model without losing shell-specific stream identity.
-- [ ] 4.6 Add paired direct tests and corpus cases for static, dynamic, malformed, multiple, combined, and file redirects.
+- [x] 4.5 Map existing PowerShell stream redirects into the shared explicit model without losing shell-specific stream identity.
+- [x] 4.6 Add paired direct tests and corpus cases for static, dynamic, malformed, multiple, combined, and file redirects.
   - [x] 4.6a Add Bash direct and executable-corpus cases for static duplicate,
     close, and move; computed descriptor targets; combined output overwrite and
     append; ordinary file redirects; arbitrary numeric source descriptors; and
     overflow/malformed fail-closed boundaries. LF/CRLF continuations at the
     descriptor boundary and inside multi-digit sources follow Bash's pre-token
     removal semantics. Executable-corpus cases pin malformed atomic failure and
     independent occurrence facts for multiple redirects.
-  - [ ] 4.6b Add the paired PowerShell direct and executable-corpus cases when
+  - [x] 4.6b Add the paired PowerShell direct and executable-corpus cases when
     task 4.5 maps its stream model.
 - [ ] 4.7 Verify the explicit model removes the need for raw-prefix inference in a Netclaw integration test.