Prove PowerShell script block data safely

Author: Aaronontheweb

IMPLEMENTATION_PLAN.md

@@ -256,10 +256,9 @@ 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 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.
+      The PowerShell manifest owns all 422 entries and round-trips them exactly,
+      including case-specific isolated-state inputs. 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
@@ -402,7 +401,7 @@ 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 393-entry executable corpus. Remote/session/SSH/VM/container
+      by the generated 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
@@ -437,8 +436,10 @@ priorities.
       facts. Supported catalog-owned module qualifications now pass structural
       admission because every possible body remains visible; the occurrence
       analyzer still withholds typed receiver facts after an observed command-
-      resolution mutation unless the authored module qualification proves the
-      identity independently. The first direct-operator sub-slice now handles
+      resolution mutation unless bounded mutation provenance proves the exact
+      authored spelling unaffected. PowerShell permits an exact alias whose
+      name looks module-qualified, so module qualification is not independent
+      identity proof. The first direct-operator sub-slice now handles
       currently supported command interiors in typed synchronous `& {}` and
       `. {}` regions without synthetic host commands. It isolates ordinary
       direct-call binding and command-resolution exit mutation, invalidates
@@ -503,10 +504,15 @@ 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. Preserve script blocks proved
-      to be data as opaque values, expose ambiguous bodies with incomplete
-      facts, and fail atomically when any potentially executable interior is
-      unsupported. Local PowerShell 7.6.4 probes pin variable-versus-location
+      receivers continue to expose incomplete bodies. 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
       independence, semantic phase order, child process/runspace boundaries,
       boundaries and the fact that the in-process `Invoke-Command` parameter
       set does not support `-AsJob`.

SPEC.POWERSHELL.md

@@ -568,6 +568,11 @@ execution and state facts.
 Aliases, supported module-qualified spellings, static call-operator spellings,
 parameter abbreviations and inline values, positional binding, parameter-set
 selection, and `ScriptBlock[]` binding resolve through the same static catalog.
+Catalog lookup is not identity proof: PowerShell permits an alias whose exact
+name looks module-qualified. A constrained baseline plus bounded mutation
+provenance must prove the authored spelling unchanged before a catalog entry
+can classify a script block as non-executing data. Mutation matching covers
+both the authored spelling and its known canonical alias target.
 PowerShell's special multiple-script-block binding for `ForEach-Object` assigns
 Begin, Process, and End phases semantically; authored syntax and occurrence
 projection remain in source order while the analyzer schedules phases in

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

@@ -435,6 +435,11 @@ follow the unknown-receiver rule and retain visible bodies with incomplete
 facts. Aliases, supported module-qualified spellings, static call
 operator spellings, parameter abbreviations/inline values, positional binding,
 parameter sets, and `ScriptBlock[]` binding use the same static catalog.
+Catalog lookup is separate from identity proof: PowerShell permits an alias
+whose exact name looks module-qualified. A constrained baseline plus bounded
+mutation provenance must prove the authored spelling unchanged before a
+catalog entry can hide a script block as data. Mutation matching covers both
+the authored spelling and its known canonical alias target.
 
 An unknown receiver or ambiguous binding is over-approximated as an execution
 region with unknown facts. Its body commands remain visible and affected

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

@@ -860,6 +860,17 @@ SHALL fail closed to every unproved command name.
 - **THEN** their execution-region facts and observing continuation are incomplete
 - **THEN** an unsupported body interior makes the whole result unparseable
 
+#### Scenario: Module-qualified-looking data receiver is shadowable
+- **WHEN** isolated-mode PowerShell assigns alias name `Microsoft.PowerShell.Utility\Write-Output` to `Invoke-Command` and then invokes that exact spelling with `{ Remove-Item target.txt }`
+- **THEN** static catalog lookup does not independently prove the receiver identity
+- **THEN** the `Remove-Item` body remains visible in an unknown incomplete execution region
+- **THEN** an unrelated exact alias mutation does not invalidate a different catalog spelling
+
+#### Scenario: Canonical alias-target mutation invalidates authored alias
+- **WHEN** isolated-mode PowerShell reassigns `Write-Output` to `Invoke-Command` and then invokes `echo { Remove-Item target.txt }`
+- **THEN** receiver proof matches the mutation against canonical `Write-Output` as well as authored `echo`
+- **THEN** the `Remove-Item` body remains visible in an unknown incomplete execution region
+
 ### Requirement: Unknown analysis remains policy-sensitive
 An unknown value SHALL identify the occurrence and position it affects so a
 consumer can determine whether command identity, option parsing, path scope,

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

@@ -230,9 +230,17 @@
     boundaries conservatively. Additional optional-module `Start-ThreadJob`
     proof is not a stable-v0.3 requirement; unproved forms follow the unknown-
     receiver rule.
-  - [ ] 7.5e Keep proved non-executing script-block data opaque; over-approximate
+  - [x] 7.5e Keep proved non-executing script-block data opaque; over-approximate
     unknown receivers/bindings as unknown incomplete regions; fail atomically
     on unsupported interiors or state transfers.
+    - Isolated-state canonical, alias, and supported module-qualified
+      `Write-Output` receivers keep script blocks opaque only while bounded
+      command-resolution state proves that exact authored spelling unchanged.
+      PowerShell permits an alias whose name is itself module-qualified-looking,
+      so default state or a matching observed mutation downgrades to an unknown
+      incomplete region. Executable-corpus entries pin proved data, an unknown
+      receiver, proved local `Invoke-Command`, the exact module-qualified-
+      looking alias boundary, and canonical-target invalidation through `echo`.
   - [ ] 7.5f Pin authored projection order separately from semantic phase order,
     exact host element coordinates, nested regions, wrappers, pipelines, loops,
     and the 16-container depth boundary.
@@ -241,8 +249,9 @@
     grammar is not required for stable v0.3.
 - [ ] 7.6 Add adversarial cases for object-valued iterables, mutation, dynamic invocation, splatting, and cap overflow.
 - [ ] 7.7 Add PowerShell corpus entries, live `pwsh` oracle coverage, and Netclaw integration cases.
-  - Add case-specific `PwshInitialStateMode` support to `PwshCorpusTool` before
-    folding isolated-state entries 362+ into its generated manifest.
+  - `PwshCorpusTool` now supports case-specific `PwshInitialStateMode`; keep
+    promoting the remaining stable execution-region and adversarial cases into
+    its generated manifest, then add the Netclaw PowerShell policy matrix.
 
 ## 10. Heredoc / Here-String Slice