Promote PowerShell value and state analysis

IMPLEMENTATION_PLAN.md

@@ -256,7 +256,7 @@ 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 owns all 422 entries and round-trips them exactly,
+      The PowerShell manifest owns all 491 entries and round-trips them exactly,
       including case-specific isolated-state inputs. Explicit false/null
       assertions remain opt-in and generator-preserved.
 - [x] Promote the remaining 21 stable Bash design cases into the executable
@@ -269,6 +269,36 @@ priorities.
       sparse exact/unknown effective-value overlays, and pins quoted, escaped,
       and continued tilde-prefix behavior against Bash. The PowerShell promotion
       half keeps OpenSpec task 1.10 open.
+- [x] Promote the first 22 stable PowerShell design cases covering value,
+      path, and redirect provenance. Exact effective values are published only
+      when parser-owned fragments prove the post-lexical value; runtime
+      automatic parameters and active wildcards remain Unknown. The sparse
+      overlay omits ordinary literals, distinguishes quoted from active tilde
+      and wildcard syntax, preserves provider and PSDrive spellings, and keeps
+      redirect resolution separate from command arguments. Local PowerShell
+      probes and direct tests pin that native tilde expansion preserves the
+      configured home string byte-for-byte, including root and trailing
+      separators. Adversarial review added 47 executable-corpus cases that
+      separate mutable `$HOME`, configured tilde expansion, process-environment
+      child initialization, current provider location, and default-versus-
+      isolated command binding; re-evaluate redirect targets from occurrence-
+      local state; and invalidate home, cwd, environment, and command-binding
+      facts after uninspected `.ps1` execution. Decoded wrappers rebuild value
+      provenance from preserved inner raw spelling, reset child-process state,
+      retain explicit native/script binding candidates only when constrained
+      command-resolution state proves them unshadowed, clear profile-mutable
+      automatic HOME and environment facts, and carry a bounded
+      invocation-owner depth for current, intermediate, and root-owned
+      redirects. Parser-owned binding provenance now distinguishes path-shaped
+      native/script candidates, constrained cmdlets and aliases, and ambiguous
+      unqualified hyphenated names without reparsing verb spelling. Script
+      blocks are excluded from host effective argv, and
+      unknown non-pipeline receivers retain visible, incomplete bodies and
+      invalidate subsequent state without discarding v0.2 leaves; unproved
+      pipelines fail atomically. Authorization completeness now requires the
+      explicit constrained command-resolution baseline, including after
+      decoded-host boundaries. Execution-region and loop/state design promotions remain, so
+      OpenSpec task 1.10 stays open.
 - [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
@@ -514,15 +544,20 @@ priorities.
       Stable v0.3 stops at the delivered Start-Job, Parallel, and remote/session
       boundaries. Optional-module Start-ThreadJob and exact deferred
       breakpoint/event/completion actions are post-v0.3 catalog work; unknown
-      receivers continue to expose incomplete bodies. Script blocks consumed
+      receivers continue to expose supported non-pipeline bodies as incomplete;
+      unproved interior pipelines fail atomically. Script blocks consumed
       by a proved canonical, alias, or supported module-qualified `Write-Output`
       receiver now remain opaque data under constrained, bounded command-
       resolution state. Unknown receivers and exact identities changed by
       observed alias mutation expose incomplete executable bodies instead.
       Generated corpus entries 418-422 pin proved data, the fail-closed unknown
       receiver, proved local `Invoke-Command`, and the exact module-qualified-
       looking and canonical-target alias boundaries; unsupported potentially
-      executable interiors still fail atomically. Local PowerShell 7.6.4 probes pin variable-versus-location
+      executable interiors still fail atomically. Static current-scope
+      `Invoke-Expression` cloning preserves cmdlet/native binding provenance;
+      paired direct, unit, and executable-corpus cases pin cmdlet tilde and
+      wildcard values plus native tilde expansion while decoded child hosts
+      remain unknown. Local PowerShell 7.6.4 probes pin variable-versus-location
       independence, semantic phase order, child process/runspace boundaries,
       boundaries and the fact that the in-process `Invoke-Command` parameter
       set does not support `-AsJob`.

PROJECT_CONTEXT.md

@@ -87,7 +87,8 @@ zero-native-deps .NET parser sized to what security gates actually need.
   origin/phase/timing/cardinality facts remain separate from
   shell-specific variable, location, command-resolution, runspace, and process
   state analysis; proved script-block data stays opaque and unknown receivers
-  conservatively expose incomplete bodies.
+  conservatively expose supported non-pipeline bodies as incomplete. An
+  unproved pipeline inside such a region fails the whole parse atomically.
 - Add fixed, non-executing value and state analysis: at most 32 candidates, at
   most 16 structural container levels, and the existing wrapper depth of 5.
 - Deliver Bash `for ... in` and PowerShell `foreach` in stable v0.3. Condition

SPEC.POWERSHELL.md

@@ -363,7 +363,8 @@ quoted_string    := single_quoted | double_quoted
   `DynamicSkip` leaf. Script blocks are classified after command and parameter
   binding: cataloged execution-bearing bindings create typed regions,
   cataloged data bindings remain opaque, and unknown receivers create unknown
-  incomplete regions with visible bodies. An `@()` or `@{}` value with execution-bearing content is
+  incomplete regions whose supported non-pipeline bodies remain visible. An
+  unproved pipeline inside such a region fails atomically. An `@()` or `@{}` value with execution-bearing content is
   unparseable until that expression form has complete command discovery;
   a non-executing literal form may remain an opaque value.
 - Under v0.2, control-flow keywords fall outside the grammar. Stable v0.3 owns
@@ -380,7 +381,8 @@ language keyword only at statement position when followed by `(`;
 bounded non-executing parenthesized argument remains opaque. A script-block
 argument is classified by its proved receiver and parameter binding: executing
 bindings create regions, proved data remains opaque, and unknown receivers
-create unknown incomplete regions. It is not reinterpreted as a loop body.
+create unknown incomplete regions for supported non-pipeline bodies. An
+unproved interior pipeline fails atomically. It is not reinterpreted as a loop body.
 `&&` and `||` join pipelines, not
 control-flow statements, so
 they cannot precede or follow `foreach`; `;` and newline remain legal statement
@@ -451,6 +453,18 @@ 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.
+An uncontrolled child profile can mutate automatic `$HOME` and environment
+variables before the payload runs, so decoded children do not inherit exact
+facts for `$HOME` or `$env:USERPROFILE`. Provider/native tilde initialization
+is tracked independently. Path-shaped command names are also shadowable by
+aliases; an explicit native or `.ps1` spelling is a binding candidate, not an
+identity proof, until constrained command-resolution state proves it
+unmodified. Default ambient uncertainty preserves ordinary v0.2 compatibility
+leaves, but it leaves the v0.3 authorization occurrence incomplete and
+binding-dependent effective values unknown. An unproved
+invocation may be arbitrary in-process code, so it invalidates subsequent
+observable state; an unproved pipeline fails atomically until pipeline state
+propagation is modeled.
 Recognized variable, alias, function, or module mutation invalidates later
 proofs in every observing scope; cwd-only mutation retains the independent
 initial-state assertion.
@@ -506,9 +520,10 @@ A script block passed to a command remains an authored `DynamicSkip` argument
 on the host `Clause`. After canonical command and parameter binding, a proved
 execution-bearing block additionally creates an attached
 `ExecutionRegionSyntax`; a proved data block does not. An unknown receiver or
-ambiguous binding conservatively creates an unknown incomplete region so every
-body command remains visible. If that body cannot be parsed completely, the
-whole result is unparseable.
+ambiguous binding conservatively creates an unknown incomplete region. Every
+command in a completely parsed supported non-pipeline body remains visible. If
+the body cannot be parsed completely, or it contains a pipeline whose stage
+identity is unproved, the whole result is unparseable.
 
 The version-pinned PowerShell 7 catalog covers:
 
@@ -562,8 +577,9 @@ Optional-module `Start-ThreadJob` and deferred breakpoint, event, and argument-
 completion receivers are not stable-v0.3 catalog-completeness promises.
 Existing conservative recognition may remain, but additional module/version or
 trigger-time proof does not gate the release. Every unproved form follows the
-unknown-receiver rule: completely parsed bodies remain visible with incomplete
-execution and state facts.
+unknown-receiver rule: supported non-pipeline bodies remain visible with
+incomplete execution and state facts, while an unproved interior pipeline
+fails atomically.
 
 Aliases, supported module-qualified spellings, static call-operator spellings,
 parameter abbreviations and inline values, positional binding, parameter-set
@@ -1180,6 +1196,13 @@ unterminated `${...}` interpolation makes the entire result unparseable.
 Adjacent fragments after a redirect operator form one target; the suffix is
 never emitted as an unrelated argument.
 
+Exact `$HOME` and `$env:USERPROFILE` composition requires the corresponding
+current-runspace or environment fact. A decoded child with uncontrolled profile
+startup has neither fact even when its parent was analyzed under the isolated
+mode. Native-versus-cmdlet path interpretation likewise requires constrained,
+unmutated command resolution; PowerShell permits aliases whose names are
+explicit native or `.ps1` paths.
+
 When every fragment, transformation, binding fact, cwd/home fact, and
 consumer fact is exact, mixed literal and expandable fragments compose to one
 exact compatibility result rather than becoming `DynamicSkip`. Any opaque or

SPEC.md

@@ -335,6 +335,19 @@ Current-runspace regions such as `( ... )`, `$()`, and a static
 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`.
+The decoded child also does not inherit exact `$HOME` or environment-variable
+facts: an uncontrolled profile can mutate either before the payload runs.
+Configured provider/native tilde state remains a separate process-initialization
+fact. An explicit native or `.ps1` path spelling supplies only an argument-
+binding candidate because PowerShell aliases can shadow path-shaped names; the
+candidate becomes a proof only under constrained, unmutated command-resolution
+state. Default ambient uncertainty alone does not invent an observed mutation
+or discard the v0.2 compatibility leaves. It does make the v0.3 authorization
+occurrence incomplete because command identity is
+not proved; binding-dependent effective values remain `Unknown` as well. Since
+that occurrence may resolve to arbitrary in-process code, subsequent observable
+runspace state is unknown. An unproved pipeline fails atomically until pipeline
+state propagation is modeled.
 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

docs/CONSUMER_GUIDE.md

@@ -243,11 +243,15 @@ Unmodeled unquoted `time`, `!`, `coproc`, and `{ ...; }` syntax follows the
 same rule because those constructs can hide nested or current-shell execution;
 quoted spellings and external `/usr/bin/time` do not acquire reserved syntax.
 
-PowerShell `foreach` value proofs require the parallel but shell-specific
+PowerShell authorization 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
+still expose supported non-pipeline structure and preserve v0.2 compatibility
+leaves, but ambient typed, validated, read-only, scoped, alias, function, and
+module state prevents both a closed-world binding proof and a complete v0.3
+command-identity proof. An unproved invocation invalidates subsequent cwd,
+value, redirect, and command-resolution facts; an unproved pipeline fails
+atomically until pipeline state propagation is modeled. 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
@@ -263,6 +267,8 @@ var parser = new PwshParser(new PwshParserOptions
 });
 ```
 
+Approval reuse based on `ParsedCommand.Commands` therefore requires this
+constrained command-resolution baseline, not merely a loop-value assertion.
 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